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