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.
22 Require Import HaskCoreToWeak.
23 Require Import HaskCoreTypes.
25 Open Scope string_scope.
26 Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
27 Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
29 Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a b) c) κ) : HaskType (app a (app b c)) κ.
30 rewrite <- ass_app in lt.
34 Definition upPhi {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
38 then let fresh := @FreshHaskTyVar Γ tv in OK _
39 else φ tv' >>= fun tv'' => OK (fun TV ite => tv'' TV (weakITE ite))).
40 rewrite <- _H; apply fresh.
43 Definition upPhi2 {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ)
44 : (TyVarResolver (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)).
52 Definition substPhi {Γ:TypeEnv}(κ κ':Kind)(θ:HaskType Γ κ) : HaskType (κ::Γ) κ' -> HaskType Γ κ'.
56 unfold HaskType in ht.
59 apply ICons; [ idtac | apply env ].
63 Definition substphi {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ.
69 inversion θ; subst; auto.
77 (* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *)
78 Record StrongAltConPlusJunk {tc:TyCon} :=
79 { sacpj_sac : @StrongAltCon tc
80 ; sacpj_phi : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_gamma sacpj_sac Γ))
81 ; sacpj_psi : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_delta sacpj_sac Γ atypes (weakCK'' Δ))
83 Implicit Arguments StrongAltConPlusJunk [ ].
84 Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon.
86 (* yes, I know, this is really clumsy *)
87 Variable emptyφ : TyVarResolver nil.
88 Extract Inlined Constant emptyφ => "(\x -> Prelude.error ""encountered unbound tyvar!"")".
90 Definition mkPhi (lv:list WeakTypeVar)
91 : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)).
92 set (upPhi2(Γ:=nil) lv emptyφ) as φ2.
93 rewrite <- app_nil_end in φ2.
97 Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)).
98 Definition tyConKinds tc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (tyConTyVars tc)).
100 Definition fixkind {κ}(tv:WeakTypeVar) := weakTypeVar tv κ.
101 Notation " ` x " := (@fixkind _ x) (at level 100).
103 Ltac matchThings T1 T2 S :=
104 destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];
105 [ idtac | apply (Error (S +++ toString T1 +++ " " +++ toString T2)) ].
107 Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★).
109 unfold InstantiatedTypeEnv in ite.
114 Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★.
124 Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ).
125 refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) :=
126 addErrorMessage ("weakTypeToType " +++ toString t)
128 | WFunTyCon => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow))
129 | WTyCon tc => let case_WTyCon := tt in _
130 | WClassP c lt => let case_WClassP := tt in Error "weakTypeToType: WClassP not implemented"
131 | WIParam _ ty => let case_WIParam := tt in Error "weakTypeToType: WIParam not implemented"
132 | WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
133 | WTyVarTy v => let case_WTyVarTy := tt in φ v >>= fun v' => _
134 | WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upPhi wtv φ) t >>= fun t => _
135 | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody
136 >>= fun tbody' => φ (@fixkind ECKind ec) >>= fun ec' => _
137 | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt in
138 weakTypeToType _ φ t1 >>= fun t1' =>
139 weakTypeToType _ φ t2 >>= fun t2' =>
140 weakTypeToType _ φ t3 >>= fun t3' => _
142 ((fix weakTypeListToTypeList (lk:list Kind) (lt:list WeakType)
143 { struct lt } : ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV lk) :=
145 | nil => match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
146 | nil => OK (fun TV _ => TyFunApp_nil)
147 | _ => Error "WTyFunApp not applied to enough types"
149 | tx::lt' => weakTypeToType Γ φ tx >>= fun t' =>
150 match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
151 | nil => Error ("WTyFunApp applied to too many types"(* +++ eol +++
152 " tyCon= " +++ toString tc +++ eol +++
153 " tyConKindArgs= " +++ toString (fst (tyFunKind tc)) +++ eol +++
154 " tyConKindResult= " +++ toString (snd (tyFunKind tc)) +++ eol +++
155 " types= " +++ toString lt +++ eol*))
156 | k::lk' => weakTypeListToTypeList lk' lt' >>= fun rhtl' =>
157 let case_weakTypeListToTypeList := tt in _
160 ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in _
161 end ); clear weakTypeToType.
162 apply ConcatenableString.
164 destruct case_WTyVarTy.
165 apply (addErrorMessage "case_WTyVarTy").
167 exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))).
169 destruct case_WAppTy.
170 apply (addErrorMessage "case_WAppTy").
171 destruct t1' as [k1' t1'].
172 destruct t2' as [k2' t2'].
173 set ("tried to apply type "+++toString t1'+++" of kind "+++toString k1'+++" to type "+++
174 toString t2'+++" of kind "+++toString k2') as err.
176 try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
177 subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
178 apply (Error ("Kind mismatch in WAppTy: "+++err)).
180 destruct case_weakTypeListToTypeList.
181 apply (addErrorMessage "case_weakTypeListToTypeList").
182 destruct t' as [ k' t' ].
183 matchThings k k' "Kind mismatch in weakTypeListToTypeList".
185 apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
187 destruct case_WTyFunApp.
188 apply (addErrorMessage "case_WTyFunApp").
190 eapply haskTypeOfSomeKind.
191 unfold HaskType; intros.
192 apply (TyFunApp tc (fst (tyFunKind tc)) (snd (tyFunKind tc))).
196 destruct case_WTyCon.
197 apply (addErrorMessage "case_WTyCon").
199 eapply haskTypeOfSomeKind.
200 unfold HaskType; intros.
203 destruct case_WCodeTy.
204 apply (addErrorMessage "case_WCodeTy").
206 matchThings κ ★ "Kind mismatch in WCodeTy: ".
208 eapply haskTypeOfSomeKind.
209 unfold HaskType; intros.
211 apply (TVar (ec' TV X)).
216 destruct case_WCoFunTy.
217 apply (addErrorMessage "case_WCoFunTy").
218 destruct t1' as [ k1' t1' ].
219 destruct t2' as [ k2' t2' ].
220 destruct t3' as [ k3' t3' ].
221 matchThings k1' k2' "Kind mismatch in arguments of WCoFunTy".
223 matchThings k3' ★ "Kind mismatch in result of WCoFunTy".
226 apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
228 destruct case_WForAllTy.
229 apply (addErrorMessage "case_WForAllTy").
231 matchThings ★ κ "Kind mismatch in WForAllTy: ".
234 apply (@haskTypeOfSomeKind _ ★).
239 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
240 Section StrongAltCon.
241 Context (tc : TyCon)(dc:DataCon tc).
243 Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
244 -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
247 apply (addErrorMessage "weakTypeToType'").
248 set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
249 set (@substphi _ _ avars') as q.
250 set (upPhi2 (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ2.
251 set (@weakTypeToType _ φ2 ct) as t.
252 destruct t as [|t]; try apply (Error error_message).
253 destruct t as [tk t].
254 matchThings tk ★ "weakTypeToType'".
257 set (@weakT'' _ Γ _ t) as t'.
258 set (@lamer _ _ _ _ t') as t''.
259 fold (tyConKinds tc) in t''.
260 fold (dataConExKinds dc) in t''.
264 unfold dataConExKinds.
265 rewrite <- vec2list_map_list2vec.
266 rewrite <- vec2list_map_list2vec.
267 rewrite vec2list_list2vec.
268 rewrite vec2list_list2vec.
272 Definition mkStrongAltCon : @StrongAltCon tc.
274 {| sac_altcon := WeakDataAlt dc
275 ; sac_numCoerVars := length (dataConCoerKinds dc)
276 ; sac_numExprVars := length (dataConFieldTypes dc)
277 ; sac_ekinds := dataConExKinds dc
278 ; sac_coercions := fun Γ avars => let case_sac_coercions := tt in _
279 ; sac_types := fun Γ avars => let case_sac_types := tt in _
282 destruct case_sac_coercions.
283 refine (vec_map _ (list2vec (dataConCoerKinds dc))).
286 unfold tyConKind in avars.
287 set (@weakTypeToType' Γ) as q.
288 unfold tyConKinds in q.
289 rewrite <- vec2list_map_list2vec in q.
290 rewrite vec2list_list2vec in q.
293 q avars w >>= fun t1 =>
294 q avars w0 >>= fun t2 =>
295 OK (mkHaskCoercionKind t1 t2)
297 | Error s => Prelude_error s
301 destruct case_sac_types.
302 refine (vec_map _ (list2vec (dataConFieldTypes dc))).
304 unfold tyConKind in avars.
305 set (@weakTypeToType' Γ) as q.
306 unfold tyConKinds in q.
307 rewrite <- vec2list_map_list2vec in q.
308 rewrite vec2list_list2vec in q.
309 set (q avars X) as y.
311 | Error s =>Prelude_error s
317 Lemma weakCV' : forall {Γ}{Δ} Γ',
319 -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
321 unfold HaskCoVar in *.
322 intros; apply (X TV CV).
323 apply ilist_chop' in env; auto.
324 unfold InstantiatedCoercionEnv in *.
325 unfold weakCK'' in cenv.
327 rewrite <- map_preserves_length in cenv.
329 rewrite <- map_preserves_length in cenv.
333 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
335 {| sacpj_sac := mkStrongAltCon
336 ; sacpj_phi := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
338 fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
342 unfold HaskCoVar in *.
346 unfold sac_delta in *.
347 unfold InstantiatedCoercionEnv in *.
348 apply vec_chop' in cenv.
352 Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
363 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc).
365 set (c:DataCon _) as dc.
366 set ((dataConTyCon c):TyCon) as tc' in *.
367 set (eqd_dec tc tc') as eqpf; destruct eqpf;
369 | apply (Error ("in a case of tycon "+++toString tc+++", found a branch with datacon "+++toString (dc:CoreDataCon))) ]; subst.
371 eapply mkStrongAltConPlusJunk.
375 apply OK; refine {| sacpj_sac := {|
376 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
377 ; sac_altcon := WeakLitAlt h
379 intro; intro φ; apply φ.
380 intro; intro; intro; intro ψ. simpl. unfold sac_gamma; simpl. unfold sac_delta; simpl.
381 rewrite weakCK'_nil_inert. apply ψ.
382 apply OK; refine {| sacpj_sac := {|
383 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
384 ; sac_altcon := WeakDEFAULT |} |}.
385 intro; intro φ; apply φ.
386 intro; intro; intro; intro ψ. simpl. unfold sac_gamma; simpl. unfold sac_delta; simpl.
387 rewrite weakCK'_nil_inert. apply ψ.
390 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
391 fun wev => match wev with weakExprVar _ t => t end.
392 Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
394 Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
396 Definition weakPsi {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
397 WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
404 inversion cenv; auto.
407 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
408 Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} {l} τ' l' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ l)
409 : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ' l').
410 apply (addErrorMessage ("castExpr " +++ err_msg)).
412 destruct (eqd_dec l l'); [ idtac
413 | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
414 " got: " +++(fold_left (fun x y => y+++","+++y) (map (toString ○ haskTyVarToType) l) "")+++eol+++
415 " wanted: "+++(fold_left (fun x y => x+++","+++y) (map (toString ○ haskTyVarToType) l') "")
417 destruct (eqd_dec τ τ'); [ idtac
418 | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
419 " got: " +++toString τ+++eol+++
420 " wanted: "+++toString τ'
427 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
428 match wcv with weakCoerVar _ t _ => (kindOfCoreType (weakTypeToCoreType t)) end.
429 Coercion coVarKind : WeakCoerVar >-> Kind.
431 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
433 set (weakTypeToType φ t) as wt.
434 destruct wt; try apply (Error error_message).
436 matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in ").
442 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
445 | T_Leaf (Some (wev,e)) => match weakTypeToTypeOfKind φ wev ★ with
446 | OK t' => [((wev:CoreVar),t')]
449 | T_Branch b1 b2 => (varsTypes b1 φ),,(varsTypes b2 φ)
452 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
453 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
454 | nil => match wtl with
456 | _ => Error "length mismatch in mkAvars"
458 | k::lk' => match wtl with
459 | nil => Error "length mismatch in mkAvars"
461 weakTypeToTypeOfKind φ wt k >>= fun t =>
462 mkAvars wtl' lk' φ >>= fun rest =>
463 OK (ICons _ _ t rest)
467 Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool :=
474 else update_ig ig vars' v'
477 (* does the specified variable occur free in the expression? *)
478 Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
481 | WEVar cv => if eqd_dec (wev:CoreVar) (cv:CoreVar) then true else false
482 | WECast e co => doesWeakVarOccur wev e
483 | WENote n e => doesWeakVarOccur wev e
484 | WETyApp e t => doesWeakVarOccur wev e
485 | WECoApp e co => doesWeakVarOccur wev e
486 | WEBrak _ ec e _ => doesWeakVarOccur wev e
487 | WEEsc _ ec e _ => doesWeakVarOccur wev e
488 | WECSP _ ec e _ => doesWeakVarOccur wev e
489 | WELet cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
490 | WEApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
491 | WELam cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
492 | WETyLam cv e => doesWeakVarOccur wev e
493 | WECoLam cv e => doesWeakVarOccur wev e
494 | WECase vscrut escrut tbranches tc avars alts =>
495 doesWeakVarOccur wev escrut ||
496 if eqd_dec (wev:CoreVar) (vscrut:CoreVar) then false else
497 ((fix doesWeakVarOccurAlts alts {struct alts} : bool :=
499 | T_Leaf None => false
500 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
501 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
502 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
503 | T_Branch b1 b2 => doesWeakVarOccurAlts b1 || doesWeakVarOccurAlts b2
506 doesWeakVarOccur wev e ||
507 (fix doesWeakVarOccurLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) : bool :=
509 | T_Leaf None => false
510 | T_Leaf (Some (cv,e)) => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
511 | T_Branch b1 b2 => doesWeakVarOccurLetRec b1 || doesWeakVarOccurLetRec b2
514 Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
515 (alts:Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr)) : bool :=
517 | T_Leaf None => false
518 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
519 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
520 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
521 | T_Branch b1 b2 => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
524 Definition checkDistinct :
525 forall {V}(EQ:EqDecidable V)(lv:list V), ???(distinct lv).
527 set (distinct_decidable lv) as q.
530 exact (Error "checkDistinct failed").
533 (* FIXME: check the kind of the type of the weakexprvar to support >0 *)
534 Definition mkGlobal Γ (τ:HaskType Γ ★) (wev:WeakExprVar) : Global Γ.
535 refine {| glob_kinds := nil |}.
541 Definition weakExprToStrongExpr : forall
545 (ψ:CoVarResolver Γ Δ)
546 (ξ:CoreVar -> LeveledHaskType Γ ★)
550 WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ lev ).
552 fix weakExprToStrongExpr
556 (ψ:CoVarResolver Γ Δ)
557 (ξ:CoreVar -> LeveledHaskType Γ ★)
561 (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ lev ) :=
562 addErrorMessage ("in weakExprToStrongExpr " +++ toString we)
566 then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ τ lev)
567 else castExpr we ("WEVar "+++toString (v:CoreVar)) τ lev (EVar Γ Δ ξ v)
569 | WELit lit => castExpr we ("WELit "+++toString lit) τ lev (ELit Γ Δ ξ lit lev)
571 | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
572 weakTypeOfWeakExpr ebody >>= fun tbody =>
573 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
574 let ξ' := update_xi ξ lev (((ev:CoreVar),tv)::nil) in
575 let ig' := update_ig ig ((ev:CoreVar)::nil) in
576 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>
577 castExpr we "WELam" τ lev (ELam Γ Δ ξ tv tbody' lev ev ebody')
579 | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' =>
580 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
581 weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' =>
582 castExpr we "WEBrak" τ lev (EBrak Γ Δ ξ ec' tbody' lev e')
584 | WEEsc _ ec e tbody => φ ec >>= fun ec'' =>
585 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
587 | nil => Error "ill-leveled escapification"
588 | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
589 >>= fun e' => castExpr we "WEEsc" τ lev (EEsc Γ Δ ξ ec' tbody' lev' e')
592 | WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage"
594 | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ _ n e')
596 | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>
597 weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
598 weakExprToStrongExpr Γ Δ φ ψ (update_xi ξ lev (((v:CoreVar),tv)::nil))
599 (update_ig ig ((v:CoreVar)::nil)) τ lev ebody
601 OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
603 | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
604 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
605 weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' =>
606 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' =>
607 OK (EApp _ _ _ _ _ _ e1' e2')
609 | WETyLam tv e => let φ2 := upPhi tv φ in
610 weakTypeOfWeakExpr e >>= fun te =>
611 weakTypeToTypeOfKind φ2 te ★ >>= fun τ' =>
612 weakExprToStrongExpr _ (weakCE_(n:=O) Δ) φ2
613 (fun x => (ψ x) >>= fun y =>
614 OK (weakCV_ y)) (weakLT_○ξ) ig _ (weakL_ lev) e
615 >>= fun e' => castExpr we "WETyLam2" _ _
616 (ETyLam Γ Δ ξ tv (mkTAll' τ') lev 0 e')
618 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
620 | WForAllTy wtv te' =>
621 let φ2 := upPhi wtv φ in
622 weakTypeToTypeOfKind φ2 te' ★ >>= fun te'' =>
623 weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
624 weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
625 castExpr we "WETyApp" _ _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
626 | _ => Error ("weakTypeToType: WETyApp body with type "+++toString te)
629 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
631 | WCoFunTy t1 t2 t3 =>
632 weakTypeToType φ t1 >>= fun t1' =>
634 haskTypeOfSomeKind κ t1'' =>
635 weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
636 weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
637 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
638 castExpr we "WECoApp" _ _ e' >>= fun e'' =>
639 OK (ECoApp Γ Δ κ t1'' t2''
640 (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
642 | _ => Error ("weakTypeToType: WECoApp body with type "+++toString te)
645 | WECoLam cv e => let (_,t1,t2) := cv in
646 weakTypeOfWeakExpr e >>= fun te =>
647 weakTypeToTypeOfKind φ te ★ >>= fun te' =>
648 weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
649 weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
650 weakExprToStrongExpr Γ (_ :: Δ) φ (weakPsi ψ) ξ ig te' lev e >>= fun e' =>
651 castExpr we "WECoLam" _ _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
653 | WECast e co => let (t1,t2) := weakCoercionTypes co in
654 weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
655 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
656 weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
657 castExpr we "WECast" _ _
658 (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
661 let ξ' := update_xi ξ lev _ in
662 let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
664 (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
665 : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
667 | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
668 | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e)
670 binds b1 >>= fun b1' =>
671 binds b2 >>= fun b2' =>
672 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
674 in binds >>= fun binds' =>
675 checkDistinct CoreVarEqDecidable (map (@fst _ _) (leaves (varsTypes rb φ))) >>= fun rb_distinct =>
676 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
677 OK (ELetRec Γ Δ ξ lev τ _ _ binds' e')
679 | WECase vscrut escrut tbranches tc avars alts =>
680 weakTypeOfWeakExpr escrut >>= fun tscrut =>
681 weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
682 if doesWeakVarOccurAlts vscrut alts
683 then Error "encountered a Case which actually used its binder - these should have been desugared away!!"
684 else mkAvars avars (tyConKind tc) φ >>= fun avars' =>
685 weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' =>
686 (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
687 ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac &
688 Expr (sac_gamma sac Γ) (sac_delta sac Γ avars' (weakCK'' Δ))(scbwv_xi scb ξ lev)(weakT' tbranches')(weakL' lev)}}) :=
690 | T_Leaf None => OK []
691 | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
692 mkStrongAltConPlusJunk' tc ac >>= fun sac =>
693 list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
695 (let case_pf := tt in _) >>= fun pf =>
696 let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
697 weakExprToStrongExpr (sac_gamma sac Γ) (sac_delta sac Γ avars' (weakCK'' Δ)) (sacpj_phi sac _ φ)
698 (sacpj_psi sac _ _ avars' ψ)
700 (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
701 (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
702 let case_case := tt in OK [ _ ]
704 mkTree b1 >>= fun b1' =>
705 mkTree b2 >>= fun b2' =>
707 end) alts >>= fun tree =>
709 weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
710 castExpr we "ECase" τ lev (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
711 end)); try clear binds; try apply ConcatenableString.
714 apply (addErrorMessage "case_some").
716 destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
717 matchThings h (unlev (ξ' wev)) "LetRec".
719 rewrite matchTypeVars_pf.
720 clear matchTypeVars_pf.
721 set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
722 destruct e''; try apply (Error error_message).
727 induction (leaves (varsTypes rb φ)).
736 set (distinct_decidable (vec2list exprvars')) as dec.
737 destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ].