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


-- | tons of inductive problems - support library and tools
--   
@package tip-lib
@version 0.1.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
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 Eq a => Eq (Type a)
instance Ord a => Ord (Type a)
instance Show a => Show (Type a)
instance Functor Type
instance Traversable Type
instance Foldable Type
instance Eq a => Eq (Pat a)
instance Ord a => Ord (Pat a)
instance Show a => Show (Pat a)
instance Functor Pat
instance Traversable Pat
instance Foldable Pat
instance Eq a => Eq (Stmt a)
instance Ord a => Ord (Stmt a)
instance Show a => Show (Stmt a)
instance Functor Stmt
instance Traversable Stmt
instance Foldable Stmt
instance Eq a => Eq (Expr a)
instance Ord a => Ord (Expr a)
instance Show a => Show (Expr a)
instance Functor Expr
instance Traversable Expr
instance Foldable Expr
instance Eq a => Eq (Decl a)
instance Ord a => Ord (Decl a)
instance Show a => Show (Decl a)
instance Functor Decl
instance Traversable Decl
instance Foldable Decl
instance Eq a => Eq (Decls a)
instance Ord a => Ord (Decls a)
instance Show a => Show (Decls a)
instance Functor Decls
instance Traversable Decls
instance Foldable Decls

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 (Monoid w, Monad m) => Monad (WriterT w m)
instance (Monoid w, Monad m) => Applicative (WriterT w m)
instance (Monoid w, Monad m) => Functor (WriterT w m)


-- | Handy utilities
module Tip.Utils

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

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

-- | 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.
--   
--   Useful to find the highest unique in a structure
maximumOn :: (Foldable f, Ord b) => (a -> b) -> f a -> b


-- | 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
(:@:) :: 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
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
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 -> Int -> Sort a
sort_name :: Sort a -> a
sort_arity :: Sort a -> Int

-- | 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
con_name :: Constructor a -> a
con_discrim :: Constructor a -> 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 -> [a] -> Expr a -> Formula a
fm_role :: Formula a -> Role

