X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToWeak.v;h=deb7adc20b2b1bb7dfd4edf42c319d1cfad65240;hp=42790b3ae7590afafff90623ceef14089c08077f;hb=3def45d67899c421a3eabaf0c5238d4469ad10d7;hpb=e4fcbccb71fc54544e9acc62e95d1d15ec86294b

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index 42790b3..deb7adc 100644
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -10,7 +10,8 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
@@ -94,33 +95,33 @@ Section HaskStrongToWeak.
   
   Context {VV}{eqVV:EqDecidable VV}{toStringVV:ToString VV}.
   
-  Definition update_χ (χ:VV->???WeakExprVar)(vv:VV)(ev':WeakExprVar) : VV->???WeakExprVar :=
+  Definition update_chi (χ:VV->???WeakExprVar)(vv:VV)(ev':WeakExprVar) : VV->???WeakExprVar :=
     fun vv' =>
       if eqd_dec vv vv'
       then OK ev'
       else χ vv'.
 
-  Fixpoint update_χ' (χ:VV->???WeakExprVar)(varsexprs:list (VV * WeakExprVar)) : VV->???WeakExprVar :=
+  Fixpoint update_chi' (χ:VV->???WeakExprVar)(varsexprs:list (VV * WeakExprVar)) : VV->???WeakExprVar :=
     match varsexprs with
       | nil => χ
-      | (vv,wev)::rest => update_χ (update_χ' χ rest) vv wev
+      | (vv,wev)::rest => update_chi (update_chi' χ rest) vv wev
     end.
 
-  Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ)
+  Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}{l}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ l)
     : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ
     -> UniqM WeakExpr :=
-    match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with
+    match exp as E in @Expr _ _ G D X T L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with
     | EVar  Γ' _ ξ' ev              => fun ite => match χ ev with OK v => return WEVar v | Error s => failM s end
     | EGlobal Γ' _ ξ'   g v lev     => fun ite => bind tv' = mapM (ilist_to_list (ilmap (fun κ x => typeToWeakType x ite) v))
                                                 ; return (fold_left (fun x y => WETyApp x y) tv' (WEVar g))
     | ELam  Γ'   _ _ tv _ _ cv e    => fun ite => bind tv' = typeToWeakType tv ite
                                                 ; bind ev' = mkWeakExprVar tv'
-                                                ; bind e'  = exprToWeakExpr (update_χ χ cv ev') e ite
+                                                ; bind e'  = exprToWeakExpr (update_chi χ cv ev') e ite
                                                 ; return WELam ev' e'
     | ELet  Γ' _ _ t _ _ ev e1 e2   => fun ite => bind tv' = typeToWeakType t ite
                                                 ; bind e1' = exprToWeakExpr χ e1 ite
                                                 ; bind ev' = mkWeakExprVar tv'
-                                                ; bind e2' = exprToWeakExpr (update_χ χ ev ev') e2 ite
+                                                ; bind e2' = exprToWeakExpr (update_chi χ ev ev') e2 ite
                                                 ; return WELet ev' e1' e2'
     | ELit  _ _ _ lit _             => fun ite => return WELit lit
     | EApp  Γ' _ _ _ _ _ e1 e2      => fun ite => bind e1' = exprToWeakExpr χ e1 ite
@@ -132,7 +133,7 @@ Section HaskStrongToWeak.
     | EBrak Γ' _ _ ec t _ e         => fun ite => bind t' = typeToWeakType t ite
                                                 ; bind e' = exprToWeakExpr χ e ite
                                                 ; return WEBrak hetmet_brak (ec _ ite) e' t'
-    | ENote _ _ _ _ n e             => fun ite => bind e' = exprToWeakExpr χ e ite
+    | ENote _ _ _ _ _ n e           => fun ite => bind e' = exprToWeakExpr χ e ite
                                                 ; return WENote n e'
     | ETyApp  Γ Δ κ σ τ ξ l       e => fun ite => bind t' = typeToWeakType τ ite
                                                 ; bind e' = exprToWeakExpr χ e ite
@@ -157,7 +158,7 @@ Section HaskStrongToWeak.
                   ; bind tbranches' = @typeToWeakType Γ _ tbranches ite
                   ; bind escrut'    = exprToWeakExpr χ escrut ite
                   ; bind branches'  =
-                      ((fix caseBranches (tree:Tree ??{sac : _ & { scb : StrongCaseBranchWithVVs VV _ _ _ sac & Expr _ _ _ _ } })
+                      ((fix caseBranches (tree:Tree ??{sac : _ & { scb : StrongCaseBranchWithVVs VV _ _ _ sac & Expr _ _ _ _ _ } })
                             : UniqM (Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
                             match tree with
                               | T_Leaf None           => return []
@@ -171,7 +172,7 @@ Section HaskStrongToWeak.
                                                                          ; bind v' = mkWeakExprVar tleaf
                                                                          ; return ((fst vt),v'))
                                                                 varstypes)
-                                    ; let χ' := update_χ' χ exprvars in
+                                    ; let χ' := update_chi' χ exprvars in
                                       bind e'' = exprToWeakExpr χ' e (snd evars_ite)
                                     ; return [(sac_altcon sac, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')]
                               | T_Branch b1 b2        => bind b1' = caseBranches b1
@@ -187,7 +188,7 @@ Section HaskStrongToWeak.
                                                                          ; bind v' = mkWeakExprVar tleaf
                                                                          ; return ((fst vt),v'))
                                                                 (leaves vars))
-                                                ; let χ' := update_χ' χ vars' in
+                                                ; let χ' := update_chi' χ vars' in
                                                   bind elrb' = exprLetRec2WeakExprLetRec χ' elrb ite
                                                 ; bind e'    = exprToWeakExpr χ' e ite
                                                 ; return WELetRec elrb' e'
@@ -207,7 +208,7 @@ Section HaskStrongToWeak.
   end.
 
 
-  Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ)
+  Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}{l}(exp:@Expr _ eqVV Γ Δ ξ τ l)
     (ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
     : ???WeakExpr :=
     match exprToWeakExpr (fun v => Error ("unbound variable " +++ toString v)) exp ite with