-- | 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 TypeSynonymInstances  #-}
{-# 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 (..)
  , qualifyTop, qualifyTopDummy
  
  -- * Looking up names
  , maybeResolveSym 
  , lookupGhcDataCon 
  , lookupGhcDnTyCon 
  , lookupGhcTyCon 
  , lookupGhcVar 
  , lookupGhcNamedVar 

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

  -- * Misc 
  , srcVars 

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

  -- * Post-processing types
  , txRefSort
  , errResolve

  -- * Fixing local variables
  , resolveLocalBinds 
  , partitionLocalBinds 
  ) where 

import qualified Control.Exception                 as Ex 
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.Utils.Files         as F 
import qualified Language.Fixpoint.Types               as F 
import qualified Language.Fixpoint.Types.Visitor       as F 
import qualified Language.Fixpoint.Misc                as Misc 
import qualified Language.Haskell.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 qualified Language.Haskell.Liquid.Types.Errors  as Errors 
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 :: String -> a -> a
myTracepp = String -> a -> a
forall a. PPrint a => String -> a -> a
F.notracepp 

-------------------------------------------------------------------------------
-- | 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 :: LogicMap
-> [(Symbol, Var)]
-> Subst
-> TyThingMap
-> Config
-> QImports
-> HashSet Symbol
-> LocalVars
-> HashSet Symbol
-> GhcSrc
-> Env
RE 
  { reLMap :: LogicMap
reLMap      = LogicMap
lmap
  , reSyms :: [(Symbol, Var)]
reSyms      = [(Symbol, Var)]
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, Var)]
syms        = [ (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
v, Var
v) | Var
v <- [Var]
vars ] 
    vars :: [Var]
vars        = GhcSrc -> [Var]
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 = [Var] -> LocalVars
localVarMap ([Var] -> LocalVars) -> (GhcSrc -> [Var]) -> GhcSrc -> LocalVars
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [CoreBind] -> [Var]
localBinds ([CoreBind] -> [Var]) -> (GhcSrc -> [CoreBind]) -> GhcSrc -> [Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GhcSrc -> [CoreBind]
_giCbs

-- TODO: rewrite using CoreVisitor
localBinds :: [Ghc.CoreBind] -> [Ghc.Var]
localBinds :: [CoreBind] -> [Var]
localBinds                    = (CoreBind -> [Var]) -> [CoreBind] -> [Var]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (HashSet Symbol -> CoreBind -> [Var]
bgo HashSet Symbol
forall a. HashSet a
S.empty) 
  where
    add :: Var -> HashSet Symbol -> HashSet Symbol
add  Var
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) (Var -> Maybe Symbol
localKey Var
x) 
    adds :: CoreBind -> HashSet Symbol -> HashSet Symbol
adds CoreBind
b HashSet Symbol
g                  = (Var -> HashSet Symbol -> HashSet Symbol)
-> HashSet Symbol -> [Var] -> HashSet Symbol
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Var -> HashSet Symbol -> HashSet Symbol
add HashSet Symbol
g (CoreBind -> [Var]
forall b. Bind b -> [b]
Ghc.bindersOf CoreBind
b) 
    take :: Var -> HashSet Symbol -> [Var]
take Var
x HashSet Symbol
g                  = [Var] -> (Symbol -> [Var]) -> Maybe Symbol -> [Var]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\Symbol
k -> if Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
k HashSet Symbol
g then [] else [Var
x]) (Var -> Maybe Symbol
localKey Var
x)
    pgo :: HashSet Symbol -> (Var, Expr Var) -> [Var]
pgo HashSet Symbol
g (Var
x, Expr Var
e)              = Var -> HashSet Symbol -> [Var]
take Var
x HashSet Symbol
g [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ HashSet Symbol -> Expr Var -> [Var]
go (Var -> HashSet Symbol -> HashSet Symbol
add Var
x HashSet Symbol
g) Expr Var
e
    bgo :: HashSet Symbol -> CoreBind -> [Var]
bgo HashSet Symbol
g (Ghc.NonRec Var
x Expr Var
e)    = HashSet Symbol -> (Var, Expr Var) -> [Var]
pgo HashSet Symbol
g (Var
x, Expr Var
e) 
    bgo HashSet Symbol
g (Ghc.Rec [(Var, Expr Var)]
xes)       = ((Var, Expr Var) -> [Var]) -> [(Var, Expr Var)] -> [Var]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (HashSet Symbol -> (Var, Expr Var) -> [Var]
pgo HashSet Symbol
g) [(Var, Expr Var)]
xes 
    go :: HashSet Symbol -> Expr Var -> [Var]
go  HashSet Symbol
g (Ghc.App Expr Var
e Expr Var
a)       = (Expr Var -> [Var]) -> [Expr Var] -> [Var]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (HashSet Symbol -> Expr Var -> [Var]
go  HashSet Symbol
g) [Expr Var
e, Expr Var
a]
    go  HashSet Symbol
g (Ghc.Lam Var
_ Expr Var
e)       = HashSet Symbol -> Expr Var -> [Var]
go HashSet Symbol
g Expr Var
e
    go  HashSet Symbol
g (Ghc.Let CoreBind
b Expr Var
e)       = HashSet Symbol -> CoreBind -> [Var]
bgo HashSet Symbol
g CoreBind
b [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ HashSet Symbol -> Expr Var -> [Var]
go (CoreBind -> HashSet Symbol -> HashSet Symbol
adds CoreBind
b HashSet Symbol
g) Expr Var
e 
    go  HashSet Symbol
g (Ghc.Tick Tickish Var
_ Expr Var
e)      = HashSet Symbol -> Expr Var -> [Var]
go HashSet Symbol
g Expr Var
e
    go  HashSet Symbol
g (Ghc.Cast Expr Var
e Coercion
_)      = HashSet Symbol -> Expr Var -> [Var]
go HashSet Symbol
g Expr Var
e
    go  HashSet Symbol
g (Ghc.Case Expr Var
e Var
_ Type
_ [Alt Var]
cs) = HashSet Symbol -> Expr Var -> [Var]
go HashSet Symbol
g Expr Var
e [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ (Alt Var -> [Var]) -> [Alt Var] -> [Var]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (HashSet Symbol -> Expr Var -> [Var]
go HashSet Symbol
g (Expr Var -> [Var]) -> (Alt Var -> Expr Var) -> Alt Var -> [Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Alt Var -> Expr Var
forall a b c. (a, b, c) -> c
Misc.thd3) [Alt Var]
cs
    go  HashSet Symbol
_ (Ghc.Var Var
_)         = []
    go  HashSet Symbol
_ Expr Var
_                   = []

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

localKey   :: Ghc.Var -> Maybe F.Symbol
localKey :: Var -> Maybe Symbol
localKey Var
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))
-> (Var -> Symbol) -> Var -> (Symbol, Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
GM.dropModuleUnique (Symbol -> Symbol) -> (Var -> Symbol) -> Var -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> (Symbol, Symbol)) -> Var -> (Symbol, Symbol)
forall a b. (a -> b) -> a -> b
$ Var
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, Var -> Expr
mkVarExpr Var
v) 
                       | (Symbol
x, [(Symbol, Var)]
mxs) <- HashMap Symbol [(Symbol, Var)] -> [(Symbol, [(Symbol, Var)])]
forall k v. HashMap k v -> [(k, v)]
M.toList       (GhcSrc -> HashMap Symbol [(Symbol, Var)]
makeSymMap GhcSrc
src) 
                       , Var
v        <- Maybe Var -> [Var]
forall a. Maybe a -> [a]
Mb.maybeToList (Symbol -> [(Symbol, Var)] -> Maybe Var
forall a. Symbol -> [(Symbol, a)] -> Maybe a
okUnqualified Symbol
me [(Symbol, Var)]
mxs) 
                       , Bool -> Bool
not (Symbol -> Bool
isWiredInName Symbol
x)
                   ] 
    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 :: 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, Var)]
makeSymMap GhcSrc
src = [(Symbol, (Symbol, Var))] -> HashMap Symbol [(Symbol, Var)]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group [ (Symbol
sym, (Symbol
m, Var
x)) 
                                | Var
x           <- GhcSrc -> [Var]
srcVars GhcSrc
src
                                , let (Symbol
m, Symbol
sym) = Var -> (Symbol, Symbol)
forall a. Symbolic a => a -> (Symbol, Symbol)
qualifiedSymbol Var
x ]

makeTyThingMap :: GhcSrc -> TyThingMap 
makeTyThingMap :: GhcSrc -> TyThingMap
makeTyThingMap GhcSrc
src =
  [(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)
             ] 

tyThingSymbol :: Ghc.TyThing -> Maybe F.Symbol 
tyThingSymbol :: TyThing -> Maybe Symbol
tyThingSymbol (Ghc.AnId     Var
x) = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
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 :: 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. (Eq b, Hashable 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 = [ Var -> TyThing
Ghc.AnId   Var
x | Var
x <- [Var]
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 :: [Var]
vars        = [Var] -> [Var]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([Var] -> [Var]) -> [Var] -> [Var]
forall a b. (a -> b) -> a -> b
$ [DataCon] -> [Var]
dataConVars [DataCon]
dcs [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ GhcSrc -> [Var]
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 = [Var] -> [TyCon]
varTyCons ([Var] -> [TyCon]) -> (GhcSrc -> [Var]) -> GhcSrc -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GhcSrc -> [Var]
srcVars 

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

dataConVars :: [Ghc.DataCon] -> [Ghc.Var]
dataConVars :: [DataCon] -> [Var]
dataConVars [DataCon]
dcs = [[Var]] -> [Var]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat 
  [ DataCon -> Var
Ghc.dataConWorkId (DataCon -> Var) -> [DataCon] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataCon]
dcs 
  , DataCon -> Var
Ghc.dataConWrapId (DataCon -> Var) -> [DataCon] -> [Var]
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 :: 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 :: 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 :: HashMap TyCon RTyCon
tcmTyRTy = RTyCon -> RTyCon
forall a. Qualify a => a -> a
tx (RTyCon -> RTyCon) -> HashMap TyCon RTyCon -> HashMap TyCon RTyCon
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyConMap -> HashMap TyCon RTyCon
tcmTyRTy TyConMap
tyi 
    , tcmFIRTy :: HashMap (TyCon, [Sort]) RTyCon
tcmFIRTy = RTyCon -> RTyCon
forall a. Qualify a => a -> a
tx (RTyCon -> RTyCon)
-> HashMap (TyCon, [Sort]) RTyCon -> HashMap (TyCon, [Sort]) RTyCon
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyConMap -> HashMap (TyCon, [Sort]) RTyCon
tcmFIRTy TyConMap
tyi 
    } 
    where 
      tx :: (Qualify a) => a -> a 
      tx :: 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 :: Maybe SizeFun
tcpSizeFun = Env -> ModName -> SourcePos -> [Symbol] -> SizeFun -> SizeFun
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name (TyConP -> SourcePos
tcpLoc TyConP
tcp) [Symbol]
bs (SizeFun -> SizeFun) -> Maybe SizeFun -> Maybe SizeFun
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyConP -> Maybe SizeFun
tcpSizeFun TyConP
tcp }

instance Qualify SizeFun where 
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> SizeFun -> SizeFun
qualify Env
env ModName
name SourcePos
_ [Symbol]
bs (SymSizeFun LocSymbol
lx) = LocSymbol -> SizeFun
SymSizeFun (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 -> Either UserError Symbol
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Either UserError 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  UserError
_ -> 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 (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 (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 (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 (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 :: Maybe SizeFun
sizeFunction = Env -> ModName -> SourcePos -> [Symbol] -> SizeFun -> SizeFun
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (SizeFun -> SizeFun) -> Maybe SizeFun -> Maybe SizeFun
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyConInfo -> Maybe SizeFun
sizeFunction TyConInfo
tci }

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

instance Qualify (Measure SpecType Ghc.DataCon) where 
  qualify :: Env
-> ModName
-> SourcePos
-> [Symbol]
-> Measure SpecType DataCon
-> Measure SpecType DataCon
qualify Env
env ModName
name SourcePos
_ [Symbol]
bs Measure SpecType DataCon
m = Measure SpecType DataCon
m -- FIXME substEnv env name bs $ 
    { msName :: LocSymbol
msName = Env -> ModName -> SourcePos -> [Symbol] -> LocSymbol -> LocSymbol
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs     LocSymbol
lname 
    , msEqns :: [Def SpecType DataCon]
msEqns = Env
-> ModName
-> SourcePos
-> [Symbol]
-> Def SpecType DataCon
-> Def SpecType DataCon
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (Def SpecType DataCon -> Def SpecType DataCon)
-> [Def SpecType DataCon] -> [Def SpecType DataCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Measure SpecType DataCon -> [Def SpecType DataCon]
forall ty ctor. Measure ty ctor -> [Def ty ctor]
msEqns Measure SpecType DataCon
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 :: Body
body  = Env -> ModName -> SourcePos -> [Symbol] -> Body -> Body
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l ([Symbol]
bs [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
bs') (Def ty ctor -> Body
forall ty ctor. Def ty ctor -> Body
body Def ty ctor
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 :: [Def LocBareType LocSymbol]
msEqns = Env
-> ModName
-> SourcePos
-> [Symbol]
-> [Def LocBareType LocSymbol]
-> [Def LocBareType LocSymbol]
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (Measure LocBareType LocSymbol -> [Def LocBareType LocSymbol]
forall ty ctor. Measure ty ctor -> [Def ty ctor]
msEqns Measure LocBareType LocSymbol
m)
    } 

instance Qualify DataCtor where 
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> DataCtor -> DataCtor
qualify Env
env ModName
name SourcePos
l [Symbol]
bs DataCtor
c = DataCtor
c
    { dcTheta :: [BareType]
dcTheta  = Env -> ModName -> SourcePos -> [Symbol] -> [BareType] -> [BareType]
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (DataCtor -> [BareType]
dcTheta  DataCtor
c) 
    , dcFields :: [(Symbol, BareType)]
dcFields = Env
-> ModName
-> SourcePos
-> [Symbol]
-> [(Symbol, BareType)]
-> [(Symbol, BareType)]
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (DataCtor -> [(Symbol, BareType)]
dcFields DataCtor
c) 
    , dcResult :: Maybe BareType
dcResult = Env
-> ModName
-> SourcePos
-> [Symbol]
-> Maybe BareType
-> Maybe BareType
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (DataCtor -> Maybe BareType
dcResult DataCtor
c)
    }
 
instance Qualify DataDecl where 
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> DataDecl -> DataDecl
qualify Env
env ModName
name SourcePos
l [Symbol]
bs DataDecl
d = DataDecl
d 
    { tycDCons :: [DataCtor]
tycDCons  = Env -> ModName -> SourcePos -> [Symbol] -> [DataCtor] -> [DataCtor]
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (DataDecl -> [DataCtor]
tycDCons  DataDecl
d)
    , tycPropTy :: Maybe BareType
tycPropTy = Env
-> ModName
-> SourcePos
-> [Symbol]
-> Maybe BareType
-> Maybe BareType
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (DataDecl -> Maybe BareType
tycPropTy DataDecl
d) 
    } 

instance Qualify ModSpecs where 
  qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs
qualify Env
env ModName
name SourcePos
l [Symbol]
bs = (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 :: [Measure LocBareType LocSymbol]
measures   = Env
-> ModName
-> SourcePos
-> [Symbol]
-> [Measure LocBareType LocSymbol]
-> [Measure LocBareType LocSymbol]
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (BareSpec -> [Measure LocBareType LocSymbol]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures   BareSpec
sp) 
  , asmSigs :: [(LocSymbol, LocBareType)]
asmSigs    = Env
-> ModName
-> SourcePos
-> [Symbol]
-> [(LocSymbol, LocBareType)]
-> [(LocSymbol, LocBareType)]
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (BareSpec -> [(LocSymbol, LocBareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
asmSigs    BareSpec
sp)
  , sigs :: [(LocSymbol, LocBareType)]
sigs       = Env
-> ModName
-> SourcePos
-> [Symbol]
-> [(LocSymbol, LocBareType)]
-> [(LocSymbol, LocBareType)]
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (BareSpec -> [(LocSymbol, LocBareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
sigs       BareSpec
sp)
  , localSigs :: [(LocSymbol, LocBareType)]
localSigs  = Env
-> ModName
-> SourcePos
-> [Symbol]
-> [(LocSymbol, LocBareType)]
-> [(LocSymbol, LocBareType)]
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (BareSpec -> [(LocSymbol, LocBareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
localSigs  BareSpec
sp)
  , reflSigs :: [(LocSymbol, LocBareType)]
reflSigs   = Env
-> ModName
-> SourcePos
-> [Symbol]
-> [(LocSymbol, LocBareType)]
-> [(LocSymbol, LocBareType)]
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (BareSpec -> [(LocSymbol, LocBareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
reflSigs   BareSpec
sp)
  , dataDecls :: [DataDecl]
dataDecls  = Env -> ModName -> SourcePos -> [Symbol] -> [DataDecl] -> [DataDecl]
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (BareSpec -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
dataDecls  BareSpec
sp)
  , newtyDecls :: [DataDecl]
newtyDecls = Env -> ModName -> SourcePos -> [Symbol] -> [DataDecl] -> [DataDecl]
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name SourcePos
l [Symbol]
bs (BareSpec -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
newtyDecls BareSpec
sp)
  , ialiases :: [(LocBareType, LocBareType)]
ialiases   = [ (LocBareType -> LocBareType
f LocBareType
x, LocBareType -> LocBareType
f LocBareType
y) | (LocBareType
x, LocBareType
y) <- BareSpec -> [(LocBareType, LocBareType)]
forall ty bndr. Spec ty bndr -> [(ty, ty)]
ialiases BareSpec
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 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 { qBody :: Expr
F.qBody = Env -> ModName -> SourcePos -> [Symbol] -> Expr -> Expr
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
qualify Env
env ModName
name (Qualifier -> SourcePos
F.qPos Qualifier
q) [Symbol]
bs' (Qualifier -> Expr
F.qBody Qualifier
q) } 
    where 
      bs' :: [Symbol]
bs'                 = [Symbol]
bs [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 :: 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 :: 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 :: Env -> ModName -> a -> Maybe Var
lookupGhcNamedVar Env
env ModName
name a
z = Env -> ModName -> String -> LocSymbol -> Maybe Var
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 -> Ghc.Var 
lookupGhcVar :: Env -> ModName -> String -> LocSymbol -> Var
lookupGhcVar Env
env ModName
name String
kind LocSymbol
lx = 
  case Env -> ModName -> String -> LocSymbol -> Either UserError Var
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Either UserError a
resolveLocSym Env
env ModName
name String
kind LocSymbol
lx of 
    Right Var
v -> Var -> Maybe Var -> Var
forall a. a -> Maybe a -> a
Mb.fromMaybe Var
v       (Env -> LocSymbol -> [Var] -> Maybe Var
lookupLocalVar Env
env LocSymbol
lx [Var
v]) 
    Left  UserError
e -> Var -> Maybe Var -> Var
forall a. a -> Maybe a -> a
Mb.fromMaybe (UserError -> Var
forall a. UserError -> a
err UserError
e) (Env -> LocSymbol -> [Var] -> Maybe Var
lookupLocalVar Env
env LocSymbol
lx []) 
  where
    -- err e   = Misc.errorP "error-lookupGhcVar" (F.showpp (e, F.loc lx, lx))
    err :: UserError -> a
err     = UserError -> a
forall a e. Exception e => e -> a
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 -> [Var] -> Maybe Var
lookupLocalVar Env
env LocSymbol
lx [Var]
gvs = Int -> [(Int, Var)] -> Maybe Var
forall i a. (Ord i, Num i) => i -> [(i, a)] -> Maybe a
Misc.findNearest Int
lxn [(Int, Var)]
kvs
  where 
    _msg :: String
_msg                  = String
"LOOKUP-LOCAL: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Symbol, Int, [(Int, Var)]) -> String
forall a. PPrint a => a -> String
F.showpp (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lx, Int
lxn, [(Int, Var)]
kvs)
    kvs :: [(Int, Var)]
kvs                   = [(Int, Var)]
gs [(Int, Var)] -> [(Int, Var)] -> [(Int, Var)]
forall a. [a] -> [a] -> [a]
++ [(Int, Var)] -> Symbol -> LocalVars -> [(Int, Var)]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] Symbol
x (Env -> LocalVars
reLocalVars Env
env) 
    gs :: [(Int, Var)]
gs                    = [(Var -> Int
forall a. Loc a => a -> Int
F.srcLine Var
v, Var
v) | Var
v <- [Var]
gvs]
    lxn :: Int
lxn                   = LocSymbol -> Int
forall a. Loc a => a -> Int
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 -> Ghc.DataCon 
lookupGhcDataCon :: Env -> ModName -> String -> LocSymbol -> DataCon
lookupGhcDataCon = Env -> ModName -> String -> LocSymbol -> DataCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> a
strictResolveSym 

lookupGhcTyCon :: Env -> ModName -> String -> LocSymbol -> Ghc.TyCon 
lookupGhcTyCon :: Env -> ModName -> String -> LocSymbol -> TyCon
lookupGhcTyCon Env
env ModName
name String
k LocSymbol
lx = String -> TyCon -> 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)) 
                               (TyCon -> TyCon) -> TyCon -> TyCon
forall a b. (a -> b) -> a -> b
$ Env -> ModName -> String -> LocSymbol -> TyCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> a
strictResolveSym Env
env ModName
name String
k LocSymbol
lx

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

lookupGhcDnTyConE :: Env -> ModName -> String -> DataName -> Either UserError Ghc.TyCon
lookupGhcDnTyConE :: Env -> ModName -> String -> DataName -> Either UserError TyCon
lookupGhcDnTyConE Env
env ModName
name String
msg (DnCon  LocSymbol
s) 
  = Env -> ModName -> String -> LocSymbol -> Either UserError 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 -> Either UserError TyCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Either UserError a
resolveLocSym Env
env ModName
name String
msg LocSymbol
s of 
      Right TyCon
r -> TyCon -> Either UserError TyCon
forall a b. b -> Either a b
Right TyCon
r 
      Left  UserError
e -> case Env -> ModName -> String -> LocSymbol -> Either UserError TyCon
lookupGhcDnCon  Env
env ModName
name String
msg LocSymbol
s of 
                   Right TyCon
r -> TyCon -> Either UserError TyCon
forall a b. b -> Either a b
Right TyCon
r 
                   Left  UserError
_ -> UserError -> Either UserError TyCon
forall a b. a -> Either a b
Left  UserError
e

lookupGhcDnCon :: Env -> ModName -> String -> LocSymbol -> Either UserError Ghc.TyCon 
lookupGhcDnCon :: Env -> ModName -> String -> LocSymbol -> Either UserError TyCon
lookupGhcDnCon Env
env ModName
name String
msg = (DataCon -> TyCon)
-> Either UserError DataCon -> Either UserError TyCon
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataCon -> TyCon
Ghc.dataConTyCon (Either UserError DataCon -> Either UserError TyCon)
-> (LocSymbol -> Either UserError DataCon)
-> LocSymbol
-> Either UserError TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ModName -> String -> LocSymbol -> Either UserError DataCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Either UserError 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
-> Either UserError SpecType
ofBareTypeE Env
env ModName
name SourcePos
l Maybe [PVar BSort]
forall a. Maybe a
Nothing BareType
t of 
    Left UserError
e  -> String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
myTracepp (String
"knownType: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (BareType, UserError) -> String
forall a. PPrint a => a -> String
F.showpp (BareType
t, UserError
e)) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Bool
False 
    Right SpecType
_ -> Bool
True 



_rTypeTyCons :: (Ord c) => RType c tv r -> [c]
_rTypeTyCons :: 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 Var -> Bool
forall a. Maybe a -> Bool
Mb.isJust Maybe Var
v 
  where 
    v :: Maybe Ghc.Var -- This annotation is crucial
    v :: Maybe Var
v = String -> Maybe Var -> Maybe Var
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 Var -> Maybe Var) -> Maybe Var -> Maybe Var
forall a b. (a -> b) -> a -> b
$ Env -> ModName -> String -> LocSymbol -> Maybe Var
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 -> Either UserError a 

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

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



resolveWith :: (PPrint a) => PJ.Doc -> (Ghc.TyThing -> Maybe a) -> Env -> ModName -> String -> LocSymbol 
            -> Either UserError a 
resolveWith :: Doc
-> (TyThing -> Maybe a)
-> Env
-> ModName
-> String
-> LocSymbol
-> Either UserError 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
    []  -> UserError -> Either UserError a
forall a b. a -> Either a b
Left  (Doc -> String -> LocSymbol -> UserError
errResolve Doc
kind String
str LocSymbol
lx) 
    [a
x] -> a -> Either UserError a
forall a b. b -> Either a b
Right a
x 
    [a]
xs  -> UserError -> Either UserError a
forall a b. a -> Either a b
Left (UserError -> Either UserError a)
-> UserError -> Either UserError a
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> [Doc] -> UserError
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
    -- oThings = Mb.mapMaybe (\(x, y) -> (x,) <$> f y) things
    _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 :: (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
name 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]
mods ]
    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]
mods)
    (Symbol
x, Maybe [Symbol]
mods)              = 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
name
    allowExt :: Bool
allowExt               = Env -> LocSymbol -> Bool
allowExtResolution Env
env LocSymbol
lsym 
    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], Bool) -> String
forall a. PPrint a => a -> String
F.showpp (LocSymbol
lsym, Symbol
name, Symbol
m, Maybe [Symbol]
mods, Bool
allowExt)) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ 
                               Env -> Symbol -> Symbol -> Bool -> Maybe [Symbol] -> [Int]
matchMod Env
env Symbol
name Symbol
m Bool
allowExt Maybe [Symbol]
mods 

-- | [NOTE:External-Resolution] @allowExtResolution@ determines whether a @LocSymbol@ 
--   can be resolved by a @TyThing@ that is _outside_ the module corresponding to @LocSymbol@. 
--   We need to allow this, e.g. to resolve names like @Data.Set.Set@ with @Data.Set.Internal.Set@, 
--   but should do so ONLY when the LocSymbol comes from a "hand-written" .spec file or 
--   something from the LH prelude. Other names, e.g. from "machine-generated" .bspec files 
--   should already be FULLY-qualified to to their actual definition (e.g. Data.Set.Internal.Set) 
--   and so we should DISALLOW external-resolution in such cases.

allowExtResolution :: Env -> LocSymbol -> Bool 
allowExtResolution :: Env -> LocSymbol -> Bool
allowExtResolution Env
env LocSymbol
lx = case Maybe String
fileMb of 
  Maybe String
Nothing   -> Bool
True 
  Just String
f    -> String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
myTracepp (String
"allowExt: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String, String) -> String
forall a. Show a => a -> String
show (String
f, String
tgtFile)) 
                 (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String
f String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
tgtFile Bool -> Bool -> Bool
|| String -> String -> Bool
Misc.isIncludeFile String
incDir String
f Bool -> Bool -> Bool
|| Ext -> String -> Bool
F.isExtFile Ext
F.Spec String
f 
  where 
    tgtFile :: String
tgtFile = GhcSrc -> String
_giTarget (Env -> GhcSrc
reSrc Env
env)
    incDir :: String
incDir  = GhcSrc -> String
_giIncDir (Env -> GhcSrc
reSrc Env
env)
    fileMb :: Maybe String
fileMb  = SrcSpan -> Maybe String
Errors.srcSpanFileMb (LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSymbol
lx) 

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
Misc.fromFirstMaybes [] (Symbol -> Maybe [(Symbol, TyThing)]
get (Symbol -> Maybe [(Symbol, TyThing)])
-> [Symbol] -> [Maybe [(Symbol, TyThing)]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol
x, 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 -> Bool -> Maybe [F.Symbol] -> [Int]
matchMod :: Env -> Symbol -> Symbol -> Bool -> Maybe [Symbol] -> [Int]
matchMod Env
env Symbol
tgtName Symbol
defName Bool
allowExt = 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
allowExt Bool -> Bool -> Bool
&& 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 (t :: * -> *) a. Foldable t => t a -> Int
length [Text]
parentHierarchy Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Text] -> 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 = 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 = 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 -> UserError 
errResolve :: Doc -> String -> LocSymbol -> UserError
errResolve Doc
k String
msg LocSymbol
lx = SrcSpan -> Doc -> Doc -> Doc -> UserError
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) 

-- symbolicString :: F.Symbolic a => a -> String
-- symbolicString = F.symbolString . F.symbol

-- | @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 -> ModName -> String -> LocSymbol -> a
strictResolveSym Env
env ModName
name String
kind LocSymbol
x = case Env -> ModName -> String -> LocSymbol -> Either UserError a
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Either UserError a
resolveLocSym Env
env ModName
name String
kind LocSymbol
x of 
  Left  UserError
err -> String -> String -> a
forall a. String -> String -> a
Misc.errorP String
"error-strictResolveSym" (UserError -> String
forall a. PPrint a => a -> String
F.showpp UserError
err) -- uError err 
  Right a
val -> a
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 :: Env -> ModName -> String -> LocSymbol -> Maybe a
maybeResolveSym Env
env ModName
name String
kind LocSymbol
x = case Env -> ModName -> String -> LocSymbol -> Either UserError a
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Either UserError a
resolveLocSym Env
env ModName
name String
kind LocSymbol
x of 
  Left  UserError
_   -> 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 = (UserError -> SpecType)
-> (SpecType -> SpecType) -> Either UserError SpecType -> SpecType
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either UserError -> SpecType
forall a. UserError -> a
fail SpecType -> SpecType
forall a. a -> a
id (Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> BareType
-> Either UserError SpecType
ofBareTypeE Env
env ModName
name SourcePos
l Maybe [PVar BSort]
ps BareType
t)
  where 
    fail :: UserError -> a
fail                   = UserError -> 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 -> Either UserError SpecType 
ofBareTypeE :: Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> BareType
-> Either UserError SpecType
ofBareTypeE Env
env ModName
name SourcePos
l Maybe [PVar BSort]
ps BareType
t = Env
-> ModName
-> ([Symbol] -> RReft -> RReft)
-> SourcePos
-> BareType
-> Either UserError SpecType
forall r.
Expandable r =>
Env
-> ModName
-> ([Symbol] -> r -> r)
-> SourcePos
-> BRType r
-> Either UserError (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 :: Reft
ur_reft = CoSub -> Reft -> Reft
coSubReft CoSub
su (RReft -> Reft
forall r. UReft r -> r
ur_reft RReft
r) } 

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


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

ofBSortE :: Env -> ModName -> F.SourcePos -> BSort -> Either UserError RSort 
ofBSortE :: Env -> ModName -> SourcePos -> BSort -> Either UserError RSort
ofBSortE Env
env ModName
name SourcePos
l BSort
t = Env
-> ModName
-> ([Symbol] -> () -> ())
-> SourcePos
-> BSort
-> Either UserError RSort
forall r.
Expandable r =>
Env
-> ModName
-> ([Symbol] -> r -> r)
-> SourcePos
-> BRType r
-> Either UserError (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 -> RSort) -> PVar BSort -> RPVar
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> ModName -> SourcePos -> BSort -> RSort
ofBSort Env
env ModName
name SourcePos
l) 

--------------------------------------------------------------------------------
txParam :: F.SourcePos -> ((UsedPVar -> UsedPVar) -> t) -> [UsedPVar] -> RType c tv r -> t
txParam :: 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 :: [((), Symbol, Expr)]
pargs = [((), Symbol, Expr)]
args' }
  where
    args' :: [((), Symbol, Expr)]
args' | Bool -> Bool
not ([((), Symbol, Expr)] -> 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 :: [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 :: 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 
         -> Either UserError (RRType r)
ofBRType :: Env
-> ModName
-> ([Symbol] -> r -> r)
-> SourcePos
-> BRType r
-> Either UserError (RRType r)
ofBRType Env
env ModName
name [Symbol] -> r -> r
f SourcePos
l BRType r
t  = [Symbol] -> BRType r -> Either UserError (RRType r)
go [] BRType r
t 
  where
    goReft :: [Symbol] -> r -> m r
goReft [Symbol]
bs r
r             = r -> m r
forall (m :: * -> *) a. Monad m => a -> m a
return ([Symbol] -> r -> r
f [Symbol]
bs r
r) 
    goRImpF :: [Symbol]
-> Symbol
-> BRType r
-> BRType r
-> r
-> Either UserError (RRType r)
goRImpF [Symbol]
bs Symbol
x BRType r
t1 BRType r
t2 r
r    = Symbol -> RRType r -> RRType r -> r -> RRType r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RImpF Symbol
x (RRType r -> RRType r -> r -> RRType r)
-> Either UserError (RRType r)
-> Either UserError (RRType r -> r -> RRType r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Symbol -> RRType r -> RRType r
forall r c tv.
(Reftable r, TyConable c) =>
Symbol -> RType c tv r -> RType c tv r
rebind Symbol
x (RRType r -> RRType r)
-> Either UserError (RRType r) -> Either UserError (RRType r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> BRType r -> Either UserError (RRType r)
go [Symbol]
bs BRType r
t1) Either UserError (RRType r -> r -> RRType r)
-> Either UserError (RRType r) -> Either UserError (r -> RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> BRType r -> Either UserError (RRType r)
go (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
bs) BRType r
t2 Either UserError (r -> RRType r)
-> Either UserError r -> Either UserError (RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either UserError r
forall (m :: * -> *). Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
    goRFun :: [Symbol]
-> Symbol
-> BRType r
-> BRType r
-> r
-> Either UserError (RRType r)
goRFun  [Symbol]
bs Symbol
x BRType r
t1 BRType r
t2 r
r    = Symbol -> RRType r -> RRType r -> r -> RRType r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun  Symbol
x (RRType r -> RRType r -> r -> RRType r)
-> Either UserError (RRType r)
-> Either UserError (RRType r -> r -> RRType r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Symbol -> RRType r -> RRType r
forall r c tv.
(Reftable r, TyConable c) =>
Symbol -> RType c tv r -> RType c tv r
rebind Symbol
x (RRType r -> RRType r)
-> Either UserError (RRType r) -> Either UserError (RRType r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> BRType r -> Either UserError (RRType r)
go [Symbol]
bs BRType r
t1) Either UserError (RRType r -> r -> RRType r)
-> Either UserError (RRType r) -> Either UserError (r -> RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> BRType r -> Either UserError (RRType r)
go (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
bs) BRType r
t2 Either UserError (r -> RRType r)
-> Either UserError r -> Either UserError (RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either UserError 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] -> BRType r -> Either UserError (RRType r)
go [Symbol]
bs (RAppTy BRType r
t1 BRType r
t2 r
r)  = RRType r -> RRType r -> r -> RRType r
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy (RRType r -> RRType r -> r -> RRType r)
-> Either UserError (RRType r)
-> Either UserError (RRType r -> r -> RRType r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> BRType r -> Either UserError (RRType r)
go [Symbol]
bs BRType r
t1 Either UserError (RRType r -> r -> RRType r)
-> Either UserError (RRType r) -> Either UserError (r -> RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> BRType r -> Either UserError (RRType r)
go [Symbol]
bs BRType r
t2 Either UserError (r -> RRType r)
-> Either UserError r -> Either UserError (RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either UserError r
forall (m :: * -> *). Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
    go [Symbol]
bs (RApp BTyCon
tc [BRType r]
ts [RTProp BTyCon BTyVar r]
rs r
r) = [Symbol]
-> BTyCon
-> [BRType r]
-> [RTProp BTyCon BTyVar r]
-> r
-> Either UserError (RRType r)
goRApp [Symbol]
bs BTyCon
tc [BRType r]
ts [RTProp BTyCon BTyVar r]
rs r
r 
    go [Symbol]
bs (RImpF Symbol
x BRType r
t1 BRType r
t2 r
r) = [Symbol]
-> Symbol
-> BRType r
-> BRType r
-> r
-> Either UserError (RRType r)
goRImpF [Symbol]
bs Symbol
x BRType r
t1 BRType r
t2 r
r 
    go [Symbol]
bs (RFun  Symbol
x BRType r
t1 BRType r
t2 r
r) = [Symbol]
-> Symbol
-> BRType r
-> BRType r
-> r
-> Either UserError (RRType r)
goRFun  [Symbol]
bs Symbol
x BRType r
t1 BRType r
t2 r
r 
    go [Symbol]
bs (RVar BTyVar
a r
r)        = RTyVar -> r -> RRType r
forall c tv r. tv -> r -> RType c tv r
RVar (BTyVar -> RTyVar
RT.bareRTyVar BTyVar
a) (r -> RRType r)
-> Either UserError r -> Either UserError (RRType r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> r -> Either UserError r
forall (m :: * -> *). Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
    go [Symbol]
bs (RAllT RTVU BTyCon BTyVar
a BRType r
t r
r)     = RTVU RTyCon RTyVar -> RRType r -> r -> RRType r
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU RTyCon RTyVar
forall s2. RTVar RTyVar s2
a' (RRType r -> r -> RRType r)
-> Either UserError (RRType r) -> Either UserError (r -> RRType r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> BRType r -> Either UserError (RRType r)
go [Symbol]
bs BRType r
t Either UserError (r -> RRType r)
-> Either UserError r -> Either UserError (RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either UserError 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 BRType r
t)       = RPVar -> RRType r -> RRType r
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP RPVar
a' (RRType r -> RRType r)
-> Either UserError (RRType r) -> Either UserError (RRType r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> BRType r -> Either UserError (RRType r)
go [Symbol]
bs BRType 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 BRType r
t1 BRType r
t2)   = Symbol -> RRType r -> RRType r -> RRType r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
x  (RRType r -> RRType r -> RRType r)
-> Either UserError (RRType r)
-> Either UserError (RRType r -> RRType r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> BRType r -> Either UserError (RRType r)
go [Symbol]
bs BRType r
t1    Either UserError (RRType r -> RRType r)
-> Either UserError (RRType r) -> Either UserError (RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> BRType r -> Either UserError (RRType r)
go [Symbol]
bs BRType r
t2
    go [Symbol]
bs (REx Symbol
x BRType r
t1 BRType r
t2)     = Symbol -> RRType r -> RRType r -> RRType r
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx   Symbol
x  (RRType r -> RRType r -> RRType r)
-> Either UserError (RRType r)
-> Either UserError (RRType r -> RRType r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> BRType r -> Either UserError (RRType r)
go [Symbol]
bs BRType r
t1    Either UserError (RRType r -> RRType r)
-> Either UserError (RRType r) -> Either UserError (RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> BRType r -> Either UserError (RRType r)
go (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
bs) BRType r
t2
    go [Symbol]
bs (RRTy [(Symbol, BRType r)]
xts r
r Oblig
o BRType r
t)  = [(Symbol, RRType r)] -> r -> Oblig -> RRType r -> RRType r
forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy  ([(Symbol, RRType r)] -> r -> Oblig -> RRType r -> RRType r)
-> Either UserError [(Symbol, RRType r)]
-> Either UserError (r -> Oblig -> RRType r -> RRType r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either UserError [(Symbol, RRType r)]
xts' Either UserError (r -> Oblig -> RRType r -> RRType r)
-> Either UserError r
-> Either UserError (Oblig -> RRType r -> RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Symbol] -> r -> Either UserError r
forall (m :: * -> *). Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r) Either UserError (Oblig -> RRType r -> RRType r)
-> Either UserError Oblig
-> Either UserError (RRType r -> RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Oblig -> Either UserError Oblig
forall (f :: * -> *) a. Applicative f => a -> f a
pure Oblig
o) Either UserError (RRType r -> RRType r)
-> Either UserError (RRType r) -> Either UserError (RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> BRType r -> Either UserError (RRType r)
go [Symbol]
bs BRType r
t
      where xts' :: Either UserError [(Symbol, RRType r)]
xts'            = ((Symbol, BRType r) -> Either UserError (Symbol, RRType r))
-> [(Symbol, BRType r)] -> Either UserError [(Symbol, RRType r)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((BRType r -> Either UserError (RRType r))
-> (Symbol, BRType r) -> Either UserError (Symbol, RRType r)
forall (m :: * -> *) b c a.
Applicative m =>
(b -> m c) -> (a, b) -> m (a, c)
Misc.mapSndM ([Symbol] -> BRType r -> Either UserError (RRType r)
go [Symbol]
bs)) [(Symbol, BRType r)]
xts
    go [Symbol]
bs (RHole r
r)         = r -> RRType r
forall c tv r. r -> RType c tv r
RHole    (r -> RRType r)
-> Either UserError r -> Either UserError (RRType r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> r -> Either UserError r
forall (m :: * -> *). Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
    go [Symbol]
bs (RExprArg Located Expr
le)     = RRType r -> Either UserError (RRType r)
forall (m :: * -> *) a. Monad m => a -> m a
return    (RRType r -> Either UserError (RRType r))
-> RRType r -> Either UserError (RRType r)
forall a b. (a -> b) -> a -> b
$ Located Expr -> RRType 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 UserError (RTProp RTyCon RTyVar r)
goRef [Symbol]
bs (RProp [(Symbol, BSort)]
ss (RHole r
r)) = [(Symbol, RSort)] -> r -> RTProp RTyCon RTyVar r
forall τ r c tv. [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
rPropP ([(Symbol, RSort)] -> r -> RTProp RTyCon RTyVar r)
-> Either UserError [(Symbol, RSort)]
-> Either UserError (r -> RTProp RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (((Symbol, BSort) -> Either UserError (Symbol, RSort))
-> [(Symbol, BSort)] -> Either UserError [(Symbol, RSort)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Symbol, BSort) -> Either UserError (Symbol, RSort)
forall t. (t, BSort) -> Either UserError (t, RSort)
goSyms [(Symbol, BSort)]
ss) Either UserError (r -> RTProp RTyCon RTyVar r)
-> Either UserError r -> Either UserError (RTProp RTyCon RTyVar r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either UserError r
forall (m :: * -> *). Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
    goRef [Symbol]
bs (RProp [(Symbol, BSort)]
ss BRType r
t)         = [(Symbol, RSort)] -> RRType r -> RTProp RTyCon RTyVar r
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp  ([(Symbol, RSort)] -> RRType r -> RTProp RTyCon RTyVar r)
-> Either UserError [(Symbol, RSort)]
-> Either UserError (RRType r -> RTProp RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (((Symbol, BSort) -> Either UserError (Symbol, RSort))
-> [(Symbol, BSort)] -> Either UserError [(Symbol, RSort)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Symbol, BSort) -> Either UserError (Symbol, RSort)
forall t. (t, BSort) -> Either UserError (t, RSort)
goSyms [(Symbol, BSort)]
ss) Either UserError (RRType r -> RTProp RTyCon RTyVar r)
-> Either UserError (RRType r)
-> Either UserError (RTProp RTyCon RTyVar r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> BRType r -> Either UserError (RRType r)
go [Symbol]
bs BRType r
t
    goSyms :: (t, BSort) -> Either UserError (t, RSort)
goSyms (t
x, BSort
t)                 = (t
x,) (RSort -> (t, RSort))
-> Either UserError RSort -> Either UserError (t, RSort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> ModName -> SourcePos -> BSort -> Either UserError RSort
ofBSortE Env
env ModName
name SourcePos
l BSort
t 
    goRApp :: [Symbol]
-> BTyCon
-> [BRType r]
-> [RTProp BTyCon BTyVar r]
-> r
-> Either UserError (RRType r)
goRApp [Symbol]
bs BTyCon
tc [BRType r]
ts [RTProp BTyCon BTyVar r]
rs r
r          = r
-> Located TyCon
-> [RTProp RTyCon RTyVar r]
-> [RRType r]
-> RRType 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]
 -> [RRType r]
 -> RRType r)
-> Either UserError r
-> Either
     UserError
     (Located TyCon
      -> [RTProp RTyCon RTyVar r] -> [RRType r] -> RRType r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> r -> Either UserError r
forall (m :: * -> *). Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r Either
  UserError
  (Located TyCon
   -> [RTProp RTyCon RTyVar r] -> [RRType r] -> RRType r)
-> Either UserError (Located TyCon)
-> Either
     UserError ([RTProp RTyCon RTyVar r] -> [RRType r] -> RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Either UserError (Located TyCon)
lc' Either
  UserError ([RTProp RTyCon RTyVar r] -> [RRType r] -> RRType r)
-> Either UserError [RTProp RTyCon RTyVar r]
-> Either UserError ([RRType r] -> RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (RTProp BTyCon BTyVar r
 -> Either UserError (RTProp RTyCon RTyVar r))
-> [RTProp BTyCon BTyVar r]
-> Either UserError [RTProp RTyCon RTyVar r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Symbol]
-> RTProp BTyCon BTyVar r
-> Either UserError (RTProp RTyCon RTyVar r)
goRef [Symbol]
bs) [RTProp BTyCon BTyVar r]
rs Either UserError ([RRType r] -> RRType r)
-> Either UserError [RRType r] -> Either UserError (RRType r)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (BRType r -> Either UserError (RRType r))
-> [BRType r] -> Either UserError [RRType r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Symbol] -> BRType r -> Either UserError (RRType r)
go [Symbol]
bs) [BRType r]
ts
      where
        lc' :: Either UserError (Located TyCon)
lc'                    = LocSymbol -> TyCon -> Located TyCon
forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
lc (TyCon -> Located TyCon)
-> Either UserError TyCon -> Either UserError (Located TyCon)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> ModName -> LocSymbol -> Int -> Either UserError TyCon
matchTyCon Env
env ModName
name LocSymbol
lc ([BRType r] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [BRType 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 -> Either UserError Ghc.TyCon
matchTyCon :: Env -> ModName -> LocSymbol -> Int -> Either UserError 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 -> Either UserError TyCon
forall a b. b -> Either a b
Right TyCon
Ghc.listTyCon
  | Symbol -> Bool
forall c. TyConable c => c -> Bool
isTuple Symbol
c               = TyCon -> Either UserError TyCon
forall a b. b -> Either a b
Right TyCon
tuplTc 
  | Bool
otherwise               = Env -> ModName -> String -> LocSymbol -> Either UserError TyCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Either UserError 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 :: 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 (t :: * -> *) a. Foldable t => t a -> Int
length [RType RTyCon RTyVar r]
ts) 
      then UserError -> RType RTyCon RTyVar r
forall a e. Exception e => e -> a
Ex.throw UserError
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, RSort, 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.subsTyVars_meet [(RTyVar, RSort, 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 :: [Var]
tvs = [ Var
v | (Var
v, TyConBinder
b) <- [Var] -> [TyConBinder] -> [(Var, TyConBinder)]
forall a b. [a] -> [b] -> [(a, b)]
zip (TyCon -> [Var]
GM.tyConTyVarsDef TyCon
c) (TyCon -> [TyConBinder]
Ghc.tyConBinders TyCon
c), TyConBinder -> Bool
GM.isAnonBinder TyConBinder
b]
       su :: [(RTyVar, RSort, RType RTyCon RTyVar r)]
su  = (Var
 -> RType RTyCon RTyVar r -> (RTyVar, RSort, RType RTyCon RTyVar r))
-> [Var]
-> [RType RTyCon RTyVar r]
-> [(RTyVar, RSort, RType RTyCon RTyVar r)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Var
a RType RTyCon RTyVar r
t -> (Var -> RTyVar
RT.rTyVar Var
a, RType RTyCon RTyVar r -> RSort
forall c tv r. RType c tv r -> RType c tv ()
toRSort RType RTyCon RTyVar r
t, RType RTyCon RTyVar r
t)) [Var]
tvs [RType RTyCon RTyVar r]
ts
       nts :: Int
nts = [Var] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
tvs

       err :: UserError
       err :: UserError
err = SrcSpan -> Doc -> SrcSpan -> Doc -> UserError
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 (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 :: 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 -> RType c tv r) -> String -> RType c tv r
forall a b. (a -> b) -> a -> b
$ String
"Bare.Type.tyApp on invalid inputs"

expandRTypeSynonyms :: (Expandable r) => RRType r -> RRType r
expandRTypeSynonyms :: 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
. RRType r -> Type
forall r. ToTypeable r => RRType r -> Type
RT.toType

{- 
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
r)
  = 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
r'
  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 (t :: * -> *) a. Foldable t => t a -> Int
length [RPVar]
pvs) [RTProp RTyCon RTyVar RReft]
rs
    r' :: RReft
r'                 = (RReft -> RTProp RTyCon RTyVar RReft -> RReft)
-> RReft -> [RTProp RTyCon RTyVar RReft] -> RReft
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
r [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 :: 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' :: SrcSpan
-> s
-> Int
-> RPVar
-> RTProp RTyCon RTyVar RReft
-> RTProp RTyCon RTyVar RReft
addSymSortRef' SrcSpan
_ s
_ Int
_ RPVar
p (RProp [(Symbol, RSort)]
s (RVar RTyVar
v RReft
r)) | RTyVar -> Bool
forall a. Symbolic a => a -> Bool
isDummy RTyVar
v
  = [(Symbol, RSort)] -> SpecType -> RTProp RTyCon RTyVar RReft
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RSort)]
xs SpecType
t
    where
      t :: SpecType
t  = RSort -> SpecType
forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort (RPVar -> RSort
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, RSort)]
xs = String -> [(Symbol, RSort)] -> RPVar -> [(Symbol, RSort)]
forall b t. String -> [(Symbol, b)] -> PVar t -> [(Symbol, t)]
spliceArgs String
"addSymSortRef 1" [(Symbol, RSort)]
s RPVar
p

addSymSortRef' SrcSpan
sp s
rc Int
i RPVar
p (RProp [(Symbol, RSort)]
_ (RHole r :: RReft
r@(MkUReft Reft
_ (Pr [UsedPVar
up]))))
  | [Symbol] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [RSort] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RSort]
ts
  = [(Symbol, RSort)] -> SpecType -> RTProp RTyCon RTyVar RReft
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RSort)]
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 (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
xs) ([RSort] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RSort]
ts)
    where
      xts :: [(Symbol, RSort)]
xts = String -> [Symbol] -> [RSort] -> [(Symbol, RSort)]
forall t t1. String -> [t] -> [t1] -> [(t, t1)]
Misc.safeZipWithError String
"addSymSortRef'" [Symbol]
xs [RSort]
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 :: [RSort]
ts  = (RSort, Symbol, Expr) -> RSort
forall a b c. (a, b, c) -> a
Misc.fst3 ((RSort, Symbol, Expr) -> RSort)
-> [(RSort, Symbol, Expr)] -> [RSort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RPVar -> [(RSort, Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs RPVar
p

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

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

spliceArgs :: String  -> [(F.Symbol, b)] -> PVar t -> [(F.Symbol, t)]
spliceArgs :: String -> [(Symbol, b)] -> PVar t -> [(Symbol, t)]
spliceArgs String
msg [(Symbol, b)]
s 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)]
s) (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
-> [(Var, LocBareType, Maybe [Located Expr])]
-> [(Var, LocBareType, Maybe [Located Expr])]
resolveLocalBinds Env
env [(Var, LocBareType, Maybe [Located Expr])]
xtes = [ (Var
x,LocBareType
t,Maybe [Located Expr]
es) | (Var
x, (LocBareType
t, Maybe [Located Expr]
es)) <- [(Var, (LocBareType, Maybe [Located Expr]))]
topTs [(Var, (LocBareType, Maybe [Located Expr]))]
-> [(Var, (LocBareType, Maybe [Located Expr]))]
-> [(Var, (LocBareType, Maybe [Located Expr]))]
forall a. [a] -> [a] -> [a]
++ [(Var, (LocBareType, Maybe [Located Expr]))]
-> [(Var, (LocBareType, Maybe [Located Expr]))]
replace [(Var, (LocBareType, Maybe [Located Expr]))]
locTs ]
  where 
    ([(Var, (LocBareType, Maybe [Located Expr]))]
locTs, [(Var, (LocBareType, Maybe [Located Expr]))]
topTs)         = [(Var, (LocBareType, Maybe [Located Expr]))]
-> ([(Var, (LocBareType, Maybe [Located Expr]))],
    [(Var, (LocBareType, Maybe [Located Expr]))])
forall a. [(Var, a)] -> ([(Var, a)], [(Var, a)])
partitionLocalBinds [ (Var
x, (LocBareType
t, Maybe [Located Expr]
es)) | (Var
x, LocBareType
t, Maybe [Located Expr]
es) <- [(Var, LocBareType, Maybe [Located Expr])]
xtes] 
    replace :: [(Var, (LocBareType, Maybe [Located Expr]))]
-> [(Var, (LocBareType, Maybe [Located Expr]))]
replace                = HashMap Var (LocBareType, Maybe [Located Expr])
-> [(Var, (LocBareType, Maybe [Located Expr]))]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Var (LocBareType, Maybe [Located Expr])
 -> [(Var, (LocBareType, Maybe [Located Expr]))])
-> ([(Var, (LocBareType, Maybe [Located Expr]))]
    -> HashMap Var (LocBareType, Maybe [Located Expr]))
-> [(Var, (LocBareType, Maybe [Located Expr]))]
-> [(Var, (LocBareType, Maybe [Located Expr]))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap Var (LocBareType, Maybe [Located Expr])
-> HashMap Var (LocBareType, Maybe [Located Expr])
replaceSigs (HashMap Var (LocBareType, Maybe [Located Expr])
 -> HashMap Var (LocBareType, Maybe [Located Expr]))
-> ([(Var, (LocBareType, Maybe [Located Expr]))]
    -> HashMap Var (LocBareType, Maybe [Located Expr]))
-> [(Var, (LocBareType, Maybe [Located Expr]))]
-> HashMap Var (LocBareType, Maybe [Located Expr])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Var, (LocBareType, Maybe [Located Expr]))]
-> HashMap Var (LocBareType, Maybe [Located Expr])
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList 
    replaceSigs :: HashMap Var (LocBareType, Maybe [Located Expr])
-> HashMap Var (LocBareType, Maybe [Located Expr])
replaceSigs HashMap Var (LocBareType, Maybe [Located Expr])
sigm       = CoreVisitor
  SymMap (HashMap Var (LocBareType, Maybe [Located Expr]))
-> SymMap
-> HashMap Var (LocBareType, Maybe [Located Expr])
-> [CoreBind]
-> HashMap Var (LocBareType, Maybe [Located Expr])
forall env acc.
CoreVisitor env acc -> env -> acc -> [CoreBind] -> acc
coreVisitor CoreVisitor
  SymMap (HashMap Var (LocBareType, Maybe [Located Expr]))
replaceVisitor SymMap
forall k v. HashMap k v
M.empty HashMap Var (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 Var (LocBareType, Maybe [Located Expr]))
replaceVisitor = CoreVisitor :: forall env acc.
(env -> Var -> env)
-> (env -> acc -> Var -> acc)
-> (env -> acc -> Expr Var -> acc)
-> CoreVisitor env acc
CoreVisitor 
  { envF :: SymMap -> Var -> SymMap
envF  = SymMap -> Var -> SymMap
addBind
  , bindF :: SymMap
-> HashMap Var (LocBareType, Maybe [Located Expr])
-> Var
-> HashMap Var (LocBareType, Maybe [Located Expr])
bindF = SymMap
-> HashMap Var (LocBareType, Maybe [Located Expr])
-> Var
-> HashMap Var (LocBareType, Maybe [Located Expr])
updSigMap
  , exprF :: SymMap
-> HashMap Var (LocBareType, Maybe [Located Expr])
-> Expr Var
-> HashMap Var (LocBareType, Maybe [Located Expr])
exprF = \SymMap
_ HashMap Var (LocBareType, Maybe [Located Expr])
m Expr Var
_ -> HashMap Var (LocBareType, Maybe [Located Expr])
m 
  }

addBind :: SymMap -> Ghc.Var -> SymMap 
addBind :: SymMap -> Var -> SymMap
addBind SymMap
env Var
v = case Var -> Maybe Symbol
localKey Var
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 (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
v) SymMap
env 
  Maybe Symbol
Nothing -> SymMap
env
    
updSigMap :: SymMap -> SigMap -> Ghc.Var -> SigMap 
updSigMap :: SymMap
-> HashMap Var (LocBareType, Maybe [Located Expr])
-> Var
-> HashMap Var (LocBareType, Maybe [Located Expr])
updSigMap SymMap
env HashMap Var (LocBareType, Maybe [Located Expr])
m Var
v = case Var
-> HashMap Var (LocBareType, Maybe [Located Expr])
-> Maybe (LocBareType, Maybe [Located Expr])
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Var
v HashMap Var (LocBareType, Maybe [Located Expr])
m of 
  Maybe (LocBareType, Maybe [Located Expr])
Nothing  -> HashMap Var (LocBareType, Maybe [Located Expr])
m 
  Just (LocBareType, Maybe [Located Expr])
tes -> Var
-> (LocBareType, Maybe [Located Expr])
-> HashMap Var (LocBareType, Maybe [Located Expr])
-> HashMap Var (LocBareType, Maybe [Located Expr])
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Var
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]
++ Var -> String
forall a. Outputable a => a -> String
GM.showPpr Var
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 Var (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 :: [(Var, a)] -> ([(Var, a)], [(Var, a)])
partitionLocalBinds = ((Var, a) -> Bool) -> [(Var, a)] -> ([(Var, a)], [(Var, a)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (Maybe Symbol -> Bool
forall a. Maybe a -> Bool
Mb.isJust (Maybe Symbol -> Bool)
-> ((Var, a) -> Maybe Symbol) -> (Var, a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Maybe Symbol
localKey (Var -> Maybe Symbol)
-> ((Var, a) -> Var) -> (Var, a) -> Maybe Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, a) -> Var
forall a b. (a, b) -> a
fst)