{-| An info object contains additional information about a piece of abstract
    syntax that isn't part of the actual syntax. For instance, it might contain
    the source code position of an expression or the concrete syntax that
    an internal expression originates from.
-}

module Agda.Syntax.Info where

import Prelude hiding (null)

import Control.DeepSeq

import Data.Semigroup (Semigroup)

import GHC.Generics (Generic)

import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Concrete
import Agda.Syntax.Fixity
import Agda.Syntax.Scope.Base (ScopeInfo, emptyScopeInfo)

import Agda.Utils.Functor
import Agda.Utils.Null

{--------------------------------------------------------------------------
    Meta information
 --------------------------------------------------------------------------}

data MetaInfo = MetaInfo
  { MetaInfo -> Range
metaRange          :: Range
  , MetaInfo -> ScopeInfo
metaScope          :: ScopeInfo
  , MetaInfo -> Maybe MetaId
metaNumber         :: Maybe MetaId
  , MetaInfo -> String
metaNameSuggestion :: String
  }
  deriving (Int -> MetaInfo -> ShowS
[MetaInfo] -> ShowS
MetaInfo -> String
(Int -> MetaInfo -> ShowS)
-> (MetaInfo -> String) -> ([MetaInfo] -> ShowS) -> Show MetaInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MetaInfo -> ShowS
showsPrec :: Int -> MetaInfo -> ShowS
$cshow :: MetaInfo -> String
show :: MetaInfo -> String
$cshowList :: [MetaInfo] -> ShowS
showList :: [MetaInfo] -> ShowS
Show, MetaInfo -> MetaInfo -> Bool
(MetaInfo -> MetaInfo -> Bool)
-> (MetaInfo -> MetaInfo -> Bool) -> Eq MetaInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MetaInfo -> MetaInfo -> Bool
== :: MetaInfo -> MetaInfo -> Bool
$c/= :: MetaInfo -> MetaInfo -> Bool
/= :: MetaInfo -> MetaInfo -> Bool
Eq, (forall x. MetaInfo -> Rep MetaInfo x)
-> (forall x. Rep MetaInfo x -> MetaInfo) -> Generic MetaInfo
forall x. Rep MetaInfo x -> MetaInfo
forall x. MetaInfo -> Rep MetaInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MetaInfo -> Rep MetaInfo x
from :: forall x. MetaInfo -> Rep MetaInfo x
$cto :: forall x. Rep MetaInfo x -> MetaInfo
to :: forall x. Rep MetaInfo x -> MetaInfo
Generic)

emptyMetaInfo :: MetaInfo
emptyMetaInfo :: MetaInfo
emptyMetaInfo = MetaInfo
  { metaRange :: Range
metaRange          = Range
forall a. Range' a
noRange
  , metaScope :: ScopeInfo
metaScope          = ScopeInfo
emptyScopeInfo
  , metaNumber :: Maybe MetaId
metaNumber         = Maybe MetaId
forall a. Maybe a
Nothing
  , metaNameSuggestion :: String
metaNameSuggestion = String
""
  }

instance HasRange MetaInfo where
  getRange :: MetaInfo -> Range
getRange = MetaInfo -> Range
metaRange

instance KillRange MetaInfo where
  killRange :: KillRangeT MetaInfo
killRange MetaInfo
m = MetaInfo
m { metaRange :: Range
metaRange = Range
forall a. Range' a
noRange }

instance NFData MetaInfo

{--------------------------------------------------------------------------
    General expression information
 --------------------------------------------------------------------------}

newtype ExprInfo = ExprRange Range
  deriving (Int -> ExprInfo -> ShowS
[ExprInfo] -> ShowS
ExprInfo -> String
(Int -> ExprInfo -> ShowS)
-> (ExprInfo -> String) -> ([ExprInfo] -> ShowS) -> Show ExprInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ExprInfo -> ShowS
showsPrec :: Int -> ExprInfo -> ShowS
$cshow :: ExprInfo -> String
show :: ExprInfo -> String
$cshowList :: [ExprInfo] -> ShowS
showList :: [ExprInfo] -> ShowS
Show, ExprInfo -> ExprInfo -> Bool
(ExprInfo -> ExprInfo -> Bool)
-> (ExprInfo -> ExprInfo -> Bool) -> Eq ExprInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ExprInfo -> ExprInfo -> Bool
== :: ExprInfo -> ExprInfo -> Bool
$c/= :: ExprInfo -> ExprInfo -> Bool
/= :: ExprInfo -> ExprInfo -> Bool
Eq, ExprInfo
ExprInfo -> Bool
ExprInfo -> (ExprInfo -> Bool) -> Null ExprInfo
forall a. a -> (a -> Bool) -> Null a
$cempty :: ExprInfo
empty :: ExprInfo
$cnull :: ExprInfo -> Bool
null :: ExprInfo -> Bool
Null, ExprInfo -> ()
(ExprInfo -> ()) -> NFData ExprInfo
forall a. (a -> ()) -> NFData a
$crnf :: ExprInfo -> ()
rnf :: ExprInfo -> ()
NFData)

exprNoRange :: ExprInfo
exprNoRange :: ExprInfo
exprNoRange = Range -> ExprInfo
ExprRange Range
forall a. Range' a
noRange

instance HasRange ExprInfo where
  getRange :: ExprInfo -> Range
getRange (ExprRange Range
r) = Range
r

instance KillRange ExprInfo where
  killRange :: KillRangeT ExprInfo
killRange (ExprRange Range
r) = ExprInfo
exprNoRange

{--------------------------------------------------------------------------
    Application information
 --------------------------------------------------------------------------}

-- | Information about application
data AppInfo = AppInfo
  { AppInfo -> Range
appRange  :: Range
  , AppInfo -> Origin
appOrigin :: Origin
  , AppInfo -> ParenPreference
appParens :: ParenPreference -- ^ Do we prefer a lambda argument with or without parens?
  }
  deriving (Int -> AppInfo -> ShowS
[AppInfo] -> ShowS
AppInfo -> String
(Int -> AppInfo -> ShowS)
-> (AppInfo -> String) -> ([AppInfo] -> ShowS) -> Show AppInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AppInfo -> ShowS
showsPrec :: Int -> AppInfo -> ShowS
$cshow :: AppInfo -> String
show :: AppInfo -> String
$cshowList :: [AppInfo] -> ShowS
showList :: [AppInfo] -> ShowS
Show, AppInfo -> AppInfo -> Bool
(AppInfo -> AppInfo -> Bool)
-> (AppInfo -> AppInfo -> Bool) -> Eq AppInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AppInfo -> AppInfo -> Bool
== :: AppInfo -> AppInfo -> Bool
$c/= :: AppInfo -> AppInfo -> Bool
/= :: AppInfo -> AppInfo -> Bool
Eq, Eq AppInfo
Eq AppInfo
-> (AppInfo -> AppInfo -> Ordering)
-> (AppInfo -> AppInfo -> Bool)
-> (AppInfo -> AppInfo -> Bool)
-> (AppInfo -> AppInfo -> Bool)
-> (AppInfo -> AppInfo -> Bool)
-> (AppInfo -> AppInfo -> AppInfo)
-> (AppInfo -> AppInfo -> AppInfo)
-> Ord AppInfo
AppInfo -> AppInfo -> Bool
AppInfo -> AppInfo -> Ordering
AppInfo -> AppInfo -> AppInfo
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: AppInfo -> AppInfo -> Ordering
compare :: AppInfo -> AppInfo -> Ordering
$c< :: AppInfo -> AppInfo -> Bool
< :: AppInfo -> AppInfo -> Bool
$c<= :: AppInfo -> AppInfo -> Bool
<= :: AppInfo -> AppInfo -> Bool
$c> :: AppInfo -> AppInfo -> Bool
> :: AppInfo -> AppInfo -> Bool
$c>= :: AppInfo -> AppInfo -> Bool
>= :: AppInfo -> AppInfo -> Bool
$cmax :: AppInfo -> AppInfo -> AppInfo
max :: AppInfo -> AppInfo -> AppInfo
$cmin :: AppInfo -> AppInfo -> AppInfo
min :: AppInfo -> AppInfo -> AppInfo
Ord, (forall x. AppInfo -> Rep AppInfo x)
-> (forall x. Rep AppInfo x -> AppInfo) -> Generic AppInfo
forall x. Rep AppInfo x -> AppInfo
forall x. AppInfo -> Rep AppInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. AppInfo -> Rep AppInfo x
from :: forall x. AppInfo -> Rep AppInfo x
$cto :: forall x. Rep AppInfo x -> AppInfo
to :: forall x. Rep AppInfo x -> AppInfo
Generic)

-- | Default is system inserted and prefer parens.
defaultAppInfo :: Range -> AppInfo
defaultAppInfo :: Range -> AppInfo
defaultAppInfo Range
r = AppInfo{ appRange :: Range
appRange = Range
r, appOrigin :: Origin
appOrigin = Origin
Inserted, appParens :: ParenPreference
appParens = ParenPreference
PreferParen }

-- | `AppInfo` with no range information.
defaultAppInfo_ :: AppInfo
defaultAppInfo_ :: AppInfo
defaultAppInfo_ = Range -> AppInfo
defaultAppInfo Range
forall a. Range' a
noRange

instance HasRange AppInfo where
  getRange :: AppInfo -> Range
getRange = AppInfo -> Range
appRange

instance KillRange AppInfo where
  killRange :: AppInfo -> AppInfo
killRange (AppInfo Range
r Origin
o ParenPreference
p) = Range -> Origin -> ParenPreference -> AppInfo
AppInfo (KillRangeT Range
forall a. KillRange a => KillRangeT a
killRange Range
r) Origin
o ParenPreference
p

instance LensOrigin AppInfo where
  getOrigin :: AppInfo -> Origin
getOrigin = AppInfo -> Origin
appOrigin
  mapOrigin :: (Origin -> Origin) -> AppInfo -> AppInfo
mapOrigin Origin -> Origin
f AppInfo
i = AppInfo
i { appOrigin :: Origin
appOrigin = Origin -> Origin
f (AppInfo -> Origin
appOrigin AppInfo
i) }

instance NFData AppInfo

{--------------------------------------------------------------------------
    Module information
 --------------------------------------------------------------------------}

