aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr_ops.ml7
-rw-r--r--interp/constrextern.ml13
-rw-r--r--interp/constrintern.ml119
-rw-r--r--interp/dumpglob.mli1
-rw-r--r--interp/modintern.ml9
-rw-r--r--interp/notation.ml272
-rw-r--r--interp/notation.mli32
-rw-r--r--interp/numTok.ml188
-rw-r--r--interp/numTok.mli52
-rw-r--r--interp/smartlocate.ml16
-rw-r--r--interp/syntax_def.ml16
-rw-r--r--interp/syntax_def.mli8
12 files changed, 495 insertions, 238 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index d6097304ec..3d99e1d227 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -15,8 +15,8 @@ open Nameops
open Libnames
open Namegen
open Glob_term
-open Constrexpr
open Notation
+open Constrexpr
(***********************)
(* For binders parsing *)
@@ -618,8 +618,9 @@ let interp_univ_constraints env evd cstrs =
let cstrs' = Univ.Constraint.add cstr cstrs in
try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
evd, cstrs'
- with Univ.UniverseInconsistency e ->
- CErrors.user_err ~hdr:"interp_constraint"
+ with Univ.UniverseInconsistency e as exn ->
+ let _, info = Exninfo.capture exn in
+ CErrors.user_err ~hdr:"interp_constraint" ~info
(Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e)
in
List.fold_left interp (evd,Univ.Constraint.empty) cstrs
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d5a5bde616..63079993c8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -19,13 +19,13 @@ open Libnames
open Namegen
open Impargs
open CAst
+open Notation
open Constrexpr
open Constrexpr_ops
open Notation_ops
open Glob_term
open Glob_ops
open Pattern
-open Notation
open Detyping
module NamedDecl = Context.Named.Declaration
@@ -836,7 +836,7 @@ let rec flatten_application c = match DAst.get c with
let same_binder_type ty nal c =
match nal, DAst.get c with
- | _::_, GProd (_,_,ty',_) -> glob_constr_eq ty ty'
+ | _::_, (GProd (_,_,ty',_) | GLambda (_,_,ty',_)) -> glob_constr_eq ty ty'
| [], _ -> true
| _ -> assert false
@@ -888,12 +888,19 @@ let q_infinity () = qualid_of_ref "num.float.infinity"
let q_neg_infinity () = qualid_of_ref "num.float.neg_infinity"
let q_nan () = qualid_of_ref "num.float.nan"
+let get_printing_float = Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Printing";"Float"]
+ ~value:true
+
let extern_float f scopes =
if Float64.is_nan f then CRef(q_nan (), None)
else if Float64.is_infinity f then CRef(q_infinity (), None)
else if Float64.is_neg_infinity f then CRef(q_neg_infinity (), None)
else
- let s = Float64.(to_string f) in
+ let s =
+ let hex = !Flags.raw_print || not (get_printing_float ()) in
+ if hex then Float64.to_hex_string f else Float64.to_string f in
let n = NumTok.Signed.of_string s in
extern_prim_token_delimiter_if_required (Numeral n)
"float" "float_scope" scopes
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f82783f47d..ee041ed088 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -115,7 +115,7 @@ type internalization_error =
| NotAProjectionOf of qualid * qualid
| ProjectionsOfDifferentRecords of qualid * qualid
-exception InternalizationError of internalization_error Loc.located
+exception InternalizationError of internalization_error
let explain_variable_capture id id' =
Id.print id ++ str " is dependent in the type of " ++ Id.print id' ++
@@ -164,8 +164,13 @@ let explain_internalization_error e =
explain_projections_of_diff_records inductive1_id inductive2_id
in pp ++ str "."
-let error_bad_inductive_type ?loc =
- user_err ?loc (str
+let _ = CErrors.register_handler (function
+ | InternalizationError e ->
+ Some (explain_internalization_error e)
+ | _ -> None)
+
+let error_bad_inductive_type ?loc ?info () =
+ user_err ?loc ?info (str
"This should be an inductive type applied to patterns.")
let error_parameter_not_implicit ?loc =
@@ -187,7 +192,7 @@ let empty_internalization_env = Id.Map.empty
let compute_internalization_data env sigma id ty typ impl =
let impl = compute_implicits_with_manual env sigma typ (is_implicit_args()) impl in
- (ty, impl, compute_arguments_scope sigma typ, var_uid id)
+ (ty, impl, compute_arguments_scope env sigma typ, var_uid id)
let compute_internalization_env env sigma ?(impls=empty_internalization_env) ty =
List.fold_left3
@@ -368,7 +373,7 @@ let impls_term_list n ?(args = []) =
(* Check if in binder "(x1 x2 .. xn : t)", none of x1 .. xn-1 occurs in t *)
let rec check_capture ty = let open CAst in function
| { loc; v = Name id } :: { v = Name id' } :: _ when occur_glob_constr id ty ->
- raise (InternalizationError (loc,VariableCapture (id,id')))
+ Loc.raise ?loc (InternalizationError (VariableCapture (id,id')))
| _::nal ->
check_capture ty nal
| [] ->
@@ -976,10 +981,6 @@ let split_by_type_pat ?loc ids subst =
assert (terms = [] && termlists = []);
subst
-let make_subst ids l =
- let fold accu (id, scopes) a = Id.Map.add id (a, scopes) accu in
- List.fold_left2 fold Id.Map.empty ids l
-
let intern_notation intern env ntnvars loc ntn fullargs =
(* Adjust to parsing of { } *)
let ntn,fullargs = contract_curly_brackets ntn fullargs in
@@ -1090,7 +1091,9 @@ let intern_extended_global_of_qualid qid =
let intern_reference qid =
let r =
try intern_extended_global_of_qualid qid
- with Not_found -> Nametab.error_global_not_found qid
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info qid
in
Smartlocate.global_of_extended_global r
@@ -1113,8 +1116,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
if List.length args < nids then error_not_enough_arguments ?loc;
let args1,args2 = List.chop nids args in
check_no_explicitation args1;
- let terms = make_subst ids (List.map fst args1) in
- let subst = (terms, Id.Map.empty, Id.Map.empty, Id.Map.empty) in
+ let subst = split_by_type ids (List.map fst args1,[],[],[]) in
let infos = (Id.Map.empty, env) in
let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in
let loc = c.loc in
@@ -1175,16 +1177,20 @@ let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us
let r, realref, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in
check_applied_projection isproj realref qid;
find_appl_head_data r, args2
- with Not_found ->
+ with Not_found as exn ->
(* Extra allowance for non globalizing functions *)
if !interning_grammar || env.unb then
(* check_applied_projection ?? *)
(gvar (loc,qualid_basename qid) us, [], []), args
- else Nametab.error_global_not_found qid
+ else
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info qid
else
let r,realref,args2 =
try intern_qualid qid intern env ntnvars us args
- with Not_found -> Nametab.error_global_not_found qid
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info qid
in
check_applied_projection isproj realref qid;
find_appl_head_data r, args2
@@ -1258,14 +1264,16 @@ let loc_of_lhs lhs =
let check_linearity lhs ids =
match has_duplicate ids with
| Some id ->
- raise (InternalizationError (loc_of_lhs lhs,NonLinearPattern id))
+ let loc = loc_of_lhs lhs in
+ Loc.raise ?loc (InternalizationError (NonLinearPattern id))
| None ->
()
(* Match the number of pattern against the number of matched args *)
let check_number_of_pattern loc n l =
let p = List.length l in
- if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p)))
+ if not (Int.equal n p) then
+ Loc.raise ?loc (InternalizationError (BadPatternsNumber (n,p)))
let check_or_pat_variables loc ids idsl =
let eq_id {v=id} {v=id'} = Id.equal id id' in
@@ -1397,7 +1405,7 @@ let find_constructor loc add_params ref =
let find_pattern_variable qid =
if qualid_is_ident qid then qualid_basename qid
- else raise (InternalizationError(qid.CAst.loc,NotAConstructor qid))
+ else Loc.raise ?loc:qid.CAst.loc (InternalizationError(NotAConstructor qid))
let check_duplicate ?loc fields =
let eq (ref1, _) (ref2, _) = qualid_eq ref1 ref2 in
@@ -1434,8 +1442,10 @@ let sort_fields ~complete loc fields completer =
let gr = locate_reference first_field_ref in
Dumpglob.add_glob ?loc:first_field_ref.CAst.loc gr;
(gr, Recordops.find_projection gr)
- with Not_found ->
- raise (InternalizationError(first_field_ref.CAst.loc, NotAProjection first_field_ref))
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ let info = Option.cata (Loc.add_loc info) info loc in
+ Exninfo.iraise (InternalizationError(NotAProjection first_field_ref), info)
in
(* the number of parameters *)
let nparams = record.Recordops.s_EXPECTEDPARAM in
@@ -1470,10 +1480,10 @@ let sort_fields ~complete loc fields completer =
try Recordops.find_projection field_glob_ref
with Not_found ->
let inductive_ref = inductive_of_record floc record in
- raise (InternalizationError(floc, NotAProjectionOf (field_ref, inductive_ref))) in
+ Loc.raise ?loc:floc (InternalizationError(NotAProjectionOf (field_ref, inductive_ref))) in
let ind1 = inductive_of_record floc record in
let ind2 = inductive_of_record floc this_field_record in
- raise (InternalizationError(loc, ProjectionsOfDifferentRecords (ind1, ind2)))
+ Loc.raise ?loc (InternalizationError(ProjectionsOfDifferentRecords (ind1, ind2)))
in
if not regular && complete then
(* "regular" is false when the field is defined
@@ -1624,8 +1634,8 @@ let drop_notations_pattern looked_for genv =
let nvars = List.length vars in
if List.length pats < nvars then error_not_enough_arguments ?loc:qid.loc;
let pats1,pats2 = List.chop nvars pats in
- let subst = make_subst vars pats1 in
- let idspl1 = List.map (in_not false qid.loc scopes (subst, Id.Map.empty) []) args in
+ let subst = split_by_type_pat vars (pats1,[]) in
+ let idspl1 = List.map (in_not false qid.loc scopes subst []) args in
let (_,argscs) = find_remaining_scopes pats1 pats2 g in
Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2)
| _ -> raise Not_found
@@ -1660,12 +1670,16 @@ let drop_notations_pattern looked_for genv =
begin
match drop_syndef top scopes head pl with
| Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
- | None -> raise (InternalizationError (loc,NotAConstructor head))
+ | None -> Loc.raise ?loc (InternalizationError (NotAConstructor head))
end
| CPatCstr (qid, Some expl_pl, pl) ->
- let g = try Nametab.locate qid
- with Not_found ->
- raise (InternalizationError (loc,NotAConstructor qid)) in
+ let g =
+ try Nametab.locate qid
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ let info = Option.cata (Loc.add_loc info) info loc in
+ Exninfo.iraise (InternalizationError (NotAConstructor qid), info)
+ in
if expl_pl == [] then
(* Convention: (@r) deactivates all further implicit arguments and scopes *)
DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
@@ -1815,20 +1829,22 @@ let intern_ind_pattern genv ntnvars scopes pat =
let no_not =
try
drop_notations_pattern (function (GlobRef.IndRef _ | GlobRef.ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat
- with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ?loc
+ with InternalizationError(NotAConstructor _) as exn ->
+ let _, info = Exninfo.capture exn in
+ error_bad_inductive_type ~info ()
in
let loc = no_not.CAst.loc in
match DAst.get no_not with
| RCPatCstr (head, expl_pl, pl) ->
- let c = (function GlobRef.IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in
+ let c = (function GlobRef.IndRef ind -> ind | _ -> error_bad_inductive_type ?loc ()) head in
let with_letin, pl2 = add_implicits_check_ind_length genv loc c
(List.length expl_pl) pl in
let idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in
(with_letin,
match product_of_cases_patterns empty_alias idslpl with
| ids,[asubst,pl] -> (c,ids,asubst,chop_params_pattern loc c pl with_letin)
- | _ -> error_bad_inductive_type ?loc)
- | x -> error_bad_inductive_type ?loc
+ | _ -> error_bad_inductive_type ?loc ())
+ | x -> error_bad_inductive_type ?loc ()
(**********************************************************************)
(* Utilities for application *)
@@ -1904,8 +1920,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let dl = Array.of_list dl in
let n =
try List.index0 Id.equal iddef lf
- with Not_found ->
- raise (InternalizationError (locid,UnboundFixName (false,iddef)))
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ let info = Option.cata (Loc.add_loc info) info locid in
+ Exninfo.iraise (InternalizationError (UnboundFixName (false,iddef)),info)
in
let env = restart_lambda_binders env in
let idl_temp = Array.map
@@ -1947,8 +1965,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let dl = Array.of_list dl in
let n =
try List.index0 Id.equal iddef lf
- with Not_found ->
- raise (InternalizationError (locid,UnboundFixName (true,iddef)))
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ let info = Option.cata (Loc.add_loc info) info locid in
+ Exninfo.iraise (InternalizationError (UnboundFixName (true,iddef)), info)
in
let env = restart_lambda_binders env in
let idl_tmp = Array.map
@@ -2176,7 +2196,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
DAst.make ?loc @@
GEvar (n, List.map (on_snd (intern_no_implicit env)) l)
| CPatVar _ ->
- raise (InternalizationError (loc,IllegalMetavariable))
+ Loc.raise ?loc (InternalizationError IllegalMetavariable)
(* end *)
| CSort s ->
DAst.make ?loc @@
@@ -2342,12 +2362,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
(intern_no_implicit enva a) :: (intern_args env subscopes args)
in
- try
- intern env c
- with
- InternalizationError (loc,e) ->
- user_err ?loc ~hdr:"internalize"
- (explain_internalization_error e)
+ intern env c
(**************************************************************************)
(* Functions to translate constr_expr into glob_constr *)
@@ -2358,9 +2373,9 @@ let extract_ids env =
(Termops.ids_of_rel_context (Environ.rel_context env))
Id.Set.empty
-let scope_of_type_kind sigma = function
+let scope_of_type_kind env sigma = function
| IsType -> Notation.current_type_scope_name ()
- | OfType typ -> compute_type_scope sigma typ
+ | OfType typ -> compute_type_scope env sigma typ
| WithoutTypeConstraint | UnknownIfTermOrType -> None
let allowed_binder_kind_of_type_kind = function
@@ -2377,7 +2392,7 @@ let empty_ltac_sign = {
let intern_gen kind env sigma
?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
c =
- let tmp_scope = scope_of_type_kind sigma kind in
+ let tmp_scope = scope_of_type_kind env sigma kind in
let k = allowed_binder_kind_of_type_kind kind in
internalize env {ids = extract_ids env; unb = false;
tmp_scope = tmp_scope; scopes = [];
@@ -2387,12 +2402,7 @@ let intern_gen kind env sigma
let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c
let intern_type env sigma c = intern_gen IsType env sigma c
let intern_pattern globalenv patt =
- try
- intern_cases_pattern globalenv Id.Map.empty (None,[]) empty_alias patt
- with
- InternalizationError (loc,e) ->
- user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
-
+ intern_cases_pattern globalenv Id.Map.empty (None,[]) empty_alias patt
(*********************************************************************)
(* Functions to parse and interpret constructions *)
@@ -2462,7 +2472,7 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign)
let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
{ Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c =
- let tmp_scope = scope_of_type_kind sigma kind in
+ let tmp_scope = scope_of_type_kind env sigma kind in
let impls = empty_internalization_env in
let k = allowed_binder_kind_of_type_kind kind in
internalize env
@@ -2505,7 +2515,6 @@ let my_intern_constr env lvar acc c =
internalize env acc false lvar c
let intern_context env impl_env binders =
- try
let lvar = (empty_ltac_sign, Id.Map.empty) in
let ids =
(* We assume all ids around are parts of the prefix of the current
@@ -2519,8 +2528,6 @@ let intern_context env impl_env binders =
tmp_scope = None; scopes = []; impls = impl_env;
binder_block_names = Some (Some AbsPi,ids)}, []) binders in
(lenv.impls, List.map glob_local_binder_of_extended bl)
- with InternalizationError (loc,e) ->
- user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
let open EConstr in
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 14e5a81308..be1e3f05d2 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -49,3 +49,4 @@ val type_of_global_ref : Names.GlobRef.t -> string
(** Registration of constant information *)
val add_constant_kind : Names.Constant.t -> Decls.logical_kind -> unit
+val constant_kind : Names.Constant.t -> Decls.logical_kind
diff --git a/interp/modintern.ml b/interp/modintern.ml
index ae152e1c1c..50f90ebea7 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -22,14 +22,15 @@ exception ModuleInternalizationError of module_internalization_error
type module_kind = Module | ModType | ModAny
-let error_not_a_module_loc kind loc qid =
+let error_not_a_module_loc ~info kind loc qid =
let s = string_of_qualid qid in
let e = match kind with
| Module -> Modops.ModuleTypingError (Modops.NotAModule s)
| ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s)
| ModAny -> ModuleInternalizationError (NotAModuleNorModtype s)
in
- Loc.raise ?loc e
+ let info = Option.cata (Loc.add_loc info) info loc in
+ Exninfo.iraise (e,info)
let error_application_to_not_path loc me =
Loc.raise ?loc (Modops.ModuleTypingError (Modops.ApplicationToNotPath me))
@@ -57,7 +58,9 @@ let lookup_module_or_modtype kind qid =
if kind == Module then raise Not_found;
let mp = Nametab.locate_modtype qid in
Dumpglob.dump_modref ?loc mp "mod"; (mp,ModType)
- with Not_found -> error_not_a_module_loc kind loc qid
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ error_not_a_module_loc ~info kind loc qid
let lookup_module lqid = fst (lookup_module_or_modtype Module lqid)
diff --git a/interp/notation.ml b/interp/notation.ml
index 7761606f11..d4a44d9622 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -125,13 +125,14 @@ let declare_scope scope =
with Not_found ->
scope_map := String.Map.add scope empty_scope !scope_map
-let error_unknown_scope sc =
- user_err ~hdr:"Notation"
+let error_unknown_scope ~info sc =
+ user_err ~hdr:"Notation" ~info
(str "Scope " ++ str sc ++ str " is not declared.")
let find_scope ?(tolerant=false) scope =
try String.Map.find scope !scope_map
- with Not_found ->
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
if tolerant then
(* tolerant mode to be turn off after deprecation phase *)
begin
@@ -140,7 +141,7 @@ let find_scope ?(tolerant=false) scope =
empty_scope
end
else
- error_unknown_scope scope
+ error_unknown_scope ~info scope
let check_scope ?(tolerant=false) scope =
let _ = find_scope ~tolerant scope in ()
@@ -158,7 +159,9 @@ let normalize_scope sc =
try
let sc = String.Map.find sc !delimiters_map in
let _ = String.Map.find sc !scope_map in sc
- with Not_found -> error_unknown_scope sc
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ error_unknown_scope ~info sc
(**********************************************************************)
(* The global stack of scopes *)
@@ -257,8 +260,10 @@ let remove_delimiters scope =
try
let _ = ignore (String.Map.find key !delimiters_map) in
delimiters_map := String.Map.remove key !delimiters_map
- with Not_found ->
- assert false (* A delimiter for scope [scope] should exist *)
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ (* XXX info *)
+ CErrors.anomaly ~info (str "A delimiter for scope [scope] should exist")
let find_delimiters_scope ?loc key =
try String.Map.find key !delimiters_map
@@ -382,7 +387,7 @@ module InnerPrimToken = struct
| _ -> false
let mkNumeral n =
- Numeral (NumTok.Signed.of_bigint n)
+ Numeral (NumTok.Signed.of_bigint CDec n)
let mkString = function
| None -> None
@@ -423,23 +428,32 @@ type numnot_option =
| Abstract of NumTok.UnsignedNat.t
type int_ty =
- { uint : Names.inductive;
+ { dec_uint : Names.inductive;
+ dec_int : Names.inductive;
+ hex_uint : Names.inductive;
+ hex_int : Names.inductive;
+ uint : Names.inductive;
int : Names.inductive }
type z_pos_ty =
{ z_ty : Names.inductive;
pos_ty : Names.inductive }
-type decimal_ty =
+type numeral_ty =
{ int : int_ty;
- decimal : Names.inductive }
+ decimal : Names.inductive;
+ hexadecimal : Names.inductive;
+ numeral : Names.inductive }
type target_kind =
- | Int of int_ty (* Coq.Init.Decimal.int + uint *)
- | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
+ | Int of int_ty (* Coq.Init.Numeral.int + uint *)
+ | UInt of int_ty (* Coq.Init.Numeral.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 *)
+ | Numeral of numeral_ty (* Coq.Init.Numeral.numeral + 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) *)
type string_target_kind =
| ListByte
@@ -601,17 +615,23 @@ let warn_abstract_large_num =
(** Decimal.Nil has index 1, then Decimal.D0 has index 2 .. Decimal.D9 is 11 *)
let digit_of_char c =
- assert ('0' <= c && c <= '9');
- Char.code c - Char.code '0' + 2
+ assert ('0' <= c && c <= '9' || 'a' <= c && c <= 'f');
+ if c <= '9' then Char.code c - Char.code '0' + 2
+ else Char.code c - Char.code 'a' + 12
let char_of_digit n =
- assert (2<=n && n<=11);
- Char.chr (n-2 + Char.code '0')
+ assert (2<=n && n<=17);
+ if n <= 11 then Char.chr (n-2 + Char.code '0')
+ else Char.chr (n-12 + Char.code 'a')
-let coquint_of_rawnum uint n =
+let coquint_of_rawnum inds c n =
+ let uint = match c with CDec -> inds.dec_uint | CHex -> inds.hex_uint in
let nil = mkConstruct (uint,1) in
match n with None -> nil | Some n ->
let str = NumTok.UnsignedNat.to_string n in
+ let str = match c with
+ | CDec -> str
+ | CHex -> String.sub str 2 (String.length str - 2) in (* cut "0x" *)
let rec do_chars s i acc =
if i < 0 then acc
else
@@ -620,61 +640,126 @@ let coquint_of_rawnum uint n =
in
do_chars str (String.length str - 1) nil
-let coqint_of_rawnum inds (sign,n) =
- let uint = coquint_of_rawnum inds.uint (Some n) in
+let coqint_of_rawnum inds c (sign,n) =
+ let ind = match c with CDec -> inds.dec_int | CHex -> inds.hex_int in
+ let uint = coquint_of_rawnum inds c (Some n) in
let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in
- mkApp (mkConstruct (inds.int, pos_neg), [|uint|])
+ mkApp (mkConstruct (ind, pos_neg), [|uint|])
-let coqdecimal_of_rawnum inds n =
- let i, f, e = NumTok.Signed.to_decimal_and_exponent n in
- let i = coqint_of_rawnum inds.int i in
- let f = coquint_of_rawnum inds.int.uint f in
+let coqnumeral_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
+ let f = coquint_of_rawnum inds.int c f in
match e with
- | None -> mkApp (mkConstruct (inds.decimal, 1), [|i; f|]) (* Decimal *)
+ | None -> mkApp (mkConstruct (ind, 1), [|i; f|]) (* (D|Hexad)ecimal *)
| Some e ->
- let e = coqint_of_rawnum inds.int e in
- mkApp (mkConstruct (inds.decimal, 2), [|i; f; e|]) (* DecimalExp *)
+ let e = coqint_of_rawnum inds.int CDec e in
+ mkApp (mkConstruct (ind, 2), [|i; f; e|]) (* (D|Hexad)ecimalExp *)
-let rawnum_of_coquint c =
+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 *)
+
+exception NonDecimal
+
+let decimal_coqnumeral_of_rawnum inds n =
+ if NumTok.Signed.classify n <> CDec then raise NonDecimal;
+ coqnumeral_of_rawnum inds CDec n
+
+let coqnumeral_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 decimal_coquint_of_rawnum inds n =
+ if NumTok.UnsignedNat.classify n <> CDec then raise NonDecimal;
+ coquint_of_rawnum inds CDec (Some n)
+
+let coquint_of_rawnum inds n =
+ let c = NumTok.UnsignedNat.classify n in
+ let n = coquint_of_rawnum inds c (Some n) in
+ mkDecHex inds.uint c n
+
+let decimal_coqint_of_rawnum inds n =
+ if NumTok.SignedNat.classify n <> CDec then raise NonDecimal;
+ coqint_of_rawnum inds CDec n
+
+let coqint_of_rawnum inds n =
+ let c = NumTok.SignedNat.classify n in
+ let n = coqint_of_rawnum inds c n in
+ mkDecHex inds.int c n
+
+let rawnum_of_coquint cl c =
let rec of_uint_loop c buf =
match Constr.kind c with
| Construct ((_,1), _) (* Nil *) -> ()
| App (c, [|a|]) ->
(match Constr.kind c with
- | Construct ((_,n), _) (* D0 to D9 *) ->
+ | Construct ((_,n), _) (* D0 to Df *) ->
let () = Buffer.add_char buf (char_of_digit n) in
of_uint_loop a buf
| _ -> raise NotAValidPrimToken)
| _ -> raise NotAValidPrimToken
in
let buf = Buffer.create 64 in
+ if cl = CHex then (Buffer.add_char buf '0'; Buffer.add_char buf 'x');
let () = of_uint_loop c buf in
- if Int.equal (Buffer.length buf) 0 then
+ if Int.equal (Buffer.length buf) (match cl with CDec -> 0 | CHex -> 2) then
(* To avoid ambiguities between Nil and (D0 Nil), we choose
to not display Nil alone as "0" *)
raise NotAValidPrimToken
else NumTok.UnsignedNat.of_string (Buffer.contents buf)
-let rawnum_of_coqint c =
+let rawnum_of_coqint cl c =
match Constr.kind c with
| App (c,[|c'|]) ->
(match Constr.kind c with
- | Construct ((_,1), _) (* Pos *) -> (SPlus,rawnum_of_coquint c')
- | Construct ((_,2), _) (* Neg *) -> (SMinus,rawnum_of_coquint c')
+ | Construct ((_,1), _) (* Pos *) -> (SPlus,rawnum_of_coquint cl c')
+ | Construct ((_,2), _) (* Neg *) -> (SMinus,rawnum_of_coquint cl c')
| _ -> raise NotAValidPrimToken)
| _ -> raise NotAValidPrimToken
-let rawnum_of_decimal c =
+let rawnum_of_coqnumeral cl c =
let of_ife i f e =
- let n = rawnum_of_coqint i in
- let f = try Some (rawnum_of_coquint f) with NotAValidPrimToken -> None in
- let e = match e with None -> None | Some e -> Some (rawnum_of_coqint e) in
- NumTok.Signed.of_decimal_and_exponent n f e in
+ let n = rawnum_of_coqint cl i in
+ let f = try Some (rawnum_of_coquint cl f) with NotAValidPrimToken -> None in
+ let e = match e with None -> None | Some e -> Some (rawnum_of_coqint CDec e) in
+ NumTok.Signed.of_int_frac_and_exponent n f e in
match Constr.kind c with
| App (_,[|i; f|]) -> of_ife i f None
| App (_,[|i; f; e|]) -> of_ife i f (Some e)
| _ -> raise NotAValidPrimToken
+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'
+ | _ -> raise NotAValidPrimToken)
+ | _ -> raise NotAValidPrimToken
+
+let decimal_rawnum_of_coqnumeral c =
+ rawnum_of_coqnumeral CDec c
+
+let rawnum_of_coqnumeral c =
+ let cl, c = destDecHex c in
+ rawnum_of_coqnumeral cl c
+
+let decimal_rawnum_of_coquint c =
+ rawnum_of_coquint CDec c
+
+let rawnum_of_coquint c =
+ let cl, c = destDecHex c in
+ rawnum_of_coquint cl c
+
+let decimal_rawnum_of_coqint c =
+ rawnum_of_coqint CDec c
+
+let rawnum_of_coqint c =
+ let cl, c = destDecHex c in
+ rawnum_of_coqint cl c
+
(***********************************************************************)
(** ** Conversion between Coq [Z] and internal bigint *)
@@ -768,15 +853,24 @@ let interp o ?loc n =
let c = match fst o.to_kind, NumTok.Signed.to_int n with
| Int int_ty, Some n ->
coqint_of_rawnum int_ty n
- | UInt uint_ty, Some (SPlus, n) ->
- coquint_of_rawnum uint_ty (Some n)
+ | UInt int_ty, Some (SPlus, n) ->
+ coquint_of_rawnum int_ty n
+ | DecimalInt int_ty, Some n ->
+ (try decimal_coqint_of_rawnum int_ty n
+ with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
+ | DecimalUInt int_ty, Some (SPlus, n) ->
+ (try decimal_coquint_of_rawnum int_ty n
+ with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
| Z z_pos_ty, Some n ->
z_of_bigint z_pos_ty (NumTok.SignedNat.to_bigint n)
| Int63, Some n ->
interp_int63 ?loc (NumTok.SignedNat.to_bigint n)
- | (Int _ | UInt _ | Z _ | Int63), _ ->
+ | (Int _ | UInt _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63), _ ->
no_such_prim_token "number" ?loc o.ty_name
- | Decimal decimal_ty, _ -> coqdecimal_of_rawnum decimal_ty n
+ | Numeral numeral_ty, _ -> coqnumeral_of_rawnum numeral_ty n
+ | Decimal numeral_ty, _ ->
+ (try decimal_coqnumeral_of_rawnum numeral_ty n
+ with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
in
let env = Global.env () in
let sigma = Evd.from_env env in
@@ -797,9 +891,12 @@ let uninterp o n =
begin function
| (Int _, c) -> NumTok.Signed.of_int (rawnum_of_coqint c)
| (UInt _, c) -> NumTok.Signed.of_nat (rawnum_of_coquint c)
- | (Z _, c) -> NumTok.Signed.of_bigint (bigint_of_z c)
- | (Int63, c) -> NumTok.Signed.of_bigint (bigint_of_int63 c)
- | (Decimal _, c) -> rawnum_of_decimal 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
+ | (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
end o n
end
@@ -1031,12 +1128,17 @@ let declare_string_interpreter ?(local=false) sc dir interp (patl,uninterp,b) =
let check_required_module ?loc sc (sp,d) =
try let _ = Nametab.global_of_path sp in ()
- with Not_found ->
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
match d with
- | [] -> user_err ?loc ~hdr:"prim_token_interpreter"
- (str "Cannot interpret in " ++ str sc ++ str " because " ++ pr_path sp ++ str " could not be found in the current environment.")
- | _ -> user_err ?loc ~hdr:"prim_token_interpreter"
- (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
+ | [] ->
+ user_err ?loc ~info ~hdr:"prim_token_interpreter"
+ (str "Cannot interpret in " ++ str sc ++ str " because " ++ pr_path sp ++
+ str " could not be found in the current environment.")
+ | _ ->
+ user_err ?loc ~info ~hdr:"prim_token_interpreter"
+ (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
the scope stack [scopes], and if yes, using delimiters or not *)
@@ -1126,8 +1228,8 @@ let find_notation ntn sc =
NotationMap.find ntn (find_scope sc).notations
let notation_of_prim_token = function
- | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.Unsigned.sprint n
- | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.Unsigned.sprint n
+ | Constrexpr.Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.Unsigned.sprint n
+ | Constrexpr.Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.Unsigned.sprint n
| String _ -> raise Not_found
let find_prim_token check_allowed ?loc p sc =
@@ -1158,8 +1260,9 @@ let interp_prim_token_gen ?loc g p local_scopes =
try
let (pat,loc), sc = find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes in
pat, (loc,sc)
- with Not_found ->
- user_err ?loc ~hdr:"interp_prim_token"
+ with Not_found as exn ->
+ 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)
@@ -1192,9 +1295,10 @@ let interp_notation ?loc ntn local_scopes =
let (n,sc) = find_interpretation ntn (find_notation ntn) scopes in
Option.iter (fun d -> warn_deprecated_notation ?loc (ntn,d)) n.not_deprecation;
n.not_interp, (n.not_location, sc)
- with Not_found ->
- user_err ?loc
- (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ user_err ?loc ~info
+ (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
let uninterp_notations c =
List.map_append (fun key -> keymap_find key !notations_key_table)
@@ -1333,14 +1437,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
- | Numeral _, NumeralNotation _ -> true
+ | Constrexpr.Numeral _, NumeralNotation _ -> true
| _, NumeralNotation _ -> false
| String _, StringNotation _ -> true
| _, StringNotation _ -> false
| _, Uid uid ->
let interp = Hashtbl.find prim_token_interpreters uid in
match n, interp with
- | Numeral _, (RawNumInterp _ | BigNumInterp _) -> true
+ | Constrexpr.Numeral _, (RawNumInterp _ | BigNumInterp _) -> true
| String _, StringInterp _ -> true
| _ -> false
with Not_found -> false
@@ -1448,8 +1552,8 @@ type scope_class = cl_typ
let scope_class_compare : scope_class -> scope_class -> int =
cl_typ_ord
-let compute_scope_class sigma t =
- let (cl,_,_) = find_class_type sigma t in
+let compute_scope_class env sigma t =
+ let (cl,_,_) = find_class_type env sigma t in
cl
module ScopeClassOrd =
@@ -1478,22 +1582,23 @@ let find_scope_class_opt = function
(**********************************************************************)
(* Special scopes associated to arguments of a global reference *)
-let rec compute_arguments_classes sigma t =
- match EConstr.kind sigma (Reductionops.whd_betaiotazeta sigma t) with
- | Prod (_,t,u) ->
- let cl = try Some (compute_scope_class sigma t) with Not_found -> None in
- cl :: compute_arguments_classes sigma u
+let rec compute_arguments_classes env sigma t =
+ match EConstr.kind sigma (Reductionops.whd_betaiotazeta env sigma t) with
+ | Prod (na, t, u) ->
+ let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum (na, t)) env in
+ let cl = try Some (compute_scope_class env sigma t) with Not_found -> None in
+ cl :: compute_arguments_classes env sigma u
| _ -> []
-let compute_arguments_scope_full sigma t =
- let cls = compute_arguments_classes sigma t in
+let compute_arguments_scope_full env sigma t =
+ let cls = compute_arguments_classes env sigma t in
let scs = List.map find_scope_class_opt cls in
scs, cls
-let compute_arguments_scope sigma t = fst (compute_arguments_scope_full sigma t)
+let compute_arguments_scope env sigma t = fst (compute_arguments_scope_full env sigma t)
-let compute_type_scope sigma t =
- find_scope_class_opt (try Some (compute_scope_class sigma t) with Not_found -> None)
+let compute_type_scope env sigma t =
+ find_scope_class_opt (try Some (compute_scope_class env sigma t) with Not_found -> None)
let current_type_scope_name () =
find_scope_class_opt (Some CL_SORT)
@@ -1531,15 +1636,16 @@ let load_arguments_scope _ (_,(_,r,n,scl,cls)) =
let cache_arguments_scope o =
load_arguments_scope 1 o
-let subst_scope_class subst cs =
- try Some (subst_cl_typ subst cs) with Not_found -> None
+let subst_scope_class env subst cs =
+ try Some (subst_cl_typ env subst cs) with Not_found -> None
let subst_arguments_scope (subst,(req,r,n,scl,cls)) =
let r' = fst (subst_global subst r) in
let subst_cl ocl = match ocl with
| None -> ocl
| Some cl ->
- match subst_scope_class subst cl with
+ let env = Global.env () in
+ match subst_scope_class env subst cl with
| Some cl' as ocl' when cl' != cl -> ocl'
| _ -> ocl in
let cls' = List.Smart.map subst_cl cls in
@@ -1565,7 +1671,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
| ArgsScopeAuto ->
let env = Global.env () in (*FIXME?*)
let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in
- let scs,cls = compute_arguments_scope_full sigma typ in
+ let scs,cls = compute_arguments_scope_full env sigma typ in
(req,r,List.length scs,scs,cls)
| ArgsScopeManual ->
(* Add to the manually given scopes the one found automatically
@@ -1573,7 +1679,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
of the manually given scopes to avoid further re-computations. *)
let env = Global.env () in (*FIXME?*)
let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in
- let l',cls = compute_arguments_scope_full sigma typ in
+ let l',cls = compute_arguments_scope_full env sigma typ in
let l1 = List.firstn n l' in
let cls1 = List.firstn n cls in
(req,r,0,l1@l,cls1)
@@ -1620,7 +1726,7 @@ let find_arguments_scope r =
let declare_ref_arguments_scope sigma ref =
let env = Global.env () in (* FIXME? *)
let typ = EConstr.of_constr @@ fst @@ Typeops.type_of_global_in_context env ref in
- let (scs,cls as o) = compute_arguments_scope_full sigma typ in
+ let (scs,cls as o) = compute_arguments_scope_full env sigma typ in
declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o
(********************************)
@@ -1807,10 +1913,10 @@ let browse_notation strict ntn map =
map [] in
List.sort (fun x y -> String.compare (snd (fst x)) (snd (fst y))) l
-let global_reference_of_notation test (ntn,(sc,c,_)) =
+let global_reference_of_notation ~head test (ntn,(sc,c,_)) =
match c with
| NRef ref when test ref -> Some (ntn,sc,ref)
- | NApp (NRef ref, l) when List.for_all isNVar_or_NHole l && test ref ->
+ | NApp (NRef ref, l) when head || List.for_all isNVar_or_NHole l && test ref ->
Some (ntn,sc,ref)
| _ -> None
@@ -1822,14 +1928,14 @@ let error_notation_not_reference ?loc ntn =
(str "Unable to interpret " ++ quote (str ntn) ++
str " as a reference.")
-let interp_notation_as_global_reference ?loc test ntn sc =
+let interp_notation_as_global_reference ?loc ~head test ntn sc =
let scopes = match sc with
| Some sc ->
let scope = find_scope (find_delimiters_scope sc) in
String.Map.add sc scope String.Map.empty
| None -> !scope_map in
let ntns = browse_notation true ntn scopes in
- let refs = List.map (global_reference_of_notation test) ntns in
+ let refs = List.map (global_reference_of_notation ~head test) ntns in
match Option.List.flatten refs with
| [_,_,ref] -> ref
| [] -> error_notation_not_reference ?loc ntn
diff --git a/interp/notation.mli b/interp/notation.mli
index 842f2b1458..e7e917463b 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -74,7 +74,7 @@ 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 **decimal**
+(** A numeral interpreter is the pair of an interpreter for **(hexa)decimal**
numbers in terms and an optional interpreter in pattern, if
non integer or negative numbers are not supported, the interpreter
must fail with an appropriate error message *)
@@ -120,23 +120,32 @@ type numnot_option =
| Abstract of NumTok.UnsignedNat.t
type int_ty =
- { uint : Names.inductive;
+ { dec_uint : Names.inductive;
+ dec_int : Names.inductive;
+ hex_uint : Names.inductive;
+ hex_int : Names.inductive;
+ uint : Names.inductive;
int : Names.inductive }
type z_pos_ty =
{ z_ty : Names.inductive;
pos_ty : Names.inductive }
-type decimal_ty =
+type numeral_ty =
{ int : int_ty;
- decimal : Names.inductive }
+ decimal : Names.inductive;
+ hexadecimal : Names.inductive;
+ numeral : Names.inductive }
type target_kind =
- | Int of int_ty (* Coq.Init.Decimal.int + uint *)
- | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
+ | Int of int_ty (* Coq.Init.Numeral.int + uint *)
+ | UInt of int_ty (* Coq.Init.Numeral.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 *)
+ | Numeral of numeral_ty (* Coq.Init.Numeral.numeral + 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) *)
type string_target_kind =
| ListByte
@@ -245,7 +254,8 @@ val availability_of_notation : specific_notation -> subscopes ->
(** {6 Miscellaneous} *)
-val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) ->
+(** If head is true, also allows applied global references. *)
+val interp_notation_as_global_reference : ?loc:Loc.t -> head:bool -> (GlobRef.t -> bool) ->
notation_key -> delimiters option -> GlobRef.t
(** Checks for already existing notations *)
@@ -264,13 +274,13 @@ type scope_class
val scope_class_compare : scope_class -> scope_class -> int
val subst_scope_class :
- Mod_subst.substitution -> scope_class -> scope_class option
+ Environ.env -> Mod_subst.substitution -> scope_class -> scope_class option
val declare_scope_class : scope_name -> scope_class -> unit
val declare_ref_arguments_scope : Evd.evar_map -> GlobRef.t -> unit
-val compute_arguments_scope : Evd.evar_map -> EConstr.types -> scope_name option list
-val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option
+val compute_arguments_scope : Environ.env -> Evd.evar_map -> EConstr.types -> scope_name option list
+val compute_type_scope : Environ.env -> Evd.evar_map -> EConstr.types -> scope_name option
(** Get the current scope bound to Sortclass, if it exists *)
val current_type_scope_name : unit -> scope_name option
diff --git a/interp/numTok.ml b/interp/numTok.ml
index e254e9e972..bb14649b91 100644
--- a/interp/numTok.ml
+++ b/interp/numTok.ml
@@ -12,6 +12,10 @@
e.g. "e"/"E" or the presence of leading 0s, or the presence of a +
in the exponent *)
+type num_class = CDec | CHex
+
+let string_del_head n s = String.sub s n (String.length s - n)
+
module UnsignedNat =
struct
type t = string
@@ -20,12 +24,15 @@ struct
assert (s.[0] >= '0' && s.[0] <= '9');
s
let to_string s =
- String.(concat "" (split_on_char '_' s))
+ String.(map Char.lowercase_ascii (concat "" (split_on_char '_' s)))
let sprint s = s
let print s = Pp.str (sprint s)
- (** Comparing two raw numbers (base 10, big-endian, non-negative).
+ let classify s =
+ if String.length s >= 2 && (s.[1] = 'x' || s.[1] = 'X') then CHex else CDec
+
+ (** Comparing two raw numbers (base 10 or 16, big-endian, non-negative).
A bit nasty, but not critical: used e.g. to decide when a number
is considered as large (see threshold warnings in notation.ml). *)
@@ -45,12 +52,20 @@ struct
0
with Comp c -> c
- let is_zero s =
- compare s "0" = 0
+ let compare n d =
+ assert (classify d = CDec);
+ match classify n with
+ | CDec -> compare (to_string n) (to_string d)
+ | CHex -> compare (string_del_head 2 (to_string n)) (to_string d)
+
+ let is_zero s =
+ compare s "0" = 0
end
type sign = SPlus | SMinus
+type 'a exp = EDec of 'a | EBin of 'a
+
module SignedNat =
struct
type t = sign * UnsignedNat.t
@@ -58,26 +73,89 @@ struct
assert (String.length s > 0);
let sign,n =
match s.[0] with
- | '-' -> (SMinus,String.sub s 1 (String.length s - 1))
- | '+' -> (SPlus,String.sub s 1 (String.length s - 1))
+ | '-' -> (SMinus,string_del_head 1 s)
+ | '+' -> (SPlus,string_del_head 1 s)
| _ -> (SPlus,s) in
(sign,UnsignedNat.of_string n)
let to_string (sign,n) =
(match sign with SPlus -> "" | SMinus -> "-") ^ UnsignedNat.to_string n
- let to_bigint n = Bigint.of_string (to_string n)
- let of_bigint n =
+ let classify (_,n) = UnsignedNat.classify n
+ let bigint_of_string (sign,n) =
+ (* nasty code to remove when switching to zarith
+ since zarith's of_string handles hexadecimal *)
+ match UnsignedNat.classify n with
+ | CDec -> Bigint.of_string (to_string (sign,n))
+ | CHex ->
+ let int_of_char c = match c with
+ | 'a'..'f' -> 10 + int_of_char c - int_of_char 'a'
+ | _ -> int_of_char c - int_of_char '0' in
+ let c16 = Bigint.of_int 16 in
+ let s = UnsignedNat.to_string n in
+ let n = ref Bigint.zero in
+ let len = String.length s in
+ for d = 2 to len - 1 do
+ n := Bigint.(add (mult !n c16) (of_int (int_of_char s.[d])))
+ done;
+ match sign with SPlus -> !n | SMinus -> Bigint.neg !n
+ let to_bigint n = bigint_of_string n
+ let string_of_nonneg_bigint c n =
+ (* nasty code to remove when switching to zarith
+ since zarith's format handles hexadecimal *)
+ match c with
+ | CDec -> Bigint.to_string n
+ | CHex ->
+ let div16 n =
+ let n, r0 = Bigint.div2_with_rest n in
+ let n, r1 = Bigint.div2_with_rest n in
+ let n, r2 = Bigint.div2_with_rest n in
+ let n, r3 = Bigint.div2_with_rest n in
+ let r = match r3, r2, r1, r0 with
+ | false, false, false, false -> "0"
+ | false, false, false, true -> "1"
+ | false, false, true, false -> "2"
+ | false, false, true, true -> "3"
+ | false, true, false, false -> "4"
+ | false, true, false, true -> "5"
+ | false, true, true, false -> "6"
+ | false, true, true, true -> "7"
+ | true, false, false, false -> "8"
+ | true, false, false, true -> "9"
+ | true, false, true, false -> "a"
+ | true, false, true, true -> "b"
+ | true, true, false, false -> "c"
+ | true, true, false, true -> "d"
+ | true, true, true, false -> "e"
+ | true, true, true, true -> "f" in
+ n, r in
+ let n = ref n in
+ let l = ref [] in
+ while Bigint.is_strictly_pos !n do
+ let n', r = div16 !n in
+ n := n';
+ l := r :: !l
+ done;
+ "0x" ^ String.concat "" (List.rev !l)
+ let of_bigint c n =
let sign, n = if Bigint.is_strictly_neg n then (SMinus, Bigint.neg n) else (SPlus, n) in
- (sign, Bigint.to_string n)
+ (sign, string_of_nonneg_bigint c n)
end
module Unsigned =
struct
type t = {
- int : string; (** \[0-9\]\[0-9_\]* *)
- frac : string; (** empty or \[0-9_\]+ *)
- exp : string (** empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *)
+ int : string;
+ frac : string;
+ exp : string
}
+ (**
+ - int: \[0-9\]\[0-9_\]*
+ - frac: empty or \[0-9_\]+
+ - exp: empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]*
+ or
+ - int: 0\[xX\]\[0-9a-fA-F\]\[0-9a-fA-F_\]*
+ - frac: empty or \[0-9a-fA-F_\]+
+ - exp: empty or \[pP\]\[+-\]?\[0-9\]\[0-9_\]* *)
let equal n1 n2 =
String.(equal n1.int n2.int && equal n1.frac n2.frac && equal n1.exp n2.exp)
@@ -96,19 +174,35 @@ struct
| Some ('0'..'9' as c) -> Stream.junk s; number (store len c) s
| Some ('_' as c) when len > 0 -> Stream.junk s; number (store len c) s
| _ -> len in
+ (* reads [0-9a-fA-F_]* *)
+ let rec hex_number len s = match Stream.peek s with
+ | Some (('0'..'9' | 'a'..'f' | 'A'..'F') as c) ->
+ Stream.junk s; hex_number (store len c) s
+ | Some ('_' as c) when len > 0 ->
+ Stream.junk s; hex_number (store len c) s
+ | _ -> len in
fun s ->
- let i = get_buff (number 0 s) in
+ let hex, i =
+ match Stream.npeek 3 s with
+ | '0' :: (('x' | 'X') as x) :: (('0'..'9' | 'a'..'f' | 'A'..'F') as c) :: _ ->
+ Stream.junk s; Stream.junk s; Stream.junk s;
+ true, get_buff (hex_number (store (store (store 0 '0') x) c) s)
+ | _ -> false, get_buff (number 0 s) in
assert (i <> "");
let f =
- match Stream.npeek 2 s with
- | '.' :: (('0'..'9' | '_') as c) :: _ ->
+ match hex, Stream.npeek 2 s with
+ | true, '.' :: (('0'..'9' | 'a'..'f' | 'A'..'F' | '_') as c) :: _ ->
+ Stream.junk s; Stream.junk s; get_buff (hex_number (store 0 c) s)
+ | false, '.' :: (('0'..'9' | '_') as c) :: _ ->
Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s)
| _ -> "" in
let e =
- match (Stream.npeek 2 s) with
- | (('e'|'E') as e) :: ('0'..'9' as c) :: _ ->
+ match hex, Stream.npeek 2 s with
+ | true, (('p'|'P') as e) :: ('0'..'9' as c) :: _
+ | false, (('e'|'E') as e) :: ('0'..'9' as c) :: _ ->
Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s)
- | (('e'|'E') as e) :: (('+'|'-') as sign) :: _ ->
+ | true, (('p'|'P') as e) :: (('+'|'-') as sign) :: _
+ | false, (('e'|'E') as e) :: (('+'|'-') as sign) :: _ ->
begin match Stream.npeek 3 s with
| _ :: _ :: ('0'..'9' as c) :: _ ->
Stream.junk s; Stream.junk s; Stream.junk s;
@@ -146,6 +240,7 @@ struct
| { int = _; frac = ""; exp = "" } -> true
| _ -> false
+ let classify n = UnsignedNat.classify n.int
end
open Unsigned
@@ -162,19 +257,30 @@ struct
| (SPlus,{int;frac;exp}) -> UnsignedNat.is_zero int && UnsignedNat.is_zero frac
| _ -> false
- let of_decimal_and_exponent (sign,int) f e =
- let exp = match e with Some e -> "e" ^ SignedNat.to_string e | None -> "" in
- let frac = match f with Some f -> UnsignedNat.to_string f | None -> "" in
+ let of_int_frac_and_exponent (sign,int) f e =
+ assert (match e with None -> true | Some e -> SignedNat.classify e = CDec);
+ let c = UnsignedNat.classify int in
+ let exp = match e with None -> "" | Some e ->
+ let e = SignedNat.to_string e in
+ match c with CDec -> "e" ^ e | CHex -> "p" ^ e in
+ let frac = match f with None -> "" | Some f ->
+ assert (c = UnsignedNat.classify f);
+ let f = UnsignedNat.to_string f in
+ match c with CDec -> f | CHex -> string_del_head 2 f in
sign, { int; frac; exp }
- let to_decimal_and_exponent (sign, { int; frac; exp }) =
+ let to_int_frac_and_exponent (sign, { int; frac; exp }) =
let e =
if exp = "" then None else
Some (match exp.[1] with
- | '-' -> SMinus, String.sub exp 2 (String.length exp - 2)
- | '+' -> SPlus, String.sub exp 2 (String.length exp - 2)
- | _ -> SPlus, String.sub exp 1 (String.length exp - 1)) in
- let f = if frac = "" then None else Some frac in
+ | '-' -> SMinus, string_del_head 2 exp
+ | '+' -> SPlus, string_del_head 2 exp
+ | _ -> SPlus, string_del_head 1 exp) in
+ let f =
+ if frac = "" then None else
+ Some (match UnsignedNat.classify int with
+ | CDec -> frac
+ | CHex -> "0x" ^ frac) in
(sign, int), f, e
let of_nat i =
@@ -211,8 +317,8 @@ struct
let of_string s =
assert (s <> "");
let sign,u = match s.[0] with
- | '-' -> (SMinus, String.sub s 1 (String.length s - 1))
- | '+' -> (SPlus, String.sub s 1 (String.length s - 1))
+ | '-' -> (SMinus, string_del_head 1 s)
+ | '+' -> (SPlus, string_del_head 1 s)
| _ -> (SPlus, s) in
(sign, Unsigned.of_string u)
@@ -224,27 +330,31 @@ struct
Some (SignedNat.to_bigint (sign,UnsignedNat.to_string n))
| _ -> None
- let of_bigint n =
- let sign, int = SignedNat.of_bigint n in
- (sign, { int; frac = ""; exp = "" })
+ let of_bigint c n =
+ of_int (SignedNat.of_bigint c n)
let to_bigint_and_exponent (s, { int; frac; exp }) =
- let s = match s with SPlus -> "" | SMinus -> "-" in
+ let c = UnsignedNat.classify int in
let int = UnsignedNat.to_string int in
let frac = UnsignedNat.to_string frac in
- let i = Bigint.of_string (s ^ int ^ frac) in
+ let i = SignedNat.to_bigint (s, int ^ frac) in
let e =
let e = if exp = "" then Bigint.zero else match exp.[1] with
- | '+' -> Bigint.of_string (UnsignedNat.to_string (String.sub exp 2 (String.length exp - 2)))
- | '-' -> Bigint.(neg (of_string (UnsignedNat.to_string (String.sub exp 2 (String.length exp - 2)))))
- | _ -> Bigint.of_string (UnsignedNat.to_string (String.sub exp 1 (String.length exp - 1))) in
- Bigint.(sub e (of_int (String.length (String.concat "" (String.split_on_char '_' frac))))) in
- (i,e)
+ | '+' -> Bigint.of_string (UnsignedNat.to_string (string_del_head 2 exp))
+ | '-' -> Bigint.(neg (of_string (UnsignedNat.to_string (string_del_head 2 exp))))
+ | _ -> Bigint.of_string (UnsignedNat.to_string (string_del_head 1 exp)) in
+ let l = String.length frac in
+ let l = match c with CDec -> l | CHex -> 4 * l in
+ Bigint.(sub e (of_int l)) in
+ (i, match c with CDec -> EDec e | CHex -> EBin e)
let of_bigint_and_exponent i e =
- of_decimal_and_exponent (SignedNat.of_bigint i) None (Some (SignedNat.of_bigint e))
+ let c = match e with EDec _ -> CDec | EBin _ -> CHex in
+ let e = match e with EDec e | EBin e -> Some (SignedNat.of_bigint CDec e) in
+ of_int_frac_and_exponent (SignedNat.of_bigint c i) None e
let is_bigger_int_than (s, { int; frac; exp }) i =
frac = "" && exp = "" && UnsignedNat.compare int i >= 0
+ let classify (_, n) = Unsigned.classify n
end
diff --git a/interp/numTok.mli b/interp/numTok.mli
index ea289df237..11d5a0f980 100644
--- a/interp/numTok.mli
+++ b/interp/numTok.mli
@@ -11,7 +11,7 @@
(** Numerals in different forms: signed or unsigned, possibly with
fractional part and exponent.
- Numerals are represented using raw strings of decimal
+ Numerals are represented using raw strings of (hexa)decimal
literals and a separate sign flag.
Note that this representation is not unique, due to possible
@@ -25,21 +25,29 @@
type sign = SPlus | SMinus
+type num_class = CDec | CHex
+
+type 'a exp = EDec of 'a | EBin of 'a
+
(** {6 String representation of a natural number } *)
module UnsignedNat :
sig
type t
val of_string : string -> t
- (** Convert from a non-empty sequence of digits (which may contain "_") *)
+ (** Convert from a non-empty sequence of digits (which may contain "_")
+ (or hexdigits when starting with "0x" or "0X") *)
val to_string : t -> string
- (** Convert to a non-empty sequence of digit that does not contain "_" *)
+ (** Convert to a non-empty sequence of digit that does not contain "_"
+ (or hexdigits, starting with "0x", all hexdigits are lower case) *)
val sprint : t -> string
val print : t -> Pp.t
(** [sprint] and [print] returns the numeral as it was parsed, for printing *)
+ val classify : t -> num_class
+
val compare : t -> t -> int
end
@@ -49,13 +57,16 @@ module SignedNat :
sig
type t = sign * UnsignedNat.t
val of_string : string -> t
- (** Convert from a non-empty sequence of digits which may contain "_" *)
+ (** Convert from a non-empty sequence of (hex)digits which may contain "_" *)
val to_string : t -> string
- (** Convert to a non-empty sequence of digit that does not contain "_" *)
+ (** Convert to a non-empty sequence of (hex)digit that does not contain "_"
+ (hexadecimals start with "0x" and all hexdigits are lower case) *)
+ val classify : t -> num_class
+
+ val of_bigint : num_class -> Bigint.bigint -> t
val to_bigint : t -> Bigint.bigint
- val of_bigint : Bigint.bigint -> t
end
(** {6 Unsigned decimal numerals } *)
@@ -78,11 +89,17 @@ sig
The recognized syntax is:
- integer part: \[0-9\]\[0-9_\]*
- - decimal part: empty or .\[0-9_\]+
- - exponent part: empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *)
+ - fractional part: empty or .\[0-9_\]+
+ - exponent part: empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]*
+ or
+ - integer part: 0\[xX\]\[0-9a-fA-F\]\[0-9a-fA-F_\]*
+ - fractional part: empty or .\[0-9a-fA-F_\]+
+ - exponent part: empty or \[pP\]\[+-\]?\[0-9\]\[0-9_\]* *)
val parse_string : string -> t option
- (** Parse the string as a positive Coq numeral, if possible *)
+ (** Parse the string as a non negative Coq numeral, if possible *)
+
+ val classify : t -> num_class
end
@@ -114,17 +131,20 @@ sig
val to_string : t -> string
(** Returns a string in the syntax of OCaml's float_of_string *)
- val of_bigint : Bigint.bigint -> t
+ val of_bigint : num_class -> Bigint.bigint -> t
val to_bigint : t -> Bigint.bigint option
(** Convert from and to bigint when the denotation of a bigint *)
- val of_decimal_and_exponent : SignedNat.t -> UnsignedNat.t option -> SignedNat.t option -> t
- val to_decimal_and_exponent : t -> SignedNat.t * UnsignedNat.t option * SignedNat.t option
- (** n, p and q such that the number is n.p*10^q *)
+ val of_int_frac_and_exponent : SignedNat.t -> UnsignedNat.t option -> SignedNat.t option -> t
+ val to_int_frac_and_exponent : t -> SignedNat.t * UnsignedNat.t option * SignedNat.t option
+ (** n, p and q such that the number is n.p*10^q or n.p*2^q
+ pre/postcondition: classify n = classify p, classify q = CDec *)
+
+ val of_bigint_and_exponent : Bigint.bigint -> Bigint.bigint exp -> t
+ val to_bigint_and_exponent : t -> Bigint.bigint * Bigint.bigint exp
+ (** n and p such that the number is n*10^p or n*2^p *)
- val to_bigint_and_exponent : t -> Bigint.bigint * Bigint.bigint
- val of_bigint_and_exponent : Bigint.bigint -> Bigint.bigint -> t
- (** n and p such that the number is n*10^p *)
+ val classify : t -> num_class
val is_bigger_int_than : t -> UnsignedNat.t -> bool
(** Test if an integer whose absolute value is bounded *)
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 98fa71e15d..33d8aa6064 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -56,21 +56,25 @@ let global_inductive_with_alias qid =
| ref ->
user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
(pr_qualid qid ++ spc () ++ str "is not an inductive type.")
- with Not_found -> Nametab.error_global_not_found qid
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info qid
let global_with_alias ?head qid =
try locate_global_with_alias ?head qid
- with Not_found -> Nametab.error_global_not_found qid
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info qid
-let smart_global ?head = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
+let smart_global ?(head = false) = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
| AN r ->
- global_with_alias ?head r
+ global_with_alias ~head r
| ByNotation (ntn,sc) ->
- Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)
+ Notation.interp_notation_as_global_reference ?loc ~head (fun _ -> true) ntn sc)
let smart_global_inductive = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
| AN r ->
global_inductive_with_alias r
| ByNotation (ntn,sc) ->
destIndRef
- (Notation.interp_notation_as_global_reference ?loc isIndRef ntn sc))
+ (Notation.interp_notation_as_global_reference ?loc ~head:false isIndRef ntn sc))
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 7184f5ea29..bd3e234a91 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Util
open Pp
open CErrors
open Names
@@ -82,16 +81,9 @@ let in_syntax_constant : (bool * syndef) -> obj =
subst_function = subst_syntax_constant;
classify_function = classify_syntax_constant }
-type syndef_interpretation = (Id.t * subscopes) list * notation_constr
-
-(* Coercions to the general format of notation that also supports
- variables bound to list of expressions *)
-let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,((Constrexpr.InConstrEntrySomeLevel,sc),NtnTypeConstr))) ids,ac)
-let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac)
-
let declare_syntactic_definition ~local deprecation id ~onlyparsing pat =
let syndef =
- { syndef_pattern = in_pat pat;
+ { syndef_pattern = pat;
syndef_onlyparsing = onlyparsing;
syndef_deprecation = deprecation;
}
@@ -106,14 +98,12 @@ let warn_deprecated_syntactic_definition =
let search_syntactic_definition ?loc kn =
let syndef = KNmap.find kn !syntax_table in
- let def = out_pat syndef.syndef_pattern in
Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation;
- def
+ syndef.syndef_pattern
let search_filtered_syntactic_definition ?loc filter kn =
let syndef = KNmap.find kn !syntax_table in
- let def = out_pat syndef.syndef_pattern in
- let res = filter def in
+ let res = filter syndef.syndef_pattern in
if Option.has_some res then
Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation;
res
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 8b323462a1..66a3132f2a 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -13,12 +13,10 @@ open Notation_term
(** Syntactic definitions. *)
-type syndef_interpretation = (Id.t * subscopes) list * notation_constr
-
val declare_syntactic_definition : local:bool -> Deprecation.t option -> Id.t ->
- onlyparsing:bool -> syndef_interpretation -> unit
+ onlyparsing:bool -> interpretation -> unit
-val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation
+val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> interpretation
val search_filtered_syntactic_definition : ?loc:Loc.t ->
- (syndef_interpretation -> 'a option) -> KerName.t -> 'a option
+ (interpretation -> 'a option) -> KerName.t -> 'a option
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 13:35:57 +0000