From 38c62ef2e9ce28370cd22aadab9d676ffb2bac56 Mon Sep 17 00:00:00 2001
From: whitequark
Date: Thu, 21 Jun 2018 01:18:38 +0000
Subject: Reformat Dyn.{ml,mli}.

---
 clib/dyn.ml  | 183 ++++++++++++++++++++++++++++-------------------------------
 clib/dyn.mli |  41 ++++++-------
 2 files changed, 106 insertions(+), 118 deletions(-)

diff --git a/clib/dyn.ml b/clib/dyn.ml
index e9b0419881..7cdbf15a44 100644
--- a/clib/dyn.ml
+++ b/clib/dyn.ml
@@ -24,32 +24,29 @@ sig
   val find : 'a key -> t -> 'a obj
   val mem : 'a key -> t -> bool
 
-  type any = Any : 'a key * 'a obj -> any
-
   type map = { map : 'a. 'a key -> 'a obj -> 'a obj }
   val map : map -> t -> t
 
+  type any = Any : 'a key * 'a obj -> any
   val iter : (any -> unit) -> t -> unit
   val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
 end
 
 module type PreS =
 sig
-type 'a tag
-type t = Dyn : 'a tag * 'a -> t
-
-val create : string -> 'a tag
-val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
-val repr : 'a tag -> string
+  type 'a tag
+  type t = Dyn : 'a tag * 'a -> t
 
-type any = Any : 'a tag -> any
+  val create : string -> 'a tag
+  val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
+  val repr : 'a tag -> string
 
-val name : string -> any option
+  val dump : unit -> (int * string) list
 
-module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag
-
-val dump : unit -> (int * string) list
+  type any = Any : 'a tag -> any
+  val name : string -> any option
 
+  module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag
 end
 
 module type S =
@@ -57,104 +54,100 @@ sig
   include PreS
 
   module Easy : sig
-
     val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag
     val make_dyn : string -> ('a -> t) * (t -> 'a)
     val inj : 'a -> 'a tag -> t
     val prj : t -> 'a tag -> 'a option
   end
-
 end
 
 module Make () = struct
-module Self : PreS = struct
-(* Dynamics, programmed with DANGER !!! *)
 
-type 'a tag = int
-
-type t = Dyn : 'a tag * 'a -> t
-
-type any = Any : 'a tag -> any
-
-let dyntab = ref (Int.Map.empty : string Int.Map.t)
-(** Instead of working with tags as strings, which are costly, we use their
-    hash. We ensure unicity of the hash in the [create] function. If ever a
-    collision occurs, which is unlikely, it is sufficient to tweak the offending
-    dynamic tag. *)
-
-let create (s : string) =
-  let hash = Hashtbl.hash s in
-  let () =
-    if Int.Map.mem hash !dyntab then
-      let old = Int.Map.find hash !dyntab in
-      let () = Printf.eprintf "Dynamic tag collision: %s vs. %s\n%!" s old in
+module Self : PreS = struct
+  (* Dynamics, programmed with DANGER !!! *)
+
+  type 'a tag = int
+
+  type t = Dyn : 'a tag * 'a -> t
+
+  type any = Any : 'a tag -> any
+
+  let dyntab = ref (Int.Map.empty : string Int.Map.t)
+  (** Instead of working with tags as strings, which are costly, we use their
+      hash. We ensure unicity of the hash in the [create] function. If ever a
+      collision occurs, which is unlikely, it is sufficient to tweak the offending
+      dynamic tag. *)
+
+  let create (s : string) =
+    let hash = Hashtbl.hash s in
+    let () =
+      if Int.Map.mem hash !dyntab then
+        let old = Int.Map.find hash !dyntab in
+        let () = Printf.eprintf "Dynamic tag collision: %s vs. %s\n%!" s old in
+        assert false
+    in
+    let () = dyntab := Int.Map.add hash s !dyntab in
+    hash
+
+  let eq : 'a 'b. 'a tag -> 'b tag -> ('a, 'b) CSig.eq option =
+    fun h1 h2 -> if Int.equal h1 h2 then Some (Obj.magic CSig.Refl) else None
+
+  let repr s =
+    try Int.Map.find s !dyntab
+    with Not_found ->
+      let () = Printf.eprintf "Unknown dynamic tag %i\n%!" s in
       assert false
