jukebox-0.4.2: A first-order reasoning toolbox

Safe Haskell	None
Language	Haskell98

Jukebox.Tools.EncodeTypes

Documentation

data Scheme Source #

Constructors

Scheme
Fields makeFunction :: Type -> NameM Function scheme1 :: (Type -> Bool) -> (Type -> Function) -> Scheme1

data Scheme1 Source #

Constructors

Scheme1
Fields forAll :: Bind Form -> Form exists :: Bind Form -> Form equals :: Term -> Term -> Form funcAxiom :: Function -> NameM Form typeAxiom :: Type -> NameM Form

guard :: Scheme1 -> (Type -> Bool) -> Input Form -> Input Form Source #

translate :: Scheme -> (Type -> Bool) -> Problem Form -> Problem Form Source #

translate1 :: Scheme -> (Type -> Bool) -> Problem Form -> Problem Form Source #

tagsFlags :: OptionParser Bool Source #

tags :: Bool -> Scheme Source #

tags1 :: Bool -> (Type -> Bool) -> (Type -> Function) -> Scheme1 Source #

tagsAxiom :: Bool -> (Type -> Bool) -> (Type -> Function) -> Function -> NameM Form Source #

tagsExists :: (Type -> Bool) -> Type -> Function -> NameM Form Source #

guards :: Scheme Source #

guards1 :: (Type -> Bool) -> (Type -> Function) -> Scheme1 Source #

naked :: Symbolic a => Bool -> Variable -> a -> Bool Source #

guardsAxiom :: (Type -> Bool) -> (Type -> Function) -> Function -> NameM Form Source #

guardsTypeAxiom :: (Type -> Bool) -> (Type -> Function) -> Type -> NameM Form Source #