From 06f5a41da2a9fcbb63489d164b6e704bfe4142e6 Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Tue, 3 Dec 2024 14:15:47 +0100
Subject: [PATCH 01/15] parser + map construction for local defines

---
 .../src/Language/Haskell/Liquid/Bag.hs        | 10 ++-
 .../Haskell/Liquid/GHC/CoreToLogic.hs         | 66 +++++++++----------
 .../src/Language/Haskell/Liquid/GHC/Plugin.hs |  3 +-
 .../src/Language/Haskell/Liquid/Parse.hs      | 23 +++++--
 4 files changed, 58 insertions(+), 44 deletions(-)

diff --git a/liquid-prelude/src/Language/Haskell/Liquid/Bag.hs b/liquid-prelude/src/Language/Haskell/Liquid/Bag.hs
index d55d1bc9e6..c0d33d45bf 100644
--- a/liquid-prelude/src/Language/Haskell/Liquid/Bag.hs
+++ b/liquid-prelude/src/Language/Haskell/Liquid/Bag.hs
@@ -26,15 +26,17 @@ 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 Language.Haskell.Liquid.Bag.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 Language.Haskell.Liquid.Bag.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 Language.Haskell.Liquid.Bag.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))
 
@@ -44,18 +46,22 @@ 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} @-}
+{-@ define Language.Haskell.Liquid.Bag.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} @-}
+{-@ define Language.Haskell.Liquid.Bag.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} @-}
+{-@ define Language.Haskell.Liquid.Bag.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} @-}
+{-@ 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)
 
@@ -63,7 +69,7 @@ sub b1 b2 = M.isSubmapOfBy (<=) (toMap b1) (toMap b2)
 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 -> { Language.Haskell.Liquid.Bag.empty /= Language.Haskell.Liquid.Bag.put x xs } @-}
 thm_emp :: (Ord k) => k -> Bag k -> ()
 thm_emp x xs = const () (get x xs)
 
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
index 3bf9cb4d8b..6158b14712 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
@@ -2,7 +2,31 @@ 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.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 GHC.CString.unpackCString# x = x"
+  , ""
+  , "define Data.RString.RString.stringEmp = (stringEmp)"
+  , "define String.stringEmp  = (stringEmp)"
+  , "define Main.mempty       = (mempty)"
+  , ""
+  , "define Control.Parallel.Strategies.withStrategy s x = (x)"
+  , ""
+  , "define Language.Haskell.Liquid.String.stringEmp = (stringEmp)"
+  , "define Language.Haskell.Liquid.Equational.eq x y = (y)"
+  , "define Language.Haskell.Liquid.ProofCombinators.withProof x y = (x)"
+  , "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,36 +45,12 @@ 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      = (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 Language.Haskell.Liquid.String.stringEmp = (stringEmp)"
-  , "define Data.RString.RString.stringEmp = (stringEmp)"
-  , "define String.stringEmp  = (stringEmp)"
-  , "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.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)"
   ]
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
index 7ae5441637..53ac994d24 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
@@ -288,7 +288,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)
@@ -384,7 +383,7 @@ processInputSpec cfg pipelineData modSummary inputSpec = do
   let lhContext = LiquidHaskellContext {
         lhGlobalCfg       = cfg
       , lhInputSpec       = inputSpec
-      , lhModuleLogicMap  = logicMap
+      , lhModuleLogicMap  = logicMap <> toLogicMap [ d | Define d <- pdSpecComments pipelineData ]
       , lhModuleSummary   = modSummary
       , lhModuleTcData    = pdTcData pipelineData
       , lhModuleGuts      = pdUnoptimisedCore pipelineData
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
index 2e61a5afa2..10d5a687bd 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
@@ -190,13 +190,13 @@ toLogicP :: Parser LogicMap
 toLogicP
   = toLogicMap <$> many toLogicOneP
 
-toLogicOneP :: Parser  (LocSymbol, [Symbol], Expr)
+toLogicOneP :: Parser (LocSymbol, [Symbol], Expr)
 toLogicOneP
   = do reserved "define"
        (x:xs) <- some locSymbolP
        reservedOp "="
        e      <- exprP <|> predP
-       return (x, val <$> xs, fmap val e)
+       return (x, val <$> xs, val <$> e)
 
 
 --------------------------------------------------------------------------------
@@ -930,7 +930,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  (LocSymbol, Symbol)                           -- ^ 'define' annotation for specifying aliases c.f. `include-CoreToLogic.lg`
+  | Define  (LocSymbol, [Symbol], Expr)                   -- ^ 'define' annotation for specifying logic aliases
   deriving (Data, Typeable)
 
 instance PPrint BPspec where
@@ -1020,7 +1020,7 @@ ppPspec _ (Pragma  (Loc _ _ s))
 ppPspec k (CMeas   m)
   = "class measure" <+> pprintTidy k (unLocMeasureV m)
 ppPspec k (IMeas   m)
-  = "instance  measure" <+> pprintTidy k (val <$> unLocMeasureV m)
+  = "instance measure" <+> pprintTidy k (val <$> unLocMeasureV m)
 ppPspec k (Class   cls)
   = pprintTidy k $ fmap (fmap parsedToBareType) cls
 ppPspec k (RInst   inst)
@@ -1031,8 +1031,8 @@ ppPspec k (DSize   (ds, ss))
   = "data size" <+> splice " " (pprintTidy k <$> map (fmap parsedToBareType) ds) <+> pprintTidy k (val ss)
 ppPspec _ (BFix    _)           --
   = "fixity"
-ppPspec k (Define  (lx, y))
-  = "define" <+> pprintTidy k (val lx) <+> "=" <+> pprintTidy k y
+ppPspec k (Define  (lx, ys , e))
+  = "define" <+> pprintTidy k (val lx) <+> " " <+> pprintTidy k ys <+> "=" <+> pprintTidy k e
 ppPspec k (Relational (lxl, lxr, tl, tr, q, p))
   = "relational"
         <+> pprintTidy k (val lxl) <+> "::" <+> pprintTidy k (parsedToBareType <$> tl) <+> "~"
@@ -1149,7 +1149,8 @@ specP
     <|> (reserved "private-reflect" >> fmap PrivateReflect axiomP  )
     <|> (reserved "opaque-reflect" >> fmap OpaqueReflect locBinderLHNameP  )
 
-    <|> fallbackSpecP "measure"    hmeasureP
+    <|> fallbackSpecP "define"  logDefineP
+    <|> fallbackSpecP "measure" hmeasureP
 
     <|> (reserved "infixl"        >> fmap BFix    infixlP  )
     <|> (reserved "infixr"        >> fmap BFix    infixrP  )
@@ -1322,6 +1323,14 @@ rtAliasP f bodyP
        let (tArgs, vArgs) = partition (isSmall . headSym) args
        return $ Loc pos posE (RTA name (f <$> tArgs) vArgs body)
 
+logDefineP :: Parser BPspec
+logDefineP =
+    do s <- locBinderP
+       args <- many locSymbolP
+       reservedOp "="
+       e <- exprP <|> predP
+       return (Define (s, val <$> args, val <$> e))
+
 hmeasureP :: Parser BPspec
 hmeasureP = do
   setLayout

From 30fd1b87ac716322fe6fcdd8331ba5161622b00b Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Wed, 4 Dec 2024 16:14:27 +0100
Subject: [PATCH 02/15] move defines to NumRefl

---
 .../src/Language/Haskell/Liquid/Bag.hs        | 28 +++++++++----------
 .../Haskell/Liquid/GHC/CoreToLogic.hs         | 10 +++++--
 tests/pos/NumRefl.hs                          |  9 ++++--
 3 files changed, 27 insertions(+), 20 deletions(-)

diff --git a/liquid-prelude/src/Language/Haskell/Liquid/Bag.hs b/liquid-prelude/src/Language/Haskell/Liquid/Bag.hs
index c0d33d45bf..569b878ac3 100644
--- a/liquid-prelude/src/Language/Haskell/Liquid/Bag.hs
+++ b/liquid-prelude/src/Language/Haskell/Liquid/Bag.hs
@@ -25,18 +25,18 @@ import qualified Data.Map      as M
 -- https://github.com/ucsd-progsys/liquidhaskell/issues/2332
 data Bag a = Bag { toMap :: M.Map a Int } deriving Eq
 
-{-@ assume empty :: {v:Bag k | v = Bag_empty 0} @-}
-{-@ define Language.Haskell.Liquid.Bag.empty        = (Bag_empty 0) @-}
+{-@ assume empty :: {v:Bag k | v              = Bag_empty 0} @-}
+{-@ define Language.Haskell.Liquid.Bag.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 Language.Haskell.Liquid.Bag.get k b      = (Bag_count b k) @-}
+{-@ assume get :: (Ord k) =>               k:k -> b:Bag k -> {v:Nat | v = Bag_count b k}  @-}
+{-@ define Language.Haskell.Liquid.Bag.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)} @-}
-{-@ define Language.Haskell.Liquid.Bag.put k b      = (Bag_union b (Bag_sng k 1)) @-}
+{-@ assume put :: (Ord k) =>               k:k -> b:Bag k -> {v:Bag k | v = Bag_union b (Bag_sng k 1)} @-}
+{-@ define Language.Haskell.Liquid.Bag.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))
 
@@ -45,23 +45,23 @@ 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} @-}
-{-@ define Language.Haskell.Liquid.Bag.union a b    = (Bag_union a b) @-}
+{-@ assume union :: (Ord k) =>               a:Bag k -> b:Bag k -> {v:Bag k | v = Bag_union a b} @-}
+{-@ define Language.Haskell.Liquid.Bag.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} @-}
-{-@ define Language.Haskell.Liquid.Bag.unionMax a b = (Bag_union_max a b) @-}
+{-@ assume unionMax :: (Ord k) =>               a:Bag k -> b:Bag k -> {v:Bag k | v = Bag_union_max a b} @-}
+{-@ define Language.Haskell.Liquid.Bag.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} @-}
-{-@ define Language.Haskell.Liquid.Bag.interMin a b = (Bag_inter_min a b) @-}
+{-@ assume interMin :: (Ord k) =>               a:Bag k -> b:Bag k -> {v:Bag k | v = Bag_inter_min a b} @-}
+{-@ define Language.Haskell.Liquid.Bag.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} @-}
-{-@ define sub a b      = (Bag_sub a b) @-}
+{-@ assume sub :: (Ord k) =>               a:Bag k -> b:Bag k -> {v:Bool | v = Bag_sub a b} @-}
+{-@ define Language.Haskell.Liquid.Bag.sub a          b                     = (Bag_sub a b) @-}
 sub :: (Ord k) => Bag k -> Bag k -> Bool
 sub b1 b2 = M.isSubmapOfBy (<=) (toMap b1) (toMap b2)
 
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
index 6158b14712..3c71fcebde 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
@@ -6,8 +6,10 @@ coreToLogic = unlines
   , "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.Internal.Num.fromInteger x   = (x)"
-  , "define GHC.Num.Integer.IS x             = (x)"
+
+--  , "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)"
   , ""
@@ -21,7 +23,9 @@ coreToLogic = unlines
   , ""
   , "define Language.Haskell.Liquid.String.stringEmp = (stringEmp)"
   , "define Language.Haskell.Liquid.Equational.eq x y = (y)"
-  , "define Language.Haskell.Liquid.ProofCombinators.withProof x y = (x)"
+
+  --, "define Language.Haskell.Liquid.ProofCombinators.withProof x y = (x)"
+
   , "define Language.Haskell.Liquid.ProofCombinators.cast x y = (y)"
   , "define Liquid.ProofCombinators.cast x y = (y)"
   , "define ProofCombinators.cast x y = (y)"
diff --git a/tests/pos/NumRefl.hs b/tests/pos/NumRefl.hs
index 8ec0ace895..9f20c3e087 100644
--- a/tests/pos/NumRefl.hs
+++ b/tests/pos/NumRefl.hs
@@ -1,10 +1,10 @@
 {-
 
-Without the 
+Without the
   define GHC.Internal.Num.fromInteger x = (x)
-  define GHC.Num.Integer.IS             = (x)
+  define GHC.Num.Integer.IS x           = (x)
 
-this program crashes with: 
+this program crashes with:
 
     Illegal type specification for `NumRefl.toNum`
     NumRefl.toNum :: forall p .
@@ -20,6 +20,9 @@ Because the resule type (Num p) => p cannot be decided to be a numeric type.
 
 module NumRefl where
 
+{-@ define GHC.Internal.Num.fromInteger x = (x) @-}
+{-@ define GHC.Num.Integer.IS x           = (x) @-}
+
 {-@ reflect toNum @-}
 toNum :: Num p => () -> p
 toNum _ = -1

From a92858b859c4fbd29c7ac21702ccef2fa09bf4f6 Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Tue, 10 Dec 2024 20:57:17 +0100
Subject: [PATCH 03/15] WIP qualify and export defines

---
 .../src/Language/Haskell/Liquid/Bag.hs        | 40 ++++-----
 .../Haskell/Liquid/ProofCombinators.hs        | 29 +++---
 .../Haskell/Liquid/GHC/CoreToLogic.hs         |  2 +-
 .../Language/Haskell/Liquid/GHC/Interface.hs  |  4 +-
 .../src/Language/Haskell/Liquid/GHC/Plugin.hs | 20 +++--
 .../Haskell/Liquid/LHNameResolution.hs        |  2 +
 .../src/Language/Haskell/Liquid/Parse.hs      |  9 +-
 .../Language/Haskell/Liquid/Types/Names.hs    |  3 +-
 .../Language/Haskell/Liquid/Types/Specs.hs    | 10 +++
 .../Language/Haskell/Liquid/Types/Types.hs    | 89 ++++++++++++-------
 tests/pos/WithProofRefl.hs                    | 13 +++
 tests/tests.cabal                             |  1 +
 12 files changed, 143 insertions(+), 79 deletions(-)
 create mode 100644 tests/pos/WithProofRefl.hs

diff --git a/liquid-prelude/src/Language/Haskell/Liquid/Bag.hs b/liquid-prelude/src/Language/Haskell/Liquid/Bag.hs
index 569b878ac3..6f4b648045 100644
--- a/liquid-prelude/src/Language/Haskell/Liquid/Bag.hs
+++ b/liquid-prelude/src/Language/Haskell/Liquid/Bag.hs
@@ -25,51 +25,51 @@ import qualified Data.Map      as M
 -- https://github.com/ucsd-progsys/liquidhaskell/issues/2332
 data Bag a = Bag { toMap :: M.Map a Int } deriving Eq
 
-{-@ assume empty :: {v:Bag k | v              = Bag_empty 0} @-}
-{-@ define Language.Haskell.Liquid.Bag.empty = (Bag_empty 0) @-}
+{-@ 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 Language.Haskell.Liquid.Bag.get k      b                    = (Bag_count b k) @-}
+{-@ 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)} @-}
-{-@ define Language.Haskell.Liquid.Bag.put k      b                      = (Bag_union b (Bag_sng k 1)) @-}
+{-@ assume put :: (Ord k) => k:k -> b:Bag k -> {v:Bag k | v = Bag_union b (Bag_sng k 1)} @-}
+{-@ 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) =>               a:Bag k -> b:Bag k -> {v:Bag k | v = Bag_union a b} @-}
-{-@ define Language.Haskell.Liquid.Bag.union a          b                      = (Bag_union a b) @-}
+{-@ 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) =>               a:Bag k -> b:Bag k -> {v:Bag k | v = Bag_union_max a b} @-}
-{-@ define Language.Haskell.Liquid.Bag.unionMax a          b                      = (Bag_union_max a b) @-}
+{-@ 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) =>               a:Bag k -> b:Bag k -> {v:Bag k | v = Bag_inter_min a b} @-}
-{-@ define Language.Haskell.Liquid.Bag.interMin a          b                      = (Bag_inter_min a b) @-}
+{-@ 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) =>               a:Bag k -> b:Bag k -> {v:Bool | v = Bag_sub a b} @-}
-{-@ define Language.Haskell.Liquid.Bag.sub a          b                     = (Bag_sub a b) @-}
+{-@ 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 /= Language.Haskell.Liquid.Bag.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)
 
