From d9051897d8f526bff0f82b785389164aa6f05b2b Mon Sep 17 00:00:00 2001 From: Sorawee Porncharoenwase Date: Tue, 12 Mar 2024 19:43:28 +0700 Subject: [PATCH] seq: optimize append There are two changes in this commit. The first change builds the list from a variadic append operation from right to left, which is the natural order for list construction. This speeds up the following program: ``` (time (void (append* (for/list ([i 30000]) (if b '() '(1)))))) ``` from 5 seconds to 1 second. The second change avoids making an assertion when doing unsafe/append on two symbolic unions. This is fine because all calls to unsafe/append is already guarded via type casting to make them symbolic unions of rosette-contract?, so there is no need to add another guard. Thanks to @camoy for raising up the issue about the unnecessary assertions. --- rosette/base/adt/seq.rkt | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/rosette/base/adt/seq.rkt b/rosette/base/adt/seq.rkt index b837e036..144fe98a 100644 --- a/rosette/base/adt/seq.rkt +++ b/rosette/base/adt/seq.rkt @@ -69,13 +69,9 @@ [((? racket-contract?) (union vs)) (unsafe-merge** vs (proc xs _))] [((union vs) (? racket-contract?)) (unsafe-merge** vs (proc _ ys))] [((union vs) (union ws)) - (apply unsafe-merge* - (assert-some - (for*/list ([v vs] [w ws] [g (in-value (&& (car v) (car w)))] #:when g) - (cons g (proc (cdr v) (cdr w)))) - #:unless (* (length vs) (length ws)) - (arguments-error (quote proc) (format "expected ~a ~a" rosette-contract? rosette-contract?) - "first argument" vs "second argument" ws)))]))] + (apply unsafe-merge* + (for*/list ([v vs] [w ws] [g (in-value (&& (car v) (car w)))] #:when g) + (cons g (proc (cdr v) (cdr w)))))]))] (define #,(lift-id #'proc) (case-lambda [() (racket-constructor)] @@ -83,8 +79,9 @@ [(xs ys) (unsafe/append (type-cast rosette-contract? xs (quote proc)) (type-cast rosette-contract? ys (quote proc)))] [xss (for/fold ([out (racket-constructor)]) - ([xs (for/list ([ys xss]) (type-cast rosette-contract? ys (quote proc)))]) - (unsafe/append out xs))])))])) + ([xs (for/list ([ys (in-list (reverse xss))]) + (type-cast rosette-contract? ys (quote proc)))]) + (unsafe/append xs out))])))])) (define-syntax (define/lift/split stx) (syntax-case stx ()