1 (*********************************************************************************************************************************)
2 (* HaskWeakToStrong: convert HaskWeak to HaskStrong *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import NaturalDeduction.
9 Require Import Coq.Strings.String.
10 Require Import Coq.Lists.List.
11 Require Import Coq.Init.Specif.
12 Require Import HaskKinds.
13 Require Import HaskLiterals.
14 Require Import HaskTyCons.
15 Require Import HaskWeakTypes.
16 Require Import HaskWeakVars.
17 Require Import HaskWeak.
18 Require Import HaskWeakToCore.
19 Require Import HaskStrongTypes.
20 Require Import HaskStrong.
21 Require Import HaskCoreVars.
23 Open Scope string_scope.
24 Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
25 Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
27 Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
31 then let fresh := @FreshHaskTyVar Γ tv in OK _
32 else φ tv' >>= fun tv'' => OK (fun TV ite => tv'' TV (weakITE ite))).
33 rewrite <- _H; apply fresh.
36 Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ)
37 : (TyVarResolver (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)).
45 Definition substPhi {Γ:TypeEnv}(κ κ':Kind)(θ:HaskType Γ κ) : HaskType (κ::Γ) κ' -> HaskType Γ κ'.
49 unfold HaskType in ht.
52 apply ICons; [ idtac | apply env ].
56 Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ.
62 inversion θ; subst; auto.
70 (* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *)
71 Record StrongAltConPlusJunk {tc:TyCon} :=
72 { sacpj_sac : @StrongAltCon tc
73 ; sacpj_φ : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_Γ sacpj_sac Γ))
74 ; sacpj_ψ : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ))
76 Implicit Arguments StrongAltConPlusJunk [ ].
77 Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon.
79 (* yes, I know, this is really clumsy *)
80 Variable emptyφ : TyVarResolver nil.
81 Extract Inlined Constant emptyφ => "(\x -> Prelude.error ""encountered unbound tyvar!"")".
83 Definition mkPhi (lv:list WeakTypeVar)
84 : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)).
85 set (upφ'(Γ:=nil) lv emptyφ) as φ'.
86 rewrite <- app_nil_end in φ'.
90 Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)).
91 Definition tyConKinds tc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (tyConTyVars tc)).
93 Definition fixkind {κ}(tv:WeakTypeVar) := weakTypeVar tv κ.
94 Notation " ` x " := (@fixkind _ x) (at level 100).
96 Ltac matchThings T1 T2 S :=
97 destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];
98 [ idtac | apply (Error (S +++ toString T1 +++ " " +++ toString T2)) ].
100 Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★).
102 unfold InstantiatedTypeEnv in ite.
107 Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★.
117 Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ).
118 refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) :=
119 addErrorMessage ("weakTypeToType " +++ toString t)
121 | WFunTyCon => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow))
122 | WTyCon tc => let case_WTyCon := tt in _
123 | WClassP c lt => let case_WClassP := tt in Error "weakTypeToType: WClassP not implemented"
124 | WIParam _ ty => let case_WIParam := tt in Error "weakTypeToType: WIParam not implemented"
125 | WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
126 | WTyVarTy v => let case_WTyVarTy := tt in φ v >>= fun v' => _
127 | WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _
128 | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody
129 >>= fun tbody' => φ (@fixkind ECKind ec) >>= fun ec' => _
130 | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt in
131 weakTypeToType _ φ t1 >>= fun t1' =>
132 weakTypeToType _ φ t2 >>= fun t2' =>
133 weakTypeToType _ φ t3 >>= fun t3' => _
135 ((fix weakTypeListToTypeList (lk:list Kind) (lt:list WeakType)
136 { struct lt } : ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV lk) :=
138 | nil => match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
139 | nil => OK (fun TV _ => TyFunApp_nil)
140 | _ => Error "WTyFunApp not applied to enough types"
142 | tx::lt' => weakTypeToType Γ φ tx >>= fun t' =>
143 match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
144 | nil => Error "WTyFunApp applied to too many types"
145 | k::lk' => weakTypeListToTypeList lk' lt' >>= fun rhtl' =>
146 let case_weakTypeListToTypeList := tt in _
149 ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in _
150 end ); clear weakTypeToType.
151 apply ConcatenableString.
153 destruct case_WTyVarTy.
154 apply (addErrorMessage "case_WTyVarTy").
156 exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))).
158 destruct case_WAppTy.
159 apply (addErrorMessage "case_WAppTy").
160 destruct t1' as [k1' t1'].
161 destruct t2' as [k2' t2'].
162 set ("tried to apply type "+++toString t1'+++" of kind "+++toString k1'+++" to type "+++
163 toString t2'+++" of kind "+++toString k2') as err.
165 try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
166 subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
167 apply (Error ("Kind mismatch in WAppTy: "+++err)).
169 destruct case_weakTypeListToTypeList.
170 apply (addErrorMessage "case_weakTypeListToTypeList").
171 destruct t' as [ k' t' ].
172 matchThings k k' "Kind mismatch in weakTypeListToTypeList".
174 apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
176 destruct case_WTyFunApp.
177 apply (addErrorMessage "case_WTyFunApp").
179 eapply haskTypeOfSomeKind.
180 unfold HaskType; intros.
181 apply (TyFunApp tc (fst (tyFunKind tc)) (snd (tyFunKind tc))).
185 destruct case_WTyCon.
186 apply (addErrorMessage "case_WTyCon").
188 eapply haskTypeOfSomeKind.
189 unfold HaskType; intros.
192 destruct case_WCodeTy.
193 apply (addErrorMessage "case_WCodeTy").
195 matchThings κ ★ "Kind mismatch in WCodeTy: ".
197 eapply haskTypeOfSomeKind.
198 unfold HaskType; intros.
200 apply (TVar (ec' TV X)).
205 destruct case_WCoFunTy.
206 apply (addErrorMessage "case_WCoFunTy").
207 destruct t1' as [ k1' t1' ].
208 destruct t2' as [ k2' t2' ].
209 destruct t3' as [ k3' t3' ].
210 matchThings k1' k2' "Kind mismatch in arguments of WCoFunTy".
212 matchThings k3' ★ "Kind mismatch in result of WCoFunTy".
215 apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
217 destruct case_WForAllTy.
218 apply (addErrorMessage "case_WForAllTy").
220 matchThings ★ κ "Kind mismatch in WForAllTy: ".
223 apply (@haskTypeOfSomeKind _ ★).
228 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
229 Section StrongAltCon.
230 Context (tc : TyCon)(dc:DataCon tc).
232 Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
233 -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
236 apply (addErrorMessage "weakTypeToType'").
237 set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
238 set (@substφ _ _ avars') as q.
239 set (upφ' (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ'.
240 set (@weakTypeToType _ φ' ct) as t.
241 destruct t as [|t]; try apply (Error error_message).
242 destruct t as [tk t].
243 matchThings tk ★ "weakTypeToType'".
246 set (@weakT'' _ Γ _ t) as t'.
247 set (@lamer _ _ _ _ t') as t''.
248 fold (tyConKinds tc) in t''.
249 fold (dataConExKinds dc) in t''.
253 unfold dataConExKinds.
254 rewrite <- vec2list_map_list2vec.
255 rewrite <- vec2list_map_list2vec.
256 rewrite vec2list_list2vec.
257 rewrite vec2list_list2vec.
261 Definition mkStrongAltCon : @StrongAltCon tc.
263 {| sac_altcon := WeakDataAlt dc
264 ; sac_numCoerVars := length (dataConCoerKinds dc)
265 ; sac_numExprVars := length (dataConFieldTypes dc)
266 ; sac_ekinds := dataConExKinds dc
267 ; sac_coercions := fun Γ avars => let case_sac_coercions := tt in _
268 ; sac_types := fun Γ avars => let case_sac_types := tt in _
271 destruct case_sac_coercions.
272 refine (vec_map _ (list2vec (dataConCoerKinds dc))).
275 unfold tyConKind in avars.
276 set (@weakTypeToType' Γ) as q.
277 unfold tyConKinds in q.
278 rewrite <- vec2list_map_list2vec in q.
279 rewrite vec2list_list2vec in q.
282 q avars w >>= fun t1 =>
283 q avars w0 >>= fun t2 =>
284 OK (mkHaskCoercionKind t1 t2)
286 | Error s => Prelude_error s
290 destruct case_sac_types.
291 refine (vec_map _ (list2vec (dataConFieldTypes dc))).
293 unfold tyConKind in avars.
294 set (@weakTypeToType' Γ) as q.
295 unfold tyConKinds in q.
296 rewrite <- vec2list_map_list2vec in q.
297 rewrite vec2list_list2vec in q.
298 set (q avars X) as y.
300 | Error s =>Prelude_error s
306 Lemma weakCV' : forall {Γ}{Δ} Γ',
308 -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
310 unfold HaskCoVar in *.
311 intros; apply (X TV CV).
312 apply ilist_chop' in env; auto.
313 unfold InstantiatedCoercionEnv in *.
314 unfold weakCK'' in cenv.
316 rewrite <- map_preserves_length in cenv.
318 rewrite <- map_preserves_length in cenv.
322 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
324 {| sacpj_sac := mkStrongAltCon
325 ; sacpj_φ := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
327 fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
331 unfold HaskCoVar in *.
336 unfold InstantiatedCoercionEnv in *.
337 apply vec_chop' in cenv.
341 Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
352 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc).
354 set (c:DataCon _) as dc.
355 set ((dataConTyCon c):TyCon) as tc' in *.
356 set (eqd_dec tc tc') as eqpf; destruct eqpf;
358 | apply (Error ("in a case of tycon "+++toString tc+++", found a branch with datacon "+++toString (dc:CoreDataCon))) ]; subst.
360 eapply mkStrongAltConPlusJunk.
364 apply OK; refine {| sacpj_sac := {|
365 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
366 ; sac_altcon := WeakLitAlt h
368 intro; intro φ; apply φ.
369 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
370 rewrite weakCK'_nil_inert. apply ψ.
371 apply OK; refine {| sacpj_sac := {|
372 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
373 ; sac_altcon := WeakDEFAULT |} |}.
374 intro; intro φ; apply φ.
375 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
376 rewrite weakCK'_nil_inert. apply ψ.
379 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
380 fun wev => match wev with weakExprVar _ t => t end.
381 Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
383 Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
385 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
386 WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
393 inversion cenv; auto.
396 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
397 Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
398 : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
399 apply (addErrorMessage ("castExpr " +++ err_msg)).
402 destruct τ' as [τ' l'].
403 destruct (eqd_dec l l'); [ idtac
404 | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
405 " got: " +++(fold_left (fun x y => y+++","+++y) (map (toString ○ haskTyVarToType) l) "")+++eol+++
406 " wanted: "+++(fold_left (fun x y => x+++","+++y) (map (toString ○ haskTyVarToType) l') "")
408 destruct (eqd_dec τ τ'); [ idtac
409 | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
410 " got: " +++toString τ+++eol+++
411 " wanted: "+++toString τ'
418 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
419 match wcv with weakCoerVar _ κ _ _ => κ end.
420 Coercion coVarKind : WeakCoerVar >-> Kind.
422 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
424 set (weakTypeToType φ t) as wt.
425 destruct wt; try apply (Error error_message).
427 matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in ").
433 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
436 | T_Leaf (Some (wev,e)) => match weakTypeToTypeOfKind φ wev ★ with
437 | OK t' => [((wev:CoreVar),t')]
440 | T_Branch b1 b2 => (varsTypes b1 φ),,(varsTypes b2 φ)
443 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
444 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
445 | nil => match wtl with
447 | _ => Error "length mismatch in mkAvars"
449 | k::lk' => match wtl with
450 | nil => Error "length mismatch in mkAvars"
452 weakTypeToTypeOfKind φ wt k >>= fun t =>
453 mkAvars wtl' lk' φ >>= fun rest =>
454 OK (ICons _ _ t rest)
458 Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool :=
465 else update_ig ig vars' v'
468 (* does the specified variable occur free in the expression? *)
469 Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
472 | WEVar cv => if eqd_dec (wev:CoreVar) (cv:CoreVar) then true else false
473 | WECast e co => doesWeakVarOccur wev e
474 | WENote n e => doesWeakVarOccur wev e
475 | WETyApp e t => doesWeakVarOccur wev e
476 | WECoApp e co => doesWeakVarOccur wev e
477 | WEBrak _ ec e _ => doesWeakVarOccur wev e
478 | WEEsc _ ec e _ => doesWeakVarOccur wev e
479 | WECSP _ ec e _ => doesWeakVarOccur wev e
480 | WELet cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
481 | WEApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
482 | WELam cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
483 | WETyLam cv e => doesWeakVarOccur wev e
484 | WECoLam cv e => doesWeakVarOccur wev e
485 | WECase vscrut escrut tbranches tc avars alts =>
486 doesWeakVarOccur wev escrut ||
487 if eqd_dec (wev:CoreVar) (vscrut:CoreVar) then false else
488 ((fix doesWeakVarOccurAlts alts {struct alts} : bool :=
490 | T_Leaf None => false
491 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
492 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
493 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
494 | T_Branch b1 b2 => doesWeakVarOccurAlts b1 || doesWeakVarOccurAlts b2
497 doesWeakVarOccur wev e ||
498 (fix doesWeakVarOccurLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) : bool :=
500 | T_Leaf None => false
501 | T_Leaf (Some (cv,e)) => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
502 | T_Branch b1 b2 => doesWeakVarOccurLetRec b1 || doesWeakVarOccurLetRec b2
505 Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
506 (alts:Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr)) : bool :=
508 | T_Leaf None => false
509 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
510 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
511 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
512 | T_Branch b1 b2 => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
515 Definition checkDistinct :
516 forall {V}(EQ:EqDecidable V)(lv:list V), ???(distinct lv).
518 set (distinct_decidable lv) as q.
521 exact (Error "checkDistinct failed").
524 (* FIXME: check the kind of the type of the weakexprvar to support >0 *)
525 Definition mkGlobal Γ (τ:HaskType Γ ★) (wev:WeakExprVar) : Global Γ.
526 refine {| glob_kinds := nil |}.
532 Definition weakExprToStrongExpr : forall
536 (ψ:CoVarResolver Γ Δ)
537 (ξ:CoreVar -> LeveledHaskType Γ ★)
541 WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
543 fix weakExprToStrongExpr
547 (ψ:CoVarResolver Γ Δ)
548 (ξ:CoreVar -> LeveledHaskType Γ ★)
552 (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
553 addErrorMessage ("in weakExprToStrongExpr " +++ toString we)
557 then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ (τ@@lev))
558 else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
560 | WELit lit => castExpr we ("WELit "+++toString lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
562 | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
563 weakTypeOfWeakExpr ebody >>= fun tbody =>
564 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
565 let ξ' := update_ξ ξ lev (((ev:CoreVar),tv)::nil) in
566 let ig' := update_ig ig ((ev:CoreVar)::nil) in
567 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>
568 castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
570 | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' =>
571 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
572 weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' =>
573 castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
575 | WEEsc _ ec e tbody => φ ec >>= fun ec'' =>
576 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
578 | nil => Error "ill-leveled escapification"
579 | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
580 >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
583 | WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage"
585 | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
587 | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>
588 weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
589 weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ lev (((v:CoreVar),tv)::nil))
590 (update_ig ig ((v:CoreVar)::nil)) τ lev ebody
592 OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
594 | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
595 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
596 weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' =>
597 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' =>
598 OK (EApp _ _ _ _ _ _ e1' e2')
600 | WETyLam tv e => let φ' := upφ tv φ in
601 weakTypeOfWeakExpr e >>= fun te =>
602 weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
603 weakExprToStrongExpr _ (weakCE Δ) φ'
604 (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
605 >>= fun e' => castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
607 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
609 | WForAllTy wtv te' =>
610 let φ' := upφ wtv φ in
611 weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>
612 weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
613 weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
614 castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
615 | _ => Error ("weakTypeToType: WETyApp body with type "+++toString te)
618 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
620 | WCoFunTy t1 t2 t3 =>
621 weakTypeToType φ t1 >>= fun t1' =>
623 haskTypeOfSomeKind κ t1'' =>
624 weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
625 weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
626 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
627 castExpr we "WECoApp" _ e' >>= fun e'' =>
628 OK (ECoApp Γ Δ κ t1'' t2''
629 (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
631 | _ => Error ("weakTypeToType: WECoApp body with type "+++toString te)
634 | WECoLam cv e => let (_,_,t1,t2) := cv in
635 weakTypeOfWeakExpr e >>= fun te =>
636 weakTypeToTypeOfKind φ te ★ >>= fun te' =>
637 weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
638 weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
639 weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ ig te' lev e >>= fun e' =>
640 castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
642 | WECast e co => let (t1,t2) := weakCoercionTypes co in
643 weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
644 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
645 weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
646 castExpr we "WECast" _
647 (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
650 let ξ' := update_ξ ξ lev _ in
651 let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
653 (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
654 : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
656 | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
657 | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e)
659 binds b1 >>= fun b1' =>
660 binds b2 >>= fun b2' =>
661 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
663 in binds >>= fun binds' =>
664 checkDistinct CoreVarEqDecidable (map (@fst _ _) (leaves (varsTypes rb φ))) >>= fun rb_distinct =>
665 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
666 OK (ELetRec Γ Δ ξ lev τ _ _ binds' e')
668 | WECase vscrut escrut tbranches tc avars alts =>
669 weakTypeOfWeakExpr escrut >>= fun tscrut =>
670 weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
671 if doesWeakVarOccurAlts vscrut alts
672 then Error "encountered a Case which actually used its binder - these should have been desugared away!!"
673 else mkAvars avars (tyConKind tc) φ >>= fun avars' =>
674 weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' =>
675 (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
676 ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac &
677 Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@ lev))}}) :=
679 | T_Leaf None => OK []
680 | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
681 mkStrongAltConPlusJunk' tc ac >>= fun sac =>
682 list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
684 (let case_pf := tt in _) >>= fun pf =>
685 let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
686 weakExprToStrongExpr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
687 (sacpj_ψ sac _ _ avars' ψ)
689 (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
690 (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
691 let case_case := tt in OK [ _ ]
693 mkTree b1 >>= fun b1' =>
694 mkTree b2 >>= fun b2' =>
696 end) alts >>= fun tree =>
698 weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
699 castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
700 end)); try clear binds; try apply ConcatenableString.
703 apply (addErrorMessage "case_some").
705 destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
706 matchThings h (unlev (ξ' wev)) "LetRec".
708 rewrite matchTypeVars_pf.
709 clear matchTypeVars_pf.
710 set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
711 destruct e''; try apply (Error error_message).
716 induction (leaves (varsTypes rb φ)).
725 set (distinct_decidable (vec2list exprvars')) as dec.
726 destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ].