{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE TypeOperators #-}
module Language.Haskell.Liquid.Types.Names
  ( CompatibleBinder(..)
  , lenLocSymbol
  , anyTypeSymbol
  , propSymbol
  , getPropIndex
  , selfSymbol
  , tyTupleSizedSymbol
  , isTyTupleSizedSymbol
  , tmTupleSizedSymbol
  , LogicName (..)
  , LHResolvedName (..)
  , LHName (..)
  , LHNameSpace (..)
  , LHThisModuleNameFlag (..)
  , makeResolvedLHName
  , getLHGHCName
  , getLHNameResolved
  , getLHNameSymbol
  , lhNameToResolvedSymbol
  , lhNameToUnqualifiedSymbol
  , makeGHCLHName
  , makeGHCLHNameFromId
  , makeGHCLHNameLocated
  , makeGHCLHNameLocatedFromId
  , makeLocalLHName
  , makeLogicLHName
  , makeGeneratedLogicLHName
  , makeUnresolvedLHName
  , mapLHNames
  , mapMLocLHNames
  , maybeReflectedLHName
  , reflectGHCName
  , reflectLHName
  , updateLHNameSymbol
  , isNonReflectedLogicName
  , logicNameOriginModule
  , isResolvedLogicName
  , isGeneratedLogicName
  ) where

import Control.DeepSeq
import qualified Data.Binary as B
import Data.Data (Data, gmapM, gmapT)
import Data.Generics (extM, extT)
import Data.Hashable
import Data.Maybe (isNothing)
import Data.String (fromString)
import qualified Data.Text                               as Text
import GHC.Generics
import GHC.Show
import GHC.Stack
import Language.Fixpoint.Types
import Language.Haskell.Liquid.GHC.Misc ( locNamedThing ) -- Symbolic GHC.Name
import Text.Read (readMaybe)
import qualified Liquid.GHC.API as GHC

import GHC.Types (Any)

propSymbol :: Symbol
propSymbol :: Symbol
propSymbol = Symbol
"Language.Haskell.Liquid.ProofCombinators.prop"

getPropIndex :: ReftV Symbol -> Maybe (ExprV Symbol)
getPropIndex :: ReftV Symbol -> Maybe (ExprV Symbol)
getPropIndex (Reft (Symbol
v, PAtom Brel
Eq (EApp (EVar Symbol
n) (EVar Symbol
v')) ExprV Symbol
idx))
  | Symbol
n Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
propSymbol
  , Symbol
v Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
v'
  = ExprV Symbol -> Maybe (ExprV Symbol)
forall a. a -> Maybe a
Just ExprV Symbol
idx
getPropIndex ReftV Symbol
_ = Maybe (ExprV Symbol)
forall a. Maybe a
Nothing

-- | Highly temporary class as a compatability layer to express that a binder,
-- especially type variables @tv@, are in the same namespace as another binder.
class CompatibleBinder b b' where
  coerceBinder :: b' -> b
  default coerceBinder :: b ~ b' => b' -> b
  coerceBinder = b' -> b
b' -> b'
forall a. a -> a
id

instance CompatibleBinder Symbol Symbol
instance CompatibleBinder (Located Symbol) (Located Symbol)
instance CompatibleBinder Symbol (Located Symbol) where
  coerceBinder :: Located Symbol -> Symbol
coerceBinder (Loc SourcePos
_ SourcePos
_ Symbol
s) = Symbol
s

-- RJ: Please add docs
lenLocSymbol :: Located Symbol
lenLocSymbol :: Located Symbol
lenLocSymbol = Symbol -> Located Symbol
forall a. a -> Located a
dummyLoc (Symbol -> Located Symbol) -> Symbol -> Located Symbol
forall a b. (a -> b) -> a -> b
$ String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"autolen" :: String)

anyTypeSymbol :: Symbol
anyTypeSymbol :: Symbol
anyTypeSymbol = String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Name -> String
forall a. Show a => a -> String
show ''Any)

selfSymbol :: Symbol
selfSymbol :: Symbol
selfSymbol = String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"liquid_internal_this" :: String)

tyTupleSizedSymbol :: Int -> Symbol
tyTupleSizedSymbol :: Int -> Symbol
tyTupleSizedSymbol Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0     = String -> Symbol
forall a. HasCallStack => String -> a
error String
"tyTupleSizedSymbol: negative arity"
                     | Bool
otherwise = String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ String
"Tuple" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n

isTyTupleSizedSymbol :: Symbol -> Maybe Int
isTyTupleSizedSymbol :: Symbol -> Maybe Int
isTyTupleSizedSymbol Symbol
s = Text -> Text -> Maybe Text
Text.stripPrefix Text
"Tuple" (Symbol -> Text
symbolText Symbol
s)
                     Maybe Text -> (Text -> Maybe Int) -> Maybe Int
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe (String -> Maybe Int) -> (Text -> String) -> Text -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
Text.unpack

tmTupleSizedSymbol :: Int -> Symbol
tmTupleSizedSymbol :: Int -> Symbol
tmTupleSizedSymbol Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0     = String -> Symbol
forall a. HasCallStack => String -> a
error String
"tmTupleSizedSymbol: negative arity"
                     | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0    = Symbol
"()"
                     | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1    = Symbol
"MkSolo"
                     | Bool
otherwise = String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ String
"(" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Char
',' String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
")"

-- | A name for an entity that does not exist in Haskell
--
-- For instance, this can be used to represent predicate aliases
-- or uninterpreted functions.
data LogicName =
    LogicName
       -- | Unqualified symbol
      !Symbol
        -- | Module where the entity was defined
      !GHC.Module
        -- | If the named entity is the reflection of some Haskell name
      !(Maybe GHC.Name)
    | GeneratedLogicName Symbol
  deriving (Typeable LogicName
Typeable LogicName =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> LogicName -> c LogicName)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LogicName)
-> (LogicName -> Constr)
-> (LogicName -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LogicName))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LogicName))
-> ((forall b. Data b => b -> b) -> LogicName -> LogicName)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LogicName -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LogicName -> r)
-> (forall u. (forall d. Data d => d -> u) -> LogicName -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> LogicName -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LogicName -> m LogicName)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LogicName -> m LogicName)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LogicName -> m LogicName)
-> Data LogicName
LogicName -> Constr
LogicName -> DataType
(forall b. Data b => b -> b) -> LogicName -> LogicName
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> LogicName -> u
forall u. (forall d. Data d => d -> u) -> LogicName -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LogicName -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LogicName -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LogicName -> m LogicName
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LogicName -> m LogicName
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LogicName
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LogicName -> c LogicName
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LogicName)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LogicName)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LogicName -> c LogicName
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LogicName -> c LogicName
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LogicName
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LogicName
$ctoConstr :: LogicName -> Constr
toConstr :: LogicName -> Constr
$cdataTypeOf :: LogicName -> DataType
dataTypeOf :: LogicName -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LogicName)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LogicName)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LogicName)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LogicName)
$cgmapT :: (forall b. Data b => b -> b) -> LogicName -> LogicName
gmapT :: (forall b. Data b => b -> b) -> LogicName -> LogicName
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LogicName -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LogicName -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LogicName -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LogicName -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LogicName -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> LogicName -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LogicName -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LogicName -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LogicName -> m LogicName
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LogicName -> m LogicName
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LogicName -> m LogicName
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LogicName -> m LogicName
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LogicName -> m LogicName
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LogicName -> m LogicName
Data, LogicName -> LogicName -> Bool
(LogicName -> LogicName -> Bool)
-> (LogicName -> LogicName -> Bool) -> Eq LogicName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LogicName -> LogicName -> Bool
== :: LogicName -> LogicName -> Bool
$c/= :: LogicName -> LogicName -> Bool
/= :: LogicName -> LogicName -> Bool
Eq, (forall x. LogicName -> Rep LogicName x)
-> (forall x. Rep LogicName x -> LogicName) -> Generic LogicName
forall x. Rep LogicName x -> LogicName
forall x. LogicName -> Rep LogicName x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LogicName -> Rep LogicName x
from :: forall x. LogicName -> Rep LogicName x
$cto :: forall x. Rep LogicName x -> LogicName
to :: forall x. Rep LogicName x -> LogicName
Generic)

