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

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

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

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

class Eq a => Top a where
  top   :: a
  isTop :: a -> Bool
  isTop = (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
==a
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 = Int -> Int -> Int
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