update baked in CoqPass.hs

[coq-hetmet.git] / src / HaskStrongToWeak.v

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index 79d954c..d86d05b 100644 (file)
--- 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.
@@ -61,7 +62,7 @@ Section HaskStrongToWeak.
                                      | WTyVarTy ec => return WCodeTy ec t2'
                                      | _           => failM  "impossible"
                                    end
-    | TyFunApp    tfc tls       => bind tls' = rawHaskTypeListToWeakType tls
+    | TyFunApp    tfc _ _ tls       => bind tls' = rawHaskTypeListToWeakType tls
                                  ; return WTyFunApp tfc tls'
   end
   with rawHaskTypeListToWeakType {κ}(rht:RawHaskTypeList κ) : UniqM (list WeakType) :=
@@ -94,16 +95,16 @@ 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 Γ Δ ξ τ)
@@ -111,15 +112,16 @@ Section HaskStrongToWeak.
     -> UniqM WeakExpr :=
     match exp as E in @Expr _ _ G D X 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 Γ' _ ξ' t wev         => fun ite => return WEVar wev
+    | 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
@@ -170,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
@@ -186,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'