diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /toplevel/g_toplevel.mlg | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
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 00000000..5aba3d6b --- /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 Entry.t +end = struct + let gec_vernac s = 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.Entry.parse vernac_toplevel pa + +} |