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
class (MeetSemiLattice a, Top a) => Dioid a where
compose :: a -> a -> a
unitCompose :: a