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 HaskLiterals.
14 Require Import HaskTyCons.
15 Require Import HaskWeakTypes.
16 Require Import HaskWeakVars.
17 Require Import HaskWeak.
18 Require Import HaskWeakToCore.
19 Require Import HaskStrongTypes.
20 Require Import HaskStrong.
22 Section HaskStrongToWeak.
24 Context (hetmet_brak : WeakExprVar).
25 Context (hetmet_esc : WeakExprVar).
27 Context (mkWeakTypeVar_ : Unique -> Kind -> WeakTypeVar).
28 Context (mkWeakCoerVar_ : Unique -> Kind -> WeakType -> WeakType -> WeakCoerVar).
29 Context (mkWeakExprVar_ : Unique -> WeakType -> WeakExprVar).
31 Definition mkWeakTypeVar (k:Kind) : UniqM WeakTypeVar := bind u = getU ; return mkWeakTypeVar_ u k.
32 Definition mkWeakCoerVar (k:Kind)(t1 t2:WeakType) : UniqM WeakCoerVar := bind u = getU ; return mkWeakCoerVar_ u k t1 t2.
33 Definition mkWeakExprVar (t:WeakType) : UniqM WeakExprVar := bind u = getU ; return mkWeakExprVar_ u t.
35 Fixpoint mfresh (lk:list Kind){Γ}(ite:IList _ (fun _ => WeakTypeVar) Γ)
36 : UniqM (((vec WeakTypeVar (length lk)) * (IList _ (fun _ => WeakTypeVar) (app lk Γ)))) :=
37 match lk as LK return UniqM ((vec WeakTypeVar (length LK)) * (IList _ (fun _ => WeakTypeVar) (app LK Γ))) with
38 | nil => return (vec_nil,ite)
39 | k::lk' => bind v = mkWeakTypeVar k
40 ; bind vars_ite' = mfresh lk' ite
41 ; return ((v:::(fst vars_ite')),v::::(snd vars_ite'))
44 Fixpoint rawHaskTypeToWeakType {κ}(rht:RawHaskType (fun _ => WeakTypeVar) κ) {struct rht} : UniqM WeakType :=
46 | TVar _ v => return WTyVarTy v
47 | TCon tc => return WTyCon tc
48 | TCoerc _ t1 t2 t3 => bind t1' = rawHaskTypeToWeakType t1
49 ; bind t2' = rawHaskTypeToWeakType t2
50 ; bind t3' = rawHaskTypeToWeakType t3
51 ; return WCoFunTy t1' t2' t3'
52 | TArrow => return WFunTyCon
53 | TApp _ _ t1 t2 => bind t1' = rawHaskTypeToWeakType t1
54 ; bind t2' = rawHaskTypeToWeakType t2
55 ; return WAppTy t1' t2'
56 | TAll k rht' => bind tv = mkWeakTypeVar k
57 ; bind t' = rawHaskTypeToWeakType (rht' tv)
58 ; return WForAllTy tv t'
59 | TCode t1 t2 => bind t1' = rawHaskTypeToWeakType t1
60 ; bind t2' = rawHaskTypeToWeakType t2
62 | WTyVarTy ec => return WCodeTy ec t2'
63 | _ => failM "impossible"
65 | TyFunApp tfc _ _ tls => bind tls' = rawHaskTypeListToWeakType tls
66 ; return WTyFunApp tfc tls'
68 with rawHaskTypeListToWeakType {κ}(rht:RawHaskTypeList κ) : UniqM (list WeakType) :=
70 | TyFunApp_nil => return nil
71 | TyFunApp_cons κ kl rht' rhtl' => bind t = rawHaskTypeToWeakType rht'
72 ; bind tl = rawHaskTypeListToWeakType rhtl'
76 Definition typeToWeakType {Γ}{κ}(τ:HaskType Γ κ)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) : UniqM WeakType :=
77 rawHaskTypeToWeakType (τ _ φ).
79 Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ)
82 Definition coercionToWeakCoercion Γ Δ κ t1 t2 ite (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2))
84 := bind t1' = @typeToWeakType Γ κ t1 ite
85 ; bind t2' = @typeToWeakType Γ κ t2 ite
86 ; return WCoUnsafe t1' t2'.
88 Fixpoint seqM {a}(l:list (UniqM a)) : UniqM (list a) :=
96 Context {VV}{eqVV:EqDecidable VV}{toStringVV:ToString VV}.
98 Definition update_χ (χ:VV->???WeakExprVar)(vv:VV)(ev':WeakExprVar) : VV->???WeakExprVar :=
104 Fixpoint update_χ' (χ:VV->???WeakExprVar)(varsexprs:list (VV * WeakExprVar)) : VV->???WeakExprVar :=
107 | (vv,wev)::rest => update_χ (update_χ' χ rest) vv wev
110 Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ)
111 : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ
113 match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with
114 | EVar Γ' _ ξ' ev => fun ite => match χ ev with OK v => return WEVar v | Error s => failM s end
115 | EGlobal Γ' _ ξ' g v lev => fun ite => bind tv' = mapM (ilist_to_list (ilmap (fun κ x => typeToWeakType x ite) v))
116 ; return (fold_left (fun x y => WETyApp x y) tv' (WEVar g))
117 | ELam Γ' _ _ tv _ _ cv e => fun ite => bind tv' = typeToWeakType tv ite
118 ; bind ev' = mkWeakExprVar tv'
119 ; bind e' = exprToWeakExpr (update_χ χ cv ev') e ite
120 ; return WELam ev' e'
121 | ELet Γ' _ _ t _ _ ev e1 e2 => fun ite => bind tv' = typeToWeakType t ite
122 ; bind e1' = exprToWeakExpr χ e1 ite
123 ; bind ev' = mkWeakExprVar tv'
124 ; bind e2' = exprToWeakExpr (update_χ χ ev ev') e2 ite
125 ; return WELet ev' e1' e2'
126 | ELit _ _ _ lit _ => fun ite => return WELit lit
127 | EApp Γ' _ _ _ _ _ e1 e2 => fun ite => bind e1' = exprToWeakExpr χ e1 ite
128 ; bind e2' = exprToWeakExpr χ e2 ite
129 ; return WEApp e1' e2'
130 | EEsc Γ' _ _ ec t _ e => fun ite => bind t' = typeToWeakType t ite
131 ; bind e' = exprToWeakExpr χ e ite
132 ; return WEEsc hetmet_esc (ec _ ite) e' t'
133 | EBrak Γ' _ _ ec t _ e => fun ite => bind t' = typeToWeakType t ite
134 ; bind e' = exprToWeakExpr χ e ite
135 ; return WEBrak hetmet_brak (ec _ ite) e' t'
136 | ENote _ _ _ _ n e => fun ite => bind e' = exprToWeakExpr χ e ite
138 | ETyApp Γ Δ κ σ τ ξ l e => fun ite => bind t' = typeToWeakType τ ite
139 ; bind e' = exprToWeakExpr χ e ite
140 ; return WETyApp e' t'
141 | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => fun ite => bind e' = exprToWeakExpr χ e ite
142 ; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
143 ; return WECoApp e' c'
144 | ECast Γ Δ ξ t1 t2 γ l e => fun ite => bind e' = exprToWeakExpr χ e ite
145 ; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
146 ; return WECast e' c'
147 | ETyLam _ _ _ k _ _ e => fun ite => bind tv = mkWeakTypeVar k
148 ; bind e' = exprToWeakExpr χ e (updateITE tv ite)
149 ; return WETyLam tv e'
150 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => fun ite => bind t1' = typeToWeakType σ₁ ite
151 ; bind t2' = typeToWeakType σ₂ ite
152 ; bind cv = mkWeakCoerVar κ t1' t2'
153 ; bind e' = exprToWeakExpr χ e ite
154 ; return WECoLam cv e'
155 | ECase Γ Δ ξ l tc tbranches atypes escrut alts =>
156 fun ite => bind tscrut' = typeToWeakType (caseType tc atypes) ite
157 ; bind vscrut' = mkWeakExprVar tscrut'
158 ; bind tbranches' = @typeToWeakType Γ _ tbranches ite
159 ; bind escrut' = exprToWeakExpr χ escrut ite
161 ((fix caseBranches (tree:Tree ??{sac : _ & { scb : StrongCaseBranchWithVVs VV _ _ _ sac & Expr _ _ _ _ } })
162 : UniqM (Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
164 | T_Leaf None => return []
166 let (sac,scb_e) := x in
167 let (scb,e) := scb_e in
168 let varstypes := vec2list (scbwv_varstypes scb) in
169 bind evars_ite = mfresh _ ite
170 ; bind exprvars = seqM (map (fun vt:VV * HaskType _ ★
171 => bind tleaf = typeToWeakType (snd vt) (snd evars_ite)
172 ; bind v' = mkWeakExprVar tleaf
173 ; return ((fst vt),v'))
175 ; let χ' := update_χ' χ exprvars in
176 bind e'' = exprToWeakExpr χ' e (snd evars_ite)
177 ; return [(sac_altcon sac, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')]
178 | T_Branch b1 b2 => bind b1' = caseBranches b1
179 ; bind b2' = caseBranches b2
182 ; bind tys = seqM (ilist_to_list (@ilmap _ _
183 (fun _ => UniqM WeakType) _ (fun _ t => typeToWeakType t ite) atypes))
184 ; return WECase vscrut' escrut' tbranches' tc tys branches'
186 | ELetRec _ _ _ _ _ vars disti elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
187 => bind tleaf = typeToWeakType (snd vt) ite
188 ; bind v' = mkWeakExprVar tleaf
189 ; return ((fst vt),v'))
191 ; let χ' := update_χ' χ vars' in
192 bind elrb' = exprLetRec2WeakExprLetRec χ' elrb ite
193 ; bind e' = exprToWeakExpr χ' e ite
194 ; return WELetRec elrb' e'
196 with exprLetRec2WeakExprLetRec {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar){vars}(elrb:@ELetRecBindings _ eqVV Γ Δ ξ τ vars)
197 : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> UniqM (Tree ??(WeakExprVar * WeakExpr)) :=
198 match elrb as E in ELetRecBindings G D X L V
199 return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM (Tree ??(WeakExprVar * WeakExpr)) with
200 | ELR_nil _ _ _ _ => fun ite => return []
201 | ELR_leaf _ _ ξ' cv v t e => fun ite => bind t' = typeToWeakType t ite
202 ; bind e' = exprToWeakExpr χ e ite
203 ; bind v' = match χ v with Error s => failM s | OK y => return y end
205 | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => bind b1' = exprLetRec2WeakExprLetRec χ b1 ite
206 ; bind b2' = exprLetRec2WeakExprLetRec χ b2 ite
211 Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ)
212 (ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
214 match exprToWeakExpr (fun v => Error ("unbound variable " +++ toString v)) exp ite with
215 uniqM f => f us >>= fun x => OK (snd x)
218 End HaskStrongToWeak.