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.

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

Remove the unneeded old symbol resolution #2479

Merged
merged 14 commits into from
Jan 27, 2025
Merged
52 changes: 14 additions & 38 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 ]
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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 ->
Expand Down Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)]
Expand Down
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
Expand Up @@ -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"
Expand Down Expand Up @@ -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
Expand Down
Loading
Loading