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


-- | Liquid Types for Haskell
--   
@package liquidhaskell
@version 0.5.0.0

module Language.Haskell.Liquid.Desugar.DsForeign
dsForeigns :: [LForeignDecl Id] -> DsM (ForeignStubs, OrdList Binding)
dsForeigns' :: [LForeignDecl Id] -> DsM (ForeignStubs, OrdList Binding)
dsFImport :: Id -> Coercion -> ForeignImport -> DsM ([Binding], SDoc, SDoc)
dsCImport :: Id -> Coercion -> CImportSpec -> CCallConv -> Safety -> Maybe Header -> DsM ([Binding], SDoc, SDoc)
dsFCall :: Id -> Coercion -> ForeignCall -> Maybe Header -> DsM ([(Id, Expr TyVar)], SDoc, SDoc)
dsPrimCall :: Id -> Coercion -> ForeignCall -> DsM ([(Id, Expr TyVar)], SDoc, SDoc)
dsFExport :: Id -> Coercion -> CLabelString -> CCallConv -> Bool -> DsM (SDoc, SDoc, String, Int)
dsFExportDynamic :: Id -> Coercion -> CCallConv -> DsM ([Binding], SDoc, SDoc)
mkFExportCBits :: DynFlags -> FastString -> Maybe Id -> [Type] -> Type -> Bool -> CCallConv -> (SDoc, SDoc, String, Int)
toCType :: Type -> (Maybe Header, SDoc)
foreignExportInitialiser :: Id -> SDoc

module Language.Haskell.Liquid.Desugar.Coverage
addTicksToBinds :: DynFlags -> Module -> ModLocation -> NameSet -> [TyCon] -> LHsBinds Id -> IO (LHsBinds Id, HpcInfo, ModBreaks)
hpcInitCode :: Module -> HpcInfo -> SDoc
instance Eq TickDensity
instance Monad TM
instance Applicative TM
instance Functor TM


-- | Utility functions for constructing Core syntax, principally for
--   desugaring
module Language.Haskell.Liquid.Desugar.DsUtils
data EquationInfo :: *
EqnInfo :: [Pat Id] -> MatchResult -> EquationInfo
eqn_pats :: EquationInfo -> [Pat Id]
eqn_rhs :: EquationInfo -> MatchResult
firstPat :: EquationInfo -> Pat Id
shiftEqns :: [EquationInfo] -> [EquationInfo]
data MatchResult :: *
MatchResult :: CanItFail -> (CoreExpr -> DsM CoreExpr) -> MatchResult
data CanItFail :: *
CanFail :: CanItFail
CantFail :: CanItFail
data CaseAlt a
MkCaseAlt :: a -> [CoreBndr] -> HsWrapper -> MatchResult -> CaseAlt a
alt_pat :: CaseAlt a -> a
alt_bndrs :: CaseAlt a -> [CoreBndr]
alt_wrapper :: CaseAlt a -> HsWrapper
alt_result :: CaseAlt a -> MatchResult
cantFailMatchResult :: CoreExpr -> MatchResult
alwaysFailMatchResult :: MatchResult
extractMatchResult :: MatchResult -> CoreExpr -> DsM CoreExpr
combineMatchResults :: MatchResult -> MatchResult -> MatchResult
adjustMatchResult :: DsWrapper -> MatchResult -> MatchResult
adjustMatchResultDs :: (CoreExpr -> DsM CoreExpr) -> MatchResult -> MatchResult
mkCoLetMatchResult :: CoreBind -> MatchResult -> MatchResult
mkViewMatchResult :: Id -> CoreExpr -> Id -> MatchResult -> MatchResult
mkGuardedMatchResult :: CoreExpr -> MatchResult -> MatchResult
matchCanFail :: MatchResult -> Bool
mkEvalMatchResult :: Id -> Type -> MatchResult -> MatchResult
mkCoPrimCaseMatchResult :: Id -> Type -> [(Literal, MatchResult)] -> MatchResult
mkCoAlgCaseMatchResult :: DynFlags -> Id -> Type -> [CaseAlt DataCon] -> MatchResult
mkCoSynCaseMatchResult :: Id -> Type -> CaseAlt PatSyn -> MatchResult
wrapBind :: Var -> Var -> CoreExpr -> CoreExpr
wrapBinds :: [(Var, Var)] -> CoreExpr -> CoreExpr
mkErrorAppDs :: Id -> Type -> SDoc -> DsM CoreExpr
mkCoreAppDs :: CoreExpr -> CoreExpr -> CoreExpr
mkCoreAppsDs :: CoreExpr -> [CoreExpr] -> CoreExpr
seqVar :: Var -> CoreExpr -> CoreExpr
mkLHsVarPatTup :: [Id] -> LPat Id
mkLHsPatTup :: [LPat Id] -> LPat Id
mkVanillaTuplePat :: [OutPat Id] -> Boxity -> Pat Id
mkBigLHsVarTup :: [Id] -> LHsExpr Id
mkBigLHsTup :: [LHsExpr Id] -> LHsExpr Id
mkBigLHsVarPatTup :: [Id] -> LPat Id
mkBigLHsPatTup :: [LPat Id] -> LPat Id
mkSelectorBinds :: [Maybe (Tickish Id)] -> LPat Id -> CoreExpr -> DsM [(Id, CoreExpr)]
selectSimpleMatchVarL :: LPat Id -> DsM Id
selectMatchVars :: [Pat Id] -> DsM [Id]
selectMatchVar :: Pat Id -> DsM Id
mkOptTickBox :: Maybe (Tickish Id) -> CoreExpr -> CoreExpr
mkBinaryTickBox :: Int -> Int -> CoreExpr -> DsM CoreExpr

module Language.Haskell.Liquid.Desugar.MatchLit
dsLit :: HsLit -> DsM CoreExpr
dsOverLit :: HsOverLit Id -> DsM CoreExpr
hsLitKey :: DynFlags -> HsLit -> Literal
hsOverLitKey :: OutputableBndr a => HsOverLit a -> Bool -> Literal
tidyLitPat :: HsLit -> Pat Id
tidyNPat :: (HsLit -> Pat Id) -> HsOverLit Id -> Maybe (SyntaxExpr Id) -> SyntaxExpr Id -> Pat Id
matchLiterals :: [Id] -> Type -> [[EquationInfo]] -> DsM MatchResult
matchNPlusKPats :: [Id] -> Type -> [EquationInfo] -> DsM MatchResult
matchNPats :: [Id] -> Type -> [EquationInfo] -> DsM MatchResult
warnAboutIdentities :: DynFlags -> CoreExpr -> Type -> DsM ()
warnAboutEmptyEnumerations :: DynFlags -> LHsExpr Id -> Maybe (LHsExpr Id) -> LHsExpr Id -> DsM ()

module Language.Haskell.Liquid.Desugar.DsGRHSs
dsGuarded :: GRHSs Id (LHsExpr Id) -> Type -> DsM CoreExpr
dsGRHSs :: HsMatchContext Name -> [Pat Id] -> GRHSs Id (LHsExpr Id) -> Type -> DsM MatchResult
dsGRHS :: HsMatchContext Name -> Type -> LGRHS Id (LHsExpr Id) -> DsM MatchResult

module Language.Haskell.Liquid.Desugar.DsBinds
dsTopLHsBinds :: LHsBinds Id -> DsM (OrdList (Id, CoreExpr))
dsLHsBinds :: LHsBinds Id -> DsM [(Id, CoreExpr)]
decomposeRuleLhs :: [Var] -> CoreExpr -> Either SDoc ([Var], Id, [CoreExpr])
dsSpec :: Maybe CoreExpr -> Located TcSpecPrag -> DsM (Maybe (OrdList (Id, CoreExpr), CoreRule))
dsHsWrapper :: HsWrapper -> CoreExpr -> DsM CoreExpr
dsTcEvBinds :: TcEvBinds -> DsM [CoreBind]
dsEvBinds :: Bag EvBind -> DsM [CoreBind]

module Language.Haskell.Liquid.Desugar.MatchCon
matchConFamily :: [Id] -> Type -> [[EquationInfo]] -> DsM MatchResult
matchPatSyn :: [Id] -> Type -> [EquationInfo] -> DsM MatchResult

module Language.Haskell.Liquid.Desugar.Match
match :: [Id] -> Type -> [EquationInfo] -> DsM MatchResult
matchEquations :: HsMatchContext Name -> [Id] -> [EquationInfo] -> Type -> DsM CoreExpr
matchWrapper :: HsMatchContext Name -> MatchGroup Id (LHsExpr Id) -> DsM ([Id], CoreExpr)
matchSimply :: CoreExpr -> HsMatchContext Name -> LPat Id -> CoreExpr -> CoreExpr -> DsM CoreExpr
matchSinglePat :: CoreExpr -> HsMatchContext Name -> LPat Id -> Type -> MatchResult -> DsM MatchResult

module Language.Haskell.Liquid.Desugar.DsArrows
dsProcExpr :: LPat Id -> LHsCmdTop Id -> DsM CoreExpr

module Language.Haskell.Liquid.Desugar.DsListComp
dsListComp :: [ExprLStmt Id] -> Type -> DsM CoreExpr
dsPArrComp :: [ExprStmt Id] -> DsM CoreExpr
dsMonadComp :: [ExprLStmt Id] -> DsM CoreExpr

module Language.Haskell.Liquid.Desugar.DsExpr
dsExpr :: HsExpr Id -> DsM CoreExpr
dsLExpr :: LHsExpr Id -> DsM CoreExpr
dsLocalBinds :: HsLocalBinds Id -> CoreExpr -> DsM CoreExpr
dsValBinds :: HsValBinds Id -> CoreExpr -> DsM CoreExpr
dsLit :: HsLit -> DsM CoreExpr

module Language.Haskell.Liquid.Desugar.Desugar

-- | Main entry point to the desugarer.
deSugarWithLoc :: HscEnv -> ModLocation -> TcGblEnv -> IO (Messages, Maybe ModGuts)

-- | Main entry point to the desugarer.
deSugar :: HscEnv -> ModLocation -> TcGblEnv -> IO (Messages, Maybe ModGuts)
deSugarExpr :: HscEnv -> LHsExpr Id -> IO (Messages, Maybe CoreExpr)

module Language.Haskell.Liquid.Desugar.DsMeta
dsBracket :: HsBracket Name -> [PendingTcSplice] -> DsM CoreExpr
templateHaskellNames :: [Name]
qTyConName :: Name
nameTyConName :: Name
liftName :: Name
liftStringName :: Name
expQTyConName :: Name
patQTyConName :: Name
decQTyConName :: Name
decsQTyConName :: Name
typeQTyConName :: Name
decTyConName :: Name
typeTyConName :: Name
mkNameG_dName :: Name
mkNameG_vName :: Name
mkNameG_tcName :: Name
quoteExpName :: Name
quotePatName :: Name
quoteDecName :: Name
quoteTypeName :: Name
tExpTyConName :: Name
tExpDataConName :: Name
unTypeName :: Name
unTypeQName :: Name
unsafeTExpCoerceName :: Name

module Language.Haskell.Liquid.Desugar.Check
check :: [EquationInfo] -> ([ExhaustivePat], [EquationInfo])
type ExhaustivePat = ([WarningPat], [(Name, [HsLit])])

module Paths_liquidhaskell
version :: Version
getBinDir :: IO FilePath
getLibDir :: IO FilePath
getDataDir :: IO FilePath
getLibexecDir :: IO FilePath
getDataFileName :: FilePath -> IO FilePath
getSysconfDir :: IO FilePath


-- | Main API for compiling plain Haskell source code.
--   
--   This module implements compilation of a Haskell source. It is
--   <i>not</i> concerned with preprocessing of source files; this is
--   handled in <a>DriverPipeline</a>.
--   
--   There are various entry points depending on what mode we're in:
--   "batch" mode (<tt>--make</tt>), "one-shot" mode (<tt>-c</tt>,
--   <tt>-S</tt> etc.), and "interactive" mode (GHCi). There are also entry
--   points for individual passes: parsing, typechecking/renaming,
--   desugaring, and simplification.
--   
--   All the functions here take an <a>HscEnv</a> as a parameter, but none
--   of them return a new one: <a>HscEnv</a> is treated as an immutable
--   value from here on in (although it has mutable components, for the
--   caches).
--   
--   Warning messages are dealt with consistently throughout this API:
--   during compilation warnings are collected, and before any function in
--   <tt>HscMain</tt> returns, the warnings are either printed, or turned
--   into a real compialtion error if the <tt>-Werror</tt> flag is enabled.
--   
--   (c) The GRASP/AQUA Project, Glasgow University, 1993-2000
module Language.Haskell.Liquid.Desugar.HscMain

-- | Convert a typechecked module to Core
hscDesugarWithLoc :: HscEnv -> ModSummary -> TcGblEnv -> IO ModGuts

module Language.Haskell.Liquid.Variance
data Variance
Invariant :: Variance
Bivariant :: Variance
Contravariant :: Variance
Covariant :: Variance
type VarianceInfo = [Variance]
instance Typeable Variance
instance Data Variance
instance Show Variance

module Language.Haskell.Liquid.Names
lenLocSymbol :: Located Symbol


-- | This module contains a wrappers and utility functions for accessing
--   GHC module information. It should NEVER depend on ANY module inside
--   the Language.Haskell.Liquid.* tree.
module Language.Haskell.Liquid.GhcMisc
data MGIModGuts
MI :: !CoreProgram -> !Module -> !Dependencies -> !ImportedMods -> !GlobalRdrEnv -> ![TyCon] -> ![FamInst] -> !NameSet -> !(Maybe [ClsInst]) -> MGIModGuts
mgi_binds :: MGIModGuts -> !CoreProgram
mgi_module :: MGIModGuts -> !Module
mgi_deps :: MGIModGuts -> !Dependencies
mgi_dir_imps :: MGIModGuts -> !ImportedMods
mgi_rdr_env :: MGIModGuts -> !GlobalRdrEnv
mgi_tcs :: MGIModGuts -> ![TyCon]
mgi_fam_insts :: MGIModGuts -> ![FamInst]
mgi_exports :: MGIModGuts -> !NameSet
mgi_cls_inst :: MGIModGuts -> !(Maybe [ClsInst])
miModGuts :: Maybe [ClsInst] -> ModGuts -> MGIModGuts
srcSpanTick :: Module -> SrcSpan -> Tickish a
tickSrcSpan :: Outputable a => Tickish a -> SrcSpan
stringTyVar :: String -> TyVar
stringTyCon :: Char -> Int -> String -> TyCon
hasBaseTypeVar :: Var -> Bool
isBaseType :: Type -> Bool
validTyVar :: String -> Bool
tvId :: Var -> [Char]
tracePpr :: Outputable a => [Char] -> a -> a
pprShow :: Show a => a -> SDoc
tidyCBs :: [Bind b] -> [Bind b]
unTick :: Bind b -> Bind b
unTickExpr :: Expr b -> Expr b
isFractionalClass :: Class -> Bool
isDataConId :: Id -> Bool
getDataConVarUnique :: Var -> Unique
newtype Loc
L :: (Int, Int) -> Loc
unpackRealSrcSpan :: RealSrcSpan -> (String, Int, Int, Int, Int)
realSrcSpan :: String -> Int -> Int -> Int -> Int -> RealSrcSpan
toFixSDoc :: Fixpoint a => a -> Doc
sDocDoc :: SDoc -> Doc
pprDoc :: Outputable a => a -> Doc
showPpr :: Outputable a => a -> String
showSDoc :: SDoc -> String
showSDocDump :: SDoc -> String
typeUniqueString :: Outputable a => a -> String
sourcePosSrcSpan :: SourcePos -> SrcSpan
sourcePosSrcLoc :: SourcePos -> SrcLoc
srcSpanSourcePos :: SrcSpan -> SourcePos
srcSpanSourcePosE :: SrcSpan -> SourcePos
srcSpanFilename :: SrcSpan -> String
srcSpanStartLoc :: RealSrcSpan -> Loc
srcSpanEndLoc :: RealSrcSpan -> Loc
oneLine :: RealSrcSpan -> Bool
lineCol :: RealSrcSpan -> (Int, Int)
realSrcSpanSourcePos :: RealSrcSpan -> SourcePos
realSrcSpanSourcePosE :: RealSrcSpan -> SourcePos
getSourcePos :: NamedThing a => a -> SourcePos
getSourcePosE :: NamedThing a => a -> SourcePos
collectArguments :: Int -> CoreExpr -> [Var]
collectValBinders' :: Expr Var -> ([Var], Expr Var)
ignoreLetBinds :: Expr t -> Expr t
isDictionaryExpression :: Expr Id -> Maybe Id
isDictionary :: Symbolic a => a -> Bool
isInternal :: Symbolic a => a -> Bool
realTcArity :: TyCon -> Arity
kindArity :: Kind -> Arity
uniqueHash :: Uniquable a => Int -> a -> Int
lookupRdrName :: HscEnv -> ModuleName -> RdrName -> IO (Maybe Name)
addContext :: GhcMonad m => InteractiveImport -> m ()
qualImportDecl :: ModuleName -> ImportDecl name
ignoreInline :: ParsedModule -> ParsedModule
symbolTyCon :: Char -> Int -> Symbol -> TyCon
symbolTyVar :: Symbol -> TyVar
varSymbol :: Var -> Symbol
qualifiedNameSymbol :: Name -> Symbol
fastStringText :: FastString -> Text
tyConTyVarsDef :: TyCon -> [TyVar]
gHC_VERSION :: String
desugarModule :: TypecheckedModule -> Ghc DesugaredModule
symbolFastString :: Symbol -> FastString
lintCoreBindings :: [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
synTyConRhs_maybe :: TyCon -> Maybe Type
tcRnLookupRdrName :: HscEnv -> Located RdrName -> IO (Messages, Maybe [Name])
instance Eq Loc
instance Ord Loc
instance Show Loc
instance Symbolic FastString
instance Symbolic Var
instance Symbolic Name
instance Symbolic TyCon
instance Hashable TyCon
instance Hashable Var
instance Show TyCon
instance Show Class
instance Show Var
instance Show Name
instance Fixpoint Type
instance Fixpoint Name
instance Fixpoint Var
instance FromJSON SrcSpan
instance ToJSON SrcSpan
instance FromJSON RealSrcSpan
instance ToJSON RealSrcSpan
instance Outputable a => Outputable (HashSet a)
instance Hashable SrcSpan
instance Hashable Loc

module Language.Haskell.Liquid.Visitors
class CBVisitable a
freeVars :: CBVisitable a => HashSet Var -> a -> [Var]
readVars :: CBVisitable a => a -> [Var]
letVars :: CBVisitable a => a -> [Var]
literals :: CBVisitable a => a -> [Literal]
instance CBVisitable AltCon
instance CBVisitable (Alt Var)
instance CBVisitable (Expr Var)
instance CBVisitable CoreBind
instance CBVisitable [CoreBind]


-- | This module contains the code for generating "tags" for constraints
--   based on their source, i.e. the top-level binders under which the
--   constraint was generated. These tags are used by fixpoint to
--   prioritize constraints by the "source-level" function.
module Language.Haskell.Liquid.CTags

-- | The <tt>TagKey</tt> is the top-level binder, and <tt>Tag</tt> is a
--   singleton Int list
type TagKey = Var
type TagEnv = HashMap TagKey Tag
defaultTag :: Tag
makeTagEnv :: [CoreBind] -> TagEnv
getTag :: TagKey -> TagEnv -> Tag
memTagEnv :: TagKey -> TagEnv -> Bool


-- | Formats Haskell source code as HTML with CSS and Mouseover Type
--   Annotations
module Language.Haskell.Liquid.ACSS

-- | Formats Haskell source code using HTML and mouse-over annotations
hscolour :: Bool -> Bool -> String -> String

-- | Formats Haskell source code using HTML and mouse-over annotations
hsannot :: Bool -> CommentTransform -> Bool -> (String, AnnMap) -> String
data AnnMap
Ann :: HashMap Loc (String, String) -> [(Loc, Loc, String)] -> !Status -> AnnMap

-- | Loc -&gt; (Var, Type)
types :: AnnMap -> HashMap Loc (String, String)

-- | List of error intervals
errors :: AnnMap -> [(Loc, Loc, String)]
status :: AnnMap -> !Status
breakS :: [Char]
srcModuleName :: String -> String
data Status
Safe :: Status
Unsafe :: Status
Error :: Status
Crash :: Status
instance Eq Status
instance Ord Status
instance Show Status
instance Show Annotation
instance Show Lit
instance Show AnnMap

module Language.Haskell.Liquid.GhcPlay
class Subable a
sub :: Subable a => HashMap CoreBndr CoreExpr -> a -> a
subTy :: Subable a => HashMap TyVar Type -> a -> a
subVar :: Expr t -> Id
substTysWith :: HashMap Var Type -> Type -> Type
instance Subable Type
instance Subable (Bind Var)
instance Subable Var
instance Subable (Alt Var)
instance Subable Coercion
instance Subable CoreExpr

module Language.Haskell.Liquid.Misc
firstDuplicate :: Ord a => [a] -> Maybe a
safeIndex :: [Char] -> Int -> [c] -> c
(!?) :: [a] -> Int -> Maybe a
safeFromJust :: [Char] -> Maybe t -> t
fst4 :: (t, t1, t2, t3) -> t
snd4 :: (t, t1, t2, t3) -> t1
mapFourth4 :: (t -> t4) -> (t1, t2, t3, t) -> (t1, t2, t3, t4)
addFst3 :: t -> (t1, t2) -> (t, t1, t2)
addThd3 :: t2 -> (t, t1) -> (t, t1, t2)
dropFst3 :: (t, t1, t2) -> (t1, t2)
dropThd3 :: (t1, t2, t) -> (t1, t2)
replaceN :: (Num a, Eq a, Enum a) => a -> t -> [t] -> [t]
fourth4 :: (t, t1, t2, t3) -> t3
third4 :: (t, t1, t2, t3) -> t2
mapSndM :: Monad m => (t -> m a) -> (t1, t) -> m (t1, a)
firstM :: Functor f => (t -> f a) -> (t, t1) -> f (a, t1)
secondM :: Functor f => (t -> f a) -> (t1, t) -> f (t1, a)
first3M :: Functor f => (t -> f a) -> (t, t1, t2) -> f (a, t1, t2)
second3M :: Functor f => (t -> f a) -> (t1, t, t2) -> f (t1, a, t2)
third3M :: Functor f => (t -> f a) -> (t1, t2, t) -> f (t1, t2, a)
third3 :: (t -> t3) -> (t1, t2, t) -> (t1, t2, t3)
zip4 :: [t] -> [t1] -> [t2] -> [t3] -> [(t, t1, t2, t3)]
ghc :: [Char]
getIncludeDir :: IO FilePath
getCssPath :: IO FilePath
getCoreToLogicPath :: IO FilePath
maximumWithDefault :: Ord a => a -> [a] -> a
safeZipWithError :: [Char] -> [t] -> [t1] -> [(t, t1)]
safeZip3WithError :: [Char] -> [t] -> [t1] -> [t2] -> [(t, t1, t2)]
mapNs :: (Num a, Eq a) => [a] -> (a1 -> a1) -> [a1] -> [a1]
mapN :: (Num a, Eq a) => a -> (a1 -> a1) -> [a1] -> [a1]
pad :: [Char] -> (a -> a) -> [a] -> [a] -> ([a], [a])
ordNub :: Ord a => [a] -> [a]
intToString :: Int -> String


-- | This module should contain all the global type definitions and basic
--   instances.
module Language.Haskell.Liquid.Types

-- | Command Line Config Options
--   --------------------------------------------
data Config
Config :: [FilePath] -> [FilePath] -> Bool -> Bool -> Bool -> Bool -> [String] -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> Maybe SMTSolver -> Bool -> Bool -> Bool -> [String] -> [String] -> Config

-- | source files to check
files :: Config -> [FilePath]

-- | path to directory for including specs
idirs :: Config -> [FilePath]

-- | check subset of binders modified (+ dependencies) since last check
diffcheck :: Config -> Bool

-- | supports real number arithmetic
real :: Config -> Bool

-- | check all binders (overrides diffcheck)
fullcheck :: Config -> Bool

-- | use native (Haskell) fixpoint constraint solver
native :: Config -> Bool

-- | set of binders to check
binders :: Config -> [String]

-- | whether to complain about specifications for unexported and unused
--   values
noCheckUnknown :: Config -> Bool

-- | disable termination check
notermination :: Config -> Bool

-- | disable warnings output (only show errors)
nowarnings :: Config -> Bool

-- | type all internal variables with true
trustinternals :: Config -> Bool

-- | disable case expand
nocaseexpand :: Config -> Bool

-- | enable strata analysis
strata :: Config -> Bool

-- | disable truing top level types
notruetypes :: Config -> Bool

-- | check totality in definitions
totality :: Config -> Bool

-- | disable prunning unsorted Refinements
noPrune :: Config -> Bool

-- | the maximum number of parameters to accept when mining qualifiers
maxParams :: Config -> Int

-- | name of smtsolver to use [default: try z3, cvc4, mathsat in order]
smtsolver :: Config -> Maybe SMTSolver

-- | drop module qualifers from pretty-printed names.
shortNames :: Config -> Bool

-- | don't show subtyping errors and contexts.
shortErrors :: Config -> Bool

-- | find and use .cabal file to include paths to sources for imported
--   modules
cabalDir :: Config -> Bool

-- | command-line options to pass to GHC
ghcOptions :: Config -> [String]

-- | .c files to compile and link against (for GHC)
cFiles :: Config -> [String]

-- | GHC Information : Code &amp; Spec ------------------------------
data GhcInfo
GI :: !HscEnv -> ![CoreBind] -> ![Var] -> ![Var] -> ![Var] -> ![Var] -> ![FilePath] -> ![String] -> ![FilePath] -> !GhcSpec -> GhcInfo
env :: GhcInfo -> !HscEnv
cbs :: GhcInfo -> ![CoreBind]
derVars :: GhcInfo -> ![Var]
impVars :: GhcInfo -> ![Var]
defVars :: GhcInfo -> ![Var]
useVars :: GhcInfo -> ![Var]
hqFiles :: GhcInfo -> ![FilePath]
imports :: GhcInfo -> ![String]
includes :: GhcInfo -> ![FilePath]
spec :: GhcInfo -> !GhcSpec

-- | The following is the overall type for <i>specifications</i> obtained
--   from parsing the target source and dependent libraries
data GhcSpec
SP :: ![(Var, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Symbol, Located SpecType)] -> ![Located SpecType] -> ![(Located SpecType, Located SpecType)] -> ![(DataCon, DataConP)] -> ![(TyCon, TyConP)] -> ![(Symbol, Var)] -> TCEmb TyCon -> ![Qualifier] -> ![Var] -> ![(Var, [Int])] -> ![(Var, [Expr])] -> !(HashSet Var) -> !(HashSet Var) -> !(HashSet TyCon) -> !Config -> !NameSet -> [Measure SpecType DataCon] -> HashMap TyCon RTyCon -> DEnv Var SpecType -> GhcSpec

-- | Asserted Reftypes eg. see include/Prelude.spec
tySigs :: GhcSpec -> ![(Var, Located SpecType)]

-- | Assumed Reftypes
asmSigs :: GhcSpec -> ![(Var, Located SpecType)]

-- | Data Constructor Measure Sigs eg. (:) :: a -&gt; xs:[a] -&gt; {v: Int
--   | v = 1 + len(xs) }
ctors :: GhcSpec -> ![(Var, Located SpecType)]

-- | Measure Types eg. len :: [a] -&gt; Int
meas :: GhcSpec -> ![(Symbol, Located SpecType)]

-- | Data Type Invariants eg. forall a. {v: [a] | len(v) &gt;= 0}
invariants :: GhcSpec -> ![Located SpecType]

-- | Data Type Invariant Aliases
ialiases :: GhcSpec -> ![(Located SpecType, Located SpecType)]

-- | Predicated Data-Constructors e.g. see tests<i>pos</i>Map.hs
dconsP :: GhcSpec -> ![(DataCon, DataConP)]

-- | Predicated Type-Constructors eg. see tests<i>pos</i>Map.hs
tconsP :: GhcSpec -> ![(TyCon, TyConP)]

-- | List of <a>Symbol</a> free in spec and corresponding GHC var eg.
--   (Cons, Cons#7uz) from tests<i>pos</i>ex1.hs
freeSyms :: GhcSpec -> ![(Symbol, Var)]

-- | How to embed GHC Tycons into fixpoint sorts e.g. "embed Set as
--   Set_set" from include<i>Data</i>Set.spec
tcEmbeds :: GhcSpec -> TCEmb TyCon

-- | Qualifiers in Source/Spec files e.g tests<i>pos</i>qualTest.hs
qualifiers :: GhcSpec -> ![Qualifier]

-- | Top-level Binders To Verify (empty means ALL binders)
tgtVars :: GhcSpec -> ![Var]

-- | Lexicographically ordered size witnesses for termination
decr :: GhcSpec -> ![(Var, [Int])]

-- | Lexicographically ordered expressions for termination
texprs :: GhcSpec -> ![(Var, [Expr])]

-- | Variables that should be checked in the environment they are used
lvars :: GhcSpec -> !(HashSet Var)

-- | Binders to IGNORE during termination checking
lazy :: GhcSpec -> !(HashSet Var)

-- | Binders to IGNORE during termination checking
autosize :: GhcSpec -> !(HashSet TyCon)

-- | Configuration Options
config :: GhcSpec -> !Config

-- | <tt>Name</tt>s exported by the module being verified
exports :: GhcSpec -> !NameSet
measures :: GhcSpec -> [Measure SpecType DataCon]
tyconEnv :: GhcSpec -> HashMap TyCon RTyCon

-- | Dictionary Environment
dicts :: GhcSpec -> DEnv Var SpecType

-- | Which Top-Level Binders Should be Verified
data TargetVars
AllVars :: TargetVars
Only :: ![Var] -> TargetVars

-- | Located Values
--   ---------------------------------------------------------
data Located a :: * -> *
Loc :: SrictNotUnpackedSourcePos -> SrictNotUnpackedSourcePos -> a -> Located a

-- | Start Position
loc :: Located a -> SrictNotUnpackedSourcePos

-- | End Position
locE :: Located a -> SrictNotUnpackedSourcePos
val :: Located a -> a
dummyLoc :: a -> Located a
type LocSymbol = Located Symbol
type LocText = Located Text
dummyName :: Symbol
isDummy :: Symbolic a => a -> Bool
data RTyCon
RTyCon :: TyCon -> ![RPVar] -> !TyConInfo -> RTyCon

-- | Co- and Contra-variance for TyCon --------------------------------
--   
--   Indexes start from 0 and type or predicate arguments can be both
--   covariant and contravaariant e.g., for the below Foo dataType
--   
--   data Foo a b c d <a>:: b -</a> Prop, q :: Int -&gt; Prop, r :: a -&gt;
--   Prop&gt; = F (a<a>r</a> -&gt; b<a>p</a>) | Q (c -&gt; a) | G
--   (Int<a>q</a> -&gt; a<a>r</a>)
--   
--   there will be:
--   
--   varianceTyArgs = [Bivariant , Covariant, Contravatiant, Invariant]
--   variancePsArgs = [Covariant, Contravatiant, Bivariant]
data TyConInfo
TyConInfo :: !VarianceInfo -> !VarianceInfo -> !(Maybe (Symbol -> Expr)) -> TyConInfo

-- | variance info for type variables
varianceTyArgs :: TyConInfo -> !VarianceInfo

-- | variance info for predicate variables
variancePsArgs :: TyConInfo -> !VarianceInfo

-- | logical function that computes the size of the structure
sizeFunction :: TyConInfo -> !(Maybe (Symbol -> Expr))
defaultTyConInfo :: TyConInfo
rTyConPVs :: RTyCon -> [RPVar]
rTyConPropVs :: RTyCon -> [PVar RSort]

-- | Accessors for <tt>RTyCon</tt>
isClassRTyCon :: RTyCon -> Bool
isClassType :: TyConable c => RType c t t1 -> Bool
data RType c tv r
RVar :: !tv -> !r -> RType c tv r
rt_var :: RType c tv r -> !tv
rt_reft :: RType c tv r -> !r
RFun :: !Symbol -> !(RType c tv r) -> !(RType c tv r) -> !r -> RType c tv r
rt_bind :: RType c tv r -> !Symbol
rt_in :: RType c tv r -> !(RType c tv r)
rt_out :: RType c tv r -> !(RType c tv r)
rt_reft :: RType c tv r -> !r
RAllT :: !tv -> !(RType c tv r) -> RType c tv r
rt_tvbind :: RType c tv r -> !tv
rt_ty :: RType c tv r -> !(RType c tv r)
RAllP :: !(PVar (RType c tv ())) -> !(RType c tv r) -> RType c tv r
rt_pvbind :: RType c tv r -> !(PVar (RType c tv ()))
rt_ty :: RType c tv r -> !(RType c tv r)
RAllS :: !(Symbol) -> !(RType c tv r) -> RType c tv r
rt_sbind :: RType c tv r -> !(Symbol)
rt_ty :: RType c tv r -> !(RType c tv r)
RApp :: !c -> ![RType c tv r] -> ![RTProp c tv r] -> !r -> RType c tv r
rt_tycon :: RType c tv r -> !c
rt_args :: RType c tv r -> ![RType c tv r]
rt_pargs :: RType c tv r -> ![RTProp c tv r]
rt_reft :: RType c tv r -> !r
RAllE :: !Symbol -> !(RType c tv r) -> !(RType c tv r) -> RType c tv r
rt_bind :: RType c tv r -> !Symbol
rt_allarg :: RType c tv r -> !(RType c tv r)
rt_ty :: RType c tv r -> !(RType c tv r)
REx :: !Symbol -> !(RType c tv r) -> !(RType c tv r) -> RType c tv r
rt_bind :: RType c tv r -> !Symbol
rt_exarg :: RType c tv r -> !(RType c tv r)
rt_ty :: RType c tv r -> !(RType c tv r)

-- | For expression arguments to type aliases see tests<i>pos</i>vector2.hs
RExprArg :: (Located Expr) -> RType c tv r
RAppTy :: !(RType c tv r) -> !(RType c tv r) -> !r -> RType c tv r
rt_arg :: RType c tv r -> !(RType c tv r)
rt_res :: RType c tv r -> !(RType c tv r)
rt_reft :: RType c tv r -> !r
RRTy :: ![(Symbol, RType c tv r)] -> !r -> !Oblig -> !(RType c tv r) -> RType c tv r
rt_env :: RType c tv r -> ![(Symbol, RType c tv r)]
rt_ref :: RType c tv r -> !r
rt_obl :: RType c tv r -> !Oblig
rt_ty :: RType c tv r -> !(RType c tv r)

-- | let LH match against the Haskell type and add k-vars, e.g. `x:_` see
--   tests<i>pos</i>Holes.hs
RHole :: r -> RType c tv r

-- | <tt>Ref</tt> describes `Prop τ` and <tt>HProp</tt> arguments applied
--   to type constructors. For example, in [a]<a>-</a> v &gt; h}&gt;, we
--   apply (via <a>RApp</a>) * the <a>RProp</a> denoted by `{h -&gt; v &gt;
--   h}` to * the <a>RTyCon</a> denoted by `[]`. Thus, <tt>Ref</tt> is used
--   for abstract-predicate (arguments) that are associated with _type
--   constructors_ i.e. whose semantics are _dependent upon_ the data-type.
--   In contrast, the <a>Predicate</a> argument in <a>ur_pred</a> in the
--   <tt>UReft</tt> applies directly to any type and has semantics
--   _independent of_ the data-type.
data Ref τ r t

-- | Parse-time <a>RProp</a>
RPropP :: [(Symbol, τ)] -> r -> Ref τ r t
rf_args :: Ref τ r t -> [(Symbol, τ)]
rf_reft :: Ref τ r t -> r

-- | Abstract refinement associated with <a>RTyCon</a>
RProp :: [(Symbol, τ)] -> t -> Ref τ r t
rf_args :: Ref τ r t -> [(Symbol, τ)]
rf_body :: Ref τ r t -> t

-- | Abstract heap-refinement associated with <a>RTyCon</a>
RHProp :: [(Symbol, τ)] -> World t -> Ref τ r t
rf_args :: Ref τ r t -> [(Symbol, τ)]
rf_heap :: Ref τ r t -> World t

-- | <tt>RTProp</tt> is a convenient alias for <tt>Ref</tt> that will save
--   a bunch of typing. In general, perhaps we need not expose <tt>Ref</tt>
--   directly at all.
type RTProp c tv r = Ref (RType c tv ()) r (RType c tv r)
newtype RTyVar
RTV :: TyVar -> RTyVar

-- | Refinement Type Aliases
data RTAlias tv ty
RTA :: Symbol -> [tv] -> [tv] -> ty -> SourcePos -> SourcePos -> RTAlias tv ty
rtName :: RTAlias tv ty -> Symbol
rtTArgs :: RTAlias tv ty -> [tv]
rtVArgs :: RTAlias tv ty -> [tv]
rtBody :: RTAlias tv ty -> ty
rtPos :: RTAlias tv ty -> SourcePos
rtPosE :: RTAlias tv ty -> SourcePos
data HSeg t
HBind :: !Symbol -> t -> HSeg t
hs_addr :: HSeg t -> !Symbol
hs_val :: HSeg t -> t
HVar :: UsedPVar -> HSeg t

-- | A <tt>World</tt> is a Separation Logic predicate that is essentially a
--   sequence of binders that satisfies two invariants (TODO:LIQUID): 1.
--   Each `hs_addr :: Symbol` appears at most once, 2. There is at most one
--   <a>HVar</a> in a list.
newtype World t
World :: [HSeg t] -> World t
class Eq c => TyConable c where isClass = const False isNumCls = const False isFracCls = const False
isFun :: TyConable c => c -> Bool
isList :: TyConable c => c -> Bool
isTuple :: TyConable c => c -> Bool
ppTycon :: TyConable c => c -> Doc
isClass :: TyConable c => c -> Bool
isNumCls :: TyConable c => c -> Bool
isFracCls :: TyConable c => c -> Bool
class (TyConable c, Eq c, Eq tv, Hashable tv, Reftable r, PPrint r) => RefTypable c tv r
ppRType :: RefTypable c tv r => Prec -> RType c tv r -> Doc
class SubsTy tv ty a
subt :: SubsTy tv ty a => (tv, ty) -> a -> a

-- | Abstract Predicate Variables ----------------------------------
data PVar t
PV :: !Symbol -> !(PVKind t) -> !Symbol -> ![(t, Symbol, Expr)] -> PVar t
pname :: PVar t -> !Symbol
ptype :: PVar t -> !(PVKind t)
parg :: PVar t -> !Symbol
pargs :: PVar t -> ![(t, Symbol, Expr)]
isPropPV :: PVar t -> Bool
pvType :: PVar t -> t
data PVKind t
PVProp :: t -> PVKind t
PVHProp :: PVKind t
newtype Predicate
Pr :: [UsedPVar] -> Predicate
data UReft r
U :: !r -> !Predicate -> !Strata -> UReft r
ur_reft :: UReft r -> !r
ur_pred :: UReft r -> !Predicate
ur_strata :: UReft r -> !Strata

-- | Values Related to Specifications ------------------------------------
--   
--   Data type refinements
data DataDecl
D :: LocSymbol -> [Symbol] -> [PVar BSort] -> [Symbol] -> [(LocSymbol, [(Symbol, BareType)])] -> !SourcePos -> (Maybe (Symbol -> Expr)) -> DataDecl

-- | Type Constructor Name
tycName :: DataDecl -> LocSymbol

-- | Tyvar Parameters
tycTyVars :: DataDecl -> [Symbol]

-- | PVar Parameters
tycPVars :: DataDecl -> [PVar BSort]

-- | PLabel Parameters
tycTyLabs :: DataDecl -> [Symbol]

-- | <ul>
--   <li><i>DataCon, [(fieldName, fieldType)</i> ]</li>
--   </ul>
tycDCons :: DataDecl -> [(LocSymbol, [(Symbol, BareType)])]

-- | Source Position
tycSrcPos :: DataDecl -> !SourcePos

-- | Measure that should decrease in recursive calls
tycSFun :: DataDecl -> (Maybe (Symbol -> Expr))
data DataConP
DataConP :: !SourcePos -> ![RTyVar] -> ![PVar RSort] -> ![Symbol] -> ![SpecType] -> ![(Symbol, SpecType)] -> !SpecType -> !SourcePos -> DataConP
dc_loc :: DataConP -> !SourcePos
freeTyVars :: DataConP -> ![RTyVar]
freePred :: DataConP -> ![PVar RSort]
freeLabels :: DataConP -> ![Symbol]

-- | FIXME: WHAT IS THIS??
tyConsts :: DataConP -> ![SpecType]

-- | These are backwards, why??
tyArgs :: DataConP -> ![(Symbol, SpecType)]
tyRes :: DataConP -> !SpecType
dc_locE :: DataConP -> !SourcePos
data TyConP
TyConP :: ![RTyVar] -> ![PVar RSort] -> ![Symbol] -> !VarianceInfo -> !VarianceInfo -> !(Maybe (Symbol -> Expr)) -> TyConP
freeTyVarsTy :: TyConP -> ![RTyVar]
freePredTy :: TyConP -> ![PVar RSort]
freeLabelTy :: TyConP -> ![Symbol]
varianceTs :: TyConP -> !VarianceInfo
variancePs :: TyConP -> !VarianceInfo
sizeFun :: TyConP -> !(Maybe (Symbol -> Expr))
type RRType = RType RTyCon RTyVar
type BRType = RType LocSymbol Symbol
type RRProp r = Ref RSort r (RRType r)
type BSort = BRType ()
type BPVar = PVar BSort
type BareType = BRType RReft
type PrType = RRType Predicate
type SpecType = RRType RReft
type SpecProp = RRProp RReft
type RSort = RRType ()
type UsedPVar = PVar ()
type RPVar = PVar RSort
type RReft = UReft Reft

-- | Error Data Type ---------------------------------------------------
--   
--   The type used during constraint generation, used also to define
--   contexts for errors, hence in this file, and NOT in Constraint.hs
newtype REnv
REnv :: (HashMap Symbol SpecType) -> REnv

-- | Constructor and Destructors for RTypes ----------------------------
data RTypeRep c tv r
RTypeRep :: [tv] -> [PVar (RType c tv ())] -> [Symbol] -> [Symbol] -> [r] -> [RType c tv r] -> (RType c tv r) -> RTypeRep c tv r
ty_vars :: RTypeRep c tv r -> [tv]
ty_preds :: RTypeRep c tv r -> [PVar (RType c tv ())]
ty_labels :: RTypeRep c tv r -> [Symbol]
ty_binds :: RTypeRep c tv r -> [Symbol]
ty_refts :: RTypeRep c tv r -> [r]
ty_args :: RTypeRep c tv r -> [RType c tv r]
ty_res :: RTypeRep c tv r -> (RType c tv r)
fromRTypeRep :: RTypeRep c a r -> RType c a r
toRTypeRep :: RType c tv r -> RTypeRep c tv r
mkArrow :: [a] -> [PVar (RType c a ())] -> [Symbol] -> [(Symbol, RType c a r, r)] -> RType c a r -> RType c a r
bkArrowDeep :: RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a)
bkArrow :: RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a)
safeBkArrow :: RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a)
mkUnivs :: [a] -> [PVar (RType c a ())] -> [Symbol] -> RType c a r -> RType c a r
bkUniv :: RType t1 a t2 -> ([a], [PVar (RType t1 a ())], [Symbol], RType t1 a t2)
bkClass :: TyConable c => RType c tv r -> ([(c, [RType c tv r])], RType c tv r)
rFun :: Monoid r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rCls :: Monoid r => TyCon -> [RType RTyCon tv r] -> RType RTyCon tv r
rRCls :: Monoid r => c -> [RType c tv r] -> RType c tv r
pvars :: Predicate -> [UsedPVar]
pappSym :: Show a => a -> Symbol
pApp :: Symbol -> [Expr] -> Pred
isBase :: RType t t1 t2 -> Bool
isFunTy :: RType t t1 t2 -> Bool
isTrivial :: (TyConable c, Reftable r) => RType c tv r -> Bool
efoldReft :: (TyConable c, Reftable r) => (c -> [RType c tv r] -> [(Symbol, a)]) -> (RType c tv r -> a) -> (SEnv a -> Maybe (RType c tv r) -> r -> c1 -> c1) -> (PVar (RType c tv ()) -> SEnv a -> SEnv a) -> SEnv a -> c1 -> RType c tv r -> c1
foldReft :: (TyConable c, Reftable r) => (r -> c1 -> c1) -> c1 -> RType c tv r -> c1
mapReft :: (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReftM :: Monad m => (r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapBot :: (RType c tv s -> RType c tv s) -> RType c tv s -> RType c tv s
mapBind :: (Symbol -> Symbol) -> RType c tv r -> RType c tv r
data Oblig

-- | Obligation that proves termination
OTerm :: Oblig

-- | Obligation that proves invariants
OInv :: Oblig

-- | Obligation that proves constraints
OCons :: Oblig
ignoreOblig :: RType t t1 t2 -> RType t t1 t2
addTermCond :: SpecType -> RReft -> SpecType
addInvCond :: SpecType -> RReft -> SpecType

-- | Annotations -------------------------------------------------------
newtype AnnInfo a
AI :: (HashMap SrcSpan [(Maybe Text, a)]) -> AnnInfo a
data Annot t
AnnUse :: t -> Annot t
AnnDef :: t -> Annot t
AnnRDf :: t -> Annot t
AnnLoc :: SrcSpan -> Annot t

-- | Output ------------------------------------------------------------
data Output a
O :: Maybe [String] -> ![Error] -> !(AnnInfo a) -> !(AnnInfo a) -> ![SrcSpan] -> FixResult Error -> Output a
o_vars :: Output a -> Maybe [String]
o_errors :: Output a -> ![Error]
o_types :: Output a -> !(AnnInfo a)
o_templs :: Output a -> !(AnnInfo a)
o_bots :: Output a -> ![SrcSpan]
o_result :: Output a -> FixResult Error
hole :: Pred
isHole :: Pred -> Bool
hasHole :: Reftable r => r -> Bool
ofRSort :: Reftable r => RType c tv () -> RType c tv r
toRSort :: RType c tv r -> RType c tv ()
rTypeValueVar :: Reftable r => RType c tv r -> Symbol
rTypeReft :: Reftable r => RType c tv r -> Reft
stripRTypeBase :: RType t t1 a -> Maybe a
class PPrint a where pprintTidy _ = pprint
pprint :: PPrint a => a -> Doc
pprintTidy :: PPrint a => Tidy -> a -> Doc
showpp :: PPrint a => a -> String
data PPEnv
PP :: Bool -> Bool -> Bool -> Bool -> PPEnv
ppPs :: PPEnv -> Bool
ppTyVar :: PPEnv -> Bool
ppSs :: PPEnv -> Bool
ppShort :: PPEnv -> Bool

-- | Printer
--   ----------------------------------------------------------------
data Tidy
Lossy :: Tidy
Full :: Tidy
ppEnv :: PPEnv
ppEnvShort :: PPEnv -> PPEnv
data ModName
ModName :: !ModType -> !ModuleName -> ModName
data ModType
Target :: ModType
SrcImport :: ModType
SpecImport :: ModType
isSrcImport :: ModName -> Bool
isSpecImport :: ModName -> Bool
getModName :: ModName -> ModuleName
getModString :: ModName -> String
data RTEnv
RTE :: HashMap Symbol (RTAlias RTyVar SpecType) -> HashMap Symbol (RTAlias Symbol Pred) -> HashMap Symbol (RTAlias Symbol Expr) -> RTEnv
typeAliases :: RTEnv -> HashMap Symbol (RTAlias RTyVar SpecType)
predAliases :: RTEnv -> HashMap Symbol (RTAlias Symbol Pred)
exprAliases :: RTEnv -> HashMap Symbol (RTAlias Symbol Expr)
mapRT :: (HashMap Symbol (RTAlias RTyVar SpecType) -> HashMap Symbol (RTAlias RTyVar SpecType)) -> RTEnv -> RTEnv
mapRP :: (HashMap Symbol (RTAlias Symbol Pred) -> HashMap Symbol (RTAlias Symbol Pred)) -> RTEnv -> RTEnv
mapRE :: (HashMap Symbol (RTAlias Symbol Expr) -> HashMap Symbol (RTAlias Symbol Expr)) -> RTEnv -> RTEnv

-- | Converting Results To Answers -------------------------------------
class Result a
result :: Result a => a -> FixResult Error

-- | In the below, we use EMsg instead of, say, SpecType because the latter
--   is impossible to serialize, as it contains GHC internals like TyCon
--   and Class inside it.
type Error = TError SpecType

-- | INVARIANT : all Error constructors should have a pos field
data TError t

-- | liquid type error
ErrSubType :: !SrcSpan -> !Doc -> !(HashMap Symbol t) -> !t -> !t -> TError t
pos :: TError t -> !SrcSpan
msg :: TError t -> !Doc
ctx :: TError t -> !(HashMap Symbol t)
tact :: TError t -> !t
texp :: TError t -> !t

-- | liquid type error
ErrFCrash :: !SrcSpan -> !Doc -> !(HashMap Symbol t) -> !t -> !t -> TError t
pos :: TError t -> !SrcSpan
msg :: TError t -> !Doc
ctx :: TError t -> !(HashMap Symbol t)
tact :: TError t -> !t
texp :: TError t -> !t

-- | liquid type error
ErrAssType :: !SrcSpan -> !Oblig -> !Doc -> !RReft -> TError t
pos :: TError t -> !SrcSpan
obl :: TError t -> !Oblig
msg :: TError t -> !Doc
ref :: TError t -> !RReft

-- | specification parse error
ErrParse :: !SrcSpan -> !Doc -> !ParseError -> TError t
pos :: TError t -> !SrcSpan
msg :: TError t -> !Doc
err :: TError t -> !ParseError

-- | sort error in specification
ErrTySpec :: !SrcSpan -> !Doc -> !t -> !Doc -> TError t
pos :: TError t -> !SrcSpan
var :: TError t -> !Doc
typ :: TError t -> !t
msg :: TError t -> !Doc

-- | sort error in specification
ErrTermSpec :: !SrcSpan -> !Doc -> !Expr -> !Doc -> TError t
pos :: TError t -> !SrcSpan
var :: TError t -> !Doc
exp :: TError t -> !Expr
msg :: TError t -> !Doc

-- | multiple alias with same name error
ErrDupAlias :: !SrcSpan -> !Doc -> !Doc -> ![SrcSpan] -> TError t
pos :: TError t -> !SrcSpan
var :: TError t -> !Doc
kind :: TError t -> !Doc
locs :: TError t -> ![SrcSpan]

-- | multiple specs for same binder error
ErrDupSpecs :: !SrcSpan -> !Doc -> ![SrcSpan] -> TError t
pos :: TError t -> !SrcSpan
var :: TError t -> !Doc
locs :: TError t -> ![SrcSpan]

-- | multiple specs for same binder error
ErrBadData :: !SrcSpan -> !Doc -> !Doc -> TError t
pos :: TError t -> !SrcSpan
var :: TError t -> !Doc
msg :: TError t -> !Doc

-- | Invariant sort error
ErrInvt :: !SrcSpan -> !t -> !Doc -> TError t
pos :: TError t -> !SrcSpan
inv :: TError t -> !t
msg :: TError t -> !Doc

-- | Using sort error
ErrIAl :: !SrcSpan -> !t -> !Doc -> TError t
pos :: TError t -> !SrcSpan
inv :: TError t -> !t
msg :: TError t -> !Doc

-- | Incompatible using error
ErrIAlMis :: !SrcSpan -> !t -> !t -> !Doc -> TError t
pos :: TError t -> !SrcSpan
t1 :: TError t -> !t
t2 :: TError t -> !t
msg :: TError t -> !Doc

-- | Measure sort error
ErrMeas :: !SrcSpan -> !Symbol -> !Doc -> TError t
pos :: TError t -> !SrcSpan
ms :: TError t -> !Symbol
msg :: TError t -> !Doc

-- | Haskell bad Measure error
ErrHMeas :: !SrcSpan -> !Symbol -> !Doc -> TError t
pos :: TError t -> !SrcSpan
ms :: TError t -> !Symbol
msg :: TError t -> !Doc

-- | Unbound symbol in specification
ErrUnbound :: !SrcSpan -> !Doc -> TError t
pos :: TError t -> !SrcSpan
var :: TError t -> !Doc

-- | GHC error: parsing or type checking
ErrGhc :: !SrcSpan -> !Doc -> TError t
pos :: TError t -> !SrcSpan
msg :: TError t -> !Doc

-- | Mismatch between Liquid and Haskell types
ErrMismatch :: !SrcSpan -> !Doc -> !Type -> !Type -> TError t
pos :: TError t -> !SrcSpan
var :: TError t -> !Doc
hs :: TError t -> !Type
lq :: TError t -> !Type

-- | Cyclic Refined Type Alias Definitions
ErrAliasCycle :: !SrcSpan -> ![(SrcSpan, Doc)] -> TError t
pos :: TError t -> !SrcSpan
acycle :: TError t -> ![(SrcSpan, Doc)]

-- | Illegal RTAlias application (from BSort, eg. in PVar)
ErrIllegalAliasApp :: !SrcSpan -> !Doc -> !SrcSpan -> TError t
pos :: TError t -> !SrcSpan
dname :: TError t -> !Doc
dpos :: TError t -> !SrcSpan
ErrAliasApp :: !SrcSpan -> !Int -> !Doc -> !SrcSpan -> !Int -> TError t
pos :: TError t -> !SrcSpan
nargs :: TError t -> !Int
dname :: TError t -> !Doc
dpos :: TError t -> !SrcSpan
dargs :: TError t -> !Int

-- | Previously saved error, that carries over after DiffCheck
ErrSaved :: !SrcSpan -> !Doc -> TError t
pos :: TError t -> !SrcSpan
msg :: TError t -> !Doc

-- | Termination Error
ErrTermin :: ![Var] -> !SrcSpan -> !Doc -> TError t
bind :: TError t -> ![Var]
pos :: TError t -> !SrcSpan
msg :: TError t -> !Doc

-- | Refined Class/Interfaces Conflict
ErrRClass :: !SrcSpan -> !Doc -> ![(SrcSpan, Doc)] -> TError t
pos :: TError t -> !SrcSpan
cls :: TError t -> !Doc
insts :: TError t -> ![(SrcSpan, Doc)]

-- | Unexpected PANIC
ErrOther :: !SrcSpan -> !Doc -> TError t
pos :: TError t -> !SrcSpan
msg :: TError t -> !Doc
newtype EMsg
EMsg :: String -> EMsg
type ErrorResult = FixResult Error
errSpan :: TError a -> SrcSpan
errOther :: Doc -> Error
errToFCrash :: Error -> Error

-- | Source Information Associated With Constraints --------------------
data Cinfo
Ci :: !SrcSpan -> !(Maybe Error) -> Cinfo
ci_loc :: Cinfo -> !SrcSpan
ci_err :: Cinfo -> !(Maybe Error)
data Measure ty ctor
M :: LocSymbol -> ty -> [Def ty ctor] -> Measure ty ctor
name :: Measure ty ctor -> LocSymbol
sort :: Measure ty ctor -> ty
eqns :: Measure ty ctor -> [Def ty ctor]
data CMeasure ty
CM :: LocSymbol -> ty -> CMeasure ty
cName :: CMeasure ty -> LocSymbol
cSort :: CMeasure ty -> ty
data Def ty ctor
Def :: LocSymbol -> [(Symbol, ty)] -> ctor -> Maybe ty -> [(Symbol, Maybe ty)] -> Body -> Def ty ctor
measure :: Def ty ctor -> LocSymbol
dparams :: Def ty ctor -> [(Symbol, ty)]
ctor :: Def ty ctor -> ctor
dsort :: Def ty ctor -> Maybe ty
binds :: Def ty ctor -> [(Symbol, Maybe ty)]
body :: Def ty ctor -> Body
data Body

-- | Measure Refinement: {v | v = e }
E :: Expr -> Body

-- | Measure Refinement: {v | (? v) <a>=</a> p }
P :: Pred -> Body

-- | Measure Refinement: {v | p}
R :: Symbol -> Pred -> Body
data RClass ty
RClass :: LocSymbol -> [ty] -> [Symbol] -> [(LocSymbol, ty)] -> RClass ty
rcName :: RClass ty -> LocSymbol
rcSupers :: RClass ty -> [ty]
rcTyVars :: RClass ty -> [Symbol]
rcMethods :: RClass ty -> [(LocSymbol, ty)]

-- | KVar Profile -----------------------------------------
data KVKind
RecBindE :: KVKind
NonRecBindE :: KVKind
TypeInstE :: KVKind
PredInstE :: KVKind
LamE :: KVKind
CaseE :: KVKind
LetE :: KVKind
data KVProf
emptyKVProf :: KVProf
updKVProf :: KVKind -> [KVar] -> KVProf -> KVProf
mapRTAVars :: (a -> tv) -> RTAlias a ty -> RTAlias tv ty
insertsSEnv :: SEnv a -> [(Symbol, a)] -> SEnv a
data Stratum
SVar :: Symbol -> Stratum
SDiv :: Stratum
SWhnf :: Stratum
SFin :: Stratum
type Strata = [Stratum]
isSVar :: Stratum -> Bool
getStrata :: RType t t1 (UReft r) -> [Stratum]
makeDivType :: SpecType -> SpecType
makeFinType :: SpecType -> SpecType
type LogicMap = HashMap Symbol LMap
toLogicMap :: [(Symbol, [Symbol], Expr)] -> HashMap Symbol LMap
eAppWithMap :: (Hashable k, Eq k) => HashMap k LMap -> Located k -> [Expr] -> Expr -> Expr
data LMap
LMap :: Symbol -> [Symbol] -> Expr -> LMap
lvar :: LMap -> Symbol
largs :: LMap -> [Symbol]
lexpr :: LMap -> Expr
type RDEnv = DEnv Var SpecType
newtype DEnv x ty
DEnv :: (HashMap x (HashMap Symbol ty)) -> DEnv x ty

-- | Refined Instances ---------------------------------------------------
data RInstance t
RI :: LocSymbol -> t -> [(LocSymbol, t)] -> RInstance t
riclass :: RInstance t -> LocSymbol
ritype :: RInstance t -> t
risigs :: RInstance t -> [(LocSymbol, t)]
class Reftable r => UReftable r where ofUReft (U r _ _) = ofReft r
ofUReft :: UReftable r => UReft Reft -> r
liquidBegin :: String
liquidEnd :: String
instance [overlap ok] Typeable Config
instance [overlap ok] Typeable PVKind
instance [overlap ok] Typeable PVar
instance [overlap ok] Typeable Predicate
instance [overlap ok] Typeable RTyVar
instance [overlap ok] Typeable TyConInfo
instance [overlap ok] Typeable Oblig
instance [overlap ok] Typeable HSeg
instance [overlap ok] Typeable World
instance [overlap ok] Typeable Ref
instance [overlap ok] Typeable RType
instance [overlap ok] Typeable RTyCon
instance [overlap ok] Typeable TyConP
instance [overlap ok] Typeable Stratum
instance [overlap ok] Typeable UReft
instance [overlap ok] Typeable DataConP
instance [overlap ok] Typeable EMsg
instance [overlap ok] Typeable TError
instance [overlap ok] Typeable Body
instance [overlap ok] Typeable Def
instance [overlap ok] Typeable Measure
instance [overlap ok] Typeable KVKind
instance [overlap ok] (Eq ctor, Eq ty) => Eq (Def ty ctor)
instance [overlap ok] Data Config
instance [overlap ok] Show Config
instance [overlap ok] Eq Config
instance [overlap ok] Eq Tidy
instance [overlap ok] Ord Tidy
instance [overlap ok] Generic (PVKind t)
instance [overlap ok] Data t => Data (PVKind t)
instance [overlap ok] Foldable PVKind
instance [overlap ok] Traversable PVKind
instance [overlap ok] Show t => Show (PVKind t)
instance [overlap ok] Generic (PVar t)
instance [overlap ok] Data t => Data (PVar t)
instance [overlap ok] Show t => Show (PVar t)
instance [overlap ok] Generic Predicate
instance [overlap ok] Data Predicate
instance [overlap ok] Generic RTyVar
instance [overlap ok] Data RTyVar
instance [overlap ok] Generic TyConInfo
instance [overlap ok] Data TyConInfo
instance [overlap ok] Generic Oblig
instance [overlap ok] Data Oblig
instance [overlap ok] Generic (HSeg t)
instance [overlap ok] Data t => Data (HSeg t)
instance [overlap ok] Generic (World t)
instance [overlap ok] Data t => Data (World t)
instance [overlap ok] Generic (Ref τ r t)
instance [overlap ok] (Data τ, Data r, Data t) => Data (Ref τ r t)
instance [overlap ok] Generic (RType c tv r)
instance [overlap ok] (Data c, Data tv, Data r) => Data (RType c tv r)
instance [overlap ok] Generic RTyCon
instance [overlap ok] Data RTyCon
instance [overlap ok] Generic TyConP
instance [overlap ok] Data TyConP
instance [overlap ok] Generic Stratum
instance [overlap ok] Data Stratum
instance [overlap ok] Eq Stratum
instance [overlap ok] Generic (UReft r)
instance [overlap ok] Data r => Data (UReft r)
instance [overlap ok] Generic DataConP
instance [overlap ok] Data DataConP
instance [overlap ok] (Eq x, Hashable x) => Monoid (DEnv x ty)
instance [overlap ok] Generic EMsg
instance [overlap ok] Data EMsg
instance [overlap ok] Functor TError
instance [overlap ok] Eq Cinfo
instance [overlap ok] Ord Cinfo
instance [overlap ok] Generic Cinfo
instance [overlap ok] Eq ModType
instance [overlap ok] Ord ModType
instance [overlap ok] Eq ModName
instance [overlap ok] Ord ModName
instance [overlap ok] Show Body
instance [overlap ok] Eq Body
instance [overlap ok] Data Body
instance [overlap ok] (Show ty, Show ctor) => Show (Def ty ctor)
instance [overlap ok] (Data ty, Data ctor) => Data (Def ty ctor)
instance [overlap ok] (Data ty, Data ctor) => Data (Measure ty ctor)
instance [overlap ok] Show ty => Show (RClass ty)
instance [overlap ok] Generic (AnnInfo a)
instance [overlap ok] Generic (Output a)
instance [overlap ok] Generic KVKind
instance [overlap ok] Eq KVKind
instance [overlap ok] Ord KVKind
instance [overlap ok] Show KVKind
instance [overlap ok] Enum KVKind
instance [overlap ok] Data KVKind
instance Datatype D1PVKind
instance Constructor C1_0PVKind
instance Constructor C1_1PVKind
instance Datatype D1PVar
instance Constructor C1_0PVar
instance Selector S1_0_0PVar
instance Selector S1_0_1PVar
instance Selector S1_0_2PVar
instance Selector S1_0_3PVar
instance Datatype D1Predicate
instance Constructor C1_0Predicate
instance Datatype D1RTyVar
instance Constructor C1_0RTyVar
instance Datatype D1TyConInfo
instance Constructor C1_0TyConInfo
instance Selector S1_0_0TyConInfo
instance Selector S1_0_1TyConInfo
instance Selector S1_0_2TyConInfo
instance Datatype D1Oblig
instance Constructor C1_0Oblig
instance Constructor C1_1Oblig
instance Constructor C1_2Oblig
instance Datatype D1HSeg
instance Constructor C1_0HSeg
instance Constructor C1_1HSeg
instance Selector S1_0_0HSeg
instance Selector S1_0_1HSeg
instance Datatype D1World
instance Constructor C1_0World
instance Datatype D1Ref
instance Constructor C1_0Ref
instance Constructor C1_1Ref
instance Constructor C1_2Ref
instance Selector S1_0_0Ref
instance Selector S1_0_1Ref
instance Selector S1_1_0Ref
instance Selector S1_1_1Ref
instance Selector S1_2_0Ref
instance Selector S1_2_1Ref
instance Datatype D1RType
instance Constructor C1_0RType
instance Constructor C1_1RType
instance Constructor C1_2RType
instance Constructor C1_3RType
instance Constructor C1_4RType
instance Constructor C1_5RType
instance Constructor C1_6RType
instance Constructor C1_7RType
instance Constructor C1_8RType
instance Constructor C1_9RType
instance Constructor C1_10RType
instance Constructor C1_11RType
instance Selector S1_0_0RType
instance Selector S1_0_1RType
instance Selector S1_1_0RType
instance Selector S1_1_1RType
instance Selector S1_1_2RType
instance Selector S1_1_3RType
instance Selector S1_2_0RType
instance Selector S1_2_1RType
instance Selector S1_3_0RType
instance Selector S1_3_1RType
instance Selector S1_4_0RType
instance Selector S1_4_1RType
instance Selector S1_5_0RType
instance Selector S1_5_1RType
instance Selector S1_5_2RType
instance Selector S1_5_3RType
instance Selector S1_6_0RType
instance Selector S1_6_1RType
instance Selector S1_6_2RType
instance Selector S1_7_0RType
instance Selector S1_7_1RType
instance Selector S1_7_2RType
instance Selector S1_9_0RType
instance Selector S1_9_1RType
instance Selector S1_9_2RType
instance Selector S1_10_0RType
instance Selector S1_10_1RType
instance Selector S1_10_2RType
instance Selector S1_10_3RType
instance Datatype D1RTyCon
instance Constructor C1_0RTyCon
instance Selector S1_0_0RTyCon
instance Selector S1_0_1RTyCon
instance Selector S1_0_2RTyCon
instance Datatype D1TyConP
instance Constructor C1_0TyConP
instance Selector S1_0_0TyConP
instance Selector S1_0_1TyConP
instance Selector S1_0_2TyConP
instance Selector S1_0_3TyConP
instance Selector S1_0_4TyConP
instance Selector S1_0_5TyConP
instance Datatype D1Stratum
instance Constructor C1_0Stratum
instance Constructor C1_1Stratum
instance Constructor C1_2Stratum
instance Constructor C1_3Stratum
instance Datatype D1UReft
instance Constructor C1_0UReft
instance Selector S1_0_0UReft
instance Selector S1_0_1UReft
instance Selector S1_0_2UReft
instance Datatype D1DataConP
instance Constructor C1_0DataConP
instance Selector S1_0_0DataConP
instance Selector S1_0_1DataConP
instance Selector S1_0_2DataConP
instance Selector S1_0_3DataConP
instance Selector S1_0_4DataConP
instance Selector S1_0_5DataConP
instance Selector S1_0_6DataConP
instance Selector S1_0_7DataConP
instance Datatype D1EMsg
instance Constructor C1_0EMsg
instance Datatype D1Cinfo
instance Constructor C1_0Cinfo
instance Selector S1_0_0Cinfo
instance Selector S1_0_1Cinfo
instance Datatype D1AnnInfo
instance Constructor C1_0AnnInfo
instance Datatype D1Output
instance Constructor C1_0Output
instance Selector S1_0_0Output
instance Selector S1_0_1Output
instance Selector S1_0_2Output
instance Selector S1_0_3Output
instance Selector S1_0_4Output
instance Selector S1_0_5Output
instance Datatype D1KVKind
instance Constructor C1_0KVKind
instance Constructor C1_1KVKind
instance Constructor C1_2KVKind
instance Constructor C1_3KVKind
instance Constructor C1_4KVKind
instance Constructor C1_5KVKind
instance Constructor C1_6KVKind
instance [overlap ok] Show DataCon
instance [overlap ok] PPrint DataCon
instance [overlap ok] Symbolic DataCon
instance [overlap ok] NFData KVProf
instance [overlap ok] PPrint KVProf
instance [overlap ok] PPrint KVKind
instance [overlap ok] NFData KVKind
instance [overlap ok] Hashable KVKind
instance [overlap ok] Monoid (Output a)
instance [overlap ok] NFData (Annot a)
instance [overlap ok] NFData a => NFData (AnnInfo a)
instance [overlap ok] Functor AnnInfo
instance [overlap ok] Monoid (AnnInfo a)
instance [overlap ok] Functor RClass
instance [overlap ok] Subable Body
instance [overlap ok] Subable (Def ty ctor)
instance [overlap ok] Subable (Measure ty ctor)
instance [overlap ok] Monoid RTEnv
instance [overlap ok] Symbolic ModuleName
instance [overlap ok] Symbolic ModName
instance [overlap ok] Show ModName
instance [overlap ok] Result (FixResult Cinfo)
instance [overlap ok] Result Error
instance [overlap ok] Result [Error]
instance [overlap ok] NFData Cinfo
instance [overlap ok] Error Error
instance [overlap ok] Ord Error
instance [overlap ok] Eq Error
instance [overlap ok] PPrint EMsg
instance [overlap ok] PPrint SortedReft
instance [overlap ok] PPrint Reft
instance [overlap ok] PPrint Refa
instance [overlap ok] PPrint Predicate
instance [overlap ok] PPrint a => PPrint (PVar a)
instance [overlap ok] PPrint Pred
instance [overlap ok] PPrint SymConst
instance [overlap ok] PPrint Expr
instance [overlap ok] PPrint Symbol
instance [overlap ok] PPrint Sort
instance [overlap ok] PPrint Bop
instance [overlap ok] PPrint Brel
instance [overlap ok] PPrint Constant
instance [overlap ok] PPrint Integer
instance [overlap ok] PPrint Int
instance [overlap ok] PPrint a => PPrint (Located a)
instance [overlap ok] PPrint Text
instance [overlap ok] PPrint String
instance [overlap ok] PPrint ()
instance [overlap ok] PPrint SourcePos
instance [overlap ok] PPrint Strata
instance [overlap ok] PPrint Stratum
instance [overlap ok] Show Stratum
instance [overlap ok] Functor (RType a b)
instance [overlap ok] Functor UReft
instance [overlap ok] Reftable Predicate
instance [overlap ok] (Subable r, RefTypable c tv r) => Subable (RType c tv r)
instance [overlap ok] (Reftable r, RefTypable c tv r) => Subable (RTProp c tv r)
instance [overlap ok] Subable r => Subable (UReft r)
instance [overlap ok] (PPrint r, Reftable r) => Reftable (UReft r)
instance [overlap ok] UReftable ()
instance [overlap ok] UReftable (UReft Reft)
instance [overlap ok] Reftable Strata
instance [overlap ok] Subable Strata
instance [overlap ok] Subable Stratum
instance [overlap ok] Show DataDecl
instance [overlap ok] Ord DataDecl
instance [overlap ok] Eq DataDecl
instance [overlap ok] Functor RInstance
instance [overlap ok] Show RTyCon
instance [overlap ok] PPrint RTyCon
instance [overlap ok] Fixpoint Cinfo
instance [overlap ok] Fixpoint RTyCon
instance [overlap ok] Eq RTyCon
instance [overlap ok] TyConable LocSymbol
instance [overlap ok] TyConable Symbol
instance [overlap ok] TyConable RTyCon
instance [overlap ok] Monoid Strata
instance [overlap ok] PPrint Oblig
instance [overlap ok] Show Oblig
instance [overlap ok] Show TyConInfo
instance [overlap ok] Default TyConInfo
instance [overlap ok] Symbolic RTyVar
instance [overlap ok] NFData RTyVar
instance [overlap ok] NFData PrType
instance [overlap ok] NFData Strata
instance [overlap ok] NFData r => NFData (UReft r)
instance [overlap ok] Subable Qualifier
instance [overlap ok] Subable Predicate
instance [overlap ok] Subable UsedPVar
instance [overlap ok] Monoid a => Monoid (UReft a)
instance [overlap ok] Monoid Predicate
instance [overlap ok] NFData Predicate
instance [overlap ok] NFData SrcSpan
instance [overlap ok] NFData Var
instance [overlap ok] Hashable (PVar a)
instance [overlap ok] NFData a => NFData (PVar a)
instance [overlap ok] NFData a => NFData (PVKind a)
instance [overlap ok] Functor PVar
instance [overlap ok] Functor PVKind
instance [overlap ok] Ord (PVar t)
instance [overlap ok] Eq (PVar t)
instance [overlap ok] Show LMap
instance [overlap ok] (PPrint a, PPrint b) => PPrint (a, b)
instance [overlap ok] PPrint a => PPrint [a]
instance [overlap ok] PPrint a => PPrint (Maybe a)

module Language.Haskell.Liquid.Strata
class SubStratum a where subsS su x = foldr subS x su
subS :: SubStratum a => (Symbol, Stratum) -> a -> a
subsS :: SubStratum a => [(Symbol, Stratum)] -> a -> a
solveStrata :: [([Stratum], [Stratum])] -> [(Symbol, Stratum)]
(<:=) :: [Stratum] -> [Stratum] -> Bool
instance SubStratum SpecType
instance SubStratum (Annot SpecType)
instance SubStratum a => SubStratum [a]
instance (SubStratum a, SubStratum b) => SubStratum (a, b)
instance SubStratum Stratum

module Language.Haskell.Liquid.Fresh
class (Applicative m, Monad m) => Freshable m a where true = return . id refresh = return . id
fresh :: Freshable m a => m a
true :: Freshable m a => a -> m a
refresh :: Freshable m a => a -> m a
instance (Freshable m Integer, Freshable m r, Reftable r, RefTypable RTyCon RTyVar r) => Freshable m (RRType r)
instance Freshable m Integer => Freshable m Strata
instance Freshable m Integer => Freshable m RReft
instance Freshable m Integer => Freshable m Reft
instance Freshable m Integer => Freshable m [Refa]
instance Freshable m Integer => Freshable m Refa
instance Freshable m Integer => Freshable m Symbol


-- | This module contains various functions for operating on the
--   <tt>World</tt> type defined in Language.Haskell.Liquid.Types
module Language.Haskell.Liquid.World
empty :: World t
instance Monoid (World t)

module Language.Haskell.Liquid.Simplify
simplifyBounds :: SpecType -> SpecType

module Language.Haskell.Liquid.TransformRec
transformRecExpr :: CoreProgram -> CoreProgram
transformScope :: [Bind Id] -> [Bind Id]
instance Freshable Var
instance Freshable Unique
instance Freshable Int

module Language.Haskell.Liquid.ANFTransform
anormalize :: Bool -> HscEnv -> MGIModGuts -> IO [CoreBind]
instance Functor DsM
instance Monad DsM
instance MonadUnique DsM
instance Applicative DsM


-- | Module with all the printing and serialization routines
module Language.Haskell.Liquid.PrettyPrint

-- | Printer
--   ----------------------------------------------------------------
data Tidy
Lossy :: Tidy
Full :: Tidy

-- | Pretty Printing RefType ----------------------------------
rtypeDoc :: (PPrint (RType a tv ()), PPrint (RType a tv r), PPrint a, PPrint r, PPrint tv, TyConable a, Reftable (RTProp a tv r), Reftable r) => Tidy -> RType a tv r -> Doc
ppr_rtype :: (PPrint (RType a tv ()), PPrint (RType a tv r), PPrint a, PPrint r, PPrint tv, TyConable a, Reftable (RTProp a tv r), Reftable r) => PPEnv -> Prec -> RType a tv r -> Doc

-- | Printing an Ordered List
pprManyOrdered :: (PPrint a, Ord a) => Tidy -> String -> [a] -> [Doc]
pprintLongList :: PPrint a => [a] -> Doc
ppSpine :: PPrint a => RType a t t1 -> Doc
pprintSymbol :: Symbol -> Doc
instance (Ord k, PPrint k, PPrint v) => PPrint (HashMap k v)
instance PPrint a => PPrint (AnnInfo a)
instance PPrint t => PPrint (Annot t)
instance (PPrint r, Reftable r) => PPrint (UReft r)
instance (Reftable s, PPrint s, PPrint p, Reftable p, PPrint t, PPrint (RType b c p)) => PPrint (Ref t s (RType b c p))
instance PPrint RTyVar
instance Show Predicate
instance PPrint Class
instance PPrint Type
instance PPrint TyCon
instance PPrint Name
instance PPrint Var
instance PPrint ParseError
instance PPrint SourceError
instance PPrint ErrMsg
instance PPrint Doc
instance PPrint SrcSpan


-- | Refinement Types. Mostly mirroring the GHC Type definition, but with
--   room for refinements of various sorts.
module Language.Haskell.Liquid.RefType
uTop :: r -> UReft r
uReft :: (Symbol, Refa) -> UReft Reft

-- | Various functions for converting vanilla <a>Reft</a> to <tt>Spec</tt>
uRType :: RType c tv a -> RType c tv (UReft a)
uRType' :: RType c tv (UReft a) -> RType c tv a
uRTypeGen :: Reftable b => RType c tv a -> RType c tv b
uPVar :: PVar t -> UsedPVar
applySolution :: Functor f => FixSolution -> f SpecType -> f SpecType
isDecreasing :: Eq a => HashSet TyCon -> [a] -> RType RTyCon a t -> Bool
makeDecrType :: Symbolic a => HashSet TyCon -> [(a, (Symbol, RType RTyCon t (UReft Reft)))] -> (Symbol, RType RTyCon t (UReft Reft))
makeNumEnv :: TyConable c => [RType c b t] -> [b]
makeLexRefa :: [Expr] -> [Expr] -> UReft Reft
pdVar :: PVar t -> Predicate
findPVar :: [PVar (RType c tv ())] -> UsedPVar -> PVar (RType c tv ())
freeTyVars :: Eq a => RType t a t1 -> [a]
tyClasses :: RefTypable RTyCon t t1 => RType RTyCon t t1 -> [(Class, [RType RTyCon t t1])]
tyConName :: TyCon -> Symbol
ofType :: Monoid r => Type -> RType RTyCon RTyVar r
toType :: (Reftable r, PPrint r) => RRType r -> Type
rTyVar :: TyVar -> RTyVar
rVar :: Monoid r => TyVar -> RType c RTyVar r
rApp :: TyCon -> [RType RTyCon tv r] -> [RTProp RTyCon tv r] -> r -> RType RTyCon tv r
rEx :: [(Symbol, RType c tv r)] -> RType c tv r -> RType c tv r
symbolRTyVar :: Symbol -> RTyVar
addTyConInfo :: (PPrint r, Reftable r) => (HashMap TyCon FTycon) -> (HashMap TyCon RTyCon) -> RRType r -> RRType r
appRTyCon :: SubsTy RTyVar (RType c RTyVar ()) RPVar => HashMap TyCon FTycon -> HashMap TyCon RTyCon -> RTyCon -> [RType c RTyVar r] -> RTyCon
typeSort :: TCEmb TyCon -> Type -> Sort
typeUniqueSymbol :: Type -> Symbol
strengthen :: Reftable r => RType c tv r -> r -> RType c tv r
generalize :: RefTypable c tv r => RType c tv r -> RType c tv r
normalizePds :: RefTypable c tv r => RType c tv r -> RType c tv r
subts :: SubsTy tv ty c => [(tv, ty)] -> c -> c
subvPredicate :: (UsedPVar -> UsedPVar) -> Predicate -> Predicate
subvUReft :: (UsedPVar -> UsedPVar) -> UReft Reft -> UReft Reft
subsTyVar_meet :: (FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => (tv, RType c tv (), RType c tv s) -> RType c tv s -> RType c tv s
subsTyVars_meet :: (FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => [(tv, RType c tv (), RType c tv s)] -> RType c tv s -> RType c tv s
subsTyVar_nomeet :: (FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => (tv, RType c tv (), RType c tv s) -> RType c tv s -> RType c tv s
subsTyVars_nomeet :: (FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, TyConable c, Reftable s, Hashable tv, Eq tv) => [(tv, RType c tv (), RType c tv s)] -> RType c tv s -> RType c tv s
dataConSymbol :: DataCon -> Symbol
dataConMsReft :: Reftable r => RType c tv r -> [Symbol] -> Reft
dataConReft :: DataCon -> [Symbol] -> Reft

-- | Binders generated by class predicates, typically for constraining
--   tyvars (e.g. FNum)
classBinds :: TyConable c => RType c RTyVar t -> [(Symbol, SortedReft)]
isSizeable :: HashSet TyCon -> TyCon -> Bool
rTypeSortedReft :: (PPrint r, Reftable r) => TCEmb TyCon -> RRType r -> SortedReft
rTypeSort :: (PPrint r, Reftable r) => TCEmb TyCon -> RRType r -> Sort
shiftVV :: SpecType -> Symbol -> SpecType
mkDataConIdsTy :: (PPrint r, Reftable r) => (DataCon, RType RTyCon RTyVar r) -> [(Var, RType RTyCon RTyVar r)]
mkTyConInfo :: TyCon -> VarianceInfo -> VarianceInfo -> (Maybe (Symbol -> Expr)) -> TyConInfo
strengthenRefTypeGen :: (RefTypable c tv (), RefTypable c tv r, PPrint (RType c tv r), FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c) => RType c tv r -> RType c tv r -> RType c tv r
strengthenDataConType :: Symbolic t => (t, RType c a (UReft Reft)) -> (t, RType c a (UReft Reft))
instance [incoherent] (Show tv, Show ty) => Show (RTAlias tv ty)
instance [incoherent] Expression Var
instance [incoherent] (SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r))
instance [incoherent] SubsTy Symbol BSort BSort
instance [incoherent] SubsTy Symbol BSort LocSymbol
instance [incoherent] SubsTy RTyVar RSort RSort
instance [incoherent] SubsTy RTyVar RTyVar SpecType
instance [incoherent] SubsTy RTyVar RSort SpecType
instance [incoherent] SubsTy RTyVar RSort PrType
instance [incoherent] SubsTy RTyVar RSort RTyCon
instance [incoherent] SubsTy tv ty ty => SubsTy tv ty (PVar ty)
instance [incoherent] SubsTy tv ty ty => SubsTy tv ty (PVKind ty)
instance [incoherent] SubsTy tv ty Reft
instance [incoherent] SubsTy tv ty ()
instance [incoherent] PPrint REnv
instance [incoherent] PPrint (RTProp c tv r) => Show (RTProp c tv r)
instance [incoherent] PPrint (RType c tv r) => Show (RType c tv r)
instance [incoherent] RefTypable c tv r => PPrint (RType c tv r)
instance [incoherent] PPrint (UReft r) => Show (UReft r)
instance [incoherent] Show RTyVar
instance [incoherent] (NFData b, NFData c, NFData e) => NFData (RType b c e)
instance [incoherent] (NFData a, NFData b, NFData t) => NFData (Ref t a b)
instance [incoherent] Hashable RTyCon
instance [incoherent] Ord RTyCon
instance [incoherent] Hashable RTyVar
instance [incoherent] Ord RTyVar
instance [incoherent] Eq RTyVar
instance [incoherent] Eq Predicate
instance [incoherent] RefTypable c tv () => Eq (RType c tv ())
instance [incoherent] FreeVar LocSymbol Symbol
instance [incoherent] FreeVar RTyCon RTyVar
instance [incoherent] (Reftable r, PPrint r) => RefTypable RTyCon RTyVar r
instance [incoherent] (SubsTy Symbol (RType c Symbol ()) c, TyConable c, Reftable r, PPrint r, PPrint c, FreeVar c Symbol, SubsTy Symbol (RType c Symbol ()) (RType c Symbol ())) => RefTypable c Symbol r
instance [incoherent] Fixpoint Class
instance [incoherent] Fixpoint String
instance [incoherent] (PPrint r, Reftable r) => Reftable (RType RTyCon RTyVar r)
instance [incoherent] Subable (RRProp Reft)
instance [incoherent] (Reftable r, RefTypable c tv r, RefTypable c tv (), FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c) => Reftable (RTProp c tv r)
instance [incoherent] (SubsTy c (RType b c ()) b, Monoid r, Reftable r, RefTypable b c r, RefTypable b c (), FreeVar b c, SubsTy c (RType b c ()) (RType b c ())) => Monoid (RTProp b c r)
instance [incoherent] (SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, Reftable r, RefTypable c tv (), RefTypable c tv (UReft r)) => Monoid (Ref (RType c tv ()) r (RType c tv (UReft r)))
instance [incoherent] (SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, RefTypable c tv (), RefTypable c tv r, PPrint (RType c tv r), FreeVar c tv) => Monoid (RType c tv r)

module Language.Haskell.Liquid.PredType
type PrType = RRType Predicate
data TyConP
TyConP :: ![RTyVar] -> ![PVar RSort] -> ![Symbol] -> !VarianceInfo -> !VarianceInfo -> !(Maybe (Symbol -> Expr)) -> TyConP
freeTyVarsTy :: TyConP -> ![RTyVar]
freePredTy :: TyConP -> ![PVar RSort]
freeLabelTy :: TyConP -> ![Symbol]
varianceTs :: TyConP -> !VarianceInfo
variancePs :: TyConP -> !VarianceInfo
sizeFun :: TyConP -> !(Maybe (Symbol -> Expr))
data DataConP
DataConP :: !SourcePos -> ![RTyVar] -> ![PVar RSort] -> ![Symbol] -> ![SpecType] -> ![(Symbol, SpecType)] -> !SpecType -> !SourcePos -> DataConP
dc_loc :: DataConP -> !SourcePos
freeTyVars :: DataConP -> ![RTyVar]
freePred :: DataConP -> ![PVar RSort]
freeLabels :: DataConP -> ![Symbol]

-- | FIXME: WHAT IS THIS??
tyConsts :: DataConP -> ![SpecType]

-- | These are backwards, why??
tyArgs :: DataConP -> ![(Symbol, SpecType)]
tyRes :: DataConP -> !SpecType
dc_locE :: DataConP -> !SourcePos
dataConTy :: Monoid r => HashMap RTyVar (RType RTyCon RTyVar r) -> Type -> RType RTyCon RTyVar r
dataConPSpecType :: DataCon -> DataConP -> SpecType
makeTyConInfo :: [(TyCon, TyConP)] -> HashMap TyCon RTyCon

-- | Instantiate <a>PVar</a> with <a>RTProp</a>
--   -----------------------------------------------
--   
--   <tt>replacePreds</tt> is the main function used to substitute an
--   (abstract) predicate with a concrete Ref, that is either an
--   <a>RProp</a> or <a>RHProp</a> type. The substitution is invoked to
--   obtain the <a>SpecType</a> resulting at <i>predicate application</i>
--   sites in <a>Constraint</a>. The range of the <a>PVar</a> substitutions
--   are <i>fresh</i> or <i>true</i> <tt>RefType</tt>. That is, there are
--   no further _quantified_ <a>PVar</a> in the target.
replacePreds :: String -> SpecType -> [(RPVar, SpecProp)] -> SpecType
replacePredsWithRefs :: (UsedPVar, (Symbol, [((), Symbol, Expr)]) -> Pred) -> UReft Reft -> UReft Reft
pVartoRConc :: PVar t -> (Symbol, [(a, b, Expr)]) -> Pred

-- | Interface: Modified CoreSyn.exprType due to predApp
--   -------------------
predType :: Type

-- | <tt>pvarRType π</tt> returns a trivial <tt>RType</tt> corresponding to
--   the function signature for a <tt>PVar</tt> <tt>π</tt>. For example, if
--   <tt>π :: T1 -&gt; T2 -&gt; T3 -&gt; Prop</tt> then <tt>pvarRType
--   π</tt> returns an <tt>RType</tt> with an <tt>RTycon</tt> called
--   <tt>predRTyCon</tt> `RApp predRTyCon [T1, T2, T3]`
pvarRType :: (PPrint r, Reftable r) => PVar RSort -> RRType r
substParg :: Functor f => (Symbol, Expr) -> f Predicate -> f Predicate
pApp :: Symbol -> [Expr] -> Pred
wiredSortedSyms :: [(Symbol, Sort)]
instance Show DataConP
instance PPrint DataConP
instance Show TyConP
instance PPrint TyConP

module Language.Haskell.Liquid.Constraint.Types
data CGEnv
CGE :: !SrcSpan -> !REnv -> !(SEnv Var) -> !RDEnv -> !FEnv -> !(HashSet Var) -> !RTyConInv -> !RTyConIAl -> !REnv -> !REnv -> TCEmb TyCon -> !TagEnv -> !(Maybe TagKey) -> !(Maybe (HashMap Symbol SpecType)) -> !(HashMap Symbol CoreExpr) -> !HEnv -> !LConstraint -> CGEnv

-- | Location in original source file
loc :: CGEnv -> !SrcSpan

-- | SpecTypes for Bindings in scope
renv :: CGEnv -> !REnv

-- | Map from free Symbols (e.g. datacons) to Var , penv :: !(F.SEnv
--   PrType) -- ^ PrTypes for top-level bindings (merge with renv)
syenv :: CGEnv -> !(SEnv Var)

-- | Dictionary Environment
denv :: CGEnv -> !RDEnv

-- | Fixpoint Environment
fenv :: CGEnv -> !FEnv

-- | recursive defs being processed (for annotations)
recs :: CGEnv -> !(HashSet Var)

-- | Datatype invariants
invs :: CGEnv -> !RTyConInv

-- | Datatype checkable invariants
ial :: CGEnv -> !RTyConIAl

-- | Top-level variables with (assert)-guarantees to verify
grtys :: CGEnv -> !REnv

-- | Top-level variables with assumed types
assms :: CGEnv -> !REnv

-- | How to embed GHC Tycons into fixpoint sorts
emb :: CGEnv -> TCEmb TyCon

-- | Map from top-level binders to fixpoint tag
tgEnv :: CGEnv -> !TagEnv

-- | Current top-level binder
tgKey :: CGEnv -> !(Maybe TagKey)

-- | Type of recursive function with decreasing constraints
trec :: CGEnv -> !(Maybe (HashMap Symbol SpecType))

-- | Let binding that have not been checked
lcb :: CGEnv -> !(HashMap Symbol CoreExpr)

-- | Types with holes, will need refreshing
holes :: CGEnv -> !HEnv

-- | Logical Constraints
lcs :: CGEnv -> !LConstraint
data LConstraint
LC :: [[(Symbol, SpecType)]] -> LConstraint
data SubC
SubC :: !CGEnv -> !SpecType -> !SpecType -> SubC
senv :: SubC -> !CGEnv
lhs :: SubC -> !SpecType
rhs :: SubC -> !SpecType
SubR :: !CGEnv -> !Oblig -> !RReft -> SubC
senv :: SubC -> !CGEnv
oblig :: SubC -> !Oblig
ref :: SubC -> !RReft
data WfC
WfC :: !CGEnv -> !SpecType -> WfC
type FixSubC = SubC Cinfo
type FixWfC = WfC Cinfo
data CGInfo
CGInfo :: ![SubC] -> ![WfC] -> ![SubC] -> ![FixSubC] -> ![Bool] -> ![FixWfC] -> !Integer -> !BindEnv -> !(AnnInfo (Annot SpecType)) -> !(HashMap TyCon RTyCon) -> ![(Var, [Int])] -> !(HashMap Var [Expr]) -> !(HashSet Var) -> !(HashSet Var) -> !(HashSet TyCon) -> !(TCEmb TyCon) -> !(Kuts) -> ![(Symbol, Sort)] -> !Bool -> !Bool -> !Bool -> !Bool -> ![TError SpecType] -> !KVProf -> !Int -> HashMap BindId SrcSpan -> CGInfo

-- | subtyping constraints over RType
hsCs :: CGInfo -> ![SubC]

-- | wellformedness constraints over RType
hsWfs :: CGInfo -> ![WfC]

-- | additional stratum constrains for let bindings
sCs :: CGInfo -> ![SubC]

-- | subtyping over Sort (post-splitting)
fixCs :: CGInfo -> ![FixSubC]

-- | tracks constraints that come from let-bindings
isBind :: CGInfo -> ![Bool]

-- | wellformedness constraints over Sort (post-splitting)
fixWfs :: CGInfo -> ![FixWfC]

-- | counter for generating fresh KVars
freshIndex :: CGInfo -> !Integer

-- | set of environment binders
binds :: CGInfo -> !BindEnv

-- | source-position annotation map
annotMap :: CGInfo -> !(AnnInfo (Annot SpecType))

-- | information about type-constructors
tyConInfo :: CGInfo -> !(HashMap TyCon RTyCon)

-- | ? FIX THIS
specDecr :: CGInfo -> ![(Var, [Int])]

-- | Terminating Metrics for Recursive functions
termExprs :: CGInfo -> !(HashMap Var [Expr])

-- | Set of variables to ignore for termination checking
specLVars :: CGInfo -> !(HashSet Var)

-- | ? FIX THIS
specLazy :: CGInfo -> !(HashSet Var)

-- | ? FIX THIS
autoSize :: CGInfo -> !(HashSet TyCon)

-- | primitive Sorts into which TyCons should be embedded
tyConEmbed :: CGInfo -> !(TCEmb TyCon)

-- | Fixpoint Kut variables (denoting "back-edges"/recursive KVars)
kuts :: CGInfo -> !(Kuts)

-- | ? FIX THIS
lits :: CGInfo -> ![(Symbol, Sort)]

-- | Check Termination (?)
tcheck :: CGInfo -> !Bool

-- | Check Strata (?)
scheck :: CGInfo -> !Bool

-- | Trust ghc auto generated bindings
trustghc :: CGInfo -> !Bool

-- | prune unsorted refinements
pruneRefs :: CGInfo -> !Bool

-- | Errors during constraint generation
logErrors :: CGInfo -> ![TError SpecType]

-- | Profiling distribution of KVars
kvProf :: CGInfo -> !KVProf

-- | number of recursive functions seen (for benchmarks)
recCount :: CGInfo -> !Int

-- | Source Span associated with Fixpoint Binder
bindSpans :: CGInfo -> HashMap BindId SrcSpan
pprCGInfo :: t -> Doc
newtype HEnv
HEnv :: (HashSet Symbol) -> HEnv
fromListHEnv :: [Symbol] -> HEnv
elemHEnv :: Symbol -> HEnv -> Bool
type RTyConInv = HashMap RTyCon [SpecType]
type RTyConIAl = HashMap RTyCon [SpecType]
mkRTyConInv :: [Located SpecType] -> RTyConInv
mkRTyConIAl :: [(a, Located SpecType)] -> RTyConInv
addRTyConInv :: RTyConInv -> SpecType -> SpecType
addRInv :: RTyConInv -> (Var, SpecType) -> (Var, SpecType)
conjoinInvariantShift :: RType RTyCon tv RReft -> SpecType -> RType RTyCon tv RReft
conjoinInvariant :: RType RTyCon tv RReft -> SpecType -> RType RTyCon tv RReft
grapBindsWithType :: RType RTyCon RTyVar r -> CGEnv -> [Symbol]
toListREnv :: REnv -> [(Symbol, SpecType)]
filterREnv :: (SpecType -> Bool) -> REnv -> REnv
fromListREnv :: [(Symbol, SpecType)] -> REnv
deleteREnv :: Symbol -> REnv -> REnv
insertREnv :: Symbol -> SpecType -> REnv -> REnv
lookupREnv :: Symbol -> REnv -> Maybe SpecType
memberREnv :: Symbol -> REnv -> Bool
data FEnv
FE :: !IBindEnv -> !(SEnv Sort) -> FEnv

-- | Integer Keys for Fixpoint Environment
fe_binds :: FEnv -> !IBindEnv

-- | Fixpoint Environment
fe_env :: FEnv -> !(SEnv Sort)
insertFEnv :: FEnv -> ((Symbol, Sort), BindId) -> FEnv
insertsFEnv :: FEnv -> [((Symbol, Sort), BindId)] -> FEnv
initFEnv :: [(Symbol, Sort)] -> FEnv
instance PPrint CGInfo
instance SubStratum SubC
instance PPrint WfC
instance PPrint SubC
instance Show CGEnv
instance PPrint CGEnv

module Language.Haskell.Liquid.Constraint.Constraint
typeToConstraint :: [(Symbol, SpecType)] -> LConstraint
addConstraints :: [(Symbol, SpecType)] -> CGEnv -> CGEnv
constraintToLogic :: CGEnv -> LConstraint -> Pred
constraintToLogicOne :: Reftable r => CGEnv -> [(Symbol, RType RTyCon RTyVar r)] -> Pred
subConstraintToLogicOne :: (Reftable r1, Reftable r) => [(Symbol, (Symbol, RType t t1 r))] -> (Symbol, (Symbol, RType t2 t3 r1)) -> Pred
combinations :: [[a]] -> [[a]]
instance Monoid LConstraint

module Language.Haskell.Liquid.Bounds
data Bound t e
Bound :: LocSymbol -> [t] -> [(LocSymbol, t)] -> [(LocSymbol, t)] -> e -> Bound t e

-- | The name of the bound
bname :: Bound t e -> LocSymbol

-- | Type variables that appear in the bounds
tyvars :: Bound t e -> [t]

-- | These are abstract refinements, for now
bparams :: Bound t e -> [(LocSymbol, t)]

-- | These are value variables
bargs :: Bound t e -> [(LocSymbol, t)]

-- | The body of the bound
bbody :: Bound t e -> e
type RBound = RRBound RSort
type RRBound tv = Bound tv Pred
type RBEnv = HashMap LocSymbol RBound
type RRBEnv tv = HashMap LocSymbol (RRBound tv)
makeBound :: (PPrint r, UReftable r) => RRBound RSort -> [RRType r] -> [Symbol] -> (RRType r) -> (RRType r)
envToSub :: [(t, t1)] -> ([(t, t1)], t1, t1)
instance Bifunctor Bound
instance (PPrint e, PPrint t) => PPrint (Bound t e)
instance (PPrint e, PPrint t) => Show (Bound t e)
instance Eq (Bound t e)
instance Hashable (Bound t e)

module Language.Haskell.Liquid.Measure
data Spec ty bndr
Spec :: ![Measure ty bndr] -> ![(LocSymbol, ty)] -> ![(LocSymbol, ty)] -> ![(LocSymbol, ty)] -> ![Located ty] -> ![(Located ty, Located ty)] -> ![Symbol] -> ![DataDecl] -> ![FilePath] -> ![RTAlias Symbol BareType] -> ![RTAlias Symbol Pred] -> ![RTAlias Symbol Expr] -> !(TCEmb (LocSymbol)) -> ![Qualifier] -> ![(LocSymbol, [Int])] -> ![(LocSymbol)] -> !(HashSet LocSymbol) -> !(HashSet LocSymbol) -> !(HashSet LocSymbol) -> !(HashSet LocSymbol) -> !(HashSet LocSymbol) -> ![Located String] -> ![Measure ty ()] -> ![Measure ty bndr] -> ![RClass ty] -> ![(LocSymbol, [Expr])] -> ![RInstance ty] -> ![(LocSymbol, [Variance])] -> !(RRBEnv ty) -> Spec ty bndr

-- | User-defined properties for ADTs
measures :: Spec ty bndr -> ![Measure ty bndr]

-- | Assumed (unchecked) types
asmSigs :: Spec ty bndr -> ![(LocSymbol, ty)]

-- | Imported functions and types
sigs :: Spec ty bndr -> ![(LocSymbol, ty)]

-- | Local type signatures
localSigs :: Spec ty bndr -> ![(LocSymbol, ty)]

-- | Data type invariants
invariants :: Spec ty bndr -> ![Located ty]

-- | Data type invariants to be checked
ialiases :: Spec ty bndr -> ![(Located ty, Located ty)]

-- | Loaded spec module names
imports :: Spec ty bndr -> ![Symbol]

-- | Predicated data definitions
dataDecls :: Spec ty bndr -> ![DataDecl]

-- | Included qualifier files
includes :: Spec ty bndr -> ![FilePath]

-- | RefType aliases
aliases :: Spec ty bndr -> ![RTAlias Symbol BareType]

-- | Refinement/Predicate aliases
paliases :: Spec ty bndr -> ![RTAlias Symbol Pred]

-- | Expression aliases
ealiases :: Spec ty bndr -> ![RTAlias Symbol Expr]

-- | GHC-Tycon-to-fixpoint Tycon map
embeds :: Spec ty bndr -> !(TCEmb (LocSymbol))

-- | Qualifiers in source/spec files
qualifiers :: Spec ty bndr -> ![Qualifier]

-- | Information on decreasing arguments
decr :: Spec ty bndr -> ![(LocSymbol, [Int])]

-- | Variables that should be checked in the environment they are used
lvars :: Spec ty bndr -> ![(LocSymbol)]

-- | Ignore Termination Check in these Functions
lazy :: Spec ty bndr -> !(HashSet LocSymbol)

-- | Binders to turn into measures using haskell definitions
hmeas :: Spec ty bndr -> !(HashSet LocSymbol)

-- | Binders to turn into bounds using haskell definitions
hbounds :: Spec ty bndr -> !(HashSet LocSymbol)

-- | Binders to turn into logic inline using haskell definitions
inlines :: Spec ty bndr -> !(HashSet LocSymbol)

-- | Type Constructors that get automatically sizing info
autosize :: Spec ty bndr -> !(HashSet LocSymbol)

-- | Command-line configurations passed in through source
pragmas :: Spec ty bndr -> ![Located String]

-- | Measures attached to a type-class
cmeasures :: Spec ty bndr -> ![Measure ty ()]

-- | Mappings from (measure,type) -&gt; measure
imeasures :: Spec ty bndr -> ![Measure ty bndr]

-- | Refined Type-Classes
classes :: Spec ty bndr -> ![RClass ty]

-- | Terminating Conditions for functions
termexprs :: Spec ty bndr -> ![(LocSymbol, [Expr])]
rinstance :: Spec ty bndr -> ![RInstance ty]
dvariance :: Spec ty bndr -> ![(LocSymbol, [Variance])]
bounds :: Spec ty bndr -> !(RRBEnv ty)
type BareSpec = Spec BareType LocSymbol
data MSpec ty ctor
MSpec :: HashMap Symbol [Def ty ctor] -> HashMap LocSymbol (Measure ty ctor) -> HashMap LocSymbol (Measure ty ()) -> ![Measure ty ctor] -> MSpec ty ctor
ctorMap :: MSpec ty ctor -> HashMap Symbol [Def ty ctor]
measMap :: MSpec ty ctor -> HashMap LocSymbol (Measure ty ctor)
cmeasMap :: MSpec ty ctor -> HashMap LocSymbol (Measure ty ())
imeas :: MSpec ty ctor -> ![Measure ty ctor]
mkM :: LocSymbol -> ty -> [Def ty bndr] -> Measure ty bndr
mkMSpec :: [Measure ty (Located Symbol)] -> [Measure ty ()] -> [Measure ty (Located Symbol)] -> MSpec ty (Located Symbol)
mkMSpec' :: Symbolic ctor => [Measure ty ctor] -> MSpec ty ctor
qualifySpec :: Symbol -> Spec ty bndr -> Spec ty bndr
mapTy :: (tya -> tyb) -> Measure tya c -> Measure tyb c
dataConTypes :: MSpec (RRType Reft) DataCon -> ([(Var, RRType Reft)], [(LocSymbol, RRType Reft)])
defRefType :: Def (RRType Reft) DataCon -> RRType Reft

-- | A wired-in measure <tt>strLen</tt> that describes the length of a
--   string literal, with type <tt>Addr#</tt>.
strLen :: Measure SpecType ctor
wiredInMeasures :: MSpec SpecType DataCon
instance PPrint (CMeasure t) => Show (CMeasure t)
instance PPrint t => PPrint (CMeasure t)
instance PPrint (Measure t a) => Show (Measure t a)
instance (PPrint t, PPrint a) => PPrint (MSpec t a)
instance (PPrint t, PPrint a) => PPrint (Measure t a)
instance PPrint a => PPrint (Def t a)
instance PPrint Body
instance Bifunctor Spec
instance Bifunctor MSpec
instance Bifunctor Measure
instance Bifunctor Def
instance Functor (MSpec t)
instance Functor CMeasure
instance Functor (Measure t)
instance Functor (Def t)
instance Monoid (Spec ty bndr)
instance Eq ctor => Monoid (MSpec ty ctor)
instance (Show ty, Show ctor, PPrint ctor, PPrint ty) => Show (MSpec ty ctor)

module Language.Haskell.Liquid.Parse
hsSpecificationP :: SourceName -> String -> Either Error (ModName, BareSpec)
lhsSpecificationP :: SourceName -> String -> Either Error (ModName, BareSpec)

-- | Used to parse .spec files
specSpecificationP :: SourceName -> String -> Either Error (ModName, BareSpec)
parseSymbolToLogic :: SourceName -> String -> Either Error (HashMap Symbol LMap)
instance Inputable (Measure BareType LocSymbol)
instance Inputable BareType
instance Show (Pspec a b)


-- | This module contains functions for cleaning up types before they are
--   rendered, e.g. in error messages or annoations.
module Language.Haskell.Liquid.Tidy
tidySpecType :: Tidy -> SpecType -> SpecType
tidySymbol :: Symbol -> Symbol
isTmpSymbol :: Symbol -> Bool

module Language.Haskell.Liquid.WiredIn

-- | LH Primitive TyCons ----------------------------------------------
propTyCon :: TyCon

-- | LH Primitive TyCons ----------------------------------------------
hpropTyCon :: TyCon

-- | LH Primitive Types ----------------------------------------------
propType :: Reftable r => RRType r
maxArity :: Arity
wiredTyCons :: [(TyCon, TyConP)]
wiredDataCons :: [(DataCon, Located DataConP)]
wiredTyDataCons :: ([(TyCon, TyConP)], [(DataCon, Located DataConP)])
listTyDataCons :: ([(TyCon, TyConP)], [(DataCon, DataConP)])
tupleTyDataCons :: Int -> ([(TyCon, TyConP)], [(DataCon, DataConP)])
pdVarReft :: PVar t -> UReft Reft
mkps :: [Symbol] -> [t] -> [(Symbol, Expr)] -> [PVar t]
mkps_ :: [Symbol] -> [t] -> [(Symbol, Expr)] -> [(t, Symbol, Expr)] -> [PVar t] -> [PVar t]

module Language.Haskell.Liquid.CoreToLogic
coreToDef :: Reftable r => LocSymbol -> Var -> CoreExpr -> LogicM [Def (RRType r) DataCon]
coreToFun :: LocSymbol -> Var -> CoreExpr -> LogicM ([Var], Either Pred Expr)
mkLit :: Literal -> Maybe Expr
runToLogic :: LogicMap -> (String -> Error) -> LogicM t -> Either t Error
logicType :: Reftable r => Type -> RRType r
strengthenResult :: Var -> SpecType
instance Simplify CoreAlt
instance Simplify CoreBind
instance Simplify CoreExpr
instance Show CoreExpr
instance Applicative LogicM
instance Functor LogicM
instance Monad LogicM

module Language.Haskell.Liquid.Literals
literalFRefType :: Literal -> RType RTyCon RTyVar Reft
literalFReft :: Literal -> Reft

-- | <a>literalConst</a> returns <a>Nothing</a> for unhandled lits because
--   otherwise string-literals show up as global int-constants which blow
--   up qualifier instantiation.
literalConst :: TCEmb TyCon -> Literal -> (Sort, Maybe Expr)

module Language.Haskell.Liquid.Bare.SymSort
txRefSort :: (PPrint t, Reftable t) => HashMap TyCon RTyCon -> HashMap TyCon FTycon -> RType RTyCon RTyVar (UReft t) -> RType RTyCon RTyVar (UReft t)

module Language.Haskell.Liquid.Bare.Existential

-- | Niki: please write more documentation for this, maybe an example? I
--   can't really tell whats going on... (RJ)
txExpToBind :: SpecType -> SpecType

module Language.Haskell.Liquid.Dictionaries
makeDictionaries :: [RInstance SpecType] -> DEnv Symbol SpecType
makeDictionary :: RInstance SpecType -> (Symbol, HashMap Symbol SpecType)
dfromList :: [(Var, HashMap Symbol t)] -> DEnv Var t
dmapty :: (a -> b) -> DEnv v a -> DEnv v b
dmap :: (v1 -> v2) -> HashMap k v1 -> HashMap k v2
dinsert :: (Hashable x, Eq x) => DEnv x ty -> x -> HashMap Symbol ty -> DEnv x ty
dlookup :: (Hashable k, Eq k) => DEnv k t -> k -> Maybe (HashMap Symbol t)
dhasinfo :: Show a1 => Maybe (HashMap Symbol a) -> a1 -> Maybe a

module Language.Haskell.Liquid.RefSplit
splitXRelatedRefs :: Symbol -> SpecType -> (SpecType, SpecType)
instance Show (UReft Reft)
instance Subable x => IsFree x


-- | This module defines the representation of Subtyping and WF
--   Constraints, and the code for syntax-directed constraint generation.
module Language.Haskell.Liquid.Constraint.Generate
generateConstraints :: GhcInfo -> CGInfo
instance Show a => Show (Template a)
instance Functor Template
instance Foldable Template
instance Traversable Template
instance NFData REnv
instance NFData CGInfo
instance NFData WfC
instance NFData Type
instance NFData RTyCon
instance NFData Class
instance NFData SubC
instance NFData FEnv
instance NFData CGEnv
instance Freshable CG Integer


-- | This module contains the functions related to <tt>Error</tt> type, in
--   particular, to <tt>tidyError</tt> using a solution, and
--   <tt>pprint</tt> errors.
module Language.Haskell.Liquid.Errors
tidyError :: FixSolution -> Error -> Error

-- | Throw a panic exception
exitWithPanic :: String -> a
instance FromJSON Error
instance ToJSON Error
instance Exception [Error]
instance Exception Error
instance Show Error
instance PPrint Error


-- | This module contains the code for Incremental checking, which finds
--   the part of a target file (the subset of the <tt>[CoreBind]</tt> that
--   have been modified since it was last checked, as determined by a diff
--   against a saved version of the file.
module Language.Haskell.Liquid.DiffCheck

-- | Main type of value returned for diff-check.
data DiffCheck
DC :: [CoreBind] -> !(Output Doc) -> !GhcSpec -> DiffCheck
newBinds :: DiffCheck -> [CoreBind]
oldOutput :: DiffCheck -> !(Output Doc)
newSpec :: DiffCheck -> !GhcSpec

-- | <a>slice</a> returns a subset of the <tt>[CoreBind]</tt> of the input
--   <tt>target</tt> file which correspond to top-level binders whose code
--   has changed and their transitive dependencies.
slice :: FilePath -> [CoreBind] -> GhcSpec -> IO (Maybe DiffCheck)

-- | <tt>thin</tt> returns a subset of the <tt>[CoreBind]</tt> given which
--   correspond to those binders that depend on any of the <tt>Var</tt>s
--   provided.
thin :: [CoreBind] -> [Var] -> [CoreBind]

-- | <tt>save</tt> creates an .saved version of the <tt>target</tt> file,
--   which will be used to find what has changed the <i>next time</i>
--   <tt>target</tt> is checked.
saveResult :: FilePath -> Output Doc -> IO ()
instance Eq Def
instance Ord Def
instance FromJSON (Output Doc)
instance ToJSON (Output Doc)
instance FromJSON a => FromJSON (AnnInfo a)
instance ToJSON a => ToJSON (AnnInfo a)
instance (Eq k, Hashable k, FromJSON k, FromJSON v) => FromJSON (HashMap k v)
instance (ToJSON k, ToJSON v) => ToJSON (HashMap k v)
instance FromJSON Doc
instance ToJSON Doc
instance FromJSON (FixResult Error)
instance ToJSON (FixResult Error)
instance FromJSON SourcePos
instance ToJSON SourcePos
instance Functor Diff
instance Show Def


-- | This module contains a single function that extracts the cabal
--   information about a target file, if any. This information can be used
--   to extend the source-directories that are searched to find modules
--   that are imported by the target file.
module Language.Haskell.Liquid.Cabal
cabalInfo :: FilePath -> IO (Maybe Info)
data Info
Info :: FilePath -> [FilePath] -> [FilePath] -> [Extension] -> [String] -> [String] -> [String] -> FilePath -> Info
cabalFile :: Info -> FilePath
buildDirs :: Info -> [FilePath]
sourceDirs :: Info -> [FilePath]
exts :: Info -> [Extension]
otherOptions :: Info -> [String]
packageDbs :: Info -> [String]
packageDeps :: Info -> [String]
macroPath :: Info -> FilePath
instance Show Info

module Language.Haskell.Liquid.Bare.Env

-- | Error-Reader-IO For Bare Transformation
--   --------------------------------------
type BareM = WriterT [Warn] (ErrorT Error (StateT BareEnv IO))
type Warn = String
type TCEnv = HashMap TyCon RTyCon
data BareEnv
BE :: !ModName -> !TCEnv -> !RTEnv -> ![(Symbol, Var)] -> HscEnv -> LogicMap -> InlnEnv -> RBEnv -> BareEnv
modName :: BareEnv -> !ModName
tcEnv :: BareEnv -> !TCEnv
rtEnv :: BareEnv -> !RTEnv
varEnv :: BareEnv -> ![(Symbol, Var)]
hscEnv :: BareEnv -> HscEnv
logicEnv :: BareEnv -> LogicMap
inlines :: BareEnv -> InlnEnv
bounds :: BareEnv -> RBEnv
data TInline
TI :: [Symbol] -> Either Pred Expr -> TInline
tiargs :: TInline -> [Symbol]
tibody :: TInline -> Either Pred Expr
type InlnEnv = HashMap Symbol TInline
inModule :: MonadState BareEnv m => ModName -> m b -> m b
withVArgs :: (PPrint a, MonadState BareEnv m) => SourcePos -> SourcePos -> [a] -> m b -> m b
setRTAlias :: MonadState BareEnv m => Symbol -> RTAlias RTyVar SpecType -> m ()
setRPAlias :: MonadState BareEnv m => Symbol -> RTAlias Symbol Pred -> m ()
setREAlias :: MonadState BareEnv m => Symbol -> RTAlias Symbol Expr -> m ()
execBare :: BareM a -> BareEnv -> IO (Either Error a)
instance Show TInline

module Language.Haskell.Liquid.Bare.RefToLogic
class Transformable a where tx' lmap imap x = foldrWithKey tx x limap where limap = fromList ((mapSnd Left <$> toList lmap) ++ (mapSnd Right <$> toList imap))
txRefToLogic :: Transformable r => LogicMap -> InlnEnv -> r -> r
instance Transformable Body
instance Transformable (Def t c)
instance Transformable (Measure t c)
instance Transformable Expr
instance Transformable Pred
instance (Transformable a, Transformable b) => Transformable (Either a b)
instance Transformable Reft
instance Transformable RReft
instance Transformable r => Transformable (RType c v r)
instance Transformable TInline
instance Transformable DataConP
instance Transformable a => Transformable [a]

module Language.Haskell.Liquid.Bare.Lookup
class Symbolic a => GhcLookup a
lookupName :: GhcLookup a => HscEnv -> ModName -> a -> IO [Name]
srcSpan :: GhcLookup a => a -> SrcSpan
lookupGhcThing :: (GhcLookup a, MonadState BareEnv m, MonadError (TError t) m, MonadIO m) => [Char] -> (TyThing -> Maybe b) -> a -> m b

-- | It's possible that we have already resolved the <a>Name</a> we are
--   looking for, but have had to turn it back into a <a>String</a>, e.g.
--   to be used in an <tt>Expr</tt>, as in <tt>{v:Ordering | v = EQ}</tt>.
--   In this case, the fully-qualified <a>Name</a> (<tt>GHC.Types.EQ</tt>)
--   will likely not be in scope, so we store our own mapping of
--   fully-qualified <a>Name</a>s to <a>Var</a>s and prefer pulling
--   <a>Var</a>s from it.
lookupGhcVar :: GhcLookup a => a -> BareM Var
lookupGhcTyCon :: GhcLookup a => a -> BareM TyCon
lookupGhcDataCon :: (MonadState BareEnv m, MonadError (TError t) m, MonadIO m) => Located Symbol -> m DataCon
instance GhcLookup Name
instance GhcLookup (Located Symbol)

module Language.Haskell.Liquid.Bare.Expand
expandReft :: RReft -> BareM RReft
expandPred :: Pred -> BareM Pred
expandExpr :: Expr -> BareM Expr

module Language.Haskell.Liquid.Bare.Misc
makeSymbols :: (TyConable c2, TyConable c1, TyConable c, MonadState BareEnv m, Reftable r2, Reftable r1, Reftable r) => [Var] -> [Symbol] -> [(a1, Located (RType c2 tv2 r2))] -> [(a, Located (RType c1 tv1 r1))] -> [Located (RType c tv r)] -> m [(Symbol, Var)]
joinVar :: [Var] -> (Var, s, t) -> (Var, s, t)
mkVarExpr :: Var -> Expr
data MapTyVarST
MTVST :: [(Var, RTyVar)] -> Error -> MapTyVarST
vmap :: MapTyVarST -> [(Var, RTyVar)]
errmsg :: MapTyVarST -> Error
initMapSt :: Error -> MapTyVarST
runMapTyVars :: StateT MapTyVarST (Either Error) () -> MapTyVarST -> Either Error MapTyVarST
mapTyVars :: (PPrint r, Reftable r) => Type -> RRType r -> StateT MapTyVarST (Either Error) ()
symbolRTyVar :: Symbol -> RTyVar
simpleSymbolVar :: Var -> Symbol
hasBoolResult :: Type -> Bool

module Language.Haskell.Liquid.Bare.Plugged
makePluggedSigs :: ModName -> TCEmb TyCon -> HashMap TyCon RTyCon -> NameSet -> [(Var, Located (RRType RReft))] -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) [(Var, Located (RType RTyCon RTyVar RReft))]
makePluggedAsmSigs :: TCEmb TyCon -> HashMap TyCon RTyCon -> [(Var, Located (RRType RReft))] -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) [(Var, Located (RType RTyCon RTyVar RReft))]
makePluggedDataCons :: TCEmb TyCon -> HashMap TyCon RTyCon -> [(DataCon, Located DataConP)] -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) [(DataCon, Located DataConP)]

module Language.Haskell.Liquid.Bare.Resolve
class Resolvable a
resolve :: Resolvable a => SourcePos -> a -> BareM a
instance Resolvable ()
instance Resolvable t => Resolvable (PVar t)
instance Resolvable Predicate
instance Resolvable Reft
instance Resolvable (UReft Reft)
instance Resolvable Sort
instance Resolvable Symbol
instance Resolvable LocSymbol
instance Resolvable Expr
instance Resolvable Pred
instance Resolvable Qualifier
instance Resolvable a => Resolvable [a]

module Language.Haskell.Liquid.Bare.OfType
ofBareType :: SourcePos -> BareType -> BareM SpecType
ofMeaSort :: BareType -> BareM SpecType
ofBSort :: BSort -> BareM RSort
ofBPVar :: BPVar -> BareM RPVar
mkSpecType :: SourcePos -> BareType -> BareM SpecType
mkSpecType' :: SourcePos -> [PVar BSort] -> BareType -> BareM SpecType

module Language.Haskell.Liquid.Bare.DataType
makeConTypes :: (ModName, Spec ty bndr) -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) ([(TyCon, TyConP)], [[(DataCon, Located DataConP)]])
makeTyConEmbeds :: (ModName, Spec ty bndr) -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) (TCEmb TyCon)
dataConSpec :: [(DataCon, DataConP)] -> [(Var, RType RTyCon RTyVar RReft)]
meetDataConSpec :: [(Var, RType RTyCon RTyVar RReft)] -> [(DataCon, DataConP)] -> [(Var, RType RTyCon RTyVar RReft)]

