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 --- contrib/ring/ring.ml | 4 ++-- library/declare.ml | 16 ++++++++-------- library/goptions.ml | 12 ++++++------ library/impargs.ml | 2 +- library/lib.ml | 11 +++++++---- library/libobject.ml | 17 +++++++++-------- library/libobject.mli | 5 +++-- pretyping/classops.ml | 4 ++-- pretyping/recordops.ml | 6 +++--- pretyping/syntax_def.ml | 2 +- proofs/macros.ml | 4 ++-- proofs/tacinterp.ml | 8 ++++---- tactics/auto.ml | 4 ++-- tactics/dhyp.ml | 4 ++-- tactics/equality.ml | 4 ++-- toplevel/metasyntax.ml | 8 ++++---- toplevel/mltop.ml4 | 4 ++-- 17 files changed, 60 insertions(+), 55 deletions(-) diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index f82cb6417..2a817668e 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -145,12 +145,12 @@ let _ = let (theory_to_obj, obj_to_theory) = let cache_th (_,(c, th)) = theories_map_add (c,th) - and spec_th x = x in + and export_th x = Some x in declare_object ("tactic-ring-theory", { load_function = (fun _ -> ()); open_function = cache_th; cache_function = cache_th; - specification_function = spec_th }) + export_function = export_th }) (* from the set A, guess the associated theory *) (* With this simple solution, the theory to use is automatically guessed *) 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 + diff --git a/pretyping/classops.ml b/pretyping/classops.ml index b4274e9fe..306f2b8ce 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -173,7 +173,7 @@ let (inClass,outClass) = { load_function = (fun _ -> ()); open_function = cache_class; cache_function = cache_class; - specification_function = (function x -> x) }) + export_function = (function x -> Some x) }) let add_new_class (cl,s,stre,p) = Lib.add_anonymous_leaf (inClass ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p}))) @@ -324,4 +324,4 @@ let (inCoercion,outCoercion) = { load_function = (fun _ -> ()); open_function = cache_coercion; cache_function = cache_coercion; - specification_function = (function x -> x) }) + export_function = (function x -> Some x) }) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index b3b0af463..45b16c935 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -38,7 +38,7 @@ let (inStruc,outStruc) = { load_function = (fun _ -> ()); cache_function = cache_structure; open_function = cache_structure; - specification_function = (function x -> x) }) + export_function = (function x -> Some x) }) let add_new_struc (s,c,n,l) = Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l})) @@ -72,7 +72,7 @@ let (inObjDef,outObjDef) = { load_function = (fun _ -> ()); open_function = cache_obj; cache_function = cache_obj; - specification_function = (function x -> x)}) + export_function = (function x -> Some x)}) let add_new_objdef (o,c,la,lp,l) = try @@ -88,7 +88,7 @@ let ((inObjDef1 : section_path -> obj),(outObjDef1 : obj -> section_path)) = { load_function = (fun _ -> ()); open_function = cache_objdef1; cache_function = cache_objdef1; - specification_function = (function x -> x)}) + export_function = (function x -> Some x)}) let objdef_info o = List.assoc o !oBJDEFS diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml index 736a2be67..00ed971c1 100644 --- a/pretyping/syntax_def.ml +++ b/pretyping/syntax_def.ml @@ -31,7 +31,7 @@ let (in_syntax_constant, out_syntax_constant) = cache_function = cache_syntax_constant; load_function = (fun _ -> ()); open_function = cache_syntax_constant; - specification_function = (fun x -> x) } + export_function = (fun x -> Some x) } in declare_object ("SYNTAXCONSTANT", od) diff --git a/proofs/macros.ml b/proofs/macros.ml index 92cc8cf41..4a7a826f9 100644 --- a/proofs/macros.ml +++ b/proofs/macros.ml @@ -39,12 +39,12 @@ let _ = let (inMD,outMD) = let add (na,md) = mactab := Stringmap.add na md !mactab in let cache_md (_,(na,md)) = add (na,md) in - let specification_md x = x in + let export_md x = Some x in declare_object ("TACTIC-MACRO-DATA", { cache_function = cache_md; load_function = (fun _ -> ()); open_function = cache_md; - specification_function = specification_md }) + export_function = export_md }) let add_macro_hint na (ids,body) = if Stringmap.mem na !mactab then errorlabstrm "add_macro_hint" diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 72593da36..f45d896d4 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -944,10 +944,10 @@ let (inMD,outMD) = let ve=val_interp (Evd.empty,Environ.empty_env,[],[],None,get_debug ()) td in add (na,ve) in declare_object ("TACTIC-DEFINITION", - {cache_function = cache_md; - load_function = (fun _ -> ()); - open_function = cache_md; - specification_function = (fun x -> x)}) + {cache_function = cache_md; + load_function = (fun _ -> ()); + open_function = cache_md; + export_function = (fun x -> Some x)}) (* Adds a Tactic Definition in the table *) let add_tacdef na vbody = diff --git a/tactics/auto.ml b/tactics/auto.ml index 32c256ad3..10de3ab49 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -163,14 +163,14 @@ let add_hint dbname hintlist = let cache_autohint (_,(name,hintlist)) = try add_hint name hintlist with _ -> anomaly "Auto.add_hint" -let specification_autohint x = x +let export_autohint x = Some x let (inAutoHint,outAutoHint) = declare_object ("AUTOHINT", { load_function = (fun _ -> ()); cache_function = cache_autohint; open_function = cache_autohint; - specification_function = specification_autohint }) + export_function = export_autohint }) (**************************************************************************) (* The "Hint" vernacular command *) diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 938ead22f..628c337f9 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -187,7 +187,7 @@ let cache_dd (_,(na,dd)) = [< 'sTR"The code which adds destructor hints broke;"; 'sPC; 'sTR"this is not supposed to happen" >] -let specification_dd x = x +let export_dd x = Some x type destructor_data_object = identifier * destructor_data @@ -197,7 +197,7 @@ let ((inDD : destructor_data_object->obj), { load_function = (fun _ -> ()); cache_function = cache_dd; open_function = cache_dd; - specification_function = specification_dd }) + export_function = export_dd }) let add_destructor_hint na pat pri code = Lib.add_anonymous_leaf diff --git a/tactics/equality.ml b/tactics/equality.ml index 3943cc07e..6d1cc5a69 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1583,7 +1583,7 @@ let rules_of_base rbase = List.rev (Gmapl.find rbase !rew_tab) (*Functions necessary to the library object declaration*) let load_autorewrite_rule _ = () let cache_autorewrite_rule (_,(rbase,lrl)) = add_list_rules rbase lrl -let specification_autorewrite_rule x = x +let export_autorewrite_rule x = Some x (*Declaration of the AUTOREWRITE_RULE library object*) let (in_autorewrite_rule,out_autorewrite_rule)= @@ -1592,7 +1592,7 @@ let (in_autorewrite_rule,out_autorewrite_rule)= { Libobject.load_function = load_autorewrite_rule; Libobject.open_function = cache_autorewrite_rule; Libobject.cache_function = cache_autorewrite_rule; - Libobject.specification_function = specification_autorewrite_rule }) + Libobject.export_function = export_autorewrite_rule }) (* Semantic of the HintRewrite vernacular command *) let _ = diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 78481ca1e..4a4c92531 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -49,7 +49,7 @@ let (inPPSyntax,outPPSyntax) = { load_function = (fun _ -> ()); open_function = cache_syntax; cache_function = cache_syntax; - specification_function = (fun x -> x) }) + export_function = (fun x -> Some x) }) (* Syntax extension functions (registered in the environnement) *) @@ -81,7 +81,7 @@ let (inToken, outToken) = { load_function = (fun _ -> ()); open_function = cache_token; cache_function = cache_token; - specification_function = (fun x -> x)}) + export_function = (fun x -> Some x)}) let add_token_obj s = Lib.add_anonymous_leaf (inToken s) @@ -94,7 +94,7 @@ let (inGrammar, outGrammar) = { load_function = (fun _ -> ()); open_function = cache_grammar; cache_function = cache_grammar; - specification_function = (fun x -> x)}) + export_function = (fun x -> Some x)}) let add_grammar_obj univ al = Lib.add_anonymous_leaf (inGrammar (Extend.interp_grammar_command univ al)) @@ -139,7 +139,7 @@ let (inInfix, outInfix) = { load_function = (fun _ -> ()); open_function = cache_infix; cache_function = cache_infix; - specification_function = (fun x -> x)}) + export_function = (fun x -> Some x)}) let prec_assoc = function | Some(Gramext.RightA) -> (":L",":E") diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 66577bea6..7d0761771 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -221,14 +221,14 @@ let cache_ml_module_object (_,{mnames=mnames}) = add_loaded_module mname) mnames -let specification_ml_module_object x = x +let export_ml_module_object x = Some x let (inMLModule,outMLModule) = declare_object ("ML-MODULE", { load_function = cache_ml_module_object; cache_function = cache_ml_module_object; open_function = (fun _ -> ()); - specification_function = specification_ml_module_object }) + export_function = export_ml_module_object }) let declare_ml_modules l = Lib.add_anonymous_leaf (inMLModule {mnames=l}) -- cgit v1.2.3