-
Notifications
You must be signed in to change notification settings - Fork 7
/
rewrite.m
282 lines (223 loc) · 12.2 KB
/
rewrite.m
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
# tree rewrite
https://en.wikipedia.org/wiki/Rewriting
# {| a; | b} --> a | {| b}
# tree_bar recurses into tree_bar, not exps or exp, else:
# | a; (| b; | c)
# --> | a; op_if ...
# but (| b; | c) is rewritten with op_if rule below, and that cannot be simplify further to have a | b | c
# : Exps
tree_bar : Exp? Exp =
spot, Binary (_, Pre '|' a) ';' b? spot, Binary a '|' b
a? a
# a, (b, c) -> a, b, c
# a, ((b, c)) -> a, (b, c)
pair_row : Exp? Exps =
_, Binary a ',' b? a, pair_row b
_, Tree [a]? [a] # special for last node - a,b, c,d -> ((a, b), (c, d))
a? [a]
pair_seq : Exp? Exp =
spot, Binary a ',' b? spot, Row_ [a, b.pair_seq]
_, Tree [a]? a
a? a
exps0 s:Exps : Exps = s exp
exps s:Exps : Exps = s exp + !nameless_funs
exp a:Exp : Exp = a.do_exp1.do_exp2
do_exp1 exp=spot,term:Exp : Exp =
term .
Pre o a? spot, Pre o a.do_exp1
Post a o? spot, Post a.do_exp1 o
Binary a o b? o .
','? spot, Row_ (List.map (pair_row exp) do_exp1) # a, (b, c) -> a, b, c
? spot, Binary a.do_exp1 o b.do_exp1
Tree [(_, Name 'List'), a]? spot, Listy a.pair_seq.do_exp1
Tree s? spot, Tree do_exp1.s
Row s? spot, Row_ do_exp1.s
? exp
do_exps2 : Exps? Exps =
(_, Tree r), s? do_exps2 r+s
# x = f a
# | x & ((y, z) = x; g y z)
# | h 0
#
# -->
#
# f a .
# (y, z)? g y z
# ? h 0
# match rule sequence - {(a? b; c) d} === eq {a} {d} & b | {c d}
# if (a == d) b {c d}
[(_, Binary (spot, Binary rule '?' body) ';' also), arg]? # ;-exp recursion
bind, arg2 = Exp.bind_name arg
else = spot, Tree [also, arg2]
[exp (Rule.bind_exp bind (spot, Binary (Rule.rewrite rule body arg2) '|' else))]
[(spot, Binary rule '?' body), arg]? # ;-exp base
bind, arg2 = Exp.bind_name arg
[exp (Rule.bind_exp bind (Rule.rewrite rule body arg2))]
[(spot, Pre '?' body), arg]? # _?a -> ?a
bind, arg2 = Exp.bind_name arg
[exp (Rule.bind_exp bind (Rule.rewrite (spot, Name '_') body arg2))]
s? s exp
# seq of all bindings across ; - else, [x,y = a,b; c] -> [(x=a; y=b); c] not [x=a; (y=b; c)]
do_exp_exps2 exp=spot,term:Exp : Exps = term .
# https://en.wikipedia.org/wiki/Guard_(computer_science)
# consecutive conditionals: | a; | b; | c --> a | (b | c)
# {; (| 0 a) (| 0 b)} --> {| 0 (| a b)}
Binary (_, Pre '|' _) ';' _? [do_exp2 (tree_bar exp)]
Binary a ';' b? do_exp_exps2 a + do_exp_exps2 b
Binary (_, Row s) '=' a?
bind, body = Exp.bind_name a
tests, binds = List.map_at s (Rule.test_bind_row body,!s) 0 . List.unzip # fixme - need tests?
List.map (Opt.add bind binds.List.adds) do_exp2
? [do_exp_exp2 exp]
do_exp2 exp:Exp : Exp = Opt.get (Exp.binary_exps ';' (do_exp_exps2 exp)) $Fun
# https://en.wikipedia.org/wiki/Anonymous_function
# https://en.wikipedia.org/wiki/Closure_(computer_programming)
# https://en.wikipedia.org/wiki/Partial_application
nameless_funs = %0 : %Exps
arg_vars _,e:Exp : *S = e .
Binary (_, Name x) ':' _? [x]
# Binary (_, (Binary (_, Name x) ',' (_, Name y))) ':' _? [x, y]
Binary (_, (Row s)) ':' _? List.map_opt_rev s (_ : Exp? !S = (_, Name x)? x)
# todo
# 1. ignore the function itself, need names in lexical scope during typing in Type.m to determine if f or X.f are free variable, todo for higher-order functions REWRITE_FREE_VARS_FUN
# 2. also local top-level in the unit, such as Thread.lock in Thread.main REWRITE_FREE_VARS_LOCAL
# 3. also need to done rewriting ((a . X) . y) -> X.y a in do_exp2 do_exp_exps2 before [free_vars], see REWRITE_UNIT_NAME
# 4. need types of free variables to rewrite into full function def - f x:t in [do_exp_exp2] below
# free_vars s:*S e=_,m:Exp : *S = m .
# Rewrite.NAME_BUG: some varialbe names such as [p] with local functions cause crashes, or [h] in parameter
free_vars s:*S e=_,m:Exp : *Exp = m .
Name x & S.is_lower x? ! List.in S.eq s x & [e]
Pre _ a? free_vars s a
Post a _? free_vars s a
Binary (_, Name _) '.' _? []
Binary (_, Binary (_, Name x) '=' a) ';' b? free_vars s a + free_vars x,s b
Binary (_, Binary (_, Row r) '=' _) ';' a? free_vars (List.add (List.map_opt_rev r (_ : Exp? !S = (_, Name x)? x)) s) a
Binary (_, Binary a '.' (_, Name x)) '.' (_, Name _) & S.is_capital x? free_vars s a # REWRITE_UNIT_NAME
Binary (_, Binary (_, Tree (_, Name '_'),args) ':' _) '=' body? free_vars (List.add (List.map_add args arg_vars) s) body # inside function, same as REWRITE_NAMELESS below
Binary a ':' _? free_vars s a
Binary a _ b? List.add (free_vars s a) (free_vars s b)
Tree _,r? List.map_add r (free_vars s)
Row r? List.map_add r (free_vars s)
_? []
do_exp_exp2 spot,term:Exp : Exp = term .
Pre '|' a? do_exp2 a # | a -> a
Pre '?' body? # nameless local function
free = free_vars [] body
args = [(spot, Binary (spot, Name '_') ':' (spot, Name '_'))]
all_args = (free & List.map free (_ x:Exp : Exp = spot, Binary x ':' (spot, Name 'Any'))) + args
name = spot, Name 'f'.S.tick
#free & (Tree name,all_args) . Term.log
Ref.seq_add nameless_funs
do_exp2 # f _:_ : 0 = a where the type is Any, not Z
spot, Binary
spot, Binary
spot, Tree name,all_args
':'
(spot, Name 'Z')
'='
body
# free & (spot, Tree name,free | name) . Exp.log
free & spot, Tree name,free | name # f x:t y:u @ free y
Pre '$' a=(spot2, Str _)? spot, Row_ [(spot, Pre '$' (spot2, Name 'Spot')), a] # $'foo' -> $Spot, 'foo'
Pre o a? spot, Pre o (do_exp2 a)
# see REWRITE_REAL2 for disabling this rewrite
# Post (_, Nat x) '.'? spot, Real (R.of1 x) # REWRITE_REAL
Post a o? spot, Post (do_exp2 a) o
Listy a? spot, Listy (do_exp2 a)
Tree (_, Binary (_, Name 'List') '.' (_, Name 'adds_')),s? # TYPE_VARARG - List.adds_ a b c -> List.adds [a, b, c]
do_exp2 (spot, Tree [(spot, Name2 'List' 'adds'), Exp.seq_row1 s+[(spot, Nat 0)]])
Tree (_, Binary (_, Name 'Seq') '.' (_, Name 'adds_')),s? # TYPE_VARARG - Seq.adds_ a b c -> Seq.adds [a, b, c]
do_exp2 (spot, Tree [(spot, Name2 'Seq' 'adds'), Exp.seq_row1 s+[(spot, Nat 0)]])
Tree (_, Binary (_, Name 'B') '.' (_, Name 'or')),s? # TYPE_VARARG - B.or a b c -> a | (b | c)
do_exp2 (Opt.get (Exp.binary_exps '|' s) $Fun)
Tree [a, (_, Name '²')]? do_exp2 (spot, Binary a '^' (spot, Real 2.)) # a² -> a^2
Tree [a, (spot2, Name '√'), b]? do_exp2 (spot, Binary a '*' (spot, Tree [(spot2, Name2 'R' '√'), b])) # a√b -> a * (√b)
Tree [a, (spot2, Name 'ϕ'), b]? do_exp2 (spot, Binary a '*' (spot, Tree [(spot2, Name2 'R' 'ϕ'), b])) # aϕb -> a * (ϕb)
Tree s? Group.exps_exp (do_exps2 s)
# cannot use [y] to represent the fractional part of a real due to leading zeros, else: 0.0016 becomes 0,016 -> 0.22
# Binary (_, Nat x) '.' (_, Nat y)? spot, Real (R.of2 x y) # REWRITE_REAL2
# unit fullname X . y -> X.y
Binary (_, Name x) '.' (_, Name y) & S.is_capital x? spot, Name2 x y
# REWRITE_UNIT_NAME long unit fullname a.X.y -> ((a . X) . y) -> X.y a
Binary (_, Binary a '.' (_, Name x)) '.' (_, Name y) & S.is_capital x? Group.exps_exp (do_exps2 [(spot, Name2 x y), a])
# REWRITE_INFIX
# a .f b -> (a (. f) b) -> f a b
# f a b . g d e -> (f a b (. g) d e) -> (g (f a b) d e)
# reverse apply
# x.f -> f x
# f a b . g d e -> (g d e (f a b))
Binary a '.' b? Group.exps_exp (do_exps2 [b, a])
# generated by Rule.tests_binds, but not user source code
Binary (_, Binary a '&' b) '|' c? # a & b | c --> if a b c
Group.exps_exp (do_exps2 [(spot, Name 'op_if'), a, b, c])
Binary a '|' b? # a | b -> x = a; if x x b
# bind, c = Exp.bind_name a
# exp (Rule.bind_exp bind (spot, Tree [(spot, Name 'op_if'), c, c, b]))
do_exp2 (spot, Tree [(spot, Name 'op_if0'), a, b])
Binary a '&' b? # a & b --> if a b 0
Group.exps_exp (do_exps2 [((spot, Name 'op_if')), a, b, (spot, Nat 0)])
Binary (spot2, Tree fun) '=' body? # default nil return type - f x:t = a -> f x:t = a
do_exp2 (spot, Binary (spot2, Binary (spot2, Tree fun) ':' (spot2, Name 'Z')) '=' body)
# todo, _ in multi args - f x:t _ : u = a -> f x:t _:Z : u = a
Binary (spot1, Binary (spot2, Tree [name, (spot3, Name '_')]) ':' return) '=' body? # default nil argument type - f _ : t = a -> f _ : t = a
do_exp2 (spot, Binary (spot1, Binary (spot2, Tree [name, (spot3, Binary spot3,Name'_' ':' spot3,Name'Z')]) ':' return) '=' body)
# eta expand for match rule
# {f = (a? b)} === {f x = (a? b) x}
# {f = (a? b; c)} === {f x = (a? b; c) x}
# f : t?u = (a? b) -> f x:t : u = (a? b) x
Binary (_, Binary fun ':' (_, Binary arg_type '?' return_type)) '=' body & Exp.is_fun body?
arg = spot, Name 'x'.S.tick
typed_arg = spot, Binary arg ':' arg_type
fun2 = fun.Exp.tree .
Tree name_args? Tree name_args+[typed_arg] # f y.. x:t
Name name? Tree [fun, typed_arg] # f x:t
? Exp.seq_error $Fun 'invalid fun' [(spot, term)]
body2 = spot, Tree [body, arg] # (a? b) x
do_exp2 (spot, Binary (spot, Binary (spot, fun2) ':' return_type) '=' body2) # f y.. x:t : u = (a? b) x
Binary (_, Binary (_, Tree (_, Name '_'),args) ':' type) '=' body? # REWRITE_NAMELESS _ x:t : u = a -> f$n x:t : u = a
name = spot, Name 'f'.S.tick
free = free_vars (List.map_add args arg_vars) body
all_args = (free & List.map free (_ x:Exp : Exp = spot, Binary x ':' (spot, Name 'Any'))) + args
Ref.seq_add nameless_funs (spot, Binary (spot, Binary (spot, Tree name,all_args) ':' type) '=' body).do_exp2
free & spot, Tree name,free | name # f x:t y:u @ free y
# f x,y:t : u = a
# f z:t : u = (x,y = z; a)
Binary (_, Binary (_, Tree name,params) ':' return) '=' body? # todo - skip if params = simple var
params2, bind_list = params Rule.binds . List.unzip
body2 = Exp.binary_exps ';' bind_list.List.adds+[body]
# todo - nto do_exp2 around the whole exp because the pattern is always applied (even without pair)
spot, Binary (spot, Binary (spot, Tree name,params2).do_exp2 ':' return.do_exp2) '=' body2.do_exp2
Binary a o b? spot, Binary (do_exp2 a) o (do_exp2 b) # [a; b] and [x,.. = a] already handled in do_exp_exps2
Row s? spot, Row_ (s do_exp2)
# todo - Name -> Str or Real
Name '½'? spot, Real 1./2.
Name '⅓'? spot, Real 1./3.
Name '¼'? spot, Real 1./4.
# Name 'ℯ'? spot, Real (R.exp 1.)
# Name 'π'? spot, Real 3.14159265358979323846264338327950288
? spot, term
Fact (1 . (1? 42) == 42)
Fact (41,1 . (x, 1? x + 2) == 43)
Fact (A . ((x = A)? x) == A)
Fact (A . ((x = A)? x; (x = B_)? x) == A)
Fact (B_ . ((x = A)? x; (x = B_)? x) == B_)
of x:S : S = x.Exp.str_exps.Group.exps.exps.0.Exp.str
Fact (of '42' == '42')
Fact (of '"foo"' == "'foo'")
Fact (of 'a' == 'a')
Fact (of 'a+b' == '(a + b)')
Fact (of 'a,b' == '(a,b)')
Fact (of 'f a,b' == '(f (a,b))')
Fact (of 'a,b' == '(a,b)')
Fact (of 'a,b,c' == '(a,b,c)')
Fact (of 'a,b, c,d' == '((a,b),(c,d))')
Fact (of 'a,(b,c)' == '(a,(b,c))')
Fact (of 'a, (f b, c)' == '(a,((f b),c))')
Fact (of 'x = a, b' == '(x = (a,b))')
Fact (of '[a,b]' == '[a, b]')
Fact (of '[a,b,c]' == '[a, b, c]')
Fact (of '[a,(b,c)]' == '[a, (b,c)]')
Fact (of '[a,b, c,d]' == '[(a,b), (c,d)]')
Fact (of '[0.a]' == '[(a 0)]') # rewrite after listy
Fact (of 'a+b' == '(a + b)')
Fact (of 'f a+b' == '(f (a + b))')