Imported Upstream version 8.5~beta1+dfsg

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