Mercurial > hg > Members > kono > Proof > agda-reflection

comparison reflection-ex.agda @ 0:776f851a03a3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reflection and tactics
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 15 Mar 2019 17:35:46 +0900
parents
children 6f01428aaf2d
comparison
equal deleted inserted replaced
-1:000000000000 0:776f851a03a3
1 module reflection-ex where
2
3 open import Data.Bool
4 open import Data.String
5 open import Data.Nat
6
7 postulate Name : Set
8 {-# BUILTIN QNAME Name #-}
9
10 primitive
11 primQNameEquality : Name → Name → Bool
12 primQNameLess : Name → Name → Bool
13 primShowQName : Name → String
14
15 nameOfNat : Name
16 nameOfNat = quote ℕ
17
18 isNat : Name → Bool
19 isNat (quote ℕ) = true
20 isNat _ = false
21
22 postulate Meta : Set
23 {-# BUILTIN AGDAMETA Meta #-}
24
25 primitive
26 primMetaEquality : Meta → Meta → Bool
27 primMetaLess : Meta → Meta → Bool
28 primShowMeta : Meta → String
29
30 open import Data.Word
31 open import Data.Float
32 open import Data.Char
33
34 data Literal : Set where
35 nat : (n : ℕ) → Literal
36 word64 : (n : Word64) → Literal
37 float : (x : Float) → Literal
38 char : (c : Char) → Literal
39 string : (s : String) → Literal
40 name : (x : Name) → Literal
41 meta : (x : Meta) → Literal
42
43 {-# BUILTIN AGDALITERAL Literal #-}
44 {-# BUILTIN AGDALITNAT nat #-}
45 {-# BUILTIN AGDALITWORD64 word64 #-}
46 {-# BUILTIN AGDALITFLOAT float #-}
47 {-# BUILTIN AGDALITCHAR char #-}
48 {-# BUILTIN AGDALITSTRING string #-}
49 {-# BUILTIN AGDALITQNAME name #-}
50 {-# BUILTIN AGDALITMETA meta #-}
51
52 data Visibility : Set where
53 visible hidden instance′ : Visibility
54
55 {-# BUILTIN HIDING Visibility #-}
56 {-# BUILTIN VISIBLE visible #-}
57 {-# BUILTIN HIDDEN hidden #-}
58 {-# BUILTIN INSTANCE instance′ #-}
59
60 data Relevance : Set where
61 relevant irrelevant : Relevance
62
63 {-# BUILTIN RELEVANCE Relevance #-}
64 {-# BUILTIN RELEVANT relevant #-}
65 {-# BUILTIN IRRELEVANT irrelevant #-}
66
67 data ArgInfo : Set where
68 arg-info : (v : Visibility) (r : Relevance) → ArgInfo
69
70 data Arg (A : Set) : Set where
71 arg : (i : ArgInfo) (x : A) → Arg A
72
73 {-# BUILTIN ARGINFO ArgInfo #-}
74 {-# BUILTIN ARGARGINFO arg-info #-}
75 {-# BUILTIN ARG Arg #-}
76 {-# BUILTIN ARGARG arg #-}
77
78
79 open import Data.List
80
81 data Pattern : Set where
82 con : (c : Name) (ps : List (Arg Pattern)) → Pattern
83 dot : Pattern
84 var : (s : String) → Pattern
85 lit : (l : Literal) → Pattern
86 proj : (f : Name) → Pattern
87 absurd : Pattern
88
89 {-# BUILTIN AGDAPATTERN Pattern #-}
90 {-# BUILTIN AGDAPATCON con #-}
91 {-# BUILTIN AGDAPATDOT dot #-}
92 {-# BUILTIN AGDAPATVAR var #-}
93 {-# BUILTIN AGDAPATLIT lit #-}
94 {-# BUILTIN AGDAPATPROJ proj #-}
95 {-# BUILTIN AGDAPATABSURD absurd #-}
96
97 data Abs (A : Set) : Set where
98 abs : (s : String) (x : A) → Abs A
99
100 {-# BUILTIN ABS Abs #-}
101 {-# BUILTIN ABSABS abs #-}
102
103 data Term : Set
104 data Sort : Set
105 data Clause : Set
106 Type = Term
107
108 data Term where
109 var : (x : ℕ) (args : List (Arg Term)) → Term
110 con : (c : Name) (args : List (Arg Term)) → Term
111 def : (f : Name) (args : List (Arg Term)) → Term
112 lam : (v : Visibility) (t : Abs Term) → Term
113 pat-lam : (cs : List Clause) (args : List (Arg Term)) → Term
114 pi : (a : Arg Type) (b : Abs Type) → Term
115 agda-sort : (s : Sort) → Term
116 lit : (l : Literal) → Term
117 meta : (x : Meta) → List (Arg Term) → Term
118 unknown : Term -- Treated as '_' when unquoting.
119
120 data Sort where
121 set : (t : Term) → Sort -- A Set of a given (possibly neutral) level.
122 lit : (n : ℕ) → Sort -- A Set of a given concrete level.
123 unknown : Sort
124
125 data Clause where
126 clause : (ps : List (Arg Pattern)) (t : Term) → Clause
127 absurd-clause : (ps : List (Arg Pattern)) → Clause
128
129 {-# BUILTIN AGDASORT Sort #-}
130 {-# BUILTIN AGDATERM Term #-}
131 {-# BUILTIN AGDACLAUSE Clause #-}
132
133 {-# BUILTIN AGDATERMVAR var #-}
134 {-# BUILTIN AGDATERMCON con #-}
135 {-# BUILTIN AGDATERMDEF def #-}
136 {-# BUILTIN AGDATERMMETA meta #-}
137 {-# BUILTIN AGDATERMLAM lam #-}
138 {-# BUILTIN AGDATERMEXTLAM pat-lam #-}
139 {-# BUILTIN AGDATERMPI pi #-}
140 {-# BUILTIN AGDATERMSORT agda-sort #-}
141 {-# BUILTIN AGDATERMLIT lit #-}
142 {-# BUILTIN AGDATERMUNSUPPORTED unknown #-}
143
144 {-# BUILTIN AGDASORTSET set #-}
145 {-# BUILTIN AGDASORTLIT lit #-}
146 {-# BUILTIN AGDASORTUNSUPPORTED unknown #-}
147
148 {-# BUILTIN AGDACLAUSECLAUSE clause #-}
149 {-# BUILTIN AGDACLAUSEABSURD absurd-clause #-}
150
151 data Definition : Set where
152 function : (cs : List Clause) → Definition
153 data-type : (pars : ℕ) (cs : List Name) → Definition -- parameters and constructors
154 record-type : (c : Name) (fs : List (Arg Name)) → -- c: name of record constructor
155 Definition -- fs: fields
156 data-cons : (d : Name) → Definition -- d: name of data type
157 axiom : Definition
158 prim-fun : Definition
159
160 {-# BUILTIN AGDADEFINITION Definition #-}
161 {-# BUILTIN AGDADEFINITIONFUNDEF function #-}
162 {-# BUILTIN AGDADEFINITIONDATADEF data-type #-}
163 {-# BUILTIN AGDADEFINITIONRECORDDEF record-type #-}
164 {-# BUILTIN AGDADEFINITIONDATACONSTRUCTOR data-cons #-}
165 {-# BUILTIN AGDADEFINITIONPOSTULATE axiom #-}
166 {-# BUILTIN AGDADEFINITIONPRIMITIVE prim-fun #-}
167
168 -- Error messages can contain embedded names and terms.
169 data ErrorPart : Set where
170 strErr : String → ErrorPart
171 termErr : Term → ErrorPart
172 nameErr : Name → ErrorPart
173
174 {-# BUILTIN AGDAERRORPART ErrorPart #-}
175 {-# BUILTIN AGDAERRORPARTSTRING strErr #-}
176 {-# BUILTIN AGDAERRORPARTTERM termErr #-}
177 {-# BUILTIN AGDAERRORPARTNAME nameErr #-}
178
179 postulate
180 TC : ∀ {a} → Set a → Set a
181 returnTC : ∀ {a} {A : Set a} → A → TC A
182 bindTC : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B
183
184
185 {-# BUILTIN AGDATCM TC #-}
186 {-# BUILTIN AGDATCMRETURN returnTC #-}
187 {-# BUILTIN AGDATCMBIND bindTC #-}
188
189 open import Data.Unit
190 open import Data.Product
191
192 postulate
193 -- Unify two terms, potentially solving metavariables in the process.
194 unify : Term → Term → TC ⊤
195
196 -- Throw a type error. Can be caught by catchTC.
197 typeError : ∀ {a} {A : Set a} → List ErrorPart → TC A
198
199 -- Block a type checking computation on a metavariable. This will abort
200 -- the computation and restart it (from the beginning) when the
201 -- metavariable is solved.
202 blockOnMeta : ∀ {a} {A : Set a} → Meta → TC A
203
204 -- Prevent current solutions of metavariables from being rolled back in
205 -- case 'blockOnMeta' is called.
206 commitTC : TC ⊤
207
208 -- Backtrack and try the second argument if the first argument throws a
209 -- type error.
210 catchTC : ∀ {a} {A : Set a} → TC A → TC A → TC A
211
212 -- Infer the type of a given term
213 inferType : Term → TC Type
214
215 -- Check a term against a given type. This may resolve implicit arguments
216 -- in the term, so a new refined term is returned. Can be used to create
217 -- new metavariables: newMeta t = checkType unknown t
218 checkType : Term → Type → TC Term
219
220 -- Compute the normal form of a term.
221 normalise : Term → TC Term
222
223 -- Compute the weak head normal form of a term.
224 reduce : Term → TC Term
225 -- Get the current context. Returns the context in reverse order, so that
226 -- it is indexable by deBruijn index. Note that the types in the context are
227 -- valid in the rest of the context. To use in the current context they need
228 -- to be weakened by 1 + their position in the list.
229 getContext : TC (List (Arg Type))
230
231 -- Extend the current context with a variable of the given type.
232 extendContext : ∀ {a} {A : Set a} → Arg Type → TC A → TC A
233
234 -- Set the current context. Takes a context telescope with the outer-most
235 -- entry first, in contrast to 'getContext'. Each type should be valid in the
236 -- context formed by the preceding elements in the list.
237 inContext : ∀ {a} {A : Set a} → List (Arg Type) → TC A → TC A
238
239 -- Quote a value, returning the corresponding Term.
240 quoteTC : ∀ {a} {A : Set a} → A → TC Term
241
242 -- Unquote a Term, returning the corresponding value.
243 unquoteTC : ∀ {a} {A : Set a} → Term → TC A
244
245 -- Create a fresh name.
246 freshName : String → TC Name
247
248 -- Declare a new function of the given type. The function must be defined
249 -- later using 'defineFun'. Takes an Arg Name to allow declaring instances
250 -- and irrelevant functions. The Visibility of the Arg must not be hidden.
251 declareDef : Arg Name → Type → TC ⊤
252
253 -- Declare a new postulate of the given type. The Visibility of the Arg
254 -- must not be hidden. It fails when executed from command-line with --safe
255 -- option.
256 declarePostulate : Arg Name → Type → TC ⊤
257
258 -- Define a declared function. The function may have been declared using
259 -- 'declareDef' or with an explicit type signature in the program.
260 defineFun : Name → List Clause → TC ⊤
261
262 -- Get the type of a defined name. Replaces 'primNameType'.
263 getType : Name → TC Type
264
265 -- Get the definition of a defined name. Replaces 'primNameDefinition'.
266 getDefinition : Name → TC Definition
267
268 -- Check if a name refers to a macro
269 isMacro : Name → TC Bool
270
271 -- Change the behaviour of inferType, checkType, quoteTC, getContext
272 -- to normalise (or not) their results. The default behaviour is no
273 -- normalisation.
274 withNormalisation : ∀ {a} {A : Set a} → Bool → TC A → TC A
275
276 -- Prints the third argument if the corresponding verbosity level is turned
277 -- on (with the -v flag to Agda).
278 debugPrint : String → ℕ → List ErrorPart → TC ⊤
279
280 -- Fail if the given computation gives rise to new, unsolved
281 -- "blocking" constraints.
282 noConstraints : ∀ {a} {A : Set a} → TC A → TC A
283
284 -- Run the given TC action and return the first component. Resets to
285 -- the old TC state if the second component is 'false', or keep the
286 -- new TC state if it is 'true'.
287 runSpeculative : ∀ {a} {A : Set a} → TC (Σ A λ _ → Bool) → TC A
288
289 {-# BUILTIN AGDATCMUNIFY unify #-}
290 {-# BUILTIN AGDATCMTYPEERROR typeError #-}
291 {-# BUILTIN AGDATCMBLOCKONMETA blockOnMeta #-}
292 {-# BUILTIN AGDATCMCATCHERROR catchTC #-}
293 {-# BUILTIN AGDATCMINFERTYPE inferType #-}
294 {-# BUILTIN AGDATCMCHECKTYPE checkType #-}
295 {-# BUILTIN AGDATCMNORMALISE normalise #-}
296 {-# BUILTIN AGDATCMREDUCE reduce #-}
297 {-# BUILTIN AGDATCMGETCONTEXT getContext #-}
298 {-# BUILTIN AGDATCMEXTENDCONTEXT extendContext #-}
299 {-# BUILTIN AGDATCMINCONTEXT inContext #-}
300 {-# BUILTIN AGDATCMQUOTETERM quoteTC #-}
301 {-# BUILTIN AGDATCMUNQUOTETERM unquoteTC #-}
302 {-# BUILTIN AGDATCMFRESHNAME freshName #-}
303 {-# BUILTIN AGDATCMDECLAREDEF declareDef #-}
304 {-# BUILTIN AGDATCMDECLAREPOSTULATE declarePostulate #-}
305 {-# BUILTIN AGDATCMDEFINEFUN defineFun #-}
306 {-# BUILTIN AGDATCMGETTYPE getType #-}
307 {-# BUILTIN AGDATCMGETDEFINITION getDefinition #-}
308 {-# BUILTIN AGDATCMCOMMIT commitTC #-}
309 {-# BUILTIN AGDATCMISMACRO isMacro #-}
310 {-# BUILTIN AGDATCMWITHNORMALISATION withNormalisation #-}
311 {-# BUILTIN AGDATCMDEBUGPRINT debugPrint #-}
312 {-# BUILTIN AGDATCMNOCONSTRAINTS noConstraints #-}
313 {-# BUILTIN AGDATCMRUNSPECULATIVE runSpeculative #-}
314
315 macro
316 plus-to-times : Term → Term → TC ⊤
317 plus-to-times (def (quote _+_) (a ∷ b ∷ [])) hole = unify hole (def (quote _*_) (a ∷ b ∷ []))
318 plus-to-times v hole = unify hole v
319
320 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
321
322 thm : (a b : ℕ) → plus-to-times (a + b) ≡ a * b
323 thm a b = refl
324
325 postulate magic : Type → Term
326
327 macro
328 by-magic : Term → TC ⊤
329 by-magic hole =
330 bindTC (inferType hole) λ goal →
331 unify hole (magic goal)
332
333 open import Relation.Nullary
334
335 -- thm1 : {P NP : Set} → ¬ P ≡ NP
336 -- thm1 = ? by-magic
337
338 --unquoteDecl x₁ .. x ₙ = m
339 --unquoteDef x₁ .. x ₙ = m
340
341 -- Defining: id-name {A} x = x
342 defId : (id-name : Name) → TC ⊤
343 defId id-name = do
344 defineFun id-name
345 [ clause
346 ( arg (arg-info hidden relevant) (var "A")
347 ∷ arg (arg-info visible relevant) (var "x")
348 ∷ [] )
349 (var 0 [])
350 ]
351
352 id : {A : Set} (x : A) → A
353 unquoteDef id = defId id
354
355 open import Level renaming ( suc to succ ; zero to Zero )
356
357 mkId : (id-name : Name) → TC ⊤
358 mkId id-name =
359 do
360 ty ← quoteTC ({A : Set} (x : A) → A)
361 declareDef (arg (arg-info visible relevant) id-name) ty
362 defId id-name
363 where
364 _>>=_ : {a : Level} {B A : Set a} (m : TC B) (f : (x : B) → TC A) → TC A
365 _>>=_ = bindTC
366 _>>_ : {a : Level} {B A : Set a} (m : TC B) (m' : TC A) → TC A
367 _>>_ x y = bindTC x ( λ _ → y )
368
369
370 mkId' : (id-name : Name) → TC ⊤
371 mkId' id-name =
372 bindTC
373 ( quoteTC ({A : Set} (x : A) → A) )
374 ( λ ty → bindTC (declareDef (arg (arg-info visible relevant) id-name) ty )
375 ( λ _ → defId id-name) )
376
377 lemma1 : ( x : Name ) → mkId x ≡ mkId' x
378 lemma1 x = refl
379
380 unquoteDecl id′ = mkId id′