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 _ ★).
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 Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool :=
464 else update_ig ig vars' v'
467 (* does the specified variable occur free in the expression? *)
468 Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
471 | WEVar cv => if eqd_dec (wev:CoreVar) (cv:CoreVar) then true else false
472 | WECast e co => doesWeakVarOccur wev e
473 | WENote n e => doesWeakVarOccur wev e
474 | WETyApp e t => doesWeakVarOccur wev e
475 | WECoApp e co => doesWeakVarOccur wev e
476 | WEBrak _ ec e _ => doesWeakVarOccur wev e
477 | WEEsc _ ec e _ => doesWeakVarOccur wev e
478 | WECSP _ ec e _ => doesWeakVarOccur wev e
479 | WELet cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
480 | WEApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
481 | WELam cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
482 | WETyLam cv e => doesWeakVarOccur wev e
483 | WECoLam cv e => doesWeakVarOccur wev e
484 | WECase vscrut escrut tbranches tc avars alts =>
485 doesWeakVarOccur wev escrut ||
486 if eqd_dec (wev:CoreVar) (vscrut:CoreVar) then false else
487 ((fix doesWeakVarOccurAlts alts {struct alts} : bool :=
489 | T_Leaf None => false
490 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
491 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
492 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
493 | T_Branch b1 b2 => doesWeakVarOccurAlts b1 || doesWeakVarOccurAlts b2
496 doesWeakVarOccur wev e ||
497 (fix doesWeakVarOccurLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) : bool :=
499 | T_Leaf None => false
500 | T_Leaf (Some (cv,e)) => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
501 | T_Branch b1 b2 => doesWeakVarOccurLetRec b1 || doesWeakVarOccurLetRec b2
504 Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
505 (alts:Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr)) : bool :=
507 | T_Leaf None => false
508 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
509 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
510 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
511 | T_Branch b1 b2 => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
514 (*Definition ensureCaseBindersAreNotUsed (we:WeakExpr) : UniqM WeakExpr := FIXME *)
516 Definition weakExprToStrongExpr : forall
520 (ψ:CoVarResolver Γ Δ)
521 (ξ:CoreVar -> LeveledHaskType Γ ★)
525 WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
527 fix weakExprToStrongExpr
531 (ψ:CoVarResolver Γ Δ)
532 (ξ:CoreVar -> LeveledHaskType Γ ★)
536 (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
537 addErrorMessage ("in weakExprToStrongExpr " +++ we)
541 then OK (EGlobal Γ Δ ξ (τ@@lev) v)
542 else castExpr we ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
544 | WELit lit => castExpr we ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
546 | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
547 weakTypeOfWeakExpr ebody >>= fun tbody =>
548 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
549 let ξ' := update_ξ ξ lev (((ev:CoreVar),tv)::nil) in
550 let ig' := update_ig ig ((ev:CoreVar)::nil) in
551 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>
552 castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
554 | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' =>
555 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
556 weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' =>
557 castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
559 | WEEsc _ ec e tbody => φ ec >>= fun ec'' =>
560 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
562 | nil => Error "ill-leveled escapification"
563 | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
564 >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
567 | WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage"
569 | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
571 | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>
572 weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
573 weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ lev (((v:CoreVar),tv)::nil))
574 (update_ig ig ((v:CoreVar)::nil)) τ lev ebody
576 OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
578 | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
579 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
580 weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' =>
581 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' =>
582 OK (EApp _ _ _ _ _ _ e1' e2')
584 | WETyLam tv e => let φ' := upφ tv φ in
585 weakTypeOfWeakExpr e >>= fun te =>
586 weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
587 weakExprToStrongExpr _ (weakCE Δ) φ'
588 (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
589 >>= fun e' => castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
591 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
593 | WForAllTy wtv te' =>
594 let φ' := upφ wtv φ in
595 weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>
596 weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
597 weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
598 castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
599 | _ => Error ("weakTypeToType: WETyApp body with type "+++te)
602 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
604 | WCoFunTy t1 t2 t3 =>
605 weakTypeToType φ t1 >>= fun t1' =>
607 haskTypeOfSomeKind κ t1'' =>
608 weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
609 weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
610 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
611 castExpr we "WECoApp" _ e' >>= fun e'' =>
612 OK (ECoApp Γ Δ κ t1'' t2''
613 (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
615 | _ => Error ("weakTypeToType: WECoApp body with type "+++te)
618 | WECoLam cv e => let (_,_,t1,t2) := cv in
619 weakTypeOfWeakExpr e >>= fun te =>
620 weakTypeToTypeOfKind φ te ★ >>= fun te' =>
621 weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
622 weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
623 weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ ig te' lev e >>= fun e' =>
624 castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
626 | WECast e co => let (t1,t2) := weakCoercionTypes co in
627 weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
628 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
629 weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
630 castExpr we "WECast" _
631 (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
634 let ξ' := update_ξ ξ lev _ in
635 let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
637 (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
638 : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
640 | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
641 | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e)
643 binds b1 >>= fun b1' =>
644 binds b2 >>= fun b2' =>
645 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
647 in binds >>= fun binds' =>
648 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
649 OK (ELetRec Γ Δ ξ lev τ _ binds' e')
651 | WECase vscrut escrut tbranches tc avars alts =>
652 weakTypeOfWeakExpr escrut >>= fun tscrut =>
653 weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
654 if doesWeakVarOccurAlts vscrut alts
655 then Error "encountered a Case which actually used its binder - these should have been desugared away!!"
656 else mkAvars avars (tyConKind tc) φ >>= fun avars' =>
657 weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' =>
658 (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
659 ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' &
660 Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@ lev))}) :=
662 | T_Leaf None => OK []
663 | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
664 mkStrongAltConPlusJunk' tc ac >>= fun sac =>
665 list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
667 (let case_pf := tt in _) >>= fun pf =>
668 let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
669 weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
670 (sacpj_ψ sac _ _ avars' ψ)
672 (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
673 (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
674 let case_case := tt in OK [ _ ]
676 mkTree b1 >>= fun b1' =>
677 mkTree b2 >>= fun b2' =>
679 end) alts >>= fun tree =>
681 weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
682 castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
683 end)); try clear binds.
686 apply (addErrorMessage "case_some").
688 destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
689 matchThings h (unlev (ξ' wev)) "LetRec".
691 rewrite matchTypeVars_pf.
692 clear matchTypeVars_pf.
693 set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
694 destruct e''; try apply (Error error_message).
699 induction (leaves (varsTypes rb φ)).
706 set (distinct_decidable (vec2list exprvars')) as dec.
707 destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ].