+++ /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 G = Options
- module A = Aut
-
- let _ = Parsing.set_trace !G.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 }
- ;