← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to test/succeed/Reflection.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
test/succeed/Reflection.agda
1
 
{-# OPTIONS --universe-polymorphism #-}
2
 
module Reflection where
3
 
 
4
 
open import Common.Prelude hiding (Unit; module Unit) renaming (Nat to ℕ)
5
 
open import Common.Reflect
6
 
 
7
 
data _≡_ {a}{A : Set a}(x : A) : A → Set a where
8
 
  refl : x ≡ x
9
 
 
10
 
{-# BUILTIN EQUALITY _≡_ #-}
11
 
{-# BUILTIN REFL refl #-}
12
 
 
13
 
data Id {A : Set}(x : A) : (B : Set) → B → Set where
14
 
  course : Id x A x
15
 
 
16
 
primitive
17
 
  primTrustMe : ∀{a}{A : Set a}{x y : A} → x ≡ y
18
 
 
19
 
open import Common.Level
20
 
 
21
 
unEl : Type → Term
22
 
unEl (el _ t) = t
23
 
 
24
 
argᵛʳ : ∀{A} → A → Arg A
25
 
argᵛʳ = arg visible relevant
26
 
 
27
 
argʰʳ : ∀{A} → A → Arg A
28
 
argʰʳ = arg hidden relevant
29
 
 
30
 
el₀ : Term → Type
31
 
el₀ = el (lit 0)
32
 
 
33
 
el₁ : Term → Type
34
 
el₁ = el (lit 1)
35
 
 
36
 
set₀ : Type
37
 
set₀ = el₁ (sort (lit 0))
38
 
 
39
 
unCheck : Term → Term
40
 
unCheck (def x (_ ∷ _ ∷ arg _ _ t ∷ [])) = t
41
 
unCheck t = unknown
42
 
 
43
 
mutual
44
 
  data Check {a}{A : Set a}(x : A) : Set where
45
 
    _is_of_ : (t t′ : Term) →
46
 
              Id (primTrustMe {x = unCheck t} {t′}
47
 
                 )
48
 
                 (t′ ≡ t′) refl → Check x
49
 
 
50
 
  `Check : QName
51
 
  `Check = quote Check
52
 
 
53
 
test₁ : Check ({A : Set} → A → A)
54
 
test₁ = quoteGoal t in
55
 
        t is pi (argʰʳ set₀) (el₀ (pi (argᵛʳ (el₀ (var 0 []))) (el₀ (var 1 []))))
56
 
        of course
57
 
 
58
 
test₂ : (X : Set) → Check (λ (x : X) → x)
59
 
test₂ X = quoteGoal t in
60
 
          t is lam visible (var 0 []) of course
61
 
 
62
 
infixr 40 _`∷_
63
 
 
64
 
_`∷_ : Term → Term → Term
65
 
x `∷ xs = con (quote _∷_) (argᵛʳ x ∷ argᵛʳ xs ∷ [])
66
 
`[]     = con (quote []) []
67
 
`true   = con (quote true) []
68
 
`false  = con (quote false) []
69
 
 
70
 
test₃ : Check (true ∷ false ∷ [])
71
 
test₃ = quoteGoal t in
72
 
        t is `true `∷ `false `∷ `[] of course
73
 
 
74
 
`List : Term → Term
75
 
`List A = def (quote List) (argᵛʳ A ∷ [])
76
 
`ℕ      = def (quote ℕ) []
77
 
 
78
 
`Term : Term
79
 
`Term = def (quote Term) []
80
 
`Type : Term
81
 
`Type = def (quote Type) []
82
 
`Sort : Term
83
 
`Sort = def (quote Sort) []
84
 
 
85
 
test₄ : Check (List ℕ)
86
 
test₄ = quoteGoal t in
87
 
        t is `List `ℕ of course
88
 
 
89
 
test₅ : primQNameType (quote Term) ≡ set₀
90
 
test₅ = refl
91
 
 
92
 
test₆ : unEl (primQNameType (quote set₀)) ≡ `Type
93
 
test₆ = refl
94
 
 
95
 
test₇ : primQNameType (quote Sort.lit) ≡ el₀ (pi (argᵛʳ (el₀ `ℕ)) (el₀ `Sort))
96
 
test₇ = refl
97
 
 
98
 
mutual
99
 
  ℕdef : DataDef
100
 
  ℕdef = _
101
 
 
102
 
  test₈ : dataDef ℕdef ≡ primQNameDefinition (quote ℕ)
103
 
  test₈ = refl
104
 
 
105
 
test₉ : primDataConstructors ℕdef ≡ quote ℕ.zero ∷ quote ℕ.suc ∷ []
106
 
test₉ = refl
107
 
 
108
 
test₁₀ : primQNameDefinition (quote ℕ.zero) ≡ dataConstructor
109
 
test₁₀ = refl
110
 
 
111
 
postulate
112
 
  a : ℕ
113
 
 
114
 
test₁₁ : primQNameDefinition (quote a) ≡ axiom
115
 
test₁₁ = refl
116
 
 
117
 
test₁₂ : primQNameDefinition (quote primQNameDefinition) ≡ prim
118
 
test₁₂ = refl
119
 
 
120
 
record Unit : Set where
121
 
 
122
 
mutual
123
 
  UnitDef : RecordDef
124
 
  UnitDef = _
125
 
 
126
 
  test₁₃ : recordDef UnitDef ≡ primQNameDefinition (quote Unit)
127
 
  test₁₃ = refl
128
 
 
129
 
test₁₄ : Check 1
130
 
test₁₄ = quoteGoal t in
131
 
           t is con (quote ℕ.suc) (argᵛʳ (con (quote ℕ.zero) []) ∷ [])
132
 
           of course