diff --git a/liquid-prelude/src/Language/Haskell/Liquid/Foreign.hs b/liquid-prelude/src/Language/Haskell/Liquid/Foreign.hs index 47a0871c7b..0bfa060e3c 100644 --- a/liquid-prelude/src/Language/Haskell/Liquid/Foreign.hs +++ b/liquid-prelude/src/Language/Haskell/Liquid/Foreign.hs @@ -35,7 +35,7 @@ cSizeInt :: CSize -> Int cSizeInt = fromIntegral -{-@ assume mkPtr :: x:GHC.Prim.Addr# -> {v: (Ptr b) | ((plen v) = (addrLen x) && ((plen v) >= 0)) } @-} +{-@ assume mkPtr :: x:Addr# -> {v: (Ptr b) | ((plen v) = (addrLen x) && ((plen v) >= 0)) } @-} mkPtr :: Addr# -> Ptr b mkPtr = undefined -- Ptr x diff --git a/liquidhaskell-boot/liquidhaskell-boot.cabal b/liquidhaskell-boot/liquidhaskell-boot.cabal index 82d77c665f..c33813ef79 100644 --- a/liquidhaskell-boot/liquidhaskell-boot.cabal +++ b/liquidhaskell-boot/liquidhaskell-boot.cabal @@ -74,6 +74,7 @@ library Language.Haskell.Liquid.GHC.Plugin Language.Haskell.Liquid.GHC.Plugin.Tutorial Language.Haskell.Liquid.LawInstances + Language.Haskell.Liquid.LHNameResolution Language.Haskell.Liquid.Liquid Language.Haskell.Liquid.Measure Language.Haskell.Liquid.Misc @@ -124,6 +125,7 @@ library build-depends: base >= 4.11.1.0 && < 5 , Diff >= 0.3 && < 0.6 + , array , aeson , binary , bytestring >= 0.10 diff --git a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs index 6100703442..93d971783b 100644 --- a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs +++ b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs @@ -204,6 +204,7 @@ import GHC.Builtin.Types as Ghc , intTyCon , intTyConName , liftedTypeKind + , liftedTypeKindTyConName , listTyCon , listTyConName , naturalTy @@ -214,7 +215,9 @@ import GHC.Builtin.Types as Ghc , trueDataConId , tupleDataCon , tupleTyCon + , tupleTyConName , typeSymbolKind + , unrestrictedFunTyConName ) import GHC.Builtin.Types.Prim as Ghc ( isArrowTyCon @@ -293,6 +296,7 @@ import GHC.Core.DataCon as Ghc , dataConWrapId , dataConWrapId_maybe , isTupleDataCon + , promoteDataCon ) import GHC.Core.FamInstEnv as Ghc ( FamFlavor(DataFamilyInst) @@ -403,6 +407,7 @@ import GHC.Data.FastString as Ghc , bytesFS , concatFS , fsLit + , lexicalCompareFS , mkFastString , mkFastStringByteString , mkPtrString# @@ -433,7 +438,8 @@ import GHC.HsToCore.Monad as Ghc ( DsM, initDsTc, initDsWithModGuts, newUnique ) import GHC.Iface.Syntax as Ghc ( IfaceAnnotation(ifAnnotatedValue) ) -import GHC.Plugins as Ghc ( deserializeWithData +import GHC.Plugins as Ghc ( Serialized(Serialized) + , deserializeWithData , fromSerialized , toSerialized , defaultPlugin @@ -450,7 +456,7 @@ import GHC.Core.Opt.OccurAnal as Ghc import GHC.Core.TyCo.FVs as Ghc (tyCoVarsOfCo, tyCoVarsOfType) import GHC.Driver.Backend as Ghc (interpreterBackend) import GHC.Driver.Env as Ghc - ( HscEnv(hsc_mod_graph, hsc_unit_env, hsc_dflags, hsc_plugins) + ( HscEnv(hsc_NC, hsc_mod_graph, hsc_unit_env, hsc_dflags, hsc_plugins) , Hsc , hscSetFlags, hscUpdateFlags ) @@ -467,6 +473,8 @@ import GHC.Hs as Ghc ) import GHC.HsToCore.Expr as Ghc ( dsLExpr ) +import GHC.Iface.Binary as Ghc + ( TraceBinIFace(QuietBinIFace), getWithUserData, putWithUserData ) import GHC.Iface.Errors.Ppr as Ghc ( missingInterfaceErrorDiagnostic ) import GHC.Iface.Load as Ghc @@ -501,6 +509,8 @@ import GHC.Tc.Types.Origin as Ghc (lexprCtOrigin) import GHC.Tc.Utils.Monad as Ghc ( captureConstraints , discardConstraints + , getGblEnv + , setGblEnv , getEnv , getTopEnv , failIfErrsM @@ -537,6 +547,7 @@ import GHC.Types.Basic as Ghc , PprPrec , PromotionFlag(NotPromoted) , TopLevelFlag(NotTopLevel) + , TupleSort(BoxedTuple) , funPrec , InlinePragma(inl_act, inl_inline, inl_rule, inl_sat, inl_src) , isDeadOcc @@ -597,6 +608,7 @@ import GHC.Types.Name as Ghc , getSrcSpan , isInternalName , isSystemName + , isTupleTyConName , mkInternalName , mkSystemName , mkTcOcc @@ -604,19 +616,35 @@ import GHC.Types.Name as Ghc , mkVarOcc , mkVarOccFS , nameModule_maybe + , nameNameSpace , nameOccName , nameSrcLoc , nameStableString + , nameUnique , occNameFS , occNameString , stableNameCmp ) +import GHC.Types.Name.Cache as Ghc (NameCache) +import GHC.Types.Name.Occurrence as Ghc + ( NameSpace + , isFieldNameSpace + , mkOccName + , dataName + , tcName + ) import GHC.Types.Name.Reader as Ghc - ( ImpItemSpec(ImpAll) + ( GlobalRdrEnv + , ImpItemSpec(ImpAll) + , LookupGRE(LookupRdrName) + , WhichGREs(SameNameSpace) , getRdrName , globalRdrEnvElts , greName + , lookupGRE , mkQual + , mkRdrQual + , mkRdrUnqual , mkVarUnqual , mkUnqual , nameRdrName @@ -692,6 +720,7 @@ import GHC.Unit.Module as Ghc , IsBootInterface(NotBoot, IsBoot) , ModuleNameWithIsBoot , UnitId + , stableModuleCmp , fsToUnit , mkModuleNameFS , moduleNameFS @@ -710,6 +739,14 @@ import GHC.Unit.Module.ModGuts as Ghc , mg_usages ) ) +import GHC.Utils.Binary as Ghc + ( Binary(get, put_) + , getByte + , openBinMem + , putByte + , unsafeUnpackBinBuffer + , withBinBuffer + ) import GHC.Utils.Error as Ghc (pprLocMsgEnvelope, withTiming) import GHC.Utils.Logger as Ghc (Logger(logFlags), putLogMsg) import GHC.Utils.Outputable as Ghc hiding ((<>)) diff --git a/liquidhaskell-boot/src-ghc/Liquid/GHC/API/StableModule.hs b/liquidhaskell-boot/src-ghc/Liquid/GHC/API/StableModule.hs index 72568af491..b287b9bf1d 100644 --- a/liquidhaskell-boot/src-ghc/Liquid/GHC/API/StableModule.hs +++ b/liquidhaskell-boot/src-ghc/Liquid/GHC/API/StableModule.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveDataTypeable #-} {-# OPTIONS_GHC -Wno-orphans #-} @@ -16,6 +17,7 @@ module Liquid.GHC.API.StableModule ( import qualified GHC import qualified GHC.Unit.Types as GHC import qualified GHC.Unit.Module as GHC +import Data.Data (Data) import Data.Hashable import GHC.Generics hiding (to, moduleName) import Data.Binary @@ -27,7 +29,7 @@ import Data.Binary -- newtype StableModule = StableModule { unStableModule :: GHC.Module } - deriving Generic + deriving (Data, Generic) -- | Converts a 'Module' into a 'StableModule'. toStableModule :: GHC.Module -> StableModule diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs index f0508a5733..595632bfe8 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs @@ -26,6 +26,7 @@ import Control.Monad (forM, mplus, when) import Control.Applicative ((<|>)) import qualified Control.Exception as Ex import qualified Data.Binary as B +import Data.IORef (newIORef) import qualified Data.Maybe as Mb import qualified Data.List as L import qualified Data.HashMap.Strict as M @@ -191,7 +192,10 @@ makeGhcSpec :: Config -> Ghc.TcRn (Either Diagnostics ([Warning], GhcSpec)) ------------------------------------------------------------------------------------- makeGhcSpec cfg src lmap targetSpec dependencySpecs = do - (dg0, sp) <- makeGhcSpec0 cfg src lmap targetSpec dependencySpecs + hscEnv <- Ghc.getTopEnv + session <- Ghc.Session <$> Ghc.liftIO (newIORef hscEnv) + tcg <- Ghc.getGblEnv + (dg0, sp) <- makeGhcSpec0 cfg session tcg src lmap targetSpec dependencySpecs let diagnostics = Bare.checkTargetSpec (targetSpec : map snd dependencySpecs) (toTargetSrc src) (ghcSpecEnv sp) @@ -231,12 +235,14 @@ ghcSpecEnv sp = F.notracepp "RENV" $ fromListSEnv binds ------------------------------------------------------------------------------------- makeGhcSpec0 :: Config + -> Ghc.Session + -> Ghc.TcGblEnv -> GhcSrc -> LogicMap -> Ms.BareSpec -> [(ModName, Ms.BareSpec)] -> Ghc.TcRn (Diagnostics, GhcSpec) -makeGhcSpec0 cfg src lmap targetSpec dependencySpecs = do +makeGhcSpec0 cfg session tcg src lmap targetSpec dependencySpecs = do -- build up environments tycEnv <- makeTycEnv1 name env (tycEnv0, datacons) coreToLg simplifier let tyi = Bare.tcTyConMap tycEnv @@ -356,10 +362,10 @@ makeGhcSpec0 cfg src lmap targetSpec dependencySpecs = do else (targetSpec, []) mySpec1 = mySpec0 <> lSpec0 lSpec0 = makeLiftedSpec0 cfg src embs lmap mySpec0 - embs = makeEmbeds src env ((name, mySpec0) : dependencySpecs) + embs = makeEmbeds src env (mySpec0 : map snd dependencySpecs) dm = Bare.tcDataConMap tycEnv0 (dg0, datacons, tycEnv0) = makeTycEnv0 cfg name env embs mySpec2 iSpecs2 - env = Bare.makeEnv cfg src lmap ((name, targetSpec) : dependencySpecs) + env = Bare.makeEnv cfg session tcg src lmap ((name, targetSpec) : dependencySpecs) -- check barespecs name = F.notracepp ("ALL-SPECS" ++ zzz) $ _giTargetMod src zzz = F.showpp (fst <$> mspecs) @@ -369,17 +375,17 @@ makeImports specs = concatMap (expSigs . snd) specs' where specs' = filter (isSrcImport . fst) specs -makeEmbeds :: GhcSrc -> Bare.Env -> [(ModName, Ms.BareSpec)] -> F.TCEmb Ghc.TyCon +makeEmbeds :: GhcSrc -> Bare.Env -> [Ms.BareSpec] -> F.TCEmb Ghc.TyCon makeEmbeds src env = Bare.addClassEmbeds (_gsCls src) (_gsFiTcs src) . mconcat . map (makeTyConEmbeds env) -makeTyConEmbeds :: Bare.Env -> (ModName, Ms.BareSpec) -> F.TCEmb Ghc.TyCon -makeTyConEmbeds env (name, spec) +makeTyConEmbeds :: Bare.Env -> Ms.BareSpec -> F.TCEmb Ghc.TyCon +makeTyConEmbeds env spec = F.tceFromList [ (tc, t) | (c,t) <- F.tceToList (Ms.embeds spec), tc <- symTc c ] where - symTc = Mb.maybeToList . Bare.maybeResolveSym env name "embed-tycon" + symTc = Mb.maybeToList . either (const Nothing) Just . Bare.matchTyCon env -------------------------------------------------------------------------------- -- | [NOTE]: REFLECT-IMPORTS diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Class.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Class.hs index ae989b6e9e..039e7bd82a 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Class.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Class.hs @@ -149,7 +149,7 @@ makeCLaws env sigEnv myName specs = do return (Mb.catMaybes zMbs) where err tc = error ("Not a type class: " ++ F.showpp tc) - classTc = Bare.maybeResolveSym env myName "makeClass" . btc_tc . rcName + classTc = either (const Nothing) Just . Bare.matchTyCon env . btc_tc . rcName classTcs = [ (name, cls, tc) | (name, spec) <- M.toList specs , cls <- Ms.claws spec , tc <- Mb.maybeToList (classTc cls) @@ -167,7 +167,7 @@ makeClasses env sigEnv myName specs = do classTcs = [ (name, cls, tc) | (name, spec) <- M.toList specs , cls <- Ms.classes spec , tc <- Mb.maybeToList (classTc cls) ] - classTc = Bare.maybeResolveSym env myName "makeClass" . btc_tc . rcName + classTc = either (const Nothing) Just . Bare.matchTyCon env . btc_tc . rcName mkClass :: Bare.Env -> Bare.SigEnv -> ModName -> ModName -> RClass LocBareType -> Ghc.TyCon -> Bare.Lookup (Maybe (DataConP, [(ModName, Ghc.Var, LocSpecType)])) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs index 1f5473ef2a..b1b726c541 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs @@ -34,6 +34,7 @@ import qualified Language.Haskell.Liquid.GHC.Misc as GM import qualified Liquid.GHC.API as Ghc import Language.Haskell.Liquid.Types.DataDecl import Language.Haskell.Liquid.Types.Errors +import Language.Haskell.Liquid.Types.Names import Language.Haskell.Liquid.Types.PredType (dataConPSpecType) import qualified Language.Haskell.Liquid.Types.RefType as RT import Language.Haskell.Liquid.Types.RType @@ -44,7 +45,6 @@ import qualified Language.Fixpoint.Misc as Misc import qualified Language.Haskell.Liquid.Misc as Misc import Language.Haskell.Liquid.Types.Variance import Language.Haskell.Liquid.WiredIn -import Language.Haskell.Liquid.Types.Names (selfSymbol) import qualified Language.Haskell.Liquid.Measure as Ms @@ -418,11 +418,11 @@ makeConTypes'' env name spec dcs vdcs = do return (unzip zong) -type DSizeMap = M.HashMap F.Symbol (F.Symbol, [F.Symbol]) +type DSizeMap = M.HashMap F.Symbol (F.Symbol, [LHName]) normalizeDSize :: [([LocBareType], F.LocSymbol)] -> DSizeMap normalizeDSize ds = M.fromList (concatMap go ds) where go (ts,x) = let xs = Mb.mapMaybe (getTc . val) ts - in [(tc, (val x, xs)) | tc <- xs] + in [(getLHNameSymbol tc, (val x, xs)) | tc <- xs] getTc (RAllT _ t _) = getTc t getTc (RApp c _ _ _) = Just (val $ btc_tc c) getTc _ = Nothing @@ -439,10 +439,10 @@ makeSize smap d | otherwise = d -makeSizeCtor :: (F.Symbol, [F.Symbol]) -> DataCtor -> DataCtor +makeSizeCtor :: (F.Symbol, [LHName]) -> DataCtor -> DataCtor makeSizeCtor (s,xs) d = d {dcFields = fmap (mapBot go) <$> dcFields d} where - go (RApp c ts rs r) | F.symbol c `elem` xs + go (RApp c ts rs r) | val (btc_tc c) `elem` xs = RApp c ts rs (r `meet` rsz) go t = t rsz = MkUReft (F.Reft (F.vv_, F.PAtom F.Lt diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs index ff8955020b..82b590d836 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs @@ -34,7 +34,6 @@ import qualified Control.Exception as Ex import qualified Data.HashMap.Strict as M import qualified Data.Char as Char import qualified Data.List as L -import qualified Text.Printf as Printf import qualified Text.PrettyPrint.HughesPJ as PJ import qualified Language.Fixpoint.Types as F @@ -43,8 +42,10 @@ import qualified Language.Fixpoint.Misc as Misc import Language.Fixpoint.Types (Expr(..)) -- , Symbol, symbol) import qualified Language.Haskell.Liquid.GHC.Misc as GM import qualified Liquid.GHC.API as Ghc +import Language.Haskell.Liquid.LHNameResolution (exprArg) import Language.Haskell.Liquid.Types.Errors import Language.Haskell.Liquid.Types.DataDecl +import Language.Haskell.Liquid.Types.Names import qualified Language.Haskell.Liquid.Types.RefType as RT import Language.Haskell.Liquid.Types.RType import Language.Haskell.Liquid.Types.RTypeOp @@ -219,11 +220,11 @@ genExpandOrder table graph ordNub :: Ord a => [a] -> [a] ordNub = map head . L.group . L.sort -buildTypeEdges :: (F.Symbolic c) => AliasTable x t -> RType c tv r -> [F.Symbol] +buildTypeEdges :: AliasTable x t -> BareType -> [F.Symbol] buildTypeEdges table = ordNub . go where -- go :: t -> [Symbol] - go (RApp c ts rs _) = go_alias (F.symbol c) ++ concatMap go ts ++ concatMap go (mapMaybe go_ref rs) + go (RApp c ts rs _) = go_alias (getLHNameSymbol $ val $ btc_tc c) ++ concatMap go ts ++ concatMap go (mapMaybe go_ref rs) go (RFun _ _ t1 t2 _) = go t1 ++ go t2 go (RAppTy t1 t2 _) = go t1 ++ go t2 go (RAllE _ t1 t2) = go t1 ++ go t2 @@ -413,7 +414,7 @@ expandBareType rtEnv _ = go goRef (RProp ss t) = RProp ss (go t) lookupRTEnv :: BTyCon -> BareRTEnv -> Maybe (Located BareRTAlias) -lookupRTEnv c rtEnv = M.lookup (F.symbol c) (typeAliases rtEnv) +lookupRTEnv c rtEnv = M.lookup (getLHNameSymbol $ val $ btc_tc c) (typeAliases rtEnv) expandRTAliasApp :: F.SourcePos -> Located BareRTAlias -> [BareType] -> RReft -> BareType expandRTAliasApp l (Loc la _ rta) args r = case isOK of @@ -459,31 +460,6 @@ errRTAliasApp l la rta = Just . ErrAliasApp sp name sp' sp' = GM.sourcePosSrcSpan la - --------------------------------------------------------------------------------- --- | exprArg converts a tyVar to an exprVar because parser cannot tell --- this function allows us to treating (parsed) "types" as "value" --- arguments, e.g. type Matrix a Row Col = List (List a Row) Col --- Note that during parsing, we don't necessarily know whether a --- string is a type or a value expression. E.g. in tests/pos/T1189.hs, --- the string `Prop (Ev (plus n n))` where `Prop` is the alias: --- {-@ type Prop E = {v:_ | prop v = E} @-} --- the parser will chomp in `Ev (plus n n)` as a `BareType` and so --- `exprArg` converts that `BareType` into an `Expr`. --------------------------------------------------------------------------------- -exprArg :: F.SourcePos -> String -> BareType -> Expr -exprArg l msg = F.notracepp ("exprArg: " ++ msg) . go - where - go :: BareType -> Expr - go (RExprArg e) = val e - go (RVar x _) = EVar (F.symbol x) - go (RApp x [] [] _) = EVar (F.symbol x) - go (RApp f ts [] _) = F.mkEApp (F.symbol <$> btc_tc f) (go <$> ts) - go (RAppTy t1 t2 _) = F.EApp (go t1) (go t2) - go z = panic sp $ Printf.printf "Unexpected expression parameter: %s in %s" (show z) msg - sp = Just (GM.sourcePosSrcSpan l) - - ---------------------------------------------------------------------------------------- -- | @cookSpecType@ is the central place where a @BareType@ gets processed, -- in multiple steps, into a @SpecType@. See [NOTE:Cooking-SpecType] for diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Laws.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Laws.hs index bd464fe31c..f0cfb480e1 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Laws.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Laws.hs @@ -41,7 +41,8 @@ makeInstanceLaw env sigEnv sigs name rilaw = LawInstance tc = classTc (rilName rilaw) errmsg = error ("Not a type class: " ++ F.showpp tc) - classTc = tyConClass_maybe <=< (Bare.maybeResolveSym env name "makeClass" . btc_tc) + classTc = tyConClass_maybe <=< + either (const Nothing) Just . Bare.matchTyCon env . btc_tc mkTy :: LocBareType -> LocSpecType mkTy = Bare.cookSpecType env sigEnv name Bare.GenTV diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Misc.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Misc.hs index 8bd0f4262b..9bcab521d7 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Misc.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Misc.hs @@ -15,7 +15,7 @@ module Language.Haskell.Liquid.Bare.Misc import Prelude hiding (error) -import Liquid.GHC.API as Ghc hiding (Located, showPpr) +import Liquid.GHC.API as Ghc hiding (Located, get, showPpr) import Control.Monad (zipWithM_) import Control.Monad.Except (MonadError, throwError) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs index 726dec5cfa..9ff72462bf 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs @@ -28,6 +28,7 @@ module Language.Haskell.Liquid.Bare.Resolve , lookupGhcTyCon , lookupGhcVar , lookupGhcNamedVar + , matchTyCon -- * Checking if names exist , knownGhcVar @@ -70,10 +71,12 @@ import qualified Language.Fixpoint.Types as F import qualified Language.Fixpoint.Types.Visitor as F import qualified Language.Fixpoint.Misc as Misc import qualified Liquid.GHC.API as Ghc +import qualified Language.Haskell.Liquid.GHC.Interface as Interface import qualified Language.Haskell.Liquid.GHC.Misc as GM import qualified Language.Haskell.Liquid.Misc as Misc import Language.Haskell.Liquid.Types.DataDecl import Language.Haskell.Liquid.Types.Errors +import Language.Haskell.Liquid.Types.Names import Language.Haskell.Liquid.Types.RType import Language.Haskell.Liquid.Types.RTypeOp import qualified Language.Haskell.Liquid.Types.RefType as RT @@ -85,6 +88,7 @@ import Language.Haskell.Liquid.Bare.Types import Language.Haskell.Liquid.Bare.Misc import Language.Haskell.Liquid.UX.Config import Language.Haskell.Liquid.WiredIn +import System.IO.Unsafe (unsafePerformIO) myTracepp :: (F.PPrint a) => String -> a -> a myTracepp = F.notracepp @@ -95,9 +99,11 @@ type Lookup a = Either [Error] a ------------------------------------------------------------------------------- -- | Creating an environment ------------------------------------------------------------------------------- -makeEnv :: Config -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> Env -makeEnv cfg src lmap specs = RE - { reLMap = lmap +makeEnv :: Config -> Ghc.Session -> Ghc.TcGblEnv -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> Env +makeEnv cfg session tcg src lmap specs = RE + { reSession = session + , reTcGblEnv = tcg + , reLMap = lmap , reSyms = syms , _reSubst = makeVarSubst src , _reTyThings = makeTyThingMap src @@ -915,38 +921,43 @@ ofBRType env name f l = go [] goSyms (x, t) = (x,) <$> ofBSortE env name l t goRApp bs tc ts rs r = bareTCApp <$> goReft bs r <*> lc' <*> mapM (goRef bs) rs <*> mapM (go bs) ts where - lc' = F.atLoc lc <$> matchTyCon env name lc (length ts) + lc' = F.atLoc lc <$> matchTyCon env lc lc = btc_tc tc - -- goRApp _ _ _ _ = impossible Nothing "goRApp failed through to final case" - -{- - -- TODO-REBARE: goRImpF bounds _ (RApp c ps' _ _) t _ - -- TODO-REBARE: | Just bnd <- M.lookup (btc_tc c) bounds - -- TODO-REBARE: = do let (ts', ps) = splitAt (length $ tyvars bnd) ps' - -- TODO-REBARE: ts <- mapM go ts' - -- TODO-REBARE: makeBound bnd ts [x | RVar (BTV x) _ <- ps] <$> go t - -- TODO-REBARE: goRFun bounds _ (RApp c ps' _ _) t _ - -- TODO-REBARE: | Just bnd <- M.lookup (btc_tc c) bounds - -- TODO-REBARE: = do let (ts', ps) = splitAt (length $ tyvars bnd) ps' - -- TODO-REBARE: ts <- mapM go ts' - -- TODO-REBARE: makeBound bnd ts [x | RVar (BTV x) _ <- ps] <$> go t - - -- TODO-REBARE: ofBareRApp env name t@(F.Loc _ _ !(RApp tc ts _ r)) - -- TODO-REBARE: | Loc l _ c <- btc_tc tc - -- TODO-REBARE: , Just rta <- M.lookup c aliases - -- TODO-REBARE: = appRTAlias l rta ts =<< resolveReft r - --} - -matchTyCon :: Env -> ModName -> LocSymbol -> Int -> Lookup Ghc.TyCon -matchTyCon env name lc@(Loc _ _ c) arity - | isList c && arity == 1 = Right Ghc.listTyCon - | isTuple c = Right tuplTc - | otherwise = resolveLocSym env name msg lc - where - msg = "matchTyCon: " ++ F.showpp c - tuplTc = Ghc.tupleTyCon Ghc.Boxed arity +-- | Get the TyCon from an LHName. +-- +-- This function uses 'unsafePerformIO' to lookup the 'Ghc.TyThing' of a 'Ghc.Name'. +-- This should be benign because the result doesn't depend of when exactly this is +-- called. Since this code is intended to be used inside a GHC plugin, there is no +-- danger that GHC is finalized before the result is evaluated. +matchTyCon :: Env -> Located LHName -> Lookup Ghc.TyCon +matchTyCon env lc@(Loc _ _ c0) = unsafePerformIO $ do + case c0 of + LHNUnresolved _ _ -> panic (Just $ GM.fSrcSpan lc) $ "matchTyCon: unresolved name: " ++ show c0 + LHNResolved rn _ -> case rn of + LHRLocal _ -> panic (Just $ GM.fSrcSpan lc) $ "matchTyCon: cannot resolve a local name: " ++ show c0 + LHRIndex i -> panic (Just $ GM.fSrcSpan lc) $ "matchTyCon: cannot resolve a LHRIndex " ++ show i + LHRLogic (LogicName s _) -> panic (Just $ GM.fSrcSpan lc) $ "matchTyCon: cannot resolve a LHRLogic name " ++ show s + LHRGHC n -> do + (_, m) <- Ghc.reflectGhc (Interface.lookupTyThing (reTcGblEnv env) n) (reSession env) + case m of + Just (Ghc.ATyCon tc) -> return (Right tc) + Just (Ghc.AConLike (Ghc.RealDataCon dc)) -> + return $ Right $ Ghc.promoteDataCon dc + Just _ -> return $ Left + [ ErrResolve + (GM.fSrcSpan lc) + "type constructor" + (PJ.text $ show c0) + "not a type constructor" + ] + Nothing -> return $ Left + [ ErrResolve + (GM.fSrcSpan lc) + "type constructor" + (PJ.text $ show c0) + "not found" + ] bareTCApp :: (Expandable r) => r diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Types.hs index 8d27982812..dd19035b38 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Types.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Types.hs @@ -70,16 +70,18 @@ plugSrc _ = Nothing -- | Name resolution environment ------------------------------------------------------------------------------- data Env = RE - { reLMap :: !LogicMap - , reSyms :: ![(F.Symbol, Ghc.Var)] -- ^ see "syms" in old makeGhcSpec' - , _reSubst :: !F.Subst -- ^ see "su" in old makeGhcSpec' - , _reTyThings :: !TyThingMap - , reCfg :: !Config - , reQualImps :: !QImports -- ^ qualified imports - , reAllImps :: !(S.HashSet F.Symbol) -- ^ all imported modules - , reLocalVars :: !LocalVars -- ^ lines at which local variables are defined. - , reGlobSyms :: !(S.HashSet F.Symbol) -- ^ global symbols, typically unlifted measures like 'len', 'fromJust' - , reSrc :: !GhcSrc -- ^ all source info + { reSession :: Ghc.Session + , reTcGblEnv :: Ghc.TcGblEnv + , reLMap :: LogicMap + , reSyms :: [(F.Symbol, Ghc.Var)] -- ^ see "syms" in old makeGhcSpec' + , _reSubst :: F.Subst -- ^ see "su" in old makeGhcSpec' + , _reTyThings :: TyThingMap + , reCfg :: Config + , reQualImps :: QImports -- ^ qualified imports + , reAllImps :: S.HashSet F.Symbol -- ^ all imported modules + , reLocalVars :: LocalVars -- ^ lines at which local variables are defined. + , reGlobSyms :: S.HashSet F.Symbol -- ^ global symbols, typically unlifted measures like 'len', 'fromJust' + , reSrc :: GhcSrc -- ^ all source info } instance HasConfig Env where diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Env.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Env.hs index e65d37ad3b..7872a3c2eb 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Env.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Env.hs @@ -68,7 +68,7 @@ import Language.Fixpoint.SortCheck (pruneUnsortedReft) -import Liquid.GHC.API hiding (panic) +import Liquid.GHC.API hiding (get, panic) import Language.Haskell.Liquid.Types.RefType import qualified Language.Haskell.Liquid.GHC.SpanStack as Sp import Language.Haskell.Liquid.Types.Errors diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Fresh.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Fresh.hs index cd37e18974..d4abb3eaa5 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Fresh.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Fresh.hs @@ -40,7 +40,7 @@ import Language.Haskell.Liquid.Types.Types import Language.Haskell.Liquid.Constraint.Types import qualified Language.Haskell.Liquid.GHC.Misc as GM import Language.Haskell.Liquid.UX.Config -import Liquid.GHC.API as Ghc +import Liquid.GHC.API as Ghc hiding (get) -------------------------------------------------------------------------------- -- | This is all hardwiring stuff to CG ---------------------------------------- diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs index 783fda3a44..43db709325 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs @@ -36,6 +36,7 @@ module Language.Haskell.Liquid.GHC.Interface ( , makeFamInstEnv , clearSpec , checkFilePragmas + , lookupTyThing , lookupTyThings , availableTyThings , updLiftedSpec diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs index f5332685c1..cc11f28c66 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs @@ -29,7 +29,7 @@ import Debug.Trace import Prelude hiding (error) import Liquid.GHC.API as Ghc hiding - (L, line, sourceName, showPpr, panic, showSDoc) + (L, get, line, sourceName, showPpr, panic, showSDoc) import qualified Liquid.GHC.API as Ghc (GenLocated (L)) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs index 301e577371..bd8329378c 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs @@ -7,6 +7,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE TupleSections #-} module Language.Haskell.Liquid.GHC.Plugin ( @@ -21,6 +22,7 @@ import qualified Language.Fixpoint.Types as F import qualified Language.Haskell.Liquid.GHC.Misc as LH import qualified Language.Haskell.Liquid.UX.CmdLine as LH import qualified Language.Haskell.Liquid.GHC.Interface as LH +import Language.Haskell.Liquid.LHNameResolution (collectTypeAliases, resolveLHNames) import qualified Language.Haskell.Liquid.Liquid as LH import qualified Language.Haskell.Liquid.Types.PrettyPrint as LH ( filterReportErrors , filterReportErrorsWith @@ -301,7 +303,7 @@ liquidCheckModule cfg0 ms tcg specs = do env <- getTopEnv session <- Session <$> liftIO (newIORef env) liftIO $ flip reflectGhc session $ mkPipelineData ms tcg specs - liquidLib <- liquidHaskellCheckWithConfig cfg pipelineData ms + liquidLib <- setGblEnv tcg $ liquidHaskellCheckWithConfig cfg pipelineData ms traverse (serialiseSpec tcg) liquidLib where thisFile = LH.modSummaryHsFile ms @@ -347,7 +349,7 @@ serialiseSpec tcGblEnv liquidLib = do -- liftIO $ putStrLn "liquidHaskellCheck 9" -- --- - let serialisedSpec = Serialisation.serialiseLiquidLib liquidLib thisModule + serialisedSpec <- liftIO $ Serialisation.serialiseLiquidLib liquidLib thisModule debugLog $ "Serialised annotation ==> " ++ (O.showSDocUnsafe . O.ppr $ serialisedSpec) -- liftIO $ putStrLn "liquidHaskellCheck 10" @@ -356,9 +358,14 @@ serialiseSpec tcGblEnv liquidLib = do where thisModule = tcg_mod tcGblEnv -processInputSpec :: Config -> PipelineData -> ModSummary -> BareSpec -> TcM (Either LiquidCheckException LiquidLib) +processInputSpec + :: Config + -> PipelineData + -> ModSummary + -> BareSpec + -> TcM (Either LiquidCheckException LiquidLib) processInputSpec cfg pipelineData modSummary inputSpec = do - hscEnv <- env_top <$> getEnv + hscEnv <- getTopEnv debugLog $ " Input spec: \n" ++ show inputSpec debugLog $ "Relevant ===> \n" ++ unlines (renderModule <$> S.toList (relevantModules (hsc_mod_graph hscEnv) modGuts)) @@ -502,15 +509,15 @@ processModule LiquidHaskellContext{..} = do debugLog ("Module ==> " ++ renderModule thisModule) hscEnv <- env_top <$> getEnv - let bareSpec = lhInputSpec + let bareSpec0 = lhInputSpec -- /NOTE/: For the Plugin to work correctly, we shouldn't call 'canonicalizePath', because otherwise -- this won't trigger the \"external name resolution\" as part of 'Language.Haskell.Liquid.Bare.Resolve' -- (cfr. 'allowExtResolution'). let file = LH.modSummaryHsFile lhModuleSummary - _ <- liftIO $ LH.checkFilePragmas $ Ms.pragmas (fromBareSpec bareSpec) + _ <- liftIO $ LH.checkFilePragmas $ Ms.pragmas (fromBareSpec bareSpec0) - withPragmas lhGlobalCfg file (Ms.pragmas $ fromBareSpec bareSpec) $ \moduleCfg -> do + withPragmas lhGlobalCfg file (Ms.pragmas $ fromBareSpec bareSpec0) $ \moduleCfg -> do dependencies <- loadDependencies moduleCfg (S.toList lhRelevantModules) debugLog $ "Found " <> show (HM.size $ getDependencies dependencies) <> " dependencies:" @@ -528,9 +535,15 @@ processModule LiquidHaskellContext{..} = do -- Due to the fact the internals can throw exceptions from pure code at any point, we need to -- call 'evaluate' to force any exception and catch it, if we can. - + tcg <- getGblEnv + let rtAliases = collectTypeAliases thisModule bareSpec0 (HM.toList $ getDependencies dependencies) + eBareSpec = resolveLHNames rtAliases (tcg_rdr_env tcg) bareSpec0 result <- - makeTargetSpec moduleCfg lhModuleLogicMap targetSrc bareSpec dependencies + case eBareSpec of + Left errors -> pure $ Left $ mkDiagnostics [] errors + Right bareSpec -> + fmap (,bareSpec) <$> + makeTargetSpec moduleCfg lhModuleLogicMap targetSrc bareSpec dependencies let continue = pure $ Left (ErrorsOccurred []) reportErrs :: (Show e, F.PPrint e) => [TError e] -> TcRn (Either LiquidCheckException ProcessModuleResult) @@ -541,7 +554,7 @@ processModule LiquidHaskellContext{..} = do Left diagnostics -> do liftIO $ mapM_ (printWarning logger) (allWarnings diagnostics) reportErrs $ allErrors diagnostics - Right (warnings, targetSpec, liftedSpec) -> do + Right ((warnings, targetSpec, liftedSpec), bareSpec) -> do liftIO $ mapM_ (printWarning logger) warnings let targetInfo = TargetInfo targetSrc targetSpec diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/Serialisation.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/Serialisation.hs index 8c42eecf5b..3fb707cd8c 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/Serialisation.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/Serialisation.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE TypeApplications #-} {-# LANGUAGE ScopedTypeVariables #-} module Language.Haskell.Liquid.GHC.Plugin.Serialisation ( -- * Serialising and deserialising things from/to specs. @@ -8,64 +7,134 @@ module Language.Haskell.Liquid.GHC.Plugin.Serialisation ( ) where +import qualified Data.Array as Array import Data.Foldable ( asum ) import Control.Monad import qualified Data.Binary as B -import Data.Binary ( Binary ) +import qualified Data.Binary.Builder as Builder +import qualified Data.Binary.Put as B import qualified Data.ByteString.Lazy as B -import Data.Typeable +import Data.Data (Data) +import Data.Generics (ext0, gmapAccumT) +import Data.HashMap.Strict as M import Data.Maybe ( listToMaybe ) +import Data.Word (Word8) -import Liquid.GHC.API +import qualified Liquid.GHC.API as GHC import Language.Haskell.Liquid.GHC.Plugin.Types (LiquidLib) +import Language.Haskell.Liquid.Types.Names -- -- Serialising and deserialising Specs -- -deserialiseBinaryObjectFromEPS - :: forall a. (Typeable a, Binary a) - => Module - -> ExternalPackageState - -> Maybe a -deserialiseBinaryObjectFromEPS thisModule eps = extractFromEps +getLiquidLibBytesFromEPS + :: GHC.Module + -> GHC.ExternalPackageState + -> Maybe LiquidLibBytes +getLiquidLibBytesFromEPS thisModule eps = extractFromEps where - extractFromEps :: Maybe a - extractFromEps = listToMaybe $ findAnns (B.decode . B.pack) (eps_ann_env eps) (ModuleTarget thisModule) - -deserialiseBinaryObject :: forall a. (Typeable a, Binary a) - => Module - -> ExternalPackageState - -> HomePackageTable - -> Maybe a -deserialiseBinaryObject thisModule eps hpt = - asum [extractFromHpt, deserialiseBinaryObjectFromEPS thisModule eps] + extractFromEps :: Maybe LiquidLibBytes + extractFromEps = listToMaybe $ GHC.findAnns LiquidLibBytes (GHC.eps_ann_env eps) (GHC.ModuleTarget thisModule) + +getLiquidLibBytes :: GHC.Module + -> GHC.ExternalPackageState + -> GHC.HomePackageTable + -> Maybe LiquidLibBytes +getLiquidLibBytes thisModule eps hpt = + asum [extractFromHpt, getLiquidLibBytesFromEPS thisModule eps] where - extractFromHpt :: Maybe a + extractFromHpt :: Maybe LiquidLibBytes extractFromHpt = do - modInfo <- lookupHpt hpt (moduleName thisModule) - guard (thisModule == (mi_module . hm_iface $ modInfo)) - xs <- mapM (fromSerialized deserialise . ifAnnotatedValue) (mi_anns . hm_iface $ modInfo) + modInfo <- GHC.lookupHpt hpt (GHC.moduleName thisModule) + guard (thisModule == (GHC.mi_module . GHC.hm_iface $ modInfo)) + xs <- mapM (GHC.fromSerialized LiquidLibBytes . GHC.ifAnnotatedValue) (GHC.mi_anns . GHC.hm_iface $ modInfo) listToMaybe xs - deserialise :: [B.Word8] -> a - deserialise payload = B.decode (B.pack payload) +newtype LiquidLibBytes = LiquidLibBytes { unLiquidLibBytes :: [Word8] } + +-- | Serialise a 'LiquidLib', removing the termination checks from the target. +serialiseLiquidLib :: LiquidLib -> GHC.Module -> IO GHC.Annotation +serialiseLiquidLib lib thisModule = do + bs <- encodeLiquidLib lib + return $ GHC.Annotation + (GHC.ModuleTarget thisModule) + (GHC.toSerialized unLiquidLibBytes (LiquidLibBytes $ B.unpack bs)) + +deserialiseLiquidLib + :: GHC.Module + -> GHC.ExternalPackageState + -> GHC.HomePackageTable + -> GHC.NameCache + -> IO (Maybe LiquidLib) +deserialiseLiquidLib thisModule eps hpt nameCache = do + let mlibbs = getLiquidLibBytes thisModule eps hpt + case mlibbs of + Just (LiquidLibBytes ws) -> do + let bs = B.pack ws + Just <$> decodeLiquidLib nameCache bs + _ -> return Nothing -serialiseBinaryObject :: forall a. (Binary a, Typeable a) => a -> Module -> Annotation -serialiseBinaryObject obj thisModule = serialised +deserialiseLiquidLibFromEPS + :: GHC.Module + -> GHC.ExternalPackageState + -> GHC.NameCache + -> IO (Maybe LiquidLib) +deserialiseLiquidLibFromEPS thisModule eps nameCache = do + let mlibbs = getLiquidLibBytesFromEPS thisModule eps + case mlibbs of + Just (LiquidLibBytes ws) -> do + let bs = B.pack ws + Just <$> decodeLiquidLib nameCache bs + _ -> return Nothing + +encodeLiquidLib :: LiquidLib -> IO B.ByteString +encodeLiquidLib lib0 = do + let (lib1, ns) = collectLHNames lib0 + bh <- GHC.openBinMem (1024*1024) + GHC.putWithUserData GHC.QuietBinIFace bh ns + GHC.withBinBuffer bh $ \bs -> + return $ Builder.toLazyByteString $ B.execPut (B.put lib1) <> Builder.fromByteString bs + +decodeLiquidLib :: GHC.NameCache -> B.ByteString -> IO LiquidLib +decodeLiquidLib nameCache bs0 = do + case B.decodeOrFail bs0 of + Left (_, _, err) -> error $ "decodeLiquidLib: decodeOrFail: " ++ err + Right (bs1, _, lib) -> do + bh <- GHC.unsafeUnpackBinBuffer $ B.toStrict bs1 + ns <- GHC.getWithUserData nameCache bh + let n = fromIntegral $ length ns + arr = Array.listArray (0, n - 1) ns + return $ mapLHNames (resolveLHNameIndex arr) lib where - serialised :: Annotation - serialised = Annotation (ModuleTarget thisModule) (toSerialized (B.unpack . B.encode) obj) + resolveLHNameIndex :: Array.Array Word LHResolvedName -> LHName -> LHName + resolveLHNameIndex arr lhname = + case getLHNameResolved lhname of + LHRIndex i -> + if i <= snd (Array.bounds arr) then + makeResolvedLHName (arr Array.! i) (getLHNameSymbol lhname) + else + error $ "decodeLiquidLib: index out of bounds: " ++ show (i, Array.bounds arr) + _ -> + lhname --- | Serialise a 'LiquidLib', removing the termination checks from the target. -serialiseLiquidLib :: LiquidLib -> Module -> Annotation -serialiseLiquidLib lib = serialiseBinaryObject @LiquidLib lib +newtype AccF a b = AccF { unAccF :: a -> b -> (a, b) } -deserialiseLiquidLib :: Module -> ExternalPackageState -> HomePackageTable -> Maybe LiquidLib -deserialiseLiquidLib thisModule = deserialiseBinaryObject @LiquidLib thisModule +collectLHNames :: Data a => a -> (a, [LHResolvedName]) +collectLHNames t = + let ((_, _, xs), t') = go (0, M.empty, []) t + in (t', reverse xs) + where + go + :: Data a + => (Word, M.HashMap LHResolvedName Word, [LHResolvedName]) + -> a + -> ((Word, M.HashMap LHResolvedName Word, [LHResolvedName]), a) + go = gmapAccumT $ unAccF $ AccF go `ext0` AccF collectName -deserialiseLiquidLibFromEPS :: Module -> ExternalPackageState -> Maybe LiquidLib -deserialiseLiquidLibFromEPS = deserialiseBinaryObjectFromEPS @LiquidLib + collectName acc@(sz, m, xs) n = case M.lookup n m of + Just i -> (acc, LHRIndex i) + Nothing -> ((sz + 1, M.insert n sz m, n : xs), LHRIndex sz) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs index 72f1aa9092..ea6c7b5bca 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs @@ -51,7 +51,7 @@ findRelevantSpecs lhAssmPkgExcludes hscEnv mods = do loadRelevantSpec :: ExternalPackageState -> Module -> TcM SpecFinderResult loadRelevantSpec eps currentModule = do res <- liftIO $ runMaybeT $ - lookupInterfaceAnnotations eps (ue_hpt $ hsc_unit_env hscEnv) currentModule + lookupInterfaceAnnotations eps (ue_hpt $ hsc_unit_env hscEnv) (hsc_NC hscEnv) currentModule case res of Nothing -> do mAssm <- loadModuleLHAssumptionsIfAny currentModule @@ -71,7 +71,7 @@ findRelevantSpecs lhAssmPkgExcludes hscEnv mods = do -- read the EPS again eps2 <- liftIO $ readIORef (euc_eps $ ue_eps $ hsc_unit_env hscEnv) -- now look up the assumptions - liftIO $ runMaybeT $ lookupInterfaceAnnotationsEPS eps2 assumptionsMod + liftIO $ runMaybeT $ lookupInterfaceAnnotationsEPS eps2 (hsc_NC hscEnv) assumptionsMod FoundMultiple{} -> failWithTc $ mkTcRnUnknownMessage $ mkPlainError [] $ missingInterfaceErrorDiagnostic (initIfaceMessageOpts $ hsc_dflags hscEnv) $ cannotFindModule hscEnv assumptionsModName res @@ -85,14 +85,14 @@ findRelevantSpecs lhAssmPkgExcludes hscEnv mods = do mkModuleNameFS $ moduleNameFS (moduleName m) <> "_LHAssumptions" -- | Load specs from an interface file. -lookupInterfaceAnnotations :: ExternalPackageState -> HomePackageTable -> SpecFinder m -lookupInterfaceAnnotations eps hpt thisModule = do - lib <- MaybeT $ pure $ Serialisation.deserialiseLiquidLib thisModule eps hpt +lookupInterfaceAnnotations :: ExternalPackageState -> HomePackageTable -> NameCache -> SpecFinder m +lookupInterfaceAnnotations eps hpt nameCache thisModule = do + lib <- MaybeT $ Serialisation.deserialiseLiquidLib thisModule eps hpt nameCache pure $ LibFound thisModule lib -lookupInterfaceAnnotationsEPS :: ExternalPackageState -> SpecFinder m -lookupInterfaceAnnotationsEPS eps thisModule = do - lib <- MaybeT $ pure $ Serialisation.deserialiseLiquidLibFromEPS thisModule eps +lookupInterfaceAnnotationsEPS :: ExternalPackageState -> NameCache -> SpecFinder m +lookupInterfaceAnnotationsEPS eps nameCache thisModule = do + lib <- MaybeT $ Serialisation.deserialiseLiquidLibFromEPS thisModule eps nameCache pure $ LibFound thisModule lib -- | Returns a list of 'StableModule's which can be filtered out of the dependency list, because they are diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/Types.hs index 38809b979b..434ba922df 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/Types.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/Types.hs @@ -1,6 +1,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-} module Language.Haskell.Liquid.GHC.Plugin.Types @@ -29,6 +30,7 @@ module Language.Haskell.Liquid.GHC.Plugin.Types ) where import Data.Binary as B +import Data.Data ( Data ) import GHC.Generics hiding ( moduleName ) import qualified Data.HashSet as HS @@ -47,7 +49,7 @@ data LiquidLib = LiquidLib -- ^ The target /LiftedSpec/. , llDeps :: TargetDependencies -- ^ The specs which were necessary to produce the target 'BareSpec'. - } deriving (Show, Generic) + } deriving (Show, Data, Generic) instance B.Binary LiquidLib diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs new file mode 100644 index 0000000000..a5d5e357e0 --- /dev/null +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs @@ -0,0 +1,229 @@ +-- | This module provides a GHC 'Plugin' that allows LiquidHaskell to be hooked directly into GHC's +-- compilation pipeline, facilitating its usage and adoption. + +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE LambdaCase #-} + +module Language.Haskell.Liquid.LHNameResolution + ( collectTypeAliases + , resolveLHNames + , exprArg + ) where + +import Liquid.GHC.API as GHC hiding (Expr, panic) +import qualified Language.Haskell.Liquid.GHC.Misc as LH +import Language.Haskell.Liquid.Types.Names +import Language.Haskell.Liquid.Types.RType + +import Control.Monad.Writer +import Data.Data (Data, gmapT) +import Data.Generics (extT) + + +import qualified Data.HashSet as HS +import qualified Data.HashMap.Strict as HM + +import Language.Fixpoint.Types hiding (Error, panic) +import Language.Haskell.Liquid.Types.Errors (TError(ErrDupNames, ErrResolve), panic) +import Language.Haskell.Liquid.Types.Specs +import Language.Haskell.Liquid.Types.Types + +import qualified Text.PrettyPrint.HughesPJ as PJ +import qualified Text.Printf as Printf + +-- | Collects type aliases from the current module and its dependencies. +-- +-- It doesn't matter at the moment in which module a type alias is defined. +-- Type alias names cannot be qualified at the moment, and therefore their +-- names identify them uniquely. +collectTypeAliases + :: Module + -> BareSpec + -> [(StableModule, LiftedSpec)] + -> HM.HashMap Symbol (GHC.Module, RTAlias Symbol BareType) +collectTypeAliases m bs deps = + let spec = getBareSpec bs + bsAliases = [ (rtName a, (m, a)) | a <- map val (aliases spec) ] + depAliases = + [ (rtName a, (unStableModule sm, a)) + | (sm, lspec) <- deps + , a <- map val (HS.toList $ liftedAliases lspec) + ] + in + HM.fromList $ bsAliases ++ depAliases + +-- | Converts occurrences of LHNUnresolved to LHNResolved using the provided +-- type aliases and GlobalRdrEnv. +resolveLHNames + :: HM.HashMap Symbol (Module, RTAlias Symbol BareType) + -> GlobalRdrEnv + -> BareSpec + -> Either [Error] BareSpec +resolveLHNames taliases globalRdrEnv = + (\(bs, es) -> if null es then Right bs else Left es) . + runWriter . + mapMLocLHNames (\l -> (<$ l) <$> resolveLHName l) . + fixExpressionArgsOfTypeAliases taliases + where + resolveLHName lname = case val lname of + LHNUnresolved LHTcName s + | isTuple s -> + pure $ LHNResolved (LHRGHC $ GHC.tupleTyConName GHC.BoxedTuple (tupleArity s)) s + | isList s -> + pure $ LHNResolved (LHRGHC GHC.listTyConName) s + | s == "*" -> + pure $ LHNResolved (LHRGHC GHC.liftedTypeKindTyConName) s + | otherwise -> + case HM.lookup s taliases of + Just (m, _) -> pure $ LHNResolved (LHRLogic $ LogicName s m) s + Nothing -> case GHC.lookupGRE globalRdrEnv (mkLookupGRE LHTcName s) of + [e] -> pure $ LHNResolved (LHRGHC $ GHC.greName e) s + es@(_:_) -> do + tell [ErrDupNames + (LH.fSrcSpan lname) + (pprint s) + (map (PJ.text . showPprUnsafe) es) + ] + pure $ val lname + [] -> do + tell [errResolve "type constructor" "Cannot resolve name" (s <$ lname)] + pure $ val lname + LHNUnresolved LHDataConName s -> + case GHC.lookupGRE globalRdrEnv (mkLookupGRE LHDataConName s) of + [e] -> + pure $ LHNResolved (LHRGHC $ GHC.greName e) s + es@(_:_) -> do + tell [ErrDupNames + (LH.fSrcSpan lname) + (pprint s) + (map (PJ.text . showPprUnsafe) es) + ] + pure $ val lname + [] -> do + tell [errResolve "data constructor" "Cannot resolve name" (s <$ lname)] + pure $ val lname + n@(LHNResolved (LHRLocal _) _) -> pure n + n -> + let sp = Just $ LH.sourcePosSrcSpan $ loc lname + in panic sp $ "resolveLHNames: Unexpected resolved name: " ++ show n + + errResolve :: PJ.Doc -> String -> LocSymbol -> Error + errResolve k msg lx = ErrResolve (LH.fSrcSpan lx) k (pprint (val lx)) (PJ.text msg) + + mkLookupGRE ns s = + let m = LH.takeModuleNames s + n = LH.dropModuleNames s + oname = GHC.mkOccName (mkGHCNameSpace ns) $ symbolString n + rdrn = + if m == "" then + GHC.mkRdrUnqual oname + else + GHC.mkRdrQual (GHC.mkModuleName $ symbolString m) oname + in GHC.LookupRdrName rdrn GHC.SameNameSpace + + mkGHCNameSpace = \case + LHTcName -> GHC.tcName + LHDataConName -> GHC.dataName + + tupleArity s = + let a = read $ drop 5 $ symbolString s + in if a > 64 then + error $ "tupleArity: Too large (more than 64): " ++ show a + else + a + +-- | Changes unresolved names to local resolved names in the body of type +-- aliases. +resolveBoundVarsInTypeAliases :: BareSpec -> BareSpec +resolveBoundVarsInTypeAliases = updateAliases resolveBoundVars + where + resolveBoundVars boundVars = \case + LHNUnresolved LHTcName s -> + if elem s boundVars then + LHNResolved (LHRLocal s) s + else + LHNUnresolved LHTcName s + n -> + error $ "resolveLHNames: Unexpected resolved name: " ++ show n + + -- Applies a function to the body of type aliases, passes to every call the + -- arguments of the alias. + updateAliases f bs = + let spec = getBareSpec bs + in MkBareSpec spec + { aliases = [ Loc sp0 sp1 (a { rtBody = mapLHNames (f args) (rtBody a) }) + | Loc sp0 sp1 a <- aliases spec + , let args = rtTArgs a ++ rtVArgs a + ] + } + +-- | The expression arguments of type aliases are initially parsed as +-- types. This function converts them to expressions. +-- +-- For instance, in @Prop (Ev (plus n n))@ where `Prop` is the alias +-- +-- > {-@ type Prop E = {v:_ | prop v = E} @-} +-- +-- the parser builds a type for @Ev (plus n n)@. +-- +fixExpressionArgsOfTypeAliases + :: HM.HashMap Symbol (Module, RTAlias Symbol BareType) + -> BareSpec + -> BareSpec +fixExpressionArgsOfTypeAliases taliases = + mapBareTypes go . resolveBoundVarsInTypeAliases + where + go :: BareType -> BareType + go (RApp c@(BTyCon { btc_tc = Loc _ _ (LHNUnresolved LHTcName s) }) ts rs r) + | Just (_, rta) <- HM.lookup s taliases = + RApp c (fixExprArgs (btc_tc c) rta (map go ts)) (map goRef rs) r + go (RApp c ts rs r) = + RApp c (map go ts) (map goRef rs) r + go (RAppTy t1 t2 r) = RAppTy (go t1) (go t2) r + go (RFun x i t1 t2 r) = RFun x i (go t1) (go t2) r + go (RAllT a t r) = RAllT a (go t) r + go (RAllP a t) = RAllP a (go t) + go (RAllE x t1 t2) = RAllE x (go t1) (go t2) + go (REx x t1 t2) = REx x (go t1) (go t2) + go (RRTy e r o t) = RRTy e r o (go t) + go t@RHole{} = t + go t@RVar{} = t + go t@RExprArg{} = t + goRef (RProp ss t) = RProp ss (go t) + + fixExprArgs lname rta ts = + let n = length (rtTArgs rta) + (targs, eargs) = splitAt n ts + msg = "FIX-EXPRESSION-ARG: " ++ showpp (rtName rta) + toExprArg = exprArg (LH.fSourcePos lname) msg + in targs ++ [ RExprArg $ toExprArg e <$ lname | e <- eargs ] + +mapBareTypes :: (BareType -> BareType) -> BareSpec -> BareSpec +mapBareTypes f = go + where + go :: Data a => a -> a + go = gmapT (go `extT` f) + +-- | exprArg converts a tyVar to an exprVar because parser cannot tell +-- this function allows us to treating (parsed) "types" as "value" +-- arguments, e.g. type Matrix a Row Col = List (List a Row) Col +-- Note that during parsing, we don't necessarily know whether a +-- string is a type or a value expression. E.g. in tests/pos/T1189.hs, +-- the string `Prop (Ev (plus n n))` where `Prop` is the alias: +-- {-@ type Prop E = {v:_ | prop v = E} @-} +-- the parser will chomp in `Ev (plus n n)` as a `BareType` and so +-- `exprArg` converts that `BareType` into an `Expr`. +exprArg :: SourcePos -> String -> BareType -> Expr +exprArg l msg = notracepp ("exprArg: " ++ msg) . go + where + go :: BareType -> Expr + go (RExprArg e) = val e + go (RVar x _) = EVar (symbol x) + go (RApp x [] [] _) = EVar (getLHNameSymbol $ val $ btc_tc x) + go (RApp f ts [] _) = mkEApp (getLHNameSymbol <$> btc_tc f) (go <$> ts) + go (RAppTy t1 t2 _) = EApp (go t1) (go t2) + go z = panic sp $ Printf.printf "Unexpected expression parameter: %s in %s" (show z) msg + sp = Just (LH.sourcePosSrcSpan l) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs index e953936425..28c44e7a69 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs @@ -251,7 +251,12 @@ btP = do (do b <- locInfixSymbolP PC _ t2 <- btP - return $ PC sb $ RApp (mkBTyCon b) [t1,t2] [] mempty) + return $ PC sb $ RApp + (mkBTyCon $ fmap (makeUnresolvedLHName LHTcName) b) + [t1,t2] + [] + mempty + ) <|> return c @@ -461,18 +466,20 @@ lowerIdTail l = bTyConP :: Parser BTyCon bTyConP - = (reservedOp "'" >> (mkPromotedBTyCon <$> locUpperIdP)) - <|> mkBTyCon <$> locUpperIdP - <|> (reserved "*" >> return (mkBTyCon (dummyLoc $ symbol ("*" :: String)))) + = (reservedOp "'" >> (mkPromotedBTyCon . fmap (makeUnresolvedLHName LHDataConName) <$> locUpperIdP)) + <|> mkBTyCon . fmap (makeUnresolvedLHName LHTcName) <$> locUpperIdP + <|> (reserved "*" >> + return (mkBTyCon (dummyLoc $ makeUnresolvedLHName LHTcName $ symbol ("*" :: String))) + ) "bTyConP" -mkPromotedBTyCon :: LocSymbol -> BTyCon +mkPromotedBTyCon :: Located LHName -> BTyCon mkPromotedBTyCon x = BTyCon x False True -- (consSym '\'' <$> x) False True classBTyConP :: Parser BTyCon -classBTyConP = mkClassBTyCon <$> locUpperIdP +classBTyConP = mkClassBTyCon . fmap (makeUnresolvedLHName LHTcName) <$> locUpperIdP -mkClassBTyCon :: LocSymbol -> BTyCon +mkClassBTyCon :: Located LHName -> BTyCon mkClassBTyCon x = BTyCon x True False bbaseNoAppP :: Parser (Reft -> BareType) @@ -609,11 +616,11 @@ dummyBindP :: Parser Symbol dummyBindP = tempSymbol "db" <$> freshIntP isPropBareType :: RType BTyCon t t1 -> Bool -isPropBareType = isPrimBareType boolConName - -isPrimBareType :: Symbol -> RType BTyCon t t1 -> Bool -isPrimBareType n (RApp tc [] _ _) = val (btc_tc tc) == n -isPrimBareType _ _ = False +isPropBareType (RApp tc [] _ _) = + case val (btc_tc tc) of + LHNUnresolved _ s -> s == boolConName + _ -> False +isPropBareType _ = False getClasses :: RType BTyCon t t1 -> [RType BTyCon t t1] getClasses (RApp tc ts ps r) @@ -758,8 +765,8 @@ bLst :: Maybe (RType BTyCon tv (UReft r)) -> [RTProp BTyCon tv (UReft r)] -> r -> RType BTyCon tv (UReft r) -bLst (Just t) rs r = RApp (mkBTyCon $ dummyLoc listConName) [t] rs (reftUReft r) -bLst Nothing rs r = RApp (mkBTyCon $ dummyLoc listConName) [] rs (reftUReft r) +bLst (Just t) rs r = RApp (mkBTyCon $ dummyLoc $ makeUnresolvedLHName LHTcName listConName) [t] rs (reftUReft r) +bLst Nothing rs r = RApp (mkBTyCon $ dummyLoc $ makeUnresolvedLHName LHTcName listConName) [] rs (reftUReft r) bTup :: (PPrint r, Reftable r, Reftable (RType BTyCon BTyVar (UReft r)), Reftable (RTProp BTyCon BTyVar (UReft r))) => [(Maybe Symbol, RType BTyCon BTyVar (UReft r))] @@ -772,12 +779,14 @@ bTup [(_,t)] _ r bTup ts rs r | all Mb.isNothing (fst <$> ts) || length ts < 2 = RApp - (mkBTyCon $ dummyLoc $ fromString $ "Tuple" ++ show (length ts)) + (mkBTyCon $ dummyLoc $ makeUnresolvedLHName LHTcName $ fromString $ "Tuple" ++ show (length ts)) (snd <$> ts) rs (reftUReft r) | otherwise = RApp - (mkBTyCon $ dummyLoc $ fromString $ "Tuple" ++ show (length ts)) - (top . snd <$> ts) rs' (reftUReft r) + (mkBTyCon $ dummyLoc $ makeUnresolvedLHName LHTcName $ fromString $ "Tuple" ++ show (length ts)) + (top . snd <$> ts) + rs' + (reftUReft r) where args = [(Mb.fromMaybe dummySymbol x, mapReft mempty t) | (x,t) <- ts] makeProp i = RProp (take i args) ((snd <$> ts)!!i) @@ -842,7 +851,7 @@ data Pspec ty ctor | Using (ty, ty) -- ^ 'using' declaration (for local invariants on a type) | Alias (Located (RTAlias Symbol BareType)) -- ^ 'type' alias declaration | EAlias (Located (RTAlias Symbol Expr)) -- ^ 'predicate' alias declaration - | Embed (LocSymbol, FTycon, TCArgs) -- ^ 'embed' declaration + | Embed (Located LHName, FTycon, TCArgs) -- ^ 'embed' declaration | Qualif Qualifier -- ^ 'qualif' definition | LVars LocSymbol -- ^ 'lazyvar' annotation, defer checks to *use* sites | Lazy LocSymbol -- ^ 'lazy' annotation, skip termination check on binder @@ -1275,9 +1284,9 @@ invaliasP genBareTypeP :: Parser BareType genBareTypeP = bareTypeP -embedP :: Parser (Located Symbol, FTycon, TCArgs) +embedP :: Parser (Located LHName, FTycon, TCArgs) embedP = do - x <- locUpperIdP + x <- fmap (makeUnresolvedLHName LHTcName) <$> locUpperIdP a <- try (reserved "*" >> return WithArgs) <|> return NoArgs -- TODO: reserved "*" looks suspicious _ <- reserved "as" t <- fTyConP diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/ANF.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/ANF.hs index e3e3e0447a..3e6444e34b 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/ANF.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/ANF.hs @@ -14,7 +14,7 @@ module Language.Haskell.Liquid.Transforms.ANF (anormalize) where import Debug.Trace (trace) import Prelude hiding (error) import Language.Haskell.Liquid.GHC.TypeRep -import Liquid.GHC.API as Ghc hiding ( mkTyArg +import Liquid.GHC.API as Ghc hiding ( get, mkTyArg , showPpr , DsM , panic) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs index 367b0d11d5..5c3e4f47b0 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs @@ -25,7 +25,7 @@ import Data.Bifunctor (first) import Data.ByteString (ByteString) import Prelude hiding (error) import Language.Haskell.Liquid.GHC.TypeRep () -- needed for Eq 'Type' -import Liquid.GHC.API hiding (Expr, Located, panic) +import Liquid.GHC.API hiding (Expr, Located, get, panic) import qualified Liquid.GHC.API as Ghc import qualified Liquid.GHC.API as C import qualified Data.List as L diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/Rewrite.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/Rewrite.hs index d2d699d5a3..e0a85e344c 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/Rewrite.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/Rewrite.hs @@ -24,7 +24,7 @@ module Language.Haskell.Liquid.Transforms.Rewrite ) where -import Liquid.GHC.API as Ghc hiding (showPpr, substExpr) +import Liquid.GHC.API as Ghc hiding (get, showPpr, substExpr) import Language.Haskell.Liquid.GHC.TypeRep () import Data.Maybe (fromMaybe, isJust, mapMaybe) import Control.Monad.State hiding (lift) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Dictionaries.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Dictionaries.hs index 53b4c1ea0d..c96ece555b 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Dictionaries.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Dictionaries.hs @@ -1,8 +1,7 @@ {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleContexts #-} module Language.Haskell.Liquid.Types.Dictionaries ( - makeDictionaries - , makeDictionary + makeDictionary , dfromList , dmapty , dmap @@ -21,6 +20,7 @@ import Language.Haskell.Liquid.Types.PrettyPrint () import qualified Language.Haskell.Liquid.GHC.Misc as GM import qualified Liquid.GHC.API as Ghc import Language.Haskell.Liquid.Types.Errors +import Language.Haskell.Liquid.Types.Names import Language.Haskell.Liquid.Types.RType import Language.Haskell.Liquid.Types.RTypeOp -- import Language.Haskell.Liquid.Types.Visitors (freeVars) @@ -29,15 +29,8 @@ import Language.Haskell.Liquid.Types.Types import qualified Data.HashMap.Strict as M - - - -makeDictionaries :: [RInstance LocSpecType] -> DEnv F.Symbol LocSpecType -makeDictionaries = DEnv . M.fromList . map makeDictionary - - makeDictionary :: RInstance LocSpecType -> (F.Symbol, M.HashMap F.Symbol (RISig LocSpecType)) -makeDictionary (RI c ts xts) = (makeDictionaryName (btc_tc c) ts, M.fromList (first val <$> xts)) +makeDictionary (RI c ts xts) = (makeDictionaryName (getLHNameSymbol <$> btc_tc c) ts, M.fromList (first val <$> xts)) makeDictionaryName :: LocSymbol -> [LocSpecType] -> F.Symbol makeDictionaryName t ts diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs index 5e60f5f320..ddfff80484 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs @@ -1,7 +1,34 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE ScopedTypeVariables #-} module Language.Haskell.Liquid.Types.Names - (lenLocSymbol, anyTypeSymbol, functionComposisionSymbol, selfSymbol) where + ( lenLocSymbol + , anyTypeSymbol + , functionComposisionSymbol + , selfSymbol + , LogicName (..) + , LHResolvedName (..) + , LHName (..) + , LHNameSpace (..) + , makeResolvedLHName + , getLHNameResolved + , getLHNameSymbol + , makeUnresolvedLHName + , mapLHNames + , mapMLocLHNames + ) where +import Control.DeepSeq +import qualified Data.Binary as B +import Data.Data (Data, gmapM, gmapT) +import Data.Generics (extM, extT) +import Data.Hashable +import Data.String (fromString) +import GHC.Generics +import GHC.Stack import Language.Fixpoint.Types +import qualified Liquid.GHC.API as GHC +import Text.PrettyPrint.HughesPJ.Compat -- RJ: Please add docs lenLocSymbol :: Located Symbol @@ -18,3 +45,132 @@ functionComposisionSymbol = symbol ("GHC.Internal.Base.." :: String) selfSymbol :: Symbol selfSymbol = symbol ("liquid_internal_this" :: String) + +-- | A name for an entity that does not exist in Haskell +-- +-- For instance, this can be used to represent predicate aliases +-- or uninterpreted functions. +data LogicName = LogicName + { lnSymbol :: !Symbol + , lnModule :: !GHC.Module + } + deriving (Data, Eq, Generic) + +-- | A name whose procedence is known. +data LHResolvedName + = LHRLogic !LogicName + | LHRGHC !GHC.Name -- ^ A name for an entity that exists in Haskell + | LHRLocal !Symbol -- ^ A name for a local variable, e.g. one that is + -- bound by a type alias. + | -- | The index of a name in some environment + -- + -- Before serializing names, they are converted to indices. The names + -- themselves are kept in an environment or table that is serialized + -- separately. This is to acommodate how GHC serializes its Names. + LHRIndex Word + deriving (Data, Eq, Generic, Ord) + +-- | A name that is potentially unresolved. +data LHName + = -- | In order to integrate the resolved names gradually, we keep the + -- unresolved names. + LHNResolved !LHResolvedName !Symbol + | LHNUnresolved !LHNameSpace !Symbol + deriving (Data, Eq, Generic, Ord) + +data LHNameSpace + = LHTcName + | LHDataConName + deriving (Data, Eq, Generic, Ord) + +instance B.Binary LHNameSpace +instance NFData LHNameSpace +instance Hashable LHNameSpace + +instance Ord LogicName where + compare (LogicName s1 m1) (LogicName s2 m2) = + case compare s1 s2 of + EQ -> GHC.stableModuleCmp m1 m2 + x -> x + +instance Show LHName where + show (LHNResolved _ s) = symbolString s + show (LHNUnresolved _ s) = symbolString s + +instance NFData LHName +instance NFData LHResolvedName +instance NFData LogicName + +instance Hashable LHResolvedName where + hashWithSalt s (LHRLogic n) = s `hashWithSalt` (0::Int) `hashWithSalt` n + hashWithSalt s (LHRGHC n) = + s `hashWithSalt` (1::Int) `hashWithSalt` GHC.getKey (GHC.nameUnique n) + hashWithSalt s (LHRLocal n) = s `hashWithSalt` (2::Int) `hashWithSalt` n + hashWithSalt s (LHRIndex w) = s `hashWithSalt` (3::Int) `hashWithSalt` w + +instance Hashable LHName +instance Hashable LogicName where + hashWithSalt s (LogicName sym m) = + s `hashWithSalt` sym + `hashWithSalt` GHC.moduleStableString m + +instance B.Binary LHName +instance B.Binary LHResolvedName where + get = do + tag <- B.getWord8 + case tag of + 0 -> LHRLocal . fromString <$> B.get + 1 -> LHRIndex <$> B.get + _ -> error "B.Binary: invalid tag for LHResolvedName" + put (LHRLogic _n) = error "cannot serialize LHRLogic" + put (LHRGHC _n) = error "cannot serialize LHRGHC" + put (LHRLocal s) = B.putWord8 0 >> B.put (symbolString s) + put (LHRIndex n) = B.putWord8 1 >> B.put n + +instance GHC.Binary LHResolvedName where + get bh = do + tag <- GHC.getByte bh + case tag of + 0 -> LHRLogic <$> GHC.get bh + 1 -> LHRGHC <$> GHC.get bh + 2 -> LHRLocal . fromString <$> GHC.get bh + _ -> error "GHC.Binary: invalid tag for LHResolvedName" + put_ bh (LHRLogic n) = GHC.putByte bh 0 >> GHC.put_ bh n + put_ bh (LHRGHC n) = GHC.putByte bh 1 >> GHC.put_ bh n + put_ bh (LHRLocal n) = GHC.putByte bh 2 >> GHC.put_ bh (symbolString n) + put_ _bh (LHRIndex _n) = error "GHC.Binary: cannot serialize LHRIndex" + +instance GHC.Binary LogicName where + get bh = LogicName . fromString <$> GHC.get bh <*> GHC.get bh + put_ bh (LogicName s m) = GHC.put_ bh (symbolString s) >> GHC.put_ bh m + +instance PPrint LHName where + pprintTidy _ = text . show + +makeResolvedLHName :: LHResolvedName -> Symbol -> LHName +makeResolvedLHName = LHNResolved + +makeUnresolvedLHName :: LHNameSpace -> Symbol -> LHName +makeUnresolvedLHName = LHNUnresolved + +-- | Get the unresolved Symbol from an LHName. +getLHNameSymbol :: LHName -> Symbol +getLHNameSymbol (LHNResolved _ s) = s +getLHNameSymbol (LHNUnresolved _ s) = s + +-- | Get the unresolved Symbol from an LHName. +getLHNameResolved :: HasCallStack => LHName -> LHResolvedName +getLHNameResolved (LHNResolved n _) = n +getLHNameResolved n@LHNUnresolved{} = error $ "getLHNameResolved: unresolved name: " ++ show n + +mapLHNames :: Data a => (LHName -> LHName) -> a -> a +mapLHNames f = go + where + go :: Data a => a -> a + go = gmapT (go `extT` f) + +mapMLocLHNames :: forall m a. (Data a, Monad m) => (Located LHName -> m (Located LHName)) -> a -> m a +mapMLocLHNames f = go + where + go :: forall b. Data b => b -> m b + go = gmapM (go `extM` f) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RType.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RType.hs index c59ca85e69..345a0800ff 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RType.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RType.hs @@ -131,6 +131,7 @@ import qualified Language.Fixpoint.Types as F import Language.Fixpoint.Types (Expr, Symbol) import Language.Haskell.Liquid.GHC.Misc +import Language.Haskell.Liquid.Types.Names import Language.Haskell.Liquid.Types.Variance import Language.Haskell.Liquid.Types.Errors import Language.Haskell.Liquid.Misc @@ -376,7 +377,7 @@ instance F.Symbolic RTyVar where -- tyVarUniqueSymbol tv = F.symbol $ show (getName tv) ++ "_" ++ show (varUnique tv) data BTyCon = BTyCon - { btc_tc :: !F.LocSymbol -- ^ TyCon name with location information + { btc_tc :: !(F.Located LHName) -- ^ TyCon name with location information , btc_class :: !Bool -- ^ Is this a class type constructor? , btc_prom :: !Bool -- ^ Is Promoted Data Con? } @@ -395,15 +396,12 @@ data RTyCon = RTyCon instance F.Symbolic RTyCon where symbol = F.symbol . rtc_tc -instance F.Symbolic BTyCon where - symbol = F.val . btc_tc - instance NFData BTyCon instance NFData RTyCon -mkBTyCon :: F.LocSymbol -> BTyCon +mkBTyCon :: F.Located LHName -> BTyCon mkBTyCon x = BTyCon x False False @@ -524,12 +522,30 @@ instance TyConable F.LocSymbol where ppTycon = ppTycon . F.val instance TyConable BTyCon where - isFun = isFun . btc_tc - isList = isList . btc_tc - isTuple = isTuple . btc_tc + isFun b = case F.val (btc_tc b) of + LHNUnresolved _ s -> isFun s + LHNResolved (LHRGHC n) _ -> n == unrestrictedFunTyConName + _ -> False + + isList b = case F.val (btc_tc b) of + LHNUnresolved _ s -> isList s + LHNResolved (LHRGHC n) _ -> n == listTyConName + _ -> False + + isTuple b = case F.val (btc_tc b) of + LHNUnresolved _ s -> isTuple s + LHNResolved (LHRGHC n) _ -> Ghc.isTupleTyConName n + _ -> False + isClass = isClassBTyCon - ppTycon = ppTycon . btc_tc + ppTycon b = case F.val (btc_tc b) of + LHNUnresolved _ s -> ppTycon s + LHNResolved rn _ -> case rn of + LHRGHC n -> text $ showPpr n + LHRLocal s -> ppTycon s + LHRIndex i -> text $ "(Unknown LHRIndex " ++ show i ++ ")" + LHRLogic (LogicName s _) -> ppTycon s instance Eq RTyCon where x == y = rtc_tc x == rtc_tc y @@ -544,7 +560,13 @@ instance F.Fixpoint RTyCon where toFix (RTyCon c _ _) = text $ showPpr c instance F.Fixpoint BTyCon where - toFix = text . F.symbolString . F.val . btc_tc + toFix b = case F.val (btc_tc b) of + LHNUnresolved _ s -> text $ F.symbolString s + LHNResolved rn _ -> case rn of + LHRGHC n -> text $ F.symbolString $ F.symbol n + LHRLocal s -> text $ F.symbolString s + LHRIndex i -> panic (Just $ fSrcSpan b) $ "toFix BTyCon: Unknown LHRIndex " ++ show i + LHRLogic (LogicName s _) -> text $ F.symbolString s instance F.PPrint RTyCon where pprintTidy k c @@ -555,7 +577,13 @@ instance F.PPrint RTyCon where pvs = rtc_pvars c instance F.PPrint BTyCon where - pprintTidy _ = text . F.symbolString . F.val . btc_tc + pprintTidy _ b = case F.val (btc_tc b) of + LHNUnresolved _ s -> text $ F.symbolString s + LHNResolved rn _ -> case rn of + LHRGHC n -> text $ F.symbolString $ F.symbol n + LHRLocal s -> text $ F.symbolString s + LHRIndex i -> text $ "(Unknown LHRIndex " ++ show i ++ ")" + LHRLogic (LogicName s _) -> text $ F.symbolString s instance F.PPrint v => F.PPrint (RTVar v s) where pprintTidy k (RTVar x _) = F.pprintTidy k x diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RefType.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RefType.hs index 5b43e129aa..74b1eb2089 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RefType.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/RefType.hs @@ -119,7 +119,7 @@ import Language.Haskell.Liquid.Misc import Language.Haskell.Liquid.Types.Names import qualified Language.Haskell.Liquid.GHC.Misc as GM import Language.Haskell.Liquid.GHC.Play (mapType, stringClassArg, isRecursivenewTyCon) -import Liquid.GHC.API as Ghc hiding ( Expr +import Liquid.GHC.API as Ghc hiding ( Expr, get , Located , tyConName , punctuate @@ -548,8 +548,10 @@ bApp :: TyCon -> [BRType r] -> [BRProp r] -> r -> BRType r bApp c = RApp (tyConBTyCon c) tyConBTyCon :: TyCon -> BTyCon -tyConBTyCon = mkBTyCon . fmap tyConName . GM.locNamedThing --- tyConBTyCon = mkBTyCon . fmap symbol . locNamedThing +tyConBTyCon tc = + mkBTyCon $ + makeResolvedLHName (LHRGHC (getName tc)) . tyConName <$> GM.locNamedThing tc + --- NV TODO : remove this code!!! diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs index 69016cb09c..80066169bc 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs @@ -4,6 +4,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE StandaloneDeriving #-} @@ -71,18 +72,20 @@ import GHC.Generics hiding (to, moduleName) import Data.Binary import qualified Language.Fixpoint.Types as F import Language.Fixpoint.Misc (sortNub) +import Data.Data (Data) import Data.Hashable import qualified Data.HashSet as S import Data.HashSet (HashSet) import qualified Data.HashMap.Strict as M import Data.HashMap.Strict (HashMap) import Language.Haskell.Liquid.Types.DataDecl +import Language.Haskell.Liquid.Types.Names import Language.Haskell.Liquid.Types.RType import Language.Haskell.Liquid.Types.Types import Language.Haskell.Liquid.Types.Variance import Language.Haskell.Liquid.Types.Bounds import Language.Haskell.Liquid.UX.Config -import Liquid.GHC.API hiding (text, (<+>)) +import Liquid.GHC.API hiding (Binary, text, (<+>)) import Language.Haskell.Liquid.GHC.Types import Text.PrettyPrint.HughesPJ (text, (<+>)) import Text.PrettyPrint.HughesPJ as HughesPJ (($$)) @@ -379,7 +382,7 @@ type SpecMeasure = Measure LocSpecType DataCon -- to undefined or out-of-scope entities. newtype BareSpec = MkBareSpec { getBareSpec :: Spec LocBareType F.LocSymbol } - deriving (Generic, Show, Binary) + deriving (Data, Generic, Show, Binary) instance Semigroup BareSpec where x <> y = MkBareSpec { getBareSpec = getBareSpec x <> getBareSpec y } @@ -408,7 +411,7 @@ data Spec ty bndr = Spec , includes :: ![FilePath] -- ^ Included qualifier files , aliases :: ![F.Located (RTAlias F.Symbol BareType)] -- ^ RefType aliases , ealiases :: ![F.Located (RTAlias F.Symbol F.Expr)] -- ^ Expression aliases - , embeds :: !(F.TCEmb F.LocSymbol) -- ^ GHC-Tycon-to-fixpoint Tycon map + , embeds :: !(F.TCEmb (F.Located LHName)) -- ^ GHC-Tycon-to-fixpoint Tycon map , qualifiers :: ![F.Qualifier] -- ^ Qualifiers in source files , lvars :: !(S.HashSet F.LocSymbol) -- ^ Variables that should be checked in the environment they are used , lazy :: !(S.HashSet F.LocSymbol) -- ^ Ignore Termination Check in these Functions @@ -440,7 +443,7 @@ data Spec ty bndr = Spec , dsize :: ![([ty], F.LocSymbol)] -- ^ Size measure to enforce fancy termination , bounds :: !(RRBEnv ty) , axeqs :: ![F.Equation] -- ^ Equalities used for Proof-By-Evaluation - } deriving (Generic, Show) + } deriving (Data, Generic, Show) instance Binary (Spec LocBareType F.LocSymbol) @@ -605,7 +608,7 @@ data LiftedSpec = LiftedSpec -- ^ RefType aliases , liftedEaliases :: HashSet (F.Located (RTAlias F.Symbol F.Expr)) -- ^ Expression aliases - , liftedEmbeds :: F.TCEmb F.LocSymbol + , liftedEmbeds :: F.TCEmb (F.Located LHName) -- ^ GHC-Tycon-to-fixpoint Tycon map , liftedQualifiers :: HashSet F.Qualifier -- ^ Qualifiers in source/spec files @@ -633,7 +636,7 @@ data LiftedSpec = LiftedSpec , liftedBounds :: RRBEnv LocBareType , liftedAxeqs :: HashSet F.Equation -- ^ Equalities used for Proof-By-Evaluation - } deriving (Eq, Generic, Show) + } deriving (Eq, Data, Generic, Show) deriving Hashable via Generically LiftedSpec deriving Binary via Generically LiftedSpec @@ -677,7 +680,7 @@ emptyLiftedSpec = LiftedSpec -- | The /target/ dependencies that concur to the creation of a 'TargetSpec' and a 'LiftedSpec'. newtype TargetDependencies = TargetDependencies { getDependencies :: HashMap StableModule LiftedSpec } - deriving (Eq, Show, Generic) + deriving (Data, Eq, Show, Generic) deriving Binary via Generically TargetDependencies -- instance S.Store TargetDependencies diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Variance.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Variance.hs index f0cf833e30..c955e14870 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Variance.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Variance.hs @@ -25,7 +25,7 @@ import qualified Data.HashSet as S import qualified Language.Fixpoint.Types as F import qualified Language.Haskell.Liquid.GHC.Misc as GM -import Liquid.GHC.API as Ghc hiding (text) +import Liquid.GHC.API as Ghc hiding (Binary, text) type VarianceInfo = [Variance] diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs index 9915d8be42..a5505ee777 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs @@ -23,13 +23,16 @@ import Language.Haskell.TH.Lib import Language.Haskell.TH.Syntax import Language.Haskell.TH.Quote -import Language.Fixpoint.Types hiding (Error, Loc, SrcSpan) +import Language.Fixpoint.Types hiding (Error, Loc, SrcSpan, panic) import qualified Language.Fixpoint.Types as F import Language.Haskell.Liquid.GHC.Misc (fSrcSpan) import Liquid.GHC.API (SrcSpan) +import qualified Liquid.GHC.API as GHC +import qualified GHC.Types.Name.Occurrence import Language.Haskell.Liquid.Parse import Language.Haskell.Liquid.Types.Errors +import Language.Haskell.Liquid.Types.Names import Language.Haskell.Liquid.Types.RType import Language.Haskell.Liquid.Types.RefType import Language.Haskell.Liquid.Types.Types @@ -103,6 +106,33 @@ mkSpecDecs _ = symbolName :: Symbolic s => s -> Name symbolName = mkName . symbolString . symbol +lhNameToName :: Located LHName -> Name +lhNameToName lname = case val lname of + LHNUnresolved _ s -> symbolName s + LHNResolved rn _ -> case rn of + LHRGHC n -> case GHC.nameModule_maybe n of + Nothing -> mkName (GHC.getOccString n) + Just m -> + mkNameG + (toTHNameSpace $ GHC.nameNameSpace n) + (GHC.unitString $ GHC.moduleUnit m) + (GHC.moduleNameString $ GHC.moduleName m) + (GHC.getOccString n) + LHRLocal s -> symbolName s + LHRIndex i -> panic (Just $ fSrcSpan lname) $ "Cannot produce a TH Name for a LHRIndex " ++ show i + LHRLogic (LogicName s _m) -> + panic (Just $ fSrcSpan lname) $ "Cannot produce a TH Name for a LogicName: " ++ show s + + where + toTHNameSpace :: GHC.NameSpace -> NameSpace + toTHNameSpace ns + | ns == GHC.dataName = DataName + | ns == GHC.tcName = TcClsName + | ns == GHC.Types.Name.Occurrence.varName = VarName + | GHC.isFieldNameSpace ns = panic (Just $ fSrcSpan lname) "lhNameToName: Unimplemented case for FieldName NameSpace" + | otherwise = panic (Just $ fSrcSpan lname) "lhNameToName: Unknown GHC.NameSpace" + + -- BareType to TH Type --------------------------------------------------------- simplifyBareType :: LocSymbol -> BareType -> Either UserError Type @@ -129,11 +159,10 @@ simplifyBareType'' ([], []) (RFun _ _ i o _) = (\x y -> ArrowT `AppT` x `AppT` y) <$> simplifyBareType' i <*> simplifyBareType' o simplifyBareType'' ([], []) (RApp cc as _ _) = - let c = btc_tc cc - c' | isFun c = ArrowT - | isTuple c = TupleT (length as) - | isList c = ListT - | otherwise = ConT $ symbolName c + let c' | isFun cc = ArrowT + | isTuple cc = TupleT (length as) + | isList cc = ListT + | otherwise = ConT $ lhNameToName (btc_tc cc) in foldl' AppT c' <$> sequenceA (filterExprArgs $ simplifyBareType' <$> as) simplifyBareType'' _ (RExprArg e) = diff --git a/src/Data/ByteString/Char8_LHAssumptions.hs b/src/Data/ByteString/Char8_LHAssumptions.hs index 0fd49f54b6..ddc288ade7 100644 --- a/src/Data/ByteString/Char8_LHAssumptions.hs +++ b/src/Data/ByteString/Char8_LHAssumptions.hs @@ -5,282 +5,283 @@ module Data.ByteString.Char8_LHAssumptions where import Data.ByteString_LHAssumptions() import Data.ByteString import Data.ByteString.Char8 +import GHC.Types {-@ assume Data.ByteString.Char8.singleton - :: GHC.Types.Char -> { bs : Data.ByteString.ByteString | bslen bs == 1 } + :: GHC.Types.Char -> { bs : ByteString | bslen bs == 1 } assume Data.ByteString.Char8.pack :: w8s : [GHC.Types.Char] - -> { bs : Data.ByteString.ByteString | bslen bs == len w8s } + -> { bs : ByteString | bslen bs == len w8s } assume Data.ByteString.Char8.unpack - :: bs : Data.ByteString.ByteString + :: bs : ByteString -> { w8s : [GHC.Types.Char] | len w8s == bslen bs } assume Data.ByteString.Char8.cons :: GHC.Types.Char - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen o == bslen i + 1 } + -> i : ByteString + -> { o : ByteString | bslen o == bslen i + 1 } assume Data.ByteString.Char8.snoc - :: i : Data.ByteString.ByteString + :: i : ByteString -> GHC.Types.Char - -> { o : Data.ByteString.ByteString | bslen o == bslen i + 1 } + -> { o : ByteString | bslen o == bslen i + 1 } -assume Data.ByteString.Char8.head :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> GHC.Types.Char +assume Data.ByteString.Char8.head :: { bs : ByteString | 1 <= bslen bs } -> GHC.Types.Char assume Data.ByteString.Char8.uncons - :: i : Data.ByteString.ByteString - -> Maybe (GHC.Types.Char, { o : Data.ByteString.ByteString | bslen o == bslen i - 1 }) + :: i : ByteString + -> Maybe (GHC.Types.Char, { o : ByteString | bslen o == bslen i - 1 }) assume Data.ByteString.Char8.unsnoc - :: i : Data.ByteString.ByteString - -> Maybe ({ o : Data.ByteString.ByteString | bslen o == bslen i - 1 }, GHC.Types.Char) + :: i : ByteString + -> Maybe ({ o : ByteString | bslen o == bslen i - 1 }, GHC.Types.Char) -assume Data.ByteString.Char8.last :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> GHC.Types.Char +assume Data.ByteString.Char8.last :: { bs : ByteString | 1 <= bslen bs } -> GHC.Types.Char assume Data.ByteString.Char8.map :: (GHC.Types.Char -> GHC.Types.Char) - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen o == bslen i } + -> i : ByteString + -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.Char8.intersperse :: GHC.Types.Char - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | (bslen i == 0 <=> bslen o == 0) && (1 <= bslen i <=> bslen o == 2 * bslen i - 1) } + -> i : ByteString + -> { o : ByteString | (bslen i == 0 <=> bslen o == 0) && (1 <= bslen i <=> bslen o == 2 * bslen i - 1) } assume Data.ByteString.Char8.foldl1 :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char) - -> { bs : Data.ByteString.ByteString | 1 <= bslen bs } + -> { bs : ByteString | 1 <= bslen bs } -> Char assume Data.ByteString.Char8.foldl1' :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char) - -> { bs : Data.ByteString.ByteString | 1 <= bslen bs } + -> { bs : ByteString | 1 <= bslen bs } -> GHC.Types.Char assume Data.ByteString.Char8.foldr1 :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char) - -> { bs : Data.ByteString.ByteString | 1 <= bslen bs } + -> { bs : ByteString | 1 <= bslen bs } -> Char assume Data.ByteString.Char8.foldr1' :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char) - -> { bs : Data.ByteString.ByteString | 1 <= bslen bs } + -> { bs : ByteString | 1 <= bslen bs } -> GHC.Types.Char assume Data.ByteString.Char8.concatMap - :: (GHC.Types.Char -> Data.ByteString.ByteString) - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen i == 0 ==> bslen o == 0 } + :: (GHC.Types.Char -> ByteString) + -> i : ByteString + -> { o : ByteString | bslen i == 0 ==> bslen o == 0 } assume Data.ByteString.Char8.any :: (GHC.Types.Char -> GHC.Types.Bool) - -> bs : Data.ByteString.ByteString + -> bs : ByteString -> { b : GHC.Types.Bool | bslen bs == 0 ==> not b } assume Data.ByteString.Char8.all :: (GHC.Types.Char -> GHC.Types.Bool) - -> bs : Data.ByteString.ByteString + -> bs : ByteString -> { b : GHC.Types.Bool | bslen bs == 0 ==> b } assume Data.ByteString.Char8.maximum - :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> GHC.Types.Char + :: { bs : ByteString | 1 <= bslen bs } -> GHC.Types.Char assume Data.ByteString.Char8.minimum - :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> GHC.Types.Char + :: { bs : ByteString | 1 <= bslen bs } -> GHC.Types.Char assume Data.ByteString.Char8.scanl :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char) -> GHC.Types.Char - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen o == bslen i } + -> i : ByteString + -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.Char8.scanl1 :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char) - -> i : { i : Data.ByteString.ByteString | 1 <= bslen i } - -> { o : Data.ByteString.ByteString | bslen o == bslen i } + -> i : { i : ByteString | 1 <= bslen i } + -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.Char8.scanr :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char) -> GHC.Types.Char - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen o == bslen i } + -> i : ByteString + -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.Char8.scanr1 :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char) - -> i : { i : Data.ByteString.ByteString | 1 <= bslen i } - -> { o : Data.ByteString.ByteString | bslen o == bslen i } + -> i : { i : ByteString | 1 <= bslen i } + -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.Char8.mapAccumL :: (acc -> GHC.Types.Char -> (acc, GHC.Types.Char)) -> acc - -> i : Data.ByteString.ByteString - -> (acc, { o : Data.ByteString.ByteString | bslen o == bslen i }) + -> i : ByteString + -> (acc, { o : ByteString | bslen o == bslen i }) assume Data.ByteString.Char8.mapAccumR :: (acc -> GHC.Types.Char -> (acc, GHC.Types.Char)) -> acc - -> i : Data.ByteString.ByteString - -> (acc, { o : Data.ByteString.ByteString | bslen o == bslen i }) + -> i : ByteString + -> (acc, { o : ByteString | bslen o == bslen i }) assume Data.ByteString.Char8.replicate :: n : Int -> GHC.Types.Char - -> { bs : Data.ByteString.ByteString | bslen bs == n } + -> { bs : ByteString | bslen bs == n } assume Data.ByteString.Char8.unfoldrN :: n : Int -> (a -> Maybe (GHC.Types.Char, a)) -> a - -> ({ bs : Data.ByteString.ByteString | bslen bs <= n }, Maybe a) + -> ({ bs : ByteString | bslen bs <= n }, Maybe a) assume Data.ByteString.Char8.takeWhile :: (GHC.Types.Char -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen o <= bslen i } + -> i : ByteString + -> { o : ByteString | bslen o <= bslen i } assume Data.ByteString.Char8.dropWhile :: (GHC.Types.Char -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen o <= bslen i } + -> i : ByteString + -> { o : ByteString | bslen o <= bslen i } assume Data.ByteString.Char8.span :: (GHC.Types.Char -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i } - , { r : Data.ByteString.ByteString | bslen r <= bslen i } + -> i : ByteString + -> ( { l : ByteString | bslen l <= bslen i } + , { r : ByteString | bslen r <= bslen i } ) assume Data.ByteString.Char8.spanEnd :: (GHC.Types.Char -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i } - , { r : Data.ByteString.ByteString | bslen r <= bslen i } + -> i : ByteString + -> ( { l : ByteString | bslen l <= bslen i } + , { r : ByteString | bslen r <= bslen i } ) assume Data.ByteString.Char8.break :: (GHC.Types.Char -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i } - , { r : Data.ByteString.ByteString | bslen r <= bslen i } + -> i : ByteString + -> ( { l : ByteString | bslen l <= bslen i } + , { r : ByteString | bslen r <= bslen i } ) assume Data.ByteString.Char8.breakEnd :: (GHC.Types.Char -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i } - , { r : Data.ByteString.ByteString | bslen r <= bslen i } + -> i : ByteString + -> ( { l : ByteString | bslen l <= bslen i } + , { r : ByteString | bslen r <= bslen i } ) assume Data.ByteString.Char8.groupBy :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> [{ o : Data.ByteString.ByteString | 1 <= bslen o && bslen o <= bslen i }] + -> i : ByteString + -> [{ o : ByteString | 1 <= bslen o && bslen o <= bslen i }] assume Data.ByteString.Char8.split :: GHC.Types.Char - -> i : Data.ByteString.ByteString - -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }] + -> i : ByteString + -> [{ o : ByteString | bslen o <= bslen i }] assume Data.ByteString.Char8.splitWith :: (GHC.Types.Char -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }] + -> i : ByteString + -> [{ o : ByteString | bslen o <= bslen i }] assume Data.ByteString.Char8.lines - :: i : Data.ByteString.ByteString - -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }] + :: i : ByteString + -> [{ o : ByteString | bslen o <= bslen i }] assume Data.ByteString.Char8.words - :: i : Data.ByteString.ByteString - -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }] + :: i : ByteString + -> [{ o : ByteString | bslen o <= bslen i }] assume Data.ByteString.Char8.unlines - :: is : [Data.ByteString.ByteString] - -> { o : Data.ByteString.ByteString | (len is == 0 <=> bslen o == 0) && bslen o >= len is } + :: is : [ByteString] + -> { o : ByteString | (len is == 0 <=> bslen o == 0) && bslen o >= len is } assume Data.ByteString.Char8.unwords - :: is : [Data.ByteString.ByteString] - -> { o : Data.ByteString.ByteString | (len is == 0 ==> bslen o == 0) && (1 <= len is ==> bslen o >= len is - 1) } + :: is : [ByteString] + -> { o : ByteString | (len is == 0 ==> bslen o == 0) && (1 <= len is ==> bslen o >= len is - 1) } assume Data.ByteString.Char8.elem :: GHC.Types.Char - -> bs : Data.ByteString.ByteString + -> bs : ByteString -> { b : GHC.Types.Bool | bslen bs == 0 ==> not b } assume Data.ByteString.Char8.notElem :: GHC.Types.Char - -> bs : Data.ByteString.ByteString + -> bs : ByteString -> { b : GHC.Types.Bool | bslen bs == 0 ==> b } assume Data.ByteString.Char8.find :: (GHC.Types.Char -> GHC.Types.Bool) - -> bs : Data.ByteString.ByteString + -> bs : ByteString -> Maybe { w8 : GHC.Types.Char | bslen bs /= 0 } assume Data.ByteString.Char8.filter :: (GHC.Types.Char -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen o <= bslen i } + -> i : ByteString + -> { o : ByteString | bslen o <= bslen i } assume Data.ByteString.Char8.index - :: bs : Data.ByteString.ByteString + :: bs : ByteString -> { n : Int | 0 <= n && n < bslen bs } -> GHC.Types.Char assume Data.ByteString.Char8.elemIndex :: GHC.Types.Char - -> bs : Data.ByteString.ByteString + -> bs : ByteString -> Maybe { n : Int | 0 <= n && n < bslen bs } assume Data.ByteString.Char8.elemIndices :: GHC.Types.Char - -> bs : Data.ByteString.ByteString + -> bs : ByteString -> [{ n : Int | 0 <= n && n < bslen bs }] assume Data.ByteString.Char8.elemIndexEnd :: GHC.Types.Char - -> bs : Data.ByteString.ByteString + -> bs : ByteString -> Maybe { n : Int | 0 <= n && n < bslen bs } assume Data.ByteString.Char8.findIndex :: (GHC.Types.Char -> GHC.Types.Bool) - -> bs : Data.ByteString.ByteString + -> bs : ByteString -> Maybe { n : Int | 0 <= n && n < bslen bs } assume Data.ByteString.Char8.findIndices :: (GHC.Types.Char -> GHC.Types.Bool) - -> bs : Data.ByteString.ByteString + -> bs : ByteString -> [{ n : Int | 0 <= n && n < bslen bs }] assume Data.ByteString.Char8.count :: GHC.Types.Char - -> bs : Data.ByteString.ByteString + -> bs : ByteString -> { n : Int | 0 <= n && n < bslen bs } assume Data.ByteString.Char8.zip - :: l : Data.ByteString.ByteString - -> r : Data.ByteString.ByteString + :: l : ByteString + -> r : ByteString -> { o : [(GHC.Types.Char, GHC.Types.Char)] | len o <= bslen l && len o <= bslen r } assume Data.ByteString.Char8.zipWith :: (GHC.Types.Char -> GHC.Types.Char -> a) - -> l : Data.ByteString.ByteString - -> r : Data.ByteString.ByteString + -> l : ByteString + -> r : ByteString -> { o : [a] | len o <= bslen l && len o <= bslen r } assume Data.ByteString.Char8.unzip :: i : [(GHC.Types.Char, GHC.Types.Char)] - -> ( { l : Data.ByteString.ByteString | bslen l == len i } - , { r : Data.ByteString.ByteString | bslen r == len i } + -> ( { l : ByteString | bslen l == len i } + , { r : ByteString | bslen r == len i } ) assume Data.ByteString.ReadInt.readInt - :: i : Data.ByteString.ByteString - -> Maybe { p : (Int, { o : Data.ByteString.ByteString | bslen o < bslen i}) | bslen i /= 0 } + :: i : ByteString + -> Maybe { p : (Int, { o : ByteString | bslen o < bslen i}) | bslen i /= 0 } assume Data.ByteString.ReadNat.readInteger - :: i : Data.ByteString.ByteString - -> Maybe { p : (Integer, { o : Data.ByteString.ByteString | bslen o < bslen i}) | bslen i /= 0 } + :: i : ByteString + -> Maybe { p : (Integer, { o : ByteString | bslen o < bslen i}) | bslen i /= 0 } @-} diff --git a/src/Data/ByteString/Lazy/Char8_LHAssumptions.hs b/src/Data/ByteString/Lazy/Char8_LHAssumptions.hs index 7976efd3aa..175a5413dd 100644 --- a/src/Data/ByteString/Lazy/Char8_LHAssumptions.hs +++ b/src/Data/ByteString/Lazy/Char8_LHAssumptions.hs @@ -5,252 +5,253 @@ module Data.ByteString.Lazy.Char8_LHAssumptions where import Data.ByteString.Lazy hiding (hGetNonBlocking, scanl) import Data.ByteString.Lazy.Char8 import Data.ByteString.Lazy_LHAssumptions() +import Data.Int {-@ -assume Data.ByteString.Lazy.Char8.last :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> GHC.Types.Char +assume Data.ByteString.Lazy.Char8.last :: { bs : ByteString | 1 <= bllen bs } -> Char assume Data.ByteString.Lazy.Char8.singleton - :: GHC.Types.Char -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == 1 } + :: Char -> { bs : ByteString | bllen bs == 1 } assume Data.ByteString.Lazy.Char8.pack - :: w8s : [GHC.Types.Char] - -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == len w8s } + :: w8s : [Char] + -> { bs : ByteString | bllen bs == len w8s } assume Data.ByteString.Lazy.Char8.unpack - :: bs : Data.ByteString.Lazy.ByteString - -> { w8s : [GHC.Types.Char] | len w8s == bllen bs } + :: bs : ByteString + -> { w8s : [Char] | len w8s == bllen bs } assume Data.ByteString.Lazy.Char8.cons - :: GHC.Types.Char - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i + 1 } + :: Char + -> i : ByteString + -> { o : ByteString | bllen o == bllen i + 1 } assume Data.ByteString.Lazy.Char8.snoc - :: i : Data.ByteString.Lazy.ByteString - -> GHC.Types.Char - -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i + 1 } + :: i : ByteString + -> Char + -> { o : ByteString | bllen o == bllen i + 1 } assume Data.ByteString.Lazy.Char8.head - :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } - -> GHC.Types.Char + :: { bs : ByteString | 1 <= bllen bs } + -> Char assume Data.ByteString.Lazy.Char8.uncons - :: i : Data.ByteString.Lazy.ByteString - -> Maybe (GHC.Types.Char, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i - 1 }) + :: i : ByteString + -> Maybe (Char, { o : ByteString | bllen o == bllen i - 1 }) assume Data.ByteString.Lazy.Char8.unsnoc - :: i : Data.ByteString.Lazy.ByteString - -> Maybe ({ o : Data.ByteString.Lazy.ByteString | bllen o == bllen i - 1 }, GHC.Types.Char) + :: i : ByteString + -> Maybe ({ o : ByteString | bllen o == bllen i - 1 }, Char) assume Data.ByteString.Lazy.Char8.map - :: (GHC.Types.Char -> GHC.Types.Char) - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i } + :: (Char -> Char) + -> i : ByteString + -> { o : ByteString | bllen o == bllen i } assume Data.ByteString.Lazy.Char8.intersperse - :: GHC.Types.Char - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | (bllen i == 0 <=> bllen o == 0) && (1 <= bllen i <=> bllen o == 2 * bllen i - 1) } + :: Char + -> i : ByteString + -> { o : ByteString | (bllen i == 0 <=> bllen o == 0) && (1 <= bllen i <=> bllen o == 2 * bllen i - 1) } assume Data.ByteString.Lazy.Char8.foldl1 - :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char) - -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } - -> GHC.Types.Char + :: (Char -> Char -> Char) + -> { bs : ByteString | 1 <= bllen bs } + -> Char assume Data.ByteString.Lazy.Char8.foldl1' - :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char) - -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } - -> GHC.Types.Char + :: (Char -> Char -> Char) + -> { bs : ByteString | 1 <= bllen bs } + -> Char assume Data.ByteString.Lazy.Char8.foldr1 - :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char) - -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } - -> GHC.Types.Char + :: (Char -> Char -> Char) + -> { bs : ByteString | 1 <= bllen bs } + -> Char assume Data.ByteString.Lazy.Char8.concatMap - :: (GHC.Types.Char -> Data.ByteString.Lazy.ByteString) - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen i == 0 ==> bllen o == 0 } + :: (Char -> ByteString) + -> i : ByteString + -> { o : ByteString | bllen i == 0 ==> bllen o == 0 } -assume Data.ByteString.Lazy.Char8.any :: (GHC.Types.Char -> GHC.Types.Bool) - -> bs : Data.ByteString.Lazy.ByteString - -> { b : GHC.Types.Bool | bllen bs == 0 ==> not b } +assume Data.ByteString.Lazy.Char8.any :: (Char -> Bool) + -> bs : ByteString + -> { b : Bool | bllen bs == 0 ==> not b } -assume Data.ByteString.Lazy.Char8.all :: (GHC.Types.Char -> GHC.Types.Bool) - -> bs : Data.ByteString.Lazy.ByteString - -> { b : GHC.Types.Bool | bllen bs == 0 ==> b } +assume Data.ByteString.Lazy.Char8.all :: (Char -> Bool) + -> bs : ByteString + -> { b : Bool | bllen bs == 0 ==> b } -assume Data.ByteString.Lazy.Char8.maximum :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> GHC.Types.Char +assume Data.ByteString.Lazy.Char8.maximum :: { bs : ByteString | 1 <= bllen bs } -> Char -assume Data.ByteString.Lazy.Char8.minimum :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> GHC.Types.Char +assume Data.ByteString.Lazy.Char8.minimum :: { bs : ByteString | 1 <= bllen bs } -> Char assume Data.ByteString.Lazy.Char8.scanl - :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char) - -> GHC.Types.Char - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i } + :: (Char -> Char -> Char) + -> Char + -> i : ByteString + -> { o : ByteString | bllen o == bllen i } assume Data.ByteString.Lazy.Char8.scanl1 - :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char) - -> i : { i : Data.ByteString.Lazy.ByteString | 1 <= bllen i } - -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i } + :: (Char -> Char -> Char) + -> i : { i : ByteString | 1 <= bllen i } + -> { o : ByteString | bllen o == bllen i } assume Data.ByteString.Lazy.Char8.scanr - :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char) - -> GHC.Types.Char - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i } + :: (Char -> Char -> Char) + -> Char + -> i : ByteString + -> { o : ByteString | bllen o == bllen i } assume Data.ByteString.Lazy.Char8.scanr1 - :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Char) - -> i : { i : Data.ByteString.Lazy.ByteString | 1 <= bllen i } - -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i } + :: (Char -> Char -> Char) + -> i : { i : ByteString | 1 <= bllen i } + -> { o : ByteString | bllen o == bllen i } assume Data.ByteString.Lazy.Char8.mapAccumL - :: (acc -> GHC.Types.Char -> (acc, GHC.Types.Char)) + :: (acc -> Char -> (acc, Char)) -> acc - -> i : Data.ByteString.Lazy.ByteString - -> (acc, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }) + -> i : ByteString + -> (acc, { o : ByteString | bllen o == bllen i }) assume Data.ByteString.Lazy.Char8.mapAccumR - :: (acc -> GHC.Types.Char -> (acc, GHC.Types.Char)) + :: (acc -> Char -> (acc, Char)) -> acc - -> i : Data.ByteString.Lazy.ByteString - -> (acc, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }) + -> i : ByteString + -> (acc, { o : ByteString | bllen o == bllen i }) assume Data.ByteString.Lazy.Char8.replicate :: n : Int64 - -> GHC.Types.Char - -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == n } + -> Char + -> { bs : ByteString | bllen bs == n } assume Data.ByteString.Lazy.Char8.takeWhile - :: (GHC.Types.Char -> GHC.Types.Bool) - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i } + :: (Char -> Bool) + -> i : ByteString + -> { o : ByteString | bllen o <= bllen i } assume Data.ByteString.Lazy.Char8.dropWhile - :: (GHC.Types.Char -> GHC.Types.Bool) - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i } + :: (Char -> Bool) + -> i : ByteString + -> { o : ByteString | bllen o <= bllen i } assume Data.ByteString.Lazy.Char8.span - :: (GHC.Types.Char -> GHC.Types.Bool) - -> i : Data.ByteString.Lazy.ByteString - -> ( { l : Data.ByteString.Lazy.ByteString | bllen l <= bllen i } - , { r : Data.ByteString.Lazy.ByteString | bllen r <= bllen i } + :: (Char -> Bool) + -> i : ByteString + -> ( { l : ByteString | bllen l <= bllen i } + , { r : ByteString | bllen r <= bllen i } ) assume Data.ByteString.Lazy.Char8.break - :: (GHC.Types.Char -> GHC.Types.Bool) - -> i : Data.ByteString.Lazy.ByteString - -> ( { l : Data.ByteString.Lazy.ByteString | bllen l <= bllen i } - , { r : Data.ByteString.Lazy.ByteString | bllen r <= bllen i } + :: (Char -> Bool) + -> i : ByteString + -> ( { l : ByteString | bllen l <= bllen i } + , { r : ByteString | bllen r <= bllen i } ) assume Data.ByteString.Lazy.Char8.groupBy - :: (GHC.Types.Char -> GHC.Types.Char -> GHC.Types.Bool) - -> i : Data.ByteString.Lazy.ByteString - -> [{ o : Data.ByteString.Lazy.ByteString | 1 <= bllen o && bllen o <= bllen i }] + :: (Char -> Char -> Bool) + -> i : ByteString + -> [{ o : ByteString | 1 <= bllen o && bllen o <= bllen i }] assume Data.ByteString.Lazy.Char8.split - :: GHC.Types.Char - -> i : Data.ByteString.Lazy.ByteString - -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }] + :: Char + -> i : ByteString + -> [{ o : ByteString | bllen o <= bllen i }] assume Data.ByteString.Lazy.Char8.splitWith - :: (GHC.Types.Char -> GHC.Types.Bool) - -> i : Data.ByteString.Lazy.ByteString - -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }] + :: (Char -> Bool) + -> i : ByteString + -> [{ o : ByteString | bllen o <= bllen i }] assume Data.ByteString.Lazy.Char8.lines - :: i : Data.ByteString.Lazy.ByteString - -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }] + :: i : ByteString + -> [{ o : ByteString | bllen o <= bllen i }] assume Data.ByteString.Lazy.Char8.words - :: i : Data.ByteString.Lazy.ByteString - -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }] + :: i : ByteString + -> [{ o : ByteString | bllen o <= bllen i }] assume Data.ByteString.Lazy.Char8.unlines - :: is : [Data.ByteString.Lazy.ByteString] - -> { o : Data.ByteString.Lazy.ByteString | (len is == 0 <=> bllen o == 0) && bllen o >= len is } + :: is : [ByteString] + -> { o : ByteString | (len is == 0 <=> bllen o == 0) && bllen o >= len is } assume Data.ByteString.Lazy.Char8.unwords - :: is : [Data.ByteString.Lazy.ByteString] - -> { o : Data.ByteString.Lazy.ByteString | (len is == 0 ==> bllen o == 0) && (1 <= len is ==> bllen o >= len is - 1) } + :: is : [ByteString] + -> { o : ByteString | (len is == 0 ==> bllen o == 0) && (1 <= len is ==> bllen o >= len is - 1) } assume Data.ByteString.Lazy.Char8.elem - :: GHC.Types.Char - -> bs : Data.ByteString.Lazy.ByteString - -> { b : GHC.Types.Bool | bllen bs == 0 ==> not b } + :: Char + -> bs : ByteString + -> { b : Bool | bllen bs == 0 ==> not b } assume Data.ByteString.Lazy.Char8.notElem - :: GHC.Types.Char - -> bs : Data.ByteString.Lazy.ByteString - -> { b : GHC.Types.Bool | bllen bs == 0 ==> b } + :: Char + -> bs : ByteString + -> { b : Bool | bllen bs == 0 ==> b } assume Data.ByteString.Lazy.Char8.find - :: (GHC.Types.Char -> GHC.Types.Bool) - -> bs : Data.ByteString.Lazy.ByteString - -> Maybe { w8 : GHC.Types.Char | bllen bs /= 0 } + :: (Char -> Bool) + -> bs : ByteString + -> Maybe { w8 : Char | bllen bs /= 0 } assume Data.ByteString.Lazy.Char8.filter - :: (GHC.Types.Char -> GHC.Types.Bool) - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i } + :: (Char -> Bool) + -> i : ByteString + -> { o : ByteString | bllen o <= bllen i } assume Data.ByteString.Lazy.Char8.index - :: bs : Data.ByteString.Lazy.ByteString + :: bs : ByteString -> { n : Int64 | 0 <= n && n < bllen bs } - -> GHC.Types.Char + -> Char assume Data.ByteString.Lazy.Char8.elemIndex - :: GHC.Types.Char - -> bs : Data.ByteString.Lazy.ByteString + :: Char + -> bs : ByteString -> Maybe { n : Int64 | 0 <= n && n < bllen bs } assume Data.ByteString.Lazy.Char8.elemIndices - :: GHC.Types.Char - -> bs : Data.ByteString.Lazy.ByteString + :: Char + -> bs : ByteString -> [{ n : Int64 | 0 <= n && n < bllen bs }] assume Data.ByteString.Lazy.Char8.findIndex - :: (GHC.Types.Char -> GHC.Types.Bool) - -> bs : Data.ByteString.Lazy.ByteString + :: (Char -> Bool) + -> bs : ByteString -> Maybe { n : Int64 | 0 <= n && n < bllen bs } assume Data.ByteString.Lazy.Char8.findIndices - :: (GHC.Types.Char -> GHC.Types.Bool) - -> bs : Data.ByteString.Lazy.ByteString + :: (Char -> Bool) + -> bs : ByteString -> [{ n : Int64 | 0 <= n && n < bllen bs }] assume Data.ByteString.Lazy.Char8.count - :: GHC.Types.Char - -> bs : Data.ByteString.Lazy.ByteString + :: Char + -> bs : ByteString -> { n : Int64 | 0 <= n && n < bllen bs } assume Data.ByteString.Lazy.Char8.zip - :: l : Data.ByteString.Lazy.ByteString - -> r : Data.ByteString.Lazy.ByteString - -> { o : [(GHC.Types.Char, GHC.Types.Char)] | len o <= bllen l && len o <= bllen r } + :: l : ByteString + -> r : ByteString + -> { o : [(Char, Char)] | len o <= bllen l && len o <= bllen r } assume Data.ByteString.Lazy.Char8.zipWith - :: (GHC.Types.Char -> GHC.Types.Char -> a) - -> l : Data.ByteString.Lazy.ByteString - -> r : Data.ByteString.Lazy.ByteString + :: (Char -> Char -> a) + -> l : ByteString + -> r : ByteString -> { o : [a] | len o <= bllen l && len o <= bllen r } assume Data.ByteString.Lazy.Char8.unzip - :: i : [(GHC.Types.Char, GHC.Types.Char)] - -> ( { l : Data.ByteString.Lazy.ByteString | bllen l == len i } - , { r : Data.ByteString.Lazy.ByteString | bllen r == len i } + :: i : [(Char, Char)] + -> ( { l : ByteString | bllen l == len i } + , { r : ByteString | bllen r == len i } ) assume Data.ByteString.Lazy.ReadInt.readInt - :: i : Data.ByteString.Lazy.ByteString - -> Maybe { p : (Int, { o : Data.ByteString.Lazy.ByteString | bllen o < bllen i}) | bllen i /= 0 } + :: i : ByteString + -> Maybe { p : (Int, { o : ByteString | bllen o < bllen i}) | bllen i /= 0 } assume Data.ByteString.Lazy.ReadNat.readInteger - :: i : Data.ByteString.Lazy.ByteString - -> Maybe { p : (Integer, { o : Data.ByteString.Lazy.ByteString | bllen o < bllen i}) | bllen i /= 0 } + :: i : ByteString + -> Maybe { p : (Integer, { o : ByteString | bllen o < bllen i}) | bllen i /= 0 } @-} diff --git a/src/Data/ByteString/Lazy_LHAssumptions.hs b/src/Data/ByteString/Lazy_LHAssumptions.hs index 3ffb7593f0..2eabdae61a 100644 --- a/src/Data/ByteString/Lazy_LHAssumptions.hs +++ b/src/Data/ByteString/Lazy_LHAssumptions.hs @@ -2,344 +2,345 @@ {-# OPTIONS_GHC -Wno-unused-imports #-} module Data.ByteString.Lazy_LHAssumptions where -import Data.ByteString +import qualified Data.ByteString import Data.ByteString_LHAssumptions() import Data.ByteString.Lazy +import Data.Int import Data.String_LHAssumptions() import GHC.Int_LHAssumptions() {-@ -measure bllen :: Data.ByteString.Lazy.ByteString -> { n : GHC.Internal.Int.Int64 | 0 <= n } +measure bllen :: ByteString -> { n : Int64 | 0 <= n } -invariant { bs : Data.ByteString.Lazy.ByteString | 0 <= bllen bs } +invariant { bs : ByteString | 0 <= bllen bs } -invariant { bs : Data.ByteString.Lazy.ByteString | bllen bs == stringlen bs } +invariant { bs : ByteString | bllen bs == stringlen bs } -assume Data.ByteString.Lazy.empty :: { bs : Data.ByteString.Lazy.ByteString | bllen bs == 0 } +assume Data.ByteString.Lazy.empty :: { bs : ByteString | bllen bs == 0 } assume Data.ByteString.Lazy.singleton - :: _ -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == 1 } + :: _ -> { bs : ByteString | bllen bs == 1 } assume Data.ByteString.Lazy.pack :: w8s : [_] -> { bs : _ | bllen bs == len w8s } assume Data.ByteString.Lazy.unpack - :: bs : Data.ByteString.Lazy.ByteString + :: bs : ByteString -> { w8s : [_] | len w8s == bllen bs } assume Data.ByteString.Lazy.Internal.fromStrict :: i : Data.ByteString.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen o == bslen i } + -> { o : ByteString | bllen o == bslen i } assume Data.ByteString.Lazy.Internal.toStrict - :: i : Data.ByteString.Lazy.ByteString + :: i : ByteString -> { o : Data.ByteString.ByteString | bslen o == bllen i } assume Data.ByteString.Lazy.fromChunks :: i : [Data.ByteString.ByteString] - -> { o : Data.ByteString.Lazy.ByteString | len i == 0 <=> bllen o == 0 } + -> { o : ByteString | len i == 0 <=> bllen o == 0 } assume Data.ByteString.Lazy.toChunks - :: i : Data.ByteString.Lazy.ByteString + :: i : ByteString -> { os : [{ o : Data.ByteString.ByteString | bslen o <= bllen i}] | len os == 0 <=> bllen i == 0 } assume Data.ByteString.Lazy.cons :: _ - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i + 1 } + -> i : ByteString + -> { o : ByteString | bllen o == bllen i + 1 } assume Data.ByteString.Lazy.snoc - :: i : Data.ByteString.Lazy.ByteString + :: i : ByteString -> _ - -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i + 1 } + -> { o : ByteString | bllen o == bllen i + 1 } assume Data.ByteString.Lazy.append - :: l : Data.ByteString.Lazy.ByteString - -> r : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen l + bllen r } + :: l : ByteString + -> r : ByteString + -> { o : ByteString | bllen o == bllen l + bllen r } assume Data.ByteString.Lazy.head - :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } + :: { bs : ByteString | 1 <= bllen bs } -> _ assume Data.ByteString.Lazy.uncons - :: i : Data.ByteString.Lazy.ByteString - -> Maybe (_, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i - 1 }) + :: i : ByteString + -> Maybe (_, { o : ByteString | bllen o == bllen i - 1 }) assume Data.ByteString.Lazy.unsnoc - :: i : Data.ByteString.Lazy.ByteString - -> Maybe ({ o : Data.ByteString.Lazy.ByteString | bllen o == bllen i - 1 }, _) + :: i : ByteString + -> Maybe ({ o : ByteString | bllen o == bllen i - 1 }, _) -assume Data.ByteString.Lazy.last :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _ +assume Data.ByteString.Lazy.last :: { bs : ByteString | 1 <= bllen bs } -> _ -assume Data.ByteString.Lazy.tail :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _ +assume Data.ByteString.Lazy.tail :: { bs : ByteString | 1 <= bllen bs } -> _ -assume Data.ByteString.Lazy.init :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _ +assume Data.ByteString.Lazy.init :: { bs : ByteString | 1 <= bllen bs } -> _ -assume Data.ByteString.Lazy.null :: bs : Data.ByteString.Lazy.ByteString -> { b : GHC.Types.Bool | b <=> bllen bs == 0 } +assume Data.ByteString.Lazy.null :: bs : ByteString -> { b : Bool | b <=> bllen bs == 0 } assume Data.ByteString.Lazy.length - :: bs : Data.ByteString.Lazy.ByteString -> { n : GHC.Internal.Int.Int64 | bllen bs == n } + :: bs : ByteString -> { n : Int64 | bllen bs == n } assume Data.ByteString.Lazy.map :: (_ -> _) - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i } + -> i : ByteString + -> { o : ByteString | bllen o == bllen i } assume Data.ByteString.Lazy.reverse - :: i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i } + :: i : ByteString + -> { o : ByteString | bllen o == bllen i } assume Data.ByteString.Lazy.intersperse :: _ - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | (bllen i == 0 <=> bllen o == 0) && (1 <= bllen i <=> bllen o == 2 * bllen i - 1) } + -> i : ByteString + -> { o : ByteString | (bllen i == 0 <=> bllen o == 0) && (1 <= bllen i <=> bllen o == 2 * bllen i - 1) } assume Data.ByteString.Lazy.intercalate - :: l : Data.ByteString.Lazy.ByteString - -> rs : [Data.ByteString.Lazy.ByteString] - -> { o : Data.ByteString.Lazy.ByteString | len rs == 0 ==> bllen o == 0 } + :: l : ByteString + -> rs : [ByteString] + -> { o : ByteString | len rs == 0 ==> bllen o == 0 } assume Data.ByteString.Lazy.transpose - :: is : [Data.ByteString.Lazy.ByteString] - -> { os : [{ bs : Data.ByteString.Lazy.ByteString | bllen bs <= len is }] | len is == 0 ==> len os == 0} + :: is : [ByteString] + -> { os : [{ bs : ByteString | bllen bs <= len is }] | len is == 0 ==> len os == 0} assume Data.ByteString.Lazy.foldl1 :: (_ -> _ -> _) - -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } + -> { bs : ByteString | 1 <= bllen bs } -> _ assume Data.ByteString.Lazy.foldl1' :: (_ -> _ -> _) - -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } + -> { bs : ByteString | 1 <= bllen bs } -> _ assume Data.ByteString.Lazy.foldr1 :: (_ -> _ -> _) - -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } + -> { bs : ByteString | 1 <= bllen bs } -> _ assume Data.ByteString.Lazy.concat - :: is : [Data.ByteString.Lazy.ByteString] - -> { o : Data.ByteString.Lazy.ByteString | (len is == 0) ==> (bllen o == 0) } + :: is : [ByteString] + -> { o : ByteString | (len is == 0) ==> (bllen o == 0) } assume Data.ByteString.Lazy.concatMap - :: (_ -> Data.ByteString.Lazy.ByteString) - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen i == 0 ==> bllen o == 0 } + :: (_ -> ByteString) + -> i : ByteString + -> { o : ByteString | bllen i == 0 ==> bllen o == 0 } -assume Data.ByteString.Lazy.any :: (_ -> GHC.Types.Bool) - -> bs : Data.ByteString.Lazy.ByteString - -> { b : GHC.Types.Bool | bllen bs == 0 ==> not b } +assume Data.ByteString.Lazy.any :: (_ -> Bool) + -> bs : ByteString + -> { b : Bool | bllen bs == 0 ==> not b } -assume Data.ByteString.Lazy.all :: (_ -> GHC.Types.Bool) - -> bs : Data.ByteString.Lazy.ByteString - -> { b : GHC.Types.Bool | bllen bs == 0 ==> b } +assume Data.ByteString.Lazy.all :: (_ -> Bool) + -> bs : ByteString + -> { b : Bool | bllen bs == 0 ==> b } -assume Data.ByteString.Lazy.maximum :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _ +assume Data.ByteString.Lazy.maximum :: { bs : ByteString | 1 <= bllen bs } -> _ -assume Data.ByteString.Lazy.minimum :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _ +assume Data.ByteString.Lazy.minimum :: { bs : ByteString | 1 <= bllen bs } -> _ assume Data.ByteString.Lazy.scanl :: (_ -> _ -> _) -> _ - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i } + -> i : ByteString + -> { o : ByteString | bllen o == bllen i } assume Data.ByteString.Lazy.mapAccumL :: (acc -> _ -> (acc, _)) -> acc - -> i : Data.ByteString.Lazy.ByteString - -> (acc, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }) + -> i : ByteString + -> (acc, { o : ByteString | bllen o == bllen i }) assume Data.ByteString.Lazy.mapAccumR :: (acc -> _ -> (acc, _)) -> acc - -> i : Data.ByteString.Lazy.ByteString - -> (acc, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }) + -> i : ByteString + -> (acc, { o : ByteString | bllen o == bllen i }) assume Data.ByteString.Lazy.replicate - :: n : GHC.Internal.Int.Int64 + :: n : Int64 -> _ - -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == n } + -> { bs : ByteString | bllen bs == n } assume Data.ByteString.Lazy.take - :: n : GHC.Internal.Int.Int64 - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | (n <= 0 ==> bllen o == 0) && + :: n : Int64 + -> i : ByteString + -> { o : ByteString | (n <= 0 ==> bllen o == 0) && ((0 <= n && n <= bllen i) <=> bllen o == n) && (bllen i <= n <=> bllen o = bllen i) } assume Data.ByteString.Lazy.drop - :: n : GHC.Internal.Int.Int64 - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen o == bllen i) && + :: n : Int64 + -> i : ByteString + -> { o : ByteString | (n <= 0 <=> bllen o == bllen i) && ((0 <= n && n <= bllen i) <=> bllen o == bllen i - n) && (bllen i <= n <=> bllen o == 0) } assume Data.ByteString.Lazy.splitAt - :: n : GHC.Internal.Int.Int64 - -> i : Data.ByteString.Lazy.ByteString - -> ( { l : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen l == 0) && + :: n : Int64 + -> i : ByteString + -> ( { l : ByteString | (n <= 0 <=> bllen l == 0) && ((0 <= n && n <= bllen i) <=> bllen l == n) && (bllen i <= n <=> bllen l == bllen i) } - , { r : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen r == bllen i) && + , { r : ByteString | (n <= 0 <=> bllen r == bllen i) && ((0 <= n && n <= bllen i) <=> bllen r == bllen i - n) && (bllen i <= n <=> bllen r == 0) } ) assume Data.ByteString.Lazy.takeWhile - :: (_ -> GHC.Types.Bool) - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i } + :: (_ -> Bool) + -> i : ByteString + -> { o : ByteString | bllen o <= bllen i } assume Data.ByteString.Lazy.dropWhile - :: (_ -> GHC.Types.Bool) - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i } + :: (_ -> Bool) + -> i : ByteString + -> { o : ByteString | bllen o <= bllen i } assume Data.ByteString.Lazy.span - :: (_ -> GHC.Types.Bool) - -> i : Data.ByteString.Lazy.ByteString - -> ( { l : Data.ByteString.Lazy.ByteString | bllen l <= bllen i } - , { r : Data.ByteString.Lazy.ByteString | bllen r <= bllen i } + :: (_ -> Bool) + -> i : ByteString + -> ( { l : ByteString | bllen l <= bllen i } + , { r : ByteString | bllen r <= bllen i } ) assume Data.ByteString.Lazy.break - :: (_ -> GHC.Types.Bool) - -> i : Data.ByteString.Lazy.ByteString - -> ( { l : Data.ByteString.Lazy.ByteString | bllen l <= bllen i } - , { r : Data.ByteString.Lazy.ByteString | bllen r <= bllen i } + :: (_ -> Bool) + -> i : ByteString + -> ( { l : ByteString | bllen l <= bllen i } + , { r : ByteString | bllen r <= bllen i } ) assume Data.ByteString.Lazy.group - :: i : Data.ByteString.Lazy.ByteString - -> [{ o : Data.ByteString.Lazy.ByteString | 1 <= bllen o && bllen o <= bllen i }] + :: i : ByteString + -> [{ o : ByteString | 1 <= bllen o && bllen o <= bllen i }] assume Data.ByteString.Lazy.groupBy - :: (_ -> _ -> GHC.Types.Bool) - -> i : Data.ByteString.Lazy.ByteString - -> [{ o : Data.ByteString.Lazy.ByteString | 1 <= bllen o && bllen o <= bllen i }] + :: (_ -> _ -> Bool) + -> i : ByteString + -> [{ o : ByteString | 1 <= bllen o && bllen o <= bllen i }] assume Data.ByteString.Lazy.inits - :: i : Data.ByteString.Lazy.ByteString - -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }] + :: i : ByteString + -> [{ o : ByteString | bllen o <= bllen i }] assume Data.ByteString.Lazy.tails - :: i : Data.ByteString.Lazy.ByteString - -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }] + :: i : ByteString + -> [{ o : ByteString | bllen o <= bllen i }] assume Data.ByteString.Lazy.split :: _ - -> i : Data.ByteString.Lazy.ByteString - -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }] + -> i : ByteString + -> [{ o : ByteString | bllen o <= bllen i }] assume Data.ByteString.Lazy.splitWith - :: (_ -> GHC.Types.Bool) - -> i : Data.ByteString.Lazy.ByteString - -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }] + :: (_ -> Bool) + -> i : ByteString + -> [{ o : ByteString | bllen o <= bllen i }] assume Data.ByteString.Lazy.isPrefixOf - :: l : Data.ByteString.Lazy.ByteString - -> r : Data.ByteString.Lazy.ByteString - -> { b : GHC.Types.Bool | bllen l >= bllen r ==> not b } + :: l : ByteString + -> r : ByteString + -> { b : Bool | bllen l >= bllen r ==> not b } assume Data.ByteString.Lazy.isSuffixOf - :: l : Data.ByteString.Lazy.ByteString - -> r : Data.ByteString.Lazy.ByteString - -> { b : GHC.Types.Bool | bllen l >= bllen r ==> not b } + :: l : ByteString + -> r : ByteString + -> { b : Bool | bllen l >= bllen r ==> not b } assume Data.ByteString.Lazy.elem :: _ - -> bs : Data.ByteString.Lazy.ByteString - -> { b : GHC.Types.Bool | (bllen bs == 0) ==> not b } + -> bs : ByteString + -> { b : Bool | (bllen bs == 0) ==> not b } assume Data.ByteString.Lazy.notElem :: _ - -> bs : Data.ByteString.Lazy.ByteString - -> { b : GHC.Types.Bool | (bllen bs == 0) ==> b } + -> bs : ByteString + -> { b : Bool | (bllen bs == 0) ==> b } assume Data.ByteString.Lazy.find - :: (_ -> GHC.Types.Bool) - -> bs : Data.ByteString.Lazy.ByteString + :: (_ -> Bool) + -> bs : ByteString -> Maybe { w8 : _ | bllen bs /= 0 } assume Data.ByteString.Lazy.filter - :: (_ -> GHC.Types.Bool) - -> i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i } + :: (_ -> Bool) + -> i : ByteString + -> { o : ByteString | bllen o <= bllen i } assume Data.ByteString.Lazy.partition - :: (_ -> GHC.Types.Bool) - -> i : Data.ByteString.Lazy.ByteString - -> ( { l : Data.ByteString.Lazy.ByteString | bllen l <= bllen i } - , { r : Data.ByteString.Lazy.ByteString | bllen r <= bllen i } + :: (_ -> Bool) + -> i : ByteString + -> ( { l : ByteString | bllen l <= bllen i } + , { r : ByteString | bllen r <= bllen i } ) assume Data.ByteString.Lazy.index - :: bs : Data.ByteString.Lazy.ByteString - -> { n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs } + :: bs : ByteString + -> { n : Int64 | 0 <= n && n < bllen bs } -> _ assume Data.ByteString.Lazy.elemIndex :: _ - -> bs : Data.ByteString.Lazy.ByteString - -> Maybe { n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs } + -> bs : ByteString + -> Maybe { n : Int64 | 0 <= n && n < bllen bs } assume Data.ByteString.Lazy.elemIndices :: _ - -> bs : Data.ByteString.Lazy.ByteString - -> [{ n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs }] + -> bs : ByteString + -> [{ n : Int64 | 0 <= n && n < bllen bs }] assume Data.ByteString.Lazy.elemIndexEnd :: _ - -> bs : Data.ByteString.Lazy.ByteString - -> Maybe { n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs } + -> bs : ByteString + -> Maybe { n : Int64 | 0 <= n && n < bllen bs } assume Data.ByteString.Lazy.findIndex - :: (_ -> GHC.Types.Bool) - -> bs : Data.ByteString.Lazy.ByteString - -> Maybe { n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs } + :: (_ -> Bool) + -> bs : ByteString + -> Maybe { n : Int64 | 0 <= n && n < bllen bs } assume Data.ByteString.Lazy.findIndices - :: (_ -> GHC.Types.Bool) - -> bs : Data.ByteString.Lazy.ByteString - -> [{ n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs }] + :: (_ -> Bool) + -> bs : ByteString + -> [{ n : Int64 | 0 <= n && n < bllen bs }] assume Data.ByteString.Lazy.count :: _ - -> bs : Data.ByteString.Lazy.ByteString - -> { n : GHC.Internal.Int.Int64 | 0 <= n && n < bllen bs } + -> bs : ByteString + -> { n : Int64 | 0 <= n && n < bllen bs } assume Data.ByteString.Lazy.zip - :: l : Data.ByteString.Lazy.ByteString - -> r : Data.ByteString.Lazy.ByteString + :: l : ByteString + -> r : ByteString -> { o : [(_, _)] | len o <= bllen l && len o <= bllen r } assume Data.ByteString.Lazy.zipWith :: (_ -> _ -> a) - -> l : Data.ByteString.Lazy.ByteString - -> r : Data.ByteString.Lazy.ByteString + -> l : ByteString + -> r : ByteString -> { o : [a] | len o <= bllen l && len o <= bllen r } assume Data.ByteString.Lazy.unzip :: i : [(_, _)] - -> ( { l : Data.ByteString.Lazy.ByteString | bllen l == len i } - , { r : Data.ByteString.Lazy.ByteString | bllen r == len i } + -> ( { l : ByteString | bllen l == len i } + , { r : ByteString | bllen r == len i } ) assume Data.ByteString.Lazy.copy - :: i : Data.ByteString.Lazy.ByteString - -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i } + :: i : ByteString + -> { o : ByteString | bllen o == bllen i } assume Data.ByteString.Lazy.hGet :: _ -> n : { n : Int | 0 <= n } - -> IO { bs : Data.ByteString.Lazy.ByteString | bllen bs == n || bllen bs == 0 } + -> IO { bs : ByteString | bllen bs == n || bllen bs == 0 } assume Data.ByteString.Lazy.hGetNonBlocking :: _ -> n : { n : Int | 0 <= n } - -> IO { bs : Data.ByteString.Lazy.ByteString | bllen bs <= n } + -> IO { bs : ByteString | bllen bs <= n } @-} diff --git a/src/Data/ByteString/Short_LHAssumptions.hs b/src/Data/ByteString/Short_LHAssumptions.hs index 3add547bb5..2b422e3b8e 100644 --- a/src/Data/ByteString/Short_LHAssumptions.hs +++ b/src/Data/ByteString/Short_LHAssumptions.hs @@ -6,27 +6,28 @@ import Data.ByteString import Data.ByteString_LHAssumptions() import Data.ByteString.Short import Data.String_LHAssumptions() +import Data.Word {-@ -measure sbslen :: Data.ByteString.Short.ShortByteString -> { n : Int | 0 <= n } +measure sbslen :: ShortByteString -> { n : Int | 0 <= n } -invariant { bs : Data.ByteString.Short.ShortByteString | 0 <= sbslen bs } +invariant { bs : ShortByteString | 0 <= sbslen bs } -invariant { bs : Data.ByteString.Short.ShortByteString | sbslen bs == stringlen bs } +invariant { bs : ShortByteString | sbslen bs == stringlen bs } -assume Data.ByteString.Short.Internal.toShort :: i : Data.ByteString.ByteString -> { o : Data.ByteString.Short.ShortByteString | sbslen o == bslen i } +assume Data.ByteString.Short.Internal.toShort :: i : ByteString -> { o : ShortByteString | sbslen o == bslen i } -assume Data.ByteString.Short.Internal.fromShort :: o : Data.ByteString.Short.ShortByteString -> { i : Data.ByteString.ByteString | bslen i == sbslen o } +assume Data.ByteString.Short.Internal.fromShort :: o : ShortByteString -> { i : ByteString | bslen i == sbslen o } -assume Data.ByteString.Short.Internal.pack :: w8s : [Word8] -> { bs : Data.ByteString.Short.ShortByteString | sbslen bs == len w8s } +assume Data.ByteString.Short.Internal.pack :: w8s : [Word8] -> { bs : ShortByteString | sbslen bs == len w8s } -assume Data.ByteString.Short.Internal.unpack :: bs : Data.ByteString.Short.ShortByteString -> { w8s : [Word8] | len w8s == sbslen bs } +assume Data.ByteString.Short.Internal.unpack :: bs : ShortByteString -> { w8s : [Word8] | len w8s == sbslen bs } -assume Data.ByteString.Short.Internal.empty :: { bs : Data.ByteString.Short.ShortByteString | sbslen bs == 0 } +assume Data.ByteString.Short.Internal.empty :: { bs : ShortByteString | sbslen bs == 0 } -assume Data.ByteString.Short.Internal.null :: bs : Data.ByteString.Short.ShortByteString -> { b : GHC.Types.Bool | b <=> sbslen bs == 0 } +assume Data.ByteString.Short.Internal.null :: bs : ShortByteString -> { b : Bool | b <=> sbslen bs == 0 } -assume Data.ByteString.Short.Internal.length :: bs : Data.ByteString.Short.ShortByteString -> { n : Int | sbslen bs == n } +assume Data.ByteString.Short.Internal.length :: bs : ShortByteString -> { n : Int | sbslen bs == n } -assume Data.ByteString.Short.Internal.index :: bs : Data.ByteString.Short.ShortByteString -> { n : Int | 0 <= n && n < sbslen bs } -> Word8 +assume Data.ByteString.Short.Internal.index :: bs : ShortByteString -> { n : Int | 0 <= n && n < sbslen bs } -> Word8 @-} diff --git a/src/Data/ByteString/Unsafe_LHAssumptions.hs b/src/Data/ByteString/Unsafe_LHAssumptions.hs index 29982a8b5f..d7639d5adb 100644 --- a/src/Data/ByteString/Unsafe_LHAssumptions.hs +++ b/src/Data/ByteString/Unsafe_LHAssumptions.hs @@ -2,36 +2,37 @@ {-# OPTIONS_GHC -Wno-unused-imports #-} module Data.ByteString.Unsafe_LHAssumptions where +import Data.ByteString import Data.ByteString.Unsafe import Data.ByteString_LHAssumptions() import GHC.Types_LHAssumptions() {-@ assume Data.ByteString.Unsafe.unsafeHead - :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _ + :: { bs : ByteString | 1 <= bslen bs } -> _ assume Data.ByteString.Unsafe.unsafeTail - :: bs : { v : Data.ByteString.ByteString | bslen v > 0 } - -> { v : Data.ByteString.ByteString | bslen v = bslen bs - 1 } + :: bs : { v : ByteString | bslen v > 0 } + -> { v : ByteString | bslen v = bslen bs - 1 } assume Data.ByteString.Unsafe.unsafeInit - :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _ + :: { bs : ByteString | 1 <= bslen bs } -> _ assume Data.ByteString.Unsafe.unsafeLast - :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _ + :: { bs : ByteString | 1 <= bslen bs } -> _ assume Data.ByteString.Unsafe.unsafeIndex - :: bs : Data.ByteString.ByteString + :: bs : ByteString -> { n : Int | 0 <= n && n < bslen bs } -> _ assume Data.ByteString.Unsafe.unsafeTake :: n : { n : Int | 0 <= n } - -> i : { i : Data.ByteString.ByteString | n <= bslen i } - -> { o : Data.ByteString.ByteString | bslen o == n } + -> i : { i : ByteString | n <= bslen i } + -> { o : ByteString | bslen o == n } assume Data.ByteString.Unsafe.unsafeDrop :: n : { n : Int | 0 <= n } - -> i : { i : Data.ByteString.ByteString | n <= bslen i } - -> { o : Data.ByteString.ByteString | bslen o == bslen i - n } + -> i : { i : ByteString | n <= bslen i } + -> { o : ByteString | bslen o == bslen i - n } @-} diff --git a/src/Data/ByteString_LHAssumptions.hs b/src/Data/ByteString_LHAssumptions.hs index 1a6df0cf8f..b4cf68c186 100644 --- a/src/Data/ByteString_LHAssumptions.hs +++ b/src/Data/ByteString_LHAssumptions.hs @@ -7,374 +7,374 @@ import Data.String_LHAssumptions() import GHC.Word {-@ -measure bslen :: Data.ByteString.ByteString -> { n : Int | 0 <= n } +measure bslen :: ByteString -> { n : Int | 0 <= n } -invariant { bs : Data.ByteString.ByteString | 0 <= bslen bs } +invariant { bs : ByteString | 0 <= bslen bs } -invariant { bs : Data.ByteString.ByteString | bslen bs == stringlen bs } +invariant { bs : ByteString | bslen bs == stringlen bs } -assume Data.ByteString.Internal.Type.empty :: { bs : Data.ByteString.ByteString | bslen bs == 0 } +assume Data.ByteString.Internal.Type.empty :: { bs : ByteString | bslen bs == 0 } -assume Data.ByteString.singleton :: _ -> { bs : Data.ByteString.ByteString | bslen bs == 1 } +assume Data.ByteString.singleton :: _ -> { bs : ByteString | bslen bs == 1 } assume Data.ByteString.pack :: w8s : [_] - -> { bs : Data.ByteString.ByteString | bslen bs == len w8s } + -> { bs : ByteString | bslen bs == len w8s } -assume Data.ByteString.unpack :: bs : Data.ByteString.ByteString +assume Data.ByteString.unpack :: bs : ByteString -> { w8s : [_] | len w8s == bslen bs } assume Data.ByteString.cons :: _ - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen o == bslen i + 1 } + -> i : ByteString + -> { o : ByteString | bslen o == bslen i + 1 } -assume Data.ByteString.snoc :: i : Data.ByteString.ByteString +assume Data.ByteString.snoc :: i : ByteString -> _ - -> { o : Data.ByteString.ByteString | bslen o == bslen i + 1 } + -> { o : ByteString | bslen o == bslen i + 1 } -assume Data.ByteString.append :: l : Data.ByteString.ByteString - -> r : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen o == bslen l + bslen r } +assume Data.ByteString.append :: l : ByteString + -> r : ByteString + -> { o : ByteString | bslen o == bslen l + bslen r } -assume Data.ByteString.head :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _ +assume Data.ByteString.head :: { bs : ByteString | 1 <= bslen bs } -> _ -assume Data.ByteString.unsnoc :: i:Data.ByteString.ByteString - -> (Maybe ({ o : Data.ByteString.ByteString | bslen o == bslen i - 1 }, _)) +assume Data.ByteString.unsnoc :: i:ByteString + -> (Maybe ({ o : ByteString | bslen o == bslen i - 1 }, _)) -assume Data.ByteString.last :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _ +assume Data.ByteString.last :: { bs : ByteString | 1 <= bslen bs } -> _ -assume Data.ByteString.tail :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _ +assume Data.ByteString.tail :: { bs : ByteString | 1 <= bslen bs } -> _ assume Data.ByteString.init - :: {i:Data.ByteString.ByteString | 1 <= bslen i } - -> {o:Data.ByteString.ByteString | bslen o == bslen i - 1 } + :: {i:ByteString | 1 <= bslen i } + -> {o:ByteString | bslen o == bslen i - 1 } assume Data.ByteString.null - :: bs : Data.ByteString.ByteString - -> { b : GHC.Types.Bool | b <=> bslen bs == 0 } + :: bs : ByteString + -> { b : Bool | b <=> bslen bs == 0 } -assume Data.ByteString.length :: bs : Data.ByteString.ByteString -> { n : Int | bslen bs == n } +assume Data.ByteString.length :: bs : ByteString -> { n : Int | bslen bs == n } assume Data.ByteString.map :: (_ -> _) - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen o == bslen i } + -> i : ByteString + -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.reverse - :: i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen o == bslen i } + :: i : ByteString + -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.intersperse :: _ - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | (bslen i == 0 <=> bslen o == 0) && (1 <= bslen i <=> bslen o == 2 * bslen i - 1) } + -> i : ByteString + -> { o : ByteString | (bslen i == 0 <=> bslen o == 0) && (1 <= bslen i <=> bslen o == 2 * bslen i - 1) } assume Data.ByteString.intercalate - :: l : Data.ByteString.ByteString - -> rs : [Data.ByteString.ByteString] - -> { o : Data.ByteString.ByteString | len rs == 0 ==> bslen o == 0 } + :: l : ByteString + -> rs : [ByteString] + -> { o : ByteString | len rs == 0 ==> bslen o == 0 } assume Data.ByteString.transpose - :: is : [Data.ByteString.ByteString] - -> { os : [{ bs : Data.ByteString.ByteString | bslen bs <= len is }] | len is == 0 ==> len os == 0} + :: is : [ByteString] + -> { os : [{ bs : ByteString | bslen bs <= len is }] | len is == 0 ==> len os == 0} assume Data.ByteString.foldl1 :: (_ -> _ -> _) - -> { bs : Data.ByteString.ByteString | 1 <= bslen bs } + -> { bs : ByteString | 1 <= bslen bs } -> _ assume Data.ByteString.foldl1' :: (_ -> _ -> _) - -> { bs : Data.ByteString.ByteString | 1 <= bslen bs } + -> { bs : ByteString | 1 <= bslen bs } -> _ assume Data.ByteString.foldr1 :: (_ -> _ -> _) - -> { bs : Data.ByteString.ByteString | 1 <= bslen bs } + -> { bs : ByteString | 1 <= bslen bs } -> _ assume Data.ByteString.foldr1' :: (_ -> _ -> _) - -> { bs : Data.ByteString.ByteString | 1 <= bslen bs } + -> { bs : ByteString | 1 <= bslen bs } -> _ assume Data.ByteString.concat - :: is : [Data.ByteString.ByteString] - -> { o : Data.ByteString.ByteString | (len is == 0) ==> (bslen o == 0) } + :: is : [ByteString] + -> { o : ByteString | (len is == 0) ==> (bslen o == 0) } assume Data.ByteString.concatMap - :: (_ -> Data.ByteString.ByteString) - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen i == 0 ==> bslen o == 0 } + :: (_ -> ByteString) + -> i : ByteString + -> { o : ByteString | bslen i == 0 ==> bslen o == 0 } assume Data.ByteString.any - :: (_ -> GHC.Types.Bool) - -> bs : Data.ByteString.ByteString - -> { b : GHC.Types.Bool | bslen bs == 0 ==> not b } + :: (_ -> Bool) + -> bs : ByteString + -> { b : Bool | bslen bs == 0 ==> not b } assume Data.ByteString.all - :: (_ -> GHC.Types.Bool) - -> bs : Data.ByteString.ByteString - -> { b : GHC.Types.Bool | bslen bs == 0 ==> b } + :: (_ -> Bool) + -> bs : ByteString + -> { b : Bool | bslen bs == 0 ==> b } -assume Data.ByteString.maximum :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _ +assume Data.ByteString.maximum :: { bs : ByteString | 1 <= bslen bs } -> _ -assume Data.ByteString.minimum :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _ +assume Data.ByteString.minimum :: { bs : ByteString | 1 <= bslen bs } -> _ assume Data.ByteString.scanl :: (_ -> _ -> _) -> _ - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen o == bslen i } + -> i : ByteString + -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.scanl1 :: (_ -> _ -> _) - -> i : { i : Data.ByteString.ByteString | 1 <= bslen i } - -> { o : Data.ByteString.ByteString | bslen o == bslen i } + -> i : { i : ByteString | 1 <= bslen i } + -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.scanr :: (_ -> _ -> _) -> _ - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen o == bslen i } + -> i : ByteString + -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.scanr1 :: (_ -> _ -> _) - -> i : { i : Data.ByteString.ByteString | 1 <= bslen i } - -> { o : Data.ByteString.ByteString | bslen o == bslen i } + -> i : { i : ByteString | 1 <= bslen i } + -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.mapAccumL :: (acc -> _ -> (acc, _)) -> acc - -> i : Data.ByteString.ByteString - -> (acc, { o : Data.ByteString.ByteString | bslen o == bslen i }) + -> i : ByteString + -> (acc, { o : ByteString | bslen o == bslen i }) assume Data.ByteString.mapAccumR :: (acc -> _ -> (acc, _)) -> acc - -> i : Data.ByteString.ByteString - -> (acc, { o : Data.ByteString.ByteString | bslen o == bslen i }) + -> i : ByteString + -> (acc, { o : ByteString | bslen o == bslen i }) assume Data.ByteString.replicate :: n : Int -> _ - -> { bs : Data.ByteString.ByteString | bslen bs == n } + -> { bs : ByteString | bslen bs == n } assume Data.ByteString.unfoldrN :: n : Int -> (a -> Maybe (_, a)) -> a - -> ({ bs : Data.ByteString.ByteString | bslen bs <= n }, Maybe a) + -> ({ bs : ByteString | bslen bs <= n }, Maybe a) assume Data.ByteString.take :: n : Int - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | (n <= 0 <=> bslen o == 0) && + -> i : ByteString + -> { o : ByteString | (n <= 0 <=> bslen o == 0) && ((0 <= n && n <= bslen i) <=> bslen o == n) && (bslen i <= n <=> bslen o = bslen i) } assume Data.ByteString.drop :: n : Int - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | (n <= 0 <=> bslen o == bslen i) && + -> i : ByteString + -> { o : ByteString | (n <= 0 <=> bslen o == bslen i) && ((0 <= n && n <= bslen i) <=> bslen o == bslen i - n) && (bslen i <= n <=> bslen o == 0) } assume Data.ByteString.splitAt :: n : Int - -> i : Data.ByteString.ByteString - -> ( { l : Data.ByteString.ByteString | (n <= 0 <=> bslen l == 0) && + -> i : ByteString + -> ( { l : 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) && + , { r : ByteString | (n <= 0 <=> bslen r == bslen i) && ((0 <= n && n <= bslen i) <=> bslen r == bslen i - n) && (bslen i <= n <=> bslen r == 0) } ) assume Data.ByteString.takeWhile - :: (_ -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen o <= bslen i } + :: (_ -> Bool) + -> i : ByteString + -> { o : ByteString | bslen o <= bslen i } assume Data.ByteString.dropWhile - :: (_ -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen o <= bslen i } + :: (_ -> Bool) + -> i : ByteString + -> { o : ByteString | bslen o <= bslen i } assume Data.ByteString.span - :: (_ -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i } - , { r : Data.ByteString.ByteString | bslen r <= bslen i } + :: (_ -> Bool) + -> i : ByteString + -> ( { l : ByteString | bslen l <= bslen i } + , { r : ByteString | bslen r <= bslen i } ) assume Data.ByteString.spanEnd - :: (_ -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i } - , { r : Data.ByteString.ByteString | bslen r <= bslen i } + :: (_ -> Bool) + -> i : ByteString + -> ( { l : ByteString | bslen l <= bslen i } + , { r : ByteString | bslen r <= bslen i } ) assume Data.ByteString.break - :: (_ -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i } - , { r : Data.ByteString.ByteString | bslen r <= bslen i } + :: (_ -> Bool) + -> i : ByteString + -> ( { l : ByteString | bslen l <= bslen i } + , { r : ByteString | bslen r <= bslen i } ) assume Data.ByteString.breakEnd - :: (_ -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i } - , { r : Data.ByteString.ByteString | bslen r <= bslen i } + :: (_ -> Bool) + -> i : ByteString + -> ( { l : ByteString | bslen l <= bslen i } + , { r : ByteString | bslen r <= bslen i } ) assume Data.ByteString.group - :: i : Data.ByteString.ByteString - -> [{ o : Data.ByteString.ByteString | 1 <= bslen o && bslen o <= bslen i }] + :: i : ByteString + -> [{ o : ByteString | 1 <= bslen o && bslen o <= bslen i }] assume Data.ByteString.groupBy - :: (_ -> _ -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> [{ o : Data.ByteString.ByteString | 1 <= bslen o && bslen o <= bslen i }] + :: (_ -> _ -> Bool) + -> i : ByteString + -> [{ o : ByteString | 1 <= bslen o && bslen o <= bslen i }] assume Data.ByteString.inits - :: i : Data.ByteString.ByteString - -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }] + :: i : ByteString + -> [{ o : ByteString | bslen o <= bslen i }] assume Data.ByteString.tails - :: i : Data.ByteString.ByteString - -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }] + :: i : ByteString + -> [{ o : ByteString | bslen o <= bslen i }] assume Data.ByteString.split :: _ - -> i : Data.ByteString.ByteString - -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }] + -> i : ByteString + -> [{ o : ByteString | bslen o <= bslen i }] assume Data.ByteString.splitWith - :: (_ -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }] + :: (_ -> Bool) + -> i : ByteString + -> [{ o : ByteString | bslen o <= bslen i }] assume Data.ByteString.isPrefixOf - :: l : Data.ByteString.ByteString - -> r : Data.ByteString.ByteString - -> { b : GHC.Types.Bool | bslen l >= bslen r ==> not b } + :: l : ByteString + -> r : ByteString + -> { b : Bool | bslen l >= bslen r ==> not b } assume Data.ByteString.isSuffixOf - :: l : Data.ByteString.ByteString - -> r : Data.ByteString.ByteString - -> { b : GHC.Types.Bool | bslen l > bslen r ==> not b } + :: l : ByteString + -> r : ByteString + -> { b : Bool | bslen l > bslen r ==> not b } assume Data.ByteString.isInfixOf - :: l : Data.ByteString.ByteString - -> r : Data.ByteString.ByteString - -> { b : GHC.Types.Bool | bslen l > bslen r ==> not b } + :: l : ByteString + -> r : ByteString + -> { b : Bool | bslen l > bslen r ==> not b } assume Data.ByteString.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) } + :: il : ByteString + -> ir : ByteString + -> ( { ol : ByteString | bslen ol <= bslen ir && (bslen il > bslen ir ==> bslen ol == bslen ir)} + , { or : ByteString | bslen or <= bslen ir && (bslen il > bslen ir ==> bslen or == 0) } ) assume Data.ByteString.elem :: _ - -> bs : Data.ByteString.ByteString - -> { b : GHC.Types.Bool | bslen bs == 0 ==> not b } + -> bs : ByteString + -> { b : Bool | bslen bs == 0 ==> not b } assume Data.ByteString.notElem :: _ - -> bs : Data.ByteString.ByteString - -> { b : GHC.Types.Bool | bslen bs == 0 ==> b } + -> bs : ByteString + -> { b : Bool | bslen bs == 0 ==> b } assume Data.ByteString.find - :: (_ -> GHC.Types.Bool) - -> bs : Data.ByteString.ByteString + :: (_ -> Bool) + -> bs : ByteString -> (Maybe { w8 : _ | bslen bs /= 0 }) assume Data.ByteString.filter - :: (_ -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen o <= bslen i } + :: (_ -> Bool) + -> i : ByteString + -> { o : ByteString | bslen o <= bslen i } assume Data.ByteString.partition - :: (Word8 -> GHC.Types.Bool) - -> i : Data.ByteString.ByteString - -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i } - , { r : Data.ByteString.ByteString | bslen r <= bslen i } + :: (Word8 -> Bool) + -> i : ByteString + -> ( { l : ByteString | bslen l <= bslen i } + , { r : ByteString | bslen r <= bslen i } ) -assume Data.ByteString.index :: bs : Data.ByteString.ByteString -> { n : Int | 0 <= n && n < bslen bs } -> _ +assume Data.ByteString.index :: bs : ByteString -> { n : Int | 0 <= n && n < bslen bs } -> _ assume Data.ByteString.elemIndex :: _ - -> bs : Data.ByteString.ByteString + -> bs : ByteString -> (Maybe { n : Int | 0 <= n && n < bslen bs }) assume Data.ByteString.elemIndices :: _ - -> bs : Data.ByteString.ByteString + -> bs : ByteString -> [{ n : Int | 0 <= n && n < bslen bs }] assume Data.ByteString.elemIndexEnd :: _ - -> bs : Data.ByteString.ByteString + -> bs : ByteString -> (Maybe { n : Int | 0 <= n && n < bslen bs }) assume Data.ByteString.findIndex - :: (_ -> GHC.Types.Bool) - -> bs : Data.ByteString.ByteString + :: (_ -> Bool) + -> bs : ByteString -> (Maybe { n : Int | 0 <= n && n < bslen bs }) assume Data.ByteString.findIndices - :: (_ -> GHC.Types.Bool) - -> bs : Data.ByteString.ByteString + :: (_ -> Bool) + -> bs : ByteString -> [{ n : Int | 0 <= n && n < bslen bs }] assume Data.ByteString.count :: _ - -> bs : Data.ByteString.ByteString + -> bs : ByteString -> { n : Int | 0 <= n && n < bslen bs } assume Data.ByteString.zip - :: l : Data.ByteString.ByteString - -> r : Data.ByteString.ByteString + :: l : ByteString + -> r : ByteString -> { o : [(_, _)] | len o <= bslen l && len o <= bslen r } assume Data.ByteString.zipWith :: (_ -> _ -> a) - -> l : Data.ByteString.ByteString - -> r : Data.ByteString.ByteString + -> l : ByteString + -> r : ByteString -> { o : [a] | len o <= bslen l && len o <= bslen r } assume Data.ByteString.unzip :: i : [(_, _)] - -> ( { l : Data.ByteString.ByteString | bslen l == len i } - , { r : Data.ByteString.ByteString | bslen r == len i } + -> ( { l : ByteString | bslen l == len i } + , { r : ByteString | bslen r == len i } ) assume Data.ByteString.sort - :: i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen o == bslen i } + :: i : ByteString + -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.copy - :: i : Data.ByteString.ByteString - -> { o : Data.ByteString.ByteString | bslen o == bslen i } + :: i : ByteString + -> { o : ByteString | bslen o == bslen i } assume Data.ByteString.hGet :: _ -> n : { n : Int | 0 <= n } - -> (IO { bs : Data.ByteString.ByteString | bslen bs == n || bslen bs == 0 }) + -> (IO { bs : ByteString | bslen bs == n || bslen bs == 0 }) assume Data.ByteString.hGetSome :: _ -> n : { n : Int | 0 <= n } - -> (IO { bs : Data.ByteString.ByteString | bslen bs <= n }) + -> (IO { bs : ByteString | bslen bs <= n }) assume Data.ByteString.hGetNonBlocking :: _ -> n : { n : Int | 0 <= n } - -> (IO { bs : Data.ByteString.ByteString | bslen bs <= n }) + -> (IO { bs : ByteString | bslen bs <= n }) assume Data.ByteString.uncons - :: i : Data.ByteString.ByteString - -> (Maybe (_, { o : Data.ByteString.ByteString | bslen o == bslen i - 1 })) + :: i : ByteString + -> (Maybe (_, { o : ByteString | bslen o == bslen i - 1 })) @-} diff --git a/src/Data/Either_LHAssumptions.hs b/src/Data/Either_LHAssumptions.hs index e9c867c98b..0c6c0757e4 100644 --- a/src/Data/Either_LHAssumptions.hs +++ b/src/Data/Either_LHAssumptions.hs @@ -1,10 +1,11 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} module Data.Either_LHAssumptions where import GHC.Types_LHAssumptions() {-@ -measure isLeft :: GHC.Internal.Data.Either.Either a b -> Bool +measure isLeft :: Either a b -> Bool isLeft (Left x) = true isLeft (Right x) = false @-} diff --git a/src/Data/Set_LHAssumptions.hs b/src/Data/Set_LHAssumptions.hs index 5ae7a499af..eb7e0103dc 100644 --- a/src/Data/Set_LHAssumptions.hs +++ b/src/Data/Set_LHAssumptions.hs @@ -7,7 +7,7 @@ import GHC.Types_LHAssumptions() {-@ -embed Data.Set.Internal.Set as Set_Set +embed Set as Set_Set // ---------------------------------------------------------------------------------------------- // -- | Logical Set Operators: Interpreted "natively" by the SMT solver ------------------------- @@ -15,54 +15,54 @@ embed Data.Set.Internal.Set as Set_Set // union -measure Set_cup :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) +measure Set_cup :: (Set a) -> (Set a) -> (Set a) // intersection -measure Set_cap :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) +measure Set_cap :: (Set a) -> (Set a) -> (Set a) // difference -measure Set_dif :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) +measure Set_dif :: (Set a) -> (Set a) -> (Set a) // singleton -measure Set_sng :: a -> (Data.Set.Internal.Set a) +measure Set_sng :: a -> (Set a) // emptiness test -measure Set_emp :: (Data.Set.Internal.Set a) -> GHC.Types.Bool +measure Set_emp :: (Set a) -> Bool // empty set -measure Set_empty :: forall a. GHC.Types.Int -> (Data.Set.Internal.Set a) +measure Set_empty :: forall a. Int -> (Set a) // membership test -measure Set_mem :: a -> (Data.Set.Internal.Set a) -> GHC.Types.Bool +measure Set_mem :: a -> (Set a) -> Bool // inclusion test -measure Set_sub :: (Data.Set.Internal.Set a) -> (Data.Set.Internal.Set a) -> GHC.Types.Bool +measure Set_sub :: (Set a) -> (Set a) -> Bool // --------------------------------------------------------------------------------------------- // -- | Refined Types for Data.Set Operations -------------------------------------------------- // --------------------------------------------------------------------------------------------- -assume Data.Set.Internal.isSubsetOf :: (GHC.Classes.Ord a) => x:(Data.Set.Internal.Set a) -> y:(Data.Set.Internal.Set a) -> {v:GHC.Types.Bool | v <=> Set_sub x y} -assume Data.Set.Internal.member :: (GHC.Classes.Ord a) => x:a -> xs:(Data.Set.Internal.Set a) -> {v:GHC.Types.Bool | v <=> Set_mem x xs} -assume Data.Set.Internal.null :: (GHC.Classes.Ord a) => xs:(Data.Set.Internal.Set a) -> {v:GHC.Types.Bool | v <=> Set_emp xs} +assume isSubsetOf :: (Ord a) => x:(Set a) -> y:(Set a) -> {v:Bool | v <=> Set_sub x y} +assume Data.Set.Internal.member :: Ord a => x:a -> xs:(Set a) -> {v:Bool | v <=> Set_mem x xs} +assume Data.Set.Internal.null :: Ord a => xs:(Set a) -> {v:Bool | v <=> Set_emp xs} -assume Data.Set.Internal.empty :: {v:(Data.Set.Internal.Set a) | Set_emp v} -assume Data.Set.Internal.singleton :: x:a -> {v:(Data.Set.Internal.Set a) | v = (Set_sng x)} -assume Data.Set.Internal.insert :: (GHC.Classes.Ord a) => x:a -> xs:(Data.Set.Internal.Set a) -> {v:(Data.Set.Internal.Set a) | v = Set_cup xs (Set_sng x)} -assume Data.Set.Internal.delete :: (GHC.Classes.Ord a) => x:a -> xs:(Data.Set.Internal.Set a) -> {v:(Data.Set.Internal.Set a) | v = Set_dif xs (Set_sng x)} +assume Data.Set.Internal.empty :: {v:(Set a) | Set_emp v} +assume Data.Set.Internal.singleton :: x:a -> {v:(Set a) | v = (Set_sng x)} +assume Data.Set.Internal.insert :: Ord a => x:a -> xs:(Set a) -> {v:(Set a) | v = Set_cup xs (Set_sng x)} +assume Data.Set.Internal.delete :: (Ord a) => x:a -> xs:(Set a) -> {v:(Set a) | v = Set_dif xs (Set_sng x)} -assume Data.Set.Internal.union :: GHC.Classes.Ord a => xs:(Data.Set.Internal.Set a) -> ys:(Data.Set.Internal.Set a) -> {v:(Data.Set.Internal.Set a) | v = Set_cup xs ys} -assume Data.Set.Internal.intersection :: GHC.Classes.Ord a => xs:(Data.Set.Internal.Set a) -> ys:(Data.Set.Internal.Set a) -> {v:(Data.Set.Internal.Set a) | v = Set_cap xs ys} -assume Data.Set.Internal.difference :: GHC.Classes.Ord a => xs:(Data.Set.Internal.Set a) -> ys:(Data.Set.Internal.Set a) -> {v:(Data.Set.Internal.Set a) | v = Set_dif xs ys} +assume Data.Set.Internal.union :: Ord a => xs:(Set a) -> ys:(Set a) -> {v:(Set a) | v = Set_cup xs ys} +assume Data.Set.Internal.intersection :: Ord a => xs:(Set a) -> ys:(Set a) -> {v:(Set a) | v = Set_cap xs ys} +assume Data.Set.Internal.difference :: Ord a => xs:(Set a) -> ys:(Set a) -> {v:(Set a) | v = Set_dif xs ys} -assume Data.Set.Internal.fromList :: GHC.Classes.Ord a => xs:[a] -> {v:Data.Set.Internal.Set a | v = listElts xs} -assume Data.Set.Internal.toList :: GHC.Classes.Ord a => s:Data.Set.Internal.Set a -> {xs:[a] | s = listElts xs} +assume Data.Set.Internal.fromList :: Ord a => xs:[a] -> {v:Set a | v = listElts xs} +assume Data.Set.Internal.toList :: Ord a => s:Set a -> {xs:[a] | s = listElts xs} // --------------------------------------------------------------------------------------------- // -- | The set of elements in a list ---------------------------------------------------------- // --------------------------------------------------------------------------------------------- -measure listElts :: [a] -> (Data.Set.Internal.Set a) +measure listElts :: [a] -> Set a listElts [] = {v | (Set_emp v)} listElts (x:xs) = {v | v = Set_cup (Set_sng x) (listElts xs) } diff --git a/src/Data/String_LHAssumptions.hs b/src/Data/String_LHAssumptions.hs index bc1f4cc05b..265e78b405 100644 --- a/src/Data/String_LHAssumptions.hs +++ b/src/Data/String_LHAssumptions.hs @@ -6,10 +6,10 @@ import Data.String import GHC.Types_LHAssumptions() {-@ -measure stringlen :: a -> GHC.Types.Int +measure stringlen :: a -> Int assume GHC.Internal.Data.String.fromString - :: forall a. GHC.Internal.Data.String.IsString a - => i : [GHC.Types.Char] + :: forall a. IsString a + => i : [Char] -> { o : a | i ~~ o && len i == stringlen o } @-} diff --git a/src/Foreign/C/String_LHAssumptions.hs b/src/Foreign/C/String_LHAssumptions.hs index 7f08478282..66c40fb8cc 100644 --- a/src/Foreign/C/String_LHAssumptions.hs +++ b/src/Foreign/C/String_LHAssumptions.hs @@ -8,12 +8,12 @@ import GHC.Ptr import GHC.Types_LHAssumptions() {-@ -type CStringLen = ((GHC.Internal.Ptr.Ptr GHC.Internal.Foreign.C.Types.CChar), Nat)<{\p v -> (v <= (plen p))}> -type CStringLenN N = ((GHC.Internal.Ptr.Ptr GHC.Internal.Foreign.C.Types.CChar), {v:Nat | v = N})<{\p v -> (v <= (plen p))}> +type CStringLen = ((Ptr CChar), Nat)<{\p v -> (v <= (plen p))}> +type CStringLenN N = ((Ptr CChar), {v:Nat | v = N})<{\p v -> (v <= (plen p))}> -// measure cStringLen :: GHC.Internal.Foreign.C.String.CStringLen -> GHC.Types.Int -measure cStringLen :: ((GHC.Internal.Ptr.Ptr GHC.Internal.Foreign.C.Types.CChar), GHC.Types.Int) -> GHC.Types.Int +// measure cStringLen :: CStringLen -> Int +measure cStringLen :: ((Ptr CChar), Int) -> Int -// measure cStringLen :: ((GHC.Internal.Ptr.Ptr GHC.Internal.Foreign.C.Types.CChar), GHC.Types.Int) -> GHC.Types.Int +// measure cStringLen :: ((Ptr CChar), Int) -> Int // cStringLen (c, n) = n @-} diff --git a/src/Foreign/C/Types_LHAssumptions.hs b/src/Foreign/C/Types_LHAssumptions.hs index 345952035f..254d8415ce 100644 --- a/src/Foreign/C/Types_LHAssumptions.hs +++ b/src/Foreign/C/Types_LHAssumptions.hs @@ -1,12 +1,14 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} module Foreign.C.Types_LHAssumptions where +import Foreign.C.Types import GHC.Int_LHAssumptions() {-@ -embed Foreign.C.Types.CInt as int -embed Foreign.C.Types.CSize as int -embed Foreign.C.Types.CULong as int +embed CInt as int +embed CSize as int +embed CULong as int @-} diff --git a/src/Foreign/Concurrent_LHAssumptions.hs b/src/Foreign/Concurrent_LHAssumptions.hs index 055e5dba7c..7614bea88a 100644 --- a/src/Foreign/Concurrent_LHAssumptions.hs +++ b/src/Foreign/Concurrent_LHAssumptions.hs @@ -6,5 +6,5 @@ import Foreign.Concurrent import GHC.ForeignPtr_LHAssumptions() {-@ -assume GHC.Internal.Foreign.Concurrent.newForeignPtr :: p:(PtrV a) -> GHC.Types.IO () -> (GHC.Types.IO (ForeignPtrN a (plen p))) +assume GHC.Internal.Foreign.Concurrent.newForeignPtr :: p:(PtrV a) -> IO () -> (IO (ForeignPtrN a (plen p))) @-} diff --git a/src/Foreign/ForeignPtr_LHAssumptions.hs b/src/Foreign/ForeignPtr_LHAssumptions.hs index cb14e0d53c..c61dbc9ebc 100644 --- a/src/Foreign/ForeignPtr_LHAssumptions.hs +++ b/src/Foreign/ForeignPtr_LHAssumptions.hs @@ -3,16 +3,18 @@ module Foreign.ForeignPtr_LHAssumptions where import Foreign.Concurrent_LHAssumptions() -import Foreign.ForeignPtr +import Foreign.Storable +import GHC.ForeignPtr +import GHC.Internal.Foreign.ForeignPtr.Imp import GHC.ForeignPtr_LHAssumptions() {-@ -assume GHC.Internal.ForeignPtr.withForeignPtr :: forall a b. fp:(GHC.Internal.ForeignPtr.ForeignPtr a) - -> ((PtrN a (fplen fp)) -> GHC.Types.IO b) - -> (GHC.Types.IO b) +assume GHC.Internal.ForeignPtr.withForeignPtr :: forall a b. fp:(ForeignPtr a) + -> ((PtrN a (fplen fp)) -> IO b) + -> IO b -assume GHC.Internal.Foreign.ForeignPtr.Imp.newForeignPtr :: _ -> p:(PtrV a) -> (GHC.Types.IO (ForeignPtrN a (plen p))) +assume GHC.Internal.Foreign.ForeignPtr.Imp.newForeignPtr :: _ -> p:(PtrV a) -> (IO (ForeignPtrN a (plen p))) // this uses `sizeOf (undefined :: a)`, so the ForeignPtr does not necessarily have length `n` diff --git a/src/Foreign/Ptr_LHAssumptions.hs b/src/Foreign/Ptr_LHAssumptions.hs index 12a6430978..b728856836 100644 --- a/src/Foreign/Ptr_LHAssumptions.hs +++ b/src/Foreign/Ptr_LHAssumptions.hs @@ -1,10 +1,13 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} module Foreign.Ptr_LHAssumptions where +import Foreign.Ptr +import GHC.Ptr_LHAssumptions () {-@ -invariant {v:Foreign.Ptr.Ptr a | 0 <= plen v } -invariant {v:Foreign.Ptr.Ptr a | 0 <= pbase v } +invariant {v:Ptr a | 0 <= plen v } +invariant {v:Ptr a | 0 <= pbase v } @-} diff --git a/src/Foreign/Storable_LHAssumptions.hs b/src/Foreign/Storable_LHAssumptions.hs index 20174db9e6..6dc694660e 100644 --- a/src/Foreign/Storable_LHAssumptions.hs +++ b/src/Foreign/Storable_LHAssumptions.hs @@ -4,27 +4,28 @@ module Foreign.Storable_LHAssumptions where import GHC.Ptr_LHAssumptions() import Foreign.Storable +import GHC.Ptr {-@ predicate PValid P N = ((0 <= N) && (N < (plen P))) -assume GHC.Internal.Foreign.Storable.poke :: (GHC.Internal.Foreign.Storable.Storable a) - => {v: (GHC.Internal.Ptr.Ptr a) | 0 < (plen v)} +assume GHC.Internal.Foreign.Storable.poke :: (Storable a) + => {v: (Ptr a) | 0 < (plen v)} -> a - -> (GHC.Types.IO ()) + -> (IO ()) -assume GHC.Internal.Foreign.Storable.peek :: (GHC.Internal.Foreign.Storable.Storable a) - => p:{v: (GHC.Internal.Ptr.Ptr a) | 0 < (plen v)} - -> (GHC.Types.IO {v:a | v = (deref p)}) +assume GHC.Internal.Foreign.Storable.peek :: (Storable a) + => p:{v: (Ptr a) | 0 < (plen v)} + -> (IO {v:a | v = (deref p)}) -assume GHC.Internal.Foreign.Storable.peekByteOff :: (GHC.Internal.Foreign.Storable.Storable a) - => forall b. p:(GHC.Internal.Ptr.Ptr b) - -> {v:GHC.Types.Int | (PValid p v)} - -> (GHC.Types.IO a) +assume GHC.Internal.Foreign.Storable.peekByteOff :: (Storable a) + => forall b. p:(Ptr b) + -> {v:Int | (PValid p v)} + -> (IO a) -assume GHC.Internal.Foreign.Storable.pokeByteOff :: (GHC.Internal.Foreign.Storable.Storable a) - => forall b. p:(GHC.Internal.Ptr.Ptr b) - -> {v:GHC.Types.Int | (PValid p v)} +assume GHC.Internal.Foreign.Storable.pokeByteOff :: (Storable a) + => forall b. p:(Ptr b) + -> {v:Int | (PValid p v)} -> a - -> GHC.Types.IO () + -> IO () @-} diff --git a/src/GHC/CString_LHAssumptions.hs b/src/GHC/CString_LHAssumptions.hs index e295358f10..76d1c4c2eb 100644 --- a/src/GHC/CString_LHAssumptions.hs +++ b/src/GHC/CString_LHAssumptions.hs @@ -1,17 +1,19 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} {-# LANGUAGE MagicHash #-} {-# OPTIONS_GHC -Wno-missing-signatures #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.CString_LHAssumptions() where import GHC.CString +import GHC.Prim import GHC.Types_LHAssumptions() _f = unpackCString# {-@ -measure strLen :: Addr# -> GHC.Types.Int +measure strLen :: Addr# -> Int assume GHC.CString.unpackCString# - :: x:GHC.Prim.Addr# - -> {v:[GHC.Types.Char] | v ~~ x && len v == strLen x} + :: x:Addr# + -> {v:[Char] | v ~~ x && len v == strLen x} @-} diff --git a/src/GHC/Classes_LHAssumptions.hs b/src/GHC/Classes_LHAssumptions.hs index 662f77aa9a..e721ae7b0a 100644 --- a/src/GHC/Classes_LHAssumptions.hs +++ b/src/GHC/Classes_LHAssumptions.hs @@ -1,36 +1,36 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Classes_LHAssumptions where -import GHC.Classes() -import GHC.Types() +import GHC.Classes import GHC.Types_LHAssumptions() {-@ -assume GHC.Classes.not :: x:GHC.Types.Bool -> {v:GHC.Types.Bool | ((v) <=> ~(x))} -assume (GHC.Classes.&&) :: x:GHC.Types.Bool -> y:GHC.Types.Bool - -> {v:GHC.Types.Bool | ((v) <=> ((x) && (y)))} -assume (GHC.Classes.||) :: x:GHC.Types.Bool -> y:GHC.Types.Bool - -> {v:GHC.Types.Bool | ((v) <=> ((x) || (y)))} -assume (GHC.Classes.==) :: (GHC.Classes.Eq a) => x:a -> y:a - -> {v:GHC.Types.Bool | ((v) <=> x = y)} -assume (GHC.Classes./=) :: (GHC.Classes.Eq a) => x:a -> y:a - -> {v:GHC.Types.Bool | ((v) <=> x != y)} -assume (GHC.Classes.>) :: (GHC.Classes.Ord a) => x:a -> y:a - -> {v:GHC.Types.Bool | ((v) <=> x > y)} -assume (GHC.Classes.>=) :: (GHC.Classes.Ord a) => x:a -> y:a - -> {v:GHC.Types.Bool | ((v) <=> x >= y)} -assume (GHC.Classes.<) :: (GHC.Classes.Ord a) => x:a -> y:a - -> {v:GHC.Types.Bool | ((v) <=> x < y)} -assume (GHC.Classes.<=) :: (GHC.Classes.Ord a) => x:a -> y:a - -> {v:GHC.Types.Bool | ((v) <=> x <= y)} +assume GHC.Classes.not :: x:Bool -> {v:Bool | ((v) <=> ~(x))} +assume (GHC.Classes.&&) :: x:Bool -> y:Bool + -> {v:Bool | ((v) <=> ((x) && (y)))} +assume (GHC.Classes.||) :: x:Bool -> y:Bool + -> {v:Bool | ((v) <=> ((x) || (y)))} +assume (GHC.Classes.==) :: (Eq a) => x:a -> y:a + -> {v:Bool | ((v) <=> x = y)} +assume (GHC.Classes./=) :: (Eq a) => x:a -> y:a + -> {v:Bool | ((v) <=> x != y)} +assume (GHC.Classes.>) :: (Ord a) => x:a -> y:a + -> {v:Bool | ((v) <=> x > y)} +assume (GHC.Classes.>=) :: (Ord a) => x:a -> y:a + -> {v:Bool | ((v) <=> x >= y)} +assume (GHC.Classes.<) :: (Ord a) => x:a -> y:a + -> {v:Bool | ((v) <=> x < y)} +assume (GHC.Classes.<=) :: (Ord a) => x:a -> y:a + -> {v:Bool | ((v) <=> x <= y)} -assume GHC.Classes.compare :: (GHC.Classes.Ord a) => x:a -> y:a - -> {v:GHC.Types.Ordering | (((v = GHC.Types.EQ) <=> (x = y)) && - ((v = GHC.Types.LT) <=> (x < y)) && - ((v = GHC.Types.GT) <=> (x > y))) } +assume GHC.Classes.compare :: (Ord a) => x:a -> y:a + -> {v:Ordering | (((v = EQ) <=> (x = y)) && + ((v = LT) <=> (x < y)) && + ((v = GT) <=> (x > y))) } -assume GHC.Classes.max :: (GHC.Classes.Ord a) => x:a -> y:a -> {v:a | v = (if x > y then x else y) } -assume GHC.Classes.min :: (GHC.Classes.Ord a) => x:a -> y:a -> {v:a | v = (if x < y then x else y) } +assume GHC.Classes.max :: (Ord a) => x:a -> y:a -> {v:a | v = (if x > y then x else y) } +assume GHC.Classes.min :: (Ord a) => x:a -> y:a -> {v:a | v = (if x < y then x else y) } @-} diff --git a/src/GHC/Exts_LHAssumptions.hs b/src/GHC/Exts_LHAssumptions.hs index 242ca963a6..bee8dab95e 100644 --- a/src/GHC/Exts_LHAssumptions.hs +++ b/src/GHC/Exts_LHAssumptions.hs @@ -3,16 +3,17 @@ module GHC.Exts_LHAssumptions where import GHC.Base +import GHC.Prim import GHC.Types_LHAssumptions() {-@ -assume GHC.Prim.+# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v: GHC.Prim.Int# | v = x + y} -assume GHC.Prim.-# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v: GHC.Prim.Int# | v = x - y} -assume GHC.Prim.==# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x = y} -assume GHC.Prim.>=# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x >= y} -assume GHC.Prim.<=# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x <= y} -assume GHC.Prim.<# :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x < y} -assume GHC.Prim.># :: x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v:GHC.Prim.Int# | v = 1 <=> x > y} +assume GHC.Prim.+# :: x:Int# -> y:Int# -> {v: Int# | v = x + y} +assume GHC.Prim.-# :: x:Int# -> y:Int# -> {v: Int# | v = x - y} +assume GHC.Prim.==# :: x:Int# -> y:Int# -> {v:Int# | v = 1 <=> x = y} +assume GHC.Prim.>=# :: x:Int# -> y:Int# -> {v:Int# | v = 1 <=> x >= y} +assume GHC.Prim.<=# :: x:Int# -> y:Int# -> {v:Int# | v = 1 <=> x <= y} +assume GHC.Prim.<# :: x:Int# -> y:Int# -> {v:Int# | v = 1 <=> x < y} +assume GHC.Prim.># :: x:Int# -> y:Int# -> {v:Int# | v = 1 <=> x > y} @-} diff --git a/src/GHC/ForeignPtr_LHAssumptions.hs b/src/GHC/ForeignPtr_LHAssumptions.hs index 7b8d57882b..477a1fbf6f 100644 --- a/src/GHC/ForeignPtr_LHAssumptions.hs +++ b/src/GHC/ForeignPtr_LHAssumptions.hs @@ -3,14 +3,15 @@ module GHC.ForeignPtr_LHAssumptions where import GHC.ForeignPtr +import GHC.Ptr import GHC.Ptr_LHAssumptions() {-@ -measure fplen :: GHC.Internal.ForeignPtr.ForeignPtr a -> GHC.Types.Int +measure fplen :: ForeignPtr a -> Int -type ForeignPtrV a = {v: GHC.Internal.ForeignPtr.ForeignPtr a | 0 <= fplen v} -type ForeignPtrN a N = {v: GHC.Internal.ForeignPtr.ForeignPtr a | 0 <= fplen v && fplen v == N } +type ForeignPtrV a = {v: ForeignPtr a | 0 <= fplen v} +type ForeignPtrN a N = {v: ForeignPtr a | 0 <= fplen v && fplen v == N } -assume GHC.Internal.ForeignPtr.newForeignPtr_ :: p:(GHC.Internal.Ptr.Ptr a) -> (GHC.Types.IO (ForeignPtrN a (plen p))) -assume GHC.Internal.ForeignPtr.mallocPlainForeignPtrBytes :: n:{v:GHC.Types.Int | v >= 0 } -> (GHC.Types.IO (ForeignPtrN a n)) +assume GHC.Internal.ForeignPtr.newForeignPtr_ :: p:(Ptr a) -> (IO (ForeignPtrN a (plen p))) +assume GHC.Internal.ForeignPtr.mallocPlainForeignPtrBytes :: n:{v:Int | v >= 0 } -> (IO (ForeignPtrN a n)) @-} diff --git a/src/GHC/IO/Handle_LHAssumptions.hs b/src/GHC/IO/Handle_LHAssumptions.hs index fa25374ab5..1cb77ea8b7 100644 --- a/src/GHC/IO/Handle_LHAssumptions.hs +++ b/src/GHC/IO/Handle_LHAssumptions.hs @@ -3,15 +3,16 @@ module GHC.IO.Handle_LHAssumptions where import GHC.IO.Handle +import GHC.Ptr import GHC.Types_LHAssumptions() {-@ -assume GHC.Internal.IO.Handle.Text.hGetBuf :: GHC.Internal.IO.Handle.Handle -> GHC.Internal.Ptr.Ptr a -> n:Nat - -> (GHC.Types.IO {v:Nat | v <= n}) +assume GHC.Internal.IO.Handle.Text.hGetBuf :: Handle -> Ptr a -> n:Nat + -> (IO {v:Nat | v <= n}) -assume GHC.Internal.IO.Handle.Text.hGetBufNonBlocking :: GHC.Internal.IO.Handle.Handle -> GHC.Internal.Ptr.Ptr a -> n:Nat - -> (GHC.Types.IO {v:Nat | v <= n}) +assume GHC.Internal.IO.Handle.Text.hGetBufNonBlocking :: Handle -> Ptr a -> n:Nat + -> (IO {v:Nat | v <= n}) -assume GHC.Internal.IO.Handle.hFileSize :: GHC.Internal.IO.Handle.Handle - -> (GHC.Types.IO {v:Integer | v >= 0}) +assume GHC.Internal.IO.Handle.hFileSize :: Handle + -> (IO {v:Integer | v >= 0}) @-} diff --git a/src/GHC/Int_LHAssumptions.hs b/src/GHC/Int_LHAssumptions.hs index c10bd5ad3f..6598669479 100644 --- a/src/GHC/Int_LHAssumptions.hs +++ b/src/GHC/Int_LHAssumptions.hs @@ -5,10 +5,10 @@ module GHC.Int_LHAssumptions where import GHC.Int {-@ -embed GHC.Internal.Int.Int8 as int -embed GHC.Internal.Int.Int16 as int -embed GHC.Internal.Int.Int32 as int -embed GHC.Internal.Int.Int64 as int +embed Int8 as int +embed Int16 as int +embed Int32 as int +embed Int64 as int -type Nat64 = {v:GHC.Internal.Int.Int64 | v >= 0} +type Nat64 = {v:Int64 | v >= 0} @-} diff --git a/src/GHC/Internal/Base_LHAssumptions.hs b/src/GHC/Internal/Base_LHAssumptions.hs index ece6f6a575..6ef2577353 100644 --- a/src/GHC/Internal/Base_LHAssumptions.hs +++ b/src/GHC/Internal/Base_LHAssumptions.hs @@ -16,12 +16,12 @@ assume GHC.Internal.Base.. :: forall

c -> Bool, q :: a -> b -> Bool, -> (zcmp:a -> b) -> xcmp:a -> c -measure autolen :: forall a. a -> GHC.Types.Int +measure autolen :: forall a. a -> Int // Useless as compiled into GHC primitive, which is ignored assume GHC.Internal.Base.assert :: {v:Bool | v } -> a -> a -instance measure len :: forall a. [a] -> GHC.Types.Int +instance measure len :: forall a. [a] -> Int len [] = 0 len (y:ys) = 1 + len ys @@ -32,8 +32,8 @@ assume GHC.Internal.Base.++ :: xs:[a] -> ys:[a] -> {v:[a] | len v == len assume (GHC.Internal.Base.$) :: (a -> b) -> a -> b assume GHC.Internal.Base.id :: x:a -> {v:a | v = x} -qualif IsEmp(v:GHC.Types.Bool, xs: [a]) : (v <=> (len xs > 0)) -qualif IsEmp(v:GHC.Types.Bool, xs: [a]) : (v <=> (len xs = 0)) +qualif IsEmp(v:Bool, xs: [a]) : (v <=> (len xs > 0)) +qualif IsEmp(v:Bool, xs: [a]) : (v <=> (len xs = 0)) qualif ListZ(v: [a]) : (len v = 0) qualif ListZ(v: [a]) : (len v >= 0) diff --git a/src/GHC/Internal/Data/Foldable_LHAssumptions.hs b/src/GHC/Internal/Data/Foldable_LHAssumptions.hs index 745ddae37a..771be54c00 100644 --- a/src/GHC/Internal/Data/Foldable_LHAssumptions.hs +++ b/src/GHC/Internal/Data/Foldable_LHAssumptions.hs @@ -1,9 +1,11 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Internal.Data.Foldable_LHAssumptions where +import GHC.Internal.Data.Foldable import GHC.Types_LHAssumptions() {-@ -assume GHC.Internal.Data.Foldable.length :: GHC.Internal.Data.Foldable.Foldable f => forall a. xs:f a -> {v:Nat | v = len xs} -assume GHC.Internal.Data.Foldable.null :: GHC.Internal.Data.Foldable.Foldable f => forall a. v:(f a) -> {b:Bool | (b <=> len v = 0) && (not b <=> len v > 0)} +assume GHC.Internal.Data.Foldable.length :: Foldable f => forall a. xs:f a -> {v:Nat | v = len xs} +assume GHC.Internal.Data.Foldable.null :: Foldable f => forall a. v:(f a) -> {b:Bool | (b <=> len v = 0) && (not b <=> len v > 0)} @-} diff --git a/src/GHC/Internal/Data/Maybe_LHAssumptions.hs b/src/GHC/Internal/Data/Maybe_LHAssumptions.hs index be06ae9cbe..80c1771f0e 100644 --- a/src/GHC/Internal/Data/Maybe_LHAssumptions.hs +++ b/src/GHC/Internal/Data/Maybe_LHAssumptions.hs @@ -3,19 +3,20 @@ module GHC.Internal.Data.Maybe_LHAssumptions where import GHC.Types_LHAssumptions() -import Data.Maybe +import GHC.Internal.Data.Maybe +import GHC.Internal.Maybe {-@ -assume GHC.Internal.Data.Maybe.maybe :: v:b -> (a -> b) -> u:(GHC.Internal.Maybe.Maybe a) -> {w:b | not (isJust u) => w == v} -assume GHC.Internal.Data.Maybe.isNothing :: v:(GHC.Internal.Maybe.Maybe a) -> {b:Bool | not (isJust v) == b} -assume GHC.Internal.Data.Maybe.fromMaybe :: v:a -> u:(GHC.Internal.Maybe.Maybe a) -> {x:a | not (isJust u) => x == v} +assume GHC.Internal.Data.Maybe.maybe :: v:b -> (a -> b) -> u:(Maybe a) -> {w:b | not (isJust u) => w == v} +assume GHC.Internal.Data.Maybe.isNothing :: v:(Maybe a) -> {b:Bool | not (isJust v) == b} +assume GHC.Internal.Data.Maybe.fromMaybe :: v:a -> u:(Maybe a) -> {x:a | not (isJust u) => x == v} -assume GHC.Internal.Data.Maybe.isJust :: v:(GHC.Internal.Maybe.Maybe a) -> {b:Bool | b == isJust v} -measure isJust :: GHC.Internal.Maybe.Maybe a -> Bool - isJust (GHC.Internal.Maybe.Just x) = true - isJust (GHC.Internal.Maybe.Nothing) = false +assume GHC.Internal.Data.Maybe.isJust :: v:(Maybe a) -> {b:Bool | b == isJust v} +measure isJust :: Maybe a -> Bool + isJust (Just x) = true + isJust (Nothing) = false -assume GHC.Internal.Data.Maybe.fromJust :: {v:(GHC.Internal.Maybe.Maybe a) | isJust v} -> a -measure fromJust :: GHC.Internal.Maybe.Maybe a -> a - fromJust (GHC.Internal.Maybe.Just x) = x +assume GHC.Internal.Data.Maybe.fromJust :: {v:(Maybe a) | isJust v} -> a +measure fromJust :: Maybe a -> a + fromJust (Just x) = x @-} diff --git a/src/GHC/Internal/Float_LHAssumptions.hs b/src/GHC/Internal/Float_LHAssumptions.hs index e1111bc9fc..515fdb417f 100644 --- a/src/GHC/Internal/Float_LHAssumptions.hs +++ b/src/GHC/Internal/Float_LHAssumptions.hs @@ -1,6 +1,10 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Internal.Float_LHAssumptions(Floating(..)) where +import GHC.Internal.Float +import GHC.Internal.Real + {-@ class (GHC.Internal.Real.Fractional a) => GHC.Internal.Float.Floating a where GHC.Internal.Float.pi :: a diff --git a/src/GHC/Internal/Int_LHAssumptions.hs b/src/GHC/Internal/Int_LHAssumptions.hs index f5b760a553..d0ca2d4743 100644 --- a/src/GHC/Internal/Int_LHAssumptions.hs +++ b/src/GHC/Internal/Int_LHAssumptions.hs @@ -1,10 +1,12 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Internal.Int_LHAssumptions where -{-@ -embed GHC.Internal.Int.Int8 as int -embed GHC.Internal.Int.Int16 as int -embed GHC.Internal.Int.Int32 as int -embed GHC.Internal.Int.Int64 as int +import GHC.Internal.Int +{-@ +embed Int8 as int +embed Int16 as int +embed Int32 as int +embed Int64 as int @-} diff --git a/src/GHC/Internal/List_LHAssumptions.hs b/src/GHC/Internal/List_LHAssumptions.hs index 6dcf748c88..d9dbef3fa0 100644 --- a/src/GHC/Internal/List_LHAssumptions.hs +++ b/src/GHC/Internal/List_LHAssumptions.hs @@ -2,7 +2,7 @@ {-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Internal.List_LHAssumptions where -import GHC.List +import GHC.Internal.List import GHC.Types_LHAssumptions() {-@ @@ -12,9 +12,9 @@ assume GHC.Internal.List.tail :: xs:{v: [a] | len v > 0} -> {v: [a] | le assume GHC.Internal.List.last :: xs:{v: [a] | len v > 0} -> a assume GHC.Internal.List.init :: xs:{v: [a] | len v > 0} -> {v: [a] | len(v) = len(xs) - 1} -assume GHC.Internal.List.null :: xs:[a] -> {v: GHC.Types.Bool | ((v) <=> len(xs) = 0) } -assume GHC.Internal.List.length :: xs:[a] -> {v: GHC.Types.Int | v = len(xs)} -assume GHC.Internal.List.filter :: (a -> GHC.Types.Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)} +assume GHC.Internal.List.null :: xs:[a] -> {v: Bool | ((v) <=> len(xs) = 0) } +assume GHC.Internal.List.length :: xs:[a] -> {v: Int | v = len(xs)} +assume GHC.Internal.List.filter :: (a -> Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)} assume GHC.Internal.List.scanl :: (a -> b -> a) -> a -> xs:[b] -> {v: [a] | len(v) = 1 + len(xs) } assume GHC.Internal.List.scanl1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) } assume GHC.Internal.List.foldr1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> a @@ -32,22 +32,22 @@ assume GHC.Internal.List.replicate :: n:Nat -> x:a -> {v: [{v:a | v = x}] | l assume GHC.Internal.List.cycle :: {v: [a] | len(v) > 0 } -> [a] lazy GHC.Internal.List.cycle -assume GHC.Internal.List.takeWhile :: (a -> GHC.Types.Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)} -assume GHC.Internal.List.dropWhile :: (a -> GHC.Types.Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)} +assume GHC.Internal.List.takeWhile :: (a -> Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)} +assume GHC.Internal.List.dropWhile :: (a -> Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)} -assume GHC.Internal.List.take :: n:GHC.Types.Int +assume GHC.Internal.List.take :: n:Int -> xs:[a] -> {v:[a] | if n >= 0 then (len v = (if (len xs) < n then (len xs) else n)) else (len v = 0)} -assume GHC.Internal.List.drop :: n:GHC.Types.Int +assume GHC.Internal.List.drop :: n:Int -> xs:[a] -> {v:[a] | (if (n >= 0) then (len(v) = (if (len(xs) < n) then 0 else len(xs) - n)) else ((len v) = (len xs)))} assume GHC.Internal.List.splitAt :: n:_ -> x:[a] -> ({v:[a] | (if (n >= 0) then (if (len x) < n then (len v) = (len x) else (len v) = n) else ((len v) = 0))},[a])<{\x1 x2 -> (len x2) = (len x) - (len x1)}> -assume GHC.Internal.List.span :: (a -> GHC.Types.Bool) +assume GHC.Internal.List.span :: (a -> Bool) -> xs:[a] -> ({v:[a]|((len v)<=(len xs))}, {v:[a]|((len v)<=(len xs))}) -assume GHC.Internal.List.break :: (a -> GHC.Types.Bool) -> xs:[a] -> ([a],[a])<{\x y -> (len xs) = (len x) + (len y)}> +assume GHC.Internal.List.break :: (a -> Bool) -> xs:[a] -> ([a],[a])<{\x y -> (len xs) = (len x) + (len y)}> assume GHC.Internal.List.reverse :: xs:[a] -> {v: [a] | len(v) = len(xs)} diff --git a/src/GHC/Internal/Num_LHAssumptions.hs b/src/GHC/Internal/Num_LHAssumptions.hs index 93ce59efdb..33c233af66 100644 --- a/src/GHC/Internal/Num_LHAssumptions.hs +++ b/src/GHC/Internal/Num_LHAssumptions.hs @@ -1,17 +1,19 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Internal.Num_LHAssumptions where +import GHC.Internal.Num import GHC.Num.Integer_LHAssumptions() {-@ -assume GHC.Internal.Num.fromInteger :: x:GHC.Num.Integer.Integer -> {v:a | v = x } +assume GHC.Internal.Num.fromInteger :: x:Integer -> {v:a | v = x } -assume GHC.Internal.Num.negate :: (GHC.Internal.Num.Num a) +assume GHC.Internal.Num.negate :: (Num a) => x:a -> {v:a | v = -x} -assume GHC.Internal.Num.abs :: (GHC.Internal.Num.Num a) => x:a -> {y:a | (x >= 0 ==> y = x) && (x < 0 ==> y = -x) } +assume GHC.Internal.Num.abs :: (Num a) => x:a -> {y:a | (x >= 0 ==> y = x) && (x < 0 ==> y = -x) } assume GHC.Internal.Num.+ :: x:a -> y:a -> {v:a | v = x + y } -assume GHC.Internal.Num.- :: (GHC.Internal.Num.Num a) => x:a -> y:a -> {v:a | v = x - y } +assume GHC.Internal.Num.- :: (Num a) => x:a -> y:a -> {v:a | v = x - y } @-} diff --git a/src/GHC/Internal/Word_LHAssumptions.hs b/src/GHC/Internal/Word_LHAssumptions.hs index 75ac775381..44cf8e6695 100644 --- a/src/GHC/Internal/Word_LHAssumptions.hs +++ b/src/GHC/Internal/Word_LHAssumptions.hs @@ -1,13 +1,16 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Internal.Word_LHAssumptions where +import GHC.Internal.Word + {-@ -embed GHC.Internal.Word.Word as int -embed GHC.Internal.Word.Word8 as int -embed GHC.Internal.Word.Word16 as int -embed GHC.Internal.Word.Word32 as int -embed GHC.Internal.Word.Word64 as int +embed Word as int +embed Word8 as int +embed Word16 as int +embed Word32 as int +embed Word64 as int -invariant {v : GHC.Internal.Word.Word32 | 0 <= v } -invariant {v : GHC.Internal.Word.Word16 | 0 <= v } +invariant {v : Word32 | 0 <= v } +invariant {v : Word16 | 0 <= v } @-} diff --git a/src/GHC/Num/Integer_LHAssumptions.hs b/src/GHC/Num/Integer_LHAssumptions.hs index fc0f051e10..4b32bb0a92 100644 --- a/src/GHC/Num/Integer_LHAssumptions.hs +++ b/src/GHC/Num/Integer_LHAssumptions.hs @@ -3,12 +3,12 @@ {-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Num.Integer_LHAssumptions() where -import GHC.Types +import GHC.Prim import GHC.Num.Integer import GHC.Types_LHAssumptions() {-@ -assume GHC.Num.Integer.IS :: x:GHC.Prim.Int# -> {v: GHC.Num.Integer.Integer | v = (x :: int) } +assume GHC.Num.Integer.IS :: x:Int# -> {v: Integer | v = (x :: int) } -embed GHC.Num.Integer.Integer as int +embed Integer as int @-} diff --git a/src/GHC/Ptr_LHAssumptions.hs b/src/GHC/Ptr_LHAssumptions.hs index fcf69d0051..74210fbd53 100644 --- a/src/GHC/Ptr_LHAssumptions.hs +++ b/src/GHC/Ptr_LHAssumptions.hs @@ -2,13 +2,13 @@ {-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Ptr_LHAssumptions where -import GHC.Ptr +import GHC.Internal.Ptr import GHC.Types_LHAssumptions() {-@ -measure pbase :: GHC.Internal.Ptr.Ptr a -> GHC.Types.Int -measure plen :: GHC.Internal.Ptr.Ptr a -> GHC.Types.Int -measure isNullPtr :: GHC.Internal.Ptr.Ptr a -> Bool +measure pbase :: GHC.Internal.Ptr.Ptr a -> Int +measure plen :: GHC.Internal.Ptr.Ptr a -> Int +measure isNullPtr :: GHC.Internal.Ptr.Ptr a -> Bool type PtrN a N = {v: PtrV a | plen v == N } type PtrV a = {v: GHC.Internal.Ptr.Ptr a | 0 <= plen v } @@ -16,12 +16,12 @@ type PtrV a = {v: GHC.Internal.Ptr.Ptr a | 0 <= plen v } assume GHC.Internal.Ptr.castPtr :: p:(PtrV a) -> (PtrN b (plen p)) assume GHC.Internal.Ptr.plusPtr :: base:(PtrV a) - -> off:{v:GHC.Types.Int | v <= plen base } + -> off:{v:Int | v <= plen base } -> {v:(PtrV b) | pbase v = pbase base && plen v = plen base - off} assume GHC.Internal.Ptr.minusPtr :: q:(PtrV a) -> p:{v:(PtrV b) | pbase v == pbase q && plen v >= plen q} -> {v:Nat | v == plen p - plen q} -measure deref :: GHC.Internal.Ptr.Ptr a -> a +measure deref :: Ptr a -> a @-} diff --git a/src/GHC/Real_LHAssumptions.hs b/src/GHC/Real_LHAssumptions.hs index 7637c38ed4..0a8fed89b2 100644 --- a/src/GHC/Real_LHAssumptions.hs +++ b/src/GHC/Real_LHAssumptions.hs @@ -1,7 +1,11 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} -- Reexports are necessary for LH to expose specs of type classes module GHC.Real_LHAssumptions(Integral(..), Fractional(..)) where +import GHC.Internal.Enum +import GHC.Internal.Num +import GHC.Internal.Real import GHC.Types_LHAssumptions() {-@ diff --git a/src/GHC/Types_LHAssumptions.hs b/src/GHC/Types_LHAssumptions.hs index 6699ada378..97389f2765 100644 --- a/src/GHC/Types_LHAssumptions.hs +++ b/src/GHC/Types_LHAssumptions.hs @@ -1,8 +1,10 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} {-# LANGUAGE MagicHash #-} {-# OPTIONS_GHC -Wno-missing-signatures #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.Types_LHAssumptions() where +import GHC.Prim import GHC.Types -- This definition is needed to make the listed data constructors @@ -11,43 +13,43 @@ _f = (D#, F#, W#) {-@ // Boxed types -embed GHC.Types.Double as real -embed GHC.Prim.Double# as real -embed GHC.Types.Float as real -embed GHC.Prim.Float# as real -embed GHC.Types.Word as int -embed GHC.Prim.Word# as int -embed GHC.Prim.Word64# as int -embed GHC.Types.Int as int -embed GHC.Prim.Int# as int -embed GHC.Types.Bool as bool -embed GHC.Types.Char as Char -embed GHC.Prim.Char# as Char -embed GHC.Prim.Addr# as Str - -embed GHC.Num.Integer.Integer as int - -assume GHC.Types.True :: {v:GHC.Types.Bool | v } -assume GHC.Types.False :: {v:GHC.Types.Bool | (~ v) } -assume GHC.Types.isTrue# :: n:_ -> {v:GHC.Types.Bool | (n = 1 <=> v)} - -assume GHC.Types.D# :: x:GHC.Prim.Double# -> {v: GHC.Types.Double | v = (x :: real) } -assume GHC.Types.F# :: x:GHC.Prim.Float# -> {v: GHC.Types.Float | v = (x :: real) } -assume GHC.Types.I# :: x:GHC.Prim.Int# -> {v: GHC.Types.Int | v = (x :: int) } -assume GHC.Types.C# :: x:GHC.Prim.Char# -> {v: GHC.Types.Char | v = (x :: Char) } -assume GHC.Types.W# :: w:GHC.Prim.Word# -> {v:GHC.Types.Word | v == w } - -measure addrLen :: GHC.Prim.Addr# -> GHC.Types.Int - -type GeInt N = {v: GHC.Types.Int | v >= N } -type LeInt N = {v: GHC.Types.Int | v <= N } -type Nat = {v: GHC.Types.Int | v >= 0 } -type Even = {v: GHC.Types.Int | (v mod 2) = 0 } -type Odd = {v: GHC.Types.Int | (v mod 2) = 1 } +embed Double as real +embed Double# as real +embed Float as real +embed Float# as real +embed Word as int +embed Word# as int +embed Word64# as int +embed Int as int +embed Int# as int +embed Bool as bool +embed Char as Char +embed Char# as Char +embed Addr# as Str + +embed Integer as int + +assume GHC.Types.True :: {v:Bool | v } +assume GHC.Types.False :: {v:Bool | (~ v) } +assume GHC.Types.isTrue# :: n:_ -> {v:Bool | (n = 1 <=> v)} + +assume GHC.Types.D# :: x:Double# -> {v: Double | v = (x :: real) } +assume GHC.Types.F# :: x:Float# -> {v: Float | v = (x :: real) } +assume GHC.Types.I# :: x:Int# -> {v: Int | v = (x :: int) } +assume GHC.Types.C# :: x:Char# -> {v: Char | v = (x :: Char) } +assume GHC.Types.W# :: w:Word# -> {v:Word | v == w } + +measure addrLen :: GHC.Prim.Addr# -> Int + +type GeInt N = {v: Int | v >= N } +type LeInt N = {v: Int | v <= N } +type Nat = {v: Int | v >= 0 } +type Even = {v: Int | (v mod 2) = 0 } +type Odd = {v: Int | (v mod 2) = 1 } type BNat N = {v: Nat | v <= N } -type TT = {v: GHC.Types.Bool | v} -type FF = {v: GHC.Types.Bool | not v} -type String = [GHC.Types.Char] +type TT = {v: Bool | v} +type FF = {v: Bool | not v} +type String = [Char] -class measure len :: forall f a. f a -> GHC.Types.Int +class measure len :: forall f a. f a -> Int @-} diff --git a/src/Liquid/Prelude/Real_LHAssumptions.hs b/src/Liquid/Prelude/Real_LHAssumptions.hs index 850b1e08b0..b316d5a32c 100644 --- a/src/Liquid/Prelude/Real_LHAssumptions.hs +++ b/src/Liquid/Prelude/Real_LHAssumptions.hs @@ -1,8 +1,9 @@ {-# OPTIONS_GHC -fplugin=LiquidHaskellBoot #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} module Liquid.Prelude.Real_LHAssumptions where -import GHC.Num() +import GHC.Internal.Num {-@ -assume GHC.Internal.Num.* :: (GHC.Internal.Num.Num a) => x:a -> y:a -> {v:a | v = x * y} +assume GHC.Internal.Num.* :: Num a => x:a -> y:a -> {v:a | v = x * y} @-} diff --git a/src/Liquid/Prelude/Totality_LHAssumptions.hs b/src/Liquid/Prelude/Totality_LHAssumptions.hs index 5b861d7ff5..30432212e9 100644 --- a/src/Liquid/Prelude/Totality_LHAssumptions.hs +++ b/src/Liquid/Prelude/Totality_LHAssumptions.hs @@ -3,17 +3,18 @@ module Liquid.Prelude.Totality_LHAssumptions where import Control.Exception.Base +import GHC.Prim {-@ measure totalityError :: a -> Bool -assume GHC.Internal.Control.Exception.Base.patError :: {v:GHC.Prim.Addr# | totalityError "Pattern match(es) are non-exhaustive"} -> a +assume GHC.Internal.Control.Exception.Base.patError :: {v:Addr# | totalityError "Pattern match(es) are non-exhaustive"} -> a -assume GHC.Internal.Control.Exception.Base.recSelError :: {v:GHC.Prim.Addr# | totalityError "Use of partial record field selector"} -> a +assume GHC.Internal.Control.Exception.Base.recSelError :: {v:Addr# | totalityError "Use of partial record field selector"} -> a -assume GHC.Internal.Control.Exception.Base.nonExhaustiveGuardsError :: {v:GHC.Prim.Addr# | totalityError "Guards are non-exhaustive"} -> a +assume GHC.Internal.Control.Exception.Base.nonExhaustiveGuardsError :: {v:Addr# | totalityError "Guards are non-exhaustive"} -> a -assume GHC.Internal.Control.Exception.Base.noMethodBindingError :: {v:GHC.Prim.Addr# | totalityError "Missing method(s) on instance declaration"} -> a +assume GHC.Internal.Control.Exception.Base.noMethodBindingError :: {v:Addr# | totalityError "Missing method(s) on instance declaration"} -> a -assume GHC.Internal.Control.Exception.Base.recConError :: {v:GHC.Prim.Addr# | totalityError "Missing field in record construction"} -> a +assume GHC.Internal.Control.Exception.Base.recConError :: {v:Addr# | totalityError "Missing field in record construction"} -> a @-} diff --git a/tests/basic/neg/Inc01.hs b/tests/basic/neg/Inc01.hs index dcdb3f593f..23fbe31ead 100644 --- a/tests/basic/neg/Inc01.hs +++ b/tests/basic/neg/Inc01.hs @@ -2,16 +2,16 @@ -- | Test module Inc01 where -{-@ inc :: {v:GHC.Types.Int | v >= 0} -> {v:GHC.Types.Int | v >= 0} @-} +{-@ inc :: {v:Int | v >= 0} -> {v:Int | v >= 0} @-} inc :: Int -> Int inc x = plus x one -{-@ one :: {v:GHC.Types.Int | v >= 0} @-} +{-@ one :: {v:Int | v >= 0} @-} one :: Int one = undefined -{-@ plus :: x:GHC.Types.Int -> y:GHC.Types.Int -> {v:GHC.Types.Int| v = x - y} @-} +{-@ plus :: x:Int -> y:Int -> {v:Int| v = x - y} @-} plus :: Int -> Int -> Int plus = undefined diff --git a/tests/basic/pos/Inc01.hs b/tests/basic/pos/Inc01.hs index 2ab054dbad..37b50f284c 100644 --- a/tests/basic/pos/Inc01.hs +++ b/tests/basic/pos/Inc01.hs @@ -1,15 +1,15 @@ -- | Test module Inc01 where -{-@ inc :: {v:GHC.Types.Int | v >= 0} -> {v:GHC.Types.Int | v >= 0} @-} +{-@ inc :: {v:Int | v >= 0} -> {v:Int | v >= 0} @-} inc :: Int -> Int inc x = plus x one -{-@ one :: {v:GHC.Types.Int | v >= 0} @-} +{-@ one :: {v:Int | v >= 0} @-} one :: Int one = undefined -{-@ plus :: x:GHC.Types.Int -> y:GHC.Types.Int -> {v:GHC.Types.Int| v = x + y} @-} +{-@ plus :: x:Int -> y:Int -> {v:Int| v = x + y} @-} plus :: Int -> Int -> Int plus = undefined diff --git a/tests/basic/pos/OpaqueRefl02.hs b/tests/basic/pos/OpaqueRefl02.hs index 284b72ad67..ba425de3c9 100644 --- a/tests/basic/pos/OpaqueRefl02.hs +++ b/tests/basic/pos/OpaqueRefl02.hs @@ -4,11 +4,11 @@ module OpaqueRefl02 where -{-@ measure GHC.Internal.List.filter :: (a -> Bool) -> [a] -> [a] @-} -{-@ assume GHC.Internal.List.filter :: p:(a -> Bool) -> xs:[a] -> {v : [a] | v == GHC.Internal.List.filter p xs && len v <= len xs} @-} -{-@ measure GHC.Internal.Real.even :: a -> GHC.Types.Bool @-} -{-@ assume GHC.Internal.Real.even :: x:a -> {VV : GHC.Types.Bool | VV == GHC.Internal.Real.even x} @-} +{-@ measure filter :: (a -> Bool) -> [a] -> [a] @-} +{-@ assume filter :: p:(a -> Bool) -> xs:[a] -> {v : [a] | v == filter p xs && len v <= len xs} @-} +{-@ measure even :: a -> Bool @-} +{-@ assume even :: x:a -> {VV : Bool | VV == even x} @-} {-@ reflect keepEvens @-} keepEvens :: [Int] -> [Int] -keepEvens = filter even \ No newline at end of file +keepEvens = filter even diff --git a/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/Internal.hs b/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/Internal.hs index 8ad470f3e1..1917aa040a 100644 --- a/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/Internal.hs +++ b/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/Internal.hs @@ -562,7 +562,7 @@ memchr p w s = c_memchr p (fromIntegral w) s foreign import ccall unsafe "string.h memcmp" memcmp :: Ptr Word8 -> Ptr Word8 -> CSize -> IO CInt -{-@ assume memcmp :: p:(Ptr Word8) -> q:(Ptr Word8) -> {v:CSize | (v <= (plen p) && v <= (plen q)) } -> IO GHC.Internal.Foreign.C.Types.CInt @-} +{-@ assume memcmp :: p:(Ptr Word8) -> q:(Ptr Word8) -> {v:CSize | (v <= (plen p) && v <= (plen q)) } -> IO CInt @-} foreign import ccall unsafe "string.h memcpy" c_memcpy :: Ptr Word8 -> Ptr Word8 -> CSize -> IO (Ptr Word8) diff --git a/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/Lazy.hs b/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/Lazy.hs index 901457e3b7..d1ca98e450 100644 --- a/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/Lazy.hs +++ b/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/Lazy.hs @@ -589,7 +589,7 @@ init :: ByteString -> ByteString -- init Empty = errorEmptyList "init" init (Chunk c0 cs0) = goInit c0 cs0 -{-@ goInit :: c:{Data.ByteString.Internal.ByteString | bLength c > 0} -> cs:ByteString -> {v:ByteString | lbLength v = bLength c + lbLength cs - 1} / [lbLength cs] @-} +{-@ goInit :: c:{S.ByteString | bLength c > 0} -> cs:ByteString -> {v:ByteString | lbLength v = bLength c + lbLength cs - 1} / [lbLength cs] @-} goInit :: S.ByteString -> ByteString -> ByteString goInit c Empty | S.length c == 1 = Empty | otherwise = Chunk (S.init c) Empty diff --git a/tests/benchmarks/esop2013-submission/Base.hs b/tests/benchmarks/esop2013-submission/Base.hs index af88594923..4659a4593d 100644 --- a/tests/benchmarks/esop2013-submission/Base.hs +++ b/tests/benchmarks/esop2013-submission/Base.hs @@ -1129,7 +1129,7 @@ alter_go f k (Bin sx kx x l r) = case compare k kx of -- See Note: Type of local 'go' function -{-@ findIndex :: (Ord k) => k -> OMap k a -> GHC.Types.Int @-} +{-@ findIndex :: (Ord k) => k -> OMap k a -> Int @-} findIndex :: Ord k => k -> Map k a -> Int findIndex = findIndex_go 0 --LIQUID findIndex = go 0 @@ -1143,7 +1143,7 @@ findIndex = findIndex_go 0 --LIQUID GT -> go (idx + size l + 1) k r --LIQUID EQ -> idx + size l -{-@ findIndex_go :: (Ord k) => Int -> k -> OMap k a -> GHC.Types.Int @-} +{-@ findIndex_go :: (Ord k) => Int -> k -> OMap k a -> Int @-} findIndex_go :: Ord k => Int -> k -> Map k a -> Int STRICT_1_OF_3(findIndex_go) STRICT_2_OF_3(findIndex_go) @@ -1165,7 +1165,7 @@ findIndex_go idx k (Bin _ kx _ l r) = case compare k kx of -- > isJust (lookupIndex 6 (fromList [(5,"a"), (3,"b")])) == False -- See Note: Type of local 'go' function -{-@ lookupIndex :: (Ord k) => k -> OMap k a -> Maybe GHC.Types.Int @-} +{-@ lookupIndex :: (Ord k) => k -> OMap k a -> Maybe Int @-} lookupIndex :: Ord k => k -> Map k a -> Maybe Int lookupIndex = lookupIndex_go 0 --LIQUID lookupIndex = go 0 @@ -1179,7 +1179,7 @@ lookupIndex = lookupIndex_go 0 --LIQUID GT -> go (idx + size l + 1) k r --LIQUID EQ -> Just $! idx + size l -{-@ lookupIndex_go :: (Ord k) => Int -> k -> OMap k a -> Maybe GHC.Types.Int @-} +{-@ lookupIndex_go :: (Ord k) => Int -> k -> OMap k a -> Maybe Int @-} lookupIndex_go :: Ord k => Int -> k -> Map k a -> Maybe Int STRICT_1_OF_3(lookupIndex_go) STRICT_2_OF_3(lookupIndex_go) @@ -1200,7 +1200,7 @@ lookupIndex_go idx k (Bin _ kx _ l r) = case compare k kx of -- > elemAt 2 (fromList [(5,"a"), (3,"b")]) Error: index out of range -{-@ elemAt :: GHC.Types.Int -> OMap k a -> (k, a) @-} +{-@ elemAt :: Int -> OMap k a -> (k, a) @-} elemAt :: Int -> Map k a -> (k,a) STRICT_1_OF_2(elemAt) elemAt _ Tip = error "Map.elemAt: index out of range" @@ -1224,7 +1224,7 @@ elemAt i (Bin _ kx x l r) -- > updateAt (\_ _ -> Nothing) 2 (fromList [(5,"a"), (3,"b")]) Error: index out of range -- > updateAt (\_ _ -> Nothing) (-1) (fromList [(5,"a"), (3,"b")]) Error: index out of range -{-@ updateAt :: (k -> a -> Maybe a) -> GHC.Types.Int -> OMap k a -> OMap k a @-} +{-@ updateAt :: (k -> a -> Maybe a) -> Int -> OMap k a -> OMap k a @-} updateAt :: (k -> a -> Maybe a) -> Int -> Map k a -> Map k a updateAt f i t = i `seq` case t of @@ -1246,7 +1246,7 @@ updateAt f i t = i `seq` -- > deleteAt 2 (fromList [(5,"a"), (3,"b")]) Error: index out of range -- > deleteAt (-1) (fromList [(5,"a"), (3,"b")]) Error: index out of range -{-@ deleteAt :: GHC.Types.Int -> OMap k a -> OMap k a @-} +{-@ deleteAt :: Int -> OMap k a -> OMap k a @-} deleteAt :: Int -> Map k a -> Map k a deleteAt i t = i `seq` case t of diff --git a/tests/benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/Common.hs b/tests/benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/Common.hs index c2efc3c6fa..6900f47da6 100644 --- a/tests/benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/Common.hs +++ b/tests/benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/Common.hs @@ -56,20 +56,20 @@ import qualified Data.Vector.Primitive.Mutable -- | Assumed Types for Vector {-@ assume Data.Vector.Generic.Mutable.length - :: (Data.Vector.Generic.Mutable.Base.MVector v a) + :: (MVector v a) => x:(v s a) -> {v:Nat | v = (vsize x)} @-} {-@ assume Data.Vector.Generic.Mutable.unsafeRead - :: (PrimMonad m, Data.Vector.Generic.Mutable.Base.MVector v a) + :: (PrimMonad m, MVector v a) => x:(v (PrimState m) a) -> (OkIdx x) -> m a @-} {-@ assume Data.Vector.Generic.Mutable.unsafeWrite - :: (PrimMonad m, Data.Vector.Generic.Mutable.Base.MVector v a) + :: (PrimMonad m, MVector v a) => x:(v (PrimState m) a) -> (OkIdx x) -> a @@ -77,7 +77,7 @@ import qualified Data.Vector.Primitive.Mutable @-} {-@ assume Data.Vector.Generic.Mutable.unsafeSwap - :: (PrimMonad m, Data.Vector.Generic.Mutable.Base.MVector v a) + :: (PrimMonad m, MVector v a) => x:(v (PrimState m) a) -> (OkIdx x) -> (OkIdx x) @@ -85,7 +85,7 @@ import qualified Data.Vector.Primitive.Mutable @-} {-@ assume Data.Vector.Generic.Mutable.unsafeSlice - :: (Data.Vector.Generic.Mutable.Base.MVector v a) + :: (MVector v a) => i:Nat -> n:Nat -> {v:(v s a) | (OkOff v i n)} @@ -93,14 +93,14 @@ import qualified Data.Vector.Primitive.Mutable @-} {-@ assume Data.Vector.Generic.Mutable.unsafeCopy - :: (PrimMonad m, Data.Vector.Generic.Mutable.Base.MVector v a) + :: (PrimMonad m, MVector v a) => src:(v (PrimState m) a) -> {dst:(v (PrimState m) a) | (EqSiz src dst)} -> m () @-} {-@ assume Data.Vector.Generic.Mutable.new - :: (PrimMonad m, Data.Vector.Generic.Mutable.Base.MVector v a) + :: (PrimMonad m, MVector v a) => nINTENDO:Nat -> m {v: (v (PrimState m) a) | (vsize v) = nINTENDO} @-} diff --git a/tests/errors/MultiInstMeasures.hs b/tests/errors/MultiInstMeasures.hs index 9f5ef78bbb..a2910f8154 100644 --- a/tests/errors/MultiInstMeasures.hs +++ b/tests/errors/MultiInstMeasures.hs @@ -6,11 +6,11 @@ import GHC.Ptr {-@ class measure sizeOf :: forall a . Ptr a -> Int @-} -{-@ instance measure sizeOf :: (Ptr GHC.Internal.Word.Word16) -> Int +{-@ instance measure sizeOf :: (Ptr Word16) -> Int sizeOf (Ptr x) = 2 @-} -{-@ instance measure sizeOf :: (Ptr GHC.Internal.Word.Word32) -> Int +{-@ instance measure sizeOf :: (Ptr Word32) -> Int sizeOf (Ptr y) = 4 @-} diff --git a/tests/harness/Test/Groups.hs b/tests/harness/Test/Groups.hs index 6959697180..8537b42620 100644 --- a/tests/harness/Test/Groups.hs +++ b/tests/harness/Test/Groups.hs @@ -22,7 +22,7 @@ microTestGroups = , "datacon-neg" , "names-pos" , "names-neg" - , "name-resolution-neg" + , "name-resolution-pos" , "reflect-pos" , "reflect-neg" , "absref-pos" diff --git a/tests/name-resolution/neg/C.hs b/tests/name-resolution/neg/C.hs deleted file mode 100644 index 3e2bdaedc9..0000000000 --- a/tests/name-resolution/neg/C.hs +++ /dev/null @@ -1,8 +0,0 @@ -{-@ LIQUID "--expect-error-containing=Unknown type constructor `A.Ty`" @-} -module C where - -import B - --- This is an instance of Liquid Haskell's resolving names twice. --- `B.Exp` uses `Ty` which is defined in module A --- but it is somehow out of scope when compiling module C. diff --git a/tests/name-resolution/neg/A.hs b/tests/name-resolution/pos/A.hs similarity index 100% rename from tests/name-resolution/neg/A.hs rename to tests/name-resolution/pos/A.hs diff --git a/tests/name-resolution/neg/B.hs b/tests/name-resolution/pos/B.hs similarity index 100% rename from tests/name-resolution/neg/B.hs rename to tests/name-resolution/pos/B.hs diff --git a/tests/name-resolution/pos/C.hs b/tests/name-resolution/pos/C.hs new file mode 100644 index 0000000000..69923ff203 --- /dev/null +++ b/tests/name-resolution/pos/C.hs @@ -0,0 +1,9 @@ +{-# OPTIONS_GHC -Wno-unused-imports #-} +-- | This is an instance of Liquid Haskell's resolving names twice. +-- `B.Exp` uses `Ty` which is defined in module A +-- but it used to be out of scope when compiling module C before +-- fixing renaming bugs. +module C where + +import B + diff --git a/tests/names/pos/Assume01.hs b/tests/names/pos/Assume01.hs index f6470dca2e..1cf61acb5c 100644 --- a/tests/names/pos/Assume01.hs +++ b/tests/names/pos/Assume01.hs @@ -1,6 +1,6 @@ module Assume01 where -import qualified Data.Set as S +import Data.Set {-@ type UList a = {v:[a] | ListUnique v} @-} @@ -12,7 +12,7 @@ import qualified Data.Set as S {-@ predicate EqElts X Y = ((listElts X) = (listElts Y)) @-} -{-@ measure listDup :: [a] -> (Data.Set.Set a) +{-@ measure listDup :: [a] -> Set a listDup [] = {v | Set_emp v } listDup (x:xs) = {v | v = if (Set_mem x (listElts xs)) then (Set_cup (Set_sng x) (listDup xs)) else (listDup xs) } @-} diff --git a/tests/pos/ListISort_bag.hs b/tests/pos/ListISort_bag.hs index 693cfc6dd2..51bfc8c784 100644 --- a/tests/pos/ListISort_bag.hs +++ b/tests/pos/ListISort_bag.hs @@ -16,7 +16,7 @@ insert y (x:xs) | otherwise = x : insert y xs {-@ measure bag @-} -{-@ bag :: Ord a => [a] -> Bag a @-} +{-@ bag :: Ord a => [a] -> B.Bag a @-} bag :: (Ord a) => [a] -> B.Bag a bag [] = B.empty bag (x:xs) = B.put x (bag xs) diff --git a/tests/pos/MergeSort_bag.hs b/tests/pos/MergeSort_bag.hs index f342e838d3..fdafb78073 100644 --- a/tests/pos/MergeSort_bag.hs +++ b/tests/pos/MergeSort_bag.hs @@ -9,7 +9,7 @@ module MergeSort_bag (bag, sort) where import qualified Language.Haskell.Liquid.Bag as B {-@ measure bag @-} -{-@ bag :: Ord a => [a] -> Bag a @-} +{-@ bag :: Ord a => [a] -> B.Bag a @-} bag :: (Ord a) => [a] -> B.Bag a bag [] = B.empty bag (x:xs) = B.put x (bag xs) diff --git a/tests/pos/PrimInt0.hs b/tests/pos/PrimInt0.hs index bb71f76827..7543e31d7f 100644 --- a/tests/pos/PrimInt0.hs +++ b/tests/pos/PrimInt0.hs @@ -17,7 +17,7 @@ itake :: Int -> Int itake 0 = 0 itake n = 1 + itake (n - 1) -{-@ ptake :: n: {v: GHC.Prim.Int# | 0 <= v} -> {v:[a] | ((len v) >= n)} -> {v:[a] | (len(v) = n)} @-} +{-@ ptake :: n: {v: Int# | 0 <= v} -> {v:[a] | ((len v) >= n)} -> {v:[a] | (len(v) = n)} @-} ptake :: Int# -> [a] -> [a] ptake 0# _ = [] ptake n# (x:xs) = x : ptake (n# -# 1#) xs diff --git a/tests/pos/T2093.hs b/tests/pos/T2093.hs index 6273cf5f97..b1184b4401 100644 --- a/tests/pos/T2093.hs +++ b/tests/pos/T2093.hs @@ -2,8 +2,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE GADTs #-} -{-@ embed GHC.Natural.Natural as int @-} -{-@ embed GHC.Num.Natural.Natural as int @-} +{-@ embed Natural as int @-} {-@ LIQUID "--no-totality" @-} module T2093 where diff --git a/tests/tests.cabal b/tests/tests.cabal index b19523836f..5fea8e4916 100644 --- a/tests/tests.cabal +++ b/tests/tests.cabal @@ -857,10 +857,10 @@ executable names-neg default-language: Haskell2010 -flag name-resolution-neg +flag name-resolution-pos default: False -executable name-resolution-neg +executable name-resolution-pos main-is: Main.hs if !flag(names-neg) && flag(stack) buildable: False @@ -883,7 +883,7 @@ executable name-resolution-neg , liquidhaskell hs-source-dirs: app - , name-resolution/neg + , name-resolution/pos default-language: Haskell2010