From 094b577f61f105f0a92f3f84d7e739884dd993a7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 19 Nov 2017 05:11:18 +0100 Subject: [parser] Remove unnecessary statically initialized hook. Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to put any pattern in binders, prefixed by a quote."] its current placement as well as the hook don't make a lot of sense. In particular, they prevent parts of Coq working without linking the parser. To this purpose, we need to consolidate the `Constrexpr` utilities. While we are at it we do so and remove the `Topconstr` module which is fully redundant with `Constrexpr_ops`. --- interp/constrexpr_ops.mli | 37 +++++++++++++++++++++++++++++++++++-- 1 file changed, 35 insertions(+), 2 deletions(-) (limited to 'interp/constrexpr_ops.mli') diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 7bd275e51..3ecb3d321 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -56,11 +56,11 @@ val mkCProdN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_exp (** @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}*) @@ -83,3 +83,36 @@ val names_of_local_binders : local_binder_expr list -> Name.t located list val names_of_local_assums : local_binder_expr list -> Name.t located 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 -> Id.t located 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 -- cgit v1.2.3