{-# LANGUAGE NoDeepSubsumption #-}
module Mikan.Termination.Masking (maskNonDataArgs) where

import Control.Monad.Trans.Maybe
import Control.Monad

import Data.List.NonEmpty (NonEmpty((:|)))
import Data.Monoid

import Mikan.Syntax.Common.Pretty (Pretty)
import Mikan.Syntax.Internal
import Mikan.Syntax.Common

import Mikan.TypeChecking.Monad.Signature
import Mikan.TypeChecking.Monad.Context
import Mikan.TypeChecking.Monad.Debug
import Mikan.TypeChecking.Monad.Base

import Mikan.TypeChecking.Positivity.Occurrence
import Mikan.TypeChecking.Free.Reduce
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Telescope
import Mikan.TypeChecking.Datatypes
import Mikan.TypeChecking.Records
import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.Pretty

import Mikan.Termination.Monad

import Mikan.Utils.VarSet qualified as VS
import Mikan.Utils.VarSet (VarSet)
import Mikan.Utils.StrictReader
import Mikan.Utils.Impossible
import Mikan.Utils.List1 (List1)
import Mikan.Utils.List
import Mikan.Utils.Size

-- | Compute the type of the constructor pattern at the given type, i.e.
-- applying it to the parameters recovered from @t@.
constructorType
  :: ConHead  -- ^ @con@
  -> Type     -- ^ @t@
  -> TCM (Type, Definition)
constructorType :: ConHead -> Type -> TCM (Type, Definition)
constructorType ConHead
c' Type
p_ty = do
  c_ty <- QName -> TCMT IO Type
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m Type
typeOfConst (ConHead -> QName
conName ConHead
c')
  reduce (unEl p_ty) >>= \case
    Def QName
d [Elim]
as | Just [Arg Term]
as <- [Elim] -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
as -> do
      dt_def <- QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d
      case theDef dt_def of
        Datatype{ dataMutual :: Defn -> Maybe [QName]
dataMutual = Maybe [QName]
g, dataPars :: Defn -> Nat
dataPars = Nat
n } -> (,) (Type -> Definition -> (Type, Definition))
-> TCMT IO Type -> TCMT IO (Definition -> (Type, Definition))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type
c_ty Type -> [Arg Term] -> TCMT IO Type
forall (m :: * -> *) a.
(MonadReduce m, HasBuiltins m, PiApplyArgs a) =>
Type -> a -> m Type
`piApplyM` Nat -> [Arg Term] -> [Arg Term]
forall a. Nat -> [a] -> [a]
take Nat
n [Arg Term]
as TCMT IO (Definition -> (Type, Definition))
-> TCMT IO Definition -> TCM (Type, Definition)
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Definition -> TCMT IO Definition
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Definition
dt_def
        Record{ recMutual :: Defn -> Maybe [QName]
recMutual = Maybe [QName]
g, recPars :: Defn -> Nat
recPars = Nat
n }     -> (,) (Type -> Definition -> (Type, Definition))
-> TCMT IO Type -> TCMT IO (Definition -> (Type, Definition))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type
c_ty Type -> [Arg Term] -> TCMT IO Type
forall (m :: * -> *) a.
(MonadReduce m, HasBuiltins m, PiApplyArgs a) =>
Type -> a -> m Type
`piApplyM` Nat -> [Arg Term] -> [Arg Term]
forall a. Nat -> [a] -> [a]
take Nat
n [Arg Term]
as TCMT IO (Definition -> (Type, Definition))
-> TCMT IO Definition -> TCM (Type, Definition)
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Definition -> TCMT IO Definition
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Definition
dt_def
        Defn
_ -> TCM (Type, Definition)
forall a. HasCallStack => a
__IMPOSSIBLE__
    Term
_ -> TCM (Type, Definition)
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Check whether the given type is a legitimate type for an argument
-- to be subject to structural termination.
--
-- This means that it must be a function type returning a data-or-record
-- type, and that the /parameters/ of the return do not depend on the
-- newly introduced variables, or on any of the given forbidden
-- variables.
--
-- Returns the function type if so, with the codomain reduced.
usableRecursiveType
  :: VarSet
    -- ^ Variables which can not appear in the parameters.
  -> Type
    -- ^ The type we want to check
  -> TCM (Maybe Type)
usableRecursiveType :: VarSet -> Type -> TCM (Maybe Type)
usableRecursiveType VarSet
forced Type
ty = MaybeT (TCMT IO) Type -> TCM (Maybe Type)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT do
  TelV tel t <- Type -> MaybeT (TCMT IO) (TelV Type)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath (Type -> MaybeT (TCMT IO) (TelV Type))
-> MaybeT (TCMT IO) Type -> MaybeT (TCMT IO) (TelV Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> MaybeT (TCMT IO) Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
ty
  t <- reduce t
  addContext tel do
    (dnm, args) <- case unEl t of
      Def QName
dnm [Elim]
args -> (QName, [Elim]) -> MaybeT (TCMT IO) (QName, [Elim])
forall a. a -> MaybeT (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName
dnm, [Elim]
args)
      Term
_            -> MaybeT (TCMT IO) (QName, [Elim])
forall a. MaybeT (TCMT IO) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

    npars <- MaybeT $ getNumberOfParameters dnm
    let
      !(pars, ixs) = splitAt' npars args
      !st          = Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel
      forbidden    = VarSet -> VarSet -> VarSet
VS.union (Nat -> VarSet
VS.full Nat
st) (Nat -> VarSet -> VarSet
VS.weaken Nat
st VarSet
forced)
    liftReduce (reallyFree forbidden pars) >>= \case
      Left Blocked_
blocked      -> Blocker -> MaybeT (TCMT IO) Type
forall a. Blocker -> MaybeT (TCMT IO) a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocked_ -> Blocker
forall t a. Blocked' t a -> Blocker
getBlocker Blocked_
blocked)
      Right (Just [Elim]
pars) -> Type -> MaybeT (TCMT IO) Type
forall a. a -> MaybeT (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> MaybeT (TCMT IO) Type) -> Type -> MaybeT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$! Tele (Dom Type) -> Type -> Type
telePi Tele (Dom Type)
tel (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ QName -> [Elim] -> Term
Def QName
dnm ([Elim]
pars [Elim] -> [Elim] -> [Elim]
forall a. [a] -> [a] -> [a]
++! [Elim]
ixs) Term -> Type -> Type
forall a b. a -> Type'' Term b -> Type'' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Type
t
      Right Maybe [Elim]
Nothing     -> MaybeT (TCMT IO) Type
forall a. MaybeT (TCMT IO) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

-- | Patterns that can be masked.
class MaskPatterns a where
  -- | Lens into the pattern
  toPattern :: Lens' a DeBruijnPattern

instance MaskPatterns DeBruijnPattern where toPattern :: Lens' DeBruijnPattern DeBruijnPattern
toPattern = (DeBruijnPattern -> f DeBruijnPattern)
-> DeBruijnPattern -> f DeBruijnPattern
forall a. a -> a
id
instance MaskPatterns (NamedArg DeBruijnPattern) where
  toPattern :: Lens' (NamedArg DeBruijnPattern) DeBruijnPattern
toPattern DeBruijnPattern -> f DeBruijnPattern
f (Arg ArgInfo
ai (Named Maybe NamedName
n DeBruijnPattern
p)) = DeBruijnPattern -> f DeBruijnPattern
f DeBruijnPattern
p f DeBruijnPattern
-> (DeBruijnPattern -> NamedArg DeBruijnPattern)
-> f (NamedArg DeBruijnPattern)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \DeBruijnPattern
x -> ArgInfo
-> Named NamedName DeBruijnPattern -> NamedArg DeBruijnPattern
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Maybe NamedName
-> DeBruijnPattern -> Named NamedName DeBruijnPattern
forall name a. Maybe name -> a -> Named name a
Named Maybe NamedName
n DeBruijnPattern
x)

toElim :: MaskPatterns a => a -> Elim
toElim :: forall a. MaskPatterns a => a -> Elim
toElim = Arg DeBruijnPattern -> Elim
patternToElim (Arg DeBruijnPattern -> Elim)
-> (a -> Arg DeBruijnPattern) -> a -> Elim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijnPattern -> Arg DeBruijnPattern
forall a. a -> Arg a
defaultArg (DeBruijnPattern -> Arg DeBruijnPattern)
-> (a -> DeBruijnPattern) -> a -> Arg DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting DeBruijnPattern a DeBruijnPattern -> a -> DeBruijnPattern
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting DeBruijnPattern a DeBruijnPattern
forall a. MaskPatterns a => Lens' a DeBruijnPattern
Lens' a DeBruijnPattern
toPattern

mask :: MaskPatterns a => a -> a
mask :: forall a. MaskPatterns a => a -> a
mask = ASetter a a DeBruijnPattern DeBruijnPattern
-> (DeBruijnPattern -> DeBruijnPattern) -> a -> a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter a a DeBruijnPattern DeBruijnPattern
forall a. MaskPatterns a => Lens' a DeBruijnPattern
Lens' a DeBruijnPattern
toPattern \case
  x :: DeBruijnPattern
x@ProjP{} -> DeBruijnPattern
x
  DeBruijnPattern
x         -> DeBruijnPattern -> DeBruijnPattern
forall x. Pattern' x -> Pattern' x
MaskP DeBruijnPattern
x

-- | Return 'True' if any of the patterns in the argument is a 'DotP',
-- i.e. if this pattern has had its value forced by matching on an
-- indexed inductive type.
isForced :: MaskPatterns a => a -> Bool
isForced :: forall a. MaskPatterns a => a -> Bool
isForced a
pat =
  let
    is :: DeBruijnPattern -> Any
    is :: DeBruijnPattern -> Any
is = \case
      DotP{} -> Bool -> Any
Any Bool
True
      DeBruijnPattern
_      -> Any
forall a. Monoid a => a
mempty
  in Any -> Bool
getAny (Any -> Bool) -> Any -> Bool
forall a b. (a -> b) -> a -> b
$ (DeBruijnPattern -> Any) -> DeBruijnPattern -> Any
forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m) -> b -> m
foldPattern DeBruijnPattern -> Any
is (a
pat a -> Getting DeBruijnPattern a DeBruijnPattern -> DeBruijnPattern
forall s a. s -> Getting a s a -> a
^. Getting DeBruijnPattern a DeBruijnPattern
forall a. MaskPatterns a => Lens' a DeBruijnPattern
Lens' a DeBruijnPattern
toPattern)

-- | Helper type for the data that needs to be adjusted across a
-- 'HandlePi'.
data Masking = M
  { Masking -> VarSet
_mForced :: !VarSet
    -- ^ The set of variables in the context built by typed masking that
    -- correspond to dot patterns, i.e. forced arguments.
    --
    -- These variables can not appear in the parameters of data types
    -- that we want to do recursion on (mikan#115).
  , Masking -> Term
_mTerm   :: !Term
    -- ^ An accumulator term consisting of the head that we called
    -- 'maskNonDataArgs' for, applied to the patterns we have masked so
    -- far.
  }

type HandlePi a = forall b. a -> Masking -> (Dom Type, Abs Type) -> (Masking -> Type -> TCM b) -> TCM b

-- | Treat application patterns as though they were fresh variables.
handleAsNeutral :: MaskPatterns a => HandlePi a
handleAsNeutral :: forall a. MaskPatterns a => HandlePi a
handleAsNeutral a
p (M VarSet
forced Term
acc_tm) (Dom Type
dom, Abs Type
abs) Masking -> Type -> TCM b
cont = Dom Type -> Abs Type -> (Type -> TCM b) -> TCM b
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs Dom Type
dom Abs Type
abs \Type
ty ->
  let
    !m' :: Masking
m' = M
      -- this and underAbstractionAbs have pretty bad asymptotics but we
      -- really do need to track all the binders, and this is the
      -- easiest way to build the accumulator term correctly.
      { _mTerm :: Term
_mTerm   = Nat -> Term -> Term
forall a. Subst a => Nat -> a -> a
raise Nat
1 Term
acc_tm Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Dom' Term Term -> Arg Term
forall t a. Dom' t a -> Arg a
argFromDom (Nat -> Term
var Nat
0 Term -> Dom Type -> Dom' Term Term
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type
dom)]
      -- weaken the forced variables by 1, but also mark this binder as
      -- "corresponding to a forced pattern" if it has a DotP.
      , _mForced :: VarSet
_mForced = if DeBruijnPattern -> Bool
forall a. MaskPatterns a => a -> Bool
isForced (a
p a -> Getting DeBruijnPattern a DeBruijnPattern -> DeBruijnPattern
forall s a. s -> Getting a s a -> a
^. Getting DeBruijnPattern a DeBruijnPattern
forall a. MaskPatterns a => Lens' a DeBruijnPattern
Lens' a DeBruijnPattern
toPattern)
          then Nat -> VarSet -> VarSet
VS.insert Nat
0 (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$ Nat -> VarSet -> VarSet
VS.weaken Nat
1 VarSet
forced
          else Nat -> VarSet -> VarSet
VS.weaken Nat
1 VarSet
forced
      }
  in Masking -> Type -> TCM b
cont Masking
m' Type
ty

-- | Treat application patterns by their values.
handleAsValue :: MaskPatterns a => HandlePi a
handleAsValue :: forall a. MaskPatterns a => HandlePi a
handleAsValue a
p (M VarSet
forced Term
acc_tm) (Dom Type
dom, Abs Type
abs) Masking -> Type -> TCM b
go =
  let m' :: Term -> Masking
m' Term
t = VarSet -> Term -> Masking
M VarSet
forced (Term
acc_tm Term -> Term -> Term
forall t. Apply t => t -> Term -> t
`apply1` Term
t) in
  case a -> Elim
forall a. MaskPatterns a => a -> Elim
toElim a
p of
    Apply (Arg ArgInfo
_ Term
t) -> Masking -> Type -> TCM b
go (Term -> Masking
m' Term
t) (Abs Type
abs Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`lazyAbsApp` Term
SubstArg Type
t)
    IApply Term
_ Term
_   Term
t  -> Masking -> Type -> TCM b
go (Term -> Masking
m' Term
t) (Abs Type
abs Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`lazyAbsApp` Term
SubstArg Type
t)
    Proj{}          -> String -> TCM b
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
"maskPatterns (NamedArg DeBruijnPattern): handlePi got pattern that became Proj?"

-- | Actual implementation of 'maskNonDataArgs'.
maskArgumentList
  :: forall a. MaskPatterns a
  => HandlePi a -- ^ How to handle nested argument lists.
  -> Term       -- ^ A term to accumulate eliminations (needed for copattern matching)
  -> Type       -- ^ The type of the term
  -> [a] -> TCM [a]
maskArgumentList :: forall a.
MaskPatterns a =>
HandlePi a -> Term -> Type -> [a] -> TCM [a]
maskArgumentList HandlePi a
handlePi Term
init_tm Type
init_ty [a]
args = do
  let
    pi :: List1 a -> Masking -> Type -> TCM [a]
    pi :: List1 a -> Masking -> Type -> TCM [a]
pi (a
p :| [a]
ps) acc :: Masking
acc@(M VarSet
forced Term
acc_tm) Type
ty = Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
ty TCMT IO Type
-> (Type -> TCMT IO (Either (Dom Type, Abs Type) Type))
-> TCMT IO (Either (Dom Type, Abs Type) Type)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> TCMT IO (Either (Dom Type, Abs Type) Type)
forall (m :: * -> *).
HasBuiltins m =>
Type -> m (Either (Dom Type, Abs Type) Type)
piOrPath TCMT IO (Either (Dom Type, Abs Type) Type)
-> (Either (Dom Type, Abs Type) Type -> TCM [a]) -> TCM [a]
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Left (Dom Type
dom, Abs Type
abs) -> do
        String -> Nat -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"term.mask" Nat
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"pattern is application and type is function"
          , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
4 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"dom    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM Dom Type
dom
          , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
4 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"abs    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Abs Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Abs Type -> m Doc
prettyTCM Abs Type
abs
          , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
4 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"forced =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM ((Nat -> Term) -> [Nat] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Nat -> Term
var (VarSet -> [Nat]
VS.toAscList VarSet
forced))
          , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
4 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"p      =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> DeBruijnPattern -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DeBruijnPattern -> m Doc
prettyTCM (a
p a -> Getting DeBruijnPattern a DeBruijnPattern -> DeBruijnPattern
forall s a. s -> Getting a s a -> a
^. Getting DeBruijnPattern a DeBruijnPattern
forall a. MaskPatterns a => Lens' a DeBruijnPattern
Lens' a DeBruijnPattern
toPattern)
          ]

        p' <- VarSet -> Type -> TCM (Maybe Type)
