|
71 | 71 | #:attr obj (if (Object? o) o -empty-obj))) |
72 | 72 |
|
73 | 73 | ;; < <= >= = |
74 | | -(define (numeric-comparison-function prop-constructor) |
75 | | - (λ (args-stx result) |
76 | | - (syntax-parse args-stx |
77 | | - [((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int))) |
78 | | - (define p (prop-constructor (attribute e1.obj) (attribute e2.obj))) |
79 | | - (add-p/not-p result p)] |
80 | | - [((~var e1 (w/type -Int)) (~var e2 (w/type -Int)) (~var e3 (w/type -Int))) |
81 | | - #:when (or (and (Object? (attribute e1.obj)) (Object? (attribute e2.obj))) |
82 | | - (and (Object? (attribute e2.obj)) (Object? (attribute e3.obj)))) |
83 | | - (define p (-and (prop-constructor (attribute e1.obj) (attribute e2.obj)) |
84 | | - (prop-constructor (attribute e2.obj) (attribute e3.obj)))) |
85 | | - (add-p/not-p result p)] |
86 | | - [_ result]))) |
| 74 | +(define ((numeric-comparison-function prop-constructor) args-stx result) |
| 75 | + (syntax-parse args-stx |
| 76 | + [((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int))) |
| 77 | + (define p (prop-constructor (attribute e1.obj) (attribute e2.obj))) |
| 78 | + (add-p/not-p result p)] |
| 79 | + [((~var e1 (w/type -Int)) (~var e2 (w/type -Int)) (~var e3 (w/type -Int))) |
| 80 | + #:when (or (and (Object? (attribute e1.obj)) (Object? (attribute e2.obj))) |
| 81 | + (and (Object? (attribute e2.obj)) (Object? (attribute e3.obj)))) |
| 82 | + (define p |
| 83 | + (-and (prop-constructor (attribute e1.obj) (attribute e2.obj)) |
| 84 | + (prop-constructor (attribute e2.obj) (attribute e3.obj)))) |
| 85 | + (add-p/not-p result p)] |
| 86 | + [_ result])) |
87 | 87 |
|
88 | 88 | ;; +/- |
89 | | -(define (plus/minus plus?) |
90 | | - (λ (args-stx result) |
91 | | - (match result |
92 | | - [(tc-result1: ret-t ps orig-obj) |
93 | | - (syntax-parse args-stx |
94 | | - ;; +/- (2 args) |
95 | | - [((~var e1 (w/obj+type -Int)) |
96 | | - (~var e2 (w/obj+type -Int))) |
97 | | - (define (sign o) (if plus? o (scale-obj -1 o))) |
98 | | - (define l (-lexp (attribute e1.obj) (sign (attribute e2.obj)))) |
99 | | - (ret (-refine/fresh x ret-t (-eq (-lexp x) l)) |
100 | | - ps |
101 | | - l)] |
102 | | - ;; +/- (3 args) |
103 | | - [((~var e1 (w/obj+type -Int)) |
104 | | - (~var e2 (w/obj+type -Int)) |
105 | | - (~var e3 (w/obj+type -Int))) |
106 | | - (define (sign o) (if plus? o (scale-obj -1 o))) |
107 | | - (define l (-lexp (attribute e1.obj) (sign (attribute e2.obj)) (sign (attribute e3.obj)))) |
108 | | - (ret (-refine/fresh x ret-t (-eq (-lexp x) l)) |
109 | | - ps |
110 | | - l)] |
111 | | - [_ result])] |
112 | | - [_ result]))) |
| 89 | +(define ((plus/minus plus?) args-stx result) |
| 90 | + (match result |
| 91 | + [(tc-result1: ret-t ps orig-obj) |
| 92 | + (syntax-parse args-stx |
| 93 | + ;; +/- (2 args) |
| 94 | + [((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int))) |
| 95 | + (define (sign o) |
| 96 | + (if plus? |
| 97 | + o |
| 98 | + (scale-obj -1 o))) |
| 99 | + (define l (-lexp (attribute e1.obj) (sign (attribute e2.obj)))) |
| 100 | + (ret (-refine/fresh x ret-t (-eq (-lexp x) l)) ps l)] |
| 101 | + ;; +/- (3 args) |
| 102 | + [((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int)) (~var e3 (w/obj+type -Int))) |
| 103 | + (define (sign o) |
| 104 | + (if plus? |
| 105 | + o |
| 106 | + (scale-obj -1 o))) |
| 107 | + (define l (-lexp (attribute e1.obj) (sign (attribute e2.obj)) (sign (attribute e3.obj)))) |
| 108 | + (ret (-refine/fresh x ret-t (-eq (-lexp x) l)) ps l)] |
| 109 | + [_ result])] |
| 110 | + [_ result])) |
113 | 111 |
|
114 | 112 | ;; equal?/eqv?/eq? |
115 | 113 | ;; if only one side is a supported type, we can learn integer equality for |
116 | 114 | ;; a result of `#t`, whereas if both sides are of the supported type, |
117 | 115 | ;; we learn on both `#t` and `#f` answers |
118 | | -(define (equality-function supported-type) |
119 | | - (λ (args-stx result) |
120 | | - (syntax-parse args-stx |
121 | | - [((~var e1 (w/obj+type supported-type)) (~var e2 (w/obj+type supported-type))) |
122 | | - (define p (-eq (attribute e1.obj) (attribute e2.obj))) |
123 | | - (add-p/not-p result p)] |
124 | | - [((~var e1 (w/obj+type supported-type)) (~var e2 (w/obj+type Univ))) |
125 | | - (define p (-eq (attribute e1.obj) (attribute e2.obj))) |
126 | | - (add-to-pos-side result p)] |
127 | | - [((~var e1 (w/obj+type Univ)) (~var e2 (w/obj+type supported-type))) |
128 | | - (define p (-eq (attribute e1.obj) (attribute e2.obj))) |
129 | | - (add-to-pos-side result p)] |
130 | | - [_ result]))) |
| 116 | +(define ((equality-function supported-type) args-stx result) |
| 117 | + (syntax-parse args-stx |
| 118 | + [((~var e1 (w/obj+type supported-type)) (~var e2 (w/obj+type supported-type))) |
| 119 | + (define p (-eq (attribute e1.obj) (attribute e2.obj))) |
| 120 | + (add-p/not-p result p)] |
| 121 | + [((~var e1 (w/obj+type supported-type)) (~var e2 (w/obj+type Univ))) |
| 122 | + (define p (-eq (attribute e1.obj) (attribute e2.obj))) |
| 123 | + (add-to-pos-side result p)] |
| 124 | + [((~var e1 (w/obj+type Univ)) (~var e2 (w/obj+type supported-type))) |
| 125 | + (define p (-eq (attribute e1.obj) (attribute e2.obj))) |
| 126 | + (add-to-pos-side result p)] |
| 127 | + [_ result])) |
131 | 128 |
|
132 | 129 | ;; * |
133 | | -(define product-function |
134 | | - (λ (args-stx result) |
135 | | - (match result |
136 | | - [(tc-result1: ret-t ps orig-obj) |
137 | | - (syntax-parse args-stx |
138 | | - [((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int))) |
139 | | - (define product-obj (-obj* (attribute e1.obj) (attribute e2.obj))) |
140 | | - (cond |
141 | | - [(Object? product-obj) |
142 | | - (ret (-refine/fresh x ret-t (-eq (-lexp x) product-obj)) |
143 | | - ps |
144 | | - product-obj)] |
145 | | - [else result])] |
146 | | - [_ result])] |
147 | | - [_ result]))) |
| 130 | +(define (product-function args-stx result) |
| 131 | + (match result |
| 132 | + [(tc-result1: ret-t ps orig-obj) |
| 133 | + (syntax-parse args-stx |
| 134 | + [((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int))) |
| 135 | + (define product-obj (-obj* (attribute e1.obj) (attribute e2.obj))) |
| 136 | + (cond |
| 137 | + [(Object? product-obj) |
| 138 | + (ret (-refine/fresh x ret-t (-eq (-lexp x) product-obj)) ps product-obj)] |
| 139 | + [else result])] |
| 140 | + [_ result])] |
| 141 | + [_ result])) |
148 | 142 |
|
149 | 143 | ;; make-vector |
150 | | -(define make-vector-function |
151 | | - (λ (args-stx result) |
152 | | - (match result |
153 | | - [(tc-result1: ret-t ps orig-obj) |
154 | | - (syntax-parse args-stx |
155 | | - [((~var size (w/obj+type -Int)) . _) |
156 | | - (ret (-refine/fresh v ret-t (-eq (-lexp (-vec-len-of (-id-path v))) |
157 | | - (attribute size.obj))) |
158 | | - ps |
159 | | - orig-obj)] |
160 | | - [_ result])] |
161 | | - [_ result]))) |
| 144 | +(define (make-vector-function args-stx result) |
| 145 | + (match result |
| 146 | + [(tc-result1: ret-t ps orig-obj) |
| 147 | + (syntax-parse args-stx |
| 148 | + [((~var size (w/obj+type -Int)) . _) |
| 149 | + (ret (-refine/fresh v ret-t (-eq (-lexp (-vec-len-of (-id-path v))) (attribute size.obj))) |
| 150 | + ps |
| 151 | + orig-obj)] |
| 152 | + [_ result])] |
| 153 | + [_ result])) |
162 | 154 |
|
163 | 155 | ;; modulo |
164 | | -(define modulo-function |
165 | | - (λ (args-stx result) |
166 | | - (match result |
167 | | - [(tc-result1: ret-t ps orig-obj) |
168 | | - (syntax-parse args-stx |
169 | | - [((~var e1 (w/type -Int)) (~var e2 (w/obj+type -Nat))) |
170 | | - (ret (-refine/fresh x ret-t (-lt (-lexp x) (attribute e2.obj))) |
171 | | - ps |
172 | | - orig-obj)] |
173 | | - [_ result])] |
174 | | - [_ result]))) |
| 156 | +(define (modulo-function args-stx result) |
| 157 | + (match result |
| 158 | + [(tc-result1: ret-t ps orig-obj) |
| 159 | + (syntax-parse args-stx |
| 160 | + [((~var e1 (w/type -Int)) (~var e2 (w/obj+type -Nat))) |
| 161 | + (ret (-refine/fresh x ret-t (-lt (-lexp x) (attribute e2.obj))) ps orig-obj)] |
| 162 | + [_ result])] |
| 163 | + [_ result])) |
175 | 164 |
|
176 | 165 | ;; random |
177 | | -(define random-function |
178 | | - (λ (args-stx result) |
179 | | - (match result |
180 | | - [(tc-result1: ret-t ps orig-obj) |
181 | | - (syntax-parse args-stx |
182 | | - ;; random (1 arg) |
183 | | - [((~var e1 (w/obj+type -Nat))) |
184 | | - (ret (-refine/fresh x ret-t (-lt (-lexp x) (attribute e1.obj))) |
185 | | - ps |
186 | | - orig-obj)] |
187 | | - ;; random (2 arg) |
188 | | - [((~var e1 (w/type -Int)) (~var e2 (w/type -Int))) |
189 | | - #:when (or (Object? (attribute e1.obj)) |
190 | | - (Object? (attribute e2.obj))) |
191 | | - (ret (-refine/fresh x ret-t (-and (-leq (attribute e1.obj) (-lexp x)) |
192 | | - (-lt (-lexp x) (attribute e2.obj)))) |
193 | | - ps |
194 | | - orig-obj)] |
195 | | - [_ result])] |
196 | | - [_ result]))) |
| 166 | +(define (random-function args-stx result) |
| 167 | + (match result |
| 168 | + [(tc-result1: ret-t ps orig-obj) |
| 169 | + (syntax-parse args-stx |
| 170 | + ;; random (1 arg) |
| 171 | + [((~var e1 (w/obj+type -Nat))) |
| 172 | + (ret (-refine/fresh x ret-t (-lt (-lexp x) (attribute e1.obj))) ps orig-obj)] |
| 173 | + ;; random (2 arg) |
| 174 | + [((~var e1 (w/type -Int)) (~var e2 (w/type -Int))) |
| 175 | + #:when (or (Object? (attribute e1.obj)) (Object? (attribute e2.obj))) |
| 176 | + (ret (-refine/fresh x |
| 177 | + ret-t |
| 178 | + (-and (-leq (attribute e1.obj) (-lexp x)) |
| 179 | + (-lt (-lexp x) (attribute e2.obj)))) |
| 180 | + ps |
| 181 | + orig-obj)] |
| 182 | + [_ result])] |
| 183 | + [_ result])) |
197 | 184 |
|
198 | 185 | ;; add1 / sub1 |
199 | | -(define (add/sub-1-function add?) |
200 | | - (λ (args-stx result) |
201 | | - (match result |
202 | | - [(tc-result1: ret-t ps orig-obj) |
203 | | - (syntax-parse args-stx |
204 | | - [((~var e1 (w/obj+type -Int))) |
205 | | - (define l ((if add? -lexp-add1 -lexp-sub1) (attribute e1.obj))) |
206 | | - (ret (-refine/fresh x ret-t (-eq (-lexp x) l)) |
207 | | - ps |
208 | | - l)] |
209 | | - [_ result])] |
210 | | - [_ result]))) |
| 186 | +(define ((add/sub-1-function add?) args-stx result) |
| 187 | + (match result |
| 188 | + [(tc-result1: ret-t ps orig-obj) |
| 189 | + (syntax-parse args-stx |
| 190 | + [((~var e1 (w/obj+type -Int))) |
| 191 | + (define l ((if add? -lexp-add1 -lexp-sub1) (attribute e1.obj))) |
| 192 | + (ret (-refine/fresh x ret-t (-eq (-lexp x) l)) ps l)] |
| 193 | + [_ result])] |
| 194 | + [_ result])) |
211 | 195 |
|
212 | 196 | (define linear-integer-function-table |
213 | 197 | (make-immutable-free-id-table |
|
0 commit comments