8000 [Numeral notations] Use Coqlib registered constants by vbgl · Pull Request #8720 · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

[Numeral notations] Use Coqlib registered constants #8720

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jan 31, 2019
Merged

[Numeral notations] Use Coqlib registered constants #8720

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6830457
[Numeral notations] Use Coqlib registered constants
vbgl Oct 12, 2018
0fdc539
[Numeral notations] Lazy resolution of decimal types
vbgl Oct 12, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions doc/sphinx/user-extensions/syntax-extensions.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1496,12 +1496,13 @@ Numeral notations
function returns :g:`None`, or if the interpretation is registered
for only non-negative integers, and the given numeral is negative.

.. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}.

.. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first).

The parsing function given to the :cmd:`Numeral Notation`
vernacular is not of the right type.

.. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}.
.. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first).

The printing function given to the :cmd:`Numeral Notation`
vernacular is not of the right type.
Expand Down
100 changes: 51 additions & 49 deletions plugins/syntax/numeral.ml
View file
Open in desktop
8000
Original file line number Diff line number Diff line change
Expand Up @@ -33,50 +33,59 @@ let get_constructors ind =
Array.to_list
(Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc)

let q_z = qualid_of_string "Coq.Numbers.BinNums.Z"
let q_positive = qualid_of_string "Coq.Numbers.BinNums.positive"
let q_int = qualid_of_string "Coq.Init.Decimal.int"
let q_uint = qualid_of_string "Coq.Init.Decimal.uint"
let q_option = qualid_of_string "Coq.Init.Datatypes.option"
let qualid_of_ref n =
n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty

let q_option () = qualid_of_ref "core.option.type"

let unsafe_locate_ind q =
match Nametab.locate q with
| IndRef i -> i
| _ -> raise Not_found

let locate_ind q =
try unsafe_locate_ind q
with Not_found -> Nametab.error_global_not_found q

let locate_z () =
try
Some { z_ty = unsafe_locate_ind q_z;
pos_ty = unsafe_locate_ind q_positive }
with Not_found -> None
let zn = "num.Z.type" in
let pn = "num.pos.type" in
if Coqlib.has_ref zn && Coqlib.has_ref pn
then
let q_z = qualid_of_ref zn in
let q_pos = qualid_of_ref pn in
Some ({
z_ty = unsafe_locate_ind q_z;
pos_ty = unsafe_locate_ind q_pos;
}, mkRefC q_z)
else None

let locate_int () =
{ uint = locate_ind q_uint;
int = locate_ind q_int }
let int = "num.int.type" in
let uint = "num.uint.type" in
if Coqlib.has_ref int && Coqlib.has_ref uint
then
let q_int = qualid_of_ref int in
let q_uint = qualid_of_ref uint in
Some ({
int = unsafe_locate_ind q_int;
uint = unsafe_locate_ind q_uint;
}, mkRefC q_int, mkRefC q_uint)
else None

let has_type f ty =
let (sigma, env) = Pfedit.get_current_context () in
let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in
try let _ = Constrintern.interp_constr env sigma c in true
with Pretype_errors.PretypeError _ -> false

let type_error_to f ty loadZ =
let type_error_to f ty =
CErrors.user_err
(pr_qualid f ++ str " should go from Decimal.int to " ++
pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++
fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++
(if loadZ then str " (require BinNums first)." else str "."))
fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first).")

let type_error_of g ty loadZ =
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 could be used" ++
(if loadZ then str " (require BinNums first)." else str "."))
str "Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first).")
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think you should only display the part about Require if the types don't resolve / aren't registered. But I don't object strongly.


