-- | This module provides functions to resolve names in specs.
--
-- There are two major namespaces in LH:
--
-- 1) The names of Haskell entities
-- 2) The names of logic entities
--
-- At the moment LH resolves names to Haskell entities, while resolving logic
-- entities remains work in progress.
--
-- Haskell entities include all functions that LH might reflect, or types that
-- might be referred in refinement types, type aliases or other annotations.
--
-- Logic entities include the names of reflected functions, inlined functions,
-- uninterpreted functions, predefined functions, local bindings, reflected data
-- constructors and parameters of Haskell functions in specs of other local
-- bindings.
--
-- The resolution pipeline goes as follows.
--
-- * First the module specs are parsed into a 'BareSpecParsed'.
--   Here all names are unresolved.
-- * Next the names of Haskell entities are resolved by 'resolveLHNames'.
--   For now, this pass doesn't change the type of the names.
-- * Next the names of logic entities are resolved. This pass produces
--   a 'BareSpecLHName', where 'Symbol's are replaced with 'LHName'.
--
-- 'BareSpecLHName' has an approximate bijection to 'BareSpec' via a 'LogicNameEnv'
-- which allows to convert 'LHName' to an unambiguous form of 'Symbol'
-- and back. The bijection is implemented with the functions 'toBareSpecLHName'
-- and 'fromBareSpecLHName'. This allows to use liquid-fixpoint functions
-- unmodified as they will continue to operate on (now unambiguous) Symbols.
-- The bijection is approximate because in the roundtrip the representation of
-- LHName's might change.
--
-- At the same time, the 'BareSpecLHName' form is kept to serialize and to
-- resolve names of modules that import the specs.
--

{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE NamedFieldPuns             #-}
{-# LANGUAGE TupleSections              #-}
{-# LANGUAGE TypeApplications           #-}

module Language.Haskell.Liquid.LHNameResolution
  ( resolveLHNames
  , resolveSymbolToTcName
  , exprArg
  , fromBareSpecLHName
  , toBareSpecLHName
  , symbolToLHName
  , LogicNameEnv(..)
  ) where

import qualified Liquid.GHC.API         as GHC hiding (Expr, panic)
import qualified Language.Haskell.Liquid.GHC.Interface   as LH
import qualified Language.Haskell.Liquid.GHC.Misc        as LH
import           Language.Haskell.Liquid.Types.Names
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp

import           Control.Monad.Except (ExceptT, runExceptT, throwError)
import           Control.Monad ((<=<), mplus, unless, void)
import           Control.Monad.Identity
import           Control.Monad.State.Strict
import           Data.Bifunctor (first, second)
import qualified Data.Char                               as Char
import           Data.Coerce (coerce)
import           Data.Data (Data, gmapM)
import           Data.Generics (extM)


import qualified Data.HashSet                            as HS
import qualified Data.HashMap.Strict                     as HM
import           Data.List (find, isSuffixOf, nubBy, partition)
import           Data.List.Extra (dropEnd)
import qualified Data.Map as Map
import           Data.Maybe (mapMaybe, maybeToList)
import qualified Data.Text                               as Text
import qualified GHC.Types.Name.Occurrence

import           Language.Fixpoint.Types as F hiding (Error, panic)
import qualified Language.Haskell.Liquid.Bare.Resolve as Resolve
import           Language.Haskell.Liquid.Bare.Types (LocalVars(lvNames), LocalVarDetails(lvdLclEnv))
import           Language.Fixpoint.Misc as Misc
import           Language.Haskell.Liquid.Name.LogicNameEnv
import qualified Language.Haskell.Liquid.Types.DataDecl as DataDecl
import           Language.Haskell.Liquid.Types.Errors (TError(ErrDupNames, ErrResolve), panic)
import           Language.Haskell.Liquid.Types.Specs as Specs
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.UX.Config
import           Language.Haskell.Liquid.WiredIn

import qualified Text.PrettyPrint.HughesPJ as PJ
import qualified Text.Printf               as Printf

-- | Collects type aliases from the current module and its dependencies.
--
-- By construction, type alises from transitive dependencies are neglected (see 'moduleAliases').
-- We do so because all type aliases in scope are added to the 'LiftedSpec' later.
-- Aliases with the same unqualified name coexist during name resolution,
-- as long as we have a means to disambiguate (namely, by qualifing the import).
-- In this case, when building the 'LiftedSpec' we carry only the first such alias according
-- to lexicographic order.
collectTypeAliases
  :: GHC.ImportedMods
  -> GHC.Module
  -> BareSpecParsed
  -> TargetDependencies
  -> InScopeEnv (RTAlias Symbol ())
collectTypeAliases :: ImportedMods
-> GenModule Unit
-> Spec LocSymbol BareTypeParsed
-> TargetDependencies
-> InScopeEnv (RTAlias Symbol ())
collectTypeAliases ImportedMods
impMods GenModule Unit
thisModule Spec LocSymbol BareTypeParsed
spec TargetDependencies
deps =
    let bsAliases :: InScopeEnv (RTAlias Symbol ())
bsAliases = GenModule Unit
-> ImportedMods
-> (GenModule Unit, [(LHName, RTAlias Symbol ())])
-> InScopeEnv (RTAlias Symbol ())
forall a.
GenModule Unit
-> ImportedMods -> (GenModule Unit, [(LHName, a)]) -> InScopeEnv a
mkAliasEnv GenModule Unit
thisModule ImportedMods
impMods (GenModule Unit
thisModule, [(LHName, RTAlias Symbol ())]
bsNames)
        bsNames :: [(LHName, RTAlias Symbol ())]
bsNames = [ (Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> (RTAlias Symbol BareTypeParsed -> Located LHName)
-> RTAlias Symbol BareTypeParsed
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias Symbol BareTypeParsed -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName (RTAlias Symbol BareTypeParsed -> LHName)
-> RTAlias Symbol BareTypeParsed -> LHName
forall a b. (a -> b) -> a -> b
$ RTAlias Symbol BareTypeParsed
rta, RTAlias Symbol BareTypeParsed -> RTAlias Symbol ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void RTAlias Symbol BareTypeParsed
rta) | RTAlias Symbol BareTypeParsed
rta <- Spec LocSymbol BareTypeParsed -> [RTAlias Symbol BareTypeParsed]
forall lname ty.
Spec lname ty -> [RTAlias Symbol (BareTypeV lname)]
aliases Spec LocSymbol BareTypeParsed
spec]
        depAliases :: [InScopeEnv (RTAlias Symbol ())]
depAliases = ((GenModule Unit, [(LHName, RTAlias Symbol ())])
 -> InScopeEnv (RTAlias Symbol ()))
-> [(GenModule Unit, [(LHName, RTAlias Symbol ())])]
-> [InScopeEnv (RTAlias Symbol ())]
forall a b. (a -> b) -> [a] -> [b]
map (GenModule Unit
-> ImportedMods
-> (GenModule Unit, [(LHName, RTAlias Symbol ())])
-> InScopeEnv (RTAlias Symbol ())
forall a.
GenModule Unit
-> ImportedMods -> (GenModule Unit, [(LHName, a)]) -> InScopeEnv a
mkAliasEnv GenModule Unit
thisModule ImportedMods
impMods) ([(GenModule Unit, [(LHName, RTAlias Symbol ())])]
 -> [InScopeEnv (RTAlias Symbol ())])
-> [(GenModule Unit, [(LHName, RTAlias Symbol ())])]
-> [InScopeEnv (RTAlias Symbol ())]
forall a b. (a -> b) -> a -> b
$
          [ (GenModule Unit
m, [(LHName, RTAlias Symbol ())]
depNames)
          | (StableModule
sm, LiftedSpec
lspec) <- HashMap StableModule LiftedSpec -> [(StableModule, LiftedSpec)]
forall k v. HashMap k v -> [(k, v)]
HM.toList (TargetDependencies -> HashMap StableModule LiftedSpec
getDependencies TargetDependencies
deps)
          , let m :: GenModule Unit
m = StableModule -> GenModule Unit
GHC.unStableModule StableModule
sm
          , let depNames :: [(LHName, RTAlias Symbol ())]
depNames = [ (Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> (RTAlias Symbol BareTypeLHName -> Located LHName)
-> RTAlias Symbol BareTypeLHName
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias Symbol BareTypeLHName -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName (RTAlias Symbol BareTypeLHName -> LHName)
-> RTAlias Symbol BareTypeLHName -> LHName
forall a b. (a -> b) -> a -> b
$ RTAlias Symbol BareTypeLHName
rta , RTAlias Symbol BareTypeLHName -> RTAlias Symbol ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void RTAlias Symbol BareTypeLHName
rta)
                           | RTAlias Symbol BareTypeLHName
rta <- HashSet (RTAlias Symbol BareTypeLHName)
-> [RTAlias Symbol BareTypeLHName]
forall a. HashSet a -> [a]
HS.toList (HashSet (RTAlias Symbol BareTypeLHName)
 -> [RTAlias Symbol BareTypeLHName])
-> HashSet (RTAlias Symbol BareTypeLHName)
-> [RTAlias Symbol BareTypeLHName]
forall a b. (a -> b) -> a -> b
$ LiftedSpec -> HashSet (RTAlias Symbol BareTypeLHName)
liftedAliases LiftedSpec
lspec
                           ]
          ]
     in
        [InScopeEnv (RTAlias Symbol ())] -> InScopeEnv (RTAlias Symbol ())
forall a. [InScopeEnv a] -> InScopeEnv a
unionAliasEnvs ([InScopeEnv (RTAlias Symbol ())]
 -> InScopeEnv (RTAlias Symbol ()))
-> [InScopeEnv (RTAlias Symbol ())]
-> InScopeEnv (RTAlias Symbol ())
forall a b. (a -> b) -> a -> b
$ InScopeEnv (RTAlias Symbol ())
bsAliases InScopeEnv (RTAlias Symbol ())
-> [InScopeEnv (RTAlias Symbol ())]
-> [InScopeEnv (RTAlias Symbol ())]
forall a. a -> [a] -> [a]
: [InScopeEnv (RTAlias Symbol ())]
depAliases

--------------------------------------------------------------------------------
-- | [NOTE:EXPRESSION-ALIASES]:
--
-- In a lifted spec, expression aliases include fully unfolded predicate,
-- inline, and define annotations. By contrast, a bare spec’s expression
-- aliases include only predicate aliases. This is because symbols from these
-- three kinds of annotations are unfolded uniformly in logical expressions
-- during spec lifting.
--
-- Inlines and defines are converted to expression aliases via 'lmapEalias',
-- which assigns them a 'GeneratedLogicName'. This allows us to distinguish
-- them from predicate aliases, which should be the only 'LogicName's among
-- expression aliases.
--
-- Here, we collect the symbols of inlines and defines from expression aliases
-- to identify their uses when resolving logic variable names.
-- This should be redundant when these aliases are resolved via the
-- logic environments and a dedicated lifted field for inlines is added.
--------------------------------------------------------------------------------
collectInlinesAndDefines:: TargetDependencies -> HS.HashSet Symbol
collectInlinesAndDefines :: TargetDependencies -> HashSet Symbol
collectInlinesAndDefines TargetDependencies
deps = [HashSet Symbol] -> HashSet Symbol
forall a. Eq a => [HashSet a] -> HashSet a
HS.unions
  [ (LHName -> Symbol) -> HashSet LHName -> HashSet Symbol
forall b a. Hashable b => (a -> b) -> HashSet a -> HashSet b
HS.map LHName -> Symbol
lhNameToResolvedSymbol HashSet LHName
depInlinesAndDefines
  | (StableModule
_, LiftedSpec
lspec) <- HashMap StableModule LiftedSpec -> [(StableModule, LiftedSpec)]
forall k v. HashMap k v -> [(k, v)]
HM.toList (TargetDependencies -> HashMap StableModule LiftedSpec
getDependencies TargetDependencies
deps)
  , let exprAliases :: HashSet LHName
exprAliases = (RTAlias Symbol (ExprV LHName) -> LHName)
-> HashSet (RTAlias Symbol (ExprV LHName)) -> HashSet LHName
forall b a. Hashable b => (a -> b) -> HashSet a -> HashSet b
HS.map (Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> (RTAlias Symbol (ExprV LHName) -> Located LHName)
-> RTAlias Symbol (ExprV LHName)
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias Symbol (ExprV LHName) -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName) (HashSet (RTAlias Symbol (ExprV LHName)) -> HashSet LHName)
-> HashSet (RTAlias Symbol (ExprV LHName)) -> HashSet LHName
forall a b. (a -> b) -> a -> b
$ LiftedSpec -> HashSet (RTAlias Symbol (ExprV LHName))
liftedEaliases LiftedSpec
lspec
        depInlinesAndDefines :: HashSet LHName
depInlinesAndDefines = (LHName -> Bool) -> HashSet LHName -> HashSet LHName
forall a. (a -> Bool) -> HashSet a -> HashSet a
HS.filter (Bool -> Bool
not (Bool -> Bool) -> (LHName -> Bool) -> LHName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LHName -> Bool
isResolvedLogicName) HashSet LHName
exprAliases
   ]

-- | Converts occurrences of LHNUnresolved to LHNResolved using the provided
-- type aliases and GlobalRdrEnv.
resolveLHNames
  :: Config
  -> GHC.Module
  -> LocalVars
  -> GHC.ImportedMods
  -> GHC.GlobalRdrEnv
  -> BareSpecParsed
  -> TargetDependencies
  -> Either [Error] (BareSpec, LogicNameEnv, LogicMap)
resolveLHNames :: Config
-> GenModule Unit
-> LocalVars
-> ImportedMods
-> GlobalRdrEnv
-> Spec LocSymbol BareTypeParsed
-> TargetDependencies
-> Either [Error] (BareSpec, LogicNameEnv, LogicMap)
resolveLHNames Config
cfg GenModule Unit
thisModule LocalVars
localVars ImportedMods
impMods GlobalRdrEnv
globalRdrEnv Spec LocSymbol BareTypeParsed
bareSpec0 TargetDependencies
dependencies =
  (StateT
   RenameOutput
   Identity
   (Either [Error] (BareSpec, LogicNameEnv, LogicMap))
 -> RenameOutput
 -> Either [Error] (BareSpec, LogicNameEnv, LogicMap))
-> RenameOutput
-> StateT
     RenameOutput
     Identity
     (Either [Error] (BareSpec, LogicNameEnv, LogicMap))
-> Either [Error] (BareSpec, LogicNameEnv, LogicMap)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT
  RenameOutput
  Identity
  (Either [Error] (BareSpec, LogicNameEnv, LogicMap))
-> RenameOutput
-> Either [Error] (BareSpec, LogicNameEnv, LogicMap)
forall s a. State s a -> s -> a
evalState RenameOutput { roErrors :: [Error]
roErrors = [], roUsedNames :: [LHName]
roUsedNames = [], roUsedDataCons :: HashSet LHName
roUsedDataCons = HashSet LHName
forall a. Monoid a => a
mempty } (StateT
   RenameOutput
   Identity
   (Either [Error] (BareSpec, LogicNameEnv, LogicMap))
 -> Either [Error] (BareSpec, LogicNameEnv, LogicMap))
-> StateT
     RenameOutput
     Identity
     (Either [Error] (BareSpec, LogicNameEnv, LogicMap))
-> Either [Error] (BareSpec, LogicNameEnv, LogicMap)
forall a b. (a -> b) -> a -> b
$
    ExceptT
  [Error]
  (StateT RenameOutput Identity)
  (BareSpec, LogicNameEnv, LogicMap)
-> StateT
     RenameOutput
     Identity
     (Either [Error] (BareSpec, LogicNameEnv, LogicMap))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT
   [Error]
   (StateT RenameOutput Identity)
   (BareSpec, LogicNameEnv, LogicMap)
 -> StateT
      RenameOutput
      Identity
      (Either [Error] (BareSpec, LogicNameEnv, LogicMap)))
-> ExceptT
     [Error]
     (StateT RenameOutput Identity)
     (BareSpec, LogicNameEnv, LogicMap)
-> StateT
     RenameOutput
     Identity
     (Either [Error] (BareSpec, LogicNameEnv, LogicMap))
forall a b. (a -> b) -> a -> b
$ do
      -- Prepare type aliases for resolution.
      sp0 <- StateT RenameOutput Identity (Spec LocSymbol BareTypeParsed)
-> ExceptT
     [Error]
     (StateT RenameOutput Identity)
     (Spec LocSymbol BareTypeParsed)
forall (m :: * -> *) a. Monad m => m a -> ExceptT [Error] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT RenameOutput Identity (Spec LocSymbol BareTypeParsed)
 -> ExceptT
      [Error]
      (StateT RenameOutput Identity)
      (Spec LocSymbol BareTypeParsed))
-> StateT RenameOutput Identity (Spec LocSymbol BareTypeParsed)
-> ExceptT
     [Error]
     (StateT RenameOutput Identity)
     (Spec LocSymbol BareTypeParsed)
forall a b. (a -> b) -> a -> b
$ InScopeEnv (RTAlias Symbol ())
-> Spec LocSymbol BareTypeParsed
-> StateT RenameOutput Identity (Spec LocSymbol BareTypeParsed)
fixExpressionArgsOfTypeAliases InScopeEnv (RTAlias Symbol ())
taliases (Spec LocSymbol BareTypeParsed
 -> StateT RenameOutput Identity (Spec LocSymbol BareTypeParsed))
-> Spec LocSymbol BareTypeParsed
-> StateT RenameOutput Identity (Spec LocSymbol BareTypeParsed)
forall a b. (a -> b) -> a -> b
$ Spec LocSymbol BareTypeParsed -> Spec LocSymbol BareTypeParsed
resolveBoundVarsInTypeAliases Spec LocSymbol BareTypeParsed
bareSpec0

      checkErrors

      -- First resolution pass: A generic traversal that resolves names
      -- of Haskell entities and type alias binders.
      sp1 <- lift $ mapMLocLHNames (\Located LHName
l -> (LHName -> Located LHName -> Located LHName
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Located LHName
l) (LHName -> Located LHName)
-> StateT RenameOutput Identity LHName
-> StateT RenameOutput Identity (Located LHName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located LHName -> StateT RenameOutput Identity LHName
resolveLHName Located LHName
l) sp0

      -- Data decls contain fieldnames that introduce measures with the
      -- same names. We resolve them before constructing the logic
      -- environments.
      dataDecls <- lift $ mapM (mapDataDeclFieldNamesM resolveFieldLogicName) (dataDecls sp1)
      let sp2 = Spec LocSymbol BareTypeParsed
sp1 {dataDecls}

      checkErrors

      -- Second resolution pass: a traversal to resolve logic names using the following
      -- lookup environments.
      let (inScopeEnv, logicNameEnv0, privateReflectNames) =
            makeLogicEnvs impMods thisModule sp2 dependencies

          -- Add resolved local defines to the logic map.
          lmap1 = LogicMap
lmap LogicMap -> LogicMap -> LogicMap
forall a. Semigroup a => a -> a -> a
<> HashMap Symbol LMap -> LogicMap
mkLogicMap ([(Symbol, LMap)] -> HashMap Symbol LMap
forall k v. Hashable k => [(k, v)] -> HashMap k v
HM.fromList ([(Symbol, LMap)] -> HashMap Symbol LMap)
-> [(Symbol, LMap)] -> HashMap Symbol LMap
forall a b. (a -> b) -> a -> b
$
                   [ (LocSymbol -> Symbol
forall a. Located a -> a
F.val (LocSymbol -> Symbol) -> LocSymbol -> Symbol
forall a b. (a -> b) -> a -> b
$ LHName -> Symbol
lhNameToResolvedSymbol (LHName -> Symbol) -> Located LHName -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located LHName
k,
                      (LocSymbol -> Symbol
forall a. Located a -> a
val (LocSymbol -> Symbol) -> LMapV LocSymbol -> LMap
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LMapV LocSymbol
v) { lmVar = lhNameToResolvedSymbol <$> k })
                   | (Located LHName
k,LMapV LocSymbol
v) <- Spec LocSymbol BareTypeParsed
-> [(Located LHName, LMapV LocSymbol)]
forall lname ty. Spec lname ty -> [(Located LHName, LMapV lname)]
defines Spec LocSymbol BareTypeParsed
sp2 ])
      sp3 <- lift $ fromBareSpecLHName <$>
                  resolveLogicNames
                    cfg
                    thisModule
                    inScopeEnv
                    globalRdrEnv
                    lmap1
                    localVars
                    logicNameEnv0
                    privateReflectNames
                    depsInlinesAndDefines
                    sp2

      checkErrors

      dcs <- gets roUsedDataCons
      return (sp3 { usedDataCons = dcs }, logicNameEnv0, lmap1)
  where
    -- Early exit name resolution if errors are found and pass them to the output.
    checkErrors :: ExceptT [Error] (StateT RenameOutput Identity) ()
    checkErrors :: ExceptT [Error] (StateT RenameOutput Identity) ()
checkErrors = do
      es <- (RenameOutput -> [Error])
-> ExceptT [Error] (StateT RenameOutput Identity) [Error]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets RenameOutput -> [Error]
roErrors
      unless (null es) (throwError es)

    -- We collect type aliases before resolving names so we have a means to disambiguate
    -- imported and local ones (according to their resolution status).
    taliases :: InScopeEnv (RTAlias Symbol ())
taliases = ImportedMods
-> GenModule Unit
-> Spec LocSymbol BareTypeParsed
-> TargetDependencies
-> InScopeEnv (RTAlias Symbol ())
collectTypeAliases ImportedMods
impMods GenModule Unit
thisModule Spec LocSymbol BareTypeParsed
bareSpec0 TargetDependencies
dependencies
    depsInlinesAndDefines :: HashSet Symbol
depsInlinesAndDefines = TargetDependencies -> HashSet Symbol
collectInlinesAndDefines TargetDependencies
dependencies

    -- Add defines from dependencies to the logical map.
    lmap :: LogicMap
lmap =
        (LogicMap
LH.listLMap LogicMap -> LogicMap -> LogicMap
forall a. Semigroup a => a -> a -> a
<>) (LogicMap -> LogicMap) -> LogicMap -> LogicMap
forall a b. (a -> b) -> a -> b
$
        [LogicMap] -> LogicMap
forall a. Monoid a => [a] -> a
mconcat ([LogicMap] -> LogicMap) -> [LogicMap] -> LogicMap
forall a b. (a -> b) -> a -> b
$
        (LiftedSpec -> LogicMap) -> [LiftedSpec] -> [LogicMap]
forall a b. (a -> b) -> [a] -> [b]
map (HashMap Symbol LMap -> LogicMap
mkLogicMap (HashMap Symbol LMap -> LogicMap)
-> (LiftedSpec -> HashMap Symbol LMap) -> LiftedSpec -> LogicMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LMapV LHName -> LMap)
-> HashMap Symbol (LMapV LHName) -> HashMap Symbol LMap
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HM.map ((LHName -> Symbol) -> LMapV LHName -> LMap
forall a b. (a -> b) -> LMapV a -> LMapV b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHName -> Symbol
lhNameToResolvedSymbol) (HashMap Symbol (LMapV LHName) -> HashMap Symbol LMap)
-> (LiftedSpec -> HashMap Symbol (LMapV LHName))
-> LiftedSpec
-> HashMap Symbol LMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LiftedSpec -> HashMap Symbol (LMapV LHName)
liftedDefines) ([LiftedSpec] -> [LogicMap]) -> [LiftedSpec] -> [LogicMap]
forall a b. (a -> b) -> a -> b
$
        HashMap StableModule LiftedSpec -> [LiftedSpec]
forall k v. HashMap k v -> [v]
HM.elems (HashMap StableModule LiftedSpec -> [LiftedSpec])
-> HashMap StableModule LiftedSpec -> [LiftedSpec]
forall a b. (a -> b) -> a -> b
$
        TargetDependencies -> HashMap StableModule LiftedSpec
getDependencies TargetDependencies
dependencies

    resolveFieldLogicName :: LHName -> StateT RenameOutput Identity LHName
resolveFieldLogicName LHName
n =
      case LHName
n of
        LHNUnresolved LHNameSpace
LHLogicNameBinder Symbol
s -> LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ Symbol -> GenModule Unit -> Maybe Name -> LHName
makeLogicLHName Symbol
s GenModule Unit
thisModule Maybe Name
forall a. Maybe a
Nothing
        LHName
_ -> Maybe SrcSpan -> [Char] -> StateT RenameOutput Identity LHName
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char] -> StateT RenameOutput Identity LHName)
-> [Char] -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ [Char]
"unexpected name: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ LHName -> [Char]
forall a. Show a => a -> [Char]
show LHName
n

    resolveLHName :: Located LHName -> StateT RenameOutput Identity LHName
resolveLHName Located LHName
lname =
      case Located LHName -> LHName
forall a. Located a -> a
val Located LHName
lname of
        LHNUnresolved (LHTcName LHThisModuleNameFlag
lcl) Symbol
s
          | Symbol -> Bool
forall c. TyConable c => c -> Bool
isTuple Symbol
s ->
            LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ LHResolvedName -> Symbol -> LHName
LHNResolved (Name -> LHResolvedName
LHRGHC (Name -> LHResolvedName) -> Name -> LHResolvedName
forall a b. (a -> b) -> a -> b
$ TupleSort -> Int -> Name
GHC.tupleTyConName TupleSort
GHC.BoxedTuple (Symbol -> Int
tupleArity Symbol
s)) Symbol
s
          | Symbol -> Bool
forall c. TyConable c => c -> Bool
isList Symbol
s ->
            LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ LHResolvedName -> Symbol -> LHName
LHNResolved (Name -> LHResolvedName
LHRGHC Name
GHC.listTyConName) Symbol
s
          | Symbol
s Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"*" ->
            LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ LHResolvedName -> Symbol -> LHName
LHNResolved (Name -> LHResolvedName
LHRGHC Name
GHC.liftedTypeKindTyConName) Symbol
s
          | Bool
otherwise ->
            case InScopeEnv (RTAlias Symbol ())
-> Symbol -> TypeAliasResolution (RTAlias Symbol ())
forall a.
InScopeEnv (RTAlias Symbol a)
-> Symbol -> TypeAliasResolution (RTAlias Symbol a)
resolveTypeAlias InScopeEnv (RTAlias Symbol ())
taliases Symbol
s of
              -- Priority is given to aliases defined in the current module,
              -- so name occurrences are resolved using them, disregarding
              -- any imported aliases with the same name.
              -- This allows the user to shadow imported aliases.
              FoundTypeAliases { tarLocallyDefined :: forall a. TypeAliasResolution a -> [(GenModule Unit, LHName, a)]
tarLocallyDefined = [(GenModule Unit
m, LHName
_, RTAlias Symbol ()
_)] } ->
                LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ Symbol -> GenModule Unit -> Maybe Name -> LHName
makeLogicLHName (Symbol -> Symbol
LH.dropModuleNames Symbol
s) GenModule Unit
m Maybe Name
forall a. Maybe a
Nothing
              FoundTypeAliases { tarImported :: forall a. TypeAliasResolution a -> [(GenModule Unit, LHName, a)]
tarImported = [(GenModule Unit
_, LHName
lh, RTAlias Symbol ()
_)]
                               , tarLocallyDefined :: forall a. TypeAliasResolution a -> [(GenModule Unit, LHName, a)]
tarLocallyDefined = []} | LHThisModuleNameFlag
lcl LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool
forall a. Eq a => a -> a -> Bool
== LHThisModuleNameFlag
LHAnyModuleNameF ->
                LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure LHName
lh
              -- If multiple matches are found, report the ambiguous name and return it.
              tar :: TypeAliasResolution (RTAlias Symbol ())
tar@(FoundTypeAliases { }) -> do Error -> State RenameOutput ()
addError (Error -> State RenameOutput ()) -> Error -> State RenameOutput ()
forall a b. (a -> b) -> a -> b
$ LocSymbol -> TypeAliasResolution (RTAlias Symbol ()) -> Error
forall x a. LocSymbol -> TypeAliasResolution (RTAlias x a) -> Error
errResolveTypeAlias (Symbol
s Symbol -> Located LHName -> LocSymbol
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Located LHName
lname) TypeAliasResolution (RTAlias Symbol ())
tar
                                               LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ Located LHName -> LHName
forall a. Located a -> a
val Located LHName
lname
              NoSuchTypeAlias [Symbol]
alts -> [Symbol]
-> LHNameSpace
-> Located LHName
-> Symbol
-> StateT RenameOutput Identity LHName
lookupGRELHName [Symbol]
alts (LHThisModuleNameFlag -> LHNameSpace
LHTcName LHThisModuleNameFlag
lcl) Located LHName
lname Symbol
s
        LHNUnresolved ns :: LHNameSpace
ns@(LHVarName LHThisModuleNameFlag
lcl) Symbol
s
          | Symbol -> Bool
isDataCon Symbol
s ->
              [Symbol]
-> LHNameSpace
-> Located LHName
-> Symbol
-> StateT RenameOutput Identity LHName
lookupGRELHName [] (LHThisModuleNameFlag -> LHNameSpace
LHDataConName LHThisModuleNameFlag
lcl) Located LHName
lname Symbol
s
          | Bool -> Bool
not (Symbol -> Bool
LH.isQualifiedSym Symbol
s)
          , Just Var
v <- LocalVars -> LocSymbol -> Maybe Var
Resolve.lookupLetBoundVar LocalVars
localVars (Located LHName -> Symbol -> LocSymbol
forall l b. Loc l => l -> b -> Located b
atLoc Located LHName
lname Symbol
s)
          ->
              LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ LHResolvedName -> Symbol -> LHName
LHNResolved (Name -> LHResolvedName
LHRGHC (Var -> Name
forall a. NamedThing a => a -> Name
GHC.getName Var
v)) Symbol
s
          | Bool
otherwise ->
              [Symbol]
-> LHNameSpace
-> Located LHName
-> Symbol
-> StateT RenameOutput Identity LHName
lookupGRELHName [] LHNameSpace
ns Located LHName
lname Symbol
s
        LHNUnresolved LHNameSpace
LHLogicNameBinder Symbol
s ->
          LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ Symbol -> GenModule Unit -> Maybe Name -> LHName
makeLogicLHName Symbol
s GenModule Unit
thisModule Maybe Name
forall a. Maybe a
Nothing
        n :: LHName
n@(LHNUnresolved LHNameSpace
LHLogicName Symbol
_) ->
          -- This one will be resolved by resolveLogicNames
          LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure LHName
n
        LHNUnresolved ns :: LHNameSpace
ns@(LHDataConName LHThisModuleNameFlag
_) Symbol
s -> [Symbol]
-> LHNameSpace
-> Located LHName
-> Symbol
-> StateT RenameOutput Identity LHName
lookupGRELHName [] LHNameSpace
ns Located LHName
lname Symbol
s
        n :: LHName
n@LHNResolved { } -> LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure LHName
n

    lookupGRELHName :: [Symbol]
-> LHNameSpace
-> Located LHName
-> Symbol
-> StateT RenameOutput Identity LHName
lookupGRELHName [Symbol]
alts LHNameSpace
ns Located LHName
lname Symbol
s =
      case LHNameSpace -> [GlobalRdrEltX GREInfo] -> [GlobalRdrEltX GREInfo]
forall {info}.
LHNameSpace -> [GlobalRdrEltX info] -> [GlobalRdrEltX info]
maybeDropImported LHNameSpace
ns ([GlobalRdrEltX GREInfo] -> [GlobalRdrEltX GREInfo])
-> [GlobalRdrEltX GREInfo] -> [GlobalRdrEltX GREInfo]
forall a b. (a -> b) -> a -> b
$ GlobalRdrEnv -> LookupGRE GREInfo -> [GlobalRdrEltX GREInfo]
forall info.
GlobalRdrEnvX info -> LookupGRE info -> [GlobalRdrEltX info]
GHC.lookupGRE GlobalRdrEnv
globalRdrEnv (LHNameSpace -> Symbol -> LookupGRE GREInfo
mkLookupGRE LHNameSpace
ns Symbol
s) of
        [GlobalRdrEltX GREInfo
e] -> do
          let n :: Name
n = GlobalRdrEltX GREInfo -> Name
forall info. GlobalRdrEltX info -> Name
GHC.greName GlobalRdrEltX GREInfo
e
          LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ LHResolvedName -> Symbol -> LHName
LHNResolved (Name -> LHResolvedName
LHRGHC Name
n) Symbol
s
        es :: [GlobalRdrEltX GREInfo]
es@(GlobalRdrEltX GREInfo
_:[GlobalRdrEltX GREInfo]
_) -> do
          Error -> State RenameOutput ()
addError
            (SrcSpan -> Doc -> Doc -> [Doc] -> Error
forall t. SrcSpan -> Doc -> Doc -> [Doc] -> TError t
ErrDupNames
               (Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
LH.fSrcSpan Located LHName
lname)
               (LHNameSpace -> Doc
nameSpaceKind LHNameSpace
ns)
               (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
s)
               ((GlobalRdrEltX GREInfo -> Doc) -> [GlobalRdrEltX GREInfo] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Doc
PJ.text ([Char] -> Doc)
-> (GlobalRdrEltX GREInfo -> [Char])
-> GlobalRdrEltX GREInfo
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalRdrEltX GREInfo -> [Char]
forall a. Outputable a => a -> [Char]
GHC.showPprUnsafe) [GlobalRdrEltX GREInfo]
es)
            )
          LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ Located LHName -> LHName
forall a. Located a -> a
val Located LHName
lname
        [] -> do
          Error -> State RenameOutput ()
addError
            ([Symbol] -> Doc -> [Char] -> LocSymbol -> Error
errResolve [Symbol]
alts (LHNameSpace -> Doc
nameSpaceKind LHNameSpace
ns) [Char]
"Cannot resolve name" (Symbol
s Symbol -> Located LHName -> LocSymbol
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Located LHName
lname))
          LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ Located LHName -> LHName
forall a. Located a -> a
val Located LHName
lname

    maybeDropImported :: LHNameSpace -> [GlobalRdrEltX info] -> [GlobalRdrEltX info]
maybeDropImported LHNameSpace
ns [GlobalRdrEltX info]
es
      | LHNameSpace -> Bool
localNameSpace LHNameSpace
ns = (GlobalRdrEltX info -> Bool)
-> [GlobalRdrEltX info] -> [GlobalRdrEltX info]
forall a. (a -> Bool) -> [a] -> [a]
filter GlobalRdrEltX info -> Bool
forall info. GlobalRdrEltX info -> Bool
GHC.isLocalGRE [GlobalRdrEltX info]
es
      | Bool
otherwise = [GlobalRdrEltX info]
es

    localNameSpace :: LHNameSpace -> Bool
localNameSpace = \case
      LHDataConName LHThisModuleNameFlag
lcl -> LHThisModuleNameFlag
lcl LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool
forall a. Eq a => a -> a -> Bool
== LHThisModuleNameFlag
LHThisModuleNameF
      LHVarName LHThisModuleNameFlag
lcl -> LHThisModuleNameFlag
lcl LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool
forall a. Eq a => a -> a -> Bool
== LHThisModuleNameFlag
LHThisModuleNameF
      LHTcName LHThisModuleNameFlag
lcl -> LHThisModuleNameFlag
lcl LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool
forall a. Eq a => a -> a -> Bool
== LHThisModuleNameFlag
LHThisModuleNameF
      LHNameSpace
LHLogicNameBinder -> Bool
False
      LHNameSpace
LHLogicName -> Bool
False

    nameSpaceKind :: LHNameSpace -> PJ.Doc
    nameSpaceKind :: LHNameSpace -> Doc
nameSpaceKind = \case
      LHTcName LHThisModuleNameFlag
LHAnyModuleNameF -> Doc
"type constructor"
      LHTcName LHThisModuleNameFlag
LHThisModuleNameF -> Doc
"locally-defined type constructor"
      LHDataConName LHThisModuleNameFlag
LHAnyModuleNameF -> Doc
"data constructor"
      LHDataConName LHThisModuleNameFlag
LHThisModuleNameF -> Doc
"locally-defined data constructor"
      LHVarName LHThisModuleNameFlag
LHAnyModuleNameF -> Doc
"variable"
      LHVarName LHThisModuleNameFlag
LHThisModuleNameF -> Doc
"variable from the current module"
      LHNameSpace
LHLogicNameBinder -> Doc
"logic name binder"
      LHNameSpace
LHLogicName -> Doc
"logic name"

    isDataCon :: Symbol -> Bool
isDataCon Symbol
s = case Text -> Maybe (Char, Text)
Text.uncons ((Char -> Bool) -> Text -> Text
Text.takeWhileEnd (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'.') (Symbol -> Text
symbolText Symbol
s)) of
      Just (Char
c, Text
_) -> Char -> Bool
Char.isUpper Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
':'
      Maybe (Char, Text)
Nothing -> Bool
False

tupleArity :: Symbol -> Int
tupleArity :: Symbol -> Int
tupleArity Symbol
s =
      let a :: Int
a = [Char] -> Int
forall a. Read a => [Char] -> a
read ([Char] -> Int) -> [Char] -> Int
forall a b. (a -> b) -> a -> b
$ Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
drop Int
5 ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ Symbol -> [Char]
symbolString Symbol
s
       in if Int
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
64 then
            [Char] -> Int
forall a. HasCallStack => [Char] -> a
error ([Char] -> Int) -> [Char] -> Int
forall a b. (a -> b) -> a -> b
$ [Char]
"tupleArity: Too large (more than 64): " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
a
          else
            Int
a

errResolve :: [Symbol] -> PJ.Doc -> String -> LocSymbol -> Error
errResolve :: [Symbol] -> Doc -> [Char] -> LocSymbol -> Error
errResolve [Symbol]
alts Doc
k [Char]
msg LocSymbol
ls =
  SrcSpan -> Doc -> Doc -> Doc -> Error
forall t. SrcSpan -> Doc -> Doc -> Doc -> TError t
ErrResolve
    (LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
LH.fSrcSpan LocSymbol
ls)
    Doc
k
    (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (Symbol -> Doc) -> Symbol -> Doc
forall a b. (a -> b) -> a -> b
$ LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
ls)
    (if [Symbol] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol]
alts then
        [Char] -> Doc
PJ.text [Char]
msg
      else
        [Char] -> Doc
PJ.text [Char]
msg Doc -> Doc -> Doc
PJ.$$
        [Doc] -> Doc
PJ.sep ([Char] -> Doc
PJ.text [Char]
"Maybe you meant one of:" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Symbol -> Doc) -> [Symbol] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint [Symbol]
alts)
    )


-- | Produces an LHName from a symbol by looking it in the rdr environment.
resolveSymbolToTcName :: GHC.GlobalRdrEnv -> LocSymbol -> Either Error (Located LHName)
resolveSymbolToTcName :: GlobalRdrEnv -> LocSymbol -> Either Error (Located LHName)
resolveSymbolToTcName GlobalRdrEnv
globalRdrEnv LocSymbol
lx
    | Symbol -> Bool
forall c. TyConable c => c -> Bool
isTuple Symbol
s =
      Located LHName -> Either Error (Located LHName)
