diff --git a/docs/mkDocs/docs/options.md b/docs/mkDocs/docs/options.md index f2fe15e4de..a8c96fb9fd 100644 --- a/docs/mkDocs/docs/options.md +++ b/docs/mkDocs/docs/options.md @@ -243,6 +243,18 @@ Opaque reflections: - GHC.Internal.Real.even ``` +If not reflecting `keepEvens`, the other functions can still be opaquely-reflected with the `opaque-reflect` +annotation. + +```Haskell +{-@ LIQUID "--reflection" @-} +{-@ LIQUID "--dump-opaque-reflections" @-} + +module OpaqueRefl06 where + +{-@ opaque-reflect even @-} +{-@ opaque-reflect filter @-} +``` Note: you can also reflect functions *away* from their definition, using interface files. For instance, you may do: @@ -267,10 +279,10 @@ not all functions can be reflected, for the same reasons as some of your own fun for instance). If the reflection of these happen to need the reflection of private variables inside those modules, you can also request their reflection -with another `reflect` annotation with the _fully-qualified_ name of the private variable to reflect, i.e. something like: +with a `private-reflect` annotation with the _fully-qualified_ name of the private variable to reflect, i.e. something like: ``` -{-@ reflect MyMod.privFn @-} +{-@ private-reflect MyMod.privFn @-} ``` Note: reflection of private variables only work if these variables occur in the definition of other variables that could already be reflected. diff --git a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs index 8314d7f729..caeae689a6 100644 --- a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs +++ b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs @@ -236,6 +236,7 @@ import GHC.Core as Ghc , Expr(App, Case, Cast, Coercion, Lam, Let, Lit, Tick, Type, Var) , Unfolding(CoreUnfolding, DFunUnfolding, uf_tmpl) , bindersOf + , bindersOfBinds , cmpAlt , collectArgs , collectBinders diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs index 5895e66f73..a0b001487a 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs @@ -22,7 +22,6 @@ module Language.Haskell.Liquid.Bare ( , saveLiftedSpec ) where -import Prelude hiding (error) import Control.Monad (forM, mplus, when) import qualified Control.Exception as Ex import qualified Data.Binary as B @@ -484,16 +483,22 @@ specTypeCons = foldRType tc [] tc acc _ = acc reflectedVars :: Ms.BareSpec -> [Ghc.CoreBind] -> [Ghc.Var] -reflectedVars spec cbs = fst <$> xDefs +reflectedVars spec cbs = + filter + (isReflSym . makeGHCLHNameLocatedFromId) + (Ghc.bindersOfBinds cbs) where - xDefs = Mb.mapMaybe (`GM.findVarDef` cbs) reflSyms - reflSyms = val <$> S.toList (Ms.reflects spec) + isReflSym x = + S.member x (Ms.reflects spec) || + S.member (fmap getLHNameSymbol x) (Ms.privateReflects spec) measureVars :: Ms.BareSpec -> [Ghc.CoreBind] -> [Ghc.Var] -measureVars spec cbs = fst <$> xDefs +measureVars spec cbs = + filter + ((`S.member` measureSyms) . makeGHCLHNameLocatedFromId) + (Ghc.bindersOfBinds cbs) where - xDefs = Mb.mapMaybe (`GM.findVarDef` cbs) measureSyms - measureSyms = val <$> S.toList (Ms.hmeas spec) + measureSyms = Ms.hmeas spec ------------------------------------------------------------------------------------------ makeSpecVars :: Config -> GhcSrc -> Ms.BareSpec -> Bare.Env -> Bare.MeasEnv @@ -701,9 +706,12 @@ makeSpecRefl cfg src specs env name sig tycEnv = do case anyNonReflFn of Just (actSym , preSym) -> let preSym' = show (val preSym) in - let errorMsg = preSym' ++ " must be reflected first using {-@ reflect " ++ preSym' ++ " @-}" in - let error = ErrHMeas (GM.sourcePosSrcSpan $ loc actSym) (pprint $ val actSym) (text errorMsg) :: Error - in Ex.throw error + let errorMsg = preSym' ++ " must be reflected first using {-@ reflect " ++ preSym' ++ " @-}" + in Ex.throw + (ErrHMeas + (GM.sourcePosSrcSpan $ loc actSym) + (pprint $ val actSym) + (text errorMsg) :: Error) Nothing -> return SpRefl { gsLogicMap = lmap , gsAutoInst = autoInst @@ -721,7 +729,9 @@ makeSpecRefl cfg src specs env name sig tycEnv = do rflLocSyms = Bare.getLocReflects (Just env) specs rflSyms = S.map val rflLocSyms lmap = Bare.reLMap env - notInReflOnes (_, a) = not $ a `S.member` Ms.reflects mySpec + notInReflOnes (_, a) = not $ + a `S.member` Ms.reflects mySpec || + fmap getLHNameSymbol a `S.member` Ms.privateReflects mySpec anyNonReflFn = L.find notInReflOnes (Ms.asmReflectSigs mySpec) isReflectVar :: S.HashSet F.Symbol -> Ghc.Var -> Bool @@ -820,13 +830,9 @@ makeSpecSig cfg name mySpec specs env sigEnv tycEnv measEnv cbs = do (instances, dicts) = Bare.makeSpecDictionaries env sigEnv (name, mySpec) (M.toList specs) allSpecs = (name, mySpec) : M.toList specs rtEnv = Bare.sigRTEnv sigEnv - getVar sym = case Bare.lookupGhcVar env name "assume-reflection specs" sym of + getVar sym = case Bare.lookupGhcIdLHName env sym of Right x -> x - Left _ -> Ex.throw $ mkError sym $ "Not in scope: " ++ show (val sym) - - mkError :: LocSymbol -> String -> Error - mkError x str = ErrHMeas (GM.sourcePosSrcSpan $ loc x) (pprint $ val x) (text str) - -- hmeas = makeHMeas env allSpecs + Left _ -> panic (Just $ GM.fSrcSpan sym) "function to reflect not in scope" strengthenSigs :: [(Ghc.Var, (Int, LocSpecType))] ->[(Ghc.Var, LocSpecType)] strengthenSigs sigs = go <$> Misc.groupList sigs @@ -842,12 +848,17 @@ makeMthSigs measEnv = [ (v, t) | (_, v, t) <- Bare.meMethods measEnv ] makeInlSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)] makeInlSigs env rtEnv = makeLiftedSigs rtEnv (CoreToLogic.inlineSpecType (typeclass (getConfig env))) - . makeFromSet "hinlines" Ms.inlines env + . concatMap (map (lookupFunctionId env) . S.toList . Ms.inlines . snd) makeMsrSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)] makeMsrSigs env rtEnv = makeLiftedSigs rtEnv (CoreToLogic.inlineSpecType (typeclass (getConfig env))) - . makeFromSet "hmeas" Ms.hmeas env + . concatMap (map (lookupFunctionId env) . S.toList . Ms.hmeas . snd) + +lookupFunctionId :: Bare.Env -> Located LHName -> Ghc.Id +lookupFunctionId env x = + either (panic (Just $ GM.fSrcSpan x) "function not found") id $ + Bare.lookupGhcIdLHName env x makeLiftedSigs :: BareRTEnv -> (Ghc.Var -> SpecType) -> [Ghc.Var] -> [(Ghc.Var, LocSpecType)] makeLiftedSigs rtEnv f xs @@ -858,12 +869,6 @@ makeLiftedSigs rtEnv f xs where expand = Bare.specExpandType rtEnv -makeFromSet :: String -> (Ms.BareSpec -> S.HashSet LocSymbol) -> Bare.Env -> [(ModName, Ms.BareSpec)] - -> [Ghc.Var] -makeFromSet msg f env specs = concat [ mk n xs | (n, s) <- specs, let xs = S.toList (f s)] - where - mk name = Mb.mapMaybe (Bare.maybeResolveSym env name msg) - makeTySigs :: Bare.Env -> Bare.SigEnv -> ModName -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, LocSpecType, Maybe [Located F.Expr])] makeTySigs env sigEnv name spec = do @@ -1118,18 +1123,12 @@ makeMeasureInvariants :: Bare.Env -> ModName -> GhcSpecSig -> Ms.BareSpec makeMeasureInvariants env name sig mySpec = Mb.catMaybes <$> unzip (measureTypeToInv env name <$> [(x, (y, ty)) | x <- xs, (y, ty) <- sigs - , isSymbolOfVar (val x) y ]) + , x == makeGHCLHNameLocatedFromId y ]) where sigs = gsTySigs sig xs = S.toList (Ms.hmeas mySpec) -isSymbolOfVar :: Symbol -> Ghc.Var -> Bool -isSymbolOfVar x v = x == symbol' v - where - symbol' :: Ghc.Var -> Symbol - symbol' = GM.dropModuleNames . symbol . Ghc.getName - -measureTypeToInv :: Bare.Env -> ModName -> (LocSymbol, (Ghc.Var, LocSpecType)) -> ((Maybe Ghc.Var, LocSpecType), Maybe UnSortedExpr) +measureTypeToInv :: Bare.Env -> ModName -> (Located LHName, (Ghc.Var, LocSpecType)) -> ((Maybe Ghc.Var, LocSpecType), Maybe UnSortedExpr) measureTypeToInv env name (x, (v, t)) = notracepp "measureTypeToInv" ((Just v, t {val = Bare.qualifyTop env name (F.loc x) mtype}), usorted) where @@ -1139,7 +1138,11 @@ measureTypeToInv env name (x, (v, t)) res = ty_res trep z = last args tz = last rts - usorted = if isSimpleADT tz then Nothing else first (:[]) <$> mkReft (dummyLoc $ F.symbol v) z tz res + usorted = + if isSimpleADT tz then + Nothing + else + first (:[]) <$> mkReft (dummyLoc $ val $ makeGHCLHNameLocatedFromId v) z tz res mtype | null rts = uError $ ErrHMeas (GM.sourcePosSrcSpan $ loc t) (pprint x) "Measure has no arguments!" @@ -1148,18 +1151,18 @@ measureTypeToInv env name (x, (v, t)) isSimpleADT (RApp _ ts _ _) = all isRVar ts isSimpleADT _ = False -mkInvariant :: LocSymbol -> Symbol -> SpecType -> SpecType -> SpecType +mkInvariant :: Located LHName -> Symbol -> SpecType -> SpecType -> SpecType mkInvariant x z t tr = strengthen (top <$> t) (MkUReft reft' mempty) where reft' = Mb.maybe mempty Reft mreft mreft = mkReft x z t tr -mkReft :: LocSymbol -> Symbol -> SpecType -> SpecType -> Maybe (Symbol, Expr) +mkReft :: Located LHName -> Symbol -> SpecType -> SpecType -> Maybe (Symbol, Expr) mkReft x z _t tr | Just q <- stripRTypeBase tr = let Reft (v, p) = toReft q - su = mkSubst [(v, mkEApp x [EVar v]), (z,EVar v)] + su = mkSubst [(v, mkEApp (fmap getLHNameSymbol x) [EVar v]), (z,EVar v)] -- p' = pAnd $ filter (\e -> z `notElem` syms e) $ conjuncts p in Just (v, subst su p) mkReft _ _ _ _ @@ -1317,10 +1320,13 @@ addOpaqueReflMeas cfg tycEnv env spec measEnv specs eqs = do -- could have duplicates -- We skip the variables from the axiom equations that correspond to the actual functions -- of opaque reflections, since we never need to look at the unfoldings of those - qualifySym l = Bare.qualifyTop env name (loc l) (val l) - actualFns = S.fromList $ qualifySym . fst <$> Ms.asmReflectSigs spec + actualFns = S.fromList $ val . fst <$> Ms.asmReflectSigs spec shouldBeUsedForScanning sym = not (sym `S.member` actualFns) - varsUsedForTcScanning = L.filter (shouldBeUsedForScanning . symbol) $ fst3 <$> eqs + varsUsedForTcScanning = + [ v + | (v, _, _) <- eqs + , shouldBeUsedForScanning $ makeGHCLHName (Ghc.getName v) (symbol v) + ] tcs = S.toList $ Ghc.dataConTyCon `S.map` Bare.getReflDCs measEnv varsUsedForTcScanning dataDecls = Bare.makeHaskellDataDecls cfg name spec tcs tyi = Bare.tcTyConMap tycEnv diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs index 51ff203e81..0a50afcb68 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs @@ -40,7 +40,6 @@ import Language.Haskell.Liquid.Bare.Types as Bare import Language.Haskell.Liquid.Bare.Measure as Bare import Language.Haskell.Liquid.UX.Config import qualified Data.List as L -import Language.Haskell.Liquid.Misc (fst4) import Control.Applicative import Data.Function (on) import qualified Data.Map as Map @@ -68,7 +67,7 @@ makeHaskellAxioms :: Config -> GhcSrc -> Bare.Env -> Bare.TycEnv -> ModName -> L ----------------------------------------------------------------------------------------------- makeHaskellAxioms cfg src env tycEnv name lmap spSig spec = do wiDefs <- wiredDefs cfg env name spSig - let refDefs = getReflectDefs src spSig spec env name + let refDefs = getReflectDefs src spSig spec env return (makeAxiom env tycEnv name lmap <$> (wiDefs ++ refDefs)) ----------------------------------------------------------------------------------------------- @@ -85,13 +84,15 @@ makeAssumeReflectAxioms :: GhcSrc -> Bare.Env -> Bare.TycEnv -> ModName -> GhcSp makeAssumeReflectAxioms src env tycEnv name spSig spec = do -- Send an error message if we're redefining a reflection case findDuplicatePair val reflActSymbols <|> findDuplicateBetweenLists val refSymbols reflActSymbols of - Just (x , y) -> Ex.throw $ mkError y $ "Duplicate reflection of " ++ show x ++ " and " ++ show y + Just (x , y) -> Ex.throw $ mkError y $ + "Duplicate reflection of " ++ show x ++ " and " ++ show y Nothing -> return $ turnIntoAxiom <$> Ms.asmReflectSigs spec where turnIntoAxiom (actual, pretended) = makeAssumeReflectAxiom spSig env embs name (actual, pretended) - refDefs = getReflectDefs src spSig spec env name + refDefs = getReflectDefs src spSig spec env embs = Bare.tcEmbs tycEnv - refSymbols = fst4 <$> refDefs + refSymbols = + (\(x, _, v, _) -> F.atLoc x $ makeGHCLHName (Ghc.getName v) (F.symbol v)) <$> refDefs reflActSymbols = fst <$> Ms.asmReflectSigs spec ----------------------------------------------------------------------------------------------- @@ -99,7 +100,7 @@ makeAssumeReflectAxioms src env tycEnv name spSig spec = do -- `makeAssumeReflectAxioms`. Can also be used to compute the updated SpecType of -- -- a type where we add the post-condition that actual and pretended are the same -- makeAssumeReflectAxiom :: GhcSpecSig -> Bare.Env -> F.TCEmb Ghc.TyCon -> ModName - -> (LocSymbol, LocSymbol) -- actual function and pretended function + -> (Located LHName, Located LHName) -- actual function and pretended function -> (Ghc.Var, LocSpecType, F.Equation) ----------------------------------------------------------------------------------------------- makeAssumeReflectAxiom sig env tce name (actual, pretended) = @@ -114,15 +115,15 @@ makeAssumeReflectAxiom sig env tce name (actual, pretended) = at = val $ strengthenSpecWithMeasure sig env actualV pretended{val=qPretended} -- Get the Ghc.Var's of the actual and pretended function names - actualV = case Bare.lookupGhcVar env name "assume-reflection" actual of + actualV = case Bare.lookupGhcIdLHName env actual of Right x -> x - Left _ -> Ex.throw $ mkError actual $ "Not in scope: " ++ show (val actual) - pretendedV = case Bare.lookupGhcVar env name "assume-reflection" pretended of + Left _ -> panic (Just $ GM.fSrcSpan actual) "function to reflect not in scope" + pretendedV = case Bare.lookupGhcIdLHName env pretended of Right x -> x - Left _ -> Ex.throw $ mkError pretended $ "Not in scope: " ++ show (val pretended) + Left _ -> panic (Just $ GM.fSrcSpan pretended) "function to reflect not in scope" -- Get the qualified name symbols for the actual and pretended functions - qActual = Bare.qualifyTop env name (F.loc actual) (val actual) - qPretended = Bare.qualifyTop env name (F.loc pretended) (val pretended) + qActual = Bare.qualifyTop env name (F.loc actual) (getLHNameSymbol $ val actual) + qPretended = Bare.qualifyTop env name (F.loc pretended) (getLHNameSymbol $ val pretended) -- Get the GHC type of the actual and pretended functions actualTy = Ghc.varType actualV pretendedTy = Ghc.varType pretendedV @@ -173,14 +174,16 @@ strengthenSpecWithMeasure sig env actualV qPretended = -- -- Iterates until no new definition is found. In which case, we fail -- if there are still symbols left which we failed to find the source for. -getReflectDefs :: GhcSrc -> GhcSpecSig -> Ms.BareSpec -> Bare.Env -> ModName +getReflectDefs :: GhcSrc -> GhcSpecSig -> Ms.BareSpec -> Bare.Env -> [(LocSymbol, Maybe SpecType, Ghc.Var, Ghc.CoreExpr)] -getReflectDefs src sig spec env modName = +getReflectDefs src sig spec env = searchInTransitiveClosure symsToResolve initialDefinedMap [] where sigs = gsTySigs sig - symsToResolve = S.toList (Ms.reflects spec) - cbs = _giCbs src + symsToResolve = + map Left (S.toList (Ms.reflects spec)) ++ + map Right (S.toList (Ms.privateReflects spec)) + cbs = Ghc.flattenBinds $ _giCbs src initialDefinedMap = M.empty -- First argument of the `searchInTransitiveClosure` function should always @@ -202,13 +205,13 @@ getReflectDefs src sig spec env modName = [] -> acc -- No one newly found but at least one symbol left - we throw -- an error - x:_ -> Ex.throw . mkError x $ + x:_ -> Ex.throw . either mkError mkError x $ "Not found in scope nor in the amongst these variables: " ++ foldr (\x1 acc1 -> acc1 ++ " , " ++ show x1) "" newFvMap else searchInTransitiveClosure newToResolve newFvMap newAcc where -- Try to get the definitions of the symbols that are left (`toResolve`) - resolvedSyms = findVarDefType cbs sigs env modName fvMap <$> toResolve + resolvedSyms = findVarDefType cbs sigs env fvMap <$> toResolve -- Collect the newly found definitions found = Mb.catMaybes resolvedSyms -- Add them to the accumulator @@ -231,9 +234,14 @@ getReflectDefs src sig spec env modName = getAllFreeVars = Ghc.exprSomeFreeVarsList (const True) +-- | Names for functions that need to be reflected +-- +-- > Left nameInScope | Right qualifiedPrivateName +type ToReflectName = Either (Located LHName) LocSymbol + -- Finds the definition of a variable in the given Core binds, or in the -- unfoldings of a Var. Used for reflection. Returns the same --- `LocSymbol` given as argument, the SpecType of this symbol, its corresponding +-- `LHName` given as argument, the SpecType of this symbol, its corresponding -- variable and definition (the `CoreExpr`). -- -- Takes as arguments: @@ -253,23 +261,33 @@ getReflectDefs src sig spec env modName = -- Errors can be raised whenever the symbol was found but the rest of the -- process failed (no unfoldings available, lifted functions not exported, -- etc.). -findVarDefType :: [Ghc.CoreBind] -> [(Ghc.Var, LocSpecType)] -> Bare.Env -> ModName - -> M.HashMap LocSymbol Ghc.Var -> LocSymbol +findVarDefType :: [(Ghc.Id, Ghc.CoreExpr)] -> [(Ghc.Var, LocSpecType)] -> Bare.Env + -> M.HashMap LocSymbol Ghc.Var -> ToReflectName -> Maybe (LocSymbol, Maybe SpecType, Ghc.Var, Ghc.CoreExpr) -findVarDefType cbs sigs env modName defs x = case findVarDefMethod (val x) cbs of +findVarDefType cbs sigs env _defs (Left x) = + case L.find ((val x ==) . makeGHCLHNameFromId . fst) cbs of -- YL: probably ok even without checking typeclass flag since user cannot -- manually reflect internal names Just (v, e) -> - if GM.isExternalId v || isMethod (F.symbol x) || isDictionary (F.symbol x) then - Just (x, val <$> lookup v sigs, v, e) - else - Ex.throw $ mkError x $ - "Lifted functions must be exported; please export " ++ show v + Just (fmap getLHNameSymbol x, val <$> lookup v sigs, v, e) Nothing -> do - var <- Bare.maybeResolveSym env modName "findVarDefType" qSym <|> - M.lookup qSym defs + let ecall = panic (Just $ GM.fSrcSpan x) "function to reflect not found" + var = either ecall id (Bare.lookupGhcIdLHName env x) + info = Ghc.idInfo var + unfolding = getExprFromUnfolding . Ghc.realUnfoldingInfo $ info + case unfolding of + Just e -> + Just (fmap getLHNameSymbol x, val <$> lookup var sigs, var, e) + _ -> + Ex.throw $ mkError x $ unwords + [ "Symbol exists but is not defined in the current file," + , "and no unfolding is available in the interface files" + ] + +findVarDefType _cbs sigs _env defs (Right x) = do + var <- M.lookup x defs let info = Ghc.idInfo var - let unfolding = getExpr . Ghc.realUnfoldingInfo $ info + let unfolding = getExprFromUnfolding . Ghc.realUnfoldingInfo $ info case unfolding of Just e -> Just (x, val <$> lookup var sigs, var, e) @@ -278,13 +296,10 @@ findVarDefType cbs sigs env modName defs x = case findVarDefMethod (val x) cbs o [ "Symbol exists but is not defined in the current file," , "and no unfolding is available in the interface files" ] - where - qSym = x {val = qualifySym x} - qualifySym l = Bare.qualifyTop env modName (loc l) (val l) - getExpr :: Ghc.Unfolding -> Maybe Ghc.CoreExpr - getExpr (Ghc.CoreUnfolding expr _ _ _ _) = Just expr - getExpr _ = Nothing +getExprFromUnfolding :: Ghc.Unfolding -> Maybe Ghc.CoreExpr +getExprFromUnfolding (Ghc.CoreUnfolding expr _ _ _ _) = Just expr +getExprFromUnfolding _ = Nothing -------------------------------------------------------------------------------- makeAxiom :: Bare.Env -> Bare.TycEnv -> ModName -> LogicMap @@ -300,7 +315,7 @@ makeAxiom env tycEnv name lmap (x, mbT, v, def) dm = Bare.tcDataConMap tycEnv allowTC = typeclass (getConfig env) -mkError :: LocSymbol -> String -> Error +mkError :: PPrint a => Located a -> String -> Error mkError x str = ErrHMeas (sourcePosSrcSpan $ loc x) (pprint $ val x) (PJ.text str) makeAssumeType diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs index ced489c01a..34b88f56f3 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs @@ -39,6 +39,7 @@ import Language.Haskell.Liquid.GHC.Play (getNonPositivesTyCon import Language.Haskell.Liquid.Misc (condNull, thd5) import Language.Haskell.Liquid.Types.DataDecl import Language.Haskell.Liquid.Types.Errors +import Language.Haskell.Liquid.Types.Names import Language.Haskell.Liquid.Types.PredType import Language.Haskell.Liquid.Types.PrettyPrint import Language.Haskell.Liquid.Types.RType @@ -92,9 +93,9 @@ checkBareSpec sp , S.fromList fields ] ] - inlines = Ms.inlines sp - hmeasures = Ms.hmeas sp - reflects = Ms.reflects sp + inlines = S.map (fmap getLHNameSymbol) (Ms.inlines sp) + hmeasures = S.map (fmap getLHNameSymbol) (Ms.hmeas sp) + reflects = S.map (fmap getLHNameSymbol) (Ms.reflects sp) measures = msName <$> Ms.measures sp fields = concatMap dataDeclFields (Ms.dataDecls sp) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs index f946def3eb..97931b4ea6 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs @@ -58,7 +58,7 @@ import qualified Language.Haskell.Liquid.Bare.DataType as Bare import qualified Language.Haskell.Liquid.Bare.ToBare as Bare import Language.Haskell.Liquid.UX.Config import Control.Monad (mapM) -import qualified GHC.List as L +import qualified Data.List as L -------------------------------------------------------------------------------- makeHaskellMeasures :: Bool -> GhcSrc -> Bare.TycEnv -> LogicMap -> Ms.BareSpec @@ -68,14 +68,17 @@ makeHaskellMeasures allowTC src tycEnv lmap spec = Bare.measureToBare <$> ms where ms = makeMeasureDefinition allowTC tycEnv lmap cbs <$> mSyms - cbs = nonRecCoreBinds (_giCbs src) + cbs = Ghc.flattenBinds (_giCbs src) mSyms = S.toList (Ms.hmeas spec) -makeMeasureDefinition :: Bool -> Bare.TycEnv -> LogicMap -> [Ghc.CoreBind] -> LocSymbol - -> Measure LocSpecType Ghc.DataCon +makeMeasureDefinition + :: Bool -> Bare.TycEnv -> LogicMap -> [(Ghc.Id, Ghc.CoreExpr)] -> Located LHName + -> Measure LocSpecType Ghc.DataCon makeMeasureDefinition allowTC tycEnv lmap cbs x = - case GM.findVarDef (val x) cbs of - Nothing -> Ex.throw $ errHMeas x "Cannot extract measure from haskell function" + case L.find ((x ==) . makeGHCLHNameLocatedFromId . fst) cbs of + Nothing -> + Ex.throw $ + errHMeas (fmap getLHNameSymbol x) "Cannot extract measure from haskell function" Just (v, cexp) -> Ms.mkM vx vinfo mdef MsLifted (makeUnSorted allowTC (Ghc.varType v) mdef) where vx = F.atLoc x (F.symbol v) @@ -125,14 +128,15 @@ makeHaskellInlines :: Bool -> GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.Bare makeHaskellInlines allowTC src embs lmap spec = makeMeasureInline allowTC embs lmap cbs <$> inls where - cbs = nonRecCoreBinds (_giCbs src) + cbs = Ghc.flattenBinds (_giCbs src) inls = S.toList (Ms.inlines spec) -makeMeasureInline :: Bool -> F.TCEmb Ghc.TyCon -> LogicMap -> [Ghc.CoreBind] -> LocSymbol - -> (LocSymbol, LMap) +makeMeasureInline + :: Bool -> F.TCEmb Ghc.TyCon -> LogicMap -> [(Ghc.Id, Ghc.CoreExpr)] -> Located LHName + -> (LocSymbol, LMap) makeMeasureInline allowTC embs lmap cbs x = - case GM.findVarDef (val x) cbs of - Nothing -> Ex.throw $ errHMeas x "Cannot inline haskell function" + case L.find ((val x ==) . makeGHCLHNameFromId . fst) cbs of + Nothing -> Ex.throw $ errHMeas (fmap getLHNameSymbol x) "Cannot inline haskell function" Just (v, defn) -> (vx, coreToFun' allowTC embs Nothing lmap vx v defn ok) where vx = F.atLoc x (F.symbol v) @@ -153,12 +157,6 @@ coreToFun' allowTC embs dmMb lmap x v defn ok = either Ex.throw ok act dm = Mb.fromMaybe mempty dmMb -nonRecCoreBinds :: [Ghc.CoreBind] -> [Ghc.CoreBind] -nonRecCoreBinds = concatMap go - where - go cb@(Ghc.NonRec _ _) = [cb] - go (Ghc.Rec xes) = [Ghc.NonRec x e | (x, e) <- xes] - ------------------------------------------------------------------------------- makeHaskellDataDecls :: Config -> ModName -> Ms.BareSpec -> [Ghc.TyCon] -> [DataDecl] @@ -378,10 +376,12 @@ getLocReflects mbEnv = S.unions . fmap (uncurry $ names mbEnv) . M.toList names (Just env) modName modSpec = Bare.qualifyLocSymbolTop env modName `S.map` unqualified modSpec names Nothing _ modSpec = unqualified modSpec unqualified modSpec = S.unions - [ Ms.reflects modSpec - , S.fromList (snd <$> Ms.asmReflectSigs modSpec) - , S.fromList (fst <$> Ms.asmReflectSigs modSpec) - , Ms.inlines modSpec, Ms.hmeas modSpec + [ S.map (fmap getLHNameSymbol) (Ms.reflects modSpec) + , Ms.privateReflects modSpec + , S.fromList (fmap getLHNameSymbol . snd <$> Ms.asmReflectSigs modSpec) + , S.fromList (fmap getLHNameSymbol . fst <$> Ms.asmReflectSigs modSpec) + , S.map (fmap getLHNameSymbol) (Ms.inlines modSpec) + , S.map (fmap getLHNameSymbol) (Ms.hmeas modSpec) ] -- Get all the symbols that are defined in the logic, based on the environment and the specs. @@ -437,11 +437,11 @@ makeOpaqueReflMeasures env measEnv specs eqs = where -- Get the set of variables for the requested opaque reflections requestedOpaqueRefl = S.unions - . fmap (uncurry (S.map . getVar) . second Ms.opaqueReflects) + . map (S.map getVar . Ms.opaqueReflects . snd) . M.toList $ specs - getVar name sym = case Bare.lookupGhcVar env name "opaque-reflection" sym of + getVar sym = case Bare.lookupGhcIdLHName env sym of Right x -> x - Left _ -> Ex.throw $ mkError sym $ "Not in scope: " ++ show (val sym) + Left _ -> panic (Just $ GM.fSrcSpan sym) "function to reflect not in scope" definedSymbols = getDefinedSymbolsInLogic env measEnv specs undefinedInLogic v = not (S.member (varLocSym v) definedSymbols) -- Variables to consider @@ -459,9 +459,6 @@ makeOpaqueReflMeasures env measEnv specs eqs = bmeas = M locSym bareType [] MsReflect [] smeas = M locSym (val specType) [] MsReflect [] -mkError :: LocSymbol -> String -> Error -mkError x str = ErrHMeas (GM.sourcePosSrcSpan $ loc x) (pprint $ val x) (text str) - getUnfoldingOfVar :: Ghc.Var -> Maybe Ghc.CoreExpr getUnfoldingOfVar = getExpr . Ghc.realUnfoldingInfo . Ghc.idInfo where diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Typeclass.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Typeclass.hs index 715eb71d65..586b53cd51 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Typeclass.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Typeclass.hs @@ -60,8 +60,8 @@ compileClasses src env (name, spec) rest = { dataDecls = clsDecls , reflects = F.notracepp "reflects " $ S.fromList ( fmap - ( fmap GM.dropModuleNames - . GM.namedLocSymbol + ( fmap (updateLHNameSymbol GM.dropModuleNames) + . makeGHCLHNameLocatedFromId . Ghc.instanceDFunId . fst ) @@ -87,7 +87,7 @@ compileClasses src env (name, spec) rest = merge sig v = case v of Nothing -> Just [sig] Just vs -> Just (sig : vs) - methods = [ GM.namedLocSymbol x | (_, xs) <- instmethods, x <- xs ] + methods = [ makeGHCLHNameLocatedFromId x | (_, xs) <- instmethods, x <- xs ] -- instance methods mkSymbol x diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs index ed86fcbe0b..f596c830e5 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs @@ -657,17 +657,6 @@ ignoreCoreBinds vs cbs go (Rec xes) = [Rec (filter ((`notElem` vs) . fst) xes)] -findVarDef :: Symbol -> [CoreBind] -> Maybe (Var, CoreExpr) -findVarDef sym cbs = case xCbs of - (NonRec v def : _ ) -> Just (v, def) - (Rec [(v, def)] : _ ) -> Just (v, def) - _ -> Nothing - where - xCbs = [ cb | cb <- concatMap unRec cbs, sym `elem` coreBindSymbols cb ] - unRec (Rec xes) = [NonRec x es | (x,es) <- xes] - unRec nonRec = [nonRec] - - findVarDefMethod :: Symbol -> [CoreBind] -> Maybe (Var, CoreExpr) findVarDefMethod sym cbs = case rcbs of diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs index 1df173b562..b1c25c03bd 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs @@ -837,7 +837,7 @@ type BPspec = Pspec LocBareType LocSymbol data Pspec ty ctor = Meas (Measure ty ctor) -- ^ 'measure' definition | Assm (Located LHName, ty) -- ^ 'assume' signature (unchecked) - | AssmReflect (LocSymbol, LocSymbol) -- ^ 'assume reflects' signature (unchecked) + | AssmReflect (Located LHName, Located LHName) -- ^ 'assume reflects' signature (unchecked) | Asrt (Located LHName, ty) -- ^ 'assert' signature (checked) | LAsrt (LocSymbol, ty) -- ^ 'local' assertion -- TODO RJ: what is this | Asrts ([Located LHName], (ty, Maybe [Located Expr])) -- ^ sym0, ..., symn :: ty / [m0,..., mn] @@ -859,13 +859,13 @@ data Pspec ty ctor | Rewrite (Located LHName) -- ^ 'rewrite' annotation, the binder generates a rewrite rule | Rewritewith (Located LHName, [Located LHName]) -- ^ 'rewritewith' annotation, the first binder is using the rewrite rules of the second list, | Insts (Located LHName) -- ^ 'auto-inst' or 'ple' annotation; use ple locally on binder - | HMeas LocSymbol -- ^ 'measure' annotation; lift Haskell binder as measure - | Reflect LocSymbol -- ^ 'reflect' annotation; reflect Haskell binder as function in logic - | OpaqueReflect LocSymbol -- ^ 'opaque-reflect' annotation - | Inline LocSymbol -- ^ 'inline' annotation; inline (non-recursive) binder as an alias + | HMeas (Located LHName) -- ^ 'measure' annotation; lift Haskell binder as measure + | Reflect (Located LHName) -- ^ 'reflect' annotation; reflect Haskell binder as function in logic + | PrivateReflect LocSymbol -- ^ 'private-reflect' annotation + | OpaqueReflect (Located LHName) -- ^ 'opaque-reflect' annotation + | Inline (Located LHName) -- ^ 'inline' annotation; inline (non-recursive) binder as an alias | Ignore (Located LHName) -- ^ 'ignore' annotation; skip all checks inside this binder | ASize (Located LHName) -- ^ 'autosize' annotation; automatically generate size metric for this type - | HBound LocSymbol -- ^ 'bound' annotation; lift Haskell binder as an abstract-refinement "bound" | PBound (Bound ty Expr) -- ^ 'bound' definition | Pragma (Located String) -- ^ 'LIQUID' pragma, used to save configuration options in source files | CMeas (Measure ty ()) -- ^ 'class measure' definition @@ -948,14 +948,14 @@ ppPspec k (HMeas lx) = "measure" <+> pprintTidy k (val lx) ppPspec k (Reflect lx) = "reflect" <+> pprintTidy k (val lx) +ppPspec k (PrivateReflect lx) + = "private-reflect" <+> pprintTidy k (val lx) ppPspec k (OpaqueReflect lx) = "opaque-reflect" <+> pprintTidy k (val lx) ppPspec k (Inline lx) = "inline" <+> pprintTidy k (val lx) ppPspec k (Ignore lx) = "ignore" <+> pprintTidy k (val lx) -ppPspec k (HBound lx) - = "bound" <+> pprintTidy k (val lx) ppPspec k (ASize lx) = "autosize" <+> pprintTidy k (val lx) ppPspec k (PBound bnd) @@ -1012,7 +1012,6 @@ ppPspec k (AssmRel (lxl, lxr, tl, tr, q, p)) -- show (Axiom _) = "Axiom" show (Reflect _) = "Reflect" show (HMeas _) = "HMeas" - show (HBound _) = "HBound" show (Inline _) = "Inline" show (Pragma _) = "Pragma" show (CMeas _) = "CMeas" @@ -1083,12 +1082,12 @@ mkSpec name xs = (name,) $ qualifySpec (symbol name) Measure.Spec , Measure.rewriteWith = M.fromList [s | Rewritewith s <- xs] , Measure.bounds = M.fromList [(bname i, i) | PBound i <- xs] , Measure.reflects = S.fromList [s | Reflect s <- xs] + , Measure.privateReflects = S.fromList [s | PrivateReflect s <- xs] , Measure.opaqueReflects = S.fromList [s | OpaqueReflect s <- xs] , Measure.hmeas = S.fromList [s | HMeas s <- xs] , Measure.inlines = S.fromList [s | Inline s <- xs] , Measure.ignores = S.fromList [s | Ignore s <- xs] , Measure.autosize = S.fromList [s | ASize s <- xs] - , Measure.hbounds = S.fromList [s | HBound s <- xs] , Measure.axeqs = [] } @@ -1103,20 +1102,20 @@ specP <|> (reserved "local" >> fmap LAsrt tyBindP ) -- TODO: These next two are synonyms, kill one - <|> fallbackSpecP "axiomatize" (fmap Reflect axiomP ) - <|> fallbackSpecP "reflect" (fmap Reflect axiomP ) - <|> (reserved "opaque-reflect" >> fmap OpaqueReflect axiomP ) + <|> fallbackSpecP "axiomatize" (fmap Reflect locBinderLHNameP) + <|> fallbackSpecP "reflect" (fmap Reflect locBinderLHNameP) + <|> (reserved "private-reflect" >> fmap PrivateReflect axiomP ) + <|> (reserved "opaque-reflect" >> fmap OpaqueReflect locBinderLHNameP ) <|> fallbackSpecP "measure" hmeasureP <|> (reserved "infixl" >> fmap BFix infixlP ) <|> (reserved "infixr" >> fmap BFix infixrP ) <|> (reserved "infix" >> fmap BFix infixP ) - <|> fallbackSpecP "inline" (fmap Inline inlineP ) + <|> fallbackSpecP "inline" (fmap Inline locBinderLHNameP) <|> fallbackSpecP "ignore" (fmap Ignore locBinderLHNameP) - <|> fallbackSpecP "bound" (fmap PBound boundP - <|> fmap HBound hboundP ) + <|> fallbackSpecP "bound" (fmap PBound boundP) <|> (reserved "class" >> ((reserved "measure" >> fmap CMeas cMeasureP ) <|> fmap Class classP )) @@ -1177,12 +1176,6 @@ rewriteWithP = (,) <$> locBinderLHNameP <*> brackets (sepBy1 locBinderLHNameP co axiomP :: Parser LocSymbol axiomP = locBinderP -hboundP :: Parser LocSymbol -hboundP = locBinderP - -inlineP :: Parser LocSymbol -inlineP = locBinderP - datavarianceP :: Parser (Located LHName, [Variance]) datavarianceP = liftM2 (,) (locUpperIdLHNameP LHTcName) (many varianceP) @@ -1217,9 +1210,9 @@ tyBindLHNameP = do return (x, t) -- | Parses a loc symbol. -assmReflectBindP :: Parser (LocSymbol, LocSymbol) +assmReflectBindP :: Parser (Located LHName, Located LHName) assmReflectBindP = - (,) <$> locBinderP <* reservedOp "as" <*> locBinderP + (,) <$> locBinderLHNameP <* reservedOp "as" <*> locBinderLHNameP termBareTypeP :: Parser (Located BareType, Maybe [Located Expr]) termBareTypeP = do @@ -1281,13 +1274,14 @@ rtAliasP f bodyP hmeasureP :: Parser BPspec hmeasureP = do setLayout - b <- locBinderP - (do reservedOp "::" - ty <- located genBareTypeP - popLayout >> popLayout - eqns <- block $ try $ measureDefP (rawBodyP <|> tyBodyP ty) - return (Meas $ Measure.mkM b ty eqns MsMeasure mempty)) - <|> (popLayout >> popLayout >> return (HMeas b)) + do b <- try (locBinderP <* reservedOp "::") + ty <- located genBareTypeP + popLayout >> popLayout + eqns <- block $ try $ measureDefP (rawBodyP <|> tyBodyP ty) + return (Meas $ Measure.mkM b ty eqns MsMeasure mempty) + <|> + do b <- locBinderLHNameP + popLayout >> popLayout >> return (HMeas b) measureP :: Parser (Measure (Located BareType) LocSymbol) measureP = do diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs index ce572a1d8f..3a0db200cd 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs @@ -14,6 +14,7 @@ module Language.Haskell.Liquid.Types.Names , getLHNameResolved , getLHNameSymbol , makeGHCLHName + , makeGHCLHNameFromId , makeGHCLHNameLocated , makeGHCLHNameLocatedFromId , makeLocalLHName @@ -82,7 +83,26 @@ data LHName -- unresolved names. LHNResolved !LHResolvedName !Symbol | LHNUnresolved !LHNameSpace !Symbol - deriving (Data, Eq, Generic, Ord) + deriving (Data, Generic) + +-- | An Eq instance that ignores the Symbol in resolved names +instance Eq LHName where + LHNResolved n0 _ == LHNResolved n1 _ = n0 == n1 + LHNUnresolved ns0 s0 == LHNUnresolved ns1 s1 = ns0 == ns1 && s0 == s1 + _ == _ = False + +-- | An Ord instance that ignores the Symbol in resolved names +instance Ord LHName where + compare (LHNResolved n0 _) (LHNResolved n1 _) = compare n0 n1 + compare (LHNUnresolved ns0 s0) (LHNUnresolved ns1 s1) = + compare (ns0, s0) (ns1, s1) + compare LHNResolved{} _ = LT + compare LHNUnresolved{} _ = GT + +-- | A Hashable instance that ignores the Symbol in resolved names +instance Hashable LHName where + hashWithSalt s (LHNResolved n _) = hashWithSalt s n + hashWithSalt s (LHNUnresolved ns sym) = s `hashWithSalt` ns `hashWithSalt` sym data LHNameSpace = LHTcName @@ -115,7 +135,6 @@ instance Hashable LHResolvedName where 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 @@ -160,6 +179,14 @@ makeResolvedLHName = LHNResolved makeGHCLHName :: GHC.Name -> Symbol -> LHName makeGHCLHName n s = makeResolvedLHName (LHRGHC n) s +makeGHCLHNameFromId :: GHC.Id -> LHName +makeGHCLHNameFromId x = + let n = case GHC.idDetails x of + GHC.DataConWrapId dc -> GHC.getName dc + GHC.DataConWorkId dc -> GHC.getName dc + _ -> GHC.getName x + in makeGHCLHName n (symbol n) + makeLocalLHName :: Symbol -> LHName makeLocalLHName s = LHNResolved (LHRLocal s) s diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs index 531ff5244c..6667321fc3 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs @@ -380,7 +380,7 @@ data Spec ty bndr = Spec { measures :: ![Measure ty bndr] -- ^ User-defined properties for ADTs , expSigs :: ![(F.Symbol, F.Sort)] -- ^ Exported logic symbols , 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 + , asmReflectSigs :: ![(F.Located LHName, F.Located LHName)] -- ^ Assume reflects : left is the actual function and right the pretended one , sigs :: ![(F.Located LHName, ty)] -- ^ Asserted spec signatures , invariants :: ![(Maybe F.LocSymbol, ty)] -- ^ Data type invariants; the Maybe is the generating measure , ialiases :: ![(ty, ty)] -- ^ Data type invariants to be checked @@ -395,13 +395,13 @@ data Spec ty bndr = Spec , rewrites :: !(S.HashSet (F.Located LHName)) -- ^ Theorems turned into rewrite rules , rewriteWith :: !(M.HashMap (F.Located LHName) [F.Located LHName]) -- ^ Definitions using rewrite rules , fails :: !(S.HashSet (F.Located LHName)) -- ^ These Functions should be unsafe - , reflects :: !(S.HashSet F.LocSymbol) -- ^ Binders to reflect - , opaqueReflects :: !(S.HashSet F.LocSymbol) -- ^ Binders to opaque-reflect + , reflects :: !(S.HashSet (F.Located LHName)) -- ^ Binders to reflect + , privateReflects :: !(S.HashSet F.LocSymbol) -- ^ Private binders to reflect + , opaqueReflects :: !(S.HashSet (F.Located LHName)) -- ^ Binders to opaque-reflect , autois :: !(S.HashSet (F.Located LHName)) -- ^ Automatically instantiate axioms in these Functions - , hmeas :: !(S.HashSet F.LocSymbol) -- ^ Binders to turn into measures using haskell definitions - , hbounds :: !(S.HashSet F.LocSymbol) -- ^ Binders to turn into bounds using haskell definitions - , inlines :: !(S.HashSet F.LocSymbol) -- ^ Binders to turn into logic inline using haskell definitions - , ignores :: !(S.HashSet (F.Located LHName)) -- ^ Binders to ignore during checking; that is DON't check the corebind. + , hmeas :: !(S.HashSet (F.Located LHName)) -- ^ Binders to turn into measures using haskell definitions + , inlines :: !(S.HashSet (F.Located LHName)) -- ^ Binders to turn into logic inline using haskell definitions + , ignores :: !(S.HashSet (F.Located LHName)) -- ^ Binders to ignore during checking; that is DON't check the corebind. , autosize :: !(S.HashSet (F.Located LHName)) -- ^ Type Constructors that get automatically sizing info , pragmas :: ![F.Located String] -- ^ Command-line configurations passed in through source , cmeasures :: ![Measure ty ()] -- ^ Measures attached to a type-class @@ -464,9 +464,9 @@ instance Semigroup (Spec ty bndr) where , rewriteWith = M.union (rewriteWith s1) (rewriteWith s2) , fails = S.union (fails s1) (fails s2) , reflects = S.union (reflects s1) (reflects s2) + , privateReflects = S.union (privateReflects s1) (privateReflects s2) , opaqueReflects = S.union (opaqueReflects s1) (opaqueReflects s2) , hmeas = S.union (hmeas s1) (hmeas s2) - , hbounds = S.union (hbounds s1) (hbounds s2) , inlines = S.union (inlines s1) (inlines s2) , ignores = S.union (ignores s1) (ignores s2) , autosize = S.union (autosize s1) (autosize s2) @@ -498,8 +498,8 @@ instance Monoid (Spec ty bndr) where , autois = S.empty , hmeas = S.empty , reflects = S.empty + , privateReflects = S.empty , opaqueReflects = S.empty - , hbounds = S.empty , inlines = S.empty , ignores = S.empty , autosize = S.empty @@ -532,7 +532,6 @@ instance Monoid (Spec ty bndr) where -- * The 'lazy', we don't do termination checking in lifted specs; -- * The 'reflects', the reflection has already happened at this point; -- * The 'hmeas', we have /already/ turned these into measures at this point; --- * The 'hbounds', ditto as 'hmeas'; -- * The 'inlines', ditto as 'hmeas'; -- * The 'ignores', ditto as 'hmeas'; -- * The 'pragmas', we can't make any use of this information for lifted specs; @@ -547,8 +546,6 @@ data LiftedSpec = LiftedSpec -- ^ Exported logic symbols , liftedAsmSigs :: HashSet (F.Located LHName, LocBareType) -- ^ Assumed (unchecked) types; including reflected signatures - , liftedAsmReflectSigs :: HashSet (F.LocSymbol, F.LocSymbol) - -- ^ Reflected assumed signatures , liftedSigs :: HashSet (F.Located LHName, LocBareType) -- ^ Asserted spec signatures , liftedInvariants :: HashSet (Maybe F.LocSymbol, LocBareType) @@ -599,7 +596,6 @@ emptyLiftedSpec = LiftedSpec { liftedMeasures = mempty , liftedExpSigs = mempty , liftedAsmSigs = mempty - , liftedAsmReflectSigs = mempty , liftedSigs = mempty , liftedInvariants = mempty , liftedIaliases = mempty @@ -772,7 +768,6 @@ toLiftedSpec a = LiftedSpec { liftedMeasures = S.fromList . measures $ a , liftedExpSigs = S.fromList . expSigs $ a , liftedAsmSigs = S.fromList . asmSigs $ a - , liftedAsmReflectSigs = S.fromList . asmReflectSigs $ a , liftedSigs = S.fromList . sigs $ a , liftedInvariants = S.fromList . invariants $ a , liftedIaliases = S.fromList . ialiases $ a @@ -803,7 +798,7 @@ unsafeFromLiftedSpec a = Spec { measures = S.toList . liftedMeasures $ a , expSigs = S.toList . liftedExpSigs $ a , asmSigs = S.toList . liftedAsmSigs $ a - , asmReflectSigs = S.toList . liftedAsmReflectSigs $ a + , asmReflectSigs = mempty , sigs = S.toList . liftedSigs $ a , relational = mempty , asmRel = mempty @@ -821,10 +816,10 @@ unsafeFromLiftedSpec a = Spec , rewrites = mempty , rewriteWith = mempty , reflects = mempty + , privateReflects = mempty , opaqueReflects = mempty , autois = liftedAutois a , hmeas = mempty - , hbounds = mempty , inlines = mempty , ignores = mempty , autosize = liftedAutosize a diff --git a/liquidhaskell-boot/tests/Parser.hs b/liquidhaskell-boot/tests/Parser.hs index c7e70f7333..47f7e7ceaa 100644 --- a/liquidhaskell-boot/tests/Parser.hs +++ b/liquidhaskell-boot/tests/Parser.hs @@ -103,10 +103,6 @@ testSpecP = parseSingleSpec "bound Foo = true" @?== "bound Foo forall [] . [] = true" - , testCase "bound HBound" $ - parseSingleSpec "bound step" @?== - "bound step" - , testCase "class measure" $ parseSingleSpec "class measure sz :: forall a. a -> Int" @?== "class measure sz :: forall a . lq_tmp$db##0:a -> Int" diff --git a/tests/basic/neg/AssmRefl01.hs b/tests/basic/neg/AssmRefl01.hs index adce7c5285..da350c44fc 100644 --- a/tests/basic/neg/AssmRefl01.hs +++ b/tests/basic/neg/AssmRefl01.hs @@ -1,5 +1,5 @@ -- | Testing when the pretended function is not reflected into the logic -{-@ LIQUID "--expect-error-containing=\"myfoobar\" must be reflected first using {-@ reflect \"myfoobar\" @-}" @-} +{-@ LIQUID "--expect-error-containing=myfoobar must be reflected first using {-@ reflect myfoobar @-}" @-} {-@ LIQUID "--reflection" @-} {-@ LIQUID "--ple" @-} diff --git a/tests/basic/neg/AssmRefl02.hs b/tests/basic/neg/AssmRefl02.hs index cb19e1aa04..cf37181fd9 100644 --- a/tests/basic/neg/AssmRefl02.hs +++ b/tests/basic/neg/AssmRefl02.hs @@ -1,5 +1,5 @@ -- | Duplicate reflection -{-@ LIQUID "--expect-error-containing=Duplicate reflection of \"foobar\"" @-} +{-@ LIQUID "--expect-error-containing=Duplicate reflection of foobar" @-} {-@ LIQUID "--reflection" @-} {-@ LIQUID "--ple" @-} @@ -16,4 +16,4 @@ myfoobar n = n `mod` 2 == 1 {-@ test :: { foobar 5 } @-} test :: () -test = () \ No newline at end of file +test = () diff --git a/tests/basic/neg/AssmRefl04.hs b/tests/basic/neg/AssmRefl04.hs index 9b616c5045..16d13fedd1 100644 --- a/tests/basic/neg/AssmRefl04.hs +++ b/tests/basic/neg/AssmRefl04.hs @@ -1,5 +1,5 @@ -- | Duplicate assume reflects -{-@ LIQUID "--expect-error-containing=Duplicate reflection of \"alwaysFalse\"" @-} +{-@ LIQUID "--expect-error-containing=Duplicate reflection of alwaysFalse" @-} {-@ LIQUID "--reflection" @-} {-@ LIQUID "--ple" @-} @@ -20,4 +20,4 @@ alwaysFalse2 = False {-@ test :: { alwaysFalse } @-} test :: () -test = () \ No newline at end of file +test = () diff --git a/tests/basic/pos/ReflExt02A.hs b/tests/basic/pos/ReflExt02A.hs index 7298a47f98..8c41572ffe 100644 --- a/tests/basic/pos/ReflExt02A.hs +++ b/tests/basic/pos/ReflExt02A.hs @@ -11,10 +11,10 @@ import ReflExt02B {-@ reflect ReflExt02B.myAdd @-} -{-@ reflect myAdd @-} +{-@ reflect ReflExt02A.myAdd @-} myAdd :: Int myAdd = 12 -- 3 + 2 + 1 = 6 {-@ lemma :: {ReflExt02B.myAdd 3 2 = 6 } @-} -lemma = () \ No newline at end of file +lemma = () diff --git a/tests/basic/pos/ReflExt03A.hs b/tests/basic/pos/ReflExt03A.hs index 331514df8f..e08f511050 100644 --- a/tests/basic/pos/ReflExt03A.hs +++ b/tests/basic/pos/ReflExt03A.hs @@ -8,8 +8,8 @@ module ReflExt03A where import ReflExt03B {-@ reflect f @-} -{-@ reflect ReflExt03B.myAdd @-} +{-@ private-reflect ReflExt03B.myAdd @-} -- 3 * 2 + 2 = 8 {-@ lemma :: {f 3 2 = 8} @-} -lemma = () \ No newline at end of file +lemma = () diff --git a/tests/benchmarks/cse230/src/Week10/State.hs b/tests/benchmarks/cse230/src/Week10/State.hs index ba1cfc1896..ba73a8276d 100644 --- a/tests/benchmarks/cse230/src/Week10/State.hs +++ b/tests/benchmarks/cse230/src/Week10/State.hs @@ -3,7 +3,7 @@ module State where -import Prelude hiding ((++), const, max) +import Prelude hiding ((++), const, max, init) import ProofCombinators data GState k v = Init v | Bind k v (GState k v) diff --git a/tests/benchmarks/icfp15/pos/Dropwhile.hs b/tests/benchmarks/icfp15/pos/Dropwhile.hs index e3f23077c2..1259302209 100644 --- a/tests/benchmarks/icfp15/pos/Dropwhile.hs +++ b/tests/benchmarks/icfp15/pos/Dropwhile.hs @@ -46,7 +46,7 @@ dropWhile f Emp = Emp -- | This `witness` bound relates the predicate used in dropWhile -{-@ bound witness @-} +{- bound witness @-} witness :: Eq a => (a -> Bool) -> (a -> Bool -> Bool) -> a -> Bool -> a -> Bool witness p w = \ y b v -> (not b) ==> w y b ==> (v == y) ==> p v diff --git a/tests/benchmarks/sf/Lists.hs b/tests/benchmarks/sf/Lists.hs index 4952edc9c1..d06b2d602f 100644 --- a/tests/benchmarks/sf/Lists.hs +++ b/tests/benchmarks/sf/Lists.hs @@ -4,7 +4,7 @@ module Lists where -import Prelude hiding (reverse, length, filter) +import Prelude hiding (reverse, length, filter, pred, sum) -- import Prelude (Char, Int, Bool (..)) import Language.Haskell.Liquid.ProofCombinators diff --git a/tests/errors/AmbiguousInline.hs b/tests/errors/AmbiguousInline.hs index 6b86e6ead1..c7cb1a97de 100644 --- a/tests/errors/AmbiguousInline.hs +++ b/tests/errors/AmbiguousInline.hs @@ -19,8 +19,7 @@ import Debug.Trace import GHC.TypeLits import Language.Haskell.Liquid.Prelude (liquidAssert) --- FIX import Prelude hiding (min, max) -import Prelude hiding (max) +import Prelude hiding (min, max) junk = BS.head diff --git a/tests/errors/AmbiguousReflect.hs b/tests/errors/AmbiguousReflect.hs index c3fa361a06..708f6752a3 100644 --- a/tests/errors/AmbiguousReflect.hs +++ b/tests/errors/AmbiguousReflect.hs @@ -1,13 +1,8 @@ +{-@ LIQUID "--expect-error-containing=Ambiguous specification symbol `mappend`" @-} {-@ LIQUID "--reflection" @-} module AmbiguousReflect where --- ISSUE: Uncomment the below to make this test pass --- --- import Prelude hiding (mappend) --- --- LH should give an error message indicating the above. - data D = D Int Int {-@ reflect mappend @-} diff --git a/tests/pos/Dropwhile.hs b/tests/pos/Dropwhile.hs index 605abceada..122b7648cc 100644 --- a/tests/pos/Dropwhile.hs +++ b/tests/pos/Dropwhile.hs @@ -63,7 +63,7 @@ dropWhile f Emp = Emp -- | This `witness` bound relates the predicate used in dropWhile -{-@ bound witness @-} +{- bound witness @-} witness :: Eq a => (a -> Bool) -> (a -> Bool -> Bool) -> a -> Bool -> a -> Bool witness p w = \ y b v -> (not b) ==> w y b ==> (v == y) ==> p v diff --git a/tests/pos/RepeatHigherOrder.hs b/tests/pos/RepeatHigherOrder.hs index 403a86a648..57df66885f 100644 --- a/tests/pos/RepeatHigherOrder.hs +++ b/tests/pos/RepeatHigherOrder.hs @@ -11,7 +11,7 @@ import Language.Haskell.Liquid.Prelude repeat :: Int -> (a -> a) -> a -> a goal :: Int -> Int -{-@ bound step @-} +{- bound step @-} step :: (a -> a -> Bool) -> (Int -> a -> Bool) -> Int -> a -> a -> Bool step pf pr = \ i x x' -> pr (i - 1) x ==> pf x x' ==> pr i x' diff --git a/tests/todo/ImportBoundLib.hs b/tests/todo/ImportBoundLib.hs index b88602694f..e2f6122ed7 100644 --- a/tests/todo/ImportBoundLib.hs +++ b/tests/todo/ImportBoundLib.hs @@ -2,7 +2,7 @@ module ImportBoundLib where data Proof -{-@ bound chain @-} +{- bound chain @-} chain :: (Proof -> Bool) -> (Proof -> Bool) -> (Proof -> Bool) -> Proof -> Bool chain p q r = \v -> p v