suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

add #:post condition to meta functions

Browse Source
This commit is contained in:
Robby Findler 2014-07-09 05:55:22 -05:00
parent 406ba23077
commit e991dd4628
5 changed files with 185 additions and 73 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
View File

@ -1106,9 +1106,12 @@ reduce it further).
...) ...)
([metafunction-contract (code:line) ([metafunction-contract (code:line)
(code:line id : @#,ttpattern-sequence ... -> range (code:line id : @#,ttpattern-sequence ... -> range
maybe-pre-condition)] maybe-pre-condition
maybe-post-condition)]
[maybe-pre-condition (code:line #:pre @#,tttterm) [maybe-pre-condition (code:line #:pre @#,tttterm)
(code:line)] (code:line)]
[maybe-post-condition (code:line #:post @#,tttterm)
(code:line)]
[range @#,ttpattern [range @#,ttpattern
(code:line @#,ttpattern or range) (code:line @#,ttpattern or range)
(code:line @#,ttpattern ∨ range) (code:line @#,ttpattern ∨ range)
@ -1133,7 +1136,10 @@ If present, the term inside the @racket[maybe-pre-condition] is evaluated
after a successful match to the input pattern in the contract (with after a successful match to the input pattern in the contract (with
any variables from the input contract bound). If any variables from the input contract bound). If
it returns @racket[#f], then the input contract is considered to not it returns @racket[#f], then the input contract is considered to not
have matched and an error is also raised. have matched and an error is also raised. When a metafunction
returns, the expression in the @racket[maybe-post-condition] is
evaluated (if present), with any variables from the input or output
contract bound.
The @racket[side-condition], @racket[hidden-side-condition], The @racket[side-condition], @racket[hidden-side-condition],
@racket[where], and @racket[where/hidden] clauses behave as @racket[where], and @racket[where/hidden] clauses behave as
@ -1213,6 +1219,8 @@ ensures that there is a unique match for that case. Without
it, @racket[(term (- (x x) x))] would lead to an ambiguous it, @racket[(term (- (x x) x))] would lead to an ambiguous
match. match.
@history[#:changed "1.4" @list{Added @racket[#:post] conditions.}]
} }
@defform[(define-metafunction/extension f language @defform[(define-metafunction/extension f language

2
pkgs/redex-pkgs/redex-lib/info.rkt
View File

@ -18,4 +18,4 @@
(define pkg-authors '(robby bfetscher)) (define pkg-authors '(robby bfetscher))
(define version "1.3") (define version "1.4")

50
pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt
View File

@ -407,7 +407,7 @@
(begin (begin
(unless (identifier? #'lang) (unless (identifier? #'lang)
(raise-syntax-error #f "expected an identifier in the language position" stx #'lang)) (raise-syntax-error #f "expected an identifier in the language position" stx #'lang))
(define-values (contract-name dom-ctcs pre-condition codom-contracts pats) (define-values (contract-name dom-ctcs pre-condition codom-contracts post-condition pats)
(split-out-contract stx (syntax-e #'def-form-id) #'body #t)) (split-out-contract stx (syntax-e #'def-form-id) #'body #t))
(with-syntax* ([((name trms ...) rest ...) (car pats)] (with-syntax* ([((name trms ...) rest ...) (car pats)]
[(mode-stx ...) #`(#:mode (name I))] [(mode-stx ...) #`(#:mode (name I))]
@ -425,7 +425,7 @@
;; initial test determines if a contract is specified or not ;; initial test determines if a contract is specified or not
(cond (cond
[(pair? (syntax-e (car (syntax->list rest)))) [(pair? (syntax-e (car (syntax->list rest))))
(values #f #f #f (list #'any) (check-clauses stx syn-error-name (syntax->list rest) relation?))] (values #f #f #f (list #'any) #f (check-clauses stx syn-error-name (syntax->list rest) relation?))]
[else [else
(syntax-case rest () (syntax-case rest ()
[(id separator more ...) [(id separator more ...)
@ -438,7 +438,7 @@
(raise-syntax-error syn-error-name (raise-syntax-error syn-error-name
"expected clause definitions to follow domain contract" "expected clause definitions to follow domain contract"
stx)) stx))
(values #'id contract #f (list #'any) (check-clauses stx syn-error-name clauses #t)))] (values #'id contract #f (list #'any) #f (check-clauses stx syn-error-name clauses #t)))]
[else [else
(unless (eq? ': (syntax-e #'separator)) (unless (eq? ': (syntax-e #'separator))
(raise-syntax-error syn-error-name "expected a colon to follow the meta-function's name" stx #'separator)) (raise-syntax-error syn-error-name "expected a colon to follow the meta-function's name" stx #'separator))
@ -448,18 +448,19 @@
[(null? more) [(null? more)
(raise-syntax-error syn-error-name "expected an ->" stx)] (raise-syntax-error syn-error-name "expected an ->" stx)]
[(eq? (syntax-e (car more)) '->) [(eq? (syntax-e (car more)) '->)
(define-values (raw-clauses rev-codomains pre-condition) (define-values (raw-clauses rev-codomains pre-condition post-condition)
(let loop ([prev (car more)] (let loop ([prev (car more)]
[more (cdr more)] [more (cdr more)]
[codomains '()]) [codomains '()])
(cond (cond
[(null? more) [(null? more)
(raise-syntax-error syn-error-name "expected a range contract to follow" stx prev)] (raise-syntax-error syn-error-name
"expected a range contract to follow" stx prev)]
[else [else
(define after-this-one (cdr more)) (define after-this-one (cdr more))
(cond (cond
[(null? after-this-one) [(null? after-this-one)
(values null (cons (car more) codomains) #t)] (values null (cons (car more) codomains) #t #t)]
[else [else
(define kwd (cadr more)) (define kwd (cadr more))
(cond (cond
@ -467,17 +468,41 @@
(loop kwd (loop kwd
(cddr more) (cddr more)
(cons (car more) codomains))] (cons (car more) codomains))]
[(and (not relation?) (equal? (syntax-e kwd) '#:pre)) [(and (not relation?)
(or (equal? (syntax-e kwd) '#:pre)
(equal? (syntax-e kwd) '#:post)))
(when (null? (cddr more)) (when (null? (cddr more))
(raise-syntax-error 'define-metafunction (raise-syntax-error
"expected an expression to follow #:pre keyword" 'define-metafunction
kwd)) (format "expected an expression to follow ~a keyword"
(values (cdddr more) (syntax-e kwd))
kwd))
(define pre #t)
(define post #t)
(define remainder (cdddr more))
(cond
[(equal? (syntax-e kwd) '#:pre)
(set! pre (caddr more))
(define without-pre (cdddr more))
(when (and (pair? without-pre)
(equal? (syntax-e (car without-pre)) '#:post))
(when (null? (cddr without-pre))
(raise-syntax-error
'define-metafunction
"expected an expression to follow #:post keyword"
kwd))
(set! remainder (cddr without-pre))
(set! post (cadr without-pre)))]
[(equal? (syntax-e kwd) '#:post)
(set! post (caddr more))])
(values remainder
(cons (car more) codomains) (cons (car more) codomains)
(caddr more))] pre
post)]
[else [else
(values (cdr more) (values (cdr more)
(cons (car more) codomains) (cons (car more) codomains)
#t
#t)])])]))) #t)])])])))
(let ([doms (reverse dom-pats)] (let ([doms (reverse dom-pats)]
[clauses (check-clauses stx syn-error-name raw-clauses relation?)]) [clauses (check-clauses stx syn-error-name raw-clauses relation?)])
@ -485,6 +510,7 @@
doms doms
(if relation? #f pre-condition) (if relation? #f pre-condition)
(reverse rev-codomains) (reverse rev-codomains)
(if relation? #f post-condition)
clauses))] clauses))]
[else [else
(loop (cdr more) (cons (car more) dom-pats))]))])] (loop (cdr more) (cons (car more) dom-pats))]))])]

162
pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt
View File

@ -1186,8 +1186,10 @@
(syntax-local-value (syntax-local-value
prev-metafunction prev-metafunction
(λ () (λ ()
(raise-syntax-error syn-error-name "expected a previously defined metafunction" orig-stx prev-metafunction)))) (raise-syntax-error
(let*-values ([(contract-name dom-ctcs pre-condition codom-contracts pats) syn-error-name
"expected a previously defined metafunction" orig-stx prev-metafunction))))
(let*-values ([(contract-name dom-ctcs pre-condition codom-contracts post-condition pats)
(split-out-contract orig-stx syn-error-name #'rest #f)] (split-out-contract orig-stx syn-error-name #'rest #f)]
[(name _) (defined-name (list contract-name) pats orig-stx)]) [(name _) (defined-name (list contract-name) pats orig-stx)])
(when (and prev-metafunction (eq? (syntax-e #'name) (syntax-e prev-metafunction))) (when (and prev-metafunction (eq? (syntax-e #'name) (syntax-e prev-metafunction)))
@ -1208,8 +1210,13 @@
name name
name-predicate name-predicate
#,dom-ctcs #,dom-ctcs
#,pre-condition #,(if pre-condition
(list pre-condition)
#f)
#,codom-contracts #,codom-contracts
#,(if post-condition
(list post-condition)
#f)
#,pats #,pats
#,syn-error-name)) #,syn-error-name))
(term-define-fn name name2))]) (term-define-fn name name2))])
@ -1252,16 +1259,26 @@
(define-syntax (generate-metafunction stx) (define-syntax (generate-metafunction stx)
(syntax-case stx () (syntax-case stx ()
[(_ orig-stx lang prev-metafunction [(_ orig-stx lang prev-metafunction-stx
name name-predicate name name-predicate
dom-ctcs pre-condition dom-ctcs-stx pre-condition-stx
codom-contracts pats syn-error-name) codom-contracts-stx post-condition-stx
(let ([prev-metafunction (and (syntax-e #'prev-metafunction) #'prev-metafunction)] pats-stx syn-error-name)
[dom-ctcs (syntax-e #'dom-ctcs)] (let ()
[pre-condition (syntax-e #'pre-condition)] (define (condition-or-false s)
[codom-contracts (syntax-e #'codom-contracts)] (define info (syntax-e s))
[pats (syntax-e #'pats)] (cond
[syn-error-name (syntax-e #'syn-error-name)]) [info
(unless (pair? info) (error 'condition-or-false "~s" s))
(car info)]
[else #f]))
(define prev-metafunction (and (syntax-e #'prev-metafunction-stx) #'prev-metafunction-stx))
(define dom-ctcs (syntax-e #'dom-ctcs-stx))
(define pre-condition (condition-or-false #'pre-condition-stx))
(define codom-contracts (syntax-e #'codom-contracts-stx))
(define post-condition (condition-or-false #'post-condition-stx))
(define pats (syntax-e #'pats-stx))
(define syn-error-name (syntax-e #'syn-error-name))
(define lang-nts (define lang-nts
(definition-nts #'lang #'orig-stx syn-error-name)) (definition-nts #'lang #'orig-stx syn-error-name))
(with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats] (with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats]
@ -1322,21 +1339,29 @@
(syntax-line lhs) (syntax-line lhs)
(syntax-column lhs))) (syntax-column lhs)))
pats)] pats)]
[(dom-syncheck-expr dom-side-conditions-rewritten dom-names dom-names/ellipses) [(dom-syncheck-expr dom-side-conditions-rewritten
(dom-names ...)
dom-names/ellipses)
(if dom-ctcs (if dom-ctcs
(rewrite-side-conditions/check-errs (rewrite-side-conditions/check-errs
#'lang #'lang
syn-error-name syn-error-name
#f #f
#`(side-condition #,dom-ctcs (term #,pre-condition))) dom-ctcs)
#'((void) any () ()))] #'((void) any () ()))]
[((codom-syncheck-expr codom-side-conditions-rewritten codom-names codom-names/ellipses) ...) [((codom-syncheck-expr
codom-side-conditions-rewritten
codom-names
codom-names/ellipses) ...)
(map (λ (codom-contract) (map (λ (codom-contract)
(rewrite-side-conditions/check-errs (rewrite-side-conditions/check-errs
#'lang #'lang
syn-error-name syn-error-name
#f #f
codom-contract)) (if post-condition
#`(side-condition (#,dom-ctcs #,codom-contract)
(term #,post-condition))
codom-contract)))
codom-contracts)] codom-contracts)]
[(rhs-fns ...) [(rhs-fns ...)
(map (λ (names names/ellipses rhs/where) (map (λ (names names/ellipses rhs/where)
@ -1415,7 +1440,13 @@
(λ () (λ ()
(add-mf-dqs #,(check-pats #'(list gen-clause ...)))))]))) (add-mf-dqs #,(check-pats #'(list gen-clause ...)))))])))
#,(if dom-ctcs #'dsc #f) #,(if dom-ctcs #'dsc #f)
(λ (bindings)
#,(bind-pattern-names 'define-metafunction
#'dom-names/ellipses
#'((lookup-binding bindings 'dom-names) ...)
#`(term #,pre-condition)))
`(codom-side-conditions-rewritten ...) `(codom-side-conditions-rewritten ...)
#,(and post-condition #t)
'name)))) 'name))))
'disappeared-use 'disappeared-use
(map syntax-local-introduce (map syntax-local-introduce
@ -1575,7 +1606,11 @@
(syntax->list extras))) (syntax->list extras)))
(define (build-metafunction lang cases parent-cases wrap dom-contract-pat codom-contract-pats name) (define (build-metafunction lang cases parent-cases
wrap
dom-contract-pat pre-condition
codom-contract-pats post-condition?
name)
(let* ([dom-compiled-pattern (and dom-contract-pat (compile-pattern lang dom-contract-pat #f))] (let* ([dom-compiled-pattern (and dom-contract-pat (compile-pattern lang dom-contract-pat #f))]
[codom-compiled-patterns (map (λ (codom-contract-pat) (compile-pattern lang codom-contract-pat #f)) [codom-compiled-patterns (map (λ (codom-contract-pat) (compile-pattern lang codom-contract-pat #f))
codom-contract-pats)] codom-contract-pats)]
@ -1610,8 +1645,17 @@
(let ([cache-ref (hash-ref cache exp not-in-cache)]) (let ([cache-ref (hash-ref cache exp not-in-cache)])
(cond (cond
[(or (not (caching-enabled?)) (eq? cache-ref not-in-cache)) [(or (not (caching-enabled?)) (eq? cache-ref not-in-cache))
(define dom-match-result
(if dom-compiled-pattern
(match-pattern dom-compiled-pattern exp)
'()))
(when dom-compiled-pattern (when dom-compiled-pattern
(unless (match-pattern dom-compiled-pattern exp) (unless dom-match-result
(redex-error name
"~s is not in my domain"
`(,name ,@exp)))
(unless (for/and ([mtch (in-list dom-match-result)])
(pre-condition (mtch-bindings mtch)))
(redex-error name (redex-error name
"~s is not in my domain" "~s is not in my domain"
`(,name ,@exp)))) `(,name ,@exp))))
@ -1623,45 +1667,49 @@
[(null? ids) [(null? ids)
(redex-error name "no clauses matched for ~s" `(,name . ,exp))] (redex-error name "no clauses matched for ~s" `(,name . ,exp))]
[else [else
(let ([pattern (car lhss)] (define pattern (car lhss))
[rhs (car rhss)] (define rhs (car rhss))
[id (car ids)] (define id (car ids))
[continue (λ () (loop (cdr ids) (cdr lhss) (cdr rhss) (+ num 1)))]) (define (continue) (loop (cdr ids) (cdr lhss) (cdr rhss) (+ num 1)))
(let ([mtchs (match-pattern pattern exp)]) (define mtchs (match-pattern pattern exp))
(cond (cond
[(not mtchs) (continue)] [(not mtchs) (continue)]
[else [else
(let ([anss (apply append (define anss
(filter values (apply append
(map (λ (mtch) (rhs traced-metafunc (mtch-bindings mtch))) (filter values
mtchs)))] (map (λ (mtch) (rhs traced-metafunc (mtch-bindings mtch)))
[ht (make-hash)]) mtchs))))
(for-each (λ (ans) (hash-set! ht ans #t)) anss) (define ht (make-hash))
(cond (for-each (λ (ans) (hash-set! ht ans #t)) anss)
[(null? anss) (cond
(continue)] [(null? anss)
[(not (= 1 (hash-count ht))) (continue)]
(redex-error name "~a matched ~s ~a returned different results" [(not (= 1 (hash-count ht)))
(if (< num 0) (redex-error name "~a matched ~s ~a returned different results"
"a clause from an extended metafunction" (if (< num 0)
(format "clause #~a (counting from 0)" num)) "a clause from an extended metafunction"
`(,name ,@exp) (format "clause #~a (counting from 0)" num))
(if (= 1 (length mtchs)) `(,name ,@exp)
"but" (if (= 1 (length mtchs))
(format "~a different ways and " "but"
(length mtchs))))] (format "~a different ways and "
[else (length mtchs))))]
(let ([ans (car anss)]) [else
(unless (ormap (λ (codom-compiled-pattern) (define ans (car anss))
(match-pattern codom-compiled-pattern ans)) (unless (for/or ([codom-compiled-pattern
codom-compiled-patterns) (in-list codom-compiled-patterns)])
(redex-error name (match-pattern codom-compiled-pattern
"codomain test failed for ~s, call was ~s" (if post-condition?
ans (list exp ans)
`(,name ,@exp))) ans)))
(cache-result exp ans id) (redex-error name
(log-coverage id) "codomain test failed for ~s, call was ~s"
ans)]))])))]))] ans
`(,name ,@exp)))
(cache-result exp ans id)
(log-coverage id)
ans])])]))]
[else [else
(log-coverage (cdr cache-ref)) (log-coverage (cdr cache-ref))
(car cache-ref)])))] (car cache-ref)])))]

32
pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt
View File

@ -1197,7 +1197,37 @@
(test (term (m 1 1)) 1) (test (term (m 1 1)) 1)
(test (with-handlers ((exn:fail:redex? exn-message)) (test (with-handlers ((exn:fail:redex? exn-message))
(term (m 1 2))) (term (m 1 2)))
#rx"is not in my domain")) #rx"is not in my domain")
(define-metafunction empty-language
is-nat : any -> boolean
[(is-nat natural) #t]
[(is-nat any) #f])
(define-metafunction empty-language
post-only : any_1 -> any_2
#:post (same any_1 any_2)
[(post-only any) 1])
(test (term (post-only 1)) 1)
(test (with-handlers ([exn:fail:redex? exn-message])
(term (post-only 2)))
#rx"codomain")
(define-metafunction empty-language
pre-and-post : any_1 -> any_2
#:pre (is-nat any_1)
#:post (same any_1 any_2)
[(pre-and-post any) 1])
(test (term (pre-and-post 1)) 1)
(test (with-handlers ([exn:fail:redex? exn-message])
(term (pre-and-post x)))
#rx"is not in my domain")
(test (with-handlers ([exn:fail:redex? exn-message])
(term (pre-and-post 2)))
#rx"codomain")
)
(let () (let ()
(define-language L (define-language L