Skip to content

Commit

Permalink
Merge pull request #2411 from ucsd-progsys/fd/ghc-names-2
Browse files Browse the repository at this point in the history
Use LHNames for names of data cons and adts
  • Loading branch information
facundominguez authored Oct 25, 2024
2 parents 7fb9dc3 + 158cc43 commit d1fe5a0
Show file tree
Hide file tree
Showing 16 changed files with 148 additions and 110 deletions.
2 changes: 1 addition & 1 deletion liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1047,7 +1047,7 @@ makeNewTypes env sigEnv specs = do
makeNewType :: Bare.Env -> Bare.SigEnv -> ModName -> DataDecl ->
Bare.Lookup [(Ghc.TyCon, LocSpecType)]
makeNewType env sigEnv name d = do
tcMb <- Bare.lookupGhcDnTyCon env name "makeNewType" tcName
tcMb <- Bare.lookupGhcDnTyCon env name tcName
case tcMb of
Just tc -> return [(tc, lst)]
_ -> return []
Expand Down
40 changes: 22 additions & 18 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,7 @@ import qualified Language.Haskell.Liquid.Measure as Ms
import qualified Language.Haskell.Liquid.Bare.Types as Bare
import qualified Language.Haskell.Liquid.Bare.Resolve as Bare
import Language.Haskell.Liquid.UX.Config
import qualified Text.PrettyPrint.HughesPJ as PJ
import Text.Printf (printf)
import Text.PrettyPrint ((<+>))

Expand Down Expand Up @@ -221,7 +222,9 @@ makeDataDecls cfg tce name tds ds
| otherwise = (mempty, [])
where
makeDecls = exactDCFlag cfg && not (noADT cfg)
warns = (mkWarnDecl . fst . fst . snd <$> badTcs) ++ (mkWarnDecl <$> badDecs)
warns =
(mkWarnDecl . fmap pprint . dataNameSymbol . tycName . fst . fst . snd <$> badTcs) ++
(mkWarnDecl . (\d -> F.atLoc d (pprint $ F.symbol d)) <$> badDecs)
tds' = resolveTyCons name tds
tcDds = filter ((/= Ghc.listTyCon) . fst)
$ groupDataCons tds' ds
Expand All @@ -239,8 +242,8 @@ checkRegularData ds = (oks, badDs)
badSyms = {- F.notracepp "BAD-Data" . -} S.fromList . fmap F.symbol $ badDs
oks = [ d | d <- ds, not (S.member (F.symbol d) badSyms) ]

mkWarnDecl :: (F.Loc a, F.Symbolic a) => a -> Warning
mkWarnDecl d = mkWarning (GM.fSrcSpan d) ("Non-regular data declaration" <+> pprint (F.symbol d))
mkWarnDecl :: Located PJ.Doc -> Warning
mkWarnDecl d = mkWarning (GM.fSrcSpan d) ("Non-regular data declaration" <+> val d)


-- [NOTE:Orphan-TyCons]
Expand Down Expand Up @@ -408,7 +411,7 @@ makeConTypes' _myName env (name, spec) = makeConTypes'' env name spec dcs vdcs

-- Essentially transforms the data declarations into LH's enhanced types for type constructors and
-- data constructors
makeConTypes'' :: Bare.Env -> ModName -> Ms.BareSpec -> [DataDecl] -> [(F.LocSymbol, [Variance])]
makeConTypes'' :: Bare.Env -> ModName -> Ms.BareSpec -> [DataDecl] -> [(F.Located LHName, [Variance])]
-> Bare.Lookup ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
makeConTypes'' env name spec dcs vdcs = do
dcs' <- canonizeDecls env name dcs
Expand All @@ -418,11 +421,11 @@ makeConTypes'' env name spec dcs vdcs = do
return (unzip zong)