let vernac_numeral_notation local ty f g scope opts =
let int_ty = locate_int () in
Expand All @@ -86,43 +95,36 @@ let vernac_numeral_notation local ty f g scope opts =
let of_ty = Smartlocate.global_with_alias g in
let cty = mkRefC ty in
let app x y = mkAppC (x,[y]) in
let cref q = mkRefC q in
let arrow x y =
mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y)
in
let cZ = cref q_z in
let cint = cref q_int in
let cuint = cref q_uint in
let coption = cref q_option in
let opt r = app coption r in
let opt r = app (mkRefC (q_option ())) r in
let constructors = get_constructors tyc in
(* Check the type of f *)
let to_kind =
if has_type f (arrow cint cty) then Int int_ty, Direct
else if has_type f (arrow cint (opt cty)) then Int int_ty, Option
else if has_type f (arrow cuint cty) then UInt int_ty.uint, Direct
else if has_type f (arrow cuint (opt cty)) then UInt int_ty.uint, Option
else
match z_pos_ty with
| Some z_pos_ty ->
if has_type f (arrow cZ cty) then Z z_pos_ty, Direct
else if has_type f (arrow cZ (opt cty)) then Z z_pos_ty, Option
else type_error_to f ty false
| None -> type_error_to f ty true
match int_ty with
| Some (int_ty, cint, _) when has_type f (arrow cint cty) -> Int int_ty, Direct
| Some (int_ty, cint, _) when has_type f (arrow cint (opt cty)) -> Int int_ty, Option
| Some (int_ty, _, cuint) when has_type f (arrow cuint cty) -> UInt int_ty.uint, Direct
| Some (int_ty, _, cuint) when has_type f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option
| _ ->
match z_pos_ty with
| Some (z_pos_ty, cZ) when has_type f (arrow cZ cty) -> Z z_pos_ty, Direct
| Some (z_pos_ty, cZ) when has_type f (arrow cZ (opt cty)) -> Z z_pos_ty, Option
| _ -> type_error_to f ty
in
(* Check the type of g *)
let of_kind =
if has_type g (arrow cty cint) then Int int_ty, Direct
else if has_type g (arrow cty (opt cint)) then Int int_ty, Option
else if has_type g (arrow cty cuint) then UInt int_ty.uint, Direct
else if has_type g (arrow cty (opt cuint)) then UInt int_ty.uint, Option
else
match z_pos_ty with
| Some z_pos_ty ->
if has_type g (arrow cty cZ) then Z z_pos_ty, Direct
else if has_type g (arrow cty (opt cZ)) then Z z_pos_ty, Option
else type_error_of g ty false
| None -> type_error_of g ty true
match int_ty with
| Some (int_ty, cint, _) when has_type g (arrow cty cint) -> Int int_ty, Direct
| Some (int_ty, cint, _) when has_type g (arrow cty (opt cint)) -> Int int_ty, Option
| Some (int_ty, _, cuint) when has_type g (arrow cty cuint) -> UInt int_ty.uint, Direct
| Some (int_ty, _, cuint) when has_type g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option
| _ ->
match z_pos_ty with
| Some (z_pos_ty, cZ) when has_type g (arrow cty cZ) -> Z z_pos_ty, Direct
| Some (z_pos_ty, cZ) when has_type g (arrow cty (opt cZ)) -> Z z_pos_ty, Option
| _ -> type_error_of g ty
in
let o = { to_kind; to_ty; of_kind; of_ty;
ty_name = ty;
Expand Down
5 changes: 4 additions & 1 deletion theories/Init/Decimal.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ Notation zero := (D0 Nil).

(** For signed integers, we use two constructors [Pos] and [Neg]. *)

Inductive int := Pos (d:uint) | Neg (d:uint).
Variant int := Pos (d:uint) | Neg (d:uint).
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why this change?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree it’s unrelated. But since I was already touching this file, I took the opportunity to tidy it a bit…


Declare Scope dec_uint_scope.
Delimit Scope dec_uint_scope with uint.
Expand All @@ -50,6 +50,9 @@ Declare Scope dec_int_scope.
Delimit Scope dec_int_scope with int.
Bind Scope dec_int_scope with int.

Register uint as num.uint.type.
Register int as num.int.type.

(** This representation favors simplicity over canonicity.
For normalizing numbers, we need to remove head zero digits,
and choose our canonical representation of 0 (here [D0 Nil]
Expand Down
1 change: 1 addition & 0 deletions theories/Numbers/BinNums.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ Bind Scope positive_scope with positive.
Arguments xO _%positive.
Arguments xI _%positive.

Register positive as num.pos.type.
Register xI as num.pos.xI.
Register xO as num.pos.xO.
Register xH as num.pos.xH.
Expand Down
0