module Mikan.TypeChecking.Rules.WithApp (checkWithAppHead, checkWithApplication) where

import Prelude hiding ( null )

import Control.DeepSeq

import GHC.Generics

import Mikan.Syntax.Abstract qualified as A
import Mikan.Syntax.Info qualified as A
import Mikan.Syntax.Concrete.Pretty ()
import Mikan.Syntax.Common
import Mikan.Syntax.Fixity
import Mikan.Syntax.Internal as I

import Mikan.TypeChecking.MetaVars
import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Telescope
import Mikan.TypeChecking.Conversion
import Mikan.TypeChecking.Constraints

import {-# SOURCE #-} Mikan.TypeChecking.Rules.Application
import Mikan.TypeChecking.CheckInternal (CheckInternal(checkInternal'), defaultAction)

import Mikan.Utils.List
import Mikan.Utils.List1  ( List1, pattern (:|) )
import Mikan.Utils.List1 qualified as List1
import Mikan.Utils.Monad
import Mikan.Utils.Size

import Mikan.Utils.Impossible

-- Entry point for checking a with-application @e | es@.
--
-- The expression on the left is given after its elaboration. This
-- function checks whether it is a valid head for a @with@-application
-- and, if so, proceeds to check the arguments, as per
-- 'checkWithApplication'.
checkWithAppHead
  :: Comparison   -- ^ How to check the target type
  -> Type         -- ^ Expected type
  -> A.Expr       -- ^ Abstract expression from which @tm@ was elaborated, used for error reporting
  -> Term         -- ^ The term @tm@ we want to apply
  -> List1 A.Expr -- ^ Nonempty list of "piped" expressions
  -> TCM Term
checkWithAppHead :: Comparison -> Type -> Expr -> Term -> List1 Expr -> TCM Term
checkWithAppHead Comparison
cmp Type
t Expr
e Term
tm List1 Expr
es = do
  tm <- Term -> Term
stripDontCare (Term -> Term) -> TCM Term -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCM Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
tm
  case tm of
    Def QName
hd Elims
as  -> Comparison
-> Type -> WithAppHead -> QName -> Elims -> List1 Expr -> TCM Term
checkWithApplication Comparison
cmp Type
t (QName -> Expr -> WithAppHead
WithAppHead QName
hd Expr
e) QName
hd Elims
as List1 Expr
es
    MetaV MetaId
mv Elims
_ -> TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem (Comparison
-> Type -> Expr -> Term -> List1 Expr -> TypeCheckingProblem
CheckWithAppHead Comparison
cmp Type
t Expr
e Term
tm List1 Expr
es) (MetaId -> Blocker
unblockOnMeta MetaId
mv)
    Dummy{}    -> TCM Term
forall a. HasCallStack => a
__IMPOSSIBLE__
    Term
_          -> WithAppError -> TCM Term
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (WithAppError -> TCM Term) -> WithAppError -> TCM Term
forall a b. (a -> b) -> a -> b
$ Term -> WithAppError
NotWithAppHead Term
tm

appWithAppHead :: WithAppHead -> [A.Expr] -> WithAppHead
appWithAppHead :: WithAppHead -> [Expr] -> WithAppHead
appWithAppHead WithAppHead
_ [] = WithAppHead
forall a. HasCallStack => a
__IMPOSSIBLE__
appWithAppHead (WithAppHead QName
qn Expr
ex) (Expr
e:[Expr]
es) = QName -> Expr -> WithAppHead
WithAppHead QName
qn (Expr -> WithAppHead) -> Expr -> WithAppHead
forall a b. (a -> b) -> a -> b
$ ExprInfo -> Expr -> List1 Expr -> Expr
A.WithApp ExprInfo
A.exprNoRange Expr
ex (Expr
e Expr -> [Expr] -> List1 Expr
forall a. a -> [a] -> NonEmpty a
:| [Expr]
es)

-- | Check that an application of a defined name to some eliminations
-- can be the head of a @with@-application, and elaborate the given
-- abstract expressions into arguments for the corresponding
-- @with@-function.
--
-- The application @f es0@ of the head symbol should reduce in a single
-- step of co/pattern matching (see 'unfoldDefinitionStep') to a
-- @with@-function associated to @f@. This is a liberal approximation to
-- "@es0@ matches a @with@-clause of @f@" that is guaranteed not to
-- diverge from the implementation of pattern matching used for ordinary
-- reduction, but it does technically allow re-applying a recursive
-- @with@-application of @f@.
--
-- Finally, check that the part of the head function's telescope that
-- was abstracted of the @with@-expressions remains valid with the new
-- arguments, and that the overall expression has the given target type.
checkWithApplication
  :: Comparison    -- ^ How to check the target type
  -> Type          -- ^ Expected type
  -> WithAppHead   -- ^ Head expression, used for error reporting; shape does not matter
  -> QName         -- ^ Head symbol @f@ of the left-hand side
  -> Elims         -- ^ Checked eliminations @es0@ on the head symbol
  -> List1 A.Expr  -- ^ Nonempty list of "piped" expressions
  -> TCM Term
checkWithApplication :: Comparison
-> Type -> WithAppHead -> QName -> Elims -> List1 Expr -> TCM Term
checkWithApplication Comparison
cmp Type
t WithAppHead
hd QName
fn Elims
as List1 Expr
es = do
  VerboseKey -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.term.with" Int
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
"type checking with-application" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (WithAppHead -> Expr
wahExpr WithAppHead
hd)
    , TCMT IO Doc
"fn =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
fn
    , TCMT IO Doc
"as =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elims -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elims -> m Doc
prettyTCM Elims
as
    , TCMT IO Doc
"es =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> List1 Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA List1 Expr
es
    ]
  QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
fn TCMT IO Definition -> (Definition -> Defn) -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Definition -> Defn
theDef TCMT IO Defn -> (Defn -> TCMT IO ()) -> TCMT IO ()
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
    Function{} -> () -> TCMT IO ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Defn
def        -> WithAppError -> TCMT IO ()
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (WithAppError -> TCMT IO ()) -> WithAppError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ QName -> Defn -> WithAppError
WithAppNonFun QName
fn Defn
def

  -- we want to apply exactly the necessary amount of reduction to
  -- reduce fn to one of its right-hand sides.
  ReduceM (Reduced (Blocked Term) Term)
-> TCMT IO (Reduced (Blocked Term) Term)
forall a. ReduceM a -> TCMT IO a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (Term -> QName -> Elims -> ReduceM (Reduced (Blocked Term) Term)
unfoldDefinitionStep (QName -> Elims -> Term
Def QName
fn []) QName
fn Elims
as) TCMT IO (Reduced (Blocked Term) Term)
-> (Reduced (Blocked Term) Term -> TCM Term) -> TCM Term
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
    -- getting stuck is either grounds for postponement (stuck on a meta
    -- or a definition-in-progress) or for an error.
    NoReduction (Blocked Blocker
blk Term
_) -> TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem (Comparison
-> Type
-> WithAppHead
-> QName
-> Elims
-> List1 Expr
-> TypeCheckingProblem
CheckWithApp Comparison
cmp Type
t WithAppHead
hd QName
fn Elims
as List1 Expr
es) Blocker
blk
    NoReduction (NotBlocked NotBlocked' Term
notb Term
d) -> case NotBlocked' Term
notb of
      -- possible if the context is absurd and we have @foo {! false !} | bar@
      NotBlocked' Term
AbsurdMatch      -> WithAppError -> TCM Term
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (WithAppError -> TCM Term) -> WithAppError -> TCM Term
forall a b. (a -> b) -> a -> b
$ WithAppHead -> QName -> Elims -> WithAppError
WithAppAbsurd WithAppHead
hd QName
fn Elims
as
      -- possible if the definition is by pattern-matching and the
      -- matched argument hasn't been supplied
      NotBlocked' Term
Underapplied     -> WithAppError -> TCM Term
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (WithAppError -> TCM Term) -> WithAppError -> TCM Term
forall a b. (a -> b) -> a -> b
$ WithAppHead -> QName -> Elims -> WithAppError
WithAppUndersat WithAppHead
hd QName
fn Elims
as
      -- possible if the definition is by pattern-matching and the
      -- matched argument is neutral
      StuckOn Elim' Term
e        -> WithAppError -> TCM Term
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (WithAppError -> TCM Term) -> WithAppError -> TCM Term
forall a b. (a -> b) -> a -> b
$ WithAppHead -> QName -> Elims -> Elim' Term -> WithAppError
WithAppNeutral WithAppHead
hd QName
fn Elims
as Elim' Term
e

      -- possible if us and the definition are in the same mutual block
      -- and the definition has not yet been checked
      NotBlocked' Term
ReallyNotBlocked -> case Term
d of
        Def QName
d0 Elims
_ -> TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem (Comparison
-> Type
-> WithAppHead
-> QName
-> Elims
-> List1 Expr
-> TypeCheckingProblem
CheckWithApp Comparison
cmp Type
t WithAppHead
hd QName
fn Elims
as List1 Expr
es) (QName -> Blocker
unblockOnDef QName
d0)
        Term
_        -> TCM Term
forall a. HasCallStack => a
__IMPOSSIBLE__ -- should not be possible.

      MissingClauses QName
d -> TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem (Comparison
-> Type
-> WithAppHead
-> QName
-> Elims
-> List1 Expr
-> TypeCheckingProblem
CheckWithApp Comparison
cmp Type
t WithAppHead
hd QName
fn Elims
as List1 Expr
es) (QName -> Blocker
unblockOnDef QName
d)

    -- if the reduct is headed by a definition, we can actually proceed.
    YesReduction Simplification
_ (Term -> Term
stripDontCare -> Def QName
withfun Elims
wargs) -> do
      withdef <- QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
withfun
      -- first we have to retrieve the data necessary for type-checking
      -- es, while also making sure that the new head is a with-function
      -- generated from a clause of fn.
      (parent, delta1, nargs) <- case theDef withdef of
        Function{ funWith :: Defn -> WithFunInfo
funWith = WithFunInfo QName
p Telescope
d1 Int
w }
          | QName
p QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
fn   -> (QName, Telescope, Int) -> TCMT IO (QName, Telescope, Int)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName
p, Telescope
d1, Int
w)
          | Bool
otherwise -> WithAppError -> TCMT IO (QName, Telescope, Int)
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (WithAppError -> TCMT IO (QName, Telescope, Int))
-> WithAppError -> TCMT IO (QName, Telescope, Int)
forall a b. (a -> b) -> a -> b
$ WithAppHead -> QName -> Elims -> ReductNotWithFun -> WithAppError
WithAppReductNotDef WithAppHead
hd QName
fn Elims
as (QName -> Term -> ReductNotWithFun
OtherWithFun QName
p (QName -> Elims -> Term
Def QName
withfun Elims
wargs))
        Defn
_ -> WithAppError -> TCMT IO (QName, Telescope, Int)
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (WithAppError -> TCMT IO (QName, Telescope, Int))
-> WithAppError -> TCMT IO (QName, Telescope, Int)
forall a b. (a -> b) -> a -> b
$ WithAppHead -> QName -> Elims -> ReductNotWithFun -> WithAppError
WithAppReductNotDef WithAppHead
hd QName
fn Elims
as (QName -> Defn -> ReductNotWithFun
NotWithFun QName
withfun (Definition -> Defn
theDef Definition
withdef))

      -- the arguments to a with rhs are variables from the clause
      -- telescope necessary for checking the scrutinees, then those
      -- expressions themselves (which we are replacing), and finally
      -- the variables corresponding to patterns that the scrutinee
      -- either appears in or is independent of.
      let
        (d1args, drop nargs -> d2args) = splitAt' (size delta1) wargs
        (here, there) = splitAt' nargs (List1.toList es)

      unless (length here == nargs) $
        typeError $ WithAppNotEnoughArgs hd fn as nargs (length here)

      tdelta2 <- piApplyM (defType withdef) (mustAllApplyElims d1args)
      reportSDoc "tc.term.with" 30 $ vcat
        [ "preparing to type-check user arguments of with-application"
        , nest 2 $ "tΔ₂    =" <+> prettyTCM tdelta2
        , nest 2 $ "t      =" <+> prettyTCM t
        , nest 2 $ "here   =" <+> prettyA here
        , nest 2 $ "there  =" <+> prettyA there
        , nest 2 $ "d2args =" <+> pretty d2args
        ]

      -- checkArguments thinks that it is checking the overall
      -- expression, so it may try to check that the target type it is
      -- given matches the type of the function applied to its
      -- arguments; this may fail if the function hasn't been supplied
      -- all its arguments. we therefore give it a fresh meta to check
      -- against to placate the target-type check.
      --
      -- in this case, we will try to elaborate undersaturated
      -- applications whenever the @with@-expression was actually
      -- abstracted out of parts of the parent function's context.
      newt <- newTypeMeta_
      checkArguments CmpEq ReallyDontExpandLast (wahExpr hd) (map defaultNamedArg here) tdelta2 newt \(ACState [CheckedArg]
args Expr
_ Type
t1 CheckedTarget
chk) -> do
        -- however, the meta can go unsolved if the target-type check
        -- didn't run.
        case CheckedTarget
chk of
          NotCheckedTarget{} -> Type -> Type -> TCMT IO ()
equalType Type
newt Type
t1
          CheckedTarget{}    -> () -> TCMT IO ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

        let
          !as :: Elims
as = Elims
d1args Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! (CheckedArg -> Elim' Term) -> [CheckedArg] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' CheckedArg -> Elim' Term
caElim [CheckedArg]
args Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++! Elims
d2args

          -- we have to recheck that any terms that got moved after the
          -- scrutinee remain type correct when it is replaced with the
          -- user's given expression.
          -- this computes the type of the with-function applied to all
          -- its arguments.
          recheck :: Elims -> Type -> TCMT IO Type
recheck [] Type
ty = Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
ty
          recheck (Apply (Arg ArgInfo
_ Term
a):Elims
as) Type
ty = do
            (dom, abs, _) <- Type -> TCMT IO (Dom Type, Abs Type, Boundary)
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadTCError m) =>
Type -> m (Dom Type, Abs Type, Boundary)
shouldBePiOrPath Type
ty
            a <- checkInternal' defaultAction a CmpLeq (unDom dom)
            recheck as (abs `lazyAbsApp` a)
          recheck (Elim' Term
_:Elims
_) Type
_ = TCMT IO Type
forall a. HasCallStack => a
__IMPOSSIBLE__

        VerboseKey -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.term.with" Int
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
"checked arguments of with-application"
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"t1     =" 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
t1
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"newt   =" 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
newt
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
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
t
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"d2args =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elims -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elims -> m Doc
prettyTCM Elims
d2args
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"as     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elims -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elims -> m Doc
prettyTCM Elims
as
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"f as   =" 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 (QName -> Elims -> Term
Def QName
withfun Elims
as)
          ]

        t1d2 <- Elims -> Type -> TCMT IO Type
