|
99 | 99 |
|
100 | 100 | ;; Leq to the internal leq rep |
101 | 101 | (define (Leq->leq l) |
102 | | - (match l |
103 | | - [(LeqProp: (LExp: c1 ts1) (LExp: c2 ts2)) |
104 | | - (leq (lexp c1 ts1) (lexp c2 ts2))])) |
| 102 | + (match-define (LeqProp: (LExp: c1 ts1) (LExp: c2 ts2)) l) |
| 103 | + (leq (lexp c1 ts1) (lexp c2 ts2))) |
105 | 104 |
|
106 | 105 |
|
107 | 106 | ;; ***************************************************************************** |
|
215 | 214 | [(eqv? a 0) (lexp 0 (make-terms))] |
216 | 215 | [(= a 1) exp] |
217 | 216 | [else |
218 | | - (match exp |
219 | | - [(lexp: c h) |
220 | | - (lexp (* c a) |
221 | | - (terms-scale h a))])])) |
| 217 | + (match-define (lexp: c h) exp) |
| 218 | + (lexp (* c a) (terms-scale h a))])) |
222 | 219 |
|
223 | 220 | (module+ test |
224 | 221 | (check-equal? (lexp-set (lexp* 17 '(42 x)) 'x 0) |
|
332 | 329 | (-> lexp? (-> any/c any/c) string?) |
333 | 330 | (define vars (terms-vars (lexp-vars e))) |
334 | 331 | (define const (lexp-const e)) |
335 | | - (define term->string |
336 | | - (λ (x) (string-append (if (= 1 (lexp-coeff e x)) |
337 | | - "" |
338 | | - (number->string (lexp-coeff e x))) |
339 | | - "(" (if pp |
340 | | - (pp x) |
341 | | - (~a x)) ")"))) |
| 332 | + (define (term->string x) |
| 333 | + (string-append (if (= 1 (lexp-coeff e x)) |
| 334 | + "" |
| 335 | + (number->string (lexp-coeff e x))) |
| 336 | + "(" |
| 337 | + (if pp |
| 338 | + (pp x) |
| 339 | + (~a x)) |
| 340 | + ")")) |
342 | 341 | (cond |
343 | 342 | [(terms-empty? vars) (number->string const)] |
344 | 343 | [(zero? const) |
|
487 | 486 | ;; leq2: ... + cx + .... <= ... + dx + ... |
488 | 487 | (let-values ([(l1 r1) (leq-lexps leq1)] |
489 | 488 | [(l2 r2) (leq-lexps leq2)]) |
490 | | - (let ([a (lexp-coeff l1 x)] [b (lexp-coeff r1 x)] |
491 | | - [c (lexp-coeff l2 x)] [d (lexp-coeff r2 x)]) |
492 | | - (cond |
493 | | - ;; leq1: ax <= lexp1 |
494 | | - ;; leq2: lexp2 <= dx |
495 | | - [(and (eqv? 0 b) (eqv? 0 c)) |
496 | | - (leq (lexp-scale l2 a) |
497 | | - (lexp-scale r1 d))] |
498 | | - ;; leq1: lexp1 <= bx |
499 | | - ;; leq2: cx <= lexp2 |
500 | | - [(and (eqv? 0 a) (eqv? 0 d)) |
501 | | - (leq (lexp-scale l1 c) |
502 | | - (lexp-scale r2 b))] |
503 | | - [else |
504 | | - (error 'leq-join "cannot join ~a and ~a by ~a" leq1 leq2 x)])))) |
| 489 | + (define a (lexp-coeff l1 x)) |
| 490 | + (define b (lexp-coeff r1 x)) |
| 491 | + (define c (lexp-coeff l2 x)) |
| 492 | + (define d (lexp-coeff r2 x)) |
| 493 | + (cond |
| 494 | + ;; leq1: ax <= lexp1 |
| 495 | + ;; leq2: lexp2 <= dx |
| 496 | + [(and (eqv? 0 b) (eqv? 0 c)) (leq (lexp-scale l2 a) (lexp-scale r1 d))] |
| 497 | + ;; leq1: lexp1 <= bx |
| 498 | + ;; leq2: cx <= lexp2 |
| 499 | + [(and (eqv? 0 a) (eqv? 0 d)) (leq (lexp-scale l1 c) (lexp-scale r2 b))] |
| 500 | + [else (error 'leq-join "cannot join ~a and ~a by ~a" leq1 leq2 x)]))) |
505 | 501 |
|
506 | 502 | (module+ test |
507 | 503 | (check-equal? (leq-join (leq (lexp* '(2 x)) |
|
600 | 596 | (values xlhs xrhs (cons ineq nox))])))) |
601 | 597 |
|
602 | 598 | (module+ test |
603 | | - (check-equal? (let-values ([(lt gt no) |
604 | | - (sli-partition (list (leq (lexp* '(2 x) '(4 y) 1) |
605 | | - (lexp* '(2 y)))) |
606 | | - 'x)]) |
607 | | - (list lt gt no)) |
| 599 | + (check-equal? (call-with-values |
| 600 | + (λ () (sli-partition (list (leq (lexp* '(2 x) '(4 y) 1) (lexp* '(2 y)))) 'x)) |
| 601 | + list) |
608 | 602 | (list (list (leq (lexp* '(2 x)) |
609 | 603 | (lexp* '(-2 y) -1))) |
610 | 604 | (list) |
611 | 605 | (list))) |
612 | | - (check-equal? (let-values ([(lt gt no) |
613 | | - (sli-partition (list (leq (lexp* '(2 x) '(4 y) 1) |
614 | | - (lexp* '(2 y))) |
615 | | - (leq (lexp* '(2 x) '(4 y)) |
616 | | - (lexp* '(2 y) '(42 x)))) |
617 | | - 'x)]) |
618 | | - (list lt gt no)) |
| 606 | + (check-equal? (call-with-values (λ () |
| 607 | + (sli-partition (list (leq (lexp* '(2 x) '(4 y) 1) (lexp* '(2 y))) |
| 608 | + (leq (lexp* '(2 x) '(4 y)) |
| 609 | + (lexp* '(2 y) '(42 x)))) |
| 610 | + 'x)) |
| 611 | + list) |
619 | 612 | (list (list (leq (lexp* '(2 x)) |
620 | 613 | (lexp* '(-2 y) -1))) |
621 | 614 | (list (leq (lexp* '(2 y)) |
622 | 615 | (lexp* '(40 x)))) |
623 | 616 | (list))) |
624 | | - (check-equal? (let-values ([(lt gt no) |
625 | | - (sli-partition (list (leq (lexp* '(2 x) '(4 y) -1) |
626 | | - (lexp* '(2 y))) |
627 | | - (leq (lexp* '(2 x) '(4 y)) |
628 | | - (lexp* '(2 y) '(42 x))) |
629 | | - (leq (lexp* '(2 z) '(4 y)) |
630 | | - (lexp* '(2 y) '(42 q)))) |
631 | | - 'x)]) |
632 | | - (list lt gt no)) |
| 617 | + (check-equal? (call-with-values |
| 618 | + (λ () |
| 619 | + (sli-partition (list (leq (lexp* '(2 x) '(4 y) -1) (lexp* '(2 y))) |
| 620 | + (leq (lexp* '(2 x) '(4 y)) (lexp* '(2 y) '(42 x))) |
| 621 | + (leq (lexp* '(2 z) '(4 y)) (lexp* '(2 y) '(42 q)))) |
| 622 | + 'x)) |
| 623 | + list) |
633 | 624 | (list (list (leq (lexp* '(2 x)) |
634 | 625 | (lexp* '(-2 y) 1))) |
635 | 626 | (list (leq (lexp* '(2 y)) |
|
0 commit comments