lots of cleanup

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

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index e86e544..e956dd6 100644 (file)
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -18,39 +18,6 @@ Require Import HaskWeakToCore.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 
-(* Uniques *)
-Variable UniqSupply      : Type.                   Extract Inlined Constant UniqSupply     => "UniqSupply.UniqSupply".
-Variable Unique          : Type.                   Extract Inlined Constant Unique         => "Unique.Unique".
-Variable uniqFromSupply  : UniqSupply -> Unique.   Extract Inlined Constant uniqFromSupply => "UniqSupply.uniqFromSupply".
-Variable splitUniqSupply : UniqSupply -> UniqSupply * UniqSupply.
-    Extract Inlined Constant splitUniqSupply => "UniqSupply.splitUniqSupply".
-
-Inductive UniqM {T:Type} : Type :=
- | uniqM    : (UniqSupply -> ???(UniqSupply * T)) -> UniqM.
- Implicit Arguments UniqM [ ].
-
-Instance UniqMonad : Monad UniqM :=
-{ returnM := fun T (x:T) => uniqM (fun u => OK (u,x))
-; bindM   := fun a b (x:UniqM a) (f:a->UniqM b) =>
-  uniqM (fun u =>
-    match x with
-      | uniqM fa =>
-        match fa u with
-          | Error s   => Error s
-          | OK (u',va) => match f va with
-                           | uniqM fb => fb u'
-                         end
-        end
-    end)
-}.
-
-Definition getU : UniqM Unique :=
-  uniqM (fun us => let (us1,us2) := splitUniqSupply us in OK (us1,(uniqFromSupply us2))).
-
-Notation "'bind' x = e ; f" := (@bindM _ _ _ _ e (fun x => f)) (x ident, at level 60, right associativity).
-Notation "'return' x" := (returnM x) (at level 100).
-Notation "'failM'  x" := (uniqM (fun _ => Error x)) (at level 100).
-
 Section HaskStrongToWeak.
 
   Context (hetmet_brak : WeakExprVar).
@@ -189,11 +156,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 _ ★
@@ -203,7 +172,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')
@@ -227,7 +196,7 @@ Section HaskStrongToWeak.
     match elrb as E in ELetRecBindings G D X L V
        return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM (Tree ??(WeakExprVar * WeakExpr)) with
     | ELR_nil    _ _ _ _           => fun ite => return []
-    | ELR_leaf   _ _ ξ' cv v e     => fun ite => bind t'  = typeToWeakType (unlev (ξ' v)) ite
+    | ELR_leaf   _ _ ξ' cv v t e   => fun ite => bind t'  = typeToWeakType t ite
                                                ; bind e'  = exprToWeakExpr χ e ite
                                                ; bind v'  = match χ v with Error s => failM s | OK y => return y end
                                                ; return [(v',e')]
@@ -240,8 +209,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.