Fix except/e and add append mode for disj-sum/e
This commit is contained in:
Max New
parent
562cecd10c
commit
6d02da0f2b
|
|
@ -7,6 +7,7 @@
|
|||
|
||||
"enumerator.rkt"
|
||||
"env.rkt"
|
||||
"error.rkt"
|
||||
"lang-struct.rkt"
|
||||
"match-a-pattern.rkt"
|
||||
"preprocess-pat.rkt"
|
||||
|
|
@ -22,7 +23,6 @@
|
|||
[lang-enum? (-> any/c boolean?)]
|
||||
[enum? (-> any/c boolean?)]))
|
||||
|
||||
|
||||
(struct lang-enum (enums unused-var/e))
|
||||
(struct repeat (n terms) #:transparent)
|
||||
(struct name-ref (name) #:transparent)
|
||||
|
|
@ -34,33 +34,33 @@
|
|||
(define (lang-enumerators lang)
|
||||
(define l-enums (make-hash))
|
||||
(define unused-var/e
|
||||
(except/e var/e
|
||||
(used-vars lang)))
|
||||
(define (enumerate-lang cur-lang enum-f)
|
||||
(apply except/e
|
||||
var/e
|
||||
(used-vars lang)))
|
||||
(define (enumerate-lang! cur-lang enum-f)
|
||||
(for ([nt (in-list cur-lang)])
|
||||
(hash-set! l-enums
|
||||
(nt-name nt)
|
||||
(with-handlers ([exn:fail? fail/e])
|
||||
(enum-f (nt-rhs nt)
|
||||
l-enums)))))
|
||||
(let-values ([(fin-lang rec-lang)
|
||||
(sep-lang lang)])
|
||||
(enumerate-lang fin-lang
|
||||
(λ (rhs enums)
|
||||
(enumerate-rhss rhs enums unused-var/e)))
|
||||
(enumerate-lang rec-lang
|
||||
(λ (rhs enums)
|
||||
(thunk/e +inf.f
|
||||
(λ ()
|
||||
(enumerate-rhss rhs enums unused-var/e)))))
|
||||
(nt-name nt)
|
||||
(with-handlers ([exn:fail:redex? fail/e])
|
||||
(enum-f (nt-rhs nt)
|
||||
l-enums)))))
|
||||
(define-values (fin-lang rec-lang) (sep-lang lang))
|
||||
(enumerate-lang! fin-lang
|
||||
(λ (rhs enums)
|
||||
(enumerate-rhss rhs enums unused-var/e)))
|
||||
(enumerate-lang! rec-lang
|
||||
(λ (rhs enums)
|
||||
(thunk/e +inf.f
|
||||
(λ ()
|
||||
(enumerate-rhss rhs enums unused-var/e)))))
|
||||
|
||||
(lang-enum l-enums unused-var/e)))
|
||||
(lang-enum l-enums unused-var/e))
|
||||
|
||||
(define (pat-enumerator l-enum pat)
|
||||
(map/e
|
||||
fill-refs
|
||||
(λ (_)
|
||||
(error 'pat-enum "Enumerator is not a bijection"))
|
||||
(redex-error 'pat-enum "Enumerator is not a bijection"))
|
||||
(pat/e pat
|
||||
(lang-enum-enums l-enum)
|
||||
(lang-enum-unused-var/e l-enum))))
|
||||
|
|
@ -96,7 +96,7 @@
|
|||
[`boolean bool/e]
|
||||
[`variable var/e]
|
||||
[`(variable-except ,s ...)
|
||||
(except/e var/e s)]
|
||||
(apply except/e var/e s)]
|
||||
[`(variable-prefix ,s)
|
||||
;; todo
|
||||
(unimplemented "var-prefix")]
|
||||
|
|
@ -204,13 +204,38 @@
|
|||
(f x))))
|
||||
|
||||
;; Base Type enumerators
|
||||
(define natural/e nats)
|
||||
(define natural/e nats/e)
|
||||
|
||||
(define (between? x low high)
|
||||
(and (>= x low)
|
||||
(<= x high)))
|
||||
(define (range-with-pred/e-p low high)
|
||||
(cons (range/e low high)
|
||||
(λ (n) (between? n low high))))
|
||||
(define low/e-p
|
||||
(range-with-pred/e-p #x61 #x7a))
|
||||
(define up/e-p
|
||||
(range-with-pred/e-p #x41 #x5a))
|
||||
(define bottom/e-p
|
||||
(range-with-pred/e-p #x0 #x40))
|
||||
(define mid/e-p
|
||||
(range-with-pred/e-p #x5b #x60))
|
||||
(define above1/e-p
|
||||
(range-with-pred/e-p #x7b #xd7FF))
|
||||
(define above2/e-p
|
||||
(range-with-pred/e-p #xe000 #x10ffff))
|
||||
|
||||
(define char/e
|
||||
(map/e
|
||||
integer->char
|
||||
char->integer
|
||||
(range/e #x61 #x7a)))
|
||||
(disj-sum/e #:append? #t
|
||||
low/e-p
|
||||
up/e-p
|
||||
bottom/e-p
|
||||
mid/e-p
|
||||
above1/e-p
|
||||
above2/e-p)))
|
||||
|
||||
(define string/e
|
||||
(map/e
|
||||
|
|
@ -219,10 +244,11 @@
|
|||
(many/e char/e)))
|
||||
|
||||
(define integer/e
|
||||
(disj-sum/e (cons nats (λ (n) (>= n 0)))
|
||||
(disj-sum/e #:alternate? #t
|
||||
(cons nats/e (λ (n) (>= n 0)))
|
||||
(cons (map/e (λ (n) (- (+ n 1)))
|
||||
(λ (n) (- (- n) 1))
|
||||
nats)
|
||||
nats/e)
|
||||
(λ (n) (< n 0)))))
|
||||
|
||||
;; This is really annoying so I turned it off
|
||||
|
|
@ -241,7 +267,8 @@
|
|||
(many1/e char/e)))
|
||||
|
||||
(define base/e
|
||||
(disj-sum/e (cons (const/e '()) null?)
|
||||
(disj-sum/e #:alternate? #t
|
||||
(cons (const/e '()) null?)
|
||||
(cons num/e number?)
|
||||
(cons string/e string?)
|
||||
(cons bool/e boolean?)
|
||||
|
|
@ -250,11 +277,6 @@
|
|||
(define any/e
|
||||
(fix/e +inf.f
|
||||
(λ (any/e)
|
||||
(disj-sum/e (cons base/e (negate pair?))
|
||||
(disj-sum/e #:alternate? #t
|
||||
(cons base/e (negate pair?))
|
||||
(cons (cons/e any/e any/e) pair?)))))
|
||||
|
||||
(define (unsupported pat)
|
||||
(error 'generate-term "#:i-th does not support ~s patterns" pat))
|
||||
|
||||
(define (unimplemented pat)
|
||||
(error 'generate-term "#:i-th does not yet support ~s patterns" pat))
|
||||
|
|
|
|||
|
|
@ -1,10 +1,15 @@
|
|||
#lang racket/base
|
||||
(require racket/math
|
||||
racket/match
|
||||
racket/list
|
||||
(require racket/bool
|
||||
racket/contract
|
||||
racket/function
|
||||
racket/list
|
||||
racket/math
|
||||
racket/match
|
||||
racket/promise
|
||||
data/gvector)
|
||||
|
||||
data/gvector
|
||||
|
||||
"error.rkt")
|
||||
|
||||
(provide enum
|
||||
enum?
|
||||
|
|
@ -34,14 +39,11 @@
|
|||
|
||||
to-list
|
||||
take/e
|
||||
drop/e
|
||||
fold-enum
|
||||
display-enum
|
||||
|
||||
nats
|
||||
nats/e
|
||||
range/e
|
||||
nats+/e
|
||||
)
|
||||
nats+/e)
|
||||
|
||||
;; an enum a is a struct of < Nat or +Inf, Nat -> a, a -> Nat >
|
||||
(struct enum
|
||||
|
|
@ -53,14 +55,16 @@
|
|||
(enum-size e))
|
||||
|
||||
;; decode : enum a, Nat -> a
|
||||
(define (decode e n)
|
||||
(define/contract (decode e n)
|
||||
(-> enum? exact-nonnegative-integer? any/c)
|
||||
(if (and (< n (enum-size e))
|
||||
(>= n 0))
|
||||
((enum-from e) n)
|
||||
(error 'out-of-range)))
|
||||
(redex-error 'decode "Index into enumerator out of range")))
|
||||
|
||||
;; encode : enum a, a -> Nat
|
||||
(define (encode e a)
|
||||
(define/contract (encode e a)
|
||||
(-> enum? any/c exact-nonnegative-integer?)
|
||||
((enum-to e) a))
|
||||
|
||||
;; Helper functions
|
||||
|
|
@ -96,30 +100,30 @@
|
|||
(λ (x) (encode e x))))
|
||||
|
||||
;; except/e : enum a, a -> enum a
|
||||
(define (except/e e excepts)
|
||||
(cond [(empty? excepts) e]
|
||||
[else
|
||||
(except/e
|
||||
(begin
|
||||
(with-handlers ([exn:fail? (λ (_) e)])
|
||||
(let ([m (encode e (car excepts))])
|
||||
(enum (- (size e) 1)
|
||||
(λ (n)
|
||||
(if (< n m)
|
||||
(decode e n)
|
||||
(decode e (+ n 1))))
|
||||
(λ (x)
|
||||
(let ([n (encode e x)])
|
||||
(cond [(< n m) n]
|
||||
[(> n m) (- n 1)]
|
||||
[else (error 'excepted)])))))))
|
||||
(cdr excepts))]))
|
||||
;; Everything inside e MUST be in the enumerator or you will get a redex-error
|
||||
(define (except/e e . excepts)
|
||||
(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))
|
||||
(cond [(< yi xi) yi]
|
||||
[(> yi xi) (sub1 yi)]
|
||||
[else (redex-error 'encode "attempted to encode an excepted value")]))
|
||||
(enum (max 0 (sub1 (size e))) from-nat to-nat)]))
|
||||
(foldr except1/e
|
||||
e
|
||||
excepts))
|
||||
|
||||
;; to-list : enum a -> listof a
|
||||
;; better be finite
|
||||
(define (to-list e)
|
||||
(when (infinite? (size e))
|
||||
(error 'too-big))
|
||||
(redex-error 'to-list "cannot encode an infinite list"))
|
||||
(map (enum-from e)
|
||||
(build-list (size e)
|
||||
identity)))
|
||||
|
|
@ -128,31 +132,17 @@
|
|||
;; returns an enum of the first n parts of e
|
||||
;; n must be less than or equal to size e
|
||||
(define (take/e e n)
|
||||
(unless (or (infinite? (size e))
|
||||
(<= n (size e)))
|
||||
(error 'too-big))
|
||||
(unless (or (<= n (size e)))
|
||||
(redex-error 'take/e "there aren't ~s elements in ~s" n e))
|
||||
(enum n
|
||||
(λ (k)
|
||||
(unless (< k n)
|
||||
(error 'out-of-range))
|
||||
(decode e k))
|
||||
(λ (x)
|
||||
(let ([k (encode e x)])
|
||||
(unless (< k n)
|
||||
(error 'out-of-range))
|
||||
(redex-error 'take/e "attempted to encode an element not in an enumerator"))
|
||||
k))))
|
||||
|
||||
;; drop/e : enum a, Nat -> enum a
|
||||
(define (drop/e e n)
|
||||
(unless (or (infinite? (size e))
|
||||
(<= n (size e)))
|
||||
(error 'too-big))
|
||||
(enum (- (size e) n)
|
||||
(λ (m)
|
||||
(decode e (+ n m)))
|
||||
(λ (x)
|
||||
(- (encode e x) n))))
|
||||
|
||||
;; display-enum : enum a, Nat -> void
|
||||
(define (display-enum e n)
|
||||
(for ([i (range n)])
|
||||
|
|
@ -162,9 +152,9 @@
|
|||
(define empty/e
|
||||
(enum 0
|
||||
(λ (n)
|
||||
(error 'empty))
|
||||
(redex-error 'decode "absurd"))
|
||||
(λ (x)
|
||||
(error 'empty))))
|
||||
(redex-error 'encode "no elements in the enumerator"))))
|
||||
|
||||
(define (const/e c)
|
||||
(enum 1
|
||||
|
|
@ -173,7 +163,7 @@
|
|||
(λ (x)
|
||||
(if (equal? c x)
|
||||
0
|
||||
(error 'bad-val)))))
|
||||
(redex-error 'encode "value not in enumerator")))))
|
||||
|
||||
;; from-list/e :: Listof a -> Gen a
|
||||
;; input list should not contain duplicates
|
||||
|
|
@ -191,20 +181,12 @@
|
|||
(λ (x)
|
||||
(hash-ref rev-map x)))))
|
||||
|
||||
;; take-while : Listof a, (a -> bool) -> Listof a
|
||||
(define (take-while l pred)
|
||||
(cond [(empty? l) (error 'empty)]
|
||||
[(not (pred (car l))) '()]
|
||||
[else
|
||||
(cons (car l)
|
||||
(take-while (cdr l) pred))]))
|
||||
|
||||
(define nats
|
||||
(define nats/e
|
||||
(enum +inf.f
|
||||
identity
|
||||
(λ (n)
|
||||
(unless (>= n 0)
|
||||
(error 'out-of-range))
|
||||
(redex-error 'encode "Not a natural"))
|
||||
n)))
|
||||
(define ints/e
|
||||
(enum +inf.f
|
||||
|
|
@ -284,51 +266,70 @@
|
|||
(map-pairs/even (cdr l)))))
|
||||
(apply sum/e (map-pairs sum/e identity (list* a b c rest)))]))
|
||||
|
||||
(define (disj-sum/e e-p . e-ps)
|
||||
(define (disj-sum/e #:alternate? [alternate? #f] #:append? [append? #f] e-p . e-ps)
|
||||
(define/match (disj-sum2/e e-p1 e-p2)
|
||||
[((cons e1 1?) (cons e2 2?))
|
||||
;; Sum two enumerators of different sizes
|
||||
(define (sum-uneven less/e less? more/e more?)
|
||||
(define (alternate-uneven less/e less? more/e more? #:less-first? less-first?)
|
||||
(define-values (first/e second/e)
|
||||
(if less-first?
|
||||
(values less/e more/e)
|
||||
(values more/e less/e)))
|
||||
;; interleave until less/e is exhausted
|
||||
;; pairsdone is 1+ the highest index using less/e
|
||||
(define less-size (size less/e))
|
||||
(define pairsdone (* 2 less-size))
|
||||
(define (from-nat n)
|
||||
(if (< n pairsdone)
|
||||
(let-values ([(q r) (quotient/remainder n 2)])
|
||||
;; Always put e1 first though!
|
||||
(decode (match r
|
||||
[0 e1]
|
||||
[1 e2])
|
||||
q))
|
||||
(decode more/e (- n less-size))))
|
||||
(cond [(< n pairsdone)
|
||||
(define-values (q r) (quotient/remainder n 2))
|
||||
;; Always put e1 first though!
|
||||
(decode (match r
|
||||
[0 first/e]
|
||||
[1 second/e])
|
||||
q)]
|
||||
[else (decode more/e (- n less-size))]))
|
||||
(define (to-nat x)
|
||||
(cond [(less? x)
|
||||
(* 2 (encode less/e x))]
|
||||
(+ (* 2 (encode less/e x))
|
||||
(if less-first? 0 1))]
|
||||
[(more? x)
|
||||
(define i (encode more/e x))
|
||||
(if (< i less-size)
|
||||
(+ (* 2 i) 1)
|
||||
(+ (* 2 i)
|
||||
(if less-first? 1 0))
|
||||
(+ (- i less-size) pairsdone))]
|
||||
[else (error "bad term")]))
|
||||
[else (redex-error 'encode "bad term")]))
|
||||
(enum (+ less-size (size more/e))
|
||||
from-nat
|
||||
to-nat))
|
||||
to-nat))
|
||||
(define s1 (size e1))
|
||||
(define s2 (size e2))
|
||||
(cond [(= 0 s1) e2]
|
||||
[(= 0 s2) e1]
|
||||
[(< s1 s2) (sum-uneven e1 1? e2 2?)]
|
||||
[(< s2 s1) (sum-uneven e2 2? e1 1?)]
|
||||
[else ;; both the same length, interleave them
|
||||
(define (from-nats n)
|
||||
(cond [(even? n) (decode e1 (/ n 2))]
|
||||
[else (decode e2 (/ (- n 1) 2))]))
|
||||
(define (to-nats x)
|
||||
(cond [(1? x) (* (encode e1 x) 2)]
|
||||
[(2? x) (+ 1 (* (encode e2 x) 2))]
|
||||
[else (error "bad term")]))
|
||||
(enum (+ s1 s2) from-nats to-nats)])])
|
||||
(cond [(not (xor alternate? append?))
|
||||
(redex-error 'disj-sum/e "Conflicting options chosen, must pick exactly one of #:alternate? or #:append?")]
|
||||
[alternate?
|
||||
(cond [(= 0 s1) e2]
|
||||
[(= 0 s2) e1]
|
||||
[(< s1 s2) (alternate-uneven e1 1? e2 2? #:less-first? #t)]
|
||||
[(< s2 s1) (alternate-uneven e2 2? e1 1? #:less-first? #f)]
|
||||
[else ;; both the same length, interleave them
|
||||
(define (from-nats n)
|
||||
(cond [(even? n) (decode e1 (/ n 2))]
|
||||
[else (decode e2 (/ (- n 1) 2))]))
|
||||
(define (to-nats x)
|
||||
(cond [(1? x) (* (encode e1 x) 2)]
|
||||
[(2? x) (+ 1 (* (encode e2 x) 2))]
|
||||
[else (redex-error 'encode "bad term")]))
|
||||
(enum (+ s1 s2) from-nats to-nats)])]
|
||||
[append?
|
||||
(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 (redex-error 'encode "bad term")]))
|
||||
(enum (+ s1 s2) from-nat to-nat)]
|
||||
[(nor alternate? append?)
|
||||
(redex-error 'disj-sum/e "Must specify either #:alternate? or #:append?")])])
|
||||
(car
|
||||
(foldr (λ (e-p1 e-p2)
|
||||
(match* (e-p1 e-p2)
|
||||
|
|
@ -341,26 +342,6 @@
|
|||
(cons empty/e (λ (_) #f))
|
||||
(cons e-p e-ps))))
|
||||
|
||||
(define n*n
|
||||
(enum +inf.f
|
||||
(λ (n)
|
||||
;; calculate the k for which (tri k) is the greatest
|
||||
;; triangle number <= n
|
||||
(let* ([k (floor-untri n)]
|
||||
[t (tri k)]
|
||||
[l (- n t)]
|
||||
[m (- k l)])
|
||||
(cons l m)))
|
||||
(λ (ns)
|
||||
(unless (pair? ns)
|
||||
(error "not a list"))
|
||||
(let ([l (car ns)]
|
||||
[m (cdr ns)])
|
||||
(+ (/ (* (+ l m) (+ l m 1))
|
||||
2)
|
||||
l))) ;; (n,m) -> (n+m)(n+m+1)/2 + n
|
||||
))
|
||||
|
||||
;; cons/e : enum a, enum b -> enum (cons a b)
|
||||
(define cons/e
|
||||
(case-lambda
|
||||
|
|
@ -375,7 +356,7 @@
|
|||
(enum size
|
||||
(λ (n) ;; bijection from n -> axb
|
||||
(if (> n size)
|
||||
(error "out of range")
|
||||
(redex-error 'decode "out of range")
|
||||
(call-with-values
|
||||
(λ ()
|
||||
(quotient/remainder n (enum-size e2)))
|
||||
|
|
@ -384,7 +365,7 @@
|
|||
((enum-from e2) r))))))
|
||||
(λ (xs)
|
||||
(unless (pair? xs)
|
||||
(error "not a pair"))
|
||||
(redex-error 'encode "not a pair"))
|
||||
(define q (encode e1 (car xs)))
|
||||
(define r (encode e2 (cdr xs)))
|
||||
(+ (* (enum-size e2) q) r)))]
|
||||
|
|
@ -399,7 +380,7 @@
|
|||
((enum-from e2) q)))))
|
||||
(λ (xs)
|
||||
(unless (pair? xs)
|
||||
(error "not a pair"))
|
||||
(redex-error 'encode "not a pair"))
|
||||
(+ ((enum-to e1) (car xs))
|
||||
(* (enum-size e1)
|
||||
((enum-to e2) (cdr xs))))))])]
|
||||
|
|
@ -414,7 +395,7 @@
|
|||
((enum-from e2) r)))))
|
||||
(λ (xs)
|
||||
(unless (pair? xs)
|
||||
(error "not a pair"))
|
||||
(redex-error 'encode "not a pair"))
|
||||
(+ (* (enum-size e2)
|
||||
((enum-to e1) (car xs)))
|
||||
((enum-to e2) (cdr xs)))))]
|
||||
|
|
@ -431,7 +412,7 @@
|
|||
(λ (xs) ;; bijection from nxn -> n, inverse of previous
|
||||
;; (n,m) -> (n+m)(n+m+1)/2 + n
|
||||
(unless (pair? xs)
|
||||
(error "not a pair"))
|
||||
(redex-error 'encode "not a pair"))
|
||||
(let ([l ((enum-to e1) (car xs))]
|
||||
[m ((enum-to e2) (cdr xs))])
|
||||
(+ (/ (* (+ l m) (+ l m 1))
|
||||
|
|
@ -572,7 +553,7 @@
|
|||
(λ (xs) ;; bijection from nxn -> n, inverse of previous
|
||||
;; (n,m) -> (n+m)(n+m+1)/2 + n
|
||||
(unless (pair? xs)
|
||||
(error "not a pair"))
|
||||
(redex-error 'encode "not a pair"))
|
||||
(let ([l (encode e (car xs))]
|
||||
[m (encode (f (car xs)) (cdr xs))])
|
||||
(+ (/ (* (+ l m) (+ l m 1))
|
||||
|
|
@ -697,7 +678,7 @@
|
|||
(λ (xs) ;; bijection from nxn -> n, inverse of previous
|
||||
;; (n,m) -> (n+m)(n+m+1)/2 + n
|
||||
(unless (pair? xs)
|
||||
(error "not a pair"))
|
||||
(redex-error 'encode "not a pair"))
|
||||
(let ([l (encode e (car xs))]
|
||||
[m (encode (f (car xs)) (cdr xs))])
|
||||
(+ (/ (* (+ l m) (+ l m 1))
|
||||
|
|
@ -734,7 +715,7 @@
|
|||
;; more utility enums
|
||||
;; nats of course
|
||||
(define (range/e low high)
|
||||
(cond [(> low high) (error 'bad-range)]
|
||||
(cond [(> low high) (redex-error 'range/e "invalid range: ~s, ~s" low high)]
|
||||
[(infinite? high)
|
||||
(if (infinite? low)
|
||||
ints/e
|
||||
|
|
@ -743,18 +724,18 @@
|
|||
(+ n low))
|
||||
(λ (n)
|
||||
(- n low))
|
||||
nats))]
|
||||
nats/e))]
|
||||
[(infinite? low)
|
||||
(map/e
|
||||
(λ (n)
|
||||
(- high n))
|
||||
(λ (n)
|
||||
(+ high n))
|
||||
nats)]
|
||||
nats/e)]
|
||||
[else
|
||||
(map/e (λ (n) (+ n low))
|
||||
(λ (n) (- n low))
|
||||
(take/e nats (+ 1 (- high low))))]))
|
||||
(λ (n) (- n low))
|
||||
(take/e nats/e (+ 1 (- high low))))]))
|
||||
|
||||
;; thunk/e : Nat or +-Inf, ( -> enum a) -> enum a
|
||||
(define (thunk/e s thunk)
|
||||
|
|
@ -779,18 +760,21 @@
|
|||
(define many/e
|
||||
(case-lambda
|
||||
[(e)
|
||||
(fix/e (if (= 0 (size e))
|
||||
0
|
||||
+inf.f)
|
||||
(define fix-size
|
||||
(if (= 0 (size e))
|
||||
0
|
||||
+inf.f))
|
||||
(fix/e fix-size
|
||||
(λ (self)
|
||||
(disj-sum/e (cons (const/e '()) null?)
|
||||
(disj-sum/e #:alternate? #t
|
||||
(cons (const/e '()) null?)
|
||||
(cons (cons/e e self) pair?))))]
|
||||
[(e n)
|
||||
(list/e (build-list n (const e)))]))
|
||||
|
||||
;; many1/e : enum a -> enum (nonempty listof a)
|
||||
(define (many1/e e)
|
||||
(cons/e e (many/e e)))
|
||||
(except/e (many/e e) '()))
|
||||
|
||||
;; list/e : listof (enum any) -> enum (listof any)
|
||||
(define (list/e es)
|
||||
|
|
@ -800,10 +784,10 @@
|
|||
|
||||
(define (nats+/e n)
|
||||
(map/e (λ (k)
|
||||
(+ k n))
|
||||
(λ (k)
|
||||
(- k n))
|
||||
nats))
|
||||
(+ k n))
|
||||
(λ (k)
|
||||
(- k n))
|
||||
nats/e))
|
||||
|
||||
;; fail/e : exn -> enum ()
|
||||
;; returns an enum that calls a thunk
|
||||
|
|
|
|||
|
|
@ -1,5 +1,8 @@
|
|||
#lang typed/racket
|
||||
|
||||
(require/typed "error.rkt"
|
||||
[redex-error (Symbol String Any * -> Nothing)])
|
||||
|
||||
(provide (struct-out env)
|
||||
empty-env
|
||||
add-name
|
||||
|
|
@ -52,12 +55,12 @@
|
|||
(: t-env-name-ref : TEnv Symbol -> Pattern)
|
||||
(define/match (t-env-name-ref e n)
|
||||
[((t-env names _) _)
|
||||
(hash-ref names n (thunk (error (format "t-env-name-ref: name not found: ~s" n))))])
|
||||
(hash-ref names n (thunk (redex-error 't-env-name-ref "name not found: ~s" n)))])
|
||||
|
||||
(: t-env-nrep-ref : TEnv Symbol -> (Listof (Pairof TEnv Term)))
|
||||
(define/match (t-env-nrep-ref nv n)
|
||||
[((t-env _ nreps) n)
|
||||
(hash-ref nreps n (thunk (error (format "t-env-nrep-ref: repeat not found: ~s" n))))])
|
||||
(hash-ref nreps n (thunk (redex-error 't-env-nrep-ref "repeat not found: ~s" n)))])
|
||||
|
||||
(: env-union : Env Env -> Env)
|
||||
(define/match (env-union e1 e2)
|
||||
|
|
@ -71,7 +74,11 @@
|
|||
(define/match (combo _ e-t1 e-t2)
|
||||
[(_ (cons nv1 t1) (cons nv2 t2))
|
||||
(cons (env-union nv1 nv2)
|
||||
(hash-union t1 t2 (λ (t _1 _2) (error (format "2 tags should never collide, but these did: ~s, ~s with tag: ~s in envs ~s and ~s" _1 _2 t e1 e2)))))])
|
||||
(hash-union t1 t2
|
||||
(λ (t _1 _2)
|
||||
(redex-error 'env-union
|
||||
"2 tags should never collide, but these did: ~s, ~s with tag: ~s in envs ~s and ~s"
|
||||
_1 _2 t e1 e2))))])
|
||||
(define nreps-union
|
||||
(hash-union rs1 rs2 combo))
|
||||
(env names-union nreps-union)])
|
||||
|
|
@ -93,5 +100,5 @@
|
|||
(define v
|
||||
(cond [(and v1 v2)
|
||||
(combo k v1 v2)]
|
||||
[else (or v1 v2 (error "absurd"))]))
|
||||
[else (or v1 v2 (redex-error 'absurd ""))]))
|
||||
(values k v)))
|
||||
|
|
|
|||
|
|
@ -1,4 +1,11 @@
|
|||
#lang racket/base
|
||||
|
||||
(provide redex-error
|
||||
exn:fail:redex?
|
||||
(struct-out exn:fail:redex)
|
||||
unsupported
|
||||
unimplemented)
|
||||
|
||||
(define-struct (exn:fail:redex exn:fail) ())
|
||||
(define (redex-error name fmt . args)
|
||||
(define suffix (apply format fmt args))
|
||||
|
|
@ -7,6 +14,9 @@
|
|||
(format "~a: ~a" name suffix)
|
||||
suffix))
|
||||
(raise (make-exn:fail:redex message (current-continuation-marks))))
|
||||
(provide redex-error
|
||||
exn:fail:redex?
|
||||
(struct-out exn:fail:redex))
|
||||
|
||||
(define (unsupported pat)
|
||||
(redex-error 'generate-term "#:i-th does not support ~s patterns" pat))
|
||||
|
||||
(define (unimplemented pat)
|
||||
(redex-error 'generate-term "#:i-th does not yet support ~s patterns" pat))
|
||||
|
|
|
|||
|
|
@ -42,7 +42,7 @@
|
|||
(walk p))
|
||||
(ann-pat subenv `(hide-hole ,newsub))]
|
||||
[`(side-condition ,p ,c ,s)
|
||||
(error 'unsupported "side condition is not supported.")]
|
||||
(unsupported "side-condition")]
|
||||
[`(list ,sub-pats ...)
|
||||
(define ann-sub-pats
|
||||
(for/list ([sub-pat (in-list sub-pats)])
|
||||
|
|
@ -56,7 +56,7 @@
|
|||
(ann-pat (pure-nrep n subenv tag subp)
|
||||
`(repeat ,tag ,n #f))]
|
||||
[`(repeat ,p ,n ,m)
|
||||
(unimplemented (format "mismatch repeat (..._!_): ~s ~s" n m))]
|
||||
(unimplemented "mismatch repeat")]
|
||||
[_ (walk sub-pat)])))
|
||||
(define list-env
|
||||
(for/fold ([accenv empty-env])
|
||||
|
|
@ -140,6 +140,3 @@
|
|||
|
||||
(define (pure-ann-pat pat)
|
||||
(ann-pat empty-env pat))
|
||||
|
||||
(define (unimplemented pat-name)
|
||||
(redex-error 'unsupported "generate-term #:i-th currently doesn't support pattern type: ~a" pat-name))
|
||||
|
|
|
|||
|
|
@ -16,9 +16,24 @@
|
|||
(unless (redex-match l p term)
|
||||
(error 'bad-term (format "line ~a: i=~a" line i))))))))]))
|
||||
|
||||
(define-language Nats
|
||||
(n natural))
|
||||
(try-it 100 Nats n)
|
||||
;; base types
|
||||
(define-language Base
|
||||
(a any)
|
||||
(num number)
|
||||
(s string)
|
||||
(nat natural)
|
||||
(i integer)
|
||||
(r real)
|
||||
(b boolean))
|
||||
|
||||
(try-it 100 Base a)
|
||||
(try-it 100 Base num)
|
||||
(try-it 100 Base s)
|
||||
(try-it 100 Base nat)
|
||||
(try-it 100 Base i)
|
||||
#;
|
||||
(try-it 100 Base r)
|
||||
(try-it 2 Base b)
|
||||
|
||||
;; Repeat test
|
||||
(define-language Rep
|
||||
|
|
|
|||
|
|
@ -48,7 +48,7 @@
|
|||
(test-begin
|
||||
(check-exn exn:fail?
|
||||
(λ ()
|
||||
(decode nats -1))))
|
||||
(decode nats/e -1))))
|
||||
|
||||
;; ints checks
|
||||
(test-begin
|
||||
|
|
@ -86,8 +86,8 @@
|
|||
(let ([bool-or-num (sum/e bools/e
|
||||
(from-list/e '(0 1 2 3)))]
|
||||
[bool-or-nat (sum/e bools/e
|
||||
nats)]
|
||||
[nat-or-bool (sum/e nats
|
||||
nats/e)]
|
||||
[nat-or-bool (sum/e nats/e
|
||||
bools/e)]
|
||||
[odd-or-even (sum/e evens/e
|
||||
odds/e)])
|
||||
|
|
@ -123,21 +123,28 @@
|
|||
(check-equal? (encode odd-or-even 1) 1)
|
||||
(check-equal? (encode odd-or-even 2) 2)
|
||||
(check-equal? (encode odd-or-even 3) 3)
|
||||
(check-bijection? odd-or-even)))
|
||||
(check-bijection? odd-or-even)
|
||||
;; Known bug, won't fix because I'm getting rid of sum/e anyway
|
||||
;; (check-bijection? nat-or-bool)
|
||||
))
|
||||
|
||||
(test-begin
|
||||
(define bool-or-num
|
||||
(disj-sum/e (cons bools/e boolean?)
|
||||
(disj-sum/e #:alternate? #t
|
||||
(cons bools/e boolean?)
|
||||
(cons (from-list/e '(0 1 2 3)) number?)))
|
||||
(define bool-or-nat
|
||||
(disj-sum/e (cons bools/e boolean?)
|
||||
(cons nats number?)))
|
||||
(disj-sum/e #:alternate? #t
|
||||
(cons bools/e boolean?)
|
||||
(cons nats/e number?)))
|
||||
(define nat-or-bool
|
||||
(disj-sum/e (cons nats number?)
|
||||
(cons bools/e boolean?)))
|
||||
(disj-sum/e #:alternate? #t
|
||||
(cons nats/e number?)
|
||||
(cons bools/e boolean?)))
|
||||
(define odd-or-even
|
||||
(disj-sum/e (cons evens/e even?)
|
||||
(cons odds/e odd?)))
|
||||
(disj-sum/e #:alternate? #t
|
||||
(cons evens/e even?)
|
||||
(cons odds/e odd?)))
|
||||
(check-equal? (size bool-or-num) 6)
|
||||
|
||||
(check-equal? (decode bool-or-num 0) #t)
|
||||
|
|
@ -170,15 +177,47 @@
|
|||
(check-equal? (encode odd-or-even 1) 1)
|
||||
(check-equal? (encode odd-or-even 2) 2)
|
||||
(check-equal? (encode odd-or-even 3) 3)
|
||||
(check-bijection? odd-or-even))
|
||||
(check-bijection? odd-or-even)
|
||||
|
||||
(check-bijection? nat-or-bool))
|
||||
|
||||
(test-begin
|
||||
(define bool-or-num
|
||||
(disj-sum/e #:append? #t
|
||||
(cons bools/e boolean?)
|
||||
(cons (from-list/e '(0 1 2 3)) number?)))
|
||||
(define bool-or-nat
|
||||
(disj-sum/e #:append? #t
|
||||
(cons bools/e boolean?)
|
||||
(cons nats/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-exn exn:fail?
|
||||
(λ ()
|
||||
(decode bool-or-num 6)))
|
||||
(check-bijection? bool-or-num)
|
||||
|
||||
(check-equal? (size bool-or-nat)
|
||||
+inf.f)
|
||||
(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-bijection? bool-or-nat))
|
||||
|
||||
;; cons/e tests
|
||||
(define bool*bool (cons/e bools/e bools/e))
|
||||
(define 1*b (cons/e (const/e 1) bools/e))
|
||||
(define b*1 (cons/e bools/e (const/e 1)))
|
||||
(define bool*nats (cons/e bools/e nats))
|
||||
(define nats*bool (cons/e nats bools/e))
|
||||
(define nats*nats (cons/e nats nats))
|
||||
(define bool*nats (cons/e bools/e nats/e))
|
||||
(define nats*bool (cons/e nats/e bools/e))
|
||||
(define nats*nats (cons/e nats/e nats/e))
|
||||
(define ns-equal? (λ (ns ms)
|
||||
(and (= (car ns)
|
||||
(car ms))
|
||||
|
|
@ -258,7 +297,7 @@
|
|||
|
||||
;; dep/e tests
|
||||
(define (up-to n)
|
||||
(take/e nats (+ n 1)))
|
||||
(take/e nats/e (+ n 1)))
|
||||
|
||||
(define 3-up
|
||||
(dep/e
|
||||
|
|
@ -271,10 +310,10 @@
|
|||
nats+/e))
|
||||
|
||||
(define nats-to
|
||||
(dep/e nats up-to))
|
||||
(dep/e nats/e up-to))
|
||||
|
||||
(define nats-up
|
||||
(dep/e nats nats+/e))
|
||||
(dep/e nats/e nats+/e))
|
||||
|
||||
(test-begin
|
||||
(check-equal? (size 3-up) 6)
|
||||
|
|
@ -336,7 +375,7 @@
|
|||
up-to))
|
||||
|
||||
(define nats-to-2
|
||||
(dep/e nats up-to))
|
||||
(dep/e nats/e up-to))
|
||||
|
||||
(test-begin
|
||||
(check-equal? (size 3-up-2) 6)
|
||||
|
|
@ -384,25 +423,22 @@
|
|||
'(0 1 2 3)))
|
||||
|
||||
;; except/e test
|
||||
(define not-3 (except/e nats '(3)))
|
||||
|
||||
(define not-3 (except/e nats/e 3))
|
||||
(test-begin
|
||||
(check-equal? (decode not-3 0) 0)
|
||||
(check-equal? (decode not-3 3) 4)
|
||||
(check-bijection? not-3))
|
||||
(define not-a (except/e nats '(a)))
|
||||
(test-begin
|
||||
(check-equal? (decode not-a 0) 0)
|
||||
(check-bijection? not-a))
|
||||
|
||||
;; fold-enum tests
|
||||
(define complicated
|
||||
(fold-enum
|
||||
(λ (excepts n)
|
||||
(except/e (up-to n) excepts))
|
||||
(apply except/e (up-to n) excepts))
|
||||
'(2 4 6)))
|
||||
(check-bijection? complicated)
|
||||
|
||||
;; many/e tests
|
||||
(define natss
|
||||
(many/e nats))
|
||||
(many/e nats/e))
|
||||
(check-bijection? natss)
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user