Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/pub/software/coq-hetmet

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

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index dacdcae..25ecd7b 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) :=
@@ -111,7 +112,8 @@ 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
@@ -156,11 +158,13 @@ Section HaskStrongToWeak.
                   ; bind tbranches' = @typeToWeakType Γ _ tbranches ite
                   ; bind escrut'    = exprToWeakExpr χ escrut ite
                   ; bind branches'  =
-                      ((fix caseBranches (tree:Tree ??{scb : StrongCaseBranchWithVVs VV _ _ _ & 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 []
-                              | T_Leaf (Some x)       => let (scb,e) := x in
+                              | T_Leaf (Some x)       =>
+                                let (sac,scb_e) := x in
+                                let (scb,e) := scb_e in
                                 let varstypes := vec2list (scbwv_varstypes scb) in
                                       bind evars_ite = mfresh _ ite
                                     ; bind exprvars  = seqM (map (fun vt:VV * HaskType _ ★
@@ -170,7 +174,7 @@ Section HaskStrongToWeak.
                                                                 varstypes)
                                     ; let χ' := update_χ' χ exprvars in
                                       bind e'' = exprToWeakExpr χ' e (snd evars_ite)
-                                    ; return [(sac_altcon scb, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')]
+                                    ; return [(sac_altcon sac, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')]
                               | T_Branch b1 b2        => bind b1' = caseBranches b1
                                                        ; bind b2' = caseBranches b2
                                                        ; return (b1',,b2')
@@ -179,7 +183,7 @@ Section HaskStrongToWeak.
                                   (fun _ => UniqM WeakType) _ (fun _ t => typeToWeakType t ite) atypes))
                   ; return WECase vscrut' escrut' tbranches' tc tys branches'
 
-    | ELetRec _ _ _ _ _ vars elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
+    | ELetRec _ _ _ _ _ vars disti elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
                                                                         => bind tleaf = typeToWeakType (snd vt) ite
                                                                          ; bind v' = mkWeakExprVar tleaf
                                                                          ; return ((fst vt),v'))
@@ -207,8 +211,8 @@ Section HaskStrongToWeak.
   Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ)
     (ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
     : ???WeakExpr :=
-    match exprToWeakExpr (fun v => Error ("unbound variable " +++ v)) exp ite with
+    match exprToWeakExpr (fun v => Error ("unbound variable " +++ toString v)) exp ite with
       uniqM f => f us >>= fun x => OK (snd x)
       end.
 
-End HaskStrongToWeak.
\ No newline at end of file
+End HaskStrongToWeak.