{-| 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
@

This module implements the analysis of which constructor arguments are forced. The process of moving
the binding site of forced arguments is implemented in the unifier (see the Solution step of
Agda.TypeChecking.Rules.LHS.Unify.unifyStep).

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
  ( computeForcingAnnotations,
    isForced,
    nextIsForced ) where

import Data.Monoid -- for (<>) in GHC 8.0.2

import Agda.Interaction.Options

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

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope

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

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 :: QName -> Type -> TCM [IsForced]
computeForcingAnnotations :: QName -> Type -> TCM [IsForced]
computeForcingAnnotations QName
c Type
t =
  TCMT IO Bool -> TCM [IsForced] -> TCM [IsForced] -> TCM [IsForced]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (PragmaOptions -> Bool
optForcing (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions {-then-}) ([IsForced] -> TCM [IsForced]
forall (m :: * -> *) a. Monad m => a -> m a
return []) (TCM [IsForced] -> TCM [IsForced])
-> TCM [IsForced] -> TCM [IsForced]
forall a b. (a -> b) -> a -> b
$ {-else-} 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.
    Type
t <- Type -> TCMT IO Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
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 Tele (Dom Type)
tel (El Sort' Term
_ Term
a) <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
t
    let vs :: Elims
vs = case Term
a of
          Def QName
_ Elims
us -> Elims
us
          Term
_        -> Elims
forall a. HasCallStack => a
__IMPOSSIBLE__
        n :: Nat
n = Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel
        xs :: [(Modality, Nat)]
        xs :: [(Modality, Nat)]
xs = Elims -> [(Modality, Nat)]
forall a. ForcedVariables a => a -> [(Modality, Nat)]
forcedVariables Elims
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 in that
        -- case it isn't really forced.
        isForced :: Modality -> Nat -> Bool
        isForced :: Modality -> Nat -> Bool
isForced Modality
m Nat
i =
               (Modality -> Bool
forall a. LensQuantity a => a -> Bool
hasQuantity0 Modality
m Bool -> Bool -> Bool
|| Modality -> Bool
forall a. LensQuantity a => a -> Bool
noUserQuantity Modality
m)
            Bool -> Bool -> Bool
&& (Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
m Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
/= Relevance
Irrelevant)
            Bool -> Bool -> Bool
&& ((Modality, Nat) -> Bool) -> [(Modality, Nat)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(Modality
m', Nat
j) -> Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
j
            Bool -> Bool -> Bool
&& Modality
m' Modality -> Modality -> Bool
`moreUsableModality` Modality
m) [(Modality, Nat)]
xs
        forcedArgs :: [IsForced]
forcedArgs =
          [ if Modality -> Nat -> Bool
isForced Modality
m Nat
i then IsForced
Forced else IsForced
NotForced
          | (Nat
i, Modality
m) <- [Nat] -> [Modality] -> [(Nat, Modality)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom Nat
n) ([Modality] -> [(Nat, Modality)])
-> [Modality] -> [(Nat, Modality)]
forall a b. (a -> b) -> a -> b
$ (Dom (ArgName, Type) -> Modality)
-> [Dom (ArgName, Type)] -> [Modality]
forall a b. (a -> b) -> [a] -> [b]
map Dom (ArgName, Type) -> Modality
forall a. LensModality a => a -> Modality
getModality (Tele (Dom Type) -> [Dom (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
tel)
          ]
    ArgName -> Nat -> [ArgName] -> TCMT IO ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
ArgName -> Nat -> a -> m ()
reportS ArgName
"tc.force" Nat
60
      [ ArgName
"Forcing analysis for " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ QName -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow QName
c
      , ArgName
"  xs          = " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ [Nat] -> ArgName
forall a. Show a => a -> ArgName
show (((Modality, Nat) -> Nat) -> [(Modality, Nat)] -> [Nat]
forall a b. (a -> b) -> [a] -> [b]
map (Modality, Nat) -> Nat
forall a b. (a, b) -> b
snd [(Modality, Nat)]
xs)
      , ArgName
"  forcedArgs  = " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ [IsForced] -> ArgName
forall a. Show a => a -> ArgName
show [IsForced]
forcedArgs
      ]
    [IsForced] -> TCM [IsForced]
forall (m :: * -> *) a. Monad m => a -> m a
return [IsForced]
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 = (b -> [(Modality, Nat)]) -> t b -> [(Modality, Nat)]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap b -> [(Modality, Nat)]
forall a. ForcedVariables a => a -> [(Modality, Nat)]
forcedVariables

instance ForcedVariables a => ForcedVariables [a] where

-- Note that the 'a' does not include the 'Arg' in 'Apply'.
instance ForcedVariables a => ForcedVariables (Elim' a) where
  forcedVariables :: Elim' a -> [(Modality, Nat)]
forcedVariables (Apply Arg a
x) = Arg a -> [(Modality, Nat)]
forall a. ForcedVariables a => a -> [(Modality, Nat)]
forcedVariables Arg a
x
  forcedVariables IApply{}  = []  -- No forced variables in path applications
  forcedVariables Proj{}    = []

instance ForcedVariables a => ForcedVariables (Arg a) where
  forcedVariables :: Arg a -> [(Modality, Nat)]
forcedVariables Arg a
x = [ (Modality -> Modality -> Modality
composeModality Modality
m Modality
m', Nat
i) | (Modality
m', Nat
i) <- a -> [(Modality, Nat)]
forall a. ForcedVariables a => a -> [(Modality, Nat)]
forcedVariables (Arg a -> a
forall e. Arg e -> e
unArg Arg a
x) ]
    where m :: Modality
m = Arg a -> Modality
forall a. LensModality a => a -> Modality
getModality Arg a
x

-- | Assumes that the term is in normal form.
instance ForcedVariables Term where
  forcedVariables :: Term -> [(Modality, Nat)]
forcedVariables = \case
    Var Nat
i [] -> [(Modality
unitModality, Nat
i)]
    Con ConHead
_ ConInfo
_ Elims
vs -> Elims -> [(Modality, Nat)]
forall a. ForcedVariables a => a -> [(Modality, Nat)]
forcedVariables Elims
vs
    Term
_ -> []

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

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