module Agda.Syntax.Common where
import Control.Applicative
import Data.ByteString.Char8 (ByteString)
import qualified Data.ByteString.Char8 as ByteString
import Data.Foldable
import Data.Hashable
import Data.Traversable
import Data.Typeable (Typeable)
import Test.QuickCheck
import Agda.Syntax.Position
import Agda.Utils.Functor
import Agda.Utils.Pretty
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
data Delayed = Delayed | NotDelayed
deriving (Typeable, Show, Eq, Ord)
instance KillRange Delayed where
killRange = id
data Induction = Inductive | CoInductive
deriving (Typeable, Eq, Ord)
instance Show Induction where
show Inductive = "inductive"
show CoInductive = "coinductive"
instance HasRange Induction where
getRange _ = noRange
instance KillRange Induction where
killRange = id
instance Arbitrary Induction where
arbitrary = elements [Inductive, CoInductive]
instance CoArbitrary Induction where
coarbitrary Inductive = variant 0
coarbitrary CoInductive = variant 1
data Hiding = Hidden | Instance | NotHidden
deriving (Typeable, Show, Eq, Ord)
instance KillRange Hiding where
killRange = id
class LensHiding a where
getHiding :: a -> Hiding
setHiding :: Hiding -> a -> a
setHiding h = mapHiding (const h)
mapHiding :: (Hiding -> Hiding) -> a -> a
mapHiding f a = setHiding (f $ getHiding a) a
instance LensHiding Hiding where
getHiding = id
setHiding = const
mapHiding = id
isHidden :: LensHiding a => a -> Bool
isHidden a = getHiding a == Hidden
notHidden :: LensHiding a => a -> Bool
notHidden a = getHiding a == NotHidden
visible :: LensHiding a => a -> Bool
visible a = getHiding a == NotHidden
notVisible :: LensHiding a => a -> Bool
notVisible a = getHiding a /= NotHidden
hide :: LensHiding a => a -> a
hide = setHiding Hidden
makeInstance :: LensHiding a => a -> a
makeInstance = setHiding Instance
data Relevance
= Relevant
| NonStrict
| Irrelevant
| Forced
| UnusedArg
deriving (Typeable, Show, Eq, Enum, Bounded)
instance KillRange Relevance where
killRange rel = rel
instance Arbitrary Relevance where
arbitrary = elements [minBound..maxBound]
instance Ord Relevance where
(<=) = moreRelevant
class LensRelevance a where
getRelevance :: a -> Relevance
setRelevance :: Relevance -> a -> a
setRelevance h = mapRelevance (const h)
mapRelevance :: (Relevance -> Relevance) -> a -> a
mapRelevance f a = setRelevance (f $ getRelevance a) a
instance LensRelevance Relevance where
getRelevance = id
setRelevance = const
mapRelevance = id
isRelevant :: LensRelevance a => a -> Bool
isRelevant a = getRelevance a == Relevant
isIrrelevant :: LensRelevance a => a -> Bool
isIrrelevant a = getRelevance a == Irrelevant
moreRelevant :: Relevance -> Relevance -> Bool
moreRelevant r r' =
case (r, r') of
(_, Irrelevant) -> True
(Irrelevant, _) -> False
(Relevant, _) -> True
(_, Relevant) -> False
(UnusedArg, _) -> True
(_, UnusedArg) -> False
(Forced, _) -> True
(_, Forced) -> False
(NonStrict,NonStrict) -> True
data ArgInfo c = ArgInfo
{ argInfoHiding :: Hiding
, argInfoRelevance :: Relevance
, argInfoColors :: [c]
} deriving (Typeable, Eq, Ord, Functor, Foldable, Traversable, Show)
instance KillRange c => KillRange (ArgInfo c) where
killRange (ArgInfo h r cs) = killRange3 ArgInfo h r cs
instance LensHiding (ArgInfo c) where
getHiding = argInfoHiding
setHiding h ai = ai { argInfoHiding = h }
mapHiding f ai = ai { argInfoHiding = f (argInfoHiding ai) }
instance LensRelevance (ArgInfo c) where
getRelevance = argInfoRelevance
setRelevance h ai = ai { argInfoRelevance = h }
mapRelevance f ai = ai { argInfoRelevance = f (argInfoRelevance ai) }
mapArgInfoColors :: ([c] -> [c']) -> ArgInfo c -> ArgInfo c'
mapArgInfoColors f info = info { argInfoColors = f $ argInfoColors info }
defaultArgInfo :: ArgInfo c
defaultArgInfo = ArgInfo { argInfoHiding = NotHidden
, argInfoRelevance = Relevant
, argInfoColors = [] }
data Arg c e = Arg
{ argInfo :: ArgInfo c
, unArg :: e
} deriving (Typeable, Ord, Functor, Foldable, Traversable)
instance Decoration (Arg c) where
traverseF f (Arg ai a) = Arg ai <$> f a
instance HasRange a => HasRange (Arg c a) where
getRange = getRange . unArg
instance (KillRange c, KillRange a) => KillRange (Arg c a) where
killRange (Arg info a) = killRange2 Arg info a
instance Sized a => Sized (Arg c a) where
size = size . unArg
instance (Eq a, Eq c) => Eq (Arg c a) where
Arg (ArgInfo h1 _ cs1) x1 == Arg (ArgInfo h2 _ cs2) x2 = (h1, cs1, x1) == (h2, cs2, x2)
instance (Show a, Show c) => Show (Arg c a) where
show (Arg (ArgInfo h r cs) x) = showC cs $ 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 UnusedArg s = "k" ++ s
showR Relevant s = "r" ++ s
showC cs s = show cs ++ s
instance LensHiding (Arg c e) where
getHiding = getHiding . argInfo
mapHiding = mapArgInfo . mapHiding
instance LensRelevance (Arg c e) where
getRelevance = getRelevance . argInfo
mapRelevance = mapArgInfo . mapRelevance
mapArgInfo :: (ArgInfo c -> ArgInfo c') -> Arg c a -> Arg c' a
mapArgInfo f arg = arg { argInfo = f $ argInfo arg }
argColors :: Arg c a -> [c]
argColors = argInfoColors . argInfo
mapArgColors :: ([c] -> [c']) -> Arg c a -> Arg c' a
mapArgColors = mapArgInfo . mapArgInfoColors
setArgColors :: [c] -> Arg c' a -> Arg c a
setArgColors = mapArgColors . const
defaultArg :: a -> Arg c a
defaultArg = Arg defaultArgInfo
defaultColoredArg :: ([c],a) -> Arg c a
defaultColoredArg (cs,a) = setArgColors cs $ defaultArg a
noColorArg :: Hiding -> Relevance -> a -> Arg c a
noColorArg h r = Arg ArgInfo { argInfoHiding = h
, argInfoRelevance = r
, argInfoColors = []
}
withArgsFrom :: [a] -> [Arg c b] -> [Arg c a]
xs `withArgsFrom` args =
zipWith (\x arg -> fmap (const x) arg) xs args
withNamedArgsFrom :: [a] -> [NamedArg c b] -> [NamedArg c a]
xs `withNamedArgsFrom` args =
zipWith (\x -> fmap (x <$)) xs args
class Eq a => Underscore a where
underscore :: a
isUnderscore :: a -> Bool
isUnderscore = (== underscore)
instance Underscore String where
underscore = "_"
instance Underscore ByteString where
underscore = ByteString.pack underscore
instance Underscore Doc where
underscore = text underscore
data Dom c e = Dom
{ domInfo :: ArgInfo c
, unDom :: e
} deriving (Typeable, Eq, Ord, Functor, Foldable, Traversable)
instance Decoration (Dom c) where
traverseF f (Dom ai a) = Dom ai <$> f a
instance HasRange a => HasRange (Dom c a) where
getRange = getRange . unDom
instance (KillRange c, KillRange a) => KillRange (Dom c a) where
killRange (Dom info a) = killRange2 Dom info a
instance Sized a => Sized (Dom c a) where
size = size . unDom
instance (Show a, Show c) => Show (Dom c a) where
show = show . argFromDom
instance LensHiding (Dom c e) where
getHiding = getHiding . domInfo
mapHiding = mapDomInfo . mapHiding
instance LensRelevance (Dom c e) where
getRelevance = getRelevance . domInfo
mapRelevance = mapDomInfo . mapRelevance
mapDomInfo :: (ArgInfo c -> ArgInfo c') -> Dom c a -> Dom c' a
mapDomInfo f arg = arg { domInfo = f $ domInfo arg }
domColors :: Dom c a -> [c]
domColors = argInfoColors . domInfo
argFromDom :: Dom c a -> Arg c a
argFromDom (Dom i a) = Arg i a
domFromArg :: Arg c a -> Dom c a
domFromArg (Arg i a) = Dom i a
defaultDom :: a -> Dom c a
defaultDom = Dom defaultArgInfo
data Named name a =
Named { nameOf :: Maybe name
, namedThing :: a
}
deriving (Eq, Ord, Typeable, Functor, Foldable, Traversable)
type Named_ = Named RString
unnamed :: a -> Named name a
unnamed = Named Nothing
named :: name -> a -> Named name a
named = Named . Just
instance Decoration (Named name) where
traverseF f (Named n a) = Named n <$> f a
instance HasRange a => HasRange (Named name a) where
getRange = getRange . namedThing
instance (KillRange name, KillRange a) => KillRange (Named name a) where
killRange (Named n a) = Named (killRange n) (killRange a)
instance Sized a => Sized (Named name a) where
size = size . namedThing
instance Show a => Show (Named_ a) where
show (Named Nothing x) = show x
show (Named (Just n) x) = rawNameToString (rangedThing n) ++ " = " ++ show x
type NamedArg c a = Arg c (Named_ a)
namedArg :: NamedArg c a -> a
namedArg = namedThing . unArg
defaultNamedArg :: a -> NamedArg c a
defaultNamedArg = defaultArg . unnamed
updateNamedArg :: (a -> b) -> NamedArg c a -> NamedArg c b
updateNamedArg = fmap . fmap
data Ranged a = Ranged
{ rangeOf :: Range
, rangedThing :: a
}
deriving (Typeable, Functor, Foldable, Traversable)
unranged :: a -> Ranged a
unranged = Ranged noRange
instance Show a => Show (Ranged a) where
show = show . rangedThing
instance Eq a => Eq (Ranged a) where
Ranged _ x == Ranged _ y = x == y
instance Ord a => Ord (Ranged a) where
compare (Ranged _ x) (Ranged _ y) = compare x y
instance HasRange (Ranged a) where
getRange = rangeOf
instance KillRange (Ranged a) where
killRange (Ranged _ x) = Ranged noRange x
instance Decoration Ranged where
traverseF f (Ranged r x) = Ranged r <$> f x
type RawName = String
rawNameToString :: RawName -> String
rawNameToString = id
stringToRawName :: String -> RawName
stringToRawName = id
type RString = Ranged RawName
data IsInfix = InfixDef | PrefixDef
deriving (Typeable, Show, Eq, Ord)
data Access = PrivateAccess | PublicAccess
| OnlyQualified
deriving (Typeable, Show, Eq, Ord)
data IsAbstract = AbstractDef | ConcreteDef
deriving (Typeable, Show, Eq, Ord)
instance KillRange IsAbstract where
killRange = id
data IsInstance = InstanceDef | NotInstanceDef
deriving (Typeable, Show, Eq, Ord)
type Nat = Int
type Arity = Nat
data NameId = NameId Integer Integer
deriving (Eq, Ord, Typeable)
instance Show NameId where
show (NameId x i) = show x ++ "@" ++ show i
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
instance Hashable NameId where
hashWithSalt salt (NameId n m) = hashWithSalt salt (n, m)
newtype Constr a = Constr a
newtype InteractionId = InteractionId { interactionId :: Nat }
deriving (Eq,Ord,Num,Integral,Real,Enum)
instance Show InteractionId where
show (InteractionId x) = "?" ++ show x
instance KillRange InteractionId where killRange = id
data TerminationCheck m
= TerminationCheck
| NoTerminationCheck
| NonTerminating
| Terminating
| TerminationMeasure !Range m
deriving (Typeable, Show, Eq, Functor)
instance KillRange m => KillRange (TerminationCheck m) where
killRange (TerminationMeasure _ m) = TerminationMeasure noRange (killRange m)
killRange t = t