Removed tabs from redex enum code

This commit is contained in:
Max New 2013-05-13 21:14:48 -05:00
parent d174a0c0a0
commit e86e47a968
2 changed files with 941 additions and 941 deletions

View File

@ -1,11 +1,11 @@
#lang racket/base #lang racket/base
(require racket/contract (require racket/contract
racket/list racket/list
racket/match racket/match
racket/function racket/function
"lang-struct.rkt" "lang-struct.rkt"
"match-a-pattern.rkt" "match-a-pattern.rkt"
"enumerator.rkt") "enumerator.rkt")
(provide (provide
(contract-out (contract-out
@ -19,18 +19,18 @@
(define (lang-enumerators nts) (define (lang-enumerators nts)
(let* ([l-enums (make-hash)] (let* ([l-enums (make-hash)]
[rec-nt-terms (find-recs nts)] [rec-nt-terms (find-recs nts)]
[sorted-nts (sort-nt-terms nts rec-nt-terms)]) [sorted-nts (sort-nt-terms nts rec-nt-terms)])
(foldl (foldl
(λ (nt m) (λ (nt m)
(hash-set (hash-set
m m
(nt-name nt) (nt-name nt)
(with-handlers (with-handlers
([exn:fail? fail/enum]) ([exn:fail? fail/enum])
(rec-pat/enum `(nt ,(nt-name nt)) (rec-pat/enum `(nt ,(nt-name nt))
sorted-nts sorted-nts
rec-nt-terms)))) rec-nt-terms))))
(hash) (hash)
sorted-nts))) sorted-nts)))
@ -39,14 +39,14 @@
(define (pat-enumerator lang-enums pat) (define (pat-enumerator lang-enums pat)
(enum-names pat (enum-names pat
(sep-names pat) (sep-names pat)
lang-enums)) lang-enums))
(define (rec-pat/enum pat nts rec-nt-terms) (define (rec-pat/enum pat nts rec-nt-terms)
(enum-names pat (enum-names pat
nts nts
(sep-names pat) (sep-names pat)
rec-nt-terms)) rec-nt-terms))
;; find-recs : lang -> (hash symbol -o> (assoclist rhs bool)) ;; find-recs : lang -> (hash symbol -o> (assoclist rhs bool))
@ -57,50 +57,50 @@
[(n) (is-rec? n (hash))] [(n) (is-rec? n (hash))]
[(nt seen) [(nt seen)
(or (seen? seen (nt-name nt)) (or (seen? seen (nt-name nt))
(ormap (ormap
(λ (rhs) (λ (rhs)
(let rec ([pat (rhs-pattern rhs)]) (let rec ([pat (rhs-pattern rhs)])
(match-a-pattern (match-a-pattern
pat pat
[`any #f] [`any #f]
[`number #f] [`number #f]
[`string #f] [`string #f]
[`natural #f] [`natural #f]
[`integer #f] [`integer #f]
[`real #f] [`real #f]
[`boolean #f] [`boolean #f]
[`variable #f] [`variable #f]
[`(variable-except ,s ...) #f] [`(variable-except ,s ...) #f]
[`(variable-prefix ,s) #f] [`(variable-prefix ,s) #f]
[`variable-not-otherwise-mentioned #f] [`variable-not-otherwise-mentioned #f]
[`hole #f] [`hole #f]
[`(nt ,id) [`(nt ,id)
(is-rec? (make-nt (is-rec? (make-nt
id id
(lookup nt-pats id)) (lookup nt-pats id))
(add-seen seen (add-seen seen
(nt-name nt)))] (nt-name nt)))]
[`(name ,name ,pat) [`(name ,name ,pat)
(rec pat)] (rec pat)]
[`(mismatch-name ,name ,pat) [`(mismatch-name ,name ,pat)
(rec pat)] (rec pat)]
[`(in-hole ,p1 ,p2) [`(in-hole ,p1 ,p2)
(or (rec p1) (or (rec p1)
(rec p2))] (rec p2))]
[`(hide-hole ,p) (rec p)] [`(hide-hole ,p) (rec p)]
[`(side-condition ,p ,g ,e) ;; error [`(side-condition ,p ,g ,e) ;; error
(unsupported/enum pat)] (unsupported/enum pat)]
[`(cross ,s) [`(cross ,s)
(unsupported/enum pat)] ;; error (unsupported/enum pat)] ;; error
[`(list ,sub-pats ...) [`(list ,sub-pats ...)
(ormap (λ (sub-pat) (ormap (λ (sub-pat)
(match sub-pat (match sub-pat
[`(repeat ,pat ,name ,mismatch) [`(repeat ,pat ,name ,mismatch)
(rec pat)] (rec pat)]
[else (rec sub-pat)])) [else (rec sub-pat)]))
sub-pats)] sub-pats)]
[(? (compose not pair?)) #f]))) [(? (compose not pair?)) #f])))
(nt-rhs nt)))])) (nt-rhs nt)))]))
(define (calls-rec? rhs recs) (define (calls-rec? rhs recs)
(let rec ([pat (rhs-pattern rhs)]) (let rec ([pat (rhs-pattern rhs)])
(match-a-pattern (match-a-pattern
@ -118,43 +118,43 @@
[`variable-not-otherwise-mentioned #f] [`variable-not-otherwise-mentioned #f]
[`hole #f] [`hole #f]
[`(nt ,id) [`(nt ,id)
(hash-ref recs id)] (hash-ref recs id)]
[`(name ,name ,pat) [`(name ,name ,pat)
(rec pat)] (rec pat)]
[`(mismatch-name ,name ,pat) [`(mismatch-name ,name ,pat)
(rec pat)] (rec pat)]
[`(in-hole ,p1 ,p2) [`(in-hole ,p1 ,p2)
(or (rec p1) (or (rec p1)
(rec p2))] (rec p2))]
[`(hide-hole ,p) (rec p)] [`(hide-hole ,p) (rec p)]
[`(side-condition ,p ,g ,e) ;; error [`(side-condition ,p ,g ,e) ;; error
(rec p)] (rec p)]
[`(cross ,s) [`(cross ,s)
(unsupported/enum pat)] ;; error (unsupported/enum pat)] ;; error
[`(list ,sub-pats ...) [`(list ,sub-pats ...)
(ormap (λ (sub-pat) (ormap (λ (sub-pat)
(match sub-pat (match sub-pat
[`(repeat ,pat ,name ,mismatch) [`(repeat ,pat ,name ,mismatch)
(rec pat)] (rec pat)]
[else (rec sub-pat)])) [else (rec sub-pat)]))
sub-pats)] sub-pats)]
[(? (compose not pair?)) #f]))) [(? (compose not pair?)) #f])))
(define (seen? m s) (define (seen? m s)
(hash-ref m s #f)) (hash-ref m s #f))
(define (add-seen m s) (define (add-seen m s)
(hash-set m s #t)) (hash-set m s #t))
(let ([recs (let ([recs
(foldl (foldl
(λ (nt m) (λ (nt m)
(hash-set m (nt-name nt) (is-rec? nt))) (hash-set m (nt-name nt) (is-rec? nt)))
(hash) nt-pats)]) (hash) nt-pats)])
(foldl (foldl
(λ (nt m) (λ (nt m)
(let ([rhs (nt-rhs nt)]) (let ([rhs (nt-rhs nt)])
(hash-set m (nt-name nt) (hash-set m (nt-name nt)
(map (λ (rhs) (map (λ (rhs)
(cons rhs (calls-rec? rhs recs))) (cons rhs (calls-rec? rhs recs)))
rhs)))) rhs))))
(hash) (hash)
nt-pats))) nt-pats)))
@ -163,17 +163,17 @@
(map (map
(λ (nt) (λ (nt)
(let ([rec-nts (hash-ref recs (nt-name nt))]) (let ([rec-nts (hash-ref recs (nt-name nt))])
(make-nt (nt-name nt) (make-nt (nt-name nt)
(sort (nt-rhs nt) (sort (nt-rhs nt)
(λ (r1 r2) (λ (r1 r2)
(and (not (cdr (assoc r1 rec-nts))) (and (not (cdr (assoc r1 rec-nts)))
(cdr (assoc r2 rec-nts)))))))) (cdr (assoc r2 rec-nts))))))))
nt-pats)) nt-pats))
;; sep-names : single-pattern lang -> (assoclist symbol pattern) ;; sep-names : single-pattern lang -> (assoclist symbol pattern)
(define (sep-names pat) (define (sep-names pat)
(let loop ([pat pat] (let loop ([pat pat]
[named-pats '()]) [named-pats '()])
(match-a-pattern (match-a-pattern
pat pat
[`any named-pats] [`any named-pats]
@ -192,13 +192,13 @@
[`(nt ,id) named-pats] [`(nt ,id) named-pats]
[`(name ,name ,pat) [`(name ,name ,pat)
(loop pat (loop pat
(add-if-new name pat named-pats))] (add-if-new name pat named-pats))]
[`(mismatch-name ,name ,pat) [`(mismatch-name ,name ,pat)
(loop pat (loop pat
(add-if-new name pat named-pats))] (add-if-new name pat named-pats))]
[`(in-hole ,p1 ,p2) [`(in-hole ,p1 ,p2)
(loop p2 (loop p2
(loop p1 named-pats))] (loop p1 named-pats))]
[`(hide-hole ,p) (loop p named-pats)] [`(hide-hole ,p) (loop p named-pats)]
[`(side-condition ,p ,g ,e) ;; error [`(side-condition ,p ,g ,e) ;; error
(unsupported/enum pat)] (unsupported/enum pat)]
@ -206,263 +206,263 @@
(unsupported/enum pat)] ;; error (unsupported/enum pat)] ;; error
[`(list ,sub-pats ...) [`(list ,sub-pats ...)
(foldl (λ (sub-pat named-pats) (foldl (λ (sub-pat named-pats)
(match sub-pat (match sub-pat
;; unnamed repeat ;; unnamed repeat
[`(repeat ,pat #f #f) [`(repeat ,pat #f #f)
(loop pat named-pats)] (loop pat named-pats)]
;; named repeat ;; named repeat
[`(repeat ,pat ,name #f) [`(repeat ,pat ,name #f)
(loop pat (loop pat
(add-if-new name 'name-r named-pats))] (add-if-new name 'name-r named-pats))]
;; mismatch named repeat ;; mismatch named repeat
[`(repeat ,pat #f ,mismatch) [`(repeat ,pat #f ,mismatch)
(loop pat (loop pat
(add-if-new mismatch 'mismatch-r named-pats))] (add-if-new mismatch 'mismatch-r named-pats))]
;; normal subpattern ;; normal subpattern
[else (loop sub-pat named-pats)])) [else (loop sub-pat named-pats)]))
named-pats named-pats
sub-pats)] sub-pats)]
[(? (compose not pair?)) [(? (compose not pair?))
named-pats]))) named-pats])))
(define (add-if-new k v l) (define (add-if-new k v l)
(cond [(assoc k l) l] (cond [(assoc k l) l]
[else (cons `(,k ,v) l)])) [else (cons `(,k ,v) l)]))
(define enum-names (define enum-names
(case-lambda (case-lambda
[(pat named-pats nts) [(pat named-pats nts)
(enum-names-with (enum-names-with
(λ (pat named) (λ (pat named)
(pat/enum-with-names pat nts named)) (pat/enum-with-names pat nts named))
pat named-pats)] pat named-pats)]
[(pat nts named-pats rec-nt-terms) [(pat nts named-pats rec-nt-terms)
(enum-names-with (enum-names-with
(λ (pat named) (λ (pat named)
(pat/enum-with-names pat nts named rec-nt-terms)) (pat/enum-with-names pat nts named rec-nt-terms))
pat named-pats)])) pat named-pats)]))
(define (enum-names-with f pat named-pats) (define (enum-names-with f pat named-pats)
(let rec ([named-pats named-pats] (let rec ([named-pats named-pats]
[env (hash)]) [env (hash)])
(cond [(null? named-pats) (f pat env)] (cond [(null? named-pats) (f pat env)]
[else [else
(match (match
(car named-pats) (car named-pats)
;; named repeat ;; named repeat
[`(,name name-r) [`(,name name-r)
(error/enum 'unimplemented "named-repeat")] (error/enum 'unimplemented "named-repeat")]
;; mismatch repeat ;; mismatch repeat
[`(,name mismatch-r) [`(,name mismatch-r)
(error/enum 'unimplemented "mismatch-repeat")] (error/enum 'unimplemented "mismatch-repeat")]
[`(,name ,pat mismatch) [`(,name ,pat mismatch)
(error/enum 'unimplemented "mismatch")] (error/enum 'unimplemented "mismatch")]
;; named ;; named
[`(,name ,pat) [`(,name ,pat)
(map/enum ;; loses bijection (map/enum ;; loses bijection
cdr cdr
(λ (x) (cons name x)) (λ (x) (cons name x))
(dep/enum (dep/enum
(f pat env) (f pat env)
(λ (term) (λ (term)
(rec (cdr named-pats) (rec (cdr named-pats)
(hash-set env (hash-set env
name name
term)))))] term)))))]
[else (error 'bad-assoc)])]))) [else (error 'bad-assoc)])])))
(define pat/enum-with-names (define pat/enum-with-names
(case-lambda (case-lambda
[(pat nt-enums named-terms) [(pat nt-enums named-terms)
(let loop ([pat pat]) (let loop ([pat pat])
(match-a-pattern (match-a-pattern
pat pat
[`any [`any
(sum/enum (sum/enum
any/enum any/enum
(listof/enum any/enum))] (listof/enum any/enum))]
[`number num/enum] [`number num/enum]
[`string string/enum] [`string string/enum]
[`natural natural/enum] [`natural natural/enum]
[`integer integer/enum] [`integer integer/enum]
[`real real/enum] [`real real/enum]
[`boolean bool/enum] [`boolean bool/enum]
[`variable var/enum] [`variable var/enum]
[`(variable-except ,s ...) [`(variable-except ,s ...)
;; todo ;; todo
(error/enum 'unimplemented "var-except")] (error/enum 'unimplemented "var-except")]
[`(variable-prefix ,s) [`(variable-prefix ,s)
;; todo ;; todo
(error/enum 'unimplemented "var-prefix")] (error/enum 'unimplemented "var-prefix")]
[`variable-not-otherwise-mentioned [`variable-not-otherwise-mentioned
(error/enum 'unimplemented "var-not-mentioned")] ;; error (error/enum 'unimplemented "var-not-mentioned")] ;; error
[`hole [`hole
(const/enum 'hole)] (const/enum 'hole)]
[`(nt ,id) [`(nt ,id)
(hash-ref nt-enums id)] (hash-ref nt-enums id)]
[`(name ,name ,pat) [`(name ,name ,pat)
(const/enum (hash-ref named-terms name))] (const/enum (hash-ref named-terms name))]
[`(mismatch-name ,name ,pat) [`(mismatch-name ,name ,pat)
(error/enum 'unimplemented "mismatch-name")] (error/enum 'unimplemented "mismatch-name")]
[`(in-hole ,p1 ,p2) ;; untested [`(in-hole ,p1 ,p2) ;; untested
(map/enum (map/enum
(λ (t1-t2) ;; loses bijection (λ (t1-t2) ;; loses bijection
(plug-hole (car t1-t2) (plug-hole (car t1-t2)
(cdr t1-t2))) (cdr t1-t2)))
(λ (plugged) (λ (plugged)
(cons 'hole plugged)) (cons 'hole plugged))
(prod/enum (prod/enum
(loop p1) (loop p1)
(loop p2)))] (loop p2)))]
[`(hide-hole ,p) [`(hide-hole ,p)
(loop p)] (loop p)]
[`(side-condition ,p ,g ,e) [`(side-condition ,p ,g ,e)
(unsupported/enum pat)] (unsupported/enum pat)]
[`(cross ,s) [`(cross ,s)
(unsupported/enum pat)] (unsupported/enum pat)]
[`(list ,sub-pats ...) [`(list ,sub-pats ...)
;; enum-list ;; enum-list
(map/enum (map/enum
flatten-1 flatten-1
identity identity
(list/enum (list/enum
(map (map
(λ (sub-pat) (λ (sub-pat)
(match sub-pat (match sub-pat
[`(repeat ,pat #f #f) [`(repeat ,pat #f #f)
(map/enum (map/enum
cdr cdr
(λ (ts) (λ (ts)
(cons (length ts) (cons (length ts)
ts)) ts))
(dep/enum (dep/enum
nats nats
(λ (n) (λ (n)
(list/enum (list/enum
(build-list n (const (loop pat)))))))] (build-list n (const (loop pat)))))))]
[`(repeat ,pat ,name #f) [`(repeat ,pat ,name #f)
(error/enum 'unimplemented "named-repeat")] (error/enum 'unimplemented "named-repeat")]
[`(repeat ,pat #f ,mismatch) [`(repeat ,pat #f ,mismatch)
(error/enum 'unimplemented "mismatch-repeat")] (error/enum 'unimplemented "mismatch-repeat")]
[else (map/enum [else (map/enum
(λ (x) (list x)) (λ (x) (list x))
car car
(loop sub-pat))])) (loop sub-pat))]))
sub-pats)))] sub-pats)))]
[(? (compose not pair?)) [(? (compose not pair?))
(const/enum pat)]))] (const/enum pat)]))]
[(pat nts named-terms rec-nt-terms) [(pat nts named-terms rec-nt-terms)
(let loop ([pat pat]) (let loop ([pat pat])
(match-a-pattern (match-a-pattern
pat pat
[`any [`any
(sum/enum (sum/enum
any/enum any/enum
(listof/enum any/enum))] (listof/enum any/enum))]
[`number num/enum] [`number num/enum]
[`string string/enum] [`string string/enum]
[`natural natural/enum] [`natural natural/enum]
[`integer integer/enum] [`integer integer/enum]
[`real real/enum] [`real real/enum]
[`boolean bool/enum] [`boolean bool/enum]
[`variable var/enum] [`variable var/enum]
[`(variable-except ,s ...) [`(variable-except ,s ...)
;; todo ;; todo
(error/enum 'unimplemented "var except")] (error/enum 'unimplemented "var except")]
[`(variable-prefix ,s) [`(variable-prefix ,s)
;; todo ;; todo
(error/enum 'unimplemented "var prefix")] (error/enum 'unimplemented "var prefix")]
[`variable-not-otherwise-mentioned [`variable-not-otherwise-mentioned
(error/enum 'unimplemented "var not otherwise mentioned")] (error/enum 'unimplemented "var not otherwise mentioned")]
[`hole [`hole
(const/enum 'hole)] (const/enum 'hole)]
[`(nt ,id) [`(nt ,id)
(let ([rhss (lookup nts id)]) (let ([rhss (lookup nts id)])
(apply sum/enum (apply sum/enum
(map (map
(λ (rhs) (λ (rhs)
(cond [(cdr (assoc rhs (hash-ref rec-nt-terms id))) (cond [(cdr (assoc rhs (hash-ref rec-nt-terms id)))
(thunk/enum (thunk/enum
+inf.f +inf.f
(λ () (λ ()
(rec-pat/enum (rhs-pattern rhs) (rec-pat/enum (rhs-pattern rhs)
nts nts
rec-nt-terms)))] rec-nt-terms)))]
[else [else
(rec-pat/enum (rhs-pattern rhs) (rec-pat/enum (rhs-pattern rhs)
nts nts
rec-nt-terms)])) rec-nt-terms)]))
rhss)))] rhss)))]
[`(name ,name ,pat) [`(name ,name ,pat)
(const/enum (hash-ref named-terms name))] (const/enum (hash-ref named-terms name))]
[`(mismatch-name ,name ,pat) [`(mismatch-name ,name ,pat)
(error/enum 'unimplemented "mismatch-name")] (error/enum 'unimplemented "mismatch-name")]
[`(in-hole ,p1 ,p2) ;; untested [`(in-hole ,p1 ,p2) ;; untested
(map/enum (map/enum
(λ (t1-t2) (λ (t1-t2)
(decomposition (car t1-t2) (decomposition (car t1-t2)
(cdr t1-t2))) (cdr t1-t2)))
(λ (decomp) (λ (decomp)
(cons (decomposition-ctx decomp) (cons (decomposition-ctx decomp)
(decomposition-term decomp))) (decomposition-term decomp)))
(prod/enum (prod/enum
(loop p1) (loop p1)
(loop p2)))] (loop p2)))]
[`(hide-hole ,p) [`(hide-hole ,p)
;; todo ;; todo
(loop p)] (loop p)]
[`(side-condition ,p ,g ,e) [`(side-condition ,p ,g ,e)
(unsupported/enum pat)] (unsupported/enum pat)]
[`(cross ,s) [`(cross ,s)
(unsupported/enum pat)] (unsupported/enum pat)]
[`(list ,sub-pats ...) [`(list ,sub-pats ...)
;; enum-list ;; enum-list
(map/enum (map/enum
flatten-1 flatten-1
identity identity
(list/enum (list/enum
(map (map
(λ (sub-pat) (λ (sub-pat)
(match sub-pat (match sub-pat
[`(repeat ,pat #f #f) [`(repeat ,pat #f #f)
(map/enum (map/enum
cdr cdr
(λ (ts) (λ (ts)
(cons (length ts) (cons (length ts)
ts)) ts))
(dep/enum (dep/enum
nats nats
(λ (n) (λ (n)
(list/enum (list/enum
(build-list n (const (loop pat)))))))] (build-list n (const (loop pat)))))))]
[`(repeat ,pat ,name #f) [`(repeat ,pat ,name #f)
(error/enum 'unimplemented "named-repeat")] (error/enum 'unimplemented "named-repeat")]
[`(repeat ,pat #f ,mismatch) [`(repeat ,pat #f ,mismatch)
(error/enum 'unimplemented "mismatch-repeat")] (error/enum 'unimplemented "mismatch-repeat")]
[else (map/enum [else (map/enum
list list
cdr cdr
(loop sub-pat))])) (loop sub-pat))]))
sub-pats)))] sub-pats)))]
[(? (compose not pair?)) [(? (compose not pair?))
(const/enum pat)]))])) (const/enum pat)]))]))
(define (flatten-1 xs) (define (flatten-1 xs)
(append-map (append-map
(λ (x) (λ (x)
(if (or (pair? x) (if (or (pair? x)
(null? x)) (null? x))
x x
(list x))) (list x)))
xs)) xs))
;; lookup : lang symbol -> (listof rhs) ;; lookup : lang symbol -> (listof rhs)
(define (lookup nts name) (define (lookup nts name)
(let rec ([nts nts]) (let rec ([nts nts])
(cond [(null? nts) (error 'unkown-nt)] (cond [(null? nts) (error 'unkown-nt)]
[(eq? name (nt-name (car nts))) [(eq? name (nt-name (car nts)))
(nt-rhs (car nts))] (nt-rhs (car nts))]
[else (rec (cdr nts))]))) [else (rec (cdr nts))])))
(define natural/enum nats) (define natural/enum nats)
@ -480,15 +480,15 @@
(define integer/enum (define integer/enum
(sum/enum nats (sum/enum nats
(map/enum (λ (n) (- (+ n 1))) (map/enum (λ (n) (- (+ n 1)))
(λ (n) (- (- n) 1)) (λ (n) (- (- n) 1))
nats))) nats)))
(define real/enum (from-list/enum '(0.0 1.5 123.112354))) (define real/enum (from-list/enum '(0.0 1.5 123.112354)))
(define num/enum (define num/enum
(sum/enum natural/enum (sum/enum natural/enum
integer/enum integer/enum
real/enum)) real/enum))
(define bool/enum (define bool/enum
(from-list/enum '(#t #f))) (from-list/enum '(#t #f)))
@ -501,15 +501,15 @@
(define any/enum (define any/enum
(sum/enum num/enum (sum/enum num/enum
string/enum string/enum
bool/enum bool/enum
var/enum)) var/enum))
(define (plug-hole ctx term) (define (plug-hole ctx term)
(let loop ([ctx ctx]) (let loop ([ctx ctx])
(match (match
ctx ctx
['hole term] ['hole term]
[`(,ts ...) [`(,ts ...)
(map loop ts)] (map loop ts)]
[x x]))) [x x])))

File diff suppressed because it is too large Load Diff