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 HaskCoreTypes.
24 Open Scope string_scope.
25 Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
26 Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
28 Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
32 then let fresh := @FreshHaskTyVar Γ tv in OK _
33 else φ tv' >>= fun tv'' => OK (fun TV ite => tv'' TV (weakITE ite))).
34 rewrite <- _H; apply fresh.
37 Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ)
38 : (TyVarResolver (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)).
46 Definition substPhi {Γ:TypeEnv}(κ κ':Kind)(θ:HaskType Γ κ) : HaskType (κ::Γ) κ' -> HaskType Γ κ'.
50 unfold HaskType in ht.
53 apply ICons; [ idtac | apply env ].
57 Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ.
63 inversion θ; subst; auto.
71 (* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *)
72 Record StrongAltConPlusJunk {tc:TyCon} :=
73 { sacpj_sac : @StrongAltCon tc
74 ; sacpj_φ : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_Γ sacpj_sac Γ))
75 ; sacpj_ψ : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ))
77 Implicit Arguments StrongAltConPlusJunk [ ].
78 Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon.
80 (* yes, I know, this is really clumsy *)
81 Variable emptyφ : TyVarResolver nil.
82 Extract Inlined Constant emptyφ => "(\x -> Prelude.error ""encountered unbound tyvar!"")".
84 Definition mkPhi (lv:list WeakTypeVar)
85 : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)).
86 set (upφ'(Γ:=nil) lv emptyφ) as φ'.
87 rewrite <- app_nil_end in φ'.
91 Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)).
92 Definition tyConKinds tc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (tyConTyVars tc)).
94 Definition fixkind {κ}(tv:WeakTypeVar) := weakTypeVar tv κ.
95 Notation " ` x " := (@fixkind _ x) (at level 100).
97 Ltac matchThings T1 T2 S :=
98 destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];
99 [ idtac | apply (Error (S +++ toString T1 +++ " " +++ toString T2)) ].
101 Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★).
103 unfold InstantiatedTypeEnv in ite.
108 Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★.
118 Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ).
119 refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) :=
120 addErrorMessage ("weakTypeToType " +++ toString t)
122 | WFunTyCon => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow))
123 | WTyCon tc => let case_WTyCon := tt in _
124 | WClassP c lt => let case_WClassP := tt in Error "weakTypeToType: WClassP not implemented"
125 | WIParam _ ty => let case_WIParam := tt in Error "weakTypeToType: WIParam not implemented"
126 | WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
127 | WTyVarTy v => let case_WTyVarTy := tt in φ v >>= fun v' => _
128 | WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _
129 | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody
130 >>= fun tbody' => φ (@fixkind ECKind ec) >>= fun ec' => _
131 | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt in
132 weakTypeToType _ φ t1 >>= fun t1' =>
133 weakTypeToType _ φ t2 >>= fun t2' =>
134 weakTypeToType _ φ t3 >>= fun t3' => _
136 ((fix weakTypeListToTypeList (lk:list Kind) (lt:list WeakType)
137 { struct lt } : ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV lk) :=
139 | nil => match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
140 | nil => OK (fun TV _ => TyFunApp_nil)
141 | _ => Error "WTyFunApp not applied to enough types"
143 | tx::lt' => weakTypeToType Γ φ tx >>= fun t' =>
144 match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
145 | nil => Error ("WTyFunApp applied to too many types"(* +++ eol +++
146 " tyCon= " +++ toString tc +++ eol +++
147 " tyConKindArgs= " +++ toString (fst (tyFunKind tc)) +++ eol +++
148 " tyConKindResult= " +++ toString (snd (tyFunKind tc)) +++ eol +++
149 " types= " +++ toString lt +++ eol*))
150 | k::lk' => weakTypeListToTypeList lk' lt' >>= fun rhtl' =>
151 let case_weakTypeListToTypeList := tt in _
154 ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in _
155 end ); clear weakTypeToType.
156 apply ConcatenableString.
158 destruct case_WTyVarTy.
159 apply (addErrorMessage "case_WTyVarTy").
161 exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))).
163 destruct case_WAppTy.
164 apply (addErrorMessage "case_WAppTy").
165 destruct t1' as [k1' t1'].
166 destruct t2' as [k2' t2'].
167 set ("tried to apply type "+++toString t1'+++" of kind "+++toString k1'+++" to type "+++
168 toString t2'+++" of kind "+++toString k2') as err.
170 try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
171 subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
172 apply (Error ("Kind mismatch in WAppTy: "+++err)).
174 destruct case_weakTypeListToTypeList.
175 apply (addErrorMessage "case_weakTypeListToTypeList").
176 destruct t' as [ k' t' ].
177 matchThings k k' "Kind mismatch in weakTypeListToTypeList".
179 apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
181 destruct case_WTyFunApp.
182 apply (addErrorMessage "case_WTyFunApp").
184 eapply haskTypeOfSomeKind.
185 unfold HaskType; intros.
186 apply (TyFunApp tc (fst (tyFunKind tc)) (snd (tyFunKind tc))).
190 destruct case_WTyCon.
191 apply (addErrorMessage "case_WTyCon").
193 eapply haskTypeOfSomeKind.
194 unfold HaskType; intros.
197 destruct case_WCodeTy.
198 apply (addErrorMessage "case_WCodeTy").
200 matchThings κ ★ "Kind mismatch in WCodeTy: ".
202 eapply haskTypeOfSomeKind.
203 unfold HaskType; intros.
205 apply (TVar (ec' TV X)).
210 destruct case_WCoFunTy.
211 apply (addErrorMessage "case_WCoFunTy").
212 destruct t1' as [ k1' t1' ].
213 destruct t2' as [ k2' t2' ].
214 destruct t3' as [ k3' t3' ].
215 matchThings k1' k2' "Kind mismatch in arguments of WCoFunTy".
217 matchThings k3' ★ "Kind mismatch in result of WCoFunTy".
220 apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
222 destruct case_WForAllTy.
223 apply (addErrorMessage "case_WForAllTy").
225 matchThings ★ κ "Kind mismatch in WForAllTy: ".
228 apply (@haskTypeOfSomeKind _ ★).
233 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
234 Section StrongAltCon.
235 Context (tc : TyCon)(dc:DataCon tc).
237 Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
238 -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
241 apply (addErrorMessage "weakTypeToType'").
242 set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
243 set (@substφ _ _ avars') as q.
244 set (upφ' (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ'.
245 set (@weakTypeToType _ φ' ct) as t.
246 destruct t as [|t]; try apply (Error error_message).
247 destruct t as [tk t].
248 matchThings tk ★ "weakTypeToType'".
251 set (@weakT'' _ Γ _ t) as t'.
252 set (@lamer _ _ _ _ t') as t''.
253 fold (tyConKinds tc) in t''.
254 fold (dataConExKinds dc) in t''.
258 unfold dataConExKinds.
259 rewrite <- vec2list_map_list2vec.
260 rewrite <- vec2list_map_list2vec.
261 rewrite vec2list_list2vec.
262 rewrite vec2list_list2vec.
266 Definition mkStrongAltCon : @StrongAltCon tc.
268 {| sac_altcon := WeakDataAlt dc
269 ; sac_numCoerVars := length (dataConCoerKinds dc)
270 ; sac_numExprVars := length (dataConFieldTypes dc)
271 ; sac_ekinds := dataConExKinds dc
272 ; sac_coercions := fun Γ avars => let case_sac_coercions := tt in _
273 ; sac_types := fun Γ avars => let case_sac_types := tt in _
276 destruct case_sac_coercions.
277 refine (vec_map _ (list2vec (dataConCoerKinds dc))).
280 unfold tyConKind in avars.
281 set (@weakTypeToType' Γ) as q.
282 unfold tyConKinds in q.
283 rewrite <- vec2list_map_list2vec in q.
284 rewrite vec2list_list2vec in q.
287 q avars w >>= fun t1 =>
288 q avars w0 >>= fun t2 =>
289 OK (mkHaskCoercionKind t1 t2)
291 | Error s => Prelude_error s
295 destruct case_sac_types.
296 refine (vec_map _ (list2vec (dataConFieldTypes dc))).
298 unfold tyConKind in avars.
299 set (@weakTypeToType' Γ) as q.
300 unfold tyConKinds in q.
301 rewrite <- vec2list_map_list2vec in q.
302 rewrite vec2list_list2vec in q.
303 set (q avars X) as y.
305 | Error s =>Prelude_error s
311 Lemma weakCV' : forall {Γ}{Δ} Γ',
313 -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
315 unfold HaskCoVar in *.
316 intros; apply (X TV CV).
317 apply ilist_chop' in env; auto.
318 unfold InstantiatedCoercionEnv in *.
319 unfold weakCK'' in cenv.
321 rewrite <- map_preserves_length in cenv.
323 rewrite <- map_preserves_length in cenv.
327 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
329 {| sacpj_sac := mkStrongAltCon
330 ; sacpj_φ := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
332 fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
336 unfold HaskCoVar in *.
341 unfold InstantiatedCoercionEnv in *.
342 apply vec_chop' in cenv.
346 Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
357 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc).
359 set (c:DataCon _) as dc.
360 set ((dataConTyCon c):TyCon) as tc' in *.
361 set (eqd_dec tc tc') as eqpf; destruct eqpf;
363 | apply (Error ("in a case of tycon "+++toString tc+++", found a branch with datacon "+++toString (dc:CoreDataCon))) ]; subst.
365 eapply mkStrongAltConPlusJunk.
369 apply OK; refine {| sacpj_sac := {|
370 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
371 ; sac_altcon := WeakLitAlt h
373 intro; intro φ; apply φ.
374 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
375 rewrite weakCK'_nil_inert. apply ψ.
376 apply OK; refine {| sacpj_sac := {|
377 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
378 ; sac_altcon := WeakDEFAULT |} |}.
379 intro; intro φ; apply φ.
380 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
381 rewrite weakCK'_nil_inert. apply ψ.
384 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
385 fun wev => match wev with weakExprVar _ t => t end.
386 Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
388 Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
390 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
391 WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
398 inversion cenv; auto.
401 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
402 Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
403 : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
404 apply (addErrorMessage ("castExpr " +++ err_msg)).
407 destruct τ' as [τ' l'].
408 destruct (eqd_dec l l'); [ idtac
409 | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
410 " got: " +++(fold_left (fun x y => y+++","+++y) (map (toString ○ haskTyVarToType) l) "")+++eol+++
411 " wanted: "+++(fold_left (fun x y => x+++","+++y) (map (toString ○ haskTyVarToType) l') "")
413 destruct (eqd_dec τ τ'); [ idtac
414 | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
415 " got: " +++toString τ+++eol+++
416 " wanted: "+++toString τ'
423 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
424 match wcv with weakCoerVar _ t _ => (kindOfCoreType (weakTypeToCoreType t)) end.
425 Coercion coVarKind : WeakCoerVar >-> Kind.
427 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
429 set (weakTypeToType φ t) as wt.
430 destruct wt; try apply (Error error_message).
432 matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in ").
438 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
441 | T_Leaf (Some (wev,e)) => match weakTypeToTypeOfKind φ wev ★ with
442 | OK t' => [((wev:CoreVar),t')]
445 | T_Branch b1 b2 => (varsTypes b1 φ),,(varsTypes b2 φ)
448 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
449 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
450 | nil => match wtl with
452 | _ => Error "length mismatch in mkAvars"
454 | k::lk' => match wtl with
455 | nil => Error "length mismatch in mkAvars"
457 weakTypeToTypeOfKind φ wt k >>= fun t =>
458 mkAvars wtl' lk' φ >>= fun rest =>
459 OK (ICons _ _ t rest)
463 Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool :=
470 else update_ig ig vars' v'
473 (* does the specified variable occur free in the expression? *)
474 Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
477 | WEVar cv => if eqd_dec (wev:CoreVar) (cv:CoreVar) then true else false
478 | WECast e co => doesWeakVarOccur wev e
479 | WENote n e => doesWeakVarOccur wev e
480 | WETyApp e t => doesWeakVarOccur wev e
481 | WECoApp e co => doesWeakVarOccur wev e
482 | WEBrak _ ec e _ => doesWeakVarOccur wev e
483 | WEEsc _ ec e _ => doesWeakVarOccur wev e
484 | WECSP _ ec e _ => doesWeakVarOccur wev e
485 | WELet cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
486 | WEApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
487 | WELam cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
488 | WETyLam cv e => doesWeakVarOccur wev e
489 | WECoLam cv e => doesWeakVarOccur wev e
490 | WECase vscrut escrut tbranches tc avars alts =>
491 doesWeakVarOccur wev escrut ||
492 if eqd_dec (wev:CoreVar) (vscrut:CoreVar) then false else
493 ((fix doesWeakVarOccurAlts alts {struct alts} : bool :=
495 | T_Leaf None => false
496 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
497 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
498 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
499 | T_Branch b1 b2 => doesWeakVarOccurAlts b1 || doesWeakVarOccurAlts b2
502 doesWeakVarOccur wev e ||
503 (fix doesWeakVarOccurLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) : bool :=
505 | T_Leaf None => false
506 | T_Leaf (Some (cv,e)) => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
507 | T_Branch b1 b2 => doesWeakVarOccurLetRec b1 || doesWeakVarOccurLetRec b2
510 Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
511 (alts:Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr)) : bool :=
513 | T_Leaf None => false
514 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
515 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
516 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
517 | T_Branch b1 b2 => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
520 Definition checkDistinct :
521 forall {V}(EQ:EqDecidable V)(lv:list V), ???(distinct lv).
523 set (distinct_decidable lv) as q.
526 exact (Error "checkDistinct failed").
529 (* FIXME: check the kind of the type of the weakexprvar to support >0 *)
530 Definition mkGlobal Γ (τ:HaskType Γ ★) (wev:WeakExprVar) : Global Γ.
531 refine {| glob_kinds := nil |}.
537 Definition weakExprToStrongExpr : forall
541 (ψ:CoVarResolver Γ Δ)
542 (ξ:CoreVar -> LeveledHaskType Γ ★)
546 WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
548 fix weakExprToStrongExpr
552 (ψ:CoVarResolver Γ Δ)
553 (ξ:CoreVar -> LeveledHaskType Γ ★)
557 (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
558 addErrorMessage ("in weakExprToStrongExpr " +++ toString we)
562 then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ (τ@@lev))
563 else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
565 | WELit lit => castExpr we ("WELit "+++toString lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
567 | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
568 weakTypeOfWeakExpr ebody >>= fun tbody =>
569 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
570 let ξ' := update_ξ ξ lev (((ev:CoreVar),tv)::nil) in
571 let ig' := update_ig ig ((ev:CoreVar)::nil) in
572 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>
573 castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
575 | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' =>
576 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
577 weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' =>
578 castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
580 | WEEsc _ ec e tbody => φ ec >>= fun ec'' =>
581 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
583 | nil => Error "ill-leveled escapification"
584 | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
585 >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
588 | WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage"
590 | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
592 | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>
593 weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
594 weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ lev (((v:CoreVar),tv)::nil))
595 (update_ig ig ((v:CoreVar)::nil)) τ lev ebody
597 OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
599 | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
600 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
601 weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' =>
602 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' =>
603 OK (EApp _ _ _ _ _ _ e1' e2')
605 | WETyLam tv e => let φ' := upφ tv φ in
606 weakTypeOfWeakExpr e >>= fun te =>
607 weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
608 weakExprToStrongExpr _ (weakCE Δ) φ'
609 (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
610 >>= fun e' => castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
612 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
614 | WForAllTy wtv te' =>
615 let φ' := upφ wtv φ in
616 weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>
617 weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
618 weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
619 castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
620 | _ => Error ("weakTypeToType: WETyApp body with type "+++toString te)
623 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
625 | WCoFunTy t1 t2 t3 =>
626 weakTypeToType φ t1 >>= fun t1' =>
628 haskTypeOfSomeKind κ t1'' =>
629 weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
630 weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
631 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
632 castExpr we "WECoApp" _ e' >>= fun e'' =>
633 OK (ECoApp Γ Δ κ t1'' t2''
634 (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
636 | _ => Error ("weakTypeToType: WECoApp body with type "+++toString te)
639 | WECoLam cv e => let (_,t1,t2) := cv in
640 weakTypeOfWeakExpr e >>= fun te =>
641 weakTypeToTypeOfKind φ te ★ >>= fun te' =>
642 weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
643 weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
644 weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ ig te' lev e >>= fun e' =>
645 castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
647 | WECast e co => let (t1,t2) := weakCoercionTypes co in
648 weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
649 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
650 weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
651 castExpr we "WECast" _
652 (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
655 let ξ' := update_ξ ξ lev _ in
656 let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
658 (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
659 : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
661 | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
662 | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e)
664 binds b1 >>= fun b1' =>
665 binds b2 >>= fun b2' =>
666 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
668 in binds >>= fun binds' =>
669 checkDistinct CoreVarEqDecidable (map (@fst _ _) (leaves (varsTypes rb φ))) >>= fun rb_distinct =>
670 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
671 OK (ELetRec Γ Δ ξ lev τ _ _ binds' e')
673 | WECase vscrut escrut tbranches tc avars alts =>
674 weakTypeOfWeakExpr escrut >>= fun tscrut =>
675 weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
676 if doesWeakVarOccurAlts vscrut alts
677 then Error "encountered a Case which actually used its binder - these should have been desugared away!!"
678 else mkAvars avars (tyConKind tc) φ >>= fun avars' =>
679 weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' =>
680 (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
681 ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac &
682 Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@ lev))}}) :=
684 | T_Leaf None => OK []
685 | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
686 mkStrongAltConPlusJunk' tc ac >>= fun sac =>
687 list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
689 (let case_pf := tt in _) >>= fun pf =>
690 let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
691 weakExprToStrongExpr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
692 (sacpj_ψ sac _ _ avars' ψ)
694 (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
695 (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
696 let case_case := tt in OK [ _ ]
698 mkTree b1 >>= fun b1' =>
699 mkTree b2 >>= fun b2' =>
701 end) alts >>= fun tree =>
703 weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
704 castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
705 end)); try clear binds; try apply ConcatenableString.
708 apply (addErrorMessage "case_some").
710 destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
711 matchThings h (unlev (ξ' wev)) "LetRec".
713 rewrite matchTypeVars_pf.
714 clear matchTypeVars_pf.
715 set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
716 destruct e''; try apply (Error error_message).
721 induction (leaves (varsTypes rb φ)).
730 set (distinct_decidable (vec2list exprvars')) as dec.
731 destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ].