Adds support for ellipsis-repeated premises
This commit is contained in:
Casey Klein
parent
f803f187bd
commit
87f3541979
|
|
@ -1053,7 +1053,8 @@
|
|||
[(struct metafunc-extra-where (lhs rhs))
|
||||
(where-pict (wrapper->pict lhs) (wrapper->pict rhs))]
|
||||
[(struct metafunc-extra-side-cond (expr))
|
||||
(wrapper->pict expr)])
|
||||
(wrapper->pict expr)]
|
||||
[wrapper (wrapper->pict wrapper)])
|
||||
(list-ref eqn 1))))
|
||||
eqns)])
|
||||
((relation-clauses-combine)
|
||||
|
|
|
|||
|
|
@ -316,6 +316,10 @@
|
|||
[w/ellipses names/ellipses])
|
||||
(hash-set extended (syntax-e name) w/ellipses))))
|
||||
|
||||
(define-for-syntax (ellipsis? stx)
|
||||
(and (identifier? stx)
|
||||
(free-identifier=? stx (quote-syntax ...))))
|
||||
|
||||
;; the withs, freshs, and side-conditions come in backwards order
|
||||
(define-for-syntax (bind-withs orig-name main lang lang-nts stx where-mode body names w/ellipses)
|
||||
(with-disappeared-uses
|
||||
|
|
@ -386,27 +390,43 @@
|
|||
(verify-names-ok '#,orig-name the-names len-counter)
|
||||
(variables-not-in #,to-not-be-in the-names))])
|
||||
#,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in) env))]
|
||||
[((form-name . pats) . rest-clauses)
|
||||
[((form-name . pats) . after)
|
||||
(judgment-form-id? #'form-name)
|
||||
(let*-values ([(judgment-form) (syntax-local-value/record #'form-name (λ (_) #t))]
|
||||
(let*-values ([(premise) (syntax-case stx () [(p . _) #'p])]
|
||||
[(rest-clauses under-ellipsis?)
|
||||
(syntax-case #'after ()
|
||||
[(maybe-ellipsis . more)
|
||||
(ellipsis? #'maybe-ellipsis)
|
||||
(values #'more #t)]
|
||||
[_ (values #'after #f)])]
|
||||
[(judgment-form) (syntax-local-value/record #'form-name (λ (_) #t))]
|
||||
[(mode) (judgment-form-mode judgment-form)]
|
||||
[(judgment-proc) (judgment-form-proc judgment-form)]
|
||||
[(input-template output-pre-pattern) (split-by-mode (syntax->list #'pats) mode)]
|
||||
[(input-template output-pre-pattern)
|
||||
(let-values ([(in out) (split-by-mode (syntax->list #'pats) mode)])
|
||||
(if under-ellipsis?
|
||||
(let ([ellipsis (syntax/loc premise (... ...))])
|
||||
(values #`(#,in #,ellipsis) #`(#,out #,ellipsis)))
|
||||
(values in out)))]
|
||||
[(output-pattern)
|
||||
(rewrite-side-conditions/check-errs lang-nts orig-name #t output-pre-pattern)]
|
||||
[(output-names output-names/ellipses)
|
||||
(extract-names lang-nts orig-name #t output-pattern)]
|
||||
(extract-names lang-nts orig-name #t output-pre-pattern)]
|
||||
[(binding-constraints temporaries env+)
|
||||
(generate-binding-constraints output-names output-names/ellipses env orig-name)]
|
||||
[(rest-body) (loop #'rest-clauses #`(list judgment-output #,to-not-be-in) env+)]
|
||||
[(call) (quasisyntax/loc #'form-name
|
||||
(call-judgment-form
|
||||
'form-name #,judgment-proc '#,mode (term #,input-template)))])
|
||||
[(rest-body) (loop rest-clauses #`(list judgment-output #,to-not-be-in) env+)]
|
||||
[(call)
|
||||
(let ([input (quasisyntax/loc premise (term #,input-template))])
|
||||
(define (make-traced input)
|
||||
(quasisyntax/loc premise
|
||||
(call-judgment-form 'form-name #,judgment-proc '#,mode #,input)))
|
||||
(if under-ellipsis?
|
||||
#`(repeated-premise-outputs #,input (λ (x) #,(make-traced #'x)))
|
||||
(make-traced input)))])
|
||||
(with-syntax ([(output-name ...) output-names]
|
||||
[(output-name/ellipsis ...) output-names/ellipses]
|
||||
[(temp ...) temporaries]
|
||||
[(binding-constraint ...) binding-constraints])
|
||||
(syntax-case stx () [(clause . _) #'clause])
|
||||
#`(begin
|
||||
(void #,(defined-check judgment-proc "judgment form" #:external #'form-name))
|
||||
(for/fold ([outputs '()]) ([sub-output #,call])
|
||||
|
|
@ -415,13 +435,24 @@
|
|||
(if mtchs
|
||||
(for/fold ([outputs outputs]) ([mtch mtchs])
|
||||
(let ([temp (lookup-binding (mtch-bindings mtch) 'output-name)] ...)
|
||||
(and binding-constraint ...
|
||||
(term-let ([output-name/ellipsis temp] ...)
|
||||
(let ([output-rest #,rest-body])
|
||||
(and output-rest
|
||||
(append outputs output-rest)))))))
|
||||
(define mtch-outputs
|
||||
(and binding-constraint ...
|
||||
(term-let ([output-name/ellipsis temp] ...)
|
||||
#,rest-body)))
|
||||
(if mtch-outputs
|
||||
(append mtch-outputs outputs)
|
||||
outputs)))
|
||||
outputs)))))]))))
|
||||
|
||||
(define (repeated-premise-outputs inputs premise)
|
||||
(if (null? inputs)
|
||||
'(())
|
||||
(let ([output (premise (car inputs))])
|
||||
(if (null? output)
|
||||
'()
|
||||
(for*/list ([o output] [os (repeated-premise-outputs (cdr inputs) premise)])
|
||||
(cons o os))))))
|
||||
|
||||
(define (call-judgment-form form-name form-proc mode input)
|
||||
(define traced (current-traced-metafunctions))
|
||||
(if (or (eq? 'all traced) (memq form-name traced))
|
||||
|
|
@ -1500,22 +1531,9 @@
|
|||
(define-syntax #,judgment-form-name
|
||||
(judgment-form '#,judgment-form-name '#,mode #'judgment-form-proc #'#,lang #'judgment-form-lws))
|
||||
(define judgment-form-proc
|
||||
(let-syntax ([delayed
|
||||
(λ (stx)
|
||||
(syntax-case stx ()
|
||||
[(_ lang clauses ctcs full-def)
|
||||
(let ([nts (definition-nts #'lang #'full-def '#,syn-err-name)])
|
||||
(mode-check '#,mode (syntax->list #'clauses) nts '#,syn-err-name)
|
||||
(compile-judgment-form-proc
|
||||
'#,judgment-form-name '#,mode (syntax->list #'clauses) #'ctcs nts #'lang '#,syn-err-name))]))])
|
||||
(delayed #,lang #,clauses #,position-contracts #,stx)))
|
||||
(compile-judgment-form-proc #,judgment-form-name #,lang #,mode #,clauses #,position-contracts #,stx #,syn-err-name))
|
||||
(define judgment-form-lws
|
||||
(let-syntax ([delayed
|
||||
(λ (stx)
|
||||
(syntax-case stx ()
|
||||
[(_ clauses)
|
||||
(compile-judgment-form-lws (syntax->list #'clauses))]))])
|
||||
(delayed #,clauses)))))
|
||||
(compiled-judgment-form-lws #,clauses))))
|
||||
(syntax-property
|
||||
(prune-syntax
|
||||
(if (eq? 'top-level (syntax-local-context))
|
||||
|
|
@ -1781,15 +1799,16 @@
|
|||
(judgment-form-id? #'form-name)
|
||||
(let* ([syn-err-name (syntax-e #'j-h)]
|
||||
[lang (judgment-form-lang (syntax-local-value #'form-name))]
|
||||
[nts (definition-nts lang stx syn-err-name)])
|
||||
[nts (definition-nts lang stx syn-err-name)]
|
||||
[judgment (syntax-case stx () [(_ judgment _) #'judgment])])
|
||||
(check-judgment-arity #'(form-name . pats))
|
||||
(bind-withs syn-err-name '() lang nts (list #'(form-name . pats))
|
||||
(bind-withs syn-err-name '() lang nts (list judgment)
|
||||
'flatten #`(list (term #,#'tmpl)) '() '()))]
|
||||
[(_ (not-form-name . _) . _)
|
||||
(not (judgment-form-id? #'form-name))
|
||||
(raise-syntax-error #f "expected a judgment form name" stx #'not-form-name)]))
|
||||
|
||||
(define-for-syntax (compile-judgment-form-proc name mode clauses contracts nts lang syn-error-name)
|
||||
(define-for-syntax (do-compile-judgment-form-proc name mode clauses contracts nts lang syn-error-name)
|
||||
(define (compile-clause clause)
|
||||
(syntax-case clause ()
|
||||
[((_ . conc-pats) . prems)
|
||||
|
|
@ -1845,7 +1864,7 @@
|
|||
[_ #t]))
|
||||
(syntax->list extras))))
|
||||
|
||||
(define-for-syntax (compile-judgment-form-lws clauses)
|
||||
(define-for-syntax (do-compile-judgment-form-lws clauses)
|
||||
(syntax-case clauses ()
|
||||
[(((_ . conc-body) . prems) ...)
|
||||
(let ([rev-premss
|
||||
|
|
@ -1893,6 +1912,18 @@
|
|||
(syntax-case judgment ()
|
||||
[(form-name . body)
|
||||
(split-by-mode (syntax->list #'body) (judgment-form-mode (syntax-local-value #'form-name)))]))
|
||||
(define (drop-ellipses prems)
|
||||
(syntax-case prems ()
|
||||
[() '()]
|
||||
[(prem maybe-ellipsis . remaining)
|
||||
(ellipsis? #'maybe-ellipsis)
|
||||
(syntax-case #'prem ()
|
||||
[(form-name . _)
|
||||
(judgment-form-id? #'form-name)
|
||||
(cons #'prem (drop-ellipses #'remaining))]
|
||||
[_ (raise-syntax-error syn-err-name "ellipses must follow judgment form uses" #'maybe-ellipsis)])]
|
||||
[(prem . remaining)
|
||||
(cons #'prem (drop-ellipses #'remaining))]))
|
||||
(define (fold-clause pat-pos tmpl-pos acc-init clause)
|
||||
(syntax-case clause ()
|
||||
[(conc . prems)
|
||||
|
|
@ -1900,7 +1931,7 @@
|
|||
(check-judgment-arity #'conc)
|
||||
(define acc-out
|
||||
(for/fold ([acc (foldl pat-pos acc-init conc-in)])
|
||||
([prem (syntax->list #'prems)])
|
||||
([prem (drop-ellipses #'prems)])
|
||||
(syntax-case prem ()
|
||||
[(form-name . _)
|
||||
(judgment-form-id? #'form-name)
|
||||
|
|
@ -1963,7 +1994,10 @@
|
|||
#,(to-lw/proc #'pat) #,(to-lw/proc #'exp))]
|
||||
[(side-condition x)
|
||||
#`(make-metafunc-extra-side-cond
|
||||
#,(to-lw/uq/proc #'x))]))
|
||||
#,(to-lw/uq/proc #'x))]
|
||||
[maybe-ellipsis
|
||||
(ellipsis? #'maybe-ellipsis)
|
||||
(to-lw/proc #'maybe-ellipsis)]))
|
||||
(in-order-non-hidden hm)))
|
||||
(syntax->list #'seq-of-tl-side-cond/binds))]
|
||||
[(((where-bind-id/lw . where-bind-pat/lw) ...) ...)
|
||||
|
|
@ -1994,6 +2028,25 @@
|
|||
rhs/lw)
|
||||
...))]))
|
||||
|
||||
(define-syntax (compile-judgment-form-proc stx)
|
||||
(syntax-case stx ()
|
||||
[(_ judgment-form-name lang mode clauses ctcs full-def syn-err-name)
|
||||
(let ([nts (definition-nts #'lang #'full-def (syntax-e #'syn-err-name))])
|
||||
(mode-check (syntax->datum #'mode) (syntax->list #'clauses) nts (syntax-e #'syn-err-name))
|
||||
(do-compile-judgment-form-proc
|
||||
(syntax-e #'judgment-form-name)
|
||||
(syntax->datum #'mode)
|
||||
(syntax->list #'clauses)
|
||||
#'ctcs
|
||||
nts
|
||||
#'lang
|
||||
(syntax-e #'syn-err-name)))]))
|
||||
|
||||
(define-syntax (compiled-judgment-form-lws stx)
|
||||
(syntax-case stx ()
|
||||
[(_ clauses)
|
||||
(do-compile-judgment-form-lws (syntax->list #'clauses))]))
|
||||
|
||||
(define (build-metafunction lang cases parent-cases wrap dom-contract-pat codom-contract-pats name relation?)
|
||||
(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))
|
||||
|
|
|
|||
|
|
@ -1092,11 +1092,13 @@ and @racket[#f] otherwise.
|
|||
dashes
|
||||
conclusion]]
|
||||
[conclusion (form-id pat/term ...)]
|
||||
[premise (judgment-form-id pat/term ...)
|
||||
[premise (code:line (judgment-form-id pat/term ...) maybe-ellipsis)
|
||||
(where @#,ttpattern @#,tttterm)
|
||||
(where/hidden @#,ttpattern @#,tttterm)]
|
||||
[pat/term @#,ttpattern
|
||||
@#,tttterm]
|
||||
[maybe-ellipsis (code:line)
|
||||
...]
|
||||
[dashes ---
|
||||
----
|
||||
-----
|
||||
|
|
@ -1176,6 +1178,25 @@ A rule's @racket[where] and @racket[where/hidden] premises behave as in
|
|||
(judgment-holds (gt (s (s z)) (s z)))
|
||||
(judgment-holds (gt (s z) (s z)))]
|
||||
|
||||
A literal ellipsis may follow a judgment premise when a template in one of the
|
||||
judgment's input positions contains a pattern variable bound at ellipsis-depth
|
||||
one.
|
||||
@examples[
|
||||
#:eval redex-eval
|
||||
(define-judgment-form nats
|
||||
#:mode (even I)
|
||||
#:contract (even n)
|
||||
[(even z)]
|
||||
[(even (s (s n)))
|
||||
(even n)])
|
||||
(define-judgment-form nats
|
||||
#:mode (all-even I)
|
||||
#:contract (all-even (n ...))
|
||||
[(all-even (n ...))
|
||||
(even n) ...])
|
||||
(judgment-holds (all-even (z (s (s z)) z)))
|
||||
(judgment-holds (all-even (z (s (s z)) (s z))))]
|
||||
|
||||
Redex evaluates premises depth-first, even when it doing so leads to
|
||||
non-termination. For example, consider the following definitions:
|
||||
@interaction[
|
||||
|
|
|
|||
|
|
@ -305,7 +305,20 @@
|
|||
(nps z (name n_1 (s (s n_1))))
|
||||
(where (name b n_2) z)])
|
||||
|
||||
(test (render-judgment-form nps) "judgment-form-name-patterns.png"))
|
||||
(test (render-judgment-form nps) "judgment-form-name-patterns.png")
|
||||
|
||||
(define-judgment-form nats
|
||||
#:mode (lt2 I)
|
||||
[(lt2 z)]
|
||||
[(lt2 (s z))])
|
||||
|
||||
(define-judgment-form nats
|
||||
#:mode (uses-ellipses I)
|
||||
[(uses-ellipses (n ...))
|
||||
(lt2 n) ...
|
||||
(sum z z z)])
|
||||
|
||||
(test (render-judgment-form uses-ellipses) "judgment-form-ellipsis.png"))
|
||||
|
||||
(let ()
|
||||
(define-language STLC
|
||||
|
|
|
|||
BIN
collects/redex/tests/bmps-macosx/judgment-form-ellipsis.png
Normal file
BIN
collects/redex/tests/bmps-macosx/judgment-form-ellipsis.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 2.6 KiB |
|
|
@ -1,12 +1,12 @@
|
|||
(#rx"input q at position 1"
|
||||
([judgment ctc-fail])
|
||||
(judgment-holds (judgment q s)))
|
||||
([judgment (ctc-fail q s)])
|
||||
(judgment-holds judgment))
|
||||
(#rx"output q at position 2"
|
||||
([judgment ctc-fail])
|
||||
(judgment-holds (judgment a s)))
|
||||
([judgment (ctc-fail a s)])
|
||||
(judgment-holds judgment))
|
||||
(#rx"input q at position 1"
|
||||
([judgment ctc-fail])
|
||||
(judgment-holds (judgment b s)))
|
||||
([judgment (ctc-fail b s)])
|
||||
(judgment-holds judgment))
|
||||
(#rx"output q at position 2"
|
||||
([judgment ctc-fail])
|
||||
(judgment-holds (judgment c s)))
|
||||
([judgment (ctc-fail c s)])
|
||||
(judgment-holds judgment))
|
||||
|
|
@ -0,0 +1,10 @@
|
|||
(#rx"incompatible ellipsis match counts"
|
||||
([premise (bad-zip ((any_1 any_i) ...))])
|
||||
([name bad-zip] [binder1 any_1] [binder2 any_i] [ellipsis ...])
|
||||
(let ()
|
||||
(define-language L)
|
||||
(define-judgment-form L
|
||||
#:mode (name I)
|
||||
[(name (binder1 ellipsis binder2 ellipsis))
|
||||
premise])
|
||||
(judgment-holds (name (1 2)))))
|
||||
|
|
@ -135,4 +135,31 @@
|
|||
(define-judgment-form syn-err-lang
|
||||
#:mode (uses-unquote I O)
|
||||
[(uses-unquote n unq)])
|
||||
(void)))
|
||||
|
||||
(#rx"missing ellipses"
|
||||
([use any_0]) ([ellipsis ...] [def any_0])
|
||||
(let ()
|
||||
(define-judgment-form syn-err-lang
|
||||
#:mode (tmpl-depth I O)
|
||||
[(tmpl-depth (def ellipsis) any)
|
||||
(tmpl-depth use any)])
|
||||
(void)))
|
||||
(#rx"same binder.*different depths"
|
||||
([binder1 any_0] [binder2 any_0])
|
||||
([ellipsis ...])
|
||||
(let ()
|
||||
(define-judgment-form syn-err-lang
|
||||
#:mode (pat-depth I O)
|
||||
[(pat-depth (binder2 ellipsis) ())
|
||||
(pat-depth () binder1)])
|
||||
(void)))
|
||||
(#rx"too many ellipses"
|
||||
([premise (no-ellipsis any)])
|
||||
([binder any] [name no-ellipsis] [ellipsis ...])
|
||||
(let ()
|
||||
(define-judgment-form syn-err-lang
|
||||
#:mode (name I)
|
||||
[(name binder)
|
||||
premise ellipsis])
|
||||
(void)))
|
||||
|
|
@ -1817,7 +1817,7 @@
|
|||
(--> a any
|
||||
(judgment-holds (R a any))))
|
||||
'a)
|
||||
'(b a)))
|
||||
'(a b)))
|
||||
|
||||
;
|
||||
;
|
||||
|
|
@ -1913,8 +1913,8 @@
|
|||
(test (judgment-holds (sumo n_1 n_2 z) ([,'n_1 n_1] [,'n_2 n_2]))
|
||||
(list (term ([n_1 z] [n_2 z]))))
|
||||
(test (judgment-holds (sumo n_1 n_2 (s z)) ([,'n_1 n_1] [,'n_2 n_2]))
|
||||
(list (term ([n_1 (s z)] [n_2 z]))
|
||||
(term ([n_1 z] [n_2 (s z)]))))
|
||||
(list (term ([n_1 z] [n_2 (s z)]))
|
||||
(term ([n_1 (s z)] [n_2 z]))))
|
||||
|
||||
(define-judgment-form nats
|
||||
#:mode (sumo-ls O O I)
|
||||
|
|
@ -1938,7 +1938,7 @@
|
|||
[(member n_i (n_0 ... n_i n_i+1 ...))])
|
||||
|
||||
(test (judgment-holds (member n (z (s z) z (s (s z)))) n)
|
||||
(list (term (s (s z))) (term z) (term (s z)) (term z)))
|
||||
(list (term z) (term (s z)) (term z) (term (s (s z)))))
|
||||
|
||||
(define-judgment-form nats
|
||||
#:mode (has-zero I)
|
||||
|
|
@ -1975,6 +1975,71 @@
|
|||
(test (judgment-holds (uses-add2 (s (s (s (s z)))) n) n)
|
||||
(list (term (s (s (s z))))))
|
||||
|
||||
(define-judgment-form nats
|
||||
#:mode (add1 I O)
|
||||
#:contract (add1 n n)
|
||||
[(add1 n (s n))])
|
||||
|
||||
(define-judgment-form nats
|
||||
#:mode (map-add1 I O)
|
||||
#:contract (map-add1 (n ...) (n ...))
|
||||
[(map-add1 (n ...) (n_+ ...))
|
||||
(add1 n n_+) ...])
|
||||
|
||||
(test (judgment-holds (map-add1 () (n ...))
|
||||
(n ...))
|
||||
(list (term ())))
|
||||
|
||||
(test (judgment-holds (map-add1 (z (s z) (s (s z))) (n ...))
|
||||
(n ...))
|
||||
(list (term ((s z) (s (s z)) (s (s (s z)))))))
|
||||
|
||||
(define-judgment-form nats
|
||||
#:mode (map-add1-check I O)
|
||||
#:contract (map-add1-check (n ...) (n ...))
|
||||
[(map-add1-check (n ...) ((s n) ...))
|
||||
(add1 n (s n)) ...])
|
||||
|
||||
(test (judgment-holds (map-add1-check (z (s z) (s (s z))) (n ...))
|
||||
(n ...))
|
||||
(list (term ((s z) (s (s z)) (s (s (s z)))))))
|
||||
|
||||
(define-judgment-form nats
|
||||
#:mode (add-some-noz I O)
|
||||
#:contract (add-some-noz n n)
|
||||
[(add-some-noz z z)]
|
||||
[(add-some-noz (s n) (s n))]
|
||||
[(add-some-noz (s n) (s (s n)))])
|
||||
|
||||
(define-judgment-form nats
|
||||
#:mode (map-add-some-noz I O)
|
||||
#:contract (map-add-some-noz (n ...) (n ...))
|
||||
[(map-add-some-noz (n ...) (n_+ ...))
|
||||
(add-some-noz n n_+) ...])
|
||||
|
||||
(test (judgment-holds (map-add-some-noz (z (s z) (s (s z))) (n ...))
|
||||
(n ...))
|
||||
(list (term (z (s (s z)) (s (s (s z)))))
|
||||
(term (z (s (s z)) (s (s z))))
|
||||
(term (z (s z) (s (s (s z)))))
|
||||
(term (z (s z) (s (s z))))))
|
||||
|
||||
(define-judgment-form nats
|
||||
#:mode (add-some I O)
|
||||
#:contract (add-some n n)
|
||||
[(add-some n n)]
|
||||
[(add-some n (s n))])
|
||||
|
||||
(define-judgment-form nats
|
||||
#:mode (map-add-some-one I O)
|
||||
#:contract (map-add-some-one (n ...) (n ...))
|
||||
[(map-add-some-one (n ...) ((s n) ...))
|
||||
(add-some n (s n)) ...])
|
||||
|
||||
(test (judgment-holds (map-add-some-one (z (s z) (s (s z))) (n ...))
|
||||
(n ...))
|
||||
(list (term ((s z) (s (s z)) (s (s (s z)))))))
|
||||
|
||||
(define-judgment-form nats
|
||||
#:mode (hyphens I)
|
||||
[(hyphens b)
|
||||
|
|
@ -2059,7 +2124,8 @@
|
|||
[(ctc-fail c s)
|
||||
(ctc-fail a s)]))
|
||||
(exec-runtime-error-tests "run-err-tests/judgment-form-contracts.rktd")
|
||||
(exec-runtime-error-tests "run-err-tests/judgment-form-undefined.rktd"))
|
||||
(exec-runtime-error-tests "run-err-tests/judgment-form-undefined.rktd")
|
||||
(exec-runtime-error-tests "run-err-tests/judgment-form-ellipses.rktd"))
|
||||
|
||||
(parameterize ([current-namespace (make-base-namespace)])
|
||||
(eval '(require redex/reduction-semantics))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user