module Agda.Syntax.Info where
import Data.Typeable (Typeable)
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)
data MetaInfo = MetaInfo
{ metaRange :: Range
, metaScope :: ScopeInfo
, metaNumber :: Maybe Nat
, metaNameSuggestion :: String
}
deriving (Typeable, Show)
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 (Typeable, Show)
exprNoRange :: ExprInfo
exprNoRange = ExprRange noRange
instance HasRange ExprInfo where
getRange (ExprRange r) = r
instance KillRange ExprInfo where
killRange (ExprRange r) = exprNoRange
data ModuleInfo = ModuleInfo
{ minfoRange :: Range
, minfoAsTo :: Range
, minfoAsName :: Maybe C.Name
, minfoOpenShort :: Maybe OpenShortHand
, minfoDirective :: Maybe ImportDirective
}
deriving (Typeable)
deriving instance (Show OpenShortHand, Show ImportDirective) => 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 (Typeable, Show)
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
, defInfo :: DeclInfo
}
deriving (Typeable, Show)
mkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo
mkDefInfo x f a ab r = DefInfo f a ab NotInstanceDef (DeclInfo x r)
mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> Range -> DefInfo
mkDefInfoInstance x f a ab i r = DefInfo f a ab i (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 (Typeable, Show)
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
, mutualRange :: Range
}
deriving (Typeable, Show)
instance HasRange MutualInfo where
getRange = mutualRange
instance KillRange MutualInfo where
killRange i = i { mutualRange = noRange }
newtype LHSInfo = LHSRange Range
deriving (Typeable, Show)
instance HasRange LHSInfo where
getRange (LHSRange r) = r
instance KillRange LHSInfo where
killRange (LHSRange r) = LHSRange noRange
data PatInfo
= PatRange Range
| PatSource Range (Precedence -> Pattern)
deriving (Typeable)
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 noRange
killRange (PatSource r f) = PatSource noRange f
patNoRange :: PatInfo
patNoRange = PatRange noRange
data ConPatInfo = ConPatInfo
{ patImplicit :: Bool
, patInfo :: PatInfo
}
instance Show ConPatInfo where
show (ConPatInfo b i) = (if b then ("implicit " ++) else id) $ show i
instance HasRange ConPatInfo where
getRange = getRange . patInfo
instance KillRange ConPatInfo where
killRange (ConPatInfo b i) = ConPatInfo b $ killRange i
instance SetRange ConPatInfo where
setRange r (ConPatInfo b i) = ConPatInfo b $ PatRange r