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.
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 OK _
32 else φ tv' >>= fun tv'' => OK (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 (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ))
76 Implicit Arguments StrongAltConPlusJunk [ ].
77 Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon.
79 (* yes, I know, this is really clumsy *)
80 Variable emptyφ : TyVarResolver nil.
81 Extract Inlined Constant emptyφ => "(\x -> Prelude.error ""encountered unbound tyvar!"")".
83 Definition mkPhi (lv:list WeakTypeVar)
84 : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)).
85 set (upφ'(Γ:=nil) lv emptyφ) as φ'.
86 rewrite <- app_nil_end in φ'.
90 Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)).
91 Definition tyConKinds tc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (tyConTyVars tc)).
93 Definition fixkind {κ}(tv:WeakTypeVar) := weakTypeVar tv κ.
94 Notation " ` x " := (@fixkind _ x) (at level 100).
96 Ltac matchThings T1 T2 S :=
97 destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];
98 [ idtac | apply (Error (S +++ T1 +++ " " +++ T2)) ].
100 Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★).
102 unfold InstantiatedTypeEnv in ite.
107 Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★.
117 Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ).
118 refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) :=
119 addErrorMessage ("weakTypeToType " +++ t)
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.
152 apply (addErrorMessage "case_WTyVarTy").
154 exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))).
156 destruct case_WAppTy.
157 apply (addErrorMessage "case_WAppTy").
158 destruct t1' as [k1' t1'].
159 destruct t2' as [k2' t2'].
160 set ("tried to apply type "+++t1'+++" of kind "+++k1'+++" to type "+++t2'+++" of kind "+++k2') as err.
162 try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
163 subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
164 apply (Error ("Kind mismatch in WAppTy: "+++err)).
166 destruct case_weakTypeListToTypeList.
167 apply (addErrorMessage "case_weakTypeListToTypeList").
168 destruct t' as [ k' t' ].
169 matchThings k k' "Kind mismatch in weakTypeListToTypeList".
171 apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
173 destruct case_WTyFunApp.
174 apply (addErrorMessage "case_WTyFunApp").
176 eapply haskTypeOfSomeKind.
177 unfold HaskType; intros.
182 destruct case_WTyCon.
183 apply (addErrorMessage "case_WTyCon").
185 eapply haskTypeOfSomeKind.
186 unfold HaskType; intros.
189 destruct case_WCodeTy.
190 apply (addErrorMessage "case_WCodeTy").
192 matchThings κ ★ "Kind mismatch in WCodeTy: ".
194 eapply haskTypeOfSomeKind.
195 unfold HaskType; intros.
197 apply (TVar (ec' TV X)).
202 destruct case_WCoFunTy.
203 apply (addErrorMessage "case_WCoFunTy").
204 destruct t1' as [ k1' t1' ].
205 destruct t2' as [ k2' t2' ].
206 destruct t3' as [ k3' t3' ].
207 matchThings k1' k2' "Kind mismatch in arguments of WCoFunTy".
209 matchThings k3' ★ "Kind mismatch in result of WCoFunTy".
212 apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
214 destruct case_WForAllTy.
215 apply (addErrorMessage "case_WForAllTy").
217 matchThings ★ κ "Kind mismatch in WForAllTy: ".
220 apply (@haskTypeOfSomeKind _ ★).
226 Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error".
228 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
229 Section StrongAltCon.
230 Context (tc : TyCon)(dc:DataCon tc).
232 Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
233 -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
236 apply (addErrorMessage "weakTypeToType'").
237 set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
238 set (@substφ _ _ avars') as q.
239 set (upφ' (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ'.
240 set (@weakTypeToType _ φ' ct) as t.
241 destruct t as [|t]; try apply (Error error_message).
242 destruct t as [tk t].
243 matchThings tk ★ "weakTypeToType'".
246 set (@weakT'' _ Γ _ t) as t'.
247 set (@lamer _ _ _ _ t') as t''.
248 fold (tyConKinds tc) in t''.
249 fold (dataConExKinds dc) in t''.
253 unfold dataConExKinds.
254 rewrite <- vec2list_map_list2vec.
255 rewrite <- vec2list_map_list2vec.
256 rewrite vec2list_list2vec.
257 rewrite vec2list_list2vec.
261 Definition mkStrongAltCon : @StrongAltCon tc.
263 {| sac_altcon := DataAlt dc
264 ; sac_numCoerVars := length (dataConCoerKinds dc)
265 ; sac_numExprVars := length (dataConFieldTypes dc)
266 ; sac_ekinds := dataConExKinds dc
267 ; sac_coercions := fun Γ avars => let case_sac_coercions := tt in _
268 ; sac_types := fun Γ avars => let case_sac_types := tt in _
271 destruct case_sac_coercions.
272 refine (vec_map _ (list2vec (dataConCoerKinds dc))).
275 unfold tyConKind in avars.
276 set (@weakTypeToType' Γ) as q.
277 unfold tyConKinds in q.
278 rewrite <- vec2list_map_list2vec in q.
279 rewrite vec2list_list2vec in q.
282 q avars w >>= fun t1 =>
283 q avars w0 >>= fun t2 =>
284 OK (mkHaskCoercionKind t1 t2)
286 | Error s => Prelude_error s
290 destruct case_sac_types.
291 refine (vec_map _ (list2vec (dataConFieldTypes dc))).
293 unfold tyConKind in avars.
294 set (@weakTypeToType' Γ) as q.
295 unfold tyConKinds in q.
296 rewrite <- vec2list_map_list2vec in q.
297 rewrite vec2list_list2vec in q.
298 set (q avars X) as y.
300 | Error s =>Prelude_error s
306 Lemma weakCV' : forall {Γ}{Δ} Γ',
308 -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
310 unfold HaskCoVar in *.
311 intros; apply (X TV CV).
312 apply ilist_chop' in env; auto.
313 unfold InstantiatedCoercionEnv in *.
314 unfold weakCK'' in cenv.
316 rewrite <- map_preserves_length in cenv.
318 rewrite <- map_preserves_length in cenv.
322 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
324 {| sacpj_sac := mkStrongAltCon
325 ; sacpj_φ := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
327 fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
331 unfold HaskCoVar in *.
336 unfold InstantiatedCoercionEnv in *.
337 apply vec_chop' in cenv.
341 Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
352 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc).
354 set (c:DataCon _) as dc.
355 set ((dataConTyCon c):TyCon) as tc' in *.
356 set (eqd_dec tc tc') as eqpf; destruct eqpf;
358 | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++(dc:CoreDataCon))) ]; subst.
360 eapply mkStrongAltConPlusJunk.
364 apply OK; refine {| sacpj_sac := {|
365 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
366 ; sac_altcon := LitAlt h
368 intro; intro φ; apply φ.
369 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
370 rewrite weakCK'_nil_inert. apply ψ.
371 apply OK; refine {| sacpj_sac := {|
372 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
373 ; sac_altcon := DEFAULT |} |}.
374 intro; intro φ; apply φ.
375 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
376 rewrite weakCK'_nil_inert. apply ψ.
379 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
380 fun wev => match wev with weakExprVar _ t => t end.
381 Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
383 Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
385 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
386 WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
393 inversion cenv; auto.
396 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
397 Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
398 : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
399 apply (addErrorMessage ("castExpr " +++ err_msg)).
402 destruct τ' as [τ' l'].
403 destruct (eqd_dec l l'); [ idtac
404 | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
405 " got: " +++(fold_left (fun x y => y+++","+++y) (map haskTyVarToType l) "")+++eol+++
406 " wanted: "+++(fold_left (fun x y => x+++","+++y) (map haskTyVarToType l') "")
408 destruct (eqd_dec τ τ'); [ idtac
409 | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
410 " got: " +++τ+++eol+++
418 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
419 match wcv with weakCoerVar _ κ _ _ => κ end.
420 Coercion coVarKind : WeakCoerVar >-> Kind.
422 Definition weakTypeToType'' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) κ, ???(HaskType Γ κ).
424 set (weakTypeToType φ t) as wt.
425 destruct wt; try apply (Error error_message).
427 matchThings κ κ0 "Kind mismatch in weakTypeToType'': ".
433 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
436 | T_Leaf (Some (wev,e)) => match weakTypeToType'' φ wev ★ with
438 | OK t' => [((wev:CoreVar),t')]
440 | 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 weakTypeToType'' φ wt k >>= fun t =>
454 mkAvars wtl' lk' φ >>= fun rest =>
455 OK (ICons _ _ t rest)
459 Definition weakExprToStrongExpr : forall
463 (ψ:CoVarResolver Γ Δ)
464 (ξ:CoreVar -> LeveledHaskType Γ ★)
467 WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
469 fix weakExprToStrongExpr
473 (ψ:CoVarResolver Γ Δ)
474 (ξ:CoreVar -> LeveledHaskType Γ ★)
477 (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
480 | WEVar v => castExpr we ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
482 | WELit lit => castExpr we ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
484 | WELam ev ebody => weakTypeToType'' φ ev ★ >>= fun tv =>
485 weakTypeOfWeakExpr ebody >>= fun tbody =>
486 weakTypeToType'' φ tbody ★ >>= fun tbody' =>
487 let ξ' := update_ξ ξ (((ev:CoreVar),tv@@lev)::nil) in
488 weakExprToStrongExpr Γ Δ φ ψ ξ' tbody' lev ebody >>= fun ebody' =>
489 castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
491 | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' =>
492 weakTypeToType'' φ tbody ★ >>= fun tbody' =>
493 weakExprToStrongExpr Γ Δ φ ψ ξ tbody' ((ec')::lev) e >>= fun e' =>
494 castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
496 | WEEsc _ ec e tbody => φ ec >>= fun ec'' =>
497 weakTypeToType'' φ tbody ★ >>= fun tbody' =>
499 | nil => Error "ill-leveled escapification"
500 | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ ec' |- tbody' ]>) lev' e
501 >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
504 | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
506 | WELet v ve ebody => weakTypeToType'' φ v ★ >>= fun tv =>
507 weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
508 weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) τ lev ebody
510 OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
512 | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
513 weakTypeToType'' φ t2 ★ >>= fun t2' =>
514 weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' =>
515 weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' =>
516 OK (EApp _ _ _ _ _ _ e1' e2')
518 | WETyLam tv e => let φ' := upφ tv φ in
519 weakTypeOfWeakExpr e >>= fun te =>
520 weakTypeToType'' φ' te ★ >>= fun τ' =>
521 weakExprToStrongExpr _ (weakCE Δ) φ'
522 (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) τ' (weakL lev) e
524 castExpr we "WETyLam1" _ e' >>= fun e'' =>
525 castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e'')
527 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
529 | WForAllTy wtv te' =>
530 let φ' := upφ wtv φ in
531 weakTypeToType'' φ' te' ★ >>= fun te'' =>
532 weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' =>
533 weakTypeToType'' φ t (wtv:Kind) >>= fun t' =>
534 castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
535 | _ => Error ("weakTypeToType: WETyApp body with type "+++te)
538 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
540 | WCoFunTy t1 t2 t3 =>
541 weakTypeToType φ t1 >>= fun t1' =>
543 haskTypeOfSomeKind κ t1'' =>
544 weakTypeToType'' φ t2 κ >>= fun t2'' =>
545 weakTypeToType'' φ t3 ★ >>= fun t3'' =>
546 weakExprToStrongExpr Γ Δ φ ψ ξ (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
547 castExpr we "WECoApp" _ e' >>= fun e'' =>
548 OK (ECoApp Γ Δ κ t1'' t2''
549 (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
551 | _ => Error ("weakTypeToType: WECoApp body with type "+++te)
554 | WECoLam cv e => let (_,_,t1,t2) := cv in
555 weakTypeOfWeakExpr e >>= fun te =>
556 weakTypeToType'' φ te ★ >>= fun te' =>
557 weakTypeToType'' φ t1 cv >>= fun t1' =>
558 weakTypeToType'' φ t2 cv >>= fun t2' =>
559 weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
560 castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
562 | WECast e co => let (t1,t2) := weakCoercionTypes co in
563 weakTypeToType'' φ t1 ★ >>= fun t1' =>
564 weakTypeToType'' φ t2 ★ >>= fun t2' =>
565 weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>
566 castExpr we "WECast" _
567 (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
570 let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _)
572 (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
573 : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
575 | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
576 | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e)
578 binds b1 >>= fun b1' =>
579 binds b2 >>= fun b2' =>
580 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
582 in binds >>= fun binds' =>
583 weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e >>= fun e' =>
584 OK (ELetRec Γ Δ ξ lev τ _ binds' e')
586 | WECase vscrut ve tbranches tc avars alts =>
587 weakTypeToType'' φ (vscrut:WeakType) ★ >>= fun tv =>
588 weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
589 let ξ' := update_ξ ξ (((vscrut:CoreVar),tv@@lev)::nil) in
590 mkAvars avars (tyConKind tc) φ >>= fun avars' =>
591 weakTypeToType'' φ tbranches ★ >>= fun tbranches' =>
592 (fix mkTree (t:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
593 ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
594 Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ' lev)(weakLT' (tbranches' @@ lev))}) :=
596 | T_Leaf None => OK []
597 | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
598 mkStrongAltConPlusJunk' tc ac >>= fun sac =>
599 list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
601 let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
602 weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
603 (sacpj_ψ sac _ _ avars' ψ)
604 (scbwv_ξ scb ξ' lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
605 let case_case := tt in OK [ _ ]
607 mkTree b1 >>= fun b1' =>
608 mkTree b2 >>= fun b2' =>
610 end) alts >>= fun tree =>
611 castExpr we "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun escrut =>
612 castExpr we "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' escrut tree)
613 >>= fun ecase' => OK (ELet _ _ _ tv _ lev (vscrut:CoreVar) ve' ecase')
620 apply (addErrorMessage "case_some").
622 destruct (weakTypeToType'' φ wev ★); try apply (Error error_message).
623 matchThings h (unlev (ξ' wev)) "LetRec".
625 rewrite matchTypeVars_pf.
626 clear matchTypeVars_pf.
627 set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
628 destruct e''; try apply (Error error_message).