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.Monoid
import Data.Traversable
import Data.Typeable (Typeable)
import GHC.Generics (Generic)
import Test.QuickCheck hiding (Small)
import Agda.Syntax.Position
import Agda.Utils.Functor
import Agda.Utils.Pretty
#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 Monoid Hiding where
mempty = NotHidden
mappend NotHidden h = h
mappend h NotHidden = h
mappend Hidden Hidden = Hidden
mappend Instance Instance = Instance
mappend _ _ = __IMPOSSIBLE__
instance KillRange Hiding where
killRange = id
data WithHiding a = WithHiding Hiding a
deriving (Typeable, Eq, Ord, Show, Functor, Foldable, Traversable)
instance Decoration WithHiding where
traverseF f (WithHiding h a) = WithHiding h <$> f a
instance Applicative WithHiding where
pure = WithHiding mempty
WithHiding h f <*> WithHiding h' a = WithHiding (mappend h h') (f a)
instance HasRange a => HasRange (WithHiding a) where
getRange = getRange . dget
instance SetRange a => SetRange (WithHiding a) where
setRange = fmap . setRange
instance KillRange a => KillRange (WithHiding a) where
killRange = fmap killRange
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
instance LensHiding (WithHiding a) where
getHiding (WithHiding h _) = h
setHiding h (WithHiding _ a) = WithHiding h a
mapHiding f (WithHiding h a) = WithHiding (f h) a
mergeHiding :: LensHiding a => WithHiding a -> a
mergeHiding (WithHiding h a) = mapHiding (mappend h) a
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 Big = Big | Small
deriving (Typeable, Show, Eq, Enum, Bounded)
instance Ord Big where
Big <= Small = False
_ <= _ = True
data Relevance
= Relevant
| NonStrict
| Irrelevant
| Forced Big
| UnusedArg
deriving (Typeable, Show, Eq)
allRelevances :: [Relevance]
allRelevances =
[ Relevant
, NonStrict
, Irrelevant
, Forced Small
, Forced Big
, UnusedArg
]
instance KillRange Relevance where
killRange rel = rel
instance Arbitrary Relevance where
arbitrary = elements allRelevances
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
irrelevantOrUnused :: Relevance -> Bool
irrelevantOrUnused r =
case r of
Irrelevant -> True
UnusedArg -> True
NonStrict -> False
Relevant -> False
Forced{} -> False
unusableRelevance :: Relevance -> Bool
unusableRelevance rel = NonStrict `moreRelevant` rel
composeRelevance :: Relevance -> Relevance -> Relevance
composeRelevance r r' =
case (r, r') of
(Irrelevant, _) -> Irrelevant
(_, Irrelevant) -> Irrelevant
(NonStrict, _) -> NonStrict
(_, NonStrict) -> NonStrict
(Forced b, Forced b') -> Forced (max b b')
(Forced b, _) -> Forced b
(_, Forced b) -> Forced b
(UnusedArg, _) -> UnusedArg
(_, UnusedArg) -> UnusedArg
(Relevant, Relevant) -> Relevant
inverseComposeRelevance :: Relevance -> Relevance -> Relevance
inverseComposeRelevance r x =
case (r, x) of
(Relevant, x) -> x
_ | r == x -> Relevant
(Forced{}, Forced{}) -> Relevant
(UnusedArg, x) -> x
(Forced{}, UnusedArg) -> Relevant
(Forced{}, x) -> x
(Irrelevant, x) -> Relevant
(_, Irrelevant) -> Irrelevant
(NonStrict, _) -> Relevant
ignoreForced :: Relevance -> Relevance
ignoreForced Forced{} = Relevant
ignoreForced UnusedArg = Relevant
ignoreForced Relevant = Relevant
ignoreForced NonStrict = NonStrict
ignoreForced Irrelevant = Irrelevant
irrToNonStrict :: Relevance -> Relevance
irrToNonStrict Irrelevant = NonStrict
irrToNonStrict rel = rel
nonStrictToIrr :: Relevance -> Relevance
nonStrictToIrr NonStrict = Irrelevant
nonStrictToIrr rel = rel
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 SetRange a => SetRange (Arg c a) where
setRange r = fmap $ setRange r
instance (KillRange c, KillRange a) => KillRange (Arg c a) where
killRange (Arg info a) = killRange2 Arg info a
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 r s = case r of
Irrelevant -> "." ++ s
NonStrict -> "?" ++ s
Forced Big -> "!b" ++ s
Forced Small -> "!" ++ s
UnusedArg -> "k" ++ s
Relevant -> "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 (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 SetRange a => SetRange (Named name a) where
setRange r = fmap $ setRange r
instance (KillRange name, KillRange a) => KillRange (Named name a) where
killRange (Named n a) = Named (killRange n) (killRange a)
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 ConPOrigin
= ConPImplicit
| ConPCon
| ConPRec
deriving (Typeable, Show, Eq, Ord, Enum, Bounded)
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, Generic)
instance KillRange NameId where
killRange = id
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)
instance Arbitrary NameId where
arbitrary = elements [ NameId x y | x <- [1, 1], y <- [1, 1] ]
instance CoArbitrary NameId
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