diff options
Diffstat (limited to 'pretyping/cases.mli')
| -rw-r--r-- | pretyping/cases.mli | 108 |
1 files changed, 86 insertions, 22 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 826d68a4..c599766a 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -1,14 +1,14 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Names open Term +open Context open Evd open Environ open Inductiveops @@ -23,37 +23,101 @@ type pattern_matching_error = | BadConstructor of constructor * inductive | WrongNumargConstructor of constructor * int | WrongNumargInductive of inductive * int - | WrongPredicateArity of constr * constr * constr - | NeedsInversion of constr * constr | UnusedClause of cases_pattern list | NonExhaustive of cases_pattern list | CannotInferPredicate of (constr * types) array -exception PatternMatchingError of env * pattern_matching_error +exception PatternMatchingError of env * evar_map * pattern_matching_error -val raise_pattern_matching_error : (loc * env * pattern_matching_error) -> 'a +val error_wrong_numarg_constructor_loc : Loc.t -> env -> constructor -> int -> 'a -val error_wrong_numarg_constructor_loc : loc -> env -> constructor -> int -> 'a +val error_wrong_numarg_inductive_loc : Loc.t -> env -> inductive -> int -> 'a -val error_wrong_numarg_inductive_loc : loc -> env -> inductive -> int -> 'a +(** {6 Compilation primitive. } *) -val error_bad_constructor_loc : loc -> constructor -> inductive -> 'a +val compile_cases : + Loc.t -> case_style -> + (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref -> + type_constraint -> + env -> glob_constr option * tomatch_tuples * cases_clauses -> + unsafe_judgment -val error_bad_pattern_loc : loc -> constructor -> constr -> 'a +val constr_of_pat : + Environ.env -> + Evd.evar_map ref -> + rel_declaration list -> + Glob_term.cases_pattern -> + Names.Id.t list -> + Glob_term.cases_pattern * + (rel_declaration list * Term.constr * + (Term.types * Term.constr list) * Glob_term.cases_pattern) * + Names.Id.t list -val error_wrong_predicate_arity_loc : loc -> env -> constr -> constr -> constr -> 'a +type 'a rhs = + { rhs_env : env; + rhs_vars : Id.t list; + avoid_ids : Id.t list; + it : 'a option} -val error_needs_inversion : env -> constr -> types -> 'a +type 'a equation = + { patterns : cases_pattern list; + rhs : 'a rhs; + alias_stack : Name.t list; + eqn_loc : Loc.t; + used : bool ref } -(** {6 Compilation primitive. } *) +type 'a matrix = 'a equation list + +(* 1st argument of IsInd is the original ind before extracting the summary *) +type tomatch_type = + | IsInd of types * inductive_type * Name.t list + | NotInd of constr option * types + +(* spiwack: The first argument of [Pushed] is [true] for initial + Pushed and [false] otherwise. Used to decide whether the term being + matched on must be aliased in the variable case (only initial + Pushed need to be aliased). The first argument of [Alias] is [true] + if the alias was introduced by an initial pushed and [false] + otherwise.*) +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 * rel_declaration + +type tomatch_stack = tomatch_status list + +(* We keep a constr for aliases and a cases_pattern for error message *) + +type pattern_history = + | Top + | MakeConstructor of constructor * pattern_continuation + +and pattern_continuation = + | Continuation of int * cases_pattern list * pattern_history + | Result of cases_pattern list + +type 'a pattern_matching_problem = + { env : env; + evdref : evar_map ref; + pred : constr; + tomatch : tomatch_stack; + history : pattern_continuation; + mat : 'a matrix; + caseloc : Loc.t; + casestyle : case_style; + typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment } + + +val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment -module type S = sig - val compile_cases : - loc -> case_style -> - (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref -> - type_constraint -> - env -> glob_constr option * tomatch_tuples * cases_clauses -> - unsafe_judgment -end +val prepare_predicate : Loc.t -> + (Evarutil.type_constraint -> + Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) -> + Environ.env -> + Evd.evar_map -> + (Term.types * tomatch_type) list -> + Context.rel_context list -> + Constr.constr option -> + 'a option -> (Evd.evar_map * Names.name list * Term.constr) list -module Cases_F(C : Coercion.S) : S |