Merge pull request #2422 from ucsd-progsys/fd/dead-code

Eliminate unused fields from specs

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs

@@ -313,8 +313,7 @@ makeGhcSpec0 cfg session tcg localVars src lmap targetSpec dependencySpecs = do
     , _gsTerm   = spcTerm
 
     , _gsLSpec  = finalLiftedSpec
-                { impSigs   = makeImports mspecs
-                , expSigs   = [ (F.symbol v, F.sr_sort $ Bare.varSortedReft embs v) | v <- gsReflects refl ]
+                { expSigs   = [ (F.symbol v, F.sr_sort $ Bare.varSortedReft embs v) | v <- gsReflects refl ]
                 , dataDecls = Bare.dataDeclSize mySpec $ dataDecls mySpec
                 , measures  = Ms.measures mySpec
                   -- We want to export measures in a 'LiftedSpec', especially if they are
@@ -1366,7 +1365,6 @@ makeLiftedSpec :: ModName -> GhcSrc -> Bare.Env
 -----------------------------------------------------------------------------------------
 makeLiftedSpec name src env refl sData sig qual myRTE lSpec0 = lSpec0
   { Ms.asmSigs    = F.notracepp   ("makeLiftedSpec : ASSUMED-SIGS " ++ F.showpp name ) (xbs ++ myDCs)
-  , Ms.reflSigs   = F.notracepp "REFL-SIGS" $ map (first (fmap getLHNameSymbol)) xbs
   , Ms.sigs       = F.notracepp   ("makeLiftedSpec : LIFTED-SIGS " ++ F.showpp name ) $
                       mkSigs (gsTySigs sig)
   , Ms.invariants = [ (Bare.varLocSym <$> x, Bare.specToBare <$> t)

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs

@@ -388,7 +388,6 @@ expandBareSpec rtEnv l sp = sp
   { measures   = expand rtEnv l (measures   sp)
   , asmSigs    = map (second (expand rtEnv l)) (asmSigs sp)
   , sigs       = map (second (expand rtEnv l)) (sigs sp)
-  , reflSigs   = expand rtEnv l (reflSigs   sp)
   , ialiases   = [ (f x, f y) | (x, y) <- ialiases sp ]
   , dataDecls  = expand rtEnv l (dataDecls  sp)
   , newtyDecls = expand rtEnv l (newtyDecls sp)

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs

@@ -455,7 +455,6 @@ qualifyBareSpec env name l bs sp = sp
   { measures   = qualify env name l bs (measures   sp)
   , asmSigs    = qualify env name l bs (asmSigs    sp)
   , sigs       = qualify env name l bs (sigs       sp)
-  , reflSigs   = qualify env name l bs (reflSigs   sp)
   , dataDecls  = qualify env name l bs (dataDecls  sp)
   , newtyDecls = qualify env name l bs (newtyDecls sp)
   , ialiases   = [ (f x, f y) | (x, y) <- ialiases sp ]

liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs

@@ -841,7 +841,6 @@ data Pspec ty ctor
   | 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]
-  | Impt    Symbol                                        -- ^ 'import' a specification module
   | DDecl   DataDecl                                      -- ^ refined 'data'    declaration
   | NTDecl  DataDecl                                      -- ^ refined 'newtype' declaration
   | Relational (LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr) -- ^ relational signature
@@ -916,8 +915,6 @@ ppPspec k (LAsrt (lx, t))
   = "local assert"  <+> pprintTidy k (val lx) <+> "::" <+> pprintTidy k t
 ppPspec k (Asrts (lxs, (t, les)))
   = ppAsserts k lxs t les
-ppPspec k (Impt  x)
-  = "import" <+> pprintTidy k x
 ppPspec k (DDecl d)
   = pprintTidy k d
 ppPspec k (NTDecl d)
@@ -1069,12 +1066,9 @@ mkSpec name xs         = (name,) $ qualifySpec (symbol name) Measure.Spec
   , Measure.asmReflectSigs = [(l, r) | AssmReflect (l, r) <- xs]
   , Measure.sigs       = [a | Asrt   a <- xs]
                       ++ [(y, t) | Asrts (ys, (t, _)) <- xs, y <- ys]
-  , Measure.reflSigs   = []
-  , Measure.impSigs    = []
   , Measure.expSigs    = []
   , Measure.invariants = [(Nothing, t) | Invt   t <- xs]
   , Measure.ialiases   = [t | Using t <- xs]
-  , Measure.imports    = [i | Impt   i <- xs]
   , Measure.dataDecls  = [d | DDecl  d <- xs] ++ [d | NTDecl d <- xs]
   , Measure.newtyDecls = [d | NTDecl d <- xs]
   , Measure.includes   = [q | Incl   q <- xs]
@@ -1146,8 +1140,6 @@ specP
          <|> (reserved "laws"     >> fmap ILaws instanceLawP)
          <|> fmap RInst  instanceP ))
 
-    <|> (reserved "import"        >> fmap Impt   symbolP   )
-
     <|> (reserved "data"
         >> ((reserved "variance"  >> fmap Varia  datavarianceP)
         <|> (reserved "size"      >> fmap DSize  dsizeP)

liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs

@@ -396,15 +396,12 @@ instance Monoid BareSpec where
 -- | A generic 'Spec' type, polymorphic over the inner choice of type and binder.
 data Spec ty bndr  = Spec
   { measures   :: ![Measure ty bndr]                                  -- ^ User-defined properties for ADTs
-  , impSigs    :: ![(F.Symbol, F.Sort)]                               -- ^ Imported variables types
-  , expSigs    :: ![(F.Symbol, F.Sort)]                               -- ^ Exported variables types
-  , asmSigs    :: ![(F.Located LHName, ty)]                                -- ^ Assumed (unchecked) types; including reflected signatures
+  , 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
-  , sigs       :: ![(F.Located LHName, ty)]                           -- ^ Imported functions and types
-  , reflSigs   :: ![(F.LocSymbol, ty)]                                -- ^ Reflected type signatures
+  , 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
-  , imports    :: ![F.Symbol]                                         -- ^ Loaded spec module names
   , dataDecls  :: ![DataDecl]                                         -- ^ Predicated data definitions
   , newtyDecls :: ![DataDecl]                                         -- ^ Predicated new type definitions
   , includes   :: ![FilePath]                                         -- ^ Included qualifier files
@@ -458,15 +455,12 @@ instance (Show ty, Show bndr, F.PPrint ty, F.PPrint bndr) => F.PPrint (Spec ty b
 instance Semigroup (Spec ty bndr) where
   s1 <> s2
     = Spec { measures   =           measures   s1 ++ measures   s2
-           , impSigs    =           impSigs    s1 ++ impSigs    s2
            , expSigs    =           expSigs    s1 ++ expSigs    s2
            , asmSigs    =           asmSigs    s1 ++ asmSigs    s2
            , asmReflectSigs    =    asmReflectSigs s1 ++ asmReflectSigs s2
            , sigs       =           sigs       s1 ++ sigs       s2
-           , reflSigs   =           reflSigs   s1 ++ reflSigs   s2
            , invariants =           invariants s1 ++ invariants s2
            , ialiases   =           ialiases   s1 ++ ialiases   s2
-           , imports    = sortNub $ imports    s1 ++ imports    s2
            , dataDecls  =           dataDecls  s1 ++ dataDecls  s2
            , newtyDecls =           newtyDecls s1 ++ newtyDecls s2
            , includes   = sortNub $ includes   s1 ++ includes   s2
@@ -508,15 +502,12 @@ instance Monoid (Spec ty bndr) where
   mappend = (<>)
   mempty
     = Spec { measures   = []
-           , impSigs    = []
            , expSigs    = []
            , asmSigs    = []
            , asmReflectSigs = []
            , sigs       = []
-           , reflSigs   = []
            , invariants = []
            , ialiases   = []
-           , imports    = []
            , dataDecls  = []
            , newtyDecls = []
            , includes   = []
@@ -581,22 +572,18 @@ instance Monoid (Spec ty bndr) where
 data LiftedSpec = LiftedSpec
   { liftedMeasures   :: HashSet (Measure LocBareType F.LocSymbol)
     -- ^ User-defined properties for ADTs
-  , liftedImpSigs    :: HashSet (F.Symbol, F.Sort)
-    -- ^ Imported variables types
   , liftedExpSigs    :: HashSet (F.Symbol, F.Sort)
-    -- ^ Exported variables types
+    -- ^ 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)
-    -- ^ Imported functions and types
+    -- ^ Asserted spec signatures
   , liftedInvariants :: HashSet (Maybe F.LocSymbol, LocBareType)
     -- ^ Data type invariants; the Maybe is the generating measure
   , liftedIaliases   :: HashSet (LocBareType, LocBareType)
     -- ^ Data type invariants to be checked
-  , liftedImports    :: HashSet F.Symbol
-    -- ^ Loaded spec module names
   , liftedDataDecls  :: HashSet DataDecl
     -- ^ Predicated data definitions
   , liftedNewtyDecls :: HashSet DataDecl
@@ -642,14 +629,12 @@ instance Binary F.Equation
 emptyLiftedSpec :: LiftedSpec
 emptyLiftedSpec = LiftedSpec
   { liftedMeasures = mempty
-  , liftedImpSigs  = mempty
   , liftedExpSigs  = mempty
   , liftedAsmSigs  = mempty
   , liftedAsmReflectSigs  = mempty
   , liftedSigs     = mempty
   , liftedInvariants = mempty
   , liftedIaliases   = mempty
-  , liftedImports    = mempty
   , liftedDataDecls  = mempty
   , liftedNewtyDecls = mempty
   , liftedAliases    = mempty
@@ -821,14 +806,12 @@ fromBareSpec = getBareSpec
 toLiftedSpec :: Spec LocBareType F.LocSymbol -> LiftedSpec
 toLiftedSpec a = LiftedSpec
   { liftedMeasures   = S.fromList . measures $ a
-  , liftedImpSigs    = S.fromList . impSigs  $ 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
-  , liftedImports    = S.fromList . imports $ a
   , liftedDataDecls  = S.fromList . dataDecls $ a
   , liftedNewtyDecls = S.fromList . newtyDecls $ a
   , liftedAliases    = S.fromList . aliases $ a
@@ -856,17 +839,14 @@ toLiftedSpec a = LiftedSpec
 unsafeFromLiftedSpec :: LiftedSpec -> Spec LocBareType F.LocSymbol
 unsafeFromLiftedSpec a = Spec
   { measures   = S.toList . liftedMeasures $ a
-  , impSigs    = S.toList . liftedImpSigs $ a
   , expSigs    = S.toList . liftedExpSigs $ a
   , asmSigs    = S.toList . liftedAsmSigs $ a
   , asmReflectSigs = S.toList . liftedAsmReflectSigs $ a
   , sigs       = S.toList . liftedSigs $ a
-  , reflSigs   = mempty
   , relational = mempty
   , asmRel     = mempty
   , invariants = S.toList . liftedInvariants $ a
   , ialiases   = S.toList . liftedIaliases $ a
-  , imports    = S.toList . liftedImports $ a
   , dataDecls  = S.toList . liftedDataDecls $ a
   , newtyDecls = S.toList . liftedNewtyDecls $ a
   , includes   = mempty

liquidhaskell-boot/tests/Parser.hs

@@ -123,10 +123,6 @@ testSpecP =
        parseSingleSpec "class Sized s where\n  size :: forall a. x:s a -> {v:Nat | v = sz x}" @?==
             "class  (Sized s) where\n    size :: forall a . x:s a -> {v : Nat | v == sz x}"
 
-    , testCase "import" $
-       parseSingleSpec "import Foo" @?==
-          "import Foo"
-
     , testCase "data variance" $
        parseSingleSpec "data variance IO bivariant" @?==
           "data variance IO Bivariant"