| Safe Haskell | Safe |
|---|---|
| Language | Haskell98 |
Distribution.SPDX.Extra.Internal
Description
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 #
Constructors
| 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 #