type DSizeMap = M.HashMap F.Symbol (F.Symbol, [LHName])
type DSizeMap = M.HashMap LHName (F.Symbol, [LHName])
normalizeDSize :: [([LocBareType], F.LocSymbol)] -> DSizeMap
normalizeDSize ds = M.fromList (concatMap go ds)
where go (ts,x) = let xs = Mb.mapMaybe (getTc . val) ts
in [(getLHNameSymbol tc, (val x, xs)) | tc <- xs]
in [(tc, (val x, xs)) | tc <- xs]
getTc (RAllT _ t _) = getTc t
getTc (RApp c _ _ _) = Just (val $ btc_tc c)
getTc _ = Nothing
Expand All @@ -434,7 +437,7 @@ dataDeclSize spec dcs = makeSize smap <$> dcs

makeSize :: DSizeMap -> DataDecl -> DataDecl
makeSize smap d
| Just p <- M.lookup (F.symbol $ tycName d) smap
| Just p <- M.lookup (val $ dataNameSymbol $ tycName d) smap
= d {tycDCons = fmap (fmap (makeSizeCtor p)) (tycDCons d) }
| otherwise
= d
Expand Down Expand Up @@ -492,7 +495,7 @@ canonizeDecls env name dataDecls = do

dataDeclKey :: Bare.Env -> ModName -> DataDecl -> Bare.Lookup (Maybe F.Symbol)
dataDeclKey env name d = do
tcMb <- Bare.lookupGhcDnTyCon env name "canonizeDecls" (tycName d)
tcMb <- Bare.lookupGhcDnTyCon env name (tycName d)
case tcMb of
Nothing ->
return Nothing
Expand Down Expand Up @@ -520,11 +523,11 @@ checkDataCtors env name c dd (Just cons) = do
dcs = S.fromList . fmap F.symbol . Ghc.tyConDataCons $ c

-- The data constructors in the spec (which we have to qualify for them to match the GHC data constructors)
mbDcs <- mapM (Bare.failMaybe env name . Bare.lookupGhcDataCon env name "checkDataCtors" . dcName) cons
mbDcs <- mapM (Bare.failMaybe env name . Bare.lookupGhcDataConLHName env . dcName) cons
let rdcs = S.fromList . fmap F.symbol . Mb.catMaybes $ mbDcs
if dcs == rdcs
then mapM checkDataCtorDupField cons
else Left [errDataConMismatch (dataNameSymbol (tycName dd)) dcs rdcs]
else Left [errDataConMismatch (getLHNameSymbol <$> dataNameSymbol (tycName dd)) dcs rdcs]

-- | Checks whether the given data constructor has duplicate fields.
--
Expand All @@ -545,17 +548,18 @@ selectDD (_, ds) = case [ d | d <- ds, tycKind d == DataReflected ] of
_ -> Left ds

groupVariances :: [DataDecl]
-> [(LocSymbol, [Variance])]
-> [(Maybe DataDecl, Maybe (LocSymbol, [Variance]))]
-> [(Located LHName, [Variance])]
-> [(Maybe DataDecl, Maybe (Located LHName, [Variance]))]
groupVariances dcs vdcs = merge (L.sort dcs) (L.sortBy (\x y -> compare (fst x) (fst y)) vdcs)
where
merge (d:ds) (v:vs)
| F.symbol d == sym v = (Just d, Just v) : merge ds vs
| F.symbol d < sym v = (Just d, Nothing) : merge ds (v:vs)
| ddName d == sym v = (Just d, Just v) : merge ds vs
| ddName d < sym v = (Just d, Nothing) : merge ds (v:vs)
| otherwise = (Nothing, Just v) : merge (d:ds) vs
merge [] vs = (Nothing,) . Just <$> vs
merge ds [] = (,Nothing) . Just <$> ds
sym = val . fst
ddName = val . dataNameSymbol . tycName


-- | 'checkDataDecl' checks that the supplied DataDecl is indeed a refinement
Expand All @@ -573,15 +577,15 @@ checkDataDecl c d = F.notracepp _msg (isGADT || cN == dN || null (tycDCons d))

