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 upPhi {Γ}(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 upPhi2 {Γ}(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 substphi {Γ: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_phi : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_gamma sacpj_sac Γ))
75 ; sacpj_psi : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_delta 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 (upPhi2(Γ:=nil) lv emptyφ) as φ2.
87 rewrite <- app_nil_end in φ2.
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 _ (upPhi 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 (@substphi _ _ avars') as q.
244 set (upPhi2 (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ2.
245 set (@weakTypeToType _ φ2 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_phi := 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 *.
340 unfold sac_delta 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_gamma; simpl. unfold sac_delta; 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_gamma; simpl. unfold sac_delta; 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 weakPsi {Γ}{Δ: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) {Γ} {Δ} {ξ} {τ} {l} τ' l' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ l)
403 : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ' l').
404 apply (addErrorMessage ("castExpr " +++ err_msg)).
406 destruct (eqd_dec l l'); [ idtac
407 | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
408 " got: " +++(fold_left (fun x y => y+++","+++y) (map (toString ○ haskTyVarToType) l) "")+++eol+++
409 " wanted: "+++(fold_left (fun x y => x+++","+++y) (map (toString ○ haskTyVarToType) l') "")
411 destruct (eqd_dec τ τ'); [ idtac
412 | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
413 " got: " +++toString τ+++eol+++
414 " wanted: "+++toString τ'
421 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
422 match wcv with weakCoerVar _ t _ => (kindOfCoreType (weakTypeToCoreType t)) end.
423 Coercion coVarKind : WeakCoerVar >-> Kind.
425 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
427 set (weakTypeToType φ t) as wt.
428 destruct wt; try apply (Error error_message).
430 matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in ").
436 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
439 | T_Leaf (Some (wev,e)) => match weakTypeToTypeOfKind φ wev ★ with
440 | OK t' => [((wev:CoreVar),t')]
443 | T_Branch b1 b2 => (varsTypes b1 φ),,(varsTypes b2 φ)
446 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
447 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
448 | nil => match wtl with
450 | _ => Error "length mismatch in mkAvars"
452 | k::lk' => match wtl with
453 | nil => Error "length mismatch in mkAvars"
455 weakTypeToTypeOfKind φ wt k >>= fun t =>
456 mkAvars wtl' lk' φ >>= fun rest =>
457 OK (ICons _ _ t rest)
461 Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool :=
468 else update_ig ig vars' v'
471 (* does the specified variable occur free in the expression? *)
472 Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
475 | WEVar cv => if eqd_dec (wev:CoreVar) (cv:CoreVar) then true else false
476 | WECast e co => doesWeakVarOccur wev e
477 | WENote n e => doesWeakVarOccur wev e
478 | WETyApp e t => doesWeakVarOccur wev e
479 | WECoApp e co => doesWeakVarOccur wev e
480 | WEBrak _ ec e _ => doesWeakVarOccur wev e
481 | WEEsc _ ec e _ => doesWeakVarOccur wev e
482 | WECSP _ ec e _ => doesWeakVarOccur wev e
483 | WELet cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
484 | WEApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
485 | WELam cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
486 | WETyLam cv e => doesWeakVarOccur wev e
487 | WECoLam cv e => doesWeakVarOccur wev e
488 | WECase vscrut escrut tbranches tc avars alts =>
489 doesWeakVarOccur wev escrut ||
490 if eqd_dec (wev:CoreVar) (vscrut:CoreVar) then false else
491 ((fix doesWeakVarOccurAlts alts {struct alts} : bool :=
493 | T_Leaf None => false
494 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
495 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
496 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
497 | T_Branch b1 b2 => doesWeakVarOccurAlts b1 || doesWeakVarOccurAlts b2
500 doesWeakVarOccur wev e ||
501 (fix doesWeakVarOccurLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) : bool :=
503 | T_Leaf None => false
504 | T_Leaf (Some (cv,e)) => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
505 | T_Branch b1 b2 => doesWeakVarOccurLetRec b1 || doesWeakVarOccurLetRec b2
508 Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
509 (alts:Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr)) : bool :=
511 | T_Leaf None => false
512 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
513 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
514 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
515 | T_Branch b1 b2 => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
518 Definition checkDistinct :
519 forall {V}(EQ:EqDecidable V)(lv:list V), ???(distinct lv).
521 set (distinct_decidable lv) as q.
524 exact (Error "checkDistinct failed").
527 (* FIXME: check the kind of the type of the weakexprvar to support >0 *)
528 Definition mkGlobal Γ (τ:HaskType Γ ★) (wev:WeakExprVar) : Global Γ.
529 refine {| glob_kinds := nil |}.
535 Definition weakExprToStrongExpr : forall
539 (ψ:CoVarResolver Γ Δ)
540 (ξ:CoreVar -> LeveledHaskType Γ ★)
544 WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ lev ).
546 fix weakExprToStrongExpr
550 (ψ:CoVarResolver Γ Δ)
551 (ξ:CoreVar -> LeveledHaskType Γ ★)
555 (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ lev ) :=
556 addErrorMessage ("in weakExprToStrongExpr " +++ toString we)
560 then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ τ lev)
561 else castExpr we ("WEVar "+++toString (v:CoreVar)) τ lev (EVar Γ Δ ξ v)
563 | WELit lit => castExpr we ("WELit "+++toString lit) τ lev (ELit Γ Δ ξ lit lev)
565 | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
566 weakTypeOfWeakExpr ebody >>= fun tbody =>
567 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
568 let ξ' := update_xi ξ lev (((ev:CoreVar),tv)::nil) in
569 let ig' := update_ig ig ((ev:CoreVar)::nil) in
570 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>
571 castExpr we "WELam" τ lev (ELam Γ Δ ξ tv tbody' lev ev ebody')
573 | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' =>
574 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
575 weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' =>
576 castExpr we "WEBrak" τ lev (EBrak Γ Δ ξ ec' tbody' lev e')
578 | WEEsc _ ec e tbody => φ ec >>= fun ec'' =>
579 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
581 | nil => Error "ill-leveled escapification"
582 | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
583 >>= fun e' => castExpr we "WEEsc" τ lev (EEsc Γ Δ ξ ec' tbody' lev' e')
586 | WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage"
588 | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ _ n e')
590 | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>
591 weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
592 weakExprToStrongExpr Γ Δ φ ψ (update_xi ξ lev (((v:CoreVar),tv)::nil))
593 (update_ig ig ((v:CoreVar)::nil)) τ lev ebody
595 OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
597 | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
598 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
599 weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' =>
600 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' =>
601 OK (EApp _ _ _ _ _ _ e1' e2')
603 | WETyLam tv e => let φ2 := upPhi tv φ in
604 weakTypeOfWeakExpr e >>= fun te =>
605 weakTypeToTypeOfKind φ2 te ★ >>= fun τ' =>
606 weakExprToStrongExpr _ (weakCE Δ) φ2
607 (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
608 >>= fun e' => castExpr we "WETyLam2" _ _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
610 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
612 | WForAllTy wtv te' =>
613 let φ2 := upPhi wtv φ in
614 weakTypeToTypeOfKind φ2 te' ★ >>= fun te'' =>
615 weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
616 weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
617 castExpr we "WETyApp" _ _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
618 | _ => Error ("weakTypeToType: WETyApp body with type "+++toString te)
621 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
623 | WCoFunTy t1 t2 t3 =>
624 weakTypeToType φ t1 >>= fun t1' =>
626 haskTypeOfSomeKind κ t1'' =>
627 weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
628 weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
629 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
630 castExpr we "WECoApp" _ _ e' >>= fun e'' =>
631 OK (ECoApp Γ Δ κ t1'' t2''
632 (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
634 | _ => Error ("weakTypeToType: WECoApp body with type "+++toString te)
637 | WECoLam cv e => let (_,t1,t2) := cv in
638 weakTypeOfWeakExpr e >>= fun te =>
639 weakTypeToTypeOfKind φ te ★ >>= fun te' =>
640 weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
641 weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
642 weakExprToStrongExpr Γ (_ :: Δ) φ (weakPsi ψ) ξ ig te' lev e >>= fun e' =>
643 castExpr we "WECoLam" _ _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
645 | WECast e co => let (t1,t2) := weakCoercionTypes co in
646 weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
647 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
648 weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
649 castExpr we "WECast" _ _
650 (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
653 let ξ' := update_xi ξ lev _ in
654 let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
656 (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
657 : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
659 | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
660 | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e)
662 binds b1 >>= fun b1' =>
663 binds b2 >>= fun b2' =>
664 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
666 in binds >>= fun binds' =>
667 checkDistinct CoreVarEqDecidable (map (@fst _ _) (leaves (varsTypes rb φ))) >>= fun rb_distinct =>
668 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
669 OK (ELetRec Γ Δ ξ lev τ _ _ binds' e')
671 | WECase vscrut escrut tbranches tc avars alts =>
672 weakTypeOfWeakExpr escrut >>= fun tscrut =>
673 weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
674 if doesWeakVarOccurAlts vscrut alts
675 then Error "encountered a Case which actually used its binder - these should have been desugared away!!"
676 else mkAvars avars (tyConKind tc) φ >>= fun avars' =>
677 weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' =>
678 (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
679 ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac &
680 Expr (sac_gamma sac Γ) (sac_delta sac Γ avars' (weakCK'' Δ))(scbwv_xi scb ξ lev)(weakT' tbranches')(weakL' lev)}}) :=
682 | T_Leaf None => OK []
683 | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
684 mkStrongAltConPlusJunk' tc ac >>= fun sac =>
685 list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
687 (let case_pf := tt in _) >>= fun pf =>
688 let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
689 weakExprToStrongExpr (sac_gamma sac Γ) (sac_delta sac Γ avars' (weakCK'' Δ)) (sacpj_phi sac _ φ)
690 (sacpj_psi sac _ _ avars' ψ)
692 (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
693 (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
694 let case_case := tt in OK [ _ ]
696 mkTree b1 >>= fun b1' =>
697 mkTree b2 >>= fun b2' =>
699 end) alts >>= fun tree =>
701 weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
702 castExpr we "ECase" τ lev (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
703 end)); try clear binds; try apply ConcatenableString.
706 apply (addErrorMessage "case_some").
708 destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
709 matchThings h (unlev (ξ' wev)) "LetRec".
711 rewrite matchTypeVars_pf.
712 clear matchTypeVars_pf.
713 set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
714 destruct e''; try apply (Error error_message).
719 induction (leaves (varsTypes rb φ)).
728 set (distinct_decidable (vec2list exprvars')) as dec.
729 destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ].