Safe Haskell	None
Language	Haskell2010

Twee.Constraints

Documentation

data Atom f Source #

Constructors

Constant (Fun f)
Variable Var

Instances

Eq (Fun f) => Eq (Atom f) Source #
Methods (==) :: Atom f -> Atom f -> Bool # (/=) :: Atom f -> Atom f -> Bool #
Ord (Fun f) => Ord (Atom f) Source #
Methods compare :: Atom f -> Atom f -> Ordering # (<) :: Atom f -> Atom f -> Bool # (<=) :: Atom f -> Atom f -> Bool # (>) :: Atom f -> Atom f -> Bool # (>=) :: Atom f -> Atom f -> Bool # max :: Atom f -> Atom f -> Atom f # min :: Atom f -> Atom f -> Atom f #
Show (Atom f) Source #
Methods showsPrec :: Int -> Atom f -> ShowS # show :: Atom f -> String # showList :: [Atom f] -> ShowS #
(Numbered f, PrettyTerm f) => Pretty (Atom f) Source #
Methods pPrintPrec :: PrettyLevel -> Rational -> Atom f -> Doc # pPrint :: Atom f -> Doc # pPrintList :: PrettyLevel -> [Atom f] -> Doc #

atoms :: Term f -> [Atom f] Source #

toTerm :: Atom f -> Term f Source #

fromTerm :: Term f -> Maybe (Atom f) Source #

data Formula f Source #

Constructors

Less (Atom f) (Atom f)
LessEq (Atom f) (Atom f)
And [Formula f]
Or [Formula f]

Instances

Eq (Fun f) => Eq (Formula f) Source #
Methods (==) :: Formula f -> Formula f -> Bool # (/=) :: Formula f -> Formula f -> Bool #
Ord (Fun f) => Ord (Formula f) Source #
Methods compare :: Formula f -> Formula f -> Ordering # (<) :: Formula f -> Formula f -> Bool # (<=) :: Formula f -> Formula f -> Bool # (>) :: Formula f -> Formula f -> Bool # (>=) :: Formula f -> Formula f -> Bool # max :: Formula f -> Formula f -> Formula f # min :: Formula f -> Formula f -> Formula f #
Show (Formula f) Source #
Methods showsPrec :: Int -> Formula f -> ShowS # show :: Formula f -> String # showList :: [Formula f] -> ShowS #
(Numbered f, PrettyTerm f) => Pretty (Formula f) Source #
Methods pPrintPrec :: PrettyLevel -> Rational -> Formula f -> Doc # pPrint :: Formula f -> Doc # pPrintList :: PrettyLevel -> [Formula f] -> Doc #

negateFormula :: Formula f -> Formula f Source #

conj :: (Foldable t, Numbered f, Ord f) => t (Formula f) -> Formula f Source #

disj :: (Foldable t, Numbered f, Ord f) => t (Formula f) -> Formula f Source #

(&&&) :: (Ord f, Numbered f) => Formula f -> Formula f -> Formula f Source #

(|||) :: (Ord f, Numbered f) => Formula f -> Formula f -> Formula f Source #

true :: Formula f Source #

false :: Formula f Source #

data Branch f Source #

Constructors

Branch
Fields funs :: [Fun f] less :: [(Atom f, Atom f)] equals :: [(Atom f, Atom f)]

Instances

Eq (Fun f) => Eq (Branch f) Source #
Methods (==) :: Branch f -> Branch f -> Bool # (/=) :: Branch f -> Branch f -> Bool #
Ord (Fun f) => Ord (Branch f) Source #
Methods compare :: Branch f -> Branch f -> Ordering # (<) :: Branch f -> Branch f -> Bool # (<=) :: Branch f -> Branch f -> Bool # (>) :: Branch f -> Branch f -> Bool # (>=) :: Branch f -> Branch f -> Bool # max :: Branch f -> Branch f -> Branch f # min :: Branch f -> Branch f -> Branch f #
(Numbered f, PrettyTerm f) => Pretty (Branch f) Source #
Methods pPrintPrec :: PrettyLevel -> Rational -> Branch f -> Doc # pPrint :: Branch f -> Doc # pPrintList :: PrettyLevel -> [Branch f] -> Doc #

trueBranch :: Branch f Source #

norm :: Eq f => Branch f -> Atom f -> Atom f Source #

contradictory :: (Numbered f, Minimal f, Ord f) => Branch f -> Bool Source #

formAnd :: (Numbered f, Minimal f, Ord f) => Formula f -> [Branch f] -> [Branch f] Source #

branches :: (Numbered f, Minimal f, Ord f) => Formula f -> [Branch f] Source #

addLess :: (Numbered f, Minimal f, Ord f) => Atom f -> Atom f -> Branch f -> [Branch f] Source #

addEquals :: (Numbered f, Minimal f, Ord f) => Atom f -> Atom f -> Branch f -> [Branch f] Source #

addTerm :: (Numbered f, Minimal f, Ord f) => Atom f -> Branch f -> Branch f Source #

newtype Model f Source #

Constructors

Model (Map (Atom f) (Int, Int))

Instances

Show (Model f) Source #
Methods showsPrec :: Int -> Model f -> ShowS # show :: Model f -> String # showList :: [Model f] -> ShowS #
(Numbered f, PrettyTerm f) => Pretty (Model f) Source #
Methods pPrintPrec :: PrettyLevel -> Rational -> Model f -> Doc # pPrint :: Model f -> Doc # pPrintList :: PrettyLevel -> [Model f] -> Doc #

modelToLiterals :: Model f -> [Formula f] Source #

modelFromOrder :: (Numbered f, Minimal f, Ord f) => [Atom f] -> Model f Source #

weakenModel :: Ord (Fun f) => Model f -> [Model f] Source #

varInModel :: (Numbered f, Minimal f, Ord f) => Model f -> Var -> Bool Source #

varGroups :: (Numbered f, Minimal f, Ord f) => Model f -> [(Fun f, [Var], Maybe (Fun f))] Source #

class Minimal a where Source #

Minimal complete definition

minimal

Methods

minimal :: a Source #

Instances

(Numbered f, Minimal f) => Minimal (Fun f) Source #
Methods minimal :: Fun f Source #
Minimal (Extended f) Source #
Methods minimal :: Extended f Source #

lessEqInModel :: (Numbered f, Minimal f, Ord f) => Model f -> Atom f -> Atom f -> Maybe Strictness Source #

solve :: (Numbered f, Minimal f, Ord f, PrettyTerm f) => [Atom f] -> Branch f -> Either (Model f) (Subst f) Source #

class Ord f => Ordered f where Source #

Minimal complete definition

lessEq, lessIn

Methods

orientTerms :: Term f -> Term f -> Maybe Ordering Source #

lessEq :: Term f -> Term f -> Bool Source #

lessIn :: Model f -> Term f -> Term f -> Maybe Strictness Source #

data Strictness Source #

Constructors

Strict
Nonstrict

Instances

Eq Strictness Source #
Methods (==) :: Strictness -> Strictness -> Bool # (/=) :: Strictness -> Strictness -> Bool #
Show Strictness Source #
Methods showsPrec :: Int -> Strictness -> ShowS # show :: Strictness -> String # showList :: [Strictness] -> ShowS #