1#lang racket/base
2
3(require redex/benchmark
4         "util.rkt"
5         redex/reduction-semantics)
6(provide (all-defined-out))
7
8(define the-error "neglected to restrict case-lam to accept only 'val' arguments")
9
10(define-rewrite bug15v
11  ((verify (case-lam (name l (lam (val ellipsis1) (n ellipsis2) e)) ellipsis3) s n_l b γ η f)
12   . rest)
13  ==>
14  ((verify (case-lam (name l (lam (τ ellipsis1) (n ellipsis2) e)) ellipsis3) s n_l b γ η f)
15   . rest)
16  #:context (define-metafunction)
17  #:variables (rest ellipsis1 ellipsis2 ellipsis3)
18  #:exactly-once)
19
20(define-rewrite bug15rt
21  `(case-lam ,@(map (curry recur depth #f) ls))
22  ==>
23  `(case-lam ,@(map (curry recur depth #t) ls))
24  #:context (match)
25  #:exactly-once)
26
27(define-rewrite bug15-jdg
28  [(lam-verified?* ((lam τl nl e) el) sl m)
29   (vals τl)
30   (lam-verified? (lam τl nl e) sl m)
31   (lam-verified?* el sl m)]
32  ==>
33  [(lam-verified?* ((lam τl nl e) el) sl m)
34   (lam-verified? (lam τl nl e) sl m)
35   (lam-verified?* el sl m)]
36  #:context (define-judgment-form)
37  #:exactly-once)
38
39(include/rewrite (lib "redex/examples/racket-machine/grammar.rkt") grammar)
40
41(include/rewrite (lib "redex/examples/racket-machine/verification.rkt") verification bug15v)
42
43(include/rewrite (lib "redex/examples/racket-machine/randomized-tests.rkt") randomized-tests rt-rw bug15rt)
44
45(include/rewrite (lib "redex/benchmark/models/rvm/verif-jdg.rkt") verif-jdg bug15-jdg)
46
47(include/rewrite "generators.rkt" generators bug-mod-rw)
48
49(define small-counter-example
50  '(let-one 42
51            (boxenv 0
52                    (application (case-lam (lam (ref) () (loc-box 0)))
53                                 (loc-box 1)))))
54
55(test small-counter-example)
56