implemented LogicIR.Expr and LogicIR.Fold

src/LogicIR/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)
\ No newline at end of file

src/LogicIR/Fold.hs

+module LogicIR.Fold where
+
+import LogicIR.Expr
+
+-- Fold algrbra for numeral expressions
+type NExprAlgebra r = (Int -> r, -- NConst
+                       String -> r, -- NVar
+                       NUnop -> r -> r, -- NUnop
+                       r -> NBinop -> r -> r, -- NBinop
+                       String -> r -> r -- NArray
+                      )
+
+-- Fold for numeral expressions
+foldNExpr :: NExprAlgebra r -> NExpr -> r
+foldNExpr (const, var, unop, binop, array) = fold where
+    fold e = case e of
+                  NConst n -> const n
+                  NVar n -> var n
+                  NUnop o e -> unop o (fold e)
+                  NBinop a o b -> binop (fold a) o (fold b)
+                  NArray n e -> array n (fold e)
+
+-- Fold algebra for logical expressions
+type LExprAlgebra r = (Bool -> r, -- LConst
+                       String -> r, -- LVar
+                       r -> r, -- LNot
+                       r -> LBinop -> r -> r, -- LBinop
+                       NExpr -> COp -> NExpr -> r, -- LComp
+                       QOp -> [String] -> r -> r, -- LQuant
+                       String -> NExpr -> r -- LArray
+                      )
+
+-- Fold for logical expressions
+foldLExpr :: LExprAlgebra r -> LExpr -> r
+foldLExpr (const, var, not, binop, comp, quant, array) = fold where
+    fold e = case e of
+                  LConst c -> const c
+                  LVar n -> var n
+                  LNot e -> not (fold e)
+                  LBinop a o b -> binop (fold a) o (fold b)
+                  LComp a o b -> comp a o b
+                  LQuant o vs e -> quant o vs (fold e)
+                  LArray n e -> array n e
\ No newline at end of file