diff options
Diffstat (limited to 'library')
45 files changed, 1245 insertions, 2495 deletions
diff --git a/library/assumptions.ml b/library/assumptions.ml deleted file mode 100644 index 04ee14fb53..0000000000 --- a/library/assumptions.ml +++ /dev/null @@ -1,250 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* The following definitions are used by the function - [assumptions] which gives as an output the set of all - axioms and sections variables on which a given term depends - in a context (expectingly the Global context) *) - -(* Initial author: Arnaud Spiwack - Module-traversing code: Pierre Letouzey *) - -open Pp -open Errors -open Util -open Names -open Term -open Declarations -open Mod_subst - -type context_object = - | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of constant (* An axiom or a constant. *) - | Opaque of constant (* An opaque constant. *) - | Transparent of constant - -(* Defines a set of [assumption] *) -module OrderedContextObject = -struct - type t = context_object - let compare x y = - match x , y with - | Variable i1 , Variable i2 -> Id.compare i1 i2 - | Axiom k1 , Axiom k2 -> con_ord k1 k2 - | Opaque k1 , Opaque k2 -> con_ord k1 k2 - | Transparent k1 , Transparent k2 -> con_ord k1 k2 - | Axiom _ , Variable _ -> 1 - | Opaque _ , Variable _ - | Opaque _ , Axiom _ -> 1 - | Transparent _ , Variable _ - | Transparent _ , Axiom _ - | Transparent _ , Opaque _ -> 1 - | _ , _ -> -1 -end - -module ContextObjectSet = Set.Make (OrderedContextObject) -module ContextObjectMap = Map.Make (OrderedContextObject) - -(** For a constant c in a module sealed by an interface (M:T and - not M<:T), [Global.lookup_constant] may return a [constant_body] - without body. We fix this by looking in the implementation - of the module *) - -let modcache = ref (MPmap.empty : structure_body MPmap.t) - -let rec search_mod_label lab = function - | [] -> raise Not_found - | (l, SFBmodule mb) :: _ when Label.equal l lab -> mb - | _ :: fields -> search_mod_label lab fields - -let rec search_cst_label lab = function - | [] -> raise Not_found - | (l, SFBconst cb) :: _ when Label.equal l lab -> cb - | _ :: fields -> search_cst_label lab fields - -(* TODO: using [empty_delta_resolver] below is probably slightly incorrect. But: - a) I don't see currently what should be used instead - b) this shouldn't be critical for Print Assumption. At worse some - constants will have a canonical name which is non-canonical, - leading to failures in [Global.lookup_constant], but our own - [lookup_constant] should work. -*) - -let rec fields_of_functor f subs mp0 args = function - |NoFunctor a -> f subs mp0 args a - |MoreFunctor (mbid,_,e) -> - match args with - | [] -> assert false (* we should only encounter applied functors *) - | mpa :: args -> - let subs = add_mbid mbid mpa empty_delta_resolver (*TODO*) subs in - fields_of_functor f subs mp0 args e - -let rec lookup_module_in_impl mp = - try Global.lookup_module mp - with Not_found -> - (* The module we search might not be exported by its englobing module(s). - We access the upper layer, and then do a manual search *) - match mp with - | MPfile _ | MPbound _ -> - raise Not_found (* should have been found by [lookup_module] *) - | MPdot (mp',lab') -> - let fields = memoize_fields_of_mp mp' in - search_mod_label lab' fields - -and memoize_fields_of_mp mp = - try MPmap.find mp !modcache - with Not_found -> - let l = fields_of_mp mp in - modcache := MPmap.add mp l !modcache; - l - -and fields_of_mp mp = - let mb = lookup_module_in_impl mp in - let fields,inner_mp,subs = fields_of_mb empty_subst mb [] in - let subs = - if mp_eq inner_mp mp then subs - else add_mp inner_mp mp mb.mod_delta subs - in - Modops.subst_structure subs fields - -and fields_of_mb subs mb args = match mb.mod_expr with - |Algebraic expr -> fields_of_expression subs mb.mod_mp args expr - |Struct sign -> fields_of_signature subs mb.mod_mp args sign - |Abstract|FullStruct -> fields_of_signature subs mb.mod_mp args mb.mod_type - -(** The Abstract case above corresponds to [Declare Module] *) - -and fields_of_signature x = - fields_of_functor - (fun subs mp0 args struc -> - assert (List.is_empty args); - (struc, mp0, subs)) x - -and fields_of_expr subs mp0 args = function - |MEident mp -> - let mb = lookup_module_in_impl (subst_mp subs mp) in - fields_of_mb subs mb args - |MEapply (me1,mp2) -> fields_of_expr subs mp0 (mp2::args) me1 - |MEwith _ -> assert false (* no 'with' in [mod_expr] *) - -and fields_of_expression x = fields_of_functor fields_of_expr x - -let lookup_constant_in_impl cst fallback = - try - let mp,dp,lab = repr_kn (canonical_con cst) in - let fields = memoize_fields_of_mp mp in - (* A module found this way is necessarily closed, in particular - our constant cannot be in an opened section : *) - search_cst_label lab fields - with Not_found -> - (* Either: - - The module part of the constant isn't registered yet : - we're still in it, so the [constant_body] found earlier - (if any) was a true axiom. - - The label has not been found in the structure. This is an error *) - match fallback with - | Some cb -> cb - | None -> anomaly (str "Print Assumption: unknown constant " ++ pr_con cst) - -let lookup_constant cst = - try - let cb = Global.lookup_constant cst in - if Declareops.constant_has_body cb then cb - else lookup_constant_in_impl cst (Some cb) - with Not_found -> lookup_constant_in_impl cst None - -let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) = - modcache := MPmap.empty; - let (idts,knst) = st in - (* Infix definition for chaining function that accumulate - on a and a ContextObjectSet, ContextObjectMap. *) - let ( ** ) f1 f2 s m = let (s',m') = f1 s m in f2 s' m' in - (* This function eases memoization, by checking if an object is already - stored before trying and applying a function. - If the object is there, the function is not fired (we are in a - particular case where memoized object don't need a treatment at all). - If the object isn't there, it is stored and the function is fired*) - let try_and_go o f s m = - if ContextObjectSet.mem o s then - (s,m) - else - f (ContextObjectSet.add o s) m - in - let identity2 s m = (s,m) - in - (* Goes recursively into the term to see if it depends on assumptions. - The 3 important cases are : - - Const _ where we need to first unfold the constant and return - the needed assumptions of its body in the environment, - - Rel _ which means the term is a variable which has been bound - earlier by a Lambda or a Prod (returns [] ), - - Var _ which means that the term refers to a section variable or - a "Let" definition, in the former it is an assumption of [t], - in the latter is must be unfolded like a Const. - The other cases are straightforward recursion. - Calls to the environment are memoized, thus avoiding exploration of - the DAG of the environment as if it was a tree (can cause - exponential behavior and prevent the algorithm from terminating - in reasonable time). [s] is a set of [context_object], representing - the object already visited.*) - let rec do_constr t s acc = - let rec iter t = - match kind_of_term t with - | Var id -> do_memoize_id id - | Meta _ | Evar _ -> assert false - | Cast (e1,_,e2) | Prod (_,e1,e2) | Lambda (_,e1,e2) -> - (iter e1)**(iter e2) - | LetIn (_,e1,e2,e3) -> (iter e1)**(iter e2)**(iter e3) - | App (e1, e_array) -> (iter e1)**(iter_array e_array) - | Case (_,e1,e2,e_array) -> (iter e1)**(iter e2)**(iter_array e_array) - | Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) -> - (iter_array e1_array) ** (iter_array e2_array) - | Const (kn,_) -> do_memoize_kn kn - | _ -> identity2 (* closed atomic types + rel *) - and iter_array a = Array.fold_right (fun e f -> (iter e)**f) a identity2 - in iter t s acc - - and add_id id s acc = - (* a Var can be either a variable, or a "Let" definition.*) - match Global.lookup_named id with - | (_,None,t) -> - (s,ContextObjectMap.add (Variable id) t acc) - | (_,Some bdy,_) -> do_constr bdy s acc - - and do_memoize_id id = - try_and_go (Variable id) (add_id id) - - and add_kn kn s acc = - let cb = lookup_constant kn in - let do_type cst = - let ctype = Global.type_of_global_unsafe (Globnames.ConstRef kn) in - (s,ContextObjectMap.add cst ctype acc) - in - let (s,acc) = - if Declareops.constant_has_body cb then - if Declareops.is_opaque cb || not (Cpred.mem kn knst) then - (** it is opaque *) - if add_opaque then do_type (Opaque kn) - else (s, acc) - else - if add_transparent then do_type (Transparent kn) - else (s, acc) - else (s, acc) - in - match Global.body_of_constant_body cb with - | None -> do_type (Axiom kn) - | Some body -> do_constr body s acc - - and do_memoize_kn kn = - try_and_go (Axiom kn) (add_kn kn) - - in - fun t -> - snd (do_constr t - (ContextObjectSet.empty) - (ContextObjectMap.empty)) diff --git a/library/assumptions.mli b/library/assumptions.mli deleted file mode 100644 index 0a2c62f582..0000000000 --- a/library/assumptions.mli +++ /dev/null @@ -1,30 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Util -open Names -open Term - -(** A few declarations for the "Print Assumption" command - @author spiwack *) -type context_object = - | Variable of Id.t (** A section variable or a Let definition *) - | Axiom of constant (** An axiom or a constant. *) - | Opaque of constant (** An opaque constant. *) - | Transparent of constant (** A transparent constant *) - -(** AssumptionSet.t is a set of [assumption] *) -module ContextObjectSet : Set.S with type elt = context_object -module ContextObjectMap : Map.ExtS - with type key = context_object and module Set := ContextObjectSet - -(** collects all the assumptions (optionally including opaque definitions) - on which a term relies (together with their type) *) -val assumptions : - ?add_opaque:bool -> ?add_transparent:bool -> transparent_state -> constr -> - Term.types ContextObjectMap.t diff --git a/library/declare.ml b/library/declare.ml index 7f42a747ed..31c9c24bc3 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,7 +9,7 @@ (** This module is about the low-level declaration of logical objects *) open Pp -open Errors +open CErrors open Util open Names open Libnames @@ -27,22 +27,30 @@ open Decls open Decl_kinds (** flag for internal message display *) -type internal_flag = - | KernelVerbose (* kernel action, a message is displayed *) - | KernelSilent (* kernel action, no message is displayed *) - | UserVerbose (* user action, a message is displayed *) +type internal_flag = + | UserAutomaticRequest (* kernel action, a message is displayed *) + | InternalTacticRequest (* kernel action, no message is displayed *) + | UserIndividualRequest (* user action, a message is displayed *) + +(** XML output hooks *) + +let (f_xml_declare_variable, xml_declare_variable) = Hook.make ~default:ignore () +let (f_xml_declare_constant, xml_declare_constant) = Hook.make ~default:ignore () +let (f_xml_declare_inductive, xml_declare_inductive) = Hook.make ~default:ignore () + +let if_xml f x = if !Flags.xml_export then f x else () (** Declaration of section variables and local definitions *) type section_variable_entry = - | SectionLocalDef of definition_entry + | SectionLocalDef of Safe_typing.private_constants definition_entry | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind let cache_variable ((sp,_),o) = match o with - | Inl ctx -> Global.push_context_set ctx + | Inl ctx -> Global.push_context_set false ctx | Inr (id,(p,d,mk)) -> (* Constr raisonne sur les noms courts *) if variable_exists id then @@ -50,20 +58,20 @@ let cache_variable ((sp,_),o) = let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *) | SectionLocalAssum ((ty,ctx),poly,impl) -> - let () = Global.push_named_assum ((id,ty),ctx) in + let () = Global.push_named_assum ((id,ty,poly),ctx) in let impl = if impl then Implicit else Explicit in impl, true, poly, ctx | SectionLocalDef (de) -> - let () = Global.push_named_def (id,de) in - Explicit, de.const_entry_opaque, de.const_entry_polymorphic, - (Univ.ContextSet.of_context de.const_entry_universes) in + let univs = Global.push_named_def (id,de) in + Explicit, de.const_entry_opaque, + de.const_entry_polymorphic, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); add_section_variable id impl poly ctx; Dischargedhypsmap.set_discharged_hyps sp []; add_variable_data id (p,opaq,ctx,poly,mk) let discharge_variable (_,o) = match o with - | Inr (id,_) -> + | Inr (id,_) -> if variable_polymorphic id then None else Some (Inl (variable_context id)) | Inl _ -> Some o @@ -83,6 +91,7 @@ let declare_variable id obj = declare_var_implicits id; Notation.declare_ref_arguments_scope (VarRef id); Heads.declare_head (EvalVarRef id); + if_xml (Hook.get f_xml_declare_variable) oname; oname @@ -93,9 +102,13 @@ type constant_obj = { cst_hyps : Dischargedhypsmap.discharged_hyps; cst_kind : logical_kind; cst_locl : bool; + mutable cst_exported : Safe_typing.exported_private_constant list; + (* mutable: to avoid change the libobject API, since cache_function + * does not return an updated object *) + mutable cst_was_seff : bool } -type constant_declaration = constant_entry * logical_kind +type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind (* At load-time, the segment starting from the module name to the discharge *) (* section (if Remark or Fact) is needed to access a construction *) @@ -116,8 +129,9 @@ let open_constant i ((sp,kn), obj) = match (Global.lookup_constant con).const_body with | (Def _ | Undef _) -> () | OpaqueDef lc -> - match Opaqueproof.get_constraints (Global.opaque_tables ())lc with - | Some f when Future.is_val f -> Global.push_context_set (Future.force f) + match Opaqueproof.get_constraints (Global.opaque_tables ()) lc with + | Some f when Future.is_val f -> + Global.push_context_set false (Future.force f) | _ -> () let exists_name id = @@ -130,12 +144,21 @@ let check_exists sp = let cache_constant ((sp,kn), obj) = let id = basename sp in let _,dir,_ = repr_kn kn in - let () = check_exists sp in - let kn' = Global.add_constant dir id obj.cst_decl in + let kn' = + if obj.cst_was_seff then begin + obj.cst_was_seff <- false; + if Global.exists_objlabel (Label.of_id (basename sp)) + then constant_of_kn kn + else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp)) + end else + let () = check_exists sp in + let kn', exported = Global.add_constant dir id obj.cst_decl in + obj.cst_exported <- exported; + kn' in assert (eq_constant kn' (constant_of_kn kn)); Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); let cst = Global.lookup_constant kn' in - add_section_constant (cst.const_proj <> None) kn' cst.const_hyps; + add_section_constant cst.const_polymorphic kn' cst.const_hyps; Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps; add_constant_kind (constant_of_kn kn) obj.cst_kind @@ -156,19 +179,22 @@ let discharge_constant ((sp, kn), obj) = (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = - ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) + ConstantEntry + (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) let dummy_constant cst = { cst_decl = dummy_constant_entry; cst_hyps = []; cst_kind = cst.cst_kind; cst_locl = cst.cst_locl; + cst_exported = []; + cst_was_seff = cst.cst_was_seff; } let classify_constant cst = Substitute (dummy_constant cst) -let inConstant : constant_obj -> obj = - declare_object { (default_object "CONSTANT") with +let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) = + declare_object_full { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; open_function = open_constant; @@ -176,17 +202,42 @@ let inConstant : constant_obj -> obj = subst_function = ident_subst_function; discharge_function = discharge_constant } +let declare_scheme = ref (fun _ _ -> assert false) +let set_declare_scheme f = declare_scheme := f + let declare_constant_common id cst = - let (sp,kn) = add_leaf id (inConstant cst) in + let update_tables c = +(* Printf.eprintf "tables: %s\n%!" (Names.Constant.to_string c); *) + declare_constant_implicits c; + Heads.declare_head (EvalConstRef c); + Notation.declare_ref_arguments_scope (ConstRef c) in + let o = inConstant cst in + let _, kn as oname = add_leaf id o in + List.iter (fun (c,ce,role) -> + (* handling of private_constants just exported *) + let o = inConstant { + cst_decl = ConstantEntry (false, ce); + cst_hyps = [] ; + cst_kind = IsProof Theorem; + cst_locl = false; + cst_exported = []; + cst_was_seff = true; } in + let id = Label.to_id (pi3 (Constant.repr3 c)) in + ignore(add_leaf id o); + update_tables c; + let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in + match role with + | Safe_typing.Subproof -> () + | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]) + (outConstant o).cst_exported; + pull_to_head oname; let c = Global.constant_of_delta_kn kn in - declare_constant_implicits c; - Heads.declare_head (EvalConstRef c); - Notation.declare_ref_arguments_scope (ConstRef c); + update_tables c; c -let definition_entry ?(opaque=false) ?(inline=false) ?types - ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Declareops.no_seff) body = - { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff); +let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types + ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = + { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; const_entry_type = types; const_entry_polymorphic = poly; @@ -195,97 +246,34 @@ let definition_entry ?(opaque=false) ?(inline=false) ?types const_entry_feedback = None; const_entry_inline_code = inline} -let declare_scheme = ref (fun _ _ -> assert false) -let set_declare_scheme f = declare_scheme := f -let declare_sideff env fix_exn se = - let cbl, scheme = match se with - | SEsubproof (c, cb, pt) -> [c, cb, pt], None - | SEscheme (cbl, k) -> - List.map (fun (_,c,cb,pt) -> c,cb,pt) cbl, Some (cbl,k) in - let id_of c = Names.Label.to_id (Names.Constant.label c) in - let pt_opaque_of cb pt = - match cb, pt with - | { const_body = Def sc }, _ -> (Mod_subst.force_constr sc, Univ.ContextSet.empty), false - | { const_body = OpaqueDef _ }, `Opaque(pt,univ) -> (pt, univ), true - | _ -> assert false - in - let ty_of cb = - match cb.Declarations.const_type with - | Declarations.RegularArity t -> Some t - | Declarations.TemplateArity _ -> None in - let cst_of cb pt = - let pt, opaque = pt_opaque_of cb pt in - let univs, subst = - if cb.const_polymorphic then - let univs = Univ.instantiate_univ_context cb.const_universes in - univs, Vars.subst_instance_constr (Univ.UContext.instance univs) - else cb.const_universes, fun x -> x - in - let pt = (subst (fst pt), snd pt) in - let ty = Option.map subst (ty_of cb) in - { cst_decl = ConstantEntry (DefinitionEntry { - const_entry_body = Future.from_here ~fix_exn (pt, Declareops.no_seff); - const_entry_secctx = Some cb.Declarations.const_hyps; - const_entry_type = ty; - const_entry_opaque = opaque; - const_entry_inline_code = false; - const_entry_feedback = None; - const_entry_polymorphic = cb.const_polymorphic; - const_entry_universes = univs; - }); - cst_hyps = [] ; - cst_kind = Decl_kinds.IsDefinition Decl_kinds.Definition; - cst_locl = true; - } in - let exists c = - try ignore(Environ.lookup_constant c env); true - with Not_found -> false in - let knl = - CList.map_filter (fun (c,cb,pt) -> - if exists c then None - else Some (c,declare_constant_common (id_of c) (cst_of cb pt))) cbl in - match scheme with - | None -> () - | Some (inds_consts,kind) -> - !declare_scheme kind (Array.of_list - (List.map (fun (c,kn) -> - CList.find_map (fun (x,c',_,_) -> - if Constant.equal c c' then Some (x,kn) else None) inds_consts) - knl)) - -let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) = - let cd = (* We deal with side effects of non-opaque constants *) +let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = + let export = (* We deal with side effects *) match cd with - | Entries.DefinitionEntry ({ - const_entry_opaque = false; const_entry_body = bo } as de) - | Entries.DefinitionEntry ({ - const_entry_polymorphic = true; const_entry_body = bo } as de) - -> - let _, seff = Future.force bo in - if Declareops.side_effects_is_empty seff then cd - else begin - let seff = Declareops.uniquize_side_effects seff in - Declareops.iter_side_effects - (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff; - Entries.DefinitionEntry { de with - const_entry_body = Future.chain ~pure:true bo (fun (pt, _) -> - pt, Declareops.no_seff) } - end - | _ -> cd + | DefinitionEntry de when + export_seff || + not de.const_entry_opaque || + de.const_entry_polymorphic -> + let bo = de.const_entry_body in + let _, seff = Future.force bo in + Safe_typing.empty_private_constants <> seff + | _ -> false in let cst = { - cst_decl = ConstantEntry cd; + cst_decl = ConstantEntry (export,cd); cst_hyps = [] ; cst_kind = kind; cst_locl = local; + cst_exported = []; + cst_was_seff = false; } in let kn = declare_constant_common id cst in + let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in kn -let declare_definition ?(internal=UserVerbose) +let declare_definition ?(internal=UserIndividualRequest) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) ?(poly=false) id ?types (body,ctx) = - let cb = + let cb = definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body in declare_constant ~internal ~local id @@ -337,7 +325,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) = let kn' = Global.add_mind dir id mie in assert (eq_mind kn' (mind_of_kn kn)); let mind = Global.lookup_mind kn' in - add_section_kn kn' mind.mind_hyps; + add_section_kn mind.mind_polymorphic kn' mind.mind_hyps; Dischargedhypsmap.set_discharged_hyps sp dhyps; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names @@ -365,7 +353,8 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_polymorphic = false; mind_entry_universes = Univ.UContext.empty; - mind_entry_private = None }) + mind_entry_private = None; +}) type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry @@ -381,15 +370,16 @@ let inInductive : inductive_obj -> obj = let declare_projections mind = let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in match spec.mind_record with - | Some (Some (_, kns, pjs)) -> - Array.iteri (fun i kn -> + | Some (Some (_, kns, pjs)) -> + Array.iteri (fun i kn -> let id = Label.to_id (Constant.label kn) in let entry = {proj_entry_ind = mind; proj_entry_arg = i} in let kn' = declare_constant id (ProjectionEntry entry, - IsDefinition StructureComponent) + IsDefinition StructureComponent) in - assert(eq_constant kn kn')) kns; true - | Some None | None -> false + assert(eq_constant kn kn')) kns; true,true + | Some None -> true,false + | None -> false,false (* for initial declaration *) let declare_mind mie = @@ -398,9 +388,10 @@ let declare_mind mie = | [] -> anomaly (Pp.str "cannot declare an empty list of inductives") in let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in let mind = Global.mind_of_delta_kn kn in - let isprim = declare_projections mind in + let isrecord,isprim = declare_projections mind in declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; + if_xml (Hook.get f_xml_declare_inductive) (isrecord,oname); oname, isprim (* Declaration messages *) @@ -408,7 +399,7 @@ let declare_mind mie = let pr_rank i = pr_nth (i+1) let fixpoint_message indexes l = - Flags.if_verbose msg_info (match l with + Flags.if_verbose Feedback.msg_info (match l with | [] -> anomaly (Pp.str "no recursive definition") | [id] -> pr_id id ++ str " is recursively defined" ++ (match indexes with @@ -423,7 +414,7 @@ let fixpoint_message indexes l = | None -> mt ())) let cofixpoint_message l = - Flags.if_verbose msg_info (match l with + Flags.if_verbose Feedback.msg_info (match l with | [] -> anomaly (Pp.str "No corecursive definition.") | [id] -> pr_id id ++ str " is corecursively defined" | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++ @@ -433,57 +424,125 @@ let recursive_message isfix i l = (if isfix then fixpoint_message i else cofixpoint_message) l let definition_message id = - Flags.if_verbose msg_info (pr_id id ++ str " is defined") + Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is defined") let assumption_message id = - Flags.if_verbose msg_info (pr_id id ++ str " is assumed") + (* Changing "assumed" to "declared", "assuming" referring more to + the type of the object than to the name of the object (see + discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) + Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is declared") (** Global universe names, in a different summary *) -type universe_names = - (Univ.universe_level Idmap.t * Id.t Univ.LMap.t) +type universe_context_decl = polymorphic * Univ.universe_context_set -let input_universes : universe_names -> Libobject.obj = - let open Libobject in - declare_object +let cache_universe_context (p, ctx) = + Global.push_context_set p ctx; + if p then Lib.add_section_context ctx + +let input_universe_context : universe_context_decl -> Libobject.obj = + declare_object + { (default_object "Global universe context state") with + cache_function = (fun (na, pi) -> cache_universe_context pi); + load_function = (fun _ (_, pi) -> cache_universe_context pi); + discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x); + classify_function = (fun a -> Keep a) } + +let declare_universe_context poly ctx = + Lib.add_anonymous_leaf (input_universe_context (poly, ctx)) + +(* Discharged or not *) +type universe_decl = polymorphic * (Id.t * Univ.universe_level) list + +let cache_universes (p, l) = + let glob = Global.global_universe_names () in + let glob', ctx = + List.fold_left (fun ((idl,lid),ctx) (id, lev) -> + ((Idmap.add id (p, lev) idl, + Univ.LMap.add lev id lid), + Univ.ContextSet.add_universe lev ctx)) + (glob, Univ.ContextSet.empty) l + in + cache_universe_context (p, ctx); + Global.set_global_universe_names glob' + +let input_universes : universe_decl -> Libobject.obj = + declare_object { (default_object "Global universe name state") with - cache_function = (fun (na, pi) -> Universes.set_global_universe_names pi); - load_function = (fun _ (_, pi) -> Universes.set_global_universe_names pi); - discharge_function = (fun (_, a) -> Some a); + cache_function = (fun (na, pi) -> cache_universes pi); + load_function = (fun _ (_, pi) -> cache_universes pi); + discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x); classify_function = (fun a -> Keep a) } -let do_universe l = - let glob = Universes.global_universe_names () in - let glob' = - List.fold_left (fun (idl,lid) (l, id) -> - let lev = Universes.new_univ_level (Global.current_dirpath ()) in - (Idmap.add id lev idl, Univ.LMap.add lev id lid)) - glob l +let do_universe poly l = + let in_section = Lib.sections_are_opened () in + let () = + if poly && not in_section then + user_err ~hdr:"Constraint" + (str"Cannot declare polymorphic universes outside sections") + in + let l = + List.map (fun (l, id) -> + let lev = Universes.new_univ_level (Global.current_dirpath ()) in + (id, lev)) l in - Lib.add_anonymous_leaf (input_universes glob') + Lib.add_anonymous_leaf (input_universes (poly, l)) + +type constraint_decl = polymorphic * Univ.constraints +let cache_constraints (na, (p, c)) = + let ctx = + Univ.ContextSet.add_constraints c + Univ.ContextSet.empty (* No declared universes here, just constraints *) + in cache_universe_context (p,ctx) -let input_constraints : Univ.constraints -> Libobject.obj = - let open Libobject in +let discharge_constraints (_, (p, c as a)) = + if p then None else Some a + +let input_constraints : constraint_decl -> Libobject.obj = + let open Libobject in declare_object { (default_object "Global universe constraints") with - cache_function = (fun (na, c) -> Global.add_constraints c); - load_function = (fun _ (_, c) -> Global.add_constraints c); - discharge_function = (fun (_, a) -> Some a); + cache_function = cache_constraints; + load_function = (fun _ -> cache_constraints); + discharge_function = discharge_constraints; classify_function = (fun a -> Keep a) } -let do_constraint l = - let u_of_id = - let names, _ = Universes.global_universe_names () in - fun (loc, id) -> - try Idmap.find id names - with Not_found -> - user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) +let do_constraint poly l = + let open Misctypes in + let u_of_id x = + match x with + | GProp -> Loc.dummy_loc, (false, Univ.Level.prop) + | GSet -> Loc.dummy_loc, (false, Univ.Level.set) + | GType None -> + user_err ~hdr:"Constraint" + (str "Cannot declare constraints on anonymous universes") + | GType (Some (loc, id)) -> + let id = Id.of_string id in + let names, _ = Global.global_universe_names () in + try loc, Idmap.find id names + with Not_found -> + user_err ~loc ~hdr:"Constraint" (str "Undeclared universe " ++ pr_id id) + in + let in_section = Lib.sections_are_opened () in + let () = + if poly && not in_section then + user_err ~hdr:"Constraint" + (str"Cannot declare polymorphic constraints outside sections") + in + let check_poly loc p loc' p' = + if poly then () + else if p || p' then + let loc = if p then loc else loc' in + user_err ~loc ~hdr:"Constraint" + (str "Cannot declare a global constraint on " ++ + str "a polymorphic universe, use " + ++ str "Polymorphic Constraint instead") in let constraints = List.fold_left (fun acc (l, d, r) -> - let lu = u_of_id l and ru = u_of_id r in - Univ.Constraint.add (lu, d, ru) acc) + let ploc, (p, lu) = u_of_id l and rloc, (p', ru) = u_of_id r in + check_poly ploc p rloc p'; + Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l in - Lib.add_anonymous_leaf (input_constraints constraints) - + Lib.add_anonymous_leaf (input_constraints (poly, constraints)) diff --git a/library/declare.mli b/library/declare.mli index 03b66271a2..f70d594d7e 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -22,7 +22,7 @@ open Decl_kinds (** Declaration of local constructions (Variable/Hypothesis/Local) *) type section_variable_entry = - | SectionLocalDef of definition_entry + | SectionLocalDef of Safe_typing.private_constants definition_entry | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -32,35 +32,34 @@ val declare_variable : variable -> variable_declaration -> object_name (** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... *) -type constant_declaration = constant_entry * logical_kind +type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind -(** [declare_constant id cd] declares a global declaration - (constant/parameter) with name [id] in the current section; it returns - the full path of the declaration - - internal specify if the constant has been created by the kernel or by the - user, and in the former case, if its errors should be silent - - *) type internal_flag = - | KernelVerbose - | KernelSilent - | UserVerbose + | UserAutomaticRequest + | InternalTacticRequest + | UserIndividualRequest (* Defaut definition entries, transparent with no secctx or proj information *) -val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> - ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Declareops.side_effects -> - constr -> definition_entry +val definition_entry : ?fix_exn:Future.fix_exn -> + ?opaque:bool -> ?inline:bool -> ?types:types -> + ?poly:polymorphic -> ?univs:Univ.universe_context -> + ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry + +(** [declare_constant id cd] declares a global declaration + (constant/parameter) with name [id] in the current section; it returns + the full path of the declaration + internal specify if the constant has been created by the kernel or by the + user, and in the former case, if its errors should be silent *) val declare_constant : - ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> constant + ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> constr Univ.in_universe_context_set -> constant -(** Since transparent constant's side effects are globally declared, we +(** Since transparent constants' side effects are globally declared, we * need that *) val set_declare_scheme : (string -> (inductive * constant) array -> unit) -> unit @@ -70,6 +69,11 @@ val set_declare_scheme : the whole block and a boolean indicating if it is a primitive record. *) val declare_mind : mutual_inductive_entry -> object_name * bool +(** Hooks for XML output *) +val xml_declare_variable : (object_name -> unit) Hook.t +val xml_declare_constant : (internal_flag * constant -> unit) Hook.t +val xml_declare_inductive : (bool * object_name -> unit) Hook.t + (** Declaration messages *) val definition_message : Id.t -> unit @@ -83,7 +87,11 @@ val exists_name : Id.t -> bool -(** Global universe names and constraints *) +(** Global universe contexts, names and constraints *) + +val declare_universe_context : polymorphic -> Univ.universe_context_set -> unit -val do_universe : Id.t Loc.located list -> unit -val do_constraint : (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit +val do_universe : polymorphic -> Id.t Loc.located list -> unit +val do_constraint : polymorphic -> + (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> + unit diff --git a/library/declaremods.ml b/library/declaremods.ml index cc7c4d7f11..3a263b1e12 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -1,13 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Declarations @@ -166,12 +166,14 @@ let consistency_checks exists dir dirinfo = let globref = try Nametab.locate_dir (qualid_of_dirpath dir) with Not_found -> - anomaly (pr_dirpath dir ++ str " should already exist!") + user_err ~hdr:"consistency_checks" + (pr_dirpath dir ++ str " should already exist!") in assert (eq_global_dir_reference globref dirinfo) else if Nametab.exists_dir dir then - anomaly (pr_dirpath dir ++ str " already exists") + user_err ~hdr:"consistency_checks" + (pr_dirpath dir ++ str " already exists") let compute_visibility exists i = if exists then Nametab.Exactly i else Nametab.Until i @@ -369,7 +371,7 @@ let rec replace_module_object idl mp0 objs0 mp1 objs1 = match idl, objs0 with | _,[] -> [] | id::idl,(id',obj)::tail when Id.equal id id' -> - assert (object_has_tag obj "MODULE"); + assert (String.equal (object_tag obj) "MODULE"); let mp_id = MPdot(mp0, Label.of_id id) in let objs = match idl with | [] -> Lib.subst_objects (map_mp mp1 mp_id empty_delta_resolver) objs1 @@ -555,6 +557,17 @@ let openmodtype_info = Summary.ref ([] : module_type_body list) ~name:"MODTYPE-INFO" +(** XML output hooks *) + +let (f_xml_declare_module, xml_declare_module) = Hook.make ~default:ignore () +let (f_xml_start_module, xml_start_module) = Hook.make ~default:ignore () +let (f_xml_end_module, xml_end_module) = Hook.make ~default:ignore () +let (f_xml_declare_module_type, xml_declare_module_type) = Hook.make ~default:ignore () +let (f_xml_start_module_type, xml_start_module_type) = Hook.make ~default:ignore () +let (f_xml_end_module_type, xml_end_module_type) = Hook.make ~default:ignore () + +let if_xml f x = if !Flags.xml_export then f x else () + (** {6 Modules : start, end, declare} *) module RawModOps = struct @@ -576,7 +589,9 @@ let start_module interp_modast export id args res fs = openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps }; let prefix = Lib.start_module export id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix); - Lib.add_frozen_state (); mp + Lib.add_frozen_state (); + if_xml (Hook.get f_xml_start_module) mp; + mp let end_module () = let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in @@ -615,6 +630,7 @@ let end_module () = assert (ModPath.equal (mp_of_kn (snd newoname)) mp); Lib.add_frozen_state () (* to prevent recaching *); + if_xml (Hook.get f_xml_end_module) mp; mp let declare_module interp_modast id args res mexpr_o fs = @@ -626,7 +642,11 @@ let declare_module interp_modast id args res mexpr_o fs = let env = Global.env () in let mty_entry_o, subs, inl_res = match res with | Enforce (mty,ann) -> - Some (fst (interp_modast env ModType mty)), [], inl2intopt ann + let inl = inl2intopt ann in + let mte, _ = interp_modast env ModType mty in + (* We check immediately that mte is well-formed *) + let _ = Mod_typing.translate_mse env None inl mte in + Some mte, [], inl | Check mtys -> None, build_subtypes interp_modast env mp arg_entries_r mtys, default_inline () @@ -664,6 +684,7 @@ let declare_module interp_modast id args res mexpr_o fs = let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in ignore (Lib.add_leaf id (in_module sobjs)); + if_xml (Hook.get f_xml_declare_module) mp; mp end @@ -680,7 +701,9 @@ let start_modtype interp_modast id args mtys fs = openmodtype_info := sub_mty_l; let prefix = Lib.start_modtype id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix); - Lib.add_frozen_state (); mp + Lib.add_frozen_state (); + if_xml (Hook.get f_xml_start_module_type) mp; + mp let end_modtype () = let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in @@ -697,6 +720,7 @@ let end_modtype () = assert (ModPath.equal (mp_of_kn (snd oname)) mp); Lib.add_frozen_state ()(* to prevent recaching *); + if_xml (Hook.get f_xml_end_module_type) mp; mp let declare_modtype interp_modast id args mtys (mty,ann) fs = @@ -707,7 +731,10 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs = let arg_entries_r = intern_args interp_modast args in let params = mk_params_entry arg_entries_r in let env = Global.env () in - let entry = params, fst (interp_modast env ModType mty) in + let mte, _ = interp_modast env ModType mty in + (* We check immediately that mte is well-formed *) + let _ = Mod_typing.translate_mse env None inl mte in + let entry = params, mte in let sub_mty_l = build_subtypes interp_modast env mp arg_entries_r mtys in let sobjs = get_functor_sobjs false env inl entry in let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in @@ -727,6 +754,7 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs = check_subtypes_mt mp sub_mty_l; ignore (Lib.add_leaf id (in_modtype sobjs)); + if_xml (Hook.get f_xml_declare_module_type) mp; mp end @@ -794,7 +822,7 @@ let protect_summaries f = try f fs with reraise -> (* Something wrong: undo the whole process *) - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in let () = Summary.unfreeze_summaries fs in iraise reraise @@ -845,10 +873,6 @@ type library_objects = Lib.lib_objects * Lib.lib_objects (** For the native compiler, we cache the library values *) -type library_values = Nativecode.symbol array -let library_values = - Summary.ref (Dirmap.empty : library_values Dirmap.t) ~name:"LIBVALUES" - let register_library dir cenv (objs:library_objects) digest univ = let mp = MPfile dir in let () = @@ -857,15 +881,15 @@ let register_library dir cenv (objs:library_objects) digest univ = ignore(Global.lookup_module mp); with Not_found -> (* If not, let's do it now ... *) - let mp', values = Global.import cenv univ digest in + let mp' = Global.import cenv univ digest in if not (ModPath.equal mp mp') then anomaly (Pp.str "Unexpected disk module name"); - library_values := Dirmap.add dir values !library_values in let sobjs,keepobjs = objs in do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs -let get_library_symbols_tbl dir = Dirmap.find dir !library_values +let get_library_native_symbols dir = + Safe_typing.get_library_native_symbols (Global.safe_env ()) dir let start_library dir = let mp = Global.start_library dir in @@ -873,7 +897,13 @@ let start_library dir = Lib.start_compilation dir mp; Lib.add_frozen_state () +let end_library_hook = ref ignore +let append_end_library_hook f = + let old_f = !end_library_hook in + end_library_hook := fun () -> old_f(); f () + let end_library ?except dir = + !end_library_hook(); let oname = Lib.end_compilation_checks dir in let mp,cenv,ast = Global.export ?except dir in let prefix, lib_stack = Lib.end_compilation oname in @@ -950,7 +980,7 @@ type 'modast module_params = let debug_print_modtab _ = let pr_seg = function | [] -> str "[]" - | l -> str ("[." ^ string_of_int (List.length l) ^ ".]") + | l -> str "[." ++ int (List.length l) ++ str ".]" in let pr_modinfo mp (prefix,substobjs,keepobjs) s = s ++ str (string_of_mp mp) ++ (spc ()) diff --git a/library/declaremods.mli b/library/declaremods.mli index c3578ec421..3917fe8d64 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -63,6 +63,13 @@ val start_modtype : val end_modtype : unit -> module_path +(** Hooks for XML output *) +val xml_declare_module : (module_path -> unit) Hook.t +val xml_start_module : (module_path -> unit) Hook.t +val xml_end_module : (module_path -> unit) Hook.t +val xml_declare_module_type : (module_path -> unit) Hook.t +val xml_start_module_type : (module_path -> unit) Hook.t +val xml_end_module_type : (module_path -> unit) Hook.t (** {6 Libraries i.e. modules on disk } *) @@ -75,7 +82,7 @@ val register_library : Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest -> Univ.universe_context_set -> unit -val get_library_symbols_tbl : library_name -> Nativecode.symbol array +val get_library_native_symbols : library_name -> Nativecode.symbols val start_library : library_name -> unit @@ -83,6 +90,9 @@ val end_library : ?except:Future.UUIDSet.t -> library_name -> Safe_typing.compiled_library * library_objects * Safe_typing.native_library +(** append a function to be executed at end_library *) +val append_end_library_hook : (unit -> unit) -> unit + (** [really_import_module mp] opens the module [mp] (in a Caml sense). It modifies Nametab and performs the [open_object] function for every object of the module. Raises [Not_found] when [mp] is unknown diff --git a/library/decls.ml b/library/decls.ml index 8d5085f70e..2952c258a5 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -11,10 +11,11 @@ open Util open Names -open Context open Decl_kinds open Libnames +module NamedDecl = Context.Named.Declaration + (** Datas associated to section variables and local definitions *) type variable_data = @@ -50,13 +51,15 @@ let constant_kind kn = Cmap.find kn !csttab let initialize_named_context_for_proof () = let sign = Global.named_context () in List.fold_right - (fun (id,c,t as d) signv -> - let d = if variable_opacity id then (id,None,t) else d in + (fun d signv -> + let id = NamedDecl.get_id d in + let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val let last_section_hyps dir = - fold_named_context - (fun (id,_,_) sec_ids -> + Context.Named.fold_outside + (fun d sec_ids -> + let id = NamedDecl.get_id d in try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids with Not_found -> sec_ids) (Environ.named_context (Global.env())) diff --git a/library/decls.mli b/library/decls.mli index ac0d907d87..1ca7f89469 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index e4280334dc..cea1fd7d6e 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli index 736892016b..ea4a9424e5 100644 --- a/library/dischargedhypsmap.mli +++ b/library/dischargedhypsmap.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/global.ml b/library/global.ml index 875097e48c..5fa710b360 100644 --- a/library/global.ml +++ b/library/global.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,6 +8,7 @@ open Names open Environ +open Decl_kinds (** We introduce here the global environment of the system, and we declare it as a synchronized table. *) @@ -19,6 +20,7 @@ module GlobalSafeEnv : sig val safe_env : unit -> Safe_typing.safe_environment val set_safe_env : Safe_typing.safe_environment -> unit val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit + val is_joined_environment : unit -> bool end = struct @@ -27,6 +29,9 @@ let global_env = ref Safe_typing.empty_environment let join_safe_environment ?except () = global_env := Safe_typing.join_safe_environment ?except !global_env +let is_joined_environment () = + Safe_typing.is_joined_environment !global_env + let () = Summary.declare_summary global_env_summary_name { Summary.freeze_function = (function @@ -38,7 +43,7 @@ let () = let assert_not_parsing () = if !Flags.we_are_parsing then - Errors.anomaly ( + CErrors.anomaly ( Pp.strbrk"The global environment cannot be accessed during parsing") let safe_env () = assert_not_parsing(); !global_env @@ -50,6 +55,7 @@ end let safe_env = GlobalSafeEnv.safe_env let join_safe_environment ?except () = GlobalSafeEnv.join_safe_environment ?except () +let is_joined_environment = GlobalSafeEnv.is_joined_environment let env () = Safe_typing.env_of_safe_env (safe_env ()) @@ -73,13 +79,13 @@ let globalize_with_summary fs f = let i2l = Label.of_id let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) -let push_named_def d = globalize0 (Safe_typing.push_named_def d) +let push_named_def d = globalize (Safe_typing.push_named_def d) let add_constraints c = globalize0 (Safe_typing.add_constraints c) -let push_context_set c = globalize0 (Safe_typing.push_context_set c) -let push_context c = globalize0 (Safe_typing.push_context c) +let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) +let push_context b c = globalize0 (Safe_typing.push_context b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) -let set_type_in_type () = globalize0 (Safe_typing.set_type_in_type) +let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d) let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) @@ -194,13 +200,13 @@ let type_of_global_in_context env r = | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in let univs = - if mib.mind_polymorphic then mib.mind_universes + if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes else Univ.UContext.empty in Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in let univs = - if mib.mind_polymorphic then mib.mind_universes + if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes else Univ.UContext.empty in let inst = Univ.UContext.instance univs in @@ -224,6 +230,17 @@ let universes_of_global env r = let universes_of_global gr = universes_of_global (env ()) gr +(** Global universe names *) +type universe_names = + (polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t + +let global_universes = + Summary.ref ~name:"Global universe names" + ((Idmap.empty, Univ.LMap.empty) : universe_names) + +let global_universe_names () = !global_universes +let set_global_universe_names s = global_universes := s + let is_polymorphic r = let env = env() in match r with @@ -240,12 +257,20 @@ let is_template_polymorphic r = | IndRef ind -> Environ.template_polymorphic_ind ind env | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env +let is_type_in_type r = + let env = env() in + match r with + | VarRef id -> false + | ConstRef c -> Environ.type_in_type_constant c env + | IndRef ind -> Environ.type_in_type_ind ind env + | ConstructRef cstr -> Environ.type_in_type_ind (inductive_of_constructor cstr) env + let current_dirpath () = Safe_typing.current_dirpath (safe_env ()) let with_global f = let (a, ctx) = f (env ()) (current_dirpath ()) in - push_context_set ctx; a + push_context_set false ctx; a (* spiwack: register/unregister functions for retroknowledge *) let register field value by_clause = diff --git a/library/global.mli b/library/global.mli index af23d9b72c..a4a38ce846 100644 --- a/library/global.mli +++ b/library/global.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -19,31 +19,32 @@ val env : unit -> Environ.env val env_is_initial : unit -> bool -val universes : unit -> Univ.universes +val universes : unit -> UGraph.t val named_context_val : unit -> Environ.named_context_val -val named_context : unit -> Context.named_context +val named_context : unit -> Context.Named.t (** {6 Enriching the global environment } *) (** Changing the (im)predicativity of the system *) val set_engagement : Declarations.engagement -> unit -val set_type_in_type : unit -> unit +val set_typing_flags : Declarations.typing_flags -> unit (** Variables, Local definitions, constants, inductive types *) -val push_named_assum : (Id.t * Constr.types) Univ.in_universe_context_set -> unit -val push_named_def : (Id.t * Entries.definition_entry) -> unit +val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit +val push_named_def : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set val add_constant : - DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant + DirPath.t -> Id.t -> Safe_typing.global_declaration -> + constant * Safe_typing.exported_private_constant list val add_mind : DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive (** Extra universe constraints *) val add_constraints : Univ.constraints -> unit -val push_context : Univ.universe_context -> unit -val push_context_set : Univ.universe_context_set -> unit +val push_context : bool -> Univ.universe_context -> unit +val push_context_set : bool -> Univ.universe_context_set -> unit (** Non-interactive modules and module types *) @@ -73,7 +74,7 @@ val add_module_parameter : (** {6 Queries in the global environment } *) -val lookup_named : variable -> Context.named_declaration +val lookup_named : variable -> Context.Named.Declaration.t val lookup_constant : constant -> Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body @@ -95,6 +96,13 @@ val constraints_of_constant_body : val universes_of_constant_body : Declarations.constant_body -> Univ.universe_context +(** Global universe name <-> level mapping *) +type universe_names = + (Decl_kinds.polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t + +val global_universe_names : unit -> universe_names +val set_global_universe_names : universe_names -> unit + (** {6 Compiled libraries } *) val start_library : DirPath.t -> module_path @@ -102,7 +110,7 @@ val export : ?except:Future.UUIDSet.t -> DirPath.t -> module_path * Safe_typing.compiled_library * Safe_typing.native_library val import : Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest -> - module_path * Nativecode.symbol array + module_path (** {6 Misc } *) @@ -112,15 +120,31 @@ val import : val env_of_context : Environ.named_context_val -> Environ.env val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit +val is_joined_environment : unit -> bool val is_polymorphic : Globnames.global_reference -> bool val is_template_polymorphic : Globnames.global_reference -> bool +val is_type_in_type : Globnames.global_reference -> bool val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.types Univ.in_universe_context -val type_of_global_unsafe : Globnames.global_reference -> Constr.types +(** Returns the type of the constant in its global or local universe + context. The type should not be used without pushing it's universe + context in the environmnent of usage. For non-universe-polymorphic + constants, it does not matter. *) -(** Returns the universe context of the global reference (whatever it's polymorphic status is). *) +val type_of_global_unsafe : Globnames.global_reference -> Constr.types +(** Returns the type of the constant, forgetting its universe context if + it is polymorphic, use with care: for polymorphic constants, the + type cannot be used to produce a term used by the kernel. For safe + handling of polymorphic global references, one should look at a + particular instantiation of the reference, in some particular + universe context (part of an [env] or [evar_map]), see + e.g. [type_of_constant_in]. If you want to create a fresh instance + of the reference and get its type look at [Evd.fresh_global] or + [Evarutil.new_global] and [Retyping.get_type_of]. *) + +(** Returns the universe context of the global reference (whatever its polymorphic status is). *) val universes_of_global : Globnames.global_reference -> Univ.universe_context (** {6 Retroknowledge } *) diff --git a/library/globnames.ml b/library/globnames.ml index 5eb091af4c..a78f5f13a9 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -1,13 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util -open Errors +open CErrors open Names open Term open Mod_subst @@ -15,10 +14,10 @@ open Libnames (*s Global reference is a kernel side type for all references together *) type global_reference = - | VarRef of variable - | ConstRef of constant - | IndRef of inductive - | ConstructRef of constructor + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of constant (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) let isVarRef = function VarRef _ -> true | _ -> false let isConstRef = function ConstRef _ -> true | _ -> false @@ -108,17 +107,16 @@ let global_eq_gen eq_cst eq_ind eq_cons x y = let global_ord_gen ord_cst ord_ind ord_cons x y = if x == y then 0 else match x, y with + | VarRef v1, VarRef v2 -> Id.compare v1 v2 + | VarRef _, _ -> -1 + | _, VarRef _ -> 1 | ConstRef cx, ConstRef cy -> ord_cst cx cy + | ConstRef _, _ -> -1 + | _, ConstRef _ -> 1 | IndRef indx, IndRef indy -> ord_ind indx indy + | IndRef _, _ -> -1 + | _ , IndRef _ -> 1 | ConstructRef consx, ConstructRef consy -> ord_cons consx consy - | VarRef v1, VarRef v2 -> Id.compare v1 v2 - - | VarRef _, (ConstRef _ | IndRef _ | ConstructRef _) -> -1 - | ConstRef _, VarRef _ -> 1 - | ConstRef _, (IndRef _ | ConstructRef _) -> -1 - | IndRef _, (VarRef _ | ConstRef _) -> 1 - | IndRef _, ConstructRef _ -> -1 - | ConstructRef _, (VarRef _ | ConstRef _ | IndRef _) -> 1 let global_hash_gen hash_cst hash_ind hash_cons gr = let open Hashset.Combine in diff --git a/library/globnames.mli b/library/globnames.mli index 253c20baae..f4956e3df2 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -13,10 +13,10 @@ open Mod_subst (** {6 Global reference is a kernel side type for all references together } *) type global_reference = - | VarRef of variable - | ConstRef of constant - | IndRef of inductive - | ConstructRef of constructor + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of constant (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) val isVarRef : global_reference -> bool val isConstRef : global_reference -> bool diff --git a/library/goptions.ml b/library/goptions.ml index 4aea33685e..1c08b9539f 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,7 +9,7 @@ (* This module manages customization parameters at the vernacular level *) open Pp -open Errors +open CErrors open Util open Libobject open Libnames @@ -20,6 +20,7 @@ type option_value = | BoolValue of bool | IntValue of int option | StringValue of string + | StringOptValue of string option (** Summary of an option status *) type option_state = { @@ -35,7 +36,7 @@ type option_state = { let nickname table = String.concat " " table let error_undeclared_key key = - error ((nickname key)^": no table or option of this type") + user_err ~hdr:"Goptions" (str (nickname key) ++ str ": no table or option of this type") (****************************************************************************) (* 1- Tables *) @@ -107,7 +108,8 @@ module MakeTable = (fun c -> t := MySet.remove c !t)) let print_table table_name printer table = - pp (str table_name ++ + Feedback.msg_notice + (str table_name ++ (hov 0 (if MySet.is_empty table then str " None" ++ fnl () else MySet.fold @@ -121,7 +123,7 @@ module MakeTable = method mem x = let y = A.encode x in let answer = MySet.mem y !t in - msg_info (A.member_message y answer) + Feedback.msg_info (A.member_message y answer) method print = print_table A.title A.printer !t end @@ -206,6 +208,10 @@ type 'a option_sig = { optread : unit -> 'a; optwrite : 'a -> unit } +type option_locality = OptLocal | OptDefault | OptGlobal + +type option_mod = OptSet | OptAppend + module OptionOrd = struct type t = option_name @@ -231,48 +237,57 @@ with Not_found -> open Libobject open Lib -let declare_option cast uncast +let warn_deprecated_option = + CWarnings.create ~name:"deprecated-option" ~category:"deprecated" + (fun key -> str "Option" ++ spc () ++ str (nickname key) ++ + strbrk " is deprecated") + +let get_locality = function + | Some true -> OptLocal + | Some false -> OptGlobal + | None -> OptDefault + +let declare_option cast uncast append ?(preprocess = fun x -> x) { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = check_key key; let default = read() in - (* spiwack: I use two spaces in the nicknames of "local" and "global" objects. - That way I shouldn't collide with [nickname key] for any [key]. As [key]-s are - lists of strings *without* spaces. *) - let (write,lwrite,gwrite) = if sync then - let ldecl_obj = (* "Local": doesn't survive section or modules. *) - declare_object {(default_object ("L "^nickname key)) with - cache_function = (fun (_,v) -> write v); - classify_function = (fun _ -> Dispose)} - in - let decl_obj = (* default locality: survives sections but not modules. *) - declare_object {(default_object (nickname key)) with - cache_function = (fun (_,v) -> write v); - classify_function = (fun _ -> Dispose); - discharge_function = (fun (_,v) -> Some v)} - in - let gdecl_obj = (* "Global": survives section and modules. *) - declare_object {(default_object ("G "^nickname key)) with - cache_function = (fun (_,v) -> write v); - classify_function = (fun v -> Substitute v); - subst_function = (fun (_,v) -> v); - discharge_function = (fun (_,v) -> Some v); - load_function = (fun _ (_,v) -> write v)} - in - let _ = Summary.declare_summary (nickname key) - { Summary.freeze_function = (fun _ -> read ()); - Summary.unfreeze_function = write; - Summary.init_function = (fun () -> write default) } - in - begin fun v -> add_anonymous_leaf (decl_obj v) end , - begin fun v -> add_anonymous_leaf (ldecl_obj v) end , - begin fun v -> add_anonymous_leaf (gdecl_obj v) end - else write,write,write + let change = + if sync then + let _ = Summary.declare_summary (nickname key) + { Summary.freeze_function = (fun _ -> read ()); + Summary.unfreeze_function = write; + Summary.init_function = (fun () -> write default) } in + let cache_options (_,(l,m,v)) = + match m with + | OptSet -> write v + | OptAppend -> write (append (read ()) v) in + let load_options i o = cache_options o in + let subst_options (subst,obj) = obj in + let discharge_options (_,(l,_,_ as o)) = + match l with OptLocal -> None | _ -> Some o in + let classify_options (l,_,_ as o) = + match l with OptGlobal -> Substitute o | _ -> Dispose in + let options : option_locality * option_mod * _ -> obj = + declare_object + { (default_object (nickname key)) with + load_function = load_options; + cache_function = cache_options; + subst_function = subst_options; + discharge_function = discharge_options; + classify_function = classify_options } in + (fun l m v -> let v = preprocess v in Lib.add_anonymous_leaf (options (l, m, v))) + else + (fun _ m v -> + let v = preprocess v in + match m with + | OptSet -> write v + | OptAppend -> write (append (read ()) v)) in + let warn () = if depr then warn_deprecated_option key in let cread () = cast (read ()) in - let cwrite v = write (uncast v) in - let clwrite v = lwrite (uncast v) in - let cgwrite v = gwrite (uncast v) in - value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,clwrite,cgwrite)) !value_tab; + let cwrite l v = warn (); change l OptSet (uncast v) in + let cappend l v = warn (); change l OptAppend (uncast v) in + value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,cappend)) !value_tab; write type 'a write_function = 'a -> unit @@ -281,30 +296,38 @@ let declare_int_option = declare_option (fun v -> IntValue v) (function IntValue v -> v | _ -> anomaly (Pp.str "async_option")) + (fun _ _ -> anomaly (Pp.str "async_option")) let declare_bool_option = declare_option (fun v -> BoolValue v) (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option")) + (fun _ _ -> anomaly (Pp.str "async_option")) let declare_string_option = declare_option (fun v -> StringValue v) (function StringValue v -> v | _ -> anomaly (Pp.str "async_option")) + (fun x y -> x^","^y) +let declare_stringopt_option = + declare_option + (fun v -> StringOptValue v) + (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option")) + (fun _ _ -> anomaly (Pp.str "async_option")) (* 3- User accessible commands *) (* Setting values of options *) +let warn_unknown_option = + CWarnings.create ~name:"unknown-option" ~category:"option" + (fun key -> strbrk "There is no option " ++ + str (nickname key) ++ str ".") + let set_option_value locality check_and_cast key v = - let (name, depr, (_,read,write,lwrite,gwrite)) = - try get_option key - with Not_found -> error ("There is no option "^(nickname key)^".") - in - let write = match locality with - | None -> write - | Some true -> lwrite - | Some false -> gwrite - in - write (check_and_cast v (read ())) + let opt = try Some (get_option key) with Not_found -> None in + match opt with + | None -> warn_unknown_option key + | Some (name, depr, (_,read,write,append)) -> + write (get_locality locality) (check_and_cast v (read ())) let bad_type_error () = error "Bad type of value for this option." @@ -318,11 +341,13 @@ let check_bool_value v = function let check_string_value v = function | StringValue _ -> StringValue v + | StringOptValue _ -> StringOptValue (Some v) | _ -> bad_type_error () let check_unset_value v = function | BoolValue _ -> BoolValue false | IntValue _ -> IntValue None + | StringOptValue _ -> StringOptValue None | _ -> bad_type_error () (* Nota: For compatibility reasons, some errors are treated as @@ -332,13 +357,18 @@ let check_unset_value v = function let set_int_option_value_gen locality = set_option_value locality check_int_value let set_bool_option_value_gen locality key v = - try set_option_value locality check_bool_value key v - with UserError (_,s) -> msg_warning s + set_option_value locality check_bool_value key v let set_string_option_value_gen locality = set_option_value locality check_string_value let unset_option_value_gen locality key = - try set_option_value locality check_unset_value key () - with UserError (_,s) -> msg_warning s + set_option_value locality check_unset_value key () + +let set_string_option_append_value_gen locality key v = + let opt = try Some (get_option key) with Not_found -> None in + match opt with + | None -> warn_unknown_option key + | Some (name, depr, (_,read,write,append)) -> + append (get_locality locality) (check_string_value v (read ())) let set_int_option_value = set_int_option_value_gen None let set_bool_option_value = set_bool_option_value_gen None @@ -348,25 +378,27 @@ let set_string_option_value = set_string_option_value_gen None let msg_option_value (name,v) = match v with - | BoolValue true -> str "true" - | BoolValue false -> str "false" + | BoolValue true -> str "on" + | BoolValue false -> str "off" | IntValue (Some n) -> int n | IntValue None -> str "undefined" - | StringValue s -> str s + | StringValue s -> quote (str s) + | StringOptValue None -> str"undefined" + | StringOptValue (Some s) -> quote (str s) (* | IdentValue r -> pr_global_env Id.Set.empty r *) let print_option_value key = - let (name, depr, (_,read,_,_,_)) = get_option key in + let (name, depr, (_,read,_,_)) = get_option key in let s = read () in match s with | BoolValue b -> - msg_info (str ("The "^name^" mode is "^(if b then "on" else "off"))) + Feedback.msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) | _ -> - msg_info (str ("Current value of "^name^" is ") ++ msg_option_value (name, s)) + Feedback.msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) let get_tables () = let tables = !value_tab in - let fold key (name, depr, (sync,read,_,_,_)) accu = + let fold key (name, depr, (sync,read,_,_)) accu = let state = { opt_sync = sync; opt_name = name; @@ -379,28 +411,28 @@ let get_tables () = let print_tables () = let print_option key name value depr = - let msg = str (" "^(nickname key)^": ") ++ msg_option_value (name, value) in + let msg = str " " ++ str (nickname key) ++ str ": " ++ msg_option_value (name, value) in if depr then msg ++ str " [DEPRECATED]" ++ fnl () else msg ++ fnl () in str "Synchronous options:" ++ fnl () ++ OptionMap.fold - (fun key (name, depr, (sync,read,_,_,_)) p -> + (fun key (name, depr, (sync,read,_,_)) p -> if sync then p ++ print_option key name (read ()) depr else p) !value_tab (mt ()) ++ str "Asynchronous options:" ++ fnl () ++ OptionMap.fold - (fun key (name, depr, (sync,read,_,_,_)) p -> + (fun key (name, depr, (sync,read,_,_)) p -> if sync then p else p ++ print_option key name (read ()) depr) !value_tab (mt ()) ++ str "Tables:" ++ fnl () ++ List.fold_right - (fun (nickkey,_) p -> p ++ str (" "^nickkey) ++ fnl ()) + (fun (nickkey,_) p -> p ++ str " " ++ str nickkey ++ fnl ()) !string_table (mt ()) ++ List.fold_right - (fun (nickkey,_) p -> p ++ str (" "^nickkey) ++ fnl ()) + (fun (nickkey,_) p -> p ++ str " " ++ str nickkey ++ fnl ()) !ref_table (mt ()) ++ fnl () diff --git a/library/goptions.mli b/library/goptions.mli index 1c44f89081..3b3651f393 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -122,17 +122,24 @@ type 'a option_sig = { (** When an option is declared synchronous ([optsync] is [true]), the output is a synchronous write function. Otherwise it is [optwrite] *) +(** The [preprocess] function is triggered before setting the option. It can be + used to emit a warning on certain values, and clean-up the final value. *) type 'a write_function = 'a -> unit -val declare_int_option : int option option_sig -> int option write_function -val declare_bool_option : bool option_sig -> bool write_function -val declare_string_option: string option_sig -> string write_function +val declare_int_option : ?preprocess:(int option -> int option) -> + int option option_sig -> int option write_function +val declare_bool_option : ?preprocess:(bool -> bool) -> + bool option_sig -> bool write_function +val declare_string_option: ?preprocess:(string -> string) -> + string option_sig -> string write_function +val declare_stringopt_option: ?preprocess:(string option -> string option) -> + string option option_sig -> string option write_function (** {6 Special functions supposed to be used only in vernacentries.ml } *) -module OptionMap : Map.S with type key = option_name +module OptionMap : CSig.MapS with type key = option_name val get_string_table : option_name -> @@ -153,6 +160,7 @@ val get_ref_table : val set_int_option_value_gen : bool option -> option_name -> int option -> unit val set_bool_option_value_gen : bool option -> option_name -> bool -> unit val set_string_option_value_gen : bool option -> option_name -> string -> unit +val set_string_option_append_value_gen : bool option -> option_name -> string -> unit val unset_option_value_gen : bool option -> option_name -> unit val set_int_option_value : option_name -> int option -> unit @@ -165,6 +173,7 @@ type option_value = | BoolValue of bool | IntValue of int option | StringValue of string + | StringOptValue of string option (** Summary of an option status *) type option_state = { diff --git a/library/heads.ml b/library/heads.ml index 5c153b0676..02465f22fc 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -15,6 +15,7 @@ open Environ open Globnames open Libobject open Lib +open Context.Named.Declaration (** Characterization of the head of a term *) @@ -63,12 +64,15 @@ let kind_of_head env t = (try on_subterm k l b (variable_head id) with Not_found -> (* a goal variable *) - match pi2 (lookup_named id env) with - | Some c -> aux k l c b - | None -> NotImmediatelyComputableHead) + match lookup_named id env with + | LocalDef (_,c,_) -> aux k l c b + | LocalAssum _ -> NotImmediatelyComputableHead) | Const (cst,_) -> (try on_subterm k l b (constant_head cst) - with Not_found -> assert false) + with Not_found -> + CErrors.anomaly + Pp.(str "constant not found in kind_of_head: " ++ + str (Names.Constant.to_string cst))) | Construct _ | CoFix _ -> if b then NotImmediatelyComputableHead else ConstructorHead | Sort _ | Ind _ | Prod _ -> RigidHead RigidType @@ -129,8 +133,8 @@ let compute_head = function | None -> RigidHead (RigidParameter cst) | Some c -> kind_of_head env c) | EvalVarRef id -> - (match pi2 (Global.lookup_named id) with - | Some c when not (Decls.variable_opacity id) -> + (match Global.lookup_named id with + | LocalDef (_,c,_) when not (Decls.variable_opacity id) -> kind_of_head (Global.env()) c | _ -> RigidHead (RigidVar id)) diff --git a/library/heads.mli b/library/heads.mli index 52f43824fd..5acf5f54f7 100644 --- a/library/heads.mli +++ b/library/heads.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/impargs.ml b/library/impargs.ml index 4b0e2e3d1a..836568b890 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -1,15 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Globnames +open Nameops open Term open Reduction open Declarations @@ -21,6 +22,9 @@ open Constrexpr open Termops open Namegen open Decl_kinds +open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (*s Flags governing the computation of implicit arguments *) @@ -67,15 +71,14 @@ let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern let is_contextual_implicit_args () = !implicit_args.contextual let is_maximal_implicit_args () = !implicit_args.maximal -let with_implicits flags f x = +let with_implicit_protection f x = let oflags = !implicit_args in try - implicit_args := flags; let rslt = f x in implicit_args := oflags; rslt with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in let () = implicit_args := oflags in iraise reraise @@ -103,7 +106,7 @@ 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. +- [Manual] means the argument has been explicitly set as implicit. We also consider arguments inferable from the conclusion but it is operational only if [conclusion_matters] is true. @@ -172,8 +175,7 @@ let is_flexible_reference env bound depth f = let cb = Environ.lookup_constant kn env in (match cb.const_body with Def _ -> true | _ -> false) | Var id -> - let (_, value, _) = Environ.lookup_named id env in - begin match value with None -> false | _ -> true end + env |> Environ.lookup_named id |> is_local_def | Ind _ | Construct _ -> false | _ -> true @@ -187,7 +189,7 @@ let is_reversible_pattern bound depth f l = (* Precondition: rels in env are for inductive types only *) let add_free_rels_until strict strongly_strict revpat bound env m pos acc = let rec frec rig (env,depth as ed) c = - let hd = if strict then whd_betadeltaiota env c else c in + let hd = if strict then whd_all env c else c in let c = if strongly_strict then hd else c in match kind_of_term hd with | Rel n when (n < bound+depth) && (n >= depth) -> @@ -233,13 +235,14 @@ let find_displayed_name_in all avoid na (_,b as envnames_b) = let compute_implicits_gen strict strongly_strict revpat contextual all env t = let rigid = ref true in + let open Context.Rel.Declaration in let rec aux env avoid n names t = - let t = whd_betadeltaiota env t in + let t = whd_all env t in match kind_of_term t with | Prod (na,a,b) -> let na',avoid' = find_displayed_name_in all avoid na (names,b) in add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1)) - (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b) + (aux (push_rel (LocalAssum (na',a)) env) avoid' (n+1) (na'::names) b) | _ -> rigid := is_rigid_head t; let names = List.rev names in @@ -248,10 +251,10 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = add_free_rels_until strict strongly_strict revpat n env t Conclusion v else v in - match kind_of_term (whd_betadeltaiota env t) with + match kind_of_term (whd_all env t) with | Prod (na,a,b) -> let na',avoid = find_displayed_name_in all [] na ([],b) in - let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in + let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in !rigid, Array.to_list v | _ -> true, [] @@ -337,12 +340,14 @@ let check_correct_manual_implicits autoimps l = List.iter (function | ExplByName id,(b,fi,forced) -> if not forced then - error ("Wrong or non-dependent implicit argument name: "^(Id.to_string id)^".") + user_err + (str "Wrong or non-dependent implicit argument name: " ++ pr_id id ++ str ".") | ExplByPos (i,_id),_t -> if i<1 || i>List.length autoimps then - error ("Bad implicit argument number: "^(string_of_int i)^".") + user_err + (str "Bad implicit argument number: " ++ int i ++ str ".") else - errorlabstrm "" + user_err (str "Cannot set implicit argument number " ++ int i ++ str ": it has no name.")) l @@ -424,7 +429,7 @@ let compute_mib_implicits flags manual kn = (Array.mapi (* No need to lift, arities contain no de Bruijn *) (fun i mip -> (** No need to care about constraints here *) - (Name mip.mind_typename, None, Global.type_of_global_unsafe (IndRef (kn,i)))) + Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, Global.type_of_global_unsafe (IndRef (kn,i)))) mib.mind_packets) in let env_ar = push_rel_context ar env in let imps_one_inductive i mip = @@ -446,8 +451,7 @@ let compute_all_mib_implicits flags manual kn = let compute_var_implicits flags manual id = let env = Global.env () in - let (_,_,ty) = lookup_named id env in - compute_semi_auto_implicits env flags manual ty + compute_semi_auto_implicits env flags manual (NamedDecl.get_type (lookup_named id env)) (* Implicits of a global reference. *) @@ -488,13 +492,15 @@ let implicits_of_global ref = let l = Refmap.find ref !implicits_table in try let rename_l = Arguments_renaming.arguments_names ref in - let rename imp name = match imp, name with - | Some (_, x,y), Name id -> Some (id, x,y) - | _ -> imp in - List.map2 (fun (t, il) rl -> t, List.map2 rename il rl) l rename_l + let rec rename implicits names = match implicits, names with + | [], _ -> [] + | _, [] -> implicits + | Some (_, x,y) :: implicits, Name id :: names -> + Some (id, x,y) :: rename implicits names + | imp :: implicits, _ :: names -> imp :: rename implicits names + in + List.map (fun (t, il) -> t, rename il rename_l) l with Not_found -> l - | Invalid_argument _ -> - anomaly (Pp.str "renamings list and implicits list have different lenghts") with Not_found -> [DefaultImpArgs,[]] let cache_implicits_decl (ref,imps) = @@ -512,21 +518,11 @@ let subst_implicits (subst,(req,l)) = (ImplLocal,List.smartmap (subst_implicits_decl subst) l) let impls_of_context ctx = - let map (id, impl, _, _) = match impl with - | Implicit -> Some (id, Manual, (true, true)) + let map (decl, impl) = match impl with + | Implicit -> Some (NamedDecl.get_id decl, Manual, (true, true)) | _ -> None in - let is_set (_, _, b, _) = match b with - | None -> true - | Some _ -> false - in - List.rev_map map (List.filter is_set ctx) - -let section_segment_of_reference = function - | ConstRef con -> pi1 (section_segment_of_constant con) - | IndRef (kn,_) | ConstructRef ((kn,_),_) -> - pi1 (section_segment_of_mutual_inductive kn) - | _ -> [] + List.rev_map map (List.filter (fst %> is_local_assum) ctx) let adjust_side_condition p = function | LessArgsThan n -> LessArgsThan (n+p) @@ -541,7 +537,7 @@ let discharge_implicits (_,(req,l)) = | ImplLocal -> None | ImplInteractive (ref,flags,exp) -> (try - let vars = section_segment_of_reference ref in + let vars = variable_section_segment_of_reference ref in let ref' = if isVarRef ref then ref else pop_global_reference ref in let extra_impls = impls_of_context vars in let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in @@ -559,7 +555,7 @@ let discharge_implicits (_,(req,l)) = | ImplMutualInductive (kn,flags) -> (try let l' = List.map (fun (gr, l) -> - let vars = section_segment_of_reference gr in + let vars = variable_section_segment_of_reference gr in let extra_impls = impls_of_context vars in ((if isVarRef gr then gr else pop_global_reference gr), List.map (add_section_impls vars extra_impls) l)) l @@ -660,14 +656,14 @@ let check_inclusion l = let rec aux = function | n1::(n2::_ as nl) -> if n1 <= n2 then - error "Sequences of implicit arguments must be of different lengths"; + error "Sequences of implicit arguments must be of different lengths."; aux nl | _ -> () in aux (List.map (fun (imps,_) -> List.length imps) l) let check_rigidity isrigid = if not isrigid then - errorlabstrm "" (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.") + user_err (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.") let projection_implicits env p impls = let pb = Environ.lookup_projection p env in diff --git a/library/impargs.mli b/library/impargs.mli index 1d3a73e94c..3919a519c9 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -29,8 +29,7 @@ val is_reversible_pattern_implicit_args : unit -> bool val is_contextual_implicit_args : unit -> bool val is_maximal_implicit_args : unit -> bool -type implicits_flags -val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b +val with_implicit_protection : ('a -> 'b) -> 'a -> 'b (** {6 ... } *) (** An [implicits_list] is a list of positions telling which arguments @@ -59,8 +58,8 @@ type implicit_explanation = inferable following a rigid path (useful to know how to print a partial application) *) | Manual - (** means the argument has been explicitely set as implicit. *) - + (** means the argument has been explicitly set as implicit. *) + (** We also consider arguments inferable from the conclusion but it is operational only if [conclusion_matters] is true. *) @@ -136,14 +135,5 @@ val select_impargs_size : int -> implicits_list list -> implicit_status list val select_stronger_impargs : implicits_list list -> implicit_status list -type implicit_interactive_request - -type implicit_discharge_request = - | ImplLocal - | ImplConstant of constant * implicits_flags - | ImplMutualInductive of mutual_inductive * implicits_flags - | ImplInteractive of global_reference * implicits_flags * - implicit_interactive_request - val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool (** Equality on [explicitation]. *) diff --git a/library/keys.ml b/library/keys.ml index 3d277476f1..057dc3b65d 100644 --- a/library/keys.ml +++ b/library/keys.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,35 +12,31 @@ open Globnames open Term open Libobject -type key = +type key = | KGlob of global_reference - | KLam + | KLam | KLet | KProd | KSort - | KEvar - | KCase - | KFix + | KCase + | KFix | KCoFix - | KRel - | KMeta + | KRel module KeyOrdered = struct type t = key let hash gr = match gr with - | KGlob gr -> 10 + RefOrdered.hash gr + | KGlob gr -> 8 + RefOrdered.hash gr | KLam -> 0 | KLet -> 1 | KProd -> 2 | KSort -> 3 - | KEvar -> 4 - | KCase -> 5 - | KFix -> 6 - | KCoFix -> 7 - | KRel -> 8 - | KMeta -> 9 + | KCase -> 4 + | KFix -> 5 + | KCoFix -> 6 + | KRel -> 7 let compare gr1 gr2 = match gr1, gr2 with @@ -62,8 +58,6 @@ module Keyset = Keymap.Set (* Mapping structure for references to be considered equivalent *) -type keys = Keyset.t Keymap.t - let keys = Summary.ref Keymap.empty ~name:"Keys_decl" let add_kv k v m = @@ -153,12 +147,10 @@ let pr_key pr_global = function | KLet -> str"Let" | KProd -> str"Product" | KSort -> str"Sort" - | KEvar -> str"Evar" | KCase -> str"Case" | KFix -> str"Fix" | KCoFix -> str"CoFix" | KRel -> str"Rel" - | KMeta -> str"Meta" let pr_keyset pr_global v = prlist_with_sep spc (pr_key pr_global) (Keyset.elements v) diff --git a/library/keys.mli b/library/keys.mli index bfbb4c58f6..69668590d6 100644 --- a/library/keys.mli +++ b/library/keys.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/kindops.ml b/library/kindops.ml index 5604864737..21b1bec33c 100644 --- a/library/kindops.ml +++ b/library/kindops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -25,7 +25,7 @@ let string_of_theorem_kind = function let string_of_definition_kind def = let (locality, poly, kind) = def in - let error () = Errors.anomaly (Pp.str "Internal definition kind") in + let error () = CErrors.anomaly (Pp.str "Internal definition kind") in match kind with | Definition -> begin match locality with @@ -64,4 +64,4 @@ let string_of_definition_kind def = | Global -> "Global Instance" end | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> - Errors.anomaly (Pp.str "Internal definition kind") + CErrors.anomaly (Pp.str "Internal definition kind") diff --git a/library/kindops.mli b/library/kindops.mli index cd2e39cf85..3e95eaa7d9 100644 --- a/library/kindops.mli +++ b/library/kindops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/lib.ml b/library/lib.ml index 9977b66654..4fd29a94de 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -1,18 +1,21 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Pp -open Errors +open CErrors open Util open Libnames open Globnames open Nameops open Libobject +open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration type is_type = bool (* Module Type or just Module *) type export = bool option (* None for a Module Type *) @@ -75,7 +78,8 @@ let classify_segment seg = | (_,ClosedModule _) :: stk -> clean acc stk | (_,OpenedSection _) :: _ -> error "there are still opened sections" | (_,OpenedModule (ty,_,_,_)) :: _ -> - error ("there are still opened " ^ module_kind ty ^"s") + user_err ~hdr:"Lib.classify_segment" + (str "there are still opened " ++ str (module_kind ty) ++ str "s") | (_,FrozenState _) :: stk -> clean acc stk in clean ([],[],[]) (List.rev seg) @@ -197,6 +201,9 @@ let split_lib_at_opening sp = let add_entry sp node = lib_stk := (sp,node) :: !lib_stk +let pull_to_head oname = + lib_stk := (oname,List.assoc oname !lib_stk) :: List.remove_assoc oname !lib_stk + let anonymous_id = let n = ref 0 in fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n)) @@ -227,11 +234,16 @@ let add_leaves id objs = List.iter add_obj objs; oname -let add_anonymous_leaf obj = +let add_anonymous_leaf ?(cache_first = true) obj = let id = anonymous_id () in let oname = make_oname id in - cache_object (oname,obj); - add_entry oname (Leaf obj) + if cache_first then begin + cache_object (oname,obj); + add_entry oname (Leaf obj) + end else begin + add_entry oname (Leaf obj); + cache_object (oname,obj) + end let add_frozen_state () = add_anonymous_entry @@ -263,7 +275,7 @@ let start_mod is_type export id mp fs = else Nametab.exists_module dir in if exists then - errorlabstrm "open_module" (pr_id id ++ str " already exists"); + user_err ~hdr:"open_module" (pr_id id ++ str " already exists"); add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs)); path_prefix := prefix; prefix @@ -273,8 +285,8 @@ let start_modtype = start_mod true None let error_still_opened string oname = let id = basename (fst oname) in - errorlabstrm "" - (str ("The "^string^" ") ++ pr_id id ++ str " is still opened.") + user_err + (str "The " ++ str string ++ str " " ++ pr_id id ++ str " is still opened.") let end_mod is_type = let oname,fs = @@ -318,7 +330,8 @@ let end_compilation_checks dir = try match snd (find_entry_p is_opening_node) with | OpenedSection _ -> error "There are some open sections." | OpenedModule (ty,_,_,_) -> - error ("There are some open "^module_kind ty^"s.") + user_err ~hdr:"Lib.end_compilation_checks" + (str "There are some open " ++ str (module_kind ty) ++ str "s.") | _ -> assert false with Not_found -> () in @@ -369,7 +382,8 @@ let find_opening_node id = let oname,entry = find_entry_p is_opening_node in let id' = basename (fst oname) in if not (Names.Id.equal id id') then - error ("Last block to end has name "^(Names.Id.to_string id')^"."); + user_err ~hdr:"Lib.find_opening_node" + (str "Last block to end has name " ++ pr_id id' ++ str "."); entry with Not_found -> error "There is nothing to end." @@ -382,66 +396,84 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types +type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t +type secentry = + | Variable of (Names.Id.t * Decl_kinds.binding_kind * + Decl_kinds.polymorphic * Univ.universe_context_set) + | Context of Univ.universe_context_set + let sectab = - Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind * - Decl_kinds.polymorphic * Univ.universe_context_set) list * - Opaqueproof.work_list * abstr_list) list) + Summary.ref ([] : (secentry list * Opaqueproof.work_list * abstr_list) list) ~name:"section-context" let add_section () = sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty), (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab +let check_same_poly p vars = + let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in + if List.exists pred vars then + error "Cannot mix universe polymorphic and monomorphic declarations in sections." + let add_section_variable id impl poly ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | (vars,repl,abs)::sl -> - sectab := ((id,impl,poly,ctx)::vars,repl,abs)::sl + List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab; + sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl + +let add_section_context ctx = + match !sectab with + | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) + | (vars,repl,abs)::sl -> + check_same_poly true vars; + sectab := (Context ctx :: vars,repl,abs)::sl let extract_hyps (secs,ohyps) = let rec aux = function - | ((id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' -> + | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> let l, r = aux (idl,hyps) in - (id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r - | ((_,_,poly,ctx)::idl,hyps) -> + (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r + | (Variable (_,_,poly,ctx)::idl,hyps) -> let l, r = aux (idl,hyps) in l, if poly then Univ.ContextSet.union r ctx else r + | (Context ctx :: idl, hyps) -> + let l, r = aux (idl, hyps) in + l, Univ.ContextSet.union r ctx | [], _ -> [],Univ.ContextSet.empty in aux (secs,ohyps) -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 instance_from_variable_context = + List.map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list -let named_of_variable_context ctx = List.map (fun (id,_,b,t) -> (id,b,t)) ctx +let named_of_variable_context = + List.map fst -let add_section_replacement f g hyps = +let add_section_replacement f g poly hyps = match !sectab with | [] -> () | (vars,exps,abs)::sl -> + let () = check_same_poly poly vars in let sechyps,ctx = extract_hyps (vars,hyps) in let ctx = Univ.ContextSet.to_context ctx in let subst, ctx = Univ.abstract_universes true ctx in let args = instance_from_variable_context (List.rev sechyps) in - sectab := (vars,f (Univ.UContext.instance ctx,args) exps,g (sechyps,subst,ctx) abs)::sl + sectab := (vars,f (Univ.UContext.instance ctx,args) exps, + g (sechyps,subst,ctx) abs)::sl -let add_section_kn kn = +let add_section_kn poly kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in - add_section_replacement f f + add_section_replacement f f poly -let add_section_constant is_projection kn = +let add_section_constant poly kn = let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in - add_section_replacement f f + add_section_replacement f f poly let replacement_context () = pi2 (List.hd !sectab) @@ -451,12 +483,21 @@ let section_segment_of_constant con = let section_segment_of_mutual_inductive kn = Names.Mindmap.find kn (snd (pi3 (List.hd !sectab))) +let variable_section_segment_of_reference = function + | ConstRef con -> pi1 (section_segment_of_constant con) + | IndRef (kn,_) | ConstructRef ((kn,_),_) -> + pi1 (section_segment_of_mutual_inductive kn) + | _ -> [] + let section_instance = function | VarRef id -> - if List.exists (fun (id',_,_,_) -> Names.id_eq id id') - (pi1 (List.hd !sectab)) - then Univ.Instance.empty, [||] - else raise Not_found + let eq = function + | Variable (id',_,_,_) -> Names.id_eq id id' + | Context _ -> false + in + if List.exists eq (pi1 (List.hd !sectab)) + then Univ.Instance.empty, [||] + else raise Not_found | ConstRef con -> Names.Cmap.find con (fst (pi2 (List.hd !sectab))) | IndRef (kn,_) | ConstructRef ((kn,_),_) -> @@ -465,27 +506,25 @@ let section_instance = function let is_in_section ref = try ignore (section_instance ref); true with Not_found -> false -let full_replacement_context () = List.map pi2 !sectab -let full_section_segment_of_constant con = - List.map (fun (vars,_,(x,_)) -> fun hyps -> - named_of_variable_context - (try pi1 (Names.Cmap.find con x) - with Not_found -> fst (extract_hyps (vars, hyps)))) !sectab - (*************) (* Sections. *) +(* XML output hooks *) +let (f_xml_open_section, xml_open_section) = Hook.make ~default:ignore () +let (f_xml_close_section, xml_close_section) = Hook.make ~default:ignore () + let open_section id = let olddir,(mp,oldsec) = !path_prefix in let dir = add_dirpath_suffix olddir id in let prefix = dir, (mp, add_dirpath_suffix oldsec id) in if Nametab.exists_section dir then - errorlabstrm "open_section" (pr_id id ++ str " already exists."); + user_err ~hdr:"open_section" (pr_id id ++ str " already exists."); let fs = Summary.freeze_summaries ~marshallable:`No in add_entry (make_oname id) (OpenedSection (prefix, fs)); (*Pushed for the lifetime of the section: removed by unfrozing the summary*) Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); path_prefix := prefix; + if !Flags.xml_export then Hook.get f_xml_open_section id; add_section () @@ -514,6 +553,7 @@ let close_section () = let full_olddir = fst !path_prefix in pop_path_prefix (); add_entry oname (ClosedSection (List.rev (mark::secdecls))); + if !Flags.xml_export then Hook.get f_xml_close_section (basename (fst oname)); let newdecls = List.map discharge_item secdecls in Summary.unfreeze_summaries fs; List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls; @@ -566,15 +606,6 @@ let rec dp_of_mp = function |Names.MPbound _ -> library_dp () |Names.MPdot (mp,_) -> dp_of_mp mp -let rec split_mp = function - |Names.MPfile dp -> dp, Names.DirPath.empty - |Names.MPdot (prfx, lbl) -> - let mprec, dprec = split_mp prfx in - mprec, Libnames.add_dirpath_suffix dprec (Names.Label.to_id lbl) - |Names.MPbound mbid -> - let (_,id,dp) = Names.MBId.repr mbid in - library_dp (), Names.DirPath.make [id] - let rec split_modpath = function |Names.MPfile dp -> dp, [] |Names.MPbound mbid -> library_dp (), [Names.MBId.to_id mbid] @@ -586,20 +617,6 @@ let library_part = function |VarRef id -> library_dp () |ref -> dp_of_mp (mp_of_global ref) -let remove_section_part ref = - let sp = Nametab.path_of_global ref in - let dir,_ = repr_path sp in - match ref with - | VarRef id -> - anomaly (Pp.str "remove_section_part not supported on local variables") - | _ -> - if is_dirpath_prefix_of dir (cwd ()) then - (* Not yet (fully) discharged *) - pop_dirpath_n (sections_depth ()) (cwd ()) - else - (* Theorem/Lemma outside its outer section of definition *) - dir - (************************) (* Discharging names *) diff --git a/library/lib.mli b/library/lib.mli index 9c4d26c5b2..9f9d8c7e5f 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -54,7 +54,8 @@ val segment_of_objects : current list of operations (most recent ones coming first). *) val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name -val add_anonymous_leaf : Libobject.obj -> unit +val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit +val pull_to_head : Libnames.object_name -> unit (** this operation adds all objects with the same name and calls [load_object] for each of them *) @@ -137,10 +138,8 @@ val library_dp : unit -> Names.DirPath.t (** Extract the library part of a name even if in a section *) val dp_of_mp : Names.module_path -> Names.DirPath.t -val split_mp : Names.module_path -> Names.DirPath.t * Names.DirPath.t val split_modpath : Names.module_path -> Names.DirPath.t * Names.Id.t list val library_part : Globnames.global_reference -> Names.DirPath.t -val remove_section_part : Globnames.global_reference -> Names.DirPath.t (** {6 Sections } *) @@ -156,26 +155,31 @@ val unfreeze : frozen -> unit val init : unit -> unit +(** XML output hooks *) +val xml_open_section : (Names.Id.t -> unit) Hook.t +val xml_close_section : (Names.Id.t -> unit) Hook.t + (** {6 Section management for discharge } *) -type variable_info = Names.Id.t * Decl_kinds.binding_kind * - Term.constr option * Term.types +type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t val instance_from_variable_context : variable_context -> Names.Id.t array -val named_of_variable_context : variable_context -> Context.named_context +val named_of_variable_context : variable_context -> Context.Named.t val section_segment_of_constant : Names.constant -> abstr_info val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info - +val variable_section_segment_of_reference : Globnames.global_reference -> variable_context + val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array val is_in_section : Globnames.global_reference -> bool val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit - -val add_section_constant : bool (* is_projection *) -> - Names.constant -> Context.named_context -> unit -val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit +val add_section_context : Univ.universe_context_set -> unit +val add_section_constant : Decl_kinds.polymorphic -> + Names.constant -> Context.Named.t -> unit +val add_section_kn : Decl_kinds.polymorphic -> + Names.mutual_inductive -> Context.Named.t -> unit val replacement_context : unit -> Opaqueproof.work_list (** {6 Discharge: decrease the section level if in the current section } *) @@ -184,10 +188,3 @@ val discharge_kn : Names.mutual_inductive -> Names.mutual_inductive val discharge_con : Names.constant -> Names.constant val discharge_global : Globnames.global_reference -> Globnames.global_reference val discharge_inductive : Names.inductive -> Names.inductive - -(* discharging a constant in one go *) -val full_replacement_context : unit -> Opaqueproof.work_list list -val full_section_segment_of_constant : - Names.constant -> (Context.named_context -> Context.named_context) list - - diff --git a/library/libnames.ml b/library/libnames.ml index f2a9d041d1..dd74e192ff 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -1,19 +1,19 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Pp -open Errors +open CErrors open Util open Names (**********************************************) -let pr_dirpath sl = (str (DirPath.to_string sl)) +let pr_dirpath sl = str (DirPath.to_string sl) (*s Operations on dirpaths *) @@ -32,6 +32,11 @@ let is_dirpath_prefix_of d1 d2 = List.prefix_of Id.equal (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) +let is_dirpath_suffix_of dir1 dir2 = + let dir1 = DirPath.repr dir1 in + let dir2 = DirPath.repr dir2 in + List.prefix_of Id.equal dir1 dir2 + let chop_dirpath n d = let d1,d2 = List.chop n (List.rev (DirPath.repr d)) in DirPath.make (List.rev d1), DirPath.make (List.rev d2) @@ -192,7 +197,7 @@ let string_of_reference = function let pr_reference = function | Qualid (_,qid) -> pr_qualid qid - | Ident (_,id) -> str (Id.to_string id) + | Ident (_,id) -> Id.print id let loc_of_reference = function | Qualid (loc,qid) -> loc diff --git a/library/libnames.mli b/library/libnames.mli index 3b5feb94e8..58d1da9d64 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -37,6 +37,8 @@ val append_dirpath : DirPath.t -> DirPath.t -> DirPath.t val drop_dirpath_prefix : DirPath.t -> DirPath.t -> DirPath.t val is_dirpath_prefix_of : DirPath.t -> DirPath.t -> bool +val is_dirpath_suffix_of : DirPath.t -> DirPath.t -> bool + module Dirset : Set.S with type elt = DirPath.t module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset @@ -58,7 +60,7 @@ val path_of_string : string -> full_path val string_of_path : full_path -> string val pr_path : full_path -> std_ppcmds -module Spmap : Map.S with type key = full_path +module Spmap : CSig.MapS with type key = full_path val restrict_path : int -> full_path -> full_path diff --git a/library/libobject.ml b/library/libobject.ml index 5f2a2127d9..caa03c85be 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -1,24 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Libnames +open Pp +open Util -(* 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 limited 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;; +module Dyn = Dyn.Make(struct end) type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a @@ -33,15 +25,13 @@ type 'a object_declaration = { discharge_function : object_name * 'a -> 'a option; rebuild_function : 'a -> 'a } -let yell s = Errors.anomaly (Pp.str 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!")); + CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!")); classify_function = (fun obj -> Keep obj); discharge_function = (fun _ -> None); rebuild_function = (fun x -> x)} @@ -71,15 +61,14 @@ type dynamic_object_declaration = { dyn_discharge_function : object_name * obj -> obj option; dyn_rebuild_function : obj -> obj } -let object_tag = Dyn.tag -let object_has_tag = Dyn.has_tag +let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t let cache_tab = (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) let declare_object_full odecl = let na = odecl.object_name in - let (infun,outfun) = Dyn.create na in + let (infun, outfun) = Dyn.Easy.make_dyn na in let cacher (oname,lobj) = odecl.cache_function (oname,outfun lobj) and loader i (oname,lobj) = odecl.load_function i (oname,outfun lobj) and opener i (oname,lobj) = odecl.open_function i (oname,outfun lobj) @@ -102,33 +91,27 @@ let declare_object_full odecl = dyn_rebuild_function = rebuild }; (infun,outfun) -let declare_object odecl = fst (declare_object_full odecl) +(* The "try .. with .. " allows for correct printing when calling + declare_object a loading time. +*) -let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t) +let declare_object odecl = + try fst (declare_object_full odecl) + with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e) +let declare_object_full odecl = + try declare_object_full odecl + with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e) (* 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. *) + are triggered. *) 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 -> - failwith "local to_apply_dyn_fun" in - f dodecl - with - Failure "local to_apply_dyn_fun" -> - if not (!relax_flag || Hashtbl.mem missing_tab tag) then - begin - Pp.msg_warning - (Pp.str ("Cannot find library functions for an object with tag " - ^ tag ^ " (a plugin may be missing)")); - Hashtbl.add missing_tab tag () - end; - deflt + let dodecl = + try Hashtbl.find cache_tab tag + with Not_found -> assert false + in + f dodecl let cache_object ((_,lobj) as node) = apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj @@ -150,3 +133,5 @@ let discharge_object ((_,lobj) as node) = let rebuild_object lobj = apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj + +let dump = Dyn.dump diff --git a/library/libobject.mli b/library/libobject.mli index 099381897f..51b9af059f 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -99,7 +99,6 @@ val declare_object : 'a object_declaration -> ('a -> obj) val object_tag : obj -> string -val object_has_tag : obj -> string -> bool val cache_object : object_name * obj -> unit val load_object : int -> object_name * obj -> unit @@ -108,4 +107,7 @@ val subst_object : substitution * obj -> obj val classify_object : obj -> obj substitutivity val discharge_object : object_name * obj -> obj option val rebuild_object : obj -> obj -val relax : bool -> unit + +(** {6 Debug} *) + +val dump : unit -> (int * string) list diff --git a/library/library.ml b/library/library.ml index b078e2c478..3086e3d182 100644 --- a/library/library.ml +++ b/library/library.ml @@ -1,13 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Pp -open Errors +open CErrors open Util open Names @@ -17,37 +17,102 @@ open Libobject open Lib (************************************************************************) +(*s Low-level interning/externing of libraries to files *) + +let raw_extern_library f = + System.raw_extern_state Coq_config.vo_magic_number f + +let raw_intern_library f = + System.with_magic_number_check + (System.raw_intern_state Coq_config.vo_magic_number) f + +(************************************************************************) +(** Serialized objects loaded on-the-fly *) + +exception Faulty of string + +module Delayed : +sig + +type 'a delayed +val in_delayed : string -> in_channel -> 'a delayed * Digest.t +val fetch_delayed : 'a delayed -> 'a + +end = +struct + +type 'a delayed = { + del_file : string; + del_off : int; + del_digest : Digest.t; +} + +let in_delayed f ch = + let pos = pos_in ch in + let _, digest = System.skip_in_segment f ch in + ({ del_file = f; del_digest = digest; del_off = pos; }, digest) + +(** Fetching a table of opaque terms at position [pos] in file [f], + expecting to find first a copy of [digest]. *) + +let fetch_delayed del = + let { del_digest = digest; del_file = f; del_off = pos; } = del in + try + let ch = raw_intern_library f in + let () = seek_in ch pos in + let obj, _, digest' = System.marshal_in_segment f ch in + let () = close_in ch in + if not (String.equal digest digest') then raise (Faulty f); + obj + with e when CErrors.noncritical e -> raise (Faulty f) + +end + +open Delayed + + +(************************************************************************) (*s Modules on disk contain the following informations (after the magic number, and before the digest). *) type compilation_unit_name = DirPath.t type library_disk = { - md_name : compilation_unit_name; md_compiled : Safe_typing.compiled_library; md_objects : Declaremods.library_objects; +} + +type summary_disk = { + md_name : compilation_unit_name; + md_imports : compilation_unit_name array; md_deps : (compilation_unit_name * Safe_typing.vodigest) array; - md_imports : compilation_unit_name array } +} (*s Modules loaded in memory contain the following informations. They are kept in the global table [libraries_table]. *) type library_t = { library_name : compilation_unit_name; - library_compiled : Safe_typing.compiled_library; - library_objects : Declaremods.library_objects; + library_data : library_disk delayed; library_deps : (compilation_unit_name * Safe_typing.vodigest) array; library_imports : compilation_unit_name array; library_digests : Safe_typing.vodigest; library_extra_univs : Univ.universe_context_set; } +type library_summary = { + libsum_name : compilation_unit_name; + libsum_digests : Safe_typing.vodigest; + libsum_imports : compilation_unit_name array; +} + module LibraryOrdered = DirPath module LibraryMap = Map.Make(LibraryOrdered) module LibraryFilenameMap = Map.Make(LibraryOrdered) (* This is a map from names to loaded libraries *) -let libraries_table = Summary.ref LibraryMap.empty ~name:"LIBRARY" +let libraries_table : library_summary LibraryMap.t ref = + Summary.ref LibraryMap.empty ~name:"LIBRARY" (* This is the map of loaded libraries filename *) (* (not synchronized so as not to be caught in the states on disk) *) @@ -66,7 +131,8 @@ let find_library dir = let try_find_library dir = try find_library dir with Not_found -> - error ("Unknown library " ^ (DirPath.to_string dir)) + user_err ~hdr:"Library.find_library" + (str "Unknown library " ++ pr_dirpath dir) let register_library_filename dir f = (* Not synchronized: overwrite the previous binding if one existed *) @@ -89,32 +155,31 @@ let library_is_loaded dir = with Not_found -> false let library_is_opened dir = - List.exists (fun m -> DirPath.equal m.library_name dir) !libraries_imports_list + List.exists (fun name -> DirPath.equal name dir) !libraries_imports_list -let loaded_libraries () = - List.map (fun m -> m.library_name) !libraries_loaded_list +let loaded_libraries () = !libraries_loaded_list -let opened_libraries () = - List.map (fun m -> m.library_name) !libraries_imports_list +let opened_libraries () = !libraries_imports_list (* If a library is loaded several time, then the first occurrence must be performed first, thus the libraries_loaded_list ... *) let register_loaded_library m = + let libname = m.libsum_name in let link m = - let dirname = Filename.dirname (library_full_filename m.library_name) in - let prefix = Nativecode.mod_uid_of_dirpath m.library_name ^ "." in + let dirname = Filename.dirname (library_full_filename libname) in + let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in let f = prefix ^ "cmo" in let f = Dynlink.adapt_filename f in - if not !Flags.no_native_compiler then + if not Coq_config.no_native_compiler then Nativelib.link_library ~prefix ~dirname ~basename:f in let rec aux = function - | [] -> link m; [m] - | m'::_ as l when DirPath.equal m'.library_name m.library_name -> l + | [] -> link m; [libname] + | m'::_ as l when DirPath.equal m' libname -> l | m'::l' -> m' :: aux l' in libraries_loaded_list := aux !libraries_loaded_list; - libraries_table := LibraryMap.add m.library_name m !libraries_table + libraries_table := LibraryMap.add libname m !libraries_table (* ... while if a library is imported/exported several time, then only the last occurrence is really needed - though the imported @@ -125,7 +190,7 @@ let register_loaded_library m = let rec remember_last_of_each l m = match l with | [] -> [m] - | m'::l' when DirPath.equal m'.library_name m.library_name -> remember_last_of_each l' m + | m'::l' when DirPath.equal m' m -> remember_last_of_each l' m | m'::l' -> m' :: remember_last_of_each l' m let register_open_library export m = @@ -139,17 +204,15 @@ let register_open_library export m = (* [open_library export explicit m] opens library [m] if not already opened _or_ if explicitly asked to be (re)opened *) -let eq_lib_name m1 m2 = DirPath.equal m1.library_name m2.library_name - let open_library export explicit_libs m = if (* Only libraries indirectly to open are not reopen *) (* Libraries explicitly mentionned by the user are always reopen *) - List.exists (eq_lib_name m) explicit_libs - || not (library_is_opened m.library_name) + List.exists (fun m' -> DirPath.equal m m') explicit_libs + || not (library_is_opened m) then begin register_open_library export m; - Declaremods.really_import_module (MPfile m.library_name) + Declaremods.really_import_module (MPfile m) end else if export then @@ -164,45 +227,42 @@ let open_libraries export modl = (fun l m -> let subimport = Array.fold_left - (fun l m -> remember_last_of_each l (try_find_library m)) - l m.library_imports - in remember_last_of_each subimport m) + (fun l m -> remember_last_of_each l m) + l m.libsum_imports + in remember_last_of_each subimport m.libsum_name) [] modl in - List.iter (open_library export modl) to_open_list + let explicit = List.map (fun m -> m.libsum_name) modl in + List.iter (open_library export explicit) to_open_list (**********************************************************************) -(* import and export - synchronous operations*) +(* import and export of libraries - synchronous operations *) +(* at the end similar to import and export of modules except that it *) +(* is optimized: when importing several libraries at the same time *) +(* which themselves indirectly imports the very same modules, these *) +(* ones are imported only ones *) -let open_import i (_,(dir,export)) = +let open_import_library i (_,(modl,export)) = if Int.equal i 1 then (* even if the library is already imported, we re-import it *) (* if not (library_is_opened dir) then *) - open_libraries export [try_find_library dir] + open_libraries export (List.map try_find_library modl) -let cache_import obj = - open_import 1 obj +let cache_import_library obj = + open_import_library 1 obj -let subst_import (_,o) = o +let subst_import_library (_,o) = o -let classify_import (_,export as obj) = +let classify_import_library (_,export as obj) = if export then Substitute obj else Dispose -let in_import : DirPath.t * bool -> obj = +let in_import_library : DirPath.t list * bool -> obj = declare_object {(default_object "IMPORT LIBRARY") with - cache_function = cache_import; - open_function = open_import; - subst_function = subst_import; - classify_function = classify_import } - - -(************************************************************************) -(*s Low-level interning/externing of libraries to files *) - -(*s Loading from disk to cache (preparation phase) *) + cache_function = cache_import_library; + open_function = open_import_library; + subst_function = subst_import_library; + classify_function = classify_import_library } -let (raw_extern_library, raw_intern_library) = - System.raw_extern_intern Coq_config.vo_magic_number (************************************************************************) (*s Locate absolute or partially qualified library names in the path *) @@ -211,11 +271,18 @@ exception LibUnmappedDir exception LibNotFound type library_location = LibLoaded | LibInPath +let warn_several_object_files = + CWarnings.create ~name:"several-object-files" ~category:"require" + (fun (vi, vo) -> str"Loading" ++ spc () ++ str vi ++ + strbrk " instead of " ++ str vo ++ + strbrk " because it is more recent") + let locate_absolute_library dir = (* Search in loadpath *) let pref, base = split_dirpath dir in - let loadpath = Loadpath.expand_root_path pref in + let loadpath = Loadpath.filter_path (fun dir -> DirPath.equal dir pref) in let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in + let loadpath = List.map fst loadpath in let find ext = try let name = Id.to_string base ^ ext in @@ -224,18 +291,17 @@ let locate_absolute_library dir = with Not_found -> [] in match find ".vo" @ find ".vio" with | [] -> raise LibNotFound - | [file] -> dir, file + | [file] -> file | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ - str vo ++ str " because it is more recent"); - dir, vi - | [vo;vi] -> dir, vo + warn_several_object_files (vi, vo); + vi + | [vo;vi] -> vo | _ -> assert false -let locate_qualified_library warn qid = +let locate_qualified_library ?root ?(warn = true) qid = (* Search library in loadpath *) let dir, base = repr_qualid qid in - let loadpath = Loadpath.expand_path dir in + let loadpath = Loadpath.expand_path ?root dir in let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in let find ext = try @@ -250,8 +316,7 @@ let locate_qualified_library warn qid = | [lpath, file] -> lpath, file | [lpath_vo, vo; lpath_vi, vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ - str vo ++ str " because it is more recent"); + warn_several_object_files (vi, vo); lpath_vi, vi | [lpath_vo, vo; _ ] -> lpath_vo, vo | _ -> assert false @@ -264,12 +329,12 @@ let locate_qualified_library warn qid = let error_unmapped_dir qid = let prefix, _ = repr_qualid qid in - errorlabstrm "load_absolute_library_from" + user_err ~hdr:"load_absolute_library_from" (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ()) let error_lib_not_found qid = - errorlabstrm "load_absolute_library_from" + user_err ~hdr:"load_absolute_library_from" (str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath") let try_locate_absolute_library dir = @@ -279,14 +344,6 @@ let try_locate_absolute_library dir = | LibUnmappedDir -> error_unmapped_dir (qualid_of_dirpath dir) | LibNotFound -> error_lib_not_found (qualid_of_dirpath dir) -let try_locate_qualified_library (loc,qid) = - try - let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in - dir,f - with - | LibUnmappedDir -> error_unmapped_dir qid - | LibNotFound -> error_lib_not_found qid - (************************************************************************) (** {6 Tables of opaque proof terms} *) @@ -296,34 +353,10 @@ let try_locate_qualified_library (loc,qid) = terms, and access them only when a specific command (e.g. Print or Print Assumptions) needs it. *) -exception Faulty - -(** Fetching a table of opaque terms at position [pos] in file [f], - expecting to find first a copy of [digest]. *) - -let fetch_table what dp (f,pos,digest) = - let dir_path = Names.DirPath.to_string dp in - try - msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); - let ch = System.with_magic_number_check raw_intern_library f in - let () = seek_in ch pos in - if not (String.equal (System.digest_in f ch) digest) then raise Faulty; - let table, pos', digest' = System.marshal_in_segment f ch in - let () = close_in ch in - let ch' = open_in f in - if not (String.equal (Digest.channel ch' pos') digest') then raise Faulty; - let () = close_in ch' in - table - with e when Errors.noncritical e -> - error - ("The file "^f^" (bound to " ^ dir_path ^ - ") is inaccessible or corrupted,\n" ^ - "cannot load some "^what^" in it.\n") - (** Delayed / available tables of opaque terms *) type 'a table_status = - | ToFetch of string * int * Digest.t + | ToFetch of 'a Future.computation array delayed | Fetched of 'a Future.computation array let opaque_tables = @@ -336,25 +369,33 @@ let add_opaque_table dp st = let add_univ_table dp st = univ_tables := LibraryMap.add dp st !univ_tables -let access_table fetch_table add_table tables dp i = - let t = match LibraryMap.find dp tables with +let access_table what tables dp i = + let t = match LibraryMap.find dp !tables with | Fetched t -> t - | ToFetch (f,pos,digest) -> - let t = fetch_table dp (f,pos,digest) in - add_table dp (Fetched t); + | ToFetch f -> + let dir_path = Names.DirPath.to_string dp in + Flags.if_verbose Feedback.msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); + let t = + try fetch_delayed f + with Faulty f -> + user_err ~hdr:"Library.access_table" + (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++ + str ") is inaccessible or corrupted,\ncannot load some " ++ + str what ++ str " in it.\n") + in + tables := LibraryMap.add dp (Fetched t) !tables; t in assert (i < Array.length t); t.(i) let access_opaque_table dp i = - access_table - (fetch_table "opaque proofs") - add_opaque_table !opaque_tables dp i + let what = "opaque proofs" in + access_table what opaque_tables dp i + let access_univ_table dp i = try - Some (access_table - (fetch_table "universe contexts of opaque proofs") - add_univ_table !univ_tables dp i) + let what = "universe contexts of opaque proofs" in + Some (access_table what univ_tables dp i) with Not_found -> None let () = @@ -364,118 +405,92 @@ let () = (************************************************************************) (* Internalise libraries *) +type seg_sum = summary_disk type seg_lib = library_disk type seg_univ = (* true = vivo, false = vi *) Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool type seg_discharge = Opaqueproof.cooking_info list array type seg_proofs = Term.constr Future.computation array -let mk_library md digests univs = +let mk_library sd md digests univs = { - library_name = md.md_name; - library_compiled = md.md_compiled; - library_objects = md.md_objects; - library_deps = md.md_deps; - library_imports = md.md_imports; + library_name = sd.md_name; + library_data = md; + library_deps = sd.md_deps; + library_imports = sd.md_imports; library_digests = digests; library_extra_univs = univs; } +let mk_summary m = { + libsum_name = m.library_name; + libsum_imports = m.library_imports; + libsum_digests = m.library_digests; +} + let intern_from_file f = - let ch = System.with_magic_number_check raw_intern_library f in - let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment f ch in + let ch = raw_intern_library f in + let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in + let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in let _ = System.skip_in_segment f ch in - let pos, digest = System.skip_in_segment f ch in + let _ = System.skip_in_segment f ch in + let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in close_in ch; - register_library_filename lmd.md_name f; - add_opaque_table lmd.md_name (ToFetch (f,pos,digest)); + register_library_filename lsd.md_name f; + add_opaque_table lsd.md_name (ToFetch del_opaque); let open Safe_typing in match univs with - | None -> mk_library lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty + | None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty | Some (utab,uall,true) -> - add_univ_table lmd.md_name (Fetched utab); - mk_library lmd (Dvivo (digest_lmd,digest_u)) uall + add_univ_table lsd.md_name (Fetched utab); + mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall | Some (utab,_,false) -> - add_univ_table lmd.md_name (Fetched utab); - mk_library lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty + add_univ_table lsd.md_name (Fetched utab); + mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty module DPMap = Map.Make(DirPath) -let deps_to_string deps = - Array.fold_left (fun s (n, _) -> s^"\n - "^(DirPath.to_string n)) "" deps - let rec intern_library (needed, contents) (dir, f) from = - Pp.feedback(Feedback.FileDependency (from, f)); (* Look if in the current logical environment *) - try find_library dir, (needed, contents) + try (find_library dir).libsum_digests, (needed, contents) with Not_found -> (* Look if already listed and consequently its dependencies too *) - try DPMap.find dir contents, (needed, contents) + try (DPMap.find dir contents).library_digests, (needed, contents) with Not_found -> + Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); (* [dir] is an absolute name which matches [f] which must be in loadpath *) + let f = match f with Some f -> f | None -> try_locate_absolute_library dir in let m = intern_from_file f in if not (DirPath.equal dir m.library_name) then - errorlabstrm "load_physical_library" - (str ("The file " ^ f ^ " contains library") ++ spc () ++ + user_err ~hdr:"load_physical_library" + (str "The file " ++ str f ++ str " contains library" ++ spc () ++ pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); - Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f)); - m, intern_library_deps (needed, contents) dir m (Some f) + Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f)); + m.library_digests, intern_library_deps (needed, contents) dir m f and intern_library_deps libs dir m from = let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in (dir :: needed, DPMap.add dir m contents ) and intern_mandatory_library caller from libs (dir,d) = - let m, libs = intern_library libs (try_locate_absolute_library dir) from in - if not (Safe_typing.digest_match ~actual:m.library_digests ~required:d) then - errorlabstrm "" (strbrk ("Compiled library "^ DirPath.to_string caller ^ - ".vo makes inconsistent assumptions over library " ^ - DirPath.to_string dir)); + let digest, libs = intern_library libs (dir, None) (Some from) in + if not (Safe_typing.digest_match ~actual:digest ~required:d) then + user_err (str "Compiled library " ++ pr_dirpath caller ++ + str " (in file " ++ str from ++ str ") makes inconsistent assumptions \ + over library " ++ pr_dirpath dir); libs -let rec_intern_library libs mref = - let _, libs = intern_library libs mref None in +let rec_intern_library libs (dir, f) = + let _, libs = intern_library libs (dir, Some f) None in libs -let check_library_short_name f dir = function - | Some id when not (Id.equal id (snd (split_dirpath dir))) -> - errorlabstrm "check_library_short_name" - (str ("The file " ^ f ^ " contains library") ++ spc () ++ - pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++ - pr_id id) - | _ -> () - -let rec_intern_by_filename_only id f = - let m = try intern_from_file f with Sys_error s -> error s in - (* Only the base name is expected to match *) - check_library_short_name f m.library_name id; - (* We check no other file containing same library is loaded *) - if library_is_loaded m.library_name then - begin - msg_warning - (pr_dirpath m.library_name ++ str " is already loaded from file " ++ - str (library_full_filename m.library_name)); - m.library_name, [] - end - else - let needed, contents = intern_library_deps ([], DPMap.empty) m.library_name m (Some f) in - let needed = List.map (fun dir -> dir, DPMap.find dir contents) needed in - m.library_name, needed - let native_name_from_filename f = - let ch = System.with_magic_number_check raw_intern_library f in - let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment f ch in + let ch = raw_intern_library f in + let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in Nativecode.mod_uid_of_dirpath lmd.md_name -let rec_intern_library_from_file idopt f = - (* A name is specified, we have to check it contains library id *) - let paths = Loadpath.get_paths () in - let _, f = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in - rec_intern_by_filename_only idopt f - (**********************************************************************) (*s [require_library] loads and possibly opens a library. This is a synchronized operation. It is performed as follows: @@ -494,13 +509,14 @@ let rec_intern_library_from_file idopt f = *) let register_library m = + let l = fetch_delayed m.library_data in Declaremods.register_library m.library_name - m.library_compiled - m.library_objects + l.md_compiled + l.md_objects m.library_digests m.library_extra_univs; - register_loaded_library m + register_loaded_library (mk_summary m) (* Follow the semantics of Anticipate object: - called at module or module type closing when a Require occurs in @@ -535,54 +551,66 @@ let in_require : require_obj -> obj = (* Require libraries, import them if [export <> None], mark them for export if [export = Some true] *) +let (f_xml_require, xml_require) = Hook.make ~default:ignore () + +let warn_require_in_module = + CWarnings.create ~name:"require-in-module" ~category:"deprecated" + (fun () -> strbrk "Require inside a module is" ++ + strbrk " deprecated and strongly discouraged. " ++ + strbrk "You can Require a module at toplevel " ++ + strbrk "and optionally Import it inside another one.") + let require_library_from_dirpath modrefl export = let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in let modrefl = List.map fst modrefl in if Lib.is_module_or_modtype () then begin + warn_require_in_module (); add_anonymous_leaf (in_require (needed,modrefl,None)); Option.iter (fun exp -> - List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl) + add_anonymous_leaf (in_import_library (modrefl,exp))) export end else add_anonymous_leaf (in_require (needed,modrefl,export)); - add_frozen_state () - -let require_library qidl export = - let modrefl = List.map try_locate_qualified_library qidl in - require_library_from_dirpath modrefl export - -let require_library_from_file idopt file export = - let modref,needed = rec_intern_library_from_file idopt file in - let needed = List.rev_map snd needed in - if Lib.is_module_or_modtype () then begin - add_anonymous_leaf (in_require (needed,[modref],None)); - Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp))) - export - end - else - add_anonymous_leaf (in_require (needed,[modref],export)); + if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl; add_frozen_state () (* the function called by Vernacentries.vernac_import *) -let import_module export (loc,qid) = - try - match Nametab.locate_module qid with - | MPfile dir -> - if Lib.is_module_or_modtype () || not export then - add_anonymous_leaf (in_import (dir, export)) - else - add_anonymous_leaf (in_import (dir, export)) - | mp -> - Declaremods.import_module export mp - with - Not_found -> - user_err_loc - (loc,"import_library", - str ((string_of_qualid qid)^" is not a module")) +let safe_locate_module (loc,qid) = + try Nametab.locate_module qid + with Not_found -> + user_err ~loc ~hdr:"import_library" + (pr_qualid qid ++ str " is not a module") + +let import_module export modl = + (* Optimization: libraries in a raw in the list are imported + "globally". If there is non-library in the list; it breaks the + optimization For instance: "Import Arith MyModule Zarith" will + not be optimized (possibly resulting in redefinitions, but + "Import MyModule Arith Zarith" and "Import Arith Zarith MyModule" + will have the submodules imported by both Arith and ZArith + imported only once *) + let flush = function + | [] -> () + | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in + let rec aux acc = function + | (loc,dir as m) :: l -> + let m,acc = + try Nametab.locate_module dir, acc + with Not_found-> flush acc; safe_locate_module m, [] in + (match m with + | MPfile dir -> aux (dir::acc) l + | mp -> + flush acc; + try Declaremods.import_module export mp; aux [] l + with Not_found -> + user_err ~loc ~hdr:"import_library" + (pr_qualid dir ++ str " is not a module")) + | [] -> flush acc + in aux [] modl (************************************************************************) (*s Initializing the compilation of a library. *) @@ -590,10 +618,10 @@ let import_module export (loc,qid) = let check_coq_overwriting p id = let l = DirPath.repr p in let is_empty = match l with [] -> true | _ -> false in - if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then - errorlabstrm "" - (strbrk ("Cannot build module "^DirPath.to_string p^"."^Id.to_string id^ - ": it starts with prefix \"Coq\" which is reserved for the Coq library.")) + if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then + user_err + (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++ + str "it starts with prefix \"Coq\" which is reserved for the Coq library.") (* Verifies that a string starts by a letter and do not contain others caracters than letters, digits, or `_` *) @@ -604,7 +632,7 @@ let check_module_name s = (if c = '\'' then str "\"'\"" else (str "'" ++ str (String.make 1 c) ++ str "'")) ++ strbrk " is not allowed in module names\n" in - let err c = errorlabstrm "" (msg c) in + let err c = user_err (msg c) in match String.get s 0 with | 'a' .. 'z' | 'A' .. 'Z' -> for i = 1 to (String.length s)-1 do @@ -614,53 +642,52 @@ let check_module_name s = done | c -> err c -let start_library f = - let paths = Loadpath.get_paths () in - let _, longf = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in +let start_library fo = let ldir0 = try - let lp = Loadpath.find_load_path (Filename.dirname longf) in + let lp = Loadpath.find_load_path (Filename.dirname fo) in Loadpath.logical lp with Not_found -> Nameops.default_root_prefix in - let file = Filename.basename f in + let file = Filename.chop_extension (Filename.basename fo) in let id = Id.of_string file in check_module_name file; check_coq_overwriting ldir0 id; let ldir = add_dirpath_suffix ldir0 id in Declaremods.start_library ldir; - ldir,longf + ldir let load_library_todo f = - let paths = Loadpath.get_paths () in - let _, longf = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in + let longf = Loadpath.locate_file (f^".v") in let f = longf^"io" in - let ch = System.with_magic_number_check raw_intern_library f in + let ch = raw_intern_library f in + let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in let (s3 : seg_discharge option), _, _ = System.marshal_in_segment f ch in let tasks, _, _ = System.marshal_in_segment f ch in let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in close_in ch; - if tasks = None then errorlabstrm "restart" (str"not a .vio file"); - if s2 = None then errorlabstrm "restart" (str"not a .vio file"); - if s3 = None then errorlabstrm "restart" (str"not a .vio file"); - if pi3 (Option.get s2) then errorlabstrm "restart" (str"not a .vio file"); - longf, s1, Option.get s2, Option.get s3, Option.get tasks, s5 + if tasks = None then user_err ~hdr:"restart" (str"not a .vio file"); + if s2 = None then user_err ~hdr:"restart" (str"not a .vio file"); + if s3 = None then user_err ~hdr:"restart" (str"not a .vio file"); + if pi3 (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file"); + longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5 (************************************************************************) (*s [save_library dir] ends library [dir] and save it to the disk. *) let current_deps () = - List.map (fun m -> m.library_name, m.library_digests) !libraries_loaded_list + let map name = + let m = try_find_library name in + (name, m.libsum_digests) + in + List.map map !libraries_loaded_list -let current_reexports () = - List.map (fun m -> m.library_name) !libraries_exports_list +let current_reexports () = !libraries_exports_list let error_recursively_dependent_library dir = - errorlabstrm "" + user_err (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.") @@ -677,13 +704,14 @@ let error_recursively_dependent_library dir = writing the content and computing the checksum... *) let save_library_to ?todo dir f otab = - let f, except = match todo with + let except = match todo with | None -> assert(!Flags.compilation_mode = Flags.BuildVo); - f ^ "o", Future.UUIDSet.empty + assert(Filename.check_suffix f ".vo"); + Future.UUIDSet.empty | Some (l,_) -> - f ^ "io", - List.fold_left (fun e r -> Future.UUIDSet.add r.Stateid.uuid e) + assert(Filename.check_suffix f ".vio"); + List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty l in let cenv, seg, ast = Declaremods.end_library ~except dir in let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in @@ -692,32 +720,40 @@ let save_library_to ?todo dir f otab = | None -> None, None, None | Some (tasks, rcbackup) -> let tasks = - List.map Stateid.(fun r -> - { r with uuid = Future.UUIDMap.find r.uuid f2t_map }) tasks in + List.map Stateid.(fun (r,b) -> + try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b + with Not_found -> assert b; { r with uuid = -1 }, b) + tasks in Some (tasks,rcbackup), Some (univ_table,Univ.ContextSet.empty,false), Some disch_table in let except = Future.UUIDSet.fold (fun uuid acc -> - Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc) + try Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc + with Not_found -> acc) except Int.Set.empty in let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in Array.iteri (fun i x -> - if not(is_done_or_todo i x) then Errors.errorlabstrm "library" + if not(is_done_or_todo i x) then CErrors.user_err ~hdr:"library" Pp.(str"Proof object "++int i++str" is not checked nor to be checked")) opaque_table; - let md = { + let sd = { md_name = dir; + md_deps = Array.of_list (current_deps ()); + md_imports = Array.of_list (current_reexports ()); + } in + let md = { md_compiled = cenv; md_objects = seg; - md_deps = Array.of_list (current_deps ()); - md_imports = Array.of_list (current_reexports ()) } in - if Array.exists (fun (d,_) -> DirPath.equal d dir) md.md_deps then + } in + if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then error_recursively_dependent_library dir; (* Open the vo file and write the magic number *) - let (f',ch) = raw_extern_library f in + let f' = f in + let ch = raw_extern_library f' in try (* Writing vo payload *) + System.marshal_out_segment f' ch (sd : seg_sum); System.marshal_out_segment f' ch (md : seg_lib); System.marshal_out_segment f' ch (utab : seg_univ option); System.marshal_out_segment f' ch (dtab : seg_discharge option); @@ -725,19 +761,21 @@ let save_library_to ?todo dir f otab = System.marshal_out_segment f' ch (opaque_table : seg_proofs); close_out ch; (* Writing native code files *) - if not !Flags.no_native_compiler then + if !Flags.native_compiler then let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in if not (Nativelib.compile_library dir ast fn) then - msg_error (str"Could not compile the library to native code. Skipping.") + error "Could not compile the library to native code." with reraise -> - let reraise = Errors.push reraise in - let () = msg_warning (str ("Removed file "^f')) in + let reraise = CErrors.push reraise in + let () = Feedback.msg_warning (str "Removed file " ++ str f') in let () = close_out ch in let () = Sys.remove f' in iraise reraise -let save_library_raw f lib univs proofs = - let (f',ch) = raw_extern_library (f^"o") in +let save_library_raw f sum lib univs proofs = + let f' = f^"o" in + let ch = raw_extern_library f' in + System.marshal_out_segment f' ch (sum : seg_sum); System.marshal_out_segment f' ch (lib : seg_lib); System.marshal_out_segment f' ch (Some univs : seg_univ option); System.marshal_out_segment f' ch (None : seg_discharge option); @@ -745,24 +783,13 @@ let save_library_raw f lib univs proofs = System.marshal_out_segment f' ch (proofs : seg_proofs); close_out ch -(************************************************************************) -(*s Display the memory use of a library. *) - -open Printf - -let mem s = - let m = try_find_library s in - h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)" - (CObj.size_kb m) (CObj.size_kb m.library_compiled) - (CObj.size_kb m.library_objects))) - module StringOrd = struct type t = string let compare = String.compare end module StringSet = Set.Make(StringOrd) let get_used_load_paths () = StringSet.elements (List.fold_left (fun acc m -> StringSet.add - (Filename.dirname (library_full_filename m.library_name)) acc) + (Filename.dirname (library_full_filename m)) acc) StringSet.empty !libraries_loaded_list) let _ = Nativelib.get_load_paths := get_used_load_paths diff --git a/library/library.mli b/library/library.mli index 13d83a5c02..b9044b60dd 100644 --- a/library/library.mli +++ b/library/library.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -21,14 +21,12 @@ open Libnames (** {6 ... } *) (** Require = load in the environment + open (if the optional boolean is not [None]); mark also for export if the boolean is [Some true] *) -val require_library : qualid located list -> bool option -> unit val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit -val require_library_from_file : - Id.t option -> CUnix.physical_path -> bool option -> unit -(** {6 ... } *) +(** {6 Start the compilation of a library } *) (** Segments of a library *) +type seg_sum type seg_lib type seg_univ = (* cst, all_cst, finished? *) Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool @@ -37,19 +35,21 @@ type seg_proofs = Term.constr Future.computation array (** Open a module (or a library); if the boolean is true then it's also an export otherwise just a simple import *) -val import_module : bool -> qualid located -> unit +val import_module : bool -> qualid located list -> unit -(** {6 Start the compilation of a library } *) -val start_library : string -> DirPath.t * string +(** Start the compilation of a file as a library. The first argument must be + output file, and the + returned path is the associated absolute logical path of the library. *) +val start_library : CUnix.physical_path -> DirPath.t -(** {6 End the compilation of a library and save it to a ".vo" file } *) +(** End the compilation of a library and save it to a ".vo" file *) val save_library_to : - ?todo:((Future.UUID.t,'document) Stateid.request list * 'counters) -> + ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit val load_library_todo : - string -> string * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs -val save_library_raw : string -> seg_lib -> seg_univ -> seg_proofs -> unit + string -> string * seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs +val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit (** {6 Interrogate the status of libraries } *) @@ -67,17 +67,23 @@ val library_full_filename : DirPath.t -> string (** - Overwrite the filename of all libraries (used when restoring a state) *) val overwrite_library_filenames : string -> unit +(** {6 Hook for the xml exportation of libraries } *) +val xml_require : (DirPath.t -> unit) Hook.t + (** {6 Locate a library in the load paths } *) exception LibUnmappedDir exception LibNotFound type library_location = LibLoaded | LibInPath val locate_qualified_library : - bool -> qualid -> library_location * DirPath.t * CUnix.physical_path -val try_locate_qualified_library : qualid located -> DirPath.t * string + ?root:DirPath.t -> ?warn:bool -> qualid -> + library_location * DirPath.t * CUnix.physical_path +(** Locates a library by implicit name. + + @raise LibUnmappedDir if the library is not in the path + @raise LibNotFound if there is no corresponding file in the path -(** {6 Statistics: display the memory use of a library. } *) -val mem : DirPath.t -> Pp.std_ppcmds +*) (** {6 Native compiler. } *) val native_name_from_filename : string -> string diff --git a/library/library.mllib b/library/library.mllib index eca28c8222..df4f735034 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -5,7 +5,6 @@ Libobject Summary Nametab Global -Universes Lib Declaremods Loadpath @@ -16,5 +15,4 @@ Dischargedhypsmap Goptions Decls Heads -Assumptions Keys diff --git a/library/loadpath.ml b/library/loadpath.ml index 5876eedd2a..d03c6c5553 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,18 +8,16 @@ open Pp open Util -open Errors +open CErrors open Names open Libnames -type path_type = ImplicitPath | ImplicitRootPath | RootPath - (** Load paths. Mapping from physical to logical paths. *) type t = { path_physical : CUnix.physical_path; path_logical : DirPath.t; - path_type : path_type; + path_implicit : bool; } let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS" @@ -30,8 +28,6 @@ let physical p = p.path_physical let get_load_paths () = !load_paths -let get_paths () = List.map physical !load_paths - let anomaly_too_many_paths path = anomaly (str "Several logical paths are associated to" ++ spc () ++ str path) @@ -54,82 +50,68 @@ let remove_load_path dir = let filter p = not (String.equal p.path_physical dir) in load_paths := List.filter filter !load_paths -let add_load_path phys_path path_type coq_path = +let warn_overriding_logical_loadpath = + CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath" + (fun (phys_path, old_path, coq_path) -> + str phys_path ++ strbrk " was previously bound to " ++ + pr_dirpath old_path ++ strbrk "; it is remapped to " ++ + pr_dirpath coq_path) + +let add_load_path phys_path coq_path ~implicit = let phys_path = CUnix.canonical_path_name phys_path in let filter p = String.equal p.path_physical phys_path in let binding = { path_logical = coq_path; path_physical = phys_path; - path_type = path_type; + path_implicit = implicit; } in match List.filter filter !load_paths with | [] -> load_paths := binding :: !load_paths - | [p] -> - let dir = p.path_logical in - if not (DirPath.equal coq_path dir) - (* If this is not the default -I . to coqtop *) - && not - (String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) - && DirPath.equal coq_path (Nameops.default_root_prefix)) - then + | [{ path_logical = old_path; path_implicit = old_implicit }] -> + let replace = + if DirPath.equal coq_path old_path then + implicit <> old_implicit + else + let () = + (* Do not warn when overriding the default "-I ." path *) + if not (DirPath.equal old_path Nameops.default_root_prefix) then + warn_overriding_logical_loadpath (phys_path, old_path, coq_path) + in + true in + if replace then begin - (* Assume the user is concerned by library naming *) - if not (DirPath.equal dir Nameops.default_root_prefix) then - msg_warning - (str phys_path ++ strbrk " was previously bound to " ++ - pr_dirpath dir ++ strbrk "; it is remapped to " ++ - pr_dirpath coq_path); remove_load_path phys_path; load_paths := binding :: !load_paths; end | _ -> anomaly_too_many_paths phys_path -let extend_path_with_dirpath p dir = - List.fold_left Filename.concat p - (List.rev_map Id.to_string (DirPath.repr dir)) - -let expand_root_path dir = +let filter_path f = let rec aux = function | [] -> [] | p :: l -> - if p.path_type <> ImplicitPath && is_dirpath_prefix_of p.path_logical dir then - let suffix = drop_dirpath_prefix p.path_logical dir in - extend_path_with_dirpath p.path_physical suffix :: aux l + if f p.path_logical then (p.path_physical, p.path_logical) :: aux l else 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 DirPath.is_empty d1 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 expand p dir = - let ph = extend_path_with_dirpath p.path_physical dir in - let log = append_dirpath p.path_logical dir in - (ph, log) - -let expand_path dir = +let expand_path ?root dir = let rec aux = function | [] -> [] - | p :: l -> - match p.path_type with - | ImplicitPath -> expand p dir :: aux l - | ImplicitRootPath -> - let inters = intersections p.path_logical dir in - List.map (expand p) inters @ aux l - | RootPath -> - if is_dirpath_prefix_of p.path_logical dir then - expand p (drop_dirpath_prefix p.path_logical dir) :: aux l - else aux l in + | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l -> + let success = + match root with + | None -> + if implicit then is_dirpath_suffix_of dir lg + else DirPath.equal dir lg + | Some root -> + is_dirpath_prefix_of root lg && + is_dirpath_suffix_of dir (drop_dirpath_prefix root lg) in + if success then (ph, lg) :: aux l else aux l in aux !load_paths + +let locate_file fname = + let paths = List.map physical !load_paths in + let _,longfname = + System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in + longfname diff --git a/library/loadpath.mli b/library/loadpath.mli index 62dc5d5912..4e79edbdcf 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -15,11 +15,6 @@ open Names *) -type path_type = - | ImplicitPath (** Can be implicitly appended to a logical path. *) - | ImplicitRootPath (** Can be implicitly appended to the suffix of a logical path. *) - | RootPath (** Can only be a prefix of a logical path. *) - type t (** Type of loadpath bindings. *) @@ -32,11 +27,8 @@ val logical : t -> DirPath.t val get_load_paths : unit -> t list (** Get the current loadpath association. *) -val get_paths : unit -> CUnix.physical_path list -(** Same as [get_load_paths] but only get the physical part. *) - -val add_load_path : CUnix.physical_path -> path_type -> DirPath.t -> unit -(** [add_load_path phys type log] adds the binding [phys := log] to the current +val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit +(** [add_load_path phys log type] adds the binding [phys := log] to the current loadpaths. *) val remove_load_path : CUnix.physical_path -> unit @@ -50,9 +42,14 @@ val find_load_path : CUnix.physical_path -> t val is_in_load_paths : CUnix.physical_path -> bool (** Whether a physical path is currently bound. *) -val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list +val expand_path : ?root:DirPath.t -> DirPath.t -> (CUnix.physical_path * DirPath.t) list (** Given a relative logical path, associate the list of absolute physical and - logical paths which are possible expansions of it. *) + logical paths which are possible matches of it. *) + +val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list +(** As {!expand_path} but uses a filter function instead, and ignores the + implicit status of loadpaths. *) -val expand_root_path : DirPath.t -> CUnix.physical_path list -(** As [expand_path] but restricts to root loadpaths. *) +val locate_file : string -> string +(** Locate a file among the registered paths. Do not use this function, as + it does not respect the visibility of paths. *) diff --git a/library/nameops.ml b/library/nameops.ml index 02b085a7ac..6020db33d9 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,7 +12,7 @@ open Names (* Identifiers *) -let pr_id id = str (Id.to_string id) +let pr_id id = Id.print id let pr_name = function | Anonymous -> str "_" @@ -67,9 +67,21 @@ let root_of_id id = let suffixstart = cut_ident true id in Id.of_string (String.sub (Id.to_string id) 0 suffixstart) -(* Rem: semantics is a bit different, if an ident starts with toto00 then - after successive renamings it comes to toto09, then it goes on with toto10 *) -let lift_subscript id = +(* Return the same identifier as the original one but whose {i subscript} is incremented. + If the original identifier does not have a suffix, [0] is appended to it. + + Example mappings: + + [bar] ↦ [bar0] + [bar0] ↦ [bar1] + [bar00] ↦ [bar01] + [bar1] ↦ [bar2] + [bar01] ↦ [bar01] + [bar9] ↦ [bar10] + [bar09] ↦ [bar10] + [bar99] ↦ [bar100] +*) +let increment_subscript id = let id = Id.to_string id in let len = String.length id in let rec add carrypos = @@ -136,7 +148,12 @@ let name_fold_map f e = function | Name id -> let (e,id) = f e id in (e,Name id) | Anonymous -> e,Anonymous -let pr_lab l = str (Label.to_string l) +let name_max na1 na2 = + match na1 with + | Name _ -> na1 + | Anonymous -> na2 + +let pr_lab l = Label.print l let default_library = Names.DirPath.initial (* = ["Top"] *) diff --git a/library/nameops.mli b/library/nameops.mli index 23432ae2fa..3a67b61a13 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -21,9 +21,34 @@ val root_of_id : Id.t -> Id.t (** remove trailing digits, ' and _ *) val add_suffix : Id.t -> string -> Id.t val add_prefix : string -> Id.t -> Id.t -val has_subscript : Id.t -> bool -val lift_subscript : Id.t -> Id.t -val forget_subscript : Id.t -> Id.t +(** Below, by {i subscript} we mean a suffix composed solely from (decimal) digits. *) + +val has_subscript : Id.t -> bool + +val increment_subscript : Id.t -> Id.t +(** Return the same identifier as the original one but whose {i subscript} is incremented. + If the original identifier does not have a suffix, [0] is appended to it. + + Example mappings: + + [bar] ↦ [bar0] + + [bar0] ↦ [bar1] + + [bar00] ↦ [bar01] + + [bar1] ↦ [bar2] + + [bar01] ↦ [bar01] + + [bar9] ↦ [bar10] + + [bar09] ↦ [bar10] + + [bar99] ↦ [bar100] +*) + +val forget_subscript : Id.t -> Id.t val out_name : Name.t -> Id.t (** [out_name] associates [id] to [Name id]. Raises [Failure "Nameops.out_name"] @@ -34,7 +59,7 @@ val name_iter : (Id.t -> unit) -> Name.t -> unit val name_cons : Name.t -> Id.t list -> Id.t list val name_app : (Id.t -> Id.t) -> Name.t -> Name.t val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t - +val name_max : Name.t -> Name.t -> Name.t val pr_lab : Label.t -> Pp.std_ppcmds diff --git a/library/nametab.ml b/library/nametab.ml index 6af1e686b0..b76048e890 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Pp open Names @@ -16,10 +16,8 @@ open Globnames exception GlobalizationError of qualid -let error_global_not_found_loc loc q = - Loc.raise loc (GlobalizationError q) - -let error_global_not_found q = raise (GlobalizationError q) +let error_global_not_found ?loc q = + Loc.raise ?loc (GlobalizationError q) (* Kinds of global names *) @@ -82,6 +80,14 @@ module Make (U : UserName) (E : EqualityType) : NAMETREE struct type elt = E.t + (* A name became inaccessible, even with absolute qualification. + Example: + Module F (X : S). Module X. + The argument X of the functor F is masked by the inner module X. + *) + let masking_absolute n = + Flags.if_verbose Feedback.msg_info (str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!")) + type user_name = U.t type path_status = @@ -119,9 +125,7 @@ struct | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - msg_warning (str ("Trying to mask the absolute name \"" - ^ U.to_string n ^ "\"!")); - tree.path + masking_absolute n; tree.path | Nothing | Relative _ -> Relative (uname,o) else tree.path @@ -144,7 +148,6 @@ struct | Nothing | Relative _ -> mktree (Absolute (uname,o)) tree.map - let rec push_exactly uname o level tree = function | [] -> anomaly (Pp.str "Prefix longer than path! Impossible!") @@ -155,9 +158,7 @@ let rec push_exactly uname o level tree = function | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - msg_warning (str ("Trying to mask the absolute name \"" - ^ U.to_string n ^ "\"!")); - tree.path + masking_absolute n; tree.path | Nothing | Relative _ -> Relative (uname,o) in @@ -452,11 +453,11 @@ let global r = try match locate_extended qid with | TrueGlobal ref -> ref | SynDef _ -> - user_err_loc (loc,"global", - str "Unexpected reference to a notation: " ++ - pr_qualid qid) + user_err ~loc ~hdr:"global" + (str "Unexpected reference to a notation: " ++ + pr_qualid qid) with Not_found -> - error_global_not_found_loc loc qid + error_global_not_found ~loc qid (* Exists functions ********************************************************) @@ -523,15 +524,16 @@ let shortest_qualid_of_tactic kn = KnTab.shortest_qualid Id.Set.empty sp !the_tactictab let pr_global_env env ref = - try str (string_of_qualid (shortest_qualid_of_global env ref)) - with Not_found as e -> prerr_endline "pr_global_env not found"; raise e + try pr_qualid (shortest_qualid_of_global env ref) + with Not_found as e -> + if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e let global_inductive r = match global r with | IndRef ind -> ind | ref -> - user_err_loc (loc_of_reference r,"global_inductive", - pr_reference r ++ spc () ++ str "is not an inductive type") + user_err ~loc:(loc_of_reference r) ~hdr:"global_inductive" + (pr_reference r ++ spc () ++ str "is not an inductive type") (********************************************************************) diff --git a/library/nametab.mli b/library/nametab.mli index e3aeb67579..d20c399b60 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -60,8 +60,7 @@ open Globnames exception GlobalizationError of qualid (** Raises a globalization error *) -val error_global_not_found_loc : Loc.t -> qualid -> 'a -val error_global_not_found : qualid -> 'a +val error_global_not_found : ?loc:Loc.t -> qualid -> 'a (** {6 Register visibility of things } *) diff --git a/library/states.ml b/library/states.ml index a1c2a095d0..95bd819d66 100644 --- a/library/states.ml +++ b/library/states.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,6 +12,7 @@ open System type state = Lib.frozen * Summary.frozen let summary_of_state = snd +let replace_summary (lib,_) s = lib, s let freeze ~marshallable = (Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable) @@ -20,18 +21,12 @@ let unfreeze (fl,fs) = Lib.unfreeze fl; Summary.unfreeze_summaries fs -let (extern_state,intern_state) = - let ensure_suffix f = CUnix.make_suffix f ".coq" in - let (raw_extern, raw_intern) = - extern_intern Coq_config.state_magic_number in - (fun s -> - let s = ensure_suffix s in - raw_extern s (freeze ~marshallable:`Yes)), - (fun s -> - let s = ensure_suffix s in - let paths = Loadpath.get_paths () in - unfreeze (with_magic_number_check (raw_intern paths) s); - Library.overwrite_library_filenames s) +let extern_state s = + System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:`Yes) + +let intern_state s = + unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s); + Library.overwrite_library_filenames s (* Rollback. *) @@ -40,7 +35,7 @@ let with_state_protection f x = try let a = f x in unfreeze st; a with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in (unfreeze st; iraise reraise) let with_state_protection_on_exception = Future.transactify diff --git a/library/states.mli b/library/states.mli index 66de14909a..12c71c9991 100644 --- a/library/states.mli +++ b/library/states.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -21,6 +21,7 @@ val freeze : marshallable:Summary.marshallable -> state val unfreeze : state -> unit val summary_of_state : state -> Summary.frozen +val replace_summary : state -> Summary.frozen -> state (** {6 Rollback } *) diff --git a/library/summary.ml b/library/summary.ml index 7e7628a1b7..6efa07f388 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -1,15 +1,17 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Pp -open Errors +open CErrors open Util +module Dyn = Dyn.Make(struct end) + type marshallable = [ `Yes | `No | `Shallow ] type 'a summary_declaration = { freeze_function : marshallable -> 'a; @@ -21,7 +23,7 @@ let summaries = ref Int.Map.empty let mangle id = id ^ "-SUMMARY" let internal_declare_summary hash sumname sdecl = - let (infun, outfun) = Dyn.create (mangle sumname) in + let (infun, outfun) = Dyn.Easy.make_dyn (mangle sumname) in let dyn_freeze b = infun (sdecl.freeze_function b) and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum) and dyn_init = sdecl.init_function in @@ -66,6 +68,7 @@ let freeze_summaries ~marshallable : frozen = let fold id (_, decl) accu = (* to debug missing Lazy.force if marshallable <> `No then begin + let id, _ = Int.Map.find id !summaries in prerr_endline ("begin marshalling " ^ id); ignore(Marshal.to_string (decl.freeze_function marshallable) []); prerr_endline ("end marshalling " ^ id); @@ -102,10 +105,10 @@ let unfreeze_summaries fs = in let fold id decl state = try fold id decl state - with e when Errors.noncritical e -> - let e = Errors.push e in + with e when CErrors.noncritical e -> + let e = CErrors.push e in Printf.eprintf "Error unfrezing summay %s\n%s\n%!" - (name_of_summary id) (Pp.string_of_ppcmds (Errors.iprint e)); + (name_of_summary id) (Pp.string_of_ppcmds (CErrors.iprint e)); iraise e in (** We rely on the order of the frozen list, and the order of folding *) @@ -146,7 +149,7 @@ let unfreeze_summary datas = let (name, summary) = Int.Map.find id !summaries in try summary.unfreeze_function data with e -> - let e = Errors.push e in + let e = CErrors.push e in prerr_endline ("Exception unfreezing " ^ name); iraise e) datas @@ -163,8 +166,15 @@ let project_summary { summaries; ml_module } ?(complement=false) ids = List.filter (fun (id, _) -> List.mem id ids) summaries let pointer_equal l1 l2 = + let ptr_equal d1 d2 = + let Dyn.Dyn (t1, x1) = d1 in + let Dyn.Dyn (t2, x2) = d2 in + match Dyn.eq t1 t2 with + | None -> false + | Some Refl -> x1 == x2 + in CList.for_all2eq - (fun (id1,v1) (id2,v2) -> id1 = id2 && Dyn.pointer_equal v1 v2) l1 l2 + (fun (id1,v1) (id2,v2) -> id1 = id2 && ptr_equal v1 v2) l1 l2 (** All-in-one reference declaration + registration *) @@ -175,3 +185,30 @@ let ref ?(freeze=fun _ r -> r) ~name x = unfreeze_function = ((:=) r); init_function = (fun () -> r := x) }; r + +module Local = struct + +type 'a local_ref = ('a CEphemeron.key * string) ref + +let (:=) r v = r := (CEphemeron.create v, snd !r) + +let (!) r = + let key, name = !r in + try CEphemeron.get key + with CEphemeron.InvalidKey -> + let _, { init_function } = + Int.Map.find (String.hash (mangle name)) !summaries in + init_function (); + CEphemeron.get (fst !r) + +let ref ?(freeze=fun x -> x) ~name init = + let r = Pervasives.ref (CEphemeron.create init, name) in + declare_summary name + { freeze_function = (fun _ -> freeze !r); + unfreeze_function = ((:=) r); + init_function = (fun () -> r := init) }; + r + +end + +let dump = Dyn.dump diff --git a/library/summary.mli b/library/summary.mli index 48c9390d07..1b57613cb7 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -42,6 +42,17 @@ val declare_summary : string -> 'a summary_declaration -> unit val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref +(* As [ref] but the value is local to a process, i.e. not sent to, say, proof + * workers. It is useful to implement a local cache for example. *) +module Local : sig + + type 'a local_ref + val ref : ?freeze:('a -> 'a) -> name:string -> 'a -> 'a local_ref + val (:=) : 'a local_ref -> 'a -> unit + val (!) : 'a local_ref -> 'a + +end + (** Special name for the summary of ML modules. This summary entry is special because its unfreeze may load ML code and hence add summary entries. Thus is has to be recognizable, and handled appropriately *) @@ -71,3 +82,7 @@ val unfreeze_summary : frozen_bits -> unit val surgery_summary : frozen -> frozen_bits -> frozen val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits val pointer_equal : frozen_bits -> frozen_bits -> bool + +(** {6 Debug} *) + +val dump : unit -> (int * string) list diff --git a/library/universes.ml b/library/universes.ml deleted file mode 100644 index 79070763ec..0000000000 --- a/library/universes.ml +++ /dev/null @@ -1,1006 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Util -open Pp -open Names -open Term -open Environ -open Univ - -type universe_names = - Univ.universe_level Idmap.t * Id.t Univ.LMap.t - -let global_universes = Summary.ref ~name:"Global universe names" - ((Idmap.empty, Univ.LMap.empty) : universe_names) - -let global_universe_names () = !global_universes -let set_global_universe_names s = global_universes := s - -let pr_with_global_universes l = - try Nameops.pr_id (LMap.find l (snd !global_universes)) - with Not_found -> Level.pr l - -type universe_constraint_type = ULe | UEq | ULub - -type universe_constraint = universe * universe_constraint_type * universe - -module Constraints = struct - module S = Set.Make( - struct - type t = universe_constraint - - let compare_type c c' = - match c, c' with - | ULe, ULe -> 0 - | ULe, _ -> -1 - | _, ULe -> 1 - | UEq, UEq -> 0 - | UEq, _ -> -1 - | ULub, ULub -> 0 - | ULub, _ -> 1 - - let compare (u,c,v) (u',c',v') = - let i = compare_type c c' in - if Int.equal i 0 then - let i' = Universe.compare u u' in - if Int.equal i' 0 then Universe.compare v v' - else - if c != ULe && Universe.compare u v' = 0 && Universe.compare v u' = 0 then 0 - else i' - else i - end) - - include S - - let add (l,d,r as cst) s = - if Universe.equal l r then s - else add cst s - - let tr_dir = function - | ULe -> Le - | UEq -> Eq - | ULub -> Eq - - let op_str = function ULe -> " <= " | UEq -> " = " | ULub -> " /\\ " - - let pr c = - fold (fun (u1,op,u2) pp_std -> - pp_std ++ Universe.pr u1 ++ str (op_str op) ++ - Universe.pr u2 ++ fnl ()) c (str "") - - let equal x y = - x == y || equal x y - -end - -type universe_constraints = Constraints.t -type 'a universe_constrained = 'a * universe_constraints - -type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints - -let enforce_eq_instances_univs strict x y c = - let d = if strict then ULub else UEq in - let ax = Instance.to_array x and ay = Instance.to_array y in - if Array.length ax != Array.length ay then - Errors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++ - Pp.str " instances of different lengths"); - CArray.fold_right2 - (fun x y -> Constraints.add (Universe.make x, d, Universe.make y)) - ax ay c - -let subst_univs_universe_constraint fn (u,d,v) = - let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in - if Universe.equal u' v' then None - else Some (u',d,v') - -let subst_univs_universe_constraints subst csts = - Constraints.fold - (fun c -> Option.fold_right Constraints.add (subst_univs_universe_constraint subst c)) - csts Constraints.empty - - -let to_constraints g s = - let tr (x,d,y) acc = - let add l d l' acc = Constraint.add (l,Constraints.tr_dir d,l') acc in - match Universe.level x, d, Universe.level y with - | Some l, (ULe | UEq | ULub), Some l' -> add l d l' acc - | _, ULe, Some l' -> enforce_leq x y acc - | _, ULub, _ -> acc - | _, d, _ -> - let f = if d == ULe then check_leq else check_eq in - if f g x y then acc else - raise (Invalid_argument - "to_constraints: non-trivial algebraic constraint between universes") - in Constraints.fold tr s Constraint.empty - -let eq_constr_univs_infer univs m n = - if m == n then true, Constraints.empty - else - let cstrs = ref Constraints.empty in - let eq_universes strict = Univ.Instance.check_eq univs in - let eq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else - let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true - else - (cstrs := Constraints.add (u1, UEq, u2) !cstrs; - true) - in - let rec eq_constr' m n = - m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n - in - let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in - res, !cstrs - -let leq_constr_univs_infer univs m n = - if m == n then true, Constraints.empty - else - let cstrs = ref Constraints.empty in - let eq_universes strict l l' = Univ.Instance.check_eq univs l l' in - let eq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else - let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true - else (cstrs := Constraints.add (u1, UEq, u2) !cstrs; - true) - in - let leq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else - let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_leq univs u1 u2 then true - else - (cstrs := Constraints.add (u1, ULe, u2) !cstrs; - true) - in - let rec eq_constr' m n = - m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n - in - let rec compare_leq m n = - Constr.compare_head_gen_leq eq_universes eq_sorts leq_sorts - eq_constr' leq_constr' m n - and leq_constr' m n = m == n || compare_leq m n in - let res = compare_leq m n in - res, !cstrs - -let eq_constr_universes m n = - if m == n then true, Constraints.empty - else - let cstrs = ref Constraints.empty in - let eq_universes strict l l' = - cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in - let eq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else - (cstrs := Constraints.add - (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs; - true) - in - let rec eq_constr' m n = - m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n - in - let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in - res, !cstrs - -let leq_constr_universes m n = - if m == n then true, Constraints.empty - else - let cstrs = ref Constraints.empty in - let eq_universes strict l l' = - cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in - let eq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else (cstrs := Constraints.add - (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs; - true) - in - let leq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else - (cstrs := Constraints.add - (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs; - true) - in - let rec eq_constr' m n = - m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n - in - let rec compare_leq m n = - Constr.compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n - and leq_constr' m n = m == n || compare_leq m n in - let res = compare_leq m n in - res, !cstrs - -let compare_head_gen_proj env equ eqs eqc' m n = - match kind_of_term m, kind_of_term n with - | Proj (p, c), App (f, args) - | App (f, args), Proj (p, c) -> - (match kind_of_term f with - | Const (p', u) when eq_constant (Projection.constant p) p' -> - let pb = Environ.lookup_projection p env in - let npars = pb.Declarations.proj_npars in - if Array.length args == npars + 1 then - eqc' c args.(npars) - else false - | _ -> false) - | _ -> Constr.compare_head_gen equ eqs eqc' m n - -let eq_constr_universes_proj env m n = - if m == n then true, Constraints.empty - else - let cstrs = ref Constraints.empty in - let eq_universes strict l l' = - cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in - let eq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else - (cstrs := Constraints.add - (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs; - true) - in - let rec eq_constr' m n = - m == n || compare_head_gen_proj env eq_universes eq_sorts eq_constr' m n - in - let res = eq_constr' m n in - res, !cstrs - -(* Generator of levels *) -let new_univ_level, set_remote_new_univ_level = - RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1) - ~build:(fun n -> Univ.Level.make (Global.current_dirpath ()) n) - -let new_univ_level _ = new_univ_level () - (* Univ.Level.make db (new_univ_level ()) *) - -let fresh_level () = new_univ_level (Global.current_dirpath ()) - -(* TODO: remove *) -let new_univ dp = Univ.Universe.make (new_univ_level dp) -let new_Type dp = mkType (new_univ dp) -let new_Type_sort dp = Type (new_univ dp) - -let fresh_universe_instance ctx = - Instance.subst_fn (fun _ -> new_univ_level (Global.current_dirpath ())) - (UContext.instance ctx) - -let fresh_instance_from_context ctx = - let inst = fresh_universe_instance ctx in - let constraints = instantiate_univ_constraints inst ctx in - inst, constraints - -let fresh_instance ctx = - let ctx' = ref LSet.empty in - let inst = - Instance.subst_fn (fun v -> - let u = new_univ_level (Global.current_dirpath ()) in - ctx' := LSet.add u !ctx'; u) - (UContext.instance ctx) - in !ctx', inst - -let existing_instance ctx inst = - let () = - let a1 = Instance.to_array inst - and a2 = Instance.to_array (UContext.instance ctx) in - let len1 = Array.length a1 and len2 = Array.length a2 in - if not (len1 == len2) then - Errors.errorlabstrm "Universes" - (str "Polymorphic constant expected " ++ int len2 ++ - str" levels but was given " ++ int len1) - else () - in LSet.empty, inst - -let fresh_instance_from ctx inst = - let ctx', inst = - match inst with - | Some inst -> existing_instance ctx inst - | None -> fresh_instance ctx - in - let constraints = instantiate_univ_constraints inst ctx in - inst, (ctx', constraints) - -let unsafe_instance_from ctx = - (Univ.UContext.instance ctx, ctx) - -(** Fresh universe polymorphic construction *) - -let fresh_constant_instance env c inst = - let cb = lookup_constant c env in - if cb.Declarations.const_polymorphic then - let inst, ctx = - fresh_instance_from - (Declareops.universes_of_constant (Environ.opaque_tables env) cb) inst - in - ((c, inst), ctx) - else ((c,Instance.empty), ContextSet.empty) - -let fresh_inductive_instance env ind inst = - let mib, mip = Inductive.lookup_mind_specif env ind in - if mib.Declarations.mind_polymorphic then - let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in - ((ind,inst), ctx) - else ((ind,Instance.empty), ContextSet.empty) - -let fresh_constructor_instance env (ind,i) inst = - let mib, mip = Inductive.lookup_mind_specif env ind in - if mib.Declarations.mind_polymorphic then - let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in - (((ind,i),inst), ctx) - else (((ind,i),Instance.empty), ContextSet.empty) - -let unsafe_constant_instance env c = - let cb = lookup_constant c env in - if cb.Declarations.const_polymorphic then - let inst, ctx = unsafe_instance_from - (Declareops.universes_of_constant (Environ.opaque_tables env) cb) in - ((c, inst), ctx) - else ((c,Instance.empty), UContext.empty) - -let unsafe_inductive_instance env ind = - let mib, mip = Inductive.lookup_mind_specif env ind in - if mib.Declarations.mind_polymorphic then - let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in - ((ind,inst), ctx) - else ((ind,Instance.empty), UContext.empty) - -let unsafe_constructor_instance env (ind,i) = - let mib, mip = Inductive.lookup_mind_specif env ind in - if mib.Declarations.mind_polymorphic then - let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in - (((ind,i),inst), ctx) - else (((ind,i),Instance.empty), UContext.empty) - -open Globnames - -let fresh_global_instance ?names env gr = - match gr with - | VarRef id -> mkVar id, ContextSet.empty - | ConstRef sp -> - let c, ctx = fresh_constant_instance env sp names in - mkConstU c, ctx - | ConstructRef sp -> - let c, ctx = fresh_constructor_instance env sp names in - mkConstructU c, ctx - | IndRef sp -> - let c, ctx = fresh_inductive_instance env sp names in - mkIndU c, ctx - -let fresh_constant_instance env sp = - fresh_constant_instance env sp None - -let fresh_inductive_instance env sp = - fresh_inductive_instance env sp None - -let fresh_constructor_instance env sp = - fresh_constructor_instance env sp None - -let unsafe_global_instance env gr = - match gr with - | VarRef id -> mkVar id, UContext.empty - | ConstRef sp -> - let c, ctx = unsafe_constant_instance env sp in - mkConstU c, ctx - | ConstructRef sp -> - let c, ctx = unsafe_constructor_instance env sp in - mkConstructU c, ctx - | IndRef sp -> - let c, ctx = unsafe_inductive_instance env sp in - mkIndU c, ctx - -let constr_of_global gr = - let c, ctx = fresh_global_instance (Global.env ()) gr in - if not (Univ.ContextSet.is_empty ctx) then - if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then - (* Should be an error as we might forget constraints, allow for now - to make firstorder work with "using" clauses *) - c - else raise (Invalid_argument - ("constr_of_global: globalization of polymorphic reference " ^ - Pp.string_of_ppcmds (Nametab.pr_global_env Id.Set.empty gr) ^ - " would forget universes.")) - else c - -let constr_of_reference = constr_of_global - -let unsafe_constr_of_global gr = - unsafe_global_instance (Global.env ()) gr - -let constr_of_global_univ (gr,u) = - match gr with - | VarRef id -> mkVar id - | ConstRef sp -> mkConstU (sp,u) - | ConstructRef sp -> mkConstructU (sp,u) - | IndRef sp -> mkIndU (sp,u) - -let fresh_global_or_constr_instance env = function - | IsConstr c -> c, ContextSet.empty - | IsGlobal gr -> fresh_global_instance env gr - -let global_of_constr c = - match kind_of_term c with - | Const (c, u) -> ConstRef c, u - | Ind (i, u) -> IndRef i, u - | Construct (c, u) -> ConstructRef c, u - | Var id -> VarRef id, Instance.empty - | _ -> raise Not_found - -let global_app_of_constr c = - match kind_of_term c with - | Const (c, u) -> (ConstRef c, u), None - | Ind (i, u) -> (IndRef i, u), None - | Construct (c, u) -> (ConstructRef c, u), None - | Var id -> (VarRef id, Instance.empty), None - | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c - | _ -> raise Not_found - -open Declarations - -let type_of_reference env r = - match r with - | VarRef id -> Environ.named_type id env, ContextSet.empty - | ConstRef c -> - let cb = Environ.lookup_constant c env in - let ty = Typeops.type_of_constant_type env cb.const_type in - if cb.const_polymorphic then - let inst, ctx = fresh_instance_from (Declareops.universes_of_constant (Environ.opaque_tables env) cb) None in - Vars.subst_instance_constr inst ty, ctx - else ty, ContextSet.empty - - | IndRef ind -> - let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - if mib.mind_polymorphic then - let inst, ctx = fresh_instance_from mib.mind_universes None in - let ty = Inductive.type_of_inductive env (specif, inst) in - ty, ctx - else - let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in - ty, ContextSet.empty - | ConstructRef cstr -> - let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - if mib.mind_polymorphic then - let inst, ctx = fresh_instance_from mib.mind_universes None in - Inductive.type_of_constructor (cstr,inst) specif, ctx - else Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty - -let type_of_global t = type_of_reference (Global.env ()) t - -let unsafe_type_of_reference env r = - match r with - | VarRef id -> Environ.named_type id env - | ConstRef c -> - let cb = Environ.lookup_constant c env in - Typeops.type_of_constant_type env cb.const_type - - | IndRef ind -> - let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - let (_, inst), _ = unsafe_inductive_instance env ind in - Inductive.type_of_inductive env (specif, inst) - - | ConstructRef (ind, _ as cstr) -> - let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - let (_, inst), _ = unsafe_inductive_instance env ind in - Inductive.type_of_constructor (cstr,inst) specif - -let unsafe_type_of_global t = unsafe_type_of_reference (Global.env ()) t - -let fresh_sort_in_family env = function - | InProp -> prop_sort, ContextSet.empty - | InSet -> set_sort, ContextSet.empty - | InType -> - let u = fresh_level () in - Type (Univ.Universe.make u), ContextSet.singleton u - -let new_sort_in_family sf = - fst (fresh_sort_in_family (Global.env ()) sf) - -let extend_context (a, ctx) (ctx') = - (a, ContextSet.union ctx ctx') - -let new_global_univ () = - let u = fresh_level () in - (Univ.Universe.make u, ContextSet.singleton u) - -(** Simplification *) - -module LevelUnionFind = Unionfind.Make (Univ.LSet) (Univ.LMap) - -let add_list_map u t map = - try - let l = LMap.find u map in - LMap.update u (t :: l) map - with Not_found -> - LMap.add u [t] map - -module UF = LevelUnionFind - -(** Precondition: flexible <= ctx *) -let choose_canonical ctx flexible algs s = - let global = LSet.diff s ctx in - let flexible, rigid = LSet.partition flexible (LSet.inter s ctx) in - (** If there is a global universe in the set, choose it *) - if not (LSet.is_empty global) then - let canon = LSet.choose global in - canon, (LSet.remove canon global, rigid, flexible) - else (** No global in the equivalence class, choose a rigid one *) - if not (LSet.is_empty rigid) then - let canon = LSet.choose rigid in - canon, (global, LSet.remove canon rigid, flexible) - else (** There are only flexible universes in the equivalence - class, choose a non-algebraic. *) - let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in - if not (LSet.is_empty nonalgs) then - let canon = LSet.choose nonalgs in - canon, (global, rigid, LSet.remove canon flexible) - else - let canon = LSet.choose algs in - canon, (global, rigid, LSet.remove canon flexible) - -let subst_univs_fn_puniverses lsubst (c, u as cu) = - let u' = Instance.subst_fn lsubst u in - if u' == u then cu else (c, u') - -let nf_evars_and_universes_opt_subst f subst = - let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in - let lsubst = Univ.level_subst_of subst in - let rec aux c = - match kind_of_term c with - | Evar (evk, args) -> - let args = Array.map aux args in - (match try f (evk, args) with Not_found -> None with - | None -> c - | Some c -> aux c) - | Const pu -> - let pu' = subst_univs_fn_puniverses lsubst pu in - if pu' == pu then c else mkConstU pu' - | Ind pu -> - let pu' = subst_univs_fn_puniverses lsubst pu in - if pu' == pu then c else mkIndU pu' - | Construct pu -> - let pu' = subst_univs_fn_puniverses lsubst pu in - if pu' == pu then c else mkConstructU pu' - | Sort (Type u) -> - let u' = Univ.subst_univs_universe subst u in - if u' == u then c else mkSort (sort_of_univ u') - | _ -> map_constr aux c - in aux - -let fresh_universe_context_set_instance ctx = - if ContextSet.is_empty ctx then LMap.empty, ctx - else - let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in - let univs',subst = LSet.fold - (fun u (univs',subst) -> - let u' = fresh_level () in - (LSet.add u' univs', LMap.add u u' subst)) - univs (LSet.empty, LMap.empty) - in - let cst' = subst_univs_level_constraints subst cst in - subst, (univs', cst') - -let normalize_univ_variable ~find ~update = - let rec aux cur = - let b = find cur in - let b' = subst_univs_universe aux b in - if Universe.equal b' b then b - else update cur b' - in aux - -let normalize_univ_variable_opt_subst ectx = - let find l = - match Univ.LMap.find l !ectx with - | Some b -> b - | None -> raise Not_found - in - let update l b = - assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - ectx := Univ.LMap.add l (Some b) !ectx; b - in normalize_univ_variable ~find ~update - -let normalize_univ_variable_subst subst = - let find l = Univ.LMap.find l !subst in - let update l b = - assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - subst := Univ.LMap.add l b !subst; b in - normalize_univ_variable ~find ~update - -let normalize_universe_opt_subst subst = - let normlevel = normalize_univ_variable_opt_subst subst in - subst_univs_universe normlevel - -let normalize_universe_subst subst = - let normlevel = normalize_univ_variable_subst subst in - subst_univs_universe normlevel - -let normalize_opt_subst ctx = - let ectx = ref ctx in - let normalize = normalize_univ_variable_opt_subst ectx in - let () = - Univ.LMap.iter (fun u v -> - if Option.is_empty v then () - else try ignore(normalize u) with Not_found -> assert(false)) ctx - in !ectx - -type universe_opt_subst = universe option universe_map - -let make_opt_subst s = - fun x -> - (match Univ.LMap.find x s with - | Some u -> u - | None -> raise Not_found) - -let subst_opt_univs_constr s = - let f = make_opt_subst s in - Vars.subst_univs_fn_constr f - - -let normalize_univ_variables ctx = - let ctx = normalize_opt_subst ctx in - let undef, def, subst = - Univ.LMap.fold (fun u v (undef, def, subst) -> - match v with - | None -> (Univ.LSet.add u undef, def, subst) - | Some b -> (undef, Univ.LSet.add u def, Univ.LMap.add u b subst)) - ctx (Univ.LSet.empty, Univ.LSet.empty, Univ.LMap.empty) - in ctx, undef, def, subst - -let pr_universe_body = function - | None -> mt () - | Some v -> str" := " ++ Univ.Universe.pr v - -let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body - -exception Found of Level.t -let find_inst insts v = - try LMap.iter (fun k (enf,alg,v') -> - if not alg && enf && Universe.equal v' v then raise (Found k)) - insts; raise Not_found - with Found l -> l - -let compute_lbound left = - (** The universe variable was not fixed yet. - Compute its level using its lower bound. *) - let sup l lbound = - match lbound with - | None -> Some l - | Some l' -> Some (Universe.sup l l') - in - List.fold_left (fun lbound (d, l) -> - if d == Le (* l <= ?u *) then sup l lbound - else (* l < ?u *) - (assert (d == Lt); - if not (Universe.level l == None) then - sup (Universe.super l) lbound - else None)) - None left - -let instantiate_with_lbound u lbound alg enforce (ctx, us, algs, insts, cstrs) = - if enforce then - let inst = Universe.make u in - let cstrs' = enforce_leq lbound inst cstrs in - (ctx, us, LSet.remove u algs, - LMap.add u (enforce,alg,lbound) insts, cstrs'), (enforce, alg, inst) - else (* Actually instantiate *) - (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs, - LMap.add u (enforce,alg,lbound) insts, cstrs), (enforce, alg, lbound) - -type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t - -let pr_constraints_map cmap = - LMap.fold (fun l cstrs acc -> - Level.pr l ++ str " => " ++ - prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ fnl () - ++ acc) - cmap (mt ()) - -let minimize_univ_variables ctx us algs left right cstrs = - let left, lbounds = - Univ.LMap.fold (fun r lower (left, lbounds as acc) -> - if Univ.LMap.mem r us || not (Univ.LSet.mem r ctx) then acc - else (* Fixed universe, just compute its glb for sharing *) - let lbounds' = - match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with - | None -> lbounds - | Some lbound -> LMap.add r (true, false, lbound) lbounds - in (Univ.LMap.remove r left, lbounds')) - left (left, Univ.LMap.empty) - in - let rec instance (ctx', us, algs, insts, cstrs as acc) u = - let acc, left = - try let l = LMap.find u left in - List.fold_left (fun (acc, left') (d, l) -> - let acc', (enf,alg,l') = aux acc l in - (* if alg then assert(not alg); *) - let l' = - if enf then Universe.make l - else l' - (* match Universe.level l' with Some _ -> l' | None -> Universe.make l *) - in - acc', (d, l') :: left') (acc, []) l - with Not_found -> acc, [] - and right = - try Some (LMap.find u right) - with Not_found -> None - in - let instantiate_lbound lbound = - let alg = LSet.mem u algs in - if alg then - (* u is algebraic and has no upper bound constraints: we - instantiate it with it's lower bound, if any *) - instantiate_with_lbound u lbound true false acc - else (* u is non algebraic *) - match Universe.level lbound with - | Some l -> (* The lowerbound is directly a level *) - (* u is not algebraic but has no upper bounds, - we instantiate it with its lower bound if it is a - different level, otherwise we keep it. *) - if not (Level.equal l u) && not (LSet.mem l algs) then - (* if right = None then. Should check that u does not - have upper constraints that are not already in right *) - instantiate_with_lbound u lbound false false acc - (* else instantiate_with_lbound u lbound false true acc *) - else - (* assert false: l can't be alg *) - acc, (true, false, lbound) - | None -> - try - (* if right <> None then raise Not_found; *) - (* Another universe represents the same lower bound, - we can share them with no harm. *) - let can = find_inst insts lbound in - instantiate_with_lbound u (Universe.make can) false false acc - with Not_found -> - (* We set u as the canonical universe representing lbound *) - instantiate_with_lbound u lbound false true acc - in - let acc' acc = - match right with - | None -> acc - | Some cstrs -> - let dangling = List.filter (fun (d, r) -> not (LMap.mem r us)) cstrs in - if List.is_empty dangling then acc - else - let ((ctx', us, algs, insts, cstrs), (enf,_,inst as b)) = acc in - let cstrs' = List.fold_left (fun cstrs (d, r) -> - if d == Univ.Le then - enforce_leq inst (Universe.make r) cstrs - else - try let lev = Option.get (Universe.level inst) in - Constraint.add (lev, d, r) cstrs - with Option.IsNone -> assert false) - cstrs dangling - in - (ctx', us, algs, insts, cstrs'), b - in - if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u)) - else - let lbound = compute_lbound left in - match lbound with - | None -> (* Nothing to do *) - acc' (acc, (true, false, Universe.make u)) - | Some lbound -> - acc' (instantiate_lbound lbound) - and aux (ctx', us, algs, seen, cstrs as acc) u = - try acc, LMap.find u seen - with Not_found -> instance acc u - in - LMap.fold (fun u v (ctx', us, algs, seen, cstrs as acc) -> - if v == None then fst (aux acc u) - else LSet.remove u ctx', us, LSet.remove u algs, seen, cstrs) - us (ctx, us, algs, lbounds, cstrs) - -let normalize_context_set ctx us algs = - let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in - let uf = UF.create () in - let csts = - (* We first put constraints in a normal-form: all self-loops are collapsed - to equalities. *) - let g = Univ.merge_constraints csts Univ.empty_universes in - Univ.constraints_of_universes g - in - let noneqs = - Constraint.fold (fun (l,d,r) noneqs -> - if d == Eq then (UF.union l r uf; noneqs) - else Constraint.add (l,d,r) noneqs) - csts Constraint.empty - in - let partition = UF.partition uf in - let flex x = LMap.mem x us in - let ctx, subst, eqs = List.fold_left (fun (ctx, subst, cstrs) s -> - let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in - (* Add equalities for globals which can't be merged anymore. *) - let cstrs = LSet.fold (fun g cst -> - Constraint.add (canon, Univ.Eq, g) cst) global - cstrs - in - let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in - let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in - (LSet.diff (LSet.diff ctx rigid) flexible, subst, cstrs)) - (ctx, LMap.empty, Constraint.empty) partition - in - (* Noneqs is now in canonical form w.r.t. equality constraints, - and contains only inequality constraints. *) - let noneqs = subst_univs_level_constraints subst noneqs in - let us = LMap.fold (fun u v acc -> LMap.add u (Some (Universe.make v)) acc) subst us in - (* Compute the left and right set of flexible variables, constraints - mentionning other variables remain in noneqs. *) - let noneqs, ucstrsl, ucstrsr = - Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) -> - let lus = LMap.mem l us - and rus = LMap.mem r us - in - let ucstrsl' = - if lus then add_list_map l (d, r) ucstrsl - else ucstrsl - and ucstrsr' = - add_list_map r (d, l) ucstrsr - in - let noneqs = - if lus || rus then noneq - else Constraint.add cstr noneq - in (noneqs, ucstrsl', ucstrsr')) - noneqs (Constraint.empty, LMap.empty, LMap.empty) - in - (* Now we construct the instantiation of each variable. *) - let ctx', us, algs, inst, noneqs = - minimize_univ_variables ctx us algs ucstrsr ucstrsl noneqs - in - let us = normalize_opt_subst us in - (us, algs), (ctx', Constraint.union noneqs eqs) - -(* let normalize_conkey = Profile.declare_profile "normalize_context_set" *) -(* let normalize_context_set a b c = Profile.profile3 normalize_conkey normalize_context_set a b c *) - -let universes_of_constr c = - let rec aux s c = - match kind_of_term c with - | Const (_, u) | Ind (_, u) | Construct (_, u) -> - LSet.union (Instance.levels u) s - | Sort u when not (Sorts.is_small u) -> - let u = univ_of_sort u in - LSet.union (Universe.levels u) s - | _ -> fold_constr aux s c - in aux LSet.empty c - -let restrict_universe_context (univs,csts) s = - (* Universes that are not necessary to typecheck the term. - E.g. univs introduced by tactics and not used in the proof term. *) - let diff = LSet.diff univs s in - let rec aux diff candid univs ness = - let (diff', candid', univs', ness') = - Constraint.fold - (fun (l, d, r as c) (diff, candid, univs, csts) -> - if not (LSet.mem l diff) then - (LSet.remove r diff, candid, univs, Constraint.add c csts) - else if not (LSet.mem r diff) then - (LSet.remove l diff, candid, univs, Constraint.add c csts) - else (diff, Constraint.add c candid, univs, csts)) - candid (diff, Constraint.empty, univs, ness) - in - if ness' == ness then (LSet.diff univs diff', ness) - else aux diff' candid' univs' ness' - in aux diff csts univs Constraint.empty - -let simplify_universe_context (univs,csts) = - let uf = UF.create () in - let noneqs = - Constraint.fold (fun (l,d,r) noneqs -> - if d == Eq && (LSet.mem l univs || LSet.mem r univs) then - (UF.union l r uf; noneqs) - else Constraint.add (l,d,r) noneqs) - csts Constraint.empty - in - let partition = UF.partition uf in - let flex x = LSet.mem x univs in - let subst, univs', csts' = List.fold_left (fun (subst, univs, cstrs) s -> - let canon, (global, rigid, flexible) = choose_canonical univs flex LSet.empty s in - (* Add equalities for globals which can't be merged anymore. *) - let cstrs = LSet.fold (fun g cst -> - Constraint.add (canon, Univ.Eq, g) cst) (LSet.union global rigid) - cstrs - in - let subst = LSet.fold (fun f -> LMap.add f canon) - flexible subst - in (subst, LSet.diff univs flexible, cstrs)) - (LMap.empty, univs, noneqs) partition - in - (* Noneqs is now in canonical form w.r.t. equality constraints, - and contains only inequality constraints. *) - let csts' = subst_univs_level_constraints subst csts' in - (univs', csts'), subst - -let is_small_leq (l,d,r) = - Level.is_small l && d == Univ.Le - -(* Prop < i <-> Set+1 <= i <-> Set < i *) -let translate_cstr (l,d,r as cstr) = - if Level.equal Level.prop l && d == Univ.Lt then - (Level.set, d, r) - else cstr - -let refresh_constraints univs (ctx, cstrs) = - let cstrs', univs' = - Univ.Constraint.fold (fun c (cstrs', univs as acc) -> - let c = translate_cstr c in - if Univ.check_constraint univs c && not (is_small_leq c) then acc - else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs)) - cstrs (Univ.Constraint.empty, univs) - in ((ctx, cstrs'), univs') - - -(**********************************************************************) -(* Tools for sort-polymorphic inductive types *) - -(* Miscellaneous functions to remove or test local univ assumed to - occur only in the le constraints *) - -(* - Solve a system of universe constraint of the form - - u_s11, ..., u_s1p1, w1 <= u1 - ... - u_sn1, ..., u_snpn, wn <= un - -where - - - the ui (1 <= i <= n) are universe variables, - - the sjk select subsets of the ui for each equations, - - the wi are arbitrary complex universes that do not mention the ui. -*) - -let is_direct_sort_constraint s v = match s with - | Some u -> univ_level_mem u v - | None -> false - -let solve_constraints_system levels level_bounds level_min = - let open Univ in - let levels = - Array.mapi (fun i o -> - match o with - | Some u -> - (match Universe.level u with - | Some u -> Some u - | _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None) - | None -> None) - levels in - let v = Array.copy level_bounds in - let nind = Array.length v in - let clos = Array.map (fun _ -> Int.Set.empty) levels in - (* First compute the transitive closure of the levels dependencies *) - for i=0 to nind-1 do - for j=0 to nind-1 do - if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then - clos.(i) <- Int.Set.add j clos.(i); - done; - done; - let rec closure () = - let continue = ref false in - Array.iteri (fun i deps -> - let deps' = - Int.Set.fold (fun j acc -> Int.Set.union acc clos.(j)) deps deps - in - if Int.Set.equal deps deps' then () - else (clos.(i) <- deps'; continue := true)) - clos; - if !continue then closure () - else () - in - closure (); - for i=0 to nind-1 do - for j=0 to nind-1 do - if not (Int.equal i j) && Int.Set.mem j clos.(i) then - (v.(i) <- Universe.sup v.(i) level_bounds.(j); - level_min.(i) <- Universe.sup level_min.(i) level_min.(j)) - done; - for j=0 to nind-1 do - match levels.(j) with - | Some u -> v.(i) <- univ_level_rem u v.(i) level_min.(i) - | None -> () - done - done; - v diff --git a/library/universes.mli b/library/universes.mli deleted file mode 100644 index f2f68d329c..0000000000 --- a/library/universes.mli +++ /dev/null @@ -1,253 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Util -open Pp -open Names -open Term -open Context -open Environ -open Locus -open Univ - -(** Universes *) - -type universe_names = - Univ.universe_level Idmap.t * Id.t Univ.LMap.t - -val global_universe_names : unit -> universe_names -val set_global_universe_names : universe_names -> unit - -val pr_with_global_universes : Level.t -> Pp.std_ppcmds - -(** The global universe counter *) -val set_remote_new_univ_level : universe_level RemoteCounter.installer - -(** Side-effecting functions creating new universe levels. *) - -val new_univ_level : Names.dir_path -> universe_level -val new_univ : Names.dir_path -> universe -val new_Type : Names.dir_path -> types -val new_Type_sort : Names.dir_path -> sorts - -val new_global_univ : unit -> universe in_universe_context_set -val new_sort_in_family : sorts_family -> sorts - -(** {6 Constraints for type inference} - - When doing conversion of universes, not only do we have =/<= constraints but - also Lub constraints which correspond to unification of two levels which might - not be necessary if unfolding is performed. -*) - -type universe_constraint_type = ULe | UEq | ULub - -type universe_constraint = universe * universe_constraint_type * universe -module Constraints : sig - include Set.S with type elt = universe_constraint - - val pr : t -> Pp.std_ppcmds -end - -type universe_constraints = Constraints.t -type 'a universe_constrained = 'a * universe_constraints -type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints - -val subst_univs_universe_constraints : universe_subst_fn -> - universe_constraints -> universe_constraints - -val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_function - -val to_constraints : universes -> universe_constraints -> constraints - -(** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts, - application grouping, the universe constraints in [u] and additional constraints [c]. *) -val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained - -(** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b] - modulo alpha, casts, application grouping, the universe constraints - in [u] and additional constraints [c]. *) -val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained - -(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, - application grouping and the universe constraints in [c]. *) -val eq_constr_universes : constr -> constr -> bool universe_constrained - -(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo - alpha, casts, application grouping and the universe constraints in [c]. *) -val leq_constr_universes : constr -> constr -> bool universe_constrained - -(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, - application grouping and the universe constraints in [c]. *) -val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrained - -(** Build a fresh instance for a given context, its associated substitution and - the instantiated constraints. *) - -val fresh_instance_from_context : universe_context -> - universe_instance constrained - -val fresh_instance_from : universe_context -> universe_instance option -> - universe_instance in_universe_context_set - -val fresh_sort_in_family : env -> sorts_family -> - sorts in_universe_context_set -val fresh_constant_instance : env -> constant -> - pconstant in_universe_context_set -val fresh_inductive_instance : env -> inductive -> - pinductive in_universe_context_set -val fresh_constructor_instance : env -> constructor -> - pconstructor in_universe_context_set - -val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_reference -> - constr in_universe_context_set - -val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> - constr in_universe_context_set - -(** Get fresh variables for the universe context. - Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) -val fresh_universe_context_set_instance : universe_context_set -> - universe_level_subst * universe_context_set - -(** Raises [Not_found] if not a global reference. *) -val global_of_constr : constr -> Globnames.global_reference puniverses - -val global_app_of_constr : constr -> Globnames.global_reference puniverses * constr option - -val constr_of_global_univ : Globnames.global_reference puniverses -> constr - -val extend_context : 'a in_universe_context_set -> universe_context_set -> - 'a in_universe_context_set - -(** Simplification and pruning of constraints: - [normalize_context_set ctx us] - - - Instantiate the variables in [us] with their most precise - universe levels respecting the constraints. - - - Normalizes the context [ctx] w.r.t. equality constraints, - choosing a canonical universe in each equivalence class - (a global one if there is one) and transitively saturate - the constraints w.r.t to the equalities. *) - -module UF : Unionfind.PartitionSig with type elt = universe_level - -type universe_opt_subst = universe option universe_map - -val make_opt_subst : universe_opt_subst -> universe_subst_fn - -val subst_opt_univs_constr : universe_opt_subst -> constr -> constr - -val normalize_context_set : universe_context_set -> - universe_opt_subst (* The defined and undefined variables *) -> - universe_set (* univ variables that can be substituted by algebraics *) -> - (universe_opt_subst * universe_set) in_universe_context_set - -val normalize_univ_variables : universe_opt_subst -> - universe_opt_subst * universe_set * universe_set * universe_subst - -val normalize_univ_variable : - find:(universe_level -> universe) -> - update:(universe_level -> universe -> universe) -> - universe_level -> universe - -val normalize_univ_variable_opt_subst : universe_opt_subst ref -> - (universe_level -> universe) - -val normalize_univ_variable_subst : universe_subst ref -> - (universe_level -> universe) - -val normalize_universe_opt_subst : universe_opt_subst ref -> - (universe -> universe) - -val normalize_universe_subst : universe_subst ref -> - (universe -> universe) - -(** Create a fresh global in the global environment, without side effects. - BEWARE: this raises an ANOMALY on polymorphic constants/inductives: - the constraints should be properly added to an evd. - See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for - the proper way to get a fresh copy of a global reference. *) -val constr_of_global : Globnames.global_reference -> constr - -(** ** DEPRECATED ** synonym of [constr_of_global] *) -val constr_of_reference : Globnames.global_reference -> constr - -(** [unsafe_constr_of_global gr] turns [gr] into a constr, works on polymorphic - references by taking the original universe instance that is not recorded - anywhere. The constraints are forgotten as well. DO NOT USE in new code. *) -val unsafe_constr_of_global : Globnames.global_reference -> constr in_universe_context - -(** Returns the type of the global reference, by creating a fresh instance of polymorphic - references and computing their instantiated universe context. (side-effect on the - universe counter, use with care). *) -val type_of_global : Globnames.global_reference -> types in_universe_context_set - -(** [unsafe_type_of_global gr] returns [gr]'s type, works on polymorphic - references by taking the original universe instance that is not recorded - anywhere. The constraints are forgotten as well. - USE with care. *) -val unsafe_type_of_global : Globnames.global_reference -> types - -(** Full universes substitutions into terms *) - -val nf_evars_and_universes_opt_subst : (existential -> constr option) -> - universe_opt_subst -> constr -> constr - -(** Shrink a universe context to a restricted set of variables *) - -val universes_of_constr : constr -> universe_set -val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set -val simplify_universe_context : universe_context_set -> - universe_context_set * universe_level_subst - -val refresh_constraints : universes -> universe_context_set -> universe_context_set * universes - -(** Pretty-printing *) - -val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds - -(* For tracing *) - -type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t - -val pr_constraints_map : constraints_map -> Pp.std_ppcmds - -val choose_canonical : universe_set -> (Level.t -> bool) (* flexibles *) -> universe_set -> universe_set -> - universe_level * (universe_set * universe_set * universe_set) - -val compute_lbound : (constraint_type * Univ.universe) list -> universe option - -val instantiate_with_lbound : - Univ.LMap.key -> - Univ.universe -> - bool -> - bool -> - Univ.LSet.t * Univ.universe option Univ.LMap.t * - Univ.LSet.t * - (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints -> - (Univ.LSet.t * Univ.universe option Univ.LMap.t * - Univ.LSet.t * - (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints) * - (bool * bool * Univ.universe) - -val minimize_univ_variables : - Univ.LSet.t -> - Univ.universe option Univ.LMap.t -> - Univ.LSet.t -> - constraints_map -> constraints_map -> - Univ.constraints -> - Univ.LSet.t * Univ.universe option Univ.LMap.t * - Univ.LSet.t * - (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints - -(** {6 Support for old-style sort-polymorphism } *) - -val solve_constraints_system : universe option array -> universe array -> universe array -> - universe array |