%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 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
- %nonassoc CP CB CA
+ %nonassoc CP CB CA
%right WTO STO
%%
hash:
;
abst:
- | ID CN term { $1, true, $3 }
- | TE CN term { "", false, $3 }
- | TE ID CN term { $2, false, $4 }
+ | ID CN term { $1, true, $3 }
+ | TE term { "", false, $2 }
+ | ID TE term { $1, false, $3 }
;
abbr:
| ID EQ term { $1, $3 }
| ids { T.Void $1 }
;
atom:
- | STAR IX { T.Sort $2 }
- | STAR ID { T.NSrt $2 }
- | hash IX { T.LRef ($2, 0) }
- | hash IX PLUS IX { T.LRef ($2, $4) }
- | hash ID { T.NRef $2 }
+ | STAR IX { T.Sort $2 }
+ | STAR ID { T.NSrt $2 }
+ | hash IX { T.LRef ($2, 0) }
+ | hash IX PLUS IX { T.LRef ($2, $4) }
+ | ID { T.NRef $1 }
+ | HASH ID { T.NRef $2 }
+ | atom OP term CP { T.Inst ($1, [$3]) }
+ | atom OP terms CP { T.Inst ($1, $3) }
;
term:
- | atom { $1 }
- | OA term CA fs term { T.Cast ($2, $5) }
- | OP terms CP fs term { T.Appl ($2, $5) }
- | atom OP terms CP { T.Inst ($1, $3) }
- | OB binder CB fs term { T.Bind ($2, $5) }
- | term WTO term { T.Impl (false, "", $1, $3) }
- | TE CN term WTO term { T.Impl (false, "", $3, $5) }
- | TE ID CN term WTO term { T.Impl (false, $2, $4, $6) }
- | term STO term { T.Impl (true, "", $1, $3) }
- | TE CN term STO term { T.Impl (true, "", $3, $5) }
- | TE ID CN term STO term { T.Impl (true, $2, $4, $6) }
+ | atom { $1 }
+ | OA term CA fs term { T.Cast ($2, $5) }
+ | OP term CP fs term { T.Appl ([$2], $5) }
+ | OP terms CP fs term { T.Appl ($2, $5) }
+ | OB binder CB fs term { T.Bind ($2, $5) }
+ | term WTO term { T.Impl (false, "", $1, $3) }
+ | ID TE term WTO term { T.Impl (false, $1, $3, $5) }
+ | term STO term { T.Impl (true, "", $1, $3) }
+ | ID TE term STO term { T.Impl (true, $1, $3, $5) }
+ | OP term CP { $2 }
;
terms:
- | term { [$1] }
+ | term CM term { [$1; $3] }
| term CM terms { $1 :: $3 }
;
{ Some (T.Entity ($1, $3, $2, $5)) }
| def comment ID EQ term CN term
{ Some (T.Entity ($1, $3, $2, T.Cast ($7, $5))) }
+ | GEN term
+ { Some (T.Generate [$2]) }
+ | GEN terms
+ { Some (T.Generate $2) }
+ | REQ ids
+ { Some (T.Require $2) }
| OPEN ID
{ Some (T.Section (Some $2)) }
| CLOSE
{ None }
;
start:
- | GRAPH {} | decl {} | def {}
- | OPEN {} | CLOSE {} | SORTS {} | EOF {}
+ | GRAPH {} | decl {} | def {} | GEN {} |
+ | REQ {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
;
entry:
| xentity { $1, false }