aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ltac/g_class.mlg4
-rw-r--r--plugins/ltac/rewrite.ml38
-rw-r--r--plugins/ltac/tacinterp.ml60
-rw-r--r--plugins/ltac/tactic_matching.ml10
-rw-r--r--plugins/omega/coq_omega.ml8
-rw-r--r--plugins/ssr/ssrview.ml4
-rw-r--r--plugins/syntax/float_syntax.ml5
-rw-r--r--plugins/syntax/numeral.ml97
-rw-r--r--plugins/syntax/r_syntax.ml18
9 files changed, 169 insertions, 75 deletions
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 81e745b714..35c90444b1 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -142,7 +142,9 @@ let progress_evars t =
let sigma = Tacmach.New.project gl' in
let newconcl = Proofview.Goal.concl gl' in
if eq_constr_mod_evars sigma concl newconcl
- then Tacticals.New.tclFAIL 0 (Pp.str"No progress made (modulo evars)")
+ then
+ let info = Exninfo.reify () in
+ Tacticals.New.tclFAIL ~info 0 (Pp.str"No progress made (modulo evars)")
else Proofview.tclUNIT ()
end
in t <*> check
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index d6b2a17882..4bc8d61258 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1566,7 +1566,8 @@ let assert_replacing id newt tac =
Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
let newfail n s =
- Proofview.tclZERO (Refiner.FailError (n, lazy s))
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info (Refiner.FailError (n, lazy s))
let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let open Proofview.Notations in
@@ -1576,8 +1577,10 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let treat sigma res =
match res with
| None -> newfail 0 (str "Nothing to rewrite")
- | Some None -> if progress then newfail 0 (str"Failed to progress")
- else Proofview.tclUNIT ()
+ | Some None ->
+ if progress
+ then newfail 0 (str"Failed to progress")
+ else Proofview.tclUNIT ()
| Some (Some res) ->
let (undef, prf, newt) = res in
let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in
@@ -1641,7 +1644,9 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let tactic_init_setoid () =
try init_setoid (); Proofview.tclUNIT ()
- with e when CErrors.noncritical e -> Tacticals.New.tclFAIL 0 (str"Setoid library not loaded")
+ with e when CErrors.noncritical e ->
+ let _, info = Exninfo.capture e in
+ Tacticals.New.tclFAIL ~info 0 (str"Setoid library not loaded")
let cl_rewrite_clause_strat progress strat clause =
tactic_init_setoid () <*>
@@ -1650,10 +1655,11 @@ let cl_rewrite_clause_strat progress strat clause =
(cl_rewrite_clause_newtac ~progress strat clause)
(fun (e, info) -> match e with
| RewriteFailure e ->
- tclZEROMSG (str"setoid rewrite failed: " ++ e)
+ tclZEROMSG ~info (str"setoid rewrite failed: " ++ e)
| Refiner.FailError (n, pp) ->
- tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp)
- | e -> Proofview.tclZERO ~info e))
+ tclFAIL ~info n (str"setoid rewrite failed: " ++ Lazy.force pp)
+ | e ->
+ Proofview.tclZERO ~info e))
(** Setoid rewriting when called with "setoid_rewrite" *)
let cl_rewrite_clause l left2right occs clause =
@@ -2109,7 +2115,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals =
(cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl)))
(fun (e, info) -> match e with
| RewriteFailure e ->
- tclFAIL 0 (str"setoid rewrite failed: " ++ e)
+ tclFAIL ~info 0 (str"setoid rewrite failed: " ++ e)
| e -> Proofview.tclZERO ~info e)
end
@@ -2117,8 +2123,8 @@ let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite
(** [setoid_]{reflexivity,symmetry,transitivity} tactics *)
-let not_declared env sigma ty rel =
- tclFAIL 0
+let not_declared ~info env sigma ty rel =
+ tclFAIL ~info 0
(str" The relation " ++ Printer.pr_econstr_env env sigma rel ++ str" is not a declared " ++
str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library")
@@ -2135,7 +2141,10 @@ let setoid_proof ty fn fallback =
let car = snd (List.hd (fst (Reductionops.splay_prod env sigma t))) in
(try init_relation_classes () with _ -> raise Not_found);
fn env sigma car rel
- with e -> Proofview.tclZERO e
+ with e ->
+ (* XXX what is the right test here as to whether e can be converted ? *)
+ let e, info = Exninfo.capture e in
+ Proofview.tclZERO ~info e
end
begin function
| e ->
@@ -2145,9 +2154,10 @@ let setoid_proof ty fn fallback =
| Hipattern.NoEquationFound ->
begin match e with
| (Not_found, _) ->
- let rel, _, _ = decompose_app_rel env sigma concl in
- not_declared env sigma ty rel
- | (e, info) -> Proofview.tclZERO ~info e
+ let rel, _, _ = decompose_app_rel env sigma concl in
+ not_declared ~info env sigma ty rel
+ | (e, info) ->
+ Proofview.tclZERO ~info e
end
| e' -> Proofview.tclZERO ~info e'
end
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 5e8babbf80..97f7a198e6 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -781,7 +781,9 @@ let interp_message_token ist = function
| MsgIdent {loc;v=id} ->
let v = try Some (Id.Map.find id ist.lfun) with Not_found -> None in
match v with
- | None -> Ftactic.lift (Tacticals.New.tclZEROMSG (Id.print id ++ str" not found."))
+ | None -> Ftactic.lift (
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (Id.print id ++ str" not found."))
| Some v -> message_of_value v
let interp_message ist l =
@@ -1094,11 +1096,15 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
end
| TacFail (g,n,s) ->
let msg = interp_message ist s in
- let tac l = Tacticals.New.tclFAIL (interp_int_or_var ist n) l in
+ let tac ~info l = Tacticals.New.tclFAIL ~info (interp_int_or_var ist n) l in
let tac =
match g with
- | TacLocal -> fun l -> Proofview.tclINDEPENDENT (tac l)
- | TacGlobal -> tac
+ | TacLocal ->
+ let info = Exninfo.reify () in
+ fun l -> Proofview.tclINDEPENDENT (tac ~info l)
+ | TacGlobal ->
+ let info = Exninfo.reify () in
+ tac ~info
in
Ftactic.run msg tac
| TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac)
@@ -1181,8 +1187,11 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let len1 = List.length alias.Tacenv.alias_args in
let len2 = List.length l in
if len1 = len2 then tac
- else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \
- expected " ++ int len1 ++ str ", found " ++ int len2)
+ else
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info
+ (str "Arguments length mismatch: \
+ expected " ++ int len1 ++ str ", found " ++ int len2)
in
Ftactic.run tac (fun () -> Proofview.tclUNIT ())
@@ -1274,7 +1283,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
and interp_app loc ist fv largs : Val.t Ftactic.t =
Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
let (>>=) = Ftactic.bind in
- let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in
+ let fail ~info = Tacticals.New.tclZEROMSG ~info (str "Illegal tactic application.") in
if has_type fv (topwit wit_tacvalue) then
match to_tacvalue fv with
(* if var=[] and body has been delayed by val_interp, then body
@@ -1320,12 +1329,18 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,newlfun,lvar,body)))
| (VFun(appl,trace,olfun,[],body)) ->
let extra_args = List.length largs in
- Tacticals.New.tclZEROMSG (str "Illegal tactic application: got " ++
- str (string_of_int extra_args) ++
- str " extra " ++ str (String.plural extra_args "argument") ++
- str ".")
- | VRec(_,_) -> fail
- else fail
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info
+ (str "Illegal tactic application: got " ++
+ str (string_of_int extra_args) ++
+ str " extra " ++ str (String.plural extra_args "argument") ++
+ str ".")
+ | VRec(_,_) ->
+ let info = Exninfo.reify () in
+ fail ~info
+ else
+ let info = Exninfo.reify () in
+ fail ~info
(* Gives the tactic corresponding to the tactic value *)
and tactic_of_value ist vle =
@@ -1353,7 +1368,8 @@ and tactic_of_value ist vle =
let givenargs =
List.map (fun (arg,_) -> Names.Id.to_string arg) (Names.Id.Map.bindings vmap) in
let numgiven = List.length givenargs in
- Tacticals.New.tclZEROMSG
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info
(Pp.str tactic_nm ++ Pp.str " was not fully applied:" ++ spc() ++
(match numargs with
0 -> assert false
@@ -1371,11 +1387,15 @@ and tactic_of_value ist vle =
| _ ->
Pp.str "arguments were provided for variables " ++
pr_enum Pp.str givenargs ++ Pp.str ".")
- | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
+ | VRec _ ->
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (str "A fully applied tactic is expected.")
else if has_type vle (topwit wit_tactic) then
let tac = out_gen (topwit wit_tactic) vle in
tactic_of_value ist tac
- else Tacticals.New.tclZEROMSG (str "Expression does not evaluate to a tactic.")
+ else
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (str "Expression does not evaluate to a tactic.")
(* Interprets the clauses of a recursive LetIn *)
and interp_letrec ist llc u =
@@ -1569,10 +1589,12 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t =
pr_econstr_env env sigma cresult)
end <*>
Ftactic.return cresult
- with CannotCoerceTo _ ->
+ with CannotCoerceTo _ as exn ->
+ let _, info = Exninfo.capture exn in
let env = Proofview.Goal.env gl in
- Tacticals.New.tclZEROMSG (str "Must evaluate to a closed term" ++ fnl() ++
- str "offending expression: " ++ fnl() ++ pr_inspect env e result)
+ Tacticals.New.tclZEROMSG ~info
+ (str "Must evaluate to a closed term" ++ fnl() ++
+ str "offending expression: " ++ fnl() ++ pr_inspect env e result)
end
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index 525199735d..2b43b11fe1 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -186,7 +186,9 @@ module PatternMatching (E:StaticEnvironment) = struct
{ stream = fun k ctx -> m.stream (fun () ctx -> y.stream k ctx) ctx }
(** Failure of the pattern-matching monad: no success. *)
- let fail (type a) : a m = { stream = fun _ _ -> Proofview.tclZERO matching_error }
+ let fail (type a) : a m = { stream = fun _ _ ->
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info matching_error }
let run (m : 'a m) =
let ctx = {
@@ -209,7 +211,11 @@ module PatternMatching (E:StaticEnvironment) = struct
(** Declares a substitution, a context substitution and a term substitution. *)
let put subst context terms : unit m =
let s = { subst ; context ; terms ; lhs = () } in
- { stream = fun k ctx -> match merge s ctx with None -> Proofview.tclZERO matching_error | Some s -> k () s }
+ { stream = fun k ctx -> match merge s ctx with
+ | None ->
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info matching_error
+ | Some s -> k () s }
(** Declares a substitution. *)
let put_subst subst : unit m = put subst empty_context_subst empty_term_subst
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 79d6c05e1d..3ba6365783 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1475,7 +1475,9 @@ let coq_omega =
let path = simplify_strong (new_id,new_var_num,display_var) system in
if !display_action_flag then display_action display_var path;
tclTHEN prelude (replay_history tactic_normalisation path)
- with NO_CONTRADICTION -> tclZEROMSG (Pp.str"Omega can't solve this system")
+ with NO_CONTRADICTION as e ->
+ let _, info = Exninfo.capture e in
+ tclZEROMSG ~info (Pp.str"Omega can't solve this system")
end
end
@@ -1890,7 +1892,9 @@ let destructure_goal =
end)
intro
with Undecidable -> Tactics.elim_type (Lazy.force coq_False)
- | e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ | e when Proofview.V82.catchable_exception e ->
+ let e, info = Exninfo.capture e in
+ Proofview.tclZERO ~info e
in
tclTHEN goal_tac destructure_hyps
in
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 88a3e85211..ad0a31622c 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -194,9 +194,11 @@ let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
Pp.(str"interp-out: " ++ Printer.pr_econstr_env env sigma term));
tclUNIT (env,sigma,term)
with e ->
+ (* XXX this is another catch all! *)
+ let e, info = Exninfo.capture e in
Ssrprinters.ppdebug (lazy
Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env glob));
- tclZERO e
+ tclZERO ~info e
end
(* Commits the term to the monad *)
diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml
index e0a9906689..9861a060ab 100644
--- a/plugins/syntax/float_syntax.ml
+++ b/plugins/syntax/float_syntax.ml
@@ -42,7 +42,7 @@ let interp_float ?loc n =
| Float64.(PZero | NZero) -> not (NumTok.Signed.is_zero n)
| Float64.(PNormal | NNormal | PSubn | NSubn) ->
let m, e =
- let (_, i), f, e = NumTok.Signed.to_decimal_and_exponent n in
+ let (_, i), f, e = NumTok.Signed.to_int_frac_and_exponent n in
let i = NumTok.UnsignedNat.to_string i in
let f = match f with
| None -> "" | Some f -> NumTok.UnsignedNat.to_string f in
@@ -70,7 +70,8 @@ let interp_float ?loc n =
else (* e < 0 *)
if e' <= e then check m' (-e) m (e - e')
else check' m' (-e) (e' - e) m in
- if inexact () then warn_inexact_float ?loc (sn, f);
+ if NumTok.(Signed.classify n = CDec) && inexact () then
+ warn_inexact_float ?loc (sn, f);
DAst.make ?loc (GFloat f)
(* Pretty printing is already handled in constrextern.ml *)
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 2250d57809..2db76719b8 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -55,24 +55,45 @@ let locate_z () =
}, mkRefC q_z)
else None
-let locate_decimal () =
- let int = "num.int.type" in
- let uint = "num.uint.type" in
+let locate_numeral () =
+ let dint = "num.int.type" in
+ let duint = "num.uint.type" in
let dec = "num.decimal.type" in
- if Coqlib.has_ref int && Coqlib.has_ref uint && Coqlib.has_ref dec
+ let hint = "num.hexadecimal_int.type" in
+ let huint = "num.hexadecimal_uint.type" in
+ let hex = "num.hexadecimal.type" in
+ let int = "num.num_int.type" in
+ let uint = "num.num_uint.type" in
+ let num = "num.numeral.type" in
+ if Coqlib.has_ref dint && Coqlib.has_ref duint && Coqlib.has_ref dec
+ && Coqlib.has_ref hint && Coqlib.has_ref huint && Coqlib.has_ref hex
+ && Coqlib.has_ref int && Coqlib.has_ref uint && Coqlib.has_ref num
then
+ let q_dint = qualid_of_ref dint in
+ let q_duint = qualid_of_ref duint in
+ let q_dec = qualid_of_ref dec in
+ let q_hint = qualid_of_ref hint in
+ let q_huint = qualid_of_ref huint in
+ let q_hex = qualid_of_ref hex in
let q_int = qualid_of_ref int in
let q_uint = qualid_of_ref uint in
- let q_dec = qualid_of_ref dec in
+ let q_num = qualid_of_ref num in
let int_ty = {
+ dec_int = unsafe_locate_ind q_dint;
+ dec_uint = unsafe_locate_ind q_duint;
+ hex_int = unsafe_locate_ind q_hint;
+ hex_uint = unsafe_locate_ind q_huint;
int = unsafe_locate_ind q_int;
uint = unsafe_locate_ind q_uint;
} in
- let dec_ty = {
+ let num_ty = {
int = int_ty;
decimal = unsafe_locate_ind q_dec;
+ hexadecimal = unsafe_locate_ind q_hex;
+ numeral = unsafe_locate_ind q_num;
} in
- Some (int_ty, mkRefC q_int, mkRefC q_uint, dec_ty, mkRefC q_dec)
+ Some (int_ty, mkRefC q_int, mkRefC q_uint, mkRefC q_dint, mkRefC q_duint,
+ num_ty, mkRefC q_num, mkRefC q_dec)
else None
let locate_int63 () =
@@ -90,20 +111,27 @@ let has_type env sigma f ty =
let type_error_to f ty =
CErrors.user_err
- (pr_qualid f ++ str " should go from Decimal.int to " ++
+ (pr_qualid f ++ str " should go from Numeral.int to " ++
pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++
- fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).")
+ fnl () ++ str "Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first).")
let type_error_of g ty =
CErrors.user_err
(pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
- str " to Decimal.int or (option Decimal.int)." ++ fnl () ++
- str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).")
+ str " to Numeral.int or (option Numeral.int)." ++ fnl () ++
+ str "Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first).")
+
+let warn_deprecated_decimal =
+ CWarnings.create ~name:"decimal-numeral-notation" ~category:"deprecated"
+ (fun () ->
+ strbrk "Deprecated Numeral Notation for Decimal.uint, \
+ Decimal.int or Decimal.decimal. Use Numeral.uint, \
+ Numeral.int or Numeral.numeral respectively.")
let vernac_numeral_notation local ty f g scope opts =
let env = Global.env () in
let sigma = Evd.from_env env in
- let dec_ty = locate_decimal () in
+ let num_ty = locate_numeral () in
let z_pos_ty = locate_z () in
let int63_ty = locate_int63 () in
let tyc = Smartlocate.global_inductive_with_alias ty in
@@ -118,13 +146,19 @@ let vernac_numeral_notation local ty f g scope opts =
let constructors = get_constructors tyc in
(* Check the type of f *)
let to_kind =
- match dec_ty with
- | Some (int_ty, cint, _, _, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct
- | Some (int_ty, cint, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option
- | Some (int_ty, _, cuint, _, _) when has_type env sigma f (arrow cuint cty) -> UInt int_ty.uint, Direct
- | Some (int_ty, _, cuint, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option
- | Some (_, _, _, dec_ty, cdec) when has_type env sigma f (arrow cdec cty) -> Decimal dec_ty, Direct
- | Some (_, _, _, dec_ty, cdec) when has_type env sigma f (arrow cdec (opt cty)) -> Decimal dec_ty, Option
+ match num_ty with
+ | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct
+ | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option
+ | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint cty) -> UInt int_ty, Direct
+ | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty, Option
+ | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum cty) -> Numeral num_ty, Direct
+ | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum (opt cty)) -> Numeral num_ty, Option
+ | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint cty) -> DecimalInt int_ty, Direct
+ | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> DecimalInt int_ty, Option
+ | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint cty) -> DecimalUInt int_ty, Direct
+ | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> DecimalUInt int_ty, Option
+ | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec cty) -> Decimal num_ty, Direct
+ | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec (opt cty)) -> Decimal num_ty, Option
| _ ->
match z_pos_ty with
| Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ cty) -> Z z_pos_ty, Direct
@@ -137,13 +171,19 @@ let vernac_numeral_notation local ty f g scope opts =
in
(* Check the type of g *)
let of_kind =
- match dec_ty with
- | Some (int_ty, cint, _, _, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct
- | Some (int_ty, cint, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option
- | Some (int_ty, _, cuint, _, _) when has_type env sigma g (arrow cty cuint) -> UInt int_ty.uint, Direct
- | Some (int_ty, _, cuint, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option
- | Some (_, _, _, dec_ty, cdec) when has_type env sigma g (arrow cty cdec) -> Decimal dec_ty, Direct
- | Some (_, _, _, dec_ty, cdec) when has_type env sigma g (arrow cty (opt cdec)) -> Decimal dec_ty, Option
+ match num_ty with
+ | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct
+ | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option
+ | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty cuint) -> UInt int_ty, Direct
+ | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty, Option
+ | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty cnum) -> Numeral num_ty, Direct
+ | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty (opt cnum)) -> Numeral num_ty, Option
+ | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty cint) -> DecimalInt int_ty, Direct
+ | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> DecimalInt int_ty, Option
+ | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty cuint) -> DecimalUInt int_ty, Direct
+ | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> DecimalUInt int_ty, Option
+ | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty cdec) -> Decimal num_ty, Direct
+ | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty (opt cdec)) -> Decimal num_ty, Option
| _ ->
match z_pos_ty with
| Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty cZ) -> Z z_pos_ty, Direct
@@ -154,6 +194,11 @@ let vernac_numeral_notation local ty f g scope opts =
| Some cint63 when has_type env sigma g (arrow cty (opt cint63)) -> Int63, Option
| _ -> type_error_of g ty
in
+ (match to_kind, of_kind with
+ | ((DecimalInt _ | DecimalUInt _ | Decimal _), _), _
+ | _, ((DecimalInt _ | DecimalUInt _ | Decimal _), _) ->
+ warn_deprecated_decimal ()
+ | _ -> ());
let o = { to_kind; to_ty; of_kind; of_ty;
ty_name = ty;
warning = opts }
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index c4e9c8b73d..23a7cc07c5 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -114,20 +114,21 @@ let glob_pow_pos = GlobRef.ConstRef (Constant.make2 z_modpath @@ Label.make "pow
let r_of_rawnum ?loc n =
let n,e = NumTok.Signed.to_bigint_and_exponent n in
+ let e,p = NumTok.(match e with EDec e -> e, 10 | EBin e -> e, 2) in
let izr z =
DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z]) in
let rmult r r' =
DAst.make @@ GApp (DAst.make @@ GRef(glob_Rmult,None), [r; r']) in
let rdiv r r' =
DAst.make @@ GApp (DAst.make @@ GRef(glob_Rdiv,None), [r; r']) in
- let pow10 e =
- let ten = z_of_int ?loc (Bigint.of_int 10) in
+ let pow p e =
+ let p = z_of_int ?loc (Bigint.of_int p) in
let e = pos_of_bignat e in
- DAst.make @@ GApp (DAst.make @@ GRef(glob_pow_pos,None), [ten; e]) in
+ DAst.make @@ GApp (DAst.make @@ GRef(glob_pow_pos,None), [p; e]) in
let n =
izr (z_of_int ?loc n) in
- if Bigint.is_strictly_pos e then rmult n (izr (pow10 e))
- else if Bigint.is_strictly_neg e then rdiv n (izr (pow10 (neg e)))
+ if Bigint.is_strictly_pos e then rmult n (izr (pow p e))
+ else if Bigint.is_strictly_neg e then rdiv n (izr (pow p (neg e)))
else n (* e = 0 *)
(**********************************************************************)
@@ -149,7 +150,8 @@ let rawnum_of_r c =
let le = String.length (Bigint.to_string e) in
Bigint.(less_than (add (of_int li) (of_int le)) e) in
(* print 123 * 10^-2 as 123e-2 *)
- let numTok_exponent () = NumTok.Signed.of_bigint_and_exponent i e in
+ let numTok_exponent () =
+ NumTok.Signed.of_bigint_and_exponent i (NumTok.EDec e) in
(* print 123 * 10^-2 as 1.23, precondition e < 0 *)
let numTok_dot () =
let s, i =
@@ -163,12 +165,12 @@ let rawnum_of_r c =
else "0", String.make (e - ni) '0' ^ i in
let i = s, NumTok.UnsignedNat.of_string i in
let f = NumTok.UnsignedNat.of_string f in
- NumTok.Signed.of_decimal_and_exponent i (Some f) None in
+ NumTok.Signed.of_int_frac_and_exponent i (Some f) None in
if choose_exponent then numTok_exponent () else numTok_dot () in
match DAst.get c with
| GApp (r, [a]) when is_gr r glob_IZR ->
let n = bigint_of_z a in
- NumTok.Signed.of_bigint n
+ NumTok.(Signed.of_bigint CDec n)
| GApp (md, [l; r]) when is_gr md glob_Rmult || is_gr md glob_Rdiv ->
begin match DAst.get l, DAst.get r with
| GApp (i, [l]), GApp (i', [r])
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 16:54:03 +0000