-- | top-level quantified type variables
fm_tvs :: Formula a -> [a]
fm_body :: Formula a -> Expr a
data Role
Assert :: Role
Prove :: Role
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
instance Monad m => TransformBiM m (Function a) (Theory a)
instance Monad m => TransformBiM m (Type a) (Type a)
instance Monad m => TransformBiM m (Expr a) (Formula a)
instance Monad m => TransformBiM m (Expr a) (Theory a)
instance Monad m => TransformBiM m (Local a) (Expr a)
instance Monad m => TransformBiM m (Pattern a) (Expr a)
instance Monad m => TransformBiM m (Expr a) (Function a)
instance Monad m => TransformBiM m (Expr a) (Expr a)
instance TransformBi (Type a0) (Type a0)
instance TransformBi (Type a0) (Expr a0)
instance TransformBi (Type a0) (Theory a0)
instance TransformBi (Pattern a0) (Theory a0)
instance TransformBi (Pattern a0) (Expr a0)
instance TransformBi (Local a0) (Expr a0)
instance TransformBi (Head a0) (Theory a0)
instance TransformBi (Head a0) (Expr a0)
instance TransformBi (Expr a0) (Theory a0)
instance TransformBi (Expr a0) (Function a0)
instance TransformBi a0 (Formula a0)
instance TransformBi a0 (Expr a0)
instance TransformBi (Expr a0) (Expr a0)
instance UniverseBi (Theory a0) Builtin
instance UniverseBi (Theory a0) (Global a0)
instance UniverseBi (Theory a0) (Constructor a0)
instance UniverseBi (Type a0) (Type a0)
instance UniverseBi (Theory a0) (Type a0)
instance UniverseBi (Theory a0) (Expr a0)
instance UniverseBi (Expr a0) (Global a0)
instance UniverseBi (Expr a0) (Local a0)
instance UniverseBi (Expr a0) (Pattern a0)
instance UniverseBi (Datatype a0) (Type a0)
instance UniverseBi (Function a0) (Type a0)
instance UniverseBi (Function a0) (Global a0)
instance UniverseBi (Function a0) (Expr a0)
instance UniverseBi (Expr a0) (Expr a0)
instance Eq Quant
instance Ord Quant
instance Show Quant
instance Eq QuantInfo
instance Ord QuantInfo
instance Show QuantInfo
instance Eq Lit
instance Ord Lit
instance Show Lit
instance Eq Builtin
instance Ord Builtin
instance Show Builtin
instance Eq BuiltinType
instance Ord BuiltinType
instance Show BuiltinType
instance Eq a => Eq (Type a)
instance Ord a => Ord (Type a)
instance Show a => Show (Type a)
instance Functor Type
instance Foldable Type
instance Traversable Type
instance Eq a => Eq (PolyType a)
instance Ord a => Ord (PolyType a)
instance Show a => Show (PolyType a)
instance Functor PolyType
instance Foldable PolyType
instance Traversable PolyType
instance Eq a => Eq (Global a)
instance Ord a => Ord (Global a)
instance Show a => Show (Global a)
instance Functor Global
instance Foldable Global
instance Traversable Global
instance Eq a => Eq (Head a)
instance Ord a => Ord (Head a)
instance Show a => Show (Head a)
instance Functor Head
instance Foldable Head
instance Traversable Head
instance Eq a => Eq (Local a)
instance Ord a => Ord (Local a)
instance Show a => Show (Local a)
instance Functor Local
instance Foldable Local
instance Traversable Local
instance Eq a => Eq (Pattern a)
instance Ord a => Ord (Pattern a)
instance Show a => Show (Pattern a)
instance Functor Pattern
instance Foldable Pattern
instance Traversable Pattern
instance Eq a => Eq (Expr a)
instance Ord a => Ord (Expr a)
instance Show a => Show (Expr a)
instance Functor Expr
instance Foldable Expr
instance Traversable Expr
instance Eq a => Eq (Case a)
instance Ord a => Ord (Case a)
instance Show a => Show (Case a)
instance Functor Case
instance Foldable Case
instance Traversable Case
instance Eq a => Eq (Function a)
instance Ord a => Ord (Function a)
instance Show a => Show (Function a)
instance Functor Function
instance Foldable Function
instance Traversable Function
instance Eq a => Eq (Signature a)
instance Ord a => Ord (Signature a)
instance Show a => Show (Signature a)
instance Functor Signature
instance Foldable Signature
instance Traversable Signature
instance Eq a => Eq (Sort a)
instance Ord a => Ord (Sort a)
instance Show a => Show (Sort a)
instance Functor Sort
instance Foldable Sort
instance Traversable Sort
instance Eq a => Eq (Constructor a)
instance Ord a => Ord (Constructor a)
instance Show a => Show (Constructor a)
instance Functor Constructor
instance Foldable Constructor
instance Traversable Constructor
instance Eq a => Eq (Datatype a)
instance Ord a => Ord (Datatype a)
instance Show a => Show (Datatype a)
instance Functor Datatype
instance Foldable Datatype
instance Traversable Datatype
instance Eq Role
instance Ord Role
instance Show Role
instance Eq a => Eq (Formula a)
instance Ord a => Ord (Formula a)
instance Show a => Show (Formula a)
instance Functor Formula
instance Foldable Formula
instance Traversable Formula
instance Eq a => Eq (Theory a)
instance Ord a => Ord (Theory a)
instance Show a => Show (Theory a)
instance Functor Theory
instance Foldable Theory
instance Traversable Theory
instance Monoid (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
varStr :: PrettyVar a => a -> String

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

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

-- | Conditional parentheses
parIf :: Bool -> Doc -> Doc
instance PrettyVar Int
instance PrettyVar String


-- | 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)
fresh :: Name a => Fresh a
refresh :: Name a => a -> Fresh a
freshNamed :: Name a => String -> Fresh a
refreshNamed :: Name a => String -> a -> Fresh a
getUnique :: Name a => a -> Int
instance Monad Fresh
instance Applicative Fresh
instance Functor Fresh
instance MonadFix Fresh
instance Name Int


-- | General functions for constructing and examining Tip syntax.
module Tip.Core
(===) :: Expr a -> Expr a -> Expr a
(=/=) :: Expr a -> 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
applyType :: Ord a => [a] -> [Type a] -> Type a -> Type a
applyPolyType :: Ord a => PolyType a -> [Type a] -> ([Type a], Type a)
litView :: Expr a -> Maybe Lit
boolView :: Expr a -> Maybe Bool

-- | 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]
locals :: Ord a => Expr a -> [Local a]
free :: 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
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
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 (Eq (f a), Eq (g a)) => Eq ((:+:) f g a)
instance (Ord (f a), Ord (g a)) => Ord ((:+:) f g a)
instance (Show (f a), Show (g a)) => Show ((:+:) f g a)
instance (Functor f, Functor g) => Functor (f :+: g)
instance Definition Datatype
instance Definition Function
instance Definition Signature
instance (Definition f, Definition g) => Definition (f :+: g)


-- | 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 :: Int -> 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
isGlobal :: Ord a => a -> Scope a -> Bool
isLocal :: Ord a => a -> Scope a -> Bool
isSort :: Ord a => a -> Scope a -> Bool
isTyVar :: 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 Eq a => Eq (TypeInfo a)
instance Show a => Show (TypeInfo a)
instance Show a => Show (GlobalInfo a)
instance Show a => Show (Scope a)
instance Functor m => Functor (ScopeT a m)
instance (Monad m, Functor m) => Applicative (ScopeT a m)
instance Monad m => Monad (ScopeT a m)
instance Monad m => MonadPlus (ScopeT a m)
instance (Monad m, Functor m) => Alternative (ScopeT a m)
instance Monad m => MonadState (Scope a) (ScopeT a m)
instance Monad m => MonadError Doc (ScopeT a m)
instance Error Doc
instance MonadTrans (ScopeT a)

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 Eq RenamedId
instance Ord RenamedId
instance Show RenamedId
instance Eq a => Eq (TwoStage a)
instance Ord a => Ord (TwoStage a)
instance PrettyVar a => Show (TwoStage a)
instance PrettyVar RenamedId

