Remove unused field hbounds from Specs

ucsd-progsys · Nov 7, 2024 · 925f8b7 · 925f8b7
1 parent 13cdc83
commit 925f8b7
Show file tree

Hide file tree

Showing 7 changed files with 5 additions and 23 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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