Add support for Sorts in numeral notations

5 files changed, 118 insertions, 4 deletions

diff --git a/doc/changelog/03-notations/09883-numeral-notations-sorts.rst b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst
new file mode 100644
index 0000000000..abc5a516ae
--- /dev/null
+++ b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst
@@ -0,0 +1,4 @@
+- Numeral Notations now support sorts in the input to printing
+  functions (e.g., numeral notations can be defined for terms
+  containing things like `@cons Set nat nil`).  (`#9883
+  <https://github.com/coq/coq/pull/9883>`_, by Jason Gross).
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index a28ce600ca..02910e603a 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1442,8 +1442,8 @@ Numeral notations
      of the resulting term will be refreshed.
 
      Note that only fully-reduced ground terms (terms containing only
-     function application, constructors, inductive type families, and
-     primitive integers) will be considered for printing.
+     function application, constructors, inductive type families,
+     sorts, and primitive integers) will be considered for printing.
 
    .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num).
 
@@ -1592,8 +1592,8 @@ String notations
      of the resulting term will be refreshed.
 
      Note that only fully-reduced ground terms (terms containing only
-     function application, constructors, inductive type families, and
-     primitive integers) will be considered for printing.
+     function application, constructors, inductive type families,
+     sorts, and primitive integers) will be considered for printing.
 
    .. exn:: Cannot interpret this string as a value of type @type
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 70d3e4175e..c157cf43fb 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -503,6 +503,9 @@ let rec constr_of_glob env sigma g = match DAst.get g with
       let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in
       sigma,mkApp (c, Array.of_list cl)
   | Glob_term.GInt i -> sigma, mkInt i
+  | Glob_term.GSort gs ->
+      let sigma,c = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family gs) in
+      sigma,mkSort c
   | _ ->
       raise NotAValidPrimToken
 
@@ -516,6 +519,10 @@ let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with
   | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (GlobRef.IndRef ind, None))
   | Var id -> DAst.make ?loc (Glob_term.GRef (GlobRef.VarRef id, None))
   | Int i -> DAst.make ?loc (Glob_term.GInt i)
+  | Sort Sorts.SProp -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GSProp, 0]))
+  | Sort Sorts.Prop -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GProp, 0]))
+  | Sort Sorts.Set -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GSet, 0]))
+  | Sort (Sorts.Type _) -> DAst.make ?loc (Glob_term.GSort (Glob_term.UAnonymous {rigid=true}))
   | _ -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedTerm c))
 
 let no_such_prim_token uninterpreted_token_kind ?loc ty =
diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out
index 460c77879c..505dc52ebe 100644
--- a/test-suite/output/NumeralNotations.out
+++ b/test-suite/output/NumeralNotations.out
@@ -180,3 +180,41 @@ let v := 4%Zlike in v : Zlike
      : Zlike
 0%Zlike
      : Zlike
+let v := 0%kt in v : ty
+     : ty
+let v := 1%kt in v : ty
+     : ty
+let v := 2%kt in v : ty
+     : ty
+let v := 3%kt in v : ty
+     : ty
+let v := 4%kt in v : ty
+     : ty
+let v := 5%kt in v : ty
+     : ty
+The command has indeed failed with message:
+Cannot interpret this number as a value of type ty
+     = 0%kt
+     : ty
+     = 1%kt
+     : ty
+     = 2%kt
+     : ty
+     = 3%kt
+     : ty
+     = 4%kt
+     : ty
+     = 5%kt
+     : ty
+let v : ty := Build_ty Empty_set zero in v : ty
+     : ty
+let v : ty := Build_ty unit one in v : ty
+     : ty
+let v : ty := Build_ty bool two in v : ty
+     : ty
+let v : ty := Build_ty Prop prop in v : ty
+     : ty
+let v : ty := Build_ty Set set in v : ty
+     : ty
+let v : ty := Build_ty Type type in v : ty
+     : ty
diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v
index 44805ad09d..c306b15ef3 100644
--- a/test-suite/output/NumeralNotations.v
+++ b/test-suite/output/NumeralNotations.v
@@ -391,3 +391,68 @@ Module Test19.
   Check {| summands := (cons 1 (cons 2 (cons (-1) nil)))%Z |}.
   Check {| summands := nil |}.
 End Test19.
+
+Module Test20.
+  (** Test Sorts *)
+  Local Set Universe Polymorphism.
+  Inductive known_type : Type -> Type :=
+  | prop : known_type Prop
+  | set : known_type Set
+  | type : known_type Type
+  | zero : known_type Empty_set
+  | one : known_type unit
+  | two : known_type bool.
+
+  Existing Class known_type.
+  Existing Instances zero one two prop.
+  Existing Instance set | 2.
+  Existing Instance type | 4.
+
+  Record > ty := { t : Type ; kt : known_type t }.
+
+  Definition ty_of_uint (x : Decimal.uint) : option ty
+    := match Nat.of_uint x with
+       | 0 => @Some ty zero
+       | 1 => @Some ty one
+       | 2 => @Some ty two
+       | 3 => @Some ty prop
+       | 4 => @Some ty set
+       | 5 => @Some ty type
+       | _ => None
+       end.
+  Definition uint_of_ty (x : ty) : Decimal.uint
+    := Nat.to_uint match kt x with
+                   | prop => 3
+                   | set => 4
+                   | type => 5
+                   | zero => 0
+                   | one => 1
+                   | two => 2
+                   end.
+
+  Declare Scope kt_scope.
+  Delimit Scope kt_scope with kt.
+
+  Numeral Notation ty ty_of_uint uint_of_ty : kt_scope.
+
+  Check let v := 0%kt in v : ty.
+  Check let v := 1%kt in v : ty.
+  Check let v := 2%kt in v : ty.
+  Check let v := 3%kt in v : ty.
+  Check let v := 4%kt in v : ty.
+  Check let v := 5%kt in v : ty.
+  Fail Check let v := 6%kt in v : ty.
+  Eval cbv in (_ : known_type Empty_set) : ty.
+  Eval cbv in (_ : known_type unit) : ty.
+  Eval cbv in (_ : known_type bool) : ty.
+  Eval cbv in (_ : known_type Prop) : ty.
+  Eval cbv in (_ : known_type Set) : ty.
+  Eval cbv in (_ : known_type Type) : ty.
+  Local Set Printing All.
+  Check let v := 0%kt in v : ty.
+  Check let v := 1%kt in v : ty.
+  Check let v := 2%kt in v : ty.
+  Check let v := 3%kt in v : ty.
+  Check let v := 4%kt in v : ty.
+  Check let v := 5%kt in v : ty.
+End Test20.