almost finished with main theorem
[coq-hetmet.git] / src / HaskStrongToWeak.v
1 (*********************************************************************************************************************************)
2 (* HaskStrongToWeak: convert HaskStrong to HaskWeak                                                                              *)
3 (*********************************************************************************************************************************)
4
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.
20
21 Section HaskStrongToWeak.
22
23   Context (hetmet_brak : WeakExprVar).
24   Context (hetmet_esc  : WeakExprVar).
25
26   Context (mkWeakTypeVar_ : Unique -> Kind                         -> WeakTypeVar).
27   Context (mkWeakCoerVar_ : Unique -> Kind -> WeakType -> WeakType -> WeakCoerVar).
28   Context (mkWeakExprVar_ : Unique ->         WeakType             -> WeakExprVar).
29
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.
33
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'))
41     end.
42
43   Fixpoint rawHaskTypeToWeakType {κ}(rht:RawHaskType (fun _ => WeakTypeVar) κ) {struct rht} : UniqM WeakType :=
44   match rht with
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
60                                  ; match t1' with
61                                      | WTyVarTy ec => return WCodeTy ec t2'
62                                      | _           => failM  "impossible"
63                                    end
64     | TyFunApp    tfc tls       => bind tls' = rawHaskTypeListToWeakType tls
65                                  ; return WTyFunApp tfc tls'
66   end
67   with rawHaskTypeListToWeakType {κ}(rht:RawHaskTypeList κ) : UniqM (list WeakType) :=
68   match rht with
69     | TyFunApp_nil                   => return nil
70     | TyFunApp_cons  κ kl rht' rhtl' => bind t  = rawHaskTypeToWeakType rht'
71                                       ; bind tl = rawHaskTypeListToWeakType rhtl'
72                                       ; return t::tl
73   end.
74   
75   Definition typeToWeakType {Γ}{κ}(τ:HaskType Γ κ)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) : UniqM WeakType :=
76     rawHaskTypeToWeakType (τ _ φ).
77   
78   Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ)
79     := tv::::ite.
80   
81   Definition coercionToWeakCoercion Γ Δ κ t1 t2 ite (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2))
82     : UniqM WeakCoercion
83     := bind t1' = @typeToWeakType Γ κ t1 ite
84      ; bind t2' = @typeToWeakType Γ κ t2 ite
85      ; return WCoUnsafe t1' t2'.
86   
87   Fixpoint seqM {a}(l:list (UniqM a)) : UniqM (list a) :=
88     match l with
89       | nil  => return nil
90       | x::y => bind x' = x
91               ; bind y' = seqM y
92               ; return x'::y'
93     end.
94   
95   Context {VV}{eqVV:EqDecidable VV}{toStringVV:ToString VV}.
96   
97   Definition update_χ (χ:VV->???WeakExprVar)(vv:VV)(ev':WeakExprVar) : VV->???WeakExprVar :=
98     fun vv' =>
99       if eqd_dec vv vv'
100       then OK ev'
101       else χ vv'.
102
103   Fixpoint update_χ' (χ:VV->???WeakExprVar)(varsexprs:list (VV * WeakExprVar)) : VV->???WeakExprVar :=
104     match varsexprs with
105       | nil => χ
106       | (vv,wev)::rest => update_χ (update_χ' χ rest) vv wev
107     end.
108
109   Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ)
110     : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ
111     -> UniqM WeakExpr :=
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 Γ' _ ξ' t wev         => fun ite => return WEVar wev
115     | ELam  Γ'   _ _ tv _ _ cv e    => fun ite => bind tv' = typeToWeakType tv ite
116                                                 ; bind ev' = mkWeakExprVar tv'
117                                                 ; bind e'  = exprToWeakExpr (update_χ χ cv ev') e ite
118                                                 ; return WELam ev' e'
119     | ELet  Γ' _ _ t _ _ ev e1 e2   => fun ite => bind tv' = typeToWeakType t ite
120                                                 ; bind e1' = exprToWeakExpr χ e1 ite
121                                                 ; bind ev' = mkWeakExprVar tv'
122                                                 ; bind e2' = exprToWeakExpr (update_χ χ ev ev') e2 ite
123                                                 ; return WELet ev' e1' e2'
124     | ELit  _ _ _ lit _             => fun ite => return WELit lit
125     | EApp  Γ' _ _ _ _ _ e1 e2      => fun ite => bind e1' = exprToWeakExpr χ e1 ite
126                                                 ; bind e2' = exprToWeakExpr χ e2 ite
127                                                 ; return WEApp e1' e2'
128     | EEsc  Γ' _ _ ec t _ e         => fun ite => bind t' = typeToWeakType t ite
129                                                 ; bind e' = exprToWeakExpr χ e ite
130                                                 ; return WEEsc hetmet_esc (ec _ ite) e' t'
131     | EBrak Γ' _ _ ec t _ e         => fun ite => bind t' = typeToWeakType t ite
132                                                 ; bind e' = exprToWeakExpr χ e ite
133                                                 ; return WEBrak hetmet_brak (ec _ ite) e' t'
134     | ENote _ _ _ _ n e             => fun ite => bind e' = exprToWeakExpr χ e ite
135                                                 ; return WENote n e'
136     | ETyApp  Γ Δ κ σ τ ξ l       e => fun ite => bind t' = typeToWeakType τ ite
137                                                 ; bind e' = exprToWeakExpr χ e ite
138                                                 ; return WETyApp e' t'
139     | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e  => fun ite => bind e' = exprToWeakExpr χ e ite
140                                                 ; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
141                                                 ; return WECoApp e' c'
142     | ECast Γ Δ ξ t1 t2 γ l e      => fun ite  => bind e' = exprToWeakExpr χ e ite
143                                                 ; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
144                                                 ; return WECast e' c'
145     | ETyLam _ _ _ k _ _ e          => fun ite => bind tv = mkWeakTypeVar k
146                                                 ; bind e' = exprToWeakExpr χ e (updateITE tv ite)
147                                                 ; return WETyLam tv e'
148     | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e    => fun ite => bind t1' = typeToWeakType σ₁ ite
149                                                 ; bind t2' = typeToWeakType σ₂ ite
150                                                 ; bind cv  = mkWeakCoerVar κ t1' t2'
151                                                 ; bind e'  = exprToWeakExpr χ e ite
152                                                 ; return WECoLam cv e'
153     | ECase Γ Δ ξ l tc tbranches atypes escrut alts => 
154          fun ite => bind tscrut'    = typeToWeakType (caseType tc atypes) ite
155                   ; bind vscrut'    = mkWeakExprVar tscrut'
156                   ; bind tbranches' = @typeToWeakType Γ _ tbranches ite
157                   ; bind escrut'    = exprToWeakExpr χ escrut ite
158                   ; bind branches'  =
159                       ((fix caseBranches (tree:Tree ??{sac : _ & { scb : StrongCaseBranchWithVVs VV _ _ _ sac & Expr _ _ _ _ } })
160                             : UniqM (Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
161                             match tree with
162                               | T_Leaf None           => return []
163                               | T_Leaf (Some x)       =>
164                                 let (sac,scb_e) := x in
165                                 let (scb,e) := scb_e in
166                                 let varstypes := vec2list (scbwv_varstypes scb) in
167                                       bind evars_ite = mfresh _ ite
168                                     ; bind exprvars  = seqM (map (fun vt:VV * HaskType _ ★
169                                                                         => bind tleaf = typeToWeakType (snd vt) (snd evars_ite)
170                                                                          ; bind v' = mkWeakExprVar tleaf
171                                                                          ; return ((fst vt),v'))
172                                                                 varstypes)
173                                     ; let χ' := update_χ' χ exprvars in
174                                       bind e'' = exprToWeakExpr χ' e (snd evars_ite)
175                                     ; return [(sac_altcon sac, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')]
176                               | T_Branch b1 b2        => bind b1' = caseBranches b1
177                                                        ; bind b2' = caseBranches b2
178                                                        ; return (b1',,b2')
179                             end) alts)
180                   ; bind tys = seqM (ilist_to_list (@ilmap _ _
181                                   (fun _ => UniqM WeakType) _ (fun _ t => typeToWeakType t ite) atypes))
182                   ; return WECase vscrut' escrut' tbranches' tc tys branches'
183
184     | ELetRec _ _ _ _ _ vars elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
185                                                                         => bind tleaf = typeToWeakType (snd vt) ite
186                                                                          ; bind v' = mkWeakExprVar tleaf
187                                                                          ; return ((fst vt),v'))
188                                                                 (leaves vars))
189                                                 ; let χ' := update_χ' χ vars' in
190                                                   bind elrb' = exprLetRec2WeakExprLetRec χ' elrb ite
191                                                 ; bind e'    = exprToWeakExpr χ' e ite
192                                                 ; return WELetRec elrb' e'
193     end
194     with exprLetRec2WeakExprLetRec  {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar){vars}(elrb:@ELetRecBindings _ eqVV Γ Δ ξ τ vars)
195       : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> UniqM (Tree ??(WeakExprVar * WeakExpr)) :=
196     match elrb as E in ELetRecBindings G D X L V
197        return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM (Tree ??(WeakExprVar * WeakExpr)) with
198     | ELR_nil    _ _ _ _           => fun ite => return []
199     | ELR_leaf   _ _ ξ' cv v t e   => fun ite => bind t'  = typeToWeakType t ite
200                                                ; bind e'  = exprToWeakExpr χ e ite
201                                                ; bind v'  = match χ v with Error s => failM s | OK y => return y end
202                                                ; return [(v',e')]
203     | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => bind b1' = exprLetRec2WeakExprLetRec χ b1 ite
204                                                ; bind b2' = exprLetRec2WeakExprLetRec χ b2 ite
205                                                ; return b1',,b2'
206   end.
207
208
209   Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ)
210     (ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
211     : ???WeakExpr :=
212     match exprToWeakExpr (fun v => Error ("unbound variable " +++ toString v)) exp ite with
213       uniqM f => f us >>= fun x => OK (snd x)
214       end.
215
216 End HaskStrongToWeak.