From aaad965a84d97fdd64367138e692ebd49321ccd9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 24 Oct 2017 11:22:23 +0200 Subject: Port g_prim to the homebrew GEXTEND parser. --- parsing/g_prim.ml4 | 122 -------------------------------------------------- parsing/g_prim.mlg | 127 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 127 insertions(+), 122 deletions(-) delete mode 100644 parsing/g_prim.ml4 create mode 100644 parsing/g_prim.mlg (limited to 'parsing') diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 deleted file mode 100644 index 91dce27fe..000000000 --- a/parsing/g_prim.ml4 +++ /dev/null @@ -1,122 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 1024 * 2048 then raise Exit; - n - with Failure _ | Exit -> - CErrors.user_err ~loc (Pp.str "Cannot support a so large number.") - -GEXTEND 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:!@loc id ] ] - ; - var: (* as identref, but interpret as a term identifier in ltac *) - [ [ id = ident -> CAst.make ~loc:!@loc id ] ] - ; - identref: - [ [ id = ident -> CAst.make ~loc:!@loc id ] ] - ; - field: - [ [ s = FIELD -> Id.of_string s ] ] - ; - fields: - [ [ id = field; (l,id') = fields -> (l@[id],id') - | id = field -> ([],id) - ] ] - ; - fullyqualid: - [ [ id = ident; (l,id')=fields -> CAst.make ~loc:!@loc @@ id::List.rev (id'::l) - | id = ident -> CAst.make ~loc:!@loc [id] - ] ] - ; - basequalid: - [ [ id = ident; (l,id')=fields -> local_make_qualid !@loc (l@[id]) id' - | id = ident -> qualid_of_ident ~loc:!@loc id - ] ] - ; - name: - [ [ IDENT "_" -> CAst.make ~loc:!@loc Anonymous - | id = ident -> CAst.make ~loc:!@loc @@ Name id ] ] - ; - reference: - [ [ id = ident; (l,id') = fields -> - 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:!@loc @@ Constrexpr.AN c - | ntn = by_notation -> CAst.make ~loc:!@loc @@ Constrexpr.ByNotation ntn ] ] - ; - qualid: - [ [ qid = basequalid -> qid ] ] - ; - ne_string: - [ [ s = STRING -> - if s="" then CErrors.user_err ~loc:!@loc (Pp.str"Empty string."); s - ] ] - ; - ne_lstring: - [ [ s = ne_string -> CAst.make ~loc:!@loc s ] ] - ; - dirpath: - [ [ id = ident; l = LIST0 field -> - DirPath.make (List.rev (id::l)) ] ] - ; - string: - [ [ s = STRING -> s ] ] - ; - lstring: - [ [ s = string -> (CAst.make ~loc:!@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 diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg new file mode 100644 index 000000000..774db97f2 --- /dev/null +++ b/parsing/g_prim.mlg @@ -0,0 +1,127 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* 1024 * 2048 then raise Exit; + n + with Failure _ | Exit -> + CErrors.user_err ~loc (Pp.str "Cannot support a so large number.") + +} + +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 -- cgit v1.2.3