-- | 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         #-}
{-# LANGUAGE TypeOperators         #-}

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

    -- * Resolving symbols
  , Lookup

  -- * Looking up names
  , lookupGhcDataConLHName
  , lookupGhcDnTyCon
  , lookupGhcIdLHName
  , lookupLetBoundVar
  , 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 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. 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.orphNamesOfExprs ([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 (Located BareType) (Located LHName) -> Symbol
forall {v} {ty} {ctor}. MeasureV v ty ctor -> Symbol
mbName (MeasureV Symbol (Located BareType) (Located LHName) -> Symbol)
-> [MeasureV Symbol (Located BareType) (Located LHName)]
-> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [MeasureV Symbol (Located BareType) (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 (Located BareType) () -> Symbol
forall {v} {ty} {ctor}. MeasureV v ty ctor -> Symbol
mbName (MeasureV Symbol (Located BareType) () -> Symbol)
-> [MeasureV Symbol (Located BareType) ()] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [MeasureV Symbol (Located BareType) ()]
forall lname ty. Spec lname ty -> [MeasureV lname (Located ty) ()]
cmeasures BareSpec
spec)
      [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (MeasureV Symbol (Located BareType) (Located LHName) -> Symbol
forall {v} {ty} {ctor}. MeasureV v ty ctor -> Symbol
mbName (MeasureV Symbol (Located BareType) (Located LHName) -> Symbol)
-> [MeasureV Symbol (Located BareType) (Located LHName)]
-> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [MeasureV Symbol (Located BareType) (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 (Located BareType) (Located LHName) -> Symbol
forall {v} {ty} {ctor}. MeasureV v ty ctor -> Symbol
mbName (MeasureV Symbol (Located BareType) (Located LHName) -> Symbol)
-> [MeasureV Symbol (Located BareType) (Located LHName)]
-> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [MeasureV Symbol (Located BareType) (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

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
x CoreExpr
e) = [Var] -> Bool -> Bool -> (Var, CoreExpr) -> [LocalVarDetails]
pgo [Var]
g Bool
True Bool
False (Var
x, 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] -> Bool -> Bool -> (Var, CoreExpr) -> [LocalVarDetails]
pgo [Var]
g Bool
True Bool
True) [(Var, CoreExpr)]
xes
    pgo :: [Var] -> Bool -> Bool -> (Var, CoreExpr) -> [LocalVarDetails]
pgo [Var]
g Bool
isTopLevel Bool
isRec (Var
x, CoreExpr
e) = [Var] -> Bool -> Bool -> Var -> LocalVarDetails
mkLocalVarDetails [Var]
g Bool
isTopLevel 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 -> Bool -> (Var, CoreExpr) -> [LocalVarDetails]
pgo [Var]
g Bool
False 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 -> Bool -> (Var, CoreExpr) -> [LocalVarDetails]
pgo [Var]
g Bool
False 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 -> Bool -> Var -> LocalVarDetails
mkLocalVarDetails [Var]
g Bool
isTopLevel 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
      , lvdIsTopLevel :: Bool
lvdIsTopLevel = Bool
isTopLevel
      , 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

-- | @lookupLetBoundVar@ yields the name of the closest let-bound definition.
--   See tests/names/pos/LocalSpec.hs for a motivating example.
--
-- This function never returns a top-level variable.
--
-- PRECONDITION: the input symbol is not qualified.
--
lookupLetBoundVar :: LocalVars -> LocSymbol -> Maybe Ghc.Var
lookupLetBoundVar :: LocalVars -> Located Symbol -> Maybe Var
lookupLetBoundVar LocalVars
localVars Located Symbol
lx
   | Symbol -> Bool
GM.isQualifiedSym Symbol
x = [Char] -> Maybe Var
forall a. HasCallStack => [Char] -> a
error ([Char] -> Maybe Var) -> [Char] -> Maybe Var
forall a b. (a -> b) -> a -> b
$ [Char]
"lookupLetBoundVar: called on a qualified symbol: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Located Symbol -> [Char]
forall a. Show a => a -> [Char]
show Located Symbol
lx
   | Bool
otherwise = SourcePos -> [LocalVarDetails] -> Maybe Var
findNearest SourcePos
lxn [LocalVarDetails]
kvs
  where
    x :: Symbol
x = Located Symbol -> Symbol
forall a. Located a -> a
F.val Located Symbol
lx
    kvs :: [LocalVarDetails]
kvs = [LocalVarDetails] -> [LocalVarDetails]
prioritizeRecBinds ([LocalVarDetails]
-> Symbol -> HashMap Symbol [LocalVarDetails] -> [LocalVarDetails]
forall k v. Hashable k => v -> k -> HashMap k v -> v
M.lookupDefault [] Symbol
x (LocalVars -> HashMap Symbol [LocalVarDetails]
lvSymbols LocalVars
localVars))
    lxn :: SourcePos
lxn = SrcSpan -> SourcePos
F.sp_start (SrcSpan -> SourcePos) -> SrcSpan -> SourcePos
forall a b. (a -> b) -> a -> b
$ Located Symbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan Located Symbol
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] -> [LocalVarDetails]
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]
recs [LocalVarDetails] -> [LocalVarDetails] -> [LocalVarDetails]
forall a. [a] -> [a] -> [a]
++ [LocalVarDetails]
nrecs

    findNearest :: F.SourcePos -> [LocalVarDetails] -> Maybe Ghc.Var
    findNearest :: SourcePos -> [LocalVarDetails] -> Maybe Var
findNearest SourcePos
key = SourcePos -> [LocalVarDetails] -> Maybe Var
pickByLocation SourcePos
key ([LocalVarDetails] -> Maybe Var)
-> ([LocalVarDetails] -> [LocalVarDetails])
-> [LocalVarDetails]
-> Maybe Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  (LocalVarDetails -> LocalVarDetails -> Ordering)
-> [LocalVarDetails] -> [LocalVarDetails]
forall a. (a -> a -> Ordering) -> [a] -> [a]
L.sortBy (SourcePos -> SourcePos -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (SourcePos -> SourcePos -> Ordering)
-> (LocalVarDetails -> SourcePos)
-> LocalVarDetails
-> LocalVarDetails
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` LocalVarDetails -> SourcePos
lvdSourcePos)

    pickByLocation :: F.SourcePos -> [LocalVarDetails] -> Maybe Ghc.Var
    pickByLocation :: SourcePos -> [LocalVarDetails] -> Maybe Var
pickByLocation SourcePos
_ [] = Maybe Var
forall a. Maybe a
Nothing
    pickByLocation SourcePos
_ [LocalVarDetails
lvd]
      | LocalVarDetails -> Bool
lvdIsTopLevel LocalVarDetails
lvd = Maybe Var
forall a. Maybe a
Nothing
      | Bool
otherwise = Var -> Maybe Var
forall a. a -> Maybe a
Just (Var -> Maybe Var) -> Var -> Maybe Var
forall a b. (a -> b) -> a -> b
$ LocalVarDetails -> Var
lvdVar LocalVarDetails
lvd
    pickByLocation SourcePos
key (LocalVarDetails
lvd0 : xs :: [LocalVarDetails]
xs@(LocalVarDetails
lvd1 : [LocalVarDetails]
_))
      | LocalVarDetails -> SourcePos
lvdSourcePos LocalVarDetails
lvd1 SourcePos -> SourcePos -> Bool
forall a. Ord a => a -> a -> Bool
< SourcePos
key  = SourcePos -> [LocalVarDetails] -> Maybe Var
pickByLocation SourcePos
key [LocalVarDetails]
xs
      | LocalVarDetails -> SourcePos
lvdSourcePos LocalVarDetails
lvd0 SourcePos -> SourcePos -> Bool
forall a. Ord a => a -> a -> Bool
< SourcePos
key  = SourcePos -> [LocalVarDetails] -> Maybe Var
pickByLocation SourcePos
key [LocalVarDetails
lvd1]
      | Bool
otherwise = SourcePos -> [LocalVarDetails] -> Maybe Var
pickByLocation SourcePos
key [LocalVarDetails
lvd0]


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 -> Located BareType -> 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])
-> (RTypeBV Symbol Symbol c tv r -> [c])
-> RTypeBV Symbol Symbol c tv r
-> [c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([c] -> RTypeBV Symbol Symbol c tv r -> [c])
-> [c] -> RTypeBV Symbol Symbol c tv r -> [c]
forall acc c tv r.
(acc -> RType c tv r -> acc) -> acc -> RType c tv r -> acc
foldRType [c] -> RTypeBV Symbol Symbol c tv r -> [c]
forall {a} {b} {v} {tv} {r}. [a] -> RTypeBV b v a tv r -> [a]
f []
  where
    f :: [a] -> RTypeBV b v a tv r -> [a]
f [a]
acc t :: RTypeBV b v a tv r
t@RApp {} = RTypeBV b v a tv r -> a
forall b v c tv r. RTypeBV b v c tv r -> c
rt_tycon RTypeBV b v a tv r
t a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
acc
    f [a]
acc RTypeBV b 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] -> Located Symbol -> Error
errResolve Doc
k [Char]
msg Located Symbol
lx = SrcSpan -> Doc -> Doc -> Doc -> Error
forall t. SrcSpan -> Doc -> Doc -> Doc -> TError t
ErrResolve (Located Symbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located Symbol
lx) Doc
k (Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint (Located Symbol -> Symbol
forall a. Located a -> a
F.val Located Symbol
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]
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> SourcePos
-> BareType
-> Lookup SpecType
forall r.
Expandable r =>
Env
-> ([Symbol] -> r -> r)
-> SourcePos
-> BRType r
-> Lookup (RRType r)
ofBRType Env
env ((UReftBV Symbol Symbol (ReftBV Symbol Symbol)
 -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> [Symbol]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall a b. a -> b -> a
const (SourcePos
-> Maybe [PVar BSort]
-> BareType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol 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
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
resolveReft SourcePos
l Maybe [PVar BSort]
ps BareType
t
        = SourcePos
-> ((UsedPVar -> UsedPVar)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> [UsedPVar]
-> BareType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall t c tv r.
SourcePos
-> ((UsedPVar -> UsedPVar) -> t) -> [UsedPVar] -> RType c tv r -> t
txParam SourcePos
l (UsedPVar -> UsedPVar)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol 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
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)
 -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> (UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol 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 = RTypeRepBV
  Symbol
  Symbol
  BTyCon
  BTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> [PVar BSort]
forall b v c tv r.
RTypeRepBV b v c tv r
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
ty_preds (BareType
-> RTypeRepBV
     Symbol
     Symbol
     BTyCon
     BTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep BareType
t)

fixReftTyVars :: BareType -> RReft -> RReft
fixReftTyVars :: BareType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
fixReftTyVars BareType
bt  = CoSub
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
coSubRReft CoSub
coSub
  where
    coSub :: CoSub
coSub         = [(Symbol, Sort)] -> CoSub
forall k v. 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
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
coSubRReft CoSub
su UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r = UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r { ur_reft = coSubReft su (ur_reft r) }

coSubReft :: F.CoSub -> F.Reft -> F.Reft
coSubReft :: CoSub -> ReftBV Symbol Symbol -> ReftBV Symbol Symbol
coSubReft CoSub
su (F.Reft (Symbol
x, Expr
e)) = (Symbol, Expr) -> ReftBV Symbol Symbol
forall b v. (b, ExprBV b v) -> ReftBV b 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 NoReft
ofBSort Env
env SourcePos
l BSort
t = ([Error] -> RType RTyCon RTyVar NoReft)
-> (RType RTyCon RTyVar NoReft -> RType RTyCon RTyVar NoReft)
-> Either [Error] (RType RTyCon RTyVar NoReft)
-> RType RTyCon RTyVar NoReft
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ([Char] -> [Char] -> RType RTyCon RTyVar NoReft
forall a. [Char] -> [Char] -> a
Misc.errorP [Char]
"error-ofBSort" ([Char] -> RType RTyCon RTyVar NoReft)
-> ([Error] -> [Char]) -> [Error] -> RType RTyCon RTyVar NoReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Error] -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp) RType RTyCon RTyVar NoReft -> RType RTyCon RTyVar NoReft
forall a. a -> a
id (HasCallStack =>
Env
-> SourcePos
-> BSort
-> Either [Error] (RType RTyCon RTyVar NoReft)
Env
-> SourcePos
-> BSort
-> Either [Error] (RType RTyCon RTyVar NoReft)
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 NoReft)
ofBSortE Env
env SourcePos
l BSort
t = Env
-> ([Symbol] -> NoReft -> NoReft)
-> SourcePos
-> BSort
-> Either [Error] (RType RTyCon RTyVar NoReft)
forall r.
Expandable r =>
Env
-> ([Symbol] -> r -> r)
-> SourcePos
-> BRType r
-> Lookup (RRType r)
ofBRType Env
env ((NoReft -> NoReft) -> [Symbol] -> NoReft -> NoReft
forall a b. a -> b -> a
const NoReft -> NoReft
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 NoReft) -> PVar BSort -> RPVar
forall a b.
(a -> b) -> PVarBV Symbol Symbol a -> PVarBV Symbol Symbol b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (HasCallStack =>
Env -> SourcePos -> BSort -> RType RTyCon RTyVar NoReft
Env -> SourcePos -> BSort -> RType RTyCon RTyVar NoReft
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 b v t. PVarBV b v t -> [(t, b, ExprBV b 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 b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs UsedPVar
π') (UsedPVar -> [((), Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs UsedPVar
π)
          | Bool
otherwise            = UsedPVar -> [((), Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs UsedPVar
π'
    π' :: UsedPVar
π'    = UsedPVar -> Maybe UsedPVar -> UsedPVar
forall a. a -> Maybe a -> a
Mb.fromMaybe UsedPVar
forall {b}. b
err (Maybe UsedPVar -> UsedPVar) -> Maybe UsedPVar -> UsedPVar
forall a b. (a -> b) -> a -> b
$ Symbol -> HashMap Symbol UsedPVar -> Maybe UsedPVar
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup (UsedPVar -> Symbol
forall b v t. PVarBV b v t -> b
pname UsedPVar
π) HashMap Symbol UsedPVar
m
    err :: b
err   = UserError -> b
forall a. UserError -> a
uError (UserError -> b) -> UserError -> b
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. Hashable k => [(k, v)] -> HashMap k v
M.fromList [(UsedPVar -> Symbol
forall b v t. PVarBV b v t -> b
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 = (PVarBV Symbol Symbol (RTypeBV Symbol Symbol c tv NoReft)
 -> UsedPVar)
-> [PVarBV Symbol Symbol (RTypeBV Symbol Symbol c tv NoReft)]
-> [UsedPVar]
forall a b. (a -> b) -> [a] -> [b]
map PVarBV Symbol Symbol (RTypeBV Symbol Symbol c tv NoReft)
-> UsedPVar
forall v t. PVarV v t -> UsedPVarV v
RT.uPVar ([PVarBV Symbol Symbol (RTypeBV Symbol Symbol c tv NoReft)]
 -> [UsedPVar])
-> (RTypeBV Symbol Symbol c tv r
    -> [PVarBV Symbol Symbol (RTypeBV Symbol Symbol c tv NoReft)])
-> RTypeBV Symbol Symbol c tv r
-> [UsedPVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeRepBV Symbol Symbol c tv r
-> [PVarBV Symbol Symbol (RTypeBV Symbol Symbol c tv NoReft)]
forall b v c tv r.
RTypeRepBV b v c tv r
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
ty_preds (RTypeRepBV Symbol Symbol c tv r
 -> [PVarBV Symbol Symbol (RTypeBV Symbol Symbol c tv NoReft)])
-> (RTypeBV Symbol Symbol c tv r
    -> RTypeRepBV Symbol Symbol c tv r)
-> RTypeBV Symbol Symbol c tv r
-> [PVarBV Symbol Symbol (RTypeBV Symbol Symbol c tv NoReft)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV Symbol Symbol c tv r -> RTypeRepBV Symbol Symbol c tv r
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep



--------------------------------------------------------------------------------
type Expandable r = ( PPrint r
                    , IsReft r
                    , ReftBind r ~ F.Symbol
                    , ReftVar r ~ F.Symbol
                    , F.Subable r
                    , F.Variable r ~ F.Symbol
                    , SubsTy RTyVar (RType RTyCon RTyVar NoReft) 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]
-> RTypeBV Symbol 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
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> r
-> Either [Error] (RType RTyCon RTyVar r)
goRFun [Symbol]
bs Symbol
x RFInfo
i RTypeBV Symbol Symbol BTyCon BTyVar r
t1 RTypeBV Symbol Symbol BTyCon BTyVar r
t2 r
r  = Symbol
-> RFInfo
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> r
-> RType RTyCon RTyVar r
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b 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
<$> (Variable (RType RTyCon RTyVar r)
-> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall {b} {v} {c} {tv} {r}.
(Variable (RTypeBV b v c tv r) ~ ReftBind r,
 Subable (RTypeBV b v c tv r), ToReft r) =>
Variable (RTypeBV b v c tv r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
rebind Symbol
Variable (RType RTyCon RTyVar r)
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]
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeBV Symbol 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]
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
bs) RTypeBV Symbol 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 :: Variable (RTypeBV b v c tv r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
rebind Variable (RTypeBV b v c tv r)
x RTypeBV b v c tv r
t              = RTypeBV b v c tv r
-> (Variable (RTypeBV b v c tv r),
    ExprBV
      (Variable (RTypeBV b v c tv r)) (Variable (RTypeBV b v c tv r)))
-> RTypeBV b v c tv r
forall a.
Subable a =>
a -> (Variable a, ExprBV (Variable a) (Variable a)) -> a
F.subst1 RTypeBV b v c tv r
t (Variable (RTypeBV b v c tv r)
x, Variable (RTypeBV b v c tv r)
-> ExprBV
     (Variable (RTypeBV b v c tv r)) (Variable (RTypeBV b v c tv r))
forall b v. v -> ExprBV b v
F.EVar (Variable (RTypeBV b v c tv r)
 -> ExprBV
      (Variable (RTypeBV b v c tv r)) (Variable (RTypeBV b v c tv r)))
-> Variable (RTypeBV b v c tv r)
-> ExprBV
     (Variable (RTypeBV b v c tv r)) (Variable (RTypeBV b v c tv r))
forall a b. (a -> b) -> a -> b
$ RTypeBV b v c tv r -> ReftBind r
forall r b v c tv.
(ToReft r, Binder (ReftBind r)) =>
RTypeBV b v c tv r -> ReftBind r
rTypeValueVar RTypeBV b v c tv r
t)
    go :: [Symbol]
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs (RAppTy RTypeBV Symbol Symbol BTyCon BTyVar r
t1 RTypeBV Symbol Symbol BTyCon BTyVar r
t2 r
r)  = RType RTyCon RTyVar r
-> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r
forall b v c tv r.
RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b 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]
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeBV Symbol 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]
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeBV Symbol 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 [RTypeBV Symbol Symbol BTyCon BTyVar r]
ts [RTPropBV Symbol Symbol BTyCon BTyVar r]
rs r
r) = [Symbol]
-> BTyCon
-> [RTypeBV Symbol Symbol BTyCon BTyVar r]
-> [RTPropBV Symbol Symbol BTyCon BTyVar r]
-> r
-> Either [Error] (RType RTyCon RTyVar r)
goRApp [Symbol]
bs BTyCon
tc [RTypeBV Symbol Symbol BTyCon BTyVar r]
ts [RTPropBV Symbol Symbol BTyCon BTyVar r]
rs r
r
    go [Symbol]
bs (RFun Symbol
x RFInfo
i RTypeBV Symbol Symbol BTyCon BTyVar r
t1 RTypeBV Symbol Symbol BTyCon BTyVar r
t2 r
r) = [Symbol]
-> Symbol
-> RFInfo
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> r
-> Either [Error] (RType RTyCon RTyVar r)
goRFun [Symbol]
bs Symbol
x RFInfo
i RTypeBV Symbol Symbol BTyCon BTyVar r
t1 RTypeBV Symbol Symbol BTyCon BTyVar r
t2 r
r
    go [Symbol]
bs (RVar BTyVar
a r
r)        = RTyVar -> r -> RType RTyCon RTyVar r
forall b v c tv r. tv -> r -> RTypeBV b 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 RTVUBV Symbol Symbol BTyCon BTyVar
a RTypeBV Symbol Symbol BTyCon BTyVar r
t r
r)     = RTVUBV Symbol Symbol RTyCon RTyVar
-> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT RTVUBV Symbol Symbol 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]
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeBV Symbol 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)
-> RTVUBV Symbol Symbol BTyCon BTyVar -> RTVar RTyVar BSort
forall tv1 tv2 s. (tv1 -> tv2) -> RTVar tv1 s -> RTVar tv2 s
mapTyVarValue BTyVar -> RTyVar
RT.bareRTyVar RTVUBV Symbol Symbol BTyCon BTyVar
a)
    go [Symbol]
bs (RAllP PVar BSort
a RTypeBV Symbol Symbol BTyCon BTyVar r
t)       = RPVar -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b 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]
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeBV Symbol 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 RTypeBV Symbol Symbol BTyCon BTyVar r
t1 RTypeBV Symbol Symbol BTyCon BTyVar r
t2)   = Symbol
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b 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]
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeBV Symbol 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]
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeBV Symbol Symbol BTyCon BTyVar r
t2
    go [Symbol]
bs (REx Symbol
x RTypeBV Symbol Symbol BTyCon BTyVar r
t1 RTypeBV Symbol Symbol BTyCon BTyVar r
t2)     = Symbol
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b 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]
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeBV Symbol 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]
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
bs) RTypeBV Symbol Symbol BTyCon BTyVar r
t2
    go [Symbol]
bs (RRTy [(Symbol, RTypeBV Symbol Symbol BTyCon BTyVar r)]
xts r
r Oblig
o RTypeBV Symbol Symbol BTyCon BTyVar r
t)  = [(Symbol, RType RTyCon RTyVar r)]
-> r -> Oblig -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall b v c tv r.
[(b, RTypeBV b v c tv r)]
-> r -> Oblig -> RTypeBV b v c tv r -> RTypeBV b 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]
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeBV Symbol Symbol BTyCon BTyVar r
t
      where xts' :: Either [Error] [(Symbol, RType RTyCon RTyVar r)]
xts'            = ((Symbol, RTypeBV Symbol Symbol BTyCon BTyVar r)
 -> Either [Error] (Symbol, RType RTyCon RTyVar r))
-> [(Symbol, RTypeBV Symbol 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 ((RTypeBV Symbol Symbol BTyCon BTyVar r
 -> Either [Error] (RType RTyCon RTyVar r))
-> (Symbol, RTypeBV Symbol 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]
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs)) [(Symbol, RTypeBV Symbol Symbol BTyCon BTyVar r)]
xts
    go [Symbol]
bs (RHole r
r)         = r -> RType RTyCon RTyVar r
forall b v c tv r. r -> RTypeBV b 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 b v c tv r. Located (ExprBV b v) -> RTypeBV b v c tv r
RExprArg Located Expr
le
    goRef :: [Symbol]
-> RTPropBV Symbol Symbol BTyCon BTyVar r
-> Either [Error] (RTProp RTyCon RTyVar r)
goRef [Symbol]
bs (RProp [(Symbol, BSort)]
ss (RHole r
r)) = [(Symbol, RType RTyCon RTyVar NoReft)]
-> r -> RTProp RTyCon RTyVar r
forall b τ r v c tv. [(b, τ)] -> r -> RefB b τ (RTypeV v c tv r)
rPropP ([(Symbol, RType RTyCon RTyVar NoReft)]
 -> r -> RTProp RTyCon RTyVar r)
-> Either [Error] [(Symbol, RType RTyCon RTyVar NoReft)]
-> 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 NoReft))
-> [(Symbol, BSort)]
-> Either [Error] [(Symbol, RType RTyCon RTyVar NoReft)]
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 NoReft)
forall {t}.
(t, BSort) -> Either [Error] (t, RType RTyCon RTyVar NoReft)
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 RTypeBV Symbol Symbol BTyCon BTyVar r
t)         = [(Symbol, RType RTyCon RTyVar NoReft)]
-> RType RTyCon RTyVar r -> RTProp RTyCon RTyVar r
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp  ([(Symbol, RType RTyCon RTyVar NoReft)]
 -> RType RTyCon RTyVar r -> RTProp RTyCon RTyVar r)
-> Either [Error] [(Symbol, RType RTyCon RTyVar NoReft)]
-> 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 NoReft))
-> [(Symbol, BSort)]
-> Either [Error] [(Symbol, RType RTyCon RTyVar NoReft)]
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 NoReft)
forall {t}.
(t, BSort) -> Either [Error] (t, RType RTyCon RTyVar NoReft)
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]
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs RTypeBV Symbol Symbol BTyCon BTyVar r
t
    goSyms :: (t, BSort) -> Either [Error] (t, RType RTyCon RTyVar NoReft)
goSyms (t
x, BSort
t)                 = (t
x,) (RType RTyCon RTyVar NoReft -> (t, RType RTyCon RTyVar NoReft))
-> Either [Error] (RType RTyCon RTyVar NoReft)
-> Either [Error] (t, RType RTyCon RTyVar NoReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HasCallStack =>
Env
-> SourcePos
-> BSort
-> Either [Error] (RType RTyCon RTyVar NoReft)
Env
-> SourcePos
-> BSort
-> Either [Error] (RType RTyCon RTyVar NoReft)
ofBSortE Env
env SourcePos
l BSort
t
    goRApp :: [Symbol]
-> BTyCon
-> [RTypeBV Symbol Symbol BTyCon BTyVar r]
-> [RTPropBV Symbol Symbol BTyCon BTyVar r]
-> r
-> Either [Error] (RType RTyCon RTyVar r)
goRApp [Symbol]
bs BTyCon
tc [RTypeBV Symbol Symbol BTyCon BTyVar r]
ts [RTPropBV Symbol 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
<*> (RTPropBV Symbol Symbol BTyCon BTyVar r
 -> Either [Error] (RTProp RTyCon RTyVar r))
-> [RTPropBV Symbol 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]
-> RTPropBV Symbol Symbol BTyCon BTyVar r
-> Either [Error] (RTProp RTyCon RTyVar r)
goRef [Symbol]
bs) [RTPropBV Symbol 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
<*> (RTypeBV Symbol Symbol BTyCon BTyVar r
 -> Either [Error] (RType RTyCon RTyVar r))
-> [RTypeBV Symbol 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]
-> RTypeBV Symbol Symbol BTyCon BTyVar r
-> Either [Error] (RType RTyCon RTyVar r)
go [Symbol]
bs) [RTypeBV Symbol 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.
Meet r =>
RType c tv r
-> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
tyApp ([(RTyVar, RType RTyCon RTyVar NoReft, RType RTyCon RTyVar r)]
-> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall tv (t :: * -> *) r c b v.
(Eq tv, Foldable t, Hashable tv, IsReft r, TyConable c, Binder b,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) c,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) r,
 SubsTy
   tv (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv (NoReftB b)),
 FreeVar c tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) tv,
 SubsTy
   tv
   (RTypeBV b v c tv (NoReftB b))
   (RTVar tv (RTypeBV b v c tv (NoReftB b)))) =>
t (tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
RT.subsTyVarsMeet [(RTyVar, RType RTyCon RTyVar NoReft, 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. IsReft 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 NoReft, RType RTyCon RTyVar r)]
su  = (Var
 -> RType RTyCon RTyVar r
 -> (RTyVar, RType RTyCon RTyVar NoReft, RType RTyCon RTyVar r))
-> [Var]
-> [RType RTyCon RTyVar r]
-> [(RTyVar, RType RTyCon RTyVar NoReft, 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 NoReft
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
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 b v tv.
(ToReft r, TyConable c, Binder b, ReftBind r ~ b) =>
RTypeBV b v 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 b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b 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 r. IsReft r => r
trueReft

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 :: Meet r => RType c tv r -> [RType c tv r] -> [RTProp c tv r] -> r
      -> RType c tv r
tyApp :: forall r c tv.
Meet r =>
RType c tv r
-> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
tyApp (RApp c
c [RTypeBV Symbol Symbol c tv r]
ts [RTPropBV Symbol Symbol c tv r]
rs r
r) [RTypeBV Symbol Symbol c tv r]
ts' [RTPropBV Symbol Symbol c tv r]
rs' r
r' = c
-> [RTypeBV Symbol Symbol c tv r]
-> [RTPropBV Symbol Symbol c tv r]
-> r
-> RTypeBV Symbol Symbol c tv r
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp c
c ([RTypeBV Symbol Symbol c tv r]
ts [RTypeBV Symbol Symbol c tv r]
-> [RTypeBV Symbol Symbol c tv r] -> [RTypeBV Symbol Symbol c tv r]
forall a. [a] -> [a] -> [a]
++ [RTypeBV Symbol Symbol c tv r]
ts') ([RTPropBV Symbol Symbol c tv r]
rs [RTPropBV Symbol Symbol c tv r]
-> [RTPropBV Symbol Symbol c tv r]
-> [RTPropBV Symbol Symbol c tv r]
forall a. [a] -> [a] -> [a]
++ [RTPropBV Symbol Symbol c tv r]
rs') (r
r r -> r -> r
forall r. Meet r => r -> r -> r
`meet` r
r')
tyApp RTypeBV Symbol Symbol c tv r
t                []  []  r
r  = RTypeBV Symbol Symbol c tv r
t RTypeBV Symbol Symbol c tv r -> r -> RTypeBV Symbol Symbol c tv r
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
`RT.strengthen` r
r
tyApp RTypeBV Symbol Symbol c tv r
_                 [RTypeBV Symbol Symbol c tv r]
_  [RTPropBV Symbol Symbol c tv r]
_   r
_  = Maybe SrcSpan -> [Char] -> RTypeBV Symbol 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 -> RType RTyCon RTyVar r
forall r. IsReft r => Type -> RRType r
RT.ofType (Type -> RType RTyCon RTyVar r)
-> (RType RTyCon RTyVar r -> Type)
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
Ghc.expandTypeSynonyms (Type -> Type)
-> (RType RTyCon RTyVar r -> Type) -> RType RTyCon RTyVar r -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> RType RTyCon RTyVar 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 -> Located SpecType -> Located SpecType
txRefSort TyConMap
tyi TCEmb TyCon
tce Located SpecType
t = Located SpecType -> SpecType -> Located SpecType
forall l b. Loc l => l -> b -> Located b
F.atLoc Located SpecType
t (SpecType -> Located SpecType) -> SpecType -> Located SpecType
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 (Located SpecType -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located SpecType
t) TCEmb TyCon
tce TyConMap
tyi) (Located SpecType -> SpecType
forall a. Located a -> a
val Located SpecType
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 [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
rs UReftBV Symbol Symbol (ReftBV Symbol Symbol)
rr)
  = RTyCon
-> [SpecType]
-> [RTPropBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> SpecType
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp RTyCon
rc [SpecType]
ts ((RPVar
 -> RTPropBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
 -> Int
 -> RTPropBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> [RPVar]
-> [RTPropBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> [Int]
-> [RTPropBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 (SrcSpan
-> RTyCon
-> RPVar
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Int
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall s.
PPrint s =>
SrcSpan
-> s
-> RPVar
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Int
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
addSymSortRef SrcSpan
sp RTyCon
rc) [RPVar]
pvs [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
rargs [Int
1..]) UReftBV Symbol Symbol (ReftBV Symbol 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'
    ([RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
rargs, [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
rrest)     = Int
-> [RTPropBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> ([RTPropBV
       Symbol
       Symbol
       RTyCon
       RTyVar
       (UReftBV Symbol Symbol (ReftBV Symbol Symbol))],
    [RTPropBV
       Symbol
       Symbol
       RTyCon
       RTyVar
       (UReftBV Symbol Symbol (ReftBV Symbol 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) [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
rs
    r2 :: UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r2                 = (UReftBV Symbol Symbol (ReftBV Symbol Symbol)
 -> RTPropBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
 -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> [RTPropBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> UReftBV Symbol Symbol (ReftBV Symbol 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' UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall {r} {b} {τ} {b} {v} {c} {tv}.
(Meet r, Monoid r) =>
r -> RefB b τ (RTypeBV b v c tv r) -> r
go UReftBV Symbol Symbol (ReftBV Symbol Symbol)
rr [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
rrest
    go :: r -> RefB b τ (RTypeBV b v c tv r) -> r
go r
r (RProp [(b, τ)]
_ (RHole r
r')) = r
r' r -> r -> r
forall r. Meet r => r -> r -> r
`meet` r
r
    go r
r (RProp  [(b, τ)]
_ RTypeBV b v 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 (RTypeBV b v c tv r -> Maybe r
forall b v c tv r. RTypeBV b v c tv r -> Maybe r
stripRTypeBase RTypeBV b v c tv r
t') in r
r r -> r -> r
forall r. Meet 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
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Int
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
addSymSortRef SrcSpan
sp s
rc RPVar
p RTPropBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
r Int
i = SrcSpan
-> s
-> Int
-> RPVar
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall s.
PPrint s =>
SrcSpan
-> s
-> Int
-> RPVar
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
addSymSortRef' SrcSpan
sp s
rc Int
i RPVar
p RTPropBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
r

addSymSortRef' :: (PPrint s) => Ghc.SrcSpan -> s -> Int -> RPVar -> SpecProp -> SpecProp
addSymSortRef' :: forall s.
PPrint s =>
SrcSpan
-> s
-> Int
-> RPVar
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
addSymSortRef' SrcSpan
sp s
rc Int
i RPVar
p (RProp [(Symbol, RType RTyCon RTyVar NoReft)]
s (RVar RTyVar
v UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)) | RTyVar -> Bool
forall a. Symbolic a => a -> Bool
isDummy RTyVar
v
  = if [(Symbol, RType RTyCon RTyVar NoReft)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RType RTyCon RTyVar NoReft)]
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> [(RType RTyCon RTyVar NoReft, Symbol, Expr)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (RPVar -> [(RType RTyCon RTyVar NoReft, Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs RPVar
p)
    then UserError
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall a. UserError -> a
uError (UserError
 -> RTPropBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> UserError
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol 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
$ RPVar -> Symbol
forall b v t. PVarBV b v t -> b
pname RPVar
p) Int
i ([(RType RTyCon RTyVar NoReft, Symbol, Expr)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (RPVar -> [(RType RTyCon RTyVar NoReft, Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs RPVar
p) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ([(Symbol, RType RTyCon RTyVar NoReft)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RType RTyCon RTyVar NoReft)]
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
    else [(Symbol, RType RTyCon RTyVar NoReft)]
-> SpecType
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, RType RTyCon RTyVar NoReft)]
xs SpecType
t
    where
      -- When the lambda provides fewer args than the PVar expects,
      -- the lambda's refinement variable (last lambda arg) should bind
      -- to the next PVar parameter position, not to the value type.
      -- e.g. for p :: a -> a -> b -> Bool, {\x y -> x >= y} should
      -- bind x→arg1, y→arg2 (not y→value).
      nLambdaArgs :: Int
nLambdaArgs = [(Symbol, RType RTyCon RTyVar NoReft)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RType RTyCon RTyVar NoReft)]
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1  -- s bindings + 1 refvar
      nPVarArgs :: Int
nPVarArgs   = [(RType RTyCon RTyVar NoReft, Symbol, Expr)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (RPVar -> [(RType RTyCon RTyVar NoReft, Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs RPVar
p) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1  -- pargs + 1 value
      ([(Symbol, RType RTyCon RTyVar NoReft)]
s', UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r')
        | Int
nLambdaArgs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
nPVarArgs
        , MkUReft (F.Reft (Symbol
rv, Expr
body)) PredicateBV Symbol Symbol
prd <- UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
        = -- Promote the refvar to a regular binding; the body still refers
          -- to rv which now names the (length s + 1)th PVar arg.
          -- Use a fresh vv as the Reft binder (value variable).
          let vv :: Symbol
vv    = Maybe Integer -> Symbol
F.vv (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0)
              -- Sort placeholder; spliceArgs replaces it with the PVar's sort
              dSort :: RType RTyCon RTyVar NoReft
dSort = (RType RTyCon RTyVar NoReft, Symbol, Expr)
-> RType RTyCon RTyVar NoReft
forall a b c. (a, b, c) -> a
Misc.fst3 ([(RType RTyCon RTyVar NoReft, Symbol, Expr)]
-> (RType RTyCon RTyVar NoReft, Symbol, Expr)
forall a. HasCallStack => [a] -> a
last (RPVar -> [(RType RTyCon RTyVar NoReft, Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs RPVar
p))
          in ([(Symbol, RType RTyCon RTyVar NoReft)]
s [(Symbol, RType RTyCon RTyVar NoReft)]
-> [(Symbol, RType RTyCon RTyVar NoReft)]
-> [(Symbol, RType RTyCon RTyVar NoReft)]
forall a. [a] -> [a] -> [a]
++ [(Symbol
rv, RType RTyCon RTyVar NoReft
dSort)], ReftBV Symbol Symbol
-> PredicateBV Symbol Symbol
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ((Symbol, Expr) -> ReftBV Symbol Symbol
forall b v. (b, ExprBV b v) -> ReftBV b v
F.Reft (Symbol
vv, Expr
body)) PredicateBV Symbol Symbol
prd)
        | Bool
otherwise
        = ([(Symbol, RType RTyCon RTyVar NoReft)]
s, UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)
      t :: SpecType
t  = RType RTyCon RTyVar NoReft -> SpecType
forall r b v c tv.
IsReft r =>
RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv r
ofRSort (RPVar -> RType RTyCon RTyVar NoReft
forall b v t. PVarBV b v t -> t
pvType RPVar
p) SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> SpecType
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
`RT.strengthen` UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r'
      xs :: [(Symbol, RType RTyCon RTyVar NoReft)]
xs = [Char]
-> [(Symbol, RType RTyCon RTyVar NoReft)]
-> RPVar
-> [(Symbol, RType RTyCon RTyVar NoReft)]
forall b t. [Char] -> [(Symbol, b)] -> PVar t -> [(Symbol, t)]
spliceArgs [Char]
"addSymSortRef 1" [(Symbol, RType RTyCon RTyVar NoReft)]
s' RPVar
p

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

addSymSortRef' SrcSpan
_ s
_ Int
_ RPVar
_ (RProp [(Symbol, RType RTyCon RTyVar NoReft)]
s (RHole UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r))
  = [(Symbol, RType RTyCon RTyVar NoReft)]
-> SpecType
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, RType RTyCon RTyVar NoReft)]
s (UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> SpecType
forall b v c tv r. r -> RTypeBV b v c tv r
RHole UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)

addSymSortRef' SrcSpan
sp s
rc Int
i RPVar
p (RProp [(Symbol, RType RTyCon RTyVar NoReft)]
s SpecType
t)
  = if [(Symbol, RType RTyCon RTyVar NoReft)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RType RTyCon RTyVar NoReft)]
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> [(RType RTyCon RTyVar NoReft, Symbol, Expr)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (RPVar -> [(RType RTyCon RTyVar NoReft, Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs RPVar
p)
    then UserError
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall a. UserError -> a
uError (UserError
 -> RTPropBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> UserError
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol 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
$ RPVar -> Symbol
forall b v t. PVarBV b v t -> b
pname RPVar
p) Int
i ([(RType RTyCon RTyVar NoReft, Symbol, Expr)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (RPVar -> [(RType RTyCon RTyVar NoReft, Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs RPVar
p) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ([(Symbol, RType RTyCon RTyVar NoReft)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RType RTyCon RTyVar NoReft)]
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
    else [(Symbol, RType RTyCon RTyVar NoReft)]
-> SpecType
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, RType RTyCon RTyVar NoReft)]
xs SpecType
t
    where
      xs :: [(Symbol, RType RTyCon RTyVar NoReft)]
xs = [Char]
-> [(Symbol, RType RTyCon RTyVar NoReft)]
-> RPVar
-> [(Symbol, RType RTyCon RTyVar NoReft)]
forall b t. [Char] -> [(Symbol, b)] -> PVar t -> [(Symbol, t)]
spliceArgs [Char]
"addSymSortRef 2" [(Symbol, RType RTyCon RTyVar NoReft)]
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 b v t. PVarBV b v t -> [(t, b, ExprBV b 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, Located BareType, Maybe [Located Expr])]
-> [(Var, Located BareType, Maybe [Located Expr])]
resolveLocalBinds Env
env [(Var, Located BareType, Maybe [Located Expr])]
xtes = [ (Var
x,Located BareType
t,Maybe [Located Expr]
es) | (Var
x, (Located BareType
t, Maybe [Located Expr]
es)) <- [(Var, (Located BareType, Maybe [Located Expr]))]
topTs [(Var, (Located BareType, Maybe [Located Expr]))]
-> [(Var, (Located BareType, Maybe [Located Expr]))]
-> [(Var, (Located BareType, Maybe [Located Expr]))]
forall a. [a] -> [a] -> [a]
++ [(Var, (Located BareType, Maybe [Located Expr]))]
-> [(Var, (Located BareType, Maybe [Located Expr]))]
replace [(Var, (Located BareType, Maybe [Located Expr]))]
locTs ]
  where
    ([(Var, (Located BareType, Maybe [Located Expr]))]
locTs, [(Var, (Located BareType, Maybe [Located Expr]))]
topTs)         = [(Var, (Located BareType, Maybe [Located Expr]))]
-> ([(Var, (Located BareType, Maybe [Located Expr]))],
    [(Var, (Located BareType, Maybe [Located Expr]))])
forall a. [(Var, a)] -> ([(Var, a)], [(Var, a)])
partitionLocalBinds [ (Var
x, (Located BareType
t, Maybe [Located Expr]
es)) | (Var
x, Located BareType
t, Maybe [Located Expr]
es) <- [(Var, Located BareType, Maybe [Located Expr])]
xtes]
    replace :: [(Var, (Located BareType, Maybe [Located Expr]))]
-> [(Var, (Located BareType, Maybe [Located Expr]))]
replace                = HashMap Var (Located BareType, Maybe [Located Expr])
-> [(Var, (Located BareType, Maybe [Located Expr]))]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Var (Located BareType, Maybe [Located Expr])
 -> [(Var, (Located BareType, Maybe [Located Expr]))])
-> ([(Var, (Located BareType, Maybe [Located Expr]))]
    -> HashMap Var (Located BareType, Maybe [Located Expr]))
-> [(Var, (Located BareType, Maybe [Located Expr]))]
-> [(Var, (Located BareType, Maybe [Located Expr]))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap Var (Located BareType, Maybe [Located Expr])
-> HashMap Var (Located BareType, Maybe [Located Expr])
replaceSigs (HashMap Var (Located BareType, Maybe [Located Expr])
 -> HashMap Var (Located BareType, Maybe [Located Expr]))
-> ([(Var, (Located BareType, Maybe [Located Expr]))]
    -> HashMap Var (Located BareType, Maybe [Located Expr]))
-> [(Var, (Located BareType, Maybe [Located Expr]))]
-> HashMap Var (Located BareType, Maybe [Located Expr])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Var, (Located BareType, Maybe [Located Expr]))]
-> HashMap Var (Located BareType, Maybe [Located Expr])
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList
    replaceSigs :: HashMap Var (Located BareType, Maybe [Located Expr])
-> HashMap Var (Located BareType, Maybe [Located Expr])
replaceSigs HashMap Var (Located BareType, Maybe [Located Expr])
sigm       = CoreVisitor
  SymMap (HashMap Var (Located BareType, Maybe [Located Expr]))
-> SymMap
-> HashMap Var (Located BareType, Maybe [Located Expr])
-> [Bind Var]
-> HashMap Var (Located BareType, Maybe [Located Expr])
forall env acc.
CoreVisitor env acc -> env -> acc -> [Bind Var] -> acc
coreVisitor CoreVisitor
  SymMap (HashMap Var (Located BareType, Maybe [Located Expr]))
replaceVisitor SymMap
forall k v. HashMap k v
M.empty HashMap Var (Located BareType, 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 (Located BareType, Maybe [Located Expr]))
replaceVisitor = CoreVisitor
  { envF :: SymMap -> Var -> SymMap
envF  = SymMap -> Var -> SymMap
addBind
  , bindF :: SymMap
-> HashMap Var (Located BareType, Maybe [Located Expr])
-> Var
-> HashMap Var (Located BareType, Maybe [Located Expr])
bindF = SymMap
-> HashMap Var (Located BareType, Maybe [Located Expr])
-> Var
-> HashMap Var (Located BareType, Maybe [Located Expr])
updSigMap
  , exprF :: SymMap
-> HashMap Var (Located BareType, Maybe [Located Expr])
-> CoreExpr
-> HashMap Var (Located BareType, Maybe [Located Expr])
exprF = \SymMap
_ HashMap Var (Located BareType, Maybe [Located Expr])
m CoreExpr
_ -> HashMap Var (Located BareType, 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. 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 (Located BareType, Maybe [Located Expr])
-> Var
-> HashMap Var (Located BareType, Maybe [Located Expr])
updSigMap SymMap
env HashMap Var (Located BareType, Maybe [Located Expr])
m Var
v = case Var
-> HashMap Var (Located BareType, Maybe [Located Expr])
-> Maybe (Located BareType, Maybe [Located Expr])
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Var
v HashMap Var (Located BareType, Maybe [Located Expr])
m of
  Maybe (Located BareType, Maybe [Located Expr])
Nothing  -> HashMap Var (Located BareType, Maybe [Located Expr])
m
  Just (Located BareType, Maybe [Located Expr])
tes -> Var
-> (Located BareType, Maybe [Located Expr])
-> HashMap Var (Located BareType, Maybe [Located Expr])
-> HashMap Var (Located BareType, Maybe [Located Expr])
forall k v. Hashable k => k -> v -> HashMap k v -> HashMap k v
M.insert Var
v ([Char]
-> (Located BareType, Maybe [Located Expr])
-> (Located BareType, 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) ((Located BareType, Maybe [Located Expr])
 -> (Located BareType, Maybe [Located Expr]))
-> (Located BareType, Maybe [Located Expr])
-> (Located BareType, Maybe [Located Expr])
forall a b. (a -> b) -> a -> b
$ SymMap
-> (Located BareType, Maybe [Located Expr])
-> (Located BareType, Maybe [Located Expr])
renameLocalSig SymMap
env (Located BareType, Maybe [Located Expr])
tes) HashMap Var (Located BareType, Maybe [Located Expr])
m

renameLocalSig :: SymMap -> (LocBareType, Maybe [Located F.Expr])
               -> (LocBareType, Maybe [Located F.Expr])
renameLocalSig :: SymMap
-> (Located BareType, Maybe [Located Expr])
-> (Located BareType, Maybe [Located Expr])
renameLocalSig SymMap
env (Located BareType
t, Maybe [Located Expr]
es) = ((Variable (Located BareType)
 -> ExprBV
      (Variable (Located BareType)) (Variable (Located BareType)))
-> Located BareType -> Located BareType
forall a.
Subable a =>
(Variable a -> ExprBV (Variable a) (Variable a)) -> a -> a
F.substf Symbol -> Expr
Variable (Located BareType)
-> ExprBV
     (Variable (Located BareType)) (Variable (Located BareType))
forall {b}. Symbol -> ExprBV b Symbol
tSub Located BareType
t, (Variable (Maybe [Located Expr])
 -> ExprBV
      (Variable (Maybe [Located Expr]))
      (Variable (Maybe [Located Expr])))
-> Maybe [Located Expr] -> Maybe [Located Expr]
forall a.
Subable a =>
(Variable a -> ExprBV (Variable a) (Variable a)) -> a -> a
F.substf Symbol -> Expr
Variable (Maybe [Located Expr])
-> ExprBV
     (Variable (Maybe [Located Expr])) (Variable (Maybe [Located Expr]))
forall {b}. Symbol -> ExprBV b Symbol
esSub Maybe [Located Expr]
es)
  where
    tSub :: Symbol -> ExprBV b Symbol
tSub                   = Symbol -> ExprBV b Symbol
forall b v. v -> ExprBV b v
F.EVar (Symbol -> ExprBV b Symbol)
-> (Symbol -> Symbol) -> Symbol -> ExprBV b Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymMap -> Symbol -> Symbol
qualifySymMap SymMap
env
    esSub :: Symbol -> ExprBV b Symbol
esSub                  = Symbol -> ExprBV b Symbol
forall {b}. Symbol -> ExprBV b Symbol
tSub (Symbol -> ExprBV b Symbol)
-> [Symbol] -> Symbol -> ExprBV b Symbol
forall v b. Eq v => (v -> ExprBV b v) -> [v] -> v -> ExprBV b v
`F.substfExcept` [Symbol]
xs
    xs :: [Symbol]
xs                     = RTypeRepBV
  Symbol
  Symbol
  BTyCon
  BTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> [Symbol]
forall b v c tv r. RTypeRepBV b v c tv r -> [b]
ty_binds (BareType
-> RTypeRepBV
     Symbol
     Symbol
     BTyCon
     BTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep (Located BareType -> BareType
forall a. Located a -> a
F.val Located BareType
t))

qualifySymMap :: SymMap -> F.Symbol -> F.Symbol
qualifySymMap :: SymMap -> Symbol -> Symbol
qualifySymMap SymMap
env Symbol
x = Symbol -> Symbol -> SymMap -> Symbol
forall k v. 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)