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
;; Example showing how to use multisets to hold associative & commutative operations
(datatype*
(Math
(Num i64)
(Var String)
(Add Math Math)
(Mul Math Math)
(Product MathMultiSet)
(Sum MathMultiSet))
(sort MathToMath (UnstableFn (Math) Math))
(sort MathMultiSet (MultiSet Math)))
;; expr1 = 2 * (x + 3)
(let $expr1 (Mul (Num 2) (Add (Var "x") (Num 3))))
;; expr2 = 6 + 2 * x
(let $expr2 (Add (Num 6) (Mul (Num 2) (Var "x"))))
(rewrite (Add a b) (Sum (multiset-of a b)))
(rewrite (Mul a b) (Product (multiset-of a b)))
;; 0 or 1 elements sums/products also can be extracted back to numbers
(rule
(
(= sum (Sum sum-inner))
(= 0 (multiset-length sum-inner))
)
((union sum (Num 0)))
)
(rule
(
(= sum (Sum sum-inner))
(= 1 (multiset-length sum-inner))
)
((union sum (multiset-pick sum-inner)))
)
(rule
(
(= product (Product product-inner))
(= 0 (multiset-length product-inner))
)
((union product (Num 1)))
)
(rule
(
(= product (Product product-inner))
(= 1 (multiset-length product-inner))
)
((union product (multiset-pick product-inner)))
)
; (rewrite (Mul a (Add b c))
; (Add (Mul a b) (Mul a c)))
; -> we would like to write it like this, but cannot (yet) bc we can't match on the inner structure of the multisets
; and we don't support anonymous functions
; (rewrite (Product (multiset-insert a (Sum bc)))
; (Sum (multiset-map (lambda (x) (Product (multiset-insert a x))) bc)))
;; so instead we can define a function and partially apply it to get the same function as the lambda
(constructor tmp-fn (MathMultiSet Math) Math)
(rewrite (tmp-fn xs x) (Product (multiset-insert xs x)))
(rule
(
;; and we can do a cross product search of all possible pairs of products/sums to find one we want
(= sum (Sum bc))
(= product (Product product-inner))
(multiset-contains product-inner sum)
(> (multiset-length product-inner) 1)
(= a (multiset-remove product-inner sum))
)
(
(union product (Sum
(unstable-multiset-map
(unstable-fn "tmp-fn" a)
bc)
))
)
)
; (rewrite (Add (Num a) (Num b))
; (Num (+ a b)))
(rule
(
(= sum (Sum sum-inner))
(= num-a (Num a))
(multiset-contains sum-inner num-a)
(= without-a (multiset-remove sum-inner num-a))
(= num-b (Num b))
(multiset-contains without-a num-b)
)
(
(union sum
(Sum (multiset-insert (multiset-remove without-a num-b) (Num (+ a b))))
)
)
)
; (rewrite (Mul (Num a) (Num b))
; (Num (* a b)))
(rule
(
(= product (Product product-inner))
(= num-a (Num a))
(multiset-contains product-inner num-a)
(= without-a (multiset-remove product-inner num-a))
(= num-b (Num b))
(multiset-contains without-a num-b)
)
(
(union product
(Product (multiset-insert (multiset-remove without-a num-b) (Num (* a b))))
)
)
)
(run 100)
(check (= $expr1 $expr2))