-- | A name whose procedence is known.
data LHResolvedName
    = LHRLogic !LogicName
    | LHRGHC !GHC.Name    -- ^ A name for an entity that exists in Haskell
    | LHRLocal !Symbol    -- ^ A name for a local variable, e.g. one that is
                          --   bound by a type alias.
    | -- | The index of a name in some environment
      --
      -- Before serializing names, they are converted to indices. The names
      -- themselves are kept in an environment or table that is serialized
      -- separately. This is to acommodate how GHC serializes its Names.
      LHRIndex Word
  deriving (Typeable LHResolvedName
Typeable LHResolvedName =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> LHResolvedName -> c LHResolvedName)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LHResolvedName)
-> (LHResolvedName -> Constr)
-> (LHResolvedName -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LHResolvedName))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c LHResolvedName))
-> ((forall b. Data b => b -> b)
    -> LHResolvedName -> LHResolvedName)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LHResolvedName -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LHResolvedName -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> LHResolvedName -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> LHResolvedName -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> LHResolvedName -> m LHResolvedName)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> LHResolvedName -> m LHResolvedName)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> LHResolvedName -> m LHResolvedName)
-> Data LHResolvedName
LHResolvedName -> Constr
LHResolvedName -> DataType
(forall b. Data b => b -> b) -> LHResolvedName -> LHResolvedName
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> LHResolvedName -> u
forall u. (forall d. Data d => d -> u) -> LHResolvedName -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LHResolvedName -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LHResolvedName -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> LHResolvedName -> m LHResolvedName
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LHResolvedName -> m LHResolvedName
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LHResolvedName
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LHResolvedName -> c LHResolvedName
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LHResolvedName)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LHResolvedName)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LHResolvedName -> c LHResolvedName
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LHResolvedName -> c LHResolvedName
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LHResolvedName
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LHResolvedName
$ctoConstr :: LHResolvedName -> Constr
toConstr :: LHResolvedName -> Constr
$cdataTypeOf :: LHResolvedName -> DataType
dataTypeOf :: LHResolvedName -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LHResolvedName)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LHResolvedName)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LHResolvedName)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LHResolvedName)
$cgmapT :: (forall b. Data b => b -> b) -> LHResolvedName -> LHResolvedName
gmapT :: (forall b. Data b => b -> b) -> LHResolvedName -> LHResolvedName
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LHResolvedName -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LHResolvedName -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LHResolvedName -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LHResolvedName -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LHResolvedName -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> LHResolvedName -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> LHResolvedName -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> LHResolvedName -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> LHResolvedName -> m LHResolvedName
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> LHResolvedName -> m LHResolvedName
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LHResolvedName -> m LHResolvedName
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LHResolvedName -> m LHResolvedName
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LHResolvedName -> m LHResolvedName
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LHResolvedName -> m LHResolvedName
Data, LHResolvedName -> LHResolvedName -> Bool
(LHResolvedName -> LHResolvedName -> Bool)
-> (LHResolvedName -> LHResolvedName -> Bool) -> Eq LHResolvedName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LHResolvedName -> LHResolvedName -> Bool
== :: LHResolvedName -> LHResolvedName -> Bool
$c/= :: LHResolvedName -> LHResolvedName -> Bool
/= :: LHResolvedName -> LHResolvedName -> Bool
Eq, (forall x. LHResolvedName -> Rep LHResolvedName x)
-> (forall x. Rep LHResolvedName x -> LHResolvedName)
-> Generic LHResolvedName
forall x. Rep LHResolvedName x -> LHResolvedName
forall x. LHResolvedName -> Rep LHResolvedName x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LHResolvedName -> Rep LHResolvedName x
from :: forall x. LHResolvedName -> Rep LHResolvedName x
$cto :: forall x. Rep LHResolvedName x -> LHResolvedName
to :: forall x. Rep LHResolvedName x -> LHResolvedName
Generic, Eq LHResolvedName
Eq LHResolvedName =>
(LHResolvedName -> LHResolvedName -> Ordering)
-> (LHResolvedName -> LHResolvedName -> Bool)
-> (LHResolvedName -> LHResolvedName -> Bool)
-> (LHResolvedName -> LHResolvedName -> Bool)
-> (LHResolvedName -> LHResolvedName -> Bool)
-> (LHResolvedName -> LHResolvedName -> LHResolvedName)
-> (LHResolvedName -> LHResolvedName -> LHResolvedName)
-> Ord LHResolvedName
LHResolvedName -> LHResolvedName -> Bool
LHResolvedName -> LHResolvedName -> Ordering
LHResolvedName -> LHResolvedName -> LHResolvedName
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: LHResolvedName -> LHResolvedName -> Ordering
compare :: LHResolvedName -> LHResolvedName -> Ordering
$c< :: LHResolvedName -> LHResolvedName -> Bool
< :: LHResolvedName -> LHResolvedName -> Bool
$c<= :: LHResolvedName -> LHResolvedName -> Bool
<= :: LHResolvedName -> LHResolvedName -> Bool
$c> :: LHResolvedName -> LHResolvedName -> Bool
> :: LHResolvedName -> LHResolvedName -> Bool
$c>= :: LHResolvedName -> LHResolvedName -> Bool
>= :: LHResolvedName -> LHResolvedName -> Bool
$cmax :: LHResolvedName -> LHResolvedName -> LHResolvedName
max :: LHResolvedName -> LHResolvedName -> LHResolvedName
$cmin :: LHResolvedName -> LHResolvedName -> LHResolvedName
min :: LHResolvedName -> LHResolvedName -> LHResolvedName
Ord)

-- | A name that is potentially unresolved, carrying along the 'Symbol'
-- found by the parser.
data LHName
    = -- | In order to integrate the resolved names gradually, we keep the
      -- unresolved names.
      LHNResolved !LHResolvedName !Symbol
    | LHNUnresolved !LHNameSpace !Symbol
  deriving (Typeable LHName
Typeable LHName =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> LHName -> c LHName)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LHName)
-> (LHName -> Constr)
-> (LHName -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LHName))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHName))
-> ((forall b. Data b => b -> b) -> LHName -> LHName)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LHName -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LHName -> r)
-> (forall u. (forall d. Data d => d -> u) -> LHName -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> LHName -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LHName -> m LHName)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LHName -> m LHName)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LHName -> m LHName)
-> Data LHName
LHName -> Constr
LHName -> DataType
(forall b. Data b => b -> b) -> LHName -> LHName
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> LHName -> u
forall u. (forall d. Data d => d -> u) -> LHName -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHName -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHName -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LHName -> m LHName
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LHName -> m LHName
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LHName
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LHName -> c LHName
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LHName)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHName)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LHName -> c LHName
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LHName -> c LHName
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LHName
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LHName
$ctoConstr :: LHName -> Constr
toConstr :: LHName -> Constr
$cdataTypeOf :: LHName -> DataType
dataTypeOf :: LHName -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LHName)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LHName)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHName)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHName)
$cgmapT :: (forall b. Data b => b -> b) -> LHName -> LHName
gmapT :: (forall b. Data b => b -> b) -> LHName -> LHName
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHName -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHName -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHName -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHName -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LHName -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> LHName -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LHName -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LHName -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LHName -> m LHName
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LHName -> m LHName
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LHName -> m LHName
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LHName -> m LHName
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LHName -> m LHName
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LHName -> m LHName
Data, (forall x. LHName -> Rep LHName x)
-> (forall x. Rep LHName x -> LHName) -> Generic LHName
forall x. Rep LHName x -> LHName
forall x. LHName -> Rep LHName x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LHName -> Rep LHName x
from :: forall x. LHName -> Rep LHName x
$cto :: forall x. Rep LHName x -> LHName
to :: forall x. Rep LHName x -> LHName
Generic)

-- | An Eq instance that ignores the Symbol in resolved names
instance Eq LHName where
  LHNResolved LHResolvedName
n0 Symbol
_ == :: LHName -> LHName -> Bool
== LHNResolved LHResolvedName
n1 Symbol
_ = LHResolvedName
n0 LHResolvedName -> LHResolvedName -> Bool
forall a. Eq a => a -> a -> Bool
== LHResolvedName
n1
  LHNUnresolved LHNameSpace
ns0 Symbol
s0 == LHNUnresolved LHNameSpace
ns1 Symbol
s1 = LHNameSpace
ns0 LHNameSpace -> LHNameSpace -> Bool
forall a. Eq a => a -> a -> Bool
== LHNameSpace
ns1 Bool -> Bool -> Bool
&& Symbol
s0 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
s1
  LHName
_ == LHName
_ = Bool
False

-- | An Ord instance that ignores the Symbol in resolved names
instance Ord LHName where
  compare :: LHName -> LHName -> Ordering
compare (LHNResolved LHResolvedName
n0 Symbol
_) (LHNResolved LHResolvedName
n1 Symbol
_) = LHResolvedName -> LHResolvedName -> Ordering
forall a. Ord a => a -> a -> Ordering
compare LHResolvedName
n0 LHResolvedName
n1
  compare (LHNUnresolved LHNameSpace
ns0 Symbol
s0) (LHNUnresolved LHNameSpace
ns1 Symbol
s1) =
    (LHNameSpace, Symbol) -> (LHNameSpace, Symbol) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (LHNameSpace
ns0, Symbol
s0) (LHNameSpace
ns1, Symbol
s1)
  compare LHNResolved{} LHName
_ = Ordering
LT
  compare LHNUnresolved{} LHName
_ = Ordering
GT

-- | A Hashable instance that ignores the Symbol in resolved names
instance Hashable LHName where
  hashWithSalt :: Int -> LHName -> Int
hashWithSalt Int
s (LHNResolved LHResolvedName
n Symbol
_) = Int -> LHResolvedName -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s LHResolvedName
n
  hashWithSalt Int
s (LHNUnresolved LHNameSpace
ns Symbol
sym) = Int
s Int -> LHNameSpace -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` LHNameSpace
ns Int -> Symbol -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Symbol
sym

data LHNameSpace
    = LHTcName LHThisModuleNameFlag       -- ^ Type constructors
    | LHDataConName LHThisModuleNameFlag  -- ^ Data constructors with procedence
    | LHVarName LHThisModuleNameFlag      -- ^ Variables with procedence
    | LHLogicNameBinder                   -- ^ Logic names (LHS)
    | LHLogicName                         -- ^ Logic names (RHS)
  deriving (Typeable LHNameSpace
Typeable LHNameSpace =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> LHNameSpace -> c LHNameSpace)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LHNameSpace)
-> (LHNameSpace -> Constr)
-> (LHNameSpace -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LHNameSpace))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c LHNameSpace))
-> ((forall b. Data b => b -> b) -> LHNameSpace -> LHNameSpace)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LHNameSpace -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LHNameSpace -> r)
-> (forall u. (forall d. Data d => d -> u) -> LHNameSpace -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> LHNameSpace -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LHNameSpace -> m LHNameSpace)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LHNameSpace -> m LHNameSpace)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LHNameSpace -> m LHNameSpace)
-> Data LHNameSpace
LHNameSpace -> Constr
LHNameSpace -> DataType
(forall b. Data b => b -> b) -> LHNameSpace -> LHNameSpace
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> LHNameSpace -> u
forall u. (forall d. Data d => d -> u) -> LHNameSpace -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LHNameSpace -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LHNameSpace -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LHNameSpace -> m LHNameSpace
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LHNameSpace -> m LHNameSpace
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LHNameSpace
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LHNameSpace -> c LHNameSpace
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LHNameSpace)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LHNameSpace)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LHNameSpace -> c LHNameSpace
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LHNameSpace -> c LHNameSpace
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LHNameSpace
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LHNameSpace
$ctoConstr :: LHNameSpace -> Constr
toConstr :: LHNameSpace -> Constr
$cdataTypeOf :: LHNameSpace -> DataType
dataTypeOf :: LHNameSpace -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LHNameSpace)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LHNameSpace)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LHNameSpace)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LHNameSpace)
$cgmapT :: (forall b. Data b => b -> b) -> LHNameSpace -> LHNameSpace
gmapT :: (forall b. Data b => b -> b) -> LHNameSpace -> LHNameSpace
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LHNameSpace -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LHNameSpace -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LHNameSpace -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LHNameSpace -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LHNameSpace -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> LHNameSpace -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LHNameSpace -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LHNameSpace -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LHNameSpace -> m LHNameSpace
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LHNameSpace -> m LHNameSpace
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LHNameSpace -> m LHNameSpace
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LHNameSpace -> m LHNameSpace
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LHNameSpace -> m LHNameSpace
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LHNameSpace -> m LHNameSpace
Data, LHNameSpace -> LHNameSpace -> Bool
(LHNameSpace -> LHNameSpace -> Bool)
-> (LHNameSpace -> LHNameSpace -> Bool) -> Eq LHNameSpace
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LHNameSpace -> LHNameSpace -> Bool
== :: LHNameSpace -> LHNameSpace -> Bool
$c/= :: LHNameSpace -> LHNameSpace -> Bool
/= :: LHNameSpace -> LHNameSpace -> Bool
Eq, (forall x. LHNameSpace -> Rep LHNameSpace x)
-> (forall x. Rep LHNameSpace x -> LHNameSpace)
-> Generic LHNameSpace
forall x. Rep LHNameSpace x -> LHNameSpace
forall x. LHNameSpace -> Rep LHNameSpace x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LHNameSpace -> Rep LHNameSpace x
from :: forall x. LHNameSpace -> Rep LHNameSpace x
$cto :: forall x. Rep LHNameSpace x -> LHNameSpace
to :: forall x. Rep LHNameSpace x -> LHNameSpace
Generic, Eq LHNameSpace
Eq LHNameSpace =>
(LHNameSpace -> LHNameSpace -> Ordering)
-> (LHNameSpace -> LHNameSpace -> Bool)
-> (LHNameSpace -> LHNameSpace -> Bool)
-> (LHNameSpace -> LHNameSpace -> Bool)
-> (LHNameSpace -> LHNameSpace -> Bool)
-> (LHNameSpace -> LHNameSpace -> LHNameSpace)
-> (LHNameSpace -> LHNameSpace -> LHNameSpace)
-> Ord LHNameSpace
LHNameSpace -> LHNameSpace -> Bool
LHNameSpace -> LHNameSpace -> Ordering
LHNameSpace -> LHNameSpace -> LHNameSpace
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: LHNameSpace -> LHNameSpace -> Ordering
compare :: LHNameSpace -> LHNameSpace -> Ordering
$c< :: LHNameSpace -> LHNameSpace -> Bool
< :: LHNameSpace -> LHNameSpace -> Bool
$c<= :: LHNameSpace -> LHNameSpace -> Bool
<= :: LHNameSpace -> LHNameSpace -> Bool
$c> :: LHNameSpace -> LHNameSpace -> Bool
> :: LHNameSpace -> LHNameSpace -> Bool
$c>= :: LHNameSpace -> LHNameSpace -> Bool
>= :: LHNameSpace -> LHNameSpace -> Bool
$cmax :: LHNameSpace -> LHNameSpace -> LHNameSpace
max :: LHNameSpace -> LHNameSpace -> LHNameSpace
$cmin :: LHNameSpace -> LHNameSpace -> LHNameSpace
min :: LHNameSpace -> LHNameSpace -> LHNameSpace
Ord, Int -> LHNameSpace -> String -> String
[LHNameSpace] -> String -> String
LHNameSpace -> String
(Int -> LHNameSpace -> String -> String)
-> (LHNameSpace -> String)
-> ([LHNameSpace] -> String -> String)
-> Show LHNameSpace
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> LHNameSpace -> String -> String
showsPrec :: Int -> LHNameSpace -> String -> String
$cshow :: LHNameSpace -> String
show :: LHNameSpace -> String
$cshowList :: [LHNameSpace] -> String -> String
showList :: [LHNameSpace] -> String -> String
Show)

instance B.Binary LHNameSpace
instance NFData LHNameSpace
instance Hashable LHNameSpace

-- | Whether the name should be looked up in the current module only or in any
-- module
data LHThisModuleNameFlag = LHThisModuleNameF | LHAnyModuleNameF
  deriving (Typeable LHThisModuleNameFlag
Typeable LHThisModuleNameFlag =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> LHThisModuleNameFlag
 -> c LHThisModuleNameFlag)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LHThisModuleNameFlag)
-> (LHThisModuleNameFlag -> Constr)
-> (LHThisModuleNameFlag -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LHThisModuleNameFlag))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c LHThisModuleNameFlag))
-> ((forall b. Data b => b -> b)
    -> LHThisModuleNameFlag -> LHThisModuleNameFlag)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LHThisModuleNameFlag -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LHThisModuleNameFlag -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> LHThisModuleNameFlag -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> LHThisModuleNameFlag -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> LHThisModuleNameFlag -> m LHThisModuleNameFlag)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> LHThisModuleNameFlag -> m LHThisModuleNameFlag)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> LHThisModuleNameFlag -> m LHThisModuleNameFlag)
-> Data LHThisModuleNameFlag
LHThisModuleNameFlag -> Constr
LHThisModuleNameFlag -> DataType
(forall b. Data b => b -> b)
-> LHThisModuleNameFlag -> LHThisModuleNameFlag
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> LHThisModuleNameFlag -> u
forall u.
(forall d. Data d => d -> u) -> LHThisModuleNameFlag -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LHThisModuleNameFlag -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LHThisModuleNameFlag -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> LHThisModuleNameFlag -> m LHThisModuleNameFlag
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LHThisModuleNameFlag -> m LHThisModuleNameFlag
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LHThisModuleNameFlag
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> LHThisModuleNameFlag
-> c LHThisModuleNameFlag
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LHThisModuleNameFlag)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LHThisModuleNameFlag)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> LHThisModuleNameFlag
-> c LHThisModuleNameFlag
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> LHThisModuleNameFlag
-> c LHThisModuleNameFlag
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LHThisModuleNameFlag
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LHThisModuleNameFlag
$ctoConstr :: LHThisModuleNameFlag -> Constr
toConstr :: LHThisModuleNameFlag -> Constr
$cdataTypeOf :: LHThisModuleNameFlag -> DataType
dataTypeOf :: LHThisModuleNameFlag -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LHThisModuleNameFlag)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LHThisModuleNameFlag)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LHThisModuleNameFlag)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LHThisModuleNameFlag)
$cgmapT :: (forall b. Data b => b -> b)
-> LHThisModuleNameFlag -> LHThisModuleNameFlag
gmapT :: (forall b. Data b => b -> b)
-> LHThisModuleNameFlag -> LHThisModuleNameFlag
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LHThisModuleNameFlag -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LHThisModuleNameFlag -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LHThisModuleNameFlag -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LHThisModuleNameFlag -> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> LHThisModuleNameFlag -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> LHThisModuleNameFlag -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> LHThisModuleNameFlag -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> LHThisModuleNameFlag -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> LHThisModuleNameFlag -> m LHThisModuleNameFlag
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> LHThisModuleNameFlag -> m LHThisModuleNameFlag
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LHThisModuleNameFlag -> m LHThisModuleNameFlag
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LHThisModuleNameFlag -> m LHThisModuleNameFlag
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LHThisModuleNameFlag -> m LHThisModuleNameFlag
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LHThisModuleNameFlag -> m LHThisModuleNameFlag
Data, LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool
(LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool)
-> (LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool)
-> Eq LHThisModuleNameFlag
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool
== :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool
$c/= :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool
/= :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool
Eq, (forall x. LHThisModuleNameFlag -> Rep LHThisModuleNameFlag x)
-> (forall x. Rep LHThisModuleNameFlag x -> LHThisModuleNameFlag)
-> Generic LHThisModuleNameFlag
forall x. Rep LHThisModuleNameFlag x -> LHThisModuleNameFlag
forall x. LHThisModuleNameFlag -> Rep LHThisModuleNameFlag x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LHThisModuleNameFlag -> Rep LHThisModuleNameFlag x
from :: forall x. LHThisModuleNameFlag -> Rep LHThisModuleNameFlag x
$cto :: forall x. Rep LHThisModuleNameFlag x -> LHThisModuleNameFlag
to :: forall x. Rep LHThisModuleNameFlag x -> LHThisModuleNameFlag
Generic, Eq LHThisModuleNameFlag
Eq LHThisModuleNameFlag =>
(LHThisModuleNameFlag -> LHThisModuleNameFlag -> Ordering)
-> (LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool)
-> (LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool)
-> (LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool)
-> (LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool)
-> (LHThisModuleNameFlag
    -> LHThisModuleNameFlag -> LHThisModuleNameFlag)
-> (LHThisModuleNameFlag
    -> LHThisModuleNameFlag -> LHThisModuleNameFlag)
-> Ord LHThisModuleNameFlag
LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool
LHThisModuleNameFlag -> LHThisModuleNameFlag -> Ordering
LHThisModuleNameFlag
-> LHThisModuleNameFlag -> LHThisModuleNameFlag
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Ordering
compare :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Ordering
$c< :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool
< :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool
$c<= :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool
<= :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool
$c> :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool
> :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool
$c>= :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool
>= :: LHThisModuleNameFlag -> LHThisModuleNameFlag -> Bool
$cmax :: LHThisModuleNameFlag
-> LHThisModuleNameFlag -> LHThisModuleNameFlag
max :: LHThisModuleNameFlag
-> LHThisModuleNameFlag -> LHThisModuleNameFlag
$cmin :: LHThisModuleNameFlag
-> LHThisModuleNameFlag -> LHThisModuleNameFlag
min :: LHThisModuleNameFlag
-> LHThisModuleNameFlag -> LHThisModuleNameFlag
Ord, Int -> LHThisModuleNameFlag -> String -> String
[LHThisModuleNameFlag] -> String -> String
LHThisModuleNameFlag -> String
(Int -> LHThisModuleNameFlag -> String -> String)
-> (LHThisModuleNameFlag -> String)
-> ([LHThisModuleNameFlag] -> String -> String)
-> Show LHThisModuleNameFlag
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> LHThisModuleNameFlag -> String -> String
showsPrec :: Int -> LHThisModuleNameFlag -> String -> String
$cshow :: LHThisModuleNameFlag -> String
show :: LHThisModuleNameFlag -> String
$cshowList :: [LHThisModuleNameFlag] -> String -> String
showList :: [LHThisModuleNameFlag] -> String -> String
Show)

instance B.Binary LHThisModuleNameFlag
instance NFData LHThisModuleNameFlag
instance Hashable LHThisModuleNameFlag

instance Ord LogicName where
  compare :: LogicName -> LogicName -> Ordering
compare (LogicName Symbol
s1 GenModule Unit
m1 Maybe Name
_) (LogicName Symbol
s2 GenModule Unit
m2 Maybe Name
_) =
    case Symbol -> Symbol -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Symbol
s1 Symbol
s2 of
      Ordering
EQ -> GenModule Unit -> GenModule Unit -> Ordering
GHC.stableModuleCmp GenModule Unit
m1 GenModule Unit
m2
      Ordering
x -> Ordering
x
  compare LogicName{} GeneratedLogicName{} = Ordering
LT
  compare GeneratedLogicName{} LogicName{} = Ordering
GT
  compare (GeneratedLogicName Symbol
s1) (GeneratedLogicName Symbol
s2) = Symbol -> Symbol -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Symbol
s1 Symbol
s2

instance Show LHName where
  showsPrec :: Int -> LHName -> String -> String
showsPrec Int
d LHName
n0 = Bool -> (String -> String) -> String -> String
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
app_prec) ((String -> String) -> String -> String)
-> (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ case LHName
n0 of
      LHNResolved LHResolvedName
n Symbol
s ->
        String -> String -> String
showString String
"LHNResolved " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        Int -> LHResolvedName -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec (Int
app_prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) LHResolvedName
n (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        String -> String
showSpace (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        Int -> Symbol -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec (Int
app_prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Symbol
s
      LHNUnresolved LHNameSpace
ns Symbol
s ->
        String -> String -> String
showString String
"LHNUnresolved " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        Int -> LHNameSpace -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec (Int
app_prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) LHNameSpace
ns (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        String -> String
showSpace (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        Int -> Symbol -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec (Int
app_prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Symbol
s
    where
      app_prec :: Int
app_prec = Int
10

instance Show LHResolvedName where
  showsPrec :: Int -> LHResolvedName -> String -> String
showsPrec Int
d LHResolvedName
n0 = Bool -> (String -> String) -> String -> String
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
app_prec) ((String -> String) -> String -> String)
-> (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ case LHResolvedName
n0 of
      LHRGHC Name
n1 -> String -> String -> String
showString String
"LHRGHC " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString (Name -> String
forall a. Outputable a => a -> String
GHC.showPprDebug Name
n1)
      LHRLogic LogicName
n1 -> String -> String -> String
showString String
"LHRLogic " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> LogicName -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec (Int
app_prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) LogicName
n1
      LHRLocal Symbol
n1 -> String -> String -> String
showString String
"LHRLocal " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Symbol -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec (Int
app_prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Symbol
n1
      LHRIndex Word
i -> String -> String -> String
showString String
"LHRIndex " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Word -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec (Int
app_prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Word
i
    where
      app_prec :: Int
app_prec = Int
10

instance Show LogicName where
  showsPrec :: Int -> LogicName -> String -> String
showsPrec Int
d LogicName
n0 = Bool -> (String -> String) -> String -> String
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
app_prec) ((String -> String) -> String -> String)
-> (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ case LogicName
n0 of
      LogicName Symbol
s1 GenModule Unit
m Maybe Name
mr ->
        String -> String -> String
showString String
"LogicName " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        Int -> Symbol -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec (Int
app_prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Symbol
s1 (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        String -> String
showSpace (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        String -> String -> String
showString (GenModule Unit -> String
forall a. Outputable a => a -> String
GHC.showPprDebug GenModule Unit
m) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        String -> String
showSpace (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        Maybe Name -> String -> String
forall {a}. Outputable a => Maybe a -> String -> String
showsPrecMaybeName Maybe Name
mr
      GeneratedLogicName Symbol
s1 ->
        String -> String -> String
showString String
"GeneratedLogicName " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        Int -> Symbol -> String -> String
forall a. Show a => Int -> a -> String -> String
showsPrec (Int
app_prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Symbol
s1
    where
      app_prec :: Int
app_prec = Int
10

      showsPrecMaybeName :: Maybe a -> String -> String
showsPrecMaybeName Maybe a
mr = case Maybe a
mr of
        Maybe a
Nothing -> String -> String -> String
showString String
"Nothing"
        Just a
n -> Bool -> (String -> String) -> String -> String
showParen Bool
True ((String -> String) -> String -> String)
-> (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> String
showString String
"Just " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString (a -> String
forall a. Outputable a => a -> String
GHC.showPprDebug a
n)

instance NFData LHName
instance NFData LHResolvedName
instance NFData LogicName

instance Hashable LHResolvedName where
  hashWithSalt :: Int -> LHResolvedName -> Int
hashWithSalt Int
s (LHRLogic LogicName
n) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0::Int) Int -> LogicName -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` LogicName
n
  hashWithSalt Int