data ModuleInfo = ModuleInfo
  { ModuleInfo -> Range
minfoRange    :: Range
  , ModuleInfo -> Range
minfoAsTo     :: Range
    -- ^ The range of the \"as\" and \"to\" keywords,
    -- if any. Retained for highlighting purposes.
  , ModuleInfo -> Maybe Name
minfoAsName   :: Maybe C.Name
    -- ^ The \"as\" module name, if any. Retained for highlighting purposes.
  , ModuleInfo -> Maybe OpenShortHand
minfoOpenShort :: Maybe OpenShortHand
  , ModuleInfo -> Maybe ImportDirective
minfoDirective :: Maybe ImportDirective
    -- ^ Retained for @abstractToConcrete@ of 'ModuleMacro'.
  }
  deriving (ModuleInfo -> ModuleInfo -> Bool
(ModuleInfo -> ModuleInfo -> Bool)
-> (ModuleInfo -> ModuleInfo -> Bool) -> Eq ModuleInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ModuleInfo -> ModuleInfo -> Bool
== :: ModuleInfo -> ModuleInfo -> Bool
$c/= :: ModuleInfo -> ModuleInfo -> Bool
/= :: ModuleInfo -> ModuleInfo -> Bool
Eq, Int -> ModuleInfo -> ShowS
[ModuleInfo] -> ShowS
ModuleInfo -> String
(Int -> ModuleInfo -> ShowS)
-> (ModuleInfo -> String)
-> ([ModuleInfo] -> ShowS)
-> Show ModuleInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ModuleInfo -> ShowS
showsPrec :: Int -> ModuleInfo -> ShowS
$cshow :: ModuleInfo -> String
show :: ModuleInfo -> String
$cshowList :: [ModuleInfo] -> ShowS
showList :: [ModuleInfo] -> ShowS
Show, (forall x. ModuleInfo -> Rep ModuleInfo x)
-> (forall x. Rep ModuleInfo x -> ModuleInfo) -> Generic ModuleInfo
forall x. Rep ModuleInfo x -> ModuleInfo
forall x. ModuleInfo -> Rep ModuleInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ModuleInfo -> Rep ModuleInfo x
from :: forall x. ModuleInfo -> Rep ModuleInfo x
$cto :: forall x. Rep ModuleInfo x -> ModuleInfo
to :: forall x. Rep ModuleInfo x -> ModuleInfo
Generic)

instance HasRange ModuleInfo where
  getRange :: ModuleInfo -> Range
getRange = ModuleInfo -> Range
minfoRange

instance SetRange ModuleInfo where
  setRange :: Range -> ModuleInfo -> ModuleInfo
setRange Range
r ModuleInfo
i = ModuleInfo
i { minfoRange :: Range
minfoRange = Range
r }

instance KillRange ModuleInfo where
  killRange :: ModuleInfo -> ModuleInfo
killRange ModuleInfo
m = ModuleInfo
m { minfoRange :: Range
minfoRange = Range
forall a. Range' a
noRange }

instance NFData ModuleInfo

---------------------------------------------------------------------------
-- Let info
---------------------------------------------------------------------------

newtype LetInfo = LetRange Range
  deriving (Int -> LetInfo -> ShowS
[LetInfo] -> ShowS
LetInfo -> String
(Int -> LetInfo -> ShowS)
-> (LetInfo -> String) -> ([LetInfo] -> ShowS) -> Show LetInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LetInfo -> ShowS
showsPrec :: Int -> LetInfo -> ShowS
$cshow :: LetInfo -> String
show :: LetInfo -> String
$cshowList :: [LetInfo] -> ShowS
showList :: [LetInfo] -> ShowS
Show, LetInfo -> LetInfo -> Bool
(LetInfo -> LetInfo -> Bool)
-> (LetInfo -> LetInfo -> Bool) -> Eq LetInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LetInfo -> LetInfo -> Bool
== :: LetInfo -> LetInfo -> Bool
$c/= :: LetInfo -> LetInfo -> Bool
/= :: LetInfo -> LetInfo -> Bool
Eq, LetInfo
LetInfo -> Bool
LetInfo -> (LetInfo -> Bool) -> Null LetInfo
forall a. a -> (a -> Bool) -> Null a
$cempty :: LetInfo
empty :: LetInfo
$cnull :: LetInfo -> Bool
null :: LetInfo -> Bool
Null, LetInfo -> ()
(LetInfo -> ()) -> NFData LetInfo
forall a. (a -> ()) -> NFData a
$crnf :: LetInfo -> ()
rnf :: LetInfo -> ()
NFData)

instance HasRange LetInfo where
  getRange :: LetInfo -> Range
getRange (LetRange Range
r)   = Range
r

instance KillRange LetInfo where
  killRange :: KillRangeT LetInfo
killRange (LetRange Range
r) = Range -> LetInfo
LetRange Range
forall a. Range' a
noRange

{--------------------------------------------------------------------------
    Definition information (declarations that actually define something)
 --------------------------------------------------------------------------}

