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 :: IORef Bool
debug = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. a -> IO (IORef a)
newIORef Bool
False

setDebugging :: Bool -> IO ()
setDebugging :: Bool -> IO ()
setDebugging = forall a. IORef a -> a -> IO ()
writeIORef IORef Bool
debug

trace :: String -> a -> a
trace :: forall a. String -> a -> a
trace String
s = forall a. Bool -> (a -> a) -> a -> a
applyWhen (forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef Bool
debug) forall a b. (a -> b) -> a -> b
$ forall a. String -> a -> a
Debug.trace String
s

traceM :: Applicative f => String -> f ()
traceM :: forall (f :: * -> *). Applicative f => String -> f ()
traceM String
s = forall a. String -> a -> a
trace String
s forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

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

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

instance Plus Int Int Int where
  plus :: Int -> Int -> Int
plus = forall a. Num a => a -> a -> a
(+)

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