summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Info.hs
blob: 5c919551e3b5074ec15cdd201940a910a869041c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE UndecidableInstances #-}

{-| 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 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)

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

data MetaInfo = MetaInfo
  { metaRange          :: Range
  , metaScope          :: ScopeInfo
  , metaNumber         :: Maybe Nat  -- ^ The 'MetaId', not the 'InteractionId'.
  , 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 }

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

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

{--------------------------------------------------------------------------
    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 (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 }

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

newtype LetInfo = LetRange Range
  deriving (Typeable, Show)

instance HasRange LetInfo where
  getRange (LetRange r)   = r

instance KillRange LetInfo where
  killRange (LetRange r) = LetRange noRange

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

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)

-- | Same as @mkDefInfo@ but where we can also give the @IsInstance@
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 }

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

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 }

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

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 }

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

newtype LHSInfo = LHSRange Range
  deriving (Typeable, Show)

instance HasRange LHSInfo where
  getRange (LHSRange r) = r

instance KillRange LHSInfo where
  killRange (LHSRange r) = LHSRange noRange

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

-- | For a general pattern we can either remember just the source code
--   position or the entire concrete pattern it came from.
data PatInfo
  = PatRange Range
  | PatSource Range (Precedence -> Pattern)
      -- ^ Even if we store the original pattern we have to know
      --   whether to put parenthesis around it.
  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

-- | Empty range for patterns.
patNoRange :: PatInfo
patNoRange = PatRange noRange

-- | Constructor pattern info.
data ConPatInfo = ConPatInfo
  { patImplicit :: Bool
    -- ^ Does this pattern come form the eta-expansion of an implicit pattern?
  , 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