You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
97 lines
2.7 KiB
97 lines
2.7 KiB
module Systems where
|
|
|
|
import qualified Data.Map.Strict as Map
|
|
import qualified Data.Set as Set
|
|
import Data.Map.Strict (Map)
|
|
import Data.Set (Set)
|
|
import Data.List
|
|
|
|
import Presyntax
|
|
|
|
newtype Face = Face { getFace :: Map String Bool }
|
|
deriving (Eq, Show, Ord)
|
|
|
|
evalFormula :: Formula -> Face -> Bool
|
|
evalFormula (Is0 x) f =
|
|
case Map.lookup x (getFace f) of
|
|
Just x -> not x
|
|
Nothing -> error $ "dimension not bound in formula: " ++ show x
|
|
|
|
evalFormula (Is1 x) f =
|
|
case Map.lookup x (getFace f) of
|
|
Just x -> x
|
|
Nothing -> error $ "dimension not bound in formula: " ++ show x
|
|
|
|
evalFormula (And a b) f = evalFormula a f && evalFormula b f
|
|
evalFormula (Or a b) f = evalFormula a f || evalFormula b f
|
|
|
|
evalFormula Top _ = True
|
|
evalFormula Bot _ = False
|
|
|
|
freeVarsFormula :: Formula -> Set String
|
|
freeVarsFormula (Is0 x) = Set.singleton x
|
|
freeVarsFormula (Is1 x) = Set.singleton x
|
|
freeVarsFormula (And a b) = Set.union (freeVarsFormula a) (freeVarsFormula b)
|
|
freeVarsFormula (Or a b) = Set.union (freeVarsFormula a) (freeVarsFormula b)
|
|
freeVarsFormula Top = mempty
|
|
freeVarsFormula Bot = mempty
|
|
|
|
faces :: Formula -> ([Face], [Face])
|
|
faces formula = partition (evalFormula formula) allPossible where
|
|
truths [] = [mempty]
|
|
truths (x:xs) = uncurry Map.insert <$> [(x, True), (x, False)] <*> truths xs
|
|
|
|
allPossible = Face <$> truths (Set.toList (freeVarsFormula formula))
|
|
|
|
impossible, possible, tautological :: Formula -> Bool
|
|
impossible = null . fst . faces
|
|
possible = not . null . fst . faces
|
|
tautological = not . null . snd . faces
|
|
|
|
toDNF :: Formula -> Formula
|
|
toDNF = orFormula . map formulaOfFace . fst . faces
|
|
|
|
formulaOfFace :: Face -> Formula
|
|
formulaOfFace = andFormula . map (\(x, i) -> if i then Is1 x else Is0 x) . Map.toDescList . getFace
|
|
|
|
andFormula :: [Formula] -> Formula
|
|
andFormula = foldr and Top where
|
|
and x y =
|
|
case x of
|
|
Top -> case y of
|
|
Bot -> Bot
|
|
_ -> y
|
|
Bot -> Bot
|
|
_ -> case y of
|
|
Top -> x
|
|
_ -> And x y
|
|
|
|
orFormula :: [Formula] -> Formula
|
|
orFormula [] = Bot
|
|
orFormula (x:xs) = or x (orFormula xs) where
|
|
or x y =
|
|
case x of
|
|
Top -> Top
|
|
Bot -> case y of
|
|
Top -> Top
|
|
_ -> y
|
|
_ -> case y of
|
|
Bot -> x
|
|
_ -> Or x y
|
|
|
|
notFormula :: Formula -> Formula
|
|
notFormula Top = Bot
|
|
notFormula Bot = Top
|
|
notFormula (Is0 x) = Is1 x
|
|
notFormula (Is1 x) = Is0 x
|
|
notFormula (And x y) = Or (notFormula x) (notFormula y)
|
|
notFormula (Or x y) = And (notFormula x) (notFormula y)
|
|
|
|
newtype System a = FMap { getSystem :: Map Formula a }
|
|
deriving (Eq, Show, Ord)
|
|
|
|
emptySystem :: System a
|
|
emptySystem = FMap mempty
|
|
|
|
mapSystem :: System a -> (a -> b) -> System b
|
|
mapSystem (FMap x) f = FMap (Map.filterWithKey (\f _ -> f /= Bot) (fmap f x))
|