From 68304575dd3fd85d26e2f1bdff84721df8481952 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Fri, 12 Oct 2018 12:22:43 +0000 Subject: [Numeral notations] Use Coqlib registered constants --- plugins/syntax/numeral.ml | 34 +++++++++++++++++++++------------- theories/Init/Decimal.v | 5 ++++- theories/Numbers/BinNums.v | 1 + 3 files changed, 26 insertions(+), 14 deletions(-) diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 470deb4a60..efd36ad03c 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -33,11 +33,12 @@ 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_int () = qualid_of_ref "num.int.type" +let q_uint () = qualid_of_ref "num.uint.type" +let q_option () = qualid_of_ref "core.option.type" let unsafe_locate_ind q = match Nametab.locate q with @@ -45,14 +46,22 @@ let unsafe_locate_ind q = | _ -> raise Not_found let locate_ind q = + let q = q () in 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; @@ -86,11 +95,10 @@ 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 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 @@ -104,7 +112,7 @@ let vernac_numeral_notation local ty f g scope opts = 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 -> + | Some (z_pos_ty, cZ) -> 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 @@ -118,7 +126,7 @@ let vernac_numeral_notation local ty f g scope opts = 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 -> + | Some (z_pos_ty, cZ) -> 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 diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 537400fb05..3d4b3d0568 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -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). Declare Scope dec_uint_scope. Delimit Scope dec_uint_scope with uint. @@ -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] diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v index ef2c688759..247827597a 100644 --- a/theories/Numbers/BinNums.v +++ b/theories/Numbers/BinNums.v @@ -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. -- cgit v1.2.3 From 0fdc5394c1f0821ae343beb8714d838c89aa4fd0 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Fri, 12 Oct 2018 14:08:21 +0000 Subject: [Numeral notations] Lazy resolution of decimal types --- doc/sphinx/user-extensions/syntax-extensions.rst | 5 +- plugins/syntax/numeral.ml | 78 +++++++++++------------- 2 files changed, 39 insertions(+), 44 deletions(-) diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index c707da1353..ae66791b0c 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -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. diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index efd36ad03c..ea564ae2ba 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -36,8 +36,6 @@ let get_constructors ind = let qualid_of_ref n = n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty -let q_int () = qualid_of_ref "num.int.type" -let q_uint () = qualid_of_ref "num.uint.type" let q_option () = qualid_of_ref "core.option.type" let unsafe_locate_ind q = @@ -45,11 +43,6 @@ let unsafe_locate_ind q = | IndRef i -> i | _ -> raise Not_found -let locate_ind q = - let q = q () in - try unsafe_locate_ind q - with Not_found -> Nametab.error_global_not_found q - let locate_z () = let zn = "num.Z.type" in let pn = "num.pos.type" in @@ -64,8 +57,17 @@ let locate_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 @@ -73,19 +75,17 @@ let has_type f ty = 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).") let vernac_numeral_notation local ty f g scope opts = let int_ty = locate_int () in @@ -95,42 +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 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, cZ) -> - 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, cZ) -> - 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; -- cgit v1.2.3