-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Liquid Types for Haskell
--
-- Liquid Types for Haskell.
@package liquidhaskell
@version 0.8.2.2
module Gradual.GUI.Misc
script :: String -> String
module Gradual.Misc
-- | Mapping
-- ------------------------------------------------------------------
mapThd3 :: (c -> d) -> (a, b, c) -> (a, b, d)
mapSndM :: Functor m => (b -> m c) -> (a, b) -> m (a, c)
mapMWithLog :: String -> (a -> IO b) -> [a] -> IO [b]
-- | Powersets
-- ----------------------------------------------------------------
powersetUpTo :: Int -> [a] -> [[a]]
-- | Combining
-- ----------------------------------------------------------------
flatten :: [(k, (i, [v]))] -> [[(k, (i, v))]]
expand :: (a -> [a]) -> [a] -> [[a]]
expand2 :: (b -> [b]) -> [(a, b)] -> [[(a, b)]]
expand3 :: (c -> [c]) -> [(a, b, c)] -> [[(a, b, c)]]
allCombinations :: [[a]] -> [[a]]
module Gradual.Trivial
simplify :: SInfo a -> SInfo a
module Language.Haskell.Liquid.Bag
type Bag a = Map a Int
empty :: Bag k
get :: (Ord k) => k -> Bag k -> Int
put :: (Ord k) => k -> Bag k -> Bag k
union :: (Ord k) => Bag k -> Bag k -> Bag k
module Language.Haskell.Liquid.Desugar.Coverage
addTicksToBinds :: HscEnv -> Module -> ModLocation -> NameSet -> [TyCon] -> LHsBinds Id -> IO (LHsBinds Id, HpcInfo, Maybe ModBreaks)
hpcInitCode :: Module -> HpcInfo -> SDoc
instance GHC.Classes.Eq Language.Haskell.Liquid.Desugar.Coverage.TickishType
instance GHC.Classes.Eq Language.Haskell.Liquid.Desugar.Coverage.TickDensity
instance GHC.Base.Functor Language.Haskell.Liquid.Desugar.Coverage.TM
instance GHC.Base.Applicative Language.Haskell.Liquid.Desugar.Coverage.TM
instance GHC.Base.Monad Language.Haskell.Liquid.Desugar.Coverage.TM
instance DynFlags.HasDynFlags Language.Haskell.Liquid.Desugar.Coverage.TM
instance UniqSupply.MonadUnique Language.Haskell.Liquid.Desugar.Coverage.TM
module Language.Haskell.Liquid.Desugar.DsMonad
type DsM = TcRnIf DsGblEnv DsLclEnv
-- | Map each element of a structure to a monadic action, evaluate these
-- actions from left to right, and collect the results. For a version
-- that ignores the results see mapM_.
mapM :: Traversable t => forall (m :: * -> *) a b. Monad m => (a -> m b) -> t a -> m t b
-- | The mapAndUnzipM function maps its first argument over a list,
-- returning the result as a pair of lists. This function is mainly used
-- with complicated data structures or a state-transforming monad.
mapAndUnzipM :: Applicative m => (a -> m (b, c)) -> [a] -> m ([b], [c])
-- | Run a DsM action inside the IO monad.
initDs :: HscEnv -> TcGblEnv -> DsM a -> IO (Messages, Maybe a)
-- | Run a DsM action inside the TcM monad.
initDsTc :: DsM a -> TcM a
initTcDsForSolver :: TcM a -> DsM (Messages, Maybe a)
-- | Run a DsM action in the context of an existing ModGuts
initDsWithModGuts :: HscEnv -> ModGuts -> DsM a -> IO (Messages, Maybe a)
fixDs :: (a -> DsM a) -> DsM a
-- | Monadic version of foldl
foldlM :: Monad m => (a -> b -> m a) -> a -> [b] -> m a
-- | Monadic version of foldr
foldrM :: Monad m => (b -> a -> m a) -> a -> [b] -> m a
whenGOptM :: () => GeneralFlag -> TcRnIf gbl lcl () -> TcRnIf gbl lcl ()
unsetGOptM :: () => GeneralFlag -> TcRnIf gbl lcl a -> TcRnIf gbl lcl a
unsetWOptM :: () => WarningFlag -> TcRnIf gbl lcl a -> TcRnIf gbl lcl a
xoptM :: () => Extension -> TcRnIf gbl lcl Bool
-- | A functor with application, providing operations to
--
--
-- - embed pure expressions (pure), and
-- - sequence computations and combine their results (<*>
-- and liftA2).
--
--
-- A minimal complete definition must include implementations of
-- pure and of either <*> or liftA2. If it
-- defines both, then they must behave the same as their default
-- definitions:
--
-- (<*>) = liftA2 id
-- liftA2 f x y = f <$> x <*>
-- y
--
-- Further, any definition must satisfy the following:
--
--
--
-- The other methods have the following default definitions, which may be
-- overridden with equivalent specialized implementations:
--
--
--
-- As a consequence of these laws, the Functor instance for
-- f will satisfy
--
--
--
-- It may be useful to note that supposing
--
--
-- forall x y. p (q x y) = f x . g y
--
--
-- it follows from the above that
--
--
-- liftA2 p (liftA2 q u v) = liftA2 f u . liftA2 g v
--
--
-- If f is also a Monad, it should satisfy
--
--
--
-- (which implies that pure and <*> satisfy the
-- applicative functor laws).
class Functor f => Applicative (f :: * -> *)
-- | Lift a value.
pure :: Applicative f => a -> f a
-- | Sequential application.
--
-- A few functors support an implementation of <*> that is
-- more efficient than the default one.
(<*>) :: Applicative f => f (a -> b) -> f a -> f b
-- | Sequence actions, discarding the value of the first argument.
(*>) :: Applicative f => f a -> f b -> f b
-- | Sequence actions, discarding the value of the second argument.
(<*) :: Applicative f => f a -> f b -> f a
-- | An infix synonym for fmap.
--
-- The name of this operator is an allusion to $. Note the
-- similarities between their types:
--
--
-- ($) :: (a -> b) -> a -> b
-- (<$>) :: Functor f => (a -> b) -> f a -> f b
--
--
-- Whereas $ is function application, <$> is
-- function application lifted over a Functor.
--
-- Examples
--
-- Convert from a Maybe Int to a
-- Maybe String using show:
--
--
-- >>> show <$> Nothing
-- Nothing
--
-- >>> show <$> Just 3
-- Just "3"
--
--
-- Convert from an Either Int Int to
-- an Either Int String using
-- show:
--
--
-- >>> show <$> Left 17
-- Left 17
--
-- >>> show <$> Right 17
-- Right "17"
--
--
-- Double each element of a list:
--
--
-- >>> (*2) <$> [1,2,3]
-- [2,4,6]
--
--
-- Apply even to the second element of a pair:
--
--
-- >>> even <$> (2,2)
-- (2,True)
--
(<$>) :: Functor f => (a -> b) -> f a -> f b
infixl 4 <$>
duplicateLocalDs :: Id -> DsM Id
newSysLocalDsNoLP :: Type -> DsM Id
newSysLocalDs :: Type -> DsM Id
newSysLocalsDsNoLP :: [Type] -> DsM [Id]
newSysLocalsDs :: [Type] -> DsM [Id]
newUniqueId :: Id -> Type -> DsM Id
newFailLocalDs :: Type -> DsM Id
newPredVarDs :: PredType -> DsM Var
getSrcSpanDs :: DsM SrcSpan
putSrcSpanDs :: SrcSpan -> DsM a -> DsM a
mkPrintUnqualifiedDs :: DsM PrintUnqualified
newUnique :: () => TcRnIf gbl lcl Unique
-- | Unique Supply
--
-- A value of type UniqSupply is unique, and it can supply
-- one distinct Unique. Also, from the supply, one can also
-- manufacture an arbitrary number of further UniqueSupply
-- values, which will be distinct from the first and from all others.
data UniqSupply :: *
newUniqueSupply :: () => TcRnIf gbl lcl UniqSupply
getGhcModeDs :: DsM GhcMode
dsGetFamInstEnvs :: DsM FamInstEnvs
dsLookupGlobal :: Name -> DsM TyThing
dsLookupGlobalId :: Name -> DsM Id
-- | Get a name from Data.Array.Parallel for the desugarer, from the
-- ds_parr_bi component of the global desugerar environment.
dsDPHBuiltin :: (PArrBuiltin -> a) -> DsM a
dsLookupTyCon :: Name -> DsM TyCon
dsLookupDataCon :: Name -> DsM DataCon
dsLookupConLike :: Name -> DsM ConLike
data PArrBuiltin :: *
PArrBuiltin :: Var -> Var -> Var -> Var -> Var -> Var -> Var -> Var -> Var -> Var -> Var -> Var -> PArrBuiltin
-- | lengthP
[lengthPVar] :: PArrBuiltin -> Var
-- | replicateP
[replicatePVar] :: PArrBuiltin -> Var
-- | singletonP
[singletonPVar] :: PArrBuiltin -> Var
-- | mapP
[mapPVar] :: PArrBuiltin -> Var
-- | filterP
[filterPVar] :: PArrBuiltin -> Var
-- | zipP
[zipPVar] :: PArrBuiltin -> Var
-- | crossMapP
[crossMapPVar] :: PArrBuiltin -> Var
-- | (!:)
[indexPVar] :: PArrBuiltin -> Var
-- | emptyP
[emptyPVar] :: PArrBuiltin -> Var
-- | (+:+)
[appPVar] :: PArrBuiltin -> Var
-- | enumFromToP
[enumFromToPVar] :: PArrBuiltin -> Var
-- | enumFromThenToP
[enumFromThenToPVar] :: PArrBuiltin -> Var
-- | Lookup a name exported by Prim or Prim. Panic if there
-- isn't one, or if it is defined multiple times.
dsLookupDPHRdrEnv :: OccName -> DsM Name
-- | Lookup a name exported by Prim or Prim, returning
-- Nothing if it's not defined. Panic if it's defined multiple
-- times.
dsLookupDPHRdrEnv_maybe :: OccName -> DsM (Maybe Name)
-- | Populate ds_parr_bi from ds_dph_env.
dsInitPArrBuiltin :: DsM a -> DsM a
type DsMetaEnv = NameEnv DsMetaVal
data DsMetaVal :: *
DsBound :: Id -> DsMetaVal
DsSplice :: HsExpr Id -> DsMetaVal
dsGetMetaEnv :: DsM (NameEnv DsMetaVal)
dsLookupMetaEnv :: Name -> DsM (Maybe DsMetaVal)
dsExtendMetaEnv :: DsMetaEnv -> DsM a -> DsM a
-- | Get in-scope type constraints (pm check)
getDictsDs :: DsM (Bag EvVar)
-- | Add in-scope type constraints (pm check)
addDictsDs :: Bag EvVar -> DsM a -> DsM a
-- | Get in-scope term constraints (pm check)
getTmCsDs :: DsM (Bag SimpleEq)
-- | Add in-scope term constraints (pm check)
addTmCsDs :: Bag SimpleEq -> DsM a -> DsM a
-- | Increase the counter for elapsed pattern match check iterations. If
-- the current counter is already over the limit, fail
incrCheckPmIterDs :: DsM Int
-- | Reset the counter for pattern match check iterations to zero
resetPmIterDs :: DsM ()
-- | The COMPLETE pragams provided by the user for a given
-- TyCon.
dsGetCompleteMatches :: TyCon -> DsM [CompleteMatch]
type DsWarning = (SrcSpan, SDoc)
-- | Emit a warning for the current source location NB: Warns whether or
-- not -Wxyz is set
warnDs :: WarnReason -> SDoc -> DsM ()
-- | Emit a warning only if the correct WarnReason is set in the DynFlags
warnIfSetDs :: WarningFlag -> SDoc -> DsM ()
errDs :: SDoc -> DsM ()
-- | Issue an error, but return the expression for (), so that we can
-- continue reporting errors.
errDsCoreExpr :: SDoc -> DsM CoreExpr
failWithDs :: SDoc -> DsM a
failDs :: DsM a
discardWarningsDs :: DsM a -> DsM a
askNoErrsDs :: DsM a -> DsM (a, Bool)
data DsMatchContext
DsMatchContext :: (HsMatchContext Name) -> SrcSpan -> DsMatchContext
data EquationInfo
EqnInfo :: [Pat Id] -> MatchResult -> EquationInfo
[eqn_pats] :: EquationInfo -> [Pat Id]
[eqn_rhs] :: EquationInfo -> MatchResult
data MatchResult
MatchResult :: CanItFail -> (CoreExpr -> DsM CoreExpr) -> MatchResult
type DsWrapper = CoreExpr -> CoreExpr
idDsWrapper :: DsWrapper
data CanItFail
CanFail :: CanItFail
CantFail :: CanItFail
orFail :: CanItFail -> CanItFail -> CanItFail
-- | Fail with an error message if the type is levity polymorphic.
dsNoLevPoly :: Type -> SDoc -> DsM ()
-- | Check an expression for levity polymorphism, failing if it is levity
-- polymorphic.
dsNoLevPolyExpr :: CoreExpr -> SDoc -> DsM ()
-- | Runs the thing_inside. If there are no errors, then returns the expr
-- given. Otherwise, returns unitExpr. This is useful for doing a bunch
-- of levity polymorphism checks and then avoiding making a core App. (If
-- we make a core App on a levity polymorphic argument, detecting how to
-- handle the let/app invariant might call isUnliftedType, which panics
-- on a levity polymorphic type.) See #12709 for an example of why this
-- machinery is necessary.
dsWhenNoErrs :: DsM a -> (a -> CoreExpr) -> DsM CoreExpr
instance Outputable.Outputable Language.Haskell.Liquid.Desugar.DsMonad.EquationInfo
instance Outputable.Outputable Language.Haskell.Liquid.Desugar.DsMonad.DsMatchContext
instance HscTypes.MonadThings (IOEnv.IOEnv (TcRnTypes.Env TcRnTypes.DsGblEnv TcRnTypes.DsLclEnv))
-- | 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 -> [Var] -> HsWrapper -> MatchResult -> CaseAlt a
[alt_pat] :: CaseAlt a -> a
[alt_bndrs] :: CaseAlt a -> [Var]
[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 -> 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 :: SDoc -> CoreExpr -> CoreExpr -> CoreExpr
mkCoreAppsDs :: SDoc -> CoreExpr -> [CoreExpr] -> CoreExpr
mkCastDs :: CoreExpr -> Coercion -> CoreExpr
seqVar :: Var -> CoreExpr -> CoreExpr
mkLHsVarPatTup :: [Id] -> LPat Id
mkLHsPatTup :: [LPat Id] -> LPat Id
mkVanillaTuplePat :: [OutPat Id] -> Boxity -> Pat Id
mkBigLHsVarTupId :: [Id] -> LHsExpr Id
mkBigLHsTupId :: [LHsExpr Id] -> LHsExpr Id
mkBigLHsVarPatTupId :: [Id] -> LPat Id
mkBigLHsPatTupId :: [LPat Id] -> LPat Id
mkSelectorBinds :: [[Tickish Id]] -> LPat Id -> CoreExpr -> DsM (Id, [(Id, CoreExpr)])
selectSimpleMatchVarL :: LPat Id -> DsM Id
selectMatchVars :: [Pat Id] -> DsM [Id]
selectMatchVar :: Pat Id -> DsM Id
mkOptTickBox :: [Tickish Id] -> CoreExpr -> CoreExpr
mkBinaryTickBox :: Int -> Int -> CoreExpr -> DsM CoreExpr
-- | Use -XStrict to add a ! or remove a ~
--
-- Examples: ~pat => pat -- when -XStrict (even if pat = ~pat') !pat
-- => !pat -- always pat => !pat -- when -XStrict pat => pat --
-- otherwise
decideBangHood :: DynFlags -> LPat id -> LPat id
-- | Unconditionally make a Pat strict.
addBang :: LPat id -> LPat id
module Language.Haskell.Liquid.Desugar.DsCCall
dsCCall :: CLabelString -> [CoreExpr] -> Safety -> Type -> DsM CoreExpr
mkFCall :: DynFlags -> Unique -> ForeignCall -> [CoreExpr] -> Type -> CoreExpr
unboxArg :: CoreExpr -> DsM (CoreExpr, CoreExpr -> CoreExpr)
boxResult :: Type -> DsM (Type, CoreExpr -> CoreExpr)
resultWrapper :: Type -> DsM (Maybe Type, CoreExpr -> CoreExpr)
module Language.Haskell.Liquid.Desugar.DsForeign
dsForeigns :: [LForeignDecl Id] -> DsM (ForeignStubs, OrdList Binding)
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
isTrueLHsExpr :: LHsExpr Id -> Maybe (CoreExpr -> DsM CoreExpr)
module Language.Haskell.Liquid.Desugar.DsBinds
-- | Desugar top level binds, strict binds are treated like normal binds
-- since there is no good time to force before first usage.
dsTopLHsBinds :: LHsBinds Id -> DsM (OrdList (Id, CoreExpr))
-- | Desugar all other kind of bindings, Ids of strict binds are returned
-- to later be forced in the binding group body, see Note [Desugar Strict
-- binds]
dsLHsBinds :: LHsBinds Id -> DsM ([Id], [(Id, CoreExpr)])
decomposeRuleLhs :: [Var] -> CoreExpr -> Either SDoc ([Var], Id, [CoreExpr])
dsSpec :: Maybe CoreExpr -> Located TcSpecPrag -> DsM (Maybe (OrdList (Id, CoreExpr), CoreRule))
dsHsWrapper :: HsWrapper -> DsM (CoreExpr -> CoreExpr)
dsTcEvBinds :: TcEvBinds -> DsM [CoreBind]
dsTcEvBinds_s :: [TcEvBinds] -> DsM [CoreBind]
dsEvBinds :: Bag EvBind -> DsM [CoreBind]
dsMkUserRule :: Module -> Bool -> RuleName -> Activation -> Name -> [CoreBndr] -> [CoreExpr] -> CoreExpr -> DsM CoreRule
module Language.Haskell.Liquid.Desugar.MatchCon
matchConFamily :: [Id] -> Type -> [[EquationInfo]] -> DsM MatchResult
matchPatSyn :: [Id] -> Type -> [EquationInfo] -> DsM MatchResult
module Language.Haskell.Liquid.Desugar.MatchLit
dsLit :: HsLit -> DsM CoreExpr
dsOverLit :: HsOverLit Id -> DsM CoreExpr
dsOverLit' :: DynFlags -> HsOverLit Id -> DsM CoreExpr
hsLitKey :: DynFlags -> HsLit -> Literal
tidyLitPat :: HsLit -> Pat Id
tidyNPat :: (HsLit -> Pat Id) -> HsOverLit Id -> Maybe (SyntaxExpr Id) -> SyntaxExpr Id -> Type -> 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 ()
warnAboutOverflowedLiterals :: DynFlags -> HsOverLit Id -> DsM ()
warnAboutEmptyEnumerations :: DynFlags -> LHsExpr Id -> Maybe (LHsExpr Id) -> LHsExpr Id -> DsM ()
module Language.Haskell.Liquid.Desugar.DsMeta
dsBracket :: HsBracket Name -> [PendingTcSplice] -> DsM CoreExpr
-- | Code generation for the Static Pointer Table
--
-- (c) 2014 I/O Tweag
--
-- Each module that uses static keyword declares an
-- initialization function of the form hs_spt_init_module() which
-- is emitted into the _stub.c file and annotated with
-- attribute((constructor)) so that it gets executed at startup
-- time.
--
-- The function's purpose is to call hs_spt_insert to insert the static
-- pointers of this module in the hashtable of the RTS, and it looks
-- something like this:
--
--
-- static void hs_hpc_init_Main(void) __attribute__((constructor));
-- static void hs_hpc_init_Main(void) {
--
-- static StgWord64 k0[2] = {16252233372134256ULL,7370534374096082ULL};
-- extern StgPtr Main_sptEntryZC0_closure;
-- hs_spt_insert(k0, &Main_sptEntryZC0_closure);
--
-- static StgWord64 k1[2] = {12545634534567898ULL,5409674567544151ULL};
-- extern StgPtr Main_sptEntryZC1_closure;
-- hs_spt_insert(k1, &Main_sptEntryZC1_closure);
--
-- }
--
--
-- where the constants are fingerprints produced from the static forms.
--
-- There is also a finalization function for the time when the module is
-- unloaded.
--
--
-- static void hs_hpc_fini_Main(void) __attribute__((destructor));
-- static void hs_hpc_fini_Main(void) {
--
-- static StgWord64 k0[2] = {16252233372134256ULL,7370534374096082ULL};
-- hs_spt_remove(k0);
--
-- static StgWord64 k1[2] = {12545634534567898ULL,5409674567544151ULL};
-- hs_spt_remove(k1);
--
-- }
--
module Language.Haskell.Liquid.Desugar.StaticPtrTable
-- | sptInitCode module statics is a C stub to insert the static
-- entries statics of module into the static pointer
-- table.
--
-- Each entry contains the fingerprint used to locate the entry and the
-- top-level binding for the entry.
sptInitCode :: Module -> [(Fingerprint, (Id, CoreExpr))] -> SDoc
module Language.Haskell.Liquid.Desugar.TmOracle
-- | Lifted expressions for pattern match checking.
data PmExpr :: *
PmExprVar :: Name -> PmExpr
PmExprCon :: ConLike -> [PmExpr] -> PmExpr
PmExprLit :: PmLit -> PmExpr
PmExprEq :: PmExpr -> PmExpr -> PmExpr
PmExprOther :: HsExpr Id -> PmExpr
-- | Literals (simple and overloaded ones) for pattern match checking.
data PmLit :: *
PmSLit :: HsLit -> PmLit
PmOLit :: Bool -> HsOverLit Id -> PmLit
-- | Term equalities
type SimpleEq = (Id, PmExpr)
type ComplexEq = (PmExpr, PmExpr)
-- | The type of substitutions.
type PmVarEnv = NameEnv PmExpr
-- | Expression False
falsePmExpr :: PmExpr
-- | Equality between literals for pattern match checking.
eqPmLit :: PmLit -> PmLit -> Bool
filterComplex :: [ComplexEq] -> [PmNegLitCt]
-- | Check if an expression is lifted or not
isNotPmExprOther :: PmExpr -> Bool
runPmPprM :: () => PmPprM a -> [PmNegLitCt] -> (a, [(SDoc, [PmLit])])
lhsExprToPmExpr :: LHsExpr Id -> PmExpr
hsExprToPmExpr :: HsExpr Id -> PmExpr
pprPmExprWithParens :: PmExpr -> PmPprM SDoc
-- | External interface to the term oracle.
tmOracle :: TmState -> [ComplexEq] -> Maybe TmState
-- | The state of the term oracle (includes complex constraints that cannot
-- progress unless we get more information).
type TmState = ([ComplexEq], TmOracleEnv)
-- | Initial state of the oracle.
initialTmState :: TmState
-- | Solve a complex equality (top-level).
solveOneEq :: TmState -> ComplexEq -> Maybe TmState
-- | When we know that a variable is fresh, we do not actually have to
-- check whether anything changes, we know that nothing does. Hence,
-- extendSubst simply extends the substitution, unlike what
-- extendSubstAndSolve does.
extendSubst :: Id -> PmExpr -> TmState -> TmState
-- | Check whether a constraint (x ~ BOT) can succeed, given the resulting
-- state of the term oracle.
canDiverge :: Name -> TmState -> Bool
-- | Lift a SimpleEq to a ComplexEq
toComplex :: SimpleEq -> ComplexEq
-- | Apply an (un-flattened) substitution to an expression.
exprDeepLookup :: PmVarEnv -> PmExpr -> PmExpr
-- | Type of a PmLit
pmLitType :: PmLit -> Type
-- | Flatten the DAG (Could be improved in terms of performance.).
flattenPmVarEnv :: PmVarEnv -> PmVarEnv
module Language.Haskell.Liquid.Desugar.Check
-- | Check a single pattern binding (let)
checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat Id -> DsM ()
-- | Check a matchgroup (case, functions, etc.)
checkMatches :: DynFlags -> DsMatchContext -> [Id] -> [LMatch Id (LHsExpr Id)] -> DsM ()
-- | Check whether any part of pattern match checking is enabled (does not
-- matter whether it is the redundancy check or the exhaustiveness
-- check).
isAnyPmCheckEnabled :: DynFlags -> DsMatchContext -> Bool
-- | Generate a simple equality when checking a case expression: case x of
-- { matches } When checking matches we record that (x ~ y) where y is
-- the initial uncovered. All matches will have to satisfy this equality.
genCaseTmCs1 :: Maybe (LHsExpr Id) -> [Id] -> Bag SimpleEq
-- | Generate equalities when checking a case expression: case x of { p1
-- -> e1; ... pn -> en } When we go deeper to check e.g. e1 we
-- record two equalities: (x ~ y), where y is the initial uncovered when
-- checking (p1; .. ; pn) and (x ~ p1).
genCaseTmCs2 :: Maybe (LHsExpr Id) -> [Pat Id] -> [Id] -> DsM (Bag SimpleEq)
instance GHC.Classes.Ord Language.Haskell.Liquid.Desugar.Check.Provenance
instance GHC.Classes.Eq Language.Haskell.Liquid.Desugar.Check.Provenance
instance GHC.Show.Show Language.Haskell.Liquid.Desugar.Check.Provenance
instance GHC.Show.Show Language.Haskell.Liquid.Desugar.Check.Diverged
instance GHC.Show.Show Language.Haskell.Liquid.Desugar.Check.Covered
instance Outputable.Outputable Language.Haskell.Liquid.Desugar.Check.PartialResult
instance GHC.Base.Monoid Language.Haskell.Liquid.Desugar.Check.PartialResult
instance Outputable.Outputable Language.Haskell.Liquid.Desugar.Check.Provenance
instance GHC.Base.Monoid Language.Haskell.Liquid.Desugar.Check.Provenance
instance Outputable.Outputable Language.Haskell.Liquid.Desugar.Check.Diverged
instance GHC.Base.Monoid Language.Haskell.Liquid.Desugar.Check.Diverged
instance Outputable.Outputable Language.Haskell.Liquid.Desugar.Check.Covered
instance GHC.Base.Monoid Language.Haskell.Liquid.Desugar.Check.Covered
instance Outputable.Outputable Language.Haskell.Liquid.Desugar.Check.ValVec
module Language.Haskell.Liquid.Desugar.Match
match :: [MatchId] -> Type -> [EquationInfo] -> DsM MatchResult
matchEquations :: HsMatchContext Name -> [MatchId] -> [EquationInfo] -> Type -> DsM CoreExpr
matchWrapper :: HsMatchContext Name -> Maybe (LHsExpr Id) -> 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.DsListComp
dsListComp :: [ExprLStmt Id] -> Type -> DsM CoreExpr
dsPArrComp :: [ExprStmt Id] -> DsM CoreExpr
dsMonadComp :: [ExprLStmt Id] -> DsM CoreExpr
module Language.Haskell.Liquid.Desugar.DsArrows
dsProcExpr :: LPat Id -> LHsCmdTop Id -> DsM CoreExpr
module Language.Haskell.Liquid.Desugar.DsExpr
dsExpr :: HsExpr Id -> DsM CoreExpr
dsLExpr :: LHsExpr Id -> DsM CoreExpr
-- | Variant of dsLExpr that ensures that the result is not levity
-- polymorphic. This should be used when the resulting expression will be
-- an argument to some other function. See Note [Levity polymorphism
-- checking] in DsMonad See Note [Levity polymorphism invariants] in
-- CoreSyn
dsLExprNoLP :: LHsExpr Id -> DsM CoreExpr
dsLocalBinds :: LHsLocalBinds Id -> CoreExpr -> DsM CoreExpr
dsValBinds :: HsValBinds Id -> CoreExpr -> DsM CoreExpr
dsLit :: HsLit -> DsM CoreExpr
dsSyntaxExpr :: SyntaxExpr Id -> [CoreExpr] -> DsM CoreExpr
module Language.Haskell.Liquid.Desugar.Desugar
-- | Main entry point to the desugarer.
deSugar :: HscEnv -> ModLocation -> TcGblEnv -> IO (Messages, Maybe ModGuts)
deSugarExpr :: HscEnv -> LHsExpr Id -> IO (Messages, Maybe CoreExpr)
-- | Main API for compiling plain Haskell source code.
--
-- This module implements compilation of a Haskell source. It is
-- not concerned with preprocessing of source files; this is
-- handled in DriverPipeline.
--
-- There are various entry points depending on what mode we're in:
-- "batch" mode (--make), "one-shot" mode (-c,
-- -S 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 HscEnv as a parameter, but none
-- of them return a new one: HscEnv 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
-- HscMain returns, the warnings are either printed, or turned
-- into a real compialtion error if the -Werror 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.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
-- | This module contains functions for "resugaring" low-level GHC
-- CoreExpr into high-level patterns, that can receive special
-- case handling in different phases (e.g. ANF, Constraint Generation,
-- etc.)
module Language.Haskell.Liquid.GHC.Resugar
-- | Data type for high-level patterns
-- -----------------------------------------
data Pattern
-- | e1 >>= x -> e2
PatBind :: !CoreExpr -> !Var -> !CoreExpr -> !Type -> !CoreExpr -> !Type -> !Type -> !Var -> Pattern
[patE1] :: Pattern -> !CoreExpr
-- | x
[patX] :: Pattern -> !Var
[patE2] :: Pattern -> !CoreExpr
-- | m
[patM] :: Pattern -> !Type
-- | $dT
[patDct] :: Pattern -> !CoreExpr
[patTyA] :: Pattern -> !Type
[patTyB] :: Pattern -> !Type
[patFF] :: Pattern -> !Var
PatReturn :: !CoreExpr -> !Type -> !CoreExpr -> !Type -> !Var -> Pattern
-- | e
[patE] :: Pattern -> !CoreExpr
-- | m
[patM] :: Pattern -> !Type
-- | $dT
[patDct] :: Pattern -> !CoreExpr
-- | t
[patTy] :: Pattern -> !Type
-- | "return"
[patRet] :: Pattern -> !Var
PatProject :: !Var -> !Var -> !Type -> !DataCon -> ![Var] -> !Int -> Pattern
-- | xe
[patXE] :: Pattern -> !Var
-- | x
[patX] :: Pattern -> !Var
-- | t
[patTy] :: Pattern -> !Type
-- | C
[patCtor] :: Pattern -> !DataCon
-- |
[patBinds] :: Pattern -> ![Var]
-- | i :: NatLT {len patBinds}
[patIdx] :: Pattern -> !Int
PatSelfBind :: !Var -> !CoreExpr -> Pattern
-- | x
[patX] :: Pattern -> !Var
-- | e
[patE] :: Pattern -> !CoreExpr
PatSelfRecBind :: !Var -> !CoreExpr -> Pattern
-- | x
[patX] :: Pattern -> !Var
-- | e
[patE] :: Pattern -> !CoreExpr
-- | Lift expressions into High-level patterns
-- ---------------------------------
lift :: CoreExpr -> Maybe Pattern
-- | Lower patterns back into expressions
-- --------------------------------------
lower :: Pattern -> CoreExpr
module Language.Haskell.Liquid.List
transpose :: Int -> [[a]] -> [[a]]
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
unsafeError :: String -> 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
infixr 8 ==>
module Language.Haskell.Liquid.ProofCombinators
(==:) :: a -> a -> Proof -> a
infixl 3 ==:
-- | proof operators requiring proof terms
--
-- Comparison operators requiring proof terms
(<=:) :: a -> a -> Proof -> a
infixl 3 <=:
(<:) :: a -> a -> Proof -> a
infixl 3 <:
(>:) :: a -> a -> Proof -> a
infixl 3 >:
(==?) :: ToProve a r => a -> a -> r
infixl 3 ==?
(==.) :: OptEq a r => a -> a -> r
infixl 3 ==.
(<=.) :: OptLEq a r => a -> a -> r
infixl 3 <=.
(<.) :: OptLess a r => a -> a -> r
infixl 3 <.
(>.) :: OptGt a r => a -> a -> r
infixl 3 >.
(>=.) :: OptGEq a r => a -> a -> r
infixl 3 >=.
(?) :: (Proof -> a) -> Proof -> a
infixl 3 ?
(***) :: a -> QED -> Proof
infixl 2 ***
-- | Proof combinators (are Proofean combinators)
(==>) :: Proof -> Proof -> Proof
(&&&) :: Proof -> Proof -> Proof
-- | Because provide lemmata ? or ∵
(∵) :: (Proof -> a) -> Proof -> a
infixl 3 ∵
-- | proof goes from Int to resolve types for the optional proof
-- combinators
proof :: Int -> Proof
toProof :: a -> Proof
simpleProof :: Proof
trivial :: Proof
data QED
QED :: QED
type Proof = ()
byTheorem :: a -> Proof -> a
castWithTheorem :: a -> b -> b
cast :: b -> a -> a
-- | Function Equality
class Arg a
(=*=.) :: Arg a => (a -> b) -> (a -> b) -> (a -> Proof) -> (a -> b)
data PAnd a b
PAnd :: a -> b -> PAnd a b
data POr a b
POrLeft :: a -> POr a b
POrRight :: b -> POr a b
instance a ~ b => Language.Haskell.Liquid.ProofCombinators.OptGt a (Language.Haskell.Liquid.ProofCombinators.Proof -> b)
instance a ~ b => Language.Haskell.Liquid.ProofCombinators.OptGt a b
instance a ~ b => Language.Haskell.Liquid.ProofCombinators.OptLess a (Language.Haskell.Liquid.ProofCombinators.Proof -> b)
instance a ~ b => Language.Haskell.Liquid.ProofCombinators.OptLess a b
instance Language.Haskell.Liquid.ProofCombinators.OptGEq a (Language.Haskell.Liquid.ProofCombinators.Proof -> a)
instance Language.Haskell.Liquid.ProofCombinators.OptGEq a a
instance a ~ b => Language.Haskell.Liquid.ProofCombinators.OptLEq a (Language.Haskell.Liquid.ProofCombinators.Proof -> b)
instance a ~ b => Language.Haskell.Liquid.ProofCombinators.OptLEq a b
instance a ~ b => Language.Haskell.Liquid.ProofCombinators.OptEq a (Language.Haskell.Liquid.ProofCombinators.Proof -> b)
instance a ~ b => Language.Haskell.Liquid.ProofCombinators.OptEq a b
instance a ~ b => Language.Haskell.Liquid.ProofCombinators.ToProve a b
instance a ~ b => Language.Haskell.Liquid.ProofCombinators.ToProve a (Language.Haskell.Liquid.ProofCombinators.Proof -> b)
module Language.Haskell.Liquid.Types.Names
lenLocSymbol :: Located Symbol
anyTypeSymbol :: Symbol
-- | This module contains the LH specifications (assumes) for various
-- imported modules.
module Language.Haskell.Liquid.Types.Specifications
-- | Gross hack, to force dependency and loading of module.
specAnchor :: Int
module Language.Haskell.Liquid.Types.Variance
data Variance
Invariant :: Variance
Bivariant :: Variance
Contravariant :: Variance
Covariant :: Variance
type VarianceInfo = [Variance]
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Variance.Variance
instance GHC.Show.Show Language.Haskell.Liquid.Types.Variance.Variance
instance Data.Data.Data Language.Haskell.Liquid.Types.Variance.Variance
instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Variance.Variance
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Variance.Variance
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Variance.Variance
-- | Command Line Configuration Options
-- ----------------------------------------
module Language.Haskell.Liquid.UX.Config
data Config
Config :: [FilePath] -> [FilePath] -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> [String] -> Bool -> Bool -> Bool -> Int -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Maybe Int -> Int -> Int -> Int -> Maybe SMTSolver -> Bool -> Bool -> Bool -> [String] -> [String] -> Eliminate -> Int -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Maybe Int -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Instantiate -> Bool -> Bool -> Bool -> Bool -> 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
-- | uninterpreted integer multiplication and division
[linear] :: Config -> Bool
-- | interpretation of string theory in the logic
[stringTheory] :: Config -> Bool
-- | allow higher order binders into the logic
[higherorder] :: Config -> Bool
-- | allow higher order qualifiers
[higherorderqs] :: Config -> Bool
-- | allow function extentionality axioms
[extensionality] :: Config -> Bool
-- | allow lambda alpha-equivalence axioms
[alphaEquivalence] :: Config -> Bool
-- | allow lambda beta-equivalence axioms
[betaEquivalence] :: Config -> Bool
-- | allow lambda normalization-equivalence axioms
[normalForm] :: Config -> Bool
-- | check all binders (overrides diffcheck)
[fullcheck] :: Config -> Bool
-- | save fixpoint query
[saveQuery] :: Config -> Bool
-- | set of binders to check
[checks] :: Config -> [String]
-- | whether to complain about specifications for unexported and unused
-- values
[noCheckUnknown] :: Config -> Bool
-- | disable termination check
[notermination] :: Config -> Bool
-- | enable gradual type checking
[gradual] :: Config -> Bool
-- | depth of gradual concretization
[gdepth] :: Config -> Int
-- | interactive gradual solving
[ginteractive] :: Config -> Bool
-- | Check for termination and totality, Overrides no-termination flags
[totalHaskell] :: Config -> Bool
-- | automatically construct proofs from axioms
[autoproofs] :: Config -> Bool
-- | disable warnings output (only show errors)
[nowarnings] :: Config -> Bool
-- | disable creation of intermediate annotation files
[noannotations] :: 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
-- | disable totality check in definitions
[nototality] :: Config -> Bool
-- | enable prunning unsorted Refinements
[pruneUnsorted] :: Config -> Bool
-- | number of cores used to solve constraints
[cores] :: Config -> Maybe Int
-- | Minimum size of a partition
[minPartSize] :: Config -> Int
-- | Maximum size of a partition. Overrides minPartSize
[maxPartSize] :: Config -> Int
-- | 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]
-- | eliminate (i.e. don't use qualifs for) for "none", "cuts" or "all"
-- kvars
[eliminate] :: Config -> Eliminate
-- | port at which lhi should listen
[port] :: Config -> Int
-- | Automatically generate singleton types for data constructors
[exactDC] :: Config -> Bool
-- | Disable ADTs (only used with exactDC)
[noADT] :: Config -> Bool
-- | Do not automatically lift data constructor fields into measures
[noMeasureFields] :: Config -> Bool
-- | scrape qualifiers from imported specifications
[scrapeImports] :: Config -> Bool
-- | scrape qualifiers from auto specifications
[scrapeInternals] :: Config -> Bool
-- | scrape qualifiers from used, imported specifications
[scrapeUsedImports] :: Config -> Bool
-- | print eliminate stats
[elimStats] :: Config -> Bool
-- | eliminate upto given depth of KVar chains
[elimBound] :: Config -> Maybe Int
-- | print results (safe/errors) as JSON
[json] :: Config -> Bool
-- | attempt to generate counter-examples to type errors
[counterExamples] :: Config -> Bool
-- | check and time each (asserted) type-sig separately
[timeBinds] :: Config -> Bool
-- | treat code patterns (e.g. e1 >>= x -> e2) specially for
-- inference
[noPatternInline] :: Config -> Bool
-- | print full blown core (with untidy names) in verbose mode
[untidyCore] :: Config -> Bool
-- | simplify GHC core before constraint-generation
[noSimplifyCore] :: Config -> Bool
-- | treat non-linear kvars as cuts
[nonLinCuts] :: Config -> Bool
-- | How to instantiate axioms NO-TRIGGER , proofMethod :: ProofMethod -- ^
-- How to create automatic instances NO-TRIGGER , fuel :: Int -- ^ Fuel
-- for axiom instantiation
[autoInstantiate] :: Config -> Instantiate
-- | Debug Instantiation
[debugInstantionation] :: Config -> Bool
-- | Disable non-concrete KVar slicing
[noslice] :: Config -> Bool
-- | Disable loading lifted specifications (for "legacy" libs)
[noLiftedImport] :: Config -> Bool
-- | Enable proof-by-logical-evaluation
[proofLogicEval] :: Config -> Bool
class HasConfig t
getConfig :: HasConfig t => t -> Config
patternFlag :: HasConfig t => t -> Bool
higherOrderFlag :: HasConfig t => t -> Bool
pruneFlag :: HasConfig t => t -> Bool
expandFlag :: HasConfig t => t -> Bool
hasOpt :: HasConfig t => t -> (Config -> Bool) -> Bool
totalityCheck :: HasConfig t => t -> Bool
terminationCheck :: HasConfig t => t -> Bool
allowPLE :: Config -> Bool
allowLocalPLE :: Config -> Bool
allowGlobalPLE :: Config -> Bool
instance GHC.Classes.Eq Language.Haskell.Liquid.UX.Config.Config
instance GHC.Show.Show Language.Haskell.Liquid.UX.Config.Config
instance Data.Data.Data Language.Haskell.Liquid.UX.Config.Config
instance GHC.Generics.Generic Language.Haskell.Liquid.UX.Config.Config
instance GHC.Generics.Generic Language.Haskell.Liquid.UX.Config.Instantiate
instance Data.Data.Data Language.Haskell.Liquid.UX.Config.Instantiate
instance GHC.Classes.Eq Language.Haskell.Liquid.UX.Config.Instantiate
instance Language.Haskell.Liquid.UX.Config.HasConfig Language.Haskell.Liquid.UX.Config.Config
instance Data.Serialize.Serialize Language.Haskell.Liquid.UX.Config.Config
instance Data.Serialize.Serialize Language.Haskell.Liquid.UX.Config.Instantiate
instance System.Console.CmdArgs.Default.Default Language.Haskell.Liquid.UX.Config.Instantiate
instance GHC.Show.Show Language.Haskell.Liquid.UX.Config.Instantiate
instance Data.Serialize.Serialize Language.Fixpoint.Types.Config.SMTSolver
module Gradual.Types
data GConfig
GConfig :: String -> Int -> Int -> Int -> GConfig
[gtarget] :: GConfig -> String
[depth] :: GConfig -> Int
[pId] :: GConfig -> Int
[pNumber] :: GConfig -> Int
defConfig :: GConfig
setPId :: GConfig -> Int -> GConfig
makeGConfig :: Config -> GConfig
type GSub a = HashMap KVar (a, Expr)
type GMap a = HashMap KVar (a, [Expr])
type GSpan = HashMap KVar [(KVar, Maybe SrcSpan)]
toGMap :: [(KVar, (a, [Expr]))] -> GMap a
fromGMap :: GMap a -> [(KVar, (a, [Expr]))]
fromGSub :: GSub a -> [(KVar, (a, Expr))]
removeInfo :: GMap a -> GMap ()
module Gradual.Uniquify
-- | Make each gradual appearence unique
-- -------------------------------------
uniquify :: (NFData a, Fixpoint a, Loc a) => SInfo a -> (GSpan, SInfo a)
instance Gradual.Uniquify.Unique a => Gradual.Uniquify.Unique (Data.HashMap.Base.HashMap Language.Fixpoint.Types.Constraints.SubcId a)
instance Language.Fixpoint.Types.Spans.Loc a => Gradual.Uniquify.Unique (Language.Fixpoint.Types.Constraints.SimpC a)
instance Gradual.Uniquify.Unique Language.Fixpoint.Types.Environments.IBindEnv
instance Gradual.Uniquify.Unique Language.Fixpoint.Types.Environments.BindId
instance Gradual.Uniquify.Unique Language.Fixpoint.Types.Refinements.SortedReft
instance Gradual.Uniquify.Unique Language.Fixpoint.Types.Refinements.Reft
instance Gradual.Uniquify.Unique Language.Fixpoint.Types.Refinements.Expr
module Gradual.Refinements
makeGMap :: GConfig -> Config -> SInfo a -> [(KVar, (GWInfo, [Expr]))] -> IO (GMap GWInfo)
module Gradual.Concretize
class Gradual a
concretize :: Gradual a => GMap GWInfo -> a -> [(GSub GWInfo, a)]
instance Gradual.Concretize.Gradual (Language.Fixpoint.Types.Constraints.SInfo a)
instance Gradual.Concretize.GSubable Language.Fixpoint.Types.Environments.BindEnv
instance Gradual.Concretize.GSubable (Language.Fixpoint.Types.Constraints.SimpC a)
instance Gradual.Concretize.GSubable v => Gradual.Concretize.GSubable (Data.HashMap.Base.HashMap Language.Fixpoint.Types.Constraints.SubcId v)
instance Gradual.Concretize.GSubable Language.Fixpoint.Types.Refinements.SortedReft
instance Gradual.Concretize.GSubable Language.Fixpoint.Types.Refinements.Reft
module Paths_liquidhaskell
version :: Version
getBinDir :: IO FilePath
getLibDir :: IO FilePath
getDynLibDir :: IO FilePath
getDataDir :: IO FilePath
getLibexecDir :: IO FilePath
getDataFileName :: FilePath -> IO FilePath
getSysconfDir :: IO FilePath
module Language.Haskell.Liquid.Misc
type Nat = Int
(.&&.) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
(.||.) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
up :: (b -> c -> d) -> (a -> b) -> (a -> c) -> (a -> d)
timedAction :: (Show msg) => Maybe msg -> IO a -> IO a
(!?) :: [a] -> Int -> Maybe a
safeFromJust :: String -> Maybe t -> t
takeLast :: Int -> [a] -> [a]
getNth :: Int -> [a] -> Maybe a
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 :: (Enum a, Eq a, Num a) => a -> t -> [t] -> [t]
fourth4 :: (t, t1, t2, t3) -> t3
third4 :: (t, t1, t2, t3) -> t2
mapSndM :: (Applicative m) => (b -> m c) -> (a, b) -> m (a, c)
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)]
getIncludeDir :: IO FilePath
getCssPath :: IO FilePath
getCoreToLogicPath :: IO FilePath
zipMaybe :: [a] -> [b] -> Maybe [(a, b)]
safeZipWithError :: String -> [t] -> [t1] -> [(t, t1)]
safeZip3WithError :: String -> [t] -> [t1] -> [t2] -> [(t, t1, t2)]
mapNs :: (Eq a, Num a, Foldable t) => t a -> (a1 -> a1) -> [a1] -> [a1]
mapN :: (Eq a, Num a) => a -> (a1 -> a1) -> [a1] -> [a1]
zipWithDefM :: Monad m => (a -> a -> m a) -> [a] -> [a] -> m [a]
single :: t -> [t]
mapFst3 :: (t -> t1) -> (t, t2, t3) -> (t1, t2, t3)
mapSnd3 :: (t -> t2) -> (t1, t, t3) -> (t1, t2, t3)
mapThd3 :: (t -> t3) -> (t1, t2, t) -> (t1, t2, t3)
firstMaybes :: [Maybe a] -> Maybe a
hashMapMapWithKey :: (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
hashMapMapKeys :: (Eq k, Hashable k) => (t -> k) -> HashMap t v -> HashMap k v
concatMapM :: (Monad f, Traversable t) => (a1 -> f [a]) -> t a1 -> f [a]
firstElems :: [(ByteString, ByteString)] -> ByteString -> Maybe (Int, ByteString, (ByteString, ByteString))
splitters :: [(ByteString, t)] -> ByteString -> [(Int, t, (ByteString, ByteString))]
bchopAlts :: [(ByteString, ByteString)] -> ByteString -> [ByteString]
chopAlts :: [(String, String)] -> String -> [String]
sortDiff :: (Ord a) => [a] -> [a] -> [a]
angleBrackets :: Doc -> Doc
mkGraph :: (Eq a, Eq b, Hashable a, Hashable b) => [(a, b)] -> HashMap a (HashSet b)
tryIgnore :: String -> IO () -> IO ()
condNull :: Bool -> [a] -> [a]
firstJust :: (a -> Maybe b) -> [a] -> Maybe b
intToString :: Int -> String
mapAccumM :: (Monad m, Traversable t) => (a -> b -> m (a, c)) -> a -> t b -> m (a, t c)
ifM :: (Monad m) => m Bool -> m b -> m b -> m b
nubHashOn :: (Eq k, Hashable k) => (a -> k) -> [a] -> [a]
nubHashLast :: (Eq k, Hashable k) => (a -> k) -> [a] -> [a]
nubHashLastM :: (Eq k, Hashable k, Monad m) => (a -> m k) -> [a] -> m [a]
uniqueByKey :: (Eq k, Hashable k) => [(k, v)] -> Either (k, [v]) [v]
uniqueByKey' :: (Eq k, Hashable k) => ((k, [v]) -> Either e v) -> [(k, v)] -> Either e [v]
join :: (Eq b, Hashable b) => [(a, b)] -> [(b, c)] -> [(a, c)]
-- | This module contains the *types* related creating Errors. It depends
-- only on Fixpoint and basic haskell libraries, and hence, should be
-- importable everywhere.
module Language.Haskell.Liquid.Types.Errors
-- | Generic Type for Error Messages
-- -------------------------------------------
--
-- 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
-- | haskell type location
[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 with a counter-example
ErrSubTypeModel :: !SrcSpan -> !Doc -> !(HashMap Symbol (WithModel t)) -> !(WithModel t) -> !t -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[msg] :: TError t -> !Doc
[ctxM] :: TError t -> !(HashMap Symbol (WithModel t))
[tactM] :: TError t -> !(WithModel t)
[texp] :: TError t -> !t
-- | liquid type error
ErrFCrash :: !SrcSpan -> !Doc -> !(HashMap Symbol t) -> !t -> !t -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[msg] :: TError t -> !Doc
[ctx] :: TError t -> !(HashMap Symbol t)
[tact] :: TError t -> !t
[texp] :: TError t -> !t
-- | condition failure error
ErrAssType :: !SrcSpan -> !Oblig -> !Doc -> !(HashMap Symbol t) -> t -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[obl] :: TError t -> !Oblig
[msg] :: TError t -> !Doc
[ctx] :: TError t -> !(HashMap Symbol t)
[cond] :: TError t -> t
-- | specification parse error
ErrParse :: !SrcSpan -> !Doc -> !ParseError -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[msg] :: TError t -> !Doc
[pErr] :: TError t -> !ParseError
-- | sort error in specification
ErrTySpec :: !SrcSpan -> !Doc -> !t -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[var] :: TError t -> !Doc
[typ] :: TError t -> !t
[msg] :: TError t -> !Doc
-- | sort error in specification
ErrTermSpec :: !SrcSpan -> !Doc -> !Doc -> !Expr -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[var] :: TError t -> !Doc
[msg] :: TError t -> !Doc
[exp] :: TError t -> !Expr
[msg'] :: TError t -> !Doc
-- | multiple alias with same name error
ErrDupAlias :: !SrcSpan -> !Doc -> !Doc -> ![SrcSpan] -> TError t
-- | haskell type location
[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
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[var] :: TError t -> !Doc
[locs] :: TError t -> ![SrcSpan]
-- | multiple definitions of the same instance measure
ErrDupIMeas :: !SrcSpan -> !Doc -> !Doc -> ![SrcSpan] -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[var] :: TError t -> !Doc
[tycon] :: TError t -> !Doc
[locs] :: TError t -> ![SrcSpan]
-- | multiple definitions of the same measure
ErrDupMeas :: !SrcSpan -> !Doc -> ![SrcSpan] -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[var] :: TError t -> !Doc
[locs] :: TError t -> ![SrcSpan]
-- | duplicate fields in same datacon
ErrDupField :: !SrcSpan -> !Doc -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[dcon] :: TError t -> !Doc
[field] :: TError t -> !Doc
-- | name resolves to multiple possible GHC vars
ErrDupNames :: !SrcSpan -> !Doc -> ![Doc] -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[var] :: TError t -> !Doc
[names] :: TError t -> ![Doc]
-- | bad data type specification (?)
ErrBadData :: !SrcSpan -> !Doc -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[var] :: TError t -> !Doc
[msg] :: TError t -> !Doc
-- | refined datacon mismatches haskell datacon
ErrDataCon :: !SrcSpan -> !Doc -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[var] :: TError t -> !Doc
[msg] :: TError t -> !Doc
-- | Invariant sort error
ErrInvt :: !SrcSpan -> !t -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[inv] :: TError t -> !t
[msg] :: TError t -> !Doc
-- | Using sort error
ErrIAl :: !SrcSpan -> !t -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[inv] :: TError t -> !t
[msg] :: TError t -> !Doc
-- | Incompatible using error
ErrIAlMis :: !SrcSpan -> !t -> !t -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[tAs] :: TError t -> !t
[tUs] :: TError t -> !t
[msg] :: TError t -> !Doc
-- | Measure sort error
ErrMeas :: !SrcSpan -> !Doc -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[ms] :: TError t -> !Doc
[msg] :: TError t -> !Doc
-- | Haskell bad Measure error
ErrHMeas :: !SrcSpan -> !Doc -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[ms] :: TError t -> !Doc
[msg] :: TError t -> !Doc
-- | Unbound symbol in specification
ErrUnbound :: !SrcSpan -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[var] :: TError t -> !Doc
-- | Unbound predicate being applied
ErrUnbPred :: !SrcSpan -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[var] :: TError t -> !Doc
-- | GHC error: parsing or type checking
ErrGhc :: !SrcSpan -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[msg] :: TError t -> !Doc
-- | Mismatch between Liquid and Haskell types
ErrMismatch :: !SrcSpan -> !Doc -> !Doc -> !Doc -> !Doc -> !SrcSpan -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[var] :: TError t -> !Doc
[msg] :: TError t -> !Doc
[hs] :: TError t -> !Doc
[lqTy] :: TError t -> !Doc
-- | lq type location
[lqPos] :: TError t -> !SrcSpan
-- | Mismatch in expected/actual args of abstract refinement
ErrPartPred :: !SrcSpan -> !Doc -> !Doc -> !Int -> !Int -> !Int -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[ectr] :: TError t -> !Doc
[var] :: TError t -> !Doc
[argN] :: TError t -> !Int
[expN] :: TError t -> !Int
[actN] :: TError t -> !Int
-- | Cyclic Refined Type Alias Definitions
ErrAliasCycle :: !SrcSpan -> ![(SrcSpan, Doc)] -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[acycle] :: TError t -> ![(SrcSpan, Doc)]
-- | Illegal RTAlias application (from BSort, eg. in PVar)
ErrIllegalAliasApp :: !SrcSpan -> !Doc -> !SrcSpan -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[dname] :: TError t -> !Doc
[dpos] :: TError t -> !SrcSpan
ErrAliasApp :: !SrcSpan -> !Doc -> !SrcSpan -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[dname] :: TError t -> !Doc
[dpos] :: TError t -> !SrcSpan
[msg] :: TError t -> !Doc
-- | Termination Error
ErrTermin :: !SrcSpan -> ![Doc] -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[bind] :: TError t -> ![Doc]
[msg] :: TError t -> !Doc
-- | Refined Class/Interfaces Conflict
ErrRClass :: !SrcSpan -> !Doc -> ![(SrcSpan, Doc)] -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[cls] :: TError t -> !Doc
[insts] :: TError t -> ![(SrcSpan, Doc)]
-- | Non well sorted Qualifier
ErrBadQual :: !SrcSpan -> !Doc -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[qname] :: TError t -> !Doc
[msg] :: TError t -> !Doc
-- | Previously saved error, that carries over after DiffCheck
ErrSaved :: !SrcSpan -> !Doc -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[nam] :: TError t -> !Doc
[msg] :: TError t -> !Doc
ErrFilePragma :: !SrcSpan -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
ErrTyCon :: !SrcSpan -> !Doc -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[msg] :: TError t -> !Doc
[tcname] :: TError t -> !Doc
ErrLiftExp :: !SrcSpan -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[msg] :: TError t -> !Doc
ErrParseAnn :: !SrcSpan -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> !SrcSpan
[msg] :: TError t -> !Doc
-- | Sigh. Other.
ErrOther :: SrcSpan -> !Doc -> TError t
-- | haskell type location
[pos] :: TError t -> SrcSpan
[msg] :: TError t -> !Doc
-- | Context information for Error Messages
-- ------------------------------------
data CtxError t
CtxError :: TError t -> Doc -> CtxError t
[ctErr] :: CtxError t -> TError t
[ctCtx] :: CtxError t -> Doc
errorWithContext :: TError Doc -> IO (CtxError Doc)
-- | Different kinds of Check Obligations
-- ------------------------------------
data Oblig
-- | Obligation that proves termination
OTerm :: Oblig
-- | Obligation that proves invariants
OInv :: Oblig
-- | Obligation that proves subtyping constraints
OCons :: Oblig
data WithModel t
NoModel :: t -> WithModel t
WithModel :: !Doc -> t -> WithModel t
dropModel :: WithModel t -> t
-- | Simple unstructured type for panic
-- ----------------------------------------
type UserError = TError Doc
-- | Construct and show an Error, then crash
panic :: Maybe SrcSpan -> String -> a
-- | Construct and show an Error, then crash
panicDoc :: SrcSpan -> Doc -> a
-- | Construct and show an Error with an optional SrcSpan, then crash This
-- function should be used to mark unimplemented functionality
todo :: Maybe SrcSpan -> String -> a
-- | Construct and show an Error with an optional SrcSpan, then crash This
-- function should be used to mark impossible-to-reach codepaths
impossible :: Maybe SrcSpan -> String -> a
-- | Construct and show an Error, then crash
uError :: UserError -> a
-- | Convert a GHC error into a list of our errors.
sourceErrors :: String -> SourceError -> [TError t]
errDupSpecs :: Doc -> ListNE SrcSpan -> TError t
ppError :: (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError' :: (PPrint a, Show a) => Tidy -> Doc -> Doc -> TError a -> Doc
ppVar :: PPrint a => a -> Doc
realSrcSpan :: FilePath -> Int -> Int -> Int -> Int -> RealSrcSpan
unpackRealSrcSpan :: RealSrcSpan -> (String, Int, Int, Int, Int)
instance GHC.Base.Functor Language.Haskell.Liquid.Types.Errors.CtxError
instance GHC.Base.Functor Language.Haskell.Liquid.Types.Errors.TError
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Errors.TError t)
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Errors.WithModel t)
instance GHC.Classes.Eq t => GHC.Classes.Eq (Language.Haskell.Liquid.Types.Errors.WithModel t)
instance GHC.Show.Show t => GHC.Show.Show (Language.Haskell.Liquid.Types.Errors.WithModel t)
instance GHC.Base.Functor Language.Haskell.Liquid.Types.Errors.WithModel
instance Data.Data.Data Language.Haskell.Liquid.Types.Errors.Oblig
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Errors.Oblig
instance GHC.Classes.Eq (Language.Haskell.Liquid.Types.Errors.CtxError t)
instance GHC.Classes.Ord (Language.Haskell.Liquid.Types.Errors.CtxError t)
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Errors.UserError
instance GHC.Show.Show Language.Haskell.Liquid.Types.Errors.UserError
instance GHC.Exception.Exception Language.Haskell.Liquid.Types.Errors.UserError
instance GHC.Classes.Eq (Language.Haskell.Liquid.Types.Errors.TError a)
instance GHC.Classes.Ord (Language.Haskell.Liquid.Types.Errors.TError a)
instance (Language.Fixpoint.Types.PrettyPrint.PPrint a, GHC.Show.Show a) => Data.Aeson.Types.ToJSON.ToJSON (Language.Haskell.Liquid.Types.Errors.TError a)
instance Data.Aeson.Types.FromJSON.FromJSON (Language.Haskell.Liquid.Types.Errors.TError a)
instance Control.DeepSeq.NFData t => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.Errors.WithModel t)
instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Errors.Oblig
instance GHC.Show.Show Language.Haskell.Liquid.Types.Errors.Oblig
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Errors.Oblig
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Errors.Oblig
instance Language.Fixpoint.Types.PrettyPrint.PPrint Text.Parsec.Error.ParseError
instance Control.DeepSeq.NFData Text.Parsec.Error.ParseError
instance Language.Fixpoint.Types.PrettyPrint.PPrint SrcLoc.SrcSpan
instance Data.Aeson.Types.ToJSON.ToJSON SrcLoc.RealSrcSpan
instance Data.Aeson.Types.FromJSON.FromJSON SrcLoc.RealSrcSpan
instance Data.Aeson.Types.ToJSON.ToJSON SrcLoc.SrcSpan
instance Data.Aeson.Types.FromJSON.FromJSON SrcLoc.SrcSpan
instance Data.Aeson.Types.ToJSON.ToJSONKey SrcLoc.SrcSpan
instance Data.Aeson.Types.FromJSON.FromJSONKey SrcLoc.SrcSpan
-- | 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.GHC.Misc
isAnonBinder :: TyConBinder -> Bool
mkAlive :: Var -> Id
-- | Datatype For Holding GHC ModGuts
-- ------------------------------------------
data MGIModGuts
MI :: !CoreProgram -> !Module -> !Dependencies -> ![ModuleName] -> !GlobalRdrEnv -> ![TyCon] -> ![FamInst] -> !NameSet -> !(Maybe [ClsInst]) -> MGIModGuts
[mgi_binds] :: MGIModGuts -> !CoreProgram
[mgi_module] :: MGIModGuts -> !Module
[mgi_deps] :: MGIModGuts -> !Dependencies
[mgi_dir_imps] :: MGIModGuts -> ![ModuleName]
[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
mg_dir_imps :: ModGuts -> [ModuleName]
mgi_namestring :: MGIModGuts -> String
-- | Encoding and Decoding Location
-- --------------------------------------------
srcSpanTick :: Module -> SrcSpan -> Tickish a
tickSrcSpan :: Outputable a => Tickish a -> SrcSpan
-- | Generic Helpers for Accessing GHC Innards
-- ---------------------------------
stringTyVar :: String -> TyVar
stringVar :: String -> Type -> Var
stringTyCon :: Char -> Int -> String -> TyCon
stringTyConWithKind :: Kind -> Char -> Int -> String -> TyCon
hasBaseTypeVar :: Var -> Bool
isBaseType :: Type -> Bool
validTyVar :: String -> Bool
tvId :: TyVar -> String
tidyCBs :: [CoreBind] -> [CoreBind]
unTick :: CoreBind -> CoreBind
unTickExpr :: CoreExpr -> CoreExpr
isFractionalClass :: Class -> Bool
-- | Pretty Printers
-- -----------------------------------------------------------
tracePpr :: Outputable a => String -> a -> a
pprShow :: Show a => a -> SDoc
toFixSDoc :: Fixpoint a => a -> Doc
sDocDoc :: SDoc -> Doc
pprDoc :: Outputable a => a -> Doc
showPpr :: Outputable a => a -> String
showSDoc :: SDoc -> String
myQualify :: PrintUnqualified
showSDocDump :: SDoc -> String
typeUniqueString :: Outputable a => a -> String
-- | Manipulating Source Spans
-- -------------------------------------------------
newtype Loc
L :: (Int, Int) -> Loc
fSrcSpan :: (Loc a) => a -> SrcSpan
fSrcSpanSrcSpan :: SrcSpan -> SrcSpan
srcSpanFSrcSpan :: SrcSpan -> SrcSpan
sourcePos2SrcSpan :: SourcePos -> SourcePos -> SrcSpan
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
locNamedThing :: NamedThing a => a -> Located a
namedLocSymbol :: (Symbolic a, NamedThing a) => a -> Located Symbol
varLocInfo :: (Type -> a) -> Var -> Located a
namedPanic :: (NamedThing a) => a -> String -> b
-- | Manipulating CoreExpr
-- -----------------------------------------------------
collectArguments :: Int -> CoreExpr -> [Var]
collectValBinders' :: Expr Var -> ([Var], Expr Var)
ignoreLetBinds :: Expr t -> Expr t
-- | Predicates on CoreExpr and DataCons
-- ---------------------------------------
isTupleId :: Id -> Bool
idDataConM :: Id -> Maybe DataCon
isDataConId :: Id -> Bool
getDataConVarUnique :: Var -> Unique
isDictionaryExpression :: Expr Id -> Maybe Id
realTcArity :: TyCon -> Arity
kindTCArity :: TyCon -> Arity
kindArity :: Kind -> Arity
uniqueHash :: Uniquable a => Int -> a -> Int
lookupRdrName :: HscEnv -> ModuleName -> RdrName -> IO (Maybe Name)
qualImportDecl :: ModuleName -> ImportDecl name
ignoreInline :: ParsedModule -> ParsedModule
-- | Symbol Conversions
-- --------------------------------------------------------
symbolTyConWithKind :: Kind -> Char -> Int -> Symbol -> TyCon
symbolTyCon :: Char -> Int -> Symbol -> TyCon
symbolTyVar :: Symbol -> TyVar
localVarSymbol :: Var -> Symbol
exportedVarSymbol :: Var -> Symbol
qualifiedNameSymbol :: Name -> Symbol
fastStringText :: FastString -> Text
tyConTyVarsDef :: TyCon -> [TyVar]
noTyVars :: TyCon -> Bool
-- | Symbol Instances
-- |
-- - NOTE:REFLECT-IMPORTS we **eschew** the unique
-- suffix for exported vars, to make it possible to lookup names from
-- symbols _across_ modules; anyways exported names are top-level and you
-- shouldn't have local binders that shadow them. However, we **keep**
-- the unique suffix for local variables, as otherwise there are
-- spurious, but extremely problematic, name collisions in the fixpoint
-- environment.
--
-- | Manipulating Symbols
-- ------------------------------------------------------
splitModuleName :: Symbol -> (Symbol, Symbol)
dropModuleNamesAndUnique :: Symbol -> Symbol
dropModuleNames :: Symbol -> Symbol
dropModuleNamesCorrect :: Symbol -> Symbol
takeModuleNames :: Symbol -> Symbol
dropModuleUnique :: Symbol -> Symbol
cmpSymbol :: Symbol -> Symbol -> Bool
sepModNames :: Text
sepUnique :: Text
mungeNames :: (String -> [Text] -> Symbol) -> Text -> String -> Symbol -> Symbol
qualifySymbol :: Symbol -> Symbol -> Symbol
isQualified :: Text -> Bool
wrapParens :: (IsString a, Monoid a) => a -> a
isParened :: Text -> Bool
isDictionary :: Symbolic a => a -> Bool
isInternal :: Symbolic a => a -> Bool
stripParens :: Text -> Text
stripParensSym :: Symbol -> Symbol
desugarModule :: TypecheckedModule -> Ghc DesugaredModule
-- | GHC Compatibility Layer
-- ---------------------------------------------------
gHC_VERSION :: String
symbolFastString :: Symbol -> FastString
type Prec = TyPrec
lintCoreBindings :: [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
synTyConRhs_maybe :: TyCon -> Maybe Type
tcRnLookupRdrName :: HscEnv -> Located RdrName -> IO (Messages, Maybe [Name])
showCBs :: Bool -> [CoreBind] -> String
findVarDef :: Symbol -> [CoreBind] -> Maybe (Var, CoreExpr)
coreBindSymbols :: CoreBind -> [Symbol]
simplesymbol :: (NamedThing t) => t -> Symbol
binders :: Bind a -> [a]
instance GHC.Show.Show Language.Haskell.Liquid.GHC.Misc.Loc
instance GHC.Classes.Ord Language.Haskell.Liquid.GHC.Misc.Loc
instance GHC.Classes.Eq Language.Haskell.Liquid.GHC.Misc.Loc
instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.GHC.Misc.Loc
instance Outputable.Outputable a => Outputable.Outputable (Data.HashSet.HashSet a)
instance Data.Hashable.Class.Hashable SrcLoc.SrcSpan
instance Language.Fixpoint.Types.Names.Symbolic FastString.FastString
instance Language.Fixpoint.Types.Names.Symbolic TyCon.TyCon
instance Language.Fixpoint.Types.Names.Symbolic Class.Class
instance Language.Fixpoint.Types.Names.Symbolic Name.Name
instance Language.Fixpoint.Types.Names.Symbolic Var.Var
instance Data.Hashable.Class.Hashable Var.Var
instance Data.Hashable.Class.Hashable TyCon.TyCon
instance Language.Fixpoint.Types.PrettyPrint.Fixpoint Var.Var
instance Language.Fixpoint.Types.PrettyPrint.Fixpoint Name.Name
instance Language.Fixpoint.Types.PrettyPrint.Fixpoint TyCoRep.Type
instance GHC.Show.Show Name.Name
instance GHC.Show.Show Var.Var
instance GHC.Show.Show Class.Class
instance GHC.Show.Show TyCon.TyCon
instance Control.DeepSeq.NFData Class.Class
instance Control.DeepSeq.NFData TyCon.TyCon
instance Control.DeepSeq.NFData TyCoRep.Type
instance Control.DeepSeq.NFData Var.Var
-- | Formats Haskell source code as HTML with CSS and Mouseover Type
-- Annotations
module Language.Haskell.Liquid.UX.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 -> (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
tokeniseWithLoc :: CommentTransform -> String -> [(TokenType, String, Loc)]
instance GHC.Show.Show Language.Haskell.Liquid.UX.ACSS.Lit
instance GHC.Show.Show Language.Haskell.Liquid.UX.ACSS.Annotation
instance GHC.Show.Show Language.Haskell.Liquid.UX.ACSS.Status
instance GHC.Classes.Ord Language.Haskell.Liquid.UX.ACSS.Status
instance GHC.Classes.Eq Language.Haskell.Liquid.UX.ACSS.Status
instance GHC.Show.Show Language.Haskell.Liquid.UX.ACSS.AnnMap
-- | This module contains a wrappers and utility functions for accessing
-- GHC module information. It should NEVER depend on
module Language.Haskell.Liquid.GHC.TypeRep
mkTyArg :: TyVar -> TyVarBinder
showTy :: Type -> String
instance (GHC.Classes.Eq tyvar, GHC.Classes.Eq argf) => GHC.Classes.Eq (Var.TyVarBndr tyvar argf)
instance Language.Haskell.Liquid.GHC.TypeRep.SubstTy TyCoRep.Type
instance Language.Haskell.Liquid.GHC.TypeRep.SubstTy TyCoRep.Coercion
instance Language.Haskell.Liquid.GHC.TypeRep.SubstTy CoAxiom.Role
instance Language.Haskell.Liquid.GHC.TypeRep.SubstTy (CoAxiom.CoAxiom CoAxiom.Branched)
instance Language.Haskell.Liquid.GHC.TypeRep.SubstTy TyCoRep.UnivCoProvenance
instance Language.Haskell.Liquid.GHC.TypeRep.SubstTy CoAxiom.CoAxiomRule
instance (Language.Haskell.Liquid.GHC.TypeRep.SubstTy a, GHC.Base.Functor m) => Language.Haskell.Liquid.GHC.TypeRep.SubstTy (m a)
instance GHC.Classes.Eq TyCoRep.Type
instance GHC.Classes.Eq TyCoRep.Coercion
module Language.Haskell.Liquid.Types.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 Language.Haskell.Liquid.Types.Visitors.CBVisitable [CoreSyn.CoreBind]
instance Language.Haskell.Liquid.Types.Visitors.CBVisitable CoreSyn.CoreBind
instance Language.Haskell.Liquid.Types.Visitors.CBVisitable (CoreSyn.Expr Var.Var)
instance Language.Haskell.Liquid.Types.Visitors.CBVisitable (CoreSyn.Alt Var.Var)
instance Language.Haskell.Liquid.Types.Visitors.CBVisitable CoreSyn.AltCon
module Language.Haskell.Liquid.GHC.SpanStack
-- | A single span
data Span
-- | binder for whom we are generating constraint
Var :: !Var -> Span
-- | nearest known Source Span
Tick :: !(Tickish Var) -> Span
-- | Opaque type for a stack of spans
data SpanStack
empty :: SpanStack
push :: Span -> SpanStack -> SpanStack
srcSpan :: SpanStack -> SrcSpan
showSpan :: (Show a) => a -> SrcSpan
instance GHC.Show.Show Language.Haskell.Liquid.GHC.SpanStack.Span
module Language.Haskell.Liquid.GHC.Play
dataConImplicitIds :: DataCon -> [Id]
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
substExpr :: HashMap Var Var -> CoreExpr -> CoreExpr
mapType :: (Type -> Type) -> Type -> Type
stringClassArg :: Type -> Maybe Type
instance Language.Haskell.Liquid.GHC.Play.Subable CoreSyn.CoreExpr
instance Language.Haskell.Liquid.GHC.Play.Subable TyCoRep.Coercion
instance Language.Haskell.Liquid.GHC.Play.Subable (CoreSyn.Alt Var.Var)
instance Language.Haskell.Liquid.GHC.Play.Subable Var.Var
instance Language.Haskell.Liquid.GHC.Play.Subable (CoreSyn.Bind Var.Var)
instance Language.Haskell.Liquid.GHC.Play.Subable TyCoRep.Type
module Gradual.PrettyPrinting
class Pretty a
pretty :: Pretty a => a -> String
simplifyExpr :: Expr -> Expr
instance Gradual.PrettyPrinting.Pretty Language.Fixpoint.Types.Refinements.Expr
instance Gradual.PrettyPrinting.Pretty Language.Fixpoint.Types.Refinements.KVar
instance Gradual.PrettyPrinting.Pretty Language.Fixpoint.Types.Names.Symbol
instance (Gradual.PrettyPrinting.Pretty a, Gradual.PrettyPrinting.Pretty b) => Gradual.PrettyPrinting.Pretty (a, b)
instance Gradual.PrettyPrinting.Pretty a => Gradual.PrettyPrinting.Pretty [a]
module Gradual.GUI.Types
data Unique
Unique :: Int -> SrcSpan -> Symbol -> Unique
[uId] :: Unique -> Int
[uLoc] :: Unique -> SrcSpan
[uName] :: Unique -> Symbol
type LocTokens = [(TokenType, String, Loc)]
type Deps = Dependencies ()
type SDeps = Dependencies String
type Dependencies val = [(Unique, [(Unique, val)])]
type PKeys = [[KVar]]
makePKeys :: [[GSub a]] -> PKeys
kVarId :: Dependencies v -> KVar -> (Int, Int)
srcDeps :: Dependencies v -> [(Int, Int, SrcSpan, v)]
gSpanToDeps :: GSub a -> GSpan -> SDeps
kVarSpan :: Symbol -> SrcSpan
takeFileName :: String -> String
symbolLoc :: Symbol -> Loc
instance GHC.Show.Show Gradual.GUI.Types.Unique
module Gradual.GUI.Annotate
renderHtml :: FilePath -> String -> LocTokens -> SDeps -> String
-- | This module should contain all the global type definitions and basic
-- instances.
module Language.Haskell.Liquid.Types
data Config
Config :: [FilePath] -> [FilePath] -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> [String] -> Bool -> Bool -> Bool -> Int -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Maybe Int -> Int -> Int -> Int -> Maybe SMTSolver -> Bool -> Bool -> Bool -> [String] -> [String] -> Eliminate -> Int -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Maybe Int -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Instantiate -> Bool -> Bool -> Bool -> Bool -> 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
-- | uninterpreted integer multiplication and division
[linear] :: Config -> Bool
-- | interpretation of string theory in the logic
[stringTheory] :: Config -> Bool
-- | allow higher order binders into the logic
[higherorder] :: Config -> Bool
-- | allow higher order qualifiers
[higherorderqs] :: Config -> Bool
-- | allow function extentionality axioms
[extensionality] :: Config -> Bool
-- | allow lambda alpha-equivalence axioms
[alphaEquivalence] :: Config -> Bool
-- | allow lambda beta-equivalence axioms
[betaEquivalence] :: Config -> Bool
-- | allow lambda normalization-equivalence axioms
[normalForm] :: Config -> Bool
-- | check all binders (overrides diffcheck)
[fullcheck] :: Config -> Bool
-- | save fixpoint query
[saveQuery] :: Config -> Bool
-- | set of binders to check
[checks] :: Config -> [String]
-- | whether to complain about specifications for unexported and unused
-- values
[noCheckUnknown] :: Config -> Bool
-- | disable termination check
[notermination] :: Config -> Bool
-- | enable gradual type checking
[gradual] :: Config -> Bool
-- | depth of gradual concretization
[gdepth] :: Config -> Int
-- | interactive gradual solving
[ginteractive] :: Config -> Bool
-- | Check for termination and totality, Overrides no-termination flags
[totalHaskell] :: Config -> Bool
-- | automatically construct proofs from axioms
[autoproofs] :: Config -> Bool
-- | disable warnings output (only show errors)
[nowarnings] :: Config -> Bool
-- | disable creation of intermediate annotation files
[noannotations] :: 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
-- | disable totality check in definitions
[nototality] :: Config -> Bool
-- | enable prunning unsorted Refinements
[pruneUnsorted] :: Config -> Bool
-- | number of cores used to solve constraints
[cores] :: Config -> Maybe Int
-- | Minimum size of a partition
[minPartSize] :: Config -> Int
-- | Maximum size of a partition. Overrides minPartSize
[maxPartSize] :: Config -> Int
-- | 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]
-- | eliminate (i.e. don't use qualifs for) for "none", "cuts" or "all"
-- kvars
[eliminate] :: Config -> Eliminate
-- | port at which lhi should listen
[port] :: Config -> Int
-- | Automatically generate singleton types for data constructors
[exactDC] :: Config -> Bool
-- | Disable ADTs (only used with exactDC)
[noADT] :: Config -> Bool
-- | Do not automatically lift data constructor fields into measures
[noMeasureFields] :: Config -> Bool
-- | scrape qualifiers from imported specifications
[scrapeImports] :: Config -> Bool
-- | scrape qualifiers from auto specifications
[scrapeInternals] :: Config -> Bool
-- | scrape qualifiers from used, imported specifications
[scrapeUsedImports] :: Config -> Bool
-- | print eliminate stats
[elimStats] :: Config -> Bool
-- | eliminate upto given depth of KVar chains
[elimBound] :: Config -> Maybe Int
-- | print results (safe/errors) as JSON
[json] :: Config -> Bool
-- | attempt to generate counter-examples to type errors
[counterExamples] :: Config -> Bool
-- | check and time each (asserted) type-sig separately
[timeBinds] :: Config -> Bool
-- | treat code patterns (e.g. e1 >>= x -> e2) specially for
-- inference
[noPatternInline] :: Config -> Bool
-- | print full blown core (with untidy names) in verbose mode
[untidyCore] :: Config -> Bool
-- | simplify GHC core before constraint-generation
[noSimplifyCore] :: Config -> Bool
-- | treat non-linear kvars as cuts
[nonLinCuts] :: Config -> Bool
-- | How to instantiate axioms NO-TRIGGER , proofMethod :: ProofMethod -- ^
-- How to create automatic instances NO-TRIGGER , fuel :: Int -- ^ Fuel
-- for axiom instantiation
[autoInstantiate] :: Config -> Instantiate
-- | Debug Instantiation
[debugInstantionation] :: Config -> Bool
-- | Disable non-concrete KVar slicing
[noslice] :: Config -> Bool
-- | Disable loading lifted specifications (for "legacy" libs)
[noLiftedImport] :: Config -> Bool
-- | Enable proof-by-logical-evaluation
[proofLogicEval] :: Config -> Bool
class HasConfig t
getConfig :: HasConfig t => t -> Config
patternFlag :: HasConfig t => t -> Bool
higherOrderFlag :: HasConfig t => t -> Bool
pruneFlag :: HasConfig t => t -> Bool
expandFlag :: HasConfig t => t -> Bool
hasOpt :: HasConfig t => t -> (Config -> Bool) -> Bool
totalityCheck :: HasConfig t => t -> Bool
terminationCheck :: HasConfig t => t -> Bool
-- | GHC Information : Code & Spec ------------------------------
data GhcInfo
GI :: !FilePath -> !ModuleName -> !HscEnv -> ![CoreBind] -> ![Var] -> ![Var] -> ![Var] -> ![Var] -> ![FilePath] -> ![String] -> ![FilePath] -> !GhcSpec -> GhcInfo
-- | Source file for module
[target] :: GhcInfo -> !FilePath
-- | Name for module
[targetMod] :: GhcInfo -> !ModuleName
-- | GHC Env used to resolve names for module
[env] :: GhcInfo -> !HscEnv
-- | Source Code
[cbs] :: GhcInfo -> ![CoreBind]
-- | ?
[derVars] :: GhcInfo -> ![Var]
-- | Binders that are _read_ in module (but not defined?)
[impVars] :: GhcInfo -> ![Var]
-- | (Top-level) binders that are _defined_ in module
[defVars] :: GhcInfo -> ![Var]
-- | Binders that are _read_ in module , tyCons :: ![TyCon] -- ^ Types that
-- are defined inside module
[useVars] :: GhcInfo -> ![Var]
-- | Imported .hqual files
[hqFiles] :: GhcInfo -> ![FilePath]
-- | ??? dead?
[imports] :: GhcInfo -> ![String]
-- | ??? dead?
[includes] :: GhcInfo -> ![FilePath]
-- | All specification information for module
[spec] :: GhcInfo -> !GhcSpec
-- | The following is the overall type for specifications obtained
-- from parsing the target source and dependent libraries
data GhcSpec
SP :: ![(Var, LocSpecType)] -> ![(Var, LocSpecType)] -> ![(Var, LocSpecType)] -> ![(Var, LocSpecType)] -> ![(Symbol, LocSpecType)] -> ![(Symbol, LocSpecType)] -> ![(Maybe Var, LocSpecType)] -> ![(LocSpecType, LocSpecType)] -> ![Located DataCon] -> ![(TyCon, TyConP)] -> ![(Symbol, Var)] -> TCEmb TyCon -> ![Qualifier] -> ![DataDecl] -> ![Var] -> ![(Var, [Int])] -> ![(Var, [Located Expr])] -> ![(TyCon, LocSpecType)] -> !(HashSet Var) -> !(HashSet Var) -> !(HashSet TyCon) -> !(HashMap Var (Maybe Int)) -> !Config -> !NameSet -> [Measure SpecType DataCon] -> HashMap TyCon RTyCon -> DEnv Var SpecType -> [AxiomEq] -> [Var] -> LogicMap -> Maybe Type -> !RTEnv -> GhcSpec
-- | Asserted Reftypes
[gsTySigs] :: GhcSpec -> ![(Var, LocSpecType)]
-- | Assumed Reftypes
[gsAsmSigs] :: GhcSpec -> ![(Var, LocSpecType)]
-- | Auto generated Signatures
[gsInSigs] :: GhcSpec -> ![(Var, LocSpecType)]
-- | Data Constructor Measure Sigs
[gsCtors] :: GhcSpec -> ![(Var, LocSpecType)]
-- | Literals/Constants e.g. datacons: EQ, GT, string lits: "zombie",...
[gsLits] :: GhcSpec -> ![(Symbol, LocSpecType)]
-- | Measure Types eg. len :: [a] -> Int
[gsMeas] :: GhcSpec -> ![(Symbol, LocSpecType)]
-- | Data Type Invariants that came from the definition of var measure eg.
-- forall a. {v: [a] | len(v) >= 0}
[gsInvariants] :: GhcSpec -> ![(Maybe Var, LocSpecType)]
-- | Data Type Invariant Aliases
[gsIaliases] :: GhcSpec -> ![(LocSpecType, LocSpecType)]
-- | Predicated Data-Constructors e.g. see testsposMap.hs
[gsDconsP] :: GhcSpec -> ![Located DataCon]
-- | Predicated Type-Constructors eg. see testsposMap.hs
[gsTconsP] :: GhcSpec -> ![(TyCon, TyConP)]
-- | List of Symbol free in spec and corresponding GHC var eg.
-- (Cons, Cons#7uz) from testsposex1.hs
[gsFreeSyms] :: GhcSpec -> ![(Symbol, Var)]
-- | How to embed GHC Tycons into fixpoint sorts e.g. "embed Set as
-- Set_set" from includeDataSet.spec
[gsTcEmbeds] :: GhcSpec -> TCEmb TyCon
-- | Qualifiers in Source/Spec files e.g testsposqualTest.hs
[gsQualifiers] :: GhcSpec -> ![Qualifier]
-- | ADTs extracted from Haskell 'data' definitions
[gsADTs] :: GhcSpec -> ![DataDecl]
-- | Top-level Binders To Verify (empty means ALL binders)
[gsTgtVars] :: GhcSpec -> ![Var]
-- | Lexicographically ordered size witnesses for termination
[gsDecr] :: GhcSpec -> ![(Var, [Int])]
-- | Lexicographically ordered expressions for termination
[gsTexprs] :: GhcSpec -> ![(Var, [Located Expr])]
-- | Mapping of 'newtype' type constructors with their refined types.
[gsNewTypes] :: GhcSpec -> ![(TyCon, LocSpecType)]
-- | Variables that should be checked in the environment they are used
[gsLvars] :: GhcSpec -> !(HashSet Var)
-- | Binders to IGNORE during termination checking
[gsLazy] :: GhcSpec -> !(HashSet Var)
-- | Binders to IGNORE during termination checking
[gsAutosize] :: GhcSpec -> !(HashSet TyCon)
-- | Binders to expand with automatic axiom instances maybe with specified
-- fuel
[gsAutoInst] :: GhcSpec -> !(HashMap Var (Maybe Int))
-- | Configuration Options
[gsConfig] :: GhcSpec -> !Config
-- | Names exported by the module being verified
[gsExports] :: GhcSpec -> !NameSet
[gsMeasures] :: GhcSpec -> [Measure SpecType DataCon]
[gsTyconEnv] :: GhcSpec -> HashMap TyCon RTyCon
-- | Dictionary Environment
[gsDicts] :: GhcSpec -> DEnv Var SpecType
-- | Axioms from reflected functions
[gsAxioms] :: GhcSpec -> [AxiomEq]
-- | Binders for reflected functions
[gsReflects] :: GhcSpec -> [Var]
[gsLogicMap] :: GhcSpec -> LogicMap
[gsProofType] :: GhcSpec -> Maybe Type
-- | Refinement type aliases
[gsRTAliases] :: GhcSpec -> !RTEnv
-- | Which Top-Level Binders Should be Verified
data TargetVars
AllVars :: TargetVars
Only :: ![Var] -> TargetVars
data Located a :: * -> *
Loc :: !SourcePos -> !SourcePos -> !a -> Located a
-- | Start Position
[loc] :: Located a -> !SourcePos
-- | End Position
[locE] :: Located a -> !SourcePos
[val] :: Located a -> !a
dummyLoc :: () => a -> Located a
-- | Located Symbols -----------------------------------------------------
type LocSymbol = Located Symbol
type LocText = Located Text
dummyName :: Symbol
isDummy :: Symbolic a => a -> Bool
data BTyCon
BTyCon :: !LocSymbol -> !Bool -> !Bool -> BTyCon
-- | TyCon name with location information
[btc_tc] :: BTyCon -> !LocSymbol
-- | Is this a class type constructor?
[btc_class] :: BTyCon -> !Bool
-- | Is Promoted Data Con?
[btc_prom] :: BTyCon -> !Bool
mkBTyCon :: LocSymbol -> BTyCon
mkClassBTyCon :: LocSymbol -> BTyCon
mkPromotedBTyCon :: LocSymbol -> BTyCon
isClassBTyCon :: BTyCon -> Bool
newtype BTyVar
BTV :: Symbol -> BTyVar
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 :: b - Prop, q :: Int -> Prop, r :: a ->
-- Prop> = F (ar -> bp) | Q (c -> a) | G
-- (Intq -> ar)
--
-- there will be:
--
-- varianceTyArgs = [Bivariant , Covariant, Contravatiant, Invariant]
-- variancePsArgs = [Covariant, Contravatiant, Bivariant]
data TyConInfo
TyConInfo :: !VarianceInfo -> !VarianceInfo -> !(Maybe SizeFun) -> TyConInfo
-- | variance info for type variables
[varianceTyArgs] :: TyConInfo -> !VarianceInfo
-- | variance info for predicate variables
[variancePsArgs] :: TyConInfo -> !VarianceInfo
-- | logical UNARY function that computes the size of the structure
[sizeFunction] :: TyConInfo -> !(Maybe SizeFun)
defaultTyConInfo :: TyConInfo
rTyConPVs :: RTyCon -> [RPVar]
rTyConPropVs :: RTyCon -> [PVar RSort]
isClassRTyCon :: RTyCon -> Bool
isClassType :: TyConable c => RType c t t1 -> Bool
isEqType :: TyConable c => RType c t t1 -> Bool
isRVar :: RType c tv r -> Bool
-- | Accessors for RTyCon
isBool :: RType RTyCon 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 :: !(RTVU c tv) -> !(RType c tv r) -> RType c tv r
[rt_tvbind] :: RType c tv r -> !(RTVU c tv)
[rt_ty] :: RType c tv r -> !(RType c tv r)
-- | "forall x y :: Nat, w :: Int . TYPE" ^^^^^^^^^^^^^^^^^^^
-- (rt_pvbind)
RAllP :: !(PVU c tv) -> !(RType c tv r) -> RType c tv r
[rt_pvbind] :: RType c tv r -> !(PVU c tv)
[rt_ty] :: RType c tv r -> !(RType c tv r)
-- | "forall w . TYPE" ^^^^^ (rt_sbind)
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 testsposvector2.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
-- testsposHoles.hs
RHole :: r -> RType c tv r
-- | Ref describes `Prop τ` and HProp arguments applied
-- to type constructors. For example, in [a]- v > h}>, we
-- apply (via RApp) * the RProp denoted by `{h -> v >
-- h}` to * the RTyCon denoted by `[]`. Thus, Ref 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 Predicate argument in ur_pred in the
-- UReft applies directly to any type and has semantics
-- _independent of_ the data-type.
data Ref τ t
RProp :: [(Symbol, τ)] -> t -> Ref τ t
[rf_args] :: Ref τ t -> [(Symbol, τ)]
-- | Abstract refinement associated with RTyCon
[rf_body] :: Ref τ t -> t
-- | RTProp is a convenient alias for Ref that will save
-- a bunch of typing. In general, perhaps we need not expose Ref
-- directly at all.
type RTProp c tv r = Ref (RType c tv ()) (RType c tv r)
rPropP :: [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
newtype RTyVar
RTV :: TyVar -> RTyVar
-- | Refinement Type Aliases
data RTAlias x a
RTA :: Symbol -> [x] -> [x] -> a -> SourcePos -> SourcePos -> RTAlias x a
-- | name of the alias
[rtName] :: RTAlias x a -> Symbol
-- | type parameters
[rtTArgs] :: RTAlias x a -> [x]
-- | value parameters
[rtVArgs] :: RTAlias x a -> [x]
-- | what the alias expands to
[rtBody] :: RTAlias x a -> a
-- | start position
[rtPos] :: RTAlias x a -> SourcePos
-- | end position
[rtPosE] :: RTAlias x a -> SourcePos
type OkRT c tv r = (TyConable c, PPrint tv, PPrint c, PPrint r, Reftable r, Reftable (RTProp c tv ()), Reftable (RTProp c tv r), Eq c, Eq tv, Hashable tv)
lmapEAlias :: LMap -> RTAlias Symbol Expr
data HSeg t
HBind :: !Symbol -> t -> HSeg t
[hs_addr] :: HSeg t -> !Symbol
[hs_val] :: HSeg t -> t
HVar :: UsedPVar -> HSeg t
-- | A World 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
-- HVar in a list.
newtype World t
World :: [HSeg t] -> World t
class (Eq c) => TyConable c
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
isEqual :: TyConable c => c -> Bool
isNumCls :: TyConable c => c -> Bool
isFracCls :: TyConable c => c -> Bool
class SubsTy tv ty a
subt :: SubsTy tv ty a => (tv, ty) -> a -> a
data RTVar tv s
RTVar :: tv -> RTVInfo s -> RTVar tv s
[ty_var_value] :: RTVar tv s -> tv
[ty_var_info] :: RTVar tv s -> RTVInfo s
data RTVInfo s
RTVNoInfo :: RTVInfo s
RTVInfo :: Symbol -> s -> Bool -> RTVInfo s
[rtv_name] :: RTVInfo s -> Symbol
[rtv_kind] :: RTVInfo s -> s
[rtv_is_val] :: RTVInfo s -> Bool
makeRTVar :: tv -> RTVar tv s
mapTyVarValue :: (tv1 -> tv2) -> RTVar tv1 s -> RTVar tv2 s
dropTyVarInfo :: RTVar tv s1 -> RTVar tv s2
rTVarToBind :: RTVar RTyVar s -> Maybe (Symbol, s)
-- | 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
MkUReft :: !r -> !Predicate -> !Strata -> UReft r
[ur_reft] :: UReft r -> !r
[ur_pred] :: UReft r -> !Predicate
[ur_strata] :: UReft r -> !Strata
-- | Termination expressions
data SizeFun
-- | x -> F.EVar x
IdSizeFun :: SizeFun
-- | x -> f x
SymSizeFun :: LocSymbol -> SizeFun
szFun :: SizeFun -> Symbol -> Expr
-- | Data type refinements
data DataDecl
D :: DataName -> [Symbol] -> [PVar BSort] -> [Symbol] -> [DataCtor] -> !SourcePos -> Maybe SizeFun -> Maybe BareType -> !DataDeclKind -> DataDecl
-- | Type Constructor Name
[tycName] :: DataDecl -> DataName
-- | Tyvar Parameters
[tycTyVars] :: DataDecl -> [Symbol]
-- | PVar Parameters
[tycPVars] :: DataDecl -> [PVar BSort]
-- | PLabel Parameters
[tycTyLabs] :: DataDecl -> [Symbol]
-- | Data Constructors
[tycDCons] :: DataDecl -> [DataCtor]
-- | Source Position
[tycSrcPos] :: DataDecl -> !SourcePos
-- | Default termination measure
[tycSFun] :: DataDecl -> Maybe SizeFun
-- | Type of Ind-Prop
[tycPropTy] :: DataDecl -> Maybe BareType
-- | User-defined or Auto-lifted
[tycKind] :: DataDecl -> !DataDeclKind
-- | The name of the TyCon corresponding to a DataDecl
data DataName
-- | for isVanillyAlgTyCon we can directly use the TyCon
-- name
DnName :: !LocSymbol -> DataName
-- | for FamInst TyCon we save some DataCon name
DnCon :: !LocSymbol -> DataName
dataNameSymbol :: DataName -> LocSymbol
-- | Data Constructor
data DataCtor
DataCtor :: LocSymbol -> [(Symbol, BareType)] -> Maybe BareType -> DataCtor
-- | DataCon name
[dcName] :: DataCtor -> LocSymbol
-- |
-- - (fieldName, fieldType)
--
[dcFields] :: DataCtor -> [(Symbol, BareType)]
-- | Possible output (if in GADT form)
[dcResult] :: DataCtor -> Maybe BareType
data DataConP
DataConP :: !SourcePos -> ![RTyVar] -> ![PVar RSort] -> ![Symbol] -> ![SpecType] -> ![(Symbol, SpecType)] -> !SpecType -> !Bool -> !Symbol -> !SourcePos -> DataConP
[dc_loc] :: DataConP -> !SourcePos
-- | Type parameters
[freeTyVars] :: DataConP -> ![RTyVar]
-- | Abstract Refinement parameters
[freePred] :: DataConP -> ![PVar RSort]
-- | ? strata stuff
[freeLabels] :: DataConP -> ![Symbol]
-- | ? Class constraints (via dataConStupidTheta)
[tyConstrs] :: DataConP -> ![SpecType]
-- | Value parameters
[tyArgs] :: DataConP -> ![(Symbol, SpecType)]
-- | Result type , tyData :: !SpecType -- ^ The generic ADT, see
-- [NOTE:DataCon-Data]
[tyRes] :: DataConP -> !SpecType
-- | Was this specified in GADT style (if so, DONT use function names as
-- fields)
[dcpIsGadt] :: DataConP -> !Bool
-- | Which module was this defined in
[dcpModule] :: DataConP -> !Symbol
[dc_locE] :: DataConP -> !SourcePos
data HasDataDecl
NoDecl :: (Maybe SizeFun) -> HasDataDecl
HasDecl :: HasDataDecl
hasDecl :: DataDecl -> HasDataDecl
-- | What kind of DataDecl is it?
data DataDeclKind
-- | User defined data-definitions (should have refined fields)
DataUser :: DataDeclKind
-- | Automatically lifted data-definitions (do not have refined fields)
DataReflected :: DataDeclKind
data TyConP
TyConP :: !SourcePos -> ![RTyVar] -> ![PVar RSort] -> ![Symbol] -> !VarianceInfo -> !VarianceInfo -> !(Maybe SizeFun) -> TyConP
[ty_loc] :: TyConP -> !SourcePos
[freeTyVarsTy] :: TyConP -> ![RTyVar]
[freePredTy] :: TyConP -> ![PVar RSort]
[freeLabelTy] :: TyConP -> ![Symbol]
[varianceTs] :: TyConP -> !VarianceInfo
[variancePs] :: TyConP -> !VarianceInfo
[sizeFun] :: TyConP -> !(Maybe SizeFun)
type RRType = RType RTyCon RTyVar
type RRProp r = Ref RSort (RRType r)
type BRType = RType BTyCon BTyVar
type BRProp r = Ref BSort (BRType r)
type BSort = BRType ()
type BPVar = PVar BSort
type RTVU c tv = RTVar tv (RType c tv ())
type PVU c tv = PVar (RType c tv ())
type BareType = BRType RReft
type PrType = RRType Predicate
type SpecType = RRType RReft
type SpecProp = RRProp RReft
type SpecRep = RRep RReft
type LocBareType = Located BareType
type LocSpecType = Located SpecType
type RSort = RRType ()
-- | Predicates
-- ----------------------------------------------------------------
type UsedPVar = PVar ()
type RPVar = PVar RSort
type RReft = UReft Reft
-- | The type used during constraint generation, used also to define
-- contexts for errors, hence in this file, and NOT in elsewhere. **DO
-- NOT ATTEMPT TO MOVE** Am splitting into + global : many bindings,
-- shared across all constraints + local : few bindings, relevant to
-- particular constraints
data REnv
REnv :: HashMap Symbol SpecType -> HashMap Symbol SpecType -> REnv
-- | the "global" names for module
[reGlobal] :: REnv -> HashMap Symbol SpecType
-- | the "local" names for sub-exprs
[reLocal] :: REnv -> HashMap Symbol SpecType
-- | Constructor and Destructors for RTypes
-- ------------------------------------
data RTypeRep c tv r
RTypeRep :: [RTVar tv (RType c 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 -> [RTVar tv (RType c 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 tv r -> RType c tv r
toRTypeRep :: RType c tv r -> RTypeRep c tv r
mkArrow :: [RTVar tv (RType c tv ())] -> [PVar (RType c tv ())] -> [Symbol] -> [(Symbol, RType c tv r, r)] -> RType c tv r -> RType c tv 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 :: (Foldable t, Foldable t1, Foldable t2) => t (RTVar tv (RType c tv ())) -> t1 (PVar (RType c tv ())) -> t2 Symbol -> RType c tv r -> RType c tv r
bkUniv :: RType t1 a t2 -> ([RTVar a (RType t1 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] -> Expr
isBase :: RType t t1 t2 -> Bool
isFunTy :: RType t t1 t2 -> Bool
isTrivial :: (Reftable r, TyConable c) => RType c tv r -> Bool
efoldReft :: (Reftable r, TyConable c) => (Symbol -> RType c tv r -> Bool) -> (c -> [RType c tv r] -> [(Symbol, a)]) -> (RTVar tv (RType c tv ()) -> [(Symbol, a)]) -> (RType c tv r -> a) -> (SEnv a -> Maybe (RType c tv r) -> r -> b -> b) -> (PVar (RType c tv ()) -> SEnv a -> SEnv a) -> SEnv a -> b -> RType c tv r -> b
foldReft :: (Reftable r, TyConable c) => (SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a
foldReft' :: (Reftable r, TyConable c) => (Symbol -> RType c tv r -> Bool) -> (RType c tv r -> b) -> (SEnv b -> Maybe (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a
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)
mapPropM :: (Monad m) => (RTProp c tv r -> m (RTProp c tv r)) -> RType c tv r -> m (RType c tv r)
mapBot :: (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBind :: (Symbol -> Symbol) -> RType c tv r -> RType c tv r
foldRType :: (acc -> RType c tv r -> acc) -> acc -> RType c tv r -> acc
-- | Different kinds of Check Obligations
-- ------------------------------------
data Oblig
-- | Obligation that proves termination
OTerm :: Oblig
-- | Obligation that proves invariants
OInv :: Oblig
-- | Obligation that proves subtyping constraints
OCons :: Oblig
ignoreOblig :: RType t t1 t2 -> RType t t1 t2
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] -> !(AnnInfo a) -> !(AnnInfo a) -> ![SrcSpan] -> ErrorResult -> Output a
[o_vars] :: Output a -> Maybe [String]
[o_types] :: Output a -> !(AnnInfo a)
[o_templs] :: Output a -> !(AnnInfo a)
[o_bots] :: Output a -> ![SrcSpan]
[o_result] :: Output a -> ErrorResult
hole :: Expr
isHole :: Expr -> 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 c tv r -> Maybe r
topRTypeBase :: (Reftable r) => RType c tv r -> RType c tv r
-- | Implement either pprintTidy or pprintPrec
class PPrint a
pprintTidy :: PPrint a => Tidy -> a -> Doc
pprintPrec :: PPrint a => Int -> Tidy -> a -> Doc
-- | Top-level pretty printer
pprint :: PPrint a => a -> Doc
showpp :: PPrint a => a -> String
-- | Printer
-- ----------------------------------------------------------------
data PPEnv
PP :: Bool -> Bool -> Bool -> Bool -> PPEnv
[ppPs] :: PPEnv -> Bool
[ppTyVar] :: PPEnv -> Bool
[ppSs] :: PPEnv -> Bool
[ppShort] :: PPEnv -> Bool
ppEnv :: PPEnv
ppEnvShort :: PPEnv -> PPEnv
-- | Module Names
-- --------------------------------------------------------------
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
-- | Refinement Type Aliases
-- ---------------------------------------------------
data RTEnv
RTE :: HashMap Symbol (RTAlias RTyVar SpecType) -> HashMap Symbol (RTAlias Symbol Expr) -> RTEnv
[typeAliases] :: RTEnv -> HashMap Symbol (RTAlias RTyVar SpecType)
[exprAliases] :: RTEnv -> HashMap Symbol (RTAlias Symbol Expr)
mapRT :: (HashMap Symbol (RTAlias RTyVar SpecType) -> HashMap Symbol (RTAlias RTyVar SpecType)) -> RTEnv -> RTEnv
mapRE :: (HashMap Symbol (RTAlias Symbol Expr) -> HashMap Symbol (RTAlias Symbol Expr)) -> RTEnv -> RTEnv
type Error = TError SpecType
-- | Error Data Type
-- -----------------------------------------------------------
type ErrorResult = FixResult UserError
-- | Source Information Associated With Constraints
-- ----------------------------
data Cinfo
Ci :: !SrcSpan -> !(Maybe Error) -> !(Maybe Var) -> Cinfo
[ci_loc] :: Cinfo -> !SrcSpan
[ci_err] :: Cinfo -> !(Maybe Error)
[ci_var] :: Cinfo -> !(Maybe Var)
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
-- | Measures
data Body
-- | Measure Refinement: {v | v = e }
E :: Expr -> Body
-- | Measure Refinement: {v | (? v) = p }
P :: Expr -> Body
-- | Measure Refinement: {v | p}
R :: Symbol -> Expr -> Body
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]
data RClass ty
RClass :: BTyCon -> [ty] -> [BTyVar] -> [(LocSymbol, ty)] -> RClass ty
[rcName] :: RClass ty -> BTyCon
[rcSupers] :: RClass ty -> [ty]
[rcTyVars] :: RClass ty -> [BTyVar]
[rcMethods] :: RClass ty -> [(LocSymbol, ty)]
-- | KVar Profile
-- --------------------------------------------------------------
data KVKind
-- | Recursive binder letrec x = ...
RecBindE :: Var -> KVKind
-- | Non recursive binder let x = ...
NonRecBindE :: Var -> KVKind
TypeInstE :: KVKind
PredInstE :: KVKind
LamE :: KVKind
-- | Int is the number of cases
CaseE :: Int -> KVKind
LetE :: KVKind
-- | Projecting out field of
ProjectE :: KVKind
data KVProf
emptyKVProf :: KVProf
updKVProf :: KVKind -> Kuts -> 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
data LogicMap
LM :: HashMap Symbol LMap -> HashMap Var (Maybe Symbol) -> LogicMap
-- | Map from symbols to equations they define
[lmSymDefs] :: LogicMap -> HashMap Symbol LMap
-- | Map from (lifted) Vars to Symbol; see: NOTE:LIFTED-VAR-SYMBOLS
-- and NOTE:REFLECT-IMPORTs
[lmVarSyms] :: LogicMap -> HashMap Var (Maybe Symbol)
toLogicMap :: [(LocSymbol, [Symbol], Expr)] -> LogicMap
eAppWithMap :: LogicMap -> Located Symbol -> [Expr] -> Expr -> Expr
data LMap
LMap :: LocSymbol -> [Symbol] -> Expr -> LMap
[lmVar] :: LMap -> LocSymbol
[lmArgs] :: LMap -> [Symbol]
[lmExpr] :: LMap -> Expr
type RDEnv = DEnv Var SpecType
newtype DEnv x ty
DEnv :: (HashMap x (HashMap Symbol (RISig ty))) -> DEnv x ty
-- | Refined Instances ---------------------------------------------------
data RInstance t
RI :: BTyCon -> [t] -> [(LocSymbol, RISig t)] -> RInstance t
[riclass] :: RInstance t -> BTyCon
[ritype] :: RInstance t -> [t]
[risigs] :: RInstance t -> [(LocSymbol, RISig t)]
data RISig t
RIAssumed :: t -> RISig t
RISig :: t -> RISig t
class Reftable r => UReftable r
ofUReft :: UReftable r => UReft Reft -> r
liquidBegin :: String
liquidEnd :: String
-- | Values Related to Specifications ------------------------------------
data Axiom b s e
Axiom :: (Var, Maybe DataCon) -> Maybe b -> [b] -> [s] -> e -> e -> Axiom b s e
[aname] :: Axiom b s e -> (Var, Maybe DataCon)
[rname] :: Axiom b s e -> Maybe b
[abinds] :: Axiom b s e -> [b]
[atypes] :: Axiom b s e -> [s]
[alhs] :: Axiom b s e -> e
[arhs] :: Axiom b s e -> e
type HAxiom = Axiom Var Type CoreExpr
type AxiomEq = Equation
rtyVarUniqueSymbol :: RTyVar -> Symbol
tyVarUniqueSymbol :: TyVar -> Symbol
rtyVarType :: RTyVar -> Type
instance GHC.Base.Functor (Language.Haskell.Liquid.Types.MSpec ty)
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.MSpec ty ctor)
instance (Data.Data.Data ctor, Data.Data.Data ty) => Data.Data.Data (Language.Haskell.Liquid.Types.MSpec ty ctor)
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.KVProf
instance Data.Data.Data Language.Haskell.Liquid.Types.KVKind
instance GHC.Show.Show Language.Haskell.Liquid.Types.KVKind
instance GHC.Classes.Ord Language.Haskell.Liquid.Types.KVKind
instance GHC.Classes.Eq Language.Haskell.Liquid.Types.KVKind
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.KVKind
instance GHC.Base.Functor Language.Haskell.Liquid.Types.Output
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Output a)
instance GHC.Base.Functor Language.Haskell.Liquid.Types.Annot
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Annot t)
instance Data.Data.Data t => Data.Data.Data (Language.Haskell.Liquid.Types.Annot t)
instance GHC.Base.Functor Language.Haskell.Liquid.Types.AnnInfo
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.AnnInfo a)
instance Data.Data.Data a => Data.Data.Data (Language.Haskell.Liquid.Types.AnnInfo a)
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.RClass ty)
instance Data.Data.Data ty => Data.Data.Data (Language.Haskell.Liquid.Types.RClass ty)
instance GHC.Base.Functor Language.Haskell.Liquid.Types.RClass
instance GHC.Show.Show ty => GHC.Show.Show (Language.Haskell.Liquid.Types.RClass ty)
instance GHC.Base.Functor Language.Haskell.Liquid.Types.CMeasure
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.CMeasure ty)
instance Data.Data.Data ty => Data.Data.Data (Language.Haskell.Liquid.Types.CMeasure ty)
instance GHC.Base.Functor (Language.Haskell.Liquid.Types.Measure ty)
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Measure ty ctor)
instance (Data.Data.Data ctor, Data.Data.Data ty) => Data.Data.Data (Language.Haskell.Liquid.Types.Measure ty ctor)
instance GHC.Base.Functor (Language.Haskell.Liquid.Types.Def ty)
instance (GHC.Classes.Eq ctor, GHC.Classes.Eq ty) => GHC.Classes.Eq (Language.Haskell.Liquid.Types.Def ty ctor)
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Def ty ctor)
instance (Data.Data.Data ctor, Data.Data.Data ty) => Data.Data.Data (Language.Haskell.Liquid.Types.Def ty ctor)
instance (GHC.Show.Show ctor, GHC.Show.Show ty) => GHC.Show.Show (Language.Haskell.Liquid.Types.Def ty ctor)
instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Body
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Body
instance Data.Data.Data Language.Haskell.Liquid.Types.Body
instance GHC.Show.Show Language.Haskell.Liquid.Types.Body
instance GHC.Show.Show Language.Haskell.Liquid.Types.ModName
instance GHC.Classes.Ord Language.Haskell.Liquid.Types.ModName
instance GHC.Classes.Eq Language.Haskell.Liquid.Types.ModName
instance GHC.Show.Show Language.Haskell.Liquid.Types.ModType
instance GHC.Classes.Ord Language.Haskell.Liquid.Types.ModType
instance GHC.Classes.Eq Language.Haskell.Liquid.Types.ModType
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Cinfo
instance GHC.Classes.Ord Language.Haskell.Liquid.Types.Cinfo
instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Cinfo
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.RTAlias x a)
instance (Data.Data.Data a, Data.Data.Data x) => Data.Data.Data (Language.Haskell.Liquid.Types.RTAlias x a)
instance GHC.Show.Show Language.Haskell.Liquid.Types.HasDataDecl
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.DataDecl
instance Data.Data.Data Language.Haskell.Liquid.Types.DataDecl
instance GHC.Show.Show Language.Haskell.Liquid.Types.DataDeclKind
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.DataDeclKind
instance Data.Data.Data Language.Haskell.Liquid.Types.DataDeclKind
instance GHC.Classes.Eq Language.Haskell.Liquid.Types.DataDeclKind
instance Data.Data.Data Language.Haskell.Liquid.Types.TyConP
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.TyConP
instance Data.Data.Data Language.Haskell.Liquid.Types.DataConP
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.DataConP
instance Data.Data.Data Language.Haskell.Liquid.Types.RTyCon
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.RTyCon
instance Data.Data.Data Language.Haskell.Liquid.Types.TyConInfo
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.TyConInfo
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.SizeFun
instance Data.Data.Data Language.Haskell.Liquid.Types.SizeFun
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.DataCtor
instance Data.Data.Data Language.Haskell.Liquid.Types.DataCtor
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.DataName
instance Data.Data.Data Language.Haskell.Liquid.Types.DataName
instance GHC.Classes.Ord Language.Haskell.Liquid.Types.DataName
instance GHC.Classes.Eq Language.Haskell.Liquid.Types.DataName
instance (GHC.Show.Show ty, GHC.Show.Show x) => GHC.Show.Show (Language.Haskell.Liquid.Types.DEnv x ty)
instance (Data.Hashable.Class.Hashable x, GHC.Classes.Eq x) => GHC.Base.Monoid (Language.Haskell.Liquid.Types.DEnv x ty)
instance GHC.Show.Show t => GHC.Show.Show (Language.Haskell.Liquid.Types.RInstance t)
instance Data.Data.Data t => Data.Data.Data (Language.Haskell.Liquid.Types.RInstance t)
instance GHC.Base.Functor Language.Haskell.Liquid.Types.RInstance
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.RInstance t)
instance GHC.Show.Show t => GHC.Show.Show (Language.Haskell.Liquid.Types.RISig t)
instance Data.Data.Data t => Data.Data.Data (Language.Haskell.Liquid.Types.RISig t)
instance GHC.Base.Functor Language.Haskell.Liquid.Types.RISig
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.RISig t)
instance Data.Traversable.Traversable Language.Haskell.Liquid.Types.UReft
instance Data.Foldable.Foldable Language.Haskell.Liquid.Types.UReft
instance GHC.Base.Functor Language.Haskell.Liquid.Types.UReft
instance Data.Data.Data r => Data.Data.Data (Language.Haskell.Liquid.Types.UReft r)
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.UReft r)
instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Stratum
instance Data.Data.Data Language.Haskell.Liquid.Types.Stratum
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Stratum
instance Data.Data.Data t => Data.Data.Data (Language.Haskell.Liquid.Types.World t)
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.World t)
instance Data.Data.Data t => Data.Data.Data (Language.Haskell.Liquid.Types.HSeg t)
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.HSeg t)
instance GHC.Base.Functor (Language.Haskell.Liquid.Types.RType c tv)
instance (Data.Data.Data r, Data.Data.Data tv, Data.Data.Data c) => Data.Data.Data (Language.Haskell.Liquid.Types.RType c tv r)
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.RType c tv r)
instance GHC.Base.Functor (Language.Haskell.Liquid.Types.Ref τ)
instance (Data.Data.Data t, Data.Data.Data τ) => Data.Data.Data (Language.Haskell.Liquid.Types.Ref τ t)
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Ref τ t)
instance (Data.Data.Data s, Data.Data.Data tv) => Data.Data.Data (Language.Haskell.Liquid.Types.RTVar tv s)
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.RTVar tv s)
instance GHC.Base.Functor Language.Haskell.Liquid.Types.RTVInfo
instance Data.Data.Data s => Data.Data.Data (Language.Haskell.Liquid.Types.RTVInfo s)
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.RTVInfo s)
instance Data.Data.Data Language.Haskell.Liquid.Types.BTyCon
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.BTyCon
instance Data.Data.Data Language.Haskell.Liquid.Types.RTyVar
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.RTyVar
instance Data.Data.Data Language.Haskell.Liquid.Types.BTyVar
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.BTyVar
instance GHC.Show.Show Language.Haskell.Liquid.Types.BTyVar
instance Data.Data.Data Language.Haskell.Liquid.Types.Predicate
instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Predicate
instance GHC.Base.Functor Language.Haskell.Liquid.Types.PVar
instance GHC.Show.Show t => GHC.Show.Show (Language.Haskell.Liquid.Types.PVar t)
instance Data.Data.Data t => Data.Data.Data (Language.Haskell.Liquid.Types.PVar t)
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.PVar t)
instance GHC.Show.Show t => GHC.Show.Show (Language.Haskell.Liquid.Types.PVKind t)
instance Data.Traversable.Traversable Language.Haskell.Liquid.Types.PVKind
instance Data.Foldable.Foldable Language.Haskell.Liquid.Types.PVKind
instance GHC.Base.Functor Language.Haskell.Liquid.Types.PVKind
instance Data.Data.Data t => Data.Data.Data (Language.Haskell.Liquid.Types.PVKind t)
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.PVKind t)
instance GHC.Show.Show Language.Haskell.Liquid.Types.LogicMap
instance GHC.Show.Show Language.Haskell.Liquid.Types.PPEnv
instance Data.Bifunctor.Bifunctor Language.Haskell.Liquid.Types.MSpec
instance (Language.Fixpoint.Types.PrettyPrint.PPrint t, Language.Fixpoint.Types.PrettyPrint.PPrint a) => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.MSpec t a)
instance (GHC.Show.Show ty, GHC.Show.Show ctor, Language.Fixpoint.Types.PrettyPrint.PPrint ctor, Language.Fixpoint.Types.PrettyPrint.PPrint ty) => GHC.Show.Show (Language.Haskell.Liquid.Types.MSpec ty ctor)
instance GHC.Classes.Eq ctor => GHC.Base.Monoid (Language.Haskell.Liquid.Types.MSpec ty ctor)
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.KVProf
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.KVProf
instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.KVKind
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.KVKind
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.KVKind
instance GHC.Base.Monoid (Language.Haskell.Liquid.Types.Output a)
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.Annot a)
instance GHC.Base.Monoid (Language.Haskell.Liquid.Types.AnnInfo a)
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.AnnInfo a)
instance Data.Binary.Class.Binary ty => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.RClass ty)
instance Language.Fixpoint.Types.PrettyPrint.PPrint t => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.CMeasure t)
instance Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.CMeasure t) => GHC.Show.Show (Language.Haskell.Liquid.Types.CMeasure t)
instance Language.Haskell.Liquid.UX.Config.HasConfig Language.Haskell.Liquid.Types.GhcInfo
instance Language.Haskell.Liquid.UX.Config.HasConfig Language.Haskell.Liquid.Types.GhcSpec
instance Data.Bifunctor.Bifunctor Language.Haskell.Liquid.Types.Measure
instance (Data.Binary.Class.Binary t, Data.Binary.Class.Binary c) => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.Measure t c)
instance (Language.Fixpoint.Types.PrettyPrint.PPrint t, Language.Fixpoint.Types.PrettyPrint.PPrint a) => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Measure t a)
instance Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Measure t a) => GHC.Show.Show (Language.Haskell.Liquid.Types.Measure t a)
instance Language.Fixpoint.Types.Refinements.Subable (Language.Haskell.Liquid.Types.Measure ty ctor)
instance Data.Bifunctor.Bifunctor Language.Haskell.Liquid.Types.Def
instance (Data.Binary.Class.Binary t, Data.Binary.Class.Binary c) => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.Def t c)
instance Language.Fixpoint.Types.PrettyPrint.PPrint a => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Def t a)
instance Language.Fixpoint.Types.Refinements.Subable (Language.Haskell.Liquid.Types.Def ty ctor)
instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Body
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Body
instance Language.Fixpoint.Types.Refinements.Subable Language.Haskell.Liquid.Types.Body
instance GHC.Base.Monoid Language.Haskell.Liquid.Types.RTEnv
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.ModName
instance Language.Fixpoint.Types.Names.Symbolic Language.Haskell.Liquid.Types.ModName
instance Language.Fixpoint.Types.PrettyPrint.Fixpoint Language.Haskell.Liquid.Types.Cinfo
instance Language.Fixpoint.Types.Spans.Loc Language.Haskell.Liquid.Types.Cinfo
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Cinfo
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.REnv
instance Language.Haskell.Liquid.Types.UReftable (Language.Haskell.Liquid.Types.UReft Language.Fixpoint.Types.Refinements.Reft)
instance Language.Haskell.Liquid.Types.UReftable ()
instance (Data.Binary.Class.Binary x, Data.Binary.Class.Binary a) => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.RTAlias x a)
instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.DataDecl
instance GHC.Classes.Eq Language.Haskell.Liquid.Types.DataDecl
instance GHC.Classes.Ord Language.Haskell.Liquid.Types.DataDecl
instance Language.Fixpoint.Types.Spans.Loc Language.Haskell.Liquid.Types.DataDecl
instance GHC.Show.Show Language.Haskell.Liquid.Types.DataDecl
instance Language.Fixpoint.Types.Names.Symbolic Language.Haskell.Liquid.Types.DataDecl
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.DataDeclKind
instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.DataDeclKind
instance Language.Fixpoint.Types.Spans.Loc Language.Haskell.Liquid.Types.DataConP
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.RTyCon
instance Language.Haskell.Liquid.Types.TyConable Language.Haskell.Liquid.Types.RTyCon
instance GHC.Classes.Eq Language.Haskell.Liquid.Types.RTyCon
instance Language.Fixpoint.Types.PrettyPrint.Fixpoint Language.Haskell.Liquid.Types.RTyCon
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.RTyCon
instance GHC.Show.Show Language.Haskell.Liquid.Types.RTyCon
instance Data.Default.Class.Default Language.Haskell.Liquid.Types.TyConInfo
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.TyConInfo
instance GHC.Show.Show Language.Haskell.Liquid.Types.TyConInfo
instance GHC.Show.Show Language.Haskell.Liquid.Types.SizeFun
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.SizeFun
instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.SizeFun
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.SizeFun
instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.DataCtor
instance Language.Fixpoint.Types.Spans.Loc Language.Haskell.Liquid.Types.DataCtor
instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.DataName
instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.DataName
instance Language.Fixpoint.Types.Spans.Loc Language.Haskell.Liquid.Types.DataName
instance GHC.Show.Show Language.Haskell.Liquid.Types.DataName
instance Language.Fixpoint.Types.Names.Symbolic Language.Haskell.Liquid.Types.DataName
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.DataName
instance GHC.Show.Show (Language.Haskell.Liquid.Types.Axiom Var.Var TyCoRep.Type CoreSyn.CoreExpr)
instance Data.Binary.Class.Binary t => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.RInstance t)
instance Data.Binary.Class.Binary t => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.RISig t)
instance Language.Haskell.Liquid.Types.TyConable TyCon.TyCon
instance Language.Haskell.Liquid.Types.TyConable Language.Haskell.Liquid.Types.Symbol
instance Language.Haskell.Liquid.Types.TyConable Language.Fixpoint.Types.Names.LocSymbol
instance Language.Haskell.Liquid.Types.TyConable Language.Haskell.Liquid.Types.BTyCon
instance (Language.Fixpoint.Types.Refinements.Reftable r, Language.Haskell.Liquid.Types.TyConable c) => Language.Fixpoint.Types.Refinements.Subable (Language.Haskell.Liquid.Types.RTProp c tv r)
instance (Language.Fixpoint.Types.Refinements.Subable r, Language.Fixpoint.Types.Refinements.Reftable r, Language.Haskell.Liquid.Types.TyConable c) => Language.Fixpoint.Types.Refinements.Subable (Language.Haskell.Liquid.Types.RType c tv r)
instance GHC.Base.Monoid a => GHC.Base.Monoid (Language.Haskell.Liquid.Types.UReft a)
instance Control.DeepSeq.NFData r => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.UReft r)
instance Data.Binary.Class.Binary r => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.UReft r)
instance (Language.Fixpoint.Types.PrettyPrint.PPrint r, Language.Fixpoint.Types.Refinements.Reftable r) => Language.Fixpoint.Types.Refinements.Reftable (Language.Haskell.Liquid.Types.UReft r)
instance Language.Fixpoint.Types.Refinements.Expression (Language.Haskell.Liquid.Types.UReft ())
instance Language.Fixpoint.Types.Refinements.Subable r => Language.Fixpoint.Types.Refinements.Subable (Language.Haskell.Liquid.Types.UReft r)
instance GHC.Base.Monoid Language.Haskell.Liquid.Types.Strata
instance Language.Fixpoint.Types.Refinements.Reftable Language.Haskell.Liquid.Types.Strata
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Strata
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Stratum
instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Stratum
instance Language.Fixpoint.Types.Refinements.Subable Language.Haskell.Liquid.Types.Stratum
instance GHC.Show.Show Language.Haskell.Liquid.Types.Stratum
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Stratum
instance GHC.Show.Show tv => GHC.Show.Show (Language.Haskell.Liquid.Types.RTVU c tv)
instance (Data.Binary.Class.Binary c, Data.Binary.Class.Binary tv, Data.Binary.Class.Binary r) => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.RType c tv r)
instance (Control.DeepSeq.NFData c, Control.DeepSeq.NFData tv, Control.DeepSeq.NFData r) => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.RType c tv r)
instance (Language.Fixpoint.Types.PrettyPrint.PPrint r, Language.Fixpoint.Types.Refinements.Reftable r, Language.Fixpoint.Types.PrettyPrint.PPrint t, Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.RType c tv r)) => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Ref t (Language.Haskell.Liquid.Types.RType c tv r))
instance (Data.Binary.Class.Binary τ, Data.Binary.Class.Binary t) => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.Ref τ t)
instance (Control.DeepSeq.NFData τ, Control.DeepSeq.NFData t) => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.Ref τ t)
instance GHC.Classes.Eq tv => GHC.Classes.Eq (Language.Haskell.Liquid.Types.RTVar tv s)
instance (Data.Binary.Class.Binary tv, Data.Binary.Class.Binary s) => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.RTVar tv s)
instance (Control.DeepSeq.NFData tv, Control.DeepSeq.NFData s) => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.RTVar tv s)
instance Language.Fixpoint.Types.PrettyPrint.PPrint v => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.RTVar v s)
instance Control.DeepSeq.NFData s => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.RTVInfo s)
instance Data.Binary.Class.Binary s => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.RTVInfo s)
instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.BTyCon
instance Language.Fixpoint.Types.Names.Symbolic Language.Haskell.Liquid.Types.BTyCon
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.BTyCon
instance GHC.Classes.Eq Language.Haskell.Liquid.Types.BTyCon
instance Language.Fixpoint.Types.PrettyPrint.Fixpoint Language.Haskell.Liquid.Types.BTyCon
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.BTyCon
instance GHC.Show.Show Language.Haskell.Liquid.Types.BTyCon
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.RTyVar
instance Language.Fixpoint.Types.Names.Symbolic Language.Haskell.Liquid.Types.RTyVar
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.RTyVar
instance GHC.Classes.Eq Language.Haskell.Liquid.Types.BTyVar
instance GHC.Classes.Ord Language.Haskell.Liquid.Types.BTyVar
instance Data.String.IsString Language.Haskell.Liquid.Types.BTyVar
instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.BTyVar
instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.BTyVar
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.BTyVar
instance Language.Fixpoint.Types.Names.Symbolic Language.Haskell.Liquid.Types.BTyVar
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.BTyVar
instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Predicate
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Predicate
instance GHC.Base.Monoid Language.Haskell.Liquid.Types.Predicate
instance Language.Fixpoint.Types.Refinements.Subable Language.Haskell.Liquid.Types.Predicate
instance Language.Fixpoint.Types.Refinements.Reftable Language.Haskell.Liquid.Types.Predicate
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Predicate
instance Language.Fixpoint.Types.Refinements.Subable Language.Haskell.Liquid.Types.UsedPVar
instance GHC.Classes.Eq (Language.Haskell.Liquid.Types.PVar t)
instance GHC.Classes.Ord (Language.Haskell.Liquid.Types.PVar t)
instance Data.Binary.Class.Binary t => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.PVar t)
instance Control.DeepSeq.NFData t => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.PVar t)
instance Data.Hashable.Class.Hashable (Language.Haskell.Liquid.Types.PVar a)
instance Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.PVar a)
instance Data.Binary.Class.Binary a => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.PVKind a)
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.PVKind a)
instance GHC.Base.Monoid Language.Haskell.Liquid.Types.LogicMap
instance GHC.Show.Show Language.Haskell.Liquid.Types.LMap
instance Language.Fixpoint.Types.Refinements.Subable Language.Haskell.Liquid.Types.Qualifier
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.Errors.TError a)
instance GHC.Show.Show Module.ModuleName
instance Language.Fixpoint.Types.Names.Symbolic Module.ModuleName
instance Language.Fixpoint.Types.Refinements.Subable t => Language.Fixpoint.Types.Refinements.Subable (Language.Haskell.Liquid.Types.Errors.WithModel t)
instance Language.Fixpoint.Types.Names.Symbolic DataCon.DataCon
instance Language.Fixpoint.Types.PrettyPrint.PPrint DataCon.DataCon
instance GHC.Show.Show DataCon.DataCon
module Language.Haskell.Liquid.Types.Strata
class SubStratum a
subS :: SubStratum a => (Symbol, Stratum) -> a -> a
subsS :: SubStratum a => [(Symbol, Stratum)] -> a -> a
solveStrata :: [([Stratum], [Stratum])] -> [(Symbol, Stratum)]
(<:=) :: (Foldable t, Foldable t1) => t Stratum -> t1 Stratum -> Bool
instance Language.Haskell.Liquid.Types.Strata.SubStratum Language.Haskell.Liquid.Types.Stratum
instance (Language.Haskell.Liquid.Types.Strata.SubStratum a, Language.Haskell.Liquid.Types.Strata.SubStratum b) => Language.Haskell.Liquid.Types.Strata.SubStratum (a, b)
instance Language.Haskell.Liquid.Types.Strata.SubStratum a => Language.Haskell.Liquid.Types.Strata.SubStratum [a]
instance Language.Haskell.Liquid.Types.Strata.SubStratum (Language.Haskell.Liquid.Types.Annot Language.Haskell.Liquid.Types.SpecType)
instance Language.Haskell.Liquid.Types.Strata.SubStratum Language.Haskell.Liquid.Types.SpecType
-- | This module contains a single function that converts a RType -> Doc
-- without using *any* simplifications.
module Language.Haskell.Liquid.Types.PrettyPrint
type OkRT c tv r = (TyConable c, PPrint tv, PPrint c, PPrint r, Reftable r, Reftable (RTProp c tv ()), Reftable (RTProp c tv r), Eq c, Eq tv, Hashable tv)
rtypeDoc :: (OkRT c tv r) => Tidy -> RType c tv r -> Doc
pprManyOrdered :: (PPrint a, Ord a) => Tidy -> String -> [a] -> [Doc]
pprintLongList :: PPrint a => Tidy -> [a] -> Doc
pprintSymbol :: Symbol -> Doc
instance Language.Fixpoint.Types.PrettyPrint.PPrint ErrUtils.ErrMsg
instance Language.Fixpoint.Types.PrettyPrint.PPrint HscTypes.SourceError
instance Language.Fixpoint.Types.PrettyPrint.PPrint Var.Var
instance Language.Fixpoint.Types.PrettyPrint.PPrint Name.Name
instance Language.Fixpoint.Types.PrettyPrint.PPrint TyCon.TyCon
instance Language.Fixpoint.Types.PrettyPrint.PPrint TyCoRep.Type
instance Language.Fixpoint.Types.PrettyPrint.PPrint Class.Class
instance GHC.Show.Show Language.Haskell.Liquid.Types.Predicate
instance Language.Fixpoint.Types.PrettyPrint.PPrint t => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Annot t)
instance Language.Fixpoint.Types.PrettyPrint.PPrint a => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.AnnInfo a)
instance Language.Fixpoint.Types.PrettyPrint.PPrint a => GHC.Show.Show (Language.Haskell.Liquid.Types.AnnInfo a)
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.LMap
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.LogicMap
instance Language.Haskell.Liquid.Types.OkRT c tv r => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.RType c tv r)
instance (Language.Fixpoint.Types.PrettyPrint.PPrint tv, Language.Fixpoint.Types.PrettyPrint.PPrint ty) => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.RTAlias tv ty)
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Fixpoint.Types.PrettyPrint.Tidy
instance (Language.Fixpoint.Types.PrettyPrint.PPrint r, Language.Fixpoint.Types.Refinements.Reftable r) => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.UReft r)
-- | 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.UX.CTags
-- | The TagKey is the top-level binder, and Tag 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
-- | Refinement Types. Mostly mirroring the GHC Type definition, but with
-- room for refinements of various sorts. TODO: Desperately needs
-- re-organization.
module Language.Haskell.Liquid.Types.RefType
uTop :: r -> UReft r
uReft :: (Symbol, Expr) -> UReft Reft
-- | Various functions for converting vanilla Reft to Spec
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 :: HashSet TyCon -> [RTyVar] -> SpecType -> Bool
makeDecrType :: Symbolic a => HashSet TyCon -> [(a, (Symbol, RType RTyCon t (UReft Reft)))] -> (Symbol, RType RTyCon t (UReft Reft))
-- | Termination Predicates
-- ----------------------------------------------------
makeNumEnv :: (Foldable t, TyConable c) => t (RType c b t1) -> [b]
makeLexRefa :: [Located Expr] -> [Located Expr] -> UReft Reft
pdVar :: PVar t -> Predicate
findPVar :: [PVar (RType c tv ())] -> UsedPVar -> PVar (RType c tv ())
class FreeVar a v
freeTyVars :: Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
tyClasses :: (OkRT RTyCon tv r) => RType RTyCon tv r -> [(Class, [RType RTyCon tv r])]
tyConName :: TyCon -> Symbol
quantifyRTy :: Eq tv => [RTVar tv (RType c tv ())] -> RType c tv r -> RType c tv r
quantifyFreeRTy :: Eq tv => RType c tv r -> RType c tv r
ofType :: Monoid r => Type -> RRType r
toType :: (ToTypeable r) => RRType r -> Type
bareOfType :: Monoid r => Type -> BRType r
bTyVar :: Symbol -> BTyVar
rTyVar :: TyVar -> RTyVar
-- | Helper Functions (RJ: Helping to do what?)
-- --------------------------------
rVar :: Monoid r => TyVar -> RType c RTyVar r
rApp :: TyCon -> [RType RTyCon tv r] -> [RTProp RTyCon tv r] -> r -> RType RTyCon tv r
gApp :: TyCon -> [RTyVar] -> [PVar a] -> SpecType
rEx :: Foldable t => t (Symbol, RType c tv r) -> RType c tv r -> RType c tv r
symbolRTyVar :: Symbol -> RTyVar
bareRTyVar :: BTyVar -> RTyVar
tyConBTyCon :: TyCon -> BTyCon
pdVarReft :: PVar t -> UReft Reft
-- | Type Substitutions
-- --------------------------------------------------------
subts :: (Foldable t, SubsTy tv ty c) => t (tv, ty) -> c -> c
subvPredicate :: (UsedPVar -> UsedPVar) -> Predicate -> Predicate
subvUReft :: (UsedPVar -> UsedPVar) -> UReft Reft -> UReft Reft
subsTyVar_meet :: (Eq tv, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVar_meet' :: (Eq tv, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => (tv, RType c tv r) -> RType c tv r -> RType c tv r
subsTyVar_nomeet :: (Eq tv, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVars_nomeet :: (Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVars_meet :: (Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c, SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
addTyConInfo :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => TCEmb TyCon -> (HashMap TyCon RTyCon) -> RRType r -> RRType r
appRTyCon :: SubsTy RTyVar (RType c RTyVar ()) RPVar => TCEmb TyCon -> HashMap TyCon RTyCon -> RTyCon -> [RType c RTyVar r] -> RTyCon
typeUniqueSymbol :: Type -> Symbol
-- | Binders generated by class predicates, typically for constraining
-- tyvars (e.g. FNum)
classBinds :: TCEmb TyCon -> SpecType -> [(Symbol, SortedReft)]
isSizeable :: HashSet TyCon -> TyCon -> Bool
strengthen :: Reftable r => RType c tv r -> r -> RType c tv r
generalize :: (Eq tv) => RType c tv r -> RType c tv r
normalizePds :: (OkRT c tv r) => RType c tv r -> RType c tv r
dataConMsReft :: Reftable r => RType c tv r -> [Symbol] -> Reft
dataConReft :: DataCon -> [Symbol] -> Reft
-- | Annotations and Solutions
-- -------------------------------------------------
rTypeSortedReft :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => TCEmb TyCon -> RRType r -> SortedReft
rTypeSort :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => TCEmb TyCon -> RRType r -> Sort
-- | From Old Fixpoint
-- ---------------------------------------------------------
typeSort :: TCEmb TyCon -> Type -> Sort
shiftVV :: SpecType -> Symbol -> SpecType
expandProductType :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r)) => Var -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
mkTyConInfo :: TyCon -> VarianceInfo -> VarianceInfo -> Maybe SizeFun -> TyConInfo
meetable :: (OkRT c tv r) => RType c tv r -> RType c tv r -> Bool
strengthenRefTypeGen :: (OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r, SubsTy tv (RType c tv ()) tv, SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) => RType c tv r -> RType c tv r -> RType c tv r
strengthenDataConType :: Symbolic t => (t, RType c tv (UReft Reft)) -> (t, RType c tv (UReft Reft))
isBaseTy :: Type -> Bool
updateRTVar :: Monoid r => RTVar RTyVar i -> RTVar RTyVar (RType RTyCon RTyVar r)
isValKind :: Kind -> Bool
kindToRType :: Monoid r => Type -> RRType r
rTVarInfo :: Monoid r => TyVar -> RTVInfo (RRType r)
instance (Language.Haskell.Liquid.Types.SubsTy tv (Language.Haskell.Liquid.Types.RType c tv ()) (Language.Haskell.Liquid.Types.RType c tv ()), Language.Haskell.Liquid.Types.SubsTy tv (Language.Haskell.Liquid.Types.RType c tv ()) c, Language.Haskell.Liquid.Types.OkRT c tv r, Language.Haskell.Liquid.Types.RefType.FreeVar c tv, Language.Haskell.Liquid.Types.SubsTy tv (Language.Haskell.Liquid.Types.RType c tv ()) r, Language.Haskell.Liquid.Types.SubsTy tv (Language.Haskell.Liquid.Types.RType c tv ()) tv, Language.Haskell.Liquid.Types.SubsTy tv (Language.Haskell.Liquid.Types.RType c tv ()) (Language.Haskell.Liquid.Types.RTVar tv (Language.Haskell.Liquid.Types.RType c tv ()))) => GHC.Base.Monoid (Language.Haskell.Liquid.Types.RType c tv r)
instance (Language.Haskell.Liquid.Types.SubsTy tv (Language.Haskell.Liquid.Types.RType c tv ()) c, Language.Haskell.Liquid.Types.OkRT c tv r, Language.Haskell.Liquid.Types.RefType.FreeVar c tv, Language.Haskell.Liquid.Types.SubsTy tv (Language.Haskell.Liquid.Types.RType c tv ()) r, Language.Haskell.Liquid.Types.SubsTy tv (Language.Haskell.Liquid.Types.RType c tv ()) (Language.Haskell.Liquid.Types.RType c tv ()), Language.Haskell.Liquid.Types.SubsTy tv (Language.Haskell.Liquid.Types.RType c tv ()) tv, Language.Haskell.Liquid.Types.SubsTy tv (Language.Haskell.Liquid.Types.RType c tv ()) (Language.Haskell.Liquid.Types.RTVar tv (Language.Haskell.Liquid.Types.RType c tv ()))) => GHC.Base.Monoid (Language.Haskell.Liquid.Types.RTProp c tv r)
instance Language.Haskell.Liquid.Types.RefType.FreeVar Language.Haskell.Liquid.Types.RTyCon Language.Haskell.Liquid.Types.RTyVar
instance Language.Haskell.Liquid.Types.RefType.FreeVar Language.Haskell.Liquid.Types.BTyCon Language.Haskell.Liquid.Types.BTyVar
instance Language.Fixpoint.Types.Refinements.Reftable (Language.Haskell.Liquid.Types.RTProp Language.Haskell.Liquid.Types.RTyCon Language.Haskell.Liquid.Types.RTyVar (Language.Haskell.Liquid.Types.UReft Language.Fixpoint.Types.Refinements.Reft))
instance Language.Fixpoint.Types.Refinements.Reftable (Language.Haskell.Liquid.Types.RTProp Language.Haskell.Liquid.Types.RTyCon Language.Haskell.Liquid.Types.RTyVar ())
instance Language.Fixpoint.Types.Refinements.Reftable (Language.Haskell.Liquid.Types.RTProp Language.Haskell.Liquid.Types.BTyCon Language.Haskell.Liquid.Types.BTyVar (Language.Haskell.Liquid.Types.UReft Language.Fixpoint.Types.Refinements.Reft))
instance Language.Fixpoint.Types.Refinements.Reftable (Language.Haskell.Liquid.Types.RTProp Language.Haskell.Liquid.Types.BTyCon Language.Haskell.Liquid.Types.BTyVar ())
instance Language.Fixpoint.Types.Refinements.Reftable (Language.Haskell.Liquid.Types.RTProp Language.Haskell.Liquid.Types.RTyCon Language.Haskell.Liquid.Types.RTyVar Language.Fixpoint.Types.Refinements.Reft)
instance Language.Fixpoint.Types.Refinements.Subable (Language.Haskell.Liquid.Types.RRProp Language.Fixpoint.Types.Refinements.Reft)
instance (Language.Fixpoint.Types.PrettyPrint.PPrint r, Language.Fixpoint.Types.Refinements.Reftable r, Language.Haskell.Liquid.Types.SubsTy Language.Haskell.Liquid.Types.RTyVar (Language.Haskell.Liquid.Types.RType Language.Haskell.Liquid.Types.RTyCon Language.Haskell.Liquid.Types.RTyVar ()) r, Language.Fixpoint.Types.Refinements.Reftable (Language.Haskell.Liquid.Types.RTProp Language.Haskell.Liquid.Types.RTyCon Language.Haskell.Liquid.Types.RTyVar r)) => Language.Fixpoint.Types.Refinements.Reftable (Language.Haskell.Liquid.Types.RType Language.Haskell.Liquid.Types.RTyCon Language.Haskell.Liquid.Types.RTyVar r)
instance Language.Fixpoint.Types.Refinements.Reftable (Language.Haskell.Liquid.Types.RType Language.Haskell.Liquid.Types.BTyCon Language.Haskell.Liquid.Types.BTyVar (Language.Haskell.Liquid.Types.UReft Language.Fixpoint.Types.Refinements.Reft))
instance Language.Fixpoint.Types.PrettyPrint.Fixpoint GHC.Base.String
instance Language.Fixpoint.Types.PrettyPrint.Fixpoint Class.Class
instance (GHC.Classes.Eq c, GHC.Classes.Eq tv, Data.Hashable.Class.Hashable tv) => GHC.Classes.Eq (Language.Haskell.Liquid.Types.RType c tv ())
instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Predicate
instance GHC.Classes.Eq Language.Haskell.Liquid.Types.RTyVar
instance GHC.Classes.Ord Language.Haskell.Liquid.Types.RTyVar
instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.RTyVar
instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.RTyCon
instance Language.Haskell.Liquid.Types.SubsTy Language.Haskell.Liquid.Types.RTyVar (Language.Haskell.Liquid.Types.RType Language.Haskell.Liquid.Types.RTyCon Language.Haskell.Liquid.Types.RTyVar ()) Language.Haskell.Liquid.Types.RTyVar
instance Language.Haskell.Liquid.Types.SubsTy Language.Haskell.Liquid.Types.RTyVar (Language.Haskell.Liquid.Types.RType Language.Haskell.Liquid.Types.RTyCon Language.Haskell.Liquid.Types.RTyVar ()) (Language.Haskell.Liquid.Types.RTVar Language.Haskell.Liquid.Types.RTyVar (Language.Haskell.Liquid.Types.RType Language.Haskell.Liquid.Types.RTyCon Language.Haskell.Liquid.Types.RTyVar ()))
instance Language.Haskell.Liquid.Types.SubsTy Language.Haskell.Liquid.Types.BTyVar (Language.Haskell.Liquid.Types.RType c Language.Haskell.Liquid.Types.BTyVar ()) Language.Haskell.Liquid.Types.BTyVar
instance Language.Haskell.Liquid.Types.SubsTy Language.Haskell.Liquid.Types.BTyVar (Language.Haskell.Liquid.Types.RType c Language.Haskell.Liquid.Types.BTyVar ()) (Language.Haskell.Liquid.Types.RTVar Language.Haskell.Liquid.Types.BTyVar (Language.Haskell.Liquid.Types.RType c Language.Haskell.Liquid.Types.BTyVar ()))
instance Language.Haskell.Liquid.Types.SubsTy tv ty ()
instance Language.Haskell.Liquid.Types.SubsTy tv ty Language.Fixpoint.Types.Names.Symbol
instance Language.Haskell.Liquid.Types.SubsTy tv ty Language.Fixpoint.Types.Refinements.Expr => Language.Haskell.Liquid.Types.SubsTy tv ty Language.Fixpoint.Types.Refinements.Reft
instance Language.Haskell.Liquid.Types.SubsTy tv ty Language.Fixpoint.Types.Sorts.Sort => Language.Haskell.Liquid.Types.SubsTy tv ty Language.Fixpoint.Types.Refinements.Expr
instance (Language.Haskell.Liquid.Types.SubsTy tv ty a, Language.Haskell.Liquid.Types.SubsTy tv ty b) => Language.Haskell.Liquid.Types.SubsTy tv ty (a, b)
instance Language.Haskell.Liquid.Types.SubsTy Language.Haskell.Liquid.Types.BTyVar (Language.Haskell.Liquid.Types.RType Language.Haskell.Liquid.Types.BTyCon Language.Haskell.Liquid.Types.BTyVar ()) Language.Fixpoint.Types.Sorts.Sort
instance Language.Haskell.Liquid.Types.SubsTy Language.Fixpoint.Types.Names.Symbol Language.Haskell.Liquid.Types.RSort Language.Fixpoint.Types.Sorts.Sort
instance Language.Haskell.Liquid.Types.SubsTy Language.Haskell.Liquid.Types.RTyVar Language.Haskell.Liquid.Types.RSort Language.Fixpoint.Types.Sorts.Sort
instance Language.Haskell.Liquid.Types.SubsTy tv ty ty => Language.Haskell.Liquid.Types.SubsTy tv ty (Language.Haskell.Liquid.Types.PVKind ty)
instance Language.Haskell.Liquid.Types.SubsTy tv ty ty => Language.Haskell.Liquid.Types.SubsTy tv ty (Language.Haskell.Liquid.Types.PVar ty)
instance Language.Haskell.Liquid.Types.SubsTy Language.Haskell.Liquid.Types.RTyVar Language.Haskell.Liquid.Types.RSort Language.Haskell.Liquid.Types.RTyCon
instance Language.Haskell.Liquid.Types.SubsTy Language.Haskell.Liquid.Types.RTyVar Language.Haskell.Liquid.Types.RSort Language.Haskell.Liquid.Types.PrType
instance Language.Haskell.Liquid.Types.SubsTy Language.Haskell.Liquid.Types.RTyVar Language.Haskell.Liquid.Types.RSort Language.Haskell.Liquid.Types.SpecType
instance Language.Haskell.Liquid.Types.SubsTy Var.TyVar TyCoRep.Type Language.Haskell.Liquid.Types.SpecType
instance Language.Haskell.Liquid.Types.SubsTy Language.Haskell.Liquid.Types.RTyVar Language.Haskell.Liquid.Types.RTyVar Language.Haskell.Liquid.Types.SpecType
instance Language.Haskell.Liquid.Types.SubsTy Language.Haskell.Liquid.Types.RTyVar Language.Haskell.Liquid.Types.RSort Language.Haskell.Liquid.Types.RSort
instance Language.Haskell.Liquid.Types.SubsTy tv Language.Haskell.Liquid.Types.RSort Language.Haskell.Liquid.Types.Predicate
instance Language.Haskell.Liquid.Types.SubsTy tv ty r => Language.Haskell.Liquid.Types.SubsTy tv ty (Language.Haskell.Liquid.Types.UReft r)
instance Language.Haskell.Liquid.Types.SubsTy Language.Haskell.Liquid.Types.BTyVar Language.Haskell.Liquid.Types.BSort Language.Haskell.Liquid.Types.BTyCon
instance Language.Haskell.Liquid.Types.SubsTy Language.Haskell.Liquid.Types.BTyVar Language.Haskell.Liquid.Types.BSort Language.Haskell.Liquid.Types.BSort
instance (Language.Haskell.Liquid.Types.SubsTy tv ty (Language.Haskell.Liquid.Types.UReft r), Language.Haskell.Liquid.Types.SubsTy tv ty (Language.Haskell.Liquid.Types.RType c tv ())) => Language.Haskell.Liquid.Types.SubsTy tv ty (Language.Haskell.Liquid.Types.RTProp c tv (Language.Haskell.Liquid.Types.UReft r))
instance Language.Fixpoint.Types.Refinements.Expression Var.Var
instance (GHC.Show.Show tv, GHC.Show.Show ty) => GHC.Show.Show (Language.Haskell.Liquid.Types.RTAlias tv ty)
instance GHC.Show.Show Language.Haskell.Liquid.Types.RTyVar
instance Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.UReft r) => GHC.Show.Show (Language.Haskell.Liquid.Types.UReft r)
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.DataDecl
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.DataCtor
instance Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.RType c tv r) => GHC.Show.Show (Language.Haskell.Liquid.Types.RType c tv r)
instance Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.RTProp c tv r) => GHC.Show.Show (Language.Haskell.Liquid.Types.RTProp c tv r)
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.REnv
-- | This module contains functions for cleaning up types before they are
-- rendered, e.g. in error messages or annoations, and also some PPrint
-- instances that rely upon tidying.
module Language.Haskell.Liquid.UX.Tidy
tidySpecType :: Tidy -> SpecType -> SpecType
tidySymbol :: Symbol -> Symbol
isTmpSymbol :: Symbol -> Bool
-- | This function is put in this module as it depends on the Exception
-- instance, which depends on the PPrint instance, which depends on
-- tidySpecType.
--
-- Show an Error, then crash
panicError :: Error -> a
-- | Converting Results To Answers -------------------------------------
class Result a
result :: Result a => a -> FixResult UserError
errorToUserError :: Error -> UserError
cinfoError :: Cinfo -> Error
instance Language.Haskell.Liquid.UX.Tidy.Result Language.Haskell.Liquid.Types.Errors.UserError
instance Language.Haskell.Liquid.UX.Tidy.Result [Language.Haskell.Liquid.Types.Error]
instance Language.Haskell.Liquid.UX.Tidy.Result Language.Haskell.Liquid.Types.Error
instance Language.Haskell.Liquid.UX.Tidy.Result (Language.Fixpoint.Types.Errors.FixResult Language.Haskell.Liquid.Types.Cinfo)
instance Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Errors.CtxError Text.PrettyPrint.HughesPJ.Doc)
instance Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Errors.CtxError Language.Haskell.Liquid.Types.SpecType)
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Error
instance GHC.Show.Show Language.Haskell.Liquid.Types.Error
instance GHC.Exception.Exception Language.Haskell.Liquid.Types.Error
instance GHC.Exception.Exception [Language.Haskell.Liquid.Types.Error]
module Language.Haskell.Liquid.Types.PredType
type PrType = RRType Predicate
data TyConP
TyConP :: !SourcePos -> ![RTyVar] -> ![PVar RSort] -> ![Symbol] -> !VarianceInfo -> !VarianceInfo -> !(Maybe SizeFun) -> TyConP
[ty_loc] :: TyConP -> !SourcePos
[freeTyVarsTy] :: TyConP -> ![RTyVar]
[freePredTy] :: TyConP -> ![PVar RSort]
[freeLabelTy] :: TyConP -> ![Symbol]
[varianceTs] :: TyConP -> !VarianceInfo
[variancePs] :: TyConP -> !VarianceInfo
[sizeFun] :: TyConP -> !(Maybe SizeFun)
data DataConP
DataConP :: !SourcePos -> ![RTyVar] -> ![PVar RSort] -> ![Symbol] -> ![SpecType] -> ![(Symbol, SpecType)] -> !SpecType -> !Bool -> !Symbol -> !SourcePos -> DataConP
[dc_loc] :: DataConP -> !SourcePos
-- | Type parameters
[freeTyVars] :: DataConP -> ![RTyVar]
-- | Abstract Refinement parameters
[freePred] :: DataConP -> ![PVar RSort]
-- | ? strata stuff
[freeLabels] :: DataConP -> ![Symbol]
-- | ? Class constraints (via dataConStupidTheta)
[tyConstrs] :: DataConP -> ![SpecType]
-- | Value parameters
[tyArgs] :: DataConP -> ![(Symbol, SpecType)]
-- | Result type , tyData :: !SpecType -- ^ The generic ADT, see
-- [NOTE:DataCon-Data]
[tyRes] :: DataConP -> !SpecType
-- | Was this specified in GADT style (if so, DONT use function names as
-- fields)
[dcpIsGadt] :: DataConP -> !Bool
-- | Which module was this defined in
[dcpModule] :: DataConP -> !Symbol
[dc_locE] :: DataConP -> !SourcePos
dataConTy :: Monoid r => HashMap RTyVar (RType RTyCon RTyVar r) -> Type -> RType RTyCon RTyVar r
dataConPSpecType :: DataCon -> DataConP -> [(Var, SpecType)]
makeTyConInfo :: [(TyCon, TyConP)] -> HashMap TyCon RTyCon
-- | Instantiate PVar with RTProp
-- -----------------------------------------------
--
-- replacePreds is the main function used to substitute an
-- (abstract) predicate with a concrete Ref, that is either an
-- RProp or RHProp type. The substitution is invoked to
-- obtain the SpecType resulting at predicate application
-- sites in Constraint. The range of the PVar substitutions
-- are fresh or true RefType. That is, there are
-- no further _quantified_ PVar in the target.
replacePreds :: String -> SpecType -> [(RPVar, SpecProp)] -> SpecType
replacePredsWithRefs :: (UsedPVar, (Symbol, [((), Symbol, Expr)]) -> Expr) -> UReft Reft -> UReft Reft
pVartoRConc :: PVar t -> (Symbol, [(a, b, Expr)]) -> Expr
-- | Interface: Modified CoreSyn.exprType due to predApp
-- -------------------
predType :: Type
-- | pvarRType π returns a trivial RType corresponding to
-- the function signature for a PVar π. For example, if
-- π :: T1 -> T2 -> T3 -> Prop then pvarRType
-- π returns an RType with an RTycon called
-- predRTyCon `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] -> Expr
pappSort :: Int -> Sort
pappArity :: Int
dataConWorkRep :: DataCon -> SpecRep
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.TyConP
instance GHC.Show.Show Language.Haskell.Liquid.Types.TyConP
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.DataConP
instance GHC.Show.Show Language.Haskell.Liquid.Types.DataConP
module Language.Haskell.Liquid.WiredIn
wiredTyCons :: [(TyCon, TyConP)]
wiredDataCons :: [(DataCon, Located DataConP)]
wiredSortedSyms :: [(Symbol, Sort)]
-- | LH Primitive TyCons
-- -------------------------------------------------------
dictionaryVar :: Var
dictionaryTyVar :: TyVar
dictionaryBind :: Bind Var
proofTyConName :: Symbol
-- | LH Primitive TyCons ----------------------------------------------
combineProofsName :: String
-- | Horrible hack to support hardwired symbols like head,
-- tail, fst, snd and other LH generated symbols
-- that *do not* correspond to GHC Vars and *should not* be resolved to
-- GHC Vars.
isWiredIn :: Located Symbol -> Bool
dcPrefix :: Symbol
-- | This code has various wrappers around meet and
-- strengthen that are here so that we can throw decent error
-- messages if they fail. The module depends on RefType and
-- Tidy.
module Language.Haskell.Liquid.Types.Meet
meetVarTypes :: Doc -> (SrcSpan, SpecType) -> (SrcSpan, SpecType) -> SpecType
module Language.Haskell.Liquid.Types.Fresh
class (Applicative m, Monad m) => Freshable m a
fresh :: Freshable m a => m a
true :: Freshable m a => a -> m a
refresh :: Freshable m a => a -> m a
refreshTy :: (FreshM m) => SpecType -> m SpecType
refreshVV :: FreshM m => SpecType -> m SpecType
refreshArgs :: (FreshM m) => SpecType -> m SpecType
refreshHoles :: (Symbolic t, Reftable r, TyConable c, Freshable f r) => [(t, RType c tv r)] -> f ([Symbol], [(t, RType c tv r)])
refreshArgsSub :: (FreshM m) => SpecType -> m (SpecType, Subst)
instance (Language.Haskell.Liquid.Types.Fresh.Freshable m GHC.Integer.Type.Integer, GHC.Base.Monad m, GHC.Base.Applicative m) => Language.Haskell.Liquid.Types.Fresh.Freshable m Language.Fixpoint.Types.Names.Symbol
instance (Language.Haskell.Liquid.Types.Fresh.Freshable m GHC.Integer.Type.Integer, GHC.Base.Monad m, GHC.Base.Applicative m) => Language.Haskell.Liquid.Types.Fresh.Freshable m Language.Fixpoint.Types.Refinements.Expr
instance (Language.Haskell.Liquid.Types.Fresh.Freshable m GHC.Integer.Type.Integer, GHC.Base.Monad m, GHC.Base.Applicative m) => Language.Haskell.Liquid.Types.Fresh.Freshable m [Language.Fixpoint.Types.Refinements.Expr]
instance (Language.Haskell.Liquid.Types.Fresh.Freshable m GHC.Integer.Type.Integer, GHC.Base.Monad m, GHC.Base.Applicative m) => Language.Haskell.Liquid.Types.Fresh.Freshable m Language.Fixpoint.Types.Refinements.Reft
instance Language.Haskell.Liquid.Types.Fresh.Freshable m GHC.Integer.Type.Integer => Language.Haskell.Liquid.Types.Fresh.Freshable m Language.Haskell.Liquid.Types.RReft
instance Language.Haskell.Liquid.Types.Fresh.Freshable m GHC.Integer.Type.Integer => Language.Haskell.Liquid.Types.Fresh.Freshable m Language.Haskell.Liquid.Types.Strata
instance (Language.Haskell.Liquid.Types.Fresh.Freshable m GHC.Integer.Type.Integer, Language.Haskell.Liquid.Types.Fresh.Freshable m r, Language.Fixpoint.Types.Refinements.Reftable r) => Language.Haskell.Liquid.Types.Fresh.Freshable m (Language.Haskell.Liquid.Types.RRType r)
module Language.Haskell.Liquid.Types.Dictionaries
makeDictionaries :: [RInstance SpecType] -> DEnv Symbol SpecType
makeDictionary :: RInstance SpecType -> (Symbol, HashMap Symbol (RISig SpecType))
dfromList :: [(Var, HashMap Symbol (RISig t))] -> DEnv Var t
dmapty :: (a -> b) -> DEnv v a -> DEnv v b
dmap :: (v1 -> v2) -> HashMap k v1 -> HashMap k v2
dinsert :: (Eq x, Hashable x) => DEnv x ty -> x -> HashMap Symbol (RISig ty) -> DEnv x ty
dlookup :: (Eq k, Hashable k) => DEnv k t -> k -> Maybe (HashMap Symbol (RISig t))
dhasinfo :: (Symbolic a1, Show a) => Maybe (HashMap Symbol a) -> a1 -> Maybe a
mapRISig :: (a -> b) -> RISig a -> RISig b
fromRISig :: RISig a -> a
module Language.Haskell.Liquid.Types.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 Expr
type RBEnv = HashMap LocSymbol RBound
type RRBEnv tv = HashMap LocSymbol (RRBound tv)
makeBound :: (PPrint r, UReftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r) => RRBound RSort -> [RRType r] -> [Symbol] -> RRType r -> RRType r
instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Bounds.Bound t e)
instance (Data.Data.Data e, Data.Data.Data t) => Data.Data.Data (Language.Haskell.Liquid.Types.Bounds.Bound t e)
instance (Data.Binary.Class.Binary t, Data.Binary.Class.Binary e) => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.Bounds.Bound t e)
instance Data.Hashable.Class.Hashable (Language.Haskell.Liquid.Types.Bounds.Bound t e)
instance GHC.Classes.Eq (Language.Haskell.Liquid.Types.Bounds.Bound t e)
instance (Language.Fixpoint.Types.PrettyPrint.PPrint e, Language.Fixpoint.Types.PrettyPrint.PPrint t) => GHC.Show.Show (Language.Haskell.Liquid.Types.Bounds.Bound t e)
instance (Language.Fixpoint.Types.PrettyPrint.PPrint e, Language.Fixpoint.Types.PrettyPrint.PPrint t) => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Bounds.Bound t e)
instance Data.Bifunctor.Bifunctor Language.Haskell.Liquid.Types.Bounds.Bound
module Language.Haskell.Liquid.Transforms.Simplify
simplifyBounds :: SpecType -> SpecType
-- | This module contains the functions related to Error type, in
-- particular, to tidyError using a solution, and
-- pprint errors.
module Language.Haskell.Liquid.UX.Errors
tidyError :: FixSolution -> Error -> Error
-- | This module contains the code for Incremental checking, which finds
-- the part of a target file (the subset of the [CoreBind] 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.UX.DiffCheck
-- | Data Types
-- ----------------------------------------------------------------
--
-- 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
-- | slice returns a subset of the [CoreBind] of the input
-- target file which correspond to top-level binders whose code
-- has changed and their transitive dependencies.
slice :: FilePath -> [CoreBind] -> GhcSpec -> IO (Maybe DiffCheck)
-- | thin cbs sp vs returns a subset of the cbs ::
-- [CoreBind] which correspond to the definitions of vs and
-- the functions transitively called therein for which there are *no*
-- type signatures. Callees with type signatures are assumed to satisfy
-- those signatures.
thin :: [CoreBind] -> GhcSpec -> [Var] -> DiffCheck
-- | save creates an .saved version of the target file,
-- which will be used to find what has changed the next time
-- target is checked.
saveResult :: FilePath -> Output Doc -> IO ()
-- | checkedNames returns the names of the top-level binders that
-- will be checked
checkedVars :: DiffCheck -> [Var]
filterBinds :: [CoreBind] -> HashSet Var -> [CoreBind]
instance GHC.Classes.Ord Language.Haskell.Liquid.UX.DiffCheck.Def
instance GHC.Classes.Eq Language.Haskell.Liquid.UX.DiffCheck.Def
instance GHC.Show.Show Language.Haskell.Liquid.UX.DiffCheck.Def
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.UX.DiffCheck.DiffCheck
instance GHC.Base.Functor Data.Algorithm.Diff.Diff
instance Data.Aeson.Types.ToJSON.ToJSON Text.Parsec.Pos.SourcePos
instance Data.Aeson.Types.FromJSON.FromJSON Text.Parsec.Pos.SourcePos
instance Data.Aeson.Types.ToJSON.ToJSON Language.Haskell.Liquid.Types.ErrorResult
instance Data.Aeson.Types.FromJSON.FromJSON Language.Haskell.Liquid.Types.ErrorResult
instance Data.Aeson.Types.ToJSON.ToJSON Text.PrettyPrint.HughesPJ.Doc
instance Data.Aeson.Types.FromJSON.FromJSON Text.PrettyPrint.HughesPJ.Doc
instance Data.Aeson.Types.ToJSON.ToJSON a => Data.Aeson.Types.ToJSON.ToJSON (Language.Haskell.Liquid.Types.AnnInfo a)
instance Data.Aeson.Types.FromJSON.FromJSON a => Data.Aeson.Types.FromJSON.FromJSON (Language.Haskell.Liquid.Types.AnnInfo a)
instance Data.Aeson.Types.ToJSON.ToJSON (Language.Haskell.Liquid.Types.Output Text.PrettyPrint.HughesPJ.Doc)
instance Data.Aeson.Types.FromJSON.FromJSON (Language.Haskell.Liquid.Types.Output Text.PrettyPrint.HughesPJ.Doc)
-- | 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.UX.Annotate
-- | Gross hack, to force dependency and loading of module.
specAnchor :: Int
-- | output creates the pretty printed output
mkOutput :: Config -> ErrorResult -> FixSolution -> AnnInfo (Annot SpecType) -> Output Doc
-- | annotate actually renders the output to files
annotate :: Config -> [FilePath] -> Output Doc -> IO AnnMap
tokeniseWithLoc :: String -> [(TokenType, String, Loc)]
annErrors :: AnnMap -> AnnErrors
instance Data.Aeson.Types.ToJSON.ToJSON Language.Haskell.Liquid.UX.Annotate.Annot1
instance Data.Aeson.Types.ToJSON.ToJSON Language.Haskell.Liquid.UX.Annotate.AnnErrors
instance (GHC.Show.Show k, Data.Aeson.Types.ToJSON.ToJSON a) => Data.Aeson.Types.ToJSON.ToJSON (Language.Haskell.Liquid.UX.Annotate.Assoc k a)
instance Data.Aeson.Types.ToJSON.ToJSON Language.Haskell.Liquid.UX.ACSS.Status
instance Data.Aeson.Types.ToJSON.ToJSON Language.Haskell.Liquid.GHC.Misc.Loc
instance Data.Aeson.Types.ToJSON.ToJSON Language.Haskell.Liquid.UX.ACSS.AnnMap
-- | This module contains all the code needed to output the result which is
-- either: SAFE or WARNING 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.UX.CmdLine
getOpts :: [String] -> IO Config
mkOpts :: Config -> IO Config
defConfig :: Config
withPragmas :: Config -> FilePath -> [Located String] -> IO Config
-- | Attempt to canonicalize all FilePaths in the Config so
-- we don't have to worry about relative paths.
canonicalizePaths :: FilePath -> Config -> IO Config
-- | Exit Function -----------------------------------------------------
exitWithResult :: Config -> [FilePath] -> Output Doc -> IO (Output Doc)
addErrors :: FixResult a -> [a] -> FixResult a
-- | check subset of binders modified (+ dependencies) since last check
diffcheck :: Config -> Bool
instance Language.Fixpoint.Types.PrettyPrint.Fixpoint (Language.Fixpoint.Types.Errors.FixResult Language.Haskell.Liquid.UX.CmdLine.CError)
instance GHC.Show.Show (Language.Haskell.Liquid.Types.Errors.CtxError Text.PrettyPrint.HughesPJ.Doc)
module Gradual.GUI
render :: GConfig -> GSpan -> [[GSub a]] -> IO ()
module Language.Haskell.Liquid.Transforms.RefSplit
splitXRelatedRefs :: Symbol -> SpecType -> (SpecType, SpecType)
instance Language.Fixpoint.Types.Refinements.Subable x => Language.Haskell.Liquid.Transforms.RefSplit.IsFree x
instance GHC.Show.Show (Language.Haskell.Liquid.Types.UReft Language.Fixpoint.Types.Refinements.Reft)
module Language.Haskell.Liquid.Measure
data Spec ty bndr
Spec :: ![Measure ty bndr] -> ![(LocSymbol, ty)] -> ![(LocSymbol, ty)] -> ![(LocSymbol, ty)] -> ![(LocSymbol, ty)] -> ![(Maybe LocSymbol, ty)] -> ![(ty, ty)] -> ![Symbol] -> ![DataDecl] -> ![DataDecl] -> ![FilePath] -> ![RTAlias Symbol BareType] -> ![RTAlias Symbol Expr] -> !(TCEmb LocSymbol) -> ![Qualifier] -> ![(LocSymbol, [Int])] -> ![LocSymbol] -> !(HashSet LocSymbol) -> !(HashSet LocSymbol) -> !(HashMap LocSymbol (Maybe Int)) -> !(HashSet LocSymbol) -> !(HashSet LocSymbol) -> !(HashSet LocSymbol) -> !(HashSet LocSymbol) -> ![Located String] -> ![Measure ty ()] -> ![Measure ty bndr] -> ![RClass ty] -> ![(LocSymbol, [Located Expr])] -> ![RInstance ty] -> ![(LocSymbol, [Variance])] -> !(RRBEnv ty) -> !(HashMap LocSymbol Symbol) -> ![AxiomEq] -> Spec ty bndr
-- | User-defined properties for ADTs
[measures] :: Spec ty bndr -> ![Measure ty bndr]
-- | Assumed (unchecked) types; including reflected signatures
[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)]
-- | Reflected type signatures
[reflSigs] :: Spec ty bndr -> ![(LocSymbol, ty)]
-- | Data type invariants; the Maybe is the generating measure
[invariants] :: Spec ty bndr -> ![(Maybe LocSymbol, ty)]
-- | Data type invariants to be checked
[ialiases] :: Spec ty bndr -> ![(ty, ty)]
-- | Loaded spec module names
[imports] :: Spec ty bndr -> ![Symbol]
-- | Predicated data definitions
[dataDecls] :: Spec ty bndr -> ![DataDecl]
-- | Predicated new type definitions
[newtyDecls] :: Spec ty bndr -> ![DataDecl]
-- | Included qualifier files
[includes] :: Spec ty bndr -> ![FilePath]
-- | RefType aliases
[aliases] :: Spec ty bndr -> ![RTAlias Symbol BareType]
-- | 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 reflect
[reflects] :: Spec ty bndr -> !(HashSet LocSymbol)
-- | Automatically instantiate axioms in these Functions with maybe
-- specified fuel
[autois] :: Spec ty bndr -> !(HashMap LocSymbol (Maybe Int))
-- | 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) -> 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, [Located Expr])]
[rinstance] :: Spec ty bndr -> ![RInstance ty]
-- | ? Where do these come from ?!
[dvariance] :: Spec ty bndr -> ![(LocSymbol, [Variance])]
[bounds] :: Spec ty bndr -> !(RRBEnv ty)
-- | Temporary (?) hack to deal with dictionaries in specifications see
-- testsposNatClass.hs
[defs] :: Spec ty bndr -> !(HashMap LocSymbol Symbol)
-- | AxiomEqualities used for Proof-By-Evaluation
[axeqs] :: Spec ty bndr -> ![AxiomEq]
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]
type BareSpec = Spec LocBareType LocSymbol
type BareMeasure = Measure LocBareType LocSymbol
type SpecMeasure = Measure LocSpecType DataCon
mkM :: LocSymbol -> ty -> [Def ty bndr] -> Measure ty bndr
mkMSpec :: [Measure t LocSymbol] -> [Measure t ()] -> [Measure t LocSymbol] -> MSpec t LocSymbol
mkMSpec' :: Symbolic ctor => [Measure ty ctor] -> MSpec ty ctor
qualifySpec :: Symbol -> Spec ty bndr -> Spec ty bndr
dataConTypes :: MSpec (RRType Reft) DataCon -> ([(Var, RRType Reft)], [(LocSymbol, RRType Reft)])
defRefType :: Type -> Def (RRType Reft) DataCon -> RRType Reft
instance GHC.Generics.Generic (Language.Haskell.Liquid.Measure.Spec ty bndr)
instance Data.Binary.Class.Binary Language.Haskell.Liquid.Measure.BareSpec
instance GHC.Base.Monoid (Language.Haskell.Liquid.Measure.Spec ty bndr)
module Language.Haskell.Liquid.Parse
-- | Top Level Parsing API
-- -----------------------------------------------------
--
-- Used to parse .hs and .lhs files (via ApiAnnotations)
hsSpecificationP :: ModuleName -> [(SourcePos, String)] -> [BPspec] -> Either [Error] (ModName, BareSpec)
-- | Used to parse .spec files
specSpecificationP :: SourceName -> String -> Either Error (ModName, BareSpec)
singleSpecP :: SourcePos -> String -> Either Error BPspec
type BPspec = Pspec (Located BareType) LocSymbol
data Pspec ty ctor
Meas :: (Measure ty ctor) -> Pspec ty ctor
Assm :: (LocSymbol, ty) -> Pspec ty ctor
Asrt :: (LocSymbol, ty) -> Pspec ty ctor
LAsrt :: (LocSymbol, ty) -> Pspec ty ctor
Asrts :: ([LocSymbol], (ty, Maybe [Located Expr])) -> Pspec ty ctor
Impt :: Symbol -> Pspec ty ctor
DDecl :: DataDecl -> Pspec ty ctor
NTDecl :: DataDecl -> Pspec ty ctor
Incl :: FilePath -> Pspec ty ctor
Invt :: ty -> Pspec ty ctor
IAlias :: (ty, ty) -> Pspec ty ctor
Alias :: (RTAlias Symbol BareType) -> Pspec ty ctor
EAlias :: (RTAlias Symbol Expr) -> Pspec ty ctor
Embed :: (LocSymbol, FTycon) -> Pspec ty ctor
Qualif :: Qualifier -> Pspec ty ctor
Decr :: (LocSymbol, [Int]) -> Pspec ty ctor
LVars :: LocSymbol -> Pspec ty ctor
Lazy :: LocSymbol -> Pspec ty ctor
Insts :: (LocSymbol, Maybe Int) -> Pspec ty ctor
HMeas :: LocSymbol -> Pspec ty ctor
Reflect :: LocSymbol -> Pspec ty ctor
Inline :: LocSymbol -> Pspec ty ctor
ASize :: LocSymbol -> Pspec ty ctor
HBound :: LocSymbol -> Pspec ty ctor
PBound :: (Bound ty Expr) -> Pspec ty ctor
Pragma :: (Located String) -> Pspec ty ctor
CMeas :: (Measure ty ()) -> Pspec ty ctor
IMeas :: (Measure ty ctor) -> Pspec ty ctor
Class :: (RClass ty) -> Pspec ty ctor
RInst :: (RInstance ty) -> Pspec ty ctor
Varia :: (LocSymbol, [Variance]) -> Pspec ty ctor
BFix :: () -> Pspec ty ctor
Define :: (LocSymbol, Symbol) -> Pspec ty ctor
parseSymbolToLogic :: SourceName -> String -> Either Error LogicMap
instance (GHC.Show.Show ty, Language.Fixpoint.Types.PrettyPrint.PPrint ctor, Language.Fixpoint.Types.PrettyPrint.PPrint ty) => GHC.Show.Show (Language.Haskell.Liquid.Parse.Pspec ty ctor)
instance (Data.Data.Data ctor, Data.Data.Data ty) => Data.Data.Data (Language.Haskell.Liquid.Parse.Pspec ty ctor)
instance GHC.Show.Show Language.Haskell.Liquid.Parse.ParamComp
instance GHC.Show.Show Language.Haskell.Liquid.Parse.PcScope
instance GHC.Classes.Eq Language.Haskell.Liquid.Parse.PcScope
module Language.Haskell.Liquid.UX.QuasiQuoter
lq :: QuasiQuoter
newtype LiquidQuote
LiquidQuote :: BPspec -> LiquidQuote
[liquidQuoteSpec] :: LiquidQuote -> BPspec
instance Data.Data.Data Language.Haskell.Liquid.UX.QuasiQuoter.LiquidQuote
instance GHC.Base.Functor Language.Haskell.Liquid.UX.QuasiQuoter.Simpl
instance GHC.Base.Applicative Language.Haskell.Liquid.UX.QuasiQuoter.Simpl
instance GHC.Base.Monad Language.Haskell.Liquid.UX.QuasiQuoter.Simpl
module LiquidHaskell
lq :: QuasiQuoter
-- | This module contains functions that convert things to their
-- Bare versions, e.g. SpecType -> BareType etc.
module Language.Haskell.Liquid.Bare.ToBare
specToBare :: SpecType -> BareType
measureToBare :: SpecMeasure -> BareMeasure
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.Bare.Env
-- | Error-Reader-IO For Bare Transformation
-- -----------------------------------
type BareM = WriterT [Warn] (ExceptT Error (StateT BareEnv IO))
type Warn = String
type TCEnv = HashMap TyCon RTyCon
data BareEnv
BE :: !ModName -> !TCEnv -> !RTEnv -> !(HashMap Symbol Var) -> !(HscEnv) -> !LogicMap -> !DataConMap -> !(RBEnv) -> !(TCEmb TyCon) -> !(HashMap Symbol LocSymbol) -> !(HashMap Symbol LocSymbol) -> !Config -> !Integer -> BareEnv
[modName] :: BareEnv -> !ModName
[tcEnv] :: BareEnv -> !TCEnv
[rtEnv] :: BareEnv -> !RTEnv
[varEnv] :: BareEnv -> !(HashMap Symbol Var)
[hscEnv] :: BareEnv -> !(HscEnv)
[logicEnv] :: BareEnv -> !LogicMap
[dcEnv] :: BareEnv -> !DataConMap
[bounds] :: BareEnv -> !(RBEnv)
[embeds] :: BareEnv -> !(TCEmb TyCon)
[axSyms] :: BareEnv -> !(HashMap Symbol LocSymbol)
[propSyms] :: BareEnv -> !(HashMap Symbol LocSymbol)
[beConfig] :: BareEnv -> !Config
[beIndex] :: BareEnv -> !Integer
type InlnEnv = HashMap Symbol LMap
inModule :: ModName -> BareM b -> BareM b
withVArgs :: (Foldable t, PPrint a) => SourcePos -> SourcePos -> t a -> BareM b -> BareM b
setRTAlias :: Symbol -> RTAlias RTyVar SpecType -> BareM ()
setREAlias :: Symbol -> RTAlias Symbol Expr -> BareM ()
setDataDecls :: [DataDecl] -> BareM ()
execBare :: BareM a -> BareEnv -> IO (Either Error a)
insertLogicEnv :: String -> LocSymbol -> [Symbol] -> Expr -> BareM ()
insertAxiom :: Var -> Maybe Symbol -> BareM ()
addDefs :: HashSet (Var, Symbol) -> BareM ()
-- | DataConMap stores the names of those ctor-fields that have been
-- declared as SMT ADTs so we don't make up new names for them.
type DataConMap = HashMap (Symbol, Int) Symbol
dataConMap :: [DataDecl] -> DataConMap
instance Language.Haskell.Liquid.Types.Fresh.Freshable Language.Haskell.Liquid.Bare.Env.BareM GHC.Integer.Type.Integer
instance Language.Haskell.Liquid.UX.Config.HasConfig Language.Haskell.Liquid.Bare.Env.BareEnv
module Language.Haskell.Liquid.Bare.Misc
makeSymbols :: (Id -> Bool) -> [Id] -> [Symbol] -> BareM [(Symbol, Var)]
freeSymbols :: (Reftable r, Reftable r1, Reftable r2, TyConable c, TyConable c1, TyConable c2) => [Symbol] -> [(a1, Located (RType c2 tv2 r2))] -> [(a, Located (RType c1 tv1 r1))] -> [(Located (RType c tv r))] -> [LocSymbol]
joinVar :: [Var] -> (Var, s, t) -> (Var, s, t)
mkVarExpr :: Id -> 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 :: Type -> SpecType -> StateT MapTyVarST (Either Error) ()
matchKindArgs :: [SpecType] -> [SpecType] -> [SpecType]
symbolRTyVar :: Symbol -> RTyVar
simpleSymbolVar :: Var -> Symbol
hasBoolResult :: Type -> Bool
symbolMeasure :: String -> Symbol -> Maybe Int -> Symbol
isKind :: Kind -> Bool
-- | 'makeDataConChecker d' creates the measure for `is$d` which tests
-- whether a given value was created by d. e.g. is$Nil or
-- is$Cons.
makeDataConChecker :: DataCon -> Symbol
-- | 'makeDataConSelector d' creates the selector `select$d$i` which
-- projects the i-th field of a constructed value. e.g. `select$Cons$1`
-- and `select$Cons$2` are respectively equivalent to head and
-- tail.
makeDataConSelector :: Maybe DataConMap -> DataCon -> Int -> Symbol
module Language.Haskell.Liquid.Transforms.CoreToLogic
coreToDef :: Reftable r => LocSymbol -> Var -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon]
coreToFun :: LocSymbol -> Var -> CoreExpr -> LogicM ([Var], Either Expr Expr)
coreToLogic :: CoreExpr -> LogicM Expr
mkLit :: Literal -> Maybe Expr
mkI :: Integer -> Maybe Expr
mkS :: ByteString -> Maybe Expr
runToLogic :: TCEmb TyCon -> LogicMap -> DataConMap -> (String -> Error) -> LogicM t -> Either Error t
runToLogicWithBoolBinds :: [Var] -> TCEmb TyCon -> LogicMap -> DataConMap -> (String -> Error) -> LogicM t -> Either Error t
logicType :: (Reftable r) => Type -> RRType r
strengthenResult :: Var -> SpecType
strengthenResult' :: Var -> SpecType
normalize :: Simplify a => a -> a
instance Language.Haskell.Liquid.Transforms.CoreToLogic.Simplify CoreSyn.CoreExpr
instance Language.Haskell.Liquid.Transforms.CoreToLogic.Simplify CoreSyn.CoreBind
instance Language.Haskell.Liquid.Transforms.CoreToLogic.Simplify CoreSyn.CoreAlt
instance GHC.Show.Show CoreSyn.CoreExpr
module Language.Haskell.Liquid.Types.Literals
literalFRefType :: Literal -> RType RTyCon RTyVar Reft
literalFReft :: Literal -> Reft
-- | literalConst returns Nothing 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)
mkI :: Integer -> Maybe Expr
mkS :: ByteString -> Maybe Expr
module Language.Haskell.Liquid.Bare.Axiom
makeHaskellAxioms :: TCEmb TyCon -> [CoreBind] -> GhcSpec -> BareSpec -> [DataDecl] -> BareM [(Var, LocSpecType, AxiomEq)]
instance Language.Haskell.Liquid.Bare.Axiom.Subable Var.Var
instance Language.Haskell.Liquid.Bare.Axiom.Subable CoreSyn.CoreExpr
instance Language.Haskell.Liquid.Bare.Axiom.Subable CoreSyn.CoreAlt
-- | This module contains functions for recursively "rewriting" GHC core
-- using "rules".
module Language.Haskell.Liquid.Transforms.Rewrite
-- | Top-level rewriter
-- --------------------------------------------------------
rewriteBinds :: Config -> [CoreBind] -> [CoreBind]
module Language.Haskell.Liquid.Transforms.Rec
transformRecExpr :: CoreProgram -> CoreProgram
transformScope :: [Bind Id] -> [Bind Id]
outerScTr :: [Bind Id] -> [Bind Id]
innerScTr :: Functor f => f (Bind Id) -> f (Bind Id)
isIdTRecBound :: Id -> Bool
setIdTRecBound :: Id -> Id
instance Language.Haskell.Liquid.Transforms.Rec.Freshable GHC.Types.Int
instance Language.Haskell.Liquid.Transforms.Rec.Freshable Unique.Unique
instance Language.Haskell.Liquid.Transforms.Rec.Freshable Var.Var
-- | Convert GHC Core into Administrative Normal Form (ANF)
-- --------------------
module Language.Haskell.Liquid.Transforms.ANF
-- | A-Normalize a module
-- ------------------------------------------------------
anormalize :: Config -> HscEnv -> ModGuts -> IO [CoreBind]
instance GHC.Base.Applicative Language.Haskell.Liquid.Transforms.ANF.DsM
instance UniqSupply.MonadUnique Language.Haskell.Liquid.Transforms.ANF.DsM
instance GHC.Base.Monad Language.Haskell.Liquid.Transforms.ANF.DsM
instance GHC.Base.Functor Language.Haskell.Liquid.Transforms.ANF.DsM
instance Language.Haskell.Liquid.UX.Config.HasConfig Language.Haskell.Liquid.Transforms.ANF.AnfEnv
module Language.Haskell.Liquid.Constraint.Types
type CG = State CGInfo
-- | Generation: Types
-- ---------------------------------------------------------
data CGInfo
CGInfo :: !(SEnv Sort) -> ![SubC] -> ![WfC] -> ![SubC] -> ![FixSubC] -> ![Bool] -> ![FixWfC] -> !Integer -> !BindEnv -> !(AnnInfo (Annot SpecType)) -> !(HashMap TyCon RTyCon) -> ![(Var, [Int])] -> !(HashMap TyCon SpecType) -> !(HashMap Var [Located Expr]) -> !(HashSet Var) -> !(HashSet Var) -> !(HashSet TyCon) -> !(TCEmb TyCon) -> !Kuts -> ![HashSet KVar] -> !(SEnv Sort) -> !(SEnv Sort) -> ![DataDecl] -> !Bool -> !Bool -> !Bool -> ![Error] -> !KVProf -> !Int -> HashMap BindId SrcSpan -> !Bool -> !GhcInfo -> ![(Var, SpecType)] -> CGInfo
-- | top-level fixpoint env
[fEnv] :: CGInfo -> !(SEnv Sort)
-- | 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])]
-- | Mapping of new type type constructors with their refined types.
[newTyEnv] :: CGInfo -> !(HashMap TyCon SpecType)
-- | Terminating Metrics for Recursive functions
[termExprs] :: CGInfo -> !(HashMap Var [Located Expr])
-- | Set of variables to ignore for termination checking
[specLVars] :: CGInfo -> !(HashSet Var)
-- | "Lazy binders", skip termination checking
[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
-- | Fixpoint "packs" of correlated kvars
[kvPacks] :: CGInfo -> ![HashSet KVar]
-- | Global symbols in the refinement logic
[cgLits] :: CGInfo -> !(SEnv Sort)
-- | Distinct constant symbols in the refinement logic
[cgConsts] :: CGInfo -> !(SEnv Sort)
-- | ADTs extracted from Haskell 'data' definitions
[cgADTs] :: CGInfo -> ![DataDecl]
-- | Check Termination (?)
[tcheck] :: CGInfo -> !Bool
-- | Check Strata (?)
[scheck] :: CGInfo -> !Bool
-- | prune unsorted refinements
[pruneRefs] :: CGInfo -> !Bool
-- | Errors during constraint generation
[logErrors] :: CGInfo -> ![Error]
-- | 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
[allowHO] :: CGInfo -> !Bool
[ghcI] :: CGInfo -> !GhcInfo
-- | Refined Types of Data Constructors
[dataConTys] :: CGInfo -> ![(Var, SpecType)]
data CGEnv
CGE :: !SpanStack -> !REnv -> !(SEnv Var) -> !RDEnv -> !(SEnv Sort) -> !(SEnv Sort) -> !FEnv -> !(HashSet Var) -> !(HashSet Var) -> !RTyConInv -> !RTyConInv -> !RTyConIAl -> !REnv -> !REnv -> !REnv -> TCEmb TyCon -> !TagEnv -> !(Maybe TagKey) -> !(Maybe (HashMap Symbol SpecType)) -> !(HashMap Symbol CoreExpr) -> !HEnv -> !LConstraint -> !(HashMap Var Symbol) -> !(Maybe (TError SpecType)) -> !GhcInfo -> !(Maybe Var) -> CGEnv
-- | Location in original source file
[cgLoc] :: CGEnv -> !SpanStack
-- | SpecTypes for Bindings in scope
[renv] :: CGEnv -> !REnv
-- | Map from free Symbols (e.g. datacons) to Var
[syenv] :: CGEnv -> !(SEnv Var)
-- | Dictionary Environment
[denv] :: CGEnv -> !RDEnv
-- | Global literals
[litEnv] :: CGEnv -> !(SEnv Sort)
-- | Distinct literals
[constEnv] :: CGEnv -> !(SEnv Sort)
-- | Fixpoint Environment
[fenv] :: CGEnv -> !FEnv
-- | recursive defs being processed (for annotations)
[recs] :: CGEnv -> !(HashSet Var)
-- | recursive defs being processed (for annotations)
[fargs] :: CGEnv -> !(HashSet Var)
-- | Datatype invariants
[invs] :: CGEnv -> !RTyConInv
-- | Datatype recursive invariants: ignored in the base case assumed in rec
-- call
[rinvs] :: 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
-- | Top-level variables with auto generated internal types
[intys] :: 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 (c.f. LAZYVARs)
[lcb] :: CGEnv -> !(HashMap Symbol CoreExpr)
-- | Types with holes, will need refreshing
[holes] :: CGEnv -> !HEnv
-- | Logical Constraints
[lcs] :: CGEnv -> !LConstraint
-- | axiom environment maps reflected Haskell functions to the logical
-- functions
[aenv] :: CGEnv -> !(HashMap Var Symbol)
-- | error that should be reported at the user , cgCfg :: !Config -- ^
-- top-level config options
[cerr] :: CGEnv -> !(Maybe (TError SpecType))
-- | top-level GhcInfo
[cgInfo] :: CGEnv -> !GhcInfo
-- | top level function being checked
[cgVar] :: CGEnv -> !(Maybe Var)
data LConstraint
LC :: [[(Symbol, SpecType)]] -> LConstraint
-- | Fixpoint Environment
-- ------------------------------------------------------
data FEnv
FE :: !IBindEnv -> !(SEnv Sort) -> !(SEnv BindId) -> FEnv
-- | Integer Keys for Fixpoint Environment
[feBinds] :: FEnv -> !IBindEnv
-- | Fixpoint Environment
[feEnv] :: FEnv -> !(SEnv Sort)
-- | Map from Symbol to current BindId
[feIdEnv] :: FEnv -> !(SEnv BindId)
initFEnv :: [(Symbol, Sort)] -> FEnv
insertsFEnv :: FEnv -> [((Symbol, Sort), BindId)] -> FEnv
-- | Helper Types: HEnv
-- --------------------------------------------------------
data HEnv
fromListHEnv :: [Symbol] -> HEnv
elemHEnv :: Symbol -> HEnv -> Bool
-- | Subtyping Constraints
-- -----------------------------------------------------
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
type FixSubC = SubC Cinfo
subVar :: FixSubC -> Maybe Var
data WfC
WfC :: !CGEnv -> !SpecType -> WfC
type FixWfC = WfC Cinfo
type RTyConInv = HashMap RTyCon [RInv]
mkRTyConInv :: [(Maybe Var, Located SpecType)] -> RTyConInv
addRTyConInv :: RTyConInv -> SpecType -> SpecType
addRInv :: RTyConInv -> (Var, SpecType) -> (Var, SpecType)
type RTyConIAl = HashMap RTyCon [RInv]
mkRTyConIAl :: [(a, Located SpecType)] -> RTyConInv
removeInvariant :: CGEnv -> CoreBind -> (CGEnv, RTyConInv)
restoreInvariant :: CGEnv -> RTyConInv -> CGEnv
makeRecInvariants :: CGEnv -> [Var] -> CGEnv
addArgument :: CGEnv -> Var -> CGEnv
addArguments :: CGEnv -> [Var] -> CGEnv
instance GHC.Show.Show Language.Haskell.Liquid.Constraint.Types.RInv
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Constraint.Types.CGInfo
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Constraint.Types.CGInfo
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Constraint.Types.SubC
instance Language.Haskell.Liquid.Types.Strata.SubStratum Language.Haskell.Liquid.Constraint.Types.SubC
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Constraint.Types.SubC
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Constraint.Types.WfC
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Constraint.Types.WfC
instance Language.Haskell.Liquid.UX.Config.HasConfig Language.Haskell.Liquid.Constraint.Types.CGEnv
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Constraint.Types.CGEnv
instance GHC.Show.Show Language.Haskell.Liquid.Constraint.Types.CGEnv
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Constraint.Types.CGEnv
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Constraint.Types.FEnv
instance Control.DeepSeq.NFData Language.Haskell.Liquid.Constraint.Types.RInv
instance GHC.Base.Monoid Language.Haskell.Liquid.Constraint.Types.LConstraint
module Language.Haskell.Liquid.Constraint.Fresh
refreshArgsTop :: (Var, SpecType) -> CG SpecType
-- | Generation: Freshness
-- -----------------------------------------------------
--
-- Right now, we generate NO new pvars. Rather than clutter code with
-- uRType calls, put it in one place where the above invariant is
-- obviously enforced. Constraint generation should ONLY use
-- freshTy_type and freshTy_expr
freshTy_type :: KVKind -> CoreExpr -> Type -> CG SpecType
freshTy_expr :: KVKind -> CoreExpr -> Type -> CG SpecType
trueTy :: Type -> CG SpecType
addKuts :: (PPrint a) => a -> SpecType -> CG ()
instance Language.Haskell.Liquid.Types.Fresh.Freshable Language.Haskell.Liquid.Constraint.Types.CG GHC.Integer.Type.Integer
-- | This module defines the representation for Environments needed during
-- constraint generation.
module Language.Haskell.Liquid.Constraint.Env
(+++=) :: (CGEnv, String) -> (Symbol, CoreExpr, SpecType) -> CG CGEnv
(+=) :: CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
extendEnvWithVV :: CGEnv -> SpecType -> CG CGEnv
addBinders :: CGEnv -> Symbol -> [(Symbol, SpecType)] -> CG CGEnv
addSEnv :: CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
(-=) :: CGEnv -> Symbol -> CGEnv
globalize :: CGEnv -> CGEnv
fromListREnv :: [(Symbol, SpecType)] -> [(Symbol, SpecType)] -> REnv
toListREnv :: REnv -> [(Symbol, SpecType)]
insertREnv :: Symbol -> SpecType -> REnv -> REnv
localBindsOfType :: RRType r -> REnv -> [Symbol]
lookupREnv :: Symbol -> REnv -> Maybe SpecType
(?=) :: (?callStack :: CallStack) => CGEnv -> Symbol -> Maybe SpecType
rTypeSortedReft' :: (PPrint r, Reftable r, SubsTy RTyVar RSort r, Reftable (RTProp RTyCon RTyVar r)) => Bool -> CGEnv -> RRType r -> SortedReft
setLocation :: CGEnv -> Span -> CGEnv
setBind :: CGEnv -> Var -> CGEnv
setRecs :: CGEnv -> [Var] -> CGEnv
setTRec :: CGEnv -> [(Var, SpecType)] -> CGEnv
getLocation :: CGEnv -> SrcSpan
-- | This module contains various functions that add/update in the CG
-- monad.
module Language.Haskell.Liquid.Constraint.Monad
pushConsBind :: CG a -> CG a
-- | addC adds a subtyping constraint into the global pool.
addC :: SubC -> String -> CG ()
-- | addPost: RJ: what DOES this function do?
addPost :: CGEnv -> SpecType -> CG SpecType
-- | Add Well formedness Constraint
addW :: WfC -> CG ()
-- | Add a warning
addWarning :: Error -> CG ()
-- | Add Identifier Annotations, used for annotation binders (i.e. at
-- binder sites)
addIdA :: Var -> Annot SpecType -> CG ()
boundRecVar :: SrcSpan -> AnnInfo (Annot a) -> Bool
-- | Used for annotating reads (i.e. at Var x sites)
addLocA :: Maybe Var -> SrcSpan -> Annot SpecType -> CG ()
-- | Update annotations for a location, due to (ghost) predicate
-- applications
updateLocA :: Maybe SrcSpan -> SpecType -> CG ()
addA :: (Outputable a) => SrcSpan -> Maybe a -> b -> AnnInfo b -> AnnInfo b
lookupNewType :: TyCon -> CG (Maybe SpecType)
module Language.Haskell.Liquid.Constraint.Constraint
constraintToLogic :: REnv -> LConstraint -> Expr
addConstraints :: CGEnv -> [(Symbol, SpecType)] -> CGEnv
-- | Constraint Splitting
-- ------------------------------------------------------
module Language.Haskell.Liquid.Constraint.Split
splitC :: SubC -> CG [FixSubC]
splitW :: WfC -> CG [FixWfC]
splitS :: SubC -> CG [([Stratum], [Stratum])]
envToSub :: [(a, b)] -> ([(a, b)], b, b)
-- | Constraint Generation Panic
-- -----------------------------------------------
panicUnbound :: (PPrint x) => CGEnv -> x -> a
module Language.Haskell.Liquid.Bare.SymSort
txRefSort :: TCEnv -> TCEmb TyCon -> Located SpecType -> Located SpecType
module Language.Haskell.Liquid.Bare.Plugged
makePluggedSigs :: ModName -> TCEmb TyCon -> HashMap TyCon RTyCon -> NameSet -> [(Var, LocSpecType)] -> BareM [(Var, LocSpecType)]
makePluggedAsmSigs :: TCEmb TyCon -> HashMap TyCon RTyCon -> [(Var, LocSpecType)] -> BareM [(Var, LocSpecType)]
makePluggedDataCons :: TCEmb TyCon -> HashMap TyCon RTyCon -> [(DataCon, Located DataConP)] -> BareM [(DataCon, Located DataConP)]
module Language.Haskell.Liquid.Bare.Lookup
-- | Querying GHC for Id, Type, Class, Con etc.
-- --------------------------------
class Symbolic a => GhcLookup a
lookupName :: GhcLookup a => HscEnv -> ModName -> Maybe NameSpace -> a -> IO [Name]
srcSpan :: GhcLookup a => a -> SrcSpan
-- | It's possible that we have already resolved the Name we are
-- looking for, but have had to turn it back into a String, e.g.
-- to be used in an Expr, as in {v:Ordering | v = EQ}.
-- In this case, the fully-qualified Name (GHC.Types.EQ)
-- will likely not be in scope, so we store our own mapping of
-- fully-qualified Names to Vars and prefer pulling
-- Vars from it.
lookupGhcVar :: GhcLookup a => a -> BareM Var
lookupGhcTyCon :: GhcLookup a => String -> a -> BareM TyCon
lookupGhcDnTyCon :: String -> DataName -> BareM TyCon
lookupGhcDataCon :: Located Symbol -> BareM DataCon
instance Language.Haskell.Liquid.Bare.Lookup.GhcLookup (Language.Fixpoint.Types.Spans.Located Language.Fixpoint.Types.Names.Symbol)
instance Language.Haskell.Liquid.Bare.Lookup.GhcLookup Name.Name
instance Language.Haskell.Liquid.Bare.Lookup.GhcLookup FieldLabel.FieldLabel
instance Language.Haskell.Liquid.Bare.Lookup.GhcLookup Language.Haskell.Liquid.Types.DataName
instance Language.Fixpoint.Types.Names.Symbolic FieldLabel.FieldLabel
module Language.Haskell.Liquid.Bare.Resolve
class Resolvable a
resolve :: Resolvable a => SourcePos -> a -> BareM a
instance Language.Haskell.Liquid.Bare.Resolve.Resolvable a => Language.Haskell.Liquid.Bare.Resolve.Resolvable [a]
instance Language.Haskell.Liquid.Bare.Resolve.Resolvable Language.Fixpoint.Types.Constraints.Qualifier
instance Language.Haskell.Liquid.Bare.Resolve.Resolvable Language.Fixpoint.Types.Refinements.Expr
instance Language.Haskell.Liquid.Bare.Resolve.Resolvable Language.Fixpoint.Types.Names.LocSymbol
instance Language.Haskell.Liquid.Bare.Resolve.Resolvable Language.Fixpoint.Types.Names.Symbol
instance Language.Haskell.Liquid.Bare.Resolve.Resolvable Language.Fixpoint.Types.Sorts.Sort
instance Language.Haskell.Liquid.Bare.Resolve.Resolvable (Language.Haskell.Liquid.Types.UReft Language.Fixpoint.Types.Refinements.Reft)
instance Language.Haskell.Liquid.Bare.Resolve.Resolvable Language.Fixpoint.Types.Refinements.Reft
instance Language.Haskell.Liquid.Bare.Resolve.Resolvable Language.Haskell.Liquid.Types.Predicate
instance Language.Haskell.Liquid.Bare.Resolve.Resolvable t => Language.Haskell.Liquid.Bare.Resolve.Resolvable (Language.Haskell.Liquid.Types.PVar t)
instance Language.Haskell.Liquid.Bare.Resolve.Resolvable ()
module Language.Haskell.Liquid.Bare.Expand
class ExpandAliases a
expand :: ExpandAliases a => SourcePos -> a -> BareM a
expand' :: (ExpandAliases a) => a -> BareM a
instance Language.Haskell.Liquid.Bare.Expand.ExpandAliases Language.Fixpoint.Types.Refinements.Expr
instance Language.Haskell.Liquid.Bare.Expand.ExpandAliases Language.Fixpoint.Types.Refinements.Reft
instance Language.Haskell.Liquid.Bare.Expand.ExpandAliases Language.Haskell.Liquid.Types.SpecType
instance Language.Haskell.Liquid.Bare.Expand.ExpandAliases Language.Haskell.Liquid.Types.Body
instance Language.Haskell.Liquid.Bare.Expand.ExpandAliases ty => Language.Haskell.Liquid.Bare.Expand.ExpandAliases (Language.Haskell.Liquid.Types.Def ty ctor)
instance Language.Haskell.Liquid.Bare.Expand.ExpandAliases ty => Language.Haskell.Liquid.Bare.Expand.ExpandAliases (Language.Haskell.Liquid.Types.Measure ty ctor)
instance Language.Haskell.Liquid.Bare.Expand.ExpandAliases Language.Haskell.Liquid.Types.DataConP
instance Language.Haskell.Liquid.Bare.Expand.ExpandAliases Language.Haskell.Liquid.Types.RReft
instance Language.Haskell.Liquid.Bare.Expand.ExpandAliases a => Language.Haskell.Liquid.Bare.Expand.ExpandAliases (Language.Fixpoint.Types.Spans.Located a)
instance Language.Haskell.Liquid.Bare.Expand.ExpandAliases a => Language.Haskell.Liquid.Bare.Expand.ExpandAliases (GHC.Base.Maybe a)
instance Language.Haskell.Liquid.Bare.Expand.ExpandAliases a => Language.Haskell.Liquid.Bare.Expand.ExpandAliases [a]
instance Language.Haskell.Liquid.Bare.Expand.ExpandAliases b => Language.Haskell.Liquid.Bare.Expand.ExpandAliases (a, b)
module Language.Haskell.Liquid.Bare.OfType
ofBareType :: SourcePos -> BareType -> BareM SpecType
ofMeaSort :: BareType -> BareM SpecType
ofBPVar :: BPVar -> BareM RPVar
mkLSpecType :: Located BareType -> BareM (Located SpecType)
mkSpecType' :: SourcePos -> [PVar BSort] -> BareType -> BareM SpecType
module Language.Haskell.Liquid.Bare.RTEnv
-- | makeRTEnv initializes the env needed to expand
-- refinements and types, that is, the below needs to be called *before*
-- we use expand
makeRTEnv :: ModName -> BareSpec -> [(ModName, BareSpec)] -> HashMap Symbol LMap -> BareM ()
-- | This module contains (most of) the code needed to lift Haskell
-- entitites, . code- (CoreBind), and data- (Tycon) definitions into the
-- spec level.
module Language.Haskell.Liquid.Bare.Measure
makeHaskellDataDecls :: Config -> BareSpec -> [TyCon] -> [DataDecl]
makeHaskellMeasures :: TCEmb TyCon -> [CoreBind] -> BareSpec -> BareM [Measure (Located BareType) LocSymbol]
makeHaskellInlines :: TCEmb TyCon -> [CoreBind] -> BareSpec -> BareM [(LocSymbol, LMap)]
makeHaskellBounds :: TCEmb TyCon -> CoreProgram -> HashSet (Var, LocSymbol) -> BareM RBEnv
makeMeasureSpec :: (ModName, BareSpec) -> BareM (MSpec SpecType DataCon)
makeMeasureSpec' :: MSpec SpecType DataCon -> ([(Var, SpecType)], [(LocSymbol, RRType Reft)])
makeClassMeasureSpec :: MSpec (RType c tv (UReft r2)) t -> [(LocSymbol, CMeasure (RType c tv r2))]
-- | makeMeasureSelectors converts the DataCons and creates
-- the measures for the selectors and checkers that then enable
-- reflection.
makeMeasureSelectors :: Config -> DataConMap -> (DataCon, Located DataConP) -> [Measure SpecType DataCon]
strengthenHaskellMeasures :: HashSet (Located Var) -> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
strengthenHaskellInlines :: HashSet (Located Var) -> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
varMeasures :: (Monoid r) => [Var] -> [(Symbol, Located (RRType r))]
module Language.Haskell.Liquid.Bare.Spec
makeClasses :: ModName -> Config -> [Var] -> (ModName, Spec (Located BareType) bndr) -> BareM [((DataCon, DataConP), [(ModName, Var, LocSpecType)])]
makeQualifiers :: (ModName, Spec ty bndr) -> BareM [Qualifier]
makeHints :: [Var] -> Spec ty bndr -> BareM [(Var, [Int])]
makeLVar :: [Var] -> Spec ty bndr -> BareM [Var]
makeLazy :: [Var] -> Spec ty bndr -> BareM [Var]
makeAutoInsts :: [Var] -> Spec ty bndr -> BareM [(Var, Maybe Int)]
makeDefs :: [Var] -> Spec ty bndr -> BareM [(Var, Symbol)]
makeHMeas :: [Var] -> Spec ty bndr -> BareM [(Located Var, LocSymbol)]
makeHInlines :: [Var] -> Spec ty bndr -> BareM [(Located Var, LocSymbol)]
makeTExpr :: [Var] -> Spec ty bndr -> BareM [(Var, [Located Expr])]
-- | API: Bare Refinement Types
-- ------------------------------------------------
makeTargetVars :: ModName -> [Var] -> [String] -> BareM [Var]
makeAssertSpec :: ModName -> Config -> [Var] -> [Var] -> (ModName, BareSpec) -> BareM [(ModName, Var, LocSpecType)]
makeAssumeSpec :: ModName -> Config -> [Var] -> [Var] -> (ModName, BareSpec) -> BareM [(ModName, Var, LocSpecType)]
makeDefaultMethods :: [Var] -> [(ModName, Var, Located SpecType)] -> [(ModName, Var, Located SpecType)]
makeIAliases :: (ModName, Spec (Located BareType) bndr) -> BareM [(Located SpecType, Located SpecType)]
makeInvariants :: (ModName, Spec (Located BareType) bndr) -> BareM [(Maybe Var, Located SpecType)]
makeNewTypes :: (ModName, Spec (Located BareType) bndr) -> BareM [(TyCon, Located SpecType)]
makeSpecDictionaries :: TCEmb TyCon -> [Var] -> [(a, BareSpec)] -> GhcSpec -> BareM GhcSpec
makeBounds :: TCEmb TyCon -> ModName -> [Var] -> [CoreBind] -> [(ModName, BareSpec)] -> BareM ()
makeHBounds :: [Var] -> Spec ty bndr -> BareM [(Var, LocSymbol)]
lookupIds :: Bool -> [(LocSymbol, a)] -> BareM [(Var, LocSymbol, a)]
module Language.Haskell.Liquid.Bare.DataType
makeDataDecls :: Config -> TCEmb TyCon -> ModName -> [(ModName, TyCon, DataPropDecl)] -> [(DataCon, Located DataConP)] -> [DataDecl]
-- | NOTE:AUTO-INDPRED (teststodoIndPred1.hs) -- DO NOT DELETE --
-- RJ: too hard, too brittle, I _thought_ we could just -- generate the
-- F.DataDecl, but really, you need the GHC -- names for the Prop-Ctor if
-- you want to be able to `import` -- a predicate across modules. Seems a
-- LOT easier to just have -- the program explicitly create the the
-- proposition type -- e.g. as shownn in (testsposIndPred0.hs)
-- --------------------------------------------------------------------------------
--
-- type SpecTypeRep = RTypeRep RTyCon RTyVar RReft
--
--
-- - - | makePropDecl creates the DataDecl for the
-- *proposition* described
-- - - by the corresponding TyCon DataDecl, e.g.
-- testspos/IndPred0.hs makePropDecl :: F.TCEmb TyCon -> TyCon
-- -> DataPropDecl -> Maybe F.DataDecl makePropDecl tce tc (dd, pd)
-- = makePropTyDecl tce tc dd $ pd
--
--
-- makePropTyDecl :: F.TCEmb TyCon -> TyCon -> DataDecl ->
-- SpecType -> F.DataDecl makePropTyDecl tce tc dd t = F.DDecl {
-- F.ddTyCon = ftc , F.ddVars = length (ty_vars tRep) , F.ddCtors = [
-- makePropTyCtor tce ftc tRep ] } where ftc = propFTycon tc dd tRep =
-- toRTypeRep t
--
-- propFTycon :: TyCon -> DataDecl -> F.FTycon propFTycon tc =
-- F.symbolFTycon . fmap (suffixSymbol F.propConName) .
-- tyConLocSymbol tc
--
-- makePropTyCtor :: F.TCEmb TyCon -> F.FTycon -> SpecTypeRep ->
-- F.DataCtor makePropTyCtor tce ftc t = F.DCtor { F.dcName =
-- F.fTyconSymbol ftc , F.dcFields = makePropTyFields tce ftc t }
--
-- makePropTyFields :: F.TCEmb TyCon -> F.FTycon -> SpecTypeRep
-- -> [F.DataField] makePropTyFields tce ftc t = makeDataFields tce
-- ftc as xts where as = [ a | RTVar a _ <- ty_vars t ] xts = zipWith
-- (i t -> (fld i, t)) [0..] (ty_args t) tcSym = F.fTyconSymbol ftc
-- fld = F.atLoc tcSym . GM.symbolMeasure "propField" (val tcSym) . Just
--
-- isPropDecl :: F.DataDecl -> Bool isPropDecl d = (F.isSuffixOfSym
-- F.propConName . F.symbol . F.ddTyCon $ d) && (length
-- (F.ddCtors d) == 1)
--
-- qualifyDataDecl :: ModName -> DataDecl -> DataDecl
-- qualifyDataDecl name d = d { tycName = qualifyName name (tycName d)}
--
-- qualifyName :: ModName -> LocSymbol -> LocSymbol qualifyName n x
-- = F.atLoc x $ GM.qualifySymbol nSym (val x) where nSym =
-- GM.takeModuleNames (F.symbol n)
--
-- Bare Predicate: DataCon Definitions
-- ---------------------------------------
makeConTypes :: (ModName, Spec ty bndr) -> BareM ([(ModName, TyCon, TyConP, Maybe DataPropDecl)], [[(DataCon, Located DataConP)]])
makeTyConEmbeds :: (ModName, Spec ty bndr) -> BareM (TCEmb TyCon)
makeRecordSelectorSigs :: [(DataCon, Located DataConP)] -> BareM [(Var, LocSpecType)]
meetDataConSpec :: [(Var, SpecType)] -> [(DataCon, DataConP)] -> [(Var, SpecType)]
-- | makeClassEmbeds: sort-embeddings for numeric, and family-instance
-- tycons
addClassEmbeds :: Maybe [ClsInst] -> [TyCon] -> TCEmb TyCon -> TCEmb TyCon
-- | DataConMap stores the names of those ctor-fields that have been
-- declared as SMT ADTs so we don't make up new names for them.
type DataConMap = HashMap (Symbol, Int) Symbol
dataConMap :: [DataDecl] -> DataConMap
module Language.Haskell.Liquid.Bare.Check
-- | Checking GhcSpec
-- ------------------------------------------------------------------------
checkGhcSpec :: [(ModName, BareSpec)] -> SEnv SortedReft -> GhcSpec -> Either [Error] GhcSpec
checkTerminationExpr :: (Eq v, PPrint v) => TCEmb TyCon -> SEnv SortedReft -> (v, LocSpecType, [Located Expr]) -> Maybe Error
checkTy :: Bool -> (Doc -> Error) -> TCEmb TyCon -> TCEnv -> SEnv SortedReft -> Located SpecType -> Maybe Error
-- | This module contains the functions that convert from
-- descriptions of symbols, names and types (over freshly parsed
-- bare Strings), to representations connected to GHC vars,
-- names, and types. The actual representations of bare and real
-- (refinement) types are all in RefType -- they are different
-- instances of RType
module Language.Haskell.Liquid.Bare
-- | The following is the overall type for specifications obtained
-- from parsing the target source and dependent libraries
data GhcSpec
SP :: ![(Var, LocSpecType)] -> ![(Var, LocSpecType)] -> ![(Var, LocSpecType)] -> ![(Var, LocSpecType)] -> ![(Symbol, LocSpecType)] -> ![(Symbol, LocSpecType)] -> ![(Maybe Var, LocSpecType)] -> ![(LocSpecType, LocSpecType)] -> ![Located DataCon] -> ![(TyCon, TyConP)] -> ![(Symbol, Var)] -> TCEmb TyCon -> ![Qualifier] -> ![DataDecl] -> ![Var] -> ![(Var, [Int])] -> ![(Var, [Located Expr])] -> ![(TyCon, LocSpecType)] -> !(HashSet Var) -> !(HashSet Var) -> !(HashSet TyCon) -> !(HashMap Var (Maybe Int)) -> !Config -> !NameSet -> [Measure SpecType DataCon] -> HashMap TyCon RTyCon -> DEnv Var SpecType -> [AxiomEq] -> [Var] -> LogicMap -> Maybe Type -> !RTEnv -> GhcSpec
-- | Asserted Reftypes
[gsTySigs] :: GhcSpec -> ![(Var, LocSpecType)]
-- | Assumed Reftypes
[gsAsmSigs] :: GhcSpec -> ![(Var, LocSpecType)]
-- | Auto generated Signatures
[gsInSigs] :: GhcSpec -> ![(Var, LocSpecType)]
-- | Data Constructor Measure Sigs
[gsCtors] :: GhcSpec -> ![(Var, LocSpecType)]
-- | Literals/Constants e.g. datacons: EQ, GT, string lits: "zombie",...
[gsLits] :: GhcSpec -> ![(Symbol, LocSpecType)]
-- | Measure Types eg. len :: [a] -> Int
[gsMeas] :: GhcSpec -> ![(Symbol, LocSpecType)]
-- | Data Type Invariants that came from the definition of var measure eg.
-- forall a. {v: [a] | len(v) >= 0}
[gsInvariants] :: GhcSpec -> ![(Maybe Var, LocSpecType)]
-- | Data Type Invariant Aliases
[gsIaliases] :: GhcSpec -> ![(LocSpecType, LocSpecType)]
-- | Predicated Data-Constructors e.g. see testsposMap.hs
[gsDconsP] :: GhcSpec -> ![Located DataCon]
-- | Predicated Type-Constructors eg. see testsposMap.hs
[gsTconsP] :: GhcSpec -> ![(TyCon, TyConP)]
-- | List of Symbol free in spec and corresponding GHC var eg.
-- (Cons, Cons#7uz) from testsposex1.hs
[gsFreeSyms] :: GhcSpec -> ![(Symbol, Var)]
-- | How to embed GHC Tycons into fixpoint sorts e.g. "embed Set as
-- Set_set" from includeDataSet.spec
[gsTcEmbeds] :: GhcSpec -> TCEmb TyCon
-- | Qualifiers in Source/Spec files e.g testsposqualTest.hs
[gsQualifiers] :: GhcSpec -> ![Qualifier]
-- | ADTs extracted from Haskell 'data' definitions
[gsADTs] :: GhcSpec -> ![DataDecl]
-- | Top-level Binders To Verify (empty means ALL binders)
[gsTgtVars] :: GhcSpec -> ![Var]
-- | Lexicographically ordered size witnesses for termination
[gsDecr] :: GhcSpec -> ![(Var, [Int])]
-- | Lexicographically ordered expressions for termination
[gsTexprs] :: GhcSpec -> ![(Var, [Located Expr])]
-- | Mapping of 'newtype' type constructors with their refined types.
[gsNewTypes] :: GhcSpec -> ![(TyCon, LocSpecType)]
-- | Variables that should be checked in the environment they are used
[gsLvars] :: GhcSpec -> !(HashSet Var)
-- | Binders to IGNORE during termination checking
[gsLazy] :: GhcSpec -> !(HashSet Var)
-- | Binders to IGNORE during termination checking
[gsAutosize] :: GhcSpec -> !(HashSet TyCon)
-- | Binders to expand with automatic axiom instances maybe with specified
-- fuel
[gsAutoInst] :: GhcSpec -> !(HashMap Var (Maybe Int))
-- | Configuration Options
[gsConfig] :: GhcSpec -> !Config
-- | Names exported by the module being verified
[gsExports] :: GhcSpec -> !NameSet
[gsMeasures] :: GhcSpec -> [Measure SpecType DataCon]
[gsTyconEnv] :: GhcSpec -> HashMap TyCon RTyCon
-- | Dictionary Environment
[gsDicts] :: GhcSpec -> DEnv Var SpecType
-- | Axioms from reflected functions
[gsAxioms] :: GhcSpec -> [AxiomEq]
-- | Binders for reflected functions
[gsReflects] :: GhcSpec -> [Var]
[gsLogicMap] :: GhcSpec -> LogicMap
[gsProofType] :: GhcSpec -> Maybe Type
-- | Refinement type aliases
[gsRTAliases] :: GhcSpec -> !RTEnv
makeGhcSpec :: Config -> FilePath -> ModName -> [CoreBind] -> [TyCon] -> Maybe [ClsInst] -> [Var] -> [Var] -> NameSet -> HscEnv -> Either Error LogicMap -> [(ModName, BareSpec)] -> IO GhcSpec
loadLiftedSpec :: Config -> FilePath -> IO BareSpec
saveLiftedSpec :: FilePath -> ModName -> BareSpec -> IO ()
module Language.Haskell.Liquid.GHC.Interface
-- | GHC Interface Pipeline
-- ----------------------------------------------------
getGhcInfos :: Maybe HscEnv -> Config -> [FilePath] -> IO ([GhcInfo], HscEnv)
-- | GHC Configuration & Setup
-- -------------------------------------------------
runLiquidGhc :: Maybe HscEnv -> Config -> Ghc a -> IO a
pprintCBs :: [CoreBind] -> Doc
isExportedVar :: GhcInfo -> Var -> Bool
-- | Extract Ids
-- ---------------------------------------------------------------
exportedVars :: GhcInfo -> [Var]
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.GhcSpec
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.GhcInfo
instance GHC.Show.Show Language.Haskell.Liquid.Types.GhcInfo
instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.TargetVars
instance Language.Haskell.Liquid.UX.Tidy.Result HscTypes.SourceError
-- | This module defines the representation of Subtyping and WF
-- Constraints, and the code for syntax-directed constraint generation.
module Language.Haskell.Liquid.Constraint.Init
initEnv :: GhcInfo -> CG CGEnv
initCGI :: Config -> GhcInfo -> CGInfo
-- | This module defines the representation of Subtyping and WF
-- Constraints, and the code for syntax-directed constraint generation.
module Language.Haskell.Liquid.Constraint.Generate
-- | Constraint Generation: Toplevel
-- -------------------------------------------
generateConstraints :: GhcInfo -> CGInfo
instance Data.Traversable.Traversable Language.Haskell.Liquid.Constraint.Generate.Template
instance Data.Foldable.Foldable Language.Haskell.Liquid.Constraint.Generate.Template
instance GHC.Base.Functor Language.Haskell.Liquid.Constraint.Generate.Template
instance GHC.Show.Show a => GHC.Show.Show (Language.Haskell.Liquid.Constraint.Generate.Template a)
module Language.Haskell.Liquid.Constraint.Qualifier
qualifiers :: GhcInfo -> SEnv Sort -> [Qualifier]
-- | Use explicitly given qualifiers .spec or source (.hs, .lhs) files
useSpcQuals :: (HasConfig t) => t -> Bool
module Language.Haskell.Liquid.Constraint.ToFixpoint
cgInfoFInfo :: GhcInfo -> CGInfo -> IO (FInfo Cinfo)
fixConfig :: FilePath -> Config -> Config
module Test.Target.Expr
eq :: Expr -> Expr -> Expr
infix 4 `eq`
ge :: Expr -> Expr -> Expr
infix 5 `ge`
le :: Expr -> Expr -> Expr
infix 5 `le`
gt :: Expr -> Expr -> Expr
infix 5 `gt`
lt :: Expr -> Expr -> Expr
infix 5 `lt`
iff :: Expr -> Expr -> Expr
infix 3 `iff`
imp :: Expr -> Expr -> Expr
infix 3 `imp`
app :: Symbolic a => a -> [Expr] -> Expr
var :: Symbolic a => a -> Expr
prop :: Expr -> Expr
instance GHC.Num.Num Language.Fixpoint.Types.Refinements.Expr
module Test.Target.Types
data TargetException
SmtFailedToProduceOutput :: TargetException
SmtError :: String -> TargetException
ExpectedValues :: Response -> TargetException
PreconditionCheckFailed :: String -> TargetException
EvalError :: String -> TargetException
ensureValues :: MonadThrow m => m Response -> m Response
type Constraint = [Expr]
type Variable = (Symbol, Sort)
type Value = Text
type DataConEnv = [(Symbol, SpecType)]
type MeasureEnv = [Measure SpecType DataCon]
boolsort :: Sort
choicesort :: Sort
data Result
Passed :: !Int -> Result
Failed :: !String -> Result
Errored :: !String -> Result
data Val
VB :: !Bool -> Val
VV :: !Constant -> Val
VX :: !SymConst -> Val
VS :: !(Set Val) -> Val
VC :: Symbol -> [Val] -> Val
instance GHC.Classes.Ord Test.Target.Types.Val
instance GHC.Classes.Eq Test.Target.Types.Val
instance GHC.Show.Show Test.Target.Types.Val
instance GHC.Generics.Generic Test.Target.Types.Val
instance GHC.Show.Show Test.Target.Types.Result
instance Language.Fixpoint.Types.PrettyPrint.PPrint Test.Target.Types.Val
instance Language.Fixpoint.Types.Names.Symbolic Test.Target.Types.Variable
instance Language.Fixpoint.Smt.Types.SMTLIB2 Test.Target.Types.Constraint
instance GHC.Show.Show Test.Target.Types.TargetException
instance GHC.Exception.Exception Test.Target.Types.TargetException
module Test.Target.Util
type Depth = Int
io :: MonadIO m => IO a -> m a
myTrace :: Show a => String -> a -> a
reft :: SpecType -> Reft
data HList (a :: [*])
[Nil] :: HList '[]
[:::] :: a -> HList bs -> HList (a : bs)
type AllHave (c :: k -> Constraint) (xs :: [k]) = Constraints (Map c xs)
makeDecl :: SEnv DataDecl -> Symbol -> Sort -> Command
deconSort :: Sort -> ([Sort], Sort)
safeFromJust :: String -> Maybe a -> a
applyPreds :: SpecType -> SpecType -> [(Symbol, SpecType)]
propPsToProp :: [(RPVar, SpecProp)] -> SpecProp -> SpecProp
propPToProp :: (RPVar, SpecProp) -> SpecProp -> SpecProp
splitEApp_maybe :: Expr -> Maybe (Symbol, [Expr])
stripQuals :: SpecType -> SpecType
fourth4 :: (t, t1, t2, t3) -> t3
getSpec :: [String] -> FilePath -> IO GhcSpec
runGhc :: [String] -> Ghc a -> IO a
loadModule :: FilePath -> Ghc ModSummary
instance Test.Target.Util.AllHave GHC.Show.Show as => GHC.Show.Show (Test.Target.Util.HList as)
module Test.Target.Monad
whenVerbose :: Target () -> Target ()
noteUsed :: (Symbol, Value) -> Target ()
addDep :: Symbol -> Expr -> Target ()
addConstraint :: Expr -> Target ()
addConstructor :: Variable -> Target ()
addSort :: Sort -> Target ()
addVariable :: Variable -> Target ()
inModule :: Symbol -> Target a -> Target a
making :: Sort -> Target a -> Target a
-- | Find the refined type of a data constructor.
lookupCtor :: Symbol -> SpecType -> Target SpecType
-- | Given a data constructor d and an action, create a new choice
-- variable c and execute the action while guarding any
-- generated constraints with c. Returns (action-result,
-- c).
guarded :: String -> Target Expr -> Target (Expr, Expr)
-- | Generate a fresh variable of the given Sort.
fresh :: Sort -> Target Symbol
-- | Given a data constructor d, create a new choice variable
-- corresponding to d.
freshChoice :: String -> Target Symbol
freshInt :: Target Int
-- | Ask the SMT solver for the Value of the given variable.
getValue :: Symbol -> Target Value
data Target a
runTarget :: TargetOpts -> TargetState -> Target a -> IO a
data TargetState
TargetState :: ![Variable] -> ![Variable] -> !Constraint -> !(HashMap Symbol [Symbol]) -> ![(Symbol, Value)] -> !DataConEnv -> !MeasureEnv -> !(TCEmb TyCon) -> !(HashMap TyCon RTyCon) -> ![(Symbol, Symbol)] -> ![Variable] -> ![(Symbol, SpecType)] -> !(Maybe Symbol) -> !(HashSet Sort) -> !Symbol -> !FilePath -> !Sort -> !Context -> TargetState
[variables] :: TargetState -> ![Variable]
[choices] :: TargetState -> ![Variable]
[constraints] :: TargetState -> !Constraint
[deps] :: TargetState -> !(HashMap Symbol [Symbol])
[realized] :: TargetState -> ![(Symbol, Value)]
[ctorEnv] :: TargetState -> !DataConEnv
[measEnv] :: TargetState -> !MeasureEnv
[embEnv] :: TargetState -> !(TCEmb TyCon)
[tyconInfo] :: TargetState -> !(HashMap TyCon RTyCon)
[freesyms] :: TargetState -> ![(Symbol, Symbol)]
[constructors] :: TargetState -> ![Variable]
[sigs] :: TargetState -> ![(Symbol, SpecType)]
[chosen] :: TargetState -> !(Maybe Symbol)
[sorts] :: TargetState -> !(HashSet Sort)
[modName] :: TargetState -> !Symbol
[filePath] :: TargetState -> !FilePath
[makingTy] :: TargetState -> !Sort
[smtContext] :: TargetState -> !Context
initState :: FilePath -> GhcSpec -> Context -> TargetState
data TargetOpts
TargetOpts :: !Int -> !SMTSolver -> !Bool -> !Bool -> !Bool -> !(Maybe Int) -> !Bool -> ![String] -> TargetOpts
[depth] :: TargetOpts -> !Int
[solver] :: TargetOpts -> !SMTSolver
[verbose] :: TargetOpts -> !Bool
[logging] :: TargetOpts -> !Bool
-- | whether to keep going after finding a counter-example, useful for
-- checking coverage
[keepGoing] :: TargetOpts -> !Bool
-- | whether to stop after a certain number of successful tests, or
-- enumerate the whole input space
[maxSuccess] :: TargetOpts -> !(Maybe Int)
-- | whether to use SmallCheck's notion of depth
[scDepth] :: TargetOpts -> !Bool
-- | extra options to pass to GHC
[ghcOpts] :: TargetOpts -> ![String]
defaultOpts :: TargetOpts
instance Control.Monad.Reader.Class.MonadReader Test.Target.Monad.TargetOpts Test.Target.Monad.Target
instance Control.Monad.Catch.MonadCatch Test.Target.Monad.Target
instance Control.Monad.State.Class.MonadState Test.Target.Monad.TargetState Test.Target.Monad.Target
instance GHC.Base.Alternative Test.Target.Monad.Target
instance Control.Monad.IO.Class.MonadIO Test.Target.Monad.Target
instance GHC.Base.Monad Test.Target.Monad.Target
instance GHC.Base.Applicative Test.Target.Monad.Target
instance GHC.Base.Functor Test.Target.Monad.Target
instance Control.Monad.Catch.MonadThrow Test.Target.Monad.Target
module Test.Target.Eval
-- | Evaluate a refinement with the given expression substituted for the
-- value variable.
eval :: Reft -> Expr -> Target Bool
-- | Evaluate a refinement with the given expression substituted for the
-- value variable, in the given environment of free symbols.
evalWith :: HashMap Symbol Val -> Reft -> Expr -> Target Bool
evalExpr :: Expr -> HashMap Symbol Val -> Target Val
module Test.Target.Targetable
-- | A class of datatypes for which we can efficiently generate constrained
-- values by querying an SMT solver.
--
-- If possible, instances should not be written by hand, but rather by
-- using the default implementations via GHC.Generics, e.g.
--
--
-- import GHC.Generics
-- import Test.Target.Targetable
--
-- data Foo = ... deriving Generic
-- instance Targetable Foo
--
class Targetable a
-- | Construct an SMT query describing all values of the given type up to
-- the given Depth.
query :: (Targetable a, (?loc :: CallStack)) => Proxy a -> Depth -> Symbol -> SpecType -> Target Symbol
-- | Reconstruct a Haskell value from the SMT model.
decode :: Targetable a => Symbol -> SpecType -> Target a
-- | Check whether a Haskell value inhabits the given type. Also returns a
-- logical expression corresponding to the Haskell value.
check :: Targetable a => a -> SpecType -> Target (Bool, Expr)
-- | Translate a Haskell value into a logical expression.
toExpr :: Targetable a => a -> Expr
-- | What is the Haskell type? (Mainly used to make the SMT queries more
-- readable).
getType :: Targetable a => Proxy a -> Sort
-- | What is the Haskell type? (Mainly used to make the SMT queries more
-- readable).
getType :: (Targetable a, Generic a, Rep a ~ D1 d f, Datatype d) => Proxy a -> Sort
-- | Construct an SMT query describing all values of the given type up to
-- the given Depth.
query :: (Targetable a, (?loc :: CallStack)) => (Generic a, GQuery (Rep a)) => Proxy a -> Int -> Symbol -> SpecType -> Target Symbol
-- | Translate a Haskell value into a logical expression.
toExpr :: (Targetable a, Generic a, GToExpr (Rep a)) => a -> Expr
-- | Reconstruct a Haskell value from the SMT model.
decode :: (Targetable a, Generic a, GDecode (Rep a)) => Symbol -> SpecType -> Target a
-- | Check whether a Haskell value inhabits the given type. Also returns a
-- logical expression corresponding to the Haskell value.
check :: (Targetable a, Generic a, GCheck (Rep a)) => a -> SpecType -> Target (Bool, Expr)
qquery :: Targetable a => Proxy a -> Int -> SpecType -> Target Symbol
-- | Given a data constuctor d and a refined type for ds
-- output, return a list of types representing suitable arguments for
-- d.
unfold :: Symbol -> SpecType -> Target [(Symbol, SpecType)]
-- | Given a data constructor d and a list of expressions
-- xs, construct a new expression corresponding to d
-- xs.
apply :: Symbol -> SpecType -> [Expr] -> Target Expr
-- | Split a symbolic variable representing the application of a data
-- constructor into a pair of the data constructor and the sub-variables.
unapply :: Symbol -> Target (Symbol, [Symbol])
-- | Given a symbolic variable and a list of (choice, var) pairs,
-- oneOf x choices asserts that x must equal one of the
-- vars in choices.
oneOf :: Symbol -> [(Expr, Expr)] -> Target ()
-- | Given a symbolic variable x, figure out which of xs
-- choice varaibles was picked and return it.
whichOf :: Symbol -> Target Symbol
-- | Assert a logical predicate, guarded by the current choice variable.
constrain :: (?loc :: CallStack) => Expr -> Target ()
-- | Given a refinement {v | p} and an expression e,
-- construct the predicate p[e/v].
ofReft :: Reft -> Expr -> Expr
instance Test.Target.Targetable.Targetable a => Test.Target.Targetable.GCheckFields (GHC.Generics.K1 i a)
instance (GHC.Generics.Constructor c, Test.Target.Targetable.GCheckFields f) => Test.Target.Targetable.GCheck (GHC.Generics.C1 c f)
instance (Test.Target.Targetable.GCheckFields f, Test.Target.Targetable.GCheckFields g) => Test.Target.Targetable.GCheckFields (f GHC.Generics.:*: g)
instance Test.Target.Targetable.GCheckFields f => Test.Target.Targetable.GCheckFields (GHC.Generics.S1 c f)
instance Test.Target.Targetable.GCheckFields GHC.Generics.U1
instance Test.Target.Targetable.Targetable a => Test.Target.Targetable.GDecodeFields (GHC.Generics.K1 i a)
instance (GHC.Generics.Constructor c, Test.Target.Targetable.GDecodeFields f) => Test.Target.Targetable.GDecode (GHC.Generics.C1 c f)
instance (Test.Target.Targetable.GDecodeFields f, Test.Target.Targetable.GDecodeFields g) => Test.Target.Targetable.GDecodeFields (f GHC.Generics.:*: g)
instance Test.Target.Targetable.GDecodeFields f => Test.Target.Targetable.GDecodeFields (GHC.Generics.S1 c f)
instance Test.Target.Targetable.GDecodeFields GHC.Generics.U1
instance (GHC.Generics.Constructor c, Test.Target.Targetable.GRecursive f, Test.Target.Targetable.GQueryFields f) => Test.Target.Targetable.GQueryCtors (GHC.Generics.C1 c f)
instance (Test.Target.Targetable.GQueryFields f, Test.Target.Targetable.GQueryFields g) => Test.Target.Targetable.GQueryFields (f GHC.Generics.:*: g)
instance Test.Target.Targetable.GQuery f => Test.Target.Targetable.GQueryFields (GHC.Generics.S1 c f)
instance Test.Target.Targetable.GQueryFields GHC.Generics.U1
instance (Test.Target.Targetable.GRecursive f, Test.Target.Targetable.GRecursive g) => Test.Target.Targetable.GRecursive (f GHC.Generics.:*: g)
instance Test.Target.Targetable.Targetable a => Test.Target.Targetable.GRecursive (GHC.Generics.S1 c (GHC.Generics.K1 i a))
instance Test.Target.Targetable.GRecursive GHC.Generics.U1
instance (GHC.Generics.Constructor c, Test.Target.Targetable.GToExprFields f) => Test.Target.Targetable.GToExprCtor (GHC.Generics.C1 c f)
instance (Test.Target.Targetable.GToExprFields f, Test.Target.Targetable.GToExprFields g) => Test.Target.Targetable.GToExprFields (f GHC.Generics.:*: g)
instance Test.Target.Targetable.GToExpr f => Test.Target.Targetable.GToExprFields (GHC.Generics.S1 c f)
instance Test.Target.Targetable.GToExprFields GHC.Generics.U1
instance (GHC.Generics.Datatype c, Test.Target.Targetable.GQueryCtors f) => Test.Target.Targetable.GQuery (GHC.Generics.D1 c f)
instance (Test.Target.Targetable.GQueryCtors f, Test.Target.Targetable.GQueryCtors g) => Test.Target.Targetable.GQueryCtors (f GHC.Generics.:+: g)
instance (GHC.Generics.Datatype c, Test.Target.Targetable.GToExprCtor f) => Test.Target.Targetable.GToExpr (GHC.Generics.D1 c f)
instance (Test.Target.Targetable.GToExprCtor f, Test.Target.Targetable.GToExprCtor g) => Test.Target.Targetable.GToExprCtor (f GHC.Generics.:+: g)
instance Test.Target.Targetable.Targetable ()
instance Test.Target.Targetable.Targetable GHC.Types.Int
instance Test.Target.Targetable.Targetable GHC.Integer.Type.Integer
instance Test.Target.Targetable.Targetable GHC.Types.Char
instance Test.Target.Targetable.Targetable GHC.Word.Word8
instance Test.Target.Targetable.Targetable GHC.Types.Bool
instance Test.Target.Targetable.Targetable a => Test.Target.Targetable.Targetable [a]
instance Test.Target.Targetable.Targetable a => Test.Target.Targetable.Targetable (GHC.Base.Maybe a)
instance (Test.Target.Targetable.Targetable a, Test.Target.Targetable.Targetable b) => Test.Target.Targetable.Targetable (Data.Either.Either a b)
instance (Test.Target.Targetable.Targetable a, Test.Target.Targetable.Targetable b) => Test.Target.Targetable.Targetable (a, b)
instance (Test.Target.Targetable.Targetable a, Test.Target.Targetable.Targetable b, Test.Target.Targetable.Targetable c) => Test.Target.Targetable.Targetable (a, b, c)
instance (Test.Target.Targetable.Targetable a, Test.Target.Targetable.Targetable b, Test.Target.Targetable.Targetable c, Test.Target.Targetable.Targetable d) => Test.Target.Targetable.Targetable (a, b, c, d)
instance Test.Target.Targetable.Targetable a => Test.Target.Targetable.GToExpr (GHC.Generics.K1 i a)
instance Test.Target.Targetable.Targetable a => Test.Target.Targetable.GQuery (GHC.Generics.K1 i a)
instance (GHC.Generics.Datatype c, Test.Target.Targetable.GCheck f) => Test.Target.Targetable.GCheck (GHC.Generics.D1 c f)
instance (Test.Target.Targetable.GCheck f, Test.Target.Targetable.GCheck g) => Test.Target.Targetable.GCheck (f GHC.Generics.:+: g)
instance (GHC.Generics.Datatype c, Test.Target.Targetable.GDecode f) => Test.Target.Targetable.GDecode (GHC.Generics.D1 c f)
instance (Test.Target.Targetable.GDecode f, Test.Target.Targetable.GDecode g) => Test.Target.Targetable.GDecode (f GHC.Generics.:+: g)
module Test.Target.Testable
-- | Test that a function inhabits the given refinement type by enumerating
-- valid inputs and calling the function on the inputs.
test :: Testable f => f -> SpecType -> Target Result
-- | A class of functions that Target can test. A function is
-- Testable iff all of its component types are
-- Targetable and all of its argument types are Showable.
--
-- You should never have to define a new Testable instance.
class (AllHave Targetable (Args f), Targetable (Res f), AllHave Show (Args f)) => Testable f
setup :: Target ()
instance (GHC.Show.Show a, Test.Target.Targetable.Targetable a, Test.Target.Testable.Testable b) => Test.Target.Testable.Testable (a -> b)
instance (Test.Target.Targetable.Targetable a, Test.Target.Util.Args a ~ '[], Test.Target.Util.Res a ~ a) => Test.Target.Testable.Testable a
module Test.Target.Targetable.Function
instance (Test.Target.Targetable.Targetable a, Test.Target.Targetable.Targetable b, b ~ Test.Target.Util.Res (a -> b)) => Test.Target.Targetable.Targetable (a -> b)
instance (Test.Target.Targetable.Targetable a, Test.Target.Targetable.Targetable b, Test.Target.Targetable.Targetable c, c ~ Test.Target.Util.Res (a -> b -> c)) => Test.Target.Targetable.Targetable (a -> b -> c)
instance (Test.Target.Targetable.Targetable a, Test.Target.Targetable.Targetable b, Test.Target.Targetable.Targetable c, Test.Target.Targetable.Targetable d, d ~ Test.Target.Util.Res (a -> b -> c -> d)) => Test.Target.Targetable.Targetable (a -> b -> c -> d)
module Language.Haskell.Liquid.Model
getModels :: GhcInfo -> Config -> FixResult Error -> IO (FixResult Error)
getModel :: GhcInfo -> Config -> Error -> Ghc Error
getModel' :: GhcInfo -> Config -> Error -> Ghc Error
withContext :: Config -> SMTSolver -> FilePath -> (Context -> IO a) -> IO a
toFixCfg :: Config -> Config
dictProxy :: forall t. Dict (Targetable t) -> Proxy t
asTypeOfDict :: forall t. t -> Dict (Targetable t) -> t
data Dict :: Constraint -> *
[Dict] :: a => Dict a
data TargetDict
TargetDict :: (Dict (Targetable t)) -> TargetDict
addDicts :: [PredType] -> [(Symbol, SpecType)] -> Ghc [(Symbol, SpecType, Maybe TargetDict)]
addDict :: [PredType] -> (Symbol, SpecType) -> Ghc (Symbol, SpecType, Maybe TargetDict)
addDict' :: [PredType] -> (Symbol, SpecType) -> Ghc (Symbol, SpecType, Maybe TargetDict)
type Su = [(TyVar, Type)]
-- | Attempt to monomorphize a Type according to simple defaulting
-- rules.
monomorphize :: [PredType] -> Type -> Ghc (Maybe Su)
monomorphizeOne :: [PredType] -> TyVar -> Maybe Su -> Ghc (Maybe Su)
monomorphizeFree :: TyVar -> Su -> Maybe Su
hscParsedStmt :: HscEnv -> GhciLStmt RdrName -> IO (Maybe ([Id], IO [HValue], FixityEnv))
handleWarnings :: Hsc ()
ioMsgMaybe :: IO (Messages, Maybe a) -> Hsc a
throwErrors :: ErrorMessages -> Hsc a
getWarnings :: Hsc WarningMessages
clearWarnings :: Hsc ()
logWarnings :: WarningMessages -> Hsc ()
hscParsedDecls :: HscEnv -> [LHsDecl RdrName] -> IO ([TyThing], InteractiveContext)
module Language.Haskell.Liquid.Liquid
liquid :: [String] -> IO b
-- | This fellow does the real work
runLiquid :: MbEnv -> Config -> IO (ExitCode, MbEnv)
type MbEnv = Maybe HscEnv
liquidConstraints :: Config -> IO (Either [CGInfo] ExitCode)
instance GHC.Show.Show Language.Haskell.Liquid.Types.Cinfo
module Language.Haskell.Liquid.Interactive.Types
-- | Command
-- ------------------------------------------------------------------
type Command = Config
type Response = (Status, Int)
status :: ExitCode -> Status
-- | State
-- --------------------------------------------------------------------
data State
State :: Int -> MbEnv -> State
[sCount] :: State -> Int
[sMbEnv] :: State -> MbEnv
instance GHC.Show.Show Language.Haskell.Liquid.Interactive.Types.Status
instance Data.Data.Data Language.Haskell.Liquid.Interactive.Types.Status
instance GHC.Generics.Generic Language.Haskell.Liquid.Interactive.Types.Status
instance Data.Serialize.Serialize Language.Haskell.Liquid.Interactive.Types.Status
module Language.Haskell.Liquid.Interactive.Handler
initial :: State
handler :: MVar State -> Command -> IO Response
module Test.Target
-- | Test whether a function inhabits its refinement type by enumerating
-- valid inputs and calling the function.
target :: Testable f => f -> String -> FilePath -> IO ()
-- | Like target, but returns the Result instead of printing
-- to standard out.
targetResult :: Testable f => f -> String -> FilePath -> IO Result
-- | Like target, but accepts options to control the enumeration
-- depth, solver, and verbosity.
targetWith :: Testable f => f -> String -> FilePath -> TargetOpts -> IO ()
-- | Like targetWith, but returns the Result instead of
-- printing to standard out.
targetResultWith :: Testable f => f -> String -> FilePath -> TargetOpts -> IO Result
targetTH :: Name -> Q (TExp (FilePath -> IO ()))
targetResultTH :: Name -> Q (TExp (FilePath -> IO Result))
targetWithTH :: Name -> Q (TExp (FilePath -> TargetOpts -> IO ()))
targetResultWithTH :: Name -> Q (TExp (FilePath -> TargetOpts -> IO Result))
data Result
Passed :: !Int -> Result
Failed :: !String -> Result
Errored :: !String -> Result
-- | A class of functions that Target can test. A function is
-- Testable iff all of its component types are
-- Targetable and all of its argument types are Showable.
--
-- You should never have to define a new Testable instance.
class (AllHave Targetable (Args f), Targetable (Res f), AllHave Show (Args f)) => Testable f
-- | A class of datatypes for which we can efficiently generate constrained
-- values by querying an SMT solver.
--
-- If possible, instances should not be written by hand, but rather by
-- using the default implementations via GHC.Generics, e.g.
--
--
-- import GHC.Generics
-- import Test.Target.Targetable
--
-- data Foo = ... deriving Generic
-- instance Targetable Foo
--
class Targetable a
-- | Construct an SMT query describing all values of the given type up to
-- the given Depth.
query :: (Targetable a, (?loc :: CallStack)) => Proxy a -> Depth -> Symbol -> SpecType -> Target Symbol
-- | Reconstruct a Haskell value from the SMT model.
decode :: Targetable a => Symbol -> SpecType -> Target a
-- | Check whether a Haskell value inhabits the given type. Also returns a
-- logical expression corresponding to the Haskell value.
check :: Targetable a => a -> SpecType -> Target (Bool, Expr)
-- | Translate a Haskell value into a logical expression.
toExpr :: Targetable a => a -> Expr
-- | What is the Haskell type? (Mainly used to make the SMT queries more
-- readable).
getType :: Targetable a => Proxy a -> Sort
-- | What is the Haskell type? (Mainly used to make the SMT queries more
-- readable).
getType :: (Targetable a, Generic a, Rep a ~ D1 d f, Datatype d) => Proxy a -> Sort
-- | Construct an SMT query describing all values of the given type up to
-- the given Depth.
query :: (Targetable a, (?loc :: CallStack)) => (Generic a, GQuery (Rep a)) => Proxy a -> Int -> Symbol -> SpecType -> Target Symbol
-- | Translate a Haskell value into a logical expression.
toExpr :: (Targetable a, Generic a, GToExpr (Rep a)) => a -> Expr
-- | Reconstruct a Haskell value from the SMT model.
decode :: (Targetable a, Generic a, GDecode (Rep a)) => Symbol -> SpecType -> Target a
-- | Check whether a Haskell value inhabits the given type. Also returns a
-- logical expression corresponding to the Haskell value.
check :: (Targetable a, Generic a, GCheck (Rep a)) => a -> SpecType -> Target (Bool, Expr)
data TargetOpts
TargetOpts :: !Int -> !SMTSolver -> !Bool -> !Bool -> !Bool -> !(Maybe Int) -> !Bool -> ![String] -> TargetOpts
[depth] :: TargetOpts -> !Int
[solver] :: TargetOpts -> !SMTSolver
[verbose] :: TargetOpts -> !Bool
[logging] :: TargetOpts -> !Bool
-- | whether to keep going after finding a counter-example, useful for
-- checking coverage
[keepGoing] :: TargetOpts -> !Bool
-- | whether to stop after a certain number of successful tests, or
-- enumerate the whole input space
[maxSuccess] :: TargetOpts -> !(Maybe Int)
-- | whether to use SmallCheck's notion of depth
[scDepth] :: TargetOpts -> !Bool
-- | extra options to pass to GHC
[ghcOpts] :: TargetOpts -> ![String]
defaultOpts :: TargetOpts
data Test
T :: t -> Test
-- | Monomorphise an arbitrary property by defaulting all type variables to
-- Integer.
--
-- For example, if f has type Ord a => [a] ->
-- [a] then $(monomorphic 'f) has type
-- [Integer] -> [Integer].
--
-- If you want to use monomorphic in the same file where you
-- defined the property, the same scoping problems pop up as in
-- quickCheckAll: see the note there about return [].
monomorphic :: Name -> ExpQ