diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-29 01:17:22 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-09 18:06:36 +0100 |
commit | dea662ae5fd7225c06392e1b3f5acb1cd8e97e91 (patch) | |
tree | 492c69afb526eaa0cc79debff2280017874820cd /lib | |
parent | 319a3c230e9f9ec5a8a5bea9e07b6b8d17444ac9 (diff) |
[lib] Convenience function for `Dyn.Easy`
Diffstat (limited to 'lib')
-rw-r--r-- | lib/dyn.ml | 10 | ||||
-rw-r--r-- | lib/dyn.mli | 1 |
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 *) |