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