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 HaskCoreLiterals.
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 HaskCoreTypes.
21 Require Import HaskCoreVars.
22 Require Import HaskCoreToWeak.
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 +++ T1 +++ " " +++ 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 Γ) :=
121 | WFunTyCon => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow))
122 | WTyCon tc => let case_WTyCon := tt in _
123 | WClassP c lt => let case_WClassP := tt in Error "weakTypeToType: WClassP not implemented"
124 | WIParam _ ty => let case_WIParam := tt in Error "weakTypeToType: WIParam not implemented"
125 | WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
126 | WTyVarTy v => let case_WTyVarTy := tt in φ v >>= fun v' => _
127 | WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _
128 | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody >>= fun tbody' => φ (@fixkind ★ 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.
151 destruct case_WTyVarTy.
153 exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))).
155 destruct case_WAppTy.
156 destruct t1' as [k1' t1'].
157 destruct t2' as [k2' t2'].
159 try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
160 subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
161 apply (Error "Kind mismatch in WAppTy:: ").
163 destruct case_weakTypeListToTypeList.
164 destruct t' as [ k' t' ].
165 matchThings k k' "Kind mismatch in weakTypeListToTypeList".
167 apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
169 destruct case_WTyFunApp.
171 eapply haskTypeOfSomeKind.
172 unfold HaskType; intros.
177 destruct case_WTyCon.
179 eapply haskTypeOfSomeKind.
180 unfold HaskType; intros.
183 destruct case_WCodeTy.
185 matchThings κ ★ "Kind mismatch in WCodeTy: ".
187 eapply haskTypeOfSomeKind.
188 unfold HaskType; intros.
190 apply (TVar (ec' TV X)).
195 destruct case_WCoFunTy.
196 destruct t1' as [ k1' t1' ].
197 destruct t2' as [ k2' t2' ].
198 destruct t3' as [ k3' t3' ].
199 matchThings k1' k2' "Kind mismatch in arguments of WCoFunTy".
201 matchThings k3' ★ "Kind mismatch in result of WCoFunTy".
204 apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
206 destruct case_WForAllTy.
208 matchThings ★ κ "Kind mismatch in WForAllTy: ".
211 apply (@haskTypeOfSomeKind _ ★).
217 Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error".
219 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
220 Section StrongAltCon.
221 Context (tc : TyCon)(dc:DataCon tc).
223 Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
224 -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
227 set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
228 set (@substφ _ _ avars') as q.
229 set (upφ' (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ'.
230 set (@weakTypeToType _ φ' ct) as t.
231 destruct t as [|t]; try apply (Error error_message).
232 destruct t as [tk t].
233 matchThings tk ★ "weakTypeToType'".
236 set (@weakT'' _ Γ _ t) as t'.
237 set (@lamer _ _ _ _ t') as t''.
238 fold (tyConKinds tc) in t''.
239 fold (dataConExKinds dc) in t''.
243 unfold dataConExKinds.
244 rewrite <- vec2list_map_list2vec.
245 rewrite <- vec2list_map_list2vec.
246 rewrite vec2list_list2vec.
247 rewrite vec2list_list2vec.
251 Definition mkStrongAltCon : @StrongAltCon tc.
253 {| sac_altcon := DataAlt dc
254 ; sac_numCoerVars := length (dataConCoerKinds dc)
255 ; sac_numExprVars := length (dataConFieldTypes dc)
256 ; sac_ekinds := dataConExKinds dc
257 ; sac_coercions := fun Γ avars => let case_sac_coercions := tt in _
258 ; sac_types := fun Γ avars => let case_sac_types := tt in _
261 destruct case_sac_coercions.
262 refine (vec_map _ (list2vec (dataConCoerKinds dc))).
265 unfold tyConKind in avars.
266 set (@weakTypeToType' Γ) as q.
267 unfold tyConKinds in q.
268 rewrite <- vec2list_map_list2vec in q.
269 rewrite vec2list_list2vec in q.
272 q avars w >>= fun t1 =>
273 q avars w0 >>= fun t2 =>
274 OK (mkHaskCoercionKind t1 t2)
276 | Error s => Prelude_error s
280 destruct case_sac_types.
281 refine (vec_map _ (list2vec (dataConFieldTypes dc))).
283 unfold tyConKind in avars.
284 set (@weakTypeToType' Γ) as q.
285 unfold tyConKinds in q.
286 rewrite <- vec2list_map_list2vec in q.
287 rewrite vec2list_list2vec in q.
288 set (q avars X) as y.
290 | Error s =>Prelude_error s
296 Lemma weakCV' : forall {Γ}{Δ} Γ',
298 -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
300 unfold HaskCoVar in *.
301 intros; apply (X TV CV).
302 apply ilist_chop' in env; auto.
303 unfold InstantiatedCoercionEnv in *.
304 unfold weakCK'' in cenv.
306 rewrite <- map_preserves_length in cenv.
308 rewrite <- map_preserves_length in cenv.
312 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
314 {| sacpj_sac := mkStrongAltCon
315 ; sacpj_φ := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
317 fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
321 unfold HaskCoVar in *.
326 unfold InstantiatedCoercionEnv in *.
327 apply vec_chop' in cenv.
331 Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
342 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc).
344 set (c:DataCon _) as dc.
345 set ((dataConTyCon c):TyCon) as tc' in *.
346 set (eqd_dec tc tc') as eqpf; destruct eqpf;
348 | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++(dc:CoreDataCon))) ]; subst.
350 eapply mkStrongAltConPlusJunk.
354 apply OK; refine {| sacpj_sac := {|
355 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
356 ; sac_altcon := LitAlt h
358 intro; intro φ; apply φ.
359 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
360 rewrite weakCK'_nil_inert. apply ψ.
361 apply OK; refine {| sacpj_sac := {|
362 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
363 ; sac_altcon := DEFAULT |} |}.
364 intro; intro φ; apply φ.
365 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
366 rewrite weakCK'_nil_inert. apply ψ.
369 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
370 fun wev => match wev with weakExprVar _ t => t end.
371 Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
373 Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
375 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
376 WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
383 inversion cenv; auto.
386 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
387 Definition castExpr (err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
388 : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
391 destruct τ' as [τ' l'].
392 destruct (eqd_dec l l'); [ idtac | apply (Error ("level mismatch in castExpr: "+++err_msg)) ].
393 destruct (eqd_dec τ τ'); [ idtac | apply (Error ("type mismatch in castExpr: " +++err_msg+++" "+++τ+++" and "+++τ')) ].
399 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
400 match wcv with weakCoerVar _ κ _ _ => κ end.
401 Coercion coVarKind : WeakCoerVar >-> Kind.
403 Definition weakTypeToType'' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) κ, ???(HaskType Γ κ).
405 set (weakTypeToType φ t) as wt.
406 destruct wt; try apply (Error error_message).
408 matchThings κ κ0 "Kind mismatch in weakTypeToType'': ".
414 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
417 | T_Leaf (Some (wev,e)) => match weakTypeToType'' φ wev ★ with
419 | OK t' => [((wev:CoreVar),t')]
421 | T_Branch b1 b2 => (varsTypes b1 φ),,(varsTypes b2 φ)
425 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
426 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
427 | nil => match wtl with
429 | _ => Error "length mismatch in mkAvars"
431 | k::lk' => match wtl with
432 | nil => Error "length mismatch in mkAvars"
434 weakTypeToType'' φ wt k >>= fun t =>
435 mkAvars wtl' lk' φ >>= fun rest =>
436 OK (ICons _ _ t rest)
440 Definition weakExprToStrongExpr : forall
444 (ψ:CoVarResolver Γ Δ)
445 (ξ:CoreVar -> LeveledHaskType Γ ★)
448 WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
450 fix weakExprToStrongExpr
454 (ψ:CoVarResolver Γ Δ)
455 (ξ:CoreVar -> LeveledHaskType Γ ★)
458 (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
461 | WEVar v => castExpr ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
463 | WELit lit => castExpr ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
465 | WELam ev ebody => weakTypeToType'' φ ev ★ >>= fun tv =>
466 weakTypeOfWeakExpr ebody >>= fun tbody =>
467 weakTypeToType'' φ tbody ★ >>= fun tbody' =>
468 let ξ' := update_ξ ξ (((ev:CoreVar),tv@@lev)::nil) in
469 weakExprToStrongExpr Γ Δ φ ψ ξ' tbody' lev ebody >>= fun ebody' =>
470 castExpr "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
472 | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' =>
473 weakTypeToType'' φ tbody ★ >>= fun tbody' =>
474 weakExprToStrongExpr Γ Δ φ ψ ξ tbody' ((ec')::lev) e >>= fun e' =>
475 castExpr "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
477 | WEEsc _ ec e tbody => φ ec >>= fun ec'' =>
478 weakTypeToType'' φ tbody ★ >>= fun tbody' =>
480 | nil => Error "ill-leveled escapification"
481 | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ ec' |- tbody' ]>) lev' e
482 >>= fun e' => castExpr "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
485 | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
487 | WELet v ve ebody => weakTypeToType'' φ v ★ >>= fun tv =>
488 weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
489 weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) τ lev ebody
491 OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
493 | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
494 weakTypeToType'' φ t2 ★ >>= fun t2' =>
495 weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' =>
496 weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' =>
497 OK (EApp _ _ _ _ _ _ e1' e2')
499 | WETyLam tv e => let φ' := upφ tv φ in
500 weakTypeOfWeakExpr e >>= fun te =>
501 weakTypeToType'' φ' te ★ >>= fun τ' =>
502 weakExprToStrongExpr _ (weakCE Δ) φ'
503 (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) τ' (weakL lev) e
505 castExpr "WETyLam1" _ e' >>= fun e'' =>
506 castExpr "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e'')
508 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
510 | WForAllTy wtv te' =>
511 let φ' := upφ wtv φ in
512 weakTypeToType'' φ' te' ★ >>= fun te'' =>
513 weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' =>
514 weakTypeToType'' φ t (wtv:Kind) >>= fun t' =>
515 castExpr "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
516 | _ => Error ("weakTypeToType: WETyApp body with type "+++te)
519 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
521 | WCoFunTy t1 t2 t3 =>
522 weakTypeToType φ t1 >>= fun t1' =>
524 haskTypeOfSomeKind κ t1'' =>
525 weakTypeToType'' φ t2 κ >>= fun t2'' =>
526 weakTypeToType'' φ t3 ★ >>= fun t3'' =>
527 weakExprToStrongExpr Γ Δ φ ψ ξ (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
528 castExpr "WECoApp" _ e' >>= fun e'' =>
529 OK (ECoApp Γ Δ κ t1'' t2''
530 (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
532 | _ => Error ("weakTypeToType: WECoApp body with type "+++te)
535 | WECoLam cv e => let (_,_,t1,t2) := cv in
536 weakTypeOfWeakExpr e >>= fun te =>
537 weakTypeToType'' φ te ★ >>= fun te' =>
538 weakTypeToType'' φ t1 cv >>= fun t1' =>
539 weakTypeToType'' φ t2 cv >>= fun t2' =>
540 weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
541 castExpr "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
543 | WECast e co => let (κ,t1,t2,_) := co in
544 weakTypeToType'' φ t1 ★ >>= fun t1' =>
545 weakTypeToType'' φ t2 ★ >>= fun t2' =>
546 weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>
548 (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
551 let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _)
553 (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
554 : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
556 | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
557 | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e)
559 binds b1 >>= fun b1' =>
560 binds b2 >>= fun b2' =>
561 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
563 in binds >>= fun binds' =>
564 weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e >>= fun e' =>
565 OK (ELetRec Γ Δ ξ lev τ _ binds' e')
567 | WECase vscrut ve tbranches tc avars alts =>
568 weakTypeToType'' φ (vscrut:WeakType) ★ >>= fun tv =>
569 weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
570 let ξ' := update_ξ ξ (((vscrut:CoreVar),tv@@lev)::nil) in
571 mkAvars avars (tyConKind tc) φ >>= fun avars' =>
572 weakTypeToType'' φ tbranches ★ >>= fun tbranches' =>
573 (fix mkTree (t:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
574 ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
575 Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ' lev)(weakLT' (tbranches' @@ lev))}) :=
577 | T_Leaf None => OK []
578 | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
579 mkStrongAltConPlusJunk' tc ac >>= fun sac =>
580 list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
582 let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
583 weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
584 (sacpj_ψ sac _ _ avars' ψ)
585 (scbwv_ξ scb ξ' lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
586 let case_case := tt in OK [ _ ]
588 mkTree b1 >>= fun b1' =>
589 mkTree b2 >>= fun b2' =>
591 end) alts >>= fun tree =>
592 castExpr "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun escrut =>
593 castExpr "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' escrut tree)
594 >>= fun ecase' => OK (ELet _ _ _ tv _ lev (vscrut:CoreVar) ve' ecase')
602 destruct (weakTypeToType'' φ wev ★); try apply (Error error_message).
603 matchThings h (unlev (ξ' wev)) "LetRec".
605 rewrite matchTypeVars_pf.
606 clear matchTypeVars_pf.
607 set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
608 destruct e''; try apply (Error error_message).