recheck Elims
d2args Type
t1
        reportSDoc "tc.term.with" 30 $ vcat
          [ "re-checked Δ₂ arguments of with-application"
          , nest 2 $ "t1d2 =" <+> prettyTCM t1d2
          ]

        case there of
          -- done, now need to coerce from the type we inferred to the
          -- type we expected.
          [] -> (MetaId, Term) -> Term
forall a b. (a, b) -> b
snd ((MetaId, Term) -> Term) -> TCMT IO (MetaId, Term) -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Comparison -> Term -> Type -> Type -> TCMT IO (MetaId, Term)
coerceMeta Comparison
cmp (QName -> Elims -> Term
Def QName
withfun Elims
as) Type
t1d2 Type
t

          -- still have pipes to go, continue checking but now
          -- pretending that we are checking an application of the
          -- auxiliary function.
          -- appWithAppHead handles remembering the name of the original
          -- head for error reporting.
          (Expr
e : [Expr]
es) -> Comparison
-> Type -> WithAppHead -> QName -> Elims -> List1 Expr -> TCM Term
checkWithApplication Comparison
cmp Type
t (WithAppHead -> [Expr] -> WithAppHead
appWithAppHead WithAppHead
hd [Expr]
here) QName
withfun Elims
as (Expr
e Expr -> [Expr] -> List1 Expr
forall a. a -> [a] -> NonEmpty a
:| [Expr]
es)

    YesReduction Simplification
