-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | tons of inductive problems - support library and tools
--   
--   This package provides a tool for processing inductive theorem proving
--   problems in TIP format (see the homepage for details).
@package tip-lib
@version 0.2.2


-- | A representation of Haskell programs
module Tip.Haskell.Repr
data Decls a
Decls :: [Decl a] -> Decls a
data Decl a
TySig :: a -> [Type a] -> (Type a) -> Decl a
FunDecl :: a -> [([Pat a], Expr a)] -> Decl a
DataDecl :: a -> [a] -> [(a, [Type a])] -> [a] -> Decl a
InstDecl :: [Type a] -> (Type a) -> [Decl a] -> Decl a
ClassDecl :: [Type a] -> (Type a) -> [Decl a] -> Decl a
TypeDef :: (Type a) -> (Type a) -> Decl a
Where :: Decl a -> [Decl a] -> Decl a
TH :: (Expr a) -> Decl a
Module :: String -> Decl a
LANGUAGE :: String -> Decl a
QualImport :: String -> (Maybe String) -> Decl a
funDecl :: a -> [a] -> Expr a -> Decl a
data Type a
TyCon :: a -> [Type a] -> Type a
TyVar :: a -> Type a
TyTup :: [Type a] -> Type a
TyArr :: (Type a) -> (Type a) -> Type a
TyForall :: [a] -> (Type a) -> Type a
TyCtx :: [Type a] -> (Type a) -> Type a
TyImp :: a -> (Type a) -> Type a
modTyCon :: (a -> a) -> Type a -> Type a
data Expr a
Apply :: a -> [Expr a] -> Expr a
ImpVar :: a -> Expr a
Do :: [Stmt a] -> (Expr a) -> Expr a
Lam :: [Pat a] -> (Expr a) -> Expr a
Let :: a -> (Expr a) -> (Expr a) -> Expr a
ImpLet :: a -> (Expr a) -> (Expr a) -> Expr a
List :: [Expr a] -> Expr a
Tup :: [Expr a] -> Expr a
String :: a -> Expr a
Noop :: Expr a

-- | <pre>
--   return ()
--   </pre>
Case :: (Expr a) -> [(Pat a, Expr a)] -> Expr a
Int :: Integer -> Expr a
QuoteTyCon :: a -> Expr a
QuoteName :: a -> Expr a
THSplice :: (Expr a) -> Expr a
Record :: (Expr a) -> [(a, Expr a)] -> Expr a
(:::) :: Expr a -> Type a -> Expr a
nestedTyTup :: [Type a] -> Type a
nestedTup :: [Expr a] -> Expr a
nestedTupPat :: [Pat a] -> Pat a
mkDo :: [Stmt t] -> Expr t -> Expr t
var :: a -> Expr a
data Pat a
VarPat :: a -> Pat a
ConPat :: a -> [Pat a] -> Pat a
TupPat :: [Pat a] -> Pat a
WildPat :: Pat a
IntPat :: Integer -> Pat a
data Stmt a
Bind :: a -> (Expr a) -> Stmt a
BindTyped :: a -> (Type a) -> (Expr a) -> Stmt a
Stmt :: (Expr a) -> Stmt a
instance Data.Foldable.Foldable Tip.Haskell.Repr.Decls
instance Data.Traversable.Traversable Tip.Haskell.Repr.Decls
instance GHC.Base.Functor Tip.Haskell.Repr.Decls
instance GHC.Show.Show a => GHC.Show.Show (Tip.Haskell.Repr.Decls a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Haskell.Repr.Decls a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Haskell.Repr.Decls a)
instance Data.Foldable.Foldable Tip.Haskell.Repr.Decl
instance Data.Traversable.Traversable Tip.Haskell.Repr.Decl
instance GHC.Base.Functor Tip.Haskell.Repr.Decl
instance GHC.Show.Show a => GHC.Show.Show (Tip.Haskell.Repr.Decl a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Haskell.Repr.Decl a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Haskell.Repr.Decl a)
instance Data.Foldable.Foldable Tip.Haskell.Repr.Expr
instance Data.Traversable.Traversable Tip.Haskell.Repr.Expr
instance GHC.Base.Functor Tip.Haskell.Repr.Expr
instance GHC.Show.Show a => GHC.Show.Show (Tip.Haskell.Repr.Expr a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Haskell.Repr.Expr a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Haskell.Repr.Expr a)
instance Data.Foldable.Foldable Tip.Haskell.Repr.Stmt
instance Data.Traversable.Traversable Tip.Haskell.Repr.Stmt
instance GHC.Base.Functor Tip.Haskell.Repr.Stmt
instance GHC.Show.Show a => GHC.Show.Show (Tip.Haskell.Repr.Stmt a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Haskell.Repr.Stmt a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Haskell.Repr.Stmt a)
instance Data.Foldable.Foldable Tip.Haskell.Repr.Pat
instance Data.Traversable.Traversable Tip.Haskell.Repr.Pat
instance GHC.Base.Functor Tip.Haskell.Repr.Pat
instance GHC.Show.Show a => GHC.Show.Show (Tip.Haskell.Repr.Pat a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Haskell.Repr.Pat a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Haskell.Repr.Pat a)
instance Data.Foldable.Foldable Tip.Haskell.Repr.Type
instance Data.Traversable.Traversable Tip.Haskell.Repr.Type
instance GHC.Base.Functor Tip.Haskell.Repr.Type
instance GHC.Show.Show a => GHC.Show.Show (Tip.Haskell.Repr.Type a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Haskell.Repr.Type a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Haskell.Repr.Type a)

module Tip.Utils.Rename
type RenameM a b = ReaderT (Suggestor a b) (State (Map a b, Set b))
type Suggestor a b = a -> [b]
disambig :: (a -> String) -> Suggestor a String
disambig2 :: (a -> String) -> (b -> String) -> Suggestor (Either a b) String
evalRenameM :: (Ord b) => Suggestor a b -> [b] -> RenameM a b r -> r
runRenameM :: (Ord b) => Suggestor a b -> [b] -> Map a b -> RenameM a b r -> (r, Map a b)
insert :: (Ord a, Ord b) => a -> RenameM a b b
insertMany :: (Ord a, Ord b) => [a] -> RenameM a b [b]
lkup :: (Ord a, Ord b) => a -> RenameM a b b
rename :: (Ord a, Ord b, Traversable t) => t a -> RenameM a b (t b)
renameWith :: (Ord a, Ord b, Traversable t) => Suggestor a b -> t a -> t b
renameWithBlocks :: (Ord a, Ord b, Traversable t) => [b] -> Suggestor a b -> t a -> t b

module Tip.Writer
newtype WriterT w m a
WriterT :: (forall b. (w -> a -> m b) -> m b) -> WriterT w m a
[unWriterT] :: WriterT w m a -> forall b. (w -> a -> m b) -> m b
runWriterT :: (Monoid w, Monad m) => WriterT w m a -> m (a, w)
tell :: (Monoid w, Monad m) => w -> WriterT w m ()
lift :: (Monoid w, Monad m) => m a -> WriterT w m a
censor :: (Monoid w, Monad m) => (w -> w) -> WriterT w m a -> WriterT w m a
instance (GHC.Base.Monoid w, GHC.Base.Monad m) => GHC.Base.Functor (Tip.Writer.WriterT w m)
instance (GHC.Base.Monoid w, GHC.Base.Monad m) => GHC.Base.Applicative (Tip.Writer.WriterT w m)
instance (GHC.Base.Monoid w, GHC.Base.Monad m) => GHC.Base.Monad (Tip.Writer.WriterT w m)


-- | Handy utilities
module Tip.Utils

-- | Sort and remove duplicates
usort :: Ord a => [a] -> [a]

-- | Sort and remove duplicates wrt some custom ordering
usortOn :: Ord b => (a -> b) -> [a] -> [a]

-- | Union on a predicate
unionOn :: Ord b => (a -> b) -> [a] -> [a] -> [a]

-- | Returns the duplicates in a list
duplicates :: Ord a => [a] -> [a]
data Component a
Rec :: [a] -> Component a
NonRec :: a -> Component a
flattenComponent :: Component a -> [a]

-- | Strongly connected components
components :: Ord name => (thing -> name) -> (thing -> [name]) -> [thing] -> [Component thing]
lookupComponent :: Eq thing => thing -> [Component thing] -> Maybe (Component thing)

-- | Sort things in topologically in strongly connected components
sortThings :: Ord name => (thing -> name) -> (thing -> [name]) -> [thing] -> [[thing]]

-- | Recursive
recursive :: Ord name => (thing -> name) -> (thing -> [name]) -> [thing] -> [name]

-- | Makes a nice flag from a constructor string
--   
--   <pre>
--   &gt; flagify "PrintPolyFOL"
--   "print-poly-fol"
--   </pre>
flagify :: String -> String

-- | Makes a flag from something <tt>Show</tt>-able
flagifyShow :: Show a => a -> String

-- | Calculates the maximum value of a foldable value.
maximumOn :: (Foldable f, Ord b) => (a -> b) -> f a -> b

-- | Pair up a list with its previous elements
--   
--   <pre>
--   withPrevious "abc" = [('a',""),('b',"a"),('c',"ab")]
--   </pre>
withPrevious :: [a] -> [(a, [a])]

-- | Cursored traversal with previous and next elements of a list
cursor :: [a] -> [([a], a, [a])]
instance GHC.Base.Functor Tip.Utils.Component
instance GHC.Show.Show a => GHC.Show.Show (Tip.Utils.Component a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Utils.Component a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Utils.Component a)


-- | the abstract syntax
module Tip.Types
data Head a
Gbl :: (Global a) -> Head a
Builtin :: Builtin -> Head a
data Local a
Local :: a -> Type a -> Local a
[lcl_name] :: Local a -> a
[lcl_type] :: Local a -> Type a
data Global a
Global :: a -> PolyType a -> [Type a] -> Global a
[gbl_name] :: Global a -> a
[gbl_type] :: Global a -> PolyType a
[gbl_args] :: Global a -> [Type a]
data Expr a

-- | Function application: always perfectly saturated. Lambdas and locals
--   are applied with <a>At</a> as head.
(:@:) :: Head a -> [Expr a] -> Expr a
Lcl :: (Local a) -> Expr a
Lam :: [Local a] -> (Expr a) -> Expr a

-- | The default case comes first if there is one
Match :: (Expr a) -> [Case a] -> Expr a

