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 upPhi {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
33 then let fresh := @FreshHaskTyVar Γ tv in OK _
34 else φ tv' >>= fun tv'' => OK (fun TV ite => tv'' TV (weakITE ite))).
35 rewrite <- _H; apply fresh.
38 Definition upPhi2 {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ)
39 : (TyVarResolver (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)).
47 Definition substPhi {Γ:TypeEnv}(κ κ':Kind)(θ:HaskType Γ κ) : HaskType (κ::Γ) κ' -> HaskType Γ κ'.
51 unfold HaskType in ht.
54 apply ICons; [ idtac | apply env ].
58 Definition substphi {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ.
64 inversion θ; subst; auto.
72 (* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *)
73 Record StrongAltConPlusJunk {tc:TyCon} :=
74 { sacpj_sac : @StrongAltCon tc
75 ; sacpj_phi : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_gamma sacpj_sac Γ))
76 ; sacpj_psi : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_delta sacpj_sac Γ atypes (weakCK'' Δ))
78 Implicit Arguments StrongAltConPlusJunk [ ].
79 Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon.
81 (* yes, I know, this is really clumsy *)
82 Variable emptyφ : TyVarResolver nil.
83 Extract Inlined Constant emptyφ => "(\x -> Prelude.error ""encountered unbound tyvar!"")".
85 Definition mkPhi (lv:list WeakTypeVar)
86 : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)).
87 set (upPhi2(Γ:=nil) lv emptyφ) as φ2.
88 rewrite <- app_nil_end in φ2.
92 Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)).
93 Definition tyConKinds tc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (tyConTyVars tc)).
95 Definition fixkind {κ}(tv:WeakTypeVar) := weakTypeVar tv κ.
96 Notation " ` x " := (@fixkind _ x) (at level 100).
98 Ltac matchThings T1 T2 S :=
99 destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];
100 [ idtac | apply (Error (S +++ toString T1 +++ " " +++ toString T2)) ].
102 Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★).
104 unfold InstantiatedTypeEnv in ite.
109 Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★.
119 Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ).
120 refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) :=
121 addErrorMessage ("weakTypeToType " +++ toString t)
123 | WFunTyCon => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow))
124 | WTyCon tc => let case_WTyCon := tt in _
125 | WClassP c lt => let case_WClassP := tt in Error "weakTypeToType: WClassP not implemented"
126 | WIParam _ ty => let case_WIParam := tt in Error "weakTypeToType: WIParam not implemented"
127 | WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
128 | WTyVarTy v => let case_WTyVarTy := tt in φ v >>= fun v' => _
129 | WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upPhi wtv φ) t >>= fun t => _
130 | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody
131 >>= fun tbody' => φ (@fixkind ECKind ec) >>= fun ec' => _
132 | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt in
133 weakTypeToType _ φ t1 >>= fun t1' =>
134 weakTypeToType _ φ t2 >>= fun t2' =>
135 weakTypeToType _ φ t3 >>= fun t3' => _
137 ((fix weakTypeListToTypeList (lk:list Kind) (lt:list WeakType)
138 { struct lt } : ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV lk) :=
140 | nil => match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
141 | nil => OK (fun TV _ => TyFunApp_nil)
142 | _ => Error "WTyFunApp not applied to enough types"
144 | tx::lt' => weakTypeToType Γ φ tx >>= fun t' =>
145 match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
146 | nil => Error ("WTyFunApp applied to too many types"(* +++ eol +++
147 " tyCon= " +++ toString tc +++ eol +++
148 " tyConKindArgs= " +++ toString (fst (tyFunKind tc)) +++ eol +++
149 " tyConKindResult= " +++ toString (snd (tyFunKind tc)) +++ eol +++
150 " types= " +++ toString lt +++ eol*))
151 | k::lk' => weakTypeListToTypeList lk' lt' >>= fun rhtl' =>
152 let case_weakTypeListToTypeList := tt in _
155 ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in _
156 end ); clear weakTypeToType.
157 apply ConcatenableString.
159 destruct case_WTyVarTy.
160 apply (addErrorMessage "case_WTyVarTy").
162 exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))).
164 destruct case_WAppTy.
165 apply (addErrorMessage "case_WAppTy").
166 destruct t1' as [k1' t1'].
167 destruct t2' as [k2' t2'].
168 set ("tried to apply type "+++toString t1'+++" of kind "+++toString k1'+++" to type "+++
169 toString t2'+++" of kind "+++toString k2') as err.
171 try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
172 subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
173 apply (Error ("Kind mismatch in WAppTy: "+++err)).
175 destruct case_weakTypeListToTypeList.
176 apply (addErrorMessage "case_weakTypeListToTypeList").
177 destruct t' as [ k' t' ].
178 matchThings k k' "Kind mismatch in weakTypeListToTypeList".
180 apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
182 destruct case_WTyFunApp.
183 apply (addErrorMessage "case_WTyFunApp").
185 eapply haskTypeOfSomeKind.
186 unfold HaskType; intros.
187 apply (TyFunApp tc (fst (tyFunKind tc)) (snd (tyFunKind tc))).
191 destruct case_WTyCon.
192 apply (addErrorMessage "case_WTyCon").
194 eapply haskTypeOfSomeKind.
195 unfold HaskType; intros.
198 destruct case_WCodeTy.
199 apply (addErrorMessage "case_WCodeTy").
201 matchThings κ ★ "Kind mismatch in WCodeTy: ".
203 eapply haskTypeOfSomeKind.
204 unfold HaskType; intros.
206 apply (TVar (ec' TV X)).
211 destruct case_WCoFunTy.
212 apply (addErrorMessage "case_WCoFunTy").
213 destruct t1' as [ k1' t1' ].
214 destruct t2' as [ k2' t2' ].
215 destruct t3' as [ k3' t3' ].
216 matchThings k1' k2' "Kind mismatch in arguments of WCoFunTy".
218 matchThings k3' ★ "Kind mismatch in result of WCoFunTy".
221 apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
223 destruct case_WForAllTy.
224 apply (addErrorMessage "case_WForAllTy").
226 matchThings ★ κ "Kind mismatch in WForAllTy: ".
229 apply (@haskTypeOfSomeKind _ ★).
234 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
235 Section StrongAltCon.
236 Context (tc : TyCon)(dc:DataCon tc).
238 Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
239 -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
242 apply (addErrorMessage "weakTypeToType'").
243 set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
244 set (@substphi _ _ avars') as q.
245 set (upPhi2 (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ2.
246 set (@weakTypeToType _ φ2 ct) as t.
247 destruct t as [|t]; try apply (Error error_message).
248 destruct t as [tk t].
249 matchThings tk ★ "weakTypeToType'".
252 set (@weakT'' _ Γ _ t) as t'.
253 set (@lamer _ _ _ _ t') as t''.
254 fold (tyConKinds tc) in t''.
255 fold (dataConExKinds dc) in t''.
259 unfold dataConExKinds.
260 rewrite <- vec2list_map_list2vec.
261 rewrite <- vec2list_map_list2vec.
262 rewrite vec2list_list2vec.
263 rewrite vec2list_list2vec.
267 Definition mkStrongAltCon : @StrongAltCon tc.
269 {| sac_altcon := WeakDataAlt dc
270 ; sac_numCoerVars := length (dataConCoerKinds dc)
271 ; sac_numExprVars := length (dataConFieldTypes dc)
272 ; sac_ekinds := dataConExKinds dc
273 ; sac_coercions := fun Γ avars => let case_sac_coercions := tt in _
274 ; sac_types := fun Γ avars => let case_sac_types := tt in _
277 destruct case_sac_coercions.
278 refine (vec_map _ (list2vec (dataConCoerKinds dc))).
281 unfold tyConKind in avars.
282 set (@weakTypeToType' Γ) as q.
283 unfold tyConKinds in q.
284 rewrite <- vec2list_map_list2vec in q.
285 rewrite vec2list_list2vec in q.
288 q avars w >>= fun t1 =>
289 q avars w0 >>= fun t2 =>
290 OK (mkHaskCoercionKind t1 t2)
292 | Error s => Prelude_error s
296 destruct case_sac_types.
297 refine (vec_map _ (list2vec (dataConFieldTypes dc))).
299 unfold tyConKind in avars.
300 set (@weakTypeToType' Γ) as q.
301 unfold tyConKinds in q.
302 rewrite <- vec2list_map_list2vec in q.
303 rewrite vec2list_list2vec in q.
304 set (q avars X) as y.
306 | Error s =>Prelude_error s
312 Lemma weakCV' : forall {Γ}{Δ} Γ',
314 -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
316 unfold HaskCoVar in *.
317 intros; apply (X TV CV).
318 apply ilist_chop' in env; auto.
319 unfold InstantiatedCoercionEnv in *.
320 unfold weakCK'' in cenv.
322 rewrite <- map_preserves_length in cenv.
324 rewrite <- map_preserves_length in cenv.
328 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
330 {| sacpj_sac := mkStrongAltCon
331 ; sacpj_phi := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
333 fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
337 unfold HaskCoVar in *.
341 unfold sac_delta in *.
342 unfold InstantiatedCoercionEnv in *.
343 apply vec_chop' in cenv.
347 Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
358 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc).
360 set (c:DataCon _) as dc.
361 set ((dataConTyCon c):TyCon) as tc' in *.
362 set (eqd_dec tc tc') as eqpf; destruct eqpf;
364 | apply (Error ("in a case of tycon "+++toString tc+++", found a branch with datacon "+++toString (dc:CoreDataCon))) ]; subst.
366 eapply mkStrongAltConPlusJunk.
370 apply OK; refine {| sacpj_sac := {|
371 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
372 ; sac_altcon := WeakLitAlt h
374 intro; intro φ; apply φ.
375 intro; intro; intro; intro ψ. simpl. unfold sac_gamma; simpl. unfold sac_delta; simpl.
376 rewrite weakCK'_nil_inert. apply ψ.
377 apply OK; refine {| sacpj_sac := {|
378 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
379 ; sac_altcon := WeakDEFAULT |} |}.
380 intro; intro φ; apply φ.
381 intro; intro; intro; intro ψ. simpl. unfold sac_gamma; simpl. unfold sac_delta; simpl.
382 rewrite weakCK'_nil_inert. apply ψ.
385 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
386 fun wev => match wev with weakExprVar _ t => t end.
387 Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
389 Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
391 Definition weakPsi {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
392 WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
399 inversion cenv; auto.
402 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
403 Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} {l} τ' l' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ l)
404 : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ' l').
405 apply (addErrorMessage ("castExpr " +++ err_msg)).
407 destruct (eqd_dec l l'); [ idtac
408 | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
409 " got: " +++(fold_left (fun x y => y+++","+++y) (map (toString ○ haskTyVarToType) l) "")+++eol+++
410 " wanted: "+++(fold_left (fun x y => x+++","+++y) (map (toString ○ haskTyVarToType) l') "")
412 destruct (eqd_dec τ τ'); [ idtac
413 | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
414 " got: " +++toString τ+++eol+++
415 " wanted: "+++toString τ'
422 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
423 match wcv with weakCoerVar _ t _ => (kindOfCoreType (weakTypeToCoreType t)) end.
424 Coercion coVarKind : WeakCoerVar >-> Kind.
426 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
428 set (weakTypeToType φ t) as wt.
429 destruct wt; try apply (Error error_message).
431 matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in ").
437 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
440 | T_Leaf (Some (wev,e)) => match weakTypeToTypeOfKind φ wev ★ with
441 | OK t' => [((wev:CoreVar),t')]
444 | T_Branch b1 b2 => (varsTypes b1 φ),,(varsTypes b2 φ)
447 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
448 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
449 | nil => match wtl with
451 | _ => Error "length mismatch in mkAvars"
453 | k::lk' => match wtl with
454 | nil => Error "length mismatch in mkAvars"
456 weakTypeToTypeOfKind φ wt k >>= fun t =>
457 mkAvars wtl' lk' φ >>= fun rest =>
458 OK (ICons _ _ t rest)
462 Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool :=
469 else update_ig ig vars' v'
472 (* does the specified variable occur free in the expression? *)
473 Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
476 | WEVar cv => if eqd_dec (wev:CoreVar) (cv:CoreVar) then true else false
477 | WECast e co => doesWeakVarOccur wev e
478 | WENote n e => doesWeakVarOccur wev e
479 | WETyApp e t => doesWeakVarOccur wev e
480 | WECoApp e co => doesWeakVarOccur wev e
481 | WEBrak _ ec e _ => doesWeakVarOccur wev e
482 | WEEsc _ ec e _ => doesWeakVarOccur wev e
483 | WECSP _ ec e _ => doesWeakVarOccur wev e
484 | WELet cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
485 | WEApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
486 | WELam cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
487 | WETyLam cv e => doesWeakVarOccur wev e
488 | WECoLam cv e => doesWeakVarOccur wev e
489 | WECase vscrut escrut tbranches tc avars alts =>
490 doesWeakVarOccur wev escrut ||
491 if eqd_dec (wev:CoreVar) (vscrut:CoreVar) then false else
492 ((fix doesWeakVarOccurAlts alts {struct alts} : bool :=
494 | T_Leaf None => false
495 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
496 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
497 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
498 | T_Branch b1 b2 => doesWeakVarOccurAlts b1 || doesWeakVarOccurAlts b2
501 doesWeakVarOccur wev e ||
502 (fix doesWeakVarOccurLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) : bool :=
504 | T_Leaf None => false
505 | T_Leaf (Some (cv,e)) => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
506 | T_Branch b1 b2 => doesWeakVarOccurLetRec b1 || doesWeakVarOccurLetRec b2
509 Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
510 (alts:Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr)) : bool :=
512 | T_Leaf None => false
513 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
514 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
515 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
516 | T_Branch b1 b2 => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
519 Definition checkDistinct :
520 forall {V}(EQ:EqDecidable V)(lv:list V), ???(distinct lv).
522 set (distinct_decidable lv) as q.
525 exact (Error "checkDistinct failed").
528 (* FIXME: check the kind of the type of the weakexprvar to support >0 *)
529 Definition mkGlobal Γ (τ:HaskType Γ ★) (wev:WeakExprVar) : Global Γ.
530 refine {| glob_kinds := nil |}.
536 Definition weakExprToStrongExpr : forall
540 (ψ:CoVarResolver Γ Δ)
541 (ξ:CoreVar -> LeveledHaskType Γ ★)
545 WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ lev ).
547 fix weakExprToStrongExpr
551 (ψ:CoVarResolver Γ Δ)
552 (ξ:CoreVar -> LeveledHaskType Γ ★)
556 (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ lev ) :=
557 addErrorMessage ("in weakExprToStrongExpr " +++ toString we)
561 then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ τ lev)
562 else castExpr we ("WEVar "+++toString (v:CoreVar)) τ lev (EVar Γ Δ ξ v)
564 | WELit lit => castExpr we ("WELit "+++toString lit) τ lev (ELit Γ Δ ξ lit lev)
566 | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
567 weakTypeOfWeakExpr ebody >>= fun tbody =>
568 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
569 let ξ' := update_xi ξ lev (((ev:CoreVar),tv)::nil) in
570 let ig' := update_ig ig ((ev:CoreVar)::nil) in
571 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>
572 castExpr we "WELam" τ lev (ELam Γ Δ ξ tv tbody' lev ev ebody')
574 | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' =>
575 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
576 weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' =>
577 castExpr we "WEBrak" τ lev (EBrak Γ Δ ξ ec' tbody' lev e')
579 | WEEsc _ ec e tbody => φ ec >>= fun ec'' =>
580 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
582 | nil => Error "ill-leveled escapification"
583 | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
584 >>= fun e' => castExpr we "WEEsc" τ lev (EEsc Γ Δ ξ ec' tbody' lev' e')
587 | WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage"
589 | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ _ n e')
591 | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>
592 weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
593 weakExprToStrongExpr Γ Δ φ ψ (update_xi ξ lev (((v:CoreVar),tv)::nil))
594 (update_ig ig ((v:CoreVar)::nil)) τ lev ebody
596 OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
598 | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
599 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
600 weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' =>
601 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' =>
602 OK (EApp _ _ _ _ _ _ e1' e2')
604 | WETyLam tv e => let φ2 := upPhi tv φ in
605 weakTypeOfWeakExpr e >>= fun te =>
606 weakTypeToTypeOfKind φ2 te ★ >>= fun τ' =>
607 weakExprToStrongExpr _ (weakCE Δ) φ2
608 (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
609 >>= fun e' => castExpr we "WETyLam2" _ _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
611 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
613 | WForAllTy wtv te' =>
614 let φ2 := upPhi wtv φ in
615 weakTypeToTypeOfKind φ2 te' ★ >>= fun te'' =>
616 weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
617 weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
618 castExpr we "WETyApp" _ _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
619 | _ => Error ("weakTypeToType: WETyApp body with type "+++toString te)
622 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
624 | WCoFunTy t1 t2 t3 =>
625 weakTypeToType φ t1 >>= fun t1' =>
627 haskTypeOfSomeKind κ t1'' =>
628 weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
629 weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
630 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
631 castExpr we "WECoApp" _ _ e' >>= fun e'' =>
632 OK (ECoApp Γ Δ κ t1'' t2''
633 (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
635 | _ => Error ("weakTypeToType: WECoApp body with type "+++toString te)
638 | WECoLam cv e => let (_,t1,t2) := cv in
639 weakTypeOfWeakExpr e >>= fun te =>
640 weakTypeToTypeOfKind φ te ★ >>= fun te' =>
641 weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
642 weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
643 weakExprToStrongExpr Γ (_ :: Δ) φ (weakPsi ψ) ξ ig te' lev e >>= fun e' =>
644 castExpr we "WECoLam" _ _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
646 | WECast e co => let (t1,t2) := weakCoercionTypes co in
647 weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
648 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
649 weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
650 castExpr we "WECast" _ _
651 (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
654 let ξ' := update_xi ξ lev _ in
655 let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
657 (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
658 : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
660 | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
661 | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e)
663 binds b1 >>= fun b1' =>
664 binds b2 >>= fun b2' =>
665 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
667 in binds >>= fun binds' =>
668 checkDistinct CoreVarEqDecidable (map (@fst _ _) (leaves (varsTypes rb φ))) >>= fun rb_distinct =>
669 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
670 OK (ELetRec Γ Δ ξ lev τ _ _ binds' e')
672 | WECase vscrut escrut tbranches tc avars alts =>
673 weakTypeOfWeakExpr escrut >>= fun tscrut =>
674 weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
675 if doesWeakVarOccurAlts vscrut alts
676 then Error "encountered a Case which actually used its binder - these should have been desugared away!!"
677 else mkAvars avars (tyConKind tc) φ >>= fun avars' =>
678 weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' =>
679 (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
680 ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac &
681 Expr (sac_gamma sac Γ) (sac_delta sac Γ avars' (weakCK'' Δ))(scbwv_xi scb ξ lev)(weakT' tbranches')(weakL' lev)}}) :=
683 | T_Leaf None => OK []
684 | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
685 mkStrongAltConPlusJunk' tc ac >>= fun sac =>
686 list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
688 (let case_pf := tt in _) >>= fun pf =>
689 let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
690 weakExprToStrongExpr (sac_gamma sac Γ) (sac_delta sac Γ avars' (weakCK'' Δ)) (sacpj_phi sac _ φ)
691 (sacpj_psi sac _ _ avars' ψ)
693 (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
694 (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
695 let case_case := tt in OK [ _ ]
697 mkTree b1 >>= fun b1' =>
698 mkTree b2 >>= fun b2' =>
700 end) alts >>= fun tree =>
702 weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
703 castExpr we "ECase" τ lev (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
704 end)); try clear binds; try apply ConcatenableString.
707 apply (addErrorMessage "case_some").
709 destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
710 matchThings h (unlev (ξ' wev)) "LetRec".
712 rewrite matchTypeVars_pf.
713 clear matchTypeVars_pf.
714 set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
715 destruct e''; try apply (Error error_message).
720 induction (leaves (varsTypes rb φ)).
729 set (distinct_decidable (vec2list exprvars')) as dec.
730 destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ].