    -- | Defines 'CutOff' type which is used in "Agda.Interaction.Options".
    --   This module's purpose is to eliminate the dependency of
    --   "Agda.TypeChecking.Monad.Base" on the termination checker and
    --   everything it imports.

    module Agda.Termination.CutOff
      ( CutOff(CutOff, DontCutOff)
      , defaultCutOff
      ) where

    import Control.DeepSeq

    -- | Cut off structural order comparison at some depth in termination checker?

    data CutOff
      = CutOff !Int -- ^ @c >= 0@ means: record decrease up to including @c+1@.
      | DontCutOff
      deriving (CutOff -> CutOff -> Bool
    (CutOff -> CutOff -> Bool)
    -> (CutOff -> CutOff -> Bool) -> Eq CutOff
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: CutOff -> CutOff -> Bool
    $c/= :: CutOff -> CutOff -> Bool
    == :: CutOff -> CutOff -> Bool
    $c== :: CutOff -> CutOff -> Bool
    Eq , Eq CutOff
    Eq CutOff
    -> (CutOff -> CutOff -> Ordering)
    -> (CutOff -> CutOff -> Bool)
    -> (CutOff -> CutOff -> Bool)
    -> (CutOff -> CutOff -> Bool)
    -> (CutOff -> CutOff -> Bool)
    -> (CutOff -> CutOff -> CutOff)
    -> (CutOff -> CutOff -> CutOff)
    -> Ord CutOff
    CutOff -> CutOff -> Bool
    CutOff -> CutOff -> Ordering
    CutOff -> CutOff -> CutOff
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: CutOff -> CutOff -> CutOff
    $cmin :: CutOff -> CutOff -> CutOff
    max :: CutOff -> CutOff -> CutOff
    $cmax :: CutOff -> CutOff -> CutOff
    >= :: CutOff -> CutOff -> Bool
    $c>= :: CutOff -> CutOff -> Bool
    > :: CutOff -> CutOff -> Bool
    $c> :: CutOff -> CutOff -> Bool
    <= :: CutOff -> CutOff -> Bool
    $c<= :: CutOff -> CutOff -> Bool
    < :: CutOff -> CutOff -> Bool
    $c< :: CutOff -> CutOff -> Bool
    compare :: CutOff -> CutOff -> Ordering
    $ccompare :: CutOff -> CutOff -> Ordering
    Ord)

    instance Show CutOff where
      show :: CutOff -> String
    show (CutOff Int
    k) = Int -> String
    forall a. Show a => a -> String
    show Int
    k
      show CutOff
    DontCutOff = String
    "∞"

    instance NFData CutOff where
      rnf :: CutOff -> ()
    rnf (CutOff Int
    _) = ()
      rnf CutOff
    DontCutOff = ()

    -- | The default termination depth.

    defaultCutOff :: CutOff
    defaultCutOff :: CutOff
    defaultCutOff = Int -> CutOff
    CutOff Int
    0 -- minimum value