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

comparison reflection-ex.agda @ 1:6f01428aaf2d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 26 Mar 2019 18:02:06 +0900
parents 776f851a03a3
children
comparison
equal deleted inserted replaced
0:776f851a03a3 1:6f01428aaf2d
16 nameOfNat = quote ℕ 16 nameOfNat = quote ℕ
17 17
18 isNat : Name → Bool 18 isNat : Name → Bool
19 isNat (quote ℕ) = true 19 isNat (quote ℕ) = true
20 isNat _ = false 20 isNat _ = false
21
22 lemma1 = isNat (quote ℕ)
23 lemma10 = isNat (quote isNat)
24 -- quote Set is not work
21 25
22 postulate Meta : Set 26 postulate Meta : Set
23 {-# BUILTIN AGDAMETA Meta #-} 27 {-# BUILTIN AGDAMETA Meta #-}
24 28
25 primitive 29 primitive
46 {-# BUILTIN AGDALITFLOAT float #-} 50 {-# BUILTIN AGDALITFLOAT float #-}
47 {-# BUILTIN AGDALITCHAR char #-} 51 {-# BUILTIN AGDALITCHAR char #-}
48 {-# BUILTIN AGDALITSTRING string #-} 52 {-# BUILTIN AGDALITSTRING string #-}
49 {-# BUILTIN AGDALITQNAME name #-} 53 {-# BUILTIN AGDALITQNAME name #-}
50 {-# BUILTIN AGDALITMETA meta #-} 54 {-# BUILTIN AGDALITMETA meta #-}
55
56 lemma11 : ℕ -> Literal
57 lemma11 n = nat n
51 58
52 data Visibility : Set where 59 data Visibility : Set where
53 visible hidden instance′ : Visibility 60 visible hidden instance′ : Visibility
54 61
55 {-# BUILTIN HIDING Visibility #-} 62 {-# BUILTIN HIDING Visibility #-}
320 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym ) 327 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
321 328
322 thm : (a b : ℕ) → plus-to-times (a + b) ≡ a * b 329 thm : (a b : ℕ) → plus-to-times (a + b) ≡ a * b
323 thm a b = refl 330 thm a b = refl
324 331
332 to-term : List ℕ → Term
333 to-term [] = con (quote List.[]) []
334 to-term (h ∷ t) = con (quote List._∷_)
335 ( arg (arg-info visible relevant ) (lit (nat h ))
336 ∷ ( arg (arg-info visible relevant ) (to-term t) )
337 ∷ [] )
338
339 varlistArgs : List (Arg Term ) → List ℕ → List ℕ
340
341 varlistPattern : List (Arg Pattern ) → ℕ → List ℕ → List ℕ
342 varlistPattern [] n vars = vars
343 varlistPattern (arg i (con c ps) ∷ t) n vars = varlistPattern t n (varlistPattern ps n vars)
344 varlistPattern (arg i dot ∷ t) n vars = varlistPattern t n vars
345 varlistPattern (arg i (var s) ∷ t) n vars = varlistPattern t (suc n) vars
346 varlistPattern (arg i (lit l) ∷ t) n vars = varlistPattern t n vars
347 varlistPattern (arg i (proj f) ∷ t) n vars = varlistPattern t n vars
348 varlistPattern (arg i absurd ∷ t) n vars = varlistPattern t n vars
349
350 varlist1 : Term → List ℕ → List ℕ
351 varlist1 (var n args ) vars = ( n ∷ vars )
352 varlist1 (con c args) vars = varlistArgs args vars
353 varlist1 (def f args) vars = varlistArgs args ( 11 ∷ vars )
354 varlist1 (lam v (abs s x)) vars = varlist1 x vars
355 varlist1 (pat-lam cs args) vars = varlistArgs args vars
356 varlist1 (pi a b) vars = vars
357 varlist1 (agda-sort s) vars = vars
358 varlist1 (lit l) vars = vars
359 varlist1 (meta x args) vars = varlistArgs args vars
360 varlist1 unknown vars = vars
361
362 varlistArgs [] vars = vars
363 varlistArgs (arg i x ∷ rest) vars =
364 varlistArgs rest ( varlist1 x vars )
365
366 macro
367 varlist : Term → Term → TC ⊤
368 varlist term hole =
369 unify hole ( to-term ( varlist1 term [] ) )
370
371 t0 = varlist ℕ
372 t1 = \ x y -> varlist ( varlist1 x y )
373 t2 = varlist ( \ (x : Term ) (y : List ℕ ) -> varlist1 x y ) -- is normalized as varlist1 which has no variables
374 t3 = varlist ( \ ( x y : ℕ ) -> (x , y) )
375 t4 = \{A : Set} -> \ (x y : A ) -> varlist (\ (z : A -> A ) -> z y)
376 -- t4' = \{A : Set} -> \ (x y : A ) -> varlist (\ z -> z y)
377 t5 = \ (x y : ℕ )-> varlist ( x , y )
378
379 -- copy_term : Set → Set
380 -- copy_term = ?
381
382 -- lemma : {A : Set} -> (x y : A) -> (p : A -> A ) -> copy_term ( p x ) ≡ p y
383
325 postulate magic : Type → Term 384 postulate magic : Type → Term
326 385
327 macro 386 macro
328 by-magic : Term → TC ⊤ 387 by-magic : Term → TC ⊤
329 by-magic hole = 388 by-magic hole =
372 bindTC 431 bindTC
373 ( quoteTC ({A : Set} (x : A) → A) ) 432 ( quoteTC ({A : Set} (x : A) → A) )
374 ( λ ty → bindTC (declareDef (arg (arg-info visible relevant) id-name) ty ) 433 ( λ ty → bindTC (declareDef (arg (arg-info visible relevant) id-name) ty )
375 ( λ _ → defId id-name) ) 434 ( λ _ → defId id-name) )
376 435
377 lemma1 : ( x : Name ) → mkId x ≡ mkId' x 436 lemma2 : ( x : Name ) → mkId x ≡ mkId' x
378 lemma1 x = refl 437 lemma2 x = refl
379 438
380 unquoteDecl id′ = mkId id′ 439 unquoteDecl id′ = mkId id′