add UniqMonad

diff --git a/src/General.v b/src/General.v
index 188a2dc..ffd0d29 100644 (file)
--- a/src/General.v
+++ b/src/General.v
@@ -738,6 +738,46 @@ Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???(
     apply (Error (error_message (length l) n)).
     Defined.
 
     apply (Error (error_message (length l) n)).
     Defined.
 

+(* 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".
+Variable unique_eq       : forall u1 u2:Unique, sumbool (u1=u2) (u1≠u2).
+    Extract Inlined Constant unique_eq => "(==)".
+Variable unique_toString : Unique -> string.
+    Extract Inlined Constant unique_toString => "show".
+Instance EqDecidableUnique : EqDecidable Unique :=
+  { eqd_dec := unique_eq }.
+Instance EqDecidableToString : ToString Unique :=
+  { toString := unique_toString }.
+
+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).

 
 
 
 
 
 

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index e86e544..cbe6715 100644 (file)
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -18,39 +18,6 @@ Require Import HaskWeakToCore.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 
 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).
 Section HaskStrongToWeak.
 
   Context (hetmet_brak : WeakExprVar).