← Back to branch summary

~ubuntu-branches/ubuntu/utopic/agda-stdlib/utopic-proposed

« back to all changes in this revision

Viewing changes to src/Reflection.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 09:46:46 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805094646-zqd0c4m8ndngqg6x
Tags: 0.8-1
* [4ca6fd0] Update debian/watch to fetch tarballs from github
* [84d4313] Imported Upstream version 0.8
* [7b08243] debian/control: Require agda 2.4.x per upstream
* [37e7e10] debian/control: Standards-Version → 3.9.5, no changes required.
* [9051b9d] Run upstream's "GenerateEverything" script

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Reflection.agda
71
71
 
72
72
-- Arguments.
73
73
 
74
 
data Arg A : Set where
75
 
  arg : (v : Visibility) (r : Relevance) (x : A) → Arg A
76
 
 
77
 
{-# BUILTIN ARG    Arg #-}
78
 
{-# BUILTIN ARGARG arg #-}
 
74
data Arg-info : Set where
 
75
  arg-info : (v : Visibility) (r : Relevance) → Arg-info
 
76
 
 
77
data Arg (A : Set) : Set where
 
78
  arg : (i : Arg-info) (x : A) → Arg A
 
79
 
 
80
{-# BUILTIN ARGINFO    Arg-info #-}
 
81
{-# BUILTIN ARGARGINFO arg-info #-}
 
82
{-# BUILTIN ARG        Arg      #-}
 
83
{-# BUILTIN ARGARG     arg      #-}
79
84
 
80
85
-- Terms.
81
86
 
191
196
           x ≡ y × u ≡ v × r ≡ s → f x u r ≡ f y v s
192
197
  cong₃′ f (refl , refl , refl) = refl
193
198
 
194
 
  arg₁ : ∀ {A v v′ r r′} {x x′ : A} → arg v r x ≡ arg v′ r′ x′ → v ≡ v′
 
199
  arg₁ : ∀ {A i i′} {x x′ : A} → arg i x ≡ arg i′ x′ → i ≡ i′
195
200
  arg₁ refl = refl
196
201
 
197
 
  arg₂ : ∀ {A v v′ r r′} {x x′ : A} → arg v r x ≡ arg v′ r′ x′ → r ≡ r′
 
202
  arg₂ : ∀ {A i i′} {x x′ : A} → arg i x ≡ arg i′ x′ → x ≡ x′
198
203
  arg₂ refl = refl
199
204
 
200
 
  arg₃ : ∀ {A v v′ r r′} {x x′ : A} → arg v r x ≡ arg v′ r′ x′ → x ≡ x′
201
 
  arg₃ refl = refl
 
205
  arg-info₁ : ∀ {v v′ r r′} → arg-info v r ≡ arg-info v′ r′ → v ≡ v′
 
206
  arg-info₁ refl = refl
 
207
 
 
208
  arg-info₂ : ∀ {v v′ r r′} → arg-info v r ≡ arg-info v′ r′ → r ≡ r′
 
209
  arg-info₂ refl = refl
202
210
 
203
211
  cons₁ : ∀ {A : Set} {x y} {xs ys : List A} → x ∷ xs ≡ y ∷ ys → x ≡ y
204
212
  cons₁ refl = refl
268
276
relevant   ≟-Relevance irrelevant = no λ()
269
277
irrelevant ≟-Relevance relevant   = no λ()
270
278
 
 
279
_≟-Arg-info_ : Decidable (_≡_ {A = Arg-info})
 
280
arg-info v r ≟-Arg-info arg-info v′ r′ =
 
281
  Dec.map′ (cong₂′ arg-info)
 
282
           < arg-info₁ , arg-info₂ >
 
283
           (v ≟-Visibility v′ ×-dec r ≟-Relevance r′)
 
284
 
271
285
mutual
272
286
  infix 4 _≟_ _≟-Args_ _≟-ArgType_
273
287
 
274
288
  _≟-ArgTerm_ : Decidable (_≡_ {A = Arg Term})
275
 
  arg e r a ≟-ArgTerm arg e′ r′ a′ =
276
 
    Dec.map′ (cong₃′ arg)
277
 
             < arg₁ , < arg₂ , arg₃ > >
278
 
             (e ≟-Visibility e′ ×-dec r ≟-Relevance r′ ×-dec a ≟ a′)
 
289
  arg i a ≟-ArgTerm arg i′ a′ =
 
290
    Dec.map′ (cong₂′ arg)
 
291
             < arg₁ , arg₂ >
 
292
             (i ≟-Arg-info i′ ×-dec a ≟ a′)
279
293
 
280
294
  _≟-ArgType_ : Decidable (_≡_ {A = Arg Type})
281
 
  arg e r a ≟-ArgType arg e′ r′ a′ =
282
 
    Dec.map′ (cong₃′ arg)
283
 
             < arg₁ , < arg₂ , arg₃ > >
284
 
             (e ≟-Visibility e′ ×-dec
285
 
              r ≟-Relevance r′  ×-dec
286
 
              a ≟-Type a′)
 
295
  arg i a ≟-ArgType arg i′ a′ =
 
296
    Dec.map′ (cong₂′ arg)
 
297
             < arg₁ , arg₂ >
 
298
             (i ≟-Arg-info i′ ×-dec a ≟-Type a′)
287
299
 
288
300
  _≟-Args_ : Decidable (_≡_ {A = List (Arg Term)})
289
301
  []       ≟-Args []       = yes refl