1 (*********************************************************************************************************************************)
2 (* HaskWeakToStrong: convert HaskWeak to HaskStrong *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import NaturalDeduction.
9 Require Import Coq.Strings.String.
10 Require Import Coq.Lists.List.
11 Require Import Coq.Init.Specif.
12 Require Import HaskKinds.
13 Require Import HaskLiterals.
14 Require Import HaskTyCons.
15 Require Import HaskWeakTypes.
16 Require Import HaskWeakVars.
17 Require Import HaskWeak.
18 Require Import HaskWeakToCore.
19 Require Import HaskStrongTypes.
20 Require Import HaskStrong.
21 Require Import HaskCoreVars.
22 Require Import HaskCoreTypes.
24 Open Scope string_scope.
25 Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
26 Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
28 Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
32 then let fresh := @FreshHaskTyVar Γ tv in OK _
33 else φ tv' >>= fun tv'' => OK (fun TV ite => tv'' TV (weakITE ite))).
34 rewrite <- _H; apply fresh.
37 Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ)
38 : (TyVarResolver (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)).
46 Definition substPhi {Γ:TypeEnv}(κ κ':Kind)(θ:HaskType Γ κ) : HaskType (κ::Γ) κ' -> HaskType Γ κ'.
50 unfold HaskType in ht.
53 apply ICons; [ idtac | apply env ].
57 Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ.
63 inversion θ; subst; auto.
71 (* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *)
72 Record StrongAltConPlusJunk {tc:TyCon} :=
73 { sacpj_sac : @StrongAltCon tc
74 ; sacpj_φ : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_Γ sacpj_sac Γ))
75 ; sacpj_ψ : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ))
77 Implicit Arguments StrongAltConPlusJunk [ ].
78 Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon.
80 (* yes, I know, this is really clumsy *)
81 Variable emptyφ : TyVarResolver nil.
82 Extract Inlined Constant emptyφ => "(\x -> Prelude.error ""encountered unbound tyvar!"")".
84 Definition mkPhi (lv:list WeakTypeVar)
85 : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)).
86 set (upφ'(Γ:=nil) lv emptyφ) as φ'.
87 rewrite <- app_nil_end in φ'.
91 Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)).
92 Definition tyConKinds tc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (tyConTyVars tc)).
94 Definition fixkind {κ}(tv:WeakTypeVar) := weakTypeVar tv κ.
95 Notation " ` x " := (@fixkind _ x) (at level 100).
97 Ltac matchThings T1 T2 S :=
98 destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];
99 [ idtac | apply (Error (S +++ toString T1 +++ " " +++ toString T2)) ].
101 Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★).
103 unfold InstantiatedTypeEnv in ite.
108 Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★.
118 Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ).
119 refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) :=
120 addErrorMessage ("weakTypeToType " +++ toString t)
122 | WFunTyCon => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow))
123 | WTyCon tc => let case_WTyCon := tt in _
124 | WClassP c lt => let case_WClassP := tt in Error "weakTypeToType: WClassP not implemented"
125 | WIParam _ ty => let case_WIParam := tt in Error "weakTypeToType: WIParam not implemented"
126 | WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
127 | WTyVarTy v => let case_WTyVarTy := tt in φ v >>= fun v' => _
128 | WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _
129 | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody
130 >>= fun tbody' => φ (@fixkind ECKind ec) >>= fun ec' => _
131 | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt in
132 weakTypeToType _ φ t1 >>= fun t1' =>
133 weakTypeToType _ φ t2 >>= fun t2' =>
134 weakTypeToType _ φ t3 >>= fun t3' => _
136 ((fix weakTypeListToTypeList (lk:list Kind) (lt:list WeakType)
137 { struct lt } : ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV lk) :=
139 | nil => match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
140 | nil => OK (fun TV _ => TyFunApp_nil)
141 | _ => Error "WTyFunApp not applied to enough types"
143 | tx::lt' => weakTypeToType Γ φ tx >>= fun t' =>
144 match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
145 | nil => Error "WTyFunApp applied to too many types"
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.
152 apply ConcatenableString.
154 destruct case_WTyVarTy.
155 apply (addErrorMessage "case_WTyVarTy").
157 exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))).
159 destruct case_WAppTy.
160 apply (addErrorMessage "case_WAppTy").
161 destruct t1' as [k1' t1'].
162 destruct t2' as [k2' t2'].
163 set ("tried to apply type "+++toString t1'+++" of kind "+++toString k1'+++" to type "+++
164 toString t2'+++" of kind "+++toString k2') as err.
166 try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
167 subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
168 apply (Error ("Kind mismatch in WAppTy: "+++err)).
170 destruct case_weakTypeListToTypeList.
171 apply (addErrorMessage "case_weakTypeListToTypeList").
172 destruct t' as [ k' t' ].
173 matchThings k k' "Kind mismatch in weakTypeListToTypeList".
175 apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
177 destruct case_WTyFunApp.
178 apply (addErrorMessage "case_WTyFunApp").
180 eapply haskTypeOfSomeKind.
181 unfold HaskType; intros.
182 apply (TyFunApp tc (fst (tyFunKind tc)) (snd (tyFunKind tc))).
186 destruct case_WTyCon.
187 apply (addErrorMessage "case_WTyCon").
189 eapply haskTypeOfSomeKind.
190 unfold HaskType; intros.
193 destruct case_WCodeTy.
194 apply (addErrorMessage "case_WCodeTy").
196 matchThings κ ★ "Kind mismatch in WCodeTy: ".
198 eapply haskTypeOfSomeKind.
199 unfold HaskType; intros.
201 apply (TVar (ec' TV X)).
206 destruct case_WCoFunTy.
207 apply (addErrorMessage "case_WCoFunTy").
208 destruct t1' as [ k1' t1' ].
209 destruct t2' as [ k2' t2' ].
210 destruct t3' as [ k3' t3' ].
211 matchThings k1' k2' "Kind mismatch in arguments of WCoFunTy".
213 matchThings k3' ★ "Kind mismatch in result of WCoFunTy".
216 apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
218 destruct case_WForAllTy.
219 apply (addErrorMessage "case_WForAllTy").
221 matchThings ★ κ "Kind mismatch in WForAllTy: ".
224 apply (@haskTypeOfSomeKind _ ★).
229 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
230 Section StrongAltCon.
231 Context (tc : TyCon)(dc:DataCon tc).
233 Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
234 -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
237 apply (addErrorMessage "weakTypeToType'").
238 set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
239 set (@substφ _ _ avars') as q.
240 set (upφ' (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ'.
241 set (@weakTypeToType _ φ' ct) as t.
242 destruct t as [|t]; try apply (Error error_message).
243 destruct t as [tk t].
244 matchThings tk ★ "weakTypeToType'".
247 set (@weakT'' _ Γ _ t) as t'.
248 set (@lamer _ _ _ _ t') as t''.
249 fold (tyConKinds tc) in t''.
250 fold (dataConExKinds dc) in t''.
254 unfold dataConExKinds.
255 rewrite <- vec2list_map_list2vec.
256 rewrite <- vec2list_map_list2vec.
257 rewrite vec2list_list2vec.
258 rewrite vec2list_list2vec.
262 Definition mkStrongAltCon : @StrongAltCon tc.
264 {| sac_altcon := WeakDataAlt dc
265 ; sac_numCoerVars := length (dataConCoerKinds dc)
266 ; sac_numExprVars := length (dataConFieldTypes dc)
267 ; sac_ekinds := dataConExKinds dc
268 ; sac_coercions := fun Γ avars => let case_sac_coercions := tt in _
269 ; sac_types := fun Γ avars => let case_sac_types := tt in _
272 destruct case_sac_coercions.
273 refine (vec_map _ (list2vec (dataConCoerKinds dc))).
276 unfold tyConKind in avars.
277 set (@weakTypeToType' Γ) as q.
278 unfold tyConKinds in q.
279 rewrite <- vec2list_map_list2vec in q.
280 rewrite vec2list_list2vec in q.
283 q avars w >>= fun t1 =>
284 q avars w0 >>= fun t2 =>
285 OK (mkHaskCoercionKind t1 t2)
287 | Error s => Prelude_error s
291 destruct case_sac_types.
292 refine (vec_map _ (list2vec (dataConFieldTypes dc))).
294 unfold tyConKind in avars.
295 set (@weakTypeToType' Γ) as q.
296 unfold tyConKinds in q.
297 rewrite <- vec2list_map_list2vec in q.
298 rewrite vec2list_list2vec in q.
299 set (q avars X) as y.
301 | Error s =>Prelude_error s
307 Lemma weakCV' : forall {Γ}{Δ} Γ',
309 -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
311 unfold HaskCoVar in *.
312 intros; apply (X TV CV).
313 apply ilist_chop' in env; auto.
314 unfold InstantiatedCoercionEnv in *.
315 unfold weakCK'' in cenv.
317 rewrite <- map_preserves_length in cenv.
319 rewrite <- map_preserves_length in cenv.
323 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
325 {| sacpj_sac := mkStrongAltCon
326 ; sacpj_φ := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
328 fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
332 unfold HaskCoVar in *.
337 unfold InstantiatedCoercionEnv in *.
338 apply vec_chop' in cenv.
342 Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
353 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc).
355 set (c:DataCon _) as dc.
356 set ((dataConTyCon c):TyCon) as tc' in *.
357 set (eqd_dec tc tc') as eqpf; destruct eqpf;
359 | apply (Error ("in a case of tycon "+++toString tc+++", found a branch with datacon "+++toString (dc:CoreDataCon))) ]; subst.
361 eapply mkStrongAltConPlusJunk.
365 apply OK; refine {| sacpj_sac := {|
366 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
367 ; sac_altcon := WeakLitAlt h
369 intro; intro φ; apply φ.
370 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
371 rewrite weakCK'_nil_inert. apply ψ.
372 apply OK; refine {| sacpj_sac := {|
373 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
374 ; sac_altcon := WeakDEFAULT |} |}.
375 intro; intro φ; apply φ.
376 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
377 rewrite weakCK'_nil_inert. apply ψ.
380 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
381 fun wev => match wev with weakExprVar _ t => t end.
382 Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
384 Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
386 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
387 WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
394 inversion cenv; auto.
397 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
398 Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
399 : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
400 apply (addErrorMessage ("castExpr " +++ err_msg)).
403 destruct τ' as [τ' l'].
404 destruct (eqd_dec l l'); [ idtac
405 | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
406 " got: " +++(fold_left (fun x y => y+++","+++y) (map (toString ○ haskTyVarToType) l) "")+++eol+++
407 " wanted: "+++(fold_left (fun x y => x+++","+++y) (map (toString ○ haskTyVarToType) l') "")
409 destruct (eqd_dec τ τ'); [ idtac
410 | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
411 " got: " +++toString τ+++eol+++
412 " wanted: "+++toString τ'
419 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
420 match wcv with weakCoerVar _ t _ => (kindOfCoreType (weakTypeToCoreType t)) end.
421 Coercion coVarKind : WeakCoerVar >-> Kind.
423 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
425 set (weakTypeToType φ t) as wt.
426 destruct wt; try apply (Error error_message).
428 matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in ").
434 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
437 | T_Leaf (Some (wev,e)) => match weakTypeToTypeOfKind φ wev ★ with
438 | OK t' => [((wev:CoreVar),t')]
441 | T_Branch b1 b2 => (varsTypes b1 φ),,(varsTypes b2 φ)
444 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
445 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
446 | nil => match wtl with
448 | _ => Error "length mismatch in mkAvars"
450 | k::lk' => match wtl with
451 | nil => Error "length mismatch in mkAvars"
453 weakTypeToTypeOfKind φ wt k >>= fun t =>
454 mkAvars wtl' lk' φ >>= fun rest =>
455 OK (ICons _ _ t rest)
459 Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool :=
466 else update_ig ig vars' v'
469 (* does the specified variable occur free in the expression? *)
470 Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
473 | WEVar cv => if eqd_dec (wev:CoreVar) (cv:CoreVar) then true else false
474 | WECast e co => doesWeakVarOccur wev e
475 | WENote n e => doesWeakVarOccur wev e
476 | WETyApp e t => doesWeakVarOccur wev e
477 | WECoApp e co => doesWeakVarOccur wev e
478 | WEBrak _ ec e _ => doesWeakVarOccur wev e
479 | WEEsc _ ec e _ => doesWeakVarOccur wev e
480 | WECSP _ ec e _ => doesWeakVarOccur wev e
481 | WELet cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
482 | WEApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
483 | WELam cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
484 | WETyLam cv e => doesWeakVarOccur wev e
485 | WECoLam cv e => doesWeakVarOccur wev e
486 | WECase vscrut escrut tbranches tc avars alts =>
487 doesWeakVarOccur wev escrut ||
488 if eqd_dec (wev:CoreVar) (vscrut:CoreVar) then false else
489 ((fix doesWeakVarOccurAlts alts {struct alts} : bool :=
491 | T_Leaf None => false
492 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
493 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
494 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
495 | T_Branch b1 b2 => doesWeakVarOccurAlts b1 || doesWeakVarOccurAlts b2
498 doesWeakVarOccur wev e ||
499 (fix doesWeakVarOccurLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) : bool :=
501 | T_Leaf None => false
502 | T_Leaf (Some (cv,e)) => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
503 | T_Branch b1 b2 => doesWeakVarOccurLetRec b1 || doesWeakVarOccurLetRec b2
506 Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
507 (alts:Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr)) : bool :=
509 | T_Leaf None => false
510 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
511 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
512 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
513 | T_Branch b1 b2 => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
516 Definition checkDistinct :
517 forall {V}(EQ:EqDecidable V)(lv:list V), ???(distinct lv).
519 set (distinct_decidable lv) as q.
522 exact (Error "checkDistinct failed").
525 (* FIXME: check the kind of the type of the weakexprvar to support >0 *)
526 Definition mkGlobal Γ (τ:HaskType Γ ★) (wev:WeakExprVar) : Global Γ.
527 refine {| glob_kinds := nil |}.
533 Definition weakExprToStrongExpr : forall
537 (ψ:CoVarResolver Γ Δ)
538 (ξ:CoreVar -> LeveledHaskType Γ ★)
542 WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
544 fix weakExprToStrongExpr
548 (ψ:CoVarResolver Γ Δ)
549 (ξ:CoreVar -> LeveledHaskType Γ ★)
553 (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
554 addErrorMessage ("in weakExprToStrongExpr " +++ toString we)
558 then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ (τ@@lev))
559 else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
561 | WELit lit => castExpr we ("WELit "+++toString lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
563 | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
564 weakTypeOfWeakExpr ebody >>= fun tbody =>
565 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
566 let ξ' := update_ξ ξ lev (((ev:CoreVar),tv)::nil) in
567 let ig' := update_ig ig ((ev:CoreVar)::nil) in
568 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>
569 castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
571 | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' =>
572 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
573 weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' =>
574 castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
576 | WEEsc _ ec e tbody => φ ec >>= fun ec'' =>
577 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
579 | nil => Error "ill-leveled escapification"
580 | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
581 >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
584 | WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage"
586 | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
588 | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>
589 weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
590 weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ lev (((v:CoreVar),tv)::nil))
591 (update_ig ig ((v:CoreVar)::nil)) τ lev ebody
593 OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
595 | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
596 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
597 weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' =>
598 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' =>
599 OK (EApp _ _ _ _ _ _ e1' e2')
601 | WETyLam tv e => let φ' := upφ tv φ in
602 weakTypeOfWeakExpr e >>= fun te =>
603 weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
604 weakExprToStrongExpr _ (weakCE Δ) φ'
605 (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
606 >>= fun e' => castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
608 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
610 | WForAllTy wtv te' =>
611 let φ' := upφ wtv φ in
612 weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>
613 weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
614 weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
615 castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
616 | _ => Error ("weakTypeToType: WETyApp body with type "+++toString te)
619 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
621 | WCoFunTy t1 t2 t3 =>
622 weakTypeToType φ t1 >>= fun t1' =>
624 haskTypeOfSomeKind κ t1'' =>
625 weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
626 weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
627 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
628 castExpr we "WECoApp" _ e' >>= fun e'' =>
629 OK (ECoApp Γ Δ κ t1'' t2''
630 (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
632 | _ => Error ("weakTypeToType: WECoApp body with type "+++toString te)
635 | WECoLam cv e => let (_,t1,t2) := cv in
636 weakTypeOfWeakExpr e >>= fun te =>
637 weakTypeToTypeOfKind φ te ★ >>= fun te' =>
638 weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
639 weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
640 weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ ig te' lev e >>= fun e' =>
641 castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
643 | WECast e co => let (t1,t2) := weakCoercionTypes co in
644 weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
645 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
646 weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
647 castExpr we "WECast" _
648 (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
651 let ξ' := update_ξ ξ lev _ in
652 let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
654 (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
655 : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
657 | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
658 | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e)
660 binds b1 >>= fun b1' =>
661 binds b2 >>= fun b2' =>
662 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
664 in binds >>= fun binds' =>
665 checkDistinct CoreVarEqDecidable (map (@fst _ _) (leaves (varsTypes rb φ))) >>= fun rb_distinct =>
666 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
667 OK (ELetRec Γ Δ ξ lev τ _ _ binds' e')
669 | WECase vscrut escrut tbranches tc avars alts =>
670 weakTypeOfWeakExpr escrut >>= fun tscrut =>
671 weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
672 if doesWeakVarOccurAlts vscrut alts
673 then Error "encountered a Case which actually used its binder - these should have been desugared away!!"
674 else mkAvars avars (tyConKind tc) φ >>= fun avars' =>
675 weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' =>
676 (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
677 ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac &
678 Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@ lev))}}) :=
680 | T_Leaf None => OK []
681 | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
682 mkStrongAltConPlusJunk' tc ac >>= fun sac =>
683 list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
685 (let case_pf := tt in _) >>= fun pf =>
686 let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
687 weakExprToStrongExpr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
688 (sacpj_ψ sac _ _ avars' ψ)
690 (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
691 (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
692 let case_case := tt in OK [ _ ]
694 mkTree b1 >>= fun b1' =>
695 mkTree b2 >>= fun b2' =>
697 end) alts >>= fun tree =>
699 weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
700 castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
701 end)); try clear binds; try apply ConcatenableString.
704 apply (addErrorMessage "case_some").
706 destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
707 matchThings h (unlev (ξ' wev)) "LetRec".
709 rewrite matchTypeVars_pf.
710 clear matchTypeVars_pf.
711 set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
712 destruct e''; try apply (Error error_message).
717 induction (leaves (varsTypes rb φ)).
726 set (distinct_decidable (vec2list exprvars')) as dec.
727 destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ].