diff --git a/liquidhaskell-boot.cabal b/liquidhaskell-boot.cabal --- a/liquidhaskell-boot.cabal +++ b/liquidhaskell-boot.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: liquidhaskell-boot -version: 0.9.12.2 +version: 0.9.12.2.1 synopsis: Liquid Types for Haskell description: This package provides a plugin to verify Haskell programs. But most likely you should be using the [liquidhaskell package](https://hackage.haskell.org/package/liquidhaskell) @@ -122,7 +122,7 @@ hs-source-dirs: src src-ghc src-ghc-9.10 build-depends: base >= 4.11.1.0 && < 5 - , Diff >= 0.3 && < 0.6 + , Diff >= 0.3 && < 1.1 , array , aeson , binary @@ -142,9 +142,9 @@ , gitrev , hashable >= 1.3 && < 1.6 , hscolour >= 1.22 - , liquid-fixpoint == 0.9.6.3.3 + , liquid-fixpoint == 0.9.6.3.5 , mtl >= 2.1 - , optparse-applicative < 0.19 + , optparse-applicative < 0.20 , githash , megaparsec >= 8 , pretty >= 1.1 diff --git a/src-ghc/Liquid/GHC/API.hs b/src-ghc/Liquid/GHC/API.hs --- a/src-ghc/Liquid/GHC/API.hs +++ b/src-ghc/Liquid/GHC/API.hs @@ -206,6 +206,7 @@ , liftedTypeKindTyConName , listTyCon , listTyConName + , zonkAnyTyCon , naturalTy , nilDataCon , stringTy @@ -403,6 +404,7 @@ , newTyConInstRhs , piResultTys , splitAppTys + , splitForAllForAllTyBinders , splitFunTy_maybe , splitFunTys , splitTyConApp @@ -476,7 +478,12 @@ import GHC.Core.Opt.OccurAnal as Ghc ( occurAnalysePgm ) import GHC.Core.TyCo.FVs as Ghc (tyCoVarsOfCo, tyCoVarsOfType) -import GHC.Driver.Backend as Ghc (interpreterBackend) +import GHC.Driver.Backend as Ghc (backendName, interpreterBackend) +import GHC.Driver.Backend.Internal as Ghc (BackendName(NoBackend)) +import GHC.Driver.DynFlags as Ghc + ( DumpFlag(Opt_D_dump_timings) + , dopt_set + ) import GHC.Driver.Env as Ghc ( HscEnv(hsc_NC, hsc_unit_env, hsc_dflags, hsc_plugins) , Hsc @@ -826,7 +833,13 @@ , withBinBuffer ) import GHC.Utils.Error as Ghc (pprLocMsgEnvelope, withTiming) -import GHC.Utils.Logger as Ghc (Logger(logFlags), putLogMsg) +import GHC.Utils.Logger as Ghc + ( LogFlags + , Logger(logFlags) + , putLogMsg + , log_set_dopt + , updateLogFlags + ) import GHC.Utils.Outputable as Ghc hiding ((<>)) import GHC.Utils.Panic as Ghc (panic, throwGhcException, throwGhcExceptionIO) import GHC.Utils.Misc as Ghc (lengthAtLeast) diff --git a/src-ghc/Liquid/GHC/API/Extra.hs b/src-ghc/Liquid/GHC/API/Extra.hs --- a/src-ghc/Liquid/GHC/API/Extra.hs +++ b/src-ghc/Liquid/GHC/API/Extra.hs @@ -24,8 +24,14 @@ , thisPackage , tyConRealArity , untick + , withTimingWallClock ) where +import Control.Monad +import Control.Monad.IO.Class +import GHC.Conc (getAllocationCounter) +import Debug.Trace +import GHC.Clock (getMonotonicTimeNSec) import Liquid.GHC.API.StableModule as StableModule import GHC hiding (modInfoLookupName) import Data.Data (Data, gmapQr, gmapT) @@ -51,7 +57,10 @@ import GHC.Types.SrcLoc as Ghc import GHC.Types.Unique (getUnique, hasKey) +import GHC.Utils.Error as Ghc +import GHC.Utils.Logger as Ghc import GHC.Utils.Outputable as Ghc hiding ((<>)) +import qualified GHC.Utils.Outputable as Ghc import GHC.Unit.Module @@ -263,3 +272,72 @@ minus_RDR :: RdrName minus_RDR = nameRdrName minusName + +-- | A version of 'withTiming' that uses wall clock time instead of CPU time. +-- +-- This version is copied and modified from GHC's 'GHC.Utils.Error.withTiming' +withTimingWallClock :: MonadIO m + => Logger + -> SDoc -- ^ The name of the phase + -> (a -> ()) -- ^ A function to force the result + -- (often either @const ()@ or 'rnf') + -> m a -- ^ The body of the phase to be timed + -> m a +withTimingWallClock logger what force_result action = + if logVerbAtLeast logger 2 || logHasDumpFlag logger Opt_D_dump_timings + then do when printTimingsNotDumpToFile $ liftIO $ + logInfo logger $ withPprStyle defaultUserStyle $ + text "***" <+> what Ghc.<> colon + let ctx = log_default_user_context (logFlags logger) + alloc0 <- liftIO getAllocationCounter + !start <- liftIO getMonotonicTimeNSec + eventBegins ctx what + recordAllocs alloc0 + !r <- action + () <- pure $ force_result r + eventEnds ctx what + !end <- liftIO getMonotonicTimeNSec + alloc1 <- liftIO getAllocationCounter + recordAllocs alloc1 + -- recall that allocation counter counts down + let alloc = alloc0 - alloc1 + time = (end - start) `div` 1000000 + + when (logVerbAtLeast logger 2 && printTimingsNotDumpToFile) + $ liftIO $ logInfo logger $ withPprStyle defaultUserStyle + (text "!!!" <+> what Ghc.<> colon <+> text "finished in" + <+> word64 time + <+> text "milliseconds" + Ghc.<> comma + <+> text "allocated" + <+> doublePrec 3 (realToFrac alloc / 1024 / 1024) + <+> text "megabytes") + + liftIO $ putDumpFileMaybe logger Opt_D_dump_timings "" FormatText + $ text $ showSDocOneLine ctx + $ hsep [ what Ghc.<> colon + , text "alloc=" Ghc.<> ppr alloc + , text "time=" Ghc.<> word64 time + ] + pure r + else action + + where -- Avoid both printing to console and dumping to a file (#20316). + printTimingsNotDumpToFile = + not (log_dump_to_file (logFlags logger)) + + recordAllocs alloc = + liftIO $ traceMarkerIO $ "GHC:allocs:" ++ show alloc + + eventBegins ctx w = do + let doc = eventBeginsDoc ctx w + liftIO $ traceMarkerIO doc + liftIO $ traceEventIO doc + + eventEnds ctx w = do + let doc = eventEndsDoc ctx w + liftIO $ traceMarkerIO doc + liftIO $ traceEventIO doc + + eventBeginsDoc ctx w = showSDocOneLine ctx $ text "GHC:started:" <+> w + eventEndsDoc ctx w = showSDocOneLine ctx $ text "GHC:finished:" <+> w diff --git a/src/Language/Haskell/Liquid/Bare.hs b/src/Language/Haskell/Liquid/Bare.hs --- a/src/Language/Haskell/Liquid/Bare.hs +++ b/src/Language/Haskell/Liquid/Bare.hs @@ -93,17 +93,18 @@ -> TargetDependencies -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec)) makeTargetSpec cfg localVars lnameEnv lmap targetSrc bareSpec dependencies = do - let targDiagnostics = Bare.checkTargetSrc cfg targetSrc + let targDiagnostics = Bare.checkTargetSrc cfg bareSpec targetSrc let depsDiagnostics = mapM (Bare.checkBareSpec . snd) legacyDependencies let bareSpecDiagnostics = Bare.checkBareSpec bareSpec - case targDiagnostics >> depsDiagnostics >> bareSpecDiagnostics of - Left d | noErrors d -> secondPhase (allWarnings d) + let stratDiagnostics = Bare.checkStratTys bareSpec targetSrc + case targDiagnostics >> depsDiagnostics >> bareSpecDiagnostics >> stratDiagnostics of + Left d | noErrors d -> secondPhase [] (allWarnings d) Left d -> return $ Left d - Right () -> secondPhase mempty + Right stratNames -> secondPhase stratNames mempty where - secondPhase :: [Warning] -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec)) - secondPhase phaseOneWarns = do - diagOrSpec <- makeGhcSpec cfg lnameEnv localVars (fromTargetSrc targetSrc) lmap bareSpec legacyDependencies + secondPhase :: [Ghc.Name] -> [Warning] -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec)) + secondPhase stratNames phaseOneWarns = do + diagOrSpec <- makeGhcSpec stratNames cfg lnameEnv localVars (fromTargetSrc targetSrc) lmap bareSpec legacyDependencies case diagOrSpec of Left d -> return $ Left d Right (warns, ghcSpec) -> do @@ -144,7 +145,8 @@ -- | @makeGhcSpec@ invokes @makeGhcSpec0@ to construct the @GhcSpec@ and then -- validates it using @checkGhcSpec@. ------------------------------------------------------------------------------------- -makeGhcSpec :: Config +makeGhcSpec :: [Ghc.Name] + -> Config -> LogicNameEnv -> Bare.LocalVars -> GhcSrc @@ -153,12 +155,12 @@ -> [(ModName, Ms.BareSpec)] -> Ghc.TcRn (Either Diagnostics ([Warning], GhcSpec)) ------------------------------------------------------------------------------------- -makeGhcSpec cfg lenv localVars src lmap targetSpec dependencySpecs = do +makeGhcSpec stratNames cfg lenv localVars src lmap bareSpec dependencySpecs = do ghcTyLookupEnv <- Bare.makeGHCTyLookupEnv (_giCbs src) tcg <- Ghc.getGblEnv instEnvs <- Ghc.tcGetInstEnvs - (dg0, sp) <- makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec dependencySpecs - let diagnostics = Bare.checkTargetSpec (targetSpec : map snd dependencySpecs) + (dg0, sp) <- makeGhcSpec0 stratNames cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap bareSpec dependencySpecs + let diagnostics = Bare.checkTargetSpec (bareSpec : map snd dependencySpecs) (toTargetSrc src) (ghcSpecEnv sp) (_giCbs src) @@ -195,7 +197,8 @@ -- lets us use aliases inside data-constructor definitions. ------------------------------------------------------------------------------------- makeGhcSpec0 - :: Config + :: [Ghc.Name] + -> Config -> Bare.GHCTyLookupEnv -> Ghc.TcGblEnv -> Ghc.InstEnvs @@ -206,20 +209,24 @@ -> Ms.BareSpec -> [(ModName, Ms.BareSpec)] -> Ghc.TcRn (Diagnostics, GhcSpec) -makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec dependencySpecs = do +makeGhcSpec0 stratNames cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap bareSpec dependencySpecs = do globalRdrEnv <- Ghc.tcg_rdr_env <$> Ghc.getGblEnv -- build up environments tycEnv <- makeTycEnv1 env (tycEnv0, datacons) coreToLg simplifier let tyi = Bare.tcTyConMap tycEnv let sigEnv = makeSigEnv embs tyi (_gsExports src) rtEnv + -- This spec is used to add lifted measures. let lSpec1 = makeLiftedSpec1 cfg src tycEnv lmap mySpec1 + -- 'mySpec' and 'specs' contain the result of the first lifting stages, see [NOTE]: REFLECT-IMPORTS + -- and the expanded aliases obtained using 'rtEnv'. 'myRTE' is a filtered 'rtEnv' used at the final + -- lifting. let mySpec = mySpec2 <> lSpec1 let specs = M.insert name mySpec iSpecs2 - let myRTE = myRTEnv src env sigEnv rtEnv + let myRTE = myRTEnv src env sigEnv rtEnv -- NB: we first compute a measure environment w/o the opaque reflections, so that we can bootstrap -- the signature `sig`. Then we'll add the opaque reflections before we compute `sData` and al. let (dg1, measEnv0) = withDiagnostics $ makeMeasEnv env tycEnv sigEnv specs - let (dg2, (specInstances, sig)) = withDiagnostics $ makeSpecSig cfg name mySpec iSpecs2 env sigEnv tycEnv measEnv0 (_giCbs src) + let (dg2, (specInstances, sig)) = withDiagnostics $ makeSpecSig stratNames cfg name mySpec iSpecs2 env sigEnv tycEnv measEnv0 (_giCbs src) elaboratedSig <- if allowTC then Bare.makeClassAuxTypes (elaborateSpecType coreToLg simplifier) datacons instMethods >>= elaborateSig sig @@ -282,15 +289,34 @@ -- Preserve rinstances. , asmReflectSigs = Ms.asmReflectSigs mySpec , reflects = Ms.reflects mySpec0 - , cmeasures = mconcat $ map Ms.cmeasures $ map snd dependencySpecs ++ [targetSpec] - , embeds = Ms.embeds targetSpec + , cmeasures = mconcat $ map Ms.cmeasures $ map snd dependencySpecs ++ [bareSpec] + , embeds = Ms.embeds bareSpec , privateReflects = mconcat $ map (privateReflects . snd) mspecs - , defines = Ms.defines targetSpec + , defines = Ms.defines bareSpec , usedDataCons = usedDcs + -- Placing the @bareSpec@ at the end causes local aliases + -- to take precedence over imported ones when their names clash. + -- Alternatively, the last among @dependencySpecs@ (which is + -- ordered lexcographically) is picked. + -- See @tests/name/pos/ImportedTypeAlias.hs@ + , aliases = M.elems $ M.fromList $ + [ (lhNameToUnqualifiedSymbol (val . rtName $ rt) , rt) + | rt <- concat $ + map (aliases . snd) dependencySpecs ++ + [expandedAliasesOf myRTE typeAliases $ aliases bareSpec] + ] + , ealiases = M.elems $ M.fromList $ + [ (lhNameToUnqualifiedSymbol (val . rtName $ rt) , rt) + | rt <- concat $ + map (ealiases . snd) dependencySpecs ++ + [expandedAliasesOf myRTE exprAliases $ ealiases mySpec1'] + ] } }) where thisModule = Ghc.tcg_mod tcg + expandedAliasesOf myRTE fld = Mb.mapMaybe ((`M.lookup` fld myRTE) . val . rtName) + -- typeclass elaboration coreToLg ce = @@ -322,24 +348,30 @@ simplifier :: Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr simplifier = pure -- no simplification allowTC = typeclass cfg + -- Specs with type and expression aliases expanded. mySpec2 = Bare.expand rtEnv (F.dummyPos "expand-mySpec2") mySpec1 iSpecs2 = Bare.expand rtEnv (F.dummyPos "expand-iSpecs2") (M.fromList dependencySpecs) - rtEnv = Bare.makeRTEnv env name mySpec1 dependencySpecs lmap + -- Environment for alias lookup and expansion. + rtEnv = Bare.makeRTEnv lenv name mySpec1' dependencySpecs mspecs = (name, mySpec0) : dependencySpecs + -- mySpec0 adds typeclass methods to the bare spec. (mySpec0, instMethods) = if allowTC - then Bare.compileClasses src env (name, targetSpec) dependencySpecs - else (targetSpec, []) + then Bare.compileClasses src env (name, bareSpec) dependencySpecs + else (bareSpec, []) + mySpec1' = addDefinesToExprAliases env lmap mySpec1 + -- Ready for alias expansion. mySpec1 = mySpec0 <> lSpec0 + -- This spec just has the 'ealiases' (with Haskell inlines) and 'dataDecls' fields. lSpec0 = makeLiftedSpec0 cfg src embs lmap mySpec0 embs = makeEmbeds src ghcTyLookupEnv (mySpec0 : map snd dependencySpecs) dm = Bare.tcDataConMap tycEnv0 (dg0, datacons, tycEnv0) = makeTycEnv0 cfg name env embs mySpec2 iSpecs2 - env = Bare.makeEnv cfg ghcTyLookupEnv dataConIds tcg instEnvs localVars src lmap ((name, targetSpec) : dependencySpecs) + env = Bare.makeEnv cfg ghcTyLookupEnv dataConIds tcg instEnvs localVars src lmap ((name, bareSpec) : dependencySpecs) -- check barespecs name = F.notracepp ("ALL-SPECS" ++ zzz) $ _giTargetMod src zzz = F.showpp (fst <$> mspecs) - usedDcs = collectAllDataCons (_giCbs src) $ targetSpec : map snd dependencySpecs + usedDcs = collectAllDataCons (_giCbs src) $ bareSpec : map snd dependencySpecs dataConIds = [ Ghc.dataConWorkId dc | lhn <- S.toList usedDcs @@ -428,6 +460,19 @@ where symTc = Mb.maybeToList . either (const Nothing) Just . Bare.lookupGhcTyConLHName env +-- | See [NOTE:EXPRESSION-ALIASES] +addDefinesToExprAliases :: Bare.Env -> LogicMap -> Ms.BareSpec -> Ms.BareSpec +addDefinesToExprAliases env lmap mySpec = + mySpec { + Ms.ealiases = Ms.ealiases mySpec ++ + if typeclass (getConfig env) then [] + -- lmap expansion happens during elaboration + -- this clearly breaks things if a signature + -- contains lmap functions but never gets + -- elaborated + else [ e | (_, xl) <- M.toList (lmSymDefs lmap), let e = lmapEAlias xl ] + } + -------------------------------------------------------------------------------- -- | [NOTE]: REFLECT-IMPORTS -- @@ -454,7 +499,8 @@ -- This is because we need the inlines to build the @BareRTEnv@ which then -- does the alias @expand@ business, that in turn, lets us build the DataConP, -- i.e. the refined datatypes and their associate selectors, projectors etc, --- that are needed for subsequent stages of the lifting. +-- that are needed for subsequent stages of the lifting. Here is relevant to +-- [NOTE:EXPRESSION-ALIASES]. -------------------------------------------------------------------------------- makeLiftedSpec0 :: Config -> GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareSpec -> Ms.BareSpec @@ -819,10 +865,10 @@ ---------------------------------------------------------------------------------------- -makeSpecSig :: Config -> ModName -> Ms.BareSpec -> Bare.ModSpecs -> Bare.Env -> Bare.SigEnv -> Bare.TycEnv -> Bare.MeasEnv -> [Ghc.CoreBind] +makeSpecSig :: [Ghc.Name] -> Config -> ModName -> Ms.BareSpec -> Bare.ModSpecs -> Bare.Env -> Bare.SigEnv -> Bare.TycEnv -> Bare.MeasEnv -> [Ghc.CoreBind] -> Bare.Lookup ([RInstance LocBareType], GhcSpecSig) ---------------------------------------------------------------------------------------- -makeSpecSig cfg name mySpec specs env sigEnv tycEnv measEnv cbs = do +makeSpecSig stratNames cfg name mySpec specs env sigEnv tycEnv measEnv cbs = do mySigs <- makeTySigs env sigEnv name mySpec aSigs <- F.notracepp ("makeSpecSig aSigs " ++ F.showpp name) $ makeAsmSigs env sigEnv name allSpecs let asmSigs = Bare.tcSelVars tycEnv ++ aSigs @@ -837,6 +883,7 @@ asmRel <- makeRelation env name sigEnv (Ms.asmRel mySpec) return (instances, SpSig { gsTySigs = tySigs + , gsStratCtos = stratNames , gsAsmSigs = asmSigs , gsAsmReflects = bimap getVar getVar <$> concatMap (asmReflectSigs . snd) allSpecs , gsRefSigs = [] @@ -1373,7 +1420,6 @@ , isLocInFile srcF t ] , Ms.axeqs = gsMyAxioms refl - , Ms.aliases = F.notracepp "MY-ALIASES" $ M.elems . typeAliases $ myRTE , Ms.ealiases = M.elems . exprAliases $ myRTE , Ms.qualifiers = filter (isLocInFile srcF) (gsQualifiers qual) } @@ -1386,7 +1432,6 @@ xbs = toBare <$> reflTySigs reflTySigs = [(x, t) | (x,t,_) <- gsHAxioms refl] reflVars = S.fromList (fst <$> reflTySigs) - -- myAliases fld = M.elems . fld $ myRTE srcF = _giTarget src isLocalName = \case @@ -1418,42 +1463,36 @@ -------------------------------------------------------------------------------- --- | @myRTEnv@ slices out the part of RTEnv that was generated by aliases defined --- in the _target_ file, "cooks" the aliases (by conversion to SpecType), and --- then saves them back as BareType. +-- | @myRTEnv@ "cooks" the type aliases by converting them to SpecType and then +-- back to BareType. -------------------------------------------------------------------------------- myRTEnv :: GhcSrc -> Bare.Env -> Bare.SigEnv -> BareRTEnv -> BareRTEnv -myRTEnv src env sigEnv rtEnv = mkRTE tAs' eAs +myRTEnv src env sigEnv rtEnv = rtEnv { typeAliases = M.fromList [ (aName a, a) | a <- tAs' ] } where - tAs' = normalizeBareAlias env sigEnv name <$> tAs - tAs = myAliases typeAliases - eAs = myAliases exprAliases - myAliases fld = filter (isLocInFile srcF) . M.elems . fld $ rtEnv - srcF = _giTarget src - name = _giTargetMod src - -mkRTE :: [Located (RTAlias x a)] -> [Located (RTAlias F.Symbol F.Expr)] -> RTEnv x a -mkRTE tAs eAs = RTE - { typeAliases = M.fromList [ (aName a, a) | a <- tAs ] - , exprAliases = M.fromList [ (aName a, a) | a <- eAs ] - } - where aName = rtName . F.val + tAs' = normalizeBareAlias env sigEnv modName <$> tAs + tAs = M.elems . typeAliases $ rtEnv + modName = _giTargetMod src + aName = F.val . rtName -normalizeBareAlias :: Bare.Env -> Bare.SigEnv -> ModName -> Located BareRTAlias - -> Located BareRTAlias -normalizeBareAlias env sigEnv name lx = fixRTA <$> lx +-- | Prepare an alias for constraint checking by /fixing/ its body and type argument names. +normalizeBareAlias :: Bare.Env -> Bare.SigEnv -> ModName -> BareRTAlias + -> BareRTAlias +normalizeBareAlias env sigEnv name a = fixRTA a where fixRTA :: BareRTAlias -> BareRTAlias fixRTA = mapRTAVars fixArg . fmap fixBody + -- | Uses GHC to assign arguments a unique symbol by lifting them as local 'Type' variables and back. fixArg :: Symbol -> Symbol fixArg = F.symbol . GM.symbolTyVar + -- | Completely /cooks/ the body of a type alias by conversion to 'SpecType' + -- and back. At this point they have been expanded already. fixBody :: BareType -> BareType fixBody = Bare.specToBare . F.val . Bare.cookSpecType env sigEnv name Bare.RawTV - . F.atLoc lx + . F.atLoc (rtName a) withDiagnostics :: (Monoid a) => Bare.Lookup a -> (Diagnostics, a) diff --git a/src/Language/Haskell/Liquid/Bare/Axiom.hs b/src/Language/Haskell/Liquid/Bare/Axiom.hs --- a/src/Language/Haskell/Liquid/Bare/Axiom.hs +++ b/src/Language/Haskell/Liquid/Bare/Axiom.hs @@ -45,6 +45,7 @@ import Data.Function (on) import qualified Data.Map as Map import qualified Data.HashMap.Strict as M +import System.IO.Unsafe (unsafePerformIO) findDuplicatePair :: Ord k => (a -> k) -> [a] -> Maybe (a, a) findDuplicatePair key xs = @@ -113,8 +114,11 @@ else Ex.throw $ mkError actual $ show qPretended ++ " and " ++ show qActual ++ " should have the same type. But " ++ - "types " ++ F.showpp pretendedTy ++ " and " ++ F.showpp actualTy ++ " do not match." + "types\n\n" ++ showType pretendedTy ++ "\n\n and\n\n" ++ showType actualTy ++ "\n\ndo not match." where + showType = Ghc.showPpr + (unsafePerformIO $ Ghc.reflectGhc Ghc.getDynFlags $ gtleSession $ reTyLookupEnv env) + at = val $ strengthenSpecWithMeasure sig env actualV pretended{val=qPretended} -- Get the Ghc.Var's of the actual and pretended function names diff --git a/src/Language/Haskell/Liquid/Bare/Check.hs b/src/Language/Haskell/Liquid/Bare/Check.hs --- a/src/Language/Haskell/Liquid/Bare/Check.hs +++ b/src/Language/Haskell/Liquid/Bare/Check.hs @@ -3,16 +3,18 @@ {-# LANGUAGE TupleSections #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE DeriveTraversable #-} + {-# OPTIONS_GHC -Wno-x-partial #-} module Language.Haskell.Liquid.Bare.Check ( checkTargetSpec , checkBareSpec , checkTargetSrc + , checkStratTys , tyCompat ) where - import Language.Haskell.Liquid.Constraint.ToFixpoint import Liquid.GHC.API as Ghc hiding ( Located @@ -34,6 +36,7 @@ import qualified Language.Fixpoint.Misc as Misc import Language.Fixpoint.SortCheck (ElabM, checkSorted, checkSortedReftFull, checkSortFull) import qualified Language.Fixpoint.Types as F +import qualified Language.Fixpoint.Types.Config as FC import qualified Language.Haskell.Liquid.GHC.Misc as GM import Language.Haskell.Liquid.GHC.Play (getNonPositivesTyCon) import Language.Haskell.Liquid.Misc (condNull, thd5, foldMapM) @@ -53,29 +56,103 @@ import qualified Language.Haskell.Liquid.Bare.Types as Bare import qualified Language.Haskell.Liquid.Bare.Resolve as Bare import Language.Haskell.Liquid.UX.Config -import Language.Fixpoint.Types.Config (ElabFlags (ElabFlags), solverFlags) - +-- import Language.Fixpoint.Types.Config (ElabFlags (ElabFlags)) ---------------------------------------------------------------------------------------------- -- | Checking TargetSrc ------------------------------------------------------------------------ ---------------------------------------------------------------------------------------------- -checkTargetSrc :: Config -> TargetSrc -> Either Diagnostics () -checkTargetSrc cfg spec +checkTargetSrc :: Config -> BareSpec -> TargetSrc -> Either Diagnostics () +checkTargetSrc cfg bare spec | nopositivity cfg || nopositives == emptyDiagnostics = Right () | otherwise = Left nopositives - where nopositives = checkPositives (gsTcs spec) + where nopositives = checkPositives bare $ gsTcs spec +isStratifiedTyCon :: BareSpec -> TyCon -> Bool +isStratifiedTyCon bs tc = Ghc.tyConName tc `elem` sn + where sn = mapMaybe (getLHGHCName . F.val) $ S.toList $ stratified bs -checkPositives :: [TyCon] -> Diagnostics -checkPositives tys = mkDiagnostics [] $ mkNonPosError (getNonPositivesTyCon tys) +checkPositives :: BareSpec -> [TyCon] -> Diagnostics +checkPositives bare tys = mkDiagnostics [] + $ mkNonPosError + $ filter (not . isStratifiedTyCon bare . fst) + $ getNonPositivesTyCon tys mkNonPosError :: [(TyCon, [DataCon])] -> [Error] mkNonPosError tcs = [ ErrPosTyCon (getSrcSpan tc) (pprint tc) (pprint dc <+> ":" <+> pprint (dataConRepType dc)) | (tc, dc:_) <- tcs] +-------------------------------------------------- +-- | Checking that stratified ctors are present -- +-------------------------------------------------- + +--- | Like 'Either' but the 'Semigroup' instance combines the failure +--- | values. +data Validation e a + = Failure e + | Success a + deriving (Show, Eq, Functor, Foldable, Traversable) + +instance (Semigroup e, Semigroup a) => Semigroup (Validation e a) where + Failure e1 <> Failure e2 = Failure (e1 <> e2) + Failure e <> _ = Failure e + _ <> Failure e = Failure e + Success x <> Success y = Success (x <> y) + +instance (Semigroup e, Monoid a) => Monoid (Validation e a) where + mempty = Success mempty + mappend = (<>) + +valToEither :: Validation e a -> Either e a +valToEither (Failure e) = Left e +valToEither (Success x) = Right x + +-- | Check that all stratified types have their constructors +-- defined with refinement type signatures in the BareSpec. +-- +-- Yields the names of the data constructors of the stratified types. +checkStratTys :: BareSpec -> TargetSrc -> Either Diagnostics [Name] +checkStratTys bare spec = + valToEither + $ foldMap (checkStratTy bare) + $ mapMaybe (traverse (findTyCon (gsTcs spec))) + $ S.toList $ stratified bare + +-- | Find the TyCon corresponding to the given LHName in the given list of TyCons +findTyCon :: [TyCon] -> LHName -> Maybe TyCon +findTyCon tcs nm = do + c <- getLHGHCName nm + L.find ((== c) . Ghc.tyConName) tcs + +-- | Check that the given TyCon is an ADT and that all its constructors +-- have refinements in the BareSpec. +checkStratTy :: BareSpec -> Located TyCon -> Validation Diagnostics [Name] +checkStratTy spec ltycon = + case tyConDataCons_maybe (val ltycon) of + Just ctors -> foldMap (checkStratCtor ltycon spec) ctors + Nothing -> Failure $ mkDiagnostics mempty [ err ] + where + pos = GM.sourcePos2SrcSpan (loc ltycon) (locE ltycon) + err = ErrStratNotAdt pos (pprint (Ghc.tyConName $ val ltycon)) + +-- | Check that the given DataCon has a refinement type signature in the BareSpec. +-- +-- Yields the names of the data constructors that are stratified. +checkStratCtor :: Located TyCon -> BareSpec -> DataCon -> Validation Diagnostics [Name] +checkStratCtor ltycon spec datacon + | hasRefinementTypeSignature datacon (map (val . fst) $ sigs spec) + = Success [ dataConName datacon ] + | otherwise = Failure $ mkDiagnostics mempty [ err ] + where + pos = GM.sourcePos2SrcSpan (loc ltycon) (locE ltycon) + err = ErrStratNotRefCtor pos (pprint $ dataConName datacon) (pprint $ Ghc.tyConName $ val ltycon) + hasRefinementTypeSignature :: DataCon -> [LHName] -> Bool + hasRefinementTypeSignature dc lns = + dataConName dc `elem` mapMaybe getLHGHCName lns + + ---------------------------------------------------------------------------------------------- -- | Checking BareSpec ------------------------------------------------------------------------ ---------------------------------------------------------------------------------------------- @@ -166,8 +243,8 @@ -- TODO-REBARE ++ checkQualifiers env (gsQualifiers (gsQual sp)) <> checkDuplicate (gsAsmSigs (gsSig tsp)) <> checkDupIntersect (gsTySigs (gsSig tsp)) (gsAsmSigs (gsSig tsp)) - <> checkRTAliases "Type Alias" env tAliases - <> checkRTAliases "Pred Alias" env eAliases + <> checkRTAliases "Type Alias" env myTAliases + <> checkRTAliases "Pred Alias" env myPAliases -- ++ _checkDuplicateFieldNames (gsDconsP sp) -- NV TODO: allow instances of refined classes to be refined -- but make sure that all the specs are checked. @@ -179,10 +256,11 @@ then mempty else checkConstructorRefinement (gsTySigs $ gsSig tsp) - _rClasses = concatMap Ms.classes specs - _rInsts = concatMap Ms.rinstance specs - tAliases = concat [Ms.aliases sp | sp <- specs] - eAliases = concat [Ms.ealiases sp | sp <- specs] + _rClasses = concatMap Ms.classes specs + _rInsts = concatMap Ms.rinstance specs + -- Duplicate alias (definition) is checked within the bare spec only. + myTAliases = Ms.aliases (head specs) + myPAliases = Ms.ealiases (head specs) emb = gsTcEmbeds (gsName tsp) tcEnv = gsTyconEnv (gsName tsp) ms = gsMeasures (gsData tsp) @@ -194,9 +272,11 @@ noPrune = not (pruneFlag tsp) txCtors ts = [(v, fmap (fmap (fmap (F.filterUnMatched temps))) t) | (v, t) <- ts] temps = F.makeTemplates $ gsUnsorted $ gsData tsp - ef = maybe (ElabFlags False) solverFlags $ smtsolver $ getConfig tsp - -- env' = L.foldl' (\e (x, s) -> insertSEnv x (RR s mempty) e) env wiredSortedSyms + ef = mkElabFlags (smtsolver $ getConfig tsp) +mkElabFlags :: Maybe FC.SMTSolver -> FC.ElabFlags +mkElabFlags Nothing = FC.ElabFlags False False +mkElabFlags (Just slv) = FC.mkElabFlags slv False -- | Tests that the returned refinement type of data constructors has predicate @True@ or @prop v == e@. @@ -222,11 +302,7 @@ validRef (F.Reft (_, F.PTrue)) = True -- Prop foo from ProofCombinators - validRef (F.Reft (v, F.PAtom F.Eq (F.EApp (F.EVar n) (F.EVar v')) _)) - | n == "Language.Haskell.Liquid.ProofCombinators.prop" - , v == v' - = True - validRef _ = False + validRef n = isJust $ getPropIndex n isCtorName x = case idDetails x of DataConWorkId _ -> True @@ -267,7 +343,7 @@ vtes = [ (x, (t, es)) | (x, t) <- gsTySigs sig, let es = M.lookup x vExprs] vExprs = M.fromList [ (x, es) | (x, _, es) <- gsTexprs sig ] - checkVisitor :: ElabFlags -> CoreVisitor (F.SEnv F.SortedReft) Diagnostics + checkVisitor :: FC.ElabFlags -> CoreVisitor (F.SEnv F.SortedReft) Diagnostics checkVisitor ef = CoreVisitor { envF = \env v -> F.insertSEnv (F.symbol v) (vSort v) env , bindF = \env acc v -> runReader (errs env v) ef <> acc @@ -305,7 +381,7 @@ $+$ msg) (pprint (tcpCon tcp)) - go :: ElabFlags -> TyConP -> Maybe ((F.Symbol -> F.Expr, TyConP), Doc) + go :: FC.ElabFlags -> TyConP -> Maybe ((F.Symbol -> F.Expr, TyConP), Doc) go ef tcp = case tcpSizeFun tcp of Nothing -> Nothing Just f | isWiredInLenFn f -> Nothing -- Skip the check. @@ -326,7 +402,8 @@ -> F.SEnv F.SortedReft -> (Maybe Var, LocSpecType) -> ElabM Diagnostics -checkInv allowHO bsc emb tcEnv env (_, t) = checkTy allowHO bsc err emb tcEnv env t +checkInv allowHO bsc emb tcEnv env (_, t) = + checkTy allowHO bsc err emb tcEnv env t where err = ErrInvt (GM.sourcePosSrcSpan $ loc t) (val t) @@ -363,7 +440,7 @@ -- FIXME: Should _ be removed if it isn't used? -checkRTAliases :: String -> t -> [Located (RTAlias s a)] -> Diagnostics +checkRTAliases :: String -> t -> [RTAlias s a] -> Diagnostics checkRTAliases msg _ as = err1s where err1s = checkDuplicateRTAlias msg as @@ -377,7 +454,8 @@ -> F.SEnv F.SortedReft -> (v, LocSpecType) -> ElabM Diagnostics -checkBind allowHO bsc s emb tcEnv env (v, t) = checkTy allowHO bsc msg emb tcEnv env t +checkBind allowHO bsc s emb tcEnv env (v, t) = + checkTy allowHO bsc msg emb tcEnv env t where msg = ErrTySpec (GM.fSrcSpan t) (Just s) (pprint v) (val t) @@ -399,10 +477,10 @@ -- mkErr = uncurry (\ e d -> ErrTermSpec (GM.sourcePosSrcSpan l) (pprint v) (text "ill-sorted" ) e t d) -- mkErr' = uncurry (\ e d -> ErrTermSpec (GM.sourcePosSrcSpan l) (pprint v) (text "non-numeric") e t d) - go :: ElabFlags -> [F.Located F.Expr] -> Maybe (F.Expr, Doc) + go :: FC.ElabFlags -> [F.Located F.Expr] -> Maybe (F.Expr, Doc) go ef = L.foldl' (\err e -> err <|> (val e,) <$> runReader (checkSorted (F.srcSpan e) env' (val e)) ef) Nothing - go' :: ElabFlags -> [F.Located F.Expr] -> Maybe (F.Expr, Doc) + go' :: FC.ElabFlags -> [F.Located F.Expr] -> Maybe (F.Expr, Doc) go' ef = L.foldl' (\err e -> err <|> (val e,) <$> runReader (checkSorted (F.srcSpan e) env' (cmpZero e)) ef) Nothing env' = F.sr_sort <$> L.foldl' (\e (x,s) -> F.insertSEnv x s e) env xts @@ -456,15 +534,15 @@ xts' = F.notracepp "XTS" $ filter (not . (`elem` cls) . fst) xts cls = F.notracepp "CLS" cms -checkDuplicateRTAlias :: String -> [Located (RTAlias s a)] -> Diagnostics +checkDuplicateRTAlias :: String -> [RTAlias s a] -> Diagnostics checkDuplicateRTAlias s tas = mkDiagnostics mempty (map mkError dups) where - mkError xs@(x:_) = ErrDupAlias (GM.fSrcSpan x) - (text s) - (pprint . rtName . val $ x) - (GM.fSrcSpan <$> xs) - mkError [] = panic Nothing "mkError: called on empty list" - dups = [z | z@(_:_:_) <- groupDuplicatesOn (rtName . val) tas] + mkError xs@(x:_) = ErrDupAlias (GM.fSrcSpan $ rtName x) + (text s) + (pprint $ rtName x) + (GM.fSrcSpan . rtName <$> xs) + mkError [] = panic Nothing "mkError: called on empty list" + dups = [z | z@(_:_:_) <- groupDuplicatesOn (lhNameToUnqualifiedSymbol . val . rtName) tas] groupDuplicatesOn :: Ord b => (a -> b) -> [a] -> [[a]] groupDuplicatesOn f = L.groupBy ((==) `on` f) . L.sortOn f @@ -604,7 +682,7 @@ mkPEnv _ = [] pvType' p = Misc.safeHead (showpp p ++ " not in env of " ++ showpp rt) [pvType q | q <- penv, pname p == pname q] - +-- TODO remove the unused UReft arg checkReft :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar (UReft r))) => F.SrcSpan -> F.SEnv F.SortedReft -> F.TCEmb TyCon -> Maybe (RRType (UReft r)) -> UReft r -> ElabM (Maybe Doc) checkReft _ _ _ Nothing _ = pure Nothing -- TODO:RPropP/Ref case, not sure how to check these yet. @@ -777,6 +855,3 @@ (pprint (val (msName m))) (pprint ((dataConTyCon . ctor . head . msEqns) m)) (GM.fSrcSpan <$> (m:ms))) - - - diff --git a/src/Language/Haskell/Liquid/Bare/Elaborate.hs b/src/Language/Haskell/Liquid/Bare/Elaborate.hs --- a/src/Language/Haskell/Liquid/Bare/Elaborate.hs +++ b/src/Language/Haskell/Liquid/Bare/Elaborate.hs @@ -556,6 +556,7 @@ rename F.FInt = F.FInt rename F.FReal = F.FReal rename F.FNum = F.FNum + rename (F.FNatNum n) = F.FNatNum n rename F.FFrac = F.FFrac rename ( F.FObj s ) = F.FObj (f s) rename t'@(F.FVar _ ) = t' @@ -704,9 +705,6 @@ RApp RTyCon { rtc_tc = tc } ts _ _ -> mkHsTyConApp (getRdrName tc) [ specTypeToLHsType t | t <- ts, notExprArg t ] - where - notExprArg (RExprArg _) = False - notExprArg _ = True RAllE _ tin tout -> nlHsFunTy (specTypeToLHsType tin) (specTypeToLHsType tout) REx _ tin tout -> nlHsFunTy (specTypeToLHsType tin) (specTypeToLHsType tout) RAppTy _ (RExprArg _) _ -> diff --git a/src/Language/Haskell/Liquid/Bare/Expand.hs b/src/Language/Haskell/Liquid/Bare/Expand.hs --- a/src/Language/Haskell/Liquid/Bare/Expand.hs +++ b/src/Language/Haskell/Liquid/Bare/Expand.hs @@ -28,11 +28,13 @@ import Data.Maybe import Control.Monad +import Control.Monad.Identity import Control.Monad.State import Data.Bifunctor (second) import Data.Functor ((<&>)) import qualified Control.Exception as Ex import qualified Data.HashMap.Strict as M +import qualified Data.HashSet as HS import qualified Data.Char as Char import qualified Data.List as L import qualified Text.PrettyPrint.HughesPJ as PJ @@ -51,8 +53,10 @@ import Language.Haskell.Liquid.Types.RTypeOp import Language.Haskell.Liquid.Types.Specs import Language.Haskell.Liquid.Types.Types +import Language.Haskell.Liquid.LHNameResolution (symbolToLHName) import qualified Language.Haskell.Liquid.Misc as Misc import qualified Language.Haskell.Liquid.Measure as Ms +import Language.Haskell.Liquid.Name.LogicNameEnv (LogicNameEnv(..)) import qualified Language.Haskell.Liquid.Bare.Resolve as Bare import qualified Language.Haskell.Liquid.Bare.Types as Bare import qualified Language.Haskell.Liquid.Bare.Plugged as Bare @@ -64,40 +68,53 @@ -- that is, the below needs to be called *before* we use `Expand.expand` -------------------------------------------------------------------------------- makeRTEnv - :: Bare.Env + :: LogicNameEnv -> ModName -> Ms.BareSpec -> [(ModName, Ms.BareSpec)] - -> LogicMap -> BareRTEnv -------------------------------------------------------------------------------- -makeRTEnv env modName mySpec dependencySpecs lmap +makeRTEnv lenv modName mySpec dependencySpecs = renameRTArgs $ makeRTAliases tAs $ makeREAliases eAs where - tAs = [ t | (_, s) <- specs, t <- Ms.aliases s ] - eAs = [ e | (_m, s) <- specs, e <- Ms.ealiases s ] - ++ if typeclass (getConfig env) then [] - -- lmap expansion happens during elaboration - -- this clearly breaks things if a signature - -- contains lmap functions but never gets - -- elaborated - else [ e | (_, xl) <- M.toList (lmSymDefs lmap) - , let e = lmapEAlias xl ] + tAs = concatMap (Ms.aliases . snd) specs + eAs = concatMap (getLHNameExprAliases . snd) specs specs = (modName, mySpec) : dependencySpecs + -- | 'Symbol's are temporarily converted to 'LHName's in expression alias + -- bodies to use the same lookup and expansion procedure for both + -- kinds of aliases. Implemented as an specialization of + -- 'toBareSpecLHName' for the expression aliases field. + getLHNameExprAliases:: Ms.BareSpec -> [RTAlias F.Symbol (ExprV LHName)] + getLHNameExprAliases = runIdentity . go + + go :: Ms.BareSpec -> Identity [RTAlias F.Symbol (ExprV LHName)] + go = mapM (emapRTAlias (\e -> emapExprVM (symToLHName . (++ e)))) . ealiases + + symToLHName = symbolToLHName "makeRTEnv" lenv unhandledNames + unhandledNames = HS.fromList $ map fst $ expSigs mySpec + -- | We apply @renameRTArgs@ *after* expanding each alias-definition, to -- ensure that the substitutions work properly (i.e. don't miss expressions -- hidden inside @RExprArg@ or as strange type parameters. renameRTArgs :: BareRTEnv -> BareRTEnv renameRTArgs rte = RTE - { typeAliases = M.map (fmap (renameTys . renameVV . renameRTVArgs)) (typeAliases rte) - , exprAliases = M.map (fmap renameRTVArgs) (exprAliases rte) + { typeAliases = M.map (renameTys . renameVV . renameRTVArgs) (typeAliases rte) + , exprAliases = M.map renameRTVArgs (exprAliases rte) } -makeREAliases :: [Located (RTAlias F.Symbol F.Expr)] -> BareRTEnv +-- | Recursively expands expression aliases by unfolding the definitions of all +-- inner aliases and adds them to the environment. +-- Innermost aliases are unfolded and added first, and an error is thrown if +-- cyclic dependencies are detected. +makeREAliases :: [RTAlias F.Symbol (F.ExprV LHName)] -> BareRTEnv makeREAliases = graphExpand buildExprEdges f mempty where - f rtEnv xt = setREAlias rtEnv (expandLoc rtEnv xt) + f rtEnv xt = setREAlias rtEnv (expand rtEnv (F.loc . rtName $ xt) (lhNametoSymbol xt)) + -- Expression aliases 'LHName's are transformed back to 'Symbol's for the + -- actual expansion to take place and to be stored in the environment. + lhNametoSymbol :: RTAlias F.Symbol (F.ExprV LHName) -> RTAlias F.Symbol Expr + lhNametoSymbol xt = (fmap $ fmap lhNameToResolvedSymbol) xt -- | @renameTys@ ensures that @RTAlias@ type parameters have distinct names @@ -106,7 +123,7 @@ renameTys rt = rt { rtTArgs = ys, rtBody = sbts (rtBody rt) (zip xs ys) } where xs = rtTArgs rt - ys = (`F.suffixSymbol` rtName rt) <$> xs + ys = (`F.suffixSymbol` (lhNameToUnqualifiedSymbol . val . rtName $ rt)) <$> xs sbts = foldl (flip subt) @@ -126,65 +143,78 @@ oldArgs = rtVArgs rt rtArg x i = F.suffixSymbol x (F.intSymbol "rta" i) -makeRTAliases :: [Located (RTAlias F.Symbol BareType)] -> BareRTEnv -> BareRTEnv +-- | Recursively expands type aliases by unfolding the definitions of all inner +-- aliases and adds them to the environment. +-- Innermost aliases are unfolded and added first, and an error is thrown if +-- cyclic dependencies are detected. +-- Note that when called from 'makeRTEnv', the input environment contains only +-- expanded expression aliases. +makeRTAliases :: [RTAlias F.Symbol BareType] -> BareRTEnv -> BareRTEnv makeRTAliases lxts rte = graphExpand buildTypeEdges f rte lxts where - f rtEnv xt = setRTAlias rtEnv (expandLoc rtEnv xt) + f rtEnv xt = setRTAlias rtEnv (expand rtEnv (F.loc . rtName $ xt) xt) -------------------------------------------------------------------------------------------------------------- +-- | Builds a directed graph of aliases, checks for cyclic dependencies, +-- reorders them so that inner aliases are processed first, and folds over +-- the graph to add each expanded node to the environment. graphExpand :: (PPrint t) - => (AliasTable x t -> t -> [F.Symbol]) -- ^ dependencies - -> (thing -> Located (RTAlias x t) -> thing) -- ^ update + => (AliasTable x t -> t -> [LHName]) -- ^ dependencies + -> (thing -> RTAlias x t -> thing) -- ^ update -> thing -- ^ initial - -> [Located (RTAlias x t)] -- ^ vertices + -> [RTAlias x t] -- ^ vertices -> thing -- ^ final graphExpand buildEdges expBody env lxts = L.foldl' expBody env (genExpandOrder table' graph) where - -- xts = val <$> lxts table = buildAliasTable lxts graph = buildAliasGraph (buildEdges table) lxts table' = checkCyclicAliases table graph -setRTAlias :: RTEnv x t -> Located (RTAlias x t) -> RTEnv x t +-- | Inserts a type alias into the environment. +setRTAlias :: RTEnv x t -> RTAlias x t -> RTEnv x t setRTAlias env a = env { typeAliases = M.insert n a (typeAliases env) } where - n = rtName (val a) + n = val . rtName $ a -setREAlias :: RTEnv x t -> Located (RTAlias F.Symbol F.Expr) -> RTEnv x t +-- | Inserts an expression alias into the environment. +setREAlias :: RTEnv x t -> RTAlias F.Symbol F.Expr -> RTEnv x t setREAlias env a = env { exprAliases = M.insert n a (exprAliases env) } where - n = rtName (val a) - - + n = val . rtName $ a -------------------------------------------------------------------------------- -type AliasTable x t = M.HashMap F.Symbol (Located (RTAlias x t)) -buildAliasTable :: [Located (RTAlias x t)] -> AliasTable x t -buildAliasTable = M.fromList . map (\rta -> (rtName (val rta), rta)) +type AliasTable x t = M.HashMap LHName (RTAlias x t) -fromAliasSymbol :: AliasTable x t -> F.Symbol -> Located (RTAlias x t) -fromAliasSymbol table sym - = fromMaybe err (M.lookup sym table) +buildAliasTable :: [RTAlias x t] -> AliasTable x t +buildAliasTable = M.fromList . map (\rta -> (val . rtName $ rta, rta)) + +fromAliasLHName :: AliasTable x t -> LHName -> RTAlias x t +fromAliasLHName table lhname + = fromMaybe err (M.lookup lhname table) where - err = panic Nothing ("fromAliasSymbol: Dangling alias symbol: " ++ show sym) + err = panic Nothing ("fromAliasLHName: Dangling alias name: " ++ show lhname) +-- | An adjacency list of nodes representing a directed graph. +-- Used to detect cyclic alias dependencies and to order the expansion +-- of aliases. type Graph t = [Node t] +-- | A node described by a label, a key, and a list of connected nodes, +-- all parameterized by the same type. This type is used to represent +-- aliases nested within other aliases. type Node t = (t, t, [t]) -buildAliasGraph :: (PPrint t) => (t -> [F.Symbol]) -> [Located (RTAlias x t)] - -> Graph F.Symbol -buildAliasGraph buildEdges = map (buildAliasNode buildEdges) - -buildAliasNode :: (PPrint t) => (t -> [F.Symbol]) -> Located (RTAlias x t) - -> Node F.Symbol -buildAliasNode f la = (rtName a, rtName a, f (rtBody a)) +buildAliasGraph :: (PPrint t) => (t -> [LHName]) -> [RTAlias x t] + -> Graph LHName +buildAliasGraph buildEdges = map (buildNode buildEdges) where - a = val la + buildNode :: (PPrint t) => (t -> [LHName]) -> RTAlias x t + -> Node LHName + buildNode f a = (val . rtName $ a, val . rtName $ a, f (rtBody a)) -checkCyclicAliases :: AliasTable x t -> Graph F.Symbol -> AliasTable x t +checkCyclicAliases :: AliasTable x t -> Graph LHName -> AliasTable x t checkCyclicAliases table graph = case mapMaybe go (stronglyConnComp graph) of [] -> table @@ -193,34 +223,32 @@ go (CyclicSCC vs) = Just vs go (AcyclicSCC _) = Nothing -cycleAliasErr :: AliasTable x t -> [F.Symbol] -> Error -cycleAliasErr _ [] = panic Nothing "checkCyclicAliases: No type aliases in reported cycle" -cycleAliasErr t symList@(rta:_) = ErrAliasCycle { pos = fst (locate rta) - , acycle = map locate symList } +cycleAliasErr :: AliasTable x t -> [LHName] -> Error +cycleAliasErr _ [] = panic Nothing "checkCyclicAliases: No aliases in reported cycle" +cycleAliasErr t nameList@(name:_) = ErrAliasCycle { pos = fst (locate name) + , acycle = map locate nameList } where - locate sym = ( GM.fSrcSpan $ fromAliasSymbol t sym - , pprint sym ) - + locate n = ( GM.fSrcSpan . rtName $ fromAliasLHName t n + , pprint n ) -genExpandOrder :: AliasTable x t -> Graph F.Symbol -> [Located (RTAlias x t)] +-- | Orders aliases so that nested ones are processed first. +genExpandOrder :: AliasTable x t -> Graph LHName -> [RTAlias x t] genExpandOrder table graph - = map (fromAliasSymbol table) symOrder + = map (fromAliasLHName table) nameOrder where (digraph, lookupVertex, _) = graphFromEdges graph - symOrder + nameOrder = map (Misc.fst3 . lookupVertex) $ reverse $ topSort digraph -------------------------------------------------------------------------------- -ordNub :: Ord a => [a] -> [a] -ordNub = map head . L.group . L.sort - -buildTypeEdges :: AliasTable x t -> BareType -> [F.Symbol] -buildTypeEdges table = ordNub . go +-- | Gathers all constructor names within a the body of a type alias +-- that match a key from the type 'AliasTable'. +buildTypeEdges :: AliasTable x t -> BareType -> [LHName] +buildTypeEdges table = Misc.ordNub . go where - -- go :: t -> [Symbol] - go (RApp c ts rs _) = go_alias (getLHNameSymbol $ val $ btc_tc c) ++ concatMap go ts ++ concatMap go (mapMaybe go_ref rs) + go (RApp c ts rs _) = go_alias (val $ btc_tc c) ++ concatMap go ts ++ concatMap go (mapMaybe go_ref rs) go (RFun _ _ t1 t2 _) = go t1 ++ go t2 go (RAppTy t1 t2 _) = go t1 ++ go t2 go (RAllE _ t1 t2) = go t1 ++ go t2 @@ -235,10 +263,11 @@ go_ref (RProp _ (RHole _)) = Nothing go_ref (RProp _ t) = Just t -buildExprEdges :: M.HashMap F.Symbol a -> F.Expr -> [F.Symbol] -buildExprEdges table = ordNub . go +-- | Gathers all variable names within the body of an expression alias +-- that match a key from the expression 'AliasTable'. +buildExprEdges :: AliasTable x t -> F.ExprV LHName -> [LHName] +buildExprEdges table = Misc.ordNub . go where - go :: F.Expr -> [F.Symbol] go (EApp e1 e2) = go e1 ++ go e2 go (ENeg e) = go e go (EBin _ e1 e2) = go e1 ++ go e2 @@ -254,13 +283,13 @@ go (PIff p q) = go p ++ go q go (PAll _ p) = go p go (ELam _ e) = go e + go (ELet _ e1 e2) = go e1 ++ go e2 go (ECoerc _ _ e) = go e go (PAtom _ e1 e2) = go e1 ++ go e2 go (ETApp e _) = go e go (ETAbs e _) = go e go (PKVar _ _) = [] go (PExist _ e) = go e - go (PGrad _ _ _ e) = go e go_alias f = [f | M.member f table ] @@ -398,11 +427,11 @@ go t@RExprArg{} = t goRef (RProp ss t) = RProp (map (expand rtEnv l <$>) ss) (go t) -lookupRTEnv :: BTyCon -> BareRTEnv -> Maybe (Located BareRTAlias) -lookupRTEnv c rtEnv = M.lookup (getLHNameSymbol $ val $ btc_tc c) (typeAliases rtEnv) +lookupRTEnv :: BTyCon -> BareRTEnv -> Maybe BareRTAlias +lookupRTEnv c rtEnv = M.lookup (val $ btc_tc c) (typeAliases rtEnv) -expandRTAliasApp :: F.SourcePos -> Located BareRTAlias -> [BareType] -> RReft -> BareType -expandRTAliasApp l (Loc la _ rta) args r = case isOK of +expandRTAliasApp :: F.SourcePos -> BareRTAlias -> [BareType] -> RReft -> BareType +expandRTAliasApp l rta@(RTA {rtName = Loc la _ _}) args r = case isOK of Just e -> Ex.throw e Nothing -> F.subst esu . (`RT.strengthen` r) . RT.subsTyVarsMeet tsu $ rtBody rta where @@ -466,8 +495,9 @@ ---------------------------------------------------------------------------------------- cookSpecType :: Bare.Env -> Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> LocBareType -> LocSpecType -cookSpecType env sigEnv name x bt - = either Ex.throw id (cookSpecTypeE env sigEnv name x bt) +cookSpecType env sigEnv name x bt = + either Ex.throw id $ + cookSpecTypeE env sigEnv name x bt where _msg = "cookSpecType: " ++ GM.showPpr (z, Ghc.varType <$> z) z = Bare.plugSrc x @@ -480,7 +510,8 @@ cookSpecTypeE env sigEnv name@(ModName _ _) x bt = fmap f . bareSpecType env $ bareExpandType rtEnv bt where - f = (if doplug || not allowTC then plugHoles allowTC sigEnv name x else id) + f :: LocSpecType -> LocSpecType + f = (if doplug || not allowTC then plugHoles allowTC sigEnv name x else id) . fmap (RT.addTyConInfo embs tyi) . Bare.txRefSort tyi embs . fmap txExpToBind -- What does this function DO @@ -510,7 +541,7 @@ generalizeWith _ t = RT.generalize t generalizeVar :: Ghc.Var -> SpecType -> SpecType -generalizeVar v t = mkUnivs (zip as (repeat mempty)) [] t +generalizeVar v t = mkUnivs [(a, mempty) | a <- as] [] t where as = filter isGen (RT.freeTyVars t) (vas,_) = Ghc.splitForAllTyCoVars (GM.expandVarType v) @@ -529,21 +560,24 @@ specExpandType = expandLoc bareSpecType :: Bare.Env -> LocBareType -> Bare.Lookup LocSpecType -bareSpecType env bt = case Bare.ofBareTypeE env (F.loc bt) Nothing (val bt) of - Left e -> Left e - Right t -> Right (F.atLoc bt t) +bareSpecType env bt = + case Bare.ofBareTypeE env (F.loc bt) Nothing (val bt) of + Left e -> Left e + Right t -> Right (F.atLoc bt t) maybePlug :: Bool -> Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> LocSpecType -> LocSpecType -maybePlug allowTC sigEnv name kx = case Bare.plugSrc kx of - Nothing -> id - Just _ -> plugHoles allowTC sigEnv name kx +maybePlug allowTC sigEnv name kx = + case Bare.plugSrc kx of + Nothing -> id + Just _ -> plugHoles allowTC sigEnv name kx plugHoles :: Bool -> Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> LocSpecType -> LocSpecType -plugHoles allowTC sigEnv name = Bare.makePluggedSig allowTC name embs tyi exports +plugHoles allowTC sigEnv name = + Bare.makePluggedSig allowTC name embs tyi exports where - embs = Bare.sigEmbs sigEnv - tyi = Bare.sigTyRTyMap sigEnv - exports = Bare.sigExports sigEnv + embs = Bare.sigEmbs sigEnv + tyi = Bare.sigTyRTyMap sigEnv + exports = Bare.sigExports sigEnv {- [NOTE:Cooking-SpecType] A @SpecType@ is _raw_ when it is obtained directly from a @BareType@, i.e. @@ -610,6 +644,7 @@ go (PAll xs p) = PAll xs (go p) go (PExist xs p) = PExist xs (go p) go (ELam xt e) = ELam xt (go e) + go (ELet x e1 e2) = ELet x (go e1) (go e2) go (ECoerc a t e) = ECoerc a t (go e) go (ETApp e s) = ETApp (go e) s go (ETAbs e s) = ETAbs (go e) s @@ -618,7 +653,6 @@ go (PIff e1 e2) = PIff (go e1) (go e2) go (PAtom b e1 e2) = PAtom b (go e1) (go e2) go (EIte p e1 e2) = EIte (go p)(go e1) (go e2) - go (PGrad k su i e) = PGrad k su i (go e) go e@(PKVar _ _) = e go e@(ESym _) = e go e@(ECon _) = e @@ -637,7 +671,7 @@ Just re -> expandApp l re es' Nothing -> F.eApps (EVar f) es' where - eAs = exprAliases rtEnv + eAs = M.mapKeys lhNameToResolvedSymbol $ exprAliases rtEnv mBody = M.lookup f eAs `mplus` M.lookup (GM.dropModuleUnique f) eAs es' = expandExpr rtEnv l <$> es _f0 = GM.dropModuleNamesAndUnique f @@ -647,18 +681,17 @@ -------------------------------------------------------------------------------- -- | Expand Alias Application -------------------------------------------------- -------------------------------------------------------------------------------- -expandApp :: F.Subable ty => F.SourcePos -> Located (RTAlias F.Symbol ty) -> [Expr] -> ty -expandApp l lre es +expandApp :: F.Subable ty => F.SourcePos -> RTAlias F.Symbol ty -> [Expr] -> ty +expandApp l re es | Just su <- args = F.subst su (rtBody re) | otherwise = Ex.throw err where - re = F.val lre args = F.mkSubst <$> Misc.zipMaybe (rtVArgs re) es err :: UserError err = ErrAliasApp sp alias sp' msg sp = GM.sourcePosSrcSpan l alias = pprint (rtName re) - sp' = GM.fSrcSpan lre -- sourcePosSrcSpan (rtPos re) + sp' = GM.fSrcSpan . rtName $ re msg = "expects" PJ.<+> pprint (length $ rtVArgs re) PJ.<+> "arguments but it is given" PJ.<+> pprint (length es) @@ -669,7 +702,8 @@ ------------------------------------------------------------------------------- txExpToBind :: SpecType -> SpecType ------------------------------------------------------------------------------- -txExpToBind t = evalState (expToBindT t) (ExSt 0 M.empty πs) +txExpToBind t = + evalState (expToBindT t) (ExSt 0 M.empty πs) where πs = M.fromList [(pname p, p) | p <- ty_preds $ toRTypeRep t ] diff --git a/src/Language/Haskell/Liquid/Bare/Measure.hs b/src/Language/Haskell/Liquid/Bare/Measure.hs --- a/src/Language/Haskell/Liquid/Bare/Measure.hs +++ b/src/Language/Haskell/Liquid/Bare/Measure.hs @@ -402,7 +402,7 @@ concat (tycDCons `Mb.mapMaybe` (dataDecls spec ++ newtyDecls spec)) getFromDataCtor decl = S.fromList $ map lhNameToResolvedSymbol $ val (dcName decl) : (fst <$> dcFields decl) - getAliases spec = S.fromList $ rtName . val <$> Ms.ealiases spec + getAliases spec = S.fromList $ lhNameToUnqualifiedSymbol . val . rtName <$> Ms.ealiases spec -- Get the set of `DataCon`s (DCs) needed for the reflection of a given list of variables, -- and which are not already present in the logic diff --git a/src/Language/Haskell/Liquid/Bare/Misc.hs b/src/Language/Haskell/Liquid/Bare/Misc.hs --- a/src/Language/Haskell/Liquid/Bare/Misc.hs +++ b/src/Language/Haskell/Liquid/Bare/Misc.hs @@ -108,7 +108,8 @@ -- Renaming Type Variables in Haskell Signatures ------------------------------ ------------------------------------------------------------------------------- runMapTyVars :: Bool -> Type -> SpecType -> (PJ.Doc -> PJ.Doc -> Error) -> Either Error MapTyVarST -runMapTyVars allowTC τ t err = execStateT (mapTyVars allowTC τ t) (MTVST [] err) +runMapTyVars allowTC τ t err = + execStateT (mapTyVars allowTC τ t) (MTVST [] err) data MapTyVarST = MTVST { vmap :: [(Var, RTyVar)] @@ -141,8 +142,8 @@ mapTyVars _ _ (RExprArg _) = return () mapTyVars allowTC (AppTy τ τ') (RAppTy t t' _) - = do mapTyVars allowTC τ t - mapTyVars allowTC τ' t' + = do mapTyVars allowTC τ t + mapTyVars allowTC τ' t' mapTyVars _ _ (RHole _) = return () mapTyVars _ k _ | isKind k @@ -154,8 +155,10 @@ throwError (err (F.pprint hsT) (F.pprint lqT)) isKind :: Kind -> Bool -isKind = isTYPEorCONSTRAINT -- TODO:GHC-863 isStarKind k -- typeKind k - +isKind k = isTYPEorCONSTRAINT k -- TODO:GHC-863 isStarKind k -- typeKind k + || case k of + TyVarTy kk -> varType kk == Ghc.liftedTypeKind + _ -> False mapTyRVar :: MonadError Error m => Var -> RTyVar -> MapTyVarST -> m MapTyVarST diff --git a/src/Language/Haskell/Liquid/Bare/Plugged.hs b/src/Language/Haskell/Liquid/Bare/Plugged.hs --- a/src/Language/Haskell/Liquid/Bare/Plugged.hs +++ b/src/Language/Haskell/Liquid/Bare/Plugged.hs @@ -282,7 +282,9 @@ -- zipWithDefM: if ts and ts' have different length then the liquid and haskell types are different. -- keep different types for now, as a pretty error message will be created at Bare.Check go (RApp _ ts _ _) (RApp c ts' p r) - | length ts == length ts' = RApp c (Misc.zipWithDef go ts $ Bare.matchKindArgs ts ts') p r + -- Removing length check because Haskell types can contain kinds which is safe based on the comment above + -- | length ts == length ts' + = RApp c (Misc.zipWithDef go ts $ Bare.matchKindArgs ts ts') p r go hsT lqT = Ex.throw (err (F.pprint hsT) (F.pprint lqT)) -- otherwise = Ex.throw err diff --git a/src/Language/Haskell/Liquid/Bare/Resolve.hs b/src/Language/Haskell/Liquid/Bare/Resolve.hs --- a/src/Language/Haskell/Liquid/Bare/Resolve.hs +++ b/src/Language/Haskell/Liquid/Bare/Resolve.hs @@ -188,7 +188,7 @@ -- | @lookupLocalVar@ takes as input the list of "global" (top-level) vars -- that also match the name @lx@; we then pick the "closest" definition. --- See tests/names/LocalSpec.hs for a motivating example. +-- See tests/names/pos/LocalSpec.hs for a motivating example. lookupLocalVar :: F.Loc a => LocalVars -> LocSymbol -> [a] -> Maybe (Either a Ghc.Var) lookupLocalVar localVars lx gvs = findNearest lxn kvs diff --git a/src/Language/Haskell/Liquid/Bare/Typeclass.hs b/src/Language/Haskell/Liquid/Bare/Typeclass.hs --- a/src/Language/Haskell/Liquid/Bare/Typeclass.hs +++ b/src/Language/Haskell/Liquid/Bare/Typeclass.hs @@ -348,7 +348,7 @@ ptys = [(F.vv (Just i), classRFInfo True, pty, mempty) | (i,pty) <- zip [0,1..] isPredSpecTys] fullSig = mkArrow - (zip isRTvs (repeat mempty)) + [(bRTV, mempty) | bRTV <- isRTvs] [] ptys . subst (zip clsTvs isSpecTys) $ diff --git a/src/Language/Haskell/Liquid/Constraint/Env.hs b/src/Language/Haskell/Liquid/Constraint/Env.hs --- a/src/Language/Haskell/Liquid/Constraint/Env.hs +++ b/src/Language/Haskell/Liquid/Constraint/Env.hs @@ -113,7 +113,7 @@ lookupREnv x rE = msum $ M.lookup x <$> renvMaps rE memberREnv :: F.Symbol -> REnv -> Bool -memberREnv x rE = or $ M.member x <$> renvMaps rE +memberREnv x rE = any (M.member x) (renvMaps rE) globalREnv :: REnv -> REnv globalREnv (REnv gM lM) = REnv gM' M.empty diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs --- a/src/Language/Haskell/Liquid/Constraint/Generate.hs +++ b/src/Language/Haskell/Liquid/Constraint/Generate.hs @@ -7,6 +7,7 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE NamedFieldPuns #-} {-# OPTIONS_GHC -Wno-orphans #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} @@ -28,8 +29,9 @@ import qualified Language.Haskell.Liquid.GHC.SpanStack as Sp import qualified Language.Haskell.Liquid.GHC.Misc as GM -- ( isInternal, collectArguments, tickSrcSpan, showPpr ) import Text.PrettyPrint.HughesPJ ( text ) -import Control.Monad ( foldM, forM, forM_, when, void ) +import Control.Monad ( foldM, forM, forM_, when, void, unless) import Control.Monad.State +import Data.Bifunctor (first) import Data.Maybe (fromMaybe, isJust, mapMaybe) import Data.Either.Extra (eitherToMaybe) import qualified Data.HashMap.Strict as M @@ -67,7 +69,7 @@ import Language.Haskell.Liquid.Bare.DataType (dataConMap, makeDataConChecker) import Language.Haskell.Liquid.UX.Config ( HasConfig(getConfig), - Config(typeclass, gradual, checkDerived, extensionality, + Config(typeclass, checkDerived, extensionality, nopolyinfer, noADT, dependantCase, exactDC, rankNTypes), patternFlag, higherOrderFlag ) @@ -86,7 +88,6 @@ consAct γ cfg info = do let sSpc = gsSig . giSpec $ info let gSrc = giSrc info - when (gradual cfg) (mapM_ (addW . WfC γ . val . snd) (gsTySigs sSpc ++ gsAsmSigs sSpc)) γ' <- foldM (consCBTop cfg info) γ (giCbs gSrc) -- Relational Checking: the following only runs when the list of relational specs is not empty (ψ, γ'') <- foldM (consAssmRel cfg info) ([], γ') (gsAsmRel sSpc ++ gsRelation sSpc) @@ -97,11 +98,107 @@ hws <- gets hsWfs fcs <- concat <$> mapM (splitC (typeclass (getConfig info))) hcs fws <- concat <$> mapM splitW hws + checkStratCtors γ sSpc modify $ \st -> st { fEnv = fEnv st `mappend` feEnv (fenv γ) , cgLits = litEnv γ , cgConsts = cgConsts st `mappend` constEnv γ , fixCs = fcs , fixWfs = fws } + + +--------------------------------- +-- | Checking stratified ctors -- +--------------------------------- +type FExpr = F.ExprV F.Symbol +type Ctors = S.HashSet F.Symbol + +checkStratCtors :: CGEnv -> GhcSpecSig -> CG () +checkStratCtors env sSpc = do + let ctors = S.fromList $ M.keys $ F.seBinds $ constEnv env + let ctorRefinements = filter (isStrat . fst) $ gsTySigs sSpc + forM_ ctorRefinements $ uncurry $ checkCtor ctors + where + -- (Alecs): For some reason it can't see that they are the same + -- GHC name, probably is due to some worker wrapper shenannigans + hack = occNameString . nameOccName + isStrat nm = hack (varName nm) `elem` map hack (gsStratCtos sSpc) + +uncurryPi :: SpecType -> ([SpecType], SpecType) +uncurryPi (RFun _ _ dom cod _) = first (dom :) $ uncurryPi cod +uncurryPi rest = ([], rest) + +getTyConName :: SpecType -> Name +getTyConName a = Ghc.tyConName $ rtc_tc $ rt_tycon a + +checkCtor :: Ctors -> Var -> LocSpecType -> CG () +checkCtor ctors name typ = do + let loc = GM.fSrcSpan $ F.loc typ + let (args, ret) = uncurryPi $ val typ + -- The constuctor that we want not to appear negatively + let tyName = getTyConName ret + -- Its index information + retIdx <- case getPropIndex $ ur_reft $ rt_reft ret of + Just idx -> pure idx + Nothing -> uError $ ErrStratNotPropRet loc (pprint tyName) (pprint name) (F.pprint ret) + -- For every argument of the constructor we check that all the + -- self-refernce are refined by a "smaller" `prop` annotation + forM_ args $ checkNg ctors loc name tyName retIdx + +checkNg :: Ctors -> SrcSpan -> Var -> Name -> FExpr -> SpecType -> CG () +checkNg ctors loc ctorName tyName retIdx = go + where + go :: SpecType -> CG () + go RVar {} = pure () + go RAllT { rt_ty } = go rt_ty + go RAllP { rt_ty } = go rt_ty + go RFun { rt_in, rt_out } = do + go rt_in + go rt_out + go r@RApp { rt_tycon = RTyCon { rtc_tc }, rt_args, rt_reft } = do + if Ghc.tyConName rtc_tc == tyName then do + case getPropIndex $ ur_reft rt_reft of + (Just arg) -> do + -- We compare index information The occurrence is safe + -- iff the index of the return type is strictly bigger + -- than the one in negative position + unless (isStructurallySmaller ctors arg retIdx) $ do + uError $ ErrStratIdxNotSmall loc + (pprint tyName) (pprint ctorName) (F.pprint retIdx) (F.pprint arg) + -- We don't have index information for both so we bail + _ -> uError $ ErrStratOccProp loc (pprint tyName) (pprint ctorName) (F.pprint r) + else do + forM_ rt_args go + go _ = lift $ impossible (Just loc) "checkNg unexpected type" + + +isStructurallySmaller :: Ctors -> FExpr -> FExpr -> Bool +isStructurallySmaller ctors l r + -- Congruence rule + | (F.EVar nl, argsl) <- F.splitEAppThroughECst l + , (F.EVar nr, argsr) <- F.splitEAppThroughECst r + , nl == nr + , length argsl == length argsr + , nl `elem` ctors + = lexOrder ctors argsl argsr + | otherwise = isSubterm ctors l r && l /= r + +lexOrder :: Ctors -> [F.ExprV F.Symbol] -> [F.ExprV F.Symbol] -> Bool +lexOrder _ [] [] = False +lexOrder ctors (l:ls) (r:rs) + | isStructurallySmaller ctors l r = True + | l == r = lexOrder ctors ls rs + | otherwise = False +lexOrder _ _ _ = errorP "" "lexOrder: different length lists" + +isSubterm :: Ctors -> FExpr -> FExpr -> Bool +isSubterm ctors l r | l == r + = True + -- Congruence rule + | (F.EVar nm, args) <- F.splitEAppThroughECst r + , nm `elem` ctors + = any (isSubterm ctors l) args + | otherwise + = False -------------------------------------------------------------------------------- -- | Ensure that the instance type is a subtype of the class type -------------- diff --git a/src/Language/Haskell/Liquid/Constraint/Qualifier.hs b/src/Language/Haskell/Liquid/Constraint/Qualifier.hs --- a/src/Language/Haskell/Liquid/Constraint/Qualifier.hs +++ b/src/Language/Haskell/Liquid/Constraint/Qualifier.hs @@ -9,7 +9,7 @@ where import Prelude hiding (error) -import Data.List (delete, nub) +import Data.List (delete, nub, partition) import Data.Maybe (isJust, catMaybes, fromMaybe, isNothing) import qualified Data.HashSet as S import qualified Data.HashMap.Strict as M @@ -18,6 +18,7 @@ import Language.Fixpoint.Types hiding (panic, mkQual) import qualified Language.Fixpoint.Types.Config as FC +import Language.Fixpoint.Misc (fst3) import Language.Fixpoint.SortCheck import Language.Haskell.Liquid.Types.RefType import Language.Haskell.Liquid.GHC.Misc (getSourcePos) @@ -31,7 +32,7 @@ import Language.Haskell.Liquid.Types.Specs import Language.Haskell.Liquid.Types.Types import Language.Haskell.Liquid.UX.Config -import Language.Fixpoint.Types.Config (ElabFlags) +import Language.Fixpoint.Types.Config (ElabFlags) -------------------------------------------------------------------------------- @@ -39,10 +40,16 @@ -------------------------------------------------------------------------------- giQuals info lEnv = notracepp ("GI-QUALS: " ++ showpp lEnv) - $ condNull (useSpcQuals info) (gsQualifiers . gsQual . giSpec $ info) + $ currentSpec + ++ condNull (useSpcQuals info) otherSpecs ++ condNull (useSigQuals info) (sigQualifiers info lEnv) ++ condNull (useAlsQuals info) (alsQualifiers info lEnv) + where + (currentSpec, otherSpecs) = partition isQualifierFromCurrentModule (gsQualifiers . gsQual . giSpec $ info) + isQualifierFromCurrentModule qual = + fst3 (sourcePosElts (qPos qual)) == giTarget (giSrc info) + -- -------------------------------------------------------------------------------- -- qualifiers :: GhcInfo -> SEnv Sort -> [Qualifier] -- -------------------------------------------------------------------------------- @@ -84,10 +91,22 @@ , validQual lEnv q ] where - ef = maybe (FC.ElabFlags False) FC.solverFlags . smtsolver . getConfig $ info + ef = elabFlag info k = maxQualParams info tce = gsTcEmbeds . gsName . giSpec $ info +elabFlag :: (HasConfig t) => t -> FC.ElabFlags +elabFlag info = FC.ElabFlags setBag False + where + setBag = maybe False elabSetBag . smtsolver . getConfig $ info + elabSetBag :: FC.SMTSolver -> Bool + elabSetBag FC.Z3 = True + elabSetBag FC.Z3mem = True + elabSetBag _ = False + + + + validQual :: SEnv Sort -> Qualifier -> Bool validQual lEnv q = isJust $ checkSortExpr (srcSpan q) env (qBody q) where @@ -107,7 +126,7 @@ , length (qParams q) <= k + 1 ] where - ef = maybe (FC.ElabFlags False) FC.solverFlags . smtsolver . getConfig $ info + ef = elabFlag info k = maxQualParams info tce = gsTcEmbeds . gsName . giSpec $ info @@ -180,7 +199,6 @@ = [ mkQ' v so pa | let (RR so (Reft (v, ra))) = rTypeSortedReft tce rrt , pa <- conjuncts ra , not $ isHole pa - , not $ isGradual pa , notracepp ("refTopQuals: " ++ showpp pa) $ isNothing $ runReader (checkSorted (srcSpan l) (insertSEnv v so γ') pa) ef ] diff --git a/src/Language/Haskell/Liquid/Constraint/Relational.hs b/src/Language/Haskell/Liquid/Constraint/Relational.hs --- a/src/Language/Haskell/Liquid/Constraint/Relational.hs +++ b/src/Language/Haskell/Liquid/Constraint/Relational.hs @@ -559,13 +559,13 @@ γ'' <- γ' += ("consRelSub Base R", rr, t2) let cstr = F.subst (F.mkSubst [(resL, F.EVar rl), (resR, F.EVar rr)]) $ F.PImp p1 p2 entl γ'' (traceWhenLoud ("consRelSub Base cstr " ++ F.showpp cstr) cstr) "consRelSub Base" -consRelSub _ t1@(RHole _) t2@(RHole _) _ _ = F.panic $ "consRelSub is undefined for RHole " ++ show (t1, t2) +consRelSub _ t1@(RHole _) t2@(RHole _) _ _ = F.panic $ "consRelSub is undefined for RHole " ++ show (t1, t2) consRelSub _ t1@(RExprArg _) t2@(RExprArg _) _ _ = F.panic $ "consRelSub is undefined for RExprArg " ++ show (t1, t2) -consRelSub _ t1@REx {} t2@REx {} _ _ = F.panic $ "consRelSub is undefined for REx " ++ show (t1, t2) -consRelSub _ t1@RAllE {} t2@RAllE {} _ _ = F.panic $ "consRelSub is undefined for RAllE " ++ show (t1, t2) -consRelSub _ t1@RRTy {} t2@RRTy {} _ _ = F.panic $ "consRelSub is undefined for RRTy " ++ show (t1, t2) -consRelSub _ t1@RAllP {} t2@RAllP {} _ _ = F.panic $ "consRelSub is undefined for RAllP " ++ show (t1, t2) -consRelSub _ t1@RAllT {} t2@RAllT {} _ _ = F.panic $ "consRelSub is undefined for RAllT " ++ show (t1, t2) +consRelSub _ t1@REx {} t2@REx {} _ _ = F.panic $ "consRelSub is undefined for REx " ++ show (t1, t2) +consRelSub _ t1@RAllE {} t2@RAllE {} _ _ = F.panic $ "consRelSub is undefined for RAllE " ++ show (t1, t2) +consRelSub _ t1@RRTy {} t2@RRTy {} _ _ = F.panic $ "consRelSub is undefined for RRTy " ++ show (t1, t2) +consRelSub _ t1@RAllP {} t2@RAllP {} _ _ = F.panic $ "consRelSub is undefined for RAllP " ++ show (t1, t2) +consRelSub _ t1@RAllT {} t2@RAllT {} _ _ = F.panic $ "consRelSub is undefined for RAllT " ++ show (t1, t2) consRelSub _ t1 t2 _ _ = F.panic $ "consRelSub is undefined for different types " ++ show (t1, t2) -------------------------------------------------------------- diff --git a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs --- a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs +++ b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs @@ -27,11 +27,9 @@ import Language.Haskell.Liquid.UX.Config import Language.Haskell.Liquid.UX.DiffCheck (coreDefs, coreDeps, dependsOn, Def(..)) import qualified Language.Haskell.Liquid.GHC.Misc as GM -- (simplesymbol) -import qualified Data.List as L import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S -- import Language.Fixpoint.Misc -import qualified Language.Haskell.Liquid.Misc as Misc import Language.Haskell.Liquid.Types.Errors import Language.Haskell.Liquid.Types.RType @@ -41,37 +39,33 @@ fixConfig :: FilePath -> Config -> FC.Config fixConfig tgt cfg = def - { FC.solver = Mb.fromJust (smtsolver cfg) - , FC.linear = linear cfg - , FC.eliminate = eliminate cfg - , FC.nonLinCuts = not (higherOrderFlag cfg) -- eliminate cfg /= FC.All - , FC.save = saveQuery cfg - , FC.srcFile = tgt - , FC.cores = cores cfg - , FC.minPartSize = minPartSize cfg - , FC.maxPartSize = maxPartSize cfg - , FC.elimStats = elimStats cfg - , FC.elimBound = elimBound cfg - , FC.allowHO = higherOrderFlag cfg - , FC.allowHOqs = higherorderqs cfg - , FC.smtTimeout = smtTimeout cfg - , FC.stringTheory = stringTheory cfg - , FC.gradual = gradual cfg - , FC.ginteractive = ginteractive cfg - , FC.noslice = noslice cfg - , FC.rewriteAxioms = allowPLE cfg - , FC.pleWithUndecidedGuards = pleWithUndecidedGuards cfg - , FC.etabeta = etabeta cfg - , FC.localRewrites = dependantCase cfg - , FC.etaElim = not (exactDC cfg) && extensionality cfg -- SEE: https://github.com/ucsd-progsys/liquidhaskell/issues/1601 - , FC.extensionality = extensionality cfg - , FC.interpreter = interpreter cfg - , FC.oldPLE = oldPLE cfg - , FC.rwTerminationCheck = rwTerminationCheck cfg - , FC.noLazyPLE = noLazyPLE cfg - , FC.fuel = fuel cfg - , FC.noEnvironmentReduction = not (environmentReduction cfg) - , FC.inlineANFBindings = inlineANFBindings cfg + { FC.solver = Mb.fromJust (smtsolver cfg) + , FC.linear = linear cfg + , FC.eliminate = eliminate cfg + , FC.nonLinCuts = not (higherOrderFlag cfg) -- eliminate cfg /= FC.All + , FC.save = saveQuery cfg + , FC.srcFile = tgt + , FC.cores = cores cfg + , FC.minPartSize = minPartSize cfg + , FC.maxPartSize = maxPartSize cfg + , FC.elimStats = elimStats cfg + , FC.elimBound = elimBound cfg + , FC.allowHO = higherOrderFlag cfg + , FC.allowHOqs = higherorderqs cfg + , FC.smtTimeout = smtTimeout cfg + , FC.noStringTheory = not (stringTheory cfg) + , FC.noslice = noslice cfg + , FC.rewriteAxioms = allowPLE cfg + , FC.pleUndecGuards = pleWithUndecidedGuards cfg + , FC.etabeta = etabeta cfg + , FC.localRewrites = dependantCase cfg + , FC.etaElim = not (exactDC cfg) && extensionality cfg -- SEE: https://github.com/ucsd-progsys/liquidhaskell/issues/1601 + , FC.extensionality = extensionality cfg + , FC.interpreter = interpreter cfg + , FC.rwTermination = rwTerminationCheck cfg + , FC.fuel = fuel cfg + , FC.noEnvReduction = not (environmentReduction cfg) + , FC.inlineANFBinds = inlineANFBindings cfg } cgInfoFInfo :: TargetInfo -> CGInfo -> IO (F.FInfo Cinfo) @@ -80,11 +74,10 @@ targetFInfo :: TargetInfo -> CGInfo -> F.FInfo Cinfo targetFInfo info cgi = mappend (mempty { F.ae = ax, F.lrws = localRewrites cgi }) fi where - fi = F.fi cs ws bs ls consts ks qs bi aHO aHOqs es mempty adts ebs + fi = F.fi cs ws bs ls consts ks qs bi aHO aHOqs es mempty adts cs = fixCs cgi ws = fixWfs cgi bs = binds cgi - ebs = ebinds cgi ls = fEnv cgi consts = cgConsts cgi ks = kuts cgi @@ -104,10 +97,7 @@ (doExpand sp cfg <$> fcs) (makeRewrites info <$> fcs) where - eqs = if oldPLE cfg - then makeEquations (typeclass cfg) sp ++ map (uncurry $ specTypeEq emb) xts - else axioms - emb = gsTcEmbeds (gsName sp) + eqs = axioms cfg = getConfig info sp = giSpec info axioms = gsMyAxioms refl ++ gsImpAxioms refl @@ -213,17 +203,6 @@ -- 3. Don't create `define` for the ctor. -- Unfortunately 3 breaks a bunch of tests... -specTypeEq :: F.TCEmb TyCon -> Var -> SpecType -> F.Equation -specTypeEq emb f t = F.mkEquation (F.symbol f) xts body tOut - where - xts = Misc.safeZipWithError "specTypeEq" xs (RT.rTypeSort emb <$> ts) - body = specTypeToResultRef bExp t - tOut = RT.rTypeSort emb (ty_res tRep) - tRep = toRTypeRep t - xs = ty_binds tRep - ts = ty_args tRep - bExp = F.eApps (F.eVar f) (F.EVar <$> xs) - makeSimplify :: (Var, SpecType) -> [F.Rewrite] makeSimplify (var, t) | not (GM.isDataConId var) @@ -265,56 +244,6 @@ fromEVar (F.EVar x) = x fromEVar _ = impossible Nothing "makeSimplify.fromEVar" - -makeEquations :: Bool -> TargetSpec -> [F.Equation] -makeEquations allowTC sp = [ F.mkEquation f xts (equationBody allowTC (F.EVar f) xArgs e mbT) t - | F.Equ f xts e t _ <- axioms - , let xArgs = F.EVar . fst <$> xts - , let mbT = if null xArgs then Nothing else M.lookup f sigs - ] - where - axioms = gsMyAxioms refl ++ gsImpAxioms refl - refl = gsRefl sp - sigs = M.fromList [ (GM.simplesymbol v, t) | (v, t) <- gsTySigs (gsSig sp) ] - -equationBody :: Bool -> F.Expr -> [F.Expr] -> F.Expr -> Maybe LocSpecType -> F.Expr -equationBody allowTC f xArgs e mbT - | Just t <- mbT = F.pAnd [eBody, rBody t] - | otherwise = eBody - where - eBody = F.PAtom F.Eq (F.eApps f xArgs) e - rBody t = specTypeToLogic allowTC xArgs (F.eApps f xArgs) (val t) - --- NV Move this to types? --- sound but imprecise approximation of a type in the logic -specTypeToLogic :: Bool -> [F.Expr] -> F.Expr -> SpecType -> F.Expr -specTypeToLogic allowTC es expr st - | ok = F.subst su (F.PImp (F.pAnd args) res) - | otherwise = F.PTrue - where - res = specTypeToResultRef expr st - args = zipWith mkExpr (mkReft <$> ts) es - mkReft t = toReft $ Mb.fromMaybe mempty (stripRTypeBase t) - mkExpr (F.Reft (v, ev)) e = F.subst1 ev (v, e) - - - ok = okLen && okClass && okArgs - okLen = length xs == length xs - okClass = all (isTauto . snd) cls - okArgs = all okArg ts - - okArg (RVar _ _) = True - okArg t@RApp{} = isTauto (t{rt_reft = mempty}) - okArg _ = False - - - su = F.mkSubst $ zip xs es - (cls, nocls) = L.partition ((if allowTC then isEmbeddedClass else isClassType).snd) $ zip (ty_binds trep) (ty_args trep) - :: ([(F.Symbol, SpecType)], [(F.Symbol, SpecType)]) - (xs, ts) = unzip nocls :: ([F.Symbol], [SpecType]) - - trep = toRTypeRep st - specTypeToResultRef :: F.Expr -> SpecType -> F.Expr specTypeToResultRef e t diff --git a/src/Language/Haskell/Liquid/GHC/Interface.hs b/src/Language/Haskell/Liquid/GHC/Interface.hs --- a/src/Language/Haskell/Liquid/GHC/Interface.hs +++ b/src/Language/Haskell/Liquid/GHC/Interface.hs @@ -33,7 +33,6 @@ , modSummaryHsFile , makeFamInstEnv , clearSpec - , checkFilePragmas , lookupTyThing , updLiftedSpec ) where @@ -50,7 +49,6 @@ ) import qualified Liquid.GHC.API as Ghc -import Control.Exception import Control.Monad import Control.Monad.Trans.Maybe @@ -61,7 +59,6 @@ import Text.PrettyPrint.HughesPJ hiding (first, (<>)) import Language.Fixpoint.Types hiding (err, panic, Error, Result, Expr) -import qualified Language.Fixpoint.Misc as Misc import Language.Haskell.Liquid.GHC.Misc import Language.Haskell.Liquid.GHC.Types (MGIModGuts(..)) import Language.Haskell.Liquid.GHC.Play @@ -151,19 +148,6 @@ "modSummaryHsFile: missing .hs file for " ++ showPpr (ms_mod modSummary)) (ml_hs_file $ ms_location modSummary) - -checkFilePragmas :: [Located String] -> IO () -checkFilePragmas = Misc.applyNonNull (return ()) throw . mapMaybe err - where - err pragma - | check (val pragma) = Just (ErrFilePragma $ fSrcSpan pragma :: Error) - | otherwise = Nothing - check pragma = any (`isPrefixOf` pragma) bad - bad = - [ "-i", "--idirs" - , "-g", "--ghc-option" - , "--c-files", "--cfiles" - ] -------------------------------------------------------------------------------- -- | Family instance information diff --git a/src/Language/Haskell/Liquid/GHC/Plugin.hs b/src/Language/Haskell/Liquid/GHC/Plugin.hs --- a/src/Language/Haskell/Liquid/GHC/Plugin.hs +++ b/src/Language/Haskell/Liquid/GHC/Plugin.hs @@ -110,7 +110,7 @@ , pluginRecompile = purePlugin } where - liquidPlugin :: (MonadIO m) => [CommandLineOption] -> a -> (Config -> m a) -> m a + liquidPlugin :: MonadIO m => [CommandLineOption] -> a -> (Config -> m a) -> m a liquidPlugin opts def go = do cfg <- liftIO $ LH.getOpts opts if skipModule cfg then return def else go cfg @@ -123,17 +123,24 @@ typecheckPlugin opts summary gblEnv = liquidPlugin opts gblEnv $ \cfg -> typecheckPluginGo cfg summary gblEnv - -- Unfortunately, we can't make Haddock run the LH plugin, because the former - -- does mangle the '.hi' files, causing annotations to not be persisted in the - -- 'ExternalPackageState' and/or 'HomePackageTable'. For this reason we disable - -- the plugin altogether if the module is being compiled with Haddock. - -- See also: https://github.com/ucsd-progsys/liquidhaskell/issues/1727 - -- for a post-mortem. typecheckPluginGo cfg summary gblEnv = do - logger <- getLogger - dynFlags <- getDynFlags - withTiming logger (text "LiquidHaskell" <+> brackets (ppr $ ms_mod_name summary)) (const ()) $ do - if gopt Opt_Haddock dynFlags + logger0 <- getLogger + let logger = updateLogFlags logger0 (maybeDDumpTimings cfg) + GHC.withTiming + logger (text "LiquidHaskellCPU" <+> brackets (ppr $ ms_mod_name summary)) (const ()) $ + GHC.withTimingWallClock + logger (text "LiquidHaskell" <+> brackets (ppr $ ms_mod_name summary)) (const ()) $ do + dynFlags <- getDynFlags + -- Haddock runs the LH plugin, but it does not expose the annotations of dependencies. + -- This makes verification fail, so for now, we disable the plugin when haddock runs it. + -- + -- Detecting if Haddock is running the plugin is not obvious enough. We + -- try to see for now if Haddock comments are being collected and if the + -- noBackend is set. + -- + -- See https://gitlab.haskell.org/ghc/ghc/-/issues/26761 + -- and https://github.com/ucsd-progsys/liquidhaskell/issues/2188 + if gopt Opt_Haddock dynFlags && GHC.backendName (backend dynFlags) == GHC.NoBackend then do -- Warn the user let msg = PJ.vcat [ PJ.text "LH can't be run with Haddock." @@ -155,6 +162,13 @@ Right newGblEnv' -> pure newGblEnv' + -- We instruct LH to collect timings instead of doing it directly to GHC + -- This helps work around https://github.com/haskell/cabal/issues/11116 + maybeDDumpTimings :: Config -> LogFlags -> LogFlags + maybeDDumpTimings cfg = + if ddumpTimings cfg then log_set_dopt Opt_D_dump_timings + else id + -------------------------------------------------------------------------------- -- | Inter-phase communication ------------------------------------------------- -------------------------------------------------------------------------------- @@ -300,7 +314,7 @@ liquidCheckModule :: Config -> ModSummary -> TcGblEnv -> [BPspec] -> TcM (Either LiquidCheckException TcGblEnv) liquidCheckModule cfg0 ms tcg specs = do - withPragmas cfg0 thisFile pragmas $ \cfg -> do + withPragmas cfg0 pragmas $ \cfg -> do pipelineData <- do env <- getTopEnv session <- Session <$> liftIO (newIORef env) @@ -308,7 +322,6 @@ liquidLib <- setGblEnv tcg $ liquidHaskellCheckWithConfig cfg pipelineData ms traverse (serialiseSpec tcg) liquidLib where - thisFile = LH.modSummaryHsFile ms pragmas = [ s | Pragma s <- specs ] mkPipelineData :: (GhcMonad m) => ModSummary -> TcGblEnv -> [BPspec] -> m PipelineData @@ -412,10 +425,10 @@ out <- liftIO $ LH.checkTargetInfo pmrTargetInfo let bareSpec = lhInputSpec lhContext - file = LH.modSummaryHsFile $ lhModuleSummary lhContext - withPragmas (lhGlobalCfg lhContext) file (Ms.pragmas bareSpec) $ \moduleCfg -> do + withPragmas (lhGlobalCfg lhContext) (Ms.pragmas bareSpec) $ \moduleCfg -> do let filters = getFilters moduleCfg + file = LH.modSummaryHsFile $ lhModuleSummary lhContext -- Report the outcome of the checking LH.reportResult (errorLogger file filters) moduleCfg [giTarget (giSrc pmrTargetInfo)] out -- If there are unmatched filters or errors, and we are not reporting with @@ -448,11 +461,13 @@ -- | Working with bare & lifted specs ------------------------------------------ -------------------------------------------------------------------------------- +-- | Loads the specs of direct dependencies and /their/ dependencies as well. loadDependencies :: Config -> [Module] -> TcM TargetDependencies loadDependencies currentModuleConfig mods = do hscEnv <- env_top <$> getEnv results <- SpecFinder.findRelevantSpecs (excludeAutomaticAssumptionsFor currentModuleConfig) hscEnv mods + -- REVIEW: What does reversing the list accomplishes here? let deps = TargetDependencies $ foldl' processResult mempty (reverse results) redundant <- liftIO $ configToRedundantDependencies hscEnv currentModuleConfig @@ -498,14 +513,8 @@ debugLog ("Module ==> " ++ renderModule thisModule) let bareSpec0 = lhInputSpec - -- /NOTE/: For the Plugin to work correctly, we shouldn't call 'canonicalizePath', because otherwise - -- this won't trigger the \"external name resolution\" as part of 'Language.Haskell.Liquid.Bare.Resolve' - -- (cfr. 'allowExtResolution'). - let file = LH.modSummaryHsFile lhModuleSummary - _ <- liftIO $ LH.checkFilePragmas $ Ms.pragmas bareSpec0 - - withPragmas lhGlobalCfg file (Ms.pragmas bareSpec0) $ \moduleCfg -> do + withPragmas lhGlobalCfg (Ms.pragmas bareSpec0) $ \moduleCfg -> do dependencies <- loadDependencies moduleCfg lhRelevantModules debugLog $ "Found " <> show (HM.size $ getDependencies dependencies) <> " dependencies:" @@ -518,6 +527,7 @@ hscEnv <- getTopEnv let preNormalizedCore = preNormalizeCore moduleCfg modGuts0 modGuts = modGuts0 { mg_binds = preNormalizedCore } + file = LH.modSummaryHsFile lhModuleSummary targetSrc <- liftIO $ makeTargetSrc moduleCfg file modGuts hscEnv logger <- getLogger @@ -587,6 +597,9 @@ putStrLn "\n*************** Pre-normalized CoreBinds *****************\n" putStrLn $ unlines $ L.intersperse "" $ map (GHC.showPpr (GHC.hsc_dflags hscEnv)) (mg_binds modGuts) coreBinds <- anormalize cfg hscEnv modGuts + when (dumpNormalizedCore cfg) $ do + putStrLn "\n*************** normalized CoreBinds *****************\n" + putStrLn $ unlines $ L.intersperse "" $ map (GHC.showPpr (GHC.hsc_dflags hscEnv)) coreBinds let allTcs = mgi_tcs mgiModGuts diff --git a/src/Language/Haskell/Liquid/GHC/TypeRep.hs b/src/Language/Haskell/Liquid/GHC/TypeRep.hs --- a/src/Language/Haskell/Liquid/GHC/TypeRep.hs +++ b/src/Language/Haskell/Liquid/GHC/TypeRep.hs @@ -9,8 +9,6 @@ {-# OPTIONS_GHC -Wno-orphans #-} module Language.Haskell.Liquid.GHC.TypeRep ( - mkTyArg, - showTy ) where @@ -19,9 +17,6 @@ import Language.Fixpoint.Types (symbol) -- e368f3265b80aeb337fbac3f6a70ee54ab14edfd - -mkTyArg :: TyVar -> TyVarBinder -mkTyArg v = Bndr v Required instance Eq Type where t1 == t2 = eqType' t1 t2 diff --git a/src/Language/Haskell/Liquid/LHNameResolution.hs b/src/Language/Haskell/Liquid/LHNameResolution.hs --- a/src/Language/Haskell/Liquid/LHNameResolution.hs +++ b/src/Language/Haskell/Liquid/LHNameResolution.hs @@ -9,7 +9,7 @@ -- entities remains work in progress. -- -- Haskell entities include all functions that LH might reflect, or types that --- might be referred in refinment types, type aliases or other annotations. +-- might be referred in refinement types, type aliases or other annotations. -- -- Logic entities include the names of reflected functions, inlined functions, -- uninterpreted functions, predefined functions, local bindings, reflected data @@ -23,16 +23,15 @@ -- * Next the names of Haskell entities are resolved by 'resolveLHNames'. -- For now, this pass doesn't change the type of the names. -- * Next the names of logic entities are resolved. This pass produces --- a 'BareSpecLHName', where 'Symbol's are replaced with 'LHName'. At --- the moment most LHNames are just wrappers over the symbols. As name --- resolution is implemented for logic names, the wrappers will be --- replaced with the actual result of name resolution. +-- a 'BareSpecLHName', where 'Symbol's are replaced with 'LHName'. -- --- 'BareSpecLHName' has a bijection to 'BareSpec' via a 'LogicNameEnv' +-- 'BareSpecLHName' has an approximate bijection to 'BareSpec' via a 'LogicNameEnv' -- which allows to convert 'LHName' to an unambiguous form of 'Symbol' -- and back. The bijection is implemented with the functions 'toBareSpecLHName' -- and 'fromBareSpecLHName'. This allows to use liquid-fixpoint functions -- unmodified as they will continue to operate on (now unambiguous) Symbols. +-- The bijection is approximate because in the roundtrip the representation of +-- LHName's might change. -- -- At the same time, the 'BareSpecLHName' form is kept to serialize and to -- resolve names of modules that import the specs. @@ -53,6 +52,7 @@ , exprArg , fromBareSpecLHName , toBareSpecLHName + , symbolToLHName , LogicNameEnv(..) ) where @@ -63,19 +63,20 @@ import Language.Haskell.Liquid.Types.RType import Language.Haskell.Liquid.Types.RTypeOp +import Control.Monad.Except (ExceptT, runExceptT, throwError) import Control.Monad ((<=<), mplus, unless, void) import Control.Monad.Identity import Control.Monad.State.Strict -import Data.Bifunctor (first) +import Data.Bifunctor (first, second) import qualified Data.Char as Char import Data.Coerce (coerce) -import Data.Data (Data, gmapT) -import Data.Generics (extT) +import Data.Data (Data, gmapM) +import Data.Generics (extM) import qualified Data.HashSet as HS import qualified Data.HashMap.Strict as HM -import Data.List (find, isSuffixOf, nubBy) +import Data.List (find, isSuffixOf, nubBy, partition) import Data.List.Extra (dropEnd) import qualified Data.Map as Map import Data.Maybe (fromMaybe, listToMaybe, mapMaybe, maybeToList) @@ -85,6 +86,7 @@ import Language.Fixpoint.Types as F hiding (Error, panic) import qualified Language.Haskell.Liquid.Bare.Resolve as Resolve import Language.Haskell.Liquid.Bare.Types (LocalVars(lvNames), LocalVarDetails(lvdLclEnv)) +import Language.Fixpoint.Misc as Misc import Language.Haskell.Liquid.Name.LogicNameEnv import qualified Language.Haskell.Liquid.Types.DataDecl as DataDecl import Language.Haskell.Liquid.Types.Errors (TError(ErrDupNames, ErrResolve), panic) @@ -98,36 +100,58 @@ -- | Collects type aliases from the current module and its dependencies. -- --- It doesn't matter at the moment in which module a type alias is defined. --- Type alias names cannot be qualified at the moment, and therefore their --- names identify them uniquely. +-- By construction, type alises from transitive dependencies are neglected (see 'moduleAliases'). +-- We do so because all type aliases in scope are added to the 'LiftedSpec' later. +-- Aliases with the same unqualified name coexist during name resolution, +-- as long as we have a means to disambiguate (namely, by qualifing the import). +-- In this case, when building the 'LiftedSpec' we carry only the first such alias according +-- to lexicographic order. collectTypeAliases - :: GHC.Module + :: GHC.ImportedMods + -> GHC.Module -> BareSpecParsed -> TargetDependencies - -> HM.HashMap Symbol (GHC.Module, RTAlias Symbol ()) -collectTypeAliases m spec deps = - let bsAliases = [ (rtName a, (m, void a)) | a <- map val (aliases spec) ] - depAliases = - [ (rtName a, (GHC.unStableModule sm, void a)) + -> InScopeEnv (RTAlias Symbol ()) +collectTypeAliases impMods thisModule spec deps = + let bsAliases = mkAliasEnv thisModule impMods (thisModule, bsNames) + bsNames = [ (val . rtName $ rta, void rta) | rta <- aliases spec] + depAliases = map (mkAliasEnv thisModule impMods) $ + [ (m, depNames) | (sm, lspec) <- HM.toList (getDependencies deps) - , a <- map val (HS.toList $ liftedAliases lspec) + , let m = GHC.unStableModule sm + , let depNames = [ (val . rtName $ rta , void rta) + | rta <- HS.toList $ liftedAliases lspec + ] ] in - HM.fromList $ bsAliases ++ depAliases + unionAliasEnvs $ bsAliases : depAliases -collectExprAliases - :: BareSpecParsed - -> TargetDependencies - -> HS.HashSet Symbol -collectExprAliases spec deps = - let bsAliases = HS.fromList $ map (rtName . val) (ealiases spec) - depAliases = - [ HS.map (rtName . val) $ liftedEaliases lspec - | (_, lspec) <- HM.toList (getDependencies deps) - ] - in - HS.unions $ bsAliases : depAliases +-------------------------------------------------------------------------------- +-- | [NOTE:EXPRESSION-ALIASES]: +-- +-- In a lifted spec, expression aliases include fully unfolded predicate, +-- inline, and define annotations. By contrast, a bare spec’s expression +-- aliases include only predicate aliases. This is because symbols from these +-- three kinds of annotations are unfolded uniformly in logical expressions +-- during spec lifting. +-- +-- Inlines and defines are converted to expression aliases via 'lmapEalias', +-- which assigns them a 'GeneratedLogicName'. This allows us to distinguish +-- them from predicate aliases, which should be the only 'LogicName's among +-- expression aliases. +-- +-- Here, we collect the symbols of inlines and defines from expression aliases +-- to identify their uses when resolving logic variable names. +-- This should be redundant when these aliases are resolved via the +-- logic environments and a dedicated lifted field for inlines is added. +-------------------------------------------------------------------------------- +collectInlinesAndDefines:: TargetDependencies -> HS.HashSet Symbol +collectInlinesAndDefines deps = HS.unions + [ HS.map lhNameToResolvedSymbol depInlinesAndDefines + | (_, lspec) <- HM.toList (getDependencies deps) + , let exprAliases = HS.map (val . rtName) $ liftedEaliases lspec + depInlinesAndDefines = HS.filter (not . isResolvedLogicName) exprAliases + ] -- | Converts occurrences of LHNUnresolved to LHNResolved using the provided -- type aliases and GlobalRdrEnv. @@ -140,59 +164,66 @@ -> BareSpecParsed -> TargetDependencies -> Either [Error] (BareSpec, LogicNameEnv, LogicMap) -resolveLHNames cfg thisModule localVars impMods globalRdrEnv bareSpec0 dependencies = do - let ((bs, logicNameEnv, lmap2), ro) = - flip runState RenameOutput {roErrors = [], roUsedNames = [], roUsedDataCons = mempty} $ do - -- A generic traversal that resolves names of Haskell entities - sp1 <- mapMLocLHNames (\l -> (<$ l) <$> resolveLHName l) $ - fixExpressionArgsOfTypeAliases taliases bareSpec0 - -- Data decls contain fieldnames that introduce measures with the - -- same names. We resolved them before constructing the logic - -- environment. - dataDecls <- mapM (mapDataDeclFieldNamesM resolveFieldLogicName) (dataDecls sp1) - let sp2 = sp1 {dataDecls} +resolveLHNames cfg thisModule localVars impMods globalRdrEnv bareSpec0 dependencies = + flip evalState RenameOutput { roErrors = [], roUsedNames = [], roUsedDataCons = mempty } $ + runExceptT $ do + -- Prepare type aliases for resolution. + sp0 <- lift $ fixExpressionArgsOfTypeAliases taliases $ resolveBoundVarsInTypeAliases bareSpec0 - es0 <- gets roErrors - if null es0 then do + checkErrors - -- Now we do a second traversal to resolve logic names - let (inScopeEnv, logicNameEnv0, privateReflectNames, unhandledNames) = - makeLogicEnvs impMods thisModule sp2 dependencies - -- Add resolved local defines to the logic map - lmap1 = - lmap <> mkLogicMap (HM.fromList $ - (\(k , v) -> - let k' = lhNameToResolvedSymbol <$> k in - (F.val k', (val <$> v) { lmVar = k' })) - <$> defines sp2) - sp3 <- fromBareSpecLHName <$> - resolveLogicNames - cfg - inScopeEnv - globalRdrEnv - unhandledNames - lmap1 - localVars - logicNameEnv0 - privateReflectNames - allEaliases - sp2 - dcs <- gets roUsedDataCons - return (sp3 {usedDataCons = dcs} , logicNameEnv0, lmap1) - else - return ( error "resolveLHNames: invalid spec" - , error "resolveLHNames: invalid logic environment" - , error "resolveLHNames: invalid logic map") - logicNameEnv' = extendLogicNameEnv logicNameEnv (roUsedNames ro) - if null (roErrors ro) then - Right (bs, logicNameEnv', lmap2) - else - Left (roErrors ro) + -- First resolution pass: A generic traversal that resolves names + -- of Haskell entities and type alias binders. + sp1 <- lift $ mapMLocLHNames (\l -> (<$ l) <$> resolveLHName l) sp0 + + -- Data decls contain fieldnames that introduce measures with the + -- same names. We resolve them before constructing the logic + -- environments. + dataDecls <- lift $ mapM (mapDataDeclFieldNamesM resolveFieldLogicName) (dataDecls sp1) + let sp2 = sp1 {dataDecls} + + checkErrors + + -- Second resolution pass: a traversal to resolve logic names using the following + -- lookup environments. + let (inScopeEnv, logicNameEnv0, privateReflectNames) = + makeLogicEnvs impMods thisModule sp2 dependencies + + -- Add resolved local defines to the logic map. + lmap1 = lmap <> mkLogicMap (HM.fromList $ + [ (F.val $ lhNameToResolvedSymbol <$> k, + (val <$> v) { lmVar = lhNameToResolvedSymbol <$> k }) + | (k,v) <- defines sp2 ]) + sp3 <- lift $ fromBareSpecLHName <$> + resolveLogicNames + cfg + thisModule + inScopeEnv + globalRdrEnv + lmap1 + localVars + logicNameEnv0 + privateReflectNames + depsInlinesAndDefines + sp2 + + checkErrors + + dcs <- gets roUsedDataCons + return (sp3 { usedDataCons = dcs }, logicNameEnv0, lmap1) where - taliases = collectTypeAliases thisModule bareSpec0 dependencies - allEaliases = collectExprAliases bareSpec0 dependencies + -- Early exit name resolution if errors are found and pass them to the output. + checkErrors :: ExceptT [Error] (StateT RenameOutput Identity) () + checkErrors = do + es <- gets roErrors + unless (null es) (throwError es) - -- add defines from dependencies to the logical map + -- We collect type aliases before resolving names so we have a means to disambiguate + -- imported and local ones (according to their resolution status). + taliases = collectTypeAliases impMods thisModule bareSpec0 dependencies + depsInlinesAndDefines = collectInlinesAndDefines dependencies + + -- Add defines from dependencies to the logical map. lmap = (LH.listLMap <>) $ mconcat $ @@ -207,7 +238,7 @@ resolveLHName lname = case val lname of - LHNUnresolved LHTcName s + LHNUnresolved (LHTcName lcl) s | isTuple s -> pure $ LHNResolved (LHRGHC $ GHC.tupleTyConName GHC.BoxedTuple (tupleArity s)) s | isList s -> @@ -215,24 +246,35 @@ | s == "*" -> pure $ LHNResolved (LHRGHC GHC.liftedTypeKindTyConName) s | otherwise -> - case HM.lookup s taliases of - Just (m, _) -> pure $ LHNResolved (LHRLogic $ LogicName s m Nothing) s - Nothing -> lookupGRELHName LHTcName lname s listToMaybe + case resolveTypeAlias taliases s of + -- Priority is given to aliases defined in the current module, + -- so name occurrences are resolved using them, disregarding + -- any imported aliases with the same name. + -- This allows the user to shadow imported aliases. + FoundTypeAliases { tarLocallyDefined = [(m, _, _)] } -> + pure $ makeLogicLHName (LH.dropModuleNames s) m Nothing + FoundTypeAliases { tarImported = [(_, lh, _)] + , tarLocallyDefined = []} | lcl == LHAnyModuleNameF -> + pure lh + -- If multiple matches are found, report the ambiguous name and return it. + tar@(FoundTypeAliases { }) -> do addError $ errResolveTypeAlias (s <$ lname) tar + pure $ val lname + NoSuchTypeAlias alts -> lookupGRELHName alts (LHTcName lcl) lname s listToMaybe LHNUnresolved ns@(LHVarName lcl) s | isDataCon s -> - lookupGRELHName (LHDataConName lcl) lname s listToMaybe + lookupGRELHName [] (LHDataConName lcl) lname s listToMaybe | otherwise -> - lookupGRELHName ns lname s + lookupGRELHName [] ns lname s (fmap (either id GHC.getName) . Resolve.lookupLocalVar localVars (atLoc lname s)) LHNUnresolved LHLogicNameBinder s -> pure $ makeLogicLHName s thisModule Nothing n@(LHNUnresolved LHLogicName _) -> -- This one will be resolved by resolveLogicNames pure n - LHNUnresolved ns s -> lookupGRELHName ns lname s listToMaybe - n -> pure n + LHNUnresolved ns@(LHDataConName _) s -> lookupGRELHName [] ns lname s listToMaybe + n@LHNResolved { } -> pure n - lookupGRELHName ns lname s localNameLookup = + lookupGRELHName alts ns lname s localNameLookup = case maybeDropImported ns $ GHC.lookupGRE globalRdrEnv (mkLookupGRE ns s) of [e] -> do let n = GHC.greName e @@ -247,6 +289,7 @@ addError (ErrDupNames (LH.fSrcSpan lname) + "variable" (pprint s) (map (PJ.text . GHC.showPprUnsafe) es) ) @@ -257,7 +300,7 @@ pure $ LHNResolved (LHRGHC n') s Nothing -> do addError - (errResolve (nameSpaceKind ns) "Cannot resolve name" (s <$ lname)) + (errResolve alts (nameSpaceKind ns) "Cannot resolve name" (s <$ lname)) pure $ val lname maybeDropImported ns es @@ -267,13 +310,14 @@ localNameSpace = \case LHDataConName lcl -> lcl == LHThisModuleNameF LHVarName lcl -> lcl == LHThisModuleNameF - LHTcName -> False + LHTcName lcl -> lcl == LHThisModuleNameF LHLogicNameBinder -> False LHLogicName -> False nameSpaceKind :: LHNameSpace -> PJ.Doc nameSpaceKind = \case - LHTcName -> "type constructor" + LHTcName LHAnyModuleNameF -> "type constructor" + LHTcName LHThisModuleNameF -> "locally-defined type constructor" LHDataConName LHAnyModuleNameF -> "data constructor" LHDataConName LHThisModuleNameF -> "locally-defined data constructor" LHVarName LHAnyModuleNameF -> "variable" @@ -293,9 +337,20 @@ else a -errResolve :: PJ.Doc -> String -> LocSymbol -> Error -errResolve k msg lx = ErrResolve (LH.fSrcSpan lx) k (pprint (val lx)) (PJ.text msg) +errResolve :: [Symbol] -> PJ.Doc -> String -> LocSymbol -> Error +errResolve alts k msg ls = + ErrResolve + (LH.fSrcSpan ls) + k + (pprint $ val ls) + (if null alts then + PJ.text msg + else + PJ.text msg PJ.$$ + PJ.sep (PJ.text "Maybe you meant one of:" : map pprint alts) + ) + -- | Produces an LHName from a symbol by looking it in the rdr environment. resolveSymbolToTcName :: GHC.GlobalRdrEnv -> LocSymbol -> Either Error (Located LHName) resolveSymbolToTcName globalRdrEnv lx @@ -306,11 +361,12 @@ | s == "*" = pure $ LHNResolved (LHRGHC GHC.liftedTypeKindTyConName) s <$ lx | otherwise = - case GHC.lookupGRE globalRdrEnv (mkLookupGRE LHTcName s) of + case GHC.lookupGRE globalRdrEnv (mkLookupGRE (LHTcName LHAnyModuleNameF) s) of [e] -> Right $ LHNResolved (LHRGHC $ GHC.greName e) s <$ lx - [] -> Left $ errResolve "type constructor" "Cannot resolve name" lx + [] -> Left $ errResolve [] "type constructor" "Cannot resolve name" lx es -> Left $ ErrDupNames (LH.fSrcSpan lx) + "type constructor" (pprint s) (map (PJ.text . GHC.showPprUnsafe) es) where @@ -352,7 +408,7 @@ where mkWhichGREs :: LHNameSpace -> GHC.WhichGREs GHC.GREInfo mkWhichGREs = \case - LHTcName -> GHC.SameNameSpace + LHTcName _ -> GHC.SameNameSpace LHDataConName _ -> GHC.SameNameSpace LHVarName _ -> GHC.RelevantGREs { GHC.includeFieldSelectors = GHC.WantNormal @@ -363,7 +419,7 @@ LHLogicName -> panic Nothing "mkWhichGREs: unexpected namespace LHLogicName" mkGHCNameSpace = \case - LHTcName -> GHC.tcName + LHTcName _ -> GHC.tcName LHDataConName _ -> GHC.dataName LHVarName _ -> GHC.Types.Name.Occurrence.varName LHLogicNameBinder -> panic Nothing "mkGHCNameSpace: unexpected namespace LHLogicNameBinder" @@ -375,11 +431,11 @@ resolveBoundVarsInTypeAliases = updateAliases resolveBoundVars where resolveBoundVars boundVars = \case - LHNUnresolved LHTcName s -> + LHNUnresolved (LHTcName lcl) s -> if elem s boundVars then LHNResolved (LHRLocal s) s else - LHNUnresolved LHTcName s + LHNUnresolved (LHTcName lcl) s n -> error $ "resolveLHNames: Unexpected resolved name: " ++ show n @@ -387,8 +443,8 @@ -- arguments of the alias. updateAliases f spec = spec - { aliases = [ Loc sp0 sp1 (a { rtBody = mapLHNames (f args) (rtBody a) }) - | Loc sp0 sp1 a <- aliases spec + { aliases = [ a { rtBody = mapLHNames (f args) (rtBody a) } + | a <- aliases spec , let args = rtTArgs a ++ rtVArgs a ] } @@ -401,44 +457,67 @@ -- > {-@ type Prop E = {v:_ | prop v = E} @-} -- -- the parser builds a type for @Ev (plus n n)@. +-- | @fixExpressionArgsOfTypeAliases taliases spec@ converts types to +-- values when they appear in value positions of type aliases according +-- to @taliases@. -- +-- The expression arguments of type aliases are initially parsed as +-- types. This function converts them to expressions. +-- +-- For instance, in @Prop (Ev (plus n n))@ where `Prop` is the alias +-- +-- > {-@ type Prop E = {v:_ | prop v = E} @-} +-- +-- the parser builds a type for @Ev (plus n n)@, making a type +-- constructor of @Ev@ and type variables of @plus@ and @n@. But +-- @Ev@ is really a data constructor, @plus@ is a function, and @n@ +-- is a value. fixExpressionArgsOfTypeAliases - :: HM.HashMap Symbol (GHC.Module, RTAlias Symbol ()) - -> BareSpecParsed + :: InScopeEnv (RTAlias Symbol ()) -> BareSpecParsed -fixExpressionArgsOfTypeAliases taliases = - mapBareTypes go . resolveBoundVarsInTypeAliases + -> StateT RenameOutput Identity BareSpecParsed +fixExpressionArgsOfTypeAliases taliases = mapMBareTypes go where - go :: BareTypeParsed -> BareTypeParsed - go (RApp c@(BTyCon { btc_tc = Loc _ _ (LHNUnresolved LHTcName s) }) ts rs r) - | Just (_, rta) <- HM.lookup s taliases = - RApp c (fixExprArgs (btc_tc c) rta (map go ts)) (map goRef rs) r - go (RApp c ts rs r) = - RApp c (map go ts) (map goRef rs) r - go (RAppTy t1 t2 r) = RAppTy (go t1) (go t2) r - go (RFun x i t1 t2 r) = RFun x i (go t1) (go t2) r - go (RAllT a t r) = RAllT a (go t) r - go (RAllP a t) = RAllP a (go t) - go (RAllE x t1 t2) = RAllE x (go t1) (go t2) - go (REx x t1 t2) = REx x (go t1) (go t2) - go (RRTy e r o t) = RRTy e r o (go t) - go t@RHole{} = t - go t@RVar{} = t - go t@RExprArg{} = t - goRef (RProp ss t) = RProp ss (go t) + go :: BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed + go (RApp c@(BTyCon { btc_tc = lname@(Loc _ _ (LHNUnresolved (LHTcName _) s)) }) ts rs r) + | tar@(FoundTypeAliases imported local) <- resolveTypeAlias taliases s = + case (imported, local) of + -- Local alias definitions get priority over imported ones. + -- This allows the user to shadow imported aliases. + (_ ,[(_, _, rta)]) -> + RApp <$> pure c <*> fixExprArgs (btc_tc c) rta (mapM go ts) <*> mapM goRef rs <*> pure r + ([(_, _, rta)] , []) -> + RApp <$> pure c <*> fixExprArgs (btc_tc c) rta (mapM go ts) <*> mapM goRef rs <*> pure r + -- Report ambiguos name and continue traversing. + _ -> do + addError $ errResolveTypeAlias (s <$ lname) tar + RApp <$> pure c <*> mapM go ts <*> mapM goRef rs <*> pure r + go (RApp c ts rs r) = RApp <$> pure c <*> mapM go ts <*> mapM goRef rs <*> pure r + go (RAppTy t1 t2 r) = RAppTy <$> go t1 <*> go t2 <*> pure r + go (RFun x i t1 t2 r) = RFun <$> pure x <*> pure i <*> go t1 <*> go t2 <*> pure r + go (RAllT a t r) = RAllT <$> pure a <*> go t <*> pure r + go (RAllP a t) = RAllP a <$> go t + go (RAllE x t1 t2) = RAllE x <$> go t1 <*> go t2 + go (REx x t1 t2) = REx x <$> go t1 <*> go t2 + go (RRTy e r o t) = RRTy e r o <$> go t + go t@RHole{} = pure t + go t@RVar{} = pure t + go t@RExprArg{} = pure t + goRef (RProp ss t) = RProp ss <$> go t - fixExprArgs lname rta ts = + fixExprArgs lname rta mts = do + ts <- mts let n = length (rtTArgs rta) (targs, eargs) = splitAt n ts msg = "FIX-EXPRESSION-ARG: " ++ showpp (rtName rta) toExprArg = exprArg (LH.fSourcePos lname) msg - in targs ++ [ RExprArg $ toExprArg e <$ lname | e <- eargs ] + pure $ targs ++ [ RExprArg $ toExprArg e <$ lname | e <- eargs ] -mapBareTypes :: (BareTypeParsed -> BareTypeParsed) -> BareSpecParsed -> BareSpecParsed -mapBareTypes f = go +mapMBareTypes :: forall m a.(Data a, Monad m) => (BareTypeParsed -> m BareTypeParsed) -> a -> m a +mapMBareTypes f = go where - go :: Data a => a -> a - go = gmapT (go `extT` f) + go :: forall b. Data b => b -> m b + go = gmapM (go `extM` f) -- | exprArg converts a tyVar to an exprVar because parser cannot tell -- this function allows us to treating (parsed) "types" as "value" @@ -448,31 +527,110 @@ -- the string `Prop (Ev (plus n n))` where `Prop` is the alias: -- {-@ type Prop E = {v:_ | prop v = E} @-} -- the parser will chomp in `Ev (plus n n)` as a `BareType` and so --- `exprArg` converts that `BareType` into an `Expr`. +-- | @exprArg@ converts a type to a value. +-- +-- At parse time the arguments of type aliases are all treated as types. +-- This needs fixing before verification because some arguments are +-- meant to be values. Hence, this function to correct the +-- arguments in question. See the documentation of +-- @fixExpressionArgsOfTypeAliases@ for some more context. exprArg :: SourcePos -> String -> BareTypeParsed -> ExprV LocSymbol exprArg l msg = notracepp ("exprArg: " ++ msg) . go where go :: BareTypeParsed -> ExprV LocSymbol go (RExprArg e) = val e - go (RVar (BTV x) _) = EVar x + go (RVar (BTV x) _) = EVar x go (RApp x [] [] _) = EVar (getLHNameSymbol <$> btc_tc x) - go (RApp f ts [] _) = eApps (EVar (getLHNameSymbol <$> btc_tc f)) (go <$> ts) + go (RApp f ts [] _) = eApps (EVar (renameAmbiguousCtor . getLHNameSymbol <$> btc_tc f)) (go <$> ts) go (RAppTy t1 t2 _) = EApp (go t1) (go t2) go z = panic sp $ Printf.printf "Unexpected expression parameter: %s in %s" (show $ parsedToBareType z) msg sp = Just (LH.sourcePosSrcSpan l) +renameAmbiguousCtor :: Symbol -> Symbol +renameAmbiguousCtor x + | Just n <- isTyTupleSizedSymbol x = tmTupleSizedSymbol n + | otherwise = x + +-- | A type alias 'lookupInScopeEnv' that distinguishes locally defined names +-- from imported ones based on their resolution status: +-- unresolved names correspond to type aliases defined in the current module, +-- whereas all imported names are expected to be resolved. +resolveTypeAlias + :: InScopeEnv (RTAlias Symbol a) + -> Symbol + -> TypeAliasResolution (RTAlias Symbol a) +resolveTypeAlias taliases s = case lookupInScopeEnv taliases s of + Right ns -> let (imported, local) = + partition (\(_,lhname,_) -> isResolvedLogicName lhname ) ns + in FoundTypeAliases imported local + Left alts -> NoSuchTypeAlias alts + +-- | When resolving type aliases we either find matching 'LHName's +-- or similar, but distinct, 'Symbol's. +data TypeAliasResolution a + = NoSuchTypeAlias [Symbol] + | FoundTypeAliases + { tarImported :: [(GHC.Module, LHName, a)] + , tarLocallyDefined :: [(GHC.Module, LHName, a)] + } + +errResolveTypeAlias :: LocSymbol -> TypeAliasResolution (RTAlias x a) -> Error +errResolveTypeAlias ls (FoundTypeAliases imported local) = + ErrDupNames (LH.fSrcSpan ls) "type alias" (pprint $ val ls) + ( + -- Currently, multiple local definitions prevent this error from being raised, + -- because duplicate names are discarded when constructing the alias environment + -- for each individual module, + -- and a local alias always shadows any imported one. Such duplicates are detected + -- later during validation of the final target spec. + -- + -- Also, note that collected local type alias names remain unresolved at this stage, + -- so we must extract their symbol using a function that can safely handle unresolved + -- names. + map (\(_, lhn, rta) -> pprint (getLHNameSymbol lhn) + PJ.<+> + PJ.text "defined in current module at" + PJ.<+> + pprint (LH.fSrcSpan . rtName $ rta) + ) + local + ++ + map (\(m, lhn, rta) -> pprint (lhNameToUnqualifiedSymbol lhn) + PJ.<+> + PJ.text "imported from module" + PJ.<+> + PJ.text (GHC.moduleNameString (GHC.moduleName m)) + PJ.<+> + PJ.text "defined at" + PJ.<+> + pprint (LH.fSrcSpan . rtName $ rta) + ) + imported + ) +errResolveTypeAlias ls (NoSuchTypeAlias alts) = + errResolve alts "type alias" "Cannot resolve name" ls + + -- | An environment of names in scope -- --- For each symbol we have the aliases with which it is imported and the --- name corresponding to each alias. -type InScopeNonReflectedEnv = SEnv [(GHC.ModuleName, (GHC.Module, LHName))] +-- We construct it using 'mkAliasEnv' and 'unionAliasEnvs' in such a way that each +-- symbol in the environment corresponds to all matching 'LHNames' along with +-- the aliases of the module we import it from. +-- Currently, the parameter is used to include the type alias representation when +-- we 'collectTypeAliases'. +type InScopeEnv a = SEnv [(GHC.ModuleName, (GHC.Module, LHName, a))] --- | Looks the names in scope with the given symbol. --- Returns a list of close but different symbols or a non empty list +type InScopeNonReflectedEnv = InScopeEnv () + +-- | Looks for the 'LHName's in scope with the given symbol, +-- taking possible qualification prefixes into account. +-- Returns a list of close but different symbols or a non-empty list -- with the matched names. -lookupInScopeNonReflectedEnv - :: InScopeNonReflectedEnv -> Symbol -> Either [Symbol] [(GHC.Module, LHName)] -lookupInScopeNonReflectedEnv env s = do +lookupInScopeEnv + :: InScopeEnv a -> Symbol -> Either [Symbol] [(GHC.Module, LHName, a)] +lookupInScopeEnv env s = do + -- The symbol might be qualified or not, + -- but we use the unqualified symbol for the lookup. let n = LH.dropModuleNames s case lookupSEnvWithDistance n env of Alts closeSyms -> Left closeSyms @@ -486,7 +644,7 @@ if m == "" then n else LH.qualifySymbol m n -- | Builds an environment of non-reflected names in scope from the module --- aliases for the current module, the spec of the current module, and the specs +-- imports for the current module, the spec of the current module, and the specs -- of the dependencies. -- -- Also returns a LogicNameEnv constructed from the same names. @@ -500,28 +658,16 @@ -> ( InScopeNonReflectedEnv , LogicNameEnv , HS.HashSet LocSymbol - , HS.HashSet Symbol ) -makeLogicEnvs impAvails thisModule spec dependencies = - let unqualify s = - if s == LH.qualifySymbol (symbol $ GHC.moduleName thisModule) (LH.dropModuleNames s) then - LH.dropModuleNames s - else - s - - -- Names should be removed from this list as they are supported - -- by renaming. - unhandledNames = HS.fromList $ - map unqualify unhandledNamesList ++ map (LH.qualifySymbol (symbol $ GHC.moduleName thisModule)) unhandledNamesList - unhandledNamesList = - map (rtName . val) (ealiases spec) - ++ concatMap (map getLHNameSymbol . snd) unhandledLogicNames - unhandledLogicNames = - map (fmap collectUnhandledLiftedSpecLogicNames) dependencyPairs - logicNames = - (thisModule, thisModuleNames) : +makeLogicEnvs impMods thisModule spec dependencies = + let depsLogicNames = map (fmap collectLiftedSpecLogicNames) dependencyPairs - ++ unhandledLogicNames + logicNames = + (thisModule, thisModuleNames) : depsLogicNames + nonReflectedNamesWithUnit = + map + (second $ map (, ()) . filter isNonReflectedLogicName) + logicNames thisModuleNames = concat [ [ reflectLHName thisModule (val n) | n <- concat @@ -538,51 +684,70 @@ concatMap DataDecl.dcFields $ concat $ mapMaybe DataDecl.tycDCons $ dataDecls spec + , [ val (rtName ea) | ea <- ealiases spec ] ] privateReflectNames = mconcat $ privateReflects spec : map (liftedPrivateReflects . snd) dependencyPairs in - ( unionAliasEnvs $ map mkAliasEnv logicNames + ( unionAliasEnvs $ map (mkAliasEnv thisModule impMods) nonReflectedNamesWithUnit , mkLogicNameEnv (concatMap snd logicNames) , privateReflectNames - , unhandledNames ) where dependencyPairs = map (first GHC.unStableModule) $ HM.toList $ getDependencies dependencies - mkAliasEnv (m, lhnames) = - let aliases = moduleAliases m - in fromListSEnv - [ (s, map (,(m, lhname)) aliases) - -- Note that only non-reflected names go to the InScope environment. - -- See the local function resolveVarName for more details. - | lhname@(LHNResolved (LHRLogic (LogicName s _ Nothing)) _) <- lhnames - ] + mkLogicNameEnv names = + LogicNameEnv + { lneLHName = fromListSEnv [ (lhNameToResolvedSymbol n, n) | n <- names ] + , lneReflected = GHC.mkNameEnv [(rn, n) | n <- names, Just rn <- [maybeReflectedLHName n]] + } - unionAliasEnvs :: [InScopeNonReflectedEnv] -> InScopeNonReflectedEnv - unionAliasEnvs = - coerce . - HM.map (nubBy (\(alias1, (_, n1)) (alias2, (_, n2)) -> alias1 == alias2 && n1 == n2)) . - foldl' (HM.unionWith (++)) HM.empty . - coerce @_ @[HM.HashMap Symbol [(GHC.ModuleName, (GHC.Module, LHName))]] +unionAliasEnvs :: forall a. [InScopeEnv a] -> InScopeEnv a +unionAliasEnvs = + coerce . + -- We make sure that the module alias and the 'LHName' effectively disambiguate + -- the occurrence of a symbol. This is because the same name can come from + -- several imported modules. + HM.map (nubBy (\(alias1, (_, n1, _)) (alias2, (_, n2, _)) -> alias1 == alias2 && n1 == n2)) . + foldl' (HM.unionWith (++)) HM.empty . + coerce @_ @[HM.HashMap Symbol [(GHC.ModuleName, (GHC.Module, LHName, a))]] - moduleAliases m = - case Map.lookup m impAvails of - Just impBys -> concatMap imvAliases $ GHC.importedByUser impBys - Nothing - | thisModule == m -> - -- Aliases for the current module - [GHC.moduleName m, GHC.mkModuleName ""] - | otherwise -> - -- Use the aliases of the unsuffixed module - concatMap imvAliases $ GHC.importedByUser $ - concat $ maybeToList $ do - pString <- dropLHAssumptionsSuffix m - pMod <- findDependency pString - Map.lookup pMod impAvails +-- | Builds a symbol lookup environment from a list of names associated with the +-- module they were extracted from, adding any import aliases that module may +-- have within the current module (if it was imported directly). +mkAliasEnv:: GHC.Module -> GHC.ImportedMods -> (GHC.Module, [(LHName, a)]) -> InScopeEnv a +mkAliasEnv thisModule impMods (m, lhnames) = + let aliases = moduleAliases thisModule impMods m + in fromListSEnv + -- Note that when building a name environment for the current module + -- we might process unresolved names here. + [ (LH.dropModuleNames $ getLHNameSymbol lhname + , map (,(m, lhname, x)) aliases) + | (lhname, x) <- lhnames + ] - dropLHAssumptionsSuffix m = +-- | Produces the list of aliases a module is imported with. +-- The first parameter holds the reference to the current module. +-- Transitive dependencies get an empty alias list. +moduleAliases :: GHC.Module -> GHC.ImportedMods -> GHC.Module -> [GHC.ModuleName] +moduleAliases thisModule impMods m = + case Map.lookup m impMods of + -- Aliases for imported modules. + Just impBys -> concatMap imvAliases $ GHC.importedByUser impBys + Nothing + | thisModule == m -> + -- Aliases for the current module. + [GHC.moduleName m, GHC.mkModuleName ""] + | otherwise -> + -- For LHAssumptions modules, use the aliases of the unsuffixed module. + concatMap imvAliases $ GHC.importedByUser $ + concat $ maybeToList $ do + pString <- dropLHAssumptionsSuffix + pMod <- findDependency pString + Map.lookup pMod impMods + where + dropLHAssumptionsSuffix = let mString = GHC.moduleNameString (GHC.moduleName m) sfx = "_LHAssumptions" in if isSuffixOf sfx mString then @@ -592,31 +757,22 @@ findDependency ms = find ((ms ==) . GHC.moduleNameString . GHC.moduleName) $ - Map.keys impAvails + Map.keys impMods imvAliases imv | GHC.imv_qualified imv = [GHC.imv_name imv] | otherwise = [GHC.imv_name imv, GHC.mkModuleName ""] - mkLogicNameEnv names = - LogicNameEnv - { lneLHName = fromListSEnv [ (lhNameToResolvedSymbol n, n) | n <- names ] - , lneReflected = GHC.mkNameEnv [(rn, n) | n <- names, Just rn <- [maybeReflectedLHName n]] - } - -{- HLINT ignore collectUnhandledLiftedSpecLogicNames "Use ++" -} -collectUnhandledLiftedSpecLogicNames :: LiftedSpec -> [LHName] -collectUnhandledLiftedSpecLogicNames sp = - map (makeLocalLHName . LH.dropModuleNames . rtName . val) $ HS.toList $ liftedEaliases sp - collectLiftedSpecLogicNames :: LiftedSpec -> [LHName] collectLiftedSpecLogicNames sp = concat [ map fst (HS.toList $ liftedExpSigs sp) , map (val . msName) (HM.elems $ liftedMeasures sp) , map (val . msName) (HM.elems $ liftedCmeasures sp) + , map (val . msName) (HS.toList $ liftedOmeasures sp) , map fst $ concatMap DataDecl.dcFields $ concat $ mapMaybe DataDecl.tycDCons $ HS.toList $ liftedDataDecls sp + , map (val . rtName) $ HS.toList $ liftedEaliases sp ] -- | Resolves names in the logic namespace @@ -626,9 +782,9 @@ -- the names of data constructors that are found during renaming. resolveLogicNames :: Config + -> GHC.Module -> InScopeNonReflectedEnv -> GHC.GlobalRdrEnv - -> HS.HashSet Symbol -> LogicMap -> LocalVars -> LogicNameEnv @@ -636,7 +792,7 @@ -> HS.HashSet Symbol -> BareSpecParsed -> State RenameOutput BareSpecLHName -resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv privateReflectNames allEaliases sp = do +resolveLogicNames cfg thisModule env globalRdrEnv lmap0 localVars lnameEnv privateReflectNames depsInlinesAndDefines sp = do -- Instance measures must be defined for names of class measures. -- The names of class measures should be in @env@ imeasures <- mapM (mapMeasureNamesM resolveIMeasLogicName) (imeasures sp) @@ -659,7 +815,7 @@ -- The name is local | elem s ss = return $ makeLocalLHName s | otherwise = - case lookupInScopeNonReflectedEnv env s of + case lookupInScopeEnv env s of Left alts -> -- If names are not in the environment, they must be data constructors, -- or they must be reflected functions, or they must be in the logicmap. @@ -669,39 +825,33 @@ | elem s wiredInNames -> return $ makeLocalLHName s | otherwise -> do - unless (HS.member s unhandledNames) $ - addError (errResolveLogicName ls alts) - return $ makeLocalLHName s - Right [(_, lhname)] -> - return lhname - Right names -> do - addError $ - ErrDupNames - (LH.fSrcSpan ls) - (pprint s) - [ pprint (lhNameToResolvedSymbol n) PJ.<+> - PJ.text - ("imported from " ++ GHC.moduleNameString (GHC.moduleName m)) - | (m, n) <- names - ] - return $ makeLocalLHName s + addError $ errResolve alts "logic name" "Cannot resolve name" ls + return $ makeLocalLHName s + Right [(_, lhname, _)] -> pure lhname + -- In case of multiple matches, we give precedence to locally defined + -- logic entities for the user to be able to overwrite them. + -- TODO: When a mechanism allowing to specify explicitly which logic names + -- are imported is in place, we should cosider notifying the ambiguity directly. + Right names -> + case filter ((== thisModule) . logicNameOriginModule . Misc.snd3) names of + [(_, lhname, _)] -> pure lhname + _ -> do addError $ errDupInScopeNames ls names + return $ makeLocalLHName s where s = val ls wiredInNames = map fst wiredSortedSyms ++ map (lhNameToResolvedSymbol . fst) (concatMap (DataDecl.dcpTyArgs . val) wiredDataCons) - - errResolveLogicName s alts = - ErrResolve - (LH.fSrcSpan s) - (PJ.text "logic name") - (pprint $ val s) - (if null alts then - PJ.text "Cannot resolve name" - else - PJ.text "Cannot resolve name" PJ.$$ - PJ.sep (PJ.text "Maybe you meant one of:" : map pprint alts) - ) + errDupInScopeNames locSym inScopeNames = + ErrDupNames + (LH.fSrcSpan locSym) + "non-reflected logic entity" + (pprint (val locSym)) + [ pprint (lhNameToResolvedSymbol n) PJ.<+> + PJ.text + ("imported from " ++ GHC.moduleNameString (GHC.moduleName m)) + | (m, n, _) <- inScopeNames + ] resolveDataConName ls | unqualifiedS == ":" = Just $ @@ -739,6 +889,7 @@ addError (ErrDupNames (LH.fSrcSpan s) + "data constructor" (pprint $ val s) (map (PJ.text . GHC.showPprUnsafe) es) ) @@ -763,9 +914,8 @@ -> case gres of [e] -> do let n = GHC.greName e - -- TODO: The check for allEaliases should be redundant when - -- ealiases are put in the logic environments - if HM.member (symbol n) (lmSymDefs lmap) || HS.member (symbol n) allEaliases then + -- See [NOTE:EXPRESSION-ALIASES] + if HM.member (symbol n) (lmSymDefs lmap) || HS.member (symbol n) depsInlinesAndDefines then Just $ do let lhName = makeLogicLHName (symbol $ GHC.getOccString n) (GHC.nameModule n) Nothing addName lhName @@ -779,6 +929,7 @@ addError (ErrDupNames (LH.fSrcSpan s) + "variable" (pprint $ val s) (map (PJ.text . GHC.showPprUnsafe) es) ) @@ -808,7 +959,7 @@ return c{DataDecl.dcFields} toBareSpecLHName :: Config -> LogicNameEnv -> BareSpec -> BareSpecLHName -toBareSpecLHName cfg env sp0 = runIdentity $ go sp0 +toBareSpecLHName cfg lenv sp0 = runIdentity $ go sp0 where -- This is implemented with a monadic traversal to reuse the logic -- that collects the local symbols in scope. @@ -817,19 +968,24 @@ emapSpecM (bscope cfg) (const []) - symbolToLHName - (emapBareTypeVM (bscope cfg) symbolToLHName) + symToLHName + (emapBareTypeVM (bscope cfg) symToLHName) sp + symToLHName = symbolToLHName "toBareSpecLHName" lenv unhandledNames + unhandledNames = HS.fromList $ map fst $ expSigs sp0 - symbolToLHName :: [Symbol] -> Symbol -> Identity LHName - symbolToLHName ss s - | elem s ss = return $ makeLocalLHName s - | otherwise = - case lookupSEnv s (lneLHName env) of - Nothing -> do - unless (HS.member s unhandledNames) $ - panic Nothing $ "toBareSpecLHName: cannot find " ++ show s - return $ makeLocalLHName s - Just lhname -> return lhname +-- | Uses the logic name environment to convert a resolved 'Symbol' to 'LHName'. +-- Symbols not present in the environment correspond to local symbols (e.g. +-- bounded variables) or are explicitly left unhandled. +symbolToLHName :: String -> LogicNameEnv -> HS.HashSet Symbol -> [Symbol] -> Symbol -> Identity LHName +symbolToLHName caller lenv unhandledNames ss s + | elem s ss = return $ makeLocalLHName s + | otherwise = + case lookupSEnv s (lneLHName lenv) of + Nothing -> do + unless (HS.member s unhandledNames) $ + panic Nothing $ caller ++ ": cannot find " ++ show s + return $ makeLocalLHName s + Just lhname -> return lhname diff --git a/src/Language/Haskell/Liquid/Liquid.hs b/src/Language/Haskell/Liquid/Liquid.hs --- a/src/Language/Haskell/Liquid/Liquid.hs +++ b/src/Language/Haskell/Liquid/Liquid.hs @@ -12,6 +12,7 @@ import qualified Data.HashSet as S import Text.PrettyPrint.HughesPJ import Control.Monad (when) +import qualified Data.HashMap.Strict as HashMap import qualified Data.Maybe as Mb import qualified Data.List as L import qualified Language.Haskell.Liquid.UX.DiffCheck as DC @@ -133,29 +134,30 @@ solveCs cfg tgt cgi info names = do finfo <- cgInfoFInfo info cgi let fcfg = fixConfig tgt cfg - F.Result {resStatus=r0, resSolution=sol} <- solve fcfg finfo + F.Result {resStatus=r0, resSolution=solCuts, resNonCutsSolution=solNonCuts} <- solve fcfg finfo + let sol = HashMap.union (HashMap.map F.Delayed solCuts) solNonCuts let failBs = gsFail $ gsTerm $ giSpec info let (r,rf) = splitFails (S.map val failBs) r0 - let resErr = second (applySolution sol . cinfoError) <$> r + let resErr = second (applySolution finfo sol . cinfoError) <$> r -- resModel_ <- fmap (e2u cfg sol) <$> getModels info cfg resErr - let resModel_ = cidE2u cfg sol <$> resErr - let resModel' = resModel_ `addErrors` (e2u cfg sol <$> logErrors cgi) + let resModel_ = cidE2u cfg <$> resErr + let resModel' = resModel_ `addErrors` (e2u cfg <$> logErrors cgi) `addErrors` makeFailErrors (S.toList failBs) rf `addErrors` makeFailUseErrors (S.toList failBs) (giCbs $ giSrc info) - let lErrors = applySolution sol <$> logErrors cgi - let resModel = resModel' `addErrors` (e2u cfg sol <$> lErrors) - let out0 = mkOutput cfg resModel sol (annotMap cgi) + let lErrors = applySolution finfo sol <$> logErrors cgi + let resModel = resModel' `addErrors` (e2u cfg <$> lErrors) + let out0 = mkOutput cfg resModel finfo sol (annotMap cgi) return $ out0 { o_vars = names } { o_result = resModel } -e2u :: Config -> F.FixSolution -> Error -> UserError -e2u cfg s = fmap F.pprint . tidyError cfg s +e2u :: Config -> Error -> UserError +e2u cfg = fmap F.pprint . tidyError cfg -cidE2u :: Config -> F.FixSolution -> (Integer, Error) -> UserError -cidE2u cfg s (subcId, e) = +cidE2u :: Config -> (Integer, Error) -> UserError +cidE2u cfg (subcId, e) = let e' = attachSubcId e - in fmap F.pprint (tidyError cfg s e') + in fmap F.pprint (tidyError cfg e') where attachSubcId es@ErrSubType{} = es { cid = Just subcId } attachSubcId es@ErrSubTypeModel{} = es { cid = Just subcId } @@ -178,7 +180,7 @@ go :: CoreBind -> [(Var,[Var])] go (NonRec x e) = [(x, readVars e)] - go (Rec xes) = [(x,cls) | x <- map fst xes] where cls = concatMap readVars (snd <$> xes) + go (Rec xes) = [(x,cls) | x <- map fst xes] where cls = concatMap (readVars . snd) xes makeFailErrors :: [F.Located Var] -> [Cinfo] -> [UserError] makeFailErrors bs cis = [ mkError x | x <- bs, notElem (val x) vs ] diff --git a/src/Language/Haskell/Liquid/Measure.hs b/src/Language/Haskell/Liquid/Measure.hs --- a/src/Language/Haskell/Liquid/Measure.hs +++ b/src/Language/Haskell/Liquid/Measure.hs @@ -92,7 +92,7 @@ dataConTypes allowTC s = (ctorTys, measTys) where measTys = [(msName m, msSort m) | m <- M.elems (measMap s) ++ imeas s] - ctorTys = concatMap (makeDataConType allowTC) (notracepp "HOHOH" . snd <$> M.toList (ctorMap s)) + ctorTys = concatMap (makeDataConType allowTC . notracepp "HOHOH" . snd) (M.toList (ctorMap s)) makeDataConType :: Bool -> [Def (RRType Reft) DataCon] -> [(Var, RRType Reft)] makeDataConType _ [] @@ -126,7 +126,7 @@ isWorkerDef def -- types are missing for arguments, so definition came from a logical measure -- and it is for the worker datacon - | any Mb.isNothing (snd <$> binds def) + | any (Mb.isNothing . snd) (binds def) = True | otherwise = length (binds def) == length (fst $ splitFunTys $ snd $ splitForAllTyCoVars wot) diff --git a/src/Language/Haskell/Liquid/Misc.hs b/src/Language/Haskell/Liquid/Misc.hs --- a/src/Language/Haskell/Liquid/Misc.hs +++ b/src/Language/Haskell/Liquid/Misc.hs @@ -346,6 +346,9 @@ getFst = head . sortOn fst krvss = groupList [ (k, (r, v)) | (r, k, v) <- rkvs ] +ordNub :: Ord a => [a] -> [a] +ordNub = map head . L.group . L.sort + sortOn :: (Ord b) => (a -> b) -> [a] -> [a] sortOn f = L.sortBy (compare `on` f) diff --git a/src/Language/Haskell/Liquid/Name/LogicNameEnv.hs b/src/Language/Haskell/Liquid/Name/LogicNameEnv.hs --- a/src/Language/Haskell/Liquid/Name/LogicNameEnv.hs +++ b/src/Language/Haskell/Liquid/Name/LogicNameEnv.hs @@ -13,8 +13,9 @@ -- Symbols are expected to have been created by 'lhNameToResolvedSymbol'. -- data LogicNameEnv = LogicNameEnv - { lneLHName :: SEnv LHName - -- | Haskell names that have a reflected counterpart + { -- | A (qualified) symbol map to resolve logic names. + lneLHName :: SEnv LHName + -- | Haskell names that have a reflected counterpart. , lneReflected :: GHC.NameEnv LHName } diff --git a/src/Language/Haskell/Liquid/Parse.hs b/src/Language/Haskell/Liquid/Parse.hs --- a/src/Language/Haskell/Liquid/Parse.hs +++ b/src/Language/Haskell/Liquid/Parse.hs @@ -241,7 +241,7 @@ b <- locInfixSymbolP PC _ t2 <- btP return $ PC sb $ RApp - (mkBTyCon $ fmap (makeUnresolvedLHName LHTcName) b) + (mkBTyCon $ fmap (makeUnresolvedLHName (LHTcName LHAnyModuleNameF)) b) [t1,t2] [] trueURef @@ -458,9 +458,9 @@ bTyConP :: Parser BTyCon bTyConP = (reservedOp "'" >> mkPromotedBTyCon <$> locUpperIdLHNameP (LHDataConName LHAnyModuleNameF)) - <|> mkBTyCon <$> locUpperIdLHNameP LHTcName + <|> mkBTyCon <$> locUpperIdLHNameP (LHTcName LHAnyModuleNameF) <|> (reserved "*" >> - return (mkBTyCon (dummyLoc $ makeUnresolvedLHName LHTcName $ symbol ("*" :: String))) + return (mkBTyCon (dummyLoc $ makeUnresolvedLHName (LHTcName LHAnyModuleNameF) $ symbol ("*" :: String))) ) "bTyConP" @@ -471,7 +471,7 @@ mkPromotedBTyCon x = BTyCon x False True -- (consSym '\'' <$> x) False True classBTyConP :: Parser BTyCon -classBTyConP = mkClassBTyCon <$> locUpperIdLHNameP LHTcName +classBTyConP = mkClassBTyCon <$> locUpperIdLHNameP (LHTcName LHAnyModuleNameF) mkClassBTyCon :: Located LHName -> BTyCon mkClassBTyCon x = BTyCon x True False @@ -770,8 +770,8 @@ -> [RTPropV v BTyCon tv (UReftV v r)] -> r -> RTypeV v BTyCon tv (UReftV v r) -bLst (Just t) rs r = RApp (mkBTyCon $ dummyLoc $ makeUnresolvedLHName LHTcName listConName) [t] rs (reftUReft r) -bLst Nothing rs r = RApp (mkBTyCon $ dummyLoc $ makeUnresolvedLHName LHTcName listConName) [] rs (reftUReft r) +bLst (Just t) rs r = RApp (mkBTyCon $ dummyLoc $ makeUnresolvedLHName (LHTcName LHAnyModuleNameF) listConName) [t] rs (reftUReft r) +bLst Nothing rs r = RApp (mkBTyCon $ dummyLoc $ makeUnresolvedLHName (LHTcName LHAnyModuleNameF) listConName) [] rs (reftUReft r) bTup :: [(Maybe Symbol, BareTypeParsed)] -> [RTPropV LocSymbol BTyCon BTyVar (UReftV LocSymbol (ReftV LocSymbol))] @@ -781,13 +781,13 @@ | isTauto (fmap val r) = t | otherwise = t `strengthenUReft` reftUReft r bTup ts rs r - | all Mb.isNothing (fst <$> ts) || length ts < 2 + | all (Mb.isNothing . fst) ts || length ts < 2 = RApp - (mkBTyCon $ dummyLoc $ makeUnresolvedLHName LHTcName $ fromString $ "Tuple" ++ show (length ts)) + (mkBTyCon $ dummyLoc $ makeUnresolvedLHName (LHTcName LHAnyModuleNameF) $ tyTupleSizedSymbol (length ts)) (snd <$> ts) rs (reftUReft r) | otherwise = RApp - (mkBTyCon $ dummyLoc $ makeUnresolvedLHName LHTcName $ fromString $ "Tuple" ++ show (length ts)) + (mkBTyCon $ dummyLoc $ makeUnresolvedLHName (LHTcName LHAnyModuleNameF) $ tyTupleSizedSymbol (length ts)) (mapReft (const trueURef) . snd <$> ts) rs' (reftUReft r) @@ -845,7 +845,6 @@ go (PIff p1 p2) = PIff (go p1) (go p2) go (PAtom r e1 e2) = PAtom r (go e1) (go e2) go (PKVar k su') = PKVar k $ su' `appendSubst` su0 - go (PGrad k su' i e) = PGrad k (su' `appendSubst` su0) i (go e) go (PAll _ _) = panic Nothing "substExprV: PAll" go (PExist _ _) = panic Nothing "substExprV: PExist" go p = p @@ -887,9 +886,9 @@ | RInst (RInstance LocBareTypeParsed) -- ^ refined 'instance' definition | Invt LocBareTypeParsed -- ^ 'invariant' specification | Using (LocBareTypeParsed, LocBareTypeParsed) -- ^ 'using' declaration (for local invariants on a type) - | Alias (Located (RTAlias Symbol BareTypeParsed)) -- ^ 'type' alias declaration - | EAlias (Located (RTAlias Symbol (ExprV LocSymbol))) -- ^ 'predicate' alias declaration - | Embed (Located LHName, FTycon, TCArgs) -- ^ 'embed' declaration + | Alias (RTAlias Symbol BareTypeParsed) -- ^ 'type' alias declaration + | EAlias (RTAlias Symbol (ExprV LocSymbol)) -- ^ 'predicate' alias declaration + | Embed (Located LHName, Sort, TCArgs) -- ^ 'embed' declaration | Qualif (QualifierV LocSymbol) -- ^ 'qualif' definition | LVars (Located LHName) -- ^ 'lazyvar' annotation, defer checks to *use* sites | Lazy (Located LHName) -- ^ 'lazy' annotation, skip termination check on binder @@ -899,6 +898,7 @@ | Insts (Located LHName) -- ^ 'auto-inst' or 'ple' annotation; use ple locally on binder | HMeas (Located LHName) -- ^ 'measure' annotation; lift Haskell binder as measure | Reflect (Located LHName) -- ^ 'reflect' annotation; reflect Haskell binder as function in logic + | Stratified (Located LHName) -- ^ 'stratified' annotation; stratification check for type declarations | PrivateReflect LocSymbol -- ^ 'private-reflect' annotation | OpaqueReflect (Located LHName) -- ^ 'opaque-reflect' annotation | Inline (Located LHName) -- ^ 'inline' annotation; inline (non-recursive) binder as an alias @@ -956,9 +956,9 @@ = "invariant" <+> pprintTidy k (parsedToBareType <$> t) ppPspec k (Using (t1, t2)) = "using" <+> pprintTidy k (parsedToBareType <$> t1) <+> "as" <+> pprintTidy k (parsedToBareType <$> t2) -ppPspec k (Alias (Loc _ _ rta)) +ppPspec k (Alias rta) = "type" <+> pprintTidy k (fmap parsedToBareType rta) -ppPspec k (EAlias (Loc _ _ rte)) +ppPspec k (EAlias rte) = "predicate" <+> pprintTidy k rte ppPspec k (Embed (lx, tc, NoArgs)) = "embed" <+> pprintTidy k (val lx) <+> "as" <+> pprintTidy k tc @@ -984,6 +984,8 @@ = "measure" <+> pprintTidy k (val lx) ppPspec k (Reflect lx) = "reflect" <+> pprintTidy k (val lx) +ppPspec k (Stratified lx) + = "stratified" <+> pprintTidy k (val lx) ppPspec k (PrivateReflect lx) = "private-reflect" <+> pprintTidy k (val lx) ppPspec k (OpaqueReflect lx) @@ -1085,7 +1087,7 @@ , Measure.newtyDecls = [d | NTDecl d <- xs] , Measure.aliases = [a | Alias a <- xs] , Measure.ealiases = [e | EAlias e <- xs] - , Measure.embeds = tceFromList [(c, (fTyconSort tc, a)) | Embed (c, tc, a) <- xs] + , Measure.embeds = tceFromList [(c, (s, a)) | Embed (c, s, a) <- xs] , Measure.qualifiers = [q | Qualif q <- xs] , Measure.lvars = S.fromList [d | LVars d <- xs] , Measure.autois = S.fromList [s | Insts s <- xs] @@ -1106,6 +1108,7 @@ , 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.stratified = S.fromList [s | Stratified 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] @@ -1129,6 +1132,7 @@ -- TODO: These next two are synonyms, kill one <|> fallbackSpecP "axiomatize" (fmap Reflect locBinderLHNameP) <|> fallbackSpecP "reflect" (fmap Reflect locBinderLHNameP) + <|> fallbackSpecP "stratified" (fmap Stratified tyConThisModuleBindLHNameP) <|> (reserved "private-reflect" >> fmap PrivateReflect axiomP ) <|> (reserved "opaque-reflect" >> fmap OpaqueReflect locBinderLHNameP ) @@ -1205,7 +1209,7 @@ axiomP = locBinderP datavarianceP :: Parser (Located LHName, [Variance]) -datavarianceP = liftM2 (,) (locUpperIdLHNameP LHTcName) (many varianceP) +datavarianceP = liftM2 (,) (locUpperIdLHNameP (LHTcName LHAnyModuleNameF)) (many varianceP) dsizeP :: Parser ([Located BareTypeParsed], Located Symbol) dsizeP = liftM2 (,) (parens $ sepBy (located genBareTypeP) comma) locBinderP @@ -1280,35 +1284,33 @@ genBareTypeP :: Parser BareTypeParsed genBareTypeP = bareTypeP -embedP :: Parser (Located LHName, FTycon, TCArgs) +embedP :: Parser (Located LHName, Sort, TCArgs) embedP = do - x <- locUpperIdLHNameP LHTcName + x <- locUpperIdLHNameP (LHTcName LHAnyModuleNameF) a <- try (reserved "*" >> return WithArgs) <|> return NoArgs -- TODO: reserved "*" looks suspicious _ <- reserved "as" - t <- fTyConP - return (x, t, a) + s <- sortP + return (x, s, a) -- = xyP locUpperIdP symbolTCArgs (reserved "as") fTyConP -aliasP :: Parser (Located (RTAlias Symbol BareTypeParsed)) +aliasP :: Parser (RTAlias Symbol BareTypeParsed) aliasP = rtAliasP id bareTypeP "aliasP" -ealiasP :: Parser (Located (RTAlias Symbol (ExprV LocSymbol))) +ealiasP :: Parser (RTAlias Symbol (ExprV LocSymbol)) ealiasP = try (rtAliasP symbol predP) <|> rtAliasP symbol exprP "ealiasP" -- | Parser for a LH type synonym. -rtAliasP :: (Symbol -> tv) -> Parser ty -> Parser (Located (RTAlias tv ty)) +rtAliasP :: (Symbol -> tv) -> Parser ty -> Parser (RTAlias tv ty) rtAliasP f bodyP - = do pos <- getSourcePos - name <- upperIdP + = do lname <- locBinderLogicNameP args <- many aliasIdP reservedOp "=" body <- bodyP - posE <- getSourcePos let (tArgs, vArgs) = partition (isSmall . headSym) args - return $ Loc pos posE (RTA name (f <$> tArgs) vArgs body) + return $ RTA lname (f <$> tArgs) vArgs body logDefineP :: Parser BPspec logDefineP = @@ -1525,8 +1527,11 @@ bbindP = lowerIdP <* reservedOp "::" tyConBindLHNameP :: Parser (Located LHName) -tyConBindLHNameP = locUpperIdLHNameP LHTcName +tyConBindLHNameP = locUpperIdLHNameP (LHTcName LHAnyModuleNameF) +tyConThisModuleBindLHNameP :: Parser (Located LHName) +tyConThisModuleBindLHNameP = locUpperIdLHNameP (LHTcName LHThisModuleNameF) + dataConP :: [Symbol] -> Parser DataCtorParsed dataConP as = do x <- dataConLHNameP @@ -1593,7 +1598,7 @@ emptyDecl :: LocSymbol -> SourcePos -> Maybe (SizeFunV LocSymbol) -> DataDeclParsed emptyDecl x pos fsize@(Just _) - = DataDecl (DnName $ makeUnresolvedLHName LHTcName <$> x) [] [] Nothing pos fsize Nothing DataUser + = DataDecl (DnName $ makeUnresolvedLHName (LHTcName LHAnyModuleNameF) <$> x) [] [] Nothing pos fsize Nothing DataUser emptyDecl x pos _ = uError (ErrBadData (sourcePosSrcSpan pos) (pprint (val x)) msg) where @@ -1609,7 +1614,7 @@ return $ DataDecl dn as ps (Just dcs) pos fsize pTy DataUser dataDeclName :: SourcePos -> LocSymbol -> Bool -> [DataCtorParsed] -> DataName -dataDeclName _ x True _ = DnName $ makeUnresolvedLHName LHTcName <$> x -- vanilla data declaration +dataDeclName _ x True _ = DnName $ makeUnresolvedLHName (LHTcName LHAnyModuleNameF) <$> x -- vanilla data declaration dataDeclName _ _ False (d:_) = DnCon $ dcName d -- family instance declaration dataDeclName p x _ _ = uError (ErrBadData (sourcePosSrcSpan p) (pprint (val x)) msg) where diff --git a/src/Language/Haskell/Liquid/Transforms/ANF.hs b/src/Language/Haskell/Liquid/Transforms/ANF.hs --- a/src/Language/Haskell/Liquid/Transforms/ANF.hs +++ b/src/Language/Haskell/Liquid/Transforms/ANF.hs @@ -13,7 +13,6 @@ import Debug.Trace (trace) import Prelude hiding (error) -import Language.Haskell.Liquid.GHC.TypeRep import Liquid.GHC.API as Ghc hiding ( get, mkTyArg , showPpr , DsM @@ -36,6 +35,7 @@ import Data.Hashable import Data.HashMap.Strict (HashMap) import qualified Data.HashMap.Strict as HM +import GHC.Core.Type (ForAllTyBinder) -------------------------------------------------------------------------------- -- | A-Normalize a module ------------------------------------------------------ @@ -70,20 +70,20 @@ where t' = subst msg as as' bt msg = "WARNING: unable to renameVars on " ++ GM.showPpr x - as' = fst $ splitForAllTyCoVars $ exprType e - (as, bt) = splitForAllTyCoVars (varType x) + as' = fst $ splitForAllForAllTyBinders $ exprType e + (as, bt) = splitForAllForAllTyBinders (varType x) normalizeTyVars (Rec xes) = Rec xes' where nrec = normalizeTyVars <$> (uncurry NonRec <$> xes) xes' = (\case NonRec x e -> (x, e); _ -> impossible Nothing "This cannot happen") <$> nrec -subst :: String -> [TyVar] -> [TyVar] -> Type -> Type +subst :: String -> [ForAllTyBinder] -> [ForAllTyBinder] -> Type -> Type subst msg as as' bt | length as == length as' - = mkForAllTys (mkTyArg <$> as') $ substTy su bt + = mkForAllTys as' $ substTy su bt | otherwise - = trace msg $ mkForAllTys (mkTyArg <$> as) bt - where su = mkTvSubstPrs $ zip as (mkTyVarTys as') + = trace msg $ mkForAllTys as bt + where su = mkTvSubstPrs $ zip (map binderVar as) (mkTyVarTys (map binderVar as')) -- | eta-expand CoreBinds with quantified types normalizeForAllTys :: CoreExpr -> CoreExpr diff --git a/src/Language/Haskell/Liquid/Transforms/InlineAux.hs b/src/Language/Haskell/Liquid/Transforms/InlineAux.hs --- a/src/Language/Haskell/Liquid/Transforms/InlineAux.hs +++ b/src/Language/Haskell/Liquid/Transforms/InlineAux.hs @@ -61,7 +61,7 @@ _ -> False dfunIdSubst :: DFunId -> CoreExpr -> M.HashMap Id (Id, M.HashMap Id Id) -dfunIdSubst dfunId e = M.fromList $ zip auxIds (repeat (dfunId, methodToAux)) +dfunIdSubst dfunId e = M.fromList [(auxId, (dfunId, methodToAux)) | auxId <- auxIds] where methodToAux = M.fromList [ (m, aux) | m <- methods, aux <- auxIds, aux `isClassOpAuxOf` m ] diff --git a/src/Language/Haskell/Liquid/Types/Errors.hs b/src/Language/Haskell/Liquid/Types/Errors.hs --- a/src/Language/Haskell/Liquid/Types/Errors.hs +++ b/src/Language/Haskell/Liquid/Types/Errors.hs @@ -284,8 +284,8 @@ } -- ^ sort error in specification | ErrDupAlias { pos :: !SrcSpan - , var :: !Doc , kind :: !Doc + , var :: !Doc , locs :: ![SrcSpan] } -- ^ multiple alias with same name error @@ -311,9 +311,10 @@ } -- ^ duplicate fields in same datacon | ErrDupNames { pos :: !SrcSpan + , kind :: !Doc , var :: !Doc , names :: ![Doc] - } -- ^ name resolves to multiple possible GHC vars + } -- ^ name resolves to multiple matches | ErrBadData { pos :: !SrcSpan , var :: !Doc @@ -484,10 +485,41 @@ | ErrCtorRefinement { pos :: !SrcSpan , ctorName :: !Doc - } -- ^ The refinement of a data constructor doesn't admit - -- a refinement on the return type that - -- isn't deemd safe - + } + -- ^ The refinement of a data constructor doesn't admit a + -- refinement on the return type that isn't deemd safe + | ErrStratNotAdt { pos :: !SrcSpan + , tyName :: !Doc + } + -- ^ Type was declared stratified but it is not an ADT + | ErrStratNotRefCtor { pos :: !SrcSpan + , ctorName :: !Doc + , tyName :: !Doc + } + -- ^ Type was declared stratified but one of its constructors is not a + -- refinement constructor (i.e. it has no refinement) + | ErrStratNotPropRet { pos :: !SrcSpan + , tyName :: !Doc + , ctorName :: !Doc + , retTy :: !Doc + } + -- ^ Type was declared stratified but one of its constructors does not + -- return a Prop type + | ErrStratOccProp { pos :: !SrcSpan + , tyName :: !Doc + , ctorName :: !Doc + , tyNR :: !Doc + } + -- ^ Type was declared stratified but one of its constructors has a recursive + -- occurence that is not a Prop type + | ErrStratIdxNotSmall { pos :: !SrcSpan + , tyName :: !Doc + , ctorName :: !Doc + , retIdx :: !Doc + , occIdx :: !Doc + } + -- ^ Type was declared stratified but one of its constructors has a recursive + -- occurence whose index type is not a smaller | ErrOther { pos :: SrcSpan , msg :: !Doc } -- ^ Sigh. Other. @@ -901,8 +933,8 @@ $+$ dCtx $+$ nest 4 (text "Duplicated definitions for field" <+> ppTicks x) -ppError' _ dCtx (ErrDupNames _ x ns) - = text "Ambiguous specification symbol" <+> ppTicks x +ppError' _ dCtx (ErrDupNames _ k v ns) + = text "Ambiguous specification symbol" <+> ppTicks v <+> "for" <+> pprint k $+$ dCtx $+$ ppNames ns @@ -1063,13 +1095,50 @@ , "To deactivate or understand the need of positivity check, see:" , " " , nest 2 "https://ucsd-progsys.github.io/liquidhaskell/options/#positivity-check" + , "or consider making the type stratified" + , nest 2 "http://ucsd-progsys.github.io/liquidhaskell/specifications/#stratified-types" ] ppError' _ dCtx (ErrCtorRefinement _ ctorName) = text "Refinement of the data constructor" <+> ctorName <+> "doesn't admit an arbitrary refinements on the return type" $+$ dCtx - $+$ nest 4 (text "Were you trying to use `Prop` from `Language.Haskell.Liquid.ProofCombinators`?") + $+$ nest 4 (text "Were you trying to use `Ix` from `Language.Haskell.Liquid.ProofCombinators`?") $+$ nest 4 (text "You can disable this error by enabling the flag `--allow-unsafe-constructors`") + +ppError' _ dCtx (ErrStratNotAdt _ tyName) + = text "The type" <+> tyName + <+> "was declared stratified but it is not an algebraic data type" + $+$ dCtx + +ppError' _ dCtx (ErrStratNotRefCtor _ ctorName tyName) + = text "The constructor" <+> ctorName + <+> "of the type" <+> tyName + <+> "was declared stratified but it is not a refinement constructor (i.e. it has no refinement)" + $+$ dCtx + +ppError' _ dCtx (ErrStratNotPropRet _ tyName ctorName retTy) + = text "The constructor" <+> ctorName + <+> "of the type" <+> tyName + <+> "was declared stratified but it does not return an indexed type, instead it returns" + <+> retTy + $+$ dCtx + +ppError' _ dCtx (ErrStratOccProp _ tyName ctorName tyNR) + = text "The constructor" <+> ctorName + <+> "of the type" <+> tyName + <+> "was declared stratified but it has a recursive occurence of type" + <+> tyNR + <+> "which is not an indexed type" + $+$ dCtx + +ppError' _ dCtx (ErrStratIdxNotSmall _ tyName ctorName retIdx occIdx) + = text "The constructor" <+> ctorName + <+> "of the type" <+> tyName + <+> "was declared stratified but it has a recursive occurence whose index" + <+> occIdx + <+> "is not smaller than the return index" + <+> retIdx + $+$ dCtx ppError' _ dCtx (ErrParseAnn _ msg) = text "Malformed annotation" diff --git a/src/Language/Haskell/Liquid/Types/Names.hs b/src/Language/Haskell/Liquid/Types/Names.hs --- a/src/Language/Haskell/Liquid/Types/Names.hs +++ b/src/Language/Haskell/Liquid/Types/Names.hs @@ -6,7 +6,12 @@ module Language.Haskell.Liquid.Types.Names ( lenLocSymbol , anyTypeSymbol + , propSymbol + , getPropIndex , selfSymbol + , tyTupleSizedSymbol + , isTyTupleSizedSymbol + , tmTupleSizedSymbol , LogicName (..) , LHResolvedName (..) , LHName (..) @@ -32,6 +37,10 @@ , reflectGHCName , reflectLHName , updateLHNameSymbol + , isNonReflectedLogicName + , logicNameOriginModule + , isResolvedLogicName + , isGeneratedLogicName ) where import Control.DeepSeq @@ -39,6 +48,7 @@ import Data.Data (Data, gmapM, gmapT) import Data.Generics (extM, extT) import Data.Hashable +import Data.Maybe (isNothing) import Data.String (fromString) import qualified Data.Text as Text import GHC.Generics @@ -46,10 +56,21 @@ import GHC.Stack import Language.Fixpoint.Types import Language.Haskell.Liquid.GHC.Misc ( locNamedThing ) -- Symbolic GHC.Name +import Text.Read (readMaybe) import qualified Liquid.GHC.API as GHC import GHC.Types (Any) +propSymbol :: Symbol +propSymbol = "Language.Haskell.Liquid.ProofCombinators.prop" + +getPropIndex :: ReftV Symbol -> Maybe (ExprV Symbol) +getPropIndex (Reft (v, PAtom Eq (EApp (EVar n) (EVar v')) idx)) + | n == propSymbol + , v == v' + = Just idx +getPropIndex _ = Nothing + -- RJ: Please add docs lenLocSymbol :: Located Symbol lenLocSymbol = dummyLoc $ symbol ("autolen" :: String) @@ -60,6 +81,20 @@ selfSymbol :: Symbol selfSymbol = symbol ("liquid_internal_this" :: String) +tyTupleSizedSymbol :: Int -> Symbol +tyTupleSizedSymbol n | n < 0 = error "tyTupleSizedSymbol: negative arity" + | otherwise = symbol $ "Tuple" ++ show n + +isTyTupleSizedSymbol :: Symbol -> Maybe Int +isTyTupleSizedSymbol s = Text.stripPrefix "Tuple" (symbolText s) + >>= readMaybe . Text.unpack + +tmTupleSizedSymbol :: Int -> Symbol +tmTupleSizedSymbol n | n < 0 = error "tmTupleSizedSymbol: negative arity" + | n == 0 = "()" + | n == 1 = "MkSolo" + | otherwise = symbol $ "(" <> replicate (n - 1) ',' <> ")" + -- | A name for an entity that does not exist in Haskell -- -- For instance, this can be used to represent predicate aliases @@ -89,7 +124,8 @@ LHRIndex Word deriving (Data, Eq, Generic, Ord) --- | A name that is potentially unresolved. +-- | A name that is potentially unresolved, carrying along the 'Symbol' +-- found by the parser. data LHName = -- | In order to integrate the resolved names gradually, we keep the -- unresolved names. @@ -117,11 +153,11 @@ hashWithSalt s (LHNUnresolved ns sym) = s `hashWithSalt` ns `hashWithSalt` sym data LHNameSpace - = LHTcName - | LHDataConName LHThisModuleNameFlag - | LHVarName LHThisModuleNameFlag - | LHLogicNameBinder - | LHLogicName + = LHTcName LHThisModuleNameFlag -- ^ Type constructors + | LHDataConName LHThisModuleNameFlag -- ^ Data constructors with procedence + | LHVarName LHThisModuleNameFlag -- ^ Variables with procedence + | LHLogicNameBinder -- ^ Logic names (LHS) + | LHLogicName -- ^ Logic names (RHS) deriving (Data, Eq, Generic, Ord, Show) instance B.Binary LHNameSpace @@ -374,6 +410,21 @@ ) (symbol n) +isNonReflectedLogicName :: LHName -> Bool +isNonReflectedLogicName lhname = isResolvedLogicName lhname && (isNothing . maybeReflectedLHName) lhname + maybeReflectedLHName :: LHName -> Maybe GHC.Name maybeReflectedLHName (LHNResolved (LHRLogic (LogicName _ _ m)) _) = m maybeReflectedLHName _ = Nothing + +isResolvedLogicName :: LHName -> Bool +isResolvedLogicName (LHNResolved (LHRLogic (LogicName {})) _) = True +isResolvedLogicName _ = False + +isGeneratedLogicName :: LHName -> Bool +isGeneratedLogicName (LHNResolved (LHRLogic (GeneratedLogicName _)) _) = True +isGeneratedLogicName _ = False + +logicNameOriginModule :: LHName -> GHC.Module +logicNameOriginModule (LHNResolved (LHRLogic (LogicName _ m _)) _) = m +logicNameOriginModule n = error $ "logicNameOriginModule: Not a logic name " ++ show n diff --git a/src/Language/Haskell/Liquid/Types/PredType.hs b/src/Language/Haskell/Liquid/Types/PredType.hs --- a/src/Language/Haskell/Liquid/Types/PredType.hs +++ b/src/Language/Haskell/Liquid/Types/PredType.hs @@ -446,7 +446,7 @@ freeArgsPs p (RHole r) = freeArgsPsRef p r freeArgsPs p (RRTy env r _ t) - = L.nub $ concatMap (freeArgsPs p) (snd <$> env) ++ freeArgsPsRef p r ++ freeArgsPs p t + = L.nub $ concatMap (freeArgsPs p . snd) env ++ freeArgsPsRef p r ++ freeArgsPs p t freeArgsPsRef :: PVar t1 -> UReft t -> [F.Symbol] freeArgsPsRef p (MkUReft _ (Pr ps)) = [x | (_, x, w) <- concatMap pargs ps', F.EVar x == w] diff --git a/src/Language/Haskell/Liquid/Types/PrettyPrint.hs b/src/Language/Haskell/Liquid/Types/PrettyPrint.hs --- a/src/Language/Haskell/Liquid/Types/PrettyPrint.hs +++ b/src/Language/Haskell/Liquid/Types/PrettyPrint.hs @@ -64,6 +64,7 @@ import Language.Haskell.Liquid.GHC.Misc import Language.Haskell.Liquid.Misc import Language.Haskell.Liquid.Types.Errors +import Language.Haskell.Liquid.Types.Names (LHName (..), getLHNameSymbol, lhNameToResolvedSymbol) import Language.Haskell.Liquid.Types.RType import Language.Haskell.Liquid.Types.RTypeOp import Language.Haskell.Liquid.Types.Types @@ -169,6 +170,11 @@ , nest 2 $ text "axiom-map" , nest 4 $ pprint am ] + +instance F.Fixpoint LHName where + toFix lhname = case lhname of + LHNUnresolved { } -> pprintSymbol . getLHNameSymbol $ lhname + LHNResolved { } -> pprint . lhNameToResolvedSymbol $ lhname -------------------------------------------------------------------------------- -- | Pretty Printing RefType --------------------------------------------------- diff --git a/src/Language/Haskell/Liquid/Types/RType.hs b/src/Language/Haskell/Liquid/Types/RType.hs --- a/src/Language/Haskell/Liquid/Types/RType.hs +++ b/src/Language/Haskell/Liquid/Types/RType.hs @@ -54,6 +54,9 @@ , Predicate , PredicateV (..) + -- * Expression Arguments + , notExprArg + -- * Manipulating `Predicates` , emapExprVM , mapPredicateV @@ -336,9 +339,8 @@ PKVar k su -> PKVar k <$> emapSubstVM (f . (domain su ++) . (acc ++)) su PAll bnds e -> PAll bnds <$> go (map fst bnds ++ acc) e PExist bnds e -> PExist bnds <$> go (map fst bnds ++ acc) e - PGrad k su gi e -> - PGrad k <$> emapSubstVM (f . (acc ++)) su <*> pure gi <*> go (domain su ++ acc) e ECoerc srt0 srt1 e -> ECoerc srt0 srt1 <$> go acc e + ELet x e1 e2 -> ELet x <$> go acc e1 <*> go (x:acc) e2 domain (Su m) = M.keys m @@ -776,6 +778,10 @@ makeRTVar :: tv -> RTVar tv s makeRTVar a = RTVar a (RTVNoInfo True) +notExprArg :: RTypeV v c tv r -> Bool +notExprArg (RExprArg _) = False +notExprArg _ = True + instance (Eq tv) => Eq (RTVar tv s) where t1 == t2 = ty_var_value t1 == ty_var_value t2 @@ -857,7 +863,7 @@ emapUReftVM f g (MkUReft r p) = MkUReft <$> g r <*> emapPredicateVM f p type BRType = RTypeV Symbol BTyCon BTyVar -- ^ "Bare" parsed version -type BRTypeV v = RTypeV v BTyCon BTyVar -- ^ "Bare" parsed version +type BRTypeV v = RTypeV v BTyCon BTyVar -- ^ "Bare" parsed version type RRType = RTypeV Symbol RTyCon RTyVar -- ^ "Resolved" version type BSort = BRType () type BSortV v = BRTypeV v () diff --git a/src/Language/Haskell/Liquid/Types/RefType.hs b/src/Language/Haskell/Liquid/Types/RefType.hs --- a/src/Language/Haskell/Liquid/Types/RefType.hs +++ b/src/Language/Haskell/Liquid/Types/RefType.hs @@ -107,7 +107,7 @@ import Text.PrettyPrint.HughesPJ hiding ((<>), first) import Language.Fixpoint.Misc import Language.Fixpoint.Types hiding (DataDecl (..), DataCtor (..), panic, shiftVV, Predicate, isNumeric) -import Language.Fixpoint.Types.Visitor (mapKVars, Visitable) +import Language.Fixpoint.Types.Visitor (trans, Visitable) import qualified Language.Fixpoint.Types as F import Language.Haskell.Liquid.Types.Errors import Language.Haskell.Liquid.Types.PrettyPrint @@ -550,8 +550,8 @@ tyConBTyCon :: TyCon -> BTyCon tyConBTyCon tc = - mkBTyCon $ - makeResolvedLHName (LHRGHC (getName tc)) . tyConName <$> GM.locNamedThing tc + mkBTyCon $ + makeResolvedLHName (LHRGHC (getName tc)) . tyConName <$> GM.locNamedThing tc --- NV TODO : remove this code!!! @@ -1431,12 +1431,12 @@ = mkEApp (dummyLoc $ symbol c) (eVar <$> xs) isBaseDataCon :: DataCon -> Bool -isBaseDataCon c = and $ isBaseTy <$> map irrelevantMult (dataConOrigArgTys c ++ dataConRepArgTys c) +isBaseDataCon c = all (isBaseTy . irrelevantMult) (dataConOrigArgTys c ++ dataConRepArgTys c) isBaseTy :: Type -> Bool isBaseTy (TyVarTy _) = True isBaseTy (AppTy _ _) = False -isBaseTy (TyConApp _ ts) = and $ isBaseTy <$> ts +isBaseTy (TyConApp _ ts) = all isBaseTy ts isBaseTy FunTy{} = False isBaseTy (ForAllTy _ _) = False isBaseTy (LitTy _) = True @@ -1476,9 +1476,6 @@ = TyVarTy α toType useRFInfo (RApp RTyCon{rtc_tc = c} ts _ _) = TyConApp c (toType useRFInfo <$> filter notExprArg ts) - where - notExprArg (RExprArg _) = False - notExprArg _ = True toType useRFInfo (RAllE _ _ t) = toType useRFInfo t toType useRFInfo (REx _ _ t) @@ -1541,18 +1538,37 @@ rTypeSort tce = typeSort tce . toType True -------------------------------------------------------------------------------- -applySolution :: (Functor f) => FixSolution -> f SpecType -> f SpecType +applySolution + :: (Functor f) + => FInfo a -> M.HashMap KVar (Delayed Expr) -> f SpecType -> f SpecType -------------------------------------------------------------------------------- -applySolution = fmap . fmap . mapReft' . appSolRefa +applySolution si = fmap . fmap . mapReft' . appSolRefa si where mapReft' f (MkUReft (Reft (x, z)) p) = MkUReft (Reft (x, f z)) p appSolRefa :: Visitable t - => M.HashMap KVar Expr -> t -> t -appSolRefa s p = mapKVars f p + => GInfo c a -> M.HashMap KVar (Delayed Expr) -> t -> t +appSolRefa si s = mapKVars f0 where - f k = Just $ M.lookupDefault PTop k s + f0 k = Just $ forceDelayed $ M.lookupDefault (Delayed PTop) k s + mapKVars :: Visitable t => (KVar -> Maybe Expr) -> t -> t + mapKVars f = trans txK + where + txK (PKVar k su) + | Just p' <- f k = + rapierSubstExpr (substSymbolsSet su) (renameDomain k su) p' + txK p = p + + -- The parameters of kvars all seem to have prefix $ and suffix ##k_ + -- at the point where mapKVars is used. We compensate for that here. + renameDomain k (Su m) = + Su $ M.fromList + [ (consSym '$' (suffixSymbol v "k_"), e) + | v <- kvarDomain si k + , let e = M.lookupDefault (EVar v) v m + ] + -------------------------------------------------------------------------------- -- shiftVV :: Int -- SpecType -> Symbol -> SpecType shiftVV :: (TyConable c, Reftable (f Reft), Functor f) @@ -1583,7 +1599,7 @@ -- MOVE TO TYPES instance (Show tv, Show ty) => Show (RTAlias tv ty) where show (RTA n as xs t) = - printf "type %s %s %s = %s" (symbolString n) + printf "type %s %s %s = %s" (symbolString . getLHNameSymbol . val $ n) (unwords (show <$> as)) (unwords (show <$> xs)) (show t) @@ -1611,10 +1627,13 @@ go τ = FObj (typeUniqueSymbol τ) tyConFTyCon :: TCEmb TyCon -> TyCon -> [Sort] -> Sort -tyConFTyCon tce c ts = case tceLookup c tce of - Just (t, WithArgs) -> t - Just (t, NoArgs) -> fApp t ts - Nothing -> fApp (fTyconSort niTc) ts +-- ignore the nat arguments of the Any types, see test/pos/T2535A.hs +-- tyConFTyCon _ c _ | Ghc.zonkAnyTyCon == c = FObj (symbol c) +tyConFTyCon tce c ts = + case tceLookup c tce of + Just (t, WithArgs) -> t + Just (t, NoArgs) -> fApp t ts + Nothing -> fApp (fTyconSort niTc) ts where niTc = symbolNumInfoFTyCon (dummyLoc $ tyConName c) (isNumCls c) (isFracCls c) -- oldRes = F.notracepp _msg $ M.lookupDefault def c tce diff --git a/src/Language/Haskell/Liquid/Types/Specs.hs b/src/Language/Haskell/Liquid/Types/Specs.hs --- a/src/Language/Haskell/Liquid/Types/Specs.hs +++ b/src/Language/Haskell/Liquid/Types/Specs.hs @@ -55,6 +55,7 @@ , SpecMeasure , VarOrLocSymbol , emapSpecM + , emapRTAlias , fromBareSpecLHName , fromBareSpecParsed , mapSpecLName @@ -147,7 +148,7 @@ In order to produce these spec types we have to gather information about the module being compiled by using the GHC API and retain enough context of the compiled 'Module' in order to be able to construct the types -introduced aboves. The rest of this module introduced also these intermediate structures. +introduced above. The rest of this module introduces also these intermediate structures. -} -- $targetInfo @@ -166,9 +167,9 @@ getConfig = getConfig . giSpec -- | The 'TargetSrc' type is a collection of all the things we know about a module being currently --- checked. It include things like the name of the module, the list of 'CoreBind's, +-- checked. It includes things like the name of the module, the list of 'CoreBind's, -- the 'TyCon's declared in this module (that includes 'TyCon's for classes), typeclass instances --- and so and so forth. It might be consider a sort of 'ModGuts' embellished with LH-specific +-- and so on and so forth. It might be considered a sort of 'ModGuts' embellished with LH-specific -- information (for example, 'giDefVars' are populated with datacons from the module plus the -- let vars derived from the A-normalisation). data TargetSrc = TargetSrc @@ -197,7 +198,7 @@ -- | A 'TargetSpec' is what we /actually check via LiquidHaskell/. It is created as part of 'mkTargetSpec' -- alongside the 'LiftedSpec'. It shares a similar structure with a 'BareSpec', but manipulates and --- transforms the data in preparation to the checking process. +-- transforms the data in preparation for the checking process. data TargetSpec = TargetSpec { gsSig :: !GhcSpecSig , gsQual :: !GhcSpecQual @@ -242,6 +243,7 @@ data GhcSpecSig = SpSig { gsTySigs :: ![(Var, LocSpecType)] -- ^ Asserted Reftypes + , gsStratCtos :: ![Name] -- ^ Stratified Ctors , gsAsmSigs :: ![(Var, LocSpecType)] -- ^ Assumed Reftypes , gsAsmReflects :: ![(Var, Var)] -- ^ Assumed Reftypes (left is the actual function name and right the pretended one) , gsRefSigs :: ![(Var, LocSpecType)] -- ^ Reflected Reftypes @@ -258,6 +260,7 @@ instance Semigroup GhcSpecSig where x <> y = SpSig { gsTySigs = gsTySigs x <> gsTySigs y + , gsStratCtos = gsStratCtos x <> gsStratCtos y , gsAsmSigs = gsAsmSigs x <> gsAsmSigs y , gsAsmReflects = gsAsmReflects x <> gsAsmReflects y , gsRefSigs = gsRefSigs x <> gsRefSigs y @@ -277,7 +280,7 @@ instance Monoid GhcSpecSig where - mempty = SpSig mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty + mempty = SpSig mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty data GhcSpecData = SpData { gsCtors :: ![(Var, LocSpecType)] -- ^ Data Constructor Measure Sigs @@ -359,7 +362,7 @@ -- $bareSpec -- | A 'BareSpec' is the spec we derive by parsing the Liquid Haskell annotations of a single file. As --- such, it contains things which are relevant for validation and lifting; it contains things like +-- such, it contains things which are relevant for validation and lifting: -- the pragmas the user defined, the termination condition (if termination-checking is enabled) and so -- on and so forth. /Crucially/, as a 'BareSpec' is still subject to \"preflight checks\", it may contain -- duplicates (e.g. duplicate measures, duplicate type declarations etc.) and therefore most of the fields @@ -387,8 +390,8 @@ , ialiases :: ![(F.Located ty, F.Located ty)] -- ^ Data type invariants to be checked , dataDecls :: ![DataDeclP lname ty] -- ^ Predicated data definitions , newtyDecls :: ![DataDeclP lname ty] -- ^ Predicated new type definitions - , aliases :: ![F.Located (RTAlias F.Symbol (BareTypeV lname))] -- ^ RefType aliases - , ealiases :: ![F.Located (RTAlias F.Symbol (F.ExprV lname))] -- ^ Expression aliases + , aliases :: ![RTAlias F.Symbol (BareTypeV lname)] -- ^ RefType aliases + , ealiases :: ![RTAlias F.Symbol (F.ExprV lname)] -- ^ Expression aliases. See [NOTE:EXPRESSION-ALIASES] , embeds :: !(F.TCEmb (F.Located LHName)) -- ^ GHC-Tycon-to-fixpoint Tycon map , qualifiers :: ![F.QualifierV lname] -- ^ Qualifiers in source files , lvars :: !(S.HashSet (F.Located LHName)) -- ^ Variables that should be checked in the environment they are used @@ -397,13 +400,14 @@ , 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.Located LHName)) -- ^ Binders to reflect + , stratified :: !(S.HashSet (F.Located LHName)) -- ^ Type declaration to check for stratification , 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.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 + , autosize :: !(S.HashSet (F.Located LHName)) -- ^ Type Constructors that get sizing info automatically , pragmas :: ![F.Located String] -- ^ Command-line configurations passed in through source , cmeasures :: ![MeasureV lname (F.Located ty) ()] -- ^ Measures attached to a type-class , imeasures :: ![MeasureV lname (F.Located ty) (F.Located LHName)] -- ^ Mappings from (measure,type) -> measure @@ -439,7 +443,7 @@ :: Monad m => -- | The bscope setting, which affects which names - -- are considered to be in scope in refinment types. + -- are considered to be in scope in refinement types. Bool -- | For names that have a local environment return the names in scope. -> (LHName -> [F.Symbol]) @@ -460,8 +464,8 @@ ialiases <- mapM (bimapM (traverse fnull) (traverse fnull)) (ialiases sp) dataDecls <- mapM (emapDataDeclM bscp vf f) (dataDecls sp) newtyDecls <- mapM (emapDataDeclM bscp vf f) (newtyDecls sp) - aliases <- mapM (traverse (emapRTAlias (emapBareTypeVM bscp vf))) (aliases sp) - ealiases <- mapM (traverse (emapRTAlias (\e -> emapExprVM (vf . (++ e))))) $ ealiases sp + aliases <- mapM (emapRTAlias (emapBareTypeVM bscp vf)) (aliases sp) + ealiases <- mapM (emapRTAlias (\e -> emapExprVM (vf . (++ e)))) (ealiases sp) qualifiers <- mapM (emapQualifierM vf) $ qualifiers sp cmeasures <- mapM (emapMeasureM vf (traverse . f)) (cmeasures sp) imeasures <- mapM (emapMeasureM vf (traverse . f)) (imeasures sp) @@ -569,8 +573,8 @@ , sigs = map (fmap (fmap (mapRTypeV f . mapReft (mapUReftV f (fmap f))))) sigs , dataDecls = map (mapDataDeclV f) dataDecls , newtyDecls = map (mapDataDeclV f) newtyDecls - , aliases = map (fmap (fmap (mapRTypeV f . fmap (mapUReftV f (fmap f))))) aliases - , ealiases = map (fmap (fmap (fmap f))) ealiases + , aliases = map (fmap (mapRTypeV f . fmap (mapUReftV f (fmap f)))) aliases + , ealiases = map (fmap (fmap f)) ealiases , qualifiers = map (fmap f) qualifiers , cmeasures = map (mapMeasureV f) cmeasures , imeasures = map (mapMeasureV f) imeasures @@ -588,8 +592,8 @@ mapRelationalV f1 (n0, n1, a, b, e0, e1) = (n0, n1, fmap (mapRTypeV f1 . mapReft (mapUReftV f1 (fmap f1))) a, fmap (mapRTypeV f1 . mapReft (mapUReftV f1 (fmap f1))) b, fmap f1 e0, fmap f1 e1) --- /NOTA BENE/: These instances below are considered legacy, because merging two 'Spec's together doesn't --- really make sense, and we provide this only for legacy purposes. +-- /NOTA BENE/: The instances below are provided for legacy purposes only, because merging two 'Spec's together doesn't +-- really make sense. instance Semigroup (Spec lname ty) where s1 <> s2 = Spec { measures = measures s1 ++ measures s2 @@ -623,6 +627,7 @@ , rewriteWith = M.union (rewriteWith s1) (rewriteWith s2) , fails = S.union (fails s1) (fails s2) , reflects = S.union (reflects s1) (reflects s2) + , stratified = S.union (stratified s1) (stratified s2) , privateReflects = S.union (privateReflects s1) (privateReflects s2) , opaqueReflects = S.union (opaqueReflects s1) (opaqueReflects s2) , hmeas = S.union (hmeas s1) (hmeas s2) @@ -659,6 +664,7 @@ , autois = S.empty , hmeas = S.empty , reflects = S.empty + , stratified = S.empty , privateReflects = S.empty , opaqueReflects = S.empty , inlines = S.empty @@ -687,7 +693,7 @@ -- The general motivations for lifting a spec are (a) name resolution, (b) the fact that some info is -- only relevant for checking the body of functions but does not need to be exported, e.g. -- termination measures, or the fact that a type signature was assumed. --- A 'LiftedSpec' is /what we serialise on disk and what the clients should will be using/. +-- A 'LiftedSpec' is /what we serialise on disk and what the clients will be using/. -- -- What we /do not/ have compared to a 'BareSpec': -- @@ -728,10 +734,10 @@ -- ^ Predicated data definitions , liftedNewtyDecls :: HashSet DataDeclLHName -- ^ Predicated new type definitions - , liftedAliases :: HashSet (F.Located (RTAlias F.Symbol BareTypeLHName)) + , liftedAliases :: HashSet (RTAlias F.Symbol BareTypeLHName) -- ^ RefType aliases - , liftedEaliases :: HashSet (F.Located (RTAlias F.Symbol (F.ExprV LHName))) - -- ^ Expression aliases + , liftedEaliases :: HashSet (RTAlias F.Symbol (F.ExprV LHName)) + -- ^ Expression aliases. See [NOTE:EXPR-ALIASES] , liftedEmbeds :: F.TCEmb (F.Located LHName) -- ^ GHC-Tycon-to-fixpoint Tycon map , liftedQualifiers :: HashSet (F.QualifierV LHName) @@ -1011,6 +1017,7 @@ , rewrites = mempty , rewriteWith = mempty , reflects = mempty + , stratified = mempty , privateReflects = liftedPrivateReflects a , opaqueReflects = mempty , autois = liftedAutois a diff --git a/src/Language/Haskell/Liquid/Types/Types.hs b/src/Language/Haskell/Liquid/Types/Types.hs --- a/src/Language/Haskell/Liquid/Types/Types.hs +++ b/src/Language/Haskell/Liquid/Types/Types.hs @@ -368,24 +368,29 @@ "\nRHS :" ++ showPpr rhs -------------------------------------------------------------------------------- --- | Refinement Type Aliases +-- | Refinement Type and Expression Aliases -------------------------------------------------------------------------------- data RTAlias x a = RTA - { rtName :: Symbol -- ^ name of the alias + { rtName :: F.Located LHName -- ^ name of the alias with its definition's location , rtTArgs :: [x] -- ^ type parameters , rtVArgs :: [Symbol] -- ^ value parameters , rtBody :: a -- ^ what the alias expands to - -- , rtMod :: !ModName -- ^ module where alias was defined } deriving (Eq, Data, Generic, Functor, Foldable, Traversable) deriving Hashable via Generically (RTAlias x a) deriving B.Binary via Generically (RTAlias x a) -- TODO support ghosts in aliases? +-- | A map over a 'RTAlias' type parameters. mapRTAVars :: (a -> b) -> RTAlias a ty -> RTAlias b ty mapRTAVars f rt = rt { rtTArgs = f <$> rtTArgs rt } -lmapEAlias :: LMap -> F.Located (RTAlias Symbol Expr) -lmapEAlias (LMap v ys e) = F.atLoc v (RTA (F.val v) [] ys e) -- (F.loc v) (F.loc v) +-- | Transform a logic equation to an expression alias. +-- +-- Used when constructing 'Language.Haskell.Liquid.Types.Specs.GhcSpec' +-- to include Haskell inlines and 'LogicMap' definitions in the alias +-- environment for expansion. See [NOTE:EXPRESSION-ALIASES] +lmapEAlias :: LMap -> RTAlias Symbol Expr +lmapEAlias (LMap v ys e) = RTA (makeGeneratedLogicLHName <$> v) [] ys e -- | The type used during constraint generation, used @@ -558,11 +563,11 @@ getModString = moduleNameString . getModName -------------------------------------------------------------------------------- --- | Refinement Type Aliases --------------------------------------------------- +-- | Refinement Type and Expression Aliases Environment -------------------------------------------------------------------------------- data RTEnv tv t = RTE - { typeAliases :: M.HashMap Symbol (F.Located (RTAlias tv t)) - , exprAliases :: M.HashMap Symbol (F.Located (RTAlias Symbol Expr)) + { typeAliases :: M.HashMap LHName (RTAlias tv t) + , exprAliases :: M.HashMap LHName (RTAlias Symbol Expr) } diff --git a/src/Language/Haskell/Liquid/UX/Annotate.hs b/src/Language/Haskell/Liquid/UX/Annotate.hs --- a/src/Language/Haskell/Liquid/UX/Annotate.hs +++ b/src/Language/Haskell/Liquid/UX/Annotate.hs @@ -78,9 +78,9 @@ -- | @output@ creates the pretty printed output -------------------------------------------------------------------------------------------- -mkOutput :: Config -> ErrorResult -> FixSolution -> AnnInfo (Annot SpecType) -> Output Doc +mkOutput :: Config -> ErrorResult -> FInfo a -> FixDelayedSolution -> AnnInfo (Annot SpecType) -> Output Doc -------------------------------------------------------------------------------------------- -mkOutput cfg res sol anna +mkOutput cfg res si sol anna = O { o_vars = Nothing -- , o_errors = [] , o_types = toDoc <$> annTy @@ -90,7 +90,7 @@ } where annTmpl = closeAnnots anna - annTy = tidySpecType Lossy <$> applySolution sol annTmpl + annTy = tidySpecType Lossy <$> applySolution si sol annTmpl toDoc = rtypeDoc tidy tidy = if shortNames cfg then Lossy else Full diff --git a/src/Language/Haskell/Liquid/UX/CmdLine.hs b/src/Language/Haskell/Liquid/UX/CmdLine.hs --- a/src/Language/Haskell/Liquid/UX/CmdLine.hs +++ b/src/Language/Haskell/Liquid/UX/CmdLine.hs @@ -20,14 +20,11 @@ module Language.Haskell.Liquid.UX.CmdLine ( -- * Get Command Line Configuration - getOpts, mkOpts, defConfig, config + getOpts, defConfig -- * Update Configuration With Pragma , withPragmas - -- * Canonicalize Paths in Config - , canonicalizePaths - -- * Collecting errors , addErrors @@ -59,11 +56,9 @@ import System.Console.CmdArgs.Text import GitHash -import Data.List (nub) +import Data.List (nub, intercalate) -import System.FilePath (isAbsolute, takeDirectory, ()) - import qualified Language.Fixpoint.Types.Config as FC import qualified Language.Fixpoint.Misc as F import Language.Fixpoint.Types.Names @@ -97,7 +92,10 @@ -- Parsing Command Line---------------------------------------------------------- --------------------------------------------------------------------------------- config :: Mode (CmdArgs Config) -config = cmdArgsMode $ Config { +config = cmdArgsMode defConfig + +defConfig :: Config +defConfig = Config { loggingVerbosity = enum [ Minimal &= name "minimal" &= help "Minimal logging verbosity" , Quiet &= name "quiet" &= help "Silent logging verbosity" @@ -105,15 +103,6 @@ , Loud &= name "verbose" &= help "Verbose logging" ] - , files - = def &= typ "TARGET" - &= args - &= typFile - - , idirs - = def &= typDir - &= help "Paths to Spec Include Directory " - , fullcheck = def &= help "Full Checking: check all binders (DEFAULT)" @@ -150,25 +139,25 @@ &= name "check-var" , pruneUnsorted - = def &= help "Disable prunning unsorted Predicates" + = False &= help "Disable prunning unsorted Predicates" &= name "prune-unsorted" , notermination - = def + = False &= help "Disable Termination Check" &= name "no-termination-check" , nopositivity - = def + = False &= help "Disable Data Type Positivity Check" &= name "no-positivity-check" , rankNTypes - = def &= help "Adds precise reasoning on presence of rankNTypes" + = False &= help "Adds precise reasoning on presence of rankNTypes" &= name "rankNTypes" , noclasscheck - = def + = False &= help "Disable Class Instance Check" &= name "no-class-check" @@ -176,37 +165,24 @@ = def &= name "no-structural-termination" &= help "Disable structural termination check" - , gradual - = def &= help "Enable gradual refinement type checking" - &= name "gradual" - , bscope - = def &= help "scope of the outer binders on the inner refinements" + = False &= help "scope of the outer binders on the inner refinements" &= name "bscope" - , gdepth - = 1 - &= help "Size of gradual conretizations, 1 by default" - &= name "gradual-depth" - - , ginteractive - = def &= help "Interactive Gradual Solving" - &= name "ginteractive" - , totalHaskell - = def &= help "Check for termination and totality; overrides no-termination flags" + = False &= help "Check for termination and totality; overrides no-termination flags" &= name "total-Haskell" , nowarnings - = def &= help "Don't display warnings, only show errors" + = False &= help "Don't display warnings, only show errors" &= name "no-warnings" , noannotations - = def &= help "Don't create intermediate annotation files" + = False &= help "Don't create intermediate annotation files" &= name "no-annotations" , checkDerived - = def &= help "Check GHC generated binders (e.g. Read, Show instances)" + = False &= help "Check GHC generated binders (e.g. Read, Show instances)" &= name "check-derived" , caseExpandDepth @@ -214,15 +190,15 @@ &= name "max-case-expand" , notruetypes - = def &= help "Disable Trueing Top Level Types" + = False &= help "Disable Trueing Top Level Types" &= name "no-true-types" , nototality - = def &= help "Disable totality check" + = False &= help "Disable totality check" &= name "no-totality" , cores - = def &= help "Use m cores to solve logical constraints" + = Just 1 &= help "Use the given number of cores to solve logical constraints (default: 1). Warning: unpredictable performance. See https://github.com/ucsd-progsys/liquidhaskell/issues/2562" , minPartSize = FC.defaultMinPartSize @@ -235,7 +211,7 @@ "size. Overrides the minpartsize option.") , smtsolver - = def &= help "Name of SMT-Solver" + = Nothing &= help "Name of SMT-Solver" , noCheckUnknown = def &= explicit @@ -246,46 +222,27 @@ = defaultMaxParams &= help "Restrict qualifier mining to those taking at most `m' parameters (2 by default)" , shortNames - = def &= name "short-names" + = False &= name "short-names" &= help "Print shortened names, i.e. drop all module qualifiers." , shortErrors - = def &= name "short-errors" + = False &= name "short-errors" &= help "Don't show long error messages, just line numbers." - , cabalDir - = def &= name "cabal-dir" - &= help "Find and use .cabal to add paths to sources for imported files" - - , ghcOptions - = def &= name "ghc-option" - &= typ "OPTION" - &= help "Pass this option to GHC" - - , cFiles - = def &= name "c-files" - &= typ "OPTION" - &= help "Tell GHC to compile and link against these files" - - , port - = defaultPort - &= name "port" - &= help "Port at which lhi should listen" - , exactDC - = def &= help "Exact Type for Data Constructors" + = False &= help "Exact Type for Data Constructors" &= name "exact-data-cons" , noADT - = def &= help "Do not generate ADT representations in refinement logic" + = False &= help "Do not generate ADT representations in refinement logic" &= name "no-adt" , expectErrorContaining - = def &= help "Expect an error which containing the provided string from verification (can be provided more than once)" + = [] &= help "Expect an error which containing the provided string from verification (can be provided more than once)" &= name "expect-error-containing" , expectAnyError - = def &= help "Expect an error, no matter which kind or what it contains" + = False &= help "Expect an error, no matter which kind or what it contains" &= name "expect-any-error" , scrapeInternals @@ -347,103 +304,88 @@ -- PLE-OPT &= name "automatic-instances" , proofLogicEval - = def + = False &= help "Enable Proof-by-Logical-Evaluation" &= name "ple" , pleWithUndecidedGuards - = def + = False &= help "Unfold invocations with undecided guards in PLE" &= name "ple-with-undecided-guards" &= explicit - , oldPLE - = def - &= help "Enable Proof-by-Logical-Evaluation" - &= name "oldple" - , interpreter - = def + = False &= help "Use an interpreter to assist PLE in solving constraints" &= name "interpreter" , proofLogicEvalLocal - = def + = False &= help "Enable Proof-by-Logical-Evaluation locally, per function" &= name "ple-local" , etabeta - = def + = False &= help "Eta expand and beta reduce terms to aid PLE" &= name "etabeta" - + , dependantCase - = def + = False &= help "Allow PLE to reason about dependent cases" &= name "dependant-case" , extensionality - = def + = False &= help "Enable extensional interpretation of function equality" &= name "extensionality" , nopolyinfer - = def + = False &= help "No inference of polymorphic type application. Gives imprecision, but speedup." &= name "fast" , reflection - = def + = False &= help "Enable reflection of Haskell functions and theorem proving" &= name "reflection" , compileSpec - = def + = False &= name "compile-spec" &= help "Only compile specifications (into .bspec file); skip verification" - , noCheckImports - = def - &= name "no-check-imports" - &= help "Do not check the transitive imports; only check the target files." - , typeclass - = def + = False &= help "Enable Typeclass" &= name "typeclass" , auxInline - = def + = False &= help "Enable inlining of class methods" &= name "aux-inline" , rwTerminationCheck - = def + = False &= name "rw-termination-check" &= help ( "Enable the rewrite divergence checker. " ++ "Can speed up verification if rewriting terminates, but can also cause divergence." ) , skipModule - = def + = False &= name "skip-module" &= help "Completely skip this module, don't even compile any specifications in it." - , - noLazyPLE - = def - &= name "no-lazy-ple" - &= help "Don't use Lazy PLE" , fuel = Nothing &= help "Maximum fuel (per-function unfoldings) for PLE" , environmentReduction - = def + = False &= explicit &= name "environment-reduction" &= help "perform environment reduction (disabled by default)" , noEnvironmentReduction - = def + = False &= explicit &= name "no-environment-reduction" &= help "Don't perform environment reduction" @@ -467,42 +409,41 @@ &= help "Stop loading LHAssumptions modules for imports in these packages." &= typ "PACKAGE" , dumpOpaqueReflections - = def &= help "Dump all generated opaque reflections" + = False &= help "Dump all generated opaque reflections" &= name "dump-opaque-reflections" &= explicit , dumpPreNormalizedCore - = def &= help "Dump pre-normalized core (before a-normalization)" + = False &= help "Dump pre-normalized core (before a-normalization)" &= name "dump-pre-normalized-core" &= explicit + , dumpNormalizedCore + = False &= help "Dump a-normalized core" + &= name "dump-normalized-core" + &= explicit , allowUnsafeConstructors - = def &= help "Allow refining constructors with unsafe refinements" + = False &= help "Allow refining constructors with unsafe refinements" &= name "allow-unsafe-constructors" &= explicit - } &= program "liquid" + , ddumpTimings + = False &= help "Dump time measures of the Liquid Haskell plugin" + &= name "ddump-timings" + &= explicit + } &= program "liquidhaskell" &= help "Refinement Types for Haskell" &= summary copyright - &= details [ "LiquidHaskell is a Refinement Type based verifier for Haskell" - , "" - , "To check a Haskell file foo.hs, type:" - , " liquid foo.hs " - ] - -defaultPort :: Int -defaultPort = 3000 + &= details [ "LiquidHaskell is a Refinement Type based verifier for Haskell" ] getOpts :: [String] -> IO Config getOpts as = do cfg0 <- envCfg - cfg1 <- mkOpts =<< cmdArgsRun' - config { modeValue = (modeValue config) - { cmdArgsValue = cfg0 - } - } - as - cfg2 <- fixConfig cfg1 - let cfg3 = if json cfg2 then cfg2 {loggingVerbosity = Quiet} else cfg2 - setVerbosity (cmdargsVerbosity $ loggingVerbosity cfg3) - withSmtSolver cfg3 + cfg1 <- cmdArgsRun' + config { modeValue = (modeValue config) + { cmdArgsValue = cfg0 } + } + as + let cfg2 = if json cfg1 then cfg1 {loggingVerbosity = Quiet} else cfg1 + setVerbosity (cmdargsVerbosity $ loggingVerbosity cfg2) + withSmtSolver cfg2 cmdArgsRun' :: Mode (CmdArgs a) -> [String] -> IO a cmdArgsRun' md as @@ -524,12 +465,13 @@ case found of Just _ -> return cfg Nothing -> panic Nothing (missingSmtError smt) - Nothing -> do smts <- mapM findSmtSolver [FC.Z3, FC.Cvc4, FC.Mathsat] + Nothing -> do smts <- mapM findSmtSolver smtLookupOrder case catMaybes smts of (s:_) -> return (cfg {smtsolver = Just s}) _ -> panic Nothing noSmtError where - noSmtError = "LiquidHaskell requires an SMT Solver, i.e. z3, cvc4, or mathsat to be installed." + smtLookupOrder = [FC.Z3, FC.Cvc5, FC.Cvc4, FC.Mathsat] + noSmtError = "LiquidHaskell requires one of the following SMT solvers to be installed: " ++ intercalate ", " (show <$> smtLookupOrder) ++ "." missingSmtError smt = "Could not find SMT solver '" ++ show smt ++ "'. Is it on your PATH?" findSmtSolver :: FC.SMTSolver -> IO (Maybe FC.SMTSolver) @@ -537,28 +479,6 @@ FC.Z3mem -> return $ Just FC.Z3mem smt -> maybe Nothing (const $ Just smt) <$> findExecutable (show smt) -fixConfig :: Config -> IO Config -fixConfig config' = do - pwd <- getCurrentDirectory - cfg <- canonicalizePaths pwd config' - return $ canonConfig cfg - --- | Attempt to canonicalize all `FilePath's in the `Config' so we don't have --- to worry about relative paths. -canonicalizePaths :: FilePath -> Config -> IO Config -canonicalizePaths pwd cfg = do - tgt <- canonicalizePath pwd - isdir <- doesDirectoryExist tgt - is <- mapM (canonicalize tgt isdir) $ idirs cfg - cs <- mapM (canonicalize tgt isdir) $ cFiles cfg - return $ cfg { idirs = is, cFiles = cs } - -canonicalize :: FilePath -> Bool -> FilePath -> IO FilePath -canonicalize tgt isdir f - | isAbsolute f = return f - | isdir = canonicalizePath (tgt f) - | otherwise = canonicalizePath (takeDirectory tgt f) - envCfg :: IO Config envCfg = do so <- lookupEnv "LIQUIDHASKELL_OPTS" @@ -599,27 +519,6 @@ ] --- [NOTE:searchpath] --- 1. we used to add the directory containing the file to the searchpath, --- but this is bad because GHC does NOT do this, and it causes spurious --- "duplicate module" errors in the following scenario --- > tree --- . --- ├── Bar.hs --- └── Foo --- ├── Bar.hs --- └── Goo.hs --- If we run `liquid Foo/Goo.hs` and that imports Bar, GHC will not know --- whether we mean to import Bar.hs or Foo/Bar.hs --- 2. tests fail if you flip order of idirs' - -mkOpts :: Config -> IO Config -mkOpts cfg = do - let files' = F.sortNub $ files cfg - return $ cfg { files = files' - -- See NOTE [searchpath] - } - -------------------------------------------------------------------------------- -- | Updating options -------------------------------------------------------------------------------- @@ -630,10 +529,10 @@ } -------------------------------------------------------------------------------- -withPragmas :: MonadIO m => Config -> FilePath -> [Located String] -> (Config -> m a) -> m a +withPragmas :: MonadIO m => Config -> [Located String] -> (Config -> m a) -> m a -------------------------------------------------------------------------------- -withPragmas cfg fp ps action - = do cfg' <- liftIO $ (processPragmas cfg ps >>= canonicalizePaths fp) <&> canonConfig +withPragmas cfg ps action + = do cfg' <- liftIO $ processPragmas cfg ps <&> canonConfig -- As the verbosity is set /globally/ via the cmdargs lib, re-set it. liftIO $ setVerbosity (cmdargsVerbosity $ loggingVerbosity cfg') res <- action cfg' @@ -649,100 +548,12 @@ cmdArgsApply -- | Note that this function doesn't process list arguments properly, like --- 'cFiles' or 'expectErrorContaining' +-- 'expectErrorContaining' -- TODO: This is only used to parse the contents of the env var LIQUIDHASKELL_OPTS -- so it should be able to parse multiple arguments instead. See issue #1990. parsePragma :: Located String -> IO Config parsePragma = processPragmas defConfig . (:[]) -defConfig :: Config -defConfig = Config - { loggingVerbosity = Minimal - , files = def - , idirs = def - , fullcheck = def - , linear = def - , stringTheory = def - , higherorder = def - , smtTimeout = def - , higherorderqs = def - , diffcheck = def - , saveQuery = def - , checks = def - , nostructuralterm = def - , noCheckUnknown = def - , notermination = False - , nopositivity = False - , rankNTypes = False - , noclasscheck = False - , gradual = False - , bscope = False - , gdepth = 1 - , ginteractive = False - , totalHaskell = def -- True - , nowarnings = def - , noannotations = def - , checkDerived = False - , caseExpandDepth = 2 - , notruetypes = def - , nototality = False - , pruneUnsorted = def - , exactDC = def - , noADT = def - , expectErrorContaining = def - , expectAnyError = False - , cores = def - , minPartSize = FC.defaultMinPartSize - , maxPartSize = FC.defaultMaxPartSize - , maxParams = defaultMaxParams - , smtsolver = def - , shortNames = def - , shortErrors = def - , cabalDir = def - , ghcOptions = def - , cFiles = def - , port = defaultPort - , scrapeInternals = False - , elimStats = False - , elimBound = Nothing - , json = False - , counterExamples = False - , timeBinds = False - , untidyCore = False - , eliminate = FC.Some - , noPatternInline = False - , noSimplifyCore = False - -- PLE-OPT , autoInstantiate = def - , noslice = False - , noLiftedImport = False - , proofLogicEval = False - , pleWithUndecidedGuards = False - , oldPLE = False - , interpreter = False - , proofLogicEvalLocal = False - , etabeta = False - , dependantCase = False - , reflection = False - , extensionality = False - , nopolyinfer = False - , compileSpec = False - , noCheckImports = False - , typeclass = False - , auxInline = False - , rwTerminationCheck = False - , skipModule = False - , noLazyPLE = False - , fuel = Nothing - , environmentReduction = False - , noEnvironmentReduction = False - , inlineANFBindings = False - , pandocHtml = False - , excludeAutomaticAssumptionsFor = [] - , dumpOpaqueReflections = False - , dumpPreNormalizedCore = False - , allowUnsafeConstructors = False - } - -- | Write the annotations (i.e. the files in the \".liquid\" hidden folder) and -- report the result of the checking using a supplied function, or using an -- implicit JSON function, if @json@ flag is set. @@ -842,9 +653,9 @@ orHeader = text "LIQUID: ERROR:" <+> text s , orMessages = map (cErrToSpanned k . errToFCrash) xs } -resDocs k (F.Unsafe _ xs) = +resDocs k (F.Unsafe stats xs) = OutputResult { - orHeader = text "LIQUID: UNSAFE" + orHeader = text $ "LIQUID: UNSAFE (" <> show (Solver.numChck stats) <> " constraints checked)" , orMessages = map (cErrToSpanned k) (nub xs) } diff --git a/src/Language/Haskell/Liquid/UX/Config.hs b/src/Language/Haskell/Liquid/UX/Config.hs --- a/src/Language/Haskell/Liquid/UX/Config.hs +++ b/src/Language/Haskell/Liquid/UX/Config.hs @@ -40,8 +40,6 @@ -- NOTE: adding strictness annotations breaks the help message data Config = Config { loggingVerbosity :: Verbosity -- ^ the logging verbosity to use (defaults to 'Minimal') - , files :: [FilePath] -- ^ source files to check - , idirs :: [FilePath] -- ^ path to directory for including specs , diffcheck :: Bool -- ^ check subset of binders modified (+ dependencies) since last check , linear :: Bool -- ^ uninterpreted integer multiplication and division , stringTheory :: Bool -- ^ interpretation of string theory in the logic @@ -58,10 +56,7 @@ , noclasscheck :: Bool -- ^ disable checking class instances -- , structuralTerm :: Bool -- ^ use structural termination checker , nostructuralterm :: Bool -- ^ disable structural termination check - , gradual :: Bool -- ^ enable gradual type checking , bscope :: Bool -- ^ scope of the outer binders on the inner refinements - , gdepth :: Int -- ^ depth of gradual concretization - , ginteractive :: Bool -- ^ interactive gradual solving , totalHaskell :: Bool -- ^ Check for termination and totality, Overrides no-termination flags , nowarnings :: Bool -- ^ disable warnings output (only show errors) , noannotations :: Bool -- ^ disable creation of intermediate annotation files @@ -74,14 +69,10 @@ , minPartSize :: Int -- ^ Minimum size of a partition , maxPartSize :: Int -- ^ Maximum size of a partition. Overrides minPartSize , maxParams :: Int -- ^ the maximum number of parameters to accept when mining qualifiers - , smtsolver :: Maybe SMTSolver -- ^ name of smtsolver to use [default: try z3, cvc4, mathsat in order] + , smtsolver :: Maybe SMTSolver -- ^ SMT solver to use [if `Nothing`, try looking one up using the order defined in L.H.L.UX.CmdLine.withSmtSolver] , shortNames :: Bool -- ^ drop module qualifers from pretty-printed names. , shortErrors :: Bool -- ^ don't show subtyping errors and contexts. - , cabalDir :: Bool -- ^ find and use .cabal file to include paths to sources for imported modules - , ghcOptions :: [String] -- ^ command-line options to pass to GHC - , cFiles :: [String] -- ^ .c files to compile and link against (for GHC) , eliminate :: Eliminate -- ^ eliminate (i.e. don't use qualifs for) for "none", "cuts" or "all" kvars - , port :: Int -- ^ port at which lhi should listen , exactDC :: Bool -- ^ Automatically generate singleton types for data constructors , noADT :: Bool -- ^ Disable ADTs (only used with exactDC) , expectErrorContaining :: [String] -- ^ expect failure from Liquid with at least one of the following messages @@ -100,7 +91,6 @@ , noLiftedImport :: Bool -- ^ Disable loading lifted specifications (for "legacy" libs) , proofLogicEval :: Bool -- ^ Enable proof-by-logical-evaluation , pleWithUndecidedGuards :: Bool -- ^ Unfold invocations with undecided guards in PLE - , oldPLE :: Bool -- ^ Enable proof-by-logical-evaluation , interpreter :: Bool -- ^ Use an interpreter to assist PLE , proofLogicEvalLocal :: Bool -- ^ Enable proof-by-logical-evaluation locally, per function , etabeta :: Bool -- ^ Eta expand and beta reduce terms to aid PLE @@ -109,13 +99,11 @@ , nopolyinfer :: Bool -- ^ No inference of polymorphic type application. , reflection :: Bool -- ^ Allow "reflection"; switches on "--higherorder" and "--exactdc" , compileSpec :: Bool -- ^ Only "compile" the spec -- into .bspec file -- don't do any checking. - , noCheckImports :: Bool -- ^ Do not check the transitive imports , typeclass :: Bool -- ^ enable typeclass support. - , auxInline :: Bool -- ^ + , auxInline :: Bool -- ^ , rwTerminationCheck :: Bool -- ^ Enable termination checking for rewriting , skipModule :: Bool -- ^ Skip this module entirely (don't even compile any specs in it) - , noLazyPLE :: Bool - , fuel :: Maybe Int -- ^ Maximum PLE "fuel" (unfold depth) (default=infinite) + , fuel :: Maybe Int -- ^ Maximum PLE "fuel" (unfold depth) (default=infinite) , environmentReduction :: Bool -- ^ Perform environment reduction , noEnvironmentReduction :: Bool -- ^ Don't perform environment reduction , inlineANFBindings :: Bool -- ^ Inline ANF bindings. @@ -124,7 +112,10 @@ , excludeAutomaticAssumptionsFor :: [String] , dumpOpaqueReflections :: Bool -- Dumps all opaque reflections to the stdout , dumpPreNormalizedCore :: Bool -- Dumps the prenormalized core (before a-normalization) + , dumpNormalizedCore :: Bool -- Dumps the a-normalized core , allowUnsafeConstructors :: Bool -- ^ Allow refining constructors with unsafe refinements + , ddumpTimings :: Bool -- ^ Dump time measures of the Liquid Haskell plugin + -- Only needed to work around https://github.com/haskell/cabal/issues/11116 } deriving (Generic, Data, Show, Eq) allowPLE :: Config -> Bool diff --git a/src/Language/Haskell/Liquid/UX/Errors.hs b/src/Language/Haskell/Liquid/UX/Errors.hs --- a/src/Language/Haskell/Liquid/UX/Errors.hs +++ b/src/Language/Haskell/Liquid/UX/Errors.hs @@ -34,11 +34,11 @@ type CtxM = M.HashMap F.Symbol (WithModel SpecType) ------------------------------------------------------------------------ -tidyError :: Config -> F.FixSolution -> Error -> Error +tidyError :: Config -> Error -> Error ------------------------------------------------------------------------ -tidyError cfg sol +tidyError cfg = fmap (tidySpecType tidy) - . tidyErrContext tidy sol + . tidyErrContext tidy where tidy = configTidy cfg @@ -47,8 +47,8 @@ | shortNames cfg = F.Lossy | otherwise = F.Full -tidyErrContext :: F.Tidy -> F.FixSolution -> Error -> Error -tidyErrContext k _ e@(ErrSubType {}) +tidyErrContext :: F.Tidy -> Error -> Error +tidyErrContext k e@(ErrSubType {}) = e { ctx = c', tact = F.subst θ tA, texp = F.subst θ tE } where (θ, c') = tidyCtx k xs (ctx e) @@ -56,7 +56,7 @@ tA = tact e tE = texp e -tidyErrContext _ _ e@(ErrSubTypeModel {}) +tidyErrContext _ e@(ErrSubTypeModel {}) = e { ctxM = c', tactM = fmap (F.subst θ) tA, texp = fmap (F.subst θ) tE } where (θ, c') = tidyCtxM xs $ ctxM e @@ -64,7 +64,7 @@ tA = tactM e tE = texp e -tidyErrContext k _ e@(ErrAssType {}) +tidyErrContext k e@(ErrAssType {}) = e { ctx = c', cond = F.subst θ p } where m = ctx e @@ -72,7 +72,7 @@ xs = F.syms p p = cond e -tidyErrContext _ _ e +tidyErrContext _ e = e -------------------------------------------------------------------------------- diff --git a/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs b/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs --- a/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs +++ b/src/Language/Haskell/Liquid/UX/QuasiQuoter.hs @@ -90,12 +90,13 @@ (\t -> (`SigD` t) . lhNameToName <$> names) <$> simplifyBareType id (head names) (quantifyFreeRTy $ parsedToBareType $ val ty) mkSpecDecs (Alias rta) = - return . TySynD name tvs <$> simplifyBareType parsedToBareType lsym (rtBody (val rta)) + return . TySynD name tvs <$> simplifyBareType parsedToBareType lsym (rtBody rta) where - lsym = F.atLoc rta n - name = symbolName n - n = rtName (val rta) - tvs = (\a -> PlainTV (symbolName a) BndrReq) <$> rtTArgs (val rta) + lsym = F.atLoc (rtName rta) sym + name = symbolName sym + -- We use the symbol returned by the parser + sym = getLHNameSymbol . val $ rtName rta + tvs = (\a -> PlainTV (symbolName a) BndrReq) <$> rtTArgs rta mkSpecDecs _ = Right [] diff --git a/src/Language/Haskell/Liquid/WiredIn.hs b/src/Language/Haskell/Liquid/WiredIn.hs --- a/src/Language/Haskell/Liquid/WiredIn.hs +++ b/src/Language/Haskell/Liquid/WiredIn.hs @@ -95,7 +95,7 @@ | s <- wiredTheorySyms , let srt = F.tsSort $ fromMaybe (panic Nothing ("unknown symbol: " ++ show s)) $ - F.lookupSEnv s (F.theorySymbols F.Z3) + F.lookupSEnv s (F.theorySymbols F.Z3 <> F.theorySymbols F.Cvc5) ] where wiredTheorySyms = @@ -113,6 +113,7 @@ , "Set_sub" , "Set_add" , "Set_com" + , "Set_card" , "Bag_count" , "Bag_empty" @@ -121,6 +122,10 @@ , "Bag_sub" , "Bag_union" , "Bag_union_max" + + , "FF_val" + , "FF_add" + , "FF_mul" , "strLen" ] diff --git a/tests/Parser.hs b/tests/Parser.hs --- a/tests/Parser.hs +++ b/tests/Parser.hs @@ -152,8 +152,8 @@ "embed Set as Set_Set" , testCase "qualif" $ - parseSingleSpec "qualif Foo(v:Int): v < 0" @?== - "qualif Foo defined at :1:8" + parseSingleSpec "qualif Foo(v:Int) { v < 0 }" @?== + "qualif Foo(v: int) { v < 0 } // defined at :1:8" , testCase "lazyvar" $ parseSingleSpec "lazyvar z" @?== @@ -376,11 +376,10 @@ @?== unlines [ "predicate ValidChunk V XS N = " - , " (not (len XS == 0) =>" - , " (1 < N && 1 < len XS => len V < len XS)" - , " && (len XS <= N => len V == 1)" - , " )" - , " && (len XS == 0 => len V == 0)" + , " if len XS == 0 " + , " then len V == 0" + , " else (1 < len XS && 1 < N => len V < len XS)" + , " && (len XS <= N => len V == 1)" ]