Merge PR #12218: Numeral notations for non inductive types

Reviewed-by: herbelin
Reviewed-by: JasonGross
Reviewed-by: jfehrle
Ack-by: Zimmi48

1 files changed, 0 insertions, 217 deletions

diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
deleted file mode 100644
index 2db76719b8..0000000000
--- a/plugins/syntax/numeral.ml
+++ /dev/null
@@ -1,217 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Pp
-open Util
-open Names
-open Libnames
-open Constrexpr
-open Constrexpr_ops
-open Notation
-
-(** * Numeral notation *)
-
-let warn_abstract_large_num_no_op =
-  CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers"
-    (fun f ->
-      strbrk "The 'abstract after' directive has no effect when " ++
-      strbrk "the parsing function (" ++
-      Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++
-      strbrk "option type.")
-
-let get_constructors ind =
-  let mib,oib = Global.lookup_inductive ind in
-  let mc = oib.Declarations.mind_consnames in
-  Array.to_list
-    (Array.mapi (fun j c -> GlobRef.ConstructRef (ind, j + 1)) mc)
-
-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
-  | GlobRef.IndRef i -> i
-  | _ -> raise Not_found
-
-let locate_z () =
-  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_numeral () =
-  let dint = "num.int.type" in
-  let duint = "num.uint.type" in
-  let dec = "num.decimal.type" in
-  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_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 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, mkRefC q_dint, mkRefC q_duint,
-          num_ty, mkRefC q_num, mkRefC q_dec)
-  else None
-
-let locate_int63 () =
-  let int63n = "num.int63.type" in
-  if Coqlib.has_ref int63n
-  then
-    let q_int63 = qualid_of_ref int63n in
-    Some (mkRefC q_int63)
-  else None
-
-let has_type env sigma f ty =
-  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 =
-  CErrors.user_err
-    (pr_qualid f ++ str " should go from Numeral.int to " ++
-     pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++
-     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 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 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
-  let to_ty = Smartlocate.global_with_alias f in
-  let of_ty = Smartlocate.global_with_alias g in
-  let cty = mkRefC ty in
-  let app x y = mkAppC (x,[y]) in
-  let arrow x y =
-    mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y)
-  in
-  let opt r = app (mkRefC (q_option ())) r in
-  let constructors = get_constructors tyc in
-  (* Check the type of f *)
-  let to_kind =
-    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
-    | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ (opt cty)) -> Z z_pos_ty, Option
-    | _ ->
-    match int63_ty with
-    | Some cint63 when has_type env sigma f (arrow cint63 cty) -> Int63, Direct
-    | Some cint63 when has_type env sigma f (arrow cint63 (opt cty)) -> Int63, Option
-    | _ -> type_error_to f ty
-  in
-  (* Check the type of g *)
-  let of_kind =
-    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
-    | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty (opt cZ)) -> Z z_pos_ty, Option
-    | _ ->
-    match int63_ty with
-    | Some cint63 when has_type env sigma g (arrow cty cint63) -> Int63, Direct
-    | 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 }
-  in
-  (match opts, to_kind with
-   | Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty
-   | _ -> ());
-  let i =
-       { pt_local = local;
-         pt_scope = scope;
-         pt_interp_info = NumeralNotation o;
-         pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[];
-         pt_refs = constructors;
-         pt_in_match = true }
-  in
-  enable_prim_token_interpretation i