{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TupleSections #-}
module Language.Haskell.Liquid.Bare.Resolve
(
makeEnv
, ResolveSym (..)
, Qualify (..)
, Lookup
, qualifyTop, qualifyTopDummy
, maybeResolveSym
, lookupGhcDataCon
, lookupGhcDnTyCon
, lookupGhcTyCon
, lookupGhcVar
, lookupGhcNamedVar
, knownGhcVar
, knownGhcTyCon
, knownGhcDataCon
, knownGhcType
, srcVars
, coSubRReft
, unQualifySymbol
, ofBareTypeE
, ofBareType
, ofBPVar
, txRefSort
, errResolve
, resolveLocalBinds
, partitionLocalBinds
) where
import qualified Control.Exception as Ex
import Control.Monad (mplus)
import qualified Data.List as L
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 qualified Text.PrettyPrint.HughesPJ as PJ
import qualified Language.Fixpoint.Types as F
import qualified Language.Fixpoint.Types.Visitor as F
import qualified Language.Fixpoint.Misc as Misc
import qualified Liquid.GHC.API as Ghc
import qualified Language.Haskell.Liquid.GHC.Misc as GM
import qualified Language.Haskell.Liquid.Misc as Misc
import qualified Language.Haskell.Liquid.Types.RefType as RT
import Language.Haskell.Liquid.Types.Types
import Language.Haskell.Liquid.Measure (BareSpec)
import Language.Haskell.Liquid.Types.Specs hiding (BareSpec)
import Language.Haskell.Liquid.Types.Visitors
import Language.Haskell.Liquid.Bare.Types
import Language.Haskell.Liquid.Bare.Misc
import Language.Haskell.Liquid.WiredIn
myTracepp :: (F.PPrint a) => String -> a -> a
myTracepp :: forall a. PPrint a => String -> a -> a
myTracepp = String -> a -> a
forall a. PPrint a => String -> a -> a
F.notracepp
type Lookup a = Either [Error] a
makeEnv :: Config -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> Env
makeEnv :: Config -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> Env
makeEnv Config
cfg GhcSrc
src LogicMap
lmap [(ModName, BareSpec)]
specs = RE
{ reLMap :: LogicMap
reLMap = LogicMap
lmap
, reSyms :: [(Symbol, Id)]
reSyms = [(Symbol, Id)]
syms
, _reSubst :: Subst
_reSubst = GhcSrc -> Subst
makeVarSubst GhcSrc
src
, _reTyThings :: TyThingMap
_reTyThings = GhcSrc -> TyThingMap
makeTyThingMap GhcSrc
src
, reQualImps :: QImports
reQualImps = GhcSrc -> QImports
_gsQualImps GhcSrc
src
, reAllImps :: HashSet Symbol
reAllImps = GhcSrc -> HashSet Symbol
_gsAllImps GhcSrc
src
, reLocalVars :: LocalVars
reLocalVars = GhcSrc -> LocalVars
makeLocalVars GhcSrc
src
, reSrc :: GhcSrc
reSrc = GhcSrc
src
, reGlobSyms :: HashSet Symbol
reGlobSyms = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Symbol]
globalSyms
, reCfg :: Config
reCfg = Config
cfg
}
where
globalSyms :: [Symbol]
globalSyms = ((ModName, BareSpec) -> [Symbol])
-> [(ModName, BareSpec)] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ModName, BareSpec) -> [Symbol]
getGlobalSyms [(ModName, BareSpec)]
specs
syms :: [(Symbol, Id)]
syms = [ (Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
v, Id
v) | Id
v <- [Id]
vars ]
vars :: [Id]
vars = GhcSrc -> [Id]
srcVars GhcSrc
src
getGlobalSyms :: (ModName, BareSpec) -> [F.Symbol]
getGlobalSyms :: (ModName, BareSpec) -> [Symbol]
getGlobalSyms (ModName
_, BareSpec
spec)
= (Symbol -> Bool) -> [Symbol] -> [Symbol]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Symbol -> Bool) -> Symbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Bool
GM.isQualifiedSym)
([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ (Measure LocBareType LocSymbol -> Symbol
forall {ty} {ctor}. Measure ty ctor -> Symbol
mbName (Measure LocBareType LocSymbol -> Symbol)
-> [Measure LocBareType LocSymbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [Measure LocBareType LocSymbol]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures BareSpec
spec)
[Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (Measure LocBareType () -> Symbol
forall {ty} {ctor}. Measure ty ctor -> Symbol
mbName (Measure LocBareType () -> Symbol)
-> [Measure LocBareType ()] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [Measure LocBareType ()]
forall ty bndr. Spec ty bndr -> [Measure ty ()]
cmeasures BareSpec
spec)
[Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (Measure LocBareType LocSymbol -> Symbol
forall {ty} {ctor}. Measure ty ctor -> Symbol
mbName (Measure LocBareType LocSymbol -> Symbol)
-> [Measure LocBareType LocSymbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [Measure LocBareType LocSymbol]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
imeasures BareSpec
spec)
where
mbName :: Measure ty ctor -> Symbol
mbName = LocSymbol -> Symbol
forall a. Located a -> a
F.val (LocSymbol -> Symbol)
-> (Measure ty ctor -> LocSymbol) -> Measure ty ctor -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Measure ty ctor -> LocSymbol
forall ty ctor. Measure ty ctor -> LocSymbol
msName
makeLocalVars :: GhcSrc -> LocalVars
makeLocalVars :: GhcSrc -> LocalVars
makeLocalVars = [Id] -> LocalVars
localVarMap ([Id] -> LocalVars) -> (GhcSrc -> [Id]) -> GhcSrc -> LocalVars
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [CoreBind] -> [Id]
localBinds ([CoreBind] -> [Id]) -> (GhcSrc -> [CoreBind]) -> GhcSrc -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GhcSrc -> [CoreBind]
_giCbs
localBinds :: [Ghc.CoreBind] -> [Ghc.Var]
localBinds :: [CoreBind] -> [Id]
localBinds = (CoreBind -> [Id]) -> [CoreBind] -> [Id]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (HashSet Symbol -> CoreBind -> [Id]
bgo HashSet Symbol
forall a. HashSet a
S.empty)
where
add :: Id -> HashSet Symbol -> HashSet Symbol
add Id
x HashSet Symbol
g = HashSet Symbol
-> (Symbol -> HashSet Symbol) -> Maybe Symbol -> HashSet Symbol
forall b a. b -> (a -> b) -> Maybe a -> b
maybe HashSet Symbol
g (Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
`S.insert` HashSet Symbol
g) (Id -> Maybe Symbol
localKey Id
x)
adds :: CoreBind -> HashSet Symbol -> HashSet Symbol
adds CoreBind
b HashSet Symbol
g = (Id -> HashSet Symbol -> HashSet Symbol)
-> HashSet Symbol -> [Id] -> HashSet Symbol
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Id -> HashSet Symbol -> HashSet Symbol
add HashSet Symbol
g (CoreBind -> [Id]
forall b. Bind b -> [b]
Ghc.bindersOf CoreBind
b)
take' :: Id -> HashSet Symbol -> [Id]
take' Id
x HashSet Symbol
g = [Id] -> (Symbol -> [Id]) -> Maybe Symbol -> [Id]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\Symbol
k -> [Id
x | Bool -> Bool
not (Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
k HashSet Symbol
g)]) (Id -> Maybe Symbol
localKey Id
x)
pgo :: HashSet Symbol -> (Id, Expr Id) -> [Id]
pgo HashSet Symbol
g (Id
x, Expr Id
e) = Id -> HashSet Symbol -> [Id]
take' Id
x HashSet Symbol
g [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ HashSet Symbol -> Expr Id -> [Id]
go (Id -> HashSet Symbol -> HashSet Symbol
add Id
x HashSet Symbol
g) Expr Id
e
bgo :: HashSet Symbol -> CoreBind -> [Id]
bgo HashSet Symbol
g (Ghc.NonRec Id
x Expr Id
e) = HashSet Symbol -> (Id, Expr Id) -> [Id]
pgo HashSet Symbol
g (Id
x, Expr Id
e)
bgo HashSet Symbol
g (Ghc.Rec [(Id, Expr Id)]
xes) = ((Id, Expr Id) -> [Id]) -> [(Id, Expr Id)] -> [Id]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (HashSet Symbol -> (Id, Expr Id) -> [Id]
pgo HashSet Symbol
g) [(Id, Expr Id)]
xes
go :: HashSet Symbol -> Expr Id -> [Id]
go HashSet Symbol
g (Ghc.App Expr Id
e Expr Id
a) = (Expr Id -> [Id]) -> [Expr Id] -> [Id]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (HashSet Symbol -> Expr Id -> [Id]
go HashSet Symbol
g) [Expr Id
e, Expr Id
a]
go HashSet Symbol
g (Ghc.Lam Id
_ Expr Id
e) = HashSet Symbol -> Expr Id -> [Id]
go HashSet Symbol
g Expr Id
e
go HashSet Symbol
g (Ghc.Let CoreBind
b Expr Id
e) = HashSet Symbol -> CoreBind -> [Id]
bgo HashSet Symbol
g CoreBind
b [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ HashSet Symbol -> Expr Id -> [Id]
go (CoreBind -> HashSet Symbol -> HashSet Symbol
adds CoreBind
b HashSet Symbol
g) Expr Id
e
go HashSet Symbol
g (Ghc.Tick CoreTickish
_ Expr Id
e) = HashSet Symbol -> Expr Id -> [Id]
go HashSet Symbol
g Expr Id
e
go HashSet Symbol
g (Ghc.Cast Expr Id
e CoercionR
_) = HashSet Symbol -> Expr Id -> [Id]
go HashSet Symbol
g Expr Id
e
go HashSet Symbol
g (Ghc.Case Expr Id
e Id
_ Type
_ [Alt Id]
cs) = HashSet Symbol -> Expr Id -> [Id]
go HashSet Symbol
g Expr Id
e [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ (Alt Id -> [Id]) -> [Alt Id] -> [Id]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (HashSet Symbol -> Expr Id -> [Id]
go HashSet Symbol
g (Expr Id -> [Id]) -> (Alt Id -> Expr Id) -> Alt Id -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Ghc.Alt AltCon
_ [Id]
_ Expr Id
e') -> Expr Id
e')) [Alt Id]
cs
go HashSet Symbol
_ (Ghc.Var Id
_) = []
go HashSet Symbol
_ Expr Id
_ = []
localVarMap :: [Ghc.Var] -> LocalVars
localVarMap :: [Id] -> LocalVars
localVarMap [Id]
vs =
[(Symbol, (Int, Id))] -> LocalVars
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group [ (Symbol
x, (Int
i, Id
v)) | Id
v <- [Id]
vs
, let i :: Int
i = Pos -> Int
F.unPos (Id -> Pos
forall a. Loc a => a -> Pos
F.srcLine Id
v)
, Symbol
x <- Maybe Symbol -> [Symbol]
forall a. Maybe a -> [a]
Mb.maybeToList (Id -> Maybe Symbol
localKey Id
v)
]
localKey :: Ghc.Var -> Maybe F.Symbol
localKey :: Id -> Maybe Symbol
localKey Id
v
| Symbol -> Bool
isLocal Symbol
m = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just Symbol
x
| Bool
otherwise = Maybe Symbol
forall a. Maybe a
Nothing
where
(Symbol
m, Symbol
x) = Symbol -> (Symbol, Symbol)
splitModuleNameExact (Symbol -> (Symbol, Symbol))
-> (Id -> Symbol) -> Id -> (Symbol, Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
GM.dropModuleUnique (Symbol -> Symbol) -> (Id -> Symbol) -> Id -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Id -> (Symbol, Symbol)) -> Id -> (Symbol, Symbol)
forall a b. (a -> b) -> a -> b
$ Id
v
makeVarSubst :: GhcSrc -> F.Subst
makeVarSubst :: GhcSrc -> Subst
makeVarSubst GhcSrc
src = [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol, Expr)]
unqualSyms
where
unqualSyms :: [(Symbol, Expr)]
unqualSyms = [ (Symbol
x, Id -> Expr
mkVarExpr Id
v)
| (Symbol
x, [(Symbol, Id)]
mxs) <- HashMap Symbol [(Symbol, Id)] -> [(Symbol, [(Symbol, Id)])]
forall k v. HashMap k v -> [(k, v)]
M.toList (GhcSrc -> HashMap Symbol [(Symbol, Id)]
makeSymMap GhcSrc
src)
, Bool -> Bool
not (Symbol -> Bool
isWiredInName Symbol
x)
, Id
v <- Maybe Id -> [Id]
forall a. Maybe a -> [a]
Mb.maybeToList (Symbol -> [(Symbol, Id)] -> Maybe Id
forall a. Symbol -> [(Symbol, a)] -> Maybe a
okUnqualified Symbol
me [(Symbol, Id)]
mxs)
]
me :: Symbol
me = ModName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (GhcSrc -> ModName
_giTargetMod GhcSrc
src)
okUnqualified :: F.Symbol -> [(F.Symbol, a)] -> Maybe a
okUnqualified :: forall a. Symbol -> [(Symbol, a)] -> Maybe a
okUnqualified Symbol
_ [(Symbol
_, a
x)] = a -> Maybe a
forall a. a -> Maybe a
Just a
x
okUnqualified Symbol
me [(Symbol, a)]
mxs = [(Symbol, a)] -> Maybe a
forall {a}. [(Symbol, a)] -> Maybe a
go [(Symbol, a)]
mxs
where
go :: [(Symbol, a)] -> Maybe a
go [] = Maybe a
forall a. Maybe a
Nothing
go ((Symbol
m,a
x) : [(Symbol, a)]
rest)
| Symbol
me Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
m = a -> Maybe a
forall a. a -> Maybe a
Just a
x
| Bool
otherwise = [(Symbol, a)] -> Maybe a
go [(Symbol, a)]
rest
makeSymMap :: GhcSrc -> M.HashMap F.Symbol [(F.Symbol, Ghc.Var)]
makeSymMap :: GhcSrc -> HashMap Symbol [(Symbol, Id)]
makeSymMap GhcSrc
src = [(Symbol, (Symbol, Id))] -> HashMap Symbol [(Symbol, Id)]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group [ (Symbol
sym, (Symbol
m, Id
x))
| Id
x <- GhcSrc -> [Id]
srcVars GhcSrc
src
, let (Symbol
m, Symbol
sym) = Id -> (Symbol, Symbol)
forall a. Symbolic a => a -> (Symbol, Symbol)
qualifiedSymbol Id
x ]
makeTyThingMap :: GhcSrc -> TyThingMap
makeTyThingMap :: GhcSrc -> TyThingMap
makeTyThingMap GhcSrc
src =
TyThingMap -> TyThingMap
forall {k} {a}.
(Hashable k, Eq a, IsString k, IsString a) =>
HashMap k [(a, TyThing)] -> HashMap k [(a, TyThing)]
addListTyConName (TyThingMap -> TyThingMap) -> TyThingMap -> TyThingMap
forall a b. (a -> b) -> a -> b
$
[(Symbol, (Symbol, TyThing))] -> TyThingMap
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group [ (Symbol
x, (Symbol
m, TyThing
t)) | TyThing
t <- GhcSrc -> [TyThing]
srcThings GhcSrc
src
, Symbol
tSym <- Maybe Symbol -> [Symbol]
forall a. Maybe a -> [a]
Mb.maybeToList (TyThing -> Maybe Symbol
tyThingSymbol TyThing
t)
, let (Symbol
m, Symbol
x) = Symbol -> (Symbol, Symbol)
forall a. Symbolic a => a -> (Symbol, Symbol)
qualifiedSymbol Symbol
tSym
, Bool -> Bool
not (Symbol -> Bool
isLocal Symbol
m)
]
where
addListTyConName :: HashMap k [(a, TyThing)] -> HashMap k [(a, TyThing)]
addListTyConName HashMap k [(a, TyThing)]
m =
case k -> HashMap k [(a, TyThing)] -> Maybe [(a, TyThing)]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup k
"[]" HashMap k [(a, TyThing)]
m of
Maybe [(a, TyThing)]
Nothing -> HashMap k [(a, TyThing)]
m
Just [(a, TyThing)]
ps -> ([(a, TyThing)] -> [(a, TyThing)] -> [(a, TyThing)])
-> k
-> [(a, TyThing)]
-> HashMap k [(a, TyThing)]
-> HashMap k [(a, TyThing)]
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
M.insertWith [(a, TyThing)] -> [(a, TyThing)] -> [(a, TyThing)]
forall a. [a] -> [a] -> [a]
(++) k
"List" ([(a, TyThing)] -> [(a, TyThing)]
forall {a}. (Eq a, IsString a) => [(a, TyThing)] -> [(a, TyThing)]
filterListTyCon [(a, TyThing)]
ps) HashMap k [(a, TyThing)]
m
filterListTyCon :: [(a, TyThing)] -> [(a, TyThing)]
filterListTyCon [(a, TyThing)]
ps =
[ (a
mn, TyCon -> TyThing
Ghc.ATyCon TyCon
tc') | (a
mn, Ghc.ATyCon TyCon
tc) <- [(a, TyThing)]
ps
, a
"GHC.Types" a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
mn
, let tc' :: TyCon
tc' = TyCon
Ghc.listTyCon { Ghc.tyConName = Ghc.tyConName tc }
]
tyThingSymbol :: Ghc.TyThing -> Maybe F.Symbol
tyThingSymbol :: TyThing -> Maybe Symbol
tyThingSymbol (Ghc.AnId Id
x) = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just (Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
x)
tyThingSymbol (Ghc.ATyCon TyCon
c) = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just (TyCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyCon
c)
tyThingSymbol (Ghc.AConLike ConLike
d) = ConLike -> Maybe Symbol
conLikeSymbol ConLike
d
tyThingSymbol TyThing
_tt = Maybe Symbol
forall a. Maybe a
Nothing
conLikeSymbol :: Ghc.ConLike -> Maybe F.Symbol
conLikeSymbol :: ConLike -> Maybe Symbol
conLikeSymbol (Ghc.RealDataCon DataCon
d) = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just (DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol DataCon
d)
conLikeSymbol ConLike
_z = Maybe Symbol
forall a. Maybe a
Nothing
isLocal :: F.Symbol -> Bool
isLocal :: Symbol -> Bool
isLocal = Symbol -> Bool
isEmptySymbol
qualifiedSymbol :: (F.Symbolic a) => a -> (F.Symbol, F.Symbol)
qualifiedSymbol :: forall a. Symbolic a => a -> (Symbol, Symbol)
qualifiedSymbol = Symbol -> (Symbol, Symbol)
splitModuleNameExact (Symbol -> (Symbol, Symbol))
-> (a -> Symbol) -> a -> (Symbol, Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol
isEmptySymbol :: F.Symbol -> Bool
isEmptySymbol :: Symbol -> Bool
isEmptySymbol Symbol
x = Symbol -> Int
F.lengthSym Symbol
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
srcThings :: GhcSrc -> [Ghc.TyThing]
srcThings :: GhcSrc -> [TyThing]
srcThings GhcSrc
src = String -> [TyThing] -> [TyThing]
forall a. PPrint a => String -> a -> a
myTracepp String
"SRCTHINGS"
([TyThing] -> [TyThing]) -> [TyThing] -> [TyThing]
forall a b. (a -> b) -> a -> b
$ (TyThing -> String) -> [TyThing] -> [TyThing]
forall b a. Ord b => (a -> b) -> [a] -> [a]
Misc.hashNubWith TyThing -> String
forall a. PPrint a => a -> String
F.showpp (GhcSrc -> [TyThing]
_gsTyThings GhcSrc
src [TyThing] -> [TyThing] -> [TyThing]
forall a. [a] -> [a] -> [a]
++ GhcSrc -> [TyThing]
mySrcThings GhcSrc
src)
mySrcThings :: GhcSrc -> [Ghc.TyThing]
mySrcThings :: GhcSrc -> [TyThing]
mySrcThings GhcSrc
src = [ Id -> TyThing
Ghc.AnId Id
x | Id
x <- [Id]
vars ]
[TyThing] -> [TyThing] -> [TyThing]
forall a. [a] -> [a] -> [a]
++ [ TyCon -> TyThing
Ghc.ATyCon TyCon
c | TyCon
c <- [TyCon]
tcs ]
[TyThing] -> [TyThing] -> [TyThing]
forall a. [a] -> [a] -> [a]
++ [ DataCon -> TyThing
aDataCon DataCon
d | DataCon
d <- [DataCon]
dcs ]
where
vars :: [Id]
vars = [Id] -> [Id]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([Id] -> [Id]) -> [Id] -> [Id]
forall a b. (a -> b) -> a -> b
$ [DataCon] -> [Id]
dataConVars [DataCon]
dcs [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ GhcSrc -> [Id]
srcVars GhcSrc
src
dcs :: [DataCon]
dcs = [DataCon] -> [DataCon]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([DataCon] -> [DataCon]) -> [DataCon] -> [DataCon]
forall a b. (a -> b) -> a -> b
$ (TyCon -> [DataCon]) -> [TyCon] -> [DataCon]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TyCon -> [DataCon]
Ghc.tyConDataCons [TyCon]
tcs
tcs :: [TyCon]
tcs = [TyCon] -> [TyCon]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall a b. (a -> b) -> a -> b
$ GhcSrc -> [TyCon]
srcTyCons GhcSrc
src
aDataCon :: DataCon -> TyThing
aDataCon = ConLike -> TyThing
Ghc.AConLike (ConLike -> TyThing) -> (DataCon -> ConLike) -> DataCon -> TyThing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> ConLike
Ghc.RealDataCon
srcTyCons :: GhcSrc -> [Ghc.TyCon]
srcTyCons :: GhcSrc -> [TyCon]
srcTyCons GhcSrc
src = [[TyCon]] -> [TyCon]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ GhcSrc -> [TyCon]
_gsTcs GhcSrc
src
, GhcSrc -> [TyCon]
_gsFiTcs GhcSrc
src
, GhcSrc -> [TyCon]
_gsPrimTcs GhcSrc
src
, GhcSrc -> [TyCon]
srcVarTcs GhcSrc
src
]
srcVarTcs :: GhcSrc -> [Ghc.TyCon]
srcVarTcs :: GhcSrc -> [TyCon]
srcVarTcs = [Id] -> [TyCon]
varTyCons ([Id] -> [TyCon]) -> (GhcSrc -> [Id]) -> GhcSrc -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GhcSrc -> [Id]
srcVars
varTyCons :: [Ghc.Var] -> [Ghc.TyCon]
varTyCons :: [Id] -> [TyCon]
varTyCons = (Id -> [TyCon]) -> [Id] -> [TyCon]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Type -> [TyCon]
typeTyCons (Type -> [TyCon]) -> (Id -> Type) -> Id -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
Ghc.dropForAlls (Type -> Type) -> (Id -> Type) -> Id -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Type
Ghc.varType)
typeTyCons :: Ghc.Type -> [Ghc.TyCon]
typeTyCons :: Type -> [TyCon]
typeTyCons Type
t = Type -> [TyCon]
tops Type
t [TyCon] -> [TyCon] -> [TyCon]
forall a. [a] -> [a] -> [a]
++ Type -> [TyCon]
inners Type
t
where
tops :: Type -> [TyCon]
tops = Maybe TyCon -> [TyCon]
forall a. Maybe a -> [a]
Mb.maybeToList (Maybe TyCon -> [TyCon])
-> (Type -> Maybe TyCon) -> Type -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe TyCon
Ghc.tyConAppTyCon_maybe
inners :: Type -> [TyCon]
inners = (Type -> [TyCon]) -> [Type] -> [TyCon]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [TyCon]
typeTyCons ([Type] -> [TyCon]) -> (Type -> [Type]) -> Type -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, [Type]) -> [Type]
forall a b. (a, b) -> b
snd ((Type, [Type]) -> [Type])
-> (Type -> (Type, [Type])) -> Type -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> (Type, [Type])
Ghc.splitAppTys
srcVars :: GhcSrc -> [Ghc.Var]
srcVars :: GhcSrc -> [Id]
srcVars GhcSrc
src = (Id -> Bool) -> [Id] -> [Id]
forall a. (a -> Bool) -> [a] -> [a]
filter Id -> Bool
Ghc.isId ([Id] -> [Id])
-> ([(Int, Symbol, Id)] -> [Id]) -> [(Int, Symbol, Id)] -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Symbol, Id) -> Id) -> [(Int, Symbol, Id)] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, Symbol, Id) -> Id
forall a b c. (a, b, c) -> c
Misc.thd3 ([(Int, Symbol, Id)] -> [Id])
-> ([(Int, Symbol, Id)] -> [(Int, Symbol, Id)])
-> [(Int, Symbol, Id)]
-> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Int, Symbol, Id)] -> [(Int, Symbol, Id)]
forall r k v.
(Ord r, Hashable k, Eq k) =>
[(r, k, v)] -> [(r, k, v)]
Misc.fstByRank ([(Int, Symbol, Id)] -> [Id]) -> [(Int, Symbol, Id)] -> [Id]
forall a b. (a -> b) -> a -> b
$ [[(Int, Symbol, Id)]] -> [(Int, Symbol, Id)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ String -> Int -> Id -> (Int, Symbol, Id)
key String
"SRC-VAR-DEF" Int
0 (Id -> (Int, Symbol, Id)) -> [Id] -> [(Int, Symbol, Id)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSrc -> [Id]
_giDefVars GhcSrc
src
, String -> Int -> Id -> (Int, Symbol, Id)
key String
"SRC-VAR-DER" Int
1 (Id -> (Int, Symbol, Id)) -> [Id] -> [(Int, Symbol, Id)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet Id -> [Id]
forall a. HashSet a -> [a]
S.toList (GhcSrc -> HashSet Id
_giDerVars GhcSrc
src)
, String -> Int -> Id -> (Int, Symbol, Id)
key String
"SRC-VAR-IMP" Int
2 (Id -> (Int, Symbol, Id)) -> [Id] -> [(Int, Symbol, Id)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSrc -> [Id]
_giImpVars GhcSrc
src
, String -> Int -> Id -> (Int, Symbol, Id)
key String
"SRC-VAR-USE" Int
3 (Id -> (Int, Symbol, Id)) -> [Id] -> [(Int, Symbol, Id)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSrc -> [Id]
_giUseVars GhcSrc
src
, String -> Int -> Id -> (Int, Symbol, Id)
key String
"SRC-VAR-THN" Int
4 (Id -> (Int, Symbol, Id)) -> [Id] -> [(Int, Symbol, Id)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ Id
x | Ghc.AnId Id
x <- GhcSrc -> [TyThing]
_gsTyThings GhcSrc
src ]
]
where
key :: String -> Int -> Ghc.Var -> (Int, F.Symbol, Ghc.Var)
key :: String -> Int -> Id -> (Int, Symbol, Id)
key String
_ Int
i Id
x = (Int
i, Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
x, Id
x)
_dump :: String -> Id -> Id
_dump String
msg Id
x = (Id, SpecType) -> Id
forall a b. (a, b) -> a
fst ((Id, SpecType) -> Id)
-> ((Id, SpecType) -> (Id, SpecType)) -> (Id, SpecType) -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> (Id, SpecType) -> (Id, SpecType)
forall a. PPrint a => String -> a -> a
myTracepp String
msg ((Id, SpecType) -> Id) -> (Id, SpecType) -> Id
forall a b. (a -> b) -> a -> b
$ (Id
x, Type -> SpecType
forall r. Monoid r => Type -> RRType r
RT.ofType (Type -> Type
Ghc.expandTypeSynonyms (Id -> Type
Ghc.varType Id
x)) :: SpecType)
dataConVars :: [Ghc.DataCon] -> [Ghc.Var]
dataConVars :: [DataCon] -> [Id]
dataConVars [DataCon]
dcs = (DataCon -> Id
Ghc.dataConWorkId (DataCon -> Id) -> [DataCon] -> [Id]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataCon]
dcs) [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ (DataCon -> Id
Ghc.dataConWrapId (DataCon -> Id) -> [DataCon] -> [Id]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataCon]
dcs)
qualifyTop :: (Qualify a) => Env -> ModName -> F.SourcePos -> a -> a
qualifyTop :: forall a. Qualify a => Env -> ModName -> SourcePos -> a -> a
qualifyTop Env
env ModName
name SourcePos
l = Env -> ModName -> SourcePos -> [Symbol] -> a -> a
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l []
qualifyTopDummy :: (Qualify a) => Env -> ModName -> a -> a
qualifyTopDummy :: forall a. Qualify a => Env -> ModName -> a -> a
qualifyTopDummy Env
env ModName
name = Env -> ModName -> SourcePos -> a -> a
forall a. Qualify a => Env -> ModName -> SourcePos -> a -> a
qualifyTop Env
env ModName
name SourcePos
dummySourcePos
dummySourcePos :: F.SourcePos
dummySourcePos :: SourcePos
dummySourcePos = Located () -> SourcePos
forall a. Located a -> SourcePos
F.loc (() -> Located ()
forall a. a -> Located a
F.dummyLoc ())
class Qualify a where
qualify :: Env -> ModName -> F.SourcePos -> [F.Symbol] -> a -> a
instance Qualify TyConMap where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConMap -> TyConMap
qualify Env
env ModName
name SourcePos
l [Symbol]
bs TyConMap
tyi = TyConMap
tyi
{ tcmTyRTy = tx <$> tcmTyRTy tyi
, tcmFIRTy = tx <$> tcmFIRTy tyi
}
where
tx :: (Qualify a) => a -> a
tx :: forall a. Qualify a => a -> a
tx = Env -> ModName -> SourcePos -> [Symbol] -> a -> a
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs
instance Qualify TyConP where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConP -> TyConP
qualify Env
env ModName
name SourcePos
_ [Symbol]
bs TyConP
tcp = TyConP
tcp { tcpSizeFun = qualify env name (tcpLoc tcp) bs <$> tcpSizeFun tcp }
instance Qualify SizeFun where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> SizeFun -> SizeFun
qualify Env
env ModName
name SourcePos
_ [Symbol]
bs (SymSizeFun LocSymbol
lx) = LocSymbol -> SizeFun
SymSizeFun (Env -> ModName -> SourcePos -> [Symbol] -> LocSymbol -> LocSymbol
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name (LocSymbol -> SourcePos
forall a. Located a -> SourcePos
F.loc LocSymbol
lx) [Symbol]
bs LocSymbol
lx)
qualify Env
_ ModName
_ SourcePos
_ [Symbol]
_ SizeFun
sf = SizeFun
sf
instance Qualify F.Equation where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Equation -> Equation
qualify Env
_env ModName
_name SourcePos
_l [Symbol]
_bs Equation
x = Equation
x
instance Qualify F.Symbol where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Symbol -> Symbol
qualify Env
env ModName
name SourcePos
l [Symbol]
bs Symbol
x = Env -> ModName -> SourcePos -> [Symbol] -> Symbol -> Symbol
qualifySymbol Env
env ModName
name SourcePos
l [Symbol]
bs Symbol
x
qualifySymbol :: Env -> ModName -> F.SourcePos -> [F.Symbol] -> F.Symbol -> F.Symbol
qualifySymbol :: Env -> ModName -> SourcePos -> [Symbol] -> Symbol -> Symbol
qualifySymbol Env
env ModName
name SourcePos
l [Symbol]
bs Symbol
x
| Bool
isSpl = Symbol
x
| Bool
otherwise = case Env -> ModName -> String -> LocSymbol -> Lookup Symbol
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
"Symbol" (SourcePos -> SourcePos -> Symbol -> LocSymbol
forall a. SourcePos -> SourcePos -> a -> Located a
F.Loc SourcePos
l SourcePos
l Symbol
x) of
Left [Error]
_ -> Symbol
x
Right Symbol
v -> Symbol
v
where
isSpl :: Bool
isSpl = Env -> [Symbol] -> Symbol -> Bool
isSplSymbol Env
env [Symbol]
bs Symbol
x
isSplSymbol :: Env -> [F.Symbol] -> F.Symbol -> Bool
isSplSymbol :: Env -> [Symbol] -> Symbol -> Bool
isSplSymbol Env
env [Symbol]
bs Symbol
x
= Symbol -> Bool
isWiredInName Symbol
x
Bool -> Bool -> Bool
|| Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Symbol
x [Symbol]
bs
Bool -> Bool -> Bool
|| Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
x (Env -> HashSet Symbol
reGlobSyms Env
env)
instance (Qualify a) => Qualify (Located a) where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Located a -> Located a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs = (a -> a) -> Located a -> Located a
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> ModName -> SourcePos -> [Symbol] -> a -> a
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs)
instance (Qualify a) => Qualify [a] where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> [a] -> [a]
qualify Env
env ModName
name SourcePos
l [Symbol]
bs = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> ModName -> SourcePos -> [Symbol] -> a -> a
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs)
instance (Qualify a) => Qualify (Maybe a) where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Maybe a -> Maybe a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs = (a -> a) -> Maybe a -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> ModName -> SourcePos -> [Symbol] -> a -> a
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs)
instance Qualify Body where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Body -> Body
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (P Expr
p) = Expr -> Body
P (Env -> ModName -> SourcePos -> [Symbol] -> Expr -> Expr
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs Expr
p)
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (E Expr
e) = Expr -> Body
E (Env -> ModName -> SourcePos -> [Symbol] -> Expr -> Expr
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs Expr
e)
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (R Symbol
x Expr
p) = Symbol -> Expr -> Body
R Symbol
x (Env -> ModName -> SourcePos -> [Symbol] -> Expr -> Expr
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs Expr
p)
instance Qualify TyConInfo where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConInfo -> TyConInfo
qualify Env
env ModName
name SourcePos
l [Symbol]
bs TyConInfo
tci = TyConInfo
tci { sizeFunction = qualify env name l bs <$> sizeFunction tci }
instance Qualify RTyCon where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> RTyCon -> RTyCon
qualify Env
env ModName
name SourcePos
l [Symbol]
bs RTyCon
rtc = RTyCon
rtc { rtc_info = qualify env name l bs (rtc_info rtc) }
instance Qualify (Measure SpecType Ghc.DataCon) where
qualify :: Env
-> ModName
-> SourcePos
-> [Symbol]
-> Measure SpecType DataCon
-> Measure SpecType DataCon
qualify Env
env ModName
name SourcePos
_ [Symbol]
bs Measure SpecType DataCon
m = Measure SpecType DataCon
m
{ msName = qualify env name l bs lname
, msEqns = qualify env name l bs <$> msEqns m
}
where
l :: SourcePos
l = LocSymbol -> SourcePos
forall a. Located a -> SourcePos
F.loc LocSymbol
lname
lname :: LocSymbol
lname = Measure SpecType DataCon -> LocSymbol
forall ty ctor. Measure ty ctor -> LocSymbol
msName Measure SpecType DataCon
m
instance Qualify (Def ty ctor) where
qualify :: Env
-> ModName -> SourcePos -> [Symbol] -> Def ty ctor -> Def ty ctor
qualify Env
env ModName
name SourcePos
l [Symbol]
bs Def ty ctor
d = Def ty ctor
d
{ body = qualify env name l (bs ++ bs') (body d) }
where
bs' :: [Symbol]
bs' = (Symbol, Maybe ty) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Maybe ty) -> Symbol) -> [(Symbol, Maybe ty)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Def ty ctor -> [(Symbol, Maybe ty)]
forall ty ctor. Def ty ctor -> [(Symbol, Maybe ty)]
binds Def ty ctor
d
instance Qualify BareMeasure where
qualify :: Env
-> ModName
-> SourcePos
-> [Symbol]
-> Measure LocBareType LocSymbol
-> Measure LocBareType LocSymbol
qualify Env
env ModName
name SourcePos
l [Symbol]
bs Measure LocBareType LocSymbol
m = Measure LocBareType LocSymbol
m
{ msEqns = qualify env name l bs (msEqns m)
}
instance Qualify DataCtor where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> DataCtor -> DataCtor
qualify Env
env ModName
name SourcePos
l [Symbol]
bs DataCtor
c = DataCtor
c
{ dcTheta = qualify env name l bs (dcTheta c)
, dcFields = qualify env name l bs (dcFields c)
, dcResult = qualify env name l bs (dcResult c)
}
instance Qualify DataDecl where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> DataDecl -> DataDecl
qualify Env
env ModName
name SourcePos
l [Symbol]
bs DataDecl
d = DataDecl
d
{ tycDCons = qualify env name l bs (tycDCons d)
, tycPropTy = qualify env name l bs (tycPropTy d)
}
instance Qualify ModSpecs where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs
qualify Env
env ModName
name SourcePos
l [Symbol]
bs = (ModName -> BareSpec -> BareSpec) -> ModSpecs -> ModSpecs
forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
Misc.hashMapMapWithKey (\ModName
_ -> Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs)
instance Qualify b => Qualify (a, b) where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> (a, b) -> (a, b)
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (a
x, b
y) = (a
x, Env -> ModName -> SourcePos -> [Symbol] -> b -> b
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs b
y)
instance Qualify BareSpec where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec
qualify = Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec
qualifyBareSpec
qualifyBareSpec :: Env -> ModName -> F.SourcePos -> [F.Symbol] -> BareSpec -> BareSpec
qualifyBareSpec :: Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec
qualifyBareSpec Env
env ModName
name SourcePos
l [Symbol]
bs BareSpec
sp = BareSpec
sp
{ measures = qualify env name l bs (measures sp)
, asmSigs = qualify env name l bs (asmSigs sp)
, sigs = qualify env name l bs (sigs sp)
, localSigs = qualify env name l bs (localSigs sp)
, reflSigs = qualify env name l bs (reflSigs sp)
, dataDecls = qualify env name l bs (dataDecls sp)
, newtyDecls = qualify env name l bs (newtyDecls sp)
, ialiases = [ (f x, f y) | (x, y) <- ialiases sp ]
}
where f :: LocBareType -> LocBareType
f = Env
-> ModName -> SourcePos -> [Symbol] -> LocBareType -> LocBareType
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs
instance Qualify a => Qualify (RTAlias F.Symbol a) where
qualify :: Env
-> ModName
-> SourcePos
-> [Symbol]
-> RTAlias Symbol a
-> RTAlias Symbol a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs RTAlias Symbol a
rtAlias
= RTAlias Symbol a
rtAlias { rtName = qualify env name l bs (rtName rtAlias)
, rtTArgs = qualify env name l bs (rtTArgs rtAlias)
, rtVArgs = qualify env name l bs (rtVArgs rtAlias)
, rtBody = qualify env name l bs (rtBody rtAlias)
}
instance Qualify F.Expr where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Expr -> Expr
qualify = Env -> ModName -> SourcePos -> [Symbol] -> Expr -> Expr
forall a.
Subable a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
substEnv
instance Qualify RReft where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> RReft -> RReft
qualify = Env -> ModName -> SourcePos -> [Symbol] -> RReft -> RReft
forall a.
Subable a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
substEnv
instance Qualify F.Qualifier where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Qualifier -> Qualifier
qualify Env
env ModName
name SourcePos
_ [Symbol]
bs Qualifier
q = Qualifier
q { F.qBody = qualify env name (F.qPos q) bs' (F.qBody q) }
where
bs' :: [Symbol]
bs' = [Symbol]
bs [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (QualParam -> Symbol
F.qpSym (QualParam -> Symbol) -> [QualParam] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Qualifier -> [QualParam]
F.qParams Qualifier
q)
substEnv :: (F.Subable a) => Env -> ModName -> F.SourcePos -> [F.Symbol] -> a -> a
substEnv :: forall a.
Subable a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
substEnv Env
env ModName
name SourcePos
l [Symbol]
bs = (Symbol -> Symbol) -> a -> a
forall a. Subable a => (Symbol -> Symbol) -> a -> a
F.substa (Env -> ModName -> SourcePos -> [Symbol] -> Symbol -> Symbol
qualifySymbol Env
env ModName
name SourcePos
l [Symbol]
bs)
instance Qualify SpecType where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> SpecType -> SpecType
qualify Env
x1 ModName
x2 SourcePos
x3 [Symbol]
x4 SpecType
x5 = ([Symbol] -> RReft -> RReft) -> [Symbol] -> SpecType -> SpecType
forall r1 r2 c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RType c tv r1 -> RType c tv r2
emapReft (Env -> ModName -> SourcePos -> [Symbol] -> RReft -> RReft
forall a.
Subable a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
substFreeEnv Env
x1 ModName
x2 SourcePos
x3) [Symbol]
x4 SpecType
x5
instance Qualify BareType where
qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareType -> BareType
qualify Env
x1 ModName
x2 SourcePos
x3 [Symbol]
x4 BareType
x5 = ([Symbol] -> RReft -> RReft) -> [Symbol] -> BareType -> BareType
forall r1 r2 c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RType c tv r1 -> RType c tv r2
emapReft (Env -> ModName -> SourcePos -> [Symbol] -> RReft -> RReft
forall a.
Subable a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
substFreeEnv Env
x1 ModName
x2 SourcePos
x3) [Symbol]
x4 BareType
x5
substFreeEnv :: (F.Subable a) => Env -> ModName -> F.SourcePos -> [F.Symbol] -> a -> a
substFreeEnv :: forall a.
Subable a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
substFreeEnv Env
env ModName
name SourcePos
l [Symbol]
bs = (Symbol -> Expr) -> a -> a
forall a. Subable a => (Symbol -> Expr) -> a -> a
F.substf (Symbol -> Expr
F.EVar (Symbol -> Expr) -> (Symbol -> Symbol) -> Symbol -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ModName -> SourcePos -> [Symbol] -> Symbol -> Symbol
qualifySymbol Env
env ModName
name SourcePos
l [Symbol]
bs)
lookupGhcNamedVar :: (Ghc.NamedThing a, F.Symbolic a) => Env -> ModName -> a -> Maybe Ghc.Var
lookupGhcNamedVar :: forall a.
(NamedThing a, Symbolic a) =>
Env -> ModName -> a -> Maybe Id
lookupGhcNamedVar Env
env ModName
name a
z = Env -> ModName -> String -> LocSymbol -> Maybe Id
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Maybe a
maybeResolveSym Env
env ModName
name String
"Var" LocSymbol
lx
where
lx :: LocSymbol
lx = a -> LocSymbol
forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol a
z
lookupGhcVar :: Env -> ModName -> String -> LocSymbol -> Lookup Ghc.Var
lookupGhcVar :: Env -> ModName -> String -> LocSymbol -> Lookup Id
lookupGhcVar Env
env ModName
name String
kind LocSymbol
lx = case Env -> ModName -> String -> LocSymbol -> Lookup Id
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
kind LocSymbol
lx of
Right Id
v -> Lookup Id -> (Id -> Lookup Id) -> Maybe Id -> Lookup Id
forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe (Id -> Lookup Id
forall a b. b -> Either a b
Right Id
v) Id -> Lookup Id
forall a b. b -> Either a b
Right (Env -> LocSymbol -> [Id] -> Maybe Id
lookupLocalVar Env
env LocSymbol
lx [Id
v])
Left [Error]
e -> Lookup Id -> (Id -> Lookup Id) -> Maybe Id -> Lookup Id
forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe ([Error] -> Lookup Id
forall a b. a -> Either a b
Left [Error]
e) Id -> Lookup Id
forall a b. b -> Either a b
Right (Env -> LocSymbol -> [Id] -> Maybe Id
lookupLocalVar Env
env LocSymbol
lx [])
lookupLocalVar :: Env -> LocSymbol -> [Ghc.Var] -> Maybe Ghc.Var
lookupLocalVar :: Env -> LocSymbol -> [Id] -> Maybe Id
lookupLocalVar Env
env LocSymbol
lx [Id]
gvs = Int -> [(Int, Id)] -> Maybe Id
forall i a. (Ord i, Num i) => i -> [(i, a)] -> Maybe a
Misc.findNearest Int
lxn [(Int, Id)]
kvs
where
_msg :: String
_msg = String
"LOOKUP-LOCAL: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Symbol, Int, [(Int, Id)]) -> String
forall a. PPrint a => a -> String
F.showpp (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lx, Int
lxn, [(Int, Id)]
kvs)
kvs :: [(Int, Id)]
kvs = [(Int, Id)]
gs [(Int, Id)] -> [(Int, Id)] -> [(Int, Id)]
forall a. [a] -> [a] -> [a]
++ [(Int, Id)] -> Symbol -> LocalVars -> [(Int, Id)]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] Symbol
x (Env -> LocalVars
reLocalVars Env
env)
gs :: [(Int, Id)]
gs = [(Pos -> Int
F.unPos (Id -> Pos
forall a. Loc a => a -> Pos
F.srcLine Id
v), Id
v) | Id
v <- [Id]
gvs]
lxn :: Int
lxn = Pos -> Int
F.unPos (LocSymbol -> Pos
forall a. Loc a => a -> Pos
F.srcLine LocSymbol
lx)
(Maybe Symbol
_, Symbol
x) = Symbol -> (Maybe Symbol, Symbol)
unQualifySymbol (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lx)
lookupGhcDataCon :: Env -> ModName -> String -> LocSymbol -> Lookup Ghc.DataCon
lookupGhcDataCon :: Env -> ModName -> String -> LocSymbol -> Lookup DataCon
lookupGhcDataCon = Env -> ModName -> String -> LocSymbol -> Lookup DataCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym
lookupGhcTyCon :: Env -> ModName -> String -> LocSymbol -> Lookup Ghc.TyCon
lookupGhcTyCon :: Env -> ModName -> String -> LocSymbol -> Lookup TyCon
lookupGhcTyCon Env
env ModName
name String
k LocSymbol
lx = String -> Lookup TyCon -> Lookup TyCon
forall a. PPrint a => String -> a -> a
myTracepp (String
"LOOKUP-TYCON: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. PPrint a => a -> String
F.showpp (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
lx))
(Lookup TyCon -> Lookup TyCon) -> Lookup TyCon -> Lookup TyCon
forall a b. (a -> b) -> a -> b
$ Env -> ModName -> String -> LocSymbol -> Lookup TyCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
k LocSymbol
lx
lookupGhcDnTyCon :: Env -> ModName -> String -> DataName -> Lookup (Maybe Ghc.TyCon)
lookupGhcDnTyCon :: Env -> ModName -> String -> DataName -> Lookup (Maybe TyCon)
lookupGhcDnTyCon Env
env ModName
name String
msg = Env -> ModName -> Lookup TyCon -> Lookup (Maybe TyCon)
forall e r. Env -> ModName -> Either e r -> Either e (Maybe r)
failMaybe Env
env ModName
name (Lookup TyCon -> Lookup (Maybe TyCon))
-> (DataName -> Lookup TyCon) -> DataName -> Lookup (Maybe TyCon)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ModName -> String -> DataName -> Lookup TyCon
lookupGhcDnTyConE Env
env ModName
name String
msg
lookupGhcDnTyConE :: Env -> ModName -> String -> DataName -> Lookup Ghc.TyCon
lookupGhcDnTyConE :: Env -> ModName -> String -> DataName -> Lookup TyCon
lookupGhcDnTyConE Env
env ModName
name String
msg (DnCon LocSymbol
s)
= Env -> ModName -> String -> LocSymbol -> Lookup TyCon
lookupGhcDnCon Env
env ModName
name String
msg LocSymbol
s
lookupGhcDnTyConE Env
env ModName
name String
msg (DnName LocSymbol
s)
= case Env -> ModName -> String -> LocSymbol -> Lookup TyCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
msg LocSymbol
s of
Right TyCon
r -> TyCon -> Lookup TyCon
forall a b. b -> Either a b
Right TyCon
r
Left [Error]
e -> case Env -> ModName -> String -> LocSymbol -> Lookup TyCon
lookupGhcDnCon Env
env ModName
name String
msg LocSymbol
s of
Right TyCon
r -> TyCon -> Lookup TyCon
forall a b. b -> Either a b
Right TyCon
r
Left [Error]
_ -> [Error] -> Lookup TyCon
forall a b. a -> Either a b
Left [Error]
e
lookupGhcDnCon :: Env -> ModName -> String -> LocSymbol -> Lookup Ghc.TyCon
lookupGhcDnCon :: Env -> ModName -> String -> LocSymbol -> Lookup TyCon
lookupGhcDnCon Env
env ModName
name String
msg = (DataCon -> TyCon) -> Lookup DataCon -> Lookup TyCon
forall a b. (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataCon -> TyCon
Ghc.dataConTyCon (Lookup DataCon -> Lookup TyCon)
-> (LocSymbol -> Lookup DataCon) -> LocSymbol -> Lookup TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ModName -> String -> LocSymbol -> Lookup DataCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
msg
knownGhcType :: Env -> ModName -> LocBareType -> Bool
knownGhcType :: Env -> ModName -> LocBareType -> Bool
knownGhcType Env
env ModName
name (F.Loc SourcePos
l SourcePos
_ BareType
t) =
case Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> BareType
-> Lookup SpecType
ofBareTypeE Env
env ModName
name SourcePos
l Maybe [PVar BSort]
forall a. Maybe a
Nothing BareType
t of
Left [Error]
e -> String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
myTracepp (String
"knownType: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (BareType, [Error]) -> String
forall a. PPrint a => a -> String
F.showpp (BareType
t, [Error]
e)) Bool
False
Right SpecType
_ -> Bool
True
_rTypeTyCons :: (Ord c) => RType c tv r -> [c]
_rTypeTyCons :: forall c tv r. Ord c => RType c tv r -> [c]
_rTypeTyCons = [c] -> [c]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([c] -> [c]) -> (RType c tv r -> [c]) -> RType c tv r -> [c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([c] -> RType c tv r -> [c]) -> [c] -> RType c tv r -> [c]
forall acc c tv r.
(acc -> RType c tv r -> acc) -> acc -> RType c tv r -> acc
foldRType [c] -> RType c tv r -> [c]
forall {a} {tv} {r}. [a] -> RType a tv r -> [a]
f []
where
f :: [a] -> RType a tv r -> [a]
f [a]
acc t :: RType a tv r
t@RApp {} = RType a tv r -> a
forall c tv r. RType c tv r -> c
rt_tycon RType a tv r
t a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
acc
f [a]
acc RType a tv r
_ = [a]
acc
knownGhcVar :: Env -> ModName -> LocSymbol -> Bool
knownGhcVar :: Env -> ModName -> LocSymbol -> Bool
knownGhcVar Env
env ModName
name LocSymbol
lx = Maybe Id -> Bool
forall a. Maybe a -> Bool
Mb.isJust Maybe Id
v
where
v :: Maybe Ghc.Var
v :: Maybe Id
v = String -> Maybe Id -> Maybe Id
forall a. PPrint a => String -> a -> a
myTracepp (String
"knownGhcVar " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LocSymbol -> String
forall a. PPrint a => a -> String
F.showpp LocSymbol
lx)
(Maybe Id -> Maybe Id) -> Maybe Id -> Maybe Id
forall a b. (a -> b) -> a -> b
$ Env -> ModName -> String -> LocSymbol -> Maybe Id
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Maybe a
maybeResolveSym Env
env ModName
name String
"known-var" LocSymbol
lx
knownGhcTyCon :: Env -> ModName -> LocSymbol -> Bool
knownGhcTyCon :: Env -> ModName -> LocSymbol -> Bool
knownGhcTyCon Env
env ModName
name LocSymbol
lx = String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
myTracepp String
msg (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Maybe TyCon -> Bool
forall a. Maybe a -> Bool
Mb.isJust Maybe TyCon
v
where
msg :: String
msg = String
"knownGhcTyCon: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LocSymbol -> String
forall a. PPrint a => a -> String
F.showpp LocSymbol
lx
v :: Maybe Ghc.TyCon
v :: Maybe TyCon
v = Env -> ModName -> String -> LocSymbol -> Maybe TyCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Maybe a
maybeResolveSym Env
env ModName
name String
"known-tycon" LocSymbol
lx
knownGhcDataCon :: Env -> ModName -> LocSymbol -> Bool
knownGhcDataCon :: Env -> ModName -> LocSymbol -> Bool
knownGhcDataCon Env
env ModName
name LocSymbol
lx = Maybe DataCon -> Bool
forall a. Maybe a -> Bool
Mb.isJust Maybe DataCon
v
where
v :: Maybe Ghc.DataCon
v :: Maybe DataCon
v = String -> Maybe DataCon -> Maybe DataCon
forall a. PPrint a => String -> a -> a
myTracepp (String
"knownGhcDataCon" String -> String -> String
forall a. [a] -> [a] -> [a]
++ LocSymbol -> String
forall a. PPrint a => a -> String
F.showpp LocSymbol
lx)
(Maybe DataCon -> Maybe DataCon) -> Maybe DataCon -> Maybe DataCon
forall a b. (a -> b) -> a -> b
$ Env -> ModName -> String -> LocSymbol -> Maybe DataCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Maybe a
maybeResolveSym Env
env ModName
name String
"known-datacon" LocSymbol
lx
class ResolveSym a where
resolveLocSym :: Env -> ModName -> String -> LocSymbol -> Lookup a
instance ResolveSym Ghc.Var where
resolveLocSym :: Env -> ModName -> String -> LocSymbol -> Lookup Id
resolveLocSym = Doc
-> (TyThing -> Maybe Id)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup Id
forall a.
PPrint a =>
Doc
-> (TyThing -> Maybe a)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup a
resolveWith Doc
"variable" ((TyThing -> Maybe Id)
-> Env -> ModName -> String -> LocSymbol -> Lookup Id)
-> (TyThing -> Maybe Id)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup Id
forall a b. (a -> b) -> a -> b
$ \case
Ghc.AnId Id
x -> Id -> Maybe Id
forall a. a -> Maybe a
Just Id
x
TyThing
_ -> Maybe Id
forall a. Maybe a
Nothing
instance ResolveSym Ghc.TyCon where
resolveLocSym :: Env -> ModName -> String -> LocSymbol -> Lookup TyCon
resolveLocSym = Doc
-> (TyThing -> Maybe TyCon)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup TyCon
forall a.
PPrint a =>
Doc
-> (TyThing -> Maybe a)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup a
resolveWith Doc
"type constructor" ((TyThing -> Maybe TyCon)
-> Env -> ModName -> String -> LocSymbol -> Lookup TyCon)
-> (TyThing -> Maybe TyCon)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup TyCon
forall a b. (a -> b) -> a -> b
$ \case
Ghc.ATyCon TyCon
x -> TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just TyCon
x
TyThing
_ -> Maybe TyCon
forall a. Maybe a
Nothing
instance ResolveSym Ghc.DataCon where
resolveLocSym :: Env -> ModName -> String -> LocSymbol -> Lookup DataCon
resolveLocSym = Doc
-> (TyThing -> Maybe DataCon)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup DataCon
forall a.
PPrint a =>
Doc
-> (TyThing -> Maybe a)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup a
resolveWith Doc
"data constructor" ((TyThing -> Maybe DataCon)
-> Env -> ModName -> String -> LocSymbol -> Lookup DataCon)
-> (TyThing -> Maybe DataCon)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup DataCon
forall a b. (a -> b) -> a -> b
$ \case
Ghc.AConLike (Ghc.RealDataCon DataCon
x) -> DataCon -> Maybe DataCon
forall a. a -> Maybe a
Just DataCon
x
TyThing
_ -> Maybe DataCon
forall a. Maybe a
Nothing
instance ResolveSym F.Symbol where
resolveLocSym :: Env -> ModName -> String -> LocSymbol -> Lookup Symbol
resolveLocSym Env
env ModName
name String
_ LocSymbol
lx =
let resolved :: Lookup Id
resolved = Env -> ModName -> String -> LocSymbol -> Lookup Id
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
"Var" LocSymbol
lx
Lookup Id -> Lookup Id -> Lookup Id
forall a. Semigroup a => a -> a -> a
<> Doc
-> (TyThing -> Maybe Id)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup Id
forall a.
PPrint a =>
Doc
-> (TyThing -> Maybe a)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup a
resolveWith Doc
"variable" TyThing -> Maybe Id
lookupVarInsideRealDataCon Env
env ModName
name String
"Var" LocSymbol
lx
in case Lookup Id
resolved of
Left [Error]
_ -> Symbol -> Lookup Symbol
forall a b. b -> Either a b
Right (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
lx)
Right (Id
v :: Ghc.Var) -> Symbol -> Lookup Symbol
forall a b. b -> Either a b
Right (Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
v)
where
lookupVarInsideRealDataCon :: Ghc.TyThing -> Maybe Ghc.Var
lookupVarInsideRealDataCon :: TyThing -> Maybe Id
lookupVarInsideRealDataCon = \case
Ghc.AConLike (Ghc.RealDataCon DataCon
x) -> Id -> Maybe Id
forall a. a -> Maybe a
Just (DataCon -> Id
Ghc.dataConWorkId DataCon
x)
TyThing
_ -> Maybe Id
forall a. Maybe a
Nothing
resolveWith :: (PPrint a) => PJ.Doc -> (Ghc.TyThing -> Maybe a) -> Env -> ModName -> String -> LocSymbol
-> Lookup a
resolveWith :: forall a.
PPrint a =>
Doc
-> (TyThing -> Maybe a)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup a
resolveWith Doc
kind TyThing -> Maybe a
f Env
env ModName
name String
str LocSymbol
lx =
case (TyThing -> Maybe a) -> [((Int, Symbol), TyThing)] -> [a]
forall k a b. EqHash k => (a -> Maybe b) -> [(k, a)] -> [b]
rankedThings TyThing -> Maybe a
f [((Int, Symbol), TyThing)]
things of
[] -> [Error] -> Lookup a
forall a b. a -> Either a b
Left [Doc -> String -> LocSymbol -> Error
errResolve Doc
kind String
str LocSymbol
lx]
[a
x] -> a -> Lookup a
forall a b. b -> Either a b
Right a
x
[a]
xs -> [Error] -> Lookup a
forall a b. a -> Either a b
Left [SrcSpan -> Doc -> [Doc] -> Error
forall t. SrcSpan -> Doc -> [Doc] -> TError t
ErrDupNames SrcSpan
sp (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lx)) (a -> Doc
forall a. PPrint a => a -> Doc
pprint (a -> Doc) -> [a] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
xs)]
where
_xSym :: Symbol
_xSym = LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lx
sp :: SrcSpan
sp = SrcSpan -> SrcSpan
GM.fSrcSpanSrcSpan (LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan LocSymbol
lx)
things :: [((Int, Symbol), TyThing)]
things = String -> [((Int, Symbol), TyThing)] -> [((Int, Symbol), TyThing)]
forall a. PPrint a => String -> a -> a
myTracepp String
msg ([((Int, Symbol), TyThing)] -> [((Int, Symbol), TyThing)])
-> [((Int, Symbol), TyThing)] -> [((Int, Symbol), TyThing)]
forall a b. (a -> b) -> a -> b
$ Env -> ModName -> LocSymbol -> [((Int, Symbol), TyThing)]
lookupTyThing Env
env ModName
name LocSymbol
lx
msg :: String
msg = String
"resolveWith: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. PPrint a => a -> String
F.showpp (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
lx)
rankedThings :: (Misc.EqHash k) => (a -> Maybe b) -> [(k, a)] -> [b]
rankedThings :: forall k a b. EqHash k => (a -> Maybe b) -> [(k, a)] -> [b]
rankedThings a -> Maybe b
f [(k, a)]
ias = case ((k, [b]) -> k) -> [(k, [b])] -> [(k, [b])]
forall b a. Ord b => (a -> b) -> [a] -> [a]
Misc.sortOn (k, [b]) -> k
forall a b. (a, b) -> a
fst ([(k, b)] -> [(k, [b])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(k, b)]
ibs) of
(k
_,[b]
ts):[(k, [b])]
_ -> [b]
ts
[] -> []
where
ibs :: [(k, b)]
ibs = ((k, a) -> Maybe (k, b)) -> [(k, a)] -> [(k, b)]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (\(k
k, a
x) -> (k
k,) (b -> (k, b)) -> Maybe b -> Maybe (k, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe b
f a
x) [(k, a)]
ias
lookupTyThing :: Env -> ModName -> LocSymbol -> [((Int, F.Symbol), Ghc.TyThing)]
lookupTyThing :: Env -> ModName -> LocSymbol -> [((Int, Symbol), TyThing)]
lookupTyThing Env
env ModName
mdname LocSymbol
lsym = [ ((Int, Symbol)
k, TyThing
t) | ((Int, Symbol)
k, [TyThing]
ts) <- [((Int, Symbol), [TyThing])]
ordMatches, TyThing
t <- [TyThing]
ts]
where
ordMatches :: [((Int, Symbol), [TyThing])]
ordMatches = (((Int, Symbol), [TyThing]) -> (Int, Symbol))
-> [((Int, Symbol), [TyThing])] -> [((Int, Symbol), [TyThing])]
forall b a. Ord b => (a -> b) -> [a] -> [a]
Misc.sortOn ((Int, Symbol), [TyThing]) -> (Int, Symbol)
forall a b. (a, b) -> a
fst ([((Int, Symbol), TyThing)] -> [((Int, Symbol), [TyThing])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [((Int, Symbol), TyThing)]
matches)
matches :: [((Int, Symbol), TyThing)]
matches = String -> [((Int, Symbol), TyThing)] -> [((Int, Symbol), TyThing)]
forall a. PPrint a => String -> a -> a
myTracepp (String
"matches-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg)
[ ((Int
k, Symbol
m), TyThing
t) | (Symbol
m, TyThing
t) <- Env -> Symbol -> [(Symbol, TyThing)]
lookupThings Env
env Symbol
x
, Int
k <- String -> [Int] -> [Int]
forall a. PPrint a => String -> a -> a
myTracepp String
msg ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol -> Maybe [Symbol] -> [Int]
mm Symbol
nameSym Symbol
m Maybe [Symbol]
mds ]
msg :: String
msg = String
"lookupTyThing: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (LocSymbol, Symbol, Maybe [Symbol]) -> String
forall a. PPrint a => a -> String
F.showpp (LocSymbol
lsym, Symbol
x, Maybe [Symbol]
mds)
(Symbol
x, Maybe [Symbol]
mds) = Env -> Symbol -> (Symbol, Maybe [Symbol])
symbolModules Env
env (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lsym)
nameSym :: Symbol
nameSym = ModName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ModName
mdname
mm :: Symbol -> Symbol -> Maybe [Symbol] -> [Int]
mm Symbol
name Symbol
m Maybe [Symbol]
mods = String -> [Int] -> [Int]
forall a. PPrint a => String -> a -> a
myTracepp (String
"matchMod: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (LocSymbol, Symbol, Symbol, Maybe [Symbol]) -> String
forall a. PPrint a => a -> String
F.showpp (LocSymbol
lsym, Symbol
name, Symbol
m, Maybe [Symbol]
mods)) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$
Env -> Symbol -> Symbol -> Maybe [Symbol] -> [Int]
matchMod Env
env Symbol
name Symbol
m Maybe [Symbol]
mods
lookupThings :: Env -> F.Symbol -> [(F.Symbol, Ghc.TyThing)]
lookupThings :: Env -> Symbol -> [(Symbol, TyThing)]
lookupThings Env
env Symbol
x = String -> [(Symbol, TyThing)] -> [(Symbol, TyThing)]
forall a. PPrint a => String -> a -> a
myTracepp (String
"lookupThings: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. PPrint a => a -> String
F.showpp Symbol
x)
([(Symbol, TyThing)] -> [(Symbol, TyThing)])
-> [(Symbol, TyThing)] -> [(Symbol, TyThing)]
forall a b. (a -> b) -> a -> b
$ [(Symbol, TyThing)]
-> Maybe [(Symbol, TyThing)] -> [(Symbol, TyThing)]
forall a. a -> Maybe a -> a
Mb.fromMaybe [] (Maybe [(Symbol, TyThing)] -> [(Symbol, TyThing)])
-> Maybe [(Symbol, TyThing)] -> [(Symbol, TyThing)]
forall a b. (a -> b) -> a -> b
$ Symbol -> Maybe [(Symbol, TyThing)]
get Symbol
x Maybe [(Symbol, TyThing)]
-> Maybe [(Symbol, TyThing)] -> Maybe [(Symbol, TyThing)]
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Symbol -> Maybe [(Symbol, TyThing)]
get (Symbol -> Symbol
GM.stripParensSym Symbol
x)
where
get :: Symbol -> Maybe [(Symbol, TyThing)]
get Symbol
z = Symbol -> TyThingMap -> Maybe [(Symbol, TyThing)]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
z (Env -> TyThingMap
_reTyThings Env
env)
matchMod :: Env -> F.Symbol -> F.Symbol -> Maybe [F.Symbol] -> [Int]
matchMod :: Env -> Symbol -> Symbol -> Maybe [Symbol] -> [Int]
matchMod Env
env Symbol
tgtName Symbol
defName = Maybe [Symbol] -> [Int]
go
where
go :: Maybe [Symbol] -> [Int]
go Maybe [Symbol]
Nothing
| Symbol
defName Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
tgtName = [Int
0]
| Bool
otherwise = [Env -> Symbol -> Int -> Int
matchImp Env
env Symbol
defName Int
1]
go (Just [Symbol]
ms)
| Symbol -> Bool
isEmptySymbol Symbol
defName
Bool -> Bool -> Bool
&& [Symbol]
ms [Symbol] -> [Symbol] -> Bool
forall a. Eq a => a -> a -> Bool
== [Symbol
tgtName] = [Int
0]
| [Symbol]
ms [Symbol] -> [Symbol] -> Bool
forall a. Eq a => a -> a -> Bool
== [Symbol
defName] = [Int
1]
| Bool
isExt = [Env -> Symbol -> Int -> Int
matchImp Env
env Symbol
defName Int
2]
| Bool
otherwise = []
where
isExt :: Bool
isExt = (Symbol -> Bool) -> [Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol -> Symbol -> Bool
`isParentModuleOf` Symbol
defName) [Symbol]
ms
isParentModuleOf :: F.Symbol -> F.Symbol -> Bool
isParentModuleOf :: Symbol -> Symbol -> Bool
isParentModuleOf Symbol
parentModule Symbol
childModule
| Symbol -> Bool
isEmptySymbol Symbol
parentModule = Bool
True
| Bool
otherwise =
[Text] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Text]
parentHierarchy Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Text] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Text]
childHierarchy Bool -> Bool -> Bool
&& ((Text, Text) -> Bool) -> [(Text, Text)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Text -> Text -> Bool) -> (Text, Text) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
(==)) ([Text] -> [Text] -> [(Text, Text)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Text]
parentHierarchy [Text]
childHierarchy)
where
parentHierarchy :: [T.Text]
parentHierarchy :: [Text]
parentHierarchy = HasCallStack => Text -> Text -> [Text]
Text -> Text -> [Text]
T.splitOn Text
"." (Text -> [Text]) -> (Symbol -> Text) -> Symbol -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
F.symbolText (Symbol -> [Text]) -> Symbol -> [Text]
forall a b. (a -> b) -> a -> b
$ Symbol
parentModule
childHierarchy :: [T.Text]
childHierarchy :: [Text]
childHierarchy = HasCallStack => Text -> Text -> [Text]
Text -> Text -> [Text]
T.splitOn Text
"." (Text -> [Text]) -> (Symbol -> Text) -> Symbol -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
F.symbolText (Symbol -> [Text]) -> Symbol -> [Text]
forall a b. (a -> b) -> a -> b
$ Symbol
childModule
symbolModules :: Env -> F.Symbol -> (F.Symbol, Maybe [F.Symbol])
symbolModules :: Env -> Symbol -> (Symbol, Maybe [Symbol])
symbolModules Env
env Symbol
s = (Symbol
x, Symbol -> [Symbol]
glerb (Symbol -> [Symbol]) -> Maybe Symbol -> Maybe [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Symbol
modMb)
where
(Maybe Symbol
modMb, Symbol
x) = Symbol -> (Maybe Symbol, Symbol)
unQualifySymbol Symbol
s
glerb :: Symbol -> [Symbol]
glerb Symbol
m = [Symbol] -> Symbol -> HashMap Symbol [Symbol] -> [Symbol]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [Symbol
m] Symbol
m HashMap Symbol [Symbol]
qImps
qImps :: HashMap Symbol [Symbol]
qImps = QImports -> HashMap Symbol [Symbol]
qiNames (Env -> QImports
reQualImps Env
env)
matchImp :: Env -> F.Symbol -> Int -> Int
matchImp :: Env -> Symbol -> Int -> Int
matchImp Env
env Symbol
defName Int
i
| Bool
isUnqualImport = Int
i
| Bool
isQualImport = Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2
| Bool
otherwise = Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
where
isUnqualImport :: Bool
isUnqualImport = Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
defName (Env -> HashSet Symbol
reAllImps Env
env) Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
isQualImport
isQualImport :: Bool
isQualImport = Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
defName (QImports -> HashSet Symbol
qiModules (Env -> QImports
reQualImps Env
env))
unQualifySymbol :: F.Symbol -> (Maybe F.Symbol, F.Symbol)
unQualifySymbol :: Symbol -> (Maybe Symbol, Symbol)
unQualifySymbol Symbol
sym
| Symbol -> Bool
GM.isQualifiedSym Symbol
sym = (Symbol -> Maybe Symbol)
-> (Symbol, Symbol) -> (Maybe Symbol, Symbol)
forall a c b. (a -> c) -> (a, b) -> (c, b)
Misc.mapFst Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just (Symbol -> (Symbol, Symbol)
splitModuleNameExact Symbol
sym)
| Bool
otherwise = (Maybe Symbol
forall a. Maybe a
Nothing, Symbol
sym)
splitModuleNameExact :: F.Symbol -> (F.Symbol, F.Symbol)
splitModuleNameExact :: Symbol -> (Symbol, Symbol)
splitModuleNameExact Symbol
x' = String -> (Symbol, Symbol) -> (Symbol, Symbol)
forall a. PPrint a => String -> a -> a
myTracepp (String
"splitModuleNameExact for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. PPrint a => a -> String
F.showpp Symbol
x)
(Symbol -> Symbol
GM.takeModuleNames Symbol
x, Symbol -> Symbol
GM.dropModuleNames Symbol
x)
where
x :: Symbol
x = Symbol -> Symbol
GM.stripParensSym Symbol
x'
errResolve :: PJ.Doc -> String -> LocSymbol -> Error
errResolve :: Doc -> String -> LocSymbol -> Error
errResolve Doc
k String
msg LocSymbol
lx = SrcSpan -> Doc -> Doc -> Doc -> Error
forall t. SrcSpan -> Doc -> Doc -> Doc -> TError t
ErrResolve (LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSymbol
lx) Doc
k (Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lx)) (String -> Doc
PJ.text String
msg)
maybeResolveSym :: (ResolveSym a) => Env -> ModName -> String -> LocSymbol -> Maybe a
maybeResolveSym :: forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Maybe a
maybeResolveSym Env
env ModName
name String
kind LocSymbol
x = case Env -> ModName -> String -> LocSymbol -> Lookup a
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
kind LocSymbol
x of
Left [Error]
_ -> Maybe a
forall a. Maybe a
Nothing
Right a
val -> a -> Maybe a
forall a. a -> Maybe a
Just a
val
ofBareType :: Env -> ModName -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> SpecType
ofBareType :: Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> BareType
-> SpecType
ofBareType Env
env ModName
name SourcePos
l Maybe [PVar BSort]
ps BareType
t = ([Error] -> SpecType)
-> (SpecType -> SpecType) -> Lookup SpecType -> SpecType
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either [Error] -> SpecType
forall {a}. [Error] -> a
fail' SpecType -> SpecType
forall a. a -> a
id (Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> BareType
-> Lookup SpecType
ofBareTypeE Env
env ModName
name SourcePos
l Maybe [PVar BSort]
ps BareType
t)
where
fail' :: [Error] -> a
fail' = [Error] -> a
forall a e. Exception e => e -> a
Ex.throw
ofBareTypeE :: Env -> ModName -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> Lookup SpecType
ofBareTypeE :: Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> BareType
-> Lookup SpecType
ofBareTypeE Env
env ModName
name SourcePos
l Maybe [PVar BSort]
ps BareType
t = Env
-> ModName
-> ([Symbol] -> RReft -> RReft)
-> SourcePos
-> BareType
-> Lookup SpecType
forall r.
Expandable r =>
Env
-> ModName
-> ([Symbol] -> r -> r)
-> SourcePos
-> BRType r
-> Lookup (RRType r)
ofBRType Env
env ModName
name (Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> BareType
-> [Symbol]
-> RReft
-> RReft
resolveReft Env
env ModName
name SourcePos
l Maybe [PVar BSort]
ps BareType
t) SourcePos
l BareType
t
resolveReft :: Env -> ModName -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> [F.Symbol] -> RReft -> RReft
resolveReft :: Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> BareType
-> [Symbol]
-> RReft
-> RReft
resolveReft Env
env ModName
name SourcePos
l Maybe [PVar BSort]
ps BareType
t [Symbol]
bs
= Env -> ModName -> SourcePos -> [Symbol] -> RReft -> RReft
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs
(RReft -> RReft) -> (RReft -> RReft) -> RReft -> RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourcePos
-> ((UsedPVar -> UsedPVar) -> RReft -> RReft)
-> [UsedPVar]
-> BareType
-> RReft
-> RReft
forall t c tv r.
SourcePos
-> ((UsedPVar -> UsedPVar) -> t) -> [UsedPVar] -> RType c tv r -> t
txParam SourcePos
l (UsedPVar -> UsedPVar) -> RReft -> RReft
RT.subvUReft (PVar BSort -> UsedPVar
forall t. PVar t -> UsedPVar
RT.uPVar (PVar BSort -> UsedPVar) -> [PVar BSort] -> [UsedPVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVar BSort]
πs) BareType
t
(RReft -> RReft) -> (RReft -> RReft) -> RReft -> RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareType -> RReft -> RReft
fixReftTyVars BareType
t
where
πs :: [PVar BSort]
πs = [PVar BSort] -> Maybe [PVar BSort] -> [PVar BSort]
forall a. a -> Maybe a -> a
Mb.fromMaybe [PVar BSort]
tπs Maybe [PVar BSort]
ps
tπs :: [PVar BSort]
tπs = RTypeRep BTyCon BTyVar RReft -> [PVar BSort]
forall c tv r. RTypeRep c tv r -> [PVar (RType c tv ())]
ty_preds (BareType -> RTypeRep BTyCon BTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep BareType
t)
fixReftTyVars :: BareType -> RReft -> RReft
fixReftTyVars :: BareType -> RReft -> RReft
fixReftTyVars BareType
bt = CoSub -> RReft -> RReft
coSubRReft CoSub
coSub
where
coSub :: CoSub
coSub = [(Symbol, Sort)] -> CoSub
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (BTyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol BTyVar
a, Symbol -> Sort
F.FObj (BTyVar -> Symbol
specTvSymbol BTyVar
a)) | BTyVar
a <- [BTyVar]
tvs ]
tvs :: [BTyVar]
tvs = BareType -> [BTyVar]
forall tv c r. Ord tv => RType c tv r -> [tv]
RT.allTyVars BareType
bt
specTvSymbol :: BTyVar -> Symbol
specTvSymbol = RTyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (RTyVar -> Symbol) -> (BTyVar -> RTyVar) -> BTyVar -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BTyVar -> RTyVar
RT.bareRTyVar
coSubRReft :: F.CoSub -> RReft -> RReft
coSubRReft :: CoSub -> RReft -> RReft
coSubRReft CoSub
su RReft
r = RReft
r { ur_reft = coSubReft su (ur_reft r) }
coSubReft :: F.CoSub -> F.Reft -> F.Reft
coSubReft :: CoSub -> Reft -> Reft
coSubReft CoSub
su (F.Reft (Symbol
x, Expr
e)) = (Symbol, Expr) -> Reft
F.Reft (Symbol
x, CoSub -> Expr -> Expr
F.applyCoSub CoSub
su Expr
e)
ofBSort :: Env -> ModName -> F.SourcePos -> BSort -> RSort
ofBSort :: Env -> ModName -> SourcePos -> BSort -> RType RTyCon RTyVar ()
ofBSort Env
env ModName
name SourcePos
l BSort
t = ([Error] -> RType RTyCon RTyVar ())
-> (RType RTyCon RTyVar () -> RType RTyCon RTyVar ())
-> Either [Error] (RType RTyCon RTyVar ())
-> RType RTyCon RTyVar ()
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (String -> String -> RType RTyCon RTyVar ()
forall a. String -> String -> a
Misc.errorP String
"error-ofBSort" (String -> RType RTyCon RTyVar ())
-> ([Error] -> String) -> [Error] -> RType RTyCon RTyVar ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Error] -> String
forall a. PPrint a => a -> String
F.showpp) RType RTyCon RTyVar () -> RType RTyCon RTyVar ()
forall a. a -> a
id (Env
-> ModName
-> SourcePos
-> BSort
-> Either [Error] (RType RTyCon RTyVar ())
ofBSortE Env
env ModName
name SourcePos
l BSort
t)
ofBSortE :: Env -> ModName -> F.SourcePos -> BSort -> Lookup RSort
ofBSortE :: Env
-> ModName
-> SourcePos
-> BSort
-> Either [Error] (RType RTyCon RTyVar ())
ofBSortE Env
env ModName
name SourcePos
l BSort
t = Env
-> ModName
-> ([Symbol] -> () -> ())
-> SourcePos
-> BSort
-> Either [Error] (RType RTyCon RTyVar ())
forall r.
Expandable r =>
Env
-> ModName
-> ([Symbol] -> r -> r)
-> SourcePos
-> BRType r
-> Lookup (RRType r)
ofBRType Env
env ModName
name ((() -> ()) -> [Symbol] -> () -> ()
forall a b. a -> b -> a
const () -> ()
forall a. a -> a
id) SourcePos
l BSort
t
ofBPVar :: Env -> ModName -> F.SourcePos -> BPVar -> RPVar
ofBPVar :: Env -> ModName -> SourcePos -> PVar BSort -> RPVar
ofBPVar Env
env ModName
name SourcePos
l = (BSort -> RType RTyCon RTyVar ()) -> PVar BSort -> RPVar
forall a b. (a -> b) -> PVar a -> PVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> ModName -> SourcePos -> BSort -> RType RTyCon RTyVar ()
ofBSort Env
env ModName
name SourcePos
l)
txParam :: F.SourcePos -> ((UsedPVar -> UsedPVar) -> t) -> [UsedPVar] -> RType c tv r -> t
txParam :: forall t c tv r.
SourcePos
-> ((UsedPVar -> UsedPVar) -> t) -> [UsedPVar] -> RType c tv r -> t
txParam SourcePos
l (UsedPVar -> UsedPVar) -> t
f [UsedPVar]
πs RType c tv r
t = (UsedPVar -> UsedPVar) -> t
f (SourcePos -> HashMap Symbol UsedPVar -> UsedPVar -> UsedPVar
txPvar SourcePos
l ([UsedPVar] -> RType c tv r -> HashMap Symbol UsedPVar
forall c tv r.
[UsedPVar] -> RType c tv r -> HashMap Symbol UsedPVar
predMap [UsedPVar]
πs RType c tv r
t))
txPvar :: F.SourcePos -> M.HashMap F.Symbol UsedPVar -> UsedPVar -> UsedPVar
txPvar :: SourcePos -> HashMap Symbol UsedPVar -> UsedPVar -> UsedPVar
txPvar SourcePos
l HashMap Symbol UsedPVar
m UsedPVar
π = UsedPVar
π { pargs = args' }
where
args' :: [((), Symbol, Expr)]
args' | Bool -> Bool
not ([((), Symbol, Expr)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (UsedPVar -> [((), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
π)) = (((), Symbol, Expr) -> ((), Symbol, Expr) -> ((), Symbol, Expr))
-> [((), Symbol, Expr)]
-> [((), Symbol, Expr)]
-> [((), Symbol, Expr)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(()
_,Symbol
x ,Expr
_) (()
t,Symbol
_,Expr
y) -> (()
t, Symbol
x, Expr
y)) (UsedPVar -> [((), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
π') (UsedPVar -> [((), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
π)
| Bool
otherwise = UsedPVar -> [((), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
π'
π' :: UsedPVar
π' = UsedPVar -> Maybe UsedPVar -> UsedPVar
forall a. a -> Maybe a -> a
Mb.fromMaybe UsedPVar
forall {a}. a
err (Maybe UsedPVar -> UsedPVar) -> Maybe UsedPVar -> UsedPVar
forall a b. (a -> b) -> a -> b
$ Symbol -> HashMap Symbol UsedPVar -> Maybe UsedPVar
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (UsedPVar -> Symbol
forall t. PVar t -> Symbol
pname UsedPVar
π) HashMap Symbol UsedPVar
m
err :: a
err = UserError -> a
forall a. UserError -> a
uError (UserError -> a) -> UserError -> a
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> UserError
forall t. SrcSpan -> Doc -> TError t
ErrUnbPred SrcSpan
sp (UsedPVar -> Doc
forall a. PPrint a => a -> Doc
pprint UsedPVar
π)
sp :: SrcSpan
sp = SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l
predMap :: [UsedPVar] -> RType c tv r -> M.HashMap F.Symbol UsedPVar
predMap :: forall c tv r.
[UsedPVar] -> RType c tv r -> HashMap Symbol UsedPVar
predMap [UsedPVar]
πs RType c tv r
t = [(Symbol, UsedPVar)] -> HashMap Symbol UsedPVar
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(UsedPVar -> Symbol
forall t. PVar t -> Symbol
pname UsedPVar
π, UsedPVar
π) | UsedPVar
π <- [UsedPVar]
πs [UsedPVar] -> [UsedPVar] -> [UsedPVar]
forall a. [a] -> [a] -> [a]
++ RType c tv r -> [UsedPVar]
forall c tv r. RType c tv r -> [UsedPVar]
rtypePredBinds RType c tv r
t]
rtypePredBinds :: RType c tv r -> [UsedPVar]
rtypePredBinds :: forall c tv r. RType c tv r -> [UsedPVar]
rtypePredBinds = (PVar (RType c tv ()) -> UsedPVar)
-> [PVar (RType c tv ())] -> [UsedPVar]
forall a b. (a -> b) -> [a] -> [b]
map PVar (RType c tv ()) -> UsedPVar
forall t. PVar t -> UsedPVar
RT.uPVar ([PVar (RType c tv ())] -> [UsedPVar])
-> (RType c tv r -> [PVar (RType c tv ())])
-> RType c tv r
-> [UsedPVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeRep c tv r -> [PVar (RType c tv ())]
forall c tv r. RTypeRep c tv r -> [PVar (RType c tv ())]
ty_preds (RTypeRep c tv r -> [PVar (RType c tv ())])
-> (RType c tv r -> RTypeRep c tv r)
-> RType c tv r
-> [PVar (RType c tv ())]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType c tv r -> RTypeRep c tv r
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep
type Expandable r = ( PPrint r
, F.Reftable r
, SubsTy RTyVar (RType RTyCon RTyVar ()) r
, F.Reftable (RTProp RTyCon RTyVar r))
ofBRType :: (Expandable r) => Env -> ModName -> ([F.Symbol] -> r -> r) -> F.SourcePos -> BRType r
-> Lookup (RRType r)
ofBRType :: forall r.
Expandable r =>
Env
-> ModName
-> ([Symbol] -> r -> r)
-> SourcePos
-> BRType r
-> Lookup (RRType r)
ofBRType Env
env ModName
name [Symbol] -> r -> r
f SourcePos
l = [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go []
where
goReft :: [Symbol] -> r -> m r
goReft [Symbol]
bs r
r = r -> m r
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Symbol] -> r -> r
f [Symbol]
bs r
r)
goRFun :: [Symbol]
-> Symbol
-> RFInfo
-> RType BTyCon BTyVar r
-> RType BTyCon BTyVar r
-> r
-> Either [Error] (RType RTyCon RTyVar r)
goRFun [Symbol]
bs Symbol
x RFInfo
i RType BTyCon BTyVar r
t1 RType BTyCon BTyVar r
t2 r
r = Symbol
-> RFInfo
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> r
-> RType RTyCon RTyVar r
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i{permitTC = Just (typeclass (getConfig env))} (RType RTyCon RTyVar r
-> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either
[Error] (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Symbol -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall {r} {c} {tv}.
(Reftable r, TyConable c) =>
Symbol -> RType c tv r -> RType c tv r
rebind Symbol
x (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t1) Either
[Error] (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (r -> RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
bs) RType BTyCon BTyVar r
t2 Either [Error] (r -> RType RTyCon RTyVar r)
-> Either [Error] r -> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
rebind :: Symbol -> RType c tv r -> RType c tv r
rebind Symbol
x RType c tv r
t = RType c tv r -> (Symbol, Expr) -> RType c tv r
forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 RType c tv r
t (Symbol
x, Symbol -> Expr
F.EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ RType c tv r -> Symbol
forall r c tv. Reftable r => RType c tv r -> Symbol
rTypeValueVar RType c tv r
t)
go :: [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs (RAppTy RType BTyCon BTyVar r
t1 RType BTyCon BTyVar r
t2 r
r) = RType RTyCon RTyVar r
-> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy (RType RTyCon RTyVar r
-> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either
[Error] (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t1 Either
[Error] (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (r -> RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t2 Either [Error] (r -> RType RTyCon RTyVar r)
-> Either [Error] r -> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
go [Symbol]
bs (RApp BTyCon
tc [RType BTyCon BTyVar r]
ts [RTProp BTyCon BTyVar r]
rs r
r) = [Symbol]
-> BTyCon
-> [RType BTyCon BTyVar r]
-> [RTProp BTyCon BTyVar r]
-> r
-> Either [Error] (RType RTyCon RTyVar r)
goRApp [Symbol]
bs BTyCon
tc [RType BTyCon BTyVar r]
ts [RTProp BTyCon BTyVar r]
rs r
r
go [Symbol]
bs (RFun Symbol
x RFInfo
i RType BTyCon BTyVar r
t1 RType BTyCon BTyVar r
t2 r
r) = [Symbol]
-> Symbol
-> RFInfo
-> RType BTyCon BTyVar r
-> RType BTyCon BTyVar r
-> r
-> Either [Error] (RType RTyCon RTyVar r)
goRFun [Symbol]
bs Symbol
x RFInfo
i RType BTyCon BTyVar r
t1 RType BTyCon BTyVar r
t2 r
r
go [Symbol]
bs (RVar BTyVar
a r
r) = RTyVar -> r -> RType RTyCon RTyVar r
forall c tv r. tv -> r -> RType c tv r
RVar (BTyVar -> RTyVar
RT.bareRTyVar BTyVar
a) (r -> RType RTyCon RTyVar r)
-> Either [Error] r -> Either [Error] (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
go [Symbol]
bs (RAllT RTVU BTyCon BTyVar
a RType BTyCon BTyVar r
t r
r) = RTVar RTyVar (RType RTyCon RTyVar ())
-> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVar RTyVar (RType RTyCon RTyVar ())
forall {s2}. RTVar RTyVar s2
a' (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t Either [Error] (r -> RType RTyCon RTyVar r)
-> Either [Error] r -> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
where a' :: RTVar RTyVar s2
a' = RTVar RTyVar BSort -> RTVar RTyVar s2
forall tv s1 s2. RTVar tv s1 -> RTVar tv s2
dropTyVarInfo ((BTyVar -> RTyVar) -> RTVU BTyCon BTyVar -> RTVar RTyVar BSort
forall tv1 tv2 s. (tv1 -> tv2) -> RTVar tv1 s -> RTVar tv2 s
mapTyVarValue BTyVar -> RTyVar
RT.bareRTyVar RTVU BTyCon BTyVar
a)
go [Symbol]
bs (RAllP PVar BSort
a RType BTyCon BTyVar r
t) = RPVar -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP RPVar
a' (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t
where a' :: RPVar
a' = Env -> ModName -> SourcePos -> PVar BSort -> RPVar
ofBPVar Env
env ModName
name SourcePos
l PVar BSort
a
go [Symbol]
bs (RAllE Symbol
x RType BTyCon BTyVar r
t1 RType BTyCon BTyVar r
t2) = Symbol
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
x (RType RTyCon RTyVar r
-> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t1 Either [Error] (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t2
go [Symbol]
bs (REx Symbol
x RType BTyCon BTyVar r
t1 RType BTyCon BTyVar r
t2) = Symbol
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx Symbol
x (RType RTyCon RTyVar r
-> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t1 Either [Error] (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
bs) RType BTyCon BTyVar r
t2
go [Symbol]
bs (RRTy [(Symbol, RType BTyCon BTyVar r)]
xts r
r Oblig
o RType BTyCon BTyVar r
t) = [(Symbol, RType RTyCon RTyVar r)]
-> r -> Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy ([(Symbol, RType RTyCon RTyVar r)]
-> r -> Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] [(Symbol, RType RTyCon RTyVar r)]
-> Either
[Error]
(r -> Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either [Error] [(Symbol, RType RTyCon RTyVar r)]
xts' Either
[Error]
(r -> Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] r
-> Either
[Error] (Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r Either
[Error] (Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] Oblig
-> Either [Error] (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Oblig -> Either [Error] Oblig
forall a. a -> Either [Error] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Oblig
o Either [Error] (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t
where xts' :: Either [Error] [(Symbol, RType RTyCon RTyVar r)]
xts' = ((Symbol, RType BTyCon BTyVar r)
-> Either [Error] (Symbol, RType RTyCon RTyVar r))
-> [(Symbol, RType BTyCon BTyVar r)]
-> Either [Error] [(Symbol, RType RTyCon RTyVar r)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r))
-> (Symbol, RType BTyCon BTyVar r)
-> Either [Error] (Symbol, RType RTyCon RTyVar r)
forall (m :: * -> *) b c a.
Applicative m =>
(b -> m c) -> (a, b) -> m (a, c)
Misc.mapSndM ([Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs)) [(Symbol, RType BTyCon BTyVar r)]
xts
go [Symbol]
bs (RHole r
r) = r -> RType RTyCon RTyVar r
forall c tv r. r -> RType c tv r
RHole (r -> RType RTyCon RTyVar r)
-> Either [Error] r -> Either [Error] (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
go [Symbol]
bs (RExprArg Located Expr
le) = RType RTyCon RTyVar r -> Either [Error] (RType RTyCon RTyVar r)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return (RType RTyCon RTyVar r -> Either [Error] (RType RTyCon RTyVar r))
-> RType RTyCon RTyVar r -> Either [Error] (RType RTyCon RTyVar r)
forall a b. (a -> b) -> a -> b
$ Located Expr -> RType RTyCon RTyVar r
forall c tv r. Located Expr -> RType c tv r
RExprArg (Env
-> ModName -> SourcePos -> [Symbol] -> Located Expr -> Located Expr
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs Located Expr
le)
goRef :: [Symbol]
-> RTProp BTyCon BTyVar r
-> Either [Error] (RTProp RTyCon RTyVar r)
goRef [Symbol]
bs (RProp [(Symbol, BSort)]
ss (RHole r
r)) = [(Symbol, RType RTyCon RTyVar ())] -> r -> RTProp RTyCon RTyVar r
forall τ r c tv. [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
rPropP ([(Symbol, RType RTyCon RTyVar ())] -> r -> RTProp RTyCon RTyVar r)
-> Either [Error] [(Symbol, RType RTyCon RTyVar ())]
-> Either [Error] (r -> RTProp RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Symbol, BSort)
-> Either [Error] (Symbol, RType RTyCon RTyVar ()))
-> [(Symbol, BSort)]
-> Either [Error] [(Symbol, RType RTyCon RTyVar ())]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Symbol, BSort) -> Either [Error] (Symbol, RType RTyCon RTyVar ())
forall {t}.
(t, BSort) -> Either [Error] (t, RType RTyCon RTyVar ())
goSyms [(Symbol, BSort)]
ss Either [Error] (r -> RTProp RTyCon RTyVar r)
-> Either [Error] r -> Either [Error] (RTProp RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
goRef [Symbol]
bs (RProp [(Symbol, BSort)]
ss RType BTyCon BTyVar r
t) = [(Symbol, RType RTyCon RTyVar ())]
-> RType RTyCon RTyVar r -> RTProp RTyCon RTyVar r
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp ([(Symbol, RType RTyCon RTyVar ())]
-> RType RTyCon RTyVar r -> RTProp RTyCon RTyVar r)
-> Either [Error] [(Symbol, RType RTyCon RTyVar ())]
-> Either [Error] (RType RTyCon RTyVar r -> RTProp RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Symbol, BSort)
-> Either [Error] (Symbol, RType RTyCon RTyVar ()))
-> [(Symbol, BSort)]
-> Either [Error] [(Symbol, RType RTyCon RTyVar ())]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Symbol, BSort) -> Either [Error] (Symbol, RType RTyCon RTyVar ())
forall {t}.
(t, BSort) -> Either [Error] (t, RType RTyCon RTyVar ())
goSyms [(Symbol, BSort)]
ss Either [Error] (RType RTyCon RTyVar r -> RTProp RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RTProp RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t
goSyms :: (t, BSort) -> Either [Error] (t, RType RTyCon RTyVar ())
goSyms (t
x, BSort
t) = (t
x,) (RType RTyCon RTyVar () -> (t, RType RTyCon RTyVar ()))
-> Either [Error] (RType RTyCon RTyVar ())
-> Either [Error] (t, RType RTyCon RTyVar ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env
-> ModName
-> SourcePos
-> BSort
-> Either [Error] (RType RTyCon RTyVar ())
ofBSortE Env
env ModName
name SourcePos
l BSort
t
goRApp :: [Symbol]
-> BTyCon
-> [RType BTyCon BTyVar r]
-> [RTProp BTyCon BTyVar r]
-> r
-> Either [Error] (RType RTyCon RTyVar r)
goRApp [Symbol]
bs BTyCon
tc [RType BTyCon BTyVar r]
ts [RTProp BTyCon BTyVar r]
rs r
r = r
-> Located TyCon
-> [RTProp RTyCon RTyVar r]
-> [RType RTyCon RTyVar r]
-> RType RTyCon RTyVar r
forall r.
Expandable r =>
r
-> Located TyCon
-> [RTProp RTyCon RTyVar r]
-> [RType RTyCon RTyVar r]
-> RType RTyCon RTyVar r
bareTCApp (r
-> Located TyCon
-> [RTProp RTyCon RTyVar r]
-> [RType RTyCon RTyVar r]
-> RType RTyCon RTyVar r)
-> Either [Error] r
-> Either
[Error]
(Located TyCon
-> [RTProp RTyCon RTyVar r]
-> [RType RTyCon RTyVar r]
-> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r Either
[Error]
(Located TyCon
-> [RTProp RTyCon RTyVar r]
-> [RType RTyCon RTyVar r]
-> RType RTyCon RTyVar r)
-> Either [Error] (Located TyCon)
-> Either
[Error]
([RTProp RTyCon RTyVar r]
-> [RType RTyCon RTyVar r] -> RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Either [Error] (Located TyCon)
lc' Either
[Error]
([RTProp RTyCon RTyVar r]
-> [RType RTyCon RTyVar r] -> RType RTyCon RTyVar r)
-> Either [Error] [RTProp RTyCon RTyVar r]
-> Either
[Error] ([RType RTyCon RTyVar r] -> RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (RTProp BTyCon BTyVar r -> Either [Error] (RTProp RTyCon RTyVar r))
-> [RTProp BTyCon BTyVar r]
-> Either [Error] [RTProp RTyCon RTyVar r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([Symbol]
-> RTProp BTyCon BTyVar r
-> Either [Error] (RTProp RTyCon RTyVar r)
goRef [Symbol]
bs) [RTProp BTyCon BTyVar r]
rs Either [Error] ([RType RTyCon RTyVar r] -> RType RTyCon RTyVar r)
-> Either [Error] [RType RTyCon RTyVar r]
-> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r))
-> [RType BTyCon BTyVar r]
-> Either [Error] [RType RTyCon RTyVar r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs) [RType BTyCon BTyVar r]
ts
where
lc' :: Either [Error] (Located TyCon)
lc' = LocSymbol -> TyCon -> Located TyCon
forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
lc (TyCon -> Located TyCon)
-> Lookup TyCon -> Either [Error] (Located TyCon)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> ModName -> LocSymbol -> Int -> Lookup TyCon
matchTyCon Env
env ModName
name LocSymbol
lc ([RType BTyCon BTyVar r] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType BTyCon BTyVar r]
ts)
lc :: LocSymbol
lc = BTyCon -> LocSymbol
btc_tc BTyCon
tc
matchTyCon :: Env -> ModName -> LocSymbol -> Int -> Lookup Ghc.TyCon
matchTyCon :: Env -> ModName -> LocSymbol -> Int -> Lookup TyCon
matchTyCon Env
env ModName
name lc :: LocSymbol
lc@(Loc SourcePos
_ SourcePos
_ Symbol
c) Int
arity
| Symbol -> Bool
forall c. TyConable c => c -> Bool
isList Symbol
c Bool -> Bool -> Bool
&& Int
arity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = TyCon -> Lookup TyCon
forall a b. b -> Either a b
Right TyCon
Ghc.listTyCon
| Symbol -> Bool
forall c. TyConable c => c -> Bool
isTuple Symbol
c = TyCon -> Lookup TyCon
forall a b. b -> Either a b
Right TyCon
tuplTc
| Bool
otherwise = Env -> ModName -> String -> LocSymbol -> Lookup TyCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
msg LocSymbol
lc
where
msg :: String
msg = String
"matchTyCon: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. PPrint a => a -> String
F.showpp Symbol
c
tuplTc :: TyCon
tuplTc = Boxity -> Int -> TyCon
Ghc.tupleTyCon Boxity
Ghc.Boxed Int
arity
bareTCApp :: (Expandable r)
=> r
-> Located Ghc.TyCon
-> [RTProp RTyCon RTyVar r]
-> [RType RTyCon RTyVar r]
-> RType RTyCon RTyVar r
bareTCApp :: forall r.
Expandable r =>
r
-> Located TyCon
-> [RTProp RTyCon RTyVar r]
-> [RType RTyCon RTyVar r]
-> RType RTyCon RTyVar r
bareTCApp r
r (Loc SourcePos
l SourcePos
_ TyCon
c) [RTProp RTyCon RTyVar r]
rs [RType RTyCon RTyVar r]
ts | Just Type
rhs <- TyCon -> Maybe Type
Ghc.synTyConRhs_maybe TyCon
c
= if TyCon -> Int
GM.kindTCArity TyCon
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [RType RTyCon RTyVar r] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType RTyCon RTyVar r]
ts
then Error -> RType RTyCon RTyVar r
forall a e. Exception e => e -> a
Ex.throw Error
err
else RType RTyCon RTyVar r
-> [RType RTyCon RTyVar r]
-> [RTProp RTyCon RTyVar r]
-> r
-> RType RTyCon RTyVar r
forall r c tv.
Reftable r =>
RType c tv r
-> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
tyApp ([(RTyVar, RType RTyCon RTyVar (), RType RTyCon RTyVar r)]
-> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall tv (t :: * -> *) r c.
(Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c,
SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
SubsTy tv (RType c tv ()) tv,
SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
RT.subsTyVarsMeet [(RTyVar, RType RTyCon RTyVar (), RType RTyCon RTyVar r)]
su (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall a b. (a -> b) -> a -> b
$ Type -> RType RTyCon RTyVar r
forall r. Monoid r => Type -> RRType r
RT.ofType Type
rhs) (Int -> [RType RTyCon RTyVar r] -> [RType RTyCon RTyVar r]
forall a. Int -> [a] -> [a]
drop Int
nts [RType RTyCon RTyVar r]
ts) [RTProp RTyCon RTyVar r]
rs r
r
where
tvs :: [Id]
tvs = [ Id
v | (Id
v, TyConBinder
b) <- [Id] -> [TyConBinder] -> [(Id, TyConBinder)]
forall a b. [a] -> [b] -> [(a, b)]
zip (TyCon -> [Id]
GM.tyConTyVarsDef TyCon
c) (TyCon -> [TyConBinder]
Ghc.tyConBinders TyCon
c), TyConBinder -> Bool
GM.isAnonBinder TyConBinder
b]
su :: [(RTyVar, RType RTyCon RTyVar (), RType RTyCon RTyVar r)]
su = (Id
-> RType RTyCon RTyVar r
-> (RTyVar, RType RTyCon RTyVar (), RType RTyCon RTyVar r))
-> [Id]
-> [RType RTyCon RTyVar r]
-> [(RTyVar, RType RTyCon RTyVar (), RType RTyCon RTyVar r)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Id
a RType RTyCon RTyVar r
t -> (Id -> RTyVar
RT.rTyVar Id
a, RType RTyCon RTyVar r -> RType RTyCon RTyVar ()
forall c tv r. RType c tv r -> RType c tv ()
toRSort RType RTyCon RTyVar r
t, RType RTyCon RTyVar r
t)) [Id]
tvs [RType RTyCon RTyVar r]
ts
nts :: Int
nts = [Id] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
tvs
err :: Error
err :: Error
err = SrcSpan -> Doc -> SrcSpan -> Doc -> Error
forall t. SrcSpan -> Doc -> SrcSpan -> Doc -> TError t
ErrAliasApp (SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l) (TyCon -> Doc
forall a. PPrint a => a -> Doc
pprint TyCon
c) (TyCon -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
Ghc.getSrcSpan TyCon
c)
([Doc] -> Doc
PJ.hcat [ String -> Doc
PJ.text String
"Expects"
, Int -> Doc
forall a. PPrint a => a -> Doc
pprint (TyCon -> Int
GM.realTcArity TyCon
c)
, String -> Doc
PJ.text String
"arguments, but is given"
, Int -> Doc
forall a. PPrint a => a -> Doc
pprint ([RType RTyCon RTyVar r] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType RTyCon RTyVar r]
ts) ] )
bareTCApp r
r (Loc SourcePos
_ SourcePos
_ TyCon
c) [RTProp RTyCon RTyVar r]
rs [RType RTyCon RTyVar r]
ts | TyCon -> Bool
Ghc.isFamilyTyCon TyCon
c Bool -> Bool -> Bool
&& RType RTyCon RTyVar r -> Bool
forall r c tv. (Reftable r, TyConable c) => RType c tv r -> Bool
isTrivial RType RTyCon RTyVar r
t
= RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall r. Expandable r => RRType r -> RRType r
expandRTypeSynonyms (RType RTyCon RTyVar r
t RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`RT.strengthen` r
r)
where t :: RType RTyCon RTyVar r
t = TyCon
-> [RType RTyCon RTyVar r]
-> [RTProp RTyCon RTyVar r]
-> r
-> RType RTyCon RTyVar r
forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
RT.rApp TyCon
c [RType RTyCon RTyVar r]
ts [RTProp RTyCon RTyVar r]
rs r
forall a. Monoid a => a
mempty
bareTCApp r
r (Loc SourcePos
_ SourcePos
_ TyCon
c) [RTProp RTyCon RTyVar r]
rs [RType RTyCon RTyVar r]
ts
= TyCon
-> [RType RTyCon RTyVar r]
-> [RTProp RTyCon RTyVar r]
-> r
-> RType RTyCon RTyVar r
forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
RT.rApp TyCon
c [RType RTyCon RTyVar r]
ts [RTProp RTyCon RTyVar r]
rs r
r
tyApp :: F.Reftable r => RType c tv r -> [RType c tv r] -> [RTProp c tv r] -> r
-> RType c tv r
tyApp :: forall r c tv.
Reftable r =>
RType c tv r
-> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
tyApp (RApp c
c [RType c tv r]
ts [RTProp c tv r]
rs r
r) [RType c tv r]
ts' [RTProp c tv r]
rs' r
r' = c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
c ([RType c tv r]
ts [RType c tv r] -> [RType c tv r] -> [RType c tv r]
forall a. [a] -> [a] -> [a]
++ [RType c tv r]
ts') ([RTProp c tv r]
rs [RTProp c tv r] -> [RTProp c tv r] -> [RTProp c tv r]
forall a. [a] -> [a] -> [a]
++ [RTProp c tv r]
rs') (r
r r -> r -> r
forall r. Reftable r => r -> r -> r
`F.meet` r
r')
tyApp RType c tv r
t [] [] r
r = RType c tv r
t RType c tv r -> r -> RType c tv r
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`RT.strengthen` r
r
tyApp RType c tv r
_ [RType c tv r]
_ [RTProp c tv r]
_ r
_ = Maybe SrcSpan -> String -> RType c tv r
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"Bare.Type.tyApp on invalid inputs"
expandRTypeSynonyms :: (Expandable r) => RRType r -> RRType r
expandRTypeSynonyms :: forall r. Expandable r => RRType r -> RRType r
expandRTypeSynonyms = Type -> RRType r
forall r. Monoid r => Type -> RRType r
RT.ofType (Type -> RRType r) -> (RRType r -> Type) -> RRType r -> RRType r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
Ghc.expandTypeSynonyms (Type -> Type) -> (RRType r -> Type) -> RRType r -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> RRType r -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
RT.toType Bool
False
txRefSort :: TyConMap -> F.TCEmb Ghc.TyCon -> LocSpecType -> LocSpecType
txRefSort :: TyConMap -> TCEmb TyCon -> LocSpecType -> LocSpecType
txRefSort TyConMap
tyi TCEmb TyCon
tce LocSpecType
t = LocSpecType -> SpecType -> LocSpecType
forall l b. Loc l => l -> b -> Located b
F.atLoc LocSpecType
t (SpecType -> LocSpecType) -> SpecType -> LocSpecType
forall a b. (a -> b) -> a -> b
$ (SpecType -> SpecType) -> SpecType -> SpecType
forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot (SrcSpan -> TCEmb TyCon -> TyConMap -> SpecType -> SpecType
addSymSort (LocSpecType -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSpecType
t) TCEmb TyCon
tce TyConMap
tyi) (LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
t)
addSymSort :: Ghc.SrcSpan -> F.TCEmb Ghc.TyCon -> TyConMap -> SpecType -> SpecType
addSymSort :: SrcSpan -> TCEmb TyCon -> TyConMap -> SpecType -> SpecType
addSymSort SrcSpan
sp TCEmb TyCon
tce TyConMap
tyi (RApp rc :: RTyCon
rc@RTyCon{} [SpecType]
ts [RTProp RTyCon RTyVar RReft]
rs RReft
rr)
= RTyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> SpecType
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
rc [SpecType]
ts ((RPVar
-> RTProp RTyCon RTyVar RReft -> Int -> RTProp RTyCon RTyVar RReft)
-> [RPVar]
-> [RTProp RTyCon RTyVar RReft]
-> [Int]
-> [RTProp RTyCon RTyVar RReft]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 (SrcSpan
-> RTyCon
-> RPVar
-> RTProp RTyCon RTyVar RReft
-> Int
-> RTProp RTyCon RTyVar RReft
forall s.
PPrint s =>
SrcSpan
-> s
-> RPVar
-> RTProp RTyCon RTyVar RReft
-> Int
-> RTProp RTyCon RTyVar RReft
addSymSortRef SrcSpan
sp RTyCon
rc) [RPVar]
pvs [RTProp RTyCon RTyVar RReft]
rargs [Int
1..]) RReft
r2
where
(RTyCon
_, [RPVar]
pvs) = TCEmb TyCon
-> TyConMap -> RTyCon -> [SpecType] -> (RTyCon, [RPVar])
forall r.
ToTypeable r =>
TCEmb TyCon
-> TyConMap -> RTyCon -> [RRType r] -> (RTyCon, [RPVar])
RT.appRTyCon TCEmb TyCon
tce TyConMap
tyi RTyCon
rc [SpecType]
ts
([RTProp RTyCon RTyVar RReft]
rargs, [RTProp RTyCon RTyVar RReft]
rrest) = Int
-> [RTProp RTyCon RTyVar RReft]
-> ([RTProp RTyCon RTyVar RReft], [RTProp RTyCon RTyVar RReft])
forall a. Int -> [a] -> ([a], [a])
splitAt ([RPVar] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RPVar]
pvs) [RTProp RTyCon RTyVar RReft]
rs
r2 :: RReft
r2 = (RReft -> RTProp RTyCon RTyVar RReft -> RReft)
-> RReft -> [RTProp RTyCon RTyVar RReft] -> RReft
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' RReft -> RTProp RTyCon RTyVar RReft -> RReft
forall {r} {τ} {c} {tv}.
Reftable r =>
r -> Ref τ (RType c tv r) -> r
go RReft
rr [RTProp RTyCon RTyVar RReft]
rrest
go :: r -> Ref τ (RType c tv r) -> r
go r
r (RProp [(Symbol, τ)]
_ (RHole r
r')) = r
r' r -> r -> r
forall r. Reftable r => r -> r -> r
`F.meet` r
r
go r
r (RProp [(Symbol, τ)]
_ RType c tv r
t' ) = let r' :: r
r' = r -> Maybe r -> r
forall a. a -> Maybe a -> a
Mb.fromMaybe r
forall a. Monoid a => a
mempty (RType c tv r -> Maybe r
forall c tv r. RType c tv r -> Maybe r
stripRTypeBase RType c tv r
t') in r
r r -> r -> r
forall r. Reftable r => r -> r -> r
`F.meet` r
r'
addSymSort SrcSpan
_ TCEmb TyCon
_ TyConMap
_ SpecType
t
= SpecType
t
addSymSortRef :: (PPrint s) => Ghc.SrcSpan -> s -> RPVar -> SpecProp -> Int -> SpecProp
addSymSortRef :: forall s.
PPrint s =>
SrcSpan
-> s
-> RPVar
-> RTProp RTyCon RTyVar RReft
-> Int
-> RTProp RTyCon RTyVar RReft
addSymSortRef SrcSpan
sp s
rc RPVar
p RTProp RTyCon RTyVar RReft
r Int
i
| RPVar -> Bool
forall t. PVar t -> Bool
isPropPV RPVar
p
= SrcSpan
-> s
-> Int
-> RPVar
-> RTProp RTyCon RTyVar RReft
-> RTProp RTyCon RTyVar RReft
forall s.
PPrint s =>
SrcSpan
-> s
-> Int
-> RPVar
-> RTProp RTyCon RTyVar RReft
-> RTProp RTyCon RTyVar RReft
addSymSortRef' SrcSpan
sp s
rc Int
i RPVar
p RTProp RTyCon RTyVar RReft
r
| Bool
otherwise
= Maybe SrcSpan -> String -> RTProp RTyCon RTyVar RReft
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"addSymSortRef: malformed ref application"
addSymSortRef' :: (PPrint s) => Ghc.SrcSpan -> s -> Int -> RPVar -> SpecProp -> SpecProp
addSymSortRef' :: forall s.
PPrint s =>
SrcSpan
-> s
-> Int
-> RPVar
-> RTProp RTyCon RTyVar RReft
-> RTProp RTyCon RTyVar RReft
addSymSortRef' SrcSpan
_ s
_ Int
_ RPVar
p (RProp [(Symbol, RType RTyCon RTyVar ())]
s (RVar RTyVar
v RReft
r)) | RTyVar -> Bool
forall a. Symbolic a => a -> Bool
isDummy RTyVar
v
= [(Symbol, RType RTyCon RTyVar ())]
-> SpecType -> RTProp RTyCon RTyVar RReft
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
xs SpecType
t
where
t :: SpecType
t = RType RTyCon RTyVar () -> SpecType
forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort (RPVar -> RType RTyCon RTyVar ()
forall t. PVar t -> t
pvType RPVar
p) SpecType -> RReft -> SpecType
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`RT.strengthen` RReft
r
xs :: [(Symbol, RType RTyCon RTyVar ())]
xs = String
-> [(Symbol, RType RTyCon RTyVar ())]
-> RPVar
-> [(Symbol, RType RTyCon RTyVar ())]
forall b t. String -> [(Symbol, b)] -> PVar t -> [(Symbol, t)]
spliceArgs String
"addSymSortRef 1" [(Symbol, RType RTyCon RTyVar ())]
s RPVar
p
addSymSortRef' SrcSpan
sp s
rc Int
i RPVar
p (RProp [(Symbol, RType RTyCon RTyVar ())]
_ (RHole r :: RReft
r@(MkUReft Reft
_ (Pr [UsedPVar
up]))))
| [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [RType RTyCon RTyVar ()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType RTyCon RTyVar ()]
ts
= [(Symbol, RType RTyCon RTyVar ())]
-> SpecType -> RTProp RTyCon RTyVar RReft
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
xts (RReft -> SpecType
forall c tv r. r -> RType c tv r
RHole RReft
r)
| Bool
otherwise
=
UserError -> RTProp RTyCon RTyVar RReft
forall a. UserError -> a
uError (UserError -> RTProp RTyCon RTyVar RReft)
-> UserError -> RTProp RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Doc -> Int -> Int -> Int -> UserError
forall t. SrcSpan -> Doc -> Doc -> Int -> Int -> Int -> TError t
ErrPartPred SrcSpan
sp (s -> Doc
forall a. PPrint a => a -> Doc
pprint s
rc) (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (Symbol -> Doc) -> Symbol -> Doc
forall a b. (a -> b) -> a -> b
$ UsedPVar -> Symbol
forall t. PVar t -> Symbol
pname UsedPVar
up) Int
i ([Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
xs) ([RType RTyCon RTyVar ()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType RTyCon RTyVar ()]
ts)
where
xts :: [(Symbol, RType RTyCon RTyVar ())]
xts = String
-> [Symbol]
-> [RType RTyCon RTyVar ()]
-> [(Symbol, RType RTyCon RTyVar ())]
forall t t1. String -> [t] -> [t1] -> [(t, t1)]
Misc.safeZipWithError String
"addSymSortRef'" [Symbol]
xs [RType RTyCon RTyVar ()]
ts
xs :: [Symbol]
xs = ((), Symbol, Expr) -> Symbol
forall a b c. (a, b, c) -> b
Misc.snd3 (((), Symbol, Expr) -> Symbol) -> [((), Symbol, Expr)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UsedPVar -> [((), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
up
ts :: [RType RTyCon RTyVar ()]
ts = (RType RTyCon RTyVar (), Symbol, Expr) -> RType RTyCon RTyVar ()
forall a b c. (a, b, c) -> a
Misc.fst3 ((RType RTyCon RTyVar (), Symbol, Expr) -> RType RTyCon RTyVar ())
-> [(RType RTyCon RTyVar (), Symbol, Expr)]
-> [RType RTyCon RTyVar ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RPVar -> [(RType RTyCon RTyVar (), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs RPVar
p
addSymSortRef' SrcSpan
_ s
_ Int
_ RPVar
_ (RProp [(Symbol, RType RTyCon RTyVar ())]
s (RHole RReft
r))
= [(Symbol, RType RTyCon RTyVar ())]
-> SpecType -> RTProp RTyCon RTyVar RReft
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
s (RReft -> SpecType
forall c tv r. r -> RType c tv r
RHole RReft
r)
addSymSortRef' SrcSpan
_ s
_ Int
_ RPVar
p (RProp [(Symbol, RType RTyCon RTyVar ())]
s SpecType
t)
= [(Symbol, RType RTyCon RTyVar ())]
-> SpecType -> RTProp RTyCon RTyVar RReft
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
xs SpecType
t
where
xs :: [(Symbol, RType RTyCon RTyVar ())]
xs = String
-> [(Symbol, RType RTyCon RTyVar ())]
-> RPVar
-> [(Symbol, RType RTyCon RTyVar ())]
forall b t. String -> [(Symbol, b)] -> PVar t -> [(Symbol, t)]
spliceArgs String
"addSymSortRef 2" [(Symbol, RType RTyCon RTyVar ())]
s RPVar
p
spliceArgs :: String -> [(F.Symbol, b)] -> PVar t -> [(F.Symbol, t)]
spliceArgs :: forall b t. String -> [(Symbol, b)] -> PVar t -> [(Symbol, t)]
spliceArgs String
msg [(Symbol, b)]
syms PVar t
p = [Symbol] -> [(t, Symbol, Expr)] -> [(Symbol, t)]
forall {a} {b} {c}. Show a => [a] -> [(b, a, c)] -> [(a, b)]
go ((Symbol, b) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, b) -> Symbol) -> [(Symbol, b)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, b)]
syms) (PVar t -> [(t, Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar t
p)
where
go :: [a] -> [(b, a, c)] -> [(a, b)]
go [] [] = []
go [] ((b
s,a
x,c
_):[(b, a, c)]
as) = (a
x, b
s)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[a] -> [(b, a, c)] -> [(a, b)]
go [] [(b, a, c)]
as
go (a
x:[a]
xs) ((b
s,a
_,c
_):[(b, a, c)]
as) = (a
x,b
s)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[a] -> [(b, a, c)] -> [(a, b)]
go [a]
xs [(b, a, c)]
as
go [a]
xs [] = Maybe SrcSpan -> String -> [(a, b)]
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String -> [(a, b)]) -> String -> [(a, b)]
forall a b. (a -> b) -> a -> b
$ String
"spliceArgs: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"on XS=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [a] -> String
forall a. Show a => a -> String
show [a]
xs
resolveLocalBinds :: Env -> [(Ghc.Var, LocBareType, Maybe [Located F.Expr])]
-> [(Ghc.Var, LocBareType, Maybe [Located F.Expr])]
resolveLocalBinds :: Env
-> [(Id, LocBareType, Maybe [Located Expr])]
-> [(Id, LocBareType, Maybe [Located Expr])]
resolveLocalBinds Env
env [(Id, LocBareType, Maybe [Located Expr])]
xtes = [ (Id
x,LocBareType
t,Maybe [Located Expr]
es) | (Id
x, (LocBareType
t, Maybe [Located Expr]
es)) <- [(Id, (LocBareType, Maybe [Located Expr]))]
topTs [(Id, (LocBareType, Maybe [Located Expr]))]
-> [(Id, (LocBareType, Maybe [Located Expr]))]
-> [(Id, (LocBareType, Maybe [Located Expr]))]
forall a. [a] -> [a] -> [a]
++ [(Id, (LocBareType, Maybe [Located Expr]))]
-> [(Id, (LocBareType, Maybe [Located Expr]))]
replace [(Id, (LocBareType, Maybe [Located Expr]))]
locTs ]
where
([(Id, (LocBareType, Maybe [Located Expr]))]
locTs, [(Id, (LocBareType, Maybe [Located Expr]))]
topTs) = [(Id, (LocBareType, Maybe [Located Expr]))]
-> ([(Id, (LocBareType, Maybe [Located Expr]))],
[(Id, (LocBareType, Maybe [Located Expr]))])
forall a. [(Id, a)] -> ([(Id, a)], [(Id, a)])
partitionLocalBinds [ (Id
x, (LocBareType
t, Maybe [Located Expr]
es)) | (Id
x, LocBareType
t, Maybe [Located Expr]
es) <- [(Id, LocBareType, Maybe [Located Expr])]
xtes]
replace :: [(Id, (LocBareType, Maybe [Located Expr]))]
-> [(Id, (LocBareType, Maybe [Located Expr]))]
replace = HashMap Id (LocBareType, Maybe [Located Expr])
-> [(Id, (LocBareType, Maybe [Located Expr]))]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Id (LocBareType, Maybe [Located Expr])
-> [(Id, (LocBareType, Maybe [Located Expr]))])
-> ([(Id, (LocBareType, Maybe [Located Expr]))]
-> HashMap Id (LocBareType, Maybe [Located Expr]))
-> [(Id, (LocBareType, Maybe [Located Expr]))]
-> [(Id, (LocBareType, Maybe [Located Expr]))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap Id (LocBareType, Maybe [Located Expr])
-> HashMap Id (LocBareType, Maybe [Located Expr])
replaceSigs (HashMap Id (LocBareType, Maybe [Located Expr])
-> HashMap Id (LocBareType, Maybe [Located Expr]))
-> ([(Id, (LocBareType, Maybe [Located Expr]))]
-> HashMap Id (LocBareType, Maybe [Located Expr]))
-> [(Id, (LocBareType, Maybe [Located Expr]))]
-> HashMap Id (LocBareType, Maybe [Located Expr])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Id, (LocBareType, Maybe [Located Expr]))]
-> HashMap Id (LocBareType, Maybe [Located Expr])
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList
replaceSigs :: HashMap Id (LocBareType, Maybe [Located Expr])
-> HashMap Id (LocBareType, Maybe [Located Expr])
replaceSigs HashMap Id (LocBareType, Maybe [Located Expr])
sigm = CoreVisitor SymMap (HashMap Id (LocBareType, Maybe [Located Expr]))
-> SymMap
-> HashMap Id (LocBareType, Maybe [Located Expr])
-> [CoreBind]
-> HashMap Id (LocBareType, Maybe [Located Expr])
forall env acc.
CoreVisitor env acc -> env -> acc -> [CoreBind] -> acc
coreVisitor CoreVisitor SymMap (HashMap Id (LocBareType, Maybe [Located Expr]))
replaceVisitor SymMap
forall k v. HashMap k v
M.empty HashMap Id (LocBareType, Maybe [Located Expr])
sigm [CoreBind]
cbs
cbs :: [CoreBind]
cbs = GhcSrc -> [CoreBind]
_giCbs (Env -> GhcSrc
reSrc Env
env)
replaceVisitor :: CoreVisitor SymMap SigMap
replaceVisitor :: CoreVisitor SymMap (HashMap Id (LocBareType, Maybe [Located Expr]))
replaceVisitor = CoreVisitor
{ envF :: SymMap -> Id -> SymMap
envF = SymMap -> Id -> SymMap
addBind
, bindF :: SymMap
-> HashMap Id (LocBareType, Maybe [Located Expr])
-> Id
-> HashMap Id (LocBareType, Maybe [Located Expr])
bindF = SymMap
-> HashMap Id (LocBareType, Maybe [Located Expr])
-> Id
-> HashMap Id (LocBareType, Maybe [Located Expr])
updSigMap
, exprF :: SymMap
-> HashMap Id (LocBareType, Maybe [Located Expr])
-> Expr Id
-> HashMap Id (LocBareType, Maybe [Located Expr])
exprF = \SymMap
_ HashMap Id (LocBareType, Maybe [Located Expr])
m Expr Id
_ -> HashMap Id (LocBareType, Maybe [Located Expr])
m
}
addBind :: SymMap -> Ghc.Var -> SymMap
addBind :: SymMap -> Id -> SymMap
addBind SymMap
env Id
v = case Id -> Maybe Symbol
localKey Id
v of
Just Symbol
vx -> Symbol -> Symbol -> SymMap -> SymMap
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
vx (Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
v) SymMap
env
Maybe Symbol
Nothing -> SymMap
env
updSigMap :: SymMap -> SigMap -> Ghc.Var -> SigMap
updSigMap :: SymMap
-> HashMap Id (LocBareType, Maybe [Located Expr])
-> Id
-> HashMap Id (LocBareType, Maybe [Located Expr])
updSigMap SymMap
env HashMap Id (LocBareType, Maybe [Located Expr])
m Id
v = case Id
-> HashMap Id (LocBareType, Maybe [Located Expr])
-> Maybe (LocBareType, Maybe [Located Expr])
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Id
v HashMap Id (LocBareType, Maybe [Located Expr])
m of
Maybe (LocBareType, Maybe [Located Expr])
Nothing -> HashMap Id (LocBareType, Maybe [Located Expr])
m
Just (LocBareType, Maybe [Located Expr])
tes -> Id
-> (LocBareType, Maybe [Located Expr])
-> HashMap Id (LocBareType, Maybe [Located Expr])
-> HashMap Id (LocBareType, Maybe [Located Expr])
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Id
v (String
-> (LocBareType, Maybe [Located Expr])
-> (LocBareType, Maybe [Located Expr])
forall a. PPrint a => String -> a -> a
myTracepp (String
"UPD-LOCAL-SIG " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Outputable a => a -> String
GM.showPpr Id
v) ((LocBareType, Maybe [Located Expr])
-> (LocBareType, Maybe [Located Expr]))
-> (LocBareType, Maybe [Located Expr])
-> (LocBareType, Maybe [Located Expr])
forall a b. (a -> b) -> a -> b
$ SymMap
-> (LocBareType, Maybe [Located Expr])
-> (LocBareType, Maybe [Located Expr])
renameLocalSig SymMap
env (LocBareType, Maybe [Located Expr])
tes) HashMap Id (LocBareType, Maybe [Located Expr])
m
renameLocalSig :: SymMap -> (LocBareType, Maybe [Located F.Expr])
-> (LocBareType, Maybe [Located F.Expr])
renameLocalSig :: SymMap
-> (LocBareType, Maybe [Located Expr])
-> (LocBareType, Maybe [Located Expr])
renameLocalSig SymMap
env (LocBareType
t, Maybe [Located Expr]
es) = ((Symbol -> Expr) -> LocBareType -> LocBareType
forall a. Subable a => (Symbol -> Expr) -> a -> a
F.substf Symbol -> Expr
tSub LocBareType
t, (Symbol -> Expr) -> Maybe [Located Expr] -> Maybe [Located Expr]
forall a. Subable a => (Symbol -> Expr) -> a -> a
F.substf Symbol -> Expr
esSub Maybe [Located Expr]
es)
where
tSub :: Symbol -> Expr
tSub = Symbol -> Expr
F.EVar (Symbol -> Expr) -> (Symbol -> Symbol) -> Symbol -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymMap -> Symbol -> Symbol
qualifySymMap SymMap
env
esSub :: Symbol -> Expr
esSub = Symbol -> Expr
tSub (Symbol -> Expr) -> [Symbol] -> Symbol -> Expr
`F.substfExcept` [Symbol]
xs
xs :: [Symbol]
xs = RTypeRep BTyCon BTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds (BareType -> RTypeRep BTyCon BTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (LocBareType -> BareType
forall a. Located a -> a
F.val LocBareType
t))
qualifySymMap :: SymMap -> F.Symbol -> F.Symbol
qualifySymMap :: SymMap -> Symbol -> Symbol
qualifySymMap SymMap
env Symbol
x = Symbol -> Symbol -> SymMap -> Symbol
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Symbol
x Symbol
x SymMap
env
type SigMap = M.HashMap Ghc.Var (LocBareType, Maybe [Located F.Expr])
type SymMap = M.HashMap F.Symbol F.Symbol
partitionLocalBinds :: [(Ghc.Var, a)] -> ([(Ghc.Var, a)], [(Ghc.Var, a)])
partitionLocalBinds :: forall a. [(Id, a)] -> ([(Id, a)], [(Id, a)])
partitionLocalBinds = ((Id, a) -> Bool) -> [(Id, a)] -> ([(Id, a)], [(Id, a)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (Maybe Symbol -> Bool
forall a. Maybe a -> Bool
Mb.isJust (Maybe Symbol -> Bool)
-> ((Id, a) -> Maybe Symbol) -> (Id, a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Maybe Symbol
localKey (Id -> Maybe Symbol) -> ((Id, a) -> Id) -> (Id, a) -> Maybe Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, a) -> Id
forall a b. (a, b) -> a
fst)