module Language.Haskell.Liquid.Bare.Measure
makeHaskellMeasures :: [CoreBind] -> ModName -> (ModName, BareSpec) -> BareM (MSpec SpecType DataCon)
makeHaskellInlines :: [CoreBind] -> ModName -> (ModName, BareSpec) -> BareM ()
makeHaskellBounds :: CoreProgram -> HashSet (Var, LocSymbol) -> BareM RBEnv
makeMeasureSpec :: (ModName, Spec BareType LocSymbol) -> BareM (MSpec SpecType DataCon)
makeMeasureSpec' :: MSpec (RType RTyCon RTyVar (UReft Reft)) DataCon -> ([(Var, RType RTyCon RTyVar (UReft Reft))], [(LocSymbol, RRType Reft)])
makeClassMeasureSpec :: MSpec (RType c tv (UReft r2)) t -> [(LocSymbol, CMeasure (RType c tv r2))]
makeMeasureSelectors :: (DataCon, Located DataConP) -> [Measure SpecType DataCon]
strengthenHaskellMeasures :: HashSet (Located Var) -> [(Var, Located SpecType)]
varMeasures :: Monoid r => [Id] -> [(Symbol, Located (RType RTyCon RTyVar r))]

module Language.Haskell.Liquid.Bare.RTEnv
makeRTEnv :: [(ModName, Spec ty bndr)] -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) ()