-- | <tt>Let (Local x t) b e</tt> = <tt>(let ((l x)) b e)</tt> Unlike
--   SMT-LIB, this does not accept a list of bound
--   variable-/expression-pairs. Fix?
Let :: (Local a) -> (Expr a) -> (Expr a) -> Expr a
Quant :: QuantInfo -> Quant -> [Local a] -> (Expr a) -> Expr a
data Quant
Forall :: Quant
Exists :: Quant
data QuantInfo
NoInfo :: QuantInfo
QuantIH :: Int -> QuantInfo
data Case a
Case :: Pattern a -> Expr a -> Case a
[case_pat] :: Case a -> Pattern a
[case_rhs] :: Case a -> Expr a
data Builtin
At :: Builtin
Lit :: Lit -> Builtin
And :: Builtin
Or :: Builtin
Not :: Builtin
Implies :: Builtin
Equal :: Builtin
Distinct :: Builtin
IntAdd :: Builtin
IntSub :: Builtin
IntMul :: Builtin
IntDiv :: Builtin
IntMod :: Builtin
IntGt :: Builtin
IntGe :: Builtin
IntLt :: Builtin
IntLe :: Builtin
intBuiltin :: Builtin -> Bool
litBuiltin :: Builtin -> Bool
eqRelatedBuiltin :: Builtin -> Bool
logicalBuiltin :: Builtin -> Bool
data Lit
Int :: Integer -> Lit
Bool :: Bool -> Lit
String :: String -> Lit

-- | Patterns in branches
data Pattern a
Default :: Pattern a
ConPat :: Global a -> [Local a] -> Pattern a
[pat_con] :: Pattern a -> Global a
[pat_args] :: Pattern a -> [Local a]
LitPat :: Lit -> Pattern a

-- | Polymorphic types
data PolyType a
PolyType :: [a] -> [Type a] -> Type a -> PolyType a
[polytype_tvs] :: PolyType a -> [a]
[polytype_args] :: PolyType a -> [Type a]
[polytype_res] :: PolyType a -> Type a

-- | Types
data Type a
TyVar :: a -> Type a
TyCon :: a -> [Type a] -> Type a
(:=>:) :: [Type a] -> Type a -> Type a
BuiltinType :: BuiltinType -> Type a
data BuiltinType
Integer :: BuiltinType
Boolean :: BuiltinType
data Function a
Function :: a -> [a] -> [Local a] -> Type a -> Expr a -> Function a
[func_name] :: Function a -> a
[func_tvs] :: Function a -> [a]
[func_args] :: Function a -> [Local a]
[func_res] :: Function a -> Type a
[func_body] :: Function a -> Expr a

-- | Uninterpreted function
data Signature a
Signature :: a -> PolyType a -> Signature a
[sig_name] :: Signature a -> a
[sig_type] :: Signature a -> PolyType a

-- | Uninterpreted sort
data Sort a
Sort :: a -> [a] -> Sort a
[sort_name] :: Sort a -> a
[sort_tvs] :: Sort a -> [a]

-- | Data definition
data Datatype a
Datatype :: a -> [a] -> [Constructor a] -> Datatype a
[data_name] :: Datatype a -> a
[data_tvs] :: Datatype a -> [a]
[data_cons] :: Datatype a -> [Constructor a]
data Constructor a
Constructor :: a -> a -> [(a, Type a)] -> Constructor a

-- | Constructor name (e.g. <tt>Cons</tt>)
[con_name] :: Constructor a -> a

-- | Discriminator name (e.g. <tt>is-Cons</tt>)
[con_discrim] :: Constructor a -> a

-- | Argument types names of their projectors (e.g.
--   [(<tt>head</tt>,a),(<tt>tail</tt>,List a)])
[con_args] :: Constructor a -> [(a, Type a)]
data Theory a
Theory :: [Datatype a] -> [Sort a] -> [Signature a] -> [Function a] -> [Formula a] -> Theory a
[thy_datatypes] :: Theory a -> [Datatype a]
[thy_sorts] :: Theory a -> [Sort a]
[thy_sigs] :: Theory a -> [Signature a]
[thy_funcs] :: Theory a -> [Function a]
[thy_asserts] :: Theory a -> [Formula a]
emptyTheory :: Theory a
joinTheories :: Theory a -> Theory a -> Theory a
data Formula a
Formula :: Role -> Info a -> [a] -> Expr a -> Formula a
[fm_role] :: Formula a -> Role
[fm_info] :: Formula a -> Info a

-- | top-level quantified type variables
[fm_tvs] :: Formula a -> [a]
[fm_body] :: Formula a -> Expr a
data Info a
Definition :: a -> Info a
IH :: Int -> Info a
Lemma :: Int -> Info a
Projection :: a -> Info a
DataDomain :: a -> Info a
DataProjection :: a -> Info a
DataDistinct :: a -> Info a
Defunction :: a -> Info a
UserAsserted :: Info a
Unknown :: Info a
data Role
Assert :: Role
Prove :: Role

-- | The different kinds of declarations in a <a>Theory</a>.
data Decl a
DataDecl :: (Datatype a) -> Decl a
SortDecl :: (Sort a) -> Decl a
SigDecl :: (Signature a) -> Decl a
FuncDecl :: (Function a) -> Decl a
AssertDecl :: (Formula a) -> Decl a

-- | <a>Decl</a>arations in a <a>Theory</a>
theoryDecls :: Theory a -> [Decl a]

-- | Assemble a <a>Theory</a> from some <a>Decl</a>arations
declsToTheory :: [Decl a] -> Theory a
declsPass :: ([Decl a] -> [Decl b]) -> Theory a -> Theory b
transformExpr :: (Expr a -> Expr a) -> Expr a -> Expr a
transformExprM :: Monad m => (Expr a -> m (Expr a)) -> Expr a -> m (Expr a)
transformExprIn :: TransformBi (Expr a) (f a) => (Expr a -> Expr a) -> f a -> f a
transformExprInM :: TransformBiM m (Expr a) (f a) => (Expr a -> m (Expr a)) -> f a -> m (f a)
transformType :: (Type a -> Type a) -> Type a -> Type a
transformTypeInExpr :: (Type a -> Type a) -> Expr a -> Expr a
transformTypeInDecl :: (Type a -> Type a) -> Decl a -> Decl a
instance Data.Generics.Geniplate.TransformBi (Tip.Types.Type a0) (Tip.Types.Type a0)
instance GHC.Base.Monad m => Data.Generics.Geniplate.TransformBiM m (Tip.Types.Expr a) (Tip.Types.Expr a)
instance GHC.Base.Monad m => Data.Generics.Geniplate.TransformBiM m (Tip.Types.Expr a) (Tip.Types.Function a)
instance GHC.Base.Monad m => Data.Generics.Geniplate.TransformBiM m (Tip.Types.Pattern a) (Tip.Types.Expr a)
instance GHC.Base.Monad m => Data.Generics.Geniplate.TransformBiM m (Tip.Types.Local a) (Tip.Types.Expr a)
instance GHC.Base.Monad m => Data.Generics.Geniplate.TransformBiM m (Tip.Types.Expr a) (Tip.Types.Theory a)
instance GHC.Base.Monad m => Data.Generics.Geniplate.TransformBiM m (Tip.Types.Expr a) (Tip.Types.Formula a)
instance GHC.Base.Monad m => Data.Generics.Geniplate.TransformBiM m (Tip.Types.Type a) (Tip.Types.Type a)
instance GHC.Base.Monad m => Data.Generics.Geniplate.TransformBiM m (Tip.Types.Type a) (Tip.Types.Theory a)
instance GHC.Base.Monad m => Data.Generics.Geniplate.TransformBiM m (Tip.Types.Function a) (Tip.Types.Theory a)
instance Data.Generics.Geniplate.TransformBi (Tip.Types.Type a0) (Tip.Types.Expr a0)
instance Data.Generics.Geniplate.TransformBi (Tip.Types.Type a0) (Tip.Types.Decl a0)
instance Data.Generics.Geniplate.TransformBi (Tip.Types.Global a0) (Tip.Types.Theory a0)
instance Data.Generics.Geniplate.TransformBi (Tip.Types.Type a0) (Tip.Types.Theory a0)
instance Data.Generics.Geniplate.TransformBi (Tip.Types.Pattern a0) (Tip.Types.Theory a0)
instance Data.Generics.Geniplate.TransformBi (Tip.Types.Pattern a0) (Tip.Types.Expr a0)
instance Data.Generics.Geniplate.TransformBi (Tip.Types.Local a0) (Tip.Types.Expr a0)
instance Data.Generics.Geniplate.TransformBi (Tip.Types.Head a0) (Tip.Types.Theory a0)
instance Data.Generics.Geniplate.TransformBi (Tip.Types.Head a0) (Tip.Types.Expr a0)
instance Data.Generics.Geniplate.TransformBi (Tip.Types.Expr a0) (Tip.Types.Theory a0)
instance Data.Generics.Geniplate.TransformBi (Tip.Types.Expr a0) (Tip.Types.Function a0)
instance Data.Generics.Geniplate.TransformBi a0 (Tip.Types.Formula a0)
instance Data.Generics.Geniplate.TransformBi a0 (Tip.Types.Expr a0)
instance Data.Generics.Geniplate.TransformBi (Tip.Types.Expr a0) (Tip.Types.Expr a0)
instance Data.Generics.Geniplate.UniverseBi (Tip.Types.Theory a0) Tip.Types.Builtin
instance Data.Generics.Geniplate.UniverseBi (Tip.Types.Theory a0) (Tip.Types.Local a0)
instance Data.Generics.Geniplate.UniverseBi (Tip.Types.Theory a0) (Tip.Types.Global a0)
instance Data.Generics.Geniplate.UniverseBi (Tip.Types.Theory a0) (Tip.Types.Constructor a0)
instance Data.Generics.Geniplate.UniverseBi (Tip.Types.Type a0) (Tip.Types.Type a0)
instance Data.Generics.Geniplate.UniverseBi (Tip.Types.Theory a0) (Tip.Types.Type a0)
instance Data.Generics.Geniplate.UniverseBi (Tip.Types.Theory a0) (Tip.Types.Expr a0)
instance Data.Generics.Geniplate.UniverseBi (Tip.Types.Expr a0) (Tip.Types.Global a0)
instance Data.Generics.Geniplate.UniverseBi (Tip.Types.Expr a0) (Tip.Types.Local a0)
instance Data.Generics.Geniplate.UniverseBi (Tip.Types.Expr a0) (Tip.Types.Pattern a0)
instance Data.Generics.Geniplate.UniverseBi (Tip.Types.Datatype a0) (Tip.Types.Type a0)
instance Data.Generics.Geniplate.UniverseBi (Tip.Types.Function a0) (Tip.Types.Type a0)
instance Data.Generics.Geniplate.UniverseBi (Tip.Types.Function a0) (Tip.Types.Global a0)
instance Data.Generics.Geniplate.UniverseBi (Tip.Types.Function a0) (Tip.Types.Expr a0)
instance Data.Generics.Geniplate.UniverseBi (Tip.Types.Expr a0) (Tip.Types.Expr a0)
instance Data.Traversable.Traversable Tip.Types.Decl
instance Data.Foldable.Foldable Tip.Types.Decl
instance GHC.Base.Functor Tip.Types.Decl
instance GHC.Show.Show a => GHC.Show.Show (Tip.Types.Decl a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Types.Decl a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Types.Decl a)
instance Data.Traversable.Traversable Tip.Types.Theory
instance Data.Foldable.Foldable Tip.Types.Theory
instance GHC.Base.Functor Tip.Types.Theory
instance GHC.Show.Show a => GHC.Show.Show (Tip.Types.Theory a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Types.Theory a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Types.Theory a)
instance Data.Traversable.Traversable Tip.Types.Formula
instance Data.Foldable.Foldable Tip.Types.Formula
instance GHC.Base.Functor Tip.Types.Formula
instance GHC.Show.Show a => GHC.Show.Show (Tip.Types.Formula a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Types.Formula a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Types.Formula a)
instance GHC.Show.Show Tip.Types.Role
instance GHC.Classes.Ord Tip.Types.Role
instance GHC.Classes.Eq Tip.Types.Role
instance Data.Traversable.Traversable Tip.Types.Info
instance Data.Foldable.Foldable Tip.Types.Info
instance GHC.Base.Functor Tip.Types.Info
instance GHC.Show.Show a => GHC.Show.Show (Tip.Types.Info a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Types.Info a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Types.Info a)
instance Data.Traversable.Traversable Tip.Types.Datatype
instance Data.Foldable.Foldable Tip.Types.Datatype
instance GHC.Base.Functor Tip.Types.Datatype
instance GHC.Show.Show a => GHC.Show.Show (Tip.Types.Datatype a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Types.Datatype a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Types.Datatype a)
instance Data.Traversable.Traversable Tip.Types.Constructor
instance Data.Foldable.Foldable Tip.Types.Constructor
instance GHC.Base.Functor Tip.Types.Constructor
instance GHC.Show.Show a => GHC.Show.Show (Tip.Types.Constructor a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Types.Constructor a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Types.Constructor a)
instance Data.Traversable.Traversable Tip.Types.Sort
instance Data.Foldable.Foldable Tip.Types.Sort
instance GHC.Base.Functor Tip.Types.Sort
instance GHC.Show.Show a => GHC.Show.Show (Tip.Types.Sort a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Types.Sort a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Types.Sort a)
instance Data.Traversable.Traversable Tip.Types.Signature
instance Data.Foldable.Foldable Tip.Types.Signature
instance GHC.Base.Functor Tip.Types.Signature
instance GHC.Show.Show a => GHC.Show.Show (Tip.Types.Signature a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Types.Signature a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Types.Signature a)
instance Data.Traversable.Traversable Tip.Types.Function
instance Data.Foldable.Foldable Tip.Types.Function
instance GHC.Base.Functor Tip.Types.Function
instance GHC.Show.Show a => GHC.Show.Show (Tip.Types.Function a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Types.Function a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Types.Function a)
instance Data.Traversable.Traversable Tip.Types.Case
instance Data.Foldable.Foldable Tip.Types.Case
instance GHC.Base.Functor Tip.Types.Case
instance GHC.Show.Show a => GHC.Show.Show (Tip.Types.Case a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Types.Case a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Types.Case a)
instance Data.Traversable.Traversable Tip.Types.Expr
instance Data.Foldable.Foldable Tip.Types.Expr
instance GHC.Base.Functor Tip.Types.Expr
instance GHC.Show.Show a => GHC.Show.Show (Tip.Types.Expr a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Types.Expr a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Types.Expr a)
instance Data.Traversable.Traversable Tip.Types.Pattern
instance Data.Foldable.Foldable Tip.Types.Pattern
instance GHC.Base.Functor Tip.Types.Pattern
instance GHC.Show.Show a => GHC.Show.Show (Tip.Types.Pattern a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Types.Pattern a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Types.Pattern a)
instance Data.Traversable.Traversable Tip.Types.Local
instance Data.Foldable.Foldable Tip.Types.Local
instance GHC.Base.Functor Tip.Types.Local
instance GHC.Show.Show a => GHC.Show.Show (Tip.Types.Local a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Types.Local a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Types.Local a)
instance Data.Traversable.Traversable Tip.Types.Head
instance Data.Foldable.Foldable Tip.Types.Head
instance GHC.Base.Functor Tip.Types.Head
instance GHC.Show.Show a => GHC.Show.Show (Tip.Types.Head a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Types.Head a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Types.Head a)
instance Data.Traversable.Traversable Tip.Types.Global
instance Data.Foldable.Foldable Tip.Types.Global
instance GHC.Base.Functor Tip.Types.Global
instance GHC.Show.Show a => GHC.Show.Show (Tip.Types.Global a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Types.Global a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Types.Global a)
instance Data.Traversable.Traversable Tip.Types.PolyType
instance Data.Foldable.Foldable Tip.Types.PolyType
instance GHC.Base.Functor Tip.Types.PolyType
instance GHC.Show.Show a => GHC.Show.Show (Tip.Types.PolyType a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Types.PolyType a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Types.PolyType a)
instance Data.Traversable.Traversable Tip.Types.Type
instance Data.Foldable.Foldable Tip.Types.Type
instance GHC.Base.Functor Tip.Types.Type
instance GHC.Show.Show a => GHC.Show.Show (Tip.Types.Type a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Types.Type a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Types.Type a)
instance GHC.Show.Show Tip.Types.BuiltinType
instance GHC.Classes.Ord Tip.Types.BuiltinType
instance GHC.Classes.Eq Tip.Types.BuiltinType
instance GHC.Show.Show Tip.Types.Builtin
instance GHC.Classes.Ord Tip.Types.Builtin
instance GHC.Classes.Eq Tip.Types.Builtin
instance GHC.Show.Show Tip.Types.Lit
instance GHC.Classes.Ord Tip.Types.Lit
instance GHC.Classes.Eq Tip.Types.Lit
instance GHC.Show.Show Tip.Types.QuantInfo
instance GHC.Classes.Ord Tip.Types.QuantInfo
instance GHC.Classes.Eq Tip.Types.QuantInfo
instance GHC.Show.Show Tip.Types.Quant
instance GHC.Classes.Ord Tip.Types.Quant
instance GHC.Classes.Eq Tip.Types.Quant
instance GHC.Base.Monoid (Tip.Types.Theory a)

module Tip.Pretty

-- | Typeclass for pretty things
class Pretty a
pp :: Pretty a => a -> Doc

-- | Pretty to string
ppRender :: Pretty a => a -> String

-- | Print something pretty
pprint :: Pretty a => a -> IO ()

-- | Typeclass for variables
class PrettyVar a

-- | The string in a variable
varStr :: PrettyVar a => a -> String
newtype PPVar a
PPVar :: a -> PPVar a
[unPPVar] :: PPVar a -> a

-- | Variable to <a>Doc</a>
ppVar :: PrettyVar a => a -> Doc

-- | Infix <a>hang</a>
($\) :: Doc -> Doc -> Doc

-- | Conditional parentheses
parIf :: Bool -> Doc -> Doc
instance Tip.Pretty.PrettyVar a => Tip.Pretty.PrettyVar (Tip.Pretty.PPVar a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Pretty.PPVar a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Pretty.PPVar a)
instance Tip.Pretty.PrettyVar GHC.Base.String
instance Tip.Pretty.PrettyVar GHC.Types.Int
instance (Tip.Pretty.PrettyVar a, Tip.Pretty.PrettyVar b) => Tip.Pretty.PrettyVar (Data.Either.Either a b)
instance (Tip.Pretty.Pretty a, Tip.Pretty.Pretty b) => Tip.Pretty.Pretty (a, b)
instance (Tip.Pretty.Pretty a, Tip.Pretty.Pretty b, Tip.Pretty.Pretty c) => Tip.Pretty.Pretty (a, b, c)
instance Tip.Pretty.Pretty a => Tip.Pretty.Pretty [a]
instance Tip.Pretty.Pretty GHC.Types.Int
instance Tip.Pretty.Pretty ()
instance Tip.Pretty.PrettyVar a => Tip.Pretty.Pretty (Tip.Pretty.PPVar a)
instance Tip.Pretty.PrettyVar a => GHC.Show.Show (Tip.Pretty.PPVar a)


-- | Fresh monad and the Name type class
module Tip.Fresh

-- | The Fresh monad
newtype Fresh a
Fresh :: (State Int a) -> Fresh a

-- | Continues making unique names after the highest numbered name in a
--   foldable value.
freshPass :: (Foldable f, Name a) => (f a -> Fresh b) -> f a -> b

-- | Run fresh from starting from the greatest unique in a structure
freshFrom :: (Foldable f, Name b) => Fresh a -> f b -> a

-- | Run fresh, starting from zero
runFresh :: Fresh a -> a

-- | Run fresh from some starting value
runFreshFrom :: Int -> Fresh a -> a

-- | The Name type class
class (PrettyVar a, Ord a) => Name a where refresh _ = fresh freshNamed _ = fresh refreshNamed s n = freshNamed (s ++ varStr n)

-- | Make a fresh name
fresh :: Name a => Fresh a

-- | Refresh a name, which could have some resemblance to the original name
refresh :: Name a => a -> Fresh a

-- | Make a fresh name that can incorporate the given string
freshNamed :: Name a => String -> Fresh a

-- | Refresh a name with an additional hint string
refreshNamed :: Name a => String -> a -> Fresh a

-- | Gets the unique associated with a name.
getUnique :: Name a => a -> Int
instance Control.Monad.Fix.MonadFix Tip.Fresh.Fresh
instance GHC.Base.Functor Tip.Fresh.Fresh
instance GHC.Base.Applicative Tip.Fresh.Fresh
instance GHC.Base.Monad Tip.Fresh.Fresh
instance Tip.Fresh.Name GHC.Types.Int
instance Tip.Fresh.Name a => Tip.Fresh.Name (Tip.Pretty.PPVar a)

module Tip.Utils.Specialiser
specialise :: (Ord d, Ord c, Ord a) => [(d, [Rule c a])] -> ([(d, Subst a Void c)], [d])
safeRule :: Eq a => Rule c a -> Maybe (Rule c a)
data Rule c a
Rule :: [Expr c a] -> Expr c a -> Rule c a

-- | The trigger(s).
[rule_pre] :: Rule c a -> [Expr c a]

-- | The action. The variables here must be a subset of those in pre.
[rule_post] :: Rule c a -> Expr c a
data Expr c a
Var :: a -> Expr c a
Con :: c -> [Expr c a] -> Expr c a
data Void
absurd :: Void -> a
type Closed c = Expr c Void
subtermRules :: Rule c a -> [Rule c a]
subterms :: Expr c a -> [Expr c a]
type Subst a b c = [(a, Expr c b)]
type Inst a c = (Subst a Void c, Closed c)
instance GHC.Show.Show Tip.Utils.Specialiser.Void
instance GHC.Classes.Ord Tip.Utils.Specialiser.Void
instance GHC.Classes.Eq Tip.Utils.Specialiser.Void
instance Data.Traversable.Traversable Tip.Utils.Specialiser.Sk
instance Data.Foldable.Foldable Tip.Utils.Specialiser.Sk
instance GHC.Base.Functor Tip.Utils.Specialiser.Sk
instance GHC.Show.Show c => GHC.Show.Show (Tip.Utils.Specialiser.Sk c)
instance GHC.Classes.Ord c => GHC.Classes.Ord (Tip.Utils.Specialiser.Sk c)
instance GHC.Classes.Eq c => GHC.Classes.Eq (Tip.Utils.Specialiser.Sk c)
instance (Tip.Pretty.Pretty a, Tip.Pretty.Pretty c) => Tip.Pretty.Pretty (Tip.Utils.Specialiser.Expr c a)
instance (GHC.Classes.Eq a, Tip.Pretty.Pretty a, Tip.Pretty.Pretty c) => Tip.Pretty.Pretty (Tip.Utils.Specialiser.Rule c a)
instance Tip.Pretty.Pretty c => Tip.Pretty.Pretty (Tip.Utils.Specialiser.Sk c)
instance GHC.Classes.Ord c => Tip.Fresh.Name (Tip.Utils.Specialiser.Sk c)
instance Tip.Pretty.PrettyVar (Tip.Utils.Specialiser.Sk c)
instance Tip.Pretty.Pretty Tip.Utils.Specialiser.Void
instance Data.Traversable.Traversable (Tip.Utils.Specialiser.Rule c)
instance Data.Foldable.Foldable (Tip.Utils.Specialiser.Rule c)
instance GHC.Base.Functor (Tip.Utils.Specialiser.Rule c)
instance (GHC.Show.Show c, GHC.Show.Show a) => GHC.Show.Show (Tip.Utils.Specialiser.Rule c a)
instance (GHC.Classes.Ord c, GHC.Classes.Ord a) => GHC.Classes.Ord (Tip.Utils.Specialiser.Rule c a)
instance (GHC.Classes.Eq c, GHC.Classes.Eq a) => GHC.Classes.Eq (Tip.Utils.Specialiser.Rule c a)
instance Data.Traversable.Traversable (Tip.Utils.Specialiser.Expr c)
instance Data.Foldable.Foldable (Tip.Utils.Specialiser.Expr c)
instance GHC.Base.Functor (Tip.Utils.Specialiser.Expr c)
instance (GHC.Show.Show c, GHC.Show.Show a) => GHC.Show.Show (Tip.Utils.Specialiser.Expr c a)
instance (GHC.Classes.Ord c, GHC.Classes.Ord a) => GHC.Classes.Ord (Tip.Utils.Specialiser.Expr c a)
instance (GHC.Classes.Eq c, GHC.Classes.Eq a) => GHC.Classes.Eq (Tip.Utils.Specialiser.Expr c a)


-- | General functions for constructing and examining Tip syntax.
module Tip.Core
(===) :: Expr a -> Expr a -> Expr a
(=/=) :: Expr a -> Expr a -> Expr a
oppositeQuant :: Quant -> Quant
gentleNeg :: Expr a -> Expr a
neg :: Expr a -> Expr a
(/\) :: Expr a -> Expr a -> Expr a
(\/) :: Expr a -> Expr a -> Expr a
ands :: [Expr a] -> Expr a
ors :: [Expr a] -> Expr a
(==>) :: Expr a -> Expr a -> Expr a
(===>) :: [Expr a] -> Expr a -> Expr a
mkQuant :: Quant -> [Local a] -> Expr a -> Expr a
bool :: Bool -> Expr a
trueExpr :: Expr a
falseExpr :: Expr a
makeIf :: Expr a -> Expr a -> Expr a -> Expr a
intLit :: Integer -> Expr a
literal :: Lit -> Expr a
intType :: Type a
boolType :: Type a
applyFunction :: Function a -> [Type a] -> [Expr a] -> Expr a
applySignature :: Signature a -> [Type a] -> [Expr a] -> Expr a
apply :: Expr a -> [Expr a] -> Expr a
applyTypeIn :: Ord a => ((Type a -> Type a) -> f a -> f a) -> [a] -> [Type a] -> f a -> f a
applyType :: Ord a => [a] -> [Type a] -> Type a -> Type a
applyTypeInExpr :: Ord a => [a] -> [Type a] -> Expr a -> Expr a
applyTypeInDecl :: Ord a => [a] -> [Type a] -> Decl a -> Decl a
applyPolyType :: Ord a => PolyType a -> [Type a] -> ([Type a], Type a)
gblType :: Ord a => Global a -> ([Type a], Type a)
makeLets :: [(Local a, Expr a)] -> Expr a -> Expr a
collectLets :: Expr a -> ([(Local a, Expr a)], Expr a)
litView :: Expr a -> Maybe Lit
boolView :: Expr a -> Maybe Bool
forallView :: Expr a -> ([Local a], Expr a)

-- | A representation of Nested patterns, used in
--   <a>patternMatchingView</a>
data DeepPattern a
DeepConPat :: (Global a) -> [DeepPattern a] -> DeepPattern a
DeepVarPat :: (Local a) -> DeepPattern a
DeepLitPat :: Lit -> DeepPattern a

-- | Match as left-hand side pattern-matching definitions
--   
--   Stops at default patterns, for simplicity
patternMatchingView :: Ord a => [Local a] -> Expr a -> [([DeepPattern a], Expr a)]
ifView :: Expr a -> Maybe (Expr a, Expr a, Expr a)
projAt :: Expr a -> Maybe (Expr a, Expr a)
projGlobal :: Expr a -> Maybe a
atomic :: Expr a -> Bool
occurrences :: Eq a => Local a -> Expr a -> Int

-- | The signature of a function
signature :: Function a -> Signature a

-- | The type of a function
funcType :: Function a -> PolyType a
bound :: Ord a => Expr a -> [Local a]
free :: Ord a => Expr a -> [Local a]
locals :: Ord a => Expr a -> [Local a]
globals :: (UniverseBi (t a) (Global a), UniverseBi (t a) (Type a), Ord a) => t a -> [a]
tyVars :: Ord a => Type a -> [a]
freeTyVars :: Ord a => Expr a -> [a]

-- | The type of an expression
exprType :: Ord a => Expr a -> Type a

-- | The result type of a built in function, applied to some types
builtinType :: Ord a => Builtin -> [Type a] -> Type a
theoryTypes :: (UniverseBi (t a) (Type a), Ord a) => t a -> [Type a]
freshLocal :: Name a => Type a -> Fresh (Local a)
freshArgs :: Name a => Global a -> Fresh [Local a]
refreshLocal :: Name a => Local a -> Fresh (Local a)
freshen :: Name a => Expr a -> Fresh (Expr a)
freshenNames :: (TransformBi a (f a), Name a) => [a] -> f a -> Fresh (f a)

-- | Substitution, of local variables
--   
--   Since there are only rank-1 types, bound variables from lambdas and
--   case never have a forall type and thus are not applied to any types.
(//) :: Name a => Expr a -> Local a -> Expr a -> Fresh (Expr a)
substMany :: Name a => [(Local a, Expr a)] -> Expr a -> Fresh (Expr a)
letExpr :: Name a => Expr a -> (Local a -> Fresh (Expr a)) -> Fresh (Expr a)

-- | Substitution, but without refreshing. Only use when the replacement
--   expression contains no binders (i.e. no lambdas, no lets, no
--   quantifiers), since the binders are not refreshed at every insertion
--   point.
unsafeSubst :: Ord a => Expr a -> Local a -> Expr a -> Expr a
updateLocalType :: Type a -> Local a -> Local a
updateFuncType :: PolyType a -> Function a -> Function a
matchTypesIn :: Ord a => [a] -> [(Type a, Type a)] -> Maybe [Type a]
matchTypes :: Ord a => [(Type a, Type a)] -> Maybe [(a, Type a)]
makeGlobal :: Ord a => a -> PolyType a -> [Type a] -> Maybe (Type a) -> Maybe (Global a)
constructorType :: Datatype a -> Constructor a -> PolyType a
destructorType :: Datatype a -> Type a -> PolyType a
constructor :: Datatype a -> Constructor a -> [Type a] -> Global a
projector :: Datatype a -> Constructor a -> Int -> [Type a] -> Global a
discriminator :: Datatype a -> Constructor a -> [Type a] -> Global a

-- | Goals in first component, assertions in second
theoryGoals :: Theory a -> ([Formula a], [Formula a])

-- | Goals in first component, assertions in second
partitionGoals :: [Formula a] -> ([Formula a], [Formula a])
mapDecls :: (forall t. Traversable t => t a -> t b) -> Theory a -> Theory b
topsort :: (Ord a, Definition f) => [f a] -> [[f a]]
class Definition f
defines :: Definition f => f a -> a
uses :: Definition f => f a -> [a]
data (:+:) f g a
InL :: (f a) -> (:+:) f g a
InR :: (g a) -> (:+:) f g a
instance (GHC.Base.Functor f, GHC.Base.Functor g) => GHC.Base.Functor (f Tip.Core.:+: g)
instance (GHC.Show.Show (f a), GHC.Show.Show (g a)) => GHC.Show.Show ((Tip.Core.:+:) f g a)
instance (GHC.Classes.Ord (f a), GHC.Classes.Ord (g a)) => GHC.Classes.Ord ((Tip.Core.:+:) f g a)
instance (GHC.Classes.Eq (f a), GHC.Classes.Eq (g a)) => GHC.Classes.Eq ((Tip.Core.:+:) f g a)
instance (Tip.Core.Definition f, Tip.Core.Definition g) => Tip.Core.Definition (f Tip.Core.:+: g)
instance Tip.Core.Definition Tip.Types.Signature
instance Tip.Core.Definition Tip.Types.Function
instance Tip.Core.Definition Tip.Types.Datatype


-- | A monad for keeping track of variable scope.
module Tip.Scope

-- | The scope of a theory
scope :: (PrettyVar a, Ord a) => Theory a -> Scope a
data Scope a
Scope :: Set a -> Map a (TypeInfo a) -> Map a (Type a) -> Map a (GlobalInfo a) -> Scope a
[inner] :: Scope a -> Set a
[types] :: Scope a -> Map a (TypeInfo a)
[locals] :: Scope a -> Map a (Type a)
[globals] :: Scope a -> Map a (GlobalInfo a)
data TypeInfo a
TyVarInfo :: TypeInfo a
DatatypeInfo :: (Datatype a) -> TypeInfo a
SortInfo :: (Sort a) -> TypeInfo a
data GlobalInfo a
FunctionInfo :: (PolyType a) -> GlobalInfo a
ConstructorInfo :: (Datatype a) -> (Constructor a) -> GlobalInfo a
ProjectorInfo :: (Datatype a) -> (Constructor a) -> Int -> (Type a) -> GlobalInfo a
DiscriminatorInfo :: (Datatype a) -> (Constructor a) -> GlobalInfo a
globalType :: GlobalInfo a -> PolyType a
isType :: Ord a => a -> Scope a -> Bool
isTyVar :: Ord a => a -> Scope a -> Bool
isSort :: Ord a => a -> Scope a -> Bool
isLocal :: Ord a => a -> Scope a -> Bool
isGlobal :: Ord a => a -> Scope a -> Bool
lookupType :: Ord a => a -> Scope a -> Maybe (TypeInfo a)
lookupLocal :: Ord a => a -> Scope a -> Maybe (Type a)
lookupGlobal :: Ord a => a -> Scope a -> Maybe (GlobalInfo a)
lookupDatatype :: Ord a => a -> Scope a -> Maybe (Datatype a)
lookupFunction :: Ord a => a -> Scope a -> Maybe (PolyType a)
lookupConstructor :: Ord a => a -> Scope a -> Maybe (Datatype a, Constructor a)
lookupDiscriminator :: Ord a => a -> Scope a -> Maybe (Datatype a, Constructor a)
lookupProjector :: Ord a => a -> Scope a -> Maybe (Datatype a, Constructor a, Int, Type a)
whichDatatype :: Ord a => a -> Scope a -> Datatype a
whichLocal :: Ord a => a -> Scope a -> Type a
whichGlobal :: Ord a => a -> Scope a -> GlobalInfo a
whichFunction :: Ord a => a -> Scope a -> PolyType a
whichConstructor :: Ord a => a -> Scope a -> (Datatype a, Constructor a)
whichDiscriminator :: Ord a => a -> Scope a -> (Datatype a, Constructor a)
whichProjector :: Ord a => a -> Scope a -> (Datatype a, Constructor a, Int, Type a)
newtype ScopeT a m b
ScopeT :: StateT (Scope a) (ErrorT Doc m) b -> ScopeT a m b
[unScopeT] :: ScopeT a m b -> StateT (Scope a) (ErrorT Doc m) b
runScopeT :: Monad m => ScopeT a m b -> m (Either Doc b)
checkScopeT :: Monad m => ScopeT a m b -> m b
type ScopeM a = ScopeT a Identity
runScope :: ScopeM a b -> Either Doc b
checkScope :: ScopeM a b -> b
emptyScope :: Scope a
inContext :: Pretty a => a -> ScopeM b c -> ScopeM b c
local :: Monad m => ScopeT a m b -> ScopeT a m b
newScope :: Monad m => ScopeT a m b -> ScopeT a m b
newName :: (PrettyVar a, Ord a, Monad m) => a -> ScopeT a m ()
newTyVar :: (Monad m, Ord a, PrettyVar a) => a -> ScopeT a m ()
newSort :: (Monad m, Ord a, PrettyVar a) => Sort a -> ScopeT a m ()
newDatatype :: (Monad m, Ord a, PrettyVar a) => Datatype a -> ScopeT a m ()
newConstructor :: (Monad m, Ord a, PrettyVar a) => Datatype a -> Constructor a -> ScopeT a m ()
newFunction :: (Monad m, Ord a, PrettyVar a) => Signature a -> ScopeT a m ()
newLocal :: (Monad m, Ord a, PrettyVar a) => Local a -> ScopeT a m ()

-- | Add everything in a theory
withTheory :: (Monad m, Ord a, PrettyVar a) => Theory a -> ScopeT a m b -> ScopeT a m b
instance GHC.Base.Monad m => Control.Monad.Error.Class.MonadError Text.PrettyPrint.HughesPJ.Doc (Tip.Scope.ScopeT a m)
instance GHC.Base.Monad m => Control.Monad.State.Class.MonadState (Tip.Scope.Scope a) (Tip.Scope.ScopeT a m)
instance GHC.Base.Monad m => GHC.Base.Alternative (Tip.Scope.ScopeT a m)
instance GHC.Base.Monad m => GHC.Base.MonadPlus (Tip.Scope.ScopeT a m)
instance GHC.Base.Monad m => GHC.Base.Monad (Tip.Scope.ScopeT a m)
instance GHC.Base.Monad m => GHC.Base.Applicative (Tip.Scope.ScopeT a m)
instance GHC.Base.Functor m => GHC.Base.Functor (Tip.Scope.ScopeT a m)
instance GHC.Show.Show a => GHC.Show.Show (Tip.Scope.Scope a)
instance GHC.Show.Show a => GHC.Show.Show (Tip.Scope.GlobalInfo a)
instance GHC.Show.Show a => GHC.Show.Show (Tip.Scope.TypeInfo a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Scope.TypeInfo a)
instance Control.Monad.Trans.Class.MonadTrans (Tip.Scope.ScopeT a)
instance Control.Monad.Trans.Error.Error Text.PrettyPrint.HughesPJ.Doc

module Tip.Rename

-- | Renames a theory
renameAvoiding :: (Ord a, PrettyVar a) => [String] -> (Char -> String) -> Theory a -> Theory RenamedId

-- | The representation of renamed Ids.
newtype RenamedId
RenamedId :: String -> RenamedId
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Rename.TwoStage a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Rename.TwoStage a)
instance GHC.Show.Show Tip.Rename.RenamedId
instance GHC.Classes.Ord Tip.Rename.RenamedId
instance GHC.Classes.Eq Tip.Rename.RenamedId
instance Tip.Pretty.PrettyVar Tip.Rename.RenamedId
instance Tip.Pretty.PrettyVar a => GHC.Show.Show (Tip.Rename.TwoStage a)

module Tip.Pretty.SMT
expr :: Doc -> [Doc] -> Doc
parExpr :: Doc -> [Doc] -> Doc
parExprSep :: Doc -> [Doc] -> Doc
exprSep :: Doc -> [Doc] -> Doc
apply :: Doc -> Doc -> Doc
validSMTChar :: Char -> String
ppTheory :: (Ord a, PrettyVar a) => Theory a -> Doc
ppSort :: PrettyVar a => Sort a -> Doc
ppDatas :: PrettyVar a => [Datatype a] -> Doc
ppData :: PrettyVar a => Datatype a -> Doc
ppCon :: PrettyVar a => Constructor a -> Doc
par :: (PrettyVar a) => [a] -> Doc -> Doc
par' :: (PrettyVar a) => [a] -> Doc -> Doc
par'' :: (PrettyVar a) => [a] -> Doc -> Doc
ppUninterp :: PrettyVar a => Signature a -> Doc
ppFuncs :: (Ord a, PrettyVar a) => [Function a] -> Doc
ppFuncSig :: PrettyVar a => ([a] -> Doc -> Doc) -> Function a -> Doc -> Doc
ppFormula :: (Ord a, PrettyVar a) => Formula a -> Doc
ppExpr :: (Ord a, PrettyVar a) => Expr a -> Doc
ppLocals :: PrettyVar a => [Local a] -> Doc
ppLocal :: PrettyVar a => Local a -> Doc
ppHead :: PrettyVar a => Head a -> Doc
ppBuiltin :: Builtin -> Doc
ppLit :: Lit -> Doc
ppQuant :: Quant -> Doc
ppCase :: (Ord a, PrettyVar a) => Case a -> Doc
ppPat :: PrettyVar a => Pattern a -> Doc
ppType :: PrettyVar a => Type a -> Doc
ppBuiltinType :: BuiltinType -> Doc
ppPolyType :: PrettyVar a => PolyType a -> Doc
smtKeywords :: [String]
instance (GHC.Classes.Ord a, Tip.Pretty.PrettyVar a) => Tip.Pretty.Pretty (Tip.Types.Decl a)
instance (GHC.Classes.Ord a, Tip.Pretty.PrettyVar a) => Tip.Pretty.Pretty (Tip.Types.Theory a)
instance (GHC.Classes.Ord a, Tip.Pretty.PrettyVar a) => Tip.Pretty.Pretty (Tip.Types.Expr a)
instance Tip.Pretty.PrettyVar a => Tip.Pretty.Pretty (Tip.Types.PolyType a)
instance Tip.Pretty.PrettyVar a => Tip.Pretty.Pretty (Tip.Types.Type a)
instance (GHC.Classes.Ord a, Tip.Pretty.PrettyVar a) => Tip.Pretty.Pretty (Tip.Types.Function a)
instance (GHC.Classes.Ord a, Tip.Pretty.PrettyVar a) => Tip.Pretty.Pretty (Tip.Types.Formula a)
instance Tip.Pretty.PrettyVar a => Tip.Pretty.Pretty (Tip.Types.Datatype a)
instance Tip.Pretty.PrettyVar a => Tip.Pretty.Pretty (Tip.Types.Sort a)
instance Tip.Pretty.PrettyVar a => Tip.Pretty.Pretty (Tip.Types.Signature a)
instance Tip.Pretty.PrettyVar a => Tip.Pretty.Pretty (Tip.Types.Local a)
instance Tip.Pretty.PrettyVar a => Tip.Pretty.Pretty (Tip.Types.Global a)
instance Tip.Pretty.PrettyVar a => Tip.Pretty.Pretty (Tip.Types.Head a)
instance Tip.Pretty.PrettyVar a => Tip.Pretty.Pretty (Tip.Types.Pattern a)


