rename encode/decode to to-nat/from-nat
also, Rackety for 102 columns and drop the nat? and extended-nat? exports, using instead the standard names for those concepts: exact-nonnegative-integer? and (or/c exact-nonnegative-integer? +inf.0)
This commit is contained in:
Robby Findler
parent
1b4236722d
commit
f2c01e780b
|
|
@ -22,17 +22,9 @@ is linear in the bits of the number.
|
|||
@; XXX explain fairness
|
||||
@; XXX add citations
|
||||
|
||||
@defproc[(nat? [x any/c]) boolean?]{
|
||||
|
||||
Identifies a value as a natural number.}
|
||||
|
||||
@defproc[(extended-nat? [x any/c]) boolean?]{
|
||||
|
||||
Identifies a value as a natural number or positive infinity.}
|
||||
|
||||
@defproc[(enum [size extended-nat?]
|
||||
[from (-> nat? any/c)]
|
||||
[to (-> any/c nat?)])
|
||||
@defproc[(enum [size (or/c exact-nonnegative-integer? +inf.0)]
|
||||
[from (-> exact-nonnegative-integer? any/c)]
|
||||
[to (-> any/c exact-nonnegative-integer?)])
|
||||
enum?]{
|
||||
|
||||
Constructs an @tech{enumeration} of size @racket[size] where
|
||||
|
|
@ -43,15 +35,15 @@ function. }
|
|||
|
||||
Identifies a value as an @tech{enumeration}.}
|
||||
|
||||
@defproc[(size [e enum?]) extended-nat?]{
|
||||
@defproc[(size [e enum?]) (or/c exact-nonnegative-integer? +inf.0)]{
|
||||
|
||||
Returns the size of an @tech{enumeration}.}
|
||||
|
||||
@defproc[(decode [e enum?] [n nat?]) any/c]{
|
||||
@defproc[(decode [e enum?] [n exact-nonnegative-integer?]) any/c]{
|
||||
|
||||
Uses @racket[e] to decode @racket[n].}
|
||||
|
||||
@defproc[(encode [e enum?] [x any/c]) nat?]{
|
||||
@defproc[(to-nat [e enum?] [x any/c]) exact-nonnegative-integer?]{
|
||||
|
||||
Uses @racket[e] to encode @racket[x].}
|
||||
|
||||
|
|
@ -61,7 +53,7 @@ An @tech{enumeration} of the natural numbers.
|
|||
|
||||
@examples[#:eval the-eval
|
||||
(decode nat/e 5)
|
||||
(encode nat/e 5)
|
||||
(to-nat nat/e 5)
|
||||
]}
|
||||
|
||||
@defproc[(map/e [f (-> a ... b)]
|
||||
|
|
@ -75,7 +67,7 @@ functions of @racket[e].
|
|||
(define map-1/e
|
||||
(map/e number->string string->number nat/e))
|
||||
(decode map-1/e 5)
|
||||
(encode map-1/e "5")
|
||||
(to-nat map-1/e "5")
|
||||
(define map-2/e
|
||||
(map/e (λ (x y)
|
||||
(string-join
|
||||
|
|
@ -85,7 +77,7 @@ functions of @racket[e].
|
|||
(apply values (map string->number (string-split x))))
|
||||
nat/e nat/e))
|
||||
(decode map-2/e 5)
|
||||
(encode map-2/e "1 2")
|
||||
(to-nat map-2/e "1 2")
|
||||
]}
|
||||
|
||||
@defproc[(filter/e [e enum?] [p (-> any/c boolean?)]) enum?]{
|
||||
|
|
@ -99,19 +91,20 @@ so only use it for very small enumerations.
|
|||
(define filter-1/e
|
||||
(filter/e nat/e even?))
|
||||
(decode filter-1/e 5)
|
||||
(encode filter-1/e 8)
|
||||
(to-nat filter-1/e 8)
|
||||
]}
|
||||
|
||||
@defproc[(except/e [e enum?] [x any/c] ...) enum?]{
|
||||
|
||||
Returns an @tech{enumeration} identical to @racket[e] except that all
|
||||
@racket[x] are not included in the decoding and cannot be encoded.
|
||||
@racket[x] are not included in the decoding and cannot be encoded
|
||||
(converted to a natural number).
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(define except-1/e
|
||||
(except/e nat/e 3))
|
||||
(decode except-1/e 5)
|
||||
(encode except-1/e 8)
|
||||
(to-nat except-1/e 8)
|
||||
]}
|
||||
|
||||
@defproc[(to-stream [e enum?]) stream?]{
|
||||
|
|
@ -122,7 +115,7 @@ Returns a stream of the values in @racket[e].
|
|||
(to-stream map-2/e)
|
||||
]}
|
||||
|
||||
@defproc[(approximate [e enum?] [n nat?]) list?]{
|
||||
@defproc[(approximate [e enum?] [n exact-nonnegative-integer?]) list?]{
|
||||
|
||||
Returns a list of the first @racket[n] values in @racket[e].
|
||||
|
||||
|
|
@ -139,16 +132,16 @@ diverge if @racket[e] is infinite.
|
|||
(to-list (take/e map-2/e 5))
|
||||
]}
|
||||
|
||||
@defproc[(take/e [e enum?] [n nat?]) enum?]{
|
||||
@defproc[(take/e [e enum?] [n exact-nonnegative-integer?]) enum?]{
|
||||
|
||||
Identical to @racket[e] but only includes the first @racket[n] values.
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(decode (take/e map-2/e 5) 3)
|
||||
(encode (take/e map-2/e 5) "1 1")
|
||||
(to-nat (take/e map-2/e 5) "1 1")
|
||||
]}
|
||||
|
||||
@defproc[(slice/e [e enum?] [lo nat?] [hi nat?]) enum?]{
|
||||
@defproc[(slice/e [e enum?] [lo exact-nonnegative-integer?] [hi exact-nonnegative-integer?]) enum?]{
|
||||
|
||||
Identical to @racket[e] but only includes the values between
|
||||
@racket[lo] and @racket[hi].
|
||||
|
|
@ -157,7 +150,7 @@ Identical to @racket[e] but only includes the values between
|
|||
(to-list (slice/e map-2/e 5 10))
|
||||
]}
|
||||
|
||||
@defproc[(below/e [max nat?]) enum?]{
|
||||
@defproc[(below/e [max exact-nonnegative-integer?]) enum?]{
|
||||
|
||||
An @tech{enumeration} of the first @racket[max] naturals.
|
||||
|
||||
|
|
@ -216,7 +209,7 @@ predicate identifying elements of it. Only one or zero predicates
|
|||
should return true on any value.
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(approximate (disj-sum/e (cons nat/e nat?) (cons map-1/e string?)) 10)
|
||||
(approximate (disj-sum/e (cons nat/e exact-nonnegative-integer?) (cons map-1/e string?)) 10)
|
||||
]}
|
||||
|
||||
@defproc[(disj-append/e [e-p (cons/c enum? (-> any/c boolean?))] ...+) enum?]{
|
||||
|
|
@ -227,7 +220,7 @@ the next. @racket[e-p] are formatted as in @racket[disj-sum/e]. All
|
|||
but the last enumeration should be finite.
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(approximate (disj-append/e (cons (take/e nat/e 4) nat?)
|
||||
(approximate (disj-append/e (cons (take/e nat/e 4) exact-nonnegative-integer?)
|
||||
(cons map-1/e string?))
|
||||
10)
|
||||
]}
|
||||
|
|
@ -276,7 +269,7 @@ of the enumerations returned by @racket[f] applied to each element of
|
|||
nat/e))
|
||||
'("Brian" "Jenny" "Ted" "Ki")))
|
||||
(approximate traverse-1/e 5)
|
||||
(encode traverse-1/e
|
||||
(to-nat traverse-1/e
|
||||
'(("Brian" . 11) ("Jenny" . 15) ("Ted" . 16) ("Ki" . 7)))
|
||||
]}
|
||||
|
||||
|
|
@ -291,7 +284,7 @@ of the enumerations returned by @racket[f] applied to each value of
|
|||
(hash-traverse/e (λ (n) (below/e n))
|
||||
(hash "Brian" 5 "Jenny" 15 "Ted" 25 "Ki" 30)))
|
||||
(approximate hash-traverse-1/e 5)
|
||||
(encode hash-traverse-1/e
|
||||
(to-nat hash-traverse-1/e
|
||||
'#hash(("Brian" . 4) ("Jenny" . 1) ("Ted" . 16) ("Ki" . 7)))
|
||||
]}
|
||||
|
||||
|
|
@ -304,10 +297,10 @@ Constructs an @tech{enumeration} of pairs of values @racket[a] and
|
|||
(define dep-1/e
|
||||
(dep/e nat/e (λ (a) (below/e a))))
|
||||
(approximate dep-1/e 5)
|
||||
(encode dep-1/e (cons 17 10))
|
||||
(to-nat dep-1/e (cons 17 10))
|
||||
]}
|
||||
|
||||
@defproc[(dep2/e [n extended-nat?] [a enum?] [b (-> any/c enum?)]) enum?]{
|
||||
@defproc[(dep2/e [n (or/c exact-nonnegative-integer? +inf.0)] [a enum?] [b (-> any/c enum?)]) enum?]{
|
||||
|
||||
Like @racket[dep2/e] but requires the size of the resulting
|
||||
enumeration be given as @racket[n]. This is more efficient than
|
||||
|
|
@ -321,7 +314,7 @@ enumeration be given as @racket[n]. This is more efficient than
|
|||
(below/e 5)
|
||||
(λ (a) (below/e a))))
|
||||
(approximate dep2-1/e 5)
|
||||
(encode dep2-1/e (cons 4 3))
|
||||
(to-nat dep2-1/e (cons 4 3))
|
||||
]}
|
||||
|
||||
@defproc[(fold-enum [f (-> (listof a) b enum?)] [bs (listof b)]) enum?]{
|
||||
|
|
@ -336,10 +329,10 @@ is initialized to @racket['()].
|
|||
(below/e (+ (foldr + 0 as) b)))
|
||||
(list 1 2 3)))
|
||||
(approximate fold-enum-1/e 5)
|
||||
(encode fold-enum-1/e (list 0 1 1))
|
||||
(to-nat fold-enum-1/e (list 0 1 1))
|
||||
]}
|
||||
|
||||
@defproc[(range/e [lo nat?] [hi nat?]) enum?]{
|
||||
@defproc[(range/e [lo exact-nonnegative-integer?] [hi exact-nonnegative-integer?]) enum?]{
|
||||
|
||||
An @tech{enumeration} of the naturals between @racket[lo] and @racket[hi].
|
||||
|
||||
|
|
@ -347,7 +340,7 @@ An @tech{enumeration} of the naturals between @racket[lo] and @racket[hi].
|
|||
(approximate (range/e 42 64) 5)
|
||||
]}
|
||||
|
||||
@defproc[(thunk/e [size extended-nat?] [ep (-> enum?)]) enum?]{
|
||||
@defproc[(thunk/e [size (or/c exact-nonnegative-integer? +inf.0)] [ep (-> enum?)]) enum?]{
|
||||
|
||||
A delayed @tech{enumeration} identical to @racket[ep]. This is
|
||||
typically used with @racket[fix/e].
|
||||
|
|
@ -357,7 +350,7 @@ typically used with @racket[fix/e].
|
|||
]}
|
||||
|
||||
@defproc*[([(fix/e [f (-> enum? enum?)]) enum?]
|
||||
[(fix/e [size extended-nat?] [f (-> enum? enum?)]) enum?])]{
|
||||
[(fix/e [size (or/c exact-nonnegative-integer? +inf.0)] [f (-> enum? enum?)]) enum?])]{
|
||||
|
||||
An @tech{enumeration} calculated as the fixed-point of @racket[f]. If
|
||||
@racket[size] is not given, it is assumed to be @racket[+inf.0].
|
||||
|
|
@ -372,7 +365,7 @@ An @tech{enumeration} calculated as the fixed-point of @racket[f]. If
|
|||
]}
|
||||
|
||||
@defproc*[([(many/e [e enum?]) enum?]
|
||||
[(many/e [e enum?] [n nat?]) enum?])]{
|
||||
[(many/e [e enum?] [n exact-nonnegative-integer?]) enum?])]{
|
||||
|
||||
An @tech{enumeration} of lists of length @racket[n] of values
|
||||
enumerated by @racket[e]. If @racket[n] is not given, lists of any
|
||||
|
|
@ -530,7 +523,7 @@ enumerations in @racket[es].
|
|||
5)
|
||||
]}
|
||||
|
||||
@defproc[(box-tuples/e [k nat?]) enum?]{
|
||||
@defproc[(box-tuples/e [k exact-nonnegative-integer?]) enum?]{
|
||||
|
||||
An @tech{enumeration} of tuples of naturals of length @racket[k].
|
||||
|
||||
|
|
@ -539,7 +532,7 @@ An @tech{enumeration} of tuples of naturals of length @racket[k].
|
|||
5)
|
||||
]}
|
||||
|
||||
@defproc[(bounded-list/e [k nat?] [n nat?]) enum?]{
|
||||
@defproc[(bounded-list/e [k exact-nonnegative-integer?] [n exact-nonnegative-integer?]) enum?]{
|
||||
|
||||
An @tech{enumeration} of tuples of naturals up to @racket[n] of length @racket[k].
|
||||
|
||||
|
|
@ -548,7 +541,7 @@ An @tech{enumeration} of tuples of naturals up to @racket[n] of length @racket[k
|
|||
5)
|
||||
]}
|
||||
|
||||
@defproc[(nat+/e [lo nat?]) enum?]{
|
||||
@defproc[(nat+/e [lo exact-nonnegative-integer?]) enum?]{
|
||||
|
||||
An @tech{enumeration} of tuples of naturals of larger than @racket[lo].
|
||||
|
||||
|
|
@ -560,7 +553,7 @@ An @tech{enumeration} of tuples of naturals of larger than @racket[lo].
|
|||
@defproc[(fail/e [e exn?]) enum?]{
|
||||
|
||||
An @tech{enumeration} raises @racket[e] if @racket[decode] or
|
||||
@racket[encode] is called with on.
|
||||
@racket[to-nat] is called with on.
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(approximate
|
||||
|
|
|
|||
|
|
@ -18,30 +18,23 @@
|
|||
factorize))
|
||||
|
||||
(define nat? exact-nonnegative-integer?)
|
||||
(define (extended-nat? x)
|
||||
(or (nat? x) (= x +inf.0)))
|
||||
(define extended-nat/c (or/c nat? +inf.0))
|
||||
|
||||
(provide
|
||||
(contract-out
|
||||
[nat?
|
||||
(-> any/c
|
||||
boolean?)]
|
||||
[extended-nat?
|
||||
(-> any/c
|
||||
boolean?)]
|
||||
[enum
|
||||
(-> extended-nat? (-> nat? any/c) (-> any/c nat?)
|
||||
(-> extended-nat/c (-> nat? any/c) (-> any/c nat?)
|
||||
enum?)]
|
||||
[enum?
|
||||
(-> any/c
|
||||
boolean?)]
|
||||
[size
|
||||
(-> enum?
|
||||
extended-nat?)]
|
||||
[decode
|
||||
extended-nat/c)]
|
||||
[from-nat
|
||||
(-> enum? nat?
|
||||
any/c)]
|
||||
[encode
|
||||
[to-nat
|
||||
(-> enum? any/c
|
||||
nat?)]
|
||||
[map/e
|
||||
|
|
@ -126,13 +119,13 @@
|
|||
(-> nat? nat?
|
||||
enum?)]
|
||||
[thunk/e
|
||||
(-> extended-nat? (-> enum?)
|
||||
(-> extended-nat/c (-> enum?)
|
||||
enum?)]
|
||||
[fix/e
|
||||
(case->
|
||||
(-> (-> enum? enum?)
|
||||
enum?)
|
||||
(-> extended-nat? (-> enum? enum?)
|
||||
(-> extended-nat/c (-> enum? enum?)
|
||||
enum?))]
|
||||
[many/e
|
||||
(case->
|
||||
|
|
@ -210,18 +203,18 @@
|
|||
(define (size e)
|
||||
(enum-size e))
|
||||
|
||||
;; decode : enum a, Nat -> a
|
||||
(define (decode e n)
|
||||
;; from-nat : enum a, Nat -> a
|
||||
(define (from-nat e n)
|
||||
(if (and (< n (enum-size e))
|
||||
(>= n 0))
|
||||
((enum-from e) n)
|
||||
(error 'decode
|
||||
(error 'from-nat
|
||||
(string-append "Index into enumerator out of range. "
|
||||
"Tried to decode ~s in an enum of size ~s")
|
||||
n (size e))))
|
||||
|
||||
;; encode : enum a, a -> Nat
|
||||
(define (encode e a)
|
||||
;; to-nat : enum a, a -> Nat
|
||||
(define (to-nat e a)
|
||||
((enum-to e) a))
|
||||
|
||||
;; Helper functions
|
||||
|
|
@ -230,9 +223,9 @@
|
|||
(cond [(empty? es)
|
||||
(enum (size e)
|
||||
(λ (x)
|
||||
(f (decode e x)))
|
||||
(f (from-nat e x)))
|
||||
(λ (n)
|
||||
(encode e (inv-f n))))]
|
||||
(to-nat e (inv-f n))))]
|
||||
[else
|
||||
(define es/e (apply list/e (cons e es)))
|
||||
(map/e
|
||||
|
|
@ -244,19 +237,19 @@
|
|||
|
||||
;; filter/e : enum a, (a -> bool) -> enum a
|
||||
;; xxx size won't be accurate!
|
||||
;; xxx encode is not accurate right now!
|
||||
;; xxx to-nat is not accurate right now!
|
||||
(define (filter/e e p)
|
||||
(enum (size e)
|
||||
(λ (n)
|
||||
(let loop ([i 0]
|
||||
[seen 0])
|
||||
(let ([a (decode e i)])
|
||||
(let ([a (from-nat e i)])
|
||||
(if (p a)
|
||||
(if (= seen n)
|
||||
a
|
||||
(loop (+ i 1) (+ seen 1)))
|
||||
(loop (+ i 1) seen)))))
|
||||
(λ (x) (encode e x))))
|
||||
(λ (x) (to-nat e x))))
|
||||
|
||||
;; except/e : (enum a) a* -> (enum a)
|
||||
;; Everything inside e MUST be in the enumerator or you will get an error
|
||||
|
|
@ -264,16 +257,16 @@
|
|||
(define (except1/e x e)
|
||||
(cond [(= (size e) 0) e]
|
||||
[else
|
||||
(define xi (encode e x))
|
||||
(define (from-nat n)
|
||||
(cond [(< n xi) (decode e n)]
|
||||
[else (decode e (add1 n))]))
|
||||
(define (to-nat y)
|
||||
(define yi (encode e y))
|
||||
(define xi (to-nat e x))
|
||||
(define (from-nat2 n)
|
||||
(cond [(< n xi) (from-nat e n)]
|
||||
[else (from-nat e (add1 n))]))
|
||||
(define (to-nat2 y)
|
||||
(define yi (to-nat e y))
|
||||
(cond [(< yi xi) yi]
|
||||
[(> yi xi) (sub1 yi)]
|
||||
[else (error 'encode "attempted to encode an excepted value")]))
|
||||
(enum (max 0 (sub1 (size e))) from-nat to-nat)]))
|
||||
[else (error 'to-nat "attempted to encode an excepted value")]))
|
||||
(enum (max 0 (sub1 (size e))) from-nat2 to-nat2)]))
|
||||
(foldr except1/e
|
||||
e
|
||||
excepts))
|
||||
|
|
@ -283,13 +276,13 @@
|
|||
(cond [(n . >= . (size e))
|
||||
empty-stream]
|
||||
[else
|
||||
(stream-cons (decode e n)
|
||||
(stream-cons (from-nat e n)
|
||||
(loop (add1 n)))]))
|
||||
(loop 0))
|
||||
|
||||
(define (approximate e n)
|
||||
(for/list ([i (in-range n)])
|
||||
(decode e i)))
|
||||
(from-nat e i)))
|
||||
|
||||
;; to-list : enum a -> listof a
|
||||
;; better be finite
|
||||
|
|
@ -308,9 +301,9 @@
|
|||
(error 'take/e "there aren't ~s elements in ~s" n e))
|
||||
(enum n
|
||||
(λ (k)
|
||||
(decode e k))
|
||||
(from-nat e k))
|
||||
(λ (x)
|
||||
(let ([k (encode e x)])
|
||||
(let ([k (to-nat e x)])
|
||||
(unless (< k n)
|
||||
(error 'take/e "attempted to encode an element not in an enumerator"))
|
||||
k))))
|
||||
|
|
@ -322,12 +315,15 @@
|
|||
(error 'slice/e "bad range in slice/e: size: ~s, lo: ~s, hi: ~s" (size e) lo hi))
|
||||
(enum (hi . - . lo)
|
||||
(λ (n)
|
||||
(decode e (n . + . lo)))
|
||||
(from-nat e (n . + . lo)))
|
||||
(λ (x)
|
||||
(define n (encode e x))
|
||||
(define n (to-nat e x))
|
||||
(unless (and (n . >= . lo)
|
||||
(n . < . hi))
|
||||
(error 'slice/e "attempted to encode an element removed by slice/e: ~s was excepted, originally ~s, but sliced between ~s and ~s" x n lo hi))
|
||||
(error 'slice/e
|
||||
(string-append
|
||||
"attempted to encode an element removed by slice/e:"
|
||||
" ~s was excepted, originally ~s, but sliced between ~s and ~s" x n lo hi)))
|
||||
(n . - . lo))))
|
||||
|
||||
;; below/e
|
||||
|
|
@ -337,9 +333,9 @@
|
|||
(define empty/e
|
||||
(enum 0
|
||||
(λ (n)
|
||||
(error 'decode "absurd"))
|
||||
(error 'from-nat "absurd"))
|
||||
(λ (x)
|
||||
(error 'encode "no elements in the enumerator"))))
|
||||
(error 'to-nat "no elements in the enumerator"))))
|
||||
|
||||
(define (const/e c)
|
||||
(enum 1
|
||||
|
|
@ -348,7 +344,7 @@
|
|||
(λ (x)
|
||||
(if (equal? c x)
|
||||
0
|
||||
(error 'encode "value not in enumerator")))))
|
||||
(error 'to-nat "value not in enumerator")))))
|
||||
|
||||
;; from-list/e :: Listof a -> Gen a
|
||||
;; input list should not contain duplicates
|
||||
|
|
@ -408,8 +404,10 @@
|
|||
#:transparent)
|
||||
|
||||
(struct list-layer
|
||||
(max-index ;; Nat = layer-size + prev-layer-max-index: This is the maximum index into decode for this layer
|
||||
inexhausted-bound ;; Nat, = min (map size inexhausteds): This is the maximum index in the tuple for encode
|
||||
;; Nat = layer-size + prev-layer-max-index: This is the maximum index into decode for this layer
|
||||
(max-index
|
||||
;; Nat, = min (map size inexhausteds): This is the maximum index in the tuple for encode
|
||||
inexhausted-bound
|
||||
exhausteds ;; Vectorof (Enum a, Nat)
|
||||
inexhausteds ;; Vectorof (Enum a, Nat)
|
||||
)
|
||||
|
|
@ -490,9 +488,11 @@
|
|||
(define num-inexhausted
|
||||
(length cur-inexhausteds))
|
||||
(define max-index
|
||||
(prev-max-index . + . (apply *
|
||||
((expt cur-bound num-inexhausted) . - . (expt prev-bound num-inexhausted))
|
||||
(map (compose size car) cur-exhausteds))))
|
||||
(prev-max-index
|
||||
. + .
|
||||
(apply *
|
||||
((expt cur-bound num-inexhausted) . - . (expt prev-bound num-inexhausted))
|
||||
(map (compose size car) cur-exhausteds))))
|
||||
(define cur-layer
|
||||
(list-layer max-index
|
||||
cur-bound
|
||||
|
|
@ -513,11 +513,11 @@
|
|||
|
||||
(define (find-index x e-ps [cur-index 0])
|
||||
(match e-ps
|
||||
['() (error 'encode "invalid term")]
|
||||
['() (error 'to-nat "invalid term")]
|
||||
[(cons (cons e in-e?)
|
||||
more-e-ps)
|
||||
(cond [(in-e? x)
|
||||
(values (encode e x)
|
||||
(values (to-nat e x)
|
||||
cur-index)]
|
||||
[else
|
||||
(find-index x more-e-ps (add1 cur-index))])]))
|
||||
|
|
@ -532,14 +532,14 @@
|
|||
[((upper-bound tb ib eis) e-i)
|
||||
(define (loop low hi)
|
||||
(when (> low hi)
|
||||
(error 'encode "internal bin search bug"))
|
||||
(error 'to-nat "internal bin search bug"))
|
||||
(define mid
|
||||
(quotient (low . + . hi) 2))
|
||||
(define cur
|
||||
(cdr (vector-ref eis mid)))
|
||||
(cond [(low . = . mid)
|
||||
(unless (cur . = . e-i)
|
||||
(error 'encode "internal binary search bug"))
|
||||
(error 'to-nat "internal binary search bug"))
|
||||
mid]
|
||||
[(cur . = . e-i) mid]
|
||||
[(cur . < . e-i) (loop (add1 mid) hi)]
|
||||
|
|
@ -593,7 +593,7 @@
|
|||
(define len (vector-length es))
|
||||
(define-values (q r) (quotient/remainder this-i len))
|
||||
(define this-e (car (vector-ref es r)))
|
||||
(decode this-e (+ q prev-ib)))
|
||||
(from-nat this-e (+ q prev-ib)))
|
||||
(define (enc x)
|
||||
(define-values (index which-e)
|
||||
(find-index x e-ps))
|
||||
|
|
@ -616,14 +616,14 @@
|
|||
(define s2 (size e2))
|
||||
(when (infinite? s1)
|
||||
(error "Only the last enum in a call to disj-append/e can be infinite."))
|
||||
(define (from-nat n)
|
||||
(cond [(< n s1) (decode e1 n)]
|
||||
[else (decode e2 (- n s1))]))
|
||||
(define (to-nat x)
|
||||
(cond [(1? x) (encode e1 x)]
|
||||
[(2? x) (+ (encode e2 x) s1)]
|
||||
[else (error 'encode "bad term")]))
|
||||
(enum (+ s1 s2) from-nat to-nat)])
|
||||
(define (from-nat2 n)
|
||||
(cond [(< n s1) (from-nat e1 n)]
|
||||
[else (from-nat e2 (- n s1))]))
|
||||
(define (to-nat2 x)
|
||||
(cond [(1? x) (to-nat e1 x)]
|
||||
[(2? x) (+ (to-nat e2 x) s1)]
|
||||
[else (error 'to-nat "bad term")]))
|
||||
(enum (+ s1 s2) from-nat2 to-nat2)])
|
||||
(car
|
||||
(foldr1 (λ (e-p1 e-p2)
|
||||
(match* (e-p1 e-p2)
|
||||
|
|
@ -657,12 +657,12 @@
|
|||
(if fst-smaller?
|
||||
(values r q)
|
||||
(values q r)))
|
||||
(cons (decode e1 n1)
|
||||
(decode e2 n2)))
|
||||
(cons (from-nat e1 n1)
|
||||
(from-nat e2 n2)))
|
||||
(define/match (enc p)
|
||||
[((cons x1 x2))
|
||||
(define n1 (encode e1 x1))
|
||||
(define n2 (encode e2 x2))
|
||||
(define n1 (to-nat e1 x1))
|
||||
(define n2 (to-nat e2 x2))
|
||||
(define-values (q r)
|
||||
(if fst-smaller?
|
||||
(values n2 n1)
|
||||
|
|
@ -702,12 +702,12 @@
|
|||
(define n1 fl-root)
|
||||
(define n2 (- n root-sq fl-root))
|
||||
(values n1 n2)]))
|
||||
(cons (decode e1 n1)
|
||||
(decode e2 n2)))
|
||||
(cons (from-nat e1 n1)
|
||||
(from-nat e2 n2)))
|
||||
(define/match (enc p)
|
||||
[((cons x1 x2))
|
||||
(define n1 (encode e1 x1))
|
||||
(define n2 (encode e2 x2))
|
||||
(define n1 (to-nat e1 x1))
|
||||
(define n2 (to-nat e2 x2))
|
||||
(cond [(n1 . < . n2)
|
||||
((n2 . * . n2) . + . n1)]
|
||||
[else
|
||||
|
|
@ -758,7 +758,7 @@
|
|||
(define (search-size sizes n)
|
||||
(define (loop cur)
|
||||
(let* ([lastSize (gvector-ref sizes (- cur 1))]
|
||||
[e2 (f (decode e cur))]
|
||||
[e2 (f (from-nat e cur))]
|
||||
[s (+ lastSize (size e2))])
|
||||
(gvector-add! sizes s)
|
||||
(if (> s n)
|
||||
|
|
@ -770,7 +770,7 @@
|
|||
(define (fill-table sizes n)
|
||||
(let loop ([cur (gvector-count sizes)])
|
||||
(let* ([prevSize (gvector-ref sizes (- cur 1))]
|
||||
[curE (f (decode e cur))]
|
||||
[curE (f (from-nat e cur))]
|
||||
[s (+ prevSize (size curE))])
|
||||
(gvector-add! sizes s)
|
||||
(if (= cur n)
|
||||
|
|
@ -778,7 +778,7 @@
|
|||
(loop (+ cur 1))))))
|
||||
(if (= 0 (size e))
|
||||
empty/e
|
||||
(let ([first (size (f (decode e 0)))])
|
||||
(let ([first (size (f (from-nat e 0)))])
|
||||
(cond
|
||||
[(not (infinite? first))
|
||||
;; memo table caches the size of the dependent enumerators
|
||||
|
|
@ -800,14 +800,14 @@
|
|||
0
|
||||
(gvector-ref sizes (- ind 1)))]
|
||||
[m (- n l)]
|
||||
[x (decode e ind)]
|
||||
[x (from-nat e ind)]
|
||||
[e2 (f x)]
|
||||
[y (decode e2 m)])
|
||||
[y (from-nat e2 m)])
|
||||
(cons x y)))
|
||||
(λ (ab)
|
||||
(let* ([a (car ab)]
|
||||
[b (cdr ab)]
|
||||
[ai (encode e a)]
|
||||
[ai (to-nat e a)]
|
||||
[ei (f a)]
|
||||
[nextSize (size ei)]
|
||||
[sizeUpTo (if (= ai 0)
|
||||
|
|
@ -821,16 +821,16 @@
|
|||
(+ nextSize
|
||||
sizeUp))))))])
|
||||
(+ sizeUpTo
|
||||
(encode ei b))))))]
|
||||
(to-nat ei b))))))]
|
||||
[(not (infinite? (size e)))
|
||||
(enum +inf.0
|
||||
(λ (n)
|
||||
(define-values (q r) (quotient/remainder n (size e)))
|
||||
(cons (decode e r)
|
||||
(decode (f (decode e r)) q)))
|
||||
(cons (from-nat e r)
|
||||
(from-nat (f (from-nat e r)) q)))
|
||||
(λ (ab)
|
||||
(+ (* (size e) (encode (f (car ab)) (cdr ab)))
|
||||
(encode e (car ab)))))]
|
||||
(+ (* (size e) (to-nat (f (car ab)) (cdr ab)))
|
||||
(to-nat e (car ab)))))]
|
||||
[else ;; both infinite, same as cons/e
|
||||
(enum +inf.0
|
||||
(λ (n)
|
||||
|
|
@ -838,15 +838,15 @@
|
|||
[t (tri k)]
|
||||
[l (- n t)]
|
||||
[m (- k l)]
|
||||
[a (decode e l)])
|
||||
[a (from-nat e l)])
|
||||
(cons a
|
||||
(decode (f a) m))))
|
||||
(from-nat (f a) m))))
|
||||
(λ (xs) ;; bijection from nxn -> n, inverse of previous
|
||||
;; (n,m) -> (n+m)(n+m+1)/2 + n
|
||||
(unless (pair? xs)
|
||||
(error 'encode "not a pair"))
|
||||
(let ([l (encode e (car xs))]
|
||||
[m (encode (f (car xs)) (cdr xs))])
|
||||
(error 'to-nat "not a pair"))
|
||||
(let ([l (to-nat e (car xs))]
|
||||
[m (to-nat (f (car xs)) (cdr xs))])
|
||||
(+ (/ (* (+ l m) (+ l m 1))
|
||||
2)
|
||||
l))))]))))
|
||||
|
|
@ -880,7 +880,7 @@
|
|||
(define (search-size sizes n)
|
||||
(define (loop cur)
|
||||
(let* ([lastSize (gvector-ref sizes (- cur 1))]
|
||||
[e2 (f (decode e cur))]
|
||||
[e2 (f (from-nat e cur))]
|
||||
[s (+ lastSize (size e2))])
|
||||
(gvector-add! sizes s)
|
||||
(if (> s n)
|
||||
|
|
@ -892,7 +892,7 @@
|
|||
(define (fill-table sizes n)
|
||||
(let loop ([cur (gvector-count sizes)])
|
||||
(let* ([prevSize (gvector-ref sizes (- cur 1))]
|
||||
[curE (f (decode e cur))]
|
||||
[curE (f (from-nat e cur))]
|
||||
[s (+ prevSize (size curE))])
|
||||
(gvector-add! sizes s)
|
||||
(if (= cur n)
|
||||
|
|
@ -905,7 +905,7 @@
|
|||
;; memo table caches the size of the dependent enumerators
|
||||
;; sizes[n] = # of terms with left side index <= n
|
||||
;; sizes : gvector int
|
||||
(let* ([first (size (f (decode e 0)))]
|
||||
(let* ([first (size (f (from-nat e 0)))]
|
||||
[sizes (gvector first)])
|
||||
(enum (if (infinite? (size e))
|
||||
+inf.0
|
||||
|
|
@ -922,14 +922,14 @@
|
|||
0
|
||||
(gvector-ref sizes (- ind 1)))]
|
||||
[m (- n l)]
|
||||
[x (decode e ind)]
|
||||
[x (from-nat e ind)]
|
||||
[e2 (f x)]
|
||||
[y (decode e2 m)])
|
||||
[y (from-nat e2 m)])
|
||||
(cons x y)))
|
||||
(λ (ab)
|
||||
(let* ([a (car ab)]
|
||||
[b (cdr ab)]
|
||||
[ai (encode e a)]
|
||||
[ai (to-nat e a)]
|
||||
[ei (f a)]
|
||||
[nextSize (size ei)]
|
||||
[sizeUpTo (if (= ai 0)
|
||||
|
|
@ -943,16 +943,16 @@
|
|||
(+ nextSize
|
||||
sizeUp))))))])
|
||||
(+ sizeUpTo
|
||||
(encode ei b))))))]
|
||||
(to-nat ei b))))))]
|
||||
[(not (infinite? (size e)))
|
||||
(enum +inf.0
|
||||
(λ (n)
|
||||
(define-values (q r) (quotient/remainder n (size e)))
|
||||
(cons (decode e r)
|
||||
(decode (f (decode e r)) q)))
|
||||
(cons (from-nat e r)
|
||||
(from-nat (f (from-nat e r)) q)))
|
||||
(λ (ab)
|
||||
(+ (* (size e) (encode (f (car ab)) (cdr ab)))
|
||||
(encode e (car ab)))))]
|
||||
(+ (* (size e) (to-nat (f (car ab)) (cdr ab)))
|
||||
(to-nat e (car ab)))))]
|
||||
[else ;; both infinite, same as cons/e
|
||||
(enum +inf.0
|
||||
(λ (n)
|
||||
|
|
@ -960,15 +960,15 @@
|
|||
[t (tri k)]
|
||||
[l (- n t)]
|
||||
[m (- k l)]
|
||||
[a (decode e l)])
|
||||
[a (from-nat e l)])
|
||||
(cons a
|
||||
(decode (f a) m))))
|
||||
(from-nat (f a) m))))
|
||||
(λ (xs) ;; bijection from nxn -> n, inverse of previous
|
||||
;; (n,m) -> (n+m)(n+m+1)/2 + n
|
||||
(unless (pair? xs)
|
||||
(error 'encode "not a pair"))
|
||||
(let ([l (encode e (car xs))]
|
||||
[m (encode (f (car xs)) (cdr xs))])
|
||||
(error 'to-nat "not a pair"))
|
||||
(let ([l (to-nat e (car xs))]
|
||||
[m (to-nat (f (car xs)) (cdr xs))])
|
||||
(+ (/ (* (+ l m) (+ l m 1))
|
||||
2)
|
||||
l))))])))
|
||||
|
|
@ -1030,9 +1030,9 @@
|
|||
(define promise/e (delay (thunk)))
|
||||
(enum s
|
||||
(λ (n)
|
||||
(decode (force promise/e) n))
|
||||
(from-nat (force promise/e) n))
|
||||
(λ (x)
|
||||
(encode (force promise/e) x))))
|
||||
(to-nat (force promise/e) x))))
|
||||
|
||||
;; fix/e : [size] (enum a -> enum a) -> enum a
|
||||
(define fix/e
|
||||
|
|
@ -1042,9 +1042,9 @@
|
|||
(define self (delay (f/e (fix/e size f/e))))
|
||||
(enum size
|
||||
(λ (n)
|
||||
(decode (force self) n))
|
||||
(from-nat (force self) n))
|
||||
(λ (x)
|
||||
(encode (force self) x)))]))
|
||||
(to-nat (force self) x)))]))
|
||||
|
||||
;; many/e : enum a -> enum (listof a)
|
||||
;; or : enum a, #:length natural -> enum (listof a)
|
||||
|
|
@ -1188,8 +1188,8 @@
|
|||
(take/e nat/e (size e))))
|
||||
|
||||
(map/e
|
||||
(curry map decode es)
|
||||
(curry map encode es)
|
||||
(curry map from-nat es)
|
||||
(curry map to-nat es)
|
||||
(mixed-box-tuples/e nat/es)))
|
||||
|
||||
(define (mixed-box-tuples/e es)
|
||||
|
|
@ -1208,9 +1208,10 @@
|
|||
[e (in-list es)])
|
||||
(cons e i)))
|
||||
|
||||
(define prev-cur-layers (map cons
|
||||
(cons (list-layer 0 0 '() eis) (reverse (rest (reverse layers))))
|
||||
layers))
|
||||
(define prev-cur-layers
|
||||
(map cons
|
||||
(cons (list-layer 0 0 '() eis) (reverse (rest (reverse layers))))
|
||||
layers))
|
||||
|
||||
(define layer/es
|
||||
(for/list ([prev-cur (in-list prev-cur-layers)])
|
||||
|
|
@ -1258,7 +1259,7 @@
|
|||
min-index
|
||||
_)
|
||||
(when (n . < . max-index)
|
||||
(return (decode e (n . - . min-index))))]))))
|
||||
(return (from-nat e (n . - . min-index))))]))))
|
||||
|
||||
(define (enc tup)
|
||||
(define m (apply max tup))
|
||||
|
|
@ -1270,7 +1271,7 @@
|
|||
min-index
|
||||
max-max)
|
||||
(when (m . < . max-max)
|
||||
(return (+ min-index (encode e tup))))]))))
|
||||
(return (+ min-index (to-nat e tup))))]))))
|
||||
|
||||
(enum (apply * (map size es))
|
||||
dec
|
||||
|
|
@ -1309,13 +1310,13 @@
|
|||
(define (dec n)
|
||||
(define-values (q r)
|
||||
(quotient/remainder n fin-size))
|
||||
(define x1 (decode e1 (if fst-finite? r q)))
|
||||
(define x2 (decode e2 (if fst-finite? q r)))
|
||||
(define x1 (from-nat e1 (if fst-finite? r q)))
|
||||
(define x2 (from-nat e2 (if fst-finite? q r)))
|
||||
(cons x1 x2))
|
||||
(define/match (enc p)
|
||||
[((cons x1 x2))
|
||||
(define n1 (encode e1 x1))
|
||||
(define n2 (encode e2 x2))
|
||||
(define n1 (to-nat e1 x1))
|
||||
(define n2 (to-nat e2 x2))
|
||||
(define q (if fst-finite? n2 n1))
|
||||
(define r (if fst-finite? n1 n2))
|
||||
(+ (* fin-size q)
|
||||
|
|
@ -1438,12 +1439,12 @@
|
|||
(define k (length es))
|
||||
(define dec
|
||||
(compose
|
||||
(λ (xs) (map decode es xs))
|
||||
(λ (xs) (map from-nat es xs))
|
||||
(cantor-untuple k)))
|
||||
(define enc
|
||||
(compose
|
||||
(cantor-tuple k)
|
||||
(λ (xs) (map encode es xs))))
|
||||
(λ (xs) (map to-nat es xs))))
|
||||
(enum +inf.0 dec enc)]))
|
||||
|
||||
(define (prime-factorize k)
|
||||
|
|
@ -1499,8 +1500,8 @@
|
|||
(prime-length-box-list/e chunk/es))]))]))
|
||||
|
||||
(define (prime-length-box-list/e es)
|
||||
(map/e (curry map decode es)
|
||||
(curry map encode es)
|
||||
(map/e (curry map from-nat es)
|
||||
(curry map to-nat es)
|
||||
(box-tuples/e (length es))))
|
||||
|
||||
(define (box-tuples/e k)
|
||||
|
|
@ -1538,14 +1539,14 @@
|
|||
(define layer (apply max xs))
|
||||
(define smallest (expt layer k))
|
||||
(define layer/e (bounded-list/e k layer))
|
||||
(smallest . + . (encode layer/e xs))))
|
||||
(smallest . + . (to-nat layer/e xs))))
|
||||
|
||||
(define (box-untuple k)
|
||||
(λ (n)
|
||||
(define layer (integer-root n k))
|
||||
(define smallest (expt layer k))
|
||||
(define layer/e (bounded-list/e k layer))
|
||||
(decode layer/e (n . - . smallest))))
|
||||
(from-nat layer/e (n . - . smallest))))
|
||||
|
||||
(define (nat+/e n)
|
||||
(map/e (λ (k)
|
||||
|
|
@ -1580,7 +1581,7 @@
|
|||
(andmap =
|
||||
nums
|
||||
(map (λ (n)
|
||||
(encode e (decode e n)))
|
||||
(to-nat e (from-nat e n)))
|
||||
nums)))))
|
||||
;; Base Type enumerators
|
||||
(define (between? x low high)
|
||||
|
|
|
|||
|
|
@ -9,28 +9,28 @@
|
|||
;; const/e tests
|
||||
(let ([e (const/e 17)])
|
||||
(test-begin
|
||||
(check-eq? (decode e 0) 17)
|
||||
(check-eq? (from-nat e 0) 17)
|
||||
(check-exn exn:fail?
|
||||
(λ ()
|
||||
(decode e 1)))
|
||||
(check-eq? (encode e 17) 0)
|
||||
(from-nat e 1)))
|
||||
(check-eq? (to-nat e 17) 0)
|
||||
(check-exn exn:fail?
|
||||
(λ ()
|
||||
(encode e 0)))
|
||||
(to-nat e 0)))
|
||||
(check-bijection? e)))
|
||||
|
||||
;; from-list/e tests
|
||||
(let ([e (from-list/e '(5 4 1 8))])
|
||||
(test-begin
|
||||
(check-eq? (decode e 0) 5)
|
||||
(check-eq? (decode e 3) 8)
|
||||
(check-eq? (from-nat e 0) 5)
|
||||
(check-eq? (from-nat e 3) 8)
|
||||
(check-exn exn:fail?
|
||||
(λ () (decode e 4)))
|
||||
(check-eq? (encode e 5) 0)
|
||||
(check-eq? (encode e 8) 3)
|
||||
(λ () (from-nat e 4)))
|
||||
(check-eq? (to-nat e 5) 0)
|
||||
(check-eq? (to-nat e 8) 3)
|
||||
(check-exn exn:fail?
|
||||
(λ ()
|
||||
(encode e 17)))
|
||||
(to-nat e 17)))
|
||||
(check-bijection? e)))
|
||||
|
||||
;; map test
|
||||
|
|
@ -38,23 +38,23 @@
|
|||
|
||||
(test-begin
|
||||
(check-equal? (size nats+1) +inf.0)
|
||||
(check-equal? (decode nats+1 0) 1)
|
||||
(check-equal? (decode nats+1 1) 2)
|
||||
(check-equal? (from-nat nats+1 0) 1)
|
||||
(check-equal? (from-nat nats+1 1) 2)
|
||||
(check-bijection? nats+1))
|
||||
;; encode check
|
||||
(test-begin
|
||||
(check-exn exn:fail?
|
||||
(λ ()
|
||||
(decode nat/e -1))))
|
||||
(from-nat nat/e -1))))
|
||||
|
||||
;; ints checks
|
||||
(test-begin
|
||||
(check-eq? (decode int/e 0) 0) ; 0 -> 0
|
||||
(check-eq? (decode int/e 1) 1) ; 1 -> 1
|
||||
(check-eq? (decode int/e 2) -1) ; 2 -> 1
|
||||
(check-eq? (encode int/e 0) 0)
|
||||
(check-eq? (encode int/e 1) 1)
|
||||
(check-eq? (encode int/e -1) 2)
|
||||
(check-eq? (from-nat int/e 0) 0) ; 0 -> 0
|
||||
(check-eq? (from-nat int/e 1) 1) ; 1 -> 1
|
||||
(check-eq? (from-nat int/e 2) -1) ; 2 -> 1
|
||||
(check-eq? (to-nat int/e 0) 0)
|
||||
(check-eq? (to-nat int/e 1) 1)
|
||||
(check-eq? (to-nat int/e -1) 2)
|
||||
(check-bijection? int/e)) ; -1 -> 2, -3 -> 4
|
||||
|
||||
;; sum tests
|
||||
|
|
@ -96,36 +96,36 @@
|
|||
|
||||
(check-equal? (size bool-or-num) 6)
|
||||
|
||||
(check-equal? (decode bool-or-num 0) #t)
|
||||
(check-equal? (decode bool-or-num 1) 0)
|
||||
(check-equal? (decode bool-or-num 2) #f)
|
||||
(check-equal? (decode bool-or-num 3) 1)
|
||||
(check-equal? (decode bool-or-num 4) 2)
|
||||
(check-equal? (decode bool-or-num 5) 3)
|
||||
(check-equal? (from-nat bool-or-num 0) #t)
|
||||
(check-equal? (from-nat bool-or-num 1) 0)
|
||||
(check-equal? (from-nat bool-or-num 2) #f)
|
||||
(check-equal? (from-nat bool-or-num 3) 1)
|
||||
(check-equal? (from-nat bool-or-num 4) 2)
|
||||
(check-equal? (from-nat bool-or-num 5) 3)
|
||||
|
||||
(check-exn exn:fail?
|
||||
(λ ()
|
||||
(decode bool-or-num 6)))
|
||||
(from-nat bool-or-num 6)))
|
||||
(check-bijection? bool-or-num)
|
||||
|
||||
(check-equal? (size bool-or-nat)
|
||||
+inf.0)
|
||||
(check-equal? (decode bool-or-nat 0) #t)
|
||||
(check-equal? (decode bool-or-nat 1) 0)
|
||||
(check-equal? (from-nat bool-or-nat 0) #t)
|
||||
(check-equal? (from-nat bool-or-nat 1) 0)
|
||||
(check-bijection? bool-or-nat)
|
||||
|
||||
(check-equal? (size odd-or-even)
|
||||
+inf.0)
|
||||
(check-equal? (decode odd-or-even 0) 0)
|
||||
(check-equal? (decode odd-or-even 1) 1)
|
||||
(check-equal? (decode odd-or-even 2) 2)
|
||||
(check-equal? (from-nat odd-or-even 0) 0)
|
||||
(check-equal? (from-nat odd-or-even 1) 1)
|
||||
(check-equal? (from-nat odd-or-even 2) 2)
|
||||
(check-exn exn:fail?
|
||||
(λ ()
|
||||
(decode odd-or-even -1)))
|
||||
(check-equal? (encode odd-or-even 0) 0)
|
||||
(check-equal? (encode odd-or-even 1) 1)
|
||||
(check-equal? (encode odd-or-even 2) 2)
|
||||
(check-equal? (encode odd-or-even 3) 3)
|
||||
(from-nat odd-or-even -1)))
|
||||
(check-equal? (to-nat odd-or-even 0) 0)
|
||||
(check-equal? (to-nat odd-or-even 1) 1)
|
||||
(check-equal? (to-nat odd-or-even 2) 2)
|
||||
(check-equal? (to-nat odd-or-even 3) 3)
|
||||
(check-bijection? odd-or-even)
|
||||
|
||||
(check-bijection? nat-or-bool)
|
||||
|
|
@ -138,7 +138,7 @@
|
|||
(cons (many/e bool/e) list?)))
|
||||
|
||||
(define (test-multi-layered i x)
|
||||
(check-equal? (decode multi-layered i) x))
|
||||
(check-equal? (from-nat multi-layered i) x))
|
||||
(map test-multi-layered
|
||||
(for/list ([i (in-range 31)])
|
||||
i)
|
||||
|
|
@ -165,23 +165,23 @@
|
|||
(cons nat/e number?)))
|
||||
(check-equal? (size bool-or-num) 6)
|
||||
|
||||
(check-equal? (decode bool-or-num 0) #t)
|
||||
(check-equal? (decode bool-or-num 1) #f)
|
||||
(check-equal? (decode bool-or-num 2) 0)
|
||||
(check-equal? (decode bool-or-num 3) 1)
|
||||
(check-equal? (decode bool-or-num 4) 2)
|
||||
(check-equal? (decode bool-or-num 5) 3)
|
||||
(check-equal? (from-nat bool-or-num 0) #t)
|
||||
(check-equal? (from-nat bool-or-num 1) #f)
|
||||
(check-equal? (from-nat bool-or-num 2) 0)
|
||||
(check-equal? (from-nat bool-or-num 3) 1)
|
||||
(check-equal? (from-nat bool-or-num 4) 2)
|
||||
(check-equal? (from-nat bool-or-num 5) 3)
|
||||
|
||||
(check-exn exn:fail?
|
||||
(λ ()
|
||||
(decode bool-or-num 6)))
|
||||
(from-nat bool-or-num 6)))
|
||||
(check-bijection? bool-or-num)
|
||||
|
||||
(check-equal? (size bool-or-nat)
|
||||
+inf.0)
|
||||
(check-equal? (decode bool-or-nat 0) #t)
|
||||
(check-equal? (decode bool-or-nat 1) #f)
|
||||
(check-equal? (decode bool-or-nat 2) 0)
|
||||
(check-equal? (from-nat bool-or-nat 0) #t)
|
||||
(check-equal? (from-nat bool-or-nat 1) #f)
|
||||
(check-equal? (from-nat bool-or-nat 2) 0)
|
||||
(check-bijection? bool-or-nat))
|
||||
|
||||
;; cons/e tests
|
||||
|
|
@ -203,8 +203,8 @@
|
|||
(test-begin
|
||||
|
||||
(check-equal? (size 1*b) 2)
|
||||
(check-equal? (decode 1*b 0) (cons 1 #t))
|
||||
(check-equal? (decode 1*b 1) (cons 1 #f))
|
||||
(check-equal? (from-nat 1*b 0) (cons 1 #t))
|
||||
(check-equal? (from-nat 1*b 1) (cons 1 #f))
|
||||
(check-bijection? 1*b)
|
||||
(check-bijection? b*1)
|
||||
(check-equal? (size bool*bool) 4)
|
||||
|
|
@ -226,7 +226,7 @@
|
|||
;; fair product tests
|
||||
(define-simple-check (check-range? e l u approx)
|
||||
(let ([actual (for/set ([i (in-range l u)])
|
||||
(decode e i))]
|
||||
(from-nat e i))]
|
||||
[expected (list->set approx)])
|
||||
(equal? actual expected)))
|
||||
(test-begin
|
||||
|
|
@ -318,43 +318,43 @@
|
|||
|
||||
(test-begin
|
||||
(check-equal? (size 3-up) 6)
|
||||
(check-equal? (decode 3-up 0) (cons 0 0))
|
||||
(check-equal? (decode 3-up 1) (cons 1 0))
|
||||
(check-equal? (decode 3-up 2) (cons 1 1))
|
||||
(check-equal? (decode 3-up 3) (cons 2 0))
|
||||
(check-equal? (decode 3-up 4) (cons 2 1))
|
||||
(check-equal? (decode 3-up 5) (cons 2 2))
|
||||
(check-equal? (from-nat 3-up 0) (cons 0 0))
|
||||
(check-equal? (from-nat 3-up 1) (cons 1 0))
|
||||
(check-equal? (from-nat 3-up 2) (cons 1 1))
|
||||
(check-equal? (from-nat 3-up 3) (cons 2 0))
|
||||
(check-equal? (from-nat 3-up 4) (cons 2 1))
|
||||
(check-equal? (from-nat 3-up 5) (cons 2 2))
|
||||
(check-bijection? 3-up)
|
||||
|
||||
(check-equal? (size from-3) +inf.0)
|
||||
(check-equal? (decode from-3 0) (cons 0 0))
|
||||
(check-equal? (decode from-3 1) (cons 1 1))
|
||||
(check-equal? (decode from-3 2) (cons 2 2))
|
||||
(check-equal? (decode from-3 3) (cons 0 1))
|
||||
(check-equal? (decode from-3 4) (cons 1 2))
|
||||
(check-equal? (decode from-3 5) (cons 2 3))
|
||||
(check-equal? (decode from-3 6) (cons 0 2))
|
||||
(check-equal? (from-nat from-3 0) (cons 0 0))
|
||||
(check-equal? (from-nat from-3 1) (cons 1 1))
|
||||
(check-equal? (from-nat from-3 2) (cons 2 2))
|
||||
(check-equal? (from-nat from-3 3) (cons 0 1))
|
||||
(check-equal? (from-nat from-3 4) (cons 1 2))
|
||||
(check-equal? (from-nat from-3 5) (cons 2 3))
|
||||
(check-equal? (from-nat from-3 6) (cons 0 2))
|
||||
(check-bijection? from-3)
|
||||
|
||||
(check-equal? (size nats-to) +inf.0)
|
||||
(check-equal? (decode nats-to 0) (cons 0 0))
|
||||
(check-equal? (decode nats-to 1) (cons 1 0))
|
||||
(check-equal? (decode nats-to 2) (cons 1 1))
|
||||
(check-equal? (decode nats-to 3) (cons 2 0))
|
||||
(check-equal? (decode nats-to 4) (cons 2 1))
|
||||
(check-equal? (decode nats-to 5) (cons 2 2))
|
||||
(check-equal? (decode nats-to 6) (cons 3 0))
|
||||
(check-equal? (from-nat nats-to 0) (cons 0 0))
|
||||
(check-equal? (from-nat nats-to 1) (cons 1 0))
|
||||
(check-equal? (from-nat nats-to 2) (cons 1 1))
|
||||
(check-equal? (from-nat nats-to 3) (cons 2 0))
|
||||
(check-equal? (from-nat nats-to 4) (cons 2 1))
|
||||
(check-equal? (from-nat nats-to 5) (cons 2 2))
|
||||
(check-equal? (from-nat nats-to 6) (cons 3 0))
|
||||
(check-bijection? nats-to)
|
||||
|
||||
(check-equal? (size nats-up) +inf.0)
|
||||
(check-equal? (decode nats-up 0) (cons 0 0))
|
||||
(check-equal? (decode nats-up 1) (cons 0 1))
|
||||
(check-equal? (decode nats-up 2) (cons 1 1))
|
||||
(check-equal? (decode nats-up 3) (cons 0 2))
|
||||
(check-equal? (decode nats-up 4) (cons 1 2))
|
||||
(check-equal? (decode nats-up 5) (cons 2 2))
|
||||
(check-equal? (decode nats-up 6) (cons 0 3))
|
||||
(check-equal? (decode nats-up 7) (cons 1 3))
|
||||
(check-equal? (from-nat nats-up 0) (cons 0 0))
|
||||
(check-equal? (from-nat nats-up 1) (cons 0 1))
|
||||
(check-equal? (from-nat nats-up 2) (cons 1 1))
|
||||
(check-equal? (from-nat nats-up 3) (cons 0 2))
|
||||
(check-equal? (from-nat nats-up 4) (cons 1 2))
|
||||
(check-equal? (from-nat nats-up 5) (cons 2 2))
|
||||
(check-equal? (from-nat nats-up 6) (cons 0 3))
|
||||
(check-equal? (from-nat nats-up 7) (cons 1 3))
|
||||
|
||||
(check-bijection? nats-up))
|
||||
|
||||
|
|
@ -380,42 +380,42 @@
|
|||
|
||||
(test-begin
|
||||
(check-equal? (size 3-up-2) 6)
|
||||
(check-equal? (decode 3-up-2 0) (cons 0 0))
|
||||
(check-equal? (decode 3-up-2 1) (cons 1 0))
|
||||
(check-equal? (decode 3-up-2 2) (cons 1 1))
|
||||
(check-equal? (decode 3-up-2 3) (cons 2 0))
|
||||
(check-equal? (decode 3-up-2 4) (cons 2 1))
|
||||
(check-equal? (decode 3-up-2 5) (cons 2 2))
|
||||
(check-equal? (from-nat 3-up-2 0) (cons 0 0))
|
||||
(check-equal? (from-nat 3-up-2 1) (cons 1 0))
|
||||
(check-equal? (from-nat 3-up-2 2) (cons 1 1))
|
||||
(check-equal? (from-nat 3-up-2 3) (cons 2 0))
|
||||
(check-equal? (from-nat 3-up-2 4) (cons 2 1))
|
||||
(check-equal? (from-nat 3-up-2 5) (cons 2 2))
|
||||
|
||||
(check-equal? (encode 3-up-2 (cons 0 0)) 0)
|
||||
(check-equal? (encode 3-up-2 (cons 1 0)) 1)
|
||||
(check-equal? (encode 3-up-2 (cons 1 1)) 2)
|
||||
(check-equal? (encode 3-up-2 (cons 2 0)) 3)
|
||||
(check-equal? (to-nat 3-up-2 (cons 0 0)) 0)
|
||||
(check-equal? (to-nat 3-up-2 (cons 1 0)) 1)
|
||||
(check-equal? (to-nat 3-up-2 (cons 1 1)) 2)
|
||||
(check-equal? (to-nat 3-up-2 (cons 2 0)) 3)
|
||||
|
||||
(check-equal? (size nats-to-2) +inf.0)
|
||||
(check-equal? (encode nats-to-2 (cons 0 0)) 0)
|
||||
(check-equal? (encode nats-to-2 (cons 1 0)) 1)
|
||||
(check-equal? (encode nats-to-2 (cons 1 1)) 2)
|
||||
(check-equal? (encode nats-to-2 (cons 2 0)) 3)
|
||||
(check-equal? (encode nats-to-2 (cons 2 1)) 4)
|
||||
(check-equal? (encode nats-to-2 (cons 2 2)) 5)
|
||||
(check-equal? (encode nats-to-2 (cons 3 0)) 6)
|
||||
(check-equal? (to-nat nats-to-2 (cons 0 0)) 0)
|
||||
(check-equal? (to-nat nats-to-2 (cons 1 0)) 1)
|
||||
(check-equal? (to-nat nats-to-2 (cons 1 1)) 2)
|
||||
(check-equal? (to-nat nats-to-2 (cons 2 0)) 3)
|
||||
(check-equal? (to-nat nats-to-2 (cons 2 1)) 4)
|
||||
(check-equal? (to-nat nats-to-2 (cons 2 2)) 5)
|
||||
(check-equal? (to-nat nats-to-2 (cons 3 0)) 6)
|
||||
|
||||
(check-equal? (decode nats-to-2 0) (cons 0 0))
|
||||
(check-equal? (decode nats-to-2 1) (cons 1 0))
|
||||
(check-equal? (decode nats-to-2 2) (cons 1 1))
|
||||
(check-equal? (decode nats-to-2 3) (cons 2 0))
|
||||
(check-equal? (decode nats-to-2 4) (cons 2 1))
|
||||
(check-equal? (decode nats-to-2 5) (cons 2 2))
|
||||
(check-equal? (decode nats-to-2 6) (cons 3 0)))
|
||||
(check-equal? (from-nat nats-to-2 0) (cons 0 0))
|
||||
(check-equal? (from-nat nats-to-2 1) (cons 1 0))
|
||||
(check-equal? (from-nat nats-to-2 2) (cons 1 1))
|
||||
(check-equal? (from-nat nats-to-2 3) (cons 2 0))
|
||||
(check-equal? (from-nat nats-to-2 4) (cons 2 1))
|
||||
(check-equal? (from-nat nats-to-2 5) (cons 2 2))
|
||||
(check-equal? (from-nat nats-to-2 6) (cons 3 0)))
|
||||
|
||||
;; take/e test
|
||||
(define to-2 (up-to 2))
|
||||
(test-begin
|
||||
(check-equal? (size to-2) 3)
|
||||
(check-equal? (decode to-2 0) 0)
|
||||
(check-equal? (decode to-2 1) 1)
|
||||
(check-equal? (decode to-2 2) 2)
|
||||
(check-equal? (from-nat to-2 0) 0)
|
||||
(check-equal? (from-nat to-2 1) 1)
|
||||
(check-equal? (from-nat to-2 2) 2)
|
||||
(check-bijection? to-2))
|
||||
|
||||
;; slic/e test
|
||||
|
|
@ -432,8 +432,8 @@
|
|||
|
||||
(define not-3 (except/e nat/e 3))
|
||||
(test-begin
|
||||
(check-equal? (decode not-3 0) 0)
|
||||
(check-equal? (decode not-3 3) 4)
|
||||
(check-equal? (from-nat not-3 0) 0)
|
||||
(check-equal? (from-nat not-3 3) 4)
|
||||
(check-bijection? not-3))
|
||||
|
||||
;; fold-enum tests
|
||||
|
|
@ -454,5 +454,5 @@
|
|||
(define emptys/e
|
||||
(many/e empty/e))
|
||||
(test-begin
|
||||
(check-equal? (decode emptys/e 0) '())
|
||||
(check-equal? (from-nat emptys/e 0) '())
|
||||
(check-bijection? emptys/e))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user