diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-12-12 11:16:31 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-12 11:16:31 +0100 |
commit | 3200d6a890dfea363a6f39b856023b6a1c1dae5c (patch) | |
tree | 189089a1c29139172a47516bf0f2b85108abd973 /lib | |
parent | 3a56a7f7ec35286360fef5a661634a86c5a13daf (diff) | |
parent | 5676b113920fb48d4898817d6c0ce3353b06107f (diff) |
Merge PR #6275: [summary] Allow typed projections from global state.
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 *) |