Added holes to redex enumerator.
This commit is contained in:
parent
843edcc78d
commit
f67b1ca06c
|
@ -12,8 +12,9 @@
|
|||
make-bind
|
||||
make-mtch
|
||||
build-flat-context
|
||||
the-hole
|
||||
)
|
||||
(only-in "../../private/lang-struct.rkt"
|
||||
the-hole)
|
||||
racket/list)
|
||||
|
||||
(define plug (λ (x y)
|
||||
|
|
|
@ -20,7 +20,6 @@
|
|||
|
||||
(struct lang-enum (enums))
|
||||
(struct decomposition (ctx term))
|
||||
(struct hole ())
|
||||
(struct named (name val))
|
||||
(struct named-t (val term))
|
||||
(struct name (name) #:transparent)
|
||||
|
@ -100,10 +99,8 @@
|
|||
(set-union (loop p1 s)
|
||||
(loop p2 s))]
|
||||
[`(hide-hole ,p) (loop p s)]
|
||||
[`(side-condition ,p ,g ,e) ;; error
|
||||
(unsupported/enum pat)]
|
||||
[`(cross ,s)
|
||||
(unsupported/enum pat)] ;; error
|
||||
[`(side-condition ,p ,g ,e) s]
|
||||
[`(cross ,s) s]
|
||||
[`(list ,sub-pats ...)
|
||||
(fold-map/set
|
||||
(λ (sub-pat)
|
||||
|
@ -297,19 +294,17 @@
|
|||
(loop p2
|
||||
(loop p1 named-pats))]
|
||||
[`(hide-hole ,p) (loop p named-pats)]
|
||||
[`(side-condition ,p ,g ,e) ;; error
|
||||
(unsupported/enum pat)]
|
||||
[`(side-condition ,p ,g ,e) ;; not supported
|
||||
named-pats]
|
||||
[`(cross ,s)
|
||||
(unsupported/enum pat)] ;; error
|
||||
named-pats] ;; not supported
|
||||
[`(list ,sub-pats ...)
|
||||
(foldl (λ (sub-pat named-pats)
|
||||
(match sub-pat
|
||||
[`(repeat ,pat #f #f)
|
||||
(loop pat named-pats)]
|
||||
[`(repeat ,pat ,name #f)
|
||||
(loop pat (cons (unimplemented "named repeat") named-pats))]
|
||||
[`(repeat ,pat #f ,mismatch)
|
||||
(loop pat (cons (unimplemented "mismatch repeat") named-pats))]
|
||||
[`(repeat ,pat ,name ,mismatch)
|
||||
(loop pat (cons (unimplemented "named/mismatched repeat") named-pats))]
|
||||
[else (loop sub-pat named-pats)]))
|
||||
named-pats
|
||||
sub-pats)]
|
||||
|
@ -387,7 +382,7 @@
|
|||
[`variable-not-otherwise-mentioned
|
||||
(error/enum 'unimplemented "var-not-mentioned")] ;; error
|
||||
[`hole
|
||||
(const/enum 'hole)]
|
||||
(const/enum the-hole)]
|
||||
[`(nt ,id)
|
||||
(hash-ref nt-enums id)]
|
||||
[`(name ,n ,pat)
|
||||
|
@ -504,6 +499,8 @@
|
|||
(define (to-term aug)
|
||||
(cond [(named? aug)
|
||||
(rep-name aug)]
|
||||
[(decomposition? aug)
|
||||
(plug-hole aug)]
|
||||
[else aug]))
|
||||
|
||||
(define (rep-name s)
|
||||
|
@ -516,19 +513,16 @@
|
|||
(cond [(and (name? term)
|
||||
(equal? (name-name term) n))
|
||||
val]
|
||||
[(cons? term)
|
||||
(map loop term)]
|
||||
[(named? term)
|
||||
(map-named loop
|
||||
term)]
|
||||
[(decomposition? term)
|
||||
(map-decomp loop
|
||||
term)]
|
||||
[else term])))))
|
||||
|
||||
(define (map-named f n)
|
||||
(let ([v (named-val n)])
|
||||
(named (named-name n)
|
||||
(named-t
|
||||
(named-t-val v)
|
||||
(f (named-t-term v))))))
|
||||
|
||||
#;
|
||||
(define (plug-hole ctx term)
|
||||
(to-term
|
||||
(let loop ([ctx ctx])
|
||||
|
@ -541,3 +535,16 @@
|
|||
[`(,ts ...)
|
||||
(map loop ts)]
|
||||
[x x]))))
|
||||
|
||||
(define (map-decomp f dcmp)
|
||||
(let ([ctx (decomposition-ctx dcmp)]
|
||||
[term (decomposition-term dcmp)])
|
||||
(decomposition (f ctx)
|
||||
(f term))))
|
||||
|
||||
(define (map-named f n)
|
||||
(let ([v (named-val n)])
|
||||
(named (named-name n)
|
||||
(named-t
|
||||
(named-t-val v)
|
||||
(f (named-t-term v))))))
|
||||
|
|
|
@ -1,7 +1,10 @@
|
|||
#lang racket/base
|
||||
|
||||
(provide (struct-out nt)
|
||||
(struct-out rhs))
|
||||
(struct-out rhs)
|
||||
the-not-hole
|
||||
the-hole
|
||||
hole?)
|
||||
|
||||
;; lang = (listof nt)
|
||||
;; nt = (make-nt sym (listof rhs))
|
||||
|
@ -9,3 +12,11 @@
|
|||
;; single-pattern = sexp
|
||||
(define-struct nt (name rhs) #:transparent)
|
||||
(define-struct rhs (pattern) #:transparent)
|
||||
(define-values (the-hole the-not-hole hole?)
|
||||
(let ()
|
||||
(define-struct hole (id)
|
||||
#:property prop:equal+hash (list (λ (x y recur) #t) (λ (v recur) 255) (λ (v recur) 65535))
|
||||
#:inspector #f)
|
||||
(define the-hole (make-hole 'the-hole))
|
||||
(define the-not-hole (make-hole 'the-not-hole))
|
||||
(values the-hole the-not-hole hole?)))
|
||||
|
|
|
@ -1933,14 +1933,6 @@ See match-a-pattern.rkt for more details
|
|||
|
||||
|#
|
||||
(define (context? x) #t)
|
||||
(define-values (the-hole the-not-hole hole?)
|
||||
(let ()
|
||||
(define-struct hole (id)
|
||||
#:property prop:equal+hash (list (λ (x y recur) #t) (λ (v recur) 255) (λ (v recur) 65535))
|
||||
#:inspector #f)
|
||||
(define the-hole (make-hole 'the-hole))
|
||||
(define the-not-hole (make-hole 'the-not-hole))
|
||||
(values the-hole the-not-hole hole?)))
|
||||
|
||||
(define (hole->not-hole exp)
|
||||
(let loop ([exp exp])
|
||||
|
@ -2043,7 +2035,6 @@ See match-a-pattern.rkt for more details
|
|||
none? none
|
||||
|
||||
make-repeat
|
||||
the-not-hole the-hole hole?
|
||||
rewrite-ellipses
|
||||
build-compatible-context-language
|
||||
caching-enabled?
|
||||
|
|
|
@ -3,6 +3,7 @@
|
|||
racket/class
|
||||
framework
|
||||
racket/pretty
|
||||
"lang-struct.rkt"
|
||||
"matcher.rkt")
|
||||
|
||||
(provide reflowing-snip<%>
|
||||
|
|
|
@ -10,6 +10,7 @@
|
|||
"matcher.rkt")
|
||||
syntax/datum
|
||||
"error.rkt"
|
||||
"lang-struct.rkt"
|
||||
"matcher.rkt")
|
||||
|
||||
(provide term term-let define-term
|
||||
|
|
|
@ -1,6 +1,7 @@
|
|||
#lang racket
|
||||
(require (only-in redex term))
|
||||
(require "../../private/matcher.rkt"
|
||||
(require "../../private/lang-struct.rkt"
|
||||
"../../private/matcher.rkt"
|
||||
(only-in "../test-util.rkt" equal/bindings?)
|
||||
mzlib/list)
|
||||
(require "../../private/compiler/match.rkt")
|
||||
|
|
|
@ -35,7 +35,7 @@
|
|||
|
||||
;; Name test
|
||||
(define-language Named
|
||||
(n (any_1 any_1)))
|
||||
(n (number_1 number_1)))
|
||||
|
||||
;; Very slow, to be fixed
|
||||
(try-it 100 Named n)
|
||||
|
@ -49,3 +49,18 @@
|
|||
|
||||
(try-it 22 not-SKI x)
|
||||
(try-it 25 not-SKI y)
|
||||
|
||||
(define-language λv
|
||||
(e (e e ...)
|
||||
(if0 e e e)
|
||||
x
|
||||
v)
|
||||
(v (λ (x ...) e)
|
||||
number
|
||||
+)
|
||||
(E (v ... E e ...)
|
||||
(if0 E e e)
|
||||
hole)
|
||||
(x (variable-except λ + if0)))
|
||||
|
||||
(try-it 100 λv E)
|
||||
|
|
|
@ -1,5 +1,6 @@
|
|||
(module term-test scheme
|
||||
(require "../private/term.rkt"
|
||||
"../private/lang-struct.rkt"
|
||||
"../private/matcher.rkt"
|
||||
"test-util.rkt")
|
||||
|
||||
|
|
|
@ -1,6 +1,7 @@
|
|||
#lang scheme
|
||||
|
||||
(require "../private/matcher.rkt"
|
||||
"../private/lang-struct.rkt"
|
||||
(for-syntax syntax/parse setup/path-to-relative)
|
||||
setup/path-to-relative
|
||||
racket/runtime-path)
|
||||
|
|
Loading…
Reference in New Issue
Block a user