-- | This module has the code that uses the GHC definitions to:
--   1. MAKE a name-resolution environment,
--   2. USE the environment to translate plain symbols into Var, TyCon, etc.

{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE TupleSections         #-}

module Language.Haskell.Liquid.Bare.Resolve
  ( -- * Creating the Environment
    makeEnv

    -- * Resolving symbols
  , ResolveSym (..)
  , Qualify (..)
  , Lookup
  , qualifyTop, qualifyTopDummy

  -- * Looking up names
  , maybeResolveSym
  , lookupGhcDataCon
  , lookupGhcDnTyCon
  , lookupGhcTyCon
  , lookupGhcVar
  , lookupGhcNamedVar

  -- * Checking if names exist
  , knownGhcVar
  , knownGhcTyCon
  , knownGhcDataCon
  , knownGhcType

  -- * Misc
  , srcVars
  , coSubRReft
  , unQualifySymbol

  -- * Conversions from Bare
  , ofBareTypeE
  , ofBareType
  , ofBPVar

  -- * Post-processing types
  , txRefSort
  , errResolve

  -- * Fixing local variables
  , 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 = forall a. PPrint a => String -> a -> a
F.notracepp

-- type Lookup a = Misc.Validate [Error] a
type Lookup a = Either [Error] a

-------------------------------------------------------------------------------
-- | Creating an environment
-------------------------------------------------------------------------------
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  = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList     [Symbol]
globalSyms
  , reCfg :: Config
reCfg       = Config
cfg
  }
  where
    globalSyms :: [Symbol]
globalSyms  = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ModName, BareSpec) -> [Symbol]
getGlobalSyms [(ModName, BareSpec)]
specs
    syms :: [(Symbol, Id)]
syms        = [ (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)
  = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Bool
GM.isQualifiedSym)
       forall a b. (a -> b) -> a -> b
$ (forall {ty} {ctor}. Measure ty ctor -> Symbol
mbName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures  BareSpec
spec)
      forall a. [a] -> [a] -> [a]
++ (forall {ty} {ctor}. Measure ty ctor -> Symbol
mbName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ty bndr. Spec ty bndr -> [Measure ty ()]
cmeasures BareSpec
spec)
      forall a. [a] -> [a] -> [a]
++ (forall {ty} {ctor}. Measure ty ctor -> Symbol
mbName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ty bndr. Spec ty bndr -> [Measure ty bndr]
imeasures BareSpec
spec)
  where
    mbName :: Measure ty ctor -> Symbol
mbName = forall a. Located a -> a
F.val forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty ctor. Measure ty ctor -> LocSymbol
msName

makeLocalVars :: GhcSrc -> LocalVars
makeLocalVars :: GhcSrc -> LocalVars
makeLocalVars = [Id] -> LocalVars
localVarMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. [CoreBind] -> [Id]
localBinds forall b c a. (b -> c) -> (a -> b) -> a -> c
. GhcSrc -> [CoreBind]
_giCbs

-- TODO: rewrite using CoreVisitor
localBinds :: [Ghc.CoreBind] -> [Ghc.Var]
localBinds :: [CoreBind] -> [Id]
localBinds                    = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (HashSet Symbol -> CoreBind -> [Id]
bgo forall a. HashSet a
S.empty)
  where
    add :: Id -> HashSet Symbol -> HashSet Symbol
add  Id
x HashSet Symbol
g                  = forall b a. b -> (a -> b) -> Maybe a -> b
maybe HashSet Symbol
g (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                  = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Id -> HashSet Symbol -> HashSet Symbol
add HashSet Symbol
g (forall b. Bind b -> [b]
Ghc.bindersOf CoreBind
b)
    take' :: Id -> HashSet Symbol -> [Id]
take' Id
x HashSet Symbol
g                 = forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\Symbol
k -> [Id
x | Bool -> Bool
not (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 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)       = 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)       = 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 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 forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (HashSet Symbol -> Expr Id -> [Id]
go HashSet Symbol
g 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 =
  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 (forall a. Loc a => a -> Pos
F.srcLine Id
v)
                           , Symbol
x <- 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 = forall a. a -> Maybe a
Just Symbol
x
  | Bool
otherwise = forall a. Maybe a
Nothing
  where
    (Symbol
m, Symbol
x)    = Symbol -> (Symbol, Symbol)
splitModuleNameExact forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
GM.dropModuleUnique forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
F.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) <- 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 <- forall a. Maybe a -> [a]
Mb.maybeToList (forall a. Symbol -> [(Symbol, a)] -> Maybe a
okUnqualified Symbol
me [(Symbol, Id)]
mxs)
                   ]
    me :: Symbol
me           = forall a. Symbolic a => a -> Symbol
F.symbol (GhcSrc -> ModName
_giTargetMod GhcSrc
src)

-- | @okUnqualified mod mxs@ takes @mxs@ which is a list of modulenames-var
--   pairs all of which have the same unqualified symbol representation.
--   The function returns @Just v@ if
--   1. that list is a singleton i.e. there is a UNIQUE unqualified version, OR
--   2. there is a version whose module equals @me@.

okUnqualified :: F.Symbol -> [(F.Symbol, a)] -> Maybe a
okUnqualified :: forall a. Symbol -> [(Symbol, a)] -> Maybe a
okUnqualified Symbol
_ [(Symbol
_, a
x)] = forall a. a -> Maybe a
Just a
x
okUnqualified Symbol
me [(Symbol, a)]
mxs     = forall {a}. [(Symbol, a)] -> Maybe a
go [(Symbol, a)]
mxs
  where
    go :: [(Symbol, a)] -> Maybe a
go []                = forall a. Maybe a
Nothing
    go ((Symbol
m,a
x) : [(Symbol, a)]
rest)
      | Symbol
me forall a. Eq a => a -> a -> Bool
== Symbol
m          = 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 = 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) = forall a. Symbolic a => a -> (Symbol, Symbol)
qualifiedSymbol Id
x ]

makeTyThingMap :: GhcSrc -> TyThingMap
makeTyThingMap :: GhcSrc -> TyThingMap
makeTyThingMap GhcSrc
src =
  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      <- forall a. Maybe a -> [a]
Mb.maybeToList (TyThing -> Maybe Symbol
tyThingSymbol TyThing
t)
                            , let (Symbol
m, Symbol
x) = forall a. Symbolic a => a -> (Symbol, Symbol)
qualifiedSymbol Symbol
tSym
                            , Bool -> Bool
not (Symbol -> Bool
isLocal Symbol
m)
             ]

