Skip to content
Snippets Groups Projects
Verified Commit 432b83da authored by Ogilvie, D.H. (Duncan)'s avatar Ogilvie, D.H. (Duncan)
Browse files

add types in LogicIR

parent 36b02fba
No related branches found
No related tags found
No related merge requests found
...@@ -2,6 +2,18 @@ module LogicIR.Expr where ...@@ -2,6 +2,18 @@ module LogicIR.Expr where
-- Based on my (Duncan's) previous work: https://github.com/mrexodia/wp/blob/master/Wp.hs -- Based on my (Duncan's) previous work: https://github.com/mrexodia/wp/blob/master/Wp.hs
data Primitive = PBool
| PInt
deriving (Show, Eq, Read)
data Type = TPrim Primitive
| TArray Type
deriving (Show, Eq, Read)
-- Typed + named variable
data Var = Var Type String
deriving (Show, Eq, Read)
-- Numeral unary operators -- Numeral unary operators
data NUnop = NNeg data NUnop = NNeg
| NNot | NNot
...@@ -22,10 +34,10 @@ data NBinop = NAdd ...@@ -22,10 +34,10 @@ data NBinop = NAdd
-- Numeral expressions -- Numeral expressions
data NExpr = NConst Int -- Integer constant data NExpr = NConst Int -- Integer constant
| NVar String -- Named integer variable | NVar Var -- Variable
| NUnop NUnop NExpr -- Unary operator | NUnop NUnop NExpr -- Unary operator
| NBinop NExpr NBinop NExpr -- Binary operators | NBinop NExpr NBinop NExpr -- Binary operators
| NArray String NExpr -- Integer array access | NArray Var NExpr -- Integer array access
deriving (Show, Eq, Read) deriving (Show, Eq, Read)
-- Reference: https://en.wikipedia.org/wiki/First-order_logic#Logical_symbols -- Reference: https://en.wikipedia.org/wiki/First-order_logic#Logical_symbols
...@@ -51,10 +63,10 @@ data COp = CEqual ...@@ -51,10 +63,10 @@ data COp = CEqual
-- Logical expressions -- Logical expressions
data LExpr = LConst Bool -- True/False data LExpr = LConst Bool -- True/False
| LVar String -- Named boolean variable | LVar Var -- Variable
| LNot LExpr -- Logical negation/not | LNot LExpr -- Logical negation/not
| LBinop LExpr LBinop LExpr -- Logical operator | LBinop LExpr LBinop LExpr -- Logical operator
| LComp NExpr COp NExpr -- Integer comparison | LComp NExpr COp NExpr -- Integer comparison
| LQuant QOp [String] LExpr -- Logical quantifier | LQuant QOp [Var] LExpr -- Logical quantifier
| LArray String NExpr -- Logical array access (TODO: remove?) | LArray Var NExpr -- Logical array access (TODO: remove?)
deriving (Show, Eq, Read) deriving (Show, Eq, Read)
\ No newline at end of file
...@@ -4,10 +4,10 @@ import LogicIR.Expr ...@@ -4,10 +4,10 @@ import LogicIR.Expr
-- Fold algrbra for numeral expressions -- Fold algrbra for numeral expressions
type NExprAlgebra r = (Int -> r, -- NConst type NExprAlgebra r = (Int -> r, -- NConst
String -> r, -- NVar Var -> r, -- NVar
NUnop -> r -> r, -- NUnop NUnop -> r -> r, -- NUnop
r -> NBinop -> r -> r, -- NBinop r -> NBinop -> r -> r, -- NBinop
String -> r -> r -- NArray Var -> r -> r -- NArray
) )
-- Fold for numeral expressions -- Fold for numeral expressions
...@@ -22,12 +22,12 @@ foldNExpr (fConst, fVar, fUnop, fBinop, fArray) = fold where ...@@ -22,12 +22,12 @@ foldNExpr (fConst, fVar, fUnop, fBinop, fArray) = fold where
-- Fold algebra for logical expressions -- Fold algebra for logical expressions
type LExprAlgebra r = (Bool -> r, -- LConst type LExprAlgebra r = (Bool -> r, -- LConst
String -> r, -- LVar Var -> r, -- LVar
r -> r, -- LNot r -> r, -- LNot
r -> LBinop -> r -> r, -- LBinop r -> LBinop -> r -> r, -- LBinop
NExpr -> COp -> NExpr -> r, -- LComp NExpr -> COp -> NExpr -> r, -- LComp
QOp -> [String] -> r -> r, -- LQuant QOp -> [Var] -> r -> r, -- LQuant
String -> NExpr -> r -- LArray Var -> NExpr -> r -- LArray
) )
-- Fold for logical expressions -- Fold for logical expressions
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment