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 HaskStrongTypes.
18 Require Import HaskStrong.
19 Require Import HaskCoreTypes.
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 _
31 else 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 (ψ:WeakCoerVar -> HaskCoVar Γ Δ),
74 (WeakCoerVar -> HaskCoVar _ (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 Γ) :=
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 _
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' => _
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.
152 exact (haskTypeOfSomeKind (fun TV env => TVar (φ v TV env))).
154 destruct case_WAppTy.
155 destruct t1' as [k1' t1'].
156 destruct t2' as [k2' t2'].
158 try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
159 subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
160 apply (Error "Kind mismatch in WAppTy:: ").
162 destruct case_weakTypeListToTypeList.
163 destruct t' as [ k' t' ].
164 matchThings k k' "Kind mismatch in weakTypeListToTypeList".
166 apply (OK (fun TV ite => TyFunApp_cons _ _ (t' TV ite) (rhtl' TV ite))).
168 destruct case_WTyFunApp.
170 eapply haskTypeOfSomeKind.
171 unfold HaskType; intros.
176 destruct case_WTyCon.
178 eapply haskTypeOfSomeKind.
179 unfold HaskType; intros.
182 destruct case_WCodeTy.
184 matchThings κ ★ "Kind mismatch in WCodeTy: ".
186 eapply haskTypeOfSomeKind.
187 unfold HaskType; intros.
189 apply (TVar (φ (@fixkind ★ ec) TV X)).
194 destruct case_WCoFunTy.
195 destruct t1' as [ k1' t1' ].
196 destruct t2' as [ k2' t2' ].
197 destruct t3' as [ k3' t3' ].
198 matchThings k1' k2' "Kind mismatch in arguments of WCoFunTy".
200 matchThings k3' ★ "Kind mismatch in result of WCoFunTy".
203 apply (haskTypeOfSomeKind (t1' ∼∼ t2' ⇒ t3')).
205 destruct case_WForAllTy.
207 matchThings ★ κ "Kind mismatch in WForAllTy: ".
210 apply (@haskTypeOfSomeKind _ ★).
217 (* information about a datacon/literal/default which is common to all instances of a branch with that tag *)
218 Section StrongAltCon.
219 Context (tc : TyCon)(dc:DataCon tc).
221 Definition weakTypeToType' {Γ} : vec (HaskType Γ) tc -> WeakType → HaskType (app (vec2list (dataConExKinds dc)) Γ).
224 set (vec_map (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'.
225 set (@substφ _ _ avars') as q.
226 set (upφ' (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ'.
227 set (@weakTypeToType _ φ' ct) as t.
228 set (@weakT'' _ Γ t) as t'.
229 set (@lamer _ _ _ t') as t''.
230 fold (tyConKinds tc) in t''.
231 fold (dataConExKinds dc) in t''.
232 apply (q (tyConKinds tc)).
234 unfold dataConExKinds.
235 rewrite <- vec2list_map_list2vec.
236 rewrite <- vec2list_map_list2vec.
237 rewrite vec2list_list2vec.
238 rewrite vec2list_list2vec.
242 Definition mkStrongAltCon : @StrongAltCon tc.
244 {| sac_altcon := DataAlt dc
245 ; sac_numCoerVars := length (dataConCoerKinds dc)
246 ; sac_numExprVars := length (dataConFieldTypes dc)
247 ; sac_akinds := tyConKinds tc
248 ; sac_ekinds := dataConExKinds dc
249 ; sac_coercions := fun Γ avars => let case_sac_coercions := tt in _
250 ; sac_types := fun Γ avars => let case_sac_types := tt in _
253 destruct case_sac_coercions.
254 refine (vec_map _ (list2vec (dataConCoerKinds dc))).
257 apply (mkHaskCoercionKind (weakTypeToType' avars w) (weakTypeToType' avars w0)).
259 destruct case_sac_types.
260 refine (vec_map _ (list2vec (dataConFieldTypes dc))).
262 apply (weakTypeToType' avars).
266 Lemma weakCV' : forall {Γ}{Δ} Γ',
268 -> HaskCoVar (app Γ' Γ) (weakCK'' Δ).
270 unfold HaskCoVar in *.
271 intros; apply (X TV CV).
272 apply vec_chop' in env; auto.
273 unfold InstantiatedCoercionEnv in *.
274 unfold weakCK'' in cenv.
277 rewrite <- map_preserves_length in cenv.
281 Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc.
283 {| sacpj_sac := mkStrongAltCon
284 ; sacpj_φ := fun Γ φ => (fun htv => weakV' (φ htv))
285 ; sacpj_ψ := fun Γ Δ avars ψ => (fun htv => _ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) (ψ htv)))
289 unfold HaskCoVar in *.
294 unfold InstantiatedCoercionEnv in *.
295 apply vec_chop' in cenv.
301 Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:AltCon) : ???(@StrongAltConPlusJunk tc).
303 set (c:DataCon _) as dc.
304 set ((dataConTyCon c):TyCon) as tc' in *.
305 set (eqd_dec tc tc') as eqpf; destruct eqpf;
307 | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++dc)) ]; subst.
309 eapply mkStrongAltConPlusJunk.
313 apply OK; refine {| sacpj_sac := {| sac_akinds := tyConKinds tc
314 ; sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
315 ; sac_altcon := LitAlt h
317 intro; intro φ; apply φ.
318 intro; intro; intro; intro ψ; apply ψ.
319 apply OK; refine {| sacpj_sac := {| sac_akinds := tyConKinds tc
320 ; sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil
321 ; sac_altcon := DEFAULT |} |}.
322 intro; intro φ; apply φ.
323 intro; intro; intro; intro ψ; apply ψ.
325 Fixpoint mLetRecTypesVars {Γ} (mlr:Tree ??(WeakExprVar * WeakExpr)) φ : Tree ??(WeakExprVar * HaskType Γ ★) :=
328 | T_Leaf (Some ((weakExprVar v t),e)) => [((weakExprVar v t),weakTypeToType φ t)]
329 | T_Branch b1 b2 => ((mLetRecTypesVars b1 φ),,(mLetRecTypesVars b2 φ))
334 Definition weakExprVarToWeakType : WeakExprVar -> WeakType :=
335 fun wev => match wev with weakExprVar _ t => t end.
336 Coercion weakExprVarToWeakType : WeakExprVar >-> WeakType.
338 (*Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ.*)
340 Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> HaskCoVar Γ Δ) :
341 WeakCoerVar -> HaskCoVar Γ (κ::Δ).
345 apply (ψ X TV CV env).
346 inversion cenv; auto.
349 (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *)
350 Definition castExpr (err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
351 : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ').
354 destruct τ' as [τ' l'].
355 destruct (eqd_dec l l'); [ idtac | apply (Error ("level mismatch in castExpr: "+++err_msg)) ].
356 destruct (eqd_dec τ τ'); [ idtac | apply (Error ("type mismatch in castExpr: " +++err_msg+++" "+++τ+++" and "+++τ')) ].
362 Definition weakTypeToType' : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) κ, ???(HaskType Γ κ).
364 set (weakTypeToType φ t) as wt.
365 destruct wt; try apply (Error error_message).
367 matchThings κ κ0 "Kind mismatch in weakTypeToType': ".
373 Definition weakExprToStrongExpr : forall
377 (ψ:CoVarResolver Γ Δ)
378 (ξ:CoreVar -> LeveledHaskType Γ ★)
381 WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ).
383 fix weakExprToStrongExpr
387 (ψ:CoVarResolver Γ Δ)
388 (ξ:CoreVar -> LeveledHaskType Γ ★)
391 (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
394 | WEVar v => castExpr "WEVar" (τ @@ lev) (EVar Γ Δ ξ v)
396 | WELit lit => castExpr "WELit" (τ @@ lev) (ELit Γ Δ ξ lit lev)
398 | WELam ev e => weakTypeToType' φ ev ★ >>= fun tv =>
399 weakTypeOfWeakExpr e >>= fun t =>
400 weakTypeToType' φ t ★ >>= fun τ' =>
401 weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((ev:CoreVar),tv@@lev)::nil))
403 castExpr "WELam" _ (ELam Γ Δ ξ tv _ _ ev e')
405 | WEBrak ec e tbody => weakExprToStrongExpr Γ Δ φ ψ ξ τ ((φ (`ec))::lev) e >>= fun e' =>
406 castExpr "WEBrak" _ (EBrak _ _ _ (φ (`ec)) _ lev e')
408 | WEEsc ec e tbody => weakTypeToType' φ tbody ★ >>= fun tbody' =>
410 | nil => Error "ill-leveled escapification"
411 | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ φ (`ec) |- tbody' ]>) lev e
413 castExpr "WEEsc" (τ@@lev) (EEsc _ _ _ (φ (`ec)) _ lev e')
415 | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
417 | WELet v ve ebody => weakTypeToType' φ v ★ >>= fun tv =>
418 weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' =>
419 weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) τ lev ebody
421 OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody')
423 | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 =>
424 weakTypeToType' φ t2 ★ >>= fun t2' =>
425 weakExprToStrongExpr Γ Δ φ ψ ξ t2' lev e2 >>= fun e2' =>
426 weakExprToStrongExpr Γ Δ φ ψ ξ (t2'--->τ) lev e1 >>= fun e1' =>
427 OK (EApp _ _ _ _ _ _ e1' e2')
429 | WETyLam tv e => let φ' := upφ tv φ in
430 weakTypeOfWeakExpr e >>= fun te =>
431 weakTypeToType' φ' te ★ >>= fun τ' =>
432 weakExprToStrongExpr _ (weakCE Δ) φ' (weakCV○ψ) (weakLT○ξ) τ' (weakL lev) e
434 castExpr "WETyLam1" _ e' >>= fun e'' =>
435 castExpr "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e'')
437 | WETyApp e t => weakTypeOfWeakExpr e >>= fun te =>
439 | WForAllTy wtv te' =>
440 let φ' := upφ wtv φ in
441 weakTypeToType' φ' te' ★ >>= fun te'' =>
442 weakExprToStrongExpr Γ Δ φ ψ ξ (mkTAll te'') lev e >>= fun e' =>
443 weakTypeToType' φ t wtv >>= fun t' =>
444 castExpr "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
445 | _ => Error ("weakTypeToType: WETyApp body with type "+++te)
448 (* I had all of these working before I switched to a Kind-indexed representation for types; it will take a day or two
449 * to get them back working again *)
450 | WECoApp e t => Error "weakExprToStrongExpr: WECoApp not yet implemented"
451 | WECoLam cv e => Error "weakExprToStrongExpr: WECoLam not yet implemented"
452 | WECast e co => Error "weakExprToStrongExpr: WECast not yet implemented"
453 | WELetRec rb e => Error "weakExprToStrongExpr: WELetRec not yet implemented"
454 | WECase e tbranches tc avars alts => Error "weakExprToStrongExpr: WECase not yet implemented"