Fix Numeral Notations (3/4 - moving more stuff)

Move most of the rest of the stuff from numeral.ml to notation.ml.  Now
that we use exceptions to print error messages, all of the
interpretation code for numeral notations can be moved to notation.ml.

This is commit 1/4 in the fix for #8401.

This is a pure cut/paste commit, modulo fixing name qualifications due
to moved things, and exposing some stuff in notation.mli (to be removed
in the next commit, where we finish the numeral notation reworking).

2 files changed, 2 insertions, 276 deletions

diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4
index 55f61a58f9..68b8178368 100644
--- a/plugins/syntax/g_numeral.ml4
+++ b/plugins/syntax/g_numeral.ml4
@@ -10,8 +10,8 @@
 
 DECLARE PLUGIN "numeral_notation_plugin"
 
-open Notation
 open Numeral
+open Notation
 open Pp
 open Names
 open Vernacinterp
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index bc25e4730d..1a70c9536d 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -15,56 +15,10 @@ open Libnames
 open Globnames
 open Constrexpr
 open Constrexpr_ops
-open Constr
 open Notation
 
 (** * Numeral notation *)
 
-(** Reduction
-
-    The constr [c] below isn't necessarily well-typed, since we
-    built it via an [mkApp] of a conversion function on a term
-    that starts with the right constructor but might be partially
-    applied.
-
-    At least [c] is known to be evar-free, since it comes from
-    our own ad-hoc [constr_of_glob] or from conversions such
-    as [coqint_of_rawnum].
-*)
-
-let eval_constr env sigma (c : Constr.t) =
-  let c = EConstr.of_constr c in
-  let sigma,t = Typing.type_of env sigma c in
-  let c' = Vnorm.cbv_vm env sigma c t in
-  EConstr.Unsafe.to_constr c'
-
-(* For testing with "compute" instead of "vm_compute" :
-let eval_constr env sigma (c : Constr.t) =
-  let c = EConstr.of_constr c in
-  let c' = Tacred.compute env sigma c in
-  EConstr.Unsafe.to_constr c'
-*)
-
-let eval_constr_app env sigma c1 c2 =
-  eval_constr env sigma (mkApp (c1,[| c2 |]))
-
-exception NotANumber
-
-let warn_large_num =
-  CWarnings.create ~name:"large-number" ~category:"numbers"
-    (fun ty ->
-      strbrk "Stack overflow or segmentation fault happens when " ++
-      strbrk "working with large numbers in " ++ pr_qualid ty ++
-      strbrk " (threshold may vary depending" ++
-      strbrk " on your system limits and on the command executed).")
-
-let warn_abstract_large_num =
-  CWarnings.create ~name:"abstract-large-number" ~category:"numbers"
-    (fun (ty,f) ->
-      strbrk "To avoid stack overflow, large numbers in " ++
-      pr_qualid ty ++ strbrk " are interpreted as applications of " ++
-      Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".")
-
 let warn_abstract_large_num_no_op =
   CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers"
     (fun f ->
@@ -73,234 +27,6 @@ let warn_abstract_large_num_no_op =
       Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++
       strbrk "option type.")
 
