Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell98 |
Inspired by Simple SMT Solver.
In future this module will probably be moved into separate package.
Synopsis
- 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 :: Ord a => LatticeSyntax a -> LatticeSyntax a -> Bool
- preorder :: Ord a => LatticeSyntax a -> LatticeSyntax a -> Bool
- satisfiable :: Ord a => LatticeSyntax a -> Bool
Documentation
data LatticeSyntax a Source #
LVar a | |
LBound Bool | |
LJoin (LatticeSyntax a) (LatticeSyntax a) | |
LMeet (LatticeSyntax a) (LatticeSyntax a) |
Instances
dual :: LatticeSyntax a -> LatticeSyntax a Source #
freeVars :: LatticeSyntax a -> [a] Source #
equivalent :: Ord 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 :: Ord 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 :: Ord a => LatticeSyntax a -> Bool Source #