diff options
| -rw-r--r-- | pretyping/cases.mli | 69 |
1 files changed, 69 insertions, 0 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 07679567d..d7fff8af4 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -53,3 +53,72 @@ val constr_of_pat : (Context.Rel.Declaration.t list * Term.constr * (Term.types * Term.constr list) * Glob_term.cases_pattern) * Names.Id.t list + +type 'a rhs = + { rhs_env : env; + rhs_vars : Id.t list; + avoid_ids : Id.t list; + it : 'a option} + +type 'a equation = + { patterns : cases_pattern list; + rhs : 'a rhs; + alias_stack : Name.t list; + eqn_loc : Loc.t; + used : bool ref } + +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 * Context.Rel.Declaration.t + +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 + +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.t list -> + Constr.constr option -> + 'a option -> (Evd.evar_map * Names.name list * Term.constr) list + |