diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs index 6faf54a890..e585fd8731 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs @@ -599,7 +599,7 @@ makeSpecTerm cfg mySpec env name = do sizes <- if structuralTerm cfg then pure mempty else makeSize env name mySpec lazies <- makeLazy env name mySpec autos <- makeAutoSize env name mySpec - gfail <- makeFail env name mySpec + gfail <- makeFail env mySpec return $ SpTerm { gsLazy = S.insert dictionaryVar (lazies `mappend` sizes) , gsFail = gfail @@ -629,10 +629,10 @@ makeLazy :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.Var makeLazy env name spec = sMapM (Bare.lookupGhcVar env name "Var") (Ms.lazy spec) -makeFail :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet (Located Ghc.Var)) -makeFail env name spec = +makeFail :: Bare.Env -> Ms.BareSpec -> Bare.Lookup (S.HashSet (Located Ghc.Var)) +makeFail env spec = sForM (Ms.fails spec) $ \x -> do - vx <- Bare.lookupGhcVar env name "Var" x + vx <- Bare.lookupGhcIdLHName env x return x { val = vx } makeRewrite :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet (Located Ghc.Var)) @@ -790,12 +790,11 @@ addReflSigs env name rtEnv measEnv refl sig = notReflected xt = fst xt `notElem` reflected makeAutoInst :: Bare.Env -> ModName -> Ms.BareSpec -> - Bare.Lookup (M.HashMap Ghc.Var (Maybe Int)) -makeAutoInst env name spec = M.fromList <$> kvs + Bare.Lookup (S.HashSet Ghc.Var) +makeAutoInst env name spec = S.fromList <$> kvs where - kvs = forM (M.toList (Ms.autois spec)) $ \(k, val) -> do - vk <- Bare.lookupGhcVar env name "Var" k - return (vk, val) + kvs = forM (S.toList (Ms.autois spec)) $ + Bare.lookupGhcVar env name "Var" ---------------------------------------------------------------------------------------- diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Class.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Class.hs index 039e7bd82a..06fc9d531d 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Class.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Class.hs @@ -29,6 +29,7 @@ import qualified Liquid.GHC.API as Ghc import Language.Haskell.Liquid.Misc import Language.Haskell.Liquid.Types.DataDecl import Language.Haskell.Liquid.Types.Errors +import Language.Haskell.Liquid.Types.Names import Language.Haskell.Liquid.Types.RefType import Language.Haskell.Liquid.Types.RType import Language.Haskell.Liquid.Types.RTypeOp @@ -182,7 +183,7 @@ mkClassE env sigEnv _myName name (RClass cc ss as ms) tc = do meths <- mapM (makeMethod env sigEnv name) ms' let vts = [ (m, v, t) | (m, kv, t) <- meths, v <- Mb.maybeToList (plugSrc kv) ] let sts = [(val s, unClass $ val t) | (s, _) <- ms | (_, _, t) <- meths] - let dcp = DataConP l dc αs [] (val <$> ss') (reverse sts) rt False (F.symbol name) l' + let dcp = DataConP l dc αs [] (val <$> ss') (map (first getLHNameSymbol) (reverse sts)) rt False (F.symbol name) l' return $ F.notracepp msg (dcp, vts) where c = btc_tc cc @@ -204,11 +205,11 @@ mkConstr env sigEnv name = fmap (fmap dropUniv) . Bare.cookSpecTypeE env sigEnv unClass :: SpecType -> SpecType unClass = snd . bkClass . thrd3 . bkUniv -makeMethod :: Bare.Env -> Bare.SigEnv -> ModName -> (LocSymbol, LocBareType) +makeMethod :: Bare.Env -> Bare.SigEnv -> ModName -> (Located LHName, LocBareType) -> Bare.Lookup (ModName, PlugTV Ghc.Var, LocSpecType) makeMethod env sigEnv name (lx, bt) = (name, mbV,) <$> Bare.cookSpecTypeE env sigEnv name mbV bt where - mbV = maybe Bare.GenTV Bare.LqTV (Bare.maybeResolveSym env name "makeMethod" lx) + mbV = either (const Bare.GenTV) Bare.LqTV (Bare.lookupGhcIdLHName env lx) ------------------------------------------------------------------------------- makeSpecDictionaries :: Bare.Env -> Bare.SigEnv -> ModSpecs -> DEnv Ghc.Var LocSpecType diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs index 34b8b40749..6eed9bc01e 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs @@ -849,7 +849,6 @@ data Pspec ty ctor | CLaws (RClass ty) -- ^ 'class laws' definition | ILaws (RILaws ty) | RInst (RInstance ty) -- ^ refined 'instance' definition - | Incl FilePath -- ^ 'include' a path -- TODO: deprecate | Invt ty -- ^ 'invariant' specification | Using (ty, ty) -- ^ 'using' declaration (for local invariants on a type) | Alias (Located (RTAlias Symbol BareType)) -- ^ 'type' alias declaration @@ -858,10 +857,10 @@ data Pspec ty ctor | Qualif Qualifier -- ^ 'qualif' definition | LVars LocSymbol -- ^ 'lazyvar' annotation, defer checks to *use* sites | Lazy LocSymbol -- ^ 'lazy' annotation, skip termination check on binder - | Fail LocSymbol -- ^ 'fail' annotation, the binder should be unsafe + | Fail (Located LHName) -- ^ 'fail' annotation, the binder should be unsafe | Rewrite LocSymbol -- ^ 'rewrite' annotation, the binder generates a rewrite rule | Rewritewith (LocSymbol, [LocSymbol]) -- ^ 'rewritewith' annotation, the first binder is using the rewrite rules of the second list, - | Insts (LocSymbol, Maybe Int) -- ^ 'auto-inst' or 'ple' annotation; use ple locally on binder + | Insts LocSymbol -- ^ 'auto-inst' or 'ple' annotation; use ple locally on binder | HMeas LocSymbol -- ^ 'measure' annotation; lift Haskell binder as measure | Reflect LocSymbol -- ^ 'reflect' annotation; reflect Haskell binder as function in logic | OpaqueReflect LocSymbol -- ^ 'opaque-reflect' annotation @@ -919,8 +918,6 @@ ppPspec k (DDecl d) = pprintTidy k d ppPspec k (NTDecl d) = "newtype" <+> pprintTidy k d -ppPspec _ (Incl f) - = "include" <+> "<" PJ.<> PJ.text f PJ.<> ">" ppPspec k (Invt t) = "invariant" <+> pprintTidy k t ppPspec k (Using (t1, t2)) @@ -947,8 +944,8 @@ ppPspec k (Rewritewith (lx, lxs)) go s = pprintTidy k $ val s ppPspec k (Fail lx) = "fail" <+> pprintTidy k (val lx) -ppPspec k (Insts (lx, mbN)) - = "automatic-instances" <+> pprintTidy k (val lx) <+> maybe "" (("with" <+>) . pprintTidy k) mbN +ppPspec k (Insts lx) + = "automatic-instances" <+> pprintTidy k (val lx) ppPspec k (HMeas lx) = "measure" <+> pprintTidy k (val lx) ppPspec k (Reflect lx) @@ -1009,7 +1006,6 @@ ppPspec k (AssmRel (lxl, lxr, tl, tr, q, p)) show (Impt _) = "Impt" shcl _) = "DDecl" show (NTDecl _) = "NTDecl" - show (Incl _) = "Incl" show (Invt _) = "Invt" show (Using _) = "Using" show (Alias _) = "Alias" @@ -1020,7 +1016,6 @@ ppPspec k (AssmRel (lxl, lxr, tl, tr, q, p)) show (LVars _) = "LVars" show (Lazy _) = "Lazy" -- show (Axiom _) = "Axiom" - show (Insts _) = "Insts" show (Reflect _) = "Reflect" show (HMeas _) = "HMeas" show (HBound _) = "HBound" @@ -1071,13 +1066,12 @@ mkSpec name xs = (name,) $ qualifySpec (symbol name) Measure.Spec , Measure.ialiases = [t | Using t <- xs] , Measure.dataDecls = [d | DDecl d <- xs] ++ [d | NTDecl d <- xs] , Measure.newtyDecls = [d | NTDecl d <- xs] - , Measure.includes = [q | Incl q <- xs] , Measure.aliases = [a | Alias a <- xs] , Measure.ealiases = [e | EAlias e <- xs] , Measure.embeds = tceFromList [(c, (fTyconSort tc, a)) | Embed (c, tc, a) <- xs] , Measure.qualifiers = [q | Qualif q <- xs] , Measure.lvars = S.fromList [d | LVars d <- xs] - , Measure.autois = M.fromList [s | Insts s <- xs] + , Measure.autois = S.fromList [s | Insts s <- xs] , Measure.pragmas = [s | Pragma s <- xs] , Measure.cmeasures = [m | CMeas m <- xs] , Measure.imeasures = [m | IMeas m <- xs] @@ -1146,7 +1140,6 @@ specP <|> fmap DDecl dataDeclP )) <|> (reserved "newtype" >> fmap NTDecl dataDeclP ) <|> (reserved "relational" >> fmap Relational relationalP ) - <|> (reserved "include" >> fmap Incl filePathP ) <|> fallbackSpecP "invariant" (fmap Invt invariantP) <|> (reserved "using" >> fmap Using invaliasP ) <|> (reserved "type" >> fmap Alias aliasP ) @@ -1162,9 +1155,9 @@ specP <|> (reserved "lazy" >> fmap Lazy lazyVarP ) <|> (reserved "rewrite" >> fmap Rewrite rewriteVarP ) <|> (reserved "rewriteWith" >> fmap Rewritewith rewriteWithP ) - <|> (reserved "fail" >> fmap Fail failVarP ) - <|> (reserved "ple" >> fmap Insts autoinstP ) - <|> (reserved "automatic-instances" >> fmap Insts autoinstP ) + <|> (reserved "fail" >> fmap Fail locBinderLHNameP ) + <|> (reserved "ple" >> fmap Insts locBinderP ) + <|> (reserved "automatic-instances" >> fmap Insts locBinderP ) <|> (reserved "LIQUID" >> fmap Pragma pragmaP ) <|> (reserved "liquid" >> fmap Pragma pragmaP ) <|> {- DEFAULT -} fmap Asrts tyBindsP @@ -1188,11 +1181,6 @@ tyBindsRemP sy = do pragmaP :: Parser (Located String) pragmaP = locStringLiteral -autoinstP :: Parser (LocSymbol, Maybe Int) -autoinstP = do x <- locBinderP - i <- optional (reserved "with" >> natural) - return (x, fromIntegral <$> i) - lazyVarP :: Parser LocSymbol lazyVarP = locBinderP @@ -1203,9 +1191,6 @@ rewriteVarP = locBinderP rewriteWithP :: Parser (LocSymbol, [LocSymbol]) rewriteWithP = (,) <$> locBinderP <*> brackets (sepBy1 locBinderP comma) -failVarP :: Parser LocSymbol -failVarP = locBinderP - axiomP :: Parser LocSymbol axiomP = locBinderP @@ -1218,15 +1203,6 @@ inlineP = locBinderP asizeP :: Parser LocSymbol asizeP = locBinderP -filePathP :: Parser FilePath -filePathP = angles $ some pathCharP - where - pathCharP :: Parser Char - pathCharP = choice $ char <$> pathChars - - pathChars :: [Char] - pathChars = ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['.', '/'] - datavarianceP :: Parser (Located LHName, [Variance]) datavarianceP = liftM2 (,) (locUpperIdLHNameP LHTcName) (many varianceP) @@ -1419,7 +1395,7 @@ classP = do sups <- supersP c <- classBTyConP tvs <- manyTill (bTyVar <$> tyVarIdP) (try $ reserved "where") - ms <- block tyBindP -- <|> sepBy tyBindP semi + ms <- block tyBindLHNameP -- <|> sepBy tyBindP semi return $ RClass c sups tvs ms where supersP = try ((parens (superP `sepBy1` comma) <|> fmap pure superP) diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs index ba1a259351..221e8d92e9 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs @@ -71,7 +71,6 @@ module Language.Haskell.Liquid.Types.Specs ( import GHC.Generics hiding (to, moduleName) import Data.Binary import qualified Language.Fixpoint.Types as F -import Language.Fixpoint.Misc (sortNub) import Data.Data (Data) import Data.Hashable import qualified Data.HashSet as S @@ -318,7 +317,7 @@ instance Semigroup GhcSpecTerm where instance Monoid GhcSpecTerm where mempty = SpTerm mempty mempty mempty mempty mempty data GhcSpecRefl = SpRefl - { gsAutoInst :: !(M.HashMap Var (Maybe Int)) -- ^ Binders to USE PLE + { gsAutoInst :: !(S.HashSet Var) -- ^ Binders to USE PLE , gsHAxioms :: ![(Var, LocSpecType, F.Equation)] -- ^ Lifted definitions , gsImpAxioms :: ![F.Equation] -- ^ Axioms from imported reflected functions , gsMyAxioms :: ![F.Equation] -- ^ Axioms from my reflected functions @@ -404,7 +403,6 @@ data Spec ty bndr = Spec , ialiases :: ![(ty, ty)] -- ^ Data type invariants to be checked , dataDecls :: ![DataDecl] -- ^ Predicated data definitions , newtyDecls :: ![DataDecl] -- ^ Predicated new type definitions - , includes :: ![FilePath] -- ^ Included qualifier files , aliases :: ![F.Located (RTAlias F.Symbol BareType)] -- ^ RefType aliases , ealiases :: ![F.Located (RTAlias F.Symbol F.Expr)] -- ^ Expression aliases , embeds :: !(F.TCEmb (F.Located LHName)) -- ^ GHC-Tycon-to-fixpoint Tycon map @@ -413,10 +411,10 @@ data Spec ty bndr = Spec , lazy :: !(S.HashSet F.LocSymbol) -- ^ Ignore Termination Check in these Functions , rewrites :: !(S.HashSet F.LocSymbol) -- ^ Theorems turned into rewrite rules , rewriteWith :: !(M.HashMap F.LocSymbol [F.LocSymbol]) -- ^ Definitions using rewrite rules - , fails :: !(S.HashSet F.LocSymbol) -- ^ These Functions should be unsafe + , fails :: !(S.HashSet (F.Located LHName)) -- ^ These Functions should be unsafe , reflects :: !(S.HashSet F.LocSymbol) -- ^ Binders to reflect , opaqueReflects :: !(S.HashSet F.LocSymbol) -- ^ Binders to opaque-reflect - , autois :: !(M.HashMap F.LocSymbol (Maybe Int)) -- ^ Automatically instantiate axioms in these Functions with maybe specified fuel + , autois :: !(S.HashSet F.LocSymbol) -- ^ Automatically instantiate axioms in these Functions , hmeas :: !(S.HashSet F.LocSymbol) -- ^ Binders to turn into measures using haskell definitions , hbounds :: !(S.HashSet F.LocSymbol) -- ^ Binders to turn into bounds using haskell definitions , inlines :: !(S.HashSet F.LocSymbol) -- ^ Binders to turn into logic inline using haskell definitions @@ -463,7 +461,6 @@ instance Semigroup (Spec ty bndr) where , ialiases = ialiases s1 ++ ialiases s2 , dataDecls = dataDecls s1 ++ dataDecls s2 , newtyDecls = newtyDecls s1 ++ newtyDecls s2 - , includes = sortNub $ includes s1 ++ includes s2 , aliases = aliases s1 ++ aliases s2 , ealiases = ealiases s1 ++ ealiases s2 , qualifiers = qualifiers s1 ++ qualifiers s2 @@ -495,7 +492,7 @@ instance Semigroup (Spec ty bndr) where , ignores = S.union (ignores s1) (ignores s2) , autosize = S.union (autosize s1) (autosize s2) , bounds = M.union (bounds s1) (bounds s2) - , autois = M.union (autois s1) (autois s2) + , autois = S.union (autois s1) (autois s2) } instance Monoid (Spec ty bndr) where @@ -510,7 +507,6 @@ instance Monoid (Spec ty bndr) where , ialiases = [] , dataDecls = [] , newtyDecls = [] - , includes = [] , aliases = [] , ealiases = [] , embeds = mempty @@ -520,7 +516,7 @@ instance Monoid (Spec ty bndr) where , rewrites = S.empty , rewriteWith = M.empty , fails = S.empty - , autois = M.empty + , autois = S.empty , hmeas = S.empty , reflects = S.empty , opaqueReflects = S.empty @@ -555,8 +551,6 @@ instance Monoid (Spec ty bndr) where -- -- What we /do not/ have compared to a 'BareSpec': -- --- * The 'localSigs', as it's not necessary/visible to clients; --- * The 'includes', as they are probably not reachable for clients anyway; -- * The 'reflSigs', they are now just \"normal\" signatures; -- * The 'lazy', we don't do termination checking in lifted specs; -- * The 'reflects', the reflection has already happened at this point; @@ -598,8 +592,8 @@ data LiftedSpec = LiftedSpec -- ^ Qualifiers in source/spec files , liftedLvars :: HashSet F.LocSymbol -- ^ Variables that should be checked in the environment they are used - , liftedAutois :: M.HashMap F.LocSymbol (Maybe Int) - -- ^ Automatically instantiate axioms in these Functions with maybe specified fuel + , liftedAutois :: S.HashSet F.LocSymbol + -- ^ Automatically instantiate axioms in these Functions , liftedAutosize :: HashSet F.LocSymbol -- ^ Type Constructors that get automatically sizing info , liftedCmeasures :: HashSet (Measure LocBareType ()) @@ -684,7 +678,7 @@ dropDependency sm (TargetDependencies deps) = TargetDependencies (M.delete sm de -- | Returns 'True' if the input 'Var' is a /PLE/ one. isPLEVar :: TargetSpec -> Var -> Bool -isPLEVar sp x = M.member x (gsAutoInst (gsRefl sp)) +isPLEVar sp x = S.member x (gsAutoInst (gsRefl sp)) -- | Returns 'True' if the input 'Var' was exported in the module the input 'TargetSrc' represents. isExportedVar :: TargetSrc -> Var -> Bool @@ -849,7 +843,6 @@ unsafeFromLiftedSpec a = Spec , ialiases = S.toList . liftedIaliases $ a , dataDecls = S.toList . liftedDataDecls $ a , newtyDecls = S.toList . liftedNewtyDecls $ a - , includes = mempty , aliases = S.toList . liftedAliases $ a , ealiases = S.toList . liftedEaliases $ a , embeds = liftedEmbeds a diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs index 4e68384cc0..a7d18bdaf2 100644 --- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs +++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs @@ -177,6 +177,7 @@ import Language.Fixpoint.Types (Expr, Symbol) import Language.Haskell.Liquid.GHC.Misc import Language.Haskell.Liquid.GHC.Logging as GHC import Language.Haskell.Liquid.Types.Errors +import Language.Haskell.Liquid.Types.Names import Language.Haskell.Liquid.Types.RType import Language.Haskell.Liquid.Misc @@ -716,7 +717,7 @@ data RClass ty = RClass { rcName :: BTyCon , rcSupers :: [ty] , rcTyVars :: [BTyVar] - , rcMethods :: [(F.LocSymbol, ty)] + , rcMethods :: [(F.Located LHName, ty)] } deriving (Eq, Show, Functor, Data, Typeable, Generic) deriving Hashable via Generically (RClass ty) diff --git a/liquidhaskell-boot/tests/Parser.hs b/liquidhaskell-boot/tests/Parser.hs index 2a2235d996..c7e70f7333 100644 --- a/liquidhaskell-boot/tests/Parser.hs +++ b/liquidhaskell-boot/tests/Parser.hs @@ -135,10 +135,6 @@ testSpecP = parseSingleSpec "newtype Foo = Bar {x :: Nat}" @?== "newtype data Foo [] =\n | Bar :: forall . x : Nat -> *" - , testCase "include" $ - parseSingleSpec "include " @?== - "include " - , testCase "invariant" $ parseSingleSpec "invariant {v:Tree a | 0 <= ht v}" @?== "invariant {v : (Tree a) | 0 <= ht v}" diff --git a/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString.hs b/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString.hs index ef443a4b77..7435e5301b 100644 --- a/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString.hs +++ b/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString.hs @@ -307,8 +307,6 @@ import GHC.IO.Buffer import Language.Haskell.Liquid.Prelude hiding (eq) import Language.Haskell.Liquid.Foreign -{-@ include @-} - {-@ memcpy_ptr_baoff :: p:(Ptr a) -> RawBuffer b -> Int diff --git a/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString.hs.hquals b/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString.hs.hquals deleted file mode 100644 index 8bf0bd46ba..0000000000 --- a/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString.hs.hquals +++ /dev/null @@ -1,33 +0,0 @@ - -// for unfoldrN -qualif PLenNat(v:GHC.Ptr.Ptr a) : (0 <= plen v) - -// for UnpackFoldrINLINED -qualif UnpackFoldrINLINED(v:List a, n:int, acc:List a): (len v = n + 1 + (len acc)) - -// for ByteString.inits -qualif BLenGt(v:Data.ByteString.Internal.ByteString, n:int): ((bLength v) > n) - -// for ByteString.concat -qualif BLens(v:List Data.ByteString.Internal.ByteString) : - (0 <= bLengths v) - -qualif BLenLE(v:GHC.Ptr.Ptr a, bs:List Data.ByteString.Internal.ByteString): - (bLengths bs <= plen v) - -// for ByteString.splitWith -qualif SplitWith(v:List Data.ByteString.Internal.ByteString, l:int): - ((bLengths v) + (len v) - 1 = l) - -// for ByteString.unfoldrN -qualif PtrDiff(v:int, i:int, p:GHC.Ptr.Ptr a): - (i - v <= plen p) - - -// for ByteString.split -qualif BSValidOff(v:int,l:int,p:GHC.ForeignPtr.ForeignPtr a): - (v + l <= fplen p) - -qualif SplitLoop(v:List Data.ByteString.Internal.ByteString, l:int, n:int): - ((bLengths v) + (len v) - 1 = l - n) - diff --git a/tests/benchmarks/popl18/ple/pos/Lists.hs b/tests/benchmarks/popl18/ple/pos/Lists.hs index cdf853981a..f189d738f5 100644 --- a/tests/benchmarks/popl18/ple/pos/Lists.hs +++ b/tests/benchmarks/popl18/ple/pos/Lists.hs @@ -14,13 +14,13 @@ propConst1 :: () -> Proof propConst1 _ = trivial -{-@ automatic-instances propConst2 with 3 @-} +{-@ automatic-instances propConst2 @-} {-@ propConst2 :: () -> { (((C 1 (C 2 Emp)) ++ Emp) ++ Emp) == (C 1 (C 2 Emp)) } @-} propConst2 :: () -> Proof propConst2 _ = trivial -{-@ automatic-instances propConst3 with 4 @-} +{-@ automatic-instances propConst3 @-} {-@ propConst3 :: () -> { (((C 1 (C 2 (C 3 Emp))) ++ Emp) ++ Emp) == (C 1 (C 2 (C 3 Emp))) } @-} propConst3 :: () -> Proof propConst3 _ = trivial diff --git a/tests/benchmarks/popl18/ple/pos/Overview.hs b/tests/benchmarks/popl18/ple/pos/Overview.hs index d679b2ea29..2f0de16219 100644 --- a/tests/benchmarks/popl18/ple/pos/Overview.hs +++ b/tests/benchmarks/popl18/ple/pos/Overview.hs @@ -43,8 +43,7 @@ safe () = trivial -- | type Proof = () --- increase fuel to instantiate 3 times! -{-@ automatic-instances safe' with 3 @-} +{-@ automatic-instances safe' @-} {-@ safe' :: () -> { fib 3 == 2 } @-} safe' () = trivial diff --git a/tests/neg/Meas5.hs b/tests/neg/Meas5.hs index c67250207f..843efa3e23 100644 --- a/tests/neg/Meas5.hs +++ b/tests/neg/Meas5.hs @@ -3,8 +3,6 @@ module Meas5 () where import Language.Haskell.Liquid.Prelude -{-@ include @-} - mylen :: [a] -> Int mylen [] = 0 mylen (_:xs) = 1 + mylen xs diff --git a/tests/pos/Meas5.hs b/tests/pos/Meas5.hs index 51dcc3dce4..6297fd837e 100644 --- a/tests/pos/Meas5.hs +++ b/tests/pos/Meas5.hs @@ -2,8 +2,6 @@ module Meas5 () where import Language.Haskell.Liquid.Prelude -{-@ include @-} - mylen :: [a] -> Int mylen [] = 0 mylen (_:xs) = 1 + mylen xs diff --git a/tests/pos/Meas8.hs b/tests/pos/Meas8.hs index e901b8f46f..6a14b3a495 100644 --- a/tests/pos/Meas8.hs +++ b/tests/pos/Meas8.hs @@ -2,8 +2,6 @@ module Meas8 () where import Language.Haskell.Liquid.Prelude -{-@ include @-} - {-@ measure rlen :: [a] -> Int rlen [] = {v | v = 0} rlen (y:ys) = {v | v = (1 + rlen(ys))} diff --git a/tests/pos/SelfList.hs b/tests/pos/SelfList.hs index 41ae3f754f..7aed250cfb 100644 --- a/tests/pos/SelfList.hs +++ b/tests/pos/SelfList.hs @@ -4,8 +4,6 @@ module SelfList () where import Data.Set (Set(..)) -{-@ include @-} - {-@ invariant {v0:[{v: a | (Set_mem v (listElts v0))}] | true } @-} {-@ type IList a = {v0: [{v:a | (Set_mem v (listElts v0))}] | true } @-} diff --git a/tests/pos/selfList.hquals b/tests/pos/selfList.hquals deleted file mode 100644 index e105fc63f7..0000000000 --- a/tests/pos/selfList.hquals +++ /dev/null @@ -1 +0,0 @@ -qualif SelfSet(v : a, xs : [a]): (Set_mem v (listElts xs))