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

module Language.Haskell.Liquid.Bare.Types 
  ( -- * Name resolution environment 
    Env (..)
  , GHCTyLookupEnv (..)
  , TyThingMap 
  , ModSpecs
  , LocalVars(..)
  , LocalVarDetails (..)

    -- * Tycon and Datacon processing environment
  , TycEnv (..) 
  , DataConMap
  , RT.TyConMap

    -- * Signature processing environment 
  , SigEnv (..)

    -- * Measure related environment 
  , MeasEnv (..)

    -- * Misc 
  , PlugTV (..)
  , plugSrc
  , varRSort 
  , varSortedReft
  , failMaybe
  ) where 

import qualified Text.PrettyPrint.HughesPJ             as PJ 
import qualified Data.HashSet                          as S
import qualified Data.HashMap.Strict                   as M
import qualified Language.Fixpoint.Types               as F 
import qualified Language.Haskell.Liquid.Measure       as Ms
import           Language.Haskell.Liquid.Types.DataDecl
import           Language.Haskell.Liquid.Types.Names
import qualified Language.Haskell.Liquid.Types.RefType as RT 
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.Types.Specs   hiding (BareSpec)
import           Liquid.GHC.API       as Ghc hiding (Located, Env)
import           Language.Haskell.Liquid.GHC.Types     (StableName)
import           Language.Haskell.Liquid.UX.Config


type ModSpecs = M.HashMap ModName Ms.BareSpec

-------------------------------------------------------------------------------
-- | See [NOTE: Plug-Holes-TyVars] for a rationale for @PlugTV@ 
-------------------------------------------------------------------------------

data PlugTV v 
  = HsTV v  -- ^ Use tyvars from GHC specification (in the `v`) 
  | LqTV v  -- ^ Use tyvars from Liquid specification
  | GenTV   -- ^ Generalize ty-vars 
  | RawTV   -- ^ Do NOT generalize ty-vars (e.g. for type-aliases)
  deriving (Int -> PlugTV v -> ShowS
[PlugTV v] -> ShowS
PlugTV v -> String
(Int -> PlugTV v -> ShowS)
-> (PlugTV v -> String) -> ([PlugTV v] -> ShowS) -> Show (PlugTV v)
forall v. Show v => Int -> PlugTV v -> ShowS
forall v. Show v => [PlugTV v] -> ShowS
forall v. Show v => PlugTV v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall v. Show v => Int -> PlugTV v -> ShowS
showsPrec :: Int -> PlugTV v -> ShowS
$cshow :: forall v. Show v => PlugTV v -> String
show :: PlugTV v -> String
$cshowList :: forall v. Show v => [PlugTV v] -> ShowS
showList :: [PlugTV v] -> ShowS
Show)


instance (Show v, F.PPrint v) => F.PPrint (PlugTV v) where 
  pprintTidy :: Tidy -> PlugTV v -> Doc
pprintTidy Tidy
_ = String -> Doc
PJ.text (String -> Doc) -> (PlugTV v -> String) -> PlugTV v -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PlugTV v -> String
forall a. Show a => a -> String
show 
   
plugSrc ::  PlugTV v -> Maybe v 
plugSrc :: forall v. PlugTV v -> Maybe v
plugSrc (HsTV v
v) = v -> Maybe v
forall a. a -> Maybe a
Just v
v 
plugSrc (LqTV v
v) = v -> Maybe v
forall a. a -> Maybe a
Just v
v 
plugSrc PlugTV v
_        = Maybe v
forall a. Maybe a
Nothing

-------------------------------------------------------------------------------
-- | Name resolution environment 
-------------------------------------------------------------------------------
data Env = RE 
  { Env -> GHCTyLookupEnv
reTyLookupEnv :: GHCTyLookupEnv
  , Env -> TcGblEnv
reTcGblEnv  :: Ghc.TcGblEnv
  , Env -> InstEnvs
reInstEnvs  :: Ghc.InstEnvs
  , Env -> NameSet
reUsedExternals :: Ghc.NameSet
  , Env -> LogicMap
reLMap      :: LogicMap
  , Env -> [Id]
reDataConIds :: [Ghc.Id]                -- ^ Data constructors used in the current module
  , Env -> Config
reCfg       :: Config
  , Env -> LocalVars
reLocalVars :: LocalVars                -- ^ lines at which local variables are defined.
  , Env -> HashSet Symbol
reGlobSyms  :: S.HashSet F.Symbol       -- ^ global symbols, typically unlifted measures like 'len', 'fromJust'
  , Env -> GhcSrc
reSrc       :: GhcSrc                   -- ^ all source info
  }

data GHCTyLookupEnv = GHCTyLookupEnv
       { GHCTyLookupEnv -> Session
gtleSession :: Ghc.Session
       , GHCTyLookupEnv -> TypeEnv
gtleTypeEnv :: Ghc.TypeEnv
       }

instance HasConfig Env where 
  getConfig :: Env -> Config
getConfig = Env -> Config
reCfg 

data LocalVars = LocalVars
  { -- | A map from names to lists of pairs of @Ghc.Var@ and
    --   the lines at which they were defined.
    LocalVars -> HashMap Symbol [LocalVarDetails]
lvSymbols :: M.HashMap F.Symbol [LocalVarDetails]
    -- | A map from names to its details
  , LocalVars -> NameEnv LocalVarDetails
lvNames :: NameEnv LocalVarDetails
  }

data LocalVarDetails = LocalVarDetails
  { LocalVarDetails -> SourcePos
lvdSourcePos :: F.SourcePos
  , LocalVarDetails -> Id
lvdVar :: Ghc.Var
  , LocalVarDetails -> [Id]
lvdLclEnv :: [Ghc.Var]
  , LocalVarDetails -> Bool
lvdIsRec :: Bool  -- ^ Is the variable defined in a letrec?
  } deriving Int -> LocalVarDetails -> ShowS
[LocalVarDetails] -> ShowS
LocalVarDetails -> String
(Int -> LocalVarDetails -> ShowS)
-> (LocalVarDetails -> String)
-> ([LocalVarDetails] -> ShowS)
-> Show LocalVarDetails
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LocalVarDetails -> ShowS
showsPrec :: Int -> LocalVarDetails -> ShowS
$cshow :: LocalVarDetails -> String
show :: LocalVarDetails -> String
$cshowList :: [LocalVarDetails] -> ShowS
showList :: [LocalVarDetails] -> ShowS
Show

-------------------------------------------------------------------------------
-- | A @TyThingMap@ is used to resolve symbols into GHC @TyThing@ and, 
--   from there into Var, TyCon, DataCon, etc.
-------------------------------------------------------------------------------
type TyThingMap = M.HashMap F.Symbol [(F.Symbol, Ghc.TyThing)]

-------------------------------------------------------------------------------
-- | A @SigEnv@ contains the needed to process type signatures 
-------------------------------------------------------------------------------
data SigEnv = SigEnv 
  { SigEnv -> TCEmb TyCon
sigEmbs       :: !(F.TCEmb Ghc.TyCon) 
  , SigEnv -> TyConMap
sigTyRTyMap   :: !RT.TyConMap 
  , SigEnv -> HashSet StableName
sigExports    :: !(S.HashSet StableName)
  , SigEnv -> BareRTEnv
sigRTEnv      :: !BareRTEnv
  }

-------------------------------------------------------------------------------
-- | A @TycEnv@ contains the information needed to process Type- and Data- Constructors 
-------------------------------------------------------------------------------
data TycEnv = TycEnv 
  { TycEnv -> [TyConP]
tcTyCons      :: ![TyConP]
  , TycEnv -> [DataConP]
tcDataCons    :: ![DataConP]
  , TycEnv -> [Measure SpecType DataCon]
tcSelMeasures :: ![Measure SpecType Ghc.DataCon]
  , TycEnv -> [(Id, LocSpecType)]
tcSelVars     :: ![(Ghc.Var, LocSpecType)]
  , TycEnv -> TyConMap
tcTyConMap    :: !RT.TyConMap 
  , TycEnv -> [DataDecl]
tcAdts        :: ![F.DataDecl]
  , TycEnv -> DataConMap
tcDataConMap  :: !DataConMap 
  , TycEnv -> TCEmb TyCon
tcEmbs        :: !(F.TCEmb Ghc.TyCon)
  , TycEnv -> ModName
tcName        :: !ModName
  }

type DataConMap = M.HashMap (F.Symbol, Int) F.Symbol

-------------------------------------------------------------------------------
-- | Intermediate representation for Measure information 
-------------------------------------------------------------------------------
-- REBARE: used to be output of makeGhcSpecCHOP2
data MeasEnv = MeasEnv 
  { MeasEnv -> MSpec SpecType DataCon
meMeasureSpec :: !(MSpec SpecType Ghc.DataCon)          
  , MeasEnv -> [(Symbol, Located (RRType Reft))]
meClassSyms   :: ![(F.Symbol, Located (RRType F.Reft))] 
  , MeasEnv -> [(Symbol, Located (RRType Reft))]
meSyms        :: ![(F.Symbol, Located (RRType F.Reft))]
  , MeasEnv -> [(Id, LocSpecType)]
meDataCons    :: ![(Ghc.Var,  LocSpecType)]           
  , MeasEnv -> [DataConP]
meClasses     :: ![DataConP]                           
  , MeasEnv -> [(ModName, Id, LocSpecType)]
meMethods     :: ![(ModName, Ghc.Var, LocSpecType)]  
  , MeasEnv -> [(Id, Measure (Located BareType) (Located LHName))]
meOpaqueRefl  :: ![(Ghc.Var, Measure (Located BareType) (F.Located LHName))] -- the opaque-reflected symbols and the corresponding measures
  }

instance Semigroup MeasEnv where
  MeasEnv
