Numeral Notation: misc code improvements (records, subfunctions, exceptions ...)

2 files changed, 191 insertions, 185 deletions

diff --git a/plugins/syntax/NatSyntaxViaZ.v b/plugins/syntax/NatSyntaxViaZ.v
index adee347d90..8a4d8f236d 100644
--- a/plugins/syntax/NatSyntaxViaZ.v
+++ b/plugins/syntax/NatSyntaxViaZ.v
@@ -44,13 +44,14 @@ Definition Z_succ x :=
       end
   end.
 
-Fixpoint Z_of_nat_loop n :=
+Fixpoint Z_of_nat n :=
   match n with
   | O => Z0
-  | S p => Z_succ (Z_of_nat_loop p)
+  | S p => Z_succ (Z_of_nat p)
   end.
 
-Definition Z_of_nat n := Some (Z_of_nat_loop n).
+(** The 1st conversion must either have type [Z->nat] or [Z->option nat].
+  The 2nd one must either have type [nat->Z] or [nat->option Z]. *)
 
 Numeral Notation nat nat_of_Z Z_of_nat : nat_scope
   (warning after 5000).
diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4
index b3f0591614..b4c6a06ab0 100644
--- a/plugins/syntax/g_numeral.ml4
+++ b/plugins/syntax/g_numeral.ml4
@@ -9,7 +9,6 @@
 DECLARE PLUGIN "numeral_notation_plugin"
 
 open Pp
-open CErrors
 open Util
 open Names
 open Libnames
@@ -19,12 +18,7 @@ open Constrexpr_ops
 open Constr
 open Misctypes
 
-(* Numeral notation *)
-
-let obj_string x =
-  if Obj.is_block (Obj.repr x) then
-    "tag = " ^ string_of_int (Obj.tag (Obj.repr x))
-  else "int_val = " ^ string_of_int (Obj.magic x)
+(** * Numeral notation *)
 
 let eval_constr (c : Constr.t) =
   let env = Global.env () in
@@ -35,6 +29,20 @@ let eval_constr (c : Constr.t) =
                  (EConstr.of_constr j.Environ.uj_type)
   in EConstr.Unsafe.to_constr c'
 
