← Back to branch summary

~ubuntu-branches/ubuntu/trusty/agda/trusty

« back to all changes in this revision

Viewing changes to src/full/Agda/Syntax/Abstract.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane, Kiwamu Okabe, Iain Lane
  • Date: 2013-04-10 11:46:43 UTC
  • mfrom: (4.1.5 experimental)
  • Revision ID: package-import@ubuntu.com-20130410114643-prunhsz59f0fhrdn
Tags: 2.3.2-1
[ Kiwamu Okabe ]
* New patch: Extend haskell-src-exts dependency and fix type miss.

[ Iain Lane ]
* [dfbca48] Imported Upstream version 2.3.2
* [7746bcc] Remove all patches — all upstream.
* [2cdb691] Update build-deps to match control file
* [868ebf4] agda-mode no longer depends on haskell-mode or GHCi.
  Remove dependency and update .el file accordingly
* [9e0ba22] Add agda-bin package here, as the separate package has been
  removed
* [75a240f] agda-mode needs to depend on agda-bin
* [d290f95] Allow Quickcheck up to 2.7. Fix haskeline build-dep.
* [79190e6] Add missing geniplate and parallel BDs

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Syntax/Abstract.hs
1
 
{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveFoldable, DeriveTraversable, CPP #-}
 
1
{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveFoldable,
 
2
             DeriveTraversable, CPP, TemplateHaskell,
 
3
             MultiParamTypeClasses, FlexibleInstances,
 
4
             TypeSynonymInstances #-}
2
5
{-| The abstract syntax. This is what you get after desugaring and scope
3
6
    analysis of the concrete syntax. The type checker works on abstract syntax,
4
7
    producing internal syntax ("Agda.Syntax.Internal").
8
11
    , module Agda.Syntax.Abstract.Name
9
12
    ) where
10
13
 
11
 
import Prelude hiding (foldr)
 
14
import Prelude hiding (foldl, foldr)
12
15
import Control.Applicative
13
16
import Data.Sequence (Seq, (<|), (><))
14
17
import qualified Data.Sequence as Seq
15
18
import Data.Foldable as Fold
16
19
import Data.Traversable
17
20
import Data.Map (Map)
18
 
import Data.Generics (Typeable, Data)
 
21
import Data.Typeable (Typeable)
19
22
 
20
23
import qualified Agda.Syntax.Concrete as C
21
24
import Agda.Syntax.Concrete.Pretty ()
27
30
import Agda.Syntax.Literal
28
31
import Agda.Syntax.Scope.Base
29
32
 
 
33
import Agda.Utils.Geniplate
30
34
import Agda.Utils.Tuple
31
35
 
32
36
#include "../undefined.h"
34
38
 
35
39
data Expr
36
40
        = Var  Name                          -- ^ Bound variables
37
 
        | Def  QName                         -- ^ Constants (i.e. axioms, functions, and datatypes)
 
41
        | Def  QName                         -- ^ Constants (i.e. axioms, functions, projections, and datatypes)
38
42
        | Con  AmbiguousQName                -- ^ Constructors
39
43
        | Lit Literal                        -- ^ Literals
40
44
        | QuestionMark MetaInfo              -- ^ meta variable for interaction
46
50
        | ExtendedLam ExprInfo DefInfo QName [Clause]
47
51
        | Pi   ExprInfo Telescope Expr       -- ^
48
52
        | Fun  ExprInfo (Arg Expr) Expr      -- ^ independent function space
49
 
        | Set  ExprInfo Nat                  -- ^ Set, Set1, Set2, ...
 
53
        | Set  ExprInfo Integer              -- ^ Set, Set1, Set2, ...
50
54
        | Prop ExprInfo                      -- ^
51
55
        | Let  ExprInfo [LetBinding] Expr    -- ^
52
56
        | ETel Telescope                     -- ^ only used when printing telescopes
53
57
        | Rec  ExprInfo [(C.Name, Expr)]     -- ^ record construction
54
58
        | RecUpdate ExprInfo Expr [(C.Name, Expr)]     -- ^ record update
55
59
        | ScopedExpr ScopeInfo Expr          -- ^ scope annotation
56
 
        | QuoteGoal ExprInfo Name Expr       -- ^
 
60
        | QuoteGoal ExprInfo Name Expr       -- ^ binds @Name@ to current type in @Expr@
57
61
        | Quote ExprInfo                     -- ^
58
62
        | QuoteTerm ExprInfo                 -- ^
59
63
        | Unquote ExprInfo                   -- ^ The splicing construct: unquote ...
60
64
        | DontCare Expr                      -- ^ for printing DontCare from Syntax.Internal
61
 
  deriving (Typeable, Data, Show)
 
65
        | PatternSyn QName
 
66
  deriving (Typeable, Show)
62
67
 
63
68
data Declaration
64
69
        = Axiom      DefInfo Relevance QName Expr          -- ^ postulate
65
70
        | Field      DefInfo QName (Arg Expr)              -- ^ record field
66
71
        | Primitive  DefInfo QName Expr                    -- ^ primitive function
67
 
        | Mutual     DeclInfo [Declaration]                -- ^ a bunch of mutually recursive definitions
 
72
        | Mutual     MutualInfo [Declaration]              -- ^ a bunch of mutually recursive definitions
68
73
        | Section    ModuleInfo ModuleName [TypedBindings] [Declaration]
69
74
        | Apply      ModuleInfo ModuleName ModuleApplication (Map QName QName) (Map ModuleName ModuleName)
70
75
        | Import     ModuleInfo ModuleName
71
76
        | Pragma     Range      Pragma
72
77
        | Open       ModuleInfo ModuleName
73
78
          -- ^ only retained for highlighting purposes
74
 
        | FunDef     DefInfo QName [Clause]
 
79
        | FunDef     DefInfo QName Delayed [Clause] -- ^ sequence of function clauses
75
80
        | DataSig    DefInfo QName Telescope Expr -- ^ lone data signature
76
81
            -- ^ the 'LamBinding's are 'DomainFree' and binds the parameters of the datatype.
77
82
        | DataDef    DefInfo QName [LamBinding] [Constructor]
78
83
            -- ^ the 'LamBinding's are 'DomainFree' and binds the parameters of the datatype.
79
84
        | RecSig     DefInfo QName Telescope Expr -- ^ lone record signature
80
 
        | RecDef     DefInfo QName (Maybe QName) [LamBinding] Expr [Declaration]
 
85
        | RecDef     DefInfo QName (Maybe Induction) (Maybe QName) [LamBinding] Expr [Declaration]
81
86
            -- ^ The 'Expr' gives the constructor type telescope, @(x1 : A1)..(xn : An) -> Prop@,
82
87
            --   and the optional name is the constructor's name.
83
88
        | ScopedDecl ScopeInfo [Declaration]  -- ^ scope annotation
84
 
        deriving (Typeable, Data, Show)
 
89
        deriving (Typeable, Show)
85
90
 
86
91
class GetDefInfo a where
87
92
  getDefInfo :: a -> Maybe DefInfo
91
96
  getDefInfo (Field i _ _) = Just i
92
97
  getDefInfo (Primitive i _ _) = Just i
93
98
  getDefInfo (ScopedDecl _ (d:_)) = getDefInfo d
94
 
  getDefInfo (FunDef i _ _) = Just i
 
99
  getDefInfo (FunDef i _ _ _) = Just i
95
100
  getDefInfo (DataSig i _ _ _) = Just i
96
101
  getDefInfo (DataDef i _ _ _) = Just i
97
102
  getDefInfo (RecSig i _ _ _) = Just i
98
 
  getDefInfo (RecDef i _ _ _ _ _) = Just i
 
103
  getDefInfo (RecDef i _ _ _ _ _ _) = Just i
99
104
  getDefInfo _ = Nothing
100
105
 
101
106
data ModuleApplication = SectionApp [TypedBindings] ModuleName [NamedArg Expr]
102
107
                       | RecordModuleIFS ModuleName
103
 
  deriving (Typeable, Data, Show)
 
108
  deriving (Typeable, Show)
104
109
 
105
110
data Pragma = OptionsPragma [String]
106
111
            | BuiltinPragma String Expr
111
116
            | CompiledJSPragma QName String
112
117
            | StaticPragma QName
113
118
            | EtaPragma QName
114
 
  deriving (Typeable, Data, Show)
 
119
  deriving (Typeable, Show)
115
120
 
116
121
data LetBinding = LetBind LetInfo Relevance Name Expr Expr    -- ^ LetBind info rel name type defn
 
122
                | LetPatBind LetInfo Pattern Expr -- ^ irrefutable pattern binding
117
123
                | LetApply ModuleInfo ModuleName ModuleApplication (Map QName QName) (Map ModuleName ModuleName)
118
124
                | LetOpen ModuleInfo ModuleName     -- ^ only for highlighting and abstractToConcrete
119
 
  deriving (Typeable, Data, Show)
 
125
  deriving (Typeable, Show)
120
126
 
121
127
-- | Only 'Axiom's.
122
128
type TypeSignature  = Declaration
123
129
type Constructor    = TypeSignature
 
130
type Field          = TypeSignature
124
131
 
125
132
-- | A lambda binding is either domain free or typed.
126
133
data LamBinding
127
134
        = DomainFree Hiding Relevance Name  -- ^ . @x@ or @{x}@ or @.x@ or @.{x}@
128
135
        | DomainFull TypedBindings  -- ^ . @(xs:e)@ or @{xs:e}@
129
 
  deriving (Typeable, Data, Show)
 
136
  deriving (Typeable, Show)
130
137
 
131
138
-- | Typed bindings with hiding information.
132
139
data TypedBindings = TypedBindings Range (Arg TypedBinding)
133
140
            -- ^ . @(xs : e)@ or @{xs : e}@
134
 
  deriving (Typeable, Data, Show)
 
141
  deriving (Typeable, Show)
135
142
 
136
143
-- | A typed binding. Appears in dependent function spaces, typed lambdas, and
137
144
--   telescopes. I might be tempting to simplify this to only bind a single
141
148
--   you have to.
142
149
data TypedBinding = TBind Range [Name] Expr
143
150
                  | TNoBind Expr
144
 
  deriving (Typeable, Data, Show)
 
151
  deriving (Typeable, Show)
145
152
 
146
153
type Telescope  = [TypedBindings]
147
154
 
148
155
-- | We could throw away @where@ clauses at this point and translate them to
149
156
--   @let@. It's not obvious how to remember that the @let@ was really a
150
157
--   @where@ clause though, so for the time being we keep it here.
151
 
data Clause     = Clause LHS RHS [Declaration]
152
 
  deriving (Typeable, Data, Show)
 
158
data Clause     = Clause
 
159
  { clauseLHS        :: LHS
 
160
  , clauseRHS        :: RHS
 
161
  , clauseWhereDecls :: [Declaration]
 
162
  } deriving (Typeable, Show)
 
163
 
153
164
data RHS        = RHS Expr
154
165
                | AbsurdRHS
155
166
                | WithRHS QName [Expr] [Clause] -- ^ The 'QName' is the name of the with function.
157
168
                    -- ^ The 'QName's are the names of the generated with functions.
158
169
                    --   One for each 'Expr'.
159
170
                    --   The RHS shouldn't be another RewriteRHS
160
 
  deriving (Typeable, Data, Show)
161
 
 
162
 
data LHS        = LHS LHSInfo QName [NamedArg Pattern] [Pattern]
163
 
  deriving (Typeable, Data, Show)
 
171
  deriving (Typeable, Show)
 
172
 
 
173
-- | The lhs of a clause in spine view (inside-out).
 
174
--   Projection patterns are contained in @spLhsPats@,
 
175
--   represented as @DefP d []@.
 
176
data SpineLHS = SpineLHS
 
177
  { spLhsInfo     :: LHSInfo             -- ^ Range.
 
178
  , spLhsDefName  :: QName               -- ^ Name of function we are defining.
 
179
  , spLhsPats     :: [NamedArg Pattern]  -- ^ Function parameters (patterns).
 
180
  , spLhsWithPats :: [Pattern]           -- ^ @with@ patterns (after @|@).
 
181
  }
 
182
  deriving (Typeable, Show)
 
183
 
 
184
-- | The lhs of a clause in projection-application view (outside-in).
 
185
--   Projection patters are represented as 'LHSProj's.
 
186
data LHS = LHS
 
187
  { lhsInfo     :: LHSInfo               -- ^ Range.
 
188
  , lhsCore     :: LHSCore               -- ^ Copatterns.
 
189
  , lhsWithPats :: [Pattern]             -- ^ @with@ patterns (after @|@).
 
190
  }
 
191
  deriving (Typeable, Show)
 
192
 
 
193
-- | The lhs minus @with@-patterns in projection-application view.
 
194
--   Parameterised over the type @e@ of dot patterns.
 
195
data LHSCore' e
 
196
    -- | The head applied to ordinary patterns.
 
197
  = LHSHead  { lhsDefName  :: QName                    -- ^ Head @f@.
 
198
             , lhsPats     :: [NamedArg (Pattern' e)]  -- ^ Applied to patterns @ps@.
 
199
             }
 
200
    -- | Projection
 
201
  | LHSProj  { lhsDestructor :: QName
 
202
               -- ^ Record projection identifier.
 
203
             , lhsPatsLeft   :: [NamedArg (Pattern' e)]
 
204
               -- ^ Indices of the projection.
 
205
               --   Currently none @[]@, since we do not have indexed records.
 
206
             , lhsFocus      :: NamedArg (LHSCore' e)
 
207
               -- ^ Main branch.
 
208
             , lhsPatsRight  :: [NamedArg (Pattern' e)]
 
209
               -- ^ Further applied to patterns.
 
210
             }
 
211
  deriving (Typeable, Show, Functor, Foldable, Traversable)
 
212
 
 
213
type LHSCore = LHSCore' Expr
 
214
 
 
215
lhsToSpine :: LHS -> SpineLHS
 
216
lhsToSpine (LHS i core wps) = SpineLHS i f ps wps
 
217
  where QNamed f ps = lhsCoreToSpine core
 
218
 
 
219
lhsCoreToSpine :: LHSCore' e -> QNamed [NamedArg (Pattern' e)]
 
220
lhsCoreToSpine (LHSHead f ps) = QNamed f ps
 
221
lhsCoreToSpine (LHSProj d ps1 h ps2) = (++ (p : ps2)) <$> lhsCoreToSpine (namedArg h)
 
222
  where p = updateNamedArg (const $ DefP i d ps1) h
 
223
        i = PatRange noRange
 
224
 
 
225
-- spineToLhsCore ::
 
226
 
 
227
-- | Used for checking pattern linearity.
 
228
lhsCoreAllPatterns :: LHSCore' e -> [Pattern' e]
 
229
lhsCoreAllPatterns = map namedArg . qnamed . lhsCoreToSpine
 
230
{- OLD code, dumps projection patterns, superfluous
 
231
lhsCoreAllPatterns (LHSHead f ps) = map namedArg ps
 
232
lhsCoreAllPatterns (LHSProj d ps1 l ps2) =
 
233
  map namedArg ps1 ++
 
234
  lhsCoreAllPatterns (namedArg l) ++
 
235
  map namedArg ps2
 
236
-}
 
237
 
 
238
-- | Used in AbstractToConcrete.
 
239
lhsCoreToPattern :: LHSCore -> Pattern
 
240
lhsCoreToPattern lc =
 
241
  case lc of
 
242
    LHSHead f aps -> DefP noInfo f aps
 
243
    LHSProj d aps1 lhscore aps2 -> DefP noInfo d $
 
244
      aps1 ++ fmap (fmap lhsCoreToPattern) lhscore : aps2
 
245
  where noInfo = PatRange noRange -- TODO, preserve range!
 
246
 
 
247
mapLHSHead :: (QName -> [NamedArg Pattern] -> LHSCore) -> LHSCore -> LHSCore
 
248
mapLHSHead f (LHSHead x ps)        = f x ps
 
249
mapLHSHead f (LHSProj d ps1 l ps2) =
 
250
  LHSProj d ps1 (fmap (fmap (mapLHSHead f)) l) ps2
 
251
 
 
252
{- UNUSED
 
253
mapLHSHeadM :: (Monad m) => (QName -> [NamedArg Pattern] -> m LHSCore) -> LHSCore -> m LHSCore
 
254
mapLHSHeadM f (LHSHead x ps)        = f x ps
 
255
mapLHSHeadM f (LHSProj d ps1 l ps2) = do
 
256
  l <- mapLHSHead f l
 
257
  return $ LHSProj d ps1 l ps2
 
258
-}
164
259
 
165
260
-- | Parameterised over the type of dot patterns.
166
 
data Pattern' e = VarP Name
167
 
                | ConP PatInfo AmbiguousQName [NamedArg (Pattern' e)]
168
 
                | DefP PatInfo QName          [NamedArg (Pattern' e)]  -- ^ defined pattern
169
 
                | WildP PatInfo
170
 
                | AsP PatInfo Name (Pattern' e)
171
 
                | DotP PatInfo e
172
 
                | AbsurdP PatInfo
173
 
                | LitP Literal
174
 
                | ImplicitP PatInfo     -- ^ generated at type checking for implicit arguments
175
 
  deriving (Typeable, Data, Show, Functor, Foldable, Traversable)
 
261
data Pattern' e
 
262
  = VarP Name
 
263
  | ConP PatInfo AmbiguousQName [NamedArg (Pattern' e)]
 
264
  | DefP PatInfo QName          [NamedArg (Pattern' e)]
 
265
    -- ^ Defined pattern: function definition @f ps@ or destructor pattern @d p ps@.
 
266
  | WildP PatInfo
 
267
  | AsP PatInfo Name (Pattern' e)
 
268
  | DotP PatInfo e
 
269
  | AbsurdP PatInfo
 
270
  | LitP Literal
 
271
  | ImplicitP PatInfo
 
272
    -- ^ Generated at type checking for implicit arguments.
 
273
  | PatternSynP PatInfo QName [NamedArg (Pattern' e)]
 
274
  deriving (Typeable, Show, Functor, Foldable, Traversable)
176
275
 
177
 
type Pattern = Pattern' Expr
 
276
type Pattern  = Pattern' Expr
 
277
type Patterns = [NamedArg Pattern]
178
278
 
179
279
{--------------------------------------------------------------------------
180
280
    Instances
192
292
    getRange (TNoBind e)   = getRange e
193
293
 
194
294
instance HasRange Expr where
195
 
    getRange (Var x)            = getRange x
196
 
    getRange (Def x)            = getRange x
197
 
    getRange (Con x)            = getRange x
198
 
    getRange (Lit l)            = getRange l
199
 
    getRange (QuestionMark i)   = getRange i
200
 
    getRange (Underscore  i)    = getRange i
201
 
    getRange (App i _ _)        = getRange i
202
 
    getRange (WithApp i _ _)    = getRange i
203
 
    getRange (Lam i _ _)        = getRange i
204
 
    getRange (AbsurdLam i _)    = getRange i
205
 
    getRange (ExtendedLam 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 (RecUpdate i _ _)  = getRange i
213
 
    getRange (ETel tel)         = getRange tel
214
 
    getRange (ScopedExpr _ e)   = getRange e
215
 
    getRange (QuoteGoal _ _ e)  = getRange e
216
 
    getRange (Quote i)          = getRange i
217
 
    getRange (QuoteTerm i)      = getRange i
218
 
    getRange (Unquote i)        = getRange i
219
 
    getRange (DontCare{})       = noRange
 
295
    getRange (Var x)               = getRange x
 
296
    getRange (Def x)               = getRange x
 
297
    getRange (Con x)               = getRange x
 
298
    getRange (Lit l)               = getRange l
 
299
    getRange (QuestionMark i)      = getRange i
 
300
    getRange (Underscore  i)       = getRange i
 
301
    getRange (App i _ _)           = getRange i
 
302
    getRange (WithApp i _ _)       = getRange i
 
303
    getRange (Lam i _ _)           = getRange i
 
304
    getRange (AbsurdLam i _)       = getRange i
 
305
    getRange (ExtendedLam i _ _ _) = getRange i
 
306
    getRange (Pi i _ _)            = getRange i
 
307
    getRange (Fun i _ _)           = getRange i
 
308
    getRange (Set i _)             = getRange i
 
309
    getRange (Prop i)              = getRange i
 
310
    getRange (Let i _ _)           = getRange i
 
311
    getRange (Rec i _)             = getRange i
 
312
    getRange (RecUpdate i _ _)     = getRange i
 
313
    getRange (ETel tel)            = getRange tel
 
314
    getRange (ScopedExpr _ e)      = getRange e
 
315
    getRange (QuoteGoal _ _ e)     = getRange e
 
316
    getRange (Quote i)             = getRange i
 
317
    getRange (QuoteTerm i)         = getRange i
 
318
    getRange (Unquote i)           = getRange i
 
319
    getRange (DontCare{})          = noRange
 
320
    getRange (PatternSyn x)        = getRange x
220
321
 
221
322
instance HasRange Declaration where
222
 
    getRange (Axiom      i _ _ _       ) = getRange i
223
 
    getRange (Field      i _ _         ) = getRange i
224
 
    getRange (Mutual     i _           ) = getRange i
225
 
    getRange (Section    i _ _ _       ) = getRange i
226
 
    getRange (Apply      i _ _ _ _     ) = getRange i
227
 
    getRange (Import     i _           ) = getRange i
228
 
    getRange (Primitive  i _ _         ) = getRange i
229
 
    getRange (Pragma     i _           ) = getRange i
230
 
    getRange (Open       i _           ) = getRange i
231
 
    getRange (ScopedDecl _ d           ) = getRange d
232
 
    getRange (FunDef  i _ _         ) = getRange i
233
 
    getRange (DataSig i _ _ _       ) = getRange i
234
 
    getRange (DataDef i _ _ _       ) = getRange i
235
 
    getRange (RecSig  i _ _ _       ) = getRange i
236
 
    getRange (RecDef  i _ _ _ _ _   ) = getRange i
 
323
    getRange (Axiom      i _ _ _    ) = getRange i
 
324
    getRange (Field      i _ _      ) = getRange i
 
325
    getRange (Mutual     i _        ) = getRange i
 
326
    getRange (Section    i _ _ _    ) = getRange i
 
327
    getRange (Apply      i _ _ _ _  ) = getRange i
 
328
    getRange (Import     i _        ) = getRange i
 
329
    getRange (Primitive  i _ _      ) = getRange i
 
330
    getRange (Pragma     i _        ) = getRange i
 
331
    getRange (Open       i _        ) = getRange i
 
332
    getRange (ScopedDecl _ d        ) = getRange d
 
333
    getRange (FunDef     i _ _ _    ) = getRange i
 
334
    getRange (DataSig    i _ _ _    ) = getRange i
 
335
    getRange (DataDef    i _ _ _    ) = getRange i
 
336
    getRange (RecSig     i _ _ _    ) = getRange i
 
337
    getRange (RecDef   i _ _ _ _ _ _) = getRange i
237
338
 
238
339
instance HasRange (Pattern' e) where
239
 
    getRange (VarP x)      = getRange x
240
 
    getRange (ConP i _ _)  = getRange i
241
 
    getRange (DefP i _ _)  = getRange i
242
 
    getRange (WildP i)     = getRange i
243
 
    getRange (ImplicitP i) = getRange i
244
 
    getRange (AsP i _ _)   = getRange i
245
 
    getRange (DotP i _)    = getRange i
246
 
    getRange (AbsurdP i)   = getRange i
247
 
    getRange (LitP l)      = getRange l
 
340
    getRange (VarP x)            = getRange x
 
341
    getRange (ConP i _ _)        = getRange i
 
342
    getRange (DefP i _ _)        = getRange i
 
343
    getRange (WildP i)           = getRange i
 
344
    getRange (ImplicitP i)       = getRange i
 
345
    getRange (AsP i _ _)         = getRange i
 
346
    getRange (DotP i _)          = getRange i
 
347
    getRange (AbsurdP i)         = getRange i
 
348
    getRange (LitP l)            = getRange l
 
349
    getRange (PatternSynP i _ _) = getRange i
248
350
 
249
351
instance HasRange LHS where
250
 
    getRange (LHS i _ _ _) = getRange i
 
352
    getRange (LHS i _ _)   = getRange i
 
353
 
 
354
instance HasRange (LHSCore' e) where
 
355
    getRange (LHSHead f ps) = fuseRange f ps
 
356
    getRange (LHSProj d ps1 lhscore ps2) = d `fuseRange` ps1 `fuseRange` lhscore `fuseRange` ps2
251
357
 
252
358
instance HasRange Clause where
253
359
    getRange (Clause lhs rhs ds) = getRange (lhs,rhs,ds)
260
366
 
261
367
instance HasRange LetBinding where
262
368
    getRange (LetBind  i _ _ _ _     ) = getRange i
 
369
    getRange (LetPatBind  i _ _      ) = getRange i
263
370
    getRange (LetApply i _ _ _ _     ) = getRange i
264
371
    getRange (LetOpen  i _           ) = getRange i
265
372
 
 
373
-- setRange for patterns applies the range to the outermost pattern constructor
 
374
instance SetRange (Pattern' a) where
 
375
    setRange r (VarP x)             = VarP (setRange r x)
 
376
    setRange r (ConP _ ns as)       = ConP (PatRange r) (AmbQ $ map (setRange r) $ unAmbQ ns) as
 
377
    setRange r (DefP _ n as)        = DefP (PatRange r) (setRange r n) as
 
378
    setRange r (WildP _)            = WildP (PatRange r)
 
379
    setRange r (ImplicitP _)        = ImplicitP (PatRange r)
 
380
    setRange r (AsP _ n p)          = AsP (PatRange r) (setRange r n) p
 
381
    setRange r (DotP _ e)           = DotP (PatRange r) e
 
382
    setRange r (AbsurdP _)          = AbsurdP (PatRange r)
 
383
    setRange r (LitP l)             = LitP (setRange r l)
 
384
    setRange r (PatternSynP _ n as) = PatternSynP (PatRange r) (setRange r n) as
 
385
 
266
386
instance KillRange LamBinding where
267
387
  killRange (DomainFree h r x) = killRange1 (DomainFree h r) x
268
388
  killRange (DomainFull b)     = killRange1 DomainFull b
275
395
  killRange (TNoBind e)    = killRange1 TNoBind e
276
396
 
277
397
instance KillRange Expr where
278
 
  killRange (Var x)          = killRange1 Var x
279
 
  killRange (Def x)          = killRange1 Def x
280
 
  killRange (Con x)          = killRange1 Con x
281
 
  killRange (Lit l)          = killRange1 Lit l
282
 
  killRange (QuestionMark i) = killRange1 QuestionMark i
283
 
  killRange (Underscore  i)  = killRange1 Underscore i
284
 
  killRange (App i e1 e2)    = killRange3 App i e1 e2
285
 
  killRange (WithApp i e es) = killRange3 WithApp i e es
286
 
  killRange (Lam i b e)      = killRange3 Lam i b e
287
 
  killRange (AbsurdLam i h)  = killRange1 AbsurdLam i h
288
 
  killRange (ExtendedLam i name di pes) = killRange4 ExtendedLam i name di pes --(\_ -> ExtendedLam i def {-name di si-}) i pes
289
 
  killRange (Pi i a b)       = killRange3 Pi i a b
290
 
  killRange (Fun i a b)      = killRange3 Fun i a b
291
 
  killRange (Set i n)        = Set (killRange i) n
292
 
  killRange (Prop i)         = killRange1 Prop i
293
 
  killRange (Let i ds e)     = killRange3 Let i ds e
294
 
  killRange (Rec i fs)       = Rec (killRange i) (map (id -*- killRange) fs)
295
 
  killRange (RecUpdate i e fs) = RecUpdate (killRange i) (killRange e) (map (id -*- killRange) fs)
296
 
  killRange (ETel tel)       = killRange1 ETel tel
297
 
  killRange (ScopedExpr s e) = killRange1 (ScopedExpr s) e
298
 
  killRange (QuoteGoal i x e)= killRange3 QuoteGoal i x e
299
 
  killRange (Quote i)        = killRange1 Quote i
300
 
  killRange (QuoteTerm i)    = killRange1 QuoteTerm i
301
 
  killRange (Unquote i)      = killRange1 Unquote i
302
 
  killRange (DontCare e)     = DontCare e
 
398
  killRange (Var x)                = killRange1 Var x
 
399
  killRange (Def x)                = killRange1 Def x
 
400
  killRange (Con x)                = killRange1 Con x
 
401
  killRange (Lit l)                = killRange1 Lit l
 
402
  killRange (QuestionMark i)       = killRange1 QuestionMark i
 
403
  killRange (Underscore  i)        = killRange1 Underscore i
 
404
  killRange (App i e1 e2)          = killRange3 App i e1 e2
 
405
  killRange (WithApp i e es)       = killRange3 WithApp i e es
 
406
  killRange (Lam i b e)            = killRange3 Lam i b e
 
407
  killRange (AbsurdLam i h)        = killRange1 AbsurdLam i h
 
408
  killRange (ExtendedLam i n d ps) = killRange4 ExtendedLam i n d ps
 
409
  killRange (Pi i a b)             = killRange3 Pi i a b
 
410
  killRange (Fun i a b)            = killRange3 Fun i a b
 
411
  killRange (Set i n)              = Set (killRange i) n
 
412
  killRange (Prop i)               = killRange1 Prop i
 
413
  killRange (Let i ds e)           = killRange3 Let i ds e
 
414
  killRange (Rec i fs)             = Rec (killRange i) (map (id -*- killRange) fs)
 
415
  killRange (RecUpdate i e fs)     = RecUpdate (killRange i)
 
416
                                               (killRange e)
 
417
                                               (map (id -*- killRange) fs)
 
418
  killRange (ETel tel)             = killRange1 ETel tel
 
419
  killRange (ScopedExpr s e)       = killRange1 (ScopedExpr s) e
 
420
  killRange (QuoteGoal i x e)      = killRange3 QuoteGoal i x e
 
421
  killRange (Quote i)              = killRange1 Quote i
 
422
  killRange (QuoteTerm i)          = killRange1 QuoteTerm i
 
423
  killRange (Unquote i)            = killRange1 Unquote i
 
424
  killRange (DontCare e)           = DontCare e
 
425
  killRange (PatternSyn x)         = killRange1 PatternSyn x
303
426
 
304
427
instance KillRange Relevance where
305
428
  killRange rel = rel -- no range to kill
316
439
  killRange (Pragma     i a           ) = Pragma (killRange i) a
317
440
  killRange (Open       i x           ) = killRange2 Open       i x
318
441
  killRange (ScopedDecl a d           ) = killRange1 (ScopedDecl a) d
319
 
  killRange (FunDef  i a b       ) = killRange3 FunDef  i a b
320
 
  killRange (DataSig i a b c     ) = killRange3 DataSig i a b c
321
 
  killRange (DataDef i a b c     ) = killRange4 DataDef i a b c
322
 
  killRange (RecSig  i a b c     ) = killRange4 RecSig  i a b c
323
 
  killRange (RecDef  i a b c d e ) = killRange6 RecDef  i a b c d e
 
442
  killRange (FunDef  i a b c          ) = killRange4 FunDef  i a b c
 
443
  killRange (DataSig i a b c          ) = killRange4 DataSig i a b c
 
444
  killRange (DataDef i a b c          ) = killRange4 DataDef i a b c
 
445
  killRange (RecSig  i a b c          ) = killRange4 RecSig  i a b c
 
446
  killRange (RecDef  i a b c d e f    ) = killRange7 RecDef  i a b c d e f
324
447
 
325
448
instance KillRange ModuleApplication where
326
449
  killRange (SectionApp a b c  ) = killRange3 SectionApp a b c
330
453
  killRange (ThingWithFixity c f) = ThingWithFixity (killRange c) f
331
454
 
332
455
instance KillRange e => KillRange (Pattern' e) where
333
 
  killRange (VarP x)      = killRange1 VarP x
334
 
  killRange (ConP i a b)  = killRange3 ConP i a b
335
 
  killRange (DefP i a b)  = killRange3 DefP i a b
336
 
  killRange (WildP i)     = killRange1 WildP i
337
 
  killRange (ImplicitP i) = killRange1 ImplicitP i
338
 
  killRange (AsP i a b)   = killRange3 AsP i a b
339
 
  killRange (DotP i a)    = killRange2 DotP i a
340
 
  killRange (AbsurdP i)   = killRange1 AbsurdP i
341
 
  killRange (LitP l)      = killRange1 LitP l
 
456
  killRange (VarP x)            = killRange1 VarP x
 
457
  killRange (ConP i a b)        = killRange3 ConP i a b
 
458
  killRange (DefP i a b)        = killRange3 DefP i a b
 
459
  killRange (WildP i)           = killRange1 WildP i
 
460
  killRange (ImplicitP i)       = killRange1 ImplicitP i
 
461
  killRange (AsP i a b)         = killRange3 AsP i a b
 
462
  killRange (DotP i a)          = killRange2 DotP i a
 
463
  killRange (AbsurdP i)         = killRange1 AbsurdP i
 
464
  killRange (LitP l)            = killRange1 LitP l
 
465
  killRange (PatternSynP i a p) = killRange3 PatternSynP i a p
342
466
 
343
467
instance KillRange LHS where
344
 
  killRange (LHS i a b c) = killRange4 LHS i a b c
 
468
  killRange (LHS i a b)   = killRange3 LHS i a b
 
469
 
 
470
instance KillRange e => KillRange (LHSCore' e) where
 
471
  killRange (LHSHead a b)     = killRange2 LHSHead a b
 
472
  killRange (LHSProj a b c d) = killRange4 LHSProj a b c d
345
473
 
346
474
instance KillRange Clause where
347
475
  killRange (Clause lhs rhs ds) = killRange3 Clause lhs rhs ds
354
482
 
355
483
instance KillRange LetBinding where
356
484
  killRange (LetBind  i rel a b c   ) = killRange5 LetBind  i rel a b c
 
485
  killRange (LetPatBind i a b       ) = killRange3 LetPatBind i a b
357
486
  killRange (LetApply i a b c d     ) = killRange3 LetApply i a b c d
358
487
  killRange (LetOpen  i x           ) = killRange2 LetOpen  i x
359
488
 
 
489
instanceUniverseBiT' [] [t| (Declaration, QName)          |]
 
490
instanceUniverseBiT' [] [t| (Declaration, AmbiguousQName) |]
 
491
instanceUniverseBiT' [] [t| (Declaration, Expr)           |]
 
492
instanceUniverseBiT' [] [t| (Declaration, LetBinding)     |]
 
493
instanceUniverseBiT' [] [t| (Declaration, LamBinding)     |]
 
494
instanceUniverseBiT' [] [t| (Declaration, TypedBinding)   |]
 
495
instanceUniverseBiT' [] [t| (Declaration, Pattern)        |]
 
496
instanceUniverseBiT' [] [t| (Declaration, Declaration)    |]
 
497
instanceUniverseBiT' [] [t| (Declaration, ModuleName)     |]
 
498
instanceUniverseBiT' [] [t| (Declaration, ModuleInfo)     |]
 
499
 
360
500
------------------------------------------------------------------------
361
501
-- Queries
362
502
------------------------------------------------------------------------
374
514
allNames (DataSig _ q _ _)        = Seq.singleton q
375
515
allNames (DataDef _ q _ decls)    = q <| Fold.foldMap allNames decls
376
516
allNames (RecSig _ q _ _)         = Seq.singleton q
377
 
allNames (RecDef _ q c _ _ decls) =
 
517
allNames (RecDef _ q _ c _ _ decls) =
378
518
  q <| foldMap Seq.singleton c >< Fold.foldMap allNames decls
379
 
allNames (FunDef _ q cls)         = q <| Fold.foldMap allNamesC cls
 
519
allNames (FunDef _ q _ cls)       = q <| Fold.foldMap allNamesC cls
380
520
  where
381
521
  allNamesC :: Clause -> Seq QName
382
522
  allNamesC (Clause _ rhs decls) = allNamesR rhs ><
418
558
  allNamesE QuoteTerm {}            = Seq.empty
419
559
  allNamesE Unquote {}              = Seq.empty
420
560
  allNamesE DontCare {}             = Seq.empty
 
561
  allNamesE (PatternSyn x)          = Seq.empty
421
562
 
422
563
  allNamesLam :: LamBinding -> Seq QName
423
564
  allNamesLam DomainFree {}      = Seq.empty
429
570
 
430
571
  allNamesLet :: LetBinding -> Seq QName
431
572
  allNamesLet (LetBind _ _ _ e1 e2)  = Fold.foldMap allNamesE [e1, e2]
 
573
  allNamesLet (LetPatBind _ _ e)     = allNamesE e
432
574
  allNamesLet (LetApply _ _ app _ _) = allNamesApp app
433
575
  allNamesLet LetOpen {}             = Seq.empty
434
576
 
435
577
  allNamesApp :: ModuleApplication -> Seq QName
436
578
  allNamesApp (SectionApp bindss _ es) = Fold.foldMap allNamesBinds bindss ><
437
 
                                         Fold.foldMap allNamesE (map (namedThing . unArg) es)
 
579
                                         Fold.foldMap allNamesE (map namedArg es)
438
580
  allNamesApp RecordModuleIFS {}       = Seq.empty
439
581
 
440
582
allNames (Section _ _ _ decls) = Fold.foldMap allNames decls
462
604
  anyAbstract = Fold.any anyAbstract
463
605
 
464
606
instance AnyAbstract Declaration where
465
 
  anyAbstract (Axiom i _ _ _)     = defAbstract i == AbstractDef
466
 
  anyAbstract (Field i _ _)       = defAbstract i == AbstractDef
467
 
  anyAbstract (Mutual     _ ds)   = anyAbstract ds
468
 
  anyAbstract (ScopedDecl _ ds)   = anyAbstract ds
469
 
  anyAbstract (Section _ _ _ ds)  = anyAbstract ds
470
 
  anyAbstract (FunDef i _ _)       = defAbstract i == AbstractDef
471
 
  anyAbstract (DataDef i _ _ _)    = defAbstract i == AbstractDef
472
 
  anyAbstract (RecDef i _ _ _ _ _) = defAbstract i == AbstractDef
473
 
  anyAbstract (DataSig i _ _ _)    = defAbstract i == AbstractDef
474
 
  anyAbstract (RecSig i _ _ _)     = defAbstract i == AbstractDef
475
 
  anyAbstract _                    = __IMPOSSIBLE__
476
 
 
 
607
  anyAbstract (Axiom i _ _ _)        = defAbstract i == AbstractDef
 
608
  anyAbstract (Field i _ _)          = defAbstract i == AbstractDef
 
609
  anyAbstract (Mutual     _ ds)      = anyAbstract ds
 
610
  anyAbstract (ScopedDecl _ ds)      = anyAbstract ds
 
611
  anyAbstract (Section _ _ _ ds)     = anyAbstract ds
 
612
  anyAbstract (FunDef i _ _ _)       = defAbstract i == AbstractDef
 
613
  anyAbstract (DataDef i _ _ _)      = defAbstract i == AbstractDef
 
614
  anyAbstract (RecDef i _ _ _ _ _ _) = defAbstract i == AbstractDef
 
615
  anyAbstract (DataSig i _ _ _)      = defAbstract i == AbstractDef
 
616
  anyAbstract (RecSig i _ _ _)       = defAbstract i == AbstractDef
 
617
  anyAbstract _                      = __IMPOSSIBLE__
 
618
 
 
619
app   = foldl (App (ExprRange noRange))
 
620
 
 
621
patternToExpr :: Pattern -> Expr
 
622
patternToExpr (VarP x)            = Var x
 
623
patternToExpr (ConP _ c ps)       =
 
624
          Con c `app` map (fmap (fmap patternToExpr)) ps
 
625
patternToExpr (DefP _ f ps)       =
 
626
          Def f `app` map (fmap (fmap patternToExpr)) ps
 
627
patternToExpr (WildP _)           = Underscore emptyMetaInfo
 
628
patternToExpr (AsP _ _ p)         = patternToExpr p
 
629
patternToExpr (DotP _ e)          = e
 
630
patternToExpr (AbsurdP _)         = Underscore emptyMetaInfo  -- TODO: could this happen?
 
631
patternToExpr (LitP l)            = Lit l
 
632
patternToExpr (ImplicitP _)       = Underscore emptyMetaInfo
 
633
patternToExpr (PatternSynP _ _ _) = __IMPOSSIBLE__
 
634
 
 
635
type PatternSynDefn = ([Name], Pattern)
 
636
type PatternSynDefns = Map QName PatternSynDefn
 
637
 
 
638
lambdaLiftExpr :: [Name] -> Expr -> Expr
 
639
lambdaLiftExpr []     e = e
 
640
lambdaLiftExpr (n:ns) e = Lam (ExprRange noRange)
 
641
                                     (DomainFree NotHidden Relevant n) $
 
642
                                     lambdaLiftExpr ns e
 
643
 
 
644
substPattern :: [(Name, Pattern)] -> Pattern -> Pattern
 
645
substPattern s p = case p of
 
646
  VarP z      -> case lookup z s of
 
647
    Nothing -> p
 
648
    Just x  -> x
 
649
  ConP i q ps -> ConP i q (fmap (fmap (fmap (substPattern s))) ps)
 
650
  WildP i     -> p
 
651
  DotP i e    -> DotP i (substExpr (map (fmap patternToExpr) s) e)
 
652
  AbsurdP i   -> p
 
653
  LitP l      -> p
 
654
  _           -> __IMPOSSIBLE__ -- Implicits (generated at TC time),
 
655
                                -- pattern synonyms (already gone), and
 
656
                                -- @-patterns (not supported anyways).
 
657
 
 
658
substExpr :: [(Name, Expr)] -> Expr -> Expr
 
659
substExpr s e = case e of
 
660
  Var n -> case lookup n s of
 
661
    Nothing -> e
 
662
    Just z  -> z
 
663
  Def _                 -> e
 
664
  Con _                 -> e
 
665
  Lit _                 -> e
 
666
  QuestionMark _        -> e
 
667
  Underscore   _        -> e
 
668
  App  i e e'           -> App i (substExpr s e)
 
669
                                 (fmap (fmap (substExpr s)) e')
 
670
  WithApp i e es        -> WithApp i (substExpr s e)
 
671
                                     (fmap (substExpr s) es)
 
672
  Lam  i lb e           -> Lam i lb (substExpr s e)
 
673
  AbsurdLam i h         -> e
 
674
  ExtendedLam i di n cs -> __IMPOSSIBLE__   -- Maybe later...
 
675
  Pi   i t e            -> Pi i (fmap (substTypedBindings s) t)
 
676
                                (substExpr s e)
 
677
  Fun  i ae e           -> Fun i (fmap (substExpr s) ae)
 
678
                                 (substExpr s e)
 
679
  Set  i n              -> e
 
680
  Prop i                -> e
 
681
  Let  i ls e           -> Let i (fmap (substLetBinding s) ls)
 
682
                                 (substExpr s e)
 
683
  ETel t                -> e
 
684
  Rec  i nes            -> Rec i (fmap (fmap (substExpr s)) nes)
 
685
  RecUpdate i e nes     -> RecUpdate i (substExpr s e)
 
686
                                       (fmap (fmap (substExpr s)) nes)
 
687
  -- XXX: Do we need to do more with ScopedExprs?
 
688
  ScopedExpr si e       -> ScopedExpr si (substExpr s e)
 
689
  QuoteGoal i n e       -> QuoteGoal i n (substExpr s e)
 
690
  Quote i               -> e
 
691
  QuoteTerm i           -> e
 
692
  Unquote i             -> e
 
693
  DontCare e            -> DontCare (substExpr s e)
 
694
  PatternSyn x          -> e
 
695
 
 
696
substLetBinding :: [(Name, Expr)] -> LetBinding -> LetBinding
 
697
substLetBinding s lb = case lb of
 
698
  LetBind i r n e e' -> LetBind i r n (substExpr s e) (substExpr s e')
 
699
  LetPatBind i p e   -> LetPatBind i p (substExpr s e) -- Andreas, 2012-06-04: what about the pattern p
 
700
  _                  -> lb
 
701
 
 
702
substTypedBindings :: [(Name, Expr)] -> TypedBindings -> TypedBindings
 
703
substTypedBindings s (TypedBindings r atb) = TypedBindings r
 
704
    (fmap (substTypedBinding s) atb)
 
705
 
 
706
substTypedBinding :: [(Name, Expr)] -> TypedBinding -> TypedBinding
 
707
substTypedBinding s tb = case tb of
 
708
  TBind r ns e -> TBind r ns $ substExpr s e
 
709
  TNoBind e    -> TNoBind $ substExpr s e