_ Term
tm -> WithAppError -> TCM Term
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (WithAppError -> TCM Term) -> WithAppError -> TCM Term
forall a b. (a -> b) -> a -> b
$ WithAppHead -> QName -> Elims -> ReductNotWithFun -> WithAppError
WithAppReductNotDef WithAppHead
hd QName
fn Elims
as (Term -> ReductNotWithFun
NotDef Term
tm)

data ReductNotWithFun
  = NotDef        Term
  | NotWithFun    QName Defn
  | OtherWithFun  QName Term
  deriving (Int -> ReductNotWithFun -> ShowS
[ReductNotWithFun] -> ShowS
ReductNotWithFun -> VerboseKey
(Int -> ReductNotWithFun -> ShowS)
-> (ReductNotWithFun -> VerboseKey)
-> ([ReductNotWithFun] -> ShowS)
-> Show ReductNotWithFun
forall a.
(Int -> a -> ShowS)
-> (a -> VerboseKey) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ReductNotWithFun -> ShowS
showsPrec :: Int -> ReductNotWithFun -> ShowS
$cshow :: ReductNotWithFun -> VerboseKey
show :: ReductNotWithFun -> VerboseKey
$cshowList :: [ReductNotWithFun] -> ShowS
showList :: [ReductNotWithFun] -> ShowS
Show, (forall x. ReductNotWithFun -> Rep ReductNotWithFun x)
-> (forall x. Rep ReductNotWithFun x -> ReductNotWithFun)
-> Generic ReductNotWithFun
forall x. Rep ReductNotWithFun x -> ReductNotWithFun
forall x. ReductNotWithFun -> Rep ReductNotWithFun x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ReductNotWithFun -> Rep ReductNotWithFun x
from :: forall x. ReductNotWithFun -> Rep ReductNotWithFun x
$cto :: forall x. Rep ReductNotWithFun x -> ReductNotWithFun
to :: forall x. Rep ReductNotWithFun x -> ReductNotWithFun
Generic)

