module Agda.TypeChecking.SizedTypes.Utils where

import Data.IORef
import qualified Debug.Trace as Debug
import System.IO.Unsafe

import Agda.Utils.Function

{-# NOINLINE debug #-}
debug :: IORef Bool
debug = unsafePerformIO $ newIORef False

setDebugging :: Bool -> IO ()
setDebugging = writeIORef debug

trace :: String -> a -> a
trace s = applyWhen (unsafePerformIO $ readIORef debug) $ Debug.trace s

traceM :: Applicative f => String -> f ()
traceM s = trace s $ pure ()

class Eq a => Top a where
  top   :: a
  isTop :: a -> Bool
  isTop = (==top)

class Plus a b c where
  plus :: a -> b -> c

instance Plus Int Int Int where
  plus = (+)

class MeetSemiLattice a where
  meet :: a -> a -> a

-- | Semiring with idempotent '+' == dioid
class (MeetSemiLattice a, Top a) => Dioid a where
  compose     :: a -> a -> a  -- ^ E.g. +
  unitCompose :: a            -- ^ neutral element of @compose@, e.g. zero