-- | Check that a theory is well-typed.
--   
--   Invariants:
--   
--   <ul>
--   <li>No shadowing---checked by scope monad.</li>
--   <li>Each local is bound before it's used.</li>
--   <li>All expressions are well-typed.</li>
--   <li>The result of each constructor should be a value of that
--   datatype.</li>
--   <li>Default case comes first. No duplicate cases.</li>
--   <li>Expressions and formulas not mixed.</li>
--   </ul>
module Tip.Lint

-- | Crashes if the theory is malformed
lint :: (PrettyVar a, Ord a) => String -> Theory a -> Theory a

-- | Same as <a>lint</a>, but returns in a monad, for convenience
lintM :: (PrettyVar a, Ord a, Monad m) => String -> Theory a -> m (Theory a)

-- | Returns the error if the theory is malformed
lintTheory :: (PrettyVar a, Ord a) => Theory a -> Maybe Doc

-- | Returns a Left if the theory is malformed
lintEither :: (PrettyVar a, Ord a) => String -> Theory a -> Either Doc (Theory a)
instance GHC.Classes.Eq Tip.Lint.ExprKind

module Tip.Simplify

-- | Options for the simplifier
data SimplifyOpts a
SimplifyOpts :: Bool -> Bool -> (Occurrences -> Maybe (Scope a) -> Expr a -> Bool) -> Bool -> SimplifyOpts a

-- | Allow simplifications on lets
[touch_lets] :: SimplifyOpts a -> Bool

