*/
%{
+ module O = Options
module T = Txt
- let debug = false
-
- let _ = Parsing.set_trace debug
+ let _ = Parsing.set_trace !O.debug_parser
%}
%token <int> IX
%token <string> ID STR
%token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS TE WTO STO
- %token REQUIRE GRAPH DECL AX DEF TH OPEN CLOSE SORTS EOF
+ %token GRAPH DECL AX DEF TH GEN REQ OPEN CLOSE SORTS EOF
%start entry
- %type <Txt.command option * bool> entry
+ %type <Txt.command option> entry
%nonassoc CP CB CA
%right WTO STO
| TH { T.Th }
;
xentity:
- | REQUIRE ids
- { Some (T.Require $2) }
| GRAPH ID
- { Some (T.Graph $2) }
+ { T.Graph $2 }
| decl comment ID CN term
- { Some (T.Entity ($1, $3, $2, $5)) }
+ { T.Entity ($1, $3, $2, $5) }
| def comment ID EQ term
- { Some (T.Entity ($1, $3, $2, $5)) }
+ { T.Entity ($1, $3, $2, $5) }
| def comment ID EQ term CN term
- { Some (T.Entity ($1, $3, $2, T.Cast ($7, $5))) }
+ { T.Entity ($1, $3, $2, T.Cast ($7, $5)) }
+ | GEN term
+ { T.Generate [$2] }
+ | GEN terms
+ { T.Generate $2 }
+ | REQ ids
+ { T.Require $2 }
| OPEN ID
- { Some (T.Section (Some $2)) }
+ { T.Section (Some $2) }
| CLOSE
- { Some (T.Section None) }
+ { T.Section None }
| SORTS sorts
- { Some (T.Sorts $2) }
- | EOF
- { None }
+ { T.Sorts $2 }
;
start:
- | GRAPH {} | decl {} | def {}
- | REQUIRE {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
+ | GRAPH {} | decl {} | def {} | GEN {} |
+ | REQ {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
;
entry:
- | xentity { $1, false }
- | xentity start { $1, true }
+ | xentity start { Some $1 }
+ | EOF { None }
;