Allow local logical aliases (defines)

docs/mkDocs/docs/options.md

@@ -132,8 +132,8 @@ you can assume the reflection of both functions by defining a *pretended* functi
 as the actual function. Therein lies the assumption: if both functions don't actually behave in the same way, then you
 may introduce falsity in your logic. Thus, you have to use it with caution, only when the function wasn't already reflected,
 and when you actually know how it will behave. In the following snippet, `myfilter` is the pretended function whose definition
-is given in our module, and the actual function `GHC.List.filter` and `myfilter` and tied through 
-the `{-@ assume reflect filter as myfilter @-}` annotation. This annotation must be read as: "reflect `filter`, assuming it has the 
+is given in our module, and the actual function `GHC.List.filter` and `myfilter` and tied through
+the `{-@ assume reflect filter as myfilter @-}` annotation. This annotation must be read as: "reflect `filter`, assuming it has the
 same reflection as `myfilter`".
 
 ```Haskell
@@ -390,6 +390,29 @@ the error. If you don't want the above and instead, want only the
 By default, the inferred types will have fully qualified module names.
 To use unqualified names, much easier to read, use `--short-names`.
 
+## Logical aliasing
+
+**Directives:** `define`
+
+You can force LiquidHaskell to treat each occurrence of a Haskell name (such as
+a function or a data constructor) as a predefined logical expression with the
+`define` directive. This can be useful for treating Haskell system functions
+as  no-ops, or for linking operations on your datatypes directly to SMT theories.
+
+As an example,
+
+```haskell
+{-@ define foo x y = (Foo_t y) @-}
+```
+
+will replace every occurrence of a Haskell symbol `foo` applied to two arguments
+with a logical symbol `Foo_t` applied to only the second argument, when processing
+specifications. The symbol `foo` can either be defined in the current module or
+imported, and the defined alias is propagated to the dependencies.
+
+See `Language.Haskell.Liquid.Bag` and `Language.Haskell.Liquid.ProofCombinators`
+for examples.
+
 ## Disabling Checks on Functions
 
 **Directives:** `ignore`
@@ -444,18 +467,18 @@ See the [specifications section](specifications.md) for how to write termination
 ## Positivity Check
 
 **Options:** `no-positivity-check`
-By **default** a positivity check is performed on data definitions. 
+By **default** a positivity check is performed on data definitions.
 
 
 ```haskell
-data Bad = Bad (Bad -> Bad) | Good Bad 
+data Bad = Bad (Bad -> Bad) | Good Bad
     --           A      B           C
     -- A is in a negative position, B and C are OK
 ```
 
 Negative declarations are rejected because they admit non-terminating functions.
 
-If the positivity check is disabled, so that a similar declaration of `Bad` is allowed, 
+If the positivity check is disabled, so that a similar declaration of `Bad` is allowed,
 it is possible to construct a term of the empty type, even without recursion.
 For example see [tests/neg/Positivity1.hs](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/errors/Positivity1.hs)
 and [tests/neg/Positivity2.hs](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/errors/Positivity2.hs)

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

@@ -283,6 +283,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

@@ -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,52 +2,13 @@ module Language.Haskell.Liquid.GHC.CoreToLogic where
 
 coreToLogic :: String
 coreToLogic = unlines
-  [ "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)"
-  , "define Data.Set.Base.empty            = (Set_empty 0)"
-  , "define Data.Set.Base.null x           = (Set_emp x)"
-  , "define Data.Set.Base.member x xs      = (Set_mem x xs)"
-  , "define Data.Set.Base.isSubsetOf x y   = (Set_sub x y)"
-  , "define Data.Set.Base.fromList xs      = (listElts xs)"
-  , ""
-  , "define Data.Set.Internal.singleton x      = (Set_sng x)"
-  , "define Data.Set.Internal.union x y        = (Set_cup x y)"
-  , "define Data.Set.Internal.intersection x y = (Set_cap x y)"
-  , "define Data.Set.Internal.difference x y   = (Set_dif x y)"
-  , "define Data.Set.Internal.empty            = (Set_empty 0)"
-  , "define Data.Set.Internal.null x           = (Set_emp x)"
-  , "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 GHC.Types.True                   = (true)"
+  , "define GHC.Classes.not x                = (~ x)"
+  , "define GHC.Internal.Base.$ f x          = (f x)"
   , "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"
+  , "define Language.Haskell.Liquid.ProofCombinators.cast x y = (y)"
+  , "define Liquid.ProofCombinators.cast x y = (y)"
+  , "define ProofCombinators.cast x y = (y)"
   ]

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
@@ -286,7 +287,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)
@@ -543,25 +543,31 @@ processModule LiquidHaskellContext{..} = do
 
     tcg <- getGblEnv
     let localVars = Resolve.makeLocalVars preNormalizedCore
+        -- add defines from dependencies to the logical map
+        logicMapWithDeps =
+          foldr (\ls lmp ->
+                     lmp <> mkLogicMap (HM.map (fmap LH.lhNameToResolvedSymbol) $ liftedDefines ls))
+                lhModuleLogicMap $
+            (HM.elems . getDependencies) dependencies
         eBareSpec = resolveLHNames
           moduleCfg
           thisModule
           localVars
           (imp_mods $ tcg_imports tcg)
           (tcg_rdr_env tcg)
-          lhModuleLogicMap
+          logicMapWithDeps
           bareSpec0
           dependencies
     result <-
       case eBareSpec of
         Left errors -> pure $ Left $ mkDiagnostics [] errors
-        Right (bareSpec, lnameEnv) ->
+        Right (bareSpec, lnameEnv, lmap') ->
           fmap (,bareSpec) <$>
             makeTargetSpec
               moduleCfg
               localVars
               lnameEnv
-              lhModuleLogicMap
+              lmap'
               targetSrc
               bareSpec
               dependencies