-(** Comparing two raw numbers (base 10, big-endian, non-negative).
-    A bit nasty, but not critical: only used to decide when a
-    number is considered as large (see warnings above). *)
-
-exception Comp of int
-
-let rec rawnum_compare s s' =
- let l = String.length s and l' = String.length s' in
- if l < l' then - rawnum_compare s' s
- else
-   let d = l-l' in
-   try
-     for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done;
-     for i = d to l-1 do
-       let c = Pervasives.compare s.[i] s'.[i-d] in
-       if c != 0 then raise (Comp c)
-     done;
-     0
-   with Comp c -> c
-
-(***********************************************************************)
-
-(** ** Conversion between Coq [Decimal.int] and internal raw string *)
-
-(** Decimal.Nil has index 1, then Decimal.D0 has index 2 .. Decimal.D9 is 11 *)
-
-let digit_of_char c =
-  assert ('0' <= c && c <= '9');
-  Char.code c - Char.code '0' + 2
-
-let char_of_digit n =
-  assert (2<=n && n<=11);
-  Char.chr (n-2 + Char.code '0')
-
-let coquint_of_rawnum uint str =
-  let nil = mkConstruct (uint,1) in
-  let rec do_chars s i acc =
-    if i < 0 then acc
-    else
-      let dg = mkConstruct (uint, digit_of_char s.[i]) in
-      do_chars s (i-1) (mkApp(dg,[|acc|]))
-  in
-  do_chars str (String.length str - 1) nil
-
-let coqint_of_rawnum inds (str,sign) =
-  let uint = coquint_of_rawnum inds.uint str in
-  mkApp (mkConstruct (inds.int, if sign then 1 else 2), [|uint|])
-
-let rawnum_of_coquint c =
-  let rec of_uint_loop c buf =
-    match Constr.kind c with
-    | Construct ((_,1), _) (* Nil *) -> ()
-    | App (c, [|a|]) ->
-       (match Constr.kind c with
-        | Construct ((_,n), _) (* D0 to D9 *) ->
-           let () = Buffer.add_char buf (char_of_digit n) in
-           of_uint_loop a buf
-        | _ -> raise NotANumber)
-    | _ -> raise NotANumber
-  in
-  let buf = Buffer.create 64 in
-  let () = of_uint_loop c buf in
-  if Int.equal (Buffer.length buf) 0 then
-    (* To avoid ambiguities between Nil and (D0 Nil), we choose
-       to not display Nil alone as "0" *)
-    raise NotANumber
-  else Buffer.contents buf
-
-let rawnum_of_coqint c =
-  match Constr.kind c with
-  | App (c,[|c'|]) ->
-     (match Constr.kind c with
-      | Construct ((_,1), _) (* Pos *) -> (rawnum_of_coquint c', true)
-      | Construct ((_,2), _) (* Neg *) -> (rawnum_of_coquint c', false)
-      | _ -> raise NotANumber)
-  | _ -> raise NotANumber
-
-
-(***********************************************************************)
-
-(** ** Conversion between Coq [Z] and internal bigint *)
-
-(** First, [positive] from/to bigint *)
-
-let rec pos_of_bigint posty n =
-  match Bigint.div2_with_rest n with
-  | (q, false) ->
-      let c = mkConstruct (posty, 2) in (* xO *)
-      mkApp (c, [| pos_of_bigint posty q |])
-  | (q, true) when not (Bigint.equal q Bigint.zero) ->
-      let c = mkConstruct (posty, 1) in (* xI *)
-      mkApp (c, [| pos_of_bigint posty q |])
-  | (q, true) ->
-      mkConstruct (posty, 3) (* xH *)
-
-let rec bigint_of_pos c = match Constr.kind c with
-  | Construct ((_, 3), _) -> (* xH *) Bigint.one
-  | App (c, [| d |]) ->
-      begin match Constr.kind c with
-      | Construct ((_, n), _) ->
-          begin match n with
-          | 1 -> (* xI *) Bigint.add_1 (Bigint.mult_2 (bigint_of_pos d))
-          | 2 -> (* xO *) Bigint.mult_2 (bigint_of_pos d)
-          | n -> assert false (* no other constructor of type positive *)
-          end
-      | x -> raise NotANumber
-      end
-  | x -> raise NotANumber
-
-(** Now, [Z] from/to bigint *)
-
-let z_of_bigint { z_ty; pos_ty } n =
-  if Bigint.equal n Bigint.zero then
-    mkConstruct (z_ty, 1) (* Z0 *)
-  else
-    let (s, n) =
-      if Bigint.is_pos_or_zero n then (2, n) (* Zpos *)
-      else (3, Bigint.neg n) (* Zneg *)
-    in
-    let c = mkConstruct (z_ty, s) in
-    mkApp (c, [| pos_of_bigint pos_ty n |])
-
-let bigint_of_z z = match Constr.kind z with
-  | Construct ((_, 1), _) -> (* Z0 *) Bigint.zero
-  | App (c, [| d |]) ->
-      begin match Constr.kind c with
-      | Construct ((_, n), _) ->
-          begin match n with
-          | 2 -> (* Zpos *) bigint_of_pos d
-          | 3 -> (* Zneg *) Bigint.neg (bigint_of_pos d)
-          | n -> assert false (* no other constructor of type Z *)
-          end
-      | _ -> raise NotANumber
-      end
-  | _ -> raise NotANumber
-
-(** The uninterp function below work at the level of [glob_constr]
-    which is too low for us here. So here's a crude conversion back
-    to [constr] for the subset that concerns us. *)
-
-let rec constr_of_glob env sigma g = match DAst.get g with
-  | Glob_term.GRef (ConstructRef c, _) ->
-      let sigma,c = Evd.fresh_constructor_instance env sigma c in
-      sigma,mkConstructU c
-  | Glob_term.GApp (gc, gcl) ->
-      let sigma,c = constr_of_glob env sigma gc in
-      let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in
-      sigma,mkApp (c, Array.of_list cl)
-  | _ ->
-      raise NotANumber
-
-let rec glob_of_constr ?loc env sigma c = match Constr.kind c with
-  | App (c, ca) ->
-      let c = glob_of_constr ?loc env sigma c in
-      let cel = List.map (glob_of_constr ?loc env sigma) (Array.to_list ca) in
-      DAst.make ?loc (Glob_term.GApp (c, cel))
-  | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None))
-  | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None))
-  | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None))
-  | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None))
-  | _ -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedTerm c))
-
-let no_such_number ?loc ty =
-  CErrors.user_err ?loc
-   (str "Cannot interpret this number as a value of type " ++
-    pr_qualid ty)
-
-let interp_option ty ?loc env sigma c =
-  match Constr.kind c with
-  | App (_Some, [| _; c |]) -> glob_of_constr ?loc env sigma c
-  | App (_None, [| _ |]) -> no_such_number ?loc ty
-  | x -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedNonOptionTerm c))
-
-let uninterp_option c =
-  match Constr.kind c with
-  | App (_Some, [| _; x |]) -> x
-  | _ -> raise NotANumber
-
-let big2raw n =
-  if Bigint.is_pos_or_zero n then (Bigint.to_string n, true)
-  else (Bigint.to_string (Bigint.neg n), false)
-
-let raw2big (n,s) =
-  if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
-
-let interp o ?loc n =
-  begin match o.warning with
-  | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 ->
-     warn_large_num o.num_ty
-  | _ -> ()
-  end;
-  let c = match fst o.to_kind with
-    | Int int_ty -> coqint_of_rawnum int_ty n
-    | UInt uint_ty when snd n -> coquint_of_rawnum uint_ty (fst n)
-    | UInt _ (* n <= 0 *) -> no_such_number ?loc o.num_ty
-    | Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big n)
-  in
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in
-  let to_ty = EConstr.Unsafe.to_constr to_ty in
-  match o.warning, snd o.to_kind with
-  | Abstract threshold, Direct when rawnum_compare (fst n) threshold >= 0 ->
-     warn_abstract_large_num (o.num_ty,o.to_ty);
-     glob_of_constr ?loc env sigma (mkApp (to_ty,[|c|]))
-  | _ ->
-     let res = eval_constr_app env sigma to_ty c in
-     match snd o.to_kind with
-     | Direct -> glob_of_constr ?loc env sigma res
-     | Option -> interp_option o.num_ty ?loc env sigma res
-
-let uninterp o (Glob_term.AnyGlobConstr n) =
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  let sigma,of_ty = Evd.fresh_global env sigma o.of_ty in
-  let of_ty = EConstr.Unsafe.to_constr of_ty in
-  try
-    let sigma,n = constr_of_glob env sigma n in
-    let c = eval_constr_app env sigma of_ty n in
-    let c = if snd o.of_kind == Direct then c else uninterp_option c in
-    match fst o.of_kind with
-    | Int _ -> Some (rawnum_of_coqint c)
-    | UInt _ -> Some (rawnum_of_coquint c, true)
-    | Z _ -> Some (big2raw (bigint_of_z c))
-  with
-  | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *)
-  | NotANumber -> None (* all other functions except big2raw *)
-
 (* Here we only register the interp and uninterp functions
    for a particular Numeral Notation (determined by a unique
    string). The actual activation of the notation will be done
@@ -310,7 +36,7 @@ let uninterp o (Glob_term.AnyGlobConstr n) =
 
 let load_numeral_notation _ (_, (uid,opts)) =
   Notation.register_rawnumeral_interpretation
-    ~allow_overwrite:true uid (interp opts, uninterp opts)
+    ~allow_overwrite:true uid (Notation.Numeral.interp opts, Notation.Numeral.uninterp opts)
 
 let cache_numeral_notation x = load_numeral_notation 1 x