{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.Syntax.Common where
import Prelude hiding (null)
import Control.DeepSeq
import Control.Arrow ((&&&))
#if __GLASGOW_HASKELL__ < 804
import Data.Semigroup hiding (Arg)
#endif
import Data.ByteString.Char8 (ByteString)
import qualified Data.ByteString.Char8 as ByteString
import Data.Foldable (Foldable)
import qualified Data.Foldable as Fold
import Data.Function
import Data.Hashable (Hashable(..))
import qualified Data.Strict.Maybe as Strict
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.Maybe
import Agda.Utils.Null
import Agda.Utils.PartialOrd
import Agda.Utils.POMonoid
import Agda.Utils.Pretty
import Agda.Utils.Impossible
type Nat = Int
type Arity = Nat
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
default getHiding :: LensArgInfo a => a -> Hiding
getHiding = argInfoHiding . getArgInfo
default mapHiding :: LensArgInfo a => (Hiding -> Hiding) -> a -> a
mapHiding f = mapArgInfo $ \ ai -> ai { argInfoHiding = f $ argInfoHiding ai }
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
, modCohesion :: Cohesion
} deriving (Data, Eq, Ord, Show, Generic)
defaultModality :: Modality
defaultModality = Modality defaultRelevance defaultQuantity defaultCohesion
instance Semigroup Modality where
Modality r q c <> Modality r' q' c' = Modality (r <> r') (q <> q') (c <> c')
instance Monoid Modality where
mempty = Modality mempty mempty mempty
mappend = (<>)
instance PartialOrd Modality where
comparable (Modality r q c) (Modality r' q' c') = comparable (r, (q, c)) (r', (q', c'))
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 c) (Modality r' q' c') =
Modality (r `inverseComposeRelevance` r')
(q `inverseComposeQuantity` q')
(c `inverseComposeCohesion` c')
inverseApplyModality :: LensModality a => Modality -> a -> a
inverseApplyModality m = mapModality (m `inverseComposeModality`)
addModality :: Modality -> Modality -> Modality
addModality (Modality r q c) (Modality r' q' c') = Modality (addRelevance r r') (addQuantity q q') (addCohesion c c')
zeroModality :: Modality
zeroModality = Modality zeroRelevance zeroQuantity zeroCohesion
topModality :: Modality
topModality = Modality topRelevance topQuantity topCohesion
sameModality :: (LensModality a, LensModality b) => a -> b -> Bool
sameModality x y = case (getModality x , getModality y) of
(Modality r q c , Modality r' q' c') -> sameRelevance r r' && sameQuantity q q' && sameCohesion c c'
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 }
lModCohesion :: Lens' Cohesion Modality
lModCohesion f m = f (modCohesion m) <&> \ q -> m { modCohesion = q }
class LensModality a where
getModality :: a -> Modality
setModality :: Modality -> a -> a
setModality = mapModality . const
mapModality :: (Modality -> Modality) -> a -> a
default getModality :: LensArgInfo a => a -> Modality
getModality = argInfoModality . getArgInfo
default mapModality :: LensArgInfo a => (Modality -> Modality) -> a -> a
mapModality f = mapArgInfo $ \ ai -> ai { argInfoModality = f $ argInfoModality ai }
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) }
instance LensCohesion Modality where
getCohesion = modCohesion
setCohesion h m = m { modCohesion = h }
mapCohesion f m = m { modCohesion = f (modCohesion 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
getCohesionMod :: LensModality a => LensGet Cohesion a
getCohesionMod = getCohesion . getModality
setCohesionMod :: LensModality a => LensSet Cohesion a
setCohesionMod = mapModality . setCohesion
mapCohesionMod :: LensModality a => LensMap Cohesion a
mapCohesionMod = mapModality . mapCohesion
data Q0Origin
= Q0Inferred
| Q0 Range
| Q0Erased Range
deriving (Data, Show, Generic, Eq, Ord)
data Q1Origin
= Q1Inferred
| Q1 Range
| Q1Linear Range
deriving (Data, Show, Generic, Eq, Ord)
data QωOrigin
= QωInferred
| Qω Range
| QωPlenty Range
deriving (Data, Show, Generic, Eq, Ord)
instance Semigroup Q0Origin where
(<>) = curry $ \case
(Q0Inferred, o) -> o
(o, Q0Inferred) -> o
(o, Q0 r) -> Q0 $ fuseRange o r
(o, Q0Erased r) -> Q0 $ fuseRange o r
instance Monoid Q0Origin where
mempty = Q0Inferred
mappend = (<>)
instance Null Q0Origin where
empty = mempty
instance HasRange Q0Origin where
getRange = \case
Q0Inferred -> noRange
Q0 r -> r
Q0Erased r -> r
instance SetRange Q0Origin where
setRange r = \case
Q0Inferred -> Q0Inferred
Q0 _ -> Q0 r
Q0Erased _ -> Q0Erased r
instance KillRange Q0Origin where
killRange = \case
Q0Inferred -> Q0Inferred
Q0 _ -> Q0 noRange
Q0Erased _ -> Q0Erased noRange
instance NFData Q0Origin where
rnf = \case
Q0Inferred -> ()
Q0 _ -> ()
Q0Erased _ -> ()
instance Semigroup Q1Origin where
(<>) = curry $ \case
(Q1Inferred, o) -> o
(o, Q1Inferred) -> o
(o, Q1 r) -> Q1 $ fuseRange o r
(o, Q1Linear r) -> Q1 $ fuseRange o r
instance Monoid Q1Origin where
mempty = Q1Inferred
mappend = (<>)
instance Null Q1Origin where
empty = mempty
instance HasRange Q1Origin where
getRange = \case
Q1Inferred -> noRange
Q1 r -> r
Q1Linear r -> r
instance SetRange Q1Origin where
setRange r = \case
Q1Inferred -> Q1Inferred
Q1 _ -> Q1 r
Q1Linear _ -> Q1Linear r
instance KillRange Q1Origin where
killRange = \case
Q1Inferred -> Q1Inferred
Q1 _ -> Q1 noRange
Q1Linear _ -> Q1Linear noRange
instance NFData Q1Origin where
rnf = \case
Q1Inferred -> ()
Q1 _ -> ()
Q1Linear _ -> ()
instance Semigroup QωOrigin where
(<>) = curry $ \case
(QωInferred, o) -> o
(o, QωInferred) -> o
(o, Qω r) -> Qω $ fuseRange o r
(o, QωPlenty r) -> Qω $ fuseRange o r
instance Monoid QωOrigin where
mempty = QωInferred
mappend = (<>)
instance Null QωOrigin where
empty = mempty
instance HasRange QωOrigin where
getRange = \case
QωInferred -> noRange
Qω r -> r
QωPlenty r -> r
instance SetRange QωOrigin where
setRange r = \case
QωInferred -> QωInferred
Qω _ -> Qω r
QωPlenty _ -> QωPlenty r
instance KillRange QωOrigin where
killRange = \case
QωInferred -> QωInferred
Qω _ -> Qω noRange
QωPlenty _ -> QωPlenty noRange
instance NFData QωOrigin where
rnf = \case
QωInferred -> ()
Qω _ -> ()
QωPlenty _ -> ()
data Quantity
= Quantity0 Q0Origin
| Quantity1 Q1Origin
| Quantityω QωOrigin
deriving (Data, Show, Generic, Eq, Ord)
defaultQuantity :: Quantity
defaultQuantity = topQuantity
sameQuantity :: Quantity -> Quantity -> Bool
sameQuantity = curry $ \case
(Quantity0{}, Quantity0{}) -> True
(Quantity1{}, Quantity1{}) -> True
(Quantityω{}, Quantityω{}) -> True
_ -> False
instance Semigroup Quantity where
Quantity1{} <> q = q
q <> Quantity1{} = q
_ <> Quantity0 o = Quantity0 o
Quantity0 o <> _ = Quantity0 o
_omega <> qomega = qomega
instance Monoid Quantity where
mempty = Quantity1 mempty
mappend = (<>)
instance PartialOrd Quantity where
comparable = curry $ \case
(q, q') | sameQuantity q q' -> POEQ
(Quantityω{}, _) -> POLT
(_, Quantityω{}) -> POGT
_ -> POAny
instance POSemigroup Quantity where
instance POMonoid Quantity where
instance LeftClosedPOMonoid Quantity where
inverseCompose = inverseComposeQuantity
addQuantity :: Quantity -> Quantity -> Quantity
addQuantity = curry $ \case
(q@Quantityω{}, _) -> q
(_, q@Quantityω{}) -> q
(Quantity0{}, q) -> q
(q, Quantity0{}) -> q
(Quantity1 _, Quantity1 _) -> topQuantity
zeroQuantity :: Quantity
zeroQuantity = Quantity0 mempty
topQuantity :: Quantity
topQuantity = Quantityω mempty
moreQuantity :: Quantity -> Quantity -> Bool
moreQuantity m m' = related m POLE m'
composeQuantity :: Quantity -> Quantity -> Quantity
composeQuantity = (<>)
applyQuantity :: LensQuantity a => Quantity -> a -> a
applyQuantity q = mapQuantity (q `composeQuantity`)
inverseComposeQuantity :: Quantity -> Quantity -> Quantity
inverseComposeQuantity = curry $ \case
(Quantity1{} , x) -> x
(Quantity0{} , x) -> topQuantity
(Quantityω{} , x@Quantityω{}) -> x
(Quantityω{} , _) -> zeroQuantity
inverseApplyQuantity :: LensQuantity a => Quantity -> a -> a
inverseApplyQuantity q = mapQuantity (q `inverseComposeQuantity`)
hasQuantity0 :: LensQuantity a => a -> Bool
hasQuantity0 a
| Quantity0{} <- getQuantity a = True
| otherwise = False
hasQuantity1 :: LensQuantity a => a -> Bool
hasQuantity1 a
| Quantity1{} <- getQuantity a = True
| otherwise = False
hasQuantityω :: LensQuantity a => a -> Bool
hasQuantityω a
| Quantityω{} <- getQuantity a = True
| otherwise = False
noUserQuantity :: LensQuantity a => a -> Bool
noUserQuantity a = case getQuantity a of
Quantity0 o -> null o
Quantity1 o -> null o
Quantityω o -> null o
usableQuantity :: LensQuantity a => a -> Bool
usableQuantity = not . hasQuantity0
class LensQuantity a where
getQuantity :: a -> Quantity
setQuantity :: Quantity -> a -> a
setQuantity = mapQuantity . const
mapQuantity :: (Quantity -> Quantity) -> a -> a
default getQuantity :: LensModality a => a -> Quantity
getQuantity = modQuantity . getModality
default mapQuantity :: LensModality a => (Quantity -> Quantity) -> a -> a
mapQuantity f = mapModality $ \ ai -> ai { modQuantity = f $ modQuantity ai }
instance LensQuantity Quantity where
getQuantity = id
setQuantity = const
mapQuantity = id
instance HasRange Quantity where
getRange = \case
Quantity0 o -> getRange o
Quantity1 o -> getRange o
Quantityω o -> getRange o
instance SetRange Quantity where
setRange r = \case
Quantity0 o -> Quantity0 $ setRange r o
Quantity1 o -> Quantity1 $ setRange r o
Quantityω o -> Quantityω $ setRange r o
instance KillRange Quantity where
killRange = \case
Quantity0 o -> Quantity0 $ killRange o
Quantity1 o -> Quantity1 $ killRange o
Quantityω o -> Quantityω $ killRange o
instance NFData Quantity where
rnf (Quantity0 o) = rnf o
rnf (Quantity1 o) = rnf o
rnf (Quantityω o) = rnf o
data Relevance
= Relevant
| NonStrict
| Irrelevant
deriving (Data, Show, Eq, Enum, Bounded, Generic)
allRelevances :: [Relevance]
allRelevances = [minBound..maxBound]
defaultRelevance :: Relevance
defaultRelevance = Relevant
instance HasRange Relevance where
getRange _ = noRange
instance SetRange Relevance where
setRange _ = id
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
default getRelevance :: LensModality a => a -> Relevance
getRelevance = modRelevance . getModality
default mapRelevance :: LensModality a => (Relevance -> Relevance) -> a -> a
mapRelevance f = mapModality $ \ ai -> ai { modRelevance = f $ modRelevance ai }
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 = (<=)
sameRelevance :: Relevance -> Relevance -> Bool
sameRelevance = (==)
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
addRelevance :: Relevance -> Relevance -> Relevance
addRelevance = min
zeroRelevance :: Relevance
zeroRelevance = Irrelevant
topRelevance :: Relevance
topRelevance = Relevant
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 Cohesion
= Flat
| Continuous
| Squash
deriving (Data, Show, Eq, Enum, Bounded, Generic)
allCohesions :: [Cohesion]
allCohesions = [minBound..maxBound]
defaultCohesion :: Cohesion
defaultCohesion = Continuous
instance HasRange Cohesion where
getRange _ = noRange
instance SetRange Cohesion where
setRange _ = id
instance KillRange Cohesion where
killRange rel = rel
instance NFData Cohesion where
rnf Flat = ()
rnf Continuous = ()
rnf Squash = ()
class LensCohesion a where
getCohesion :: a -> Cohesion
setCohesion :: Cohesion -> a -> a
setCohesion h = mapCohesion (const h)
mapCohesion :: (Cohesion -> Cohesion) -> a -> a
default getCohesion :: LensModality a => a -> Cohesion
getCohesion = modCohesion . getModality
default mapCohesion :: LensModality a => (Cohesion -> Cohesion) -> a -> a
mapCohesion f = mapModality $ \ ai -> ai { modCohesion = f $ modCohesion ai }
instance LensCohesion Cohesion where
getCohesion = id
setCohesion = const
mapCohesion = id
moreCohesion :: Cohesion -> Cohesion -> Bool
moreCohesion = (<=)
sameCohesion :: Cohesion -> Cohesion -> Bool
sameCohesion = (==)
instance Ord Cohesion where
compare = curry $ \case
(r, r') | r == r' -> EQ
(_, Squash) -> LT
(Squash, _) -> GT
(Flat, _) -> LT
(_, Flat) -> GT
(Continuous,Continuous) -> EQ
instance PartialOrd Cohesion where
comparable = comparableOrd
usableCohesion :: LensCohesion a => a -> Bool
usableCohesion a = getCohesion a `moreCohesion` Continuous
composeCohesion :: Cohesion -> Cohesion -> Cohesion
composeCohesion r r' =
case (r, r') of
(Squash, _) -> Squash
(_, Squash) -> Squash
(Flat, _) -> Flat
(_, Flat) -> Flat
(Continuous, Continuous) -> Continuous
applyCohesion :: LensCohesion a => Cohesion -> a -> a
applyCohesion rel = mapCohesion (rel `composeCohesion`)
inverseComposeCohesion :: Cohesion -> Cohesion -> Cohesion
inverseComposeCohesion r x =
case (r, x) of
(Continuous , x) -> x
(Squash, x) -> Squash
(Flat , Flat) -> Flat
(Flat , _) -> Squash
inverseApplyCohesion :: LensCohesion a => Cohesion -> a -> a
inverseApplyCohesion rel = mapCohesion (rel `inverseComposeCohesion`)
instance Semigroup Cohesion where
(<>) = composeCohesion
instance Monoid Cohesion where
mempty = Continuous
mappend = (<>)
instance POSemigroup Cohesion where
instance POMonoid Cohesion where
instance LeftClosedPOMonoid Cohesion where
inverseCompose = inverseComposeCohesion
addCohesion :: Cohesion -> Cohesion -> Cohesion
addCohesion = min
zeroCohesion :: Cohesion
zeroCohesion = Squash
topCohesion :: Cohesion
topCohesion = Flat
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 Pretty a => Pretty (WithOrigin a) where
prettyPrec p = prettyPrec p . woThing
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
default getOrigin :: LensArgInfo a => a -> Origin
getOrigin = argInfoOrigin . getArgInfo
default mapOrigin :: LensArgInfo a => (Origin -> Origin) -> a -> a
mapOrigin f = mapArgInfo $ \ ai -> ai { argInfoOrigin = f $ argInfoOrigin ai }
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
default getFreeVariables :: LensArgInfo a => a -> FreeVariables
getFreeVariables = argInfoFreeVariables . getArgInfo
default mapFreeVariables :: LensArgInfo a => (FreeVariables -> FreeVariables) -> a -> a
mapFreeVariables f = mapArgInfo $ \ ai -> ai { argInfoFreeVariables = f $ argInfoFreeVariables ai }
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
instance LensCohesion ArgInfo where
getCohesion = getCohesionMod
setCohesion = setCohesionMod
mapCohesion = mapCohesionMod
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
isInsertedHidden :: (LensHiding a, LensOrigin a) => a -> Bool
isInsertedHidden a = getHiding a == Hidden && getOrigin a == Inserted
data Arg e = Arg
{ argInfo :: ArgInfo
, unArg :: e
} deriving (Data, Eq, 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 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
instance LensCohesion (Arg e) where
getCohesion = getCohesionMod
setCohesion = setCohesionMod
mapCohesion = mapCohesionMod
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 Named name a =
Named { nameOf :: Maybe name
, namedThing :: a
}
deriving (Eq, Ord, Show, Data, Functor, Foldable, Traversable)
type Named_ = Named NamedName
type NamedName = WithOrigin (Ranged ArgName)
sameName :: NamedName -> NamedName -> Bool
sameName = (==) `on` (rangedThing . woThing)
unnamed :: a -> Named name a
unnamed = Named Nothing
named :: name -> a -> Named name a
named = Named . Just
userNamed :: Ranged ArgName -> a -> Named_ a
userNamed = Named . Just . WithOrigin UserWritten
class LensNamed name a | a -> name where
lensNamed :: Lens' (Maybe name) a
default lensNamed :: (Decoration f, LensNamed name b, f b ~ a) => Lens' (Maybe name) a
lensNamed = traverseF . lensNamed
instance LensNamed name a => LensNamed name (Arg a) where
instance LensNamed name (Maybe name) where
lensNamed = id
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
bareNameOf :: LensNamed NamedName a => a -> Maybe ArgName
bareNameOf a = rangedThing . woThing <$> getNameOf a
bareNameWithDefault :: LensNamed NamedName a => ArgName -> a -> ArgName
bareNameWithDefault x a = maybe x (rangedThing . woThing) $ getNameOf a
namedSame :: (LensNamed NamedName a, LensNamed NamedName b) => a -> b -> Bool
namedSame a b = case (getNameOf a, getNameOf b) of
(Nothing, Nothing) -> True
(Just x , Just y ) -> sameName x y
_ -> False
fittingNamedArg
:: ( LensNamed NamedName arg, LensHiding arg
, LensNamed NamedName dom, LensHiding dom )
=> arg -> dom -> Maybe Bool
fittingNamedArg arg dom
| not $ sameHiding arg dom = no
| visible arg = yes
| otherwise =
caseMaybe (bareNameOf arg) yes $ \ x ->
caseMaybe (bareNameOf dom) impossible $ \ y ->
return $ x == y
where
yes = return True
no = return False
impossible = Nothing
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
updateNamedArgA :: Applicative f => (a -> f b) -> NamedArg a -> f (NamedArg b)
updateNamedArgA = traverse . traverse
setNamedArg :: NamedArg a -> b -> NamedArg b
setNamedArg a b = (b <$) <$> a
type ArgName = String
argNameToString :: ArgName -> String
argNameToString = id
stringToArgName :: String -> ArgName
stringToArgName = id
appendArgNames :: ArgName -> ArgName -> ArgName
appendArgNames = (++)
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
deriving (Data, Show, Eq, Ord)
instance Pretty Access where
pretty = text . \case
PrivateAccess _ -> "private"
PublicAccess -> "public"
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 Semigroup IsAbstract where
AbstractDef <> _ = AbstractDef
ConcreteDef <> a = a
instance Monoid IsAbstract where
mempty = ConcreteDef
mappend = (<>)
instance KillRange IsAbstract where
killRange = id
class LensIsAbstract a where
lensIsAbstract :: Lens' IsAbstract a
instance LensIsAbstract IsAbstract where
lensIsAbstract = id
class AnyIsAbstract a where
anyIsAbstract :: a -> IsAbstract
default anyIsAbstract :: (Foldable t, AnyIsAbstract b, t b ~ a) => a -> IsAbstract
anyIsAbstract = Fold.foldMap anyIsAbstract
instance AnyIsAbstract IsAbstract where
anyIsAbstract = id
instance AnyIsAbstract a => AnyIsAbstract [a] where
instance AnyIsAbstract a => AnyIsAbstract (Maybe a) where
data IsInstance
= InstanceDef Range
| NotInstanceDef
deriving (Data, Show, Eq, Ord)
instance KillRange IsInstance where
killRange = \case
InstanceDef _ -> InstanceDef noRange
i@NotInstanceDef -> i
instance HasRange IsInstance where
getRange = \case
InstanceDef r -> r
NotInstanceDef -> 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
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, Generic)
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
instance Hashable MetaId
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
type PrecedenceLevel = Double
data FixityLevel
= Unrelated
| Related !PrecedenceLevel
deriving (Eq, Ord, Show, Data)
instance Null FixityLevel where
null Unrelated = True
null Related{} = False
empty = Unrelated
data Associativity = NonAssoc | LeftAssoc | RightAssoc
deriving (Eq, Ord, Show, Data)
data Fixity = Fixity
{ fixityRange :: Range
, fixityLevel :: !FixityLevel
, fixityAssoc :: !Associativity
}
deriving (Data, Show)
noFixity :: Fixity
noFixity = Fixity noRange Unrelated NonAssoc
defaultFixity :: Fixity
defaultFixity = Fixity noRange (Related 20) NonAssoc
instance Eq Fixity where
f1 == f2 = compare f1 f2 == EQ
instance Ord Fixity where
compare = compare `on` (fixityLevel &&& fixityAssoc)
instance Null Fixity where
null = null . fixityLevel
empty = noFixity
instance HasRange Fixity where
getRange = fixityRange
instance KillRange Fixity where
killRange f = f { fixityRange = noRange }
instance NFData Fixity where
rnf (Fixity _ _ _) = ()
data Fixity' = Fixity'
{ theFixity :: !Fixity
, theNotation :: Notation
, theNameRange :: Range
}
deriving (Data, Show)
noFixity' :: Fixity'
noFixity' = Fixity' noFixity noNotation noRange
instance Eq Fixity' where
Fixity' f n _ == Fixity' f' n' _ = f == f' && n == n'
instance Null Fixity' where
null (Fixity' f n _) = null f && null n
empty = noFixity'
instance NFData Fixity' where
rnf (Fixity' _ a _) = rnf a
instance KillRange Fixity' where
killRange (Fixity' f n r) = killRange3 Fixity' f n r
_fixityAssoc :: Lens' Associativity Fixity
_fixityAssoc f r = f (fixityAssoc r) <&> \x -> r { fixityAssoc = x }
_fixityLevel :: Lens' FixityLevel Fixity
_fixityLevel f r = f (fixityLevel r) <&> \x -> r { fixityLevel = x }
class LensFixity a where
lensFixity :: Lens' Fixity a
instance LensFixity Fixity where
lensFixity = id
instance LensFixity Fixity' where
lensFixity f fix' = f (theFixity fix') <&> \ fx -> fix' { theFixity = fx }
class LensFixity' a where
lensFixity' :: Lens' Fixity' a
instance LensFixity' Fixity' where
lensFixity' = id
data ImportDirective' n m = ImportDirective
{ importDirRange :: Range
, using :: Using' n m
, hiding :: [ImportedName' n m]
, impRenaming :: [Renaming' n m]
, publicOpen :: Maybe Range
}
deriving (Data, Eq)
instance Null (ImportDirective' n m) where
null = \case
ImportDirective _ UseEverything [] [] _ -> True
_ -> False
empty = defaultImportDir
defaultImportDir :: ImportDirective' n m
defaultImportDir = ImportDirective noRange UseEverything [] [] Nothing
isDefaultImportDir :: ImportDirective' n m -> Bool
isDefaultImportDir dir = null dir && null (publicOpen dir)
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 = (<>)
instance Null (Using' n m) where
null UseEverything = True
null Using{} = False
empty = mempty
mapUsing :: ([ImportedName' n1 m1] -> [ImportedName' n2 m2]) -> Using' n1 m1 -> Using' n2 m2
mapUsing f = \case
UseEverything -> UseEverything
Using xs -> Using $ f xs
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
, renFixity :: Maybe Fixity
, 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 mf _to) = killRange3 (\ i n mf -> Renaming i n mf noRange) i n mf
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 c _) = rnf a `seq` rnf b `seq` rnf c
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
data PositivityCheck = YesPositivityCheck | NoPositivityCheck
deriving (Eq, Ord, Show, Bounded, Enum, Data)
instance KillRange PositivityCheck where
killRange = id
instance Semigroup PositivityCheck where
NoPositivityCheck <> _ = NoPositivityCheck
_ <> NoPositivityCheck = NoPositivityCheck
_ <> _ = YesPositivityCheck
instance Monoid PositivityCheck where
mempty = YesPositivityCheck
mappend = (<>)
data UniverseCheck = YesUniverseCheck | NoUniverseCheck
deriving (Eq, Ord, Show, Bounded, Enum, Data)
instance KillRange UniverseCheck where
killRange = id
data CoverageCheck = YesCoverageCheck | NoCoverageCheck
deriving (Eq, Ord, Show, Bounded, Enum, Data)
instance KillRange CoverageCheck where
killRange = id
instance Semigroup CoverageCheck where
NoCoverageCheck <> _ = NoCoverageCheck
_ <> NoCoverageCheck = NoCoverageCheck
_ <> _ = YesCoverageCheck
instance Monoid CoverageCheck where
mempty = YesCoverageCheck
mappend = (<>)
data RewriteEqn' qn p e
= Rewrite [(qn, e)]
| Invert qn [(p, e)]
deriving (Data, Eq, Show, Functor, Foldable, Traversable)
instance (NFData qn, NFData p, NFData e) => NFData (RewriteEqn' qn p e) where
rnf = \case
Rewrite es -> rnf es
Invert qn pes -> rnf (qn, pes)
instance (Pretty p, Pretty e) => Pretty (RewriteEqn' qn p e) where
pretty = \case
Rewrite es -> prefixedThings (text "rewrite") (pretty . snd <$> es)
Invert _ pes -> prefixedThings (text "invert") (pes <&> \ (p, e) -> pretty p <+> "<-" <+> pretty e)
instance (HasRange qn, HasRange p, HasRange e) => HasRange (RewriteEqn' qn p e) where
getRange = \case
Rewrite es -> getRange es
Invert qn pes -> getRange (qn, pes)
instance (KillRange qn, KillRange e, KillRange p) => KillRange (RewriteEqn' qn p e) where
killRange = \case
Rewrite es -> killRange1 Rewrite es
Invert qn pes -> killRange2 Invert qn pes
data ExpandedEllipsis
= ExpandedEllipsis
{ ellipsisRange :: Range
, ellipsisWithArgs :: Int
}
| NoEllipsis
deriving (Data, Show, Eq)
instance Null ExpandedEllipsis where
null = (== NoEllipsis)
empty = NoEllipsis
instance KillRange ExpandedEllipsis where
killRange (ExpandedEllipsis _ k) = ExpandedEllipsis noRange k
killRange NoEllipsis = NoEllipsis
instance NFData ExpandedEllipsis where
rnf (ExpandedEllipsis _ a) = rnf a
rnf NoEllipsis = ()
type Notation = [GenPart]
noNotation :: Notation
noNotation = []
data GenPart
= BindHole Range (Ranged Int)
| NormalHole Range (NamedArg (Ranged Int))
| WildHole (Ranged Int)
| IdPart RString
deriving (Data, Show)
instance Eq GenPart where
BindHole _ i == BindHole _ j = i == j
NormalHole _ x == NormalHole _ y = x == y
WildHole i == WildHole j = i == j
IdPart x == IdPart y = x == y
_ == _ = False
instance Ord GenPart where
BindHole _ i `compare` BindHole _ j = i `compare` j
NormalHole _ x `compare` NormalHole _ y = x `compare` y
WildHole i `compare` WildHole j = i `compare` j
IdPart x `compare` IdPart y = x `compare` y
BindHole{} `compare` _ = LT
_ `compare` BindHole{} = GT
NormalHole{} `compare` _ = LT
_ `compare` NormalHole{} = GT
WildHole{} `compare` _ = LT
_ `compare` WildHole{} = GT
instance HasRange GenPart where
getRange p = case p of
IdPart x -> getRange x
BindHole r _ -> r
WildHole i -> getRange i
NormalHole r _ -> r
instance SetRange GenPart where
setRange r p = case p of
IdPart x -> IdPart x
BindHole _ i -> BindHole r i
WildHole i -> WildHole i
NormalHole _ i -> NormalHole r i
instance KillRange GenPart where
killRange p = case p of
IdPart x -> IdPart $ killRange x
BindHole _ i -> BindHole noRange $ killRange i
WildHole i -> WildHole $ killRange i
NormalHole _ x -> NormalHole noRange $ killRange x
instance NFData GenPart where
rnf (BindHole _ a) = rnf a
rnf (NormalHole _ a) = rnf a
rnf (WildHole a) = rnf a
rnf (IdPart a) = rnf a