Allow local logical aliases (defines)

liquid-prelude/src/Language/Haskell/Liquid/Bag.hs

@@ -19,44 +19,50 @@ import qualified Data.Map      as M
 data Bag a = Bag { toMap :: M.Map a Int } deriving Eq
 
 {-@ assume empty :: {v:Bag k | v = Bag_empty 0} @-}
+{-@ define empty                = (Bag_empty 0) @-}
 empty :: Bag k
 empty = Bag M.empty
 
 {-@ assume get :: (Ord k) => k:k -> b:Bag k -> {v:Nat | v = Bag_count b k}  @-}
+{-@ define get               k      b                    = (Bag_count b k) @-}
 get :: (Ord k) => k -> Bag k -> Int
 get k b = M.findWithDefault 0 k (toMap b)
 
 {-@ assume put :: (Ord k) => k:k -> b:Bag k -> {v:Bag k | v = Bag_union b (Bag_sng k 1)} @-}
-{-@ ignore put @-}
+{-@ define put               k      b                      = (Bag_union b (Bag_sng k 1)) @-}
 put :: (Ord k) => k -> Bag k -> Bag k
 put k b = Bag (M.insert k (1 + get k b) (toMap b))
 
-{-@ fromList :: (Ord k) => xs:[k] -> {v:Bag k | v == fromList xs } @-}
-fromList :: (Ord k) => [k] -> Bag k
-fromList []     = empty
-fromList (x:xs) = put x (fromList xs)
-
-{-@ assume union :: (Ord k) => m1:Bag k -> m2:Bag k -> {v:Bag k | v = Bag_union m1 m2} @-}
+{-@ assume union :: (Ord k) => a:Bag k -> b:Bag k -> {v:Bag k | v = Bag_union a b} @-}
+{-@ define union               a          b                      = (Bag_union a b) @-}
 union :: (Ord k) => Bag k -> Bag k -> Bag k
 union b1 b2 = Bag (M.unionWith (+) (toMap b1) (toMap b2))
 
-{-@ assume unionMax :: (Ord k) => m1:Bag k -> m2:Bag k -> {v:Bag k | v = Bag_union_max m1 m2} @-}
+{-@ assume unionMax :: (Ord k) => a:Bag k -> b:Bag k -> {v:Bag k | v = Bag_union_max a b} @-}
+{-@ define unionMax               a          b                      = (Bag_union_max a b) @-}
 unionMax :: (Ord k) => Bag k -> Bag k -> Bag k
 unionMax b1 b2 = Bag (M.unionWith max (toMap b1) (toMap b2))
 
-{-@ assume interMin :: (Ord k) => m1:Bag k -> m2:Bag k -> {v:Bag k | v = Bag_inter_min m1 m2} @-}
+{-@ assume interMin :: (Ord k) => a:Bag k -> b:Bag k -> {v:Bag k | v = Bag_inter_min a b} @-}
+{-@ define interMin               a          b                      = (Bag_inter_min a b) @-}
 interMin :: (Ord k) => Bag k -> Bag k -> Bag k
 interMin b1 b2 = Bag (M.intersectionWith min (toMap b1) (toMap b2))
 
-{-@ assume sub :: (Ord k) => m1:Bag k -> m2:Bag k -> {v:Bool | v = Bag_sub m1 m2} @-}
+{-@ assume sub :: (Ord k) => a:Bag k -> b:Bag k -> {v:Bool | v = Bag_sub a b} @-}
+{-@ define sub               a          b                     = (Bag_sub a b) @-}
 sub :: (Ord k) => Bag k -> Bag k -> Bool
 sub b1 b2 = M.isSubmapOfBy (<=) (toMap b1) (toMap b2)
 
+{-@ fromList :: (Ord k) => xs:[k] -> {v:Bag k | v == fromList xs } @-}
+fromList :: (Ord k) => [k] -> Bag k
+fromList []     = empty
+fromList (x:xs) = put x (fromList xs)
+
 {-@ assume bagSize :: b:Bag k -> {i:Nat | i == bagSize b} @-}
 bagSize :: Bag k -> Int
 bagSize b = sum (M.elems (toMap b))
 
-{-@ thm_emp :: x:k -> xs:Bag k -> { Language.Haskell.Liquid.Bag.empty /= put x xs } @-}
+{-@ thm_emp :: x:k -> xs:Bag k -> { empty /= put x xs } @-}
 thm_emp :: (Ord k) => k -> Bag k -> ()
 thm_emp x xs = const () (get x xs)
 

