    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.TypeChecking.Rules.Display (checkDisplayPragma) where

    import Control.Monad.Except
    import Control.Monad.State
    import Data.Maybe

    import qualified Agda.Syntax.Abstract as A
    import Agda.Syntax.Abstract.Views
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Common

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Warnings (warning)

    import Agda.Syntax.Common.Pretty (prettyShow, render)

    import Agda.Utils.Impossible

    -- | Add display pragma if well-formed.
    --   Otherwise, throw 'InvalidDisplayForm' warning and ignore it.
    --
    checkDisplayPragma :: QName -> [NamedArg A.Pattern] -> A.Expr -> TCM ()
    checkDisplayPragma :: QName -> [NamedArg Pattern] -> Expr -> TCM ()
    checkDisplayPragma QName
    f [NamedArg Pattern]
    ps Expr
    e = do
      res <- TCMT IO (Either String DisplayForm)
    -> TCMT IO (Either String DisplayForm)
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO (Either String DisplayForm)
     -> TCMT IO (Either String DisplayForm))
    -> TCMT IO (Either String DisplayForm)
    -> TCMT IO (Either String DisplayForm)
    forall a b. (a -> b) -> a -> b
    $ ExceptT String TCM DisplayForm
    -> TCMT IO (Either String DisplayForm)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT do
        QName
    -> (Elims -> Elims)
    -> [NamedArg Pattern]
    -> (Nat -> Elims -> ExceptT String TCM DisplayForm)
    -> ExceptT String TCM DisplayForm
    forall b a.
    QName
    -> (Elims -> b) -> [NamedArg Pattern] -> (Nat -> b -> M a) -> M a
    pappToTerm QName
    f Elims -> Elims
    forall a. a -> a
    id [NamedArg Pattern]
    ps \Nat
    n Elims
    args -> do
          -- pappToTerm puts Var 0 for every variable. We get to know how many there were (n) so
          -- now we can renumber them with decreasing deBruijn indices.
          let lhs :: Elims
    lhs = Nat -> Elims -> Elims
    renumberElims (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) Elims
    args
          Nat -> Elims -> DisplayTerm -> DisplayForm
    Display Nat
    n Elims
    lhs (DisplayTerm -> DisplayForm)
    -> (Term -> DisplayTerm) -> Term -> DisplayForm
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> DisplayTerm
    DTerm (Term -> DisplayForm)
    -> ExceptT String TCM Term -> ExceptT String TCM DisplayForm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> ExceptT String TCM Term
    exprToTerm Expr
    e
      case res of
        Left String
    reason -> Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> String -> Warning
    InvalidDisplayForm QName
    f String
    reason
        Right DisplayForm
    df -> do
          String -> Nat -> String -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> String -> m ()
    reportSLn String
    "tc.display.pragma" Nat
    20 (String -> TCM ()) -> String -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Adding display form for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    f
          String -> Nat -> String -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Nat -> String -> m ()
    reportSLn String
    "tc.display.pragma" Nat
    90 (String -> TCM ()) -> String -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ String
    ": \n  " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ DisplayForm -> String
    forall a. Show a => a -> String
    show DisplayForm
    df
          QName -> DisplayForm -> TCM ()
    addDisplayForm QName
    f DisplayForm
    df

    -- | The monad to check display forms.
    --   The 'String' contains the reason to reject the display form.
    --
    type M = ExceptT String TCM

    -- | Helper data type to record whether a pattern on the LHS contributed
    -- a 'Proj' elimination or an 'Apply' elimination.
    data ProjOrApp = IsProj QName | IsApp Term

    var0 :: ProjOrApp
    var0 :: ProjOrApp
    var0 = Term -> ProjOrApp
    IsApp (Nat -> Term
    var Nat
    0)

    patternsToTerms0 :: [NamedArg A.Pattern] -> (Int -> Elims -> M a) -> M a
    patternsToTerms0 :: forall a. [NamedArg Pattern] -> (Nat -> Elims -> M a) -> M a
    patternsToTerms0 []       Nat -> Elims -> M a
    ret = Nat -> Elims -> M a
    ret Nat
    0 []
    patternsToTerms0 (NamedArg Pattern
    p : [NamedArg Pattern]
    ps) Nat -> Elims -> M a
    ret =
      Pattern -> (Nat -> ProjOrApp -> M a) -> M a
    forall a. Pattern -> (Nat -> ProjOrApp -> M a) -> M a
    patternToTerm (NamedArg Pattern -> Pattern
    forall a. NamedArg a -> a
    namedArg NamedArg Pattern
    p) \ Nat
    n ProjOrApp
    v ->
      [NamedArg Pattern] -> (Nat -> Elims -> M a) -> M a
    forall a. [NamedArg Pattern] -> (Nat -> Elims -> M a) -> M a
    patternsToTerms0 [NamedArg Pattern]
    ps \ Nat
    m Elims
    vs ->
      Nat -> Elims -> M a
    ret (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    m) (NamedArg Pattern -> ProjOrApp -> Elim
    forall a. LensHiding a => a -> ProjOrApp -> Elim
    inheritHiding NamedArg Pattern
    p ProjOrApp
    v Elim -> Elims -> Elims
    forall a. a -> [a] -> [a]
    : Elims
    vs)

    {-# SPECIALIZE patternsToTerms :: ListTel -> [NamedArg A.Pattern] -> (Int -> Elims -> M a) -> M a #-}
    patternsToTerms :: (LensNamed dom, NameOf dom ~ NamedName, LensHiding dom)
      => [dom] -> [NamedArg A.Pattern] -> (Int -> Elims -> M a) -> M a
    patternsToTerms :: forall dom a.
    (LensNamed dom, NameOf dom ~ NamedName, LensHiding dom) =>
    [dom] -> [NamedArg Pattern] -> (Nat -> Elims -> M a) -> M a
    patternsToTerms []        [NamedArg Pattern]
    ps Nat -> Elims -> M a
    ret = [NamedArg Pattern] -> (Nat -> Elims -> M a) -> M a
    forall a. [NamedArg Pattern] -> (Nat -> Elims -> M a) -> M a
    patternsToTerms0 [NamedArg Pattern]
    ps Nat -> Elims -> M a
    ret
    patternsToTerms (dom
    a : [dom]
    tel) [NamedArg Pattern]
    ps Nat -> Elims -> M a
    ret
      | Bool
    shouldInsertArg =
          M a -> M a
    forall a. M a -> M a
    bindWild (M a -> M a) -> M a -> M a
    forall a b. (a -> b) -> a -> b
    $ [dom] -> [NamedArg Pattern] -> (Nat -> Elims -> M a) -> M a
    forall dom a.
    (LensNamed dom, NameOf dom ~ NamedName, LensHiding dom) =>
    [dom] -> [NamedArg Pattern] -> (Nat -> Elims -> M a) -> M a
    patternsToTerms [dom]
    tel [NamedArg Pattern]
    ps \ Nat
    n Elims
    vs ->
          Nat -> Elims -> M a
    ret (Nat
    1 Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    n) (dom -> ProjOrApp -> Elim
    forall a. LensHiding a => a -> ProjOrApp -> Elim
    inheritHiding dom
    a ProjOrApp
    var0 Elim -> Elims -> Elims
    forall a. a -> [a] -> [a]
    : Elims
    vs)
      where
        shouldInsertArg :: Bool
    shouldInsertArg = case [NamedArg Pattern]
    ps of
          [] -> dom -> Bool
    forall a. LensHiding a => a -> Bool
    notVisible dom
    a
          NamedArg Pattern
    p : [NamedArg Pattern]
    ps -> Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> Maybe Bool -> Bool
    forall a. a -> Maybe a -> a
    fromMaybe Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Bool -> Bool) -> Maybe Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ NamedArg Pattern -> dom -> Maybe Bool
    forall arg dom.
    (LensNamed arg, NameOf arg ~ NamedName, LensHiding arg,
     LensNamed dom, NameOf dom ~ NamedName, LensHiding dom) =>
    arg -> dom -> Maybe Bool
    fittingNamedArg NamedArg Pattern
    p dom
    a
    patternsToTerms (dom
    a : [dom]
    tel) [] Nat -> Elims -> M a
    ret = Nat -> Elims -> M a
    ret Nat
    0 []
    patternsToTerms (dom
    a : [dom]
    tel) (NamedArg Pattern
    p : [NamedArg Pattern]
    ps) Nat -> Elims -> M a
    ret =
        Pattern -> (Nat -> ProjOrApp -> M a) -> M a
    forall a. Pattern -> (Nat -> ProjOrApp -> M a) -> M a
    patternToTerm (NamedArg Pattern -> Pattern
    forall a. NamedArg a -> a
    namedArg NamedArg Pattern
    p) \ Nat
    n ProjOrApp
    v ->
        [dom] -> [NamedArg Pattern] -> (Nat -> Elims -> M a) -> M a
    forall dom a.
    (LensNamed dom, NameOf dom ~ NamedName, LensHiding dom) =>
    [dom] -> [NamedArg Pattern] -> (Nat -> Elims -> M a) -> M a
    patternsToTerms [dom]
    tel [NamedArg Pattern]
    ps \ Nat
    m Elims
    vs ->
        Nat -> Elims -> M a
    ret (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    m) (NamedArg Pattern -> ProjOrApp -> Elim
    forall a. LensHiding a => a -> ProjOrApp -> Elim
    inheritHiding NamedArg Pattern
    p ProjOrApp
    v Elim -> Elims -> Elims
    forall a. a -> [a] -> [a]
    : Elims
    vs)

    inheritHiding :: LensHiding a => a -> ProjOrApp -> Elim
    inheritHiding :: forall a. LensHiding a => a -> ProjOrApp -> Elim
    inheritHiding a
    a (IsProj QName
    q) = ProjOrigin -> QName -> Elim
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    q
    inheritHiding a
    a (IsApp Term
    t) = Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply (Hiding -> Arg Term -> Arg Term
    forall a. LensHiding a => Hiding -> a -> a
    setHiding (a -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding a
    a) (Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    t))

    pappToTerm :: QName -> (Elims -> b) -> [NamedArg A.Pattern] -> (Int -> b -> M a) -> M a
    pappToTerm :: forall b a.
    QName
    -> (Elims -> b) -> [NamedArg Pattern] -> (Nat -> b -> M a) -> M a
    pappToTerm QName
    x Elims -> b
    f [NamedArg Pattern]
    ps Nat -> b -> M a
    ret = do
      def <- QName -> ExceptT String TCM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
      TelV tel _ <- telView $ defType def
      let pars = Definition -> Nat
    droppedPars Definition
    def
      patternsToTerms (drop pars $ telToList tel) ps \ Nat
    n Elims
    vs -> Nat -> b -> M a
    ret Nat
    n (Elims -> b
    f Elims
    vs)

    patternToTerm :: A.Pattern -> (Nat -> ProjOrApp -> M a) -> M a
    patternToTerm :: forall a. Pattern -> (Nat -> ProjOrApp -> M a) -> M a
    patternToTerm Pattern
    p Nat -> ProjOrApp -> M a
    ret =
      case Pattern
    p of
        A.VarP A.BindName{unBind :: BindName -> Name
    unBind = Name
    x}   -> Name -> M a -> M a
    forall a. Name -> M a -> M a
    bindVar Name
    x (M a -> M a) -> M a -> M a
    forall a b. (a -> b) -> a -> b
    $ Nat -> ProjOrApp -> M a
    ret Nat
    1 ProjOrApp
    var0
        A.ConP ConPatInfo
    _ AmbiguousQName
    cs [NamedArg Pattern]
    ps
          | Just QName
    c <- AmbiguousQName -> Maybe QName
    getUnambiguous AmbiguousQName
    cs -> QName
    -> (Elims -> Term)
    -> [NamedArg Pattern]
    -> (Nat -> Term -> M a)
    -> M a
    forall b a.
    QName
    -> (Elims -> b) -> [NamedArg Pattern] -> (Nat -> b -> M a) -> M a
    pappToTerm QName
    c (ConHead -> ConInfo -> Elims -> Term
    Con (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
    ConHead QName
    c DataOrRecord
    forall p. DataOrRecord' p
    IsData Induction
    Inductive []) ConInfo
    ConOCon) [NamedArg Pattern]
    ps \ Nat
    n Term
    t -> Nat -> ProjOrApp -> M a
    ret Nat
    n (Term -> ProjOrApp
    IsApp Term
    t)
          | Bool
    otherwise                   -> String -> AmbiguousQName -> M a
    ambigErr String
    "constructor" AmbiguousQName
    cs
        A.ProjP PatInfo
    _ ProjOrigin
    _ AmbiguousQName
    ds
          | Just QName
    d <- AmbiguousQName -> Maybe QName
    getUnambiguous AmbiguousQName
    ds -> Nat -> ProjOrApp -> M a
    ret Nat
    0 (ProjOrApp -> M a) -> ProjOrApp -> M a
    forall a b. (a -> b) -> a -> b
    $ QName -> ProjOrApp
    IsProj QName
    d
          | Bool
    otherwise                   -> String -> AmbiguousQName -> M a
    ambigErr String
    "projection" AmbiguousQName
    ds
        A.DefP PatInfo
    _ AmbiguousQName
    fs [NamedArg Pattern]
    ps
          | Just QName
    f <- AmbiguousQName -> Maybe QName
    getUnambiguous AmbiguousQName
    fs -> QName
    -> (Elims -> Term)
    -> [NamedArg Pattern]
    -> (Nat -> Term -> M a)
    -> M a
    forall b a.
    QName
    -> (Elims -> b) -> [NamedArg Pattern] -> (Nat -> b -> M a) -> M a
    pappToTerm QName
    f (QName -> Elims -> Term
    Def QName
    f) [NamedArg Pattern]
    ps \ Nat
    n Term
    t -> Nat -> ProjOrApp -> M a
    ret Nat
    n (Term -> ProjOrApp
    IsApp Term
    t)
          | Bool
    otherwise                   -> String -> AmbiguousQName -> M a
    ambigErr String
    "DefP" AmbiguousQName
    fs
        A.LitP PatInfo
    _ Literal
    l                      -> Nat -> ProjOrApp -> M a
    ret Nat
    0 (ProjOrApp -> M a) -> ProjOrApp -> M a
    forall a b. (a -> b) -> a -> b
    $ Term -> ProjOrApp
    IsApp (Term -> ProjOrApp) -> Term -> ProjOrApp
    forall a b. (a -> b) -> a -> b
    $ Literal -> Term
    Lit Literal
    l
        A.WildP PatInfo
    _                       -> M a -> M a
    forall a. M a -> M a
    bindWild (M a -> M a) -> M a -> M a
    forall a b. (a -> b) -> a -> b
    $ Nat -> ProjOrApp -> M a
    ret Nat
    1 ProjOrApp
    var0
        A.AsP{}                         -> String -> M a
    failP String
    "an @-pattern"
        A.DotP{}                        -> String -> M a
    failP String
    "a dot pattern"
        A.AbsurdP{}                     -> String -> M a
    failP String
    "an absurd pattern"
        A.PatternSynP{}                 -> M a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        A.RecP{}                        -> String -> M a
    failP String
    "a record pattern"
        A.EqualP{}                      -> String -> M a
    failP String
    "a system pattern"
        A.WithP{}                       -> M a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      where
        fail :: String -> ExceptT String TCM a
    fail = String -> ExceptT String TCM a
    forall a. String -> ExceptT String TCM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> ExceptT String TCM a)
    -> (String -> String) -> String -> ExceptT String TCM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String
    "its left-hand side contains " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++)
        failP :: String -> M a
    failP String
    s = String -> M a
    forall a. String -> ExceptT String TCM a
    fail (String -> M a) -> (Doc -> String) -> Doc -> M a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++) (String -> String) -> (Doc -> String) -> Doc -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String
    ": " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++) (String -> String) -> (Doc -> String) -> Doc -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> String
    forall a. Doc a -> String
    render (Doc -> M a) -> ExceptT String TCM Doc -> M a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Pattern -> ExceptT String TCM Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Pattern
    p
        ambigErr :: String -> AmbiguousQName -> M a
    ambigErr String
    thing (AmbQ List1 QName
    xs) =
          String -> M a
    forall a. String -> ExceptT String TCM a
    fail (String -> M a) -> (Doc -> String) -> Doc -> M a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> String
    forall a. Doc a -> String
    render (Doc -> M a) -> ExceptT String TCM Doc -> M a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
            String -> ExceptT String TCM Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String
    "an ambiguous " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    thing String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ":") ExceptT String TCM Doc
    -> ExceptT String TCM Doc -> ExceptT String TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <?>
              [ExceptT String TCM Doc] -> ExceptT String TCM Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep (ExceptT String TCM Doc
    -> NonEmpty (ExceptT String TCM Doc) -> [ExceptT String TCM Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate ExceptT String TCM Doc
    forall (m :: * -> *). Applicative m => m Doc
    comma ((QName -> ExceptT String TCM Doc)
    -> List1 QName -> NonEmpty (ExceptT String TCM Doc)
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap QName -> ExceptT String TCM Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty List1 QName
    xs))

    bindWild :: M a -> M a
    bindWild :: forall a. M a -> M a
    bindWild M a
    ret = do
      x <- ExceptT String TCM Name
    forall (m :: * -> *). MonadFresh NameId m => m Name
    freshNoName_
      bindVar x ret

    bindVar :: Name -> M a -> M a
    bindVar :: forall a. Name -> M a -> M a
    bindVar Name
    x M a
    ret = Name -> M a -> M a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Name -> m a -> m a
    addContext Name
    x M a
    ret

    exprToTerm :: A.Expr -> M Term
    exprToTerm :: Expr -> ExceptT String TCM Term
    exprToTerm Expr
    e =
      case Expr -> Expr
    unScope Expr
    e of
        A.Var Name
    x          -> (Term, Dom Type) -> Term
    forall a b. (a, b) -> a
    fst ((Term, Dom Type) -> Term)
    -> ExceptT String TCM (Term, Dom Type) -> ExceptT String TCM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Name -> ExceptT String TCM (Term, Dom Type)
    forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m) =>
    Name -> m (Term, Dom Type)
    getVarInfo Name
    x
        A.Def' QName
    f Suffix
    NoSuffix-> Term -> ExceptT String TCM Term
    forall a. a -> ExceptT String TCM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ExceptT String TCM Term)
    -> Term -> ExceptT String TCM Term
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    f []
        A.Def'{}         -> String -> ExceptT String TCM Term
    forall a. String -> ExceptT String TCM a
    fail String
    "suffix"
        A.Con AmbiguousQName
    c          -> Term -> ExceptT String TCM Term
    forall a. a -> ExceptT String TCM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ExceptT String TCM Term)
    -> Term -> ExceptT String TCM Term
    forall a b. (a -> b) -> a -> b
    $ ConHead -> ConInfo -> Elims -> Term
    Con (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
    ConHead (AmbiguousQName -> QName
    headAmbQ AmbiguousQName
    c) DataOrRecord
    forall p. DataOrRecord' p
    IsData Induction
    Inductive []) ConInfo
    ConOCon [] -- Don't care too much about ambiguity here
        A.Lit ExprInfo
    _ Literal
    l        -> Term -> ExceptT String TCM Term
    forall a. a -> ExceptT String TCM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ExceptT String TCM Term)
    -> Term -> ExceptT String TCM Term
    forall a b. (a -> b) -> a -> b
    $ Literal -> Term
    Lit Literal
    l
        A.App AppInfo
    _ Expr
    e NamedArg Expr
    arg    -> Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    applyE (Term -> Elims -> Term)
    -> ExceptT String TCM Term -> ExceptT String TCM (Elims -> Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> ExceptT String TCM Term
    exprToTerm Expr
    e ExceptT String TCM (Elims -> Term)
    -> ExceptT String TCM Elims -> ExceptT String TCM Term
    forall a b.
    ExceptT String TCM (a -> b)
    -> ExceptT String TCM a -> ExceptT String TCM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> ((Elim -> Elims -> Elims
    forall a. a -> [a] -> [a]
    :[]) (Elim -> Elims) -> (Term -> Elim) -> Term -> Elims
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg Expr -> ProjOrApp -> Elim
    forall a. LensHiding a => a -> ProjOrApp -> Elim
    inheritHiding NamedArg Expr
    arg (ProjOrApp -> Elim) -> (Term -> ProjOrApp) -> Term -> Elim
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> ProjOrApp
    IsApp (Term -> Elims)
    -> ExceptT String TCM Term -> ExceptT String TCM Elims
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Expr -> ExceptT String TCM Term
    exprToTerm (NamedArg Expr -> Expr
    forall a. NamedArg a -> a
    namedArg NamedArg Expr
    arg))

        A.Proj ProjOrigin
    _ AmbiguousQName
    f       -> Term -> ExceptT String TCM Term
    forall a. a -> ExceptT String TCM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ExceptT String TCM Term)
    -> Term -> ExceptT String TCM Term
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def (AmbiguousQName -> QName
    headAmbQ AmbiguousQName
    f) []   -- only for printing so we don't have to worry too much here
        A.PatternSyn AmbiguousQName
    f   -> Term -> ExceptT String TCM Term
    forall a. a -> ExceptT String TCM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ExceptT String TCM Term)
    -> Term -> ExceptT String TCM Term
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def (AmbiguousQName -> QName
    headAmbQ AmbiguousQName
    f) []
        A.Macro QName
    f        -> Term -> ExceptT String TCM Term
    forall a. a -> ExceptT String TCM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ExceptT String TCM Term)
    -> Term -> ExceptT String TCM Term
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    f []

        A.WithApp{}      -> String -> ExceptT String TCM Term
    forall a. String -> ExceptT String TCM a
    fail String
    "with application"
        A.QuestionMark{} -> String -> ExceptT String TCM Term
    forall a. String -> ExceptT String TCM a
    fail String
    "hole"
        A.Underscore{}   -> String -> ExceptT String TCM Term
    forall a. String -> ExceptT String TCM a
    fail String
    "metavariable"
        A.Dot{}          -> String -> ExceptT String TCM Term
    forall a. String -> ExceptT String TCM a
    fail String
    "dotted expression"
        A.Lam{}          -> String -> ExceptT String TCM Term
    forall a. String -> ExceptT String TCM a
    fail String
    "lambda"
        A.AbsurdLam{}    -> String -> ExceptT String TCM Term
    forall a. String -> ExceptT String TCM a
    fail String
    "lambda"
        A.ExtendedLam{}  -> String -> ExceptT String TCM Term
    forall a. String -> ExceptT String TCM a
    fail String
    "lambda"
        A.Fun{}          -> String -> ExceptT String TCM Term
    forall a. String -> ExceptT String TCM a
    fail String
    "function type"
        A.Pi{}           -> String -> ExceptT String TCM Term
    forall a. String -> ExceptT String TCM a
    fail String
    "function type"
        A.Generalized{}  -> ExceptT String TCM Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        A.Let{}          -> String -> ExceptT String TCM Term
    forall a. String -> ExceptT String TCM a
    fail String
    "let"
        A.Rec{}          -> String -> ExceptT String TCM Term
    forall a. String -> ExceptT String TCM a
    fail String
    "record"
        A.RecUpdate{}    -> String -> ExceptT String TCM Term
    forall a. String -> ExceptT String TCM a
    fail String
    "record update"
        A.ScopedExpr{}   -> ExceptT String TCM Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        A.Quote{}        -> String -> ExceptT String TCM Term
    forall a. String -> ExceptT String TCM a
    fail String
    "quotation"
        A.QuoteTerm{}    -> String -> ExceptT String TCM Term
    forall a. String -> ExceptT String TCM a
    fail String
    "quotation"
        A.Unquote{}      -> String -> ExceptT String TCM Term
    forall a. String -> ExceptT String TCM a
    fail String
    "unquote"
        A.DontCare{}     -> ExceptT String TCM Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      where
        fail :: String -> ExceptT String TCM a
    fail = String -> ExceptT String TCM a
    forall a. String -> ExceptT String TCM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> ExceptT String TCM a)
    -> (String -> String) -> String -> ExceptT String TCM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String
    "its right-hand side contains a " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++)

    renumberElims :: Nat -> Elims -> Elims
    renumberElims :: Nat -> Elims -> Elims
    renumberElims Nat
    n Elims
    es = State Nat Elims -> Nat -> Elims
    forall s a. State s a -> s -> a
    evalState (Elims -> State Nat Elims
    renumbers Elims
    es) Nat
    n
      where
        next :: State Nat Nat
        next :: State Nat Nat
    next = do i <- State Nat Nat
    forall s (m :: * -> *). MonadState s m => m s
    get; i <$ put (i - 1)

        renumbers :: Elims -> State Nat Elims
        renumbers :: Elims -> State Nat Elims
    renumbers = ((Elim -> StateT Nat Identity Elim) -> Elims -> State Nat Elims
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse ((Elim -> StateT Nat Identity Elim) -> Elims -> State Nat Elims)
    -> ((Term -> StateT Nat Identity Term)
        -> Elim -> StateT Nat Identity Elim)
    -> (Term -> StateT Nat Identity Term)
    -> Elims
    -> State Nat Elims
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> StateT Nat Identity Term)
    -> Elim -> StateT Nat Identity Elim
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Elim' a -> f (Elim' b)
    traverse) Term -> StateT Nat Identity Term
    renumber

        renumber :: Term -> State Nat Term
        renumber :: Term -> StateT Nat Identity Term
    renumber (Var Nat
    0 [])   = Nat -> Term
    var (Nat -> Term) -> State Nat Nat -> StateT Nat Identity Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> State Nat Nat
    next
        renumber (Def QName
    f Elims
    es)   = QName -> Elims -> Term
    Def QName
    f (Elims -> Term) -> State Nat Elims -> StateT Nat Identity Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> State Nat Elims
    renumbers Elims
    es
        renumber (Con ConHead
    c ConInfo
    h Elims
    es) = ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    h (Elims -> Term) -> State Nat Elims -> StateT Nat Identity Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> State Nat Elims
    renumbers Elims
    es
        renumber (Lit Literal
    l)      = Term -> StateT Nat Identity Term
    forall a. a -> StateT Nat Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> StateT Nat Identity Term)
    -> Term -> StateT Nat Identity Term
    forall a b. (a -> b) -> a -> b
    $ Literal -> Term
    Lit Literal
    l
        renumber Term
    _            = StateT Nat Identity Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- We need only handle the result of patternToTerm here