summaryrefslogtreecommitdiff
path: root/pretyping/cases.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
commit7cfc4e5146be5666419451bdd516f1f3f264d24a (patch)
treee4197645da03dc3c7cc84e434cc31d0a0cca7056 /pretyping/cases.mli
parent420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff)
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'pretyping/cases.mli')
-rw-r--r--pretyping/cases.mli108
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