Skip to content

Commit

Permalink
Merge pull request #2479 from ucsd-progsys/fd/prune-old-name-resolution
Browse files Browse the repository at this point in the history
Remove the unneeded old symbol resolution
facundominguez authored Jan 27, 2025

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
2 parents 06f55b4 + 35c6c69 commit be7fb6d
Showing 10 changed files with 38 additions and 339 deletions.
52 changes: 14 additions & 38 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
Original file line number Diff line number Diff line change
@@ -208,7 +208,7 @@ makeGhcSpec0
makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec dependencySpecs = do
globalRdrEnv <- Ghc.tcg_rdr_env <$> Ghc.getGblEnv
-- build up environments
tycEnv <- makeTycEnv1 name env (tycEnv0, datacons) coreToLg simplifier
tycEnv <- makeTycEnv1 env (tycEnv0, datacons) coreToLg simplifier
let tyi = Bare.tcTyConMap tycEnv
let sigEnv = makeSigEnv embs tyi (_gsExports src) rtEnv
let lSpec1 = makeLiftedSpec1 cfg src tycEnv lmap mySpec1
@@ -386,13 +386,12 @@ makeLiftedSpec0 :: Config -> GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareS
-> Ms.BareSpec
makeLiftedSpec0 cfg src embs lmap mySpec = mempty
{ Ms.ealiases = lmapEAlias . snd <$> Bare.makeHaskellInlines cfg src embs lmap mySpec
, Ms.dataDecls = Bare.makeHaskellDataDecls cfg name mySpec tcs
, Ms.dataDecls = Bare.makeHaskellDataDecls cfg mySpec tcs
}
where
tcs = uniqNub (_gsTcs src ++ refTcs)
refTcs = reflectedTyCons cfg embs cbs mySpec
cbs = _giCbs src
name = _giTargetMod src

uniqNub :: (Ghc.Uniquable a) => [a] -> [a]
uniqNub xs = M.elems $ M.fromList [ (index x, x) | x <- xs ]
@@ -448,13 +447,16 @@ makeSpecVars :: Config -> GhcSrc -> Ms.BareSpec -> Bare.Env -> Bare.MeasEnv
-> Bare.Lookup GhcSpecVars
------------------------------------------------------------------------------------------
makeSpecVars cfg src mySpec env measEnv = do
tgtVars <- mapM (resolveStringVar env name) (checks cfg)
let tgtVars = Mb.mapMaybe (`M.lookup` hvars) (checks cfg)
igVars <- sMapM (Bare.lookupGhcIdLHName env) (Ms.ignores mySpec)
lVars <- sMapM (Bare.lookupGhcIdLHName env) (Ms.lvars mySpec)
return (SpVar tgtVars igVars lVars cMethods)
where
name = _giTargetMod src
cMethods = snd3 <$> Bare.meMethods measEnv
hvars = M.fromList
[ (Ghc.occNameString $ Ghc.getOccName b, b)
| b <- Ghc.bindersOfBinds (_giCbs src)
]

sMapM :: (Monad m, Eq b, Hashable b) => (a -> m b) -> S.HashSet a -> m (S.HashSet b)
sMapM f xSet = do
@@ -464,16 +466,6 @@ sMapM f xSet = do
sForM :: (Monad m, Eq b, Hashable b) =>S.HashSet a -> (a -> m b) -> m (S.HashSet b)
sForM xs f = sMapM f xs

qualifySymbolic :: (F.Symbolic a) => ModName -> a -> F.Symbol
qualifySymbolic name s = GM.qualifySymbol (F.symbol name) (F.symbol s)

resolveStringVar :: Bare.Env -> ModName -> String -> Bare.Lookup Ghc.Var
resolveStringVar env name s = Bare.lookupGhcVar env name "resolve-string-var" lx
where
lx = dummyLoc (qualifySymbolic name s)



------------------------------------------------------------------------------------------
makeSpecQual
:: Config
@@ -980,11 +972,8 @@ getAsmSigs myName name spec
| otherwise =
[ (False, x, t)
| (x, t) <- Ms.asmSigs spec
++ map (first (fmap (updateLHNameSymbol qSym))) (Ms.sigs spec)
++ Ms.sigs spec
]
where
qSym = GM.qualifySymbol ns
ns = F.symbol name

makeSigEnv :: F.TCEmb Ghc.TyCon -> Bare.TyConMap -> S.HashSet StableName -> BareRTEnv -> Bare.SigEnv
makeSigEnv embs tyi exports rtEnv = Bare.SigEnv
@@ -1173,8 +1162,8 @@ makeTycEnv0 cfg myName env embs mySpec iSpecs = (diag0 <> diag1, datacons, Bare.
tyi = makeTyConInfo embs fiTcs tycons
-- tycons = F.tracepp "TYCONS" $ Misc.replaceWith tcpCon tcs wiredTyCons
-- datacons = Bare.makePluggedDataCons embs tyi (Misc.replaceWith (dcpCon . val) (F.tracepp "DATACONS" $ concat dcs) wiredDataCons)
tycons = tcs ++ knownWiredTyCons env myName
datacons = Bare.makePluggedDataCon (typeclass cfg) embs tyi <$> (concat dcs ++ knownWiredDataCons env myName)
tycons = tcs ++ wiredTyCons
datacons = Bare.makePluggedDataCon (typeclass cfg) embs tyi <$> (concat dcs ++ wiredDataCons)
tds = [(name, tcpCon tcp, dd) | (name, tcp, Just dd) <- tcDds]
(diag1, adts) = Bare.makeDataDecls cfg embs myName tds datacons
dm = Bare.dataConMap adts
@@ -1184,35 +1173,22 @@ makeTycEnv0 cfg myName env embs mySpec iSpecs = (diag0 <> diag1, datacons, Bare.


makeTycEnv1 ::
ModName
-> Bare.Env
Bare.Env
-> (Bare.TycEnv, [Located DataConP])
-> (Ghc.CoreExpr -> F.Expr)
-> (Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr)
-> Ghc.TcRn Bare.TycEnv
makeTycEnv1 myName env (tycEnv, datacons) coreToLg simplifier = do
makeTycEnv1 env (tycEnv, datacons) coreToLg simplifier = do
-- fst for selector generation, snd for dataconsig generation
lclassdcs <- forM classdcs $ traverse (Bare.elaborateClassDcp coreToLg simplifier)
let recSelectors = Bare.makeRecordSelectorSigs env myName (dcs ++ (fmap . fmap) snd lclassdcs)
let recSelectors = Bare.makeRecordSelectorSigs env (dcs ++ (fmap . fmap) snd lclassdcs)
pure $
tycEnv {Bare.tcSelVars = recSelectors, Bare.tcDataCons = F.val <$> ((fmap . fmap) fst lclassdcs ++ dcs )}
where
(classdcs, dcs) =
L.partition
(Ghc.isClassTyCon . Ghc.dataConTyCon . dcpCon . F.val) datacons


knownWiredDataCons :: Bare.Env -> ModName -> [Located DataConP]
knownWiredDataCons env name = filter isKnown wiredDataCons
where
isKnown = Bare.knownGhcDataCon env name . GM.namedLocSymbol . dcpCon . val

knownWiredTyCons :: Bare.Env -> ModName -> [TyConP]
knownWiredTyCons env name = filter isKnown wiredTyCons
where
isKnown = Bare.knownGhcTyCon env name . GM.namedLocSymbol . tcpCon


-- REBARE: formerly, makeGhcCHOP2
-------------------------------------------------------------------------------------------
makeMeasEnv :: Bare.Env -> Bare.TycEnv -> Bare.SigEnv -> Bare.ModSpecs ->
@@ -1299,7 +1275,7 @@ addOpaqueReflMeas cfg tycEnv env spec measEnv specs eqs = do
, shouldBeUsedForScanning $ makeGHCLHName (Ghc.getName v) (symbol v)
]
tcs = S.toList $ Ghc.dataConTyCon `S.map` Bare.getReflDCs measEnv varsUsedForTcScanning
dataDecls = Bare.makeHaskellDataDecls cfg name spec tcs
dataDecls = Bare.makeHaskellDataDecls cfg spec tcs
tyi = Bare.tcTyConMap tycEnv
embs = Bare.tcEmbs tycEnv
dm = Bare.tcDataConMap tycEnv
Original file line number Diff line number Diff line change
@@ -775,8 +775,8 @@ unDummy :: F.Symbol -> Int -> F.Symbol
unDummy x i | x /= F.dummySymbol = x
| otherwise = F.symbol ("_cls_lq" ++ show i)

makeRecordSelectorSigs :: Bare.Env -> ModName -> [Located DataConP] -> [(Ghc.Var, LocSpecType)]
makeRecordSelectorSigs env name = checkRecordSelectorSigs . concatMap makeOne
makeRecordSelectorSigs :: Bare.Env -> [Located DataConP] -> [(Ghc.Var, LocSpecType)]
makeRecordSelectorSigs env = checkRecordSelectorSigs . concatMap makeOne
where
makeOne (Loc l l' dcp)
| Just cls <- maybe_cls
@@ -793,7 +793,7 @@ makeRecordSelectorSigs env name = checkRecordSelectorSigs . concatMap makeOne
maybe_cls = Ghc.tyConClass_maybe (Ghc.dataConTyCon dc)
dc = dcpCon dcp
fls = Ghc.dataConFieldLabels dc
fs = Bare.lookupGhcNamedVar env name . Ghc.flSelector <$> fls
fs = Bare.lookupGhcId env . Ghc.flSelector <$> fls
ts :: [ LocSpecType ]
ts = [ Loc l l' (mkArrow (map (, mempty) (makeRTVar <$> dcpFreeTyVars dcp)) []
[(z, classRFInfo True, res, mempty)]
22 changes: 8 additions & 14 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
Original file line number Diff line number Diff line change
@@ -160,14 +160,14 @@ coreToFun' cfg embs dmMb lmap x v defn ok = either Ex.throw ok act


-------------------------------------------------------------------------------
makeHaskellDataDecls :: Config -> ModName -> Ms.BareSpec -> [Ghc.TyCon]
makeHaskellDataDecls :: Config -> Ms.BareSpec -> [Ghc.TyCon]
-> [DataDecl]
--------------------------------------------------------------------------------
makeHaskellDataDecls cfg name spec tcs
makeHaskellDataDecls cfg spec tcs
| exactDCFlag cfg = Bare.dataDeclSize spec
. Mb.mapMaybe tyConDataDecl
-- . F.tracepp "makeHaskellDataDecls-3"
. zipMap (hasDataDecl name spec . fst)
. zipMap (hasDataDecl spec . fst)
-- . F.tracepp "makeHaskellDataDecls-2"
. liftableTyCons
-- . F.tracepp "makeHaskellDataDecls-1"
@@ -195,21 +195,15 @@ zipMap f xs = zip xs (map f xs)
zipMapMaybe :: (a -> Maybe b) -> [a] -> [(a, b)]
zipMapMaybe f = Mb.mapMaybe (\x -> (x, ) <$> f x)

hasDataDecl :: ModName -> Ms.BareSpec -> Ghc.TyCon -> HasDataDecl
hasDataDecl modName spec
= \tc -> F.notracepp (msg tc) $ M.lookupDefault defn (tcName tc) decls
hasDataDecl :: Ms.BareSpec -> Ghc.TyCon -> HasDataDecl
hasDataDecl spec
= \tc -> F.notracepp (msg tc) $ M.lookupDefault defn (tyConDataName tc) decls
where
msg tc = "hasDataDecl " ++ show (tcName tc)
msg tc = "hasDataDecl " ++ show (tyConDataName tc)
defn = NoDecl Nothing
tcName = fmap (qualifiedDataName modName) . tyConDataName
dcName = qualifiedDataName modName . tycName
decls = M.fromList [ (Just dn, hasDecl d)
| d <- Ms.dataDecls spec
, let dn = dcName d]

qualifiedDataName :: ModName -> DataName -> DataName
qualifiedDataName modName (DnName lx) = DnName (updateLHNameSymbol (qualifyModName modName) <$> lx)
qualifiedDataName modName (DnCon lx) = DnCon (updateLHNameSymbol (qualifyModName modName) <$> lx)
, let dn = tycName d]

{-tyConDataDecl :: {tc:TyCon | isAlgTyCon tc} -> Maybe DataDecl @-}
tyConDataDecl :: ((Ghc.TyCon, DataName), HasDataDecl) -> Maybe DataDecl
Loading

0 comments on commit be7fb6d

Please sign in to comment.