From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 8 Aug 2008 13:18:42 +0200 Subject: Imported Upstream version 8.2~beta4+dfsg --- library/declare.ml | 14 +++--- library/declaremods.ml | 10 ++-- library/heads.ml | 4 +- library/impargs.ml | 133 ++++++++++++++++++++++++++++++++++--------------- library/impargs.mli | 48 ++++++++++++++++-- library/lib.ml | 51 ++++++++++++------- library/lib.mli | 21 +++++--- library/libnames.ml | 4 +- library/libnames.mli | 3 +- library/libobject.ml | 16 +++--- library/libobject.mli | 8 ++- library/library.ml | 116 +++++++++++++++++++++++++++--------------- library/library.mli | 10 ++-- library/states.ml | 11 ++-- 14 files changed, 302 insertions(+), 147 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 07810e3c..4bdc11c3 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: declare.ml 10840 2008-04-23 21:29:34Z herbelin $ *) +(* $Id: declare.ml 11282 2008-07-28 11:51:53Z msozeau $ *) (** This module is about the low-level declaration of logical objects *) @@ -57,10 +57,12 @@ let cache_variable ((sp,_),o) = let impl,opaq,cst,keep = match d with (* Fails if not well-typed *) | SectionLocalAssum (ty, impl, keep) -> let cst = Global.push_named_assum (id,ty) in - impl, true, cst, (if keep then Some ty else None) + let impl = if impl then Lib.Implicit else Lib.Explicit in + let keep = if keep then Some ty else None in + impl, true, cst, keep | SectionLocalDef (c,t,opaq) -> let cst = Global.push_named_def (id,c,t) in - false, opaq, cst, None in + Lib.Explicit, opaq, cst, None in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); add_section_variable id impl keep; Dischargedhypsmap.set_discharged_hyps sp []; @@ -116,7 +118,7 @@ let cache_constant ((sp,kn),(cdt,dhyps,kind)) = let discharged_hyps kn sechyps = let (_,dir,_) = repr_kn kn in - let args = array_map_to_list destVar (instance_from_named_context sechyps) in + let args = Array.to_list (instance_from_variable_context sechyps) in List.rev (List.map (Libnames.make_path dir) args) let discharge_constant ((sp,kn),(cdt,dhyps,kind)) = @@ -124,7 +126,7 @@ let discharge_constant ((sp,kn),(cdt,dhyps,kind)) = let cb = Global.lookup_constant con in let repl = replacement_context () in let sechyps = section_segment_of_constant con in - let recipe = { d_from=cb; d_modlist=repl; d_abstract=sechyps } in + let recipe = { d_from=cb; d_modlist=repl; d_abstract=named_of_variable_context sechyps } in Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind) (* Hack to reduce the size of .vo: we keep only what load/open needs *) @@ -235,7 +237,7 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) = let repl = replacement_context () in let sechyps = section_segment_of_mutual_inductive kn in Some (discharged_hyps kn sechyps, - Discharge.process_inductive sechyps repl mie) + Discharge.process_inductive (named_of_variable_context sechyps) repl mie) let dummy_one_inductive_entry mie = { mind_entry_typename = mie.mind_entry_typename; diff --git a/library/declaremods.ml b/library/declaremods.ml index 123417a6..b630b5dc 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declaremods.ml 11142 2008-06-18 15:37:31Z soubiran $ i*) +(*i $Id: declaremods.ml 11246 2008-07-22 15:10:05Z soubiran $ i*) open Pp open Util open Names @@ -433,10 +433,12 @@ and subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) = mod_entry_expr = Some (MSEident mp')},sub), substobjs, match mbids with - | [] -> + | [] -> let subst = update_subst subst' (map_mp mp' mp) in Some (subst_objects (dir,(mp',empty_dirpath)) - (join subst' (join (map_msid msid mp') - (map_mp mp mp'))) objs) + (join (join subst' subst) (join (map_msid msid mp') + (map_mp mp mp'))) + objs) + | _ -> None) | _ -> anomaly "Modops: Not an alias" diff --git a/library/heads.ml b/library/heads.ml index 626f1795..970ae87b 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: heads.ml 10841 2008-04-24 07:19:57Z herbelin $ *) +(* $Id: heads.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Pp open Util @@ -158,7 +158,7 @@ let discharge_head (_,(ref,k)) = | EvalConstRef cst -> Some (EvalConstRef (pop_con cst), k) | EvalVarRef id -> None -let rebuild_head (info,(ref,k)) = +let rebuild_head (ref,k) = (ref, compute_head ref) let export_head o = Some o diff --git a/library/impargs.ml b/library/impargs.ml index cae1986e..3a505ddb 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: impargs.ml 10796 2008-04-15 12:00:50Z herbelin $ *) +(* $Id: impargs.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Util open Names @@ -20,13 +20,14 @@ open Libobject open Lib open Nametab open Pp -open Termops open Topconstr +open Termops (*s Flags governing the computation of implicit arguments *) type implicits_flags = { main : bool; + manual : bool; (* automatic or manual only *) strict : bool; (* true = strict *) strongly_strict : bool; (* true = strongly strict *) reversible_pattern : bool; @@ -38,6 +39,7 @@ type implicits_flags = { let implicit_args = ref { main = false; + manual = false; strict = true; strongly_strict = false; reversible_pattern = false; @@ -48,6 +50,10 @@ let implicit_args = ref { let make_implicit_args flag = implicit_args := { !implicit_args with main = flag } +let make_manual_implicit_args flag = + implicit_args := { !implicit_args with main = if flag then true else !implicit_args.main; + manual = flag } + let make_strict_implicit_args flag = implicit_args := { !implicit_args with strict = flag } @@ -64,6 +70,7 @@ let make_maximal_implicit_args flag = implicit_args := { !implicit_args with maximal = flag } let is_implicit_args () = !implicit_args.main +let is_manual_implicit_args () = !implicit_args.manual let is_strict_implicit_args () = !implicit_args.strict let is_strongly_strict_implicit_args () = !implicit_args.strongly_strict let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern @@ -88,7 +95,7 @@ let set_maximality imps b = (*s Computation of implicit arguments *) -(* We remember various information about why an argument is (automatically) +(* We remember various information about why an argument is inferable as implicit - [DepRigid] means that the implicit argument can be found by @@ -105,6 +112,8 @@ let set_maximality imps b = inferable following a rigid path (useful to know how to print a partial application) +- [Manual] means the argument has been explicitely set as implicit. + We also consider arguments inferable from the conclusion but it is operational only if [conclusion_matters] is true. *) @@ -117,7 +126,7 @@ type implicit_explanation = | DepRigid of argument_position | DepFlex of argument_position | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position - | Manual of bool + | Manual let argument_less = function | Hyp n, Hyp n' -> n if argument_less (pos,fpos) or pos=fpos then DepRigid pos else DepFlexAndRigid (fpos,pos) - | Some (Manual _) -> assert false + | Some Manual -> assert false else match st with | None -> DepFlex pos @@ -147,7 +156,7 @@ let update pos rig (na,st) = if argument_less (pos,fpos) then DepFlexAndRigid (pos,rpos) else x | Some (DepFlex fpos as x) -> if argument_less (pos,fpos) then DepFlex pos else x - | Some (Manual _) -> assert false + | Some Manual -> assert false in na, Some e (* modified is_rigid_reference with a truncated env *) @@ -241,11 +250,7 @@ let compute_implicits_flags env f all t = f.reversible_pattern f.contextual all env t let set_implicit id imp insmax = - (id,(match imp with None -> Manual false | Some imp -> imp),insmax) - -let merge_imps f = function - None -> Some (Manual f) - | x -> x + (id,(match imp with None -> Manual | Some imp -> imp),insmax) let rec assoc_by_pos k = function (ExplByPos (k', x), b) :: tl when k = k' -> (x,b), tl @@ -262,7 +267,7 @@ let compute_manual_implicits env flags t enriching l = let (id, (b, f)), l' = assoc_by_pos k l in if f then let id = match id with Some id -> id | None -> id_of_string ("arg_" ^ string_of_int k) in - l', Some (id,Manual f,b) + l', Some (id,Manual,b) else l, None with Not_found -> l, None in @@ -274,11 +279,11 @@ let compute_manual_implicits env flags t enriching l = let l',imp,m = try let (b, f) = List.assoc (ExplByName id) l in - List.remove_assoc (ExplByName id) l, merge_imps f imp,Some b + List.remove_assoc (ExplByName id) l, (Some Manual), (Some b) with Not_found -> try let (id, (b, f)), l' = assoc_by_pos k l in - l', merge_imps f imp,Some b + l', (Some Manual), (Some b) with Not_found -> l,imp, if enriching && imp <> None then Some flags.maximal else None in @@ -305,11 +310,15 @@ let compute_manual_implicits env flags t enriching l = in merge 1 l autoimps +let const v _ = v + let compute_implicits_auto env f manual t = match manual with - [] -> let l = compute_implicits_flags env f false t in - prepare_implicits f l - | _ -> compute_manual_implicits env f t true manual + | [] -> + let l = compute_implicits_flags env f false t in + if f.manual then List.map (const None) l + else prepare_implicits f l + | _ -> compute_manual_implicits env f t (not f.manual) manual let compute_implicits env t = compute_implicits_auto env !implicit_args [] t @@ -333,10 +342,6 @@ let maximal_insertion_of = function | Some (_,_,b) -> b | None -> anomaly "Not an implicit argument" -let forced_implicit = function - | Some (_,Manual b,_) -> b - | _ -> false - (* [in_ctx] means we know the expected type, [n] is the index of the argument *) let is_inferable_implicit in_ctx n = function | None -> false @@ -346,7 +351,7 @@ let is_inferable_implicit in_ctx n = function | Some (_,DepRigid Conclusion,_) -> in_ctx | Some (_,DepFlex Conclusion,_) -> false | Some (_,DepFlexAndRigid (_,Conclusion),_) -> in_ctx - | Some (_,Manual _,_) -> true + | Some (_,Manual,_) -> true let positions_of_implicits = let rec aux n = function @@ -417,9 +422,18 @@ let list_split_at index l = | [] -> failwith "list_split_at: Invalid argument" in aux 0 [] l -let merge_impls oimpls impls = - let oimpls, _ = list_split_at (List.length oimpls - List.length impls) oimpls in - oimpls @ impls +let merge_impls oldimpls newimpls = + let (before, news), olds = + let len = List.length newimpls - List.length oldimpls in + if len >= 0 then list_split_at len newimpls, oldimpls + else + let before, after = list_split_at (-len) oldimpls in + (before, newimpls), after + in + before @ (List.map2 (fun orig ni -> + match orig with + | Some (_, Manual, _) -> orig + | _ -> ni) olds news) (* Caching implicits *) @@ -453,34 +467,67 @@ let subst_implicits_decl subst (r,imps as o) = let subst_implicits (_,subst,(req,l)) = (ImplLocal,list_smartmap (subst_implicits_decl subst) l) +let impls_of_context ctx = + List.rev_map (fun (id,impl,_,_) -> if impl = Lib.Implicit then Some (id, Manual, true) else None) + (List.filter (fun (_,_,b,_) -> b = None) ctx) + +let section_segment_of_reference = function + | ConstRef con -> section_segment_of_constant con + | IndRef (kn,_) | ConstructRef ((kn,_),_) -> + section_segment_of_mutual_inductive kn + | _ -> [] + let discharge_implicits (_,(req,l)) = match req with | ImplLocal -> None | ImplInteractive (ref,flags,exp) -> - Some (ImplInteractive (pop_global_reference ref,flags,exp),l) + let vars = section_segment_of_reference ref in + let ref' = pop_global_reference ref in + let l' = [ref', impls_of_context vars @ snd (List.hd l)] in + Some (ImplInteractive (ref',flags,exp),l') | ImplConstant (con,flags) -> - Some (ImplConstant (pop_con con,flags),l) + let con' = pop_con con in + let l' = [ConstRef con',impls_of_context (section_segment_of_constant con) @ snd (List.hd l)] in + Some (ImplConstant (con',flags),l') | ImplMutualInductive (kn,flags) -> - Some (ImplMutualInductive (pop_kn kn,flags),l) + let l' = List.map (fun (gr, l) -> + let vars = section_segment_of_reference gr in + (pop_global_reference gr, impls_of_context vars @ l)) l + in + Some (ImplMutualInductive (pop_kn kn,flags),l') -let rebuild_implicits (info,(req,l)) = - let manual = List.fold_left (fun acc (id, impl, keep) -> - if impl then (ExplByName id, (true, true)) :: acc else acc) - [] info - in +let rebuild_implicits (req,l) = let l' = match req with | ImplLocal -> assert false | ImplConstant (con,flags) -> - [ConstRef con, compute_constant_implicits flags manual con] + let oldimpls = snd (List.hd l) in + let newimpls = compute_constant_implicits flags [] con in + [ConstRef con, merge_impls oldimpls newimpls] | ImplMutualInductive (kn,flags) -> - compute_all_mib_implicits flags manual kn + let newimpls = compute_all_mib_implicits flags [] kn in + let rec aux olds news = + match olds, news with + | (_, oldimpls) :: old, (gr, newimpls) :: tl -> + (gr, merge_impls oldimpls newimpls) :: aux old tl + | [], [] -> [] + | _, _ -> assert false + in aux l newimpls + | ImplInteractive (ref,flags,o) -> match o with - | ImplAuto -> [ref,compute_global_implicits flags manual ref] - | ImplManual l -> - let auto = compute_global_implicits flags manual ref in -(* let auto = if flags.main then auto else List.map (fun _ -> None) auto in *) - let l' = merge_impls auto l in [ref,l'] + | ImplAuto -> + let oldimpls = snd (List.hd l) in + let newimpls = compute_global_implicits flags [] ref in + [ref,merge_impls oldimpls newimpls] + | ImplManual m -> + let oldimpls = snd (List.hd l) in + let auto = + if flags.main then + let newimpls = compute_global_implicits flags [] ref in + merge_impls oldimpls newimpls + else oldimpls + in + let l' = merge_impls auto m in [ref,l'] in (req,l') let export_implicits (req,_ as x) = @@ -545,6 +592,12 @@ let maybe_declare_manual_implicits local ref enriching l = if l = [] then () else declare_manual_implicits local ref enriching l +let lift_implicits n = + List.map (fun x -> + match fst x with + ExplByPos (k, id) -> ExplByPos (k + n, id), snd x + | _ -> x) + (*s Registration as global tables *) let init () = implicits_table := Refmap.empty diff --git a/library/impargs.mli b/library/impargs.mli index 5b55af82..705efd31 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: impargs.mli 10741 2008-04-02 15:47:07Z msozeau $ i*) +(*i $Id: impargs.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (*i*) open Names @@ -20,6 +20,7 @@ open Nametab are outside the kernel, which knows nothing about implicit arguments. *) val make_implicit_args : bool -> unit +val make_manual_implicit_args : bool -> unit val make_strict_implicit_args : bool -> unit val make_strongly_strict_implicit_args : bool -> unit val make_reversible_pattern_implicit_args : bool -> unit @@ -27,6 +28,7 @@ val make_contextual_implicit_args : bool -> unit val make_maximal_implicit_args : bool -> unit val is_implicit_args : unit -> bool +val is_manual_implicit_args : unit -> bool val is_strict_implicit_args : unit -> bool val is_strongly_strict_implicit_args : unit -> bool val is_reversible_pattern_implicit_args : unit -> bool @@ -38,16 +40,25 @@ val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b (*s An [implicits_list] is a list of positions telling which arguments of a reference can be automatically infered *) -type implicit_status -type implicits_list = implicit_status list -type implicit_explanation + +type argument_position = + | Conclusion + | Hyp of int + +type implicit_explanation = + | DepRigid of argument_position + | DepFlex of argument_position + | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position + | Manual + +type implicit_status = (identifier * implicit_explanation * bool) option +type implicits_list = implicit_status list val is_status_implicit : implicit_status -> bool val is_inferable_implicit : bool -> int -> implicit_status -> bool val name_of_implicit : implicit_status -> identifier val maximal_insertion_of : implicit_status -> bool -val forced_implicit : implicit_status -> bool val positions_of_implicits : implicits_list -> int list @@ -83,3 +94,30 @@ val maybe_declare_manual_implicits : bool -> global_reference -> bool -> manual_explicitation list -> unit val implicits_of_global : global_reference -> implicits_list + +val lift_implicits : int -> manual_explicitation list -> manual_explicitation list + +val merge_impls : implicits_list -> implicits_list -> implicits_list + +type implicit_interactive_request = + | ImplAuto + | ImplManual of implicit_status list + +type implicit_discharge_request = + | ImplLocal + | ImplConstant of constant * implicits_flags + | ImplMutualInductive of kernel_name * implicits_flags + | ImplInteractive of global_reference * implicits_flags * + implicit_interactive_request + +val discharge_implicits : 'a * + (implicit_discharge_request * + (Libnames.global_reference * + (Names.identifier * implicit_explanation * bool) option list) + list) -> + (implicit_discharge_request * + (Libnames.global_reference * + (Names.identifier * implicit_explanation * bool) option list) + list) + option + diff --git a/library/lib.ml b/library/lib.ml index ce3d2520..fa71bb2f 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: lib.ml 10982 2008-05-24 14:32:25Z herbelin $ *) +(* $Id: lib.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Pp open Util @@ -214,9 +214,9 @@ let add_leaf id obj = add_entry oname (Leaf obj); oname -let add_discharged_leaf id varinfo obj = +let add_discharged_leaf id obj = let oname = make_oname id in - let newobj = rebuild_object (varinfo, obj) in + let newobj = rebuild_object obj in cache_object (oname,newobj); add_entry oname (Leaf newobj) @@ -436,11 +436,14 @@ let what_is_opened () = find_entry_p is_something_opened - the list of variables on which each inductive depends in this section - the list of substitution to do at section closing *) +type binding_kind = Explicit | Implicit -type abstr_list = Sign.named_context Cmap.t * Sign.named_context KNmap.t +type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types +type variable_context = variable_info list +type abstr_list = variable_context Names.Cmap.t * variable_context Names.KNmap.t let sectab = - ref ([] : ((identifier * bool * Term.types option) list * Cooking.work_list * abstr_list) list) + ref ([] : ((Names.identifier * binding_kind * Term.types option) list * Cooking.work_list * abstr_list) list) let add_section () = sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab @@ -451,25 +454,34 @@ let add_section_variable id impl keep = | (vars,repl,abs)::sl -> sectab := ((id,impl,keep)::vars,repl,abs)::sl let rec extract_hyps = function - | ((id,impl,keep)::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps) - | ((id,impl,Some ty)::idl,hyps) -> (id,None,ty) :: extract_hyps (idl,hyps) + | ((id,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: extract_hyps (idl,hyps) + | ((id,impl,Some ty)::idl,hyps) -> (id,impl,None,ty) :: extract_hyps (idl,hyps) | (id::idl,hyps) -> extract_hyps (idl,hyps) | [], _ -> [] +let instance_from_variable_context sign = + let rec inst_rec = function + | (id,b,None,_) :: sign -> id :: inst_rec sign + | _ :: sign -> inst_rec sign + | [] -> [] in + Array.of_list (inst_rec sign) + +let named_of_variable_context = List.map (fun (id,_,b,t) -> (id,b,t)) + let add_section_replacement f g hyps = match !sectab with | [] -> () | (vars,exps,abs)::sl -> let sechyps = extract_hyps (vars,hyps) in - let args = Sign.instance_from_named_context (List.rev sechyps) in - sectab := (vars,f (Array.map Term.destVar args) exps,g sechyps abs)::sl + let args = instance_from_variable_context (List.rev sechyps) in + sectab := (vars,f args exps,g sechyps abs)::sl let add_section_kn kn = - let f = (fun x (l1,l2) -> (l1,KNmap.add kn x l2)) in + let f x (l1,l2) = (l1,Names.KNmap.add kn x l2) in add_section_replacement f f let add_section_constant kn = - let f = (fun x (l1,l2) -> (Cmap.add kn x l1,l2)) in + let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in add_section_replacement f f let replacement_context () = pi2 (List.hd !sectab) @@ -482,13 +494,22 @@ let section_segment_of_constant con = let section_segment_of_mutual_inductive kn = KNmap.find kn (snd (pi3 (List.hd !sectab))) +let rec list_mem_assoc_in_triple x = function + [] -> raise Not_found + | (a,_,_)::l -> compare a x = 0 or list_mem_assoc_in_triple x l + let section_instance = function - | VarRef id -> [||] + | VarRef id -> + if list_mem_assoc_in_triple id (pi1 (List.hd !sectab)) then [||] + else raise Not_found | ConstRef con -> Cmap.find con (fst (pi2 (List.hd !sectab))) | IndRef (kn,_) | ConstructRef ((kn,_),_) -> KNmap.find kn (snd (pi2 (List.hd !sectab))) +let is_in_section ref = + try ignore (section_instance ref); true with Not_found -> false + let init_sectab () = sectab := [] let freeze_sectab () = !sectab let unfreeze_sectab s = sectab := s @@ -551,10 +572,6 @@ let close_section id = with Not_found -> error "no opened section" in - let var_info = List.map - (fun (x, y, z) -> (x, y, match z with Some _ -> true | None -> false)) - (variables_context ()) - in let (secdecls,secopening,before) = split_lib oname in lib_stk := before; let full_olddir = fst !path_prefix in @@ -563,7 +580,7 @@ let close_section id = if !Flags.xml_export then !xml_close_section id; let newdecls = List.map discharge_item secdecls in Summary.section_unfreeze_summaries fs; - List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id var_info o)) newdecls; + List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls; Cooking.clear_cooking_sharing (); Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir) diff --git a/library/lib.mli b/library/lib.mli index 64074cfd..d35fcc09 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lib.mli 11046 2008-06-03 22:48:06Z msozeau $ i*) +(*i $Id: lib.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (*i*) open Util @@ -171,17 +171,24 @@ val reset_initial : unit -> unit val set_xml_open_section : (identifier -> unit) -> unit val set_xml_close_section : (identifier -> unit) -> unit +type binding_kind = Explicit | Implicit (*s Section management for discharge *) +type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types +type variable_context = variable_info list -val section_segment_of_constant : constant -> Sign.named_context -val section_segment_of_mutual_inductive: mutual_inductive -> Sign.named_context +val instance_from_variable_context : variable_context -> Names.identifier array +val named_of_variable_context : variable_context -> Sign.named_context -val section_instance : global_reference -> identifier array +val section_segment_of_constant : Names.constant -> variable_context +val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_context -val add_section_variable : identifier -> bool -> Term.types option -> unit -val add_section_constant : constant -> Sign.named_context -> unit -val add_section_kn : kernel_name -> Sign.named_context -> unit +val section_instance : Libnames.global_reference -> Names.identifier array +val is_in_section : Libnames.global_reference -> bool + +val add_section_variable : Names.identifier -> binding_kind -> Term.types option -> unit +val add_section_constant : Names.constant -> Sign.named_context -> unit +val add_section_kn : Names.kernel_name -> Sign.named_context -> unit val replacement_context : unit -> (identifier array Cmap.t * identifier array KNmap.t) diff --git a/library/libnames.ml b/library/libnames.ml index 31822da4..d0c6e8b9 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libnames.ml 10580 2008-02-22 13:39:13Z lmamane $ i*) +(*i $Id: libnames.ml 11209 2008-07-05 10:17:49Z herbelin $ i*) open Pp open Util @@ -89,6 +89,8 @@ let drop_dirpath_prefix d1 d2 = let d = Util.list_drop_prefix (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) in make_dirpath (List.rev d) +let append_dirpath d1 d2 = make_dirpath (repr_dirpath d2 @ repr_dirpath d1) + (* To know how qualified a name should be to be understood in the current env*) let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id]) diff --git a/library/libnames.mli b/library/libnames.mli index d4942061..76c406db 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libnames.mli 10308 2007-11-09 09:40:21Z herbelin $ i*) +(*i $Id: libnames.mli 11209 2008-07-05 10:17:49Z herbelin $ i*) (*i*) open Pp @@ -59,6 +59,7 @@ val chop_dirpath : int -> dir_path -> dir_path * dir_path val drop_dirpath_prefix : dir_path -> dir_path -> dir_path val extract_dirpath_prefix : int -> dir_path -> dir_path val is_dirpath_prefix_of : dir_path -> dir_path -> bool +val append_dirpath : dir_path -> dir_path -> dir_path module Dirset : Set.S with type elt = dir_path module Dirmap : Map.S with type key = dir_path diff --git a/library/libobject.ml b/library/libobject.ml index ff78f527..6b302447 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: libobject.ml 10741 2008-04-02 15:47:07Z msozeau $ *) +(* $Id: libobject.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Util open Names @@ -28,8 +28,6 @@ let relax b = relax_flag := b;; type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a -type discharge_info = (identifier * bool * bool) list - type 'a object_declaration = { object_name : string; cache_function : object_name * 'a -> unit; @@ -38,7 +36,7 @@ type 'a object_declaration = { classify_function : object_name * 'a -> 'a substitutivity; subst_function : object_name * substitution * 'a -> 'a; discharge_function : object_name * 'a -> 'a option; - rebuild_function : discharge_info * 'a -> 'a; + rebuild_function : 'a -> 'a; export_function : 'a -> 'a option } let yell s = anomaly s @@ -52,7 +50,7 @@ let default_object s = { 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); + rebuild_function = (fun x -> x); export_function = (fun _ -> None)} @@ -78,7 +76,7 @@ type dynamic_object_declaration = { 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 : discharge_info * obj -> obj; + dyn_rebuild_function : obj -> obj; dyn_export_function : obj -> obj option } let object_tag lobj = Dyn.tag lobj @@ -116,8 +114,8 @@ let declare_object odecl = Option.map infun (odecl.discharge_function (oname,outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the dischargefun" - and rebuild (varinfo,lobj) = - if Dyn.tag lobj = na then infun (odecl.rebuild_function (varinfo,outfun lobj)) + 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 @@ -174,7 +172,7 @@ let classify_object ((_,lobj) as node) = let discharge_object ((_,lobj) as node) = apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj -let rebuild_object ((_,lobj) as node) = +let rebuild_object (lobj as node) = apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function node) lobj let export_object lobj = diff --git a/library/libobject.mli b/library/libobject.mli index 5f6cf13b..4ec5746b 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libobject.mli 10840 2008-04-23 21:29:34Z herbelin $ i*) +(*i $Id: libobject.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (*i*) open Names @@ -71,8 +71,6 @@ open Mod_subst type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a -type discharge_info = (identifier * bool * bool) list - type 'a object_declaration = { object_name : string; cache_function : object_name * 'a -> unit; @@ -81,7 +79,7 @@ type 'a object_declaration = { classify_function : object_name * 'a -> 'a substitutivity; subst_function : object_name * substitution * 'a -> 'a; discharge_function : object_name * 'a -> 'a option; - rebuild_function : discharge_info * 'a -> 'a; + rebuild_function : 'a -> 'a; export_function : 'a -> 'a option } (* The default object is a "Keep" object with empty methods. @@ -116,5 +114,5 @@ val subst_object : object_name * substitution * obj -> obj val classify_object : object_name * obj -> obj substitutivity val export_object : obj -> obj option val discharge_object : object_name * obj -> obj option -val rebuild_object : discharge_info * obj -> obj +val rebuild_object : obj -> obj val relax : bool -> unit diff --git a/library/library.ml b/library/library.ml index 2904edc2..73928a9b 100644 --- a/library/library.ml +++ b/library/library.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: library.ml 11181 2008-06-27 07:35:45Z notin $ *) +(* $Id: library.ml 11313 2008-08-07 11:15:03Z barras $ *) open Pp open Util @@ -25,9 +25,9 @@ open Declaremods type logical_path = dir_path -let load_paths = ref ([],[] : System.physical_path list * logical_path list) +let load_paths = ref ([] : (System.physical_path * logical_path * bool) list) -let get_load_paths () = fst !load_paths +let get_load_paths () = List.map pi1 !load_paths (* Hints to partially detects if two paths refer to the same repertory *) let rec remove_path_dot p = @@ -57,12 +57,12 @@ let canonical_path_name p = (* We give up to find a canonical name and just simplify it... *) strip_path p -let find_logical_path phys_dir = +let find_logical_path phys_dir = let phys_dir = canonical_path_name phys_dir in - match list_filter2 (fun p d -> p = phys_dir) !load_paths with - | _,[dir] -> dir - | _,[] -> Nameops.default_root_prefix - | _,l -> anomaly ("Two logical paths are associated to "^phys_dir) + match List.filter (fun (p,d,_) -> p = phys_dir) !load_paths with + | [_,dir,_] -> dir + | [] -> Nameops.default_root_prefix + | l -> anomaly ("Two logical paths are associated to "^phys_dir) let is_in_load_paths phys_dir = let dir = canonical_path_name phys_dir in @@ -71,12 +71,12 @@ let is_in_load_paths phys_dir = List.exists check_p lp let remove_load_path dir = - load_paths := list_filter2 (fun p d -> p <> dir) !load_paths + load_paths := List.filter (fun (p,d,_) -> p <> dir) !load_paths -let add_load_path (phys_path,coq_path) = +let add_load_path isroot (phys_path,coq_path) = let phys_path = canonical_path_name phys_path in - match list_filter2 (fun p d -> p = phys_path) !load_paths with - | _,[dir] -> + match List.filter (fun (p,d,_) -> p = phys_path) !load_paths with + | [_,dir,_] -> if coq_path <> dir (* If this is not the default -I . to coqtop *) && not @@ -91,18 +91,54 @@ let add_load_path (phys_path,coq_path) = pr_dirpath dir ++ strbrk "; it is remapped to " ++ pr_dirpath coq_path); remove_load_path phys_path; - load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths) + load_paths := (phys_path,coq_path,isroot) :: !load_paths; end - | _,[] -> - load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths) + | [] -> + load_paths := (phys_path,coq_path,isroot) :: !load_paths; | _ -> anomaly ("Two logical paths are associated to "^phys_path) let physical_paths (dp,lp) = dp -let load_paths_of_dir_path dir = - fst (list_filter2 (fun p d -> d = dir) !load_paths) - -let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths) +let extend_path_with_dirpath p dir = + List.fold_left Filename.concat p + (List.map string_of_id (List.rev (repr_dirpath dir))) + +let root_paths_matching_dir_path dir = + let rec aux = function + | [] -> [] + | (p,d,true) :: l when is_dirpath_prefix_of d dir -> + let suffix = drop_dirpath_prefix d dir in + extend_path_with_dirpath p suffix :: aux l + | _ :: l -> aux l in + aux !load_paths + +(* Root p is bound to A.B.C.D and we require file C.D.E.F *) +(* We may mean A.B.C.D.E.F, or A.B.C.D.C.D.E.F *) + +(* Root p is bound to A.B.C.C and we require file C.C.E.F *) +(* We may mean A.B.C.C.E.F, or A.B.C.C.C.E.F, or A.B.C.C.C.C.E.F *) + +let intersections d1 d2 = + let rec aux d1 = + if d1 = empty_dirpath then [d2] else + let rest = aux (snd (chop_dirpath 1 d1)) in + if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest + else rest in + aux d1 + +let loadpaths_matching_dir_path dir = + let rec aux = function + | [] -> [] + | (p,d,true) :: l -> + let inters = intersections d dir in + List.map (fun tl -> (extend_path_with_dirpath p tl,append_dirpath d tl)) + inters @ + aux l + | (p,d,_) :: l -> + (extend_path_with_dirpath p dir,append_dirpath d dir) :: aux l in + aux !load_paths + +let get_full_load_paths () = List.map (fun (a,b,c) -> (a,b)) !load_paths (************************************************************************) (*s Modules on disk contain the following informations (after the magic @@ -197,6 +233,12 @@ let library_full_filename dir = try LibraryFilenameMap.find dir !libraries_filename_table with Not_found -> "" +let overwrite_library_filenames f = + let f = + if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f else f in + LibraryMap.iter (fun dir _ -> register_library_filename dir f) + !libraries_table + let library_is_loaded dir = try let _ = find_library dir in true with Not_found -> false @@ -312,10 +354,8 @@ let (in_import, out_import) = (*s Loading from disk to cache (preparation phase) *) -let vo_magic_number = 08193 (* v8.2beta3 *) - let (raw_extern_library, raw_intern_library) = - System.raw_extern_intern vo_magic_number ".vo" + System.raw_extern_intern Coq_config.vo_magic_number ".vo" let with_magic_number_check f a = try f a @@ -335,11 +375,11 @@ type library_location = LibLoaded | LibInPath let locate_absolute_library dir = (* Search in loadpath *) let pref, base = split_dirpath dir in - let loadpath = load_paths_of_dir_path pref in + let loadpath = root_paths_matching_dir_path pref in if loadpath = [] then raise LibUnmappedDir; try let name = (string_of_id base)^".vo" in - let _, file = System.where_in_path loadpath name in + let _, file = System.where_in_path false loadpath name in (dir, file) with Not_found -> (* Last chance, removed from the file system but still in memory *) @@ -348,20 +388,15 @@ let locate_absolute_library dir = else raise LibNotFound -let locate_qualified_library qid = +let locate_qualified_library warn qid = try (* Search library in loadpath *) - let dir, base = repr_qualid qid in - let loadpath = - if repr_dirpath dir = [] then get_load_paths () - else - (* we assume dir is an absolute dirpath *) - load_paths_of_dir_path dir - in + let dir, base = repr_qualid qid in + let loadpath = loadpaths_matching_dir_path dir in if loadpath = [] then raise LibUnmappedDir; - let name = (string_of_id base)^".vo" in - let path, file = System.where_in_path loadpath name in - let dir = extend_dirpath (find_logical_path path) base in + let name = string_of_id base ^ ".vo" in + let lpath, file = System.where_in_path warn (List.map fst loadpath) name in + let dir = extend_dirpath (List.assoc lpath loadpath) base in (* Look if loaded *) if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir) (* Otherwise, look for it in the file system *) @@ -387,7 +422,7 @@ let try_locate_absolute_library dir = let try_locate_qualified_library (loc,qid) = try - let (_,dir,f) = locate_qualified_library qid in + let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in dir,f with e -> explain_locate_library_error qid e @@ -590,8 +625,7 @@ let import_module export (loc,qid) = (*s Initializing the compilation of a library. *) let start_library f = - let _,longf = - System.find_file_in_path (get_load_paths ()) (f^".v") in + let _,longf = System.find_file_in_path (get_load_paths ()) (f^".v") in let ldir0 = find_logical_path (Filename.dirname longf) in let id = id_of_string (Filename.basename f) in let ldir = extend_dirpath ldir0 id in @@ -609,9 +643,9 @@ let current_reexports () = let error_recursively_dependent_library dir = errorlabstrm "" - (str "Unable to use logical name" ++ spc() ++ pr_dirpath dir ++ spc() ++ - str "to save current library" ++ spc() ++ str"because" ++ spc() ++ - str "it already depends on a library of this name.") + (strbrk "Unable to use logical name " ++ pr_dirpath dir ++ + strbrk " to save current library because" ++ + strbrk " it already depends on a library of this name.") let save_library_to dir f = let cenv, seg = Declaremods.end_library dir in diff --git a/library/library.mli b/library/library.mli index 27ace544..a66a77bc 100644 --- a/library/library.mli +++ b/library/library.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: library.mli 8877 2006-05-30 16:37:04Z notin $ i*) +(*i $Id: library.mli 11209 2008-07-05 10:17:49Z herbelin $ i*) (*i*) open Util @@ -52,6 +52,9 @@ val opened_libraries : unit -> dir_path list (* - Return the full filename of a loaded library. *) val library_full_filename : dir_path -> string + (* - Overwrite the filename of all libraries (used when restoring a state) *) +val overwrite_library_filenames : string -> unit + (*s Hook for the xml exportation of libraries *) val set_xml_require : (dir_path -> unit) -> unit @@ -61,11 +64,10 @@ val set_xml_require : (dir_path -> unit) -> unit val get_load_paths : unit -> System.physical_path list val get_full_load_paths : unit -> (System.physical_path * dir_path) list -val add_load_path : System.physical_path * dir_path -> unit +val add_load_path : bool -> System.physical_path * dir_path -> unit val remove_load_path : System.physical_path -> unit val find_logical_path : System.physical_path -> dir_path val is_in_load_paths : System.physical_path -> bool -val load_paths_of_dir_path : dir_path -> System.physical_path list (*s Locate a library in the load paths *) exception LibUnmappedDir @@ -73,7 +75,7 @@ exception LibNotFound type library_location = LibLoaded | LibInPath val locate_qualified_library : - qualid -> library_location * dir_path * System.physical_path + bool -> qualid -> library_location * dir_path * System.physical_path (*s Statistics: display the memory use of a library. *) val mem : dir_path -> Pp.std_ppcmds diff --git a/library/states.ml b/library/states.ml index 169a3857..7f7fef47 100644 --- a/library/states.ml +++ b/library/states.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: states.ml 9100 2006-08-31 18:04:26Z herbelin $ *) +(* $Id: states.ml 11313 2008-08-07 11:15:03Z barras $ *) open System @@ -19,12 +19,13 @@ let unfreeze (fl,fs) = Lib.unfreeze fl; Summary.unfreeze_summaries fs -let state_magic_number = 19764 - let (extern_state,intern_state) = - let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in + let (raw_extern, raw_intern) = + extern_intern Coq_config.state_magic_number ".coq" in (fun s -> raw_extern s (freeze())), - (fun s -> unfreeze (raw_intern (Library.get_load_paths ()) s)) + (fun s -> + unfreeze (raw_intern (Library.get_load_paths ()) s); + Library.overwrite_library_filenames s) (* Rollback. *) -- cgit v1.2.3