a <> :: MeasEnv -> MeasEnv -> MeasEnv
<> MeasEnv
b = MeasEnv
    { meMeasureSpec :: MSpec SpecType DataCon
meMeasureSpec = MeasEnv -> MSpec SpecType DataCon
meMeasureSpec MeasEnv
a MSpec SpecType DataCon
-> MSpec SpecType DataCon -> MSpec SpecType DataCon
forall a. Semigroup a => a -> a -> a
<> MeasEnv -> MSpec SpecType DataCon
meMeasureSpec MeasEnv
b
    , meClassSyms :: [(Symbol, Located (RRType Reft))]
meClassSyms   = MeasEnv -> [(Symbol, Located (RRType Reft))]
meClassSyms MeasEnv
a [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
forall a. Semigroup a => a -> a -> a
<> MeasEnv -> [(Symbol, Located (RRType Reft))]
meClassSyms MeasEnv
b
    , meSyms :: [(Symbol, Located (RRType Reft))]
meSyms        = MeasEnv -> [(Symbol, Located (RRType Reft))]
meSyms MeasEnv
a [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
forall a. Semigroup a => a -> a -> a
<> MeasEnv -> [(Symbol, Located (RRType Reft))]
meSyms MeasEnv
b
    , meDataCons :: [(Id, LocSpecType)]
meDataCons    = MeasEnv -> [(Id, LocSpecType)]
meDataCons MeasEnv
a [(Id, LocSpecType)] -> [(Id, LocSpecType)] -> [(Id, LocSpecType)]
forall a. Semigroup a => a -> a -> a
<> MeasEnv -> [(Id, LocSpecType)]
meDataCons MeasEnv
b  
    , meClasses :: [DataConP]
meClasses     = MeasEnv -> [DataConP]
meClasses MeasEnv
a [DataConP] -> [DataConP] -> [DataConP]
forall a. Semigroup a => a -> a -> a
<> MeasEnv -> [DataConP]
meClasses MeasEnv
b                       
    , meMethods :: [(ModName, Id, LocSpecType)]
meMethods     = MeasEnv -> [(ModName, Id, LocSpecType)]
meMethods MeasEnv
a [(ModName, Id, LocSpecType)]
-> [(ModName, Id, LocSpecType)] -> [(ModName, Id, LocSpecType)]
forall a. Semigroup a => a -> a -> a
<> MeasEnv -> [(ModName, Id, LocSpecType)]
meMethods MeasEnv
b
    , meOpaqueRefl :: [(Id, Measure (Located BareType) (Located LHName))]
meOpaqueRefl  = MeasEnv -> [(Id, Measure (Located BareType) (Located LHName))]
meOpaqueRefl MeasEnv
a [(Id, Measure (Located BareType) (Located LHName))]
-> [(Id, Measure (Located BareType) (Located LHName))]
-> [(Id, Measure (Located BareType) (Located LHName))]
forall a. Semigroup a => a -> a -> a
<> MeasEnv -> [(Id, Measure (Located BareType) (Located LHName))]
meOpaqueRefl MeasEnv
b
    }
instance Monoid MeasEnv where
  mempty :: MeasEnv
mempty = MeasEnv
    {
      meMeasureSpec :: MSpec SpecType DataCon
meMeasureSpec = MSpec SpecType DataCon
forall a. Monoid a => a
mempty
    , meClassSyms :: [(Symbol, Located (RRType Reft))]
meClassSyms   = [(Symbol, Located (RRType Reft))]
forall a. Monoid a => a
mempty
    , meSyms :: [(Symbol, Located (RRType Reft))]
meSyms        = [(Symbol, Located (RRType Reft))]
forall a. Monoid a => a
mempty
    , meDataCons :: [(Id, LocSpecType)]
meDataCons    = [(Id, LocSpecType)]
forall a. Monoid a => a
mempty
    , meClasses :: [DataConP]
meClasses     = [DataConP]
forall a. Monoid a => a
mempty
    , meMethods :: [(ModName, Id, LocSpecType)]
meMethods     = [(ModName, Id, LocSpecType)]
forall a. Monoid a => a
mempty
    , meOpaqueRefl :: [(Id, Measure (Located BareType) (Located LHName))]
meOpaqueRefl  = [(Id, Measure (Located BareType) (Located LHName))]
forall a. Monoid a => a
mempty
    }

-------------------------------------------------------------------------------
-- | Converting @Var@ to @Sort@
-------------------------------------------------------------------------------
varSortedReft :: F.TCEmb Ghc.TyCon -> Ghc.Var -> F.SortedReft 
varSortedReft :: TCEmb TyCon -> Id -> SortedReft
varSortedReft TCEmb TyCon
emb = TCEmb TyCon -> RType RTyCon RTyVar () -> SortedReft
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
RT.rTypeSortedReft TCEmb TyCon
emb (RType RTyCon RTyVar () -> SortedReft)
-> (Id -> RType RTyCon RTyVar ()) -> Id -> SortedReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> RType RTyCon RTyVar ()
varRSort 

varRSort  :: Ghc.Var -> RSort
varRSort :: Id -> RType RTyCon RTyVar ()
varRSort  = Type -> RType RTyCon RTyVar ()
forall r. Monoid r => Type -> RRType r
RT.ofType (Type -> RType RTyCon RTyVar ())
-> (Id -> Type) -> Id -> RType RTyCon RTyVar ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Type
Ghc.varType

-------------------------------------------------------------------------------
-- | Handling failed resolution 
-------------------------------------------------------------------------------
failMaybe :: Env -> ModName -> Either e r -> Either e (Maybe r)
failMaybe :: forall e r. Env -> ModName -> Either e r -> Either e (Maybe r)
failMaybe Env
env ModName
name Either e r
res = case Either e r
res of 
  Right r
r -> Maybe r -> Either e (Maybe r)
forall a b. b -> Either a b
Right (r -> Maybe r
forall a. a -> Maybe a
Just r
r) 
  Left  e
e -> if Env -> ModName -> Bool
isTargetModName Env
env ModName
name 
              then e -> Either e (Maybe r)
forall a b. a -> Either a b
Left e
e
              else Maybe r -> Either e (Maybe r)
forall a b. b -> Either a b
Right Maybe r
forall a. Maybe a
Nothing 

isTargetModName :: Env -> ModName -> Bool 
isTargetModName :: Env -> ModName -> Bool
isTargetModName Env
env ModName
name = ModName
name ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== GhcSrc -> ModName
_giTargetMod (Env -> GhcSrc
reSrc Env
env)