Merge pull request #2423 from ucsd-progsys/fd/fail-names

Use LHName for fail annotations and methods in class specs

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"
 
 
 ----------------------------------------------------------------------------------------

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

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)

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

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)
 

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 <listSet.hquals>" @?==
-            "include <listSet.hquals>"
-
     , testCase "invariant" $
        parseSingleSpec "invariant {v:Tree a | 0 <= ht v}" @?==
             "invariant {v : (Tree a) | 0 <= ht v}"

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 <Data/ByteString.hs.hquals> @-}
-
 {-@ memcpy_ptr_baoff :: p:(Ptr a)
                      -> RawBuffer b
                      -> Int