diff options
Diffstat (limited to 'interp/constrexpr_ops.mli')
| -rw-r--r-- | interp/constrexpr_ops.mli | 69 |
1 files changed, 55 insertions, 14 deletions
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 7bd275e510..d038bd71ab 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -1,12 +1,13 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Loc open Names open Libnames open Misctypes @@ -44,9 +45,9 @@ val mkIdentC : Id.t -> constr_expr val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr val mkCastC : constr_expr * constr_expr cast_type -> constr_expr -val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr -val mkLetInC : Name.t located * constr_expr * constr_expr option * constr_expr -> constr_expr -val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr +val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr +val mkLetInC : lname * constr_expr * constr_expr option * constr_expr -> constr_expr +val mkProdC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr (** Same as [abstract_constr_expr], with location *) @@ -54,32 +55,72 @@ val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_e val mkCProdN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr (** Same as [prod_constr_expr], with location *) +val mkCPatOr : ?loc:Loc.t -> cases_pattern_expr list -> cases_pattern_expr + +val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list -> cases_pattern_expr +(** Apply a list of pattern arguments to a pattern *) + (** @deprecated variant of mkCLambdaN *) val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr +[@@ocaml.deprecated "deprecated variant of mkCLambdaN"] (** @deprecated variant of mkCProdN *) val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr - -val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t +[@@ocaml.deprecated "deprecated variant of mkCProdN"] (** {6 Destructors}*) val coerce_reference_to_id : reference -> Id.t (** FIXME: nothing to do here *) -val coerce_to_id : constr_expr -> Id.t located +val coerce_to_id : constr_expr -> lident (** Destruct terms of the form [CRef (Ident _)]. *) -val coerce_to_name : constr_expr -> Name.t located +val coerce_to_name : constr_expr -> lname (** Destruct terms of the form [CRef (Ident _)] or [CHole _]. *) +val coerce_to_cases_pattern_expr : constr_expr -> cases_pattern_expr + (** {6 Binder manipulation} *) val default_binder_kind : binder_kind -val names_of_local_binders : local_binder_expr list -> Name.t located list +val names_of_local_binders : local_binder_expr list -> lname list (** Retrieve a list of binding names from a list of binders. *) -val names_of_local_assums : local_binder_expr list -> Name.t located list +val names_of_local_assums : local_binder_expr list -> lname list (** Same as [names_of_local_binder_exprs], but does not take the [let] bindings into account. *) + +(** {6 Folds and maps} *) + +(** Used in typeclasses *) +val fold_constr_expr_with_binders : (Id.t -> 'a -> 'a) -> + ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b + +(** Used in correctness and interface; absence of var capture not guaranteed + in pattern-matching clauses and in binders of the form [x,y:T(x)] *) + +val map_constr_expr_with_binders : + (Id.t -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) -> + 'a -> constr_expr -> constr_expr + +val replace_vars_constr_expr : + Id.t Id.Map.t -> constr_expr -> constr_expr + +(** Specific function for interning "in indtype" syntax of "match" *) +val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t + +val free_vars_of_constr_expr : constr_expr -> Id.Set.t +val occur_var_constr_expr : Id.t -> constr_expr -> bool + +val split_at_annot : local_binder_expr list -> lident option -> local_binder_expr list * local_binder_expr list + +val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list +val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list + +(** For cases pattern parsing errors *) +val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a + +(** Placeholder for global option, should be moved to a parameter *) +val asymmetric_patterns : bool ref |