Use mixed fair and finite list/e and delete unused test file
This commit is contained in:
Max New
Robby Findler
parent
6c618efddd
commit
74a2b677e8
|
|
@ -155,7 +155,7 @@
|
|||
[`(cross ,s)
|
||||
(lang-enum-get-cross-enum l-enum s)]
|
||||
[`(list ,sub-pats ...)
|
||||
(list/e
|
||||
(apply list/e
|
||||
(for/list ([sub-pat (in-list sub-pats)])
|
||||
(match sub-pat
|
||||
[`(repeat ,pat #f #f)
|
||||
|
|
|
|||
|
|
@ -104,7 +104,7 @@
|
|||
(λ (n)
|
||||
(encode e (inv-f n))))]
|
||||
[else
|
||||
(define es/e (list/e (cons e es)))
|
||||
(define es/e (apply list/e (cons e es)))
|
||||
(map/e
|
||||
(λ (xs)
|
||||
(apply f xs))
|
||||
|
|
@ -497,7 +497,7 @@
|
|||
;; Traversal (maybe come up with a better name
|
||||
;; traverse/e : (a -> enum b), (listof a) -> enum (listof b)
|
||||
(define (traverse/e f xs)
|
||||
(list/e (map f xs)))
|
||||
(apply list/e (map f xs)))
|
||||
|
||||
;; Hash Traversal
|
||||
;; hash-traverse/e : (a -> enum b), (hash[k] -o> a) -> enum (hash[k] -o> b)
|
||||
|
|
@ -839,7 +839,7 @@
|
|||
(disj-sum/e (cons (const/e '()) null?)
|
||||
(cons (cons/e e self) pair?))))]
|
||||
[(e n)
|
||||
(list/e (build-list n (const e)))]))
|
||||
(apply list/e (build-list n (const e)))]))
|
||||
|
||||
;; many1/e : enum a -> enum (nonempty listof a)
|
||||
(define (many1/e e)
|
||||
|
|
@ -917,25 +917,113 @@
|
|||
(loop xs -1 '()))
|
||||
|
||||
;; list/e : listof (enum any) -> enum (listof any)
|
||||
(define (list/e es)
|
||||
(define (list/e . es)
|
||||
(define l (length es))
|
||||
(cond
|
||||
[(= l 0) (const/e '())]
|
||||
[(= l 1) (map/e list car (car es))]
|
||||
[(all-infinite? es) (apply box-list/e es)]
|
||||
[(all-finite? es) (apply nested-cons-list/e es)]
|
||||
[else
|
||||
(define split-point (quotient l 2))
|
||||
(define-values (left right) (split-at es split-point))
|
||||
(map/e
|
||||
(λ (pr) (append (car pr) (cdr pr)))
|
||||
(λ (lst)
|
||||
(define-values (left right) (split-at lst split-point))
|
||||
(cons left right))
|
||||
(cons/e (list/e left) (list/e right)))]))
|
||||
(define tagged-es
|
||||
(for/list ([i (in-naturals)]
|
||||
[e (in-list es)])
|
||||
(cons e i)))
|
||||
(define-values (inf-eis fin-eis)
|
||||
(partition (compose infinite?
|
||||
size
|
||||
car)
|
||||
tagged-es))
|
||||
(define inf-es (map car inf-eis))
|
||||
(define inf-is (map cdr inf-eis))
|
||||
(define fin-es (map car fin-eis))
|
||||
(define fin-is (map cdr fin-eis))
|
||||
|
||||
(define inf-slots
|
||||
(reverse
|
||||
(let loop ([inf-is inf-is]
|
||||
[fin-is fin-is]
|
||||
[acc '()])
|
||||
(match* (inf-is fin-is)
|
||||
[('() '()) acc]
|
||||
[((cons _ _) '())
|
||||
(append (for/list ([_ (in-list inf-is)]) #t) acc)]
|
||||
[('() (cons _ _))
|
||||
(append (for/list ([_ (in-list fin-is)]) #f) acc)]
|
||||
[((cons ii rest-iis) (cons fi rest-fis))
|
||||
(cond [(ii . < . fi)
|
||||
(loop rest-iis
|
||||
fin-is
|
||||
(cons #t acc))]
|
||||
[else
|
||||
(loop inf-is
|
||||
rest-fis
|
||||
(cons #f acc))])]))))
|
||||
|
||||
(define/match (reconstruct infs-fins)
|
||||
[((cons infs fins))
|
||||
(let loop ([infs infs]
|
||||
[fins fins]
|
||||
[inf?s inf-slots]
|
||||
[acc '()])
|
||||
(match inf?s
|
||||
['() (reverse acc)]
|
||||
[(cons inf? rest)
|
||||
(cond [inf?
|
||||
(loop (cdr infs)
|
||||
fins
|
||||
rest
|
||||
(cons (car infs) acc))]
|
||||
[else
|
||||
(loop infs
|
||||
(cdr fins)
|
||||
rest
|
||||
(cons (car fins) acc))])]))])
|
||||
(define (deconstruct xs)
|
||||
(let loop ([xs xs]
|
||||
[inf-acc '()]
|
||||
[fin-acc '()]
|
||||
[inf?s inf-slots])
|
||||
(match* (xs inf?s)
|
||||
[('() '()) (cons (reverse inf-acc)
|
||||
(reverse fin-acc))]
|
||||
[((cons x rest-xs) (cons inf? rest-inf?s))
|
||||
(cond [inf?
|
||||
(loop rest-xs
|
||||
(cons x inf-acc)
|
||||
fin-acc
|
||||
rest-inf?s)]
|
||||
[else
|
||||
(loop rest-xs
|
||||
inf-acc
|
||||
(cons x fin-acc)
|
||||
rest-inf?s)])])))
|
||||
(map/e reconstruct
|
||||
deconstruct
|
||||
(cons/e (apply list/e inf-es)
|
||||
(apply list/e fin-es)))]))
|
||||
|
||||
(define/contract (all-infinite? es)
|
||||
((listof enum?) . -> . boolean?)
|
||||
(define (nested-cons-list/e . es)
|
||||
(define l (length es))
|
||||
(define split-point (quotient l 2))
|
||||
(define-values (left right) (split-at es split-point))
|
||||
(map/e
|
||||
(λ (pr) (append (car pr) (cdr pr)))
|
||||
(λ (lst)
|
||||
(define-values (left right) (split-at lst split-point))
|
||||
(cons left right))
|
||||
(cons/e (apply list/e left) (apply list/e right))))
|
||||
|
||||
|
||||
(define (all-infinite? es)
|
||||
(all-sizes-something? infinite? es))
|
||||
|
||||
(define (all-finite? es)
|
||||
(all-sizes-something? (negate infinite?) es))
|
||||
|
||||
(define (all-sizes-something? p? es)
|
||||
(for/and ([e (in-list es)])
|
||||
(infinite? (size e))))
|
||||
(p? (size e))))
|
||||
|
||||
;; Fair tupling via generalized cantor n-tupling
|
||||
;; ordering is monotonic in the sum of the elements of the list
|
||||
|
|
@ -943,8 +1031,7 @@
|
|||
(define all-inf? (all-infinite? es))
|
||||
(cond [(empty? es) (const/e '())]
|
||||
[(not all-inf?)
|
||||
;; TODO: improve mixed finite/infinite
|
||||
(list/e es)]
|
||||
(apply list/e es)]
|
||||
[else
|
||||
(define k (length es))
|
||||
(define dec
|
||||
|
|
@ -962,7 +1049,7 @@
|
|||
(define (box-list/e . es)
|
||||
(define all-inf? (all-infinite? es))
|
||||
(cond [(empty? es) (const/e '())]
|
||||
[(not all-inf?) (list/e es)]
|
||||
[(not all-inf?) (apply list/e es)]
|
||||
[else
|
||||
(define k (length es))
|
||||
(define dec
|
||||
|
|
@ -988,7 +1075,7 @@
|
|||
(map/e
|
||||
(curry cons bound)
|
||||
cdr
|
||||
(list/e
|
||||
(apply list/e
|
||||
(for/list ([_ (in-range (sub1 len))])
|
||||
bounded/e))))
|
||||
(define first-not-max/e
|
||||
|
|
|
|||
|
|
@ -1,243 +0,0 @@
|
|||
#lang racket/base
|
||||
(require rackunit
|
||||
redex/reduction-semantics)
|
||||
|
||||
(define-language Base
|
||||
(x a b c)
|
||||
(y d e f))
|
||||
|
||||
;; Simple repeats
|
||||
(define-extended-language S1 Base
|
||||
(s (x ... y ...)))
|
||||
|
||||
#;
|
||||
(append/e (many/e (enum x))
|
||||
(many/e (enum y)))
|
||||
|
||||
(define-extended-language S2 Base
|
||||
(s (x ..._1 y ..._1)))
|
||||
|
||||
#;
|
||||
(dep/e nats
|
||||
(λ (len)
|
||||
(append/e (listof n (enum x))
|
||||
(listof n (enum y)))))
|
||||
|
||||
(define-extended-language S3 Base
|
||||
(s (x_1 ..._1 x_1 ..._1)))
|
||||
|
||||
#;
|
||||
(dep/e nats
|
||||
(λ (len)
|
||||
(dep/e (listof n (enum x))
|
||||
(λ (x-vals)
|
||||
(append/e x-vals
|
||||
x-vals)))))
|
||||
|
||||
;; Nesting!
|
||||
(define-extended-language S4 Base
|
||||
(s ((x ...) ... (y ...) ...)))
|
||||
|
||||
#;
|
||||
(append/e (many/e (append/e (many/e (enum x))))
|
||||
(many/e (append/e (many/e (enum y)))))
|
||||
|
||||
(define-extended-language S5 Base
|
||||
(s ((x ...) ..._1 (y ...) ..._1)))
|
||||
|
||||
#;
|
||||
(dep/e nats
|
||||
(λ (len)
|
||||
(append/e (listof n (append/e (many (enum x))))
|
||||
(listof n (append/e (many (enum y)))))))
|
||||
|
||||
(define-extended-language S6 Base
|
||||
(s ((x ..._1) ..._2 (y ..._1) ..._2)))
|
||||
|
||||
|
||||
;; mapM/e : (a -> enum b) -> [a] -> ([a] -> enum [b])
|
||||
;; (compose mapM/e mapM/e) : (a -> enum b) -> [[a]] -> ([[a]] -> enum [[b]])
|
||||
;;
|
||||
#;
|
||||
(dep/e nats
|
||||
(λ (len2)
|
||||
(dep/e (listof nats)
|
||||
(λ (len1s)
|
||||
(append/e (listof len2
|
||||
(mapM/e (λ (len1)
|
||||
(listof len1 (enum x)))
|
||||
len1s))
|
||||
(listof len2
|
||||
(mapM/e (λ (len1)
|
||||
(listof len1 (enum y)))
|
||||
len1s)))))) )
|
||||
|
||||
;;
|
||||
(define-extended-language S7 Base
|
||||
(s ((x_1 ..._1) ..._2 (x_1 ..._1) ..._2)))
|
||||
|
||||
|
||||
#;
|
||||
(dep/e nats
|
||||
(λ (len2)
|
||||
(dep/e (listof nats)
|
||||
(λ (len1s)
|
||||
(dep/e
|
||||
;; We need to enumerate them in the context of the outermost "rigid"/named pattern
|
||||
(listof len2
|
||||
(mapM/e (λ (len1)
|
||||
(listof len1 (enum x))))) ;; this is an important part!!!!
|
||||
;; [[x]]
|
||||
;; we're lucky that they're the same this time, what if it's more complicated though?
|
||||
(λ (xss)
|
||||
(append/e xss
|
||||
xss)))))))
|
||||
|
||||
;; This one has different underlying patterns
|
||||
(define-extended-language S8 Base
|
||||
(s (((x_1 y) ..._1) ..._2
|
||||
(x_1 ..._1) ..._2)))
|
||||
|
||||
#;
|
||||
(dep/e nats
|
||||
(λ (len2)
|
||||
(dep/e (listof nats)
|
||||
(λ (len1s)
|
||||
(dep/e
|
||||
;; We need to enumerate them in the context of the outermost "rigid"/named pattern
|
||||
(listof len2
|
||||
(mapM/e (λ (len1)
|
||||
(listof len1 (enum x))))) ;; this is an important part!!!!
|
||||
;; [[x]]
|
||||
(λ (xss)
|
||||
(append/e ((compose mapM/e mapM/e)
|
||||
(λ (x)
|
||||
(map/e (λ (y)
|
||||
(cons x y))
|
||||
(enum y)))
|
||||
(xss))
|
||||
((compose mapM/e mapM/e)
|
||||
(λ (x)
|
||||
(const/enum x))
|
||||
xss))))))))
|
||||
|
||||
|
||||
;; This one has different patterns that differ at a higher branch
|
||||
(define-extended-language S9 Base
|
||||
(s ((x_1 ..._1 y) ..._2
|
||||
(x_1 ..._1) ..._2)))
|
||||
|
||||
#;
|
||||
(dep/e nats
|
||||
(λ (len2)
|
||||
(dep/e (listof len2 nats)
|
||||
(λ (len1s)
|
||||
(dep/e
|
||||
(listof len2
|
||||
(mapM/e (λ (len1)
|
||||
(listof len1 (enum x)))
|
||||
len1s))
|
||||
(λ (x1ss)
|
||||
(append/e
|
||||
(mapM/e
|
||||
(λ (x1s)
|
||||
(append/e (mapM/e const x1s)
|
||||
(singleton/e 1 (enum y)))))
|
||||
((compose mapM/e mapM/e)
|
||||
const/e
|
||||
x1ss))))))))
|
||||
|
||||
|
||||
;; Next lets make the insides even more compilcated
|
||||
(define-extended-language S10 Base
|
||||
(s (((y_2
|
||||
(x_1 y) ..._1
|
||||
y ...) ..._2
|
||||
y ...
|
||||
(y
|
||||
(x_1 (x_1 x_1)) ..._1
|
||||
y_2) ..._2)
|
||||
y ...
|
||||
y)))
|
||||
|
||||
#;
|
||||
;; This one's a doozy so hopefully it will be similar to the general construction
|
||||
(dep/e (vals/e ((iterate 0) nats))
|
||||
(λ (len2)
|
||||
;; as long as multiple parts of the list need access to the
|
||||
;; same vars you need to keep everyone within the dep/e
|
||||
|
||||
;; as you descend deeper you need to do that many listofs
|
||||
;; when you enumerate so in the algorithm you'll need to
|
||||
;; keep track of that.
|
||||
|
||||
;; you also must enumerate all variables that are at that
|
||||
;; depth, in this way named vals and named repeats are similar
|
||||
(dep/e (vals/e ((iterate 1 (curry many/e
|
||||
len2)) nats)
|
||||
((iterate 1 (curry many/e
|
||||
len2)) (enum y)))
|
||||
(λ (len1s ys)
|
||||
(dep/e
|
||||
(vals/e (((iterate 0 mapM/e)
|
||||
(λ (len2)
|
||||
((iterate 1 mapM/e)
|
||||
(λ (len1)
|
||||
(listof len1 (enum x))))
|
||||
len1s))
|
||||
len2))
|
||||
|
||||
;; 2 levels deep
|
||||
(λ (xss)
|
||||
(append/e
|
||||
;;
|
||||
((iterate 0 mapM/e)
|
||||
(λ (len2)
|
||||
((iterate 1 mapM/e)
|
||||
(λ (len1 y xs)
|
||||
(append/e
|
||||
(singleton/e (const/e y))
|
||||
(mapM/e (λ (x)
|
||||
(list/e (const/e x)
|
||||
(enum y)))
|
||||
xs)
|
||||
(many y)))
|
||||
ys
|
||||
xss))
|
||||
len2)
|
||||
(many (enum y))
|
||||
;; The complications of the above iterate
|
||||
;; mapM/e's might not be necessary so I'm not using them here
|
||||
(mapM/e
|
||||
(λ (y xs)
|
||||
(append/e
|
||||
(singleton/e (enum y))
|
||||
(mapM/e
|
||||
(λ (x)
|
||||
(list/e (const/e x)
|
||||
(list/e x x)))
|
||||
xs)
|
||||
(mapM/e
|
||||
const/e
|
||||
ys)))
|
||||
ys
|
||||
xss)
|
||||
(many (enum y))
|
||||
(singleton/e (enum y)))))))))
|
||||
|
||||
|
||||
;; Then have them be 3 wide instead of 2
|
||||
#;
|
||||
(define-extended-language S11 Base
|
||||
(s ((x_1 ..._1 y) ..._2
|
||||
(x_1 ..._1) ..._2)))
|
||||
|
||||
;; We should also do 3 deep
|
||||
|
||||
#;
|
||||
|
||||
|
||||
;; Nesting something within itself, yikes!
|
||||
(define-extended-language S12 Base
|
||||
(s ((x_1 ..._1 y) ..._2
|
||||
(x_1 ..._1) ..._2)))
|
||||
|
|
@ -323,6 +323,12 @@
|
|||
(check-equal? (list->inc-set '(2 0 1 2)) '(2 3 5 8))
|
||||
(check-equal? (inc-set->list '(2 3 5 8)) '(2 0 1 2)))
|
||||
|
||||
;; mixed finite/infinite list/e tests
|
||||
(test-begin
|
||||
(check-bijection? (list/e bool/e (cons/e bool/e bool/e) (fin/e 'foo 'bar 'baz)))
|
||||
(check-bijection? (list/e nats/e string/e (many/e bool/e)))
|
||||
(check-bijection? (list/e bool/e nats/e ints/e string/e (cons/e bool/e bool/e))))
|
||||
|
||||
;; multi-arg map/e test
|
||||
(define sums/e
|
||||
(map/e
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user