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 HaskStrongTypes.
18 Require Import HaskStrong.
19 Require Import HaskCoreTypes.
20 Require Import HaskCoreVars.
21 Require Import HaskCoreToWeak.
23 Open Scope string_scope.
24 Definition TyVarResolver Γ := forall wt:WeakTypeVar, HaskTyVar Γ wt.
25 Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, HaskCoVar Γ Δ.
27 Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
31 then let fresh := @FreshHaskTyVar Γ tv in _
32 else fun TV ite => φ tv' TV (weakITE ite)).
33 rewrite <- _H; apply fresh.
36 Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ)
37 : (TyVarResolver (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)).
45 Definition substPhi {Γ:TypeEnv}(κ κ':Kind)(θ:HaskType Γ κ) : HaskType (κ::Γ) κ' -> HaskType Γ κ'.
49 unfold HaskType in ht.
52 apply ICons; [ idtac | apply env ].
56 Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ.
62 inversion θ; subst; auto.
70 (* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *)
71 Record StrongAltConPlusJunk {tc:TyCon} :=
72 { sacpj_sac : @StrongAltCon tc
73 ; sacpj_φ : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_Γ sacpj_sac Γ))
74 ; sacpj_ψ : forall Γ Δ atypes (ψ:WeakCoerVar -> HaskCoVar Γ Δ),
75 (WeakCoerVar -> HaskCoVar _ (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 _
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' => _
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 (φ (@fixkind ★ 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 => weakV' (φ htv))
316 ; sacpj_ψ := fun Γ Δ avars ψ => (fun htv => _ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) (ψ htv)))
320 unfold HaskCoVar in *.
325 unfold InstantiatedCoercionEnv in *.
326 apply vec_chop' in cenv.
330 Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
341 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc).
343 set (c:DataCon _) as dc.
344 set ((dataConTyCon c):TyCon) as tc' in *.
345 set (eqd_dec tc tc') as eqpf; destruct eqpf;
347 | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++(dc:CoreDataCon))) ]; subst.
349 eapply mkStrongAltConPlusJunk.
353 apply OK; refine {| sacpj_sac := {|
354 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
355 ; sac_altcon := LitAlt h
357 intro; intro φ; apply φ.
358 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
359 rewrite weakCK'_nil_inert. apply ψ.
360 apply OK; refine {| sacpj_sac := {|
361 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
362 ; sac_altcon := DEFAULT |} |}.
363 intro; intro φ; apply φ.
364 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
365 rewrite weakCK'_nil_inert. apply ψ.
368 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
369 fun wev => match wev with weakExprVar _ t => t end.
370 Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
372 Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
374 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> HaskCoVar Γ Δ) :
375 WeakCoerVar -> HaskCoVar Γ (κ::Δ).
379 apply (ψ X TV CV env).
380 inversion cenv; auto.
383 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
384 Definition castExpr (err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
385 : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
388 destruct τ' as [τ' l'].
389 destruct (eqd_dec l l'); [ idtac | apply (Error ("level mismatch in castExpr: "+++err_msg)) ].
390 destruct (eqd_dec τ τ'); [ idtac | apply (Error ("type mismatch in castExpr: " +++err_msg+++" "+++τ+++" and "+++τ')) ].
396 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
397 match wcv with weakCoerVar _ κ _ _ => κ end.
398 Coercion coVarKind : WeakCoerVar >-> Kind.
400 Definition weakTypeToType'' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) κ, ???(HaskType Γ κ).
402 set (weakTypeToType φ t) as wt.
403 destruct wt; try apply (Error error_message).
405 matchThings κ κ0 "Kind mismatch in weakTypeToType'': ".
411 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
414 | T_Leaf (Some (wev,e)) => match weakTypeToType'' φ wev ★ with
416 | OK t' => [((wev:CoreVar),t')]
418 | T_Branch b1 b2 => (varsTypes b1 φ),,(varsTypes b2 φ)
422 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
423 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
424 | nil => match wtl with
426 | _ => Error "length mismatch in mkAvars"
428 | k::lk' => match wtl with
429 | nil => Error "length mismatch in mkAvars"
431 weakTypeToType'' φ wt k >>= fun t =>
432 mkAvars wtl' lk' φ >>= fun rest =>
433 OK (ICons _ _ t rest)
437 Definition weakExprToStrongExpr : forall
441 (ψ:CoVarResolver Γ Δ)
442 (ξ:CoreVar -> LeveledHaskType Γ ★)
445 WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
447 fix weakExprToStrongExpr
451 (ψ:CoVarResolver Γ Δ)
452 (ξ:CoreVar -> LeveledHaskType Γ ★)
455 (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
458 | WEVar v => castExpr "WEVar" (τ @@ lev) (EVar Γ Δ ξ v)
460 | WELit lit => castExpr "WELit" (τ @@ lev) (ELit Γ Δ ξ lit lev)
462 | WELam ev e => weakTypeToType'' φ ev ★ >>= fun tv =>
463 weakTypeOfWeakExpr e >>= fun t =>
464 weakTypeToType'' φ t ★ >>= fun τ' =>
465 weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((ev:CoreVar),tv@@lev)::nil))
467 castExpr "WELam" _ (ELam Γ Δ ξ tv _ _ ev e')
469 | WEBrak _ ec e tbody => weakExprToStrongExpr Γ Δ φ ψ ξ τ ((φ (`ec))::lev) e >>= fun e' =>
470 castExpr "WEBrak" _ (EBrak _ _ _ (φ (`ec)) _ lev e')
472 | WEEsc _ ec e tbody => weakTypeToType'' φ tbody ★ >>= fun tbody' =>
474 | nil => Error "ill-leveled escapification"
475 | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ φ (`ec) |- tbody' ]>) lev e
477 castExpr "WEEsc" (τ@@lev) (EEsc _ _ _ (φ (`ec)) _ lev e')
479 | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
481 | WELet v ve ebody => weakTypeToType'' φ v ★ >>= fun tv =>
482 weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
483 weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) τ lev ebody
485 OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
487 | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
488 weakTypeToType'' φ t2 ★ >>= fun t2' =>
489 weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' =>
490 weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' =>
491 OK (EApp _ _ _ _ _ _ e1' e2')
493 | WETyLam tv e => let φ' := upφ tv φ in
494 weakTypeOfWeakExpr e >>= fun te =>
495 weakTypeToType'' φ' te ★ >>= fun τ' =>
496 weakExprToStrongExpr _ (weakCE Δ) φ' (weakCV○ψ) (weakLT○ξ) τ' (weakL lev) e
498 castExpr "WETyLam1" _ e' >>= fun e'' =>
499 castExpr "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e'')
501 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
503 | WForAllTy wtv te' =>
504 let φ' := upφ wtv φ in
505 weakTypeToType'' φ' te' ★ >>= fun te'' =>
506 weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' =>
507 weakTypeToType'' φ t wtv >>= fun t' =>
508 castExpr "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
509 | _ => Error ("weakTypeToType: WETyApp body with type "+++te)
512 (* I had all of these working before I switched to a Kind-indexed representation for types; it will take a day or two
513 * to get them back working again *)
514 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
516 | WCoFunTy t1 t2 t3 =>
517 weakTypeToType φ t1 >>= fun t1' =>
519 haskTypeOfSomeKind κ t1'' =>
520 weakTypeToType'' φ t2 κ >>= fun t2'' =>
521 weakTypeToType'' φ t3 ★ >>= fun t3'' =>
522 weakExprToStrongExpr Γ Δ φ ψ ξ (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
523 castExpr "WECoApp" _ e' >>= fun e'' =>
524 OK (ECoApp Γ Δ κ t1'' t2''
525 (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
527 | _ => Error ("weakTypeToType: WECoApp body with type "+++te)
530 | WECoLam cv e => let (_,_,t1,t2) := cv in
531 weakTypeOfWeakExpr e >>= fun te =>
532 weakTypeToType'' φ te ★ >>= fun te' =>
533 weakTypeToType'' φ t1 cv >>= fun t1' =>
534 weakTypeToType'' φ t2 cv >>= fun t2' =>
535 weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
536 castExpr "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
538 | WECast e co => let (κ,t1,t2,_) := co in
539 weakTypeToType'' φ t1 ★ >>= fun t1' =>
540 weakTypeToType'' φ t2 ★ >>= fun t2' =>
541 weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>
543 (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
546 let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _)
548 (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
549 : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
551 | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
552 | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e)
554 binds b1 >>= fun b1' =>
555 binds b2 >>= fun b2' =>
556 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
558 in binds >>= fun binds' =>
559 weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e >>= fun e' =>
560 OK (ELetRec Γ Δ ξ lev τ _ binds' e')
562 | WECase vscrut e tbranches tc avars alts =>
563 mkAvars avars (tyConKind tc) φ >>= fun avars' =>
564 weakTypeToType'' φ tbranches ★ >>= fun tbranches' =>
565 let ξ' := update_ξ ξ (((vscrut:CoreVar), _ @@lev)::nil) in
566 (fix mkTree (t:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
568 : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars'
570 Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))
571 (scbwv_ξ scb ξ' lev) (weakLT' (tbranches' @@ lev))}) :=
573 | T_Leaf None => OK []
574 | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
575 mkStrongAltConPlusJunk' tc ac >>= fun sac =>
576 list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase") >>= fun exprvars' =>
577 let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
578 weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ) (sacpj_ψ sac _ _ avars' ψ)
579 (scbwv_ξ scb ξ' lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
580 let case_case := tt in OK [ _ ]
582 mkTree b1 >>= fun b1' =>
583 mkTree b2 >>= fun b2' =>
586 ) alts >>= fun tree =>
587 weakExprToStrongExpr Γ Δ φ ψ ξ (caseType tc avars') lev e >>= fun e' =>
588 castExpr "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun evar =>
589 castExpr "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' evar tree) >>= fun ecase' =>
590 OK (ELet _ _ _ _ _ lev (vscrut:CoreVar) e' ecase')
595 destruct (weakTypeToType'' φ wev ★); try apply (Error error_message).
596 matchThings h (unlev (ξ' wev)) "LetRec".
598 rewrite matchTypeVars_pf.
599 clear matchTypeVars_pf.
600 set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
601 destruct e''; try apply (Error error_message).
607 clear mkTree t o p e p0 p1 p2 alts weakExprToStrongExpr ebranch.