From b6b98a67c65d7aeeeeca12d1ccb9d55b654c554d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Jun 2016 15:12:05 +0200 Subject: A slight phase of documentation and uniformization of names of functions about interpretation, internalization, externalization of notations. Main syntactic changes: - subst_aconstr_in_glob_constr -> instantiate_notation_constr (because aconstr has been renamed to notation_constr long time ago) - extern_symbol -> extern_notation (because symbol.ml has been renamed to notation.ml long time ago) - documentation of notations_ops.mli Main semantic changes: - Notation_ops.eq_glob_constr which was partial eq disappears: use glob_constr_eq instead - In particular, this impacts a change on funind which now use the (fully implemented) glob_constr_eq Somehow, instantiate_notation_constr should be in notation_ops.ml for symmetry with match_notation_constr but it is bit painful to do. --- interp/notation_ops.mli | 32 +++++++++++++++++--------------- 1 file changed, 17 insertions(+), 15 deletions(-) (limited to 'interp/notation_ops.mli') diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 280ccfd21..576c5b943 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -10,24 +10,28 @@ open Names open Notation_term open Glob_term -(** Utilities about [notation_constr] *) +(** {5 Utilities about [notation_constr]} *) -(** Translate a [glob_constr] into a notation given the list of variables - bound by the notation; also interpret recursive patterns *) +val eq_notation_constr : notation_constr -> notation_constr -> bool -val notation_constr_of_glob_constr : notation_interp_env -> - glob_constr -> notation_constr +(** Substitution of kernel names in interpretation data *) +val subst_interpretation : + Mod_subst.substitution -> interpretation -> interpretation + (** Name of the special identifier used to encode recursive notations *) + val ldots_var : Id.t -(** Equality of [glob_constr] (warning: only partially implemented) *) -(** FIXME: nothing to do here *) -val eq_glob_constr : glob_constr -> glob_constr -> bool +(** {5 Translation back and forth between [glob_constr] and [notation_constr] *) -val eq_notation_constr : notation_constr -> notation_constr -> bool +(** Translate a [glob_constr] into a notation given the list of variables + bound by the notation; also interpret recursive patterns *) + +val notation_constr_of_glob_constr : notation_interp_env -> + glob_constr -> notation_constr -(** Re-interpret a notation as a [glob_constr], taking care of binders *) +(** Re-interpret a notation as a [glob_constr], taking care of binders *) val glob_constr_of_notation_constr_with_binders : Loc.t -> ('a -> Name.t -> 'a * Name.t) -> @@ -36,6 +40,8 @@ val glob_constr_of_notation_constr_with_binders : Loc.t -> val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr +(** {5 Matching a notation pattern against a [glob_constr] *) + (** [match_notation_constr] matches a [glob_constr] against a notation interpretation; raise [No_match] if the matching fails *) @@ -55,9 +61,5 @@ val match_notation_constr_ind_pattern : ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * (int * cases_pattern list) -(** Substitution of kernel names in interpretation data *) - -val subst_interpretation : - Mod_subst.substitution -> interpretation -> interpretation +(** {5 Matching a notation pattern against a [glob_constr] *) -val add_patterns_for_params : inductive -> cases_pattern list -> cases_pattern list -- cgit v1.2.3