module Language.Haskell.Liquid.Bare.Spec
makeClasses :: ModName -> Config -> [Var] -> (ModName, Spec BareType bndr) -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) [((DataCon, DataConP), [(ModName, Var, Located SpecType)])]
makeQualifiers :: (ModName, Spec ty bndr) -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) [Qualifier]
makeHints :: [Var] -> Spec ty bndr -> BareM [(Var, [Int])]
makeLVar :: [Var] -> Spec ty bndr -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) [Var]
makeLazy :: [Var] -> Spec ty bndr -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) [Var]
makeHIMeas :: [Var] -> Spec ty bndr -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) [Located Var]
makeTExpr :: [Var] -> Spec ty bndr -> BareM [(Var, [Expr])]

-- | API: Bare Refinement Types ----------------------------------
makeTargetVars :: ModName -> [Var] -> [String] -> BareM [Var]
makeAssertSpec :: ModName -> Config -> [Var] -> [Var] -> (ModName, Spec BareType bndr) -> BareM [(ModName, Var, Located SpecType)]
makeAssumeSpec :: ModName -> Config -> [Var] -> [Var] -> (ModName, Spec BareType bndr) -> BareM [(ModName, Var, Located SpecType)]
makeDefaultMethods :: [Var] -> [(ModName, Var, Located SpecType)] -> [(ModName, Var, Located SpecType)]
makeIAliases :: (ModName, Spec BareType bndr) -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) [(Located SpecType, Located SpecType)]
makeInvariants :: (ModName, Spec BareType bndr) -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) [Located SpecType]
makeSpecDictionaries :: HashMap TyCon FTycon -> [Var] -> [(t, Spec BareType bndr)] -> GhcSpec -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) GhcSpec
makeBounds :: Eq a => a -> [Var] -> CoreProgram -> [(a, Spec BareType bndr)] -> WriterT [Warn] (ErrorT Error (StateT BareEnv IO)) ()
makeHBounds :: [Var] -> Spec ty bndr -> BareM [(Var, LocSymbol)]


