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.
22 Open Scope string_scope.
23 Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
24 Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
26 Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
30 then let fresh := @FreshHaskTyVar Γ tv in OK _
31 else φ tv' >>= fun tv'' => OK (fun TV ite => tv'' TV (weakITE ite))).
32 rewrite <- _H; apply fresh.
35 Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ)
36 : (TyVarResolver (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)).
44 Definition substPhi {Γ:TypeEnv}(κ κ':Kind)(θ:HaskType Γ κ) : HaskType (κ::Γ) κ' -> HaskType Γ κ'.
48 unfold HaskType in ht.
51 apply ICons; [ idtac | apply env ].
55 Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ.
61 inversion θ; subst; auto.
69 (* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *)
70 Record StrongAltConPlusJunk {tc:TyCon} :=
71 { sacpj_sac : @StrongAltCon tc
72 ; sacpj_φ : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_Γ sacpj_sac Γ))
73 ; sacpj_ψ : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ))
75 Implicit Arguments StrongAltConPlusJunk [ ].
76 Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon.
78 (* yes, I know, this is really clumsy *)
79 Variable emptyφ : TyVarResolver nil.
80 Extract Inlined Constant emptyφ => "(\x -> Prelude.error ""encountered unbound tyvar!"")".
82 Definition mkPhi (lv:list WeakTypeVar)
83 : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)).
84 set (upφ'(Γ:=nil) lv emptyφ) as φ'.
85 rewrite <- app_nil_end in φ'.
89 Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)).
90 Definition tyConKinds tc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (tyConTyVars tc)).
92 Definition fixkind {κ}(tv:WeakTypeVar) := weakTypeVar tv κ.
93 Notation " ` x " := (@fixkind _ x) (at level 100).
95 Ltac matchThings T1 T2 S :=
96 destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];
97 [ idtac | apply (Error (S +++ T1 +++ " " +++ T2)) ].
99 Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★).
101 unfold InstantiatedTypeEnv in ite.
106 Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★.
116 Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ).
117 refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) :=
118 addErrorMessage ("weakTypeToType " +++ t)
120 | WFunTyCon => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow))
121 | WTyCon tc => let case_WTyCon := tt in _
122 | WClassP c lt => let case_WClassP := tt in Error "weakTypeToType: WClassP not implemented"
123 | WIParam _ ty => let case_WIParam := tt in Error "weakTypeToType: WIParam not implemented"
124 | WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
125 | WTyVarTy v => let case_WTyVarTy := tt in φ v >>= fun v' => _
126 | WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _
127 | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody >>= fun tbody' => φ (@fixkind ★ ec) >>= fun ec' => _
128 | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt in
129 weakTypeToType _ φ t1 >>= fun t1' =>
130 weakTypeToType _ φ t2 >>= fun t2' =>
131 weakTypeToType _ φ t3 >>= fun t3' => _
133 ((fix weakTypeListToTypeList (lk:list Kind) (lt:list WeakType)
134 { struct lt } : ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV lk) :=
136 | nil => match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
137 | nil => OK (fun TV _ => TyFunApp_nil)
138 | _ => Error "WTyFunApp not applied to enough types"
140 | tx::lt' => weakTypeToType Γ φ tx >>= fun t' =>
141 match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
142 | nil => Error "WTyFunApp applied to too many types"
143 | k::lk' => weakTypeListToTypeList lk' lt' >>= fun rhtl' =>
144 let case_weakTypeListToTypeList := tt in _
147 ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in _
148 end ); clear weakTypeToType.
150 destruct case_WTyVarTy.
151 apply (addErrorMessage "case_WTyVarTy").
153 exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))).
155 destruct case_WAppTy.
156 apply (addErrorMessage "case_WAppTy").
157 destruct t1' as [k1' t1'].
158 destruct t2' as [k2' t2'].
159 set ("tried to apply type "+++t1'+++" of kind "+++k1'+++" to type "+++t2'+++" of kind "+++k2') as err.
161 try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
162 subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
163 apply (Error ("Kind mismatch in WAppTy: "+++err)).
165 destruct case_weakTypeListToTypeList.
166 apply (addErrorMessage "case_weakTypeListToTypeList").
167 destruct t' as [ k' t' ].
168 matchThings k k' "Kind mismatch in weakTypeListToTypeList".
170 apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
172 destruct case_WTyFunApp.
173 apply (addErrorMessage "case_WTyFunApp").
175 eapply haskTypeOfSomeKind.
176 unfold HaskType; intros.
181 destruct case_WTyCon.
182 apply (addErrorMessage "case_WTyCon").
184 eapply haskTypeOfSomeKind.
185 unfold HaskType; intros.
188 destruct case_WCodeTy.
189 apply (addErrorMessage "case_WCodeTy").
191 matchThings κ ★ "Kind mismatch in WCodeTy: ".
193 eapply haskTypeOfSomeKind.
194 unfold HaskType; intros.
196 apply (TVar (ec' TV X)).
201 destruct case_WCoFunTy.
202 apply (addErrorMessage "case_WCoFunTy").
203 destruct t1' as [ k1' t1' ].
204 destruct t2' as [ k2' t2' ].
205 destruct t3' as [ k3' t3' ].
206 matchThings k1' k2' "Kind mismatch in arguments of WCoFunTy".
208 matchThings k3' ★ "Kind mismatch in result of WCoFunTy".
211 apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
213 destruct case_WForAllTy.
214 apply (addErrorMessage "case_WForAllTy").
216 matchThings ★ κ "Kind mismatch in WForAllTy: ".
219 apply (@haskTypeOfSomeKind _ ★).
225 Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error".
227 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
228 Section StrongAltCon.
229 Context (tc : TyCon)(dc:DataCon tc).
231 Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
232 -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
235 apply (addErrorMessage "weakTypeToType'").
236 set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
237 set (@substφ _ _ avars') as q.
238 set (upφ' (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ'.
239 set (@weakTypeToType _ φ' ct) as t.
240 destruct t as [|t]; try apply (Error error_message).
241 destruct t as [tk t].
242 matchThings tk ★ "weakTypeToType'".
245 set (@weakT'' _ Γ _ t) as t'.
246 set (@lamer _ _ _ _ t') as t''.
247 fold (tyConKinds tc) in t''.
248 fold (dataConExKinds dc) in t''.
252 unfold dataConExKinds.
253 rewrite <- vec2list_map_list2vec.
254 rewrite <- vec2list_map_list2vec.
255 rewrite vec2list_list2vec.
256 rewrite vec2list_list2vec.
260 Definition mkStrongAltCon : @StrongAltCon tc.
262 {| sac_altcon := WeakDataAlt dc
263 ; sac_numCoerVars := length (dataConCoerKinds dc)
264 ; sac_numExprVars := length (dataConFieldTypes dc)
265 ; sac_ekinds := dataConExKinds dc
266 ; sac_coercions := fun Γ avars => let case_sac_coercions := tt in _
267 ; sac_types := fun Γ avars => let case_sac_types := tt in _
270 destruct case_sac_coercions.
271 refine (vec_map _ (list2vec (dataConCoerKinds dc))).
274 unfold tyConKind in avars.
275 set (@weakTypeToType' Γ) as q.
276 unfold tyConKinds in q.
277 rewrite <- vec2list_map_list2vec in q.
278 rewrite vec2list_list2vec in q.
281 q avars w >>= fun t1 =>
282 q avars w0 >>= fun t2 =>
283 OK (mkHaskCoercionKind t1 t2)
285 | Error s => Prelude_error s
289 destruct case_sac_types.
290 refine (vec_map _ (list2vec (dataConFieldTypes dc))).
292 unfold tyConKind in avars.
293 set (@weakTypeToType' Γ) as q.
294 unfold tyConKinds in q.
295 rewrite <- vec2list_map_list2vec in q.
296 rewrite vec2list_list2vec in q.
297 set (q avars X) as y.
299 | Error s =>Prelude_error s
305 Lemma weakCV' : forall {Γ}{Δ} Γ',
307 -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
309 unfold HaskCoVar in *.
310 intros; apply (X TV CV).
311 apply ilist_chop' in env; auto.
312 unfold InstantiatedCoercionEnv in *.
313 unfold weakCK'' in cenv.
315 rewrite <- map_preserves_length in cenv.
317 rewrite <- map_preserves_length in cenv.
321 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
323 {| sacpj_sac := mkStrongAltCon
324 ; sacpj_φ := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
326 fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
330 unfold HaskCoVar in *.
335 unfold InstantiatedCoercionEnv in *.
336 apply vec_chop' in cenv.
340 Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
351 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc).
353 set (c:DataCon _) as dc.
354 set ((dataConTyCon c):TyCon) as tc' in *.
355 set (eqd_dec tc tc') as eqpf; destruct eqpf;
357 | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++(dc:CoreDataCon))) ]; subst.
359 eapply mkStrongAltConPlusJunk.
363 apply OK; refine {| sacpj_sac := {|
364 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
365 ; sac_altcon := WeakLitAlt h
367 intro; intro φ; apply φ.
368 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
369 rewrite weakCK'_nil_inert. apply ψ.
370 apply OK; refine {| sacpj_sac := {|
371 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
372 ; sac_altcon := WeakDEFAULT |} |}.
373 intro; intro φ; apply φ.
374 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
375 rewrite weakCK'_nil_inert. apply ψ.
378 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
379 fun wev => match wev with weakExprVar _ t => t end.
380 Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
382 Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
384 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
385 WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
392 inversion cenv; auto.
395 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
396 Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
397 : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
398 apply (addErrorMessage ("castExpr " +++ err_msg)).
401 destruct τ' as [τ' l'].
402 destruct (eqd_dec l l'); [ idtac
403 | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
404 " got: " +++(fold_left (fun x y => y+++","+++y) (map haskTyVarToType l) "")+++eol+++
405 " wanted: "+++(fold_left (fun x y => x+++","+++y) (map haskTyVarToType l') "")
407 destruct (eqd_dec τ τ'); [ idtac
408 | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
409 " got: " +++τ+++eol+++
417 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
418 match wcv with weakCoerVar _ κ _ _ => κ end.
419 Coercion coVarKind : WeakCoerVar >-> Kind.
421 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
423 set (weakTypeToType φ t) as wt.
424 destruct wt; try apply (Error error_message).
426 matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in ").
432 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
435 | T_Leaf (Some (wev,e)) => match weakTypeToTypeOfKind φ wev ★ with
436 | OK t' => [((wev:CoreVar),t')]
439 | T_Branch b1 b2 => (varsTypes b1 φ),,(varsTypes b2 φ)
442 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
443 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
444 | nil => match wtl with
446 | _ => Error "length mismatch in mkAvars"
448 | k::lk' => match wtl with
449 | nil => Error "length mismatch in mkAvars"
451 weakTypeToTypeOfKind φ wt k >>= fun t =>
452 mkAvars wtl' lk' φ >>= fun rest =>
453 OK (ICons _ _ t rest)
457 Definition weakExprToStrongExpr : forall
461 (ψ:CoVarResolver Γ Δ)
462 (ξ:CoreVar -> LeveledHaskType Γ ★)
465 WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
467 fix weakExprToStrongExpr
471 (ψ:CoVarResolver Γ Δ)
472 (ξ:CoreVar -> LeveledHaskType Γ ★)
475 (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
476 addErrorMessage ("in weakExprToStrongExpr " +++ we)
479 | WEVar v => castExpr we ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
481 | WELit lit => castExpr we ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
483 | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
484 weakTypeOfWeakExpr ebody >>= fun tbody =>
485 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
486 let ξ' := update_ξ ξ (((ev:CoreVar),tv@@lev)::nil) in
487 weakExprToStrongExpr Γ Δ φ ψ ξ' tbody' lev ebody >>= fun ebody' =>
488 castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
490 | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' =>
491 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
492 weakExprToStrongExpr Γ Δ φ ψ ξ tbody' ((ec')::lev) e >>= fun e' =>
493 castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
495 | WEEsc _ ec e tbody => φ ec >>= fun ec'' =>
496 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
498 | nil => Error "ill-leveled escapification"
499 | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ ec' |- tbody' ]>) lev' e
500 >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
503 | WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage"
505 | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
507 | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>
508 weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
509 weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) τ lev ebody
511 OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
513 | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
514 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
515 weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' =>
516 weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' =>
517 OK (EApp _ _ _ _ _ _ e1' e2')
519 | WETyLam tv e => let φ' := upφ tv φ in
520 weakTypeOfWeakExpr e >>= fun te =>
521 weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
522 weakExprToStrongExpr _ (weakCE Δ) φ'
523 (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) τ' (weakL lev) e
525 castExpr we "WETyLam1" _ e' >>= fun e'' =>
526 castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e'')
528 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
530 | WForAllTy wtv te' =>
531 let φ' := upφ wtv φ in
532 weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>
533 weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' =>
534 weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
535 castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
536 | _ => Error ("weakTypeToType: WETyApp body with type "+++te)
539 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
541 | WCoFunTy t1 t2 t3 =>
542 weakTypeToType φ t1 >>= fun t1' =>
544 haskTypeOfSomeKind κ t1'' =>
545 weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
546 weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
547 weakExprToStrongExpr Γ Δ φ ψ ξ (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
548 castExpr we "WECoApp" _ e' >>= fun e'' =>
549 OK (ECoApp Γ Δ κ t1'' t2''
550 (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
552 | _ => Error ("weakTypeToType: WECoApp body with type "+++te)
555 | WECoLam cv e => let (_,_,t1,t2) := cv in
556 weakTypeOfWeakExpr e >>= fun te =>
557 weakTypeToTypeOfKind φ te ★ >>= fun te' =>
558 weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
559 weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
560 weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
561 castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
563 | WECast e co => let (t1,t2) := weakCoercionTypes co in
564 weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
565 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
566 weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>
567 castExpr we "WECast" _
568 (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
571 let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _)
573 (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
574 : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
576 | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
577 | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e)
579 binds b1 >>= fun b1' =>
580 binds b2 >>= fun b2' =>
581 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
583 in binds >>= fun binds' =>
584 weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e >>= fun e' =>
585 OK (ELetRec Γ Δ ξ lev τ _ binds' e')
587 | WECase vscrut ve tbranches tc avars alts =>
588 weakTypeToTypeOfKind φ (vscrut:WeakType) ★ >>= fun tv =>
589 weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
590 let ξ' := update_ξ ξ (((vscrut:CoreVar),tv@@lev)::nil) in
591 mkAvars avars (tyConKind tc) φ >>= fun avars' =>
592 weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' =>
593 (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
594 ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
595 Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ' lev)(weakLT' (tbranches' @@ lev))}) :=
597 | T_Leaf None => OK []
598 | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
599 mkStrongAltConPlusJunk' tc ac >>= fun sac =>
600 list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
602 let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
603 weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
604 (sacpj_ψ sac _ _ avars' ψ)
605 (scbwv_ξ scb ξ' lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
606 let case_case := tt in OK [ _ ]
608 mkTree b1 >>= fun b1' =>
609 mkTree b2 >>= fun b2' =>
611 end) alts >>= fun tree =>
612 castExpr we "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun escrut =>
613 castExpr we "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' escrut tree)
614 >>= fun ecase' => OK (ELet _ _ _ tv _ lev (vscrut:CoreVar) ve' ecase')
621 apply (addErrorMessage "case_some").
623 destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
624 matchThings h (unlev (ξ' wev)) "LetRec".
626 rewrite matchTypeVars_pf.
627 clear matchTypeVars_pf.
628 set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
629 destruct e''; try apply (Error error_message).