-  in
-  let () = dyntab := Int.Map.add hash s !dyntab in
-  hash
-
-let eq : 'a 'b. 'a tag -> 'b tag -> ('a, 'b) CSig.eq option =
-  fun h1 h2 -> if Int.equal h1 h2 then Some (Obj.magic CSig.Refl) else None
-
-let repr s =
-  try Int.Map.find s !dyntab
-  with Not_found ->
-    let () = Printf.eprintf "Unknown dynamic tag %i\n%!" s in
-    assert false
-
-let name s =
-  let hash = Hashtbl.hash s in
-  if Int.Map.mem hash !dyntab then Some (Any hash) else None
-
-let dump () = Int.Map.bindings !dyntab
-
-module Map(M : TParam) =
-struct
-type t = Obj.t M.t Int.Map.t
-type 'a obj = 'a M.t
-type 'a key = 'a tag
-let cast : 'a M.t -> 'b M.t = Obj.magic
-let empty = Int.Map.empty
-let add tag v m = Int.Map.add tag (cast v) m
-let remove tag m = Int.Map.remove tag m
-let find tag m = cast (Int.Map.find tag m)
-let mem = Int.Map.mem
-
-type any = Any : 'a tag * 'a M.t -> any
-
-type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t }
-let map f m = Int.Map.mapi f.map m
-
-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
-end
 
+  let name s =
+    let hash = Hashtbl.hash s in
+    if Int.Map.mem hash !dyntab then Some (Any hash) else None
+
+  let dump () = Int.Map.bindings !dyntab
+
+  module Map(M : TParam) =
+  struct
+    type t = Obj.t M.t Int.Map.t
+    type 'a obj = 'a M.t
+    type 'a key = 'a tag
+    let cast : 'a M.t -> 'b M.t = Obj.magic
+    let empty = Int.Map.empty
+    let add tag v m = Int.Map.add tag (cast v) m
+    let remove tag m = Int.Map.remove tag m
+    let find tag m = cast (Int.Map.find tag m)
+    let mem = Int.Map.mem
+
+    type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t }
+    let map f m = Int.Map.mapi f.map m
+
+    type any = Any : 'a tag * 'a M.t -> 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
+  end
 end
 include Self
 
 module Easy = struct
