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