%token <int> IX
%token <string> ID STR
%token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS TE WTO STO CT
- %token GRAPH DECL AX CONG DEF TH GEN REQ OPEN CLOSE SORTS EOF
+ %token GRAPH MAIN DECL AX CONG DEF TH GEN REQ OPEN CLOSE SORTS EOF
%start entry
%type <Txt.command option> entry
| {}
| FS {}
;
+ main:
+ | { false }
+ | MAIN { true }
+ ;
comment:
- | { "" }
- | STR { $1 }
+ | { "", "" }
+ | STR { "", $1 }
+ | STR STR { $1, $2 }
;
ids:
| ID { [$1] }
;
xentity:
| GRAPH ID
- { T.Graph $2 }
- | decl level comment ID CN term
- { T.Entity ($1, $2, $4, $3, $6) }
- | def level comment ID EQ term
- { T.Entity ($1, $2, $4, $3, $6) }
- | def level comment ID EQ term CN term
- { T.Entity ($1, $2, $4, $3, T.Cast ($8, $6)) }
+ { T.Graph $2 }
+ | main decl level comment ID CN term
+ { T.Entity ($1, $2, $3, $5, $4, $7) }
+ | main def level comment ID EQ term
+ { T.Entity ($1, $2, $3, $5, $4, $7) }
+ | main def level comment ID EQ term CN term
+ { T.Entity ($1, $2, $3, $5, $4, T.Cast ($9, $7)) }
| GEN term
- { T.Generate [$2] }
+ { T.Generate [$2] }
| GEN terms
- { T.Generate $2 }
+ { T.Generate $2 }
| REQ ids
- { T.Require $2 }
+ { T.Require $2 }
| OPEN ID
- { T.Section (Some $2) }
+ { T.Section (Some $2) }
| CLOSE
- { T.Section None }
+ { T.Section None }
| SORTS sorts
- { T.Sorts $2 }
+ { T.Sorts $2 }
;
start:
| GRAPH {} | decl {} | def {} | GEN {} |