+exception NotANumber
+
+let warning_big_num ty =
+  strbrk "Stack overflow or segmentation fault happens when " ++
+  strbrk "working with large numbers in " ++ pr_reference ty ++
+  strbrk " (threshold may vary depending" ++
+  strbrk " on your system limits and on the command executed)."
+
+type conversion_function =
+  | Direct of Constant.t
+  | Option of Constant.t
+
+(** Conversion between Coq's [Positive] and our internal bigint *)
+
 let rec pos_of_bigint posty n =
   match Bigint.div2_with_rest n with
   | (q, false) ->
@@ -47,135 +55,127 @@ let rec pos_of_bigint posty n =
       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
+          | n -> assert false (* no other constructor of type positive *)
           end
-      | x -> raise Not_found
+      | x -> raise NotANumber
       end
-  | Construct ((_, 3), _) -> (* xH *) Bigint.one
-  | x -> anomaly (str "bigint_of_pos" ++ str (obj_string x))
+  | x -> raise NotANumber
+
+(** Conversion between Coq's [Z] and our internal bigint *)
 
-let z_of_bigint (zty, posty) ty thr n =
+type z_pos_ty =
+  { z_ty : Names.inductive;
+    pos_ty : Names.inductive }
+
+let maybe_warn (thr,msg) n =
   if Bigint.is_pos_or_zero n && not (Bigint.equal thr Bigint.zero) &&
      Bigint.less_than thr n
-  then
-    Feedback.msg_warning
-      (strbrk "Stack overflow or segmentation fault happens when " ++
-       strbrk "working with large numbers in " ++
-       str (string_of_reference ty) ++
-       strbrk " (threshold may vary depending" ++
-       strbrk " on your system limits and on the command executed).")
-  else ();
-  if not (Bigint.equal n Bigint.zero) then
+  then Feedback.msg_warning msg
+
+let z_of_bigint { z_ty; pos_ty } warn n =
+  maybe_warn warn 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 (zty, s) in
-    mkApp (c, [| pos_of_bigint posty n |])
-  else
-    mkConstruct (zty, 1) (* Z0 *)
+    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
+          | n -> assert false (* no other constructor of type Z *)
           end
-      | Const (c, _) -> anomaly (str "Const " ++ str (Constant.to_string c))
-      | x -> anomaly (str "bigint_of_z App c " ++ str (obj_string x))
+      | _ -> raise NotANumber
       end
-  | Construct ((_, 1), _) -> (* Z0 *) Bigint.zero
-  | _ -> raise Not_found
-
-let constr_of_global_reference = function
-  | VarRef v -> mkVar v
-  | ConstRef cr -> mkConst cr
-  | IndRef ind -> mkInd ind
-  | ConstructRef c -> mkConstruct c
-
-let rec constr_of_glob_constr vl gc =
-  match DAst.get gc with
-  | Glob_term.GRef (gr, gllo) ->
-      constr_of_global_reference gr
-  | Glob_term.GVar (id) ->
-      constr_of_glob_constr vl (List.assoc id vl)
+  | _ -> raise NotANumber
+
+(** The uinterp 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 g = match DAst.get g with
+  | Glob_term.GRef (ConstructRef c, _) -> mkConstruct c
   | Glob_term.GApp (gc, gcl) ->
-      let c = constr_of_glob_constr vl gc in
-      let cl = List.map (constr_of_glob_constr vl) gcl in
+      let c = constr_of_glob gc in
+      let cl = List.map constr_of_glob gcl in
       mkApp (c, Array.of_list cl)
   | _ ->
-      raise Not_found
+      raise NotANumber
 
-let rec glob_constr_of_constr ?loc c = match Constr.kind c with
-  | Var id ->
-      DAst.make ?loc (Glob_term.GRef (VarRef id, None))
+let rec glob_of_constr ?loc c = match Constr.kind c with
   | App (c, ca) ->
-      let c = glob_constr_of_constr ?loc c in
-      let cel = List.map (glob_constr_of_constr ?loc) (Array.to_list ca) in
+      let c = glob_of_constr ?loc c in
+      let cel = List.map (glob_of_constr ?loc) (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))
-  | x ->
-      anomaly (str "1 constr " ++ str (obj_string x))
-
-let interp_big_int zposty ty thr f ?loc bi =
-  let t =
-    let c = mkApp (mkConst f, [| z_of_bigint zposty ty thr bi |]) in
-    eval_constr c
-  in
-  match Constr.kind t with
-  | App (_, [| _; c |]) -> glob_constr_of_constr ?loc c
-  | App (_, [| _ |]) ->
-      CErrors.user_err ?loc
-         (str "Cannot interpret this number as a value of type " ++
-          str (string_of_reference ty))
-  | x ->
-      anomaly (str "interp_big_int " ++ str (obj_string x))
-
-let uninterp_big_int g (Glob_term.AnyGlobConstr c) =
-  match try Some (constr_of_glob_constr [] c) with Not_found -> None with
-  | Some c ->
-      begin match
-        try Some (eval_constr (mkApp (mkConst g, [| c |])))
-        with Type_errors.TypeError _ -> None
-      with
-      | Some t ->
-          begin match Constr.kind t with
-          | App (c, [| _; x |]) -> Some (bigint_of_z x)
-          | x -> None
-          end
-      | None ->
-         None
-      end
-  | None ->
-      None
+  | 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))
+  | _ -> CErrors.anomaly (str "interp_big_int: unexpected constr")
 
-let load_numeral_notation _ (_, (zposty, ty, f, g, sc, patl, thr, path)) =
-  Notation.declare_numeral_interpreter sc (path, [])
-        (interp_big_int zposty ty thr f)
-        (patl, uninterp_big_int g, true)
+let interp_big_int zposty ty warn of_z ?loc bi =
+  match of_z with
+  | Direct f ->
+     let c = mkApp (mkConst f, [| z_of_bigint zposty warn bi |]) in
+     glob_of_constr ?loc (eval_constr c)
+  | Option f ->
+     let c = mkApp (mkConst f, [| z_of_bigint zposty warn bi |]) in
+     match Constr.kind (eval_constr c) with
+     | App (_Some, [| _; c |]) -> glob_of_constr ?loc c
+     | App (_None, [| _ |]) ->
+        CErrors.user_err ?loc
+         (str "Cannot interpret this number as a value of type " ++
+          pr_reference ty)
+     | x -> CErrors.anomaly (str "interp_big_int: option expected")
 
