cleanup; add tests and docs

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)

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

@@ -544,18 +544,18 @@ processModule LiquidHaskellContext{..} = do
     tcg <- getGblEnv
     let localVars = Resolve.makeLocalVars preNormalizedCore
         -- add defines from dependencies to the logical map
-        depsLogicMap =
+        logicMapWithDeps =
           foldr (\ls lmp ->
                      lmp <> mkLogicMap (HM.map (fmap LH.lhNameToResolvedSymbol) $ liftedDefines ls))
-                mempty $
+                lhModuleLogicMap $
             (HM.elems . getDependencies) dependencies
         eBareSpec = resolveLHNames
           moduleCfg
           thisModule
           localVars
           (imp_mods $ tcg_imports tcg)
           (tcg_rdr_env tcg)
-          (lhModuleLogicMap <> depsLogicMap)
+          logicMapWithDeps
           bareSpec0
           dependencies
     result <-

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

@@ -157,10 +157,12 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
               let (inScopeEnv, logicNameEnv0, privateReflectNames, unhandledNames) =
                     makeLogicEnvs impMods thisModule sp2 dependencies
               -- Add resolved local defines to the logic map
-                  lmap1 = lmap <> mkLogicMap (HM.fromList $ (\(k , v) ->
-                                                                let k' = lhNameToResolvedSymbol <$> k in
-                                                                (F.val k', (val <$> v) { lmVar = k' }))
-                                                            <$> defines sp2)
+                  lmap1 =
+                    lmap <> mkLogicMap (HM.fromList $
+                                         (\(k , v) ->
+                                             let k' = lhNameToResolvedSymbol <$> k in
+                                             (F.val k', (val <$> v) { lmVar = k' }))
+                                         <$> defines sp2)
               sp3 <- fromBareSpecLHName <$>
                        resolveLogicNames
                          cfg
@@ -175,7 +177,9 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
                          sp2
               return (sp3, logicNameEnv0, lmap1)
             else
