1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
open Util
open Names
type 'a object_declaration = {
cache_function : section_path * 'a -> unit;
load_function : section_path * 'a -> unit;
open_function : section_path * 'a -> unit;
export_function : 'a -> 'a option }
type obj = Dyn.t (* persistent dynamic objects *)
type dynamic_object_declaration = {
dyn_cache_function : section_path * obj -> unit;
dyn_load_function : section_path * obj -> unit;
dyn_open_function : section_path * obj -> unit;
dyn_export_function : obj -> obj option }
let object_tag lobj = Dyn.tag lobj
let cache_tab =
(Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t)
let declare_object (na,odecl) =
let (infun,outfun) = Dyn.create na in
let cacher (spopt,lobj) =
if Dyn.tag lobj = na then odecl.cache_function(spopt,outfun lobj)
else anomaly "somehow we got the wrong dynamic object in the cachefun"
and loader (spopt,lobj) =
if Dyn.tag lobj = na then odecl.load_function (spopt,outfun lobj)
else anomaly "somehow we got the wrong dynamic object in the loadfun"
and opener (spopt,lobj) =
if Dyn.tag lobj = na then odecl.open_function (spopt,outfun lobj)
else anomaly "somehow we got the wrong dynamic object in the openfun"
and exporter lobj =
option_app infun (odecl.export_function (outfun lobj))
in
Hashtbl.add cache_tab na { dyn_cache_function = cacher;
dyn_load_function = loader;
dyn_open_function = opener;
dyn_export_function = exporter };
(infun,outfun)
let apply_dyn_fun f lobj =
let tag = object_tag lobj in
let dodecl =
try
Hashtbl.find cache_tab tag
with Not_found ->
anomaly ("Cannot find library functions for an object with tag "^tag)
in
f dodecl
let cache_object ((_,lobj) as node) =
apply_dyn_fun (fun d -> d.dyn_cache_function node) lobj
let load_object ((_,lobj) as node) =
apply_dyn_fun (fun d -> d.dyn_load_function node) lobj
let open_object ((_,lobj) as node) =
apply_dyn_fun (fun d -> d.dyn_open_function node) lobj
let export_object lobj =
apply_dyn_fun (fun d -> d.dyn_export_function lobj) lobj
|