-let cache_numeral_notation o = load_numeral_notation 1 o
+let uninterp_big_int to_z (Glob_term.AnyGlobConstr c) =
+  try
+    let t = constr_of_glob c in
+    match to_z with
+    | Direct g ->
+       let r = eval_constr (mkApp (mkConst g, [| t |])) in
+       Some (bigint_of_z r)
+    | Option g ->
+       let r = eval_constr (mkApp (mkConst g, [| t |])) in
+       match Constr.kind r with
+       | App (_Some, [| _; x |]) -> Some (bigint_of_z x)
+       | x -> None
+  with
+  | Type_errors.TypeError _ -> None (* cf. eval_constr *)
+  | NotANumber -> None (* cf constr_of_glob or bigint_of_z *)
 
 type numeral_notation_obj =
-  (Names.inductive * Names.inductive) *
-  Libnames.reference * Names.Constant.t *
-  Names.Constant.t *
-  Notation_term.scope_name * Glob_term.glob_constr list *
-  Bigint.bigint * Libnames.full_path
+  { num_ty : Libnames.reference;
+    z_pos_ty : z_pos_ty;
+    of_z : conversion_function;
+    to_z : conversion_function;
+    scope : Notation_term.scope_name;
+    constructors : Glob_term.glob_constr list;
+    warning : Bigint.bigint * Pp.t;
+    path : Libnames.full_path }
+
+let load_numeral_notation _ (_, o) =
+  Notation.declare_numeral_interpreter o.scope (o.path, [])
+   (interp_big_int o.z_pos_ty o.num_ty o.warning o.of_z)
+   (o.constructors, uninterp_big_int o.to_z, true)
+
+let cache_numeral_notation o = load_numeral_notation 1 o
 
 let inNumeralNotation : numeral_notation_obj -> Libobject.obj =
   Libobject.declare_object {
@@ -183,92 +183,97 @@ let inNumeralNotation : numeral_notation_obj -> Libobject.obj =
     Libobject.cache_function = cache_numeral_notation;
     Libobject.load_function = load_numeral_notation }
 
-let vernac_numeral_notation ty f g sc waft =
-  let zposty =
-    let zty =
-      let c = qualid_of_ident (Id.of_string "Z") in
-      try match Nametab.locate c with IndRef i -> i | _ -> raise Not_found
-      with Not_found -> Nametab.error_global_not_found (CAst.make c)
-    in
-    let positivety =
-      let c = qualid_of_ident (Id.of_string "positive") in
-      try match Nametab.locate c with IndRef i -> i | _ -> raise Not_found
-      with Not_found -> Nametab.error_global_not_found (CAst.make c)
-    in
-    (zty, positivety)
-  in
-  let tyc =
-    let tyq = qualid_of_reference ty in
-    try Nametab.locate CAst.(tyq.v) with Not_found ->
-      Nametab.error_global_not_found tyq
-  in
-  let fc =
-    let fq = qualid_of_reference f in
-    try Nametab.locate_constant CAst.(fq.v) with Not_found ->
-      Nametab.error_global_not_found fq
+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 ->
+         DAst.make
+           (Glob_term.GRef (ConstructRef (ind, j + 1), None)))
+       mc)
+
+let locate_ind s =
+  let q = qualid_of_string s in
+  try
+    match Nametab.locate q with
+    | IndRef i -> i
+    | _ -> raise Not_found
+  with Not_found -> Nametab.error_global_not_found (CAst.make q)
+
+(** TODO: we should ensure that BinNums is loaded (or autoload it ?) *)
+
+let locate_z () =
+  { z_ty = locate_ind "Coq.Numbers.BinNums.Z";
+    pos_ty = locate_ind "Coq.Numbers.BinNums.positive"; }
+
+let locate_globref r =
+  let q = qualid_of_reference r in
+  try Nametab.locate CAst.(q.v)
+  with Not_found -> Nametab.error_global_not_found q
+
+let locate_constant r =
+  let q = qualid_of_reference r in
+  try Nametab.locate_constant CAst.(q.v)
+  with Not_found -> Nametab.error_global_not_found q
+
+let has_type f ty =
+  let (sigma, env) = Pfedit.get_current_context () in
+  let c = mkCastC (mkRefC f, CastConv ty) in
+  try let _ = Constrintern.interp_constr env sigma c in true
+  with Pretype_errors.PretypeError _ -> false
+
+let vernac_numeral_notation ty f g scope waft =
+  let z_pos_ty = locate_z () in
+  let tyc = locate_globref ty in
+  let fc = locate_constant f in
+  let gc = locate_constant g in
+  let cty = mkRefC (CAst.(make (Qualid (qualid_of_reference ty).v)))
   in
