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

Change define-relation to compile to a judgment-form, instead of a metafunction.

Browse Source 
Also:
- remove the restriction on the use of unquote in define-judgment-form
- allows limited use (I modes only) of judgment-forms in terms
- allows the use of define-relation with the search/unification
  based random term generation
This commit is contained in:
Burke Fetscher 2012-11-29 17:17:34 -06:00
parent 0182a6c491
commit cf9b0f774b
13 changed files with 580 additions and 424 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
collects/redex/private/generate-term.rkt
View File

@ -322,7 +322,6 @@
(cond (cond
[(metafunc #'jf/mf-id) [(metafunc #'jf/mf-id)
(let () (let ()
(define relation? (term-fn-get-info (syntax-local-value #'jf/mf-id)))
(define (signal-error whatever) (define (signal-error whatever)
(when (stx-pair? whatever) (when (stx-pair? whatever)
(define cr (syntax-e (stx-car whatever))) (define cr (syntax-e (stx-car whatever)))
@ -334,28 +333,24 @@
(raise-syntax-error 'generate-term (raise-syntax-error 'generate-term
"expected a metafunction result and a size" "expected a metafunction result and a size"
stx)) stx))
(if relation? (let ([body-code
(raise-syntax-error 'generate-term (λ (res size)
"relations are not yet supported" #`(generate-mf-pat language (jf/mf-id . args) #,res #,size))])
stx) (syntax-case #'rest (=)
(let ([body-code [(= res)
(λ (res size) #`(λ (size)
#`(generate-mf-pat language (jf/mf-id . args) #,res #,size))]) #,(body-code #'res #'size))]
(syntax-case #'rest (=) [(= res size)
[(= res) (body-code #'res #'size)]
#`(λ (size) [(x . y)
#,(body-code #'res #'size))] (or (not (identifier? #'x))
[(= res size) (not (free-identifier=? #'= #'x)))
(body-code #'res #'size)] (raise-syntax-error 'generate-term
[(x . y) "expected to find ="
(or (not (identifier? #'x)) stx
(not (free-identifier=? #'= #'x))) #'x)]
(raise-syntax-error 'generate-term [whatever
"expected to find =" (signal-error #'whatever)])))]
stx
#'x)]
[whatever
(signal-error #'whatever)]))))]
[(judgment-form-id? #'jf/mf-id) [(judgment-form-id? #'jf/mf-id)
(syntax-case #'rest () (syntax-case #'rest ()
[() [()

476
collects/redex/private/judgment-form.rkt
View File

@ -45,10 +45,6 @@
(define-struct metafunc-extra-where (lhs rhs)) (define-struct metafunc-extra-where (lhs rhs))
(define-struct metafunc-extra-fresh (vars)) (define-struct metafunc-extra-fresh (vars))
(define-for-syntax (judgment-form-id? stx)
(and (identifier? stx)
(judgment-form? (syntax-local-value stx (λ () #f)))))
(begin-for-syntax (begin-for-syntax
;; pre: (judgment-form-id? stx) holds ;; pre: (judgment-form-id? stx) holds
(define (lookup-judgment-form-id stx) (define (lookup-judgment-form-id stx)
@ -179,7 +175,7 @@
#,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in) env))] #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in) env))]
[((judgment-holds j) . after) [((judgment-holds j) . after)
(loop (cons #'j #'after) to-not-be-in env)] (loop (cons #'j #'after) to-not-be-in env)]
[((form-name . pats) . after) [((form-name pats ...) . after)
(judgment-form-id? #'form-name) (judgment-form-id? #'form-name)
(let*-values ([(premise) (syntax-case stx () [(p . _) #'p])] (let*-values ([(premise) (syntax-case stx () [(p . _) #'p])]
[(rest-clauses under-ellipsis?) [(rest-clauses under-ellipsis?)
@ -192,7 +188,7 @@
[(mode) (judgment-form-mode judgment-form)] [(mode) (judgment-form-mode judgment-form)]
[(judgment-proc) (judgment-form-proc judgment-form)] [(judgment-proc) (judgment-form-proc judgment-form)]
[(input-template output-pre-pattern) [(input-template output-pre-pattern)
(let-values ([(in out) (split-by-mode (syntax->list #'pats) mode)]) (let-values ([(in out) (split-by-mode (syntax->list #'(pats ...)) mode)])
(if under-ellipsis? (if under-ellipsis?
(let ([ellipsis (syntax/loc premise (... ...))]) (let ([ellipsis (syntax/loc premise (... ...))])
(values #`(#,in #,ellipsis) #`(#,out #,ellipsis))) (values #`(#,in #,ellipsis) #`(#,out #,ellipsis)))
@ -336,14 +332,15 @@
(syntax-case judgment () (syntax-case judgment ()
[(form-name pat ...) [(form-name pat ...)
(judgment-form-id? #'form-name) (judgment-form-id? #'form-name)
(let ([expected (length (judgment-form-mode (lookup-judgment-form-id #'form-name)))] (unless (judgment-form-relation? (lookup-judgment-form-id #'form-name))
[actual (length (syntax->list #'(pat ...)))]) (let ([expected (length (judgment-form-mode (lookup-judgment-form-id #'form-name)))]
(unless (= actual expected) [actual (length (syntax->list #'(pat ...)))])
(raise-syntax-error (unless (= actual expected)
#f (raise-syntax-error
(format "mode specifies a ~a-ary relation but use supplied ~a term~a" #f
expected actual (if (= actual 1) "" "s")) (format "mode specifies a ~a-ary relation but use supplied ~a term~a"
judgment)))] expected actual (if (= actual 1) "" "s"))
judgment))))]
[(form-name pat ...) [(form-name pat ...)
(raise-syntax-error #f "expected a judgment form name" stx #'form-name)])) (raise-syntax-error #f "expected a judgment form name" stx #'form-name)]))
@ -373,7 +370,7 @@
(not-expression-context stx) (not-expression-context stx)
(syntax-case stx () (syntax-case stx ()
[(def-form-id lang . body) [(def-form-id lang . body)
(do-extended-judgment-form #'lang (syntax-e #'def-form-id) #'body #f stx)])) (do-extended-judgment-form #'lang (syntax-e #'def-form-id) #'body #f stx #f)]))
(define-syntax (define-extended-judgment-form stx) (define-syntax (define-extended-judgment-form stx)
(not-expression-context stx) (not-expression-context stx)
@ -385,9 +382,112 @@
"expected a judgment form" "expected a judgment form"
stx stx
#'original-id)) #'original-id))
(do-extended-judgment-form #'lang 'define-extended-judgment-form #'body #'original-id stx))])) (do-extended-judgment-form #'lang 'define-extended-judgment-form #'body #'original-id stx #f))]))
(define-for-syntax (do-extended-judgment-form lang syn-err-name body orig stx) (define-syntax (define-relation stx)
(syntax-case stx ()
[(def-form-id lang . body)
(let-values ([(contract-name dom-ctcs codom-contracts pats)
(split-out-contract stx (syntax-e #'def-form-id) #'body #t)])
(with-syntax* ([((name trms ...) rest ...) (car pats)]
[(mode-stx ...) #`(#:mode (name I))]
[(ctc-stx ...) (if dom-ctcs
(with-syntax ([(d-ctc ...) dom-ctcs])
#`(#:contract (name (d-ctc ...))))
#'())]
[(clauses ...) pats]
[new-body #`(mode-stx ... ctc-stx ... clauses ...)])
(do-extended-judgment-form #'lang (syntax-e #'def-form-id) #'new-body #f stx #t)))]))
(define-for-syntax (split-out-contract stx syn-error-name rest relation?)
;; initial test determines if a contract is specified or not
(cond
[(pair? (syntax-e (car (syntax->list rest))))
(values #f #f (list #'any) (check-clauses stx syn-error-name (syntax->list rest) relation?))]
[else
(syntax-case rest ()
[(id separator more ...)
(identifier? #'id)
(cond
[relation?
(let-values ([(contract clauses)
(parse-relation-contract #'(separator more ...) syn-error-name stx)])
(when (null? clauses)
(raise-syntax-error syn-error-name
"expected clause definitions to follow domain contract"
stx))
(values #'id contract (list #'any) (check-clauses stx syn-error-name clauses #t)))]
[else
(unless (eq? ': (syntax-e #'separator))
(raise-syntax-error syn-error-name "expected a colon to follow the meta-function's name" stx #'separator))
(let loop ([more (syntax->list #'(more ...))]
[dom-pats '()])
(cond
[(null? more)
(raise-syntax-error syn-error-name "expected an ->" stx)]
[(eq? (syntax-e (car more)) '->)
(define-values (raw-clauses rev-codomains)
(let loop ([prev (car more)]
[more (cdr more)]
[codomains '()])
(cond
[(null? more)
(raise-syntax-error syn-error-name "expected a range contract to follow" stx prev)]
[else
(define after-this-one (cdr more))
(cond
[(null? after-this-one)
(values null (cons (car more) codomains))]
[else
(define kwd (cadr more))
(cond
[(member (syntax-e kwd) '(or ∨ ∪))
(loop kwd
(cddr more)
(cons (car more) codomains))]
[else
(values (cdr more)
(cons (car more) codomains))])])])))
(let ([doms (reverse dom-pats)]
[clauses (check-clauses stx syn-error-name raw-clauses relation?)])
(values #'id doms (reverse rev-codomains) clauses))]
[else
(loop (cdr more) (cons (car more) dom-pats))]))])]
[_
(raise-syntax-error
syn-error-name
(format "expected the name of the ~a, followed by its contract (or no name and no contract)"
(if relation? "relation" "meta-function"))
stx
rest)])]))
(define-for-syntax (parse-relation-contract after-name syn-error-name orig-stx)
(syntax-case after-name ()
[(subset . rest-pieces)
(unless (memq (syntax-e #'subset) '(⊂ ⊆))
(raise-syntax-error syn-error-name
"expected ⊂ or ⊆ to follow the relation's name"
orig-stx #'subset))
(let ([more (syntax->list #'rest-pieces)])
(when (null? more)
(raise-syntax-error syn-error-name
(format "expected a sequence of patterns separated by x or × to follow ~a"
(syntax-e #'subset))
orig-stx
#'subset))
(let loop ([more (cdr more)]
[arg-pats (list (car more))])
(cond
[(and (not (null? more)) (memq (syntax-e (car more)) '(x ×)))
(when (null? (cdr more))
(raise-syntax-error syn-error-name
(format "expected a pattern to follow ~a" (syntax-e (car more)))
orig-stx (car more)))
(loop (cddr more)
(cons (cadr more) arg-pats))]
[else (values (reverse arg-pats) more)])))]))
(define-for-syntax (do-extended-judgment-form lang syn-err-name body orig stx is-relation?)
(define nts (definition-nts lang stx syn-err-name)) (define nts (definition-nts lang stx syn-err-name))
(define-values (judgment-form-name dup-form-names mode position-contracts clauses rule-names) (define-values (judgment-form-name dup-form-names mode position-contracts clauses rule-names)
(parse-judgment-form-body body syn-err-name stx (identifier? orig))) (parse-judgment-form-body body syn-err-name stx (identifier? orig)))
@ -395,30 +495,30 @@
#`(begin #`(begin
(define-syntax #,judgment-form-name (define-syntax #,judgment-form-name
(judgment-form '#,judgment-form-name '#,(cdr (syntax->datum mode)) #'judgment-form-runtime-proc (judgment-form '#,judgment-form-name '#,(cdr (syntax->datum mode)) #'judgment-form-runtime-proc
#'mk-judgment-form-proc #'#,lang #'judgment-form-lws #'mk-judgment-form-proc #'#,lang #'jf-lws
'#,rule-names #'judgment-runtime-gen-clauses #'mk-judgment-gen-clauses)) '#,rule-names #'judgment-runtime-gen-clauses #'mk-judgment-gen-clauses #'jf-term-proc #,is-relation?))
(define mk-judgment-form-proc (define-values (mk-judgment-form-proc mk-judgment-gen-clauses)
(compile-judgment-form-proc #,judgment-form-name #,mode #,lang #,clauses #,rule-names #,position-contracts #,orig #,stx #,syn-err-name)) (compile-judgment-form #,judgment-form-name #,mode #,lang #,clauses #,rule-names #,position-contracts
#,orig #,stx #,syn-err-name judgment-runtime-gen-clauses))
(define judgment-form-runtime-proc (mk-judgment-form-proc #,lang)) (define judgment-form-runtime-proc (mk-judgment-form-proc #,lang))
(define judgment-form-lws (define jf-lws (compiled-judgment-form-lws #,clauses #,judgment-form-name #,stx))
(compiled-judgment-form-lws #,clauses)) (define judgment-runtime-gen-clauses (mk-judgment-gen-clauses #,lang (λ () (judgment-runtime-gen-clauses))))
(define mk-judgment-gen-clauses (define jf-term-proc (make-jf-term-proc #,judgment-form-name #,syn-err-name #,lang #,nts #,mode))))
(compile-judgment-gen-clauses #,judgment-form-name #,mode #,lang
#,clauses #,position-contracts #,orig
#,stx #,syn-err-name judgment-runtime-gen-clauses))
(define judgment-runtime-gen-clauses (mk-judgment-gen-clauses #,lang (λ () (judgment-runtime-gen-clauses))))))
(syntax-property (syntax-property
(values ;prune-syntax (values ;prune-syntax
(if (eq? 'top-level (syntax-local-context)) (if (eq? 'top-level (syntax-local-context))
; Introduce the names before using them, to allow ; Introduce the names before using them, to allow
; judgment form definition at the top-level. ; judgment form definition at the top-level.
#`(begin #`(begin
(define-syntaxes (judgment-form-runtime-proc judgment-form-lws judgment-runtime-gen-clauses) (values)) (define-syntaxes (judgment-form-runtime-proc judgment-runtime-gen-clauses jf-term-proc jf-lws) (values))
#,definitions) #,definitions)
definitions)) definitions))
'disappeared-use 'disappeared-use
(map syntax-local-introduce dup-form-names))) (map syntax-local-introduce dup-form-names)))
(define-for-syntax (jf-is-relation? jf-id)
(judgment-form-relation? (lookup-judgment-form-id jf-id)))
(define-for-syntax (parse-judgment-form-body body syn-err-name full-stx extension?) (define-for-syntax (parse-judgment-form-body body syn-err-name full-stx extension?)
(define-syntax-class pos-mode (define-syntax-class pos-mode
#:literals (I O) #:literals (I O)
@ -467,22 +567,22 @@
rule:expr ...) rule:expr ...)
(let-values ([(name/mode mode) (let-values ([(name/mode mode)
(syntax-parse #'(mode ...) (syntax-parse #'(mode ...)
[((name the-mode ...)) (values #'name (car (syntax->list #'(mode ...))))] [((name the-mode ...)) (values #'name (car (syntax->list #'(mode ...))))]
[_ [_
(raise-syntax-error (raise-syntax-error
#f #f
(if (null? (syntax->list #'(mode ...))) (if (null? (syntax->list #'(mode ...)))
"expected definition to include a mode specification" "expected definition to include a mode specification"
"expected definition to include only one mode specification") "expected definition to include only one mode specification")
full-stx)])] full-stx)])]
[(name/ctc ctc) [(name/ctc ctc)
(syntax-parse #'(contract ...) (syntax-parse #'(contract ...)
[() (values #f #f)] [() (values #f #f)]
[((name . contract)) (values #'name (syntax->list #'contract))] [((name . contract)) (values #'name (syntax->list #'contract))]
[(_ . dups) [(_ . dups)
(raise-syntax-error (raise-syntax-error
syn-err-name "expected at most one contract specification" syn-err-name "expected at most one contract specification"
#f #f (syntax->list #'dups))])]) #f #f (syntax->list #'dups))])])
(define-values (parsed-rules rule-names) (parse-rules (syntax->list #'(rule ...)))) (define-values (parsed-rules rule-names) (parse-rules (syntax->list #'(rule ...))))
(values name/mode mode name/ctc ctc parsed-rules rule-names))])) (values name/mode mode name/ctc ctc parsed-rules rule-names))]))
(check-clauses full-stx syn-err-name rules #t) (check-clauses full-stx syn-err-name rules #t)
@ -545,12 +645,41 @@
the-name (list (car others)))) the-name (list (car others))))
(loop (cdr others))])))) (loop (cdr others))]))))
(define-syntax (make-jf-term-proc stx)
(syntax-case stx ()
[(_ jdg-name syn-err-name lang nts mode)
(if (member 'O (syntax->datum #'mode))
#'(λ (_)
(error 'syn-err-name "judgment forms with output mode positions cannot currently be used in term"))
(with-syntax* ([(binding ...) (generate-temporaries (cdr (syntax->list #'mode)))]
[(input) (generate-temporaries (list #'input))]
[body-stx (bind-withs #'syn-err-name '() #'lang (syntax->datum #'nts)
(if (jf-is-relation? #'jdg-name)
(list #'(jdg-name ((unquote-splicing input))))
(list #'(jdg-name (unquote binding) ...)))
'flatten
#`(list #t)
'()
'()
#f
#f)])
(if (jf-is-relation? #'jdg-name)
#`(λ (input)
(not (null? body-stx)))
#`(λ (input)
(call-with-values
(λ () (apply values input))
(λ (binding ...)
(not (null? body-stx))))))))]))
(define-syntax (judgment-holds/derivation stx) (define-syntax (judgment-holds/derivation stx)
(syntax-case stx () (syntax-case stx ()
[(_ stx-name derivation? judgment) [(_ stx-name derivation? judgment)
#`(not (null? #,(syntax/loc stx (judgment-holds/derivation stx-name derivation? judgment #t))))] #`(not (null? #,(syntax/loc stx (judgment-holds/derivation stx-name derivation? judgment #t))))]
[(_ stx-name derivation? (form-name . pats) tmpl) [(_ stx-name derivation? (form-name . pats) tmpl)
(judgment-form-id? #'form-name) (and (judgment-form-id? #'form-name)
(when (jf-is-relation? #'form-name)
(raise-syntax-error (syntax-e #'stx-name) "relations not allowed" #'form-name)))
(let* ([syn-err-name (syntax-e #'stx-name)] (let* ([syn-err-name (syntax-e #'stx-name)]
[lang (judgment-form-lang (lookup-judgment-form-id #'form-name))] [lang (judgment-form-lang (lookup-judgment-form-id #'form-name))]
[nts (definition-nts lang stx syn-err-name)] [nts (definition-nts lang stx syn-err-name)]
@ -676,8 +805,8 @@
(let (clause-proc-binding ... ...) (let (clause-proc-binding ... ...)
(let ([prev (orig-mk lang)]) (let ([prev (orig-mk lang)])
(λ (recur input init-jf-derivation-id) (λ (recur input init-jf-derivation-id)
(append (prev recur input init-jf-derivation-id) (append (prev recur input init-jf-derivation-id)
clause-proc-body-backwards ...)))))) clause-proc-body-backwards ...))))))
#`(λ (lang) #`(λ (lang)
(let (clause-proc-binding ... ...) (let (clause-proc-binding ... ...)
(λ (recur input init-jf-derivation-id) (λ (recur input init-jf-derivation-id)
@ -699,15 +828,47 @@
outputs] outputs]
[else '()])) [else '()]))
(define-for-syntax (do-compile-judgment-form-lws clauses) (define-for-syntax (do-compile-judgment-form-lws clauses jf-name-stx full-def)
(syntax-case clauses () (syntax-case clauses ()
[(((_ . conc-body) . prems) ...) [(((_ . conc-body) prems ...) ...)
(let ([rev-premss (with-syntax ([((rhss ...) (sc/ws ...)) (if (jf-is-relation? jf-name-stx)
; for consistency with metafunction extras (with-syntax ([(((rhses ...) (where/sc ...)) ...)
(for/list ([prems (syntax->list #'(prems ...))]) (relation-split-out-rhs #'((prems ...) ...) full-def)])
(reverse (syntax->list prems)))] #'(((rhses ...) ...) ((where/sc ...) ...)))
[no-rhss (map (λ (_) '()) clauses)]) (let ([rev-premss
#`(generate-lws #t (conc-body ...) #,(lhs-lws clauses) #,rev-premss #,no-rhss #f))])) ; for consistency with metafunction extras
(for/list ([prems (syntax->list #'((prems ...) ...))])
(reverse (syntax->list prems)))]
[no-rhss (map (λ (_) '()) clauses)])
(list no-rhss rev-premss)))])
#`(generate-lws #t (conc-body ...) #,(lhs-lws clauses) (sc/ws ...) (rhss ...) #f))]))
(define-for-syntax (relation-split-out-rhs raw-rhsss orig-stx)
(for/list ([rhss (in-list (syntax->list raw-rhsss))])
(define rhses '())
(define sc/wheres '())
(for ([rhs (in-list (syntax->list rhss))])
(define (found-one)
(set! sc/wheres (cons rhs sc/wheres)))
(syntax-case rhs (side-condition side-condition/hidden where where/hidden judgment-holds)
[(side-condition . stuff) (found-one)]
[(side-condition/hidden . stuff) (found-one)]
[(where . stuff) (found-one)]
[(where/hidden . stuff) (found-one)]
[(judgment-holds . stuff) (found-one)]
[_
(cond
[(null? sc/wheres)
(set! rhses (cons rhs rhses))]
[else
(raise-syntax-error 'define-relation
(format "found a '~a' clause not at the end; followed by a normal, right-hand side clause"
(syntax-e (car (syntax-e (car sc/wheres)))))
(last sc/wheres)
#f
(list rhs))])]))
(list (reverse rhses)
(reverse sc/wheres))))
(define (check-judgment-form-contract form-name term+trees contracts mode modes) (define (check-judgment-form-contract form-name term+trees contracts mode modes)
(define terms (if (eq? mode 'O) (define terms (if (eq? mode 'O)
@ -731,8 +892,6 @@
(define ((check-template bound-anywhere) temp bound) (define ((check-template bound-anywhere) temp bound)
(let check ([t temp]) (let check ([t temp])
(syntax-case t (unquote) (syntax-case t (unquote)
[(unquote . _)
(raise-syntax-error syn-err-name "unquote unsupported" t)]
[x [x
(identifier? #'x) (identifier? #'x)
(unless (cond [(free-id-table-ref bound-anywhere #'x #f) (unless (cond [(free-id-table-ref bound-anywhere #'x #f)
@ -752,9 +911,11 @@
(define (split-body judgment) (define (split-body judgment)
(syntax-case judgment () (syntax-case judgment ()
[(form-name . body) [(form-name . body)
(split-by-mode (syntax->list #'body) (if (judgment-form-relation? (lookup-judgment-form-id #'form-name))
(values (list) (list #'(body)))
(split-by-mode (syntax->list #'body)
(judgment-form-mode (judgment-form-mode
(lookup-judgment-form-id #'form-name)))])) (lookup-judgment-form-id #'form-name))))]))
(define (drop-ellipses prems) (define (drop-ellipses prems)
(syntax-case prems () (syntax-case prems ()
[() '()] [() '()]
@ -889,14 +1050,19 @@
(cons #'judgment visible)] (cons #'judgment visible)]
[_ (cons extra visible)]))) [_ (cons extra visible)])))
(define-syntax (compile-judgment-form-proc stx) (define-syntax (compile-judgment-form stx)
(syntax-case stx () (syntax-case stx ()
[(_ judgment-form-name mode-arg lang clauses rule-names ctcs orig full-def syn-err-name) [(_ judgment-form-name mode-arg lang raw-clauses rule-names ctcs orig full-def syn-err-name judgment-form-runtime-gen-clauses)
(let ([nts (definition-nts #'lang #'full-def (syntax-e #'syn-err-name))] (let ([nts (definition-nts #'lang #'full-def (syntax-e #'syn-err-name))]
[clauses (syntax->list #'clauses)] [rule-names (syntax->datum #'rule-names)]
[rule-names (syntax->datum #'rule-names)] [syn-err-name (syntax-e #'syn-err-name)]
[syn-err-name (syntax-e #'syn-err-name)]) [clauses (rewrite-relation-prems
(mode-check (cdr (syntax->datum #'mode-arg)) clauses nts syn-err-name stx) (if (jf-is-relation? #'judgment-form-name)
(fix-relation-clauses (syntax-e #'judgment-form-name) (syntax->list #'raw-clauses))
(syntax->list #'raw-clauses)))]
[mode (cdr (syntax->datum #'mode-arg))])
(unless (jf-is-relation? #'judgment-form-name)
(mode-check (cdr (syntax->datum #'mode-arg)) clauses nts syn-err-name stx))
(define contracts (syntax-case #'ctcs () (define contracts (syntax-case #'ctcs ()
[#f #f] [#f #f]
[(p ...) [(p ...)
@ -905,20 +1071,147 @@
(rewrite-side-conditions/check-errs nts #'syn-error-name #f pat)]) (rewrite-side-conditions/check-errs nts #'syn-error-name #f pat)])
#'pat)) #'pat))
(syntax->list #'(p ...)))])) (syntax->list #'(p ...)))]))
(do-compile-judgment-form-proc #'judgment-form-name (define proc-stx (do-compile-judgment-form-proc #'judgment-form-name
#'mode-arg #'mode-arg
clauses clauses
rule-names rule-names
contracts contracts
nts nts
#'orig #'orig
#'full-def #'full-def
syn-err-name))])) syn-err-name))
(define gen-stx (with-syntax* ([(comp-clauses ...)
(map (λ (c) (compile-gen-clause c mode nts syn-err-name
#'judgment-form-name #'lang))
clauses)])
(if (identifier? #'orig)
(with-syntax ([prev-mk (judgment-form-mk-gen-clauses (lookup-judgment-form-id #'orig))])
#`(λ (effective-lang judgment-form-runtime-gen-clauses)
(define mk-prev-clauses (prev-mk effective-lang judgment-form-runtime-gen-clauses))
(λ ()
(append
(mk-prev-clauses)
#,(check-pats
#'(list comp-clauses ...))))))
#`(λ (effective-lang judgment-form-runtime-gen-clauses)
(λ ()
#,(check-pats
#'(list comp-clauses ...)))))))
#`(values #,(do-compile-judgment-form-proc #'judgment-form-name
#'mode-arg
clauses
rule-names
contracts
nts
#'orig
#'full-def
syn-err-name)
#,(with-syntax* ([(comp-clauses ...)
(map (λ (c) (compile-gen-clause c mode nts syn-err-name
#'judgment-form-name #'lang))
clauses)])
(if (identifier? #'orig)
(with-syntax ([prev-mk (judgment-form-mk-gen-clauses (lookup-judgment-form-id #'orig))])
#`(λ (effective-lang judgment-form-runtime-gen-clauses)
(define mk-prev-clauses (prev-mk effective-lang judgment-form-runtime-gen-clauses))
(λ ()
(append
(mk-prev-clauses)
#,(check-pats
#'(list comp-clauses ...))))))
#`(λ (effective-lang judgment-form-runtime-gen-clauses)
(λ ()
#,(check-pats
#'(list comp-clauses ...))))))))]))
(define-for-syntax (rewrite-relation-prems clauses)
(map (λ (c)
(syntax-case c ()
[(conc prems ...)
(with-syntax ([(new-prems ...) (map (λ (p)
(syntax-case p ()
[(r-name rest ...)
(and (identifier? #'r-name)
(judgment-form-id? #'r-name)
(jf-is-relation? #'r-name))
#'(r-name (rest ...))]
[else
p]))
(syntax->list #'(prems ...)))])
#'(conc new-prems ...))]))
clauses))
(define-for-syntax (fix-relation-clauses name raw-clauses)
(map (λ (clause-stx)
(define (fix-rule rule-stx)
(syntax-case rule-stx ()
[(rule-name rest ...)
(and (identifier? #'rule-name)
(judgment-form-id? #'rule-name))
#'(rule-name rest ...)]
[rule
#'(side-condition rule)]))
(let loop ([c-stx clause-stx]
[new-c-stx '()]
[extra-stx '()])
(syntax-case c-stx ()
[()
(let* ([c-rev (reverse new-c-stx)]
[conclusion (syntax-case (car c-rev) ()
[(r-name rest ...)
#'(r-name (rest ...))])])
(with-syntax ([(cls ...) (cons conclusion (append (reverse extra-stx) (cdr c-rev)))])
#'(cls ...)))]
[((where ext-rest ...) rest ...)
(where-keyword? #'where)
(loop #'(rest ...)
new-c-stx
(cons #'(where ext-rest ...) extra-stx))]
[((side-con ext-rest ...) rest ...)
(side-condition-keyword? #'side-con)
(loop #'(rest ...)
new-c-stx
(cons #'(side-con (unquote ext-rest ...)) extra-stx))]
[(rule ellipsis rest ...)
(ellipsis? #'ellipsis)
(loop #'(rest ...)
(cons #'ellipsis (cons (fix-rule #'rule) new-c-stx))
extra-stx)]
[(rule rest ...)
(loop #'(rest ...)
(cons (fix-rule #'rule) new-c-stx)
extra-stx)])))
raw-clauses))
(define-syntax (compile-judgment-gen-clauses stx)
(syntax-case stx ()
[(_ judgment-form-name mode-arg lang clauses ctcs orig full-def syn-err-name judgment-form-runtime-gen-clauses)
(let ([clauses (syntax->list #'clauses)]
[nts (definition-nts #'lang #'full-def (syntax-e #'syn-err-name))]
[syn-err-name (syntax-e #'syn-err-name)]
[mode (cdr (syntax->datum #'mode-arg))])
(with-syntax* ([(comp-clauses ...)
(map (λ (c) (compile-gen-clause c mode nts syn-err-name
#'judgment-form-name #'lang))
clauses)])
(if (identifier? #'orig)
(with-syntax ([prev-mk (judgment-form-mk-gen-clauses (lookup-judgment-form-id #'orig))])
#`(λ (effective-lang judgment-form-runtime-gen-clauses)
(define mk-prev-clauses (prev-mk effective-lang judgment-form-runtime-gen-clauses))
(λ ()
(append
(mk-prev-clauses)
#,(check-pats
#'(list comp-clauses ...))))))
#`(λ (effective-lang judgment-form-runtime-gen-clauses)
(λ ()
#,(check-pats
#'(list comp-clauses ...)))))))]))
(define-syntax (compiled-judgment-form-lws stx) (define-syntax (compiled-judgment-form-lws stx)
(syntax-case stx () (syntax-case stx ()
[(_ clauses) [(_ clauses name def-stx)
(do-compile-judgment-form-lws (syntax->list #'clauses))])) (do-compile-judgment-form-lws (syntax->list #'clauses) #'name #'def-stx)]))
(define-for-syntax (extract-term-let-binds lhs) (define-for-syntax (extract-term-let-binds lhs)
(let loop ([lhs lhs]) (let loop ([lhs lhs])
@ -1044,32 +1337,6 @@
; ;
(define-syntax (compile-judgment-gen-clauses stx)
(syntax-case stx ()
[(_ judgment-form-name mode-arg lang clauses ctcs orig full-def syn-err-name judgment-form-runtime-gen-clauses)
(let ([clauses (syntax->list #'clauses)]
[nts (definition-nts #'lang #'full-def (syntax-e #'syn-err-name))]
[syn-err-name (syntax-e #'syn-err-name)]
[mode (cdr (syntax->datum #'mode-arg))])
(with-syntax* ([(comp-clauses ...)
(map (λ (c) (compile-gen-clause c mode nts syn-err-name
#'judgment-form-name #'lang))
clauses)])
(if (identifier? #'orig)
(with-syntax ([prev-mk (judgment-form-mk-gen-clauses (lookup-judgment-form-id #'orig))])
#`(λ (effective-lang judgment-form-runtime-gen-clauses)
(define mk-prev-clauses (prev-mk effective-lang judgment-form-runtime-gen-clauses))
(λ ()
(append
(mk-prev-clauses)
#,(check-pats
#'(list comp-clauses ...))))))
#`(λ (effective-lang judgment-form-runtime-gen-clauses)
(λ ()
#,(check-pats
#'(list comp-clauses ...)))))))]))
(define-for-syntax (compile-gen-clause clause-stx mode nts syn-error-name jdg-name lang) (define-for-syntax (compile-gen-clause clause-stx mode nts syn-error-name jdg-name lang)
@ -1201,6 +1468,7 @@
#f])) #f]))
(provide define-judgment-form (provide define-judgment-form
define-relation
define-extended-judgment-form define-extended-judgment-form
judgment-holds judgment-holds
build-derivations build-derivations
@ -1216,7 +1484,8 @@
ellipsis? ellipsis?
visible-extras visible-extras
judgment-form-id? judgment-form-id?
lookup-judgment-form-id)) lookup-judgment-form-id
split-out-contract))
(provide --> fresh with I O ;; macro keywords (provide --> fresh with I O ;; macro keywords
@ -1236,4 +1505,5 @@
rewrite-prems rewrite-prems
with-syntax* with-syntax*
definition-nts definition-nts
check-pats)) check-pats
relation-split-out-rhs))

37
collects/redex/private/pict.rkt
View File

@ -779,12 +779,8 @@
(define-syntax (render-relation stx) (define-syntax (render-relation stx)
(syntax-case stx () (syntax-case stx ()
[(form name) [(form rest ...)
(identifier? #'name) #'(render-judgment-form rest ...)]))
#'(render-relation/proc 'form (metafunction name) #f)]
[(form name #:file filename)
(identifier? #'name)
#'(render-relation/proc 'form (metafunction name) filename)]))
(define linebreaks (make-parameter #f)) (define linebreaks (make-parameter #f))
@ -845,9 +841,6 @@
(cons (car l) (loop (cdr l)))]))) (cons (car l) (loop (cdr l)))])))
(define (metafunctions->pict/proc mfs name) (define (metafunctions->pict/proc mfs name)
(for ([mf (in-list mfs)])
(when (metafunc-proc-relation? (metafunction-proc mf))
(error name "expected metafunction as argument, got a relation")))
(unless (andmap (λ (mf) (eq? (metafunc-proc-lang (metafunction-proc (car mfs))) (unless (andmap (λ (mf) (eq? (metafunc-proc-lang (metafunction-proc (car mfs)))
(metafunc-proc-lang (metafunction-proc mf)))) (metafunc-proc-lang (metafunction-proc mf))))
mfs) mfs)
@ -1066,19 +1059,6 @@
(parameterize ([dc-for-text-size (make-object bitmap-dc% (make-object bitmap% 1 1))]) (parameterize ([dc-for-text-size (make-object bitmap-dc% (make-object bitmap% 1 1))])
(metafunctions->pict/proc mfs name))])) (metafunctions->pict/proc mfs name))]))
(define (render-relation/proc form mf filename)
(render-pict (λ () (inference-rules-pict/relation form mf))
filename))
(define (inference-rules-pict/relation form mf)
(unless (metafunc-proc-relation? (metafunction-proc mf))
(error form "expected relation as argument, got a metafunction"))
(inference-rules-pict (metafunc-proc-name (metafunction-proc mf))
(metafunc-proc-pict-info (metafunction-proc mf))
(map (λ (x) #f) (metafunc-proc-pict-info (metafunction-proc mf)))
(metafunc-proc-lang (metafunction-proc mf))
#f))
(define (render-pict make-pict filename) (define (render-pict make-pict filename)
(cond (cond
[filename [filename
@ -1169,12 +1149,15 @@
(define-for-syntax (inference-rules-pict/judgment-form form-name) (define-for-syntax (inference-rules-pict/judgment-form form-name)
(define jf (syntax-local-value form-name)) (define jf (syntax-local-value form-name))
(define-values (name lws rule-names lang relation?)
(values (judgment-form-name jf) (judgment-form-lws jf) (judgment-form-rule-names jf)
(judgment-form-lang jf) (judgment-form-relation? jf)))
(syntax-property (syntax-property
#`(inference-rules-pict '#,(judgment-form-name jf) #`(inference-rules-pict '#,name
#,(judgment-form-lws jf) #,lws
'#,(judgment-form-rule-names jf) '#,rule-names
#,(judgment-form-lang jf) #,lang
#t) #,(not relation?))
'disappeared-use 'disappeared-use
(syntax-local-introduce form-name))) (syntax-local-introduce form-name)))

214
collects/redex/private/reduction-semantics.rkt
View File

@ -1117,29 +1117,21 @@
(define-syntax (define-metafunction stx) (define-syntax (define-metafunction stx)
(syntax-case stx () (syntax-case stx ()
[(_ . rest) [(_ . rest)
(internal-define-metafunction stx #f #'rest #f)])) (internal-define-metafunction stx #f #'rest)]))
(define-syntax (define-relation stx)
(syntax-case stx ()
[(_ . rest)
;; need to rule out the contracts for this one
(internal-define-metafunction stx #f #'rest #t)]))
(define-syntax (define-metafunction/extension stx) (define-syntax (define-metafunction/extension stx)
(syntax-case stx () (syntax-case stx ()
[(_ prev . rest) [(_ prev . rest)
(identifier? #'prev) (identifier? #'prev)
(internal-define-metafunction stx #'prev #'rest #f)])) (internal-define-metafunction stx #'prev #'rest)]))
(define-for-syntax (internal-define-metafunction orig-stx prev-metafunction stx relation?) (define-for-syntax (internal-define-metafunction orig-stx prev-metafunction stx)
(not-expression-context orig-stx) (not-expression-context orig-stx)
(syntax-case stx () (syntax-case stx ()
[(lang . rest) [(lang . rest)
(let ([syn-error-name (if relation? (let ([syn-error-name (if prev-metafunction
'define-relation 'define-metafunction/extension
(if prev-metafunction 'define-metafunction)])
'define-metafunction/extension
'define-metafunction))])
;; keep this near the beginning, so it signals the first error (PR 10062) ;; keep this near the beginning, so it signals the first error (PR 10062)
(definition-nts #'lang orig-stx syn-error-name) (definition-nts #'lang orig-stx syn-error-name)
(when (null? (syntax-e #'rest)) (when (null? (syntax-e #'rest))
@ -1150,7 +1142,7 @@
(λ () (λ ()
(raise-syntax-error syn-error-name "expected a previously defined metafunction" orig-stx prev-metafunction)))) (raise-syntax-error syn-error-name "expected a previously defined metafunction" orig-stx prev-metafunction))))
(let*-values ([(contract-name dom-ctcs codom-contracts pats) (let*-values ([(contract-name dom-ctcs codom-contracts pats)
(split-out-contract orig-stx syn-error-name #'rest relation?)] (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)))
(raise-syntax-error syn-error-name (raise-syntax-error syn-error-name
@ -1169,9 +1161,8 @@
#,dom-ctcs #,dom-ctcs
#,codom-contracts #,codom-contracts
#,pats #,pats
#,relation?
#,syn-error-name)) #,syn-error-name))
(term-define-fn name name2 #,relation?))]) (term-define-fn name name2))])
(if (eq? 'top-level (syntax-local-context)) (if (eq? 'top-level (syntax-local-context))
; Introduce the names before using them, to allow ; Introduce the names before using them, to allow
; metafunction definition at the top-level. ; metafunction definition at the top-level.
@ -1181,52 +1172,19 @@
defs)) defs))
(syntax defs))))))])) (syntax defs))))))]))
(define-for-syntax (relation-split-out-rhs raw-rhsss orig-stx)
(for/list ([rhss (in-list (syntax->list raw-rhsss))])
(define rhses '())
(define sc/wheres '())
(for ([rhs (in-list (syntax->list rhss))])
(define (found-one)
(set! sc/wheres (cons rhs sc/wheres)))
(syntax-case rhs (side-condition side-condition/hidden where where/hidden judgment-holds)
[(side-condition . stuff) (found-one)]
[(side-condition/hidden . stuff) (found-one)]
[(where . stuff) (found-one)]
[(where/hidden . stuff) (found-one)]
[(judgment-holds . stuff) (found-one)]
[_
(cond
[(null? sc/wheres)
(set! rhses (cons rhs rhses))]
[else
(raise-syntax-error 'define-relation
(format "found a '~a' clause not at the end; followed by a normal, right-hand side clause"
(syntax-e (car (syntax-e (car sc/wheres)))))
(last sc/wheres)
#f
(list rhs))])]))
(list (reverse rhses)
(reverse sc/wheres))))
(define-syntax (generate-metafunction stx) (define-syntax (generate-metafunction stx)
(syntax-case stx () (syntax-case stx ()
[(_ orig-stx lang prev-metafunction name name-predicate dom-ctcs codom-contracts pats relation? syn-error-name) [(_ orig-stx lang prev-metafunction name name-predicate dom-ctcs codom-contracts pats syn-error-name)
(let ([prev-metafunction (and (syntax-e #'prev-metafunction) #'prev-metafunction)] (let ([prev-metafunction (and (syntax-e #'prev-metafunction) #'prev-metafunction)]
[dom-ctcs (syntax-e #'dom-ctcs)] [dom-ctcs (syntax-e #'dom-ctcs)]
[codom-contracts (syntax-e #'codom-contracts)] [codom-contracts (syntax-e #'codom-contracts)]
[pats (syntax-e #'pats)] [pats (syntax-e #'pats)]
[relation? (syntax-e #'relation?)]
[syn-error-name (syntax-e #'syn-error-name)]) [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]
[(lhs-for-lw ...) (lhs-lws pats)]) [(lhs-for-lw ...) (lhs-lws pats)])
(with-syntax ([((rhs stuff ...) ...) (if relation? (with-syntax ([((rhs stuff ...) ...) #'((raw-rhses ...) ...)]
(with-syntax ([(((rhses ...) (where/sc ...)) ...)
(relation-split-out-rhs #'((raw-rhses ...) ...)
#'orig-stx)])
#'(((AND rhses ...) where/sc ...) ...))
#'((raw-rhses ...) ...))]
[(lhs ...) #'((lhs-clauses ...) ...)]) [(lhs ...) #'((lhs-clauses ...) ...)])
(parse-extras #'((stuff ...) ...)) (parse-extras #'((stuff ...) ...))
(with-syntax ([((side-conditions-rewritten lhs-names lhs-namess/ellipses) ...) (with-syntax ([((side-conditions-rewritten lhs-names lhs-namess/ellipses) ...)
@ -1301,30 +1259,24 @@
(map (λ (names names/ellipses rhs/where) (map (λ (names names/ellipses rhs/where)
(with-syntax ([(names ...) names] (with-syntax ([(names ...) names]
[(names/ellipses ...) names/ellipses] [(names/ellipses ...) names/ellipses]
[rhs/where rhs/where] [rhs/where rhs/where])
[relation? relation?])
(syntax (syntax
(λ (name bindings) (λ (name bindings)
(term-let-fn ((name name relation?)) (term-let-fn ((name name))
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...) (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
rhs/where)))))) rhs/where))))))
(syntax->list #'(lhs-names ...)) (syntax->list #'(lhs-names ...))
(syntax->list #'(lhs-namess/ellipses ...)) (syntax->list #'(lhs-namess/ellipses ...))
(syntax->list (syntax (rhs/wheres ...))))] (syntax->list (syntax (rhs/wheres ...))))]
[((gen-clause lhs-pat) ...) [((gen-clause lhs-pat) ...)
(if relation? (make-mf-clauses (syntax->list #'(lhs ...))
(make-rl-clauses (syntax->list #'(lhs ...)) (syntax->list #'(rhs ...))
(syntax->list #'((raw-rhses ...) ...)) (syntax->list #'((stuff ...) ...))
lang-nts syn-error-name #'name #'lang) lang-nts syn-error-name #'name #'lang)])
(make-mf-clauses (syntax->list #'(lhs ...))
(syntax->list #'(rhs ...))
(syntax->list #'((stuff ...) ...))
lang-nts syn-error-name #'name #'lang))])
(syntax-property (syntax-property
(prune-syntax (prune-syntax
#`(let ([sc `(side-conditions-rewritten ...)] #`(let ([sc `(side-conditions-rewritten ...)]
[dsc `dom-side-conditions-rewritten]) [dsc `dom-side-conditions-rewritten])
;(printf "rhs/ws: ~s\rg-rhs/ws: ~s\n" '(rhs/wheres ...) '(rg-rhs/wheres ...))
(let ([cases (map (λ (pat rhs-fn rg-lhs src) (let ([cases (map (λ (pat rhs-fn rg-lhs src)
(make-metafunc-case (make-metafunc-case
(λ (effective-lang) (compile-pattern effective-lang pat #t)) (λ (effective-lang) (compile-pattern effective-lang pat #t))
@ -1346,13 +1298,11 @@
(λ (f/dom) (λ (f/dom)
(make-metafunc-proc (make-metafunc-proc
(let ([name (lambda (x) (f/dom x))]) name) (let ([name (lambda (x) (f/dom x))]) name)
(generate-lws #,relation? (generate-lws #f
(lhs ...) (lhs ...)
(lhs-for-lw ...) (lhs-for-lw ...)
((stuff ...) ...) ((stuff ...) ...)
#,(if relation? (rhs ...)
#'((raw-rhses ...) ...)
#'(rhs ...))
#t) #t)
lang lang
#t ;; multi-args? #t ;; multi-args?
@ -1360,11 +1310,7 @@
(let ([name (lambda (x) (name-predicate x))]) name) (let ([name (lambda (x) (name-predicate x))]) name)
dsc dsc
(append cases parent-cases) (append cases parent-cases)
#,relation?
#,(cond #,(cond
[relation?
#'(λ ()
(error 'define-relation "not yet supported by generation"))]
[prev-metafunction [prev-metafunction
#`(extend-mf-clauses #,(term-fn-get-id (syntax-local-value prev-metafunction)) #`(extend-mf-clauses #,(term-fn-get-id (syntax-local-value prev-metafunction))
(λ () (λ ()
@ -1380,8 +1326,7 @@
#`new-lhs-pats))) #`new-lhs-pats)))
#,(if dom-ctcs #'dsc #f) #,(if dom-ctcs #'dsc #f)
`(codom-side-conditions-rewritten ...) `(codom-side-conditions-rewritten ...)
'name 'name))))
#,relation?))))
'disappeared-use 'disappeared-use
(map syntax-local-introduce (map syntax-local-introduce
(syntax->list #'(original-names ...))))))))))])) (syntax->list #'(original-names ...))))))))))]))
@ -1479,67 +1424,6 @@
the-name (list (car others)))) the-name (list (car others))))
(loop (cdr others))])))) (loop (cdr others))]))))
(define-for-syntax (split-out-contract stx syn-error-name rest relation?)
;; initial test determines if a contract is specified or not
(cond
[(pair? (syntax-e (car (syntax->list rest))))
(values #f #f (list #'any) (check-clauses stx syn-error-name (syntax->list rest) relation?))]
[else
(syntax-case rest ()
[(id separator more ...)
(identifier? #'id)
(cond
[relation?
(let-values ([(contract clauses)
(parse-relation-contract #'(separator more ...) syn-error-name stx)])
(when (null? clauses)
(raise-syntax-error syn-error-name
"expected clause definitions to follow domain contract"
stx))
(values #'id contract (list #'any) (check-clauses stx syn-error-name clauses #t)))]
[else
(unless (eq? ': (syntax-e #'separator))
(raise-syntax-error syn-error-name "expected a colon to follow the meta-function's name" stx #'separator))
(let loop ([more (syntax->list #'(more ...))]
[dom-pats '()])
(cond
[(null? more)
(raise-syntax-error syn-error-name "expected an ->" stx)]
[(eq? (syntax-e (car more)) '->)
(define-values (raw-clauses rev-codomains)
(let loop ([prev (car more)]
[more (cdr more)]
[codomains '()])
(cond
[(null? more)
(raise-syntax-error syn-error-name "expected a range contract to follow" stx prev)]
[else
(define after-this-one (cdr more))
(cond
[(null? after-this-one)
(values null (cons (car more) codomains))]
[else
(define kwd (cadr more))
(cond
[(member (syntax-e kwd) '(or ∨ ∪))
(loop kwd
(cddr more)
(cons (car more) codomains))]
[else
(values (cdr more)
(cons (car more) codomains))])])])))
(let ([doms (reverse dom-pats)]
[clauses (check-clauses stx syn-error-name raw-clauses relation?)])
(values #'id doms (reverse rev-codomains) clauses))]
[else
(loop (cdr more) (cons (car more) dom-pats))]))])]
[_
(raise-syntax-error
syn-error-name
(format "expected the name of the ~a, followed by its contract (or no name and no contract)"
(if relation? "relation" "meta-function"))
stx
rest)])]))
(define-for-syntax (parse-extras extras) (define-for-syntax (parse-extras extras)
(for-each (for-each
@ -1575,33 +1459,8 @@
(syntax->list stuffs))) (syntax->list stuffs)))
(syntax->list extras))) (syntax->list extras)))
(define-for-syntax (parse-relation-contract after-name syn-error-name orig-stx)
(syntax-case after-name ()
[(subset . rest-pieces)
(unless (memq (syntax-e #'subset) '(⊂ ⊆))
(raise-syntax-error syn-error-name
"expected ⊂ or ⊆ to follow the relation's name"
orig-stx #'subset))
(let ([more (syntax->list #'rest-pieces)])
(when (null? more)
(raise-syntax-error syn-error-name
(format "expected a sequence of patterns separated by x or × to follow ~a"
(syntax-e #'subset))
orig-stx
#'subset))
(let loop ([more (cdr more)]
[arg-pats (list (car more))])
(cond
[(and (not (null? more)) (memq (syntax-e (car more)) '(x ×)))
(when (null? (cdr more))
(raise-syntax-error syn-error-name
(format "expected a pattern to follow ~a" (syntax-e (car more)))
orig-stx (car more)))
(loop (cddr more)
(cons (cadr more) arg-pats))]
[else (values (reverse arg-pats) more)])))]))
(define (build-metafunction lang cases parent-cases wrap dom-contract-pat codom-contract-pats name relation?) (define (build-metafunction lang cases parent-cases wrap dom-contract-pat codom-contract-pats 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)]
@ -1609,7 +1468,6 @@
[lhss-at-lang (map (λ (case) ((metafunc-case-lhs case) lang)) all-cases)] [lhss-at-lang (map (λ (case) ((metafunc-case-lhs case) lang)) all-cases)]
[rhss-at-lang (map (λ (case) ((metafunc-case-rhs case) lang)) all-cases)] [rhss-at-lang (map (λ (case) ((metafunc-case-rhs case) lang)) all-cases)]
[ids (map metafunc-case-id all-cases)]) [ids (map metafunc-case-id all-cases)])
;(printf "all-cases: ~s\nhsss: ~s\nrhsss: ~s\nids: ~s\n" all-cases lhss-at-lang rhss-at-lang ids)
(values (values
(wrap (wrap
(letrec ([cache (make-hash)] (letrec ([cache (make-hash)]
@ -1648,11 +1506,7 @@
[num (- (length parent-cases))]) [num (- (length parent-cases))])
(cond (cond
[(null? ids) [(null? ids)
(if relation? (redex-error name "no clauses matched for ~s" `(,name . ,exp))]
(begin
(cache-result exp #f #f)
#f)
(redex-error name "no clauses matched for ~s" `(,name . ,exp)))]
[else [else
(let ([pattern (car lhss)] (let ([pattern (car lhss)]
[rhs (car rhss)] [rhs (car rhss)]
@ -1661,22 +1515,6 @@
(let ([mtchs (match-pattern pattern exp)]) (let ([mtchs (match-pattern pattern exp)])
(cond (cond
[(not mtchs) (continue)] [(not mtchs) (continue)]
[relation?
(let ([ans
(ormap (λ (mtch)
(define rhs-ans (rhs traced-metafunc (mtch-bindings mtch)))
(and rhs-ans (ormap values rhs-ans)))
mtchs)])
(unless (ormap (λ (codom-compiled-pattern) (match-pattern codom-compiled-pattern ans))
codom-compiled-patterns)
(redex-error name "codomain test failed for ~s, call was ~s" ans `(,name ,@exp)))
(cond
[ans
(cache-result exp #t id)
(log-coverage id)
#t]
[else
(continue)]))]
[else [else
(let ([anss (apply append (let ([anss (apply append
(filter values (filter values
@ -2462,7 +2300,6 @@
metafunc-proc-in-dom? metafunc-proc-in-dom?
metafunc-proc-dom-pat metafunc-proc-dom-pat
metafunc-proc-cases metafunc-proc-cases
metafunc-proc-relation?
metafunc-proc? metafunc-proc?
(struct-out metafunc-case) (struct-out metafunc-case)
@ -2502,12 +2339,3 @@
coverage?) coverage?)
(provide do-test-match) (provide do-test-match)
;; the AND metafunction is defined here to be used
;; in define-relation so that ellipses work properly
;; across clauses in relations
(define-language and-L)
(define-metafunction and-L
AND : any ... -> any
[(AND any ...)
,(andmap values (term (any ...)))])

14
collects/redex/private/term-fn.rkt
View File

@ -4,7 +4,6 @@
(provide make-term-fn (provide make-term-fn
term-fn? term-fn?
term-fn-get-id term-fn-get-id
term-fn-get-info
(struct-out term-id) (struct-out term-id)
(struct-out judgment-form) (struct-out judgment-form)
@ -21,7 +20,6 @@
metafunc-proc-in-dom? metafunc-proc-in-dom?
metafunc-proc-dom-pat metafunc-proc-dom-pat
metafunc-proc-cases metafunc-proc-cases
metafunc-proc-relation?
metafunc-proc-gen-clauses metafunc-proc-gen-clauses
metafunc-proc-lhs-pats metafunc-proc-lhs-pats
metafunc-proc? metafunc-proc?
@ -32,9 +30,8 @@
pattern-symbols) pattern-symbols)
(define-values (struct-type make-term-fn term-fn? term-fn-get term-fn-set!) (define-values (struct-type make-term-fn term-fn? term-fn-get term-fn-set!)
(make-struct-type 'term-fn #f 2 0)) (make-struct-type 'term-fn #f 1 0))
(define term-fn-get-id (make-struct-field-accessor term-fn-get 0)) (define term-fn-get-id (make-struct-field-accessor term-fn-get 0))
(define term-fn-get-info (make-struct-field-accessor term-fn-get 1))
(define-struct term-id (id depth)) (define-struct term-id (id depth))
@ -43,7 +40,7 @@
(cond [(syntax-local-value stx (λ () #f)) => p?] (cond [(syntax-local-value stx (λ () #f)) => p?]
[else #f]))) [else #f])))
(define-struct judgment-form (name mode proc mk-proc lang lws rule-names gen-clauses mk-gen-clauses) (define-struct judgment-form (name mode proc mk-proc lang lws rule-names gen-clauses mk-gen-clauses term-proc relation?)
#:transparent) #:transparent)
(define-struct defined-term (value)) (define-struct defined-term (value))
@ -75,7 +72,7 @@
variable-not-otherwise-mentioned hole symbol)) variable-not-otherwise-mentioned hole symbol))
(define-values (struct:metafunc-proc make-metafunc-proc metafunc-proc? metafunc-proc-ref metafunc-proc-set!) (define-values (struct:metafunc-proc make-metafunc-proc metafunc-proc? metafunc-proc-ref metafunc-proc-set!)
(make-struct-type 'metafunc-proc #f 11 0 #f null (current-inspector) 0)) (make-struct-type 'metafunc-proc #f 10 0 #f null (current-inspector) 0))
(define metafunc-proc-pict-info (make-struct-field-accessor metafunc-proc-ref 1)) (define metafunc-proc-pict-info (make-struct-field-accessor metafunc-proc-ref 1))
(define metafunc-proc-lang (make-struct-field-accessor metafunc-proc-ref 2)) (define metafunc-proc-lang (make-struct-field-accessor metafunc-proc-ref 2))
(define metafunc-proc-multi-arg? (make-struct-field-accessor metafunc-proc-ref 3)) (define metafunc-proc-multi-arg? (make-struct-field-accessor metafunc-proc-ref 3))
@ -83,6 +80,5 @@
(define metafunc-proc-in-dom? (make-struct-field-accessor metafunc-proc-ref 5)) (define metafunc-proc-in-dom? (make-struct-field-accessor metafunc-proc-ref 5))
(define metafunc-proc-dom-pat (make-struct-field-accessor metafunc-proc-ref 6)) (define metafunc-proc-dom-pat (make-struct-field-accessor metafunc-proc-ref 6))
(define metafunc-proc-cases (make-struct-field-accessor metafunc-proc-ref 7)) (define metafunc-proc-cases (make-struct-field-accessor metafunc-proc-ref 7))
(define metafunc-proc-relation? (make-struct-field-accessor metafunc-proc-ref 8)) (define metafunc-proc-gen-clauses (make-struct-field-accessor metafunc-proc-ref 8))
(define metafunc-proc-gen-clauses (make-struct-field-accessor metafunc-proc-ref 9)) (define metafunc-proc-lhs-pats (make-struct-field-accessor metafunc-proc-ref 9))
(define metafunc-proc-lhs-pats (make-struct-field-accessor metafunc-proc-ref 10))

57
collects/redex/private/term.rkt
View File

@ -18,7 +18,8 @@
term/nts term/nts
(for-syntax term-rewrite (for-syntax term-rewrite
term-temp->pat term-temp->pat
currently-expanding-term-fn)) currently-expanding-term-fn
judgment-form-id?))
(define-syntax (hole stx) (raise-syntax-error 'hole "used outside of term")) (define-syntax (hole stx) (raise-syntax-error 'hole "used outside of term"))
(define-syntax (in-hole stx) (raise-syntax-error 'in-hole "used outside of term")) (define-syntax (in-hole stx) (raise-syntax-error 'in-hole "used outside of term"))
@ -31,6 +32,10 @@
(define-for-syntax lang-keyword (define-for-syntax lang-keyword
(list '#:lang #f)) (list '#:lang #f))
(define-for-syntax (judgment-form-id? stx)
(and (identifier? stx)
(judgment-form? (syntax-local-value stx (λ () #f)))))
(define-syntax (term stx) (define-syntax (term stx)
(syntax-case stx () (syntax-case stx ()
[(term t . kw-args) [(term t . kw-args)
@ -70,6 +75,12 @@
[(_ inner-apps) [(_ inner-apps)
#'(λ (l) (map inner-apps l))])) #'(λ (l) (map inner-apps l))]))
(define-syntax (jf-apply stx)
(syntax-case stx ()
[(_ jf)
(judgment-form-id? #'jf)
(judgment-form-term-proc (syntax-local-value #'jf (λ () #f)))]))
(define-for-syntax currently-expanding-term-fn (make-parameter #f)) (define-for-syntax currently-expanding-term-fn (make-parameter #f))
@ -80,7 +91,7 @@
;; term-binding := `(,t-bind-pat (,mf-apps ,term-datum)) ;; term-binding := `(,t-bind-pat (,mf-apps ,term-datum))
;; t-bind-pat := id | (ref id) | `(,t-b-seq ...) ;; t-bind-pat := id | (ref id) | `(,t-b-seq ...)
;; t-b-seq := t-bind-pat | ellipsis ;; t-b-seq := t-bind-pat | ellipsis
;; mf-apps := `(mf-map ,mf-apps) | `(mf-app ,metafunction-id) ;; mf-apps := `(mf-map ,mf-apps) | `(mf-apply ,metafunction-id) | `(jf-apply ,judgment-form-id)
;; term-datum := `(quasidatum ,d) ;; term-datum := `(quasidatum ,d)
;; d := literal | pattern-variable | `(,d-seq ...) | ;; other (holes, undatum) ;; d := literal | pattern-variable | `(,d-seq ...) | ;; other (holes, undatum)
;; d-seq := d | ellipsis ;; d-seq := d | ellipsis
@ -105,7 +116,9 @@
(let-values ([(rewritten max-depth) (rewrite/max-depth args depth)]) (let-values ([(rewritten max-depth) (rewrite/max-depth args depth)])
(let ([result-id (car (generate-temporaries '(f-results)))]) (let ([result-id (car (generate-temporaries '(f-results)))])
(with-syntax ([fn fn]) (with-syntax ([fn fn])
(let loop ([func (syntax (mf-apply fn))] (let loop ([func (if (judgment-form-id? #'fn)
(syntax (jf-apply fn))
(syntax (mf-apply fn)))]
[args-stx rewritten] [args-stx rewritten]
[res result-id] [res result-id]
[args-depth (min depth max-depth)]) [args-depth (min depth max-depth)])
@ -134,6 +147,16 @@
(let ([f (term-fn-get-id (syntax-local-value/record (syntax metafunc-name) (λ (x) #t)))]) (let ([f (term-fn-get-id (syntax-local-value/record (syntax metafunc-name) (λ (x) #t)))])
(free-identifier-mapping-put! applied-metafunctions f #t) (free-identifier-mapping-put! applied-metafunctions f #t)
(rewrite-application f (syntax/loc stx (arg ...)) depth))] (rewrite-application f (syntax/loc stx (arg ...)) depth))]
[(jf-name arg ...)
(and (identifier? (syntax jf-name))
(if names
(not (memq (syntax->datum #'jf-name) names))
#t)
(judgment-form-id? #'jf-name))
(begin
(unless (not (memq 'O (judgment-form-mode (syntax-local-value #'jf-name))))
(raise-syntax-error 'term "judgment forms with output mode (\"O\") positions disallowed" arg-stx stx))
(rewrite-application #'jf-name (syntax/loc stx (arg ...)) depth))]
[f [f
(and (identifier? (syntax f)) (and (identifier? (syntax f))
(if names (if names
@ -291,7 +314,7 @@
(define-for-syntax (bind-mf-sig->pat bmfs) (define-for-syntax (bind-mf-sig->pat bmfs)
(syntax-case bmfs () (syntax-case bmfs ()
;; TODO : handle apps at ellipsis depth ;; TODO : handle apps at ellipsis depth , handle judgment forms (I only)
[(mf-apply f) [(mf-apply f)
(and (identifier? #'mf-apply) (and (identifier? #'mf-apply)
(eq? (syntax-e #'mf-apply) 'mf-apply)) (eq? (syntax-e #'mf-apply) 'mf-apply))
@ -299,39 +322,23 @@
(define-syntax (term-let-fn stx) (define-syntax (term-let-fn stx)
(syntax-case stx () (syntax-case stx ()
[(_ ([f . rhs-stuff] ...) body1 body2 ...) [(_ ([f rhs] ...) body1 body2 ...)
(with-syntax ([(g ...) (generate-temporaries (syntax (f ...)))] (with-syntax ([(g ...) (generate-temporaries (syntax (f ...)))])
[((rhs info) ...)
(for/list ([rhs-stuff (in-list (syntax->list #'(rhs-stuff ...)))]
[f (in-list (syntax->list #'(f ...)))])
(syntax-case rhs-stuff ()
[(rhs) #'(rhs #f)]
[(rhs info) #'(rhs info)]
[else (raise-syntax-error 'term-let-fn
(format "expected the rhs of a binding for ~a"
(syntax->datum f))
stx f)]))])
(syntax (syntax
(let ([g rhs] ...) (let ([g rhs] ...)
(let-syntax ([f (make-term-fn #'g info)] ...) (let-syntax ([f (make-term-fn #'g)] ...)
body1 body1
body2 ...))))])) body2 ...))))]))
(define-syntax (term-define-fn stx) (define-syntax (term-define-fn stx)
(syntax-case stx () (syntax-case stx ()
[(_ id exp info) [(_ id exp)
;; this info is currently used to record the
;; difference between define-metafunctions
;; bound identifiers and define-relation bound
;; ones for use in the unification-based generator
(with-syntax ([id2 (datum->syntax #'here (syntax-e #'id))]) (with-syntax ([id2 (datum->syntax #'here (syntax-e #'id))])
(syntax (syntax
(begin (begin
(define id2 exp) (define id2 exp)
(define-syntax id (define-syntax id
(make-term-fn #'id2 info)))))] (make-term-fn #'id2)))))]))
[(_ id exp)
#'(term-define-fn id exp #f)]))
(define-syntax (term-let/error-name stx) (define-syntax (term-let/error-name stx)
(syntax-case stx () (syntax-case stx ()

36
collects/redex/scribblings/ref.scrbl
View File

@ -43,11 +43,6 @@
[(_ args ...) [(_ args ...)
#'((tech (racketvarfont "term")) args ...)] #'((tech (racketvarfont "term")) args ...)]
[x (identifier? #'x) #'(tech (racketvarfont "term"))])) [x (identifier? #'x) #'(tech (racketvarfont "term"))]))
@(define-syntax (tttterm-no-unquote stx)
(syntax-case stx ()
[(_ args ...)
#'((tech (racketvarfont "term-without-unquote") #:key "term") args ...)]
[x (identifier? #'x) #'(tech (racketvarfont "term-without-unquote") #:key "term")]))
@(define-syntax (tterm stx) @(define-syntax (tterm stx)
(syntax-case stx () (syntax-case stx ()
@ -1191,10 +1186,10 @@ and @racket[#f] otherwise.
rule-name]] rule-name]]
[conclusion (form-id pat/term ...)] [conclusion (form-id pat/term ...)]
[premise (code:line (judgment-form-id pat/term ...) maybe-ellipsis) [premise (code:line (judgment-form-id pat/term ...) maybe-ellipsis)
(where @#,ttpattern @#,tttterm-no-unquote) (where @#,ttpattern @#,tttterm)
(where/hidden @#,ttpattern @#,tttterm-no-unquote) (where/hidden @#,ttpattern @#,tttterm)
(side-condition @#,tttterm-no-unquote) (side-condition @#,tttterm)
(side-condition/hidden @#,tttterm-no-unquote)] (side-condition/hidden @#,tttterm)]
[rule-name (code:line) [rule-name (code:line)
string string
non-ellipsis-non-hypens-var] non-ellipsis-non-hypens-var]
@ -1211,9 +1206,8 @@ Each rule must be such that its premises can be evaluated left-to-right
without ``guessing'' values for any of their pattern variables. Redex checks this without ``guessing'' values for any of their pattern variables. Redex checks this
property using the mandatory @racket[mode-spec] declaration, which partitions positions property using the mandatory @racket[mode-spec] declaration, which partitions positions
into inputs @racket[I] and outputs @racket[O]. Output positions in conclusions into inputs @racket[I] and outputs @racket[O]. Output positions in conclusions
and input positions in premises must be @|tttterm|s with no uses of and input positions in premises must be @|tttterm|s; input positions in conclusions and
@racket[unquote]; input positions in conclusions and output positions in output positions in premises must be @|ttpattern|s. When the optional @racket[contract-spec]
premises must be @|ttpattern|s. When the optional @racket[contract-spec]
declaration is present, Redex dynamically checks that the terms flowing through declaration is present, Redex dynamically checks that the terms flowing through
these positions match the provided patterns, raising an exception recognized by these positions match the provided patterns, raising an exception recognized by
@racket[exn:fail:redex] if not. @racket[exn:fail:redex] if not.
@ -1265,8 +1259,7 @@ to compute all pairs with a given sum.
(judgment-holds (sumr n_1 n_2 (s (s z))) (n_1 n_2))] (judgment-holds (sumr n_1 n_2 (s (s z))) (n_1 n_2))]
A rule's @racket[where] and @racket[where/hidden] premises behave as in A rule's @racket[where] and @racket[where/hidden] premises behave as in
@racket[reduction-relation] and @racket[define-metafunction] except the term @racket[reduction-relation] and @racket[define-metafunction].
cannot use unquotes.
@examples[ @examples[
#:eval redex-eval #:eval redex-eval
(define-judgment-form nats (define-judgment-form nats
@ -1297,8 +1290,13 @@ to those in @racket[reduction-relation] and @racket[define-metafunction], except
they do not implicitly unquote their right-hand sides. In other words, a premise they do not implicitly unquote their right-hand sides. In other words, a premise
of the form @racket[(side-condition term)] is equivalent to the premise of the form @racket[(side-condition term)] is equivalent to the premise
@racket[(where #t term)], except it does not typeset with the ``#t = '', as that would. @racket[(where #t term)], except it does not typeset with the ``#t = '', as that would.
Also, the term on the right-hand side cannot use unquotes so it is often convenient to
define a metafunction for these side-conditions. Judgments with exclusively @racket[I] mode positions may also be used in @|tttterm|s
in a manner similar to metafunctions, and evaluate to a boolean.
@examples[
#:eval redex-eval
(term (le (s z) (s (s z))))
(term (le (s z) z))]
A literal ellipsis may follow a judgment premise when a template in one of the 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 judgment's input positions contains a pattern variable bound at ellipsis-depth
@ -1452,12 +1450,6 @@ the argument contracts.
(term (subtype int num)) (term (subtype int num))
(term (subtype (int → int) (num → num))) (term (subtype (int → int) (num → num)))
(term (subtype (num → int) (num → num)))] (term (subtype (num → int) (num → num)))]
Note that relations are assumed to always return the same results for
the same inputs, and their results are cached, unless
@racket[caching-enable?] is set to @racket[#f]. Accordingly, if a
relation is called with the same inputs twice, then its right-hand
sides are evaluated only once.
} }
@defparam[current-traced-metafunctions traced-metafunctions (or/c 'all (listof symbol?))]{ @defparam[current-traced-metafunctions traced-metafunctions (or/c 'all (listof symbol?))]{

4
collects/redex/tests/gen-test.rkt
View File

@ -63,10 +63,10 @@
#t) #t)
(test-equal (generate-term nats #:satisfying (sum z (s z) n) +inf.0) (test-equal (generate-term nats #:satisfying (sum z (s z) n) +inf.0)
(term (sum z (s z) (s z)))) '(sum z (s z) (s z)))
(test-equal (generate-term nats #:satisfying (sum (s z) (s z) n) +inf.0) (test-equal (generate-term nats #:satisfying (sum (s z) (s z) n) +inf.0)
(term (sum (s z) (s z) (s (s z))))) '(sum (s z) (s z) (s (s z))))
(for ([_ 100]) (for ([_ 100])
(match (generate-term nats #:satisfying (sum n_1 n_2 n_3) 5) (match (generate-term nats #:satisfying (sum n_1 n_2 n_3) 5)

1
collects/redex/tests/run-tests.rkt
View File

@ -24,6 +24,7 @@
"tl-test.rkt" "tl-test.rkt"
"term-test.rkt" "term-test.rkt"
"rg-test.rkt" "rg-test.rkt"
"gen-test.rkt"
"keyword-macros-test.rkt" "keyword-macros-test.rkt"
"core-layout-test.rkt" "core-layout-test.rkt"
"pict-test.rkt" "pict-test.rkt"

16
collects/redex/tests/syn-err-tests/judgment-form-definition.rktd
View File

@ -142,21 +142,7 @@
[(name) [(name)
bad-prem]) bad-prem])
(void))) (void)))
(#rx"unquote unsupported"
([unq ,(+ 1)])
(let ()
(define-judgment-form syn-err-lang
#:mode (uses-unquote I)
[(uses-unquote n)
(where n unq)])
(void)))
(#rx"unquote unsupported"
([unq ,'z])
(let ()
(define-judgment-form syn-err-lang
#:mode (uses-unquote I O)
[(uses-unquote n unq)])
(void)))
(#rx"missing ellipsis" (#rx"missing ellipsis"
([use any_0]) ([ellipsis ...] [def any_0]) ([use any_0]) ([ellipsis ...] [def any_0])

2
collects/redex/tests/syn-err-tests/relation-definition.rktd
View File

@ -20,7 +20,7 @@
(define-relation syn-err-lang (define-relation syn-err-lang
[(R () ())] [(R () ())]
[(R (any_a) (any_b)) [(R (any_a) (any_b))
(R anc_c any_d) (R any_c any_d)
first-where first-where
(where any_d any_b) (where any_d any_b)
first-post-where])) first-post-where]))

97
collects/redex/tests/tl-test.rkt
View File

@ -1237,6 +1237,24 @@
(test (term (R (xx) (xx))) #t) (test (term (R (xx) (xx))) #t)
(test (term (R (()) ())) #f)) (test (term (R (()) ())) #f))
(let ()
(define-relation empty-language
[(a number_1)
(b number_1)]
[(a 2)])
(define-relation empty-language
[(b 1)]
[(b 2)])
(test (term (a 1)) #t)
(test (term (a 2)) #t)
(test (term (a 3)) #f)
(test (term (b 1)) #t)
(test (term (b 2)) #t)
(test (term (b 3)) #f))
(exec-syntax-error-tests "syn-err-tests/relation-definition.rktd") (exec-syntax-error-tests "syn-err-tests/relation-definition.rktd")
@ -2299,7 +2317,9 @@
[(different any_a any_a) #f] [(different any_a any_a) #f]
[(different any_a any_b) #t]) [(different any_a any_b) #t])
(test (judgment-holds (R 1 2)) #t) (test (judgment-holds (R 1 2)) #t)
(test (judgment-holds (R 1 1)) #f)) (test (judgment-holds (R 1 1)) #f)
(test (term (R 1 2)) #t)
(test (term (R 1 1)) #f))
(let () (let ()
(define-judgment-form empty-language (define-judgment-form empty-language
@ -2441,6 +2461,79 @@
'(J () z) '(J () z)
#f #f
'())))))))) '()))))))))
(let ()
(define-language U
(n Z (S n)))
(define-judgment-form U
#:mode (jsum I I I)
[(jsum n Z n)]
[(jsum n_1 (S n_2) (S n_3))
(jsum n_1 n_2 n_3)])
(define-relation U
sum ⊆ n x n x n
[(sum n Z n)]
[(sum n_1 (S n_2) (S n_3))
(sum n_1 n_2 n_3)])
(define-relation U
[(rjsum n_1 n_2 n_3)
(jjsum n_1 n_2 n_3)])
(define-judgment-form U
#:mode (jjsum I I I)
[(jjsum n_1 n_2 n_3)
(rrsum n_1 n_2 n_3)])
(define-relation U
[(rrsum n_1 n_2 n_3)
(jsum n_1 n_2 n_3)])
(test (term (sum Z Z Z)) #t)
(test (term (sum Z Z (S Z))) #f)
(test (term (sum (S Z) (S Z) (S (S Z)))) #t)
(test (term (sum (S Z) (S (S Z)) (S (S Z)))) #f)
(test (term (sum (S (S Z)) (S (S Z)) (S (S (S (S Z)))))) #t)
(test (term (sum (S (S Z)) (S (S Z)) (S (S (S Z))))) #f)
(test (term (jsum Z Z Z)) #t)
(test (term (jsum Z Z (S Z))) #f)
(test (term (jsum (S Z) (S Z) (S (S Z)))) #t)
(test (term (jsum (S Z) (S (S Z)) (S (S Z)))) #f)
(test (term (jsum (S (S Z)) (S (S Z)) (S (S (S (S Z)))))) #t)
(test (term (jsum (S (S Z)) (S (S Z)) (S (S (S Z))))) #f)
(test (term (rjsum Z Z Z)) #t)
(test (term (rjsum Z Z (S Z))) #f)
(test (term (rjsum (S Z) (S Z) (S (S Z)))) #t)
(test (term (rjsum (S Z) (S (S Z)) (S (S Z)))) #f)
(test (term (rjsum (S (S Z)) (S (S Z)) (S (S (S (S Z)))))) #t)
(test (term (rjsum (S (S Z)) (S (S Z)) (S (S (S Z))))) #f))
(let ()
(define-judgment-form empty-language
#:mode (Q I O)
[(Q number_1 ,(+ (term number_1) (term number_1)))]
[(Q (number_1 number_2) number_3)
(Q ,(+ (term number_1) (term number_2)) number_3)])
(test (judgment-holds (Q 1 2))
#t)
(test (judgment-holds (Q 1 3))
#f)
(test (judgment-holds (Q 1 number_1) number_1)
'(2))
(test (judgment-holds (Q 7 14))
#t)
(test (judgment-holds (Q 7 symbol))
#f)
(test (judgment-holds (Q 7 number_1) number_1)
'(14))
(test (judgment-holds (Q (1 2) 6))
#t)
(test (judgment-holds (Q (1 3) 6))
#f)
(test (judgment-holds (Q (3 4) number_1) number_1)
'(14)))
(parameterize ([current-namespace (make-base-namespace)]) (parameterize ([current-namespace (make-base-namespace)])
@ -2921,7 +3014,7 @@
(parameterize ([relation-coverage (list c)]) (parameterize ([relation-coverage (list c)])
(term (f 1)) (term (f 1))
(test (sorted-counts c) '(1 0 0)))) (test (sorted-counts c) '(1 0 0))))
#;
(let ([c (make-coverage R)]) (let ([c (make-coverage R)])
(parameterize ([relation-coverage (list c)]) (parameterize ([relation-coverage (list c)])
(term (R 2)) (term (R 2))

5
doc/release-notes/redex/HISTORY.txt
View File

@ -4,6 +4,11 @@ v5.3.2
(which allows Redex to more effectively generate things (which allows Redex to more effectively generate things
like well-typed terms) like well-typed terms)
* removed the restriction on unquotes in define-judgment-form
* added the option to use judgment-forms with only I mode
positions in terms
v5.3.1 v5.3.1
* added optional #:lang keyword to term * added optional #:lang keyword to term