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.
23 Require Import HaskStrongToWeak.
25 Open Scope string_scope.
26 Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
27 Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
29 Definition upφ {Γ}(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 upφ' {Γ}(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 substφ {Γ: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_φ : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_Γ sacpj_sac Γ))
76 ; sacpj_ψ : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_Δ 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 (upφ'(Γ:=nil) lv emptyφ) as φ'.
88 rewrite <- app_nil_end in φ'.
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 +++ T1 +++ " " +++ 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 " +++ 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 _ (upφ wtv φ) t >>= fun t => _
130 | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody >>= fun tbody' => φ (@fixkind ★ 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"
146 | k::lk' => weakTypeListToTypeList lk' lt' >>= fun rhtl' =>
147 let case_weakTypeListToTypeList := tt in _
150 ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in _
151 end ); clear weakTypeToType.
153 destruct case_WTyVarTy.
154 apply (addErrorMessage "case_WTyVarTy").
156 exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))).
158 destruct case_WAppTy.
159 apply (addErrorMessage "case_WAppTy").
160 destruct t1' as [k1' t1'].
161 destruct t2' as [k2' t2'].
162 set ("tried to apply type "+++t1'+++" of kind "+++k1'+++" to type "+++t2'+++" of kind "+++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.
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 _ ★).
228 Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error".
230 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
231 Section StrongAltCon.
232 Context (tc : TyCon)(dc:DataCon tc).
234 Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
235 -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
238 apply (addErrorMessage "weakTypeToType'").
239 set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
240 set (@substφ _ _ avars') as q.
241 set (upφ' (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ'.
242 set (@weakTypeToType _ φ' ct) as t.
243 destruct t as [|t]; try apply (Error error_message).
244 destruct t as [tk t].
245 matchThings tk ★ "weakTypeToType'".
248 set (@weakT'' _ Γ _ t) as t'.
249 set (@lamer _ _ _ _ t') as t''.
250 fold (tyConKinds tc) in t''.
251 fold (dataConExKinds dc) in t''.
255 unfold dataConExKinds.
256 rewrite <- vec2list_map_list2vec.
257 rewrite <- vec2list_map_list2vec.
258 rewrite vec2list_list2vec.
259 rewrite vec2list_list2vec.
263 Definition mkStrongAltCon : @StrongAltCon tc.
265 {| sac_altcon := WeakDataAlt dc
266 ; sac_numCoerVars := length (dataConCoerKinds dc)
267 ; sac_numExprVars := length (dataConFieldTypes dc)
268 ; sac_ekinds := dataConExKinds dc
269 ; sac_coercions := fun Γ avars => let case_sac_coercions := tt in _
270 ; sac_types := fun Γ avars => let case_sac_types := tt in _
273 destruct case_sac_coercions.
274 refine (vec_map _ (list2vec (dataConCoerKinds dc))).
277 unfold tyConKind in avars.
278 set (@weakTypeToType' Γ) as q.
279 unfold tyConKinds in q.
280 rewrite <- vec2list_map_list2vec in q.
281 rewrite vec2list_list2vec in q.
284 q avars w >>= fun t1 =>
285 q avars w0 >>= fun t2 =>
286 OK (mkHaskCoercionKind t1 t2)
288 | Error s => Prelude_error s
292 destruct case_sac_types.
293 refine (vec_map _ (list2vec (dataConFieldTypes dc))).
295 unfold tyConKind in avars.
296 set (@weakTypeToType' Γ) as q.
297 unfold tyConKinds in q.
298 rewrite <- vec2list_map_list2vec in q.
299 rewrite vec2list_list2vec in q.
300 set (q avars X) as y.
302 | Error s =>Prelude_error s
308 Lemma weakCV' : forall {Γ}{Δ} Γ',
310 -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
312 unfold HaskCoVar in *.
313 intros; apply (X TV CV).
314 apply ilist_chop' in env; auto.
315 unfold InstantiatedCoercionEnv in *.
316 unfold weakCK'' in cenv.
318 rewrite <- map_preserves_length in cenv.
320 rewrite <- map_preserves_length in cenv.
324 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
326 {| sacpj_sac := mkStrongAltCon
327 ; sacpj_φ := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
329 fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
333 unfold HaskCoVar in *.
338 unfold InstantiatedCoercionEnv in *.
339 apply vec_chop' in cenv.
343 Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
354 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc).
356 set (c:DataCon _) as dc.
357 set ((dataConTyCon c):TyCon) as tc' in *.
358 set (eqd_dec tc tc') as eqpf; destruct eqpf;
360 | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++(dc:CoreDataCon))) ]; subst.
362 eapply mkStrongAltConPlusJunk.
366 apply OK; refine {| sacpj_sac := {|
367 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
368 ; sac_altcon := WeakLitAlt h
370 intro; intro φ; apply φ.
371 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
372 rewrite weakCK'_nil_inert. apply ψ.
373 apply OK; refine {| sacpj_sac := {|
374 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
375 ; sac_altcon := WeakDEFAULT |} |}.
376 intro; intro φ; apply φ.
377 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
378 rewrite weakCK'_nil_inert. apply ψ.
381 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
382 fun wev => match wev with weakExprVar _ t => t end.
383 Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
385 Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
387 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
388 WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
395 inversion cenv; auto.
398 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
399 Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
400 : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
401 apply (addErrorMessage ("castExpr " +++ err_msg)).
404 destruct τ' as [τ' l'].
405 destruct (eqd_dec l l'); [ idtac
406 | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
407 " got: " +++(fold_left (fun x y => y+++","+++y) (map haskTyVarToType l) "")+++eol+++
408 " wanted: "+++(fold_left (fun x y => x+++","+++y) (map haskTyVarToType l') "")
410 destruct (eqd_dec τ τ'); [ idtac
411 | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
412 " got: " +++τ+++eol+++
420 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
421 match wcv with weakCoerVar _ κ _ _ => κ end.
422 Coercion coVarKind : WeakCoerVar >-> Kind.
424 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
426 set (weakTypeToType φ t) as wt.
427 destruct wt; try apply (Error error_message).
429 matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in ").
435 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
438 | T_Leaf (Some (wev,e)) => match weakTypeToTypeOfKind φ wev ★ with
439 | OK t' => [((wev:CoreVar),t')]
442 | T_Branch b1 b2 => (varsTypes b1 φ),,(varsTypes b2 φ)
445 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
446 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
447 | nil => match wtl with
449 | _ => Error "length mismatch in mkAvars"
451 | k::lk' => match wtl with
452 | nil => Error "length mismatch in mkAvars"
454 weakTypeToTypeOfKind φ wt k >>= fun t =>
455 mkAvars wtl' lk' φ >>= fun rest =>
456 OK (ICons _ _ t rest)
460 Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool :=
467 else update_ig ig vars' v'
470 (* does the specified variable occur free in the expression? *)
471 Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
474 | WEVar cv => if eqd_dec (wev:CoreVar) (cv:CoreVar) then true else false
475 | WECast e co => doesWeakVarOccur wev e
476 | WENote n e => doesWeakVarOccur wev e
477 | WETyApp e t => doesWeakVarOccur wev e
478 | WECoApp e co => doesWeakVarOccur wev e
479 | WEBrak _ ec e _ => doesWeakVarOccur wev e
480 | WEEsc _ ec e _ => doesWeakVarOccur wev e
481 | WECSP _ ec e _ => doesWeakVarOccur wev e
482 | WELet cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
483 | WEApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
484 | WELam cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
485 | WETyLam cv e => doesWeakVarOccur wev e
486 | WECoLam cv e => doesWeakVarOccur wev e
487 | WECase vscrut escrut tbranches tc avars alts =>
488 doesWeakVarOccur wev escrut ||
489 if eqd_dec (wev:CoreVar) (vscrut:CoreVar) then false else
490 ((fix doesWeakVarOccurAlts alts {struct alts} : bool :=
492 | T_Leaf None => false
493 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
494 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
495 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
496 | T_Branch b1 b2 => doesWeakVarOccurAlts b1 || doesWeakVarOccurAlts b2
499 doesWeakVarOccur wev e ||
500 (fix doesWeakVarOccurLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) : bool :=
502 | T_Leaf None => false
503 | T_Leaf (Some (cv,e)) => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
504 | T_Branch b1 b2 => doesWeakVarOccurLetRec b1 || doesWeakVarOccurLetRec b2
507 Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
508 (alts:Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr)) : bool :=
510 | T_Leaf None => false
511 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
512 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
513 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
514 | T_Branch b1 b2 => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
517 (*Definition ensureCaseBindersAreNotUsed (we:WeakExpr) : UniqM WeakExpr := FIXME *)
519 Definition weakExprToStrongExpr : forall
523 (ψ:CoVarResolver Γ Δ)
524 (ξ:CoreVar -> LeveledHaskType Γ ★)
528 WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
530 fix weakExprToStrongExpr
534 (ψ:CoVarResolver Γ Δ)
535 (ξ:CoreVar -> LeveledHaskType Γ ★)
539 (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
540 addErrorMessage ("in weakExprToStrongExpr " +++ we)
544 then OK (EGlobal Γ Δ ξ (τ@@lev) v)
545 else castExpr we ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
547 | WELit lit => castExpr we ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
549 | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
550 weakTypeOfWeakExpr ebody >>= fun tbody =>
551 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
552 let ξ' := update_ξ ξ (((ev:CoreVar),tv@@lev)::nil) in
553 let ig' := update_ig ig ((ev:CoreVar)::nil) in
554 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>
555 castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
557 | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' =>
558 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
559 weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' =>
560 castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
562 | WEEsc _ ec e tbody => φ ec >>= fun ec'' =>
563 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
565 | nil => Error "ill-leveled escapification"
566 | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
567 >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
570 | WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage"
572 | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
574 | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>
575 weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
576 weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil))
577 (update_ig ig ((v:CoreVar)::nil)) τ lev ebody
579 OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
581 | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
582 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
583 weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' =>
584 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' =>
585 OK (EApp _ _ _ _ _ _ e1' e2')
587 | WETyLam tv e => let φ' := upφ tv φ in
588 weakTypeOfWeakExpr e >>= fun te =>
589 weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
590 weakExprToStrongExpr _ (weakCE Δ) φ'
591 (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
592 >>= fun e' => castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
594 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
596 | WForAllTy wtv te' =>
597 let φ' := upφ wtv φ in
598 weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>
599 weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
600 weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
601 castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
602 | _ => Error ("weakTypeToType: WETyApp body with type "+++te)
605 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
607 | WCoFunTy t1 t2 t3 =>
608 weakTypeToType φ t1 >>= fun t1' =>
610 haskTypeOfSomeKind κ t1'' =>
611 weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
612 weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
613 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
614 castExpr we "WECoApp" _ e' >>= fun e'' =>
615 OK (ECoApp Γ Δ κ t1'' t2''
616 (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
618 | _ => Error ("weakTypeToType: WECoApp body with type "+++te)
621 | WECoLam cv e => let (_,_,t1,t2) := cv in
622 weakTypeOfWeakExpr e >>= fun te =>
623 weakTypeToTypeOfKind φ te ★ >>= fun te' =>
624 weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
625 weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
626 weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ ig te' lev e >>= fun e' =>
627 castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
629 | WECast e co => let (t1,t2) := weakCoercionTypes co in
630 weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
631 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
632 weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
633 castExpr we "WECast" _
634 (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
637 let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _) in
638 let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
640 (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
641 : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
643 | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
644 | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e)
646 binds b1 >>= fun b1' =>
647 binds b2 >>= fun b2' =>
648 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
650 in binds >>= fun binds' =>
651 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
652 OK (ELetRec Γ Δ ξ lev τ _ binds' e')
654 | WECase vscrut escrut tbranches tc avars alts =>
655 weakTypeOfWeakExpr escrut >>= fun tscrut =>
656 weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
657 if doesWeakVarOccurAlts vscrut alts
658 then Error "encountered a Case which actually used its binder - these should have been desugared away!!"
659 else mkAvars avars (tyConKind tc) φ >>= fun avars' =>
660 weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' =>
661 (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
662 ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
663 Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@ lev))}) :=
665 | T_Leaf None => OK []
666 | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
667 mkStrongAltConPlusJunk' tc ac >>= fun sac =>
668 list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
670 let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
671 weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
672 (sacpj_ψ sac _ _ avars' ψ)
674 (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
675 (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
676 let case_case := tt in OK [ _ ]
678 mkTree b1 >>= fun b1' =>
679 mkTree b2 >>= fun b2' =>
681 end) alts >>= fun tree =>
683 weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
684 castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
688 apply (addErrorMessage "case_some").
690 destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
691 matchThings h (unlev (ξ' wev)) "LetRec".
693 rewrite matchTypeVars_pf.
694 clear matchTypeVars_pf.
695 set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
696 destruct e''; try apply (Error error_message).