Copyright | (c) 2015 Oleg Grenrus |
---|---|
License | BSD3 |
Maintainer | Oleg Grenrus <oleg.grenrus@iki.fi> |
Safe Haskell | Safe |
Language | Haskell98 |
Inspired by Simple SMT Solver.
In future this module will probably be moved into separate package.
- data LatticeSyntax a
- = LVar a
- | LBound Bool
- | LJoin (LatticeSyntax a) (LatticeSyntax a)
- | LMeet (LatticeSyntax a) (LatticeSyntax a)
- dual :: LatticeSyntax a -> LatticeSyntax a
- freeVars :: LatticeSyntax a -> [a]
- equivalent :: Eq a => LatticeSyntax a -> LatticeSyntax a -> Bool
- preorder :: Eq a => LatticeSyntax a -> LatticeSyntax a -> Bool
- satisfiable :: Eq a => LatticeSyntax a -> Bool
Documentation
data LatticeSyntax a Source #
LVar a | |
LBound Bool | |
LJoin (LatticeSyntax a) (LatticeSyntax a) | |
LMeet (LatticeSyntax a) (LatticeSyntax a) |
Monad LatticeSyntax Source # | |
Functor LatticeSyntax Source # | |
Applicative LatticeSyntax Source # | |
Foldable LatticeSyntax Source # | |
Traversable LatticeSyntax Source # | |
Eq a => Eq (LatticeSyntax a) Source # | |
Data a => Data (LatticeSyntax a) Source # | |
Ord a => Ord (LatticeSyntax a) Source # | |
Read a => Read (LatticeSyntax a) Source # | |
Show a => Show (LatticeSyntax a) Source # | |
dual :: LatticeSyntax a -> LatticeSyntax a Source #
freeVars :: LatticeSyntax a -> [a] Source #
equivalent :: Eq a => LatticeSyntax a -> LatticeSyntax a -> Bool Source #
Test for equivalence.
>>>
equivalent (LMeet (LVar 'a') (LVar 'b')) (LMeet (LVar 'b') (LVar 'a'))
True
>>>
equivalent (LVar 'a') (LMeet (LVar 'a') (LVar 'a'))
True
>>>
equivalent (LMeet (LVar 'a') (LVar 'b')) (LMeet (LVar 'b') (LVar 'b'))
False
preorder :: Eq a => LatticeSyntax a -> LatticeSyntax a -> Bool Source #
Test for preorder.
a ≤ b ⇔ a ∨ b ≡ b ⇔ a ≡ a ∧ b
>>>
preorder (LVar 'a' `LMeet` LVar 'b') (LVar 'a')
True
>>>
preorder (LVar 'a') (LVar 'a' `LMeet` LVar 'b')
False
satisfiable :: Eq a => LatticeSyntax a -> Bool Source #