Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Initialize the logic map in resolveLHNames #2469

Merged
merged 2 commits into from
Jan 10, 2025
+10 −14
Merged

Initialize the logic map in resolveLHNames #2469

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
30ed007
Eliminate redundant field lhModuleLogicMap
facundominguez Jan 9, 2025
7e14f94
Build the initial logic map in resolveLHNames
facundominguez Jan 9, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 0 additions & 12 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -488,7 +484,6 @@ loadDependencies currentModuleConfig mods = do
data LiquidHaskellContext = LiquidHaskellContext {
lhGlobalCfg :: Config
, lhInputSpec :: BareSpecParsed
, lhModuleLogicMap :: LogicMap
, lhModuleSummary :: ModSummary
, lhModuleTcData :: TcData
, lhModuleGuts :: ModGuts
Expand Down Expand Up @@ -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 <-
Expand Down
12 changes: 10 additions & 2 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
Loading