-- | 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 = String -> a -> a
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  = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList     [Symbol]
globalSyms
  , reCfg :: Config
reCfg       = Config
cfg
  }
  where
    globalSyms :: [Symbol]
globalSyms  = ((ModName, BareSpec) -> [Symbol])
-> [(ModName, BareSpec)] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ModName, BareSpec) -> [Symbol]
getGlobalSyms [(ModName, BareSpec)]
specs
    syms :: [(Symbol, Id)]
syms        = [ (Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
v, Id
v) | Id
v <- [Id]
vars ]
    vars :: [Id]
vars        = GhcSrc -> [Id]
srcVars GhcSrc
src

getGlobalSyms :: (ModName, BareSpec) -> [F.Symbol]
getGlobalSyms :: (ModName, BareSpec) -> [Symbol]
getGlobalSyms (ModName
_, BareSpec
spec)
  = (Symbol -> Bool) -> [Symbol] -> [Symbol]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Symbol -> Bool) -> Symbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Bool
GM.isQualifiedSym)
       ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ (Measure LocBareType LocSymbol -> Symbol
forall {ty} {ctor}. Measure ty ctor -> Symbol
mbName (Measure LocBareType LocSymbol -> Symbol)
-> [Measure LocBareType LocSymbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [Measure LocBareType LocSymbol]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures  BareSpec
spec)
      [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (Measure LocBareType () -> Symbol
forall {ty} {ctor}. Measure ty ctor -> Symbol
mbName (Measure LocBareType () -> Symbol)
-> [Measure LocBareType ()] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [Measure LocBareType ()]
forall ty bndr. Spec ty bndr -> [Measure ty ()]
cmeasures BareSpec
spec)
      [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (Measure LocBareType LocSymbol -> Symbol
forall {ty} {ctor}. Measure ty ctor -> Symbol
mbName (Measure LocBareType LocSymbol -> Symbol)
-> [Measure LocBareType LocSymbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [Measure LocBareType LocSymbol]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
imeasures BareSpec
spec)
  where
    mbName :: Measure ty ctor -> Symbol
mbName = LocSymbol -> Symbol
forall a. Located a -> a
F.val (LocSymbol -> Symbol)
-> (Measure ty ctor -> LocSymbol) -> Measure ty ctor -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Measure ty ctor -> LocSymbol
forall ty ctor. Measure ty ctor -> LocSymbol
msName

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

-- TODO: rewrite using CoreVisitor
localBinds :: [Ghc.CoreBind] -> [Ghc.Var]
localBinds :: [CoreBind] -> [Id]
localBinds                    = (CoreBind -> [Id]) -> [CoreBind] -> [Id]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (HashSet Symbol -> CoreBind -> [Id]
bgo HashSet Symbol
forall a. HashSet a
S.empty)
  where
    add :: Id -> HashSet Symbol -> HashSet Symbol
add  Id
x HashSet Symbol
g                  = HashSet Symbol
-> (Symbol -> HashSet Symbol) -> Maybe Symbol -> HashSet Symbol
forall b a. b -> (a -> b) -> Maybe a -> b
maybe HashSet Symbol
g (Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
`S.insert` HashSet Symbol
g) (Id -> Maybe Symbol
localKey Id
x)
    adds :: CoreBind -> HashSet Symbol -> HashSet Symbol
adds CoreBind
b HashSet Symbol
g                  = (Id -> HashSet Symbol -> HashSet Symbol)
-> HashSet Symbol -> [Id] -> HashSet Symbol
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Id -> HashSet Symbol -> HashSet Symbol
add HashSet Symbol
g (CoreBind -> [Id]
forall b. Bind b -> [b]
Ghc.bindersOf CoreBind
b)
    take' :: Id -> HashSet Symbol -> [Id]
take' Id
x HashSet Symbol
g                 = [Id] -> (Symbol -> [Id]) -> Maybe Symbol -> [Id]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\Symbol
k -> [Id
x | Bool -> Bool
not (Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
k HashSet Symbol
g)]) (Id -> Maybe Symbol
localKey Id
x)
    pgo :: HashSet Symbol -> (Id, Expr Id) -> [Id]
pgo HashSet Symbol
g (Id
x, Expr Id
e)              = Id -> HashSet Symbol -> [Id]
take' Id
x HashSet Symbol
g [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ HashSet Symbol -> Expr Id -> [Id]
go (Id -> HashSet Symbol -> HashSet Symbol
add Id
x HashSet Symbol
g) Expr Id
e
    bgo :: HashSet Symbol -> CoreBind -> [Id]
bgo HashSet Symbol
g (Ghc.NonRec Id
x Expr Id
e)    = HashSet Symbol -> (Id, Expr Id) -> [Id]
pgo HashSet Symbol
g (Id
x, Expr Id
e)
    bgo HashSet Symbol
g (Ghc.Rec [(Id, Expr Id)]
xes)       = ((Id, Expr Id) -> [Id]) -> [(Id, Expr Id)] -> [Id]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (HashSet Symbol -> (Id, Expr Id) -> [Id]
pgo HashSet Symbol
g) [(Id, Expr Id)]
xes
    go :: HashSet Symbol -> Expr Id -> [Id]
go  HashSet Symbol
g (Ghc.App Expr Id
e Expr Id
a)       = (Expr Id -> [Id]) -> [Expr Id] -> [Id]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (HashSet Symbol -> Expr Id -> [Id]
go  HashSet Symbol
g) [Expr Id
e, Expr Id
a]
    go  HashSet Symbol
g (Ghc.Lam Id
_ Expr Id
e)       = HashSet Symbol -> Expr Id -> [Id]
go HashSet Symbol
g Expr Id
e
    go  HashSet Symbol
g (Ghc.Let CoreBind
b Expr Id
e)       = HashSet Symbol -> CoreBind -> [Id]
bgo HashSet Symbol
g CoreBind
b [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ HashSet Symbol -> Expr Id -> [Id]
go (CoreBind -> HashSet Symbol -> HashSet Symbol
adds CoreBind
b HashSet Symbol
g) Expr Id
e
    go  HashSet Symbol
g (Ghc.Tick CoreTickish
_ Expr Id
e)      = HashSet Symbol -> Expr Id -> [Id]
go HashSet Symbol
g Expr Id
e
    go  HashSet Symbol
g (Ghc.Cast Expr Id
e CoercionR
_)      = HashSet Symbol -> Expr Id -> [Id]
go HashSet Symbol
g Expr Id
e
    go  HashSet Symbol
g (Ghc.Case Expr Id
e Id
_ Type
_ [Alt Id]
cs) = HashSet Symbol -> Expr Id -> [Id]
go HashSet Symbol
g Expr Id
e [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ (Alt Id -> [Id]) -> [Alt Id] -> [Id]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (HashSet Symbol -> Expr Id -> [Id]
go HashSet Symbol
g (Expr Id -> [Id]) -> (Alt Id -> Expr Id) -> Alt Id -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Ghc.Alt AltCon
_ [Id]
_ Expr Id
e') -> Expr Id
e')) [Alt Id]
cs
    go  HashSet Symbol
_ (Ghc.Var Id
_)         = []
    go  HashSet Symbol
_ Expr Id
_                   = []

localVarMap :: [Ghc.Var] -> LocalVars
localVarMap :: [Id] -> LocalVars
localVarMap [Id]
vs =
  [(Symbol, (Int, Id))] -> LocalVars
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group [ (Symbol
x, (Int
i, Id
v)) | Id
v <- [Id]
vs
                           , let i :: Int
i = Pos -> Int
F.unPos (Id -> Pos
forall a. Loc a => a -> Pos
F.srcLine Id
v)
                           , Symbol
x <- Maybe Symbol -> [Symbol]
forall a. Maybe a -> [a]
Mb.maybeToList (Id -> Maybe Symbol
localKey Id
v)
             ]

localKey   :: Ghc.Var -> Maybe F.Symbol
localKey :: Id -> Maybe Symbol
localKey Id
v
  | Symbol -> Bool
isLocal Symbol
m = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just Symbol
x
  | Bool
otherwise = Maybe Symbol
forall a. Maybe a
Nothing
  where
    (Symbol
m, Symbol
x)    = Symbol -> (Symbol, Symbol)
splitModuleNameExact (Symbol -> (Symbol, Symbol))
-> (Id -> Symbol) -> Id -> (Symbol, Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
GM.dropModuleUnique (Symbol -> Symbol) -> (Id -> Symbol) -> Id -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Id -> (Symbol, Symbol)) -> Id -> (Symbol, Symbol)
forall a b. (a -> b) -> a -> b
$ Id
v

makeVarSubst :: GhcSrc -> F.Subst
makeVarSubst :: GhcSrc -> Subst
makeVarSubst GhcSrc
src = [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol, Expr)]
unqualSyms
  where
    unqualSyms :: [(Symbol, Expr)]
unqualSyms   = [ (Symbol
x, Id -> Expr
mkVarExpr Id
v)
                       | (Symbol
x, [(Symbol, Id)]
mxs) <- HashMap Symbol [(Symbol, Id)] -> [(Symbol, [(Symbol, Id)])]
forall k v. HashMap k v -> [(k, v)]
M.toList (GhcSrc -> HashMap Symbol [(Symbol, Id)]
makeSymMap GhcSrc
src)
                       , Bool -> Bool
not (Symbol -> Bool
isWiredInName Symbol
x)
                       , Id
v <- Maybe Id -> [Id]
forall a. Maybe a -> [a]
Mb.maybeToList (Symbol -> [(Symbol, Id)] -> Maybe Id
forall a. Symbol -> [(Symbol, a)] -> Maybe a
okUnqualified Symbol
me [(Symbol, Id)]
mxs)
                   ]
    me :: Symbol
me           = ModName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (GhcSrc -> ModName
_giTargetMod GhcSrc
src)

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


makeSymMap :: GhcSrc -> M.HashMap F.Symbol [(F.Symbol, Ghc.Var)]
makeSymMap :: GhcSrc -> HashMap Symbol [(Symbol, Id)]
makeSymMap GhcSrc
src = [(Symbol, (Symbol, Id))] -> HashMap Symbol [(Symbol, Id)]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group [ (Symbol
sym, (Symbol
m, Id
x))
                                | Id
x           <- GhcSrc -> [Id]
srcVars GhcSrc
src
                                , let (Symbol
m, Symbol
sym) = Id -> (Symbol, Symbol)
forall a. Symbolic a => a -> (Symbol, Symbol)
qualifiedSymbol Id
x ]

makeTyThingMap :: GhcSrc -> TyThingMap
makeTyThingMap :: GhcSrc -> TyThingMap
makeTyThingMap GhcSrc
src =
  TyThingMap -> TyThingMap
forall {k} {a}.
(Hashable k, Eq a, IsString k, IsString a) =>
HashMap k [(a, TyThing)] -> HashMap k [(a, TyThing)]
addListTyConName (TyThingMap -> TyThingMap) -> TyThingMap -> TyThingMap
forall a b. (a -> b) -> a -> b
$
  [(Symbol, (Symbol, TyThing))] -> TyThingMap
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group [ (Symbol
x, (Symbol
m, TyThing
t))  | TyThing
t         <- GhcSrc -> [TyThing]
srcThings GhcSrc
src
                            , Symbol
tSym      <- Maybe Symbol -> [Symbol]
forall a. Maybe a -> [a]
Mb.maybeToList (TyThing -> Maybe Symbol
tyThingSymbol TyThing
t)
                            , let (Symbol
m, Symbol
x) = Symbol -> (Symbol, Symbol)
forall a. Symbolic a => a -> (Symbol, Symbol)
qualifiedSymbol Symbol
tSym
                            , Bool -> Bool
not (Symbol -> Bool
isLocal Symbol
m)
             ]
  where
    -- We add the TyThing for the List constructor here. Otherwise, we
    -- lookups in the TyThingMap will fail for "List" and not for "[]".
    addListTyConName :: HashMap k [(a, TyThing)] -> HashMap k [(a, TyThing)]
addListTyConName HashMap k [(a, TyThing)]
m =
      case k -> HashMap k [(a, TyThing)] -> Maybe [(a, TyThing)]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup k
"[]" HashMap k [(a, TyThing)]
m of
        Maybe [(a, TyThing)]
Nothing -> HashMap k [(a, TyThing)]
m
        Just [(a, TyThing)]
ps -> ([(a, TyThing)] -> [(a, TyThing)] -> [(a, TyThing)])
-> k
-> [(a, TyThing)]
-> HashMap k [(a, TyThing)]
-> HashMap k [(a, TyThing)]
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
M.insertWith [(a, TyThing)] -> [(a, TyThing)] -> [(a, TyThing)]
forall a. [a] -> [a] -> [a]
(++) k
"List" ([(a, TyThing)] -> [(a, TyThing)]
forall {a}. (Eq a, IsString a) => [(a, TyThing)] -> [(a, TyThing)]
filterListTyCon [(a, TyThing)]
ps) HashMap k [(a, TyThing)]
m

    -- The TyCon name in the TyThing for @"[]"@ must be @"[]"@ apparently.
    --
    -- listTyCon uses "List", and that made later checks fail for some tests,
    -- so we cannot just return @[("GHC.Types", ATyCon listTyCon)]@
    --
    -- Returning the TyCon that GHC yields for @"[]"@ has later tests fail,
    -- because that TyCon has no associated data constructors.
    --
    -- The solution we adopted for now is to return listTyCon, and use
    -- the name from the TyThing that GHC returned.
    filterListTyCon :: [(a, TyThing)] -> [(a, TyThing)]
filterListTyCon [(a, TyThing)]
ps =
      [ (a
mn, TyCon -> TyThing
Ghc.ATyCon TyCon
tc') | (a
mn, Ghc.ATyCon TyCon
tc) <- [(a, TyThing)]
ps
          , a
"GHC.Types" a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
mn
          , let tc' :: TyCon
tc' = TyCon
Ghc.listTyCon { Ghc.tyConName = Ghc.tyConName tc }
      ]

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


conLikeSymbol :: Ghc.ConLike -> Maybe F.Symbol
conLikeSymbol :: ConLike -> Maybe Symbol
conLikeSymbol (Ghc.RealDataCon DataCon
d) = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just (DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol DataCon
d)
conLikeSymbol ConLike
_z                   = Maybe Symbol
forall a. Maybe a
Nothing -- 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 (Symbol -> (Symbol, Symbol))
-> (a -> Symbol) -> a -> (Symbol, Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol

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

srcThings :: GhcSrc -> [Ghc.TyThing]
srcThings :: GhcSrc -> [TyThing]
srcThings GhcSrc
src = String -> [TyThing] -> [TyThing]
forall a. PPrint a => String -> a -> a
myTracepp String
"SRCTHINGS"
              ([TyThing] -> [TyThing]) -> [TyThing] -> [TyThing]
forall a b. (a -> b) -> a -> b
$ (TyThing -> String) -> [TyThing] -> [TyThing]
forall b a. Ord b => (a -> b) -> [a] -> [a]
Misc.hashNubWith TyThing -> String
forall a. PPrint a => a -> String
F.showpp (GhcSrc -> [TyThing]
_gsTyThings GhcSrc
src [TyThing] -> [TyThing] -> [TyThing]
forall a. [a] -> [a] -> [a]
++ GhcSrc -> [TyThing]
mySrcThings GhcSrc
src)

mySrcThings :: GhcSrc -> [Ghc.TyThing]
mySrcThings :: GhcSrc -> [TyThing]
mySrcThings GhcSrc
src = [ Id -> TyThing
Ghc.AnId   Id
x | Id
x <- [Id]
vars ]
               [TyThing] -> [TyThing] -> [TyThing]
forall a. [a] -> [a] -> [a]
++ [ TyCon -> TyThing
Ghc.ATyCon TyCon
c | TyCon
c <- [TyCon]
tcs  ]
               [TyThing] -> [TyThing] -> [TyThing]
forall a. [a] -> [a] -> [a]
++ [ DataCon -> TyThing
aDataCon   DataCon
d | DataCon
d <- [DataCon]
dcs  ]
  where
    vars :: [Id]
vars        = [Id] -> [Id]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([Id] -> [Id]) -> [Id] -> [Id]
forall a b. (a -> b) -> a -> b
$ [DataCon] -> [Id]
dataConVars [DataCon]
dcs [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ GhcSrc -> [Id]
srcVars  GhcSrc
src
    dcs :: [DataCon]
dcs         = [DataCon] -> [DataCon]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([DataCon] -> [DataCon]) -> [DataCon] -> [DataCon]
forall a b. (a -> b) -> a -> b
$ (TyCon -> [DataCon]) -> [TyCon] -> [DataCon]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TyCon -> [DataCon]
Ghc.tyConDataCons [TyCon]
tcs
    tcs :: [TyCon]
tcs         = [TyCon] -> [TyCon]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall a b. (a -> b) -> a -> b
$ GhcSrc -> [TyCon]
srcTyCons GhcSrc
src
    aDataCon :: DataCon -> TyThing
aDataCon    = ConLike -> TyThing
Ghc.AConLike (ConLike -> TyThing) -> (DataCon -> ConLike) -> DataCon -> TyThing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> ConLike
Ghc.RealDataCon

srcTyCons :: GhcSrc -> [Ghc.TyCon]
srcTyCons :: GhcSrc -> [TyCon]
srcTyCons GhcSrc
src = [[TyCon]] -> [TyCon]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ GhcSrc -> [TyCon]
_gsTcs     GhcSrc
src
  , GhcSrc -> [TyCon]
_gsFiTcs   GhcSrc
src
  , GhcSrc -> [TyCon]
_gsPrimTcs GhcSrc
src
  , GhcSrc -> [TyCon]
srcVarTcs GhcSrc
src
  ]

srcVarTcs :: GhcSrc -> [Ghc.TyCon]
srcVarTcs :: GhcSrc -> [TyCon]
srcVarTcs = [Id] -> [TyCon]
varTyCons ([Id] -> [TyCon]) -> (GhcSrc -> [Id]) -> GhcSrc -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GhcSrc -> [Id]
srcVars

varTyCons :: [Ghc.Var] -> [Ghc.TyCon]
varTyCons :: [Id] -> [TyCon]
varTyCons = (Id -> [TyCon]) -> [Id] -> [TyCon]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Type -> [TyCon]
typeTyCons (Type -> [TyCon]) -> (Id -> Type) -> Id -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
Ghc.dropForAlls (Type -> Type) -> (Id -> Type) -> Id -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Type
Ghc.varType)

typeTyCons :: Ghc.Type -> [Ghc.TyCon]
typeTyCons :: Type -> [TyCon]
typeTyCons Type
t = Type -> [TyCon]
tops Type
t [TyCon] -> [TyCon] -> [TyCon]
forall a. [a] -> [a] -> [a]
++ Type -> [TyCon]
inners Type
t
  where
    tops :: Type -> [TyCon]
tops     = Maybe TyCon -> [TyCon]
forall a. Maybe a -> [a]
Mb.maybeToList (Maybe TyCon -> [TyCon])
-> (Type -> Maybe TyCon) -> Type -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe TyCon
Ghc.tyConAppTyCon_maybe
    inners :: Type -> [TyCon]
inners   = (Type -> [TyCon]) -> [Type] -> [TyCon]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [TyCon]
typeTyCons ([Type] -> [TyCon]) -> (Type -> [Type]) -> Type -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, [Type]) -> [Type]
forall a b. (a, b) -> b
snd ((Type, [Type]) -> [Type])
-> (Type -> (Type, [Type])) -> Type -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> (Type, [Type])
Ghc.splitAppTys

-- | 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 = (Id -> Bool) -> [Id] -> [Id]
forall a. (a -> Bool) -> [a] -> [a]
filter Id -> Bool
Ghc.isId ([Id] -> [Id])
-> ([(Int, Symbol, Id)] -> [Id]) -> [(Int, Symbol, Id)] -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  ((Int, Symbol, Id) -> Id) -> [(Int, Symbol, Id)] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, Symbol, Id) -> Id
forall a b c. (a, b, c) -> c
Misc.thd3 ([(Int, Symbol, Id)] -> [Id])
-> ([(Int, Symbol, Id)] -> [(Int, Symbol, Id)])
-> [(Int, Symbol, Id)]
-> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Int, Symbol, Id)] -> [(Int, Symbol, Id)]
forall r k v.
(Ord r, Hashable k, Eq k) =>
[(r, k, v)] -> [(r, k, v)]
Misc.fstByRank ([(Int, Symbol, Id)] -> [Id]) -> [(Int, Symbol, Id)] -> [Id]
forall a b. (a -> b) -> a -> b
$ [[(Int, Symbol, Id)]] -> [(Int, Symbol, Id)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ String -> Int -> Id -> (Int, Symbol, Id)
key String
"SRC-VAR-DEF" Int
0 (Id -> (Int, Symbol, Id)) -> [Id] -> [(Int, Symbol, Id)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSrc -> [Id]
_giDefVars GhcSrc
src
  , String -> Int -> Id -> (Int, Symbol, Id)
key String
"SRC-VAR-DER" Int
1 (Id -> (Int, Symbol, Id)) -> [Id] -> [(Int, Symbol, Id)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet Id -> [Id]
forall a. HashSet a -> [a]
S.toList (GhcSrc -> HashSet Id
_giDerVars GhcSrc
src)
  , String -> Int -> Id -> (Int, Symbol, Id)
key String
"SRC-VAR-IMP" Int
2 (Id -> (Int, Symbol, Id)) -> [Id] -> [(Int, Symbol, Id)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSrc -> [Id]
_giImpVars GhcSrc
src
  , String -> Int -> Id -> (Int, Symbol, Id)
key String
"SRC-VAR-USE" Int
3 (Id -> (Int, Symbol, Id)) -> [Id] -> [(Int, Symbol, Id)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSrc -> [Id]
_giUseVars GhcSrc
src
  , String -> Int -> Id -> (Int, Symbol, Id)
key String
"SRC-VAR-THN" Int
4 (Id -> (Int, Symbol, Id)) -> [Id] -> [(Int, Symbol, Id)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ Id
x | Ghc.AnId Id
x <- GhcSrc -> [TyThing]
_gsTyThings GhcSrc
src ]
  ]
  where
    key :: String -> Int -> Ghc.Var -> (Int, F.Symbol, Ghc.Var)
    key :: String -> Int -> Id -> (Int, Symbol, Id)
key String
_ Int
i Id
x  = (Int
i, Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
x, {- dump s -} Id
x)
    _dump :: String -> Id -> Id
_dump String
msg Id
x = (Id, SpecType) -> Id
forall a b. (a, b) -> a
fst ((Id, SpecType) -> Id)
-> ((Id, SpecType) -> (Id, SpecType)) -> (Id, SpecType) -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> (Id, SpecType) -> (Id, SpecType)
forall a. PPrint a => String -> a -> a
myTracepp String
msg ((Id, SpecType) -> Id) -> (Id, SpecType) -> Id
forall a b. (a -> b) -> a -> b
$ (Id
x, Type -> SpecType
forall r. Monoid r => Type -> RRType r
RT.ofType (Type -> Type
Ghc.expandTypeSynonyms (Id -> Type
Ghc.varType Id
x)) :: SpecType)

dataConVars :: [Ghc.DataCon] -> [Ghc.Var]
dataConVars :: [DataCon] -> [Id]
dataConVars [DataCon]
dcs = (DataCon -> Id
Ghc.dataConWorkId (DataCon -> Id) -> [DataCon] -> [Id]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataCon]
dcs) [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ (DataCon -> Id
Ghc.dataConWrapId (DataCon -> Id) -> [DataCon] -> [Id]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataCon]
dcs)

-------------------------------------------------------------------------------
-- | 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 = Env -> ModName -> SourcePos -> [Symbol] -> a -> a
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l []

qualifyTopDummy :: (Qualify a) => Env -> ModName -> a -> a
qualifyTopDummy :: forall a. Qualify a => Env -> ModName -> a -> a
qualifyTopDummy Env
env ModName
name = Env -> ModName -> SourcePos -> a -> a
forall a. Qualify a => Env -> ModName -> SourcePos -> a -> a
qualifyTop Env
env ModName
name SourcePos
dummySourcePos

dummySourcePos :: F.SourcePos
dummySourcePos :: SourcePos
dummySourcePos = Located () -> SourcePos
forall a. Located a -> SourcePos
F.loc (() -> Located ()
forall a. a -> Located a
F.dummyLoc ())

class Qualify a where
  qualify :: Env -> ModName -> F.SourcePos -> [F.Symbol] -> a -> a

instance Qualify TyConMap where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConMap -> TyConMap
qualify Env
env ModName
name SourcePos
l [Symbol]
bs TyConMap
tyi = TyConMap
tyi
    { tcmTyRTy = tx <$> tcmTyRTy tyi
    , tcmFIRTy = tx <$> tcmFIRTy tyi
    }
    where
      tx :: (Qualify a) => a -> a
      tx :: forall a. Qualify a => a -> a
tx = Env -> ModName -> SourcePos -> [Symbol] -> a -> a
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs

instance Qualify TyConP where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConP -> TyConP
qualify Env
env ModName
name SourcePos
_ [Symbol]
bs TyConP
tcp = TyConP
tcp { tcpSizeFun = qualify env name (tcpLoc tcp) bs <$> tcpSizeFun tcp }

instance Qualify SizeFun where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> SizeFun -> SizeFun
qualify Env
env ModName
name SourcePos
_ [Symbol]
bs (SymSizeFun LocSymbol
lx) = LocSymbol -> SizeFun
SymSizeFun (Env -> ModName -> SourcePos -> [Symbol] -> LocSymbol -> LocSymbol
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name (LocSymbol -> SourcePos
forall a. Located a -> SourcePos
F.loc LocSymbol
lx) [Symbol]
bs LocSymbol
lx)
  qualify Env
_   ModName
_    SourcePos
_ [Symbol]
_  SizeFun
sf              = SizeFun
sf

instance Qualify F.Equation where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Equation -> Equation
qualify Env
_env ModName
_name SourcePos
_l [Symbol]
_bs Equation
x = Equation
x -- 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 Env -> ModName -> String -> LocSymbol -> Lookup Symbol
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
"Symbol" (SourcePos -> SourcePos -> Symbol -> LocSymbol
forall a. SourcePos -> SourcePos -> a -> Located a
F.Loc SourcePos
l SourcePos
l Symbol
x) of
                  Left [Error]
_ -> Symbol
x
                  Right Symbol
v -> Symbol
v
  where
    isSpl :: Bool
isSpl     = Env -> [Symbol] -> Symbol -> Bool
isSplSymbol Env
env [Symbol]
bs Symbol
x

isSplSymbol :: Env -> [F.Symbol] -> F.Symbol -> Bool
isSplSymbol :: Env -> [Symbol] -> Symbol -> Bool
isSplSymbol Env
env [Symbol]
bs Symbol
x
  =  Symbol -> Bool
isWiredInName Symbol
x
  Bool -> Bool -> Bool
|| Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Symbol
x [Symbol]
bs
  Bool -> Bool -> Bool
|| Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
x (Env -> HashSet Symbol
reGlobSyms Env
env)

instance (Qualify a) => Qualify (Located a) where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Located a -> Located a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs = (a -> a) -> Located a -> Located a
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> ModName -> SourcePos -> [Symbol] -> a -> a
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs)

instance (Qualify a) => Qualify [a] where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> [a] -> [a]
qualify Env
env ModName
name SourcePos
l [Symbol]
bs = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> ModName -> SourcePos -> [Symbol] -> a -> a
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs)

instance (Qualify a) => Qualify (Maybe a) where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Maybe a -> Maybe a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs = (a -> a) -> Maybe a -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> ModName -> SourcePos -> [Symbol] -> a -> a
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs)

instance Qualify Body where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Body -> Body
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (P   Expr
p) = Expr -> Body
P   (Env -> ModName -> SourcePos -> [Symbol] -> Expr -> Expr
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs Expr
p)
  qualify Env
env ModName
name SourcePos
l [Symbol]
bs (E   Expr
e) = Expr -> Body
E   (Env -> ModName -> SourcePos -> [Symbol] -> Expr -> Expr
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs Expr
e)
  qualify Env
env ModName
name SourcePos
l [Symbol]
bs (R Symbol
x Expr
p) = Symbol -> Expr -> Body
R Symbol
x (Env -> ModName -> SourcePos -> [Symbol] -> Expr -> Expr
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs Expr
p)

instance Qualify TyConInfo where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> TyConInfo -> TyConInfo
qualify Env
env ModName
name SourcePos
l [Symbol]
bs TyConInfo
tci = TyConInfo
tci { sizeFunction = qualify env name l bs <$> sizeFunction tci }

instance Qualify RTyCon where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> RTyCon -> RTyCon
qualify Env
env ModName
name SourcePos
l [Symbol]
bs RTyCon
rtc = RTyCon
rtc { rtc_info = qualify env name l bs (rtc_info rtc) }

instance Qualify (Measure SpecType Ghc.DataCon) where
  qualify :: Env
-> ModName
-> SourcePos
-> [Symbol]
-> Measure SpecType DataCon
-> Measure SpecType DataCon
qualify Env
env ModName
name SourcePos
_ [Symbol]
bs Measure SpecType DataCon
m = Measure SpecType DataCon
m -- FIXME substEnv env name bs $
    { msName = qualify env name l bs     lname
    , msEqns = qualify env name l bs <$> msEqns m
    }
    where
      l :: SourcePos
l      = LocSymbol -> SourcePos
forall a. Located a -> SourcePos
F.loc  LocSymbol
lname
      lname :: LocSymbol
lname  = Measure SpecType DataCon -> LocSymbol
forall ty ctor. Measure ty ctor -> LocSymbol
msName Measure SpecType DataCon
m


instance Qualify (Def ty ctor) where
  qualify :: Env
-> ModName -> SourcePos -> [Symbol] -> Def ty ctor -> Def ty ctor
qualify Env
env ModName
name SourcePos
l [Symbol]
bs Def ty ctor
d = Def ty ctor
d
    { body  = qualify env name l (bs ++ bs') (body d) }
    where
      bs' :: [Symbol]
bs'   = (Symbol, Maybe ty) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Maybe ty) -> Symbol) -> [(Symbol, Maybe ty)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Def ty ctor -> [(Symbol, Maybe ty)]
forall ty ctor. Def ty ctor -> [(Symbol, Maybe ty)]
binds Def ty ctor
d

instance Qualify BareMeasure where
  qualify :: Env
-> ModName
-> SourcePos
-> [Symbol]
-> Measure LocBareType LocSymbol
-> Measure LocBareType LocSymbol
qualify Env
env ModName
name SourcePos
l [Symbol]
bs Measure LocBareType LocSymbol
m = Measure LocBareType LocSymbol
m
    { msEqns = qualify env name l bs (msEqns m)
    }

instance Qualify DataCtor where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> DataCtor -> DataCtor
qualify Env
env ModName
name SourcePos
l [Symbol]
bs DataCtor
c = DataCtor
c
    { dcTheta  = qualify env name l bs (dcTheta  c)
    , dcFields = qualify env name l bs (dcFields c)
    , dcResult = qualify env name l bs (dcResult c)
    }

instance Qualify DataDecl where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> DataDecl -> DataDecl
qualify Env
env ModName
name SourcePos
l [Symbol]
bs DataDecl
d = DataDecl
d
    { tycDCons  = qualify env name l bs (tycDCons  d)
    , tycPropTy = qualify env name l bs (tycPropTy d)
    }

instance Qualify ModSpecs where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs
qualify Env
env ModName
name SourcePos
l [Symbol]
bs = (ModName -> BareSpec -> BareSpec) -> ModSpecs -> ModSpecs
forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
Misc.hashMapMapWithKey (\ModName
_ -> Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs)

instance Qualify b => Qualify (a, b) where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> (a, b) -> (a, b)
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (a
x, b
y) = (a
x, Env -> ModName -> SourcePos -> [Symbol] -> b -> b
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs b
y)

instance Qualify BareSpec where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec
qualify = Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec
qualifyBareSpec

qualifyBareSpec :: Env -> ModName -> F.SourcePos -> [F.Symbol] -> BareSpec -> BareSpec
qualifyBareSpec :: Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec
qualifyBareSpec Env
env ModName
name SourcePos
l [Symbol]
bs BareSpec
sp = BareSpec
sp
  { measures   = qualify env name l bs (measures   sp)
  , asmSigs    = qualify env name l bs (asmSigs    sp)
  , sigs       = qualify env name l bs (sigs       sp)
  , localSigs  = qualify env name l bs (localSigs  sp)
  , reflSigs   = qualify env name l bs (reflSigs   sp)
  , dataDecls  = qualify env name l bs (dataDecls  sp)
  , newtyDecls = qualify env name l bs (newtyDecls sp)
  , ialiases   = [ (f x, f y) | (x, y) <- ialiases sp ]
  }
  where f :: LocBareType -> LocBareType
f      = Env
-> ModName -> SourcePos -> [Symbol] -> LocBareType -> LocBareType
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs

instance Qualify a => Qualify (RTAlias F.Symbol a) where
  qualify :: Env
-> ModName
-> SourcePos
-> [Symbol]
-> RTAlias Symbol a
-> RTAlias Symbol a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs RTAlias Symbol a
rtAlias
   = RTAlias Symbol a
rtAlias { rtName  = qualify env name l bs (rtName rtAlias)
             , rtTArgs = qualify env name l bs (rtTArgs rtAlias)
             , rtVArgs = qualify env name l bs (rtVArgs rtAlias)
             , rtBody  = qualify env name l bs (rtBody rtAlias)
             }

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

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

instance Qualify F.Qualifier where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> Qualifier -> Qualifier
qualify Env
env ModName
name SourcePos
_ [Symbol]
bs Qualifier
q = Qualifier
q { F.qBody = qualify env name (F.qPos q) bs' (F.qBody q) }
    where
      bs' :: [Symbol]
bs'                 = [Symbol]
bs [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (QualParam -> Symbol
F.qpSym (QualParam -> Symbol) -> [QualParam] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Qualifier -> [QualParam]
F.qParams Qualifier
q)

substEnv :: (F.Subable a) => Env -> ModName -> F.SourcePos -> [F.Symbol] -> a -> a
substEnv :: forall a.
Subable a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
substEnv Env
env ModName
name SourcePos
l [Symbol]
bs = (Symbol -> Symbol) -> a -> a
forall a. Subable a => (Symbol -> Symbol) -> a -> a
F.substa (Env -> ModName -> SourcePos -> [Symbol] -> Symbol -> Symbol
qualifySymbol Env
env ModName
name SourcePos
l [Symbol]
bs)

instance Qualify SpecType where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> SpecType -> SpecType
qualify Env
x1 ModName
x2 SourcePos
x3 [Symbol]
x4 SpecType
x5 = ([Symbol] -> RReft -> RReft) -> [Symbol] -> SpecType -> SpecType
forall r1 r2 c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RType c tv r1 -> RType c tv r2
emapReft (Env -> ModName -> SourcePos -> [Symbol] -> RReft -> RReft
forall a.
Subable a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
substFreeEnv Env
x1 ModName
x2 SourcePos
x3) [Symbol]
x4 SpecType
x5

instance Qualify BareType where
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareType -> BareType
qualify Env
x1 ModName
x2 SourcePos
x3 [Symbol]
x4 BareType
x5 = ([Symbol] -> RReft -> RReft) -> [Symbol] -> BareType -> BareType
forall r1 r2 c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RType c tv r1 -> RType c tv r2
emapReft (Env -> ModName -> SourcePos -> [Symbol] -> RReft -> RReft
forall a.
Subable a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
substFreeEnv Env
x1 ModName
x2 SourcePos
x3) [Symbol]
x4 BareType
x5

substFreeEnv :: (F.Subable a) => Env -> ModName -> F.SourcePos -> [F.Symbol] -> a -> a
substFreeEnv :: forall a.
Subable a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
substFreeEnv Env
env ModName
name SourcePos
l [Symbol]
bs = (Symbol -> Expr) -> a -> a
forall a. Subable a => (Symbol -> Expr) -> a -> a
F.substf (Symbol -> Expr
F.EVar (Symbol -> Expr) -> (Symbol -> Symbol) -> Symbol -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ModName -> SourcePos -> [Symbol] -> Symbol -> Symbol
qualifySymbol Env
env ModName
name SourcePos
l [Symbol]
bs)

-------------------------------------------------------------------------------
lookupGhcNamedVar :: (Ghc.NamedThing a, F.Symbolic a) => Env -> ModName -> a -> Maybe Ghc.Var
-------------------------------------------------------------------------------
lookupGhcNamedVar :: forall a.
(NamedThing a, Symbolic a) =>
Env -> ModName -> a -> Maybe Id
lookupGhcNamedVar Env
env ModName
name a
z = Env -> ModName -> String -> LocSymbol -> Maybe Id
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Maybe a
maybeResolveSym  Env
env ModName
name String
"Var" LocSymbol
lx
  where
    lx :: LocSymbol
lx                       = a -> LocSymbol
forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol a
z

lookupGhcVar :: Env -> ModName -> String -> LocSymbol -> Lookup Ghc.Var
lookupGhcVar :: Env -> ModName -> String -> LocSymbol -> Lookup Id
lookupGhcVar Env
env ModName
name String
kind LocSymbol
lx = case Env -> ModName -> String -> LocSymbol -> Lookup Id
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
kind LocSymbol
lx of
    Right Id
v -> Lookup Id -> (Id -> Lookup Id) -> Maybe Id -> Lookup Id
forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe (Id -> Lookup Id
forall a b. b -> Either a b
Right Id
v) Id -> Lookup Id
forall a b. b -> Either a b
Right (Env -> LocSymbol -> [Id] -> Maybe Id
lookupLocalVar Env
env LocSymbol
lx [Id
v])
    Left  [Error]
e -> Lookup Id -> (Id -> Lookup Id) -> Maybe Id -> Lookup Id
forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe ([Error] -> Lookup Id
forall a b. a -> Either a b
Left  [Error]
e) Id -> Lookup Id
forall a b. b -> Either a b
Right (Env -> LocSymbol -> [Id] -> Maybe Id
lookupLocalVar Env
env LocSymbol
lx [])

  -- 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 = Int -> [(Int, Id)] -> Maybe Id
forall i a. (Ord i, Num i) => i -> [(i, a)] -> Maybe a
Misc.findNearest Int
lxn [(Int, Id)]
kvs
  where
    _msg :: String
_msg                  = String
"LOOKUP-LOCAL: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Symbol, Int, [(Int, Id)]) -> String
forall a. PPrint a => a -> String
F.showpp (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lx, Int
lxn, [(Int, Id)]
kvs)
    kvs :: [(Int, Id)]
kvs                   = [(Int, Id)]
gs [(Int, Id)] -> [(Int, Id)] -> [(Int, Id)]
forall a. [a] -> [a] -> [a]
++ [(Int, Id)] -> Symbol -> LocalVars -> [(Int, Id)]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] Symbol
x (Env -> LocalVars
reLocalVars Env
env)
    gs :: [(Int, Id)]
gs                    = [(Pos -> Int
F.unPos (Id -> Pos
forall a. Loc a => a -> Pos
F.srcLine Id
v), Id
v) | Id
v <- [Id]
gvs]
    lxn :: Int
lxn                   = Pos -> Int
F.unPos (LocSymbol -> Pos
forall a. Loc a => a -> Pos
F.srcLine LocSymbol
lx)
    (Maybe Symbol
_, Symbol
x)                = Symbol -> (Maybe Symbol, Symbol)
unQualifySymbol (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lx)

lookupGhcDataCon :: Env -> ModName -> String -> LocSymbol -> Lookup Ghc.DataCon
lookupGhcDataCon :: Env -> ModName -> String -> LocSymbol -> Lookup DataCon
lookupGhcDataCon = Env -> ModName -> String -> LocSymbol -> Lookup DataCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym -- 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 = String -> Lookup TyCon -> Lookup TyCon
forall a. PPrint a => String -> a -> a
myTracepp (String
"LOOKUP-TYCON: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. PPrint a => a -> String
F.showpp (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
lx))
                               (Lookup TyCon -> Lookup TyCon) -> Lookup TyCon -> Lookup TyCon
forall a b. (a -> b) -> a -> b
$ {- strictResolveSym -} Env -> ModName -> String -> LocSymbol -> Lookup TyCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
k LocSymbol
lx

lookupGhcDnTyCon :: Env -> ModName -> String -> DataName -> Lookup (Maybe Ghc.TyCon)
-- lookupGhcDnTyCon = lookupGhcDnTyConE
lookupGhcDnTyCon :: Env -> ModName -> String -> DataName -> Lookup (Maybe TyCon)
lookupGhcDnTyCon Env
env ModName
name String
msg = Env -> ModName -> Lookup TyCon -> Lookup (Maybe TyCon)
forall e r. Env -> ModName -> Either e r -> Either e (Maybe r)
failMaybe Env
env ModName
name (Lookup TyCon -> Lookup (Maybe TyCon))
-> (DataName -> Lookup TyCon) -> DataName -> Lookup (Maybe TyCon)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ModName -> String -> DataName -> Lookup TyCon
lookupGhcDnTyConE Env
env ModName
name String
msg

lookupGhcDnTyConE :: Env -> ModName -> String -> DataName -> Lookup Ghc.TyCon
lookupGhcDnTyConE :: Env -> ModName -> String -> DataName -> Lookup TyCon
lookupGhcDnTyConE Env
env ModName
name String
msg (DnCon  LocSymbol
s)
  = Env -> ModName -> String -> LocSymbol -> Lookup TyCon
lookupGhcDnCon Env
env ModName
name String
msg LocSymbol
s
lookupGhcDnTyConE Env
env ModName
name String
msg (DnName LocSymbol
s)
  = case Env -> ModName -> String -> LocSymbol -> Lookup TyCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
msg LocSymbol
s of
      Right TyCon
r -> TyCon -> Lookup TyCon
forall a b. b -> Either a b
Right TyCon
r
      Left  [Error]
e -> case Env -> ModName -> String -> LocSymbol -> Lookup TyCon
lookupGhcDnCon  Env
env ModName
name String
msg LocSymbol
s of
                   Right TyCon
r -> TyCon -> Lookup TyCon
forall a b. b -> Either a b
Right TyCon
r
                   Left  [Error]
_ -> [Error] -> Lookup TyCon
forall a b. a -> Either a b
Left  [Error]
e


lookupGhcDnCon :: Env -> ModName -> String -> LocSymbol -> Lookup Ghc.TyCon
lookupGhcDnCon :: Env -> ModName -> String -> LocSymbol -> Lookup TyCon
lookupGhcDnCon Env
env ModName
name String
msg = (DataCon -> TyCon) -> Lookup DataCon -> Lookup TyCon
forall a b. (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataCon -> TyCon
Ghc.dataConTyCon (Lookup DataCon -> Lookup TyCon)
-> (LocSymbol -> Lookup DataCon) -> LocSymbol -> Lookup TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ModName -> String -> LocSymbol -> Lookup DataCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
msg

-------------------------------------------------------------------------------
-- | 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 Maybe [PVar BSort]
forall a. Maybe a
Nothing BareType
t of
    Left [Error]
e  -> String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
myTracepp (String
"knownType: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (BareType, [Error]) -> String
forall a. PPrint a => a -> String
F.showpp (BareType
t, [Error]
e)) Bool
False
    Right SpecType
_ -> Bool
True



_rTypeTyCons :: (Ord c) => RType c tv r -> [c]
_rTypeTyCons :: forall c tv r. Ord c => RType c tv r -> [c]
_rTypeTyCons        = [c] -> [c]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([c] -> [c]) -> (RType c tv r -> [c]) -> RType c tv r -> [c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([c] -> RType c tv r -> [c]) -> [c] -> RType c tv r -> [c]
forall acc c tv r.
(acc -> RType c tv r -> acc) -> acc -> RType c tv r -> acc
foldRType [c] -> RType c tv r -> [c]
forall {a} {tv} {r}. [a] -> RType a tv r -> [a]
f []
  where
    f :: [a] -> RType a tv r -> [a]
f [a]
acc t :: RType a tv r
t@RApp {} = RType a tv r -> a
forall c tv r. RType c tv r -> c
rt_tycon RType a tv r
t a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
acc
    f [a]
acc RType a tv r
_         = [a]
acc

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

knownGhcTyCon :: Env -> ModName -> LocSymbol -> Bool
knownGhcTyCon :: Env -> ModName -> LocSymbol -> Bool
knownGhcTyCon Env
env ModName
name LocSymbol
lx = String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
myTracepp  String
msg (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Maybe TyCon -> Bool
forall a. Maybe a -> Bool
Mb.isJust Maybe TyCon
v
  where
    msg :: String
msg = String
"knownGhcTyCon: "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ LocSymbol -> String
forall a. PPrint a => a -> String
F.showpp LocSymbol
lx
    v :: Maybe Ghc.TyCon -- This annotation is crucial
    v :: Maybe TyCon
v = Env -> ModName -> String -> LocSymbol -> Maybe TyCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Maybe a
maybeResolveSym Env
env ModName
name String
"known-tycon" LocSymbol
lx

knownGhcDataCon :: Env -> ModName -> LocSymbol -> Bool
knownGhcDataCon :: Env -> ModName -> LocSymbol -> Bool
knownGhcDataCon Env
env ModName
name LocSymbol
lx = Maybe DataCon -> Bool
forall a. Maybe a -> Bool
Mb.isJust Maybe DataCon
v
  where
    v :: Maybe Ghc.DataCon -- This annotation is crucial
    v :: Maybe DataCon
v = String -> Maybe DataCon -> Maybe DataCon
forall a. PPrint a => String -> a -> a
myTracepp (String
"knownGhcDataCon" String -> String -> String
forall a. [a] -> [a] -> [a]
++ LocSymbol -> String
forall a. PPrint a => a -> String
F.showpp LocSymbol
lx)
      (Maybe DataCon -> Maybe DataCon) -> Maybe DataCon -> Maybe DataCon
forall a b. (a -> b) -> a -> b
$ Env -> ModName -> String -> LocSymbol -> Maybe DataCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Maybe a
maybeResolveSym Env
env ModName
name String
"known-datacon" LocSymbol
lx

-------------------------------------------------------------------------------
-- | 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 = Doc
-> (TyThing -> Maybe Id)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup Id
forall a.
PPrint a =>
Doc
-> (TyThing -> Maybe a)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup a
resolveWith Doc
"variable" ((TyThing -> Maybe Id)
 -> Env -> ModName -> String -> LocSymbol -> Lookup Id)
-> (TyThing -> Maybe Id)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup Id
forall a b. (a -> b) -> a -> b
$ \case
                    Ghc.AnId Id
x -> Id -> Maybe Id
forall a. a -> Maybe a
Just Id
x
                    TyThing
_          -> Maybe Id
forall a. Maybe a
Nothing

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

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


{- 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 -> Lookup 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 =  Env -> ModName -> String -> LocSymbol -> Lookup Id
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
"Var" LocSymbol
lx
                 Lookup Id -> Lookup Id -> Lookup Id
forall a. Semigroup a => a -> a -> a
<> Doc
-> (TyThing -> Maybe Id)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup Id
forall a.
PPrint a =>
Doc
-> (TyThing -> Maybe a)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup a
resolveWith Doc
"variable" TyThing -> Maybe Id
lookupVarInsideRealDataCon Env
env ModName
name String
"Var" LocSymbol
lx
    in case Lookup Id
resolved of
      Left [Error]
_               -> Symbol -> Lookup Symbol
forall a b. b -> Either a b
Right (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
lx)
      Right (Id
v :: Ghc.Var) -> Symbol -> Lookup Symbol
forall a b. b -> Either a b
Right (Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
v)
    where
      lookupVarInsideRealDataCon :: Ghc.TyThing -> Maybe Ghc.Var
      lookupVarInsideRealDataCon :: TyThing -> Maybe Id
lookupVarInsideRealDataCon = \case
        Ghc.AConLike (Ghc.RealDataCon DataCon
x) -> Id -> Maybe Id
forall a. a -> Maybe a
Just (DataCon -> Id
Ghc.dataConWorkId DataCon
x)
        TyThing
_                                -> Maybe Id
forall a. Maybe a
Nothing



resolveWith :: (PPrint a) => PJ.Doc -> (Ghc.TyThing -> Maybe a) -> Env -> ModName -> String -> LocSymbol
            -> Lookup a
resolveWith :: forall a.
PPrint a =>
Doc
-> (TyThing -> Maybe a)
-> Env
-> ModName
-> String
-> LocSymbol
-> Lookup a
resolveWith Doc
kind TyThing -> Maybe a
f Env
env ModName
name String
str LocSymbol
lx =
  -- case Mb.mapMaybe f things of
  case (TyThing -> Maybe a) -> [((Int, Symbol), TyThing)] -> [a]
forall k a b. EqHash k => (a -> Maybe b) -> [(k, a)] -> [b]
rankedThings TyThing -> Maybe a
f [((Int, Symbol), TyThing)]
things of
    []  -> [Error] -> Lookup a
forall a b. a -> Either a b
Left [Doc -> String -> LocSymbol -> Error
errResolve Doc
kind String
str LocSymbol
lx]
    [a
x] -> a -> Lookup a
forall a b. b -> Either a b
Right a
x
    [a]
xs  -> [Error] -> Lookup a
forall a b. a -> Either a b
Left [SrcSpan -> Doc -> [Doc] -> Error
forall t. SrcSpan -> Doc -> [Doc] -> TError t
ErrDupNames SrcSpan
sp (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lx)) (a -> Doc
forall a. PPrint a => a -> Doc
pprint (a -> Doc) -> [a] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
xs)]
  where
    _xSym :: Symbol
_xSym   = LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lx
    sp :: SrcSpan
sp      = SrcSpan -> SrcSpan
GM.fSrcSpanSrcSpan (LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan LocSymbol
lx)
    things :: [((Int, Symbol), TyThing)]
things  = String -> [((Int, Symbol), TyThing)] -> [((Int, Symbol), TyThing)]
forall a. PPrint a => String -> a -> a
myTracepp String
msg ([((Int, Symbol), TyThing)] -> [((Int, Symbol), TyThing)])
-> [((Int, Symbol), TyThing)] -> [((Int, Symbol), TyThing)]
forall a b. (a -> b) -> a -> b
$ Env -> ModName -> LocSymbol -> [((Int, Symbol), TyThing)]
lookupTyThing Env
env ModName
name LocSymbol
lx
    msg :: String
msg     = String
"resolveWith: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. PPrint a => a -> String
F.showpp (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
lx)


rankedThings :: (Misc.EqHash k) => (a -> Maybe b) -> [(k, a)] -> [b]
rankedThings :: forall k a b. EqHash k => (a -> Maybe b) -> [(k, a)] -> [b]
rankedThings a -> Maybe b
f [(k, a)]
ias = case ((k, [b]) -> k) -> [(k, [b])] -> [(k, [b])]
forall b a. Ord b => (a -> b) -> [a] -> [a]
Misc.sortOn (k, [b]) -> k
forall a b. (a, b) -> a
fst ([(k, b)] -> [(k, [b])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(k, b)]
ibs) of
                       (k
_,[b]
ts):[(k, [b])]
_ -> [b]
ts
                       []       -> []
  where
    ibs :: [(k, b)]
ibs            = ((k, a) -> Maybe (k, b)) -> [(k, a)] -> [(k, b)]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (\(k
k, a
x) -> (k
k,) (b -> (k, b)) -> Maybe b -> Maybe (k, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe b
f a
x) [(k, a)]
ias

-------------------------------------------------------------------------------
-- | @lookupTyThing@ 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             = (((Int, Symbol), [TyThing]) -> (Int, Symbol))
-> [((Int, Symbol), [TyThing])] -> [((Int, Symbol), [TyThing])]
forall b a. Ord b => (a -> b) -> [a] -> [a]
Misc.sortOn ((Int, Symbol), [TyThing]) -> (Int, Symbol)
forall a b. (a, b) -> a
fst ([((Int, Symbol), TyThing)] -> [((Int, Symbol), [TyThing])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [((Int, Symbol), TyThing)]
matches)
    matches :: [((Int, Symbol), TyThing)]
matches                = String -> [((Int, Symbol), TyThing)] -> [((Int, Symbol), TyThing)]
forall a. PPrint a => String -> a -> a
myTracepp (String
"matches-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg)
                             [ ((Int
k, Symbol
m), TyThing
t) | (Symbol
m, TyThing
t) <- Env -> Symbol -> [(Symbol, TyThing)]
lookupThings Env
env Symbol
x
                                           , Int
k      <- String -> [Int] -> [Int]
forall a. PPrint a => String -> a -> a
myTracepp String
msg ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol -> Maybe [Symbol] -> [Int]
mm Symbol
nameSym Symbol
m Maybe [Symbol]
mds ]
    msg :: String
msg                    = String
"lookupTyThing: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (LocSymbol, Symbol, Maybe [Symbol]) -> String
forall a. PPrint a => a -> String
F.showpp (LocSymbol
lsym, Symbol
x, Maybe [Symbol]
mds)
    (Symbol
x, Maybe [Symbol]
mds)               = Env -> Symbol -> (Symbol, Maybe [Symbol])
symbolModules Env
env (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lsym)
    nameSym :: Symbol
nameSym                = ModName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ModName
mdname
    mm :: Symbol -> Symbol -> Maybe [Symbol] -> [Int]
mm Symbol
name Symbol
m Maybe [Symbol]
mods         = String -> [Int] -> [Int]
forall a. PPrint a => String -> a -> a
myTracepp (String
"matchMod: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (LocSymbol, Symbol, Symbol, Maybe [Symbol]) -> String
forall a. PPrint a => a -> String
F.showpp (LocSymbol
lsym, Symbol
name, Symbol
m, Maybe [Symbol]
mods)) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$
                               Env -> Symbol -> Symbol -> Maybe [Symbol] -> [Int]
matchMod Env
env Symbol
name Symbol
m Maybe [Symbol]
mods

lookupThings :: Env -> F.Symbol -> [(F.Symbol, Ghc.TyThing)]
lookupThings :: Env -> Symbol -> [(Symbol, TyThing)]
lookupThings Env
env Symbol
x = String -> [(Symbol, TyThing)] -> [(Symbol, TyThing)]
forall a. PPrint a => String -> a -> a
myTracepp (String
"lookupThings: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. PPrint a => a -> String
F.showpp Symbol
x)
                   ([(Symbol, TyThing)] -> [(Symbol, TyThing)])
-> [(Symbol, TyThing)] -> [(Symbol, TyThing)]
forall a b. (a -> b) -> a -> b
$ [(Symbol, TyThing)]
-> Maybe [(Symbol, TyThing)] -> [(Symbol, TyThing)]
forall a. a -> Maybe a -> a
Mb.fromMaybe [] (Maybe [(Symbol, TyThing)] -> [(Symbol, TyThing)])
-> Maybe [(Symbol, TyThing)] -> [(Symbol, TyThing)]
forall a b. (a -> b) -> a -> b
$ Symbol -> Maybe [(Symbol, TyThing)]
get Symbol
x Maybe [(Symbol, TyThing)]
-> Maybe [(Symbol, TyThing)] -> Maybe [(Symbol, TyThing)]
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Symbol -> Maybe [(Symbol, TyThing)]
get (Symbol -> Symbol
GM.stripParensSym Symbol
x)
  where
    get :: Symbol -> Maybe [(Symbol, TyThing)]
get Symbol
z          = Symbol -> TyThingMap -> Maybe [(Symbol, TyThing)]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
z (Env -> TyThingMap
_reTyThings Env
env)

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

-- | 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                  =
    [Text] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Text]
parentHierarchy Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Text] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Text]
childHierarchy Bool -> Bool -> Bool
&& ((Text, Text) -> Bool) -> [(Text, Text)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Text -> Text -> Bool) -> (Text, Text) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
(==)) ([Text] -> [Text] -> [(Text, Text)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Text]
parentHierarchy [Text]
childHierarchy)
  where
    parentHierarchy :: [T.Text]
    parentHierarchy :: [Text]
parentHierarchy = HasCallStack => Text -> Text -> [Text]
Text -> Text -> [Text]
T.splitOn Text
"." (Text -> [Text]) -> (Symbol -> Text) -> Symbol -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
F.symbolText (Symbol -> [Text]) -> Symbol -> [Text]
forall a b. (a -> b) -> a -> b
$ Symbol
parentModule

    childHierarchy :: [T.Text]
    childHierarchy :: [Text]
childHierarchy = HasCallStack => Text -> Text -> [Text]
Text -> Text -> [Text]
T.splitOn Text
"." (Text -> [Text]) -> (Symbol -> Text) -> Symbol -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
F.symbolText (Symbol -> [Text]) -> Symbol -> [Text]
forall a b. (a -> b) -> a -> b
$ Symbol
childModule


symbolModules :: Env -> F.Symbol -> (F.Symbol, Maybe [F.Symbol])
symbolModules :: Env -> Symbol -> (Symbol, Maybe [Symbol])
symbolModules Env
env Symbol
s = (Symbol
x, Symbol -> [Symbol]
glerb (Symbol -> [Symbol]) -> Maybe Symbol -> Maybe [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Symbol
modMb)
  where
    (Maybe Symbol
modMb, Symbol
x)      = Symbol -> (Maybe Symbol, Symbol)
unQualifySymbol Symbol
s
    glerb :: Symbol -> [Symbol]
glerb Symbol
m         = [Symbol] -> Symbol -> HashMap Symbol [Symbol] -> [Symbol]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [Symbol
m] Symbol
m HashMap Symbol [Symbol]
qImps
    qImps :: HashMap Symbol [Symbol]
qImps           = QImports -> HashMap Symbol [Symbol]
qiNames (Env -> QImports
reQualImps Env
env)

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


-- | `unQualifySymbol 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 = (Symbol -> Maybe Symbol)
-> (Symbol, Symbol) -> (Maybe Symbol, Symbol)
forall a c b. (a -> c) -> (a, b) -> (c, b)
Misc.mapFst Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just (Symbol -> (Symbol, Symbol)
splitModuleNameExact Symbol
sym)
  | Bool
otherwise             = (Maybe Symbol
forall a. Maybe a
Nothing, Symbol
sym)

splitModuleNameExact :: F.Symbol -> (F.Symbol, F.Symbol)
splitModuleNameExact :: Symbol -> (Symbol, Symbol)
splitModuleNameExact Symbol
x' = String -> (Symbol, Symbol) -> (Symbol, Symbol)
forall a. PPrint a => String -> a -> a
myTracepp (String
"splitModuleNameExact for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. PPrint a => a -> String
F.showpp Symbol
x)
                          (Symbol -> Symbol
GM.takeModuleNames Symbol
x, Symbol -> Symbol
GM.dropModuleNames Symbol
x)
  where
    x :: Symbol
x = Symbol -> Symbol
GM.stripParensSym Symbol
x'

errResolve :: PJ.Doc -> String -> LocSymbol -> Error
errResolve :: Doc -> String -> LocSymbol -> Error
errResolve Doc
k String
msg LocSymbol
lx = SrcSpan -> Doc -> Doc -> Doc -> Error
forall t. SrcSpan -> Doc -> Doc -> Doc -> TError t
ErrResolve (LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSymbol
lx) Doc
k (Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lx)) (String -> Doc
PJ.text String
msg)

-- -- | @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 Env -> ModName -> String -> LocSymbol -> Lookup a
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
kind LocSymbol
x of
  Left  [Error]
_   -> Maybe a
forall a. Maybe a
Nothing
  Right a
val -> a -> Maybe a
forall a. a -> Maybe a
Just a
val

-------------------------------------------------------------------------------
-- | @ofBareType@ 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 = ([Error] -> SpecType)
-> (SpecType -> SpecType) -> Lookup SpecType -> SpecType
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either [Error] -> SpecType
forall {a}. [Error] -> a
fail' SpecType -> SpecType
forall a. a -> a
id (Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> BareType
-> Lookup SpecType
ofBareTypeE Env
env ModName
name SourcePos
l Maybe [PVar BSort]
ps BareType
t)
  where
    fail' :: [Error] -> a
fail'                  = [Error] -> a
forall a e. Exception e => e -> a
Ex.throw
    -- 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 = Env
-> ModName
-> ([Symbol] -> RReft -> RReft)
-> SourcePos
-> BareType
-> Lookup SpecType
forall r.
Expandable r =>
Env
-> ModName
-> ([Symbol] -> r -> r)
-> SourcePos
-> BRType r
-> Lookup (RRType r)
ofBRType Env
env ModName
name (Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> BareType
-> [Symbol]
-> RReft
-> RReft
resolveReft Env
env ModName
name SourcePos
l Maybe [PVar BSort]
ps BareType
t) SourcePos
l BareType
t

resolveReft :: Env -> ModName -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> [F.Symbol] -> RReft -> RReft
resolveReft :: Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> BareType
-> [Symbol]
-> RReft
-> RReft
resolveReft Env
env ModName
name SourcePos
l Maybe [PVar BSort]
ps BareType
t [Symbol]
bs
        = Env -> ModName -> SourcePos -> [Symbol] -> RReft -> RReft
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs
        (RReft -> RReft) -> (RReft -> RReft) -> RReft -> RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourcePos
-> ((UsedPVar -> UsedPVar) -> RReft -> RReft)
-> [UsedPVar]
-> BareType
-> RReft
-> RReft
forall t c tv r.
SourcePos
-> ((UsedPVar -> UsedPVar) -> t) -> [UsedPVar] -> RType c tv r -> t
txParam SourcePos
l (UsedPVar -> UsedPVar) -> RReft -> RReft
RT.subvUReft (PVar BSort -> UsedPVar
forall t. PVar t -> UsedPVar
RT.uPVar (PVar BSort -> UsedPVar) -> [PVar BSort] -> [UsedPVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVar BSort]
πs) BareType
t
        (RReft -> RReft) -> (RReft -> RReft) -> RReft -> RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareType -> RReft -> RReft
fixReftTyVars BareType
t       -- same as fixCoercions
  where
    πs :: [PVar BSort]
πs  = [PVar BSort] -> Maybe [PVar BSort] -> [PVar BSort]
forall a. a -> Maybe a -> a
Mb.fromMaybe [PVar BSort]
tπs Maybe [PVar BSort]
ps
    tπs :: [PVar BSort]
tπs = RTypeRep BTyCon BTyVar RReft -> [PVar BSort]
forall c tv r. RTypeRep c tv r -> [PVar (RType c tv ())]
ty_preds (BareType -> RTypeRep BTyCon BTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep BareType
t)

fixReftTyVars :: BareType -> RReft -> RReft
fixReftTyVars :: BareType -> RReft -> RReft
fixReftTyVars BareType
bt  = CoSub -> RReft -> RReft
coSubRReft CoSub
coSub
  where
    coSub :: CoSub
coSub         = [(Symbol, Sort)] -> CoSub
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (BTyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol BTyVar
a, Symbol -> Sort
F.FObj (BTyVar -> Symbol
specTvSymbol BTyVar
a)) | BTyVar
a <- [BTyVar]
tvs ]
    tvs :: [BTyVar]
tvs           = BareType -> [BTyVar]
forall tv c r. Ord tv => RType c tv r -> [tv]
RT.allTyVars BareType
bt
    specTvSymbol :: BTyVar -> Symbol
specTvSymbol  = RTyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (RTyVar -> Symbol) -> (BTyVar -> RTyVar) -> BTyVar -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BTyVar -> RTyVar
RT.bareRTyVar

coSubRReft :: F.CoSub -> RReft -> RReft
coSubRReft :: CoSub -> RReft -> RReft
coSubRReft CoSub
su RReft
r = RReft
r { ur_reft = coSubReft su (ur_reft r) }

coSubReft :: F.CoSub -> F.Reft -> F.Reft
coSubReft :: CoSub -> Reft -> Reft
coSubReft CoSub
su (F.Reft (Symbol
x, Expr
e)) = (Symbol, Expr) -> Reft
F.Reft (Symbol
x, CoSub -> Expr -> Expr
F.applyCoSub CoSub
su Expr
e)


ofBSort :: Env -> ModName -> F.SourcePos -> BSort -> RSort
ofBSort :: Env -> ModName -> SourcePos -> BSort -> RType RTyCon RTyVar ()
ofBSort Env
env ModName
name SourcePos
l BSort
t = ([Error] -> RType RTyCon RTyVar ())
-> (RType RTyCon RTyVar () -> RType RTyCon RTyVar ())
-> Either [Error] (RType RTyCon RTyVar ())
-> RType RTyCon RTyVar ()
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (String -> String -> RType RTyCon RTyVar ()
forall a. String -> String -> a
Misc.errorP String
"error-ofBSort" (String -> RType RTyCon RTyVar ())
-> ([Error] -> String) -> [Error] -> RType RTyCon RTyVar ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Error] -> String
forall a. PPrint a => a -> String
F.showpp) RType RTyCon RTyVar () -> RType RTyCon RTyVar ()
forall a. a -> a
id (Env
-> ModName
-> SourcePos
-> BSort
-> Either [Error] (RType RTyCon RTyVar ())
ofBSortE Env
env ModName
name SourcePos
l BSort
t)

ofBSortE :: Env -> ModName -> F.SourcePos -> BSort -> Lookup RSort
ofBSortE :: Env
-> ModName
-> SourcePos
-> BSort
-> Either [Error] (RType RTyCon RTyVar ())
ofBSortE Env
env ModName
name SourcePos
l BSort
t = Env
-> ModName
-> ([Symbol] -> () -> ())
-> SourcePos
-> BSort
-> Either [Error] (RType RTyCon RTyVar ())
forall r.
Expandable r =>
Env
-> ModName
-> ([Symbol] -> r -> r)
-> SourcePos
-> BRType r
-> Lookup (RRType r)
ofBRType Env
env ModName
name ((() -> ()) -> [Symbol] -> () -> ()
forall a b. a -> b -> a
const () -> ()
forall a. a -> a
id) SourcePos
l BSort
t

ofBPVar :: Env -> ModName -> F.SourcePos -> BPVar -> RPVar
ofBPVar :: Env -> ModName -> SourcePos -> PVar BSort -> RPVar
ofBPVar Env
env ModName
name SourcePos
l = (BSort -> RType RTyCon RTyVar ()) -> PVar BSort -> RPVar
forall a b. (a -> b) -> PVar a -> PVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> ModName -> SourcePos -> BSort -> RType RTyCon RTyVar ()
ofBSort Env
env ModName
name SourcePos
l)

--------------------------------------------------------------------------------
txParam :: F.SourcePos -> ((UsedPVar -> UsedPVar) -> t) -> [UsedPVar] -> RType c tv r -> t
txParam :: forall t c tv r.
SourcePos
-> ((UsedPVar -> UsedPVar) -> t) -> [UsedPVar] -> RType c tv r -> t
txParam SourcePos
l (UsedPVar -> UsedPVar) -> t
f [UsedPVar]
πs RType c tv r
t = (UsedPVar -> UsedPVar) -> t
f (SourcePos -> HashMap Symbol UsedPVar -> UsedPVar -> UsedPVar
txPvar SourcePos
l ([UsedPVar] -> RType c tv r -> HashMap Symbol UsedPVar
forall c tv r.
[UsedPVar] -> RType c tv r -> HashMap Symbol UsedPVar
predMap [UsedPVar]
πs RType c tv r
t))

txPvar :: F.SourcePos -> M.HashMap F.Symbol UsedPVar -> UsedPVar -> UsedPVar
txPvar :: SourcePos -> HashMap Symbol UsedPVar -> UsedPVar -> UsedPVar
txPvar SourcePos
l HashMap Symbol UsedPVar
m UsedPVar
π = UsedPVar
π { pargs = args' }
  where
    args' :: [((), Symbol, Expr)]
args' | Bool -> Bool
not ([((), Symbol, Expr)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (UsedPVar -> [((), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
π)) = (((), Symbol, Expr) -> ((), Symbol, Expr) -> ((), Symbol, Expr))
-> [((), Symbol, Expr)]
-> [((), Symbol, Expr)]
-> [((), Symbol, Expr)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(()
_,Symbol
x ,Expr
_) (()
t,Symbol
_,Expr
y) -> (()
t, Symbol
x, Expr
y)) (UsedPVar -> [((), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
π') (UsedPVar -> [((), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
π)
          | Bool
otherwise            = UsedPVar -> [((), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
π'
    π' :: UsedPVar
π'    = UsedPVar -> Maybe UsedPVar -> UsedPVar
forall a. a -> Maybe a -> a
Mb.fromMaybe UsedPVar
forall {a}. a
err (Maybe UsedPVar -> UsedPVar) -> Maybe UsedPVar -> UsedPVar
forall a b. (a -> b) -> a -> b
$ Symbol -> HashMap Symbol UsedPVar -> Maybe UsedPVar
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (UsedPVar -> Symbol
forall t. PVar t -> Symbol
pname UsedPVar
π) HashMap Symbol UsedPVar
m
    err :: a
err   = UserError -> a
forall a. UserError -> a
uError (UserError -> a) -> UserError -> a
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> UserError
forall t. SrcSpan -> Doc -> TError t
ErrUnbPred SrcSpan
sp (UsedPVar -> Doc
forall a. PPrint a => a -> Doc
pprint UsedPVar
π)
    sp :: SrcSpan
sp    = SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l

predMap :: [UsedPVar] -> RType c tv r -> M.HashMap F.Symbol UsedPVar
predMap :: forall c tv r.
[UsedPVar] -> RType c tv r -> HashMap Symbol UsedPVar
predMap [UsedPVar]
πs RType c tv r
t = [(Symbol, UsedPVar)] -> HashMap Symbol UsedPVar
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(UsedPVar -> Symbol
forall t. PVar t -> Symbol
pname UsedPVar
π, UsedPVar
π) | UsedPVar
π <- [UsedPVar]
πs [UsedPVar] -> [UsedPVar] -> [UsedPVar]
forall a. [a] -> [a] -> [a]
++ RType c tv r -> [UsedPVar]
forall c tv r. RType c tv r -> [UsedPVar]
rtypePredBinds RType c tv r
t]

rtypePredBinds :: RType c tv r -> [UsedPVar]
rtypePredBinds :: forall c tv r. RType c tv r -> [UsedPVar]
rtypePredBinds = (PVar (RType c tv ()) -> UsedPVar)
-> [PVar (RType c tv ())] -> [UsedPVar]
forall a b. (a -> b) -> [a] -> [b]
map PVar (RType c tv ()) -> UsedPVar
forall t. PVar t -> UsedPVar
RT.uPVar ([PVar (RType c tv ())] -> [UsedPVar])
-> (RType c tv r -> [PVar (RType c tv ())])
-> RType c tv r
-> [UsedPVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeRep c tv r -> [PVar (RType c tv ())]
forall c tv r. RTypeRep c tv r -> [PVar (RType c tv ())]
ty_preds (RTypeRep c tv r -> [PVar (RType c tv ())])
-> (RType c tv r -> RTypeRep c tv r)
-> RType c tv r
-> [PVar (RType c tv ())]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType c tv r -> RTypeRep c tv r
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep



--------------------------------------------------------------------------------
type Expandable r = ( PPrint r
                    , F.Reftable r
                    , SubsTy RTyVar (RType RTyCon RTyVar ()) r
                    , F.Reftable (RTProp RTyCon RTyVar r))

ofBRType :: (Expandable r) => Env -> ModName -> ([F.Symbol] -> r -> r) -> F.SourcePos -> BRType r
         -> Lookup (RRType r)
ofBRType :: forall r.
Expandable r =>
Env
-> ModName
-> ([Symbol] -> r -> r)
-> SourcePos
-> BRType r
-> Lookup (RRType r)
ofBRType Env
env ModName
name [Symbol] -> r -> r
f SourcePos
l = [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go []
  where
    goReft :: [Symbol] -> r -> m r
goReft [Symbol]
bs r
r             = r -> m r
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Symbol] -> r -> r
f [Symbol]
bs r
r)
    goRFun :: [Symbol]
-> Symbol
-> RFInfo
-> RType BTyCon BTyVar r
-> RType BTyCon BTyVar r
-> r
-> Either [Error] (RType RTyCon RTyVar r)
goRFun [Symbol]
bs Symbol
x RFInfo
i RType BTyCon BTyVar r
t1 RType BTyCon BTyVar r
t2 r
r  = Symbol
-> RFInfo
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> r
-> RType RTyCon RTyVar r
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i{permitTC = Just (typeclass (getConfig env))} (RType RTyCon RTyVar r
 -> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either
     [Error] (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Symbol -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall {r} {c} {tv}.
(Reftable r, TyConable c) =>
Symbol -> RType c tv r -> RType c tv r
rebind Symbol
x (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t1) Either
  [Error] (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (r -> RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
bs) RType BTyCon BTyVar r
t2 Either [Error] (r -> RType RTyCon RTyVar r)
-> Either [Error] r -> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
    rebind :: Symbol -> RType c tv r -> RType c tv r
rebind Symbol
x RType c tv r
t              = RType c tv r -> (Symbol, Expr) -> RType c tv r
forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 RType c tv r
t (Symbol
x, Symbol -> Expr
F.EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ RType c tv r -> Symbol
forall r c tv. Reftable r => RType c tv r -> Symbol
rTypeValueVar RType c tv r
t)
    go :: [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs (RAppTy RType BTyCon BTyVar r
t1 RType BTyCon BTyVar r
t2 r
r)  = RType RTyCon RTyVar r
-> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy (RType RTyCon RTyVar r
 -> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either
     [Error] (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t1 Either
  [Error] (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (r -> RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t2 Either [Error] (r -> RType RTyCon RTyVar r)
-> Either [Error] r -> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
    go [Symbol]
bs (RApp BTyCon
tc [RType BTyCon BTyVar r]
ts [RTProp BTyCon BTyVar r]
rs r
r) = [Symbol]
-> BTyCon
-> [RType BTyCon BTyVar r]
-> [RTProp BTyCon BTyVar r]
-> r
-> Either [Error] (RType RTyCon RTyVar r)
goRApp [Symbol]
bs BTyCon
tc [RType BTyCon BTyVar r]
ts [RTProp BTyCon BTyVar r]
rs r
r
    go [Symbol]
bs (RFun Symbol
x RFInfo
i RType BTyCon BTyVar r
t1 RType BTyCon BTyVar r
t2 r
r) = [Symbol]
-> Symbol
-> RFInfo
-> RType BTyCon BTyVar r
-> RType BTyCon BTyVar r
-> r
-> Either [Error] (RType RTyCon RTyVar r)
goRFun [Symbol]
bs Symbol
x RFInfo
i RType BTyCon BTyVar r
t1 RType BTyCon BTyVar r
t2 r
r
    go [Symbol]
bs (RVar BTyVar
a r
r)        = RTyVar -> r -> RType RTyCon RTyVar r
forall c tv r. tv -> r -> RType c tv r
RVar (BTyVar -> RTyVar
RT.bareRTyVar BTyVar
a) (r -> RType RTyCon RTyVar r)
-> Either [Error] r -> Either [Error] (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
    go [Symbol]
bs (RAllT RTVU BTyCon BTyVar
a RType BTyCon BTyVar r
t r
r)     = RTVar RTyVar (RType RTyCon RTyVar ())
-> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVar RTyVar (RType RTyCon RTyVar ())
forall {s2}. RTVar RTyVar s2
a' (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t Either [Error] (r -> RType RTyCon RTyVar r)
-> Either [Error] r -> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
      where a' :: RTVar RTyVar s2
a'              = RTVar RTyVar BSort -> RTVar RTyVar s2
forall tv s1 s2. RTVar tv s1 -> RTVar tv s2
dropTyVarInfo ((BTyVar -> RTyVar) -> RTVU BTyCon BTyVar -> RTVar RTyVar BSort
forall tv1 tv2 s. (tv1 -> tv2) -> RTVar tv1 s -> RTVar tv2 s
mapTyVarValue BTyVar -> RTyVar
RT.bareRTyVar RTVU BTyCon BTyVar
a)
    go [Symbol]
bs (RAllP PVar BSort
a RType BTyCon BTyVar r
t)       = RPVar -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP RPVar
a' (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t
      where a' :: RPVar
a'              = Env -> ModName -> SourcePos -> PVar BSort -> RPVar
ofBPVar Env
env ModName
name SourcePos
l PVar BSort
a
    go [Symbol]
bs (RAllE Symbol
x RType BTyCon BTyVar r
t1 RType BTyCon BTyVar r
t2)   = Symbol
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
x  (RType RTyCon RTyVar r
 -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t1    Either [Error] (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t2
    go [Symbol]
bs (REx Symbol
x RType BTyCon BTyVar r
t1 RType BTyCon BTyVar r
t2)     = Symbol
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx   Symbol
x  (RType RTyCon RTyVar r
 -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t1    Either [Error] (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
bs) RType BTyCon BTyVar r
t2
    go [Symbol]
bs (RRTy [(Symbol, RType BTyCon BTyVar r)]
xts r
r Oblig
o RType BTyCon BTyVar r
t)  = [(Symbol, RType RTyCon RTyVar r)]
-> r -> Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy  ([(Symbol, RType RTyCon RTyVar r)]
 -> r -> Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] [(Symbol, RType RTyCon RTyVar r)]
-> Either
     [Error]
     (r -> Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either [Error] [(Symbol, RType RTyCon RTyVar r)]
xts' Either
  [Error]
  (r -> Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] r
-> Either
     [Error] (Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r Either
  [Error] (Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] Oblig
-> Either [Error] (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Oblig -> Either [Error] Oblig
forall a. a -> Either [Error] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Oblig
o Either [Error] (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t
      where xts' :: Either [Error] [(Symbol, RType RTyCon RTyVar r)]
xts'            = ((Symbol, RType BTyCon BTyVar r)
 -> Either [Error] (Symbol, RType RTyCon RTyVar r))
-> [(Symbol, RType BTyCon BTyVar r)]
-> Either [Error] [(Symbol, RType RTyCon RTyVar r)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r))
-> (Symbol, RType BTyCon BTyVar r)
-> Either [Error] (Symbol, RType RTyCon RTyVar r)
forall (m :: * -> *) b c a.
Applicative m =>
(b -> m c) -> (a, b) -> m (a, c)
Misc.mapSndM ([Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs)) [(Symbol, RType BTyCon BTyVar r)]
xts
    go [Symbol]
bs (RHole r
r)         = r -> RType RTyCon RTyVar r
forall c tv r. r -> RType c tv r
RHole    (r -> RType RTyCon RTyVar r)
-> Either [Error] r -> Either [Error] (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
    go [Symbol]
bs (RExprArg Located Expr
le)     = RType RTyCon RTyVar r -> Either [Error] (RType RTyCon RTyVar r)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return    (RType RTyCon RTyVar r -> Either [Error] (RType RTyCon RTyVar r))
-> RType RTyCon RTyVar r -> Either [Error] (RType RTyCon RTyVar r)
forall a b. (a -> b) -> a -> b
$ Located Expr -> RType RTyCon RTyVar r
forall c tv r. Located Expr -> RType c tv r
RExprArg (Env
-> ModName -> SourcePos -> [Symbol] -> Located Expr -> Located Expr
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs Located Expr
le)
    goRef :: [Symbol]
-> RTProp BTyCon BTyVar r
-> Either [Error] (RTProp RTyCon RTyVar r)
goRef [Symbol]
bs (RProp [(Symbol, BSort)]
ss (RHole r
r)) = [(Symbol, RType RTyCon RTyVar ())] -> r -> RTProp RTyCon RTyVar r
forall τ r c tv. [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
rPropP ([(Symbol, RType RTyCon RTyVar ())] -> r -> RTProp RTyCon RTyVar r)
-> Either [Error] [(Symbol, RType RTyCon RTyVar ())]
-> Either [Error] (r -> RTProp RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Symbol, BSort)
 -> Either [Error] (Symbol, RType RTyCon RTyVar ()))
-> [(Symbol, BSort)]
-> Either [Error] [(Symbol, RType RTyCon RTyVar ())]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Symbol, BSort) -> Either [Error] (Symbol, RType RTyCon RTyVar ())
forall {t}.
(t, BSort) -> Either [Error] (t, RType RTyCon RTyVar ())
goSyms [(Symbol, BSort)]
ss Either [Error] (r -> RTProp RTyCon RTyVar r)
-> Either [Error] r -> Either [Error] (RTProp RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
    goRef [Symbol]
bs (RProp [(Symbol, BSort)]
ss RType BTyCon BTyVar r
t)         = [(Symbol, RType RTyCon RTyVar ())]
-> RType RTyCon RTyVar r -> RTProp RTyCon RTyVar r
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp  ([(Symbol, RType RTyCon RTyVar ())]
 -> RType RTyCon RTyVar r -> RTProp RTyCon RTyVar r)
-> Either [Error] [(Symbol, RType RTyCon RTyVar ())]
-> Either [Error] (RType RTyCon RTyVar r -> RTProp RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Symbol, BSort)
 -> Either [Error] (Symbol, RType RTyCon RTyVar ()))
-> [(Symbol, BSort)]
-> Either [Error] [(Symbol, RType RTyCon RTyVar ())]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Symbol, BSort) -> Either [Error] (Symbol, RType RTyCon RTyVar ())
forall {t}.
(t, BSort) -> Either [Error] (t, RType RTyCon RTyVar ())
goSyms [(Symbol, BSort)]
ss Either [Error] (RType RTyCon RTyVar r -> RTProp RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RTProp RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RType BTyCon BTyVar r
t
    goSyms :: (t, BSort) -> Either [Error] (t, RType RTyCon RTyVar ())
goSyms (t
x, BSort
t)                 = (t
x,) (RType RTyCon RTyVar () -> (t, RType RTyCon RTyVar ()))
-> Either [Error] (RType RTyCon RTyVar ())
-> Either [Error] (t, RType RTyCon RTyVar ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env
-> ModName
-> SourcePos
-> BSort
-> Either [Error] (RType RTyCon RTyVar ())
ofBSortE Env
env ModName
name SourcePos
l BSort
t
    goRApp :: [Symbol]
-> BTyCon
-> [RType BTyCon BTyVar r]
-> [RTProp BTyCon BTyVar r]
-> r
-> Either [Error] (RType RTyCon RTyVar r)
goRApp [Symbol]
bs BTyCon
tc [RType BTyCon BTyVar r]
ts [RTProp BTyCon BTyVar r]
rs r
r          = r
-> Located TyCon
-> [RTProp RTyCon RTyVar r]
-> [RType RTyCon RTyVar r]
-> RType RTyCon RTyVar r
forall r.
Expandable r =>
r
-> Located TyCon
-> [RTProp RTyCon RTyVar r]
-> [RType RTyCon RTyVar r]
-> RType RTyCon RTyVar r
bareTCApp (r
 -> Located TyCon
 -> [RTProp RTyCon RTyVar r]
 -> [RType RTyCon RTyVar r]
 -> RType RTyCon RTyVar r)
-> Either [Error] r
-> Either
     [Error]
     (Located TyCon
      -> [RTProp RTyCon RTyVar r]
      -> [RType RTyCon RTyVar r]
      -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r Either
  [Error]
  (Located TyCon
   -> [RTProp RTyCon RTyVar r]
   -> [RType RTyCon RTyVar r]
   -> RType RTyCon RTyVar r)
-> Either [Error] (Located TyCon)
-> Either
     [Error]
     ([RTProp RTyCon RTyVar r]
      -> [RType RTyCon RTyVar r] -> RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Either [Error] (Located TyCon)
lc' Either
  [Error]
  ([RTProp RTyCon RTyVar r]
   -> [RType RTyCon RTyVar r] -> RType RTyCon RTyVar r)
-> Either [Error] [RTProp RTyCon RTyVar r]
-> Either
     [Error] ([RType RTyCon RTyVar r] -> RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (RTProp BTyCon BTyVar r -> Either [Error] (RTProp RTyCon RTyVar r))
-> [RTProp BTyCon BTyVar r]
-> Either [Error] [RTProp RTyCon RTyVar r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([Symbol]
-> RTProp BTyCon BTyVar r
-> Either [Error] (RTProp RTyCon RTyVar r)
goRef [Symbol]
bs) [RTProp BTyCon BTyVar r]
rs Either [Error] ([RType RTyCon RTyVar r] -> RType RTyCon RTyVar r)
-> Either [Error] [RType RTyCon RTyVar r]
-> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r))
-> [RType BTyCon BTyVar r]
-> Either [Error] [RType RTyCon RTyVar r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([Symbol]
-> RType BTyCon BTyVar r -> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs) [RType BTyCon BTyVar r]
ts
      where
        lc' :: Either [Error] (Located TyCon)
lc'                    = LocSymbol -> TyCon -> Located TyCon
forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
lc (TyCon -> Located TyCon)
-> Lookup TyCon -> Either [Error] (Located TyCon)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> ModName -> LocSymbol -> Int -> Lookup TyCon
matchTyCon Env
env ModName
name LocSymbol
lc ([RType BTyCon BTyVar r] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType BTyCon BTyVar r]
ts)
        lc :: LocSymbol
lc                     = BTyCon -> LocSymbol
btc_tc BTyCon
tc
    -- 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
  | Symbol -> Bool
forall c. TyConable c => c -> Bool
isList Symbol
c Bool -> Bool -> Bool
&& Int
arity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1  = TyCon -> Lookup TyCon
forall a b. b -> Either a b
Right TyCon
Ghc.listTyCon
  | Symbol -> Bool
forall c. TyConable c => c -> Bool
isTuple Symbol
c               = TyCon -> Lookup TyCon
forall a b. b -> Either a b
Right TyCon
tuplTc
  | Bool
otherwise               = Env -> ModName -> String -> LocSymbol -> Lookup TyCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Lookup a
resolveLocSym Env
env ModName
name String
msg LocSymbol
lc
  where
    msg :: String
msg                     = String
"matchTyCon: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. PPrint a => a -> String
F.showpp Symbol
c
    tuplTc :: TyCon
tuplTc                  = Boxity -> Int -> TyCon
Ghc.tupleTyCon Boxity
Ghc.Boxed Int
arity


bareTCApp :: (Expandable r)
          => r
          -> Located Ghc.TyCon
          -> [RTProp RTyCon RTyVar r]
          -> [RType RTyCon RTyVar r]
          -> RType RTyCon RTyVar r
bareTCApp :: forall r.
Expandable r =>
r
-> Located TyCon
-> [RTProp RTyCon RTyVar r]
-> [RType RTyCon RTyVar r]
-> RType RTyCon RTyVar r
bareTCApp r
r (Loc SourcePos
l SourcePos
_ TyCon
c) [RTProp RTyCon RTyVar r]
rs [RType RTyCon RTyVar r]
ts | Just Type
rhs <- TyCon -> Maybe Type
Ghc.synTyConRhs_maybe TyCon
c
  = if TyCon -> Int
GM.kindTCArity TyCon
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [RType RTyCon RTyVar r] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType RTyCon RTyVar r]
ts
      then Error -> RType RTyCon RTyVar r
forall a e. Exception e => e -> a
Ex.throw Error
err -- error (F.showpp err)
      else RType RTyCon RTyVar r
-> [RType RTyCon RTyVar r]
-> [RTProp RTyCon RTyVar r]
-> r
-> RType RTyCon RTyVar r
forall r c tv.
Reftable r =>
RType c tv r
-> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
tyApp ([(RTyVar, RType RTyCon RTyVar (), RType RTyCon RTyVar r)]
-> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall tv (t :: * -> *) r c.
(Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
RT.subsTyVarsMeet [(RTyVar, RType RTyCon RTyVar (), RType RTyCon RTyVar r)]
su (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall a b. (a -> b) -> a -> b
$ Type -> RType RTyCon RTyVar r
forall r. Monoid r => Type -> RRType r
RT.ofType Type
rhs) (Int -> [RType RTyCon RTyVar r] -> [RType RTyCon RTyVar r]
forall a. Int -> [a] -> [a]
drop Int
nts [RType RTyCon RTyVar r]
ts) [RTProp RTyCon RTyVar r]
rs r
r
    where
       tvs :: [Id]
tvs = [ Id
v | (Id
v, TyConBinder
b) <- [Id] -> [TyConBinder] -> [(Id, TyConBinder)]
forall a b. [a] -> [b] -> [(a, b)]
zip (TyCon -> [Id]
GM.tyConTyVarsDef TyCon
c) (TyCon -> [TyConBinder]
Ghc.tyConBinders TyCon
c), TyConBinder -> Bool
GM.isAnonBinder TyConBinder
b]
       su :: [(RTyVar, RType RTyCon RTyVar (), RType RTyCon RTyVar r)]
su  = (Id
 -> RType RTyCon RTyVar r
 -> (RTyVar, RType RTyCon RTyVar (), RType RTyCon RTyVar r))
-> [Id]
-> [RType RTyCon RTyVar r]
-> [(RTyVar, RType RTyCon RTyVar (), RType RTyCon RTyVar r)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Id
a RType RTyCon RTyVar r
t -> (Id -> RTyVar
RT.rTyVar Id
a, RType RTyCon RTyVar r -> RType RTyCon RTyVar ()
forall c tv r. RType c tv r -> RType c tv ()
toRSort RType RTyCon RTyVar r
t, RType RTyCon RTyVar r
t)) [Id]
tvs [RType RTyCon RTyVar r]
ts
       nts :: Int
nts = [Id] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
tvs

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

bareTCApp r
r (Loc SourcePos
_ SourcePos
_ TyCon
c) [RTProp RTyCon RTyVar r]
rs [RType RTyCon RTyVar r]
ts
  = TyCon
-> [RType RTyCon RTyVar r]
-> [RTProp RTyCon RTyVar r]
-> r
-> RType RTyCon RTyVar r
forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
RT.rApp TyCon
c [RType RTyCon RTyVar r]
ts [RTProp RTyCon RTyVar r]
rs r
r


tyApp :: F.Reftable r => RType c tv r -> [RType c tv r] -> [RTProp c tv r] -> r
      -> RType c tv r
tyApp :: forall r c tv.
Reftable r =>
RType c tv r
-> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
tyApp (RApp c
c [RType c tv r]
ts [RTProp c tv r]
rs r
r) [RType c tv r]
ts' [RTProp c tv r]
rs' r
r' = c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
c ([RType c tv r]
ts [RType c tv r] -> [RType c tv r] -> [RType c tv r]
forall a. [a] -> [a] -> [a]
++ [RType c tv r]
ts') ([RTProp c tv r]
rs [RTProp c tv r] -> [RTProp c tv r] -> [RTProp c tv r]
forall a. [a] -> [a] -> [a]
++ [RTProp c tv r]
rs') (r
r r -> r -> r
forall r. Reftable r => r -> r -> r
`F.meet` r
r')
tyApp RType c tv r
t                []  []  r
r  = RType c tv r
t RType c tv r -> r -> RType c tv r
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`RT.strengthen` r
r
tyApp RType c tv r
_                 [RType c tv r]
_  [RTProp c tv r]
_   r
_  = Maybe SrcSpan -> String -> RType c tv r
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"Bare.Type.tyApp on invalid inputs"

expandRTypeSynonyms :: (Expandable r) => RRType r -> RRType r
expandRTypeSynonyms :: forall r. Expandable r => RRType r -> RRType r
expandRTypeSynonyms = Type -> RRType r
forall r. Monoid r => Type -> RRType r
RT.ofType (Type -> RRType r) -> (RRType r -> Type) -> RRType r -> RRType r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
Ghc.expandTypeSynonyms (Type -> Type) -> (RRType r -> Type) -> RRType r -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> RRType r -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
RT.toType Bool
False

{-
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 = LocSpecType -> SpecType -> LocSpecType
forall l b. Loc l => l -> b -> Located b
F.atLoc LocSpecType
t (SpecType -> LocSpecType) -> SpecType -> LocSpecType
forall a b. (a -> b) -> a -> b
$ (SpecType -> SpecType) -> SpecType -> SpecType
forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot (SrcSpan -> TCEmb TyCon -> TyConMap -> SpecType -> SpecType
addSymSort (LocSpecType -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSpecType
t) TCEmb TyCon
tce TyConMap
tyi) (LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
t)

addSymSort :: Ghc.SrcSpan -> F.TCEmb Ghc.TyCon -> TyConMap -> SpecType -> SpecType
addSymSort :: SrcSpan -> TCEmb TyCon -> TyConMap -> SpecType -> SpecType
addSymSort SrcSpan
sp TCEmb TyCon
tce TyConMap
tyi (RApp rc :: RTyCon
rc@RTyCon{} [SpecType]
ts [RTProp RTyCon RTyVar RReft]
rs RReft
rr)
  = RTyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> SpecType
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
rc [SpecType]
ts ((RPVar
 -> RTProp RTyCon RTyVar RReft -> Int -> RTProp RTyCon RTyVar RReft)
-> [RPVar]
-> [RTProp RTyCon RTyVar RReft]
-> [Int]
-> [RTProp RTyCon RTyVar RReft]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 (SrcSpan
-> RTyCon
-> RPVar
-> RTProp RTyCon RTyVar RReft
-> Int
-> RTProp RTyCon RTyVar RReft
forall s.
PPrint s =>
SrcSpan
-> s
-> RPVar
-> RTProp RTyCon RTyVar RReft
-> Int
-> RTProp RTyCon RTyVar RReft
addSymSortRef SrcSpan
sp RTyCon
rc) [RPVar]
pvs [RTProp RTyCon RTyVar RReft]
rargs [Int
1..]) RReft
r2
  where
    (RTyCon
_, [RPVar]
pvs)           = TCEmb TyCon
-> TyConMap -> RTyCon -> [SpecType] -> (RTyCon, [RPVar])
forall r.
ToTypeable r =>
TCEmb TyCon
-> TyConMap -> RTyCon -> [RRType r] -> (RTyCon, [RPVar])
RT.appRTyCon TCEmb TyCon
tce TyConMap
tyi RTyCon
rc [SpecType]
ts
    -- pvs             = rTyConPVs rc'
    ([RTProp RTyCon RTyVar RReft]
rargs, [RTProp RTyCon RTyVar RReft]
rrest)     = Int
-> [RTProp RTyCon RTyVar RReft]
-> ([RTProp RTyCon RTyVar RReft], [RTProp RTyCon RTyVar RReft])
forall a. Int -> [a] -> ([a], [a])
splitAt ([RPVar] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RPVar]
pvs) [RTProp RTyCon RTyVar RReft]
rs
    r2 :: RReft
r2                 = (RReft -> RTProp RTyCon RTyVar RReft -> RReft)
-> RReft -> [RTProp RTyCon RTyVar RReft] -> RReft
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' RReft -> RTProp RTyCon RTyVar RReft -> RReft
forall {r} {τ} {c} {tv}.
Reftable r =>
r -> Ref τ (RType c tv r) -> r
go RReft
rr [RTProp RTyCon RTyVar RReft]
rrest
    go :: r -> Ref τ (RType c tv r) -> r
go r
r (RProp [(Symbol, τ)]
_ (RHole r
r')) = r
r' r -> r -> r
forall r. Reftable r => r -> r -> r
`F.meet` r
r
    go r
r (RProp  [(Symbol, τ)]
_ RType c tv r
t' )       = let r' :: r
r' = r -> Maybe r -> r
forall a. a -> Maybe a -> a
Mb.fromMaybe r
forall a. Monoid a => a
mempty (RType c tv r -> Maybe r
forall c tv r. RType c tv r -> Maybe r
stripRTypeBase RType c tv r
t') in r
r r -> r -> r
forall r. Reftable r => r -> r -> r
`F.meet` r
r'

addSymSort SrcSpan
_ TCEmb TyCon
_ TyConMap
_ SpecType
t
  = SpecType
t

addSymSortRef :: (PPrint s) => Ghc.SrcSpan -> s -> RPVar -> SpecProp -> Int -> SpecProp
addSymSortRef :: forall s.
PPrint s =>
SrcSpan
-> s
-> RPVar
-> RTProp RTyCon RTyVar RReft
-> Int
-> RTProp RTyCon RTyVar RReft
addSymSortRef SrcSpan
sp s
rc RPVar
p RTProp RTyCon RTyVar RReft
r Int
i
  | RPVar -> Bool
forall t. PVar t -> Bool
isPropPV RPVar
p
  = SrcSpan
-> s
-> Int
-> RPVar
-> RTProp RTyCon RTyVar RReft
-> RTProp RTyCon RTyVar RReft
forall s.
PPrint s =>
SrcSpan
-> s
-> Int
-> RPVar
-> RTProp RTyCon RTyVar RReft
-> RTProp RTyCon RTyVar RReft
addSymSortRef' SrcSpan
sp s
rc Int
i RPVar
p RTProp RTyCon RTyVar RReft
r
  | Bool
otherwise
  = Maybe SrcSpan -> String -> RTProp RTyCon RTyVar RReft
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"addSymSortRef: malformed ref application"

addSymSortRef' :: (PPrint s) => Ghc.SrcSpan -> s -> Int -> RPVar -> SpecProp -> SpecProp
addSymSortRef' :: forall s.
PPrint s =>
SrcSpan
-> s
-> Int
-> RPVar
-> RTProp RTyCon RTyVar RReft
-> RTProp RTyCon RTyVar RReft
addSymSortRef' SrcSpan
_ s
_ Int
_ RPVar
p (RProp [(Symbol, RType RTyCon RTyVar ())]
s (RVar RTyVar
v RReft
r)) | RTyVar -> Bool
forall a. Symbolic a => a -> Bool
isDummy RTyVar
v
  = [(Symbol, RType RTyCon RTyVar ())]
-> SpecType -> RTProp RTyCon RTyVar RReft
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
xs SpecType
t
    where
      t :: SpecType
t  = RType RTyCon RTyVar () -> SpecType
forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort (RPVar -> RType RTyCon RTyVar ()
forall t. PVar t -> t
pvType RPVar
p) SpecType -> RReft -> SpecType
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`RT.strengthen` RReft
r
      xs :: [(Symbol, RType RTyCon RTyVar ())]
xs = String
-> [(Symbol, RType RTyCon RTyVar ())]
-> RPVar
-> [(Symbol, RType RTyCon RTyVar ())]
forall b t. String -> [(Symbol, b)] -> PVar t -> [(Symbol, t)]
spliceArgs String
"addSymSortRef 1" [(Symbol, RType RTyCon RTyVar ())]
s RPVar
p

addSymSortRef' SrcSpan
sp s
rc Int
i RPVar
p (RProp [(Symbol, RType RTyCon RTyVar ())]
_ (RHole r :: RReft
r@(MkUReft Reft
_ (Pr [UsedPVar
up]))))
  | [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [RType RTyCon RTyVar ()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType RTyCon RTyVar ()]
ts
  = [(Symbol, RType RTyCon RTyVar ())]
-> SpecType -> RTProp RTyCon RTyVar RReft
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
xts (RReft -> SpecType
forall c tv r. r -> RType c tv r
RHole RReft
r)
  | Bool
otherwise
  = -- Misc.errorP "ZONK" $ F.showpp (rc, pname up, i, length xs, length ts)
    UserError -> RTProp RTyCon RTyVar RReft
forall a. UserError -> a
uError (UserError -> RTProp RTyCon RTyVar RReft)
-> UserError -> RTProp RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Doc -> Int -> Int -> Int -> UserError
forall t. SrcSpan -> Doc -> Doc -> Int -> Int -> Int -> TError t
ErrPartPred SrcSpan
sp (s -> Doc
forall a. PPrint a => a -> Doc
pprint s
rc) (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (Symbol -> Doc) -> Symbol -> Doc
forall a b. (a -> b) -> a -> b
$ UsedPVar -> Symbol
forall t. PVar t -> Symbol
pname UsedPVar
up) Int
i ([Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
xs) ([RType RTyCon RTyVar ()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType RTyCon RTyVar ()]
ts)
    where
      xts :: [(Symbol, RType RTyCon RTyVar ())]
xts = String
-> [Symbol]
-> [RType RTyCon RTyVar ()]
-> [(Symbol, RType RTyCon RTyVar ())]
forall t t1. String -> [t] -> [t1] -> [(t, t1)]
Misc.safeZipWithError String
"addSymSortRef'" [Symbol]
xs [RType RTyCon RTyVar ()]
ts
      xs :: [Symbol]
xs  = ((), Symbol, Expr) -> Symbol
forall a b c. (a, b, c) -> b
Misc.snd3 (((), Symbol, Expr) -> Symbol) -> [((), Symbol, Expr)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UsedPVar -> [((), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
up
      ts :: [RType RTyCon RTyVar ()]
ts  = (RType RTyCon RTyVar (), Symbol, Expr) -> RType RTyCon RTyVar ()
forall a b c. (a, b, c) -> a
Misc.fst3 ((RType RTyCon RTyVar (), Symbol, Expr) -> RType RTyCon RTyVar ())
-> [(RType RTyCon RTyVar (), Symbol, Expr)]
-> [RType RTyCon RTyVar ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RPVar -> [(RType RTyCon RTyVar (), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs RPVar
p

addSymSortRef' SrcSpan
_ s
_ Int
_ RPVar
_ (RProp [(Symbol, RType RTyCon RTyVar ())]
s (RHole RReft
r))
  = [(Symbol, RType RTyCon RTyVar ())]
-> SpecType -> RTProp RTyCon RTyVar RReft
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
s (RReft -> SpecType
forall c tv r. r -> RType c tv r
RHole RReft
r)

addSymSortRef' SrcSpan
_ s
_ Int
_ RPVar
p (RProp [(Symbol, RType RTyCon RTyVar ())]
s SpecType
t)
  = [(Symbol, RType RTyCon RTyVar ())]
-> SpecType -> RTProp RTyCon RTyVar RReft
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
xs SpecType
t
    where
      xs :: [(Symbol, RType RTyCon RTyVar ())]
xs = String
-> [(Symbol, RType RTyCon RTyVar ())]
-> RPVar
-> [(Symbol, RType RTyCon RTyVar ())]
forall b t. String -> [(Symbol, b)] -> PVar t -> [(Symbol, t)]
spliceArgs String
"addSymSortRef 2" [(Symbol, RType RTyCon RTyVar ())]
s RPVar
p

spliceArgs :: String  -> [(F.Symbol, b)] -> PVar t -> [(F.Symbol, t)]
spliceArgs :: forall b t. String -> [(Symbol, b)] -> PVar t -> [(Symbol, t)]
spliceArgs String
msg [(Symbol, b)]
syms PVar t
p = [Symbol] -> [(t, Symbol, Expr)] -> [(Symbol, t)]
forall {a} {b} {c}. Show a => [a] -> [(b, a, c)] -> [(a, b)]
go ((Symbol, b) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, b) -> Symbol) -> [(Symbol, b)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, b)]
syms) (PVar t -> [(t, Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar t
p)
  where
    go :: [a] -> [(b, a, c)] -> [(a, b)]
go []     []           = []
    go []     ((b
s,a
x,c
_):[(b, a, c)]
as) = (a
x, b
s)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[a] -> [(b, a, c)] -> [(a, b)]
go [] [(b, a, c)]
as
    go (a
x:[a]
xs) ((b
s,a
_,c
_):[(b, a, c)]
as) = (a
x,b
s)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[a] -> [(b, a, c)] -> [(a, b)]
go [a]
xs [(b, a, c)]
as
    go [a]
xs     []           = Maybe SrcSpan -> String -> [(a, b)]
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String -> [(a, b)]) -> String -> [(a, b)]
forall a b. (a -> b) -> a -> b
$ String
"spliceArgs: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"on XS=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [a] -> String
forall a. Show a => a -> String
show [a]
xs

---------------------------------------------------------------------------------
-- 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 [(Id, (LocBareType, Maybe [Located Expr]))]
-> [(Id, (LocBareType, Maybe [Located Expr]))]
-> [(Id, (LocBareType, Maybe [Located Expr]))]
forall a. [a] -> [a] -> [a]
++ [(Id, (LocBareType, Maybe [Located Expr]))]
-> [(Id, (LocBareType, Maybe [Located Expr]))]
replace [(Id, (LocBareType, Maybe [Located Expr]))]
locTs ]
  where
    ([(Id, (LocBareType, Maybe [Located Expr]))]
locTs, [(Id, (LocBareType, Maybe [Located Expr]))]
topTs)         = [(Id, (LocBareType, Maybe [Located Expr]))]
-> ([(Id, (LocBareType, Maybe [Located Expr]))],
    [(Id, (LocBareType, Maybe [Located Expr]))])
forall a. [(Id, a)] -> ([(Id, a)], [(Id, a)])
partitionLocalBinds [ (Id
x, (LocBareType
t, Maybe [Located Expr]
es)) | (Id
x, LocBareType
t, Maybe [Located Expr]
es) <- [(Id, LocBareType, Maybe [Located Expr])]
xtes]
    replace :: [(Id, (LocBareType, Maybe [Located Expr]))]
-> [(Id, (LocBareType, Maybe [Located Expr]))]
replace                = HashMap Id (LocBareType, Maybe [Located Expr])
-> [(Id, (LocBareType, Maybe [Located Expr]))]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Id (LocBareType, Maybe [Located Expr])
 -> [(Id, (LocBareType, Maybe [Located Expr]))])
-> ([(Id, (LocBareType, Maybe [Located Expr]))]
    -> HashMap Id (LocBareType, Maybe [Located Expr]))
-> [(Id, (LocBareType, Maybe [Located Expr]))]
-> [(Id, (LocBareType, Maybe [Located Expr]))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap Id (LocBareType, Maybe [Located Expr])
-> HashMap Id (LocBareType, Maybe [Located Expr])
replaceSigs (HashMap Id (LocBareType, Maybe [Located Expr])
 -> HashMap Id (LocBareType, Maybe [Located Expr]))
-> ([(Id, (LocBareType, Maybe [Located Expr]))]
    -> HashMap Id (LocBareType, Maybe [Located Expr]))
-> [(Id, (LocBareType, Maybe [Located Expr]))]
-> HashMap Id (LocBareType, Maybe [Located Expr])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Id, (LocBareType, Maybe [Located Expr]))]
-> HashMap Id (LocBareType, Maybe [Located Expr])
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList
    replaceSigs :: HashMap Id (LocBareType, Maybe [Located Expr])
-> HashMap Id (LocBareType, Maybe [Located Expr])
replaceSigs HashMap Id (LocBareType, Maybe [Located Expr])
sigm       = CoreVisitor SymMap (HashMap Id (LocBareType, Maybe [Located Expr]))
-> SymMap
-> HashMap Id (LocBareType, Maybe [Located Expr])
-> [CoreBind]
-> HashMap Id (LocBareType, Maybe [Located Expr])
forall env acc.
CoreVisitor env acc -> env -> acc -> [CoreBind] -> acc
coreVisitor CoreVisitor SymMap (HashMap Id (LocBareType, Maybe [Located Expr]))
replaceVisitor SymMap
forall k v. HashMap k v
M.empty HashMap Id (LocBareType, Maybe [Located Expr])
sigm [CoreBind]
cbs
    cbs :: [CoreBind]
cbs                    = GhcSrc -> [CoreBind]
_giCbs (Env -> GhcSrc
reSrc Env
env)

replaceVisitor :: CoreVisitor SymMap SigMap
replaceVisitor :: CoreVisitor SymMap (HashMap Id (LocBareType, Maybe [Located Expr]))
replaceVisitor = CoreVisitor
  { envF :: SymMap -> Id -> SymMap
envF  = SymMap -> Id -> SymMap
addBind
  , bindF :: SymMap
-> HashMap Id (LocBareType, Maybe [Located Expr])
-> Id
-> HashMap Id (LocBareType, Maybe [Located Expr])
bindF = SymMap
-> HashMap Id (LocBareType, Maybe [Located Expr])
-> Id
-> HashMap Id (LocBareType, Maybe [Located Expr])
updSigMap
  , exprF :: SymMap
-> HashMap Id (LocBareType, Maybe [Located Expr])
-> Expr Id
-> HashMap Id (LocBareType, Maybe [Located Expr])
exprF = \SymMap
_ HashMap Id (LocBareType, Maybe [Located Expr])
m Expr Id
_ -> HashMap Id (LocBareType, Maybe [Located Expr])
m
  }

addBind :: SymMap -> Ghc.Var -> SymMap
addBind :: SymMap -> Id -> SymMap
addBind SymMap
env Id
v = case Id -> Maybe Symbol
localKey Id
v of
  Just Symbol
vx -> Symbol -> Symbol -> SymMap -> SymMap
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
vx (Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Id
v) SymMap
env
  Maybe Symbol
Nothing -> SymMap
env

updSigMap :: SymMap -> SigMap -> Ghc.Var -> SigMap
updSigMap :: SymMap
-> HashMap Id (LocBareType, Maybe [Located Expr])
-> Id
-> HashMap Id (LocBareType, Maybe [Located Expr])
updSigMap SymMap
env HashMap Id (LocBareType, Maybe [Located Expr])
m Id
v = case Id
-> HashMap Id (LocBareType, Maybe [Located Expr])
-> Maybe (LocBareType, Maybe [Located Expr])
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Id
v HashMap Id (LocBareType, Maybe [Located Expr])
m of
  Maybe (LocBareType, Maybe [Located Expr])
Nothing  -> HashMap Id (LocBareType, Maybe [Located Expr])
m
  Just (LocBareType, Maybe [Located Expr])
tes -> Id
-> (LocBareType, Maybe [Located Expr])
-> HashMap Id (LocBareType, Maybe [Located Expr])
-> HashMap Id (LocBareType, Maybe [Located Expr])
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Id
v (String
-> (LocBareType, Maybe [Located Expr])
-> (LocBareType, Maybe [Located Expr])
forall a. PPrint a => String -> a -> a
myTracepp (String
"UPD-LOCAL-SIG " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Outputable a => a -> String
GM.showPpr Id
v) ((LocBareType, Maybe [Located Expr])
 -> (LocBareType, Maybe [Located Expr]))
-> (LocBareType, Maybe [Located Expr])
-> (LocBareType, Maybe [Located Expr])
forall a b. (a -> b) -> a -> b
$ SymMap
-> (LocBareType, Maybe [Located Expr])
-> (LocBareType, Maybe [Located Expr])
renameLocalSig SymMap
env (LocBareType, Maybe [Located Expr])
tes) HashMap Id (LocBareType, Maybe [Located Expr])
m

renameLocalSig :: SymMap -> (LocBareType, Maybe [Located F.Expr])
               -> (LocBareType, Maybe [Located F.Expr])
renameLocalSig :: SymMap
-> (LocBareType, Maybe [Located Expr])
-> (LocBareType, Maybe [Located Expr])
renameLocalSig SymMap
env (LocBareType
t, Maybe [Located Expr]
es) = ((Symbol -> Expr) -> LocBareType -> LocBareType
forall a. Subable a => (Symbol -> Expr) -> a -> a
F.substf Symbol -> Expr
tSub LocBareType
t, (Symbol -> Expr) -> Maybe [Located Expr] -> Maybe [Located Expr]
forall a. Subable a => (Symbol -> Expr) -> a -> a
F.substf Symbol -> Expr
esSub Maybe [Located Expr]
es)
  where
    tSub :: Symbol -> Expr
tSub                   = Symbol -> Expr
F.EVar (Symbol -> Expr) -> (Symbol -> Symbol) -> Symbol -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymMap -> Symbol -> Symbol
qualifySymMap SymMap
env
    esSub :: Symbol -> Expr
esSub                  = Symbol -> Expr
tSub (Symbol -> Expr) -> [Symbol] -> Symbol -> Expr
`F.substfExcept` [Symbol]
xs
    xs :: [Symbol]
xs                     = RTypeRep BTyCon BTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds (BareType -> RTypeRep BTyCon BTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (LocBareType -> BareType
forall a. Located a -> a
F.val LocBareType
t))

qualifySymMap :: SymMap -> F.Symbol -> F.Symbol
qualifySymMap :: SymMap -> Symbol -> Symbol
qualifySymMap SymMap
env Symbol
x = Symbol -> Symbol -> SymMap -> Symbol
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Symbol
x Symbol
x SymMap
env

type SigMap = M.HashMap Ghc.Var  (LocBareType, Maybe [Located F.Expr])
type SymMap = M.HashMap F.Symbol F.Symbol

---------------------------------------------------------------------------------
partitionLocalBinds :: [(Ghc.Var, a)] -> ([(Ghc.Var, a)], [(Ghc.Var, a)])
---------------------------------------------------------------------------------
partitionLocalBinds :: forall a. [(Id, a)] -> ([(Id, a)], [(Id, a)])
partitionLocalBinds = ((Id, a) -> Bool) -> [(Id, a)] -> ([(Id, a)], [(Id, a)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (Maybe Symbol -> Bool
forall a. Maybe a -> Bool
Mb.isJust (Maybe Symbol -> Bool)
-> ((Id, a) -> Maybe Symbol) -> (Id, a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Maybe Symbol
localKey (Id -> Maybe Symbol) -> ((Id, a) -> Id) -> (Id, a) -> Maybe Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, a) -> Id
forall a b. (a, b) -> a
fst)