/******************************************************************************
Simple parser for PSL/Sugar properties
(based on examples/lexyacc in mosml distribution)
******************************************************************************/

%{
open Data;

(* Function definitions lifted from <holdir>/src/0/Lib.sml *)

fun mem i =
 let fun itr [] = false
       | itr (a::rst) = i=a orelse itr rst
 in itr end;

fun insert i L = if mem i L then L else i::L

fun union [] S = S
  | union S [] = S
  | union (a::rst) S2 = union rst (insert a S2)

%}

%token <int> Number
%token <string> Name
%token AT SEMICOLON LBRKTSTAR LBRKTSTARRBRKT LBRKTPLUSRBRKT LBRKTEQ LBRKTLEFTARROW
%token COMMA COLON BAR BARBAR AMPERSAND AMPERSANDAMPERSAND LEFTARROW LEFTRIGHTARROW
%token BARLEFTARROW BAREQLEFTARROW BAREQUAL EXCLAIM STAR
%token LPAR RPAR LBRKT RBRKT LBRACE RBRACE
%token BEFORE BEFOREX BEFOREXU BEFOREU
%token WHILENOTXU EVENTUALLYX
%token NEXTX NEXTA NEXTAX NEXTE NEXTEX NEXTEVENT NEXTEVENTX NEXTEVENTAX NEXTEVENTEX
%token UNTILX UNTILXU UNTILU
%token WHILENOTX WHILENOTXU WHILENOTU WITHINX WITHINXU WITHINU XX
%token A AF AG AX ABORT ALWAYS
%token BEFORE E EF EG EX FORALL G INF NEVER NEXT U X ABORT UNTIL W WHILENOT WITHIN
%token EOF

%left AT			/* lowest precedence */
%left ABORT
%left BAR BARBAR
%left AMPERSAND AMPERSANDAMPERSAND
%left COLON SEMICOLON
%nonassoc STAR LEFTARROW BARLEFTARROW UNTIL EXCLAIM BAREQUAL
			      	/* highest precedence  */

%start MainBoolean
%start MainSERE
%start MainFL
%start MainOBE
%start MainState
%start MainPath
%start MainPathSERE
%start MainPathFL

%type <Data.bexp>                          Boolean    MainBoolean
%type <Data.sere>                          SERE       MainSERE
%type <Data.sere>                          Sequence   Sequence_or_Boolean
%type <Data.sere * Data.sere -> Data.sere> AndOrOp
%type <int * (int option)>                 Count      Range
%type <int>                                LowBound
%type <int option>                         HighBound
%type <Data.fl>                            FL         MainFL
%type <Data.obe>                           OBE        MainOBE
%type <string list>                        State      MainState
%type <(string list)list>                  Path       MainPath
%type <(string list)list * Data.sere>      PathSERE   MainPathSERE
%type <(string list)list * Data.fl>        PathFL     MainPathFL

%%

MainBoolean:
    Boolean EOF                         { $1 }
;

MainSERE:
    SERE EOF                            { $1 }
;

MainFL:
    FL EOF                              { $1 }
;

MainOBE:
    OBE EOF                             { $1 }
;

Boolean:
    Name                                { B_PROP $1 }
  | EXCLAIM Boolean                     { B_NOT $2 }
  | LPAR Boolean RPAR                   { $2 }
  | Boolean AMPERSANDAMPERSAND Boolean  { B_AND($1, $3) }
  | Boolean BARBAR Boolean              { B_OR($1, $3) }
  | Boolean LEFTARROW Boolean           { B_IMP($1, $3) }
  | Boolean LEFTRIGHTARROW Boolean      { B_IFF($1, $3) }
;

SERE:
    Boolean                             { S_BOOL $1 }
  | Sequence                            { $1 }
  | SERE AT Boolean                     { S_CLOCK($1,$3) }
  | SERE SEMICOLON SERE                 { S_CAT($1, $3) }
  | Sequence COLON Sequence             { S_FUSION($1, $3) }
  | Sequence AndOrOp Sequence           { $2($1,$3) }
  | SERE LBRKTSTARRBRKT                 { S_REPEAT $1 }
  | SERE LBRKTSTAR Count RBRKT          { S_RANGE_REPEAT($1,$3) }
  | LBRKTSTARRBRKT                      { S_REPEAT(S_BOOL B_TRUE) }
  | LBRKTSTAR Count RBRKT               { S_RANGE_REPEAT(S_BOOL B_TRUE,$2) }
  | SERE LBRKTPLUSRBRKT                 { S_NON_ZERO_REPEAT $1}
  | LBRKTPLUSRBRKT                      { S_NON_ZERO_REPEAT(S_BOOL B_TRUE)}
  | Boolean LBRKTEQ Count RBRKT         { S_RANGE_EQ_REPEAT($1,$3) }
  | Boolean LBRKTLEFTARROW RBRKT        { S_RANGE_GOTO_REPEAT($1, (1,NONE)) }
  | Boolean LBRKTLEFTARROW Count RBRKT  { S_RANGE_GOTO_REPEAT($1,$3) }
