removed named holes from Redex
svn: r11093
This commit is contained in:
Robby Findler
parent
ed6a9bad40
commit
6235970d42
|
|
@ -14,6 +14,9 @@
|
|||
|
||||
- define-metafunction and co. now use a different syntax.
|
||||
|
||||
- got rid of named holes. This means, eg, that (hole #f) now matches
|
||||
a two element list, not just the hole directly.
|
||||
|
||||
- zero occurrences of a hole when matching an `in-hole' now
|
||||
correctly fails.
|
||||
|
||||
|
|
|
|||
|
|
@ -3,9 +3,6 @@
|
|||
(only "test-util.ss" equal/bindings?)
|
||||
(lib "list.ss"))
|
||||
|
||||
(define hole (make-hole/intern none))
|
||||
(define (false-hole/name name) (make-hole/intern name #t)) ;; this used to be a #f
|
||||
|
||||
(error-print-width 500)
|
||||
|
||||
(define (make-test-mtch a b c) (make-mtch a (build-flat-context b) c))
|
||||
|
|
@ -51,34 +48,14 @@
|
|||
(test-empty '(variable-prefix x:) '() #f)
|
||||
|
||||
(test-empty 'hole 1 #f)
|
||||
(test-empty '(hole hole-name) 1 #f)
|
||||
(test-empty `hole
|
||||
hole
|
||||
(list (make-test-mtch (make-bindings (list)) hole none)))
|
||||
(test-empty `(hole #f)
|
||||
hole
|
||||
(list (make-test-mtch (make-bindings (list)) hole none)))
|
||||
(test-empty '(hole hole-name)
|
||||
hole
|
||||
#f)
|
||||
|
||||
|
||||
(test-empty '(hole a-hole-name)
|
||||
(make-hole/intern 'a-hole-name)
|
||||
(list (make-test-mtch (make-bindings (list)) (make-hole/intern 'a-hole-name) none)))
|
||||
|
||||
(test-empty '(hole #f)
|
||||
hole
|
||||
(list (make-test-mtch (make-bindings (list)) hole none)))
|
||||
|
||||
(test-empty '(in-named-hole b ((hole a) (hole b)) x)
|
||||
`(,(make-hole/intern 'a) x)
|
||||
(list (make-test-mtch (make-bindings (list)) `(,(make-hole/intern 'a) x) none)))
|
||||
the-hole
|
||||
(list (make-test-mtch (make-bindings (list)) the-hole none)))
|
||||
|
||||
(test-empty '(in-hole (name E_1 ((hide-hole hole) hole)) x)
|
||||
`(,hole x)
|
||||
(list (make-test-mtch (make-bindings (list (make-bind 'E_1 `(,hole ,hole))))
|
||||
`(x ,hole)
|
||||
`(,the-hole x)
|
||||
(list (make-test-mtch (make-bindings (list (make-bind 'E_1 `(,the-hole ,the-hole))))
|
||||
`(x ,the-hole)
|
||||
none)))
|
||||
|
||||
|
||||
|
|
@ -164,17 +141,6 @@
|
|||
equal?)
|
||||
|
||||
|
||||
(test-empty '(in-named-hole h1 (z (hole h1)) a)
|
||||
'(z a)
|
||||
(list (make-test-mtch (make-bindings (list)) '(z a) none)))
|
||||
|
||||
(test-empty '(in-named-hole h1 (z (hole h1)) a) '(z a) (list (make-test-mtch (make-bindings (list)) '(z a) none)))
|
||||
(test-empty '(in-named-hole c (any (hole c)) y)
|
||||
'(x y)
|
||||
(list (make-test-mtch (make-bindings (list (make-bind 'any 'x))) '(x y) none)))
|
||||
(test-empty '(in-named-hole a (in-named-hole b (x (hole b)) (hole a)) y)
|
||||
'(x y)
|
||||
(list (make-test-mtch (make-bindings (list)) '(x y) none)))
|
||||
(test-empty '(in-hole (in-hole (x hole) hole) y)
|
||||
'(x y)
|
||||
(list (make-test-mtch (make-bindings (list)) '(x y) none)))
|
||||
|
|
@ -346,24 +312,24 @@
|
|||
(test-xab 'exp '(+ 1 2) (list (make-test-mtch (make-bindings (list (make-bind 'exp '(+ 1 2)))) '(+ 1 2) none)))
|
||||
(test-xab '(in-hole ctxt any)
|
||||
'1
|
||||
(list (make-test-mtch (make-bindings (list (make-bind 'ctxt hole) (make-bind 'any 1))) 1 none)))
|
||||
(list (make-test-mtch (make-bindings (list (make-bind 'ctxt the-hole) (make-bind 'any 1))) 1 none)))
|
||||
(test-xab '(in-hole ctxt (name x any))
|
||||
'1
|
||||
(list (make-test-mtch (make-bindings (list (make-bind 'ctxt hole) (make-bind 'x 1) (make-bind 'any 1))) 1 none)))
|
||||
(list (make-test-mtch (make-bindings (list (make-bind 'ctxt the-hole) (make-bind 'x 1) (make-bind 'any 1))) 1 none)))
|
||||
(test-xab '(in-hole (name c ctxt) (name x any))
|
||||
'(+ 1 2)
|
||||
(list (make-test-mtch (make-bindings (list (make-bind 'ctxt (build-context hole))
|
||||
(make-bind 'c (build-context hole))
|
||||
(list (make-test-mtch (make-bindings (list (make-bind 'ctxt (build-context the-hole))
|
||||
(make-bind 'c (build-context the-hole))
|
||||
(make-bind 'x '(+ 1 2))
|
||||
(make-bind 'any '(+ 1 2))))
|
||||
'(+ 1 2) none)
|
||||
(make-test-mtch (make-bindings (list (make-bind 'ctxt (build-context `(+ ,hole 2)))
|
||||
(make-bind 'c (build-context `(+ ,hole 2)))
|
||||
(make-test-mtch (make-bindings (list (make-bind 'ctxt (build-context `(+ ,the-hole 2)))
|
||||
(make-bind 'c (build-context `(+ ,the-hole 2)))
|
||||
(make-bind 'x 1)
|
||||
(make-bind 'any 1)))
|
||||
'(+ 1 2) none)
|
||||
(make-test-mtch (make-bindings (list (make-bind 'ctxt (build-context `(+ 1 ,hole)))
|
||||
(make-bind 'c (build-context `(+ 1 ,hole)))
|
||||
(make-test-mtch (make-bindings (list (make-bind 'ctxt (build-context `(+ 1 ,the-hole)))
|
||||
(make-bind 'c (build-context `(+ 1 ,the-hole)))
|
||||
(make-bind 'x 2)
|
||||
(make-bind 'any 2)))
|
||||
'(+ 1 2) none)))
|
||||
|
|
@ -373,15 +339,15 @@
|
|||
(make-bindings (list (make-bind 'i '(+ 1 2))
|
||||
(make-bind 'number_1 1)
|
||||
(make-bind 'number_2 2)
|
||||
(make-bind 'ctxt (build-context `(+ ,hole (+ 3 4))))
|
||||
(make-bind 'c (build-context `(+ ,hole (+ 3 4))))))
|
||||
(make-bind 'ctxt (build-context `(+ ,the-hole (+ 3 4))))
|
||||
(make-bind 'c (build-context `(+ ,the-hole (+ 3 4))))))
|
||||
'(+ (+ 1 2) (+ 3 4))
|
||||
none)
|
||||
(make-test-mtch (make-bindings (list (make-bind 'i '(+ 3 4))
|
||||
(make-bind 'number_1 3)
|
||||
(make-bind 'number_2 4)
|
||||
(make-bind 'ctxt `(+ (+ 1 2) ,hole))
|
||||
(make-bind 'c `(+ (+ 1 2) ,hole))))
|
||||
(make-bind 'ctxt `(+ (+ 1 2) ,the-hole))
|
||||
(make-bind 'c `(+ (+ 1 2) ,the-hole))))
|
||||
'(+ (+ 1 2) (+ 3 4))
|
||||
none)))
|
||||
|
||||
|
|
@ -391,27 +357,27 @@
|
|||
(test-empty '(in-hole (name c (z ... hole z ...)) any)
|
||||
'(z z)
|
||||
(list
|
||||
(make-test-mtch (make-bindings (list (make-bind 'c `(z ,hole)) (make-bind 'any 'z))) '(z z) none)
|
||||
(make-test-mtch (make-bindings (list (make-bind 'c `(,hole z)) (make-bind 'any 'z))) '(z z) none)))
|
||||
(make-test-mtch (make-bindings (list (make-bind 'c `(z ,the-hole)) (make-bind 'any 'z))) '(z z) none)
|
||||
(make-test-mtch (make-bindings (list (make-bind 'c `(,the-hole z)) (make-bind 'any 'z))) '(z z) none)))
|
||||
(test-empty '(in-hole (name c (z ... hole z ...)) any)
|
||||
'(z z z)
|
||||
(list
|
||||
(make-test-mtch (make-bindings (list (make-bind 'c `(z z ,hole)) (make-bind 'any 'z))) '(z z z) none)
|
||||
(make-test-mtch (make-bindings (list (make-bind 'c `(z ,hole z)) (make-bind 'any 'z))) '(z z z) none)
|
||||
(make-test-mtch (make-bindings (list (make-bind 'c `(,hole z z)) (make-bind 'any 'z))) '(z z z) none)))
|
||||
(make-test-mtch (make-bindings (list (make-bind 'c `(z z ,the-hole)) (make-bind 'any 'z))) '(z z z) none)
|
||||
(make-test-mtch (make-bindings (list (make-bind 'c `(z ,the-hole z)) (make-bind 'any 'z))) '(z z z) none)
|
||||
(make-test-mtch (make-bindings (list (make-bind 'c `(,the-hole z z)) (make-bind 'any 'z))) '(z z z) none)))
|
||||
|
||||
(test-empty '(z (in-hole (name c (z hole)) a))
|
||||
'(z (z a))
|
||||
(list
|
||||
(make-test-mtch (make-bindings (list (make-bind 'c `(z ,hole))))
|
||||
(make-test-mtch (make-bindings (list (make-bind 'c `(z ,the-hole))))
|
||||
'(z (z a))
|
||||
none)))
|
||||
|
||||
(test-empty '(a (in-hole (name c1 (b (in-hole (name c2 (c hole)) d) hole)) e))
|
||||
'(a (b (c d) e))
|
||||
(list
|
||||
(make-test-mtch (make-bindings (list (make-bind 'c2 `(c ,hole))
|
||||
(make-bind 'c1 `(b (c d) ,hole))))
|
||||
(make-test-mtch (make-bindings (list (make-bind 'c2 `(c ,the-hole))
|
||||
(make-bind 'c1 `(b (c d) ,the-hole))))
|
||||
'(a (b (c d) e))
|
||||
none)))
|
||||
|
||||
|
|
@ -422,8 +388,8 @@
|
|||
(test-empty '(a (b (in-hole (name c1 (in-hole (name c2 (c hole)) (d hole))) e)))
|
||||
'(a (b (c (d e))))
|
||||
(list
|
||||
(make-test-mtch (make-bindings (list (make-bind 'c1 `(c (d ,hole)))
|
||||
(make-bind 'c2 `(c ,hole))))
|
||||
(make-test-mtch (make-bindings (list (make-bind 'c1 `(c (d ,the-hole)))
|
||||
(make-bind 'c2 `(c ,the-hole))))
|
||||
'(a (b (c (d e))))
|
||||
none)))
|
||||
|
||||
|
|
@ -515,33 +481,6 @@
|
|||
(list (make-test-mtch (make-bindings '()) '(x 1 x) none)))
|
||||
|
||||
|
||||
#;
|
||||
(test-xab '(in-hole ec-multi (+ number number))
|
||||
'(+ 1 2)
|
||||
(list (make-bindings (list (make-bind 'hole (make-hole-binding '(+ 1 2) '() #f))))))
|
||||
|
||||
#;
|
||||
(test-xab '(in-hole ec-multi (+ number number))
|
||||
'(+ 1 (+ 5 6))
|
||||
(list (make-bindings (list (make-bind 'hole (make-hole-binding '(+ 5 6) '(cdr cdr car) #f))))))
|
||||
|
||||
#;
|
||||
(test-xab '(in-hole ec-multi (+ number number))
|
||||
'(+ (+ (+ 1 2) 3) 4)
|
||||
(list (make-bindings (list (make-bind 'hole (make-hole-binding '(+ 1 2) '(cdr car cdr car) #f))))))
|
||||
|
||||
#;
|
||||
(test-xab '(in-hole ec-multi (+ number number))
|
||||
'(+ (+ 3 (+ 1 2)) 4)
|
||||
(list (make-bindings (list (make-bind 'hole (make-hole-binding '(+ 1 2) '(cdr car cdr cdr car) #f))))))
|
||||
|
||||
#;
|
||||
(test-xab '(in-hole ec-multi (+ number number))
|
||||
'(+ (+ (+ 1 2) (+ 3 4)) (+ 5 6))
|
||||
(list (make-bindings (list (make-bind 'hole (make-hole-binding '(+ 5 6) '(cdr cdr car) #f))))
|
||||
(make-bindings (list (make-bind 'hole (make-hole-binding '(+ 1 2) '(cdr car cdr car) #f))))
|
||||
(make-bindings (list (make-bind 'hole (make-hole-binding '(+ 3 4) '(cdr car cdr cdr car) #f))))))
|
||||
|
||||
(test-xab '(in-hole (cross simple) g)
|
||||
'g
|
||||
(list (make-mtch (make-bindings (list)) 'g none)))
|
||||
|
|
@ -682,9 +621,6 @@
|
|||
(make-rhs '(+ exp ctxt) '())
|
||||
(make-rhs 'hole '())))
|
||||
|
||||
(make-nt 'ec-multi
|
||||
(list (make-rhs 'hole '())
|
||||
(make-rhs '(in-named-hole xx ec-one ec-multi) '())))
|
||||
(make-nt 'ec-one
|
||||
(list (make-rhs '(+ (hole xx) exp) '())
|
||||
(make-rhs '(+ exp (hole xx)) '())))
|
||||
|
|
@ -788,7 +724,7 @@
|
|||
(define (build-context c)
|
||||
(let loop ([c c])
|
||||
(cond
|
||||
[(eq? c hole) hole]
|
||||
[(eq? c the-hole) the-hole]
|
||||
[(pair? c) (build-cons-context (loop (car c)) (loop (cdr c)))]
|
||||
[(or (null? c)
|
||||
(number? c)
|
||||
|
|
|
|||
|
|
@ -86,10 +86,9 @@ before the pattern compiler is invoked.
|
|||
;; pict-builder
|
||||
;; (listof symbol)
|
||||
;; (listof (listof symbol))) -- keeps track of `primary' non-terminals
|
||||
;; hole-info = (union #f none symbol)
|
||||
;; hole-info = (union #f none)
|
||||
;; #f means we're not in a `in-hole' context
|
||||
;; none means we're looking for a normal hole
|
||||
;; symbol means we're looking for a named hole named by the symbol
|
||||
;; none means we're looking for a hole
|
||||
|
||||
(define-struct compiled-lang (lang ht list-ht across-ht across-list-ht has-hole-ht
|
||||
cache bind-names-cache pict-builder literals
|
||||
|
|
@ -208,9 +207,6 @@ before the pattern compiler is invoked.
|
|||
(loop p1)
|
||||
(loop p2)]
|
||||
[`(hide-hole ,p) (loop p)]
|
||||
[`(in-named-hole ,s ,p1 ,p2)
|
||||
(loop p1)
|
||||
(loop p2)]
|
||||
[`(side-condition ,p ,g)
|
||||
(loop p)]
|
||||
[`(cross ,s) (void)]
|
||||
|
|
@ -235,7 +231,6 @@ before the pattern compiler is invoked.
|
|||
[`(variable-prefix ,var) #f]
|
||||
[`variable-not-otherwise-mentioned #f]
|
||||
[`hole #t]
|
||||
[`(hole ,(? symbol? hole-name)) #t]
|
||||
[(? string?) #f]
|
||||
[(? symbol?)
|
||||
;; cannot be a non-terminal, otherwise this function isn't called
|
||||
|
|
@ -245,8 +240,6 @@ before the pattern compiler is invoked.
|
|||
[`(in-hole ,context ,contractum)
|
||||
(recur contractum)]
|
||||
[`(hide-hole ,arg) #f]
|
||||
[`(in-named-hole ,hole-name ,context ,contractum)
|
||||
(recur contractum)]
|
||||
[`(side-condition ,pat ,condition)
|
||||
(recur pat)]
|
||||
[(? list?)
|
||||
|
|
@ -354,7 +347,6 @@ before the pattern compiler is invoked.
|
|||
[`(variable-prefix ,var) (lambda (l) pattern)]
|
||||
[`variable-not-otherwise-mentioned (λ (l) pattern)]
|
||||
[`hole (lambda (l) 'hole)]
|
||||
[`(hole ,(? symbol? hole-name)) (lambda (l) `(hole ,hole-name))]
|
||||
[(? string?) (lambda (l) pattern)]
|
||||
[(? symbol?)
|
||||
(cond
|
||||
|
|
@ -382,13 +374,6 @@ before the pattern compiler is invoked.
|
|||
(let ([m (loop p)])
|
||||
(lambda (l)
|
||||
`(hide-hole ,(m l))))]
|
||||
[`(in-named-hole ,hole-name ,context ,contractum)
|
||||
(let ([match-context (loop context)]
|
||||
[match-contractum (loop contractum)])
|
||||
(lambda (l)
|
||||
`(in-named-hole ,hole-name
|
||||
,(match-context l)
|
||||
,(match-contractum l))))]
|
||||
[`(side-condition ,pat ,condition)
|
||||
(let ([patf (loop pat)])
|
||||
(lambda (l)
|
||||
|
|
@ -468,7 +453,6 @@ before the pattern compiler is invoked.
|
|||
[`variable-not-otherwise-mentioned #f]
|
||||
[`(variable-prefix ,var) #f]
|
||||
[`hole #t]
|
||||
[`(hole ,(? symbol? hole-name)) #t]
|
||||
[(? string?) #f]
|
||||
[(? symbol?)
|
||||
(handle-symbol pattern)]
|
||||
|
|
@ -478,8 +462,6 @@ before the pattern compiler is invoked.
|
|||
(recur context)]
|
||||
[`(hide-hole ,p)
|
||||
(recur p)]
|
||||
[`(in-named-hole ,hole-name ,context ,contractum)
|
||||
(recur context)]
|
||||
[`(side-condition ,pat ,condition)
|
||||
(recur pat)]
|
||||
[(? list?)
|
||||
|
|
@ -518,7 +500,6 @@ before the pattern compiler is invoked.
|
|||
[`variable-not-otherwise-mentioned #t]
|
||||
[`(variable-prefix ,prefix) #t]
|
||||
[`hole #t]
|
||||
[`(hole ,(? symbol? hole-name)) #t]
|
||||
[(? string?) #t]
|
||||
[(? symbol?) (handle-sym pattern)]
|
||||
[`(name ,name ,pat)
|
||||
|
|
@ -527,8 +508,6 @@ before the pattern compiler is invoked.
|
|||
(recur context)]
|
||||
[`(hide-hole ,p)
|
||||
(recur p)]
|
||||
[`(in-named-hole ,hole-name ,context ,contractum)
|
||||
(recur context)]
|
||||
[`(side-condition ,pat ,condition)
|
||||
(recur pat)]
|
||||
[(? list?)
|
||||
|
|
@ -742,12 +721,6 @@ before the pattern compiler is invoked.
|
|||
(map (λ (match) (make-mtch (mtch-bindings match) (mtch-context match) none))
|
||||
matches))))
|
||||
#f))]
|
||||
[`(in-named-hole ,hole-id ,context ,contractum)
|
||||
(let-values ([(match-context ctxt-has-hole?) (compile-pattern/default-cache context)]
|
||||
[(match-contractum contractum-has-hole?) (compile-pattern/default-cache contractum)])
|
||||
(values
|
||||
(match-in-hole context contractum exp match-context match-contractum hole-id)
|
||||
(or ctxt-has-hole? contractum-has-hole?)))]
|
||||
|
||||
[`(side-condition ,pat ,condition)
|
||||
(let-values ([(match-pat has-hole?) (compile-pattern/default-cache pat)])
|
||||
|
|
@ -1124,15 +1097,14 @@ before the pattern compiler is invoked.
|
|||
(let ([mis-matched-hole
|
||||
(λ (exp)
|
||||
(and (hole? exp)
|
||||
(equal? (hole-name exp) hole-id)
|
||||
(list (make-mtch (make-bindings '())
|
||||
(make-hole/intern (hole-name exp))
|
||||
the-hole
|
||||
none))))])
|
||||
(lambda (exp hole-info)
|
||||
(if hole-info
|
||||
(if (eq? hole-id hole-info)
|
||||
(list (make-mtch (make-bindings '())
|
||||
(make-hole/intern hole-info)
|
||||
the-hole
|
||||
exp))
|
||||
(mis-matched-hole exp))
|
||||
(mis-matched-hole exp)))))
|
||||
|
|
@ -1467,7 +1439,6 @@ before the pattern compiler is invoked.
|
|||
(loop pat (cons (make-bind name '()) ribs)))]
|
||||
[`(in-hole ,context ,contractum) (loop context (loop contractum ribs))]
|
||||
[`(hide-hole ,p) (loop p ribs)]
|
||||
[`(in-named-hole ,hole-name ,context ,contractum) (loop context (loop contractum ribs))]
|
||||
[`(side-condition ,pat ,test) (loop pat ribs)]
|
||||
[(? list?)
|
||||
(let-values ([(rewritten has-hole?) (rewrite-ellipses non-underscore-binder? pattern (lambda (x) (values x #f)))])
|
||||
|
|
@ -1540,28 +1511,11 @@ before the pattern compiler is invoked.
|
|||
|
||||
|#
|
||||
(define (context? x) #t)
|
||||
(define-values (make-hole/intern hole-name hole?)
|
||||
(define-values (the-hole hole?)
|
||||
(let ()
|
||||
(define-struct hole () #f)
|
||||
(define-struct (named-hole hole) (name) #f)
|
||||
(define (hole-name h)
|
||||
(cond
|
||||
[(named-hole? h)
|
||||
(named-hole-name h)]
|
||||
[(hole? h)
|
||||
none]
|
||||
[else (error 'hole-name "expected a hole, given ~e" h)]))
|
||||
(define (make-hole/intern a)
|
||||
(or (hash-table-get hole-cache a #f)
|
||||
(let ([h (make-named-hole a)])
|
||||
(hash-table-put! hole-cache a h)
|
||||
h)))
|
||||
(define the-hole?
|
||||
(let ([hole? (λ (x) (or (hole? x) (named-hole? x)))])
|
||||
hole?))
|
||||
(define hole-cache (make-hash-table 'equal))
|
||||
(hash-table-put! hole-cache none (make-hole)) ;; see the cache to avoid a case in make-hole/intern
|
||||
(values make-hole/intern hole-name the-hole?)))
|
||||
(define the-hole (make-hole))
|
||||
(values the-hole hole?)))
|
||||
|
||||
(define (build-flat-context exp) exp)
|
||||
(define (build-cons-context e1 e2) (cons e1 e2))
|
||||
|
|
@ -1583,8 +1537,7 @@ before the pattern compiler is invoked.
|
|||
(cdr exp)
|
||||
(loop (cdr exp))))]
|
||||
|
||||
[(and (hole? exp)
|
||||
(equal? (hole-name exp) hole-info))
|
||||
[(hole? exp)
|
||||
(set! done? #t)
|
||||
hole-stuff]
|
||||
[else exp])))]))
|
||||
|
|
@ -1642,6 +1595,6 @@ before the pattern compiler is invoked.
|
|||
none? none
|
||||
|
||||
make-repeat
|
||||
make-hole/intern hole? hole-name
|
||||
the-hole hole?
|
||||
rewrite-ellipses
|
||||
build-compatible-context-language))
|
||||
|
|
|
|||
|
|
@ -410,7 +410,6 @@
|
|||
#:nt (patterns '(+ a A) '(+ a a) 'number 'number '(+ A a) 'hole '(+ a a) 'number 'number)
|
||||
#:num (build-list 5 (λ (x) (λ (_) x)))))
|
||||
'(+ (+ 0 1) (+ 2 (+ 3 4))))
|
||||
(test (generate lang (in-named-hole h B 3) 5 0) '(6 3))
|
||||
(test (generate lang (in-hole (in-hole ((in-hole hole 4) hole) 3) 5) 5 0) '(4 3))
|
||||
(test (generate lang hole 5 0) (term hole))
|
||||
(test (generate lang (hole h) 5 0) (term (hole h)))
|
||||
|
|
@ -456,7 +455,7 @@
|
|||
(let ()
|
||||
(define-language lang
|
||||
(e (hide-hole (in-hole ((hide-hole hole) hole) 1))))
|
||||
(test (generate lang e 5 0) (term ((hole #f) 1))))
|
||||
(test (generate lang e 5 0) (term (hole 1))))
|
||||
|
||||
(define (output-error-port thunk)
|
||||
(let ([port (open-output-string)])
|
||||
|
|
|
|||
|
|
@ -181,7 +181,7 @@ To do a better job of not generating programs with free variables,
|
|||
(let* ([not-in-hole (gensym)]
|
||||
[generate-contractum (hash-ref holes name not-in-hole)])
|
||||
(if (eq? generate-contractum not-in-hole)
|
||||
(if name (make-hole/intern name) (term hole))
|
||||
the-hole
|
||||
(generate-contractum))))
|
||||
(match pat
|
||||
[`number ((next-number-decision) random-numbers)]
|
||||
|
|
@ -207,9 +207,6 @@ To do a better job of not generating programs with free variables,
|
|||
[`hole (generate-hole #f)]
|
||||
[`(in-hole ,context ,contractum)
|
||||
(loop context (hash-set holes #f (λ () (loop contractum holes))))]
|
||||
[`(hole ,(? symbol? name)) (generate-hole name)]
|
||||
[`(in-named-hole ,name ,context ,contractum)
|
||||
(loop context (hash-set holes name (λ () (loop contractum holes))))]
|
||||
[`(hide-hole ,pattern) (loop pattern (make-immutable-hasheq null))]
|
||||
[`any
|
||||
(let-values ([(lang nt) ((next-any-decision) lang)])
|
||||
|
|
|
|||
|
|
@ -9,22 +9,14 @@
|
|||
(test (term (1 ,(+ 1 1))) (list 1 2))
|
||||
(test (term-let ([x 1]) (term (x x))) (list 1 1))
|
||||
(test (term-let ([(x ...) (list 1 2 3)]) (term ((y x) ...))) '((y 1) (y 2) (y 3)))
|
||||
(test (term hole) (make-hole/intern none))
|
||||
(test (term (hole #f)) (make-hole/intern none))
|
||||
(test (term (hole hole-id)) (make-hole/intern 'hole-id))
|
||||
|
||||
(test (term (in-hole (1 hole) 2)) (term (1 2)))
|
||||
(test (term (in-hole (1 (hole #f)) 2)) (term (1 2)))
|
||||
(test (term (in-named-hole x (1 (hole x)) 2)) (term (1 2)))
|
||||
(test (term (in-named-hole x (1 hole (hole x)) 2)) (term (1 hole 2)))
|
||||
(test (term (in-hole (1 hole (hole x)) 2)) (term (1 2 (hole x))))
|
||||
|
||||
(test (equal? (term hole) (term hole)) #t)
|
||||
(test (equal? (term (hole x)) (term (hole x))) #t)
|
||||
(test (equal? (term (hole x)) (term (hole y))) #f)
|
||||
(test (hole? (term hole)) #t)
|
||||
(test (hole? (term (hole #f))) #t)
|
||||
(test (hole? (term (hole the-name))) #t)
|
||||
(test (hole? (term (hole #f))) #f)
|
||||
(test (hole? (term (hole the-name))) #f)
|
||||
|
||||
(test (term-let-fn ((f (lambda (q) q)))
|
||||
(term (f 1 2 3)))
|
||||
|
|
|
|||
|
|
@ -72,13 +72,7 @@
|
|||
(syntax (unsyntax (plug (term id) (term body))))]
|
||||
[(in-hole . x)
|
||||
(raise-syntax-error 'term "malformed in-hole" orig-stx stx)]
|
||||
[(in-named-hole name id body)
|
||||
(syntax (unsyntax (plug (term id) (term body) (or (term name) none))))]
|
||||
[(in-named-hole . x)
|
||||
(raise-syntax-error 'term "malformed in-named-hole" orig-stx stx)]
|
||||
[hole (syntax (unsyntax (make-hole/intern none)))]
|
||||
[(hole #f) (syntax (unsyntax (make-hole/intern none)))]
|
||||
[(hole stuff) (syntax (unsyntax (make-hole/intern 'stuff)))]
|
||||
[hole (syntax (unsyntax the-hole))]
|
||||
[(x ...)
|
||||
(with-syntax ([(x-rewrite ...)
|
||||
(let i-loop ([xs (syntax->list (syntax (x ...)))])
|
||||
|
|
|
|||
|
|
@ -101,7 +101,7 @@
|
|||
(bind-exp snd))))]
|
||||
[(and (hole? fst)
|
||||
(hole? snd))
|
||||
(equal? (hole-name fst) (hole-name snd))]
|
||||
#t]
|
||||
[else (equal? fst snd)])))
|
||||
|
||||
;; rib-lt : rib rib -> boolean
|
||||
|
|
|
|||
|
|
@ -172,7 +172,7 @@ all non-GUI portions of Redex) and also exported by
|
|||
This section covers Redex's @deftech{pattern} language, used
|
||||
in various ways:
|
||||
|
||||
@(schemegrammar* #:literals (any number string variable variable-except variable-prefix variable-not-otherwise-mentioned hole name in-hole in-named-hole side-condition cross)
|
||||
@(schemegrammar* #:literals (any number string variable variable-except variable-prefix variable-not-otherwise-mentioned hole name in-hole side-condition cross)
|
||||
[pattern any
|
||||
number
|
||||
string
|
||||
|
|
@ -181,11 +181,9 @@ in various ways:
|
|||
(variable-prefix symbol)
|
||||
variable-not-otherwise-mentioned
|
||||
hole
|
||||
(hole symbol-or-false)
|
||||
symbol
|
||||
(name symbol pattern)
|
||||
(in-hole pattern pattern)
|
||||
(in-named-hole symbol pattern pattern)
|
||||
(hide-hole pattern)
|
||||
(side-condition pattern guard)
|
||||
(cross symbol)
|
||||
|
|
@ -333,7 +331,7 @@ Multiple ellipses are allowed. For example, this @|pattern|:
|
|||
|
||||
matches this sexpression:
|
||||
|
||||
@schemeblock[(term (a a))]
|
||||
@schemeblock[(#, @|tttterm| (a a))]
|
||||
|
||||
three different ways. One where the first @tt{a} in the @pattern
|
||||
matches nothing, and the second matches both of the
|
||||
|
|
@ -353,7 +351,7 @@ As an example, this @|pattern|:
|
|||
|
||||
only matches this sexpression:
|
||||
|
||||
@schemeblock[(term (a a))]
|
||||
@schemeblock[(#, @|tttterm| (a a))]
|
||||
|
||||
one way, with each named @pattern matching a single a. Unlike
|
||||
the above, the two @|pattern|s with mismatched lengths is ruled
|
||||
|
|
@ -369,7 +367,7 @@ Thus, with the @|pattern|:
|
|||
|
||||
and the expression
|
||||
|
||||
@schemeblock[(term (a a))]
|
||||
@schemeblock[(#, @|tttterm| (a a))]
|
||||
|
||||
two matches occur, one where @tt{x} is bound to @scheme['()] and
|
||||
@tt{y} is bound to @scheme['(a a)] and one where @tt{x} is bound to
|
||||
|
|
@ -453,6 +451,7 @@ stands for repetition unless otherwise indicated):
|
|||
string]
|
||||
[term-sequence
|
||||
term
|
||||
,@scheme-expression
|
||||
(code:line ... (code:comment "literal ellipsis"))])
|
||||
|
||||
@itemize{
|
||||
|
|
@ -465,7 +464,13 @@ corresponding symbol, unless the identifier is bound by
|
|||
@item{A term written @tt{(term-sequence ...)} constructs a list of
|
||||
the terms constructed by the sequence elements.}
|
||||
|
||||
@item{A term written @scheme[,scheme-expression] evaluates the @scheme[scheme-expression] and substitutes its value into the term at that point.}
|
||||
@item{A term written @scheme[,scheme-expression] evaluates the
|
||||
@scheme[scheme-expression] and substitutes its value into the term at
|
||||
that point.}
|
||||
|
||||
@item{A term written @scheme[,@scheme-expression] evaluates the
|
||||
@scheme[scheme-expression], which must produce a list. It then splices
|
||||
the contents of the list into the expression at that point in the sequence.}
|
||||
|
||||
@item{A term written @tt{(in-hole @|tttterm| @|tttterm|)}
|
||||
is the dual to the @pattern `in-hole' -- it accepts
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user