{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Agda.Syntax.Info where
import Prelude hiding (null)
import Data.Data (Data)
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.Function
import Agda.Utils.Null
data MetaInfo = MetaInfo
{ metaRange :: Range
, metaScope :: ScopeInfo
, metaNumber :: Maybe MetaId
, metaNameSuggestion :: String
}
deriving (Data, Show, Eq)
emptyMetaInfo :: MetaInfo
emptyMetaInfo = MetaInfo
{ metaRange = noRange
, metaScope = emptyScopeInfo
, metaNumber = Nothing
, metaNameSuggestion = ""
}
instance HasRange MetaInfo where
getRange = metaRange
instance KillRange MetaInfo where
killRange m = m { metaRange = noRange }
newtype ExprInfo = ExprRange Range
deriving (Data, Show, Eq, Null)
exprNoRange :: ExprInfo
exprNoRange = ExprRange noRange
instance HasRange ExprInfo where
getRange (ExprRange r) = r
instance KillRange ExprInfo where
killRange (ExprRange r) = exprNoRange
data AppInfo = AppInfo { appRange :: Range
, appOrigin :: Origin
, appParens :: ParenPreference
}
deriving (Data, Show, Eq, Ord)
defaultAppInfo :: Range -> AppInfo
defaultAppInfo r = AppInfo{ appRange = r, appOrigin = Inserted, appParens = PreferParen }
defaultAppInfo_ :: AppInfo
defaultAppInfo_ = defaultAppInfo noRange
instance HasRange AppInfo where
getRange = appRange
instance KillRange AppInfo where
killRange (AppInfo r o p) = AppInfo (killRange r) o p
instance LensOrigin AppInfo where
getOrigin = appOrigin
setOrigin o i = i { appOrigin = o }
data ModuleInfo = ModuleInfo
{ minfoRange :: Range
, minfoAsTo :: Range
, minfoAsName :: Maybe C.Name
, minfoOpenShort :: Maybe OpenShortHand
, minfoDirective :: Maybe ImportDirective
}
deriving (Data, Eq)
deriving instance Show ModuleInfo
instance HasRange ModuleInfo where
getRange = minfoRange
instance SetRange ModuleInfo where
setRange r i = i { minfoRange = r }
instance KillRange ModuleInfo where
killRange m = m { minfoRange = noRange }
newtype LetInfo = LetRange Range
deriving (Data, Show, Eq, Null)
instance HasRange LetInfo where
getRange (LetRange r) = r
instance KillRange LetInfo where
killRange (LetRange r) = LetRange noRange
data DefInfo = DefInfo
{ defFixity :: Fixity'
, defAccess :: Access
, defAbstract :: IsAbstract
, defInstance :: IsInstance
, defMacro :: IsMacro
, defInfo :: DeclInfo
}
deriving (Data, Show, Eq)
mkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo
mkDefInfo x f a ab r = DefInfo f a ab NotInstanceDef NotMacroDef (DeclInfo x r)
mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> IsMacro -> Range -> DefInfo
mkDefInfoInstance x f a ab i m r = DefInfo f a ab i m (DeclInfo x r)
instance HasRange DefInfo where
getRange = getRange . defInfo
instance SetRange DefInfo where
setRange r i = i { defInfo = setRange r (defInfo i) }
instance KillRange DefInfo where
killRange i = i { defInfo = killRange $ defInfo i }
data DeclInfo = DeclInfo
{ declName :: Name
, declRange :: Range
}
deriving (Data, Show, Eq)
instance HasRange DeclInfo where
getRange = declRange
instance SetRange DeclInfo where
setRange r i = i { declRange = r }
instance KillRange DeclInfo where
killRange i = i { declRange = noRange }
data MutualInfo = MutualInfo
{ mutualTermCheck :: TerminationCheck Name
, mutualPositivityCheck :: PositivityCheck
, mutualRange :: Range
}
deriving (Data, Show, Eq)
instance Null MutualInfo where
empty = MutualInfo TerminationCheck True noRange
instance HasRange MutualInfo where
getRange = mutualRange
instance KillRange MutualInfo where
killRange i = i { mutualRange = noRange }
newtype LHSInfo = LHSRange Range
deriving (Data, Show, Eq, Null)
instance HasRange LHSInfo where
getRange (LHSRange r) = r
instance KillRange LHSInfo where
killRange (LHSRange r) = LHSRange noRange
newtype PatInfo
= PatRange Range
deriving (Data, Eq, Null, Show, SetRange, HasRange, KillRange)
patNoRange :: PatInfo
patNoRange = PatRange noRange
data ConPatInfo = ConPatInfo
{ patOrigin :: ConOrigin
, patInfo :: PatInfo
, patLazy :: ConPatLazy
}
deriving (Data, Eq)
instance Show ConPatInfo where
show (ConPatInfo po i l) =
applyWhen (l == ConPatLazy) ("lazy " ++) $
applyWhen (po == ConOSystem) ("implicit " ++) $ show i
instance HasRange ConPatInfo where
getRange = getRange . patInfo
instance KillRange ConPatInfo where
killRange (ConPatInfo b i l) = ConPatInfo b (killRange i) l
instance SetRange ConPatInfo where
setRange r (ConPatInfo b i l) = ConPatInfo b (PatRange r) l
data ConPatLazy
= ConPatLazy
| ConPatEager
deriving (Data, Eq, Ord, Show, Bounded, Enum)