getDnTyCon :: Bare.Env -> ModName -> DataName -> Bare.Lookup Ghc.TyCon
getDnTyCon env name dn = do
tcMb <- Bare.lookupGhcDnTyCon env name "ofBDataDecl-1" dn
tcMb <- Bare.lookupGhcDnTyCon env name dn
case tcMb of
Just tc -> return tc
Nothing -> Left [ ErrBadData (GM.fSrcSpan dn) (pprint dn) "Unknown Type Constructor" ]
-- ugh = impossible Nothing "getDnTyCon"


-- FIXME: ES: why the maybes?
ofBDataDecl :: Bare.Env -> ModName -> Maybe DataDecl -> Maybe (LocSymbol, [Variance])
ofBDataDecl :: Bare.Env -> ModName -> Maybe DataDecl -> Maybe (Located LHName, [Variance])
-> Bare.Lookup ( (ModName, TyConP, Maybe DataPropDecl), [Located DataConP] )
ofBDataDecl env name (Just dd@(DataDecl tc as ps cts pos sfun pt _)) maybe_invariance_info = do
let Loc lc lc' _ = dataNameSymbol tc
Expand All @@ -606,7 +610,7 @@ ofBDataDecl env name (Just dd@(DataDecl tc as ps cts pos sfun pt _)) maybe_invar
err = ErrBadData (GM.fSrcSpan tc) (pprint tc) "Mismatch in number of type variables"

ofBDataDecl env name Nothing (Just (tc, is)) =
case Bare.lookupGhcTyCon env name "ofBDataDecl-2" tc of
case Bare.matchTyCon env tc of
Left e -> Left e
Right tc' -> Right ((name, TyConP srcpos tc' [] [] tcov tcontr Nothing, Nothing), [])
where
Expand All @@ -628,7 +632,7 @@ ofBDataCtor :: Bare.Env
-> DataCtor
-> Bare.Lookup DataConP
ofBDataCtor env name l l' tc αs ps πs dc = do
c' <- Bare.lookupGhcDataCon env name "ofBDataCtor" (dcName dc)
c' <- Bare.lookupGhcDataConLHName env (dcName dc)
return (ofBDataCtorTc env name l l' tc αs ps πs dc c')

ofBDataCtorTc :: Bare.Env -> ModName -> F.SourcePos -> F.SourcePos ->
Expand Down
26 changes: 15 additions & 11 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@ import qualified Liquid.GHC.API as Ghc
import qualified Language.Haskell.Liquid.GHC.Misc as GM
import Language.Haskell.Liquid.Types.DataDecl
import Language.Haskell.Liquid.Types.Errors
import Language.Haskell.Liquid.Types.Names
import qualified Language.Haskell.Liquid.Types.RefType as RT
import Language.Haskell.Liquid.Types.RType
import Language.Haskell.Liquid.Types.RTypeOp
Expand Down Expand Up @@ -181,7 +182,7 @@ isReflectableTyCon = Ghc.isFamInstTyCon .||. Ghc.isVanillaAlgTyCon
liftableTyCons :: [Ghc.TyCon] -> [(Ghc.TyCon, DataName)]
liftableTyCons
= F.notracepp "LiftableTCs 3"
. zipMapMaybe (tyConDataName True)
. zipMapMaybe tyConDataName
. F.notracepp "LiftableTCs 2"
. filter (not . Ghc.isBoxedTupleTyCon)
. F.notracepp "LiftableTCs 1"
Expand All @@ -200,15 +201,19 @@ hasDataDecl modName spec
where
msg tc = "hasDataDecl " ++ show (tcName tc)
defn = NoDecl Nothing
tcName = fmap (qualifiedDataName modName) . tyConDataName True
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 (qualifyModName modName <$> lx)
qualifiedDataName modName (DnCon lx) = DnCon (qualifyModName modName <$> lx)
qualifiedDataName modName (DnName lx) = DnName (updateLHNameSymbol (qualifyModName modName) <$> lx)
qualifiedDataName modName (DnCon lx) = DnCon (updateLHNameSymbol (qualifyModName modName) <$> lx)

updateLHNameSymbol :: (F.Symbol -> F.Symbol) -> LHName -> LHName
updateLHNameSymbol f (LHNResolved n s) = LHNResolved n (f s)
updateLHNameSymbol f (LHNUnresolved n s) = LHNUnresolved n (f s)

{-tyConDataDecl :: {tc:TyCon | isAlgTyCon tc} -> Maybe DataDecl @-}
tyConDataDecl :: ((Ghc.TyCon, DataName), HasDataDecl) -> Maybe DataDecl
Expand All @@ -227,13 +232,12 @@ tyConDataDecl ((tc, dn), NoDecl szF)
}
where decls = map dataConDecl . Ghc.tyConDataCons

tyConDataName :: Bool -> Ghc.TyCon -> Maybe DataName
tyConDataName full tc
| vanillaTc = Just (DnName (post . F.symbol <$> GM.locNamedThing tc))
| d:_ <- dcs = Just (DnCon (post . F.symbol <$> GM.locNamedThing d ))
tyConDataName :: Ghc.TyCon -> Maybe DataName
tyConDataName tc
| vanillaTc = Just (DnName ((\x -> lhNameFromGHCName (Ghc.getName x) (F.symbol x)) <$> GM.locNamedThing tc))
| d:_ <- dcs = Just (DnCon ((\x -> lhNameFromGHCName (Ghc.getName x) (F.symbol x)) <$> GM.locNamedThing d ))
| otherwise = Nothing
where
post = if full then id else GM.dropModuleNamesAndUnique
vanillaTc = Ghc.isVanillaAlgTyCon tc
dcs = Misc.sortOn F.symbol (Ghc.tyConDataCons tc)

Expand All @@ -243,7 +247,7 @@ dataConDecl d = {- F.notracepp msg $ -} DataCtor dx (F.symbol <$> as) [] xts
isGadt = not (Ghc.isVanillaDataCon d)
-- msg = printf "dataConDecl (gadt = %s)" (show isGadt)
xts = [(Bare.makeDataConSelector Nothing d i, RT.bareOfType t) | (i, t) <- its ]
dx = F.symbol <$> GM.locNamedThing d
dx = (\x -> lhNameFromGHCName (Ghc.getName x) (F.symbol x)) <$> GM.locNamedThing d
its = zip [1..] ts
(as,_ps,ts,ty) = Ghc.dataConSig d
outT = Just (RT.bareOfType ty :: BareType)
Expand Down Expand Up @@ -403,7 +407,7 @@ getDefinedSymbolsInLogic env measEnv specs =
concat (tycDCons `Mb.mapMaybe` (dataDecls spec ++ newtyDecls spec))
getFromDataCtor modName decl = S.fromList $
Bare.qualifyLocSymbolTop env modName <$>
(dcName decl : (localize . fst <$> dcFields decl))
(fmap getLHNameSymbol (dcName decl) : (localize . fst <$> dcFields decl))
getAliases spec = S.fromList $ fmap rtName <$> Ms.ealiases spec
localize :: F.Symbol -> F.LocSymbol
localize sym = maybe (dummyLoc sym) varLocSym $ L.lookup sym (Bare.reSyms env)
Expand Down
92 changes: 45 additions & 47 deletions liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ module Language.Haskell.Liquid.Bare.Resolve
-- * Looking up names
, maybeResolveSym
, lookupGhcDataCon
, lookupGhcDataConLHName
, lookupGhcDnTyCon
, lookupGhcTyCon
, lookupGhcVar
Expand Down Expand Up @@ -64,6 +65,7 @@ import qualified Data.HashSet as S
import qualified Data.Maybe as Mb
import qualified Data.HashMap.Strict as M
import qualified Data.Text as T
import GHC.Stack
import Text.Megaparsec.Pos (sourceColumn, sourceLine)
import qualified Text.PrettyPrint.HughesPJ as PJ

Expand Down Expand Up @@ -539,23 +541,26 @@ lookupGhcTyCon :: Env -> ModName -> String -> LocSymbol -> Lookup Ghc.TyCon
lookupGhcTyCon env name k lx = myTracepp ("LOOKUP-TYCON: " ++ F.showpp (val lx))
$ {- strictResolveSym -} resolveLocSym env name k lx

