Work on implementing abstract predicates

2 files changed, 8 insertions, 43 deletions

diff --git a/src/common/Monad.v b/src/common/Monad.v
index fcbe527..ece047c 100644
--- a/src/common/Monad.v
+++ b/src/common/Monad.v
@@ -18,6 +18,8 @@
 
 From Coq Require Import Lists.List.
 
+Declare Scope monad_scope.
+
 Module Type Monad.
 
   Parameter mon : Type -> Type.
@@ -36,17 +38,18 @@ End Monad.
 Module MonadExtra(M : Monad).
   Import M.
 
-  Module MonadNotation.
+  Module Import MonadNotation.
 
     Notation "'do' X <- A ; B" :=
       (bind A (fun X => B))
-        (at level 200, X name, A at level 100, B at level 200).
+        (at level 200, X name, A at level 100, B at level 200) : monad_scope.
     Notation "'do' ( X , Y ) <- A ; B" :=
       (bind2 A (fun X Y => B))
-        (at level 200, X name, Y name, A at level 100, B at level 200).
+        (at level 200, X name, Y name, A at level 100, B at level 200) : monad_scope.
 
   End MonadNotation.
-  Import MonadNotation.
+
+  #[local] Open Scope monad_scope.
 
   Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) :=
     match l with
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index 5540f34..24abece 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -31,6 +31,7 @@ Require Import compcert.lib.Integers.
 Require Import compcert.lib.Maps.
 
 Require Import vericert.common.Show.
+Require Export vericert.common.Optionmonad.
 
 (* Depend on CompCert for the basic library, as they declare and prove some
    useful theorems. *)
@@ -198,45 +199,6 @@ Ltac crush := simplify; try discriminate; try congruence; try lia; liapp;
 
 Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *)
 
-Module Option.
-
-Definition default {T : Type} (x : T) (u : option T) : T :=
-  match u with
-  | Some y => y
-  | _ => x
-  end.
-
-Definition map {S : Type} {T : Type} (f : S -> T) (u : option S) : option T :=
-  match u with
-  | Some y => Some (f y)
-  | _ => None
-  end.
-
-Definition liftA2 {T : Type} (f : T -> T -> T) (a : option T) (b : option T) : option T :=
-  match a with
-  | Some x => map (f x) b
-  | _ => None
-  end.
-
-Definition bind {A B : Type} (f : option A) (g : A -> option B) : option B :=
-  match f with
-  | Some a => g a
-  | _ => None
-  end.
-
-Definition join {A : Type} (a : option (option A)) : option A :=
-  match a with
-  | None => None
-  | Some a' => a'
-  end.
-
-Module Notation.
-Notation "'do' X <- A ; B" := (bind A (fun X => B))
-   (at level 200, X name, A at level 100, B at level 200).
-End Notation.
-
-End Option.
-
 Parameter debug_print : string -> unit.
 
 Definition debug_show {A B : Type} `{Show A} (a : A) (b : B) : B :=