Safe Haskell	None
Language	Haskell2010

Language.REST.WQOConstraints.ADT

Documentation

type WQO = WQO Source #

data ConstraintsADT a Source #

Constructors

Sat (WQO a)
Unsat
Union (ConstraintsADT a) (ConstraintsADT a)
Intersect (ConstraintsADT a) (ConstraintsADT a)

Instances

Instances details

Eq a => Eq (ConstraintsADT a) Source #
Instance details Defined in Language.REST.WQOConstraints.ADT Methods (==) :: ConstraintsADT a -> ConstraintsADT a -> Bool # (/=) :: ConstraintsADT a -> ConstraintsADT a -> Bool #
Ord a => Ord (ConstraintsADT a) Source #
Instance details Defined in Language.REST.WQOConstraints.ADT Methods compare :: ConstraintsADT a -> ConstraintsADT a -> Ordering # (<) :: ConstraintsADT a -> ConstraintsADT a -> Bool # (<=) :: ConstraintsADT a -> ConstraintsADT a -> Bool # (>) :: ConstraintsADT a -> ConstraintsADT a -> Bool # (>=) :: ConstraintsADT a -> ConstraintsADT a -> Bool # max :: ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a # min :: ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a #
(Eq a, Hashable a, Show a) => Show (ConstraintsADT a) Source #
Instance details Defined in Language.REST.WQOConstraints.ADT Methods showsPrec :: Int -> ConstraintsADT a -> ShowS # show :: ConstraintsADT a -> String # showList :: [ConstraintsADT a] -> ShowS #
Generic (ConstraintsADT a) Source #
Instance details Defined in Language.REST.WQOConstraints.ADT Associated Types type Rep (ConstraintsADT a) :: Type -> Type # Methods from :: ConstraintsADT a -> Rep (ConstraintsADT a) x # to :: Rep (ConstraintsADT a) x -> ConstraintsADT a #
Hashable a => Hashable (ConstraintsADT a) Source #
Instance details Defined in Language.REST.WQOConstraints.ADT Methods hashWithSalt :: Int -> ConstraintsADT a -> Int # hash :: ConstraintsADT a -> Int #
ToSMTVar a Int => ToSMT (ConstraintsADT a) Bool Source #
Instance details Defined in Language.REST.WQOConstraints.ADT Methods toSMT :: ConstraintsADT a -> SMTExpr Bool Source #
type Rep (ConstraintsADT a) Source #
Instance details Defined in Language.REST.WQOConstraints.ADT type Rep (ConstraintsADT a) = D1 ('MetaData "ConstraintsADT" "Language.REST.WQOConstraints.ADT" "rest-rewrite-0.3.0-C58P8WPn3kHJiQCBn16Zwt" 'False) ((C1 ('MetaCons "Sat" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WQO a))) :+: C1 ('MetaCons "Unsat" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Union" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ConstraintsADT a)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ConstraintsADT a))) :+: C1 ('MetaCons "Intersect" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ConstraintsADT a)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ConstraintsADT a)))))

cost :: (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int Source #

minDepth :: ConstraintsADT a -> Int Source #

maxDepth :: ConstraintsADT a -> Int Source #

intersect :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a Source #

union :: Eq a => ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a Source #

addConstraint :: (Ord a, Hashable a) => WQO a -> ConstraintsADT a -> ConstraintsADT a Source #

relevantConstraints :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> Set a -> Set a -> ConstraintsADT a Source #

notStrongerThan :: (Eq a, ToSMTVar a Int) => ConstraintsADT a -> ConstraintsADT a -> SMTExpr Bool Source #

noConstraints :: ConstraintsADT a Source #

unsatisfiable :: ConstraintsADT a Source #

trace' :: String -> a -> a Source #

getConstraints :: forall a. (Show a, Ord a, Hashable a) => ConstraintsADT a -> [WQO a] Source #

data GCState a Source #

Constructors

GCState
Fields cs :: Map (ConstraintsADT a) (GCResult a) ms :: Map (WQO a, WQO a) (Maybe (WQO a))

type GCResult a = [WQO a] Source #

type GCMonad a = State (GCState a) (GCResult a) Source #

cached :: Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a Source #

cached' :: (Hashable a, Show a, Ord a) => (WQO a, WQO a) -> Maybe (WQO a) -> State (GCState a) (Maybe (WQO a)) Source #

getConstraints' :: forall a. (Show a, Ord a, Hashable a) => ConstraintsADT a -> State (GCState a) [WQO a] Source #

dnfSize :: ConstraintsADT a -> Int Source #

simplify :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> ConstraintsADT a Source #

permits :: (Ord a, Hashable a, Show a) => ConstraintsADT a -> WQO a -> Bool Source #

isSatisfiable :: (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => ConstraintsADT a -> SMTExpr Bool Source #

adtOC :: (Handle, Handle) -> WQOConstraints ConstraintsADT IO Source #

adtOC' :: WQOConstraints ConstraintsADT SMTExpr Source #