data WithAppError
  = WithAppNonFun  QName Defn
  | NotWithAppHead Term
  | WithAppUndersat WithAppHead QName Elims
  | WithAppNeutral WithAppHead QName Elims Elim
  | WithAppAbsurd WithAppHead QName Elims
  | WithAppNotEnoughArgs WithAppHead QName Elims Nat1 Nat
  | WithAppReductNotDef WithAppHead QName Elims ReductNotWithFun
  deriving (Int -> WithAppError -> ShowS
[WithAppError] -> ShowS
WithAppError -> VerboseKey
(Int -> WithAppError -> ShowS)
-> (WithAppError -> VerboseKey)
-> ([WithAppError] -> ShowS)
-> Show WithAppError
forall a.
(Int -> a -> ShowS)
-> (a -> VerboseKey) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> WithAppError -> ShowS
showsPrec :: Int -> WithAppError -> ShowS
$cshow :: WithAppError -> VerboseKey
show :: WithAppError -> VerboseKey
$cshowList :: [WithAppError] -> ShowS
showList :: [WithAppError] -> ShowS
Show, (forall x. WithAppError -> Rep WithAppError x)
-> (forall x. Rep WithAppError x -> WithAppError)
-> Generic WithAppError
forall x. Rep WithAppError x -> WithAppError
forall x. WithAppError -> Rep WithAppError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. WithAppError -> Rep WithAppError x
from :: forall x. WithAppError -> Rep WithAppError x
$cto :: forall x. Rep WithAppError x -> WithAppError
to :: forall x. Rep WithAppError x -> WithAppError
Generic)

