|
127 | 127 | [_ result])) |
128 | 128 |
|
129 | 129 | ;; * |
130 | | -(define product-function |
131 | | - (λ (args-stx result) |
132 | | - (match result |
133 | | - [(tc-result1: ret-t ps orig-obj) |
134 | | - (syntax-parse args-stx |
135 | | - [((~var e1 (w/obj+type -Int)) (~var e2 (w/obj+type -Int))) |
136 | | - (define product-obj (-obj* (attribute e1.obj) (attribute e2.obj))) |
137 | | - (cond |
138 | | - [(Object? product-obj) |
139 | | - (ret (-refine/fresh x ret-t (-eq (-lexp x) product-obj)) |
140 | | - ps |
141 | | - product-obj)] |
142 | | - [else result])] |
143 | | - [_ result])] |
144 | | - [_ 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])) |
145 | 142 |
|
146 | 143 | ;; make-vector |
147 | | -(define make-vector-function |
148 | | - (λ (args-stx result) |
149 | | - (match result |
150 | | - [(tc-result1: ret-t ps orig-obj) |
151 | | - (syntax-parse args-stx |
152 | | - [((~var size (w/obj+type -Int)) . _) |
153 | | - (ret (-refine/fresh v ret-t (-eq (-lexp (-vec-len-of (-id-path v))) |
154 | | - (attribute size.obj))) |
155 | | - ps |
156 | | - orig-obj)] |
157 | | - [_ result])] |
158 | | - [_ 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])) |
159 | 154 |
|
160 | 155 | ;; modulo |
161 | | -(define modulo-function |
162 | | - (λ (args-stx result) |
163 | | - (match result |
164 | | - [(tc-result1: ret-t ps orig-obj) |
165 | | - (syntax-parse args-stx |
166 | | - [((~var e1 (w/type -Int)) (~var e2 (w/obj+type -Nat))) |
167 | | - (ret (-refine/fresh x ret-t (-lt (-lexp x) (attribute e2.obj))) |
168 | | - ps |
169 | | - orig-obj)] |
170 | | - [_ result])] |
171 | | - [_ 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])) |
172 | 164 |
|
173 | 165 | ;; random |
174 | | -(define random-function |
175 | | - (λ (args-stx result) |
176 | | - (match result |
177 | | - [(tc-result1: ret-t ps orig-obj) |
178 | | - (syntax-parse args-stx |
179 | | - ;; random (1 arg) |
180 | | - [((~var e1 (w/obj+type -Nat))) |
181 | | - (ret (-refine/fresh x ret-t (-lt (-lexp x) (attribute e1.obj))) |
182 | | - ps |
183 | | - orig-obj)] |
184 | | - ;; random (2 arg) |
185 | | - [((~var e1 (w/type -Int)) (~var e2 (w/type -Int))) |
186 | | - #:when (or (Object? (attribute e1.obj)) |
187 | | - (Object? (attribute e2.obj))) |
188 | | - (ret (-refine/fresh x ret-t (-and (-leq (attribute e1.obj) (-lexp x)) |
189 | | - (-lt (-lexp x) (attribute e2.obj)))) |
190 | | - ps |
191 | | - orig-obj)] |
192 | | - [_ result])] |
193 | | - [_ 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])) |
194 | 184 |
|
195 | 185 | ;; add1 / sub1 |
196 | 186 | (define ((add/sub-1-function add?) args-stx result) |
|
0 commit comments