module alloy/Expressions
imports
  alloy/Lexical
  alloy/Names
  alloy/expressions/Block
  alloy/Declarations
exports
  sorts Expr LetDecl RHSExpr ArrowOp BlockOrBar CompareOp Quant LiFoo

  context-free syntax
    "none"                                    -> Expr {cons("ANoneExpr")}
    "iden"                                    -> Expr {cons("AIdenExpr")}
    "univ"                                    -> Expr {cons("AUnivExpr")}
    "Int"                                     -> Expr {cons("AIntExpr")}
    "seq/Int"                                 -> Expr {cons("ASeqIntExpr")}
    "(" Expr|RHSExpr ")"                      -> Expr {bracket}
    Name                                      -> Expr {cons("ARefExpr")}
    "@" Name                                  -> Expr {cons("AAtRefExpr")}
    "let" {LetDecl ","}+ Block                -> Expr {cons("ALetExpr")}
    "let" {LetDecl ","}+ "|" (RHSExpr|Expr)   -> RHSExpr {cons("ALetBarExpr")}
    Quant {Decl ","}+ Block                   -> Expr {cons("AQuantExpr")}
    Quant {Decl ","}+ "|" (RHSExpr|Expr)      -> RHSExpr {cons("AQuantBarExpr")}
    Expr ("!"|"not")? CompareOp Expr    -> Expr    {cons("ACompareOpExpr"),left}
    Expr "=>" (Expr|RHSExpr) "else" (Expr|RHSExpr) -> Expr  {cons("AImpliesElseExpr"),right}
    Expr "implies" (Expr|RHSExpr) "else" (Expr|RHSExpr) -> Expr  {cons("AImpliesElseExpr"),right}
    Expr "[" {(Expr|RHSExpr) ","}* "]"        -> Expr {cons("ABoxJoinExpr")}
    "int"                                     -> Expr {cons("AintExpr")}
    Number                                    -> Expr
    "-" Number                                -> Expr
    "none"                                    -> Expr {cons("ANoneExpr")}
    "univ"                                    -> Expr {cons("AUnivExpr")}
    "Int"                                     -> Expr {cons("AIntExpr")}
    "seq/Int"                                 -> Expr {cons("ASeqIntExpr")}
    Block                                     -> Expr
    "{" {Decl ","}+ BlockOrBar "}"            -> Expr {cons("ASetCompExpr")}
    Expr ArrowOp Expr                     -> Expr {cons("AArrowOpExpr"), right}
    Expr ArrowOp RHSExpr                       -> Expr {cons("AArrowOpExpr"),
                                                                          right}

    "|" Expr            -> BlockOrBar  {cons("ABlockOrBar")}
    "|" RHSExpr         -> BlockOrBar  {cons("ABlockOrBar")}
    Block               -> BlockOrBar  {cons("ABlockOrBar")}

    Name "=" Expr -> LetDecl {cons("ALetDecl")}

    "all"  -> Quant {cons("AAllQuant")}
    "no"   -> Quant {cons("ANoQuant")}
    "some" -> Quant {cons("ASomeQuant")}
    "lone" -> Quant {cons("ALoneQuant")}
    "one"  -> Quant {cons("AOneQuant")}
    "sum"  -> Quant {cons("ASumQuant")}

    "not" Expr  -> Expr {cons("ANotOpExpr")}
    "!" Expr    -> Expr {cons("ANotOpExpr")}
    "no" Expr   -> Expr {cons("ANoOpExpr")}
    "some" Expr -> Expr {cons("ASomeExpr")}
    "lone" Expr -> Expr {cons("ALoneExpr")}
    "one" Expr  -> Expr {cons("AOneExpr")}
    "set" Expr  -> Expr {cons("ASetExpr")}
    "seq" Expr  -> Expr {cons("ASeq")}
    "#" Expr    -> Expr {cons("ASizeOfExpr")}
    "~" Expr    -> Expr {cons("ATranspose")}
    "*" Expr    -> Expr {cons("AReflexiveTransitiveClosure")}
    "^" Expr    -> Expr {cons("ATransitiveClosure")}

    "not" RHSExpr     -> Expr {cons("ANotOpExpr")}
    "!" RHSExpr       -> Expr {cons("ANotOpExpr")}
    "no" RHSExpr      -> Expr {cons("ANoOpExpr")}
    "some" RHSExpr    -> Expr {cons("ASomeExpr")}
    "lone" RHSExpr    -> Expr {cons("ALoneExpr")}
    "one" RHSExpr     -> Expr {cons("AOneExpr")}
    "set" RHSExpr     -> Expr {cons("ASetExpr")}
    "seq" RHSExpr     -> Expr {cons("ASeq")}
    "#" RHSExpr       -> Expr {cons("ASizeOfExpr")}
    "~" RHSExpr       -> Expr {cons("ATranspose")}
    "*" RHSExpr       -> Expr {cons("AReflexiveTransitiveClosure")}
    "^" RHSExpr       -> Expr {cons("ATransitiveClosure")}


    Expr "||" Expr      -> Expr {cons("AOrExpr"),left}
    Expr "or" Expr     -> Expr {cons("AOrExpr"),left}

    {Expr "%"}+ -> Expr {cons("CrossProduct")}

    Expr "||" Expr      -> Expr {cons("AOrExpr"), left}
    Expr "or" Expr     -> Expr {cons("AOrExpr"), left}
    Expr "&&" Expr      -> Expr {cons("AAndExpr"), left}
    Expr "and" Expr     -> Expr {cons("AAndExpr"), left}
    Expr "&" Expr     -> Expr {cons("AIntersectionExpr"), left}
    Expr "<=>" Expr     -> Expr {cons("ABiImplicationExpr"), left}
    Expr "iff" Expr    -> Expr {cons("AIffExpr"), left}
    Expr "=>" Expr      -> Expr {cons("AImpliesExpr"), right}
    Expr "implies" Expr -> Expr {cons("AImpliesExpr"), right}
    Expr "+" Expr      -> Expr {cons("APlusExpr"), left}
    Expr "-" Expr       -> Expr {cons("AMinusExpr"), left}
    Expr "++" Expr      -> Expr {cons("ARelationalOverrideExpr"), left}
    Expr "<:" Expr     -> Expr {cons("ADomainExpr"), left}
    Expr ":>" Expr      -> Expr {cons("ARangeExpr"), left}
    Expr "." Expr       -> Expr {cons("ADotJoinExpr"),left, left}
    Expr "<<" Expr      -> Expr {cons("ALShift"), left}
    Expr ">>" Expr      -> Expr {cons("ARShift"), left}

    Expr "||" RHSExpr      -> Expr {cons("AOrExpr"), left}
    Expr "or" RHSExpr     -> Expr {cons("AOrExpr"), left}
    Expr "&&" RHSExpr      -> Expr {cons("AAndExpr"), left}
    Expr "and" RHSExpr     -> Expr {cons("AAndExpr"), left}
    Expr "&" RHSExpr     -> Expr {cons("AIntersectionExpr"), left}
    Expr "<=>" RHSExpr     -> Expr {cons("ABiImplicationExpr"), left}
    Expr "iff" RHSExpr    -> Expr {cons("AIffExpr"), left}
    Expr "=>" RHSExpr      -> Expr {cons("AImpliesExpr"), right}
    Expr "implies" RHSExpr -> Expr {cons("AImpliesExpr"), right}
    Expr "+" RHSExpr      -> Expr {cons("APlusExpr"), left}
    Expr "-" RHSExpr       -> Expr {cons("AMinusExpr"), left}
    Expr "++" RHSExpr      -> Expr {cons("ARelationalOverrideExpr"), left}
    Expr "<:" RHSExpr     -> Expr {cons("ADomainExpr"), left}
    Expr ":>" RHSExpr      -> Expr {cons("ARangeExpr"), left}
    Expr "." RHSExpr       -> Expr {cons("ADotJoinExpr"), left}
    Expr "<<" RHSExpr      -> Expr {cons("ALShift"), left}
    Expr ">>" RHSExpr      -> Expr {cons("ARShift"), left}


    "="  -> CompareOp {cons("AEq")}
    "in" -> CompareOp {cons("AIn")}
    "<"  -> CompareOp {cons("ALT")}
    ">"  -> CompareOp {cons("AGT")}
    "=<" -> CompareOp {cons("ALE")}
    "<=" -> CompareOp {cons("ALE")}
    ">=" -> CompareOp {cons("AGE")}

    MulQual? "->" MulQual? -> ArrowOp {cons("AArrowOp")}

  context-free priorities
    {
    "~" Expr -> Expr {cons("ATransposeExpr")}
    "*" Expr -> Expr {cons("AReflexiveTransitiveClosureExpr")}
    "^" Expr -> Expr    {cons("ATransitiveClosureExpr")}
    }
  > {left:
        Expr "[" {(Expr|RHSExpr) ","}* "]"    -> Expr {cons("ABoxJoinExpr")}
        Expr "." Expr -> Expr {cons("ADotJoinExpr")}
    }
  > {left:
       Expr ":>" Expr      -> Expr {cons("ARangeExpr")}
    }
  > {left:
      Expr "<:" Expr     -> Expr {cons("ADomainExpr")}
    }
  > {right:
      Expr ArrowOp Expr -> Expr {cons("AArrowOpExpr")}
      Expr ArrowOp RHSExpr               -> Expr {cons("AArrowOpExpr")}
    }
  > {left:
      Expr "&" Expr     -> Expr {cons("AIntersectionExpr")}
    }
  > {left:
      Expr "++" Expr      -> Expr {cons("ARelationalOverrideExpr")}
    }
  > {left:
      "#" Expr   -> Expr {cons("ASizeOfExpr")}
    }
  >{left:
      Expr "+" Expr      -> Expr {cons("APlusExpr")}
      Expr "-" Expr      -> Expr {cons("AMinusExpr")}
      "-" Number         -> Expr {cons("ANegateNumber")}
   }
  >{left:
    Expr "<<" Expr      -> Expr {cons("ALShift")}
    Expr ">>" Expr      -> Expr {cons("ARShift")}
   }
  > { 
    "no" Expr   -> Expr {cons("ANoOpExpr")}
    "some" Expr -> Expr {cons("ASomeExpr")}
    "lone" Expr -> Expr {cons("ALoneExpr")}
    "one" Expr  -> Expr {cons("AOneExpr")}
    "set" Expr  -> Expr {cons("ASetExpr")}
    "seq" Expr  -> Expr {cons("ASeq")}
    }
  >{left:
    Expr ("!"|"not")? CompareOp Expr       -> Expr {cons("ACompareOpExpr")}
  }
  >{
        "not" Expr    -> Expr {cons("ANotOpExpr")}
        "!" Expr    -> Expr {cons("ANotOpExpr")}
  }
  >{left:
    Expr "&&" Expr      -> Expr {cons("AAndExpr"),avoid}
    Expr "and" Expr      -> Expr {cons("AAndExpr"),avoid}
  }
  > { left: Expr -> {Expr "%"}+
            {Expr "%"}+ -> Expr
  }
  >{right:
    Expr "=>" Expr      -> Expr {cons("AImpliesExpr"), avoid}
    Expr "=>" (Expr|RHSExpr) "else" (Expr|RHSExpr)-> Expr  {cons("AImpliesElseExpr")}
    Expr "implies" (Expr|RHSExpr) "else" (Expr|RHSExpr)-> Expr  {cons("AImpliesElseExpr")}
  }
  >{non-assoc:
    Expr "<=>" Expr     -> Expr {cons("ABiImplicationExpr")}
    Expr "iff" Expr    -> Expr {cons("ABiImplicationExpr"),left}
  }
  >{left:
    Expr "||" Expr      -> Expr {cons("AOrExpr")}
    Expr "or" Expr      -> Expr {cons("AOrExpr")}
  }
  >{ right:
    Expr "||" RHSExpr      -> Expr {cons("AOrExpr")}
    Expr "or" RHSExpr     -> Expr {cons("AOrExpr")}
    Expr "&&" RHSExpr      -> Expr {cons("AAndExpr")}
    Expr "and" RHSExpr     -> Expr {cons("AAndExpr")}
    Expr "&" RHSExpr     -> Expr {cons("AIntersectionExpr")}
    Expr "<=>" RHSExpr     -> Expr {cons("ABiImplicationExpr")}
    Expr "iff" RHSExpr    -> Expr {cons("AIffExpr")}
    Expr "=>" RHSExpr      -> Expr {cons("AImpliesExpr")}
    Expr "implies" RHSExpr -> Expr {cons("AImpliesExpr")}
    Expr "+" RHSExpr      -> Expr {cons("APlusExpr")}
    Expr "-" RHSExpr       -> Expr {cons("AMinusExpr")}
  }