-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Liquid Types for Haskell -- -- Liquid Types for Haskell. @package liquidhaskell @version 0.6.0.0 module Language.Haskell.Liquid.Desugar710.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.Desugar710.DsForeign dsForeigns :: [LForeignDecl Id] -> DsM (ForeignStubs, OrdList Binding) dsForeigns' :: [LForeignDecl Id] -> DsM (ForeignStubs, OrdList Binding) dsFImport :: Id -> Coercion -> ForeignImport -> DsM ([Binding], SDoc, SDoc) dsCImport :: Id -> Coercion -> CImportSpec -> CCallConv -> Safety -> Maybe Header -> DsM ([Binding], SDoc, SDoc) dsFCall :: Id -> Coercion -> ForeignCall -> Maybe Header -> DsM ([(Id, Expr TyVar)], SDoc, SDoc) dsPrimCall :: Id -> Coercion -> ForeignCall -> DsM ([(Id, Expr TyVar)], SDoc, SDoc) dsFExport :: Id -> Coercion -> CLabelString -> CCallConv -> Bool -> DsM (SDoc, SDoc, String, Int) dsFExportDynamic :: Id -> Coercion -> CCallConv -> DsM ([Binding], SDoc, SDoc) mkFExportCBits :: DynFlags -> FastString -> Maybe Id -> [Type] -> Type -> Bool -> CCallConv -> (SDoc, SDoc, String, Int) toCType :: Type -> (Maybe Header, SDoc) foreignExportInitialiser :: Id -> SDoc module Language.Haskell.Liquid.Desugar710.Coverage addTicksToBinds :: DynFlags -> Module -> ModLocation -> NameSet -> [TyCon] -> LHsBinds Id -> IO (LHsBinds Id, HpcInfo, ModBreaks) hpcInitCode :: Module -> HpcInfo -> SDoc instance GHC.Classes.Eq Language.Haskell.Liquid.Desugar710.Coverage.TickishType instance GHC.Classes.Eq Language.Haskell.Liquid.Desugar710.Coverage.TickDensity instance GHC.Base.Functor Language.Haskell.Liquid.Desugar710.Coverage.TM instance GHC.Base.Applicative Language.Haskell.Liquid.Desugar710.Coverage.TM instance GHC.Base.Monad Language.Haskell.Liquid.Desugar710.Coverage.TM instance DynFlags.HasDynFlags Language.Haskell.Liquid.Desugar710.Coverage.TM instance UniqSupply.MonadUnique Language.Haskell.Liquid.Desugar710.Coverage.TM module Language.Haskell.Liquid.Prover.Names exprToBoolSym :: Symbol module Language.Haskell.Liquid.Prover.SMTInterface makeContext :: FilePath -> [(Symbol, Sort)] -> IO Context checkValid :: Context -> [Expr] -> Expr -> IO Bool assert :: Context -> Expr -> IO () module Language.Haskell.Liquid.Prover.Misc -- | Powerset powerset :: [a] -> [[a]] powerset' :: [a] -> [[a]] (/\/) :: [a] -> [a] -> [a] findM :: (Monad m) => (a -> m Bool) -> [a] -> m (Maybe a) mapSnd :: (t -> t2) -> (t1, t) -> (t1, t2) second3 :: (t -> t2) -> (t1, t, t3) -> (t1, t2, t3) module Language.Haskell.Liquid.Prover.Constants debug :: Bool whenLoud :: Monad m => m () -> m () delta :: Int epsilon :: Int default_depth :: Int smtFileExtention :: [Char] smtFile :: [Char] -> [Char] module Paths_liquidhaskell version :: Version getBinDir :: IO FilePath getLibDir :: IO FilePath getDataDir :: IO FilePath getLibexecDir :: IO FilePath getDataFileName :: FilePath -> IO FilePath getSysconfDir :: IO FilePath -- | Command Line Config Options -- -------------------------------------------- module Language.Haskell.Liquid.UX.Config data Config Config :: [FilePath] -> [FilePath] -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> [String] -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Maybe Int -> Int -> Int -> Int -> Maybe SMTSolver -> Bool -> Bool -> Bool -> [String] -> [String] -> Bool -> Int -> Bool -> Bool -> Bool -> Bool -> Config -- | source files to check [files] :: Config -> [FilePath] -- | path to directory for including specs [idirs] :: Config -> [FilePath] -- | new liquid-fixpoint sort check [newcheck] :: Config -> Bool -- | check subset of binders modified (+ dependencies) since last check [diffcheck] :: Config -> Bool -- | uninterpreted integer multiplication and division [linear] :: Config -> Bool -- | allow higher order binders into the logic [higherorder] :: Config -> Bool -- | check all binders (overrides diffcheck) [fullcheck] :: Config -> Bool -- | save fixpoint query [saveQuery] :: Config -> Bool -- | set of binders to check [binders] :: Config -> [String] -- | whether to complain about specifications for unexported and unused -- values [noCheckUnknown] :: Config -> Bool -- | disable termination check [notermination] :: Config -> Bool -- | automatically construct proofs from axioms [autoproofs] :: Config -> Bool -- | disable warnings output (only show errors) [nowarnings] :: Config -> Bool -- | type all internal variables with true [trustinternals] :: Config -> Bool -- | disable case expand [nocaseexpand] :: Config -> Bool -- | enable strata analysis [strata] :: Config -> Bool -- | disable truing top level types [notruetypes] :: Config -> Bool -- | check totality in definitions [totality] :: Config -> Bool -- | disable prunning unsorted Refinements [noPrune] :: Config -> Bool -- | 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] :: Config -> Bool -- | port at which lhi should listen [port] :: Config -> Int -- | Automatically generate singleton types for data constructors [exactDC] :: Config -> Bool -- | scrape qualifiers from imported specifications [scrapeImports] :: Config -> Bool -- | scrape qualifiers from used, imported specifications [scrapeUsedImports] :: Config -> Bool -- | print eliminate stats [elimStats] :: Config -> Bool class HasConfig t getConfig :: HasConfig t => t -> Config hasOpt :: HasConfig t => t -> (Config -> Bool) -> Bool instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_34Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_33Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_32Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_31Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_30Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_29Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_28Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_27Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_26Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_25Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_24Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_23Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_22Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_21Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_20Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_19Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_18Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_17Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_16Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_15Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_14Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_13Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_12Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_11Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_10Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_9Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_8Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_7Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_6Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_5Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_4Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_3Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_2Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_1Config instance GHC.Generics.Selector Language.Haskell.Liquid.UX.Config.S1_0_0Config instance GHC.Generics.Constructor Language.Haskell.Liquid.UX.Config.C1_0Config instance GHC.Generics.Datatype Language.Haskell.Liquid.UX.Config.D1Config 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 Data.Serialize.Serialize Language.Fixpoint.Types.Config.SMTSolver instance Data.Serialize.Serialize Language.Haskell.Liquid.UX.Config.Config instance Language.Haskell.Liquid.UX.Config.HasConfig Language.Haskell.Liquid.UX.Config.Config -- | 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.Names lenLocSymbol :: Located Symbol module Language.Haskell.Liquid.Prover.Types type LVar = Var () type LVarCtor = VarCtor () type LAxiom = Axiom () type LQuery = Query () data Axiom a Axiom :: Var a -> [LVar] -> Predicate -> Axiom a [axiom_name] :: Axiom a -> Var a [axiom_vars] :: Axiom a -> [LVar] [axiom_body] :: Axiom a -> Predicate data Var a Var :: Symbol -> Sort -> a -> Var a [var_name] :: Var a -> Symbol [var_sort] :: Var a -> Sort [var_info] :: Var a -> a data Ctor a Ctor :: Expr a -> Sort -> [LVar] -> Predicate -> Ctor a [ctor_expr] :: Ctor a -> Expr a [ctor_sort] :: Ctor a -> Sort [ctor_vars] :: Ctor a -> [LVar] [ctor_prop] :: Ctor a -> Predicate data VarCtor a VarCtor :: Var a -> [LVar] -> Predicate -> VarCtor a [vctor_var] :: VarCtor a -> Var a [vctor_vars] :: VarCtor a -> [LVar] [vctor_prop] :: VarCtor a -> Predicate data Expr a EVar :: (Var a) -> Expr a EApp :: (Ctor a) -> [Expr a] -> Expr a newtype Predicate Pred :: Expr -> Predicate [p_pred] :: Predicate -> Expr data Proof a Invalid :: Proof a Proof :: [Instance a] -> Proof a [p_evidence] :: Proof a -> [Instance a] data Instance a Inst :: Axiom a -> [Expr a] -> Predicate -> Instance a [inst_axiom] :: Instance a -> Axiom a [inst_args] :: Instance a -> [Expr a] [inst_pred] :: Instance a -> Predicate data Query a Query :: ![Axiom a] -> ![VarCtor a] -> ![Var a] -> ![LVar] -> !Predicate -> !FilePath -> !Int -> [Predicate] -> Bool -> Query a [q_axioms] :: Query a -> ![Axiom a] [q_ctors] :: Query a -> ![VarCtor a] [q_vars] :: Query a -> ![Var a] [q_env] :: Query a -> ![LVar] [q_goal] :: Query a -> !Predicate [q_fname] :: Query a -> !FilePath [q_depth] :: Query a -> !Int [q_decls] :: Query a -> [Predicate] [q_isHO] :: Query a -> Bool -- | ArgExpr provides for each sort s | a list of expressions of sort s | -- and the list of constroctors that can create an expression of sort s. data ArgExpr a ArgExpr :: Sort -> [Expr a] -> [Ctor a] -> ArgExpr a [arg_sort] :: ArgExpr a -> Sort [arg_exprs] :: ArgExpr a -> [Expr a] [arg_ctors] :: ArgExpr a -> [Ctor a] varCtorToCtor :: VarCtor a -> Ctor a isEVar :: Expr t -> Bool mkExpr :: Expr a -> Expr instance GHC.Classes.Eq (Language.Haskell.Liquid.Prover.Types.Expr a) instance GHC.Classes.Eq (Language.Haskell.Liquid.Prover.Types.Var a) instance GHC.Classes.Eq (Language.Haskell.Liquid.Prover.Types.Ctor a) instance GHC.Base.Monoid Language.Haskell.Liquid.Prover.Types.Predicate instance GHC.Base.Monoid (Language.Haskell.Liquid.Prover.Types.Query a) instance Language.Fixpoint.Types.Refinements.Subable Language.Haskell.Liquid.Prover.Types.Predicate module Language.Haskell.Liquid.Prover.Parser parseQuery :: String -> IO LQuery queryP :: FilePath -> ParsecT String Integer Identity (Query ()) declsP :: Parser [Predicate] declP :: Parser Predicate depthP :: Parser Int goalP :: Parser Predicate ctorP :: Parser LVarCtor ctorAxiomP :: ParsecT String Integer Identity ([LVar], Predicate) bindP :: Parser LVar envP :: Parser LVar predicateP :: Parser Predicate axiomP :: Parser LAxiom argumentsP :: Parser ([LVar]) varP :: Parser LVar module Language.Haskell.Liquid.Prover.Pretty showNum :: Show a => [a] -> [Char] par :: [Char] -> [Char] sep :: [t] -> [[t]] -> [t] instance Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Prover.Types.Var a) instance Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Prover.Types.Expr a) instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Prover.Types.Predicate instance GHC.Show.Show (Language.Haskell.Liquid.Prover.Types.Axiom a) instance GHC.Show.Show (Language.Haskell.Liquid.Prover.Types.Instance a) instance GHC.Show.Show (Language.Haskell.Liquid.Prover.Types.Var a) instance GHC.Show.Show (Language.Haskell.Liquid.Prover.Types.Ctor a) instance GHC.Show.Show (Language.Haskell.Liquid.Prover.Types.VarCtor a) instance GHC.Show.Show (Language.Haskell.Liquid.Prover.Types.Expr a) instance GHC.Show.Show Language.Haskell.Liquid.Prover.Types.Predicate instance GHC.Show.Show (Language.Haskell.Liquid.Prover.Types.Query a) instance GHC.Show.Show (Language.Haskell.Liquid.Prover.Types.Proof a) instance GHC.Show.Show (Language.Haskell.Liquid.Prover.Types.ArgExpr a) module Language.Haskell.Liquid.Prover.Solve type PrEnv = SEnv SortedReft solve :: Query a -> IO (Proof a) notGHCVar :: Show a => a -> Bool iterativeSolve :: PrEnv -> Int -> Context -> [Ctor a] -> [Expr a] -> Expr -> [Axiom a] -> IO (Proof a) type Arguments a = [(Sort, [Expr a])] groupExpressions :: PrEnv -> [Expr a] -> Arguments a placeExpr :: PrEnv -> Arguments a -> Expr a -> Arguments a mergeExpressions :: Arguments a -> Arguments a -> Arguments a placeArg :: [(Sort, [a])] -> (Sort, [a]) -> [(Sort, [a])] findValid :: Context -> [Instance a] -> Expr -> IO (Maybe [Instance a]) minimize :: Context -> [Instance a] -> Expr -> IO [Instance a] bruteSearch :: Context -> [Instance a] -> Expr -> IO (Maybe [Instance a]) filterEquivalentExpressions :: PrEnv -> Context -> [Instance a] -> Arguments a -> Arguments a -> IO (Arguments a) makeEq :: PrEnv -> Expr a -> Expr a -> Maybe (Expr) assertExpressions :: PrEnv -> Context -> (Sort, [Expr a]) -> IO () predCtor :: SEnv SortedReft -> Ctor a -> [Expr] -> Expr makeExpressions :: PrEnv -> Context -> [Instance a] -> [Ctor a] -> Arguments a -> IO (Arguments a) putExpr :: t -> Maybe Sort -> [(Sort, [t])] -> [(Sort, [t])] makeArguments :: [Sort] -> Arguments a -> [[Expr a]] makeCTorArgs :: Ctor a -> Arguments a -> [[Expr a]] applyArguments :: [[a]] -> [[a]] makeArgumnetsExpr :: Int -> [Expr a] -> [[Expr a]] arity :: Ctor a -> Int initExpressions :: [Var a] -> [Expr a] instantiate :: PrEnv -> Arguments a -> Arguments a -> Axiom a -> [Instance a] makeArgs' :: Int -> [Expr a] -> [[Expr a]] duplicateArgs :: t -> t1 -> [t1] makeArgs :: Int -> [Expr a] -> [[Expr a]] axiomInstance :: PrEnv -> Axiom a -> [Expr a] -> Maybe (Instance a) checkExpr :: PrEnv -> Expr a -> Bool mkcheckExpr :: PrEnv -> Expr a -> Expr makeSorts :: Query a -> [Sort] unifiable :: Sort -> Sort -> Bool module Language.Haskell.Liquid.Types.Variance data Variance Invariant :: Variance Bivariant :: Variance Contravariant :: Variance Covariant :: Variance type VarianceInfo = [Variance] instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Variance.C1_3Variance instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Variance.C1_2Variance instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Variance.C1_1Variance instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Variance.C1_0Variance instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.Variance.D1Variance 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 Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Variance.Variance module Language.Haskell.Liquid.Misc (!?) :: [a] -> Int -> Maybe a safeFromJust :: String -> Maybe t -> t fst4 :: (t, t1, t2, t3) -> t snd4 :: (t, t1, t2, t3) -> t1 mapFourth4 :: (t -> t4) -> (t1, t2, t3, t) -> (t1, t2, t3, t4) addFst3 :: t -> (t1, t2) -> (t, t1, t2) addThd3 :: t2 -> (t, t1) -> (t, t1, t2) dropFst3 :: (t, t1, t2) -> (t1, t2) dropThd3 :: (t1, t2, t) -> (t1, t2) replaceN :: (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 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] mapFst :: (t -> t1) -> (t, t2) -> (t1, t2) mapSnd :: (t -> t2) -> (t1, t) -> (t1, t2) 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) 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 -> [[Char]] 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 () (=>>) :: Monad m => m b -> (b -> m a) -> m b firstJust :: (a -> Maybe b) -> [a] -> Maybe b intToString :: Int -> String -- | 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 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 -> !Expr -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [var] :: TError t -> !Doc [exp] :: TError t -> !Expr [msg] :: TError t -> !Doc -- | multiple alias with same name error ErrDupAlias :: !SrcSpan -> !Doc -> !Doc -> ![SrcSpan] -> TError t -- | 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 measure ErrDupMeas :: !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] -- | 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 -- | 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 -> !SrcSpan -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [var] :: TError t -> !Doc [hs] :: TError t -> !Doc [lq] :: 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 -> !Int -> !Doc -> !SrcSpan -> !Int -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [nargs] :: TError t -> !Int [dname] :: TError t -> !Doc [dpos] :: TError t -> !SrcSpan [dargs] :: TError t -> !Int -- | Previously saved error, that carries over after DiffCheck ErrSaved :: !SrcSpan -> !Doc -> TError t -- | haskell type location [pos] :: 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 -- | 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 t -> IO (CtxError t) -- | 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 -- | 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 ppError :: (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc ppError' :: (PPrint a, Show a) => Tidy -> Doc -> Doc -> TError a -> Doc realSrcSpan :: FilePath -> Int -> Int -> Int -> Int -> RealSrcSpan unpackRealSrcSpan :: RealSrcSpan -> (String, Int, Int, Int, Int) instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_27_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_27_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_26_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_26_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_26_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_25_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_25_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_25_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_24_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_24_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_24_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_23_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_23_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_22_4TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_22_3TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_22_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_22_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_22_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_21_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_21_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_21_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_20_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_20_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_19_5TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_19_4TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_19_3TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_19_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_19_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_19_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_18_4TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_18_3TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_18_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_18_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_18_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_17_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_17_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_16_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_16_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_15_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_15_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_15_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_14_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_14_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_14_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_13_3TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_13_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_13_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_13_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_12_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_12_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_12_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_11_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_11_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_11_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_10_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_10_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_10_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_9_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_9_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_9_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_8_3TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_8_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_8_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_8_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_7_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_7_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_7_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_6_3TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_6_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_6_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_6_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_5_3TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_5_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_5_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_5_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_4_3TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_4_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_4_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_4_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_3_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_3_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_3_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_2_4TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_2_3TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_2_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_2_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_2_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_1_4TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_1_3TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_1_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_1_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_1_0TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_0_4TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_0_3TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_0_2TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_0_1TError instance GHC.Generics.Selector Language.Haskell.Liquid.Types.Errors.S1_0_0TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_27TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_26TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_25TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_24TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_23TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_22TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_21TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_20TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_19TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_18TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_17TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_16TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_15TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_14TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_13TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_12TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_11TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_10TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_9TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_8TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_7TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_6TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_5TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_4TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_3TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_2TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_1TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_0TError instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.Errors.D1TError instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_2Oblig instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_1Oblig instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.Errors.C1_0Oblig instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.Errors.D1Oblig 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 Data.Data.Data Language.Haskell.Liquid.Types.Errors.Oblig instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Errors.Oblig instance Language.Fixpoint.Types.PrettyPrint.PPrint Text.Parsec.Error.ParseError instance GHC.Classes.Eq (Language.Haskell.Liquid.Types.Errors.CtxError t) instance GHC.Classes.Ord (Language.Haskell.Liquid.Types.Errors.CtxError t) 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 Control.DeepSeq.NFData Text.Parsec.Error.ParseError 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 SrcLoc.SrcSpan 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 Data.Aeson.Types.Class.ToJSON SrcLoc.RealSrcSpan instance Data.Aeson.Types.Class.FromJSON SrcLoc.RealSrcSpan instance Data.Aeson.Types.Class.ToJSON SrcLoc.SrcSpan instance Data.Aeson.Types.Class.FromJSON SrcLoc.SrcSpan instance (Language.Fixpoint.Types.PrettyPrint.PPrint a, GHC.Show.Show a) => Data.Aeson.Types.Class.ToJSON (Language.Haskell.Liquid.Types.Errors.TError a) instance Data.Aeson.Types.Class.FromJSON (Language.Haskell.Liquid.Types.Errors.TError a) -- | Utility functions for constructing Core syntax, principally for -- desugaring module Language.Haskell.Liquid.Desugar710.DsUtils data EquationInfo :: * EqnInfo :: [Pat Id] -> MatchResult -> EquationInfo [eqn_pats] :: EquationInfo -> [Pat Id] [eqn_rhs] :: EquationInfo -> MatchResult firstPat :: EquationInfo -> Pat Id shiftEqns :: [EquationInfo] -> [EquationInfo] data MatchResult :: * MatchResult :: CanItFail -> (CoreExpr -> DsM CoreExpr) -> MatchResult data CanItFail :: * CanFail :: CanItFail CantFail :: CanItFail data CaseAlt a MkCaseAlt :: a -> [CoreBndr] -> HsWrapper -> MatchResult -> CaseAlt a [alt_pat] :: CaseAlt a -> a [alt_bndrs] :: CaseAlt a -> [CoreBndr] [alt_wrapper] :: CaseAlt a -> HsWrapper [alt_result] :: CaseAlt a -> MatchResult cantFailMatchResult :: CoreExpr -> MatchResult alwaysFailMatchResult :: MatchResult extractMatchResult :: MatchResult -> CoreExpr -> DsM CoreExpr combineMatchResults :: MatchResult -> MatchResult -> MatchResult adjustMatchResult :: DsWrapper -> MatchResult -> MatchResult adjustMatchResultDs :: (CoreExpr -> DsM CoreExpr) -> MatchResult -> MatchResult mkCoLetMatchResult :: CoreBind -> MatchResult -> MatchResult mkViewMatchResult :: Id -> CoreExpr -> Id -> MatchResult -> MatchResult mkGuardedMatchResult :: CoreExpr -> MatchResult -> MatchResult matchCanFail :: MatchResult -> Bool mkEvalMatchResult :: Id -> Type -> MatchResult -> MatchResult mkCoPrimCaseMatchResult :: Id -> Type -> [(Literal, MatchResult)] -> MatchResult mkCoAlgCaseMatchResult :: DynFlags -> Id -> Type -> [CaseAlt DataCon] -> MatchResult mkCoSynCaseMatchResult :: Id -> Type -> CaseAlt PatSyn -> MatchResult wrapBind :: Var -> Var -> CoreExpr -> CoreExpr wrapBinds :: [(Var, Var)] -> CoreExpr -> CoreExpr mkErrorAppDs :: Id -> Type -> SDoc -> DsM CoreExpr mkCoreAppDs :: CoreExpr -> CoreExpr -> CoreExpr mkCoreAppsDs :: CoreExpr -> [CoreExpr] -> CoreExpr mkCastDs :: CoreExpr -> Coercion -> CoreExpr seqVar :: Var -> CoreExpr -> CoreExpr mkLHsVarPatTup :: [Id] -> LPat Id mkLHsPatTup :: [LPat Id] -> LPat Id mkVanillaTuplePat :: [OutPat Id] -> Boxity -> Pat Id mkBigLHsVarTup :: [Id] -> LHsExpr Id mkBigLHsTup :: [LHsExpr Id] -> LHsExpr Id mkBigLHsVarPatTup :: [Id] -> LPat Id mkBigLHsPatTup :: [LPat Id] -> LPat Id mkSelectorBinds :: [[Tickish Id]] -> LPat Id -> CoreExpr -> DsM [(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 module Language.Haskell.Liquid.Desugar710.MatchLit dsLit :: HsLit -> DsM CoreExpr dsOverLit :: HsOverLit Id -> DsM CoreExpr hsLitKey :: DynFlags -> HsLit -> Literal hsOverLitKey :: OutputableBndr a => HsOverLit a -> Bool -> Literal tidyLitPat :: HsLit -> Pat Id tidyNPat :: (HsLit -> Pat Id) -> HsOverLit Id -> Maybe (SyntaxExpr Id) -> SyntaxExpr Id -> Pat Id matchLiterals :: [Id] -> Type -> [[EquationInfo]] -> DsM MatchResult matchNPlusKPats :: [Id] -> Type -> [EquationInfo] -> DsM MatchResult matchNPats :: [Id] -> Type -> [EquationInfo] -> DsM MatchResult warnAboutIdentities :: DynFlags -> CoreExpr -> Type -> DsM () warnAboutEmptyEnumerations :: DynFlags -> LHsExpr Id -> Maybe (LHsExpr Id) -> LHsExpr Id -> DsM () module Language.Haskell.Liquid.Desugar710.Check check :: [EquationInfo] -> ([ExhaustivePat], [EquationInfo]) type ExhaustivePat = ([WarningPat], [(Name, [HsLit])]) module Language.Haskell.Liquid.Desugar710.DsGRHSs dsGuarded :: GRHSs Id (LHsExpr Id) -> Type -> DsM CoreExpr dsGRHSs :: HsMatchContext Name -> [Pat Id] -> GRHSs Id (LHsExpr Id) -> Type -> DsM MatchResult dsGRHS :: HsMatchContext Name -> Type -> LGRHS Id (LHsExpr Id) -> DsM MatchResult module Language.Haskell.Liquid.Desugar710.DsBinds dsTopLHsBinds :: LHsBinds Id -> DsM (OrdList (Id, CoreExpr)) dsLHsBinds :: LHsBinds Id -> DsM [(Id, CoreExpr)] decomposeRuleLhs :: [Var] -> CoreExpr -> Either SDoc ([Var], Id, [CoreExpr]) dsSpec :: Maybe CoreExpr -> Located TcSpecPrag -> DsM (Maybe (OrdList (Id, CoreExpr), CoreRule)) dsHsWrapper :: HsWrapper -> CoreExpr -> DsM CoreExpr dsTcEvBinds :: TcEvBinds -> DsM [CoreBind] dsEvBinds :: Bag EvBind -> DsM [CoreBind] module Language.Haskell.Liquid.Desugar710.MatchCon matchConFamily :: [Id] -> Type -> [[EquationInfo]] -> DsM MatchResult matchPatSyn :: [Id] -> Type -> [EquationInfo] -> DsM MatchResult module Language.Haskell.Liquid.Desugar710.Match match :: [Id] -> Type -> [EquationInfo] -> DsM MatchResult matchEquations :: HsMatchContext Name -> [Id] -> [EquationInfo] -> Type -> DsM CoreExpr matchWrapper :: HsMatchContext Name -> MatchGroup Id (LHsExpr Id) -> DsM ([Id], CoreExpr) matchSimply :: CoreExpr -> HsMatchContext Name -> LPat Id -> CoreExpr -> CoreExpr -> DsM CoreExpr matchSinglePat :: CoreExpr -> HsMatchContext Name -> LPat Id -> Type -> MatchResult -> DsM MatchResult module Language.Haskell.Liquid.Desugar710.DsArrows dsProcExpr :: LPat Id -> LHsCmdTop Id -> DsM CoreExpr module Language.Haskell.Liquid.Desugar710.DsListComp dsListComp :: [ExprLStmt Id] -> Type -> DsM CoreExpr dsPArrComp :: [ExprStmt Id] -> DsM CoreExpr dsMonadComp :: [ExprLStmt Id] -> DsM CoreExpr module Language.Haskell.Liquid.Desugar710.DsExpr dsExpr :: HsExpr Id -> DsM CoreExpr dsLExpr :: LHsExpr Id -> DsM CoreExpr dsLocalBinds :: HsLocalBinds Id -> CoreExpr -> DsM CoreExpr dsValBinds :: HsValBinds Id -> CoreExpr -> DsM CoreExpr dsLit :: HsLit -> DsM CoreExpr module Language.Haskell.Liquid.Desugar710.Desugar -- | Main entry point to the desugarer. deSugarWithLoc :: HscEnv -> ModLocation -> TcGblEnv -> IO (Messages, Maybe ModGuts) -- | Main entry point to the desugarer. deSugar :: HscEnv -> ModLocation -> TcGblEnv -> IO (Messages, Maybe ModGuts) deSugarExpr :: HscEnv -> LHsExpr Id -> IO (Messages, Maybe CoreExpr) -- | 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.Desugar710.HscMain -- | Convert a typechecked module to Core hscDesugarWithLoc :: HscEnv -> ModSummary -> TcGblEnv -> IO ModGuts module Language.Haskell.Liquid.Desugar710.DsMeta dsBracket :: HsBracket Name -> [PendingTcSplice] -> DsM CoreExpr templateHaskellNames :: [Name] qTyConName :: Name nameTyConName :: Name liftName :: Name liftStringName :: Name expQTyConName :: Name patQTyConName :: Name decQTyConName :: Name decsQTyConName :: Name typeQTyConName :: Name decTyConName :: Name typeTyConName :: Name mkNameG_dName :: Name mkNameG_vName :: Name mkNameG_tcName :: Name quoteExpName :: Name quotePatName :: Name quoteDecName :: Name quoteTypeName :: Name tExpTyConName :: Name tExpDataConName :: Name unTypeName :: Name unTypeQName :: Name unsafeTExpCoerceName :: Name -- | 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 data MGIModGuts MI :: !CoreProgram -> !Module -> !Dependencies -> !ImportedMods -> !GlobalRdrEnv -> ![TyCon] -> ![FamInst] -> !NameSet -> !(Maybe [ClsInst]) -> MGIModGuts [mgi_binds] :: MGIModGuts -> !CoreProgram [mgi_module] :: MGIModGuts -> !Module [mgi_deps] :: MGIModGuts -> !Dependencies [mgi_dir_imps] :: MGIModGuts -> !ImportedMods [mgi_rdr_env] :: MGIModGuts -> !GlobalRdrEnv [mgi_tcs] :: MGIModGuts -> ![TyCon] [mgi_fam_insts] :: MGIModGuts -> ![FamInst] [mgi_exports] :: MGIModGuts -> !NameSet [mgi_cls_inst] :: MGIModGuts -> !(Maybe [ClsInst]) miModGuts :: Maybe [ClsInst] -> ModGuts -> MGIModGuts mgi_namestring :: MGIModGuts -> String -- | Encoding and Decoding Location -- -------------------------------------------- srcSpanTick :: Module -> SrcSpan -> Tickish a tickSrcSpan :: Outputable a => Tickish a -> SrcSpan 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 :: Var -> [Char] tracePpr :: Outputable a => [Char] -> a -> a pprShow :: Show a => a -> SDoc tidyCBs :: [Bind b] -> [Bind b] unTick :: Bind b -> Bind b unTickExpr :: Expr b -> Expr b isFractionalClass :: Class -> Bool isDataConId :: Id -> Bool getDataConVarUnique :: Var -> Unique newtype Loc L :: (Int, Int) -> Loc toFixSDoc :: Fixpoint a => a -> Doc sDocDoc :: SDoc -> Doc pprDoc :: Outputable a => a -> Doc showPpr :: Outputable a => a -> String showSDoc :: SDoc -> String showSDocDump :: SDoc -> String typeUniqueString :: Outputable a => a -> String 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 collectArguments :: Int -> CoreExpr -> [Var] collectValBinders' :: Expr Var -> ([Var], Expr Var) ignoreLetBinds :: Expr t -> Expr t isDictionaryExpression :: Expr Id -> Maybe Id realTcArity :: 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 symbolTyConWithKind :: Kind -> Char -> Int -> Symbol -> TyCon symbolTyCon :: Char -> Int -> Symbol -> TyCon symbolTyVar :: Symbol -> TyVar varSymbol :: Var -> Symbol qualifiedNameSymbol :: Name -> Symbol fastStringText :: FastString -> Text tyConTyVarsDef :: TyCon -> [TyVar] gHC_VERSION :: String symbolFastString :: Symbol -> FastString desugarModule :: TypecheckedModule -> Ghc DesugaredModule type Prec = TyPrec lintCoreBindings :: [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc) synTyConRhs_maybe :: TyCon -> Maybe Type tcRnLookupRdrName :: HscEnv -> Located RdrName -> IO (Messages, Maybe [Name]) -- | Manipulating Symbols ---------------------------------------------- dropModuleNames :: Symbol -> Symbol -- | Manipulating Symbols ---------------------------------------------- takeModuleNames :: Symbol -> Symbol -- | Manipulating Symbols ---------------------------------------------- dropModuleUnique :: Symbol -> Symbol sepModNames :: IsString a => a sepUnique :: IsString a => a 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 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 Data.Hashable.Class.Hashable SrcLoc.SrcSpan instance Outputable.Outputable a => Outputable.Outputable (Data.HashSet.HashSet a) instance Language.Fixpoint.Types.Names.Symbolic FastString.FastString instance Language.Fixpoint.Types.Names.Symbolic TyCon.TyCon 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 TypeRep.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 SrcLoc.SrcSpan instance Control.DeepSeq.NFData TyCon.TyCon instance Control.DeepSeq.NFData TypeRep.Type instance Control.DeepSeq.NFData Var.Var 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.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 -- | 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 -- | 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 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 module Language.Haskell.Liquid.GHC.Play class Subable a sub :: Subable a => HashMap CoreBndr CoreExpr -> a -> a subTy :: Subable a => HashMap TyVar Type -> a -> a subVar :: Expr t -> Id substTysWith :: HashMap Var Type -> Type -> Type instance Language.Haskell.Liquid.GHC.Play.Subable CoreSyn.CoreExpr instance Language.Haskell.Liquid.GHC.Play.Subable Coercion.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 TypeRep.Type module Language.Haskell.Liquid.Transforms.Rec transformRecExpr :: CoreProgram -> CoreProgram transformScope :: [Bind Id] -> [Bind 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 :: Bool -> HscEnv -> MGIModGuts -> 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 -- | 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 -> [String] -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Maybe Int -> Int -> Int -> Int -> Maybe SMTSolver -> Bool -> Bool -> Bool -> [String] -> [String] -> Bool -> Int -> Bool -> Bool -> Bool -> Bool -> Config -- | source files to check [files] :: Config -> [FilePath] -- | path to directory for including specs [idirs] :: Config -> [FilePath] -- | new liquid-fixpoint sort check [newcheck] :: Config -> Bool -- | check subset of binders modified (+ dependencies) since last check [diffcheck] :: Config -> Bool -- | uninterpreted integer multiplication and division [linear] :: Config -> Bool -- | allow higher order binders into the logic [higherorder] :: Config -> Bool -- | check all binders (overrides diffcheck) [fullcheck] :: Config -> Bool -- | save fixpoint query [saveQuery] :: Config -> Bool -- | set of binders to check [binders] :: Config -> [String] -- | whether to complain about specifications for unexported and unused -- values [noCheckUnknown] :: Config -> Bool -- | disable termination check [notermination] :: Config -> Bool -- | automatically construct proofs from axioms [autoproofs] :: Config -> Bool -- | disable warnings output (only show errors) [nowarnings] :: Config -> Bool -- | type all internal variables with true [trustinternals] :: Config -> Bool -- | disable case expand [nocaseexpand] :: Config -> Bool -- | enable strata analysis [strata] :: Config -> Bool -- | disable truing top level types [notruetypes] :: Config -> Bool -- | check totality in definitions [totality] :: Config -> Bool -- | disable prunning unsorted Refinements [noPrune] :: Config -> Bool -- | 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] :: Config -> Bool -- | port at which lhi should listen [port] :: Config -> Int -- | Automatically generate singleton types for data constructors [exactDC] :: Config -> Bool -- | scrape qualifiers from imported specifications [scrapeImports] :: Config -> Bool -- | scrape qualifiers from used, imported specifications [scrapeUsedImports] :: Config -> Bool -- | print eliminate stats [elimStats] :: Config -> Bool class HasConfig t getConfig :: HasConfig t => t -> Config hasOpt :: HasConfig t => t -> (Config -> Bool) -> Bool -- | GHC Information : Code & Spec ------------------------------ data GhcInfo GI :: !FilePath -> !HscEnv -> ![CoreBind] -> ![Var] -> ![Var] -> ![Var] -> ![Var] -> ![FilePath] -> ![String] -> ![FilePath] -> !GhcSpec -> GhcInfo [target] :: GhcInfo -> !FilePath [env] :: GhcInfo -> !HscEnv [cbs] :: GhcInfo -> ![CoreBind] [derVars] :: GhcInfo -> ![Var] [impVars] :: GhcInfo -> ![Var] [defVars] :: GhcInfo -> ![Var] [useVars] :: GhcInfo -> ![Var] [hqFiles] :: GhcInfo -> ![FilePath] [imports] :: GhcInfo -> ![String] [includes] :: GhcInfo -> ![FilePath] [spec] :: GhcInfo -> !GhcSpec -- | The following is the overall type for specifications obtained -- from parsing the target source and dependent libraries data GhcSpec SP :: ![(Var, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Symbol, Located SpecType)] -> ![Located SpecType] -> ![(Located SpecType, Located SpecType)] -> ![(DataCon, DataConP)] -> ![(TyCon, TyConP)] -> ![(Symbol, Var)] -> TCEmb TyCon -> ![Qualifier] -> ![Var] -> ![(Var, [Int])] -> ![(Var, [Expr])] -> !(HashSet Var) -> !(HashSet Var) -> !(HashSet TyCon) -> !Config -> !NameSet -> [Measure SpecType DataCon] -> HashMap TyCon RTyCon -> DEnv Var SpecType -> [HAxiom] -> LogicMap -> Maybe Type -> GhcSpec -- | Asserted Reftypes eg. see include/Prelude.spec [tySigs] :: GhcSpec -> ![(Var, Located SpecType)] -- | Assumed Reftypes [asmSigs] :: GhcSpec -> ![(Var, Located SpecType)] -- | Auto generated Signatures [inSigs] :: GhcSpec -> ![(Var, Located SpecType)] -- | Data Constructor Measure Sigs eg. (:) :: a -> xs:[a] -> {v: Int -- | v = 1 + len(xs) } [ctors] :: GhcSpec -> ![(Var, Located SpecType)] -- | Measure Types eg. len :: [a] -> Int [meas] :: GhcSpec -> ![(Symbol, Located SpecType)] -- | Data Type Invariants eg. forall a. {v: [a] | len(v) >= 0} [invariants] :: GhcSpec -> ![Located SpecType] -- | Data Type Invariant Aliases [ialiases] :: GhcSpec -> ![(Located SpecType, Located SpecType)] -- | Predicated Data-Constructors e.g. see testsposMap.hs [dconsP] :: GhcSpec -> ![(DataCon, DataConP)] -- | Predicated Type-Constructors eg. see testsposMap.hs [tconsP] :: GhcSpec -> ![(TyCon, TyConP)] -- | List of Symbol free in spec and corresponding GHC var eg. -- (Cons, Cons#7uz) from testsposex1.hs [freeSyms] :: GhcSpec -> ![(Symbol, Var)] -- | How to embed GHC Tycons into fixpoint sorts e.g. "embed Set as -- Set_set" from includeDataSet.spec [tcEmbeds] :: GhcSpec -> TCEmb TyCon -- | Qualifiers in Source/Spec files e.g testsposqualTest.hs [qualifiers] :: GhcSpec -> ![Qualifier] -- | Top-level Binders To Verify (empty means ALL binders) [tgtVars] :: GhcSpec -> ![Var] -- | Lexicographically ordered size witnesses for termination [decr] :: GhcSpec -> ![(Var, [Int])] -- | Lexicographically ordered expressions for termination [texprs] :: GhcSpec -> ![(Var, [Expr])] -- | Variables that should be checked in the environment they are used [lvars] :: GhcSpec -> !(HashSet Var) -- | Binders to IGNORE during termination checking [lazy] :: GhcSpec -> !(HashSet Var) -- | Binders to IGNORE during termination checking [autosize] :: GhcSpec -> !(HashSet TyCon) -- | Configuration Options [config] :: GhcSpec -> !Config -- | Names exported by the module being verified [exports] :: GhcSpec -> !NameSet [measures] :: GhcSpec -> [Measure SpecType DataCon] [tyconEnv] :: GhcSpec -> HashMap TyCon RTyCon -- | Dictionary Environment [dicts] :: GhcSpec -> DEnv Var SpecType [axioms] :: GhcSpec -> [HAxiom] [logicMap] :: GhcSpec -> LogicMap [proofType] :: GhcSpec -> Maybe Type -- | Which Top-Level Binders Should be Verified data TargetVars AllVars :: TargetVars Only :: ![Var] -> TargetVars data Located a :: * -> * Loc :: SrictNotUnpackedSourcePos -> SrictNotUnpackedSourcePos -> a -> Located a -- | Start Position [loc] :: Located a -> SrictNotUnpackedSourcePos -- | End Position [locE] :: Located a -> SrictNotUnpackedSourcePos [val] :: Located a -> a dummyLoc :: a -> Located a -- | Located Symbols ----------------------------------------------------- type LocSymbol = Located Symbol type LocText = Located Text dummyName :: Symbol isDummy :: Symbolic a => a -> Bool data RTyCon RTyCon :: TyCon -> ![RPVar] -> !TyConInfo -> RTyCon -- | Co- and Contra-variance for TyCon -------------------------------- -- -- Indexes start from 0 and type or predicate arguments can be both -- covariant and contravaariant e.g., for the below Foo dataType -- -- data Foo a b c d :: 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 (Symbol -> Expr)) -> TyConInfo -- | variance info for type variables [varianceTyArgs] :: TyConInfo -> !VarianceInfo -- | variance info for predicate variables [variancePsArgs] :: TyConInfo -> !VarianceInfo -- | logical function that computes the size of the structure [sizeFunction] :: TyConInfo -> !(Maybe (Symbol -> Expr)) defaultTyConInfo :: TyConInfo rTyConPVs :: RTyCon -> [RPVar] rTyConPropVs :: RTyCon -> [PVar RSort] -- | Accessors for RTyCon isClassRTyCon :: RTyCon -> Bool isClassType :: TyConable c => RType c t t1 -> Bool isEqType :: TyConable c => RType c t t1 -> Bool data RType c tv r RVar :: !tv -> !r -> RType c tv r [rt_var] :: RType c tv r -> !tv [rt_reft] :: RType c tv r -> !r RFun :: !Symbol -> !(RType c tv r) -> !(RType c tv r) -> !r -> RType c tv r [rt_bind] :: RType c tv r -> !Symbol [rt_in] :: RType c tv r -> !(RType c tv r) [rt_out] :: RType c tv r -> !(RType c tv r) [rt_reft] :: RType c tv r -> !r RAllT :: !tv -> !(RType c tv r) -> RType c tv r [rt_tvbind] :: RType c tv r -> !tv [rt_ty] :: RType c tv r -> !(RType c tv r) RAllP :: !(PVar (RType c tv ())) -> !(RType c tv r) -> RType c tv r [rt_pvbind] :: RType c tv r -> !(PVar (RType c tv ())) [rt_ty] :: RType c tv r -> !(RType c tv r) RAllS :: !(Symbol) -> !(RType c tv r) -> RType c tv r [rt_sbind] :: RType c tv r -> !(Symbol) [rt_ty] :: RType c tv r -> !(RType c tv r) RApp :: !c -> ![RType c tv r] -> ![RTProp c tv r] -> !r -> RType c tv r [rt_tycon] :: RType c tv r -> !c [rt_args] :: RType c tv r -> ![RType c tv r] [rt_pargs] :: RType c tv r -> ![RTProp c tv r] [rt_reft] :: RType c tv r -> !r RAllE :: !Symbol -> !(RType c tv r) -> !(RType c tv r) -> RType c tv r [rt_bind] :: RType c tv r -> !Symbol [rt_allarg] :: RType c tv r -> !(RType c tv r) [rt_ty] :: RType c tv r -> !(RType c tv r) REx :: !Symbol -> !(RType c tv r) -> !(RType c tv r) -> RType c tv r [rt_bind] :: RType c tv r -> !Symbol [rt_exarg] :: RType c tv r -> !(RType c tv r) [rt_ty] :: RType c tv r -> !(RType c tv r) -- | For expression arguments to type aliases see 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 tv ty RTA :: Symbol -> [tv] -> [tv] -> ty -> SourcePos -> SourcePos -> RTAlias tv ty [rtName] :: RTAlias tv ty -> Symbol [rtTArgs] :: RTAlias tv ty -> [tv] [rtVArgs] :: RTAlias tv ty -> [tv] [rtBody] :: RTAlias tv ty -> ty [rtPos] :: RTAlias tv ty -> SourcePos [rtPosE] :: RTAlias tv ty -> SourcePos data HSeg t HBind :: !Symbol -> t -> HSeg t [hs_addr] :: HSeg t -> !Symbol [hs_val] :: HSeg t -> t HVar :: UsedPVar -> HSeg t -- | A 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 where isClass = const False isEqual = const False isNumCls = const False isFracCls = const False isFun :: TyConable c => c -> Bool isList :: TyConable c => c -> Bool isTuple :: TyConable c => c -> Bool ppTycon :: TyConable c => c -> Doc isClass :: TyConable c => c -> Bool isEqual :: TyConable c => c -> Bool isNumCls :: TyConable c => c -> Bool isFracCls :: TyConable c => c -> Bool class (TyConable c, Eq c, Eq tv, Hashable tv, Reftable r, PPrint r) => RefTypable c tv r ppRType :: RefTypable c tv r => Prec -> RType c tv r -> Doc class SubsTy tv ty a subt :: SubsTy tv ty a => (tv, ty) -> a -> a -- | Abstract Predicate Variables ---------------------------------- data PVar t PV :: !Symbol -> !(PVKind t) -> !Symbol -> ![(t, Symbol, Expr)] -> PVar t [pname] :: PVar t -> !Symbol [ptype] :: PVar t -> !(PVKind t) [parg] :: PVar t -> !Symbol [pargs] :: PVar t -> ![(t, Symbol, Expr)] isPropPV :: PVar t -> Bool pvType :: PVar t -> t data PVKind t PVProp :: t -> PVKind t PVHProp :: PVKind t newtype Predicate Pr :: [UsedPVar] -> Predicate data UReft r MkUReft :: !r -> !Predicate -> !Strata -> UReft r [ur_reft] :: UReft r -> !r [ur_pred] :: UReft r -> !Predicate [ur_strata] :: UReft r -> !Strata -- | Values Related to Specifications ------------------------------------ -- -- Data type refinements data DataDecl D :: LocSymbol -> [Symbol] -> [PVar BSort] -> [Symbol] -> [(LocSymbol, [(Symbol, BareType)])] -> !SourcePos -> (Maybe (Symbol -> Expr)) -> DataDecl -- | Type Constructor Name [tycName] :: DataDecl -> LocSymbol -- | Tyvar Parameters [tycTyVars] :: DataDecl -> [Symbol] -- | PVar Parameters [tycPVars] :: DataDecl -> [PVar BSort] -- | PLabel Parameters [tycTyLabs] :: DataDecl -> [Symbol] -- | [tycDCons] :: DataDecl -> [(LocSymbol, [(Symbol, BareType)])] -- | Source Position [tycSrcPos] :: DataDecl -> !SourcePos -- | Measure that should decrease in recursive calls [tycSFun] :: DataDecl -> (Maybe (Symbol -> Expr)) data DataConP DataConP :: !SourcePos -> ![RTyVar] -> ![PVar RSort] -> ![Symbol] -> ![SpecType] -> ![(Symbol, SpecType)] -> !SpecType -> !SourcePos -> DataConP [dc_loc] :: DataConP -> !SourcePos [freeTyVars] :: DataConP -> ![RTyVar] [freePred] :: DataConP -> ![PVar RSort] [freeLabels] :: DataConP -> ![Symbol] [tyConsts] :: DataConP -> ![SpecType] [tyArgs] :: DataConP -> ![(Symbol, SpecType)] [tyRes] :: DataConP -> !SpecType [dc_locE] :: DataConP -> !SourcePos data TyConP TyConP :: ![RTyVar] -> ![PVar RSort] -> ![Symbol] -> !VarianceInfo -> !VarianceInfo -> !(Maybe (Symbol -> Expr)) -> TyConP [freeTyVarsTy] :: TyConP -> ![RTyVar] [freePredTy] :: TyConP -> ![PVar RSort] [freeLabelTy] :: TyConP -> ![Symbol] [varianceTs] :: TyConP -> !VarianceInfo [variancePs] :: TyConP -> !VarianceInfo [sizeFun] :: TyConP -> !(Maybe (Symbol -> Expr)) type RRType = RType RTyCon RTyVar type BRType = RType LocSymbol Symbol type RRProp r = Ref RSort (RRType r) type BSort = BRType () type BPVar = PVar BSort type BareType = BRType RReft type PrType = RRType Predicate type SpecType = RRType RReft type SpecProp = RRProp RReft type RSort = RRType () type UsedPVar = PVar () type RPVar = PVar RSort type RReft = UReft Reft -- | 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 :: [tv] -> [PVar (RType c tv ())] -> [Symbol] -> [Symbol] -> [r] -> [RType c tv r] -> (RType c tv r) -> RTypeRep c tv r [ty_vars] :: RTypeRep c tv r -> [tv] [ty_preds] :: RTypeRep c tv r -> [PVar (RType c tv ())] [ty_labels] :: RTypeRep c tv r -> [Symbol] [ty_binds] :: RTypeRep c tv r -> [Symbol] [ty_refts] :: RTypeRep c tv r -> [r] [ty_args] :: RTypeRep c tv r -> [RType c tv r] [ty_res] :: RTypeRep c tv r -> (RType c tv r) fromRTypeRep :: RTypeRep c tv r -> RType c tv r toRTypeRep :: RType c tv r -> RTypeRep c tv r mkArrow :: (Foldable t, Foldable t1, Foldable t2, Foldable t3) => t tv -> t1 (PVar (RType c tv ())) -> t2 Symbol -> t3 (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 tv -> t1 (PVar (RType c tv ())) -> t2 Symbol -> RType c tv r -> RType c tv r bkUniv :: RType t1 a t2 -> ([a], [PVar (RType t1 a ())], [Symbol], RType t1 a t2) bkClass :: TyConable c => RType c tv r -> ([(c, [RType c tv r])], RType c tv r) rFun :: Monoid r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r rCls :: Monoid r => TyCon -> [RType RTyCon tv r] -> RType RTyCon tv r rRCls :: Monoid r => c -> [RType c tv r] -> RType c tv r pvars :: Predicate -> [UsedPVar] pappSym :: Show a => a -> Symbol pApp :: Symbol -> [Expr] -> 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) => (c -> [RType c tv r] -> [(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) => (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) 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 -- | 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] -> ![UserError] -> !(AnnInfo a) -> !(AnnInfo a) -> ![SrcSpan] -> ErrorResult -> Output a [o_vars] :: Output a -> Maybe [String] [o_errors] :: Output a -> ![UserError] [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 t t1 a -> Maybe a -- | 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 data ModName ModName :: !ModType -> !ModuleName -> ModName data ModType Target :: ModType SrcImport :: ModType SpecImport :: ModType isSrcImport :: ModName -> Bool isSpecImport :: ModName -> Bool getModName :: ModName -> ModuleName getModString :: ModName -> String data RTEnv RTE :: HashMap Symbol (RTAlias RTyVar SpecType) -> HashMap Symbol (RTAlias Symbol 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) -> Cinfo [ci_loc] :: Cinfo -> !SrcSpan [ci_err] :: Cinfo -> !(Maybe Error) data Measure ty ctor M :: LocSymbol -> ty -> [Def ty ctor] -> Measure ty ctor [name] :: Measure ty ctor -> LocSymbol [sort] :: Measure ty ctor -> ty [eqns] :: Measure ty ctor -> [Def ty ctor] data CMeasure ty CM :: LocSymbol -> ty -> CMeasure ty [cName] :: CMeasure ty -> LocSymbol [cSort] :: CMeasure ty -> ty data Def ty ctor Def :: LocSymbol -> [(Symbol, ty)] -> ctor -> Maybe ty -> [(Symbol, Maybe ty)] -> Body -> Def ty ctor [measure] :: Def ty ctor -> LocSymbol [dparams] :: Def ty ctor -> [(Symbol, ty)] [ctor] :: Def ty ctor -> ctor [dsort] :: Def ty ctor -> Maybe ty [binds] :: Def ty ctor -> [(Symbol, Maybe ty)] [body] :: Def ty ctor -> Body data Body -- | Measure Refinement: {v | v = e } E :: Expr -> Body -- | Measure Refinement: {v | (? v) = 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 :: LocSymbol -> [ty] -> [Symbol] -> [(LocSymbol, ty)] -> RClass ty [rcName] :: RClass ty -> LocSymbol [rcSupers] :: RClass ty -> [ty] [rcTyVars] :: RClass ty -> [Symbol] [rcMethods] :: RClass ty -> [(LocSymbol, ty)] -- | KVar Profile -- -------------------------------------------------------------- data KVKind RecBindE :: KVKind NonRecBindE :: KVKind TypeInstE :: KVKind PredInstE :: KVKind LamE :: KVKind CaseE :: KVKind LetE :: KVKind data KVProf emptyKVProf :: KVProf updKVProf :: KVKind -> 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 Symbol -> LogicMap [logic_map] :: LogicMap -> HashMap Symbol LMap [axiom_map] :: LogicMap -> HashMap Var Symbol toLogicMap :: [(Symbol, [Symbol], Expr)] -> LogicMap eAppWithMap :: LogicMap -> Located Symbol -> [Expr] -> Expr -> Expr data LMap LMap :: Symbol -> [Symbol] -> Expr -> LMap [lvar] :: LMap -> Symbol [largs] :: LMap -> [Symbol] [lexpr] :: LMap -> Expr type RDEnv = DEnv Var SpecType newtype DEnv x ty DEnv :: (HashMap x (HashMap Symbol ty)) -> DEnv x ty -- | Refined Instances --------------------------------------------------- data RInstance t RI :: LocSymbol -> t -> [(LocSymbol, t)] -> RInstance t [riclass] :: RInstance t -> LocSymbol [ritype] :: RInstance t -> t [risigs] :: RInstance t -> [(LocSymbol, t)] class Reftable r => UReftable r where ofUReft (MkUReft r _ _) = ofReft r ofUReft :: UReftable r => UReft Reft -> r liquidBegin :: String liquidEnd :: String -- | Values Related to Specifications ------------------------------------ data Axiom b s e Axiom :: (Var, Maybe DataCon) -> [b] -> [s] -> e -> e -> Axiom b s e [aname] :: Axiom b s e -> (Var, Maybe DataCon) [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 LAxiom = Axiom Symbol Sort Expr instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_3MSpec instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_2MSpec instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_1MSpec instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_0MSpec instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0MSpec instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1MSpec instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0KVProf instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1KVProf instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_6KVKind instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_5KVKind instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_4KVKind instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_3KVKind instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_2KVKind instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_1KVKind instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0KVKind instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1KVKind instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_5Output instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_4Output instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_3Output instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_2Output instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_1Output instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_0Output instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0Output instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1Output instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_3Annot instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_2Annot instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_1Annot instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0Annot instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1Annot instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0AnnInfo instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1AnnInfo instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_1CMeasure instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_0CMeasure instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0CMeasure instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1CMeasure 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 ty, Data.Data.Data ctor) => 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.Enum.Enum 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.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 Data.Bifunctor.Bifunctor Language.Haskell.Liquid.Types.Measure instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Body instance Language.Fixpoint.Types.PrettyPrint.PPrint a => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Def t a) 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.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.Fixpoint.Types.Refinements.Subable (Language.Haskell.Liquid.Types.Measure ty ctor) instance Language.Fixpoint.Types.Refinements.Subable (Language.Haskell.Liquid.Types.Def ty ctor) instance Language.Fixpoint.Types.Refinements.Subable Language.Haskell.Liquid.Types.Body 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 Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.Annot a) instance GHC.Base.Monoid (Language.Haskell.Liquid.Types.Output a) 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 Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.KVProf instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.KVProf instance Language.Fixpoint.Types.Names.Symbolic DataCon.DataCon instance Language.Fixpoint.Types.PrettyPrint.PPrint DataCon.DataCon instance GHC.Show.Show DataCon.DataCon 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.RTyVar 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.Bifunctor.Bifunctor Language.Haskell.Liquid.Types.Def instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_2Measure instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_1Measure instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_0Measure instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0Measure instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1Measure instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_5Def instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_4Def instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_3Def instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_2Def instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_1Def instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_0Def instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0Def instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1Def instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_2Body instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_1Body instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0Body instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1Body instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_1Cinfo instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_0Cinfo instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0Cinfo instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1Cinfo instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_7DataConP instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_6DataConP instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_5DataConP instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_4DataConP instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_3DataConP instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_2DataConP instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_1DataConP instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_0DataConP instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0DataConP instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1DataConP instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_2UReft instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_1UReft instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_0UReft instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0UReft instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1UReft instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_3Stratum instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_2Stratum instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_1Stratum instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0Stratum instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1Stratum instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_5TyConP instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_4TyConP instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_3TyConP instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_2TyConP instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_1TyConP instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_0TyConP instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0TyConP instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1TyConP instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_2RTyCon instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_1RTyCon instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_0RTyCon instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0RTyCon instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1RTyCon instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0World instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1World instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_1HSeg instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_0HSeg instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_1HSeg instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0HSeg instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1HSeg instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_10_3RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_10_2RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_10_1RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_10_0RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_9_2RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_9_1RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_9_0RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_7_2RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_7_1RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_7_0RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_6_2RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_6_1RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_6_0RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_5_3RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_5_2RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_5_1RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_5_0RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_4_1RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_4_0RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_3_1RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_3_0RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_2_1RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_2_0RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_1_3RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_1_2RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_1_1RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_1_0RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_1RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_0RType instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_11RType instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_10RType instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_9RType instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_8RType instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_7RType instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_6RType instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_5RType instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_4RType instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_3RType instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_2RType instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_1RType instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0RType instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1RType instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_1Ref instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_0Ref instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0Ref instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1Ref instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_2TyConInfo instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_1TyConInfo instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_0TyConInfo instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0TyConInfo instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1TyConInfo instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0RTyVar instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1RTyVar instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0Predicate instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1Predicate instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_3PVar instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_2PVar instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_1PVar instance GHC.Generics.Selector Language.Haskell.Liquid.Types.S1_0_0PVar instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0PVar instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1PVar instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_1PVKind instance GHC.Generics.Constructor Language.Haskell.Liquid.Types.C1_0PVKind instance GHC.Generics.Datatype Language.Haskell.Liquid.Types.D1PVKind 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 ty, Data.Data.Data ctor) => Data.Data.Data (Language.Haskell.Liquid.Types.Measure ty ctor) instance GHC.Base.Functor (Language.Haskell.Liquid.Types.Def ty) instance (GHC.Classes.Eq ty, GHC.Classes.Eq ctor) => 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 ty, Data.Data.Data ctor) => Data.Data.Data (Language.Haskell.Liquid.Types.Def ty ctor) instance (GHC.Show.Show ty, GHC.Show.Show ctor) => 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.Classes.Ord Language.Haskell.Liquid.Types.ModName instance GHC.Classes.Eq Language.Haskell.Liquid.Types.ModName 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.Classes.Eq x, Data.Hashable.Class.Hashable x) => GHC.Base.Monoid (Language.Haskell.Liquid.Types.DEnv x ty) instance GHC.Base.Functor Language.Haskell.Liquid.Types.RInstance instance Data.Data.Data Language.Haskell.Liquid.Types.DataConP instance GHC.Generics.Generic Language.Haskell.Liquid.Types.DataConP 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 Language.Haskell.Liquid.Types.TyConP instance GHC.Generics.Generic Language.Haskell.Liquid.Types.TyConP instance Data.Data.Data Language.Haskell.Liquid.Types.RTyCon instance GHC.Generics.Generic Language.Haskell.Liquid.Types.RTyCon 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 c, Data.Data.Data tv, Data.Data.Data r) => 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 τ, Data.Data.Data t) => Data.Data.Data (Language.Haskell.Liquid.Types.Ref τ t) instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Ref τ t) instance Data.Data.Data Language.Haskell.Liquid.Types.TyConInfo instance GHC.Generics.Generic Language.Haskell.Liquid.Types.TyConInfo 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.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 Language.Haskell.Liquid.UX.Config.HasConfig Language.Haskell.Liquid.Types.GhcInfo instance Language.Haskell.Liquid.UX.Config.HasConfig Language.Haskell.Liquid.Types.GhcSpec instance GHC.Base.Monoid Language.Haskell.Liquid.Types.LogicMap instance GHC.Show.Show Language.Haskell.Liquid.Types.LMap instance GHC.Classes.Eq (Language.Haskell.Liquid.Types.PVar t) instance GHC.Classes.Ord (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 Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.PVKind a) instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Predicate instance GHC.Base.Monoid Language.Haskell.Liquid.Types.Predicate instance GHC.Base.Monoid a => GHC.Base.Monoid (Language.Haskell.Liquid.Types.UReft a) instance Language.Fixpoint.Types.Refinements.Subable Language.Haskell.Liquid.Types.UsedPVar instance Language.Fixpoint.Types.Refinements.Subable Language.Haskell.Liquid.Types.Predicate instance Language.Fixpoint.Types.Refinements.Subable Language.Fixpoint.Types.Constraints.Qualifier instance Control.DeepSeq.NFData r => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.UReft r) instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.RTyVar instance Language.Fixpoint.Types.Names.Symbolic Language.Haskell.Liquid.Types.RTyVar instance Control.DeepSeq.NFData 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 (Control.DeepSeq.NFData c, Control.DeepSeq.NFData tv, Control.DeepSeq.NFData r) => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.RType c tv r) instance (Control.DeepSeq.NFData τ, Control.DeepSeq.NFData t) => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.Ref τ t) instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Stratum instance GHC.Base.Monoid Language.Haskell.Liquid.Types.Strata instance Language.Haskell.Liquid.Types.TyConable Language.Haskell.Liquid.Types.RTyCon instance Language.Haskell.Liquid.Types.TyConable Language.Fixpoint.Types.Names.Symbol instance Language.Haskell.Liquid.Types.TyConable Language.Fixpoint.Types.Names.LocSymbol 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.Fixpoint Language.Haskell.Liquid.Types.Cinfo instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.RTyCon instance GHC.Show.Show Language.Haskell.Liquid.Types.RTyCon instance GHC.Show.Show (Language.Haskell.Liquid.Types.Axiom Var.Var TypeRep.Type CoreSyn.CoreExpr) instance GHC.Classes.Eq Language.Haskell.Liquid.Types.DataDecl instance GHC.Classes.Ord Language.Haskell.Liquid.Types.DataDecl instance GHC.Show.Show Language.Haskell.Liquid.Types.DataDecl instance Language.Fixpoint.Types.Refinements.Subable Language.Haskell.Liquid.Types.Stratum instance Language.Fixpoint.Types.Refinements.Reftable Language.Haskell.Liquid.Types.Strata instance Language.Haskell.Liquid.Types.UReftable (Language.Haskell.Liquid.Types.UReft Language.Fixpoint.Types.Refinements.Reft) instance Language.Haskell.Liquid.Types.UReftable () 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.Subable r => Language.Fixpoint.Types.Refinements.Subable (Language.Haskell.Liquid.Types.UReft r) instance (Language.Fixpoint.Types.Refinements.Reftable r, Language.Haskell.Liquid.Types.RefTypable c tv r) => Language.Fixpoint.Types.Refinements.Subable (Language.Haskell.Liquid.Types.RTProp c tv r) instance (Language.Fixpoint.Types.Refinements.Subable r, Language.Haskell.Liquid.Types.RefTypable c tv r) => Language.Fixpoint.Types.Refinements.Subable (Language.Haskell.Liquid.Types.RType c tv r) instance Language.Fixpoint.Types.Refinements.Reftable Language.Haskell.Liquid.Types.Predicate instance GHC.Show.Show Language.Haskell.Liquid.Types.Stratum instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Stratum instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Strata instance Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.PVar a) instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Predicate instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.REnv instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.Errors.TError a) instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Cinfo instance GHC.Show.Show Language.Haskell.Liquid.Types.ModName instance Language.Fixpoint.Types.Names.Symbolic Language.Haskell.Liquid.Types.ModName instance Language.Fixpoint.Types.Names.Symbolic Module.ModuleName instance GHC.Base.Monoid Language.Haskell.Liquid.Types.RTEnv module Language.Haskell.Liquid.Constraint.Fresh class (Applicative m, Monad m) => Freshable m a where true = return . id refresh = return . id fresh :: Freshable m a => m a true :: Freshable m a => a -> m a refresh :: Freshable m a => a -> m a instance Language.Haskell.Liquid.Constraint.Fresh.Freshable m GHC.Integer.Type.Integer => Language.Haskell.Liquid.Constraint.Fresh.Freshable m Language.Fixpoint.Types.Names.Symbol instance Language.Haskell.Liquid.Constraint.Fresh.Freshable m GHC.Integer.Type.Integer => Language.Haskell.Liquid.Constraint.Fresh.Freshable m Language.Fixpoint.Types.Refinements.Expr instance Language.Haskell.Liquid.Constraint.Fresh.Freshable m GHC.Integer.Type.Integer => Language.Haskell.Liquid.Constraint.Fresh.Freshable m [Language.Fixpoint.Types.Refinements.Expr] instance Language.Haskell.Liquid.Constraint.Fresh.Freshable m GHC.Integer.Type.Integer => Language.Haskell.Liquid.Constraint.Fresh.Freshable m Language.Fixpoint.Types.Refinements.Reft instance Language.Haskell.Liquid.Constraint.Fresh.Freshable m GHC.Integer.Type.Integer => Language.Haskell.Liquid.Constraint.Fresh.Freshable m Language.Haskell.Liquid.Types.RReft instance Language.Haskell.Liquid.Constraint.Fresh.Freshable m GHC.Integer.Type.Integer => Language.Haskell.Liquid.Constraint.Fresh.Freshable m Language.Haskell.Liquid.Types.Strata instance (Language.Haskell.Liquid.Constraint.Fresh.Freshable m GHC.Integer.Type.Integer, Language.Haskell.Liquid.Constraint.Fresh.Freshable m r, Language.Fixpoint.Types.Refinements.Reftable r, Language.Haskell.Liquid.Types.RefTypable Language.Haskell.Liquid.Types.RTyCon Language.Haskell.Liquid.Types.RTyVar r) => Language.Haskell.Liquid.Constraint.Fresh.Freshable m (Language.Haskell.Liquid.Types.RRType r) module Language.Haskell.Liquid.Types.Strata class SubStratum a where subsS su x = foldr subS x su subS :: SubStratum a => (Symbol, Stratum) -> a -> a subsS :: SubStratum a => [(Symbol, Stratum)] -> a -> a solveStrata :: [([Stratum], [Stratum])] -> [(Symbol, Stratum)] (<:=) :: (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 -- | Pretty Printing RefType -- --------------------------------------------------- type OkRT c tv r = (TyConable c, PPrint tv, PPrint c, PPrint r, Reftable r, Reftable (RTProp c tv ()), Reftable (RTProp c tv r), RefTypable c tv (), RefTypable c tv r, PPrint (RType c tv r), PPrint (RType c tv ())) rtypeDoc :: (OkRT c tv r) => Tidy -> RType c tv r -> Doc ppr_rtype :: (OkRT c tv r) => PPEnv -> Prec -> RType c tv r -> Doc pprManyOrdered :: (PPrint a, Ord a) => Tidy -> String -> [a] -> [Doc] pprintLongList :: PPrint a => [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 TypeRep.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 r, Language.Fixpoint.Types.Refinements.Reftable r) => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.UReft r) -- | Refinement Types. Mostly mirroring the GHC Type definition, but with -- room for refinements of various sorts. 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 :: (Eq a, Foldable t1) => HashSet TyCon -> t1 a -> RType RTyCon a t -> Bool makeDecrType :: Symbolic a => HashSet TyCon -> [(a, (Symbol, RType RTyCon t (UReft Reft)))] -> (Symbol, RType RTyCon t (UReft Reft)) makeNumEnv :: (Foldable t, TyConable c) => t (RType c b t1) -> [b] makeLexRefa :: [Expr] -> [Expr] -> UReft Reft pdVar :: PVar t -> Predicate findPVar :: [PVar (RType c tv ())] -> UsedPVar -> PVar (RType c tv ()) freeTyVars :: Eq a => RType t a t1 -> [a] tyClasses :: RefTypable RTyCon t t1 => RType RTyCon t t1 -> [(Class, [RType RTyCon t t1])] tyConName :: TyCon -> Symbol ofType :: Monoid r => Type -> RType RTyCon RTyVar r toType :: (Reftable r, PPrint r) => RRType r -> Type rTyVar :: TyVar -> RTyVar rVar :: Monoid r => TyVar -> RType c RTyVar r rApp :: TyCon -> [RType RTyCon tv r] -> [RTProp RTyCon tv r] -> r -> RType RTyCon tv r rEx :: Foldable t => t (Symbol, RType c tv r) -> RType c tv r -> RType c tv r symbolRTyVar :: Symbol -> RTyVar addTyConInfo :: (PPrint r, Reftable r) => (HashMap TyCon FTycon) -> (HashMap TyCon RTyCon) -> RRType r -> RRType r appRTyCon :: SubsTy RTyVar (RType c RTyVar ()) RPVar => HashMap TyCon FTycon -> HashMap TyCon RTyCon -> RTyCon -> [RType c RTyVar r] -> RTyCon typeSort :: TCEmb TyCon -> Type -> Sort typeUniqueSymbol :: Type -> Symbol strengthen :: Reftable r => RType c tv r -> r -> RType c tv r generalize :: (RefTypable c tv r) => RType c tv r -> RType c tv r normalizePds :: RefTypable c tv r => RType c tv r -> RType c tv r subts :: (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 ()) (RType c tv ()), FreeVar 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 ()) (RType c tv ()), FreeVar 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 ()) (RType c tv ()), FreeVar 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 ()) (RType c tv ()), FreeVar 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 ()) (RType c tv ()), FreeVar c tv) => t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r dataConMsReft :: Reftable r => RType c tv r -> [Symbol] -> Reft dataConReft :: DataCon -> [Symbol] -> Reft -- | Binders generated by class predicates, typically for constraining -- tyvars (e.g. FNum) classBinds :: TyConable c => RType c RTyVar t -> [(Symbol, SortedReft)] isSizeable :: HashSet TyCon -> TyCon -> Bool -- | Annotations and Solutions -- ------------------------------------------------- rTypeSortedReft :: (PPrint r, Reftable r) => TCEmb TyCon -> RRType r -> SortedReft rTypeSort :: (PPrint r, Reftable r) => TCEmb TyCon -> RRType r -> Sort shiftVV :: SpecType -> Symbol -> SpecType mkDataConIdsTy :: (Reftable r, PPrint r) => (DataCon, RType RTyCon RTyVar r) -> [(Var, RType RTyCon RTyVar r)] mkTyConInfo :: TyCon -> VarianceInfo -> VarianceInfo -> (Maybe (Symbol -> Expr)) -> TyConInfo meetable :: (OkRT c tv r) => RType c tv r -> RType c tv r -> Bool strengthenRefTypeGen :: (RefTypable c tv (), RefTypable c tv r, OkRT c tv r, FreeVar c tv, SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c) => RType c tv r -> RType c tv r -> RType c tv r strengthenDataConType :: Symbolic t => (t, RType c tv (UReft Reft)) -> (t, RType c tv (UReft Reft)) isBaseTy :: Type -> Bool 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.RefTypable c tv (), Language.Haskell.Liquid.Types.RefTypable c tv r, Language.Haskell.Liquid.Types.PrettyPrint.OkRT c tv r, Language.Haskell.Liquid.Types.RefType.FreeVar 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.PrettyPrint.OkRT c tv r, Language.Haskell.Liquid.Types.RefTypable c tv r, Language.Haskell.Liquid.Types.RefTypable c tv (), Language.Haskell.Liquid.Types.RefType.FreeVar c tv, Language.Haskell.Liquid.Types.SubsTy tv (Language.Haskell.Liquid.Types.RType c tv ()) (Language.Haskell.Liquid.Types.RType c tv ())) => GHC.Base.Monoid (Language.Haskell.Liquid.Types.RTProp c tv r) instance (Language.Haskell.Liquid.Types.PrettyPrint.OkRT c tv r, Language.Haskell.Liquid.Types.RefTypable c tv r, Language.Haskell.Liquid.Types.RefTypable c tv (), Language.Haskell.Liquid.Types.RefType.FreeVar c tv, 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.Fixpoint.Types.Refinements.Reftable (Language.Haskell.Liquid.Types.RTProp c tv r) 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.Fixpoint.Types.Refinements.Reftable (Language.Haskell.Liquid.Types.RType Language.Haskell.Liquid.Types.RTyCon Language.Haskell.Liquid.Types.RTyVar r) instance Language.Fixpoint.Types.PrettyPrint.Fixpoint GHC.Base.String instance Language.Fixpoint.Types.PrettyPrint.Fixpoint Class.Class 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.Fixpoint.Types.Names.LocSymbol Language.Fixpoint.Types.Names.Symbol instance Language.Haskell.Liquid.Types.RefTypable c 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 GHC.Classes.Ord Language.Haskell.Liquid.Types.RTyCon instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.RTyCon instance Language.Haskell.Liquid.Types.SubsTy tv ty () instance Language.Haskell.Liquid.Types.SubsTy tv ty Language.Fixpoint.Types.Refinements.Reft 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 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 Language.Fixpoint.Types.Names.Symbol Language.Haskell.Liquid.Types.BSort Language.Fixpoint.Types.Names.LocSymbol instance Language.Haskell.Liquid.Types.SubsTy Language.Fixpoint.Types.Names.Symbol 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 (Language.Haskell.Liquid.Types.SubsTy Language.Fixpoint.Types.Names.Symbol (Language.Haskell.Liquid.Types.RType c Language.Fixpoint.Types.Names.Symbol ()) c, Language.Haskell.Liquid.Types.TyConable c, Language.Fixpoint.Types.Refinements.Reftable r, Language.Fixpoint.Types.PrettyPrint.PPrint r, Language.Fixpoint.Types.PrettyPrint.PPrint c, Language.Haskell.Liquid.Types.RefType.FreeVar c Language.Fixpoint.Types.Names.Symbol, Language.Haskell.Liquid.Types.SubsTy Language.Fixpoint.Types.Names.Symbol (Language.Haskell.Liquid.Types.RType c Language.Fixpoint.Types.Names.Symbol ()) (Language.Haskell.Liquid.Types.RType c Language.Fixpoint.Types.Names.Symbol ())) => Language.Haskell.Liquid.Types.RefTypable c Language.Fixpoint.Types.Names.Symbol r instance (Language.Fixpoint.Types.Refinements.Reftable r, Language.Fixpoint.Types.PrettyPrint.PPrint r) => Language.Haskell.Liquid.Types.RefTypable Language.Haskell.Liquid.Types.RTyCon Language.Haskell.Liquid.Types.RTyVar r 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.Haskell.Liquid.Types.RefTypable c tv r => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.RType c tv r) 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 module Language.Haskell.Liquid.Types.PredType type PrType = RRType Predicate data TyConP TyConP :: ![RTyVar] -> ![PVar RSort] -> ![Symbol] -> !VarianceInfo -> !VarianceInfo -> !(Maybe (Symbol -> Expr)) -> TyConP [freeTyVarsTy] :: TyConP -> ![RTyVar] [freePredTy] :: TyConP -> ![PVar RSort] [freeLabelTy] :: TyConP -> ![Symbol] [varianceTs] :: TyConP -> !VarianceInfo [variancePs] :: TyConP -> !VarianceInfo [sizeFun] :: TyConP -> !(Maybe (Symbol -> Expr)) data DataConP DataConP :: !SourcePos -> ![RTyVar] -> ![PVar RSort] -> ![Symbol] -> ![SpecType] -> ![(Symbol, SpecType)] -> !SpecType -> !SourcePos -> DataConP [dc_loc] :: DataConP -> !SourcePos [freeTyVars] :: DataConP -> ![RTyVar] [freePred] :: DataConP -> ![PVar RSort] [freeLabels] :: DataConP -> ![Symbol] [tyConsts] :: DataConP -> ![SpecType] [tyArgs] :: DataConP -> ![(Symbol, SpecType)] [tyRes] :: DataConP -> !SpecType [dc_locE] :: DataConP -> !SourcePos dataConTy :: Monoid r => HashMap RTyVar (RType RTyCon RTyVar r) -> Type -> RType RTyCon RTyVar r dataConPSpecType :: DataCon -> DataConP -> SpecType makeTyConInfo :: [(TyCon, TyConP)] -> HashMap TyCon RTyCon -- | Instantiate 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 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 -- | LH Primitive Types ---------------------------------------------- propType :: Reftable r => RRType r propTyCon :: TyCon hpropTyCon :: TyCon pdVarReft :: PVar t -> UReft Reft 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 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 Var [Expr]) -> !(HashSet Var) -> !(HashSet Var) -> !(HashSet TyCon) -> !(TCEmb TyCon) -> !Kuts -> ![(Symbol, Sort)] -> !Bool -> !Bool -> !Bool -> !Bool -> ![Error] -> !KVProf -> !Int -> HashMap BindId SrcSpan -> !Bool -> 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])] -- | Terminating Metrics for Recursive functions [termExprs] :: CGInfo -> !(HashMap Var [Expr]) -- | Set of variables to ignore for termination checking [specLVars] :: CGInfo -> !(HashSet Var) -- | ? FIX THIS [specLazy] :: CGInfo -> !(HashSet Var) -- | ? FIX THIS [autoSize] :: CGInfo -> !(HashSet TyCon) -- | primitive Sorts into which TyCons should be embedded [tyConEmbed] :: CGInfo -> !(TCEmb TyCon) -- | Fixpoint Kut variables (denoting "back-edges"/recursive KVars) [kuts] :: CGInfo -> !Kuts -- | ? FIX THIS [lits] :: CGInfo -> ![(Symbol, Sort)] -- | Check Termination (?) [tcheck] :: CGInfo -> !Bool -- | Check Strata (?) [scheck] :: CGInfo -> !Bool -- | Trust ghc auto generated bindings [trustghc] :: CGInfo -> !Bool -- | prune unsorted refinements [pruneRefs] :: CGInfo -> !Bool -- | Errors during constraint generation [logErrors] :: CGInfo -> ![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 data CGEnv CGE :: !SpanStack -> !REnv -> !(SEnv Var) -> !RDEnv -> !FEnv -> !(HashSet Var) -> !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)) -> 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 -- | Fixpoint Environment [fenv] :: CGEnv -> !FEnv -- | recursive defs being processed (for annotations) [recs] :: CGEnv -> !(HashSet Var) -- | Datatype invariants [invs] :: CGEnv -> !RTyConInv -- | Datatype checkable invariants [ial] :: CGEnv -> !RTyConIAl -- | Top-level variables with (assert)-guarantees to verify [grtys] :: CGEnv -> !REnv -- | Top-level variables with assumed types [assms] :: CGEnv -> !REnv -- | 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 axiomatized Haskell functions to the logical -- functions [aenv] :: CGEnv -> !(HashMap Var Symbol) -- | error that should be reported at the user [cerr] :: CGEnv -> !(Maybe (TError SpecType)) data LConstraint LC :: [[(Symbol, SpecType)]] -> LConstraint -- | Fixpoint Environment -- ------------------------------------------------------ data FEnv FE :: !IBindEnv -> !(SEnv Sort) -> FEnv -- | Integer Keys for Fixpoint Environment [feBinds] :: FEnv -> !IBindEnv -- | Fixpoint Environment [feEnv] :: FEnv -> !(SEnv Sort) 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 data WfC WfC :: !CGEnv -> !SpecType -> WfC type FixWfC = WfC Cinfo -- | Helper Types: Invariants -- -------------------------------------------------- type RTyConInv = HashMap RTyCon [SpecType] mkRTyConInv :: [Located SpecType] -> RTyConInv addRTyConInv :: RTyConInv -> SpecType -> SpecType addRInv :: RTyConInv -> (Var, SpecType) -> (Var, SpecType) type RTyConIAl = HashMap RTyCon [SpecType] mkRTyConIAl :: [(a, Located SpecType)] -> RTyConInv instance GHC.Base.Monoid Language.Haskell.Liquid.Constraint.Types.LConstraint instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Constraint.Types.CGEnv instance GHC.Show.Show Language.Haskell.Liquid.Constraint.Types.CGEnv instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Constraint.Types.SubC instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Constraint.Types.WfC instance Language.Haskell.Liquid.Types.Strata.SubStratum Language.Haskell.Liquid.Constraint.Types.SubC instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Constraint.Types.CGInfo 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.SubC instance Control.DeepSeq.NFData Language.Haskell.Liquid.Constraint.Types.WfC instance Control.DeepSeq.NFData Language.Haskell.Liquid.Constraint.Types.CGInfo module Language.Haskell.Liquid.Transforms.CoreToLogic coreToDef :: Reftable r => LocSymbol -> Var -> CoreExpr -> LogicM [Def (RRType r) DataCon] coreToFun :: LocSymbol -> Var -> CoreExpr -> LogicM ([Var], Either Expr Expr) coreToLogic :: CoreExpr -> LogicM Expr coreToPred :: CoreExpr -> LogicM Expr mkLit :: Literal -> Maybe Expr runToLogic :: TCEmb TyCon -> LogicMap -> (String -> Error) -> LogicM t -> Either t Error logicType :: (Reftable r) => Type -> RRType r strengthenResult :: Var -> SpecType instance GHC.Base.Monad Language.Haskell.Liquid.Transforms.CoreToLogic.LogicM instance GHC.Base.Functor Language.Haskell.Liquid.Transforms.CoreToLogic.LogicM instance GHC.Base.Applicative Language.Haskell.Liquid.Transforms.CoreToLogic.LogicM instance GHC.Show.Show CoreSyn.CoreExpr 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 module Language.Haskell.Liquid.Constraint.ProofToCore type HId = Id type HVar = Var HId type HAxiom = Axiom HId type HCtor = Ctor HId type HVarCtor = VarCtor HId type HQuery = Query HId type HInstance = Instance HId type HProof = Proof HId type HExpr = Expr HId type CmbExpr = CoreExpr -> CoreExpr -> CoreExpr class ToCore a toCore :: ToCore a => CmbExpr -> CoreExpr -> a -> CoreExpr -- | combineProofs :: combinator -> default expressions -> list of -- proofs | -> combined result combineProofs :: CmbExpr -> CoreExpr -> [CoreExpr] -> CoreExpr combine :: Show t1 => [t1] -> (Expr Var -> t -> Expr Var) -> Expr Var -> [t] -> Expr Var -- | To make application we need to instantiate expressions irrelevant to -- logic | type application and dictionaries. | Then, ANF the final -- expression makeApp :: CoreExpr -> [CoreExpr] -> CoreExpr -- | ANF anf :: ([CoreBind], [CoreExpr], [Int]) -> CoreExpr -> ([CoreBind], [CoreExpr], [Int]) -- | Filling up dictionaries makeDictionaries :: Id -> CoreExpr -> [Expr b] makeDictionary :: Id -> Type -> Expr b -- | Filling up types instantiateVars :: [(Var, Type)] -> Expr CoreBndr -> Expr CoreBndr resolveVs :: [Id] -> [(Type, Type)] -> [(Id, Type)] resolveVar :: Var -> Type -> [(Var, Type)] -> Type substTyV :: (Id, Type) -> (Type, Type) -> (Type, Type) varCombine :: Show a => a -> Type -> Var varANF :: Show a => a -> Type -> Var varANFPr :: Show a => a -> Type -> Var bkArrow :: Type -> ([Var], [Type]) instance Language.Haskell.Liquid.Constraint.ProofToCore.ToCore Language.Haskell.Liquid.Constraint.ProofToCore.HInstance instance Language.Haskell.Liquid.Constraint.ProofToCore.ToCore Language.Haskell.Liquid.Constraint.ProofToCore.HProof instance Language.Haskell.Liquid.Constraint.ProofToCore.ToCore Language.Haskell.Liquid.Constraint.ProofToCore.HAxiom instance Language.Haskell.Liquid.Constraint.ProofToCore.ToCore Language.Haskell.Liquid.Constraint.ProofToCore.HExpr instance Language.Haskell.Liquid.Constraint.ProofToCore.ToCore Language.Haskell.Liquid.Constraint.ProofToCore.HCtor instance Language.Haskell.Liquid.Constraint.ProofToCore.ToCore Language.Haskell.Liquid.Constraint.ProofToCore.HVar instance GHC.Show.Show TypeRep.Type 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) => RRBound RSort -> [RRType r] -> [Symbol] -> (RRType r) -> (RRType r) 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.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) -- | 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 (+=) :: (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' :: (Reftable r, PPrint 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 instance Language.Haskell.Liquid.Constraint.Fresh.Freshable Language.Haskell.Liquid.Constraint.Types.CG GHC.Integer.Type.Integer -- | 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 -- | 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 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.Constraint.Axioms expandProofs :: Provable a => GhcInfo -> [(Symbol, SpecType)] -> a -> CG a makeCombineType :: Maybe Type -> Type makeCombineVar :: Type -> Var instance Language.Haskell.Liquid.Constraint.Axioms.Provable CoreSyn.CoreBind instance Language.Haskell.Liquid.Constraint.Axioms.Provable CoreSyn.CoreExpr instance Language.Haskell.Liquid.Constraint.Axioms.Provable CoreSyn.CoreAlt -- | 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.Measure data Spec ty bndr Spec :: ![Measure ty bndr] -> ![(LocSymbol, ty)] -> ![(LocSymbol, ty)] -> ![(LocSymbol, ty)] -> ![Located ty] -> ![(Located ty, Located ty)] -> ![Symbol] -> ![DataDecl] -> ![FilePath] -> ![RTAlias Symbol BareType] -> ![RTAlias Symbol Expr] -> !(TCEmb LocSymbol) -> ![Qualifier] -> ![(LocSymbol, [Int])] -> ![LocSymbol] -> !(HashSet LocSymbol) -> !(HashSet LocSymbol) -> !(HashSet LocSymbol) -> !(HashSet LocSymbol) -> !(HashSet LocSymbol) -> !(HashSet LocSymbol) -> ![Located String] -> ![Measure ty ()] -> ![Measure ty bndr] -> ![RClass ty] -> ![(LocSymbol, [Expr])] -> ![RInstance ty] -> ![(LocSymbol, [Variance])] -> !(RRBEnv ty) -> Spec ty bndr -- | User-defined properties for ADTs [measures] :: Spec ty bndr -> ![Measure ty bndr] -- | Assumed (unchecked) types [asmSigs] :: Spec ty bndr -> ![(LocSymbol, ty)] -- | Imported functions and types [sigs] :: Spec ty bndr -> ![(LocSymbol, ty)] -- | Local type signatures [localSigs] :: Spec ty bndr -> ![(LocSymbol, ty)] -- | Data type invariants [invariants] :: Spec ty bndr -> ![Located ty] -- | Data type invariants to be checked [ialiases] :: Spec ty bndr -> ![(Located ty, Located ty)] -- | Loaded spec module names [imports] :: Spec ty bndr -> ![Symbol] -- | Predicated data definitions [dataDecls] :: Spec ty bndr -> ![DataDecl] -- | Included qualifier files [includes] :: Spec ty bndr -> ![FilePath] -- | RefType aliases [aliases] :: Spec ty bndr -> ![RTAlias Symbol BareType] -- | Expression aliases [ealiases] :: Spec ty bndr -> ![RTAlias Symbol Expr] -- | GHC-Tycon-to-fixpoint Tycon map [embeds] :: Spec ty bndr -> !(TCEmb LocSymbol) -- | Qualifiers in source/spec files [qualifiers] :: Spec ty bndr -> ![Qualifier] -- | Information on decreasing arguments [decr] :: Spec ty bndr -> ![(LocSymbol, [Int])] -- | Variables that should be checked in the environment they are used [lvars] :: Spec ty bndr -> ![LocSymbol] -- | Ignore Termination Check in these Functions [lazy] :: Spec ty bndr -> !(HashSet LocSymbol) -- | Binders to turn into axiomatized functions [axioms] :: Spec ty bndr -> !(HashSet LocSymbol) -- | Binders to turn into measures using haskell definitions [hmeas] :: Spec ty bndr -> !(HashSet LocSymbol) -- | Binders to turn into bounds using haskell definitions [hbounds] :: Spec ty bndr -> !(HashSet LocSymbol) -- | Binders to turn into logic inline using haskell definitions [inlines] :: Spec ty bndr -> !(HashSet LocSymbol) -- | Type Constructors that get automatically sizing info [autosize] :: Spec ty bndr -> !(HashSet LocSymbol) -- | Command-line configurations passed in through source [pragmas] :: Spec ty bndr -> ![Located String] -- | Measures attached to a type-class [cmeasures] :: Spec ty bndr -> ![Measure ty ()] -- | Mappings from (measure,type) -> measure [imeasures] :: Spec ty bndr -> ![Measure ty bndr] -- | Refined Type-Classes [classes] :: Spec ty bndr -> ![RClass ty] -- | Terminating Conditions for functions [termexprs] :: Spec ty bndr -> ![(LocSymbol, [Expr])] [rinstance] :: Spec ty bndr -> ![RInstance ty] [dvariance] :: Spec ty bndr -> ![(LocSymbol, [Variance])] [bounds] :: Spec ty bndr -> !(RRBEnv ty) type BareSpec = Spec BareType LocSymbol data MSpec ty ctor MSpec :: HashMap Symbol [Def ty ctor] -> HashMap LocSymbol (Measure ty ctor) -> HashMap LocSymbol (Measure ty ()) -> ![Measure ty ctor] -> MSpec ty ctor [ctorMap] :: MSpec ty ctor -> HashMap Symbol [Def ty ctor] [measMap] :: MSpec ty ctor -> HashMap LocSymbol (Measure ty ctor) [cmeasMap] :: MSpec ty ctor -> HashMap LocSymbol (Measure ty ()) [imeas] :: MSpec ty ctor -> ![Measure ty ctor] mkM :: LocSymbol -> ty -> [Def ty bndr] -> Measure ty bndr mkMSpec :: [Measure ty (Located Symbol)] -> [Measure ty ()] -> [Measure ty (Located Symbol)] -> MSpec ty (Located Symbol) mkMSpec' :: Symbolic ctor => [Measure ty ctor] -> MSpec ty ctor qualifySpec :: Symbol -> Spec ty bndr -> Spec ty bndr dataConTypes :: MSpec (RRType Reft) DataCon -> ([(Var, RRType Reft)], [(LocSymbol, RRType Reft)]) defRefType :: Type -> Def (RRType Reft) DataCon -> RRType Reft -- | A wired-in measure strLen that describes the length of a -- string literal, with type Addr#. strLen :: Measure SpecType ctor wiredInMeasures :: MSpec SpecType DataCon instance GHC.Base.Monoid (Language.Haskell.Liquid.Measure.Spec ty bndr) 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) module Language.Haskell.Liquid.Parse hsSpecificationP :: SourceName -> String -> Either Error (ModName, BareSpec) lhsSpecificationP :: SourceName -> String -> Either Error (ModName, BareSpec) -- | Used to parse .spec files specSpecificationP :: SourceName -> String -> Either Error (ModName, BareSpec) parseSymbolToLogic :: SourceName -> String -> Either Error LogicMap instance GHC.Show.Show (Language.Haskell.Liquid.Parse.Pspec a b) instance Language.Fixpoint.Parse.Inputable Language.Haskell.Liquid.Types.BareType instance Language.Fixpoint.Parse.Inputable (Language.Haskell.Liquid.Types.Measure Language.Haskell.Liquid.Types.BareType Language.Fixpoint.Types.Names.LocSymbol) module Language.Haskell.Liquid.Types.Dictionaries makeDictionaries :: [RInstance SpecType] -> DEnv Symbol SpecType makeDictionary :: RInstance SpecType -> (Symbol, HashMap Symbol SpecType) dfromList :: [(Var, HashMap Symbol t)] -> DEnv Var t dmapty :: (a -> b) -> DEnv v a -> DEnv v b dmap :: (v1 -> v2) -> HashMap k v1 -> HashMap k v2 dinsert :: (Eq x, Hashable x) => DEnv x ty -> x -> HashMap Symbol ty -> DEnv x ty dlookup :: (Eq k, Hashable k) => DEnv k t -> k -> Maybe (HashMap Symbol t) dhasinfo :: Show a1 => Maybe (HashMap Symbol a) -> a1 -> Maybe a 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 -- | 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 returns a subset of the [CoreBind] given which -- correspond to those binders that depend on any of the Vars -- provided. thin :: [CoreBind] -> [Var] -> [CoreBind] -- | 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 () 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 GHC.Base.Functor Data.Algorithm.Diff.Diff instance Data.Aeson.Types.Class.ToJSON Text.Parsec.Pos.SourcePos instance Data.Aeson.Types.Class.FromJSON Text.Parsec.Pos.SourcePos instance Data.Aeson.Types.Class.ToJSON Language.Haskell.Liquid.Types.ErrorResult instance Data.Aeson.Types.Class.FromJSON Language.Haskell.Liquid.Types.ErrorResult instance Data.Aeson.Types.Class.ToJSON Text.PrettyPrint.HughesPJ.Doc instance Data.Aeson.Types.Class.FromJSON Text.PrettyPrint.HughesPJ.Doc instance (Data.Aeson.Types.Class.ToJSON k, Data.Aeson.Types.Class.ToJSON v) => Data.Aeson.Types.Class.ToJSON (Data.HashMap.Base.HashMap k v) instance (GHC.Classes.Eq k, Data.Hashable.Class.Hashable k, Data.Aeson.Types.Class.FromJSON k, Data.Aeson.Types.Class.FromJSON v) => Data.Aeson.Types.Class.FromJSON (Data.HashMap.Base.HashMap k v) instance Data.Aeson.Types.Class.ToJSON a => Data.Aeson.Types.Class.ToJSON (Language.Haskell.Liquid.Types.AnnInfo a) instance Data.Aeson.Types.Class.FromJSON a => Data.Aeson.Types.Class.FromJSON (Language.Haskell.Liquid.Types.AnnInfo a) instance Data.Aeson.Types.Class.ToJSON (Language.Haskell.Liquid.Types.Output Text.PrettyPrint.HughesPJ.Doc) instance Data.Aeson.Types.Class.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 () instance Data.Aeson.Types.Class.ToJSON Language.Haskell.Liquid.UX.ACSS.Status instance Data.Aeson.Types.Class.ToJSON Language.Haskell.Liquid.UX.Annotate.Annot1 instance Data.Aeson.Types.Class.ToJSON Language.Haskell.Liquid.GHC.Misc.Loc instance Data.Aeson.Types.Class.ToJSON Language.Haskell.Liquid.UX.Annotate.AnnErrors instance (GHC.Show.Show k, Data.Aeson.Types.Class.ToJSON a) => Data.Aeson.Types.Class.ToJSON (Language.Haskell.Liquid.UX.Annotate.Assoc k a) instance Data.Aeson.Types.Class.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 -- | Updating options withPragmas :: Config -> FilePath -> [Located String] -> IO Config -- | Exit Function ----------------------------------------------------- exitWithResult :: Config -> FilePath -> Output Doc -> IO (Output Doc) -- | check subset of binders modified (+ dependencies) since last check diffcheck :: Config -> Bool instance Language.Fixpoint.Types.PrettyPrint.Fixpoint (Language.Fixpoint.Types.Errors.FixResult Language.Haskell.Liquid.UX.CmdLine.CError) 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 -> ![(Symbol, Var)] -> HscEnv -> LogicMap -> InlnEnv -> RBEnv -> BareEnv [modName] :: BareEnv -> !ModName [tcEnv] :: BareEnv -> !TCEnv [rtEnv] :: BareEnv -> !RTEnv [varEnv] :: BareEnv -> ![(Symbol, Var)] [hscEnv] :: BareEnv -> HscEnv [logicEnv] :: BareEnv -> LogicMap [inlines] :: BareEnv -> InlnEnv [bounds] :: BareEnv -> RBEnv data TInline TI :: [Symbol] -> Expr -> TInline [tiargs] :: TInline -> [Symbol] [tibody] :: TInline -> Expr type InlnEnv = HashMap Symbol TInline inModule :: MonadState BareEnv m => ModName -> m b -> m b withVArgs :: (Foldable t, PPrint a, MonadState BareEnv m) => SourcePos -> SourcePos -> t a -> m b -> m b setRTAlias :: MonadState BareEnv m => Symbol -> RTAlias RTyVar SpecType -> m () setREAlias :: MonadState BareEnv m => Symbol -> RTAlias Symbol Expr -> m () execBare :: BareM a -> BareEnv -> IO (Either Error a) insertLogicEnv :: MonadState BareEnv m => Symbol -> [Symbol] -> Expr -> m () insertAxiom :: MonadState BareEnv m => Var -> Symbol -> m () instance GHC.Show.Show Language.Haskell.Liquid.Bare.Env.TInline module Language.Haskell.Liquid.Bare.RefToLogic class Transformable a where tx' lmap imap x = foldrWithKey tx x limap where limap = fromList ((mapSnd Left <$> (toList $ logic_map lmap)) ++ (mapSnd Right <$> toList imap)) txRefToLogic :: (Transformable r) => LogicMap -> InlnEnv -> r -> r instance Language.Haskell.Liquid.Bare.RefToLogic.Transformable a => Language.Haskell.Liquid.Bare.RefToLogic.Transformable [a] instance Language.Haskell.Liquid.Bare.RefToLogic.Transformable Language.Haskell.Liquid.Types.DataConP instance Language.Haskell.Liquid.Bare.RefToLogic.Transformable Language.Haskell.Liquid.Bare.Env.TInline instance Language.Haskell.Liquid.Bare.RefToLogic.Transformable r => Language.Haskell.Liquid.Bare.RefToLogic.Transformable (Language.Haskell.Liquid.Types.RType c v r) instance Language.Haskell.Liquid.Bare.RefToLogic.Transformable Language.Haskell.Liquid.Types.RReft instance Language.Haskell.Liquid.Bare.RefToLogic.Transformable Language.Fixpoint.Types.Refinements.Reft instance (Language.Haskell.Liquid.Bare.RefToLogic.Transformable a, Language.Haskell.Liquid.Bare.RefToLogic.Transformable b) => Language.Haskell.Liquid.Bare.RefToLogic.Transformable (Data.Either.Either a b) instance Language.Haskell.Liquid.Bare.RefToLogic.Transformable Language.Fixpoint.Types.Refinements.Expr instance Language.Haskell.Liquid.Bare.RefToLogic.Transformable (Language.Haskell.Liquid.Types.Measure t c) instance Language.Haskell.Liquid.Bare.RefToLogic.Transformable (Language.Haskell.Liquid.Types.Def t c) instance Language.Haskell.Liquid.Bare.RefToLogic.Transformable Language.Haskell.Liquid.Types.Body module Language.Haskell.Liquid.Bare.SymSort txRefSort :: TCEnv -> TCEmb TyCon -> Located SpecType -> Located SpecType module Language.Haskell.Liquid.Bare.Lookup class Symbolic a => GhcLookup a lookupName :: GhcLookup a => HscEnv -> ModName -> a -> IO [Name] srcSpan :: GhcLookup a => a -> SrcSpan lookupGhcThing :: (MonadIO m, MonadError (TError t) m, MonadState BareEnv m, GhcLookup a) => [Char] -> (TyThing -> Maybe b) -> a -> m b -- | 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 => a -> BareM TyCon lookupGhcDataCon :: (MonadIO m, MonadError (TError t) m, MonadState BareEnv m) => Located Symbol -> m 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 module Language.Haskell.Liquid.Bare.Expand expandReft :: RReft -> BareM RReft expandExpr :: Expr -> BareM Expr 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.Axiom makeAxiom :: TCEmb TyCon -> LogicMap -> [CoreBind] -> GhcSpec -> BareSpec -> LocSymbol -> BareM ((Symbol, Located SpecType), [(Var, Located SpecType)], [HAxiom]) instance Language.Haskell.Liquid.Bare.Axiom.Simplifiable CoreSyn.CoreExpr instance Language.Haskell.Liquid.Bare.Axiom.Simplifiable CoreSyn.CoreBind instance Language.Haskell.Liquid.Bare.Axiom.Subable CoreSyn.CoreExpr module Language.Haskell.Liquid.Bare.Misc makeSymbols :: (Functor t1, Functor t2, Foldable t, Foldable t1, Foldable t2, Reftable r, Reftable r1, Reftable r2, MonadState BareEnv m, TyConable c, TyConable c1, TyConable c2) => (Id -> Bool) -> [Id] -> [Symbol] -> t2 (a1, Located (RType c2 tv2 r2)) -> t1 (a, Located (RType c1 tv1 r1)) -> t (Located (RType c tv r)) -> m [(Symbol, Var)] 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 :: (PPrint r, Reftable r) => Type -> RRType r -> StateT MapTyVarST (Either Error) () symbolRTyVar :: Symbol -> RTyVar simpleSymbolVar :: Var -> Symbol hasBoolResult :: Type -> Bool module Language.Haskell.Liquid.Bare.Plugged makePluggedSigs :: Traversable t => ModName -> TCEmb TyCon -> HashMap TyCon RTyCon -> NameSet -> t (Var, Located (RRType RReft)) -> WriterT [Warn] (ExceptT Error (StateT BareEnv IO)) (t (Var, Located (RType RTyCon RTyVar RReft))) makePluggedAsmSigs :: Traversable t => TCEmb TyCon -> HashMap TyCon RTyCon -> t (Var, Located (RRType RReft)) -> WriterT [Warn] (ExceptT Error (StateT BareEnv IO)) (t (Var, Located (RType RTyCon RTyVar RReft))) makePluggedDataCons :: Traversable t => TCEmb TyCon -> HashMap TyCon RTyCon -> t (DataCon, Located DataConP) -> WriterT [Warn] (ExceptT Error (StateT BareEnv IO)) (t (DataCon, Located DataConP)) 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.OfType ofBareType :: SourcePos -> BareType -> BareM SpecType ofMeaSort :: BareType -> BareM SpecType ofBSort :: BSort -> BareM RSort ofBPVar :: BPVar -> BareM RPVar mkSpecType :: SourcePos -> BareType -> BareM SpecType mkSpecType' :: SourcePos -> [PVar BSort] -> BareType -> BareM SpecType module Language.Haskell.Liquid.Bare.DataType makeConTypes :: (ModName, Spec ty bndr) -> WriterT [Warn] (ExceptT Error (StateT BareEnv IO)) ([(TyCon, TyConP)], [[(DataCon, Located DataConP)]]) makeTyConEmbeds :: (ModName, Spec ty bndr) -> WriterT [Warn] (ExceptT Error (StateT BareEnv IO)) (TCEmb TyCon) makeRecordSelectorSigs :: [(DataCon, Located DataConP)] -> BareM [(Var, Located SpecType)] dataConSpec :: [(DataCon, DataConP)] -> [(Var, SpecType)] meetDataConSpec :: [(Var, SpecType)] -> [(DataCon, DataConP)] -> [(Var, SpecType)] module Language.Haskell.Liquid.Bare.Check checkGhcSpec :: [(ModName, BareSpec)] -> SEnv SortedReft -> GhcSpec -> Either [Error] GhcSpec checkTerminationExpr :: (Eq v, PPrint v) => TCEmb TyCon -> SEnv SortedReft -> (v, Located SpecType, [Expr]) -> Maybe Error checkTy :: (Doc -> Error) -> TCEmb TyCon -> TCEnv -> SEnv SortedReft -> Located SpecType -> Maybe Error module Language.Haskell.Liquid.Bare.Measure makeHaskellMeasures :: TCEmb TyCon -> [CoreBind] -> ModName -> (ModName, BareSpec) -> BareM (MSpec SpecType DataCon) makeHaskellInlines :: TCEmb TyCon -> [CoreBind] -> ModName -> (ModName, BareSpec) -> BareM () makeHaskellBounds :: TCEmb TyCon -> CoreProgram -> HashSet (Var, LocSymbol) -> BareM RBEnv makeMeasureSpec :: (ModName, Spec BareType LocSymbol) -> BareM (MSpec SpecType DataCon) makeMeasureSpec' :: MSpec (RType RTyCon RTyVar (UReft Reft)) DataCon -> ([(Var, RType RTyCon RTyVar (UReft Reft))], [(LocSymbol, RRType Reft)]) makeClassMeasureSpec :: MSpec (RType c tv (UReft r2)) t -> [(LocSymbol, CMeasure (RType c tv r2))] makeMeasureSelectors :: (DataCon, Located DataConP) -> [Measure SpecType DataCon] strengthenHaskellMeasures :: HashSet (Located Var) -> [(Var, Located SpecType)] varMeasures :: (Monoid r) => [Var] -> [(Symbol, Located (RRType r))] module Language.Haskell.Liquid.Bare.RTEnv makeRTEnv :: [(ModName, Spec ty bndr)] -> WriterT [Warn] (ExceptT Error (StateT BareEnv IO)) () module Language.Haskell.Liquid.Bare.Spec makeClasses :: ModName -> Config -> [Var] -> (ModName, Spec BareType bndr) -> WriterT [Warn] (ExceptT Error (StateT BareEnv IO)) [((DataCon, DataConP), [(ModName, Var, Located SpecType)])] makeQualifiers :: (ModName, Spec ty bndr) -> WriterT [Warn] (ExceptT Error (StateT BareEnv IO)) [Qualifier] makeHints :: [Var] -> Spec ty bndr -> BareM [(Var, [Int])] makeLVar :: [Var] -> Spec ty bndr -> WriterT [Warn] (ExceptT Error (StateT BareEnv IO)) [Var] makeLazy :: [Var] -> Spec ty bndr -> WriterT [Warn] (ExceptT Error (StateT BareEnv IO)) [Var] makeHIMeas :: [Var] -> Spec ty bndr -> WriterT [Warn] (ExceptT Error (StateT BareEnv IO)) [Located Var] makeTExpr :: [Var] -> Spec ty bndr -> BareM [(Var, [Expr])] -- | API: Bare Refinement Types ---------------------------------- makeTargetVars :: ModName -> [Var] -> [String] -> BareM [Var] makeAssertSpec :: ModName -> Config -> [Var] -> [Var] -> (ModName, Spec BareType bndr) -> BareM [(ModName, Var, Located SpecType)] makeAssumeSpec :: ModName -> Config -> [Var] -> [Var] -> (ModName, Spec BareType bndr) -> BareM [(ModName, Var, Located SpecType)] makeDefaultMethods :: [Var] -> [(ModName, Var, Located SpecType)] -> [(ModName, Var, Located SpecType)] makeIAliases :: (ModName, Spec BareType bndr) -> WriterT [Warn] (ExceptT Error (StateT BareEnv IO)) [(Located SpecType, Located SpecType)] makeInvariants :: (ModName, Spec BareType bndr) -> WriterT [Warn] (ExceptT Error (StateT BareEnv IO)) [Located SpecType] makeSpecDictionaries :: Traversable t => TCEmb TyCon -> [Var] -> t (t1, Spec BareType bndr) -> GhcSpec -> WriterT [Warn] (ExceptT Error (StateT BareEnv IO)) GhcSpec makeBounds :: Eq a => TCEmb TyCon -> a -> [Var] -> CoreProgram -> [(a, Spec BareType bndr)] -> WriterT [Warn] (ExceptT Error (StateT BareEnv IO)) () makeHBounds :: [Var] -> Spec ty bndr -> BareM [(Var, LocSymbol)] 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 -- | This module defines the representation of Subtyping and WF -- Constraints, and the code for syntax-directed constraint generation. module Language.Haskell.Liquid.Constraint.Generate generateConstraints :: GhcInfo -> CGInfo instance 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.Bare.GhcSpec -- | The following is the overall type for specifications obtained -- from parsing the target source and dependent libraries data GhcSpec SP :: ![(Var, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Symbol, Located SpecType)] -> ![Located SpecType] -> ![(Located SpecType, Located SpecType)] -> ![(DataCon, DataConP)] -> ![(TyCon, TyConP)] -> ![(Symbol, Var)] -> TCEmb TyCon -> ![Qualifier] -> ![Var] -> ![(Var, [Int])] -> ![(Var, [Expr])] -> !(HashSet Var) -> !(HashSet Var) -> !(HashSet TyCon) -> !Config -> !NameSet -> [Measure SpecType DataCon] -> HashMap TyCon RTyCon -> DEnv Var SpecType -> [HAxiom] -> LogicMap -> Maybe Type -> GhcSpec -- | Asserted Reftypes eg. see include/Prelude.spec [tySigs] :: GhcSpec -> ![(Var, Located SpecType)] -- | Assumed Reftypes [asmSigs] :: GhcSpec -> ![(Var, Located SpecType)] -- | Auto generated Signatures [inSigs] :: GhcSpec -> ![(Var, Located SpecType)] -- | Data Constructor Measure Sigs eg. (:) :: a -> xs:[a] -> {v: Int -- | v = 1 + len(xs) } [ctors] :: GhcSpec -> ![(Var, Located SpecType)] -- | Measure Types eg. len :: [a] -> Int [meas] :: GhcSpec -> ![(Symbol, Located SpecType)] -- | Data Type Invariants eg. forall a. {v: [a] | len(v) >= 0} [invariants] :: GhcSpec -> ![Located SpecType] -- | Data Type Invariant Aliases [ialiases] :: GhcSpec -> ![(Located SpecType, Located SpecType)] -- | Predicated Data-Constructors e.g. see testsposMap.hs [dconsP] :: GhcSpec -> ![(DataCon, DataConP)] -- | Predicated Type-Constructors eg. see testsposMap.hs [tconsP] :: GhcSpec -> ![(TyCon, TyConP)] -- | List of Symbol free in spec and corresponding GHC var eg. -- (Cons, Cons#7uz) from testsposex1.hs [freeSyms] :: GhcSpec -> ![(Symbol, Var)] -- | How to embed GHC Tycons into fixpoint sorts e.g. "embed Set as -- Set_set" from includeDataSet.spec [tcEmbeds] :: GhcSpec -> TCEmb TyCon -- | Qualifiers in Source/Spec files e.g testsposqualTest.hs [qualifiers] :: GhcSpec -> ![Qualifier] -- | Top-level Binders To Verify (empty means ALL binders) [tgtVars] :: GhcSpec -> ![Var] -- | Lexicographically ordered size witnesses for termination [decr] :: GhcSpec -> ![(Var, [Int])] -- | Lexicographically ordered expressions for termination [texprs] :: GhcSpec -> ![(Var, [Expr])] -- | Variables that should be checked in the environment they are used [lvars] :: GhcSpec -> !(HashSet Var) -- | Binders to IGNORE during termination checking [lazy] :: GhcSpec -> !(HashSet Var) -- | Binders to IGNORE during termination checking [autosize] :: GhcSpec -> !(HashSet TyCon) -- | Configuration Options [config] :: GhcSpec -> !Config -- | Names exported by the module being verified [exports] :: GhcSpec -> !NameSet [measures] :: GhcSpec -> [Measure SpecType DataCon] [tyconEnv] :: GhcSpec -> HashMap TyCon RTyCon -- | Dictionary Environment [dicts] :: GhcSpec -> DEnv Var SpecType [axioms] :: GhcSpec -> [HAxiom] [logicMap] :: GhcSpec -> LogicMap [proofType] :: GhcSpec -> Maybe Type makeGhcSpec :: Config -> ModName -> [CoreBind] -> [Var] -> [Var] -> NameSet -> HscEnv -> Either Error LogicMap -> [(ModName, BareSpec)] -> IO GhcSpec -- | 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, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Var, Located SpecType)] -> ![(Symbol, Located SpecType)] -> ![Located SpecType] -> ![(Located SpecType, Located SpecType)] -> ![(DataCon, DataConP)] -> ![(TyCon, TyConP)] -> ![(Symbol, Var)] -> TCEmb TyCon -> ![Qualifier] -> ![Var] -> ![(Var, [Int])] -> ![(Var, [Expr])] -> !(HashSet Var) -> !(HashSet Var) -> !(HashSet TyCon) -> !Config -> !NameSet -> [Measure SpecType DataCon] -> HashMap TyCon RTyCon -> DEnv Var SpecType -> [HAxiom] -> LogicMap -> Maybe Type -> GhcSpec -- | Asserted Reftypes eg. see include/Prelude.spec [tySigs] :: GhcSpec -> ![(Var, Located SpecType)] -- | Assumed Reftypes [asmSigs] :: GhcSpec -> ![(Var, Located SpecType)] -- | Auto generated Signatures [inSigs] :: GhcSpec -> ![(Var, Located SpecType)] -- | Data Constructor Measure Sigs eg. (:) :: a -> xs:[a] -> {v: Int -- | v = 1 + len(xs) } [ctors] :: GhcSpec -> ![(Var, Located SpecType)] -- | Measure Types eg. len :: [a] -> Int [meas] :: GhcSpec -> ![(Symbol, Located SpecType)] -- | Data Type Invariants eg. forall a. {v: [a] | len(v) >= 0} [invariants] :: GhcSpec -> ![Located SpecType] -- | Data Type Invariant Aliases [ialiases] :: GhcSpec -> ![(Located SpecType, Located SpecType)] -- | Predicated Data-Constructors e.g. see testsposMap.hs [dconsP] :: GhcSpec -> ![(DataCon, DataConP)] -- | Predicated Type-Constructors eg. see testsposMap.hs [tconsP] :: GhcSpec -> ![(TyCon, TyConP)] -- | List of Symbol free in spec and corresponding GHC var eg. -- (Cons, Cons#7uz) from testsposex1.hs [freeSyms] :: GhcSpec -> ![(Symbol, Var)] -- | How to embed GHC Tycons into fixpoint sorts e.g. "embed Set as -- Set_set" from includeDataSet.spec [tcEmbeds] :: GhcSpec -> TCEmb TyCon -- | Qualifiers in Source/Spec files e.g testsposqualTest.hs [qualifiers] :: GhcSpec -> ![Qualifier] -- | Top-level Binders To Verify (empty means ALL binders) [tgtVars] :: GhcSpec -> ![Var] -- | Lexicographically ordered size witnesses for termination [decr] :: GhcSpec -> ![(Var, [Int])] -- | Lexicographically ordered expressions for termination [texprs] :: GhcSpec -> ![(Var, [Expr])] -- | Variables that should be checked in the environment they are used [lvars] :: GhcSpec -> !(HashSet Var) -- | Binders to IGNORE during termination checking [lazy] :: GhcSpec -> !(HashSet Var) -- | Binders to IGNORE during termination checking [autosize] :: GhcSpec -> !(HashSet TyCon) -- | Configuration Options [config] :: GhcSpec -> !Config -- | Names exported by the module being verified [exports] :: GhcSpec -> !NameSet [measures] :: GhcSpec -> [Measure SpecType DataCon] [tyconEnv] :: GhcSpec -> HashMap TyCon RTyCon -- | Dictionary Environment [dicts] :: GhcSpec -> DEnv Var SpecType [axioms] :: GhcSpec -> [HAxiom] [logicMap] :: GhcSpec -> LogicMap [proofType] :: GhcSpec -> Maybe Type makeGhcSpec :: Config -> ModName -> [CoreBind] -> [Var] -> [Var] -> NameSet -> HscEnv -> Either Error LogicMap -> [(ModName, BareSpec)] -> IO GhcSpec module Language.Haskell.Liquid.Constraint.Qualifier specificationQualifiers :: Int -> GhcInfo -> SEnv Sort -> [Qualifier] module Language.Haskell.Liquid.Constraint.ToFixpoint cgInfoFInfo :: GhcInfo -> CGInfo -> FilePath -> IO (FInfo Cinfo) module Language.Haskell.Liquid.GHC.Interface getGhcInfo :: Maybe HscEnv -> Config -> FilePath -> IO (GhcInfo, HscEnv) pprintCBs :: [CoreBind] -> Doc 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 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 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.Generics.Constructor Language.Haskell.Liquid.Interactive.Types.C1_1Status instance GHC.Generics.Constructor Language.Haskell.Liquid.Interactive.Types.C1_0Status instance GHC.Generics.Datatype Language.Haskell.Liquid.Interactive.Types.D1Status 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 Language.Haskell.Liquid.List transpose :: Int -> [[a]] -> [[a]] module Language.Haskell.Liquid.Foreign intCSize :: Int -> CSize cSizeInt :: CSize -> Int mkPtr :: Addr# -> Ptr b isNullPtr :: Ptr a -> Bool fpLen :: ForeignPtr a -> Int pLen :: Ptr a -> Int deref :: Ptr a -> a eqPtr :: Ptr a -> Ptr a -> Bool module Language.Haskell.Liquid.Prelude plus :: Int -> Int -> Int minus :: Int -> Int -> Int times :: Int -> Int -> Int eq :: Int -> Int -> Bool neq :: Int -> Int -> Bool leq :: Int -> Int -> Bool geq :: Int -> Int -> Bool lt :: Int -> Int -> Bool gt :: Int -> Int -> Bool liquidAssertB :: Bool -> Bool liquidAssert :: Bool -> a -> a liquidAssume :: Bool -> a -> a liquidAssumeB :: (a -> Bool) -> a -> a liquidError :: String -> a crash :: Bool -> a force :: Bool choose :: Int -> Int isEven :: Int -> Bool isOdd :: Int -> Bool safeZipWith :: (a -> b -> c) -> [a] -> [b] -> [c] (==>) :: Bool -> Bool -> Bool