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

bring bind-withs down under 102 columns

Browse Source
This commit is contained in:
Robby Findler 2014-10-11 09:00:05 -05:00
parent 2d66d84b2f
commit 2f351b626b
1 changed files with 45 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -145,7 +145,9 @@
;; ct-lang is an identifier guaranteed to be bound by define-language ;; ct-lang is an identifier guaranteed to be bound by define-language
;; that can be used to call rewrite-side-conditions/check-errs, but ;; that can be used to call rewrite-side-conditions/check-errs, but
;; some extension of that language may end up being bound to rt-lang ;; some extension of that language may end up being bound to rt-lang
(define-for-syntax (bind-withs orig-name main rt-lang lang-nts ct-lang stx where-mode body names w/ellipses side-condition-unquoted? jf-results-id) (define-for-syntax (bind-withs orig-name main rt-lang lang-nts ct-lang stx
where-mode body names w/ellipses
side-condition-unquoted? jf-results-id)
(with-disappeared-uses (with-disappeared-uses
(let loop ([stx stx] (let loop ([stx stx]
[to-not-be-in main] [to-not-be-in main]
@ -180,7 +182,8 @@
[(predicate) [(predicate)
#'combine-where-results/predicate] #'combine-where-results/predicate]
[else (error 'unknown-where-mode "~s" where-mode)]) [else (error 'unknown-where-mode "~s" where-mode)])
(match-pattern (compile-pattern #,rt-lang `side-conditions-rewritten #t) (term e #:lang #,ct-lang)) (match-pattern (compile-pattern #,rt-lang `side-conditions-rewritten #t)
(term e #:lang #,ct-lang))
(λ (bindings) (λ (bindings)
(let ([x (lookup-binding bindings 'names)] ...) (let ([x (lookup-binding bindings 'names)] ...)
(and binding-constraints ... (and binding-constraints ...
@ -195,7 +198,7 @@
#`(and (term s) ... #,(loop #'(y ...) to-not-be-in env)))] #`(and (term s) ... #,(loop #'(y ...) to-not-be-in env)))]
[((fresh x) y ...) [((fresh x) y ...)
(identifier? #'x) (identifier? #'x)
#`(term-let ([x (variable-not-in #,to-not-be-in 'x)]) #`(term-let ([x (variable-not-in #,to-not-be-in 'x)])
#,(loop #'(y ...) #`(list (term x) #,to-not-be-in) env))] #,(loop #'(y ...) #`(list (term x) #,to-not-be-in) env))]
[((fresh x name) y ...) [((fresh x name) y ...)
(identifier? #'x) (identifier? #'x)
@ -205,7 +208,7 @@
#,(loop #'(y ...) #`(list (term x) #,to-not-be-in) env))] #,(loop #'(y ...) #`(list (term x) #,to-not-be-in) env))]
[((fresh (y) (x ...)) z ...) [((fresh (y) (x ...)) z ...)
#`(term-let ([(y #,'...) #`(term-let ([(y #,'...)
(variables-not-in #,to-not-be-in (variables-not-in #,to-not-be-in
(map (λ (_ignore_) 'y) (map (λ (_ignore_) 'y)
(term (x ...))))]) (term (x ...))))])
#,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in) env))] #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in) env))]
@ -220,40 +223,44 @@
(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 ()
[(rest-clauses under-ellipsis?) (define premise (syntax-case stx () [(p . _) #'p]))
(syntax-case #'after () (define-values (rest-clauses under-ellipsis?)
[(maybe-ellipsis . more) (syntax-case #'after ()
(ellipsis? #'maybe-ellipsis) [(maybe-ellipsis . more)
(values #'more #t)] (ellipsis? #'maybe-ellipsis)
[_ (values #'after #f)])] (values #'more #t)]
[(judgment-form) (lookup-judgment-form-id #'form-name)] [_ (values #'after #f)]))
[(mode) (judgment-form-mode judgment-form)] (define judgment-form (lookup-judgment-form-id #'form-name))
[(judgment-proc) (judgment-form-proc judgment-form)] (define mode (judgment-form-mode judgment-form))
[(input-template output-pre-pattern) (define judgment-proc (judgment-form-proc judgment-form))
(let-values ([(in out) (split-by-mode (syntax->list #'(pats ...)) mode)]) (define-values (input-template output-pre-pattern)
(if under-ellipsis? (let-values ([(in out) (split-by-mode (syntax->list #'(pats ...)) mode)])
(let ([ellipsis (syntax/loc premise (... ...))]) (if under-ellipsis?
(values #`(#,in #,ellipsis) #`(#,out #,ellipsis))) (let ([ellipsis (syntax/loc premise (... ...))])
(values in out)))] (values #`(#,in #,ellipsis) #`(#,out #,ellipsis)))
[(syncheck-exp output-pattern output-names output-names/ellipses) (values in out))))
(with-syntax ([(syncheck-exp output names names/ellipses) (define-values (syncheck-exp output-pattern output-names output-names/ellipses)
(rewrite-side-conditions/check-errs ct-lang orig-name #t output-pre-pattern)]) (with-syntax ([(syncheck-exp output names names/ellipses)
(values #'syncheck-exp (rewrite-side-conditions/check-errs ct-lang orig-name #t
#'output output-pre-pattern)])
(syntax->list #'names) (values #'syncheck-exp
(syntax->list #'names/ellipses)))] #'output
[(binding-constraints temporaries env+) (syntax->list #'names)
(generate-binding-constraints output-names output-names/ellipses env orig-name)] (syntax->list #'names/ellipses))))
[(rest-body) (loop rest-clauses #`(list judgment-output #,to-not-be-in) env+)] (define-values (binding-constraints temporaries env+)
[(call) (generate-binding-constraints output-names output-names/ellipses env orig-name))
(let ([input (quasisyntax/loc premise (term #,input-template #:lang #,ct-lang))]) (define rest-body
(define (make-traced input) (loop rest-clauses #`(list judgment-output #,to-not-be-in) env+))
(quasisyntax/loc premise (define call
(call-judgment-form 'form-name #,judgment-proc '#,mode #,input #,(if jf-results-id #''() #f)))) (let ([input (quasisyntax/loc premise (term #,input-template #:lang #,ct-lang))])
(if under-ellipsis? (define (make-traced input)
#`(repeated-premise-outputs #,input (λ (x) #,(make-traced #'x))) (quasisyntax/loc premise
(make-traced input)))]) (call-judgment-form 'form-name #,judgment-proc '#,mode #,input
#,(if jf-results-id #''() #f))))
(if under-ellipsis?
#`(repeated-premise-outputs #,input (λ (x) #,(make-traced #'x)))
(make-traced input))))
(record-disappeared-uses (list #'form-name)) (record-disappeared-uses (list #'form-name))
(with-syntax ([(output-name ...) output-names] (with-syntax ([(output-name ...) output-names]
[(output-name/ellipsis ...) output-names/ellipses] [(output-name/ellipsis ...) output-names/ellipses]