-
-(* now tags are opaque, we can do the trick *)
-let make_dyn_tag (s : string) =
- (fun (type a) (tag : a tag) ->
-  let infun : (a -> t) = fun x -> Dyn (tag, x) in
-  let outfun : (t -> a) = fun (Dyn (t, x)) ->
-    match eq tag t with
-    | None -> assert false
-    | Some CSig.Refl -> x
-  in
-  infun, outfun, tag)
- (create s)
-
-let make_dyn (s : string) =
-  let inf, outf, _ = make_dyn_tag s in inf, outf
-
-let inj x tag = Dyn(tag,x)
-let prj : type a. t -> a tag -> a option =
+  (* now tags are opaque, we can do the trick *)
+  let make_dyn_tag (s : string) =
+   (fun (type a) (tag : a tag) ->
+    let infun : (a -> t) = fun x -> Dyn (tag, x) in
+    let outfun : (t -> a) = fun (Dyn (t, x)) ->
+      match eq tag t with
+      | None -> assert false
+      | Some CSig.Refl -> x
+    in
+    infun, outfun, tag)
+   (create s)
+
+  let make_dyn (s : string) =
+    let inf, outf, _ = make_dyn_tag s in inf, outf
+
+  let inj x tag = Dyn(tag,x)
+  let prj : type a. t -> a tag -> a option =
     fun (Dyn(tag',x)) tag ->
-    match eq tag tag' with
-    | None -> None
-    | Some CSig.Refl -> Some x
+      match eq tag tag' with
+      | None -> None
+      | Some CSig.Refl -> Some x
 end
 
 end
diff --git a/clib/dyn.mli b/clib/dyn.mli
index 51d3091429..7077e1d32e 100644
--- a/clib/dyn.mli
+++ b/clib/dyn.mli
@@ -26,43 +26,38 @@ sig
   val find : 'a key -> t -> 'a obj
   val mem : 'a key -> t -> bool
 
-  type any = Any : 'a key * 'a obj -> any
-
   type map = { map : 'a. 'a key -> 'a obj -> 'a obj }
   val map : map -> t -> t
 
+  type any = Any : 'a key * 'a obj -> any
   val iter : (any -> unit) -> t -> unit
   val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
 end
 
 module type S =
 sig
-type 'a tag
-type t = Dyn : 'a tag * 'a -> t
-
-val create : string -> 'a tag
-val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
-val repr : 'a tag -> string
+  type 'a tag
+  type t = Dyn : 'a tag * 'a -> t
+  val create : string -> 'a tag
+  val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
+  val repr : 'a tag -> string
 
-type any = Any : 'a tag -> any
+  val dump : unit -> (int * string) list
 
-val name : string -> any option
+  type any = Any : 'a tag -> any
+  val name : string -> any option
 
-module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag
+  module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag
 
-val dump : unit -> (int * string) list
-
-module Easy : sig
-
-  (* To create a dynamic type on the fly *)
-  val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag
-  val make_dyn : string -> ('a -> t) * (t -> 'a)
-
-  (* For types declared with the [create] function above *)
-  val inj : 'a -> 'a tag -> t
-  val prj : t -> 'a tag -> 'a option
-end
+  module Easy : sig
+    (* To create a dynamic type on the fly *)
+    val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag
+    val make_dyn : string -> ('a -> t) * (t -> 'a)
 
+    (* For types declared with the [create] function above *)
+    val inj : 'a -> 'a tag -> t
+    val prj : t -> 'a tag -> 'a option
+  end
 end
 
 module Make () : S
-- 
cgit v1.2.3


From 0f6762ac80cc8d1f37918e9e8f0bb39692979630 Mon Sep 17 00:00:00 2001
From: whitequark
Date: Thu, 21 Jun 2018 02:34:33 +0000
Subject: Rename Dyn.TParam→ValueS, Dyn.MapS.obj→value to clarify their
 purpose.

---
 clib/dyn.ml             | 27 ++++++++++++++-------------
 clib/dyn.mli            | 15 ++++++++-------
 pretyping/geninterp.mli |  4 ++--
 3 files changed, 24 insertions(+), 22 deletions(-)

diff --git a/clib/dyn.ml b/clib/dyn.ml
index 7cdbf15a44..6c45767246 100644
--- a/clib/dyn.ml
+++ b/clib/dyn.ml
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-module type TParam =
+module type ValueS =
 sig
   type 'a t
 end
@@ -16,18 +16,18 @@ end
 module type MapS =
 sig
   type t
-  type 'a obj
   type 'a key
+  type 'a value
   val empty : t
-  val add : 'a key -> 'a obj -> t -> t
+  val add : 'a key -> 'a value -> t -> t
   val remove : 'a key -> t -> t
-  val find : 'a key -> t -> 'a obj
+  val find : 'a key -> t -> 'a value
   val mem : 'a key -> t -> bool
 
-  type map = { map : 'a. 'a key -> 'a obj -> 'a obj }
+  type map = { map : 'a. 'a key -> 'a value -> 'a value }
   val map : map -> t -> t
 
-  type any = Any : 'a key * 'a obj -> any
+  type any = Any : 'a key * 'a value -> any
   val iter : (any -> unit) -> t -> unit
   val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
 end
@@ -46,7 +46,8 @@ sig
   type any = Any : 'a tag -> any
   val name : string -> any option
 
-  module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag
+  module Map(Value : ValueS) :
+    MapS with type 'a key = 'a tag and type 'a value = 'a Value.t
 end
 
 module type S =
@@ -104,22 +105,22 @@ module Self : PreS = struct
 
   let dump () = Int.Map.bindings !dyntab
 
-  module Map(M : TParam) =
+  module Map(Value: ValueS) =
   struct
-    type t = Obj.t M.t Int.Map.t
-    type 'a obj = 'a M.t
+    type t = Obj.t Value.t Int.Map.t
     type 'a key = 'a tag
-    let cast : 'a M.t -> 'b M.t = Obj.magic
+    type 'a value = 'a Value.t
+    let cast : 'a value -> 'b value = Obj.magic
     let empty = Int.Map.empty
     let add tag v m = Int.Map.add tag (cast v) m
     let remove tag m = Int.Map.remove tag m
     let find tag m = cast (Int.Map.find tag m)
     let mem = Int.Map.mem
 
-    type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t }
+    type map = { map : 'a. 'a tag -> 'a value -> 'a value }
     let map f m = Int.Map.mapi f.map m
 
-    type any = Any : 'a tag * 'a M.t -> any
+    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
   end
diff --git a/clib/dyn.mli b/clib/dyn.mli
index 7077e1d32e..28dac5d6c9 100644
--- a/clib/dyn.mli
+++ b/clib/dyn.mli
@@ -10,7 +10,7 @@
 
 (** Dynamically typed values *)
 
-module type TParam =
+module type ValueS =
 sig
   type 'a t
 end
@@ -18,18 +18,18 @@ end
 module type MapS =
 sig
   type t
-  type 'a obj
   type 'a key
+  type 'a value
   val empty : t
-  val add : 'a key -> 'a obj -> t -> t
+  val add : 'a key -> 'a value -> t -> t
   val remove : 'a key -> t -> t
-  val find : 'a key -> t -> 'a obj
+  val find : 'a key -> t -> 'a value
   val mem : 'a key -> t -> bool
 
-  type map = { map : 'a. 'a key -> 'a obj -> 'a obj }
+  type map = { map : 'a. 'a key -> 'a value -> 'a value }
   val map : map -> t -> t
 
-  type any = Any : 'a key * 'a obj -> any
+  type any = Any : 'a key * 'a value -> any
   val iter : (any -> unit) -> t -> unit
   val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
 end
@@ -47,7 +47,8 @@ sig
   type any = Any : 'a tag -> any
   val name : string -> any option
 
-  module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag
+  module Map(Value : ValueS) :
+    MapS with type 'a key = 'a tag and type 'a value = 'a Value.t
 
   module Easy : sig
     (* To create a dynamic type on the fly *)
diff --git a/pretyping/geninterp.mli b/pretyping/geninterp.mli
index fa522e9c34..606a6ebead 100644
--- a/pretyping/geninterp.mli
+++ b/pretyping/geninterp.mli
@@ -42,8 +42,8 @@ sig
 
 end
 
-module ValTMap (M : Dyn.TParam) :
-  Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ
+module ValTMap (Value : Dyn.ValueS) :
+  Dyn.MapS with type 'a key = 'a Val.typ and type 'a value = 'a Value.t
 
 (** Dynamic types for toplevel values. While the generic types permit to relate
     objects at various levels of interpretation, toplevel values are wearing
-- 
cgit v1.2.3


From d8dd112aeea7b615bee416ee3ae18149b839b519 Mon Sep 17 00:00:00 2001
From: whitequark
Date: Thu, 21 Jun 2018 02:46:16 +0000
Subject: Add documentation for Dyn.

---
 clib/dyn.mli | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/clib/dyn.mli b/clib/dyn.mli
index 28dac5d6c9..ff9762bd6b 100644
--- a/clib/dyn.mli
+++ b/clib/dyn.mli
@@ -37,18 +37,37 @@ end
 module type S =
 sig
   type 'a tag
+  (** Type of dynamic tags *)
+
   type t = Dyn : 'a tag * 'a -> t
+  (** Type of dynamic values *)
+
   val create : string -> 'a tag
+  (** [create n] returns a tag describing a type called [n].
+      [create] raises an exception if [n] is already registered.
+      Type names are hashed, so [create] may raise even if no type with
+      the exact same name was registered due to a collision. *)
+
   val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
+  (** [eq t1 t2] returns [Some witness] if [t1] is the same as [t2], [None] otherwise. *)
+
   val repr : 'a tag -> string
+  (** [repr tag] returns the name of the type represented by [tag]. *)
 
   val dump : unit -> (int * string) list
+  (** [dump ()] returns a list of (tag, name) pairs for every type tag registered
+      in this [Dyn.Make] instance. *)
 
   type any = Any : 'a tag -> any
+  (** Type of boxed dynamic tags *)
+
   val name : string -> any option
+  (** [name n] returns [Some t] where t is a boxed tag previously registered
+      with [create n], or [None] if there is no such tag. *)
 
   module Map(Value : ValueS) :
     MapS with type 'a key = 'a tag and type 'a value = 'a Value.t
+  (** Map from type tags to values parameterized by the tag type *)
 
   module Easy : sig
     (* To create a dynamic type on the fly *)
-- 
cgit v1.2.3