From 9051c1618062ce014719de5c3f73832e9a282a4d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 13 Jul 2017 19:53:54 +0200 Subject: [general] Move files to directories matching linking order. We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`, `Miscprint`) to their proper place as they were declared in different `mllib` files than the one in their directory. In some cases this could be refined but we don't do anything fancy, we just reflect the status quo. --- interp/declare.ml | 564 +++++++++++++++++++++++++++++++++++++ interp/declare.mli | 97 +++++++ interp/impargs.ml | 737 +++++++++++++++++++++++++++++++++++++++++++++++++ interp/impargs.mli | 139 ++++++++++ library/declare.ml | 564 ------------------------------------- library/declare.mli | 97 ------- library/impargs.ml | 737 ------------------------------------------------- library/impargs.mli | 139 ---------- printing/miscprint.ml | 74 ----- printing/miscprint.mli | 37 --- proofs/miscprint.ml | 74 +++++ proofs/miscprint.mli | 37 +++ tactics/ind_tables.ml | 203 ++++++++++++++ tactics/ind_tables.mli | 51 ++++ vernac/ind_tables.ml | 203 -------------- vernac/ind_tables.mli | 51 ---- 16 files changed, 1902 insertions(+), 1902 deletions(-) create mode 100644 interp/declare.ml create mode 100644 interp/declare.mli create mode 100644 interp/impargs.ml create mode 100644 interp/impargs.mli delete mode 100644 library/declare.ml delete mode 100644 library/declare.mli delete mode 100644 library/impargs.ml delete mode 100644 library/impargs.mli delete mode 100644 printing/miscprint.ml delete mode 100644 printing/miscprint.mli create mode 100644 proofs/miscprint.ml create mode 100644 proofs/miscprint.mli create mode 100644 tactics/ind_tables.ml create mode 100644 tactics/ind_tables.mli delete mode 100644 vernac/ind_tables.ml delete mode 100644 vernac/ind_tables.mli diff --git a/interp/declare.ml b/interp/declare.ml new file mode 100644 index 0000000000..154793a32d --- /dev/null +++ b/interp/declare.ml @@ -0,0 +1,564 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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, _, _ as info = section_segment_of_mutual_inductive mind in + Some (discharged_hyps kn sechyps, + Discharge.process_inductive info 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/interp/declare.mli b/interp/declare.mli new file mode 100644 index 0000000000..6a09434645 --- /dev/null +++ b/interp/declare.mli @@ -0,0 +1,97 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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/interp/impargs.ml b/interp/impargs.ml new file mode 100644 index 0000000000..b7125fc85d --- /dev/null +++ b/interp/impargs.ml @@ -0,0 +1,737 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + 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 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 *) + let ty, _ = Global.type_of_global_in_context env (IndRef (kn,i)) in + Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty)) + 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_in_context env (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_in_context (Global.env ()) 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/interp/impargs.mli b/interp/impargs.mli new file mode 100644 index 0000000000..4b78f54eac --- /dev/null +++ b/interp/impargs.mli @@ -0,0 +1,139 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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/declare.ml b/library/declare.ml deleted file mode 100644 index 154793a32d..0000000000 --- a/library/declare.ml +++ /dev/null @@ -1,564 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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, _, _ as info = section_segment_of_mutual_inductive mind in - Some (discharged_hyps kn sechyps, - Discharge.process_inductive info 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 6a09434645..0000000000 --- a/library/declare.mli +++ /dev/null @@ -1,97 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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/impargs.ml b/library/impargs.ml deleted file mode 100644 index b7125fc85d..0000000000 --- a/library/impargs.ml +++ /dev/null @@ -1,737 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - 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 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 *) - let ty, _ = Global.type_of_global_in_context env (IndRef (kn,i)) in - Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty)) - 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_in_context env (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_in_context (Global.env ()) 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 4b78f54eac..0000000000 --- a/library/impargs.mli +++ /dev/null @@ -1,139 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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/printing/miscprint.ml b/printing/miscprint.ml deleted file mode 100644 index 5d37c8a024..0000000000 --- a/printing/miscprint.ml +++ /dev/null @@ -1,74 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* str "*" - | IntroForthcoming false -> str "**" - | IntroNaming p -> pr_intro_pattern_naming p - | IntroAction p -> pr_intro_pattern_action prc p - -and pr_intro_pattern_naming = function - | IntroIdentifier id -> Nameops.pr_id id - | IntroFresh id -> str "?" ++ Nameops.pr_id id - | IntroAnonymous -> str "?" - -and pr_intro_pattern_action prc = function - | IntroWildcard -> str "_" - | IntroOrAndPattern pll -> pr_or_and_intro_pattern prc pll - | IntroInjection pl -> - str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++ - str "]" - | IntroApplyOn ((_,c),pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c - | IntroRewrite true -> str "->" - | IntroRewrite false -> str "<-" - -and pr_or_and_intro_pattern prc = function - | IntroAndPattern pl -> - str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")" - | IntroOrPattern pll -> - str "[" ++ - hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll) - ++ str "]" - -(** Printing of [move_location] *) - -let pr_move_location pr_id = function - | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id - | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id - | MoveFirst -> str " at top" - | MoveLast -> str " at bottom" - -(** Printing of bindings *) -let pr_binding prc = function - | loc, (NamedHyp id, c) -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c) - | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) - -let pr_bindings prc prlc = function - | ImplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - pr_sequence prc l - | ExplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | NoBindings -> mt () - -let pr_bindings_no_with prc prlc = function - | ImplicitBindings l -> - brk (0,1) ++ prlist_with_sep spc prc l - | ExplicitBindings l -> - brk (0,1) ++ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | NoBindings -> mt () - -let pr_with_bindings prc prlc (c,bl) = - hov 1 (prc c ++ pr_bindings prc prlc bl) - diff --git a/printing/miscprint.mli b/printing/miscprint.mli deleted file mode 100644 index 21d410c7b0..0000000000 --- a/printing/miscprint.mli +++ /dev/null @@ -1,37 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Pp.std_ppcmds) -> 'a intro_pattern_expr Loc.located -> Pp.std_ppcmds - -val pr_or_and_intro_pattern : - ('a -> Pp.std_ppcmds) -> 'a or_and_intro_pattern_expr -> Pp.std_ppcmds - -val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds - -(** Printing of [move_location] *) - -val pr_move_location : - ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds - -val pr_bindings : - ('a -> Pp.std_ppcmds) -> - ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds - -val pr_bindings_no_with : - ('a -> Pp.std_ppcmds) -> - ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds - -val pr_with_bindings : - ('a -> Pp.std_ppcmds) -> - ('a -> Pp.std_ppcmds) -> 'a * 'a bindings -> Pp.std_ppcmds - diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml new file mode 100644 index 0000000000..5d37c8a024 --- /dev/null +++ b/proofs/miscprint.ml @@ -0,0 +1,74 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* str "*" + | IntroForthcoming false -> str "**" + | IntroNaming p -> pr_intro_pattern_naming p + | IntroAction p -> pr_intro_pattern_action prc p + +and pr_intro_pattern_naming = function + | IntroIdentifier id -> Nameops.pr_id id + | IntroFresh id -> str "?" ++ Nameops.pr_id id + | IntroAnonymous -> str "?" + +and pr_intro_pattern_action prc = function + | IntroWildcard -> str "_" + | IntroOrAndPattern pll -> pr_or_and_intro_pattern prc pll + | IntroInjection pl -> + str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++ + str "]" + | IntroApplyOn ((_,c),pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c + | IntroRewrite true -> str "->" + | IntroRewrite false -> str "<-" + +and pr_or_and_intro_pattern prc = function + | IntroAndPattern pl -> + str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")" + | IntroOrPattern pll -> + str "[" ++ + hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll) + ++ str "]" + +(** Printing of [move_location] *) + +let pr_move_location pr_id = function + | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id + | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id + | MoveFirst -> str " at top" + | MoveLast -> str " at bottom" + +(** Printing of bindings *) +let pr_binding prc = function + | loc, (NamedHyp id, c) -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c) + | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) + +let pr_bindings prc prlc = function + | ImplicitBindings l -> + brk (1,1) ++ str "with" ++ brk (1,1) ++ + pr_sequence prc l + | ExplicitBindings l -> + brk (1,1) ++ str "with" ++ brk (1,1) ++ + pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l + | NoBindings -> mt () + +let pr_bindings_no_with prc prlc = function + | ImplicitBindings l -> + brk (0,1) ++ prlist_with_sep spc prc l + | ExplicitBindings l -> + brk (0,1) ++ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l + | NoBindings -> mt () + +let pr_with_bindings prc prlc (c,bl) = + hov 1 (prc c ++ pr_bindings prc prlc bl) + diff --git a/proofs/miscprint.mli b/proofs/miscprint.mli new file mode 100644 index 0000000000..21d410c7b0 --- /dev/null +++ b/proofs/miscprint.mli @@ -0,0 +1,37 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Pp.std_ppcmds) -> 'a intro_pattern_expr Loc.located -> Pp.std_ppcmds + +val pr_or_and_intro_pattern : + ('a -> Pp.std_ppcmds) -> 'a or_and_intro_pattern_expr -> Pp.std_ppcmds + +val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds + +(** Printing of [move_location] *) + +val pr_move_location : + ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds + +val pr_bindings : + ('a -> Pp.std_ppcmds) -> + ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds + +val pr_bindings_no_with : + ('a -> Pp.std_ppcmds) -> + ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds + +val pr_with_bindings : + ('a -> Pp.std_ppcmds) -> + ('a -> Pp.std_ppcmds) -> 'a * 'a bindings -> Pp.std_ppcmds + diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml new file mode 100644 index 0000000000..0407c1e36a --- /dev/null +++ b/tactics/ind_tables.ml @@ -0,0 +1,203 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants +type individual_scheme_object_function = + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants + +type 'a scheme_kind = string + +let scheme_map = Summary.ref Indmap.empty ~name:"Schemes" + +let pr_scheme_kind = Pp.str + +let cache_one_scheme kind (ind,const) = + let map = try Indmap.find ind !scheme_map with Not_found -> String.Map.empty in + scheme_map := Indmap.add ind (String.Map.add kind const map) !scheme_map + +let cache_scheme (_,(kind,l)) = + Array.iter (cache_one_scheme kind) l + +let subst_one_scheme subst (ind,const) = + (* Remark: const is a def: the result of substitution is a constant *) + (subst_ind subst ind,subst_constant subst const) + +let subst_scheme (subst,(kind,l)) = + (kind,Array.map (subst_one_scheme subst) l) + +let discharge_scheme (_,(kind,l)) = + Some (kind,Array.map (fun (ind,const) -> + (Lib.discharge_inductive ind,Lib.discharge_con const)) l) + +let inScheme : string * (inductive * constant) array -> obj = + declare_object {(default_object "SCHEME") with + cache_function = cache_scheme; + load_function = (fun _ -> cache_scheme); + subst_function = subst_scheme; + classify_function = (fun obj -> Substitute obj); + discharge_function = discharge_scheme} + +(**********************************************************************) +(* The table of scheme building functions *) + +type individual +type mutual + +type scheme_object_function = + | MutualSchemeFunction of mutual_scheme_object_function + | IndividualSchemeFunction of individual_scheme_object_function + +let scheme_object_table = + (Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t) + +let declare_scheme_object s aux f = + let () = + if not (Id.is_valid ("ind" ^ s)) then + user_err Pp.(str ("Illegal induction scheme suffix: " ^ s)) + in + let key = if String.is_empty aux then s else aux in + try + let _ = Hashtbl.find scheme_object_table key in +(* let aux_msg = if aux="" then "" else " (with key "^aux^")" in*) + user_err ~hdr:"IndTables.declare_scheme_object" + (str "Scheme object " ++ str key ++ str " already declared.") + with Not_found -> + Hashtbl.add scheme_object_table key (s,f); + key + +let declare_mutual_scheme_object s ?(aux="") f = + declare_scheme_object s aux (MutualSchemeFunction f) + +let declare_individual_scheme_object s ?(aux="") f = + declare_scheme_object s aux (IndividualSchemeFunction f) + +(**********************************************************************) +(* Defining/retrieving schemes *) + +let declare_scheme kind indcl = + Lib.add_anonymous_leaf (inScheme (kind,indcl)) + +let () = Declare.set_declare_scheme declare_scheme + +let is_visible_name id = + try ignore (Nametab.locate (Libnames.qualid_of_ident id)); true + with Not_found -> false + +let compute_name internal id = + match internal with + | UserAutomaticRequest | UserIndividualRequest -> id + | InternalTacticRequest -> + Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name + +let define internal id c p univs = + let fd = declare_constant ~internal in + let id = compute_name internal id in + let ctx = Evd.normalize_evar_universe_context univs in + let c = Vars.subst_univs_fn_constr + (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in + let entry = { + const_entry_body = + Future.from_val ((c,Univ.ContextSet.empty), + Safe_typing.empty_private_constants); + const_entry_secctx = None; + const_entry_type = None; + const_entry_polymorphic = p; + const_entry_universes = Evd.evar_context_universe_context ctx; + const_entry_opaque = false; + const_entry_inline_code = false; + const_entry_feedback = None; + } in + let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in + let () = match internal with + | InternalTacticRequest -> () + | _-> definition_message id + in + kn + +let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = + let (c, ctx), eff = f mode ind in + let mib = Global.lookup_mind mind in + let id = match idopt with + | Some id -> id + | None -> add_suffix mib.mind_packets.(i).mind_typename suff in + let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in + declare_scheme kind [|ind,const|]; + const, Safe_typing.add_private + (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff + +let define_individual_scheme kind mode names (mind,i as ind) = + match Hashtbl.find scheme_object_table kind with + | _,MutualSchemeFunction f -> assert false + | s,IndividualSchemeFunction f -> + define_individual_scheme_base kind s f mode names ind + +let define_mutual_scheme_base kind suff f mode names mind = + let (cl, ctx), eff = f mode mind in + let mib = Global.lookup_mind mind in + let ids = Array.init (Array.length mib.mind_packets) (fun i -> + try Int.List.assoc i names + with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in + let consts = Array.map2 (fun id cl -> + define mode id cl (Declareops.inductive_is_polymorphic mib) ctx) ids cl in + let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in + declare_scheme kind schemes; + consts, + Safe_typing.add_private + (Safe_typing.private_con_of_scheme + ~kind (Global.safe_env()) (Array.to_list schemes)) + eff + +let define_mutual_scheme kind mode names mind = + match Hashtbl.find scheme_object_table kind with + | _,IndividualSchemeFunction _ -> assert false + | s,MutualSchemeFunction f -> + define_mutual_scheme_base kind s f mode names mind + +let find_scheme_on_env_too kind ind = + let s = String.Map.find kind (Indmap.find ind !scheme_map) in + s, Safe_typing.add_private + (Safe_typing.private_con_of_scheme + ~kind (Global.safe_env()) [ind, s]) + Safe_typing.empty_private_constants + +let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) = + try find_scheme_on_env_too kind ind + with Not_found -> + match Hashtbl.find scheme_object_table kind with + | s,IndividualSchemeFunction f -> + define_individual_scheme_base kind s f mode None ind + | s,MutualSchemeFunction f -> + let ca, eff = define_mutual_scheme_base kind s f mode [] mind in + ca.(i), eff + +let check_scheme kind ind = + try let _ = find_scheme_on_env_too kind ind in true + with Not_found -> false diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli new file mode 100644 index 0000000000..005555caa0 --- /dev/null +++ b/tactics/ind_tables.mli @@ -0,0 +1,51 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants +type individual_scheme_object_function = + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants + +(** Main functions to register a scheme builder *) + +val declare_mutual_scheme_object : string -> ?aux:string -> + mutual_scheme_object_function -> mutual scheme_kind + +val declare_individual_scheme_object : string -> ?aux:string -> + individual_scheme_object_function -> + individual scheme_kind + +(** Force generation of a (mutually) scheme with possibly user-level names *) + +val define_individual_scheme : individual scheme_kind -> + internal_flag (** internal *) -> + Id.t option -> inductive -> constant * Safe_typing.private_constants + +val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> + (int * Id.t) list -> mutual_inductive -> constant array * Safe_typing.private_constants + +(** Main function to retrieve a scheme in the cache or to generate it *) +val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Safe_typing.private_constants + +val check_scheme : 'a scheme_kind -> inductive -> bool + + +val pr_scheme_kind : 'a scheme_kind -> Pp.std_ppcmds diff --git a/vernac/ind_tables.ml b/vernac/ind_tables.ml deleted file mode 100644 index 0407c1e36a..0000000000 --- a/vernac/ind_tables.ml +++ /dev/null @@ -1,203 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants -type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants - -type 'a scheme_kind = string - -let scheme_map = Summary.ref Indmap.empty ~name:"Schemes" - -let pr_scheme_kind = Pp.str - -let cache_one_scheme kind (ind,const) = - let map = try Indmap.find ind !scheme_map with Not_found -> String.Map.empty in - scheme_map := Indmap.add ind (String.Map.add kind const map) !scheme_map - -let cache_scheme (_,(kind,l)) = - Array.iter (cache_one_scheme kind) l - -let subst_one_scheme subst (ind,const) = - (* Remark: const is a def: the result of substitution is a constant *) - (subst_ind subst ind,subst_constant subst const) - -let subst_scheme (subst,(kind,l)) = - (kind,Array.map (subst_one_scheme subst) l) - -let discharge_scheme (_,(kind,l)) = - Some (kind,Array.map (fun (ind,const) -> - (Lib.discharge_inductive ind,Lib.discharge_con const)) l) - -let inScheme : string * (inductive * constant) array -> obj = - declare_object {(default_object "SCHEME") with - cache_function = cache_scheme; - load_function = (fun _ -> cache_scheme); - subst_function = subst_scheme; - classify_function = (fun obj -> Substitute obj); - discharge_function = discharge_scheme} - -(**********************************************************************) -(* The table of scheme building functions *) - -type individual -type mutual - -type scheme_object_function = - | MutualSchemeFunction of mutual_scheme_object_function - | IndividualSchemeFunction of individual_scheme_object_function - -let scheme_object_table = - (Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t) - -let declare_scheme_object s aux f = - let () = - if not (Id.is_valid ("ind" ^ s)) then - user_err Pp.(str ("Illegal induction scheme suffix: " ^ s)) - in - let key = if String.is_empty aux then s else aux in - try - let _ = Hashtbl.find scheme_object_table key in -(* let aux_msg = if aux="" then "" else " (with key "^aux^")" in*) - user_err ~hdr:"IndTables.declare_scheme_object" - (str "Scheme object " ++ str key ++ str " already declared.") - with Not_found -> - Hashtbl.add scheme_object_table key (s,f); - key - -let declare_mutual_scheme_object s ?(aux="") f = - declare_scheme_object s aux (MutualSchemeFunction f) - -let declare_individual_scheme_object s ?(aux="") f = - declare_scheme_object s aux (IndividualSchemeFunction f) - -(**********************************************************************) -(* Defining/retrieving schemes *) - -let declare_scheme kind indcl = - Lib.add_anonymous_leaf (inScheme (kind,indcl)) - -let () = Declare.set_declare_scheme declare_scheme - -let is_visible_name id = - try ignore (Nametab.locate (Libnames.qualid_of_ident id)); true - with Not_found -> false - -let compute_name internal id = - match internal with - | UserAutomaticRequest | UserIndividualRequest -> id - | InternalTacticRequest -> - Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name - -let define internal id c p univs = - let fd = declare_constant ~internal in - let id = compute_name internal id in - let ctx = Evd.normalize_evar_universe_context univs in - let c = Vars.subst_univs_fn_constr - (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in - let entry = { - const_entry_body = - Future.from_val ((c,Univ.ContextSet.empty), - Safe_typing.empty_private_constants); - const_entry_secctx = None; - const_entry_type = None; - const_entry_polymorphic = p; - const_entry_universes = Evd.evar_context_universe_context ctx; - const_entry_opaque = false; - const_entry_inline_code = false; - const_entry_feedback = None; - } in - let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in - let () = match internal with - | InternalTacticRequest -> () - | _-> definition_message id - in - kn - -let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = - let (c, ctx), eff = f mode ind in - let mib = Global.lookup_mind mind in - let id = match idopt with - | Some id -> id - | None -> add_suffix mib.mind_packets.(i).mind_typename suff in - let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in - declare_scheme kind [|ind,const|]; - const, Safe_typing.add_private - (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff - -let define_individual_scheme kind mode names (mind,i as ind) = - match Hashtbl.find scheme_object_table kind with - | _,MutualSchemeFunction f -> assert false - | s,IndividualSchemeFunction f -> - define_individual_scheme_base kind s f mode names ind - -let define_mutual_scheme_base kind suff f mode names mind = - let (cl, ctx), eff = f mode mind in - let mib = Global.lookup_mind mind in - let ids = Array.init (Array.length mib.mind_packets) (fun i -> - try Int.List.assoc i names - with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in - let consts = Array.map2 (fun id cl -> - define mode id cl (Declareops.inductive_is_polymorphic mib) ctx) ids cl in - let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in - declare_scheme kind schemes; - consts, - Safe_typing.add_private - (Safe_typing.private_con_of_scheme - ~kind (Global.safe_env()) (Array.to_list schemes)) - eff - -let define_mutual_scheme kind mode names mind = - match Hashtbl.find scheme_object_table kind with - | _,IndividualSchemeFunction _ -> assert false - | s,MutualSchemeFunction f -> - define_mutual_scheme_base kind s f mode names mind - -let find_scheme_on_env_too kind ind = - let s = String.Map.find kind (Indmap.find ind !scheme_map) in - s, Safe_typing.add_private - (Safe_typing.private_con_of_scheme - ~kind (Global.safe_env()) [ind, s]) - Safe_typing.empty_private_constants - -let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) = - try find_scheme_on_env_too kind ind - with Not_found -> - match Hashtbl.find scheme_object_table kind with - | s,IndividualSchemeFunction f -> - define_individual_scheme_base kind s f mode None ind - | s,MutualSchemeFunction f -> - let ca, eff = define_mutual_scheme_base kind s f mode [] mind in - ca.(i), eff - -let check_scheme kind ind = - try let _ = find_scheme_on_env_too kind ind in true - with Not_found -> false diff --git a/vernac/ind_tables.mli b/vernac/ind_tables.mli deleted file mode 100644 index 005555caa0..0000000000 --- a/vernac/ind_tables.mli +++ /dev/null @@ -1,51 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants -type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants - -(** Main functions to register a scheme builder *) - -val declare_mutual_scheme_object : string -> ?aux:string -> - mutual_scheme_object_function -> mutual scheme_kind - -val declare_individual_scheme_object : string -> ?aux:string -> - individual_scheme_object_function -> - individual scheme_kind - -(** Force generation of a (mutually) scheme with possibly user-level names *) - -val define_individual_scheme : individual scheme_kind -> - internal_flag (** internal *) -> - Id.t option -> inductive -> constant * Safe_typing.private_constants - -val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> - (int * Id.t) list -> mutual_inductive -> constant array * Safe_typing.private_constants - -(** Main function to retrieve a scheme in the cache or to generate it *) -val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Safe_typing.private_constants - -val check_scheme : 'a scheme_kind -> inductive -> bool - - -val pr_scheme_kind : 'a scheme_kind -> Pp.std_ppcmds -- cgit v1.2.3