Redex Enumerator support for mismatch patterns
This commit is contained in:
parent
3b2b1fb977
commit
1b1dc9cfb8
|
@ -135,9 +135,7 @@
|
|||
[`(name ,n ,pat)
|
||||
(const/e (name-ref n))]
|
||||
[`(mismatch-name ,n ,tag)
|
||||
(unsupported "mismatch patterns")
|
||||
;; (const/e (misname-ref n tag))
|
||||
]
|
||||
(const/e (misname-ref n tag))]
|
||||
[`(in-hole ,p1 ,p2)
|
||||
(map/e decomp
|
||||
(match-lambda
|
||||
|
|
|
@ -28,7 +28,6 @@
|
|||
(ann-pat (add-name subenv n subpat)
|
||||
`(name ,n ,new-subpat))]
|
||||
[`(mismatch-name ,n ,subpat)
|
||||
(unimplemented "mismatch")
|
||||
(match-define (ann-pat subenv new-subpat) (walk subpat))
|
||||
(define tag (get-and-inc!))
|
||||
(ann-pat (add-mismatch subenv n subpat tag)
|
||||
|
|
|
@ -98,15 +98,20 @@
|
|||
(try-it 25 λv x)
|
||||
|
||||
;; No longer supported
|
||||
;; (define-language M
|
||||
;; (m (x_!_1 x_!_1))
|
||||
;; (p (number_!_1 number_!_1))
|
||||
;; (n (p_!_1 p_!_1))
|
||||
;; (x number))
|
||||
(define-language M
|
||||
(m (x_!_1 x_!_1))
|
||||
(p (number_!_1 number_!_1))
|
||||
(n (p_!_1 p_!_1))
|
||||
(x number)
|
||||
|
||||
;; (try-it 100 M m)
|
||||
;; (try-it 100 M n)
|
||||
;; (try-it 100 M p)
|
||||
;; Example of poorly behaved mismatch
|
||||
(ambig (x ... x ...)))
|
||||
|
||||
(try-it 100 M m)
|
||||
(try-it 100 M n)
|
||||
(try-it 100 M p)
|
||||
;; Ambiguity kills us here
|
||||
;; (try-it 5 M (ambig_!_1 ambig_!_1))
|
||||
|
||||
;; test variable filtering
|
||||
(define-language Vars
|
||||
|
|
Loading…
Reference in New Issue
Block a user