diff options
Diffstat (limited to 'pretyping/cases.mli')
| -rw-r--r-- | pretyping/cases.mli | 68 |
1 files changed, 38 insertions, 30 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index ee4148de..04a34646 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -1,18 +1,22 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names -open Term +open Constr open Evd open Environ +open EConstr open Inductiveops open Glob_term -open Evarutil +open Ltac_pretype +open Evardefine (** {5 Compilation of pattern-matching } *) @@ -28,43 +32,43 @@ type pattern_matching_error = exception PatternMatchingError of env * evar_map * pattern_matching_error -val error_wrong_numarg_constructor_loc : Loc.t -> env -> constructor -> int -> 'a +val error_wrong_numarg_constructor : ?loc:Loc.t -> env -> constructor -> int -> 'a -val error_wrong_numarg_inductive_loc : Loc.t -> env -> inductive -> int -> 'a +val error_wrong_numarg_inductive : ?loc:Loc.t -> env -> inductive -> int -> 'a val irrefutable : env -> cases_pattern -> bool (** {6 Compilation primitive. } *) val compile_cases : - Loc.t -> case_style -> - (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref -> + ?loc:Loc.t -> case_style -> + (type_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) * evar_map ref -> type_constraint -> - env -> glob_constr option * tomatch_tuples * cases_clauses -> + env -> ltac_var_map -> glob_constr option * tomatch_tuples * cases_clauses -> unsafe_judgment val constr_of_pat : Environ.env -> Evd.evar_map ref -> - Context.Rel.Declaration.t list -> + rel_context -> Glob_term.cases_pattern -> - Names.Id.t list -> + Names.Id.Set.t -> Glob_term.cases_pattern * - (Context.Rel.Declaration.t list * Term.constr * - (Term.types * Term.constr list) * Glob_term.cases_pattern) * - Names.Id.t list + (rel_context * constr * + (types * constr list) * Glob_term.cases_pattern) * + Names.Id.Set.t type 'a rhs = { rhs_env : env; - rhs_vars : Id.t list; - avoid_ids : Id.t list; + rhs_vars : Id.Set.t; + avoid_ids : Id.Set.t; it : 'a option} type 'a equation = { patterns : cases_pattern list; rhs : 'a rhs; alias_stack : Name.t list; - eqn_loc : Loc.t; + eqn_loc : Loc.t option; used : bool ref } type 'a matrix = 'a equation list @@ -84,7 +88,7 @@ type tomatch_status = | Pushed of (bool*((constr * tomatch_type) * int list * Name.t)) | Alias of (bool * (Name.t * constr * (constr * types))) | NonDepAlias - | Abstract of int * Context.Rel.Declaration.t + | Abstract of int * rel_declaration type tomatch_stack = tomatch_status list @@ -100,25 +104,29 @@ and pattern_continuation = type 'a pattern_matching_problem = { env : env; + lvar : Ltac_pretype.ltac_var_map; evdref : evar_map ref; pred : constr; tomatch : tomatch_stack; history : pattern_continuation; mat : 'a matrix; - caseloc : Loc.t; + caseloc : Loc.t option; casestyle : case_style; typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment } -val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment +val compile : 'a pattern_matching_problem -> unsafe_judgment -val prepare_predicate : Loc.t -> - (Evarutil.type_constraint -> - Environ.env -> Evd.evar_map ref -> glob_constr -> Environ.unsafe_judgment) -> +val prepare_predicate : ?loc:Loc.t -> + (type_constraint -> + Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) -> Environ.env -> Evd.evar_map -> - (Term.types * tomatch_type) list -> - Context.Rel.t list -> - Constr.constr option -> - glob_constr option -> - (Evd.evar_map * Names.name list * Term.constr) list + Ltac_pretype.ltac_var_map -> + (types * tomatch_type) list -> + (rel_context * rel_context) list -> + constr option -> + glob_constr option -> (Evd.evar_map * Name.t list * constr) list + +val make_return_predicate_ltac_lvar : Evd.evar_map -> Name.t -> + Glob_term.glob_constr -> constr -> Ltac_pretype.ltac_var_map -> ltac_var_map |