s (LHRGHC Name
n) =
    Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1::Int) Int -> Word64 -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Unique -> Word64
GHC.getKey (Name -> Unique
GHC.nameUnique Name
n)
  hashWithSalt Int
s (LHRLocal Symbol
n) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
2::Int) Int -> Symbol -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Symbol
n
  hashWithSalt Int
s (LHRIndex Word
w) = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
3::Int) Int -> Word -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Word
w

instance Hashable LogicName where
  hashWithSalt :: Int -> LogicName -> Int
hashWithSalt Int
s (LogicName Symbol
sym GenModule Unit
m Maybe Name
_) =
        Int
s Int -> Symbol -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Symbol
sym
          Int -> String -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` GenModule Unit -> String
GHC.moduleStableString GenModule Unit
m
  hashWithSalt Int
s (GeneratedLogicName Symbol
sym) =
        Int
s Int -> Symbol -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Symbol
sym

instance B.Binary LHName
instance B.Binary LHResolvedName where
  get :: Get LHResolvedName
get = do
    tag <- Get Word8
B.getWord8
    case tag of
      Word8
0 -> Symbol -> LHResolvedName
LHRLocal (Symbol -> LHResolvedName)
-> (String -> Symbol) -> String -> LHResolvedName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Symbol
forall a. IsString a => String -> a
fromString (String -> LHResolvedName) -> Get String -> Get LHResolvedName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get String
forall t. Binary t => Get t
B.get
      Word8
1 -> Word -> LHResolvedName
LHRIndex (Word -> LHResolvedName) -> Get Word -> Get LHResolvedName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get Word
forall t. Binary t => Get t
B.get
      Word8
_ -> String -> Get LHResolvedName
forall a. HasCallStack => String -> a
error String
"B.Binary: invalid tag for LHResolvedName"
  put :: LHResolvedName -> Put
put (LHRLogic LogicName
_n) = String -> Put
forall a. HasCallStack => String -> a
error String
"cannot serialize LHRLogic"
  put (LHRGHC Name
_n) = String -> Put
forall a. HasCallStack => String -> a
error String
"cannot serialize LHRGHC"
  put (LHRLocal Symbol
s) = Word8 -> Put
B.putWord8 Word8
0 Put -> Put -> Put
forall a b. PutM a -> PutM b -> PutM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Put
forall t. Binary t => t -> Put
B.put (Symbol -> String
symbolString Symbol
s)
  put (LHRIndex Word
n) = Word8 -> Put
B.putWord8 Word8
1 Put -> Put -> Put
forall a b. PutM a -> PutM b -> PutM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Word -> Put
forall t. Binary t => t -> Put
B.put Word
n

instance GHC.Binary LHResolvedName where
  get :: ReadBinHandle -> IO LHResolvedName
get ReadBinHandle
bh = do
    tag <- ReadBinHandle -> IO Word8
GHC.getByte ReadBinHandle
bh
    case tag of
      Word8
0 -> LogicName -> LHResolvedName
LHRLogic (LogicName -> LHResolvedName) -> IO LogicName -> IO LHResolvedName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadBinHandle -> IO LogicName
forall a. Binary a => ReadBinHandle -> IO a
GHC.get ReadBinHandle
bh
      Word8
1 -> Name -> LHResolvedName
LHRGHC (Name -> LHResolvedName) -> IO Name -> IO LHResolvedName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadBinHandle -> IO Name
forall a. Binary a => ReadBinHandle -> IO a
GHC.get ReadBinHandle
bh
      Word8
2 -> Symbol -> LHResolvedName
LHRLocal (Symbol -> LHResolvedName)
-> (String -> Symbol) -> String -> LHResolvedName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Symbol
forall a. IsString a => String -> a
fromString (String -> LHResolvedName) -> IO String -> IO LHResolvedName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadBinHandle -> IO String
forall a. Binary a => ReadBinHandle -> IO a
GHC.get ReadBinHandle
bh
      Word8
_ -> String -> IO LHResolvedName
forall a. HasCallStack => String -> a
error String
"GHC.Binary: invalid tag for LHResolvedName"
  put_ :: WriteBinHandle -> LHResolvedName -> IO ()
put_ WriteBinHandle
bh (LHRLogic LogicName
n) = WriteBinHandle -> Word8 -> IO ()
GHC.putByte WriteBinHandle
bh Word8
0 IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> WriteBinHandle -> LogicName -> IO ()
forall a. Binary a => WriteBinHandle -> a -> IO ()
GHC.put_ WriteBinHandle
bh LogicName
n
  put_ WriteBinHandle
bh (LHRGHC Name
n) = WriteBinHandle -> Word8 -> IO ()
GHC.putByte WriteBinHandle
bh Word8
1 IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> WriteBinHandle -> Name -> IO ()
forall a. Binary a => WriteBinHandle -> a -> IO ()
GHC.put_ WriteBinHandle
bh Name
n
  put_ WriteBinHandle
bh (LHRLocal Symbol
n) = WriteBinHandle -> Word8 -> IO ()
GHC.putByte WriteBinHandle
bh Word8
2 IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> WriteBinHandle -> String -> IO ()
forall a. Binary a => WriteBinHandle -> a -> IO ()
GHC.put_ WriteBinHandle
bh (Symbol -> String
symbolString Symbol
n)
  put_ WriteBinHandle
_bh (LHRIndex Word
_n) = String -> IO ()
forall a. HasCallStack => String -> a
error String
"GHC.Binary: cannot serialize LHRIndex"

instance GHC.Binary LogicName where
  get :: ReadBinHandle -> IO LogicName
get ReadBinHandle
bh = do
    tag <- ReadBinHandle -> IO Word8
GHC.getByte ReadBinHandle
bh
    case tag of
      Word8
0 -> Symbol -> GenModule Unit -> Maybe Name -> LogicName
LogicName (Symbol -> GenModule Unit -> Maybe Name -> LogicName)
-> (String -> Symbol)
-> String
-> GenModule Unit
-> Maybe Name
-> LogicName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Symbol
forall a. IsString a => String -> a
fromString (String -> GenModule Unit -> Maybe Name -> LogicName)
-> IO String -> IO (GenModule Unit -> Maybe Name -> LogicName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadBinHandle -> IO String
forall a. Binary a => ReadBinHandle -> IO a
GHC.get ReadBinHandle
bh IO (GenModule Unit -> Maybe Name -> LogicName)
-> IO (GenModule Unit) -> IO (Maybe Name -> LogicName)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadBinHandle -> IO (GenModule Unit)
forall a. Binary a => ReadBinHandle -> IO a
GHC.get ReadBinHandle
bh IO (Maybe Name -> LogicName) -> IO (Maybe Name) -> IO LogicName
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadBinHandle -> IO (Maybe Name)
forall a. Binary a => ReadBinHandle -> IO a
GHC.get ReadBinHandle
bh
      Word8
1 -> Symbol -> LogicName
GeneratedLogicName (Symbol -> LogicName) -> (String -> Symbol) -> String -> LogicName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Symbol
forall a. IsString a => String -> a
fromString (String -> LogicName) -> IO String -> IO LogicName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadBinHandle -> IO String
forall a. Binary a => ReadBinHandle -> IO a
GHC.get ReadBinHandle
bh
      Word8
_ -> String -> IO LogicName
forall a. HasCallStack => String -> a
error String
"GHC.Binary: invalid tag for LogicName"
  put_ :: WriteBinHandle -> LogicName -> IO ()
put_ WriteBinHandle
bh (LogicName Symbol
s GenModule Unit
m Maybe Name
r) = do
    WriteBinHandle -> Word8 -> IO ()
GHC.putByte WriteBinHandle
bh Word8
0
    WriteBinHandle -> String -> IO ()
forall a. Binary a => WriteBinHandle -> a -> IO ()
GHC.put_ WriteBinHandle
bh (Symbol -> String
symbolString Symbol
s) IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> WriteBinHandle -> GenModule Unit -> IO ()
forall a. Binary a => WriteBinHandle -> a -> IO ()
GHC.put_ WriteBinHandle
bh GenModule Unit
m IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> WriteBinHandle -> Maybe Name -> IO ()
forall a. Binary a => WriteBinHandle -> a -> IO ()
GHC.put_ WriteBinHandle
bh Maybe Name
r
  put_ WriteBinHandle
bh (GeneratedLogicName Symbol
s) = do
    WriteBinHandle -> Word8 -> IO ()
GHC.putByte WriteBinHandle
bh Word8
1
    WriteBinHandle -> String -> IO ()
forall a. Binary a => WriteBinHandle -> a -> IO ()
GHC.put_ WriteBinHandle
bh (Symbol -> String
symbolString Symbol
s)

instance PPrint LHName where
  pprintTidy :: Tidy -> LHName -> Doc
pprintTidy Tidy
_ = Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (Symbol -> Doc) -> (LHName -> Symbol) -> LHName -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LHName -> Symbol
getLHNameSymbol

makeResolvedLHName :: LHResolvedName -> Symbol -> LHName
makeResolvedLHName :: LHResolvedName -> Symbol -> LHName
makeResolvedLHName = LHResolvedName -> Symbol -> LHName
LHNResolved

makeGHCLHName :: GHC.Name -> Symbol -> LHName
makeGHCLHName :: Name -> Symbol -> LHName
makeGHCLHName Name
n Symbol
s = LHResolvedName -> Symbol -> LHName
makeResolvedLHName (Name -> LHResolvedName
LHRGHC Name
n) Symbol
s

makeGHCLHNameFromId :: GHC.Id -> LHName
makeGHCLHNameFromId :: Var -> LHName
makeGHCLHNameFromId Var
x =
    let n :: Name
n = case HasCallStack => Var -> IdDetails
Var -> IdDetails
GHC.idDetails Var
x of
              GHC.DataConWrapId DataCon
dc -> DataCon -> Name
forall a. NamedThing a => a -> Name
GHC.getName DataCon
dc
              GHC.DataConWorkId DataCon
dc -> DataCon -> Name
forall a. NamedThing a => a -> Name
GHC.getName DataCon
dc
              IdDetails
_ -> Var -> Name
forall a. NamedThing a => a -> Name
GHC.getName Var
x
     in Name -> Symbol -> LHName
makeGHCLHName Name
n (Name -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Name
n)

makeLocalLHName :: Symbol -> LHName
makeLocalLHName :: Symbol -> LHName
makeLocalLHName Symbol
s = LHResolvedName -> Symbol -> LHName
LHNResolved (Symbol -> LHResolvedName
LHRLocal Symbol
s) Symbol
s

makeLogicLHName :: Symbol -> GHC.Module -> Maybe GHC.Name -> LHName
makeLogicLHName :: Symbol -> GenModule Unit -> Maybe Name -> LHName
makeLogicLHName Symbol
s GenModule Unit
m Maybe Name
r = LHResolvedName -> Symbol -> LHName
LHNResolved (LogicName -> LHResolvedName
LHRLogic (Symbol -> GenModule Unit -> Maybe Name -> LogicName
LogicName Symbol
s GenModule Unit
m Maybe Name
r)) Symbol
s

makeGeneratedLogicLHName :: Symbol -> LHName
makeGeneratedLogicLHName :: Symbol -> LHName
makeGeneratedLogicLHName Symbol
s = LHResolvedName -> Symbol -> LHName
LHNResolved (LogicName -> LHResolvedName
LHRLogic (Symbol -> LogicName
GeneratedLogicName Symbol
s)) Symbol
s

makeGHCLHNameLocated :: (GHC.NamedThing a, Symbolic a) => a -> Located LHName
makeGHCLHNameLocated :: forall a. (NamedThing a, Symbolic a) => a -> Located LHName
makeGHCLHNameLocated a
x =
    Name -> Symbol -> LHName
makeGHCLHName (a -> Name
forall a. NamedThing a => a -> Name
GHC.getName a
x) (a -> Symbol
forall a. Symbolic a => a -> Symbol
symbol a
x) LHName -> Located a -> Located LHName
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ a -> Located a
forall a. NamedThing a => a -> Located a
locNamedThing a
x

makeGHCLHNameLocatedFromId :: GHC.Id -> Located LHName
makeGHCLHNameLocatedFromId :: Var -> Located LHName
makeGHCLHNameLocatedFromId Var
x =
    case HasCallStack => Var -> IdDetails
Var -> IdDetails
GHC.idDetails Var
x of
      GHC.DataConWrapId DataCon
dc -> Name -> Located LHName
forall a. (NamedThing a, Symbolic a) => a -> Located LHName
makeGHCLHNameLocated (DataCon -> Name
forall a. NamedThing a => a -> Name
GHC.getName DataCon
dc)
      GHC.DataConWorkId DataCon
dc -> Name -> Located LHName
forall a. (NamedThing a, Symbolic a) => a -> Located LHName
makeGHCLHNameLocated (DataCon -> Name
forall a. NamedThing a => a -> Name
GHC.getName DataCon
dc)
      IdDetails
_ -> Var -> Located LHName
forall a. (NamedThing a, Symbolic a) => a -> Located LHName
makeGHCLHNameLocated Var
x

makeUnresolvedLHName :: LHNameSpace -> Symbol -> LHName
makeUnresolvedLHName :: LHNameSpace -> Symbol -> LHName
makeUnresolvedLHName = LHNameSpace -> Symbol -> LHName
LHNUnresolved

-- | Get the unresolved Symbol from an LHName.
getLHNameSymbol :: LHName -> Symbol
getLHNameSymbol :: LHName -> Symbol
getLHNameSymbol (LHNResolved LHResolvedName
_ Symbol
s) = Symbol
s
getLHNameSymbol (LHNUnresolved LHNameSpace
_ Symbol
s) = Symbol
s

-- | Get the resolved Symbol from an LHName.
getLHNameResolved :: HasCallStack => LHName -> LHResolvedName
getLHNameResolved :: HasCallStack => LHName -> LHResolvedName
getLHNameResolved (LHNResolved LHResolvedName
n Symbol
_) = LHResolvedName
n
getLHNameResolved n :: LHName
n@LHNUnresolved{} = String -> LHResolvedName
forall a. HasCallStack => String -> a
error (String -> LHResolvedName) -> String -> LHResolvedName
forall a b. (a -> b) -> a -> b
$ String
"getLHNameResolved: unresolved name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LHName -> String
forall a. Show a => a -> String
show LHName
n

getLHGHCName :: LHName -> Maybe GHC.Name
getLHGHCName :: LHName -> Maybe Name
getLHGHCName (LHNResolved (LHRGHC Name
n) Symbol
_) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n
getLHGHCName LHName
_ = Maybe Name
forall a. Maybe a
Nothing

mapLHNames :: Data a => (LHName -> LHName) -> a -> a
mapLHNames :: forall a. Data a => (LHName -> LHName) -> a -> a
mapLHNames LHName -> LHName
f = a -> a
forall b. Data b => b -> b
go
  where
    go :: Data a => a -> a
    go :: forall b. Data b => b -> b
go = (forall b. Data b => b -> b) -> a -> a
forall a. Data a => (forall b. Data b => b -> b) -> a -> a
gmapT (b -> b
forall b. Data b => b -> b
go (b -> b) -> (LHName -> LHName) -> b -> b
forall a b.
(Typeable a, Typeable b) =>
(a -> a) -> (b -> b) -> a -> a
`extT` LHName -> LHName
f)

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

updateLHNameSymbol :: (Symbol -> Symbol) -> LHName -> LHName
updateLHNameSymbol :: (Symbol -> Symbol) -> LHName -> LHName
updateLHNameSymbol Symbol -> Symbol
f (LHNResolved LHResolvedName
n Symbol
s) = LHResolvedName -> Symbol -> LHName
LHNResolved LHResolvedName
n (Symbol -> Symbol
f Symbol
s)
updateLHNameSymbol Symbol -> Symbol
f (LHNUnresolved LHNameSpace
n Symbol
s) = LHNameSpace -> Symbol -> LHName
LHNUnresolved LHNameSpace
n (Symbol -> Symbol
f Symbol
s)

-- | Converts resolved names to symbols.
--
-- One important postcondition of this function is that the symbol for reflected
-- names must match exactly the symbol for the corresponding Haskell function.
-- Otherwise, LH would fail to link the two at various places where it is needed.
lhNameToResolvedSymbol :: LHName -> Symbol
lhNameToResolvedSymbol :: LHName -> Symbol
lhNameToResolvedSymbol (LHNResolved (LHRLogic (LogicName Symbol
s GenModule Unit
om Maybe Name
mReflectionOf)) Symbol
_) =
    let m :: GenModule Unit
m = GenModule Unit
-> (Name -> GenModule Unit) -> Maybe Name -> GenModule Unit
forall b a. b -> (a -> b) -> Maybe a -> b
maybe GenModule Unit
om HasDebugCallStack => Name -> GenModule Unit
Name -> GenModule Unit
GHC.nameModule Maybe Name
mReflectionOf
        msymbol :: Text
msymbol = String -> Text
Text.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ ModuleName -> String
GHC.moduleNameString (ModuleName -> String) -> ModuleName -> String
forall a b. (a -> b) -> a -> b
$ GenModule Unit -> ModuleName
forall unit. GenModule unit -> ModuleName
GHC.moduleName GenModule Unit
m
     in Text -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Text -> Symbol) -> Text -> Symbol
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat [Text
msymbol, Text
".", Symbol -> Text
symbolText Symbol
s]
        {-
        TODO: Adding a prefix for the unit would allow LH to deal with
              -XPackageImports. This prefix should be added here and in
              the Symbolic instance of Name.
        munique =
          Text.dropEnd 2 $ -- Remove padding of two characters "=="
          Base64.extractBase64 $
          Base64.encodeBase64 $
          ByteString.toStrict $
          Builder.toLazyByteString $
          Builder.int32BE $
          fromIntegral $
          hash $
          GHC.unitIdString $
          GHC.moduleUnitId m
     in symbol $ mconcat ["u", munique, "##", msymbol, ".", symbolText s]
          -}
lhNameToResolvedSymbol (LHNResolved (LHRLogic (GeneratedLogicName Symbol
s)) Symbol
_) = Symbol
s
lhNameToResolvedSymbol (LHNResolved (LHRLocal Symbol
s) Symbol
_) = Symbol
s
lhNameToResolvedSymbol (LHNResolved (LHRGHC Name
n) Symbol
_) = Name -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Name
n
lhNameToResolvedSymbol LHName
n = String -> Symbol
forall a. HasCallStack => String -> a
error (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ String
"lhNameToResolvedSymbol: unexpected name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LHName -> String
forall a. Show a => a -> String
show LHName
n

lhNameToUnqualifiedSymbol :: HasCallStack => LHName -> Symbol
lhNameToUnqualifiedSymbol :: HasCallStack => LHName -> Symbol
lhNameToUnqualifiedSymbol (LHNResolved (LHRLogic (LogicName Symbol
s GenModule Unit
_ Maybe Name
_)) Symbol
_) = Symbol
s
lhNameToUnqualifiedSymbol (LHNResolved (LHRLogic (GeneratedLogicName Symbol
s)) Symbol
_) = Symbol
s
lhNameToUnqualifiedSymbol (LHNResolved (LHRLocal Symbol
s) Symbol
_) = Symbol
s
lhNameToUnqualifiedSymbol (LHNResolved (LHRGHC Name
n) Symbol
_) = String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. NamedThing a => a -> String
GHC.getOccString Name
n
lhNameToUnqualifiedSymbol LHName
n = String -> Symbol
forall a. HasCallStack => String -> a
error (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ String
"lhNameToUnqualifiedSymbol: unexpected name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LHName -> String
forall a. Show a => a -> String
show LHName
n

-- | Creates a name in the logic namespace for the given Haskell name.
reflectLHName :: HasCallStack => GHC.Module -> LHName -> LHName
reflectLHName :: HasCallStack => GenModule Unit -> LHName -> LHName
reflectLHName GenModule Unit
thisModule (LHNResolved (LHRGHC Name
n) Symbol
_) = GenModule Unit -> Name -> LHName
reflectGHCName GenModule Unit
thisModule Name
n
reflectLHName GenModule Unit
_ LHName
n = String -> LHName
forall a. HasCallStack => String -> a
error (String -> LHName) -> String -> LHName
forall a b. (a -> b) -> a -> b
$ String
"not a GHC Name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LHName -> String
forall a. Show a => a -> String
show LHName
n

-- | Creates a name in the logic namespace for the given Haskell name.
reflectGHCName :: GHC.Module -> GHC.Name -> LHName
reflectGHCName :: GenModule Unit -> Name -> LHName
reflectGHCName GenModule Unit
thisModule Name
n =
    LHResolvedName -> Symbol -> LHName
LHNResolved
      (LogicName -> LHResolvedName
LHRLogic
        (Symbol -> GenModule Unit -> Maybe Name -> LogicName
LogicName
          (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (OccName -> String
GHC.occNameString (OccName -> String) -> OccName -> String
forall a b. (a -> b) -> a -> b
$ Name -> OccName
GHC.nameOccName Name
n))
          GenModule Unit
thisModule
          (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n)
        )
      )
      (Name -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Name
n)

isNonReflectedLogicName :: LHName -> Bool
isNonReflectedLogicName :: LHName -> Bool
isNonReflectedLogicName LHName
lhname = LHName -> Bool
isResolvedLogicName LHName
lhname Bool -> Bool -> Bool
&& (Maybe Name -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe Name -> Bool) -> (LHName -> Maybe Name) -> LHName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LHName -> Maybe Name
maybeReflectedLHName) LHName
lhname

maybeReflectedLHName :: LHName -> Maybe GHC.Name
maybeReflectedLHName :: LHName -> Maybe Name
maybeReflectedLHName (LHNResolved (LHRLogic (LogicName Symbol
_ GenModule Unit
_ Maybe Name
m)) Symbol
_) = Maybe Name
m
maybeReflectedLHName LHName
_ = Maybe Name
forall a. Maybe a
Nothing

isResolvedLogicName :: LHName -> Bool
isResolvedLogicName :: LHName -> Bool
isResolvedLogicName (LHNResolved (LHRLogic (LogicName {})) Symbol
_) = Bool
True
isResolvedLogicName LHName
_ = Bool
False

isGeneratedLogicName :: LHName -> Bool
isGeneratedLogicName :: LHName -> Bool
isGeneratedLogicName (LHNResolved (LHRLogic (GeneratedLogicName Symbol
_)) Symbol
_) = Bool
True
isGeneratedLogicName LHName
_ = Bool
False

logicNameOriginModule :: LHName -> GHC.Module
logicNameOriginModule :: LHName -> GenModule Unit
logicNameOriginModule (LHNResolved (LHRLogic (LogicName Symbol
_ GenModule Unit
m Maybe Name
_)) Symbol
_) = GenModule Unit
m
logicNameOriginModule LHName
n = String -> GenModule Unit
forall a. HasCallStack => String -> a
error (String -> GenModule Unit) -> String -> GenModule Unit
forall a b. (a -> b) -> a -> b
$ String
"logicNameOriginModule: Not a logic name " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LHName -> String
forall a. Show a => a -> String
show LHName
n