usableRecursiveType VarSet
forced (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom) TCM (Maybe Type) -> (Maybe Type -> TCMT IO a) -> TCMT IO a
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Just Type
t  -> (DeBruijnPattern -> TCMT IO DeBruijnPattern) -> a -> TCMT IO a
forall a. MaskPatterns a => Lens' a DeBruijnPattern
Lens' a DeBruijnPattern
toPattern (Type -> DeBruijnPattern -> TCMT IO DeBruijnPattern
maskNonDataArgsInPattern Type
t) a
p
          Maybe Type
Nothing -> a -> TCMT IO a
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> TCMT IO a) -> a -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. MaskPatterns a => a -> a
mask a
p

        reportSDoc "term.mask" 30 $ nest 4 $ "p'     =" <+> prettyTCM (p' ^. toPattern)

        (:) p' <$> handlePi p acc (dom, abs) \Masking
tm Type
ty -> Masking -> Type -> [a] -> TCM [a]
go Masking
tm Type
ty [a]
ps

      Right{} -> [a] -> TCM [a]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([a] -> TCM [a]) -> [a] -> TCM [a]
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. MaskPatterns a => a -> a
mask a
pa -> [a] -> [a]
forall a. a -> [a] -> [a]
:(a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map a -> a
forall a. MaskPatterns a => a -> a
mask [a]
ps

    go :: Masking -> Type -> [a] -> TCM [a]
    go :: Masking -> Type -> [a] -> TCM [a]
go m :: Masking
m@(M VarSet
forced Term
acc_tm) Type
ty (a
p:[a]
ps) = do
      let ef :: Elim
ef = a -> Elim
forall a. MaskPatterns a => a -> Elim
toElim a
p
      String -> Nat -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"term.mask" Nat
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"maskArgumentList" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> DeBruijnPattern -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DeBruijnPattern -> m Doc
prettyTCM (a
p a -> Getting DeBruijnPattern a DeBruijnPattern -> DeBruijnPattern
forall s a. s -> Getting a s a -> a
^. Getting DeBruijnPattern a DeBruijnPattern
forall a. MaskPatterns a => Lens' a DeBruijnPattern
Lens' a DeBruijnPattern
toPattern)
        , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"t =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
ty
        , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"a =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
acc_tm
        , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"e =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elim -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim -> m Doc
prettyTCM Elim
ef
        ]
      case Elim
ef of
        Apply{}  -> List1 a -> Masking -> Type -> TCM [a]
pi (a
p a -> [a] -> List1 a
forall a. a -> [a] -> NonEmpty a
:| [a]
ps) Masking
m Type
ty
        IApply{} -> List1 a -> Masking -> Type -> TCM [a]
pi (a
p a -> [a] -> List1 a
forall a. a -> [a] -> NonEmpty a
:| [a]
ps) Masking
m Type
ty
        Proj ProjOrigin
o QName
pf -> do
          rest <- Term
-> Type
-> ProjOrigin
-> QName
-> TCMT IO (Maybe (Dom Type, Term, Type))
forall (m :: * -> *).
PureTCM m =>
Term
-> Type -> ProjOrigin -> QName -> m (Maybe (Dom Type, Term, Type))
projectTyped Term
acc_tm Type
ty ProjOrigin
o QName
pf TCMT IO (Maybe (Dom Type, Term, Type))
-> (Maybe (Dom Type, Term, Type) -> TCM [a]) -> TCM [a]
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Just (Dom Type
_, Term
acc_tm', Type
ty') -> Masking -> Type -> [a] -> TCM [a]
go (VarSet -> Term -> Masking
M VarSet
forced Term
acc_tm') Type
ty' [a]
ps
            Maybe (Dom Type, Term, Type)
Nothing                -> [a] -> TCM [a]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([a] -> TCM [a]) -> [a] -> TCM [a]
forall a b. (a -> b) -> a -> b
$ (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map a -> a
forall a. MaskPatterns a => a -> a
mask [a]
ps
          pure $ p:rest
    go Masking
_ Type
_ [] = [a] -> TCM [a]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

  String -> Nat -> String -> TCM [a] -> TCM [a]
forall a. String -> Nat -> String -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
String -> Nat -> String -> m a -> m a
verboseBracket String
"term.mask" Nat
20 String
"maskArgumentList" do
    String -> Nat -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"term.mask" Nat
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"masking argument list"
      , TCMT IO Doc
"  ps:     " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [DeBruijnPattern] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [DeBruijnPattern] -> m Doc
prettyTCM ([a]
args [a] -> (a -> DeBruijnPattern) -> [DeBruijnPattern]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Getting DeBruijnPattern a DeBruijnPattern -> a -> DeBruijnPattern
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting DeBruijnPattern a DeBruijnPattern
forall a. MaskPatterns a => Lens' a DeBruijnPattern
Lens' a DeBruijnPattern
toPattern)
      , TCMT IO Doc
"  init_tm:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
init_tm
      , TCMT IO Doc
"  init_ty:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
init_ty
      ]
    Masking -> Type -> [a] -> TCM [a]
go (VarSet -> Term -> Masking
M VarSet
forall a. Monoid a => a
mempty Term
init_tm) Type
init_ty [a]
args

{-# SPECIALISE maskArgumentList :: HandlePi DeBruijnPattern -> Term -> Type -> [DeBruijnPattern] -> TCM [DeBruijnPattern] #-}
{-# SPECIALISE maskArgumentList :: HandlePi (NamedArg DeBruijnPattern) -> Term -> Type -> NAPs -> TCM NAPs #-}

-- | Mask any application patterns that match against a type that is not
-- a data/record type; see issues agda#1023, agda#5910. The returned
-- list always has the same number of elements of the input.
--
-- The behaviour of this function when computing the type to be used for
-- the remainder of a pattern telescope is different between the
-- top-level (the 'DeBruijnPattern' instance) and in constructor
-- patterns below that ('maskNonDataArgsInPattern').
--
-- At toplevel, application patterns are treated as *neutrals* when
-- computing the type to be used for the rest of the patterns. This is
-- needed for agda#1023: after applying the first two arguments, the
-- function looks like
-- @
--   noo .WOne (Refl) : WOne → Zero
-- @
-- so the next pattern @wrap f@ would be treated as a datatype and
-- considered for structural recursion, which allows the proof of false
-- to go through.
--
-- When masking *inside* a constructor pattern, the arguments are
-- treated as values. An example for the necessity of this difference is
-- in @test/Succeed/MaskSigmaRecursion@. However, if this is allowed for
-- *indexed* types, we recover a variant of @Issue5910@ again.
-- Therefore, we only allow this for types that use all of their
-- arguments with non-mixed positivity, see @test/fail/Issue5910IxC@.
--
-- If at any point it becomes impossible to compute the type of the rest
-- of the telescope (e.g. because, at top-level, a pattern was skipped,
-- and the function has a computed type from then on), every following
-- (non-projection) pattern is treated as masked (see
-- @test/Fail/MaskingComputedType@).

maskNonDataArgs :: Type -> [DeBruijnPattern] -> TerM [DeBruijnPattern]
maskNonDataArgs :: Type -> [DeBruijnPattern] -> TerM [DeBruijnPattern]
maskNonDataArgs Type
ty [DeBruijnPattern]
naps = do
  f    <- TerM QName
terGetCurrent
  f_ty <- typeOfConst f
  liftTCM $ maskArgumentList handleAsNeutral (Def f []) f_ty naps

maskNonDataArgsInPattern :: Type -> DeBruijnPattern -> TCM DeBruijnPattern
maskNonDataArgsInPattern :: Type -> DeBruijnPattern -> TCMT IO DeBruijnPattern
maskNonDataArgsInPattern Type
ty DeBruijnPattern
pat = case DeBruijnPattern
pat of
  VarP{}    -> DeBruijnPattern -> TCMT IO DeBruijnPattern
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DeBruijnPattern
pat
  DotP{}    -> DeBruijnPattern -> TCMT IO DeBruijnPattern
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DeBruijnPattern
pat
  LitP{}    -> DeBruijnPattern -> TCMT IO DeBruijnPattern
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DeBruijnPattern
pat
  ProjP{}   -> DeBruijnPattern -> TCMT IO DeBruijnPattern
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DeBruijnPattern
pat
  IApplyP{} -> DeBruijnPattern -> TCMT IO DeBruijnPattern
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DeBruijnPattern
pat

  DefP{}    -> TCMT IO DeBruijnPattern
forall a. HasCallStack => a
__IMPOSSIBLE__
  MaskP{}   -> TCMT IO DeBruijnPattern
forall a. HasCallStack => a
__IMPOSSIBLE__

  ConP ConHead
hd ConPatternInfo
cpi [NamedArg DeBruijnPattern]
naps -> do
    (c_ty, con) <- ConHead -> Type -> TCM (Type, Definition)
constructorType ConHead
hd Type
ty
    reportSDoc "term.mask" 30 $ vcat
      [ "maskNonDataArgsInPattern" <+> prettyTCM pat
      , "  data positivity:" <+> prettyTCM (defArgOccurrences con)
      , "         will use?" <+> prettyTCM (map (Mixed <) (defArgOccurrences con))
      ]
    ConP hd cpi <$> if all (Mixed <) (defArgOccurrences con)
      then maskArgumentList handleAsValue   (Con hd ConOSystem []) c_ty naps
      else maskArgumentList handleAsNeutral (Con hd ConOSystem []) c_ty naps