{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -fwarn-missing-signatures #-}

module Agda.Syntax.Translation.ReflectedToAbstract where

import Control.Monad.Reader

import Data.Traversable as Trav hiding (mapM)

import Agda.Syntax.Fixity
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Info
import Agda.Syntax.Common
import Agda.Syntax.Abstract as A hiding (Apply)
import Agda.Syntax.Abstract.Pattern
import Agda.Syntax.Reflected as R

import Agda.TypeChecking.Monad as M hiding (MetaInfo)
import Agda.Syntax.Scope.Monad (getCurrentModule)

import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.List
import Agda.Utils.Functor
import Agda.Utils.Size

type Names = [Name]

type WithNames a = ReaderT Names TCM a
-- Note: we only need the TCM for fresh names

-- | Adds a new unique name to the current context.
withName :: String -> (Name -> WithNames a) -> WithNames a
withName s f = do
  name <- freshName_ s
  ctx  <- asks $ map nameConcrete
  let name' = head $ filter (notTaken ctx) $ iterate nextName name
  local (name:) $ f name'
  where
    notTaken xs x = isNoName x || nameConcrete x `notElem` xs

-- | Returns the name of the variable with the given de Bruijn index.
askName :: Int -> WithNames (Maybe Name)
askName i = reader (!!! i)

class ToAbstract r a | r -> a where
  toAbstract :: r -> WithNames a

-- | Translate reflected syntax to abstract, using the names from the current typechecking context.
toAbstract_ :: ToAbstract r a => r -> TCM a
toAbstract_ = withShowAllArguments . toAbstractWithoutImplicit

-- | Drop implicit arguments unless --show-implicit is on.
toAbstractWithoutImplicit :: ToAbstract r a => r -> TCM a
toAbstractWithoutImplicit x = runReaderT (toAbstract x) =<< getContextNames

instance ToAbstract r a => ToAbstract (Named name r) (Named name a) where
  toAbstract = traverse toAbstract

instance ToAbstract r a => ToAbstract (Arg r) (NamedArg a) where
  toAbstract (Arg i x) = Arg i <$> toAbstract (unnamed x)

instance ToAbstract [Arg Term] [NamedArg Expr] where
  toAbstract = traverse toAbstract

instance ToAbstract r Expr => ToAbstract (Dom r, Name) (A.TypedBinding) where
  toAbstract (Dom{domInfo = i,unDom = x}, name) = do
    dom <- toAbstract x
    return $ TBind noRange [unnamedArg i $ BindName name] dom

instance ToAbstract (Expr, Elim) Expr where
  toAbstract (f, Apply arg) = do
    arg     <- toAbstract arg
    showImp <- lift showImplicitArguments
    return $ if showImp || visible arg
             then App (setOrigin Reflected defaultAppInfo_) f arg
             else f

instance ToAbstract (Expr, Elims) Expr where
  toAbstract (f, elims) = foldM (curry toAbstract) f elims

instance ToAbstract r a => ToAbstract (R.Abs r) (a, Name) where
  toAbstract (Abs s x) = withName s' $ \name -> (,) <$> toAbstract x <*> return name
    where s' = if (isNoName s) then "z" else s -- TODO: only do this when var is free

instance ToAbstract Literal Expr where
  toAbstract l = return (A.Lit l)

instance ToAbstract Term Expr where
  toAbstract t = case t of
    R.Var i es -> do
      mname <- askName i
      case mname of
        Nothing -> do
          cxt   <- lift $ getContextTelescope
          names <- asks $ drop (size cxt) . reverse
          lift $ withShowAllArguments' False $ typeError $ DeBruijnIndexOutOfScope i cxt names
        Just name -> toAbstract (A.Var name, es)
    R.Con c es -> toAbstract (A.Con (unambiguous $ killRange c), es)
    R.Def f es -> do
      af <- lift $ mkDef (killRange f)
      toAbstract (af, es)
    R.Lam h t  -> do
      (e, name) <- toAbstract t
      let info  = setHiding h $ setOrigin Reflected defaultArgInfo
      return $ A.Lam exprNoRange (DomainFree $ unnamedArg info $ BindName name) e
    R.ExtLam cs es -> do
      name <- freshName_ extendedLambdaName
      m    <- lift $ getCurrentModule
      let qname   = qualify m name
          cname   = nameConcrete name
          defInfo = mkDefInfo cname noFixity' PublicAccess ConcreteDef noRange
      cs <- toAbstract $ map (QNamed qname) cs
      toAbstract (A.ExtendedLam exprNoRange defInfo qname cs, es)
    R.Pi a b   -> do
      (b, name) <- toAbstract b
      a         <- toAbstract (a, name)
      return $ A.Pi exprNoRange [a] b
    R.Sort s   -> toAbstract s
    R.Lit l    -> toAbstract l
    R.Meta x es    -> toAbstract (A.Underscore info, es)
      where info = emptyMetaInfo{ metaNumber = Just x }
    R.Unknown      -> return $ Underscore emptyMetaInfo

mkDef :: QName -> TCM A.Expr
mkDef f =
  ifM (isMacro . theDef <$> getConstInfo f)
      (return $ A.Macro f)
      (return $ A.Def f)

mkSet :: Expr -> Expr
mkSet e = App (setOrigin Reflected defaultAppInfo_) (A.Set exprNoRange 0) $ defaultNamedArg e

instance ToAbstract Sort Expr where
  toAbstract (SetS x) = mkSet <$> toAbstract x
  toAbstract (LitS x) = return $ A.Set exprNoRange x
  toAbstract UnknownS = return $ mkSet $ Underscore emptyMetaInfo

instance ToAbstract R.Pattern (Names, A.Pattern) where
  toAbstract pat = case pat of
    R.ConP c args -> do
      (names, args) <- toAbstractPats args
      return (names, A.ConP (ConPatInfo ConOCon patNoRange ConPatEager) (unambiguous $ killRange c) args)
    R.DotP    -> return ([], A.WildP patNoRange)
    R.VarP s | isNoName s -> withName "z" $ \ name -> return ([name], A.VarP $ BindName name)
        -- Ulf, 2016-08-09: Also bind noNames (#2129). This to make the
        -- behaviour consistent with lambda and pi.
        -- return ([], A.WildP patNoRange)
    R.VarP s  -> withName s $ \ name -> return ([name], A.VarP $ BindName name)
    R.LitP l  -> return ([], A.LitP l)
    R.AbsurdP -> return ([], A.AbsurdP patNoRange)
    R.ProjP d -> return ([], A.ProjP patNoRange ProjSystem $ unambiguous $ killRange d)

toAbstractPats :: [Arg R.Pattern] -> WithNames (Names, [NamedArg A.Pattern])
toAbstractPats pats = case pats of
    []   -> return ([], [])
    p:ps -> do
      (names,  p)  <- (distributeF . fmap distributeF) <$> toAbstract p
      (namess, ps) <- local (names++) $ toAbstractPats ps
      return (namess++names, p:ps)

instance ToAbstract (QNamed R.Clause) A.Clause where
  toAbstract (QNamed name (R.Clause pats rhs)) = do
    (names, pats) <- toAbstractPats pats
    rhs           <- local (names++) $ toAbstract rhs
    let lhs = spineToLhs $ SpineLHS (LHSRange noRange) name pats
    return $ A.Clause lhs [] (RHS rhs Nothing) noWhereDecls False
  toAbstract (QNamed name (R.AbsurdClause pats)) = do
    (_, pats) <- toAbstractPats pats
    let lhs = spineToLhs $ SpineLHS (LHSRange noRange) name pats
    return $ A.Clause lhs [] AbsurdRHS noWhereDecls False

instance ToAbstract [QNamed R.Clause] [A.Clause] where
  toAbstract = traverse toAbstract