data DefInfo' t = DefInfo
  { forall t. DefInfo' t -> Fixity'
defFixity   :: Fixity'
  , forall t. DefInfo' t -> Access
defAccess   :: Access
  , forall t. DefInfo' t -> IsAbstract
defAbstract :: IsAbstract
  , forall t. DefInfo' t -> IsInstance
defInstance :: IsInstance
  , forall t. DefInfo' t -> IsMacro
defMacro    :: IsMacro
  , forall t. DefInfo' t -> DeclInfo
defInfo     :: DeclInfo
  , forall t. DefInfo' t -> Maybe t
defTactic   :: Maybe t
  }
  deriving (Int -> DefInfo' t -> ShowS
[DefInfo' t] -> ShowS
DefInfo' t -> String
(Int -> DefInfo' t -> ShowS)
-> (DefInfo' t -> String)
-> ([DefInfo' t] -> ShowS)
-> Show (DefInfo' t)
forall t. Show t => Int -> DefInfo' t -> ShowS
forall t. Show t => [DefInfo' t] -> ShowS
forall t. Show t => DefInfo' t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall t. Show t => Int -> DefInfo' t -> ShowS
showsPrec :: Int -> DefInfo' t -> ShowS
$cshow :: forall t. Show t => DefInfo' t -> String
show :: DefInfo' t -> String
$cshowList :: forall t. Show t => [DefInfo' t] -> ShowS
showList :: [DefInfo' t] -> ShowS
Show, DefInfo' t -> DefInfo' t -> Bool
(DefInfo' t -> DefInfo' t -> Bool)
-> (DefInfo' t -> DefInfo' t -> Bool) -> Eq (DefInfo' t)
forall t. Eq t => DefInfo' t -> DefInfo' t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall t. Eq t => DefInfo' t -> DefInfo' t -> Bool
== :: DefInfo' t -> DefInfo' t -> Bool
$c/= :: forall t. Eq t => DefInfo' t -> DefInfo' t -> Bool
/= :: DefInfo' t -> DefInfo' t -> Bool
Eq, (forall x. DefInfo' t -> Rep (DefInfo' t) x)
-> (forall x. Rep (DefInfo' t) x -> DefInfo' t)
-> Generic (DefInfo' t)
forall x. Rep (DefInfo' t) x -> DefInfo' t
forall x. DefInfo' t -> Rep (DefInfo' t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (DefInfo' t) x -> DefInfo' t
forall t x. DefInfo' t -> Rep (DefInfo' t) x
$cfrom :: forall t x. DefInfo' t -> Rep (DefInfo' t) x
from :: forall x. DefInfo' t -> Rep (DefInfo' t) x
$cto :: forall t x. Rep (DefInfo' t) x -> DefInfo' t
to :: forall x. Rep (DefInfo' t) x -> DefInfo' t
Generic)

mkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfo :: forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfo Name
x Fixity'
f Access
a IsAbstract
ab Range
r = Name
-> Fixity'
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> Range
-> DefInfo' t
forall t.
Name
-> Fixity'
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> Range
-> DefInfo' t
mkDefInfoInstance Name
x Fixity'
f Access
a IsAbstract
ab IsInstance
NotInstanceDef IsMacro
NotMacroDef Range
r

-- | Same as @mkDefInfo@ but where we can also give the @IsInstance@
mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> IsMacro -> Range -> DefInfo' t
mkDefInfoInstance :: forall t.
Name
-> Fixity'
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> Range
-> DefInfo' t
mkDefInfoInstance Name
x Fixity'
f Access
a IsAbstract
ab IsInstance
i IsMacro
m Range
r = Fixity'
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> DeclInfo
-> Maybe t
-> DefInfo' t
forall t.
Fixity'
-> Access
-> IsAbstract
-> IsInstance
-> IsMacro
-> DeclInfo
-> Maybe t
-> DefInfo' t
DefInfo Fixity'
f Access
a IsAbstract
ab IsInstance
i IsMacro
m (Name -> Range -> DeclInfo
DeclInfo Name
x Range
r) Maybe t
forall a. Maybe a
Nothing

instance HasRange (DefInfo' t) where
  getRange :: DefInfo' t -> Range
getRange = DeclInfo -> Range
forall a. HasRange a => a -> Range
getRange (DeclInfo -> Range)
-> (DefInfo' t -> DeclInfo) -> DefInfo' t -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefInfo' t -> DeclInfo
forall t. DefInfo' t -> DeclInfo
defInfo

instance SetRange (DefInfo' t) where
  setRange :: Range -> DefInfo' t -> DefInfo' t
setRange Range
r DefInfo' t
i = DefInfo' t
i { defInfo :: DeclInfo
defInfo = Range -> DeclInfo -> DeclInfo
forall a. SetRange a => Range -> a -> a
setRange Range
r (DefInfo' t -> DeclInfo
forall t. DefInfo' t -> DeclInfo
defInfo DefInfo' t
i) }

instance KillRange t => KillRange (DefInfo' t) where
  killRange :: KillRangeT (DefInfo' t)
killRange DefInfo' t
i = DefInfo' t
i { defInfo :: DeclInfo
defInfo   = DeclInfo -> DeclInfo
forall a. KillRange a => KillRangeT a
killRange (DeclInfo -> DeclInfo) -> DeclInfo -> DeclInfo
forall a b. (a -> b) -> a -> b
$ DefInfo' t -> DeclInfo
forall t. DefInfo' t -> DeclInfo
defInfo DefInfo' t
i,
                    defTactic :: Maybe t
defTactic = KillRangeT (Maybe t)
forall a. KillRange a => KillRangeT a
killRange KillRangeT (Maybe t) -> KillRangeT (Maybe t)
forall a b. (a -> b) -> a -> b
$ DefInfo' t -> Maybe t
forall t. DefInfo' t -> Maybe t
defTactic DefInfo' t
i }

instance LensIsAbstract (DefInfo' t) where
  lensIsAbstract :: Lens' IsAbstract (DefInfo' t)
lensIsAbstract IsAbstract -> f IsAbstract
f DefInfo' t
i = (IsAbstract -> f IsAbstract
f (IsAbstract -> f IsAbstract) -> IsAbstract -> f IsAbstract
forall a b. (a -> b) -> a -> b
$! DefInfo' t -> IsAbstract
forall t. DefInfo' t -> IsAbstract
defAbstract DefInfo' t
i) f IsAbstract -> (IsAbstract -> DefInfo' t) -> f (DefInfo' t)
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ IsAbstract
a -> DefInfo' t
i { defAbstract :: IsAbstract
defAbstract = IsAbstract
a }

instance AnyIsAbstract (DefInfo' t) where
  anyIsAbstract :: DefInfo' t -> IsAbstract
anyIsAbstract = DefInfo' t -> IsAbstract
forall t. DefInfo' t -> IsAbstract
defAbstract

instance NFData t => NFData (DefInfo' t)

{--------------------------------------------------------------------------
    General declaration information
 --------------------------------------------------------------------------}

data DeclInfo = DeclInfo
  { DeclInfo -> Name
declName  :: Name
  , DeclInfo -> Range
declRange :: Range
  }
  deriving (Int -> DeclInfo -> ShowS
[DeclInfo] -> ShowS
DeclInfo -> String
(Int -> DeclInfo -> ShowS)
-> (DeclInfo -> String) -> ([DeclInfo] -> ShowS) -> Show DeclInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DeclInfo -> ShowS
showsPrec :: Int -> DeclInfo -> ShowS
$cshow :: DeclInfo -> String
show :: DeclInfo -> String
$cshowList :: [DeclInfo] -> ShowS
showList :: [DeclInfo] -> ShowS
Show, DeclInfo -> DeclInfo -> Bool
(DeclInfo -> DeclInfo -> Bool)
-> (DeclInfo -> DeclInfo -> Bool) -> Eq DeclInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DeclInfo -> DeclInfo -> Bool
== :: DeclInfo -> DeclInfo -> Bool
$c/= :: DeclInfo -> DeclInfo -> Bool
/= :: DeclInfo -> DeclInfo -> Bool
Eq, (forall x. DeclInfo -> Rep DeclInfo x)
-> (forall x. Rep DeclInfo x -> DeclInfo) -> Generic DeclInfo
forall x. Rep DeclInfo x -> DeclInfo
forall x. DeclInfo -> Rep DeclInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DeclInfo -> Rep DeclInfo x
from :: forall x. DeclInfo -> Rep DeclInfo x
$cto :: forall x. Rep DeclInfo x -> DeclInfo
to :: forall x. Rep DeclInfo x -> DeclInfo
Generic)

instance HasRange DeclInfo where
  getRange :: DeclInfo -> Range
getRange = DeclInfo -> Range
declRange

instance SetRange DeclInfo where
  setRange :: Range -> DeclInfo -> DeclInfo
setRange Range
r DeclInfo
i = DeclInfo
i { declRange :: Range
declRange = Range
r }

instance KillRange DeclInfo where
  killRange :: DeclInfo -> DeclInfo
killRange DeclInfo
i = DeclInfo
i { declRange :: Range
declRange = Range
forall a. Range' a
noRange }

instance NFData DeclInfo

{--------------------------------------------------------------------------
    Mutual block information
 --------------------------------------------------------------------------}

data MutualInfo = MutualInfo
  { MutualInfo -> TerminationCheck Name
mutualTerminationCheck :: TerminationCheck Name
  , MutualInfo -> CoverageCheck
mutualCoverageCheck    :: CoverageCheck
  , MutualInfo -> PositivityCheck
mutualPositivityCheck  :: PositivityCheck
  , MutualInfo -> Range
mutualRange            :: Range
  }
  deriving (Int -> MutualInfo -> ShowS
[MutualInfo] -> ShowS
MutualInfo -> String
(Int -> MutualInfo -> ShowS)
-> (MutualInfo -> String)
-> ([MutualInfo] -> ShowS)
-> Show MutualInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MutualInfo -> ShowS
showsPrec :: Int -> MutualInfo -> ShowS
$cshow :: MutualInfo -> String
show :: MutualInfo -> String
$cshowList :: [MutualInfo] -> ShowS
showList :: [MutualInfo] -> ShowS
Show, MutualInfo -> MutualInfo -> Bool
(MutualInfo -> MutualInfo -> Bool)
-> (MutualInfo -> MutualInfo -> Bool) -> Eq MutualInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MutualInfo -> MutualInfo -> Bool
== :: MutualInfo -> MutualInfo -> Bool
$c/= :: MutualInfo -> MutualInfo -> Bool
/= :: MutualInfo -> MutualInfo -> Bool
Eq, (forall x. MutualInfo -> Rep MutualInfo x)
-> (forall x. Rep MutualInfo x -> MutualInfo) -> Generic MutualInfo
forall x. Rep MutualInfo x -> MutualInfo
forall x. MutualInfo -> Rep MutualInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MutualInfo -> Rep MutualInfo x
from :: forall x. MutualInfo -> Rep MutualInfo x
$cto :: forall x. Rep MutualInfo x -> MutualInfo
to :: forall x. Rep MutualInfo x -> MutualInfo
Generic)

-- | Default value for 'MutualInfo'.
instance Null MutualInfo where
  empty :: MutualInfo
empty = TerminationCheck Name
-> CoverageCheck -> PositivityCheck -> Range -> MutualInfo
MutualInfo TerminationCheck Name
forall m. TerminationCheck m
TerminationCheck CoverageCheck
YesCoverageCheck PositivityCheck
YesPositivityCheck Range
forall a. Range' a
noRange

instance HasRange MutualInfo where
  getRange :: MutualInfo -> Range
getRange = MutualInfo -> Range
mutualRange

instance KillRange MutualInfo where
  killRange :: KillRangeT MutualInfo
killRange MutualInfo
i = MutualInfo
i { mutualRange :: Range
mutualRange = Range
forall a. Range' a
noRange }

instance NFData MutualInfo

{--------------------------------------------------------------------------
    Left hand side information
 --------------------------------------------------------------------------}

data LHSInfo = LHSInfo
  { LHSInfo -> Range
lhsRange    :: Range
  , LHSInfo -> ExpandedEllipsis
lhsEllipsis :: ExpandedEllipsis
  } deriving (Int -> LHSInfo -> ShowS
[LHSInfo] -> ShowS
LHSInfo -> String
(Int -> LHSInfo -> ShowS)
-> (LHSInfo -> String) -> ([LHSInfo] -> ShowS) -> Show LHSInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LHSInfo -> ShowS
showsPrec :: Int -> LHSInfo -> ShowS
$cshow :: LHSInfo -> String
show :: LHSInfo -> String
$cshowList :: [LHSInfo] -> ShowS
showList :: [LHSInfo] -> ShowS
Show, LHSInfo -> LHSInfo -> Bool
(LHSInfo -> LHSInfo -> Bool)
-> (LHSInfo -> LHSInfo -> Bool) -> Eq LHSInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LHSInfo -> LHSInfo -> Bool
== :: LHSInfo -> LHSInfo -> Bool
$c/= :: LHSInfo -> LHSInfo -> Bool
/= :: LHSInfo -> LHSInfo -> Bool
Eq, (forall x. LHSInfo -> Rep LHSInfo x)
-> (forall x. Rep LHSInfo x -> LHSInfo) -> Generic LHSInfo
forall x. Rep LHSInfo x -> LHSInfo
forall x. LHSInfo -> Rep LHSInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LHSInfo -> Rep LHSInfo x
from :: forall x. LHSInfo -> Rep LHSInfo x
$cto :: forall x. Rep LHSInfo x -> LHSInfo
to :: forall x. Rep LHSInfo x -> LHSInfo
Generic)

instance HasRange LHSInfo where
  getRange :: LHSInfo -> Range
getRange (LHSInfo Range
r ExpandedEllipsis
_) = Range
r

instance KillRange LHSInfo where
  killRange :: KillRangeT LHSInfo
killRange (LHSInfo Range
r ExpandedEllipsis
ell) = Range -> ExpandedEllipsis -> LHSInfo
LHSInfo Range
forall a. Range' a
noRange ExpandedEllipsis
ell

instance Null LHSInfo where
  null :: LHSInfo -> Bool
null LHSInfo
i = Range -> Bool
forall a. Null a => a -> Bool
null (LHSInfo -> Range
lhsRange LHSInfo
i) Bool -> Bool -> Bool
&& ExpandedEllipsis -> Bool
forall a. Null a => a -> Bool
null (LHSInfo -> ExpandedEllipsis
lhsEllipsis LHSInfo
i)
  empty :: LHSInfo
empty  = Range -> ExpandedEllipsis -> LHSInfo
LHSInfo Range
forall a. Null a => a
empty ExpandedEllipsis
forall a. Null a => a
empty

instance NFData LHSInfo

{--------------------------------------------------------------------------
    Pattern information
 --------------------------------------------------------------------------}

-- | For a general pattern we remember the source code position.
newtype PatInfo
  = PatRange Range
  deriving (PatInfo -> PatInfo -> Bool
(PatInfo -> PatInfo -> Bool)
-> (PatInfo -> PatInfo -> Bool) -> Eq PatInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PatInfo -> PatInfo -> Bool
== :: PatInfo -> PatInfo -> Bool
$c/= :: PatInfo -> PatInfo -> Bool
/= :: PatInfo -> PatInfo -> Bool
Eq, PatInfo
PatInfo -> Bool
PatInfo -> (PatInfo -> Bool) -> Null PatInfo
forall a. a -> (a -> Bool) -> Null a
$cempty :: PatInfo
empty :: PatInfo
$cnull :: PatInfo -> Bool
null :: PatInfo -> Bool
Null, NonEmpty PatInfo -> PatInfo
PatInfo -> PatInfo -> PatInfo
(PatInfo -> PatInfo -> PatInfo)
-> (NonEmpty PatInfo -> PatInfo)
-> (forall b. Integral b => b -> PatInfo -> PatInfo)
-> Semigroup PatInfo
forall b. Integral b => b -> PatInfo -> PatInfo
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: PatInfo -> PatInfo -> PatInfo
<> :: PatInfo -> PatInfo -> PatInfo
$csconcat :: NonEmpty PatInfo -> PatInfo
sconcat :: NonEmpty PatInfo -> PatInfo
$cstimes :: forall b. Integral b => b -> PatInfo -> PatInfo
stimes :: forall b. Integral b => b -> PatInfo -> PatInfo
Semigroup, Semigroup PatInfo
PatInfo
Semigroup PatInfo
-> PatInfo
-> (PatInfo -> PatInfo -> PatInfo)
-> ([PatInfo] -> PatInfo)
-> Monoid PatInfo
[PatInfo] -> PatInfo
PatInfo -> PatInfo -> PatInfo
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: PatInfo
mempty :: PatInfo
$cmappend :: PatInfo -> PatInfo -> PatInfo
mappend :: PatInfo -> PatInfo -> PatInfo
$cmconcat :: [PatInfo] -> PatInfo
mconcat :: [PatInfo] -> PatInfo
Monoid, Int -> PatInfo -> ShowS
[PatInfo] -> ShowS
PatInfo -> String
(Int -> PatInfo -> ShowS)
-> (PatInfo -> String) -> ([PatInfo] -> ShowS) -> Show PatInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PatInfo -> ShowS
showsPrec :: Int -> PatInfo -> ShowS
$cshow :: PatInfo -> String
show :: PatInfo -> String
$cshowList :: [PatInfo] -> ShowS
showList :: [PatInfo] -> ShowS
Show, HasRange PatInfo
HasRange PatInfo
-> (Range -> PatInfo -> PatInfo) -> SetRange PatInfo
Range -> PatInfo -> PatInfo
forall a. HasRange a -> (Range -> a -> a) -> SetRange a
$csetRange :: Range -> PatInfo -> PatInfo
setRange :: Range -> PatInfo -> PatInfo
SetRange, PatInfo -> Range
(PatInfo -> Range) -> HasRange PatInfo
forall a. (a -> Range) -> HasRange a
$cgetRange :: PatInfo -> Range
getRange :: PatInfo -> Range
HasRange,
            PatInfo -> PatInfo
(PatInfo -> PatInfo) -> KillRange PatInfo
forall a. KillRangeT a -> KillRange a
$ckillRange :: PatInfo -> PatInfo
killRange :: PatInfo -> PatInfo
KillRange, PatInfo -> ()
(PatInfo -> ()) -> NFData PatInfo
forall a. (a -> ()) -> NFData a
$crnf :: PatInfo -> ()
rnf :: PatInfo -> ()
NFData)

-- | Empty range for patterns.
patNoRange :: PatInfo
patNoRange :: PatInfo
patNoRange = Range -> PatInfo
PatRange Range
forall a. Range' a
noRange

-- | Constructor pattern info.
data ConPatInfo = ConPatInfo
  { ConPatInfo -> ConOrigin
conPatOrigin   :: ConOrigin
    -- ^ Does this pattern come form the eta-expansion of an implicit pattern?
    ---  Or from a user written constructor or record pattern?
  , ConPatInfo -> PatInfo
conPatInfo     :: PatInfo
  , ConPatInfo -> ConPatLazy
conPatLazy     :: ConPatLazy
  }
  deriving (ConPatInfo -> ConPatInfo -> Bool
(ConPatInfo -> ConPatInfo -> Bool)
-> (ConPatInfo -> ConPatInfo -> Bool) -> Eq ConPatInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ConPatInfo -> ConPatInfo -> Bool
== :: ConPatInfo -> ConPatInfo -> Bool
$c/= :: ConPatInfo -> ConPatInfo -> Bool
/= :: ConPatInfo -> ConPatInfo -> Bool
Eq, Int -> ConPatInfo -> ShowS
[ConPatInfo] -> ShowS
ConPatInfo -> String
(Int -> ConPatInfo -> ShowS)
-> (ConPatInfo -> String)
-> ([ConPatInfo] -> ShowS)
-> Show ConPatInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ConPatInfo -> ShowS
showsPrec :: Int -> ConPatInfo -> ShowS
$cshow :: ConPatInfo -> String
show :: ConPatInfo -> String
$cshowList :: [ConPatInfo] -> ShowS
showList :: [ConPatInfo] -> ShowS
Show, (forall x. ConPatInfo -> Rep ConPatInfo x)
-> (forall x. Rep ConPatInfo x -> ConPatInfo) -> Generic ConPatInfo
forall x. Rep ConPatInfo x -> ConPatInfo
forall x. ConPatInfo -> Rep ConPatInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ConPatInfo -> Rep ConPatInfo x
from :: forall x. ConPatInfo -> Rep ConPatInfo x
$cto :: forall x. Rep ConPatInfo x -> ConPatInfo
to :: forall x. Rep ConPatInfo x -> ConPatInfo
Generic)

instance HasRange ConPatInfo where
  getRange :: ConPatInfo -> Range
getRange = PatInfo -> Range
forall a. HasRange a => a -> Range
getRange (PatInfo -> Range)
-> (ConPatInfo -> PatInfo) -> ConPatInfo -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConPatInfo -> PatInfo
conPatInfo

instance KillRange ConPatInfo where
  killRange :: KillRangeT ConPatInfo
killRange (ConPatInfo ConOrigin
b PatInfo
i ConPatLazy
l) = ConOrigin -> PatInfo -> ConPatLazy -> ConPatInfo
ConPatInfo ConOrigin
b (PatInfo -> PatInfo
forall a. KillRange a => KillRangeT a
killRange PatInfo
i) ConPatLazy
l

instance SetRange ConPatInfo where
  setRange :: Range -> KillRangeT ConPatInfo
setRange Range
r (ConPatInfo ConOrigin
b PatInfo
i ConPatLazy
l) = ConOrigin -> PatInfo -> ConPatLazy -> ConPatInfo
ConPatInfo ConOrigin
b (Range -> PatInfo
PatRange Range
r) ConPatLazy
l

instance NFData ConPatInfo

-- | Has the constructor pattern a dotted (forced) constructor?
data ConPatLazy
  = ConPatLazy   -- ^ Dotted constructor.
  | ConPatEager  -- ^ Ordinary constructor.
  deriving (ConPatLazy -> ConPatLazy -> Bool
(ConPatLazy -> ConPatLazy -> Bool)
-> (ConPatLazy -> ConPatLazy -> Bool) -> Eq ConPatLazy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ConPatLazy -> ConPatLazy -> Bool
== :: ConPatLazy -> ConPatLazy -> Bool
$c/= :: ConPatLazy -> ConPatLazy -> Bool
/= :: ConPatLazy -> ConPatLazy -> Bool
Eq, Eq ConPatLazy
Eq ConPatLazy
-> (ConPatLazy -> ConPatLazy -> Ordering)
-> (ConPatLazy -> ConPatLazy -> Bool)
-> (ConPatLazy -> ConPatLazy -> Bool)
-> (ConPatLazy -> ConPatLazy -> Bool)
-> (ConPatLazy -> ConPatLazy -> Bool)
-> (ConPatLazy -> ConPatLazy -> ConPatLazy)
-> (ConPatLazy -> ConPatLazy -> ConPatLazy)
-> Ord ConPatLazy
ConPatLazy -> ConPatLazy -> Bool
ConPatLazy -> ConPatLazy -> Ordering
ConPatLazy -> ConPatLazy -> ConPatLazy
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ConPatLazy -> ConPatLazy -> Ordering
compare :: ConPatLazy -> ConPatLazy -> Ordering
$c< :: ConPatLazy -> ConPatLazy -> Bool
< :: ConPatLazy -> ConPatLazy -> Bool
$c<= :: ConPatLazy -> ConPatLazy -> Bool
<= :: ConPatLazy -> ConPatLazy -> Bool
$c> :: ConPatLazy -> ConPatLazy -> Bool
> :: ConPatLazy -> ConPatLazy -> Bool
$c>= :: ConPatLazy -> ConPatLazy -> Bool
>= :: ConPatLazy -> ConPatLazy -> Bool
$cmax :: ConPatLazy -> ConPatLazy -> ConPatLazy
max :: ConPatLazy -> ConPatLazy -> ConPatLazy
$cmin :: ConPatLazy -> ConPatLazy -> ConPatLazy
min :: ConPatLazy -> ConPatLazy -> ConPatLazy
Ord, Int -> ConPatLazy -> ShowS
[ConPatLazy] -> ShowS
ConPatLazy -> String
(Int -> ConPatLazy -> ShowS)
-> (ConPatLazy -> String)
-> ([ConPatLazy] -> ShowS)
-> Show ConPatLazy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ConPatLazy -> ShowS
showsPrec :: Int -> ConPatLazy -> ShowS
$cshow :: ConPatLazy -> String
show :: ConPatLazy -> String
$cshowList :: [ConPatLazy] -> ShowS
showList :: [ConPatLazy] -> ShowS
Show, ConPatLazy
ConPatLazy -> ConPatLazy -> Bounded ConPatLazy
forall a. a -> a -> Bounded a
$cminBound :: ConPatLazy
minBound :: ConPatLazy
$cmaxBound :: ConPatLazy
maxBound :: ConPatLazy
Bounded, Int -> ConPatLazy
ConPatLazy -> Int
ConPatLazy -> [ConPatLazy]
ConPatLazy -> ConPatLazy
ConPatLazy -> ConPatLazy -> [ConPatLazy]
ConPatLazy -> ConPatLazy -> ConPatLazy -> [ConPatLazy]
(ConPatLazy -> ConPatLazy)
-> (ConPatLazy -> ConPatLazy)
-> (Int -> ConPatLazy)
-> (ConPatLazy -> Int)
-> (ConPatLazy -> [ConPatLazy])
-> (ConPatLazy -> ConPatLazy -> [ConPatLazy])
-> (ConPatLazy -> ConPatLazy -> [ConPatLazy])
-> (ConPatLazy -> ConPatLazy -> ConPatLazy -> [ConPatLazy])
-> Enum ConPatLazy
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: ConPatLazy -> ConPatLazy
succ :: ConPatLazy -> ConPatLazy
$cpred :: ConPatLazy -> ConPatLazy
pred :: ConPatLazy -> ConPatLazy
$ctoEnum :: Int -> ConPatLazy
toEnum :: Int -> ConPatLazy
$cfromEnum :: ConPatLazy -> Int
fromEnum :: ConPatLazy -> Int
$cenumFrom :: ConPatLazy -> [ConPatLazy]
enumFrom :: ConPatLazy -> [ConPatLazy]
$cenumFromThen :: ConPatLazy -> ConPatLazy -> [ConPatLazy]
enumFromThen :: ConPatLazy -> ConPatLazy -> [ConPatLazy]
$cenumFromTo :: ConPatLazy -> ConPatLazy -> [ConPatLazy]
enumFromTo :: ConPatLazy -> ConPatLazy -> [ConPatLazy]
$cenumFromThenTo :: ConPatLazy -> ConPatLazy -> ConPatLazy -> [ConPatLazy]
enumFromThenTo :: ConPatLazy -> ConPatLazy -> ConPatLazy -> [ConPatLazy]
Enum, (forall x. ConPatLazy -> Rep ConPatLazy x)
-> (forall x. Rep ConPatLazy x -> ConPatLazy) -> Generic ConPatLazy
forall x. Rep ConPatLazy x -> ConPatLazy
forall x. ConPatLazy -> Rep ConPatLazy x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ConPatLazy -> Rep ConPatLazy x
from :: forall x. ConPatLazy -> Rep ConPatLazy x
$cto :: forall x. Rep ConPatLazy x -> ConPatLazy
to :: forall x. Rep ConPatLazy x -> ConPatLazy
Generic)

instance NFData ConPatLazy