forall a. a -> Either Error a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Located LHName -> Either Error (Located LHName))
-> Located LHName -> Either Error (Located LHName)
forall a b. (a -> b) -> a -> b
$ LHResolvedName -> Symbol -> LHName
LHNResolved (Name -> LHResolvedName
LHRGHC (Name -> LHResolvedName) -> Name -> LHResolvedName
forall a b. (a -> b) -> a -> b
$ TupleSort -> Int -> Name
GHC.tupleTyConName TupleSort
GHC.BoxedTuple (Symbol -> Int
tupleArity Symbol
s)) Symbol
s LHName -> LocSymbol -> Located LHName
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ LocSymbol
lx
    | Symbol -> Bool
forall c. TyConable c => c -> Bool
isList Symbol
s =
      Located LHName -> Either Error (Located LHName)
forall a. a -> Either Error a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Located LHName -> Either Error (Located LHName))
-> Located LHName -> Either Error (Located LHName)
forall a b. (a -> b) -> a -> b
$ LHResolvedName -> Symbol -> LHName
LHNResolved (Name -> LHResolvedName
LHRGHC Name
GHC.listTyConName) Symbol
s LHName -> LocSymbol -> Located LHName
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ LocSymbol
lx
    | Symbol
s Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"*" =
      Located LHName -> Either Error (Located LHName)
forall a. a -> Either Error a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Located LHName -> Either Error (Located LHName))
-> Located LHName -> Either Error (Located LHName)
forall a b. (a -> b) -> a -> b
$ LHResolvedName -> Symbol -> LHName
LHNResolved (Name -> LHResolvedName
LHRGHC Name
GHC.liftedTypeKindTyConName) Symbol
s LHName -> LocSymbol -> Located LHName
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ LocSymbol
lx
    | Bool
otherwise =
      case GlobalRdrEnv -> LookupGRE GREInfo -> [GlobalRdrEltX GREInfo]
forall info.
GlobalRdrEnvX info -> LookupGRE info -> [GlobalRdrEltX info]
GHC.lookupGRE GlobalRdrEnv
globalRdrEnv (LHNameSpace -> Symbol -> LookupGRE GREInfo
mkLookupGRE (LHThisModuleNameFlag -> LHNameSpace
LHTcName LHThisModuleNameFlag
LHAnyModuleNameF) Symbol
s) of
        [GlobalRdrEltX GREInfo
e] -> Located LHName -> Either Error (Located LHName)
forall a b. b -> Either a b
Right (Located LHName -> Either Error (Located LHName))
-> Located LHName -> Either Error (Located LHName)
forall a b. (a -> b) -> a -> b
$ LHResolvedName -> Symbol -> LHName
LHNResolved (Name -> LHResolvedName
LHRGHC (Name -> LHResolvedName) -> Name -> LHResolvedName
forall a b. (a -> b) -> a -> b
$ GlobalRdrEltX GREInfo -> Name
forall info. GlobalRdrEltX info -> Name
GHC.greName GlobalRdrEltX GREInfo
e) Symbol
s LHName -> LocSymbol -> Located LHName
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ LocSymbol
lx
        [] -> Error -> Either Error (Located LHName)
forall a b. a -> Either a b
Left (Error -> Either Error (Located LHName))
-> Error -> Either Error (Located LHName)
forall a b. (a -> b) -> a -> b
$ [Symbol] -> Doc -> [Char] -> LocSymbol -> Error
errResolve [] Doc
"type constructor" [Char]
"Cannot resolve name" LocSymbol
lx
        [GlobalRdrEltX GREInfo]
es -> Error -> Either Error (Located LHName)
forall a b. a -> Either a b
Left (Error -> Either Error (Located LHName))
-> Error -> Either Error (Located LHName)
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Doc -> [Doc] -> Error
forall t. SrcSpan -> Doc -> Doc -> [Doc] -> TError t
ErrDupNames
                (LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
LH.fSrcSpan LocSymbol
lx)
                Doc
"type constructor"
                (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
s)
                ((GlobalRdrEltX GREInfo -> Doc) -> [GlobalRdrEltX GREInfo] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Doc
PJ.text ([Char] -> Doc)
-> (GlobalRdrEltX GREInfo -> [Char])
-> GlobalRdrEltX GREInfo
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalRdrEltX GREInfo -> [Char]
forall a. Outputable a => a -> [Char]
GHC.showPprUnsafe) [GlobalRdrEltX GREInfo]
es)
  where
    s :: Symbol
s = LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
lx

-- | Resolving logic names can produce errors and new names to add to the
-- environment. New names might be produced when encountering data constructors
-- or functions from the logic map.
data RenameOutput = RenameOutput
    { RenameOutput -> [Error]
roErrors :: [Error]
      -- | Names of used data constructors, and names of used reflected
      -- functions and used logic map names
    , RenameOutput -> [LHName]
roUsedNames :: [LHName]
      -- | Names of used data constructors
    , RenameOutput -> HashSet LHName
roUsedDataCons :: HS.HashSet LHName
    }

addError :: Error -> State RenameOutput ()
addError :: Error -> State RenameOutput ()
addError Error
e = (RenameOutput -> RenameOutput) -> State RenameOutput ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\RenameOutput
ro -> RenameOutput
ro { roErrors = e : roErrors ro })

addName :: LHName -> State RenameOutput ()
addName :: LHName -> State RenameOutput ()
addName LHName
n = (RenameOutput -> RenameOutput) -> State RenameOutput ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\RenameOutput
ro -> RenameOutput
ro { roUsedNames = n : roUsedNames ro })

addDataConsName :: LHName -> State RenameOutput ()
addDataConsName :: LHName -> State RenameOutput ()
addDataConsName LHName
n = (RenameOutput -> RenameOutput) -> State RenameOutput ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\RenameOutput
ro -> RenameOutput
ro { roUsedDataCons = HS.insert n (roUsedDataCons ro) })

mkLookupGRE :: LHNameSpace -> Symbol -> GHC.LookupGRE GHC.GREInfo
mkLookupGRE :: LHNameSpace -> Symbol -> LookupGRE GREInfo
mkLookupGRE LHNameSpace
ns Symbol
s =
    let m :: Symbol
m = Symbol -> Symbol
LH.takeModuleNames Symbol
s
        n :: Symbol
n = Symbol -> Symbol
LH.dropModuleNames Symbol
s
        nString :: [Char]
nString = Symbol -> [Char]
symbolString Symbol
n
        oname :: OccName
oname = NameSpace -> [Char] -> OccName
GHC.mkOccName (LHNameSpace -> NameSpace
mkGHCNameSpace LHNameSpace
ns) [Char]
nString
        rdrn :: RdrName
rdrn =
          if Symbol
m Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"" then
            OccName -> RdrName
GHC.mkRdrUnqual OccName
oname
          else
            ModuleName -> OccName -> RdrName
GHC.mkRdrQual ([Char] -> ModuleName
GHC.mkModuleName ([Char] -> ModuleName) -> [Char] -> ModuleName
forall a b. (a -> b) -> a -> b
$ Symbol -> [Char]
symbolString Symbol
m) OccName
oname
     in RdrName -> WhichGREs GREInfo -> LookupGRE GREInfo
forall info. RdrName -> WhichGREs info -> LookupGRE info
GHC.LookupRdrName RdrName
rdrn (LHNameSpace -> WhichGREs GREInfo
mkWhichGREs LHNameSpace
ns)
  where
    mkWhichGREs :: LHNameSpace -> GHC.WhichGREs GHC.GREInfo
    mkWhichGREs :: LHNameSpace -> WhichGREs GREInfo
mkWhichGREs = \case
      LHTcName LHThisModuleNameFlag
_ -> WhichGREs GREInfo
forall info. WhichGREs info
GHC.SameNameSpace
      LHDataConName LHThisModuleNameFlag
_ -> WhichGREs GREInfo
forall info. WhichGREs info
GHC.SameNameSpace
      LHVarName LHThisModuleNameFlag
_ -> GHC.RelevantGREs
        { includeFieldSelectors :: FieldsOrSelectors
GHC.includeFieldSelectors = FieldsOrSelectors
GHC.WantNormal
        , lookupVariablesForFields :: Bool
GHC.lookupVariablesForFields = Bool
True
        , lookupTyConsAsWell :: Bool
GHC.lookupTyConsAsWell = Bool
False
        }
      LHNameSpace
LHLogicNameBinder -> Maybe SrcSpan -> [Char] -> WhichGREs GREInfo
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"mkWhichGREs: unexpected namespace LHLogicNameBinder"
      LHNameSpace
LHLogicName -> Maybe SrcSpan -> [Char] -> WhichGREs GREInfo
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"mkWhichGREs: unexpected namespace LHLogicName"

    mkGHCNameSpace :: LHNameSpace -> NameSpace
mkGHCNameSpace = \case
      LHTcName LHThisModuleNameFlag
_ -> NameSpace
GHC.tcName
      LHDataConName LHThisModuleNameFlag
_ -> NameSpace
GHC.dataName
      LHVarName LHThisModuleNameFlag
_ -> NameSpace
GHC.Types.Name.Occurrence.varName
      LHNameSpace
LHLogicNameBinder -> Maybe SrcSpan -> [Char] -> NameSpace
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"mkGHCNameSpace: unexpected namespace LHLogicNameBinder"
      LHNameSpace
LHLogicName -> Maybe SrcSpan -> [Char] -> NameSpace
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"mkGHCNameSpace: unexpected namespace LHLogicName"

-- | Changes unresolved names to local resolved names in the body of type
-- aliases.
resolveBoundVarsInTypeAliases :: BareSpecParsed -> BareSpecParsed
resolveBoundVarsInTypeAliases :: Spec LocSymbol BareTypeParsed -> Spec LocSymbol BareTypeParsed
resolveBoundVarsInTypeAliases = ([Symbol] -> LHName -> LHName)
-> Spec LocSymbol BareTypeParsed -> Spec LocSymbol BareTypeParsed
forall {lname} {ty}.
Data lname =>
([Symbol] -> LHName -> LHName) -> Spec lname ty -> Spec lname ty
updateAliases [Symbol] -> LHName -> LHName
forall {t :: * -> *}. Foldable t => t Symbol -> LHName -> LHName
resolveBoundVars
  where
    resolveBoundVars :: t Symbol -> LHName -> LHName
resolveBoundVars t Symbol
boundVars = \case
      LHNUnresolved (LHTcName LHThisModuleNameFlag
lcl) Symbol
s ->
        if Symbol -> t Symbol -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Symbol
s t Symbol
boundVars then
          LHResolvedName -> Symbol -> LHName
LHNResolved (Symbol -> LHResolvedName
LHRLocal Symbol
s) Symbol
s
        else
          LHNameSpace -> Symbol -> LHName
LHNUnresolved (LHThisModuleNameFlag -> LHNameSpace
LHTcName LHThisModuleNameFlag
lcl) Symbol
s
      LHName
n ->
        [Char] -> LHName
forall a. HasCallStack => [Char] -> a
error ([Char] -> LHName) -> [Char] -> LHName
forall a b. (a -> b) -> a -> b
$ [Char]
"resolveLHNames: Unexpected resolved name: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ LHName -> [Char]
forall a. Show a => a -> [Char]
show LHName
n

    -- Applies a function to the body of type aliases, passes to every call the
    -- arguments of the alias.
    updateAliases :: ([Symbol] -> LHName -> LHName) -> Spec lname ty -> Spec lname ty
updateAliases [Symbol] -> LHName -> LHName
f Spec lname ty
spec =
       Spec lname ty
