From b2c9129662f55eea46a8937f9fd0cfabc029457a Mon Sep 17 00:00:00 2001 From: filliatr Date: Wed, 15 Nov 2000 07:56:21 +0000 Subject: methode export git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@851 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declare.ml | 16 ++++++++-------- library/goptions.ml | 12 ++++++------ library/impargs.ml | 2 +- library/lib.ml | 11 +++++++---- library/libobject.ml | 17 +++++++++-------- library/libobject.mli | 5 +++-- 6 files changed, 34 insertions(+), 29 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 49d684ed6..72f16f48f 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -67,14 +67,14 @@ let load_variable _ = () let open_variable _ = () -let specification_variable x = x +let export_variable x = None let (in_variable, out_variable) = let od = { cache_function = cache_variable; load_function = load_variable; open_function = open_variable; - specification_function = specification_variable } in + export_function = export_variable } in declare_object ("VARIABLE", od) let out_variable sp = fst (out_variable sp) @@ -96,14 +96,14 @@ let load_parameter (sp,(_,imps)) = let open_parameter (sp,_) = Nametab.push (basename sp) sp -let specification_parameter obj = obj +let export_parameter obj = Some obj let (in_parameter, out_parameter) = let od = { cache_function = cache_parameter; load_function = load_parameter; open_function = open_parameter; - specification_function = specification_parameter } + export_function = export_parameter } in declare_object ("PARAMETER", od) @@ -141,14 +141,14 @@ let load_constant (sp,((ce,stre),imps)) = let open_constant (sp,_) = Nametab.push (basename sp) sp -let specification_constant obj = obj +let export_constant obj = Some obj let (in_constant, out_constant) = let od = { cache_function = cache_constant; load_function = load_constant; open_function = open_constant; - specification_function = specification_constant } + export_function = export_constant } in declare_object ("CONSTANT", od) @@ -176,14 +176,14 @@ let load_inductive (sp,(_,imps)) = let open_inductive (sp,(mie,_)) = push_inductive_names sp mie -let specification_inductive obj = obj +let export_inductive obj = Some obj let (in_inductive, out_inductive) = let od = { cache_function = cache_inductive; load_function = load_inductive; open_function = open_inductive; - specification_function = specification_inductive } + export_function = export_inductive } in declare_object ("INDUCTIVE", od) diff --git a/library/goptions.ml b/library/goptions.ml index ad0b844be..64b08f6f4 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -85,13 +85,13 @@ module MakeTable = let cache_options (_,(f,p)) = match f with | GOadd -> t := MySet.add p !t | GOrmv -> t := MySet.remove p !t in - let specification_options fp = fp in + let export_options fp = Some fp in let (inGo,outGo) = Libobject.declare_object (kn, { Libobject.load_function = load_options; Libobject.open_function = cache_options; Libobject.cache_function = cache_options; - Libobject.specification_function = specification_options}) in + Libobject.export_function = export_options}) in ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))), (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c)))) else @@ -204,13 +204,13 @@ let async_value_tab = ref OptionMap.empty let load_sync_value _ = () let cache_sync_value (_,(k,v)) = sync_value_tab := OptionMap.add k v !sync_value_tab -let spec_sync_value fp = fp +let export_sync_value fp = Some fp let (inOptVal,_) = - Libobject.declare_object ("Sync_option_value", - {Libobject.load_function = load_sync_value; + Libobject.declare_object ("Sync_option_value", + { Libobject.load_function = load_sync_value; Libobject.open_function = cache_sync_value; Libobject.cache_function = cache_sync_value; - Libobject.specification_function = spec_sync_value}) + Libobject.export_function = export_sync_value }) let freeze_sync_table () = !sync_value_tab let unfreeze_sync_table l = sync_value_tab := l diff --git a/library/impargs.ml b/library/impargs.ml index b479dc5b9..c9fa33e24 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -123,7 +123,7 @@ let is_implicit_inductive_definition sp = let is_implicit_var id = try let _ = Idmap.find id !var_table in true with Not_found -> false -(* Registration as global tables and roolback. *) +(* Registration as global tables and rollback. *) type frozen_t = bool * implicits Spmap.t diff --git a/library/lib.ml b/library/lib.ml index 74986d6fe..3a502d42e 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -151,12 +151,15 @@ let close_section s = let export_module () = if !module_name = None then error "no module declared"; let rec clean acc = function - | (_,Module _) :: _ -> acc - | (_,Leaf _) as node :: stk -> clean (node::acc) stk - | (_,ClosedSection _) as node :: stk -> clean (node::acc) stk + | (_,Module _) :: _ | [] -> acc + | (sp,Leaf o) as node :: stk -> + (match export_object o with + | None -> clean acc stk + | Some o' -> clean ((sp,Leaf o') :: acc) stk) + | (sp,ClosedSection (s,ctx)) :: stk -> + clean ((sp,ClosedSection (s, clean [] ctx)) :: acc) stk | (_,OpenedSection _) :: _ -> error "there are still opened sections" | (_,FrozenState _) :: stk -> clean acc stk - | _ -> assert false in clean [] !lib_stk diff --git a/library/libobject.ml b/library/libobject.ml index 1eb7aea0e..c644cc4eb 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -8,7 +8,7 @@ type 'a object_declaration = { cache_function : section_path * 'a -> unit; load_function : section_path * 'a -> unit; open_function : section_path * 'a -> unit; - specification_function : 'a -> 'a } + export_function : 'a -> 'a option } type obj = Dyn.t (* persistent dynamic objects *) @@ -16,7 +16,7 @@ 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_specification_function : obj -> obj } + dyn_export_function : obj -> obj option } let object_tag lobj = Dyn.tag lobj @@ -34,13 +34,13 @@ let declare_object (na,odecl) = 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 spec_extractor lobj = - infun(odecl.specification_function (outfun lobj)) + 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_specification_function = spec_extractor }; + dyn_export_function = exporter }; (infun,outfun) let apply_dyn_fun f lobj = @@ -50,7 +50,8 @@ let apply_dyn_fun f lobj = Hashtbl.find cache_tab tag with Not_found -> anomaly ("Cannot find library functions for an object with tag "^tag) - in f dodecl + in + f dodecl let cache_object ((_,lobj) as node) = apply_dyn_fun (fun d -> d.dyn_cache_function node) lobj @@ -61,5 +62,5 @@ let load_object ((_,lobj) as node) = let open_object ((_,lobj) as node) = apply_dyn_fun (fun d -> d.dyn_open_function node) lobj -let extract_object_specification lobj = - apply_dyn_fun (fun d -> d.dyn_specification_function lobj) lobj +let export_object lobj = + apply_dyn_fun (fun d -> d.dyn_export_function lobj) lobj diff --git a/library/libobject.mli b/library/libobject.mli index d855059fa..17a221a66 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -19,7 +19,7 @@ type 'a object_declaration = { cache_function : section_path * 'a -> unit; load_function : section_path * 'a -> unit; open_function : section_path * 'a -> unit; - specification_function : 'a -> 'a } + export_function : 'a -> 'a option } (*s Given an object name and a declaration, the function [declare_object] will hand back two functions, the "injection" and "projection" @@ -35,4 +35,5 @@ val object_tag : obj -> string val cache_object : section_path * obj -> unit val load_object : section_path * obj -> unit val open_object : section_path * obj -> unit -val extract_object_specification : obj -> obj +val export_object : obj -> obj option + -- cgit v1.2.3