From dfcb15141a19db4f1cc61c14d1cdad0275009356 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:11:00 +0200
Subject: [numeral notation] Add a pre/postprocessing

This will enable to define numeral notation on non inductive by using
an inductive type as proxy and those translations to translate to/from
the actual type to the inductive type.
---
 plugins/syntax/string_notation.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/syntax/string_notation.ml')

diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
index e7ed0d8061..dbb0e92d5c 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -82,6 +82,7 @@ let vernac_string_notation local ty f g scope =
   in
   let o = { to_kind = to_kind;
             to_ty = to_ty;
+            to_post = [||];
             of_kind = of_kind;
             of_ty = of_ty;
             ty_name = ty;
-- 
cgit v1.2.3


From 3b766fd8859b692e3e93cf83bf87d393e32c572e Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:26:00 +0200
Subject: Merge numeral and string notation plugins

---
 plugins/syntax/string_notation.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/syntax/string_notation.ml')

diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
index dbb0e92d5c..98ea318c92 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Pp
-open Util
 open Names
 open Libnames
 open Constrexpr
-- 
cgit v1.2.3


From b6214bd4d5d3003e9b60411a717e84277feead24 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:27:00 +0200
Subject: [string notation] Handle parameterized inductives and non inductives

---
 plugins/syntax/string_notation.ml | 27 +++++++++++----------------
 1 file changed, 11 insertions(+), 16 deletions(-)

(limited to 'plugins/syntax/string_notation.ml')

diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
index 98ea318c92..774d59dda3 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -14,15 +14,10 @@ open Libnames
 open Constrexpr
 open Constrexpr_ops
 open Notation
+open Number
 
 (** * String notation *)
 
-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 -> GlobRef.ConstructRef (ind, j + 1)) mc)
-
 let qualid_of_ref n =
   n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
 
@@ -45,7 +40,7 @@ let type_error_of g ty =
     (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
      str " to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).")
 
-let vernac_string_notation local ty f g scope =
+let vernac_string_notation local ty f g via scope =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let app x y = mkAppC (x,[y]) in
@@ -55,14 +50,16 @@ let vernac_string_notation local ty f g scope =
   let coption = cref (q_option ()) in
   let opt r = app coption r in
   let clist_byte = app clist cbyte in
-  let tyc = Smartlocate.global_inductive_with_alias ty in
+  let ty_name = ty in
+  let ty, via =
+    match via with None -> ty, via | Some (ty', a) -> ty', Some (ty, a) in
+  let tyc, params = locate_global_inductive (via = None) ty in
   let to_ty = Smartlocate.global_with_alias f in
   let of_ty = Smartlocate.global_with_alias g in
   let cty = cref ty in
   let arrow x y =
     mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y)
   in
-  let constructors = get_constructors tyc in
   (* Check the type of f *)
   let to_kind =
     if has_type env sigma f (arrow clist_byte cty) then ListByte, Direct
@@ -79,12 +76,10 @@ let vernac_string_notation local ty f g scope =
     else if has_type env sigma g (arrow cty (opt cbyte)) then Byte, Option
     else type_error_of g ty
   in
-  let o = { to_kind = to_kind;
-            to_ty = to_ty;
-            to_post = [||];
-            of_kind = of_kind;
-            of_ty = of_ty;
-            ty_name = ty;
+  let to_post, pt_refs = match via with
+    | None -> elaborate_to_post_params env sigma tyc params
+    | Some (ty, l) -> elaborate_to_post_via env sigma ty tyc l in
+  let o = { to_kind; to_ty; to_post; of_kind; of_ty; ty_name;
             warning = () }
   in
   let i =
@@ -92,7 +87,7 @@ let vernac_string_notation local ty f g scope =
          pt_scope = scope;
          pt_interp_info = StringNotation o;
          pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[];
-         pt_refs = constructors;
+         pt_refs;
          pt_in_match = true }
   in
   enable_prim_token_interpretation i
-- 
cgit v1.2.3