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 HaskLiteralsAndTyCons.
14 Require Import HaskWeakTypes.
15 Require Import HaskWeakVars.
16 Require Import HaskWeak.
17 Require Import HaskWeakToCore.
18 Require Import HaskStrongTypes.
19 Require Import HaskStrong.
20 Require Import HaskCoreVars.
22 Open Scope string_scope.
23 Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
24 Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
26 Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
30 then let fresh := @FreshHaskTyVar Γ tv in OK _
31 else φ tv' >>= fun tv'' => OK (fun TV ite => tv'' TV (weakITE ite))).
32 rewrite <- _H; apply fresh.
35 Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ)
36 : (TyVarResolver (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)).
44 Definition substPhi {Γ:TypeEnv}(κ κ':Kind)(θ:HaskType Γ κ) : HaskType (κ::Γ) κ' -> HaskType Γ κ'.
48 unfold HaskType in ht.
51 apply ICons; [ idtac | apply env ].
55 Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ.
61 inversion θ; subst; auto.
69 (* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *)
70 Record StrongAltConPlusJunk {tc:TyCon} :=
71 { sacpj_sac : @StrongAltCon tc
72 ; sacpj_φ : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_Γ sacpj_sac Γ))
73 ; sacpj_ψ : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ))
75 Implicit Arguments StrongAltConPlusJunk [ ].
76 Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon.
78 (* yes, I know, this is really clumsy *)
79 Variable emptyφ : TyVarResolver nil.
80 Extract Inlined Constant emptyφ => "(\x -> Prelude.error ""encountered unbound tyvar!"")".
82 Definition mkPhi (lv:list WeakTypeVar)
83 : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)).
84 set (upφ'(Γ:=nil) lv emptyφ) as φ'.
85 rewrite <- app_nil_end in φ'.
89 Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)).
90 Definition tyConKinds tc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (tyConTyVars tc)).
92 Definition fixkind {κ}(tv:WeakTypeVar) := weakTypeVar tv κ.
93 Notation " ` x " := (@fixkind _ x) (at level 100).
95 Ltac matchThings T1 T2 S :=
96 destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];
97 [ idtac | apply (Error (S +++ toString T1 +++ " " +++ toString T2)) ].
99 Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★).
101 unfold InstantiatedTypeEnv in ite.
106 Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★.
116 Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ).
117 refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) :=
118 addErrorMessage ("weakTypeToType " +++ toString t)
120 | WFunTyCon => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow))
121 | WTyCon tc => let case_WTyCon := tt in _
122 | WClassP c lt => let case_WClassP := tt in Error "weakTypeToType: WClassP not implemented"
123 | WIParam _ ty => let case_WIParam := tt in Error "weakTypeToType: WIParam not implemented"
124 | WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
125 | WTyVarTy v => let case_WTyVarTy := tt in φ v >>= fun v' => _
126 | WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _
127 | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody
128 >>= fun tbody' => φ (@fixkind ECKind ec) >>= fun ec' => _
129 | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt in
130 weakTypeToType _ φ t1 >>= fun t1' =>
131 weakTypeToType _ φ t2 >>= fun t2' =>
132 weakTypeToType _ φ t3 >>= fun t3' => _
134 ((fix weakTypeListToTypeList (lk:list Kind) (lt:list WeakType)
135 { struct lt } : ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV lk) :=
137 | nil => match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
138 | nil => OK (fun TV _ => TyFunApp_nil)
139 | _ => Error "WTyFunApp not applied to enough types"
141 | tx::lt' => weakTypeToType Γ φ tx >>= fun t' =>
142 match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
143 | nil => Error "WTyFunApp applied to too many types"
144 | k::lk' => weakTypeListToTypeList lk' lt' >>= fun rhtl' =>
145 let case_weakTypeListToTypeList := tt in _
148 ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in _
149 end ); clear weakTypeToType.
150 apply ConcatenableString.
152 destruct case_WTyVarTy.
153 apply (addErrorMessage "case_WTyVarTy").
155 exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))).
157 destruct case_WAppTy.
158 apply (addErrorMessage "case_WAppTy").
159 destruct t1' as [k1' t1'].
160 destruct t2' as [k2' t2'].
161 set ("tried to apply type "+++toString t1'+++" of kind "+++toString k1'+++" to type "+++
162 toString t2'+++" of kind "+++toString k2') as err.
164 try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
165 subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
166 apply (Error ("Kind mismatch in WAppTy: "+++err)).
168 destruct case_weakTypeListToTypeList.
169 apply (addErrorMessage "case_weakTypeListToTypeList").
170 destruct t' as [ k' t' ].
171 matchThings k k' "Kind mismatch in weakTypeListToTypeList".
173 apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
175 destruct case_WTyFunApp.
176 apply (addErrorMessage "case_WTyFunApp").
178 eapply haskTypeOfSomeKind.
179 unfold HaskType; intros.
180 apply (TyFunApp tc (fst (tyFunKind tc)) (snd (tyFunKind tc))).
184 destruct case_WTyCon.
185 apply (addErrorMessage "case_WTyCon").
187 eapply haskTypeOfSomeKind.
188 unfold HaskType; intros.
191 destruct case_WCodeTy.
192 apply (addErrorMessage "case_WCodeTy").
194 matchThings κ ★ "Kind mismatch in WCodeTy: ".
196 eapply haskTypeOfSomeKind.
197 unfold HaskType; intros.
199 apply (TVar (ec' TV X)).
204 destruct case_WCoFunTy.
205 apply (addErrorMessage "case_WCoFunTy").
206 destruct t1' as [ k1' t1' ].
207 destruct t2' as [ k2' t2' ].
208 destruct t3' as [ k3' t3' ].
209 matchThings k1' k2' "Kind mismatch in arguments of WCoFunTy".
211 matchThings k3' ★ "Kind mismatch in result of WCoFunTy".
214 apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
216 destruct case_WForAllTy.
217 apply (addErrorMessage "case_WForAllTy").
219 matchThings ★ κ "Kind mismatch in WForAllTy: ".
222 apply (@haskTypeOfSomeKind _ ★).
227 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
228 Section StrongAltCon.
229 Context (tc : TyCon)(dc:DataCon tc).
231 Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
232 -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
235 apply (addErrorMessage "weakTypeToType'").
236 set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
237 set (@substφ _ _ avars') as q.
238 set (upφ' (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ'.
239 set (@weakTypeToType _ φ' ct) as t.
240 destruct t as [|t]; try apply (Error error_message).
241 destruct t as [tk t].
242 matchThings tk ★ "weakTypeToType'".
245 set (@weakT'' _ Γ _ t) as t'.
246 set (@lamer _ _ _ _ t') as t''.
247 fold (tyConKinds tc) in t''.
248 fold (dataConExKinds dc) in t''.
252 unfold dataConExKinds.
253 rewrite <- vec2list_map_list2vec.
254 rewrite <- vec2list_map_list2vec.
255 rewrite vec2list_list2vec.
256 rewrite vec2list_list2vec.
260 Definition mkStrongAltCon : @StrongAltCon tc.
262 {| sac_altcon := WeakDataAlt dc
263 ; sac_numCoerVars := length (dataConCoerKinds dc)
264 ; sac_numExprVars := length (dataConFieldTypes dc)
265 ; sac_ekinds := dataConExKinds dc
266 ; sac_coercions := fun Γ avars => let case_sac_coercions := tt in _
267 ; sac_types := fun Γ avars => let case_sac_types := tt in _
270 destruct case_sac_coercions.
271 refine (vec_map _ (list2vec (dataConCoerKinds dc))).
274 unfold tyConKind in avars.
275 set (@weakTypeToType' Γ) as q.
276 unfold tyConKinds in q.
277 rewrite <- vec2list_map_list2vec in q.
278 rewrite vec2list_list2vec in q.
281 q avars w >>= fun t1 =>
282 q avars w0 >>= fun t2 =>
283 OK (mkHaskCoercionKind t1 t2)
285 | Error s => Prelude_error s
289 destruct case_sac_types.
290 refine (vec_map _ (list2vec (dataConFieldTypes dc))).
292 unfold tyConKind in avars.
293 set (@weakTypeToType' Γ) as q.
294 unfold tyConKinds in q.
295 rewrite <- vec2list_map_list2vec in q.
296 rewrite vec2list_list2vec in q.
297 set (q avars X) as y.
299 | Error s =>Prelude_error s
305 Lemma weakCV' : forall {Γ}{Δ} Γ',
307 -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
309 unfold HaskCoVar in *.
310 intros; apply (X TV CV).
311 apply ilist_chop' in env; auto.
312 unfold InstantiatedCoercionEnv in *.
313 unfold weakCK'' in cenv.
315 rewrite <- map_preserves_length in cenv.
317 rewrite <- map_preserves_length in cenv.
321 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
323 {| sacpj_sac := mkStrongAltCon
324 ; sacpj_φ := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
326 fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
330 unfold HaskCoVar in *.
335 unfold InstantiatedCoercionEnv in *.
336 apply vec_chop' in cenv.
340 Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
351 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc).
353 set (c:DataCon _) as dc.
354 set ((dataConTyCon c):TyCon) as tc' in *.
355 set (eqd_dec tc tc') as eqpf; destruct eqpf;
357 | apply (Error ("in a case of tycon "+++toString tc+++", found a branch with datacon "+++toString (dc:CoreDataCon))) ]; subst.
359 eapply mkStrongAltConPlusJunk.
363 apply OK; refine {| sacpj_sac := {|
364 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
365 ; sac_altcon := WeakLitAlt h
367 intro; intro φ; apply φ.
368 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
369 rewrite weakCK'_nil_inert. apply ψ.
370 apply OK; refine {| sacpj_sac := {|
371 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
372 ; sac_altcon := WeakDEFAULT |} |}.
373 intro; intro φ; apply φ.
374 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
375 rewrite weakCK'_nil_inert. apply ψ.
378 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
379 fun wev => match wev with weakExprVar _ t => t end.
380 Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
382 Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
384 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
385 WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
392 inversion cenv; auto.
395 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
396 Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
397 : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
398 apply (addErrorMessage ("castExpr " +++ err_msg)).
401 destruct τ' as [τ' l'].
402 destruct (eqd_dec l l'); [ idtac
403 | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
404 " got: " +++(fold_left (fun x y => y+++","+++y) (map (toString ○ haskTyVarToType) l) "")+++eol+++
405 " wanted: "+++(fold_left (fun x y => x+++","+++y) (map (toString ○ haskTyVarToType) l') "")
407 destruct (eqd_dec τ τ'); [ idtac
408 | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
409 " got: " +++toString τ+++eol+++
410 " wanted: "+++toString τ'
417 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
418 match wcv with weakCoerVar _ κ _ _ => κ end.
419 Coercion coVarKind : WeakCoerVar >-> Kind.
421 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
423 set (weakTypeToType φ t) as wt.
424 destruct wt; try apply (Error error_message).
426 matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in ").
432 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
435 | T_Leaf (Some (wev,e)) => match weakTypeToTypeOfKind φ wev ★ with
436 | OK t' => [((wev:CoreVar),t')]
439 | T_Branch b1 b2 => (varsTypes b1 φ),,(varsTypes b2 φ)
442 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
443 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
444 | nil => match wtl with
446 | _ => Error "length mismatch in mkAvars"
448 | k::lk' => match wtl with
449 | nil => Error "length mismatch in mkAvars"
451 weakTypeToTypeOfKind φ wt k >>= fun t =>
452 mkAvars wtl' lk' φ >>= fun rest =>
453 OK (ICons _ _ t rest)
457 Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool :=
464 else update_ig ig vars' v'
467 (* does the specified variable occur free in the expression? *)
468 Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
471 | WEVar cv => if eqd_dec (wev:CoreVar) (cv:CoreVar) then true else false
472 | WECast e co => doesWeakVarOccur wev e
473 | WENote n e => doesWeakVarOccur wev e
474 | WETyApp e t => doesWeakVarOccur wev e
475 | WECoApp e co => doesWeakVarOccur wev e
476 | WEBrak _ ec e _ => doesWeakVarOccur wev e
477 | WEEsc _ ec e _ => doesWeakVarOccur wev e
478 | WECSP _ ec e _ => doesWeakVarOccur wev e
479 | WELet cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
480 | WEApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
481 | WELam cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
482 | WETyLam cv e => doesWeakVarOccur wev e
483 | WECoLam cv e => doesWeakVarOccur wev e
484 | WECase vscrut escrut tbranches tc avars alts =>
485 doesWeakVarOccur wev escrut ||
486 if eqd_dec (wev:CoreVar) (vscrut:CoreVar) then false else
487 ((fix doesWeakVarOccurAlts alts {struct alts} : bool :=
489 | T_Leaf None => false
490 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
491 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
492 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
493 | T_Branch b1 b2 => doesWeakVarOccurAlts b1 || doesWeakVarOccurAlts b2
496 doesWeakVarOccur wev e ||
497 (fix doesWeakVarOccurLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) : bool :=
499 | T_Leaf None => false
500 | T_Leaf (Some (cv,e)) => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
501 | T_Branch b1 b2 => doesWeakVarOccurLetRec b1 || doesWeakVarOccurLetRec b2
504 Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
505 (alts:Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr)) : bool :=
507 | T_Leaf None => false
508 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
509 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
510 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
511 | T_Branch b1 b2 => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
514 Definition checkDistinct :
515 forall {V}(EQ:EqDecidable V)(lv:list V), ???(distinct lv).
517 set (distinct_decidable lv) as q.
520 exact (Error "checkDistinct failed").
523 (* FIXME: check the kind of the type of the weakexprvar to support >0 *)
524 Definition mkGlobal Γ (τ:HaskType Γ ★) (wev:WeakExprVar) : Global Γ.
525 refine {| glob_kinds := nil |}.
531 Definition weakExprToStrongExpr : forall
535 (ψ:CoVarResolver Γ Δ)
536 (ξ:CoreVar -> LeveledHaskType Γ ★)
540 WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
542 fix weakExprToStrongExpr
546 (ψ:CoVarResolver Γ Δ)
547 (ξ:CoreVar -> LeveledHaskType Γ ★)
551 (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
552 addErrorMessage ("in weakExprToStrongExpr " +++ toString we)
556 then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ (τ@@lev))
557 else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
559 | WELit lit => castExpr we ("WELit "+++toString lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
561 | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
562 weakTypeOfWeakExpr ebody >>= fun tbody =>
563 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
564 let ξ' := update_ξ ξ lev (((ev:CoreVar),tv)::nil) in
565 let ig' := update_ig ig ((ev:CoreVar)::nil) in
566 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>
567 castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
569 | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' =>
570 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
571 weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' =>
572 castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
574 | WEEsc _ ec e tbody => φ ec >>= fun ec'' =>
575 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
577 | nil => Error "ill-leveled escapification"
578 | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
579 >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
582 | WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage"
584 | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
586 | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>
587 weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
588 weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ lev (((v:CoreVar),tv)::nil))
589 (update_ig ig ((v:CoreVar)::nil)) τ lev ebody
591 OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
593 | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
594 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
595 weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' =>
596 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' =>
597 OK (EApp _ _ _ _ _ _ e1' e2')
599 | WETyLam tv e => let φ' := upφ tv φ in
600 weakTypeOfWeakExpr e >>= fun te =>
601 weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
602 weakExprToStrongExpr _ (weakCE Δ) φ'
603 (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
604 >>= fun e' => castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
606 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
608 | WForAllTy wtv te' =>
609 let φ' := upφ wtv φ in
610 weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>
611 weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
612 weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
613 castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
614 | _ => Error ("weakTypeToType: WETyApp body with type "+++toString te)
617 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
619 | WCoFunTy t1 t2 t3 =>
620 weakTypeToType φ t1 >>= fun t1' =>
622 haskTypeOfSomeKind κ t1'' =>
623 weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
624 weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
625 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
626 castExpr we "WECoApp" _ e' >>= fun e'' =>
627 OK (ECoApp Γ Δ κ t1'' t2''
628 (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
630 | _ => Error ("weakTypeToType: WECoApp body with type "+++toString te)
633 | WECoLam cv e => let (_,_,t1,t2) := cv in
634 weakTypeOfWeakExpr e >>= fun te =>
635 weakTypeToTypeOfKind φ te ★ >>= fun te' =>
636 weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
637 weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
638 weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ ig te' lev e >>= fun e' =>
639 castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
641 | WECast e co => let (t1,t2) := weakCoercionTypes co in
642 weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
643 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
644 weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
645 castExpr we "WECast" _
646 (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
649 let ξ' := update_ξ ξ lev _ in
650 let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
652 (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
653 : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
655 | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
656 | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e)
658 binds b1 >>= fun b1' =>
659 binds b2 >>= fun b2' =>
660 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
662 in binds >>= fun binds' =>
663 checkDistinct CoreVarEqDecidable (map (@fst _ _) (leaves (varsTypes rb φ))) >>= fun rb_distinct =>
664 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
665 OK (ELetRec Γ Δ ξ lev τ _ _ binds' e')
667 | WECase vscrut escrut tbranches tc avars alts =>
668 weakTypeOfWeakExpr escrut >>= fun tscrut =>
669 weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
670 if doesWeakVarOccurAlts vscrut alts
671 then Error "encountered a Case which actually used its binder - these should have been desugared away!!"
672 else mkAvars avars (tyConKind tc) φ >>= fun avars' =>
673 weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' =>
674 (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
675 ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac &
676 Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@ lev))}}) :=
678 | T_Leaf None => OK []
679 | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
680 mkStrongAltConPlusJunk' tc ac >>= fun sac =>
681 list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
683 (let case_pf := tt in _) >>= fun pf =>
684 let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
685 weakExprToStrongExpr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
686 (sacpj_ψ sac _ _ avars' ψ)
688 (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
689 (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
690 let case_case := tt in OK [ _ ]
692 mkTree b1 >>= fun b1' =>
693 mkTree b2 >>= fun b2' =>
695 end) alts >>= fun tree =>
697 weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
698 castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
699 end)); try clear binds; try apply ConcatenableString.
702 apply (addErrorMessage "case_some").
704 destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
705 matchThings h (unlev (ξ' wev)) "LetRec".
707 rewrite matchTypeVars_pf.
708 clear matchTypeVars_pf.
709 set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
710 destruct e''; try apply (Error error_message).
715 induction (leaves (varsTypes rb φ)).
724 set (distinct_decidable (vec2list exprvars')) as dec.
725 destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ].