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

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

module Language.Haskell.Liquid.Bare.Resolve
  ( -- * Creating the Environment
    makeEnv
  , makeLocalVars
  , makeGHCTyLookupEnv
  , GHCTyLookupEnv(..)

    -- * Resolving symbols
  , Lookup

  -- * Looking up names
  , lookupGhcDataConLHName
  , lookupGhcDnTyCon
  , lookupGhcIdLHName
  , lookupLocalVar
  , lookupGhcTyConLHName
  , lookupGhcTyThingFromName
  , lookupGhcId

  -- * Checking if names exist
  , knownGhcType

  -- * Misc
  , coSubRReft
  , unQualifySymbol

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

  -- * Post-processing types
  , txRefSort
  , errResolve

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

import qualified Control.Exception                 as Ex
import           Data.Bifunctor (first)
import           Data.Function (on)
import           Data.IORef (newIORef)
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           GHC.Stack
import           Text.Megaparsec.Pos (sourceColumn, sourceLine)
import qualified Text.PrettyPrint.HughesPJ         as PJ

import qualified Language.Fixpoint.Types               as F
import qualified Language.Fixpoint.Types.Visitor       as F
import qualified Language.Fixpoint.Misc                as Misc
import qualified Liquid.GHC.API       as Ghc
import qualified Language.Haskell.Liquid.GHC.Interface as Interface
import qualified Language.Haskell.Liquid.GHC.Misc      as GM
import qualified Language.Haskell.Liquid.Misc          as Misc
import           Language.Haskell.Liquid.Types.DataDecl
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Names
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import qualified Language.Haskell.Liquid.Types.RefType as RT
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Types.Visitors
import           Language.Haskell.Liquid.Bare.Types
import           Language.Haskell.Liquid.UX.Config
import           System.IO.Unsafe (unsafePerformIO)

myTracepp :: (F.PPrint a) => String -> a -> a
myTracepp :: forall a. PPrint a => [Char] -> a -> a
myTracepp = [Char] -> a -> a
forall a. PPrint a => [Char] -> a -> a
F.notracepp

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

-------------------------------------------------------------------------------
-- | Creating an environment
-------------------------------------------------------------------------------
makeEnv :: Config -> GHCTyLookupEnv -> [Ghc.Id] -> Ghc.TcGblEnv -> Ghc.InstEnvs -> LocalVars -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> Env
makeEnv :: Config
-> GHCTyLookupEnv
-> [Var]
-> TcGblEnv
-> InstEnvs
-> LocalVars
-> GhcSrc
-> LogicMap
-> [(ModName, BareSpec)]
-> Env
makeEnv Config
cfg GHCTyLookupEnv
ghcTyLookupEnv [Var]
dataConIds TcGblEnv
tcg InstEnvs
instEnv LocalVars
localVars GhcSrc
src LogicMap
lmap [(ModName, BareSpec)]
specs = RE
  { reTyLookupEnv :: GHCTyLookupEnv
reTyLookupEnv = GHCTyLookupEnv
ghcTyLookupEnv
  , reTcGblEnv :: TcGblEnv
reTcGblEnv  = TcGblEnv
tcg
  , reInstEnvs :: InstEnvs
reInstEnvs = InstEnvs
instEnv
  , reUsedExternals :: NameSet
reUsedExternals = NameSet
usedExternals
  , reLMap :: LogicMap
reLMap      = LogicMap
lmap
  , reDataConIds :: [Var]
reDataConIds = [Var]
dataConIds
  , reLocalVars :: LocalVars
reLocalVars = LocalVars
localVars
  , 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
    usedExternals :: NameSet
usedExternals = [CoreExpr] -> NameSet
Ghc.exprsOrphNames ([CoreExpr] -> NameSet) -> [CoreExpr] -> NameSet
forall a b. (a -> b) -> a -> b
$ ((Var, CoreExpr) -> CoreExpr) -> [(Var, CoreExpr)] -> [CoreExpr]
forall a b. (a -> b) -> [a] -> [b]
map (Var, CoreExpr) -> CoreExpr
forall a b. (a, b) -> b
snd ([(Var, CoreExpr)] -> [CoreExpr])
-> [(Var, CoreExpr)] -> [CoreExpr]
forall a b. (a -> b) -> a -> b
$ [Bind Var] -> [(Var, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
Ghc.flattenBinds ([Bind Var] -> [(Var, CoreExpr)])
-> [Bind Var] -> [(Var, CoreExpr)]
forall a b. (a -> b) -> a -> b
$ GhcSrc -> [Bind Var]
_giCbs 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
$ (MeasureV Symbol LocBareType (Located LHName) -> Symbol
forall {v} {ty} {ctor}. MeasureV v ty ctor -> Symbol
mbName (MeasureV Symbol LocBareType (Located LHName) -> Symbol)
-> [MeasureV Symbol LocBareType (Located LHName)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [MeasureV Symbol LocBareType (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
measures  BareSpec
spec)
      [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (MeasureV Symbol LocBareType () -> Symbol
forall {v} {ty} {ctor}. MeasureV v ty ctor -> Symbol
mbName (MeasureV Symbol LocBareType () -> Symbol)
-> [MeasureV Symbol LocBareType ()] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [MeasureV Symbol LocBareType ()]
forall lname ty. Spec lname ty -> [MeasureV lname (Located ty) ()]
cmeasures BareSpec
spec)
      [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (MeasureV Symbol LocBareType (Located LHName) -> Symbol
forall {v} {ty} {ctor}. MeasureV v ty ctor -> Symbol
mbName (MeasureV Symbol LocBareType (Located LHName) -> Symbol)
-> [MeasureV Symbol LocBareType (Located LHName)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [MeasureV Symbol LocBareType (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
imeasures BareSpec
spec)
      [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (MeasureV Symbol LocBareType (Located LHName) -> Symbol
forall {v} {ty} {ctor}. MeasureV v ty ctor -> Symbol
mbName (MeasureV Symbol LocBareType (Located LHName) -> Symbol)
-> [MeasureV Symbol LocBareType (Located LHName)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [MeasureV Symbol LocBareType (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
omeasures BareSpec
spec)
  where
    mbName :: MeasureV v ty ctor -> Symbol
mbName = LHName -> Symbol
lhNameToResolvedSymbol (LHName -> Symbol)
-> (MeasureV v ty ctor -> LHName) -> MeasureV v ty ctor -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located LHName -> LHName
forall a. Located a -> a
F.val (Located LHName -> LHName)
-> (MeasureV v ty ctor -> Located LHName)
-> MeasureV v ty ctor
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MeasureV v ty ctor -> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName

makeLocalVars :: [Ghc.CoreBind] -> LocalVars
makeLocalVars :: [Bind Var] -> LocalVars
makeLocalVars = [LocalVarDetails] -> LocalVars
localVarMap ([LocalVarDetails] -> LocalVars)
-> ([Bind Var] -> [LocalVarDetails]) -> [Bind Var] -> LocalVars
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Bind Var] -> [LocalVarDetails]
localBinds

-- TODO: rewrite using CoreVisitor
localBinds :: [Ghc.CoreBind] -> [LocalVarDetails]
localBinds :: [Bind Var] -> [LocalVarDetails]
localBinds                    = (Bind Var -> [LocalVarDetails]) -> [Bind Var] -> [LocalVarDetails]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Var] -> Bind Var -> [LocalVarDetails]
bgoT [])
  where
    bgoT :: [Var] -> Bind Var -> [LocalVarDetails]
bgoT [Var]
g (Ghc.NonRec Var
_ CoreExpr
e) = [Var] -> CoreExpr -> [LocalVarDetails]
go [Var]
g CoreExpr
e
    bgoT [Var]
g (Ghc.Rec [(Var, CoreExpr)]
xes)    = ((Var, CoreExpr) -> [LocalVarDetails])
-> [(Var, CoreExpr)] -> [LocalVarDetails]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Var] -> CoreExpr -> [LocalVarDetails]
go [Var]
g (CoreExpr -> [LocalVarDetails])
-> ((Var, CoreExpr) -> CoreExpr)
-> (Var, CoreExpr)
-> [LocalVarDetails]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, CoreExpr) -> CoreExpr
forall a b. (a, b) -> b
snd) [(Var, CoreExpr)]
xes
    pgo :: [Var] -> Bool -> (Var, CoreExpr) -> [LocalVarDetails]
pgo [Var]
g Bool
isRec (Var
x, CoreExpr
e)      = [Var] -> Bool -> Var -> LocalVarDetails
mkLocalVarDetails [Var]
g Bool
isRec Var
x LocalVarDetails -> [LocalVarDetails] -> [LocalVarDetails]
forall a. a -> [a] -> [a]
: [Var] -> CoreExpr -> [LocalVarDetails]
go [Var]
g CoreExpr
e
    bgo :: [Var] -> Bind Var -> [LocalVarDetails]
bgo [Var]
g (Ghc.NonRec Var
x CoreExpr
e)  = [Var] -> Bool -> (Var, CoreExpr) -> [LocalVarDetails]
pgo [Var]
g Bool
False (Var
x, CoreExpr
e)
    bgo [Var]
g (Ghc.Rec [(Var, CoreExpr)]
xes)     = ((Var, CoreExpr) -> [LocalVarDetails])
-> [(Var, CoreExpr)] -> [LocalVarDetails]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Var] -> Bool -> (Var, CoreExpr) -> [LocalVarDetails]
pgo [Var]
g Bool
True) [(Var, CoreExpr)]
xes
    go :: [Var] -> CoreExpr -> [LocalVarDetails]
go [Var]
g (Ghc.App CoreExpr
e CoreExpr
a)       = (CoreExpr -> [LocalVarDetails]) -> [CoreExpr] -> [LocalVarDetails]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Var] -> CoreExpr -> [LocalVarDetails]
go [Var]
g) [CoreExpr
e, CoreExpr
a]
    go [Var]
g (Ghc.Lam Var
x CoreExpr
e)       = [Var] -> CoreExpr -> [LocalVarDetails]
go (Var
xVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
g) CoreExpr
e
    go [Var]
g (Ghc.Let Bind Var
b CoreExpr
e)       = [Var] -> Bind Var -> [LocalVarDetails]
bgo [Var]
g Bind Var
b [LocalVarDetails] -> [LocalVarDetails] -> [LocalVarDetails]
forall a. [a] -> [a] -> [a]
++ [Var] -> CoreExpr -> [LocalVarDetails]
go (Bind Var -> [Var]
forall b. Bind b -> [b]
Ghc.bindersOf Bind Var
b [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var]
g) CoreExpr
e
    go [Var]
g (Ghc.Tick CoreTickish
_ CoreExpr
e)      = [Var] -> CoreExpr -> [LocalVarDetails]
go [Var]
g CoreExpr
e
    go [Var]
g (Ghc.Cast CoreExpr
e CoercionR
_)      = [Var] -> CoreExpr -> [LocalVarDetails]
go [Var]
g CoreExpr
e
    go [Var]
g (Ghc.Case CoreExpr
e Var
_ Type
_ [Alt Var]
cs) = [Var] -> CoreExpr -> [LocalVarDetails]
go [Var]
g CoreExpr
e [LocalVarDetails] -> [LocalVarDetails] -> [LocalVarDetails]
forall a. [a] -> [a] -> [a]
++ (Alt Var -> [LocalVarDetails]) -> [Alt Var] -> [LocalVarDetails]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(Ghc.Alt AltCon
_ [Var]
bs CoreExpr
e') -> [Var] -> CoreExpr -> [LocalVarDetails]
go ([Var]
bs [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var]
g) CoreExpr
e') [Alt Var]
cs
    go [Var]
_ (Ghc.Var Var
_)         = []
    go [Var]
_ CoreExpr
_                   = []

    mkLocalVarDetails :: [Var] -> Bool -> Var -> LocalVarDetails
mkLocalVarDetails [Var]
g Bool
isRec Var
v = LocalVarDetails
      { lvdSourcePos :: SourcePos
lvdSourcePos = SrcSpan -> SourcePos
F.sp_start (SrcSpan -> SourcePos) -> SrcSpan -> SourcePos
forall a b. (a -> b) -> a -> b
$ Var -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan Var
v
      , lvdVar :: Var
lvdVar = Var
v
      , lvdLclEnv :: [Var]
lvdLclEnv = [Var]
g
      , lvdIsRec :: Bool
lvdIsRec = Bool
isRec
      }

localVarMap :: [LocalVarDetails] -> LocalVars
localVarMap :: [LocalVarDetails] -> LocalVars
localVarMap [LocalVarDetails]
lvds =
    LocalVars
      { lvSymbols :: HashMap Symbol [LocalVarDetails]
lvSymbols = [(Symbol, LocalVarDetails)] -> HashMap Symbol [LocalVarDetails]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group
          [ (Symbol
x, LocalVarDetails
lvd)
          | LocalVarDetails
lvd <- [LocalVarDetails]
lvds
          , let v :: Var
v = LocalVarDetails -> Var
lvdVar LocalVarDetails
lvd
                x :: Symbol
x = [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([Char] -> Symbol) -> [Char] -> Symbol
forall a b. (a -> b) -> a -> b
$ OccName -> [Char]
Ghc.occNameString (OccName -> [Char]) -> OccName -> [Char]
forall a b. (a -> b) -> a -> b
$ Name -> OccName
Ghc.nameOccName (Name -> OccName) -> Name -> OccName
forall a b. (a -> b) -> a -> b
$ Var -> Name
Ghc.varName Var
v
          ]
      , lvNames :: NameEnv LocalVarDetails
lvNames = (LocalVarDetails -> Name)
-> [LocalVarDetails] -> NameEnv LocalVarDetails
forall a. (a -> Name) -> [a] -> NameEnv a
Ghc.mkNameEnvWith (Var -> Name
forall a. NamedThing a => a -> Name
Ghc.getName (Var -> Name)
-> (LocalVarDetails -> Var) -> LocalVarDetails -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocalVarDetails -> Var
lvdVar) [LocalVarDetails]
lvds
      }

makeGHCTyLookupEnv :: Ghc.CoreProgram -> Ghc.TcRn GHCTyLookupEnv
makeGHCTyLookupEnv :: [Bind Var] -> TcRn GHCTyLookupEnv
makeGHCTyLookupEnv [Bind Var]
cbs = do
    hscEnv <- TcRnIf TcGblEnv TcLclEnv HscEnv
forall gbl lcl. TcRnIf gbl lcl HscEnv
Ghc.getTopEnv
    session <- Ghc.Session <$> Ghc.liftIO (newIORef hscEnv)
    tcg <- Ghc.getGblEnv
      -- Types differ in tcg_type_env vs the core bindings though they seem to
      -- be alpha-equivalent. We prefer the type in the core bindings and we
      -- also include the types of local variables.
    let varsEnv = [TyThing] -> TypeEnv
Ghc.mkTypeEnv ([TyThing] -> TypeEnv) -> [TyThing] -> TypeEnv
forall a b. (a -> b) -> a -> b
$ (Var -> TyThing) -> [Var] -> [TyThing]
forall a b. (a -> b) -> [a] -> [b]
map Var -> TyThing
Ghc.AnId ([Var] -> [TyThing]) -> [Var] -> [TyThing]
forall a b. (a -> b) -> a -> b
$ [Bind Var] -> [Var]
forall a. CBVisitable a => a -> [Var]
letVars [Bind Var]
cbs
        typeEnv = TcGblEnv -> TypeEnv
Ghc.tcg_type_env TcGblEnv
tcg TypeEnv -> TypeEnv -> TypeEnv
`Ghc.plusTypeEnv` TypeEnv
varsEnv
    return GHCTyLookupEnv
      { gtleSession = session
      , gtleTypeEnv = typeEnv
      }

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

isLocal :: F.Symbol -> Bool
isLocal :: Symbol -> Bool
isLocal = Symbol -> Bool
isEmptySymbol

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

-- | @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 :: F.Loc a => LocalVars -> LocSymbol -> [a] -> Maybe (Either a Ghc.Var)
lookupLocalVar :: forall a.
Loc a =>
LocalVars -> LocSymbol -> [a] -> Maybe (Either a Var)
lookupLocalVar LocalVars
localVars LocSymbol
lx [a]
gvs = SourcePos -> [(SourcePos, Either a Var)] -> Maybe (Either a Var)
forall b. SourcePos -> [(SourcePos, b)] -> Maybe b
findNearest SourcePos
lxn [(SourcePos, Either a Var)]
kvs
  where
    kvs :: [(SourcePos, Either a Var)]
kvs                   = [LocalVarDetails] -> [(SourcePos, Either a Var)]
forall {a}. [LocalVarDetails] -> [(SourcePos, Either a Var)]
prioritizeRecBinds ([LocalVarDetails]
-> Symbol -> HashMap Symbol [LocalVarDetails] -> [LocalVarDetails]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] Symbol
x (LocalVars -> HashMap Symbol [LocalVarDetails]
lvSymbols LocalVars
localVars)) [(SourcePos, Either a Var)]
-> [(SourcePos, Either a Var)] -> [(SourcePos, Either a Var)]
forall a. [a] -> [a] -> [a]
++ [(SourcePos, Either a Var)]
forall {b}. [(SourcePos, Either a b)]
gs
    gs :: [(SourcePos, Either a b)]
gs                    = [(SrcSpan -> SourcePos
F.sp_start (SrcSpan -> SourcePos) -> SrcSpan -> SourcePos
forall a b. (a -> b) -> a -> b
$ a -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan a
v, a -> Either a b
forall a b. a -> Either a b
Left a
v) | a
v <- [a]
gvs]
    lxn :: SourcePos
lxn                   = SrcSpan -> SourcePos
F.sp_start (SrcSpan -> SourcePos) -> SrcSpan -> SourcePos
forall a b. (a -> b) -> a -> b
$ LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan LocSymbol
lx
    (Maybe Symbol
_, Symbol
x)                = Symbol -> (Maybe Symbol, Symbol)
unQualifySymbol (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lx)

    -- Sometimes GHC produces multiple bindings that have the same source
    -- location. To select among these, we give preference to the recursive
    -- bindings which might need termination metrics.
    prioritizeRecBinds :: [LocalVarDetails] -> [(SourcePos, Either a Var)]
prioritizeRecBinds [LocalVarDetails]
lvds =
      let ([LocalVarDetails]
recs, [LocalVarDetails]
nrecs) = (LocalVarDetails -> Bool)
-> [LocalVarDetails] -> ([LocalVarDetails], [LocalVarDetails])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition LocalVarDetails -> Bool
lvdIsRec [LocalVarDetails]
lvds
       in (LocalVarDetails -> (SourcePos, Either a Var))
-> [LocalVarDetails] -> [(SourcePos, Either a Var)]
forall a b. (a -> b) -> [a] -> [b]
map LocalVarDetails -> (SourcePos, Either a Var)
forall {a}. LocalVarDetails -> (SourcePos, Either a Var)
lvdToPair ([LocalVarDetails]
recs [LocalVarDetails] -> [LocalVarDetails] -> [LocalVarDetails]
forall a. [a] -> [a] -> [a]
++ [LocalVarDetails]
nrecs)
    lvdToPair :: LocalVarDetails -> (SourcePos, Either a Var)
lvdToPair LocalVarDetails
lvd = (LocalVarDetails -> SourcePos
lvdSourcePos LocalVarDetails
lvd, Var -> Either a Var
forall a b. b -> Either a b
Right (LocalVarDetails -> Var
lvdVar LocalVarDetails
lvd))

    findNearest :: F.SourcePos -> [(F.SourcePos, b)] -> Maybe b
    findNearest :: forall b. SourcePos -> [(SourcePos, b)] -> Maybe b
findNearest SourcePos
key [(SourcePos, b)]
kvs1 = [((Int, Bool, Bool), b)] -> Maybe b
forall k v. Ord k => [(k, v)] -> Maybe v
argMin [ (SourcePos -> SourcePos -> (Int, Bool, Bool)
posDistance SourcePos
key SourcePos
k, b
v) | (SourcePos
k, b
v) <- [(SourcePos, b)]
kvs1 ]

    -- We prefer the var with the smaller distance, or equal distance
    -- but left of the spec, or not left of the spec but below it.
    posDistance :: SourcePos -> SourcePos -> (Int, Bool, Bool)
posDistance SourcePos
a SourcePos
b =
      ( Int -> Int
forall a. Num a => a -> a
abs (Pos -> Int
F.unPos (SourcePos -> Pos
sourceLine SourcePos
a) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Pos -> Int
F.unPos (SourcePos -> Pos
sourceLine SourcePos
b))
      , SourcePos -> Pos
sourceColumn SourcePos
a Pos -> Pos -> Bool
forall a. Ord a => a -> a -> Bool
< SourcePos -> Pos
sourceColumn SourcePos
b -- Note: False is prefered/smaller to True
      , SourcePos -> Pos
sourceLine SourcePos
a Pos -> Pos -> Bool
forall a. Ord a => a -> a -> Bool
> SourcePos -> Pos
sourceLine SourcePos
b
      )

    argMin :: (Ord k) => [(k, v)] -> Maybe v
    argMin :: forall k v. Ord k => [(k, v)] -> Maybe v
argMin = [v] -> Maybe v
forall a. [a] -> Maybe a
Mb.listToMaybe ([v] -> Maybe v) -> ([(k, v)] -> [v]) -> [(k, v)] -> Maybe v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((k, v) -> v) -> [(k, v)] -> [v]
forall a b. (a -> b) -> [a] -> [b]
map (k, v) -> v
forall a b. (a, b) -> b
snd ([(k, v)] -> [v]) -> ([(k, v)] -> [(k, v)]) -> [(k, v)] -> [v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((k, v) -> (k, v) -> Ordering) -> [(k, v)] -> [(k, v)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
L.sortBy (k -> k -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (k -> k -> Ordering)
-> ((k, v) -> k) -> (k, v) -> (k, v) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (k, v) -> k
forall a b. (a, b) -> a
fst)


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

lookupGhcDnTyConE :: Env -> DataName -> Lookup Ghc.TyCon
lookupGhcDnTyConE :: Env -> DataName -> Either [Error] TyCon
lookupGhcDnTyConE Env
env (DnCon  Located LHName
lname)
  = DataCon -> TyCon
Ghc.dataConTyCon (DataCon -> TyCon)
-> Either [Error] DataCon -> Either [Error] TyCon
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HasCallStack => Env -> Located LHName -> Either [Error] DataCon
Env -> Located LHName -> Either [Error] DataCon
lookupGhcDataConLHName Env
env Located LHName
lname
lookupGhcDnTyConE Env
env (DnName Located LHName
lname)
  = do
   case HasCallStack => GHCTyLookupEnv -> Located LHName -> TyThing
GHCTyLookupEnv -> Located LHName -> TyThing
lookupTyThing (Env -> GHCTyLookupEnv
reTyLookupEnv Env
env) Located LHName
lname of
     Ghc.ATyCon TyCon
tc -> TyCon -> Either [Error] TyCon
forall a b. b -> Either a b
Right TyCon
tc
     Ghc.AConLike (Ghc.RealDataCon DataCon
d) -> TyCon -> Either [Error] TyCon
forall a b. b -> Either a b
Right (TyCon -> Either [Error] TyCon) -> TyCon -> Either [Error] TyCon
forall a b. (a -> b) -> a -> b
$ DataCon -> TyCon
Ghc.dataConTyCon DataCon
d
     TyThing
_ -> Maybe SrcSpan -> [Char] -> Either [Error] TyCon
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic
           (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located LHName
lname) ([Char] -> Either [Error] TyCon) -> [Char] -> Either [Error] TyCon
forall a b. (a -> b) -> a -> b
$ [Char]
"not a type or data constructor: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ LHName -> [Char]
forall a. Show a => a -> [Char]
show (Located LHName -> LHName
forall a. Located a -> a
val Located LHName
lname)

lookupGhcDataConLHName :: HasCallStack => Env -> Located LHName -> Lookup Ghc.DataCon
lookupGhcDataConLHName :: HasCallStack => Env -> Located LHName -> Either [Error] DataCon
lookupGhcDataConLHName Env
env Located LHName
lname = do
   case HasCallStack => GHCTyLookupEnv -> Located LHName -> TyThing
GHCTyLookupEnv -> Located LHName -> TyThing
lookupTyThing (Env -> GHCTyLookupEnv
reTyLookupEnv Env
env) Located LHName
lname of
     Ghc.AConLike (Ghc.RealDataCon DataCon
d) -> DataCon -> Either [Error] DataCon
forall a b. b -> Either a b
Right DataCon
d
     TyThing
_ -> Maybe SrcSpan -> [Char] -> Either [Error] DataCon
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic
           (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located LHName
lname) ([Char] -> Either [Error] DataCon)
-> [Char] -> Either [Error] DataCon
forall a b. (a -> b) -> a -> b
$ [Char]
"not a data constructor: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ LHName -> [Char]
forall a. Show a => a -> [Char]
show (Located LHName -> LHName
forall a. Located a -> a
val Located LHName
lname)

lookupGhcIdLHName :: HasCallStack => Env -> Located LHName -> Lookup Ghc.Id
lookupGhcIdLHName :: HasCallStack => Env -> Located LHName -> Lookup Var
lookupGhcIdLHName Env
env Located LHName
lname =
   case HasCallStack => GHCTyLookupEnv -> Located LHName -> TyThing
GHCTyLookupEnv -> Located LHName -> TyThing
lookupTyThing (Env -> GHCTyLookupEnv
reTyLookupEnv Env
env) Located LHName
lname of
     Ghc.AConLike (Ghc.RealDataCon DataCon
d) -> Var -> Lookup Var
forall a b. b -> Either a b
Right (DataCon -> Var
Ghc.dataConWorkId DataCon
d)
     Ghc.AnId Var
x -> Var -> Lookup Var
forall a b. b -> Either a b
Right Var
x
     TyThing
_ -> Maybe SrcSpan -> [Char] -> Lookup Var
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic
           (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located LHName
lname) ([Char] -> Lookup Var) -> [Char] -> Lookup Var
forall a b. (a -> b) -> a -> b
$ [Char]
"not a variable or data constructor: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ LHName -> [Char]
forall a. Show a => a -> [Char]
show (Located LHName -> LHName
forall a. Located a -> a
val Located LHName
lname)

lookupGhcTyThingFromName :: GHCTyLookupEnv -> Ghc.Name -> Maybe Ghc.TyThing
-- see note about unsafePerformIO in lookupTyThingMaybe
lookupGhcTyThingFromName :: GHCTyLookupEnv -> Name -> Maybe TyThing
lookupGhcTyThingFromName GHCTyLookupEnv
env Name
n =
   IO (Maybe TyThing) -> Maybe TyThing
forall a. IO a -> a
unsafePerformIO (IO (Maybe TyThing) -> Maybe TyThing)
-> IO (Maybe TyThing) -> Maybe TyThing
forall a b. (a -> b) -> a -> b
$ Ghc (Maybe TyThing) -> Session -> IO (Maybe TyThing)
forall a. Ghc a -> Session -> IO a
Ghc.reflectGhc (TypeEnv -> Name -> Ghc (Maybe TyThing)
forall (m :: * -> *).
GhcMonad m =>
TypeEnv -> Name -> m (Maybe TyThing)
Interface.lookupTyThing (GHCTyLookupEnv -> TypeEnv
gtleTypeEnv GHCTyLookupEnv
env) Name
n) (GHCTyLookupEnv -> Session
gtleSession GHCTyLookupEnv
env)

lookupGhcId :: Env -> Ghc.Name -> Maybe Ghc.Id
lookupGhcId :: Env -> Name -> Maybe Var
lookupGhcId Env
env Name
n =
    case GHCTyLookupEnv -> Name -> Maybe TyThing
lookupGhcTyThingFromName GHCTyLookupEnv
env' Name
n of
      Just (Ghc.AConLike (Ghc.RealDataCon DataCon
d)) -> Var -> Maybe Var
forall a. a -> Maybe a
Just (DataCon -> Var
Ghc.dataConWorkId DataCon
d)
      Just (Ghc.AnId Var
x) -> Var -> Maybe Var
forall a. a -> Maybe a
Just Var
x
      Maybe TyThing
_ -> Maybe Var
forall a. Maybe a
Nothing
  where
    env' :: GHCTyLookupEnv
env' = Env -> GHCTyLookupEnv
reTyLookupEnv Env
env

-------------------------------------------------------------------------------
-- | Checking existence of names
-------------------------------------------------------------------------------
knownGhcType :: Env -> LocBareType -> Bool
knownGhcType :: Env -> LocBareType -> Bool
knownGhcType Env
env (F.Loc SourcePos
l SourcePos
_ BareType
t) =
  case HasCallStack =>
Env
-> SourcePos -> Maybe [PVar BSort] -> BareType -> Lookup SpecType
Env
-> SourcePos -> Maybe [PVar BSort] -> BareType -> Lookup SpecType
ofBareTypeE Env
env SourcePos
l Maybe [PVar BSort]
forall a. Maybe a
Nothing BareType
t of
    Left [Error]
e  -> [Char] -> Bool -> Bool
forall a. PPrint a => [Char] -> a -> a
myTracepp ([Char]
"knownType: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (BareType, [Error]) -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp (BareType
t, [Error]
e)) Bool
False
    Right SpecType
_ -> Bool
True



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

-- | `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 b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first 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' = [Char] -> (Symbol, Symbol) -> (Symbol, Symbol)
forall a. PPrint a => [Char] -> a -> a
myTracepp ([Char]
"splitModuleNameExact for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp Symbol
x)
                          (Symbol -> Symbol
GM.takeModuleNames Symbol
x, Symbol -> Symbol
GM.dropModuleNames Symbol
x)
  where
    x :: Symbol
x = Symbol -> Symbol
GM.stripParensSym Symbol
x'

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

-------------------------------------------------------------------------------
-- | @ofBareType@ and @ofBareTypeE@ should be the _only_ @SpecType@ constructors
-------------------------------------------------------------------------------
ofBareType :: HasCallStack => Env -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> SpecType
ofBareType :: HasCallStack =>
Env -> SourcePos -> Maybe [PVar BSort] -> BareType -> SpecType
ofBareType Env
env SourcePos
l Maybe [PVar BSort]
ps BareType
t = ([Error] -> SpecType)
-> (SpecType -> SpecType) -> Lookup SpecType -> SpecType
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either [Error] -> SpecType
forall {a}. [Error] -> a
fail' SpecType -> SpecType
forall a. a -> a
id (HasCallStack =>
Env
-> SourcePos -> Maybe [PVar BSort] -> BareType -> Lookup SpecType
Env
-> SourcePos -> Maybe [PVar BSort] -> BareType -> Lookup SpecType
ofBareTypeE Env
env SourcePos
l Maybe [PVar BSort]
ps BareType
t)
  where
    fail' :: [Error] -> a
fail'                  = [Error] -> a
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw
    -- fail                   = Misc.errorP "error-ofBareType" . F.showpp

ofBareTypeE :: HasCallStack => Env -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> Lookup SpecType
ofBareTypeE :: HasCallStack =>
Env
-> SourcePos -> Maybe [PVar BSort] -> BareType -> Lookup SpecType
ofBareTypeE Env
env SourcePos
l Maybe [PVar BSort]
ps BareType
t = Env
-> ([Symbol]
    -> UReftV Symbol (ReftV Symbol) -> UReftV Symbol (ReftV Symbol))
-> SourcePos
-> BareType
-> Lookup SpecType
forall r.
Expandable r =>
Env
-> ([Symbol] -> r -> r)
-> SourcePos
-> BRType r
-> Lookup (RRType r)
ofBRType Env
env ((UReftV Symbol (ReftV Symbol) -> UReftV Symbol (ReftV Symbol))
-> [Symbol]
-> UReftV Symbol (ReftV Symbol)
-> UReftV Symbol (ReftV Symbol)
forall a b. a -> b -> a
const (SourcePos
-> Maybe [PVar BSort]
-> BareType
-> UReftV Symbol (ReftV Symbol)
-> UReftV Symbol (ReftV Symbol)
resolveReft SourcePos
l Maybe [PVar BSort]
ps BareType
t)) SourcePos
l BareType
t

resolveReft :: F.SourcePos -> Maybe [PVar BSort] -> BareType -> RReft -> RReft
resolveReft :: SourcePos
-> Maybe [PVar BSort]
-> BareType
-> UReftV Symbol (ReftV Symbol)
-> UReftV Symbol (ReftV Symbol)
resolveReft SourcePos
l Maybe [PVar BSort]
ps BareType
t
        = SourcePos
-> ((UsedPVar -> UsedPVar)
    -> UReftV Symbol (ReftV Symbol) -> UReftV Symbol (ReftV Symbol))
-> [UsedPVar]
-> BareType
-> UReftV Symbol (ReftV Symbol)
-> UReftV Symbol (ReftV Symbol)
forall t c tv r.
SourcePos
-> ((UsedPVar -> UsedPVar) -> t) -> [UsedPVar] -> RType c tv r -> t
txParam SourcePos
l (UsedPVar -> UsedPVar)
-> UReftV Symbol (ReftV Symbol) -> UReftV Symbol (ReftV Symbol)
RT.subvUReft (PVar BSort -> UsedPVar
forall v t. PVarV v t -> UsedPVarV v
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
        (UReftV Symbol (ReftV Symbol) -> UReftV Symbol (ReftV Symbol))
-> (UReftV Symbol (ReftV Symbol) -> UReftV Symbol (ReftV Symbol))
-> UReftV Symbol (ReftV Symbol)
-> UReftV Symbol (ReftV Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareType
-> UReftV Symbol (ReftV Symbol) -> UReftV Symbol (ReftV Symbol)
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 = RTypeRepV Symbol BTyCon BTyVar (UReftV Symbol (ReftV Symbol))
-> [PVar BSort]
forall v c tv r. RTypeRepV v c tv r -> [PVarV v (RTypeV v c tv ())]
ty_preds (BareType
-> RTypeRepV Symbol BTyCon BTyVar (UReftV Symbol (ReftV Symbol))
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep BareType
t)

fixReftTyVars :: BareType -> RReft -> RReft
fixReftTyVars :: BareType
-> UReftV Symbol (ReftV Symbol) -> UReftV Symbol (ReftV Symbol)
fixReftTyVars BareType
bt  = CoSub
-> UReftV Symbol (ReftV Symbol) -> UReftV Symbol (ReftV Symbol)
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
-> UReftV Symbol (ReftV Symbol) -> UReftV Symbol (ReftV Symbol)
coSubRReft CoSub
su UReftV Symbol (ReftV Symbol)
r = UReftV Symbol (ReftV Symbol)
r { ur_reft = coSubReft su (ur_reft r) }

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


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

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

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

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

txPvar :: F.SourcePos -> M.HashMap F.Symbol UsedPVar -> UsedPVar -> UsedPVar
txPvar :: SourcePos -> HashMap Symbol UsedPVar -> UsedPVar -> UsedPVar
txPvar SourcePos
l HashMap Symbol UsedPVar
m UsedPVar
π = UsedPVar
π { pargs = args' }
  where
    args' :: [((), Symbol, Expr)]
args' | Bool -> Bool
not ([((), Symbol, Expr)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (UsedPVar -> [((), Symbol, Expr)]
forall v t. PVarV v t -> [(t, Symbol, ExprV v)]
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 v t. PVarV v t -> [(t, Symbol, ExprV v)]
pargs UsedPVar
π') (UsedPVar -> [((), Symbol, Expr)]
forall v t. PVarV v t -> [(t, Symbol, ExprV v)]
pargs UsedPVar
π)
          | Bool
otherwise            = UsedPVar -> [((), Symbol, Expr)]
forall v t. PVarV v t -> [(t, Symbol, ExprV v)]
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 v t. PVarV v t -> Symbol
pname UsedPVar
π) HashMap Symbol UsedPVar
m
    err :: a
err   = UserError -> a
forall a. UserError -> a
uError (UserError -> a) -> UserError -> a
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> UserError
forall t. SrcSpan -> Doc -> TError t
ErrUnbPred SrcSpan
sp (UsedPVar -> Doc
forall a. PPrint a => a -> Doc
pprint UsedPVar
π)
    sp :: SrcSpan
sp    = SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l

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

rtypePredBinds :: RType c tv r -> [UsedPVar]
rtypePredBinds :: forall c tv r. RType c tv r -> [UsedPVar]
rtypePredBinds = (PVarV Symbol (RTypeV Symbol c tv ()) -> UsedPVar)
-> [PVarV Symbol (RTypeV Symbol c tv ())] -> [UsedPVar]
forall a b. (a -> b) -> [a] -> [b]
map PVarV Symbol (RTypeV Symbol c tv ()) -> UsedPVar
forall v t. PVarV v t -> UsedPVarV v
RT.uPVar ([PVarV Symbol (RTypeV Symbol c tv ())] -> [UsedPVar])
-> (RType c tv r -> [PVarV Symbol (RTypeV Symbol c tv ())])
-> RType c tv r
-> [UsedPVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeRepV Symbol c tv r -> [PVarV Symbol (RTypeV Symbol c tv ())]
forall v c tv r. RTypeRepV v c tv r -> [PVarV v (RTypeV v c tv ())]
ty_preds (RTypeRepV Symbol c tv r -> [PVarV Symbol (RTypeV Symbol c tv ())])
-> (RType c tv r -> RTypeRepV Symbol c tv r)
-> RType c tv r
-> [PVarV Symbol (RTypeV Symbol c tv ())]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType c tv r -> RTypeRepV Symbol c tv r
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep



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

ofBRType :: (Expandable r) => Env -> ([F.Symbol] -> r -> r) -> F.SourcePos -> BRType r
         -> Lookup (RRType r)
ofBRType :: forall r.
Expandable r =>
Env
-> ([Symbol] -> r -> r)
-> SourcePos
-> BRType r
-> Lookup (RRType r)
ofBRType Env
env [Symbol] -> r -> r
f SourcePos
l = [Symbol]
-> RTypeV Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go []
  where
    goReft :: [Symbol] -> r -> m r
goReft [Symbol]
bs r
r             = r -> m r
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Symbol] -> r -> r
f [Symbol]
bs r
r)
    goRFun :: [Symbol]
-> Symbol
-> RFInfo
-> RTypeV Symbol BTyCon BTyVar r
-> RTypeV Symbol BTyCon BTyVar r
-> r
-> Either [Error] (RType RTyCon RTyVar r)
goRFun [Symbol]
bs Symbol
x RFInfo
i RTypeV Symbol BTyCon BTyVar r
t1 RTypeV Symbol BTyCon BTyVar r
t2 r
r  = Symbol
-> RFInfo
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> r
-> RType RTyCon RTyVar r
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
x RFInfo
i{permitTC = Just (typeclass (getConfig env))} (RType RTyCon RTyVar r
 -> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either
     [Error] (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Symbol -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall {r} {c} {tv}.
(Reftable r, TyConable c) =>
Symbol -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
rebind Symbol
x (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> RTypeV Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeV Symbol BTyCon BTyVar r
t1) Either
  [Error] (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (r -> RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol]
-> RTypeV Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
bs) RTypeV Symbol BTyCon BTyVar r
t2 Either [Error] (r -> RType RTyCon RTyVar r)
-> Either [Error] r -> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
    rebind :: Symbol -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
rebind Symbol
x RTypeV Symbol c tv r
t              = RTypeV Symbol c tv r -> (Symbol, Expr) -> RTypeV Symbol c tv r
forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 RTypeV Symbol c tv r
t (Symbol
x, Symbol -> Expr
forall v. v -> ExprV v
F.EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ RTypeV Symbol c tv r -> Symbol
forall r c tv. Reftable r => RType c tv r -> Symbol
rTypeValueVar RTypeV Symbol c tv r
t)
    go :: [Symbol]
-> RTypeV Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs (RAppTy RTypeV Symbol BTyCon BTyVar r
t1 RTypeV Symbol BTyCon BTyVar r
t2 r
r)  = RType RTyCon RTyVar r
-> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy (RType RTyCon RTyVar r
 -> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either
     [Error] (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> RTypeV Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeV Symbol BTyCon BTyVar r
t1 Either
  [Error] (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (r -> RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol]
-> RTypeV Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeV Symbol BTyCon BTyVar r
t2 Either [Error] (r -> RType RTyCon RTyVar r)
-> Either [Error] r -> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
    go [Symbol]
bs (RApp BTyCon
tc [RTypeV Symbol BTyCon BTyVar r]
ts [RTPropV Symbol BTyCon BTyVar r]
rs r
r) = [Symbol]
-> BTyCon
-> [RTypeV Symbol BTyCon BTyVar r]
-> [RTPropV Symbol BTyCon BTyVar r]
-> r
-> Either [Error] (RType RTyCon RTyVar r)
goRApp [Symbol]
bs BTyCon
tc [RTypeV Symbol BTyCon BTyVar r]
ts [RTPropV Symbol BTyCon BTyVar r]
rs r
r
    go [Symbol]
bs (RFun Symbol
x RFInfo
i RTypeV Symbol BTyCon BTyVar r
t1 RTypeV Symbol BTyCon BTyVar r
t2 r
r) = [Symbol]
-> Symbol
-> RFInfo
-> RTypeV Symbol BTyCon BTyVar r
-> RTypeV Symbol BTyCon BTyVar r
-> r
-> Either [Error] (RType RTyCon RTyVar r)
goRFun [Symbol]
bs Symbol
x RFInfo
i RTypeV Symbol BTyCon BTyVar r
t1 RTypeV Symbol BTyCon BTyVar r
t2 r
r
    go [Symbol]
bs (RVar BTyVar
a r
r)        = RTyVar -> r -> RType RTyCon RTyVar r
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar (BTyVar -> RTyVar
RT.bareRTyVar BTyVar
a) (r -> RType RTyCon RTyVar r)
-> Either [Error] r -> Either [Error] (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
    go [Symbol]
bs (RAllT RTVUV Symbol BTyCon BTyVar
a RTypeV Symbol BTyCon BTyVar r
t r
r)     = RTVar RTyVar (RType RTyCon RTyVar ())
-> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVar RTyVar (RType RTyCon RTyVar ())
forall {s2}. RTVar RTyVar s2
a' (RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> RTypeV Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeV Symbol BTyCon BTyVar r
t Either [Error] (r -> RType RTyCon RTyVar r)
-> Either [Error] r -> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
      where a' :: RTVar RTyVar s2
a'              = RTVar RTyVar BSort -> RTVar RTyVar s2
forall tv s1 s2. RTVar tv s1 -> RTVar tv s2
dropTyVarInfo ((BTyVar -> RTyVar)
-> RTVUV Symbol BTyCon BTyVar -> RTVar RTyVar BSort
forall tv1 tv2 s. (tv1 -> tv2) -> RTVar tv1 s -> RTVar tv2 s
mapTyVarValue BTyVar -> RTyVar
RT.bareRTyVar RTVUV Symbol BTyCon BTyVar
a)
    go [Symbol]
bs (RAllP PVar BSort
a RTypeV Symbol BTyCon BTyVar r
t)       = RPVar -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP RPVar
a' (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> RTypeV Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeV Symbol BTyCon BTyVar r
t
      where a' :: RPVar
a'              = Env -> SourcePos -> PVar BSort -> RPVar
ofBPVar Env
env SourcePos
l PVar BSort
a
    go [Symbol]
bs (RAllE Symbol
x RTypeV Symbol BTyCon BTyVar r
t1 RTypeV Symbol BTyCon BTyVar r
t2)   = Symbol
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
RAllE Symbol
x  (RType RTyCon RTyVar r
 -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> RTypeV Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeV Symbol BTyCon BTyVar r
t1    Either [Error] (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol]
-> RTypeV Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeV Symbol BTyCon BTyVar r
t2
    go [Symbol]
bs (REx Symbol
x RTypeV Symbol BTyCon BTyVar r
t1 RTypeV Symbol BTyCon BTyVar r
t2)     = Symbol
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
REx   Symbol
x  (RType RTyCon RTyVar r
 -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> RTypeV Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeV Symbol BTyCon BTyVar r
t1    Either [Error] (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol]
-> RTypeV Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
bs) RTypeV Symbol BTyCon BTyVar r
t2
    go [Symbol]
bs (RRTy [(Symbol, RTypeV Symbol BTyCon BTyVar r)]
xts r
r Oblig
o RTypeV Symbol BTyCon BTyVar r
t)  = [(Symbol, RType RTyCon RTyVar r)]
-> r -> Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy  ([(Symbol, RType RTyCon RTyVar r)]
 -> r -> Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] [(Symbol, RType RTyCon RTyVar r)]
-> Either
     [Error]
     (r -> Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either [Error] [(Symbol, RType RTyCon RTyVar r)]
xts' Either
  [Error]
  (r -> Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] r
-> Either
     [Error] (Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r Either
  [Error] (Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] Oblig
-> Either [Error] (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Oblig -> Either [Error] Oblig
forall a. a -> Either [Error] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Oblig
o Either [Error] (RType RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol]
-> RTypeV Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeV Symbol BTyCon BTyVar r
t
      where xts' :: Either [Error] [(Symbol, RType RTyCon RTyVar r)]
xts'            = ((Symbol, RTypeV Symbol BTyCon BTyVar r)
 -> Either [Error] (Symbol, RType RTyCon RTyVar r))
-> [(Symbol, RTypeV Symbol BTyCon BTyVar r)]
-> Either [Error] [(Symbol, RType RTyCon RTyVar r)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((RTypeV Symbol BTyCon BTyVar r
 -> Either [Error] (RType RTyCon RTyVar r))
-> (Symbol, RTypeV Symbol BTyCon BTyVar r)
-> Either [Error] (Symbol, RType RTyCon RTyVar r)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (Symbol, a) -> f (Symbol, b)
traverse ([Symbol]
-> RTypeV Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs)) [(Symbol, RTypeV Symbol BTyCon BTyVar r)]
xts
    go [Symbol]
bs (RHole r
r)         = r -> RType RTyCon RTyVar r
forall v c tv r. r -> RTypeV v c tv r
RHole    (r -> RType RTyCon RTyVar r)
-> Either [Error] r -> Either [Error] (RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
    go [Symbol]
_ (RExprArg Located Expr
le)      = RType RTyCon RTyVar r -> Either [Error] (RType RTyCon RTyVar r)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return    (RType RTyCon RTyVar r -> Either [Error] (RType RTyCon RTyVar r))
-> RType RTyCon RTyVar r -> Either [Error] (RType RTyCon RTyVar r)
forall a b. (a -> b) -> a -> b
$ Located Expr -> RType RTyCon RTyVar r
forall v c tv r. Located (ExprV v) -> RTypeV v c tv r
RExprArg Located Expr
le
    goRef :: [Symbol]
-> RTPropV Symbol BTyCon BTyVar r
-> Either [Error] (RTProp RTyCon RTyVar r)
goRef [Symbol]
bs (RProp [(Symbol, BSort)]
ss (RHole r
r)) = [(Symbol, RType RTyCon RTyVar ())] -> r -> RTProp RTyCon RTyVar r
forall τ r v c tv. [(Symbol, τ)] -> r -> Ref τ (RTypeV v c tv r)
rPropP ([(Symbol, RType RTyCon RTyVar ())] -> r -> RTProp RTyCon RTyVar r)
-> Either [Error] [(Symbol, RType RTyCon RTyVar ())]
-> Either [Error] (r -> RTProp RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Symbol, BSort)
 -> Either [Error] (Symbol, RType RTyCon RTyVar ()))
-> [(Symbol, BSort)]
-> Either [Error] [(Symbol, RType RTyCon RTyVar ())]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Symbol, BSort) -> Either [Error] (Symbol, RType RTyCon RTyVar ())
forall {t}.
(t, BSort) -> Either [Error] (t, RType RTyCon RTyVar ())
goSyms [(Symbol, BSort)]
ss Either [Error] (r -> RTProp RTyCon RTyVar r)
-> Either [Error] r -> Either [Error] (RTProp RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r
    goRef [Symbol]
bs (RProp [(Symbol, BSort)]
ss RTypeV Symbol BTyCon BTyVar r
t)         = [(Symbol, RType RTyCon RTyVar ())]
-> RType RTyCon RTyVar r -> RTProp RTyCon RTyVar r
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp  ([(Symbol, RType RTyCon RTyVar ())]
 -> RType RTyCon RTyVar r -> RTProp RTyCon RTyVar r)
-> Either [Error] [(Symbol, RType RTyCon RTyVar ())]
-> Either [Error] (RType RTyCon RTyVar r -> RTProp RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Symbol, BSort)
 -> Either [Error] (Symbol, RType RTyCon RTyVar ()))
-> [(Symbol, BSort)]
-> Either [Error] [(Symbol, RType RTyCon RTyVar ())]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Symbol, BSort) -> Either [Error] (Symbol, RType RTyCon RTyVar ())
forall {t}.
(t, BSort) -> Either [Error] (t, RType RTyCon RTyVar ())
goSyms [(Symbol, BSort)]
ss Either [Error] (RType RTyCon RTyVar r -> RTProp RTyCon RTyVar r)
-> Either [Error] (RType RTyCon RTyVar r)
-> Either [Error] (RTProp RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol]
-> RTypeV Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeV Symbol BTyCon BTyVar r
t
    goSyms :: (t, BSort) -> Either [Error] (t, RType RTyCon RTyVar ())
goSyms (t
x, BSort
t)                 = (t
x,) (RType RTyCon RTyVar () -> (t, RType RTyCon RTyVar ()))
-> Either [Error] (RType RTyCon RTyVar ())
-> Either [Error] (t, RType RTyCon RTyVar ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HasCallStack =>
Env
-> SourcePos -> BSort -> Either [Error] (RType RTyCon RTyVar ())
Env
-> SourcePos -> BSort -> Either [Error] (RType RTyCon RTyVar ())
ofBSortE Env
env SourcePos
l BSort
t
    goRApp :: [Symbol]
-> BTyCon
-> [RTypeV Symbol BTyCon BTyVar r]
-> [RTPropV Symbol BTyCon BTyVar r]
-> r
-> Either [Error] (RType RTyCon RTyVar r)
goRApp [Symbol]
bs BTyCon
tc [RTypeV Symbol BTyCon BTyVar r]
ts [RTPropV Symbol BTyCon BTyVar r]
rs r
r          = r
-> Located TyCon
-> [RTProp RTyCon RTyVar r]
-> [RType RTyCon RTyVar r]
-> RType RTyCon RTyVar r
forall r.
Expandable r =>
r
-> Located TyCon
-> [RTProp RTyCon RTyVar r]
-> [RType RTyCon RTyVar r]
-> RType RTyCon RTyVar r
bareTCApp (r
 -> Located TyCon
 -> [RTProp RTyCon RTyVar r]
 -> [RType RTyCon RTyVar r]
 -> RType RTyCon RTyVar r)
-> Either [Error] r
-> Either
     [Error]
     (Located TyCon
      -> [RTProp RTyCon RTyVar r]
      -> [RType RTyCon RTyVar r]
      -> RType RTyCon RTyVar r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> r -> Either [Error] r
forall {m :: * -> *}. Monad m => [Symbol] -> r -> m r
goReft [Symbol]
bs r
r Either
  [Error]
  (Located TyCon
   -> [RTProp RTyCon RTyVar r]
   -> [RType RTyCon RTyVar r]
   -> RType RTyCon RTyVar r)
-> Either [Error] (Located TyCon)
-> Either
     [Error]
     ([RTProp RTyCon RTyVar r]
      -> [RType RTyCon RTyVar r] -> RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Either [Error] (Located TyCon)
lc' Either
  [Error]
  ([RTProp RTyCon RTyVar r]
   -> [RType RTyCon RTyVar r] -> RType RTyCon RTyVar r)
-> Either [Error] [RTProp RTyCon RTyVar r]
-> Either
     [Error] ([RType RTyCon RTyVar r] -> RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (RTPropV Symbol BTyCon BTyVar r
 -> Either [Error] (RTProp RTyCon RTyVar r))
-> [RTPropV Symbol BTyCon BTyVar r]
-> Either [Error] [RTProp RTyCon RTyVar r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([Symbol]
-> RTPropV Symbol BTyCon BTyVar r
-> Either [Error] (RTProp RTyCon RTyVar r)
goRef [Symbol]
bs) [RTPropV Symbol BTyCon BTyVar r]
rs Either [Error] ([RType RTyCon RTyVar r] -> RType RTyCon RTyVar r)
-> Either [Error] [RType RTyCon RTyVar r]
-> Either [Error] (RType RTyCon RTyVar r)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (RTypeV Symbol BTyCon BTyVar r
 -> Either [Error] (RType RTyCon RTyVar r))
-> [RTypeV Symbol BTyCon BTyVar r]
-> Either [Error] [RType RTyCon RTyVar r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([Symbol]
-> RTypeV Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs) [RTypeV Symbol BTyCon BTyVar r]
ts
      where
        lc' :: Either [Error] (Located TyCon)
lc'                    = Located LHName -> TyCon -> Located TyCon
forall l b. Loc l => l -> b -> Located b
F.atLoc Located LHName
lc (TyCon -> Located TyCon)
-> Either [Error] TyCon -> Either [Error] (Located TyCon)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HasCallStack =>
GHCTyLookupEnv -> Located LHName -> Either [Error] TyCon
GHCTyLookupEnv -> Located LHName -> Either [Error] TyCon
lookupGhcTyConLHName (Env -> GHCTyLookupEnv
reTyLookupEnv Env
env) Located LHName
lc
        lc :: Located LHName
lc                     = BTyCon -> Located LHName
btc_tc BTyCon
tc

lookupGhcTyConLHName :: HasCallStack => GHCTyLookupEnv -> Located LHName -> Lookup Ghc.TyCon
lookupGhcTyConLHName :: HasCallStack =>
GHCTyLookupEnv -> Located LHName -> Either [Error] TyCon
lookupGhcTyConLHName GHCTyLookupEnv
env Located LHName
lc = do
    case HasCallStack => GHCTyLookupEnv -> Located LHName -> TyThing
GHCTyLookupEnv -> Located LHName -> TyThing
lookupTyThing GHCTyLookupEnv
env Located LHName
lc of
      Ghc.ATyCon TyCon
tc -> TyCon -> Either [Error] TyCon
forall a b. b -> Either a b
Right TyCon
tc
      Ghc.AConLike (Ghc.RealDataCon DataCon
dc) -> TyCon -> Either [Error] TyCon
forall a b. b -> Either a b
Right (TyCon -> Either [Error] TyCon) -> TyCon -> Either [Error] TyCon
forall a b. (a -> b) -> a -> b
$ DataCon -> TyCon
Ghc.promoteDataCon DataCon
dc
      TyThing
_ -> Maybe SrcSpan -> [Char] -> Either [Error] TyCon
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic
            (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located LHName
lc) ([Char] -> Either [Error] TyCon) -> [Char] -> Either [Error] TyCon
forall a b. (a -> b) -> a -> b
$ [Char]
"not a type constructor: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ LHName -> [Char]
forall a. Show a => a -> [Char]
show (Located LHName -> LHName
forall a. Located a -> a
val Located LHName
lc)

-- | Get the TyThing from an LHName.
--
-- This function uses 'unsafePerformIO' to lookup the 'Ghc.TyThing' of a 'Ghc.Name'.
-- This should be benign because the result doesn't depend of when exactly this is
-- called. Since this code is intended to be used inside a GHC plugin, there is no
-- danger that GHC is finalized before the result is evaluated.
lookupTyThingMaybe :: HasCallStack => GHCTyLookupEnv -> Located LHName -> Maybe Ghc.TyThing
lookupTyThingMaybe :: HasCallStack => GHCTyLookupEnv -> Located LHName -> Maybe TyThing
lookupTyThingMaybe GHCTyLookupEnv
env lc :: Located LHName
lc@(Loc SourcePos
_ SourcePos
_ LHName
c0) = IO (Maybe TyThing) -> Maybe TyThing
forall a. IO a -> a
unsafePerformIO (IO (Maybe TyThing) -> Maybe TyThing)
-> IO (Maybe TyThing) -> Maybe TyThing
forall a b. (a -> b) -> a -> b
$ do
    case LHName
c0 of
      LHNUnresolved LHNameSpace
_ Symbol
_ -> Maybe SrcSpan -> [Char] -> IO (Maybe TyThing)
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located LHName
lc) ([Char] -> IO (Maybe TyThing)) -> [Char] -> IO (Maybe TyThing)
forall a b. (a -> b) -> a -> b
$ [Char]
"unresolved name: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ LHName -> [Char]
forall a. Show a => a -> [Char]
show LHName
c0
      LHNResolved LHResolvedName
rn Symbol
_ -> case LHResolvedName
rn of
        LHRLocal Symbol
_ -> Maybe SrcSpan -> [Char] -> IO (Maybe TyThing)
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located LHName
lc) ([Char] -> IO (Maybe TyThing)) -> [Char] -> IO (Maybe TyThing)
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot resolve a local name: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ LHName -> [Char]
forall a. Show a => a -> [Char]
show LHName
c0
        LHRIndex Word
i -> Maybe SrcSpan -> [Char] -> IO (Maybe TyThing)
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located LHName
lc) ([Char] -> IO (Maybe TyThing)) -> [Char] -> IO (Maybe TyThing)
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot resolve a LHRIndex " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Word -> [Char]
forall a. Show a => a -> [Char]
show Word
i
        LHRLogic LogicName
_ -> Maybe SrcSpan -> [Char] -> IO (Maybe TyThing)
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located LHName
lc) ([Char] -> IO (Maybe TyThing)) -> [Char] -> IO (Maybe TyThing)
forall a b. (a -> b) -> a -> b
$ [Char]
"lookupTyThing: cannot resolve a LHRLogic name " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show (LHName -> Symbol
lhNameToResolvedSymbol LHName
c0)
        LHRGHC Name
n ->
          Ghc (Maybe TyThing) -> Session -> IO (Maybe TyThing)
forall a. Ghc a -> Session -> IO a
Ghc.reflectGhc (TypeEnv -> Name -> Ghc (Maybe TyThing)
forall (m :: * -> *).
GhcMonad m =>
TypeEnv -> Name -> m (Maybe TyThing)
Interface.lookupTyThing (GHCTyLookupEnv -> TypeEnv
gtleTypeEnv GHCTyLookupEnv
env) Name
n) (GHCTyLookupEnv -> Session
gtleSession GHCTyLookupEnv
env)

lookupTyThing :: HasCallStack => GHCTyLookupEnv -> Located LHName -> Ghc.TyThing
lookupTyThing :: HasCallStack => GHCTyLookupEnv -> Located LHName -> TyThing
lookupTyThing GHCTyLookupEnv
env Located LHName
lc =
    TyThing -> Maybe TyThing -> TyThing
forall a. a -> Maybe a -> a
Mb.fromMaybe (Maybe SrcSpan -> [Char] -> TyThing
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located LHName
lc) ([Char] -> TyThing) -> [Char] -> TyThing
forall a b. (a -> b) -> a -> b
$ [Char]
"not found: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ LHName -> [Char]
forall a. Show a => a -> [Char]
show (Located LHName -> LHName
forall a. Located a -> a
val Located LHName
lc)) (Maybe TyThing -> TyThing) -> Maybe TyThing -> TyThing
forall a b. (a -> b) -> a -> b
$
      HasCallStack => GHCTyLookupEnv -> Located LHName -> Maybe TyThing
GHCTyLookupEnv -> Located LHName -> Maybe TyThing
lookupTyThingMaybe GHCTyLookupEnv
env Located LHName
lc

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

       err :: Error
       err :: Error
err = SrcSpan -> Doc -> SrcSpan -> Doc -> Error
forall t. SrcSpan -> Doc -> SrcSpan -> Doc -> TError t
ErrAliasApp (SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l) (TyCon -> Doc
forall a. PPrint a => a -> Doc
pprint TyCon
c) (TyCon -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
Ghc.getSrcSpan TyCon
c)
                         ([Doc] -> Doc
PJ.hcat [ [Char] -> Doc
PJ.text [Char]
"Expects"
                                  , Int -> Doc
forall a. PPrint a => a -> Doc
pprint (TyCon -> Int
GM.realTcArity TyCon
c)
                                  , [Char] -> Doc
PJ.text [Char]
"arguments, but is given"
                                  , Int -> Doc
forall a. PPrint a => a -> Doc
pprint ([RType RTyCon RTyVar r] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType RTyCon RTyVar r]
ts) ] )
-- TODO expandTypeSynonyms here to
bareTCApp r
r (Loc SourcePos
_ SourcePos
_ TyCon
c) [RTProp RTyCon RTyVar r]
rs [RType RTyCon RTyVar r]
ts | TyCon -> Bool
Ghc.isFamilyTyCon TyCon
c Bool -> Bool -> Bool
&& RType RTyCon RTyVar r -> Bool
forall r c tv. (Reftable r, TyConable c) => RType c tv r -> Bool
isTrivial RType RTyCon RTyVar r
t
  = RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall r. Expandable r => RRType r -> RRType r
expandRTypeSynonyms (RType RTyCon RTyVar r
t RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r
forall r v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v 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 :: Reftable r => RType c tv r -> [RType c tv r] -> [RTProp c tv r] -> r
      -> RType c tv r
tyApp :: forall r c tv.
Reftable r =>
RType c tv r
-> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
tyApp (RApp c
c [RTypeV Symbol c tv r]
ts [RTPropV Symbol c tv r]
rs r
r) [RTypeV Symbol c tv r]
ts' [RTPropV Symbol c tv r]
rs' r
r' = c
-> [RTypeV Symbol c tv r]
-> [RTPropV Symbol c tv r]
-> r
-> RTypeV Symbol c tv r
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp c
c ([RTypeV Symbol c tv r]
ts [RTypeV Symbol c tv r]
-> [RTypeV Symbol c tv r] -> [RTypeV Symbol c tv r]
forall a. [a] -> [a] -> [a]
++ [RTypeV Symbol c tv r]
ts') ([RTPropV Symbol c tv r]
rs [RTPropV Symbol c tv r]
-> [RTPropV Symbol c tv r] -> [RTPropV Symbol c tv r]
forall a. [a] -> [a] -> [a]
++ [RTPropV Symbol c tv r]
rs') (r
r r -> r -> r
forall r. Reftable r => r -> r -> r
`meet` r
r')
tyApp RTypeV Symbol c tv r
t                []  []  r
r  = RTypeV Symbol c tv r
t RTypeV Symbol c tv r -> r -> RTypeV Symbol c tv r
forall r v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v c tv r
`RT.strengthen` r
r
tyApp RTypeV Symbol c tv r
_                 [RTypeV Symbol c tv r]
_  [RTPropV Symbol c tv r]
_   r
_  = Maybe SrcSpan -> [Char] -> RTypeV Symbol c tv r
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Bare.Type.tyApp on invalid inputs"

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

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

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

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

txRefSort :: TyConMap -> F.TCEmb Ghc.TyCon -> LocSpecType -> LocSpecType
txRefSort :: TyConMap -> TCEmb TyCon -> LocSpecType -> LocSpecType
txRefSort TyConMap
tyi TCEmb TyCon
tce LocSpecType
t = LocSpecType -> SpecType -> LocSpecType
forall l b. Loc l => l -> b -> Located b
F.atLoc LocSpecType
t (SpecType -> LocSpecType) -> SpecType -> LocSpecType
forall a b. (a -> b) -> a -> b
$ (SpecType -> SpecType) -> SpecType -> SpecType
forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot (SrcSpan -> TCEmb TyCon -> TyConMap -> SpecType -> SpecType
addSymSort (LocSpecType -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSpecType
t) TCEmb TyCon
tce TyConMap
tyi) (LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
t)

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

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

addSymSortRef :: (PPrint s) => Ghc.SrcSpan -> s -> RPVar -> SpecProp -> Int -> SpecProp
addSymSortRef :: forall s.
PPrint s =>
SrcSpan
-> s
-> RPVar
-> RTProp RTyCon RTyVar (UReftV Symbol (ReftV Symbol))
-> Int
-> RTProp RTyCon RTyVar (UReftV Symbol (ReftV Symbol))
addSymSortRef SrcSpan
sp s
rc RPVar
p RTProp RTyCon RTyVar (UReftV Symbol (ReftV Symbol))
r Int
i = SrcSpan
-> s
-> Int
-> RPVar
-> RTProp RTyCon RTyVar (UReftV Symbol (ReftV Symbol))
-> RTProp RTyCon RTyVar (UReftV Symbol (ReftV Symbol))
forall s.
PPrint s =>
SrcSpan
-> s
-> Int
-> RPVar
-> RTProp RTyCon RTyVar (UReftV Symbol (ReftV Symbol))
-> RTProp RTyCon RTyVar (UReftV Symbol (ReftV Symbol))
addSymSortRef' SrcSpan
sp s
rc Int
i RPVar
p RTProp RTyCon RTyVar (UReftV Symbol (ReftV Symbol))
r

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

addSymSortRef' SrcSpan
sp s
rc Int
i RPVar
p (RProp [(Symbol, RType RTyCon RTyVar ())]
_ (RHole r :: UReftV Symbol (ReftV Symbol)
r@(MkUReft ReftV Symbol
_ (Pr [UsedPVar
up]))))
  | [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [RType RTyCon RTyVar ()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType RTyCon RTyVar ()]
ts
  = [(Symbol, RType RTyCon RTyVar ())]
-> SpecType -> RTProp RTyCon RTyVar (UReftV Symbol (ReftV Symbol))
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
xts (UReftV Symbol (ReftV Symbol) -> SpecType
forall v c tv r. r -> RTypeV v c tv r
RHole UReftV Symbol (ReftV Symbol)
r)
  | Bool
otherwise
  = -- Misc.errorP "ZONK" $ F.showpp (rc, pname up, i, length xs, length ts)
    UserError -> RTProp RTyCon RTyVar (UReftV Symbol (ReftV Symbol))
forall a. UserError -> a
uError (UserError -> RTProp RTyCon RTyVar (UReftV Symbol (ReftV Symbol)))
-> UserError -> RTProp RTyCon RTyVar (UReftV Symbol (ReftV Symbol))
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 v t. PVarV v t -> Symbol
pname UsedPVar
up) Int
i ([Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
xs) ([RType RTyCon RTyVar ()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType RTyCon RTyVar ()]
ts)
    where
      xts :: [(Symbol, RType RTyCon RTyVar ())]
xts = [Char]
-> [Symbol]
-> [RType RTyCon RTyVar ()]
-> [(Symbol, RType RTyCon RTyVar ())]
forall t t1. [Char] -> [t] -> [t1] -> [(t, t1)]
Misc.safeZipWithError [Char]
"addSymSortRef'" [Symbol]
xs [RType RTyCon RTyVar ()]
ts
      xs :: [Symbol]
xs  = ((), Symbol, Expr) -> Symbol
forall a b c. (a, b, c) -> b
Misc.snd3 (((), Symbol, Expr) -> Symbol) -> [((), Symbol, Expr)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UsedPVar -> [((), Symbol, Expr)]
forall v t. PVarV v t -> [(t, Symbol, ExprV v)]
pargs UsedPVar
up
      ts :: [RType RTyCon RTyVar ()]
ts  = (RType RTyCon RTyVar (), Symbol, Expr) -> RType RTyCon RTyVar ()
forall a b c. (a, b, c) -> a
Misc.fst3 ((RType RTyCon RTyVar (), Symbol, Expr) -> RType RTyCon RTyVar ())
-> [(RType RTyCon RTyVar (), Symbol, Expr)]
-> [RType RTyCon RTyVar ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RPVar -> [(RType RTyCon RTyVar (), Symbol, Expr)]
forall v t. PVarV v t -> [(t, Symbol, ExprV v)]
pargs RPVar
p

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

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

spliceArgs :: String  -> [(F.Symbol, b)] -> PVar t -> [(F.Symbol, t)]
spliceArgs :: forall b t. [Char] -> [(Symbol, b)] -> PVar t -> [(Symbol, t)]
spliceArgs [Char]
msg [(Symbol, b)]
syms PVar t
p = [Symbol] -> [(t, Symbol, Expr)] -> [(Symbol, t)]
forall {a} {b} {c}. Show a => [a] -> [(b, a, c)] -> [(a, b)]
go ((Symbol, b) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, b) -> Symbol) -> [(Symbol, b)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, b)]
syms) (PVar t -> [(t, Symbol, Expr)]
forall v t. PVarV v t -> [(t, Symbol, ExprV v)]
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 -> [Char] -> [(a, b)]
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char] -> [(a, b)]) -> [Char] -> [(a, b)]
forall a b. (a -> b) -> a -> b
$ [Char]
"spliceArgs: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"on XS=" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [a] -> [Char]
forall a. Show a => a -> [Char]
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])
-> [Bind Var]
-> HashMap Var (LocBareType, Maybe [Located Expr])
forall env acc.
CoreVisitor env acc -> env -> acc -> [Bind Var] -> 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 [Bind Var]
cbs
    cbs :: [Bind Var]
cbs                    = GhcSrc -> [Bind Var]
_giCbs (Env -> GhcSrc
reSrc Env
env)

replaceVisitor :: CoreVisitor SymMap SigMap
replaceVisitor :: CoreVisitor
  SymMap (HashMap Var (LocBareType, Maybe [Located Expr]))
replaceVisitor = 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])
-> CoreExpr
-> HashMap Var (LocBareType, Maybe [Located Expr])
exprF = \SymMap
_ HashMap Var (LocBareType, Maybe [Located Expr])
m CoreExpr
_ -> 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 ([Char]
-> (LocBareType, Maybe [Located Expr])
-> (LocBareType, Maybe [Located Expr])
forall a. PPrint a => [Char] -> a -> a
myTracepp ([Char]
"UPD-LOCAL-SIG " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Var -> [Char]
forall a. Outputable a => a -> [Char]
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
forall v. v -> ExprV v
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                     = RTypeRepV Symbol BTyCon BTyVar (UReftV Symbol (ReftV Symbol))
-> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds (BareType
-> RTypeRepV Symbol BTyCon BTyVar (UReftV Symbol (ReftV Symbol))
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep (LocBareType -> BareType
forall a. Located a -> a
F.val LocBareType
t))

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

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

---------------------------------------------------------------------------------
partitionLocalBinds :: [(Ghc.Var, a)] -> ([(Ghc.Var, a)], [(Ghc.Var, a)])
---------------------------------------------------------------------------------
partitionLocalBinds :: forall a. [(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)