Mercurial > hg > Members > atton > delta_monad

annotate agda/patterns.rb @ 95:cf372fbcebd8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix implicit values in deltaM-mu
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 19 Jan 2015 17:47:55 +0900
parents f9c9207c40b7
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
61
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 #!/usr/bin/env ruby
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 require 'pry'
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 # Agda {{{
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 Agda = %q(
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import list
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import basic
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Level
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import Relation.Binary.PropositionalEquality
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open ≡-Reasoning
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 module hoge where
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 data Delta {l : Level} (A : Set l) : (Set (suc l)) where
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 mono : A -> Delta A
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 delta : A -> Delta A -> Delta A
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 deltaAppend : {l : Level} {A : Set l} -> Delta A -> Delta A -> Delta A
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 deltaAppend (mono x) d = delta x d
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 deltaAppend (delta x d) ds = delta x (deltaAppend d ds)
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 headDelta : {l : Level} {A : Set l} -> Delta A -> Delta A
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 headDelta (mono x) = mono x
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 headDelta (delta x _) = mono x
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 tailDelta : {l : Level} {A : Set l} -> Delta A -> Delta A
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 tailDelta (mono x) = mono x
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 tailDelta (delta _ d) = d
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 -- Functor
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Delta A) -> (Delta B)
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 fmap f (mono x) = mono (f x)
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 fmap f (delta x d) = delta (f x) (fmap f d)
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 -- Monad (Category)
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 eta : {l : Level} {A : Set l} -> A -> Delta A
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 eta x = mono x
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 bind : {l ll : Level} {A : Set l} {B : Set ll} -> (Delta A) -> (A -> Delta B) -> Delta B
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 bind (mono x) f = f x
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 bind (delta x d) f = deltaAppend (headDelta (f x)) (bind d (tailDelta ∙ f))
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 -- can not apply id. because different Level
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 mu d = bind d id
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 returnS : {l : Level} {A : Set l} -> A -> Delta A
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 returnS x = mono x
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 returnSS : {l : Level} {A : Set l} -> A -> A -> Delta A
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 returnSS x y = deltaAppend (returnS x) (returnS y)
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 -- Monad (Haskell)
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 return : {l : Level} {A : Set l} -> A -> Delta A
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 return = eta
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 _>>=_ : {l ll : Level} {A : Set l} {B : Set ll} ->
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 (x : Delta A) -> (f : A -> (Delta B)) -> (Delta B)
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 (mono x) >>= f = f x
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 (delta x d) >>= f = deltaAppend (headDelta (f x)) (d >>= (tailDelta ∙ f))
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 -- proofs
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 -- Functor-laws
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 -- Functor-law-1 : T(id) = id'
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 functor-law-1 : {l : Level} {A : Set l} -> (d : Delta A) -> (fmap id) d ≡ id d
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 functor-law-1 (mono x) = refl
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 functor-law-1 (delta x d) = cong (delta x) (functor-law-1 d)
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 -- Functor-law-2 : T(f . g) = T(f) . T(g)
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 functor-law-2 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 (f : B -> C) -> (g : A -> B) -> (d : Delta A) ->
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 (fmap (f ∙ g)) d ≡ ((fmap f) ∙ (fmap g)) d
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 functor-law-2 f g (mono x) = refl
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d)
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 -- Monad-laws (Category)
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 {-
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 monad-law-1-sub : {l : Level} {A : Set l} -> (x : Delta (Delta A)) (d : Delta (Delta (Delta A)))
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 -> deltaAppend (headDelta (bind x id)) (bind (fmap mu d) (tailDelta ∙ id)) ≡ bind (deltaAppend (headDelta x) (bind d (tailDelta ∙ id))) id
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 monad-law-1-sub (mono x) (mono (mono (mono x₁))) = refl
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 monad-law-1-sub (mono x) (mono (mono (delta x₁ d))) = refl
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 monad-law-1-sub (mono x) (mono (delta d d1)) = begin
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 deltaAppend (headDelta (bind (mono x) id)) (bind (fmap mu (mono (delta d d1))) (tailDelta ∙ id))
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 ≡⟨ refl ⟩
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 deltaAppend (headDelta (bind (mono x) id)) (bind ((mono (mu (delta d d1)))) (tailDelta ∙ id))
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 ≡⟨ refl ⟩
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 deltaAppend (headDelta (bind (mono x) id)) (bind (mono (bind (delta d d1) id)) (tailDelta ∙ id))
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 ≡⟨ refl ⟩
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 deltaAppend (headDelta (mu (mono x))) (((tailDelta ∙ id) (mu (delta d d1))))
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 ≡⟨ refl ⟩
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 deltaAppend (headDelta (mu (mono x))) (((tailDelta ∙ id) (bind (delta d d1) id)))
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 ≡⟨ {!!} ⟩
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 deltaAppend (headDelta (mu (mono x))) (((tailDelta ∙ id) (bind (delta d d1) id)))
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 -- bind (delta (mu (mono x)) (mono (mu (delta d d1)))) id
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 ≡⟨ {!!} ⟩
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 bind (deltaAppend (headDelta (mono x)) (bind (mono (delta d d1)) (tailDelta ∙ id))) id
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 ∎
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 monad-law-1-sub (delta x x₁) (mono d) = {!!}
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 monad-law-1-sub x (delta d d1) = begin
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 deltaAppend (headDelta (bind x id)) (bind (fmap mu (delta d d1)) (tailDelta ∙ id))
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 ≡⟨ {!!} ⟩
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 bind (deltaAppend (headDelta x) (bind (delta d d1) (tailDelta ∙ id))) id
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 ∎
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 -}
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 -- monad-law-1 : join . fmap join = join . join
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 monad-law-1 : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) -> ((mu ∙ (fmap mu)) d) ≡ ((mu ∙ mu) d)
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 )
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 # }}}
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 Rules = {
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 'T3' => ['(mono T2)', '(delta T2 T3)'],
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 'T2' => ['(mono T1)', '(delta T1 T2)'],
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 'T1' => ['(mono _)', '(delta _ T1)']
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 }
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 def generate_patterns source_patterns, operations
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 patterns = source_patterns.clone
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 operations.each do |op|
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 patterns = Rules[op].flat_map do |r|
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 patterns.flat_map{|p| p.gsub(op, r)}
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 end
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 end
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141 patterns.uniq
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 end
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 def pattern_formatter non_format_patterns
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 formatted_patterns = non_format_patterns.clone
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 Rules.keys.each do |k|
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148 formatted_patterns.map!{|p| p.gsub(k, '_')}
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 end
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 formatted_patterns
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152 end
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154 def generate_function function_name, patterns, body
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155 patterns.map do |p|
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
156 "#{function_name} #{p} = #{body}"
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157 end
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158 end
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160 def generate_agda function_body
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 Agda + function_body.join("\n")
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162 end
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
163
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
164
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
165
68
f9c9207c40b7 Trying prove monad-law-1 by another pattern ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
166 patterns = ['(delta T2 (delta T2 (delta T2 _)))']
f9c9207c40b7 Trying prove monad-law-1 by another pattern ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
167 operations = ['T2'].cycle(2).to_a + ['T1'].cycle(4).to_a
61
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
168
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
169
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
170 patterns = generate_patterns(patterns, operations)
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
171
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
172 puts patterns.size
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
173 function_body = generate_function('monad-law-1', pattern_formatter(patterns), 'refl')
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
174 agda = generate_agda(function_body)
18a0520445df Add patterns generator
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
175 File.open('hoge.agda', 'w').write(agda)
68
f9c9207c40b7 Trying prove monad-law-1 by another pattern ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
176 binding.pry