1 (*********************************************************************************************************************************)
2 (* HaskStrongToWeak: convert HaskStrong to HaskWeak *)
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.
20 CoInductive Fresh A T :=
21 { next : forall a:A, (T a * Fresh A T)
22 ; split : Fresh A T * Fresh A T
25 Fixpoint rawHaskTypeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)){κ}(rht:RawHaskType (fun _ => WeakTypeVar) κ)
26 {struct rht} : WeakType :=
28 | TVar _ v => WTyVarTy v
29 | TCon tc => WTyCon tc
30 | TCoerc _ t1 t2 t3 => WCoFunTy (rawHaskTypeToWeakType f t1) (rawHaskTypeToWeakType f t2) (rawHaskTypeToWeakType f t3)
32 | TApp _ _ t1 t2 => WAppTy (rawHaskTypeToWeakType f t1) (rawHaskTypeToWeakType f t2)
33 | TAll k rht' => let (tv,f') := next _ _ f k in WForAllTy tv (rawHaskTypeToWeakType f' (rht' tv))
35 match (rawHaskTypeToWeakType f t1) with
36 | WTyVarTy ec => WCodeTy ec (rawHaskTypeToWeakType f t2)
37 | impossible => impossible (* TODO: find a way to convince Coq this can't happen *)
39 | TyFunApp tfc tls => WTyFunApp tfc (rawHaskTypeListToWeakType f tls)
41 with rawHaskTypeListToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)){κ}(rht:RawHaskTypeList κ) :=
44 | TyFunApp_cons κ kl rht' rhtl' => (rawHaskTypeToWeakType f rht')::(rawHaskTypeListToWeakType f rhtl')
47 Definition typeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar))
48 {Γ}{κ}(τ:HaskType Γ κ)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) : WeakType :=
49 rawHaskTypeToWeakType f (τ _ φ).
51 Variable unsafeCoerce : WeakCoercion. Extract Inlined Constant unsafeCoerce => "Coercion.unsafeCoerce".
53 Definition strongCoercionToWeakCoercion {Γ}{Δ}{ck}(τ:HaskCoercion Γ Δ ck)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
55 unfold HaskCoercion in τ.
59 (* This can be used to turn HaskStrong's with arbitrary expression variables into HaskStrong's which use WeakExprVar's
60 * for their variables; those can subsequently be passed to the following function (strongExprToWeakExpr) *)
62 Definition reindexStrongExpr {VV}{HH}{eqVV:EqDecidable VV}{eqHH:EqDecidable HH}
63 {Γ}{Δ}{ξ}{lev}(exp:@Expr VV eqVV Γ Δ ξ lev) : { ξ' : HH -> LeveledHaskType Γ & @Expr HH eqHH Γ Δ ξ' lev }.
67 Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ)
70 Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{lev}
71 (ftv:Fresh Kind (fun _ => WeakTypeVar))
72 (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
73 (exp:@Expr WeakExprVar _ Γ Δ ξ lev)
74 : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> WeakExpr :=
75 match exp as E in Expr G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> WeakExpr with
76 | EVar _ _ _ ev => fun ite => WEVar ev
77 | ELit _ _ _ lit _ => fun ite => WELit lit
78 | EApp Γ' _ _ _ _ _ e1 e2 => fun ite => WEApp (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite)
79 | ELam Γ' _ _ _ _ _ cv e => fun ite => WELam cv (strongExprToWeakExpr ftv fcv e ite)
80 | ELet Γ' _ _ _ _ _ ev e1 e2 => fun ite => WELet ev (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite)
81 | EEsc Γ' _ _ ec t _ e => fun ite => WEEsc (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite)
82 | EBrak Γ' _ _ ec t _ e => fun ite => WEBrak (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite)
83 | ECast Γ Δ ξ t1 t2 γ l e => fun ite => WECast (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)
84 | ENote _ _ _ _ n e => fun ite => WENote n (strongExprToWeakExpr ftv fcv e ite)
85 | ETyApp Γ Δ κ σ τ ξ l e => fun ite => WETyApp (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv τ ite)
86 | ELetRec _ _ _ _ _ vars elrb e =>fun ite=>WELetRec (exprLetRec2WeakExprLetRec ftv fcv elrb ite)(strongExprToWeakExpr ftv fcv e ite)
87 | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => fun ite => WECoApp (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)
88 | ECase Γ Δ ξ l tc tbranches sac atypes e alts =>
90 (strongExprToWeakExpr ftv fcv e ite)
91 (@typeToWeakType ftv Γ _ tbranches ite)
93 (ilist_to_list (@ilmap _ _ (fun _ => WeakType) _ (fun _ t => typeToWeakType ftv t ite) atypes))
95 (tree:Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc sac atypes
97 (sac_Δ scb Γ atypes (weakCK'' Δ))
98 (update_ξ (weakLT'○ξ) (vec2list (vec_map
99 (fun x => ((fst x),(snd x @@ weakL' l))) (scbwv_varstypes scb))))
100 (weakLT' (tbranches@@l)) })
101 : Tree ??(AltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr) :=
104 | T_Leaf (Some x) => let (scb,e) := x in
108 (*map (fun t => typeToWeakType ftv t ite') (vec2list (sac_types scb))*)nil, (* FIXME *)
109 strongExprToWeakExpr ftv fcv e (weakITE' ite))]*) []
110 | T_Branch b1 b2 => (caseBranches b1),,(caseBranches b2)
113 | ETyLam _ _ _ k _ _ e => fun ite =>
114 let (tv,ftv') := next _ _ ftv k in WETyLam tv (strongExprToWeakExpr ftv' fcv e (updateITE tv ite))
115 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => fun ite =>
116 let t1' := typeToWeakType ftv σ₁ ite in
117 let t2' := typeToWeakType ftv σ₂ ite in
118 let (cv,fcv') := next _ _ fcv (t1',t2') in WECoLam cv (strongExprToWeakExpr ftv fcv' e ite)
120 with exprLetRec2WeakExprLetRec {Γ}{Δ}{ξ}{lev}{vars}
121 (ftv:Fresh Kind (fun _ => WeakTypeVar))
122 (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
123 (elrb:@ELetRecBindings WeakExprVar _ Γ Δ ξ lev vars)
124 : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> Tree ??(WeakExprVar * WeakExpr) :=
125 match elrb as E in ELetRecBindings G D X L V
126 return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> Tree ??(WeakExprVar * WeakExpr) with
127 | ELR_nil _ _ _ _ => fun ite => []
128 | ELR_leaf _ _ _ _ cv v e => fun ite => [(v,(strongExprToWeakExpr ftv fcv e ite))]
129 | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv b2 ite)