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 +++ toString T1 +++ " " +++ toString 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 " +++ toString 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.
152 apply ConcatenableString.
154 destruct case_WTyVarTy.
155 apply (addErrorMessage "case_WTyVarTy").
157 exact (haskTypeOfSomeKind (fun TV env => TVar (v' TV env))).
159 destruct case_WAppTy.
160 apply (addErrorMessage "case_WAppTy").
161 destruct t1' as [k1' t1'].
162 destruct t2' as [k2' t2'].
163 set ("tried to apply type "+++toString t1'+++" of kind "+++toString k1'+++" to type "+++
164 toString t2'+++" of kind "+++toString k2') as err.
166 try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
167 subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
168 apply (Error ("Kind mismatch in WAppTy: "+++err)).
170 destruct case_weakTypeListToTypeList.
171 apply (addErrorMessage "case_weakTypeListToTypeList").
172 destruct t' as [ k' t' ].
173 matchThings k k' "Kind mismatch in weakTypeListToTypeList".
175 apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
177 destruct case_WTyFunApp.
178 apply (addErrorMessage "case_WTyFunApp").
180 eapply haskTypeOfSomeKind.
181 unfold HaskType; intros.
186 destruct case_WTyCon.
187 apply (addErrorMessage "case_WTyCon").
189 eapply haskTypeOfSomeKind.
190 unfold HaskType; intros.
193 destruct case_WCodeTy.
194 apply (addErrorMessage "case_WCodeTy").
196 matchThings κ ★ "Kind mismatch in WCodeTy: ".
198 eapply haskTypeOfSomeKind.
199 unfold HaskType; intros.
201 apply (TVar (ec' TV X)).
206 destruct case_WCoFunTy.
207 apply (addErrorMessage "case_WCoFunTy").
208 destruct t1' as [ k1' t1' ].
209 destruct t2' as [ k2' t2' ].
210 destruct t3' as [ k3' t3' ].
211 matchThings k1' k2' "Kind mismatch in arguments of WCoFunTy".
213 matchThings k3' ★ "Kind mismatch in result of WCoFunTy".
216 apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
218 destruct case_WForAllTy.
219 apply (addErrorMessage "case_WForAllTy").
221 matchThings ★ κ "Kind mismatch in WForAllTy: ".
224 apply (@haskTypeOfSomeKind _ ★).
229 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
230 Section StrongAltCon.
231 Context (tc : TyCon)(dc:DataCon tc).
233 Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds tc))
234 -> WeakType → ???(HaskType (app (vec2list (dataConExKinds dc)) Γ) ★).
237 apply (addErrorMessage "weakTypeToType'").
238 set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
239 set (@substφ _ _ avars') as q.
240 set (upφ' (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ'.
241 set (@weakTypeToType _ φ' ct) as t.
242 destruct t as [|t]; try apply (Error error_message).
243 destruct t as [tk t].
244 matchThings tk ★ "weakTypeToType'".
247 set (@weakT'' _ Γ _ t) as t'.
248 set (@lamer _ _ _ _ t') as t''.
249 fold (tyConKinds tc) in t''.
250 fold (dataConExKinds dc) in t''.
254 unfold dataConExKinds.
255 rewrite <- vec2list_map_list2vec.
256 rewrite <- vec2list_map_list2vec.
257 rewrite vec2list_list2vec.
258 rewrite vec2list_list2vec.
262 Definition mkStrongAltCon : @StrongAltCon tc.
264 {| sac_altcon := WeakDataAlt dc
265 ; sac_numCoerVars := length (dataConCoerKinds dc)
266 ; sac_numExprVars := length (dataConFieldTypes dc)
267 ; sac_ekinds := dataConExKinds dc
268 ; sac_coercions := fun Γ avars => let case_sac_coercions := tt in _
269 ; sac_types := fun Γ avars => let case_sac_types := tt in _
272 destruct case_sac_coercions.
273 refine (vec_map _ (list2vec (dataConCoerKinds dc))).
276 unfold tyConKind in avars.
277 set (@weakTypeToType' Γ) as q.
278 unfold tyConKinds in q.
279 rewrite <- vec2list_map_list2vec in q.
280 rewrite vec2list_list2vec in q.
283 q avars w >>= fun t1 =>
284 q avars w0 >>= fun t2 =>
285 OK (mkHaskCoercionKind t1 t2)
287 | Error s => Prelude_error s
291 destruct case_sac_types.
292 refine (vec_map _ (list2vec (dataConFieldTypes dc))).
294 unfold tyConKind in avars.
295 set (@weakTypeToType' Γ) as q.
296 unfold tyConKinds in q.
297 rewrite <- vec2list_map_list2vec in q.
298 rewrite vec2list_list2vec in q.
299 set (q avars X) as y.
301 | Error s =>Prelude_error s
307 Lemma weakCV' : forall {Γ}{Δ} Γ',
309 -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
311 unfold HaskCoVar in *.
312 intros; apply (X TV CV).
313 apply ilist_chop' in env; auto.
314 unfold InstantiatedCoercionEnv in *.
315 unfold weakCK'' in cenv.
317 rewrite <- map_preserves_length in cenv.
319 rewrite <- map_preserves_length in cenv.
323 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
325 {| sacpj_sac := mkStrongAltCon
326 ; sacpj_φ := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv'))
328 fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv')))
332 unfold HaskCoVar in *.
337 unfold InstantiatedCoercionEnv in *.
338 apply vec_chop' in cenv.
342 Lemma weakCK'_nil_inert : forall Γ Δ, (@weakCK'' Γ (@nil Kind)) Δ = Δ.
353 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAltConPlusJunk tc).
355 set (c:DataCon _) as dc.
356 set ((dataConTyCon c):TyCon) as tc' in *.
357 set (eqd_dec tc tc') as eqpf; destruct eqpf;
359 | apply (Error ("in a case of tycon "+++toString tc+++", found a branch with datacon "+++toString (dc:CoreDataCon))) ]; subst.
361 eapply mkStrongAltConPlusJunk.
365 apply OK; refine {| sacpj_sac := {|
366 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
367 ; sac_altcon := WeakLitAlt h
369 intro; intro φ; apply φ.
370 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
371 rewrite weakCK'_nil_inert. apply ψ.
372 apply OK; refine {| sacpj_sac := {|
373 sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
374 ; sac_altcon := WeakDEFAULT |} |}.
375 intro; intro φ; apply φ.
376 intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl.
377 rewrite weakCK'_nil_inert. apply ψ.
380 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
381 fun wev => match wev with weakExprVar _ t => t end.
382 Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
384 Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.
386 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) :
387 WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)).
394 inversion cenv; auto.
397 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
398 Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
399 : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
400 apply (addErrorMessage ("castExpr " +++ err_msg)).
403 destruct τ' as [τ' l'].
404 destruct (eqd_dec l l'); [ idtac
405 | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
406 " got: " +++(fold_left (fun x y => y+++","+++y) (map (toString ○ haskTyVarToType) l) "")+++eol+++
407 " wanted: "+++(fold_left (fun x y => x+++","+++y) (map (toString ○ haskTyVarToType) l') "")
409 destruct (eqd_dec τ τ'); [ idtac
410 | apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
411 " got: " +++toString τ+++eol+++
412 " wanted: "+++toString τ'
419 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
420 match wcv with weakCoerVar _ κ _ _ => κ end.
421 Coercion coVarKind : WeakCoerVar >-> Kind.
423 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
425 set (weakTypeToType φ t) as wt.
426 destruct wt; try apply (Error error_message).
428 matchThings κ κ0 ("Kind mismatch in weakTypeToTypeOfKind in ").
434 Fixpoint varsTypes {Γ}(t:Tree ??(WeakExprVar * WeakExpr))(φ:TyVarResolver Γ) : Tree ??(CoreVar * HaskType Γ ★) :=
437 | T_Leaf (Some (wev,e)) => match weakTypeToTypeOfKind φ wev ★ with
438 | OK t' => [((wev:CoreVar),t')]
441 | 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 weakTypeToTypeOfKind φ wt k >>= fun t =>
454 mkAvars wtl' lk' φ >>= fun rest =>
455 OK (ICons _ _ t rest)
459 Fixpoint update_ig (ig:CoreVar -> bool) (vars:list CoreVar) : CoreVar -> bool :=
466 else update_ig ig vars' v'
469 (* does the specified variable occur free in the expression? *)
470 Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
473 | WEVar cv => if eqd_dec (wev:CoreVar) (cv:CoreVar) then true else false
474 | WECast e co => doesWeakVarOccur wev e
475 | WENote n e => doesWeakVarOccur wev e
476 | WETyApp e t => doesWeakVarOccur wev e
477 | WECoApp e co => doesWeakVarOccur wev e
478 | WEBrak _ ec e _ => doesWeakVarOccur wev e
479 | WEEsc _ ec e _ => doesWeakVarOccur wev e
480 | WECSP _ ec e _ => doesWeakVarOccur wev e
481 | WELet cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
482 | WEApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
483 | WELam cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
484 | WETyLam cv e => doesWeakVarOccur wev e
485 | WECoLam cv e => doesWeakVarOccur wev e
486 | WECase vscrut escrut tbranches tc avars alts =>
487 doesWeakVarOccur wev escrut ||
488 if eqd_dec (wev:CoreVar) (vscrut:CoreVar) then false else
489 ((fix doesWeakVarOccurAlts alts {struct alts} : bool :=
491 | T_Leaf None => false
492 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
493 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
494 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
495 | T_Branch b1 b2 => doesWeakVarOccurAlts b1 || doesWeakVarOccurAlts b2
498 doesWeakVarOccur wev e ||
499 (fix doesWeakVarOccurLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) : bool :=
501 | T_Leaf None => false
502 | T_Leaf (Some (cv,e)) => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
503 | T_Branch b1 b2 => doesWeakVarOccurLetRec b1 || doesWeakVarOccurLetRec b2
506 Fixpoint doesWeakVarOccurAlts (wev:WeakExprVar)
507 (alts:Tree ??(WeakAltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr)) : bool :=
509 | T_Leaf None => false
510 | T_Leaf (Some (WeakDEFAULT,_,_,_,e)) => doesWeakVarOccur wev e
511 | T_Leaf (Some (WeakLitAlt lit,_,_,_,e)) => doesWeakVarOccur wev e
512 | T_Leaf (Some ((WeakDataAlt dc), tvars, cvars, evars,e)) => doesWeakVarOccur wev e (* FIXME!!! *)
513 | T_Branch b1 b2 => doesWeakVarOccurAlts wev b1 || doesWeakVarOccurAlts wev b2
516 (*Definition ensureCaseBindersAreNotUsed (we:WeakExpr) : UniqM WeakExpr := FIXME *)
518 Definition weakExprToStrongExpr : forall
522 (ψ:CoVarResolver Γ Δ)
523 (ξ:CoreVar -> LeveledHaskType Γ ★)
527 WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
529 fix weakExprToStrongExpr
533 (ψ:CoVarResolver Γ Δ)
534 (ξ:CoreVar -> LeveledHaskType Γ ★)
538 (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
539 addErrorMessage ("in weakExprToStrongExpr " +++ toString we)
543 then OK (EGlobal Γ Δ ξ (τ@@lev) v)
544 else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
546 | WELit lit => castExpr we ("WELit "+++toString lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
548 | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
549 weakTypeOfWeakExpr ebody >>= fun tbody =>
550 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
551 let ξ' := update_ξ ξ lev (((ev:CoreVar),tv)::nil) in
552 let ig' := update_ig ig ((ev:CoreVar)::nil) in
553 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' =>
554 castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody')
556 | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' =>
557 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
558 weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' =>
559 castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e')
561 | WEEsc _ ec e tbody => φ ec >>= fun ec'' =>
562 weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' =>
564 | nil => Error "ill-leveled escapification"
565 | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e
566 >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
569 | WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage"
571 | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
573 | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv =>
574 weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' =>
575 weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ lev (((v:CoreVar),tv)::nil))
576 (update_ig ig ((v:CoreVar)::nil)) τ lev ebody
578 OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
580 | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
581 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
582 weakExprToStrongExpr Γ Δ φ ψ ξ ig t2' lev e2 >>= fun e2' =>
583 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' =>
584 OK (EApp _ _ _ _ _ _ e1' e2')
586 | WETyLam tv e => let φ' := upφ tv φ in
587 weakTypeOfWeakExpr e >>= fun te =>
588 weakTypeToTypeOfKind φ' te ★ >>= fun τ' =>
589 weakExprToStrongExpr _ (weakCE Δ) φ'
590 (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
591 >>= fun e' => castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
593 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
595 | WForAllTy wtv te' =>
596 let φ' := upφ wtv φ in
597 weakTypeToTypeOfKind φ' te' ★ >>= fun te'' =>
598 weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
599 weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
600 castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
601 | _ => Error ("weakTypeToType: WETyApp body with type "+++toString te)
604 | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
606 | WCoFunTy t1 t2 t3 =>
607 weakTypeToType φ t1 >>= fun t1' =>
609 haskTypeOfSomeKind κ t1'' =>
610 weakTypeToTypeOfKind φ t2 κ >>= fun t2'' =>
611 weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' =>
612 weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
613 castExpr we "WECoApp" _ e' >>= fun e'' =>
614 OK (ECoApp Γ Δ κ t1'' t2''
615 (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
617 | _ => Error ("weakTypeToType: WECoApp body with type "+++toString te)
620 | WECoLam cv e => let (_,_,t1,t2) := cv in
621 weakTypeOfWeakExpr e >>= fun te =>
622 weakTypeToTypeOfKind φ te ★ >>= fun te' =>
623 weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>
624 weakTypeToTypeOfKind φ t2 cv >>= fun t2' =>
625 weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ ig te' lev e >>= fun e' =>
626 castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
628 | WECast e co => let (t1,t2) := weakCoercionTypes co in
629 weakTypeToTypeOfKind φ t1 ★ >>= fun t1' =>
630 weakTypeToTypeOfKind φ t2 ★ >>= fun t2' =>
631 weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' =>
632 castExpr we "WECast" _
633 (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
636 let ξ' := update_ξ ξ lev _ in
637 let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in
639 (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
640 : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
642 | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
643 | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e)
645 binds b1 >>= fun b1' =>
646 binds b2 >>= fun b2' =>
647 OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
649 in binds >>= fun binds' =>
650 weakExprToStrongExpr Γ Δ φ ψ ξ' ig' τ lev e >>= fun e' =>
651 OK (ELetRec Γ Δ ξ lev τ _ binds' e')
653 | WECase vscrut escrut tbranches tc avars alts =>
654 weakTypeOfWeakExpr escrut >>= fun tscrut =>
655 weakTypeToTypeOfKind φ tscrut ★ >>= fun tscrut' =>
656 if doesWeakVarOccurAlts vscrut alts
657 then Error "encountered a Case which actually used its binder - these should have been desugared away!!"
658 else mkAvars avars (tyConKind tc) φ >>= fun avars' =>
659 weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' =>
660 (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
661 ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac &
662 Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@ lev))}}) :=
664 | T_Leaf None => OK []
665 | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
666 mkStrongAltConPlusJunk' tc ac >>= fun sac =>
667 list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase")
669 (let case_pf := tt in _) >>= fun pf =>
670 let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in
671 weakExprToStrongExpr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ)
672 (sacpj_ψ sac _ _ avars' ψ)
674 (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb))))
675 (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
676 let case_case := tt in OK [ _ ]
678 mkTree b1 >>= fun b1' =>
679 mkTree b2 >>= fun b2' =>
681 end) alts >>= fun tree =>
683 weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
684 castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
685 end)); try clear binds; try apply ConcatenableString.
688 apply (addErrorMessage "case_some").
690 destruct (weakTypeToTypeOfKind φ wev ★); try apply (Error error_message).
691 matchThings h (unlev (ξ' wev)) "LetRec".
693 rewrite matchTypeVars_pf.
694 clear matchTypeVars_pf.
695 set (e' (unlev (ξ' (weakExprVar c w)))) as e''.
696 destruct e''; try apply (Error error_message).
701 induction (leaves (varsTypes rb φ)).
708 set (distinct_decidable (vec2list exprvars')) as dec.
709 destruct dec; [ idtac | apply (Error "malformed HaskWeak: case branch with variables repeated") ].