{-# OPTIONS_GHC -Wunused-imports #-}

-- | 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

import Agda.Utils.Impossible (__IMPOSSIBLE__)

-- | 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
$c== :: CutOff -> CutOff -> Bool
== :: CutOff -> CutOff -> Bool
$c/= :: CutOff -> CutOff -> Bool
/= :: 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
$ccompare :: CutOff -> CutOff -> Ordering
compare :: CutOff -> CutOff -> Ordering
$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
>= :: CutOff -> CutOff -> Bool
$cmax :: CutOff -> CutOff -> CutOff
max :: CutOff -> CutOff -> CutOff
$cmin :: CutOff -> CutOff -> CutOff
min :: CutOff -> CutOff -> CutOff
Ord)

-- | Numeric literals and addition for 'CutOff'.

instance Num CutOff where
  fromInteger :: Integer -> CutOff
fromInteger Integer
n
    | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0    = Int -> CutOff
CutOff (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n)
    | Bool
otherwise = CutOff
forall a. HasCallStack => a
__IMPOSSIBLE__

  CutOff
DontCutOff + :: CutOff -> CutOff -> CutOff
+ CutOff
_          = CutOff
DontCutOff
  CutOff
_          + CutOff
DontCutOff = CutOff
DontCutOff
  CutOff Int
m   + CutOff Int
n   = Int -> CutOff
CutOff (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n)

  CutOff
_ * :: CutOff -> CutOff -> CutOff
* CutOff
_    = CutOff
forall a. HasCallStack => a
__IMPOSSIBLE__
  abs :: CutOff -> CutOff
abs CutOff
_    = CutOff
forall a. HasCallStack => a
__IMPOSSIBLE__
  signum :: CutOff -> CutOff
signum CutOff
_ = CutOff
forall a. HasCallStack => a
__IMPOSSIBLE__
  negate :: CutOff -> CutOff
negate CutOff
_ = CutOff
forall a. HasCallStack => a
__IMPOSSIBLE__

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
2 -- termination-depth=3