    {-# LANGUAGE UndecidableInstances #-}  -- for Arg a => Elim' a

    -- | Tools for 'DisplayTerm' and 'DisplayForm'.

    module Agda.TypeChecking.DisplayForm (displayForm) where

    import Control.Monad
    import Control.Monad.Trans (lift)
    import Control.Monad.Trans.Maybe

    import Data.Monoid (All(..))
    import Data.IntMap (IntMap)
    import qualified Data.IntMap as IntMap
    import Data.Map (Map)
    import qualified Data.Map as Map
    import qualified Data.Set as Set

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Names
    import Agda.Syntax.Scope.Base (inverseScopeLookupName)

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Level
    import Agda.TypeChecking.Reduce (instantiate)

    import Agda.Utils.Functor
    import Agda.Utils.List
    import Agda.Utils.List1 (List1)
    import Agda.Utils.Maybe
    import Agda.Syntax.Common.Pretty

    import Agda.Utils.Impossible

    -- | Get the arities of all display forms for a name.
    displayFormArities :: (HasConstInfo m, ReadTCState m) => QName -> m [Int]
    displayFormArities :: forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m [Nat]
    displayFormArities QName
    q = (Open DisplayForm -> Nat) -> [Open DisplayForm] -> [Nat]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Elim] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length ([Elim] -> Nat)
    -> (Open DisplayForm -> [Elim]) -> Open DisplayForm -> Nat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DisplayForm -> [Elim]
    dfPats (DisplayForm -> [Elim])
    -> (Open DisplayForm -> DisplayForm) -> Open DisplayForm -> [Elim]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Open DisplayForm -> DisplayForm
    forall (t :: * -> *) a. Decoration t => t a -> a
    dget) ([Open DisplayForm] -> [Nat]) -> m [Open DisplayForm] -> m [Nat]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m [Open DisplayForm]
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m [Open DisplayForm]
    getDisplayForms QName
    q

    -- | Lift a local display form to an outer context. The substitution goes from the parent context to
    --   the context of the local display form (see Issue 958). Current only handles pure extensions of
    --   the parent context.
    liftLocalDisplayForm :: Substitution -> DisplayForm -> Maybe DisplayForm
    liftLocalDisplayForm :: Substitution -> DisplayForm -> Maybe DisplayForm
    liftLocalDisplayForm Substitution
    IdS DisplayForm
    df = DisplayForm -> Maybe DisplayForm
    forall a. a -> Maybe a
    Just DisplayForm
    df
    liftLocalDisplayForm (Wk Nat
    n Substitution
    IdS) (Display Nat
    m [Elim]
    lhs DisplayTerm
    rhs) =
      -- We lift a display form by turning matches on free variables into pattern variables, which can
      -- be done by simply adding to the dfPatternVars field.
      DisplayForm -> Maybe DisplayForm
    forall a. a -> Maybe a
    Just (DisplayForm -> Maybe DisplayForm)
    -> DisplayForm -> Maybe DisplayForm
    forall a b. (a -> b) -> a -> b
    $ Nat -> [Elim] -> DisplayTerm -> DisplayForm
    Display (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    m) [Elim]
    lhs DisplayTerm
    rhs
    liftLocalDisplayForm Substitution
    _ DisplayForm
    _ = Maybe DisplayForm
    forall a. Maybe a
    Nothing

    type MonadDisplayForm m =
      ( MonadReduce m
      , ReadTCState m
      , HasConstInfo m
      , HasBuiltins m
      , MonadDebug m
      )

    -- | Find a matching display form for @q es@.
    --   In essence this tries to rewrite @q es@ with any
    --   display form @q ps --> dt@ and returns the instantiated
    --   @dt@ if successful.  First match wins.
    displayForm :: MonadDisplayForm m => QName -> Elims -> m (Maybe DisplayTerm)
    displayForm :: forall (m :: * -> *).
    MonadDisplayForm m =>
    QName -> [Elim] -> m (Maybe DisplayTerm)
    displayForm QName
    q [Elim]
    es = do
      -- Get display forms for name q.
      odfs  <- QName -> m [Open DisplayForm]
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m [Open DisplayForm]
    getDisplayForms QName
    q
      if (null odfs) then do
        reportSLn "tc.display.top" 101 $ "no displayForm for " ++ prettyShow q
        return Nothing
      else do
        -- Display debug info about the @Open@s.
        unlessDebugPrinting $ reportSDoc "tc.display.top" 100 $ do
          cps <- viewTC eCheckpoints
          cxt <- getContextTelescope
          return $ vcat
            [ "displayForm for" <+> pretty q
            , nest 2 $ "cxt =" <+> pretty cxt
            , nest 2 $ "cps =" <+> vcat (map pretty (Map.toList cps))
            , nest 2 $ "dfs =" <+> vcat (map pretty odfs) ]
        -- Use only the display forms that can be opened in the current context.
        dfs   <- catMaybes <$> mapM (tryGetOpen liftLocalDisplayForm) odfs
        scope <- getScope
        -- Keep the display forms that match the application @q es@.
        ms <- do
          ms <- mapM (runMaybeT . (`matchDisplayForm` es)) dfs
          return [ m | Just (d, m) <- ms, wellScoped scope d ]
        -- Not safe when printing non-terminating terms.
        -- (nfdfs, us) <- normalise (dfs, es)
        unlessDebugPrinting $ reportSDoc "tc.display.top" 100 $ return $ vcat
          [ "name        :" <+> pretty q
          , "displayForms:" <+> pretty dfs
          , "arguments   :" <+> pretty es
          , "matches     :" <+> pretty ms
          , "result      :" <+> pretty (listToMaybe ms)
          ]
        -- Return the first display form that matches.
        return $ listToMaybe ms
      where
        -- Look at the original display form, not the instantiated result when
        -- checking if it's well-scoped. Otherwise we might pick up out of scope
        -- identifiers coming from the source term.
        wellScoped :: ScopeInfo -> DisplayForm -> Bool
    wellScoped ScopeInfo
    scope (Display Nat
    _ [Elim]
    _ DisplayTerm
    d)
          | DisplayTerm -> Bool
    isWithDisplay DisplayTerm
    d = Bool
    True
          | Bool
    otherwise       = All -> Bool
    getAll (All -> Bool) -> All -> Bool
    forall a b. (a -> b) -> a -> b
    $ (QName -> All) -> DisplayTerm -> All
    forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
    namesIn' (Bool -> All
    All (Bool -> All) -> (QName -> Bool) -> QName -> All
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ScopeInfo -> QName -> Bool
    inScope ScopeInfo
    scope) DisplayTerm
    d  -- all names in d should be in scope

        inScope :: ScopeInfo -> QName -> Bool
    inScope ScopeInfo
    scope QName
    x = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [QName] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null ([QName] -> Bool) -> [QName] -> Bool
    forall a b. (a -> b) -> a -> b
    $ QName -> ScopeInfo -> [QName]
    inverseScopeLookupName QName
    x ScopeInfo
    scope

        isWithDisplay :: DisplayTerm -> Bool
    isWithDisplay DWithApp{} = Bool
    True
        isWithDisplay DisplayTerm
    _          = Bool
    False

    -- | Match a 'DisplayForm' @q ps = v@ against @q es@.
    --   Return the 'DisplayTerm' @v[us]@ if the match was successful,
    --   i.e., @es / ps = Just us@.
    matchDisplayForm :: MonadDisplayForm m
                     => DisplayForm -> Elims -> MaybeT m (DisplayForm, DisplayTerm)
    matchDisplayForm :: forall (m :: * -> *).
    MonadDisplayForm m =>
    DisplayForm -> [Elim] -> MaybeT m (DisplayForm, DisplayTerm)
    matchDisplayForm d :: DisplayForm
    d@(Display Nat
    n [Elim]
    ps DisplayTerm
    v) [Elim]
    es
      | [Elim] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Elim]
    ps Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > [Elim] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Elim]
    es = MaybeT m (DisplayForm, DisplayTerm)
    forall a. MaybeT m a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
      | Bool
    otherwise             = do
          let ([Elim]
    es0, [Elim]
    es1) = Nat -> [Elim] -> ([Elim], [Elim])
    forall a. Nat -> [a] -> ([a], [a])
    splitAt ([Elim] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Elim]
    ps) [Elim]
    es

          -- The 'Display' constructor acts as though it binds the pattern
          -- pattern variables up to 'n', so a match like
          --
          --   Display 1 [@1 @0] x =? [@0 _]
          --
          -- should work (it didn't; see LiftDisplayIntermediate). In
          -- effect, this is because the LHS patterns are in some context
          -- "Γ . @0", but the RHS term is only in context Γ.
          --
          -- Therefore, we should raise the RHS term by the number of
          -- pattern variables, to bring it into the context of the
          -- patterns.

          mm <- Window -> [Elim] -> [Elim] -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> [Elim] -> [Elim] -> MaybeT m MatchResult
    match (Nat -> Nat -> Window
    Window Nat
    0 Nat
    n) [Elim]
    ps (Nat -> [Elim] -> [Elim]
    forall a. Subst a => Nat -> a -> a
    raise Nat
    n [Elim]
    es0)
          us <- forM [0 .. n - 1] $ \ Nat
    i -> do
            -- #5294: Fail if we don't have bindings for all variables. This can
            --        happen outside parameterised modules when some of the parameters
            --        are not used in the lhs.
            Just u <- Maybe (WithOrigin Term) -> MaybeT m (Maybe (WithOrigin Term))
    forall a. a -> MaybeT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (WithOrigin Term) -> MaybeT m (Maybe (WithOrigin Term)))
    -> Maybe (WithOrigin Term) -> MaybeT m (Maybe (WithOrigin Term))
    forall a b. (a -> b) -> a -> b
    $ Nat -> MatchResult -> Maybe (WithOrigin Term)
    forall a. Nat -> IntMap a -> Maybe a
    IntMap.lookup Nat
    i MatchResult
    mm
            -- Note that the RHS terms are independent of the pattern variables.
            return (applySubst (strengthenS __IMPOSSIBLE__ n) <$> u)
          return (d, substWithOrigin (parallelS $ map woThing us) us v `applyE` es1)

    type MatchResult = IntMap (WithOrigin Term)

    unionMatch :: Monad m => MatchResult -> MatchResult -> MaybeT m MatchResult
    unionMatch :: forall (m :: * -> *).
    Monad m =>
    MatchResult -> MatchResult -> MaybeT m MatchResult
    unionMatch MatchResult
    m1 MatchResult
    m2
      | MatchResult -> Bool
    forall a. IntMap a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (MatchResult -> MatchResult -> MatchResult
    forall a b. IntMap a -> IntMap b -> IntMap a
    IntMap.intersection MatchResult
    m1 MatchResult
    m2) = MatchResult -> MaybeT m MatchResult
    forall a. a -> MaybeT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MatchResult -> MaybeT m MatchResult)
    -> MatchResult -> MaybeT m MatchResult
    forall a b. (a -> b) -> a -> b
    $ MatchResult -> MatchResult -> MatchResult
    forall a. IntMap a -> IntMap a -> IntMap a
    IntMap.union MatchResult
    m1 MatchResult
    m2
      | Bool
    otherwise = MaybeT m MatchResult
    forall a. MaybeT m a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero  -- Non-linear pattern, fail for now.

    unionsMatch :: Monad m => [MatchResult] -> MaybeT m MatchResult
    unionsMatch :: forall (m :: * -> *).
    Monad m =>
    [MatchResult] -> MaybeT m MatchResult
    unionsMatch = (MatchResult -> MatchResult -> MaybeT m MatchResult)
    -> MatchResult -> [MatchResult] -> MaybeT m MatchResult
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM MatchResult -> MatchResult -> MaybeT m MatchResult
    forall (m :: * -> *).
    Monad m =>
    MatchResult -> MatchResult -> MaybeT m MatchResult
    unionMatch MatchResult
    forall a. Monoid a => a
    mempty

    data Window = Window {Window -> Nat
    dbLo, Window -> Nat
    dbHi :: Nat}

    inWindow :: Window -> Nat -> Maybe Nat
    inWindow :: Window -> Nat -> Maybe Nat
    inWindow (Window Nat
    lo Nat
    hi) Nat
    n | Nat
    lo Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Nat
    n, Nat
    n Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    hi = Nat -> Maybe Nat
    forall a. a -> Maybe a
    Just (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    lo)
                              | Bool
    otherwise       = Maybe Nat
    forall a. Maybe a
    Nothing

    shiftWindow :: Window -> Window
    shiftWindow :: Window -> Window
    shiftWindow (Window Nat
    lo Nat
    hi) = Nat -> Nat -> Window
    Window (Nat
    lo Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) (Nat
    hi Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1)

    -- | Class @Match@ for matching a term @p@ in the role of a pattern
    --   against a term @v@.
    --
    --   Free variables inside the window in @p@ are pattern variables and
    --   the result of matching is a map from pattern variables (shifted down to start at 0) to subterms
    --   of @v@.
    class Match a where
      match :: MonadDisplayForm m => Window -> a -> a -> MaybeT m MatchResult

    instance Match a => Match [a] where
      match :: forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> [a] -> [a] -> MaybeT m MatchResult
    match Window
    n [a]
    xs [a]
    ys
        | [a] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [a]
    xs Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == [a] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [a]
    ys = [MatchResult] -> MaybeT m MatchResult
    forall (m :: * -> *).
    Monad m =>
    [MatchResult] -> MaybeT m MatchResult
    unionsMatch ([MatchResult] -> MaybeT m MatchResult)
    -> MaybeT m [MatchResult] -> MaybeT m MatchResult
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (a -> a -> MaybeT m MatchResult)
    -> [a] -> [a] -> MaybeT m [MatchResult]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM (Window -> a -> a -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> a -> a -> MaybeT m MatchResult
    match Window
    n) [a]
    xs [a]
    ys
        | Bool
    otherwise = MaybeT m MatchResult
    forall a. MaybeT m a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    instance Match a => Match (Arg a) where
      match :: forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> Arg a -> Arg a -> MaybeT m MatchResult
    match Window
    n Arg a
    p Arg a
    v = (WithOrigin Term -> WithOrigin Term) -> MatchResult -> MatchResult
    forall a b. (a -> b) -> IntMap a -> IntMap b
    IntMap.map (Origin -> WithOrigin Term -> WithOrigin Term
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin (Arg a -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin Arg a
    v)) (MatchResult -> MatchResult)
    -> MaybeT m MatchResult -> MaybeT m MatchResult
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Window -> a -> a -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> a -> a -> MaybeT m MatchResult
    match Window
    n (Arg a -> a
    forall e. Arg e -> e
    unArg Arg a
    p) (Arg a -> a
    forall e. Arg e -> e
    unArg Arg a
    v)

    instance Match a => Match (Elim' a) where
      match :: forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> Elim' a -> Elim' a -> MaybeT m MatchResult
    match Window
    n Elim' a
    p Elim' a
    v =
        case (Elim' a
    p, Elim' a
    v) of
          (Proj ProjOrigin
    _ QName
    f, Proj ProjOrigin
    _ QName
    f') | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f' -> MatchResult -> MaybeT m MatchResult
    forall a. a -> MaybeT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return MatchResult
    forall a. Monoid a => a
    mempty
          (Elim' a, Elim' a)
    _ | Just Arg a
    a  <- Elim' a -> Maybe (Arg a)
    forall a. Elim' a -> Maybe (Arg a)
    isApplyElim Elim' a
    p
            , Just Arg a
    a' <- Elim' a -> Maybe (Arg a)
    forall a. Elim' a -> Maybe (Arg a)
    isApplyElim Elim' a
    v    -> Window -> Arg a -> Arg a -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> Arg a -> Arg a -> MaybeT m MatchResult
    match Window
    n Arg a
    a Arg a
    a'
          -- we do not care to differentiate between Apply and IApply for
          -- printing.
          (Elim' a, Elim' a)
    _                               -> MaybeT m MatchResult
    forall a. MaybeT m a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    instance Match Term where
      match :: forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> Term -> Term -> MaybeT m MatchResult
    match Window
    w Term
    p Term
    v = m Term -> MaybeT m Term
    forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Term -> m Term
    forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
    instantiate Term
    v) MaybeT m Term
    -> (Term -> MaybeT m MatchResult) -> MaybeT m MatchResult
    forall a b. MaybeT m a -> (a -> MaybeT m b) -> MaybeT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ Term
    v -> case (Term -> Term
    unSpine Term
    p, Term -> Term
    unSpine Term
    v) of
        (Var Nat
    i [], Term
    v)    | Just Nat
    j <- Window -> Nat -> Maybe Nat
    inWindow Window
    w Nat
    i -> MatchResult -> MaybeT m MatchResult
    forall a. a -> MaybeT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MatchResult -> MaybeT m MatchResult)
    -> MatchResult -> MaybeT m MatchResult
    forall a b. (a -> b) -> a -> b
    $ Nat -> WithOrigin Term -> MatchResult
    forall a. Nat -> a -> IntMap a
    IntMap.singleton Nat
    j (Origin -> Term -> WithOrigin Term
    forall a. Origin -> a -> WithOrigin a
    WithOrigin Origin
    Inserted Term
    v)
        (Var Nat
    i (Elim
    _:[Elim]
    _), Term
    v) | Just{} <- Window -> Nat -> Maybe Nat
    inWindow Window
    w Nat
    i -> MaybeT m MatchResult
    forall a. MaybeT m a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero  -- Higher-order pattern, fail for now.
        (Var Nat
    i [Elim]
    ps, Var Nat
    j [Elim]
    vs) | Nat
    i Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    j  -> Window -> [Elim] -> [Elim] -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> [Elim] -> [Elim] -> MaybeT m MatchResult
    match Window
    w [Elim]
    ps [Elim]
    vs
        (Def QName
    c [Elim]
    ps, Def QName
    d [Elim]
    vs) | QName
    c QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    d  -> Window -> [Elim] -> [Elim] -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> [Elim] -> [Elim] -> MaybeT m MatchResult
    match Window
    w [Elim]
    ps [Elim]
    vs
        (Con ConHead
    c ConInfo
    _ [Elim]
    ps, Con ConHead
    d ConInfo
    _ [Elim]
    vs) | ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    d -> Window -> [Elim] -> [Elim] -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> [Elim] -> [Elim] -> MaybeT m MatchResult
    match Window
    w [Elim]
    ps [Elim]
    vs
        (Lit Literal
    l, Lit Literal
    l')      | Literal
    l Literal -> Literal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Literal
    l' -> MatchResult -> MaybeT m MatchResult
    forall a. a -> MaybeT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return MatchResult
    forall a. Monoid a => a
    mempty
        (Lam ArgInfo
    h Abs Term
    p, Lam ArgInfo
    h' Abs Term
    v)  | ArgInfo
    h ArgInfo -> ArgInfo -> Bool
    forall a. Eq a => a -> a -> Bool
    == ArgInfo
    h' -> Window -> Term -> Term -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> Term -> Term -> MaybeT m MatchResult
    match (Window -> Window
    shiftWindow Window
    w) (Abs Term -> Term
    forall a. Abs a -> a
    unAbs Abs Term
    p) (Abs Term -> Term
    forall a. Abs a -> a
    unAbs Abs Term
    v)
        (Term
    p, Term
    v)               | Term
    p Term -> Term -> Bool
    forall a. Eq a => a -> a -> Bool
    == Term
    v  -> MatchResult -> MaybeT m MatchResult
    forall a. a -> MaybeT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return MatchResult
    forall a. Monoid a => a
    mempty  -- TODO: this is wrong (this is why we lifted the rhs before)
        (Term
    p, Level Level
    l)                   -> Window -> Term -> Term -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> Term -> Term -> MaybeT m MatchResult
    match Window
    w Term
    p (Term -> MaybeT m MatchResult)
    -> MaybeT m Term -> MaybeT m MatchResult
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Level -> MaybeT m Term
    forall (m :: * -> *). HasBuiltins m => Level -> m Term
    reallyUnLevelView Level
    l
        (Sort Sort
    ps, Sort Sort
    pv)             -> Window -> Sort -> Sort -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> Sort -> Sort -> MaybeT m MatchResult
    match Window
    w Sort
    ps Sort
    pv
        (Term
    p, Sort (Type Level
    v))             -> Window -> Term -> Term -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> Term -> Term -> MaybeT m MatchResult
    match Window
    w Term
    p (Term -> MaybeT m MatchResult)
    -> MaybeT m Term -> MaybeT m MatchResult
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Level -> MaybeT m Term
    forall (m :: * -> *). HasBuiltins m => Level -> m Term
    reallyUnLevelView Level
    v
        (Term, Term)
    _                              -> MaybeT m MatchResult
    forall a. MaybeT m a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    instance Match Sort where
      match :: forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> Sort -> Sort -> MaybeT m MatchResult
    match Window
    w Sort
    p Sort
    v = case (Sort
    p, Sort
    v) of
        (Type Level
    pl, Type Level
    vl) -> Window -> Level -> Level -> MaybeT m MatchResult
    forall a (m :: * -> *).
    (Match a, MonadDisplayForm m) =>
    Window -> a -> a -> MaybeT m MatchResult
    forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> Level -> Level -> MaybeT m MatchResult
    match Window
    w Level
    pl Level
    vl
        (Sort, Sort)
    _ | Sort
    p Sort -> Sort -> Bool
    forall a. Eq a => a -> a -> Bool
    == Sort
    v -> MatchResult -> MaybeT m MatchResult
    forall a. a -> MaybeT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return MatchResult
    forall a. Monoid a => a
    mempty
        (Sort, Sort)
    _          -> MaybeT m MatchResult
    forall a. MaybeT m a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    instance Match Level where
      match :: forall (m :: * -> *).
    MonadDisplayForm m =>
    Window -> Level -> Level -> MaybeT m MatchResult
    match Window
    w Level
    p Level
    v = do
        p <- Level -> MaybeT m Term
    forall (m :: * -> *). HasBuiltins m => Level -> m Term
    reallyUnLevelView Level
    p
        v <- reallyUnLevelView v
        match w p v

    -- | Substitute terms with origin into display terms,
    --   replacing variables along with their origins.
    --
    --   The purpose is to replace the pattern variables in a with-display form,
    --   and only on the top level of the lhs.  Thus, we are happy to fall back
    --   to ordinary substitution where it does not matter.
    --   This fixes issue #2590.

    class SubstWithOrigin a where
      substWithOrigin :: Substitution -> [WithOrigin Term] -> a -> a

    instance SubstWithOrigin a => SubstWithOrigin [a] where
      substWithOrigin :: Substitution -> [WithOrigin Term] -> [a] -> [a]
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots = (a -> a) -> [a] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    map (Substitution -> [WithOrigin Term] -> a -> a
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots)

    instance SubstWithOrigin a => SubstWithOrigin (List1 a) where
      substWithOrigin :: Substitution -> [WithOrigin Term] -> List1 a -> List1 a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots = (a -> a) -> List1 a -> List1 a
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Substitution -> [WithOrigin Term] -> a -> a
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots)

    instance (SubstWithOrigin a, SubstWithOrigin (Arg a)) => SubstWithOrigin (Elim' a) where
      substWithOrigin :: Substitution -> [WithOrigin Term] -> Elim' a -> Elim' a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots (Apply Arg a
    arg) = Arg a -> Elim' a
    forall a. Arg a -> Elim' a
    Apply (Arg a -> Elim' a) -> Arg a -> Elim' a
    forall a b. (a -> b) -> a -> b
    $ Substitution -> [WithOrigin Term] -> Arg a -> Arg a
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots Arg a
    arg
      substWithOrigin Substitution
    rho [WithOrigin Term]
    ots e :: Elim' a
    e@Proj{}    = Elim' a
    e
      substWithOrigin Substitution
    rho [WithOrigin Term]
    ots (IApply a
    u a
    v a
    w) = a -> a -> a -> Elim' a
    forall a. a -> a -> a -> Elim' a
    IApply
        (Substitution -> [WithOrigin Term] -> a -> a
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots a
    u)
        (Substitution -> [WithOrigin Term] -> a -> a
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots a
    v)
        (Substitution -> [WithOrigin Term] -> a -> a
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots a
    w)

    instance SubstWithOrigin (Arg Term) where
      substWithOrigin :: Substitution -> [WithOrigin Term] -> Arg Term -> Arg Term
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots (Arg ArgInfo
    ai Term
    v) =
        case Term
    v of
          -- pattern variable: replace origin if better
          Var Nat
    x [] -> case [WithOrigin Term]
    ots [WithOrigin Term] -> Nat -> Maybe (WithOrigin Term)
    forall a. [a] -> Nat -> Maybe a
    !!! Nat
    x of
            Just (WithOrigin Origin
    o Term
    u) -> ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ((Origin -> Origin) -> ArgInfo -> ArgInfo
    forall a. LensOrigin a => (Origin -> Origin) -> a -> a
    mapOrigin (Origin -> Origin -> Origin
    replaceOrigin Origin
    o) ArgInfo
    ai) Term
    u
            Maybe (WithOrigin Term)
    Nothing -> ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    rho Term
    v -- Issue #2717, not __IMPOSSIBLE__
          -- constructor: recurse
          Con ConHead
    c ConInfo
    ci [Elim]
    args -> ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ ConHead -> ConInfo -> [Elim] -> Term
    Con ConHead
    c ConInfo
    ci ([Elim] -> Term) -> [Elim] -> Term
    forall a b. (a -> b) -> a -> b
    $ Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [Elim]
    args
          -- def: recurse
          Def QName
    q [Elim]
    es -> ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ QName -> [Elim] -> Term
    Def QName
    q ([Elim] -> Term) -> [Elim] -> Term
    forall a b. (a -> b) -> a -> b
    $ Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [Elim]
    es
          -- otherwise: fall back to ordinary substitution
          Term
    _ -> ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    rho Term
    v
        where
          replaceOrigin :: Origin -> Origin -> Origin
    replaceOrigin Origin
    _ Origin
    UserWritten = Origin
    UserWritten
          replaceOrigin Origin
    o Origin
    _           = Origin
    o

    instance SubstWithOrigin Term where
      substWithOrigin :: Substitution -> [WithOrigin Term] -> Term -> Term
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots Term
    v =
        case Term
    v of
          -- constructor: recurse
          Con ConHead
    c ConInfo
    ci [Elim]
    args -> ConHead -> ConInfo -> [Elim] -> Term
    Con ConHead
    c ConInfo
    ci ([Elim] -> Term) -> [Elim] -> Term
    forall a b. (a -> b) -> a -> b
    $ Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [Elim]
    args
          -- def: recurse
          Def QName
    q [Elim]
    es -> QName -> [Elim] -> Term
    Def QName
    q ([Elim] -> Term) -> [Elim] -> Term
    forall a b. (a -> b) -> a -> b
    $ Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [Elim]
    es
          -- otherwise: fall back to oridinary substitution
          Term
    _ -> Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    rho Term
    v

    -- Do not go into dot pattern, otherwise interaction test #231 fails
    instance SubstWithOrigin DisplayTerm where
      substWithOrigin :: Substitution -> [WithOrigin Term] -> DisplayTerm -> DisplayTerm
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots =
        \case
          DTerm' Term
    v [Elim]
    es    -> Term -> [Elim] -> DisplayTerm
    DTerm' (Substitution -> [WithOrigin Term] -> Term -> Term
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots Term
    v) ([Elim] -> DisplayTerm) -> [Elim] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [Elim]
    es
          DDot'  Term
    v [Elim]
    es    -> Term -> [Elim] -> DisplayTerm
    DDot'  (Substitution -> [WithOrigin Term] -> Term -> Term
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots Term
    v) ([Elim] -> DisplayTerm) -> [Elim] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [Elim]
    es
          DDef QName
    q [Elim' DisplayTerm]
    es      -> QName -> [Elim' DisplayTerm] -> DisplayTerm
    DDef QName
    q    ([Elim' DisplayTerm] -> DisplayTerm)
    -> [Elim' DisplayTerm] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution
    -> [WithOrigin Term] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [Elim' DisplayTerm]
    es
          DCon ConHead
    c ConInfo
    ci [Arg DisplayTerm]
    args -> ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
    DCon ConHead
    c ConInfo
    ci ([Arg DisplayTerm] -> DisplayTerm)
    -> [Arg DisplayTerm] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution
    -> [WithOrigin Term] -> [Arg DisplayTerm] -> [Arg DisplayTerm]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [Arg DisplayTerm]
    args
          DWithApp DisplayTerm
    t List1 DisplayTerm
    ts [Elim]
    es -> DisplayTerm -> List1 DisplayTerm -> [Elim] -> DisplayTerm
    DWithApp
            (Substitution -> [WithOrigin Term] -> DisplayTerm -> DisplayTerm
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots DisplayTerm
    t)
            (Substitution
    -> [WithOrigin Term] -> List1 DisplayTerm -> List1 DisplayTerm
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots List1 DisplayTerm
    ts)
            (Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [Elim]
    es)

    -- Do not go into dot pattern, otherwise interaction test #231 fails
    instance SubstWithOrigin (Arg DisplayTerm) where
      substWithOrigin :: Substitution
    -> [WithOrigin Term] -> Arg DisplayTerm -> Arg DisplayTerm
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots (Arg ArgInfo
    ai DisplayTerm
    dt) =
        case DisplayTerm
    dt of
          DTerm' Term
    v [Elim]
    es    -> Substitution -> [WithOrigin Term] -> Arg Term -> Arg Term
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots (ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai Term
    v) Arg Term -> (Term -> DisplayTerm) -> Arg DisplayTerm
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> (Term -> [Elim] -> DisplayTerm
    `DTerm'` Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [Elim]
    es)
          DDot'  Term
    v [Elim]
    es    -> ArgInfo -> DisplayTerm -> Arg DisplayTerm
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (DisplayTerm -> Arg DisplayTerm) -> DisplayTerm -> Arg DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Term -> [Elim] -> DisplayTerm
    DDot' (Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    rho Term
    v)  ([Elim] -> DisplayTerm) -> [Elim] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [Elim]
    es
          DDef QName
    q [Elim' DisplayTerm]
    es      -> ArgInfo -> DisplayTerm -> Arg DisplayTerm
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (DisplayTerm -> Arg DisplayTerm) -> DisplayTerm -> Arg DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ QName -> [Elim' DisplayTerm] -> DisplayTerm
    DDef QName
    q    ([Elim' DisplayTerm] -> DisplayTerm)
    -> [Elim' DisplayTerm] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution
    -> [WithOrigin Term] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [Elim' DisplayTerm]
    es
          DCon ConHead
    c ConInfo
    ci [Arg DisplayTerm]
    args -> ArgInfo -> DisplayTerm -> Arg DisplayTerm
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (DisplayTerm -> Arg DisplayTerm) -> DisplayTerm -> Arg DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ ConHead -> ConInfo -> [Arg DisplayTerm] -> DisplayTerm
    DCon ConHead
    c ConInfo
    ci ([Arg DisplayTerm] -> DisplayTerm)
    -> [Arg DisplayTerm] -> DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ Substitution
    -> [WithOrigin Term] -> [Arg DisplayTerm] -> [Arg DisplayTerm]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [Arg DisplayTerm]
    args
          DWithApp DisplayTerm
    t List1 DisplayTerm
    ts [Elim]
    es -> ArgInfo -> DisplayTerm -> Arg DisplayTerm
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (DisplayTerm -> Arg DisplayTerm) -> DisplayTerm -> Arg DisplayTerm
    forall a b. (a -> b) -> a -> b
    $ DisplayTerm -> List1 DisplayTerm -> [Elim] -> DisplayTerm
    DWithApp
            (Substitution -> [WithOrigin Term] -> DisplayTerm -> DisplayTerm
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots DisplayTerm
    t)
            (Substitution
    -> [WithOrigin Term] -> List1 DisplayTerm -> List1 DisplayTerm
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots List1 DisplayTerm
    ts)
            (Substitution -> [WithOrigin Term] -> [Elim] -> [Elim]
    forall a.
    SubstWithOrigin a =>
    Substitution -> [WithOrigin Term] -> a -> a
    substWithOrigin Substitution
    rho [WithOrigin Term]
    ots [Elim]
    es)