*/
%{
- module G = Options
- module N = Level
- module T = Txt
-
+ module G = Options
+ module N = Layer
+ module T = Txt
+
+IFDEF PARSER THEN
let _ = Parsing.set_trace !G.debug_parser
+END
%}
%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 OP CP OB CB OA CA OC CC FS CN CM EQ STAR HASH TE CT
%token GRAPH MAIN DECL AX CONG DEF TH GEN REQ OPEN CLOSE SORTS EOF
%start entry
%type <Txt.command option> entry
-
- %nonassoc CP CB CA
- %right WTO STO
%%
hash:
| {}
| sort { [$1] }
| sort CM sorts { $1 :: $3 }
;
- level:
- | { N.infinite }
- | CT IX { N.finite $2}
+ layer:
+ | { N.infinity }
+ | CT IX { N.finite $2 }
+ ;
+
+ binder:
+ | OB ID CN term CB layer { T.Abst ($6, $2, true, $4) }
+ | OB term CB layer { T.Abst ($4, "", false, $2) }
+ | OB ID TE term CB layer { T.Abst ($6, $2, false, $4) }
+ | OB ID EQ term CB { T.Abbr ($2, $4) }
+ ;
+ binders:
+ | binder fs binder { [$1; $3] }
+ | binder fs binders { $1 :: $3 }
+ ;
+ lenv:
+ | binder { [$1] }
+ | OC binders CC { $2 }
;
- abst:
- | ID CN term { $1, true, $3 }
- | TE term { "", false, $2 }
- | ID TE term { $1, false, $3 }
- ;
- abbr:
- | ID EQ term { $1, $3 }
- ;
- absts:
- | abst { [$1] }
- | abst CM absts { $1 :: $3 }
- ;
- abbrs:
- | abbr { [$1] }
- | abbr CM abbrs { $1 :: $3 }
- ;
- binder:
- | absts { T.Abst $1 }
- | abbrs { T.Abbr $1 }
- | 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) }
- | 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) }
+ | STAR IX { T.Sort $2 }
+ | STAR ID { T.NSrt $2 }
+ | hash IX { T.LRef $2 }
+ | ID { T.NRef $1 }
+ | HASH ID { T.NRef $2 }
+ | atom OP terms CP { T.Inst ($1, $3) }
;
term:
- | 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 level fs term { T.Bind ($4, $2, $6) }
- | term WTO level term { T.Impl ($3, false, "", $1, $4) }
- | ID TE term WTO level term { T.Impl ($5, false, $1, $3, $6) }
- | term STO level term { T.Impl ($3, true, "", $1, $4) }
- | ID TE term STO level term { T.Impl ($5, true, $1, $3, $6) }
- | OP term CP { $2 }
+ | atom { $1 }
+ | OA term CA fs term { T.Cast ($2, $5) }
+ | OP term CP fs term { T.Appl ($2, $5) }
+ | lenv fs term { T.Proj ($1, $3) }
+ | OP term CP { $2 }
;
terms:
- | term CM term { [$1; $3] }
+ | term { [$1] }
| term CM terms { $1 :: $3 }
;
-
+
decl:
| DECL { T.Decl }
| AX { T.Ax }
| DEF { T.Def }
| TH { T.Th }
;
- xentity:
+ command:
| GRAPH ID
- { 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.Graph $2 }
+ | main decl comment ID CN term
+ { T.Constant ($1, $2, $4, $3, $6) }
+ | main def comment ID EQ term
+ { T.Constant ($1, $2, $4, $3, $6) }
+ | main def comment ID EQ term CN term
+ { T.Constant ($1, $2, $4, $3, T.Cast ($8, $6)) }
| 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 {} |
| REQ {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
;
entry:
- | xentity start { Some $1 }
+ | command start { Some $1 }
| EOF { None }
;