spec
            { aliases = [ a { rtBody = mapLHNames (f args) (rtBody a) }
                        | a <- aliases spec
                        , let args = RTAlias Symbol (BareTypeV lname) -> [Symbol]
forall x a. RTAlias x a -> [x]
rtTArgs RTAlias Symbol (BareTypeV lname)
a [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RTAlias Symbol (BareTypeV lname) -> [Symbol]
forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias Symbol (BareTypeV lname)
a
                        ]
            }

-- | The expression arguments of type aliases are initially parsed as
-- types. This function converts them to expressions.
--
-- For instance, in @Prop (Ev (plus n n))@ where `Prop` is the alias
--
-- > {-@ type Prop E = {v:_ | prop v = E} @-}
--
-- the parser builds a type for @Ev (plus n n)@.
-- | @fixExpressionArgsOfTypeAliases taliases spec@ converts types to
-- values when they appear in value positions of type aliases according
-- to @taliases@.
--
-- The expression arguments of type aliases are initially parsed as
-- types. This function converts them to expressions.
--
-- For instance, in @Prop (Ev (plus n n))@ where `Prop` is the alias
--
-- > {-@ type Prop E = {v:_ | prop v = E} @-}
--
-- the parser builds a type for @Ev (plus n n)@, making a type
-- constructor of @Ev@ and type variables of @plus@ and @n@. But
-- @Ev@ is really a data constructor, @plus@ is a function, and @n@
-- is a value.
fixExpressionArgsOfTypeAliases
  :: InScopeEnv (RTAlias Symbol ())
  -> BareSpecParsed
  -> StateT RenameOutput Identity BareSpecParsed
fixExpressionArgsOfTypeAliases :: InScopeEnv (RTAlias Symbol ())
-> Spec LocSymbol BareTypeParsed
-> StateT RenameOutput Identity (Spec LocSymbol BareTypeParsed)
fixExpressionArgsOfTypeAliases InScopeEnv (RTAlias Symbol ())
taliases = (BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed)
-> Spec LocSymbol BareTypeParsed
-> StateT RenameOutput Identity (Spec LocSymbol BareTypeParsed)
forall (m :: * -> *) a.
(Data a, Monad m) =>
(BareTypeParsed -> m BareTypeParsed) -> a -> m a
mapMBareTypes BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
go
  where
    go :: BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
    go :: BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
go (RApp c :: BTyCon
c@(BTyCon { btc_tc :: BTyCon -> Located LHName
btc_tc = lname :: Located LHName
lname@(Loc SourcePos
_ SourcePos
_ (LHNUnresolved (LHTcName LHThisModuleNameFlag
_) Symbol
s)) }) [BareTypeParsed]
ts [RTPropBV
   Symbol
   LocSymbol
   BTyCon
   BTyVar
   (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
rs UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
r)
      | tar :: TypeAliasResolution (RTAlias Symbol ())
tar@(FoundTypeAliases [(GenModule Unit, LHName, RTAlias Symbol ())]
imported [(GenModule Unit, LHName, RTAlias Symbol ())]
local) <- InScopeEnv (RTAlias Symbol ())
-> Symbol -> TypeAliasResolution (RTAlias Symbol ())
forall a.
InScopeEnv (RTAlias Symbol a)
-> Symbol -> TypeAliasResolution (RTAlias Symbol a)
resolveTypeAlias InScopeEnv (RTAlias Symbol ())
taliases Symbol
s =
          case ([(GenModule Unit, LHName, RTAlias Symbol ())]
imported, [(GenModule Unit, LHName, RTAlias Symbol ())]
local) of
               -- Local alias definitions get priority over imported ones.
               -- This allows the user to shadow imported aliases.
               ([(GenModule Unit, LHName, RTAlias Symbol ())]
_ ,[(GenModule Unit
_, LHName
_, RTAlias Symbol ()
rta)]) ->
                 BTyCon
-> [BareTypeParsed]
-> [RTPropBV
      Symbol
      LocSymbol
      BTyCon
      BTyVar
      (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
-> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
-> BareTypeParsed
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 (BTyCon
 -> [BareTypeParsed]
 -> [RTPropBV
       Symbol
       LocSymbol
       BTyCon
       BTyVar
       (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
 -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
 -> BareTypeParsed)
-> StateT RenameOutput Identity BTyCon
-> StateT
     RenameOutput
     Identity
     ([BareTypeParsed]
      -> [RTPropBV
            Symbol
            LocSymbol
            BTyCon
            BTyVar
            (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
      -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BTyCon -> StateT RenameOutput Identity BTyCon
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BTyCon
c StateT
  RenameOutput
  Identity
  ([BareTypeParsed]
   -> [RTPropBV
         Symbol
         LocSymbol
         BTyCon
         BTyVar
         (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
   -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT RenameOutput Identity [BareTypeParsed]
-> StateT
     RenameOutput
     Identity
     ([RTPropBV
         Symbol
         LocSymbol
         BTyCon
         BTyVar
         (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
      -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Located LHName
-> RTAlias Symbol ()
-> StateT RenameOutput Identity [BareTypeParsed]
-> StateT RenameOutput Identity [BareTypeParsed]
forall {m :: * -> *} {b} {a} {a}.
Monad m =>
Located b
-> RTAlias a a -> m [BareTypeParsed] -> m [BareTypeParsed]
fixExprArgs (BTyCon -> Located LHName
btc_tc BTyCon
c) RTAlias Symbol ()
rta ((BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed)
-> [BareTypeParsed]
-> StateT RenameOutput Identity [BareTypeParsed]
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 BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
go [BareTypeParsed]
ts) StateT
  RenameOutput
  Identity
  ([RTPropBV
      Symbol
      LocSymbol
      BTyCon
      BTyVar
      (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
   -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT
     RenameOutput
     Identity
     [RTPropBV
        Symbol
        LocSymbol
        BTyCon
        BTyVar
        (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (RTPropBV
   Symbol
   LocSymbol
   BTyCon
   BTyVar
   (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
 -> StateT
      RenameOutput
      Identity
      (RTPropBV
         Symbol
         LocSymbol
         BTyCon
         BTyVar
         (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))))
-> [RTPropBV
      Symbol
      LocSymbol
      BTyCon
      BTyVar
      (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
-> StateT
     RenameOutput
     Identity
     [RTPropBV
        Symbol
        LocSymbol
        BTyCon
        BTyVar
        (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
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 RTPropBV
  Symbol
  LocSymbol
  BTyCon
  BTyVar
  (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
-> StateT
     RenameOutput
     Identity
     (RTPropBV
        Symbol
        LocSymbol
        BTyCon
        BTyVar
        (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)))
goRef [RTPropBV
   Symbol
   LocSymbol
   BTyCon
   BTyVar
   (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
rs StateT
  RenameOutput
  Identity
  (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
-> StateT RenameOutput Identity BareTypeParsed
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
r
               ([(GenModule Unit
_, LHName
_, RTAlias Symbol ()
rta)] , []) ->
                 BTyCon
-> [BareTypeParsed]
-> [RTPropBV
      Symbol
      LocSymbol
      BTyCon
      BTyVar
      (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
-> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
-> BareTypeParsed
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 (BTyCon
 -> [BareTypeParsed]
 -> [RTPropBV
       Symbol
       LocSymbol
       BTyCon
       BTyVar
       (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
 -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
 -> BareTypeParsed)
-> StateT RenameOutput Identity BTyCon
-> StateT
     RenameOutput
     Identity
     ([BareTypeParsed]
      -> [RTPropBV
            Symbol
            LocSymbol
            BTyCon
            BTyVar
            (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
      -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BTyCon -> StateT RenameOutput Identity BTyCon
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BTyCon
c StateT
  RenameOutput
  Identity
  ([BareTypeParsed]
   -> [RTPropBV
         Symbol
         LocSymbol
         BTyCon
         BTyVar
         (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
   -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT RenameOutput Identity [BareTypeParsed]
-> StateT
     RenameOutput
     Identity
     ([RTPropBV
         Symbol
         LocSymbol
         BTyCon
         BTyVar
         (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
      -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Located LHName
-> RTAlias Symbol ()
-> StateT RenameOutput Identity [BareTypeParsed]
-> StateT RenameOutput Identity [BareTypeParsed]
forall {m :: * -> *} {b} {a} {a}.
Monad m =>
Located b
-> RTAlias a a -> m [BareTypeParsed] -> m [BareTypeParsed]
fixExprArgs (BTyCon -> Located LHName
btc_tc BTyCon
c) RTAlias Symbol ()
rta ((BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed)
-> [BareTypeParsed]
-> StateT RenameOutput Identity [BareTypeParsed]
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 BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
go [BareTypeParsed]
ts) StateT
  RenameOutput
  Identity
  ([RTPropBV
      Symbol
      LocSymbol
      BTyCon
      BTyVar
      (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
   -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT
     RenameOutput
     Identity
     [RTPropBV
        Symbol
        LocSymbol
        BTyCon
        BTyVar
        (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (RTPropBV
   Symbol
   LocSymbol
   BTyCon
   BTyVar
   (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
 -> StateT
      RenameOutput
      Identity
      (RTPropBV
         Symbol
         LocSymbol
         BTyCon
         BTyVar
         (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))))
-> [RTPropBV
      Symbol
      LocSymbol
      BTyCon
      BTyVar
      (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
-> StateT
     RenameOutput
     Identity
     [RTPropBV
        Symbol
        LocSymbol
        BTyCon
        BTyVar
        (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
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 RTPropBV
  Symbol
  LocSymbol
  BTyCon
  BTyVar
  (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
-> StateT
     RenameOutput
     Identity
     (RTPropBV
        Symbol
        LocSymbol
        BTyCon
        BTyVar
        (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)))
goRef [RTPropBV
   Symbol
   LocSymbol
   BTyCon
   BTyVar
   (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
rs StateT
  RenameOutput
  Identity
  (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
-> StateT RenameOutput Identity BareTypeParsed
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
r
               -- Report ambiguos name and continue traversing.
               ([(GenModule Unit, LHName, RTAlias Symbol ())],
 [(GenModule Unit, LHName, RTAlias Symbol ())])
_ -> do
                 Error -> State RenameOutput ()
addError (Error -> State RenameOutput ()) -> Error -> State RenameOutput ()
forall a b. (a -> b) -> a -> b
$ LocSymbol -> TypeAliasResolution (RTAlias Symbol ()) -> Error
forall x a. LocSymbol -> TypeAliasResolution (RTAlias x a) -> Error
errResolveTypeAlias (Symbol
s Symbol -> Located LHName -> LocSymbol
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Located LHName
lname) TypeAliasResolution (RTAlias Symbol ())
tar
                 BTyCon
-> [BareTypeParsed]
-> [RTPropBV
      Symbol
      LocSymbol
      BTyCon
      BTyVar
      (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
-> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
-> BareTypeParsed
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 (BTyCon
 -> [BareTypeParsed]
 -> [RTPropBV
       Symbol
       LocSymbol
       BTyCon
       BTyVar
       (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
 -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
 -> BareTypeParsed)
-> StateT RenameOutput Identity BTyCon
-> StateT
     RenameOutput
     Identity
     ([BareTypeParsed]
      -> [RTPropBV
            Symbol
            LocSymbol
            BTyCon
            BTyVar
            (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
      -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BTyCon -> StateT RenameOutput Identity BTyCon
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BTyCon
c StateT
  RenameOutput
  Identity
  ([BareTypeParsed]
   -> [RTPropBV
         Symbol
         LocSymbol
         BTyCon
         BTyVar
         (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
   -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT RenameOutput Identity [BareTypeParsed]
-> StateT
     RenameOutput
     Identity
     ([RTPropBV
         Symbol
         LocSymbol
         BTyCon
         BTyVar
         (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
      -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed)
-> [BareTypeParsed]
-> StateT RenameOutput Identity [BareTypeParsed]
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 BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
go [BareTypeParsed]
ts StateT
  RenameOutput
  Identity
  ([RTPropBV
      Symbol
      LocSymbol
      BTyCon
      BTyVar
      (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
   -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT
     RenameOutput
     Identity
     [RTPropBV
        Symbol
        LocSymbol
        BTyCon
        BTyVar
        (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (RTPropBV
   Symbol
   LocSymbol
   BTyCon
   BTyVar
   (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
 -> StateT
      RenameOutput
      Identity
      (RTPropBV
         Symbol
         LocSymbol
         BTyCon
         BTyVar
         (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))))
-> [RTPropBV
      Symbol
      LocSymbol
      BTyCon
      BTyVar
      (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
-> StateT
     RenameOutput
     Identity
     [RTPropBV
        Symbol
        LocSymbol
        BTyCon
        BTyVar
        (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
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 RTPropBV
  Symbol
  LocSymbol
  BTyCon
  BTyVar
  (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
-> StateT
     RenameOutput
     Identity
     (RTPropBV
        Symbol
        LocSymbol
        BTyCon
        BTyVar
        (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)))
goRef [RTPropBV
   Symbol
   LocSymbol
   BTyCon
   BTyVar
   (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
rs StateT
  RenameOutput
  Identity
  (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
-> StateT RenameOutput Identity BareTypeParsed
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
r
    go (RApp BTyCon
c [BareTypeParsed]
ts [RTPropBV
   Symbol
   LocSymbol
   BTyCon
   BTyVar
   (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
rs UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
r)    = BTyCon
-> [BareTypeParsed]
-> [RTPropBV
      Symbol
      LocSymbol
      BTyCon
      BTyVar
      (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
-> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
-> BareTypeParsed
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 (BTyCon
 -> [BareTypeParsed]
 -> [RTPropBV
       Symbol
       LocSymbol
       BTyCon
       BTyVar
       (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
 -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
 -> BareTypeParsed)
-> StateT RenameOutput Identity BTyCon
-> StateT
     RenameOutput
     Identity
     ([BareTypeParsed]
      -> [RTPropBV
            Symbol
            LocSymbol
            BTyCon
            BTyVar
            (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
      -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BTyCon -> StateT RenameOutput Identity BTyCon
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BTyCon
c StateT
  RenameOutput
  Identity
  ([BareTypeParsed]
   -> [RTPropBV
         Symbol
         LocSymbol
         BTyCon
         BTyVar
         (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
   -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT RenameOutput Identity [BareTypeParsed]
-> StateT
     RenameOutput
     Identity
     ([RTPropBV
         Symbol
         LocSymbol
         BTyCon
         BTyVar
         (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
      -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed)
-> [BareTypeParsed]
-> StateT RenameOutput Identity [BareTypeParsed]
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 BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
go [BareTypeParsed]
ts StateT
  RenameOutput
  Identity
  ([RTPropBV
      Symbol
      LocSymbol
      BTyCon
      BTyVar
      (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
   -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT
     RenameOutput
     Identity
     [RTPropBV
        Symbol
        LocSymbol
        BTyCon
        BTyVar
        (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (RTPropBV
   Symbol
   LocSymbol
   BTyCon
   BTyVar
   (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
 -> StateT
      RenameOutput
      Identity
      (RTPropBV
         Symbol
         LocSymbol
         BTyCon
         BTyVar
         (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))))
-> [RTPropBV
      Symbol
      LocSymbol
      BTyCon
      BTyVar
      (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
-> StateT
     RenameOutput
     Identity
     [RTPropBV
        Symbol
        LocSymbol
        BTyCon
        BTyVar
        (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
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 RTPropBV
  Symbol
  LocSymbol
  BTyCon
  BTyVar
  (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
-> StateT
     RenameOutput
     Identity
     (RTPropBV
        Symbol
        LocSymbol
        BTyCon
        BTyVar
        (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)))
goRef [RTPropBV
   Symbol
   LocSymbol
   BTyCon
   BTyVar
   (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))]
rs StateT
  RenameOutput
  Identity
  (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
-> StateT RenameOutput Identity BareTypeParsed
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
r
    go (RAppTy BareTypeParsed
t1 BareTypeParsed
t2 UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
r)    = BareTypeParsed
-> BareTypeParsed
-> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
-> BareTypeParsed
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 (BareTypeParsed
 -> BareTypeParsed
 -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
 -> BareTypeParsed)
-> StateT RenameOutput Identity BareTypeParsed
-> StateT
     RenameOutput
     Identity
     (BareTypeParsed
      -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
go BareTypeParsed
t1 StateT
  RenameOutput
  Identity
  (BareTypeParsed
   -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT RenameOutput Identity BareTypeParsed
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
go BareTypeParsed
t2 StateT
  RenameOutput
  Identity
  (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
-> StateT RenameOutput Identity BareTypeParsed
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
r
    go (RFun  Symbol
x RFInfo
i BareTypeParsed
t1 BareTypeParsed
t2 UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
r) = Symbol
-> RFInfo
-> BareTypeParsed
-> BareTypeParsed
-> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
-> BareTypeParsed
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
 -> RFInfo
 -> BareTypeParsed
 -> BareTypeParsed
 -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
 -> BareTypeParsed)
-> StateT RenameOutput Identity Symbol
-> StateT
     RenameOutput
     Identity
     (RFInfo
      -> BareTypeParsed
      -> BareTypeParsed
      -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> StateT RenameOutput Identity Symbol
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Symbol
x StateT
  RenameOutput
  Identity
  (RFInfo
   -> BareTypeParsed
   -> BareTypeParsed
   -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT RenameOutput Identity RFInfo
-> StateT
     RenameOutput
     Identity
     (BareTypeParsed
      -> BareTypeParsed
      -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RFInfo -> StateT RenameOutput Identity RFInfo
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure RFInfo
i StateT
  RenameOutput
  Identity
  (BareTypeParsed
   -> BareTypeParsed
   -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT RenameOutput Identity BareTypeParsed
-> StateT
     RenameOutput
     Identity
     (BareTypeParsed
      -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
go BareTypeParsed
t1 StateT
  RenameOutput
  Identity
  (BareTypeParsed
   -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT RenameOutput Identity BareTypeParsed
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
go BareTypeParsed
t2 StateT
  RenameOutput
  Identity
  (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
-> StateT RenameOutput Identity BareTypeParsed
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
r
    go (RAllT RTVUBV Symbol LocSymbol BTyCon BTyVar
a BareTypeParsed
t UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
r)       = RTVUBV Symbol LocSymbol BTyCon BTyVar
-> BareTypeParsed
-> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
-> BareTypeParsed
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 LocSymbol BTyCon BTyVar
 -> BareTypeParsed
 -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
 -> BareTypeParsed)
-> StateT
     RenameOutput Identity (RTVUBV Symbol LocSymbol BTyCon BTyVar)
-> StateT
     RenameOutput
     Identity
     (BareTypeParsed
      -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTVUBV Symbol LocSymbol BTyCon BTyVar
-> StateT
     RenameOutput Identity (RTVUBV Symbol LocSymbol BTyCon BTyVar)
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure RTVUBV Symbol LocSymbol BTyCon BTyVar
a StateT
  RenameOutput
  Identity
  (BareTypeParsed
   -> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT RenameOutput Identity BareTypeParsed
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
      -> BareTypeParsed)
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
go BareTypeParsed
t StateT
  RenameOutput
  Identity
  (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
   -> BareTypeParsed)
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
-> StateT RenameOutput Identity BareTypeParsed
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
-> StateT
     RenameOutput
     Identity
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
r
    go (RAllP PVUBV Symbol LocSymbol BTyCon BTyVar
a BareTypeParsed
t)         = PVUBV Symbol LocSymbol BTyCon BTyVar
-> BareTypeParsed -> BareTypeParsed
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP PVUBV Symbol LocSymbol BTyCon BTyVar
a (BareTypeParsed -> BareTypeParsed)
-> StateT RenameOutput Identity BareTypeParsed
-> StateT RenameOutput Identity BareTypeParsed
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
go BareTypeParsed
t
    go (RAllE Symbol
x BareTypeParsed
t1 BareTypeParsed
t2)     = Symbol -> BareTypeParsed -> BareTypeParsed -> BareTypeParsed
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 (BareTypeParsed -> BareTypeParsed -> BareTypeParsed)
-> StateT RenameOutput Identity BareTypeParsed
-> StateT RenameOutput Identity (BareTypeParsed -> BareTypeParsed)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
go BareTypeParsed
t1 StateT RenameOutput Identity (BareTypeParsed -> BareTypeParsed)
-> StateT RenameOutput Identity BareTypeParsed
-> StateT RenameOutput Identity BareTypeParsed
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
go BareTypeParsed
t2
    go (REx Symbol
x BareTypeParsed
t1 BareTypeParsed
t2)       = Symbol -> BareTypeParsed -> BareTypeParsed -> BareTypeParsed
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 (BareTypeParsed -> BareTypeParsed -> BareTypeParsed)
-> StateT RenameOutput Identity BareTypeParsed
-> StateT RenameOutput Identity (BareTypeParsed -> BareTypeParsed)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
go BareTypeParsed
t1 StateT RenameOutput Identity (BareTypeParsed -> BareTypeParsed)
-> StateT RenameOutput Identity BareTypeParsed
-> StateT RenameOutput Identity BareTypeParsed
forall a b.
StateT RenameOutput Identity (a -> b)
-> StateT RenameOutput Identity a -> StateT RenameOutput Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
go BareTypeParsed
t2
    go (RRTy [(Symbol, BareTypeParsed)]
e UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
r Oblig
o BareTypeParsed
t)      = [(Symbol, BareTypeParsed)]
-> UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
-> Oblig
-> BareTypeParsed
-> BareTypeParsed
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, BareTypeParsed)]
e UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
r Oblig
o  (BareTypeParsed -> BareTypeParsed)
-> StateT RenameOutput Identity BareTypeParsed
-> StateT RenameOutput Identity BareTypeParsed
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
go BareTypeParsed
t
    go t :: BareTypeParsed
t@RHole{}           = BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BareTypeParsed
t
    go t :: BareTypeParsed
t@RVar{}            = BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BareTypeParsed
t
    go t :: BareTypeParsed
t@RExprArg{}        = BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BareTypeParsed
t
    goRef :: RTPropBV
  Symbol
  LocSymbol
  BTyCon
  BTyVar
  (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
-> StateT
     RenameOutput
     Identity
     (RTPropBV
        Symbol
        LocSymbol
        BTyCon
        BTyVar
        (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)))
goRef (RProp [(Symbol, RTypeBV Symbol LocSymbol BTyCon BTyVar (NoReftB Symbol))]
ss BareTypeParsed
t)     = [(Symbol, RTypeBV Symbol LocSymbol BTyCon BTyVar (NoReftB Symbol))]
-> BareTypeParsed
-> RTPropBV
     Symbol
     LocSymbol
     BTyCon
     BTyVar
     (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol))
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, RTypeBV Symbol LocSymbol BTyCon BTyVar (NoReftB Symbol))]
ss (BareTypeParsed
 -> RTPropBV
      Symbol
      LocSymbol
      BTyCon
      BTyVar
      (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)))
-> StateT RenameOutput Identity BareTypeParsed
-> StateT
     RenameOutput
     Identity
     (RTPropBV
        Symbol
        LocSymbol
        BTyCon
        BTyVar
        (UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareTypeParsed -> StateT RenameOutput Identity BareTypeParsed
go BareTypeParsed
t

    fixExprArgs :: Located b
-> RTAlias a a -> m [BareTypeParsed] -> m [BareTypeParsed]
fixExprArgs Located b
lname RTAlias a a
rta m [BareTypeParsed]
mts = do
      ts <- m [BareTypeParsed]
mts
      let n = [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (RTAlias a a -> [a]
forall x a. RTAlias x a -> [x]
rtTArgs RTAlias a a
rta)
          (targs, eargs) = splitAt n ts
          msg = [Char]
"FIX-EXPRESSION-ARG: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Located LHName -> [Char]
forall a. PPrint a => a -> [Char]
showpp (RTAlias a a -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName RTAlias a a
rta)
          toExprArg = SourcePos -> [Char] -> BareTypeParsed -> ExprBV Symbol LocSymbol
exprArg (Located b -> SourcePos
forall a. Loc a => a -> SourcePos
LH.fSourcePos Located b
lname) [Char]
msg
      pure $ targs ++ [ RExprArg $ toExprArg e <$ lname | e <- eargs ]

mapMBareTypes :: forall m a.(Data a, Monad m) => (BareTypeParsed -> m BareTypeParsed) -> a -> m a
mapMBareTypes :: forall (m :: * -> *) a.
(Data a, Monad m) =>
(BareTypeParsed -> m BareTypeParsed) -> a -> m a
mapMBareTypes BareTypeParsed -> m BareTypeParsed
f  = a -> m a
forall b. Data b => b -> m b
go
  where
    go :: forall b. Data b => b -> m b
    go :: forall b. Data b => b -> m b
go = (forall b. Data b => b -> m b) -> b -> m b
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> a -> m a
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> b -> m b
gmapM (d -> m d
forall b. Data b => b -> m b
go (d -> m d) -> (BareTypeParsed -> m BareTypeParsed) -> d -> m d
forall (m :: * -> *) a b.
(Monad m, Typeable a, Typeable b) =>
(a -> m a) -> (b -> m b) -> a -> m a
`extM` BareTypeParsed -> m BareTypeParsed
f)

-- | exprArg converts a tyVar to an exprVar because parser cannot tell
--   this function allows us to treating (parsed) "types" as "value"
--   arguments, e.g. type Matrix a Row Col = List (List a Row) Col
--   Note that during parsing, we don't necessarily know whether a
--   string is a type or a value expression. E.g. in tests/pos/T1189.hs,
--   the string `Prop (Ev (plus n n))` where `Prop` is the alias:
--     {-@ type Prop E = {v:_ | prop v = E} @-}
--   the parser will chomp in `Ev (plus n n)` as a `BareType` and so
-- | @exprArg@ converts a type to a value.
--
--   At parse time the arguments of type aliases are all treated as types.
--   This needs fixing before verification because some arguments are
--   meant to be values. Hence, this function to correct the
--   arguments in question. See the documentation of
--   @fixExpressionArgsOfTypeAliases@ for some more context.
exprArg :: SourcePos -> String -> BareTypeParsed -> ExprV LocSymbol
exprArg :: SourcePos -> [Char] -> BareTypeParsed -> ExprBV Symbol LocSymbol
exprArg SourcePos
l [Char]
msg = [Char] -> ExprBV Symbol LocSymbol -> ExprBV Symbol LocSymbol
forall a. PPrint a => [Char] -> a -> a
notracepp ([Char]
"exprArg: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) (ExprBV Symbol LocSymbol -> ExprBV Symbol LocSymbol)
-> (BareTypeParsed -> ExprBV Symbol LocSymbol)
-> BareTypeParsed
-> ExprBV Symbol LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareTypeParsed -> ExprBV Symbol LocSymbol
go
  where
    go :: BareTypeParsed -> ExprV LocSymbol
    go :: BareTypeParsed -> ExprBV Symbol LocSymbol
go (RExprArg Located (ExprBV Symbol LocSymbol)
e)     = Located (ExprBV Symbol LocSymbol) -> ExprBV Symbol LocSymbol
forall a. Located a -> a
val Located (ExprBV Symbol LocSymbol)
e
    go (RVar (BTV LocSymbol
x) UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
_) = LocSymbol -> ExprBV Symbol LocSymbol
forall b v. v -> ExprBV b v
EVar LocSymbol
x
    go (RApp BTyCon
x [] [] UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
_) = LocSymbol -> ExprBV Symbol LocSymbol
forall b v. v -> ExprBV b v
EVar (LHName -> Symbol
getLHNameSymbol (LHName -> Symbol) -> Located LHName -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BTyCon -> Located LHName
btc_tc BTyCon
x)
    go (RApp BTyCon
f [BareTypeParsed]
ts [] UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
_) = ExprBV Symbol LocSymbol
-> [ExprBV Symbol LocSymbol] -> ExprBV Symbol LocSymbol
forall b v. ExprBV b v -> [ExprBV b v] -> ExprBV b v
eApps (LocSymbol -> ExprBV Symbol LocSymbol
forall b v. v -> ExprBV b v
EVar (Symbol -> Symbol
renameAmbiguousCtor (Symbol -> Symbol) -> (LHName -> Symbol) -> LHName -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LHName -> Symbol
getLHNameSymbol (LHName -> Symbol) -> Located LHName -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BTyCon -> Located LHName
btc_tc BTyCon
f)) (BareTypeParsed -> ExprBV Symbol LocSymbol
go (BareTypeParsed -> ExprBV Symbol LocSymbol)
-> [BareTypeParsed] -> [ExprBV Symbol LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BareTypeParsed]
ts)
    go (RAppTy BareTypeParsed
t1 BareTypeParsed
t2 UReftBV Symbol LocSymbol (ReftBV Symbol LocSymbol)
_) = ExprBV Symbol LocSymbol
-> ExprBV Symbol LocSymbol -> ExprBV Symbol LocSymbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
EApp (BareTypeParsed -> ExprBV Symbol LocSymbol
go BareTypeParsed
t1) (BareTypeParsed -> ExprBV Symbol LocSymbol
go BareTypeParsed
t2)
    go BareTypeParsed
z                = Maybe SrcSpan -> [Char] -> ExprBV Symbol LocSymbol
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
sp ([Char] -> ExprBV Symbol LocSymbol)
-> [Char] -> ExprBV Symbol LocSymbol
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> [Char] -> [Char]
forall r. PrintfType r => [Char] -> r
Printf.printf [Char]
"Unexpected expression parameter: %s in %s" (BareType -> [Char]
forall a. Show a => a -> [Char]
show (BareType -> [Char]) -> BareType -> [Char]
forall a b. (a -> b) -> a -> b
$ BareTypeParsed -> BareType
parsedToBareType BareTypeParsed
z) [Char]
msg
    sp :: Maybe SrcSpan
sp                  = SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SourcePos -> SrcSpan
LH.sourcePosSrcSpan SourcePos
l)

renameAmbiguousCtor :: Symbol -> Symbol
renameAmbiguousCtor :: Symbol -> Symbol
renameAmbiguousCtor Symbol
x
  | Just Int
n <- Symbol -> Maybe Int
isTyTupleSizedSymbol Symbol
x = Int -> Symbol
tmTupleSizedSymbol Int
n
  | Bool
otherwise = Symbol
x

-- | A type alias 'lookupInScopeEnv' that distinguishes locally defined names
-- from imported ones based on their resolution status:
-- unresolved names correspond to type aliases defined in the current module,
-- whereas all imported names are expected to be resolved.
resolveTypeAlias
   :: InScopeEnv (RTAlias Symbol a)
   -> Symbol
   -> TypeAliasResolution (RTAlias Symbol a)
resolveTypeAlias :: forall a.
InScopeEnv (RTAlias Symbol a)
-> Symbol -> TypeAliasResolution (RTAlias Symbol a)
resolveTypeAlias InScopeEnv (RTAlias Symbol a)
taliases Symbol
s = case InScopeEnv (RTAlias Symbol a)
-> Symbol
-> Either [Symbol] [(GenModule Unit, LHName, RTAlias Symbol a)]
forall a.
InScopeEnv a
-> Symbol -> Either [Symbol] [(GenModule Unit, LHName, a)]
lookupInScopeEnv InScopeEnv (RTAlias Symbol a)
taliases  Symbol
s of
  Right [(GenModule Unit, LHName, RTAlias Symbol a)]
ns -> let ([(GenModule Unit, LHName, RTAlias Symbol a)]
imported, [(GenModule Unit, LHName, RTAlias Symbol a)]
local) =
                    ((GenModule Unit, LHName, RTAlias Symbol a) -> Bool)
-> [(GenModule Unit, LHName, RTAlias Symbol a)]
-> ([(GenModule Unit, LHName, RTAlias Symbol a)],
    [(GenModule Unit, LHName, RTAlias Symbol a)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(GenModule Unit
_,LHName
lhname,RTAlias Symbol a
_) -> LHName -> Bool
isResolvedLogicName LHName
lhname ) [(GenModule Unit, LHName, RTAlias Symbol a)]
ns
              in [(GenModule Unit, LHName, RTAlias Symbol a)]
-> [(GenModule Unit, LHName, RTAlias Symbol a)]
-> TypeAliasResolution (RTAlias Symbol a)
forall a.
[(GenModule Unit, LHName, a)]
-> [(GenModule Unit, LHName, a)] -> TypeAliasResolution a
FoundTypeAliases [(GenModule Unit, LHName, RTAlias Symbol a)]
imported [(GenModule Unit, LHName, RTAlias Symbol a)]
local
  Left [Symbol]
alts -> [Symbol] -> TypeAliasResolution (RTAlias Symbol a)
forall a. [Symbol] -> TypeAliasResolution a
NoSuchTypeAlias [Symbol]
alts

-- | When resolving type aliases we either find matching 'LHName's
-- or similar, but distinct, 'Symbol's.
data TypeAliasResolution a
  = NoSuchTypeAlias [Symbol]
  | FoundTypeAliases
      { forall a. TypeAliasResolution a -> [(GenModule Unit, LHName, a)]
tarImported :: [(GHC.Module, LHName, a)]
      , forall a. TypeAliasResolution a -> [(GenModule Unit, LHName, a)]
tarLocallyDefined :: [(GHC.Module, LHName, a)]
      }

errResolveTypeAlias :: LocSymbol -> TypeAliasResolution (RTAlias x a) -> Error
errResolveTypeAlias :: forall x a. LocSymbol -> TypeAliasResolution (RTAlias x a) -> Error
errResolveTypeAlias LocSymbol
ls (FoundTypeAliases [(GenModule Unit, LHName, RTAlias x a)]
imported [(GenModule Unit, LHName, RTAlias x a)]
local) =
  SrcSpan -> Doc -> Doc -> [Doc] -> Error
forall t. SrcSpan -> Doc -> Doc -> [Doc] -> TError t
ErrDupNames (LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
LH.fSrcSpan LocSymbol
ls) Doc
"type alias" (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (Symbol -> Doc) -> Symbol -> Doc
forall a b. (a -> b) -> a -> b
$ LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
ls)
    (
      -- Currently, multiple local definitions prevent this error from being raised,
      -- because duplicate names are discarded when constructing the alias environment
      -- for each individual module,
      -- and a local alias always shadows any imported one. Such duplicates are detected
      -- later during validation of the final target spec.
      --
      -- Also, note that collected local type alias names remain unresolved at this stage,
      -- so we must extract their symbol using a function that can safely handle unresolved
      -- names.
      ((GenModule Unit, LHName, RTAlias x a) -> Doc)
-> [(GenModule Unit, LHName, RTAlias x a)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\(GenModule Unit
_, LHName
lhn, RTAlias x a
rta) -> Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (LHName -> Symbol
getLHNameSymbol LHName
lhn)
                             Doc -> Doc -> Doc
PJ.<+>
                             [Char] -> Doc
PJ.text [Char]
"defined in current module at"
                             Doc -> Doc -> Doc
PJ.<+>
                             SrcSpan -> Doc
forall a. PPrint a => a -> Doc
pprint  (Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
LH.fSrcSpan (Located LHName -> SrcSpan)
-> (RTAlias x a -> Located LHName) -> RTAlias x a -> SrcSpan
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias x a -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName (RTAlias x a -> SrcSpan) -> RTAlias x a -> SrcSpan
forall a b. (a -> b) -> a -> b
$ RTAlias x a
rta)
          )
          [(GenModule Unit, LHName, RTAlias x a)]
local
     [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
     ((GenModule Unit, LHName, RTAlias x a) -> Doc)
-> [(GenModule Unit, LHName, RTAlias x a)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\(GenModule Unit
m, LHName
lhn, RTAlias x a
rta) -> Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (HasCallStack => LHName -> Symbol
LHName -> Symbol
lhNameToUnqualifiedSymbol LHName
lhn)
                            Doc -> Doc -> Doc
PJ.<+>
                            [Char] -> Doc
PJ.text [Char]
"imported from module"
                            Doc -> Doc -> Doc
PJ.<+>
                            [Char] -> Doc
PJ.text (ModuleName -> [Char]
GHC.moduleNameString (GenModule Unit -> ModuleName
forall unit. GenModule unit -> ModuleName
GHC.moduleName GenModule Unit
m))
                            Doc -> Doc -> Doc
PJ.<+>
                            [Char] -> Doc
PJ.text [Char]
"defined at"
                            Doc -> Doc -> Doc
PJ.<+>
                            SrcSpan -> Doc
forall a. PPrint a => a -> Doc
pprint (Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
LH.fSrcSpan (Located LHName -> SrcSpan)
-> (RTAlias x a -> Located LHName) -> RTAlias x a -> SrcSpan
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias x a -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName (RTAlias x a -> SrcSpan) -> RTAlias x a -> SrcSpan
forall a b. (a -> b) -> a -> b
$ RTAlias x a
rta)
         )
         [(GenModule Unit, LHName, RTAlias x a)]
imported
    )
errResolveTypeAlias LocSymbol
ls (NoSuchTypeAlias [Symbol]
alts) =
  [Symbol] -> Doc -> [Char] -> LocSymbol -> Error
errResolve [Symbol]
alts Doc
"type alias" [Char]
"Cannot resolve name" LocSymbol
ls


-- | An environment of names in scope
--
-- We construct it using 'mkAliasEnv' and 'unionAliasEnvs' in such a way that each
-- symbol in the environment corresponds to all matching 'LHNames' along with
-- the aliases of the module we import it from.
-- Currently, the parameter is used to include the type alias representation when
-- we 'collectTypeAliases'.
type InScopeEnv a = SEnv [(GHC.ModuleName, (GHC.Module, LHName, a))]

type InScopeNonReflectedEnv = InScopeEnv ()

-- | Looks for the 'LHName's in scope with the given symbol,
-- taking possible qualification prefixes into account.
-- Returns a list of close but different symbols or a non-empty list
-- with the matched names.
lookupInScopeEnv
  :: InScopeEnv a -> Symbol -> Either [Symbol] [(GHC.Module, LHName, a)]
lookupInScopeEnv :: forall a.
InScopeEnv a
-> Symbol -> Either [Symbol] [(GenModule Unit, LHName, a)]
lookupInScopeEnv InScopeEnv a
env Symbol
s = do
    -- The symbol might be qualified or not,
    -- but we use the unqualified symbol for the lookup.
    let n :: Symbol
n = Symbol -> Symbol
LH.dropModuleNames Symbol
s
    case Symbol
-> InScopeEnv a
-> SESearchB Symbol [(ModuleName, (GenModule Unit, LHName, a))]
forall b a. Binder b => b -> SEnvB b a -> SESearchB b a
lookupSEnvWithDistance Symbol
n InScopeEnv a
env of
      Alts [Symbol]
closeSyms -> [Symbol] -> Either [Symbol] [(GenModule Unit, LHName, a)]
forall a b. a -> Either a b
Left [Symbol]
closeSyms
      F.Found [(ModuleName, (GenModule Unit, LHName, a))]
xs -> do
         let q :: Symbol
q = Symbol -> Symbol
LH.takeModuleNames Symbol
s
         case ((ModuleName, (GenModule Unit, LHName, a)) -> Bool)
-> [(ModuleName, (GenModule Unit, LHName, a))]
-> [(ModuleName, (GenModule Unit, LHName, a))]
forall a. (a -> Bool) -> [a] -> [a]
filter (([Char] -> FastString
GHC.mkFastString (Symbol -> [Char]
symbolString Symbol
q) FastString -> FastString -> Bool
forall a. Eq a => a -> a -> Bool
==) (FastString -> Bool)
-> ((ModuleName, (GenModule Unit, LHName, a)) -> FastString)
-> (ModuleName, (GenModule Unit, LHName, a))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> FastString
GHC.moduleNameFS (ModuleName -> FastString)
-> ((ModuleName, (GenModule Unit, LHName, a)) -> ModuleName)
-> (ModuleName, (GenModule Unit, LHName, a))
-> FastString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleName, (GenModule Unit, LHName, a)) -> ModuleName
forall a b. (a, b) -> a
fst) [(ModuleName, (GenModule Unit, LHName, a))]
xs of
           [] -> [Symbol] -> Either [Symbol] [(GenModule Unit, LHName, a)]
forall a b. a -> Either a b
Left ([Symbol] -> Either [Symbol] [(GenModule Unit, LHName, a)])
-> [Symbol] -> Either [Symbol] [(GenModule Unit, LHName, a)]
forall a b. (a -> b) -> a -> b
$ ((ModuleName, (GenModule Unit, LHName, a)) -> Symbol)
-> [(ModuleName, (GenModule Unit, LHName, a))] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol -> Symbol -> Symbol
maybeQualifySymbol Symbol
n (Symbol -> Symbol)
-> ((ModuleName, (GenModule Unit, LHName, a)) -> Symbol)
-> (ModuleName, (GenModule Unit, LHName, a))
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol ([Char] -> Symbol)
-> ((ModuleName, (GenModule Unit, LHName, a)) -> [Char])
-> (ModuleName, (GenModule Unit, LHName, a))
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> [Char]
GHC.moduleNameString (ModuleName -> [Char])
-> ((ModuleName, (GenModule Unit, LHName, a)) -> ModuleName)
-> (ModuleName, (GenModule Unit, LHName, a))
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleName, (GenModule Unit, LHName, a)) -> ModuleName
forall a b. (a, b) -> a
fst) [(ModuleName, (GenModule Unit, LHName, a))]
xs
           [(ModuleName, (GenModule Unit, LHName, a))]
ys -> [(GenModule Unit, LHName, a)]
-> Either [Symbol] [(GenModule Unit, LHName, a)]
forall a b. b -> Either a b
Right ([(GenModule Unit, LHName, a)]
 -> Either [Symbol] [(GenModule Unit, LHName, a)])
-> [(GenModule Unit, LHName, a)]
-> Either [Symbol] [(GenModule Unit, LHName, a)]
forall a b. (a -> b) -> a -> b
$ ((ModuleName, (GenModule Unit, LHName, a))
 -> (GenModule Unit, LHName, a))
-> [(ModuleName, (GenModule Unit, LHName, a))]
-> [(GenModule Unit, LHName, a)]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleName, (GenModule Unit, LHName, a))
-> (GenModule Unit, LHName, a)
forall a b. (a, b) -> b
snd [(ModuleName, (GenModule Unit, LHName, a))]
ys
  where
    maybeQualifySymbol :: Symbol -> Symbol -> Symbol
maybeQualifySymbol Symbol
n Symbol
m =
      if Symbol
m Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"" then Symbol
n else Symbol -> Symbol -> Symbol
LH.qualifySymbol Symbol
m Symbol
n

-- | Builds an environment of non-reflected names in scope from the module
-- imports for the current module, the spec of the current module, and the specs
-- of the dependencies.
--
-- Also returns a LogicNameEnv constructed from the same names.
-- Also returns the names of reflected private functions.
-- Also returns the set of all names that aren't handled yet by name resolution.
makeLogicEnvs
  :: GHC.ImportedMods
  -> GHC.Module
  -> BareSpecParsed
  -> TargetDependencies
  -> ( InScopeNonReflectedEnv
     , LogicNameEnv
     , HS.HashSet LocSymbol
     )
makeLogicEnvs :: ImportedMods
-> GenModule Unit
-> Spec LocSymbol BareTypeParsed
-> TargetDependencies
-> (InScopeNonReflectedEnv, LogicNameEnv, HashSet LocSymbol)
makeLogicEnvs ImportedMods
impMods GenModule Unit
thisModule Spec LocSymbol BareTypeParsed
spec TargetDependencies
dependencies =
    let depsLogicNames :: [(GenModule Unit, [LHName])]
depsLogicNames =
          ((GenModule Unit, LiftedSpec) -> (GenModule Unit, [LHName]))
-> [(GenModule Unit, LiftedSpec)] -> [(GenModule Unit, [LHName])]
forall a b. (a -> b) -> [a] -> [b]
map ((LiftedSpec -> [LHName])
-> (GenModule Unit, LiftedSpec) -> (GenModule Unit, [LHName])
forall a b. (a -> b) -> (GenModule Unit, a) -> (GenModule Unit, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LiftedSpec -> [LHName]
collectLiftedSpecLogicNames) [(GenModule Unit, LiftedSpec)]
dependencyPairs
        logicNames :: [(GenModule Unit, [LHName])]
logicNames =
          (GenModule Unit
thisModule, [LHName]
thisModuleNames) (GenModule Unit, [LHName])
-> [(GenModule Unit, [LHName])] -> [(GenModule Unit, [LHName])]
forall a. a -> [a] -> [a]
: [(GenModule Unit, [LHName])]
depsLogicNames
        nonReflectedNamesWithUnit :: [(GenModule Unit, [(LHName, ())])]
nonReflectedNamesWithUnit =
          ((GenModule Unit, [LHName]) -> (GenModule Unit, [(LHName, ())]))
-> [(GenModule Unit, [LHName])]
-> [(GenModule Unit, [(LHName, ())])]
forall a b. (a -> b) -> [a] -> [b]
map
            (([LHName] -> [(LHName, ())])
-> (GenModule Unit, [LHName]) -> (GenModule Unit, [(LHName, ())])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (([LHName] -> [(LHName, ())])
 -> (GenModule Unit, [LHName]) -> (GenModule Unit, [(LHName, ())]))
-> ([LHName] -> [(LHName, ())])
-> (GenModule Unit, [LHName])
-> (GenModule Unit, [(LHName, ())])
forall a b. (a -> b) -> a -> b
$ (LHName -> (LHName, ())) -> [LHName] -> [(LHName, ())]
forall a b. (a -> b) -> [a] -> [b]
map (, ()) ([LHName] -> [(LHName, ())])
-> ([LHName] -> [LHName]) -> [LHName] -> [(LHName, ())]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LHName -> Bool) -> [LHName] -> [LHName]
forall a. (a -> Bool) -> [a] -> [a]
filter LHName -> Bool
isNonReflectedLogicName)
            [(GenModule Unit, [LHName])]
logicNames
        thisModuleNames :: [LHName]
thisModuleNames = [[LHName]] -> [LHName]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ [ HasCallStack => GenModule Unit -> LHName -> LHName
GenModule Unit -> LHName -> LHName
reflectLHName GenModule Unit
thisModule (Located LHName -> LHName
forall a. Located a -> a
val Located LHName
n)
            | Located LHName
n <- [[Located LHName]] -> [Located LHName]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
              [ ((Located LHName, Located LHName) -> Located LHName)
-> [(Located LHName, Located LHName)] -> [Located LHName]
forall a b. (a -> b) -> [a] -> [b]
map (Located LHName, Located LHName) -> Located LHName
forall a b. (a, b) -> a
fst (Spec LocSymbol BareTypeParsed -> [(Located LHName, Located LHName)]
forall lname ty.
Spec lname ty -> [(Located LHName, Located LHName)]
asmReflectSigs Spec LocSymbol BareTypeParsed
spec)
              , HashSet (Located LHName) -> [Located LHName]
forall a. HashSet a -> [a]
HS.toList (Spec LocSymbol BareTypeParsed -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
reflects Spec LocSymbol BareTypeParsed
spec)
              , HashSet (Located LHName) -> [Located LHName]
forall a. HashSet a -> [a]
HS.toList (Spec LocSymbol BareTypeParsed -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
opaqueReflects Spec LocSymbol BareTypeParsed
spec)
              , HashSet (Located LHName) -> [Located LHName]
forall a. HashSet a -> [a]
HS.toList (Spec LocSymbol BareTypeParsed -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
inlines Spec LocSymbol BareTypeParsed
spec)
              , HashSet (Located LHName) -> [Located LHName]
forall a. HashSet a -> [a]
HS.toList (Spec LocSymbol BareTypeParsed -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
hmeas Spec LocSymbol BareTypeParsed
spec)
              ]
            ]
          , [ Located LHName -> LHName
forall a. Located a -> a
val (MeasureV LocSymbol (Located BareTypeParsed) (Located LHName)
-> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName MeasureV LocSymbol (Located BareTypeParsed) (Located LHName)
m) | MeasureV LocSymbol (Located BareTypeParsed) (Located LHName)
m <- Spec LocSymbol BareTypeParsed
-> [MeasureV LocSymbol (Located BareTypeParsed) (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
measures Spec LocSymbol BareTypeParsed
spec ]
          , [ Located LHName -> LHName
forall a. Located a -> a
val (MeasureV LocSymbol (Located BareTypeParsed) () -> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName MeasureV LocSymbol (Located BareTypeParsed) ()
m) | MeasureV LocSymbol (Located BareTypeParsed) ()
m <- Spec LocSymbol BareTypeParsed
-> [MeasureV LocSymbol (Located BareTypeParsed) ()]
forall lname ty. Spec lname ty -> [MeasureV lname (Located ty) ()]
cmeasures Spec LocSymbol BareTypeParsed
spec ]
          , ((LHName, BareTypeParsed) -> LHName)
-> [(LHName, BareTypeParsed)] -> [LHName]
forall a b. (a -> b) -> [a] -> [b]
map (LHName, BareTypeParsed) -> LHName
forall a b. (a, b) -> a
fst ([(LHName, BareTypeParsed)] -> [LHName])
-> [(LHName, BareTypeParsed)] -> [LHName]
forall a b. (a -> b) -> a -> b
$
             (DataCtorP BareTypeParsed -> [(LHName, BareTypeParsed)])
-> [DataCtorP BareTypeParsed] -> [(LHName, BareTypeParsed)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataCtorP BareTypeParsed -> [(LHName, BareTypeParsed)]
forall ty. DataCtorP ty -> [(LHName, ty)]
DataDecl.dcFields ([DataCtorP BareTypeParsed] -> [(LHName, BareTypeParsed)])
-> [DataCtorP BareTypeParsed] -> [(LHName, BareTypeParsed)]
forall a b. (a -> b) -> a -> b
$ [[DataCtorP BareTypeParsed]] -> [DataCtorP BareTypeParsed]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[DataCtorP BareTypeParsed]] -> [DataCtorP BareTypeParsed])
-> [[DataCtorP BareTypeParsed]] -> [DataCtorP BareTypeParsed]
forall a b. (a -> b) -> a -> b
$
             (DataDeclP LocSymbol BareTypeParsed
 -> Maybe [DataCtorP BareTypeParsed])
-> [DataDeclP LocSymbol BareTypeParsed]
-> [[DataCtorP BareTypeParsed]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe DataDeclP LocSymbol BareTypeParsed
-> Maybe [DataCtorP BareTypeParsed]
forall v ty. DataDeclP v ty -> Maybe [DataCtorP ty]
DataDecl.tycDCons ([DataDeclP LocSymbol BareTypeParsed]
 -> [[DataCtorP BareTypeParsed]])
-> [DataDeclP LocSymbol BareTypeParsed]
-> [[DataCtorP BareTypeParsed]]
forall a b. (a -> b) -> a -> b
$
             Spec LocSymbol BareTypeParsed
-> [DataDeclP LocSymbol BareTypeParsed]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
dataDecls Spec LocSymbol BareTypeParsed
spec
          , [ Located LHName -> LHName
forall a. Located a -> a
val (RTAlias Symbol (ExprBV Symbol LocSymbol) -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName RTAlias Symbol (ExprBV Symbol LocSymbol)
ea) | RTAlias Symbol (ExprBV Symbol LocSymbol)
ea <- Spec LocSymbol BareTypeParsed
-> [RTAlias Symbol (ExprBV Symbol LocSymbol)]
forall lname ty. Spec lname ty -> [RTAlias Symbol (ExprV lname)]
ealiases Spec LocSymbol BareTypeParsed
spec ]
          ]
        privateReflectNames :: HashSet LocSymbol
privateReflectNames =
          [HashSet LocSymbol] -> HashSet LocSymbol
forall a. Monoid a => [a] -> a
mconcat ([HashSet LocSymbol] -> HashSet LocSymbol)
-> [HashSet LocSymbol] -> HashSet LocSymbol
forall a b. (a -> b) -> a -> b
$
            Spec LocSymbol BareTypeParsed -> HashSet LocSymbol
forall lname ty. Spec lname ty -> HashSet LocSymbol
privateReflects Spec LocSymbol BareTypeParsed
spec HashSet LocSymbol -> [HashSet LocSymbol] -> [HashSet LocSymbol]
forall a. a -> [a] -> [a]
: ((GenModule Unit, LiftedSpec) -> HashSet LocSymbol)
-> [(GenModule Unit, LiftedSpec)] -> [HashSet LocSymbol]
forall a b. (a -> b) -> [a] -> [b]
map (LiftedSpec -> HashSet LocSymbol
liftedPrivateReflects (LiftedSpec -> HashSet LocSymbol)
-> ((GenModule Unit, LiftedSpec) -> LiftedSpec)
-> (GenModule Unit, LiftedSpec)
-> HashSet LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GenModule Unit, LiftedSpec) -> LiftedSpec
forall a b. (a, b) -> b
snd) [(GenModule Unit, LiftedSpec)]
dependencyPairs
     in
        ( [InScopeNonReflectedEnv] -> InScopeNonReflectedEnv
forall a. [InScopeEnv a] -> InScopeEnv a
unionAliasEnvs ([InScopeNonReflectedEnv] -> InScopeNonReflectedEnv)
-> [InScopeNonReflectedEnv] -> InScopeNonReflectedEnv
forall a b. (a -> b) -> a -> b
$ ((GenModule Unit, [(LHName, ())]) -> InScopeNonReflectedEnv)
-> [(GenModule Unit, [(LHName, ())])] -> [InScopeNonReflectedEnv]
forall a b. (a -> b) -> [a] -> [b]
map (GenModule Unit
-> ImportedMods
-> (GenModule Unit, [(LHName, ())])
-> InScopeNonReflectedEnv
forall a.
GenModule Unit
-> ImportedMods -> (GenModule Unit, [(LHName, a)]) -> InScopeEnv a
mkAliasEnv GenModule Unit
thisModule ImportedMods
impMods) [(GenModule Unit, [(LHName, ())])]
nonReflectedNamesWithUnit
        , [LHName] -> LogicNameEnv
mkLogicNameEnv (((GenModule Unit, [LHName]) -> [LHName])
-> [(GenModule Unit, [LHName])] -> [LHName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (GenModule Unit, [LHName]) -> [LHName]
forall a b. (a, b) -> b
snd [(GenModule Unit, [LHName])]
logicNames)
        , HashSet LocSymbol
privateReflectNames
        )
  where
    dependencyPairs :: [(GenModule Unit, LiftedSpec)]
dependencyPairs = ((StableModule, LiftedSpec) -> (GenModule Unit, LiftedSpec))
-> [(StableModule, LiftedSpec)] -> [(GenModule Unit, LiftedSpec)]
forall a b. (a -> b) -> [a] -> [b]
map ((StableModule -> GenModule Unit)
-> (StableModule, LiftedSpec) -> (GenModule Unit, LiftedSpec)
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 StableModule -> GenModule Unit
GHC.unStableModule) ([(StableModule, LiftedSpec)] -> [(GenModule Unit, LiftedSpec)])
-> [(StableModule, LiftedSpec)] -> [(GenModule Unit, LiftedSpec)]
forall a b. (a -> b) -> a -> b
$ HashMap StableModule LiftedSpec -> [(StableModule, LiftedSpec)]
forall k v. HashMap k v -> [(k, v)]
HM.toList (HashMap StableModule LiftedSpec -> [(StableModule, LiftedSpec)])
-> HashMap StableModule LiftedSpec -> [(StableModule, LiftedSpec)]
forall a b. (a -> b) -> a -> b
$ TargetDependencies -> HashMap StableModule LiftedSpec
getDependencies TargetDependencies
dependencies

    mkLogicNameEnv :: [LHName] -> LogicNameEnv
mkLogicNameEnv [LHName]
names =
      LogicNameEnv
        { lneLHName :: SEnv LHName
lneLHName = [(Symbol, LHName)] -> SEnv LHName
forall b a. Hashable b => [(b, a)] -> SEnvB b a
fromListSEnv [ (LHName -> Symbol
lhNameToResolvedSymbol LHName
n, LHName
n) | LHName
n <- [LHName]
names ]
        , lneReflected :: NameEnv LHName
lneReflected = [(Name, LHName)] -> NameEnv LHName
forall a. [(Name, a)] -> NameEnv a
GHC.mkNameEnv [(Name
rn, LHName
n) | LHName
n <- [LHName]
names, Just Name
rn <- [LHName -> Maybe Name
maybeReflectedLHName LHName
n]]
        }

unionAliasEnvs :: forall a. [InScopeEnv a] -> InScopeEnv a
unionAliasEnvs :: forall a. [InScopeEnv a] -> InScopeEnv a
unionAliasEnvs =
    HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))]
-> SEnvB Symbol [(ModuleName, (GenModule Unit, LHName, a))]
forall a b. Coercible a b => a -> b
coerce (HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))]
 -> SEnvB Symbol [(ModuleName, (GenModule Unit, LHName, a))])
-> ([SEnvB Symbol [(ModuleName, (GenModule Unit, LHName, a))]]
    -> HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))])
-> [SEnvB Symbol [(ModuleName, (GenModule Unit, LHName, a))]]
-> SEnvB Symbol [(ModuleName, (GenModule Unit, LHName, a))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    -- We make sure that the module alias and the 'LHName' effectively disambiguate
    -- the occurrence of a symbol. This is because the same name can come from
    -- several imported modules.
    ([(ModuleName, (GenModule Unit, LHName, a))]
 -> [(ModuleName, (GenModule Unit, LHName, a))])
-> HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))]
-> HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))]
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HM.map (((ModuleName, (GenModule Unit, LHName, a))
 -> (ModuleName, (GenModule Unit, LHName, a)) -> Bool)
-> [(ModuleName, (GenModule Unit, LHName, a))]
-> [(ModuleName, (GenModule Unit, LHName, a))]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (\(ModuleName
alias1, (GenModule Unit
_, LHName
n1, a
_)) (ModuleName
alias2, (GenModule Unit
_, LHName
n2, a
_)) -> ModuleName
alias1 ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleName
alias2 Bool -> Bool -> Bool
&& LHName
n1 LHName -> LHName -> Bool
forall a. Eq a => a -> a -> Bool
== LHName
n2)) (HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))]
 -> HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))])
-> ([SEnvB Symbol [(ModuleName, (GenModule Unit, LHName, a))]]
    -> HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))])
-> [SEnvB Symbol [(ModuleName, (GenModule Unit, LHName, a))]]
-> HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    (HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))]
 -> HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))]
 -> HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))])
-> HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))]
-> [HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))]]
-> HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (([(ModuleName, (GenModule Unit, LHName, a))]
 -> [(ModuleName, (GenModule Unit, LHName, a))]
 -> [(ModuleName, (GenModule Unit, LHName, a))])
-> HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))]
-> HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))]
-> HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))]
forall k v.
Eq k =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HM.unionWith [(ModuleName, (GenModule Unit, LHName, a))]
-> [(ModuleName, (GenModule Unit, LHName, a))]
-> [(ModuleName, (GenModule Unit, LHName, a))]
forall a. [a] -> [a] -> [a]
(++)) HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))]
forall k v. HashMap k v
HM.empty ([HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))]]
 -> HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))])
-> ([SEnvB Symbol [(ModuleName, (GenModule Unit, LHName, a))]]
    -> [HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))]])
-> [SEnvB Symbol [(ModuleName, (GenModule Unit, LHName, a))]]
-> HashMap Symbol [(ModuleName, (GenModule Unit, LHName, a))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @_ @[HM.HashMap Symbol [(GHC.ModuleName, (GHC.Module, LHName, a))]]

-- | Builds a symbol lookup environment from a list of names associated with the
-- module they were extracted from, adding any import aliases that module may
-- have within the current module (if it was imported directly).
mkAliasEnv:: GHC.Module -> GHC.ImportedMods -> (GHC.Module, [(LHName, a)]) -> InScopeEnv a
mkAliasEnv :: forall a.
GenModule Unit
-> ImportedMods -> (GenModule Unit, [(LHName, a)]) -> InScopeEnv a
mkAliasEnv GenModule Unit
thisModule ImportedMods
impMods (GenModule Unit
m, [(LHName, a)]
lhnames) =
    let aliases :: [ModuleName]
aliases = GenModule Unit -> ImportedMods -> GenModule Unit -> [ModuleName]
moduleAliases GenModule Unit
thisModule ImportedMods
impMods GenModule Unit
m
     in [(Symbol, [(ModuleName, (GenModule Unit, LHName, a))])]
-> SEnvB Symbol [(ModuleName, (GenModule Unit, LHName, a))]
forall b a. Hashable b => [(b, a)] -> SEnvB b a
fromListSEnv
          -- Note that when building a name environment for the current module
          -- we might process unresolved names here.
          [ (Symbol -> Symbol
LH.dropModuleNames (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ LHName -> Symbol
getLHNameSymbol LHName
lhname
            , (ModuleName -> (ModuleName, (GenModule Unit, LHName, a)))
-> [ModuleName] -> [(ModuleName, (GenModule Unit, LHName, a))]
forall a b. (a -> b) -> [a] -> [b]
map (,(GenModule Unit
m, LHName
lhname, a
x)) [ModuleName]
aliases)
          | (LHName
lhname, a
x) <- [(LHName, a)]
lhnames
          ]

-- | Produces the list of aliases a module is imported with.
-- The first parameter holds the reference to the current module.
-- Transitive dependencies get an empty alias list.
moduleAliases :: GHC.Module -> GHC.ImportedMods -> GHC.Module -> [GHC.ModuleName]
moduleAliases :: GenModule Unit -> ImportedMods -> GenModule Unit -> [ModuleName]
moduleAliases GenModule Unit
thisModule ImportedMods
impMods GenModule Unit
m =
    case GenModule Unit -> ImportedMods -> Maybe [ImportedBy]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup GenModule Unit
m ImportedMods
impMods of
      -- Aliases for imported modules.
      Just [ImportedBy]
impBys -> (ImportedModsVal -> [ModuleName])
-> [ImportedModsVal] -> [ModuleName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ImportedModsVal -> [ModuleName]
imvAliases ([ImportedModsVal] -> [ModuleName])
-> [ImportedModsVal] -> [ModuleName]
forall a b. (a -> b) -> a -> b
$ [ImportedBy] -> [ImportedModsVal]
GHC.importedByUser [ImportedBy]
impBys
      Maybe [ImportedBy]
Nothing
        | GenModule Unit
thisModule GenModule Unit -> GenModule Unit -> Bool
forall a. Eq a => a -> a -> Bool
== GenModule Unit
m ->
          -- Aliases for the current module.
          [GenModule Unit -> ModuleName
forall unit. GenModule unit -> ModuleName
GHC.moduleName GenModule Unit
m, [Char] -> ModuleName
GHC.mkModuleName [Char]
""]
        | Bool
otherwise ->
          -- For LHAssumptions modules, use the aliases of the unsuffixed module.
          (ImportedModsVal -> [ModuleName])
-> [ImportedModsVal] -> [ModuleName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ImportedModsVal -> [ModuleName]
imvAliases ([ImportedModsVal] -> [ModuleName])
-> [ImportedModsVal] -> [ModuleName]
forall a b. (a -> b) -> a -> b
$ [ImportedBy] -> [ImportedModsVal]
GHC.importedByUser ([ImportedBy] -> [ImportedModsVal])
-> [ImportedBy] -> [ImportedModsVal]
forall a b. (a -> b) -> a -> b
$
            [[ImportedBy]] -> [ImportedBy]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[ImportedBy]] -> [ImportedBy]) -> [[ImportedBy]] -> [ImportedBy]
forall a b. (a -> b) -> a -> b
$ Maybe [ImportedBy] -> [[ImportedBy]]
forall a. Maybe a -> [a]
maybeToList (Maybe [ImportedBy] -> [[ImportedBy]])
-> Maybe [ImportedBy] -> [[ImportedBy]]
forall a b. (a -> b) -> a -> b
$ do
              pString <- Maybe [Char]
dropLHAssumptionsSuffix
              pMod <- findDependency pString
              Map.lookup pMod impMods
  where
    dropLHAssumptionsSuffix :: Maybe [Char]
dropLHAssumptionsSuffix =
      let mString :: [Char]
mString = ModuleName -> [Char]
GHC.moduleNameString (GenModule Unit -> ModuleName
forall unit. GenModule unit -> ModuleName
GHC.moduleName GenModule Unit
m)
          sfx :: [Char]
sfx = [Char]
"_LHAssumptions"
       in if [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isSuffixOf [Char]
sfx [Char]
mString then
            [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char]) -> [Char] -> Maybe [Char]
forall a b. (a -> b) -> a -> b
$ Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
dropEnd ([Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
sfx) [Char]
mString
          else
            Maybe [Char]
forall a. Maybe a
Nothing

    findDependency :: [Char] -> Maybe (GenModule Unit)
findDependency [Char]
ms =
      (GenModule Unit -> Bool)
-> [GenModule Unit] -> Maybe (GenModule Unit)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (([Char]
ms [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
==) ([Char] -> Bool)
-> (GenModule Unit -> [Char]) -> GenModule Unit -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> [Char]
GHC.moduleNameString (ModuleName -> [Char])
-> (GenModule Unit -> ModuleName) -> GenModule Unit -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenModule Unit -> ModuleName
forall unit. GenModule unit -> ModuleName
GHC.moduleName) ([GenModule Unit] -> Maybe (GenModule Unit))
-> [GenModule Unit] -> Maybe (GenModule Unit)
forall a b. (a -> b) -> a -> b
$
      ImportedMods -> [GenModule Unit]
forall k a. Map k a -> [k]
Map.keys ImportedMods
impMods

    imvAliases :: ImportedModsVal -> [ModuleName]
imvAliases ImportedModsVal
imv
      | ImportedModsVal -> Bool
GHC.imv_qualified ImportedModsVal
imv = [ImportedModsVal -> ModuleName
GHC.imv_name ImportedModsVal
imv]
      | Bool
otherwise = [ImportedModsVal -> ModuleName
GHC.imv_name ImportedModsVal
imv, [Char] -> ModuleName
GHC.mkModuleName [Char]
""]

collectLiftedSpecLogicNames :: LiftedSpec -> [LHName]
collectLiftedSpecLogicNames :: LiftedSpec -> [LHName]
collectLiftedSpecLogicNames LiftedSpec
sp = [[LHName]] -> [LHName]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ ((LHName, Sort) -> LHName) -> [(LHName, Sort)] -> [LHName]
forall a b. (a -> b) -> [a] -> [b]
map (LHName, Sort) -> LHName
forall a b. (a, b) -> a
fst (HashSet (LHName, Sort) -> [(LHName, Sort)]
forall a. HashSet a -> [a]
HS.toList (HashSet (LHName, Sort) -> [(LHName, Sort)])
-> HashSet (LHName, Sort) -> [(LHName, Sort)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec -> HashSet (LHName, Sort)
liftedExpSigs LiftedSpec
sp)
    , (MeasureV LHName LocBareTypeLHName (Located LHName) -> LHName)
-> [MeasureV LHName LocBareTypeLHName (Located LHName)] -> [LHName]
forall a b. (a -> b) -> [a] -> [b]
map (Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> (MeasureV LHName LocBareTypeLHName (Located LHName)
    -> Located LHName)
-> MeasureV LHName LocBareTypeLHName (Located LHName)
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MeasureV LHName LocBareTypeLHName (Located LHName)
-> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName) (HashMap Symbol (MeasureV LHName LocBareTypeLHName (Located LHName))
-> [MeasureV LHName LocBareTypeLHName (Located LHName)]
forall k v. HashMap k v -> [v]
HM.elems (HashMap
   Symbol (MeasureV LHName LocBareTypeLHName (Located LHName))
 -> [MeasureV LHName LocBareTypeLHName (Located LHName)])
-> HashMap
     Symbol (MeasureV LHName LocBareTypeLHName (Located LHName))
-> [MeasureV LHName LocBareTypeLHName (Located LHName)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
-> HashMap
     Symbol (MeasureV LHName LocBareTypeLHName (Located LHName))
liftedMeasures LiftedSpec
sp)
    , (MeasureV LHName LocBareTypeLHName () -> LHName)
-> [MeasureV LHName LocBareTypeLHName ()] -> [LHName]
forall a b. (a -> b) -> [a] -> [b]
map (Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> (MeasureV LHName LocBareTypeLHName () -> Located LHName)
-> MeasureV LHName LocBareTypeLHName ()
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MeasureV LHName LocBareTypeLHName () -> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName) (HashMap Symbol (MeasureV LHName LocBareTypeLHName ())
-> [MeasureV LHName LocBareTypeLHName ()]
forall k v. HashMap k v -> [v]
HM.elems (HashMap Symbol (MeasureV LHName LocBareTypeLHName ())
 -> [MeasureV LHName LocBareTypeLHName ()])
-> HashMap Symbol (MeasureV LHName LocBareTypeLHName ())
-> [MeasureV LHName LocBareTypeLHName ()]
forall a b. (a -> b) -> a -> b
$ LiftedSpec -> HashMap Symbol (MeasureV LHName LocBareTypeLHName ())
liftedCmeasures LiftedSpec
sp)
    , (MeasureV LHName LocBareTypeLHName (Located LHName) -> LHName)
-> [MeasureV LHName LocBareTypeLHName (Located LHName)] -> [LHName]
forall a b. (a -> b) -> [a] -> [b]
map (Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> (MeasureV LHName LocBareTypeLHName (Located LHName)
    -> Located LHName)
-> MeasureV LHName LocBareTypeLHName (Located LHName)
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MeasureV LHName LocBareTypeLHName (Located LHName)
-> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName) (HashSet (MeasureV LHName LocBareTypeLHName (Located LHName))
-> [MeasureV LHName LocBareTypeLHName (Located LHName)]
forall a. HashSet a -> [a]
HS.toList (HashSet (MeasureV LHName LocBareTypeLHName (Located LHName))
 -> [MeasureV LHName LocBareTypeLHName (Located LHName)])
-> HashSet (MeasureV LHName LocBareTypeLHName (Located LHName))
-> [MeasureV LHName LocBareTypeLHName (Located LHName)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec
-> HashSet (MeasureV LHName LocBareTypeLHName (Located LHName))
liftedOmeasures LiftedSpec
sp)
    , ((LHName, BareTypeLHName) -> LHName)
-> [(LHName, BareTypeLHName)] -> [LHName]
forall a b. (a -> b) -> [a] -> [b]
map (LHName, BareTypeLHName) -> LHName
forall a b. (a, b) -> a
fst ([(LHName, BareTypeLHName)] -> [LHName])
-> [(LHName, BareTypeLHName)] -> [LHName]
forall a b. (a -> b) -> a -> b
$ (DataCtorP BareTypeLHName -> [(LHName, BareTypeLHName)])
-> [DataCtorP BareTypeLHName] -> [(LHName, BareTypeLHName)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataCtorP BareTypeLHName -> [(LHName, BareTypeLHName)]
forall ty. DataCtorP ty -> [(LHName, ty)]
DataDecl.dcFields ([DataCtorP BareTypeLHName] -> [(LHName, BareTypeLHName)])
-> [DataCtorP BareTypeLHName] -> [(LHName, BareTypeLHName)]
forall a b. (a -> b) -> a -> b
$ [[DataCtorP BareTypeLHName]] -> [DataCtorP BareTypeLHName]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[DataCtorP BareTypeLHName]] -> [DataCtorP BareTypeLHName])
-> [[DataCtorP BareTypeLHName]] -> [DataCtorP BareTypeLHName]
forall a b. (a -> b) -> a -> b
$
        (DataDeclLHName -> Maybe [DataCtorP BareTypeLHName])
-> [DataDeclLHName] -> [[DataCtorP BareTypeLHName]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe DataDeclLHName -> Maybe [DataCtorP BareTypeLHName]
forall v ty. DataDeclP v ty -> Maybe [DataCtorP ty]
DataDecl.tycDCons ([DataDeclLHName] -> [[DataCtorP BareTypeLHName]])
-> [DataDeclLHName] -> [[DataCtorP BareTypeLHName]]
forall a b. (a -> b) -> a -> b
$
        HashSet DataDeclLHName -> [DataDeclLHName]
forall a. HashSet a -> [a]
HS.toList (HashSet DataDeclLHName -> [DataDeclLHName])
-> HashSet DataDeclLHName -> [DataDeclLHName]
forall a b. (a -> b) -> a -> b
$ LiftedSpec -> HashSet DataDeclLHName
liftedDataDecls LiftedSpec
sp
    , (RTAlias Symbol (ExprV LHName) -> LHName)
-> [RTAlias Symbol (ExprV LHName)] -> [LHName]
forall a b. (a -> b) -> [a] -> [b]
map  (Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> (RTAlias Symbol (ExprV LHName) -> Located LHName)
-> RTAlias Symbol (ExprV LHName)
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias Symbol (ExprV LHName) -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName) ([RTAlias Symbol (ExprV LHName)] -> [LHName])
-> [RTAlias Symbol (ExprV LHName)] -> [LHName]
forall a b. (a -> b) -> a -> b
$ HashSet (RTAlias Symbol (ExprV LHName))
-> [RTAlias Symbol (ExprV LHName)]
forall a. HashSet a -> [a]
HS.toList (HashSet (RTAlias Symbol (ExprV LHName))
 -> [RTAlias Symbol (ExprV LHName)])
-> HashSet (RTAlias Symbol (ExprV LHName))
-> [RTAlias Symbol (ExprV LHName)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec -> HashSet (RTAlias Symbol (ExprV LHName))
liftedEaliases LiftedSpec
sp
    ]

-- | Resolves names in the logic namespace
--
-- Returns the renamed spec.
-- Adds in the monadic state the errors about ambiguous or missing names, and
-- the names of data constructors that are found during renaming.
resolveLogicNames
  :: Config
  -> GHC.Module
  -> InScopeNonReflectedEnv
  -> GHC.GlobalRdrEnv
  -> LogicMap
  -> LocalVars
  -> LogicNameEnv
  -> HS.HashSet LocSymbol
  -> HS.HashSet Symbol
  -> BareSpecParsed
  -> State RenameOutput BareSpecLHName
resolveLogicNames :: Config
-> GenModule Unit
-> InScopeNonReflectedEnv
-> GlobalRdrEnv
-> LogicMap
-> LocalVars
-> LogicNameEnv
-> HashSet LocSymbol
-> HashSet Symbol
-> Spec LocSymbol BareTypeParsed
-> StateT RenameOutput Identity BareSpecLHName
resolveLogicNames Config
cfg GenModule Unit
thisModule InScopeNonReflectedEnv
env GlobalRdrEnv
globalRdrEnv LogicMap
lmap0 LocalVars
localVars LogicNameEnv
lnameEnv HashSet LocSymbol
privateReflectNames HashSet Symbol
depsInlinesAndDefines Spec LocSymbol BareTypeParsed
sp = do
    -- Instance measures must be defined for names of class measures.
    -- The names of class measures should be in @env@
    imeasures <- (MeasureV LocSymbol (Located BareTypeParsed) (Located LHName)
 -> StateT
      RenameOutput
      Identity
      (MeasureV LocSymbol (Located BareTypeParsed) (Located LHName)))
-> [MeasureV LocSymbol (Located BareTypeParsed) (Located LHName)]
-> StateT
     RenameOutput
     Identity
     [MeasureV LocSymbol (Located BareTypeParsed) (Located LHName)]
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 ((Located LHName -> StateT RenameOutput Identity (Located LHName))
-> MeasureV LocSymbol (Located BareTypeParsed) (Located LHName)
-> StateT
     RenameOutput
     Identity
     (MeasureV LocSymbol (Located BareTypeParsed) (Located LHName))
forall (m :: * -> *) v ty ctor.
Monad m =>
(Located LHName -> m (Located LHName))
-> MeasureV v ty ctor -> m (MeasureV v ty ctor)
mapMeasureNamesM Located LHName -> StateT RenameOutput Identity (Located LHName)
resolveIMeasLogicName) (Spec LocSymbol BareTypeParsed
-> [MeasureV LocSymbol (Located BareTypeParsed) (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
imeasures Spec LocSymbol BareTypeParsed
sp)
    emapSpecM
      (bscope cfg)
      (map localVarToSymbol . maybe [] lvdLclEnv . (GHC.lookupNameEnv (lvNames localVars) <=< getLHGHCName))
      resolveLogicName
      (emapBareTypeVM (bscope cfg) resolveLogicName)
      sp {imeasures}
  where
    resolveIMeasLogicName :: Located LHName -> StateT RenameOutput Identity (Located LHName)
resolveIMeasLogicName Located LHName
lx =
      case Located LHName -> LHName
forall a. Located a -> a
val Located LHName
lx of
        LHNUnresolved LHNameSpace
LHLogicName Symbol
s -> (LHName -> Located LHName -> Located LHName
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Located LHName
lx) (LHName -> Located LHName)
-> StateT RenameOutput Identity LHName
-> StateT RenameOutput Identity (Located LHName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> LocSymbol -> StateT RenameOutput Identity LHName
resolveLogicName [] (Symbol
s Symbol -> Located LHName -> LocSymbol
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Located LHName
lx)
        LHName
_ -> Maybe SrcSpan
-> [Char] -> StateT RenameOutput Identity (Located LHName)
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
LH.fSrcSpan Located LHName
lx) ([Char] -> StateT RenameOutput Identity (Located LHName))
-> [Char] -> StateT RenameOutput Identity (Located LHName)
forall a b. (a -> b) -> a -> b
$ [Char]
"unexpected name: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Located LHName -> [Char]
forall a. Show a => a -> [Char]
show Located LHName
lx

    localVarToSymbol :: Var -> Symbol
localVarToSymbol = [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([Char] -> Symbol) -> (Var -> [Char]) -> Var -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> [Char]
GHC.occNameString (OccName -> [Char]) -> (Var -> OccName) -> Var -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> OccName
GHC.nameOccName (Name -> OccName) -> (Var -> Name) -> Var -> OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Name
GHC.varName

    resolveLogicName :: [Symbol] -> LocSymbol -> State RenameOutput LHName
    resolveLogicName :: [Symbol] -> LocSymbol -> StateT RenameOutput Identity LHName
resolveLogicName [Symbol]
ss LocSymbol
ls
        -- The name is local
      | Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Symbol
s [Symbol]
ss = LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ Symbol -> LHName
makeLocalLHName Symbol
s
      | Bool
otherwise =
        case InScopeNonReflectedEnv
-> Symbol -> Either [Symbol] [(GenModule Unit, LHName, ())]
forall a.
InScopeEnv a
-> Symbol -> Either [Symbol] [(GenModule Unit, LHName, a)]
lookupInScopeEnv InScopeNonReflectedEnv
env Symbol
s of
          Left [Symbol]
alts ->
            -- If names are not in the environment, they must be data constructors,
            -- or they must be reflected functions, or they must be in the logicmap.
            case LocSymbol -> Maybe (StateT RenameOutput Identity LHName)
resolveDataConName LocSymbol
ls Maybe (StateT RenameOutput Identity LHName)
-> Maybe (StateT RenameOutput Identity LHName)
-> Maybe (StateT RenameOutput Identity LHName)
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` LogicMap
-> LocSymbol -> Maybe (StateT RenameOutput Identity LHName)
resolveVarName LogicMap
lmap0 LocSymbol
ls of
              Just StateT RenameOutput Identity LHName
m -> StateT RenameOutput Identity LHName
m
              Maybe (StateT RenameOutput Identity LHName)
Nothing
                | Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Symbol
s [Symbol]
wiredInNames ->
                  LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ Symbol -> LHName
makeLocalLHName Symbol
s
                | Bool
otherwise -> do
                    Error -> State RenameOutput ()
addError (Error -> State RenameOutput ()) -> Error -> State RenameOutput ()
forall a b. (a -> b) -> a -> b
$ [Symbol] -> Doc -> [Char] -> LocSymbol -> Error
errResolve [Symbol]
alts Doc
"logic name" [Char]
"Cannot resolve name" LocSymbol
ls
                    LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ Symbol -> LHName
makeLocalLHName Symbol
s
          Right [(GenModule Unit
_, LHName
lhname, ()
_)] -> LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure LHName
lhname
          -- In case of multiple matches, we give precedence to locally defined
          -- logic entities for the user to be able to overwrite them.
          -- TODO: When a mechanism allowing to specify explicitly which logic names
          -- are imported is in place, we should cosider notifying the ambiguity directly.
          Right [(GenModule Unit, LHName, ())]
names ->
            case ((GenModule Unit, LHName, ()) -> Bool)
-> [(GenModule Unit, LHName, ())] -> [(GenModule Unit, LHName, ())]
forall a. (a -> Bool) -> [a] -> [a]
filter ((GenModule Unit -> GenModule Unit -> Bool
forall a. Eq a => a -> a -> Bool
== GenModule Unit
thisModule) (GenModule Unit -> Bool)
-> ((GenModule Unit, LHName, ()) -> GenModule Unit)
-> (GenModule Unit, LHName, ())
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LHName -> GenModule Unit
logicNameOriginModule (LHName -> GenModule Unit)
-> ((GenModule Unit, LHName, ()) -> LHName)
-> (GenModule Unit, LHName, ())
-> GenModule Unit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GenModule Unit, LHName, ()) -> LHName
forall a b c. (a, b, c) -> b
Misc.snd3) [(GenModule Unit, LHName, ())]
names of
              [(GenModule Unit
_, LHName
lhname, ()
_)] -> LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure LHName
lhname
              [(GenModule Unit, LHName, ())]
_ -> do Error -> State RenameOutput ()
addError (Error -> State RenameOutput ()) -> Error -> State RenameOutput ()
forall a b. (a -> b) -> a -> b
$ LocSymbol -> [(GenModule Unit, LHName, ())] -> Error
forall {a} {unit} {c} {t}.
PPrint a =>
Located a -> [(GenModule unit, LHName, c)] -> TError t
errDupInScopeNames LocSymbol
ls [(GenModule Unit, LHName, ())]
names
                      LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ Symbol -> LHName
makeLocalLHName Symbol
s
      where
        s :: Symbol
s = LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
ls
        wiredInNames :: [Symbol]
wiredInNames =
           ((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst [(Symbol, Sort)]
wiredSortedSyms [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++
           ((LHName, SpecType) -> Symbol) -> [(LHName, SpecType)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (LHName -> Symbol
lhNameToResolvedSymbol (LHName -> Symbol)
-> ((LHName, SpecType) -> LHName) -> (LHName, SpecType) -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LHName, SpecType) -> LHName
forall a b. (a, b) -> a
fst) ((Located DataConP -> [(LHName, SpecType)])
-> [Located DataConP] -> [(LHName, SpecType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DataConP -> [(LHName, SpecType)]
DataDecl.dcpTyArgs (DataConP -> [(LHName, SpecType)])
-> (Located DataConP -> DataConP)
-> Located DataConP
-> [(LHName, SpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located DataConP -> DataConP
forall a. Located a -> a
val) [Located DataConP]
wiredDataCons)
        errDupInScopeNames :: Located a -> [(GenModule unit, LHName, c)] -> TError t
errDupInScopeNames Located a
locSym [(GenModule unit, LHName, c)]
inScopeNames =
          SrcSpan -> Doc -> Doc -> [Doc] -> TError t
forall t. SrcSpan -> Doc -> Doc -> [Doc] -> TError t
ErrDupNames
            (Located a -> SrcSpan
forall a. Loc a => a -> SrcSpan
LH.fSrcSpan Located a
locSym)
            Doc
"non-reflected logic entity"
            (a -> Doc
forall a. PPrint a => a -> Doc
pprint (Located a -> a
forall a. Located a -> a
val Located a
locSym))
            [ Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (LHName -> Symbol
lhNameToResolvedSymbol LHName
n) Doc -> Doc -> Doc
PJ.<+>
              [Char] -> Doc
PJ.text
                ([Char]
"imported from " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ModuleName -> [Char]
GHC.moduleNameString (GenModule unit -> ModuleName
forall unit. GenModule unit -> ModuleName
GHC.moduleName GenModule unit
m))
            | (GenModule unit
m, LHName
n, c
_) <- [(GenModule unit, LHName, c)]
inScopeNames
            ]

    resolveDataConName :: LocSymbol -> Maybe (StateT RenameOutput Identity LHName)
resolveDataConName LocSymbol
ls
      | Symbol
unqualifiedS Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
":" = StateT RenameOutput Identity LHName
-> Maybe (StateT RenameOutput Identity LHName)
forall a. a -> Maybe a
Just (StateT RenameOutput Identity LHName
 -> Maybe (StateT RenameOutput Identity LHName))
-> StateT RenameOutput Identity LHName
-> Maybe (StateT RenameOutput Identity LHName)
forall a b. (a -> b) -> a -> b
$
        LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ Symbol -> GenModule Unit -> Maybe Name -> LHName
makeLogicLHName Symbol
unqualifiedS (HasDebugCallStack => Name -> GenModule Unit
Name -> GenModule Unit
GHC.nameModule Name
consDataConName) (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
consDataConName)
      | Symbol
unqualifiedS Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"[]" = StateT RenameOutput Identity LHName
-> Maybe (StateT RenameOutput Identity LHName)
forall a. a -> Maybe a
Just (StateT RenameOutput Identity LHName
 -> Maybe (StateT RenameOutput Identity LHName))
-> StateT RenameOutput Identity LHName
-> Maybe (StateT RenameOutput Identity LHName)
forall a b. (a -> b) -> a -> b
$
        LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ Symbol -> GenModule Unit -> Maybe Name -> LHName
makeLogicLHName Symbol
unqualifiedS (HasDebugCallStack => Name -> GenModule Unit
Name -> GenModule Unit
GHC.nameModule Name
nilDataConName) (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
nilDataConName)
      | Just Int
arity <- Text -> Maybe Int
isTupleDC (Symbol -> Text
symbolText Symbol
s) = StateT RenameOutput Identity LHName
-> Maybe (StateT RenameOutput Identity LHName)
forall a. a -> Maybe a
Just (StateT RenameOutput Identity LHName
 -> Maybe (StateT RenameOutput Identity LHName))
-> StateT RenameOutput Identity LHName
-> Maybe (StateT RenameOutput Identity LHName)
forall a b. (a -> b) -> a -> b
$
          let dcName :: Name
dcName = Int -> Name
tupleDataConName Int
arity
           in LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ Symbol -> GenModule Unit -> Maybe Name -> LHName
makeLogicLHName Symbol
s (HasDebugCallStack => Name -> GenModule Unit
Name -> GenModule Unit
GHC.nameModule Name
dcName) (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
dcName)
      where
        unqualifiedS :: Symbol
unqualifiedS = Symbol -> Symbol
LH.dropModuleNames Symbol
s
        nilDataConName :: Name
nilDataConName = Var -> Name
forall a. NamedThing a => a -> Name
GHC.getName (Var -> Name) -> Var -> Name
forall a b. (a -> b) -> a -> b
$ DataCon -> Var
GHC.dataConWorkId DataCon
GHC.nilDataCon
        consDataConName :: Name
consDataConName = Var -> Name
forall a. NamedThing a => a -> Name
GHC.getName (Var -> Name) -> Var -> Name
forall a b. (a -> b) -> a -> b
$ DataCon -> Var
GHC.dataConWorkId DataCon
GHC.consDataCon
        tupleDataConName :: Int -> Name
tupleDataConName = Var -> Name
forall a. NamedThing a => a -> Name
GHC.getName (Var -> Name) -> (Int -> Var) -> Int -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> Var
GHC.dataConWorkId (DataCon -> Var) -> (Int -> DataCon) -> Int -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Boxity -> Int -> DataCon
GHC.tupleDataCon Boxity
GHC.Boxed
        s :: Symbol
s = LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
ls
        isTupleDC :: Text -> Maybe Int
isTupleDC Text
t
          | Text -> Text -> Bool
Text.isPrefixOf Text
"(" Text
t Bool -> Bool -> Bool
&& Text -> Text -> Bool
Text.isSuffixOf Text
")" Text
t Bool -> Bool -> Bool
&&
            (Char -> Bool) -> Text -> Bool
Text.all (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
',') (HasCallStack => Text -> Text
Text -> Text
Text.init (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ HasCallStack => Text -> Text
Text -> Text
Text.tail Text
t)
          = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Text -> Int
Text.length Text
t Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2
          | Bool
otherwise
          = Maybe Int
forall a. Maybe a
Nothing
    resolveDataConName LocSymbol
s =
      case GlobalRdrEnv -> LookupGRE GREInfo -> [GlobalRdrEltX GREInfo]
forall info.
GlobalRdrEnvX info -> LookupGRE info -> [GlobalRdrEltX info]
GHC.lookupGRE GlobalRdrEnv
globalRdrEnv (LHNameSpace -> Symbol -> LookupGRE GREInfo
mkLookupGRE (LHThisModuleNameFlag -> LHNameSpace
LHDataConName LHThisModuleNameFlag
LHAnyModuleNameF) (Symbol -> LookupGRE GREInfo) -> Symbol -> LookupGRE GREInfo
forall a b. (a -> b) -> a -> b
$ LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
s) of
        [GlobalRdrEltX GREInfo
e] -> do
          let n :: Name
n = GlobalRdrEltX GREInfo -> Name
forall info. GlobalRdrEltX info -> Name
GHC.greName GlobalRdrEltX GREInfo
e
          StateT RenameOutput Identity LHName
-> Maybe (StateT RenameOutput Identity LHName)
forall a. a -> Maybe a
Just (StateT RenameOutput Identity LHName
 -> Maybe (StateT RenameOutput Identity LHName))
-> StateT RenameOutput Identity LHName
-> Maybe (StateT RenameOutput Identity LHName)
forall a b. (a -> b) -> a -> b
$ do
            let lhName :: LHName
lhName = Symbol -> GenModule Unit -> Maybe Name -> LHName
makeLogicLHName ([Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol ([Char] -> Symbol) -> [Char] -> Symbol
forall a b. (a -> b) -> a -> b
$ Name -> [Char]
forall a. NamedThing a => a -> [Char]
GHC.getOccString Name
n) (HasDebugCallStack => Name -> GenModule Unit
Name -> GenModule Unit
GHC.nameModule Name
n) (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n)
            LHName -> State RenameOutput ()
addName LHName
lhName
            LHName -> State RenameOutput ()
addDataConsName LHName
lhName
            LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return LHName
lhName
        [] ->
          Maybe (StateT RenameOutput Identity LHName)
forall a. Maybe a
Nothing
        [GlobalRdrEltX GREInfo]
es ->
          StateT RenameOutput Identity LHName
-> Maybe (StateT RenameOutput Identity LHName)
forall a. a -> Maybe a
Just (StateT RenameOutput Identity LHName
 -> Maybe (StateT RenameOutput Identity LHName))
-> StateT RenameOutput Identity LHName
-> Maybe (StateT RenameOutput Identity LHName)
forall a b. (a -> b) -> a -> b
$ do
            Error -> State RenameOutput ()
addError
              (SrcSpan -> Doc -> Doc -> [Doc] -> Error
forall t. SrcSpan -> Doc -> Doc -> [Doc] -> TError t
ErrDupNames
                 (LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
LH.fSrcSpan LocSymbol
s)
                 Doc
"data constructor"
                 (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (Symbol -> Doc) -> Symbol -> Doc
forall a b. (a -> b) -> a -> b
$ LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
s)
                 ((GlobalRdrEltX GREInfo -> Doc) -> [GlobalRdrEltX GREInfo] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Doc
PJ.text ([Char] -> Doc)
-> (GlobalRdrEltX GREInfo -> [Char])
-> GlobalRdrEltX GREInfo
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalRdrEltX GREInfo -> [Char]
forall a. Outputable a => a -> [Char]
GHC.showPprUnsafe) [GlobalRdrEltX GREInfo]
es)
              )
            LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ Symbol -> LHName
makeLocalLHName (Symbol -> LHName) -> Symbol -> LHName
forall a b. (a -> b) -> a -> b
$ LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
s

    -- Resolves names of reflected functions or names in the logic map
    --
    -- Names of reflected functions are resolved here because, to be in scope,
    -- we ask the corresponding Haskell name to be in scope. In contrast, the
    -- @InScopeNonReflectedEnv@ indicates where the reflect annotations were
    -- imported from, but not where the Haskell names were imported from.
    resolveVarName :: LogicMap
-> LocSymbol -> Maybe (StateT RenameOutput Identity LHName)
resolveVarName LogicMap
lmap LocSymbol
s = do
      let gres :: [GlobalRdrEltX GREInfo]
gres =
            GlobalRdrEnv -> LookupGRE GREInfo -> [GlobalRdrEltX GREInfo]
forall info.
GlobalRdrEnvX info -> LookupGRE info -> [GlobalRdrEltX info]
GHC.lookupGRE GlobalRdrEnv
globalRdrEnv (LookupGRE GREInfo -> [GlobalRdrEltX GREInfo])
-> LookupGRE GREInfo -> [GlobalRdrEltX GREInfo]
forall a b. (a -> b) -> a -> b
$
            LHNameSpace -> Symbol -> LookupGRE GREInfo
mkLookupGRE (LHThisModuleNameFlag -> LHNameSpace
LHVarName LHThisModuleNameFlag
LHAnyModuleNameF) (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
s)
          refls :: [LHName]
refls = (GlobalRdrEltX GREInfo -> Maybe LHName)
-> [GlobalRdrEltX GREInfo] -> [LHName]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Name -> Maybe LHName
findReflection (Name -> Maybe LHName)
-> (GlobalRdrEltX GREInfo -> Name)
-> GlobalRdrEltX GREInfo
-> Maybe LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalRdrEltX GREInfo -> Name
forall info. GlobalRdrEltX info -> Name
GHC.greName) [GlobalRdrEltX GREInfo]
gres
      case [LHName]
refls of
        [LHName
lhName] -> StateT RenameOutput Identity LHName
-> Maybe (StateT RenameOutput Identity LHName)
forall a. a -> Maybe a
Just (StateT RenameOutput Identity LHName
 -> Maybe (StateT RenameOutput Identity LHName))
-> StateT RenameOutput Identity LHName
-> Maybe (StateT RenameOutput Identity LHName)
forall a b. (a -> b) -> a -> b
$ LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return LHName
lhName
        [LHName]
_ | LocSymbol -> HashSet LocSymbol -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
HS.member LocSymbol
s HashSet LocSymbol
privateReflectNames
          -> StateT RenameOutput Identity LHName
-> Maybe (StateT RenameOutput Identity LHName)
forall a. a -> Maybe a
Just (StateT RenameOutput Identity LHName
 -> Maybe (StateT RenameOutput Identity LHName))
-> StateT RenameOutput Identity LHName
-> Maybe (StateT RenameOutput Identity LHName)
forall a b. (a -> b) -> a -> b
$ LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ Symbol -> LHName
makeLocalLHName (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
s)
          | Bool
otherwise
          -> case [GlobalRdrEltX GREInfo]
gres of
          [GlobalRdrEltX GREInfo
e] -> do
            let n :: Name
n = GlobalRdrEltX GREInfo -> Name
forall info. GlobalRdrEltX info -> Name
GHC.greName GlobalRdrEltX GREInfo
e
            -- See [NOTE:EXPRESSION-ALIASES]
            if Symbol -> HashMap Symbol LMap -> Bool
forall k a. Hashable k => k -> HashMap k a -> Bool
HM.member (Name -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Name
n) (LogicMap -> HashMap Symbol LMap
lmSymDefs LogicMap
lmap) Bool -> Bool -> Bool
|| Symbol -> HashSet Symbol -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
HS.member (Name -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Name
n) HashSet Symbol
depsInlinesAndDefines then
              StateT RenameOutput Identity LHName
-> Maybe (StateT RenameOutput Identity LHName)
forall a. a -> Maybe a
Just (StateT RenameOutput Identity LHName
 -> Maybe (StateT RenameOutput Identity LHName))
-> StateT RenameOutput Identity LHName
-> Maybe (StateT RenameOutput Identity LHName)
forall a b. (a -> b) -> a -> b
$ do
                let lhName :: LHName
lhName = Symbol -> GenModule Unit -> Maybe Name -> LHName
makeLogicLHName ([Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol ([Char] -> Symbol) -> [Char] -> Symbol
forall a b. (a -> b) -> a -> b
$ Name -> [Char]
forall a. NamedThing a => a -> [Char]
GHC.getOccString Name
n) (HasDebugCallStack => Name -> GenModule Unit
Name -> GenModule Unit
GHC.nameModule Name
n) Maybe Name
forall a. Maybe a
Nothing
                LHName -> State RenameOutput ()
addName LHName
lhName
                LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return LHName
lhName
            else
              Maybe (StateT RenameOutput Identity LHName)
forall a. Maybe a
Nothing
          [] ->
            Maybe (StateT RenameOutput Identity LHName)
forall a. Maybe a
Nothing
          [GlobalRdrEltX GREInfo]
es ->
            StateT RenameOutput Identity LHName
-> Maybe (StateT RenameOutput Identity LHName)
forall a. a -> Maybe a
Just (StateT RenameOutput Identity LHName
 -> Maybe (StateT RenameOutput Identity LHName))
-> StateT RenameOutput Identity LHName
-> Maybe (StateT RenameOutput Identity LHName)
forall a b. (a -> b) -> a -> b
$ do
              Error -> State RenameOutput ()
addError
                 (SrcSpan -> Doc -> Doc -> [Doc] -> Error
forall t. SrcSpan -> Doc -> Doc -> [Doc] -> TError t
ErrDupNames
                   (LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
LH.fSrcSpan LocSymbol
s)
                   Doc
"variable"
                   (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (Symbol -> Doc) -> Symbol -> Doc
forall a b. (a -> b) -> a -> b
$ LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
s)
                   ((GlobalRdrEltX GREInfo -> Doc) -> [GlobalRdrEltX GREInfo] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Doc
PJ.text ([Char] -> Doc)
-> (GlobalRdrEltX GREInfo -> [Char])
-> GlobalRdrEltX GREInfo
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalRdrEltX GREInfo -> [Char]
forall a. Outputable a => a -> [Char]
GHC.showPprUnsafe) [GlobalRdrEltX GREInfo]
es)
                 )
              LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (LHName -> StateT RenameOutput Identity LHName)
-> LHName -> StateT RenameOutput Identity LHName
forall a b. (a -> b) -> a -> b
$ Symbol -> LHName
makeLocalLHName (Symbol -> LHName) -> Symbol -> LHName
forall a b. (a -> b) -> a -> b
$ LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
s

    findReflection :: GHC.Name -> Maybe LHName
    findReflection :: Name -> Maybe LHName
findReflection Name
n = NameEnv LHName -> Name -> Maybe LHName
forall a. NameEnv a -> Name -> Maybe a
GHC.lookupNameEnv (LogicNameEnv -> NameEnv LHName
lneReflected LogicNameEnv
lnameEnv) Name
n

mapMeasureNamesM :: Monad m => (Located LHName -> m (Located LHName)) -> MeasureV v ty ctor -> m (MeasureV v ty ctor)
mapMeasureNamesM :: forall (m :: * -> *) v ty ctor.
Monad m =>
(Located LHName -> m (Located LHName))
-> MeasureV v ty ctor -> m (MeasureV v ty ctor)
mapMeasureNamesM Located LHName -> m (Located LHName)
f MeasureV v ty ctor
m = do
    msName <- Located LHName -> m (Located LHName)
f (MeasureV v ty ctor -> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName MeasureV v ty ctor
m)
    msEqns <- mapM mapDefNameM (msEqns m)
    return m {msName, msEqns}
  where
    mapDefNameM :: DefV v ty ctor -> m (DefV v ty ctor)
mapDefNameM DefV v ty ctor
d = do
      measure <- Located LHName -> m (Located LHName)
f (DefV v ty ctor -> Located LHName
forall v ty ctor. DefV v ty ctor -> Located LHName
measure DefV v ty ctor
d)
      return d {measure}

mapDataDeclFieldNamesM :: Monad m => (LHName -> m LHName) -> DataDecl.DataDeclP v ty -> m (DataDecl.DataDeclP v ty)
mapDataDeclFieldNamesM :: forall (m :: * -> *) v ty.
Monad m =>
(LHName -> m LHName) -> DataDeclP v ty -> m (DataDeclP v ty)
mapDataDeclFieldNamesM LHName -> m LHName
f DataDeclP v ty
d = do
    tycDCons <- ([DataCtorP ty] -> m [DataCtorP ty])
-> Maybe [DataCtorP ty] -> m (Maybe [DataCtorP ty])
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) -> Maybe a -> f (Maybe b)
traverse ((DataCtorP ty -> m (DataCtorP ty))
-> [DataCtorP ty] -> m [DataCtorP ty]
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 ((LHName -> m LHName) -> DataCtorP ty -> m (DataCtorP ty)
forall (m :: * -> *) ty.
Monad m =>
(LHName -> m LHName) -> DataCtorP ty -> m (DataCtorP ty)
mapDataCtorFieldsM LHName -> m LHName
f)) (DataDeclP v ty -> Maybe [DataCtorP ty]
forall v ty. DataDeclP v ty -> Maybe [DataCtorP ty]
DataDecl.tycDCons DataDeclP v ty
d)
    return d{DataDecl.tycDCons}
  where
    mapDataCtorFieldsM :: Monad m => (LHName -> m LHName) -> DataDecl.DataCtorP ty -> m (DataDecl.DataCtorP ty)
    mapDataCtorFieldsM :: forall (m :: * -> *) ty.
Monad m =>
(LHName -> m LHName) -> DataCtorP ty -> m (DataCtorP ty)
mapDataCtorFieldsM LHName -> m LHName
f1 DataCtorP ty
c = do
      dcFields <- ((LHName, ty) -> m (LHName, ty))
-> [(LHName, ty)] -> m [(LHName, ty)]
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 (\(LHName
n, ty
t) -> (, ty
t) (LHName -> (LHName, ty)) -> m LHName -> m (LHName, ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LHName -> m LHName
f1 LHName
n) (DataCtorP ty -> [(LHName, ty)]
forall ty. DataCtorP ty -> [(LHName, ty)]
DataDecl.dcFields DataCtorP ty
c)
      return c{DataDecl.dcFields}

toBareSpecLHName :: Config -> LogicNameEnv -> BareSpec -> BareSpecLHName
toBareSpecLHName :: Config -> LogicNameEnv -> BareSpec -> BareSpecLHName
toBareSpecLHName Config
cfg LogicNameEnv
lenv BareSpec
sp0 = Identity BareSpecLHName -> BareSpecLHName
forall a. Identity a -> a
runIdentity (Identity BareSpecLHName -> BareSpecLHName)
-> Identity BareSpecLHName -> BareSpecLHName
forall a b. (a -> b) -> a -> b
$ BareSpec -> Identity BareSpecLHName
go BareSpec
sp0
  where
    -- This is implemented with a monadic traversal to reuse the logic
    -- that collects the local symbols in scope.
    go :: BareSpec -> Identity BareSpecLHName
    go :: BareSpec -> Identity BareSpecLHName
go BareSpec
sp =
      Bool
-> (LHName -> [Symbol])
-> ([Symbol] -> Symbol -> Identity LHName)
-> ([Symbol] -> BareType -> Identity BareTypeLHName)
-> BareSpec
-> Identity BareSpecLHName
forall (m :: * -> *) lname0 lname1 ty0 ty1.
(Monad m, Ord lname0) =>
Bool
-> (LHName -> [Symbol])
-> ([Symbol] -> lname0 -> m lname1)
-> ([Symbol] -> ty0 -> m ty1)
-> Spec lname0 ty0
-> m (Spec lname1 ty1)
emapSpecM
        (Config -> Bool
bscope Config
cfg)
        ([Symbol] -> LHName -> [Symbol]
forall a b. a -> b -> a
const [])
        [Symbol] -> Symbol -> Identity LHName
symToLHName
        (Bool
-> ([Symbol] -> Symbol -> Identity LHName)
-> [Symbol]
-> BareType
-> Identity BareTypeLHName
forall (m :: * -> *) v1 v2.
(Monad m, Ord v1) =>
Bool
-> ([Symbol] -> v1 -> m v2)
-> [Symbol]
-> BareTypeV v1
-> m (BareTypeV v2)
emapBareTypeVM (Config -> Bool
bscope Config
cfg) [Symbol] -> Symbol -> Identity LHName
symToLHName)
        BareSpec
sp

    symToLHName :: [Symbol] -> Symbol -> Identity LHName
symToLHName = [Char]
-> LogicNameEnv
-> HashSet Symbol
-> [Symbol]
-> Symbol
-> Identity LHName
symbolToLHName [Char]
"toBareSpecLHName" LogicNameEnv
lenv HashSet Symbol
unhandledNames

    unhandledNames :: HashSet Symbol
unhandledNames = [Symbol] -> HashSet Symbol
forall a. Hashable a => [a] -> HashSet a
HS.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ ((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst ([(Symbol, Sort)] -> [Symbol]) -> [(Symbol, Sort)] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ BareSpec -> [(Symbol, Sort)]
forall lname ty. Spec lname ty -> [(lname, Sort)]
expSigs BareSpec
sp0

-- | Uses the logic name environment to convert a resolved 'Symbol' to 'LHName'.
-- Symbols not present in the environment correspond to local symbols (e.g.
-- bounded variables) or are explicitly left unhandled.
symbolToLHName :: String -> LogicNameEnv -> HS.HashSet Symbol -> [Symbol] -> Symbol -> Identity LHName
symbolToLHName :: [Char]
-> LogicNameEnv
-> HashSet Symbol
-> [Symbol]
-> Symbol
-> Identity LHName
symbolToLHName [Char]
caller LogicNameEnv
lenv HashSet Symbol
unhandledNames [Symbol]
ss Symbol
s
  | Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Symbol
s [Symbol]
ss = LHName -> Identity LHName
forall a. a -> Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (LHName -> Identity LHName) -> LHName -> Identity LHName
forall a b. (a -> b) -> a -> b
$ Symbol -> LHName
makeLocalLHName Symbol
s
  | Bool
otherwise =
    case Symbol -> SEnv LHName -> Maybe LHName
forall b a. Hashable b => b -> SEnvB b a -> Maybe a
lookupSEnv Symbol
s (LogicNameEnv -> SEnv LHName
lneLHName LogicNameEnv
lenv) of
      Maybe LHName
Nothing -> do
        Bool -> Identity () -> Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Symbol -> HashSet Symbol -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
HS.member Symbol
s HashSet Symbol
unhandledNames) (Identity () -> Identity ()) -> Identity () -> Identity ()
forall a b. (a -> b) -> a -> b
$
          Maybe SrcSpan -> [Char] -> Identity ()
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char] -> Identity ()) -> [Char] -> Identity ()
forall a b. (a -> b) -> a -> b
$ [Char]
caller [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": cannot find " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show Symbol
s
        LHName -> Identity LHName
forall a. a -> Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (LHName -> Identity LHName) -> LHName -> Identity LHName
forall a b. (a -> b) -> a -> b
$ Symbol -> LHName
makeLocalLHName Symbol
s
      Just LHName
lhname -> LHName -> Identity LHName
forall a. a -> Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return LHName
lhname