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