diff options
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 40 |
1 files changed, 15 insertions, 25 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 5dcc96dc29..a67948a778 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -70,14 +70,14 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name (** {6 Declare and uses back and forth an interpretation of primitive token } *) -(** A numeral interpreter is the pair of an interpreter for **integer** +(** A numeral interpreter is the pair of an interpreter for **decimal** numbers in terms and an optional interpreter in pattern, if - negative numbers are not supported, the interpreter must fail with - an appropriate error message *) + non integer or negative numbers are not supported, the interpreter + must fail with an appropriate error message *) type notation_location = (DirPath.t * DirPath.t) * string type required_module = full_path * string list -type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign +type rawnum = Constrexpr.sign * Constrexpr.raw_numeral (** The unique id string below will be used to refer to a particular registered interpreter/uninterpreter of numeral or string notation. @@ -112,8 +112,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t type numnot_option = | Nop - | Warning of raw_natural_number - | Abstract of raw_natural_number + | Warning of string + | Abstract of string type int_ty = { uint : Names.inductive; @@ -123,11 +123,16 @@ type z_pos_ty = { z_ty : Names.inductive; pos_ty : Names.inductive } +type decimal_ty = + { int : int_ty; + decimal : Names.inductive } + type target_kind = | Int of int_ty (* Coq.Init.Decimal.int + uint *) | UInt of Names.inductive (* Coq.Init.Decimal.uint *) | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *) + | Decimal of decimal_ty (* Coq.Init.Decimal.decimal + uint + int *) type string_target_kind = | ListByte @@ -211,8 +216,6 @@ type interp_rule = | NotationRule of scope_name option * notation | SynDefRule of KerName.t -module InterpRuleSet : Set.S with type elt = interp_rule - val declare_notation_interpretation : notation -> scope_name option -> interpretation -> notation_location -> onlyprint:bool -> unit @@ -222,28 +225,18 @@ val declare_uninterpretation : interp_rule -> interpretation -> unit val interp_notation : ?loc:Loc.t -> notation -> subscopes -> interpretation * (notation_location * scope_name option) -type notation_rule_core = - interp_rule (* kind of notation *) - * interpretation (* pattern associated to the notation *) - * int option (* number of expected arguments *) - -type notation_rule = - notation_rule_core - * delimiters option (* delimiter to possibly add *) - * bool (* true if the delimiter is mandatory *) +type notation_rule = interp_rule * interpretation * int option (** Return the possible notations for a given term *) -val uninterp_notations : subscopes -> 'a glob_constr_g -> notation_rule list -val uninterp_cases_pattern_notations : subscopes -> 'a cases_pattern_g -> notation_rule list -val uninterp_ind_pattern_notations : subscopes -> inductive -> notation_rule list +val uninterp_notations : 'a glob_constr_g -> notation_rule list +val uninterp_cases_pattern_notations : 'a cases_pattern_g -> notation_rule list +val uninterp_ind_pattern_notations : inductive -> notation_rule list -(* (** Test if a notation is available in the scopes context [scopes]; if available, the result is not None; the first argument is itself not None if a delimiters is needed *) val availability_of_notation : scope_name option * notation -> subscopes -> (scope_name option * delimiters option) option - *) (** {6 Miscellaneous} *) @@ -254,9 +247,6 @@ val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) -> val exists_notation_in_scope : scope_name option -> notation -> bool -> interpretation -> bool -(** Checks for already existing notations *) -val exists_notation_interpretation_in_scope : scope_name option -> notation -> bool - (** Declares and looks for scopes associated to arguments of a global ref *) val declare_arguments_scope : bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit |