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