lookupGhcDnTyCon :: Env -> ModName -> String -> DataName -> Lookup (Maybe Ghc.TyCon)
-- lookupGhcDnTyCon = lookupGhcDnTyConE
lookupGhcDnTyCon env name msg = failMaybe env name . lookupGhcDnTyConE env name msg

lookupGhcDnTyConE :: Env -> ModName -> String -> DataName -> Lookup Ghc.TyCon
lookupGhcDnTyConE env name msg (DnCon s)
= lookupGhcDnCon env name msg s
lookupGhcDnTyConE env name msg (DnName s)
= case resolveLocSym env name msg s of
Right r -> Right r
Left e -> case lookupGhcDnCon env name msg s of
Right r -> Right r
Left _ -> Left e


lookupGhcDnCon :: Env -> ModName -> String -> LocSymbol -> Lookup Ghc.TyCon
lookupGhcDnCon env name msg = fmap Ghc.dataConTyCon . resolveLocSym env name msg
lookupGhcDnTyCon :: Env -> ModName -> DataName -> Lookup (Maybe Ghc.TyCon)
lookupGhcDnTyCon env name = failMaybe env name . lookupGhcDnTyConE env

lookupGhcDnTyConE :: Env -> DataName -> Lookup Ghc.TyCon
lookupGhcDnTyConE env (DnCon lname)
= Ghc.dataConTyCon <$> lookupGhcDataConLHName env lname
lookupGhcDnTyConE env (DnName lname)
= do
case lookupTyThing env lname of
Ghc.ATyCon tc -> Right tc
Ghc.AConLike (Ghc.RealDataCon d) -> Right $ Ghc.dataConTyCon d
_ -> panic
(Just $ GM.fSrcSpan lname) $ "not a type or data constructor: " ++ show (val lname)

lookupGhcDataConLHName :: HasCallStack => Env -> Located LHName -> Lookup Ghc.DataCon
lookupGhcDataConLHName env lname = do
case lookupTyThing env lname of
Ghc.AConLike (Ghc.RealDataCon d) -> Right d
_ -> panic
(Just $ GM.fSrcSpan lname) $ "not a data constructor: " ++ show (val lname)

-------------------------------------------------------------------------------
-- | Checking existence of names
Expand Down Expand Up @@ -691,7 +696,7 @@ resolveWith kind f env name str lx =
where
_xSym = F.val lx
sp = GM.fSrcSpanSrcSpan (F.srcSpan lx)
things = myTracepp msg $ lookupTyThing env name lx
things = myTracepp msg $ lookupTyThingLH env name lx
msg = "resolveWith: " ++ str ++ " " ++ F.showpp (val lx)


Expand All @@ -703,22 +708,22 @@ rankedThings f ias = case Misc.sortOn fst (Misc.groupList ibs) of
ibs = Mb.mapMaybe (\(k, x) -> (k,) <$> f x) ias

-------------------------------------------------------------------------------
-- | @lookupTyThing@ is the central place where we lookup the @Env@ to find
-- | @lookupTyThingLH@ is the central place where we lookup the @Env@ to find
-- any @Ghc.TyThing@ that match that name. The code is a bit hairy as we
-- have various heuristics to approximiate how GHC resolves names. e.g.
-- see tests-names-pos-*.hs, esp. vector04.hs where we need the name `Vector`
-- to resolve to `Data.Vector.Vector` and not `Data.Vector.Generic.Base.Vector`...
-------------------------------------------------------------------------------
lookupTyThing :: Env -> ModName -> LocSymbol -> [((Int, F.Symbol), Ghc.TyThing)]
lookupTyThingLH :: Env -> ModName -> LocSymbol -> [((Int, F.Symbol), Ghc.TyThing)]
-------------------------------------------------------------------------------
lookupTyThing env mdname lsym = [ (k, t) | (k, ts) <- ordMatches, t <- ts]
lookupTyThingLH env mdname lsym = [ (k, t) | (k, ts) <- ordMatches, t <- ts]

