redex: add typed generators to the benchmark
- change delim-cont to generate a store as well - add version of rvm that works with #:satisfying - add version of list-machine that works with #:satisfying - new rewrites for the above - infrastructure to wire all of this together
This commit is contained in:
Burke Fetscher
parent
f271d3b167
commit
2ba4e97fa1
|
|
@ -38,7 +38,8 @@
|
|||
(Mark t) (List t))
|
||||
(B Num Bool Unit)
|
||||
|
||||
(x variable-not-otherwise-mentioned)
|
||||
;(x variable-not-otherwise-mentioned)
|
||||
(x (variable-prefix var:))
|
||||
|
||||
(b n s bool unit)
|
||||
(n number)
|
||||
|
|
@ -188,8 +189,11 @@
|
|||
(--> (monitor (-> ctc_a ctc_r) (name v (λ (x : t) e)) k l j)
|
||||
(λ (x_1 : t)
|
||||
((λ (x_2 : t) (monitor ctc_r (v x_2) k l j))
|
||||
(monitor ctc_a x_1 l k j))))
|
||||
|
||||
(monitor ctc_a x_1 l k j)))
|
||||
;;added this (10/7/14):
|
||||
(where/hidden (x_1 x_2)
|
||||
,(variables-not-in (term (ctc_a ctc_r v))
|
||||
'(var: var:))))
|
||||
;; prompt-tag/c
|
||||
(--> (monitor (prompt-tag/c ctc_1 ctc_2 t_1 t_2) v_p k l j)
|
||||
(PG ctc_1 ctc_2 v_p k l j))
|
||||
|
|
@ -822,15 +826,17 @@
|
|||
|
||||
|
||||
|
||||
|
||||
(define (random-exp depth)
|
||||
(match
|
||||
(generate-term
|
||||
abort+Γ-lang
|
||||
#:satisfying
|
||||
(tc · · e t)
|
||||
(tc · Σ e t)
|
||||
depth)
|
||||
[#f #f]
|
||||
[`(tc · · ,e ,t) e]))
|
||||
[`(tc · ,Σ ,e ,t)
|
||||
(list Σ e)]))
|
||||
|
||||
(define (eval-random-exps n [depth 4])
|
||||
(for ([_ n])
|
||||
|
|
@ -877,19 +883,19 @@
|
|||
(or (redex-match abort-lang (in-hole E (seq (update mk e_1) e_2)) exp)
|
||||
(redex-match abort-lang (in-hole E (check e v l_1 l_2)) exp)))
|
||||
|
||||
(define (soundness-holds? e)
|
||||
(define t (judgment-holds (tc · · ,e t) t))
|
||||
(define (soundness-holds? e [inp-Σ '·])
|
||||
(define t (judgment-holds (tc · ,inp-Σ ,e t) t))
|
||||
(define exceeded-max-steps #f)
|
||||
(define steps 0)
|
||||
(or (not t)
|
||||
(match (apply-reduction-relation*
|
||||
abort-red `(<> ,e ·)
|
||||
abort-red `(<> ,e ,inp-Σ)
|
||||
#:stop-when
|
||||
(λ (_)
|
||||
(set! steps (add1 steps))
|
||||
;; treat 20 steps as non-terminating
|
||||
;; treat 40 steps as non-terminating
|
||||
;; larger examples tend to be useless...
|
||||
(and (steps . > . 20)
|
||||
(and (steps . > . 40)
|
||||
(set! exceeded-max-steps #t))))
|
||||
['() #t] ;; looping reduction graph
|
||||
[`((<> ,e* ,st*))
|
||||
|
|
@ -901,16 +907,22 @@
|
|||
(equal? (judgment-holds (tc · ,st* ,e* t) t)
|
||||
t))))]
|
||||
[_
|
||||
(error 'soundness "multiple reductions found for ~s" e)])))
|
||||
(if exceeded-max-steps
|
||||
#t
|
||||
(error 'soundness "multiple reductions found for ~s" e))])))
|
||||
|
||||
(define (check-random-exps n [depth 4])
|
||||
(for ([_ n])
|
||||
(define (check-random-exps n [depth 4] #:verbose [verbose? #f])
|
||||
(for/and ([_ n])
|
||||
(define e (random-exp depth))
|
||||
(when e
|
||||
(pretty-write e)
|
||||
(unless (soundness-holds? e)
|
||||
(error 'check "soundness failed for: ~s" e)))))
|
||||
(or (not e)
|
||||
(match-let* ([(list s e) e]
|
||||
[ok? (soundness-holds? e s)])
|
||||
(when verbose?
|
||||
(pretty-write e))
|
||||
(unless ok?
|
||||
(error 'check "soundness failed for: ~s\n~s" s e))
|
||||
ok?))))
|
||||
|
||||
(define (type-check e)
|
||||
(judgment-holds (tc · · ,e t)))
|
||||
(define (type-check e Σ)
|
||||
(judgment-holds (tc · ,Σ ,e t)))
|
||||
|
||||
|
|
|
|||
|
|
@ -3,7 +3,8 @@
|
|||
(require (except-in redex/benchmark/models/delim-cont/delim-cont let)
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
redex/reduction-semantics
|
||||
racket/bool)
|
||||
racket/bool
|
||||
racket/match)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
|
@ -12,14 +13,14 @@
|
|||
(define (get-generator) generate)
|
||||
(define type 'grammar)
|
||||
(define (generate)
|
||||
(generate-term abort-lang e 4)))
|
||||
(generate-term abort+Γ-lang (<> e Σ) 4)))
|
||||
|
||||
(module+ enum-mod
|
||||
(provide generate get-generator type)
|
||||
(define (get-generator) generate)
|
||||
(define type 'enum)
|
||||
(define (generate [p-value 0.125])
|
||||
(generate-term abort-lang e #:i-th (pick-an-index p-value))))
|
||||
(generate-term abort+Γ-lang (<> e Σ) #:i-th (pick-an-index p-value))))
|
||||
|
||||
(module+ ordered-mod
|
||||
(provide generate get-generator type)
|
||||
|
|
@ -30,12 +31,27 @@
|
|||
(set! index (add1 index))))))
|
||||
(define type 'ordered)
|
||||
(define (generate [index 0])
|
||||
(generate-term abort-lang e #:i-th index)))
|
||||
(generate-term abort+Γ-lang (<> e Σ) #:i-th index)))
|
||||
|
||||
(module+ typed-mod
|
||||
(provide generate get-generator type)
|
||||
(define (get-generator) generate)
|
||||
(define type 'search)
|
||||
(define (generate)
|
||||
(match (generate-term
|
||||
abort+Γ-lang
|
||||
#:satisfying
|
||||
(tc · Σ e t)
|
||||
4)
|
||||
[`(tc ,_ ,Σ ,e ,_) `(<> ,e ,Σ)]
|
||||
[#f #f])))
|
||||
|
||||
(module+ check-mod
|
||||
(provide check)
|
||||
(define (check term)
|
||||
(or (not term)
|
||||
(implies (type-check term)
|
||||
(soundness-holds? term)))))
|
||||
(or (not term)
|
||||
(match term
|
||||
[`(<> ,e ,Σ)
|
||||
(implies (type-check e Σ)
|
||||
(soundness-holds? e Σ))]))))
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,14 @@
|
|||
#lang racket/base
|
||||
|
||||
(require racket/runtime-path
|
||||
"../util/info-util.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
(define name "delim-cont")
|
||||
(define fname (make-path-root 'delim-cont))
|
||||
|
||||
(define-runtime-path here ".")
|
||||
|
||||
(define (all-mods)
|
||||
(all-mods/type 'typed here name fname))
|
||||
|
|
@ -2,6 +2,7 @@
|
|||
|
||||
(require redex/examples/list-machine/list-machine
|
||||
redex/examples/list-machine/list-machine-typing
|
||||
(prefix-in typed: redex/benchmark/models/list-machine/ls-typed-gen)
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
redex/reduction-semantics
|
||||
racket/bool
|
||||
|
|
@ -15,14 +16,14 @@
|
|||
(define (get-generator) generate)
|
||||
(define type 'grammar)
|
||||
(define (generate)
|
||||
(generate-term list-machine-typing (l0 : ι p) 7)))
|
||||
(generate-term list-machine-typing ((l0 : ι p) Π) 7)))
|
||||
|
||||
(module+ enum-mod
|
||||
(provide generate get-generator type)
|
||||
(define (get-generator) generate)
|
||||
(define type 'enum)
|
||||
(define (generate [p-value 0.5])
|
||||
(generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index p-value))))
|
||||
(generate-term list-machine-typing ((l0 : ι p) Π) #:i-th (pick-an-index p-value))))
|
||||
|
||||
(module+ ordered-mod
|
||||
(provide generate get-generator type)
|
||||
|
|
@ -33,10 +34,23 @@
|
|||
(set! index (add1 index))))))
|
||||
(define type 'ordered)
|
||||
(define (generate [index 0])
|
||||
(generate-term list-machine-typing (l0 : ι p) #:i-th index)))
|
||||
(generate-term list-machine-typing ((l0 : ι p) Π) #:i-th index)))
|
||||
|
||||
(module+ typed-mod
|
||||
(provide generate get-generator type)
|
||||
(define (get-generator) generate)
|
||||
(define type 'search)
|
||||
(define (generate)
|
||||
(match (generate-term typed:list-machine-typing
|
||||
#:satisfying
|
||||
(typed:check-program (l0 : ι p) Π)
|
||||
7)
|
||||
[`(typed:check-program ,p ,Π)
|
||||
`(,p ,Π)]
|
||||
[#f #f])))
|
||||
|
||||
(module+ check-mod
|
||||
(provide check)
|
||||
(provide check type-check check-progress)
|
||||
|
||||
(define (check-progress p)
|
||||
(define r_0 (term (empty v0 ↦ nil)))
|
||||
|
|
@ -64,23 +78,13 @@
|
|||
(match (car closure)
|
||||
[`(,p ,r ,ι)
|
||||
(equal? ι 'halt)])))))))
|
||||
|
||||
;; TODO : change this to generate the program and type as a pair, (as the typed
|
||||
;; generator does), so we are testing the different strategies fairly?
|
||||
(define (type-check p)
|
||||
;; need to provide a program typing, so generate 10 randomly and
|
||||
;; see if any succeed...
|
||||
;; (succeeds more often than one might assume)
|
||||
(let loop ([i 0])
|
||||
(cond
|
||||
[(i . > . 10) #f]
|
||||
[else
|
||||
(define guess-Π (generate-term list-machine-typing (l0 : (v0 : nil empty) Π) 7))
|
||||
(or (and (judgment-holds (check-program ,p ,guess-Π))
|
||||
guess-Π)
|
||||
(loop (add1 i)))])))
|
||||
|
||||
(define (check p)
|
||||
(or (not p)
|
||||
(implies (type-check p) (check-progress p)))))
|
||||
|
||||
(define (type-check p Π)
|
||||
(judgment-holds (check-program ,p ,Π)))
|
||||
|
||||
(define (check pΠ)
|
||||
(or (not pΠ)
|
||||
(match pΠ
|
||||
[`(,p ,Π)
|
||||
(implies (type-check p Π) (check-progress p))]))))
|
||||
|
||||
|
|
|
|||
|
|
@ -22,6 +22,19 @@
|
|||
#:variables (rest)
|
||||
#:exactly-once)
|
||||
|
||||
(define-rewrite bug1-typed
|
||||
((:lookup-Γ Γ v_0 τ_0)
|
||||
(:lookup-Γ Γ v_1 τ_1)
|
||||
. rest)
|
||||
==>
|
||||
((:lookup-Γ Γ v_0 τ_0)
|
||||
(:lookup-Γ Γ v_0 τ_1)
|
||||
. rest)
|
||||
#:context (define-judgment-form)
|
||||
#:variables (rest)
|
||||
#:exactly-once)
|
||||
|
||||
|
||||
(define-rewrite return-stopped-rw
|
||||
(let ([closure (apply-reduction-relation*
|
||||
red
|
||||
|
|
@ -62,9 +75,18 @@
|
|||
|
||||
(include/rewrite (lib "redex/examples/list-machine/list-machine-typing.rkt") list-machine-typing bug1)
|
||||
|
||||
(include/rewrite "generators.rkt" generators bug-mod-rw return-stopped-rw)
|
||||
(include/rewrite (lib "redex/benchmark/models/list-machine/ls-typed-gen.rkt") ls-typed-gen bug1-typed)
|
||||
|
||||
(define-rewrite bug-mod3
|
||||
redex/benchmark/list-machine/ls-typed-gen
|
||||
==>
|
||||
(submod ".." ls-typed-gen)
|
||||
#:context (require))
|
||||
|
||||
(include/rewrite "generators.rkt" generators bug-mod-rw return-stopped-rw bug-mod3)
|
||||
|
||||
(define small-counter-example
|
||||
(term (l0 : (begin (cons v0 Z v0) halt) end)))
|
||||
(term ((l0 : (begin (cons v0 Z v0) halt) end)
|
||||
(l0 : (v0 : nil empty) empty))))
|
||||
|
||||
(test small-counter-example)
|
||||
|
|
|
|||
|
|
@ -67,6 +67,7 @@
|
|||
(include/rewrite "generators.rkt" generators bug-mod-rw stop-earlier-rw)
|
||||
|
||||
(define small-counter-example
|
||||
(term (l0 : (begin (cons v0 v0 v0) halt) end)))
|
||||
(term ((l0 : (begin (cons v0 v0 v0) halt) end)
|
||||
(l0 : (v0 : nil empty) empty))))
|
||||
|
||||
(test small-counter-example)
|
||||
|
|
|
|||
|
|
@ -29,6 +29,7 @@
|
|||
(include/rewrite "generators.rkt" generators bug-mod-rw)
|
||||
|
||||
(define small-counter-example
|
||||
(term (l0 : (begin (cons v0 v0 v0) (begin (fetch-field v0 1 v0) halt)) end)))
|
||||
(term ((l0 : (begin (cons v0 v0 v0) (begin (fetch-field v0 1 v0) halt)) end)
|
||||
(l0 : (v0 : nil empty) empty))))
|
||||
|
||||
(test small-counter-example)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,429 @@
|
|||
#lang racket
|
||||
|
||||
(define the-error "no error")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
racket/list
|
||||
racket/match)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
(define-language list-machine
|
||||
(a nil
|
||||
(cons a a))
|
||||
(v variable-not-otherwise-mentioned)
|
||||
(r empty
|
||||
(r v ↦ a))
|
||||
(l variable-not-otherwise-mentioned)
|
||||
(ι (jump l)
|
||||
(branch-if-nil v l)
|
||||
(fetch-field v 0 v)
|
||||
(fetch-field v 1 v)
|
||||
(cons v v v)
|
||||
halt
|
||||
(begin ι ι))
|
||||
(p (l : ι p)
|
||||
end))
|
||||
|
||||
(define-judgment-form list-machine
|
||||
#:contract (var-lookup r v a)
|
||||
#:mode (var-lookup I I O)
|
||||
[-----
|
||||
(var-lookup (r v ↦ a) v a)]
|
||||
[(where #t (different v_1 v_2))
|
||||
(var-lookup r v_2 a_2)
|
||||
-----
|
||||
(var-lookup (r v_1 ↦ a_1) v_2 a_2)])
|
||||
|
||||
(define-judgment-form list-machine
|
||||
#:contract (var-set r v a r)
|
||||
#:mode (var-set I I I O)
|
||||
[-----
|
||||
(var-set (r v ↦ a) v a_2 (r v ↦ a_2))]
|
||||
[(where #t (different v v_2))
|
||||
(var-set r v_2 a_2 r_2)
|
||||
-----
|
||||
(var-set (r v ↦ a) v_2 a_2 (r_2 v ↦ a))]
|
||||
[-----
|
||||
(var-set empty v a (empty v ↦ a))])
|
||||
|
||||
(define-judgment-form list-machine
|
||||
#:contract (program-lookup p l ι)
|
||||
#:mode (program-lookup I I O)
|
||||
[-----
|
||||
(program-lookup (l : ι p) l ι)]
|
||||
[(where #t (different l l_2))
|
||||
(program-lookup p l_2 ι_2)
|
||||
-----
|
||||
(program-lookup (l : ι p) l_2 ι_2)])
|
||||
|
||||
(define red
|
||||
(reduction-relation
|
||||
list-machine
|
||||
#:domain (p r ι)
|
||||
(--> (p r (begin (begin ι_1 ι_2) ι_3))
|
||||
(p r (begin ι_1 (begin ι_2 ι_3)))
|
||||
"step-seq")
|
||||
(--> (p r (begin (fetch-field v 0 v_2) ι))
|
||||
(p r_2 ι)
|
||||
"step-fetch-field-0"
|
||||
(judgment-holds (var-lookup r v (cons a_0 a_1)))
|
||||
(judgment-holds (var-set r v_2 a_0 r_2)))
|
||||
(--> (p r (begin (fetch-field v 1 v_2) ι))
|
||||
(p r_2 ι)
|
||||
"step-fetch-field-1"
|
||||
(judgment-holds (var-lookup r v (cons a_0 a_1)))
|
||||
(judgment-holds (var-set r v_2 a_1 r_2)))
|
||||
(--> (p r (begin (cons v_0 v_1 v_2) ι))
|
||||
(p r_2 ι)
|
||||
"step-cons"
|
||||
(judgment-holds (var-lookup r v_0 a_0))
|
||||
(judgment-holds (var-lookup r v_1 a_1))
|
||||
(judgment-holds (var-set r v_2 (cons a_0 a_1) r_2)))
|
||||
(--> (p r (begin (branch-if-nil v l) ι))
|
||||
(p r ι)
|
||||
"step-branch-not-taken"
|
||||
(judgment-holds (var-lookup r v (cons a_0 a_1))))
|
||||
(--> (p r (begin (branch-if-nil v l) ι))
|
||||
(p r ι_2)
|
||||
"step-branch-taken"
|
||||
(judgment-holds (var-lookup r v nil))
|
||||
(judgment-holds (program-lookup p l ι_2)))
|
||||
(--> (p r (jump l))
|
||||
(p r ι_2)
|
||||
"step-jump"
|
||||
(judgment-holds (program-lookup p l ι_2)))))
|
||||
|
||||
(define (run-prog p)
|
||||
(define r_0 (term (empty v0 ↦ nil)))
|
||||
(define ι_0 (car (judgment-holds (program-lookup ,p l0 ι) ι)))
|
||||
(apply-reduction-relation* red `(,p ,r_0 ,ι_0)))
|
||||
|
||||
|
||||
(define (check-progress p)
|
||||
(define r_0 (term (empty v0 ↦ nil)))
|
||||
(define ι_0 (car (judgment-holds (program-lookup ,p l0 ι) ι)))
|
||||
(or (equal? ι_0 'halt)
|
||||
(and
|
||||
(= 1
|
||||
(length (apply-reduction-relation
|
||||
red
|
||||
`(,p ,r_0 ,ι_0))))
|
||||
(let ([closure (apply-reduction-relation*
|
||||
red
|
||||
`(,p ,r_0 ,ι_0)
|
||||
#:stop-when
|
||||
(let ([count 0])
|
||||
(λ (_)
|
||||
(begin0
|
||||
(count . > . 1000)
|
||||
(set! count (add1 count))))))])
|
||||
;; if reduction terminates in less than 1000 steps, check it ends with halt
|
||||
;; (if the #:stop-when condition is true, we get back an empty list,
|
||||
;; and the same thing for a reduction cycle)
|
||||
(or (empty? closure)
|
||||
(and (= 1 (length closure))
|
||||
(match (car closure)
|
||||
[`(,p ,r ,ι)
|
||||
(equal? ι 'halt)])))))))
|
||||
|
||||
(define (check p)
|
||||
(or (not p)
|
||||
(check-progress p)))
|
||||
|
||||
(define-metafunction list-machine
|
||||
different : any any -> any
|
||||
[(different any_1 any_1)
|
||||
#f]
|
||||
[(different any_1 any_2)
|
||||
#t])
|
||||
|
||||
(define-extended-language list-machine-typing list-machine
|
||||
(τ nil (list τ) (listcons τ))
|
||||
(Γ empty (v : τ Γ))
|
||||
(Π empty (l : Γ Π)))
|
||||
|
||||
(define-judgment-form list-machine-typing
|
||||
#:contract (check-program p Π)
|
||||
#:mode (check-program I I)
|
||||
[(:lookup-Π Π l0 (v0 : nil empty))
|
||||
(labels-distinct (l0 : ι p))
|
||||
;; note : changed from l-⊂
|
||||
(d= Π (l0 : ι p))
|
||||
(labels-distinct-Π Π)
|
||||
(check-blocks Π (l0 : ι p))
|
||||
-----
|
||||
(check-program (l0 : ι p) Π)])
|
||||
|
||||
(define-judgment-form list-machine-typing
|
||||
#:contract (Γ-⊂ Γ Γ)
|
||||
#:mode (Γ-⊂ I I)
|
||||
[-----
|
||||
(Γ-⊂ Γ empty)]
|
||||
[(:lookup-Γ Γ_1 v τ_1)
|
||||
(⊂ τ_1 τ_2)
|
||||
(Γ-⊂ Γ_1 Γ_2)
|
||||
----
|
||||
(Γ-⊂ Γ_1 (v : τ_2 Γ_2))])
|
||||
|
||||
(define-judgment-form list-machine-typing
|
||||
#:contract (check-blocks Π p)
|
||||
#:mode (check-blocks I I)
|
||||
[(:lookup-Π Π l Γ)
|
||||
(check-block Π Γ ι)
|
||||
(check-blocks Π p)
|
||||
-----
|
||||
(check-blocks Π (l : ι p)) ]
|
||||
[-----
|
||||
(check-blocks Π end)])
|
||||
|
||||
(define-judgment-form list-machine-typing
|
||||
#:contract (check-block Π Γ ι)
|
||||
#:mode (check-block I I I)
|
||||
[-----
|
||||
(check-block Π Γ halt)]
|
||||
[(check-instr Π Γ ι_1 Γ_2)
|
||||
(check-block Π Γ_2 ι_2)
|
||||
-----
|
||||
(check-block Π Γ (begin ι_1 ι_2))]
|
||||
[(:lookup-Π Π l Γ_2)
|
||||
(Γ-⊂ Γ Γ_2)
|
||||
-----
|
||||
(check-block Π Γ (jump l))])
|
||||
|
||||
(define-judgment-form list-machine-typing
|
||||
#:contract (check-instr Π Γ ι Γ)
|
||||
#:mode (check-instr I I I O)
|
||||
[(check-instr Π Γ ι_1 Γ_1)
|
||||
(check-instr Π Γ_1 ι_2 Γ_2)
|
||||
-----
|
||||
(check-instr Π Γ (begin ι_1 ι_2) Γ_2)]
|
||||
[(:lookup-Γ Γ v (list τ))
|
||||
(:lookup-Π Π l Γ_1)
|
||||
(:set Γ v nil Γ_3)
|
||||
(Γ-⊂ Γ_3 Γ_1)
|
||||
(:set Γ_3 v (listcons τ) Γ_2)
|
||||
-----
|
||||
(check-instr Π Γ (branch-if-nil v l) Γ_2)]
|
||||
[(:lookup-Γ Γ v (listcons τ))
|
||||
(:lookup-Π Π l Γ_1)
|
||||
(:set Γ v nil Γ_2)
|
||||
(Γ-⊂ Γ_2 Γ_1)
|
||||
-----
|
||||
(check-instr Π Γ (branch-if-nil v l) Γ)]
|
||||
[(:lookup-Γ Γ v nil)
|
||||
(:lookup-Π Π l Γ_1)
|
||||
(Γ-⊂ Γ Γ_1)
|
||||
-----
|
||||
(check-instr Π Γ (branch-if-nil v l) Γ)]
|
||||
[(:lookup-Γ Γ v (listcons τ)) (:set Γ v_2 τ Γ_2)
|
||||
-----
|
||||
(check-instr Π Γ (fetch-field v 0 v_2) Γ_2)]
|
||||
[(:lookup-Γ Γ v (listcons τ)) (:set Γ v_2 (list τ) Γ_2)
|
||||
-----
|
||||
(check-instr Π Γ (fetch-field v 1 v_2) Γ_2)]
|
||||
[(:lookup-Γ Γ v_0 τ_0) (:lookup-Γ Γ v_1 τ_1)
|
||||
(⊔ (list τ_0) τ_1 (list τ)) (:set Γ v (listcons τ) Γ_2)
|
||||
-----
|
||||
(check-instr Π Γ (cons v_0 v_1 v) Γ_2)])
|
||||
|
||||
(define-judgment-form list-machine-typing
|
||||
#:contract (⊂ τ τ)
|
||||
#:mode (⊂ O I)
|
||||
[-----
|
||||
(⊂ τ τ)]
|
||||
[-----
|
||||
(⊂ nil (list τ))]
|
||||
[(⊂ τ τ_2)
|
||||
-----
|
||||
(⊂ (list τ) (list τ_2))]
|
||||
[(⊂ τ τ_2)
|
||||
-----
|
||||
(⊂ (listcons τ) (list τ_2))]
|
||||
[(⊂ τ τ_2)
|
||||
-----
|
||||
(⊂ (listcons τ) (listcons τ_2))])
|
||||
|
||||
(define-judgment-form list-machine-typing
|
||||
#:contract (⊔ τ τ τ)
|
||||
#:mode (⊔ I I O)
|
||||
[-----
|
||||
(⊔ τ τ τ)]
|
||||
[-----
|
||||
(⊔ (list τ) nil (list τ))]
|
||||
[-----
|
||||
(⊔ nil (list τ) (list τ))]
|
||||
[(⊔ (list τ_1) (list τ_2) τ_3)
|
||||
-----
|
||||
(⊔ (list τ_1) (listcons τ_2) τ_3)]
|
||||
[(⊔ (list τ_1) (list τ_2) τ_3)
|
||||
-----
|
||||
(⊔ (listcons τ_1) (list τ_2) τ_3)]
|
||||
[(⊔ τ_1 τ_2 τ_3)
|
||||
-----
|
||||
(⊔ (list τ_1) (list τ_2) (list τ_3))]
|
||||
[-----
|
||||
(⊔ (listcons τ) nil (list τ))]
|
||||
[-----
|
||||
(⊔ nil (listcons τ) (list τ))]
|
||||
[(⊔ τ_1 τ_2 τ_3)
|
||||
-----
|
||||
(⊔ (listcons τ_1) (listcons τ_2) (listcons τ_3))])
|
||||
|
||||
(define-judgment-form list-machine-typing
|
||||
#:contract (:lookup any v any)
|
||||
#:mode (:lookup I I O)
|
||||
[-----
|
||||
(:lookup (v : any_τ any_Γ) v any_τ)]
|
||||
[(where #t (different v_1 v_2))
|
||||
(:lookup any_Γ v_2 any_τ2)
|
||||
-----
|
||||
(:lookup (v_1 : any_τ1 any_Γ) v_2 any_τ2)])
|
||||
|
||||
(define-judgment-form list-machine-typing
|
||||
#:contract (:lookup-Γ Γ v τ)
|
||||
#:mode (:lookup-Γ I I O)
|
||||
[-----
|
||||
(:lookup-Γ (v : τ Γ) v τ)]
|
||||
[(where #t (different v_1 v_2))
|
||||
(:lookup-Γ Γ v_2 τ_2)
|
||||
-----
|
||||
(:lookup-Γ (v_1 : τ_1 Γ) v_2 τ_2)])
|
||||
|
||||
(define-judgment-form list-machine-typing
|
||||
#:contract (:lookup-Π Π l Γ)
|
||||
#:mode (:lookup-Π I I O)
|
||||
[-----
|
||||
(:lookup-Π (l : Γ Π) l Γ)]
|
||||
[(where #t (different l_1 l_2))
|
||||
(:lookup-Π Π l_2 Γ_2)
|
||||
-----
|
||||
(:lookup-Π (l_1 : Γ_1 Π) l_2 Γ_2)])
|
||||
|
||||
(define-judgment-form list-machine-typing
|
||||
#:contract (:set Γ v τ Γ)
|
||||
#:mode (:set I I I O)
|
||||
[-----
|
||||
(:set (v : any_τ any_Γ) v any_τ2 (v : any_τ2 any_Γ))]
|
||||
[(where #t (different v v_2))
|
||||
(:set any_Γ v_2 any_τ2 any_Γ2)
|
||||
-----
|
||||
(:set (v : any_τ any_Γ) v_2 any_τ2 (v : any_τ any_Γ2))]
|
||||
[-----
|
||||
(:set empty v any_τ (v : any_τ empty))])
|
||||
|
||||
(define-metafunction list-machine-typing
|
||||
[(dom (l_1 : any_1 any_2))
|
||||
(l_1 (dom any_2))]
|
||||
[(dom empty) empty])
|
||||
|
||||
(define-metafunction list-machine-typing
|
||||
[(dom-P (l_1 : ι_1 p))
|
||||
(l_1 (dom p))]
|
||||
[(dom-P end) empty])
|
||||
|
||||
(define-metafunction list-machine-typing
|
||||
[(dom-Π (l_1 : Γ_1 Π))
|
||||
(l_1 (dom Π))]
|
||||
[(dom-Π empty) empty])
|
||||
|
||||
#;
|
||||
(define-metafunction list-machine-typing
|
||||
l-⊂ : (l ...) (l ...) -> any
|
||||
[(l-⊂ (l_1 ...) (l_2 ...))
|
||||
,(let ([ht (make-hash)])
|
||||
(for ([l (in-list (term (l_2 ...)))])
|
||||
(hash-set! ht l #t))
|
||||
(for/and ([l (in-list (term (l_1 ...)))])
|
||||
(hash-ref ht l #f)))])
|
||||
|
||||
(define-relation list-machine-typing
|
||||
[(l-⊂ (l_1 empty) l_2)
|
||||
(where #t (lmem l_1 l_2))]
|
||||
[(l-⊂ (l_1 l_2) l_3)
|
||||
(l-⊂ l_2 l_3)
|
||||
(where #t (lmem l_1 l_3))]
|
||||
[(l-⊂ empty any)])
|
||||
|
||||
(define-relation list-machine-typing
|
||||
[(d= (l_1 : Γ_1 Π) (l_1 : ι p))
|
||||
(d= Π p)]
|
||||
[(d= empty end)])
|
||||
|
||||
(define-relation list-machine-typing
|
||||
[(d-⊂ (l_1 : Γ_1 Π) p)
|
||||
(has-label p l_1)
|
||||
(d-⊂ Π p)]
|
||||
[(d-⊂ (l_1 : Γ_1 Π) (l_2 : ι p))
|
||||
(d-⊂ (l_1 : Γ_1 Π) p)]
|
||||
[(d-⊂ empty p)])
|
||||
|
||||
(define-relation list-machine-typing
|
||||
[(has-label (l_1 : ι p) l_1)]
|
||||
[(has-label (l_1 : ι p) l_2)
|
||||
(has-label p l_2)])
|
||||
|
||||
(define-relation list-machine-typing
|
||||
[(labels-distinct (l_1 : ι p))
|
||||
(label-not-in l_1 p)
|
||||
(labels-distinct p)]
|
||||
[(labels-distinct end)])
|
||||
|
||||
(define-relation list-machine-typing
|
||||
[(label-not-in l_1 (l_2 : ι p))
|
||||
(different l_1 l_2)
|
||||
(label-not-in l_1 p)]
|
||||
[(label-not-in l_1 end)])
|
||||
|
||||
(define-metafunction list-machine-typing
|
||||
[(lmem l_1 (l_1 l_2))
|
||||
#t]
|
||||
[(lmem l_1 (l_2 l_3))
|
||||
(lmem l_1 l_3)]
|
||||
[(lmem l_1 empty)
|
||||
#f])
|
||||
|
||||
(define-relation list-machine-typing
|
||||
[(labels-distinct-Π (l_1 : Γ Π))
|
||||
(label-not-in-Π l_1 Π)
|
||||
(labels-distinct-Π Π)]
|
||||
[(labels-distinct-Π empty)])
|
||||
|
||||
(define-relation list-machine-typing
|
||||
[(label-not-in-Π l_1 (l_2 : Γ Π))
|
||||
(different l_1 l_2)
|
||||
(label-not-in-Π l_1 Π)]
|
||||
[(label-not-in-Π l_1 empty)])
|
||||
|
||||
(define (generate-M-term)
|
||||
(generate-term list-machine-typing (l0 : ι p) 7))
|
||||
|
||||
(define (type-check p)
|
||||
;; need to provide a program typing, so generate 10 randomly and
|
||||
;; see if any succeed...
|
||||
(let loop ([i 0])
|
||||
(cond
|
||||
[(i . > . 10) #f]
|
||||
[else
|
||||
(define guess-Π (generate-term list-machine-typing (l0 : (v0 : nil empty) Π) 7))
|
||||
(or (judgment-holds (check-program ,p ,guess-Π))
|
||||
(loop (add1 i)))])))
|
||||
|
||||
(define (typed-generator)
|
||||
(let ([g (redex-generator list-machine-typing
|
||||
(check-program p Π)
|
||||
7)])
|
||||
(λ ()
|
||||
(match (g)
|
||||
[`(check-program ,p ,Π)
|
||||
p]
|
||||
[#f #f]))))
|
||||
|
||||
(define (generate-typed-term)
|
||||
(match (generate-term list-machine-typing
|
||||
#:satisfying
|
||||
(check-program p Π)
|
||||
7)
|
||||
[`(check-program ,p ,Π)
|
||||
p]
|
||||
[#f #f]))
|
||||
|
|
@ -0,0 +1,14 @@
|
|||
#lang racket/base
|
||||
|
||||
(require racket/runtime-path
|
||||
"../util/info-util.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
(define name "list-machine")
|
||||
(define fname (make-path-root 'list-machine))
|
||||
|
||||
(define-runtime-path here ".")
|
||||
|
||||
(define (all-mods)
|
||||
(all-mods/type 'typed here name fname))
|
||||
|
|
@ -3,7 +3,8 @@
|
|||
(require redex/examples/poly-stlc
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
redex/reduction-semantics
|
||||
racket/bool)
|
||||
racket/bool
|
||||
racket/match)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
|
@ -32,6 +33,15 @@
|
|||
(define (generate [index 0])
|
||||
(generate-term poly-stlc M #:i-th index)))
|
||||
|
||||
(module+ typed-mod
|
||||
(provide generate get-generator type)
|
||||
(define type 'search)
|
||||
(define (get-generator) generate)
|
||||
(define (generate)
|
||||
((match-lambda [`(typeof • ,M ,τ) M]
|
||||
[#f #f])
|
||||
(generate-term poly-stlc #:satisfying (typeof • M τ) 3))))
|
||||
|
||||
(module+ check-mod
|
||||
(provide check)
|
||||
(define (check term)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,14 @@
|
|||
#lang racket/base
|
||||
|
||||
(require racket/runtime-path
|
||||
"../util/info-util.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
(define name "poly-stlc")
|
||||
(define fname (make-path-root 'poly-stlc))
|
||||
|
||||
(define-runtime-path here ".")
|
||||
|
||||
(define (all-mods)
|
||||
(all-mods/type 'typed here name fname))
|
||||
|
|
@ -33,6 +33,16 @@
|
|||
(define (generate [index 0])
|
||||
(generate-term rbtrees t #:i-th index)))
|
||||
|
||||
(module+ typed-mod
|
||||
(provide generate get-generator type)
|
||||
(define type 'search)
|
||||
(define (get-generator) generate)
|
||||
(define (generate)
|
||||
((match-lambda
|
||||
[`(rb-tree ,t) t]
|
||||
[#f #f])
|
||||
(generate-term rbtrees #:satisfying (rb-tree t) 3))))
|
||||
|
||||
(module+ check-mod
|
||||
(provide check)
|
||||
(define (check t)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,14 @@
|
|||
#lang racket/base
|
||||
|
||||
(require racket/runtime-path
|
||||
"../util/info-util.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
(define name "rbtrees")
|
||||
(define fname (make-path-root 'rbtrees))
|
||||
|
||||
(define-runtime-path here ".")
|
||||
|
||||
(define (all-mods)
|
||||
(all-mods/type 'typed here name fname))
|
||||
|
|
@ -7,6 +7,7 @@
|
|||
redex/examples/racket-machine/grammar
|
||||
redex/examples/racket-machine/verification
|
||||
redex/examples/racket-machine/randomized-tests
|
||||
(prefix-in jdg: redex/benchmark/models/rvm/verif-jdg)
|
||||
(only-in redex/private/generate-term pick-an-index))
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
|
@ -36,6 +37,20 @@
|
|||
(define (generate [index 0])
|
||||
(fix (generate-term bytecode e #:i-th index))))
|
||||
|
||||
(module+ typed-mod
|
||||
(provide generate get-generator type)
|
||||
(define (get-generator) generate)
|
||||
(define type 'search)
|
||||
(define (generate)
|
||||
(match (generate-term
|
||||
jdg:vl
|
||||
#:satisfying
|
||||
(jdg:V e • O #f • • ∅ s_1 γ_1 η_1)
|
||||
4)
|
||||
[#f #f]
|
||||
[`(jdg:V ,e • O #f • • ∅ ,s_1 ,γ_1 ,η_1)
|
||||
(fix (term (jdg:trans-e ,e)))])))
|
||||
|
||||
(module+ check-mod
|
||||
(provide check)
|
||||
(define (check e)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,43 @@
|
|||
#lang racket
|
||||
|
||||
(require redex/reduction-semantics)
|
||||
|
||||
(define-language bytecode
|
||||
(e (loc n)
|
||||
(loc-noclr n)
|
||||
(loc-clr n)
|
||||
(loc-box n)
|
||||
(loc-box-noclr n)
|
||||
(loc-box-clr n)
|
||||
|
||||
(let-one e e)
|
||||
(let-void n e)
|
||||
(let-void-box n e)
|
||||
|
||||
(boxenv n e)
|
||||
(install-value n e e)
|
||||
(install-value-box n e e)
|
||||
|
||||
(application e e ...)
|
||||
(seq e e e ...)
|
||||
(branch e e e)
|
||||
(let-rec (l ...) e)
|
||||
(indirect x)
|
||||
(proc-const (τ ...) e)
|
||||
(case-lam l ...)
|
||||
l
|
||||
v)
|
||||
|
||||
(l (lam (τ ...) (n ...) e))
|
||||
|
||||
(v number
|
||||
void
|
||||
'variable
|
||||
b)
|
||||
|
||||
(τ val ref)
|
||||
(n natural)
|
||||
(b #t #f)
|
||||
((x y) variable))
|
||||
|
||||
(provide bytecode)
|
||||
|
|
@ -39,6 +39,38 @@
|
|||
#:variables (rest rest1 rest2 ellipsis)
|
||||
#:exactly-once)
|
||||
|
||||
(define-rewrite bug14a-jdg
|
||||
((where uninit (sref n s_2))
|
||||
. rest)
|
||||
==>
|
||||
rest
|
||||
#:context (define-judgment-form)
|
||||
#:variables (rest)
|
||||
#:exactly-once)
|
||||
|
||||
(define-rewrite bug14b-jdg
|
||||
((uninits s_a)
|
||||
. rest)
|
||||
==>
|
||||
rest
|
||||
#:context (define-judgment-form)
|
||||
#:variables (rest)
|
||||
#:exactly-once)
|
||||
|
||||
(define-rewrite bug14c-jdg
|
||||
([(closure-intact (imm-nc sl_1) (imm sl_2))
|
||||
(closure-intact sl_1 sl_2)]
|
||||
. rest)
|
||||
==>
|
||||
([(closure-intact (imm-nc sl_1) (imm sl_2))
|
||||
(closure-intact sl_1 sl_2)]
|
||||
[(closure-intact (box sl_1) (imm sl_2))
|
||||
(closure-intact sl_1 sl_2)]
|
||||
. rest)
|
||||
#:context (define-relation)
|
||||
#:variables (rest)
|
||||
#:exactly-once)
|
||||
|
||||
(define-rewrite/compose bug14 bug14a bug14b bug14c)
|
||||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/grammar.rkt") grammar)
|
||||
|
|
@ -47,6 +79,8 @@
|
|||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/randomized-tests.rkt") randomized-tests rt-rw)
|
||||
|
||||
(include/rewrite (lib "redex/benchmark/models/rvm/verif-jdg.rkt") verif-jdg bug14a-jdg bug14b-jdg bug14c-jdg)
|
||||
|
||||
(include/rewrite "generators.rkt" generators bug-mod-rw)
|
||||
|
||||
(define small-counter-example
|
||||
|
|
|
|||
|
|
@ -24,12 +24,26 @@
|
|||
#:context (match)
|
||||
#:exactly-once)
|
||||
|
||||
(define-rewrite bug15-jdg
|
||||
[(lam-verified?* ((lam τl nl e) el) sl m)
|
||||
(vals τl)
|
||||
(lam-verified? (lam τl nl e) sl m)
|
||||
(lam-verified?* el sl m)]
|
||||
==>
|
||||
[(lam-verified?* ((lam τl nl e) el) sl m)
|
||||
(lam-verified? (lam τl nl e) sl m)
|
||||
(lam-verified?* el sl m)]
|
||||
#:context (define-judgment-form)
|
||||
#:exactly-once)
|
||||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/grammar.rkt") grammar)
|
||||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/verification.rkt") verification bug15v)
|
||||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/randomized-tests.rkt") randomized-tests rt-rw bug15rt)
|
||||
|
||||
(include/rewrite (lib "redex/benchmark/models/rvm/verif-jdg.rkt") verif-jdg bug15-jdg)
|
||||
|
||||
(include/rewrite "generators.rkt" generators bug-mod-rw)
|
||||
|
||||
(define small-counter-example
|
||||
|
|
|
|||
|
|
@ -20,10 +20,23 @@
|
|||
#:variables (ellipsis1 ellipsis2)
|
||||
#:exactly-once)
|
||||
|
||||
(define-rewrite bug2-jdg
|
||||
[(redo-clrs ((n ν) γ) s (supdt (n- (n- (slen s) n) (S O)) not s_2))
|
||||
(n< n (slen s))
|
||||
(n≠ (n- (slen s) n) O)
|
||||
(redo-clrs γ s s_2)]
|
||||
==>
|
||||
[(redo-clrs ((n ν) γ) s (supdt (n- (n- (slen s) n) (S O)) not s_2))
|
||||
(redo-clrs γ s s_2)]
|
||||
#:context (define-judgment-form)
|
||||
#:exactly-once)
|
||||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/grammar.rkt") grammar)
|
||||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/verification.rkt") verification bug2)
|
||||
|
||||
(include/rewrite (lib "redex/benchmark/models/rvm/verif-jdg.rkt") verif-jdg bug2-jdg)
|
||||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/randomized-tests.rkt") randomized-tests rt-rw)
|
||||
|
||||
(include/rewrite "generators.rkt" generators bug-mod-rw)
|
||||
|
|
|
|||
|
|
@ -11,8 +11,12 @@
|
|||
(define-rewrite bug3
|
||||
(abs-push n not s)
|
||||
==>
|
||||
(abs-push n uninit s)
|
||||
#:context (define-metafunction))
|
||||
(abs-push n uninit s))
|
||||
|
||||
(define-rewrite bug3-jdg
|
||||
(abs-push n not sl)
|
||||
==>
|
||||
(abs-push n uninit sl))
|
||||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/grammar.rkt") grammar)
|
||||
|
||||
|
|
@ -20,6 +24,8 @@
|
|||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/randomized-tests.rkt") randomized-tests rt-rw)
|
||||
|
||||
(include/rewrite (lib "redex/benchmark/models/rvm/verif-jdg.rkt") verif-jdg bug3 bug3-jdg)
|
||||
|
||||
(include/rewrite "generators.rkt" generators bug-mod-rw)
|
||||
|
||||
(define small-counter-example
|
||||
|
|
|
|||
|
|
@ -16,12 +16,26 @@
|
|||
#:variables (rest)
|
||||
#:exactly-once)
|
||||
|
||||
(define-rewrite bug4-jdg
|
||||
[(V (boxenv n_p e) s n_l b γ η f s_2 γ_2 η_2)
|
||||
(where imm (sref n_p s))
|
||||
(V e (supdt n_p box s) n_l b γ η f s_2 γ_2 η_2)
|
||||
(n< n_p n_l)]
|
||||
==>
|
||||
[(V (boxenv n_p e) s n_l b γ η f s_2 γ_2 η_2)
|
||||
(where imm (sref n_p s))
|
||||
(V e (supdt n_p box s) n_l b γ η f s_2 γ_2 η_2)]
|
||||
#:context (define-judgment-form)
|
||||
#:exactly-once)
|
||||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/grammar.rkt") grammar)
|
||||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/verification.rkt") verification bug3)
|
||||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/randomized-tests.rkt") randomized-tests rt-rw)
|
||||
|
||||
(include/rewrite (lib "redex/benchmark/models/rvm/verif-jdg.rkt") verif-jdg bug4-jdg)
|
||||
|
||||
(include/rewrite "generators.rkt" generators bug-mod-rw)
|
||||
|
||||
(define small-counter-example
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@
|
|||
|
||||
(define the-error "mishandling branches when then branch needs more stack than else branch; bug in the let-rec case not checking a stack bound")
|
||||
|
||||
(define-rewrite bug3
|
||||
(define-rewrite bug5
|
||||
((side-condition (<= (term n) (term n_l)))
|
||||
. rest)
|
||||
==>
|
||||
|
|
@ -16,12 +16,23 @@
|
|||
#:variables (rest)
|
||||
#:exactly-once)
|
||||
|
||||
(define-rewrite bug5-jdg
|
||||
((n<= n n_l)
|
||||
. rest)
|
||||
==>
|
||||
rest
|
||||
#:context (define-judgment-form)
|
||||
#:variables (rest)
|
||||
#:exactly-once)
|
||||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/grammar.rkt") grammar)
|
||||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/verification.rkt") verification bug3)
|
||||
(include/rewrite (lib "redex/examples/racket-machine/verification.rkt") verification bug5)
|
||||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/randomized-tests.rkt") randomized-tests rt-rw)
|
||||
|
||||
(include/rewrite (lib "redex/benchmark/models/rvm/verif-jdg.rkt") verif-jdg bug5-jdg)
|
||||
|
||||
(include/rewrite "generators.rkt" generators bug-mod-rw)
|
||||
|
||||
(define small-counter-example
|
||||
|
|
|
|||
|
|
@ -16,12 +16,22 @@
|
|||
#:variables (rest ellipsis)
|
||||
#:exactly-once)
|
||||
|
||||
(define-rewrite bug6-jdg
|
||||
[(V (case-lam el) s n_l b γ η f s γ η)
|
||||
(lam-verified?* el s ?)]
|
||||
==>
|
||||
[(V (case-lam el) s n_l b γ η f s γ η)]
|
||||
#:context (define-judgment-form)
|
||||
#:exactly-once)
|
||||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/grammar.rkt") grammar)
|
||||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/verification.rkt") verification bug6)
|
||||
|
||||
(include/rewrite (lib "redex/examples/racket-machine/randomized-tests.rkt") randomized-tests rt-rw)
|
||||
|
||||
(include/rewrite (lib "redex/benchmark/models/rvm/verif-jdg.rkt") verif-jdg bug6-jdg)
|
||||
|
||||
(include/rewrite "generators.rkt" generators bug-mod-rw)
|
||||
|
||||
(define small-counter-example
|
||||
|
|
|
|||
|
|
@ -0,0 +1,14 @@
|
|||
#lang racket/base
|
||||
|
||||
(require racket/runtime-path
|
||||
"../util/info-util.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
(define name "rvm")
|
||||
(define fname (make-path-root 'rvm))
|
||||
|
||||
(define-runtime-path here ".")
|
||||
|
||||
(define (all-mods)
|
||||
(all-mods/type 'typed here name fname))
|
||||
|
|
@ -24,6 +24,12 @@
|
|||
(submod ".." randomized-tests)
|
||||
#:context (require))
|
||||
|
||||
(define-rewrite bug-mod-4
|
||||
redex/benchmark/models/rvm/verif-jdg
|
||||
==>
|
||||
(submod ".." verif-jdg)
|
||||
#:context (require))
|
||||
|
||||
;; adjust large numbers to keep the reduction from blowing up
|
||||
(define-rewrite rt-rw
|
||||
[`(,(and (or 'let-void 'let-void-box) i) ,n ,e)
|
||||
|
|
@ -34,7 +40,7 @@
|
|||
#:exactly-once
|
||||
#:context (match))
|
||||
|
||||
(define-rewrite/compose bug-mod-rw bug-mod-1 bug-mod-2 bug-mod-3)
|
||||
(define-rewrite/compose bug-mod-rw bug-mod-1 bug-mod-2 bug-mod-3 bug-mod-4)
|
||||
|
||||
(define-syntax-rule (test cexp)
|
||||
(module+ test
|
||||
|
|
|
|||
|
|
@ -0,0 +1,754 @@
|
|||
#lang racket
|
||||
|
||||
(require redex/reduction-semantics)
|
||||
(require "jdg-grammar.rkt")
|
||||
|
||||
(require redex/private/gen-trace
|
||||
(only-in redex/private/generate-term
|
||||
enable-gen-trace!))
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
||||
(define (bytecode-ok? e)
|
||||
(not (eq? 'invalid (car (term (verify ,e () 0 #f () () ∅))))))
|
||||
|
||||
(define (bytecode-ok/V? e)
|
||||
(judgment-holds
|
||||
(V ,e • O #f • • ∅ s_1 γ_1 η_1)))
|
||||
|
||||
(define-extended-language verification
|
||||
bytecode
|
||||
(s (ṽ ...) invalid)
|
||||
(ṽ uninit imm box imm-nc box-nc not)
|
||||
(γ ((n ṽ) ...))
|
||||
(η (n ...))
|
||||
(f (n n (ṽ ...)) ∅)
|
||||
(m n ?))
|
||||
|
||||
(define-language bl
|
||||
(e (loc n)
|
||||
(loc-noclr n)
|
||||
(loc-clr n)
|
||||
(loc-box n)
|
||||
(loc-box-noclr n)
|
||||
(loc-box-clr n)
|
||||
|
||||
(let-one e e)
|
||||
(let-void n e)
|
||||
(let-void-box n e)
|
||||
|
||||
(boxenv n e)
|
||||
(install-value n e e)
|
||||
(install-value-box n e e)
|
||||
|
||||
(application e el)
|
||||
;; change to (seq el) ?
|
||||
(seq e e)
|
||||
(branch e e e)
|
||||
(let-rec ll e)
|
||||
(indirect x)
|
||||
(proc-const τl e)
|
||||
(case-lam ll)
|
||||
l
|
||||
v)
|
||||
|
||||
(el (e el) •)
|
||||
|
||||
(l (lam τl nl e))
|
||||
|
||||
(ll (l ll) •)
|
||||
|
||||
(τl (τ τl) •)
|
||||
|
||||
(nl (n nl) •)
|
||||
|
||||
(v n
|
||||
void
|
||||
'variable
|
||||
b)
|
||||
|
||||
(τ val ref)
|
||||
(n O (S n))
|
||||
(b boolean)
|
||||
((x y) variable))
|
||||
|
||||
(define-metafunction bl
|
||||
[(trans-e (application e el))
|
||||
(application (trans-e e) (trans-e e_2) ...)
|
||||
(where (e_2 ...) (cns->lst el))]
|
||||
[(trans-e (proc-const τl e))
|
||||
(proc-const (cns->lst τl) (trans-e e))]
|
||||
[(trans-e (case-lam el))
|
||||
(case-lam any ...)
|
||||
(where (e ...) (cns->lst el))
|
||||
(where (any ...) ((trans-e e) ...))]
|
||||
[(trans-e (any n e))
|
||||
(any (trans-n n) (trans-e e))
|
||||
(side-condition (memq (term any) '(let-void let-void-box)))]
|
||||
[(trans-e (seq e_1 e_2))
|
||||
(seq any_3 ... any_4 ...)
|
||||
(where (any_3 ...) (un-seq e_1))
|
||||
(where (any_4 ...) (un-seq e_2))]
|
||||
[(trans-e (branch e_1 e_2 e_3))
|
||||
(branch (trans-e e_1) (trans-e e_2) (trans-e e_3))]
|
||||
[(trans-e (let-one e_1 e_2))
|
||||
(let-one (trans-e e_1) (trans-e e_2))]
|
||||
[(trans-e (boxenv n e))
|
||||
(boxenv (trans-n n) (trans-e e))]
|
||||
[(trans-e (any n e_1 e_2))
|
||||
(any (trans-n n) (trans-e e_1) (trans-e e_2))
|
||||
(side-condition (memq (term any) '(install-value install-value-box)))]
|
||||
[(trans-e (proc-const τl e))
|
||||
(proc-const (cns->lst τl) (trans-e e))]
|
||||
[(trans-e (let-rec ll e))
|
||||
(let-rec ((trans-l any_l) ...) (trans-e e))
|
||||
(where (any_l ...) (cns->lst ll))]
|
||||
[(trans-e (any n))
|
||||
(any (trans-n n))
|
||||
(side-condition (memq (term any) '(loc loc-noclr loc-clr loc-box loc-box-clr loc-box-noclr)))]
|
||||
[(trans-e l_1)
|
||||
(trans-l l_1)]
|
||||
[(trans-e n)
|
||||
(trans-n n)]
|
||||
[(trans-e any)
|
||||
any])
|
||||
|
||||
(define-metafunction bl
|
||||
[(trans-l (lam τl nl e))
|
||||
(lam (cns->lst τl) (number_2 ...) (trans-e e))
|
||||
(where (n_1 ...) (cns->lst nl))
|
||||
(where (number_2 ...) ((trans-n n_1) ...))])
|
||||
|
||||
(define-metafunction bl
|
||||
[(un-seq e_1)
|
||||
(any_2 ...)
|
||||
(where (seq any_2 ...) (trans-e e_1))]
|
||||
[(un-seq e)
|
||||
((trans-e e))])
|
||||
|
||||
(define-metafunction bl
|
||||
[(trans-n O)
|
||||
0]
|
||||
[(trans-n (S n))
|
||||
,(add1 (term (trans-n n)))])
|
||||
|
||||
(define-extended-language vl
|
||||
bl
|
||||
(sl (ν sl) •)
|
||||
(s sl invalid)
|
||||
(ν uninit imm box imm-nc box-nc not)
|
||||
(γ ((n ν) γ) •)
|
||||
(η (n η) •)
|
||||
(f (n n sl) ∅)
|
||||
(m n ?))
|
||||
|
||||
|
||||
(define (check-V-res v-res)
|
||||
;(displayln (list 'check-V-res v-res))
|
||||
(match v-res
|
||||
[`(V ,e ,s1 ,n ,b ,γ1 ,η1 ,f ,s2 ,γ2 ,η2)
|
||||
(unless
|
||||
(equal?
|
||||
(term
|
||||
(verify
|
||||
(trans-e ,e)
|
||||
(trans-s ,s1)
|
||||
(trans-n ,n)
|
||||
,b
|
||||
(trans-γ ,γ1)
|
||||
(trans-η ,η1)
|
||||
(trans-f ,f)))
|
||||
(term
|
||||
((trans-s ,s2)
|
||||
(trans-γ ,γ2)
|
||||
(trans-η ,η2))))
|
||||
(error 'check-V-res "failed on ~s " e))]))
|
||||
|
||||
(define (check-Vs n #:generator [g #f])
|
||||
(define gen (redex-generator vl
|
||||
(V e • O #f • • ∅ s_1 γ_1 η_1)
|
||||
6))
|
||||
(for ([_ (in-range n)])
|
||||
(define maybe-V
|
||||
(if g
|
||||
(gen)
|
||||
(generate-term
|
||||
vl
|
||||
#:satisfying
|
||||
;(V e s n b γ η f s_1 γ_1 η_1)
|
||||
(V e • O #f • • ∅ s_1 γ_1 η_1)
|
||||
5)))
|
||||
(match maybe-V
|
||||
[#f
|
||||
(display ".")]
|
||||
[`(V ,e ,s ,n ,b ,γ ,η ,f ,s_1 ,γ_1 ,η_1)
|
||||
(displayln (term (trans-e ,e)))
|
||||
(check-V-res maybe-V)])))
|
||||
|
||||
(define-metafunction vl
|
||||
[(trans-γ ((n ν) γ))
|
||||
(((trans-n n) ν) any ...)
|
||||
(where (any ...) (trans-γ γ))]
|
||||
[(trans-γ •)
|
||||
()])
|
||||
|
||||
(define-metafunction vl
|
||||
[(trans-η (n η))
|
||||
((trans-n n) any ...)
|
||||
(where (any ...) (trans-η η))]
|
||||
[(trans-η •)
|
||||
()])
|
||||
|
||||
(define-metafunction vl
|
||||
[(trans-f ∅)
|
||||
∅]
|
||||
[(trans-f (n_1 n_2 sl))
|
||||
((trans-n n_1) (trans-n n_2) (cns->lst sl))])
|
||||
|
||||
(define-metafunction vl
|
||||
[(trans-s invalid)
|
||||
invalid]
|
||||
[(trans-s sl)
|
||||
(cns->lst sl)])
|
||||
|
||||
(define-metafunction vl
|
||||
[(cns->lst (any_1 any_2))
|
||||
(any_1 any_3 ...)
|
||||
(where (any_3 ...) (cns->lst any_2))]
|
||||
[(cns->lst •)
|
||||
()])
|
||||
|
||||
|
||||
;; verification judgment -----------------------------------------------
|
||||
|
||||
|
||||
(define-judgment-form vl
|
||||
#:mode (V I I I I I I I O O O)
|
||||
#:contract (V e s n b γ η f s γ η)
|
||||
|
||||
;localrefs
|
||||
[(V (loc n) s n_l #f γ η f s γ η)
|
||||
(lmem (sref n s) (imm (imm-nc •)))]
|
||||
[(V (loc n) s n_l #t γ η f s γ η)
|
||||
(lmem (sref n s) (imm (imm-nc (box (box-nc •)))))]
|
||||
[(V (loc-box n) s n_l b γ η f s γ η)
|
||||
(lmem (sref n s) (box (box-nc •)))]
|
||||
|
||||
[(V (loc-noclr n) s n_l #f γ η f (supdt n (nc ν_n) s) γ η_l)
|
||||
(where ν_n (sref n s))
|
||||
(log-noclr n n_l ν_n η η_l)
|
||||
(lmem ν_n (imm (imm-nc •)))]
|
||||
[(V (loc-noclr n) s n_l #t γ η f (supdt n (nc ν_n) s) γ η_l)
|
||||
(where ν_n (sref n s))
|
||||
(log-noclr n n_l ν_n η η_l)
|
||||
(lmem ν_n (imm (imm-nc (box (box-nc •)))))]
|
||||
[(V (loc-box-noclr n) s n_l b γ η f (supdt n box-nc s) γ η_l)
|
||||
(where ν_n (sref n s))
|
||||
(log-noclr n n_l ν_n η η_l)
|
||||
(lmem ν_n (box (box-nc •)))]
|
||||
|
||||
|
||||
[(V (loc-clr n) s n_l #f γ η f (supdt n not s) γ_l η)
|
||||
(where imm (sref n s))
|
||||
(log-clr n s n_l γ γ_l)]
|
||||
[(V (loc-clr n) s n_l #t γ η f (supdt n not s) γ_l η)
|
||||
(lmem (sref n s) (imm (box •)))
|
||||
(log-clr n s n_l γ γ_l)]
|
||||
[(V (loc-box-clr n) s n_l b γ η f (supdt n not s) γ_l η)
|
||||
(where box (sref n s))
|
||||
(log-clr n s n_l γ γ_l)]
|
||||
|
||||
;branch
|
||||
[(V (branch e_c e_t e_e) s n_l b γ η f s_n (concat γ_2 γ_3) η_3)
|
||||
(V e_c s n_l #f γ η ∅ s_1 γ_1 η_1)
|
||||
(V e_t (trim s_1 s) O b • • f s_2 γ_2 η_2)
|
||||
(undo-clrs γ_2 (trim s_2 s) s_21)
|
||||
(undo-noclrs η_2 s_21 s_22)
|
||||
(V e_e s_22 O b γ_1 η_1 f s_3 γ_3 η_3)
|
||||
(redo-clrs γ_2 (trim s_3 s) s_n)]
|
||||
|
||||
;let-one
|
||||
[(V (let-one e_r e_b) sl n_l b γ η f s_2 γ_2 η_2)
|
||||
(where sl_0 (uninit sl))
|
||||
(V e_r sl_0 (n+ n_l (S O)) #f γ η ∅ sl_1 γ_1 η_1)
|
||||
(where (uninit sl_1*) (trim sl_1 sl_0))
|
||||
(V e_b (imm sl_1*) (n+ n_l (S O)) b γ_1 η_1 (shift (S O) f) s_2 γ_2 η_2)]
|
||||
|
||||
;seq
|
||||
[(V (seq e_0 e_1) s n_l b γ η f s_2 γ_2 η_2)
|
||||
(V e_0 s n_l #t γ η ∅ s_1 γ_1 η_1)
|
||||
(V e_1 (trim s_1 s) n_l b γ_1 η_1 f s_2 γ_2 η_2)]
|
||||
|
||||
;application
|
||||
[(V (application (loc-noclr n) el) s n_l b_i γ η (n_f n_s sl_f) s_2 γ_2 η_2)
|
||||
(n= n (n+ n_f (len el)))
|
||||
(V-self-app (application (loc-noclr n) el) s n_l γ η (n_f n_s sl_f) s_2 γ_2 η_2)]
|
||||
[(V (application (lam τl nl e) el) s n_l b γ η f s_2 γ_2 η_2)
|
||||
(where n (len el))
|
||||
(where n_l* (n+ n n_l))
|
||||
(where s_1 (abs-push n not s))
|
||||
(V*-ref el τl s_1 n_l* γ η s_2 γ_2 η_2)
|
||||
(lam-verified? (lam τl nl e) s_1 ?)]
|
||||
[(V (application (proc-const τl e) el) s n_l b γ η f s_2 γ_2 η_2)
|
||||
(V (application (lam τl • e) el) s n_l b γ η f s_2 γ_2 η_2)]
|
||||
[(V (application e_0 el) s n_l b γ η f s_2 γ_2 η_2)
|
||||
;; the only place where cases might overlap, so exclude that explicitly
|
||||
(not-self-app (application e_0 el) s f)
|
||||
(where n (len el))
|
||||
(where n_l* (n+ n n_l))
|
||||
(V* (e_0 el) (abs-push n not s) n_l* #f γ η s_2 γ_2 η_2)]
|
||||
|
||||
; literals
|
||||
[(V n s n_l b γ η f s γ η)]
|
||||
[(V b s n_l b_i γ η f s γ η)]
|
||||
[(V (quote variable) s n_l b γ η f s γ η)]
|
||||
[(V void s n_l b γ η f s γ η)]
|
||||
|
||||
; install-value
|
||||
[(V (install-value n e_r e_b) s n_l b γ η f s_3 γ_3 η_3)
|
||||
(n< n n_l)
|
||||
(V e_r s n_l #f γ η ∅ s_1 γ_1 η_1)
|
||||
(where s_2 (trim s_1 s))
|
||||
(where uninit (sref n s_2))
|
||||
(V e_b (supdt n imm s_2) n_l b γ η f s_3 γ_3 η_3)]
|
||||
[(V (install-value-box n e_r e_b) s n_l b γ η f s_3 γ_3 η_3)
|
||||
(n< n (len s))
|
||||
(V e_r s n_l #f γ η ∅ s_1 γ_1 η_1)
|
||||
(where s_2 (trim s_1 s))
|
||||
(lmem (sref n s_2) (box (box-nc •)))
|
||||
(V e_b s_2 n_l b γ_1 η_1 f s_3 γ_3 η_3)]
|
||||
|
||||
; boxenv
|
||||
[(V (boxenv n_p e) s n_l b γ η f s_2 γ_2 η_2)
|
||||
(where imm (sref n_p s))
|
||||
(V e (supdt n_p box s) n_l b γ η f s_2 γ_2 η_2)
|
||||
(n< n_p n_l)]
|
||||
|
||||
; indirect
|
||||
[(V (indirect x) s n_l b γ η f s γ η)]
|
||||
|
||||
; let-void
|
||||
[(V (let-void n e) s n_l b_i γ η f s_1 γ_1 η_1)
|
||||
(V e (abs-push n uninit s) (n+ n n_l) b_i γ η (shift n f) s_1 γ_1 η_1)]
|
||||
[(V (let-void-box n e) s n_l b_i γ η f s_1 γ_1 η_1)
|
||||
(V e (abs-push n box s) (n+ n n_l) b_i γ η (shift n f) s_1 γ_1 η_1)]
|
||||
|
||||
; procedures in arbitrary context
|
||||
[(V (lam τl nl e) s n_l b γ η f s γ η)
|
||||
(vals (val τl))
|
||||
(lam-verified? (lam τl nl e) s ?)]
|
||||
[(V (proc-const τl e) s n_l b γ η f s_1 γ_1 η_1)
|
||||
(vals τl)
|
||||
(V (lam τl • e) s n_l b γ η f s_1 γ_1 η_1)]
|
||||
|
||||
; case-lam
|
||||
[(V (case-lam el) s n_l b γ η f s γ η)
|
||||
(lam-verified?* el s ?)]
|
||||
|
||||
; let-rec
|
||||
[(V (let-rec ll e) s n_l b γ η f s_2 γ_2 η_2)
|
||||
(where n (len ll))
|
||||
(n<= n n_l)
|
||||
(lsplit n s s_a s_b)
|
||||
(uninits s_a)
|
||||
(where s_1 (abs-push n imm s_b))
|
||||
(verify-ll O s_1 ll)
|
||||
(V e s_1 n_l b γ η f s_2 γ_2 η_2)])
|
||||
|
||||
(define-judgment-form vl
|
||||
#:mode (verify-ll I I I)
|
||||
[(verify-ll n s •)]
|
||||
[(verify-ll n s ((lam τl (n_l nl) e) ll))
|
||||
(vals τl)
|
||||
(lam-verified? (lam τl (n_l nl) e) s n)
|
||||
(verify-ll (S n) s ll)])
|
||||
|
||||
(define-judgment-form vl
|
||||
#:mode (V* I I I I I I O O O)
|
||||
#:contract (V* el s n b γ η s γ η)
|
||||
[(V* • s n_l b γ η s γ η)]
|
||||
[(V* (e_0 el) s n_l b γ η s_2 γ_2 η_2)
|
||||
(V e_0 s n_l b γ η ∅ s_1 γ_1 η_1)
|
||||
(V* el (trim s_1 s) n_l b γ_1 η_1 s_2 γ_2 η_2)])
|
||||
|
||||
(define-judgment-form vl
|
||||
#:mode (V-self-app I I I I I I O O O)
|
||||
#:contract (V-self-app e s n γ η f s γ η)
|
||||
[(V-self-app (application e_0 el) sl n_l γ η (n_f n_s sl_f) sl_1 γ_1 η_1)
|
||||
(where n (len el))
|
||||
(where n_l* (n+ n n_l))
|
||||
(V* (e_0 el) (abs-push n not sl) n_l* #f γ η sl_1 γ_1 η_1)
|
||||
(closure-intact (ssblst n_s (slen sl_f) sl_1) sl_f)])
|
||||
|
||||
(define-judgment-form vl
|
||||
#:mode (V*-ref I I I I I I O O O)
|
||||
[(V*-ref • • s n_l γ η s γ η)]
|
||||
[(V*-ref (e_0 el) (val τl) s n_l γ η s_2 γ_2 η_2)
|
||||
(V e_0 s n_l #f γ η ∅ s_1 γ_1 η_1)
|
||||
(V*-ref el τl (trim s_1 s) n_l γ_1 η_1 s_2 γ_2 η_2)]
|
||||
[(V*-ref (e_0 el) • s n_l γ η s_2 γ_2 η_2)
|
||||
(V* (e_0 el) s n_l #f γ η s_2 γ_2 η_2)]
|
||||
[(V*-ref • (τ_0 τl) s n_l γ η s γ η)]
|
||||
[(V*-ref ((loc n) el) (ref τl) s n_l γ η s_2 γ_2 η_2)
|
||||
; Require the reference to load a box.
|
||||
(V (loc-box n) s n_l #f γ η ∅ s_1 γ_1 η_1)
|
||||
(V*-ref el τl s_1 n_l γ_1 η_1 s_2 γ_2 η_2)]
|
||||
[(V*-ref ((loc-noclr n) el) (ref τl) s n_l γ η s_2 γ_2 η_2)
|
||||
; Require the reference to load a box.
|
||||
(V (loc-box-noclr n) s n_l #f γ η ∅ s_1 γ_1 η_1)
|
||||
(V*-ref el τl s_1 n_l γ_1 η_1 s_2 γ_2 η_2)]
|
||||
[(V*-ref ((loc-clr n) el) (ref τl) s n_l γ η s_2 γ_2 η_2)
|
||||
; Require the reference to load a box.
|
||||
(V (loc-box-clr n) s n_l #f γ η ∅ s_1 γ_1 η_1)
|
||||
(V*-ref el τl s_1 n_l γ_1 η_1 s_2 γ_2 η_2)])
|
||||
|
||||
(define-relation vl
|
||||
[(closure-intact • •)]
|
||||
[(closure-intact (imm-nc sl_1) (imm sl_2))
|
||||
(closure-intact sl_1 sl_2)]
|
||||
[(closure-intact (box-nc sl_1) (box sl_2))
|
||||
(closure-intact sl_1 sl_2)]
|
||||
[(closure-intact (ν sl_1) (ν sl_2))
|
||||
(closure-intact sl_1 sl_2)])
|
||||
|
||||
(define-relation vl
|
||||
[(vals (val τl))
|
||||
(vals τl)]
|
||||
[(vals •)])
|
||||
|
||||
(define-relation vl
|
||||
[(uninits (uninit sl))
|
||||
(uninits sl)]
|
||||
[(uninits •)])
|
||||
|
||||
(define-judgment-form vl
|
||||
#:mode (lam-verified? I I I)
|
||||
[(lam-verified? (lam τl nl e) sl m)
|
||||
;(where n_d (len sl))
|
||||
;(lmax nl n_m)
|
||||
;(n< n_m n_d)
|
||||
(where n_d* (n+ (len nl) (len τl)))
|
||||
(where sl_0 (collate-refs nl sl))
|
||||
(not-lmem uninit sl_0)
|
||||
(not-lmem not sl_0)
|
||||
(where s_d (drop-noclrs sl_0))
|
||||
(extract-self m nl τl s_d f)
|
||||
(V e (concat s_d (arg τl)) n_d* #f • • f sl_1 γ_1 η_1)])
|
||||
|
||||
(define-judgment-form vl
|
||||
#:mode (lam-verified?* I I I)
|
||||
[(lam-verified?* • sl m)]
|
||||
[(lam-verified?* ((lam τl nl e) el) sl m)
|
||||
(vals τl)
|
||||
(lam-verified? (lam τl nl e) sl m)
|
||||
(lam-verified?* el sl m)])
|
||||
|
||||
;; suffers from ?/n confusion
|
||||
;; fixable by transforming to a metafunction
|
||||
;; but need to add judgment-holds support
|
||||
|
||||
(define-judgment-form vl
|
||||
#:mode (extract-self I I I I O)
|
||||
[(extract-self ? nl τl sl ∅)]
|
||||
[(extract-self n nl τl sl ∅)
|
||||
(not-lmem n nl)]
|
||||
[(extract-self n_i (n_i nl) τl sl (O (len τl) sl))
|
||||
(not-lmem n_i nl)]
|
||||
[(extract-self n_i (n_0 nl) τl sl ((S n_n) n_τ sl))
|
||||
(extract-self n_i nl τl sl (n_n n_τ sl))
|
||||
(nlmem n_i nl)])
|
||||
|
||||
(define-metafunction vl
|
||||
[(loc-noclr? (loc-noclr e))
|
||||
#t]
|
||||
[(loc-noclr? e)
|
||||
#f])
|
||||
|
||||
(define-relation vl
|
||||
[(not-self-app (application e el) s ∅)]
|
||||
[(not-self-app (application e el) s f)
|
||||
(where #f (loc-noclr? e))]
|
||||
[(not-self-app (application (loc-noclr n) el) s (n_f n_s s_f))
|
||||
(n≠ n (n+ n_f (len el)))])
|
||||
|
||||
(define-relation vl
|
||||
[(n≠ O (S n))]
|
||||
[(n≠ (S n) O)]
|
||||
[(n≠ (S n_1) (S n_2))
|
||||
(n≠ n_1 n_2)])
|
||||
|
||||
#;
|
||||
(define-metafunction vl
|
||||
[(es ? nl τl sl)
|
||||
∅]
|
||||
[(extract-self n nl τl sl)
|
||||
∅
|
||||
(judgment-holds (not-lmem n nl))]
|
||||
[(extract-self n_i (n_i nl) (τ_0 τl) sl (O O sl))
|
||||
(not-lmem n_i nl)]
|
||||
[(extract-self n_i (n_0 nl) (τ_0 τl) sl ((S n_n) (S n_τ) sl))
|
||||
(extract-self n_i nl τl sl (n_n n_τ sl))
|
||||
(nlmem n_i nl)])
|
||||
|
||||
(define-metafunction vl
|
||||
[(ssblst O O sl)
|
||||
•]
|
||||
[(ssblst O (S n) (ν sl))
|
||||
(ν (ssblst O n sl))]
|
||||
[(ssblst (S n_1) n_2 (ν sl))
|
||||
(ssblst n_1 n_2 sl)])
|
||||
|
||||
(define-relation vl
|
||||
[(lmem ν (ν sl))]
|
||||
[(lmem ν (ν_1 sl))
|
||||
(lmem ν sl)])
|
||||
|
||||
(define-relation vl
|
||||
[(nlmem n (n nl))]
|
||||
[(nlmem n (n_1 nl))
|
||||
(nlmem n nl)])
|
||||
|
||||
(define-relation vl
|
||||
[(not-lmem any_1 (any_2 any_3))
|
||||
(not-lmem any_1 any_3)
|
||||
(where (any_!_4 any_!_4) (any_1 any_2))]
|
||||
[(not-lmem any_1 •)])
|
||||
|
||||
(define-judgment-form vl
|
||||
#:mode (lmax I O)
|
||||
[(lmax • O)]
|
||||
[(lmax (n nl) n)
|
||||
(lmax nl n_m)
|
||||
(n< n_m n)]
|
||||
[(lmax (n nl) n_m)
|
||||
(lmax nl n_m)
|
||||
(n< n n_m)])
|
||||
|
||||
(define-metafunction vl
|
||||
[(sref O (ν sl))
|
||||
ν]
|
||||
[(sref (S n) (ν_1 sl))
|
||||
(sref n sl)]
|
||||
[(sref n •)
|
||||
#f])
|
||||
|
||||
(define-metafunction vl
|
||||
#;[(supdt O ν_1 •)
|
||||
(ν_1 •)]
|
||||
[(supdt O ν_1 (ν_2 sl))
|
||||
(ν_1 sl)]
|
||||
[(supdt (S n) ν_1 (ν_2 sl))
|
||||
(ν_2 (supdt n ν_1 sl))])
|
||||
|
||||
(define-metafunction vl
|
||||
[(n- n_1 O)
|
||||
n_1]
|
||||
[(n- (S n_1) (S n_2))
|
||||
(n- n_1 n_2)]
|
||||
#;
|
||||
[(n- O (S n))
|
||||
#f])
|
||||
|
||||
(define-metafunction vl
|
||||
[(n+ O n)
|
||||
n]
|
||||
[(n+ (S n_1) n_2)
|
||||
(n+ n_1 (S n_2))])
|
||||
|
||||
(define-metafunction vl
|
||||
[(slen •)
|
||||
O]
|
||||
[(slen (ν sl))
|
||||
(S (slen sl))])
|
||||
|
||||
(define-metafunction vl
|
||||
[(len •)
|
||||
O]
|
||||
[(len (any_1 any_2))
|
||||
(S (len any_2))])
|
||||
|
||||
(define-relation vl
|
||||
[(n< O (S n))]
|
||||
[(n< (S n_1) (S n_2))
|
||||
(n< n_1 n_2)])
|
||||
|
||||
(define-relation vl
|
||||
[(n<= O n)]
|
||||
[(n<= (S n_1) (S n_2))
|
||||
(n<= n_1 n_2)])
|
||||
|
||||
(define-relation vl
|
||||
[(n= O O)]
|
||||
[(n= (S n_1) (S n_2))
|
||||
(n= n_1 n_2)])
|
||||
|
||||
(define-judgment-form vl
|
||||
#:mode (lsplit I I O O)
|
||||
[(lsplit O any_1 • any_1)]
|
||||
[(lsplit (S n) (any_1 any_2) (any_1 any_3) any_4)
|
||||
(lsplit n any_2 any_3 any_4)])
|
||||
|
||||
|
||||
(define-metafunction vl
|
||||
shift : n f -> f
|
||||
[(shift n ∅) ∅]
|
||||
[(shift n (n_f n_s sl))
|
||||
((n+ n n_f) (n+ n n_s) sl)])
|
||||
|
||||
(define-metafunction vl
|
||||
abs-push : n ν sl -> sl
|
||||
[(abs-push O ν sl) sl]
|
||||
[(abs-push (S n) ν sl)
|
||||
(abs-push n ν (ν sl))])
|
||||
|
||||
;; note: could turn this back into a metafunction
|
||||
;; if the restriction on relations in term positions
|
||||
;; is removed....
|
||||
;; or support judgment-holds, maybe that is better
|
||||
;; naturally a metafunction in any case...
|
||||
(define-judgment-form vl
|
||||
#:contract (log-noclr n n ν η η)
|
||||
#:mode (log-noclr I I I I O)
|
||||
[(log-noclr n_p n_l ν_p η ((n- n_p n_l) η))
|
||||
(n<= n_l n_p)
|
||||
(lmem ν_p (imm (box •)))]
|
||||
[(log-noclr n_p n_l ν_p η η)
|
||||
(lmem ν_p (imm-nc (box-nc (uninit (not •)))))]
|
||||
[(log-noclr n_p n_l ν_p η η)
|
||||
(n< n_p n_l)])
|
||||
|
||||
|
||||
(define-metafunction vl
|
||||
nc : ν -> ν
|
||||
[(nc imm) imm-nc]
|
||||
[(nc imm-nc) imm-nc]
|
||||
[(nc box) box-nc]
|
||||
[(nc box-nc) box-nc])
|
||||
|
||||
(define-judgment-form vl
|
||||
#:contract (log-clr n s n γ γ)
|
||||
#:mode (log-clr I I I I O)
|
||||
[(log-clr n_p s n_l γ (((n- (n- (slen s) n_p) (S O)) ν_np) γ))
|
||||
(where ν_np (sref n_p s))
|
||||
(n<= n_l n_p)]
|
||||
[(log-clr n_p s n_l γ γ)
|
||||
(n< n_p n_l)])
|
||||
|
||||
;; need more specific nt types in
|
||||
;; relations like this or there can be problems
|
||||
;; satisfying constraings (i.e. trying to satisfy an sl with anys)
|
||||
(define-metafunction vl
|
||||
[(concat • any_1)
|
||||
any_1]
|
||||
[(concat (any_1 any_2) any_3)
|
||||
(any_1 (concat any_2 any_3))])
|
||||
|
||||
|
||||
(define-judgment-form vl
|
||||
#:mode (undo-clrs I I O)
|
||||
[(undo-clrs γ invalid invalid)]
|
||||
[(undo-clrs • s s)]
|
||||
[(undo-clrs ((n ν) γ) s (supdt (n- (n- (slen s) n) (S O)) ν s_2))
|
||||
(n< n (slen s))
|
||||
(n≠ (n- (slen s) n) O)
|
||||
(undo-clrs γ s s_2)]
|
||||
[(undo-clrs ((n ν) γ) s s)
|
||||
(n<= (slen s) n)])
|
||||
|
||||
(define-judgment-form vl
|
||||
#:mode (undo-noclrs I I O)
|
||||
[(undo-noclrs η invalid invalid)]
|
||||
[(undo-noclrs • s s)]
|
||||
[(undo-noclrs (n η) s (supdt n imm s_2))
|
||||
(where imm-nc (sref n s))
|
||||
(undo-noclrs η s s_2)]
|
||||
[(undo-noclrs (n η) s (supdt n box s_2))
|
||||
(where box-nc (sref n s))
|
||||
(undo-noclrs η s s_2)]
|
||||
[(undo-noclrs (n η) s s_2)
|
||||
(undo-noclrs η s s_2)
|
||||
;; Bug 1
|
||||
;; (lmem (sref n s) (uninit (imm (imm-nc (boc-nc (box (not •)))))))
|
||||
(lmem (sref n s) (uninit (imm (box (not •)))))])
|
||||
|
||||
(define-judgment-form vl
|
||||
#:mode (redo-clrs I I O)
|
||||
[(redo-clrs γ invalid invalid)]
|
||||
[(redo-clrs • s s)]
|
||||
[(redo-clrs ((n ν) γ) s (supdt (n- (n- (slen s) n) (S O)) not s_2))
|
||||
(n< n (slen s))
|
||||
(n≠ (n- (slen s) n) O)
|
||||
(redo-clrs γ s s_2)]
|
||||
[(redo-clrs ((n ν) γ) s s)
|
||||
(n<= (slen s) n)])
|
||||
|
||||
(define-metafunction vl
|
||||
[(collate-refs • sl)
|
||||
•]
|
||||
[(collate-refs (n nl) sl)
|
||||
((sref n sl) (collate-refs nl sl))])
|
||||
|
||||
(define-metafunction vl
|
||||
[(drop-noclrs (imm-nc sl))
|
||||
(imm (drop-noclrs sl))]
|
||||
[(drop-noclrs (box-nc sl))
|
||||
(box sl)]
|
||||
[(drop-noclrs (ν sl))
|
||||
(ν (drop-noclrs sl))]
|
||||
[(drop-noclrs •)
|
||||
•])
|
||||
|
||||
;; had to make both of these
|
||||
;; j-forms for the below reasons...
|
||||
#;
|
||||
(define-metafunction vl
|
||||
undo-clrs : γ s -> s
|
||||
[(undo-clrs γ invalid) invalid]
|
||||
[(undo-clrs • s) s]
|
||||
[(undo-clrs ((n ν) γ) s)
|
||||
(undo-clrs γ (supdt (n- (n- (slen s) n) (S O)) ν s))]
|
||||
;; --> (slen s) < n
|
||||
;; but generation doesn't support this fall-through!!
|
||||
[(undo-clrs ((n ν) γ) s)
|
||||
(undo-clrs γ s)])
|
||||
#;
|
||||
(define-metafunction vl
|
||||
redo-clrs : γ s -> s
|
||||
[(redo-clrs γ invalid) invalid]
|
||||
[(redo-clrs • s) s]
|
||||
[(redo-clrs ((n ν) γ) s)
|
||||
(redo-clrs γ (supdt (n- (n- (slen s) n) (S O)) not s))]
|
||||
;; --> (slen s) < n
|
||||
;; but generation doesn't support this fall-through!!
|
||||
[(redo-clrs ((n ν) γ) s)
|
||||
(redo-clrs γ s)])
|
||||
|
||||
(define-metafunction vl
|
||||
trim : s s -> s
|
||||
[(trim invalid s) invalid]
|
||||
[(trim s_1 s_2)
|
||||
(sdrp (n- (slen s_1) (slen s_2)) s_1)])
|
||||
|
||||
(define-metafunction vl
|
||||
[(sdrp O sl)
|
||||
sl]
|
||||
[(sdrp (S n) (ν sl))
|
||||
(sdrp n sl)]
|
||||
[(sdrp n •)
|
||||
•])
|
||||
|
||||
(define-metafunction vl
|
||||
[(valid? invalid) #f]
|
||||
[(valid? sl) #t])
|
||||
|
||||
(define-metafunction vl
|
||||
[(arg •)
|
||||
•]
|
||||
[(arg (val τl))
|
||||
(imm (arg τl))]
|
||||
[(arg (ref τl))
|
||||
(box (arg τl))])
|
||||
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
|
@ -3,7 +3,8 @@
|
|||
(require (lib "redex/examples/stlc+lists.rkt")
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
redex/reduction-semantics
|
||||
racket/bool)
|
||||
racket/bool
|
||||
racket/match)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
|
@ -32,6 +33,15 @@
|
|||
(define (generate [index 0])
|
||||
(generate-term stlc M #:i-th index)))
|
||||
|
||||
(module+ typed-mod
|
||||
(provide generate get-generator type)
|
||||
(define type 'search)
|
||||
(define (get-generator) generate)
|
||||
(define (generate)
|
||||
((match-lambda [`(typeof • ,M ,τ) M]
|
||||
[#f #f])
|
||||
(generate-term stlc #:satisfying (typeof • M τ) 5))))
|
||||
|
||||
(module+ check-mod
|
||||
(provide check)
|
||||
(define (check term)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,14 @@
|
|||
#lang racket/base
|
||||
|
||||
(require racket/runtime-path
|
||||
"../util/info-util.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
(define name "stlc")
|
||||
(define fname (make-path-root 'stlc+lists))
|
||||
|
||||
(define-runtime-path here ".")
|
||||
|
||||
(define (all-mods)
|
||||
(all-mods/type 'typed here name fname))
|
||||
|
|
@ -3,7 +3,8 @@
|
|||
(require redex/examples/stlc+lists+subst
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
redex/reduction-semantics
|
||||
racket/bool)
|
||||
racket/bool
|
||||
racket/match)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
|
@ -32,6 +33,15 @@
|
|||
(define (generate [index 0])
|
||||
(generate-term stlc M #:i-th index)))
|
||||
|
||||
(module+ typed-mod
|
||||
(provide generate get-generator type)
|
||||
(define type 'search)
|
||||
(define (get-generator) generate)
|
||||
(define (generate)
|
||||
((match-lambda [`(typeof • ,M ,τ) M]
|
||||
[#f #f])
|
||||
(generate-term stlc #:satisfying (typeof • M τ) 5))))
|
||||
|
||||
(module+ check-mod
|
||||
(provide check)
|
||||
(define (check term)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,14 @@
|
|||
#lang racket/base
|
||||
|
||||
(require racket/runtime-path
|
||||
"../util/info-util.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
(define name "stlc-sub")
|
||||
(define fname (make-path-root 'stlc-subst))
|
||||
|
||||
(define-runtime-path here ".")
|
||||
|
||||
(define (all-mods)
|
||||
(all-mods/type 'typed here name fname))
|
||||
|
|
@ -0,0 +1,25 @@
|
|||
#lang racket/base
|
||||
|
||||
(require racket/runtime-path
|
||||
racket/list
|
||||
racket/path)
|
||||
|
||||
(provide all-mods)
|
||||
|
||||
(define-runtime-path here ".")
|
||||
|
||||
(define (all-info-files)
|
||||
(for/list ([f (in-directory here)]
|
||||
#:when (and (file-exists? f)
|
||||
(regexp-match #rx"^.*typed-info\\.rkt$"
|
||||
(path->string f)))
|
||||
#:unless (regexp-match #rx".*all-info.*"
|
||||
(path->string f)))
|
||||
(path->string
|
||||
(find-relative-path (simplify-path (current-directory))
|
||||
(simplify-path f)))))
|
||||
|
||||
(define (all-mods)
|
||||
(append-map (λ (f)
|
||||
((dynamic-require f 'all-mods)))
|
||||
(all-info-files)))
|
||||
|
|
@ -5,7 +5,8 @@
|
|||
racket/runtime-path)
|
||||
|
||||
(provide make-all-mods
|
||||
make-path-root)
|
||||
make-path-root
|
||||
all-mods/type)
|
||||
|
||||
(define-runtime-path here ".")
|
||||
|
||||
|
|
@ -14,7 +15,8 @@
|
|||
(define type->genmod
|
||||
(hash 'grammar 'adhoc-mod
|
||||
'enum 'enum-mod
|
||||
'ordered 'ordered-mod))
|
||||
'ordered 'ordered-mod
|
||||
'typed 'typed-mod))
|
||||
|
||||
(define (get-name/modpaths filename type path-root)
|
||||
(define model-name (first (regexp-split #rx"\\." (last (regexp-split #rx"/" filename)))))
|
||||
|
|
|
|||
|
|
@ -2204,7 +2204,7 @@ with @racket[#:satisfying].}
|
|||
|
||||
Toggles whether or not redex will dynamically adjust the
|
||||
chance that more recursive clauses of judgment forms or metafunctions
|
||||
are chosen earlierwhen attempting to generate terms
|
||||
are chosen earlier when attempting to generate terms
|
||||
with forms that use @racket[#:satisfying]. It is @racket[#t] by
|
||||
default, which causes redex to favor more recursive clauses at
|
||||
lower depths and less recursive clauses at depths closer to the
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user