Module Cases

Compilation of pattern-matching
type pattern_matching_error =
| BadPattern of Names.constructor * EConstr.constr
| BadConstructor of Names.constructor * Names.inductive
| WrongNumargConstructor of {
cstr : Names.constructor;
expanded : bool;
nargs : int;
expected_nassums : int;
expected_ndecls : int;
}
| WrongNumargInductive of {
ind : Names.inductive;
expanded : bool;
nargs : int;
expected_nassums : int;
expected_ndecls : int;
}
| UnusedClause of Glob_term.cases_pattern list
| NonExhaustive of Glob_term.cases_pattern list
| CannotInferPredicate of (EConstr.constr * EConstr.types) array
Pattern-matching errors
exception PatternMatchingError of Environ.env * Evd.evar_map * pattern_matching_error
val error_wrong_numarg_constructor : ?⁠loc:Loc.t -> Environ.env -> cstr:Names.constructor -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a
val error_wrong_numarg_inductive : ?⁠loc:Loc.t -> Environ.env -> ind:Names.inductive -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a
val irrefutable : Environ.env -> Glob_term.cases_pattern -> bool
Compilation primitive.
val compile_cases : ?⁠loc:Loc.t -> program_mode:bool -> Constr.case_style -> ((Evardefine.type_constraint -> GlobEnv.t -> Evd.evar_map -> Glob_term.glob_constr -> Evd.evar_map * EConstr.unsafe_judgment) * Evd.evar_map) -> Evardefine.type_constraint -> GlobEnv.t -> (Glob_term.glob_constr option * Glob_term.tomatch_tuples * Glob_term.cases_clauses) -> Evd.evar_map * EConstr.unsafe_judgment
val constr_of_pat : Environ.env -> Evd.evar_map -> EConstr.rel_context -> Glob_term.cases_pattern -> Names.Id.Set.t -> Evd.evar_map * Glob_term.cases_pattern * (EConstr.rel_context * EConstr.constr * (EConstr.types * EConstr.constr list) * Glob_term.cases_pattern) * Names.Id.Set.t
type 'a rhs = {
rhs_env : GlobEnv.t;
rhs_vars : Names.Id.Set.t;
avoid_ids : Names.Id.Set.t;
it : 'a option;
}
type 'a equation = {
patterns : Glob_term.cases_pattern list;
rhs : 'a rhs;
alias_stack : Names.Name.t list;
eqn_loc : Loc.t option;
orig : int option;
catch_all_vars : Names.Id.t CAst.t list;
}
type 'a matrix = 'a equation list
type tomatch_type =
| IsInd of EConstr.types * Inductiveops.inductive_type * Names.Name.t list
| NotInd of EConstr.constr option * EConstr.types
type tomatch_status =
| Pushed of bool * ((EConstr.constr * tomatch_type) * int list * Names.Name.t)
| Alias of bool * (Names.Name.t * EConstr.constr * (EConstr.constr * EConstr.types))
| NonDepAlias
| Abstract of int * EConstr.rel_declaration
type tomatch_stack = tomatch_status list
type pattern_history =
| Top
| MakeConstructor of Names.constructor * pattern_continuation
and pattern_continuation =
| Continuation of int * Glob_term.cases_pattern list * pattern_history
| Result of Glob_term.cases_pattern list
type 'a pattern_matching_problem = {
env : GlobEnv.t;
pred : EConstr.constr;
tomatch : tomatch_stack;
history : pattern_continuation;
mat : 'a matrix;
caseloc : Loc.t option;
casestyle : Constr.case_style;
typing_function : Evardefine.type_constraint -> GlobEnv.t -> Evd.evar_map -> 'a option -> Evd.evar_map * EConstr.unsafe_judgment;
}
val compile : program_mode:bool -> Evd.evar_map -> 'a pattern_matching_problem -> (int option * Names.Id.t CAst.t list) list * Evd.evar_map * EConstr.unsafe_judgment
val prepare_predicate : ?⁠loc:Loc.t -> program_mode:bool -> (Evardefine.type_constraint -> GlobEnv.t -> Evd.evar_map -> Glob_term.glob_constr -> Evd.evar_map * EConstr.unsafe_judgment) -> GlobEnv.t -> Evd.evar_map -> (EConstr.types * tomatch_type) list -> EConstr.rel_context list -> EConstr.constr option -> Glob_term.glob_constr option -> (Evd.evar_map * (Names.Name.t * Names.Name.t list) list * EConstr.constr) list
val make_return_predicate_ltac_lvar : GlobEnv.t -> Evd.evar_map -> Names.Name.t -> Glob_term.glob_constr -> EConstr.constr -> GlobEnv.t