From 87f35419792d273ae7220cd4fdc17b8aa93af818 Mon Sep 17 00:00:00 2001 From: Casey Klein Date: Wed, 10 Aug 2011 08:18:10 -0500 Subject: [PATCH] Adds support for ellipsis-repeated premises --- collects/redex/private/pict.rkt | 3 +- .../redex/private/reduction-semantics.rkt | 123 +++++++++++++----- collects/redex/redex.scrbl | 23 +++- collects/redex/tests/bitmap-test.rkt | 15 ++- .../bmps-macosx/judgment-form-ellipsis.png | Bin 0 -> 2695 bytes .../judgment-form-contracts.rktd | 16 +-- .../run-err-tests/judgment-form-ellipses.rktd | 10 ++ .../judgment-form-definition.rktd | 27 ++++ collects/redex/tests/tl-test.rkt | 76 ++++++++++- 9 files changed, 242 insertions(+), 51 deletions(-) create mode 100644 collects/redex/tests/bmps-macosx/judgment-form-ellipsis.png create mode 100644 collects/redex/tests/run-err-tests/judgment-form-ellipses.rktd diff --git a/collects/redex/private/pict.rkt b/collects/redex/private/pict.rkt index adfb89b40e..6e1e86db51 100644 --- a/collects/redex/private/pict.rkt +++ b/collects/redex/private/pict.rkt @@ -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) diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt index 7ea9c76ae8..88b1752716 100644 --- a/collects/redex/private/reduction-semantics.rkt +++ b/collects/redex/private/reduction-semantics.rkt @@ -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)) diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl index d78e710f6a..8a0818ea29 100644 --- a/collects/redex/redex.scrbl +++ b/collects/redex/redex.scrbl @@ -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[ diff --git a/collects/redex/tests/bitmap-test.rkt b/collects/redex/tests/bitmap-test.rkt index 068ac2e506..448de5d24f 100644 --- a/collects/redex/tests/bitmap-test.rkt +++ b/collects/redex/tests/bitmap-test.rkt @@ -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 diff --git a/collects/redex/tests/bmps-macosx/judgment-form-ellipsis.png b/collects/redex/tests/bmps-macosx/judgment-form-ellipsis.png new file mode 100644 index 0000000000000000000000000000000000000000..5d14087950c780050cb7360e117858c95713bb2b GIT binary patch literal 2695 zcmXX|2{=@38$QaGY}vobmMtdBG&C}@HW(U=FbLU(L@3#^wlT(%d=q6I%ZITJq6`t) zvX!W>FxD&$hWN=k`A`4#-{(5#J@0j{^PKm+pZmF=L&RE{@$o=-007`KN29KSV>x&# zaUTP(FdNlSaNzX3Vuk{a{u~9ZWh4OLxnzzqvWv)N<~m`7-Nf629GqnhPbJ!j+&Q!P z;Jzx)69vu_%Ft6Oq9XBJvhM8STIweXl-?_GpMaoKEdXuy=QxwG-97Pcwv({E zz0C+|CKCG|aS0@%iqg|h0fwq#z1`i4N=l3K^9_xSw5BFOA_{0v;5!Y4Lh*1XG#YJh zpMg=*)YL4-Dhm^8sMNUqt#T?g2*iyWWmKw07A7n#?Du5Zu9;0tvk(6uikFuc0J3v( zJS1KT4cs@By)R2CD)Q`oB9)n$dE-Ma zV{Pr%#)i|Ii1T??GSbrdT^w8I6crWU8r^e|`#lhYMkl7He_9;M(GD2Ldw6ts)?q9y z(=QJV4Z*WgEJ`Y1p>f*9#l>uFY&A7C92^`t9ByiA3Z8|LORpWfMMORP5fU1D;lhP8 z{kIUhT3R9xWs!NYYjhoO|Dxw`xdw4<_4RN?MUH`izZI|iVxg?9*S}Oc{IEN+@|J_r zT3S{ZjIoJ{iErNk;8oyc($@3LOeICdcmm-x1mc-0Cqx_>8IjhD+*%!bnJlhx{cUVs z=d8r((_V~^*Or%;cca@tionQpIz3a(`QPbj1DZJogTZ120a*isX*&Iqni?O_?(-51 zSBp_qRejgl$p)mRrkbTmx89z8n3p%X?$F~U1puH}-oHl&1+7ykl)=G4b1hIwp`oD; z)ayfd`1iTF$HucWGcyYNFU7>g#r^&LZ`@b{B?eApbi)R_y70lmTwGiz7#zO&^QR#m zl3E(V3BK|nPd6qyx~Qn=87D%xA60eSMg41UubG3x>(Wvm=6It8OH^DuCntxCom~ro z_&_#@>rN82u=F`|QL+XkPD6uAp(yL>M(u4b1Wmp9t4v;mXCWstGLljSCZ(A=Gvh8q z3|Z*UFes_oZI+Re0vFxb*ch`h7Y`-MKp++6l`B_Ho;oQ zdxv{>@%Z^NYw{Ee1y`}>>2*Qe&|$5T>L*f}}d z;*O*N7`XVlx;pQHOf{FL;r90X9q!RbzgwG|_ra1K-MZ@JbZ>u)@$$w;2m}%q{s-~` z95FF5s$wg>X)+K8+rAQeB;aRyeI4cu1D4uC8`0z7%`-?c+y*bX_D8 z)I_GbD{?`_hL7{ngAe+dRfv^;tM7({xHS4@fJjZXG&HOu=PQ6ia`nQ0uFo0@V0Gi#GA6R(5fHs^^w8KRnBsNA1-1D8fhu57+rUFswV z+(I}*Gy22%1qA*R@ur;r!WV{Tog*I~ACzBTae+vDv8peVJU%|2CS&jpmcs2AWfT{8 zbg;AT?Cjj_d0vh(yOLHLykOzr;2=a)m@coZ^!M>8?eT?Li30^xsz!s$%vh64TE|OJ9~GU^@Gt zqr*s&f9Ds|+3p8}(J_1b{YR>1FX(%}m=g|I?9B3V61T4k!45h!I4F|b4Y~7qcv#lW z$H~o&Od@%Cc--0Fx`}Fv-rLl2J*=jYxl>KO;91KoI$ZIP#R_MRo5%_ZcC@#H?Er~{ zNK3D+uTv{4D^F>FUJ35#>{+gxa^9Qj>gvg2YQ~Ql1_kBhsH%SN0?OcDfNX{ZC}1@; zH7QBStG2eE?ubAK9(iBnuXD`J&)0{+hDS!`W@l|&U6~BVO&=dIY3bk0iPu@&n0z|j z1tf4Nvn+73d3(Ik|9g^#mgCQw*tN6eF8Pj&yui1Xa1B!5rF)zBkdP1y3yWK~Ru%d; zm9=sc?VxJs&Iu=XU%q_V+uOUau&|?}Lq$a;O@9_3f-rmtmDbk=xtb1AsnRLy)^ImQ{hJ)z%8SMm>7;NE8B{#HG&} z0r$Z)VU+v>0`g+r9ow#5y9Qe3ut|hVcciIl&&*6gA~(sF(jd)ppIVrx`k&T z_u$~54-Zf4y}T_TdC^coNEDj$;zgCyOHP|kxE(}bU!RA!69A4qfU(+Z50g+ucl5F= z9LuhjN9()kIWJIJJww96jsa7xQ3NeU2(o@r8-d8o$T*Yd>gw9l)AKrLx-E1?Ogc@R zn;jhoHeM^MCm1E$|8a+9WFLVd?wSYN)I~`vRWW}BSiHaf^MUT~8(v;sXj=uL^gcXZ z#@xaJd3)ymILXD)(bwBM9&w>%u`-TIu%}hk4vvkEl1z&g&z?>0p3BeAPfSd#bfC^{ zM8x-RUa#fNNO=DADGY)5_tU5JygcT@LJ26(vG#eVwrHI!%o>wvl3ig}Rq1$hYIM{q zAfS2+{{@ef$^HDC-8m&;9$dj>P<4f6U7U1R8g24)~$}3-~W`Sc`LK3)1=EnElER2#IAt6CYK|!`2 zv}6|-dV70&6Dj!iZEk-4e3t|d(Cnyh-be=c{c0xT);w1Gz2m((e_{cYUa=#Q)YELHX)7KWGK zXt><&_oPkRO7`CPUeoV4DBe8cQoH)5naZ-!fH` zzJ7ke;o(ag5tuD2L|f*wQN`X6j;2ToOCD?I?O8(d-CYdZzf=FVuh+Pc7OO^oXi}D literal 0 HcmV?d00001 diff --git a/collects/redex/tests/run-err-tests/judgment-form-contracts.rktd b/collects/redex/tests/run-err-tests/judgment-form-contracts.rktd index aaf217461c..d0036e4b53 100644 --- a/collects/redex/tests/run-err-tests/judgment-form-contracts.rktd +++ b/collects/redex/tests/run-err-tests/judgment-form-contracts.rktd @@ -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))) \ No newline at end of file + ([judgment (ctc-fail c s)]) + (judgment-holds judgment)) \ No newline at end of file diff --git a/collects/redex/tests/run-err-tests/judgment-form-ellipses.rktd b/collects/redex/tests/run-err-tests/judgment-form-ellipses.rktd new file mode 100644 index 0000000000..33d7a6ccae --- /dev/null +++ b/collects/redex/tests/run-err-tests/judgment-form-ellipses.rktd @@ -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))))) \ No newline at end of file diff --git a/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd b/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd index 2c9a148fc2..ebbbdfeebc 100644 --- a/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd +++ b/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd @@ -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))) \ No newline at end of file diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt index 52f60f23ec..e2853ea061 100644 --- a/collects/redex/tests/tl-test.rkt +++ b/collects/redex/tests/tl-test.rkt @@ -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))