diff --git a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs
index 0759a0e06b..cf7a1b0218 100644
--- a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs
+++ b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs
@@ -445,7 +445,12 @@ import GHC.Plugins as Ghc ( Serialized(Serialized)
, extendIdSubst
, substExpr
)
-import GHC.Core.FVs as Ghc (exprFreeVars, exprFreeVarsList, exprSomeFreeVarsList)
+import GHC.Core.FVs as Ghc
+ ( exprFreeVars
+ , exprFreeVarsList
+ , exprsOrphNames
+ , exprSomeFreeVarsList
+ )
import GHC.Core.Opt.OccurAnal as Ghc
( occurAnalysePgm )
import GHC.Core.TyCo.FVs as Ghc (tyCoVarsOfCo, tyCoVarsOfType)
@@ -543,6 +548,7 @@ import GHC.Types.Annotations as Ghc
import GHC.Types.Avail as Ghc
( AvailInfo(Avail, AvailTC)
, availNames
+ , availsToNameSet
)
import GHC.Types.Basic as Ghc
( Arity
@@ -630,6 +636,11 @@ import GHC.Types.Name as Ghc
)
import GHC.Types.Name.Env as Ghc
( lookupNameEnv )
+import GHC.Types.Name.Set as Ghc
+ ( NameSet
+ , elemNameSet
+ , nameSetElemsStable
+ )
import GHC.Types.Name.Cache as Ghc (NameCache)
import GHC.Types.Name.Occurrence as Ghc
( NameSpace
@@ -639,14 +650,23 @@ import GHC.Types.Name.Occurrence as Ghc
, tcName
)
import GHC.Types.Name.Reader as Ghc
- ( GlobalRdrEnv
+ ( FieldsOrSelectors(WantNormal)
+ , GlobalRdrEnv
+ , GREInfo
, ImpItemSpec(ImpAll)
, LookupGRE(LookupRdrName)
- , WhichGREs(SameNameSpace)
+ , WhichGREs
+ ( SameNameSpace
+ , RelevantGREs
+ , includeFieldSelectors
+ , lookupTyConsAsWell
+ , lookupVariablesForFields
+ )
, getRdrName
, globalRdrEnvElts
, greName
, lookupGRE
+ , lookupGRE_Name
, mkQual
, mkRdrQual
, mkRdrUnqual
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
index adf2f492e8..af2f423ef2 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
@@ -1,4 +1,5 @@
{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
@@ -45,6 +46,7 @@ import qualified Liquid.GHC.API as Ghc
import Language.Haskell.Liquid.GHC.Types (StableName)
import Language.Haskell.Liquid.Types.Errors
import Language.Haskell.Liquid.Types.DataDecl
+import Language.Haskell.Liquid.Types.Names
import Language.Haskell.Liquid.Types.PredType
import Language.Haskell.Liquid.Types.RefType
import Language.Haskell.Liquid.Types.RType
@@ -166,10 +168,12 @@ makeTargetSpec cfg lmap targetSrc bareSpec dependencies = do
-- Ghc.execOptions
diagOrSpec <- makeGhcSpec cfg (fromTargetSrc targetSrc) lmap legacyBareSpec legacyDependencies
- return $ do
- (warns, ghcSpec) <- diagOrSpec
- let (targetSpec, liftedSpec) = toTargetSpec ghcSpec
- pure (phaseOneWarns <> warns, targetSpec, liftedSpec)
+ case diagOrSpec of
+ Left d -> return $ Left d
+ Right (warns, ghcSpec) -> do
+ let (targetSpec, liftedSpec) = toTargetSpec ghcSpec
+ liftedSpec' <- removeUnexportedLocalAssumptions liftedSpec
+ return $ Right (phaseOneWarns <> warns, targetSpec, liftedSpec')
toLegacyDep :: (Ghc.StableModule, LiftedSpec) -> (ModName, Ms.BareSpec)
toLegacyDep (sm, ls) = (ModName SrcImport (Ghc.moduleName . Ghc.unStableModule $ sm), unsafeFromLiftedSpec ls)
@@ -180,6 +184,17 @@ makeTargetSpec cfg lmap targetSrc bareSpec dependencies = do
legacyBareSpec :: Ms.BareSpec
legacyBareSpec = fromBareSpec bareSpec
+ -- Assumptions about local functions that are not exported aren't useful for
+ -- other modules.
+ removeUnexportedLocalAssumptions :: LiftedSpec -> Ghc.TcRn LiftedSpec
+ removeUnexportedLocalAssumptions lspec = do
+ tcg <- Ghc.getGblEnv
+ let exportedNames = Ghc.availsToNameSet (Ghc.tcg_exports tcg)
+ exportedAssumption (LHNResolved (LHRGHC n) _) =
+ Ghc.nameModule_maybe n /= Just (Ghc.tcg_mod tcg) || Ghc.elemNameSet n exportedNames
+ exportedAssumption _ = True
+ return lspec { liftedAsmSigs = S.filter (exportedAssumption . val . fst) (liftedAsmSigs lspec) }
+
-------------------------------------------------------------------------------------
-- | @makeGhcSpec@ invokes @makeGhcSpec0@ to construct the @GhcSpec@ and then
-- validates it using @checkGhcSpec@.
@@ -974,10 +989,26 @@ allAsmSigs env myName specs = do
let aSigs = [ (name, locallyDefined, x, t) | (name, spec) <- M.toList specs
, (locallyDefined, x, t) <- getAsmSigs myName name spec ]
vSigs <- forM aSigs $ \(name, locallyDefined, x, t) -> do
+ vMb <- lookupSymbolOrLHName name locallyDefined x
+ return (vMb, (locallyDefined, name, t))
+ return $ Misc.groupList
+ [ (v, z) | (Just v, z) <- vSigs
+ -- TODO: we require signatures to be in scope because LH includes them in
+ -- the environment of contraints sometimes. The criteria to add bindings to
+ -- constraints should account instead for what logic functions are used in
+ -- the constraints, which should be easier to do when precise renaming has
+ -- been implemented for expressions and reflected functions.
+ , isUsedExternalVar v || isInScope v
+ ]
+ where
+ lookupSymbolOrLHName :: ModName -> Bool -> SymbolOrLHName -> Bare.Lookup (Maybe Ghc.Var)
+ lookupSymbolOrLHName _name _locallyDefined (SOLLHName x) =
+ Just <$> Bare.lookupGhcIdLHName env x
+ lookupSymbolOrLHName name locallyDefined (SOLSymbol x) = do
-- Qualified assumes that refer to module aliases import declarations
-- are resolved looking at import declarations
let (mm, s) = Bare.unQualifySymbol (val x)
- vMb <- if not (isAbsoluteQualifiedSym mm) then resolveAsmVar env name locallyDefined x
+ if not (isAbsoluteQualifiedSym mm) then resolveAsmVar env name locallyDefined x
else if locallyDefined then
-- Fully qualified assumes that are locally defined produce an error if they aren't found
lookupImportedSym x (mm, s)
@@ -988,9 +1019,7 @@ allAsmSigs env myName specs = do
-- LH seems to send here assumes for data constructors that
-- yield Nothing, like for GHC.Types.W#
return $ lookupImportedSymMaybe (mm, s)
- return (vMb, (locallyDefined, name, t))
- return $ Misc.groupList [ (v, z) | (Just v, z) <- vSigs ]
- where
+
lookupImportedSym x qp =
let errRes = Left [Bare.errResolve "variable" "Var" x]
in maybe errRes (Right . Just) $
@@ -1005,17 +1034,44 @@ allAsmSigs env myName specs = do
isAbsoluteQualifiedSym Nothing =
False
+ isUsedExternalVar :: Ghc.Var -> Bool
+ isUsedExternalVar v = case Ghc.idDetails v of
+ Ghc.DataConWrapId dc ->
+ Ghc.getName v `Ghc.elemNameSet` Bare.reUsedExternals env
+ ||
+ Ghc.getName (Ghc.dataConWorkId dc) `Ghc.elemNameSet` Bare.reUsedExternals env
+ _ ->
+ Ghc.getName v `Ghc.elemNameSet` Bare.reUsedExternals env
+
+ isInScope :: Ghc.Var -> Bool
+ isInScope v0 =
+ let inScope v = not $ null $
+ Ghc.lookupGRE_Name
+ (Ghc.tcg_rdr_env $ Bare.reTcGblEnv env)
+ (Ghc.getName v)
+ in -- Names of data constructors are not found in the variable namespace
+ -- so we look them instead in the data constructor namespace.
+ case Ghc.idDetails v0 of
+ Ghc.DataConWrapId dc -> inScope dc
+ Ghc.DataConWorkId dc -> inScope dc
+ _ -> inScope v0
+
resolveAsmVar :: Bare.Env -> ModName -> Bool -> LocSymbol -> Bare.Lookup (Maybe Ghc.Var)
resolveAsmVar env name True lx = Just <$> Bare.lookupGhcVar env name "resolveAsmVar-True" lx
resolveAsmVar env name False lx = return $ Bare.maybeResolveSym env name "resolveAsmVar-False" lx <|> GM.maybeAuxVar (F.val lx)
+-- | Temporary data type to represent a symbol or an LHName while not all of the
+-- code has been migrated to use LHName.
+data SymbolOrLHName = SOLSymbol LocSymbol | SOLLHName (Located LHName)
-getAsmSigs :: ModName -> ModName -> Ms.BareSpec -> [(Bool, LocSymbol, LocBareType)]
+getAsmSigs :: ModName -> ModName -> Ms.BareSpec -> [(Bool, SymbolOrLHName, LocBareType)]
getAsmSigs myName name spec
- | myName == name = [ (True, x, t) | (x, t) <- Ms.asmSigs spec ] -- MUST resolve, or error
- | otherwise = [ (False, x', t) | (x, t) <- Ms.asmSigs spec
- ++ Ms.sigs spec
- , let x' = qSym x ] -- MAY-NOT resolve
+ | myName == name = [ (True, SOLLHName x, t) | (x, t) <- Ms.asmSigs spec ] -- MUST resolve, or error
+ | otherwise =
+ [ (False, x, t)
+ | (x, t) <- map (first SOLLHName) (Ms.asmSigs spec)
+ ++ map (first (SOLSymbol . qSym)) (Ms.sigs spec)
+ ]
where
qSym = fmap (GM.qualifySymbol ns)
ns = F.symbol name
@@ -1343,10 +1399,11 @@ makeLiftedSpec :: ModName -> GhcSrc -> Bare.Env
-> GhcSpecRefl -> GhcSpecData -> GhcSpecSig -> GhcSpecQual -> BareRTEnv
-> Ms.BareSpec -> Ms.BareSpec
-----------------------------------------------------------------------------------------
-makeLiftedSpec name src _env refl sData sig qual myRTE lSpec0 = lSpec0
+makeLiftedSpec name src env refl sData sig qual myRTE lSpec0 = lSpec0
{ Ms.asmSigs = F.notracepp ("makeLiftedSpec : ASSUMED-SIGS " ++ F.showpp name ) (xbs ++ myDCs)
- , Ms.reflSigs = F.notracepp "REFL-SIGS" xbs
- , Ms.sigs = F.notracepp ("makeLiftedSpec : LIFTED-SIGS " ++ F.showpp name ) $ mkSigs (gsTySigs sig)
+ , Ms.reflSigs = F.notracepp "REFL-SIGS" $ map (first (fmap getLHNameSymbol)) xbs
+ , Ms.sigs = F.notracepp ("makeLiftedSpec : LIFTED-SIGS " ++ F.showpp name ) $
+ map (first (fmap getLHNameSymbol)) $ mkSigs (gsTySigs sig)
, Ms.invariants = [ (Bare.varLocSym <$> x, Bare.specToBare <$> t)
| (x, t) <- gsInvariants sData
, isLocInFile srcF t
@@ -1357,12 +1414,11 @@ makeLiftedSpec name src _env refl sData sig qual myRTE lSpec0 = lSpec0
, Ms.qualifiers = filter (isLocInFile srcF) (gsQualifiers qual)
}
where
- myDCs = [(x,t) | (x,t) <- mkSigs (gsCtors sData)
- , F.symbol name == fst (GM.splitModuleName $ val x)]
+ myDCs = filter (isLocalName . val . fst) $ mkSigs (gsCtors sData)
mkSigs xts = [ toBare (x, t) | (x, t) <- xts
, S.member x sigVars && isExportedVar (toTargetSrc src) x
]
- toBare (x, t) = (Bare.varLocSym x, Bare.specToBare <$> t)
+ toBare (x, t) = (makeGHCLHNameLocatedFromId x, Bare.specToBare <$> t)
xbs = toBare <$> reflTySigs
sigVars = S.difference defVars reflVars
defVars = S.fromList (_giDefVars src)
@@ -1371,6 +1427,12 @@ makeLiftedSpec name src _env refl sData sig qual myRTE lSpec0 = lSpec0
-- myAliases fld = M.elems . fld $ myRTE
srcF = _giTarget src
+ isLocalName = \case
+ LHNResolved (LHRGHC n) _ ->
+ Just (Ghc.tcg_mod (Bare.reTcGblEnv env)) == Ghc.nameModule_maybe n
+ _ ->
+ False
+
-- | Returns 'True' if the input determines a location within the input file. Due to the fact we might have
-- Haskell sources which have \"companion\" specs defined alongside them, we also need to account for this
-- case, by stripping out the extensions and check that the LHS is a Haskell source and the RHS a spec file.
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
index 82b590d836..c23077e4a9 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
@@ -29,6 +29,7 @@ import Data.Maybe
import Control.Monad
import Control.Monad.State
+import Data.Bifunctor (second)
import Data.Functor ((<&>))
import qualified Control.Exception as Ex
import qualified Data.HashMap.Strict as M
@@ -385,7 +386,7 @@ instance Expand a => Expand (M.HashMap k a) where
expandBareSpec :: BareRTEnv -> F.SourcePos -> Ms.BareSpec -> Ms.BareSpec
expandBareSpec rtEnv l sp = sp
{ measures = expand rtEnv l (measures sp)
- , asmSigs = expand rtEnv l (asmSigs sp)
+ , asmSigs = map (second (expand rtEnv l)) (asmSigs sp)
, sigs = expand rtEnv l (sigs sp)
, localSigs = expand rtEnv l (localSigs sp)
, reflSigs = expand rtEnv l (reflSigs sp)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
index 3e1791c8f1..f03225ec73 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
, lookupGhcDnTyCon
, lookupGhcTyCon
, lookupGhcVar
+ , lookupGhcIdLHName
, lookupGhcNamedVar
, matchTyCon
@@ -105,6 +106,7 @@ makeEnv :: Config -> Ghc.Session -> Ghc.TcGblEnv -> GhcSrc -> LogicMap -> [(ModN
makeEnv cfg session tcg src lmap specs = RE
{ reSession = session
, reTcGblEnv = tcg
+ , reUsedExternals = usedExternals
, reLMap = lmap
, reSyms = syms
, _reSubst = makeVarSubst src
@@ -120,6 +122,8 @@ makeEnv cfg session tcg src lmap specs = RE
globalSyms = concatMap getGlobalSyms specs
syms = [ (F.symbol v, v) | v <- vars ]
vars = srcVars src
+ usedExternals = Ghc.exprsOrphNames $ map snd $ Ghc.flattenBinds $ _giCbs src
+
getGlobalSyms :: (ModName, BareSpec) -> [F.Symbol]
getGlobalSyms (_, spec)
@@ -562,6 +566,14 @@ lookupGhcDataConLHName env lname = do
_ -> panic
(Just $ GM.fSrcSpan lname) $ "not a data constructor: " ++ show (val lname)
+lookupGhcIdLHName :: HasCallStack => Env -> Located LHName -> Lookup Ghc.Id
+lookupGhcIdLHName env lname = do
+ case lookupTyThing env lname of
+ Ghc.AConLike (Ghc.RealDataCon d) -> Right (Ghc.dataConWorkId d)
+ Ghc.AnId x -> Right x
+ _ -> panic
+ (Just $ GM.fSrcSpan lname) $ "not a variable of data constructor: " ++ show (val lname)
+
-------------------------------------------------------------------------------
-- | Checking existence of names
-------------------------------------------------------------------------------
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Types.hs
index dd19035b38..8a2aa25463 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Types.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Types.hs
@@ -72,6 +72,7 @@ plugSrc _ = Nothing
data Env = RE
{ reSession :: Ghc.Session
, reTcGblEnv :: Ghc.TcGblEnv
+ , reUsedExternals :: Ghc.NameSet
, reLMap :: LogicMap
, reSyms :: [(F.Symbol, Ghc.Var)] -- ^ see "syms" in old makeGhcSpec'
, _reSubst :: F.Subst -- ^ see "su" in old makeGhcSpec'
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
index 1e575bbf62..c8696adce5 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
@@ -19,12 +19,15 @@ import Language.Haskell.Liquid.Types.Names
import Language.Haskell.Liquid.Types.RType
import Control.Monad.Writer
+import qualified Data.Char as Char
import Data.Data (Data, gmapT)
import Data.Generics (extT)
import qualified Data.HashSet as HS
import qualified Data.HashMap.Strict as HM
+import qualified Data.Text as Text
+import qualified GHC.Types.Name.Occurrence
import Language.Fixpoint.Types hiding (Error, panic)
import Language.Haskell.Liquid.Types.Errors (TError(ErrDupNames, ErrResolve), panic)
@@ -79,40 +82,40 @@ resolveLHNames taliases globalRdrEnv =
| 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
+ Nothing -> lookupGRELHName LHTcName lname s
+ LHNUnresolved LHVarName s
+ | isDataCon s -> lookupGRELHName LHDataConName lname s
+ | otherwise -> lookupGRELHName LHVarName lname s
+ LHNUnresolved ns s -> lookupGRELHName ns lname s
n@(LHNResolved (LHRLocal _) _) -> pure n
n ->
let sp = Just $ LH.sourcePosSrcSpan $ loc lname
in panic sp $ "resolveLHNames: Unexpected resolved name: " ++ show n
+ lookupGRELHName ns lname s =
+ case GHC.lookupGRE globalRdrEnv (mkLookupGRE ns 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 (nameSpaceKind ns) "Cannot resolve name" (s <$ lname)]
+ pure $ val lname
+
errResolve :: PJ.Doc -> String -> LocSymbol -> Error
errResolve k msg lx = ErrResolve (LH.fSrcSpan lx) k (pprint (val lx)) (PJ.text msg)
+ nameSpaceKind :: LHNameSpace -> PJ.Doc
+ nameSpaceKind = \case
+ LHTcName -> "type constructor"
+ LHDataConName -> "data constructor"
+ LHVarName -> "variable"
+
mkLookupGRE ns s =
let m = LH.takeModuleNames s
n = LH.dropModuleNames s
@@ -128,11 +131,22 @@ resolveLHNames taliases globalRdrEnv =
GHC.mkRdrUnqual oname
else
GHC.mkRdrQual (GHC.mkModuleName $ symbolString m) oname
- in GHC.LookupRdrName rdrn GHC.SameNameSpace
+ in GHC.LookupRdrName rdrn (mkWhichGREs ns)
+
+ mkWhichGREs :: LHNameSpace -> WhichGREs GHC.GREInfo
+ mkWhichGREs = \case
+ LHTcName -> GHC.SameNameSpace
+ LHDataConName -> GHC.SameNameSpace
+ LHVarName -> GHC.RelevantGREs
+ { GHC.includeFieldSelectors = GHC.WantNormal
+ , GHC.lookupVariablesForFields = True
+ , GHC.lookupTyConsAsWell = False
+ }
mkGHCNameSpace = \case
LHTcName -> GHC.tcName
LHDataConName -> GHC.dataName
+ LHVarName -> GHC.Types.Name.Occurrence.varName
tupleArity s =
let a = read $ drop 5 $ symbolString s
@@ -141,6 +155,10 @@ resolveLHNames taliases globalRdrEnv =
else
a
+ isDataCon s = case Text.uncons (Text.takeWhileEnd (/= '.') (symbolText s)) of
+ Just (c, _) -> Char.isUpper c || c == ':'
+ Nothing -> False
+
-- | Changes unresolved names to local resolved names in the body of type
-- aliases.
resolveBoundVarsInTypeAliases :: BareSpec -> BareSpec
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
index 8e0d3a2724..25fcaf1d14 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
@@ -832,7 +832,7 @@ type BPspec = Pspec LocBareType LocSymbol
-- | The AST for a single parsed spec.
data Pspec ty ctor
= Meas (Measure ty ctor) -- ^ 'measure' definition
- | Assm (LocSymbol, ty) -- ^ 'assume' signature (unchecked)
+ | Assm (Located LHName, ty) -- ^ 'assume' signature (unchecked)
| AssmReflect (LocSymbol, LocSymbol) -- ^ 'assume reflects' signature (unchecked)
| Asrt (LocSymbol, ty) -- ^ 'assert' signature (checked)
| LAsrt (LocSymbol, ty) -- ^ 'local' assertion -- TODO RJ: what is this
@@ -1108,7 +1108,7 @@ specP :: Parser BPspec
specP
= fallbackSpecP "assume" ((reserved "reflect" >> fmap AssmReflect assmReflectBindP)
<|> (reserved "relational" >> fmap AssmRel relationalP)
- <|> fmap Assm tyBindP )
+ <|> fmap Assm assumptionP )
<|> fallbackSpecP "assert" (fmap Asrt tyBindP )
<|> fallbackSpecP "autosize" (fmap ASize asizeP )
<|> (reserved "local" >> fmap LAsrt tyBindP )
@@ -1252,6 +1252,13 @@ tyBindP :: Parser (LocSymbol, Located BareType)
tyBindP =
(,) <$> locBinderP <* reservedOp "::" <*> located genBareTypeP
+assumptionP :: Parser (Located LHName, Located BareType)
+assumptionP = do
+ x <- locBinderP
+ _ <- reservedOp "::"
+ t <- located genBareTypeP
+ return (makeUnresolvedLHName LHVarName <$> x, t)
+
-- | Parses a loc symbol.
assmReflectBindP :: Parser (LocSymbol, LocSymbol)
assmReflectBindP =
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
index 8b6f8a15e7..ce572a1d8f 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
@@ -15,6 +15,7 @@ module Language.Haskell.Liquid.Types.Names
, getLHNameSymbol
, makeGHCLHName
, makeGHCLHNameLocated
+ , makeGHCLHNameLocatedFromId
, makeLocalLHName
, makeUnresolvedLHName
, mapLHNames
@@ -86,6 +87,7 @@ data LHName
data LHNameSpace
= LHTcName
| LHDataConName
+ | LHVarName
deriving (Data, Eq, Generic, Ord)
instance B.Binary LHNameSpace
@@ -165,6 +167,13 @@ makeGHCLHNameLocated :: (GHC.NamedThing a, Symbolic a) => a -> Located LHName
makeGHCLHNameLocated x =
makeGHCLHName (GHC.getName x) (symbol x) <$ locNamedThing x
+makeGHCLHNameLocatedFromId :: GHC.Id -> Located LHName
+makeGHCLHNameLocatedFromId x =
+ case GHC.idDetails x of
+ GHC.DataConWrapId dc -> makeGHCLHNameLocated (GHC.getName dc)
+ GHC.DataConWorkId dc -> makeGHCLHNameLocated (GHC.getName dc)
+ _ -> makeGHCLHNameLocated x
+
makeUnresolvedLHName :: LHNameSpace -> Symbol -> LHName
makeUnresolvedLHName = LHNUnresolved
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
index dd44b20a48..a66d3b9275 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
@@ -398,7 +398,7 @@ data Spec ty bndr = Spec
{ measures :: ![Measure ty bndr] -- ^ User-defined properties for ADTs
, impSigs :: ![(F.Symbol, F.Sort)] -- ^ Imported variables types
, expSigs :: ![(F.Symbol, F.Sort)] -- ^ Exported variables types
- , asmSigs :: ![(F.LocSymbol, ty)] -- ^ Assumed (unchecked) types; including reflected signatures
+ , asmSigs :: ![(F.Located LHName, ty)] -- ^ Assumed (unchecked) types; including reflected signatures
, asmReflectSigs :: ![(F.LocSymbol, F.LocSymbol)] -- ^ Assume reflects : left is the actual function and right the pretended one
, sigs :: ![(F.LocSymbol, ty)] -- ^ Imported functions and types
, localSigs :: ![(F.LocSymbol, ty)] -- ^ Local type signatures
@@ -588,7 +588,7 @@ data LiftedSpec = LiftedSpec
-- ^ Imported variables types
, liftedExpSigs :: HashSet (F.Symbol, F.Sort)
-- ^ Exported variables types
- , liftedAsmSigs :: HashSet (F.LocSymbol, LocBareType)
+ , liftedAsmSigs :: HashSet (F.Located LHName, LocBareType)
-- ^ Assumed (unchecked) types; including reflected signatures
, liftedAsmReflectSigs :: HashSet (F.LocSymbol, F.LocSymbol)
-- ^ Reflected assumed signatures
diff --git a/src/Data/ByteString/Char8_LHAssumptions.hs b/src/Data/ByteString/Char8_LHAssumptions.hs
index ddc288ade7..9cbeb6c3d8 100644
--- a/src/Data/ByteString/Char8_LHAssumptions.hs
+++ b/src/Data/ByteString/Char8_LHAssumptions.hs
@@ -277,11 +277,11 @@ assume Data.ByteString.Char8.unzip
, { r : ByteString | bslen r == len i }
)
-assume Data.ByteString.ReadInt.readInt
+assume readInt
:: i : ByteString
-> Maybe { p : (Int, { o : ByteString | bslen o < bslen i}) | bslen i /= 0 }
-assume Data.ByteString.ReadNat.readInteger
+assume readInteger
:: 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 175a5413dd..19d48054fe 100644
--- a/src/Data/ByteString/Lazy/Char8_LHAssumptions.hs
+++ b/src/Data/ByteString/Lazy/Char8_LHAssumptions.hs
@@ -246,11 +246,11 @@ assume Data.ByteString.Lazy.Char8.unzip
, { r : ByteString | bllen r == len i }
)
-assume Data.ByteString.Lazy.ReadInt.readInt
+assume readInt
:: i : ByteString
-> Maybe { p : (Int, { o : ByteString | bllen o < bllen i}) | bllen i /= 0 }
-assume Data.ByteString.Lazy.ReadNat.readInteger
+assume readInteger
:: 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 2eabdae61a..25a5e6f35b 100644
--- a/src/Data/ByteString/Lazy_LHAssumptions.hs
+++ b/src/Data/ByteString/Lazy_LHAssumptions.hs
@@ -16,32 +16,32 @@ invariant { bs : ByteString | 0 <= bllen bs }
invariant { bs : ByteString | bllen bs == stringlen bs }
-assume Data.ByteString.Lazy.empty :: { bs : ByteString | bllen bs == 0 }
+assume empty :: { bs : ByteString | bllen bs == 0 }
-assume Data.ByteString.Lazy.singleton
+assume singleton
:: _ -> { bs : ByteString | bllen bs == 1 }
-assume Data.ByteString.Lazy.pack
+assume pack
:: w8s : [_]
-> { bs : _ | bllen bs == len w8s }
-assume Data.ByteString.Lazy.unpack
+assume unpack
:: bs : ByteString
-> { w8s : [_] | len w8s == bllen bs }
-assume Data.ByteString.Lazy.Internal.fromStrict
+assume fromStrict
:: i : Data.ByteString.ByteString
-> { o : ByteString | bllen o == bslen i }
-assume Data.ByteString.Lazy.Internal.toStrict
+assume toStrict
:: i : ByteString
-> { o : Data.ByteString.ByteString | bslen o == bllen i }
-assume Data.ByteString.Lazy.fromChunks
+assume fromChunks
:: i : [Data.ByteString.ByteString]
-> { o : ByteString | len i == 0 <=> bllen o == 0 }
-assume Data.ByteString.Lazy.toChunks
+assume toChunks
:: i : ByteString
-> { os : [{ o : Data.ByteString.ByteString | bslen o <= bllen i}] | len os == 0 <=> bllen i == 0 }
diff --git a/src/Data/ByteString/Short_LHAssumptions.hs b/src/Data/ByteString/Short_LHAssumptions.hs
index 2b422e3b8e..bb495ba3d8 100644
--- a/src/Data/ByteString/Short_LHAssumptions.hs
+++ b/src/Data/ByteString/Short_LHAssumptions.hs
@@ -2,7 +2,7 @@
{-# OPTIONS_GHC -Wno-unused-imports #-}
module Data.ByteString.Short_LHAssumptions where
-import Data.ByteString
+import Data.ByteString (ByteString)
import Data.ByteString_LHAssumptions()
import Data.ByteString.Short
import Data.String_LHAssumptions()
@@ -15,19 +15,19 @@ invariant { bs : ShortByteString | 0 <= sbslen bs }
invariant { bs : ShortByteString | sbslen bs == stringlen bs }
-assume Data.ByteString.Short.Internal.toShort :: i : ByteString -> { o : ShortByteString | sbslen o == bslen i }
+assume toShort :: i : ByteString -> { o : ShortByteString | sbslen o == bslen i }
-assume Data.ByteString.Short.Internal.fromShort :: o : ShortByteString -> { i : ByteString | bslen i == sbslen o }
+assume fromShort :: o : ShortByteString -> { i : ByteString | bslen i == sbslen o }
-assume Data.ByteString.Short.Internal.pack :: w8s : [Word8] -> { bs : ShortByteString | sbslen bs == len w8s }
+assume pack :: w8s : [Word8] -> { bs : ShortByteString | sbslen bs == len w8s }
-assume Data.ByteString.Short.Internal.unpack :: bs : ShortByteString -> { w8s : [Word8] | len w8s == sbslen bs }
+assume unpack :: bs : ShortByteString -> { w8s : [Word8] | len w8s == sbslen bs }
-assume Data.ByteString.Short.Internal.empty :: { bs : ShortByteString | sbslen bs == 0 }
+assume empty :: { bs : ShortByteString | sbslen bs == 0 }
-assume Data.ByteString.Short.Internal.null :: bs : ShortByteString -> { b : Bool | b <=> sbslen bs == 0 }
+assume Data.ByteString.Short.null :: bs : ShortByteString -> { b : Bool | b <=> sbslen bs == 0 }
-assume Data.ByteString.Short.Internal.length :: bs : ShortByteString -> { n : Int | sbslen bs == n }
+assume Data.ByteString.Short.length :: bs : ShortByteString -> { n : Int | sbslen bs == n }
-assume Data.ByteString.Short.Internal.index :: bs : ShortByteString -> { n : Int | 0 <= n && n < sbslen bs } -> Word8
+assume index :: bs : ShortByteString -> { n : Int | 0 <= n && n < sbslen bs } -> Word8
@-}
diff --git a/src/Data/ByteString_LHAssumptions.hs b/src/Data/ByteString_LHAssumptions.hs
index b4cf68c186..99e85e3453 100644
--- a/src/Data/ByteString_LHAssumptions.hs
+++ b/src/Data/ByteString_LHAssumptions.hs
@@ -13,7 +13,7 @@ invariant { bs : ByteString | 0 <= bslen bs }
invariant { bs : ByteString | bslen bs == stringlen bs }
-assume Data.ByteString.Internal.Type.empty :: { bs : ByteString | bslen bs == 0 }
+assume empty :: { bs : ByteString | bslen bs == 0 }
assume Data.ByteString.singleton :: _ -> { bs : ByteString | bslen bs == 1 }
diff --git a/src/Data/Set_LHAssumptions.hs b/src/Data/Set_LHAssumptions.hs
index eb7e0103dc..c0a901bda9 100644
--- a/src/Data/Set_LHAssumptions.hs
+++ b/src/Data/Set_LHAssumptions.hs
@@ -4,6 +4,7 @@ module Data.Set_LHAssumptions where
import Data.Set
import GHC.Types_LHAssumptions()
+import Prelude hiding (null)
{-@
@@ -43,20 +44,20 @@ measure Set_sub :: (Set a) -> (Set a) -> Bool
// ---------------------------------------------------------------------------------------------
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 member :: Ord a => x:a -> xs:(Set a) -> {v:Bool | v <=> Set_mem x xs}
+assume null :: Ord a => xs:(Set a) -> {v:Bool | v <=> Set_emp xs}
-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 empty :: {v:(Set a) | Set_emp v}
+assume singleton :: x:a -> {v:(Set a) | v = (Set_sng x)}
+assume insert :: Ord a => x:a -> xs:(Set a) -> {v:(Set a) | v = Set_cup xs (Set_sng x)}
+assume delete :: (Ord a) => x:a -> xs:(Set a) -> {v:(Set a) | v = Set_dif xs (Set_sng x)}
-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 union :: Ord a => xs:(Set a) -> ys:(Set a) -> {v:(Set a) | v = Set_cup xs ys}
+assume intersection :: Ord a => xs:(Set a) -> ys:(Set a) -> {v:(Set a) | v = Set_cap xs ys}
+assume difference :: Ord a => xs:(Set a) -> ys:(Set a) -> {v:(Set a) | v = Set_dif xs ys}
-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}
+assume fromList :: Ord a => xs:[a] -> {v:Set a | v = listElts xs}
+assume toList :: Ord a => s:Set a -> {xs:[a] | s = listElts xs}
// ---------------------------------------------------------------------------------------------
// -- | The set of elements in a list ----------------------------------------------------------
diff --git a/src/Data/String_LHAssumptions.hs b/src/Data/String_LHAssumptions.hs
index 265e78b405..12796a1f90 100644
--- a/src/Data/String_LHAssumptions.hs
+++ b/src/Data/String_LHAssumptions.hs
@@ -8,7 +8,7 @@ import GHC.Types_LHAssumptions()
{-@
measure stringlen :: a -> Int
-assume GHC.Internal.Data.String.fromString
+assume fromString
:: forall a. IsString a
=> i : [Char]
-> { o : a | i ~~ o && len i == stringlen o }
diff --git a/src/Data/Tuple_LHAssumptions.hs b/src/Data/Tuple_LHAssumptions.hs
index c5c4ca8dee..0c6badf466 100644
--- a/src/Data/Tuple_LHAssumptions.hs
+++ b/src/Data/Tuple_LHAssumptions.hs
@@ -5,8 +5,8 @@ module Data.Tuple_LHAssumptions where
import Data.Tuple
{-@
-assume GHC.Internal.Data.Tuple.fst :: {f:(x:(a,b) -> {v:a | v = (fst x)}) | f == fst }
-assume GHC.Internal.Data.Tuple.snd :: {f:(x:(a,b) -> {v:b | v = (snd x)}) | f == snd }
+assume fst :: {f:(x:(a,b) -> {v:a | v = (fst x)}) | f == fst }
+assume snd :: {f:(x:(a,b) -> {v:b | v = (snd x)}) | f == snd }
measure fst :: (a, b) -> a
fst (a, b) = a
diff --git a/src/Foreign/Concurrent_LHAssumptions.hs b/src/Foreign/Concurrent_LHAssumptions.hs
index 7614bea88a..2f6196502e 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) -> IO () -> (IO (ForeignPtrN a (plen p)))
+assume 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 c61dbc9ebc..2dbc34c4f2 100644
--- a/src/Foreign/ForeignPtr_LHAssumptions.hs
+++ b/src/Foreign/ForeignPtr_LHAssumptions.hs
@@ -3,18 +3,17 @@
module Foreign.ForeignPtr_LHAssumptions where
import Foreign.Concurrent_LHAssumptions()
-import Foreign.Storable
+import Foreign.ForeignPtr
import GHC.ForeignPtr
-import GHC.Internal.Foreign.ForeignPtr.Imp
import GHC.ForeignPtr_LHAssumptions()
{-@
-assume GHC.Internal.ForeignPtr.withForeignPtr :: forall a b. fp:(ForeignPtr a)
+assume 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) -> (IO (ForeignPtrN a (plen p)))
+assume 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/Marshal/Alloc_LHAssumptions.hs b/src/Foreign/Marshal/Alloc_LHAssumptions.hs
index cd422c18c1..26584176e2 100644
--- a/src/Foreign/Marshal/Alloc_LHAssumptions.hs
+++ b/src/Foreign/Marshal/Alloc_LHAssumptions.hs
@@ -7,5 +7,5 @@ import GHC.Ptr_LHAssumptions()
import Foreign.Marshal.Alloc
{-@
-assume GHC.Internal.Foreign.Marshal.Alloc.allocaBytes :: n:Nat -> (PtrN a n -> IO b) -> IO b
+assume allocaBytes :: n:Nat -> (PtrN a n -> IO b) -> IO b
@-}
diff --git a/src/Foreign/Storable_LHAssumptions.hs b/src/Foreign/Storable_LHAssumptions.hs
index 6dc694660e..8b10d5de63 100644
--- a/src/Foreign/Storable_LHAssumptions.hs
+++ b/src/Foreign/Storable_LHAssumptions.hs
@@ -9,21 +9,21 @@ import GHC.Ptr
{-@
predicate PValid P N = ((0 <= N) && (N < (plen P)))
-assume GHC.Internal.Foreign.Storable.poke :: (Storable a)
+assume poke :: (Storable a)
=> {v: (Ptr a) | 0 < (plen v)}
-> a
-> (IO ())
-assume GHC.Internal.Foreign.Storable.peek :: (Storable a)
+assume peek :: (Storable a)
=> p:{v: (Ptr a) | 0 < (plen v)}
-> (IO {v:a | v = (deref p)})
-assume GHC.Internal.Foreign.Storable.peekByteOff :: (Storable a)
+assume peekByteOff :: (Storable a)
=> forall b. p:(Ptr b)
-> {v:Int | (PValid p v)}
-> (IO a)
-assume GHC.Internal.Foreign.Storable.pokeByteOff :: (Storable a)
+assume pokeByteOff :: (Storable a)
=> forall b. p:(Ptr b)
-> {v:Int | (PValid p v)}
-> a
diff --git a/src/GHC/Classes_LHAssumptions.hs b/src/GHC/Classes_LHAssumptions.hs
index e721ae7b0a..a1e16038ad 100644
--- a/src/GHC/Classes_LHAssumptions.hs
+++ b/src/GHC/Classes_LHAssumptions.hs
@@ -2,35 +2,34 @@
{-# OPTIONS_GHC -Wno-unused-imports #-}
module GHC.Classes_LHAssumptions where
-import GHC.Classes
import GHC.Types_LHAssumptions()
{-@
-assume GHC.Classes.not :: x:Bool -> {v:Bool | ((v) <=> ~(x))}
-assume (GHC.Classes.&&) :: x:Bool -> y:Bool
+assume not :: x:Bool -> {v:Bool | ((v) <=> ~(x))}
+assume && :: x:Bool -> y:Bool
-> {v:Bool | ((v) <=> ((x) && (y)))}
-assume (GHC.Classes.||) :: x:Bool -> y:Bool
+assume || :: x:Bool -> y:Bool
-> {v:Bool | ((v) <=> ((x) || (y)))}
-assume (GHC.Classes.==) :: (Eq a) => x:a -> y:a
+assume == :: (Eq a) => x:a -> y:a
-> {v:Bool | ((v) <=> x = y)}
-assume (GHC.Classes./=) :: (Eq a) => x:a -> y:a
+assume /= :: (Eq a) => x:a -> y:a
-> {v:Bool | ((v) <=> x != y)}
-assume (GHC.Classes.>) :: (Ord a) => x:a -> y:a
+assume > :: (Ord a) => x:a -> y:a
-> {v:Bool | ((v) <=> x > y)}
-assume (GHC.Classes.>=) :: (Ord a) => x:a -> y:a
+assume >= :: (Ord a) => x:a -> y:a
-> {v:Bool | ((v) <=> x >= y)}
-assume (GHC.Classes.<) :: (Ord a) => x:a -> y:a
+assume < :: (Ord a) => x:a -> y:a
-> {v:Bool | ((v) <=> x < y)}
-assume (GHC.Classes.<=) :: (Ord a) => x:a -> y:a
+assume <= :: (Ord a) => x:a -> y:a
-> {v:Bool | ((v) <=> x <= y)}
-assume GHC.Classes.compare :: (Ord a) => x:a -> y:a
+assume 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 :: (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) }
+assume max :: (Ord a) => x:a -> y:a -> {v:a | v = (if x > y then x else y) }
+assume min :: (Ord a) => x:a -> y:a -> {v:a | v = (if x < y then x else y) }
@-}
diff --git a/src/GHC/ForeignPtr_LHAssumptions.hs b/src/GHC/ForeignPtr_LHAssumptions.hs
index 477a1fbf6f..c68bc05c39 100644
--- a/src/GHC/ForeignPtr_LHAssumptions.hs
+++ b/src/GHC/ForeignPtr_LHAssumptions.hs
@@ -12,6 +12,6 @@ measure fplen :: ForeignPtr a -> Int
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:(Ptr a) -> (IO (ForeignPtrN a (plen p)))
-assume GHC.Internal.ForeignPtr.mallocPlainForeignPtrBytes :: n:{v:Int | v >= 0 } -> (IO (ForeignPtrN a n))
+assume newForeignPtr_ :: p:(Ptr a) -> (IO (ForeignPtrN a (plen p)))
+assume 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 1cb77ea8b7..6e52b3f84f 100644
--- a/src/GHC/IO/Handle_LHAssumptions.hs
+++ b/src/GHC/IO/Handle_LHAssumptions.hs
@@ -7,12 +7,12 @@ import GHC.Ptr
import GHC.Types_LHAssumptions()
{-@
-assume GHC.Internal.IO.Handle.Text.hGetBuf :: Handle -> Ptr a -> n:Nat
+assume hGetBuf :: Handle -> Ptr a -> n:Nat
-> (IO {v:Nat | v <= n})
-assume GHC.Internal.IO.Handle.Text.hGetBufNonBlocking :: Handle -> Ptr a -> n:Nat
+assume hGetBufNonBlocking :: Handle -> Ptr a -> n:Nat
-> (IO {v:Nat | v <= n})
-assume GHC.Internal.IO.Handle.hFileSize :: Handle
+assume hFileSize :: Handle
-> (IO {v:Integer | v >= 0})
@-}
diff --git a/src/GHC/Internal/Base_LHAssumptions.hs b/src/GHC/Internal/Base_LHAssumptions.hs
index 6ef2577353..fb8bbe4ebc 100644
--- a/src/GHC/Internal/Base_LHAssumptions.hs
+++ b/src/GHC/Internal/Base_LHAssumptions.hs
@@ -2,15 +2,15 @@
{-# OPTIONS_GHC -Wno-unused-imports #-}
module GHC.Internal.Base_LHAssumptions where
+import GHC.Base (assert)
import GHC.CString_LHAssumptions()
import GHC.Exts_LHAssumptions()
import GHC.Types_LHAssumptions()
-import GHC.Internal.Base
import Data.Tuple_LHAssumptions()
{-@
-assume GHC.Internal.Base.. :: forall c -> Bool, q :: a -> b -> Bool, r :: a -> c -> Bool>.
+assume . :: forall
c -> Bool, q :: a -> b -> Bool, r :: a -> c -> Bool>.
{xcmp::a, wcmp::b |- c <: c}
(ycmp:b -> c)
-> (zcmp:a -> b)
@@ -19,18 +19,18 @@ assume GHC.Internal.Base.. :: forall c -> Bool, q :: a -> b -> Bool,
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
+assume assert :: {v:Bool | v } -> a -> a
instance measure len :: forall a. [a] -> Int
len [] = 0
len (y:ys) = 1 + len ys
invariant {v: [a] | len v >= 0 }
-assume GHC.Internal.Base.map :: (a -> b) -> xs:[a] -> {v: [b] | len v == len xs}
-assume GHC.Internal.Base.++ :: xs:[a] -> ys:[a] -> {v:[a] | len v == len xs + len ys}
+assume map :: (a -> b) -> xs:[a] -> {v: [b] | len v == len xs}
+assume ++ :: xs:[a] -> ys:[a] -> {v:[a] | len v == len xs + len ys}
-assume (GHC.Internal.Base.$) :: (a -> b) -> a -> b
-assume GHC.Internal.Base.id :: x:a -> {v:a | v = x}
+assume $ :: (a -> b) -> a -> b
+assume id :: x:a -> {v:a | v = x}
qualif IsEmp(v:Bool, xs: [a]) : (v <=> (len xs > 0))
qualif IsEmp(v:Bool, xs: [a]) : (v <=> (len xs = 0))
diff --git a/src/GHC/Internal/List_LHAssumptions.hs b/src/GHC/Internal/List_LHAssumptions.hs
index d9dbef3fa0..c3fb5fc466 100644
--- a/src/GHC/Internal/List_LHAssumptions.hs
+++ b/src/GHC/Internal/List_LHAssumptions.hs
@@ -4,67 +4,67 @@ module GHC.Internal.List_LHAssumptions where
import GHC.Internal.List
import GHC.Types_LHAssumptions()
+import Prelude hiding (foldr1, length, null)
{-@
-
-assume GHC.Internal.List.head :: xs:{v: [a] | len v > 0} -> {v:a | v = head xs}
-assume GHC.Internal.List.tail :: xs:{v: [a] | len v > 0} -> {v: [a] | len(v) = (len(xs) - 1) && v = tail xs}
-
-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: 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
-assume GHC.Internal.List.scanr :: (a -> b -> b) -> b -> xs:[a] -> {v: [b] | len(v) = 1 + len(xs) }
-assume GHC.Internal.List.scanr1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) }
+assume head :: xs:{v: [a] | len v > 0} -> {v:a | v = head xs}
+assume tail :: xs:{v: [a] | len v > 0} -> {v: [a] | len(v) = (len(xs) - 1) && v = tail xs}
+
+assume last :: xs:{v: [a] | len v > 0} -> a
+assume init :: xs:{v: [a] | len v > 0} -> {v: [a] | len(v) = len(xs) - 1}
+assume null :: xs:[a] -> {v: Bool | ((v) <=> len(xs) = 0) }
+assume length :: xs:[a] -> {v: Int | v = len(xs)}
+assume filter :: (a -> Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)}
+assume scanl :: (a -> b -> a) -> a -> xs:[b] -> {v: [a] | len(v) = 1 + len(xs) }
+assume scanl1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) }
+assume foldr1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> a
+assume scanr :: (a -> b -> b) -> b -> xs:[a] -> {v: [b] | len(v) = 1 + len(xs) }
+assume scanr1 :: (a -> a -> a) -> xs:{v: [a] | len(v) > 0} -> {v: [a] | len(v) = len(xs) }
lazy GHC.Internal.List.iterate
-assume GHC.Internal.List.iterate :: (a -> a) -> a -> [a]
+assume iterate :: (a -> a) -> a -> [a]
-assume GHC.Internal.List.repeat :: a -> [a]
+assume repeat :: a -> [a]
lazy GHC.Internal.List.repeat
-assume GHC.Internal.List.replicate :: n:Nat -> x:a -> {v: [{v:a | v = x}] | len(v) = n}
+assume replicate :: n:Nat -> x:a -> {v: [{v:a | v = x}] | len(v) = n}
-assume GHC.Internal.List.cycle :: {v: [a] | len(v) > 0 } -> [a]
+assume cycle :: {v: [a] | len(v) > 0 } -> [a]
lazy GHC.Internal.List.cycle
-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 takeWhile :: (a -> Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)}
+assume dropWhile :: (a -> Bool) -> xs:[a] -> {v: [a] | len(v) <= len(xs)}
-assume GHC.Internal.List.take :: n:Int
+assume 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:Int
+assume 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 -> Bool)
+assume 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 span :: (a -> Bool)
-> xs:[a]
-> ({v:[a]|((len v)<=(len xs))}, {v:[a]|((len v)<=(len xs))})
-assume GHC.Internal.List.break :: (a -> Bool) -> xs:[a] -> ([a],[a])<{\x y -> (len xs) = (len x) + (len y)}>
+assume 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)}
+assume reverse :: xs:[a] -> {v: [a] | len(v) = len(xs)}
// Copy-pasted from len.hquals
qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) + len([ys]))
qualif LenSum(v:[a], xs:[b], ys:[c]): len([v]) = (len([xs]) - len([ys]))
-assume GHC.Internal.List.!! :: xs:[a] -> {v: _ | ((0 <= v) && (v < len(xs)))} -> a
+assume !! :: xs:[a] -> {v: _ | ((0 <= v) && (v < len(xs)))} -> a
-assume GHC.Internal.List.zip :: xs : [a] -> ys:[b]
+assume zip :: xs : [a] -> ys:[b]
-> {v : [(a, b)] | ((((len v) <= (len xs)) && ((len v) <= (len ys)))
&& (((len xs) = (len ys)) => ((len v) = (len xs))) )}
-assume GHC.Internal.List.zipWith :: (a -> b -> c)
+assume zipWith :: (a -> b -> c)
-> xs : [a] -> ys:[b]
-> {v : [c] | (((len v) <= (len xs)) && ((len v) <= (len ys)))}
-assume GHC.Internal.List.errorEmptyList :: {v: _ | false} -> a
+assume errorEmptyList :: {v: _ | false} -> a
@-}
diff --git a/src/GHC/Real_LHAssumptions.hs b/src/GHC/Real_LHAssumptions.hs
index 0a8fed89b2..49901f66bd 100644
--- a/src/GHC/Real_LHAssumptions.hs
+++ b/src/GHC/Real_LHAssumptions.hs
@@ -9,9 +9,9 @@ import GHC.Internal.Real
import GHC.Types_LHAssumptions()
{-@
-assume (GHC.Internal.Real.^) :: x:a -> y:{n:b | n >= 0} -> {z:a | (y == 0 => z == 1) && ((x == 0 && y /= 0) <=> z == 0)}
+assume (^) :: x:a -> y:{n:b | n >= 0} -> {z:a | (y == 0 => z == 1) && ((x == 0 && y /= 0) <=> z == 0)}
-assume GHC.Internal.Real.fromIntegral :: x:a -> {v:b|v=x}
+assume fromIntegral :: x:a -> {v:b|v=x}
class (GHC.Internal.Num.Num a) => GHC.Internal.Real.Fractional a where
(GHC.Internal.Real./) :: x:a -> y:{v:a | v /= 0} -> {v:a | v == x / y}
diff --git a/src/GHC/Types_LHAssumptions.hs b/src/GHC/Types_LHAssumptions.hs
index 97389f2765..63582b1d4e 100644
--- a/src/GHC/Types_LHAssumptions.hs
+++ b/src/GHC/Types_LHAssumptions.hs
@@ -29,8 +29,8 @@ embed Addr# as Str
embed Integer as int
-assume GHC.Types.True :: {v:Bool | v }
-assume GHC.Types.False :: {v:Bool | (~ v) }
+assume True :: {v:Bool | v }
+assume 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) }
diff --git a/src/Liquid/Prelude/Totality_LHAssumptions.hs b/src/Liquid/Prelude/Totality_LHAssumptions.hs
index 30432212e9..7d8f446961 100644
--- a/src/Liquid/Prelude/Totality_LHAssumptions.hs
+++ b/src/Liquid/Prelude/Totality_LHAssumptions.hs
@@ -8,13 +8,13 @@ import GHC.Prim
{-@
measure totalityError :: a -> Bool
-assume GHC.Internal.Control.Exception.Base.patError :: {v:Addr# | totalityError "Pattern match(es) are non-exhaustive"} -> a
+assume patError :: {v:Addr# | totalityError "Pattern match(es) are non-exhaustive"} -> a
-assume GHC.Internal.Control.Exception.Base.recSelError :: {v:Addr# | totalityError "Use of partial record field selector"} -> a
+assume recSelError :: {v:Addr# | totalityError "Use of partial record field selector"} -> a
-assume GHC.Internal.Control.Exception.Base.nonExhaustiveGuardsError :: {v:Addr# | totalityError "Guards are non-exhaustive"} -> a
+assume nonExhaustiveGuardsError :: {v:Addr# | totalityError "Guards are non-exhaustive"} -> a
-assume GHC.Internal.Control.Exception.Base.noMethodBindingError :: {v:Addr# | totalityError "Missing method(s) on instance declaration"} -> a
+assume noMethodBindingError :: {v:Addr# | totalityError "Missing method(s) on instance declaration"} -> a
-assume GHC.Internal.Control.Exception.Base.recConError :: {v:Addr# | totalityError "Missing field in record construction"} -> a
+assume recConError :: {v:Addr# | totalityError "Missing field in record construction"} -> a
@-}
diff --git a/src/Prelude_LHAssumptions.hs b/src/Prelude_LHAssumptions.hs
index e833bd306e..66df98c70c 100644
--- a/src/Prelude_LHAssumptions.hs
+++ b/src/Prelude_LHAssumptions.hs
@@ -16,7 +16,7 @@ import Liquid.Prelude.Totality_LHAssumptions()
{-@
-assume GHC.Internal.Err.error :: {v:_ | false} -> a
+assume error :: {v:_ | false} -> a
predicate Max V X Y = if X > Y then V = X else V = Y
predicate Min V X Y = if X < Y then V = X else V = Y
diff --git a/tests/basic/neg/T2349.hs b/tests/basic/neg/T2349.hs
index 2c13b50f38..1781158efc 100644
--- a/tests/basic/neg/T2349.hs
+++ b/tests/basic/neg/T2349.hs
@@ -1,6 +1,6 @@
{-# LANGUAGE GADTs #-}
{-@ LIQUID "--expect-error-containing=is not a subtype of the required type
- VV : {VV##1465 : [GHC.Types.Int] | len VV##1465 == ?b + 1}" @-}
+ VV : {VV##1461 : [GHC.Types.Int] | len VV##1461 == ?b + 1}" @-}
{-@ LIQUID "--reflection" @-}
-- | Test that the refinement types produced for GADTs are
-- compatible with the Haskell types.
diff --git a/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString.hs b/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString.hs
index 8add95a245..ef443a4b77 100644
--- a/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString.hs
+++ b/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString.hs
@@ -2146,7 +2146,7 @@ hGetNonBlocking = hGet
-- As with 'hGet', the string representation in the file is assumed to
-- be ISO-8859-1.
-{-@ assume GHC.Internal.Foreign.Marshal.Alloc.reallocBytes :: p:(Ptr a) -> n:Nat -> (IO (PtrN a n)) @-}
+{-@ assume reallocBytes :: p:(Ptr a) -> n:Nat -> (IO (PtrN a n)) @-}
hGetContents :: Handle -> IO ByteString
hGetContents h = do
let start_size = 1024
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 d1ca98e450..b57b6074fe 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
@@ -655,7 +655,7 @@ transpose css = L.map (\ss -> Chunk (S.pack ss) Empty)
--TODO: make this fast
-- REBARE: somehow with GHC 8.4 importing Data.List actually ends up importing Data.OldList ...
-{-@ assume GHC.Internal.Data.OldList.transpose :: [[a]] -> [{v:[a] | len v > 0}] @-}
+{-@ assume L.transpose :: [[a]] -> [{v:[a] | len v > 0}] @-}
-- ---------------------------------------------------------------------
diff --git a/tests/pos/Comprehension.hs b/tests/pos/Comprehension.hs
index 3a5f0f9a3f..7de05a6f94 100644
--- a/tests/pos/Comprehension.hs
+++ b/tests/pos/Comprehension.hs
@@ -4,4 +4,4 @@ module Comprehension where
foo :: Int -> [Int]
foo n = [0 .. n]
-{-@ assume GHC.Internal.Enum.enumFromTo :: (Enum a) => lo:a -> hi:a -> [{v:a | lo <= v && v <= hi}] @-}
+{-@ assume enumFromTo :: (Enum a) => lo:a -> hi:a -> [{v:a | lo <= v && v <= hi}] @-}
diff --git a/tests/pos/Foo.hs b/tests/pos/Foo.hs
index e82e51aca1..ba31b1f767 100644
--- a/tests/pos/Foo.hs
+++ b/tests/pos/Foo.hs
@@ -2,4 +2,4 @@ module Foo where
bar = 0
-{-@ assume (GHC.Internal.Base.++) :: [a] -> [a] -> [a] @-}
+{-@ assume ++ :: [a] -> [a] -> [a] @-}