where
ordMatches = Misc.sortOn fst (Misc.groupList matches)
matches = myTracepp ("matches-" ++ msg)
[ ((k, m), t) | (m, t) <- lookupThings env x
, k <- myTracepp msg $ mm nameSym m mds ]
msg = "lookupTyThing: " ++ F.showpp (lsym, x, mds)
msg = "lookupTyThingLH: " ++ F.showpp (lsym, x, mds)
(x, mds) = symbolModules env (F.val lsym)
nameSym = F.symbol mdname
mm name m mods = myTracepp ("matchMod: " ++ F.showpp (lsym, name, m, mods)) $
Expand Down Expand Up @@ -924,40 +929,33 @@ ofBRType env name f l = go []
lc' = F.atLoc lc <$> matchTyCon env lc
lc = btc_tc tc

-- | Get the TyCon from an LHName.
matchTyCon :: Env -> Located LHName -> Lookup Ghc.TyCon
matchTyCon env lc = do
case lookupTyThing env lc of
Ghc.ATyCon tc -> Right tc
Ghc.AConLike (Ghc.RealDataCon dc) -> Right $ Ghc.promoteDataCon dc
_ -> panic
(Just $ GM.fSrcSpan lc) $ "not a type constructor: " ++ show (val lc)

-- | Get the TyThing from an LHName.
--
-- This function uses 'unsafePerformIO' to lookup the 'Ghc.TyThing' of a 'Ghc.Name'.
-- This should be benign because the result doesn't depend of when exactly this is
-- called. Since this code is intended to be used inside a GHC plugin, there is no
-- danger that GHC is finalized before the result is evaluated.
matchTyCon :: Env -> Located LHName -> Lookup Ghc.TyCon
matchTyCon env lc@(Loc _ _ c0) = unsafePerformIO $ do
lookupTyThing :: Env -> Located LHName -> Ghc.TyThing
lookupTyThing env lc@(Loc _ _ c0) = unsafePerformIO $ do
case c0 of
LHNUnresolved _ _ -> panic (Just $ GM.fSrcSpan lc) $ "matchTyCon: unresolved name: " ++ show c0
LHNUnresolved _ _ -> panic (Just $ GM.fSrcSpan lc) $ "unresolved name: " ++ show c0
LHNResolved rn _ -> case rn of
LHRLocal _ -> panic (Just $ GM.fSrcSpan lc) $ "matchTyCon: cannot resolve a local name: " ++ show c0
LHRIndex i -> panic (Just $ GM.fSrcSpan lc) $ "matchTyCon: cannot resolve a LHRIndex " ++ show i
LHRLogic (LogicName s _) -> panic (Just $ GM.fSrcSpan lc) $ "matchTyCon: cannot resolve a LHRLogic name " ++ show s
LHRLocal _ -> panic (Just $ GM.fSrcSpan lc) $ "cannot resolve a local name: " ++ show c0
LHRIndex i -> panic (Just $ GM.fSrcSpan lc) $ "cannot resolve a LHRIndex " ++ show i
LHRLogic (LogicName s _) -> panic (Just $ GM.fSrcSpan lc) $ "lookupTyThing: cannot resolve a LHRLogic name " ++ show s
LHRGHC n -> do
(_, m) <- Ghc.reflectGhc (Interface.lookupTyThing (reTcGblEnv env) n) (reSession env)
case m of
Just (Ghc.ATyCon tc) -> return (Right tc)
Just (Ghc.AConLike (Ghc.RealDataCon dc)) ->
return $ Right $ Ghc.promoteDataCon dc
Just _ -> return $ Left
[ ErrResolve
(GM.fSrcSpan lc)
"type constructor"
(PJ.text $ show c0)
"not a type constructor"
]
Nothing -> return $ Left
[ ErrResolve
(GM.fSrcSpan lc)
"type constructor"
(PJ.text $ show c0)
"not found"
]
case m of
Just tt -> return tt
Nothing -> panic (Just $ GM.fSrcSpan lc) $ "not found: " ++ show c0

bareTCApp :: (Expandable r)
=> r
Expand Down
Loading

0 comments on commit d1fe5a0

Please sign in to comment.