Expr.hs

module LogicIR.Expr where

-- Based on my (Duncan's) previous work: https://github.com/mrexodia/wp/blob/master/Wp.hs

-- Numeral unary operators
data NUnop = NNeg
           | NNot
           deriving (Show, Eq, Read)

-- Numeral binary operators
data NBinop = NAdd
            | NSub
            | NMul
            | NDiv
            | NRem
            | NShl
            | NShr
            | NAnd
            | NOr
            | NXor
            deriving (Show, Eq, Read)

-- Numeral expressions
data NExpr = NConst Int -- Integer constant
           | NVar String -- Named integer variable
           | NUnop NUnop NExpr -- Unary operator
           | NBinop NExpr NBinop NExpr -- Binary operators
           | NArray String NExpr -- Integer array access
           deriving (Show, Eq, Read)

-- Reference: https://en.wikipedia.org/wiki/First-order_logic#Logical_symbols

-- Logical operators
data LBinop = LAnd -- Conjunction
            | LOr -- Disjunction
            | LImpl -- Implication
            | LBicond -- Biconditional (TODO: remove?)
            deriving (Show, Eq, Read)

-- Quantifier operators
data QOp = QAll | QAny
         deriving (Show, Eq, Read)

-- Comparison operators
data COp = CEqual
         | CLess
         | CGreater
         | CLeq
         | CGeq
         deriving (Show, Eq, Read)

-- Logical expressions
data LExpr = LConst Bool -- True/False
           | LVar String -- Named boolean variable
           | LNot LExpr -- Logical negation/not
           | LBinop LExpr LBinop LExpr -- Logical operator
           | LComp NExpr COp NExpr -- Integer comparison
           | LQuant QOp [String] LExpr -- Logical quantifier
           | LArray String NExpr -- Logical array access (TODO: remove?)
           deriving (Show, Eq, Read)