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 +++ toString T1 +++ " " +++ toString 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 " +++ toString 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.
149 apply ConcatenableString.
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 "+++toString t1'+++" of kind "+++toString k1'+++" to type "+++
161 toString t2'+++" of kind "+++toString k2') as err.
163 try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
164 subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
165 apply (Error ("Kind mismatch in WAppTy: "+++err)).
167 destruct case_weakTypeListToTypeList.
168 apply (addErrorMessage "case_weakTypeListToTypeList").
169 destruct t' as [ k' t' ].
170 matchThings k k' "Kind mismatch in weakTypeListToTypeList".
172 apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
174 destruct case_WTyFunApp.
175 apply (addErrorMessage "case_WTyFunApp").
177 eapply haskTypeOfSomeKind.
178 unfold HaskType; intros.
183 destruct case_WTyCon.
184 apply (addErrorMessage "case_WTyCon").
186 eapply haskTypeOfSomeKind.
187 unfold HaskType; intros.
190 destruct case_WCodeTy.
191 apply (addErrorMessage "case_WCodeTy").
193 matchThings κ ★ "Kind mismatch in WCodeTy: ".
195 eapply haskTypeOfSomeKind.
196 unfold HaskType; intros.
198 apply (TVar (ec' TV X)).
203 destruct case_WCoFunTy.
204 apply (addErrorMessage "case_WCoFunTy").
205 destruct t1' as [ k1' t1' ].
206 destruct t2' as [ k2' t2' ].
207 destruct t3' as [ k3' t3' ].
208 matchThings k1' k2' "Kind mismatch in arguments of WCoFunTy".
210 matchThings k3' ★ "Kind mismatch in result of WCoFunTy".
213 apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
215 destruct case_WForAllTy.
216 apply (addErrorMessage "case_WForAllTy").
218 matchThings ★ κ "Kind mismatch in WForAllTy: ".
221 apply (@haskTypeOfSomeKind _ ★).
226 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
227 Section StrongAltCon.
228 Context (tc : TyCon)(dc:DataCon tc).
230 Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
231 -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
234 apply (addErrorMessage "weakTypeToType'").
235 set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
236 set (@substφ _ _ avars') as q.
237 set (upφ' (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ'.
238 set (@weakTypeToType _ φ' ct) as t.
239 destruct t as [|t]; try apply (Error error_message).
240 destruct t as [tk t].
241 matchThings tk ★ "weakTypeToType'".
244 set (@weakT'' _ Γ _ t) as t'.
245 set (@lamer _ _ _ _ t') as t''.
246 fold (tyConKinds tc) in t''.
247 fold (dataConExKinds dc) in t''.
251 unfold dataConExKinds.
252 rewrite <- vec2list_map_list2vec.
253 rewrite <- vec2list_map_list2vec.
254 rewrite vec2list_list2vec.
255 rewrite vec2list_list2vec.
259 Definition mkStrongAltCon : @StrongAltCon tc.
261 {| sac_altcon := WeakDataAlt dc
262 ; sac_numCoerVars := length (dataConCoerKinds dc)
263 ; sac_numExprVars := length (dataConFieldTypes dc)
264 ; sac_ekinds := dataConExKinds dc
265 ; sac_coercions := fun Γ avars => let case_sac_coercions := tt in _
266 ; sac_types := fun Γ avars => let case_sac_types := tt in _
269 destruct case_sac_coercions.
270 refine (vec_map _ (list2vec (dataConCoerKinds dc))).
273 unfold tyConKind in avars.
274 set (@weakTypeToType' Γ) as q.
275 unfold tyConKinds in q.
276 rewrite <- vec2list_map_list2vec in q.
277 rewrite vec2list_list2vec in q.
280 q avars w >>= fun t1 =>
281 q avars w0 >>= fun t2 =>
282 OK (mkHaskCoercionKind t1 t2)
284 | Error s => Prelude_error s
288 destruct case_sac_types.
289 refine (vec_map _ (list2vec (dataConFieldTypes dc))).
291 unfold tyConKind in avars.
292 set (@weakTypeToType' Γ) as q.
293 unfold tyConKinds in q.
294 rewrite <- vec2list_map_list2vec in q.
295 rewrite vec2list_list2vec in q.
296 set (q avars X) as y.
298 | Error s =>Prelude_error s
304 Lemma weakCV' : forall {Γ}{Δ} Γ',
306 -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
308 unfold HaskCoVar in *.
309 intros; apply (X TV CV).
310 apply ilist_chop' in env; auto.
311 unfold InstantiatedCoercionEnv in *.
312 unfold weakCK'' in cenv.
314 rewrite <- map_preserves_length in cenv.
316 rewrite <- map_preserves_length in cenv.
320 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
322 {| sacpj_sac := mkStrongAltCon
323 ; sacpj_φ := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
325 fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
329 unfold HaskCoVar in *.
334 unfold InstantiatedCoercionEnv in *.
335 apply vec_chop' in cenv.
339 Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
350 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc).
352 set (c:DataCon _) as dc.
353 set ((dataConTyCon c):TyCon) as tc' in *.
354 set (eqd_dec tc tc') as eqpf; destruct eqpf;
356 | apply (Error ("in a case of tycon "+++toString tc+++", found a branch with datacon "+++toString (dc:CoreDataCon))) ]; subst.
358 eapply mkStrongAltConPlusJunk.
362 apply OK; refine {| sacpj_sac := {|
363 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
364 ; sac_altcon := WeakLitAlt h
366 intro; intro φ; apply φ.
367 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
368 rewrite weakCK'_nil_inert. apply ψ.
369 apply OK; refine {| sacpj_sac := {|
370 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
371 ; sac_altcon := WeakDEFAULT |} |}.
372 intro; intro φ; apply φ.
373 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
374 rewrite weakCK'_nil_inert. apply ψ.
377 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
378 fun wev => match wev with weakExprVar _ t => t end.
379 Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
381 Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
383 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
384 WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
391 inversion cenv; auto.
394 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
395 Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
396 : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
397 apply (addErrorMessage ("castExpr " +++ err_msg)).
400 destruct τ' as [τ' l'].
401 destruct (eqd_dec l l'); [ idtac
402 | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
403 " got: " +++(fold_left (fun x y => y+++","+++y) (map (toString ○ haskTyVarToType) l) "")+++eol+++
404 " wanted: "+++(fold_left (fun x y => x+++","+++y) (map (toString ○ haskTyVarToType) l') "")
406 destruct (eqd_dec τ τ'); [ idtac
407 | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
408 " got: " +++toString τ+++eol+++
409 " wanted: "+++toString τ'
416 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
417 match wcv with weakCoerVar _ κ _ _ => κ end.
418 Coercion coVarKind : WeakCoerVar >-> Kind.
420 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
422 set (weakTypeToType φ t) as wt.
423 destruct wt; try apply (Error error_message).
425 matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in ").
431 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
434 | T_Leaf (Some (wev,e)) => match weakTypeToTypeOfKind φ wev ★ with
435 | OK t' => [((wev:CoreVar),t')]
438 | T_Branch b1 b2 => (varsTypes b1 φ),,(varsTypes b2 φ)
441 Fixpoint mkAvars {Γ}(wtl:list WeakType)(lk:list Kind)(φ:TyVarResolver Γ) : ???(IList Kind (HaskType Γ) lk) :=
442 match lk as LK return ???(IList Kind (HaskType Γ) LK) with
443 | nil => match wtl with
445 | _ => Error "length mismatch in mkAvars"
447 | k::lk' => match wtl with
448 | nil => Error "length mismatch in mkAvars"
450 weakTypeToTypeOfKind φ wt k >>= fun t =>
451 mkAvars wtl' lk' φ >>= fun rest =>
452 OK (ICons _ _ t rest)
456 Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool :=
463 else update_ig ig vars' v'
466 (* does the specified variable occur free in the expression? *)
467 Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
470 | WEVar cv => if eqd_dec (wev:CoreVar) (cv:CoreVar) then true else false
471 | WECast e co => doesWeakVarOccur wev e
472 | WENote n e => doesWeakVarOccur wev e
473 | WETyApp e t => doesWeakVarOccur wev e
474 | WECoApp e co => doesWeakVarOccur wev e
475 | WEBrak _ ec e _ => doesWeakVarOccur wev e
476 | WEEsc _ ec e _ => doesWeakVarOccur wev e
477 | WECSP _ ec e _ => doesWeakVarOccur wev e
478 | WELet cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
479 | WEApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
480 | WELam cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
481 | WETyLam cv e => doesWeakVarOccur wev e
482 | WECoLam cv e => doesWeakVarOccur wev e
483 | WECase vscrut escrut tbranches tc avars alts =>
484 doesWeakVarOccur wev escrut ||
485 if eqd_dec (wev:CoreVar) (vscrut:CoreVar) then false else
486 ((fix doesWeakVarOccurAlts alts {struct alts} : bool :=
488 | T_Leaf None => false
489 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
490 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
491 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
492 | T_Branch b1 b2 => doesWeakVarOccurAlts b1 || doesWeakVarOccurAlts b2
495 doesWeakVarOccur wev e ||
496 (fix doesWeakVarOccurLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) : bool :=
498 | T_Leaf None => false
499 | T_Leaf (Some (cv,e)) => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
500 | T_Branch b1 b2 => doesWeakVarOccurLetRec b1 || doesWeakVarOccurLetRec b2
503 Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
504 (alts:Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr)) : bool :=
506 | T_Leaf None => false
507 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
508 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
509 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
510 | T_Branch b1 b2 => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
513 (*Definition ensureCaseBindersAreNotUsed (we:WeakExpr) : UniqM WeakExpr := FIXME *)
515 Definition weakExprToStrongExpr : forall
519 (ψ:CoVarResolver Γ Δ)
520 (ξ:CoreVar -> LeveledHaskType Γ ★)
524 WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
526 fix weakExprToStrongExpr
530 (ψ:CoVarResolver Γ Δ)
531 (ξ:CoreVar -> LeveledHaskType Γ ★)
535 (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
536 addErrorMessage ("in weakExprToStrongExpr " +++ toString we)
540 then OK (EGlobal Γ Δ ξ (τ@@lev) v)
541 else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
543 | WELit lit => castExpr we ("WELit "+++toString lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
545 | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
546 weakTypeOfWeakExpr ebody >>= fun tbody =>
547 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
548 let ξ' := update_ξ ξ lev (((ev:CoreVar),tv)::nil) in
549 let ig' := update_ig ig ((ev:CoreVar)::nil) in
550 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>
551 castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
553 | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' =>
554 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
555 weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' =>
556 castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
558 | WEEsc _ ec e tbody => φ ec >>= fun ec'' =>
559 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
561 | nil => Error "ill-leveled escapification"
562 | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
563 >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
566 | WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage"
568 | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
570 | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>
571 weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
572 weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ lev (((v:CoreVar),tv)::nil))
573 (update_ig ig ((v:CoreVar)::nil)) τ lev ebody
575 OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
577 | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
578 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
579 weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' =>
580 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' =>
581 OK (EApp _ _ _ _ _ _ e1' e2')
583 | WETyLam tv e => let φ' := upφ tv φ in
584 weakTypeOfWeakExpr e >>= fun te =>
585 weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
586 weakExprToStrongExpr _ (weakCE Δ) φ'
587 (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
588 >>= fun e' => castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
590 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
592 | WForAllTy wtv te' =>
593 let φ' := upφ wtv φ in
594 weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>
595 weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
596 weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
597 castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
598 | _ => Error ("weakTypeToType: WETyApp body with type "+++toString te)
601 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
603 | WCoFunTy t1 t2 t3 =>
604 weakTypeToType φ t1 >>= fun t1' =>
606 haskTypeOfSomeKind κ t1'' =>
607 weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
608 weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
609 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
610 castExpr we "WECoApp" _ e' >>= fun e'' =>
611 OK (ECoApp Γ Δ κ t1'' t2''
612 (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
614 | _ => Error ("weakTypeToType: WECoApp body with type "+++toString te)
617 | WECoLam cv e => let (_,_,t1,t2) := cv in
618 weakTypeOfWeakExpr e >>= fun te =>
619 weakTypeToTypeOfKind φ te ★ >>= fun te' =>
620 weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
621 weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
622 weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ ig te' lev e >>= fun e' =>
623 castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
625 | WECast e co => let (t1,t2) := weakCoercionTypes co in
626 weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
627 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
628 weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
629 castExpr we "WECast" _
630 (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
633 let ξ' := update_ξ ξ lev _ in
634 let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
636 (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
637 : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
639 | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
640 | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e)
642 binds b1 >>= fun b1' =>
643 binds b2 >>= fun b2' =>
644 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
646 in binds >>= fun binds' =>
647 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
648 OK (ELetRec Γ Δ ξ lev τ _ binds' e')
650 | WECase vscrut escrut tbranches tc avars alts =>
651 weakTypeOfWeakExpr escrut >>= fun tscrut =>
652 weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
653 if doesWeakVarOccurAlts vscrut alts
654 then Error "encountered a Case which actually used its binder - these should have been desugared away!!"
655 else mkAvars avars (tyConKind tc) φ >>= fun avars' =>
656 weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' =>
657 (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
658 ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac &
659 Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@ lev))}}) :=
661 | T_Leaf None => OK []
662 | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
663 mkStrongAltConPlusJunk' tc ac >>= fun sac =>
664 list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
666 (let case_pf := tt in _) >>= fun pf =>
667 let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
668 weakExprToStrongExpr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
669 (sacpj_ψ sac _ _ avars' ψ)
671 (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
672 (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
673 let case_case := tt in OK [ _ ]
675 mkTree b1 >>= fun b1' =>
676 mkTree b2 >>= fun b2' =>
678 end) alts >>= fun tree =>
680 weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
681 castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
682 end)); try clear binds; try apply ConcatenableString.
685 apply (addErrorMessage "case_some").
687 destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
688 matchThings h (unlev (ξ' wev)) "LetRec".
690 rewrite matchTypeVars_pf.
691 clear matchTypeVars_pf.
692 set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
693 destruct e''; try apply (Error error_message).
698 induction (leaves (varsTypes rb φ)).
705 set (distinct_decidable (vec2list exprvars')) as dec.
706 destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ].