From e30e864d61431a0145853fcf90b5f16b781f4a46 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 7 Nov 2018 21:19:05 -0500
Subject: Add `String Notation` vernacular like `Numeral Notation`

Users can now register string notations for custom inductives.

Much of the code and documentation was copied from numeral notations.

I chose to use a 256-constructor inductive for primitive string syntax
because (a) it is easy to convert between character codes and
constructors, and (b) it is more efficient than the existing `ascii`
type.

Some choices about proofs of the new `byte` type were made based on
efficiency.  For example, https://github.com/coq/coq/issues/8517 means
that we cannot simply use `Scheme Equality` for this type, and I have
taken some care to ensure that the proofs of decidable equality and
conversion are fast.  (Unfortunately, the `Init/Byte.v` file is the
slowest one in the prelude (it takes a couple of seconds to build), and
I'm not sure where the slowness is.)

In String.v, some uses of `0` as a `nat` were replaced by `O`, because
the file initially refused to check interactively otherwise (it
complained that `0` could not be interpreted in `string_scope` before
loading `Coq.Strings.String`).

There is unfortunately a decent amount of code duplication between
numeral notations and string notations.

I have not put too much thought into chosing names; most names have been
chosen to be similar to numeral notations, though I chose the name
`byte` from
https://github.com/coq/coq/issues/8483#issuecomment-421671785.

Unfortunately, this feature does not support declaring string syntax for
`list ascii`, unless that type is wrapped in a record or other inductive
type.  This is not a fundamental limitation; it should be relatively
easy for someone who knows the API of the reduction machinery in Coq to
extend both this and numeral notations to support any type whose hnf
starts with an inductive type.  (The reason for needing an inductive
type to bottom out at is that this is how the plugin determines what
constructors are the entry points for printing the given notation.
However, see also https://github.com/coq/coq/issues/8964 for
complications that are more likely to arise if inductive type families
are supported.)

N.B. I generated the long lists of constructors for the `byte` type with
short python scripts.

Closes #8853
---
 interp/notation.ml  | 201 +++++++++++++++++++++++++++++++++++++++++++++++++++-
 interp/notation.mli |  18 ++++-
 2 files changed, 215 insertions(+), 4 deletions(-)

(limited to 'interp')

diff --git a/interp/notation.ml b/interp/notation.ml
index db8ee5bc18..b6322c7441 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -395,11 +395,12 @@ let prim_token_uninterpreters =
 
 (*******************************************************)
 (* Numeral notation interpretation                     *)
-type numeral_notation_error =
+type numeral_or_string_notation_error =
   | UnexpectedTerm of Constr.t
   | UnexpectedNonOptionTerm of Constr.t
 
-exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error
+exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_or_string_notation_error
+exception StringNotationError of Environ.env * Evd.evar_map * numeral_or_string_notation_error
 
 type numnot_option =
   | Nop
@@ -419,8 +420,13 @@ type target_kind =
   | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
   | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
 
+type string_target_kind =
+  | ListByte
+  | Byte
+
 type option_kind = Option | Direct
 type conversion_kind = target_kind * option_kind
+type string_conversion_kind = string_target_kind * option_kind
 
 type numeral_notation_obj =
   { to_kind : conversion_kind;
@@ -430,6 +436,13 @@ type numeral_notation_obj =
     num_ty : Libnames.qualid; (* for warnings / error messages *)
     warning : numnot_option }
 
+type string_notation_obj =
+  { sto_kind : string_conversion_kind;
+    sto_ty : GlobRef.t;
+    sof_kind : string_conversion_kind;
+    sof_ty : GlobRef.t;
+    string_ty : Libnames.qualid (* for warnings / error messages *) }
+
 module Numeral = struct
 (** * Numeral notation *)
 
@@ -707,6 +720,185 @@ let uninterp o (Glob_term.AnyGlobConstr n) =
   | NotANumber -> None (* all other functions except big2raw *)
 end
 
+module Strings = struct
+(** * String 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 NotAString
+
+let qualid_of_ref n =
+  n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
+
+let q_list () = qualid_of_ref "core.list.type"
+let q_byte () = qualid_of_ref "core.byte.type"
+
+let unsafe_locate_ind q =
+  match Nametab.locate q with
+  | IndRef i -> i
+  | _ -> raise Not_found
+
+let locate_list () = unsafe_locate_ind (q_list ())
+let locate_byte () = unsafe_locate_ind (q_byte ())
+
+(***********************************************************************)
+
+(** ** Conversion between Coq [list Byte.byte] and internal raw string *)
+
+let coqbyte_of_char_code byte c =
+  mkConstruct (byte, 1 + c)
+
+let coqbyte_of_string ?loc byte s =
+  let p =
+    if Int.equal (String.length s) 1 then int_of_char s.[0]
+    else
+      if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
+      then int_of_string s
+      else
+       user_err ?loc ~hdr:"coqbyte_of_string"
+         (str "Expects a single character or a three-digits ascii code.") in
+  coqbyte_of_char_code byte p
+
+let coqbyte_of_char byte c = coqbyte_of_char_code byte (Char.code c)
+
+let make_ascii_string n =
+  if n>=32 && n<=126 then String.make 1 (char_of_int n)
+  else Printf.sprintf "%03d" n
+
+let char_code_of_coqbyte c =
+  match Constr.kind c with
+  | Construct ((_,c), _) -> c - 1
+  | _ -> raise NotAString
+
+let string_of_coqbyte c = make_ascii_string (char_code_of_coqbyte c)
+
+let coqlist_byte_of_string byte_ty list_ty str =
+  let cbyte = mkInd byte_ty in
+  let nil = mkApp (mkConstruct (list_ty, 1), [|cbyte|]) in
+  let cons x xs = mkApp (mkConstruct (list_ty, 2), [|cbyte; x; xs|]) in
+  let rec do_chars s i acc =
+    if i < 0 then acc
+    else
+      let b = coqbyte_of_char byte_ty s.[i] in
+      do_chars s (i-1) (cons b acc)
+  in
+  do_chars str (String.length str - 1) nil
+
+(* N.B. We rely on the fact that [nil] is the first constructor and [cons] is the second constructor, for [list] *)
+let string_of_coqlist_byte c =
+  let rec of_coqlist_byte_loop c buf =
+    match Constr.kind c with
+    | App (_nil, [|_ty|]) -> ()
+    | App (_cons, [|_ty;b;c|]) ->
+      let () = Buffer.add_char buf (Char.chr (char_code_of_coqbyte b)) in
+      of_coqlist_byte_loop c buf
+    | _ -> raise NotAString
+  in
+  let buf = Buffer.create 64 in
+  let () = of_coqlist_byte_loop c buf in
+  Buffer.contents buf
+
+(** 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 NotAString
+
+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 (StringNotationError(env,sigma,UnexpectedTerm c))
+
+let no_such_string ?loc ty =
+  CErrors.user_err ?loc
+   (str "Cannot interpret this string 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_string ?loc ty
+  | x -> Loc.raise ?loc (StringNotationError(env,sigma,UnexpectedNonOptionTerm c))
+
+let uninterp_option c =
+  match Constr.kind c with
+  | App (_Some, [| _; x |]) -> x
+  | _ -> raise NotAString
+
+let interp o ?loc n =
+  let byte_ty = locate_byte () in
+  let list_ty = locate_list () in
+  let c = match fst o.sto_kind with
+    | ListByte -> coqlist_byte_of_string byte_ty list_ty n
+    | Byte -> coqbyte_of_string ?loc byte_ty n
+  in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let sigma,to_ty = Evd.fresh_global env sigma o.sto_ty in
+  let to_ty = EConstr.Unsafe.to_constr to_ty in
+  let res = eval_constr_app env sigma to_ty c in
+  match snd o.sto_kind with
+  | Direct -> glob_of_constr ?loc env sigma res
+  | Option -> interp_option o.string_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.sof_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.sof_kind == Direct then c else uninterp_option c in
+    match fst o.sof_kind with
+    | ListByte -> Some (string_of_coqlist_byte c)
+    | Byte -> Some (string_of_coqbyte c)
+  with
+  | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *)
+  | NotAString -> None (* all other functions except big2raw *)
+end
+
 (* A [prim_token_infos], which is synchronized with the document
    state, either contains a unique id pointing to an unsynchronized
    prim token function, or a numeral notation object describing how to
@@ -718,6 +910,7 @@ end
 type prim_token_interp_info =
     Uid of prim_token_uid
   | NumeralNotation of numeral_notation_obj
+  | StringNotation of string_notation_obj
 
 type prim_token_infos = {
   pt_local : bool; (** Is this interpretation local? *)
@@ -942,6 +1135,7 @@ let find_prim_token check_allowed ?loc p sc =
   let interp = match info with
     | Uid uid -> Hashtbl.find prim_token_interpreters uid
     | NumeralNotation o -> InnerPrimToken.RawNumInterp (Numeral.interp o)
+    | StringNotation o -> InnerPrimToken.StringInterp (Strings.interp o)
   in
   let pat = InnerPrimToken.do_interp ?loc interp p in
   check_allowed pat;
@@ -1122,6 +1316,7 @@ let uninterp_prim_token c =
        let uninterp = match info with
          | Uid uid -> Hashtbl.find prim_token_uninterpreters uid
          | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o)
+         | StringNotation o -> InnerPrimToken.StringUninterp (Strings.uninterp o)
        in
        match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with
        | None -> raise Notation_ops.No_match
@@ -1141,6 +1336,8 @@ let availability_of_prim_token n printer_scope local_scopes =
       match n, uid with
       | Numeral _, NumeralNotation _ -> true
       | _, NumeralNotation _ -> false
+      | String _, StringNotation _ -> true
+      | _, StringNotation _ -> false
       | _, Uid uid ->
         let interp = Hashtbl.find prim_token_interpreters uid in
         match n, interp with
diff --git a/interp/notation.mli b/interp/notation.mli
index 734198bbf6..6880b9a2cd 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -104,11 +104,12 @@ val register_string_interpretation :
 
 (** * Numeral notation *)
 
-type numeral_notation_error =
+type numeral_or_string_notation_error =
   | UnexpectedTerm of Constr.t
   | UnexpectedNonOptionTerm of Constr.t
 
-exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error
+exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_or_string_notation_error
+exception StringNotationError of Environ.env * Evd.evar_map * numeral_or_string_notation_error
 
 type numnot_option =
   | Nop
@@ -128,8 +129,13 @@ type target_kind =
   | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
   | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
 
+type string_target_kind =
+  | ListByte
+  | Byte
+
 type option_kind = Option | Direct
 type conversion_kind = target_kind * option_kind
+type string_conversion_kind = string_target_kind * option_kind
 
 type numeral_notation_obj =
   { to_kind : conversion_kind;
@@ -139,9 +145,17 @@ type numeral_notation_obj =
     num_ty : Libnames.qualid; (* for warnings / error messages *)
     warning : numnot_option }
 
+type string_notation_obj =
+  { sto_kind : string_conversion_kind;
+    sto_ty : GlobRef.t;
+    sof_kind : string_conversion_kind;
+    sof_ty : GlobRef.t;
+    string_ty : Libnames.qualid (* for warnings / error messages *) }
+
 type prim_token_interp_info =
     Uid of prim_token_uid
   | NumeralNotation of numeral_notation_obj
+  | StringNotation of string_notation_obj
 
 type prim_token_infos = {
   pt_local : bool; (** Is this interpretation local? *)
-- 
cgit v1.2.3


From f7992de2dc4ce0091197b9476779fc120a2fd9ec Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 27 Nov 2018 21:03:57 -0500
Subject: Factor out common code in numeral/string notations

As per https://github.com/coq/coq/pull/8965#issuecomment-441440779
---
 interp/notation.ml  | 302 ++++++++++++++++++++--------------------------------
 interp/notation.mli |  28 ++---
 2 files changed, 124 insertions(+), 206 deletions(-)

(limited to 'interp')

diff --git a/interp/notation.ml b/interp/notation.ml
index b6322c7441..6a305c24af 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -395,12 +395,11 @@ let prim_token_uninterpreters =
 
 (*******************************************************)
 (* Numeral notation interpretation                     *)
-type numeral_or_string_notation_error =
+type prim_token_notation_error =
   | UnexpectedTerm of Constr.t
   | UnexpectedNonOptionTerm of Constr.t
 
-exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_or_string_notation_error
-exception StringNotationError of Environ.env * Evd.evar_map * numeral_or_string_notation_error
+exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_token_notation_error
 
 type numnot_option =
   | Nop
@@ -425,27 +424,21 @@ type string_target_kind =
   | Byte
 
 type option_kind = Option | Direct
-type conversion_kind = target_kind * option_kind
-type string_conversion_kind = string_target_kind * option_kind
+type 'target conversion_kind = 'target * option_kind
 
-type numeral_notation_obj =
-  { to_kind : conversion_kind;
+type ('target, 'warning) prim_token_notation_obj =
+  { to_kind : 'target conversion_kind;
     to_ty : GlobRef.t;
-    of_kind : conversion_kind;
+    of_kind : 'target conversion_kind;
     of_ty : GlobRef.t;
-    num_ty : Libnames.qualid; (* for warnings / error messages *)
-    warning : numnot_option }
+    ty_name : Libnames.qualid; (* for warnings / error messages *)
+    warning : 'warning }
 
-type string_notation_obj =
-  { sto_kind : string_conversion_kind;
-    sto_ty : GlobRef.t;
-    sof_kind : string_conversion_kind;
-    sof_ty : GlobRef.t;
-    string_ty : Libnames.qualid (* for warnings / error messages *) }
-
-module Numeral = struct
-(** * Numeral notation *)
+type numeral_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
+type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj
 
+module PrimTokenNotation = struct
+(** * Code shared between Numeral notation and String notation *)
 (** Reduction
 
     The constr [c] below isn't necessarily well-typed, since we
@@ -474,7 +467,69 @@ let eval_constr env sigma (c : Constr.t) =
 let eval_constr_app env sigma c1 c2 =
   eval_constr env sigma (mkApp (c1,[| c2 |]))
 
-exception NotANumber
+exception NotAValidPrimToken
+
+(** 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 NotAValidPrimToken
+
+let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with
+  | App (c, ca) ->
+      let c = glob_of_constr token_kind ?loc env sigma c in
+      let cel = List.map (glob_of_constr token_kind ?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 (PrimTokenNotationError(token_kind,env,sigma,UnexpectedTerm c))
+
+let no_such_prim_token uninterpreted_token_kind ?loc ty =
+  CErrors.user_err ?loc
+   (str ("Cannot interpret this "^uninterpreted_token_kind^" as a value of type ") ++
+    pr_qualid ty)
+
+let interp_option uninterpreted_token_kind token_kind ty ?loc env sigma c =
+  match Constr.kind c with
+  | App (_Some, [| _; c |]) -> glob_of_constr token_kind ?loc env sigma c
+  | App (_None, [| _ |]) -> no_such_prim_token uninterpreted_token_kind ?loc ty
+  | x -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedNonOptionTerm c))
+
+let uninterp_option c =
+  match Constr.kind c with
+  | App (_Some, [| _; x |]) -> x
+  | _ -> raise NotAValidPrimToken
+
+let uninterp to_raw 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
+    Some (to_raw (fst o.of_kind, c))
+  with
+  | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *)
+  | NotAValidPrimToken -> None (* all other functions except big2raw *)
+
+end
+
+module Numeral = struct
+(** * Numeral notation *)
+open PrimTokenNotation
 
 let warn_large_num =
   CWarnings.create ~name:"large-number" ~category:"numbers"
@@ -548,15 +603,15 @@ let rawnum_of_coquint c =
         | Construct ((_,n), _) (* D0 to D9 *) ->
            let () = Buffer.add_char buf (char_of_digit n) in
            of_uint_loop a buf
-        | _ -> raise NotANumber)
-    | _ -> raise NotANumber
+        | _ -> raise NotAValidPrimToken)
+    | _ -> raise NotAValidPrimToken
   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
+    raise NotAValidPrimToken
   else Buffer.contents buf
 
 let rawnum_of_coqint c =
@@ -565,8 +620,8 @@ let rawnum_of_coqint 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
+      | _ -> raise NotAValidPrimToken)
+  | _ -> raise NotAValidPrimToken
 
 
 (***********************************************************************)
@@ -596,9 +651,9 @@ let rec bigint_of_pos c = match Constr.kind c with
           | 2 -> (* xO *) Bigint.mult_2 (bigint_of_pos d)
           | n -> assert false (* no other constructor of type positive *)
           end
-      | x -> raise NotANumber
+      | x -> raise NotAValidPrimToken
       end
-  | x -> raise NotANumber
+  | x -> raise NotAValidPrimToken
 
 (** Now, [Z] from/to bigint *)
 
@@ -623,51 +678,9 @@ let bigint_of_z z = match Constr.kind z with
           | 3 -> (* Zneg *) Bigint.neg (bigint_of_pos d)
           | n -> assert false (* no other constructor of type Z *)
           end
-      | _ -> raise NotANumber
+      | _ -> raise NotAValidPrimToken
       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
+  | _ -> raise NotAValidPrimToken
 
 let big2raw n =
   if Bigint.is_pos_or_zero n then (Bigint.to_string n, true)
@@ -679,13 +692,13 @@ let raw2big (n,s) =
 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
+     warn_large_num o.ty_name
   | _ -> ()
   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
+    | UInt _ (* n <= 0 *) -> no_such_prim_token "number" ?loc o.ty_name
     | Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big n)
   in
   let env = Global.env () in
@@ -694,64 +707,26 @@ let interp o ?loc n =
   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|]))
+     warn_abstract_large_num (o.ty_name,o.to_ty);
+     glob_of_constr "numeral" ?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 *)
+     | Direct -> glob_of_constr "numeral" ?loc env sigma res
+     | Option -> interp_option "number" "numeral" o.ty_name ?loc env sigma res
+
+let uninterp o n =
+  PrimTokenNotation.uninterp
+    begin function
+      | (Int _, c) -> rawnum_of_coqint c
+      | (UInt _, c) -> (rawnum_of_coquint c, true)
+      | (Z _, c) -> big2raw (bigint_of_z c)
+    end o n
 end
 
 module Strings = struct
 (** * String 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 NotAString
+open PrimTokenNotation
 
 let qualid_of_ref n =
   n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
@@ -794,7 +769,7 @@ let make_ascii_string n =
 let char_code_of_coqbyte c =
   match Constr.kind c with
   | Construct ((_,c), _) -> c - 1
-  | _ -> raise NotAString
+  | _ -> raise NotAValidPrimToken
 
 let string_of_coqbyte c = make_ascii_string (char_code_of_coqbyte c)
 
@@ -818,85 +793,34 @@ let string_of_coqlist_byte c =
     | App (_cons, [|_ty;b;c|]) ->
       let () = Buffer.add_char buf (Char.chr (char_code_of_coqbyte b)) in
       of_coqlist_byte_loop c buf
-    | _ -> raise NotAString
+    | _ -> raise NotAValidPrimToken
   in
   let buf = Buffer.create 64 in
   let () = of_coqlist_byte_loop c buf in
   Buffer.contents buf
 
-(** 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 NotAString
-
-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 (StringNotationError(env,sigma,UnexpectedTerm c))
-
-let no_such_string ?loc ty =
-  CErrors.user_err ?loc
-   (str "Cannot interpret this string 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_string ?loc ty
-  | x -> Loc.raise ?loc (StringNotationError(env,sigma,UnexpectedNonOptionTerm c))
-
-let uninterp_option c =
-  match Constr.kind c with
-  | App (_Some, [| _; x |]) -> x
-  | _ -> raise NotAString
-
 let interp o ?loc n =
   let byte_ty = locate_byte () in
   let list_ty = locate_list () in
-  let c = match fst o.sto_kind with
+  let c = match fst o.to_kind with
     | ListByte -> coqlist_byte_of_string byte_ty list_ty n
     | Byte -> coqbyte_of_string ?loc byte_ty n
   in
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let sigma,to_ty = Evd.fresh_global env sigma o.sto_ty in
+  let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in
   let to_ty = EConstr.Unsafe.to_constr to_ty in
   let res = eval_constr_app env sigma to_ty c in
-  match snd o.sto_kind with
-  | Direct -> glob_of_constr ?loc env sigma res
-  | Option -> interp_option o.string_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.sof_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.sof_kind == Direct then c else uninterp_option c in
-    match fst o.sof_kind with
-    | ListByte -> Some (string_of_coqlist_byte c)
-    | Byte -> Some (string_of_coqbyte c)
-  with
-  | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *)
-  | NotAString -> None (* all other functions except big2raw *)
+  match snd o.to_kind with
+  | Direct -> glob_of_constr "string" ?loc env sigma res
+  | Option -> interp_option "string" "string" o.ty_name ?loc env sigma res
+
+let uninterp o n =
+  PrimTokenNotation.uninterp
+    begin function
+      | (ListByte, c) -> string_of_coqlist_byte c
+      | (Byte, c) -> string_of_coqbyte c
+    end o n
 end
 
 (* A [prim_token_infos], which is synchronized with the document
diff --git a/interp/notation.mli b/interp/notation.mli
index 6880b9a2cd..c0ff1a1ac3 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -104,12 +104,11 @@ val register_string_interpretation :
 
 (** * Numeral notation *)
 
-type numeral_or_string_notation_error =
+type prim_token_notation_error =
   | UnexpectedTerm of Constr.t
   | UnexpectedNonOptionTerm of Constr.t
 
-exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_or_string_notation_error
-exception StringNotationError of Environ.env * Evd.evar_map * numeral_or_string_notation_error
+exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_token_notation_error
 
 type numnot_option =
   | Nop
@@ -134,23 +133,18 @@ type string_target_kind =
   | Byte
 
 type option_kind = Option | Direct
-type conversion_kind = target_kind * option_kind
-type string_conversion_kind = string_target_kind * option_kind
+type 'target conversion_kind = 'target * option_kind
 
-type numeral_notation_obj =
-  { to_kind : conversion_kind;
+type ('target, 'warning) prim_token_notation_obj =
+  { to_kind : 'target conversion_kind;
     to_ty : GlobRef.t;
-    of_kind : conversion_kind;
+    of_kind : 'target conversion_kind;
     of_ty : GlobRef.t;
-    num_ty : Libnames.qualid; (* for warnings / error messages *)
-    warning : numnot_option }
-
-type string_notation_obj =
-  { sto_kind : string_conversion_kind;
-    sto_ty : GlobRef.t;
-    sof_kind : string_conversion_kind;
-    sof_ty : GlobRef.t;
-    string_ty : Libnames.qualid (* for warnings / error messages *) }
+    ty_name : Libnames.qualid; (* for warnings / error messages *)
+    warning : 'warning }
+
+type numeral_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
+type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj
 
 type prim_token_interp_info =
     Uid of prim_token_uid
-- 
cgit v1.2.3