From 272194ae1dd0769105e1f485c9b96670a19008a7 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 8 Nov 2009 17:31:16 +0000 Subject: Restructuration of command.ml + generic infrastructure for inductive schemes - Cleaning and uniformisation in command.ml: - For better modularity and better visibility, two files got isolated out of command.ml: - lemmas.ml is about starting and saving a proof - indschemes.ml is about declaring inductive schemes - Decomposition of the functions of command.ml into a functional part and the imperative part - Inductive schemes: - New architecture in ind_tables.ml for registering scheme builders, and for sharing and generating on demand inductive schemes - Adding new automatically generated equality schemes (file eqschemes.ml) - "_congr" for equality types (completing here commit 12273) - "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep", "_rew_backward" (similar to eq_rect), "_rew_backward_dep" for rewriting schemes (warning, rew_forward_dep cannot be stated following the standard Coq pattern for inductive types: "t=u" cannot be the last argument of the scheme) - "_case", "_case_nodep", "_case_dep" for case analysis schemes - Preliminary step towards discriminate and injection working on any equality-like type (e.g. eq_true) - Restating JMeq_congr under the canonical form of congruence schemes - Renamed "Set Equality Scheme" into "Set Equality Schemes" - Added "Set Rewriting Schemes", "Set Case Analysis Schemes" - Activation of the automatic generation of boolean equality lemmas - Partial debug and error messages improvements for the generation of boolean equality and decidable equality - Added schemes for making dependent rewrite working (unfortunately with not a fully satisfactory design - see file eqschemes.ml) - Some names of ML function made more regular (see dev/doc/changes.txt) - Incidentally, added a flush to obsolete Local/Global syntax warning git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12481 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/indrec.mli | 54 ++++++++++++++++++++++++++++------------------------ 1 file changed, 29 insertions(+), 25 deletions(-) (limited to 'pretyping/indrec.mli') diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index ac6a61c3c..91d559e17 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -27,36 +27,41 @@ exception RecursionSchemeError of recursion_scheme_error (** Eliminations *) -(* These functions build elimination predicate for Case tactic *) +type dep_flag = bool -val make_case_dep : env -> evar_map -> inductive -> sorts_family -> constr -val make_case_nodep : env -> evar_map -> inductive -> sorts_family -> constr -val make_case_gen : env -> evar_map -> inductive -> sorts_family -> constr +(* Build a case analysis elimination scheme in some sort family *) -(* This builds an elimination scheme associated (using the own arity - of the inductive) *) +val build_case_analysis_scheme : env -> evar_map -> inductive -> + dep_flag -> sorts_family -> constr -val build_indrec : env -> evar_map -> inductive -> constr -val instantiate_indrec_scheme : sorts -> int -> constr -> constr -val instantiate_type_indrec_scheme : sorts -> int -> constr -> types -> - constr * types +(* Build a dependent case elimination predicate unless type is in Prop *) -(** Complex recursion schemes [Scheme] *) +val build_case_analysis_scheme_default : env -> evar_map -> inductive -> + sorts_family -> constr -val build_mutual_indrec : - env -> evar_map -> - (inductive * mutual_inductive_body * one_inductive_body - * bool * sorts_family) list - -> constr list +(* Builds a recursive induction scheme (Peano-induction style) in the same + sort family as the inductive family; it is dependent if not in Prop *) -(** Old Case/Match typing *) +val build_induction_scheme : env -> evar_map -> inductive -> + dep_flag -> sorts_family -> constr -val type_rec_branches : bool -> env -> evar_map -> inductive_type - -> constr -> constr -> constr array * constr -val make_rec_branch_arg : - env -> evar_map -> - int * ('b * constr) option array * int -> - constr -> constructor_summary -> wf_paths list -> constr +(* Builds mutual (recursive) induction schemes *) + +val build_mutual_induction_scheme : + env -> evar_map -> (inductive * dep_flag * sorts_family) list -> constr list + +(** Scheme combinators *) + +(* [modify_sort_scheme s n c] modifies the quantification sort of + scheme c whose predicate is abstracted at position [n] of [c] *) + +val modify_sort_scheme : sorts -> int -> constr -> constr + +(* [weaken_sort_scheme s n c t] derives by subtyping from [c:t] + whose conclusion is quantified on [Type] at position [n] of [t] a + scheme quantified on sort [s] *) + +val weaken_sort_scheme : sorts -> int -> constr -> types -> constr * types (** Recursor names utilities *) @@ -64,5 +69,4 @@ val lookup_eliminator : inductive -> sorts_family -> constr val elimination_suffix : sorts_family -> string val make_elimination_ident : identifier -> sorts_family -> identifier - - +val case_suffix : string -- cgit v1.2.3