-- | This module contains the code that uses the inferred types to generate
--   1. HTMLized source with Inferred Types in mouseover annotations. 2.
--   Annotations files (e.g. for vim/emacs) 3. JSON files for the web-demo
--   etc.
module Language.Haskell.Liquid.Annotate

-- | <tt>output</tt> creates the pretty printed output
mkOutput :: Config -> FixResult Error -> FixSolution -> AnnInfo (Annot SpecType) -> Output Doc

-- | <tt>annotate</tt> actually renders the output to files
annotate :: Config -> FilePath -> Output Doc -> IO ()
instance ToJSON AnnMap
instance (Show k, ToJSON a) => ToJSON (Assoc k a)
instance ToJSON AnnErrors
instance ToJSON Loc
instance ToJSON Annot1
instance ToJSON Status


-- | This module contains all the code needed to output the result which is
--   either: <tt>SAFE</tt> or <tt>WARNING</tt> with some reasonable error
--   message when something goes wrong. All forms of errors/exceptions
--   should go through here. The idea should be to report the error, the
--   source position that causes it, generate a suitable .json file and
--   then exit.
module Language.Haskell.Liquid.CmdLine
getOpts :: IO Config
mkOpts :: Config -> IO Config

-- | Updating options
withPragmas :: Config -> FilePath -> [Located String] -> IO Config
withCabal :: Config -> IO Config

