[WP] Relocatable sig

src/plugins/wp/StmtCompiler.ml

@@ -29,7 +29,6 @@ sig
 
   module M : Model
 
-
   module Node : sig
     type t
     module Map : Qed.Idxmap.S with type key = t
@@ -43,29 +42,28 @@ sig
   module E : sig
     type t
     val create : M.sigma sequence -> F.pred -> t
-    (** Bundle an equation with the sigma sequence that created it *)
+    val get : t -> F.pred
+    val reads : t -> M.domain
+    val writes : t -> M.domain
     val relocate : M.sigma sequence -> t -> t
-    val get: t -> F.pred
   end
 
-  (** Relocatable predicate *)
-  module P :
-  sig
-    type t
-    val create : M.sigma Node.Map.t -> F.pred -> t
-    (** Bundle an equation with the sigma sequence that created it. *)
-    val relocate : M.sigma Node.Map.t -> t -> t
-    val get: t -> F.pred
-  end
-  
-  (** Relocatable condition *)
   module C :
   sig
     type t
     val create : M.sigma -> F.pred -> t
-    (** Bundle an equation with the sigma sequence that created it. *)
+    val get : t -> F.pred
+    val reads : t -> M.domain
     val relocate : M.sigma -> t -> t
+  end
+
+  module P :
+  sig
+    type t
+    val create : M.sigma Node.Map.t -> F.pred -> t
     val get: t -> F.pred
+    val reads : t -> M.domain Node.Map.t
+    val relocate : M.sigma Node.Map.t -> t -> t
   end
 
   type cfg

src/plugins/wp/StmtCompiler.mli

@@ -73,9 +73,9 @@ sig
   end
 
   type node = Node.t
-                                                  
-  val node : unit -> node
+
   (** fresh node *)
+  val node : unit -> node
 
   (** {2 Relocatable Formulae}
       Can be created once with fresh environment, and used several
@@ -84,31 +84,37 @@ sig
   (** Relocatable set of equations *)
   module E : sig
     type t
-    val create : M.sigma sequence -> F.pred -> t
+      
     (** Bundle an equation with the sigma sequence that created it *)
+    val create : M.sigma sequence -> F.pred -> t
+    val get : t -> F.pred
+    val reads : t -> M.domain
+    val writes : t -> M.domain
     val relocate : M.sigma sequence -> t -> t
-    val get: t -> F.pred
   end
 
-  (** Relocatable predicate *)
-  module P :
+  (** Relocatable condition *)
+  module C :
   sig
     type t
-    val create : M.sigma Node.Map.t -> F.pred -> t
+      
     (** Bundle an equation with the sigma sequence that created it. *)
-    val relocate : M.sigma Node.Map.t -> t -> t
-    val get: t -> F.pred
+    val create : M.sigma -> F.pred -> t
+    val get : t -> F.pred
+    val reads : t -> M.domain
+    val relocate : M.sigma -> t -> t
   end
 
-
-  (** Relocatable condition *)
-  module C :
+  (** Relocatable predicate *)
+  module P :
   sig
     type t
-    val create : M.sigma -> F.pred -> t
+      
     (** Bundle an equation with the sigma sequence that created it. *)
-    val relocate : M.sigma -> t -> t
+    val create : M.sigma Node.Map.t -> F.pred -> t
     val get: t -> F.pred
+    val reads : t -> M.domain Node.Map.t
+    val relocate : M.sigma Node.Map.t -> t -> t
   end
 
   type cfg (** Structured collection of traces. *)