liquidhaskell-boot 0.9.8.1 → 0.9.8.2
raw patch · 15 files changed
+672/−105 lines, 15 filesdep ~liquid-fixpoint
Dependency ranges changed: liquid-fixpoint
Files
- liquidhaskell-boot.cabal +4/−2
- src-ghc/Liquid/GHC/API.hs +2/−1
- src/Language/Haskell/Liquid/Bare.hs +56/−17
- src/Language/Haskell/Liquid/Bare/Axiom.hs +117/−2
- src/Language/Haskell/Liquid/Bare/Check.hs +2/−1
- src/Language/Haskell/Liquid/Bare/Elaborate.hs +30/−35
- src/Language/Haskell/Liquid/Constraint/Generate.hs +1/−1
- src/Language/Haskell/Liquid/Parse.hs +18/−23
- src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs +5/−5
- src/Language/Haskell/Liquid/Types/Specs.hs +11/−1
- src/Language/Haskell/Liquid/UX/DiffCheck.hs +1/−17
- tests/specfiles/pos/Empty.spec +1/−0
- tests/specfiles/pos/T707.spec +17/−0
- tests/specfiles/pos/T788.spec +26/−0
- tests/specfiles/pos/T924.spec +381/−0
liquidhaskell-boot.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.4 name: liquidhaskell-boot-version: 0.9.8.1+version: 0.9.8.2 synopsis: Liquid Types for Haskell description: This package provides a plugin to verify Haskell programs. But most likely you should be using the [liquidhaskell package](https://hackage.haskell.org/package/liquidhaskell)@@ -13,7 +13,9 @@ category: Language homepage: https://github.com/ucsd-progsys/liquidhaskell build-type: Simple-tested-with: GHC == 9.8.1+tested-with: GHC == 9.8.2++extra-source-files: tests/specfiles/pos/*.spec source-repository head type: git
src-ghc/Liquid/GHC/API.hs view
@@ -322,7 +322,7 @@ ( Reduction(Reduction) ) import GHC.Core.Subst as Ghc (emptySubst, extendCvSubst) import GHC.Core.TyCo.Rep as Ghc- ( FunTyFlag(FTF_T_T)+ ( FunTyFlag(FTF_T_T, FTF_C_T) , ForAllTyFlag(Required) , Coercion ( AppCo@@ -354,6 +354,7 @@ , LitTy , TyConApp , TyVarTy+ , ft_af , ft_arg , ft_res )
src/Language/Haskell/Liquid/Bare.hs view
@@ -62,6 +62,8 @@ import Control.Arrow (second) import Data.Hashable (Hashable) import qualified Language.Haskell.Liquid.Bare.Slice as Dg+import Data.Bifunctor (bimap)+import Data.Function (on) -------------------------------------------------------------------------------- -- | De/Serializing Spec files@@ -281,6 +283,7 @@ -- Preserve user-defined 'dvariance'. , rinstance = Ms.rinstance finalLiftedSpec ++ Ms.rinstance mySpec -- Preserve rinstances.+ , asmReflectSigs = Ms.asmReflectSigs mySpec } }) where@@ -647,6 +650,8 @@ rwrWith <- makeRewriteWith env name mySpec wRefls <- Bare.wiredReflects cfg env name sig xtes <- Bare.makeHaskellAxioms cfg src env tycEnv name lmap sig mySpec+ asmReflAxioms <- Bare.makeAssumeReflectAxioms src env tycEnv name sig mySpec+ let otherAxioms = thd3 <$> asmReflAxioms let myAxioms = [ Bare.qualifyTop env@@ -655,26 +660,36 @@ e {eqName = s, eqRec = S.member s (exprSymbolsSet (eqBody e))} | (x, lt, e) <- xtes , let s = symbol x- ]+ ] ++ otherAxioms+ let asmReflEls = eqName <$> otherAxioms+ let impAxioms = concatMap (filter ((`notElem` asmReflEls) . eqName) . Ms.axeqs . snd) (M.toList specs) let sigVars = F.notracepp "SIGVARS" $ (fst3 <$> xtes) -- reflects ++ (fst <$> gsAsmSigs sig) -- assumes ++ (fst <$> gsRefSigs sig)- return SpRefl- { gsLogicMap = lmap- , gsAutoInst = autoInst- , gsImpAxioms = concatMap (Ms.axeqs . snd) (M.toList specs)- , gsMyAxioms = F.notracepp "gsMyAxioms" myAxioms- , gsReflects = F.notracepp "gsReflects" (lawMethods ++ filter (isReflectVar rflSyms) sigVars ++ wRefls)- , gsHAxioms = F.notracepp "gsHAxioms" xtes- , gsWiredReft = wRefls- , gsRewrites = rwr- , gsRewritesWith = rwrWith- }+ case anyNonReflFn of+ Just (actSym , preSym) ->+ let preSym' = show (val preSym) in+ let errorMsg = preSym' ++ " must be reflected first using {-@ reflect " ++ preSym' ++ " @-}" in+ let error = ErrHMeas (GM.sourcePosSrcSpan $ loc actSym) (pprint $ val actSym) (text errorMsg) :: Error+ in Ex.throw error+ Nothing -> return SpRefl+ { gsLogicMap = lmap+ , gsAutoInst = autoInst+ , gsImpAxioms = impAxioms+ , gsMyAxioms = myAxioms+ , gsReflects = lawMethods ++ filter (isReflectVar rflSyms) sigVars ++ (fst <$> gsAsmReflects sig) ++ wRefls+ , gsHAxioms = F.notracepp "gsHAxioms" $ xtes ++ asmReflAxioms+ , gsWiredReft = wRefls+ , gsRewrites = rwr+ , gsRewritesWith = rwrWith+ } where lawMethods = F.notracepp "Law Methods" $ concatMap Ghc.classMethods (fst <$> Bare.meCLaws menv) mySpec = M.lookupDefault mempty name specs rflSyms = S.fromList (getReflects specs) lmap = Bare.reLMap env+ notInReflOnes (_, a) = not $ a `S.member` Ms.reflects mySpec+ anyNonReflFn = L.find notInReflOnes (Ms.asmReflectSigs mySpec) isReflectVar :: S.HashSet F.Symbol -> Ghc.Var -> Bool isReflectVar reflSyms v = S.member vx reflSyms@@ -684,7 +699,7 @@ getReflects :: Bare.ModSpecs -> [Symbol] getReflects = fmap val . S.toList . S.unions . fmap (names . snd) . M.toList where- names z = S.unions [ Ms.reflects z, Ms.inlines z, Ms.hmeas z ]+ names z = S.unions [ Ms.reflects z, S.fromList (snd <$> Ms.asmReflectSigs z), S.fromList (fst <$> Ms.asmReflectSigs z), Ms.inlines z, Ms.hmeas z ] ------------------------------------------------------------------------------------------ -- | @updateReflSpecSig@ uses the information about reflected functions to update the@@ -694,6 +709,12 @@ ------------------------------------------------------------------------------------------ addReflSigs env name rtEnv refl sig = sig { gsRefSigs = F.notracepp ("gsRefSigs for " ++ F.showpp name) $ map expandReflectedSignature reflSigs+ -- We make sure that the reflected functions are excluded from `gsAsmSigs`, except for the signatures of+ -- actual functions in assume-reflect. The latter are added here because 1. it's what makes tests work+ -- and 2. so that we probably "shadow" the old signatures of the actual function correctly. Note that even if the+ -- signature of the actual function was asserted and not assumed, we do not put our new signature for the actual function+ -- in `gsTySigs` (which is for asserted signatures). Indeed, the new signature will *always* be an assumption since we+ -- add the extra post-condition that the actual and pretended function behave in the same way. , gsAsmSigs = F.notracepp ("gsAsmSigs for " ++ F.showpp name) (wreflSigs ++ filter notReflected (gsAsmSigs sig)) } where@@ -709,8 +730,14 @@ (wreflSigs, reflSigs) = L.partition ((`elem` gsWiredReft refl) . fst) [ (x, t) | (x, t, _) <- gsHAxioms refl ]- reflected = fst <$> (wreflSigs ++ reflSigs)- notReflected xt = fst xt `notElem` reflected+ -- Get the set of all the actual functions (in assume-reflects)+ actualFnsInAssmRefl = S.fromList $ fst <$> gsAsmReflects sig+ isActualFn x = S.member x actualFnsInAssmRefl+ -- Get all the variables from the axioms that are not actual functions (in assume-reflects)+ notReflActualTySigs = L.filter (not . isActualFn . fst) reflSigs+ -- Get the list of reflected elements. We do not count actual functions in assume reflect as reflected+ reflected = S.fromList $ fst <$> (wreflSigs ++ notReflActualTySigs)+ notReflected xt = fst xt `notElem` reflected makeAutoInst :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (M.HashMap Ghc.Var (Maybe Int))@@ -743,6 +770,7 @@ return SpSig { gsTySigs = tySigs , gsAsmSigs = asmSigs+ , gsAsmReflects = bimap getVar getVar <$> concatMap (asmReflectSigs . snd) (M.toList specs) , gsRefSigs = [] , gsDicts = dicts -- , gsMethods = if noclasscheck cfg then [] else Bare.makeMethodTypes dicts (Bare.meClasses measEnv) cbs@@ -758,6 +786,12 @@ mySpec = M.lookupDefault mempty name specs allSpecs = M.toList specs rtEnv = Bare.sigRTEnv sigEnv+ getVar sym = case Bare.lookupGhcVar env name "wiredAxioms" sym of+ Right x -> x+ Left _ -> Ex.throw $ mkError sym $ "Not in scope: " ++ show (val sym)++ mkError :: LocSymbol -> String -> Error+ mkError x str = ErrHMeas (GM.sourcePosSrcSpan $ loc x) (pprint $ val x) (text str) -- hmeas = makeHMeas env allSpecs strengthenSigs :: [(Ghc.Var, (Int, LocSpecType))] ->[(Ghc.Var, LocSpecType)]@@ -837,7 +871,9 @@ myAsmSig v sigs = Mb.fromMaybe errImp (mbHome `mplus` mbImp) where mbHome = takeUnique mkErr sigsHome- mbImp = takeUnique mkErr (Misc.firstGroup sigsImp) -- see [NOTE:Prioritize-Home-Spec]+ -- In case we import multiple specifications for the same function stemming from `assume-reflect` from different modules, we want+ -- to follow the same convention as in other places and so take the last one in alphabetical order and shadow the others+ mbImp = takeBiggest fst (Misc.firstGroup sigsImp) -- see [NOTE:Prioritize-Home-Spec] sigsHome = [(m, t) | (True, m, t) <- sigs ] sigsImp = F.notracepp ("SIGS-IMP: " ++ F.showpp v) [(d, (m, t)) | (False, m, t) <- sigs, let d = nameDistance vName m]@@ -891,11 +927,14 @@ | vName == F.symbol tName = 0 | otherwise = 1 - takeUnique :: Ex.Exception e => ([a] -> e) -> [a] -> Maybe a takeUnique _ [] = Nothing takeUnique _ [x] = Just x takeUnique f xs = Ex.throw (f xs)++takeBiggest :: (Ord b) => (a -> b) -> [a] -> Maybe a+takeBiggest _ [] = Nothing+takeBiggest f xs = Just $ L.maximumBy (compare `on` f) xs allAsmSigs :: Bare.Env -> ModName -> Bare.ModSpecs -> Bare.Lookup [(Ghc.Var, [(Bool, ModName, LocBareType)])]
src/Language/Haskell/Liquid/Bare/Axiom.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} @@ -7,7 +8,7 @@ -- | This module contains the code that DOES reflection; i.e. converts Haskell -- definitions into refinements. -module Language.Haskell.Liquid.Bare.Axiom ( makeHaskellAxioms, wiredReflects ) where+module Language.Haskell.Liquid.Bare.Axiom ( makeHaskellAxioms, makeAssumeReflectAxioms, wiredReflects ) where import Prelude hiding (error) import Prelude hiding (mapM)@@ -32,7 +33,28 @@ import Language.Haskell.Liquid.Bare.Resolve as Bare import Language.Haskell.Liquid.Bare.Types as Bare+import qualified Data.List as L+import Language.Haskell.Liquid.Misc (fst4)+import Control.Applicative+import Data.Function (on)+import qualified Data.Map as Map +findDuplicatePair :: Ord k => (a -> k) -> [a] -> Maybe (a, a)+findDuplicatePair key xs =+ Mb.listToMaybe+ [ (a, b)+ | a:b:_ <- L.groupBy ((==) `on` key) (L.sortOn key xs)+ ]++findDuplicateBetweenLists :: (Ord k) => (a -> k) -> [a] -> [a] -> Maybe (a, a)+findDuplicateBetweenLists key l1 l2 =+ findDuplicate key (Map.fromList [ (key x, x) | x <- l1 ]) l2+ where+ findDuplicate :: Ord k => (a -> k) -> Map.Map k a -> [a] -> Maybe (a, a)+ findDuplicate key' seen l2' =+ Mb.listToMaybe+ [ (x, y) | x <- l2', Just y <- [Map.lookup (key' x) seen]]+ ----------------------------------------------------------------------------------------------- makeHaskellAxioms :: Config -> GhcSrc -> Bare.Env -> Bare.TycEnv -> ModName -> LogicMap -> GhcSpecSig -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, LocSpecType, F.Equation)]@@ -42,6 +64,99 @@ let refDefs = getReflectDefs src spSig spec return (makeAxiom env tycEnv name lmap <$> (wiDefs ++ refDefs)) +-----------------------------------------------------------------------------------------------+-- Returns a list of elements, one per assume reflect --+-- Each element is made of: --+-- * The variable name of the actual function --+-- * The refined type of actual function, where the post-condition is strengthened with --+-- ``VV == pretendedFn arg1 arg2 ...` --+-- * The assume reflect equation, linking the pretended and actual function: --+-- `actualFn arg1 arg 2 ... = pretendedFn arg1 arg2 ...` --+makeAssumeReflectAxioms :: GhcSrc -> Bare.Env -> Bare.TycEnv -> ModName -> GhcSpecSig -> Ms.BareSpec+ -> Bare.Lookup [(Ghc.Var, LocSpecType, F.Equation)]+-----------------------------------------------------------------------------------------------+makeAssumeReflectAxioms src env tycEnv name spSig spec = do+ -- Send an error message if we're redefining a reflection+ case findDuplicatePair val reflActSymbols <|> findDuplicateBetweenLists val refSymbols reflActSymbols of+ Just (x , y) -> Ex.throw $ mkError y $ "Duplicate reflection of " ++ show x ++ " and " ++ show y+ Nothing -> return $ makeAssumeReflectAxiom spSig env embs name <$> Ms.asmReflectSigs spec+ where+ refDefs = getReflectDefs src spSig spec+ embs = Bare.tcEmbs tycEnv+ refSymbols = fst4 <$> refDefs+ reflActSymbols = fst <$> Ms.asmReflectSigs spec++-----------------------------------------------------------------------------------------------+-- Processes one `assume reflect` and returns its axiom element, as detailed in --+-- `makeAssumeReflectAxioms` --+makeAssumeReflectAxiom :: GhcSpecSig -> Bare.Env -> F.TCEmb Ghc.TyCon -> ModName+ -> (LocSymbol, LocSymbol) -- actual function and pretended function+ -> (Ghc.Var, LocSpecType, F.Equation)+-----------------------------------------------------------------------------------------------+makeAssumeReflectAxiom sig env tce name (actual, pretended) =+ -- The actual and pretended function must have the same type+ if pretendedTy == actualTy then+ (actualV, actual {val = aty_at `strengthenRes` F.subst su ref} , actualEq)+ else+ Ex.throw $ mkError actual $+ show qPretended ++ " and " ++ show qActual ++ " should have the same type. But " +++ "types " ++ F.showpp pretendedTy ++ " and " ++ F.showpp actualTy ++ " do not match."+ where+ -- Get the Ghc.Var's of the actual and pretended function names+ actualV = case Bare.lookupGhcVar env name "wiredAxioms" actual of+ Right x -> x+ Left _ -> Ex.throw $ mkError actual $ "Not in scope: " ++ show (val actual)+ pretendedV = case Bare.lookupGhcVar env name "wiredAxioms" pretended of+ Right x -> x+ Left _ -> Ex.throw $ mkError pretended $ "Not in scope: " ++ show (val pretended)+ -- Get the qualified name symbols for the actual and pretended functions+ qActual = Bare.qualifyTop env name (F.loc actual) (val actual)+ qPretended = Bare.qualifyTop env name (F.loc pretended) (val pretended)+ -- Get the GHC type of the actual and pretended functions+ actualTy = Ghc.varType actualV+ pretendedTy = Ghc.varType pretendedV+ -- Compute argument names for the actual/pretended functions+ -- The argument names are lq1, lq2, etc.+ -- These argument names will be used in the equation+ args = getArgs 1 actualTy+ -- Function types can be of multiple sorts. We are only interested in the Type -> Type (i.e., ->) ones,+ -- which correspond to flag Ghc.FTF_T_T. For (=>) Constraint -> Type (flag FTF_C_T), we just ignore the+ -- (constraint) argument. For the others kinds, we throw are error, as they are unsupported.+ getArgs :: Int -> Ghc.Type -> [(F.Symbol, F.Sort)]+ getArgs n Ghc.FunTy{ft_arg=ty0, ft_res=ty1, ft_af=Ghc.FTF_T_T} = (F.symbol . ("lq" ++) . show $ n, typeSort tce ty0) : getArgs (n+1) ty1+ getArgs n Ghc.FunTy{ft_res=ty1, ft_af=Ghc.FTF_C_T} = getArgs n ty1+ getArgs _ Ghc.FunTy{} = Ex.throw $ mkError actual "This function cannot be `assume reflect`'ed. Its signature is too complex for me."+ getArgs n (Ghc.ForAllTy _ ty) = getArgs n ty+ getArgs _ _ = []++ -- Compute the refined type of the actual function. See `makeAssumeType` for details+ sigs = gsTySigs sig ++ gsAsmSigs sig -- We also look into assumed signatures+ -- Try to get the specification of the actual function from the signatures+ mbT = val <$> lookup actualV sigs+ -- Refines that spec. If the specification is not in the scope, just use the GHC type as a dummy spec+ -- to proceed with.+ rt = fromRTypeRep .+ (\trep@RTypeRep{..} ->+ trep{ty_info = fmap (\i -> i{permitTC = Just allowTC}) ty_info}) .+ toRTypeRep $ Mb.fromMaybe (ofType actualTy) mbT+ -- Decompose the function type into arguments and return types+ at = axiomType allowTC actual rt+ aty_at = aty at+ -- The return type of the function+ out = rTypeSort tce $ ares at+ -- The arguments names and types, as given by `AxiomType`+ xArgs = F.EVar . fst <$> aargs at+ allowTC = typeclass (getConfig env)+ -- Expression of the equation. It is just saying that the actual and pretended functions are the same+ -- when applied to the same arguments+ le = foldl F.EApp (F.EVar qPretended) (F.EVar . fst <$> args)+ ref = F.Reft (F.vv_, F.PAtom F.Eq (F.EVar F.vv_) le)+ -- Substitute our argument names with the actual arguments given from `xArgs`+ -- in the final, refined type+ su = F.mkSubst $ zip (fst <$> args) xArgs++ actualEq = F.mkEquation qActual args le out+ getReflectDefs :: GhcSrc -> GhcSpecSig -> Ms.BareSpec -> [(LocSymbol, Maybe SpecType, Ghc.Var, Ghc.CoreExpr)] getReflectDefs src sig spec = findVarDefType cbs sigs <$> xs@@ -58,7 +173,7 @@ Just (v, e) -> if GM.isExternalId v || isMethod (F.symbol x) || isDictionary (F.symbol x) then (x, val <$> lookup v sigs, v, e) else Ex.throw $ mkError x ("Lifted functions must be exported; please export " ++ show v)- Nothing -> Ex.throw $ mkError x "Cannot lift haskell function"+ Nothing -> Ex.throw $ mkError x $ show (val x) ++ " is not in scope" -------------------------------------------------------------------------------- makeAxiom :: Bare.Env -> Bare.TycEnv -> ModName -> LogicMap
src/Language/Haskell/Liquid/Bare/Check.hs view
@@ -9,6 +9,7 @@ ( checkTargetSpec , checkBareSpec , checkTargetSrc+ , tyCompat ) where @@ -633,7 +634,7 @@ keep | allowTC = not . isEmbeddedClass | otherwise = not . isClassType -- YL: extract permitTC information from sort- allowTC = or $ fmap (fromMaybe False . permitTC) (ty_info $ toRTypeRep sort)+ allowTC = any (fromMaybe False . permitTC) (ty_info $ toRTypeRep sort) trep = toRTypeRep ct su = checkMBodyUnify (ty_res trep) (last txs) txs = thd5 $ bkArrowDeep sort
src/Language/Haskell/Liquid/Bare/Elaborate.hs view
@@ -9,9 +9,6 @@ {-# OPTIONS_GHC -Wno-orphans #-} -{-# OPTIONS_GHC -Wno-dodgy-imports #-} -- TODO(#1913): Fix import of Data.Functor.Foldable.Fix-{-# OPTIONS_GHC -Wno-unused-top-binds #-} -- TODO(#1914): Is RTypeF even used?- -- | This module uses GHC API to elaborate the resolves expressions -- TODO: Genearlize to BareType and replace the existing resolution mechanisms@@ -37,12 +34,10 @@ import Control.Monad.Free #if MIN_VERSION_recursion_schemes(5,2,0) import Data.Fix hiding (hylo)-import Data.Functor.Foldable hiding (Fix)-#else-import Data.Functor.Foldable #endif import Data.Char ( isUpper )+import Data.Functor.Foldable import GHC.Types.Name.Occurrence import qualified Liquid.GHC.API as Ghc (noExtField)@@ -126,65 +121,65 @@ -- | Base functor of RType data RTypeF c tv r f = RVarF {- rtf_var :: !tv- , rtf_reft :: !r+ _rtf_var :: !tv+ , _rtf_reft :: !r } | RFunF {- rtf_bind :: !F.Symbol- , rtf_rinfo :: !RFInfo- , rtf_in :: !f- , rtf_out :: !f- , rtf_reft :: !r+ _rtf_bind :: !F.Symbol+ , _rtf_rinfo :: !RFInfo+ , _rtf_in :: !f+ , _rtf_out :: !f+ , _rtf_reft :: !r } | RAllTF {- rtf_tvbind :: !(RTVU c tv) -- RTVar tv (RType c tv ()))- , rtf_ty :: !f- , rtf_ref :: !r+ _rtf_tvbind :: !(RTVU c tv) -- RTVar tv (RType c tv ()))+ , _rtf_ty :: !f+ , _rtf_ref :: !r } -- | "forall x y <z :: Nat, w :: Int> . TYPE" -- ^^^^^^^^^^^^^^^^^^^ (rtf_pvbind) | RAllPF {- rtf_pvbind :: !(PVU c tv) -- ar (RType c tv ()))- , rtf_ty :: !f+ _rtf_pvbind :: !(PVU c tv) -- ar (RType c tv ()))+ , _rtf_ty :: !f } -- | For example, in [a]<{\h -> v > h}>, we apply (via `RApp`) -- * the `RProp` denoted by `{\h -> v > h}` to -- * the `RTyCon` denoted by `[]`. | RAppF {- rtf_tycon :: !c- , rtf_args :: ![f]- , rtf_pargs :: ![RTPropF c tv f]- , rtf_reft :: !r+ _rtf_tycon :: !c+ , _rtf_args :: ![f]+ , _rtf_pargs :: ![RTPropF c tv f]+ , _rtf_reft :: !r } | RAllEF {- rtf_bind :: !F.Symbol- , rtf_allarg :: !f- , rtf_ty :: !f+ _rtf_bind :: !F.Symbol+ , _rtf_allarg :: !f+ , _rtf_ty :: !f } | RExF {- rtf_bind :: !F.Symbol- , rtf_exarg :: !f- , rtf_ty :: !f+ _rtf_bind :: !F.Symbol+ , _rtf_exarg :: !f+ , _rtf_ty :: !f } | RExprArgF (F.Located F.Expr) | RAppTyF{- rtf_arg :: !f- , rtf_res :: !f- , rtf_reft :: !r+ _rtf_arg :: !f+ , _rtf_res :: !f+ , _rtf_reft :: !r } | RRTyF {- rtf_env :: ![(F.Symbol, f)]- , rtf_ref :: !r- , rtf_obl :: !Oblig- , rtf_ty :: !f+ _rtf_env :: ![(F.Symbol, f)]+ , _rtf_ref :: !r+ , _rtf_obl :: !Oblig+ , _rtf_ty :: !f } | RHoleF r
src/Language/Haskell/Liquid/Constraint/Generate.hs view
@@ -351,7 +351,7 @@ = cconsE γ (f e) t cconsE' γ e@(Cast e' c) t- = do t' <- castTy γ (exprType e) e' c+ = do t' <- (`strengthen` uTop (rTypeReft t)) <$> castTy γ (exprType e) e' c addC (SubC γ (F.notracepp ("Casted Type for " ++ GM.showPpr e ++ "\n init type " ++ showpp t) t') t) ("cconsE Cast: " ++ GM.showPpr e) cconsE' γ e t
src/Language/Haskell/Liquid/Parse.hs view
@@ -252,11 +252,11 @@ PcExplicit b -> parseFun c b <?> "btP" where- parseFun c@(PC sb t1) sym =+ parseFun c@(PC sb t1) sy = (do reservedOp "->" PC _ t2 <- btP- return (PC sb (rFun sym t1 t2)))+ return (PC sb (rFun sy t1 t2))) <|> (do reservedOp "=>"@@ -408,8 +408,8 @@ -> Parser Expr -> Parser (Reft -> BareType) -> Parser BareType-refDefP sym rp kindP' = braces $ do- x <- optBindP sym+refDefP sy rp kindP' = braces $ do+ x <- optBindP sy -- NOSUBST i <- freshIntP t <- try (kindP' <* reservedOp "|") <|> return (RHole . uTop) <?> "refDefP" ra <- rp@@ -836,6 +836,7 @@ data Pspec ty ctor = Meas (Measure ty ctor) -- ^ 'measure' definition | Assm (LocSymbol, ty) -- ^ 'assume' signature (unchecked)+ | AssmReflect (LocSymbol, LocSymbol) -- ^ 'assume reflects' signature (unchecked) | Asrt (LocSymbol, ty) -- ^ 'assert' signature (checked) | LAsrt (LocSymbol, ty) -- ^ 'local' assertion -- TODO RJ: what is this | Asrts ([LocSymbol], (ty, Maybe [Located Expr])) -- ^ TODO RJ: what is this@@ -899,6 +900,8 @@ = "measure" <+> pprintTidy k m ppPspec k (Assm (lx, t)) = "assume" <+> pprintTidy k (val lx) <+> "::" <+> pprintTidy k t+ppPspec k (AssmReflect (lx, ly))+ = "assume reflect" <+> pprintTidy k (val lx) <+> "as" <+> pprintTidy k (val ly) ppPspec k (Asrt (lx, t)) = "assert" <+> pprintTidy k (val lx) <+> "::" <+> pprintTidy k t ppPspec k (LAsrt (lx, t))@@ -1053,6 +1056,7 @@ mkSpec name xs = (name,) $ qualifySpec (symbol name) Measure.Spec { Measure.measures = [m | Meas m <- xs] , Measure.asmSigs = [a | Assm a <- xs]+ , Measure.asmReflectSigs = [(l, r) | AssmReflect (l, r) <- xs] , Measure.sigs = [a | Asrt a <- xs] ++ [(y, t) | Asrts (ys, (t, _)) <- xs, y <- ys] , Measure.localSigs = []@@ -1101,9 +1105,9 @@ -- | Parse a single top level liquid specification specP :: Parser BPspec specP- = fallbackSpecP "assume"- ((reserved "relational" >> fmap AssmRel relationalP)- <|> fmap Assm tyBindP )+ = fallbackSpecP "assume" ((reserved "reflect" >> fmap AssmReflect assmReflectBindP)+ <|> (reserved "relational" >> fmap AssmRel relationalP)+ <|> fmap Assm tyBindP ) <|> fallbackSpecP "assert" (fmap Asrt tyBindP ) <|> fallbackSpecP "autosize" (fmap ASize asizeP ) <|> (reserved "local" >> fmap LAsrt tyBindP )@@ -1174,10 +1178,10 @@ -- | Same as tyBindsP, except the single initial symbol has already been matched tyBindsRemP :: LocSymbol -> Parser ([LocSymbol], (Located BareType, Maybe [Located Expr]))-tyBindsRemP sym = do+tyBindsRemP sy = do reservedOp "::" tb <- termBareTypeP- return ([sym],tb)+ return ([sy],tb) pragmaP :: Parser (Located String) pragmaP = locStringLiteral@@ -1247,6 +1251,11 @@ tyBindP = (,) <$> locBinderP <* reservedOp "::" <*> located genBareTypeP +-- | Parses a loc symbol.+assmReflectBindP :: Parser (LocSymbol, LocSymbol)+assmReflectBindP =+ (,) <$> locBinderP <* reservedOp "as" <*> locBinderP+ termBareTypeP :: Parser (Located BareType, Maybe [Located Expr]) termBareTypeP = do t <- located genBareTypeP@@ -1631,20 +1640,6 @@ dataPropTyP :: Parser (Maybe BareType) dataPropTyP = Just <$> between (reservedOp "::") (reserved "where") bareTypeP-------------------------------------------------------------------------- | Parsing Qualifiers ---------------------------------------------------------------------------------------------------------------------fTyConP :: Parser FTycon-fTyConP- = (reserved "int" >> return intFTyCon)- <|> (reserved "Integer" >> return intFTyCon)- <|> (reserved "Int" >> return intFTyCon)- <|> (reserved "real" >> return realFTyCon)- <|> (reserved "bool" >> return boolFTyCon)- <|> (symbolFTycon <$> locUpperIdP)- <?> "fTyConP" --------------------------------------------------------------------- -- Identifiers ------------------------------------------------------
src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs view
@@ -39,7 +39,7 @@ import Control.Monad.Identity import qualified Language.Fixpoint.Misc as Misc import qualified Language.Haskell.Liquid.Misc as Misc-import Language.Fixpoint.Types hiding (panic, Error, R, simplify)+import Language.Fixpoint.Types hiding (panic, Error, R, simplify, isBool) import qualified Language.Fixpoint.Types as F import qualified Language.Haskell.Liquid.GHC.Misc as GM @@ -111,9 +111,9 @@ hasRApps _ = False --- | 'weakenResult foo t' drops the singleton constraint `v = foo x y` --- that is added, e.g. for measures in /strengthenResult'. --- This should only be used _when_ checking the body of 'foo' +-- | 'weakenResult foo t' drops the singleton constraint `v = foo x y`+-- that is added, e.g. for measures in /strengthenResult'.+-- This should only be used _when_ checking the body of 'foo' -- where the output, is, by definition, equal to the singleton. weakenResult :: Bool -> Var -> SpecType -> SpecType weakenResult allowTC v t = F.notracepp msg t'@@ -621,7 +621,7 @@ = C.Let (simplify allowTC xes) (simplify allowTC e) simplify allowTC (C.Case e x _t alts@[Alt _ _ ee,_,_]) | isBangInteger alts -- XXX(matt): seems to be for debugging?- = -- Misc.traceShow ("To simplify allowTC case") $ + = -- Misc.traceShow ("To simplify allowTC case") $ sub (M.singleton x (simplify allowTC e)) (simplify allowTC ee) simplify allowTC (C.Case e x t alts) = C.Case (simplify allowTC e) x t (filter (not . isPatErrorAlt) (simplify allowTC <$> alts))
src/Language/Haskell/Liquid/Types/Specs.hs view
@@ -232,6 +232,7 @@ data GhcSpecSig = SpSig { gsTySigs :: ![(Var, LocSpecType)] -- ^ Asserted Reftypes , gsAsmSigs :: ![(Var, LocSpecType)] -- ^ Assumed Reftypes+ , gsAsmReflects :: ![(Var, Var)] -- ^ Assumed Reftypes (left is the actual function name and right the pretended one) , gsRefSigs :: ![(Var, LocSpecType)] -- ^ Reflected Reftypes , gsInSigs :: ![(Var, LocSpecType)] -- ^ Auto generated Signatures , gsNewTypes :: ![(TyCon, LocSpecType)] -- ^ Mapping of 'newtype' type constructors with their refined types.@@ -247,6 +248,7 @@ x <> y = SpSig { gsTySigs = gsTySigs x <> gsTySigs y , gsAsmSigs = gsAsmSigs x <> gsAsmSigs y+ , gsAsmReflects = gsAsmReflects x <> gsAsmReflects y , gsRefSigs = gsRefSigs x <> gsRefSigs y , gsInSigs = gsInSigs x <> gsInSigs y , gsNewTypes = gsNewTypes x <> gsNewTypes y@@ -264,7 +266,7 @@ instance Monoid GhcSpecSig where- mempty = SpSig mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty+ mempty = SpSig mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty data GhcSpecData = SpData { gsCtors :: ![(Var, LocSpecType)] -- ^ Data Constructor Measure Sigs@@ -391,6 +393,7 @@ , impSigs :: ![(F.Symbol, F.Sort)] -- ^ Imported variables types , expSigs :: ![(F.Symbol, F.Sort)] -- ^ Exported variables types , asmSigs :: ![(F.LocSymbol, ty)] -- ^ Assumed (unchecked) types; including reflected signatures+ , asmReflectSigs :: ![(F.LocSymbol, F.LocSymbol)] -- ^ Assume reflects : left is the actual function and right the pretended one , sigs :: ![(F.LocSymbol, ty)] -- ^ Imported functions and types , localSigs :: ![(F.LocSymbol, ty)] -- ^ Local type signatures , reflSigs :: ![(F.LocSymbol, ty)] -- ^ Reflected type signatures@@ -451,6 +454,7 @@ , impSigs = impSigs s1 ++ impSigs s2 , expSigs = expSigs s1 ++ expSigs s2 , asmSigs = asmSigs s1 ++ asmSigs s2+ , asmReflectSigs = asmReflectSigs s1 ++ asmReflectSigs s2 , sigs = sigs s1 ++ sigs s2 , localSigs = localSigs s1 ++ localSigs s2 , reflSigs = reflSigs s1 ++ reflSigs s2@@ -500,6 +504,7 @@ , impSigs = [] , expSigs = [] , asmSigs = []+ , asmReflectSigs = [] , sigs = [] , localSigs = [] , reflSigs = []@@ -575,6 +580,8 @@ -- ^ Exported variables types , liftedAsmSigs :: HashSet (F.LocSymbol, LocBareType) -- ^ Assumed (unchecked) types; including reflected signatures+ , liftedAsmReflectSigs :: HashSet (F.LocSymbol, F.LocSymbol)+ -- ^ Reflected assumed signatures , liftedSigs :: HashSet (F.LocSymbol, LocBareType) -- ^ Imported functions and types , liftedInvariants :: HashSet (Maybe F.LocSymbol, LocBareType)@@ -632,6 +639,7 @@ , liftedImpSigs = mempty , liftedExpSigs = mempty , liftedAsmSigs = mempty+ , liftedAsmReflectSigs = mempty , liftedSigs = mempty , liftedInvariants = mempty , liftedIaliases = mempty@@ -810,6 +818,7 @@ , liftedImpSigs = S.fromList . impSigs $ a , liftedExpSigs = S.fromList . expSigs $ a , liftedAsmSigs = S.fromList . asmSigs $ a+ , liftedAsmReflectSigs = S.fromList . asmReflectSigs $ a , liftedSigs = S.fromList . sigs $ a , liftedInvariants = S.fromList . invariants $ a , liftedIaliases = S.fromList . ialiases $ a@@ -844,6 +853,7 @@ , impSigs = S.toList . liftedImpSigs $ a , expSigs = S.toList . liftedExpSigs $ a , asmSigs = S.toList . liftedAsmSigs $ a+ , asmReflectSigs = S.toList . liftedAsmReflectSigs $ a , sigs = S.toList . liftedSigs $ a , localSigs = mempty , reflSigs = mempty
src/Language/Haskell/Liquid/UX/DiffCheck.hs view
@@ -48,7 +48,7 @@ import qualified Data.HashMap.Strict as M import qualified Data.List as L import System.Directory (copyFile, doesFileExist)-import Language.Fixpoint.Types (atLoc, FixResult (..), SourcePos(..), safeSourcePos, unPos)+import Language.Fixpoint.Types (atLoc, FixResult (..), SourcePos(..), unPos) -- import qualified Language.Fixpoint.Misc as Misc import Language.Fixpoint.Utils.Files import Language.Fixpoint.Solver.Stats ()@@ -567,22 +567,6 @@ -------------------------------------------------------------------------------- -- | Aeson instances ----------------------------------------------------------- ----------------------------------------------------------------------------------instance ToJSON SourcePos where- toJSON p = object [ "sourceName" .= f- , "sourceLine" .= unPos l- , "sourceColumn" .= unPos c- ]- where- f = sourceName p- l = sourceLine p- c = sourceColumn p--instance FromJSON SourcePos where- parseJSON (Object v) = safeSourcePos <$> v .: "sourceName"- <*> v .: "sourceLine"- <*> v .: "sourceColumn"- parseJSON _ = mempty instance FromJSON ErrorResult
+ tests/specfiles/pos/Empty.spec view
@@ -0,0 +1,1 @@+module spec Empty where
+ tests/specfiles/pos/T707.spec view
@@ -0,0 +1,17 @@+module spec T707 where++uncons+ :: i : Data.ByteString.ByteString+ -> Maybe (Data.Word.Word8, { o : Data.ByteString.ByteString | bslen o == bslen i - 1 })++unsnoc+ :: i : Data.ByteString.ByteString+ -> Maybe ({ o : Data.ByteString.ByteString | bslen o == bslen i - 1 }, Data.Word.Word8)++uncons'+ :: i : Data.ByteString.ByteString+ -> (Maybe (Data.Word.Word8, { o : Data.ByteString.ByteString | bslen o == bslen i - 1 }))++unsnoc'+ :: i : Data.ByteString.ByteString+ -> (Maybe ({ o : Data.ByteString.ByteString | bslen o == bslen i - 1 }, Data.Word.Word8))
+ tests/specfiles/pos/T788.spec view
@@ -0,0 +1,26 @@+module spec T788 where++import GHC.Base++measure mvlen :: Data.Vector.MVector s a -> Int++invariant {v:Data.Vector.MVector s a | 0 <= mvlen v }++assume length :: forall a. x:(Data.Vector.MVector s a) -> {v : Nat | v = mvlen x }++assume unsafeRead :: Control.Monad.Primitive.PrimMonad m+ => x:(Data.Vector.MVector (Control.Monad.Primitive.PrimState m) a)+ -> ix:{v:Nat | v < mvlen x }+ -> m a++assume unsafeWrite :: Control.Monad.Primitive.PrimMonad m+ => x:(Data.Vector.MVector (Control.Monad.Primitive.PrimState m) a)+ -> ix:{v:Nat | v < mvlen x }+ -> a+ -> m ()++assume unsafeSwap :: Control.Monad.Primitive.PrimMonad m+ => x:(Data.Vector.MVector (Control.Monad.Primitive.PrimState m) a)+ -> i:{v:Nat | v < mvlen x }+ -> j:{v:Nat | v < mvlen x }+ -> m ()
+ tests/specfiles/pos/T924.spec view
@@ -0,0 +1,381 @@+module spec T924 where++measure bslen :: Data.ByteString.ByteString -> { n : Int | 0 <= n }++invariant { bs : Data.ByteString.ByteString | 0 <= bslen bs }++empty :: { bs : Data.ByteString.ByteString | bslen bs == 0 }++singleton+ :: Data.Word.Word8 -> { bs : Data.ByteString.ByteString | bslen bs == 1 }++pack+ :: w8s : [Data.Word.Word8]+ -> { bs : Data.ByteString.ByteString | bslen bs == len w8s }++unpack+ :: bs : Data.ByteString.ByteString+ -> { w8s : [Data.Word.Word8] | len w8s == bslen bs }++cons+ :: Data.Word.Word8+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i + 1 }++snoc+ :: i : Data.ByteString.ByteString+ -> Data.Word.Word8+ -> { o : Data.ByteString.ByteString | bslen o == bslen i + 1 }++append+ :: l : Data.ByteString.ByteString+ -> r : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen l + bslen r }++head :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> Data.Word.Word8++unsnoc+ :: i : Data.ByteString.ByteString+ -> Maybe ({ o : Data.ByteString.ByteString | bslen o == bslen i - 1 }, Data.Word.Word8)++last :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> Data.Word.Word8++tail :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> Data.Word.Word8++init :: {i:Data.ByteString.ByteString | 1 <= bslen i } + -> {o:Data.ByteString.ByteString | bslen o == bslen i - 1 }++null+ :: bs : Data.ByteString.ByteString+ -> { b : Bool | b <=> bslen bs == 0 }++length :: bs : Data.ByteString.ByteString -> { n : Int | bslen bs == n }++map+ :: (Data.Word.Word8 -> Data.Word.Word8)+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++reverse+ :: i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++intersperse+ :: Data.Word.Word8+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | (bslen i == 0 <=> bslen o == 0) && (1 <= bslen i <=> bslen o == 2 * bslen i - 1) }++intercalate+ :: l : Data.ByteString.ByteString+ -> rs : [Data.ByteString.ByteString]+ -> { o : Data.ByteString.ByteString | len rs == 0 ==> bslen o == 0 }++transpose+ :: is : [Data.ByteString.ByteString]+ -> { os : [{ bs : Data.ByteString.ByteString | bslen bs <= len is }] | len is == 0 ==> len os == 0}++foldl1+ :: (Data.Word.Word8 -> Data.Word.Word8 -> Data.Word.Word8)+ -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> Data.Word.Word8++foldl1'+ :: (Data.Word.Word8 -> Data.Word.Word8 -> Data.Word.Word8)+ -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> Data.Word.Word8++foldr1+ :: (Data.Word.Word8 -> Data.Word.Word8 -> Data.Word.Word8)+ -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> Data.Word.Word8++foldr1'+ :: (Data.Word.Word8 -> Data.Word.Word8 -> Data.Word.Word8)+ -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }+ -> Data.Word.Word8++concat+ :: is : [Data.ByteString.ByteString]+ -> { o : Data.ByteString.ByteString | len is == 0 ==> bslen o }++concatMap+ :: (Data.Word.Word8 -> Data.ByteString.ByteString)+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen i == 0 ==> bslen o == 0 }++any :: (Data.Word.Word8 -> Bool)+ -> bs : Data.ByteString.ByteString+ -> { b : Bool | bslen bs == 0 ==> not b }++all :: (Data.Word.Word8 -> Bool)+ -> bs : Data.ByteString.ByteString+ -> { b : Bool | bslen bs == 0 ==> b }++maximum+ :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> Data.Word.Word8++minimum+ :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> Data.Word.Word8++scanl+ :: (Data.Word.Word8 -> Data.Word.Word8 -> Data.Word.Word8)+ -> Data.Word.Word8+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++scanl1+ :: (Data.Word.Word8 -> Data.Word.Word8 -> Data.Word.Word8)+ -> i : { i : Data.ByteString.ByteString | 1 <= bslen i }+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++scanr+ :: (Data.Word.Word8 -> Data.Word.Word8 -> Data.Word.Word8)+ -> Data.Word.Word8+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++scanr1+ :: (Data.Word.Word8 -> Data.Word.Word8 -> Data.Word.Word8)+ -> i : { i : Data.ByteString.ByteString | 1 <= bslen i }+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++mapAccumL+ :: (acc -> Data.Word.Word8 -> (acc, Data.Word.Word8))+ -> acc+ -> i : Data.ByteString.ByteString+ -> (acc, { o : Data.ByteString.ByteString | bslen o == bslen i })++mapAccumR+ :: (acc -> Data.Word.Word8 -> (acc, Data.Word.Word8))+ -> acc+ -> i : Data.ByteString.ByteString+ -> (acc, { o : Data.ByteString.ByteString | bslen o == bslen i })++replicate+ :: n : Int+ -> Data.Word.Word8+ -> { bs : Data.ByteString.ByteString | bslen bs == n }++unfoldrN+ :: n : Int+ -> (a -> Maybe (Data.Word.Word8, a))+ -> a+ -> ({ bs : Data.ByteString.ByteString | bslen bs <= n }, Maybe a)++take+ :: n : Int+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | (n <= 0 <=> bslen o == 0) &&+ ((0 <= n && n <= bslen i) <=> bslen o == n) &&+ (bslen i <= n <=> bslen o = bslen i) }++drop+ :: n : Int+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | (n <= 0 <=> bslen o == bslen i) &&+ ((0 <= n && n <= bslen i) <=> bslen o == bslen i - n) &&+ (bslen i <= n <=> bslen o == 0) }++splitAt+ :: n : Int+ -> i : Data.ByteString.ByteString+ -> ( { l : Data.ByteString.ByteString | (n <= 0 <=> bslen l == 0) &&+ ((0 <= n && n <= bslen i) <=> bslen l == n) &&+ (bslen i <= n <=> bslen l == bslen i) }+ , { r : Data.ByteString.ByteString | (n <= 0 <=> bslen r == bslen i) &&+ ((0 <= n && n <= bslen i) <=> bslen r == bslen i - n) &&+ (bslen i <= n <=> bslen r == 0) }+ )++takeWhile+ :: (Data.Word.Word8 -> Bool)+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o <= bslen i }++dropWhile+ :: (Data.Word.Word8 -> Bool)+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o <= bslen i }++span+ :: (Data.Word.Word8 -> Bool)+ -> i : Data.ByteString.ByteString+ -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }+ , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ )++spanEnd+ :: (Data.Word.Word8 -> Bool)+ -> i : Data.ByteString.ByteString+ -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }+ , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ )++break+ :: (Data.Word.Word8 -> Bool)+ -> i : Data.ByteString.ByteString+ -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }+ , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ )++breakEnd+ :: (Data.Word.Word8 -> Bool)+ -> i : Data.ByteString.ByteString+ -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }+ , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ )++group+ :: i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | 1 <= bslen o && bslen o <= bslen i }]++groupBy+ :: (Data.Word.Word8 -> Data.Word.Word8 -> Bool)+ -> i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | 1 <= bslen o && bslen o <= bslen i }]++inits+ :: i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]++tails+ :: i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]++split+ :: Data.Word.Word8+ -> i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]++splitWith+ :: (Data.Word.Word8 -> Bool)+ -> i : Data.ByteString.ByteString+ -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]++isPrefixOf+ :: l : Data.ByteString.ByteString+ -> r : Data.ByteString.ByteString+ -> { b : Bool | bslen l >= bslen r ==> not b }++isSuffixOf+ :: l : Data.ByteString.ByteString+ -> r : Data.ByteString.ByteString+ -> { b : Bool | bslen l > bslen r ==> not b }++isInfixOf+ :: l : Data.ByteString.ByteString+ -> r : Data.ByteString.ByteString+ -> { b : Bool | bslen l > bslen r ==> not b }++breakSubstring+ :: il : Data.ByteString.ByteString+ -> ir : Data.ByteString.ByteString+ -> ( { ol : Data.ByteString.ByteString | bslen ol <= bslen ir && (bslen il > bslen ir ==> bslen ol == bslen ir)}+ , { or : Data.ByteString.ByteString | bslen or <= bslen ir && (bslen il > bslen ir ==> bslen or == 0) }+ )++elem+ :: Data.Word.Word8+ -> bs : Data.ByteString.ByteString+ -> { b : Bool | bslen b == 0 ==> not b }++notElem+ :: Data.Word.Word8+ -> bs : Data.ByteString.ByteString+ -> { b : Bool | bslen b == 0 ==> b }++find+ :: (Data.Word.Word8 -> Bool)+ -> bs : Data.ByteString.ByteString+ -> Maybe { w8 : Data.Word.Word8 | bslen bs /= 0 }++filter+ :: (Data.Word.Word8 -> Bool)+ -> i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o <= bslen i }++partition+ :: (Data.Word.Word8 -> Bool)+ -> i : Data.ByteString.ByteString+ -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }+ , { r : Data.ByteString.ByteString | bslen r <= bslen i }+ )++index+ :: bs : Data.ByteString.ByteString+ -> { n : Int | 0 <= n && n < bslen bs }+ -> Data.Word.Word8++elemIndex+ :: Data.Word.Word8+ -> bs : Data.ByteString.ByteString+ -> Maybe { n : Int | 0 <= n && n < bslen bs }++elemIndices+ :: Data.Word.Word8+ -> bs : Data.ByteString.ByteString+ -> [{ n : Int | 0 <= n && n < bslen bs }]++elemIndexEnd+ :: Data.Word.Word8+ -> bs : Data.ByteString.ByteString+ -> Maybe { n : Int | 0 <= n && n < bslen bs }++findIndex+ :: (Data.Word.Word8 -> Bool)+ -> bs : Data.ByteString.ByteString+ -> Maybe { n : Int | 0 <= n && n < bslen bs }++findIndices+ :: (Data.Word.Word8 -> Bool)+ -> bs : Data.ByteString.ByteString+ -> [{ n : Int | 0 <= n && n < bslen bs }]++count+ :: Data.Word.Word8+ -> bs : Data.ByteString.ByteString+ -> { n : Int | 0 <= n && n < bslen bs }++zip+ :: l : Data.ByteString.ByteString+ -> r : Data.ByteString.ByteString+ -> { o : [(Data.Word.Word8, Data.Word.Word8)] | len o <= bslen l && len o <= bslen r }++zipWith+ :: (Data.Word.Word8 -> Data.Word.Word8 -> a)+ -> l : Data.ByteString.ByteString+ -> r : Data.ByteString.ByteString+ -> { o : [a] | len o <= bslen l && len o <= bslen r }++unzip+ :: i : [(Data.Word.Word8, Data.Word.Word8)]+ -> ( { l : Data.ByteString.ByteString | bslen l == len i }+ , { r : Data.ByteString.ByteString | bslen r == len i }+ )++sort+ :: i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++copy+ :: i : Data.ByteString.ByteString+ -> { o : Data.ByteString.ByteString | bslen o == bslen i }++hGet+ :: System.IO.Handle+ -> n : { n : Int | 0 <= n }+ -> IO { bs : Data.ByteString.ByteString | bslen bs == n || bslen bs == 0 }++hGetSome+ :: System.IO.Handle+ -> n : { n : Int | 0 <= n }+ -> IO { bs : Data.ByteString.ByteString | bslen bs <= n }++hGetNonBlocking+ :: System.IO.Handle+ -> n : { n : Int | 0 <= n }+ -> IO { bs : Data.ByteString.ByteString | bslen bs <= n }++uncons+ :: i : Data.ByteString.ByteString+ -> Maybe (Data.Word.Word8, { o : Data.ByteString.ByteString | bslen o == bslen i - 1 })