diff --git a/liquidhaskell-boot.cabal b/liquidhaskell-boot.cabal --- a/liquidhaskell-boot.cabal +++ b/liquidhaskell-boot.cabal @@ -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 diff --git a/src-ghc/Liquid/GHC/API.hs b/src-ghc/Liquid/GHC/API.hs --- a/src-ghc/Liquid/GHC/API.hs +++ b/src-ghc/Liquid/GHC/API.hs @@ -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 ) diff --git a/src/Language/Haskell/Liquid/Bare.hs b/src/Language/Haskell/Liquid/Bare.hs --- a/src/Language/Haskell/Liquid/Bare.hs +++ b/src/Language/Haskell/Liquid/Bare.hs @@ -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)])] diff --git a/src/Language/Haskell/Liquid/Bare/Axiom.hs b/src/Language/Haskell/Liquid/Bare/Axiom.hs --- a/src/Language/Haskell/Liquid/Bare/Axiom.hs +++ b/src/Language/Haskell/Liquid/Bare/Axiom.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/Bare/Check.hs b/src/Language/Haskell/Liquid/Bare/Check.hs --- a/src/Language/Haskell/Liquid/Bare/Check.hs +++ b/src/Language/Haskell/Liquid/Bare/Check.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/Bare/Elaborate.hs b/src/Language/Haskell/Liquid/Bare/Elaborate.hs --- a/src/Language/Haskell/Liquid/Bare/Elaborate.hs +++ b/src/Language/Haskell/Liquid/Bare/Elaborate.hs @@ -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 . 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 diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs --- a/src/Language/Haskell/Liquid/Constraint/Generate.hs +++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/Parse.hs b/src/Language/Haskell/Liquid/Parse.hs --- a/src/Language/Haskell/Liquid/Parse.hs +++ b/src/Language/Haskell/Liquid/Parse.hs @@ -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 ------------------------------------------------------ diff --git a/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs b/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs --- a/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs +++ b/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs @@ -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)) diff --git a/src/Language/Haskell/Liquid/Types/Specs.hs b/src/Language/Haskell/Liquid/Types/Specs.hs --- a/src/Language/Haskell/Liquid/Types/Specs.hs +++ b/src/Language/Haskell/Liquid/Types/Specs.hs @@ -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 diff --git a/src/Language/Haskell/Liquid/UX/DiffCheck.hs b/src/Language/Haskell/Liquid/UX/DiffCheck.hs --- a/src/Language/Haskell/Liquid/UX/DiffCheck.hs +++ b/src/Language/Haskell/Liquid/UX/DiffCheck.hs @@ -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 diff --git a/tests/specfiles/pos/Empty.spec b/tests/specfiles/pos/Empty.spec new file mode 100644 --- /dev/null +++ b/tests/specfiles/pos/Empty.spec @@ -0,0 +1,1 @@ +module spec Empty where diff --git a/tests/specfiles/pos/T707.spec b/tests/specfiles/pos/T707.spec new file mode 100644 --- /dev/null +++ b/tests/specfiles/pos/T707.spec @@ -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)) diff --git a/tests/specfiles/pos/T788.spec b/tests/specfiles/pos/T788.spec new file mode 100644 --- /dev/null +++ b/tests/specfiles/pos/T788.spec @@ -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 () diff --git a/tests/specfiles/pos/T924.spec b/tests/specfiles/pos/T924.spec new file mode 100644 --- /dev/null +++ b/tests/specfiles/pos/T924.spec @@ -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 })