Add a staging notion to summariesrefs/pull/16056/head

We distinguish two stages and separate the system state accordingly.
`Synterp` is the syntactic interpretation phase, i.e. vernacular parsing and
execution of commands having an effect on parsing. `Interp` is the
interpretation phase, where standard commands are executed.

2 files changed, 20 insertions, 0 deletions

diff --git a/clib/dyn.ml b/clib/dyn.ml
index 8ef90a3..0e3d639 100644
--- a/clib/dyn.ml
+++ b/clib/dyn.ml
@@ -30,6 +30,9 @@ sig
   type any = Any : 'a key * 'a value -> any
   val iter : (any -> unit) -> t -> unit
   val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
+
+  type filter = { filter : 'a. 'a key -> 'a value -> bool }
+  val filter : filter -> t -> t
 end
 
 module type PreS =
@@ -54,6 +57,9 @@ sig
     sig
       type map = { map : 'a. 'a tag -> 'a V1.t -> 'a V2.t }
       val map : map -> Map(V1).t -> Map(V2).t
+
+      type filter = { filter : 'a. 'a tag -> 'a V1.t -> bool }
+      val filter : filter -> Map(V1).t -> Map(V1).t
     end
 
 end
@@ -138,6 +144,9 @@ module Self : PreS = struct
     type any = Any : 'a tag * 'a value -> any
     let iter f m = Int.Map.iter (fun k v -> f (Any (k, v))) m
     let fold f m accu = Int.Map.fold (fun k v accu -> f (Any (k, v)) accu) m accu
+
+    type filter = { filter : 'a. 'a tag -> 'a value -> bool }
+    let filter f m = Int.Map.filter f.filter m
   end
 
   module HMap (V1 : ValueS) (V2 : ValueS) =
@@ -147,6 +156,11 @@ module Self : PreS = struct
     let map (f : map) (m : Map(V1).t) : Map(V2).t =
       Int.Map.mapi f.map m
 
+    type filter = { filter : 'a. 'a tag -> 'a V1.t -> bool }
+
+    let filter (f : filter) (m : Map(V1).t) : Map(V1).t =
+      Int.Map.filter f.filter m
+
   end
 
 end
diff --git a/clib/dyn.mli b/clib/dyn.mli
index 4fd33b5..23059be 100644
--- a/clib/dyn.mli
+++ b/clib/dyn.mli
@@ -32,6 +32,9 @@ sig
   type any = Any : 'a key * 'a value -> any
   val iter : (any -> unit) -> t -> unit
   val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
+
+  type filter = { filter : 'a. 'a key -> 'a value -> bool }
+  val filter : filter -> t -> t
 end
 
 module type S =
@@ -79,6 +82,9 @@ sig
     sig
       type map = { map : 'a. 'a tag -> 'a V1.t -> 'a V2.t }
       val map : map -> Map(V1).t -> Map(V2).t
+
+      type filter = { filter : 'a. 'a tag -> 'a V1.t -> bool }
+      val filter : filter -> Map(V1).t -> Map(V1).t
     end
 
   module Easy : sig