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)
data Relevance
= Relevant
| Irrelevant
| Forced
deriving (Typeable, Data, Show, Eq, Ord)
ignoreForced :: Relevance -> Relevance
ignoreForced Forced = Relevant
ignoreForced Relevant = Relevant
ignoreForced Irrelevant = Irrelevant
instance KillRange Induction where killRange = id
instance KillRange Hiding where killRange = id
data Arg e = Arg
{ argHiding :: Hiding
, argRelevance :: Relevance
, unArg :: e
} deriving (Typeable, Data, Ord)
instance Eq a => Eq (Arg a) where
Arg h1 _ x1 == Arg h2 _ x2 = (h1, x1) == (h2, x2)
hide :: Arg a -> Arg a
hide a = a { argHiding = Hidden }
defaultArg :: a -> Arg a
defaultArg = Arg NotHidden Relevant
isHiddenArg :: Arg a -> Bool
isHiddenArg arg = argHiding arg == Hidden
makeIrrelevant :: Arg a -> Arg a
makeIrrelevant a = a { argRelevance = Irrelevant }
makeRelevant :: Arg a -> Arg a
makeRelevant a = if argRelevance a == Irrelevant
then a { argRelevance = Relevant }
else a
withArgsFrom :: [a] -> [Arg b] -> [Arg a]
xs `withArgsFrom` args =
zipWith (\x arg -> fmap (const x) arg) xs args
instance Functor Arg where
fmap f a = a { unArg = f (unArg a) }
instance Foldable Arg where
foldr f z a = f (unArg a) z
instance Traversable Arg where
traverse f (Arg h r x) = Arg h r <$> 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 h r x) = showR r $ showH h $ show x
where
showH Hidden s = "{" ++ s ++ "}"
showH NotHidden s = "(" ++ s ++ ")"
showR Irrelevant s = "." ++ s
showR Forced s = "!" ++ s
showR Relevant s = "r" ++ s
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