tyThingSymbol :: Ghc.TyThing -> Maybe F.Symbol
tyThingSymbol :: TyThing -> Maybe Symbol
tyThingSymbol (Ghc.AnId     Id
x) = forall a. a -> Maybe a
Just (forall a. Symbolic a => a -> Symbol
F.symbol Id
x)
tyThingSymbol (Ghc.ATyCon   TyCon
c) = forall a. a -> Maybe a
Just (forall a. Symbolic a => a -> Symbol
F.symbol TyCon
c)
tyThingSymbol (Ghc.AConLike ConLike
d) = ConLike -> Maybe Symbol
conLikeSymbol ConLike
d
tyThingSymbol TyThing
_tt              = forall a. Maybe a
Nothing -- panic Nothing ("TODO: tyThingSymbol" ++ showPpr tt)


conLikeSymbol :: Ghc.ConLike -> Maybe F.Symbol
conLikeSymbol :: ConLike -> Maybe Symbol
conLikeSymbol (Ghc.RealDataCon DataCon
d) = forall a. a -> Maybe a
Just (forall a. Symbolic a => a -> Symbol
F.symbol DataCon
d)
conLikeSymbol ConLike
_z                   = forall a. Maybe a
Nothing -- panic Nothing ("TODO: conLikeSymbol -- " ++ showPpr z)




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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
F.symbol

isEmptySymbol :: F.Symbol -> Bool
isEmptySymbol :: Symbol -> Bool
isEmptySymbol Symbol
x = Symbol -> Int
F.lengthSym Symbol
x forall a. Eq a => a -> a -> Bool
== Int
0

srcThings :: GhcSrc -> [Ghc.TyThing]
srcThings :: GhcSrc -> [TyThing]
srcThings GhcSrc
src = forall a. PPrint a => String -> a -> a
myTracepp String
"SRCTHINGS"
              forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> [a] -> [a]
Misc.hashNubWith forall a. PPrint a => a -> String
F.showpp (GhcSrc -> [TyThing]
_gsTyThings GhcSrc
src 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 ]
               forall a. [a] -> [a] -> [a]
++ [ TyCon -> TyThing
Ghc.ATyCon TyCon
c | TyCon
c <- [TyCon]
tcs  ]
               forall a. [a] -> [a] -> [a]
++ [ DataCon -> TyThing
aDataCon   DataCon
d | DataCon
d <- [DataCon]
dcs  ]
  where
    vars :: [Id]
vars        = forall a. Ord a => [a] -> [a]
Misc.sortNub forall a b. (a -> b) -> a -> b
$ [DataCon] -> [Id]
dataConVars [DataCon]
dcs forall a. [a] -> [a] -> [a]
++ GhcSrc -> [Id]
srcVars  GhcSrc
src
    dcs :: [DataCon]
dcs         = forall a. Ord a => [a] -> [a]
Misc.sortNub forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TyCon -> [DataCon]
Ghc.tyConDataCons [TyCon]
tcs
    tcs :: [TyCon]
tcs         = forall a. Ord a => [a] -> [a]
Misc.sortNub forall a b. (a -> b) -> a -> b
$ GhcSrc -> [TyCon]
srcTyCons GhcSrc
src
    aDataCon :: DataCon -> TyThing
aDataCon    = ConLike -> TyThing
Ghc.AConLike forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> ConLike
Ghc.RealDataCon

srcTyCons :: GhcSrc -> [Ghc.TyCon]
srcTyCons :: GhcSrc -> [TyCon]
srcTyCons GhcSrc
src = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. GhcSrc -> [Id]
srcVars

varTyCons :: [Ghc.Var] -> [Ghc.TyCon]
varTyCons :: [Id] -> [TyCon]
varTyCons = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Type -> [TyCon]
typeTyCons forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
Ghc.dropForAlls 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 forall a. [a] -> [a] -> [a]
++ Type -> [TyCon]
inners Type
t
  where
    tops :: Type -> [TyCon]
tops     = forall a. Maybe a -> [a]
Mb.maybeToList forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe TyCon
Ghc.tyConAppTyCon_maybe
    inners :: Type -> [TyCon]
inners   = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [TyCon]
typeTyCons forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> (Type, [Type])
Ghc.splitAppTys

-- | We prioritize the @Ghc.Var@ in @srcVars@ because @_giDefVars@ and @gsTyThings@
--   have _different_ values for the same binder, with different types where the
--   type params are alpha-renamed. However, for absref, we need _the same_
--   type parameters as used by GHC as those are used inside the lambdas and
--   other bindings in the code. See also [NOTE: Plug-Holes-TyVars] and
--      tests-absref-pos-Papp00.hs

srcVars :: GhcSrc -> [Ghc.Var]
srcVars :: GhcSrc -> [Id]
srcVars GhcSrc
src = forall a. (a -> Bool) -> [a] -> [a]
filter Id -> Bool
Ghc.isId forall b c a. (b -> c) -> (a -> b) -> a -> c
.  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b c. (a, b, c) -> c
Misc.thd3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r k v.
(Ord r, Hashable k, Eq k) =>
[(r, k, v)] -> [(r, k, v)]
Misc.fstByRank forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ String -> Int -> Id -> (Int, Symbol, Id)
key String
"SRC-VAR-DEF" Int
0 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 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 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 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, forall a. Symbolic a => a -> Symbol
F.symbol Id
x, {- dump s -} Id
x)
    _dump :: String -> Id -> Id
_dump String
msg Id
x = forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PPrint a => String -> a -> a
myTracepp String
msg forall a b. (a -> b) -> a -> b
$ (Id
x, 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataCon]
dcs) forall a. [a] -> [a] -> [a]
++ (DataCon -> Id
Ghc.dataConWrapId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataCon]
dcs)

-------------------------------------------------------------------------------
-- | Qualify various names
-------------------------------------------------------------------------------
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 = 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 = forall a. Qualify a => Env -> ModName -> SourcePos -> a -> a
qualifyTop Env
env ModName
name SourcePos
dummySourcePos

dummySourcePos :: F.SourcePos
dummySourcePos :: SourcePos
dummySourcePos = forall a. Located a -> SourcePos
F.loc (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 :: HashMap TyCon RTyCon
tcmTyRTy = forall a. Qualify a => a -> a
tx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyConMap -> HashMap TyCon RTyCon
tcmTyRTy TyConMap
tyi
    , tcmFIRTy :: HashMap (TyCon, [Sort]) RTyCon
tcmFIRTy = forall a. Qualify a => a -> a
tx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyConMap -> HashMap (TyCon, [Sort]) RTyCon
tcmFIRTy TyConMap
tyi
    }
    where
      tx :: (Qualify a) => a -> a
      tx :: forall a. Qualify a => a -> a
tx = 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 :: Maybe SizeFun
tcpSizeFun = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name (TyConP -> SourcePos
tcpLoc TyConP
tcp) [Symbol]
bs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyConP -> Maybe SizeFun
tcpSizeFun TyConP
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 (forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name (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 -- TODO-REBARE
-- REBARE: qualifyAxiomEq :: Bare.Env -> Var -> Subst -> AxiomEq -> AxiomEq
-- REBARE: qualifyAxiomEq v su eq = subst su eq { eqName = symbol v}

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 forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
"Symbol" (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
|| forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Symbol
x [Symbol]
bs
  Bool -> Bool -> 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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   (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   (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 (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 :: Maybe SizeFun
sizeFunction = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyConInfo -> Maybe SizeFun
sizeFunction TyConInfo
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 :: TyConInfo
rtc_info = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (RTyCon -> TyConInfo
rtc_info RTyCon
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 -- FIXME substEnv env name bs $
    { msName :: LocSymbol
msName = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs     LocSymbol
lname
    , msEqns :: [Def SpecType DataCon]
msEqns = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ty ctor. Measure ty ctor -> [Def ty ctor]
msEqns Measure SpecType DataCon
m
    }
    where
      l :: SourcePos
l      = forall a. Located a -> SourcePos
F.loc  LocSymbol
lname
      lname :: LocSymbol
lname  = 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 :: Body
body  = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l ([Symbol]
bs forall a. [a] -> [a] -> [a]
++ [Symbol]
bs') (forall ty ctor. Def ty ctor -> Body
body Def ty ctor
d) }
    where
      bs' :: [Symbol]
bs'   = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 :: [Def LocBareType LocSymbol]
msEqns = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (forall ty ctor. Measure ty ctor -> [Def ty ctor]
msEqns Measure LocBareType LocSymbol
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 :: [BareType]
dcTheta  = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (DataCtor -> [BareType]
dcTheta  DataCtor
c)
    , dcFields :: [(Symbol, BareType)]
dcFields = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (DataCtor -> [(Symbol, BareType)]
dcFields DataCtor
c)
    , dcResult :: Maybe BareType
dcResult = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (DataCtor -> Maybe BareType
dcResult DataCtor
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 :: Maybe [DataCtor]
tycDCons  = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (DataDecl -> Maybe [DataCtor]
tycDCons  DataDecl
d)
    , tycPropTy :: Maybe BareType
tycPropTy = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (DataDecl -> Maybe BareType
tycPropTy DataDecl
d)
    }

instance Qualify ModSpecs where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs
qualify Env
env ModName
name SourcePos
l [Symbol]
bs = forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
Misc.hashMapMapWithKey (\ModName
_ -> 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, 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 :: [Measure LocBareType LocSymbol]
measures   = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures   BareSpec
sp)
  , asmSigs :: [(LocSymbol, LocBareType)]
asmSigs    = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
asmSigs    BareSpec
sp)
  , sigs :: [(LocSymbol, LocBareType)]
sigs       = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
sigs       BareSpec
sp)
  , localSigs :: [(LocSymbol, LocBareType)]
localSigs  = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
localSigs  BareSpec
sp)
  , reflSigs :: [(LocSymbol, LocBareType)]
reflSigs   = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
reflSigs   BareSpec
sp)
  , dataDecls :: [DataDecl]
dataDecls  = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (forall ty bndr. Spec ty bndr -> [DataDecl]
dataDecls  BareSpec
sp)
  , newtyDecls :: [DataDecl]
newtyDecls = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (forall ty bndr. Spec ty bndr -> [DataDecl]
newtyDecls BareSpec
sp)
  , ialiases :: [(LocBareType, LocBareType)]
ialiases   = [ (LocBareType -> LocBareType
f LocBareType
x, LocBareType -> LocBareType
f LocBareType
y) | (LocBareType
x, LocBareType
y) <- forall ty bndr. Spec ty bndr -> [(ty, ty)]
ialiases BareSpec
sp ]
  }
  where f :: LocBareType -> LocBareType
f      = 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 :: Symbol
rtName  = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (forall x a. RTAlias x a -> Symbol
rtName RTAlias Symbol a
rtAlias)
             , rtTArgs :: [Symbol]
rtTArgs = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (forall x a. RTAlias x a -> [x]
rtTArgs RTAlias Symbol a
rtAlias)
             , rtVArgs :: [Symbol]
rtVArgs = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias Symbol a
rtAlias)
             , rtBody :: a
rtBody  = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (forall x a. RTAlias x a -> a
rtBody RTAlias Symbol a
rtAlias)
             }

instance Qualify F.Expr where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Expr -> Expr
qualify = forall a.
Subable a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
substEnv

instance Qualify RReft where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> RReft -> RReft
qualify = 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 { qBody :: Expr
F.qBody = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name (Qualifier -> SourcePos
F.qPos Qualifier
q) [Symbol]
bs' (Qualifier -> Expr
F.qBody Qualifier
q) }
    where
      bs' :: [Symbol]
bs'                 = [Symbol]
bs forall a. [a] -> [a] -> [a]
++ (QualParam -> Symbol
F.qpSym 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 = 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 = forall r1 r2 c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RType c tv r1 -> RType c tv r2
emapReft (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 = forall r1 r2 c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RType c tv r1 -> RType c tv r2
emapReft (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 = forall a. Subable a => (Symbol -> Expr) -> a -> a
F.substf (Symbol -> Expr
F.EVar 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 = forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Maybe a
maybeResolveSym  Env
env ModName
name String
"Var" LocSymbol
lx
  where
    lx :: LocSymbol
lx                       = 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 forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
kind LocSymbol
lx of
    Right Id
v -> forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe (forall a b. b -> Either a b
Right Id
v) forall a b. b -> Either a b
Right (Env -> LocSymbol -> [Id] -> Maybe Id
lookupLocalVar Env
env LocSymbol
lx [Id
v])
    Left  [Error]
e -> forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe (forall a b. a -> Either a b
Left  [Error]
e) forall a b. b -> Either a b
Right (Env -> LocSymbol -> [Id] -> Maybe Id
lookupLocalVar Env
env LocSymbol
lx [])

  -- where
    -- err e   = Misc.errorP "error-lookupGhcVar" (F.showpp (e, F.loc lx, lx))
  --  err     = Ex.throw

-- | @lookupLocalVar@ takes as input the list of "global" (top-level) vars
--   that also match the name @lx@; we then pick the "closest" definition.
--   See tests/names/LocalSpec.hs for a motivating example.

lookupLocalVar :: Env -> LocSymbol -> [Ghc.Var] -> Maybe Ghc.Var
lookupLocalVar :: Env -> LocSymbol -> [Id] -> Maybe Id
lookupLocalVar Env
env LocSymbol
lx [Id]
gvs = 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: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp (forall a. Located a -> a
F.val LocSymbol
lx, Int
lxn, [(Int, Id)]
kvs)
    kvs :: [(Int, Id)]
kvs                   = [(Int, Id)]
gs forall a. [a] -> [a] -> [a]
++ 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 (forall a. Loc a => a -> Pos
F.srcLine Id
v), Id
v) | Id
v <- [Id]
gvs]
    lxn :: Int
lxn                   = Pos -> Int
F.unPos (forall a. Loc a => a -> Pos
F.srcLine LocSymbol
lx)
    (Maybe Symbol
_, Symbol
x)                = Symbol -> (Maybe Symbol, Symbol)
unQualifySymbol (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 = forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym -- strictResolveSym

lookupGhcTyCon :: Env -> ModName -> String -> LocSymbol -> Lookup Ghc.TyCon
lookupGhcTyCon :: Env -> ModName -> String -> LocSymbol -> Lookup TyCon
lookupGhcTyCon Env
env ModName
name String
k LocSymbol
lx = forall a. PPrint a => String -> a -> a
myTracepp (String
"LOOKUP-TYCON: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp (forall a. Located a -> a
val LocSymbol
lx))
                               forall a b. (a -> b) -> a -> b
$ {- strictResolveSym -} 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 = lookupGhcDnTyConE
lookupGhcDnTyCon :: Env -> ModName -> String -> DataName -> Lookup (Maybe TyCon)
lookupGhcDnTyCon Env
env ModName
name String
msg = forall e r. Env -> ModName -> Either e r -> Either e (Maybe r)
failMaybe Env
env ModName
name 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 forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
msg LocSymbol
s of
      Right TyCon
r -> 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 -> forall a b. b -> Either a b
Right TyCon
r
                   Left  [Error]
_ -> 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataCon -> TyCon
Ghc.dataConTyCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
msg

-------------------------------------------------------------------------------
-- | Checking existence of names
-------------------------------------------------------------------------------
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 forall a. Maybe a
Nothing BareType
t of
    Left [Error]
e  -> forall a. PPrint a => String -> a -> a
myTracepp (String
"knownType: " forall a. [a] -> [a] -> [a]
++ 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        = forall a. Ord a => [a] -> [a]
Misc.sortNub forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall acc c tv r.
(acc -> RType c tv r -> acc) -> acc -> RType c tv r -> acc
foldRType 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 {} = forall c tv r. RType c tv r -> c
rt_tycon RType a tv r
t forall a. a -> [a] -> [a]
: [a]
acc
    f [a]
acc RType a tv r
_         = [a]
acc

-- Aargh. Silly that each of these is the SAME code, only difference is the type.

knownGhcVar :: Env -> ModName -> LocSymbol -> Bool
knownGhcVar :: Env -> ModName -> LocSymbol -> Bool
knownGhcVar Env
env ModName
name LocSymbol
lx = forall a. Maybe a -> Bool
Mb.isJust Maybe Id
v
  where
    v :: Maybe Ghc.Var -- This annotation is crucial
    v :: Maybe Id
v = forall a. PPrint a => String -> a -> a
myTracepp (String
"knownGhcVar " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp LocSymbol
lx)
      forall a b. (a -> b) -> a -> b
$ 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 = forall a. PPrint a => String -> a -> a
myTracepp  String
msg forall a b. (a -> b) -> a -> b
$ forall a. Maybe a -> Bool
Mb.isJust Maybe TyCon
v
  where
    msg :: String
msg = String
"knownGhcTyCon: "  forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp LocSymbol
lx
    v :: Maybe Ghc.TyCon -- This annotation is crucial
    v :: Maybe TyCon
v = 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 = forall a. Maybe a -> Bool
Mb.isJust Maybe DataCon
v
  where
    v :: Maybe Ghc.DataCon -- This annotation is crucial
    v :: Maybe DataCon
v = forall a. PPrint a => String -> a -> a
myTracepp (String
"knownGhcDataCon" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp LocSymbol
lx)
      forall a b. (a -> b) -> a -> b
$ forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Maybe a
maybeResolveSym Env
env ModName
name String
"known-datacon" LocSymbol
lx

-------------------------------------------------------------------------------
-- | Using the environment
-------------------------------------------------------------------------------
class ResolveSym a where
  resolveLocSym :: Env -> ModName -> String -> LocSymbol -> Lookup a

instance ResolveSym Ghc.Var where
  resolveLocSym :: Env -> ModName -> String -> LocSymbol -> Lookup Id
resolveLocSym = forall a.
PPrint a =>
Doc
-> (TyThing -> Maybe a)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup a
resolveWith Doc
"variable" forall a b. (a -> b) -> a -> b
$ \case
                    Ghc.AnId Id
x -> forall a. a -> Maybe a
Just Id
x
                    TyThing
_          -> forall a. Maybe a
Nothing

instance ResolveSym Ghc.TyCon where
  resolveLocSym :: Env -> ModName -> String -> LocSymbol -> Lookup TyCon
resolveLocSym = forall a.
PPrint a =>
Doc
-> (TyThing -> Maybe a)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup a
resolveWith Doc
"type constructor" forall a b. (a -> b) -> a -> b
$ \case
                    Ghc.ATyCon TyCon
x -> forall a. a -> Maybe a
Just TyCon
x
                    TyThing
_            -> forall a. Maybe a
Nothing

instance ResolveSym Ghc.DataCon where
  resolveLocSym :: Env -> ModName -> String -> LocSymbol -> Lookup DataCon
resolveLocSym = forall a.
PPrint a =>
Doc
-> (TyThing -> Maybe a)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup a
resolveWith Doc
"data constructor" forall a b. (a -> b) -> a -> b
$ \case
                    Ghc.AConLike (Ghc.RealDataCon DataCon
x) -> forall a. a -> Maybe a
Just DataCon
x
                    TyThing
_                                -> forall a. Maybe a
Nothing


{- Note [ResolveSym for Symbol]

In case we need to resolve (aka qualify) a 'Symbol', we need to do some extra work. Generally speaking,
all these 'ResolveSym' instances perform a lookup into a 'Map' keyed by the 'Symbol' in
order to find a 'TyThing'. More specifically such map is known as the 'TyThingMap':

type TyThingMap = M.HashMap F.Symbol [(F.Symbol, Ghc.TyThing)]

This means, in practice, that we might have more than one result indexed by a given 'Symbol', and we need
to make a choice. The function 'rankedThings' does this. By default, we try to extract only /identifiers/
(i.e. a GHC's 'Id') out of an input 'TyThing', but in the case of test \"T1688\", something different happened.
By tracing calls to 'rankedThings' (called by 'resolveLocSym') there were cases where we had something like
this as our input TyThingMap:

[
 1 : T1688Lib : Data constructor T1688Lib.Lambda,
 1 : T1688Lib : Identifier T1688Lib.Lambda
]

Here name resolution worked because 'resolveLocSym' used the 'ResolveSym' instance defined for 'GHC.Var' that
looks only for 'Id's (contained inside 'Identifier's, and we had one). In some other cases, though,
'resolveLocSym' got called with only this:

[1 : T1688Lib : Data constructor T1688Lib.Lambda]

This would /not/ yield a match, despite the fact a \"Data constructor\" in principle /does/ contain an 'Id'
(it can be extracted out of a 'RealDataCon' by calling 'dataConWorkId'). In the case of test T1688, such
failed lookup caused the 'Symbol' to /not/ qualify, which in turn caused the symbols inside the type synonym:

ProofOf( Step (App (Lambda x e) v) e)

To not qualify. Finally, by the time 'expand' was called, the 'ProofOf' type alias would be replaced with
the correct refinement, but the unqualified 'Symbol's would now cause a test failure when refining the client
module.

It's not clear to me (Alfredo) why 'resolveLocSym' is called multiple times within the same module with
different inputs, but it definitely makes sense to allow for the special case here, at least for 'Symbol's.

Probably finding the /root cause/ would entail partially rewriting the name resoultion engine.

-}


instance ResolveSym F.Symbol where
  resolveLocSym :: Env -> ModName -> String -> LocSymbol -> Either [Error] Symbol
resolveLocSym Env
env ModName
name String
_ LocSymbol
lx =
    -- If we can't resolve the input 'Symbol' from an 'Id', try again
    -- by grabbing the 'Id' of an 'AConLike', if any.
    -- See Note [ResolveSym for Symbol].
    let resolved :: Lookup Id
resolved =  forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
"Var" LocSymbol
lx
                 forall a. Semigroup a => a -> a -> a
<> 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]
_               -> forall a b. b -> Either a b
Right (forall a. Located a -> a
val LocSymbol
lx)
      Right (Id
v :: Ghc.Var) -> forall a b. b -> Either a b
Right (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) -> forall a. a -> Maybe a
Just (DataCon -> Id
Ghc.dataConWorkId DataCon
x)
        TyThing
_                                -> 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 Mb.mapMaybe f things of
  case forall k a b. EqHash k => (a -> Maybe b) -> [(k, a)] -> [b]
rankedThings TyThing -> Maybe a
f [((Int, Symbol), TyThing)]
things of
    []  -> forall a b. a -> Either a b
Left [Doc -> String -> LocSymbol -> Error
errResolve Doc
kind String
str LocSymbol
lx]
    [a
x] -> forall a b. b -> Either a b
Right a
x
    [a]
xs  -> forall a b. a -> Either a b
Left [forall t. SrcSpan -> Doc -> [Doc] -> TError t
ErrDupNames SrcSpan
sp (forall a. PPrint a => a -> Doc
pprint (forall a. Located a -> a
F.val LocSymbol
lx)) (forall a. PPrint a => a -> Doc
pprint forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
xs)]
  where
    _xSym :: Symbol
_xSym   = forall a. Located a -> a
F.val LocSymbol
lx
    sp :: SrcSpan
sp      = SrcSpan -> SrcSpan
GM.fSrcSpanSrcSpan (forall a. Loc a => a -> SrcSpan
F.srcSpan LocSymbol
lx)
    things :: [((Int, Symbol), TyThing)]
things  = forall a. PPrint a => String -> a -> a
myTracepp String
msg 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: " forall a. [a] -> [a] -> [a]
++ String
str forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp (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 forall b a. Ord b => (a -> b) -> [a] -> [a]
Misc.sortOn forall a b. (a, b) -> a
fst (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            = forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (\(k
k, a
x) -> (k
k,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe b
f a
x) [(k, a)]
ias

-------------------------------------------------------------------------------
-- | @lookupTyThing@ is the central place where we lookup the @Env@ to find
--   any @Ghc.TyThing@ that match that name. The code is a bit hairy as we
--   have various heuristics to approximiate how GHC resolves names. e.g.
--   see tests-names-pos-*.hs, esp. vector04.hs where we need the name `Vector`
--   to resolve to `Data.Vector.Vector` and not `Data.Vector.Generic.Base.Vector`...
-------------------------------------------------------------------------------
lookupTyThing :: Env -> ModName -> LocSymbol -> [((Int, F.Symbol), Ghc.TyThing)]
-------------------------------------------------------------------------------
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             = forall b a. Ord b => (a -> b) -> [a] -> [a]
Misc.sortOn forall a b. (a, b) -> a
fst (forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [((Int, Symbol), TyThing)]
matches)
    matches :: [((Int, Symbol), TyThing)]
matches                = forall a. PPrint a => String -> a -> a
myTracepp (String
"matches-" 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      <- forall a. PPrint a => String -> a -> a
myTracepp String
msg 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: " forall a. [a] -> [a] -> [a]
++ 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 (forall a. Located a -> a
F.val LocSymbol
lsym)
    nameSym :: Symbol
nameSym                = forall a. Symbolic a => a -> Symbol
F.symbol ModName
mdname
    mm :: Symbol -> Symbol -> Maybe [Symbol] -> [Int]
mm Symbol
name Symbol
m Maybe [Symbol]
mods         = forall a. PPrint a => String -> a -> a
myTracepp (String
"matchMod: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp (LocSymbol
lsym, Symbol
name, Symbol
m, Maybe [Symbol]
mods)) 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 = forall a. PPrint a => String -> a -> a
myTracepp (String
"lookupThings: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp Symbol
x)
                   forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
Mb.fromMaybe [] forall a b. (a -> b) -> a -> b
$ Symbol -> Maybe [(Symbol, TyThing)]
get Symbol
x 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          = 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               -- Score UNQUALIFIED names
     | Symbol
defName forall a. Eq a => a -> a -> Bool
== Symbol
tgtName = [Int
0]                       -- prioritize names defined in *this* module
     | Bool
otherwise          = [Env -> Symbol -> Int -> Int
matchImp Env
env Symbol
defName Int
1]  -- prioritize directly imported modules over
                                                      -- names coming from elsewhere, with a

    go (Just [Symbol]
ms)             -- Score QUALIFIED names
     |  Symbol -> Bool
isEmptySymbol Symbol
defName
     Bool -> Bool -> Bool
&& [Symbol]
ms forall a. Eq a => a -> a -> Bool
== [Symbol
tgtName]   = [Int
0]                       -- local variable, see tests-names-pos-local00.hs
     | [Symbol]
ms forall a. Eq a => a -> a -> Bool
== [Symbol
defName]    = [Int
1]
     | Bool
isExt              = [Env -> Symbol -> Int -> Int
matchImp Env
env Symbol
defName Int
2]  -- to allow matching re-exported names e.g. Data.Set.union for Data.Set.Internal.union
     | Bool
otherwise          = []
     where
       isExt :: Bool
isExt              = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol -> Symbol -> Bool
`isParentModuleOf` Symbol
defName) [Symbol]
ms

-- | Returns 'True' if the 'Symbol' given as a first argument represents a parent module for the second.
--
-- >>> L.symbolic "Data.Text" `isParentModuleOf` L.symbolic "Data.Text.Internal"
-- True
--
-- Invariants:
--
-- * The empty 'Symbol' is always considered the module prefix of the second,
--   in compliance with 'isPrefixOfSym' (AND: why?)
-- * If the parent \"hierarchy\" is smaller than the children's one, this is clearly not a parent module.
isParentModuleOf :: F.Symbol -> F.Symbol -> Bool
isParentModuleOf :: Symbol -> Symbol -> Bool
isParentModuleOf Symbol
parentModule Symbol
childModule
  | Symbol -> Bool
isEmptySymbol Symbol
parentModule = Bool
True
  | Bool
otherwise                  =
    forall (t :: * -> *) a. Foldable t => t a -> Int
length [Text]
parentHierarchy forall a. Ord a => a -> a -> Bool
<= forall (t :: * -> *) a. Foldable t => t a -> Int
length [Text]
childHierarchy Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Eq a => a -> a -> Bool
(==)) (forall a b. [a] -> [b] -> [(a, b)]
zip [Text]
parentHierarchy [Text]
childHierarchy)
  where
    parentHierarchy :: [T.Text]
    parentHierarchy :: [Text]
parentHierarchy = Text -> Text -> [Text]
T.splitOn Text
"." forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
F.symbolText forall a b. (a -> b) -> a -> b
$ Symbol
parentModule

    childHierarchy :: [T.Text]
    childHierarchy :: [Text]
childHierarchy = Text -> Text -> [Text]
T.splitOn Text
"." forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
F.symbolText 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 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         = 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@ lets us prioritize @TyThing@ defined in directly imported modules over
--   those defined elsewhere. Specifically, in decreasing order of priority we have
--   TyThings that we:
--   * DIRECTLY     imported WITHOUT qualification
--   * TRANSITIVELY imported (e.g. were re-exported by SOME imported module)
--   * QUALIFIED    imported (so qualify the symbol to get this result!)

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 forall a. Num a => a -> a -> a
+ Int
2
  | Bool
otherwise      = Int
i forall a. Num a => a -> a -> a
+ Int
1
  where
    isUnqualImport :: Bool
isUnqualImport = 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   = forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
defName (QImports -> HashSet Symbol
qiModules (Env -> QImports
reQualImps Env
env))


-- | `unQualifySymbol name sym` splits `sym` into a pair `(mod, rest)` where
--   `mod` is the name of the module, derived from `sym` if qualified.
unQualifySymbol :: F.Symbol -> (Maybe F.Symbol, F.Symbol)
unQualifySymbol :: Symbol -> (Maybe Symbol, Symbol)
unQualifySymbol Symbol
sym
  | Symbol -> Bool
GM.isQualifiedSym Symbol
sym = forall a c b. (a -> c) -> (a, b) -> (c, b)
Misc.mapFst forall a. a -> Maybe a
Just (Symbol -> (Symbol, Symbol)
splitModuleNameExact Symbol
sym)
  | Bool
otherwise             = (forall a. Maybe a
Nothing, Symbol
sym)

splitModuleNameExact :: F.Symbol -> (F.Symbol, F.Symbol)
splitModuleNameExact :: Symbol -> (Symbol, Symbol)
splitModuleNameExact Symbol
x' = forall a. PPrint a => String -> a -> a
myTracepp (String
"splitModuleNameExact for " forall a. [a] -> [a] -> [a]
++ 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 = forall t. SrcSpan -> Doc -> Doc -> Doc -> TError t
ErrResolve (forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSymbol
lx) Doc
k (forall a. PPrint a => a -> Doc
F.pprint (forall a. Located a -> a
F.val LocSymbol
lx)) (String -> Doc
PJ.text String
msg)

-- -- | @strictResolve@ wraps the plain @resolve@ to throw an error
-- --   if the name being searched for is unknown.
-- strictResolveSym :: (ResolveSym a) => Env -> ModName -> String -> LocSymbol -> a
-- strictResolveSym env name kind x = case resolveLocSym env name kind x of
--   Left  err -> Misc.errorP "error-strictResolveSym" (F.showpp err)
--   Right val -> val

-- | @maybeResolve@ wraps the plain @resolve@ to return @Nothing@
--   if the name being searched for is unknown.
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 forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
kind LocSymbol
x of
  Left  [Error]
_   -> forall a. Maybe a
Nothing
  Right a
val -> forall a. a -> Maybe a
Just a
val

-------------------------------------------------------------------------------
-- | @ofBareType@ and @ofBareTypeE@ should be the _only_ @SpecType@ constructors
-------------------------------------------------------------------------------
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 = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall {a}. [Error] -> a
fail' 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'                  = forall a e. Exception e => e -> a
Ex.throw
    -- fail                   = Misc.errorP "error-ofBareType" . F.showpp

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 = 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
        = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t c tv r.
SourcePos
-> ((UsedPVar -> UsedPVar) -> t) -> [UsedPVar] -> RType c tv r -> t
txParam SourcePos
l (UsedPVar -> UsedPVar) -> RReft -> RReft
RT.subvUReft (forall t. PVar t -> UsedPVar
RT.uPVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVar BSort]
πs) BareType
t
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareType -> RReft -> RReft
fixReftTyVars BareType
t       -- same as fixCoercions
  where
    πs :: [PVar BSort]
πs  = forall a. a -> Maybe a -> a
Mb.fromMaybe [PVar BSort]
tπs Maybe [PVar BSort]
ps
    tπs :: [PVar BSort]
tπs = forall c tv r. RTypeRep c tv r -> [PVar (RType c tv ())]
ty_preds (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         = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (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           = forall tv c r. Ord tv => RType c tv r -> [tv]
RT.allTyVars BareType
bt
    specTvSymbol :: BTyVar -> Symbol
specTvSymbol  = forall a. Symbolic a => a -> Symbol
F.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 :: Reft
ur_reft = CoSub -> Reft -> Reft
coSubReft CoSub
su (forall r. UReft r -> r
ur_reft RReft
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 = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a. String -> String -> a
Misc.errorP String
"error-ofBSort" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PPrint a => a -> String
F.showpp) forall a. a -> a
id (Env
-> ModName -> SourcePos -> BSort -> Lookup (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 -> Lookup (RType RTyCon RTyVar ())
ofBSortE Env
env ModName
name SourcePos
l BSort
t = forall r.
Expandable r =>
Env
-> ModName
-> ([Symbol] -> r -> r)
-> SourcePos
-> BRType r
-> Lookup (RRType r)
ofBRType Env
env ModName
name (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 = 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 (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 :: [((), Symbol, Expr)]
pargs = [((), Symbol, Expr)]
args' }
  where
    args' :: [((), Symbol, Expr)]
args' | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
π)) = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(()
_,Symbol
x ,Expr
_) (()
t,Symbol
_,Expr
y) -> (()
t, Symbol
x, Expr
y)) (forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
π') (forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
π)
          | Bool
otherwise            = forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
π'
    π' :: UsedPVar
π'    = forall a. a -> Maybe a -> a
Mb.fromMaybe forall {a}. a
err forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (forall t. PVar t -> Symbol
pname UsedPVar
π) HashMap Symbol UsedPVar
m
    err :: a
err   = forall a. UserError -> a
uError forall a b. (a -> b) -> a -> b
$ forall t. SrcSpan -> Doc -> TError t
ErrUnbPred SrcSpan
sp (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 = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(forall t. PVar t -> Symbol
pname UsedPVar
π, UsedPVar
π) | UsedPVar
π <- [UsedPVar]
πs forall a. [a] -> [a] -> [a]
++ 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 = forall a b. (a -> b) -> [a] -> [b]
map forall t. PVar t -> UsedPVar
RT.uPVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c tv r. RTypeRep c tv r -> [PVar (RType c tv ())]
ty_preds forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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             = 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  = 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 :: Maybe Bool
permitTC = forall a. a -> Maybe a
Just (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig Env
env))} forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall {r} {c} {tv}.
(Reftable r, TyConable c) =>
Symbol -> RType c tv r -> RType c tv r
rebind Symbol
x 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) 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
xforall a. a -> [a] -> [a]
:[Symbol]
bs) RType BTyCon BTyVar r
t2 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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              = forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 RType c tv r
t (Symbol
x, Symbol -> Expr
F.EVar forall a b. (a -> b) -> a -> b
$ 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)  = forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy 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 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 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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)        = forall c tv r. tv -> r -> RType c tv r
RVar (BTyVar -> RTyVar
RT.bareRTyVar BTyVar
a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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)     = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT forall {s2}. RTVar RTyVar s2
a' 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 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
      where a' :: RTVar RTyVar s2
a'              = forall tv s1 s2. RTVar tv s1 -> RTVar tv s2
dropTyVarInfo (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)       = forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP RPVar
a' 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)   = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
x  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    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)     = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx   Symbol
x  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    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
xforall 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)  = forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either [Error] [(Symbol, RType RTyCon RTyVar r)]
xts' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Oblig
o 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'            = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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)         = forall c tv r. r -> RType c tv r
RHole    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
    go [Symbol]
bs (RExprArg Located Expr
le)     = forall (m :: * -> *) a. Monad m => a -> m a
return    forall a b. (a -> b) -> a -> b
$ forall c tv r. Located Expr -> RType c tv r
RExprArg (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)) = forall τ r c tv. [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
rPropP forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {t}.
(t, BSort) -> Either [Error] (t, RType RTyCon RTyVar ())
goSyms [(Symbol, BSort)]
ss forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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)         = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {t}.
(t, BSort) -> Either [Error] (t, RType RTyCon RTyVar ())
goSyms [(Symbol, BSort)]
ss 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,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env
-> ModName -> SourcePos -> BSort -> Lookup (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          = forall r.
Expandable r =>
r
-> Located TyCon
-> [RTProp RTyCon RTyVar r]
-> [RType RTyCon RTyVar r]
-> RType RTyCon RTyVar r
bareTCApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Either [Error] (Located TyCon)
lc' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Symbol]
-> RTProp BTyCon BTyVar r
-> Either [Error] (RTProp RTyCon RTyVar r)
goRef [Symbol]
bs) [RTProp BTyCon BTyVar r]
rs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t 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'                    = forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
lc 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 (forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType BTyCon BTyVar r]
ts)
        lc :: LocSymbol
lc                     = BTyCon -> LocSymbol
btc_tc BTyCon
tc
    -- goRApp _ _ _ _             = impossible Nothing "goRApp failed through to final case"

{-
    -- TODO-REBARE: goRImpF bounds _ (RApp c ps' _ _) t _
    -- TODO-REBARE:  | Just bnd <- M.lookup (btc_tc c) bounds
    -- TODO-REBARE:   = do let (ts', ps) = splitAt (length $ tyvars bnd) ps'
    -- TODO-REBARE:        ts <- mapM go ts'
    -- TODO-REBARE:        makeBound bnd ts [x | RVar (BTV x) _ <- ps] <$> go t
    -- TODO-REBARE: goRFun bounds _ (RApp c ps' _ _) t _
    -- TODO-REBARE: | Just bnd <- M.lookup (btc_tc c) bounds
    -- TODO-REBARE: = do let (ts', ps) = splitAt (length $ tyvars bnd) ps'
    -- TODO-REBARE: ts <- mapM go ts'
    -- TODO-REBARE: makeBound bnd ts [x | RVar (BTV x) _ <- ps] <$> go t

  -- TODO-REBARE: ofBareRApp env name t@(F.Loc _ _ !(RApp tc ts _ r))
  -- TODO-REBARE: | Loc l _ c <- btc_tc tc
  -- TODO-REBARE: , Just rta <- M.lookup c aliases
  -- TODO-REBARE: = appRTAlias l rta ts =<< resolveReft r

-}

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
  | forall c. TyConable c => c -> Bool
isList Symbol
c Bool -> Bool -> Bool
&& Int
arity forall a. Eq a => a -> a -> Bool
== Int
1  = forall a b. b -> Either a b
Right TyCon
Ghc.listTyCon
  | forall c. TyConable c => c -> Bool
isTuple Symbol
c               = forall a b. b -> Either a b
Right TyCon
tuplTc
  | Bool
otherwise               = 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: " forall a. [a] -> [a] -> [a]
++ 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 forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType RTyCon RTyVar r]
ts
      then forall a e. Exception e => e -> a
Ex.throw Error
err -- error (F.showpp err)
      else forall r c tv.
Reftable r =>
RType c tv r
-> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
tyApp (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 forall a b. (a -> b) -> a -> b
$ forall r. Monoid r => Type -> RRType r
RT.ofType Type
rhs) (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) <- 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  = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Id
a RType RTyCon RTyVar r
t -> (Id -> RTyVar
RT.rTyVar Id
a, 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 = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
tvs

       err :: Error
       err :: Error
err = forall t. SrcSpan -> Doc -> SrcSpan -> Doc -> TError t
ErrAliasApp (SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l) (forall a. PPrint a => a -> Doc
pprint TyCon
c) (forall a. NamedThing a => a -> SrcSpan
Ghc.getSrcSpan TyCon
c)
                         ([Doc] -> Doc
PJ.hcat [ String -> Doc
PJ.text String
"Expects"
                                  , forall a. PPrint a => a -> Doc
pprint (TyCon -> Int
GM.realTcArity TyCon
c)
                                  , String -> Doc
PJ.text String
"arguments, but is given"
                                  , forall a. PPrint a => a -> Doc
pprint (forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType RTyCon RTyVar r]
ts) ] )
-- TODO expandTypeSynonyms here to
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
&& forall r c tv. (Reftable r, TyConable c) => RType c tv r -> Bool
isTrivial RType RTyCon RTyVar r
t
  = forall r. Expandable r => RRType r -> RRType r
expandRTypeSynonyms (RType RTyCon RTyVar r
t 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 = 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 forall a. Monoid a => a
mempty

bareTCApp r
r (Loc SourcePos
_ SourcePos
_ TyCon
c) [RTProp RTyCon RTyVar r]
rs [RType RTyCon RTyVar r]
ts
  = 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' = 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 forall a. [a] -> [a] -> [a]
++ [RType c tv r]
ts') ([RTProp c tv r]
rs forall a. [a] -> [a] -> [a]
++ [RTProp c tv r]
rs') (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 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
_  = forall a. Maybe SrcSpan -> String -> a
panic 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 = forall r. Monoid r => Type -> RRType r
RT.ofType forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
Ghc.expandTypeSynonyms forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. ToTypeable r => Bool -> RRType r -> Type
RT.toType Bool
False

{-
expandRTypeSynonyms :: (Expandable r) => RRType r -> RRType r
expandRTypeSynonyms t
  | rTypeHasHole t = t
  | otherwise      = expandRTypeSynonyms' t

rTypeHasHole :: RType c tv r -> Bool
rTypeHasHole = foldRType f False
  where
    f _ (RHole _) = True
    f b _         = b
-}

------------------------------------------------------------------------------------------
-- | Is this the SAME as addTyConInfo? No. `txRefSort`
-- (1) adds the _real_ sorts to RProp,
-- (2) gathers _extra_ RProp at turns them into refinements,
--     e.g. tests/pos/multi-pred-app-00.hs
------------------------------------------------------------------------------------------

txRefSort :: TyConMap -> F.TCEmb Ghc.TyCon -> LocSpecType -> LocSpecType
txRefSort :: TyConMap -> TCEmb TyCon -> LocSpecType -> LocSpecType
txRefSort TyConMap
tyi TCEmb TyCon
tce LocSpecType
t = forall l b. Loc l => l -> b -> Located b
F.atLoc LocSpecType
t forall a b. (a -> b) -> a -> b
$ 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 (forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSpecType
t) TCEmb TyCon
tce TyConMap
tyi) (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)
  = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
rc [SpecType]
ts (forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 (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)           = forall r.
ToTypeable r =>
TCEmb TyCon
-> TyConMap -> RTyCon -> [RRType r] -> (RTyCon, [RPVar])
RT.appRTyCon TCEmb TyCon
tce TyConMap
tyi RTyCon
rc [SpecType]
ts
    -- pvs             = rTyConPVs rc'
    ([RTProp RTyCon RTyVar RReft]
rargs, [RTProp RTyCon RTyVar RReft]
rrest)     = forall a. Int -> [a] -> ([a], [a])
splitAt (forall (t :: * -> *) a. Foldable t => t a -> Int
length [RPVar]
pvs) [RTProp RTyCon RTyVar RReft]
rs
    r2 :: RReft
r2                 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' 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' 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' = forall a. a -> Maybe a -> a
Mb.fromMaybe forall a. Monoid a => a
mempty (forall c tv r. RType c tv r -> Maybe r
stripRTypeBase RType c tv r
t') in 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
  | forall t. PVar t -> Bool
isPropPV RPVar
p
  = 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
  = forall a. Maybe SrcSpan -> String -> a
panic 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)) | forall a. Symbolic a => a -> Bool
isDummy RTyVar
v
  = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
xs SpecType
t
    where
      t :: SpecType
t  = forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort (forall t. PVar t -> t
pvType RPVar
p) 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 = 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]))))
  | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
xs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType RTyCon RTyVar ()]
ts
  = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
xts (forall c tv r. r -> RType c tv r
RHole RReft
r)
  | Bool
otherwise
  = -- Misc.errorP "ZONK" $ F.showpp (rc, pname up, i, length xs, length ts)
    forall a. UserError -> a
uError forall a b. (a -> b) -> a -> b
$ forall t. SrcSpan -> Doc -> Doc -> Int -> Int -> Int -> TError t
ErrPartPred SrcSpan
sp (forall a. PPrint a => a -> Doc
pprint s
rc) (forall a. PPrint a => a -> Doc
pprint forall a b. (a -> b) -> a -> b
$ forall t. PVar t -> Symbol
pname UsedPVar
up) Int
i (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
xs) (forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType RTyCon RTyVar ()]
ts)
    where
      xts :: [(Symbol, RType RTyCon RTyVar ())]
xts = forall t t1. String -> [t] -> [t1] -> [(t, t1)]
Misc.safeZipWithError String
"addSymSortRef'" [Symbol]
xs [RType RTyCon RTyVar ()]
ts
      xs :: [Symbol]
xs  = forall a b c. (a, b, c) -> b
Misc.snd3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
up
      ts :: [RType RTyCon RTyVar ()]
ts  = forall a b c. (a, b, c) -> a
Misc.fst3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. PVar t -> [(t, Symbol, Expr)]
pargs RPVar
p

addSymSortRef' SrcSpan
_ s
_ Int
_ RPVar
_ (RProp [(Symbol, RType RTyCon RTyVar ())]
s (RHole RReft
r))
  = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
s (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)
  = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
xs SpecType
t
    where
      xs :: [(Symbol, RType RTyCon RTyVar ())]
xs = 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 = forall {a} {b} {c}. Show a => [a] -> [(b, a, c)] -> [(a, b)]
go (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, b)]
syms) (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)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)forall a. a -> [a] -> [a]
:[a] -> [(b, a, c)] -> [(a, b)]
go [a]
xs [(b, a, c)]
as
    go [a]
xs     []           = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ String
"spliceArgs: " forall a. [a] -> [a] -> [a]
++ String
msg forall a. [a] -> [a] -> [a]
++ String
"on XS=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [a]
xs

---------------------------------------------------------------------------------
-- RJ: formerly, `replaceLocalBinds` AFAICT
-- | @resolveLocalBinds@ resolves that the "free" variables that appear in the
--   type-sigs for non-toplevel binders (that correspond to other locally bound)
--   source variables that are visible at that at non-top-level scope.
--   e.g. tests-names-pos-local02.hs
---------------------------------------------------------------------------------
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 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)         = 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                = forall k v. HashMap k v -> [(k, v)]
M.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap Id (LocBareType, Maybe [Located Expr])
-> HashMap Id (LocBareType, Maybe [Located Expr])
replaceSigs forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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       = forall env acc.
CoreVisitor env acc -> env -> acc -> [CoreBind] -> acc
coreVisitor CoreVisitor SymMap (HashMap Id (LocBareType, Maybe [Located Expr]))
replaceVisitor 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 -> forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
vx (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 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 -> forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Id
v (forall a. PPrint a => String -> a -> a
myTracepp (String
"UPD-LOCAL-SIG " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> String
GM.showPpr Id
v) 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) = (forall a. Subable a => (Symbol -> Expr) -> a -> a
F.substf Symbol -> Expr
tSub LocBareType
t, 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 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                     = forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds (forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (forall a. Located a -> a
F.val LocBareType
t))

qualifySymMap :: SymMap -> F.Symbol -> F.Symbol
qualifySymMap :: SymMap -> Symbol -> Symbol
qualifySymMap SymMap
env Symbol
x = 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 = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (forall a. Maybe a -> Bool
Mb.isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Maybe Symbol
localKey forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst)