-- |
-- Module      :  $Header$
-- Copyright   :  (c) 2013-2015 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE FlexibleInstances #-}

module Cryptol.ModuleSystem.Renamer (
    NamingEnv(), shadowing
  , BindsNames(..)
  , checkNamingEnv
  , Rename(..), runRenamer
  , RenamerError(..)
  , RenamerWarning(..)
  ) where

import Cryptol.ModuleSystem.NamingEnv
import Cryptol.Prims.Syntax
import Cryptol.Parser.AST
import Cryptol.Parser.Names (tnamesP)
import Cryptol.Parser.Position
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.PP

import MonadLib
import qualified Data.Map as Map

#if __GLASGOW_HASKELL__ < 710
import Control.Applicative(Applicative(..),(<$>))
import Data.Foldable (foldMap)
import Data.Monoid (Monoid(..))
import Data.Traversable (traverse)
#endif

-- Errors ----------------------------------------------------------------------

data RenamerError
  = MultipleSyms (Located QName) [NameOrigin]
    -- ^ Multiple imported symbols contain this name

  | UnboundExpr (Located QName)
    -- ^ Expression name is not bound to any definition

  | UnboundType (Located QName)
    -- ^ Type name is not bound to any definition

  | OverlappingSyms [NameOrigin]
    -- ^ An environment has produced multiple overlapping symbols

  | ExpectedValue (Located QName)
    -- ^ When a value is expected from the naming environment, but one or more
    -- types exist instead.

  | ExpectedType (Located QName)
    -- ^ When a type is missing from the naming environment, but one or more
    -- values exist with the same name.
    deriving (Show)

instance PP RenamerError where
  ppPrec _ e = case e of

    MultipleSyms lqn qns ->
      hang (text "[error] at" <+> pp (srcRange lqn))
         4 $ (text "Multiple definitions for symbol:" <+> pp (thing lqn))
          $$ vcat (map pp qns)

    UnboundExpr lqn ->
      hang (text "[error] at" <+> pp (srcRange lqn))
         4 (text "Value not in scope:" <+> pp (thing lqn))

    UnboundType lqn ->
      hang (text "[error] at" <+> pp (srcRange lqn))
         4 (text "Type not in scope:" <+> pp (thing lqn))

    OverlappingSyms qns ->
      hang (text "[error]")
         4 $ text "Overlapping symbols defined:"
          $$ vcat (map pp qns)

    ExpectedValue lqn ->
      hang (text "[error] at" <+> pp (srcRange lqn))
         4 (fsep [ text "Expected a value named", quotes (pp (thing lqn))
                 , text "but found a type instead"
                 , text "Did you mean `(" <> pp (thing lqn) <> text")?" ])

    ExpectedType lqn ->
      hang (text "[error] at" <+> pp (srcRange lqn))
         4 (fsep [ text "Expected a type named", quotes (pp (thing lqn))
                 , text "but found a value instead" ])

-- Warnings --------------------------------------------------------------------

data RenamerWarning
  = SymbolShadowed NameOrigin [NameOrigin]
    deriving (Show)

instance PP RenamerWarning where
  ppPrec _ (SymbolShadowed new originals) =
    hang (text "[warning] at" <+> loc)
       4 $ fsep [ text "This binding for" <+> sym
                , text "shadows the existing binding" <> plural <+> text "from" ]
        $$ vcat (map pp originals)

    where
    plural | length originals > 1 = char 's'
           | otherwise            = empty

    (loc,sym) = case new of
                  Local lqn   -> (pp (srcRange lqn), pp (thing lqn))
                  Imported qn -> (empty, pp qn)


-- Renaming Monad --------------------------------------------------------------

data RO = RO
  { roLoc   :: Range
  , roNames :: NamingEnv
  }

data Out = Out
  { oWarnings :: [RenamerWarning]
  , oErrors   :: [RenamerError]
  } deriving (Show)

instance Monoid Out where
  mempty      = Out [] []
  mappend l r = Out (oWarnings l `mappend` oWarnings r)
                    (oErrors   l `mappend` oErrors   r)

newtype RenameM a = RenameM
  { unRenameM :: ReaderT RO (WriterT Out Id) a }

instance Functor RenameM where
  {-# INLINE fmap #-}
  fmap f m      = RenameM (fmap f (unRenameM m))

instance Applicative RenameM where
  {-# INLINE pure #-}
  pure x        = RenameM (pure x)

  {-# INLINE (<*>) #-}
  l <*> r       = RenameM (unRenameM l <*> unRenameM r)

instance Monad RenameM where
  {-# INLINE return #-}
  return x      = RenameM (return x)

  {-# INLINE (>>=) #-}
  m >>= k       = RenameM (unRenameM m >>= unRenameM . k)

runRenamer :: NamingEnv -> RenameM a
           -> (Either [RenamerError] a,[RenamerWarning])
runRenamer env m = (res,oWarnings out)
  where

  (a,out) = runM (unRenameM m) RO { roLoc = emptyRange, roNames = env }

  res | null (oErrors out) = Right a
      | otherwise          = Left (oErrors out)

record :: RenamerError -> RenameM ()
record err = records [err]

records :: [RenamerError] -> RenameM ()
records errs = RenameM (put mempty { oErrors = errs })

located :: a -> RenameM (Located a)
located a = RenameM $ do
  ro <- ask
  return Located { srcRange = roLoc ro, thing = a }

withLoc :: HasLoc loc => loc -> RenameM a -> RenameM a
withLoc loc m = RenameM $ case getLoc loc of

  Just range -> do
    ro <- ask
    local ro { roLoc = range } (unRenameM m)

  Nothing -> unRenameM m

-- | Shadow the current naming environment with some more names.
shadowNames :: BindsNames env => env -> RenameM a -> RenameM a
shadowNames names m = RenameM $ do
  let env = namingEnv names
  ro <- ask
  put (checkEnv env (roNames ro))
  let ro' = ro { roNames = env `shadowing` roNames ro }
  local ro' (unRenameM m)

-- | Generate warnings when the left environment shadows things defined in
-- the right.  Additionally, generate errors when two names overlap in the
-- left environment.
checkEnv :: NamingEnv -> NamingEnv -> Out
checkEnv l r = Map.foldlWithKey (step neExprs) mempty (neExprs l)
     `mappend` Map.foldlWithKey (step neTypes) mempty (neTypes l)
  where

  step prj acc k ns = acc `mappend` mempty
    { oWarnings = case Map.lookup k (prj r) of
        Nothing -> []
        Just os -> [SymbolShadowed (origin (head ns)) (map origin os)]
    , oErrors   = containsOverlap ns
    }

-- | Check the RHS of a single name rewrite for conflicting sources.
containsOverlap :: HasQName a => [a] -> [RenamerError]
containsOverlap [_] = []
containsOverlap []  = panic "Renamer" ["Invalid naming environment"]
containsOverlap ns  = [OverlappingSyms (map origin ns)]

-- | Throw errors for any names that overlap in a rewrite environment.
checkNamingEnv :: NamingEnv -> ([RenamerError],[RenamerWarning])
checkNamingEnv env = (out, [])
  where
  out    = Map.foldr check outTys (neExprs env)
  outTys = Map.foldr check mempty (neTypes env)

  check ns acc = containsOverlap ns ++ acc


-- Renaming --------------------------------------------------------------------

class Rename a where
  rename :: a -> RenameM a

instance Rename a => Rename [a] where
  rename        = traverse rename

instance Rename a => Rename (Maybe a) where
  rename        = traverse rename

instance Rename a => Rename (Located a) where
  rename loc    = withLoc loc $ do
    a' <- rename (thing loc)
    return loc { thing = a' }

instance Rename a => Rename (Named a) where
  rename n      = do
    a' <-rename (value n)
    return n { value = a' }

instance Rename Module where
  rename m      = do
    decls' <- rename (mDecls m)
    return m { mDecls = decls' }

instance Rename TopDecl where
  rename td     = case td of
    Decl d      -> Decl      <$> rename d
    TDNewtype n -> TDNewtype <$> rename n
    Include{}   -> return td

instance Rename a => Rename (TopLevel a) where
  rename tl     = do
    a' <- rename (tlValue tl)
    return tl { tlValue = a' }

instance Rename Decl where
  rename d      = case d of
    DSignature ns sig -> DSignature ns <$> rename sig
    DPragma ns p      -> DPragma ns    <$> rename p
    DBind b           -> DBind         <$> rename b
    DPatBind pat e    -> DPatBind pat  <$> shadowNames (namingEnv pat) (rename e)
    DType syn         -> DType         <$> rename syn
    DLocated d' r     -> withLoc r
                       $ DLocated      <$> rename d'  <*> pure r

instance Rename Newtype where
  rename n      = do
    name' <- renameLoc renameType (nName n)
    body' <- shadowNames (nParams n) (rename (nBody n))
    return Newtype { nName   = name'
                   , nParams = nParams n
                   , nBody   = body' }

renameExpr :: QName -> RenameM QName
renameExpr qn = do
  ro <- RenameM ask
  case Map.lookup qn (neExprs (roNames ro)) of
    Just [en] -> return (qname en)
    Just []   -> panic "Renamer" ["Invalid expression renaming environment"]
    Just syms ->
      do n <- located qn
         record (MultipleSyms n (map origin syms))
         return qn
    Nothing   ->
      do n <- located qn

         case Map.lookup qn (neTypes (roNames ro)) of
           -- types existed with the name of the value expected
           Just _ -> record (ExpectedValue n)

           -- the value is just missing
           Nothing -> record (UnboundExpr n)
         return qn

renameType :: QName -> RenameM QName
renameType qn = do
  ro <- RenameM ask
  case Map.lookup qn (neTypes (roNames ro)) of
    Just [tn] -> return (qname tn)
    Just []   -> panic "Renamer" ["Invalid type renaming environment"]
    Just syms ->
      do n <- located qn
         record (MultipleSyms n (map origin syms))
         return qn
    Nothing   ->
      do n <- located qn

         case Map.lookup qn (neExprs (roNames ro)) of

           -- values exist with the same name, so throw a different error
           Just _ -> record (ExpectedType n)

           -- no terms with the same name, so the type is just unbound
           Nothing -> record (UnboundType n)

         return qn

-- | Rename a schema, assuming that none of its type variables are already in
-- scope.
instance Rename Schema where
  rename s@(Forall ps _ _ _) = shadowNames ps (renameSchema s)

-- | Rename a schema, assuming that the type variables have already been brought
-- into scope.
renameSchema :: Schema -> RenameM Schema
renameSchema (Forall ps p ty loc) = Forall ps <$> rename p <*> rename ty
                                              <*> pure loc

instance Rename Prop where
  rename p      = case p of
    CFin t        -> CFin     <$> rename t
    CEqual l r    -> CEqual   <$> rename l  <*> rename r
    CGeq l r      -> CGeq     <$> rename l  <*> rename r
    CArith t      -> CArith   <$> rename t
    CCmp t        -> CCmp     <$> rename t
    CLocated p' r -> withLoc r
                   $ CLocated <$> rename p' <*> pure r

instance Rename Type where
  rename t      = case t of
    TFun a b     -> TFun     <$> rename a  <*> rename b
    TSeq n a     -> TSeq     <$> rename n  <*> rename a
    TBit         -> return t
    TNum _       -> return t
    TChar _      -> return t
    TInf         -> return t

    TUser (QName Nothing (Name "width")) ps
                 -> TApp TCWidth <$> rename ps

    TUser qn ps  -> TUser    <$> renameType qn <*> rename ps
    TApp f xs    -> TApp f   <$> rename xs
    TRecord fs   -> TRecord  <$> rename fs
    TTuple fs    -> TTuple   <$> rename fs
    TWild        -> return t
    TLocated t' r -> withLoc r
                 $ TLocated <$> rename t' <*> pure r

instance Rename Pragma where
  rename p      = case p of
    PragmaNote _   -> return p
    PragmaProperty -> return p

-- | The type renaming environment generated by a binding.
bindingTypeEnv :: Bind -> NamingEnv
bindingTypeEnv b = patParams `shadowing` sigParams
  where
  -- type parameters
  sigParams = namingEnv (bSignature b)

  -- pattern type parameters
  patParams   = foldMap (foldMap qualType . tnamesP) (bParams b)
  qualType qn = singletonT qn (TFromParam qn)

-- | Rename a binding.
--
-- NOTE: this does not bind its own name into the naming context of its body.
-- The assumption here is that this has been done by the enclosing environment,
-- to allow for top-level renaming
instance Rename Bind where
  rename b      = do
    n' <- renameLoc renameExpr (bName b)
    shadowNames (bindingTypeEnv b) $ do
      (patenv,pats') <- renamePats (bParams b)
      sig'           <- traverse renameSchema (bSignature b)
      shadowNames patenv $
        do e'   <- rename (bDef b)
           p'   <- rename (bPragmas b)
           return b { bName      = n'
                    , bParams    = pats'
                    , bDef       = e'
                    , bSignature = sig'
                    , bPragmas   = p'
                    }

-- NOTE: this only renames types within the pattern.
instance Rename Pattern where
  rename p      = case p of
    PVar _          -> pure p
    PWild           -> pure p
    PTuple ps       -> PTuple   <$> rename ps
    PRecord nps     -> PRecord  <$> rename nps
    PList elems     -> PList    <$> rename elems
    PTyped p' t     -> PTyped   <$> rename p'    <*> rename t
    PSplit l r      -> PSplit   <$> rename l     <*> rename r
    PLocated p' loc -> withLoc loc
                     $ PLocated <$> rename p'    <*> pure loc

instance Rename Expr where
  rename e = case e of
    EVar n        -> EVar    <$> renameExpr n
    ECon _        -> return e
    ELit _        -> return e
    ETuple es     -> ETuple  <$> rename es
    ERecord fs    -> ERecord <$> rename fs
    ESel e' s     -> ESel    <$> rename e' <*> pure s
    EList es      -> EList   <$> rename es
    EFromTo s n e'-> EFromTo <$> rename s  <*> rename n  <*> rename e'
    EInfFrom a b  -> EInfFrom<$> rename a  <*> rename b
    EComp e' bs   -> do bs' <- mapM renameMatch bs
                        shadowNames (namingEnv bs')
                            (EComp <$> rename e' <*> pure bs')
    EApp f x      -> EApp    <$> rename f  <*> rename x
    EAppT f ti    -> EAppT   <$> rename f  <*> rename ti
    EIf b t f     -> EIf     <$> rename b  <*> rename t  <*> rename f
    EWhere e' ds  -> shadowNames ds (EWhere <$> rename e' <*> rename ds)
    ETyped e' ty  -> ETyped  <$> rename e' <*> rename ty
    ETypeVal ty   -> ETypeVal<$> rename ty
    EFun ps e'    -> do ps' <- rename ps
                        shadowNames ps' (EFun ps' <$> rename e')
    ELocated e' r -> withLoc r
                   $ ELocated <$> rename e' <*> pure r

instance Rename TypeInst where
  rename ti = case ti of
    NamedInst nty -> NamedInst <$> rename nty
    PosInst ty    -> PosInst   <$> rename ty

renameMatch :: [Match] -> RenameM [Match]
renameMatch  = loop
  where
  loop ms = case ms of

    m:rest -> do
      m' <- rename m
      (m':) <$> shadowNames m' (loop rest)

    [] -> return []

renamePats :: [Pattern] -> RenameM (NamingEnv,[Pattern])
renamePats  = loop
  where
  loop ps = case ps of

    p:rest -> do
      p' <- rename p
      let pe = namingEnv p'
      (env',rest') <- loop rest
      return (pe `mappend` env', p':rest')

    [] -> return (mempty, [])

instance Rename Match where
  rename m = case m of
    Match p e  ->                Match    <$> rename p <*> rename e
    MatchLet b -> shadowNames b (MatchLet <$> rename b)

instance Rename TySyn where
  rename (TySyn n ps ty) =
     shadowNames ps (TySyn <$> renameLoc renameType n <*> pure ps <*> rename ty)

renameLoc :: (a -> RenameM a) -> Located a -> RenameM (Located a)
renameLoc by loc = do
  a' <- by (thing loc)
  return loc { thing = a' }