%}
%token <int> IX
%token <string> ID STR
- %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS
- %token OPEN CLOSE GLOBAL EOF
+ %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS TE WTO STO
+ %token GRAPH DECL AX DEF TH GEN REQ OPEN CLOSE SORTS EOF
%start entry
- %type <Txt.entity option * bool> entry
+ %type <Txt.command option * bool> entry
+
+ %nonassoc CP CB CA
+ %right WTO STO
%%
hash:
| {}
| ID { [$1] }
| ID CM ids { $1 :: $3 }
;
+ sort:
+ | ID { None, $1 }
+ | IX ID { Some $1, $2 }
+ ;
+ sorts:
+ | sort { [$1] }
+ | sort CM sorts { $1 :: $3 }
+ ;
abst:
- | ID CN term { $1, $3 }
+ | 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.Appl (List.rev $3, $1) }
- | OB binder CB fs term { T.Bind ($2, $5) }
+ | 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 }
;
- start: OPEN {} | CLOSE {} | GLOBAL {} | EOF {} ;
+ decl:
+ | DECL { T.Decl }
+ | AX { T.Ax }
+ ;
+ def:
+ | DEF { T.Def }
+ | TH { T.Th }
+ ;
xentity:
- | OPEN ID { Some (T.Section (Some $2)) }
- | CLOSE { Some (T.Section None) }
- | GLOBAL comment ID CN term { Some (T.Global (false, $3, $2, $5)) }
- | GLOBAL comment ID EQ term { Some (T.Global (true, $3, $2, $5)) }
- | GLOBAL comment ID EQ term CN term { Some (T.Global (true, $3, $2, T.Cast ($7, $5))) }
- | EOF { None }
- ;
- entry:
+ | GRAPH ID
+ { Some (T.Graph $2) }
+ | decl comment ID CN term
+ { Some (T.Entity ($1, $3, $2, $5)) }
+ | def comment ID EQ term
+ { 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
+ { Some (T.Section None) }
+ | SORTS sorts
+ { Some (T.Sorts $2) }
+ | EOF
+ { None }
+ ;
+ start:
+ | GRAPH {} | decl {} | def {} | GEN {} |
+ | REQ {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
+ ;
+ entry:
| xentity { $1, false }
| xentity start { $1, true }
;