content: {-# LANGUAGE ConstraintKinds       #-}
  {-# LANGUAGE FlexibleContexts      #-}
  {-# LANGUAGE FlexibleInstances     #-}
  {-# LANGUAGE LambdaCase            #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE TupleSections         #-}
  {-# LANGUAGE UndecidableInstances  #-}
  
  module Language.Rsc.Lookup (
      getProp
    , getFieldMutability
    , extractCtor
    ) where
  
  import           Data.Default
  import           Data.Either                    (rights)
  import qualified Language.Fixpoint.Types        as F
  import           Language.Fixpoint.Types.Errors
  import           Language.Rsc.AST
  import           Language.Rsc.ClassHierarchy
  import           Language.Rsc.Core.Env
  import           Language.Rsc.Environment
  import           Language.Rsc.Errors
  import           Language.Rsc.Liquid.Types
  import           Language.Rsc.Locations
  import           Language.Rsc.Module
  import           Language.Rsc.Names
  import           Language.Rsc.Pretty
  import           Language.Rsc.Symbols
  import           Language.Rsc.Typecheck.Types
  import           Language.Rsc.Types
  
  type PPRE r = (ExprReftable Int r, PPR r)
  
  -- | Excluded fields from string index lookup
  --
  excludedFieldSymbols = F.symbol <$> [ "hasOwnProperty", "prototype", "__proto__" ]
  
  type PPRD r   = (ExprReftable Int r, PP r, F.Reftable r)
  type CEnv r t = (CheckingEnvironment r t , Functor t)
  
  -- | `getProp l γ x f t` performs the access `x.f`, where `x: t` and returns a
  --   list of pairs `(tBase, tMember)` where
  --
  --   * tBase  : the part of `t` for which the access of field `f` is successful
  --
  --   * tMember: the accessed type member.
  --
  --------------------------------------------------------------------------------
  getProp :: (CEnv r t, PPRD r, IsLocated l, F.Expression x, F.Symbolic x, F.Symbolic f)
          => l -> t r -> x -> f -> RType r -> Either Error [(RType r, TypeMember r)]
  --------------------------------------------------------------------------------
  getProp l γ x f t@(TPrim _ _) = getPropPrim l γ x f t
  
  getProp l γ x f (TOr ts _) = getPropUnion l γ x f ts
  
  -- | TODO: Chain up to 'Object'
  getProp l γ x f t@TObj{}
    = fmap (map (t,)) (accessMember l γ InstanceK x f t)
  
  -- | Enumeration
  --
  --   TODO: Instead of the actual integer value, assign unique symbolic values:
  --         E.g. A_B_C_1 ...
  --
  getProp l γ _ f t@(TRef (Gen n []) _)
    | Just e  <- resolveEnumInEnv γ n
    , Just io <- envFindTy f (e_mapping e)
    = case io of
        IntLit _ i ->
            Right [(t, FI fSym Req tIM (tNum `strengthen` exprReft i))]
        HexLit _ s ->
            case bitVectorValue s of
              Just v -> Right [(t, FI fSym Req tIM (tBV32 `strengthen` v))]
              _      -> Left (errorEnumLookup l fSym t)
        _ ->  Left (errorEnumLookup l fSym t)
    where
      fSym = F.symbol f
  
  getProp l γ x f t@(TRef _ _)
    = fmap (map (t,)) (accessMember l γ InstanceK x f t)
  
  getProp l γ x f t@(TClass _)
    = fmap (map (t,)) (accessMember l γ StaticK x f t)
  
  getProp _ γ _ f t@(TMod m)
    | Just m' <- resolveModuleInEnv γ m
    , Just v' <- envFindTy f (m_variables m')
    = Right [(t, symToField v')]
  
  getProp _ _ _ f t
    | isTFun t
    , F.symbol f == callSym
    , Just ft <- go t
    = Right [(t, MI fSym Req [(tRO, ft)])]
    where
      go    = fmap tAnd . mapM aa . bkAnd
      aa t  | Just (bs, ts, rt) <- bkFun t
            = Just (mkFun (bv:bs, b:ts, rt))
            | otherwise = Nothing
      bv    = BTV vSym dummySpan Nothing
      tv    = tVar (TV vSym dummySpan)
      b     = B thisSym Req tv
      vSym  = F.symbol "__v"
      fSym  = F.symbol f
  
  getProp l _ _ f t = Left (errorGenericLookup l (F.symbol f) t)
  
  
  --------------------------------------------------------------------------------
  getPropPrim
    :: (CEnv r t, PPRD r, IsLocated l, F.Expression x, F.Symbolic x, F.Symbolic f)
    => l -> t r -> x -> f -> RType r -> Either Error [(RType r, TypeMember r)]
  --------------------------------------------------------------------------------
  getPropPrim l γ x f t@(TPrim c _) =
    case c of
      TNumber    -> fmap (map (t,)) (lookupAmbientType l γ x f numberSym)
      TString    -> fmap (map (t,)) (lookupAmbientType l γ x f stringSym)
      TStrLit _  -> fmap (map (t,)) (lookupAmbientType l γ x f stringSym)
      TBV32      -> fmap (map (t,)) (lookupAmbientType l γ x f numberSym)
      _          -> Left (errorPrimLookup l (F.symbol f) t)
  
  getPropPrim _ _ _ _ _ = error "getPropPrim should only be applied to TApp"
  
  
  -- | `extractCtor γ t` extracts a contructor signature from a type @t@
  --
  --------------------------------------------------------------------------------
  extractCtor :: (PPRD r, CEnv r g) => g r -> RType r -> Maybe (RType r)
  --------------------------------------------------------------------------------
  extractCtor γ t = go t
    where
      go (TClass (BGen x _)) | Just (TD _ _ ms) <- resolveTypeInEnv γ x
                             = tm_ctor ms
      go (TRef _ _)          = expandType def (envCHA γ) t >>= go
      go (TObj _ ms _)       = tm_ctor ms
      go _                   = Nothing
  
  
  --------------------------------------------------------------------------------
  accessMember
    :: (CEnv r t, PPRE r, IsLocated l, F.Expression x, F.Symbolic x, F.Symbolic f)
    => l -> t r -> StaticKind -> x -> f -> RType r -> Either Error [TypeMember r]
  --------------------------------------------------------------------------------
  accessMember l γ InstanceK x m t
    | Just (TObj _ es _) <- expandType econf (envCHA γ) t
    , Just mem           <- F.symbol m `F.lookupSEnv` i_mems es
    = Right [substThis x mem]
  
    -- In the case of string indexing, build up an optional and assignable field
    | Just (TObj _ es _) <- expandType econf (envCHA γ) t
    , Just (mIdx, tIdx)  <- tm_sidx es
    , validFieldName m
    = Right [substThis x $ FI (F.symbol m) Opt mIdx tIdx]
  
    | otherwise
    = Left $ errorMemLookup l (F.symbol m) t
    where
      econf = EConf True True -- Lookup members inherited from built-in objects
  
  accessMember l γ StaticK x m t
    | Just (TObj _ es _) <- expandType econf (envCHA γ) t
    , Just mem           <- F.symbol m `F.lookupSEnv` s_mems es
    = Right [substThis x mem]
    | otherwise
    = Left $ errorMemLookup l (F.symbol m) t
    where
      econf = EConf True True -- Lookup members inherited from built-in objects
  
  
  --------------------------------------------------------------------------------
  validFieldName  :: F.Symbolic f => f -> Bool
  --------------------------------------------------------------------------------
  validFieldName f = F.symbol f `notElem` excludedFieldSymbols
  
  --------------------------------------------------------------------------------
  lookupAmbientType
    :: (CEnv r t, PPRD r, IsLocated l, F.Expression x, F.Symbolic x, F.Symbolic f)
    => l -> t r -> x -> f -> F.Symbol -> Either Error [TypeMemberQ AK r]
  --------------------------------------------------------------------------------
  lookupAmbientType l γ x f amb
    | Just (TD _ _ ms) <- resolveTypeInEnv γ (mkAbsName [] amb)
    = accessMember l γ InstanceK x f (TObj tIM ms fTop)
    | otherwise
    = Left (errorAmbientLookup l (F.symbol f) (F.symbol x))
  
  -- | Accessing the @f@ field of the union type with @ts@ as its parts, returns
  --   "Nothing" if accessing all parts return error, or "Just (ts, tfs)" if
  --   accessing @ts@ returns type @tfs@. @ts@ is useful for adding casts later on.
  --------------------------------------------------------------------------------
  getPropUnion
    :: (CEnv r t, PPRD r, IsLocated l, F.Expression x, F.Symbolic x, F.Symbolic f)
    => l -> t r -> x -> f -> [RType r] -> Either Error [(RType r, TypeMember r)]
  --------------------------------------------------------------------------------
  getPropUnion l γ x f ts =
    case rights (map (getProp l γ x f) ts) of
      [ ] -> Left (errorUnionLookup l (F.symbol f) (tOrR ts fTop))
      tfs -> Right (concat tfs)
  
  --------------------------------------------------------------------------------
  getFieldMutability :: (PPRD r, F.Symbolic s)
    => ClassHierarchy r -> RType r -> s -> Maybe (MutabilityR r)
  --------------------------------------------------------------------------------
  getFieldMutability cha t f
    | Just (TObj _ ms _i) <- expandType def cha t
    , Just (FI _ _ m _)   <- F.lookupSEnv (F.symbol f) (i_mems ms)
    = Just m
    | otherwise
    = Nothing
  
  