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 Definition weakExprToStrongExpr : forall
474 (ψ:CoVarResolver Γ Δ)
475 (ξ:CoreVar -> LeveledHaskType Γ ★)
479 WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
481 fix weakExprToStrongExpr
485 (ψ:CoVarResolver Γ Δ)
486 (ξ:CoreVar -> LeveledHaskType Γ ★)
490 (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
491 addErrorMessage ("in weakExprToStrongExpr " +++ we)
495 then OK (EGlobal Γ Δ ξ (τ@@lev) v)
496 else castExpr we ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
498 | WELit lit => castExpr we ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
500 | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
501 weakTypeOfWeakExpr ebody >>= fun tbody =>
502 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
503 let ξ' := update_ξ ξ (((ev:CoreVar),tv@@lev)::nil) in
504 let ig' := update_ig ig ((ev:CoreVar)::nil) in
505 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>
506 castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
508 | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' =>
509 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
510 weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' =>
511 castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
513 | WEEsc _ ec e tbody => φ ec >>= fun ec'' =>
514 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
516 | nil => Error "ill-leveled escapification"
517 | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
518 >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
521 | WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage"
523 | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
525 | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>
526 weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
527 weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil))
528 (update_ig ig ((v:CoreVar)::nil)) τ lev ebody
530 OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
532 | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
533 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
534 weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' =>
535 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' =>
536 OK (EApp _ _ _ _ _ _ e1' e2')
538 | WETyLam tv e => let φ' := upφ tv φ in
539 weakTypeOfWeakExpr e >>= fun te =>
540 weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
541 weakExprToStrongExpr _ (weakCE Δ) φ'
542 (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
543 >>= fun e' => castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
545 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
547 | WForAllTy wtv te' =>
548 let φ' := upφ wtv φ in
549 weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>
550 weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
551 weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
552 castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
553 | _ => Error ("weakTypeToType: WETyApp body with type "+++te)
556 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
558 | WCoFunTy t1 t2 t3 =>
559 weakTypeToType φ t1 >>= fun t1' =>
561 haskTypeOfSomeKind κ t1'' =>
562 weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
563 weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
564 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
565 castExpr we "WECoApp" _ e' >>= fun e'' =>
566 OK (ECoApp Γ Δ κ t1'' t2''
567 (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
569 | _ => Error ("weakTypeToType: WECoApp body with type "+++te)
572 | WECoLam cv e => let (_,_,t1,t2) := cv in
573 weakTypeOfWeakExpr e >>= fun te =>
574 weakTypeToTypeOfKind φ te ★ >>= fun te' =>
575 weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
576 weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
577 weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ ig te' lev e >>= fun e' =>
578 castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
580 | WECast e co => let (t1,t2) := weakCoercionTypes co in
581 weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
582 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
583 weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
584 castExpr we "WECast" _
585 (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
588 let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _) in
589 let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
591 (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
592 : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
594 | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
595 | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e)
597 binds b1 >>= fun b1' =>
598 binds b2 >>= fun b2' =>
599 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
601 in binds >>= fun binds' =>
602 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
603 OK (ELetRec Γ Δ ξ lev τ _ binds' e')
605 | WECase vscrut escrut tbranches tc avars alts =>
606 weakTypeOfWeakExpr escrut >>= fun tscrut =>
607 weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
609 let ξ' := update_ξ ξ (((vscrut:CoreVar),tscrut'@@lev)::nil) in
610 let ig' := update_ig ig ((vscrut:CoreVar)::nil) in
614 mkAvars avars (tyConKind tc) φ >>= fun avars' =>
615 weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' =>
616 (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
617 ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
618 Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ' lev)(weakLT' (tbranches' @@ lev))}) :=
620 | T_Leaf None => OK []
621 | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
622 mkStrongAltConPlusJunk' tc ac >>= fun sac =>
623 list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
625 let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
626 weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
627 (sacpj_ψ sac _ _ avars' ψ)
629 (update_ig ig' (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
630 (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
631 let case_case := tt in OK [ _ ]
633 mkTree b1 >>= fun b1' =>
634 mkTree b2 >>= fun b2' =>
636 end) alts >>= fun tree =>
638 weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
639 castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ' lev tc tbranches' avars' escrut' tree)
641 weakExprToStrongExpr Γ Δ φ ψ ξ ig tscrut' lev escrut >>= fun escrut' =>
642 castExpr we "ECaseScrut" (caseType tc avars' @@ lev) (EVar Γ Δ ξ' vscrut) >>= fun evscrut' =>
643 castExpr we "ECase" (τ@@lev)
644 (ELet Γ Δ ξ tscrut' tbranches' lev (vscrut:CoreVar) escrut'
645 (ECase Γ Δ ξ' lev tc tbranches' avars' evscrut' tree))
650 apply (addErrorMessage "case_some").
652 destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
653 matchThings h (unlev (ξ' wev)) "LetRec".
655 rewrite matchTypeVars_pf.
656 clear matchTypeVars_pf.
657 set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
658 destruct e''; try apply (Error error_message).