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 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: libobject.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
open Util
open Names
open Libnames
open Mod_subst
(* The relax flag is used to make it possible to load files while ignoring
failures to incorporate some objects. This can be useful when one
wants to work with restricted Coq programs that have only parts of
the full capabilities, but may still be able to work correctly for
limited purposes. One example is for the graphical interface, that uses
such a limite coq process to do only parsing. It loads .vo files, but
is only interested in loading the grammar rule definitions. *)
let relax_flag = ref false;;
let relax b = relax_flag := b;;
type 'a substitutivity =
Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
type 'a object_declaration = {
object_name : string;
cache_function : object_name * 'a -> unit;
load_function : int -> object_name * 'a -> unit;
open_function : int -> object_name * 'a -> unit;
classify_function : object_name * 'a -> 'a substitutivity;
subst_function : object_name * substitution * 'a -> 'a;
discharge_function : object_name * 'a -> 'a option;
rebuild_function : 'a -> 'a;
export_function : 'a -> 'a option }
let yell s = anomaly s
let default_object s = {
object_name = s;
cache_function = (fun _ -> ());
load_function = (fun _ _ -> ());
open_function = (fun _ _ -> ());
subst_function = (fun _ ->
yell ("The object "^s^" does not know how to substitute!"));
classify_function = (fun (_,obj) -> Keep obj);
discharge_function = (fun _ -> None);
rebuild_function = (fun x -> x);
export_function = (fun _ -> None)}
(* The suggested object declaration is the following:
declare_object { (default_object "MY OBJECT") with
cache_function = fun (sp,a) -> Mytbl.add sp a}
and the listed functions are only those which definitions accually
differ from the default.
This helps introducing new functions in objects.
*)
let ident_subst_function (_,_,a) = a
type obj = Dyn.t (* persistent dynamic objects *)
type dynamic_object_declaration = {
dyn_cache_function : object_name * obj -> unit;
dyn_load_function : int -> object_name * obj -> unit;
dyn_open_function : int -> object_name * obj -> unit;
dyn_subst_function : object_name * substitution * obj -> obj;
dyn_classify_function : object_name * obj -> obj substitutivity;
dyn_discharge_function : object_name * obj -> obj option;
dyn_rebuild_function : obj -> obj;
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 odecl =
let na = odecl.object_name in
let (infun,outfun) = Dyn.create na in
let cacher (oname,lobj) =
if Dyn.tag lobj = na then odecl.cache_function (oname,outfun lobj)
else anomaly "somehow we got the wrong dynamic object in the cachefun"
and loader i (oname,lobj) =
if Dyn.tag lobj = na then odecl.load_function i (oname,outfun lobj)
else anomaly "somehow we got the wrong dynamic object in the loadfun"
and opener i (oname,lobj) =
if Dyn.tag lobj = na then odecl.open_function i (oname,outfun lobj)
else anomaly "somehow we got the wrong dynamic object in the openfun"
and substituter (oname,sub,lobj) =
if Dyn.tag lobj = na then
infun (odecl.subst_function (oname,sub,outfun lobj))
else anomaly "somehow we got the wrong dynamic object in the substfun"
and classifier (spopt,lobj) =
if Dyn.tag lobj = na then
match odecl.classify_function (spopt,outfun lobj) with
| Dispose -> Dispose
| Substitute obj -> Substitute (infun obj)
| Keep obj -> Keep (infun obj)
| Anticipate (obj) -> Anticipate (infun obj)
else
anomaly "somehow we got the wrong dynamic object in the classifyfun"
and discharge (oname,lobj) =
if Dyn.tag lobj = na then
Option.map infun (odecl.discharge_function (oname,outfun lobj))
else
anomaly "somehow we got the wrong dynamic object in the dischargefun"
and rebuild lobj =
if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj))
else anomaly "somehow we got the wrong dynamic object in the rebuildfun"
and exporter lobj =
if Dyn.tag lobj = na then
Option.map infun (odecl.export_function (outfun lobj))
else
anomaly "somehow we got the wrong dynamic object in the exportfun"
in
Hashtbl.add cache_tab na { dyn_cache_function = cacher;
dyn_load_function = loader;
dyn_open_function = opener;
dyn_subst_function = substituter;
dyn_classify_function = classifier;
dyn_discharge_function = discharge;
dyn_rebuild_function = rebuild;
dyn_export_function = exporter };
(infun,outfun)
(* this function describes how the cache, load, open, and export functions
are triggered. In relaxed mode, this function just return a meaningless
value instead of raising an exception when they fail. *)
let apply_dyn_fun deflt f lobj =
let tag = object_tag lobj in
try
let dodecl =
try
Hashtbl.find cache_tab tag
with Not_found ->
if !relax_flag then
failwith "local to_apply_dyn_fun"
else
error
("Cannot find library functions for an object with tag "^tag^
" (maybe a plugin is missing)") in
f dodecl
with
Failure "local to_apply_dyn_fun" -> deflt;;
let cache_object ((_,lobj) as node) =
apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj
let load_object i ((_,lobj) as node) =
apply_dyn_fun () (fun d -> d.dyn_load_function i node) lobj
let open_object i ((_,lobj) as node) =
apply_dyn_fun () (fun d -> d.dyn_open_function i node) lobj
let subst_object ((_,_,lobj) as node) =
apply_dyn_fun lobj (fun d -> d.dyn_subst_function node) lobj
let classify_object ((_,lobj) as node) =
apply_dyn_fun Dispose (fun d -> d.dyn_classify_function node) lobj
let discharge_object ((_,lobj) as node) =
apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj
let rebuild_object (lobj as node) =
apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function node) lobj
let export_object lobj =
apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj
|