Merge pull request #2469 from ucsd-progsys/fd/lmap-cleanups

Initialize the logic map in resolveLHNames
ucsd-progsys · Jan 10, 2025 · 1e5781e · 1e5781e
2 parents d13f9d3 + 7e14f94
commit 1e5781e
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 14 deletions.
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
@@ -24,7 +24,6 @@ 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
@@ -375,14 +374,11 @@ processInputSpec cfg pipelineData modSummary inputSpec = do
   debugLog $ " Input spec: \n" ++ show (fromBareSpecParsed inputSpec)
   debugLog $ "Direct ===> \n" ++ unlines (renderModule <$> directImports tcg)
 
-  let logicMap = LH.listLMap
-
   -- debugLog $ "Logic map:\n" ++ show logicMap
 
   let lhContext = LiquidHaskellContext {
         lhGlobalCfg       = cfg
       , lhInputSpec       = inputSpec
-      , lhModuleLogicMap  = logicMap
       , lhModuleSummary   = modSummary
       , lhModuleTcData    = pdTcData pipelineData
       , lhModuleGuts      = pdUnoptimisedCore pipelineData
@@ -488,7 +484,6 @@ loadDependencies currentModuleConfig mods = do
 data LiquidHaskellContext = LiquidHaskellContext {
     lhGlobalCfg        :: Config
   , lhInputSpec        :: BareSpecParsed
-  , lhModuleLogicMap   :: LogicMap
   , lhModuleSummary    :: ModSummary
   , lhModuleTcData     :: TcData
   , lhModuleGuts       :: ModGuts
@@ -543,19 +538,12 @@ processModule LiquidHaskellContext{..} = do
 
     tcg <- getGblEnv
     let localVars = Resolve.makeLocalVars preNormalizedCore
-        -- add defines from dependencies to the logical map
-        logicMapWithDeps =
-          foldr (\ls lmp ->
-                     lmp <> mkLogicMap (HM.map (fmap LH.lhNameToResolvedSymbol) $ liftedDefines ls))
-                lhModuleLogicMap $
-            (HM.elems . getDependencies) dependencies
         eBareSpec = resolveLHNames
           moduleCfg
           thisModule
           localVars
           (imp_mods $ tcg_imports tcg)
           (tcg_rdr_env tcg)
-          logicMapWithDeps
           bareSpec0
           dependencies
     result <-

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
@@ -56,6 +56,7 @@ module Language.Haskell.Liquid.LHNameResolution
   ) where
 
 import qualified Liquid.GHC.API         as GHC hiding (Expr, panic)
+import qualified Language.Haskell.Liquid.GHC.Interface   as LH
 import qualified Language.Haskell.Liquid.GHC.Misc        as LH
 import           Language.Haskell.Liquid.Types.Names
 import           Language.Haskell.Liquid.Types.RType
@@ -134,11 +135,10 @@ resolveLHNames
   -> LocalVars
   -> GHC.ImportedMods
   -> GHC.GlobalRdrEnv
-  -> LogicMap
   -> BareSpecParsed
   -> TargetDependencies
   -> Either [Error] (BareSpec, LogicNameEnv, LogicMap)
-resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 dependencies = do
+resolveLHNames cfg thisModule localVars impMods globalRdrEnv bareSpec0 dependencies = do
     let ((bs, logicNameEnv, lmap2), (es, ns)) =
           flip runState mempty $ do
             -- A generic traversal that resolves names of Haskell entities
@@ -189,6 +189,14 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv lmap bareSpec0 depe
     taliases = collectTypeAliases thisModule bareSpec0 dependencies
     allEaliases = collectExprAliases bareSpec0 dependencies
 
+    -- add defines from dependencies to the logical map
+    lmap =
+      foldr (\ls lmp ->
+                 lmp <> mkLogicMap (HM.map (fmap lhNameToResolvedSymbol) $ liftedDefines ls)
+            )
+            LH.listLMap $
+            (HM.elems . getDependencies) dependencies
+
     resolveFieldLogicName n =
       case n of
         LHNUnresolved LHLogicNameBinder s -> pure $ makeLogicLHName s thisModule Nothing