-- | 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 (..)
  , TyThingMap 
  , ModSpecs
  , LocalVars 

    -- * 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 Control.Exception                     as Ex 
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 qualified Language.Haskell.Liquid.Types.RefType as RT 
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.Types.Specs   hiding (BareSpec)
import           Language.Haskell.Liquid.GHC.API       as Ghc hiding (Located) 
import           Language.Haskell.Liquid.GHC.Types     (StableName)


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
showList :: [PlugTV v] -> ShowS
$cshowList :: forall v. Show v => [PlugTV v] -> ShowS
show :: PlugTV v -> String
$cshow :: forall v. Show v => PlugTV v -> String
showsPrec :: Int -> PlugTV v -> ShowS
$cshowsPrec :: forall v. Show v => Int -> 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 :: 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 -> LogicMap
reLMap      :: !LogicMap
  , Env -> [(Symbol, Var)]
reSyms      :: ![(F.Symbol, Ghc.Var)]    -- ^ see "syms" in old makeGhcSpec'
  , Env -> Subst
_reSubst    :: !F.Subst                  -- ^ see "su"   in old makeGhcSpec'
  , Env -> TyThingMap
_reTyThings :: !TyThingMap 
  , Env -> Config
reCfg       :: !Config
  , Env -> QImports
reQualImps  :: !QImports                 -- ^ qualified imports
  , Env -> HashSet Symbol
reAllImps   :: !(S.HashSet F.Symbol)     -- ^ all imported modules
  , 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
  }

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

-- | @LocalVars@ is a map from names to lists of pairs of @Ghc.Var@ and 
--   the lines at which they were defined. 
type LocalVars = M.HashMap F.Symbol [(Int, Ghc.Var)]

-------------------------------------------------------------------------------
-- | 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 -> [(Var, 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 -> [(Var, LocSpecType)]
meDataCons    :: ![(Ghc.Var,  LocSpecType)]           
  , MeasEnv -> [DataConP]
meClasses     :: ![DataConP]                           
  , MeasEnv -> [(ModName, Var, LocSpecType)]
meMethods     :: ![(ModName, Ghc.Var, LocSpecType)]  
  , MeasEnv -> [(Class, [(ModName, Var, LocSpecType)])]
meCLaws       :: !([(Ghc.Class, [(ModName, Ghc.Var, LocSpecType)])])  
  }

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

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

-------------------------------------------------------------------------------
-- | Handling failed resolution 
-------------------------------------------------------------------------------
failMaybe :: Env -> ModName -> Either UserError r -> Maybe r
failMaybe :: Env -> ModName -> Either UserError r -> Maybe r
failMaybe Env
env ModName
name Either UserError r
res = case Either UserError r
res of 
  Right r
r -> r -> Maybe r
forall a. a -> Maybe a
Just r
r 
  Left  UserError
e -> if Env -> ModName -> Bool
isTargetModName Env
env ModName
name 
              then UserError -> Maybe r
forall a e. Exception e => e -> a
Ex.throw UserError
e
              else 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)