-- | transform <tt>(match x (case (K y) (e x y)))</tt> to <tt>(match x
--   (case (K y) (e (K y) y))</tt> This is useful for triggering other
--   known-case simplifications, and is therefore on by default.
[remove_variable_scrutinee_in_branches] :: SimplifyOpts a -> Bool

-- | Inlining predicate
[should_inline] :: SimplifyOpts a -> Occurrences -> Maybe (Scope a) -> Expr a -> Bool

-- | Allow function inlining to introduce match
[inline_match] :: SimplifyOpts a -> Bool
newtype Occurrences
Occurrences :: Int -> Occurrences

-- | Gentle, but without inlining
gentlyNoInline :: SimplifyOpts a

-- | Gentle options: if there is risk for code duplication, only inline
--   atomic expressions
gently :: SimplifyOpts a

-- | Aggressive options: inline everything that might plausibly lead to
--   simplification
aggressively :: Name a => SimplifyOpts a

-- | Simplify an entire theory
simplifyTheory :: Name a => SimplifyOpts a -> Theory a -> Fresh (Theory a)

-- | Simplify an expression, without knowing its theory
simplifyExpr :: (TransformBiM (WriterT Any Fresh) (Expr a) (f a), Name a) => SimplifyOpts a -> f a -> Fresh (f a)

-- | Simplify an expression within a theory
simplifyExprIn :: (TransformBiM (WriterT Any Fresh) (Expr a) (f a), Name a) => Maybe (Theory a) -> SimplifyOpts a -> f a -> Fresh (f a)
isConstructor :: Name a => Maybe (Scope a) -> Head a -> Bool
missingCase :: Name a => Maybe (Scope a) -> a -> [Case a] -> Maybe (Datatype a, Constructor a)
tryMatch :: Name a => Maybe (Scope a) -> Expr a -> [Case a] -> Maybe (Expr a)

module Tip.WorkerWrapper
data WorkerWrapper a
WorkerWrapper :: Function a -> [Local a] -> Type a -> (Expr a -> Expr a) -> (Head a -> [Expr a] -> Fresh (Expr a)) -> WorkerWrapper a

-- | The function to transform
[ww_func] :: WorkerWrapper a -> Function a

-- | New function argument type
[ww_args] :: WorkerWrapper a -> [Local a]

-- | New function result type
[ww_res] :: WorkerWrapper a -> Type a

-- | Transform function body
[ww_def] :: WorkerWrapper a -> Expr a -> Expr a

-- | Transform call to function
[ww_use] :: WorkerWrapper a -> Head a -> [Expr a] -> Fresh (Expr a)
workerWrapperTheory :: Name a => (Theory a -> Fresh [WorkerWrapper a]) -> Theory a -> Fresh (Theory a)
workerWrapperFunctions :: Name a => (Function a -> Maybe (Fresh (WorkerWrapper a))) -> Theory a -> Fresh (Theory a)
workerWrapper :: Name a => [WorkerWrapper a] -> Theory a -> Fresh (Theory a)

module Tip.Pass.Booleans

-- | Transforms boolean operators to if, but not in expression contexts.
theoryBoolOpToIf :: Ord a => Theory a -> Theory a
formulaBoolOpToIf :: Ord a => Expr a -> Expr a
hasBoolType :: Ord a => Expr a -> Bool

-- | Transforms <tt>and</tt>, <tt>or</tt>, <tt>=&gt;</tt>, <tt>not</tt> and
--   <tt>=</tt> and <tt>distinct</tt> on <tt>Bool</tt> into <tt>ite</tt>
--   (i.e. <tt>match</tt>)
boolOpToIf :: (Ord a, TransformBi (Expr a) (f a)) => f a -> f a

-- | Transforms <tt>ite</tt> (<tt>match</tt>) on boolean literals in the
--   branches into the corresponding builtin boolean function.
ifToBoolOp :: TransformBi (Expr a) (f a) => f a -> f a

-- | Names to replace the builtin boolean type with
data BoolNames a
BoolNames :: a -> a -> a -> a -> a -> BoolNames a
[boolName] :: BoolNames a -> a
[trueName] :: BoolNames a -> a
[falseName] :: BoolNames a -> a
[isTrueName] :: BoolNames a -> a
[isFalseName] :: BoolNames a -> a
freshBoolNames :: Name a => Fresh (BoolNames a)
boolGbl :: BoolNames a -> Bool -> Global a
boolExpr :: BoolNames a -> Bool -> Expr a
removeBuiltinBoolFrom :: (TransformBi (Type a) (f a), TransformBi (Pattern a) (f a), TransformBi (Head a) (f a)) => BoolNames a -> f a -> f a
removeBuiltinBoolWith :: Ord a => BoolNames a -> Theory a -> Theory a
removeBuiltinBool :: Name a => Theory a -> Fresh (Theory a)

module Tip.Pretty.Why3
data Why3Var a
Why3Var :: Bool -> a -> Why3Var a
why3VarTheory :: Ord a => Theory a -> Theory (Why3Var a)
block :: Doc -> Doc -> Doc
pcsv :: [Doc] -> Doc
csv :: [Doc] -> Doc
csv1 :: [Doc] -> Doc
separating :: ([Doc] -> Doc) -> [Doc] -> [Doc] -> Doc
escape :: Char -> String
ppTheory :: (Ord a, PrettyVar a) => Theory a -> Doc
ppSort :: (PrettyVar a, Ord a) => Sort a -> Doc
ppDatas :: (PrettyVar a, Ord a) => [Datatype a] -> Doc
ppData :: (PrettyVar a, Ord a) => Doc -> Datatype a -> Doc
ppCon :: (PrettyVar a, Ord a) => Constructor a -> Doc
ppQuant :: (PrettyVar a, Ord a) => Doc -> [Local a] -> Doc -> Doc
ppBinder :: (PrettyVar a, Ord a) => a -> Type a -> Doc
ppLocalBinder :: (PrettyVar a, Ord a) => Local a -> Doc
ppUninterp :: (PrettyVar a, Ord a) => Signature a -> Doc
ppFuncs :: (PrettyVar a, Ord a) => [Function a] -> Doc
ppFunc :: (PrettyVar a, Ord a) => Doc -> Function a -> Doc
ppDeepPattern :: PrettyVar a => DeepPattern a -> Doc
ppFormula :: (PrettyVar a, Ord a) => Formula a -> Int -> Doc
ppRole :: Role -> Doc
ppExpr :: (PrettyVar a, Ord a) => Int -> Expr a -> Doc
ppHead :: (PrettyVar a, Ord a) => Head a -> [Doc] -> Doc
ppBuiltin :: Builtin -> Doc
ppBinOp :: Builtin -> Maybe Doc
ppLit :: Lit -> Doc
ppQuantName :: Quant -> Doc
ppCase :: (PrettyVar a, Ord a) => Case a -> Doc
ppPat :: (PrettyVar a, Ord a) => Pattern a -> Doc
ppType :: (PrettyVar a, Ord a) => Int -> Type a -> Doc
ppTyVar :: (PrettyVar a, Ord a) => a -> Doc
why3Keywords :: [String]
instance GHC.Show.Show a => GHC.Show.Show (Tip.Pretty.Why3.Why3Var a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Pretty.Why3.Why3Var a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Pretty.Why3.Why3Var a)
instance Tip.Pretty.PrettyVar a => Tip.Pretty.PrettyVar (Tip.Pretty.Why3.Why3Var a)

module Tip.Pretty.Isabelle
($-$) :: Doc -> Doc -> Doc
block :: Doc -> Doc -> Doc
pcsv :: [Doc] -> Doc
csv :: [Doc] -> Doc
csv1 :: [Doc] -> Doc
separating :: ([Doc] -> Doc) -> [Doc] -> [Doc] -> Doc
escape :: Char -> String
intersperseWithPre :: (a -> a -> a) -> a -> [a] -> [a]
quote :: Doc -> Doc
quoteWhen :: (a -> Bool) -> a -> (Doc -> Doc)
ppAsTuple :: [a] -> (a -> Doc) -> Doc
ppTheory :: (Ord a, PrettyVar a) => Theory a -> Doc
ppSort :: (PrettyVar a, Ord a) => Sort a -> Doc
ppDatas :: (PrettyVar a, Ord a) => [Datatype a] -> Doc
ppData :: (PrettyVar a, Ord a) => Datatype a -> Doc
ppCon :: (PrettyVar a, Ord a) => Constructor a -> Doc
ppQuant :: (PrettyVar a, Ord a) => Doc -> [Local a] -> Doc -> Doc -> Doc
ppBinder :: (PrettyVar a, Ord a) => a -> Type a -> Doc
ppLocalBinder :: (PrettyVar a, Ord a) => Local a -> Doc
ppUninterp :: (PrettyVar a, Ord a) => Signature a -> Doc
ppFuncs :: (PrettyVar a, Ord a) => [Function a] -> Doc
ppFunc :: (PrettyVar a, Ord a) => Function a -> (Doc, [Doc])
ppDeepPattern :: PrettyVar a => DeepPattern a -> Doc
ppFormula :: (PrettyVar a, Ord a) => Formula a -> Int -> Doc
ppRole :: Role -> Doc
ppExpr :: (PrettyVar a, Ord a) => Int -> Expr a -> Doc
ppHead :: (PrettyVar a, Ord a) => Head a -> [Doc] -> Doc
ppBuiltin :: Builtin -> Doc
ppBinOp :: Builtin -> Maybe Doc
ppLit :: Lit -> Doc
ppQuantName :: Quant -> Doc
ppCase :: (PrettyVar a, Ord a) => Case a -> Doc
ppPat :: (PrettyVar a, Ord a) => Pattern a -> Doc
ppType :: (PrettyVar a, Ord a) => Int -> Type a -> Doc
ppTyVar :: (PrettyVar a, Ord a) => a -> Doc
isabelleKeywords :: [String]

module Tip.Pretty.TFF
apply :: Doc -> [Doc] -> Doc
clause :: String -> String -> Doc -> Doc
validTFFChar :: Char -> String
ppTheory :: (Ord a, PrettyVar a) => Theory a -> Doc
ppSort :: PrettyVar a => Sort a -> Doc
ppUninterp :: PrettyVar a => Signature a -> Doc
ppFormula :: (Ord a, PrettyVar a) => Formula a -> Doc
tffify :: Ord a => Expr a -> Expr a
tffvarify :: Ord a => Theory a -> Theory (Why3Var a)
ppExpr :: (Ord a, PrettyVar a) => Int -> Expr a -> Doc
ppLocal :: PrettyVar a => Local a -> Doc
ppQuant :: Quant -> Doc
ppHead :: PrettyVar a => Head a -> Doc
ppBuiltin :: Builtin -> Doc
ppLit :: Lit -> Doc
ppType :: PrettyVar a => Type a -> Doc
ppBuiltinType :: BuiltinType -> Doc

module Tip.Pretty.Waldmeister
validChar :: Char -> String
ppTheory :: (Ord a, PrettyVar a) => Theory a -> Doc
ppType :: (Ord a, PrettyVar a) => Type a -> Doc
ppSig :: (Ord a, PrettyVar a) => Signature a -> Doc
ppFormula :: (Ord a, PrettyVar a) => Formula a -> Doc
ppExpr :: (Ord a, PrettyVar a) => Expr a -> Doc
ppHead :: (Ord a, PrettyVar a) => Head a -> Doc
keywords :: [String]


-- | Parses the TIP format
module Tip.Parser

-- | Parse, and get either an error or the string's theory
parse :: String -> Either String (Theory Id)

-- | Parse from a file. If the string is empty or "-", then reads from
--   stdin.
parseFile :: String -> IO (Either String (Theory Id))

-- | Identifiers from parsed Tip syntax
data Id

-- | A source position of the identifier, if available
idPos :: Id -> Maybe (Int, Int)


-- | Passes
module Tip.Passes

-- | Continues making unique names after the highest numbered name in a
--   foldable value.
freshPass :: (Foldable f, Name a) => (f a -> Fresh b) -> f a -> b

-- | Simplify an entire theory
simplifyTheory :: Name a => SimplifyOpts a -> Theory a -> Fresh (Theory a)

-- | Gentle options: if there is risk for code duplication, only inline
--   atomic expressions
gently :: SimplifyOpts a

-- | Aggressive options: inline everything that might plausibly lead to
--   simplification
aggressively :: Name a => SimplifyOpts a

-- | Options for the simplifier
data SimplifyOpts a
SimplifyOpts :: Bool -> Bool -> (Occurrences -> Maybe (Scope a) -> Expr a -> Bool) -> Bool -> SimplifyOpts a

-- | Allow simplifications on lets
[touch_lets] :: SimplifyOpts a -> Bool

-- | transform <tt>(match x (case (K y) (e x y)))</tt> to <tt>(match x
--   (case (K y) (e (K y) y))</tt> This is useful for triggering other
--   known-case simplifications, and is therefore on by default.
[remove_variable_scrutinee_in_branches] :: SimplifyOpts a -> Bool

-- | Inlining predicate
[should_inline] :: SimplifyOpts a -> Occurrences -> Maybe (Scope a) -> Expr a -> Bool

-- | Allow function inlining to introduce match
[inline_match] :: SimplifyOpts a -> Bool

-- | Remove datatypes that have only one constructor with one field. Can
--   only be run after the <tt>addMatch</tt> pass.
removeNewtype :: Name a => Theory a -> Theory a

-- | Replace "fat arrow", <tt>=&gt;</tt>, functions with normal functions
--   wherever possible.
uncurryTheory :: Name a => Theory a -> Fresh (Theory a)

-- | Splits a theory with many goals into many theories each with one goal
splitConjecture :: Theory a -> [Theory a]

-- | Splits, type skolems and skolemises conjectures!
skolemiseConjecture :: Name a => Theory a -> Fresh [Theory a]

-- | Skolemises a conjecture, assuming that there is just one goal and that
--   it has no type variables.
skolemiseConjecture' :: Name a => Theory a -> Fresh (Theory a)
skolemise :: Expr a -> Writer ([Local a], [Expr a]) (Expr a)

-- | Negates the conjecture: changes assert-not into assert, and introduce
--   skolem types in case the goal is polymorphic. (runs
--   <a>typeSkolemConjecture</a>)
negateConjecture :: Name a => Theory a -> Fresh (Theory a)

-- | Introduce skolem types in case the goal is polymorphic.
typeSkolemConjecture :: Name a => Theory a -> Fresh (Theory a)

-- | Replaces the builtin Int to natural numbers, if the only operations
--   performed on are related to int ordering
intToNat :: Name a => Theory a -> Fresh (Theory a)

-- | Replaces abstract sorts with natural numbers
sortsToNat :: Name a => Theory a -> Fresh (Theory a)
makeConjecture :: Int -> Theory a -> Theory a
selectConjecture :: Int -> Theory a -> Theory a
provedConjecture :: Int -> Theory a -> Theory a
deleteConjecture :: Int -> Theory a -> Theory a

-- | Transforms <tt>ite</tt> (<tt>match</tt>) on boolean literals in the
--   branches into the corresponding builtin boolean function.
ifToBoolOp :: TransformBi (Expr a) (f a) => f a -> f a

-- | Transforms <tt>and</tt>, <tt>or</tt>, <tt>=&gt;</tt>, <tt>not</tt> and
--   <tt>=</tt> and <tt>distinct</tt> on <tt>Bool</tt> into <tt>ite</tt>
--   (i.e. <tt>match</tt>)
boolOpToIf :: (Ord a, TransformBi (Expr a) (f a)) => f a -> f a

-- | Transforms boolean operators to if, but not in expression contexts.
theoryBoolOpToIf :: Ord a => Theory a -> Theory a
removeBuiltinBool :: Name a => Theory a -> Fresh (Theory a)

-- | Lifts boolean operators to the top level
--   
--   replaces (and r s t) with f r s t and f x y z = and x y z
--   
--   Run CollapseEqual and BoolOpToIf afterwards
boolOpLift :: Name a => Theory a -> Fresh (Theory a)

-- | Replace SMTLIB-style selector and discriminator functions
--   (<tt>is-nil</tt>, <tt>head</tt>, <tt>tail</tt>) with case expressions.
addMatch :: Name a => Theory a -> Fresh (Theory a)

-- | Makes an effort to move match statements upwards: moves match above
--   function applications, and moves matches inside scrutinees outside.
--   
--   Does not move past quantifiers, lets, and lambdas.
commuteMatch :: (Name a, TransformBiM Fresh (Expr a) (f a)) => Maybe (Theory a) -> f a -> Fresh (f a)

-- | Turn case expressions into <tt>is-Cons</tt>, <tt>head</tt>,
--   <tt>tail</tt> etc.
removeMatch :: Name a => Theory a -> Fresh (Theory a)

-- | Look for expressions of the form <tt>(match x (case P ...P...)
--   ...)</tt> and replace them with <tt>(match x (case P ...x...)
--   ...)</tt>. This helps Why3's termination checker in some cases.
cseMatch :: Name a => CSEMatchOpts -> Theory a -> Theory a
cseMatchNormal :: CSEMatchOpts
cseMatchWhy3 :: CSEMatchOpts
fillInCases :: (Ord a, PrettyVar a) => (Type a -> Expr a) -> Theory a -> Theory a

-- | If we have
--   
--   <pre>
--   f x = E[x]
--   g y = E[y]
--   </pre>
--   
--   then we remove <tt>g</tt> and replace it with <tt>f</tt> everywhere
collapseEqual :: Ord a => Theory a -> Theory a

-- | If we have
--   
--   <pre>
--   g [a] x y = f [T1 a,T2 a] x y
--   </pre>
--   
--   then we remove <tt>g [t]</tt> and replace it with <tt>f [T1 t,T2
--   t]</tt> everywhere
removeAliases :: Ord a => Theory a -> Theory a

-- | Defunctionalization.
--   
--   <pre>
--   f x = ... \ y -&gt; e [ x ] ...
--   </pre>
--   
--   becomes
--   
--   <pre>
--   f x = ... g x ...
--   g x = \ y -&gt; e [ x ]
--   </pre>
--   
--   where <tt>g</tt> is a fresh function.
--   
--   After this pass, lambdas only exist at the top level of functions.
lambdaLift :: Name a => Theory a -> Fresh (Theory a)

-- | Lift lets to the top level.
--   
--   <pre>
--   let x = b[fvs] in e[x]
--   </pre>
--   
--   becomes
--   
--   <pre>
--   e[f fvs]
--   f fvs = b[fvs]
--   </pre>
letLift :: Name a => Theory a -> Fresh (Theory a)

-- | Axiomatize lambdas.
--   
--   <pre>
--   f x = \ y -&gt; E[x,y]
--   </pre>
--   
--   becomes
--   
--   <pre>
--   declare-fun f ...
--   assert (forall x y . @ (f x) y = E[x,y])
--   </pre>
axiomatizeLambdas :: Name a => Theory a -> Fresh (Theory a)

-- | Transforms define-fun to declare-fun in the most straightforward way.
--   All parts of the right hand side is preserved, including match and
--   if-then-else.
axiomatizeFuncdefs :: Theory a -> Theory a

-- | Makes function definitions into case by converting case to left hand
--   side pattern matching.
axiomatizeFuncdefs2 :: Name a => Theory a -> Theory a
axiomatizeDatadecls :: Name a => Bool -> Theory a -> Fresh (Theory a)
monomorphise :: Name a => Bool -> Theory a -> Fresh (Theory a)

-- | Applies induction at the given coordinates to the first goal
induction :: (Name a, Ord a) => [Int] -> Theory a -> Fresh [Theory a]
uniqLocals :: Name a => Theory a -> Fresh (Theory a)
dropSuffix :: (Traversable f, Name a) => String -> f a -> Fresh (f a)

-- | The passes in the standard Tip distribution
data StandardPass
SimplifyGently :: StandardPass
SimplifyAggressively :: StandardPass
RemoveNewtype :: StandardPass
UncurryTheory :: StandardPass
NegateConjecture :: StandardPass
TypeSkolemConjecture :: StandardPass
IntToNat :: StandardPass
SortsToNat :: StandardPass
SplitConjecture :: StandardPass
SkolemiseConjecture :: StandardPass
IfToBoolOp :: StandardPass
BoolOpToIf :: StandardPass
RemoveBuiltinBool :: StandardPass
BoolOpLift :: StandardPass
AddMatch :: StandardPass
CommuteMatch :: StandardPass
RemoveMatch :: StandardPass
CollapseEqual :: StandardPass
RemoveAliases :: StandardPass
LambdaLift :: StandardPass
LetLift :: StandardPass
AxiomatizeLambdas :: StandardPass
AxiomatizeFuncdefs :: StandardPass
AxiomatizeFuncdefs2 :: StandardPass
AxiomatizeDatadecls :: StandardPass
AxiomatizeDatadeclsUEQ :: StandardPass
Monomorphise :: Bool -> StandardPass
CSEMatch :: StandardPass
CSEMatchWhy3 :: StandardPass
EliminateDeadCode :: StandardPass
MakeConjecture :: Int -> StandardPass
SelectConjecture :: Int -> StandardPass
ProvedConjecture :: Int -> StandardPass
DeleteConjecture :: Int -> StandardPass
DropSuffix :: String -> StandardPass
UniqLocals :: StandardPass
Induction :: [Int] -> StandardPass
class Pass p
runPass :: (Pass p, Name a) => p -> Theory a -> Fresh [Theory a]
passName :: Pass p => p -> String
parsePass :: Pass p => Parser p
unitPass :: Pass p => p -> Mod FlagFields () -> Parser p
lintMany :: (Name a, Monad m) => String -> [Theory a] -> m [Theory a]
runPassLinted :: (Pass p, Name a) => p -> Theory a -> Fresh [Theory a]

-- | A sum type that supports <a>Enum</a> and <a>Bounded</a>
data Choice a b
First :: a -> Choice a b
Second :: b -> Choice a b

-- | <a>either</a> for <a>Choice</a>
choice :: (a -> c) -> (b -> c) -> Choice a b -> c
runPasses :: (Pass p, Name a) => [p] -> Theory a -> Fresh [Theory a]
continuePasses :: (Pass p, Name a) => [p] -> [Theory a] -> Fresh [Theory a]
parsePasses :: Pass p => Parser [p]
instance GHC.Read.Read Tip.Passes.StandardPass
instance GHC.Show.Show Tip.Passes.StandardPass
instance GHC.Classes.Ord Tip.Passes.StandardPass
instance GHC.Classes.Eq Tip.Passes.StandardPass
instance Tip.Pass.Pipeline.Pass Tip.Passes.StandardPass


-- | Calculate the call graph of a theory.
module Tip.CallGraph
type FS = Function :+: Signature
data Block a
Block :: [FS a] -> [FS a] -> Block a
[callers] :: Block a -> [FS a]
[callees] :: Block a -> [FS a]
flattenBlock :: Block a -> [FS a]
theoryStuff :: Theory a -> [FS a]
callGraph :: (PrettyVar a, Ord a) => Theory a -> [Block a]
data CallGraphOpts
CallGraphOpts :: Bool -> Bool -> CallGraphOpts
[exploreSingleFunctions] :: CallGraphOpts -> Bool
[exploreCalleesFirst] :: CallGraphOpts -> Bool
flatCallGraph :: (PrettyVar a, Ord a) => CallGraphOpts -> Theory a -> [[FS a]]
instance GHC.Base.Functor Tip.CallGraph.Block
instance GHC.Show.Show a => GHC.Show.Show (Tip.CallGraph.Block a)

module Tip.Haskell.Translate
prelude :: String -> HsId a
tipDSL :: String -> HsId a
quickCheck :: String -> HsId a
quickCheckUnsafe :: String -> HsId a
quickCheckAll :: String -> HsId a
quickSpec :: String -> HsId a
sysEnv :: String -> HsId a
smtenSym :: String -> HsId a
smtenEnv :: String -> HsId a
smtenMinisat :: String -> HsId a
smtenMonad :: String -> HsId a
feat :: String -> HsId a
lsc :: String -> HsId a
typeable :: String -> HsId a
data HsId a

-- | A qualified import
Qualified :: String -> Maybe String -> String -> HsId a
[qual_module] :: HsId a -> String
[qual_module_short] :: HsId a -> Maybe String
[qual_func] :: HsId a -> String

-- | The current module defines something with this very important name
Exact :: String -> HsId a

-- | From the theory
Other :: a -> HsId a

-- | For various purposes...
Derived :: (HsId a) -> String -> HsId a
addHeader :: String -> Decls a -> Decls a
addImports :: Ord a => Decls (HsId a) -> Decls (HsId a)
trTheory :: (Ord a, PrettyVar a) => Mode -> Theory a -> Decls (HsId a)
data Kind
Expr :: Kind
Formula :: Kind
theorySigs :: Theory (HsId a) -> [HsId a]
ufInfo :: Theory (HsId a) -> (Bool, [Type (HsId a)])
data Mode
Feat :: Mode
QuickCheck :: Mode
LazySmallCheck :: Bool -> Mode
Smten :: Mode
QuickSpec :: Mode
Plain :: Mode
isLazySmallCheck :: Mode -> Bool
isSmten :: Mode -> Bool
trTheory' :: (a ~ HsId b, Ord b, PrettyVar b) => Mode -> Theory a -> Decls a
arbitrary :: [Type (HsId a)] -> [Type (HsId a)]
trType :: (a ~ HsId b) => Type a -> Type a
trBuiltinType :: BuiltinType -> Type (HsId a)
withBool :: (a ~ HsId b) => (a -> [c] -> d) -> Bool -> d
hsBuiltinTys :: [(BuiltinType, String)]
hsBuiltins :: [(Builtin, String)]
typeOfBuiltin :: Builtin -> Type a
makeSig :: (PrettyVar a, Ord a) => Theory (HsId a) -> Decl (HsId a)
theoryBuiltins :: Ord a => Theory a -> [Builtin]
instance GHC.Show.Show Tip.Haskell.Translate.Mode
instance GHC.Classes.Ord Tip.Haskell.Translate.Mode
instance GHC.Classes.Eq Tip.Haskell.Translate.Mode
instance GHC.Classes.Eq Tip.Haskell.Translate.Kind
instance Data.Foldable.Foldable Tip.Haskell.Translate.HsId
instance Data.Traversable.Traversable Tip.Haskell.Translate.HsId
instance GHC.Base.Functor Tip.Haskell.Translate.HsId
instance GHC.Show.Show a => GHC.Show.Show (Tip.Haskell.Translate.HsId a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Tip.Haskell.Translate.HsId a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Tip.Haskell.Translate.HsId a)
instance Tip.Pretty.PrettyVar a => Tip.Pretty.PrettyVar (Tip.Haskell.Translate.HsId a)

module Tip.Haskell.Rename
renameDecls :: (Ord a, PrettyVar a) => Decls (HsId a) -> (Decls (HsId String), RenameMap a)
isOperator :: String -> Bool
type RenameMap a = Map (HsId a) (HsId String)

module Tip.Pretty.Haskell
ppTheory :: Name a => Mode -> Theory a -> Doc
ppTheoryWithRenamings :: Name a => String -> Mode -> Theory a -> (Doc, RenameMap a)

-- | In instance declarations, you cannot write qualified variables, but
--   need to write them unqualified. As an example, the mempty part here is
--   incorrect:
--   
--   <pre>
--   instance Data.Monoid.Monoid T where
--     Data.Monoid.mempty = K
--   </pre>
--   
--   Thus, instance function declarations will be pretty printed with
--   ppUnqual.
class PrettyVar a => PrettyHsVar a
varUnqual :: PrettyHsVar a => a -> String
ppUnqual :: PrettyHsVar a => a -> Doc
ppHsVar :: PrettyHsVar a => a -> Doc
ppOperQ :: PrettyHsVar a => Bool -> a -> [Doc] -> Doc
ppOper :: PrettyHsVar a => a -> [Doc] -> Doc
isOp :: PrettyHsVar a => a -> Bool
tuple :: [Doc] -> Doc
csv :: [Doc] -> Doc
ppPat :: PrettyHsVar a => Int -> Pat a -> Doc
ppType :: PrettyHsVar a => Bool -> Int -> Type a -> Doc
type RenameMap a = Map (HsId a) (HsId String)
data Mode
Feat :: Mode
QuickCheck :: Mode
LazySmallCheck :: Bool -> Mode
Smten :: Mode
QuickSpec :: Mode
Plain :: Mode
instance Tip.Pretty.PrettyVar a => Tip.Pretty.Haskell.PrettyHsVar (Tip.Haskell.Translate.HsId a)
instance Tip.Pretty.Haskell.PrettyHsVar a => Tip.Pretty.Pretty (Tip.Haskell.Repr.Expr a)
instance Tip.Pretty.Haskell.PrettyHsVar a => Tip.Pretty.Pretty (Tip.Haskell.Repr.Stmt a)
instance Tip.Pretty.Haskell.PrettyHsVar a => Tip.Pretty.Pretty (Tip.Haskell.Repr.Pat a)
instance Tip.Pretty.Haskell.PrettyHsVar a => Tip.Pretty.Pretty (Tip.Haskell.Repr.Decl a)
instance Tip.Pretty.Haskell.PrettyHsVar a => Tip.Pretty.Pretty (Tip.Haskell.Repr.Decls a)
instance Tip.Pretty.Haskell.PrettyHsVar a => Tip.Pretty.Pretty (Tip.Haskell.Repr.Type a)