From 47db0c95501ab2a6476f2b4185172421278c033a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Fri, 1 Nov 2024 17:55:29 +0000 Subject: [PATCH 01/10] Rename assumptionP to tyBindLHNameP --- .../src/Language/Haskell/Liquid/Parse.hs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs index 25fcaf1d14..42a5f9f69f 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs @@ -1108,7 +1108,7 @@ specP :: Parser BPspec specP = fallbackSpecP "assume" ((reserved "reflect" >> fmap AssmReflect assmReflectBindP) <|> (reserved "relational" >> fmap AssmRel relationalP) - <|> fmap Assm assumptionP ) + <|> fmap Assm tyBindLHNameP ) <|> fallbackSpecP "assert" (fmap Asrt tyBindP ) <|> fallbackSpecP "autosize" (fmap ASize asizeP ) <|> (reserved "local" >> fmap LAsrt tyBindP ) @@ -1252,8 +1252,12 @@ tyBindP :: Parser (LocSymbol, Located BareType) tyBindP = (,) <$> locBinderP <* reservedOp "::" <*> located genBareTypeP -assumptionP :: Parser (Located LHName, Located BareType) -assumptionP = do +tyBindMethodP :: Parser (LocSymbol, Located BareType) +tyBindMethodP = + (,) <$> located binderInfixParensP <* reservedOp "::" <*> located genBareTypeP + +tyBindLHNameP :: Parser (Located LHName, Located BareType) +tyBindLHNameP = do x <- locBinderP _ <- reservedOp "::" t <- located genBareTypeP From 5d40d8a3b0a3154e4b28100e7f8b9f9870451368 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Fri, 1 Nov 2024 18:18:42 +0000 Subject: [PATCH 02/10] Factorize composition of makeUnresolvedLHName with locUpperIdP in Parse.hs --- .../src/Language/Haskell/Liquid/Parse.hs | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs index 42a5f9f69f..aeb29371c7 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs @@ -466,18 +466,21 @@ lowerIdTail l = bTyConP :: Parser BTyCon bTyConP - = (reservedOp "'" >> (mkPromotedBTyCon . fmap (makeUnresolvedLHName LHDataConName) <$> locUpperIdP)) - <|> mkBTyCon . fmap (makeUnresolvedLHName LHTcName) <$> locUpperIdP + = (reservedOp "'" >> mkPromotedBTyCon <$> locUpperIdLHNameP LHDataConName) + <|> mkBTyCon <$> locUpperIdLHNameP LHTcName <|> (reserved "*" >> return (mkBTyCon (dummyLoc $ makeUnresolvedLHName LHTcName $ symbol ("*" :: String))) ) "bTyConP" +locUpperIdLHNameP :: LHNameSpace -> Parser (Located LHName) +locUpperIdLHNameP ns = fmap (makeUnresolvedLHName ns) <$> locUpperIdP + mkPromotedBTyCon :: Located LHName -> BTyCon mkPromotedBTyCon x = BTyCon x False True -- (consSym '\'' <$> x) False True classBTyConP :: Parser BTyCon -classBTyConP = mkClassBTyCon . fmap (makeUnresolvedLHName LHTcName) <$> locUpperIdP +classBTyConP = mkClassBTyCon <$> locUpperIdLHNameP LHTcName mkClassBTyCon :: Located LHName -> BTyCon mkClassBTyCon x = BTyCon x True False @@ -1227,7 +1230,7 @@ filePathP = angles $ some pathCharP pathChars = ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['.', '/'] datavarianceP :: Parser (Located LHName, [Variance]) -datavarianceP = liftM2 (,) (fmap (makeUnresolvedLHName LHTcName) <$> locUpperIdP) (many varianceP) +datavarianceP = liftM2 (,) (locUpperIdLHNameP LHTcName) (many varianceP) dsizeP :: Parser ([Located BareType], Located Symbol) dsizeP = liftM2 (,) (parens $ sepBy (located genBareTypeP) comma) locBinderP @@ -1297,7 +1300,7 @@ genBareTypeP = bareTypeP embedP :: Parser (Located LHName, FTycon, TCArgs) embedP = do - x <- fmap (makeUnresolvedLHName LHTcName) <$> locUpperIdP + x <- locUpperIdLHNameP LHTcName a <- try (reserved "*" >> return WithArgs) <|> return NoArgs -- TODO: reserved "*" looks suspicious _ <- reserved "as" t <- fTyConP From 4189a9e200151cbec6c6318b5623a44090a66030 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Fri, 1 Nov 2024 19:14:00 +0000 Subject: [PATCH 03/10] Don't add parenthesis when parsing infix operators --- .../src/Language/Haskell/Liquid/Parse.hs | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs index aeb29371c7..f80a0b2d4b 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs @@ -21,6 +21,7 @@ module Language.Haskell.Liquid.Parse import Control.Arrow (second) import Control.Monad import Control.Monad.Identity +import qualified Data.Char as Char import qualified Data.Foldable as F import Data.String import Data.Void @@ -896,11 +897,17 @@ ppAsserts k lxs t mles ppLes Nothing = "" ppLes (Just les) = "/" <+> pprintTidy k (val <$> les) +pprintSymbolWithParens :: LHName -> PJ.Doc +pprintSymbolWithParens lhname = + case show lhname of + n@(c:_) | not (Char.isAlpha c) -> "(" <> PJ.text n <> ")" + n -> PJ.text n + ppPspec :: (PPrint t, PPrint c) => Tidy -> Pspec t c -> PJ.Doc ppPspec k (Meas m) = "measure" <+> pprintTidy k m ppPspec k (Assm (lx, t)) - = "assume" <+> pprintTidy k (val lx) <+> "::" <+> pprintTidy k t + = "assume" <+> pprintSymbolWithParens (val lx) <+> "::" <+> pprintTidy k t ppPspec k (AssmReflect (lx, ly)) = "assume reflect" <+> pprintTidy k (val lx) <+> "as" <+> pprintTidy k (val ly) ppPspec k (Asrt (lx, t)) @@ -1469,13 +1476,10 @@ binderP = pwr <$> parens (idP bad) -} binderP :: Parser Symbol binderP = - symbol . (\ x -> "(" <> x <> ")") . symbolText <$> parens infixBinderIdP + parens infixBinderIdP <|> binderIdP -- Note: It is important that we do *not* use the LH/fixpoint reserved words here, -- because, for example, we must be able to use "assert" as an identifier. - -- - -- TODO, Andres: I have no idea why we make the parens part of the symbol here. - -- But I'm reproducing this behaviour for now, as it is backed up via a few tests. measureDefP :: Parser Body -> Parser (Def (Located BareType) LocSymbol) measureDefP bodyP From 1af8c5e60b76f7018f283fc76152dd6a6358d703 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Fri, 1 Nov 2024 19:39:48 +0000 Subject: [PATCH 04/10] Eliminate unused localSigs field from specs --- liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs | 2 +- liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs | 1 - .../src/Language/Haskell/Liquid/Bare/Resolve.hs | 1 - liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs | 1 - liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs | 4 ---- 5 files changed, 1 insertion(+), 8 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs index af2f423ef2..c9e71c8bd3 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs @@ -891,7 +891,7 @@ makeTySigs env sigEnv name spec = do bareTySigs :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, LocBareType)] bareTySigs env name spec = checkDuplicateSigs <$> vts where - vts = forM ( Ms.sigs spec ++ Ms.localSigs spec ) $ \ (x, t) -> do + vts = forM ( Ms.sigs spec ) $ \ (x, t) -> do v <- F.notracepp "LOOKUP-GHC-VAR" $ Bare.lookupGhcVar env name "rawTySigs" x return (v, t) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs index c23077e4a9..dfb013cf8e 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs @@ -388,7 +388,6 @@ expandBareSpec rtEnv l sp = sp { measures = expand rtEnv l (measures sp) , asmSigs = map (second (expand rtEnv l)) (asmSigs sp) , sigs = expand rtEnv l (sigs sp) - , localSigs = expand rtEnv l (localSigs sp) , reflSigs = expand rtEnv l (reflSigs sp) , ialiases = [ (f x, f y) | (x, y) <- ialiases sp ] , dataDecls = expand rtEnv l (dataDecls sp) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs index f03225ec73..e907968e84 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs @@ -447,7 +447,6 @@ qualifyBareSpec env name l bs sp = sp { measures = qualify env name l bs (measures sp) , asmSigs = qualify env name l bs (asmSigs sp) , sigs = qualify env name l bs (sigs sp) - , localSigs = qualify env name l bs (localSigs sp) , reflSigs = qualify env name l bs (reflSigs sp) , dataDecls = qualify env name l bs (dataDecls sp) , newtyDecls = qualify env name l bs (newtyDecls sp) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs index f80a0b2d4b..03d13ad9aa 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs @@ -1069,7 +1069,6 @@ mkSpec name xs = (name,) $ qualifySpec (symbol name) Measure.Spec , Measure.asmReflectSigs = [(l, r) | AssmReflect (l, r) <- xs] , Measure.sigs = [a | Asrt a <- xs] ++ [(y, t) | Asrts (ys, (t, _)) <- xs, y <- ys] - , Measure.localSigs = [] , Measure.reflSigs = [] , Measure.impSigs = [] , Measure.expSigs = [] diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs index a66d3b9275..1ddb74040a 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs @@ -401,7 +401,6 @@ data Spec ty bndr = Spec , asmSigs :: ![(F.Located LHName, ty)] -- ^ Assumed (unchecked) types; including reflected signatures , asmReflectSigs :: ![(F.LocSymbol, F.LocSymbol)] -- ^ Assume reflects : left is the actual function and right the pretended one , sigs :: ![(F.LocSymbol, ty)] -- ^ Imported functions and types - , localSigs :: ![(F.LocSymbol, ty)] -- ^ Local type signatures , reflSigs :: ![(F.LocSymbol, ty)] -- ^ Reflected type signatures , invariants :: ![(Maybe F.LocSymbol, ty)] -- ^ Data type invariants; the Maybe is the generating measure , ialiases :: ![(ty, ty)] -- ^ Data type invariants to be checked @@ -464,7 +463,6 @@ instance Semigroup (Spec ty bndr) where , asmSigs = asmSigs s1 ++ asmSigs s2 , asmReflectSigs = asmReflectSigs s1 ++ asmReflectSigs s2 , sigs = sigs s1 ++ sigs s2 - , localSigs = localSigs s1 ++ localSigs s2 , reflSigs = reflSigs s1 ++ reflSigs s2 , invariants = invariants s1 ++ invariants s2 , ialiases = ialiases s1 ++ ialiases s2 @@ -515,7 +513,6 @@ instance Monoid (Spec ty bndr) where , asmSigs = [] , asmReflectSigs = [] , sigs = [] - , localSigs = [] , reflSigs = [] , invariants = [] , ialiases = [] @@ -864,7 +861,6 @@ unsafeFromLiftedSpec a = Spec , asmSigs = S.toList . liftedAsmSigs $ a , asmReflectSigs = S.toList . liftedAsmReflectSigs $ a , sigs = S.toList . liftedSigs $ a - , localSigs = mempty , reflSigs = mempty , relational = mempty , asmRel = mempty From 628c737d344b3c2aa8a713d31e3bc480808b27c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Fri, 1 Nov 2024 20:14:18 +0000 Subject: [PATCH 05/10] Stop inserting parenthesis around infix operators in the parser (except in one leftover place) --- .../Language/Haskell/Liquid/LHNameResolution.hs | 7 +------ .../src/Language/Haskell/Liquid/Parse.hs | 14 ++++++++++++-- 2 files changed, 13 insertions(+), 8 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs index c8696adce5..abc37e8779 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs @@ -120,12 +120,7 @@ resolveLHNames taliases globalRdrEnv = let m = LH.takeModuleNames s n = LH.dropModuleNames s nString = symbolString n - -- TODO: Maybe change the parser so dataConNameP doesn't include the - -- parentheses around infix operators. - maybeUnpar = case nString of - '(':rest -> init rest - _ -> nString - oname = GHC.mkOccName (mkGHCNameSpace ns) maybeUnpar + oname = GHC.mkOccName (mkGHCNameSpace ns) nString rdrn = if m == "" then GHC.mkRdrUnqual oname diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs index 03d13ad9aa..e46fe77400 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs @@ -1418,7 +1418,7 @@ riMethodSigP = try (do reserved "assume" (x, t) <- tyBindP return (x, RIAssumed t) ) - <|> do (x, t) <- tyBindP + <|> do (x, t) <- tyBindMethodP return (x, RISig t) "riMethodSigP" @@ -1480,6 +1480,16 @@ binderP = -- Note: It is important that we do *not* use the LH/fixpoint reserved words here, -- because, for example, we must be able to use "assert" as an identifier. +-- | Like binderP, but surrounds infix operators with parenthesis. +-- +-- This is only needed by `tests/parser/pos/T892.hs` and needs to be +-- investigated why. +binderInfixParensP :: Parser Symbol +binderInfixParensP = + symbol . (\ x -> "(" <> x <> ")") . symbolText <$> parens infixBinderIdP + <|> binderIdP + + measureDefP :: Parser Body -> Parser (Def (Located BareType) LocSymbol) measureDefP bodyP = do mname <- locSymbolP @@ -1581,7 +1591,7 @@ dataConNameP where idP p = takeWhile1P Nothing (not . p) bad c = isSpace c || c `elem` ("(,)" :: String) - pwr s = symbol $ "(" <> s <> ")" + pwr s = symbol s dataSizeP :: Parser (Maybe SizeFun) dataSizeP From 20ebaf1456dfb4d2ecbd6369f21126c7b0e0044f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Sat, 2 Nov 2024 22:45:48 +0000 Subject: [PATCH 06/10] Generalize a bit lookupLocalVar --- .../src/Language/Haskell/Liquid/Bare/Resolve.hs | 17 ++++++++--------- .../src/Language/Haskell/Liquid/GHC/Misc.hs | 3 +++ 2 files changed, 11 insertions(+), 9 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs index e907968e84..1ed4ed227b 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs @@ -494,8 +494,8 @@ lookupGhcNamedVar env name z = maybeResolveSym env name "Var" lx lookupGhcVar :: Env -> ModName -> String -> LocSymbol -> Lookup Ghc.Var lookupGhcVar env name kind lx = case resolveLocSym env name kind lx of - Right v -> Mb.maybe (Right v) Right (lookupLocalVar env lx [v]) - Left e -> Mb.maybe (Left e) Right (lookupLocalVar env lx []) + Right v -> Mb.maybe (Right v) (either Right Right) (lookupLocalVar (reLocalVars env) lx [v]) + Left e -> Mb.maybe (Left e) (either Right Right) (lookupLocalVar (reLocalVars env) lx []) -- where -- err e = Misc.errorP "error-lookupGhcVar" (F.showpp (e, F.loc lx, lx)) @@ -505,12 +505,11 @@ lookupGhcVar env name kind lx = case resolveLocSym env name kind lx of -- that also match the name @lx@; we then pick the "closest" definition. -- See tests/names/LocalSpec.hs for a motivating example. -lookupLocalVar :: Env -> LocSymbol -> [Ghc.Var] -> Maybe Ghc.Var -lookupLocalVar env lx gvs = findNearest lxn kvs +lookupLocalVar :: F.Loc a => LocalVars -> LocSymbol -> [a] -> Maybe (Either a Ghc.Var) +lookupLocalVar localVars lx gvs = findNearest lxn kvs where - _msg = "LOOKUP-LOCAL: " ++ F.showpp (F.val lx, lxn, kvs) - kvs = prioritizeRecBinds (M.lookupDefault [] x $ reLocalVars env) ++ gs - gs = [(F.sp_start $ F.srcSpan v, v) | v <- gvs] + kvs = prioritizeRecBinds (M.lookupDefault [] x localVars) ++ gs + gs = [(F.sp_start $ F.srcSpan v, Left v) | v <- gvs] lxn = F.sp_start $ F.srcSpan lx (_, x) = unQualifySymbol (F.val lx) @@ -520,9 +519,9 @@ lookupLocalVar env lx gvs = findNearest lxn kvs prioritizeRecBinds lvds = let (recs, nrecs) = L.partition lvdIsRec lvds in map lvdToPair (recs ++ nrecs) - lvdToPair lvd = (lvdSourcePos lvd, lvdVar lvd) + lvdToPair lvd = (lvdSourcePos lvd, Right (lvdVar lvd)) - findNearest :: F.SourcePos -> [(F.SourcePos, Ghc.Var)] -> Maybe Ghc.Var + findNearest :: F.SourcePos -> [(F.SourcePos, b)] -> Maybe b findNearest key kvs1 = argMin [ (posDistance key k, v) | (k, v) <- kvs1 ] -- We prefer the var with the smaller distance, or equal distance diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs index cc11f28c66..ed86fcbe0b 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Misc.hs @@ -315,6 +315,9 @@ locNamedThing x = F.Loc l lE x instance F.Loc Var where srcSpan v = SS (getSourcePos v) (getSourcePosE v) +instance F.Loc Name where + srcSpan v = SS (getSourcePos v) (getSourcePosE v) + namedLocSymbol :: (F.Symbolic a, NamedThing a) => a -> F.Located F.Symbol namedLocSymbol d = F.symbol <$> locNamedThing d From 319f7161b93c66070f2df286fce1f400553b3a91 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Sat, 2 Nov 2024 23:45:43 +0000 Subject: [PATCH 07/10] Handle local variables in name resolution of LHNames --- liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs | 2 +- .../src/Language/Haskell/Liquid/Bare.hs | 23 +++++--- .../Language/Haskell/Liquid/Bare/Resolve.hs | 43 +++++++++------ .../src/Language/Haskell/Liquid/Bare/Types.hs | 1 + .../src/Language/Haskell/Liquid/GHC/Plugin.hs | 28 ++++++---- .../Haskell/Liquid/LHNameResolution.hs | 53 ++++++++++++------- 6 files changed, 97 insertions(+), 53 deletions(-) diff --git a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs index cf7a1b0218..849f7b501a 100644 --- a/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs +++ b/liquidhaskell-boot/src-ghc/Liquid/GHC/API.hs @@ -635,7 +635,7 @@ import GHC.Types.Name as Ghc , stableNameCmp ) import GHC.Types.Name.Env as Ghc - ( lookupNameEnv ) + ( NameEnv, lookupNameEnv, mkNameEnv ) import GHC.Types.Name.Set as Ghc ( NameSet , elemNameSet diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs index c9e71c8bd3..31fc338b82 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs @@ -123,12 +123,13 @@ to disk so that we can retrieve it later without having to re-check the relevant -- with a list of 'Warning's, which shouldn't abort the compilation (modulo explicit request from the user, -- to treat warnings and errors). makeTargetSpec :: Config + -> Bare.LocalVars -> LogicMap -> TargetSrc -> BareSpec -> TargetDependencies -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec)) -makeTargetSpec cfg lmap targetSrc bareSpec dependencies = do +makeTargetSpec cfg localVars lmap targetSrc bareSpec dependencies = do let targDiagnostics = Bare.checkTargetSrc cfg targetSrc let depsDiagnostics = mapM (Bare.checkBareSpec . snd) legacyDependencies let bareSpecDiagnostics = Bare.checkBareSpec legacyBareSpec @@ -167,7 +168,7 @@ makeTargetSpec cfg lmap targetSrc bareSpec dependencies = do -- "let {len :: [a] -> Int; len _ = undefined}" -- Ghc.execOptions - diagOrSpec <- makeGhcSpec cfg (fromTargetSrc targetSrc) lmap legacyBareSpec legacyDependencies + diagOrSpec <- makeGhcSpec cfg localVars (fromTargetSrc targetSrc) lmap legacyBareSpec legacyDependencies case diagOrSpec of Left d -> return $ Left d Right (warns, ghcSpec) -> do @@ -191,7 +192,9 @@ makeTargetSpec cfg lmap targetSrc bareSpec dependencies = do tcg <- Ghc.getGblEnv let exportedNames = Ghc.availsToNameSet (Ghc.tcg_exports tcg) exportedAssumption (LHNResolved (LHRGHC n) _) = - Ghc.nameModule_maybe n /= Just (Ghc.tcg_mod tcg) || Ghc.elemNameSet n exportedNames + case Ghc.nameModule_maybe n of + Nothing -> Ghc.elemNameSet n exportedNames + Just m -> m /= Ghc.tcg_mod tcg || Ghc.elemNameSet n exportedNames exportedAssumption _ = True return lspec { liftedAsmSigs = S.filter (exportedAssumption . val . fst) (liftedAsmSigs lspec) } @@ -200,17 +203,18 @@ makeTargetSpec cfg lmap targetSrc bareSpec dependencies = do -- validates it using @checkGhcSpec@. ------------------------------------------------------------------------------------- makeGhcSpec :: Config + -> Bare.LocalVars -> GhcSrc -> LogicMap -> Ms.BareSpec -> [(ModName, Ms.BareSpec)] -> Ghc.TcRn (Either Diagnostics ([Warning], GhcSpec)) ------------------------------------------------------------------------------------- -makeGhcSpec cfg src lmap targetSpec dependencySpecs = do +makeGhcSpec cfg localVars src lmap targetSpec dependencySpecs = do hscEnv <- Ghc.getTopEnv session <- Ghc.Session <$> Ghc.liftIO (newIORef hscEnv) tcg <- Ghc.getGblEnv - (dg0, sp) <- makeGhcSpec0 cfg session tcg src lmap targetSpec dependencySpecs + (dg0, sp) <- makeGhcSpec0 cfg session tcg localVars src lmap targetSpec dependencySpecs let diagnostics = Bare.checkTargetSpec (targetSpec : map snd dependencySpecs) (toTargetSrc src) (ghcSpecEnv sp) @@ -252,12 +256,13 @@ makeGhcSpec0 :: Config -> Ghc.Session -> Ghc.TcGblEnv + -> Bare.LocalVars -> GhcSrc -> LogicMap -> Ms.BareSpec -> [(ModName, Ms.BareSpec)] -> Ghc.TcRn (Diagnostics, GhcSpec) -makeGhcSpec0 cfg session tcg src lmap targetSpec dependencySpecs = do +makeGhcSpec0 cfg session tcg localVars src lmap targetSpec dependencySpecs = do -- build up environments tycEnv <- makeTycEnv1 name env (tycEnv0, datacons) coreToLg simplifier let tyi = Bare.tcTyConMap tycEnv @@ -380,7 +385,7 @@ makeGhcSpec0 cfg session tcg src lmap targetSpec dependencySpecs = do embs = makeEmbeds src env (mySpec0 : map snd dependencySpecs) dm = Bare.tcDataConMap tycEnv0 (dg0, datacons, tycEnv0) = makeTycEnv0 cfg name env embs mySpec2 iSpecs2 - env = Bare.makeEnv cfg session tcg src lmap ((name, targetSpec) : dependencySpecs) + env = Bare.makeEnv cfg session tcg localVars src lmap ((name, targetSpec) : dependencySpecs) -- check barespecs name = F.notracepp ("ALL-SPECS" ++ zzz) $ _giTargetMod src zzz = F.showpp (fst <$> mspecs) @@ -998,7 +1003,7 @@ allAsmSigs env myName specs = do -- constraints should account instead for what logic functions are used in -- the constraints, which should be easier to do when precise renaming has -- been implemented for expressions and reflected functions. - , isUsedExternalVar v || isInScope v + , isUsedExternalVar v || isInScope v || isLocalVar v ] where lookupSymbolOrLHName :: ModName -> Bool -> SymbolOrLHName -> Bare.Lookup (Maybe Ghc.Var) @@ -1056,6 +1061,8 @@ allAsmSigs env myName specs = do Ghc.DataConWorkId dc -> inScope dc _ -> inScope v0 + isLocalVar = Mb.isNothing . Ghc.nameModule_maybe . Ghc.getName + resolveAsmVar :: Bare.Env -> ModName -> Bool -> LocSymbol -> Bare.Lookup (Maybe Ghc.Var) resolveAsmVar env name True lx = Just <$> Bare.lookupGhcVar env name "resolveAsmVar-True" lx resolveAsmVar env name False lx = return $ Bare.maybeResolveSym env name "resolveAsmVar-False" lx <|> GM.maybeAuxVar (F.val lx) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs index 1ed4ed227b..ee15f69cf8 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs @@ -14,6 +14,7 @@ module Language.Haskell.Liquid.Bare.Resolve ( -- * Creating the Environment makeEnv + , makeLocalVars -- * Resolving symbols , ResolveSym (..) @@ -30,6 +31,7 @@ module Language.Haskell.Liquid.Bare.Resolve , lookupGhcVar , lookupGhcIdLHName , lookupGhcNamedVar + , lookupLocalVar , matchTyCon -- * Checking if names exist @@ -102,10 +104,11 @@ type Lookup a = Either [Error] a ------------------------------------------------------------------------------- -- | Creating an environment ------------------------------------------------------------------------------- -makeEnv :: Config -> Ghc.Session -> Ghc.TcGblEnv -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> Env -makeEnv cfg session tcg src lmap specs = RE +makeEnv :: Config -> Ghc.Session -> Ghc.TcGblEnv -> LocalVars -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> Env +makeEnv cfg session tcg localVars src lmap specs = RE { reSession = session , reTcGblEnv = tcg + , reLocalVarsEnv = makeLocalVarsEnv localVars , reUsedExternals = usedExternals , reLMap = lmap , reSyms = syms @@ -113,7 +116,7 @@ makeEnv cfg session tcg src lmap specs = RE , _reTyThings = makeTyThingMap src , reQualImps = _gsQualImps src , reAllImps = _gsAllImps src - , reLocalVars = makeLocalVars src + , reLocalVars = localVars , reSrc = src , reGlobSyms = S.fromList globalSyms , reCfg = cfg @@ -135,8 +138,12 @@ getGlobalSyms (_, spec) where mbName = F.val . msName -makeLocalVars :: GhcSrc -> LocalVars -makeLocalVars = localVarMap . localBinds . _giCbs +makeLocalVars :: [Ghc.CoreBind] -> LocalVars +makeLocalVars = localVarMap . localBinds + +makeLocalVarsEnv :: LocalVars -> Ghc.NameEnv Ghc.Var +makeLocalVarsEnv m = + Ghc.mkNameEnv [ (Ghc.getName (lvdVar d), lvdVar d) | d <- concat (M.elems m) ] -- TODO: rewrite using CoreVisitor localBinds :: [Ghc.CoreBind] -> [LocalVarDetails] @@ -566,9 +573,13 @@ lookupGhcDataConLHName env lname = do lookupGhcIdLHName :: HasCallStack => Env -> Located LHName -> Lookup Ghc.Id lookupGhcIdLHName env lname = do - case lookupTyThing env lname of - Ghc.AConLike (Ghc.RealDataCon d) -> Right (Ghc.dataConWorkId d) - Ghc.AnId x -> Right x + case lookupTyThingMaybe env lname of + Nothing + | LHNResolved (LHRGHC n) _ <- val lname + , Just x <- Ghc.lookupNameEnv (reLocalVarsEnv env) n -> + Right x + Just (Ghc.AConLike (Ghc.RealDataCon d)) -> Right (Ghc.dataConWorkId d) + Just (Ghc.AnId x) -> Right x _ -> panic (Just $ GM.fSrcSpan lname) $ "not a variable of data constructor: " ++ show (val lname) @@ -953,19 +964,21 @@ matchTyCon env lc = do -- This should be benign because the result doesn't depend of when exactly this is -- called. Since this code is intended to be used inside a GHC plugin, there is no -- danger that GHC is finalized before the result is evaluated. -lookupTyThing :: Env -> Located LHName -> Ghc.TyThing -lookupTyThing env lc@(Loc _ _ c0) = unsafePerformIO $ do +lookupTyThingMaybe :: Env -> Located LHName -> Maybe Ghc.TyThing +lookupTyThingMaybe env lc@(Loc _ _ c0) = unsafePerformIO $ do case c0 of LHNUnresolved _ _ -> panic (Just $ GM.fSrcSpan lc) $ "unresolved name: " ++ show c0 LHNResolved rn _ -> case rn of LHRLocal _ -> panic (Just $ GM.fSrcSpan lc) $ "cannot resolve a local name: " ++ show c0 LHRIndex i -> panic (Just $ GM.fSrcSpan lc) $ "cannot resolve a LHRIndex " ++ show i LHRLogic (LogicName s _) -> panic (Just $ GM.fSrcSpan lc) $ "lookupTyThing: cannot resolve a LHRLogic name " ++ show s - LHRGHC n -> do - m <- Ghc.reflectGhc (Interface.lookupTyThing (reTcGblEnv env) n) (reSession env) - case m of - Just tt -> return tt - Nothing -> panic (Just $ GM.fSrcSpan lc) $ "not found: " ++ show c0 + LHRGHC n -> + Ghc.reflectGhc (Interface.lookupTyThing (reTcGblEnv env) n) (reSession env) + +lookupTyThing :: Env -> Located LHName -> Ghc.TyThing +lookupTyThing env lc = + Mb.fromMaybe (panic (Just $ GM.fSrcSpan lc) $ "not found: " ++ show (val lc)) $ + lookupTyThingMaybe env lc bareTCApp :: (Expandable r) => r diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Types.hs index 8a2aa25463..2dbf8b0aee 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Types.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Types.hs @@ -72,6 +72,7 @@ plugSrc _ = Nothing data Env = RE { reSession :: Ghc.Session , reTcGblEnv :: Ghc.TcGblEnv + , reLocalVarsEnv :: Ghc.NameEnv Ghc.Var -- ^ an environment of local variables , reUsedExternals :: Ghc.NameSet , reLMap :: LogicMap , reSyms :: [(F.Symbol, Ghc.Var)] -- ^ see "syms" in old makeGhcSpec' diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs index 969e380e82..684159cd7d 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs @@ -73,6 +73,7 @@ import Language.Haskell.Liquid.Types.Specs import Language.Haskell.Liquid.Types.Types import Language.Haskell.Liquid.Types.Visitors import Language.Haskell.Liquid.Bare +import Language.Haskell.Liquid.Bare.Resolve (makeLocalVars) import Language.Haskell.Liquid.UX.CmdLine import Language.Haskell.Liquid.UX.Config @@ -509,6 +510,9 @@ data ProcessModuleResult = ProcessModuleResult { processModule :: LiquidHaskellContext -> TcM (Either LiquidCheckException ProcessModuleResult) processModule LiquidHaskellContext{..} = do + let modGuts0 = lhModuleGuts + thisModule = mg_module modGuts0 + debugLog ("Module ==> " ++ renderModule thisModule) hscEnv <- env_top <$> getEnv @@ -527,10 +531,12 @@ processModule LiquidHaskellContext{..} = do when debugLogs $ forM_ (HM.keys . getDependencies $ dependencies) $ debugLog . moduleStableString . unStableModule - debugLog $ "mg_exports => " ++ O.showSDocUnsafe (O.ppr $ mg_exports modGuts) - debugLog $ "mg_tcs => " ++ O.showSDocUnsafe (O.ppr $ mg_tcs modGuts) + debugLog $ "mg_exports => " ++ O.showSDocUnsafe (O.ppr $ mg_exports modGuts0) + debugLog $ "mg_tcs => " ++ O.showSDocUnsafe (O.ppr $ mg_tcs modGuts0) dynFlags <- getDynFlags + let preNormalizedCore = preNormalizeCore moduleCfg modGuts0 + modGuts = modGuts0 { mg_binds = preNormalizedCore } targetSrc <- liftIO $ makeTargetSrc moduleCfg dynFlags file lhModuleTcData modGuts hscEnv logger <- getLogger @@ -540,13 +546,18 @@ processModule LiquidHaskellContext{..} = do tcg <- getGblEnv let rtAliases = collectTypeAliases thisModule bareSpec0 (HM.toList $ getDependencies dependencies) - eBareSpec = resolveLHNames rtAliases (tcg_rdr_env tcg) bareSpec0 + localVars = makeLocalVars preNormalizedCore + eBareSpec = resolveLHNames + localVars + rtAliases + (tcg_rdr_env tcg) + bareSpec0 result <- case eBareSpec of Left errors -> pure $ Left $ mkDiagnostics [] errors Right bareSpec -> fmap (,bareSpec) <$> - makeTargetSpec moduleCfg lhModuleLogicMap targetSrc bareSpec dependencies + makeTargetSpec moduleCfg localVars lhModuleLogicMap targetSrc bareSpec dependencies let continue = pure $ Left (ErrorsOccurred []) reportErrs :: (Show e, F.PPrint e) => [TError e] -> TcRn (Either LiquidCheckException ProcessModuleResult) @@ -576,10 +587,6 @@ processModule LiquidHaskellContext{..} = do `Ex.catch` (\(e :: Error) -> reportErrs [e]) `Ex.catch` (\(es :: [Error]) -> reportErrs es) - where - modGuts = lhModuleGuts - thisModule = mg_module modGuts - makeTargetSrc :: Config -> DynFlags -> FilePath @@ -588,11 +595,10 @@ makeTargetSrc :: Config -> HscEnv -> IO TargetSrc makeTargetSrc cfg dynFlags file tcData modGuts hscEnv = do - let preNormCoreBinds = preNormalizeCore cfg modGuts when (dumpPreNormalizedCore cfg) $ do putStrLn "\n*************** Pre-normalized CoreBinds *****************\n" - putStrLn $ unlines $ L.intersperse "" $ map (GHC.showPpr dynFlags) preNormCoreBinds - coreBinds <- anormalize cfg hscEnv modGuts { mg_binds = preNormCoreBinds } + putStrLn $ unlines $ L.intersperse "" $ map (GHC.showPpr dynFlags) (mg_binds modGuts) + coreBinds <- anormalize cfg hscEnv modGuts -- The type constructors for a module are the (nubbed) union of the ones defined and -- the ones exported. This covers the case of \"wrapper modules\" that simply re-exports diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs index abc37e8779..c9f0515236 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs @@ -26,10 +26,13 @@ import Data.Generics (extT) import qualified Data.HashSet as HS import qualified Data.HashMap.Strict as HM +import Data.Maybe (fromMaybe, listToMaybe) import qualified Data.Text as Text import qualified GHC.Types.Name.Occurrence import Language.Fixpoint.Types hiding (Error, panic) +import Language.Haskell.Liquid.Bare.Resolve (lookupLocalVar) +import Language.Haskell.Liquid.Bare.Types (LocalVars) import Language.Haskell.Liquid.Types.Errors (TError(ErrDupNames, ErrResolve), panic) import Language.Haskell.Liquid.Types.Specs import Language.Haskell.Liquid.Types.Types @@ -61,11 +64,12 @@ collectTypeAliases m bs deps = -- | Converts occurrences of LHNUnresolved to LHNResolved using the provided -- type aliases and GlobalRdrEnv. resolveLHNames - :: HM.HashMap Symbol (Module, RTAlias Symbol BareType) + :: LocalVars + -> HM.HashMap Symbol (Module, RTAlias Symbol BareType) -> GlobalRdrEnv -> BareSpec -> Either [Error] BareSpec -resolveLHNames taliases globalRdrEnv = +resolveLHNames localVars taliases globalRdrEnv = (\(bs, es) -> if null es then Right bs else Left es) . runWriter . mapMLocLHNames (\l -> (<$ l) <$> resolveLHName l) . @@ -82,30 +86,43 @@ resolveLHNames taliases globalRdrEnv = | otherwise -> case HM.lookup s taliases of Just (m, _) -> pure $ LHNResolved (LHRLogic $ LogicName s m) s - Nothing -> lookupGRELHName LHTcName lname s + Nothing -> lookupGRELHName LHTcName lname s listToMaybe LHNUnresolved LHVarName s - | isDataCon s -> lookupGRELHName LHDataConName lname s - | otherwise -> lookupGRELHName LHVarName lname s - LHNUnresolved ns s -> lookupGRELHName ns lname s + | isDataCon s -> lookupGRELHName LHDataConName lname s listToMaybe + | otherwise -> + lookupGRELHName LHVarName lname s + (fmap (either id GHC.getName) . lookupLocalVar localVars (atLoc lname s)) + LHNUnresolved ns s -> lookupGRELHName ns lname s listToMaybe n@(LHNResolved (LHRLocal _) _) -> pure n n -> let sp = Just $ LH.sourcePosSrcSpan $ loc lname in panic sp $ "resolveLHNames: Unexpected resolved name: " ++ show n - lookupGRELHName ns lname s = + lookupGRELHName ns lname s localNameLookup = case GHC.lookupGRE globalRdrEnv (mkLookupGRE ns s) of - [e] -> - pure $ LHNResolved (LHRGHC $ GHC.greName e) s + [e] -> do + let n = GHC.greName e + n' = fromMaybe n $ localNameLookup [n] + pure $ LHNResolved (LHRGHC n') s es@(_:_) -> do - tell [ErrDupNames - (LH.fSrcSpan lname) - (pprint s) - (map (PJ.text . showPprUnsafe) es) - ] - pure $ val lname - [] -> do - tell [errResolve (nameSpaceKind ns) "Cannot resolve name" (s <$ lname)] - pure $ val lname + let topLevelNames = map GHC.greName es + case localNameLookup topLevelNames of + Just n | notElem n topLevelNames -> + pure $ LHNResolved (LHRGHC n) s + _ -> do + tell [ErrDupNames + (LH.fSrcSpan lname) + (pprint s) + (map (PJ.text . showPprUnsafe) es) + ] + pure $ val lname + [] -> + case localNameLookup [] of + Just n' -> + pure $ LHNResolved (LHRGHC n') s + Nothing -> do + tell [errResolve (nameSpaceKind ns) "Cannot resolve name" (s <$ lname)] + pure $ val lname errResolve :: PJ.Doc -> String -> LocSymbol -> Error errResolve k msg lx = ErrResolve (LH.fSrcSpan lx) k (pprint (val lx)) (PJ.text msg) From 21b5162491ca634c1eff68d5e2e8cd9c979c3fd7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Sun, 3 Nov 2024 14:55:01 +0000 Subject: [PATCH 08/10] Remove redundand dynFlags parameter of makeTargetSrc --- .../src/Language/Haskell/Liquid/GHC/Plugin.hs | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs index 684159cd7d..37cbaadbf4 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs @@ -514,7 +514,6 @@ processModule LiquidHaskellContext{..} = do thisModule = mg_module modGuts0 debugLog ("Module ==> " ++ renderModule thisModule) - hscEnv <- env_top <$> getEnv let bareSpec0 = lhInputSpec -- /NOTE/: For the Plugin to work correctly, we shouldn't call 'canonicalizePath', because otherwise @@ -534,10 +533,10 @@ processModule LiquidHaskellContext{..} = do debugLog $ "mg_exports => " ++ O.showSDocUnsafe (O.ppr $ mg_exports modGuts0) debugLog $ "mg_tcs => " ++ O.showSDocUnsafe (O.ppr $ mg_tcs modGuts0) - dynFlags <- getDynFlags + hscEnv <- getTopEnv let preNormalizedCore = preNormalizeCore moduleCfg modGuts0 modGuts = modGuts0 { mg_binds = preNormalizedCore } - targetSrc <- liftIO $ makeTargetSrc moduleCfg dynFlags file lhModuleTcData modGuts hscEnv + targetSrc <- liftIO $ makeTargetSrc moduleCfg file lhModuleTcData modGuts hscEnv logger <- getLogger -- See https://github.com/ucsd-progsys/liquidhaskell/issues/1711 @@ -588,16 +587,15 @@ processModule LiquidHaskellContext{..} = do `Ex.catch` (\(es :: [Error]) -> reportErrs es) makeTargetSrc :: Config - -> DynFlags -> FilePath -> TcData -> ModGuts -> HscEnv -> IO TargetSrc -makeTargetSrc cfg dynFlags file tcData modGuts hscEnv = do +makeTargetSrc cfg file tcData modGuts hscEnv = do when (dumpPreNormalizedCore cfg) $ do putStrLn "\n*************** Pre-normalized CoreBinds *****************\n" - putStrLn $ unlines $ L.intersperse "" $ map (GHC.showPpr dynFlags) (mg_binds modGuts) + putStrLn $ unlines $ L.intersperse "" $ map (GHC.showPpr (GHC.hsc_dflags hscEnv)) (mg_binds modGuts) coreBinds <- anormalize cfg hscEnv modGuts -- The type constructors for a module are the (nubbed) union of the ones defined and From 55dfcd2d222566175a11e24eedc7f102977bbae8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Sun, 3 Nov 2024 21:30:35 +0000 Subject: [PATCH 09/10] Add a test for assumptions on local variables --- tests/names/pos/LocalAssume.hs | 13 +++++++++++++ tests/tests.cabal | 1 + 2 files changed, 14 insertions(+) create mode 100644 tests/names/pos/LocalAssume.hs diff --git a/tests/names/pos/LocalAssume.hs b/tests/names/pos/LocalAssume.hs new file mode 100644 index 0000000000..7882ae641d --- /dev/null +++ b/tests/names/pos/LocalAssume.hs @@ -0,0 +1,13 @@ +-- | Tests that local assumptions are taken into consideration +module LocalAssume where + +import Prelude (Int) + +{-@ f :: {v: Int | v > 0} @-} +f :: Int +f = g + where + {-@ assume g :: {v:Int | v > 0} @-} + g :: Int + g = 0 + diff --git a/tests/tests.cabal b/tests/tests.cabal index c809d7e00d..a19a96a5ed 100644 --- a/tests/tests.cabal +++ b/tests/tests.cabal @@ -792,6 +792,7 @@ executable names-pos , Local01 , Local02 , Local03 + , LocalAssume , LocalSpec , Ord , Set00 From d5183b3c7b937b0ef30efb8f70f52371b8d6a758 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Mon, 4 Nov 2024 00:49:37 +0000 Subject: [PATCH 10/10] Set upper bound on vector, to avoid breakage of store --- cabal.project | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/cabal.project b/cabal.project index 43eb2e15a8..bcb519ac4a 100644 --- a/cabal.project +++ b/cabal.project @@ -36,3 +36,7 @@ package liquidhaskell package liquidhaskell-boot ghc-options: -j flags: +devel + +constraints: + -- vector-0.13.2.0 breaks store-0.7.18 + vector <= 0.13.1.0