-- | Exit Function -----------------------------------------------------
exitWithResult :: Config -> FilePath -> Output Doc -> IO (Output Doc)

-- | check subset of binders modified (+ dependencies) since last check
diffcheck :: Config -> Bool
instance Fixpoint (FixResult Error)
instance Monoid SMTSolver
instance Monoid Config

module Language.Haskell.Liquid.Bare.Check
checkGhcSpec :: [(ModName, BareSpec)] -> SEnv SortedReft -> GhcSpec -> Either [Error] GhcSpec
checkTerminationExpr :: (Eq v, PPrint v) => TCEmb TyCon -> SEnv SortedReft -> (v, Located SpecType, [Expr]) -> Maybe Error
checkTy :: (Doc -> Error) -> TCEmb TyCon -> TCEnv -> SEnv SortedReft -> SpecType -> Maybe Error

module Language.Haskell.Liquid.Bare.GhcSpec

-- | The following is the overall type for <i>specifications</i> obtained
--   from parsing the target source and dependent libraries
data GhcSpec
SP :: ![(Var, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Symbol, Located SpecType)] -> ![Located SpecType] -> ![(Located SpecType, Located SpecType)] -> ![(DataCon, DataConP)] -> ![(TyCon, TyConP)] -> ![(Symbol, Var)] -> TCEmb TyCon -> ![Qualifier] -> ![Var] -> ![(Var, [Int])] -> ![(Var, [Expr])] -> !(HashSet Var) -> !(HashSet Var) -> !(HashSet TyCon) -> !Config -> !NameSet -> [Measure SpecType DataCon] -> HashMap TyCon RTyCon -> DEnv Var SpecType -> GhcSpec

