From 9401a537e0a022f1be87405d4aee1fa349cfd7a8 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Wed, 9 May 2012 17:02:14 -0500 Subject: [PATCH] extend the opters to track if a contract has any negative blame (this is similar to being flat, but struct contract (lazy ones) can be non-flat and still have no negative blame). Use this to optimize struct/dc contracts; specifically when a contract has no negative blame, then we don't need to add additional wrapping for indy-ness. This ended up being fairly tricky to handle the case where there are several mutually recursive define-opt/c functions. The code tracks which definitions depend on which ones and does a graph traversal of the dependencies to find if there is any non-negative blame possible. Naturally, this uses Racket's macro system to communicate between the definitions. --- collects/racket/contract/private/opt-guts.rkt | 69 ++++--- collects/racket/contract/private/opt.rkt | 68 ++++--- collects/racket/contract/private/opters.rkt | 188 +++++++++--------- .../racket/contract/private/struct-dc.rkt | 67 +++++-- collects/tests/racket/contract-test.rktl | 80 ++++++++ 5 files changed, 317 insertions(+), 155 deletions(-) diff --git a/collects/racket/contract/private/opt-guts.rkt b/collects/racket/contract/private/opt-guts.rkt index aa6736699b..5c51ddc165 100644 --- a/collects/racket/contract/private/opt-guts.rkt +++ b/collects/racket/contract/private/opt-guts.rkt @@ -1,7 +1,7 @@ #lang racket/base (require syntax/private/boundmap ;; needs to be the private one, since the public one has contracts - (for-template racket/base) - (for-template "guts.rkt" + (for-template racket/base + "guts.rkt" "blame.rkt" "misc.rkt") (for-syntax racket/base)) @@ -23,8 +23,6 @@ opt/info-change-val opt/unknown - combine-two-chaperone?s - optres-exp optres-lifts @@ -34,7 +32,11 @@ optres-opt optres-stronger-ribs optres-chaperone - build-optres) + optres-no-negative-blame? + build-optres + + combine-two-chaperone?s + combine-two-no-negative-blame) ;; (define/opter ( opt/i opt/info stx) body) ;; @@ -73,6 +75,12 @@ ;; the boolean indicaties if this contract is a chaperone contract ;; if it is a syntax object, then evaluating its contents determines ;; if this is a chaperone contract +;; - #f -- indicating that negative blame is impossible +;; #t -- indicating that negative blame may be possible +;; (listof identifier) -- indicating that negative blame is possible +;; if it is possible in any of the identifiers in the list +;; each identifier is expected to be an identifier bound by +;; the define-opt/c (struct optres (exp lifts @@ -81,7 +89,8 @@ flat opt stronger-ribs - chaperone)) + chaperone + no-negative-blame?)) (define (build-optres #:exp exp #:lifts lifts #:superlifts superlifts @@ -89,7 +98,8 @@ #:flat flat #:opt opt #:stronger-ribs stronger-ribs - #:chaperone chaperone) + #:chaperone chaperone + #:no-negative-blame? [no-negative-blame? (syntax? flat)]) (optres exp lifts superlifts @@ -97,7 +107,8 @@ flat opt stronger-ribs - chaperone)) + chaperone + no-negative-blame?)) ;; a hash table of opters (define opters-table @@ -231,23 +242,25 @@ ;; ;; opt/unknown : opt/i id id syntax ;; -(define (opt/unknown opt/i opt/info uctc) - (log-info (format "warning in ~a:~a: opt/c doesn't know the contract ~s" - (syntax-source uctc) - (if (syntax-line uctc) - (format "~a:~a" (syntax-line uctc) (syntax-column uctc)) - (format ":~a" (syntax-position uctc))) - (syntax->datum uctc))) +(define (opt/unknown opt/i opt/info uctc [extra-warning ""]) + (log-warning (string-append (format "warning in ~a:~a: opt/c doesn't know the contract ~s" + (syntax-source uctc) + (if (syntax-line uctc) + (format "~a:~a" (syntax-line uctc) (syntax-column uctc)) + (format ":~a" (syntax-position uctc))) + (syntax->datum uctc)) + extra-warning)) (with-syntax ([(lift-var partial-var partial-flat-var) (generate-temporaries '(lift partial partial-flat))] [val (opt/info-val opt/info)] [uctc uctc] [blame (opt/info-blame opt/info)]) - (optres - #'(partial-var val) - (list (cons #'lift-var - #'(coerce-contract 'opt/c uctc))) - null + (build-optres + #:exp #'(partial-var val) + #:lifts (list (cons #'lift-var + #'(coerce-contract 'opt/c uctc))) + #:superlifts null + #:partials (list (cons #'partial-var #'((contract-projection lift-var) blame)) @@ -258,10 +271,10 @@ (lambda (x) (error 'opt/unknown "flat called on an unknown that had no flat pred ~s ~s" lift-var x))))) - #f - #'lift-var - null - #'(chaperone-contract? lift-var)))) + #:flat #f + #:opt #'lift-var + #:stronger-ribs null + #:chaperone #'(chaperone-contract? lift-var)))) ;; combine-two-chaperone?s : (or/c boolean? syntax?) (or/c boolean? syntax?) -> (or/c boolean? syntax?) (define (combine-two-chaperone?s chaperone-a? chaperone-b?) @@ -274,3 +287,11 @@ (and chaperone-b? chaperone-a?)] [else #`(and #,chaperone-a? #,chaperone-b?)])) + +(define (combine-two-no-negative-blame a b) + (cond + [(eq? a #t) b] + [(eq? a #f) #f] + [(eq? b #t) a] + [(eq? b #f) #f] + [else (append a b)])) \ No newline at end of file diff --git a/collects/racket/contract/private/opt.rkt b/collects/racket/contract/private/opt.rkt index 88abe51bcc..097122a724 100644 --- a/collects/racket/contract/private/opt.rkt +++ b/collects/racket/contract/private/opt.rkt @@ -9,7 +9,10 @@ (provide opt/c define-opt/c define/opter opt/direct - begin-lifted) + begin-lifted + (for-syntax + define-opt/recursive-fn? + define-opt/recursive-fn-neg-blame?-id)) (define-syntax (define/opter stx) (syntax-case stx () @@ -97,13 +100,13 @@ (raise-blame-error blame val "expected a value ~a to ~e" compare should-be)) (begin-for-syntax - (define-struct define-opt/recursive-fn (transformer internal-fn) + (define-struct define-opt/recursive-fn (transformer internal-fn neg-blame?-id) #:property prop:procedure 0)) ;; opt/i : id opt/info syntax -> ;; syntax syntax-list syntax-list (union syntax #f) (union syntax #f) (define-for-syntax (opt/i opt/info stx) - ;; te case dispatch here must match what top-level-unknown? is doing + ;; the case dispatch here must match what top-level-unknown? is doing (syntax-case stx () [(ctc arg ...) (and (identifier? #'ctc) (opter #'ctc)) @@ -114,20 +117,28 @@ [(f arg ...) (and (identifier? #'f) (define-opt/recursive-fn? (syntax-local-value #'f (λ () #f)))) - (build-optres - #:exp - #`(#,(define-opt/recursive-fn-internal-fn (syntax-local-value #'f)) - #,(opt/info-contract opt/info) - #,(opt/info-blame opt/info) - #,(opt/info-val opt/info) - arg ...) - #:lifts null - #:superlifts null - #:partials null - #:flat #f - #:opt #f - #:stronger-ribs null - #:chaperone #t)] + (let ([d-o/r-f (syntax-local-value #'f)]) + (build-optres + #:exp + #`(#,(define-opt/recursive-fn-internal-fn (syntax-local-value #'f)) + #,(opt/info-contract opt/info) + #,(opt/info-blame opt/info) + #,(opt/info-val opt/info) + arg ...) + #:lifts null + #:superlifts null + #:partials null + #:flat #f + #:opt #f + #:stronger-ribs null + #:chaperone #t + #:no-negative-blame? + (let ([bx (syntax-local-value (define-opt/recursive-fn-neg-blame?-id d-o/r-f) + (λ () #f))]) + (and (box? bx) + (cond + [(eq? 'unknown (unbox bx)) (list #'f)] + [else (unbox bx)])))))] [konst (coerecable-constant? #'konst) (opt-constant-contract (syntax->datum #'konst) opt/info)] @@ -210,9 +221,10 @@ (define-syntax (define-opt/c stx) (syntax-case stx () [(_ (id args ...) e) - (with-syntax ([(f1 f2) - (generate-temporaries (list (format "~a-f1" (syntax-e #'id)) - (format "~a-f2" (syntax-e #'id))))]) + (with-syntax ([(f1 f2 no-neg-blame?) + (generate-temporaries (list (format "~a-external" (syntax-e #'id)) + (format "~a-internal" (syntax-e #'id)) + (format "~a-no-neg-blame?" (syntax-e #'id))))]) #`(begin (define-syntax id (define-opt/recursive-fn @@ -224,15 +236,23 @@ [(f . call-args) (with-syntax ([app (datum->syntax stx '#%app)]) #'(app f1 . call-args))])) - #'f2)) - (define-values (f1 f2) (opt/c-helper f1 f2 (id args ...) e))))])) + #'f2 + #'no-neg-blame?)) + (define-syntax no-neg-blame? (box 'unknown)) + (define-values (f1 f2) (opt/c-helper f1 f2 no-neg-blame? (id args ...) e))))])) (define-syntax (opt/c-helper stx) (syntax-case stx () - [(_ f1 f2 (id args ...) e) + [(_ f1 f2 no-neg-blame? (id args ...) e) (let () - (define info (make-opt/info #'ctc #'val #'blame #f (syntax->list #'(args ...)) #f #f #'this #'that)) + (define info (make-opt/info #'ctc #'val #'blame #f + (syntax->list #'(args ...)) + #f #f #'this #'that)) + ;; it seems like this syntax-local-value can fail when expand-once + ;; is called, but otherwise I think it shouldn't fail + (define bx (syntax-local-value #'no-neg-blame? (λ () #f))) (define an-optres (opt/i info #'e)) + (when bx (set-box! bx (optres-no-negative-blame? an-optres))) #`(let () (define (f2 ctc blame val args ...) #,(bind-superlifts diff --git a/collects/racket/contract/private/opters.rkt b/collects/racket/contract/private/opters.rkt index b2561b8407..c1ba179dbd 100644 --- a/collects/racket/contract/private/opters.rkt +++ b/collects/racket/contract/private/opters.rkt @@ -32,97 +32,103 @@ (syntax ((contract-projection lift-var) blame)))))))) (define (opt/or-ctc ps) - (let ((lift-from-hos null) - (superlift-from-hos null) - (partial-from-hos null)) - (let-values ([(opt-ps lift-ps superlift-ps partial-ps stronger-ribs hos ho-ctc chaperone?) - (let loop ([ps ps] - [next-ps null] - [lift-ps null] - [superlift-ps null] - [partial-ps null] - [stronger-ribs null] - [hos null] - [ho-ctc #f] - [chaperone? #t]) - (cond - [(null? ps) (values next-ps - lift-ps - superlift-ps - partial-ps - stronger-ribs - (reverse hos) - ho-ctc - chaperone?)] - [else - (define ps-optres (opt/i opt/info (car ps))) - (if (optres-flat ps-optres) - (loop (cdr ps) - (cons (optres-flat ps-optres) next-ps) - (append lift-ps (optres-lifts ps-optres)) - (append superlift-ps (optres-superlifts ps-optres)) - (append partial-ps (optres-partials ps-optres)) - (append (optres-stronger-ribs ps-optres) stronger-ribs) - hos - ho-ctc - (combine-two-chaperone?s chaperone? (optres-chaperone ps-optres))) - (if (< (length hos) 1) - (loop (cdr ps) - next-ps - (append lift-ps (optres-lifts ps-optres)) - (append superlift-ps (optres-superlifts ps-optres)) - (append partial-ps (optres-partials ps-optres)) - (append (optres-stronger-ribs ps-optres) stronger-ribs) - (cons (car ps) hos) - (optres-exp ps-optres) - (combine-two-chaperone?s chaperone? (optres-chaperone ps-optres))) - (loop (cdr ps) - next-ps - lift-ps - superlift-ps - partial-ps - stronger-ribs - (cons (car ps) hos) - ho-ctc - chaperone?)))]))]) - (with-syntax ((next-ps - (with-syntax (((opt-p ...) (reverse opt-ps))) - (syntax (or opt-p ...))))) - (build-optres - #:exp - (cond - [(null? hos) - (with-syntax ([val (opt/info-val opt/info)] - [blame (opt/info-blame opt/info)]) - (syntax - (if next-ps - val - (raise-blame-error blame - val - "none of the branches of the or/c matched"))))] - [(= (length hos) 1) - (with-syntax ([ho-ctc ho-ctc] - [val (opt/info-val opt/info)]) - (syntax - (if next-ps val ho-ctc)))] - ;; FIXME something's not right with this case. - [(> (length hos) 1) - (define-values (exp new-lifts new-superlifts new-partials) (opt/or-unknown stx)) - (set! lift-from-hos new-lifts) - (set! superlift-from-hos new-superlifts) - (set! partial-from-hos new-partials) - #`(if next-ps val #,exp)]) - #:lifts - (append lift-ps lift-from-hos) - #:superlifts - (append superlift-ps superlift-from-hos) - #:partials - (append partial-ps partial-from-hos) - #:flat - (if (null? hos) (syntax next-ps) #f) - #:opt #f - #:stronger-ribs stronger-ribs - #:chaperone chaperone?))))) + (define lift-from-hos null) + (define superlift-from-hos null) + (define partial-from-hos null) + (define-values (opt-ps lift-ps superlift-ps partial-ps stronger-ribs hos ho-ctc chaperone? no-negative-blame) + (let loop ([ps ps] + [next-ps null] + [lift-ps null] + [superlift-ps null] + [partial-ps null] + [stronger-ribs null] + [hos null] + [ho-ctc #f] + [chaperone? #t] + [no-negative-blame #t]) + (cond + [(null? ps) (values next-ps + lift-ps + superlift-ps + partial-ps + stronger-ribs + (reverse hos) + ho-ctc + chaperone? + no-negative-blame)] + [else + (define ps-optres (opt/i opt/info (car ps))) + (if (optres-flat ps-optres) + (loop (cdr ps) + (cons (optres-flat ps-optres) next-ps) + (append lift-ps (optres-lifts ps-optres)) + (append superlift-ps (optres-superlifts ps-optres)) + (append partial-ps (optres-partials ps-optres)) + (append (optres-stronger-ribs ps-optres) stronger-ribs) + hos + ho-ctc + (combine-two-chaperone?s chaperone? (optres-chaperone ps-optres)) + (combine-two-no-negative-blame no-negative-blame (optres-no-negative-blame? ps-optres))) + (if (null? hos) + (loop (cdr ps) + next-ps + (append lift-ps (optres-lifts ps-optres)) + (append superlift-ps (optres-superlifts ps-optres)) + (append partial-ps (optres-partials ps-optres)) + (append (optres-stronger-ribs ps-optres) stronger-ribs) + (cons (car ps) hos) + (optres-exp ps-optres) + (combine-two-chaperone?s chaperone? (optres-chaperone ps-optres)) + (combine-two-no-negative-blame no-negative-blame (optres-no-negative-blame? ps-optres))) + (loop (cdr ps) + next-ps + lift-ps + superlift-ps + partial-ps + stronger-ribs + (cons (car ps) hos) + ho-ctc + chaperone? + no-negative-blame)))]))) + (with-syntax ((next-ps + (with-syntax (((opt-p ...) (reverse opt-ps))) + (syntax (or opt-p ...))))) + (build-optres + #:exp + (cond + [(null? hos) + (with-syntax ([val (opt/info-val opt/info)] + [blame (opt/info-blame opt/info)]) + (syntax + (if next-ps + val + (raise-blame-error blame + val + "none of the branches of the or/c matched"))))] + [(= (length hos) 1) + (with-syntax ([ho-ctc ho-ctc] + [val (opt/info-val opt/info)]) + (syntax + (if next-ps val ho-ctc)))] + ;; FIXME something's not right with this case. + [(> (length hos) 1) + (define-values (exp new-lifts new-superlifts new-partials) (opt/or-unknown stx)) + (set! lift-from-hos new-lifts) + (set! superlift-from-hos new-superlifts) + (set! partial-from-hos new-partials) + #`(if next-ps val #,exp)]) + #:lifts + (append lift-ps lift-from-hos) + #:superlifts + (append superlift-ps superlift-from-hos) + #:partials + (append partial-ps partial-from-hos) + #:flat + (if (null? hos) (syntax next-ps) #f) + #:opt #f + #:stronger-ribs stronger-ribs + #:chaperone chaperone? + #:no-negative-blame? no-negative-blame))) (syntax-case stx (or/c) [(or/c p ...) diff --git a/collects/racket/contract/private/struct-dc.rkt b/collects/racket/contract/private/struct-dc.rkt index c431133856..9135811480 100644 --- a/collects/racket/contract/private/struct-dc.rkt +++ b/collects/racket/contract/private/struct-dc.rkt @@ -755,22 +755,47 @@ (quote-module-name) '#,struct-id)) +(define-for-syntax (traverse-no-neg-blame-identifiers no-neg-blame) + (for/and ([id (in-list no-neg-blame)]) + (let loop ([parent-id id] + [path '()]) + (define x (syntax-local-value parent-id)) + (define box-id (define-opt/recursive-fn-neg-blame?-id x)) + (define bx (syntax-local-value box-id)) + (define content (unbox bx)) + (cond + [(boolean? content) content] + [(eq? content 'unknown) #f] ;; have to give up here + [else + (define ans + (for/and ([id (in-list content)]) + (cond + [(ormap (λ (y) (free-identifier=? id y)) path) + ;; if we have a loop, then we know there is + ;; no refutation of 'no-neg-blame' just cyclic + ;; dependencies in define-opt/c, so we can + ;; conclude 'no-neg-blame' holds + #t] + [else + (loop id (cons parent-id path))]))) + (set-box! bx ans) + ans])))) + (define/opter (-struct/dc opt/i opt/info stx) (syntax-case stx () [(_ struct-id clause ...) (let/ec k (define-values (info _1 _2) (parse-struct/dc stx)) - (define (give-up) - (call-with-values (λ () (opt/unknown opt/i opt/info stx)) - k)) + (define (give-up [extra ""]) (k (opt/unknown opt/i opt/info stx extra))) (cond [(ormap values (list-ref info 4)) ;; any mutable fields, just give up (give-up)] [else (define depended-on-fields (make-free-identifier-mapping)) - (define flat-fields (make-free-identifier-mapping)) - (define-values (s-fo-code s-chap-code s-lifts s-super-lifts s-partially-applied can-be-optimized? stronger-ribs chaperone?) + (define no-negative-blame-fields (make-free-identifier-mapping)) + (define-values (s-fo-code s-chap-code s-lifts s-super-lifts + s-partially-applied can-be-optimized? stronger-ribs chaperone? no-negative-blame) (for/fold ([s-fo-code '()] [s-chap-code '()] [s-lifts '()] @@ -778,7 +803,8 @@ [s-partially-applied '()] [can-be-optimized? #t] [stronger-ribs '()] - [chaperone? #t]) + [chaperone? #t] + [no-negative-blame #t]) ([clause (in-list (syntax->list #'(clause ...)))]) (define-values (sel-id lazy? dep-vars exp) @@ -799,8 +825,8 @@ (when dep-vars (for ([dep-var (in-list (syntax->list dep-vars))]) - (free-identifier-mapping-put! depended-on-fields dep-var #t))) - (free-identifier-mapping-put! flat-fields sel-id (optres-flat this-optres)) + (free-identifier-mapping-put! depended-on-fields dep-var sel-id))) + (free-identifier-mapping-put! no-negative-blame-fields sel-id (optres-no-negative-blame? this-optres)) (define this-body-code (cond @@ -817,7 +843,6 @@ (optres-partials this-optres) (optres-exp this-optres))))))] [else (optres-exp this-optres)])) - (define this-chap-code (and (or (not (optres-flat this-optres)) @@ -845,7 +870,7 @@ (#,(id->sel-id #'struct-id sel-id) #,(opt/info-val opt/info))]) #,this-body-code))) - + (values (if this-fo-code (cons this-fo-code s-fo-code) s-fo-code) @@ -857,15 +882,23 @@ (if dep-vars s-partially-applied (append (optres-partials this-optres) s-partially-applied)) (and (optres-opt this-optres) can-be-optimized?) (if dep-vars stronger-ribs (append (optres-stronger-ribs this-optres) stronger-ribs)) - (combine-two-chaperone?s chaperone? (optres-chaperone this-optres))))) + (combine-two-chaperone?s chaperone? (optres-chaperone this-optres)) + (combine-two-no-negative-blame no-negative-blame (optres-no-negative-blame? this-optres))))) ;; to avoid having to deal with indy-ness, just give up if any - ;; of the fields that are depended on aren't flat + ;; of the fields that are depended on can possibly raise negative blame (free-identifier-mapping-for-each depended-on-fields - (λ (depended-on-id flat?) - (unless (free-identifier-mapping-get flat-fields depended-on-id) - (give-up)))) + (λ (depended-on-id field-doing-the-depending) + (define no-neg-blame (free-identifier-mapping-get no-negative-blame-fields depended-on-id)) + (define dep-answer (cond + [(boolean? no-neg-blame) no-neg-blame] + [else (traverse-no-neg-blame-identifiers no-neg-blame)])) + (unless no-neg-blame + (give-up + (format " because the contract on field: ~a depends on: ~a and its contract may have negative blame" + (syntax-e field-doing-the-depending) + (syntax-e depended-on-id)))))) (with-syntax ([(stronger-prop-desc stronger-prop-pred? stronger-prop-get) (syntax-local-lift-values-expression @@ -874,6 +907,7 @@ [(free-var ...) (opt/info-free-vars opt/info)] [(index ...) (build-list (length (opt/info-free-vars opt/info)) values)] [pred? (list-ref info 2)]) + (build-optres #:exp (if (null? s-chap-code) ;; if this is #t, when we have to avoid putting the property on here. @@ -904,7 +938,8 @@ #:flat #f #:opt can-be-optimized? #:stronger-ribs stronger-ribs - #:chaperone #t))]))])) + #:chaperone #t + #:no-negative-blame? no-negative-blame))]))])) (define (struct/dc-error blame obj what) (raise-blame-error blame obj diff --git a/collects/tests/racket/contract-test.rktl b/collects/tests/racket/contract-test.rktl index 8ef4c8569d..7ce571f912 100644 --- a/collects/tests/racket/contract-test.rktl +++ b/collects/tests/racket/contract-test.rktl @@ -10622,6 +10622,86 @@ (contract (f 11) 11 'pos 'neg)) 11) + ;; try-one : syntax -> number + ;; evaluates the exp and returns the number of opt/c warnings found + (contract-eval + '(define (eval-and-count-log-messages exp) + (define my-logger (make-logger)) + (parameterize ([current-logger my-logger]) + (define ans (make-channel)) + (define recv (make-log-receiver my-logger 'warning)) + (thread + (λ () + (let loop ([opt/c-msgs 0]) + (define res (sync recv)) + (cond + [(equal? "done" (vector-ref res 1)) + (channel-put ans opt/c-msgs)] + [else + (define opt/c-msg? (regexp-match? #rx"opt/c" (vector-ref res 1))) + (loop (if opt/c-msg? + (+ opt/c-msgs 1) + opt/c-msgs))])))) + (let/ec k + (parameterize ([error-escape-handler k]) + (eval exp))) + (log-warning "done") + (channel-get ans)))) + + (ctest 1 eval-and-count-log-messages + '(let () + (struct s (a b)) + (opt/c (struct/dc s [a (-> integer? integer?)] [b (a) integer?])))) + + (ctest 1 eval-and-count-log-messages + '(let () + (struct s (a b)) + (define-opt/c (f x) + (-> integer? integer?)) + (define-opt/c (g x) + (struct/dc s [a (f 1)] [b (a) integer?])) + 1)) + + (ctest 0 eval-and-count-log-messages + '(let () + (struct s (a b)) + (define-opt/c (f x) integer?) + (opt/c (struct/dc s [a (f 1)] [b (a) integer?])))) + + (ctest 0 eval-and-count-log-messages + '(let () + (define-struct h:kons (hd tl) #:transparent) + (define-struct h:node (rank val obj children) #:transparent) + + (define-opt/c (binomial-tree-rank=/sco r v) + (or/c #f + (struct/dc h:node + [rank (=/c r)] + [val (>=/c v)] + [children (rank val) #:lazy (heap-ordered/desc/sco (- rank 1) val)]))) + + (define-opt/c (binomial-tree-rank>/sco r) + (or/c #f + (struct/dc h:node + [rank (>=/c r)] + [val any/c] + [children (rank val) #:lazy (heap-ordered/desc/sco (- rank 1) val)]))) + + (define-opt/c (heap-ordered/desc/sco rank val) + (or/c #f + (struct/dc h:kons + [hd #:lazy (binomial-tree-rank=/sco rank val)] + [tl () #:lazy (heap-ordered/desc/sco (- rank 1) val)]))) + + (define-opt/c (binomial-trees/asc/sco rank) + (or/c #f + (struct/dc h:kons + [hd #:lazy (binomial-tree-rank>/sco rank)] + [tl (hd) #:lazy (binomial-trees/asc/sco (h:node-rank hd))]))) + + (define binomial-heap/sco (binomial-trees/asc/sco -inf.0)) + 1)) + ;; ;; end of define-opt/c