jukebox-0.1: A first-order reasoning toolbox

Safe HaskellNone
LanguageHaskell98

Jukebox.Monotonox.ToFOF

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