-- | Asserted Reftypes eg. see include/Prelude.spec
tySigs :: GhcSpec -> ![(Var, Located SpecType)]

-- | Assumed Reftypes
asmSigs :: GhcSpec -> ![(Var, Located SpecType)]

-- | Data Constructor Measure Sigs eg. (:) :: a -&gt; xs:[a] -&gt; {v: Int
--   | v = 1 + len(xs) }
ctors :: GhcSpec -> ![(Var, Located SpecType)]

-- | Measure Types eg. len :: [a] -&gt; Int
meas :: GhcSpec -> ![(Symbol, Located SpecType)]

-- | Data Type Invariants eg. forall a. {v: [a] | len(v) &gt;= 0}
invariants :: GhcSpec -> ![Located SpecType]

-- | Data Type Invariant Aliases
ialiases :: GhcSpec -> ![(Located SpecType, Located SpecType)]

-- | Predicated Data-Constructors e.g. see tests<i>pos</i>Map.hs
dconsP :: GhcSpec -> ![(DataCon, DataConP)]

-- | Predicated Type-Constructors eg. see tests<i>pos</i>Map.hs
tconsP :: GhcSpec -> ![(TyCon, TyConP)]

-- | List of <a>Symbol</a> free in spec and corresponding GHC var eg.
--   (Cons, Cons#7uz) from tests<i>pos</i>ex1.hs
freeSyms :: GhcSpec -> ![(Symbol, Var)]

-- | How to embed GHC Tycons into fixpoint sorts e.g. "embed Set as
--   Set_set" from include<i>Data</i>Set.spec
tcEmbeds :: GhcSpec -> TCEmb TyCon

-- | Qualifiers in Source/Spec files e.g tests<i>pos</i>qualTest.hs
qualifiers :: GhcSpec -> ![Qualifier]

-- | Top-level Binders To Verify (empty means ALL binders)
tgtVars :: GhcSpec -> ![Var]

-- | Lexicographically ordered size witnesses for termination
decr :: GhcSpec -> ![(Var, [Int])]

-- | Lexicographically ordered expressions for termination
texprs :: GhcSpec -> ![(Var, [Expr])]

-- | Variables that should be checked in the environment they are used
lvars :: GhcSpec -> !(HashSet Var)

-- | Binders to IGNORE during termination checking
lazy :: GhcSpec -> !(HashSet Var)

-- | Binders to IGNORE during termination checking
autosize :: GhcSpec -> !(HashSet TyCon)

-- | Configuration Options
config :: GhcSpec -> !Config

-- | <tt>Name</tt>s exported by the module being verified
exports :: GhcSpec -> !NameSet
measures :: GhcSpec -> [Measure SpecType DataCon]
tyconEnv :: GhcSpec -> HashMap TyCon RTyCon

-- | Dictionary Environment
dicts :: GhcSpec -> DEnv Var SpecType
makeGhcSpec :: Config -> ModName -> [CoreBind] -> [Var] -> [Var] -> NameSet -> HscEnv -> Either Error LogicMap -> [(ModName, BareSpec)] -> IO GhcSpec


-- | This module contains the functions that convert <i>from</i>
--   descriptions of symbols, names and types (over freshly parsed
--   <i>bare</i> Strings), <i>to</i> representations connected to GHC vars,
--   names, and types. The actual <i>representations</i> of bare and real
--   (refinement) types are all in <tt>RefType</tt> -- they are different
--   instances of <tt>RType</tt>
module Language.Haskell.Liquid.Bare

-- | The following is the overall type for <i>specifications</i> obtained
--   from parsing the target source and dependent libraries
data GhcSpec
SP :: ![(Var, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Symbol, Located SpecType)] -> ![Located SpecType] -> ![(Located SpecType, Located SpecType)] -> ![(DataCon, DataConP)] -> ![(TyCon, TyConP)] -> ![(Symbol, Var)] -> TCEmb TyCon -> ![Qualifier] -> ![Var] -> ![(Var, [Int])] -> ![(Var, [Expr])] -> !(HashSet Var) -> !(HashSet Var) -> !(HashSet TyCon) -> !Config -> !NameSet -> [Measure SpecType DataCon] -> HashMap TyCon RTyCon -> DEnv Var SpecType -> GhcSpec

-- | Asserted Reftypes eg. see include/Prelude.spec
tySigs :: GhcSpec -> ![(Var, Located SpecType)]

-- | Assumed Reftypes
asmSigs :: GhcSpec -> ![(Var, Located SpecType)]

-- | Data Constructor Measure Sigs eg. (:) :: a -&gt; xs:[a] -&gt; {v: Int
--   | v = 1 + len(xs) }
ctors :: GhcSpec -> ![(Var, Located SpecType)]

-- | Measure Types eg. len :: [a] -&gt; Int
meas :: GhcSpec -> ![(Symbol, Located SpecType)]

-- | Data Type Invariants eg. forall a. {v: [a] | len(v) &gt;= 0}
invariants :: GhcSpec -> ![Located SpecType]

-- | Data Type Invariant Aliases
ialiases :: GhcSpec -> ![(Located SpecType, Located SpecType)]

-- | Predicated Data-Constructors e.g. see tests<i>pos</i>Map.hs
dconsP :: GhcSpec -> ![(DataCon, DataConP)]

-- | Predicated Type-Constructors eg. see tests<i>pos</i>Map.hs
tconsP :: GhcSpec -> ![(TyCon, TyConP)]

-- | List of <a>Symbol</a> free in spec and corresponding GHC var eg.
--   (Cons, Cons#7uz) from tests<i>pos</i>ex1.hs
freeSyms :: GhcSpec -> ![(Symbol, Var)]

-- | How to embed GHC Tycons into fixpoint sorts e.g. "embed Set as
--   Set_set" from include<i>Data</i>Set.spec
tcEmbeds :: GhcSpec -> TCEmb TyCon

-- | Qualifiers in Source/Spec files e.g tests<i>pos</i>qualTest.hs
qualifiers :: GhcSpec -> ![Qualifier]

-- | Top-level Binders To Verify (empty means ALL binders)
tgtVars :: GhcSpec -> ![Var]

-- | Lexicographically ordered size witnesses for termination
decr :: GhcSpec -> ![(Var, [Int])]

-- | Lexicographically ordered expressions for termination
texprs :: GhcSpec -> ![(Var, [Expr])]

-- | Variables that should be checked in the environment they are used
lvars :: GhcSpec -> !(HashSet Var)

-- | Binders to IGNORE during termination checking
lazy :: GhcSpec -> !(HashSet Var)

-- | Binders to IGNORE during termination checking
autosize :: GhcSpec -> !(HashSet TyCon)

-- | Configuration Options
config :: GhcSpec -> !Config

-- | <tt>Name</tt>s exported by the module being verified
exports :: GhcSpec -> !NameSet
measures :: GhcSpec -> [Measure SpecType DataCon]
tyconEnv :: GhcSpec -> HashMap TyCon RTyCon

-- | Dictionary Environment
dicts :: GhcSpec -> DEnv Var SpecType
makeGhcSpec :: Config -> ModName -> [CoreBind] -> [Var] -> [Var] -> NameSet -> HscEnv -> Either Error LogicMap -> [(ModName, BareSpec)] -> IO GhcSpec

module Language.Haskell.Liquid.Qualifier
specificationQualifiers :: Int -> GhcInfo -> [Qualifier]

module Language.Haskell.Liquid.Constraint.ToFixpoint
cgInfoFInfo :: GhcInfo -> CGInfo -> IO (FInfo Cinfo)

module Language.Haskell.Liquid.GhcInterface
getGhcInfo :: Config -> FilePath -> IO (Either ErrorResult GhcInfo)
instance Result SourceError
instance PPrint TargetVars
instance PPrint [CoreBind]
instance Show GhcInfo
instance PPrint GhcInfo
instance PPrint GhcSpec

module Language.Haskell.Liquid.List
transpose :: Int -> [[a]] -> [[a]]

module Language.Haskell.Liquid.Foreign
intCSize :: Int -> CSize
cSizeInt :: CSize -> Int
mkPtr :: Addr# -> Ptr b
isNullPtr :: Ptr a -> Bool
fpLen :: ForeignPtr a -> Int
pLen :: Ptr a -> Int
deref :: Ptr a -> a
eqPtr :: Ptr a -> Ptr a -> Bool

module Language.Haskell.Liquid.Prelude
plus :: Int -> Int -> Int
minus :: Int -> Int -> Int
times :: Int -> Int -> Int
eq :: Int -> Int -> Bool
neq :: Int -> Int -> Bool
leq :: Int -> Int -> Bool
geq :: Int -> Int -> Bool
lt :: Int -> Int -> Bool
gt :: Int -> Int -> Bool
liquidAssertB :: Bool -> Bool
liquidAssert :: Bool -> a -> a
liquidAssume :: Bool -> a -> a
liquidAssumeB :: (a -> Bool) -> a -> a
liquidError :: String -> a
crash :: Bool -> a
force :: Bool
choose :: Int -> Int
isEven :: Int -> Bool
isOdd :: Int -> Bool
safeZipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
(==>) :: Bool -> Bool -> Bool