%{
module A = Aut
+
+ let debug = false
+
+ let _ = Parsing.set_trace debug
%}
%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 book
- %type <Aut.entity list> book
+ %start entry
+ %type <Aut.command option * bool> entry
%%
path: MINUS {} | FS {} ;
oftype: CN {} | CM {} ;
| 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) }
- ;
- entities:
- | { [] }
- | entity entities { $1 :: $2 }
- ;
- book:
- | entities eof { $1 }
+ | PLUS IDENT { Some (A.Section (Some (true, $2))) }
+ | PLUS TIMES IDENT { Some (A.Section (Some (false, $3))) }
+ | MINUS IDENT { Some (A.Section None) }
+ | EXIT { Some (A.Section None) }
+ | star { Some (A.Context None) }
+ | qid star { Some (A.Context (Some $1)) }
+ | IDENT DEF EB sc term { Some (A.Block ($1, $5)) }
+ | IDENT sc term DEF EB { Some (A.Block ($1, $3)) }
+ | OB IDENT oftype term CB { Some (A.Block ($2, $4)) }
+ | IDENT DEF PN sc term { Some (A.Decl ($1, $5)) }
+ | IDENT sc term DEF PN { Some (A.Decl ($1, $3)) }
+ | IDENT DEF expand term sc term { Some (A.Def ($1, $6, $3, $4)) }
+ | IDENT sc term DEF expand term { Some (A.Def ($1, $3, $5, $6)) }
+ | eof { None }
;
+ entry:
+ | entity { $1, false }
+ | entity start { $1, true }
+