diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.ml | 16 | ||||
| -rw-r--r-- | API/API.mli | 141 |
2 files changed, 84 insertions, 73 deletions
diff --git a/API/API.ml b/API/API.ml index c4bcef6f6c..46ad36d36d 100644 --- a/API/API.ml +++ b/API/API.ml @@ -10,9 +10,9 @@ To see such order issue the comand: -``` -bash -c 'for i in kernel intf library engine pretyping interp proofs parsing printing tactics vernac stm toplevel; do echo -e "\n## $i files" && cat ${i}/${i}.mllib; done && echo -e "\n## highparsing files" && cat parsing/highparsing.mllib' > API/link -``` + ``` + bash -c 'for i in kernel intf library engine pretyping interp proofs parsing printing tactics vernac stm toplevel; do echo -e "\n## $i files" && cat ${i}/${i}.mllib; done > API/link + ``` *) (******************************************************************************) @@ -162,6 +162,7 @@ module Indrec = Indrec (* module Cases *) module Pretyping = Pretyping module Unification = Unification +module Univdecls = Univdecls (******************************************************************************) (* interp *) (******************************************************************************) @@ -223,6 +224,9 @@ module Pcoq = Pcoq module Egramml = Egramml (* Egramcoq *) +module G_vernac = G_vernac +module G_proofs = G_proofs + (******************************************************************************) (* Tactics *) (******************************************************************************) @@ -276,9 +280,3 @@ module Vernacentries = Vernacentries (******************************************************************************) module Vernac_classifier = Vernac_classifier module Stm = Stm - -(******************************************************************************) -(* Highparsing *) -(******************************************************************************) -module G_vernac = G_vernac -module G_proofs = G_proofs diff --git a/API/API.mli b/API/API.mli index 8b0bef48c9..3ed326ff0e 100644 --- a/API/API.mli +++ b/API/API.mli @@ -10,7 +10,7 @@ in Coq. To see such order issue the comand: ``` - bash -c 'for i in kernel intf library engine pretyping interp proofs parsing printing tactics vernac stm toplevel; do echo -e "\n## $i files" && cat ${i}/${i}.mllib; done && echo -e "\n## highparsing files" && cat parsing/highparsing.mllib' > API/link + bash -c 'for i in kernel intf library engine pretyping interp proofs parsing printing tactics vernac stm toplevel; do echo -e "\n## $i files" && cat ${i}/${i}.mllib; done > API/link ``` Note however that files in intf/ are located manually now as their @@ -1648,6 +1648,14 @@ sig type sort_info = Names.Name.t Loc.located list type glob_sort = sort_info glob_sort_gen + type ('a, 'b) gen_universe_decl = { + univdecl_instance : 'a; (* Declared universes *) + univdecl_extensible_instance : bool; (* Can new universes be added *) + univdecl_constraints : 'b; (* Declared constraints *) + univdecl_extensible_constraints : bool (* Can new constraints be added *) } + + type glob_constraint = glob_level * Univ.constraint_type * glob_level + type case_style = Term.case_style = | LetStyle | IfStyle @@ -2300,7 +2308,7 @@ sig val universe_context_set : evar_map -> Univ.ContextSet.t val evar_ident : evar -> evar_map -> Names.Id.t option val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list - val universe_context : ?names:(Names.Id.t Loc.located) list -> evar_map -> + val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map -> (Names.Id.t * Univ.Level.t) list * Univ.UContext.t val nf_constraints : evar_map -> evar_map val from_ctx : UState.t -> evar_map @@ -2461,7 +2469,6 @@ sig constr_expr list list * local_binder_expr list list - type typeclass_constraint = (Names.Name.t Loc.located * Names.Id.t Loc.located list option) * Decl_kinds.binding_kind * constr_expr type constr_pattern_expr = constr_expr end @@ -2744,15 +2751,15 @@ sig the whole identifier except for the {i subscript}. E.g. if we take [foo42], then [42] is the {i subscript}, and [foo] is the root. *) - val next_ident_away : Names.Id.t -> Names.Id.t list -> Names.Id.t + val next_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t val hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> string val id_of_name_using_hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> Names.Name.t -> Names.Id.t - val next_ident_away_in_goal : Names.Id.t -> Names.Id.t list -> Names.Id.t + val next_ident_away_in_goal : Names.Id.t -> Names.Id.Set.t -> Names.Id.t val default_dependent_ident : Names.Id.t - val next_global_ident_away : Names.Id.t -> Names.Id.t list -> Names.Id.t + val next_global_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t val rename_bound_vars_as_displayed : - Evd.evar_map -> Names.Id.t list -> Names.Name.t list -> EConstr.types -> EConstr.types + Evd.evar_map -> Names.Id.Set.t -> Names.Name.t list -> EConstr.types -> EConstr.types end module Termops : @@ -2763,6 +2770,7 @@ sig val pr_evar_info : Evd.evar_info -> Pp.t val print_constr : EConstr.constr -> Pp.t + val pr_sort_family : Sorts.family -> Pp.t (** [dependent m t] tests whether [m] is a subterm of [t] *) val dependent : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool @@ -2810,6 +2818,8 @@ sig val print_constr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t val clear_named_body : Names.Id.t -> Environ.env -> Environ.env val is_Prop : Evd.evar_map -> EConstr.constr -> bool + val is_Set : Evd.evar_map -> EConstr.constr -> bool + val is_Type : Evd.evar_map -> EConstr.constr -> bool val is_global : Evd.evar_map -> Globnames.global_reference -> EConstr.constr -> bool val eq_constr : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool @@ -3660,7 +3670,7 @@ sig type lname = Names.Name.t Loc.located type lident = Names.Id.t Loc.located type opacity_flag = - | Opaque of lident list option + | Opaque | Transparent type locality_flag = bool type inductive_kind = @@ -3673,7 +3683,7 @@ sig | VtProofStep of proof_step | VtProofMode of string | VtQuery of vernac_part_of_script * Feedback.route_id - | VtStm of vernac_control * vernac_part_of_script + | VtBack of vernac_part_of_script * Stateid.t | VtUnknown and vernac_qed_type = | VtKeep @@ -3682,10 +3692,6 @@ sig and vernac_start = string * opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and vernac_part_of_script = bool - and vernac_control = - | VtWait - | VtJoinDocument - | VtBack of Stateid.t and opacity_guarantee = | GuaranteesOpacity | Doesn'tGuaranteeOpacity @@ -3705,6 +3711,10 @@ sig type obsolete_locality = bool + type universe_decl_expr = (lident list, Misctypes.glob_constraint list) gen_universe_decl + + type ident_decl = lident * universe_decl_expr option + type lstring type 'a with_coercion = coercion_flag * 'a type scope_name = string @@ -3722,9 +3732,7 @@ sig | Constructors of constructor_expr list | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list - type plident = lident * lident list option - - type inductive_expr = plident with_coercion * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * inductive_kind * constructor_list_or_record_decl_expr + type inductive_expr = ident_decl with_coercion * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * inductive_kind * constructor_list_or_record_decl_expr type syntax_modifier = | SetItemLevel of string list * Extend.production_level @@ -3738,18 +3746,20 @@ sig type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation + type typeclass_constraint = (Names.Name.t Loc.located * universe_decl_expr option) * Decl_kinds.binding_kind * constr_expr + type definition_expr = | ProveBody of local_binder_expr list * constr_expr | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr * constr_expr option type proof_expr = - plident option * (local_binder_expr list * constr_expr) + ident_decl option * (local_binder_expr list * constr_expr) type proof_end = | Admitted | Proved of opacity_flag * lident option - type fixpoint_expr = plident * (Names.Id.t Loc.located option * Constrexpr.recursion_order_expr) * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr option + type fixpoint_expr = ident_decl * (Names.Id.t Loc.located option * Constrexpr.recursion_order_expr) * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr option type cofixpoint_expr @@ -3767,7 +3777,6 @@ sig type option_value type showable type bullet - type stm_vernac type comment type register_kind type locatable @@ -3817,7 +3826,7 @@ sig | VernacTimeout of int * vernac_expr | VernacFail of vernac_expr | VernacSyntaxExtension of - obsolete_locality * (lstring * syntax_modifier list) + bool * obsolete_locality * (lstring * syntax_modifier list) | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) | VernacDelimiters of scope_name * string option | VernacBindScope of scope_name * class_rawexpr list @@ -3828,12 +3837,12 @@ sig scope_name option | VernacNotationAddFormat of string * string * string | VernacDefinition of - (Decl_kinds.locality option * Decl_kinds.definition_object_kind) * plident * definition_expr + (Decl_kinds.locality option * Decl_kinds.definition_object_kind) * ident_decl * definition_expr | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list | VernacEndProof of proof_end | VernacExactProof of Constrexpr.constr_expr | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) * - inline * (plident list * Constrexpr.constr_expr) with_coercion list + inline * (ident_decl list * Constrexpr.constr_expr) with_coercion list | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list @@ -3857,7 +3866,7 @@ sig | VernacInstance of bool * Constrexpr.local_binder_expr list * - Constrexpr.typeclass_constraint * + typeclass_constraint * (bool * Constrexpr.constr_expr) option * hint_info_expr | VernacContext of Constrexpr.local_binder_expr list @@ -3919,7 +3928,6 @@ sig | VernacLocate of locatable | VernacRegister of lident * register_kind | VernacComments of comment list - | VernacStm of stm_vernac | VernacGoal of Constrexpr.constr_expr | VernacAbort of lident option | VernacAbortAll @@ -3949,7 +3957,7 @@ sig | SelectAll and vernac_classification = vernac_type * vernac_when and one_inductive_expr = - plident * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * constructor_expr list + ident_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * constructor_expr list end (* XXX: end manual intf move *) @@ -4003,7 +4011,7 @@ sig | Later : [ `thunk ] delay val print_universes : bool ref val print_evar_arguments : bool ref - val detype : 'a delay -> ?lax:bool -> bool -> Names.Id.t list -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'a Glob_term.glob_constr_g + val detype : 'a delay -> ?lax:bool -> bool -> Names.Id.Set.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'a Glob_term.glob_constr_g val subst_glob_constr : Mod_subst.substitution -> Glob_term.glob_constr -> Glob_term.glob_constr val set_detype_anonymous : (?loc:Loc.t -> int -> Names.Id.t) -> unit end @@ -4046,7 +4054,6 @@ sig val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> Environ.env -> Evd.evar_map -> Glob_term.glob_constr -> Constr.t Evd.in_evar_universe_context val check_evars : Environ.env -> Evd.evar_map -> Evd.evar_map -> EConstr.constr -> unit - val interp_elimination_sort : Misctypes.glob_sort -> Sorts.family val register_constr_interp0 : ('r, 'g, 't) Genarg.genarg_type -> (Glob_term.unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit @@ -4087,6 +4094,18 @@ sig Environ.env -> Evd.evar_map -> ?flags:unify_flags -> EConstr.constr * EConstr.constr -> Evd.evar_map * EConstr.constr end +module Univdecls : +sig + type universe_decl = + (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + + val interp_univ_decl : Environ.env -> Vernacexpr.universe_decl_expr -> + Evd.evar_map * universe_decl + val interp_univ_decl_opt : Environ.env -> Vernacexpr.universe_decl_expr option -> + Evd.evar_map * universe_decl + val default_univ_decl : universe_decl +end + (************************************************************************) (* End of modules from pretyping/ *) (************************************************************************) @@ -4142,6 +4161,7 @@ sig val wit_global : (Libnames.reference, Globnames.global_reference Loc.located Misctypes.or_var, Globnames.global_reference) Genarg.genarg_type val wit_ident : Names.Id.t Genarg.uniform_genarg_type val wit_integer : int Genarg.uniform_genarg_type + val wit_sort_family : (Sorts.family, unit, unit) Genarg.genarg_type val wit_constr : (Constrexpr.constr_expr, Tactypes.glob_constr_and_expr, EConstr.constr) Genarg.genarg_type val wit_open_constr : (Constrexpr.constr_expr, Tactypes.glob_constr_and_expr, EConstr.constr) Genarg.genarg_type val wit_intro_pattern : (Constrexpr.constr_expr Misctypes.intro_pattern_expr Loc.located, Tactypes.glob_constr_and_expr Misctypes.intro_pattern_expr Loc.located, Tactypes.intro_pattern) Genarg.genarg_type @@ -4484,12 +4504,11 @@ sig type proof_terminator type lemma_possible_guards - type universe_binders type closed_proof = proof_object * proof_terminator val make_terminator : (proof_ending -> unit) -> proof_terminator val start_dependent_proof : - Names.Id.t -> ?pl:universe_binders -> Decl_kinds.goal_kind -> + Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind -> Proofview.telescope -> proof_terminator -> unit val with_current_proof : (unit Proofview.tactic -> Proof.proof -> Proof.proof * 'a) -> 'a @@ -4609,6 +4628,7 @@ sig val pf_env : 'a Proofview.Goal.t -> Environ.env val pf_ids_of_hyps : 'a Proofview.Goal.t -> Names.Id.t list + val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Names.Id.Set.t val pf_concl : 'a Proofview.Goal.t -> EConstr.types val pf_get_new_id : Names.Id.t -> 'a Proofview.Goal.t -> Names.Id.t val pf_get_hyp_typ : Names.Id.t -> 'a Proofview.Goal.t -> EConstr.types @@ -4703,7 +4723,7 @@ sig type coq_parsable - val parsable : ?file:string -> char Stream.t -> coq_parsable + val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable val action : 'a -> action val entry_create : string -> 'a entry val entry_parse : 'a entry -> coq_parsable -> 'a @@ -4773,6 +4793,7 @@ sig val global : reference Gram.entry val universe_level : glob_level Gram.entry val sort : glob_sort Gram.entry + val sort_family : Sorts.family Gram.entry val pattern : cases_pattern_expr Gram.entry val constr_pattern : constr_expr Gram.entry val lconstr_pattern : constr_expr Gram.entry @@ -4849,6 +4870,23 @@ sig end +module G_vernac : +sig + + val def_body : Vernacexpr.definition_expr Pcoq.Gram.entry + val section_subset_expr : Vernacexpr.section_subset_expr Pcoq.Gram.entry + val query_command : (Vernacexpr.goal_selector option -> Vernacexpr.vernac_expr) Pcoq.Gram.entry + +end + +module G_proofs : +sig + + val hint : Vernacexpr.hints_expr Pcoq.Gram.entry + val hint_proof_using : 'a Pcoq.Gram.entry -> 'a option -> 'a option + +end + (************************************************************************) (* End of modules from parsing/ *) (************************************************************************) @@ -5103,7 +5141,7 @@ sig val convert_concl : ?check:bool -> EConstr.types -> Constr.cast_kind -> unit tactic val intro_using : Names.Id.t -> unit tactic val intro : unit tactic - val fresh_id_in_env : Names.Id.t list -> Names.Id.t -> Environ.env -> Names.Id.t + val fresh_id_in_env : Names.Id.Set.t -> Names.Id.t -> Environ.env -> Names.Id.t val is_quantified_hypothesis : Names.Id.t -> 'a Goal.t -> bool val tclABSTRACT : ?opaque:bool -> Names.Id.t option -> unit Proofview.tactic -> unit Proofview.tactic val intro_patterns : bool -> Tactypes.intro_patterns -> unit Proofview.tactic @@ -5203,7 +5241,7 @@ sig val eapply_with_bindings : EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic val assert_by : Names.Name.t -> EConstr.types -> unit Proofview.tactic -> unit Proofview.tactic - val intro_avoiding : Names.Id.t list -> unit Proofview.tactic + val intro_avoiding : Names.Id.Set.t -> unit Proofview.tactic val pose_proof : Names.Name.t -> EConstr.constr -> unit Proofview.tactic val pattern_option : (Locus.occurrences * EConstr.constr) list -> Locus.goal_location -> unit Proofview.tactic val compute_elim_sig : Evd.evar_map -> ?elimc:EConstr.constr Misctypes.with_bindings -> EConstr.types -> elim_scheme @@ -5333,7 +5371,7 @@ sig val lemInv_clause : Misctypes.quantified_hypothesis -> EConstr.constr -> Names.Id.t list -> unit Proofview.tactic val add_inversion_lemma_exn : - Names.Id.t -> Constrexpr.constr_expr -> Misctypes.glob_sort -> bool -> (Names.Id.t -> unit Proofview.tactic) -> + Names.Id.t -> Constrexpr.constr_expr -> Sorts.family -> bool -> (Names.Id.t -> unit Proofview.tactic) -> unit end @@ -5525,7 +5563,7 @@ sig val mk_hook : (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook - val start_proof : Names.Id.t -> ?pl:Proof_global.universe_binders -> Decl_kinds.goal_kind -> Evd.evar_map -> + val start_proof : Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind -> Evd.evar_map -> ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> @@ -5601,7 +5639,7 @@ sig type structured_fixpoint_expr = { fix_name : Id.t; - fix_univs : lident list option; + fix_univs : universe_decl_expr option; fix_annot : Id.t Loc.located option; fix_binders : local_binder_expr list; fix_body : constr_expr option; @@ -5610,7 +5648,7 @@ sig type structured_one_inductive_expr = { ind_name : Id.t; - ind_univs : lident list option; + ind_univs : universe_decl_expr option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } @@ -5626,7 +5664,7 @@ sig (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> unit - val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.lident list option -> + val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option -> Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr -> Constrexpr.constr_expr option -> unit Lemmas.declaration_hook -> unit @@ -5639,7 +5677,7 @@ sig val interp_fixpoint : structured_fixpoint_expr list -> Vernacexpr.decl_notation list -> - recursive_preentry * Vernacexpr.lident list option * UState.t * + recursive_preentry * Univdecls.universe_decl * UState.t * (EConstr.rel_context * Impargs.manual_implicits * int option) list val extract_mutual_inductive_declaration_components : @@ -5667,7 +5705,7 @@ sig ?refine:bool -> Decl_kinds.polymorphic -> Constrexpr.local_binder_expr list -> - Constrexpr.typeclass_constraint -> + Vernacexpr.typeclass_constraint -> (bool * Constrexpr.constr_expr) option -> ?generalize:bool -> ?tac:unit Proofview.tactic -> @@ -5738,28 +5776,3 @@ end (************************************************************************) (* End of modules from stm/ *) (************************************************************************) - -(************************************************************************) -(* Modules from highparsing/ *) -(************************************************************************) - -module G_vernac : -sig - - val def_body : Vernacexpr.definition_expr Pcoq.Gram.entry - val section_subset_expr : Vernacexpr.section_subset_expr Pcoq.Gram.entry - val query_command : (Vernacexpr.goal_selector option -> Vernacexpr.vernac_expr) Pcoq.Gram.entry - -end - -module G_proofs : -sig - - val hint : Vernacexpr.hints_expr Pcoq.Gram.entry - val hint_proof_using : 'a Pcoq.Gram.entry -> 'a option -> 'a option - -end - -(************************************************************************) -(* End of modules from highparsing/ *) -(************************************************************************) |