1
{-# LANGUAGE DeriveDataTypeable #-}
2
{-| The abstract syntax. This is what you get after desugaring and scope
3
analysis of the concrete syntax. The type checker works on abstract syntax,
4
producing internal syntax ("Agda.Syntax.Internal").
6
module Agda.Syntax.Abstract
7
( module Agda.Syntax.Abstract
8
, module Agda.Syntax.Abstract.Name
11
import Prelude hiding (foldr)
12
import Control.Applicative
13
import Data.Sequence (Seq, (<|), (><))
14
import qualified Data.Sequence as Seq
15
import Data.Foldable as Fold
16
import Data.Traversable
18
import Data.Generics (Typeable, Data)
20
import qualified Agda.Syntax.Concrete as C
21
import Agda.Syntax.Info
22
import Agda.Syntax.Common
23
import Agda.Syntax.Position
24
import Agda.Syntax.Abstract.Name
25
import Agda.Syntax.Literal
26
import Agda.Syntax.Scope.Base
28
import Agda.Utils.Tuple
31
= Var Name -- ^ Bound variables
32
| Def QName -- ^ Constants (i.e. axioms, functions, and datatypes)
33
| Con AmbiguousQName -- ^ Constructors
34
| Lit Literal -- ^ Literals
35
| QuestionMark MetaInfo -- ^ meta variable for interaction
36
| Underscore MetaInfo -- ^ meta variable for hidden argument (must be inferred locally)
37
| App ExprInfo Expr (NamedArg Expr) -- ^
38
| WithApp ExprInfo Expr [Expr] -- ^ with application
39
| Lam ExprInfo LamBinding Expr -- ^
40
| AbsurdLam ExprInfo Hiding
41
| Pi ExprInfo Telescope Expr -- ^
42
| Fun ExprInfo (Arg Expr) Expr -- ^ independent function space
43
| Set ExprInfo Nat -- ^
45
| Let ExprInfo [LetBinding] Expr -- ^
46
| ETel Telescope -- ^ only used when printing telescopes
47
| Rec ExprInfo [(C.Name, Expr)] -- ^ record construction
48
| ScopedExpr ScopeInfo Expr -- ^ scope annotation
49
deriving (Typeable, Data)
52
= Axiom DefInfo QName Expr -- ^ postulate
53
| Field DefInfo QName Expr -- ^ record field
54
| Primitive DefInfo QName Expr -- ^ primitive function
55
| Definition DeclInfo [TypeSignature] [Definition] -- ^ a bunch of mutually recursive definitions
56
| Section ModuleInfo ModuleName [TypedBindings] [Declaration]
57
| Apply ModuleInfo ModuleName [TypedBindings] ModuleName [NamedArg Expr] (Map QName QName) (Map ModuleName ModuleName)
58
| Import ModuleInfo ModuleName
60
| Open ModuleInfo ModuleName
61
-- ^ only retained for highlighting purposes
62
| ScopedDecl ScopeInfo [Declaration] -- ^ scope annotation
63
deriving (Typeable, Data)
65
data Pragma = OptionsPragma [String]
66
| BuiltinPragma String Expr
67
| CompiledPragma QName String
68
| CompiledTypePragma QName String
69
| CompiledDataPragma QName String [String]
70
deriving (Typeable, Data)
72
data LetBinding = LetBind LetInfo Name Expr Expr -- ^ LetBind info name type defn
73
| LetApply ModuleInfo ModuleName [TypedBindings] ModuleName [NamedArg Expr] (Map QName QName) (Map ModuleName ModuleName)
74
| LetOpen ModuleInfo ModuleName -- ^ only for highlighting
75
deriving (Typeable, Data)
77
-- | A definition without its type signature.
79
= FunDef DefInfo QName [Clause]
80
| DataDef DefInfo QName Induction [LamBinding] [Constructor]
81
-- ^ the 'LamBinding's are 'DomainFree' and binds the parameters of the datatype.
82
| RecDef DefInfo QName [LamBinding] Expr [Declaration]
83
-- ^ the 'Expr' gives the constructor type telescope: @(x1 : A1)..(xn : An) -> Prop@
84
| ScopedDef ScopeInfo Definition
85
deriving (Typeable, Data)
88
type TypeSignature = Declaration
89
type Constructor = TypeSignature
91
-- | A lambda binding is either domain free or typed.
93
= DomainFree Hiding Name -- ^ . @x@ or @{x}@
94
| DomainFull TypedBindings -- ^ . @(xs:e)@ or @{xs:e}@
95
deriving (Typeable, Data)
97
-- | Typed bindings with hiding information.
98
data TypedBindings = TypedBindings Range Hiding [TypedBinding]
99
-- ^ . @(xs:e;..;ys:e')@ or @{xs:e;..;ys:e'}@
100
deriving (Typeable, Data)
102
-- | A typed binding. Appears in dependent function spaces, typed lambdas, and
103
-- telescopes. I might be tempting to simplify this to only bind a single
104
-- name at a time. This would mean that we would have to typecheck the type
105
-- several times (@x,y:A@ vs. @x:A; y:A@). In most cases this wouldn't
106
-- really be a problem, but it's good principle to not do extra work unless
108
data TypedBinding = TBind Range [Name] Expr
110
deriving (Typeable, Data)
112
type Telescope = [TypedBindings]
114
-- | We could throw away @where@ clauses at this point and translate them to
115
-- @let@. It's not obvious how to remember that the @let@ was really a
116
-- @where@ clause though, so for the time being we keep it here.
117
data Clause = Clause LHS RHS [Declaration]
118
deriving (Typeable, Data)
121
| WithRHS QName [Expr] [Clause] -- ^ The 'QName' is the name of the with function.
122
deriving (Typeable, Data)
124
data LHS = LHS LHSInfo QName [NamedArg Pattern] [Pattern]
125
deriving (Typeable, Data)
127
-- | Parameterised over the type of dot patterns.
128
data Pattern' e = VarP Name
129
| ConP PatInfo AmbiguousQName [NamedArg (Pattern' e)]
130
| DefP PatInfo QName [NamedArg (Pattern' e)] -- ^ defined pattern
132
| AsP PatInfo Name (Pattern' e)
136
| ImplicitP PatInfo -- ^ generated at type checking for implicit arguments
137
deriving (Typeable, Data)
139
type Pattern = Pattern' Expr
141
{--------------------------------------------------------------------------
143
--------------------------------------------------------------------------}
145
instance Functor Pattern' where
148
ConP i c ps -> ConP i c $ (fmap . fmap . fmap . fmap) f ps
149
DefP i c ps -> DefP i c $ (fmap . fmap . fmap . fmap) f ps
151
AsP i x p -> AsP i x $ fmap f p
152
DotP i e -> DotP i (f e)
153
AbsurdP i -> AbsurdP i
155
ImplicitP i -> ImplicitP i
157
-- foldr should really take its arguments in a different order!
158
instance Foldable Pattern' where
159
foldr f z p = case p of
161
ConP _ _ ps -> (foldrF . foldrF . foldrF . foldrF) f ps z
162
DefP _ _ ps -> (foldrF . foldrF . foldrF . foldrF) f ps z
164
AsP _ _ p -> foldr f z p
170
foldrF f = flip (foldr f)
172
instance Traversable Pattern' where
173
traverse f p = case p of
174
VarP x -> pure $ VarP x
175
ConP i c ps -> ConP i c <$> (traverse . traverse . traverse . traverse) f ps
176
DefP i c ps -> DefP i c <$> (traverse . traverse . traverse . traverse) f ps
177
LitP l -> pure $ LitP l
178
AsP i x p -> AsP i x <$> traverse f p
179
DotP i e -> DotP i <$> f e
180
AbsurdP i -> pure $ AbsurdP i
181
WildP i -> pure $ WildP i
182
ImplicitP i -> pure $ ImplicitP i
184
instance HasRange LamBinding where
185
getRange (DomainFree _ x) = getRange x
186
getRange (DomainFull b) = getRange b
188
instance HasRange TypedBindings where
189
getRange (TypedBindings r _ _) = r
191
instance HasRange TypedBinding where
192
getRange (TBind r _ _) = r
193
getRange (TNoBind e) = getRange e
195
instance HasRange Expr where
196
getRange (Var x) = getRange x
197
getRange (Def x) = getRange x
198
getRange (Con x) = getRange x
199
getRange (Lit l) = getRange l
200
getRange (QuestionMark i) = getRange i
201
getRange (Underscore i) = getRange i
202
getRange (App i _ _) = getRange i
203
getRange (WithApp i _ _) = getRange i
204
getRange (Lam i _ _) = getRange i
205
getRange (AbsurdLam i _) = getRange i
206
getRange (Pi i _ _) = getRange i
207
getRange (Fun i _ _) = getRange i
208
getRange (Set i _) = getRange i
209
getRange (Prop i) = getRange i
210
getRange (Let i _ _) = getRange i
211
getRange (Rec i _) = getRange i
212
getRange (ETel tel) = getRange tel
213
getRange (ScopedExpr _ e) = getRange e
215
instance HasRange Declaration where
216
getRange (Axiom i _ _ ) = getRange i
217
getRange (Field i _ _ ) = getRange i
218
getRange (Definition i _ _ ) = getRange i
219
getRange (Section i _ _ _ ) = getRange i
220
getRange (Apply i _ _ _ _ _ _ ) = getRange i
221
getRange (Import i _ ) = getRange i
222
getRange (Primitive i _ _ ) = getRange i
223
getRange (Pragma i _ ) = getRange i
224
getRange (Open i _ ) = getRange i
225
getRange (ScopedDecl _ d ) = getRange d
227
instance HasRange Definition where
228
getRange (FunDef i _ _ ) = getRange i
229
getRange (DataDef i _ _ _ _ ) = getRange i
230
getRange (RecDef i _ _ _ _) = getRange i
231
getRange (ScopedDef _ d) = getRange d
233
instance HasRange (Pattern' e) where
234
getRange (VarP x) = getRange x
235
getRange (ConP i _ _) = getRange i
236
getRange (DefP i _ _) = getRange i
237
getRange (WildP i) = getRange i
238
getRange (ImplicitP i) = getRange i
239
getRange (AsP i _ _) = getRange i
240
getRange (DotP i _) = getRange i
241
getRange (AbsurdP i) = getRange i
242
getRange (LitP l) = getRange l
244
instance HasRange LHS where
245
getRange (LHS i _ _ _) = getRange i
247
instance HasRange Clause where
248
getRange (Clause lhs rhs ds) = getRange (lhs,rhs,ds)
250
instance HasRange RHS where
251
getRange AbsurdRHS = noRange
252
getRange (RHS e) = getRange e
253
getRange (WithRHS _ e cs) = fuseRange e cs
255
instance HasRange LetBinding where
256
getRange (LetBind i _ _ _ ) = getRange i
257
getRange (LetApply i _ _ _ _ _ _ ) = getRange i
258
getRange (LetOpen i _ ) = getRange i
260
instance KillRange LamBinding where
261
killRange (DomainFree h x) = killRange1 (DomainFree h) x
262
killRange (DomainFull b) = killRange1 DomainFull b
264
instance KillRange TypedBindings where
265
killRange (TypedBindings r h b) = TypedBindings (killRange r) h (killRange b)
267
instance KillRange TypedBinding where
268
killRange (TBind r xs e) = killRange3 TBind r xs e
269
killRange (TNoBind e) = killRange1 TNoBind e
271
instance KillRange Expr where
272
killRange (Var x) = killRange1 Var x
273
killRange (Def x) = killRange1 Def x
274
killRange (Con x) = killRange1 Con x
275
killRange (Lit l) = killRange1 Lit l
276
killRange (QuestionMark i) = killRange1 QuestionMark i
277
killRange (Underscore i) = killRange1 Underscore i
278
killRange (App i e1 e2) = killRange3 App i e1 e2
279
killRange (WithApp i e es) = killRange3 WithApp i e es
280
killRange (Lam i b e) = killRange3 Lam i b e
281
killRange (AbsurdLam i h) = killRange1 AbsurdLam i h
282
killRange (Pi i a b) = killRange3 Pi i a b
283
killRange (Fun i a b) = killRange3 Fun i a b
284
killRange (Set i n) = Set (killRange i) n
285
killRange (Prop i) = killRange1 Prop i
286
killRange (Let i ds e) = killRange3 Let i ds e
287
killRange (Rec i fs) = Rec (killRange i) (map (id -*- killRange) fs)
288
killRange (ETel tel) = killRange1 ETel tel
289
killRange (ScopedExpr s e) = killRange1 (ScopedExpr s) e
291
instance KillRange Declaration where
292
killRange (Axiom i a b ) = killRange3 Axiom i a b
293
killRange (Field i a b ) = killRange3 Field i a b
294
killRange (Definition i a b ) = killRange3 Definition i a b
295
killRange (Section i a b c ) = killRange4 Section i a b c
296
killRange (Apply i a b c d e f ) = killRange5 Apply i a b c d e f
297
killRange (Import i a ) = killRange2 Import i a
298
killRange (Primitive i a b ) = killRange3 Primitive i a b
299
killRange (Pragma i a ) = Pragma (killRange i) a
300
killRange (Open i x ) = killRange2 Open i x
301
killRange (ScopedDecl a d ) = killRange1 (ScopedDecl a) d
303
instance KillRange Definition where
304
killRange (FunDef i a b ) = killRange3 FunDef i a b
305
killRange (DataDef i a b c d) = killRange5 DataDef i a b c d
306
killRange (RecDef i a b c d) = killRange5 RecDef i a b c d
307
killRange (ScopedDef s a) = killRange1 (ScopedDef s) a
309
instance KillRange e => KillRange (Pattern' e) where
310
killRange (VarP x) = killRange1 VarP x
311
killRange (ConP i a b) = killRange3 ConP i a b
312
killRange (DefP i a b) = killRange3 DefP i a b
313
killRange (WildP i) = killRange1 WildP i
314
killRange (ImplicitP i) = killRange1 ImplicitP i
315
killRange (AsP i a b) = killRange3 AsP i a b
316
killRange (DotP i a) = killRange2 DotP i a
317
killRange (AbsurdP i) = killRange1 AbsurdP i
318
killRange (LitP l) = killRange1 LitP l
320
instance KillRange LHS where
321
killRange (LHS i a b c) = killRange4 LHS i a b c
323
instance KillRange Clause where
324
killRange (Clause lhs rhs ds) = killRange3 Clause lhs rhs ds
326
instance KillRange RHS where
327
killRange AbsurdRHS = AbsurdRHS
328
killRange (RHS e) = killRange1 RHS e
329
killRange (WithRHS q e cs) = killRange3 WithRHS q e cs
331
instance KillRange LetBinding where
332
killRange (LetBind i a b c ) = killRange4 LetBind i a b c
333
killRange (LetApply i a b c d e f ) = killRange5 LetApply i a b c d e f
334
killRange (LetOpen i x ) = killRange2 LetOpen i x
336
------------------------------------------------------------------------
338
------------------------------------------------------------------------
340
-- | Extracts all the names which are declared in a 'Declaration'.
341
-- This does not include open public or let expressions, but it does
342
-- include local modules and where clauses.
344
allNames :: Declaration -> Seq QName
345
allNames (Axiom _ q _) = Seq.singleton q
346
allNames (Field _ q _) = Seq.singleton q
347
allNames (Primitive _ q _) = Seq.singleton q
348
allNames (Definition _ _ defs) = Fold.foldMap allNamesD defs
350
allNamesD :: Definition -> Seq QName
351
allNamesD (FunDef _ q cls) = q <| Fold.foldMap allNamesC cls
352
allNamesD (DataDef _ q _ _ decls) = q <| Fold.foldMap allNames decls
353
allNamesD (RecDef _ q _ _ decls) = q <| Fold.foldMap allNames decls
354
allNamesD (ScopedDef _ def) = allNamesD def
356
allNamesC :: Clause -> Seq QName
357
allNamesC (Clause _ rhs decls) = allNamesR rhs ><
358
Fold.foldMap allNames decls
360
allNamesR :: RHS -> Seq QName
361
allNamesR RHS {} = Seq.empty
362
allNamesR AbsurdRHS {} = Seq.empty
363
allNamesR (WithRHS q _ cls) = q <| Fold.foldMap allNamesC cls
364
allNames (Section _ _ _ decls) = Fold.foldMap allNames decls
365
allNames Apply {} = Seq.empty
366
allNames Import {} = Seq.empty
367
allNames Pragma {} = Seq.empty
368
allNames Open {} = Seq.empty
369
allNames (ScopedDecl _ decls) = Fold.foldMap allNames decls
added
removed
src/full/Agda/Syntax/Abstract.hs