;

Sequence:
    LBRACE SERE RBRACE                  { $2 }
;

AndOrOp:
    AMPERSAND                           { S_FLEX_AND }
  | AMPERSANDAMPERSAND                  { S_AND }
  | BAR                                 { S_OR }
;

Count:
    Number                              { ($1,NONE) }
  | Range                               { $1 }
;

Range:
    LowBound COLON HighBound            { ($1,$3) }
;

LowBound:
 Number                                 { $1 }
;

HighBound:
    Number                              { SOME $1 }
  | INF                                 { NONE }
;

Sequence_or_Boolean:
    Sequence                            { $1 }
  | Boolean                             { S_BOOL $1 }

FL:
    Name                                { F_BOOL(B_PROP $1) }
  | LPAR FL RPAR                        { $2 }
  | FL AT Boolean  EXCLAIM              { F_STRONG_CLOCK($1,$3) }
  | FL AT Boolean                       { F_WEAK_CLOCK($1,$3) }
  | FL ABORT Boolean                    { F_ABORT($1,$3) }
  | EXCLAIM FL                          { F_NOT $2 }
  | FL AMPERSANDAMPERSAND FL            { F_AND($1, $3) }
  | FL BARBAR FL                        { F_OR($1, $3) }
  | FL LEFTARROW FL                     { F_IMP($1, $3) }
  | FL LEFTRIGHTARROW FL                { F_IFF($1, $3) }
  | X FL                                { F_WEAK_X $2 }
  | XX FL                               { F_STRONG_X $2 }
  | F FL                                { F_F $2 }
  | G FL                                { F_G $2 }
  | LBRKT FL U FL RBRKT                 { F_U($2,$4) }
  | LBRKT FL W FL RBRKT                 { F_W($2,$4) }
  | ALWAYS FL                           { F_ALWAYS $2 }
  | NEVER FL                            { F_NEVER $2 }
  | NEXT FL                             { F_WEAK_NEXT $2 }
  | NEXTX FL                            { F_STRONG_NEXT $2 }
  | EVENTUALLYX FL                      { F_STRONG_EVENTUALLY $2 }
  | FL UNTILX FL                        { F_STRONG_UNTIL($1,$3) }
  | FL UNTIL FL                         { F_WEAK_UNTIL($1,$3) }
  | FL UNTILXU FL                       { F_STRONG_UNTIL_INC($1,$3) }
  | FL UNTILU FL                        { F_WEAK_UNTIL_INC($1,$3) }
  | FL BEFOREX FL                       { F_STRONG_BEFORE($1,$3) }
  | FL BEFORE FL                        { F_WEAK_BEFORE($1,$3) }
  | FL BEFOREXU FL                      { F_STRONG_BEFORE_INC($1,$3) }
  | FL BEFOREU FL                       { F_WEAK_BEFORE_INC($1,$3) }
  | X LBRKT Number RBRKT LPAR FL RPAR   { F_NUM_WEAK_X($3,$6) }
  | XX LBRKT Number RBRKT LPAR FL RPAR  { F_NUM_STRONG_X($3,$6) }
  | NEXT LBRKT Number RBRKT LPAR FL RPAR{ F_NUM_WEAK_NEXT($3,$6) }
  | NEXTX LBRKT Number RBRKT LPAR FL RPAR
                                        { F_NUM_STRONG_NEXT($3,$6) }
  | NEXTA LBRKT Range RBRKT LPAR FL RPAR
                                        { F_NUM_WEAK_NEXT_A($3,$6) }
  | NEXTAX LBRKT Range RBRKT LPAR FL RPAR
                                        { F_NUM_STRONG_NEXT_A($3,$6) }
  | NEXTE LBRKT Range RBRKT LPAR FL RPAR
                                        { F_NUM_WEAK_NEXT_E($3,$6) }
  | NEXTEX LBRKT Range RBRKT LPAR FL RPAR
                                        { F_NUM_STRONG_NEXT_E($3,$6) }
  | NEXTEVENTX LPAR Boolean RPAR LPAR FL RPAR
                                        { F_STRONG_NEXT_EVENT($3,$6) }
  | NEXTEVENT LPAR Boolean RPAR LPAR FL RPAR
                                        { F_WEAK_NEXT_EVENT($3,$6) }
  | NEXTEVENTX LPAR Boolean RPAR LBRKT Number RBRKT LPAR FL RPAR
                                        { F_NUM_STRONG_NEXT_EVENT($3,$6,$9) }
  | NEXTEVENT LPAR Boolean RPAR LBRKT Number RBRKT LPAR FL RPAR
                                        { F_NUM_WEAK_NEXT_EVENT($3,$6,$9) }

  | NEXTEVENTAX LPAR Boolean RPAR LBRKT Range RBRKT LPAR FL RPAR
                                        { F_NUM_STRONG_NEXT_EVENT_A($3,$6,$9) }
  | NEXTEVENTA LPAR Boolean RPAR LBRKT Range RBRKT LPAR FL RPAR
                                        { F_NUM_WEAK_NEXT_EVENT_A($3,$6,$9) }

  | Sequence LPAR FL RPAR               { F_SUFFIX_IMP($1,$3) }
  | Sequence BARLEFTARROW Sequence EXCLAIM
                                        { F_STRONG_IMP($1,$3) }
  | Sequence BARLEFTARROW Sequence      { F_WEAK_IMP($1,$3) }
  | Sequence BAREQLEFTARROW Sequence EXCLAIM
                                        { F_SKIP_STRONG_IMP($1,$3) }
  | Sequence BAREQLEFTARROW Sequence    { F_SKIP_WEAK_IMP($1,$3) }
  | ALWAYS Sequence                     { F_SERE_ALWAYS $2 }
  | NEVER Sequence                      { F_SERE_NEVER $2 }
  | EVENTUALLYX Sequence                { F_SERE_STRONG_EVENTUALLY $2 }
  | WITHINX LPAR Sequence_or_Boolean COMMA Boolean RPAR Sequence
                                        {F_STRONG_WITHIN($3,$5,$7) }
  | WITHIN LPAR Sequence_or_Boolean COMMA Boolean RPAR Sequence
                                        {F_WEAK_WITHIN($3,$5,$7) }
  | WITHINXU LPAR Sequence_or_Boolean COMMA Boolean RPAR Sequence
                                        {F_STRONG_WITHIN_INC($3,$5,$7) }
  | WITHINU LPAR Sequence_or_Boolean COMMA Boolean RPAR Sequence
                                        {F_WEAK_WITHIN_INC($3,$5,$7) }
  | WHILENOTX LPAR Boolean RPAR Sequence
                                        {F_STRONG_WHILENOT($3,$5) }
  | WHILENOT LPAR Boolean RPAR Sequence
                                        {F_WEAK_WHILENOT($3,$5) }
  | WHILENOTXU LPAR Boolean RPAR Sequence
                                        {F_STRONG_WHILENOT_INC($3,$5) }
  | WHILENOTU LPAR Boolean RPAR Sequence
                                        {F_WEAK_WHILENOT_INC($3,$5) }

;

OBE:
    Boolean                             { O_BOOL $1 }
  | LPAR OBE RPAR                       { $2 }
  | EXCLAIM OBE                         { O_NOT $2 }
  | OBE AMPERSAND OBE                   { O_AND($1, $3) }
  | EX OBE                              { O_EX $2 }
  | E LBRKT OBE UNTIL OBE RBRKT         { O_EU($3,$5) }
  | EG OBE                              { O_EG $2 }
;

MainState:
    State EOF                           { $1 }
;

State:
    /* empty */                         { [] }
  | Name                                { [$1] }
  | Name COMMA State                    { insert $1 $3 }
;

MainPath:
    Path EOF                            { $1 }
;

Path:
    /* empty */                         { [] }
  | LBRACE State RBRACE                 { [$2] }
  | LBRACE State RBRACE Path            { $2 :: $4 }
;

MainPathSERE:
    PathSERE EOF                        { $1 }
;

PathSERE:
    Path BAREQUAL SERE                  { ($1,$3) }
;

MainPathFL:
    PathFL EOF                          { $1 }
;

PathFL:
    Path BAREQUAL FL                    { ($1,$3) }
;