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 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.
22 Variable UniqSupply : Type. Extract Inlined Constant UniqSupply => "UniqSupply.UniqSupply".
23 Variable Unique : Type. Extract Inlined Constant Unique => "Unique.Unique".
24 Variable uniqFromSupply : UniqSupply -> Unique. Extract Inlined Constant uniqFromSupply => "UniqSupply.uniqFromSupply".
25 Variable splitUniqSupply : UniqSupply -> UniqSupply * UniqSupply.
26 Extract Inlined Constant splitUniqSupply => "UniqSupply.splitUniqSupply".
28 Inductive UniqM {T:Type} : Type :=
29 | uniqM : (UniqSupply -> ???(UniqSupply * T)) -> UniqM.
30 Implicit Arguments UniqM [ ].
32 Instance UniqMonad : Monad UniqM :=
33 { returnM := fun T (x:T) => uniqM (fun u => OK (u,x))
34 ; bindM := fun a b (x:UniqM a) (f:a->UniqM b) =>
40 | OK (u',va) => match f va with
47 Definition getU : UniqM Unique :=
48 uniqM (fun us => let (us1,us2) := splitUniqSupply us in OK (us1,(uniqFromSupply us2))).
50 Notation "'bind' x = e ; f" := (@bindM _ _ _ _ e (fun x => f)) (x ident, at level 60, right associativity).
51 Notation "'return' x" := (returnM x) (at level 100).
52 Notation "'failM' x" := (uniqM (fun _ => Error x)) (at level 100).
54 Section HaskStrongToWeak.
56 Context (hetmet_brak : WeakExprVar).
57 Context (hetmet_esc : WeakExprVar).
59 Context (mkWeakTypeVar_ : Unique -> Kind -> WeakTypeVar).
60 Context (mkWeakCoerVar_ : Unique -> Kind -> WeakType -> WeakType -> WeakCoerVar).
61 Context (mkWeakExprVar_ : Unique -> WeakType -> WeakExprVar).
63 Definition mkWeakTypeVar (k:Kind) : UniqM WeakTypeVar := bind u = getU ; return mkWeakTypeVar_ u k.
64 Definition mkWeakCoerVar (k:Kind)(t1 t2:WeakType) : UniqM WeakCoerVar := bind u = getU ; return mkWeakCoerVar_ u k t1 t2.
65 Definition mkWeakExprVar (t:WeakType) : UniqM WeakExprVar := bind u = getU ; return mkWeakExprVar_ u t.
67 Fixpoint mfresh (lk:list Kind){Γ}(ite:IList _ (fun _ => WeakTypeVar) Γ)
68 : UniqM (((vec WeakTypeVar (length lk)) * (IList _ (fun _ => WeakTypeVar) (app lk Γ)))) :=
69 match lk as LK return UniqM ((vec WeakTypeVar (length LK)) * (IList _ (fun _ => WeakTypeVar) (app LK Γ))) with
70 | nil => return (vec_nil,ite)
71 | k::lk' => bind v = mkWeakTypeVar k
72 ; bind vars_ite' = mfresh lk' ite
73 ; return ((v:::(fst vars_ite')),v::::(snd vars_ite'))
76 Fixpoint rawHaskTypeToWeakType {κ}(rht:RawHaskType (fun _ => WeakTypeVar) κ) {struct rht} : UniqM WeakType :=
78 | TVar _ v => return WTyVarTy v
79 | TCon tc => return WTyCon tc
80 | TCoerc _ t1 t2 t3 => bind t1' = rawHaskTypeToWeakType t1
81 ; bind t2' = rawHaskTypeToWeakType t2
82 ; bind t3' = rawHaskTypeToWeakType t3
83 ; return WCoFunTy t1' t2' t3'
84 | TArrow => return WFunTyCon
85 | TApp _ _ t1 t2 => bind t1' = rawHaskTypeToWeakType t1
86 ; bind t2' = rawHaskTypeToWeakType t2
87 ; return WAppTy t1' t2'
88 | TAll k rht' => bind tv = mkWeakTypeVar k
89 ; bind t' = rawHaskTypeToWeakType (rht' tv)
90 ; return WForAllTy tv t'
91 | TCode t1 t2 => bind t1' = rawHaskTypeToWeakType t1
92 ; bind t2' = rawHaskTypeToWeakType t2
94 | WTyVarTy ec => return WCodeTy ec t2'
95 | _ => failM "impossible"
97 | TyFunApp tfc tls => bind tls' = rawHaskTypeListToWeakType tls
98 ; return WTyFunApp tfc tls'
100 with rawHaskTypeListToWeakType {κ}(rht:RawHaskTypeList κ) : UniqM (list WeakType) :=
102 | TyFunApp_nil => return nil
103 | TyFunApp_cons κ kl rht' rhtl' => bind t = rawHaskTypeToWeakType rht'
104 ; bind tl = rawHaskTypeListToWeakType rhtl'
108 Definition typeToWeakType {Γ}{κ}(τ:HaskType Γ κ)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) : UniqM WeakType :=
109 rawHaskTypeToWeakType (τ _ φ).
111 Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ)
114 Definition coercionToWeakCoercion Γ Δ κ t1 t2 ite (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2))
116 := bind t1' = @typeToWeakType Γ κ t1 ite
117 ; bind t2' = @typeToWeakType Γ κ t2 ite
118 ; return WCoUnsafe t1' t2'.
120 Fixpoint seqM {a}(l:list (UniqM a)) : UniqM (list a) :=
123 | x::y => bind x' = x
128 Context {VV}{eqVV:EqDecidable VV}{toStringVV:ToString VV}.
130 Definition update_χ (χ:VV->???WeakExprVar)(vv:VV)(ev':WeakExprVar) : VV->???WeakExprVar :=
136 Fixpoint update_χ' (χ:VV->???WeakExprVar)(varsexprs:list (VV * WeakExprVar)) : VV->???WeakExprVar :=
139 | (vv,wev)::rest => update_χ (update_χ' χ rest) vv wev
142 Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ)
143 : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ
145 match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with
146 | EVar Γ' _ ξ' ev => fun ite => match χ ev with OK v => return WEVar v | Error s => failM s end
147 | EGlobal Γ' _ ξ' t wev => fun ite => return WEVar wev
148 | ELam Γ' _ _ tv _ _ cv e => fun ite => bind tv' = typeToWeakType tv ite
149 ; bind ev' = mkWeakExprVar tv'
150 ; bind e' = exprToWeakExpr (update_χ χ cv ev') e ite
151 ; return WELam ev' e'
152 | ELet Γ' _ _ t _ _ ev e1 e2 => fun ite => bind tv' = typeToWeakType t ite
153 ; bind e1' = exprToWeakExpr χ e1 ite
154 ; bind ev' = mkWeakExprVar tv'
155 ; bind e2' = exprToWeakExpr (update_χ χ ev ev') e2 ite
156 ; return WELet ev' e1' e2'
157 | ELit _ _ _ lit _ => fun ite => return WELit lit
158 | EApp Γ' _ _ _ _ _ e1 e2 => fun ite => bind e1' = exprToWeakExpr χ e1 ite
159 ; bind e2' = exprToWeakExpr χ e2 ite
160 ; return WEApp e1' e2'
161 | EEsc Γ' _ _ ec t _ e => fun ite => bind t' = typeToWeakType t ite
162 ; bind e' = exprToWeakExpr χ e ite
163 ; return WEEsc hetmet_esc (ec _ ite) e' t'
164 | EBrak Γ' _ _ ec t _ e => fun ite => bind t' = typeToWeakType t ite
165 ; bind e' = exprToWeakExpr χ e ite
166 ; return WEBrak hetmet_brak (ec _ ite) e' t'
167 | ENote _ _ _ _ n e => fun ite => bind e' = exprToWeakExpr χ e ite
169 | ETyApp Γ Δ κ σ τ ξ l e => fun ite => bind t' = typeToWeakType τ ite
170 ; bind e' = exprToWeakExpr χ e ite
171 ; return WETyApp e' t'
172 | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => fun ite => bind e' = exprToWeakExpr χ e ite
173 ; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
174 ; return WECoApp e' c'
175 | ECast Γ Δ ξ t1 t2 γ l e => fun ite => bind e' = exprToWeakExpr χ e ite
176 ; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
177 ; return WECast e' c'
178 | ETyLam _ _ _ k _ _ e => fun ite => bind tv = mkWeakTypeVar k
179 ; bind e' = exprToWeakExpr χ e (updateITE tv ite)
180 ; return WETyLam tv e'
181 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => fun ite => bind t1' = typeToWeakType σ₁ ite
182 ; bind t2' = typeToWeakType σ₂ ite
183 ; bind cv = mkWeakCoerVar κ t1' t2'
184 ; bind e' = exprToWeakExpr χ e ite
185 ; return WECoLam cv e'
186 | ECase Γ Δ ξ l tc tbranches atypes escrut alts =>
187 fun ite => bind tscrut' = typeToWeakType (caseType tc atypes) ite
188 ; bind vscrut' = mkWeakExprVar tscrut'
189 ; bind tbranches' = @typeToWeakType Γ _ tbranches ite
190 ; bind escrut' = exprToWeakExpr χ escrut ite
192 ((fix caseBranches (tree:Tree ??{scb : StrongCaseBranchWithVVs VV _ _ _ & Expr _ _ _ _ })
193 : UniqM (Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
195 | T_Leaf None => return []
196 | T_Leaf (Some x) => let (scb,e) := x in
197 let varstypes := vec2list (scbwv_varstypes scb) in
198 bind evars_ite = mfresh _ ite
199 ; bind exprvars = seqM (map (fun vt:VV * HaskType _ ★
200 => bind tleaf = typeToWeakType (snd vt) (snd evars_ite)
201 ; bind v' = mkWeakExprVar tleaf
202 ; return ((fst vt),v'))
204 ; let χ' := update_χ' χ exprvars in
205 bind e'' = exprToWeakExpr χ' e (snd evars_ite)
206 ; return [(sac_altcon scb, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')]
207 | T_Branch b1 b2 => bind b1' = caseBranches b1
208 ; bind b2' = caseBranches b2
211 ; bind tys = seqM (ilist_to_list (@ilmap _ _
212 (fun _ => UniqM WeakType) _ (fun _ t => typeToWeakType t ite) atypes))
213 ; return WECase vscrut' escrut' tbranches' tc tys branches'
215 | ELetRec _ _ _ _ _ vars elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
216 => bind tleaf = typeToWeakType (snd vt) ite
217 ; bind v' = mkWeakExprVar tleaf
218 ; return ((fst vt),v'))
220 ; let χ' := update_χ' χ vars' in
221 bind elrb' = exprLetRec2WeakExprLetRec χ' elrb ite
222 ; bind e' = exprToWeakExpr χ' e ite
223 ; return WELetRec elrb' e'
225 with exprLetRec2WeakExprLetRec {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar){vars}(elrb:@ELetRecBindings _ eqVV Γ Δ ξ τ vars)
226 : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> UniqM (Tree ??(WeakExprVar * WeakExpr)) :=
227 match elrb as E in ELetRecBindings G D X L V
228 return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM (Tree ??(WeakExprVar * WeakExpr)) with
229 | ELR_nil _ _ _ _ => fun ite => return []
230 | ELR_leaf _ _ ξ' cv v e => fun ite => bind t' = typeToWeakType (unlev (ξ' v)) ite
231 ; bind e' = exprToWeakExpr χ e ite
232 ; bind v' = match χ v with Error s => failM s | OK y => return y end
234 | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => bind b1' = exprLetRec2WeakExprLetRec χ b1 ite
235 ; bind b2' = exprLetRec2WeakExprLetRec χ b2 ite
240 Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ)
241 (ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
243 match exprToWeakExpr (fun v => Error ("unbound variable " +++ v)) exp ite with
244 uniqM f => f us >>= fun x => OK (snd x)
247 End HaskStrongToWeak.