| Copyright | (c) 2015 Oleg Grenrus |
|---|---|
| License | BSD3 |
| Maintainer | Oleg Grenrus <oleg.grenrus@iki.fi> |
| Safe Haskell | Safe |
| Language | Haskell98 |
Data.SPDX.LatticeSyntax
Description
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
Constructors
| LVar a | |
| LBound Bool | |
| LJoin (LatticeSyntax a) (LatticeSyntax a) | |
| LMeet (LatticeSyntax a) (LatticeSyntax a) |
Instances
| Monad LatticeSyntax | |
| Functor LatticeSyntax | |
| Applicative LatticeSyntax | |
| Foldable LatticeSyntax | |
| Traversable LatticeSyntax | |
| Eq a => Eq (LatticeSyntax a) | |
| Data a => Data (LatticeSyntax a) | |
| Ord a => Ord (LatticeSyntax a) | |
| Read a => Read (LatticeSyntax a) | |
| Show a => Show (LatticeSyntax a) | |
| Typeable (* -> *) LatticeSyntax |
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