module z/concrete/ZTerm
imports
  z/ZTerm
  z/concrete/SchemaText
hiddens
  sorts ZCharSetComp ZSchemaConstruction
exports
  sorts Pred ZExpr SchemaText ZDecl
  context-free syntax
    Pred ";" Pred               -> Pred {cons("ZAndSemiPred"), left}
    "false"                     -> ZTerm {cons("ZFalsePred")}
 
    "∀" SchemaText "⦁" ZTerm    -> ZTerm {cons("ZAllTerm")}
    "∃" SchemaText "⦁" ZTerm    -> ZTerm {cons("ZExiTerm")}
    "∃↘1↖" SchemaText "⦁" ZTerm -> ZTerm {cons("ZExiOneTerm")}

    ZTerm "∨" ZTerm             -> ZTerm {cons("ZOrTerm"),  left}
    ZTerm "⇒" ZTerm             -> ZTerm {cons("ZImpTerm"), left}
    ZTerm "⇔" ZTerm             -> ZTerm {cons("ZIffTerm"), left}
    ZTerm "=" ZTerm             -> ZTerm {cons("ZEqPred")}

    "λ" SchemaText "⦁" ZTerm  -> ZTerm {cons("ZLambdaExpr")}
    "μ" SchemaText "⦁" ZTerm  -> ZTerm {cons("ZMuExpr")}
    "(" "μ" SchemaText ")"     -> ZTerm {cons("ZCharMuExpr")}

    "{" SchemaText "⦁" ZTerm "}" -> ZTerm {cons("ZSetComp")}

    ZCharSetComp              -> ZTerm
    "{" SchemaText "}"        -> ZCharSetComp {cons("ZCharSetComp")}
    "{" "}"                   -> ZCharSetComp {reject}
    "{" ZTerm "}"             -> ZCharSetComp {reject}

    ZSchemaConstruction       -> ZTerm
    "[" SchemaText "]"        -> ZSchemaConstruction {cons("ZSchConst")}
    "[" ZTerm "]"             -> ZSchemaConstruction {reject}
  context-free priorities
    ZTerm "⨟" ZTerm -> ZTerm >
    "μ" SchemaText "⦁" ZTerm -> ZTerm >
    "λ" SchemaText "⦁" ZTerm -> ZTerm >
    { left: ZTerm "∈" ZTerm -> ZTerm
            ZTerm "=" ZTerm -> ZTerm
    } >
    "¬" ZTerm -> ZTerm >
    ZTerm "∈" ZTerm -> ZTerm >
    ZTerm "∧" ZTerm -> ZTerm >
    ZTerm "∨" ZTerm -> ZTerm >
    ZTerm "⇒" ZTerm -> ZTerm >
    ZTerm "⇔" ZTerm -> ZTerm >
    { left: "∀" SchemaText "⦁" ZTerm -> ZTerm
            "∃" SchemaText "⦁" ZTerm -> ZTerm
	    "∃↘1↖" SchemaText "⦁" ZTerm -> ZTerm
    } >
    Pred ";" Pred -> Pred
