1 files changed, 123 insertions, 0 deletions
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
new file mode 100644
index 00000000..dfb78890
--- /dev/null
+++ b/parsing/g_prim.mlg
@@ -0,0 +1,123 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+{
+
+open Names
+open Libnames
+
+open Pcoq
+open Pcoq.Prim
+
+let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"]
+let _ = List.iter CLexer.add_keyword prim_kw
+
+
+let local_make_qualid loc l id = make_qualid ~loc (DirPath.make l) id
+
+let my_int_of_string loc s =
+  try
+    int_of_string s
+  with Failure _ ->
+    CErrors.user_err ~loc (Pp.str "This number is too large.")
+
+}
+
+GRAMMAR EXTEND Gram
+  GLOBAL:
+    bigint natural integer identref name ident var preident
+    fullyqualid qualid reference dirpath ne_lstring
+    ne_string string lstring pattern_ident pattern_identref by_notation smart_global;
+  preident:
+    [ [ s = IDENT -> { s } ] ]
+  ;
+  ident:
+    [ [ s = IDENT -> { Id.of_string s } ] ]
+  ;
+  pattern_ident:
+    [ [ LEFTQMARK; id = ident -> { id } ] ]
+  ;
+  pattern_identref:
+    [ [ id = pattern_ident -> { CAst.make ~loc id } ] ]
+  ;
+  var: (* as identref, but interpret as a term identifier in ltac *)
+    [ [ id = ident -> { CAst.make ~loc id } ] ]
+  ;
+  identref:
+    [ [ id = ident -> { CAst.make ~loc id } ] ]
+  ;
+  field:
+    [ [ s = FIELD -> { Id.of_string s } ] ]
+  ;
+  fields:
+    [ [ id = field; f = fields -> { let (l,id') = f in (l@[id],id') }
+      | id = field -> { ([],id) }
+      ] ]
+  ;
+  fullyqualid:
+    [ [ id = ident; f=fields -> { let (l,id') = f in CAst.make ~loc @@ id::List.rev (id'::l) }
+      | id = ident -> { CAst.make ~loc [id] }
+      ] ]
+  ;
+  basequalid:
+    [ [ id = ident; f=fields -> { let (l,id') = f in  local_make_qualid loc (l@[id]) id' }
+      | id = ident -> { qualid_of_ident ~loc id }
+      ] ]
+  ;
+  name:
+    [ [ IDENT "_"  -> { CAst.make ~loc Anonymous }
+      | id = ident -> { CAst.make ~loc @@ Name id } ] ]
+  ;
+  reference:
+    [ [ id = ident; f = fields -> {
+        let (l,id') = f in
+        local_make_qualid loc (l@[id]) id' }
+      | id = ident -> { local_make_qualid loc [] id }
+      ] ]
+  ;
+  by_notation:
+    [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> { key } ] -> { (s, sc) } ] ]
+  ;
+  smart_global:
+    [ [ c = reference -> { CAst.make ~loc @@ Constrexpr.AN c }
+      | ntn = by_notation -> { CAst.make ~loc @@ Constrexpr.ByNotation ntn } ] ]
+  ;
+  qualid:
+    [ [ qid = basequalid -> { qid } ] ]
+  ;
+  ne_string:
+    [ [ s = STRING ->
+        { if s="" then CErrors.user_err ~loc (Pp.str"Empty string."); s }
+    ] ]
+  ;
+  ne_lstring:
+    [ [ s = ne_string -> { CAst.make ~loc s } ] ]
+  ;
+  dirpath:
+    [ [ id = ident; l = LIST0 field ->
+        { DirPath.make (List.rev (id::l)) } ] ]
+  ;
+  string:
+    [ [ s = STRING -> { s } ] ]
+  ;
+  lstring:
+    [ [ s = string -> { CAst.make ~loc s } ] ]
+  ;
+  integer:
+    [ [ i = INT      -> { my_int_of_string loc i }
+      | "-"; i = INT -> { - my_int_of_string loc i } ] ]
+  ;
+  natural:
+    [ [ i = INT -> { my_int_of_string loc i } ] ]
+  ;
+  bigint: (* Negative numbers are dealt with elsewhere *)
+    [ [ i = INT -> { i } ] ]
+  ;
+END