instance NFData ReductNotWithFun
instance NFData WithAppError

verbaliseDef :: Defn -> String
verbaliseDef :: Defn -> VerboseKey
verbaliseDef = \case
  Axiom{}            -> VerboseKey
"a postulate"
  DataOrRecSig{}     -> VerboseKey
"a yet-undefined data or record type"
  GeneralizableVar{} -> VerboseKey
"a generalizable variable"
  AbstractDefn{}     -> VerboseKey
"abstract"
  Function{}         -> VerboseKey
"a function"
  Datatype{}         -> VerboseKey
"a data type"
  Record{}           -> VerboseKey
"a record type"
  Constructor{}      -> VerboseKey
"a constructor"
  Primitive{}        -> VerboseKey
"a primitive function"
  PrimitiveSort{}    -> VerboseKey
"a primitive sort"

verbaliseTerm :: Term -> String
verbaliseTerm :: Term -> VerboseKey
verbaliseTerm = \case
  Def{}      -> VerboseKey
forall a. HasCallStack => a
__IMPOSSIBLE__
  DontCare{} -> VerboseKey
forall a. HasCallStack => a
__IMPOSSIBLE__
  Dummy{}    -> VerboseKey
forall a. HasCallStack => a
__IMPOSSIBLE__
  MetaV{}    -> VerboseKey
"a metavariable"
  Var{}      -> VerboseKey
"a local variable"
  Con{}      -> VerboseKey
"a constructor"
  Pi{}       -> VerboseKey
"a function type"
  Sort{}     -> VerboseKey
"a sort"
  Lit{}      -> VerboseKey
"a literal"
  Lam{}      -> VerboseKey
"a lambda expression"
  Level{}    -> VerboseKey
"a universe level"

instance PrettyTCM WithAppError where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => WithAppError -> m Doc
prettyTCM = \case
    WithAppNonFun QName
nm Defn
def -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
       ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"Head of" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
hlKeyword m Doc
"with" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"-application"]
      [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"should be a reducible defined function, but"
      [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
nm] [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"is" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords (Defn -> VerboseKey
verbaliseDef Defn
def VerboseKey -> ShowS
forall a. Semigroup a => a -> a -> a
<> VerboseKey
".")

    NotWithAppHead Term
tm -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
       ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"Head of" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
hlKeyword m Doc
"with" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"-application"]
      [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"should be a reducible defined function, not"
      [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords (Term -> VerboseKey
verbaliseTerm Term
tm VerboseKey -> ShowS
forall a. Semigroup a => a -> a -> a
<> VerboseKey
".")

    WithAppUndersat (WithAppHead QName
orig Expr
_) QName
fn Elims
as -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"The application of function" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
orig]
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (QName -> Elims -> Term
Def QName
fn Elims
as)
      , [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"does not have enough arguments to identify one of its" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
hlKeyword m Doc
"with" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"-clauses."]
      ]

    WithAppAbsurd (WithAppHead QName
orig Expr
_) QName
fn Elims
as -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"The application of function" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
orig]
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (QName -> Elims -> Term
Def QName
fn Elims
as)
      , [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"matches an absurd clause, which can not have" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
hlKeyword m Doc
"with" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"-abstractions."]
      ]

    WithAppNeutral (WithAppHead QName
orig Expr
_) QName
fn Elims
as Elim' Term
blk -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"The application of function" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
orig]
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (QName -> Elims -> Term
Def QName
fn Elims
as)
      , [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"does not identify one of its" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
hlKeyword m Doc
"with" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"-clauses,"]
            [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"because its reduction is blocked on"
            [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords case Elim' Term
blk of
              IApply{} -> VerboseKey
"the argument"
              Apply{}  -> VerboseKey
"the argument"
              Proj{}   -> VerboseKey
"the projection"
      , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 case Elim' Term
blk of
          IApply Term
_ Term
_ Term
blk -> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
blk
          Apply      Arg Term
blk -> Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM Arg Term
blk
          Proj ProjOrigin
_     QName
blk -> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
blk
      ]

    WithAppNotEnoughArgs (WithAppHead QName
orig Expr
_) QName
fn Elims
as Int
want Int
have ->
      let
        but :: [m Doc]
but
          | Int
have Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
want = [m Doc
"but", Int -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
have, m Doc
"were", m Doc
"given."]
          | Int
have Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1   = VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"but only one was given."
          | Bool
otherwise   = [m Doc
"but", m Doc
"only", Int -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
have, m Doc
"were", m Doc
"given."]
      in [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
        [ m Doc
"The", m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
hlKeyword m Doc
"with" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"-application", m Doc
"of", m Doc
"function"
        , QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
orig, m Doc
"should", m Doc
"have", Int -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
want
        , if Int
want Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then m Doc
"argument," else m Doc
"arguments,"
        ]
       [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [m Doc]
but

    WithAppReductNotDef (WithAppHead QName
orig Expr
_) QName
fn Elims
as ReductNotWithFun
tm ->
      let
        expl :: m Doc
expl = case ReductNotWithFun
tm of
          NotDef Lam{} -> VerboseKey -> m Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
fwords VerboseKey
"It reduces to a lambda-abstraction. Did you apply enough arguments?"
          NotDef Term
tm    -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"It instead reduces to" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords (Term -> VerboseKey
verbaliseTerm Term
tm VerboseKey -> ShowS
forall a. Semigroup a => a -> a -> a
<> VerboseKey
".")

          NotWithFun QName
qn Function{} -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"It reduces to an application of the unrelated function" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
qn m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
          NotWithFun QName
qn Defn
what
            -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"It reduces to an application of"
            [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
qn] [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"which is not a with-function, but" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords (Defn -> VerboseKey
verbaliseDef Defn
what VerboseKey -> ShowS
forall a. Semigroup a => a -> a -> a
<> VerboseKey
".")

          OtherWithFun QName
qn' Term
tm -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"It instead reduces to a" [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
hlKeyword m Doc
"with" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"-function", m Doc
"of", QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
qn' m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
":"]
            , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
tm
            ]

      in [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ m Doc
"The application"
        , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (QName -> Elims -> Term
Def QName
fn Elims
as)
        , [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"does not reduce to a clause of"
              [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
orig]
              [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> VerboseKey -> [m Doc]
forall (m :: * -> *). Applicative m => VerboseKey -> [m Doc]
pwords VerboseKey
"defined by"
              [m Doc] -> [m Doc] -> [m Doc]
forall a. Semigroup a => a -> a -> a
<> [m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
hlKeyword m Doc
"with" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"-abstraction."]
        , m Doc
expl
        ]

instance Diagnostic WithAppError where
  diagnosticReason :: WithAppError -> DiagnosticReason
diagnosticReason WithAppError
_ = DiagnosticReason
DiagError
  diagnosticString :: WithAppError -> VerboseKey
diagnosticString = \case
    WithAppNonFun{}        -> VerboseKey
"WithApp.WrongHead"
    NotWithAppHead{}       -> VerboseKey
"WithApp.WrongHead"
    WithAppNotEnoughArgs{} -> VerboseKey
"WithApp.NotEnoughArgs"
    WithAppUndersat{}      -> VerboseKey
"WithApp.Undersat"
    WithAppNeutral{}       -> VerboseKey
"WithApp.Blocked"
    WithAppAbsurd{}        -> VerboseKey
"WithApp.Absurd"
    WithAppReductNotDef WithAppHead
_ QName
_ Elims
_ ReductNotWithFun
r -> case ReductNotWithFun
r of
      OtherWithFun{} -> VerboseKey
"WithApp.WrongWithFun"
      ReductNotWithFun
_              -> VerboseKey
"WithApp.NotWithRHS"