diff options
Diffstat (limited to 'library')
44 files changed, 152 insertions, 1700 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml index 0cb8c7afcf..8787738af9 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/coqlib.mli b/library/coqlib.mli index 716d97c9d0..1e3c37a9ed 100644 --- a/library/coqlib.mli +++ b/library/coqlib.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/declare.ml b/library/declare.ml deleted file mode 100644 index db3dbcbd92..0000000000 --- a/library/declare.ml +++ /dev/null @@ -1,564 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <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 *) -(************************************************************************) - -(** This module is about the low-level declaration of logical objects *) - -open Pp -open CErrors -open Util -open Names -open Libnames -open Globnames -open Nameops -open Term -open Declarations -open Entries -open Libobject -open Lib -open Impargs -open Safe_typing -open Cooking -open Decls -open Decl_kinds - -(** flag for internal message display *) -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 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 false ctx - | Inr (id,(p,d,mk)) -> - (* Constr raisonne sur les noms courts *) - if variable_exists id then - alreadydeclared (pr_id id ++ str " already exists"); - - 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,poly),ctx) in - let impl = if impl then Implicit else Explicit in - impl, true, poly, ctx - | SectionLocalDef (de) -> - 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,_) -> - if variable_polymorphic id then None - else Some (Inl (variable_context id)) - | Inl _ -> Some o - -type variable_obj = - (Univ.ContextSet.t, Id.t * variable_declaration) union - -let inVariable : variable_obj -> obj = - declare_object { (default_object "VARIABLE") with - cache_function = cache_variable; - discharge_function = discharge_variable; - classify_function = (fun _ -> Dispose) } - -(* for initial declaration *) -let declare_variable id obj = - let oname = add_leaf id (inVariable (Inr (id,obj))) in - 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 - - -(** Declaration of constants and parameters *) - -type constant_obj = { - cst_decl : global_declaration; - 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 = 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 *) -let load_constant i ((sp,kn), obj) = - if Nametab.exists_cci sp then - alreadydeclared (pr_id (basename sp) ++ str " already exists"); - let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Until i) sp (ConstRef con); - add_constant_kind con obj.cst_kind - -(* Opening means making the name without its module qualification available *) -let open_constant i ((sp,kn), obj) = - (** Never open a local definition *) - if obj.cst_locl then () - else - let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Exactly i) sp (ConstRef con); - 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 false (Future.force f) - | _ -> () - -let exists_name id = - variable_exists id || Global.exists_objlabel (Label.of_id id) - -let check_exists sp = - let id = basename sp in - if exists_name id then alreadydeclared (pr_id id ++ str " already exists") - -let cache_constant ((sp,kn), obj) = - let id = basename sp in - let _,dir,_ = repr_kn kn 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) ++ str".") - 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 (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; - Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps; - add_constant_kind (constant_of_kn kn) obj.cst_kind - -let discharged_hyps kn sechyps = - let (_,dir,_) = repr_kn kn in - let args = Array.to_list (instance_from_variable_context sechyps) in - List.rev_map (Libnames.make_path dir) args - -let discharge_constant ((sp, kn), obj) = - let con = constant_of_kn kn in - let from = Global.lookup_constant con in - let modlist = replacement_context () in - let hyps,subst,uctx = section_segment_of_constant con in - let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in - let abstract = (named_of_variable_context hyps, subst, uctx) in - let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in - Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; } - -(* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant_entry = - 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, 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; - classify_function = classify_constant; - 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 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 - update_tables c; - c - -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; - const_entry_universes = univs; - const_entry_opaque = opaque; - const_entry_feedback = None; - const_entry_inline_code = inline} - -let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = - let export = (* We deal with side effects *) - match cd with - | 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 (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=UserIndividualRequest) - ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) - ?(poly=false) id ?types (body,ctx) = - let cb = - definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body - in - declare_constant ~internal ~local id - (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) - -(** Declaration of inductive blocks *) - -let declare_inductive_argument_scopes kn mie = - List.iteri (fun i {mind_entry_consnames=lc} -> - Notation.declare_ref_arguments_scope (IndRef (kn,i)); - for j=1 to List.length lc do - Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j)); - done) mie.mind_entry_inds - -let inductive_names sp kn mie = - let (dp,_) = repr_path sp in - let kn = Global.mind_of_delta_kn kn in - let names, _ = - List.fold_left - (fun (names, n) ind -> - let ind_p = (kn,n) in - let names, _ = - List.fold_left - (fun (names, p) l -> - let sp = - Libnames.make_path dp l - in - ((sp, ConstructRef (ind_p,p)) :: names, p+1)) - (names, 1) ind.mind_entry_consnames in - let sp = Libnames.make_path dp ind.mind_entry_typename - in - ((sp, IndRef ind_p) :: names, n+1)) - ([], 0) mie.mind_entry_inds - in names - -let load_inductive i ((sp,kn),(_,mie)) = - let names = inductive_names sp kn mie in - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names - -let open_inductive i ((sp,kn),(_,mie)) = - let names = inductive_names sp kn mie in - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names - -let cache_inductive ((sp,kn),(dhyps,mie)) = - let names = inductive_names sp kn mie in - List.iter check_exists (List.map fst names); - let id = basename sp in - let _,dir,_ = repr_kn kn in - 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 (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps; - Dischargedhypsmap.set_discharged_hyps sp dhyps; - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names - -let discharge_inductive ((sp,kn),(dhyps,mie)) = - let mind = Global.mind_of_delta_kn kn in - let mie = Global.lookup_mind mind in - let repl = replacement_context () in - let sechyps,usubst,uctx = section_segment_of_mutual_inductive mind in - Some (discharged_hyps kn sechyps, - Discharge.process_inductive (named_of_variable_context sechyps,uctx) repl mie) - -let dummy_one_inductive_entry mie = { - mind_entry_typename = mie.mind_entry_typename; - mind_entry_arity = mkProp; - mind_entry_template = false; - mind_entry_consnames = mie.mind_entry_consnames; - mind_entry_lc = [] -} - -(* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_inductive_entry (_,m) = ([],{ - mind_entry_params = []; - mind_entry_record = None; - mind_entry_finite = Decl_kinds.BiFinite; - mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; - mind_entry_universes = Monomorphic_ind_entry Univ.UContext.empty; - mind_entry_private = None; -}) - -(* reinfer subtyping constraints for inductive after section is dischared. *) -let infer_inductive_subtyping (pth, mind_ent) = - match mind_ent.mind_entry_universes with - | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> - (pth, mind_ent) - | Cumulative_ind_entry cumi -> - begin - let env = Global.env () in - let env' = - Environ.push_context - (Univ.CumulativityInfo.univ_context cumi) env - in - (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *) - let evd = Evd.from_env env' in - (pth, Inductiveops.infer_inductive_subtyping env' evd mind_ent) - end - -type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry - -let inInductive : inductive_obj -> obj = - declare_object {(default_object "INDUCTIVE") with - cache_function = cache_inductive; - load_function = load_inductive; - open_function = open_inductive; - classify_function = (fun a -> Substitute (dummy_inductive_entry a)); - subst_function = ident_subst_function; - discharge_function = discharge_inductive; - rebuild_function = infer_inductive_subtyping } - -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 -> - 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) - in - assert(eq_constant kn kn')) kns; true,true - | Some None -> true,false - | None -> false,false - -(* for initial declaration *) -let declare_mind mie = - let id = match mie.mind_entry_inds with - | ind::_ -> ind.mind_entry_typename - | [] -> 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 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 *) - -let pr_rank i = pr_nth (i+1) - -let fixpoint_message indexes l = - 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 - | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" - | _ -> mt ()) - | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++ - spc () ++ str "are recursively defined" ++ - match indexes with - | Some a -> spc () ++ str "(decreasing respectively on " ++ - prvect_with_sep pr_comma pr_rank a ++ - str " arguments)" - | None -> mt ())) - -let cofixpoint_message l = - 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 ++ - spc () ++ str "are corecursively defined")) - -let recursive_message isfix i l = - (if isfix then fixpoint_message i else cofixpoint_message) l - -let definition_message id = - Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is defined") - -let assumption_message id = - (* 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_context_decl = polymorphic * Univ.universe_context_set - -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) -> 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 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 (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 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 = cache_constraints; - load_function = (fun _ -> cache_constraints); - discharge_function = discharge_constraints; - classify_function = (fun a -> Keep a) } - -let do_constraint poly l = - let open Misctypes in - let u_of_id x = - match x with - | GProp -> Loc.tag (false, Univ.Level.prop) - | GSet -> Loc.tag (false, Univ.Level.set) - | GType None | GType (Some (_, Anonymous)) -> - user_err ~hdr:"Constraint" - (str "Cannot declare constraints on anonymous universes") - | GType (Some (loc, Name id)) -> - 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 ploc, (p, lu) = u_of_id l and rloc, (p', ru) = u_of_id r in - check_poly ?loc:ploc p rloc p'; - Univ.Constraint.add (lu, d, ru) acc) - Univ.Constraint.empty l - in - Lib.add_anonymous_leaf (input_constraints (poly, constraints)) diff --git a/library/declare.mli b/library/declare.mli deleted file mode 100644 index f70d594d7e..0000000000 --- a/library/declare.mli +++ /dev/null @@ -1,97 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <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 Names -open Libnames -open Term -open Entries -open Decl_kinds - -(** This module provides the official functions to declare new variables, - parameters, constants and inductive types. Using the following functions - will add the entries in the global environment (module [Global]), will - register the declarations in the library (module [Lib]) --- so that the - reset works properly --- and will fill some global tables such as - [Nametab] and [Impargs]. *) - -(** Declaration of local constructions (Variable/Hypothesis/Local) *) - -type section_variable_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 - -val declare_variable : variable -> variable_declaration -> object_name - -(** Declaration of global constructions - i.e. Definition/Theorem/Axiom/Parameter/... *) - -type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind - -type internal_flag = - | UserAutomaticRequest - | InternalTacticRequest - | UserIndividualRequest - -(* Defaut definition entries, transparent with no secctx or proj information *) -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 -> ?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 constants' side effects are globally declared, we - * need that *) -val set_declare_scheme : - (string -> (inductive * constant) array -> unit) -> unit - -(** [declare_mind me] declares a block of inductive types with - their constructors in the current section; it returns the path of - 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 -val assumption_message : Id.t -> unit -val fixpoint_message : int array option -> Id.t list -> unit -val cofixpoint_message : Id.t list -> unit -val recursive_message : bool (** true = fixpoint *) -> - int array option -> Id.t list -> unit - -val exists_name : Id.t -> bool - - - -(** Global universe contexts, names and constraints *) - -val declare_universe_context : polymorphic -> Univ.universe_context_set -> 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 187b749b87..e7aa5bd0d6 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/declaremods.mli b/library/declaremods.mli index 3917fe8d64..005594b8d8 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -121,7 +121,7 @@ val iter_all_segments : (Libnames.object_name -> Libobject.obj -> unit) -> unit -val debug_print_modtab : unit -> Pp.std_ppcmds +val debug_print_modtab : unit -> Pp.t (** For printing modules, [process_module_binding] adds names of bound module (and its components) to Nametab. It also loads diff --git a/library/decls.ml b/library/decls.ml index 2952c258a5..973fe144dd 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/decls.mli b/library/decls.mli index 1ca7f89469..478f0bca0d 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 cea1fd7d6e..1673e13cca 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 ea4a9424e5..69bb6744e5 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 6d80012f47..963c977417 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -86,6 +86,7 @@ let push_context b c = globalize0 (Safe_typing.push_context b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) +let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) 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) @@ -122,12 +123,22 @@ let lookup_modtype kn = lookup_modtype kn (env()) let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ()) let opaque_tables () = Environ.opaque_tables (env ()) -let body_of_constant_body cb = Declareops.body_of_constant (opaque_tables ()) cb + +let instantiate cb c = + let open Declarations in + match cb.const_universes with + | Monomorphic_const _ -> c, Univ.AUContext.empty + | Polymorphic_const ctx -> c, ctx + +let body_of_constant_body cb = + let open Declarations in + let otab = opaque_tables () in + match cb.const_body with + | Undef _ -> None + | Def c -> Some (instantiate cb (Mod_subst.force_constr c)) + | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof otab o)) + let body_of_constant cst = body_of_constant_body (lookup_constant cst) -let constraints_of_constant_body cb = - Declareops.constraints_of_constant (opaque_tables ()) cb -let universes_of_constant_body cb = - Declareops.universes_of_constant (opaque_tables ()) cb (** Operations on kernel names *) @@ -163,54 +174,52 @@ open Globnames (** Build a fresh instance for a given context, its associated substitution and the instantiated constraints. *) -let type_of_global_unsafe r = - let env = env() in +let constr_of_global_in_context env r = + let open Constr in match r with - | VarRef id -> Environ.named_type id env - | ConstRef c -> - let cb = Environ.lookup_constant c env in - let univs = - Declareops.universes_of_polymorphic_constant - (Environ.opaque_tables env) cb in - let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in - Vars.subst_instance_constr (Univ.UContext.instance univs) ty + | VarRef id -> mkVar id, Univ.AUContext.empty + | ConstRef c -> + let cb = Environ.lookup_constant c env in + let univs = Declareops.constant_polymorphic_context cb in + mkConstU (c, Univ.make_abstract_instance univs), univs | IndRef ind -> - let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - let inst = Declareops.inductive_polymorphic_instance mib in - Inductive.type_of_inductive env (specif, inst) + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + let univs = Declareops.inductive_polymorphic_context mib in + mkIndU (ind, Univ.make_abstract_instance univs), univs | ConstructRef cstr -> - let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - let inst = Declareops.inductive_polymorphic_instance mib in - Inductive.type_of_constructor (cstr,inst) specif + let (mib,oib as specif) = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) + in + let univs = Declareops.inductive_polymorphic_context mib in + mkConstructU (cstr, Univ.make_abstract_instance univs), univs let type_of_global_in_context env r = match r with - | VarRef id -> Environ.named_type id env, Univ.UContext.empty + | VarRef id -> Environ.named_type id env, Univ.AUContext.empty | ConstRef c -> - let cb = Environ.lookup_constant c env in - let univs = - Declareops.universes_of_polymorphic_constant - (Environ.opaque_tables env) cb in - Typeops.type_of_constant_type env cb.Declarations.const_type, univs + let cb = Environ.lookup_constant c env in + let univs = Declareops.constant_polymorphic_context cb in + cb.Declarations.const_type, univs | IndRef ind -> - let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - let univs = Declareops.inductive_polymorphic_context mib in - Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + let univs = Declareops.inductive_polymorphic_context mib in + let inst = Univ.make_abstract_instance univs in + let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in + Inductive.type_of_inductive env (specif, inst), univs | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in let univs = Declareops.inductive_polymorphic_context mib in - let inst = Univ.UContext.instance univs in + let inst = Univ.make_abstract_instance univs in Inductive.type_of_constructor (cstr,inst) specif, univs let universes_of_global env r = match r with - | VarRef id -> Univ.UContext.empty + | VarRef id -> Univ.AUContext.empty | ConstRef c -> let cb = Environ.lookup_constant c env in - Declareops.universes_of_polymorphic_constant - (Environ.opaque_tables env) cb + Declareops.constant_polymorphic_context cb | IndRef ind -> let (mib, oib) = Inductive.lookup_mind_specif env ind in Declareops.inductive_polymorphic_context mib @@ -245,7 +254,7 @@ let is_template_polymorphic r = let env = env() in match r with | VarRef id -> false - | ConstRef c -> Environ.template_polymorphic_constant c env + | ConstRef c -> false | IndRef ind -> Environ.template_polymorphic_ind ind env | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env diff --git a/library/global.mli b/library/global.mli index a4a38ce846..c777691d11 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -34,9 +34,12 @@ val set_typing_flags : Declarations.typing_flags -> 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 export_private_constants : in_section:bool -> + Safe_typing.private_constants Entries.constant_entry -> + unit Entries.constant_entry * Safe_typing.exported_private_constant list + val add_constant : - DirPath.t -> Id.t -> Safe_typing.global_declaration -> - constant * Safe_typing.exported_private_constant list + DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant val add_mind : DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive @@ -89,12 +92,15 @@ val constant_of_delta_kn : kernel_name -> constant val mind_of_delta_kn : kernel_name -> mutual_inductive val opaque_tables : unit -> Opaqueproof.opaquetab -val body_of_constant : constant -> Term.constr option -val body_of_constant_body : Declarations.constant_body -> Term.constr option -val constraints_of_constant_body : - Declarations.constant_body -> Univ.constraints -val universes_of_constant_body : - Declarations.constant_body -> Univ.universe_context + +val body_of_constant : constant -> (Term.constr * Univ.AUContext.t) option +(** Returns the body of the constant if it has any, and the polymorphic context + it lives in. For monomorphic constant, the latter is empty, and for + polymorphic constants, the term contains De Bruijn universe variables that + need to be instantiated. *) + +val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AUContext.t) option +(** Same as {!body_of_constant} but on {!Declarations.constant_body}. *) (** Global universe name <-> level mapping *) type universe_names = @@ -126,26 +132,22 @@ 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 -(** Returns the type of the constant in its global or local universe +val constr_of_global_in_context : Environ.env -> + Globnames.global_reference -> Constr.types * Univ.AUContext.t +(** Returns the type of the constant in its 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. *) -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]. *) +val type_of_global_in_context : Environ.env -> + Globnames.global_reference -> Constr.types * Univ.AUContext.t +(** Returns the type of the constant in its 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 its polymorphic status is). *) -val universes_of_global : Globnames.global_reference -> Univ.universe_context +val universes_of_global : Globnames.global_reference -> Univ.abstract_universe_context (** {6 Retroknowledge } *) diff --git a/library/globnames.ml b/library/globnames.ml index 9aeb379737..dc9541a0d5 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/globnames.mli b/library/globnames.mli index f4956e3df2..0b5971b6e1 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/goptions.ml b/library/goptions.ml index a305214e82..184c6fa119 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -57,10 +57,10 @@ module MakeTable = val table : (string * key table_of_A) list ref val encode : key -> t val subst : substitution -> t -> t - val printer : t -> std_ppcmds + val printer : t -> Pp.t val key : option_name val title : string - val member_message : t -> bool -> std_ppcmds + val member_message : t -> bool -> Pp.t end) -> struct type option_mark = @@ -131,7 +131,7 @@ module type StringConvertArg = sig val key : option_name val title : string - val member_message : string -> bool -> std_ppcmds + val member_message : string -> bool -> Pp.t end module StringConvert = functor (A : StringConvertArg) -> @@ -161,10 +161,10 @@ sig val compare : t -> t -> int val encode : reference -> t val subst : substitution -> t -> t - val printer : t -> std_ppcmds + val printer : t -> Pp.t val key : option_name val title : string - val member_message : t -> bool -> std_ppcmds + val member_message : t -> bool -> Pp.t end module RefConvert = functor (A : RefConvertArg) -> diff --git a/library/goptions.mli b/library/goptions.mli index f612c4e369..cec7250f1f 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -43,7 +43,6 @@ All options are synchronized with the document. *) -open Pp open Libnames open Mod_subst @@ -64,7 +63,7 @@ module MakeStringTable : (A : sig val key : option_name val title : string - val member_message : string -> bool -> std_ppcmds + val member_message : string -> bool -> Pp.t end) -> sig val active : string -> bool @@ -88,10 +87,10 @@ module MakeRefTable : val compare : t -> t -> int val encode : reference -> t val subst : substitution -> t -> t - val printer : t -> std_ppcmds + val printer : t -> Pp.t val key : option_name val title : string - val member_message : t -> bool -> std_ppcmds + val member_message : t -> bool -> Pp.t end) -> sig val active : A.t -> bool @@ -177,6 +176,6 @@ type option_state = { } val get_tables : unit -> option_state OptionMap.t -val print_tables : unit -> std_ppcmds +val print_tables : unit -> Pp.t val error_undeclared_key : option_name -> 'a diff --git a/library/heads.ml b/library/heads.ml index 6aee63c744..c12fa94791 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -128,11 +128,11 @@ let compute_head = function let is_Def = function Declarations.Def _ -> true | _ -> false in let body = if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body - then Declareops.body_of_constant (Environ.opaque_tables env) cb else None + then Global.body_of_constant cst else None in (match body with | None -> RigidHead (RigidParameter cst) - | Some c -> kind_of_head env c) + | Some (c, _) -> kind_of_head env c) | EvalVarRef id -> (match Global.lookup_named id with | LocalDef (_,c,_) when not (Decls.variable_opacity id) -> diff --git a/library/heads.mli b/library/heads.mli index 5acf5f54f7..1ce66c841e 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 deleted file mode 100644 index 8f3bfc17e4..0000000000 --- a/library/impargs.ml +++ /dev/null @@ -1,736 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <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 CErrors -open Util -open Names -open Globnames -open Nameops -open Term -open Reduction -open Declarations -open Environ -open Libobject -open Lib -open Pp -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 *) - -type implicits_flags = { - auto : bool; (* automatic or manual only *) - strict : bool; (* true = strict *) - strongly_strict : bool; (* true = strongly strict *) - reversible_pattern : bool; - contextual : bool; (* true = contextual *) - maximal : bool -} - -let implicit_args = ref { - auto = false; - strict = true; - strongly_strict = false; - reversible_pattern = false; - contextual = false; - maximal = false; -} - -let make_implicit_args flag = - implicit_args := { !implicit_args with auto = flag } - -let make_strict_implicit_args flag = - implicit_args := { !implicit_args with strict = flag } - -let make_strongly_strict_implicit_args flag = - implicit_args := { !implicit_args with strongly_strict = flag } - -let make_reversible_pattern_implicit_args flag = - implicit_args := { !implicit_args with reversible_pattern = flag } - -let make_contextual_implicit_args flag = - implicit_args := { !implicit_args with contextual = flag } - -let make_maximal_implicit_args flag = - implicit_args := { !implicit_args with maximal = flag } - -let is_implicit_args () = !implicit_args.auto -let is_strict_implicit_args () = !implicit_args.strict -let is_strongly_strict_implicit_args () = !implicit_args.strongly_strict -let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern -let is_contextual_implicit_args () = !implicit_args.contextual -let is_maximal_implicit_args () = !implicit_args.maximal - -let with_implicit_protection f x = - let oflags = !implicit_args in - try - let rslt = f x in - implicit_args := oflags; - rslt - with reraise -> - let reraise = CErrors.push reraise in - let () = implicit_args := oflags in - iraise reraise - -let set_maximality imps b = - (* Force maximal insertion on ending implicits (compatibility) *) - let is_set x = match x with None -> false | _ -> true in - b || List.for_all is_set imps - -(*s Computation of implicit arguments *) - -(* We remember various information about why an argument is - inferable as implicit - -- [DepRigid] means that the implicit argument can be found by - unification along a rigid path (we do not print the arguments of - this kind if there is enough arguments to infer them) - -- [DepFlex] means that the implicit argument can be found by unification - along a collapsable path only (e.g. as x in (P x) where P is another - argument) (we do (defensively) print the arguments of this kind) - -- [DepFlexAndRigid] means that the least argument from which the - implicit argument can be inferred is following a collapsable path - but there is a greater argument from where the implicit argument is - inferable following a rigid path (useful to know how to print a - partial application) - -- [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. -*) - -type argument_position = - | Conclusion - | Hyp of int - -let argument_position_eq p1 p2 = match p1, p2 with -| Conclusion, Conclusion -> true -| Hyp h1, Hyp h2 -> Int.equal h1 h2 -| _ -> false - -let explicitation_eq ex1 ex2 = match ex1, ex2 with -| ExplByPos (i1, id1), ExplByPos (i2, id2) -> - Int.equal i1 i2 && Option.equal Id.equal id1 id2 -| ExplByName id1, ExplByName id2 -> - Id.equal id1 id2 -| _ -> false - -type implicit_explanation = - | DepRigid of argument_position - | DepFlex of argument_position - | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position - | Manual - -let argument_less = function - | Hyp n, Hyp n' -> n<n' - | Hyp _, Conclusion -> true - | Conclusion, _ -> false - -let update pos rig (na,st) = - let e = - if rig then - match st with - | None -> DepRigid pos - | Some (DepRigid n as x) -> - if argument_less (pos,n) then DepRigid pos else x - | Some (DepFlexAndRigid (fpos,rpos) as x) -> - if argument_less (pos,fpos) || argument_position_eq pos fpos then DepRigid pos else - if argument_less (pos,rpos) then DepFlexAndRigid (fpos,pos) else x - | Some (DepFlex fpos) -> - if argument_less (pos,fpos) || argument_position_eq pos fpos then DepRigid pos - else DepFlexAndRigid (fpos,pos) - | Some Manual -> assert false - else - match st with - | None -> DepFlex pos - | Some (DepRigid rpos as x) -> - if argument_less (pos,rpos) then DepFlexAndRigid (pos,rpos) else x - | Some (DepFlexAndRigid (fpos,rpos) as x) -> - if argument_less (pos,fpos) then DepFlexAndRigid (pos,rpos) else x - | Some (DepFlex fpos as x) -> - if argument_less (pos,fpos) then DepFlex pos else x - | Some Manual -> assert false - in na, Some e - -(* modified is_rigid_reference with a truncated env *) -let is_flexible_reference env bound depth f = - match kind_of_term f with - | Rel n when n >= bound+depth -> (* inductive type *) false - | Rel n when n >= depth -> (* previous argument *) true - | Rel n -> (* since local definitions have been expanded *) false - | Const (kn,_) -> - let cb = Environ.lookup_constant kn env in - (match cb.const_body with Def _ -> true | _ -> false) - | Var id -> - env |> Environ.lookup_named id |> is_local_def - | Ind _ | Construct _ -> false - | _ -> true - -let push_lift d (e,n) = (push_rel d e,n+1) - -let is_reversible_pattern bound depth f l = - isRel f && let n = destRel f in (n < bound+depth) && (n >= depth) && - Array.for_all (fun c -> isRel c && destRel c < depth) l && - Array.distinct 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_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) -> - let i = bound + depth - n - 1 in - acc.(i) <- update pos rig acc.(i) - | App (f,l) when revpat && is_reversible_pattern bound depth f l -> - let i = bound + depth - destRel f - 1 in - acc.(i) <- update pos rig acc.(i) - | App (f,_) when rig && is_flexible_reference env bound depth f -> - if strict then () else - iter_constr_with_full_binders push_lift (frec false) ed c - | Proj (p,c) when rig -> - if strict then () else - iter_constr_with_full_binders push_lift (frec false) ed c - | Case _ when rig -> - if strict then () else - iter_constr_with_full_binders push_lift (frec false) ed c - | Evar _ -> () - | _ -> - iter_constr_with_full_binders push_lift (frec rig) ed c - in - let () = if not (Vars.noccur_between 1 bound m) then frec true (env,1) m in - acc - -let rec is_rigid_head t = match kind_of_term t with - | Rel _ | Evar _ -> false - | Ind _ | Const _ | Var _ | Sort _ -> true - | Case (_,_,f,_) -> is_rigid_head f - | Proj (p,c) -> true - | App (f,args) -> - (match kind_of_term f with - | Fix ((fi,i),_) -> is_rigid_head (args.(fi.(i))) - | _ -> is_rigid_head f) - | Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _ - | Prod _ | Meta _ | Cast _ -> assert false - -(* calcule la liste des arguments implicites *) - -let find_displayed_name_in all avoid na (env, b) = - let b = EConstr.of_constr b in - let envnames_b = (env, b) in - let flag = RenamingElsewhereFor envnames_b in - if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b - else compute_displayed_name_in Evd.empty flag avoid na 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_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 (LocalAssum (na',a)) env) avoid' (n+1) (na'::names) b) - | _ -> - rigid := is_rigid_head t; - let names = List.rev names in - let v = Array.map (fun na -> na,None) (Array.of_list names) in - if contextual then - add_free_rels_until strict strongly_strict revpat n env t Conclusion v - else v - in - 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 (LocalAssum (na',a)) env) avoid 1 [na'] b in - !rigid, Array.to_list v - | _ -> true, [] - -let compute_implicits_flags env f all t = - compute_implicits_gen - (f.strict || f.strongly_strict) f.strongly_strict - f.reversible_pattern f.contextual all env t - -let compute_auto_implicits env flags enriching t = - if enriching then compute_implicits_flags env flags true t - else compute_implicits_gen false false false true true env t - -let compute_implicits_names env t = - let _, impls = compute_implicits_gen false false false false true env t in - List.map fst impls - -(* Extra information about implicit arguments *) - -type maximal_insertion = bool (* true = maximal contextual insertion *) -type force_inference = bool (* true = always infer, never turn into evar/subgoal *) - -type implicit_status = - (* None = Not implicit *) - (Id.t * implicit_explanation * (maximal_insertion * force_inference)) option - -type implicit_side_condition = DefaultImpArgs | LessArgsThan of int - -type implicits_list = implicit_side_condition * implicit_status list - -let is_status_implicit = function - | None -> false - | _ -> true - -let name_of_implicit = function - | None -> anomaly (Pp.str "Not an implicit argument.") - | Some (id,_,_) -> id - -let maximal_insertion_of = function - | Some (_,_,(b,_)) -> b - | None -> anomaly (Pp.str "Not an implicit argument.") - -let force_inference_of = function - | Some (_, _, (_, b)) -> b - | None -> anomaly (Pp.str "Not an implicit argument.") - -(* [in_ctx] means we know the expected type, [n] is the index of the argument *) -let is_inferable_implicit in_ctx n = function - | None -> false - | Some (_,DepRigid (Hyp p),_) -> in_ctx || n >= p - | Some (_,DepFlex (Hyp p),_) -> false - | Some (_,DepFlexAndRigid (_,Hyp q),_) -> in_ctx || n >= q - | Some (_,DepRigid Conclusion,_) -> in_ctx - | Some (_,DepFlex Conclusion,_) -> false - | Some (_,DepFlexAndRigid (_,Conclusion),_) -> in_ctx - | Some (_,Manual,_) -> true - -let positions_of_implicits (_,impls) = - let rec aux n = function - [] -> [] - | Some _ :: l -> n :: aux (n+1) l - | None :: l -> aux (n+1) l - in aux 1 impls - -(* Manage user-given implicit arguments *) - -let rec prepare_implicits f = function - | [] -> [] - | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.") - | (Name id, Some imp)::imps -> - let imps' = prepare_implicits f imps in - Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps' - | _::imps -> None :: prepare_implicits f imps - -let set_implicit id imp insmax = - (id,(match imp with None -> Manual | Some imp -> imp),insmax) - -let rec assoc_by_pos k = function - (ExplByPos (k', x), b) :: tl when Int.equal k k' -> (x,b), tl - | hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl - | [] -> raise Not_found - -let check_correct_manual_implicits autoimps l = - List.iter (function - | ExplByName id,(b,fi,forced) -> - if not forced then - 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 - user_err - (str "Bad implicit argument number: " ++ int i ++ str ".") - else - user_err - (str "Cannot set implicit argument number " ++ int i ++ - str ": it has no name.")) l - -let set_manual_implicits env flags enriching autoimps l = - let try_forced k l = - try - let (id, (b, fi, fo)), l' = assoc_by_pos k l in - if fo then - let id = match id with Some id -> id | None -> Id.of_string ("arg_" ^ string_of_int k) in - l', Some (id,Manual,(b,fi)) - else l, None - with Not_found -> l, None - in - if not (List.distinct l) then - user_err Pp.(str "Some parameters are referred more than once."); - (* Compare with automatic implicits to recover printing data and names *) - let rec merge k l = function - | (Name id,imp)::imps -> - let l',imp,m = - try - let eq = explicitation_eq in - let (b, fi, fo) = List.assoc_f eq (ExplByName id) l in - List.remove_assoc_f eq (ExplByName id) l, (Some Manual), (Some (b, fi)) - with Not_found -> - try - let (id, (b, fi, fo)), l' = assoc_by_pos k l in - l', (Some Manual), (Some (b,fi)) - with Not_found -> - let m = match enriching, imp with - | true, Some _ -> Some (flags.maximal, true) - | _ -> None - in - l, imp, m - in - let imps' = merge (k+1) l' imps in - let m = Option.map (fun (b,f) -> - (* match imp with Some Manual -> (b,f) *) - (* | _ -> *)set_maximality imps' b, f) m in - Option.map (set_implicit id imp) m :: imps' - | (Anonymous,imp)::imps -> - let l', forced = try_forced k l in - forced :: merge (k+1) l' imps - | [] when begin match l with [] -> true | _ -> false end -> [] - | [] -> - check_correct_manual_implicits autoimps l; - [] - in - merge 1 l autoimps - -let compute_semi_auto_implicits env f manual t = - match manual with - | [] -> - if not f.auto then [DefaultImpArgs, []] - else let _,l = compute_implicits_flags env f false t in - [DefaultImpArgs, prepare_implicits f l] - | _ -> - let _,autoimpls = compute_auto_implicits env f f.auto t in - [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual] - -(*s Constants. *) - -let compute_constant_implicits flags manual cst = - let env = Global.env () in - let cb = Environ.lookup_constant cst env in - let ty = Typeops.type_of_constant_type env cb.const_type in - let impls = compute_semi_auto_implicits env flags manual ty in - impls - -(*s Inductives and constructors. Their implicit arguments are stored - in an array, indexed by the inductive number, of pairs $(i,v)$ where - $i$ are the implicit arguments of the inductive and $v$ the array of - implicit arguments of the constructors. *) - -let compute_mib_implicits flags manual kn = - let env = Global.env () in - let mib = lookup_mind kn env in - let ar = - Array.to_list - (Array.mapi (* No need to lift, arities contain no de Bruijn *) - (fun i mip -> - (** No need to care about constraints here *) - 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 = - let ind = (kn,i) in - let ar = Global.type_of_global_unsafe (IndRef ind) in - ((IndRef ind,compute_semi_auto_implicits env flags manual ar), - Array.mapi (fun j c -> - (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar flags manual c)) - mip.mind_nf_lc) - in - Array.mapi imps_one_inductive mib.mind_packets - -let compute_all_mib_implicits flags manual kn = - let imps = compute_mib_implicits flags manual kn in - List.flatten - (Array.map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps) - -(*s Variables. *) - -let compute_var_implicits flags manual id = - let env = Global.env () in - compute_semi_auto_implicits env flags manual (NamedDecl.get_type (lookup_named id env)) - -(* Implicits of a global reference. *) - -let compute_global_implicits flags manual = function - | VarRef id -> compute_var_implicits flags manual id - | ConstRef kn -> compute_constant_implicits flags manual kn - | IndRef (kn,i) -> - let ((_,imps),_) = (compute_mib_implicits flags manual kn).(i) in imps - | ConstructRef ((kn,i),j) -> - let (_,cimps) = (compute_mib_implicits flags manual kn).(i) in snd cimps.(j-1) - -(* Merge a manual explicitation with an implicit_status list *) - -let merge_impls (cond,oldimpls) (_,newimpls) = - let oldimpls,usersuffiximpls = List.chop (List.length newimpls) oldimpls in - cond, (List.map2 (fun orig ni -> - match orig with - | Some (_, Manual, _) -> orig - | _ -> ni) oldimpls newimpls)@usersuffiximpls - -(* Caching implicits *) - -type implicit_interactive_request = - | ImplAuto - | ImplManual of int - -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 - -let implicits_table = Summary.ref Refmap.empty ~name:"implicits" - -let implicits_of_global ref = - try - let l = Refmap.find ref !implicits_table in - try - let rename_l = Arguments_renaming.arguments_names ref in - 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 - with Not_found -> [DefaultImpArgs,[]] - -let cache_implicits_decl (ref,imps) = - implicits_table := Refmap.add ref imps !implicits_table - -let load_implicits _ (_,(_,l)) = List.iter cache_implicits_decl l - -let cache_implicits o = - load_implicits 1 o - -let subst_implicits_decl subst (r,imps as o) = - let r' = fst (subst_global subst r) in if r==r' then o else (r',imps) - -let subst_implicits (subst,(req,l)) = - (ImplLocal,List.smartmap (subst_implicits_decl subst) l) - -let impls_of_context ctx = - let map (decl, impl) = match impl with - | Implicit -> Some (NamedDecl.get_id decl, Manual, (true, true)) - | _ -> None - in - List.rev_map map (List.filter (fst %> is_local_assum) ctx) - -let adjust_side_condition p = function - | LessArgsThan n -> LessArgsThan (n+p) - | DefaultImpArgs -> DefaultImpArgs - -let add_section_impls vars extra_impls (cond,impls) = - let p = List.length vars - List.length extra_impls in - adjust_side_condition p cond, extra_impls @ impls - -let discharge_implicits (_,(req,l)) = - match req with - | ImplLocal -> None - | ImplInteractive (ref,flags,exp) -> - (try - 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 - Some (ImplInteractive (ref',flags,exp),l') - with Not_found -> (* ref not defined in this section *) Some (req,l)) - | ImplConstant (con,flags) -> - (try - let con' = pop_con con in - let vars,_,_ = section_segment_of_constant con in - let extra_impls = impls_of_context vars in - let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in - let l' = [ConstRef con',newimpls] in - Some (ImplConstant (con',flags),l') - with Not_found -> (* con not defined in this section *) Some (req,l)) - | ImplMutualInductive (kn,flags) -> - (try - let l' = List.map (fun (gr, l) -> - 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 - in - Some (ImplMutualInductive (pop_kn kn,flags),l') - with Not_found -> (* ref not defined in this section *) Some (req,l)) - -let rebuild_implicits (req,l) = - match req with - | ImplLocal -> assert false - | ImplConstant (con,flags) -> - let oldimpls = snd (List.hd l) in - let newimpls = compute_constant_implicits flags [] con in - req, [ConstRef con, List.map2 merge_impls oldimpls newimpls] - | ImplMutualInductive (kn,flags) -> - let newimpls = compute_all_mib_implicits flags [] kn in - let rec aux olds news = - match olds, news with - | (_, oldimpls) :: old, (gr, newimpls) :: tl -> - (gr, List.map2 merge_impls oldimpls newimpls) :: aux old tl - | [], [] -> [] - | _, _ -> assert false - in req, aux l newimpls - - | ImplInteractive (ref,flags,o) -> - (if isVarRef ref && is_in_section ref then ImplLocal else req), - match o with - | ImplAuto -> - let oldimpls = snd (List.hd l) in - let newimpls = compute_global_implicits flags [] ref in - [ref,List.map2 merge_impls oldimpls newimpls] - | ImplManual userimplsize -> - let oldimpls = snd (List.hd l) in - if flags.auto then - let newimpls = List.hd (compute_global_implicits flags [] ref) in - let p = List.length (snd newimpls) - userimplsize in - let newimpls = on_snd (List.firstn p) newimpls in - [ref,List.map (fun o -> merge_impls o newimpls) oldimpls] - else - [ref,oldimpls] - -let classify_implicits (req,_ as obj) = match req with -| ImplLocal -> Dispose -| _ -> Substitute obj - -type implicits_obj = - implicit_discharge_request * - (global_reference * implicits_list list) list - -let inImplicits : implicits_obj -> obj = - declare_object {(default_object "IMPLICITS") with - cache_function = cache_implicits; - load_function = load_implicits; - subst_function = subst_implicits; - classify_function = classify_implicits; - discharge_function = discharge_implicits; - rebuild_function = rebuild_implicits } - -let is_local local ref = local || isVarRef ref && is_in_section ref - -let declare_implicits_gen req flags ref = - let imps = compute_global_implicits flags [] ref in - add_anonymous_leaf (inImplicits (req,[ref,imps])) - -let declare_implicits local ref = - let flags = { !implicit_args with auto = true } in - let req = - if is_local local ref then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in - declare_implicits_gen req flags ref - -let declare_var_implicits id = - let flags = !implicit_args in - declare_implicits_gen ImplLocal flags (VarRef id) - -let declare_constant_implicits con = - let flags = !implicit_args in - declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con) - -let declare_mib_implicits kn = - let flags = !implicit_args in - let imps = Array.map_to_list - (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) - (compute_mib_implicits flags [] kn) in - add_anonymous_leaf - (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps)) - -(* Declare manual implicits *) -type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool) - -type manual_implicits = manual_explicitation list - -let compute_implicits_with_manual env typ enriching l = - let _,autoimpls = compute_auto_implicits env !implicit_args enriching typ in - set_manual_implicits env !implicit_args enriching autoimpls l - -let check_inclusion l = - (* Check strict inclusion *) - let rec aux = function - | n1::(n2::_ as nl) -> - if n1 <= n2 then - user_err Pp.(str "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 - 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 - CList.skipn_at_least pb.Declarations.proj_npars impls - -let declare_manual_implicits local ref ?enriching l = - let flags = !implicit_args in - let env = Global.env () in - let t = Global.type_of_global_unsafe ref in - let enriching = Option.default flags.auto enriching in - let isrigid,autoimpls = compute_auto_implicits env flags enriching t in - let l' = match l with - | [] -> assert false - | [l] -> - [DefaultImpArgs, set_manual_implicits env flags enriching autoimpls l] - | _ -> - check_rigidity isrigid; - let l = List.map (fun imps -> (imps,List.length imps)) l in - let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in - check_inclusion l; - let nargs = List.length autoimpls in - List.map (fun (imps,n) -> - (LessArgsThan (nargs-n), - set_manual_implicits env flags enriching autoimpls imps)) l in - let req = - if is_local local ref then ImplLocal - else ImplInteractive(ref,flags,ImplManual (List.length autoimpls)) - in - add_anonymous_leaf (inImplicits (req,[ref,l'])) - -let maybe_declare_manual_implicits local ref ?enriching l = - match l with - | [] -> () - | _ -> declare_manual_implicits local ref ?enriching [l] - -let extract_impargs_data impls = - let rec aux p = function - | (DefaultImpArgs, imps)::_ -> [None,imps] - | (LessArgsThan n, imps)::l -> (Some (p,n),imps) :: aux (n+1) l - | [] -> [] in - aux 0 impls - -let lift_implicits n = - List.map (fun x -> - match fst x with - ExplByPos (k, id) -> ExplByPos (k + n, id), snd x - | _ -> x) - -let make_implicits_list l = [DefaultImpArgs, l] - -let rec drop_first_implicits p l = - if Int.equal p 0 then l else match l with - | _,[] as x -> x - | DefaultImpArgs,imp::impls -> - drop_first_implicits (p-1) (DefaultImpArgs,impls) - | LessArgsThan n,imp::impls -> - let n = if is_status_implicit imp then n-1 else n in - drop_first_implicits (p-1) (LessArgsThan n,impls) - -let rec select_impargs_size n = function - | [] -> [] (* Tolerance for (DefaultImpArgs,[]) *) - | [_, impls] | (DefaultImpArgs, impls)::_ -> impls - | (LessArgsThan p, impls)::l -> - if n <= p then impls else select_impargs_size n l - -let select_stronger_impargs = function - | [] -> [] (* Tolerance for (DefaultImpArgs,[]) *) - | (_,impls)::_ -> impls diff --git a/library/impargs.mli b/library/impargs.mli deleted file mode 100644 index 3919a519c9..0000000000 --- a/library/impargs.mli +++ /dev/null @@ -1,139 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <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 Names -open Globnames -open Term -open Environ - -(** {6 Implicit Arguments } *) -(** Here we store the implicit arguments. Notice that we - are outside the kernel, which knows nothing about implicit arguments. *) - -val make_implicit_args : bool -> unit -val make_strict_implicit_args : bool -> unit -val make_strongly_strict_implicit_args : bool -> unit -val make_reversible_pattern_implicit_args : bool -> unit -val make_contextual_implicit_args : bool -> unit -val make_maximal_implicit_args : bool -> unit - -val is_implicit_args : unit -> bool -val is_strict_implicit_args : unit -> bool -val is_strongly_strict_implicit_args : unit -> bool -val is_reversible_pattern_implicit_args : unit -> bool -val is_contextual_implicit_args : unit -> bool -val is_maximal_implicit_args : unit -> bool - -val with_implicit_protection : ('a -> 'b) -> 'a -> 'b - -(** {6 ... } *) -(** An [implicits_list] is a list of positions telling which arguments - of a reference can be automatically infered *) - - -type argument_position = - | Conclusion - | Hyp of int - -(** We remember various information about why an argument is - inferable as implicit *) -type implicit_explanation = - | DepRigid of argument_position - (** means that the implicit argument can be found by - unification along a rigid path (we do not print the arguments of - this kind if there is enough arguments to infer them) *) - | DepFlex of argument_position - (** means that the implicit argument can be found by unification - along a collapsable path only (e.g. as x in (P x) where P is another - argument) (we do (defensively) print the arguments of this kind) *) - | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position - (** means that the least argument from which the - implicit argument can be inferred is following a collapsable path - but there is a greater argument from where the implicit argument is - inferable following a rigid path (useful to know how to print a - partial application) *) - | 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. *) - -type maximal_insertion = bool (** true = maximal contextual insertion *) -type force_inference = bool (** true = always infer, never turn into evar/subgoal *) - -type implicit_status = (Id.t * implicit_explanation * - (maximal_insertion * force_inference)) option - (** [None] = Not implicit *) - -type implicit_side_condition - -type implicits_list = implicit_side_condition * implicit_status list - -val is_status_implicit : implicit_status -> bool -val is_inferable_implicit : bool -> int -> implicit_status -> bool -val name_of_implicit : implicit_status -> Id.t -val maximal_insertion_of : implicit_status -> bool -val force_inference_of : implicit_status -> bool - -val positions_of_implicits : implicits_list -> int list - -(** A [manual_explicitation] is a tuple of a positional or named explicitation with - maximal insertion, force inference and force usage flags. Forcing usage makes - the argument implicit even if the automatic inference considers it not inferable. *) -type manual_explicitation = Constrexpr.explicitation * - (maximal_insertion * force_inference * bool) - -type manual_implicits = manual_explicitation list - -val compute_implicits_with_manual : env -> types -> bool -> - manual_implicits -> implicit_status list - -val compute_implicits_names : env -> types -> Name.t list - -(** {6 Computation of implicits (done using the global environment). } *) - -val declare_var_implicits : variable -> unit -val declare_constant_implicits : constant -> unit -val declare_mib_implicits : mutual_inductive -> unit - -val declare_implicits : bool -> global_reference -> unit - -(** [declare_manual_implicits local ref enriching l] - Manual declaration of which arguments are expected implicit. - If not set, we decide if it should enrich by automatically inferd - implicits depending on the current state. - Unsets implicits if [l] is empty. *) - -val declare_manual_implicits : bool -> global_reference -> ?enriching:bool -> - manual_implicits list -> unit - -(** If the list is empty, do nothing, otherwise declare the implicits. *) - -val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool -> - manual_implicits -> unit - -val implicits_of_global : global_reference -> implicits_list list - -val extract_impargs_data : - implicits_list list -> ((int * int) option * implicit_status list) list - -val lift_implicits : int -> manual_implicits -> manual_implicits - -val make_implicits_list : implicit_status list -> implicits_list list - -val drop_first_implicits : int -> implicits_list -> implicits_list - -val projection_implicits : env -> projection -> implicit_status list -> - implicit_status list - -val select_impargs_size : int -> implicits_list list -> implicit_status list - -val select_stronger_impargs : implicits_list list -> implicit_status list - -val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool -(** Equality on [explicitation]. *) diff --git a/library/keys.ml b/library/keys.ml index c9e325ee57..be53aabaa4 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/keys.mli b/library/keys.mli index 6abac4de44..d5dc0e2a1f 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -19,5 +19,5 @@ val equiv_keys : key -> key -> bool val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option (** Compute the head key of a term. *) -val pr_keys : (global_reference -> Pp.std_ppcmds) -> Pp.std_ppcmds +val pr_keys : (global_reference -> Pp.t) -> Pp.t (** Pretty-print the mapping *) diff --git a/library/kindops.ml b/library/kindops.ml index 623d2537aa..882f620862 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/kindops.mli b/library/kindops.mli index 3e95eaa7d9..77979c9159 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 8127316d73..a24d20c681 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -465,9 +465,10 @@ let add_section_replacement f g poly hyps = let () = check_same_poly poly vars in let sechyps,ctx = extract_hyps (vars,hyps) in let ctx = Univ.ContextSet.to_context ctx in + let inst = Univ.UContext.instance ctx in let subst, ctx = Univ.abstract_universes ctx in let args = instance_from_variable_context (List.rev sechyps) in - sectab := (vars,f (Univ.AUContext.instance ctx,args) exps, + sectab := (vars,f (inst,args) exps, g (sechyps,subst,ctx) abs)::sl let add_section_kn poly kn = @@ -644,3 +645,16 @@ let discharge_con cst = let discharge_inductive (kn,i) = (discharge_kn kn,i) + +let discharge_abstract_universe_context (_, subst, abs_ctx) auctx = + let open Univ in + let len = LMap.cardinal subst in + let rec gen_subst i acc = + if i < 0 then acc + else + let acc = LMap.add (Level.var i) (Level.var (i + len)) acc in + gen_subst (pred i) acc + in + let subst = gen_subst (AUContext.size auctx - 1) subst in + let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in + subst, AUContext.union abs_ctx auctx diff --git a/library/lib.mli b/library/lib.mli index 284d339801..f1c9bfca24 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -183,3 +183,5 @@ 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 +val discharge_abstract_universe_context : + abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t diff --git a/library/libnames.ml b/library/libnames.ml index 50f28b0205..0453f15e87 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/libnames.mli b/library/libnames.mli index 57013ef82e..1b351290a4 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -1,20 +1,19 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Util -open Pp open Loc open Names (** {6 Dirpaths } *) (** FIXME: ought to be in Names.dir_path *) -val pr_dirpath : DirPath.t -> Pp.std_ppcmds +val pr_dirpath : DirPath.t -> Pp.t val dirpath_of_string : string -> DirPath.t val string_of_dirpath : DirPath.t -> string @@ -58,7 +57,7 @@ val basename : full_path -> Id.t (** Parsing and printing of section path as ["coq_root.module.id"] *) val path_of_string : string -> full_path val string_of_path : full_path -> string -val pr_path : full_path -> std_ppcmds +val pr_path : full_path -> Pp.t module Spmap : CSig.MapS with type key = full_path @@ -77,7 +76,7 @@ val repr_qualid : qualid -> DirPath.t * Id.t val qualid_eq : qualid -> qualid -> bool -val pr_qualid : qualid -> std_ppcmds +val pr_qualid : qualid -> Pp.t val string_of_qualid : qualid -> string val qualid_of_string : string -> qualid @@ -124,7 +123,7 @@ type reference = val eq_reference : reference -> reference -> bool val qualid_of_reference : reference -> qualid located val string_of_reference : reference -> string -val pr_reference : reference -> std_ppcmds +val pr_reference : reference -> Pp.t val loc_of_reference : reference -> Loc.t option val join_reference : reference -> reference -> reference diff --git a/library/libobject.ml b/library/libobject.ml index 897591762c..013c6fa0a5 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/libobject.mli b/library/libobject.mli index 51b9af059f..6f935bffea 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -56,6 +56,9 @@ open Mod_subst rebuild the non volatile content of a section from the data collected by the discharge function + Any type defined as a persistent object must be pure (e.g. no references) and + marshallable by the OCaml Marshal module (e.g. no closures). + *) type 'a substitutivity = diff --git a/library/library.ml b/library/library.ml index db05ad2b7b..20ecc2c229 100644 --- a/library/library.ml +++ b/library/library.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/library.mli b/library/library.mli index b9044b60dd..604167804d 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/loadpath.ml b/library/loadpath.ml index ad429ea840..757e972b1a 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/loadpath.mli b/library/loadpath.mli index 4e79edbdcf..26ed30674a 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/nameops.ml b/library/nameops.ml index 0b5dfd8d0e..adfe6f5a5d 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/nameops.mli b/library/nameops.mli index abfc09db8d..89aba24476 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -106,13 +106,13 @@ val name_max : Name.t -> Name.t -> Name.t val name_cons : Name.t -> Id.t list -> Id.t list (** @deprecated Same as [Name.cons] *) -val pr_name : Name.t -> Pp.std_ppcmds +val pr_name : Name.t -> Pp.t (** @deprecated Same as [Name.print] *) -val pr_id : Id.t -> Pp.std_ppcmds +val pr_id : Id.t -> Pp.t (** @deprecated Same as [Names.Id.print] *) -val pr_lab : Label.t -> Pp.std_ppcmds +val pr_lab : Label.t -> Pp.t (** some preset paths *) @@ -127,5 +127,5 @@ val coq_string : string (** "Coq" *) val default_root_prefix : DirPath.t (** Metavariables *) -val pr_meta : Term.metavariable -> Pp.std_ppcmds +val pr_meta : Term.metavariable -> Pp.t val string_of_meta : Term.metavariable -> string diff --git a/library/nametab.ml b/library/nametab.ml index 93e9c03cee..68fdbb4f38 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/nametab.mli b/library/nametab.mli index 095ac4f9df..025a63b1ce 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Libnames open Globnames @@ -155,7 +154,7 @@ val basename_of_global : global_reference -> Id.t (** Printing of global references using names as short as possible. @raise Not_found when the reference is not in the global tables. *) -val pr_global_env : Id.Set.t -> global_reference -> std_ppcmds +val pr_global_env : Id.Set.t -> global_reference -> Pp.t (** The [shortest_qualid] functions given an object with [user_name] diff --git a/library/states.ml b/library/states.ml index 95bd819d66..03e4610a6d 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/states.mli b/library/states.mli index 12c71c9991..780a4e8dc8 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/summary.ml b/library/summary.ml index c7bf95fd41..69eff830da 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/summary.mli b/library/summary.mli index 1b57613cb7..d093d95f29 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -14,6 +14,8 @@ type marshallable = | `No (* Full data will be store in memory, e.g. for Undo *) | `Shallow ] (* Only part of the data will be marshalled to a slave process *) +(** Types of global Coq states. The ['a] type should be pure and marshallable by + the standard OCaml marshalling function. *) type 'a summary_declaration = { (** freeze_function [true] is for marshalling to disk. * e.g. lazy must be forced *) diff --git a/library/univops.ml b/library/univops.ml index 60c12f0d81..3bafb824d1 100644 --- a/library/univops.ml +++ b/library/univops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,6 @@ open Term open Univ -open Declarations let universes_of_constr c = let rec aux s c = @@ -21,44 +20,6 @@ let universes_of_constr c = | _ -> fold_constr aux s c in aux LSet.empty c -let universes_of_inductive mind = - let process auctx = - let u = Univ.AUContext.instance auctx in - let univ_of_one_ind oind = - let arity_univs = - Context.Rel.fold_outside - (fun decl unvs -> - Univ.LSet.union - (Context.Rel.Declaration.fold_constr - (fun cnstr unvs -> - let cnstr = Vars.subst_instance_constr u cnstr in - Univ.LSet.union - (universes_of_constr cnstr) unvs) - decl Univ.LSet.empty) unvs) - oind.mind_arity_ctxt ~init:Univ.LSet.empty - in - Array.fold_left (fun unvs cns -> - let cns = Vars.subst_instance_constr u cns in - Univ.LSet.union (universes_of_constr cns) unvs) arity_univs - oind.mind_nf_lc - in - let univs = - Array.fold_left - (fun unvs pk -> - Univ.LSet.union - (univ_of_one_ind pk) unvs - ) - Univ.LSet.empty mind.mind_packets - in - let mindcnt = Univ.UContext.constraints (Univ.instantiate_univ_context auctx) in - let univs = Univ.LSet.union univs (Univ.universes_of_constraints mindcnt) in - univs - in - match mind.mind_universes with - | Monomorphic_ind _ -> LSet.empty - | Polymorphic_ind auctx -> process auctx - | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi) - 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. *) diff --git a/library/univops.mli b/library/univops.mli index 5b499c75bc..09147cb41c 100644 --- a/library/univops.mli +++ b/library/univops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,10 +8,8 @@ open Term open Univ -open Declarations (** Shrink a universe context to a restricted set of variables *) val universes_of_constr : constr -> universe_set -val universes_of_inductive : mutual_inductive_body -> universe_set val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set |