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