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 | Instance | NotHidden
deriving (Typeable, Data, Show, Eq, Ord)
data Relevance
= Relevant
| NonStrict
| Irrelevant
| Forced
deriving (Typeable, Data, Show, Eq)
instance Ord Relevance where
(<=) = moreRelevant
moreRelevant :: Relevance -> Relevance -> Bool
moreRelevant r r' =
case (r, r') of
(_, Irrelevant) -> True
(Irrelevant, _) -> False
(Relevant, _) -> True
(_, Relevant) -> False
(Forced, _) -> True
(_, Forced) -> False
(NonStrict,NonStrict) -> True
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, Functor, Foldable, Traversable)
instance Eq a => Eq (Arg a) where
Arg h1 _ x1 == Arg h2 _ x2 = (h1, x1) == (h2, x2)
makeInstance :: Arg a -> Arg a
makeInstance a = a { argHiding = Instance }
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 /= NotHidden
withArgsFrom :: [a] -> [Arg b] -> [Arg a]
xs `withArgsFrom` args =
zipWith (\x arg -> fmap (const x) arg) xs args
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 ++ ")"
showH Instance s = "{{" ++ s ++ "}}"
showR Irrelevant s = "." ++ s
showR NonStrict 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, Functor, Foldable, Traversable)
unnamed :: a -> Named name a
unnamed = Named Nothing
named :: name -> a -> Named name a
named = Named . Just
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
| OnlyQualified
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