aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-29 01:17:22 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-09 18:06:36 +0100
commitdea662ae5fd7225c06392e1b3f5acb1cd8e97e91 (patch)
tree492c69afb526eaa0cc79debff2280017874820cd /lib
parent319a3c230e9f9ec5a8a5bea9e07b6b8d17444ac9 (diff)
[lib] Convenience function for `Dyn.Easy`
Diffstat (limited to 'lib')
-rw-r--r--lib/dyn.ml10
-rw-r--r--lib/dyn.mli1
2 files changed, 9 insertions, 2 deletions
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 83e673d2c..64535d35f 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -55,6 +55,8 @@ 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
@@ -129,8 +131,9 @@ end
include Self
module Easy = struct
+
(* now tags are opaque, we can do the trick *)
-let make_dyn (s : string) =
+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)) ->
@@ -138,9 +141,12 @@ let make_dyn (s : string) =
| None -> assert false
| Some CSig.Refl -> x
in
- (infun, outfun))
+ 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 ->
diff --git a/lib/dyn.mli b/lib/dyn.mli
index e0e1a9d14..2206394e2 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -53,6 +53,7 @@ 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 *)