Cases (coq-core.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