diff --git a/liquid-prelude/src/Language/Haskell/Liquid/ProofCombinators.hs b/liquid-prelude/src/Language/Haskell/Liquid/ProofCombinators.hs
index 9faf8d6147..7774cdd238 100644
--- a/liquid-prelude/src/Language/Haskell/Liquid/ProofCombinators.hs
+++ b/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           @-}
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
index 3c71fcebde..a5dc36203a 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
@@ -24,7 +24,7 @@ coreToLogic = unlines
   , "define Language.Haskell.Liquid.String.stringEmp = (stringEmp)"
   , "define Language.Haskell.Liquid.Equational.eq x y = (y)"
 
-  --, "define Language.Haskell.Liquid.ProofCombinators.withProof x y = (x)"
+  -- , "define Language.Haskell.Liquid.ProofCombinators.withProof x y = (x)"
 
   , "define Language.Haskell.Liquid.ProofCombinators.cast x y = (y)"
   , "define Liquid.ProofCombinators.cast x y = (y)"
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs
index 9c4d82b370..67c7e2fc45 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs
+++ b/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"
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
index 53ac994d24..2f1720d8ee 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
@@ -19,11 +19,13 @@ 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.Fixpoint.Types.Refinements     as F
+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
@@ -378,12 +380,10 @@ processInputSpec cfg pipelineData modSummary inputSpec = do
 
   logicMap :: LogicMap <- liftIO LH.makeLogicMap
 
-  -- debugLog $ "Logic map:\n" ++ show logicMap
-
   let lhContext = LiquidHaskellContext {
         lhGlobalCfg       = cfg
       , lhInputSpec       = inputSpec
-      , lhModuleLogicMap  = logicMap <> toLogicMap [ d | Define d <- pdSpecComments pipelineData ]
+      , lhModuleLogicMap  = logicMap -- <> toLogicMap defines
       , lhModuleSummary   = modSummary
       , lhModuleTcData    = pdTcData pipelineData
       , lhModuleGuts      = pdUnoptimisedCore pipelineData
@@ -544,14 +544,20 @@ processModule LiquidHaskellContext{..} = do
 
     tcg <- getGblEnv
     let localVars = Resolve.makeLocalVars preNormalizedCore
+        modsym = symbol $ GHC.moduleName thisModule
+        -- we do this here because we 1) have the module name 2) process dependencies here
+        defs = map (\(ls , ae) -> (LH.qualifySymbol modsym <$> ls , ae)) $ defines bareSpec0
+        localLogicMap = toLogicMap defs
+        depsLogicMap = foldr (\h l -> l <> mempty {lmSymDefs = h}) mempty (liftedDefines <$> (HM.elems . getDependencies) dependencies)
+        lm = lhModuleLogicMap <> depsLogicMap <> localLogicMap
         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
@@ -562,7 +568,7 @@ processModule LiquidHaskellContext{..} = do
               moduleCfg
               localVars
               lnameEnv
-              lhModuleLogicMap
+              lm
               targetSrc
               bareSpec
               dependencies
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
index d8df06e96c..f45e586294 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
@@ -91,6 +91,8 @@ import           Language.Haskell.Liquid.WiredIn
 import qualified Text.PrettyPrint.HughesPJ as PJ
 import qualified Text.Printf               as Printf
 
+-- import Debug.Trace (trace)
+
 -- | Collects type aliases from the current module and its dependencies.
 --
 -- It doesn't matter at the moment in which module a type alias is defined.
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
index 10d5a687bd..5099c79a33 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
@@ -190,13 +190,13 @@ toLogicP :: Parser LogicMap
 toLogicP
   = toLogicMap <$> many toLogicOneP
 
-toLogicOneP :: Parser (LocSymbol, [Symbol], Expr)
+toLogicOneP :: Parser (LocSymbol, ([Symbol], Expr))
 toLogicOneP
   = do reserved "define"
        (x:xs) <- some locSymbolP
        reservedOp "="
        e      <- exprP <|> predP
-       return (x, val <$> xs, val <$> e)
+       return (x, (val <$> xs, val <$> e))
 
 
 --------------------------------------------------------------------------------
@@ -930,7 +930,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  (LocSymbol, [Symbol], Expr)                   -- ^ 'define' annotation for specifying logic aliases
+  | Define  (LocSymbol, [Symbol], Expr)              -- ^ 'define' annotation for specifying logic aliases
   deriving (Data, Typeable)
 
 instance PPrint BPspec where
@@ -1132,6 +1132,7 @@ mkSpec xs = Measure.Spec
   , Measure.ignores    = S.fromList [s | Ignore s <- xs]
   , Measure.autosize   = S.fromList [s | ASize  s <- xs]
   , Measure.axeqs      = []
+  , Measure.defines    = [ (x , (as , e)) | Define (x , as , e) <- xs]
   }
 
 -- | Parse a single top level liquid specification
@@ -1325,7 +1326,7 @@ rtAliasP f bodyP
 
 logDefineP :: Parser BPspec
 logDefineP =
-    do s <- locBinderP
+    do s <- locBinderP -- locBinderLHNameP
        args <- many locSymbolP
        reservedOp "="
        e <- exprP <|> predP
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
index f28da72137..2aff6740cd 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
@@ -44,6 +44,7 @@ import Language.Fixpoint.Types
 import Language.Haskell.Liquid.GHC.Misc (locNamedThing) -- Symbolic GHC.Name
 import qualified Liquid.GHC.API as GHC
 import Text.PrettyPrint.HughesPJ.Compat
+-- import qualified GHC.Plugins as GHC
 
 -- RJ: Please add docs
 lenLocSymbol :: Located Symbol
@@ -228,7 +229,7 @@ getLHNameSymbol :: LHName -> Symbol
 getLHNameSymbol (LHNResolved _ s) = s
 getLHNameSymbol (LHNUnresolved _ s) = s
 
--- | Get the unresolved Symbol from an LHName.
+-- | Get the resolved data from an LHName.
 getLHNameResolved :: HasCallStack => LHName -> LHResolvedName
 getLHNameResolved (LHNResolved n _) = n
 getLHNameResolved n@LHNUnresolved{} = error $ "getLHNameResolved: unresolved name: " ++ show n
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
index 75ee6b7808..aadc64e08d 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
@@ -421,6 +421,7 @@ data Spec lname ty = Spec
   , dsize      :: ![([F.Located ty], F.LocSymbol)]                    -- ^ Size measure to enforce fancy termination
   , bounds     :: !(RRBEnvV lname (F.Located ty))
   , axeqs      :: ![F.EquationV lname]                                -- ^ Equalities used for Proof-By-Evaluation
+  , defines    :: ![(F.LocSymbol, ([F.Symbol], F.Expr))]              -- ^ Logic aliases
   } deriving (Data, Generic)
 
 instance (Show lname, F.PPrint lname, Show ty, F.PPrint ty, F.PPrint (RTypeV lname BTyCon BTyVar (RReftV lname))) => F.PPrint (Spec lname ty) where
@@ -487,6 +488,7 @@ emapSpecM bscp lenv vf f sp = do
         (traverse (emapBoundM (traverse . f) (\e -> emapExprVM (vf . (++ e)))))
         (M.toList $ bounds sp)
     axeqs <- mapM (emapEquationM vf) $ axeqs sp
+--    defines <- mapM (emapEquationM vf) $ defines sp
     return sp
       { measures
       , expSigs
@@ -510,6 +512,7 @@ emapSpecM bscp lenv vf f sp = do
       , dsize
       , bounds
       , axeqs
+--      , defines
       }
   where
     fnull = f []
@@ -628,6 +631,7 @@ instance Semigroup (Spec lname ty) where
            , autosize   = S.union   (autosize s1)  (autosize s2)
            , bounds     = M.union   (bounds   s1)  (bounds   s2)
            , autois     = S.union   (autois s1)      (autois s2)
+           , defines    =            defines  s1 ++ defines  s2
            }
 
 instance Monoid (Spec lname ty) where
@@ -672,6 +676,7 @@ instance Monoid (Spec lname ty) where
            , dsize      = []
            , axeqs      = []
            , bounds     = M.empty
+           , defines    = []
            }
 
 -- $liftedSpec
@@ -743,6 +748,8 @@ data LiftedSpec = LiftedSpec
   , liftedBounds     :: RRBEnvV LHName LocBareTypeLHName
   , liftedAxeqs      :: HashSet (F.EquationV LHName)
     -- ^ Equalities used for Proof-By-Evaluation
+  , liftedDefines    :: M.HashMap F.Symbol LMap
+    -- ^ Logical synonyms
   } deriving (Eq, Data, Generic)
     deriving Hashable via Generically LiftedSpec
     deriving Binary   via Generically LiftedSpec
@@ -794,6 +801,7 @@ emptyLiftedSpec = LiftedSpec
   , liftedDsize      = mempty
   , liftedBounds     = mempty
   , liftedAxeqs      = mempty
+  , liftedDefines    = mempty
   }
 
 -- $trackingDeps
@@ -958,6 +966,7 @@ toLiftedSpec a = LiftedSpec
   , liftedDsize      = dsize a
   , liftedBounds     = bounds a
   , liftedAxeqs      = S.fromList . axeqs $ a
+  , liftedDefines    = M.fromList . map toLMap . defines $ a
   }
 
 -- This is a temporary internal function that we use to convert the input dependencies into a format
@@ -1003,4 +1012,5 @@ unsafeFromLiftedSpec a = Spec
   , dsize      = liftedDsize  a
   , bounds     = liftedBounds a
   , axeqs      = S.toList . liftedAxeqs $ a
+  , defines    = map (fromLMap . snd) . M.toList . liftedDefines $ a
   }
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
index 11e13a9810..7b6cc06d6d 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DeriveDataTypeable         #-}
 {-# LANGUAGE DeriveGeneric              #-}
 {-# LANGUAGE DeriveTraversable          #-}
+{-# LANGUAGE DerivingVia                #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE MultiParamTypeClasses      #-}
 {-# LANGUAGE FlexibleInstances          #-}
@@ -8,7 +9,6 @@
 {-# LANGUAGE UndecidableInstances       #-}
 {-# LANGUAGE OverloadedStrings          #-}
 {-# LANGUAGE ConstraintKinds            #-}
-{-# LANGUAGE DerivingVia                #-}
 {-# LANGUAGE NamedFieldPuns             #-}
 {-# LANGUAGE TupleSections              #-}
 
@@ -128,7 +128,7 @@ module Language.Haskell.Liquid.Types.Types (
   , mapRTAVars
 
   -- * CoreToLogic
-  , LogicMap(..), toLogicMap, eAppWithMap, LMap(..)
+  , LogicMap(..), toLMap, fromLMap, toLogicMap, {- toLogicMapWith, -} eAppWithMap, LMap(..)
 
   -- * Refined Instances
   , RDEnv, DEnv(..), RInstance(..), RISig(..)
@@ -143,31 +143,33 @@ module Language.Haskell.Liquid.Types.Types (
   )
   where
 
-import           Liquid.GHC.API as Ghc hiding ( Expr
-                                                               , isFunTy
-                                                               , ($+$)
-                                                               , nest
-                                                               , text
-                                                               , blankLine
-                                                               , (<+>)
-                                                               , vcat
-                                                               , hsep
-                                                               , comma
-                                                               , colon
-                                                               , parens
-                                                               , empty
-                                                               , char
-                                                               , panic
-                                                               , int
-                                                               , hcat
-                                                               , showPpr
-                                                               , punctuate
-                                                               , ($$)
-                                                               , braces
-                                                               , angleBrackets
-                                                               , brackets
-                                                               )
+import           Liquid.GHC.API as Ghc hiding ( Binary
+                                              , Expr
+                                              , isFunTy
+                                              , ($+$)
+                                              , nest
+                                              , text
+                                              , blankLine
+                                              , (<+>)
+                                              , vcat
+                                              , hsep
+                                              , comma
+                                              , colon
+                                              , parens
+                                              , empty
+                                              , char
+                                              , panic
+                                              , int
+                                              , hcat
+                                              , showPpr
+                                              , punctuate
+                                              , ($$)
+                                              , braces
+                                              , angleBrackets
+                                              , brackets
+                                              )
 import           Data.String
+import           Data.Binary
 import           GHC.Generics
 import           Prelude                          hiding  (error)
 
@@ -194,6 +196,8 @@ import           Language.Haskell.Liquid.Types.Names
 import           Language.Haskell.Liquid.Types.RType
 import           Language.Haskell.Liquid.Misc
 
+-- import Debug.Trace
+
 
 -----------------------------------------------------------------------------
 -- | Information about Type Constructors
@@ -265,16 +269,41 @@ data LMap = LMap
   { lmVar  :: F.LocSymbol
   , lmArgs :: [Symbol]
   , lmExpr :: Expr
-  }
+  } deriving (Eq, Data, Generic)
+    deriving Hashable via Generically LMap
+    deriving Binary   via Generically LMap
 
 instance Show LMap where
   show (LMap x xs e) = show x ++ " " ++ show xs ++ "\t |-> \t" ++ show e
 
-toLogicMap :: [(F.LocSymbol, [Symbol], Expr)] -> LogicMap
+toLMap :: (F.LocSymbol, ([Symbol], Expr)) -> (Symbol, LMap)
+toLMap (x, (ys, e)) = (F.val x, LMap {lmVar = x, lmArgs = ys, lmExpr = e})
+
+fromLMap :: LMap -> (F.LocSymbol, ([Symbol], Expr))
+fromLMap (LMap x ys e) = (x, (ys, e))
+
+toLogicMap :: [(F.LocSymbol, ([Symbol], Expr))] -> LogicMap
 toLogicMap ls = mempty {lmSymDefs = M.fromList $ map toLMap ls}
-  where
-    toLMap (x, ys, e) = (F.val x, LMap {lmVar = x, lmArgs = ys, lmExpr = e})
 
+{-
+toLogicMapWith :: (Symbol -> Symbol) -> [(F.LocSymbol, ([Symbol], Expr))] -> LogicMap
+toLogicMapWith f ls = mempty {lmSymDefs = M.fromList $ map toLMap ls}
+  where
+    toLMap (x, (ys, e)) =
+      let x' = f <$> x in
+      (F.val x', LMap {lmVar = x', lmArgs = ys, lmExpr = e})
+-}
+{-
+defsToLogicMap :: Symbol -> M.HashMap (F.LocSymbol) ([Symbol], Expr) -> LogicMap
+defsToLogicMap modsym ls = mempty {lmSymDefs = M.fromList $ map toLMap $ M.toList ls}
+  where
+    toLMap (x, (ys, e)) =
+        let qx = qualifySymbol modsym <$> x in
+        ( F.val qx
+        , LMap { lmVar = qx
+               , lmArgs = ys
+               , lmExpr = e})
+-}
 eAppWithMap :: LogicMap -> Symbol -> [Expr] -> Expr -> Expr
 eAppWithMap lmap f es expr
   | Just (LMap _ xs e) <- M.lookup f (lmSymDefs lmap)
diff --git a/tests/pos/WithProofRefl.hs b/tests/pos/WithProofRefl.hs
new file mode 100644
index 0000000000..69084fee6c
--- /dev/null
+++ b/tests/pos/WithProofRefl.hs
@@ -0,0 +1,13 @@
+{-@ LIQUID "--save" @-}
+module WithProofRefl where
+
+import Language.Haskell.Liquid.ProofCombinators
+
+{-@ reflect unify' @-}
+unify' :: Int -> Int
+unify' 0 = 42
+unify' i = (i-1) `withProof` theoremUnify' i
+
+theoremUnify' :: Int -> Proof
+theoremUnify' i = ()
+-- theoremUnify' i = theoremUnify' (i-1)
diff --git a/tests/tests.cabal b/tests/tests.cabal
index 65b6a06cc5..512a4be4ea 100644
--- a/tests/tests.cabal
+++ b/tests/tests.cabal
@@ -2014,6 +2014,7 @@ executable unit-pos-3
                     , WBL0
                     , WBL
                     , WhyLH
+                    , WithProofRefl
                     , Words1
                     , Words
                     , Wrap0

From 2d6cb4644a63759858aa5ae60fdf26331041e756 Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Tue, 10 Dec 2024 21:49:37 +0100
Subject: [PATCH 04/15] fix defines export

---
 .../src/Language/Haskell/Liquid/Bare.hs               | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
index ba5abb66e7..6d0b307646 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
@@ -64,6 +64,7 @@ import Data.Hashable (Hashable)
 import Data.Bifunctor (bimap, first)
 import Data.Function (on)
 
+-- import Debug.Trace
 
 {- $creatingTargetSpecs
 
@@ -101,13 +102,16 @@ makeTargetSpec cfg localVars lnameEnv lmap targetSrc bareSpec dependencies = do
   where
     secondPhase :: [Warning] -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
     secondPhase phaseOneWarns = do
+      --let bs' = trace ("bareDefines @" ++ show (giTargetMod targetSrc) ++ " = " ++ show (defines bareSpec)) $ bareSpec
       diagOrSpec <- makeGhcSpec cfg localVars (fromTargetSrc targetSrc) lmap bareSpec legacyDependencies
       case diagOrSpec of
         Left d -> return $ Left d
         Right (warns, ghcSpec) -> do
           let targetSpec = toTargetSpec ghcSpec
-              liftedSpec = ghcSpecToLiftedSpec ghcSpec
-          liftedSpec' <- removeUnexportedLocalAssumptions liftedSpec
+              bareSpec1 = ghcSpecToBareSpec ghcSpec
+              liftedSpec = toLiftedSpec (bareSpec1 { defines = defines bareSpec })
+              -- ls' = trace ("liftedDefines @" ++ show (giTargetMod targetSrc) ++ " = " ++ show (liftedDefines liftedSpec)) $ liftedSpec
+          liftedSpec' <- removeUnexportedLocalAssumptions liftedSpec --ls'
           return $ Right (phaseOneWarns <> warns, targetSpec, liftedSpec')
 
     toLegacyDep :: (Ghc.StableModule, LiftedSpec) -> (ModName, BareSpec)
@@ -129,7 +133,8 @@ makeTargetSpec cfg localVars lnameEnv lmap targetSrc bareSpec dependencies = do
           exportedAssumption _ = True
       return lspec { liftedAsmSigs = S.filter (exportedAssumption . val . fst) (liftedAsmSigs lspec) }
 
-    ghcSpecToLiftedSpec = toLiftedSpec . toBareSpecLHName cfg lnameEnv . _gsLSpec
+    ghcSpecToBareSpec = toBareSpecLHName cfg lnameEnv . _gsLSpec
+    --ghcSpecToLiftedSpec = toLiftedSpec . foo
 
 
 -------------------------------------------------------------------------------------

From 2a5a8dea6ee15529d1a934fb6f250270563f6dc3 Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Wed, 11 Dec 2024 10:42:34 +0100
Subject: [PATCH 05/15] cleanup

---
 .../src/Language/Haskell/Liquid/Bare.hs       |  7 +------
 .../Haskell/Liquid/GHC/CoreToLogic.hs         | 13 ------------
 .../src/Language/Haskell/Liquid/GHC/Plugin.hs | 16 +++++++-------
 .../Haskell/Liquid/LHNameResolution.hs        |  2 --
 .../src/Language/Haskell/Liquid/Parse.hs      | 10 ++++-----
 .../Language/Haskell/Liquid/Types/Names.hs    |  1 -
 .../Language/Haskell/Liquid/Types/Specs.hs    |  4 +---
 .../Language/Haskell/Liquid/Types/Types.hs    | 21 +------------------
 tests/pos/WithProofRefl.hs                    | 13 ------------
 tests/tests.cabal                             |  1 -
 10 files changed, 16 insertions(+), 72 deletions(-)
 delete mode 100644 tests/pos/WithProofRefl.hs

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
index 6d0b307646..2e9472aaaa 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
@@ -64,8 +64,6 @@ import Data.Hashable (Hashable)
 import Data.Bifunctor (bimap, first)
 import Data.Function (on)
 
--- import Debug.Trace
-
 {- $creatingTargetSpecs
 
 /Liquid Haskell/ operates on 'TargetSpec's, so this module provides a single function called
@@ -102,7 +100,6 @@ makeTargetSpec cfg localVars lnameEnv lmap targetSrc bareSpec dependencies = do
   where
     secondPhase :: [Warning] -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
     secondPhase phaseOneWarns = do
-      --let bs' = trace ("bareDefines @" ++ show (giTargetMod targetSrc) ++ " = " ++ show (defines bareSpec)) $ bareSpec
       diagOrSpec <- makeGhcSpec cfg localVars (fromTargetSrc targetSrc) lmap bareSpec legacyDependencies
       case diagOrSpec of
         Left d -> return $ Left d
@@ -110,8 +107,7 @@ makeTargetSpec cfg localVars lnameEnv lmap targetSrc bareSpec dependencies = do
           let targetSpec = toTargetSpec ghcSpec
               bareSpec1 = ghcSpecToBareSpec ghcSpec
               liftedSpec = toLiftedSpec (bareSpec1 { defines = defines bareSpec })
-              -- ls' = trace ("liftedDefines @" ++ show (giTargetMod targetSrc) ++ " = " ++ show (liftedDefines liftedSpec)) $ liftedSpec
-          liftedSpec' <- removeUnexportedLocalAssumptions liftedSpec --ls'
+          liftedSpec' <- removeUnexportedLocalAssumptions liftedSpec
           return $ Right (phaseOneWarns <> warns, targetSpec, liftedSpec')
 
     toLegacyDep :: (Ghc.StableModule, LiftedSpec) -> (ModName, BareSpec)
@@ -134,7 +130,6 @@ makeTargetSpec cfg localVars lnameEnv lmap targetSrc bareSpec dependencies = do
       return lspec { liftedAsmSigs = S.filter (exportedAssumption . val . fst) (liftedAsmSigs lspec) }
 
     ghcSpecToBareSpec = toBareSpecLHName cfg lnameEnv . _gsLSpec
-    --ghcSpecToLiftedSpec = toLiftedSpec . foo
 
 
 -------------------------------------------------------------------------------------
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
index a5dc36203a..9fe688174f 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
@@ -7,9 +7,6 @@ coreToLogic = unlines
   , "define GHC.Internal.Real.mod x y        = (x mod y)"
   , "define GHC.Internal.Real.fromIntegral x = (x)"
 
---  , "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)"
   , ""
@@ -24,8 +21,6 @@ coreToLogic = unlines
   , "define Language.Haskell.Liquid.String.stringEmp = (stringEmp)"
   , "define Language.Haskell.Liquid.Equational.eq x y = (y)"
 
-  -- , "define Language.Haskell.Liquid.ProofCombinators.withProof x y = (x)"
-
   , "define Language.Haskell.Liquid.ProofCombinators.cast x y = (y)"
   , "define Liquid.ProofCombinators.cast x y = (y)"
   , "define ProofCombinators.cast x y = (y)"
@@ -49,12 +44,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      = (listElts xs)"
---  , ""
---  , "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)"
   ]
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
index 2f1720d8ee..473d234fc1 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
@@ -19,13 +19,11 @@ 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.Fixpoint.Types.Refinements     as F
 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
@@ -380,10 +378,12 @@ processInputSpec cfg pipelineData modSummary inputSpec = do
 
   logicMap :: LogicMap <- liftIO LH.makeLogicMap
 
+-- debugLog $ "Logic map:\n" ++ show logicMap
+
   let lhContext = LiquidHaskellContext {
         lhGlobalCfg       = cfg
       , lhInputSpec       = inputSpec
-      , lhModuleLogicMap  = logicMap -- <> toLogicMap defines
+      , lhModuleLogicMap  = logicMap
       , lhModuleSummary   = modSummary
       , lhModuleTcData    = pdTcData pipelineData
       , lhModuleGuts      = pdUnoptimisedCore pipelineData
@@ -545,11 +545,11 @@ processModule LiquidHaskellContext{..} = do
     tcg <- getGblEnv
     let localVars = Resolve.makeLocalVars preNormalizedCore
         modsym = symbol $ GHC.moduleName thisModule
-        -- we do this here because we 1) have the module name 2) process dependencies here
-        defs = map (\(ls , ae) -> (LH.qualifySymbol modsym <$> ls , ae)) $ defines bareSpec0
-        localLogicMap = toLogicMap defs
-        depsLogicMap = foldr (\h l -> l <> mempty {lmSymDefs = h}) mempty (liftedDefines <$> (HM.elems . getDependencies) dependencies)
-        lm = lhModuleLogicMap <> depsLogicMap <> localLogicMap
+        defs = map (\(ls , ae) -> (LH.qualifySymbol modsym <$> ls , ae)) $
+               defines bareSpec0
+        depsLogicMap = foldr (\h l -> l <> mempty {lmSymDefs = h}) mempty $
+                       liftedDefines <$> (HM.elems . getDependencies) dependencies
+        lm = lhModuleLogicMap <> depsLogicMap <> toLogicMap defs
         eBareSpec = resolveLHNames
           moduleCfg
           thisModule
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
index f45e586294..d8df06e96c 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
@@ -91,8 +91,6 @@ import           Language.Haskell.Liquid.WiredIn
 import qualified Text.PrettyPrint.HughesPJ as PJ
 import qualified Text.Printf               as Printf
 
--- import Debug.Trace (trace)
-
 -- | Collects type aliases from the current module and its dependencies.
 --
 -- It doesn't matter at the moment in which module a type alias is defined.
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
index 5099c79a33..f8a53d491b 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
@@ -930,7 +930,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  (LocSymbol, [Symbol], Expr)              -- ^ 'define' annotation for specifying logic aliases
+  | Define  (LocSymbol, ([Symbol], Expr))              -- ^ 'define' annotation for specifying logic aliases
   deriving (Data, Typeable)
 
 instance PPrint BPspec where
@@ -1031,7 +1031,7 @@ ppPspec k (DSize   (ds, ss))
   = "data size" <+> splice " " (pprintTidy k <$> map (fmap parsedToBareType) ds) <+> pprintTidy k (val ss)
 ppPspec _ (BFix    _)           --
   = "fixity"
-ppPspec k (Define  (lx, ys , e))
+ppPspec k (Define  (lx, (ys, e)))
   = "define" <+> pprintTidy k (val lx) <+> " " <+> pprintTidy k ys <+> "=" <+> pprintTidy k e
 ppPspec k (Relational (lxl, lxr, tl, tr, q, p))
   = "relational"
@@ -1132,7 +1132,7 @@ mkSpec xs = Measure.Spec
   , Measure.ignores    = S.fromList [s | Ignore s <- xs]
   , Measure.autosize   = S.fromList [s | ASize  s <- xs]
   , Measure.axeqs      = []
-  , Measure.defines    = [ (x , (as , e)) | Define (x , as , e) <- xs]
+  , Measure.defines    = [ d | Define d <- xs]
   }
 
 -- | Parse a single top level liquid specification
@@ -1326,11 +1326,11 @@ rtAliasP f bodyP
 
 logDefineP :: Parser BPspec
 logDefineP =
-    do s <- locBinderP -- locBinderLHNameP
+    do s <- locBinderP
        args <- many locSymbolP
        reservedOp "="
        e <- exprP <|> predP
-       return (Define (s, val <$> args, val <$> e))
+       return (Define (s, (val <$> args, val <$> e)))
 
 hmeasureP :: Parser BPspec
 hmeasureP = do
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
index 2aff6740cd..5efca36156 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
@@ -44,7 +44,6 @@ import Language.Fixpoint.Types
 import Language.Haskell.Liquid.GHC.Misc (locNamedThing) -- Symbolic GHC.Name
 import qualified Liquid.GHC.API as GHC
 import Text.PrettyPrint.HughesPJ.Compat
--- import qualified GHC.Plugins as GHC
 
 -- RJ: Please add docs
 lenLocSymbol :: Located Symbol
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
index aadc64e08d..724dea8948 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
@@ -488,7 +488,6 @@ emapSpecM bscp lenv vf f sp = do
         (traverse (emapBoundM (traverse . f) (\e -> emapExprVM (vf . (++ e)))))
         (M.toList $ bounds sp)
     axeqs <- mapM (emapEquationM vf) $ axeqs sp
---    defines <- mapM (emapEquationM vf) $ defines sp
     return sp
       { measures
       , expSigs
@@ -512,7 +511,6 @@ emapSpecM bscp lenv vf f sp = do
       , dsize
       , bounds
       , axeqs
---      , defines
       }
   where
     fnull = f []
@@ -749,7 +747,7 @@ data LiftedSpec = LiftedSpec
   , liftedAxeqs      :: HashSet (F.EquationV LHName)
     -- ^ Equalities used for Proof-By-Evaluation
   , liftedDefines    :: M.HashMap F.Symbol LMap
-    -- ^ Logical synonyms
+    -- ^ Logic aliases
   } deriving (Eq, Data, Generic)
     deriving Hashable via Generically LiftedSpec
     deriving Binary   via Generically LiftedSpec
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
index 7b6cc06d6d..5eb8250ce3 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
@@ -128,7 +128,7 @@ module Language.Haskell.Liquid.Types.Types (
   , mapRTAVars
 
   -- * CoreToLogic
-  , LogicMap(..), toLMap, fromLMap, toLogicMap, {- toLogicMapWith, -} eAppWithMap, LMap(..)
+  , LogicMap(..), toLMap, fromLMap, toLogicMap, eAppWithMap, LMap(..)
 
   -- * Refined Instances
   , RDEnv, DEnv(..), RInstance(..), RISig(..)
@@ -285,25 +285,6 @@ fromLMap (LMap x ys e) = (x, (ys, e))
 toLogicMap :: [(F.LocSymbol, ([Symbol], Expr))] -> LogicMap
 toLogicMap ls = mempty {lmSymDefs = M.fromList $ map toLMap ls}
 
-{-
-toLogicMapWith :: (Symbol -> Symbol) -> [(F.LocSymbol, ([Symbol], Expr))] -> LogicMap
-toLogicMapWith f ls = mempty {lmSymDefs = M.fromList $ map toLMap ls}
-  where
-    toLMap (x, (ys, e)) =
-      let x' = f <$> x in
-      (F.val x', LMap {lmVar = x', lmArgs = ys, lmExpr = e})
--}
-{-
-defsToLogicMap :: Symbol -> M.HashMap (F.LocSymbol) ([Symbol], Expr) -> LogicMap
-defsToLogicMap modsym ls = mempty {lmSymDefs = M.fromList $ map toLMap $ M.toList ls}
-  where
-    toLMap (x, (ys, e)) =
-        let qx = qualifySymbol modsym <$> x in
-        ( F.val qx
-        , LMap { lmVar = qx
-               , lmArgs = ys
-               , lmExpr = e})
--}
 eAppWithMap :: LogicMap -> Symbol -> [Expr] -> Expr -> Expr
 eAppWithMap lmap f es expr
   | Just (LMap _ xs e) <- M.lookup f (lmSymDefs lmap)
diff --git a/tests/pos/WithProofRefl.hs b/tests/pos/WithProofRefl.hs
deleted file mode 100644
index 69084fee6c..0000000000
--- a/tests/pos/WithProofRefl.hs
+++ /dev/null
@@ -1,13 +0,0 @@
-{-@ LIQUID "--save" @-}
-module WithProofRefl where
-
-import Language.Haskell.Liquid.ProofCombinators
-
-{-@ reflect unify' @-}
-unify' :: Int -> Int
-unify' 0 = 42
-unify' i = (i-1) `withProof` theoremUnify' i
-
-theoremUnify' :: Int -> Proof
-theoremUnify' i = ()
--- theoremUnify' i = theoremUnify' (i-1)
diff --git a/tests/tests.cabal b/tests/tests.cabal
index 512a4be4ea..65b6a06cc5 100644
--- a/tests/tests.cabal
+++ b/tests/tests.cabal
@@ -2014,7 +2014,6 @@ executable unit-pos-3
                     , WBL0
                     , WBL
                     , WhyLH
-                    , WithProofRefl
                     , Words1
                     , Words
                     , Wrap0

From 0f8f117c0aff38a5454d8bace3d76cabfd2e56bc Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Wed, 11 Dec 2024 10:52:53 +0100
Subject: [PATCH 06/15] cleanup

---
 liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs | 2 --
 1 file changed, 2 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
index 9cd8c20e6b..f897729915 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
@@ -196,8 +196,6 @@ import           Language.Haskell.Liquid.Types.Names
 import           Language.Haskell.Liquid.Types.RType
 import           Language.Haskell.Liquid.Misc
 
--- import Debug.Trace
-
 
 -----------------------------------------------------------------------------
 -- | Information about Type Constructors

From 0b86503097d21cad6a57ff20c2684b07ea774ade Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Wed, 11 Dec 2024 11:11:53 +0100
Subject: [PATCH 07/15] refactor

---
 liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
index 74a411d590..97521b8075 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
@@ -545,8 +545,8 @@ processModule LiquidHaskellContext{..} = do
         modsym = symbol $ GHC.moduleName thisModule
         defs = map (\(ls , ae) -> (LH.qualifySymbol modsym <$> ls , ae)) $
                defines bareSpec0
-        depsLogicMap = foldr (\h l -> l <> mempty {lmSymDefs = h}) mempty $
-                       liftedDefines <$> (HM.elems . getDependencies) dependencies
+        depsLogicMap = foldr (\ls lmp -> lmp <> mempty {lmSymDefs = liftedDefines ls}) mempty $
+                       (HM.elems . getDependencies) dependencies
         lm = lhModuleLogicMap <> depsLogicMap <> toLogicMap defs
         eBareSpec = resolveLHNames
           moduleCfg

From 9b24f507f4e8e0f4ad3221deefe2f6753c0ca73a Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Wed, 11 Dec 2024 13:12:38 +0100
Subject: [PATCH 08/15] apply hlint suggestion

---
 liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
index 97521b8075..e80fd59395 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
@@ -43,6 +43,7 @@ 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
@@ -543,8 +544,7 @@ processModule LiquidHaskellContext{..} = do
     tcg <- getGblEnv
     let localVars = Resolve.makeLocalVars preNormalizedCore
         modsym = symbol $ GHC.moduleName thisModule
-        defs = map (\(ls , ae) -> (LH.qualifySymbol modsym <$> ls , ae)) $
-               defines bareSpec0
+        defs = first (fmap (LH.qualifySymbol modsym)) <$> defines bareSpec0
         depsLogicMap = foldr (\ls lmp -> lmp <> mempty {lmSymDefs = liftedDefines ls}) mempty $
                        (HM.elems . getDependencies) dependencies
         lm = lhModuleLogicMap <> depsLogicMap <> toLogicMap defs

From 9971f17cde80c9cfe0b895f8f0204db96f16dafb Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Tue, 17 Dec 2024 14:26:46 +0100
Subject: [PATCH 09/15] WIP reimplement define using name resolution

---
 .../src/Language/Haskell/Liquid/Bare.hs       | 11 +--
 .../src/Language/Haskell/Liquid/Bare/Check.hs |  2 +-
 .../Language/Haskell/Liquid/Bare/Measure.hs   |  6 +-
 .../src/Language/Haskell/Liquid/GHC/Plugin.hs | 24 ++++---
 .../Haskell/Liquid/LHNameResolution.hs        | 68 ++++++++++++++-----
 .../src/Language/Haskell/Liquid/Parse.hs      |  8 +--
 .../Language/Haskell/Liquid/Types/Names.hs    | 16 ++++-
 .../Haskell/Liquid/Types/PrettyPrint.hs       |  4 +-
 .../Language/Haskell/Liquid/Types/Specs.hs    | 13 ++--
 .../Language/Haskell/Liquid/Types/Types.hs    | 36 ++++++----
 tests/pos/NumRefl.hs                          |  9 ++-
 11 files changed, 132 insertions(+), 65 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
index dc7f70195d..7a2f571232 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
@@ -105,8 +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 })
+--              bareSpec1 = ghcSpecToBareSpec ghcSpec
+--              liftedSpec = toLiftedSpec lnameEnv (bareSpec1 { defines = defines bareSpec })
+              liftedSpec = ghcSpecToLiftedSpec ghcSpec
+
           liftedSpec' <- removeUnexportedLocalAssumptions liftedSpec
           return $ Right (phaseOneWarns <> warns, targetSpec, liftedSpec')
 
@@ -135,8 +137,8 @@ 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
-
+--    ghcSpecToBareSpec = toBareSpecLHName cfg lnameEnv . _gsLSpec
+    ghcSpecToLiftedSpec = toLiftedSpec lnameEnv . toBareSpecLHName cfg lnameEnv . _gsLSpec
 
 -------------------------------------------------------------------------------------
 -- | @makeGhcSpec@ invokes @makeGhcSpec0@ to construct the @GhcSpec@ and then
@@ -283,6 +285,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
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs
index d4da34ce6b..3d0af34383 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs
+++ b/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
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
index 3aae5e930a..e087aa2bd4 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
+++ b/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 mbEnv = S.unions . fmap (uncurry $ names mbEnv) . M.toList
 -- 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 (Just env) 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
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
index e80fd59395..5ce31a5493 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
@@ -24,6 +24,7 @@ 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,6 +37,7 @@ 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)
 
@@ -43,7 +45,7 @@ import           Control.Monad
 import qualified Control.Monad.Catch as Ex
 import           Control.Monad.IO.Class (MonadIO)
 
-import           Data.Bifunctor                           ( first )
+--import           Data.Bifunctor                           ( first )
 import           Data.Coerce
 import           Data.Function                            ((&))
 import qualified Data.List                               as L
@@ -76,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
@@ -543,11 +547,14 @@ processModule LiquidHaskellContext{..} = do
 
     tcg <- getGblEnv
     let localVars = Resolve.makeLocalVars preNormalizedCore
-        modsym = symbol $ GHC.moduleName thisModule
-        defs = first (fmap (LH.qualifySymbol modsym)) <$> defines bareSpec0
-        depsLogicMap = foldr (\ls lmp -> lmp <> mempty {lmSymDefs = liftedDefines ls}) mempty $
+        -- 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.logicNameToSymbol <$> l) $ liftedDefines ls}) mempty $
                        (HM.elems . getDependencies) dependencies
-        lm = lhModuleLogicMap <> depsLogicMap <> toLogicMap defs
+        -- 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
@@ -555,18 +562,19 @@ processModule LiquidHaskellContext{..} = do
           (imp_mods $ tcg_imports tcg)
           (tcg_rdr_env tcg)
           lm
-          bareSpec0 { defines = defs }
+          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
-              lm
+              lmap' {- lmap'' -}
               targetSrc
               bareSpec
               dependencies
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
index 0830c9e3f3..b5d665ce49 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
@@ -87,12 +87,15 @@ import qualified Language.Haskell.Liquid.Types.DataDecl as DataDecl
 import           Language.Haskell.Liquid.Types.Errors (TError(ErrDupNames, ErrResolve), panic)
 import           Language.Haskell.Liquid.Types.Specs as Specs
 import           Language.Haskell.Liquid.Types.Types
+--import           Language.Haskell.Liquid.Types.Names
 import           Language.Haskell.Liquid.UX.Config
 import           Language.Haskell.Liquid.WiredIn
 
 import qualified Text.PrettyPrint.HughesPJ as PJ
 import qualified Text.Printf               as Printf
 
+-- import Debug.Trace
+
 -- | Collects type aliases from the current module and its dependencies.
 --
 -- It doesn't matter at the moment in which module a type alias is defined.
@@ -124,38 +127,53 @@ resolveLHNames
   -> LogicMap
   -> BareSpecParsed
   -> TargetDependencies
-  -> Either [Error] (BareSpec, LogicNameEnv)
+  -> Either [Error] (BareSpec, LogicNameEnv, LogicMap)
 resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 dependencies = do
-    let ((bs, logicNameEnv), (es, ns)) =
+    let ((bs, logicNameEnv, lmap'), (es, ns)) =
           flip runState mempty $ do
+            -- let bs0 = trace ("bareDefines0 " ++ show (defines bareSpec0)) $ bareSpec0
             -- A generic traversal that resolves names of Haskell entities
+            -- let bs0 = trace ("resolveLHNames bareSpec0 = " ++ show (defines bareSpec0)) $ bareSpec0
             sp1 <- mapMLocLHNames (\l -> (<$ l) <$> resolveLHName l) $
-                     fixExpressionArgsOfTypeAliases taliases bareSpec0
+                     fixExpressionArgsOfTypeAliases taliases bareSpec0 -- bs0
+            -- let bs1 = trace ("resolveLHNames bareSpec1 = " ++ show (defines sp1)) $ sp1
+            --(dnames, sp1) <- mapMLocLHNames (\l -> (<$ l) <$> resolveLHName l)
+            --         (map (\l -> fmap (makeUnresolvedLHName ((LHVarName LHThisModuleNameF))) (lmVar l)) (defines bareSpec0),
+            --         fixExpressionArgsOfTypeAliases taliases bareSpec0 -- bs0
+            --         )
+            --let d1 = trace ("defines1 " ++ show (defines sp1)) $ defines sp1
+            -- let bs1 = trace ("bareDefines1 " ++ show (defines sp1)) $ sp1
+            -- let lmap' = trace ("lmap " ++ show lmap) $ lmap <> mempty {lmSymDefs = HM.fromList $ map (\l -> (val $ lmVar l , val <$> l)) $ defines bs1 }
             -- Now we do a second traversal to resolve logic names
             let (inScopeEnv, logicNameEnv0, privateReflectNames, unhandledNames) =
-                  makeLogicEnvs impMods thisModule sp1 dependencies
+                  makeLogicEnvs impMods thisModule sp1 {- bs1 -} dependencies -- dnames'
+                lm' = lmap <> mempty {lmSymDefs = HM.fromList $ map (\(k , v) -> ( qualifyLHName $ F.val k
+                                                                                   , (fmap val v) { lmVar = qualifyLHName <$> k }
+                                                                                   )) $ defines sp1 }
             sp2 <- fromBareSpecLHName <$>
                      resolveLogicNames
                        cfg
                        inScopeEnv
                        globalRdrEnv
                        unhandledNames
-                       lmap
+                       lm'
                        localVars
                        logicNameEnv0
                        privateReflectNames
                        thisModule
                        sp1
-            return (sp2, logicNameEnv0)
+            return (sp2, logicNameEnv0, lm')
         logicNameEnv' = extendLogicNameEnv logicNameEnv ns
     if null es then
-      Right (bs, logicNameEnv')
+      Right (bs, logicNameEnv', lmap')
     else
       Left es
   where
     taliases = collectTypeAliases thisModule bareSpec0 dependencies
 
-    resolveLHName lname = case val lname of
+    resolveLHName lname =
+      -- let lname' = trace ("resolveLHName lname = " ++ show lname) $ lname in
+      case val lname {- lname' -} of
       LHNUnresolved LHTcName s
         | isTuple s ->
           pure $ LHNResolved (LHRGHC $ GHC.tupleTyConName GHC.BoxedTuple (tupleArity s)) s
@@ -168,7 +186,8 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
             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
+        | isDataCon s ->
+            lookupGRELHName (LHDataConName lcl) lname s listToMaybe
         | otherwise ->
             lookupGRELHName ns lname s
               (fmap (either id GHC.getName) . Resolve.lookupLocalVar localVars (atLoc lname s))
@@ -180,11 +199,13 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
       case maybeDropImported ns $ GHC.lookupGRE globalRdrEnv (mkLookupGRE ns s) of
         [e] -> do
           let n = GHC.greName e
-              n' = fromMaybe n $ localNameLookup [n]
+              -- n0 = trace ("lookupGRELHName [e] = " ++ show n) $ n
+              n' = fromMaybe n $ localNameLookup [n  {- n0 -}]
           pure $ LHNResolved (LHRGHC n') s
         es@(_:_) -> do
           let topLevelNames = map GHC.greName es
-          case localNameLookup topLevelNames of
+              -- topLevelNames' = trace ("lookupGRELHName [es] = " ++ show topLevelNames) $ topLevelNames
+          case localNameLookup topLevelNames {- topLevelNames' -} of
             Just n | notElem n topLevelNames ->
               pure $ LHNResolved (LHRGHC n) s
             _ -> do
@@ -196,9 +217,10 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
                 )
               pure $ val lname
         [] ->
+          --- let s' = trace ("lookupGRELHName [] = " ++ show s) $ s in
           case localNameLookup [] of
             Just n' ->
-              pure $ LHNResolved (LHRGHC n') s
+              pure $ LHNResolved (LHRGHC n') s -- s'
             Nothing -> do
               addError
                 (errResolve (nameSpaceKind ns) "Cannot resolve name" (s <$ lname))
@@ -402,12 +424,13 @@ makeLogicEnvs
   -> GHC.Module
   -> BareSpecParsed
   -> TargetDependencies
+--  -> [Located LHName]
   -> ( InScopeNonReflectedEnv
      , LogicNameEnv
      , HS.HashSet LocSymbol
      , HS.HashSet Symbol
      )
-makeLogicEnvs impAvails thisModule spec dependencies =
+makeLogicEnvs impAvails thisModule spec dependencies {- defnames -} =
     let unqualify s =
           if s == LH.qualifySymbol (symbol $ GHC.moduleName thisModule) (LH.dropModuleNames s) then
             LH.dropModuleNames s
@@ -420,6 +443,7 @@ makeLogicEnvs impAvails thisModule spec dependencies =
           map unqualify unhandledNamesList ++ map (LH.qualifySymbol (symbol $ GHC.moduleName thisModule)) unhandledNamesList
         unhandledNamesList = concat $
           [ map (rtName . val) $ ealiases spec
+--          , map (val . lmVar) $ defines spec
           , map fst $
              concatMap (DataDecl.dcpTyArgs . val) wiredDataCons
           , map fst $
@@ -442,10 +466,13 @@ makeLogicEnvs impAvails thisModule spec dependencies =
               , HS.toList (opaqueReflects spec)
               , HS.toList (inlines spec)
               , HS.toList (hmeas spec)
+--              , defnames
+              -- , map (fmap makeLocalLHName . lmVar) (defines spec)
               ]
             ]
           , [ makeLogicLHName (val (msName m)) thisModule Nothing | m <- measures spec ]
           , [ makeLogicLHName (val (msName m)) thisModule Nothing | m <- cmeasures spec ]
+--          , [ makeLogicLHName (val (lmVar d)) thisModule Nothing | d <- defines spec ]
           ]
         privateReflectNames =
           mconcat $
@@ -528,6 +555,7 @@ collectLiftedSpecLogicNames sp = concat
     [ map fst (HS.toList $ liftedExpSigs sp)
     , map (fst . snd) (HM.toList $ liftedMeasures sp)
     , map (fst . snd) (HM.toList $ liftedCmeasures sp)
+--    , map (lmVar . snd) (HM.toList $ liftedDefines sp)
     ]
 
 -- | Resolves names in the logic namespace
@@ -572,11 +600,15 @@ resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv p
         -- The name is local
       | elem s ss = return $ makeLocalLHName s
       | otherwise =
-        case lookupInScopeNonReflectedEnv env s of
+        -- let s' = trace ("resolveLogicName s = " ++ show s) $ s in
+        case lookupInScopeNonReflectedEnv env s {- s' -} of
           Left alts ->
             -- If names are not in the environment, they must be data constructors,
             -- or they must be reflected functions, or they must be in the logicmap.
-            case resolveDataConName ls `mplus` resolveVarName lmap0 ls of
+            -- let lmap0' = trace ("resolveLogicName lmap0 = " ++ show lmap0) $ lmap0
+            --     ls' = trace ("resolveLogicName ls = " ++ show ls) $ ls
+            --   in
+            case resolveDataConName ls {- ls' -} `mplus` resolveVarName lmap0 ls {- lmap0' ls' -} of
               Just m -> m
               Nothing -> do
                 unless (HS.member s unhandledNames) $
@@ -650,9 +682,10 @@ resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv p
     -- @InScopeNonReflectedEnv@ indicates where the reflect annotations were
     -- imported from, but not where the Haskell names were imported from.
     resolveVarName lmap s = do
+      -- let s' = trace ("resolveVarName s = " ++ show s) $ s
       let gres =
             GHC.lookupGRE globalRdrEnv $
-            mkLookupGRE (LHVarName LHAnyModuleNameF) (val s)
+            mkLookupGRE (LHVarName LHAnyModuleNameF) (val s {- s'-})
           refls = mapMaybe (findReflection . GHC.greName) gres
       case refls of
         [lhName] -> Just $ return lhName
@@ -662,7 +695,8 @@ resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv p
           -> case gres of
           [e] -> do
             let n = GHC.greName e
-            if HM.member (symbol n) (lmSymDefs lmap) then
+                -- n' = trace ("resolveVarName n = " ++ show n) $ n
+            if HM.member (symbol n {-n'-}) (lmSymDefs lmap) then
               Just $ do
                 let lhName = makeLogicLHName (symbol n) (GHC.nameModule n) Nothing
                 addName lhName
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
index bb859585f3..c244672da4 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
@@ -930,7 +930,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  (LocSymbol, ([Symbol], Expr))              -- ^ '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
@@ -1132,7 +1132,7 @@ mkSpec xs = Measure.Spec
   , Measure.ignores    = S.fromList [s | Ignore s <- xs]
   , Measure.autosize   = S.fromList [s | ASize  s <- xs]
   , Measure.axeqs      = []
-  , Measure.defines    = [ d | Define d <- xs]
+  , Measure.defines    = [ toLMapV' d | Define d <- xs]
   }
 
 -- | Parse a single top level liquid specification
@@ -1326,11 +1326,11 @@ rtAliasP f bodyP
 
 logDefineP :: Parser BPspec
 logDefineP =
-    do s <- locBinderP
+    do s <- locBinderLHNameP
        args <- many locSymbolP
        reservedOp "="
        e <- exprP <|> predP
-       return (Define (s, (val <$> args, val <$> e)))
+       return (Define (s, (val <$> args, e)))
 
 hmeasureP :: Parser BPspec
 hmeasureP = do
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
index 5efca36156..1ba7c7f7a3 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
@@ -29,6 +29,7 @@ module Language.Haskell.Liquid.Types.Names
   , reflectGHCName
   , reflectLHName
   , updateLHNameSymbol
+  , qualifyLHName
   ) where
 
 import Control.DeepSeq
@@ -40,8 +41,9 @@ import Data.String (fromString)
 import qualified Data.Text                               as Text
 import GHC.Generics
 import GHC.Stack
+
 import Language.Fixpoint.Types
-import Language.Haskell.Liquid.GHC.Misc (locNamedThing) -- Symbolic GHC.Name
+import Language.Haskell.Liquid.GHC.Misc -- Symbolic GHC.Name
 import qualified Liquid.GHC.API as GHC
 import Text.PrettyPrint.HughesPJ.Compat
 
@@ -136,8 +138,11 @@ instance Ord LogicName where
       x -> x
 
 instance Show LHName where
-  show (LHNResolved _ s) = symbolString s
-  show (LHNUnresolved _ s) = symbolString s
+  show (LHNResolved (LHRLogic _) s) = "RL@" ++ symbolString s
+  show (LHNResolved (LHRGHC n)   s) = "RG@" ++ symbolString s ++ show n
+  show (LHNResolved (LHRLocal _) s) = "RK@" ++ symbolString s
+  show (LHNResolved (LHRIndex _) s) = "RI@" ++ symbolString s
+  show (LHNUnresolved ns s) = "U[" ++ show ns ++ "]@" ++ symbolString s
 
 instance NFData LHName
 instance NFData LHResolvedName
@@ -237,6 +242,11 @@ getLHGHCName :: LHName -> Maybe GHC.Name
 getLHGHCName (LHNResolved (LHRGHC n) _) = Just n
 getLHGHCName _ = Nothing
 
+qualifyLHName :: LHName -> Symbol
+qualifyLHName (LHNResolved (LHRGHC n) _) = qualifiedNameSymbol n
+qualifyLHName (LHNResolved _ s) = s
+qualifyLHName (LHNUnresolved _ s) = s
+
 mapLHNames :: Data a => (LHName -> LHName) -> a -> a
 mapLHNames f = go
   where
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PrettyPrint.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PrettyPrint.hs
index 56ea4e1a20..c2c78b20e0 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PrettyPrint.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PrettyPrint.hs
@@ -159,8 +159,8 @@ pprXOT k (x, v) = (xd, pprintTidy k v)
   where
     xd          = maybe "unknown" (pprintTidy k) x
 
-instance PPrint LMap where
-  pprintTidy _ (LMap x xs e) = hcat [pprint x, pprint xs, text "|->", pprint e ]
+instance (Ord v, F.Fixpoint v, PPrint v) => PPrint (LMapV v) where
+  pprintTidy _ (LMapV x xs e) = hcat [pprint x, pprint xs, text "|->", pprint e ]
 
 instance PPrint LogicMap where
   pprintTidy _ (LM lm am) = vcat [ text "Logic Map"
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
index b718a80496..a1e5b4b5db 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
@@ -74,7 +74,7 @@ module Language.Haskell.Liquid.Types.Specs (
   ) where
 
 import           GHC.Generics            hiding (to, moduleName)
-import           Data.Bifunctor          (bimap, first)
+import           Data.Bifunctor          (bimap, first, second)
 import           Data.Bitraversable      (bimapM)
 import           Data.Binary
 import qualified Language.Fixpoint.Types as F
@@ -425,7 +425,7 @@ data Spec lname ty = Spec
   , dsize      :: ![([F.Located ty], lname)]                          -- ^ Size measure to enforce fancy termination
   , bounds     :: !(RRBEnvV lname (F.Located ty))
   , axeqs      :: ![F.EquationV lname]                                -- ^ Equalities used for Proof-By-Evaluation
-  , defines    :: ![(F.LocSymbol, ([F.Symbol], F.Expr))]              -- ^ Logic aliases
+  , defines    :: ![(F.Located LHName, LMapV lname)]                  -- ^ Logic aliases
   } deriving (Data, Generic)
 
 instance (Show lname, F.PPrint lname, Show ty, F.PPrint ty, F.PPrint (RTypeV lname BTyCon BTyVar (RReftV lname))) => F.PPrint (Spec lname ty) where
@@ -492,6 +492,7 @@ emapSpecM bscp lenv vf f sp = do
         (traverse (emapBoundM (traverse . f) (\e -> emapExprVM (vf . (++ e)))))
         (M.toList $ bounds sp)
     axeqs <- mapM (emapEquationM vf) $ axeqs sp
+    defines <- mapM (traverse (emapLMapM vf)) $ defines sp
     return sp
       { measures
       , expSigs
@@ -515,6 +516,7 @@ emapSpecM bscp lenv vf f sp = do
       , dsize
       , bounds
       , axeqs
+      , defines
       }
   where
     fnull = f []
@@ -584,6 +586,7 @@ mapSpecLName f Spec {..} =
       , bounds = M.map (fmap (fmap f)) bounds
       , axeqs = map (fmap f) axeqs
       , dsize = map (fmap f) dsize
+      , defines = map (second $ fmap f) defines
       , ..
       }
   where
@@ -760,7 +763,7 @@ data LiftedSpec = LiftedSpec
   , liftedBounds     :: RRBEnvV LHName LocBareTypeLHName
   , liftedAxeqs      :: HashSet (F.EquationV LHName)
     -- ^ Equalities used for Proof-By-Evaluation
-  , liftedDefines    :: M.HashMap F.Symbol LMap
+  , liftedDefines    :: HashMap F.Symbol (LMapV LHName)
     -- ^ Logic aliases
   } deriving (Eq, Data, Generic)
     deriving Hashable via Generically LiftedSpec
@@ -991,7 +994,7 @@ toLiftedSpec lenv a = LiftedSpec
   , liftedDsize      = dsize a
   , liftedBounds     = bounds a
   , liftedAxeqs      = S.fromList . axeqs $ a
-  , liftedDefines    = M.fromList . map toLMap . defines $ a
+  , liftedDefines    = M.fromList . map (first (qualifyLHName . F.val)) . defines $ a
   }
 
 -- This is a temporary internal function that we use to convert the input dependencies into a format
@@ -1037,5 +1040,5 @@ unsafeFromLiftedSpec a = Spec
   , dsize      = liftedDsize  a
   , bounds     = liftedBounds a
   , axeqs      = S.toList . liftedAxeqs $ a
-  , defines    = map (fromLMap . snd) . M.toList . liftedDefines $ a
+  , defines    = map (\p -> first (dummyLoc . makeLocalLHName) p) . M.toList . liftedDefines $ a
   }
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
index f897729915..23bf0fc5cc 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
@@ -128,7 +128,7 @@ module Language.Haskell.Liquid.Types.Types (
   , mapRTAVars
 
   -- * CoreToLogic
-  , LogicMap(..), toLMap, fromLMap, toLogicMap, eAppWithMap, LMap(..)
+  , LogicMap(..), toLMapV, toLMapV', toLogicMap, eAppWithMap, emapLMapM, LMapV(..), LMap
 
   -- * Refined Instances
   , RDEnv, DEnv(..), RInstance(..), RISig(..)
@@ -263,34 +263,40 @@ instance Monoid LogicMap where
 instance Semigroup LogicMap where
   LM x1 x2 <> LM y1 y2 = LM (M.union x1 y1) (M.union x2 y2)
 
-data LMap = LMap
+data LMapV v = LMapV
   { lmVar  :: F.LocSymbol
   , lmArgs :: [Symbol]
-  , lmExpr :: Expr
-  } deriving (Eq, Data, Generic)
-    deriving Hashable via Generically LMap
-    deriving Binary   via Generically LMap
+  , lmExpr :: F.ExprV v
+  } deriving (Eq, Data, Generic, Functor)
+    deriving Hashable via Generically (LMapV v)
+    deriving Binary   via Generically (LMapV v)
+type LMap = LMapV F.Symbol
 
-instance Show LMap where
-  show (LMap x xs e) = show x ++ " " ++ show xs ++ "\t |-> \t" ++ show e
+instance (Show v, Ord v, F.Fixpoint v) => Show (LMapV v) where
+  show (LMapV x xs e) = show x ++ " " ++ show xs ++ "\t |-> \t" ++ show e
 
-toLMap :: (F.LocSymbol, ([Symbol], Expr)) -> (Symbol, LMap)
-toLMap (x, (ys, e)) = (F.val x, LMap {lmVar = x, lmArgs = ys, lmExpr = e})
+toLMapV' :: (F.Located LHName, ([Symbol], F.ExprV v)) -> (F.Located LHName, LMapV v)
+toLMapV' (x, (ys, e)) = (x, LMapV {lmVar = fmap getLHNameSymbol x, lmArgs = ys, lmExpr = e})
 
-fromLMap :: LMap -> (F.LocSymbol, ([Symbol], Expr))
-fromLMap (LMap x ys e) = (x, (ys, e))
+toLMapV :: (F.LocSymbol, ([Symbol], F.ExprV v)) -> (Symbol, LMapV v)
+toLMapV (x, (ys, e)) = (F.val $ x, LMapV {lmVar = x, lmArgs = ys, lmExpr = e})
 
 toLogicMap :: [(F.LocSymbol, ([Symbol], Expr))] -> LogicMap
-toLogicMap ls = mempty {lmSymDefs = M.fromList $ map toLMap ls}
+toLogicMap ls = mempty {lmSymDefs = M.fromList $ map toLMapV ls}
 
 eAppWithMap :: LogicMap -> Symbol -> [Expr] -> Expr -> Expr
 eAppWithMap lmap f es expr
-  | Just (LMap _ xs e) <- M.lookup f (lmSymDefs lmap)
+  | Just (LMapV _ xs e) <- M.lookup f (lmSymDefs lmap)
   , length xs == length es
   = F.subst (F.mkSubst $ zip xs es) e
   | otherwise
   = expr
 
+emapLMapM :: Monad m => ([Symbol] -> v0 -> m v1) -> LMapV v0 -> m (LMapV v1)
+emapLMapM f l = do
+    lmExpr <- emapExprVM (f . (++ lmArgs l)) (lmExpr l)
+    return l {lmExpr}
+
 --------------------------------------------------------------------------------
 -- | Refined Instances ---------------------------------------------------------
 --------------------------------------------------------------------------------
@@ -378,7 +384,7 @@ mapRTAVars :: (a -> b) -> RTAlias a ty -> RTAlias b ty
 mapRTAVars f rt = rt { rtTArgs = f <$> rtTArgs rt }
 
 lmapEAlias :: LMap -> F.Located (RTAlias Symbol Expr)
-lmapEAlias (LMap v ys e) = F.atLoc v (RTA (F.val v) [] ys e) -- (F.loc v) (F.loc v)
+lmapEAlias (LMapV v ys e) = F.atLoc v (RTA (F.val v) [] ys e) -- (F.loc v) (F.loc v)
 
 
 -- | The type used during constraint generation, used
diff --git a/tests/pos/NumRefl.hs b/tests/pos/NumRefl.hs
index 9f20c3e087..6e7524bd19 100644
--- a/tests/pos/NumRefl.hs
+++ b/tests/pos/NumRefl.hs
@@ -15,13 +15,16 @@ this program crashes with:
                                              && VV == (-GHC.Internal.Num.fromInteger (GHC.Num.Integer.IS 1))}
     The sort @(176) is not numeric
 
-Because the resule type (Num p) => p cannot be decided to be a numeric type.
+Because the result type (Num p) => p cannot be decided to be a numeric type.
 -}
 
 module NumRefl where
 
-{-@ define GHC.Internal.Num.fromInteger x = (x) @-}
-{-@ define GHC.Num.Integer.IS x           = (x) @-}
+{-@ define fromInteger x = (x) @-}
+-- {-@ define GHC.Num.Integer.IS x          = (x) @-}
+
+-- {-@ define GHC.Internal.Num.fromInteger x = (x) @-}
+-- {-@ define GHC.Num.Integer.IS x           = (x) @-}
 
 {-@ reflect toNum @-}
 toNum :: Num p => () -> p

From 8ff6c1c36ad50de64967d073d5e92df4e44c34b7 Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Tue, 17 Dec 2024 15:41:21 +0100
Subject: [PATCH 10/15] hlint

---
 liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
index b42f913b31..a3fc132fc7 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
@@ -279,7 +279,7 @@ toLMapV' :: (F.Located LHName, ([Symbol], F.ExprV v)) -> (F.Located LHName, LMap
 toLMapV' (x, (ys, e)) = (x, LMapV {lmVar = fmap getLHNameSymbol x, lmArgs = ys, lmExpr = e})
 
 toLMapV :: (F.LocSymbol, ([Symbol], F.ExprV v)) -> (Symbol, LMapV v)
-toLMapV (x, (ys, e)) = (F.val $ x, LMapV {lmVar = x, lmArgs = ys, lmExpr = e})
+toLMapV (x, (ys, e)) = (F.val x, LMapV {lmVar = x, lmArgs = ys, lmExpr = e})
 
 toLogicMap :: [(F.LocSymbol, ([Symbol], Expr))] -> LogicMap
 toLogicMap ls = mempty {lmSymDefs = M.fromList $ map toLMapV ls}

From f6e6eca9aa86cee7da693d14bc144d39ca51ef0d Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Wed, 18 Dec 2024 14:44:17 +0100
Subject: [PATCH 11/15] cleanup, apply review suggestions

---
 .../src/Language/Haskell/Liquid/Bare.hs       |  5 +-
 .../Language/Haskell/Liquid/Bare/Measure.hs   |  2 +-
 .../src/Language/Haskell/Liquid/GHC/Plugin.hs | 19 ++----
 .../Haskell/Liquid/LHNameResolution.hs        | 58 ++++++-------------
 .../Language/Haskell/Liquid/Types/Names.hs    |  6 --
 .../Haskell/Liquid/Types/PrettyPrint.hs       |  2 +-
 .../Language/Haskell/Liquid/Types/Specs.hs    |  2 +-
 .../Language/Haskell/Liquid/Types/Types.hs    | 15 +++--
 8 files changed, 32 insertions(+), 77 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
index 4e04255a8f..c2d3b7ad4d 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
@@ -105,8 +105,6 @@ 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
@@ -137,10 +135,9 @@ 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@.
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
index 48f751a8ad..0ab6d1ecf1 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
+++ b/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) = LMapV vx (F.symbol <$> xs) (either id id e)
+                       ok (xs, e) = LMap 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),
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
index 6202540371..60b99f599f 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
@@ -37,7 +37,6 @@ 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)
 
@@ -45,7 +44,6 @@ 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
@@ -78,8 +76,6 @@ 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
@@ -381,7 +377,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
@@ -547,34 +543,27 @@ 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)
-          lm
-          bareSpec0 -- { defines = defs }
+          (lhModuleLogicMap <> depsLogicMap)
+          bareSpec0
           dependencies
     result <-
       case eBareSpec of
         Left errors -> pure $ Left $ mkDiagnostics [] errors
         Right (bareSpec, lnameEnv, lmap') ->
-          -- let lmap'' = trace ("processModule lmap' = " ++ show lmap') $ lmap' in
           fmap (,bareSpec) <$>
             makeTargetSpec
               moduleCfg
               localVars
               lnameEnv
-              lmap' {- lmap'' -}
+              lmap'
               targetSrc
               bareSpec
               dependencies
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
index a85505d120..5482ec8171 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
@@ -87,15 +87,12 @@ import qualified Language.Haskell.Liquid.Types.DataDecl as DataDecl
 import           Language.Haskell.Liquid.Types.Errors (TError(ErrDupNames, ErrResolve), panic)
 import           Language.Haskell.Liquid.Types.Specs as Specs
 import           Language.Haskell.Liquid.Types.Types
---import           Language.Haskell.Liquid.Types.Names
 import           Language.Haskell.Liquid.UX.Config
 import           Language.Haskell.Liquid.WiredIn
 
 import qualified Text.PrettyPrint.HughesPJ as PJ
 import qualified Text.Printf               as Printf
 
--- import Debug.Trace
-
 -- | Collects type aliases from the current module and its dependencies.
 --
 -- It doesn't matter at the moment in which module a type alias is defined.
@@ -142,21 +139,11 @@ resolveLHNames
   -> TargetDependencies
   -> Either [Error] (BareSpec, LogicNameEnv, LogicMap)
 resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 dependencies = do
-    let ((bs, logicNameEnv, lmap'), (es, ns)) =
+    let ((bs, logicNameEnv, lmap2), (es, ns)) =
           flip runState mempty $ do
-            -- let bs0 = trace ("bareDefines0 " ++ show (defines bareSpec0)) $ bareSpec0
             -- A generic traversal that resolves names of Haskell entities
-            -- let bs0 = trace ("resolveLHNames bareSpec0 = " ++ show (defines bareSpec0)) $ bareSpec0
             sp1 <- mapMLocLHNames (\l -> (<$ l) <$> resolveLHName l) $
-                     fixExpressionArgsOfTypeAliases taliases bareSpec0 -- bs0
-            -- let bs1 = trace ("resolveLHNames bareSpec1 = " ++ show (defines sp1)) $ sp1
-            --(dnames, sp1) <- mapMLocLHNames (\l -> (<$ l) <$> resolveLHName l)
-            --         (map (\l -> fmap (makeUnresolvedLHName ((LHVarName LHThisModuleNameF))) (lmVar l)) (defines bareSpec0),
-            --         fixExpressionArgsOfTypeAliases taliases bareSpec0 -- bs0
-            --         )
-            --let d1 = trace ("defines1 " ++ show (defines sp1)) $ defines sp1
-            -- let bs1 = trace ("bareDefines1 " ++ show (defines sp1)) $ sp1
-            -- let lmap' = trace ("lmap " ++ show lmap) $ lmap <> mempty {lmSymDefs = HM.fromList $ map (\l -> (val $ lmVar l , val <$> l)) $ defines bs1 }
+                     fixExpressionArgsOfTypeAliases taliases bareSpec0
             -- Data decls contain fieldnames that introduce measures with the
             -- same names. We resolved them before constructing the logic
             -- environment.
@@ -168,9 +155,10 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
 
               -- Now we do a second traversal to resolve logic names
               let (inScopeEnv, logicNameEnv0, privateReflectNames, unhandledNames) =
-                    makeLogicEnvs impMods thisModule sp2 {- bs1 -} dependencies -- dnames'
-                  lm' = lmap <> mempty {lmSymDefs = HM.fromList $ map (\(k , v) -> ( qualifyLHName $ F.val k
-                                                                                     , (fmap val v) { lmVar = qualifyLHName <$> k }
+                    makeLogicEnvs impMods thisModule sp2 dependencies
+              -- Add resolved local defines to the logic map
+                  lmap1 = lmap <> mempty {lmSymDefs = HM.fromList $ map (\(k , v) -> ( lhNameToResolvedSymbol $ F.val k
+                                                                                     , (fmap val v) { lmVar = lhNameToResolvedSymbol <$> k }
                                                                                      )) $ defines sp2 }
               sp3 <- fromBareSpecLHName <$>
                        resolveLogicNames
@@ -178,18 +166,18 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
                          inScopeEnv
                          globalRdrEnv
                          unhandledNames
-                         lm'
+                         lmap1
                          localVars
                          logicNameEnv0
                          privateReflectNames
                          allEaliases
                          sp2
-              return (sp3, logicNameEnv0, lm')
+              return (sp3, logicNameEnv0, lmap1)
             else
               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', lmap')
+      Right (bs, logicNameEnv', lmap2)
     else
       Left es
   where
@@ -202,8 +190,7 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
         _ -> panic Nothing $ "unexpected name: " ++ show n
 
     resolveLHName lname =
-      -- let lname' = trace ("resolveLHName lname = " ++ show lname) $ lname in
-      case val lname {- lname' -} of
+      case val lname of
       LHNUnresolved LHTcName s
         | isTuple s ->
           pure $ LHNResolved (LHRGHC $ GHC.tupleTyConName GHC.BoxedTuple (tupleArity s)) s
@@ -233,13 +220,11 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
       case maybeDropImported ns $ GHC.lookupGRE globalRdrEnv (mkLookupGRE ns s) of
         [e] -> do
           let n = GHC.greName e
-              -- n0 = trace ("lookupGRELHName [e] = " ++ show n) $ n
-              n' = fromMaybe n $ localNameLookup [n  {- n0 -}]
+              n' = fromMaybe n $ localNameLookup [n]
           pure $ LHNResolved (LHRGHC n') s
         es@(_:_) -> do
           let topLevelNames = map GHC.greName es
-              -- topLevelNames' = trace ("lookupGRELHName [es] = " ++ show topLevelNames) $ topLevelNames
-          case localNameLookup topLevelNames {- topLevelNames' -} of
+          case localNameLookup topLevelNames of
             Just n | notElem n topLevelNames ->
               pure $ LHNResolved (LHRGHC n) s
             _ -> do
@@ -251,10 +236,9 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
                 )
               pure $ val lname
         [] ->
-          --- let s' = trace ("lookupGRELHName [] = " ++ show s) $ s in
           case localNameLookup [] of
             Just n' ->
-              pure $ LHNResolved (LHRGHC n') s -- s'
+              pure $ LHNResolved (LHRGHC n') s
             Nothing -> do
               addError
                 (errResolve (nameSpaceKind ns) "Cannot resolve name" (s <$ lname))
@@ -466,13 +450,12 @@ makeLogicEnvs
   -> GHC.Module
   -> BareSpecParsed
   -> TargetDependencies
---  -> [Located LHName]
   -> ( InScopeNonReflectedEnv
      , LogicNameEnv
      , HS.HashSet LocSymbol
      , HS.HashSet Symbol
      )
-makeLogicEnvs impAvails thisModule spec dependencies {- defnames -} =
+makeLogicEnvs impAvails thisModule spec dependencies =
     let unqualify s =
           if s == LH.qualifySymbol (symbol $ GHC.moduleName thisModule) (LH.dropModuleNames s) then
             LH.dropModuleNames s
@@ -500,8 +483,6 @@ makeLogicEnvs impAvails thisModule spec dependencies {- defnames -} =
               , HS.toList (opaqueReflects spec)
               , HS.toList (inlines spec)
               , HS.toList (hmeas spec)
---              , defnames
-              -- , map (fmap makeLocalLHName . lmVar) (defines spec)
               ]
             ]
           , [ val (msName m) | m <- measures spec ]
@@ -631,15 +612,11 @@ resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv p
         -- The name is local
       | elem s ss = return $ makeLocalLHName s
       | otherwise =
-        -- let s' = trace ("resolveLogicName s = " ++ show s) $ s in
-        case lookupInScopeNonReflectedEnv env s {- s' -} of
+        case lookupInScopeNonReflectedEnv env s of
           Left alts ->
             -- If names are not in the environment, they must be data constructors,
             -- or they must be reflected functions, or they must be in the logicmap.
-            -- let lmap0' = trace ("resolveLogicName lmap0 = " ++ show lmap0) $ lmap0
-            --     ls' = trace ("resolveLogicName ls = " ++ show ls) $ ls
-            --   in
-            case resolveDataConName ls {- ls' -} `mplus` resolveVarName lmap0 ls {- lmap0' ls' -} of
+            case resolveDataConName ls `mplus` resolveVarName lmap0 ls of
               Just m -> m
               Nothing
                 | elem s wiredInNames ->
@@ -726,10 +703,9 @@ resolveLogicNames cfg env globalRdrEnv unhandledNames lmap0 localVars lnameEnv p
     -- @InScopeNonReflectedEnv@ indicates where the reflect annotations were
     -- imported from, but not where the Haskell names were imported from.
     resolveVarName lmap s = do
-      -- let s' = trace ("resolveVarName s = " ++ show s) $ s
       let gres =
             GHC.lookupGRE globalRdrEnv $
-            mkLookupGRE (LHVarName LHAnyModuleNameF) (val s {- s'-})
+            mkLookupGRE (LHVarName LHAnyModuleNameF) (val s)
           refls = mapMaybe (findReflection . GHC.greName) gres
       case refls of
         [lhName] -> Just $ return lhName
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
index c9b0886160..4bb61d38ea 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
@@ -31,7 +31,6 @@ module Language.Haskell.Liquid.Types.Names
   , reflectGHCName
   , reflectLHName
   , updateLHNameSymbol
-  , qualifyLHName
   ) where
 
 import Control.DeepSeq
@@ -300,11 +299,6 @@ getLHGHCName :: LHName -> Maybe GHC.Name
 getLHGHCName (LHNResolved (LHRGHC n) _) = Just n
 getLHGHCName _ = Nothing
 
-qualifyLHName :: LHName -> Symbol
-qualifyLHName (LHNResolved (LHRGHC n) _) = qualifiedNameSymbol n
-qualifyLHName (LHNResolved _ s) = s
-qualifyLHName (LHNUnresolved _ s) = s
-
 mapLHNames :: Data a => (LHName -> LHName) -> a -> a
 mapLHNames f = go
   where
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PrettyPrint.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PrettyPrint.hs
index c2c78b20e0..4eeede09ed 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PrettyPrint.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PrettyPrint.hs
@@ -160,7 +160,7 @@ pprXOT k (x, v) = (xd, pprintTidy k v)
     xd          = maybe "unknown" (pprintTidy k) x
 
 instance (Ord v, F.Fixpoint v, PPrint v) => PPrint (LMapV v) where
-  pprintTidy _ (LMapV x xs e) = hcat [pprint x, pprint xs, text "|->", pprint e ]
+  pprintTidy _ (LMap x xs e) = hcat [pprint x, pprint xs, text "|->", pprint e ]
 
 instance PPrint LogicMap where
   pprintTidy _ (LM lm am) = vcat [ text "Logic Map"
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
index db8011d570..07e3647beb 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
@@ -988,7 +988,7 @@ toLiftedSpec a = LiftedSpec
   , liftedDsize      = dsize a
   , liftedBounds     = bounds a
   , liftedAxeqs      = S.fromList . axeqs $ a
-  , liftedDefines    = M.fromList . map (first (qualifyLHName . F.val)) . defines $ a
+  , liftedDefines    = M.fromList . map (first (lhNameToResolvedSymbol . F.val)) . defines $ a
   }
 
 -- This is a temporary internal function that we use to convert the input dependencies into a format
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
index a3fc132fc7..9abb9ca9a7 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
@@ -263,30 +263,29 @@ instance Monoid LogicMap where
 instance Semigroup LogicMap where
   LM x1 x2 <> LM y1 y2 = LM (M.union x1 y1) (M.union x2 y2)
 
-data LMapV v = LMapV
+data LMapV v = LMap
   { lmVar  :: F.LocSymbol
   , lmArgs :: [Symbol]
   , lmExpr :: F.ExprV v
   } deriving (Eq, Data, Generic, Functor)
-    deriving Hashable via Generically (LMapV v)
-    deriving Binary   via Generically (LMapV v)
+    deriving (Binary, Hashable) via Generically (LMapV v)
 type LMap = LMapV F.Symbol
 
 instance (Show v, Ord v, F.Fixpoint v) => Show (LMapV v) where
-  show (LMapV x xs e) = show x ++ " " ++ show xs ++ "\t |-> \t" ++ show e
+  show (LMap x xs e) = show x ++ " " ++ show xs ++ "\t |-> \t" ++ show e
 
 toLMapV' :: (F.Located LHName, ([Symbol], F.ExprV v)) -> (F.Located LHName, LMapV v)
-toLMapV' (x, (ys, e)) = (x, LMapV {lmVar = fmap getLHNameSymbol x, lmArgs = ys, lmExpr = e})
+toLMapV' (x, (ys, e)) = (x, LMap {lmVar = fmap getLHNameSymbol x, lmArgs = ys, lmExpr = e})
 
 toLMapV :: (F.LocSymbol, ([Symbol], F.ExprV v)) -> (Symbol, LMapV v)
-toLMapV (x, (ys, e)) = (F.val x, LMapV {lmVar = x, lmArgs = ys, lmExpr = e})
+toLMapV (x, (ys, e)) = (F.val x, LMap {lmVar = x, lmArgs = ys, lmExpr = e})
 
 toLogicMap :: [(F.LocSymbol, ([Symbol], Expr))] -> LogicMap
 toLogicMap ls = mempty {lmSymDefs = M.fromList $ map toLMapV ls}
 
 eAppWithMap :: LogicMap -> Symbol -> [Expr] -> Expr -> Expr
 eAppWithMap lmap f es expr
-  | Just (LMapV _ xs e) <- M.lookup f (lmSymDefs lmap)
+  | Just (LMap _ xs e) <- M.lookup f (lmSymDefs lmap)
   , length xs == length es
   = F.subst (F.mkSubst $ zip xs es) e
   | otherwise
@@ -384,7 +383,7 @@ mapRTAVars :: (a -> b) -> RTAlias a ty -> RTAlias b ty
 mapRTAVars f rt = rt { rtTArgs = f <$> rtTArgs rt }
 
 lmapEAlias :: LMap -> F.Located (RTAlias Symbol Expr)
-lmapEAlias (LMapV v ys e) = F.atLoc v (RTA (F.val v) [] ys e) -- (F.loc v) (F.loc v)
+lmapEAlias (LMap v ys e) = F.atLoc v (RTA (F.val v) [] ys e) -- (F.loc v) (F.loc v)
 
 
 -- | The type used during constraint generation, used

From 8960f824c554c471e30b7285a0ab279427598541 Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Wed, 18 Dec 2024 15:17:25 +0100
Subject: [PATCH 12/15] refactor

---
 .../src/Language/Haskell/Liquid/Bare.hs           |  2 +-
 .../src/Language/Haskell/Liquid/GHC/Plugin.hs     |  8 ++++++--
 .../Language/Haskell/Liquid/LHNameResolution.hs   |  7 ++++---
 .../src/Language/Haskell/Liquid/Parse.hs          |  2 +-
 .../src/Language/Haskell/Liquid/Types/Names.hs    |  3 +--
 .../src/Language/Haskell/Liquid/Types/Specs.hs    |  2 +-
 .../src/Language/Haskell/Liquid/Types/Types.hs    | 15 +++++++++------
 tests/pos/NumRefl.hs                              |  7 +------
 tests/tests.cabal                                 |  1 -
 9 files changed, 24 insertions(+), 23 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
index c2d3b7ad4d..16eb422a2c 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
@@ -64,6 +64,7 @@ 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 +107,6 @@ makeTargetSpec cfg localVars lnameEnv lmap targetSrc bareSpec dependencies = do
         Right (warns, ghcSpec) -> do
           let targetSpec = toTargetSpec ghcSpec
               liftedSpec = ghcSpecToLiftedSpec ghcSpec
-
           liftedSpec' <- removeUnexportedLocalAssumptions liftedSpec
           return $ Right (phaseOneWarns <> warns, targetSpec, liftedSpec')
 
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
index 60b99f599f..3c7ad9662c 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
@@ -543,8 +543,12 @@ processModule LiquidHaskellContext{..} = do
 
     tcg <- getGblEnv
     let localVars = Resolve.makeLocalVars preNormalizedCore
-        depsLogicMap = foldr (\ls lmp -> lmp <> mempty {lmSymDefs = HM.map (\l -> LH.lhNameToResolvedSymbol <$> l) $ liftedDefines ls}) mempty $
-                       (HM.elems . getDependencies) dependencies
+        -- add defines from dependencies to the logical map
+        depsLogicMap =
+          foldr (\ls lmp ->
+                     lmp <> mkLogicMap (HM.map (fmap LH.lhNameToResolvedSymbol) $ liftedDefines ls))
+                mempty $
+            (HM.elems . getDependencies) dependencies
         eBareSpec = resolveLHNames
           moduleCfg
           thisModule
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
index 5482ec8171..fbc2c19db1 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
@@ -157,9 +157,10 @@ 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 <> mempty {lmSymDefs = HM.fromList $ map (\(k , v) -> ( lhNameToResolvedSymbol $ F.val k
-                                                                                     , (fmap val v) { lmVar = lhNameToResolvedSymbol <$> 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
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
index 802cf1eef2..aca68c1745 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
@@ -1133,7 +1133,7 @@ mkSpec xs = Measure.Spec
   , Measure.ignores    = S.fromList [s | Ignore s <- xs]
   , Measure.autosize   = S.fromList [s | ASize  s <- xs]
   , Measure.axeqs      = []
-  , Measure.defines    = [ toLMapV' d | Define d <- xs]
+  , Measure.defines    = [ toLMapV d | Define d <- xs]
   }
 
 -- | Parse a single top level liquid specification
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
index 4bb61d38ea..f7e640800e 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Names.hs
@@ -43,9 +43,8 @@ import qualified Data.Text                               as Text
 import GHC.Generics
 import GHC.Show
 import GHC.Stack
-
 import Language.Fixpoint.Types
-import Language.Haskell.Liquid.GHC.Misc -- Symbolic GHC.Name
+import Language.Haskell.Liquid.GHC.Misc ( locNamedThing ) -- Symbolic GHC.Name
 import qualified Liquid.GHC.API as GHC
 
 -- RJ: Please add docs
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
index 07e3647beb..2e5e8564a4 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs
@@ -1034,5 +1034,5 @@ unsafeFromLiftedSpec a = Spec
   , dsize      = liftedDsize  a
   , bounds     = liftedBounds a
   , axeqs      = S.toList . liftedAxeqs $ a
-  , defines    = map (\p -> first (dummyLoc . makeLocalLHName) p) . M.toList . liftedDefines $ a
+  , defines    = map (first (dummyLoc . makeLocalLHName)) . M.toList . liftedDefines $ a
   }
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
index 9abb9ca9a7..beb7762aab 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Types.hs
@@ -128,7 +128,7 @@ module Language.Haskell.Liquid.Types.Types (
   , mapRTAVars
 
   -- * CoreToLogic
-  , LogicMap(..), toLMapV, toLMapV', toLogicMap, eAppWithMap, emapLMapM, LMapV(..), LMap
+  , LogicMap(..), toLMapV, mkLogicMap, toLogicMap, eAppWithMap, emapLMapM, LMapV(..), LMap
 
   -- * Refined Instances
   , RDEnv, DEnv(..), RInstance(..), RISig(..)
@@ -274,14 +274,17 @@ type LMap = LMapV F.Symbol
 instance (Show v, Ord v, F.Fixpoint v) => Show (LMapV v) where
   show (LMap x xs e) = show x ++ " " ++ show xs ++ "\t |-> \t" ++ show e
 
-toLMapV' :: (F.Located LHName, ([Symbol], F.ExprV v)) -> (F.Located LHName, LMapV v)
-toLMapV' (x, (ys, e)) = (x, LMap {lmVar = fmap getLHNameSymbol x, lmArgs = ys, lmExpr = e})
+toLMapV :: (F.Located LHName, ([Symbol], F.ExprV v)) -> (F.Located LHName, LMapV v)
+toLMapV (x, (ys, e)) = (x, LMap {lmVar = getLHNameSymbol <$> x, lmArgs = ys, lmExpr = e})
 
-toLMapV :: (F.LocSymbol, ([Symbol], F.ExprV v)) -> (Symbol, LMapV v)
-toLMapV (x, (ys, e)) = (F.val x, LMap {lmVar = x, lmArgs = ys, lmExpr = e})
+mkLogicMap :: M.HashMap Symbol LMap -> LogicMap
+mkLogicMap ls = mempty {lmSymDefs = ls}
 
 toLogicMap :: [(F.LocSymbol, ([Symbol], Expr))] -> LogicMap
-toLogicMap ls = mempty {lmSymDefs = M.fromList $ map toLMapV ls}
+toLogicMap = mkLogicMap . M.fromList . map toLMapV0
+  where
+  toLMapV0 :: (F.LocSymbol, ([Symbol], F.ExprV v)) -> (Symbol, LMapV v)
+  toLMapV0 (x, (ys, e)) = (F.val x, LMap {lmVar = x, lmArgs = ys, lmExpr = e})
 
 eAppWithMap :: LogicMap -> Symbol -> [Expr] -> Expr -> Expr
 eAppWithMap lmap f es expr
diff --git a/tests/pos/NumRefl.hs b/tests/pos/NumRefl.hs
index dce29b4e75..47425c1a84 100644
--- a/tests/pos/NumRefl.hs
+++ b/tests/pos/NumRefl.hs
@@ -1,8 +1,7 @@
 {-
 
 Without the
-  define GHC.Internal.Num.fromInteger x = (x)
-  define GHC.Num.Integer.IS x           = (x)
+  define fromInteger x = (x)
 
 this program crashes with:
 
@@ -21,10 +20,6 @@ Because the result type (Num p) => p cannot be decided to be a numeric type.
 module NumRefl where
 
 {-@ define fromInteger x = (x) @-}
--- {-@ define IS x          = (x) @-}
-
--- {-@ define GHC.Internal.Num.fromInteger x = (x) @-}
--- {-@ define GHC.Num.Integer.IS x           = (x) @-}
 
 {-@ reflect toNum @-}
 toNum :: Num p => () -> p
diff --git a/tests/tests.cabal b/tests/tests.cabal
index 7e70da6fb3..9e15d4ada3 100644
--- a/tests/tests.cabal
+++ b/tests/tests.cabal
@@ -1863,7 +1863,6 @@ executable unit-pos-3
 
     other-modules:
                       NumRefl
---                    , WithProofRefl
                     , Streams
                     , StrictPair0
                     , StrictPair1

From f502dd0689f3b7561972dece3e8e7b11a402c9e2 Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Wed, 18 Dec 2024 16:43:14 +0100
Subject: [PATCH 13/15] cleanup; add tests and docs

---
 docs/mkDocs/docs/options.md                   | 33 ++++++++--
 .../src/Language/Haskell/Liquid/GHC/Plugin.hs |  6 +-
 .../Haskell/Liquid/LHNameResolution.hs        | 62 ++++++++++---------
 .../src/Language/Haskell/Liquid/Parse.hs      |  2 +-
 .../benchmarks/popl18/ple/pos/Unification.hs  |  1 -
 tests/neg/MyBag.hs                            | 14 +++++
 tests/neg/MyBagDefine.hs                      | 16 +++++
 tests/ple/pos/Isort_erase.hs                  | 21 ++++++-
 tests/pos/MyBag.hs                            | 14 +++++
 tests/pos/MyBagDefine.hs                      | 12 ++++
 tests/pos/NumRefl1.hs                         | 12 ++++
 tests/tests.cabal                             |  7 ++-
 12 files changed, 157 insertions(+), 43 deletions(-)
 create mode 100644 tests/neg/MyBag.hs
 create mode 100644 tests/neg/MyBagDefine.hs
 create mode 100644 tests/pos/MyBag.hs
 create mode 100644 tests/pos/MyBagDefine.hs
 create mode 100644 tests/pos/NumRefl1.hs

diff --git a/docs/mkDocs/docs/options.md b/docs/mkDocs/docs/options.md
index a8c96fb9fd..f4d06a87be 100644
--- a/docs/mkDocs/docs/options.md
+++ b/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)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
index 3c7ad9662c..ddebec0a33 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
@@ -544,10 +544,10 @@ 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
@@ -555,7 +555,7 @@ processModule LiquidHaskellContext{..} = do
           localVars
           (imp_mods $ tcg_imports tcg)
           (tcg_rdr_env tcg)
-          (lhModuleLogicMap <> depsLogicMap)
+          logicMapWithDeps
           bareSpec0
           dependencies
     result <-
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
index fbc2c19db1..f014ea7e3b 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
+++ b/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
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
index aca68c1745..cb813b4c43 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs
+++ b/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
diff --git a/tests/benchmarks/popl18/ple/pos/Unification.hs b/tests/benchmarks/popl18/ple/pos/Unification.hs
index 7d1e8db0f9..4a2ba626bb 100644
--- a/tests/benchmarks/popl18/ple/pos/Unification.hs
+++ b/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 } @-}
diff --git a/tests/neg/MyBag.hs b/tests/neg/MyBag.hs
new file mode 100644
index 0000000000..9f7ae1b44c
--- /dev/null
+++ b/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)
diff --git a/tests/neg/MyBagDefine.hs b/tests/neg/MyBagDefine.hs
new file mode 100644
index 0000000000..a43b651618
--- /dev/null
+++ b/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)
diff --git a/tests/ple/pos/Isort_erase.hs b/tests/ple/pos/Isort_erase.hs
index 1e5c4eddff..c47eabfaaa 100644
--- a/tests/ple/pos/Isort_erase.hs
+++ b/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
diff --git a/tests/pos/MyBag.hs b/tests/pos/MyBag.hs
new file mode 100644
index 0000000000..9f7ae1b44c
--- /dev/null
+++ b/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)
diff --git a/tests/pos/MyBagDefine.hs b/tests/pos/MyBagDefine.hs
new file mode 100644
index 0000000000..193b22e092
--- /dev/null
+++ b/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)
diff --git a/tests/pos/NumRefl1.hs b/tests/pos/NumRefl1.hs
new file mode 100644
index 0000000000..bb9ba20681
--- /dev/null
+++ b/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
+
diff --git a/tests/tests.cabal b/tests/tests.cabal
index 9e15d4ada3..c0a3838534 100644
--- a/tests/tests.cabal
+++ b/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

From f84a7e84cdb27b1a17ac84606d497ec5553884e9 Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Wed, 18 Dec 2024 20:58:10 +0100
Subject: [PATCH 14/15] fix neg test

---
 tests/neg/MyBagDefine.hs | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/tests/neg/MyBagDefine.hs b/tests/neg/MyBagDefine.hs
index a43b651618..3b33b04489 100644
--- a/tests/neg/MyBagDefine.hs
+++ b/tests/neg/MyBagDefine.hs
@@ -10,7 +10,3 @@ import Data.Set
 {-@ 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)

From b008f8401ec8f3e71e2c8a0d422d3c94f74ea5e6 Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Thu, 19 Dec 2024 16:27:50 +0100
Subject: [PATCH 15/15] move more defines out of CoreToLogic

---
 .../Haskell/Liquid/GHC/CoreToLogic.hs         | 30 -------------------
 src/Data/Set_LHAssumptions.hs                 | 21 +++++++++++++
 src/GHC/CString_LHAssumptions.hs              |  2 ++
 src/GHC/Real_LHAssumptions.hs                 |  5 ++++
 4 files changed, 28 insertions(+), 30 deletions(-)

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
index af3189eabd..2a74678fcd 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/CoreToLogic.hs
@@ -3,42 +3,12 @@ module Language.Haskell.Liquid.GHC.CoreToLogic where
 coreToLogic :: String
 coreToLogic = unlines
   [ "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)"
-  , "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)"
   ]
diff --git a/src/Data/Set_LHAssumptions.hs b/src/Data/Set_LHAssumptions.hs
index f95db559d0..22e7dc97d7 100644
--- a/src/Data/Set_LHAssumptions.hs
+++ b/src/Data/Set_LHAssumptions.hs
@@ -3,6 +3,7 @@
 module Data.Set_LHAssumptions where
 
 import Data.Set
+import Data.Set.Internal as I
 import GHC.Types_LHAssumptions()
 import Prelude hiding (null)
 
@@ -38,4 +39,24 @@ measure listElts :: [a] -> Set a
   listElts []     = {v | (Set_emp v)}
   listElts (x:xs) = {v | v = Set_cup (Set_sng x) (listElts xs) }
 
+define singleton x      = (Set_sng x)
+define union x y        = (Set_cup x y)
+define intersection x y = (Set_cap x y)
+define difference x y   = (Set_dif x y)
+define empty            = (Set_empty 0)
+define null x           = (Set_emp x)
+define member x xs      = (Set_mem x xs)
+define isSubsetOf x y   = (Set_sub x y)
+define fromList xs      = (Data.Set_LHAssumptions.listElts xs)
+
+define I.singleton x      = (Set_sng x)
+define I.union x y        = (Set_cup x y)
+define I.intersection x y = (Set_cap x y)
+define I.difference x y   = (Set_dif x y)
+define I.empty            = (Set_empty 0)
+define I.null x           = (Set_emp x)
+define I.member x xs      = (Set_mem x xs)
+define I.isSubsetOf x y   = (Set_sub x y)
+define I.fromList xs      = (Data.Set_LHAssumptions.listElts xs)
+
 @-}
diff --git a/src/GHC/CString_LHAssumptions.hs b/src/GHC/CString_LHAssumptions.hs
index d41a028b99..0f7ef6f04f 100644
--- a/src/GHC/CString_LHAssumptions.hs
+++ b/src/GHC/CString_LHAssumptions.hs
@@ -14,4 +14,6 @@ _f = unpackCString#
 assume GHC.CString.unpackCString#
   :: x:Addr#
   -> {v:[Char] | v ~~ x && len v == strLen x}
+
+define GHC.CString.unpackCString# x = x
 @-}
diff --git a/src/GHC/Real_LHAssumptions.hs b/src/GHC/Real_LHAssumptions.hs
index 0e9e1389bf..18a05479ff 100644
--- a/src/GHC/Real_LHAssumptions.hs
+++ b/src/GHC/Real_LHAssumptions.hs
@@ -46,4 +46,9 @@ class (Real a, Enum a) => Integral a where
 
 //  fixpoint can't handle (x mod y), only (x mod c) so we need to be more clever here
 //  mod :: x:a -> y:a -> {v:a | v = (x mod y) }
+
+define div x y        = (x / y)
+define mod x y        = (x mod y)
+define fromIntegral x = (x)
+
 @-}