liquid-prelude/src/Language/Haskell/Liquid/ProofCombinators.hs

@@ -10,7 +10,7 @@ module Language.Haskell.Liquid.ProofCombinators (
 
   -- * Proof is just a () alias
   Proof
-  , toProof 
+  , toProof
 
   -- * Proof constructors
   , trivial, unreachable, (***), QED(..)
@@ -21,18 +21,18 @@ module Language.Haskell.Liquid.ProofCombinators (
   -- * These two operators check all intermediate equalities
   , (===) -- proof of equality is implicit eg. x === y
   , (=<=) -- proof of equality is implicit eg. x <= y
-  , (=>=)  -- proof of equality is implicit eg. x =>= y 
+  , (=>=)  -- proof of equality is implicit eg. x =>= y
 
   -- * This operator does not check intermediate equalities
-  , (==.) 
+  , (==.)
 
   -- Uncheck operator used only for proof debugging
   , (==!) -- x ==! y always succeeds
 
   -- * Combining Proofs
   , (&&&)
-  , withProof 
-  , impossible 
+  , withProof
+  , impossible
 
   -- * PLE-specific
   , pleUnfold
@@ -120,9 +120,9 @@ _ =>= y  = y
 infixl 3 ?
 
 {-@ (?) :: forall a b <pa :: a -> Bool, pb :: b -> Bool>. a<pa> -> b<pb> -> a<pa> @-}
-(?) :: a -> b -> a 
-x ? _ = x 
-{-# INLINE (?)   #-} 
+(?) :: a -> b -> a
+x ? _ = x
+{-# INLINE (?)   #-}
 
 -------------------------------------------------------------------------------
 -- | Assumed equality
@@ -149,13 +149,13 @@ infixl 3 ==!
 -- | The above operators check each intermediate proof step.
 --   The operator `==.` below accepts an optional proof term
 --   argument, but does not check intermediate steps.
---   So, using `==.` the proofs are faster, but the error messages worse. 
+--   So, using `==.` the proofs are faster, but the error messages worse.
 
 infixl 3 ==.
 
-{-# INLINE (==.) #-} 
-(==.) :: a -> a -> a 
-_ ==. x = x 
+{-# INLINE (==.) #-}
+(==.) :: a -> a -> a
+_ ==. x = x
 
 -------------------------------------------------------------------------------
 -- | * Combining Proof Certificates -------------------------------------------
@@ -165,7 +165,8 @@ _ ==. x = x
 x &&& _ = x
 
 
-{-@ withProof :: x:a -> b -> {v:a | v = x} @-}
+{-@        withProof :: x:a -> b -> {v:a | v = x} @-}
+{-@ define withProof    x      y            = (x) @-}
 withProof :: a -> b -> a
 withProof x _ = x
 
@@ -174,7 +175,7 @@ impossible :: a -> b
 impossible _ = undefined
 
 -------------------------------------------------------------------------------
--- | Convenient Syntax for Inductive Propositions 
+-- | Convenient Syntax for Inductive Propositions
 -------------------------------------------------------------------------------
 
 {-@ measure prop :: a -> b           @-}

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

@@ -64,7 +64,6 @@ import Data.Hashable (Hashable)
 import Data.Bifunctor (bimap, first)
 import Data.Function (on)
 
-
 {- $creatingTargetSpecs
 
 /Liquid Haskell/ operates on 'TargetSpec's, so this module provides a single function called
@@ -106,7 +105,10 @@ makeTargetSpec cfg localVars lnameEnv lmap targetSrc bareSpec dependencies = do
         Left d -> return $ Left d
         Right (warns, ghcSpec) -> do
           let targetSpec = toTargetSpec ghcSpec
+--              bareSpec1 = ghcSpecToBareSpec ghcSpec
+--              liftedSpec = toLiftedSpec lnameEnv (bareSpec1 { defines = defines bareSpec })
               liftedSpec = ghcSpecToLiftedSpec ghcSpec
+
           liftedSpec' <- removeUnexportedLocalAssumptions liftedSpec
           return $ Right (phaseOneWarns <> warns, targetSpec, liftedSpec')
 
@@ -135,9 +137,10 @@ makeTargetSpec cfg localVars lnameEnv lmap targetSrc bareSpec dependencies = do
           exportedAssumption _ = True
       return lspec { liftedAsmSigs = S.filter (exportedAssumption . val . fst) (liftedAsmSigs lspec) }
 
+--    ghcSpecToBareSpec = toBareSpecLHName cfg lnameEnv . _gsLSpec
+--    ghcSpecToLiftedSpec = toLiftedSpec lnameEnv . toBareSpecLHName cfg lnameEnv . _gsLSpec
     ghcSpecToLiftedSpec = toLiftedSpec . toBareSpecLHName cfg lnameEnv . _gsLSpec
 
-
 -------------------------------------------------------------------------------------
 -- | @makeGhcSpec@ invokes @makeGhcSpec0@ to construct the @GhcSpec@ and then
 --   validates it using @checkGhcSpec@.
@@ -283,6 +286,7 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec
                 , cmeasures  = mconcat $ map Ms.cmeasures $ map snd dependencySpecs ++ [targetSpec]
                 , embeds = Ms.embeds targetSpec
                 , privateReflects = mconcat $ map (privateReflects . snd) mspecs
+                , defines = Ms.defines targetSpec
                 }
     })
   where

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

@@ -553,7 +553,7 @@ checkAbstractRefs rt = go rt
 
 checkReft                    :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar (UReft r)))
                              => F.SrcSpan -> F.SEnv F.SortedReft -> F.TCEmb TyCon -> Maybe (RRType (UReft r)) -> UReft r -> Maybe Doc
-checkReft _ _   _   Nothing _   = Nothing -- TODO:RPropP/Ref case, not sure how to check these yet.
+checkReft _  _   _   Nothing  _ = Nothing -- TODO:RPropP/Ref case, not sure how to check these yet.
 checkReft sp env emb (Just t) _ = (\z -> dr $+$ z) <$> checkSortedReftFull sp env r
   where
     r                           = rTypeSortedReft emb t

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

@@ -140,7 +140,7 @@ makeMeasureInline allowTC embs lmap cbs x =
     Just (v, defn) -> (vx, coreToFun' allowTC embs Nothing lmap vx v defn ok)
                      where
                        vx         = F.atLoc x (F.symbol v)
-                       ok (xs, e) = LMap vx (F.symbol <$> xs) (either id id e)
+                       ok (xs, e) = LMapV vx (F.symbol <$> xs) (either id id e)
 
 -- | @coreToFun'@ takes a @Maybe DataConMap@: we need a proper map when lifting
 --   measures and reflects (which have case-of, and hence, need the projection symbols),
@@ -387,7 +387,7 @@ getLocReflects = S.unions . map names . M.elems
 -- Get all the symbols that are defined in the logic, based on the environment and the specs.
 -- Also, fully qualify the defined symbols by the way (for those for which it's possible and not already done).
 getDefinedSymbolsInLogic :: Bare.Env -> Bare.MeasEnv -> Bare.ModSpecs -> S.HashSet F.LocSymbol
-getDefinedSymbolsInLogic env measEnv specs = 
+getDefinedSymbolsInLogic env measEnv specs =
   S.unions (uncurry getFromAxioms <$> specsList) -- reflections that ended up in equations
     `S.union` getLocReflects specs -- reflected symbols
     `S.union` measVars -- Get the data constructors, ex. for Lit00.0
@@ -472,7 +472,7 @@ getUnfoldingOfVar = getExpr . Ghc.realUnfoldingInfo . Ghc.idInfo
 -- For this purpose, you need to give the variable naming the definition to reflect
 -- and its corresponding equation in the logic.
 getFreeVarsOfReflectionOfVar  :: Ghc.Var -> F.Equation -> S.HashSet Ghc.Var
-getFreeVarsOfReflectionOfVar var eq = 
+getFreeVarsOfReflectionOfVar var eq =
     S.filter (\v -> F.symbol v `S.member` freeSymbolsInReflectedBody) freeVarsInCoreExpr
   where
     reflExpr = getUnfoldingOfVar var

liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs

@@ -2,7 +2,27 @@ module Language.Haskell.Liquid.GHC.CoreToLogic where
 
 coreToLogic :: String
 coreToLogic = unlines
-  [ "define Data.Set.Base.singleton x      = (Set_sng x)"
+  [ "define GHC.Types.True                   = (true)"
+  , "define GHC.Internal.Real.div x y        = (x / y)"
+  , "define GHC.Internal.Real.mod x y        = (x mod y)"
+  , "define GHC.Internal.Real.fromIntegral x = (x)"
+
+  , "define GHC.Classes.not x                = (~ x)"
+  , "define GHC.Internal.Base.$ f x          = (f x)"
+  , ""
+  , "define GHC.CString.unpackCString# x = x"
+  , ""
+  , "define Main.mempty       = (mempty)"
+  , ""
+  , "define Control.Parallel.Strategies.withStrategy s x = (x)"
+  , ""
+  , "define Language.Haskell.Liquid.Equational.eq x y = (y)"
+
+  , "define Language.Haskell.Liquid.ProofCombinators.cast x y = (y)"
+  , "define Liquid.ProofCombinators.cast x y = (y)"
+  , "define ProofCombinators.cast x y = (y)"
+  , ""
+  , "define Data.Set.Base.singleton x      = (Set_sng x)"
   , "define Data.Set.Base.union x y        = (Set_cup x y)"
   , "define Data.Set.Base.intersection x y = (Set_cap x y)"
   , "define Data.Set.Base.difference x y   = (Set_dif x y)"
@@ -21,33 +41,4 @@ coreToLogic = unlines
   , "define Data.Set.Internal.member x xs      = (Set_mem x xs)"
   , "define Data.Set.Internal.isSubsetOf x y   = (Set_sub x y)"
   , "define Data.Set.Internal.fromList xs      = (Data.Set_LHAssumptions.listElts xs)"
-  , ""
-  , "define GHC.Internal.Real.fromIntegral x = (x)"
-  , ""
-  , "define GHC.Types.True                 = (true)"
-  , "define GHC.Internal.Real.div x y      = (x / y)"
-  , "define GHC.Internal.Real.mod x y      = (x mod y)"
-  , "define GHC.Internal.Num.fromInteger x = (x)"
-  , "define GHC.Num.Integer.IS x           = (x)"
-  , "define GHC.Classes.not x              = (~ x)"
-  , "define GHC.Internal.Base.$ f x        = (f x)"
-  , ""
-  , "define Language.Haskell.Liquid.Bag.get k b      = (Bag_count b k)"
-  , "define Language.Haskell.Liquid.Bag.put k b      = (Bag_union b (Bag_sng k 1))"
-  , "define Language.Haskell.Liquid.Bag.union a b    = (Bag_union a b)"
-  , "define Language.Haskell.Liquid.Bag.unionMax a b = (Bag_union_max a b)"
-  , "define Language.Haskell.Liquid.Bag.interMin a b = (Bag_inter_min a b)"
-  , "define Language.Haskell.Liquid.Bag.sub a b      = (Bag_sub a b)"
-  , "define Language.Haskell.Liquid.Bag.empty        = (Bag_empty 0)"
-  , ""
-  , "define Main.mempty       = (mempty)"
-  , "define Language.Haskell.Liquid.ProofCombinators.cast x y = (y)"
-  , "define Language.Haskell.Liquid.ProofCombinators.withProof x y = (x)"
-  , "define ProofCombinators.cast x y = (y)"
-  , "define Liquid.ProofCombinators.cast x y = (y)"
-  , "define Control.Parallel.Strategies.withStrategy s x = (x)"
-  , ""
-  , "define Language.Haskell.Liquid.Equational.eq x y = (y)"
-  , ""
-  , "define GHC.CString.unpackCString# x = x"
   ]

liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs

@@ -274,8 +274,8 @@ makeLogicMap = do
     Right lm -> return (lm <> listLMap)
 
 listLMap :: LogicMap -- TODO-REBARE: move to wiredIn
-listLMap  = toLogicMap [ (dummyLoc nilName , []     , hNil)
-                       , (dummyLoc consName, [x, xs], hCons (EVar <$> [x, xs])) ]
+listLMap  = toLogicMap [ (dummyLoc nilName , ([]     , hNil))
+                       , (dummyLoc consName, ([x, xs], hCons (EVar <$> [x, xs]))) ]
   where
     x     = "x"
     xs    = "xs"

liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs

@@ -19,11 +19,12 @@ import qualified Liquid.GHC.API         as O
 import           Liquid.GHC.API         as GHC hiding (Type)
 import qualified Text.PrettyPrint.HughesPJ               as PJ
 import qualified Language.Fixpoint.Types                 as F
-import qualified  Language.Haskell.Liquid.GHC.Misc        as LH
+import qualified Language.Haskell.Liquid.GHC.Misc        as LH
 import qualified Language.Haskell.Liquid.UX.CmdLine      as LH
 import qualified Language.Haskell.Liquid.GHC.Interface   as LH
 import           Language.Haskell.Liquid.LHNameResolution (resolveLHNames)
 import qualified Language.Haskell.Liquid.Liquid          as LH
+import qualified Language.Haskell.Liquid.Types.Names     as LH
 import qualified Language.Haskell.Liquid.Types.PrettyPrint as LH ( filterReportErrors
                                                                  , filterReportErrorsWith
                                                                  , defaultFilterReporter
@@ -36,13 +37,15 @@ import           Language.Haskell.Liquid.GHC.Plugin.SpecFinder
                                                          as SpecFinder
 
 import           Language.Haskell.Liquid.GHC.Types       (MGIModGuts(..), miModGuts)
+
 import           Language.Haskell.Liquid.Transforms.InlineAux (inlineAux)
 import           Language.Haskell.Liquid.Transforms.Rewrite (rewriteBinds)
 
 import           Control.Monad
 import qualified Control.Monad.Catch as Ex
 import           Control.Monad.IO.Class (MonadIO)
 
+--import           Data.Bifunctor                           ( first )
 import           Data.Coerce
 import           Data.Function                            ((&))
 import qualified Data.List                               as L
@@ -75,6 +78,8 @@ import qualified Language.Haskell.Liquid.Bare.Resolve as Resolve
 import           Language.Haskell.Liquid.UX.CmdLine
 import           Language.Haskell.Liquid.UX.Config
 
+-- import Debug.Trace
+
 -- | Represents an abnormal but non-fatal state of the plugin. Because it is not
 -- meant to escape the plugin, it is not thrown in IO but instead carried around
 -- in an `Either`'s `Left` case and handled at the top level of the plugin
@@ -286,7 +291,6 @@ typecheckHook cfg0 ms tcGblEnv = swapBreadcrumb thisModule Nothing >>= \case
   where
     thisModule = ms_mod ms
 
-
 typecheckHook' :: Config -> ModSummary -> TcGblEnv -> [SpecComment] -> TcM (Either LiquidCheckException TcGblEnv)
 typecheckHook' cfg ms tcGblEnv specComments = do
   debugLog $ "We are in module: " <> show (toStableModule thisModule)
@@ -377,7 +381,7 @@ processInputSpec cfg pipelineData modSummary inputSpec = do
 
   logicMap :: LogicMap <- liftIO LH.makeLogicMap
 
-  -- debugLog $ "Logic map:\n" ++ show logicMap
+-- debugLog $ "Logic map:\n" ++ show logicMap
 
   let lhContext = LiquidHaskellContext {
         lhGlobalCfg       = cfg
@@ -543,25 +547,34 @@ processModule LiquidHaskellContext{..} = do
 
     tcg <- getGblEnv
     let localVars = Resolve.makeLocalVars preNormalizedCore
+        -- modsym = symbol $ GHC.moduleName thisModule
+        --defs = {- first (fmap (LH.qualifySymbol modsym)) <$> -} defines bareSpec0
+        -- ldefines = liftedDefines <$> (HM.elems . getDependencies) dependencies
+        -- ldefines' = trace ("processModule ldefines = " ++ show (map HM.keys ldefines)) $ ldefines
+        depsLogicMap = foldr (\ls lmp -> lmp <> mempty {lmSymDefs = HM.map (\l -> LH.lhNameToResolvedSymbol <$> l) $ liftedDefines ls}) mempty $
+                       (HM.elems . getDependencies) dependencies
+        -- depsLogicMap = foldr (\ls lmp -> lmp <> mempty {lmSymDefs = HM.map (\l -> LH.logicNameToSymbol <$> l) $ ls}) mempty ldefines'
+        lm = lhModuleLogicMap <> depsLogicMap--  <> mempty {lmSymDefs = HM.fromList $ map (\(k , v) -> (LH.getLHNameSymbol $ F.val k , fmap val v)) defs }
         eBareSpec = resolveLHNames
           moduleCfg
           thisModule
           localVars
           (imp_mods $ tcg_imports tcg)
           (tcg_rdr_env tcg)
-          lhModuleLogicMap
-          bareSpec0
+          lm
+          bareSpec0 -- { defines = defs }
           dependencies
     result <-
       case eBareSpec of
         Left errors -> pure $ Left $ mkDiagnostics [] errors
-        Right (bareSpec, lnameEnv) ->
+        Right (bareSpec, lnameEnv, lmap') ->
+          -- let lmap'' = trace ("processModule lmap' = " ++ show lmap') $ lmap' in
           fmap (,bareSpec) <$>
             makeTargetSpec
               moduleCfg
               localVars
               lnameEnv
-              lhModuleLogicMap
+              lmap' {- lmap'' -}
               targetSrc
               bareSpec
               dependencies