-- | 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 refinment 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'. At
--   the moment most LHNames are just wrappers over the symbols. As name
--   resolution is implemented for logic names, the wrappers will be
--   replaced with the actual result of name resolution.
--
-- 'BareSpecLHName' has a 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.
--
-- 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
  , 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 ((<=<), mplus, unless, void)
import           Control.Monad.Identity
import           Control.Monad.State.Strict
import           Data.Bifunctor (first)
import qualified Data.Char                               as Char
import           Data.Coerce (coerce)
import           Data.Data (Data, gmapT)
import           Data.Generics (extT)


import qualified Data.HashSet                            as HS
import qualified Data.HashMap.Strict                     as HM
import           Data.List (find, isSuffixOf, nubBy)
import           Data.List.Extra (dropEnd)
import           Data.Maybe (fromMaybe, listToMaybe, 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.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.
--
-- It doesn't matter at the moment in which module a type alias is defined.
-- Type alias names cannot be qualified at the moment, and therefore their
-- names identify them uniquely.
collectTypeAliases
  :: GHC.Module
  -> BareSpecParsed
  -> TargetDependencies
  -> HM.HashMap Symbol (GHC.Module, RTAlias Symbol ())
collectTypeAliases :: Module
-> BareSpecParsed
-> TargetDependencies
-> HashMap Symbol (Module, RTAlias Symbol ())
collectTypeAliases Module
m BareSpecParsed
spec TargetDependencies
deps =
    let bsAliases :: [(Symbol, (Module, RTAlias Symbol ()))]
bsAliases = [ (RTAlias Symbol (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
-> Symbol
forall x a. RTAlias x a -> Symbol
rtName RTAlias Symbol (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
a, (Module
m, RTAlias Symbol (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
-> RTAlias Symbol ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void RTAlias Symbol (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
a)) | RTAlias Symbol (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
a <- (Located
   (RTAlias
      Symbol (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))
 -> RTAlias
      Symbol (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))
-> [Located
      (RTAlias
         Symbol (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))]
-> [RTAlias
      Symbol (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
forall a b. (a -> b) -> [a] -> [b]
map Located
  (RTAlias
     Symbol (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))
-> RTAlias
     Symbol (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
forall a. Located a -> a
val (BareSpecParsed
-> [Located
      (RTAlias
         Symbol (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))]
forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (BareTypeV lname))]
aliases BareSpecParsed
spec) ]
        depAliases :: [(Symbol, (Module, RTAlias Symbol ()))]
depAliases =
          [ (RTAlias Symbol BareTypeLHName -> Symbol
forall x a. RTAlias x a -> Symbol
rtName RTAlias Symbol BareTypeLHName
a, (StableModule -> Module
GHC.unStableModule StableModule
sm, RTAlias Symbol BareTypeLHName -> RTAlias Symbol ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void RTAlias Symbol BareTypeLHName
a))
          | (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)
          , RTAlias Symbol BareTypeLHName
a <- (Located (RTAlias Symbol BareTypeLHName)
 -> RTAlias Symbol BareTypeLHName)
-> [Located (RTAlias Symbol BareTypeLHName)]
-> [RTAlias Symbol BareTypeLHName]
forall a b. (a -> b) -> [a] -> [b]
map Located (RTAlias Symbol BareTypeLHName)
-> RTAlias Symbol BareTypeLHName
forall a. Located a -> a
val (HashSet (Located (RTAlias Symbol BareTypeLHName))
-> [Located (RTAlias Symbol BareTypeLHName)]
forall a. HashSet a -> [a]
HS.toList (HashSet (Located (RTAlias Symbol BareTypeLHName))
 -> [Located (RTAlias Symbol BareTypeLHName)])
-> HashSet (Located (RTAlias Symbol BareTypeLHName))
-> [Located (RTAlias Symbol BareTypeLHName)]
forall a b. (a -> b) -> a -> b
$ LiftedSpec -> HashSet (Located (RTAlias Symbol BareTypeLHName))
liftedAliases LiftedSpec
lspec)
          ]
     in
        [(Symbol, (Module, RTAlias Symbol ()))]
-> HashMap Symbol (Module, RTAlias Symbol ())
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HM.fromList ([(Symbol, (Module, RTAlias Symbol ()))]
 -> HashMap Symbol (Module, RTAlias Symbol ()))
-> [(Symbol, (Module, RTAlias Symbol ()))]
-> HashMap Symbol (Module, RTAlias Symbol ())
forall a b. (a -> b) -> a -> b
$ [(Symbol, (Module, RTAlias Symbol ()))]
bsAliases [(Symbol, (Module, RTAlias Symbol ()))]
-> [(Symbol, (Module, RTAlias Symbol ()))]
-> [(Symbol, (Module, RTAlias Symbol ()))]
forall a. [a] -> [a] -> [a]
++ [(Symbol, (Module, RTAlias Symbol ()))]
depAliases

collectExprAliases
  :: BareSpecParsed
  -> TargetDependencies
  -> HS.HashSet Symbol
collectExprAliases :: BareSpecParsed -> TargetDependencies -> HashSet Symbol
collectExprAliases BareSpecParsed
spec TargetDependencies
deps =
    let bsAliases :: HashSet Symbol
bsAliases = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
HS.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ (Located (RTAlias Symbol (ExprV LocSymbol)) -> Symbol)
-> [Located (RTAlias Symbol (ExprV LocSymbol))] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (RTAlias Symbol (ExprV LocSymbol) -> Symbol
forall x a. RTAlias x a -> Symbol
rtName (RTAlias Symbol (ExprV LocSymbol) -> Symbol)
-> (Located (RTAlias Symbol (ExprV LocSymbol))
    -> RTAlias Symbol (ExprV LocSymbol))
-> Located (RTAlias Symbol (ExprV LocSymbol))
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (RTAlias Symbol (ExprV LocSymbol))
-> RTAlias Symbol (ExprV LocSymbol)
forall a. Located a -> a
val) (BareSpecParsed -> [Located (RTAlias Symbol (ExprV LocSymbol))]
forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (ExprV lname))]
ealiases BareSpecParsed
spec)
        depAliases :: [HashSet Symbol]
depAliases =
          [ (Located (RTAlias Symbol (ExprV LHName)) -> Symbol)
-> HashSet (Located (RTAlias Symbol (ExprV LHName)))
-> HashSet Symbol
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
HS.map (RTAlias Symbol (ExprV LHName) -> Symbol
forall x a. RTAlias x a -> Symbol
rtName (RTAlias Symbol (ExprV LHName) -> Symbol)
-> (Located (RTAlias Symbol (ExprV LHName))
    -> RTAlias Symbol (ExprV LHName))
-> Located (RTAlias Symbol (ExprV LHName))
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (RTAlias Symbol (ExprV LHName))
-> RTAlias Symbol (ExprV LHName)
forall a. Located a -> a
val) (HashSet (Located (RTAlias Symbol (ExprV LHName)))
 -> HashSet Symbol)
-> HashSet (Located (RTAlias Symbol (ExprV LHName)))
-> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ LiftedSpec -> HashSet (Located (RTAlias Symbol (ExprV LHName)))
liftedEaliases LiftedSpec
lspec
          | (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)
          ]
     in
        [HashSet Symbol] -> HashSet Symbol
forall a. Eq a => [HashSet a] -> HashSet a
HS.unions ([HashSet Symbol] -> HashSet Symbol)
-> [HashSet Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ HashSet Symbol
bsAliases HashSet Symbol -> [HashSet Symbol] -> [HashSet Symbol]
forall a. a -> [a] -> [a]
: [HashSet Symbol]
depAliases

-- | 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
-> Module
-> LocalVars
-> ImportedMods
-> GlobalRdrEnv
-> BareSpecParsed
-> TargetDependencies
-> Either [Error] (BareSpec, LogicNameEnv, LogicMap)
resolveLHNames Config
cfg Module
thisModule LocalVars
localVars ImportedMods
impMods GlobalRdrEnv
globalRdrEnv BareSpecParsed
bareSpec0 TargetDependencies
dependencies = do
    let ((BareSpec
bs, LogicNameEnv
logicNameEnv, LogicMap
lmap2), RenameOutput
ro) =
          (State RenameOutput (BareSpec, LogicNameEnv, LogicMap)
 -> RenameOutput
 -> ((BareSpec, LogicNameEnv, LogicMap), RenameOutput))
-> RenameOutput
-> State RenameOutput (BareSpec, LogicNameEnv, LogicMap)
-> ((BareSpec, LogicNameEnv, LogicMap), RenameOutput)
forall a b c. (a -> b -> c) -> b -> a -> c
flip State RenameOutput (BareSpec, LogicNameEnv, LogicMap)
-> RenameOutput
-> ((BareSpec, LogicNameEnv, LogicMap), RenameOutput)
forall s a. State s a -> s -> (a, s)
runState RenameOutput {roErrors :: [Error]
roErrors = [], roUsedNames :: [LHName]
roUsedNames = [], roUsedDataCons :: HashSet LHName
roUsedDataCons = HashSet LHName
forall a. Monoid a => a
mempty} (State RenameOutput (BareSpec, LogicNameEnv, LogicMap)
 -> ((BareSpec, LogicNameEnv, LogicMap), RenameOutput))
-> State RenameOutput (BareSpec, LogicNameEnv, LogicMap)
-> ((BareSpec, LogicNameEnv, LogicMap), RenameOutput)
forall a b. (a -> b) -> a -> b
$ do
            -- A generic traversal that resolves names of Haskell entities
            sp1 <- (Located LHName -> StateT RenameOutput Identity (Located LHName))
-> BareSpecParsed -> StateT RenameOutput Identity BareSpecParsed
forall (m :: * -> *) a.
(Data a, Monad m) =>
(Located LHName -> m (Located LHName)) -> a -> m a
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) (BareSpecParsed -> StateT RenameOutput Identity BareSpecParsed)
-> BareSpecParsed -> StateT RenameOutput Identity BareSpecParsed
forall a b. (a -> b) -> a -> b
$
                     HashMap Symbol (Module, RTAlias Symbol ())
-> BareSpecParsed -> BareSpecParsed
fixExpressionArgsOfTypeAliases HashMap Symbol (Module, RTAlias Symbol ())
taliases BareSpecParsed
bareSpec0
            -- Data decls contain fieldnames that introduce measures with the
            -- same names. We resolved them before constructing the logic
            -- environment.
            dataDecls <- mapM (mapDataDeclFieldNamesM resolveFieldLogicName) (dataDecls sp1)
            let sp2 = BareSpecParsed
sp1 {dataDecls}

            es0 <- gets roErrors
            if null es0 then do

              -- Now we do a second traversal to resolve logic names
              let (inScopeEnv, logicNameEnv0, privateReflectNames, unhandledNames) =
                    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. (Eq k, 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
$
                                         (\(Located LHName
k , LMapV LocSymbol
v) ->
                                             let k' :: LocSymbol
k' = LHName -> Symbol
lhNameToResolvedSymbol (LHName -> Symbol) -> Located LHName -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located LHName
k in
                                             (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
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 = k' }))
                                         ((Located LHName, LMapV LocSymbol) -> (Symbol, LMap))
-> [(Located LHName, LMapV LocSymbol)] -> [(Symbol, LMap)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpecParsed -> [(Located LHName, LMapV LocSymbol)]
forall lname ty. Spec lname ty -> [(Located LHName, LMapV lname)]
defines BareSpecParsed
sp2)
              sp3 <- fromBareSpecLHName <$>
                       resolveLogicNames
                         cfg
                         inScopeEnv
                         globalRdrEnv
                         unhandledNames
                         lmap1
                         localVars
                         logicNameEnv0
                         privateReflectNames
                         allEaliases
                         sp2
              dcs <- gets roUsedDataCons
              return (sp3 {usedDataCons = dcs} , logicNameEnv0, lmap1)
            else
              return ( error "resolveLHNames: invalid spec"
                     , error "resolveLHNames: invalid logic environment"
                     , error "resolveLHNames: invalid logic map")
        logicNameEnv' :: LogicNameEnv
logicNameEnv' = LogicNameEnv -> [LHName] -> LogicNameEnv
extendLogicNameEnv LogicNameEnv
logicNameEnv (RenameOutput -> [LHName]
roUsedNames RenameOutput
ro)
    if [Error] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (RenameOutput -> [Error]
roErrors RenameOutput
ro) then
      (BareSpec, LogicNameEnv, LogicMap)
-> Either [Error] (BareSpec, LogicNameEnv, LogicMap)
forall a b. b -> Either a b
Right (BareSpec
bs, LogicNameEnv
logicNameEnv', LogicMap
lmap2)
    else
      [Error] -> Either [Error] (BareSpec, LogicNameEnv, LogicMap)
forall a b. a -> Either a b
Left (RenameOutput -> [Error]
roErrors RenameOutput
ro)
  where
    taliases :: HashMap Symbol (Module, RTAlias Symbol ())
taliases = Module
-> BareSpecParsed
-> TargetDependencies
-> HashMap Symbol (Module, RTAlias Symbol ())
collectTypeAliases Module
thisModule BareSpecParsed
bareSpec0 TargetDependencies
dependencies
    allEaliases :: HashSet Symbol
allEaliases = BareSpecParsed -> TargetDependencies -> HashSet Symbol
collectExprAliases BareSpecParsed
bareSpec0 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 -> Module -> Maybe Name -> LHName
makeLogicLHName Symbol
s Module
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 LHNameSpace
LHTcName 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 Symbol
-> HashMap Symbol (Module, RTAlias Symbol ())
-> Maybe (Module, RTAlias Symbol ())
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HM.lookup Symbol
s HashMap Symbol (Module, RTAlias Symbol ())
taliases of
              Just (Module
m, 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
$ LHResolvedName -> Symbol -> LHName
LHNResolved (LogicName -> LHResolvedName
LHRLogic (LogicName -> LHResolvedName) -> LogicName -> LHResolvedName
forall a b. (a -> b) -> a -> b
$ Symbol -> Module -> Maybe Name -> LogicName
LogicName Symbol
s Module
m Maybe Name
forall a. Maybe a
Nothing) Symbol
s
              Maybe (Module, RTAlias Symbol ())
Nothing -> LHNameSpace
-> Located LHName
-> Symbol
-> ([Name] -> Maybe Name)
-> StateT RenameOutput Identity LHName
lookupGRELHName LHNameSpace
LHTcName Located LHName
lname Symbol
s [Name] -> Maybe Name
forall a. [a] -> Maybe a
listToMaybe
        LHNUnresolved ns :: LHNameSpace
ns@(LHVarName LHThisModuleNameFlag
lcl) Symbol
s
          | Symbol -> Bool
isDataCon Symbol
s ->
              LHNameSpace
-> Located LHName
-> Symbol
-> ([Name] -> Maybe Name)
-> StateT RenameOutput Identity LHName
lookupGRELHName (LHThisModuleNameFlag -> LHNameSpace
LHDataConName LHThisModuleNameFlag
lcl) Located LHName
lname Symbol
s [Name] -> Maybe Name
forall a. [a] -> Maybe a
listToMaybe
          | Bool
otherwise ->
              LHNameSpace
-> Located LHName
-> Symbol
-> ([Name] -> Maybe Name)
-> StateT RenameOutput Identity LHName
lookupGRELHName LHNameSpace
ns Located LHName
lname Symbol
s
                ((Either Name Var -> Name) -> Maybe (Either Name Var) -> Maybe Name
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name -> Name) -> (Var -> Name) -> Either Name Var -> Name
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Name -> Name
forall a. a -> a
id Var -> Name
forall a. NamedThing a => a -> Name
GHC.getName) (Maybe (Either Name Var) -> Maybe Name)
-> ([Name] -> Maybe (Either Name Var)) -> [Name] -> Maybe Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocalVars -> LocSymbol -> [Name] -> Maybe (Either Name Var)
forall a.
Loc a =>
LocalVars -> LocSymbol -> [a] -> Maybe (Either a Var)
Resolve.lookupLocalVar LocalVars
localVars (Located LHName -> Symbol -> LocSymbol
forall l b. Loc l => l -> b -> Located b
atLoc 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 -> Module -> Maybe Name -> LHName
makeLogicLHName Symbol
s Module
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 LHNameSpace
ns Symbol
s -> LHNameSpace
-> Located LHName
-> Symbol
-> ([Name] -> Maybe Name)
-> StateT RenameOutput Identity LHName
lookupGRELHName LHNameSpace
ns Located LHName
lname Symbol
s [Name] -> Maybe Name
forall a. [a] -> Maybe a
listToMaybe
        LHName
n -> LHName -> StateT RenameOutput Identity LHName
forall a. a -> StateT RenameOutput Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure LHName
n

    lookupGRELHName :: LHNameSpace
-> Located LHName
-> Symbol
-> ([Name] -> Maybe Name)
-> StateT RenameOutput Identity LHName
lookupGRELHName LHNameSpace
ns Located LHName
lname Symbol
s [Name] -> Maybe Name
localNameLookup =
      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
              n' :: Name
n' = Name -> Maybe Name -> Name
forall a. a -> Maybe a -> a
fromMaybe Name
n (Maybe Name -> Name) -> Maybe Name -> Name
forall a b. (a -> b) -> a -> b
$ [Name] -> Maybe Name
localNameLookup [Name
n]
          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
          let topLevelNames :: [Name]
topLevelNames = (GlobalRdrEltX GREInfo -> Name)
-> [GlobalRdrEltX GREInfo] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map GlobalRdrEltX GREInfo -> Name
forall info. GlobalRdrEltX info -> Name
GHC.greName [GlobalRdrEltX GREInfo]
es
          case [Name] -> Maybe Name
localNameLookup [Name]
topLevelNames of
            Just Name
n | Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Name
n [Name]
topLevelNames ->
              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
            Maybe Name
_ -> do
              Error -> State RenameOutput ()
addError
                (SrcSpan -> Doc -> [Doc] -> Error
forall t. SrcSpan -> Doc -> [Doc] -> TError t
ErrDupNames
                   (Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
LH.fSrcSpan Located LHName
lname)
                   (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
        [] ->
          case [Name] -> Maybe Name
localNameLookup [] of
            Just Name
n' ->
              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
            Maybe Name
Nothing -> do
              Error -> State RenameOutput ()
addError
                (Doc -> [Char] -> LocSymbol -> Error
errResolve (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
      LHNameSpace
LHTcName -> Bool
False
      LHNameSpace
LHLogicNameBinder -> Bool
False
      LHNameSpace
LHLogicName -> Bool
False

    nameSpaceKind :: LHNameSpace -> PJ.Doc
    nameSpaceKind :: LHNameSpace -> Doc
nameSpaceKind = \case
      LHNameSpace
LHTcName -> Doc
"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 :: PJ.Doc -> String -> LocSymbol -> Error
errResolve :: Doc -> [Char] -> LocSymbol -> Error
errResolve Doc
k [Char]
msg LocSymbol
lx = SrcSpan -> Doc -> Doc -> Doc -> Error
forall t. SrcSpan -> Doc -> Doc -> Doc -> TError t
ErrResolve (LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
LH.fSrcSpan LocSymbol
lx) Doc
k (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
lx)) ([Char] -> Doc
PJ.text [Char]
msg)

-- | 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 LHNameSpace
LHTcName 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
$ 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] -> Error
forall t. SrcSpan -> Doc -> [Doc] -> TError t
ErrDupNames
                (LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
LH.fSrcSpan LocSymbol
lx)
                (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
      LHNameSpace
LHTcName -> 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
      LHNameSpace
LHTcName -> 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 :: BareSpecParsed -> BareSpecParsed
resolveBoundVarsInTypeAliases = ([Symbol] -> LHName -> LHName) -> BareSpecParsed -> BareSpecParsed
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 LHNameSpace
LHTcName 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 LHNameSpace
LHTcName 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 = [ Loc sp0 sp1 (a { rtBody = mapLHNames (f args) (rtBody a) })
                        | Loc sp0 sp1 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
  :: HM.HashMap Symbol (GHC.Module, RTAlias Symbol ())
  -> BareSpecParsed
  -> BareSpecParsed
fixExpressionArgsOfTypeAliases :: HashMap Symbol (Module, RTAlias Symbol ())
-> BareSpecParsed -> BareSpecParsed
fixExpressionArgsOfTypeAliases HashMap Symbol (Module, RTAlias Symbol ())
taliases =
    (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
 -> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
-> BareSpecParsed -> BareSpecParsed
mapBareTypes RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
go (BareSpecParsed -> BareSpecParsed)
-> (BareSpecParsed -> BareSpecParsed)
-> BareSpecParsed
-> BareSpecParsed
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpecParsed -> BareSpecParsed
resolveBoundVarsInTypeAliases
  where
    go :: BareTypeParsed -> BareTypeParsed
    go :: RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
go (RApp c :: BTyCon
c@(BTyCon { btc_tc :: BTyCon -> Located LHName
btc_tc = Loc SourcePos
_ SourcePos
_ (LHNUnresolved LHNameSpace
LHTcName Symbol
s) }) [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
ts [RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
rs RReftV LocSymbol
r)
      | Just (Module
_, RTAlias Symbol ()
rta) <- Symbol
-> HashMap Symbol (Module, RTAlias Symbol ())
-> Maybe (Module, RTAlias Symbol ())
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HM.lookup Symbol
s HashMap Symbol (Module, RTAlias Symbol ())
taliases =
        BTyCon
-> [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
-> [RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
-> RReftV LocSymbol
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp BTyCon
c (Located LHName
-> RTAlias Symbol ()
-> [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
-> [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
forall {b} {a} {a}.
Located b
-> RTAlias a a
-> [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
-> [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
fixExprArgs (BTyCon -> Located LHName
btc_tc BTyCon
c) RTAlias Symbol ()
rta ((RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
 -> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
-> [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
-> [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
forall a b. (a -> b) -> [a] -> [b]
map RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
go [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
ts)) ((RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
 -> RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
-> [RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
-> [RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
forall a b. (a -> b) -> [a] -> [b]
map RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
goRef [RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
rs) RReftV LocSymbol
r
    go (RApp BTyCon
c [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
ts [RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
rs RReftV LocSymbol
r) =
        BTyCon
-> [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
-> [RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
-> RReftV LocSymbol
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp BTyCon
c ((RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
 -> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
-> [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
-> [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
forall a b. (a -> b) -> [a] -> [b]
map RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
go [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
ts) ((RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
 -> RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
-> [RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
-> [RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
forall a b. (a -> b) -> [a] -> [b]
map RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
goRef [RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
rs) RReftV LocSymbol
r
    go (RAppTy RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t1 RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t2 RReftV LocSymbol
r)  = RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RReftV LocSymbol
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
go RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t1) (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
go RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t2) RReftV LocSymbol
r
    go (RFun  Symbol
x RFInfo
i RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t1 RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t2 RReftV LocSymbol
r) = Symbol
-> RFInfo
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RReftV LocSymbol
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun  Symbol
x RFInfo
i (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
go RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t1) (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
go RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t2) RReftV LocSymbol
r
    go (RAllT RTVUV LocSymbol BTyCon BTyVar
a RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t RReftV LocSymbol
r)     = RTVUV LocSymbol BTyCon BTyVar
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RReftV LocSymbol
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV LocSymbol BTyCon BTyVar
a (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
go RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t) RReftV LocSymbol
r
    go (RAllP PVUV LocSymbol BTyCon BTyVar
a RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t)       = PVUV LocSymbol BTyCon BTyVar
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV LocSymbol BTyCon BTyVar
a (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
go RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t)
    go (RAllE Symbol
x RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t1 RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t2)   = Symbol
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
RAllE Symbol
x (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
go RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t1) (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
go RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t2)
    go (REx Symbol
x RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t1 RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t2)     = Symbol
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
REx   Symbol
x (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
go RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t1) (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
go RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t2)
    go (RRTy [(Symbol, RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
e RReftV LocSymbol
r Oblig
o RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t)    = [(Symbol, RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
-> RReftV LocSymbol
-> Oblig
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy  [(Symbol, RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
e RReftV LocSymbol
r Oblig
o     (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
go RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t)
    go t :: RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t@RHole{}         = RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t
    go t :: RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t@RVar{}          = RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t
    go t :: RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t@RExprArg{}      = RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t
    goRef :: RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
goRef (RProp [(Symbol, RTypeV LocSymbol BTyCon BTyVar ())]
ss RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t)   = [(Symbol, RTypeV LocSymbol BTyCon BTyVar ())]
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTPropV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RTypeV LocSymbol BTyCon BTyVar ())]
ss (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
go RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t)

    fixExprArgs :: Located b
-> RTAlias a a
-> [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
-> [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
fixExprArgs Located b
lname RTAlias a a
rta [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
ts =
      let n :: Int
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)
          ([RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
targs, [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
eargs) = Int
-> [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
-> ([RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)],
    [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
ts
          msg :: [Char]
msg = [Char]
"FIX-EXPRESSION-ARG: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. PPrint a => a -> [Char]
showpp (RTAlias a a -> Symbol
forall x a. RTAlias x a -> Symbol
rtName RTAlias a a
rta)
          toExprArg :: RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> ExprV LocSymbol
toExprArg = SourcePos
-> [Char]
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> ExprV LocSymbol
exprArg (Located b -> SourcePos
forall a. Loc a => a -> SourcePos
LH.fSourcePos Located b
lname) [Char]
msg
       in [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
targs [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
-> [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
-> [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
forall a. [a] -> [a] -> [a]
++ [ Located (ExprV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
forall v c tv r. Located (ExprV v) -> RTypeV v c tv r
RExprArg (Located (ExprV LocSymbol)
 -> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
-> Located (ExprV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
forall a b. (a -> b) -> a -> b
$ RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> ExprV LocSymbol
toExprArg RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
e ExprV LocSymbol -> Located b -> Located (ExprV LocSymbol)
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Located b
lname | RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
e <- [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
eargs ]

mapBareTypes :: (BareTypeParsed -> BareTypeParsed) -> BareSpecParsed -> BareSpecParsed
mapBareTypes :: (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
 -> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
-> BareSpecParsed -> BareSpecParsed
mapBareTypes RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
f  = BareSpecParsed -> BareSpecParsed
forall a. Data a => a -> a
go
  where
    go :: Data a => a -> a
    go :: forall a. Data a => a -> a
go = (forall a. Data a => a -> a) -> a -> a
forall a. Data a => (forall a. Data a => a -> a) -> a -> a
gmapT (b -> b
forall a. Data a => a -> a
go (b -> b)
-> (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
    -> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
-> b
-> b
forall a b.
(Typeable a, Typeable b) =>
(a -> a) -> (b -> b) -> a -> a
`extT` RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
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 that `BareType` into an `Expr`.
exprArg :: SourcePos -> String -> BareTypeParsed -> ExprV LocSymbol
exprArg :: SourcePos
-> [Char]
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> ExprV LocSymbol
exprArg SourcePos
l [Char]
msg = [Char] -> ExprV LocSymbol -> ExprV LocSymbol
forall a. PPrint a => [Char] -> a -> a
notracepp ([Char]
"exprArg: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) (ExprV LocSymbol -> ExprV LocSymbol)
-> (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
    -> ExprV LocSymbol)
-> RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> ExprV LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> ExprV LocSymbol
go
  where
    go :: BareTypeParsed -> ExprV LocSymbol
    go :: RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> ExprV LocSymbol
go (RExprArg Located (ExprV LocSymbol)
e)     = Located (ExprV LocSymbol) -> ExprV LocSymbol
forall a. Located a -> a
val Located (ExprV LocSymbol)
e
    go (RVar (BTV LocSymbol
x) RReftV LocSymbol
_)       = LocSymbol -> ExprV LocSymbol
forall v. v -> ExprV v
EVar LocSymbol
x
    go (RApp BTyCon
x [] [] RReftV LocSymbol
_) = LocSymbol -> ExprV LocSymbol
forall v. v -> ExprV 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 [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
ts [] RReftV LocSymbol
_) = ExprV LocSymbol -> [ExprV LocSymbol] -> ExprV LocSymbol
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps (LocSymbol -> ExprV LocSymbol
forall v. v -> ExprV 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
f)) (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> ExprV LocSymbol
go (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
 -> ExprV LocSymbol)
-> [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
-> [ExprV LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
ts)
    go (RAppTy RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t1 RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t2 RReftV LocSymbol
_) = ExprV LocSymbol -> ExprV LocSymbol -> ExprV LocSymbol
forall v. ExprV v -> ExprV v -> ExprV v
EApp (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> ExprV LocSymbol
go RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t1) (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> ExprV LocSymbol
go RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
t2)
    go RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
z                = Maybe SrcSpan -> [Char] -> ExprV LocSymbol
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
sp ([Char] -> ExprV LocSymbol) -> [Char] -> ExprV 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
$ RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol) -> BareType
parsedToBareType RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)
z) [Char]
msg
    sp :: Maybe SrcSpan
sp                  = SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SourcePos -> SrcSpan
LH.sourcePosSrcSpan SourcePos
l)

-- | An environment of names in scope
--
-- For each symbol we have the aliases with which it is imported and the
-- name corresponding to each alias.
type InScopeNonReflectedEnv = SEnv [(GHC.ModuleName, (GHC.Module, LHName))]

-- | Looks the names in scope with the given symbol.
-- Returns a list of close but different symbols or a non empty list
-- with the matched names.
lookupInScopeNonReflectedEnv
  :: InScopeNonReflectedEnv -> Symbol -> Either [Symbol] [(GHC.Module, LHName)]
lookupInScopeNonReflectedEnv :: InScopeNonReflectedEnv
-> Symbol -> Either [Symbol] [(Module, LHName)]
lookupInScopeNonReflectedEnv InScopeNonReflectedEnv
env Symbol
s = do
    let n :: Symbol
n = Symbol -> Symbol
LH.dropModuleNames Symbol
s
    case Symbol
-> InScopeNonReflectedEnv
-> SESearch [(ModuleName, (Module, LHName))]
forall a. Symbol -> SEnv a -> SESearch a
lookupSEnvWithDistance Symbol
n InScopeNonReflectedEnv
env of
      Alts [Symbol]
closeSyms -> [Symbol] -> Either [Symbol] [(Module, LHName)]
forall a b. a -> Either a b
Left [Symbol]
closeSyms
      F.Found [(ModuleName, (Module, LHName))]
xs -> do
         let q :: Symbol
q = Symbol -> Symbol
LH.takeModuleNames Symbol
s
         case ((ModuleName, (Module, LHName)) -> Bool)
-> [(ModuleName, (Module, LHName))]
-> [(ModuleName, (Module, LHName))]
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, (Module, LHName)) -> FastString)
-> (ModuleName, (Module, LHName))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> FastString
GHC.moduleNameFS (ModuleName -> FastString)
-> ((ModuleName, (Module, LHName)) -> ModuleName)
-> (ModuleName, (Module, LHName))
-> FastString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleName, (Module, LHName)) -> ModuleName
forall a b. (a, b) -> a
fst) [(ModuleName, (Module, LHName))]
xs of
           [] -> [Symbol] -> Either [Symbol] [(Module, LHName)]
forall a b. a -> Either a b
Left ([Symbol] -> Either [Symbol] [(Module, LHName)])
-> [Symbol] -> Either [Symbol] [(Module, LHName)]
forall a b. (a -> b) -> a -> b
$ ((ModuleName, (Module, LHName)) -> Symbol)
-> [(ModuleName, (Module, LHName))] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol -> Symbol -> Symbol
maybeQualifySymbol Symbol
n (Symbol -> Symbol)
-> ((ModuleName, (Module, LHName)) -> Symbol)
-> (ModuleName, (Module, LHName))
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol ([Char] -> Symbol)
-> ((ModuleName, (Module, LHName)) -> [Char])
-> (ModuleName, (Module, LHName))
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> [Char]
GHC.moduleNameString (ModuleName -> [Char])
-> ((ModuleName, (Module, LHName)) -> ModuleName)
-> (ModuleName, (Module, LHName))
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleName, (Module, LHName)) -> ModuleName
forall a b. (a, b) -> a
fst) [(ModuleName, (Module, LHName))]
xs
           [(ModuleName, (Module, LHName))]
ys -> [(Module, LHName)] -> Either [Symbol] [(Module, LHName)]
forall a b. b -> Either a b
Right ([(Module, LHName)] -> Either [Symbol] [(Module, LHName)])
-> [(Module, LHName)] -> Either [Symbol] [(Module, LHName)]
forall a b. (a -> b) -> a -> b
$ ((ModuleName, (Module, LHName)) -> (Module, LHName))
-> [(ModuleName, (Module, LHName))] -> [(Module, LHName)]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleName, (Module, LHName)) -> (Module, LHName)
forall a b. (a, b) -> b
snd [(ModuleName, (Module, LHName))]
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
-- aliases 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
     , HS.HashSet Symbol
     )
makeLogicEnvs :: ImportedMods
-> Module
-> BareSpecParsed
-> TargetDependencies
-> (InScopeNonReflectedEnv, LogicNameEnv, HashSet LocSymbol,
    HashSet Symbol)
makeLogicEnvs ImportedMods
impAvails Module
thisModule BareSpecParsed
spec TargetDependencies
dependencies =
    let unqualify :: Symbol -> Symbol
unqualify Symbol
s =
          if Symbol
s Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> Symbol -> Symbol
LH.qualifySymbol (ModuleName -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (ModuleName -> Symbol) -> ModuleName -> Symbol
forall a b. (a -> b) -> a -> b
$ Module -> ModuleName
forall unit. GenModule unit -> ModuleName
GHC.moduleName Module
thisModule) (Symbol -> Symbol
LH.dropModuleNames Symbol
s) then
            Symbol -> Symbol
LH.dropModuleNames Symbol
s
          else
            Symbol
s

        -- Names should be removed from this list as they are supported
        -- by renaming.
        unhandledNames :: HashSet Symbol
unhandledNames = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
HS.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$
          (Symbol -> Symbol) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Symbol
unqualify [Symbol]
unhandledNamesList [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (Symbol -> Symbol) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol -> Symbol -> Symbol
LH.qualifySymbol (ModuleName -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (ModuleName -> Symbol) -> ModuleName -> Symbol
forall a b. (a -> b) -> a -> b
$ Module -> ModuleName
forall unit. GenModule unit -> ModuleName
GHC.moduleName Module
thisModule)) [Symbol]
unhandledNamesList
        unhandledNamesList :: [Symbol]
unhandledNamesList =
          (Located (RTAlias Symbol (ExprV LocSymbol)) -> Symbol)
-> [Located (RTAlias Symbol (ExprV LocSymbol))] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (RTAlias Symbol (ExprV LocSymbol) -> Symbol
forall x a. RTAlias x a -> Symbol
rtName (RTAlias Symbol (ExprV LocSymbol) -> Symbol)
-> (Located (RTAlias Symbol (ExprV LocSymbol))
    -> RTAlias Symbol (ExprV LocSymbol))
-> Located (RTAlias Symbol (ExprV LocSymbol))
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (RTAlias Symbol (ExprV LocSymbol))
-> RTAlias Symbol (ExprV LocSymbol)
forall a. Located a -> a
val) (BareSpecParsed -> [Located (RTAlias Symbol (ExprV LocSymbol))]
forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (ExprV lname))]
ealiases BareSpecParsed
spec)
          [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ ((Module, [LHName]) -> [Symbol])
-> [(Module, [LHName])] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((LHName -> Symbol) -> [LHName] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map LHName -> Symbol
getLHNameSymbol ([LHName] -> [Symbol])
-> ((Module, [LHName]) -> [LHName])
-> (Module, [LHName])
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Module, [LHName]) -> [LHName]
forall a b. (a, b) -> b
snd) [(Module, [LHName])]
unhandledLogicNames
        unhandledLogicNames :: [(Module, [LHName])]
unhandledLogicNames =
          ((Module, LiftedSpec) -> (Module, [LHName]))
-> [(Module, LiftedSpec)] -> [(Module, [LHName])]
forall a b. (a -> b) -> [a] -> [b]
map ((LiftedSpec -> [LHName])
-> (Module, LiftedSpec) -> (Module, [LHName])
forall a b. (a -> b) -> (Module, a) -> (Module, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LiftedSpec -> [LHName]
collectUnhandledLiftedSpecLogicNames) [(Module, LiftedSpec)]
dependencyPairs
        logicNames :: [(Module, [LHName])]
logicNames =
          (Module
thisModule, [LHName]
thisModuleNames) (Module, [LHName]) -> [(Module, [LHName])] -> [(Module, [LHName])]
forall a. a -> [a] -> [a]
:
          ((Module, LiftedSpec) -> (Module, [LHName]))
-> [(Module, LiftedSpec)] -> [(Module, [LHName])]
forall a b. (a -> b) -> [a] -> [b]
map ((LiftedSpec -> [LHName])
-> (Module, LiftedSpec) -> (Module, [LHName])
forall a b. (a -> b) -> (Module, a) -> (Module, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LiftedSpec -> [LHName]
collectLiftedSpecLogicNames) [(Module, LiftedSpec)]
dependencyPairs
          [(Module, [LHName])]
-> [(Module, [LHName])] -> [(Module, [LHName])]
forall a. [a] -> [a] -> [a]
++ [(Module, [LHName])]
unhandledLogicNames
        thisModuleNames :: [LHName]
thisModuleNames = [[LHName]] -> [LHName]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ [ HasCallStack => Module -> LHName -> LHName
Module -> LHName -> LHName
reflectLHName Module
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 (BareSpecParsed -> [(Located LHName, Located LHName)]
forall lname ty.
Spec lname ty -> [(Located LHName, Located LHName)]
asmReflectSigs BareSpecParsed
spec)
              , HashSet (Located LHName) -> [Located LHName]
forall a. HashSet a -> [a]
HS.toList (BareSpecParsed -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
reflects BareSpecParsed
spec)
              , HashSet (Located LHName) -> [Located LHName]
forall a. HashSet a -> [a]
HS.toList (BareSpecParsed -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
opaqueReflects BareSpecParsed
spec)
              , HashSet (Located LHName) -> [Located LHName]
forall a. HashSet a -> [a]
HS.toList (BareSpecParsed -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
inlines BareSpecParsed
spec)
              , HashSet (Located LHName) -> [Located LHName]
forall a. HashSet a -> [a]
HS.toList (BareSpecParsed -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
hmeas BareSpecParsed
spec)
              ]
            ]
          , [ Located LHName -> LHName
forall a. Located a -> a
val (MeasureV
  LocSymbol
  (Located (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))
  (Located LHName)
-> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName MeasureV
  LocSymbol
  (Located (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))
  (Located LHName)
m) | MeasureV
  LocSymbol
  (Located (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))
  (Located LHName)
m <- BareSpecParsed
-> [MeasureV
      LocSymbol
      (Located (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))
      (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
measures BareSpecParsed
spec ]
          , [ Located LHName -> LHName
forall a. Located a -> a
val (MeasureV
  LocSymbol
  (Located (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))
  ()
-> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName MeasureV
  LocSymbol
  (Located (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))
  ()
m) | MeasureV
  LocSymbol
  (Located (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))
  ()
m <- BareSpecParsed
-> [MeasureV
      LocSymbol
      (Located (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))
      ()]
forall lname ty. Spec lname ty -> [MeasureV lname (Located ty) ()]
cmeasures BareSpecParsed
spec ]
          , ((LHName, RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
 -> LHName)
-> [(LHName, RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
-> [LHName]
forall a b. (a -> b) -> [a] -> [b]
map (LHName, RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
-> LHName
forall a b. (a, b) -> a
fst ([(LHName, RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
 -> [LHName])
-> [(LHName, RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
-> [LHName]
forall a b. (a -> b) -> a -> b
$
             (DataCtorP (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
 -> [(LHName, RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))])
-> [DataCtorP (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
-> [(LHName, RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataCtorP (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
-> [(LHName, RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
forall ty. DataCtorP ty -> [(LHName, ty)]
DataDecl.dcFields ([DataCtorP (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
 -> [(LHName, RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))])
-> [DataCtorP (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
-> [(LHName, RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
forall a b. (a -> b) -> a -> b
$ [[DataCtorP (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]]
-> [DataCtorP (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[DataCtorP (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]]
 -> [DataCtorP (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))])
-> [[DataCtorP
       (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]]
-> [DataCtorP (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
forall a b. (a -> b) -> a -> b
$
             (DataDeclP
   LocSymbol (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
 -> Maybe
      [DataCtorP (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))])
-> [DataDeclP
      LocSymbol (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
-> [[DataCtorP
       (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe DataDeclP
  LocSymbol (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))
-> Maybe
     [DataCtorP (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
forall v ty. DataDeclP v ty -> Maybe [DataCtorP ty]
DataDecl.tycDCons ([DataDeclP
    LocSymbol (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
 -> [[DataCtorP
        (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]])
-> [DataDeclP
      LocSymbol (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
-> [[DataCtorP
       (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]]
forall a b. (a -> b) -> a -> b
$
             BareSpecParsed
-> [DataDeclP
      LocSymbol (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol))]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
dataDecls BareSpecParsed
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
$
            BareSpecParsed -> HashSet LocSymbol
forall lname ty. Spec lname ty -> HashSet LocSymbol
privateReflects BareSpecParsed
spec HashSet LocSymbol -> [HashSet LocSymbol] -> [HashSet LocSymbol]
forall a. a -> [a] -> [a]
: ((Module, LiftedSpec) -> HashSet LocSymbol)
-> [(Module, LiftedSpec)] -> [HashSet LocSymbol]
forall a b. (a -> b) -> [a] -> [b]
map (LiftedSpec -> HashSet LocSymbol
liftedPrivateReflects (LiftedSpec -> HashSet LocSymbol)
-> ((Module, LiftedSpec) -> LiftedSpec)
-> (Module, LiftedSpec)
-> HashSet LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Module, LiftedSpec) -> LiftedSpec
forall a b. (a, b) -> b
snd) [(Module, LiftedSpec)]
dependencyPairs
     in
        ( [InScopeNonReflectedEnv] -> InScopeNonReflectedEnv
unionAliasEnvs ([InScopeNonReflectedEnv] -> InScopeNonReflectedEnv)
-> [InScopeNonReflectedEnv] -> InScopeNonReflectedEnv
forall a b. (a -> b) -> a -> b
$ ((Module, [LHName]) -> InScopeNonReflectedEnv)
-> [(Module, [LHName])] -> [InScopeNonReflectedEnv]
forall a b. (a -> b) -> [a] -> [b]
map (Module, [LHName]) -> InScopeNonReflectedEnv
mkAliasEnv [(Module, [LHName])]
logicNames
        , [LHName] -> LogicNameEnv
mkLogicNameEnv (((Module, [LHName]) -> [LHName])
-> [(Module, [LHName])] -> [LHName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Module, [LHName]) -> [LHName]
forall a b. (a, b) -> b
snd [(Module, [LHName])]
logicNames)
        , HashSet LocSymbol
privateReflectNames
        , HashSet Symbol
unhandledNames
        )
  where
    dependencyPairs :: [(Module, LiftedSpec)]
dependencyPairs = ((StableModule, LiftedSpec) -> (Module, LiftedSpec))
-> [(StableModule, LiftedSpec)] -> [(Module, LiftedSpec)]
forall a b. (a -> b) -> [a] -> [b]
map ((StableModule -> Module)
-> (StableModule, LiftedSpec) -> (Module, 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 -> Module
GHC.unStableModule) ([(StableModule, LiftedSpec)] -> [(Module, LiftedSpec)])
-> [(StableModule, LiftedSpec)] -> [(Module, 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

    mkAliasEnv :: (Module, [LHName]) -> InScopeNonReflectedEnv
mkAliasEnv (Module
m, [LHName]
lhnames) =
      let aliases :: [ModuleName]
aliases = Module -> [ModuleName]
moduleAliases Module
m
       in [(Symbol, [(ModuleName, (Module, LHName))])]
-> InScopeNonReflectedEnv
forall a. [(Symbol, a)] -> SEnv a
fromListSEnv
            [ (Symbol
s, (ModuleName -> (ModuleName, (Module, LHName)))
-> [ModuleName] -> [(ModuleName, (Module, LHName))]
forall a b. (a -> b) -> [a] -> [b]
map (,(Module
m, LHName
lhname)) [ModuleName]
aliases)
              -- Note that only non-reflected names go to the InScope environment.
              -- See the local function resolveVarName for more details.
            | lhname :: LHName
lhname@(LHNResolved (LHRLogic (LogicName Symbol
s Module
_ Maybe Name
Nothing)) Symbol
_) <- [LHName]
lhnames
            ]

    unionAliasEnvs :: [InScopeNonReflectedEnv] -> InScopeNonReflectedEnv
    unionAliasEnvs :: [InScopeNonReflectedEnv] -> InScopeNonReflectedEnv
unionAliasEnvs =
      HashMap Symbol [(ModuleName, (Module, LHName))]
-> InScopeNonReflectedEnv
forall a b. Coercible a b => a -> b
coerce (HashMap Symbol [(ModuleName, (Module, LHName))]
 -> InScopeNonReflectedEnv)
-> ([InScopeNonReflectedEnv]
    -> HashMap Symbol [(ModuleName, (Module, LHName))])
-> [InScopeNonReflectedEnv]
-> InScopeNonReflectedEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      ([(ModuleName, (Module, LHName))]
 -> [(ModuleName, (Module, LHName))])
-> HashMap Symbol [(ModuleName, (Module, LHName))]
-> HashMap Symbol [(ModuleName, (Module, LHName))]
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HM.map (((ModuleName, (Module, LHName))
 -> (ModuleName, (Module, LHName)) -> Bool)
-> [(ModuleName, (Module, LHName))]
-> [(ModuleName, (Module, LHName))]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (\(ModuleName
alias1, (Module
_, LHName
n1)) (ModuleName
alias2, (Module
_, LHName
n2)) -> 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, (Module, LHName))]
 -> HashMap Symbol [(ModuleName, (Module, LHName))])
-> ([InScopeNonReflectedEnv]
    -> HashMap Symbol [(ModuleName, (Module, LHName))])
-> [InScopeNonReflectedEnv]
-> HashMap Symbol [(ModuleName, (Module, LHName))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      (HashMap Symbol [(ModuleName, (Module, LHName))]
 -> HashMap Symbol [(ModuleName, (Module, LHName))]
 -> HashMap Symbol [(ModuleName, (Module, LHName))])
-> HashMap Symbol [(ModuleName, (Module, LHName))]
-> [HashMap Symbol [(ModuleName, (Module, LHName))]]
-> HashMap Symbol [(ModuleName, (Module, LHName))]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (([(ModuleName, (Module, LHName))]
 -> [(ModuleName, (Module, LHName))]
 -> [(ModuleName, (Module, LHName))])
-> HashMap Symbol [(ModuleName, (Module, LHName))]
-> HashMap Symbol [(ModuleName, (Module, LHName))]
-> HashMap Symbol [(ModuleName, (Module, LHName))]
forall k v.
Eq k =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HM.unionWith [(ModuleName, (Module, LHName))]
-> [(ModuleName, (Module, LHName))]
-> [(ModuleName, (Module, LHName))]
forall a. [a] -> [a] -> [a]
(++)) HashMap Symbol [(ModuleName, (Module, LHName))]
forall k v. HashMap k v
HM.empty ([HashMap Symbol [(ModuleName, (Module, LHName))]]
 -> HashMap Symbol [(ModuleName, (Module, LHName))])
-> ([InScopeNonReflectedEnv]
    -> [HashMap Symbol [(ModuleName, (Module, LHName))]])
-> [InScopeNonReflectedEnv]
-> HashMap Symbol [(ModuleName, (Module, LHName))]
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))]]

    moduleAliases :: Module -> [ModuleName]
moduleAliases Module
m =
      case ImportedMods -> Module -> Maybe [ImportedBy]
forall a. ModuleEnv a -> Module -> Maybe a
GHC.lookupModuleEnv ImportedMods
impAvails Module
m of
        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
          | Module
thisModule Module -> Module -> Bool
forall a. Eq a => a -> a -> Bool
== Module
m ->
            -- Aliases for the current module
            [Module -> ModuleName
forall unit. GenModule unit -> ModuleName
GHC.moduleName Module
m, [Char] -> ModuleName
GHC.mkModuleName [Char]
""]
          | Bool
otherwise ->
            -- 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 <- Module -> Maybe [Char]
forall {unit}. GenModule unit -> Maybe [Char]
dropLHAssumptionsSuffix Module
m
                pMod <- findDependency pString
                GHC.lookupModuleEnv impAvails pMod

    dropLHAssumptionsSuffix :: GenModule unit -> Maybe [Char]
dropLHAssumptionsSuffix GenModule unit
m =
      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 Module
findDependency [Char]
ms =
      (Module -> Bool) -> [Module] -> Maybe Module
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) -> (Module -> [Char]) -> Module -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> [Char]
GHC.moduleNameString (ModuleName -> [Char])
-> (Module -> ModuleName) -> Module -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Module -> ModuleName
forall unit. GenModule unit -> ModuleName
GHC.moduleName) ([Module] -> Maybe Module) -> [Module] -> Maybe Module
forall a b. (a -> b) -> a -> b
$
      ImportedMods -> [Module]
forall a. ModuleEnv a -> [Module]
GHC.moduleEnvKeys ImportedMods
impAvails

    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]
""]

    mkLogicNameEnv :: [LHName] -> LogicNameEnv
mkLogicNameEnv [LHName]
names =
      LogicNameEnv
        { lneLHName :: SEnv LHName
lneLHName = [(Symbol, LHName)] -> SEnv LHName
forall a. [(Symbol, a)] -> SEnv 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]]
        }

{- HLINT ignore collectUnhandledLiftedSpecLogicNames "Use ++" -}
collectUnhandledLiftedSpecLogicNames :: LiftedSpec -> [LHName]
collectUnhandledLiftedSpecLogicNames :: LiftedSpec -> [LHName]
collectUnhandledLiftedSpecLogicNames LiftedSpec
sp =
    (Located (RTAlias Symbol (ExprV LHName)) -> LHName)
-> [Located (RTAlias Symbol (ExprV LHName))] -> [LHName]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol -> LHName
makeLocalLHName (Symbol -> LHName)
-> (Located (RTAlias Symbol (ExprV LHName)) -> Symbol)
-> Located (RTAlias Symbol (ExprV LHName))
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
LH.dropModuleNames (Symbol -> Symbol)
-> (Located (RTAlias Symbol (ExprV LHName)) -> Symbol)
-> Located (RTAlias Symbol (ExprV LHName))
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias Symbol (ExprV LHName) -> Symbol
forall x a. RTAlias x a -> Symbol
rtName (RTAlias Symbol (ExprV LHName) -> Symbol)
-> (Located (RTAlias Symbol (ExprV LHName))
    -> RTAlias Symbol (ExprV LHName))
-> Located (RTAlias Symbol (ExprV LHName))
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (RTAlias Symbol (ExprV LHName))
-> RTAlias Symbol (ExprV LHName)
forall a. Located a -> a
val) ([Located (RTAlias Symbol (ExprV LHName))] -> [LHName])
-> [Located (RTAlias Symbol (ExprV LHName))] -> [LHName]
forall a b. (a -> b) -> a -> b
$ HashSet (Located (RTAlias Symbol (ExprV LHName)))
-> [Located (RTAlias Symbol (ExprV LHName))]
forall a. HashSet a -> [a]
HS.toList (HashSet (Located (RTAlias Symbol (ExprV LHName)))
 -> [Located (RTAlias Symbol (ExprV LHName))])
-> HashSet (Located (RTAlias Symbol (ExprV LHName)))
-> [Located (RTAlias Symbol (ExprV LHName))]
forall a b. (a -> b) -> a -> b
$ LiftedSpec -> HashSet (Located (RTAlias Symbol (ExprV LHName)))
liftedEaliases LiftedSpec
sp

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)
    , ((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
$
        (DataDeclP LHName BareTypeLHName
 -> Maybe [DataCtorP BareTypeLHName])
-> [DataDeclP LHName BareTypeLHName]
-> [[DataCtorP BareTypeLHName]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe DataDeclP LHName BareTypeLHName -> Maybe [DataCtorP BareTypeLHName]
forall v ty. DataDeclP v ty -> Maybe [DataCtorP ty]
DataDecl.tycDCons ([DataDeclP LHName BareTypeLHName] -> [[DataCtorP BareTypeLHName]])
-> [DataDeclP LHName BareTypeLHName]
-> [[DataCtorP BareTypeLHName]]
forall a b. (a -> b) -> a -> b
$
        HashSet (DataDeclP LHName BareTypeLHName)
-> [DataDeclP LHName BareTypeLHName]
forall a. HashSet a -> [a]
HS.toList (HashSet (DataDeclP LHName BareTypeLHName)
 -> [DataDeclP LHName BareTypeLHName])
-> HashSet (DataDeclP LHName BareTypeLHName)
-> [DataDeclP LHName BareTypeLHName]
forall a b. (a -> b) -> a -> b
$ LiftedSpec -> HashSet (DataDeclP LHName BareTypeLHName)
liftedDataDecls 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
  -> InScopeNonReflectedEnv
  -> GHC.GlobalRdrEnv
  -> HS.HashSet Symbol
  -> LogicMap
  -> LocalVars
  -> LogicNameEnv
  -> HS.HashSet LocSymbol
  -> HS.HashSet Symbol
  -> BareSpecParsed
  -> State RenameOutput BareSpecLHName
resolveLogicNames :: Config
-> InScopeNonReflectedEnv
-> GlobalRdrEnv
-> HashSet Symbol
-> LogicMap
-> LocalVars
-> LogicNameEnv
-> HashSet LocSymbol
-> HashSet Symbol
-> BareSpecParsed
-> StateT RenameOutput Identity BareSpecLHName
resolveLogicNames Config
cfg InScopeNonReflectedEnv
env GlobalRdrEnv
globalRdrEnv HashSet Symbol
unhandledNames LogicMap
lmap0 LocalVars
localVars LogicNameEnv
lnameEnv HashSet LocSymbol
privateReflectNames HashSet Symbol
allEaliases BareSpecParsed
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 (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))
   (Located LHName)
 -> StateT
      RenameOutput
      Identity
      (MeasureV
         LocSymbol
         (Located (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))
         (Located LHName)))
-> [MeasureV
      LocSymbol
      (Located (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))
      (Located LHName)]
-> StateT
     RenameOutput
     Identity
     [MeasureV
        LocSymbol
        (Located (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))
        (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 (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))
     (Located LHName)
-> StateT
     RenameOutput
     Identity
     (MeasureV
        LocSymbol
        (Located (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))
        (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) (BareSpecParsed
-> [MeasureV
      LocSymbol
      (Located (RTypeV LocSymbol BTyCon BTyVar (RReftV LocSymbol)))
      (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
imeasures BareSpecParsed
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] [(Module, LHName)]
lookupInScopeNonReflectedEnv 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
                  Bool -> State RenameOutput () -> State RenameOutput ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HS.member Symbol
s HashSet Symbol
unhandledNames) (State RenameOutput () -> State RenameOutput ())
-> State RenameOutput () -> State RenameOutput ()
forall a b. (a -> b) -> a -> b
$
                    Error -> State RenameOutput ()
addError (LocSymbol -> [Symbol] -> Error
forall {a} {a} {t}.
(PPrint a, PPrint a) =>
Located a -> [a] -> TError t
errResolveLogicName LocSymbol
ls [Symbol]
alts)
                  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 [(Module
_, 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
          Right [(Module, LHName)]
names -> do
            Error -> State RenameOutput ()
addError (Error -> State RenameOutput ()) -> Error -> State RenameOutput ()
forall a b. (a -> b) -> a -> b
$
              SrcSpan -> Doc -> [Doc] -> Error
forall t. SrcSpan -> Doc -> [Doc] -> TError t
ErrDupNames
                (LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
LH.fSrcSpan LocSymbol
ls)
                (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
s)
                [ 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 (Module -> ModuleName
forall unit. GenModule unit -> ModuleName
GHC.moduleName Module
m))
                | (Module
m, LHName
n) <- [(Module, 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)

    errResolveLogicName :: Located a -> [a] -> TError t
errResolveLogicName Located a
s [a]
alts =
      SrcSpan -> Doc -> Doc -> Doc -> TError t
forall t. SrcSpan -> Doc -> Doc -> Doc -> TError t
ErrResolve
        (Located a -> SrcSpan
forall a. Loc a => a -> SrcSpan
LH.fSrcSpan Located a
s)
        ([Char] -> Doc
PJ.text [Char]
"logic name")
        (a -> Doc
forall a. PPrint a => a -> Doc
pprint (a -> Doc) -> a -> Doc
forall a b. (a -> b) -> a -> b
$ Located a -> a
forall a. Located a -> a
val Located a
s)
        (if [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
alts then
           [Char] -> Doc
PJ.text [Char]
"Cannot resolve name"
         else
           [Char] -> Doc
PJ.text [Char]
"Cannot resolve name" 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]
: (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. PPrint a => a -> Doc
pprint [a]
alts)
        )

    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 -> Module -> Maybe Name -> LHName
makeLogicLHName Symbol
unqualifiedS (HasDebugCallStack => Name -> Module
Name -> Module
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 -> Module -> Maybe Name -> LHName
makeLogicLHName Symbol
unqualifiedS (HasDebugCallStack => Name -> Module
Name -> Module
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 -> Module -> Maybe Name -> LHName
makeLogicLHName Symbol
s (HasDebugCallStack => Name -> Module
Name -> Module
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 -> Module -> 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 -> Module
Name -> Module
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] -> Error
forall t. SrcSpan -> Doc -> [Doc] -> TError t
ErrDupNames
                 (LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
LH.fSrcSpan LocSymbol
s)
                 (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. (Eq 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
            -- TODO: The check for allEaliases should be redundant when
            -- ealiases are put in the logic environments
            if Symbol -> HashMap Symbol LMap -> Bool
forall k a. (Eq k, 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. (Eq a, Hashable a) => a -> HashSet a -> Bool
HS.member (Name -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Name
n) HashSet Symbol
allEaliases 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 -> Module -> 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 -> Module
Name -> Module
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] -> Error
forall t. SrcSpan -> Doc -> [Doc] -> TError t
ErrDupNames
                   (LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
LH.fSrcSpan LocSymbol
s)
                   (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
env 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 =>
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
symbolToLHName
        (Bool
-> ([Symbol] -> Symbol -> Identity LHName)
-> [Symbol]
-> BareType
-> Identity BareTypeLHName
forall (m :: * -> *) v1 v2.
Monad m =>
Bool
-> ([Symbol] -> v1 -> m v2)
-> [Symbol]
-> BareTypeV v1
-> m (BareTypeV v2)
emapBareTypeVM (Config -> Bool
bscope Config
cfg) [Symbol] -> Symbol -> Identity LHName
symbolToLHName)
        BareSpec
sp

    unhandledNames :: HashSet Symbol
unhandledNames = [Symbol] -> HashSet Symbol
forall a. (Eq 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

    symbolToLHName :: [Symbol] -> Symbol -> Identity LHName
    symbolToLHName :: [Symbol] -> Symbol -> Identity LHName
symbolToLHName [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 a. Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
s (LogicNameEnv -> SEnv LHName
lneLHName LogicNameEnv
env) of
          Maybe LHName
Nothing -> do
            Bool -> Identity () -> Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Symbol -> HashSet Symbol -> Bool
forall a. (Eq 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]
"toBareSpecLHName: 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