changed the notation of metafunctions
svn: r11039
This commit is contained in:
Robby Findler
parent
50b418809d
commit
ef86c20a1d
|
|
@ -103,10 +103,10 @@ reflects the (broken) spec).
|
|||
quote))
|
||||
(not (prim-op? (term x))))))
|
||||
|
||||
(define-metafunction beg-e-subst lang
|
||||
[(x v x) v]
|
||||
[(x v (any_1 ...)) ((beg-e-subst (x v any_1)) ...)]
|
||||
[(x v any) any])
|
||||
(define-metafunction lang
|
||||
[(beg-e-subst (x v x)) v]
|
||||
[(beg-e-subst (x v (any_1 ...))) ((beg-e-subst (x v any_1)) ...)]
|
||||
[(beg-e-subst (x v any)) any])
|
||||
|
||||
(define (maker? v)
|
||||
(and (symbol? v)
|
||||
|
|
|
|||
|
|
@ -28,23 +28,24 @@
|
|||
(--> (in-hole e-ctxt_1 (let (x_1 v_1) e_1))
|
||||
(in-hole e-ctxt_1 (subst (x_1 v_1 e_1))))))
|
||||
|
||||
(define-metafunction subst
|
||||
lang
|
||||
[(x_1 e_1 (lambda (x_1) e_2)) (lambda (x_1) e_2)]
|
||||
[(x_1 e_1 (lambda (x_2) e_2))
|
||||
(define-metafunction lang
|
||||
[(subst (x_1 e_1 (lambda (x_1) e_2))) (lambda (x_1) e_2)]
|
||||
[(subst (x_1 e_1 (lambda (x_2) e_2)))
|
||||
,(term-let ((x_new (variable-not-in (term e_1) (term x_2))))
|
||||
(term (lambda (x_new) (subst (x_1 e_1 (subst (x_2 x_new e_2)))))))]
|
||||
[(x_1 e_1 (let (x_1 e_2) e_3)) (let (x_1 (subst (x_1 e_1 e_2))) e_3)]
|
||||
[(x_1 e_1 (let (x_2 e_2) e_3))
|
||||
[(subst (x_1 e_1 (let (x_1 e_2) e_3))) (let (x_1 (subst (x_1 e_1 e_2))) e_3)]
|
||||
[(subst (x_1 e_1 (let (x_2 e_2) e_3)))
|
||||
,(term-let ((x_new (variable-not-in (term e_1) (term x_2))))
|
||||
(term (let (x_2 (subst (x_1 e_1 e_2))) (subst (x_1 e_1 (subst (x_2 x_new e_3)))))))]
|
||||
[(x_1 e_1 x_1) e_1]
|
||||
[(x_1 e_1 x_2) x_2]
|
||||
[(x_1 e_1 (app e_2 e_3)) (app (subst (x_1 e_1 e_2))
|
||||
(subst (x_1 e_1 e_3)))]
|
||||
[(x_1 e_1 (+ e_2 e_3)) (+ (subst (x_1 e_1 e_2))
|
||||
(subst (x_1 e_1 e_3)))]
|
||||
[(x_1 e_1 number_1) number_1])
|
||||
[(subst (x_1 e_1 x_1)) e_1]
|
||||
[(subst (x_1 e_1 x_2)) x_2]
|
||||
[(subst (x_1 e_1 (app e_2 e_3)))
|
||||
(app (subst (x_1 e_1 e_2))
|
||||
(subst (x_1 e_1 e_3)))]
|
||||
[(subst (x_1 e_1 (+ e_2 e_3)))
|
||||
(+ (subst (x_1 e_1 e_2))
|
||||
(subst (x_1 e_1 e_3)))]
|
||||
[(subst (x_1 e_1 number_1)) number_1])
|
||||
|
||||
(traces lang reductions
|
||||
'(let (plus (lambda (m)
|
||||
|
|
|
|||
|
|
@ -5,20 +5,18 @@
|
|||
(define-language subst-lang
|
||||
(x variable))
|
||||
|
||||
(define-metafunction subst-n
|
||||
subst-lang
|
||||
[((x_1 any_1) (x_2 any_2) ... any_3)
|
||||
(define-metafunction subst-lang
|
||||
[(subst-n ((x_1 any_1) (x_2 any_2) ... any_3))
|
||||
(subst (x_1 any_1 (subst-n ((x_2 any_2) ... any_3))))]
|
||||
[(any_3) any_3])
|
||||
[(subst-n (any_3)) any_3])
|
||||
|
||||
(define-metafunction subst
|
||||
subst-lang
|
||||
(define-metafunction subst-lang
|
||||
;; 1. x_1 bound, so don't continue in λ body
|
||||
[(x_1 any_1 (λ (x_2 ... x_1 x_3 ...) any_2))
|
||||
[(subst (x_1 any_1 (λ (x_2 ... x_1 x_3 ...) any_2)))
|
||||
(λ (x_2 ... x_1 x_3 ...) any_2)
|
||||
(side-condition (not (member (term x_1) (term (x_2 ...)))))]
|
||||
;; 2. general purpose capture avoiding case
|
||||
[(x_1 any_1 (λ (x_2 ...) any_2))
|
||||
[(subst (x_1 any_1 (λ (x_2 ...) any_2)))
|
||||
,(term-let ([(x_new ...)
|
||||
(variables-not-in (term (x_1 any_1 any_2))
|
||||
(term (x_2 ...)))])
|
||||
|
|
@ -26,22 +24,21 @@
|
|||
(λ (x_new ...)
|
||||
(subst (x_1 any_1 (subst-vars ((x_2 x_new) ... any_2)))))))]
|
||||
;; 3. replace x_1 with e_1
|
||||
[(x_1 any_1 x_1) any_1]
|
||||
[(subst (x_1 any_1 x_1)) any_1]
|
||||
;; 4. x_1 and x_2 are different, so don't replace
|
||||
[(x_1 any_1 x_2) x_2]
|
||||
[(subst (x_1 any_1 x_2)) x_2]
|
||||
;; the last two cases cover all other expression forms
|
||||
[(x_1 any_1 (any_2 ...))
|
||||
[(subst (x_1 any_1 (any_2 ...)))
|
||||
((subst (x_1 any_1 any_2)) ...)]
|
||||
[(x_1 any_1 any_2) any_2])
|
||||
[(subst (x_1 any_1 any_2)) any_2])
|
||||
|
||||
(define-metafunction subst-vars
|
||||
subst-lang
|
||||
[((x_1 any_1) x_1) any_1]
|
||||
[((x_1 any_1) (any_2 ...)) ((subst-vars ((x_1 any_1) any_2)) ...)]
|
||||
[((x_1 any_1) any_2) any_2]
|
||||
[((x_1 any_1) (x_2 any_2) ... any_3)
|
||||
(define-metafunction subst-lang
|
||||
[(subst-vars ((x_1 any_1) x_1)) any_1]
|
||||
[(subst-vars ((x_1 any_1) (any_2 ...))) ((subst-vars ((x_1 any_1) any_2)) ...)]
|
||||
[(subst-vars ((x_1 any_1) any_2)) any_2]
|
||||
[(subst-vars ((x_1 any_1) (x_2 any_2) ... any_3))
|
||||
(subst-vars ((x_1 any_1) (subst-vars ((x_2 any_2) ... any_3))))]
|
||||
[(any) any])
|
||||
[(subst-vars (any)) any])
|
||||
|
||||
(begin
|
||||
(test-equal (term (subst (x y x))) (term y))
|
||||
|
|
|
|||
|
|
@ -34,8 +34,8 @@
|
|||
(extend-reduction-relation red lang (--> 1 2)))
|
||||
"extended-reduction-relation.png")
|
||||
|
||||
(define-multi-args-metafunction S lang
|
||||
[(x v e) e])
|
||||
(define-metafunction lang
|
||||
[(S x v e) e])
|
||||
|
||||
(test (metafunction->pict S)
|
||||
"metafunction.png")
|
||||
|
|
|
|||
|
|
@ -95,9 +95,7 @@
|
|||
#,(syntax-column stx)
|
||||
#f
|
||||
#f
|
||||
#,(if (term-fn-multi-arg? (syntax-local-value #'x))
|
||||
#''multi
|
||||
#''single))]
|
||||
'multi)]
|
||||
[x
|
||||
(identifier? #'x)
|
||||
#`(init-loc-wrapper
|
||||
|
|
|
|||
|
|
@ -25,11 +25,7 @@
|
|||
(language->pict var-not-ab #f)
|
||||
|
||||
(let ()
|
||||
(define-metafunction zero empty-language [any_in 0])
|
||||
(metafunction->pict zero))
|
||||
|
||||
(let ()
|
||||
(define-multi-args-metafunction zero empty-language [(any_in any_out) 0])
|
||||
(define-metafunction empty-language [(zero any_in) 0])
|
||||
(metafunction->pict zero))
|
||||
|
||||
(reduction-relation->pict
|
||||
|
|
|
|||
|
|
@ -746,160 +746,151 @@
|
|||
|
||||
(define-syntax (in-domain? stx)
|
||||
(syntax-case stx ()
|
||||
[(_ exp name)
|
||||
[(_ (name exp ...))
|
||||
(begin
|
||||
(unless (identifier? #'name)
|
||||
(raise-syntax-error #f "expected an identifier" stx #'name))
|
||||
#'(in-domain?/proc (metafunction-form name) exp))]))
|
||||
#'(in-domain?/proc (metafunction-form name) (term (exp ...))))]))
|
||||
|
||||
(define (in-domain?/proc mf exp)
|
||||
(let ([mp (metafunction-proc mf)])
|
||||
((metafunc-proc-in-dom? mp)
|
||||
(if (metafunc-proc-multi-arg? mp)
|
||||
exp
|
||||
(list exp)))))
|
||||
exp)))
|
||||
|
||||
(define-syntax (define-metafunction stx)
|
||||
(syntax-case stx ()
|
||||
[(_ name lang-exp [lhs roc ...] ...)
|
||||
(with-syntax ([(lhs-w ...) (map (λ (x) (list x)) (syntax->list #'(lhs ...)))])
|
||||
(syntax/loc stx
|
||||
(internal-define-metafunction
|
||||
#f #f name lang-exp
|
||||
[lhs-w roc ...] ...)))]))
|
||||
|
||||
|
||||
(define-syntax (define-metafunction/extension stx)
|
||||
(syntax-case stx ()
|
||||
[(_ name lang-exp prev [lhs roc ...] ...)
|
||||
(identifier? #'name)
|
||||
(with-syntax ([(lhs-w ...) (map (λ (x) (list x)) (syntax->list #'(lhs ...)))])
|
||||
(syntax/loc stx
|
||||
(internal-define-metafunction
|
||||
prev #f name lang-exp
|
||||
[lhs-w roc ...] ...)))]))
|
||||
|
||||
(define-syntax (define-multi-args-metafunction stx)
|
||||
(syntax-case stx ()
|
||||
[(_ name lang-exp [(lhs ...) roc ...] ...)
|
||||
(with-syntax ([s (list* #'internal-define-metafunction
|
||||
#f #t
|
||||
(cdr (syntax->list stx)))])
|
||||
(syntax/loc stx s))]
|
||||
[(_ name lang-exp clauses ...)
|
||||
(begin
|
||||
(unless (identifier? #'name)
|
||||
(raise-syntax-error 'define-multi-args-metafunction "expected the name of a language" stx #'name))
|
||||
(for-each
|
||||
(λ (clause)
|
||||
(syntax-case clause ()
|
||||
[((a ...) b) (void)]
|
||||
[(a b)
|
||||
(raise-syntax-error 'define-multi-args-metafunction "expected lhs clause to be a sequence (with parens)"
|
||||
stx
|
||||
#'a)]
|
||||
[else
|
||||
(raise-syntax-error 'define-metafunction "expected a lhs and rhs clause" stx clause)]))
|
||||
(syntax->list (syntax (clauses ...))))
|
||||
(raise-syntax-error 'define-multi-args-metafunction "missing error message check" stx))]))
|
||||
|
||||
(define-syntax (define-multi-args-metafunction/extension stx)
|
||||
(syntax-case stx ()
|
||||
[(_ name lang-exp prev [lhs roc ...] ...)
|
||||
(identifier? #'name)
|
||||
(syntax/loc stx
|
||||
(internal-define-metafunction
|
||||
prev #t name lang-exp
|
||||
[lhs roc ...] ...))]))
|
||||
|
||||
(define-syntax-set (internal-define-metafunction)
|
||||
(define (internal-define-metafunction/proc stx)
|
||||
(define-syntax-set (define-metafunction define-metafunction/extension)
|
||||
|
||||
(define (define-metafunction/proc stx)
|
||||
(syntax-case stx ()
|
||||
[(_ prev-metafunction multi-args? name lang (lhs rhs stuff ...) ...)
|
||||
(and (identifier? #'name)
|
||||
(identifier? #'lang))
|
||||
(with-syntax ([(((tl-side-conds ...) ...)
|
||||
(tl-bindings ...))
|
||||
(extract-side-conditions (syntax-e #'name) stx #'((stuff ...) ...))])
|
||||
(let ([lang-nts (language-id-nts #'lang 'define-metafunction)])
|
||||
(with-syntax ([(side-conditions-rewritten ...)
|
||||
(map (λ (x) (rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
#t
|
||||
'define-metafunction
|
||||
x))
|
||||
(syntax->list (syntax ((side-condition lhs (and tl-side-conds ...)) ...))))]
|
||||
[(rhs-fns ...)
|
||||
(map (λ (lhs rhs bindings)
|
||||
(let-values ([(names names/ellipses) (extract-names lang-nts 'define-metafunction #t lhs)])
|
||||
(with-syntax ([(names ...) names]
|
||||
[(names/ellipses ...) names/ellipses]
|
||||
[rhs rhs]
|
||||
[((tl-var tl-exp) ...) bindings])
|
||||
(syntax
|
||||
(λ (name bindings)
|
||||
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
|
||||
(term-let ([tl-var tl-exp] ...)
|
||||
(term-let-fn ((name name))
|
||||
(term rhs)))))))))
|
||||
(syntax->list (syntax (lhs ...)))
|
||||
(syntax->list (syntax (rhs ...)))
|
||||
(syntax->list (syntax (tl-bindings ...))))]
|
||||
[(name2) (generate-temporaries (syntax (name)))]
|
||||
[((side-cond ...) ...)
|
||||
;; For generating a pict, separate out side conditions wrapping the LHS and at the top-level
|
||||
(map (lambda (lhs scs)
|
||||
(append
|
||||
(let loop ([lhs lhs])
|
||||
(syntax-case lhs (side-condition term)
|
||||
[(side-condition pat (term sc))
|
||||
(cons #'sc (loop #'pat))]
|
||||
[_else null]))
|
||||
scs))
|
||||
(syntax->list #'(lhs ...))
|
||||
(syntax->list #'((tl-side-conds ...) ...)))]
|
||||
[(((bind-id . bind-pat) ...) ...)
|
||||
;; Also for pict, extract pattern bindings
|
||||
(map extract-pattern-binds (syntax->list #'(lhs ...)))]
|
||||
[(lhs-app ...) (if (syntax-e #'multi-args?)
|
||||
(syntax->list (syntax (lhs ...)))
|
||||
;; if single arg, drop the extra parens, since they have the wrong
|
||||
;; source locations anyways
|
||||
(map (λ (x) (car (syntax-e x)))
|
||||
(syntax->list (syntax (lhs ...)))))])
|
||||
#`(begin
|
||||
(define name2
|
||||
(build-metafunction
|
||||
lang
|
||||
(list `side-conditions-rewritten ...)
|
||||
(list rhs-fns ...)
|
||||
#,(if (syntax-e #'prev-metafunction)
|
||||
(let ([term-fn (syntax-local-value #'prev-metafunction)])
|
||||
#`(metafunc-proc-cps #,(term-fn-get-id term-fn)))
|
||||
#''())
|
||||
#,(if (syntax-e #'prev-metafunction)
|
||||
(let ([term-fn (syntax-local-value #'prev-metafunction)])
|
||||
#`(metafunc-proc-rhss #,(term-fn-get-id term-fn)))
|
||||
#''())
|
||||
(λ (f/dom cps rhss)
|
||||
(make-metafunc-proc
|
||||
(let ([name (lambda (x) (f/dom x #f))]) name)
|
||||
(list (list (to-lw lhs-app)
|
||||
(list (to-lw/uq side-cond) ...)
|
||||
(list (cons (to-lw bind-id)
|
||||
(to-lw bind-pat))
|
||||
...)
|
||||
(to-lw rhs))
|
||||
...)
|
||||
lang
|
||||
multi-args?
|
||||
'name
|
||||
cps
|
||||
rhss
|
||||
(let ([name (lambda (x) (f/dom x #t))]) name)))
|
||||
'name))
|
||||
(term-define-fn name name2 multi-args?)))))]
|
||||
[(_ prev-metafunction multi-args? name lang clauses ...)
|
||||
[(_ . rest)
|
||||
(internal-define-metafunction stx #f #'rest)]))
|
||||
|
||||
(define (define-metafunction/extension/proc stx)
|
||||
(syntax-case stx ()
|
||||
[(_ prev . rest)
|
||||
(identifier? #'prev)
|
||||
(internal-define-metafunction stx #'prev #'rest)]))
|
||||
|
||||
(define (internal-define-metafunction orig-stx prev-metafunction stx)
|
||||
(syntax-case stx ()
|
||||
[(lang . rest)
|
||||
(let ([syn-error-name (if prev-metafunction
|
||||
'define-metafunction/extension
|
||||
'define-metafunction)])
|
||||
(unless (identifier? #'lang)
|
||||
(raise-syntax-error syn-error-name "expected an identifier in the language position" orig-stx #'lang))
|
||||
(when (null? (syntax-e #'rest))
|
||||
(raise-syntax-error syn-error-name "no clauses" orig-stx))
|
||||
(let-values ([(dom-ctcs codom-contract pats)
|
||||
(split-out-contract orig-stx syn-error-name #'rest)])
|
||||
(with-syntax ([(((name lhs-clauses ...) rhs stuff ...) ...) pats]
|
||||
[(lhs-for-lw ...)
|
||||
(with-syntax ([((lhs-for-lw _ _ ...) ...) pats])
|
||||
(map (λ (x) (datum->syntax #f (cdr (syntax-e x)) x))
|
||||
(syntax->list #'(lhs-for-lw ...))))])
|
||||
(with-syntax ([(lhs ...) #'((lhs-clauses ...) ...)]
|
||||
[name (let loop ([name (car (syntax->list #'(name ...)))]
|
||||
[names (cdr (syntax->list #'(name ...)))])
|
||||
(cond
|
||||
[(null? names) name]
|
||||
[else
|
||||
(unless (eq? (syntax-e name) (syntax-e (car names)))
|
||||
(raise-syntax-error 'define-metafunction
|
||||
"expected each clause to use the same name"
|
||||
stx
|
||||
(list name (car names))))
|
||||
(loop name (cdr names))]))])
|
||||
|
||||
(with-syntax ([(((tl-side-conds ...) ...)
|
||||
(tl-bindings ...))
|
||||
(extract-side-conditions (syntax-e #'name) stx #'((stuff ...) ...))])
|
||||
(let ([lang-nts (language-id-nts #'lang 'define-metafunction)])
|
||||
(with-syntax ([(side-conditions-rewritten ...)
|
||||
(map (λ (x) (rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
#t
|
||||
'define-metafunction
|
||||
x))
|
||||
(syntax->list (syntax ((side-condition lhs (and tl-side-conds ...)) ...))))]
|
||||
[dom-side-conditions-rewritten
|
||||
(and dom-ctcs
|
||||
(rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
#t
|
||||
'define-metafunction
|
||||
dom-ctcs))]
|
||||
[codom-side-conditions-rewritten
|
||||
(rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
#t
|
||||
'define-metafunction
|
||||
codom-contract)]
|
||||
[(rhs-fns ...)
|
||||
(map (λ (lhs rhs bindings)
|
||||
(let-values ([(names names/ellipses) (extract-names lang-nts 'define-metafunction #t lhs)])
|
||||
(with-syntax ([(names ...) names]
|
||||
[(names/ellipses ...) names/ellipses]
|
||||
[rhs rhs]
|
||||
[((tl-var tl-exp) ...) bindings])
|
||||
(syntax
|
||||
(λ (name bindings)
|
||||
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
|
||||
(term-let ([tl-var tl-exp] ...)
|
||||
(term-let-fn ((name name))
|
||||
(term rhs)))))))))
|
||||
(syntax->list (syntax (lhs ...)))
|
||||
(syntax->list (syntax (rhs ...)))
|
||||
(syntax->list (syntax (tl-bindings ...))))]
|
||||
[(name2 name-predicate) (generate-temporaries (syntax (name name)))]
|
||||
[((side-cond ...) ...)
|
||||
;; For generating a pict, separate out side conditions wrapping the LHS and at the top-level
|
||||
(map (lambda (lhs scs)
|
||||
(append
|
||||
(let loop ([lhs lhs])
|
||||
(syntax-case lhs (side-condition term)
|
||||
[(side-condition pat (term sc))
|
||||
(cons #'sc (loop #'pat))]
|
||||
[_else null]))
|
||||
scs))
|
||||
(syntax->list #'(lhs ...))
|
||||
(syntax->list #'((tl-side-conds ...) ...)))]
|
||||
[(((bind-id . bind-pat) ...) ...)
|
||||
;; Also for pict, extract pattern bindings
|
||||
(map extract-pattern-binds (syntax->list #'(lhs ...)))])
|
||||
#`(begin
|
||||
(define-values (name2 name-predicate)
|
||||
(build-metafunction
|
||||
lang
|
||||
(list `side-conditions-rewritten ...)
|
||||
(list rhs-fns ...)
|
||||
#,(if prev-metafunction
|
||||
(let ([term-fn (syntax-local-value prev-metafunction)])
|
||||
#`(metafunc-proc-cps #,(term-fn-get-id term-fn)))
|
||||
#''())
|
||||
#,(if prev-metafunction
|
||||
(let ([term-fn (syntax-local-value prev-metafunction)])
|
||||
#`(metafunc-proc-rhss #,(term-fn-get-id term-fn)))
|
||||
#''())
|
||||
(λ (f/dom cps rhss)
|
||||
(make-metafunc-proc
|
||||
(let ([name (lambda (x) (f/dom x))]) name)
|
||||
(list (list (to-lw lhs-for-lw)
|
||||
(list (to-lw/uq side-cond) ...)
|
||||
(list (cons (to-lw bind-id)
|
||||
(to-lw bind-pat))
|
||||
...)
|
||||
(to-lw rhs))
|
||||
...)
|
||||
lang
|
||||
#t ;; multi-args?
|
||||
'name
|
||||
cps
|
||||
rhss
|
||||
(let ([name (lambda (x) (name-predicate x))]) name)))
|
||||
`dom-side-conditions-rewritten
|
||||
`codom-side-conditions-rewritten
|
||||
'name))
|
||||
(term-define-fn name name2)))))))))]
|
||||
[(_ prev-metafunction name lang clauses ...)
|
||||
(begin
|
||||
(unless (identifier? #'name)
|
||||
(raise-syntax-error 'define-metafunction "expected the name of a language" stx #'name))
|
||||
|
|
@ -913,7 +904,60 @@
|
|||
(raise-syntax-error 'define-metafunction "expected a lhs and rhs clause" stx clause)]))
|
||||
(syntax->list (syntax (clauses ...))))
|
||||
(raise-syntax-error 'define-metafunction "missing error check for bad syntax" stx))]))
|
||||
|
||||
|
||||
(define (split-out-contract stx syn-error-name rest)
|
||||
;; initial test determines if a contract is specified or not
|
||||
(cond
|
||||
[(pair? (syntax-e (car (syntax->list rest))))
|
||||
(values #f #'any (check-clauses stx syn-error-name rest))]
|
||||
[else
|
||||
(syntax-case rest ()
|
||||
[(id colon more ...)
|
||||
(begin
|
||||
(unless (eq? ': (syntax-e #'colon))
|
||||
(raise-syntax-error syn-error-name "expected a colon to follow the meta-function's name" stx #'colon))
|
||||
(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)) '->)
|
||||
(when (null? (cdr more))
|
||||
(raise-syntax-error syn-error-name "expected a range contract to follow the arrow" stx (car more)))
|
||||
(let ([doms (reverse dom-pats)]
|
||||
[codomain (car more)]
|
||||
[clauses (check-clauses stx syn-error-name (cddr more))])
|
||||
(values doms codomain clauses))]
|
||||
[else
|
||||
(loop (cdr more) (cons (car more) dom-pats))])))]
|
||||
[_
|
||||
(raise-syntax-error
|
||||
syn-error-name
|
||||
"expected the name of the meta-function, followed by its contract (or no name and no contract)"
|
||||
stx
|
||||
rest)])]))
|
||||
|
||||
(define (check-clauses stx syn-error-name rest)
|
||||
(syntax-case rest ()
|
||||
[([(lhs ...) roc ...] ...)
|
||||
rest]
|
||||
[([x roc ...] ...)
|
||||
(for-each
|
||||
(λ (x)
|
||||
(syntax-case x ()
|
||||
[(lhs ...) (void)]
|
||||
[x (raise-syntax-error syn-error-name "expected a function prototype" stx #'x)]))
|
||||
(syntax->list #'(x ...)))
|
||||
(raise-syntax-error syn-error-name "error checking failed.1" stx)]
|
||||
[(x ...)
|
||||
(for-each
|
||||
(λ (x)
|
||||
(syntax-case x ()
|
||||
[(stuff ...) (void)]
|
||||
[x (raise-syntax-error syn-error-name "expected a metafunction clause" stx #'x)]))
|
||||
(syntax->list #'(x ...)))
|
||||
(raise-syntax-error syn-error-name "error checking failed.2" stx)]))
|
||||
|
||||
|
||||
(define (extract-side-conditions name stx stuffs)
|
||||
(let loop ([stuffs (syntax->list stuffs)]
|
||||
|
|
@ -945,43 +989,50 @@
|
|||
"expected a side-condition or where clause"
|
||||
(car stuff))])]))]))))
|
||||
|
||||
(define (build-metafunction lang patterns rhss old-cps old-rhss wrap name)
|
||||
(define (build-metafunction lang patterns rhss old-cps old-rhss wrap dom-contract-pat rng-contract-pat name)
|
||||
(let ([compiled-patterns (append old-cps
|
||||
(map (λ (pat) (compile-pattern lang pat #t)) patterns))])
|
||||
(wrap
|
||||
(letrec ([metafunc/run (λ (x) (metafunc x #f))]
|
||||
[metafunc
|
||||
(λ (exp dom-test?)
|
||||
(let loop ([patterns compiled-patterns]
|
||||
[rhss (append old-rhss rhss)]
|
||||
[num (- (length old-cps))])
|
||||
(cond
|
||||
[(null? patterns)
|
||||
(if dom-test?
|
||||
#f
|
||||
(error name "no clauses matched for ~s" `(,name . ,exp)))]
|
||||
[else
|
||||
(let ([pattern (car patterns)]
|
||||
[rhs (car rhss)])
|
||||
(let ([mtchs (match-pattern pattern exp)])
|
||||
(cond
|
||||
[(not mtchs) (loop (cdr patterns)
|
||||
(cdr rhss)
|
||||
(+ num 1))]
|
||||
[(not (null? (cdr mtchs)))
|
||||
(error name "~a matched ~s ~a different ways"
|
||||
(if (< num 0)
|
||||
"a clause from an extended metafunction"
|
||||
(format "clause ~a" num))
|
||||
exp
|
||||
(length mtchs))]
|
||||
[else
|
||||
(if dom-test?
|
||||
#t
|
||||
(rhs metafunc/run (mtch-bindings (car mtchs))))])))])))])
|
||||
metafunc)
|
||||
compiled-patterns
|
||||
rhss)))
|
||||
(map (λ (pat) (compile-pattern lang pat #t)) patterns))]
|
||||
[dom-compiled-pattern (and dom-contract-pat (compile-pattern lang dom-contract-pat #t))]
|
||||
[rng-compiled-pattern (compile-pattern lang rng-contract-pat #t)])
|
||||
(values
|
||||
(wrap
|
||||
(letrec ([metafunc
|
||||
(λ (exp)
|
||||
(when dom-compiled-pattern
|
||||
(unless (match-pattern dom-compiled-pattern exp)
|
||||
(error name
|
||||
"~s is not in my domain"
|
||||
`(,name ,@exp))))
|
||||
(let loop ([patterns compiled-patterns]
|
||||
[rhss (append old-rhss rhss)]
|
||||
[num (- (length old-cps))])
|
||||
(cond
|
||||
[(null? patterns)
|
||||
(error name "no clauses matched for ~s" `(,name . ,exp))]
|
||||
[else
|
||||
(let ([pattern (car patterns)]
|
||||
[rhs (car rhss)])
|
||||
(let ([mtchs (match-pattern pattern exp)])
|
||||
(cond
|
||||
[(not mtchs) (loop (cdr patterns)
|
||||
(cdr rhss)
|
||||
(+ num 1))]
|
||||
[(not (null? (cdr mtchs)))
|
||||
(error name "~a matched ~s ~a different ways"
|
||||
(if (< num 0)
|
||||
"a clause from an extended metafunction"
|
||||
(format "clause ~a" num))
|
||||
`(,name ,@exp)
|
||||
(length mtchs))]
|
||||
[else
|
||||
(rhs metafunc (mtch-bindings (car mtchs)))])))])))])
|
||||
metafunc)
|
||||
compiled-patterns
|
||||
rhss)
|
||||
(if dom-compiled-pattern
|
||||
(λ (exp) (and (match-pattern dom-compiled-pattern exp) #t))
|
||||
(λ (exp) (and (ormap (λ (pat) (match-pattern pat exp)) compiled-patterns)
|
||||
#t))))))
|
||||
|
||||
(define-syntax (metafunction-form stx)
|
||||
(syntax-case stx ()
|
||||
|
|
@ -1574,10 +1625,9 @@
|
|||
|
||||
define-language
|
||||
define-extended-language
|
||||
|
||||
define-metafunction
|
||||
define-metafunction/extension
|
||||
define-multi-args-metafunction
|
||||
define-multi-args-metafunction/extension
|
||||
|
||||
(rename-out [metafunction-form metafunction])
|
||||
metafunction? metafunction-proc
|
||||
|
|
|
|||
|
|
@ -1,17 +1,24 @@
|
|||
;; require this file to run all of the test suites for redex.
|
||||
|
||||
(module run-tests mzscheme
|
||||
(require "pict-test.ss" ;; this one should go last, so it is listed first
|
||||
|
||||
"bitmap-test.ss" ;; second to last
|
||||
|
||||
"core-layout-test.ss"
|
||||
|
||||
"rg-test.ss"
|
||||
"term-test.ss"
|
||||
"tl-test.ss"
|
||||
"matcher-test.ss"
|
||||
"lw-test.ss")
|
||||
|
||||
(printf "\nWARNING: didn't run color-test.ss or subst-test.ss\n"))
|
||||
#lang scheme/base
|
||||
(require scheme/runtime-path)
|
||||
|
||||
(define test-files
|
||||
'("lw-test.ss"
|
||||
"matcher-test.ss"
|
||||
"tl-test.ss"
|
||||
"term-test.ss"
|
||||
"rg-test.ss"
|
||||
"core-layout-test.ss"
|
||||
"bitmap-test.ss"
|
||||
"pict-test.ss"))
|
||||
|
||||
(define-runtime-path here ".")
|
||||
|
||||
(for-each
|
||||
(λ (test-file)
|
||||
(printf "requiring ~a\n" test-file)
|
||||
(dynamic-require (build-path here test-file) #f))
|
||||
test-files)
|
||||
|
||||
(printf "\nWARNING: didn't run color-test.ss or subst-test.ss\n")
|
||||
|
|
|
|||
|
|
@ -1,10 +1,8 @@
|
|||
(module term-fn mzscheme
|
||||
(provide make-term-fn
|
||||
term-fn?
|
||||
term-fn-multi-arg?
|
||||
term-fn-get-id)
|
||||
|
||||
(define-values (struct-type make-term-fn term-fn? term-fn-get term-fn-set!)
|
||||
(make-struct-type 'term-fn #f 2 0))
|
||||
(define term-fn-get-id (make-struct-field-accessor term-fn-get 0))
|
||||
(define term-fn-multi-arg? (make-struct-field-accessor term-fn-get 1)))
|
||||
(make-struct-type 'term-fn #f 1 0))
|
||||
(define term-fn-get-id (make-struct-field-accessor term-fn-get 0)))
|
||||
|
|
|
|||
|
|
@ -31,15 +31,6 @@
|
|||
(and (identifier? (syntax f))
|
||||
(term-fn? (syntax-local-value (syntax f) (λ () #f))))
|
||||
(let ([term-fn (syntax-local-value (syntax f) (λ () #f))])
|
||||
|
||||
(unless (term-fn-multi-arg? term-fn)
|
||||
(let ([arg-count (length (syntax->list #'(arg ...)))])
|
||||
(unless (= 1 arg-count)
|
||||
(raise-syntax-error 'term
|
||||
(format "single argument metafunction supplied with ~a arguments"
|
||||
arg-count)
|
||||
orig-stx
|
||||
stx))))
|
||||
(with-syntax ([f (term-fn-get-id term-fn)]
|
||||
[(f-results) (generate-temporaries '(f-results))])
|
||||
(let d-loop ([arg-dots (loop (syntax (arg ...)) depth)]
|
||||
|
|
@ -121,20 +112,19 @@
|
|||
(with-syntax ([(g ...) (generate-temporaries (syntax (f ...)))])
|
||||
(syntax
|
||||
(let ([g rhs] ...)
|
||||
(let-syntax ([f (make-term-fn #'g #t)] ...)
|
||||
(let-syntax ([f (make-term-fn #'g)] ...)
|
||||
body1
|
||||
body2 ...))))]))
|
||||
|
||||
(define-syntax (term-define-fn stx)
|
||||
(syntax-case stx ()
|
||||
[(_ id exp multi-arg?)
|
||||
[(_ id exp)
|
||||
(with-syntax ([(id2) (generate-temporaries (syntax (id)))])
|
||||
(syntax
|
||||
(begin
|
||||
(define id2 exp)
|
||||
(define-syntax id
|
||||
(make-term-fn ((syntax-local-certifier) #'id2)
|
||||
multi-arg?)))))]))
|
||||
(make-term-fn ((syntax-local-certifier) #'id2))))))]))
|
||||
|
||||
(define-syntax (term-let stx)
|
||||
(syntax-case stx ()
|
||||
|
|
|
|||
|
|
@ -205,20 +205,18 @@
|
|||
;
|
||||
|
||||
|
||||
(define-metafunction f
|
||||
grammar
|
||||
[(side-condition (number_1 number_2)
|
||||
(< (term number_1)
|
||||
(term number_2)))
|
||||
(define-metafunction grammar
|
||||
[(f (side-condition (number_1 number_2)
|
||||
(< (term number_1)
|
||||
(term number_2))))
|
||||
x]
|
||||
[(number 1) y]
|
||||
[(number_1 2) ,(+ (term number_1) 2)]
|
||||
[(4 4) q]
|
||||
[(4 4) r])
|
||||
[(f (number 1)) y]
|
||||
[(f (number_1 2)) ,(+ (term number_1) 2)]
|
||||
[(f (4 4)) q]
|
||||
[(f (4 4)) r])
|
||||
|
||||
(define-metafunction g
|
||||
grammar
|
||||
[X x])
|
||||
(define-metafunction grammar
|
||||
[(g X) x])
|
||||
|
||||
(test (term (f (1 17))) 'x)
|
||||
(test (term (f (11 1))) 'y)
|
||||
|
|
@ -230,9 +228,8 @@
|
|||
|
||||
;; match one clause two ways => error
|
||||
(let ()
|
||||
(define-metafunction ll
|
||||
empty-language
|
||||
[(number_1 ... number_2 ...) 4])
|
||||
(define-metafunction empty-language
|
||||
[(ll (number_1 ... number_2 ...)) 4])
|
||||
(test (with-handlers ((exn? (λ (x) 'exn-raised)))
|
||||
(term (ll ()))
|
||||
'no-exn)
|
||||
|
|
@ -246,111 +243,110 @@
|
|||
(test (with-handlers ((exn? (λ (x) 'exn-raised))) (term (f mis-match)) 'no-exn)
|
||||
'exn-raised)
|
||||
|
||||
(define-metafunction h
|
||||
grammar
|
||||
[(M_1 M_2) ((h M_2) (h M_1))]
|
||||
[number_1 ,(+ (term number_1) 1)])
|
||||
(define-metafunction grammar
|
||||
[(h (M_1 M_2)) ((h M_2) (h M_1))]
|
||||
[(h number_1) ,(+ (term number_1) 1)])
|
||||
|
||||
(test (term (h ((1 2) 3)))
|
||||
(term (4 (3 2))))
|
||||
|
||||
(define-metafunction h2
|
||||
grammar
|
||||
[(Q_1 ...) ((h2 Q_1) ...)]
|
||||
[variable z])
|
||||
(define-metafunction grammar
|
||||
[(h2 (Q_1 ...)) ((h2 Q_1) ...)]
|
||||
[(h2 variable) z])
|
||||
|
||||
(test (term (h2 ((x y) a b c)))
|
||||
(term ((z z) z z z)))
|
||||
|
||||
(let ()
|
||||
(define-metafunction f empty-language
|
||||
[(1) 1]
|
||||
[(2) 2]
|
||||
[3 3])
|
||||
(test (in-domain? (term 1) f) #f)
|
||||
(test (in-domain? (term (1)) f) #t)
|
||||
(test (in-domain? (term ((1))) f) #f)
|
||||
(test (in-domain? (term 3) f) #t)
|
||||
(test (in-domain? (term 4) f) #f))
|
||||
(define-metafunction empty-language
|
||||
[(f (1)) 1]
|
||||
[(f (2)) 2]
|
||||
[(f 3) 3])
|
||||
(test (in-domain? (f 1)) #f)
|
||||
(test (in-domain? (f (1))) #t)
|
||||
(test (in-domain? (f ((1)))) #f)
|
||||
(test (in-domain? (f 3)) #t)
|
||||
(test (in-domain? (f 4)) #f))
|
||||
|
||||
(let ()
|
||||
(define-multi-args-metafunction f empty-language
|
||||
[(1) 1]
|
||||
[(2) 2]
|
||||
[(3 4) 3])
|
||||
(test (in-domain? (term 1) f) #f)
|
||||
(test (in-domain? (term (1)) f) #t)
|
||||
(test (in-domain? (term ((1))) f) #f)
|
||||
(test (in-domain? (term (3 4)) f) #t)
|
||||
(test (in-domain? (term 3) f) #f))
|
||||
(define-metafunction empty-language
|
||||
f : number -> number
|
||||
[(f 1) 1])
|
||||
(test (in-domain? (f 1)) #t)
|
||||
(test (in-domain? (f 2)) #t)
|
||||
(test (in-domain? (f x)) #f))
|
||||
|
||||
(let ()
|
||||
(define-metafunction empty-language
|
||||
[(f x) x])
|
||||
(test
|
||||
(term-let ((y 'x))
|
||||
(in-domain? (f y)))
|
||||
#t)
|
||||
(test
|
||||
(term-let ((y 'z))
|
||||
(in-domain? (f y)))
|
||||
#f))
|
||||
|
||||
;; mutually recursive metafunctions
|
||||
(define-metafunction odd
|
||||
grammar
|
||||
[zero #f]
|
||||
[(add1 UN_1) (even UN_1)])
|
||||
(define-metafunction grammar
|
||||
[(odd zero) #f]
|
||||
[(odd (add1 UN_1)) (even UN_1)])
|
||||
|
||||
(define-metafunction even
|
||||
grammar
|
||||
[zero #t]
|
||||
[(add1 UN_1) (odd UN_1)])
|
||||
(define-metafunction grammar
|
||||
[(even zero) #t]
|
||||
[(even (add1 UN_1)) (odd UN_1)])
|
||||
|
||||
(test (term (odd (add1 (add1 (add1 (add1 zero))))))
|
||||
(term #f))
|
||||
|
||||
(let ()
|
||||
(define-metafunction pRe
|
||||
empty-language
|
||||
[xxx 1])
|
||||
(define-metafunction empty-language
|
||||
[(pRe xxx) 1])
|
||||
|
||||
(define-metafunction Merge-Exns
|
||||
empty-language
|
||||
[any_1 any_1])
|
||||
(define-metafunction empty-language
|
||||
[(Merge-Exns any_1) any_1])
|
||||
|
||||
(test (term (pRe (Merge-Exns xxx)))
|
||||
1))
|
||||
|
||||
(let ()
|
||||
(define-metafunction f
|
||||
empty-language
|
||||
[(x) ,(term-let ([var-should-be-lookedup 'y]) (term (f var-should-be-lookedup)))]
|
||||
[y y]
|
||||
[var-should-be-lookedup var-should-be-lookedup]) ;; taking this case is bad!
|
||||
(define-metafunction empty-language
|
||||
[(f (x)) ,(term-let ([var-should-be-lookedup 'y]) (term (f var-should-be-lookedup)))]
|
||||
[(f y) y]
|
||||
[(f var-should-be-lookedup) var-should-be-lookedup]) ;; taking this case is bad!
|
||||
|
||||
(test (term (f (x))) (term y)))
|
||||
|
||||
(let ()
|
||||
(define-metafunction f
|
||||
empty-language
|
||||
[(x) (x ,@(term-let ([var-should-be-lookedup 'y]) (term (f var-should-be-lookedup))) x)]
|
||||
[y (y)]
|
||||
[var-should-be-lookedup (var-should-be-lookedup)]) ;; taking this case is bad!
|
||||
(define-metafunction empty-language
|
||||
[(f (x)) (x ,@(term-let ([var-should-be-lookedup 'y]) (term (f var-should-be-lookedup))) x)]
|
||||
[(f y) (y)]
|
||||
[(f var-should-be-lookedup) (var-should-be-lookedup)]) ;; taking this case is bad!
|
||||
|
||||
(test (term (f (x))) (term (x y x))))
|
||||
|
||||
(let ()
|
||||
(define-metafunction f
|
||||
empty-language
|
||||
[(any_1 any_2)
|
||||
(define-metafunction empty-language
|
||||
[(f (any_1 any_2))
|
||||
case1
|
||||
(side-condition (not (equal? (term any_1) (term any_2))))
|
||||
(side-condition (not (equal? (term any_1) 'x)))]
|
||||
[(any_1 any_2)
|
||||
[(f (any_1 any_2))
|
||||
case2
|
||||
(side-condition (not (equal? (term any_1) (term any_2))))]
|
||||
[(any_1 any_2)
|
||||
[(f (any_1 any_2))
|
||||
case3])
|
||||
(test (term (f (q r))) (term case1))
|
||||
(test (term (f (x y))) (term case2))
|
||||
(test (term (f (x x))) (term case3)))
|
||||
|
||||
(let ()
|
||||
(define-metafunction f
|
||||
empty-language
|
||||
[(n number) (n number)]
|
||||
[(a any) (a any)]
|
||||
[(v variable) (v variable)]
|
||||
[(s string) (s string)])
|
||||
(define-metafunction empty-language
|
||||
[(f (n number)) (n number)]
|
||||
[(f (a any)) (a any)]
|
||||
[(f (v variable)) (v variable)]
|
||||
[(f (s string)) (s string)])
|
||||
(test (term (f (n 1))) (term (n 1)))
|
||||
(test (term (f (a (#f "x" whatever)))) (term (a (#f "x" whatever))))
|
||||
(test (term (f (v x))) (term (v x)))
|
||||
|
|
@ -358,48 +354,48 @@
|
|||
|
||||
;; test ..._1 patterns
|
||||
(let ()
|
||||
(define-metafunction zip empty-language
|
||||
[((variable_id ..._1) (number_val ..._1))
|
||||
(define-metafunction empty-language
|
||||
[(zip ((variable_id ..._1) (number_val ..._1)))
|
||||
((variable_id number_val) ...)])
|
||||
|
||||
(test (term (zip ((a b) (1 2)))) (term ((a 1) (b 2)))))
|
||||
|
||||
(let ()
|
||||
(define-multi-args-metafunction f empty-language
|
||||
[(any_1 any_2 any_3) (any_3 any_2 any_1)])
|
||||
(define-metafunction empty-language
|
||||
[(f any_1 any_2 any_3) (any_3 any_2 any_1)])
|
||||
(test (term (f 1 2 3))
|
||||
(term (3 2 1))))
|
||||
|
||||
(let ()
|
||||
(define-metafunction f empty-language
|
||||
[(any_1 any_2 any_3) 3])
|
||||
(define-metafunction/extension g empty-language f
|
||||
[(any_1 any_2) 2])
|
||||
(define-metafunction empty-language
|
||||
[(f (any_1 any_2 any_3)) 3])
|
||||
(define-metafunction/extension f empty-language
|
||||
[(g (any_1 any_2)) 2])
|
||||
(test (term (g (1 2))) 2)
|
||||
(test (term (g (1 2 3))) 3))
|
||||
|
||||
(let ()
|
||||
(define-multi-args-metafunction f empty-language
|
||||
[(any_1 any_2 any_3) 3])
|
||||
(define-multi-args-metafunction/extension g empty-language f
|
||||
[(any_1 any_2) 2])
|
||||
(define-metafunction empty-language
|
||||
[(f any_1 any_2 any_3) 3])
|
||||
(define-metafunction/extension f empty-language
|
||||
[(g any_1 any_2) 2])
|
||||
(test (term (g 1 2)) 2)
|
||||
(test (term (g 1 2 3)) 3))
|
||||
|
||||
(let ()
|
||||
(define-multi-args-metafunction f empty-language
|
||||
[(number_1 number_2) (f number_1)])
|
||||
(define-multi-args-metafunction/extension g empty-language f
|
||||
[(number_1) number_1])
|
||||
(define-multi-args-metafunction h empty-language
|
||||
[(number_1 number_2) (h number_1)]
|
||||
[(number_1) number_1])
|
||||
(define-metafunction empty-language
|
||||
[(f number_1 number_2) (f number_1)])
|
||||
(define-metafunction/extension f empty-language
|
||||
[(g number_1) number_1])
|
||||
(define-metafunction empty-language
|
||||
[(h number_1 number_2) (h number_1)]
|
||||
[(h number_1) number_1])
|
||||
(test (term (g 11 17)) 11)
|
||||
(test (term (h 11 17)) 11))
|
||||
|
||||
(let ()
|
||||
(define-metafunction f empty-language
|
||||
[(number_1 number_2)
|
||||
(define-metafunction empty-language
|
||||
[(f (number_1 number_2))
|
||||
number_3
|
||||
(where number_3 (+ (term number_1) (term number_2)))])
|
||||
(test (term (f (11 17))) 28))
|
||||
|
|
@ -862,13 +858,12 @@
|
|||
1)
|
||||
|
||||
(require (lib "list.ss"))
|
||||
;; free-vars : e -> (listof x)
|
||||
(define-metafunction free-vars
|
||||
lc-lang
|
||||
[(e_1 e_2 ...)
|
||||
(define-metafunction lc-lang
|
||||
free-vars : e -> (listof x)
|
||||
[(free-vars (e_1 e_2 ...))
|
||||
,(apply append (term ((free-vars e_1) (free-vars e_2) ...)))]
|
||||
[x_1 ,(list (term x_1))]
|
||||
[(lambda (x_1 ...) e_1)
|
||||
[(free-vars x_1) ,(list (term x_1))]
|
||||
[(free-vars (lambda (x_1 ...) e_1))
|
||||
,(foldr remq (term (free-vars e_1)) (term (x_1 ...)))])
|
||||
|
||||
(test (term (free-vars (lambda (x) (x y))))
|
||||
|
|
|
|||
|
|
@ -622,23 +622,26 @@ Returns the names of all of the reduction relation's clauses
|
|||
(or false if there is no name for a given clause).
|
||||
}
|
||||
|
||||
> (compatible-closure <reduction-relation> <lang> <non-terminal>) SYNTAX
|
||||
@defform[(compatible-closure reduction-relation lang non-terminal)]{
|
||||
|
||||
This accepts a reduction, a language, the name of a
|
||||
non-terminal in the language and returns the compatible
|
||||
closure of the reduction for the specified non-terminal.
|
||||
}
|
||||
|
||||
> (context-closure <reduction-relation> <lang> <pattern>) SYNTAX
|
||||
@defform[(context-closure reduction-relation lang pattern)]{
|
||||
|
||||
This accepts a reduction, a language, a pattern representing
|
||||
a context (ie, that can be used as the first argument to
|
||||
`in-hole'; often just a non-terminal) in the language and
|
||||
returns the closure of the reduction in that context.
|
||||
}
|
||||
|
||||
> (define-metafunction name <language-exp>
|
||||
[<pattern> <rhs-expression> (side-condition <exp>) ...] ...) SYNTAX
|
||||
@defform[(define-metafunction language-exp
|
||||
[(name pattern ...) exp (side-condition exp) ...]
|
||||
...)]{
|
||||
|
||||
The `define-metafunction' form builds a function on
|
||||
The @scheme[define-metafunction] form builds a function on
|
||||
sexpressions according to the pattern and right-hand-side
|
||||
expressions. The first argument indicates the language used
|
||||
to resolve non-terminals in the pattern expressions. Each of
|
||||
|
|
@ -646,8 +649,8 @@ the rhs-expressions is implicitly wrapped in `term'. In
|
|||
addition, recursive calls in the right-hand side of the
|
||||
metafunction clauses should appear inside `term'.
|
||||
|
||||
If specified, the side-conditions are collected with an
|
||||
`and' and used as guards on the case being matched. The
|
||||
If specified, the side-conditions are collected with
|
||||
@scheme[and] and used as guards on the case being matched. The
|
||||
argument to each side-condition should be a Scheme
|
||||
expression, and the pattern variables in the <pattern> are
|
||||
bound in that expression.
|
||||
|
|
@ -655,14 +658,15 @@ bound in that expression.
|
|||
As an example, this metafunction finds the free variables in
|
||||
an expression in the lc-lang above:
|
||||
|
||||
;; free-vars : e -> (listof x)
|
||||
(define-metafunction free-vars
|
||||
lc-lang
|
||||
[(e_1 e_2 ...)
|
||||
@schemeblock[
|
||||
(define-metafunction lc-lang
|
||||
free-vars : e -> (x ...)
|
||||
[(free-vars (e_1 e_2 ...))
|
||||
,(apply append (term ((free-vars e_1) (free-vars e_2) ...)))]
|
||||
[x_1 ,(list (term x_1))]
|
||||
[(lambda (x_1 ...) e_1)
|
||||
[(free-vars x_1) ,(list (term x_1))]
|
||||
[(free-vars (lambda (x_1 ...) e_1))
|
||||
,(foldr remq (term (free-vars e_1)) (term (x_1 ...)))])
|
||||
]
|
||||
|
||||
The first argument to define-metafunction is the grammar
|
||||
(defined above). Following that are three cases, one for
|
||||
|
|
@ -673,49 +677,22 @@ application are the free variables of each of the subterms;
|
|||
the free variables of a variable is just the variable
|
||||
itself, and the free variables of a lambda expression are
|
||||
the free variables of the body, minus the bound parameters.
|
||||
}
|
||||
|
||||
> (define-metafunction/extension name <language-exp> extending-name
|
||||
[<pattern> <rhs-expression> (side-condition <exp>) ...] ...) SYNTAX
|
||||
|
||||
@defform[(define-metafunction/extension extending-name language-exp
|
||||
[(name pattern ...) rhs-expression (side-condition <exp>) ...]
|
||||
...)]{
|
||||
This defines a metafunction as an extension of an existing
|
||||
one. The extended metafunction behaves as if the original
|
||||
patterns were in this definitions, with the name of the
|
||||
function fixed up so that recursive functions behave as expected.
|
||||
function fixed up to be @scheme[extending-name].
|
||||
}
|
||||
|
||||
> (define-multi-args-metafunction name <language-exp>
|
||||
[<pattern> <rhs-expression> (side-condition <exp>) ...] ...) SYNTAX
|
||||
|
||||
Like define-metafunction, this defines a
|
||||
metafunction. Unlike it, this defines a metafunction that
|
||||
accepts multiple arguments.
|
||||
|
||||
There are two significant differences:
|
||||
|
||||
- patterns match the entire argument list, rather than just
|
||||
matching the single argument
|
||||
- the typesetting for define-multi-args-metafunction uses
|
||||
commas to separate the arguments in the definition
|
||||
and at the callsites.
|
||||
|
||||
> (define-multi-arg-metafunction/extension name <language-exp> extending-name
|
||||
[<pattern> <rhs-expression> (side-condition <exp>) ...] ...) SYNTAX
|
||||
|
||||
Like define-metafunction/extension, this defines a
|
||||
metafunction as an extension of an existing one, but this
|
||||
time for multi-argument metafunctions.
|
||||
|
||||
> (in-domain? <term> <metafunction-name>)
|
||||
|
||||
Returns #t if <term> is in the domain of the specified
|
||||
metafunction.
|
||||
|
||||
If the metafunction is defined with define-metafunction,
|
||||
then the term representing the argument should appear
|
||||
exactly as it appears in a call to the metafunction.
|
||||
|
||||
If the metafunction is defined with
|
||||
define-multi-args-metafunction, then the arguments should
|
||||
be parenthesized.
|
||||
@defform[(in-domain? (metafunction-name term ...))]{
|
||||
Returns @scheme[#t] if the inputs specified to @scheme[metafunction-name] are
|
||||
legtimate inputs according to @scheme[metafunction-name]'s contract,
|
||||
and @scheme[#f] otherwise.
|
||||
}
|
||||
|
||||
> (test-equal e1 e2) SYNTAX
|
||||
|
||||
|
|
|
|||
|
|
@ -26,8 +26,6 @@
|
|||
none?
|
||||
define-metafunction
|
||||
define-metafunction/extension
|
||||
define-multi-args-metafunction
|
||||
define-multi-args-metafunction/extension
|
||||
metafunction
|
||||
in-domain?)
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user