diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-05 12:53:20 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-05 13:38:14 +0100 |
commit | 895d34a264d9d90adfe4f0618c3bb0663dc01615 (patch) | |
tree | da8406b2fd882318c8264487596f2aca0e5f9f2a /library/libobject.ml | |
parent | 8596423ed6345495ca5ec0aedb8a9a431bee2e5d (diff) |
Leveraging GADTs to provide a better Dyn API.
Diffstat (limited to 'library/libobject.ml')
-rw-r--r-- | library/libobject.ml | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/library/libobject.ml b/library/libobject.ml index c63875907..f0d281a2d 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -8,6 +8,7 @@ open Libnames open Pp +open Util module Dyn = Dyn.Make(struct end) @@ -72,15 +73,25 @@ type dynamic_object_declaration = { dyn_discharge_function : object_name * obj -> obj option; dyn_rebuild_function : obj -> obj } -let object_tag = Dyn.tag -let object_has_tag = Dyn.has_tag +let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t let cache_tab = (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) +let make_dyn (type a) (tag : a Dyn.tag) = + let infun x = Dyn.Dyn (tag, x) in + let outfun : (Dyn.t -> a) = fun dyn -> + let Dyn.Dyn (t, x) = dyn in + match Dyn.eq t tag with + | None -> assert false + | Some Refl -> x + in + (infun, outfun) + let declare_object_full odecl = let na = odecl.object_name in - let (infun,outfun) = Dyn.create na in + let tag = Dyn.create na in + let (infun, outfun) = make_dyn tag in let cacher (oname,lobj) = odecl.cache_function (oname,outfun lobj) and loader i (oname,lobj) = odecl.load_function i (oname,outfun lobj) and opener i (oname,lobj) = odecl.open_function i (oname,outfun lobj) |