Commit e07881b0 authored by Philipp Meyer's avatar Philipp Meyer

Added true and false as atoms for formulas

parent bf11f9ae
...@@ -19,7 +19,7 @@ languageDef = ...@@ -19,7 +19,7 @@ languageDef =
Token.commentLine = "//", Token.commentLine = "//",
Token.identStart = letter <|> char '_', Token.identStart = letter <|> char '_',
Token.identLetter = alphaNum <|> char '_', Token.identLetter = alphaNum <|> char '_',
Token.reservedNames = [], Token.reservedNames = ["true", "false"],
Token.reservedOpNames = ["->", "<", "<=", "=", ">=", ">", Token.reservedOpNames = ["->", "<", "<=", "=", ">=", ">",
"+", "-", "*", "&&", "||", "!"] "+", "-", "*", "&&", "||", "!"]
} }
...@@ -142,13 +142,18 @@ parseOp = (reservedOp "<" *> return Lt) <|> ...@@ -142,13 +142,18 @@ parseOp = (reservedOp "<" *> return Lt) <|>
(reservedOp ">" *> return Gt) <|> (reservedOp ">" *> return Gt) <|>
(reservedOp ">=" *> return Ge) (reservedOp ">=" *> return Ge)
atom :: Parser Formula linIneq :: Parser Formula
atom = do linIneq = do
lhs <- term lhs <- term
op <- parseOp op <- parseOp
rhs <- term rhs <- term
return (Atom (LinIneq lhs op rhs)) return (Atom (LinIneq lhs op rhs))
atom :: Parser Formula
atom = (reserved "true" *> return FTrue) <|>
(reserved "false" *> return FFalse) <|>
linIneq
parensForm :: Parser Formula parensForm :: Parser Formula
parensForm = atom <|> parens formula parensForm = atom <|> parens formula
......
...@@ -40,7 +40,8 @@ data LinearInequation = LinIneq Term Op Term ...@@ -40,7 +40,8 @@ data LinearInequation = LinIneq Term Op Term
instance Show LinearInequation where instance Show LinearInequation where
show (LinIneq lhs op rhs) = show lhs ++ " " ++ show op ++ " " ++ show rhs show (LinIneq lhs op rhs) = show lhs ++ " " ++ show op ++ " " ++ show rhs
data Formula = Atom LinearInequation data Formula = FTrue | FFalse
| Atom LinearInequation
| Neg Formula | Neg Formula
| Formula :&: Formula | Formula :&: Formula
| Formula :|: Formula | Formula :|: Formula
...@@ -49,6 +50,8 @@ infixr 3 :&: ...@@ -49,6 +50,8 @@ infixr 3 :&:
infixr 2 :|: infixr 2 :|:
instance Show Formula where instance Show Formula where
show FTrue = "true"
show FFalse = "false"
show (Atom a) = show a show (Atom a) = show a
show (Neg p) = "¬" ++ "(" ++ show p ++ ")" show (Neg p) = "¬" ++ "(" ++ show p ++ ")"
show (p :&: q) = "(" ++ show p ++ " ∧ " ++ show q ++ ")" show (p :&: q) = "(" ++ show p ++ " ∧ " ++ show q ++ ")"
......
...@@ -24,6 +24,8 @@ evaluateLinIneq (LinIneq lhs op rhs) m = ...@@ -24,6 +24,8 @@ evaluateLinIneq (LinIneq lhs op rhs) m =
opToFunction op (evaluateTerm lhs m) (evaluateTerm rhs m) opToFunction op (evaluateTerm lhs m) (evaluateTerm rhs m)
evaluateFormula :: Formula -> ModelSI -> SBool evaluateFormula :: Formula -> ModelSI -> SBool
evaluateFormula FTrue _ = true
evaluateFormula FFalse _ = false
evaluateFormula (Atom a) m = evaluateLinIneq a m evaluateFormula (Atom a) m = evaluateLinIneq a m
evaluateFormula (Neg p) m = bnot $ evaluateFormula p m evaluateFormula (Neg p) m = bnot $ evaluateFormula p m
evaluateFormula (p :&: q) m = evaluateFormula p m &&& evaluateFormula q m evaluateFormula (p :&: q) m = evaluateFormula p m &&& evaluateFormula q m
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment