diff options
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 260 |
1 files changed, 179 insertions, 81 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index c150ae7abb..8d05fab63c 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -32,7 +32,7 @@ open NumTok fail if a number has no interpretation in the scope (e.g. there is no interpretation for negative numbers in [nat]); interpreters both for terms and patterns can be set; these interpreters are in permanent table - [numeral_interpreter_tab] + [number_interpreter_tab] - a set of ML printers for expressions denoting numbers parsable in this scope - a set of interpretations for infix (more generally distfix) notations @@ -451,13 +451,13 @@ module InnerPrimToken = struct let do_interp ?loc interp primtok = match primtok, interp with - | Numeral n, RawNumInterp interp -> interp ?loc n - | Numeral n, BigNumInterp interp -> + | Number n, RawNumInterp interp -> interp ?loc n + | Number n, BigNumInterp interp -> (match NumTok.Signed.to_bigint n with | Some n -> interp ?loc n | None -> raise Not_found) | String s, StringInterp interp -> interp ?loc s - | (Numeral _ | String _), + | (Number _ | String _), (RawNumInterp _ | BigNumInterp _ | StringInterp _) -> raise Not_found type uninterpreter = @@ -471,16 +471,16 @@ module InnerPrimToken = struct | StringUninterp f, StringUninterp f' -> f == f' | _ -> false - let mkNumeral n = - Numeral (NumTok.Signed.of_bigint CDec n) + let mkNumber n = + Number (NumTok.Signed.of_bigint CDec n) let mkString = function | None -> None | Some s -> if Unicode.is_utf8 s then Some (String s) else None let do_uninterp uninterp g = match uninterp with - | RawNumUninterp u -> Option.map (fun (s,n) -> Numeral (s,n)) (u g) - | BigNumUninterp u -> Option.map mkNumeral (u g) + | RawNumUninterp u -> Option.map (fun (s,n) -> Number (s,n)) (u g) + | BigNumUninterp u -> Option.map mkNumber (u g) | StringUninterp u -> mkString (u g) end @@ -500,7 +500,7 @@ let prim_token_uninterpreters = (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.uninterpreter) Hashtbl.t) (*******************************************************) -(* Numeral notation interpretation *) +(* Number notation interpretation *) type prim_token_notation_error = | UnexpectedTerm of Constr.t | UnexpectedNonOptionTerm of Constr.t @@ -524,21 +524,21 @@ type z_pos_ty = { z_ty : Names.inductive; pos_ty : Names.inductive } -type numeral_ty = +type number_ty = { int : int_ty; decimal : Names.inductive; hexadecimal : Names.inductive; - numeral : Names.inductive } + number : Names.inductive } type target_kind = - | Int of int_ty (* Coq.Init.Numeral.int + uint *) - | UInt of int_ty (* Coq.Init.Numeral.uint *) + | Int of int_ty (* Coq.Init.Number.int + uint *) + | UInt of int_ty (* Coq.Init.Number.uint *) | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *) - | Numeral of numeral_ty (* Coq.Init.Numeral.numeral + uint + int *) + | Number of number_ty (* Coq.Init.Number.number + uint + int *) | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *) | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *) - | Decimal of numeral_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *) + | Decimal of number_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *) type string_target_kind = | ListByte @@ -547,19 +547,36 @@ type string_target_kind = type option_kind = Option | Direct type 'target conversion_kind = 'target * option_kind +(** A postprocessing translation [to_post] can be done after execution + of the [to_ty] interpreter. The reverse translation is performed + before the [of_ty] uninterpreter. + + [to_post] is an array of [n] lists [l_i] of tuples [(f, t, + args)]. When the head symbol of the translated term matches one of + the [f] in the list [l_0] it is replaced by [t] and its arguments + are translated acording to [args] where [ToPostCopy] means that the + argument is kept unchanged and [ToPostAs k] means that the + argument is recursively translated according to [l_k]. + [ToPostHole] introduces an additional implicit argument hole + (in the reverse translation, the corresponding argument is removed). + [ToPostCheck r] behaves as [ToPostCopy] except in the reverse + translation which fails if the copied term is not [r]. + When [n] is null, no translation is performed. *) +type to_post_arg = ToPostCopy | ToPostAs of int | ToPostHole | ToPostCheck of GlobRef.t type ('target, 'warning) prim_token_notation_obj = { to_kind : 'target conversion_kind; to_ty : GlobRef.t; + to_post : ((GlobRef.t * GlobRef.t * to_post_arg list) list) array; of_kind : 'target conversion_kind; of_ty : GlobRef.t; ty_name : Libnames.qualid; (* for warnings / error messages *) warning : 'warning } -type numeral_notation_obj = (target_kind, numnot_option) prim_token_notation_obj +type number_notation_obj = (target_kind, numnot_option) prim_token_notation_obj type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj module PrimTokenNotation = struct -(** * Code shared between Numeral notation and String notation *) +(** * Code shared between Number notation and String notation *) (** Reduction The constr [c] below isn't necessarily well-typed, since we @@ -593,22 +610,69 @@ exception NotAValidPrimToken to [constr] for the subset that concerns us. Note that if you update [constr_of_glob], you should update the - corresponding numeral notation *and* string notation doc in + corresponding number notation *and* string notation doc in doc/sphinx/user-extensions/syntax-extensions.rst that describes what it means for a term to be ground / to be able to be considered for parsing. *) -let rec constr_of_glob env sigma g = match DAst.get g with - | Glob_term.GRef (GlobRef.ConstructRef c, _) -> - let sigma,c = Evd.fresh_constructor_instance env sigma c in - sigma,mkConstructU c - | Glob_term.GRef (GlobRef.IndRef c, _) -> - let sigma,c = Evd.fresh_inductive_instance env sigma c in - sigma,mkIndU c +let constr_of_globref allow_constant env sigma = function + | GlobRef.ConstructRef c -> + let sigma,c = Evd.fresh_constructor_instance env sigma c in + sigma,mkConstructU c + | GlobRef.IndRef c -> + let sigma,c = Evd.fresh_inductive_instance env sigma c in + sigma,mkIndU c + | GlobRef.ConstRef c when allow_constant -> + let sigma,c = Evd.fresh_constant_instance env sigma c in + sigma,mkConstU c + | _ -> raise NotAValidPrimToken + +let rec constr_of_glob allow_constant to_post post env sigma g = match DAst.get g with + | Glob_term.GRef (r, _) -> + let o = List.find_opt (fun (_,r',_) -> GlobRef.equal r r') post in + begin match o with + | None -> constr_of_globref allow_constant env sigma r + | Some (r, _, a) -> + (* [g] is not a GApp so check that [post] + does not expect any actual argument + (i.e., [a] contains only ToPostHole since they mean "ignore arg") *) + if List.exists ((<>) ToPostHole) a then raise NotAValidPrimToken; + constr_of_globref true env sigma r + end | Glob_term.GApp (gc, gcl) -> - let sigma,c = constr_of_glob env sigma gc in - let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in - sigma,mkApp (c, Array.of_list cl) + let o = match DAst.get gc with + | Glob_term.GRef (r, _) -> List.find_opt (fun (_,r',_) -> GlobRef.equal r r') post + | _ -> None in + begin match o with + | None -> + let sigma,c = constr_of_glob allow_constant to_post post env sigma gc in + let sigma,cl = List.fold_left_map (constr_of_glob allow_constant to_post post env) sigma gcl in + sigma,mkApp (c, Array.of_list cl) + | Some (r, _, a) -> + let sigma,c = constr_of_globref true env sigma r in + let rec aux sigma a gcl = match a, gcl with + | [], [] -> sigma,[] + | ToPostCopy :: a, gc :: gcl -> + let sigma,c = constr_of_glob allow_constant [||] [] env sigma gc in + let sigma,cl = aux sigma a gcl in + sigma, c :: cl + | ToPostCheck r :: a, gc :: gcl -> + let () = match DAst.get gc with + | Glob_term.GRef (r', _) when GlobRef.equal r r' -> () + | _ -> raise NotAValidPrimToken in + let sigma,c = constr_of_glob true [||] [] env sigma gc in + let sigma,cl = aux sigma a gcl in + sigma, c :: cl + | ToPostAs i :: a, gc :: gcl -> + let sigma,c = constr_of_glob allow_constant to_post to_post.(i) env sigma gc in + let sigma,cl = aux sigma a gcl in + sigma, c :: cl + | ToPostHole :: post, _ :: gcl -> aux sigma post gcl + | [], _ :: _ | _ :: _, [] -> raise NotAValidPrimToken + in + let sigma,cl = aux sigma a gcl in + sigma,mkApp (c, Array.of_list cl) + end | Glob_term.GInt i -> sigma, mkInt i | Glob_term.GSort gs -> let sigma,c = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family gs) in @@ -616,6 +680,10 @@ let rec constr_of_glob env sigma g = match DAst.get g with | _ -> raise NotAValidPrimToken +let constr_of_glob to_post env sigma (Glob_term.AnyGlobConstr g) = + let post = match to_post with [||] -> [] | _ -> to_post.(0) in + constr_of_glob false to_post post env sigma g + let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with | App (c, ca) -> let c = glob_of_constr token_kind ?loc env sigma c in @@ -637,9 +705,38 @@ let no_such_prim_token uninterpreted_token_kind ?loc ty = (str ("Cannot interpret this "^uninterpreted_token_kind^" as a value of type ") ++ pr_qualid ty) -let interp_option uninterpreted_token_kind token_kind ty ?loc env sigma c = +let rec postprocess token_kind ?loc ty to_post post g = + let g', gl = match DAst.get g with Glob_term.GApp (g, gl) -> g, gl | _ -> g, [] in + let o = + match DAst.get g' with + | Glob_term.GRef (r, None) -> + List.find_opt (fun (r',_,_) -> GlobRef.equal r r') post + | _ -> None in + match o with None -> g | Some (_, r, a) -> + let rec f n a gl = match a, gl with + | [], [] -> [] + | ToPostHole :: a, gl -> + let e = Evar_kinds.ImplicitArg (r, (n, None), true) in + let h = DAst.make ?loc (Glob_term.GHole (e, Namegen.IntroAnonymous, None)) in + h :: f (n+1) a gl + | (ToPostCopy | ToPostCheck _) :: a, g :: gl -> g :: f (n+1) a gl + | ToPostAs c :: a, g :: gl -> + postprocess token_kind ?loc ty to_post to_post.(c) g :: f (n+1) a gl + | [], _::_ | _::_, [] -> + no_such_prim_token token_kind ?loc ty + in + let gl = f 1 a gl in + let g = DAst.make ?loc (Glob_term.GRef (r, None)) in + DAst.make ?loc (Glob_term.GApp (g, gl)) + +let glob_of_constr token_kind ty ?loc env sigma to_post c = + let g = glob_of_constr token_kind ?loc env sigma c in + match to_post with [||] -> g | _ -> + postprocess token_kind ?loc ty to_post to_post.(0) g + +let interp_option uninterpreted_token_kind token_kind ty ?loc env sigma to_post c = match Constr.kind c with - | App (_Some, [| _; c |]) -> glob_of_constr token_kind ?loc env sigma c + | App (_Some, [| _; c |]) -> glob_of_constr token_kind ty ?loc env sigma to_post c | App (_None, [| _ |]) -> no_such_prim_token uninterpreted_token_kind ?loc ty | x -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedNonOptionTerm c)) @@ -648,13 +745,13 @@ let uninterp_option c = | App (_Some, [| _; x |]) -> x | _ -> raise NotAValidPrimToken -let uninterp to_raw o (Glob_term.AnyGlobConstr n) = +let uninterp to_raw o n = let env = Global.env () in let sigma = Evd.from_env env in let sigma,of_ty = Evd.fresh_global env sigma o.of_ty in let of_ty = EConstr.Unsafe.to_constr of_ty in try - let sigma,n = constr_of_glob env sigma n in + let sigma,n = constr_of_glob o.to_post env sigma n in let c = eval_constr_app env sigma of_ty n in let c = if snd o.of_kind == Direct then c else uninterp_option c in Some (to_raw (fst o.of_kind, c)) @@ -675,8 +772,8 @@ let rec int63_of_pos_bigint i = (Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo)) else Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo) -module Numeral = struct -(** * Numeral notation *) +module Numbers = struct +(** * Number notation *) open PrimTokenNotation let warn_large_num = @@ -732,7 +829,7 @@ let coqint_of_rawnum inds c (sign,n) = let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in mkApp (mkConstruct (ind, pos_neg), [|uint|]) -let coqnumeral_of_rawnum inds c n = +let coqnumber_of_rawnum inds c n = let ind = match c with CDec -> inds.decimal | CHex -> inds.hexadecimal in let i, f, e = NumTok.Signed.to_int_frac_and_exponent n in let i = coqint_of_rawnum inds.int c i in @@ -744,19 +841,19 @@ let coqnumeral_of_rawnum inds c n = mkApp (mkConstruct (ind, 2), [|i; f; e|]) (* (D|Hexad)ecimalExp *) let mkDecHex ind c n = match c with - | CDec -> mkApp (mkConstruct (ind, 1), [|n|]) (* (UInt|Int|)Dec *) - | CHex -> mkApp (mkConstruct (ind, 2), [|n|]) (* (UInt|Int|)Hex *) + | CDec -> mkApp (mkConstruct (ind, 1), [|n|]) (* (UInt|Int|)Decimal *) + | CHex -> mkApp (mkConstruct (ind, 2), [|n|]) (* (UInt|Int|)Hexadecimal *) exception NonDecimal -let decimal_coqnumeral_of_rawnum inds n = +let decimal_coqnumber_of_rawnum inds n = if NumTok.Signed.classify n <> CDec then raise NonDecimal; - coqnumeral_of_rawnum inds CDec n + coqnumber_of_rawnum inds CDec n -let coqnumeral_of_rawnum inds n = +let coqnumber_of_rawnum inds n = let c = NumTok.Signed.classify n in - let n = coqnumeral_of_rawnum inds c n in - mkDecHex inds.numeral c n + let n = coqnumber_of_rawnum inds c n in + mkDecHex inds.number c n let decimal_coquint_of_rawnum inds n = if NumTok.UnsignedNat.classify n <> CDec then raise NonDecimal; @@ -806,7 +903,7 @@ let rawnum_of_coqint cl c = | _ -> raise NotAValidPrimToken) | _ -> raise NotAValidPrimToken -let rawnum_of_coqnumeral cl c = +let rawnum_of_coqnumber cl c = let of_ife i f e = let n = rawnum_of_coqint cl i in let f = try Some (rawnum_of_coquint cl f) with NotAValidPrimToken -> None in @@ -820,17 +917,17 @@ let rawnum_of_coqnumeral cl c = let destDecHex c = match Constr.kind c with | App (c,[|c'|]) -> (match Constr.kind c with - | Construct ((_,1), _) (* (UInt|Int|)Dec *) -> CDec, c' - | Construct ((_,2), _) (* (UInt|Int|)Hex *) -> CHex, c' + | Construct ((_,1), _) (* (UInt|Int|)Decimal *) -> CDec, c' + | Construct ((_,2), _) (* (UInt|Int|)Hexadecimal *) -> CHex, c' | _ -> raise NotAValidPrimToken) | _ -> raise NotAValidPrimToken -let decimal_rawnum_of_coqnumeral c = - rawnum_of_coqnumeral CDec c +let decimal_rawnum_of_coqnumber c = + rawnum_of_coqnumber CDec c -let rawnum_of_coqnumeral c = +let rawnum_of_coqnumber c = let cl, c = destDecHex c in - rawnum_of_coqnumeral cl c + rawnum_of_coqnumber cl c let decimal_rawnum_of_coquint c = rawnum_of_coquint CDec c @@ -952,9 +1049,9 @@ let interp o ?loc n = interp_int63 ?loc (NumTok.SignedNat.to_bigint n) | (Int _ | UInt _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63), _ -> no_such_prim_token "number" ?loc o.ty_name - | Numeral numeral_ty, _ -> coqnumeral_of_rawnum numeral_ty n - | Decimal numeral_ty, _ -> - (try decimal_coqnumeral_of_rawnum numeral_ty n + | Number number_ty, _ -> coqnumber_of_rawnum number_ty n + | Decimal number_ty, _ -> + (try decimal_coqnumber_of_rawnum number_ty n with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name) in let env = Global.env () in @@ -964,12 +1061,13 @@ let interp o ?loc n = match o.warning, snd o.to_kind with | Abstract threshold, Direct when NumTok.Signed.is_bigger_int_than n threshold -> warn_abstract_large_num (o.ty_name,o.to_ty); - glob_of_constr "numeral" ?loc env sigma (mkApp (to_ty,[|c|])) + assert (Array.length o.to_post = 0); + glob_of_constr "number" o.ty_name ?loc env sigma o.to_post (mkApp (to_ty,[|c|])) | _ -> let res = eval_constr_app env sigma to_ty c in match snd o.to_kind with - | Direct -> glob_of_constr "numeral" ?loc env sigma res - | Option -> interp_option "number" "numeral" o.ty_name ?loc env sigma res + | Direct -> glob_of_constr "number" o.ty_name ?loc env sigma o.to_post res + | Option -> interp_option "number" "number" o.ty_name ?loc env sigma o.to_post res let uninterp o n = PrimTokenNotation.uninterp @@ -978,10 +1076,10 @@ let uninterp o n = | (UInt _, c) -> NumTok.Signed.of_nat (rawnum_of_coquint c) | (Z _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_z c) | (Int63, c) -> NumTok.Signed.of_bigint CDec (bigint_of_int63 c) - | (Numeral _, c) -> rawnum_of_coqnumeral c + | (Number _, c) -> rawnum_of_coqnumber c | (DecimalInt _, c) -> NumTok.Signed.of_int (decimal_rawnum_of_coqint c) | (DecimalUInt _, c) -> NumTok.Signed.of_nat (decimal_rawnum_of_coquint c) - | (Decimal _, c) -> decimal_rawnum_of_coqnumeral c + | (Decimal _, c) -> decimal_rawnum_of_coqnumber c end o n end @@ -1014,11 +1112,12 @@ let coqbyte_of_string ?loc byte s = let p = if Int.equal (String.length s) 1 then int_of_char s.[0] else - if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2] - then int_of_string s - else + let n = + if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2] + then int_of_string s else 256 in + if n < 256 then n else user_err ?loc ~hdr:"coqbyte_of_string" - (str "Expects a single character or a three-digits ascii code.") in + (str "Expects a single character or a three-digit ASCII code.") in coqbyte_of_char_code byte p let coqbyte_of_char byte c = coqbyte_of_char_code byte (Char.code c) @@ -1073,8 +1172,8 @@ let interp o ?loc n = let to_ty = EConstr.Unsafe.to_constr to_ty in let res = eval_constr_app env sigma to_ty c in match snd o.to_kind with - | Direct -> glob_of_constr "string" ?loc env sigma res - | Option -> interp_option "string" "string" o.ty_name ?loc env sigma res + | Direct -> glob_of_constr "string" o.ty_name ?loc env sigma o.to_post res + | Option -> interp_option "string" "string" o.ty_name ?loc env sigma o.to_post res let uninterp o n = PrimTokenNotation.uninterp @@ -1086,21 +1185,21 @@ end (* A [prim_token_infos], which is synchronized with the document state, either contains a unique id pointing to an unsynchronized - prim token function, or a numeral notation object describing how to + prim token function, or a number notation object describing how to interpret and uninterpret. We provide [prim_token_infos] because we expect plugins to provide their own interpretation functions, - rather than going through numeral notations, which are available as + rather than going through number notations, which are available as a vernacular. *) type prim_token_interp_info = Uid of prim_token_uid - | NumeralNotation of numeral_notation_obj + | NumberNotation of number_notation_obj | StringNotation of string_notation_obj type prim_token_infos = { pt_local : bool; (** Is this interpretation local? *) pt_scope : scope_name; (** Concerned scope *) - pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *) + pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a number notation object describing (un)interp functions *) pt_required : required_module; (** Module that should be loaded first *) pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) pt_in_match : bool (** Is this prim token legal in match patterns ? *) @@ -1124,7 +1223,7 @@ let hashtbl_check_and_set allow_overwrite uid f h eq = | _ -> user_err ~hdr:"prim_token_interpreter" (str "Unique identifier " ++ str uid ++ - str " already used to register a numeral or string (un)interpreter.") + str " already used to register a number or string (un)interpreter.") let register_gen_interpretation allow_overwrite uid (interp, uninterp) = hashtbl_check_and_set @@ -1152,7 +1251,6 @@ let cache_prim_token_interpretation (_,infos) = String.Map.add sc (infos.pt_required,ptii) !prim_token_interp_infos; let add_uninterp r = let l = try GlobRef.Map.find r !prim_token_uninterp_infos with Not_found -> [] in - let l = List.remove_assoc_f String.equal sc l in prim_token_uninterp_infos := GlobRef.Map.add r ((sc,(ptii,infos.pt_in_match)) :: l) !prim_token_uninterp_infos in @@ -1225,7 +1323,7 @@ let check_required_module ?loc sc (sp,d) = (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".") -(* Look if some notation or numeral printer in [scope] can be used in +(* Look if some notation or number printer in [scope] can be used in the scope stack [scopes], and if yes, using delimiters or not *) let find_with_delimiters = function @@ -1242,7 +1340,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function | NotationInScope scope' when String.equal scope scope' -> Some (None,None) | _ -> - (* If the most recently open scope has a notation/numeral printer + (* If the most recently open scope has a notation/number printer but not the expected one then we need delimiters *) if find scope then find_with_delimiters ntn_scope @@ -1380,8 +1478,8 @@ let find_notation ntn sc = | _ -> raise Not_found let notation_of_prim_token = function - | Constrexpr.Numeral (SPlus,n) -> InConstrEntry, NumTok.Unsigned.sprint n - | Constrexpr.Numeral (SMinus,n) -> InConstrEntry, "- "^NumTok.Unsigned.sprint n + | Constrexpr.Number (SPlus,n) -> InConstrEntry, NumTok.Unsigned.sprint n + | Constrexpr.Number (SMinus,n) -> InConstrEntry, "- "^NumTok.Unsigned.sprint n | String _ -> raise Not_found let find_prim_token check_allowed ?loc p sc = @@ -1399,7 +1497,7 @@ let find_prim_token check_allowed ?loc p sc = check_required_module ?loc sc spdir; let interp = match info with | Uid uid -> Hashtbl.find prim_token_interpreters uid - | NumeralNotation o -> InnerPrimToken.RawNumInterp (Numeral.interp o) + | NumberNotation o -> InnerPrimToken.RawNumInterp (Numbers.interp o) | StringNotation o -> InnerPrimToken.StringInterp (Strings.interp o) in let pat = InnerPrimToken.do_interp ?loc interp p in @@ -1416,8 +1514,8 @@ let interp_prim_token_gen ?loc g p local_scopes = let _, info = Exninfo.capture exn in user_err ?loc ~info ~hdr:"interp_prim_token" ((match p with - | Numeral _ -> - str "No interpretation for numeral " ++ pr_notation (notation_of_prim_token p) + | Number _ -> + str "No interpretation for number " ++ pr_notation (notation_of_prim_token p) | String s -> str "No interpretation for string " ++ qs s) ++ str ".") let interp_prim_token ?loc = @@ -1667,14 +1765,14 @@ let availability_of_prim_token n printer_scope local_scopes = let uid = snd (String.Map.find scope !prim_token_interp_infos) in let open InnerPrimToken in match n, uid with - | Constrexpr.Numeral _, NumeralNotation _ -> true - | _, NumeralNotation _ -> false + | Constrexpr.Number _, NumberNotation _ -> true + | _, NumberNotation _ -> false | String _, StringNotation _ -> true | _, StringNotation _ -> false | _, Uid uid -> let interp = Hashtbl.find prim_token_interpreters uid in match n, interp with - | Constrexpr.Numeral _, (RawNumInterp _ | BigNumInterp _) -> true + | Constrexpr.Number _, (RawNumInterp _ | BigNumInterp _) -> true | String _, StringInterp _ -> true | _ -> false with Not_found -> false @@ -1689,7 +1787,7 @@ let rec find_uninterpretation need_delim def find = function def | OpenScopeItem scope :: scopes -> (try find need_delim scope - with Not_found -> find_uninterpretation need_delim def find scopes) (* TODO: here we should also update the need_delim list with all regular notations in scope [scope] that could shadow a numeral notation *) + with Not_found -> find_uninterpretation need_delim def find scopes) (* TODO: here we should also update the need_delim list with all regular notations in scope [scope] that could shadow a number notation *) | LonelyNotationItem ntn::scopes -> find_uninterpretation (ntn::need_delim) def find scopes @@ -1701,7 +1799,7 @@ let uninterp_prim_token c local_scopes = try let uninterp = match info with | Uid uid -> Hashtbl.find prim_token_uninterpreters uid - | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o) + | NumberNotation o -> InnerPrimToken.RawNumUninterp (Numbers.uninterp o) | StringNotation o -> InnerPrimToken.StringUninterp (Strings.uninterp o) in match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with |