|
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 | 130 | (define product-function |
|
196 | 193 | [_ result]))) |
197 | 194 |
|
198 | 195 | ;; 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]))) |
| 196 | +(define ((add/sub-1-function add?) args-stx result) |
| 197 | + (match result |
| 198 | + [(tc-result1: ret-t ps orig-obj) |
| 199 | + (syntax-parse args-stx |
| 200 | + [((~var e1 (w/obj+type -Int))) |
| 201 | + (define l ((if add? -lexp-add1 -lexp-sub1) (attribute e1.obj))) |
| 202 | + (ret (-refine/fresh x ret-t (-eq (-lexp x) l)) ps l)] |
| 203 | + [_ result])] |
| 204 | + [_ result])) |
211 | 205 |
|
212 | 206 | (define linear-integer-function-table |
213 | 207 | (make-immutable-free-id-table |
|
0 commit comments