module Agda.Syntax.Common where
import Data.Generics (Typeable, Data)
import Control.Applicative
import Data.Foldable
import Data.Traversable
import Test.QuickCheck
import Agda.Syntax.Position
import Agda.Utils.Monad
import Agda.Utils.Size
#include "../undefined.h"
import Agda.Utils.Impossible
data Induction = Inductive | CoInductive
deriving (Typeable, Data, Show, Eq, Ord)
data Hiding = Hidden | NotHidden
deriving (Typeable, Data, Show, Eq, Ord)
instance KillRange Induction where killRange = id
instance KillRange Hiding where killRange = id
data Arg e = Arg { argHiding :: Hiding, unArg :: e }
deriving (Typeable, Data, Eq, Ord)
instance Functor Arg where
fmap f (Arg h x) = Arg h $ f x
instance Foldable Arg where
foldr f z (Arg _ x) = f x z
instance Traversable Arg where
traverse f (Arg h x) = Arg h <$> f x
instance HasRange a => HasRange (Arg a) where
getRange = getRange . unArg
instance KillRange a => KillRange (Arg a) where
killRange = fmap killRange
instance Sized a => Sized (Arg a) where
size = size . unArg
instance Show a => Show (Arg a) where
show (Arg Hidden x) = "{" ++ show x ++ "}"
show (Arg NotHidden x) = "(" ++ show x ++ ")"
data Named name a =
Named { nameOf :: Maybe name
, namedThing :: a
}
deriving (Eq, Ord, Typeable, Data)
unnamed :: a -> Named name a
unnamed = Named Nothing
named :: name -> a -> Named name a
named = Named . Just
instance Functor (Named name) where
fmap f (Named n x) = Named n $ f x
instance Foldable (Named name) where
foldr f z (Named _ x) = f x z
instance Traversable (Named name) where
traverse f (Named n x) = Named n <$> f x
instance HasRange a => HasRange (Named name a) where
getRange = getRange . namedThing
instance KillRange a => KillRange (Named name a) where
killRange = fmap killRange
instance Sized a => Sized (Named name a) where
size = size . namedThing
instance Show a => Show (Named String a) where
show (Named Nothing x) = show x
show (Named (Just n) x) = n ++ " = " ++ show x
type NamedArg a = Arg (Named String a)
data IsInfix = InfixDef | PrefixDef
deriving (Typeable, Data, Show, Eq, Ord)
data Access = PrivateAccess | PublicAccess
deriving (Typeable, Data, Show, Eq, Ord)
data IsAbstract = AbstractDef | ConcreteDef
deriving (Typeable, Data, Show, Eq, Ord)
type Nat = Integer
type Arity = Nat
data NameId = NameId Nat Integer
deriving (Eq, Ord, Typeable, Data)
instance Enum NameId where
succ (NameId n m) = NameId (n + 1) m
pred (NameId n m) = NameId (n 1) m
toEnum n = __IMPOSSIBLE__
fromEnum (NameId n _) = fromIntegral n
newtype Constr a = Constr a
instance Arbitrary Induction where
arbitrary = elements [Inductive, CoInductive]
instance CoArbitrary Induction where
coarbitrary Inductive = variant 0
coarbitrary CoInductive = variant 1