module Agda.Syntax.Info where
import Data.Generics (Typeable, Data)
import Text.Show.Functions
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)
data Info = Nope
data MetaInfo =
MetaInfo { metaRange :: Range
, metaScope :: ScopeInfo
, metaNumber :: Maybe Nat
}
deriving (Typeable, Data, Show)
instance HasRange MetaInfo where
getRange = metaRange
instance KillRange MetaInfo where
killRange m = m { metaRange = killRange $ metaRange m }
data ExprInfo
= ExprRange Range
| ExprSource Range (Precedence -> Expr)
deriving (Typeable, Data, Show)
instance HasRange ExprInfo where
getRange (ExprRange r ) = r
getRange (ExprSource r _) = r
instance KillRange ExprInfo where
killRange (ExprRange r) = ExprRange (killRange r)
killRange (ExprSource r f) = ExprSource (killRange r) f
data ModuleInfo =
ModuleInfo { minfoRange :: Range
, minfoAsTo :: Range
, minfoAsName :: Maybe C.Name
, minfoOpenShort :: Maybe OpenShortHand
, minfoDirective :: Maybe ImportDirective
}
deriving (Typeable, Data)
deriving instance (Show OpenShortHand, Show ImportDirective) => Show ModuleInfo
instance HasRange ModuleInfo where
getRange = minfoRange
instance KillRange ModuleInfo where
killRange m = m { minfoRange = killRange $ minfoRange m }
newtype LetInfo = LetRange Range
deriving (Typeable, Data, Show)
instance HasRange LetInfo where
getRange (LetRange r) = r
instance KillRange LetInfo where
killRange (LetRange r) = LetRange (killRange r)
data DefInfo =
DefInfo { defFixity :: Fixity'
, defAccess :: Access
, defAbstract :: IsAbstract
, defInfo :: DeclInfo
}
deriving (Typeable, Data, Show)
mkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo
mkDefInfo x f a ab r = DefInfo f a ab (DeclInfo x r)
instance HasRange DefInfo where
getRange = getRange . defInfo
instance KillRange DefInfo where
killRange i = i { defInfo = killRange $ defInfo i }
data DeclInfo =
DeclInfo { declName :: Name
, declRange :: Range
}
deriving (Typeable, Data, Show)
instance HasRange DeclInfo where
getRange = declRange
instance KillRange DeclInfo where
killRange i = i { declRange = killRange $ declRange i }
newtype LHSInfo = LHSRange Range
deriving (Typeable, Data, Show)
instance HasRange LHSInfo where
getRange (LHSRange r) = r
instance KillRange LHSInfo where
killRange (LHSRange r) = LHSRange (killRange r)
data PatInfo = PatRange Range
| PatSource Range (Precedence -> Pattern)
deriving (Typeable, Data)
instance Show PatInfo where
show (PatRange r) = "PatRange " ++ show r
show (PatSource r _) = "PatSource " ++ show r
instance HasRange PatInfo where
getRange (PatRange r) = r
getRange (PatSource r _) = r
instance KillRange PatInfo where
killRange (PatRange r) = PatRange $ killRange r
killRange (PatSource r f) = PatSource (killRange r) f