--- /dev/null
+/* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ */
+
+%{
+ module O = Options
+ module A = Aut
+
+ let _ = Parsing.set_trace !O.debug_parser
+%}
+ %token <int> NUM
+ %token <string> IDENT
+ %token EOF MINUS PLUS TIMES AT FS CN CM SC QT TD OP CP OB CB OA CA
+ %token TYPE PROP DEF EB E PN EXIT
+
+ %start entry
+ %type <Aut.command option> entry
+%%
+ path: MINUS {} | FS {} ;
+ oftype: CN {} | CM {} ;
+ star: TIMES {} | AT {} ;
+ sc: E {} | SC {} | CN {} ;
+ eof: SC {} | EOF {} ;
+
+ expand:
+ | { true }
+ | TD { false }
+ ;
+ local:
+ | { false }
+ | path { true }
+ ;
+
+ idents:
+ | IDENT { [$1] }
+ | IDENT path idents { $1 :: $3 }
+ ;
+ qid:
+ | IDENT { ($1, true, []) }
+ | IDENT QT QT { ($1, true, []) }
+ | IDENT QT local idents QT { ($1, $3, $4) }
+ ;
+ term:
+ | TYPE { A.Sort true }
+ | PROP { A.Sort false }
+ | qid { A.GRef ($1, []) }
+ | qid OP CP { A.GRef ($1, []) }
+ | qid OP terms CP { A.GRef ($1, $3) }
+ | OA term CA term { A.Appl ($2, $4) }
+ | OB IDENT oftype term CB term { A.Abst ($2, $4, $6) }
+ ;
+ terms:
+ | term { [$1] }
+ | term CM terms { $1 :: $3 }
+ ;
+
+ start:
+ | PLUS {} | MINUS {} | EXIT {} | eof {}
+ | star {} | IDENT {} | OB {}
+ ;
+ entity:
+ | PLUS IDENT { A.Section (Some (true, $2)) }
+ | PLUS TIMES IDENT { A.Section (Some (false, $3)) }
+ | MINUS IDENT { A.Section None }
+ | EXIT { A.Section None }
+ | star { A.Context None }
+ | qid star { A.Context (Some $1) }
+ | IDENT DEF EB sc term { A.Block ($1, $5) }
+ | IDENT sc term DEF EB { A.Block ($1, $3) }
+ | OB IDENT oftype term CB { A.Block ($2, $4) }
+ | IDENT DEF PN sc term { A.Decl ($1, $5) }
+ | IDENT sc term DEF PN { A.Decl ($1, $3) }
+ | IDENT DEF expand term sc term { A.Def ($1, $6, $3, $4) }
+ | IDENT sc term DEF expand term { A.Def ($1, $3, $5, $6) }
+ ;
+ entry:
+ | entity start { Some $1 }
+ | eof { None }
+ ;