module z/ZTerm
imports
  z/Names
hiddens
  sorts DecorExpr
exports
  sorts ZTerm Pred ZExpr
  context-free syntax
    ZTerm                       -> Pred
    ZTerm                       -> ZExpr

    ZTerm "∧" ZTerm             -> ZTerm {cons("ZAndTerm"), left}
    "¬" ZTerm                   -> ZTerm {cons("ZNotTerm")}
    "true"                      -> ZTerm {cons("ZTruePred")}
    "(" Pred ")"                -> ZTerm {bracket}

    ZTerm "∈" ZTerm -> ZTerm {cons("ZInPred")}

    ZTerm "⨟" ZTerm           -> ZTerm {cons("ZCompExpr")}
    ZTerm "⨠" ZTerm          -> ZTerm {cons("ZPipeExpr")}
    "pre" ZTerm               -> ZTerm {cons("ZPreExpr")}
    {ZTerm "×"}+              -> ZTerm {cons("ZProdExpr")}
    "ℙ" ZTerm                 -> ZTerm {cons("ZPowerExpr")}
    ZTerm ZTerm               -> ZTerm {cons("ZApplExpr")}
    DecorExpr                 -> ZTerm
    ZTerm STROKE              -> DecorExpr {cons("ZDecorExpr")}
    "θ" ZTerm STROKE          -> DecorExpr {reject}
    ZTerm "[" {(ZName "/" ZName) ","}+ "]" -> ZTerm {cons("ZSchemaRenaming")}
    ZTerm "." ZName           -> ZTerm {cons("ZSelExpr")}
    "θ" ZTerm                 -> ZTerm {cons("ZThetaExpr")}
    "θ" ZTerm STROKE          -> ZTerm {cons("ZThetaExpr")}
    ZName                     -> ZTerm {cons("ZRefExpr")}
    ZName "[" {ZTerm ","}+ "]" -> ZTerm {cons("ZGenInstExpr")}
    "{" {ZTerm ","}* "}"      -> ZTerm {cons("ZSetExt")}

    "(" ZTerm "," {ZTerm ","}+ ")" -> ZTerm {cons("ZTupleExpr")}
    "⦉" "⦊"                   -> ZTerm {cons("BindExpr")}

  context-free priorities
    {
      "θ" ZTerm                 -> ZTerm
      "θ" ZTerm STROKE          -> ZTerm
    } >
    {
      ZTerm "." ZName -> ZTerm
    } >
    ZTerm "[" {(ZName "/" ZName) ","}+ "]" -> ZTerm >
    DecorExpr -> ZTerm >
    ZTerm ZTerm -> ZTerm >
    {
      left: {ZTerm "×"}+ -> ZTerm
            ZTerm -> {ZTerm "×"}+
    } >
    "pre" ZTerm -> ZTerm >
    ZTerm "⨠" ZTerm -> ZTerm >
    ZTerm "⨟" ZTerm -> ZTerm >
    { left: ZTerm "∈" ZTerm -> ZTerm
    } >
    "¬" ZTerm -> ZTerm >
    ZTerm "∧" ZTerm -> ZTerm