-  let lqid = CAst.((qualid_of_reference ty).v) in
-  let crq = mkRefC (CAst.make (Qualid lqid)) in
-  let app x y = CAst.make (CApp ((None, x), [(y, None)])) in
-  let cref s = mkIdentC (Names.Id.of_string s) in
+  let app x y = mkAppC (x,[y]) in
+  let cref s = mkIdentC (Id.of_string s) in
   let arrow x y =
-    mkProdC ([CAst.make Anonymous], Default Decl_kinds.Explicit, x, y)
+    mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y)
   in
-  let _ =
-    (* checking "f" is of type "Z -> option ty" *)
-    let c =
-      mkCastC
-        (mkRefC f,
-         CastConv (arrow (cref "Z") (app (cref "option") crq)))
-    in
-    let (sigma, env) = Pfedit.get_current_context () in
-    Constrintern.intern_constr env sigma c
+  (* Check that [ty] is an inductive type *)
+  let constructors = match tyc with
+    | IndRef ind -> get_constructors ind
+    | ConstRef _ | ConstructRef _ | VarRef _ ->
+       CErrors.user_err
+        (pr_reference ty ++ str " is not an inductive type")
   in
-  let thr = Bigint.of_int waft in
-  let path = Nametab.path_of_global tyc in
-  match tyc with
-  | IndRef (sp, spi) ->
-      let gc =
-        let gq = qualid_of_reference g in
-        try Nametab.locate_constant CAst.(gq.v) with Not_found ->
-          Nametab.error_global_not_found gq
-      in
-      let _ =
-        (* checking "g" is of type "ty -> option Z" *)
-        let c =
-          mkCastC
-            (mkRefC g,
-             CastConv (arrow crq (app (cref "option") (cref "Z"))))
-        in
-        let (sigma, env) = Pfedit.get_current_context () in
-        Constrintern.interp_open_constr env sigma c
-      in
-      let env = Global.env () in
-      let patl =
-        let mc =
-          let mib = Environ.lookup_mind sp env in
-          let inds =
-            List.init (Array.length mib.Declarations.mind_packets)
-                      (fun x -> (sp, x))
-          in
-          let ind = List.hd inds in
-          let mip = mib.Declarations.mind_packets.(snd ind) in
-          mip.Declarations.mind_consnames
-        in
-        Array.to_list
-          (Array.mapi
-             (fun i c ->
-               DAst.make
-                 (Glob_term.GRef
-                    (ConstructRef ((sp, spi), i + 1), None)))
-             mc)
-      in
-      Lib.add_anonymous_leaf
-        (inNumeralNotation
-           (zposty, ty, fc, gc, sc, patl, thr, path))
-  | ConstRef _ | ConstructRef _ | VarRef _ ->
+  (* Is "f" of type "Z -> ty" or "Z -> option ty" ? *)
+  let of_z =
+    if has_type f (arrow (cref "Z") cty) then
+      Direct fc
+    else if has_type f (arrow (cref "Z") (app (cref "option") cty)) then
+      Option fc
+    else
+       CErrors.user_err
+        (pr_reference f ++ str " should goes from Z to " ++
+         pr_reference ty ++ str " or (option " ++ pr_reference ty ++ str ")")
+  in
+  (* Is "g" of type "ty -> Z" or "ty -> option Z" ? *)
+  let to_z =
+    if has_type g (arrow cty (cref "Z")) then
+      Direct gc
+    else if has_type g (arrow cty (app (cref "option") (cref "Z"))) then
+      Option gc
+    else
       CErrors.user_err
-        (str (string_of_reference ty) ++ str " is not an inductive type")
+        (pr_reference g ++ str " should goes from " ++
+         pr_reference ty ++ str " to Z or (option Z)")
+  in
+  Lib.add_anonymous_leaf
+    (inNumeralNotation
+       { num_ty = ty;
+         z_pos_ty;
+         of_z;
+         to_z;
+         scope;
+         constructors;
+         warning = (Bigint.of_int waft, warning_big_num ty);
+         path = Nametab.path_of_global tyc })
 
 open Stdarg