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/liquidhaskell-boot.cabal

@@ -61,7 +61,6 @@ library
                       Liquid.GHC.API.Compat
                       Liquid.GHC.API.Extra
                       Liquid.GHC.API.StableModule
-                      Language.Haskell.Liquid.GHC.CoreToLogic
                       Language.Haskell.Liquid.GHC.Interface
                       Language.Haskell.Liquid.GHC.Logging
                       Language.Haskell.Liquid.GHC.Misc

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/Interface.hs

@@ -26,7 +26,7 @@ module Language.Haskell.Liquid.GHC.Interface (
 
   -- * Internal exports (provisional)
   , extractSpecComments
-  , makeLogicMap
+  , listLMap
   , classCons
   , derivedVars
   , importVars
@@ -63,18 +63,14 @@ import Data.Maybe
 
 import qualified Data.HashSet        as S
 
-import System.IO
-import Text.Megaparsec.Error
 import Text.PrettyPrint.HughesPJ        hiding (first, (<>))
 import Language.Fixpoint.Types          hiding (err, panic, Error, Result, Expr)
 import qualified Language.Fixpoint.Misc as Misc
-import qualified Language.Haskell.Liquid.GHC.CoreToLogic as CoreToLogic
 import Language.Haskell.Liquid.GHC.Misc
 import Language.Haskell.Liquid.GHC.Types (MGIModGuts(..))
 import Language.Haskell.Liquid.GHC.Play
 import Language.Haskell.Liquid.WiredIn (isDerivedInstance)
 import qualified Language.Haskell.Liquid.Measure  as Ms
-import Language.Haskell.Liquid.Parse
 import Language.Haskell.Liquid.Types.Errors
 import Language.Haskell.Liquid.Types.PrettyPrint
 import Language.Haskell.Liquid.Types.Specs
@@ -260,22 +256,13 @@ extractSpecComment (Ghc.L sp (ApiBlockComment txt))
 
 extractSpecComment _ = Nothing
 
-
 --------------------------------------------------------------------------------
--- Assemble Information for Spec Extraction ------------------------------------
+-- Information for Spec Extraction ---------------------------------------------
 --------------------------------------------------------------------------------
 
-makeLogicMap :: IO LogicMap
-makeLogicMap = do
-  case parseSymbolToLogic "CoreToLogic.coreToLogic" CoreToLogic.coreToLogic of
-    Left peb -> do
-      hPutStrLn stderr (errorBundlePretty peb)
-      panic Nothing "makeLogicMap failed"
-    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"