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, 214 deletions

diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
deleted file mode 100644
index d66b9537b4..0000000000
--- a/plugins/syntax/r_syntax.ml
+++ /dev/null
@@ -1,214 +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 Util
-open Names
-open Glob_term
-
-(* Poor's man DECLARE PLUGIN *)
-let __coq_plugin_name = "r_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-exception Non_closed_number
-
-(**********************************************************************)
-(* Parsing positive via scopes                                        *)
-(**********************************************************************)
-
-let binnums = ["Coq";"Numbers";"BinNums"]
-
-let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
-
-let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> GlobRef.equal r gr
-| _ -> false
-
-let positive_modpath = MPfile (make_dir binnums)
-
-let positive_kn = MutInd.make2 positive_modpath (Label.make "positive")
-let path_of_xI = ((positive_kn,0),1)
-let path_of_xO = ((positive_kn,0),2)
-let path_of_xH = ((positive_kn,0),3)
-let glob_xI = GlobRef.ConstructRef path_of_xI
-let glob_xO = GlobRef.ConstructRef path_of_xO
-let glob_xH = GlobRef.ConstructRef path_of_xH
-
-let pos_of_bignat ?loc x =
-  let ref_xI = DAst.make @@ GRef (glob_xI, None) in
-  let ref_xH = DAst.make @@ GRef (glob_xH, None) in
-  let ref_xO = DAst.make @@ GRef (glob_xO, None) in
-  let rec pos_of x =
-    match Z.(div_rem x (of_int 2)) with
-      | (q,rem) when rem = Z.zero -> DAst.make @@ GApp (ref_xO,[pos_of q])
-      | (q,_) when not Z.(equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q])
-      | (q,_) -> ref_xH
-  in
-  pos_of x
-
-(**********************************************************************)
-(* Printing positive via scopes                                       *)
-(**********************************************************************)
-
-let rec bignat_of_pos c = match DAst.get c with
-  | GApp (r, [a]) when is_gr r glob_xO -> Z.mul Z.(of_int 2) (bignat_of_pos a)
-  | GApp (r, [a]) when is_gr r glob_xI -> Z.add Z.one Z.(mul (of_int 2) (bignat_of_pos a))
-  | GRef (a, _) when GlobRef.equal a glob_xH -> Z.one
-  | _ -> raise Non_closed_number
-
-(**********************************************************************)
-(* Parsing Z via scopes                                               *)
-(**********************************************************************)
-
-let z_kn = MutInd.make2 positive_modpath (Label.make "Z")
-let path_of_ZERO = ((z_kn,0),1)
-let path_of_POS = ((z_kn,0),2)
-let path_of_NEG = ((z_kn,0),3)
-let glob_ZERO = GlobRef.ConstructRef path_of_ZERO
-let glob_POS = GlobRef.ConstructRef path_of_POS
-let glob_NEG = GlobRef.ConstructRef path_of_NEG
-
-let z_of_int ?loc n =
-  if not Z.(equal n zero) then
-    let sgn, n =
-      if Z.(leq zero n) then glob_POS, n else glob_NEG, Z.neg n in
-    DAst.make @@ GApp(DAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n])
-  else
-    DAst.make @@ GRef (glob_ZERO, None)
-
-(**********************************************************************)
-(* Printing Z via scopes                                              *)
-(**********************************************************************)
-
-let bigint_of_z c = match DAst.get c with
-  | GApp (r,[a]) when is_gr r glob_POS -> bignat_of_pos a
-  | GApp (r,[a]) when is_gr r glob_NEG -> Z.neg (bignat_of_pos a)
-  | GRef (a, _) when GlobRef.equal a glob_ZERO -> Z.zero
-  | _ -> raise Non_closed_number
-
-(**********************************************************************)
-(* Parsing R via scopes                                               *)
-(**********************************************************************)
-
-let rdefinitions = ["Coq";"Reals";"Rdefinitions"]
-let r_modpath = MPfile (make_dir rdefinitions)
-let r_base_modpath = MPdot (r_modpath, Label.make "RbaseSymbolsImpl")
-let r_path = make_path ["Coq";"Reals";"Rdefinitions";"RbaseSymbolsImpl"] "R"
-
-let glob_IZR = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "IZR")
-let glob_Rmult = GlobRef.ConstRef (Constant.make2 r_base_modpath @@ Label.make "Rmult")
-let glob_Rdiv = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "Rdiv")
-
-let binintdef = ["Coq";"ZArith";"BinIntDef"]
-let z_modpath = MPdot (MPfile (make_dir binintdef), Label.make "Z")
-
-let glob_pow_pos = GlobRef.ConstRef (Constant.make2 z_modpath @@ Label.make "pow_pos")
-
-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 pow p e =
-    let p = z_of_int ?loc (Z.of_int p) in
-    let e = pos_of_bignat 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 Int.equal (Z.sign e) 1 then rmult n (izr (pow p e))
-  else if Int.equal (Z.sign e) (-1) then rdiv n (izr (pow p (Z.neg e)))
-  else n  (* e = 0 *)
-
-(**********************************************************************)
-(* Printing R via scopes                                              *)
-(**********************************************************************)
-
-let rawnum_of_r c =
-  (* print i * 10^e, precondition: e <> 0 *)
-  let numTok_of_int_exp i e =
-    (* choose between 123e-2 and 1.23, this is purely heuristic
-       and doesn't play any soundness role *)
-    let choose_exponent =
-      if Int.equal (Z.sign e) 1 then
-        true  (* don't print 12 * 10^2 as 1200 to distinguish them *)
-      else
-        let i = Z.to_string i in
-        let li = if i.[0] = '-' then String.length i - 1 else String.length i in
-        let e = Z.neg e in
-        let le = String.length (Z.to_string e) in
-        Z.(lt (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 (NumTok.EDec e) in
-    (* print 123 * 10^-2 as 1.23, precondition e < 0 *)
-    let numTok_dot () =
-      let s, i =
-        if Z.sign i >= 0 then NumTok.SPlus, Z.to_string i
-        else NumTok.SMinus, Z.(to_string (neg i)) in
-      let ni = String.length i in
-      let e = - (Z.to_int e) in
-      assert (e > 0);
-      let i, f =
-        if e < ni then String.sub i 0 (ni - e), String.sub i (ni - e) e
-        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_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 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])
-          when is_gr i glob_IZR && is_gr i' glob_IZR ->
-        begin match DAst.get r with
-        | GApp (p, [t; e]) when is_gr p glob_pow_pos ->
-           let t = bigint_of_z t in
-           if not (Z.(equal t (of_int 10))) then
-             raise Non_closed_number
-           else
-             let i = bigint_of_z l in
-             let e = bignat_of_pos e in
-             let e = if is_gr md glob_Rdiv then Z.neg e else e in
-             numTok_of_int_exp i e
-        | _ -> raise Non_closed_number
-        end
-     | _ -> raise Non_closed_number
-     end
-  | _ -> raise Non_closed_number
-
-let uninterp_r (AnyGlobConstr p) =
-  try
-    Some (rawnum_of_r p)
-  with Non_closed_number ->
-    None
-
-open Notation
-
-let at_declare_ml_module f x =
-  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
-
-let r_scope = "R_scope"
-
-let _ =
-  register_rawnumeral_interpretation r_scope (r_of_rawnum,uninterp_r);
-  at_declare_ml_module enable_prim_token_interpretation
-    { pt_local = false;
-      pt_scope = r_scope;
-      pt_interp_info = Uid r_scope;
-      pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]);
-      pt_refs = [glob_IZR; glob_Rmult; glob_Rdiv];
-      pt_in_match = false }