module Tip.Pretty.SMT
expr :: Doc -> [Doc] -> Doc
parExprSep :: Doc -> [Doc] -> Doc
parExpr :: 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
ppUninterp :: PrettyVar a => Signature a -> Doc
ppFuncs :: (Ord a, PrettyVar a) => [Function a] -> Doc
ppFuncSig :: PrettyVar a => Function a -> 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
ppPolyType :: PrettyVar a => PolyType a -> Doc
smtKeywords :: [String]
instance PrettyVar a => Pretty (Pattern a)
instance PrettyVar a => Pretty (Head a)
instance PrettyVar a => Pretty (Global a)
instance PrettyVar a => Pretty (Local a)
instance PrettyVar a => Pretty (Signature a)
instance PrettyVar a => Pretty (Datatype a)
instance (Ord a, PrettyVar a) => Pretty (Formula a)
instance (Ord a, PrettyVar a) => Pretty (Function a)
instance PrettyVar a => Pretty (Type a)
instance PrettyVar a => Pretty (PolyType a)
instance (Ord a, PrettyVar a) => Pretty (Expr a)
instance (Ord a, PrettyVar a) => Pretty (Theory 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
instance Eq ExprKind

module Tip.Simplify

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

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

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

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

-- | 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

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)


-- | 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 -> (Maybe (Scope a) -> Expr a -> Bool) -> Bool -> SimplifyOpts a

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

-- | Inlining predicate
should_inline :: SimplifyOpts a -> 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)

-- | Negates the conjecture: changes assert-not into assert, and introduce
--   skolem types in case the goal is polymorphic.
negateConjecture :: Name a => Theory a -> Fresh (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>distict</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

-- | 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)) => 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 x y = f x y
--   </pre>
--   
--   then we remove <tt>g</tt> and replace it with <tt>f</tt> everywhere
removeAliases :: Eq 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)

-- | The passes in the standard Tip distribution
data StandardPass
SimplifyGently :: StandardPass
SimplifyAggressively :: StandardPass
RemoveNewtype :: StandardPass
UncurryTheory :: StandardPass
NegateConjecture :: StandardPass
IfToBoolOp :: StandardPass
BoolOpToIf :: StandardPass
AddMatch :: StandardPass
CommuteMatch :: StandardPass
RemoveMatch :: StandardPass
CollapseEqual :: StandardPass
RemoveAliases :: StandardPass
LambdaLift :: StandardPass
LetLift :: StandardPass
AxiomatizeLambdas :: StandardPass
CSEMatch :: StandardPass
CSEMatchWhy3 :: StandardPass
EliminateDeadCode :: 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
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)
parsePasses :: Pass p => Parser [p]
instance Eq StandardPass
instance Ord StandardPass
instance Show StandardPass
instance Read StandardPass
instance Enum StandardPass
instance Bounded StandardPass
instance Pass StandardPass

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
csv1 :: [Doc] -> Doc
csv :: [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 Eq a => Eq (Why3Var a)
instance Ord a => Ord (Why3Var a)
instance Show a => Show (Why3Var a)
instance PrettyVar a => PrettyVar (Why3Var a)

module Tip.Pretty.Isabelle
($-$) :: Doc -> Doc -> Doc
block :: Doc -> Doc -> Doc
pcsv :: [Doc] -> Doc
csv1 :: [Doc] -> Doc
csv :: [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]


-- | Parses the TIP format
module Tip.Parser

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

-- | Identifiers from parsed Tip syntax
data Id

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


-- | 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 Show a => Show (Block a)
instance Functor Block

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
feat :: 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 :: Decls a -> Decls a
addImports :: Ord a => Decls (HsId a) -> Decls (HsId a)
trTheory :: (Ord a, PrettyVar a) => 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)])
trTheory' :: (a ~ HsId b, Ord b, PrettyVar b) => 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 Eq a => Eq (HsId a)
instance Ord a => Ord (HsId a)
instance Show a => Show (HsId a)
instance Functor HsId
instance Traversable HsId
instance Foldable HsId
instance Eq Kind
instance PrettyVar a => PrettyVar (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 => Theory a -> Doc
ppTheoryWithRenamings :: Name a => 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)
instance PrettyHsVar a => Pretty (Type a)
instance PrettyHsVar a => Pretty (Decls a)
instance PrettyHsVar a => Pretty (Decl a)
instance PrettyHsVar a => Pretty (Pat a)
instance PrettyHsVar a => Pretty (Stmt a)
instance PrettyHsVar a => Pretty (Expr a)
instance PrettyVar a => PrettyHsVar (HsId a)