content: {-# OPTIONS_GHC -Wunused-imports #-}
  {-# OPTIONS_GHC -Wunused-matches #-}
  
  {-| 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 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)
  
  import Agda.Utils.Functor
  import Agda.Utils.Null
  
  {--------------------------------------------------------------------------
      Meta information
   --------------------------------------------------------------------------}
  
  -- | Kind of a meta: the method how to solve it.
  --
  data MetaKind
    = InstanceMeta     -- ^ Meta variable solved by instance search.
    | UnificationMeta  -- ^ Meta variable solved by unification (default).
    deriving (Show, Eq, Generic)
  
  instance Null MetaKind where
    empty = UnificationMeta
  
  instance NFData MetaKind
  
  -- | Default meta kind from its 'Hiding' context.
  --
  hidingToMetaKind :: Hiding -> MetaKind
  hidingToMetaKind = \case
    Instance{} -> InstanceMeta
    Hidden     -> UnificationMeta
    NotHidden  -> UnificationMeta
  
  -- | Name suggestion for meta variable.  Empty string means no suggestion.
  type MetaNameSuggestion = String
  
  -- | Information associated to a meta variable in the abstract syntax.
  --
  data MetaInfo = MetaInfo
    { metaRange          :: Range
    , metaScope          :: ScopeInfo
    , metaNumber         :: Maybe MetaId
    , metaNameSuggestion :: MetaNameSuggestion
    , metaKind           :: MetaKind
    }
    deriving (Show, Eq, Generic)
  
  emptyMetaInfo :: MetaInfo
  emptyMetaInfo = MetaInfo
    { metaRange          = noRange
    , metaScope          = empty
    , metaNumber         = Nothing
    , metaNameSuggestion = ""
    , metaKind           = empty
    }
  
  instance Null MetaInfo where
    empty = emptyMetaInfo
  
  instance HasRange MetaInfo where
    getRange = metaRange
  
  instance KillRange MetaInfo where
    killRange m = m { metaRange = noRange }
  
  instance NFData MetaInfo where
    rnf (MetaInfo _ a b c d) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d
  
  {--------------------------------------------------------------------------
      General expression information
   --------------------------------------------------------------------------}
  
  newtype ExprInfo = ExprRange Range
    deriving (Show, Eq, Null, NFData)
  
  exprNoRange :: ExprInfo
  exprNoRange = ExprRange noRange
  
  instance HasRange ExprInfo where
    getRange (ExprRange r) = r
  
  instance KillRange ExprInfo where
    killRange (ExprRange _) = exprNoRange
  
  {--------------------------------------------------------------------------
      Application information
   --------------------------------------------------------------------------}
  
  -- | Information about application
  data AppInfo = AppInfo
    { appRange  :: Range
    , appOrigin :: Origin
    , appParens :: ParenPreference -- ^ Do we prefer a lambda argument with or without parens?
    }
    deriving (Show, Eq, Ord, Generic)
  
  -- | Default is system inserted and prefer parens.
  defaultAppInfo :: Range -> AppInfo
  defaultAppInfo r = AppInfo{ appRange = r, appOrigin = Inserted, appParens = PreferParen }
  
  -- | `AppInfo` with no range information.
  defaultAppInfo_ :: AppInfo
  defaultAppInfo_ = defaultAppInfo noRange
  
  instance Null AppInfo where
    empty = defaultAppInfo_
  
  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
    mapOrigin f i = i { appOrigin = f (appOrigin i) }
  
  instance NFData AppInfo
  
  {--------------------------------------------------------------------------
      Module information
   --------------------------------------------------------------------------}
  
  data ModuleInfo = ModuleInfo
    { minfoRange    :: Range
    , minfoAsTo     :: Range
      -- ^ The range of the \"as\" and \"to\" keywords,
      -- if any. Retained for highlighting purposes.
    , minfoAsName   :: Maybe C.Name
      -- ^ The \"as\" module name, if any. Retained for highlighting purposes.
    , minfoOpenShort :: Maybe OpenShortHand
    , minfoDirective :: Maybe ImportDirective
      -- ^ Retained for @abstractToConcrete@ of 'ModuleMacro'.
    }
    deriving (Eq, Show, Generic)
  
  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 }
  
  instance NFData ModuleInfo
  
  ---------------------------------------------------------------------------
  -- Let info
  ---------------------------------------------------------------------------
  
  newtype LetInfo = LetRange Range
    deriving (Show, Eq, Null, NFData)
  
  instance HasRange LetInfo where
    getRange (LetRange r)   = r
  
  instance KillRange LetInfo where
    killRange (LetRange _) = LetRange noRange
  
  {--------------------------------------------------------------------------
      Definition information (declarations that actually define something)
   --------------------------------------------------------------------------}
  
  data DefInfo' t = DefInfo
    { defFixity   :: Fixity'
    , defAccess   :: Access
    , defAbstract :: IsAbstract
    , defOpaque   :: IsOpaque
    , defInstance :: IsInstance
    , defMacro    :: IsMacro
    , defInfo     :: DeclInfo
    , defTactic   :: TacticAttribute' t
    }
    deriving (Show, Eq, Generic)
  
  mkDefInfo :: Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
  mkDefInfo x f a ab r = mkDefInfoInstance x f a ab NotInstanceDef NotMacroDef r
  
  -- | Same as @mkDefInfo@ but where we can also give the @IsInstance@
  mkDefInfoInstance :: Name -> Fixity' -> Access -> IsAbstract -> IsInstance -> IsMacro -> Range -> DefInfo' t
  mkDefInfoInstance x f a ab i m r = DefInfo f a ab TransparentDef i m (DeclInfo x r) empty
  
  instance HasRange (DefInfo' t) where
    getRange = getRange . defInfo
  
  instance SetRange (DefInfo' t) where
    setRange r i = i { defInfo = setRange r (defInfo i) }
  
  instance KillRange t => KillRange (DefInfo' t) where
    killRange i = i { defInfo   = killRange $ defInfo i,
                      defTactic = killRange $ defTactic i }
  
  instance LensIsAbstract (DefInfo' t) where
    lensIsAbstract f i = (f $! defAbstract i) <&> \ a -> i { defAbstract = a }
  
  instance LensIsOpaque (DefInfo' t) where
    lensIsOpaque f i = (f $! defOpaque i) <&> \ a -> i { defOpaque = a }
  
  instance AnyIsAbstract (DefInfo' t) where
    anyIsAbstract = defAbstract
  
  instance AllAreOpaque (DefInfo' t) where
    jointOpacity = jointOpacity . defOpaque
  
  instance NFData t => NFData (DefInfo' t)
  
  {--------------------------------------------------------------------------
      General declaration information
   --------------------------------------------------------------------------}
  
  data DeclInfo = DeclInfo
    { declName  :: Name
    , declRange :: Range
    }
    deriving (Show, Eq, Generic)
  
  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 }
  
  instance NFData DeclInfo
  
  {--------------------------------------------------------------------------
      Mutual block information
   --------------------------------------------------------------------------}
  
  data MutualInfo = MutualInfo
    { mutualTerminationCheck :: TerminationCheck Name
    , mutualCoverageCheck    :: CoverageCheck
    , mutualPositivityCheck  :: PositivityCheck
    , mutualRange            :: Range
    }
    deriving (Show, Eq, Generic)
  
  -- | Default value for 'MutualInfo'.
  instance Null MutualInfo where
    empty = MutualInfo TerminationCheck YesCoverageCheck YesPositivityCheck noRange
  
  instance HasRange MutualInfo where
    getRange = mutualRange
  
  instance KillRange MutualInfo where
    killRange i = i { mutualRange = noRange }
  
  instance NFData MutualInfo
  
  {--------------------------------------------------------------------------
      Left hand side information
   --------------------------------------------------------------------------}
  
  data LHSInfo = LHSInfo
    { lhsRange    :: Range
    , lhsEllipsis :: ExpandedEllipsis
    } deriving (Show, Eq, Generic)
  
  instance HasRange LHSInfo where
    getRange (LHSInfo r _) = r
  
  instance KillRange LHSInfo where
    killRange (LHSInfo _ ell) = LHSInfo noRange ell
  
  instance Null LHSInfo where
    null i = null (lhsRange i) && null (lhsEllipsis i)
    empty  = LHSInfo empty empty
  
  instance NFData LHSInfo
  
  {--------------------------------------------------------------------------
      Pattern information
   --------------------------------------------------------------------------}
  
  -- | For a general pattern we remember the source code position.
  newtype PatInfo
    = PatRange Range
    deriving (Eq, Null, Semigroup, Monoid, Show, SetRange, HasRange,
              KillRange, NFData)
  
  -- | Empty range for patterns.
  patNoRange :: PatInfo
  patNoRange = PatRange noRange
  
  -- | Constructor pattern info.
  data ConPatInfo = ConPatInfo
    { 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
    , conPatLazy     :: ConPatLazy
    }
    deriving (Eq, Show, Generic)
  
  instance HasRange ConPatInfo where
    getRange = getRange . conPatInfo
  
  instance KillRange ConPatInfo where
    killRange (ConPatInfo b i l) = ConPatInfo b (killRange i) l
  
  instance SetRange ConPatInfo where
    setRange r (ConPatInfo b _ l) = ConPatInfo b (PatRange r) l
  
  instance NFData ConPatInfo
  
  -- | Has the constructor pattern a dotted (forced) constructor?
  data ConPatLazy
    = ConPatLazy   -- ^ Dotted constructor.
    | ConPatEager  -- ^ Ordinary constructor.
    deriving (Eq, Ord, Show, Bounded, Enum, Generic)
  
  instance NFData ConPatLazy
  