-              return (error "resolveLHNames: invalid spec", error "resolveLHNames: invalid logic environment" , error "resolveLHNames: invalid logic map")
+              return ( error "resolveLHNames: invalid spec"
+                     , error "resolveLHNames: invalid logic environment"
+                     , error "resolveLHNames: invalid logic map")
         logicNameEnv' = extendLogicNameEnv logicNameEnv ns
     if null es then
       Right (bs, logicNameEnv', lmap2)
@@ -192,30 +196,30 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
 
     resolveLHName lname =
       case val lname of
-      LHNUnresolved LHTcName s
-        | isTuple s ->
-          pure $ LHNResolved (LHRGHC $ GHC.tupleTyConName GHC.BoxedTuple (tupleArity s)) s
-        | isList s ->
-          pure $ LHNResolved (LHRGHC GHC.listTyConName) s
-        | s == "*" ->
-          pure $ LHNResolved (LHRGHC GHC.liftedTypeKindTyConName) s
-        | otherwise ->
-          case HM.lookup s taliases of
-            Just (m, _) -> pure $ LHNResolved (LHRLogic $ LogicName s m Nothing) s
-            Nothing -> lookupGRELHName LHTcName lname s listToMaybe
-      LHNUnresolved ns@(LHVarName lcl) s
-        | isDataCon s ->
-            lookupGRELHName (LHDataConName lcl) lname s listToMaybe
-        | otherwise ->
-            lookupGRELHName ns lname s
-              (fmap (either id GHC.getName) . Resolve.lookupLocalVar localVars (atLoc lname s))
-      LHNUnresolved LHLogicNameBinder s ->
-        pure $ makeLogicLHName s thisModule Nothing
-      n@(LHNUnresolved LHLogicName _) ->
-        -- This one will be resolved by resolveLogicNames
-        pure n
-      LHNUnresolved ns s -> lookupGRELHName ns lname s listToMaybe
-      n -> pure n
+        LHNUnresolved LHTcName s
+          | isTuple s ->
+            pure $ LHNResolved (LHRGHC $ GHC.tupleTyConName GHC.BoxedTuple (tupleArity s)) s
+          | isList s ->
+            pure $ LHNResolved (LHRGHC GHC.listTyConName) s
+          | s == "*" ->
+            pure $ LHNResolved (LHRGHC GHC.liftedTypeKindTyConName) s
+          | otherwise ->
+            case HM.lookup s taliases of
+              Just (m, _) -> pure $ LHNResolved (LHRLogic $ LogicName s m Nothing) s
+              Nothing -> lookupGRELHName LHTcName lname s listToMaybe
+        LHNUnresolved ns@(LHVarName lcl) s
+          | isDataCon s ->
+              lookupGRELHName (LHDataConName lcl) lname s listToMaybe
+          | otherwise ->
+              lookupGRELHName ns lname s
+                (fmap (either id GHC.getName) . Resolve.lookupLocalVar localVars (atLoc lname s))
+        LHNUnresolved LHLogicNameBinder s ->
+          pure $ makeLogicLHName s thisModule Nothing
+        n@(LHNUnresolved LHLogicName _) ->
+          -- This one will be resolved by resolveLogicNames
+          pure n
+        LHNUnresolved ns s -> lookupGRELHName ns lname s listToMaybe
+        n -> pure n
 
     lookupGRELHName ns lname s localNameLookup =
       case maybeDropImported ns $ GHC.lookupGRE globalRdrEnv (mkLookupGRE ns s) of

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

@@ -931,7 +931,7 @@ data BPspec
   | Varia   (Located LHName, [Variance])                  -- ^ 'variance' annotations, marking type constructor params as co-, contra-, or in-variant
   | DSize   ([LocBareTypeParsed], LocSymbol)              -- ^ 'data size' annotations, generating fancy termination metric
   | BFix    ()                                            -- ^ fixity annotation
-  | Define  (Located LHName, ([Symbol], ExprV LocSymbol))              -- ^ 'define' annotation for specifying logic aliases
+  | Define  (Located LHName, ([Symbol], ExprV LocSymbol)) -- ^ 'define' annotation for specifying logic aliases
   deriving (Data, Typeable)
 
 instance PPrint BPspec where

tests/benchmarks/popl18/ple/pos/Unification.hs

@@ -26,7 +26,6 @@ data P a b = P a b
 -- | If unification succeeds then the returned substitution makes input terms equal
 -- | Unification may fail with Nothing, or diverge
 
--- TODO try before apply PR
 {-@ lazy unify @-}
 {-@ unify :: t1:Term -> t2:Term
           -> Maybe {θ:Substitution | apply θ t1 == apply θ t2 } @-}

tests/neg/MyBag.hs

@@ -0,0 +1,14 @@
+module MyBag where
+
+import qualified Data.Map as M
+
+{-@ embed Bag as Bag_t @-}
+data Bag a = Bag { toMap :: M.Map a Int } deriving Eq
+
+{-@ assume empty :: {v:Bag k | v = Bag_empty 0} @-}
+empty :: Bag k
+empty = Bag M.empty
+
+{-@ assume sng :: (Ord k) => k:k -> {v:Bag k | v = Bag_sng k 1} @-}
+sng :: (Ord k) => k -> Bag k
+sng k = Bag (M.singleton k 1)

tests/neg/MyBagDefine.hs

@@ -0,0 +1,16 @@
+{-@ LIQUID "--expect-any-error" @-}
+module MyBagDefine where
+
+import MyBag
+import Data.Set
+
+{-@ define empty = (Bag_empty 0) @-}
+{-@ define sng k = (Bag_sng k 1) @-}
+
+{-@ thm_emp :: x:k -> { empty /= sng x } @-}
+thm_emp :: (Ord k) => k -> ()
+thm_emp x = const () (sng x)
+
+{-@ thm_emp' :: x:k -> xs:Bag k -> { empty /= put x xs } @-}
+thm_emp' :: (Ord k) => k -> Bag k -> ()
+thm_emp' x xs = const () (put x xs)

tests/ple/pos/Isort_erase.hs

@@ -1,7 +1,22 @@
 {-@ LIQUID "--reflection" @-}
 {-@ LIQUID "--ple"        @-}
 
-module Isort_erase where 
+{-
+This test relies on `withProof` being logically aliased to identity on the
+first argument, as `define`d in Language.Haskell.Liquid.ProofCombinators.
+Without this alias in scope, it will fail with the following error:
+
+    Liquid Type Mismatch
+
+    The inferred type
+      VV : {v : GHC.Types.Bool | Isort_erase.isSorted (Isort_erase.Cons y1 (Isort_erase.insert x ys))
+                                 && v == Isort_erase.lem_ins y1 x ys}
+
+    is not a subtype of the required type
+      VV : {VV : GHC.Types.Bool | Isort_erase.isSorted (Isort_erase.Cons y (Isort_erase.insert x ?a))}
+-}
+
+module Isort_erase where
 
 import Prelude hiding (id, sum)
 import Language.Haskell.Liquid.ProofCombinators
@@ -21,11 +36,11 @@ isSorted (Cons x xs) =
 
 {-@ reflect insert @-}
 {-@ insert :: x:Int -> {xs:List | isSorted xs} -> {xs:List | isSorted xs} @-}
-insert :: Int -> List -> List 
+insert :: Int -> List -> List
 insert x Emp     = Cons x Emp
 insert x (Cons y ys)
   | x <= y        = Cons x (Cons y ys)
-  | otherwise     = (Cons y (insert x ys)) `withProof` (lem_ins y x ys) 
+  | otherwise     = (Cons y (insert x ys)) `withProof` (lem_ins y x ys)
 
 {-@ lem_ins :: y:Int -> {x:Int | y < x} -> {ys:List | isSorted (Cons y ys)} -> {isSorted (Cons y (insert x ys))} @-}
 lem_ins :: Int -> Int -> List -> Bool

tests/pos/MyBag.hs

@@ -0,0 +1,14 @@
+module MyBag where
+
+import qualified Data.Map as M
+
+{-@ embed Bag as Bag_t @-}
+data Bag a = Bag { toMap :: M.Map a Int } deriving Eq
+
+{-@ assume empty :: {v:Bag k | v = Bag_empty 0} @-}
+empty :: Bag k
+empty = Bag M.empty
+
+{-@ assume sng :: (Ord k) => k:k -> {v:Bag k | v = Bag_sng k 1} @-}
+sng :: (Ord k) => k -> Bag k
+sng k = Bag (M.singleton k 1)

tests/pos/MyBagDefine.hs

@@ -0,0 +1,12 @@
+module MyBagDefine where
+
+import MyBag as B
+import Data.Set
+
+{- dropping the qualification will trigger the "Ambiguous specification symbol" error -}
+{-@ define B.empty = (Bag_empty 0) @-}
+{-@ define sng k = (Bag_sng k 1) @-}
+
+{-@ thm_emp :: x:k -> { B.empty /= sng x } @-}
+thm_emp :: (Ord k) => k -> ()
+thm_emp x = const () (sng x)

tests/pos/NumRefl1.hs

@@ -0,0 +1,12 @@
+module NumRefl1 where
+
+{-
+The `define` should be propagated from NumRefl, otherwise the test fails
+with the same error.
+-}
+import NumRefl
+
+{-@ reflect toNum1 @-}
+toNum1 :: Num p => () -> p
+toNum1 _ = -2
+

tests/tests.cabal

@@ -1269,6 +1269,8 @@ executable unit-neg
                     , MultiParamTypeClasses
                     , MultipleInvariants
                     , Multi_pred_app_00
+                    , MyBag
+                    , MyBagDefine
                     , NameResolution
                     , NestedRecursion
                     , NoExhaustiveGuardsError
@@ -1862,7 +1864,10 @@ executable unit-pos-3
       buildable:      False
 
     other-modules:
-                      NumRefl
+                      MyBag
+                    , MyBagDefine
+                    , NumRefl
+                    , NumRefl1
                     , Streams
                     , StrictPair0
                     , StrictPair1