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 updateITE_ {Γ:TypeEnv}{TV:Kind->Type}{κ}{n}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ)
83 : InstantiatedTypeEnv TV (list_ins n κ Γ).
85 rewrite <- (list_take_drop _ Γ n) in ite.
87 apply ilist_chop in ite; auto.
90 apply ilist_chop' in ite.
94 Definition coercionToWeakCoercion Γ Δ κ t1 t2 ite (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2))
96 := bind t1' = @typeToWeakType Γ κ t1 ite
97 ; bind t2' = @typeToWeakType Γ κ t2 ite
98 ; return WCoUnsafe t1' t2'.
100 Fixpoint seqM {a}(l:list (UniqM a)) : UniqM (list a) :=
103 | x::y => bind x' = x
108 Context {VV}{eqVV:EqDecidable VV}{toStringVV:ToString VV}.
110 Definition update_chi (χ:VV->???WeakExprVar)(vv:VV)(ev':WeakExprVar) : VV->???WeakExprVar :=
116 Fixpoint update_chi' (χ:VV->???WeakExprVar)(varsexprs:list (VV * WeakExprVar)) : VV->???WeakExprVar :=
119 | (vv,wev)::rest => update_chi (update_chi' χ rest) vv wev
122 Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}{l}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ l)
123 : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ
125 match exp as E in @Expr _ _ G D X T L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with
126 | EVar Γ' _ ξ' ev => fun ite => match χ ev with OK v => return WEVar v | Error s => failM s end
127 | EGlobal Γ' _ ξ' g v lev => fun ite => bind tv' = mapM (ilist_to_list (ilmap (fun κ x => typeToWeakType x ite) v))
128 ; return (fold_left (fun x y => WETyApp x y) tv' (WEVar g))
129 | ELam Γ' _ _ tv _ _ cv e => fun ite => bind tv' = typeToWeakType tv ite
130 ; bind ev' = mkWeakExprVar tv'
131 ; bind e' = exprToWeakExpr (update_chi χ cv ev') e ite
132 ; return WELam ev' e'
133 | ELet Γ' _ _ t _ _ ev e1 e2 => fun ite => bind tv' = typeToWeakType t ite
134 ; bind e1' = exprToWeakExpr χ e1 ite
135 ; bind ev' = mkWeakExprVar tv'
136 ; bind e2' = exprToWeakExpr (update_chi χ ev ev') e2 ite
137 ; return WELet ev' e1' e2'
138 | ELit _ _ _ lit _ => fun ite => return WELit lit
139 | EApp Γ' _ _ _ _ _ e1 e2 => fun ite => bind e1' = exprToWeakExpr χ e1 ite
140 ; bind e2' = exprToWeakExpr χ e2 ite
141 ; return WEApp e1' e2'
142 | EEsc Γ' _ _ ec t _ e => fun ite => bind t' = typeToWeakType t ite
143 ; bind e' = exprToWeakExpr χ e ite
144 ; return WEEsc hetmet_esc (ec _ ite) e' t'
145 | EBrak Γ' _ _ ec t _ e => fun ite => bind t' = typeToWeakType t ite
146 ; bind e' = exprToWeakExpr χ e ite
147 ; return WEBrak hetmet_brak (ec _ ite) e' t'
148 | ENote _ _ _ _ _ n e => fun ite => bind e' = exprToWeakExpr χ e ite
150 | ETyApp Γ Δ κ σ τ ξ l e => fun ite => bind t' = typeToWeakType τ ite
151 ; bind e' = exprToWeakExpr χ e ite
152 ; return WETyApp e' t'
153 | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => fun ite => bind e' = exprToWeakExpr χ e ite
154 ; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
155 ; return WECoApp e' c'
156 | ECast Γ Δ ξ t1 t2 γ l e => fun ite => bind e' = exprToWeakExpr χ e ite
157 ; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
158 ; return WECast e' c'
159 | ETyLam _ _ _ k _ _ n e => fun ite => bind tv = mkWeakTypeVar k
160 ; bind e' = exprToWeakExpr χ e (updateITE_ tv ite)
161 ; return WETyLam tv e'
162 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => fun ite => bind t1' = typeToWeakType σ₁ ite
163 ; bind t2' = typeToWeakType σ₂ ite
164 ; bind cv = mkWeakCoerVar κ t1' t2'
165 ; bind e' = exprToWeakExpr χ e ite
166 ; return WECoLam cv e'
167 | ECase Γ Δ ξ l tc tbranches atypes escrut alts =>
168 fun ite => bind tscrut' = typeToWeakType (caseType tc atypes) ite
169 ; bind vscrut' = mkWeakExprVar tscrut'
170 ; bind tbranches' = @typeToWeakType Γ _ tbranches ite
171 ; bind escrut' = exprToWeakExpr χ escrut ite
173 ((fix caseBranches (tree:Tree ??{sac : _ & { scb : StrongCaseBranchWithVVs VV _ _ _ sac & Expr _ _ _ _ _ } })
174 : UniqM (Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
176 | T_Leaf None => return []
178 let (sac,scb_e) := x in
179 let (scb,e) := scb_e in
180 let varstypes := vec2list (scbwv_varstypes scb) in
181 bind evars_ite = mfresh _ ite
182 ; bind exprvars = seqM (map (fun vt:VV * HaskType _ ★
183 => bind tleaf = typeToWeakType (snd vt) (snd evars_ite)
184 ; bind v' = mkWeakExprVar tleaf
185 ; return ((fst vt),v'))
187 ; let χ' := update_chi' χ exprvars in
188 bind e'' = exprToWeakExpr χ' e (snd evars_ite)
189 ; return [(sac_altcon sac, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')]
190 | T_Branch b1 b2 => bind b1' = caseBranches b1
191 ; bind b2' = caseBranches b2
194 ; bind tys = seqM (ilist_to_list (@ilmap _ _
195 (fun _ => UniqM WeakType) _ (fun _ t => typeToWeakType t ite) atypes))
196 ; return WECase vscrut' escrut' tbranches' tc tys branches'
198 | ELetRec _ _ _ _ _ vars disti elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
199 => bind tleaf = typeToWeakType (snd vt) ite
200 ; bind v' = mkWeakExprVar tleaf
201 ; return ((fst vt),v'))
203 ; let χ' := update_chi' χ vars' in
204 bind elrb' = exprLetRec2WeakExprLetRec χ' elrb ite
205 ; bind e' = exprToWeakExpr χ' e ite
206 ; return WELetRec elrb' e'
208 with exprLetRec2WeakExprLetRec {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar){vars}(elrb:@ELetRecBindings _ eqVV Γ Δ ξ τ vars)
209 : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> UniqM (Tree ??(WeakExprVar * WeakExpr)) :=
210 match elrb as E in ELetRecBindings G D X L V
211 return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM (Tree ??(WeakExprVar * WeakExpr)) with
212 | ELR_nil _ _ _ _ => fun ite => return []
213 | ELR_leaf _ _ ξ' cv v t e => fun ite => bind t' = typeToWeakType t ite
214 ; bind e' = exprToWeakExpr χ e ite
215 ; bind v' = match χ v with Error s => failM s | OK y => return y end
217 | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => bind b1' = exprLetRec2WeakExprLetRec χ b1 ite
218 ; bind b2' = exprLetRec2WeakExprLetRec χ b2 ite
223 Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}{l}(exp:@Expr _ eqVV Γ Δ ξ τ l)
224 (ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
226 match exprToWeakExpr (fun v => Error ("unbound variable " +++ toString v)) exp ite with
227 uniqM f => f us >>= fun x => OK (snd x)
230 End HaskStrongToWeak.