adjust generate-term so that it has an '=' in its concrete
syntax when generating something from a metafunction export redex-generator (and add docs) rename generate-types.rkt to typing-rules-no-ellipses.rkt
This commit is contained in:
Robby Findler
parent
478fedeeb7
commit
3d5178bcb0
|
|
@ -8,9 +8,8 @@
|
|||
;; This file makes some small changes to the system in
|
||||
;; typing-rules.rkt (in the same directory) to allow generation
|
||||
;; of terms that satisfy the "typeof" judgment-form. Specifically,
|
||||
;; since this kind of random generation doesn't yet support ellipses,
|
||||
;; they have to be eliminated form the judgment-form and the
|
||||
;; metafunctions it depends on.
|
||||
;; since generation doesn't yet support ellipses, they have to be
|
||||
;; eliminated from the judgment-form and the metafunctions it depends on.
|
||||
|
||||
(define-language STLC
|
||||
(e (λ (x τ) e)
|
||||
|
|
@ -77,12 +76,20 @@
|
|||
(typeof () e τ)
|
||||
5))
|
||||
|
||||
(define (random-terms n)
|
||||
(define (random-typed-terms n)
|
||||
(define gen-one (redex-generator STLC (typeof () e τ) 5))
|
||||
(for/list ([_ n])
|
||||
(match (random-typed-term)
|
||||
[`(typeof () ,e ,t)
|
||||
(define types (judgment-holds (typeof () ,e τ) τ))
|
||||
(unless (= 1 (length types))
|
||||
(error 'typeof "non-unique types: ~s in ~s\n" types e))
|
||||
(test-equal (car types) t)
|
||||
e])))
|
||||
(extract-term-from-derivation
|
||||
(gen-one))))
|
||||
|
||||
(define (extract-term-from-derivation t)
|
||||
(match t
|
||||
[`(typeof () ,e ,t)
|
||||
;; test to make sure the generator
|
||||
;; generated something that the
|
||||
;; judgment form actually accepts
|
||||
(define types (judgment-holds (typeof () ,e τ) τ))
|
||||
(unless (= 1 (length types))
|
||||
(error 'typeof "non-unique types: ~s in ~s\n" types e))
|
||||
(test-equal (car types) t)
|
||||
e]))
|
||||
|
|
@ -341,12 +341,19 @@
|
|||
(let ([body-code
|
||||
(λ (res size)
|
||||
#`(generate-mf-pat language (jf/mf-id . args) #,res #,size))])
|
||||
(syntax-case #'rest ()
|
||||
[(res)
|
||||
(syntax-case #'rest (=)
|
||||
[(= res)
|
||||
#`(λ (size)
|
||||
#,(body-code #'size))]
|
||||
[(res size)
|
||||
#,(body-code #'res #'size))]
|
||||
[(= res size)
|
||||
(body-code #'res #'size)]
|
||||
[(x . y)
|
||||
(or (not (identifier? #'x))
|
||||
(not (free-identifier=? #'= #'x)))
|
||||
(raise-syntax-error 'generate-term
|
||||
"expected to find ="
|
||||
stx
|
||||
#'x)]
|
||||
[whatever
|
||||
(signal-error #'whatever)]))))]
|
||||
[(judgment-form-id? #'jf/mf-id)
|
||||
|
|
|
|||
|
|
@ -413,7 +413,7 @@
|
|||
; Introduce the names before using them, to allow
|
||||
; judgment form definition at the top-level.
|
||||
#`(begin
|
||||
(define-syntaxes (judgment-form-runtime-proc judgment-form-lws) (values))
|
||||
(define-syntaxes (judgment-form-runtime-proc judgment-form-lws judgment-runtime-gen-clauses) (values))
|
||||
#,definitions)
|
||||
definitions))
|
||||
'disappeared-use
|
||||
|
|
|
|||
|
|
@ -64,6 +64,7 @@
|
|||
generate-term
|
||||
check-metafunction
|
||||
check-reduction-relation
|
||||
redex-generator
|
||||
exn:fail:redex:generation-failure?
|
||||
(struct-out exn:fail:redex:test)
|
||||
(struct-out counterexample))
|
||||
|
|
|
|||
|
|
@ -1641,7 +1641,7 @@ metafunctions or unnamed reduction-relation cases) to application counts.}
|
|||
(generate-term term-spec)]
|
||||
([term-spec (code:line language @#,ttpattern)
|
||||
(code:line language #:satisfying (judgment-form-id @#,ttpattern ...))
|
||||
(code:line language #:satisfying (metafunction-id @#,ttpattern ...) @#,ttpattern)
|
||||
(code:line language #:satisfying (metafunction-id @#,ttpattern ...) = @#,ttpattern)
|
||||
(code:line #:source metafunction)
|
||||
(code:line #:source relation-expr)]
|
||||
[kw-args (code:line #:attempt-num attempts-expr)
|
||||
|
|
@ -1824,6 +1824,27 @@ term that does not match @racket[pattern].}
|
|||
(add1 (abs n)))
|
||||
#:attempts 3)]
|
||||
|
||||
@defform/subs[(redex-generator language-id satisfying size-expr)
|
||||
([satisfying (judgment-form-id @#,ttpattern ...)
|
||||
(code:line (metafunction-id @#,ttpattern ...) = @#,ttpattern)])
|
||||
#:contracts ([size-expr natural-number/c])]{
|
||||
|
||||
@italic{WARNING: @racket[redex-generator] is a new, experimental form,
|
||||
and its API may change.}
|
||||
|
||||
Returns a thunk that, each time it is called, either generates a random
|
||||
s-expression based on @racket[satisfying] or fails to (and returns @racket[#f]).
|
||||
The terms returned by a particular thunk are guaranteed to be distinct.
|
||||
|
||||
@examples[#:eval
|
||||
redex-eval
|
||||
(define gen-sum (redex-generator nats (sum n_1 n_2 n_3) 5))
|
||||
(gen-sum)
|
||||
(gen-sum)
|
||||
(gen-sum)
|
||||
(gen-sum)]
|
||||
}
|
||||
|
||||
@defstruct[counterexample ([term any/c]) #:inspector #f]{
|
||||
Produced by @racket[redex-check], @racket[check-reduction-relation], and
|
||||
@racket[check-metafunction] when testing falsifies a property.}
|
||||
|
|
@ -1834,6 +1855,7 @@ Raised by @racket[redex-check], @racket[check-reduction-relation], and
|
|||
The @racket[exn:fail:redex:test-source] component contains the exception raised by the property,
|
||||
and the @racket[exn:fail:redex:test-term] component contains the term that induced the exception.}
|
||||
|
||||
|
||||
@defform/subs[(check-reduction-relation relation property kw-args ...)
|
||||
([kw-arg (code:line #:attempts attempts-expr)
|
||||
(code:line #:retries retries-expr)
|
||||
|
|
|
|||
|
|
@ -133,8 +133,7 @@
|
|||
|
||||
(test-equal (generate-term STLC
|
||||
#:satisfying
|
||||
(lookup x ([x int] ([x (int → int)] •)))
|
||||
(int → int)
|
||||
(lookup x ([x int] ([x (int → int)] •))) = (int → int)
|
||||
6)
|
||||
#f))
|
||||
|
||||
|
|
@ -317,7 +316,7 @@
|
|||
(void)]))
|
||||
|
||||
(for ([_ 50])
|
||||
(define t (generate-term l #:satisfying (fltr n e) e_1 5))
|
||||
(define t (generate-term l #:satisfying (fltr n e) = e_1 5))
|
||||
(match t
|
||||
[`((fltr ,n ,e) = ,e1)
|
||||
(test-equal (term (fltr ,n ,e)) e1)]
|
||||
|
|
@ -332,9 +331,7 @@
|
|||
[`((fltr ,n ,e) = ,e1)
|
||||
(test-equal (term (fltr ,n ,e)) e1)])
|
||||
terms)
|
||||
(void)
|
||||
|
||||
)
|
||||
(void))
|
||||
|
||||
(let ()
|
||||
|
||||
|
|
@ -360,30 +357,30 @@
|
|||
[(is-a/b/c/d/e? e) T])
|
||||
|
||||
|
||||
(test-equal (generate-term L #:satisfying (is-a? a) any +inf.0)
|
||||
(test-equal (generate-term L #:satisfying (is-a? a) = any +inf.0)
|
||||
'((is-a? a) = T))
|
||||
(test-equal (generate-term L #:satisfying (is-a? b) any +inf.0)
|
||||
(test-equal (generate-term L #:satisfying (is-a? b) = any +inf.0)
|
||||
'((is-a? b) = F))
|
||||
(test-equal (generate-term L #:satisfying (is-a? c) any +inf.0)
|
||||
(test-equal (generate-term L #:satisfying (is-a? c) = any +inf.0)
|
||||
'((is-a? c) = F))
|
||||
(test-equal (generate-term L #:satisfying (is-a/b? a) any +inf.0)
|
||||
(test-equal (generate-term L #:satisfying (is-a/b? a) = any +inf.0)
|
||||
'((is-a/b? a) = T))
|
||||
(test-equal (generate-term L #:satisfying (is-a/b? b) any +inf.0)
|
||||
(test-equal (generate-term L #:satisfying (is-a/b? b) = any +inf.0)
|
||||
'((is-a/b? b) = T))
|
||||
(test-equal (generate-term L #:satisfying (is-a/b? c) any +inf.0)
|
||||
(test-equal (generate-term L #:satisfying (is-a/b? c) = any +inf.0)
|
||||
'((is-a/b? c) = F))
|
||||
|
||||
(test-equal (generate-term L #:satisfying (is-a/b/c/d/e? a) any +inf.0)
|
||||
(test-equal (generate-term L #:satisfying (is-a/b/c/d/e? a) = any +inf.0)
|
||||
'((is-a/b/c/d/e? a) = T))
|
||||
(test-equal (generate-term L #:satisfying (is-a/b/c/d/e? b) any +inf.0)
|
||||
(test-equal (generate-term L #:satisfying (is-a/b/c/d/e? b) = any +inf.0)
|
||||
'((is-a/b/c/d/e? b) = T))
|
||||
(test-equal (generate-term L #:satisfying (is-a/b/c/d/e? c) any +inf.0)
|
||||
(test-equal (generate-term L #:satisfying (is-a/b/c/d/e? c) = any +inf.0)
|
||||
'((is-a/b/c/d/e? c) = T))
|
||||
(test-equal (generate-term L #:satisfying (is-a/b/c/d/e? d) any +inf.0)
|
||||
(test-equal (generate-term L #:satisfying (is-a/b/c/d/e? d) = any +inf.0)
|
||||
'((is-a/b/c/d/e? d) = T))
|
||||
(test-equal (generate-term L #:satisfying (is-a/b/c/d/e? e) any +inf.0)
|
||||
(test-equal (generate-term L #:satisfying (is-a/b/c/d/e? e) = any +inf.0)
|
||||
'((is-a/b/c/d/e? e) = T))
|
||||
(test-equal (generate-term L #:satisfying (is-a/b/c/d/e? f) any +inf.0)
|
||||
(test-equal (generate-term L #:satisfying (is-a/b/c/d/e? f) = any +inf.0)
|
||||
'((is-a/b/c/d/e? f) = F)))
|
||||
|
||||
;; errors for unsupprted pats
|
||||
|
|
@ -394,7 +391,7 @@
|
|||
(define-metafunction L
|
||||
[(f n) (g n)])
|
||||
(test (with-handlers ((exn:fail? exn-message))
|
||||
(generate-term L #:satisfying (f any) any +inf.0)
|
||||
(generate-term L #:satisfying (f any) = any +inf.0)
|
||||
"didn't raise an exception")
|
||||
#rx".*generate-term:.*side-condition.*"))
|
||||
(let ()
|
||||
|
|
@ -404,7 +401,7 @@
|
|||
(define-metafunction L
|
||||
[(f n) (g n)])
|
||||
(test (with-handlers ((exn:fail? exn-message))
|
||||
(generate-term L #:satisfying (f any) any +inf.0)
|
||||
(generate-term L #:satisfying (f any) = any +inf.0)
|
||||
"didn't raise an exception")
|
||||
#rx".*generate-term:.*repeat.*"))
|
||||
|
||||
|
|
@ -441,7 +438,7 @@
|
|||
(where q_3 (f q_2))])
|
||||
|
||||
(test (with-handlers ([exn:fail? exn-message])
|
||||
(generate-term L #:satisfying (f r_1) r_2 +inf.0))
|
||||
(generate-term L #:satisfying (f r_1) = r_2 +inf.0))
|
||||
#rx".*generate-term:.*undatum.*"))
|
||||
|
||||
|
||||
|
|
@ -451,7 +448,7 @@
|
|||
[(n any) any])
|
||||
(define-metafunction L
|
||||
[(f n) (n 1)])
|
||||
(test-equal (generate-term L #:satisfying (f any_1) any_2 +inf.0)
|
||||
(test-equal (generate-term L #:satisfying (f any_1) = any_2 +inf.0)
|
||||
'((f 2) = (2 1))))
|
||||
|
||||
(let ()
|
||||
|
|
@ -460,7 +457,7 @@
|
|||
[(n any) any])
|
||||
(define-metafunction L
|
||||
[(f n) n])
|
||||
(test-equal (generate-term L #:satisfying (f any_1) any_2 +inf.0)
|
||||
(test-equal (generate-term L #:satisfying (f any_1) = any_2 +inf.0)
|
||||
'((f 2) = 2)))
|
||||
|
||||
(let ()
|
||||
|
|
@ -477,25 +474,25 @@
|
|||
[(t n_1 n_2)
|
||||
4])
|
||||
|
||||
(test-equal (generate-term l #:satisfying (t 1 1) 1 +inf.0)
|
||||
(test-equal (generate-term l #:satisfying (t 1 1) = 1 +inf.0)
|
||||
'((t 1 1) = 1))
|
||||
(test-equal (generate-term l #:satisfying (t 1 1) 2 +inf.0)
|
||||
(test-equal (generate-term l #:satisfying (t 1 1) = 2 +inf.0)
|
||||
#f)
|
||||
(test-equal (generate-term l #:satisfying (t 1 2) 2 +inf.0)
|
||||
(test-equal (generate-term l #:satisfying (t 1 2) = 2 +inf.0)
|
||||
'((t 1 2) = 2))
|
||||
(test-equal (generate-term l #:satisfying (t 1 2) 3 +inf.0)
|
||||
(test-equal (generate-term l #:satisfying (t 1 2) = 3 +inf.0)
|
||||
#f)
|
||||
(test-equal (generate-term l #:satisfying (t 1 3) 3 +inf.0)
|
||||
(test-equal (generate-term l #:satisfying (t 1 3) = 3 +inf.0)
|
||||
'((t 1 3) = 3))
|
||||
(test-equal (generate-term l #:satisfying (t 1 3) 4 +inf.0)
|
||||
(test-equal (generate-term l #:satisfying (t 1 3) = 4 +inf.0)
|
||||
#f)
|
||||
(test-equal (generate-term l #:satisfying (t 6 7) 4 +inf.0)
|
||||
(test-equal (generate-term l #:satisfying (t 6 7) = 4 +inf.0)
|
||||
'((t 6 7) = 4))
|
||||
(test-equal (generate-term l #:satisfying (t 6 7) 3 +inf.0)
|
||||
(test-equal (generate-term l #:satisfying (t 6 7) = 3 +inf.0)
|
||||
#f)
|
||||
(test-equal (generate-term l #:satisfying (t 6 7) 2 +inf.0)
|
||||
(test-equal (generate-term l #:satisfying (t 6 7) = 2 +inf.0)
|
||||
#f)
|
||||
(test-equal (generate-term l #:satisfying (t 6 7) 1 +inf.0)
|
||||
(test-equal (generate-term l #:satisfying (t 6 7) = 1 +inf.0)
|
||||
#f))
|
||||
|
||||
#;
|
||||
|
|
|
|||
|
|
@ -1322,15 +1322,13 @@
|
|||
|
||||
(test (generate-term nats
|
||||
#:satisfying
|
||||
(sum z z)
|
||||
n
|
||||
(sum z z) = n
|
||||
5)
|
||||
'((sum z z) = z))
|
||||
|
||||
(test (generate-term nats
|
||||
#:satisfying
|
||||
(sum (s z) (s z))
|
||||
n
|
||||
(sum (s z) (s z)) = n
|
||||
5)
|
||||
'((sum (s z) (s z)) = (s (s z)))))
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user