diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /interp/notation_ops.mli | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'interp/notation_ops.mli')
-rw-r--r-- | interp/notation_ops.mli | 37 |
1 files changed, 21 insertions, 16 deletions
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 280ccfd2..c8fcbf74 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 : Id.t list * Id.t list -> 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]} *) + +(** 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 * reversibility_flag -(** 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,14 +40,19 @@ 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 *) exception No_match +type glob_decl2 = + (name, cases_pattern) Util.union * Decl_kinds.binding_kind * + glob_constr option * glob_constr val match_notation_constr : bool -> glob_constr -> interpretation -> (glob_constr * subscopes) list * (glob_constr list * subscopes) list * - (glob_decl list * subscopes) list + (glob_decl2 list * subscopes) list val match_notation_constr_cases_pattern : cases_pattern -> interpretation -> @@ -55,9 +64,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 |