diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-02 15:06:17 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-02 15:06:17 +0200 |
commit | 02fe76c0c1c3f01c6fb4310dd4450b35f43005da (patch) | |
tree | 1d1c7c47fff5688105d0f868f9ab89d479ede899 /toplevel/g_toplevel.mlg | |
parent | f6f606232ae3c32e5c90d4fd427721875529b777 (diff) | |
parent | 47bbe39d480f02dc92e4856fa8d872f52b9903a4 (diff) |
Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension points of Camlp5
Diffstat (limited to 'toplevel/g_toplevel.mlg')
-rw-r--r-- | toplevel/g_toplevel.mlg | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg new file mode 100644 index 000000000..53d3eef23 --- /dev/null +++ b/toplevel/g_toplevel.mlg @@ -0,0 +1,54 @@ +(************************************************************************) +(* * 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 Pcoq +open Pcoq.Prim +open Vernacexpr + +(* Vernaculars specific to the toplevel *) +type vernac_toplevel = + | VernacBacktrack of int * int * int + | VernacDrop + | VernacQuit + | VernacControl of vernac_control + +module Toplevel_ : sig + val vernac_toplevel : vernac_toplevel CAst.t Gram.entry +end = struct + let gec_vernac s = Gram.entry_create ("toplevel:" ^ s) + let vernac_toplevel = gec_vernac "vernac_toplevel" +end + +open Toplevel_ + +} + +GRAMMAR EXTEND Gram + GLOBAL: vernac_toplevel; + vernac_toplevel: FIRST + [ [ IDENT "Drop"; "." -> { CAst.make VernacDrop } + | IDENT "Quit"; "." -> { CAst.make VernacQuit } + | IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." -> + { CAst.make (VernacBacktrack (n,m,p)) } + | cmd = Pvernac.main_entry -> + { match cmd with + | None -> raise Stm.End_of_input + | Some (loc,c) -> CAst.make ~loc (VernacControl c) } + ] + ] + ; +END + +{ + +let parse_toplevel pa = Pcoq.Gram.entry_parse vernac_toplevel pa + +} |