{-# LANGUAGE CPP               #-}
{-# LANGUAGE TypeFamilies #-}

{-| A constructor argument is forced if it appears as pattern variable
in an index of the target.

For instance @x@ is forced in @sing@ and @n@ is forced in @zero@ and @suc@:

@
  data Sing {a}{A : Set a} : A -> Set where
    sing : (x : A) -> Sing x

  data Fin : Nat -> Set where
    zero : (n : Nat) -> Fin (suc n)
    suc  : (n : Nat) (i : Fin n) -> Fin (suc n)
@

At runtime, forced constructor arguments may be erased as they can be
recovered from dot patterns.  For instance,
@
  unsing : {A : Set} (x : A) -> Sing x -> A
  unsing .x (sing x) = x
@
can become
@
  unsing x sing = x
@
and
@
  proj : (n : Nat) (i : Fin n) -> Nat
  proj .(suc n) (zero n) = n
  proj .(suc n) (suc n i) = n
@
becomes
@
  proj (suc n) zero    = n
  proj (suc n) (suc i) = n
@

Forcing is a concept from pattern matching and thus builds on the
concept of equality (I) used there (closed terms, extensional) which is
different from the equality (II) used in conversion checking and the
constraint solver (open terms, intensional).

Up to issue 1441 (Feb 2015), the forcing analysis here relied on the
wrong equality (II), considering type constructors as injective.  This is
unsound for program extraction, but ok if forcing is only used to decide which
arguments to skip during conversion checking.

From now on, forcing uses equality (I) and does not search for forced
variables under type constructors.  This may lose some savings during
conversion checking.  If this turns out to be a problem, the old
forcing could be brought back, using a new modality @Skip@ to indicate
that this is a relevant argument but still can be skipped during
conversion checking as it is forced by equality (II).

-}

module Agda.TypeChecking.Forcing where

import Control.Arrow (first, second)
import Control.Monad
import Control.Monad.Trans.Maybe
import Control.Monad.Writer (WriterT(..), tell)
import Data.Foldable hiding (any)
import Data.Traversable
import Data.Semigroup hiding (Arg)
import Data.Maybe
import Data.List ((\\))

import Agda.Interaction.Options

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty hiding ((<>))
import Agda.TypeChecking.Telescope

import Agda.Utils.Function
import Agda.Utils.PartialOrd
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Size

#include "undefined.h"
import Agda.Utils.Impossible

-- | Given the type of a constructor (excluding the parameters),
--   decide which arguments are forced.
--   Precondition: the type is of the form @Γ → D vs@ and the @vs@
--   are in normal form.
computeForcingAnnotations :: Type -> TCM [IsForced]
computeForcingAnnotations t =
  ifM (not . optForcing <$> commandLineOptions)
      (return []) $ do
  -- Andreas, 2015-03-10  Normalization prevents Issue 1454.
  -- t <- normalise t
  -- Andreas, 2015-03-28  Issue 1469: Normalization too costly.
  -- Instantiation also fixes Issue 1454.
  -- Note that normalization of s0 below does not help.
  t <- instantiateFull t
  -- Ulf, 2018-01-28 (#2919): We do need to reduce the target type enough to
  -- get to the actual data type.
  -- Also #2947: The type might reduce to a pi type.
  TelV tel (El _ a) <- telView t
  let vs = case a of
        Def _ us -> us
        _        -> __IMPOSSIBLE__
      n  = size tel
      xs = forcedVariables vs
      -- #2819: We can only mark an argument as forced if it appears in the
      -- type with a relevance below (i.e. more relevant) than the one of the
      -- constructor argument. Otherwise we can't actually get the value from
      -- the type. Also the argument shouldn't be irrelevant, since it that
      -- case it isn't really forced.
      isForced m i = getRelevance m /= Irrelevant &&
                     any (\ (m', j) -> i == j && related m' POLE m) xs
      forcedArgs =
        [ if isForced m i then Forced else NotForced
        | (i, m) <- zip (downFrom n) $ map getModality (telToList tel)
        ]
  reportSLn "tc.force" 60 $ unlines
    [ "Forcing analysis"
    , "  xs          = " ++ show xs
    , "  forcedArgs  = " ++ show forcedArgs
    ]
  return forcedArgs

-- | Compute the pattern variables of a term or term-like thing.
class ForcedVariables a where
  forcedVariables :: a -> [(Modality, Nat)]

  default forcedVariables :: (ForcedVariables b, Foldable t, a ~ t b) => a -> [(Modality, Nat)]
  forcedVariables = foldMap forcedVariables

instance ForcedVariables a => ForcedVariables [a] where

-- Note the 'a' does not include the 'Arg' in 'Apply'.
instance ForcedVariables a => ForcedVariables (Elim' a) where
  forcedVariables (Apply x) = forcedVariables x
  forcedVariables Proj{} = []

instance ForcedVariables a => ForcedVariables (Arg a) where
  forcedVariables x = [ (m <> m', i) | (m', i) <- forcedVariables (unArg x) ]
    where m = getModality x

-- | Assumes that the term is in normal form.
instance ForcedVariables Term where
  forcedVariables t = case t of
    Var i [] -> [(mempty, i)]
    Con _ _ vs -> forcedVariables vs
    _ -> []

isForced :: IsForced -> Bool
isForced Forced    = True
isForced NotForced = False

nextIsForced :: [IsForced] -> (IsForced, [IsForced])
nextIsForced []     = (NotForced, [])
nextIsForced (f:fs) = (f, fs)

-----------------------------------------------------------------------------
-- * Forcing translation
-----------------------------------------------------------------------------

-- | Move bindings for forced variables to unforced positions.
forcingTranslation :: [NamedArg DeBruijnPattern] -> TCM [NamedArg DeBruijnPattern]
forcingTranslation ps = do
  (qs, rebind) <- dotForcedPatterns ps
  reportSDoc "tc.force" 50 $ text "forcingTranslation" <?> vcat
    [ text "patterns:" <?> pretty ps
    , text "dotted:  " <?> pretty qs
    , text "rebind:  " <?> pretty rebind ]
  rs <- foldM rebindForcedPattern qs rebind
  when (not $ null rebind) $ reportSDoc "tc.force" 50 $ nest 2 $ text "result:  " <?> pretty rs
  return rs

-- | Applies the forcing translation in order to update modalities of forced
--   arguments in the telescope. This is used before checking a right-hand side
--   in order to make sure all uses of forced arguments agree with the
--   relevance of the position where the variable will ultimately be bound.
--   Precondition: the telescope types the bound variables of the patterns.
forceTranslateTelescope :: Telescope -> [NamedArg DeBruijnPattern] -> TCM Telescope
forceTranslateTelescope delta qs = do
  qs' <- forcingTranslation qs
  let xms  = patternVarModalities qs
      xms' = patternVarModalities qs'
      old  = xms \\ xms'
      new  = xms' \\ xms
  if null new then return delta else do
      reportSLn "tc.force" 40 $ "Updating modalities of forced arguments\n" ++
                                "  from: " ++ show old ++ "\n" ++
                                "  to:   " ++ show new
      let mods    = map (first dbPatVarIndex) new
          ms      = reverse [ lookup i mods | i <- [0..size delta - 1] ]
          delta'  = telFromList $ zipWith (maybe id setModality) ms $ telToList delta
      reportSDoc "tc.force" 60 $ nest 2 $ text "delta' =" <?> prettyTCM delta'
      return delta'

-- | Rebind a forced pattern in a non-forced position. The forced pattern has
--   already been dotted by 'dotForcedPatterns', so the remaining task is to
--   find a dot pattern in an unforced position that can be turned into a
--   proper match of the forced pattern.
--
--   For instance (with patterns prettified to ease readability):
--
--    rebindForcedPattern [.(suc n), cons .n x xs] n = [suc n, cons .n x xs]
--
rebindForcedPattern :: [NamedArg DeBruijnPattern] -> DeBruijnPattern -> TCM [NamedArg DeBruijnPattern]
rebindForcedPattern ps toRebind = go $ zip (repeat NotForced) ps
  where
    targetDotP = patternToTerm toRebind

    go [] = __IMPOSSIBLE__ -- unforcing cannot fail
    go ((Forced,    p) : ps) = (p :) <$> go ps
    go ((NotForced, p) : ps) =
      case namedArg p of
        VarP{}   -> (p :) <$> go ps
        DotP _ v -> mkPat v >>= \ case
          Nothing -> (p :) <$> go ps
          Just q' -> return $ fmap (q' <$) p : map snd ps
        ConP c i qs -> do
          fqs <- withForced c qs
          qps <- go (fqs ++ ps)
          let (qs', ps') = splitAt (length qs) qps
          return $ fmap (ConP c i qs' <$) p : ps'
        LitP{}  -> (p :) <$> go ps
        ProjP{} -> (p :) <$> go ps

    withForced :: ConHead -> [a] -> TCM [(IsForced, a)]
    withForced c qs = do
      fs <- defForced <$> getConstInfo (conName c)
      return $ zip (fs ++ repeat NotForced) qs

    -- Try to turn a term in a dot pattern into a pattern matching q
    mkPat :: Term -> TCM (Maybe DeBruijnPattern)
    mkPat v = mkPat' (NotForced, v)

    mkPat' :: (IsForced, Term) -> TCM (Maybe DeBruijnPattern)
    mkPat' (Forced, _) = return Nothing
    mkPat' (NotForced, v) | targetDotP == v = return (Just toRebind)
    mkPat' (NotForced, v) =
      case v of
        Con c co es -> do
          let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
          fvs <- withForced c vs
          let fvs' = [ (f,) <$> a | (f, a) <- fvs ] :: [Arg (IsForced, Term)]
          -- It takes a bit of juggling to apply mkPat' under the the 'Arg's, but since it
          -- type checks, it's pretty much guaranteed to be the right thing.
          mps :: [Maybe (Arg DeBruijnPattern)] <- mapM (runMaybeT . traverse (MaybeT . mkPat')) fvs'
          case break (isJust . snd) (zip vs mps) of
            (mvs1, (_, Just p) : mvs2) -> do
              let vs1 = map fst mvs1
                  vs2 = map fst mvs2
                  ci = (toConPatternInfo co) { conPLazy = True }
                  dots = (map . fmap) dotP
              return $ Just $ ConP c ci $ doname $ dots vs1 ++ [p] ++ dots vs2
            _ -> return Nothing
        _ -> return Nothing
      where
        doname = (map . fmap) unnamed

-- | Dot all forced patterns and return a list of patterns that need to be
--   undotted elsewhere. Patterns that need to be undotted are those that bind
--   variables or does some actual (non-eta) matching.
dotForcedPatterns :: [NamedArg DeBruijnPattern] -> TCM ([NamedArg DeBruijnPattern], [DeBruijnPattern])
dotForcedPatterns ps = runWriterT $ (traverse . traverse . traverse) (forced NotForced) ps
  where
    forced :: IsForced -> DeBruijnPattern -> WriterT [DeBruijnPattern] TCM DeBruijnPattern
    forced f p =
      case p of
        DotP{}          -> return p
        ProjP{}         -> return p
        _ | f == Forced -> do
          properMatch <- isProperMatch p
          dotP (patternToTerm p) <$ tell [p | properMatch || length p > 0]
        VarP{}          -> return p
        LitP{}          -> return p
        ConP c i ps     -> do
          fs <- defForced <$> getConstInfo (conName c)
          ConP c i <$> zipWithM forcedArg (fs ++ repeat NotForced) ps

    forcedArg f = (traverse . traverse) (forced f)

    isProperMatch LitP{}  = return True
    isProperMatch VarP{}  = return False
    isProperMatch ProjP{} = return False
    isProperMatch DotP{}  = return False
    isProperMatch (ConP c i ps) =
      ifM (isEtaCon $ conName c)
          (anyM ps (isProperMatch . namedArg))
          (return True)