{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.Syntax.Common where
import Control.DeepSeq
import Data.ByteString.Char8 (ByteString)
import qualified Data.ByteString.Char8 as ByteString
import Data.Foldable
import Data.Hashable (Hashable(..))
import qualified Data.Strict.Maybe as Strict
import Data.Semigroup hiding (Arg)
import Data.Traversable
import Data.Data (Data)
import Data.Word
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import GHC.Generics (Generic)
import Agda.Syntax.Position
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.PartialOrd
import Agda.Utils.POMonoid
import Agda.Utils.Pretty hiding ((<>))
#include "undefined.h"
import Agda.Utils.Impossible
data Delayed = Delayed | NotDelayed
deriving (Data, Show, Eq, Ord)
instance KillRange Delayed where
killRange = id
data FileType = AgdaFileType | MdFileType | RstFileType | TexFileType | OrgFileType
deriving (Data, Eq, Ord, Show)
instance Pretty FileType where
pretty = \case
AgdaFileType -> "Agda"
MdFileType -> "Markdown"
RstFileType -> "ReStructedText"
TexFileType -> "LaTeX"
OrgFileType -> "org-mode"
data HasEta = NoEta | YesEta
deriving (Data, Show, Eq, Ord)
instance HasRange HasEta where
getRange _ = noRange
instance KillRange HasEta where
killRange = id
instance NFData HasEta where
rnf NoEta = ()
rnf YesEta = ()
data Induction = Inductive | CoInductive
deriving (Data, Eq, Ord, Show)
instance Pretty Induction where
pretty Inductive = "inductive"
pretty CoInductive = "coinductive"
instance HasRange Induction where
getRange _ = noRange
instance KillRange Induction where
killRange = id
instance NFData Induction where
rnf Inductive = ()
rnf CoInductive = ()
data Overlappable = YesOverlap | NoOverlap
deriving (Data, Show, Eq, Ord)
data Hiding = Hidden | Instance Overlappable | NotHidden
deriving (Data, Show, Eq, Ord)
instance Pretty Hiding where
pretty = \case
Hidden -> "hidden"
NotHidden -> "visible"
Instance{} -> "instance"
instance Semigroup Overlappable where
NoOverlap <> NoOverlap = NoOverlap
YesOverlap <> YesOverlap = YesOverlap
_ <> _ = __IMPOSSIBLE__
instance Semigroup Hiding where
NotHidden <> h = h
h <> NotHidden = h
Hidden <> Hidden = Hidden
Instance o <> Instance o' = Instance (o <> o')
_ <> _ = __IMPOSSIBLE__
instance Monoid Overlappable where
mempty = NoOverlap
mappend = (<>)
instance Monoid Hiding where
mempty = NotHidden
mappend = (<>)
instance KillRange Hiding where
killRange = id
instance NFData Overlappable where
rnf NoOverlap = ()
rnf YesOverlap = ()
instance NFData Hiding where
rnf Hidden = ()
rnf (Instance o) = rnf o
rnf NotHidden = ()
data WithHiding a = WithHiding
{ whHiding :: !Hiding
, whThing :: a
}
deriving (Data, 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
instance NFData a => NFData (WithHiding a) where
rnf (WithHiding _ a) = rnf a
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
visible :: LensHiding a => a -> Bool
visible a = getHiding a == NotHidden
notVisible :: LensHiding a => a -> Bool
notVisible a = getHiding a /= NotHidden
hidden :: LensHiding a => a -> Bool
hidden a = getHiding a == Hidden
hide :: LensHiding a => a -> a
hide = setHiding Hidden
hideOrKeepInstance :: LensHiding a => a -> a
hideOrKeepInstance x =
case getHiding x of
Hidden -> x
Instance{} -> x
NotHidden -> setHiding Hidden x
makeInstance :: LensHiding a => a -> a
makeInstance = makeInstance' NoOverlap
makeInstance' :: LensHiding a => Overlappable -> a -> a
makeInstance' o = setHiding (Instance o)
isOverlappable :: LensHiding a => a -> Bool
isOverlappable x =
case getHiding x of
Instance YesOverlap -> True
_ -> False
isInstance :: LensHiding a => a -> Bool
isInstance x =
case getHiding x of
Instance{} -> True
_ -> False
sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding x y =
case (getHiding x, getHiding y) of
(Instance{}, Instance{}) -> True
(hx, hy) -> hx == hy
data Modality = Modality
{ modRelevance :: Relevance
, modQuantity :: Quantity
} deriving (Data, Eq, Ord, Show, Generic)
defaultModality :: Modality
defaultModality = Modality defaultRelevance defaultQuantity
instance Semigroup Modality where
Modality r q <> Modality r' q' = Modality (r <> r') (q <> q')
instance Monoid Modality where
mempty = Modality mempty mempty
mappend = (<>)
instance PartialOrd Modality where
comparable (Modality r q) (Modality r' q') = comparable (r, q) (r', q')
instance POSemigroup Modality where
instance POMonoid Modality where
instance LeftClosedPOMonoid Modality where
inverseCompose = inverseComposeModality
moreUsableModality :: Modality -> Modality -> Bool
moreUsableModality m m' = related m POLE m'
usableModality :: LensModality a => a -> Bool
usableModality a = usableRelevance m && usableQuantity m
where m = getModality a
composeModality :: Modality -> Modality -> Modality
composeModality = (<>)
applyModality :: LensModality a => Modality -> a -> a
applyModality m = mapModality (m `composeModality`)
inverseComposeModality :: Modality -> Modality -> Modality
inverseComposeModality (Modality r q) (Modality r' q') =
Modality (r `inverseComposeRelevance` r')
(q `inverseComposeQuantity` q')
inverseApplyModality :: LensModality a => Modality -> a -> a
inverseApplyModality m = mapModality (m `inverseComposeModality`)
instance KillRange Modality where
killRange = id
instance NFData Modality where
lModRelevance :: Lens' Relevance Modality
lModRelevance f m = f (modRelevance m) <&> \ r -> m { modRelevance = r }
lModQuantity :: Lens' Quantity Modality
lModQuantity f m = f (modQuantity m) <&> \ q -> m { modQuantity = q }
class LensModality a where
getModality :: a -> Modality
setModality :: Modality -> a -> a
setModality = mapModality . const
mapModality :: (Modality -> Modality) -> a -> a
mapModality f a = setModality (f $ getModality a) a
instance LensModality Modality where
getModality = id
setModality = const
mapModality = id
instance LensRelevance Modality where
getRelevance = modRelevance
setRelevance h m = m { modRelevance = h }
mapRelevance f m = m { modRelevance = f (modRelevance m) }
instance LensQuantity Modality where
getQuantity = modQuantity
setQuantity h m = m { modQuantity = h }
mapQuantity f m = m { modQuantity = f (modQuantity m) }
getRelevanceMod :: LensModality a => LensGet Relevance a
getRelevanceMod = getRelevance . getModality
setRelevanceMod :: LensModality a => LensSet Relevance a
setRelevanceMod = mapModality . setRelevance
mapRelevanceMod :: LensModality a => LensMap Relevance a
mapRelevanceMod = mapModality . mapRelevance
getQuantityMod :: LensModality a => LensGet Quantity a
getQuantityMod = getQuantity . getModality
setQuantityMod :: LensModality a => LensSet Quantity a
setQuantityMod = mapModality . setQuantity
mapQuantityMod :: LensModality a => LensMap Quantity a
mapQuantityMod = mapModality . mapQuantity
data Quantity
= Quantity0
| Quantity1
| Quantityω
deriving (Data, Show, Generic, Eq, Enum, Bounded, Ord)
defaultQuantity :: Quantity
defaultQuantity = Quantityω
instance Semigroup Quantity where
Quantity1 <> q = q
q <> Quantity1 = q
Quantity0 <> _ = Quantity0
_ <> Quantity0 = Quantity0
Quantityω <> _ = Quantityω
instance Monoid Quantity where
mempty = Quantity1
mappend = (<>)
instance PartialOrd Quantity where
comparable = curry $ \case
(q, q') | q == q' -> POEQ
(Quantityω, _) -> POLT
(_, Quantityω) -> POGT
_ -> POAny
instance POSemigroup Quantity where
instance POMonoid Quantity where
instance LeftClosedPOMonoid Quantity where
inverseCompose = inverseComposeQuantity
moreQuantity :: Quantity -> Quantity -> Bool
moreQuantity m m' = related m POLE m'
usableQuantity :: LensQuantity a => a -> Bool
usableQuantity a = getQuantity a /= Quantity0
composeQuantity :: Quantity -> Quantity -> Quantity
composeQuantity = (<>)
applyQuantity :: LensQuantity a => Quantity -> a -> a
applyQuantity q = mapQuantity (q `composeQuantity`)
inverseComposeQuantity :: Quantity -> Quantity -> Quantity
inverseComposeQuantity q x =
case (q, x) of
(Quantity1 , x) -> x
(Quantity0 , x) -> Quantityω
(Quantityω , Quantityω) -> Quantityω
(Quantityω , _) -> Quantity0
inverseApplyQuantity :: LensQuantity a => Quantity -> a -> a
inverseApplyQuantity q = mapQuantity (q `inverseComposeQuantity`)
class LensQuantity a where
getQuantity :: a -> Quantity
setQuantity :: Quantity -> a -> a
setQuantity = mapQuantity . const
mapQuantity :: (Quantity -> Quantity) -> a -> a
mapQuantity f a = setQuantity (f $ getQuantity a) a
instance LensQuantity Quantity where
getQuantity = id
setQuantity = const
mapQuantity = id
instance KillRange Quantity where
killRange = id
instance NFData Quantity where
rnf Quantity0 = ()
rnf Quantity1 = ()
rnf Quantityω = ()
data Relevance
= Relevant
| NonStrict
| Irrelevant
deriving (Data, Show, Eq, Enum, Bounded, Generic)
allRelevances :: [Relevance]
allRelevances = [minBound..maxBound]
defaultRelevance :: Relevance
defaultRelevance = Relevant
instance KillRange Relevance where
killRange rel = rel
instance NFData Relevance where
rnf Relevant = ()
rnf NonStrict = ()
rnf Irrelevant = ()
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
isNonStrict :: LensRelevance a => a -> Bool
isNonStrict a = getRelevance a == NonStrict
moreRelevant :: Relevance -> Relevance -> Bool
moreRelevant = (<=)
instance Ord Relevance where
compare = curry $ \case
(r, r') | r == r' -> EQ
(_, Irrelevant) -> LT
(Irrelevant, _) -> GT
(Relevant, _) -> LT
(_, Relevant) -> GT
(NonStrict,NonStrict) -> EQ
instance PartialOrd Relevance where
comparable = comparableOrd
usableRelevance :: LensRelevance a => a -> Bool
usableRelevance a = case getRelevance a of
Irrelevant -> False
NonStrict -> False
Relevant -> True
composeRelevance :: Relevance -> Relevance -> Relevance
composeRelevance r r' =
case (r, r') of
(Irrelevant, _) -> Irrelevant
(_, Irrelevant) -> Irrelevant
(NonStrict, _) -> NonStrict
(_, NonStrict) -> NonStrict
(Relevant, Relevant) -> Relevant
applyRelevance :: LensRelevance a => Relevance -> a -> a
applyRelevance rel = mapRelevance (rel `composeRelevance`)
inverseComposeRelevance :: Relevance -> Relevance -> Relevance
inverseComposeRelevance r x =
case (r, x) of
(Relevant , x) -> x
(Irrelevant, x) -> Relevant
(NonStrict , Irrelevant) -> Irrelevant
(NonStrict , _) -> Relevant
inverseApplyRelevance :: LensRelevance a => Relevance -> a -> a
inverseApplyRelevance rel = mapRelevance (rel `inverseComposeRelevance`)
instance Semigroup Relevance where
(<>) = composeRelevance
instance Monoid Relevance where
mempty = Relevant
mappend = (<>)
instance POSemigroup Relevance where
instance POMonoid Relevance where
instance LeftClosedPOMonoid Relevance where
inverseCompose = inverseComposeRelevance
irrToNonStrict :: Relevance -> Relevance
irrToNonStrict Irrelevant = NonStrict
irrToNonStrict rel = rel
nonStrictToRel :: Relevance -> Relevance
nonStrictToRel NonStrict = Relevant
nonStrictToRel rel = rel
nonStrictToIrr :: Relevance -> Relevance
nonStrictToIrr NonStrict = Irrelevant
nonStrictToIrr rel = rel
data Origin
= UserWritten
| Inserted
| Reflected
| CaseSplit
| Substitution
deriving (Data, Show, Eq, Ord)
instance KillRange Origin where
killRange = id
instance NFData Origin where
rnf UserWritten = ()
rnf Inserted = ()
rnf Reflected = ()
rnf CaseSplit = ()
rnf Substitution = ()
data WithOrigin a = WithOrigin
{ woOrigin :: !Origin
, woThing :: a
}
deriving (Data, Eq, Ord, Show, Functor, Foldable, Traversable)
instance Decoration WithOrigin where
traverseF f (WithOrigin h a) = WithOrigin h <$> f a
instance HasRange a => HasRange (WithOrigin a) where
getRange = getRange . dget
instance SetRange a => SetRange (WithOrigin a) where
setRange = fmap . setRange
instance KillRange a => KillRange (WithOrigin a) where
killRange = fmap killRange
instance NFData a => NFData (WithOrigin a) where
rnf (WithOrigin _ a) = rnf a
class LensOrigin a where
getOrigin :: a -> Origin
setOrigin :: Origin -> a -> a
setOrigin o = mapOrigin (const o)
mapOrigin :: (Origin -> Origin) -> a -> a
mapOrigin f a = setOrigin (f $ getOrigin a) a
instance LensOrigin Origin where
getOrigin = id
setOrigin = const
mapOrigin = id
instance LensOrigin (WithOrigin a) where
getOrigin (WithOrigin h _) = h
setOrigin h (WithOrigin _ a) = WithOrigin h a
mapOrigin f (WithOrigin h a) = WithOrigin (f h) a
data FreeVariables = UnknownFVs | KnownFVs IntSet
deriving (Data, Eq, Ord, Show)
instance Semigroup FreeVariables where
UnknownFVs <> _ = UnknownFVs
_ <> UnknownFVs = UnknownFVs
KnownFVs vs1 <> KnownFVs vs2 = KnownFVs (IntSet.union vs1 vs2)
instance Monoid FreeVariables where
mempty = KnownFVs IntSet.empty
mappend = (<>)
instance NFData FreeVariables where
rnf UnknownFVs = ()
rnf (KnownFVs fv) = rnf fv
unknownFreeVariables :: FreeVariables
unknownFreeVariables = UnknownFVs
noFreeVariables :: FreeVariables
noFreeVariables = mempty
oneFreeVariable :: Int -> FreeVariables
oneFreeVariable = KnownFVs . IntSet.singleton
freeVariablesFromList :: [Int] -> FreeVariables
freeVariablesFromList = mconcat . map oneFreeVariable
class LensFreeVariables a where
getFreeVariables :: a -> FreeVariables
setFreeVariables :: FreeVariables -> a -> a
setFreeVariables o = mapFreeVariables (const o)
mapFreeVariables :: (FreeVariables -> FreeVariables) -> a -> a
mapFreeVariables f a = setFreeVariables (f $ getFreeVariables a) a
instance LensFreeVariables FreeVariables where
getFreeVariables = id
setFreeVariables = const
mapFreeVariables = id
hasNoFreeVariables :: LensFreeVariables a => a -> Bool
hasNoFreeVariables x =
case getFreeVariables x of
UnknownFVs -> False
KnownFVs fv -> IntSet.null fv
data ArgInfo = ArgInfo
{ argInfoHiding :: Hiding
, argInfoModality :: Modality
, argInfoOrigin :: Origin
, argInfoFreeVariables :: FreeVariables
} deriving (Data, Eq, Ord, Show)
instance KillRange ArgInfo where
killRange i = i
class LensArgInfo a where
getArgInfo :: a -> ArgInfo
setArgInfo :: ArgInfo -> a -> a
setArgInfo ai = mapArgInfo (const ai)
mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a
mapArgInfo f a = setArgInfo (f $ getArgInfo a) a
instance LensArgInfo ArgInfo where
getArgInfo = id
setArgInfo = const
mapArgInfo = id
instance NFData ArgInfo where
rnf (ArgInfo a b c d) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d
instance LensHiding ArgInfo where
getHiding = argInfoHiding
setHiding h ai = ai { argInfoHiding = h }
mapHiding f ai = ai { argInfoHiding = f (argInfoHiding ai) }
instance LensModality ArgInfo where
getModality = argInfoModality
setModality m ai = ai { argInfoModality = m }
mapModality f ai = ai { argInfoModality = f (argInfoModality ai) }
instance LensOrigin ArgInfo where
getOrigin = argInfoOrigin
setOrigin o ai = ai { argInfoOrigin = o }
mapOrigin f ai = ai { argInfoOrigin = f (argInfoOrigin ai) }
instance LensFreeVariables ArgInfo where
getFreeVariables = argInfoFreeVariables
setFreeVariables o ai = ai { argInfoFreeVariables = o }
mapFreeVariables f ai = ai { argInfoFreeVariables = f (argInfoFreeVariables ai) }
instance LensRelevance ArgInfo where
getRelevance = getRelevanceMod
setRelevance = setRelevanceMod
mapRelevance = mapRelevanceMod
instance LensQuantity ArgInfo where
getQuantity = getQuantityMod
setQuantity = setQuantityMod
mapQuantity = mapQuantityMod
defaultArgInfo :: ArgInfo
defaultArgInfo = ArgInfo
{ argInfoHiding = NotHidden
, argInfoModality = defaultModality
, argInfoOrigin = UserWritten
, argInfoFreeVariables = UnknownFVs
}
getHidingArgInfo :: LensArgInfo a => LensGet Hiding a
getHidingArgInfo = getHiding . getArgInfo
setHidingArgInfo :: LensArgInfo a => LensSet Hiding a
setHidingArgInfo = mapArgInfo . setHiding
mapHidingArgInfo :: LensArgInfo a => LensMap Hiding a
mapHidingArgInfo = mapArgInfo . mapHiding
getModalityArgInfo :: LensArgInfo a => LensGet Modality a
getModalityArgInfo = getModality . getArgInfo
setModalityArgInfo :: LensArgInfo a => LensSet Modality a
setModalityArgInfo = mapArgInfo . setModality
mapModalityArgInfo :: LensArgInfo a => LensMap Modality a
mapModalityArgInfo = mapArgInfo . mapModality
getOriginArgInfo :: LensArgInfo a => LensGet Origin a
getOriginArgInfo = getOrigin . getArgInfo
setOriginArgInfo :: LensArgInfo a => LensSet Origin a
setOriginArgInfo = mapArgInfo . setOrigin
mapOriginArgInfo :: LensArgInfo a => LensMap Origin a
mapOriginArgInfo = mapArgInfo . mapOrigin
getFreeVariablesArgInfo :: LensArgInfo a => LensGet FreeVariables a
getFreeVariablesArgInfo = getFreeVariables . getArgInfo
setFreeVariablesArgInfo :: LensArgInfo a => LensSet FreeVariables a
setFreeVariablesArgInfo = mapArgInfo . setFreeVariables
mapFreeVariablesArgInfo :: LensArgInfo a => LensMap FreeVariables a
mapFreeVariablesArgInfo = mapArgInfo . mapFreeVariables
data Arg e = Arg
{ argInfo :: ArgInfo
, unArg :: e
} deriving (Data, Ord, Show, Functor, Foldable, Traversable)
instance Decoration Arg where
traverseF f (Arg ai a) = Arg ai <$> f a
instance HasRange a => HasRange (Arg a) where
getRange = getRange . unArg
instance SetRange a => SetRange (Arg a) where
setRange r = fmap $ setRange r
instance KillRange a => KillRange (Arg a) where
killRange (Arg info a) = killRange2 Arg info a
instance Eq a => Eq (Arg a) where
Arg (ArgInfo h1 m1 _ _) x1 == Arg (ArgInfo h2 m2 _ _) x2 =
h1 == h2 && (isIrrelevant m1 || isIrrelevant m2 || x1 == x2)
instance NFData e => NFData (Arg e) where
rnf (Arg a b) = rnf a `seq` rnf b
instance LensArgInfo (Arg a) where
getArgInfo = argInfo
setArgInfo ai arg = arg { argInfo = ai }
mapArgInfo f arg = arg { argInfo = f $ argInfo arg }
instance LensHiding (Arg e) where
getHiding = getHidingArgInfo
setHiding = setHidingArgInfo
mapHiding = mapHidingArgInfo
instance LensModality (Arg e) where
getModality = getModalityArgInfo
setModality = setModalityArgInfo
mapModality = mapModalityArgInfo
instance LensOrigin (Arg e) where
getOrigin = getOriginArgInfo
setOrigin = setOriginArgInfo
mapOrigin = mapOriginArgInfo
instance LensFreeVariables (Arg e) where
getFreeVariables = getFreeVariablesArgInfo
setFreeVariables = setFreeVariablesArgInfo
mapFreeVariables = mapFreeVariablesArgInfo
instance LensRelevance (Arg e) where
getRelevance = getRelevanceMod
setRelevance = setRelevanceMod
mapRelevance = mapRelevanceMod
instance LensQuantity (Arg e) where
getQuantity = getQuantityMod
setQuantity = setQuantityMod
mapQuantity = mapQuantityMod
defaultArg :: a -> Arg a
defaultArg = Arg defaultArgInfo
withArgsFrom :: [a] -> [Arg b] -> [Arg a]
xs `withArgsFrom` args =
zipWith (\x arg -> fmap (const x) arg) xs args
withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg 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 e = Dom
{ domInfo :: ArgInfo
, domFinite :: !Bool
, domName :: Maybe RString
, unDom :: e
} deriving (Data, Ord, Show, Functor, Foldable, Traversable)
instance Decoration Dom where
traverseF f (Dom ai b x a) = Dom ai b x <$> f a
instance HasRange a => HasRange (Dom a) where
getRange = getRange . unDom
instance KillRange a => KillRange (Dom a) where
killRange (Dom info b x a) = killRange4 Dom info b x a
instance Eq a => Eq (Dom a) where
Dom (ArgInfo h1 m1 _ _) b1 s1 x1 == Dom (ArgInfo h2 m2 _ _) b2 s2 x2 =
(h1, m1, b1, s1, x1) == (h2, m2, b2, s2, x2)
instance LensArgInfo (Dom e) where
getArgInfo = domInfo
setArgInfo ai dom = dom { domInfo = ai }
mapArgInfo f dom = dom { domInfo = f $ domInfo dom }
instance LensHiding (Dom e) where
getHiding = getHidingArgInfo
setHiding = setHidingArgInfo
mapHiding = mapHidingArgInfo
instance LensModality (Dom e) where
getModality = getModalityArgInfo
setModality = setModalityArgInfo
mapModality = mapModalityArgInfo
instance LensOrigin (Dom e) where
getOrigin = getOriginArgInfo
setOrigin = setOriginArgInfo
mapOrigin = mapOriginArgInfo
instance LensFreeVariables (Dom e) where
getFreeVariables = getFreeVariablesArgInfo
setFreeVariables = setFreeVariablesArgInfo
mapFreeVariables = mapFreeVariablesArgInfo
instance LensRelevance (Dom e) where
getRelevance = getRelevanceMod
setRelevance = setRelevanceMod
mapRelevance = mapRelevanceMod
instance LensQuantity (Dom e) where
getQuantity = getQuantityMod
setQuantity = setQuantityMod
mapQuantity = mapQuantityMod
argFromDom :: Dom a -> Arg a
argFromDom (Dom i _ _ a) = Arg i a
namedArgFromDom :: Dom a -> NamedArg a
namedArgFromDom (Dom i _ s a) = Arg i $ Named s a
domFromArg :: Arg a -> Dom a
domFromArg (Arg i a) = Dom i False Nothing a
domFromNamedArg :: NamedArg a -> Dom a
domFromNamedArg (Arg i a) = Dom i False (nameOf a) (namedThing a)
defaultDom :: a -> Dom a
defaultDom = defaultArgDom defaultArgInfo
defaultArgDom :: ArgInfo -> a -> Dom a
defaultArgDom info x = Dom info False Nothing x
defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a
defaultNamedArgDom info s = Dom info False (Just $ unranged s)
data Named name a =
Named { nameOf :: Maybe name
, namedThing :: a
}
deriving (Eq, Ord, Show, Data, Functor, Foldable, Traversable)
type Named_ = Named RString
unnamed :: a -> Named name a
unnamed = Named Nothing
named :: name -> a -> Named name a
named = Named . Just
class LensNamed name a | a -> name where
lensNamed :: Lens' (Maybe name) a
instance LensNamed name (Named name a) where
lensNamed f (Named mn a) = f mn <&> \ mn' -> Named mn' a
getNameOf :: LensNamed name a => a -> Maybe name
getNameOf a = a ^. lensNamed
setNameOf :: LensNamed name a => Maybe name -> a -> a
setNameOf = set lensNamed
mapNameOf :: LensNamed name a => (Maybe name -> Maybe name) -> a -> a
mapNameOf = over lensNamed
instance LensNamed name a => LensNamed name (Arg a) where
lensNamed = traverseF . lensNamed
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 (NFData name, NFData a) => NFData (Named name a) where
rnf (Named a b) = rnf a `seq` rnf b
type NamedArg a = Arg (Named_ a)
namedArg :: NamedArg a -> a
namedArg = namedThing . unArg
defaultNamedArg :: a -> NamedArg a
defaultNamedArg = unnamedArg defaultArgInfo
unnamedArg :: ArgInfo -> a -> NamedArg a
unnamedArg info = Arg info . unnamed
updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg = fmap . fmap
setNamedArg :: NamedArg a -> b -> NamedArg b
setNamedArg a b = (b <$) <$> a
data Ranged a = Ranged
{ rangeOf :: Range
, rangedThing :: a
}
deriving (Data, Show, Functor, Foldable, Traversable)
unranged :: a -> Ranged a
unranged = Ranged noRange
instance Pretty a => Pretty (Ranged a) where
pretty = pretty . 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
instance NFData a => NFData (Ranged a) where
rnf (Ranged _ a) = rnf a
type RawName = String
rawNameToString :: RawName -> String
rawNameToString = id
stringToRawName :: String -> RawName
stringToRawName = id
type RString = Ranged RawName
data ConOrigin
= ConOSystem
| ConOCon
| ConORec
| ConOSplit
deriving (Data, Show, Eq, Ord, Enum, Bounded)
instance KillRange ConOrigin where
killRange = id
bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin
bestConInfo ConOSystem o = o
bestConInfo o _ = o
data ProjOrigin
= ProjPrefix
| ProjPostfix
| ProjSystem
deriving (Data, Show, Eq, Ord, Enum, Bounded)
instance KillRange ProjOrigin where
killRange = id
data DataOrRecord = IsData | IsRecord
deriving (Data, Eq, Ord, Show)
data IsInfix = InfixDef | PrefixDef
deriving (Data, Show, Eq, Ord)
data Access
= PrivateAccess Origin
| PublicAccess
| OnlyQualified
deriving (Data, Show, Eq, Ord)
instance Pretty Access where
pretty = text . \case
PrivateAccess _ -> "private"
PublicAccess -> "public"
OnlyQualified -> "only-qualified"
instance NFData Access where
rnf _ = ()
instance HasRange Access where
getRange _ = noRange
instance KillRange Access where
killRange = id
data IsAbstract = AbstractDef | ConcreteDef
deriving (Data, Show, Eq, Ord)
instance KillRange IsAbstract where
killRange = id
data IsInstance = InstanceDef | NotInstanceDef
deriving (Data, Show, Eq, Ord)
instance KillRange IsInstance where
killRange = id
instance HasRange IsInstance where
getRange _ = noRange
instance NFData IsInstance where
rnf InstanceDef = ()
rnf NotInstanceDef = ()
data IsMacro = MacroDef | NotMacroDef
deriving (Data, Show, Eq, Ord)
instance KillRange IsMacro where killRange = id
instance HasRange IsMacro where getRange _ = noRange
type Nat = Int
type Arity = Nat
data NameId = NameId {-# UNPACK #-} !Word64 {-# UNPACK #-} !Word64
deriving (Eq, Ord, Data, Generic, Show)
instance KillRange NameId where
killRange = id
instance Pretty NameId where
pretty (NameId n m) = text $ show n ++ "@" ++ show m
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 NFData NameId where
rnf (NameId _ _) = ()
instance Hashable NameId where
{-# INLINE hashWithSalt #-}
hashWithSalt salt (NameId n m) = hashWithSalt salt (n, m)
newtype MetaId = MetaId { metaId :: Nat }
deriving (Eq, Ord, Num, Real, Enum, Integral, Data)
instance Pretty MetaId where
pretty (MetaId n) = text $ "_" ++ show n
instance Show MetaId where
showsPrec p (MetaId n) = showParen (p > 0) $
showString "MetaId " . shows n
instance NFData MetaId where
rnf (MetaId x) = rnf x
newtype Constr a = Constr a
data PositionInName
= Beginning
| Middle
| End
deriving (Show, Eq, Ord, Data)
data MaybePlaceholder e
= Placeholder !PositionInName
| NoPlaceholder !(Strict.Maybe PositionInName) e
deriving (Data, Eq, Ord, Functor, Foldable, Traversable, Show)
noPlaceholder :: e -> MaybePlaceholder e
noPlaceholder = NoPlaceholder Strict.Nothing
instance HasRange a => HasRange (MaybePlaceholder a) where
getRange Placeholder{} = noRange
getRange (NoPlaceholder _ e) = getRange e
instance KillRange a => KillRange (MaybePlaceholder a) where
killRange p@Placeholder{} = p
killRange (NoPlaceholder p e) = killRange1 (NoPlaceholder p) e
instance NFData a => NFData (MaybePlaceholder a) where
rnf (Placeholder _) = ()
rnf (NoPlaceholder _ a) = rnf a
newtype InteractionId = InteractionId { interactionId :: Nat }
deriving ( Eq
, Ord
, Show
, Num
, Integral
, Real
, Enum
, Data
)
instance Pretty InteractionId where
pretty (InteractionId i) = text $ "?" ++ show i
instance KillRange InteractionId where killRange = id
data ImportDirective' n m = ImportDirective
{ importDirRange :: Range
, using :: Using' n m
, hiding :: [ImportedName' n m]
, impRenaming :: [Renaming' n m]
, publicOpen :: Bool
}
deriving (Data, Eq)
data Using' n m = UseEverything | Using [ImportedName' n m]
deriving (Data, Eq)
instance Semigroup (Using' n m) where
UseEverything <> u = u
u <> UseEverything = u
Using xs <> Using ys = Using (xs ++ ys)
instance Monoid (Using' n m) where
mempty = UseEverything
mappend = (<>)
defaultImportDir :: ImportDirective' n m
defaultImportDir = ImportDirective noRange UseEverything [] [] False
isDefaultImportDir :: ImportDirective' n m -> Bool
isDefaultImportDir (ImportDirective _ UseEverything [] [] False) = True
isDefaultImportDir _ = False
data ImportedName' n m
= ImportedModule m
| ImportedName n
deriving (Data, Eq, Ord, Show)
setImportedName :: ImportedName' a a -> a -> ImportedName' a a
setImportedName (ImportedName x) y = ImportedName y
setImportedName (ImportedModule x) y = ImportedModule y
data Renaming' n m = Renaming
{ renFrom :: ImportedName' n m
, renTo :: ImportedName' n m
, renToRange :: Range
}
deriving (Data, Eq)
instance (HasRange a, HasRange b) => HasRange (ImportDirective' a b) where
getRange = importDirRange
instance (HasRange a, HasRange b) => HasRange (Using' a b) where
getRange (Using xs) = getRange xs
getRange UseEverything = noRange
instance (HasRange a, HasRange b) => HasRange (Renaming' a b) where
getRange r = getRange (renFrom r, renTo r)
instance (HasRange a, HasRange b) => HasRange (ImportedName' a b) where
getRange (ImportedName x) = getRange x
getRange (ImportedModule x) = getRange x
instance (KillRange a, KillRange b) => KillRange (ImportDirective' a b) where
killRange (ImportDirective _ u h r p) =
killRange3 (\u h r -> ImportDirective noRange u h r p) u h r
instance (KillRange a, KillRange b) => KillRange (Using' a b) where
killRange (Using i) = killRange1 Using i
killRange UseEverything = UseEverything
instance (KillRange a, KillRange b) => KillRange (Renaming' a b) where
killRange (Renaming i n _) = killRange2 (\i n -> Renaming i n noRange) i n
instance (KillRange a, KillRange b) => KillRange (ImportedName' a b) where
killRange (ImportedModule n) = killRange1 ImportedModule n
killRange (ImportedName n) = killRange1 ImportedName n
instance (NFData a, NFData b) => NFData (ImportDirective' a b) where
rnf (ImportDirective _ a b c _) = rnf a `seq` rnf b `seq` rnf c
instance (NFData a, NFData b) => NFData (Using' a b) where
rnf UseEverything = ()
rnf (Using a) = rnf a
instance (NFData a, NFData b) => NFData (Renaming' a b) where
rnf (Renaming a b _) = rnf a `seq` rnf b
instance (NFData a, NFData b) => NFData (ImportedName' a b) where
rnf (ImportedModule a) = rnf a
rnf (ImportedName a) = rnf a
data TerminationCheck m
= TerminationCheck
| NoTerminationCheck
| NonTerminating
| Terminating
| TerminationMeasure Range m
deriving (Data, Show, Eq, Functor)
instance KillRange m => KillRange (TerminationCheck m) where
killRange (TerminationMeasure _ m) = TerminationMeasure noRange (killRange m)
killRange t = t
instance NFData a => NFData (TerminationCheck a) where
rnf TerminationCheck = ()
rnf NoTerminationCheck = ()
rnf NonTerminating = ()
rnf Terminating = ()
rnf (TerminationMeasure _ a) = rnf a
type PositivityCheck = Bool
data UniverseCheck = YesUniverseCheck | NoUniverseCheck
deriving (Eq, Ord, Show, Bounded, Enum, Data)
instance KillRange UniverseCheck where
killRange = id