{-# OPTIONS_GHC -fno-warn-name-shadowing #-} module Property (Property(..), Formula(..), QuantFormula(..), quantifiedVariables, innerFormula, Op(..), Term(..), PropResult(..), resultAnd, resultOr, resultNot, resultsAnd, resultsOr) where data Term a = Var a | Const Integer | Minus (Term a) | Term a :+: Term a | Term a :-: Term a | Term a :*: Term a deriving (Eq) instance (Show a) => Show (Term a) where show (Var x) = show x show (Const c) = show c show (Minus t) = "-" ++ show t show (t :+: u) = "(" ++ show t ++ " + " ++ show u ++ ")" show (t :-: u) = "(" ++ show t ++ " - " ++ show u ++ ")" show (t :*: u) = show t ++ " * " ++ show u instance Functor Term where fmap f (Var x) = Var (f x) fmap _ (Const c) = Const c fmap f (Minus t) = Minus (fmap f t) fmap f (t :+: u) = fmap f t :+: fmap f u fmap f (t :-: u) = fmap f t :-: fmap f u fmap f (t :*: u) = fmap f t :*: fmap f u data Op = Gt | Ge | Eq | Ne | Le | Lt deriving (Eq) instance Show Op where show Gt = ">" show Ge = "≥" show Eq = "=" show Ne = "≠" show Le = "≤" show Lt = "<" data QuantFormula a = ExQuantFormula [a] (Formula a) deriving (Eq) data Formula a = FTrue | FFalse | LinearInequation (Term a) Op (Term a) | Neg (Formula a) | Formula a :&: Formula a | Formula a :|: Formula a deriving (Eq) infixr 3 :&: infixr 2 :|: quantifiedVariables :: QuantFormula a -> [a] quantifiedVariables (ExQuantFormula xs _) = xs innerFormula :: QuantFormula a -> Formula a innerFormula (ExQuantFormula _ p) = p instance (Show a) => Show (QuantFormula a) where show (ExQuantFormula [] p) = show p show (ExQuantFormula ps p) = "∃" ++ unwords (map show ps) ++ ": " ++ show p instance (Show a) => Show (Formula a) where show FTrue = "true" show FFalse = "false" show (LinearInequation lhs op rhs) = show lhs ++ " " ++ show op ++ " " ++ show rhs show (Neg p) = "¬" ++ "(" ++ show p ++ ")" show (p :&: q) = "(" ++ show p ++ " ∧ " ++ show q ++ ")" show (p :|: q) = "(" ++ show p ++ " ∨ " ++ show q ++ ")" instance Functor QuantFormula where fmap f (ExQuantFormula xs p) = ExQuantFormula (fmap f xs) (fmap f p) instance Functor Formula where fmap _ FTrue = FTrue fmap _ FFalse = FFalse fmap f (LinearInequation lhs op rhs) = LinearInequation (fmap f lhs) op (fmap f rhs) fmap f (Neg p) = Neg (fmap f p) fmap f (p :&: q) = fmap f p :&: fmap f q fmap f (p :|: q) = fmap f p :|: fmap f q data Property = LayeredTermination | StrongConsensus | StrongConsensusWithCorrectness instance Show Property where show LayeredTermination = "layered termination" show StrongConsensus = "strong consensus" show StrongConsensusWithCorrectness = "strong consensus with correctness" data PropResult = Satisfied | Unsatisfied | Unknown deriving (Eq) instance Show PropResult where show Satisfied = "satisfied" show Unsatisfied = "not satisfied" show Unknown = "may not be satisfied" resultAnd :: PropResult -> PropResult -> PropResult resultAnd Satisfied x = x resultAnd Unsatisfied _ = Unsatisfied resultAnd _ Unsatisfied = Unsatisfied resultAnd Unknown _ = Unknown resultOr :: PropResult -> PropResult -> PropResult resultOr Satisfied _ = Satisfied resultOr _ Satisfied = Satisfied resultOr Unsatisfied x = x resultOr Unknown _ = Unknown resultNot :: PropResult -> PropResult resultNot Satisfied = Unsatisfied resultNot Unsatisfied = Unsatisfied resultNot Unknown = Unknown resultsAnd :: [PropResult] -> PropResult resultsAnd = foldr resultAnd Satisfied resultsOr :: [PropResult] -> PropResult resultsOr = foldr resultOr Unsatisfied