From c449b69f8f5843b0b87d7e233b393f55d764241d Mon Sep 17 00:00:00 2001 From: Sorawee Porncharoenwase Date: Sat, 16 Mar 2024 19:29:26 +0700 Subject: [PATCH] core: optimizing lifiting When there is no contract error in any case, there is no need to emit the assertions. --- rosette/base/core/lift.rkt | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/rosette/base/core/lift.rkt b/rosette/base/core/lift.rkt index d6901ae3..f9ee8461 100644 --- a/rosette/base/core/lift.rkt +++ b/rosette/base/core/lift.rkt @@ -63,10 +63,12 @@ (id val) (match (type-cast rosette-type? val (quote id)) [(? contracted? v) (id v)] - [(union vs) (apply merge* (assert-some - (for/list ([v vs] #:when (contracted? (cdr v))) - (cons (car v) (id (cdr v)))) - (contract-error (quote id) contracted? val)))] + [(union vs) + (merge+ + (for/list ([v (in-list vs)] #:when (contracted? (cdr v))) + (cons (car v) (id (cdr v)))) + #:unless (length vs) + #:error (contract-error (quote id) contracted? val))] [_ (assert #f (contract-error (quote id) contracted? val))])))] [(_ (id0 id ...) : racket-contract? -> rosette-type?) #'(splicing-let ([contracted? racket-contract?]) @@ -79,10 +81,12 @@ (id val) (match (type-cast rosette-type? val (quote id)) [(? contracted? v) (id v)] - [(union vs) (apply merge* (assert-some - (for/list ([v vs] #:when (contracted? (cdr v))) - (cons (car v) (id (cdr v)))) - (contract-error (quote id) contracted? val)))] + [(union vs) + (merge+ + (for/list ([v (in-list vs)] #:when (contracted? (cdr v))) + (cons (car v) (id (cdr v)))) + #:unless (length vs) + #:error (contract-error (quote id) contracted? val))] [_ (assert #f (contract-error (quote id) contracted? val))])))] [(_ id : racket-contract? -> rosette-type?) #`(splicing-let ([contracted? racket-contract?])