(module reduction-semantics mzscheme
(require "matcher.ss"
"struct.ss"
"term.ss"
"loc-wrapper.ss"
(lib "list.ss")
(lib "etc.ss"))
(require-for-syntax (lib "name.ss" "syntax")
"rewrite-side-conditions.ss"
"term-fn.ss"
(lib "boundmap.ss" "syntax"))
(define (language-nts lang)
(hash-table-map (compiled-lang-ht lang) (λ (x y) x)))
(define-syntax (term-match/single stx)
(syntax-case stx ()
[(_ lang [pattern rhs] ...)
(with-syntax ([(((names ...) (names/ellipses ...)) ...)
(map (λ (x) (let-values ([(names names/ellipses) (extract-names 'term-match/single x)])
(list names names/ellipses)))
(syntax->list (syntax (pattern ...))))]
[(side-conditions-rewritten ...)
(map (λ (x) (rewrite-side-conditions/check-errs 'term-match x))
(syntax->list (syntax (pattern ...))))]
[(cp-x ...) (generate-temporaries #'(pattern ...))])
#'(let ([lang-x lang])
(let ([cp-x (compile-pattern lang-x `side-conditions-rewritten)] ...)
(λ (exp)
(let/ec k
(let ([match (match-pattern cp-x exp)])
(when match
(unless (null? (cdr match))
(error 'term-match "pattern ~s matched term ~e multiple ways"
'pattern
exp))
(k (term-let ([names/ellipses (lookup-binding (mtch-bindings (car match)) 'names)] ...)
rhs))))
...
(error 'term-match "no patterns matched ~e" exp))))))]))
(define-syntax (term-match stx)
(syntax-case stx ()
[(_ lang [pattern rhs] ...)
(with-syntax ([(((names ...) (names/ellipses ...)) ...)
(map (λ (x) (let-values ([(names names/ellipses) (extract-names 'term-match x)])
(list names names/ellipses)))
(syntax->list (syntax (pattern ...))))]
[(side-conditions-rewritten ...)
(map (λ (x) (rewrite-side-conditions/check-errs 'term-match x))
(syntax->list (syntax (pattern ...))))]
[(cp-x ...) (generate-temporaries #'(pattern ...))])
#'(let ([lang-x lang])
(let ([cp-x (compile-pattern lang-x `side-conditions-rewritten)] ...)
(λ (exp)
(append
(let ([matches (match-pattern cp-x exp)])
(if matches
(map (λ (match)
(term-let ([names/ellipses (lookup-binding (mtch-bindings match) 'names)] ...)
rhs))
matches)
'())) ...)))))]))
(define-syntax (compatible-closure stx)
(syntax-case stx ()
[(_ red lang nt)
(identifier? (syntax nt))
(with-syntax ([side-conditions-rewritten (rewrite-side-conditions/check-errs 'compatible-closure (syntax (cross nt)))])
(syntax (do-context-closure red lang `side-conditions-rewritten 'compatible-closure)))]
[(_ red lang nt)
(raise-syntax-error 'compatible-closure "expected a non-terminal as last argument" stx (syntax nt))]))
(define-syntax (context-closure stx)
(syntax-case stx ()
[(_ red lang pattern)
(with-syntax ([side-conditions-rewritten (rewrite-side-conditions/check-errs 'context-closure (syntax pattern))])
(syntax
(do-context-closure
red
lang
`side-conditions-rewritten
'context-closure)))]))
(define (do-context-closure red lang pat name)
(unless (reduction-relation? red)
(error name "expected <reduction-relation> as first argument, got ~e" red))
(unless (compiled-lang? lang)
(error name "expected <lang> as second argument, got ~e" lang))
(let ([cp (compile-pattern
lang
`(in-hole (name ctxt ,pat)
(name exp any)))])
(make-reduction-relation
lang
(map
(λ (f)
(λ (main-exp exp extend acc)
(let loop ([ms (or (match-pattern cp exp) '())]
[acc acc])
(cond
[(null? ms) acc]
[else
(let* ([mtch (car ms)]
[bindings (mtch-bindings mtch)])
(loop (cdr ms)
(f main-exp
(lookup-binding bindings 'exp)
(λ (x) (extend (plug (lookup-binding bindings 'ctxt) x)))
acc)))]))))
(reduction-relation-procs red))
(reduction-relation-rule-names red)
(reduction-relation-lws red))))
(define (do-test-match lang pat)
(unless (compiled-lang? lang)
(error 'test-match "expected first argument to be a language, got ~e" lang))
(let ([cpat (compile-pattern lang pat)])
(λ (exp)
(match-pattern cpat exp))))
(define-syntax (--> stx) (raise-syntax-error '--> "used outside of reduction-relation"))
(define-syntax (fresh stx) (raise-syntax-error 'fresh "used outside of reduction-relation"))
(define-syntax (where stx) (raise-syntax-error 'where "used outside of reduction-relation"))
(define (apply-reduction-relation/tag-with-names p v)
(let loop ([procs (reduction-relation-procs p)]
[acc '()])
(cond
[(null? procs) acc]
[else
(loop (cdr procs)
((car procs) v v values acc))])))
(define (apply-reduction-relation p v) (map cadr (apply-reduction-relation/tag-with-names p v)))
(define-for-syntax (extract-pattern-binds lhs)
(let loop ([lhs lhs])
(syntax-case* lhs (name) (lambda (a b) (eq? (syntax-e a) (syntax-e b)))
[(name id expr)
(identifier? #'id)
(cons (cons #'id #'expr) (loop #'expr))]
[(a . b)
(append (loop #'a) (loop #'b))]
[_else null])))
(define-for-syntax (extract-term-let-binds lhs)
(let loop ([lhs lhs])
(syntax-case* lhs (term-let) (lambda (a b) (eq? (syntax-e a) (syntax-e b)))
[(term-let ((x e1) ...) e2 ...)
(append (map cons
(syntax->list #'(x ...))
(syntax->list #'(e1 ...)))
(loop #'(e2 ...)))]
[(a . b)
(append (loop #'a) (loop #'b))]
[_else null])))
(define-syntax-set (-reduction-relation)
(define (-reduction-relation/proc stx)
(syntax-case stx ()
[(_ lang args ...)
(with-syntax ([(rules ...) (before-where (syntax (args ...)))]
[(shortcuts ...) (after-where (syntax (args ...)))])
(with-syntax ([(lws ...) (map rule->lws (syntax->list #'(rules ...)))])
(reduction-relation/helper
stx
(syntax lang)
(syntax->list (syntax (rules ...)))
(syntax->list (syntax (shortcuts ...)))
#'(list lws ...))))]))
(define (before-where stx)
(let loop ([lst (syntax->list stx)])
(cond
[(null? lst) null]
[else
(let ([fst (car lst)])
(syntax-case (car lst) (where)
[where null]
[else (cons (car lst) (loop (cdr lst)))]))])))
(define (after-where stx)
(let loop ([lst (syntax->list stx)])
(cond
[(null? lst) null]
[else
(let ([fst (car lst)])
(syntax-case (car lst) (where)
[where (cdr lst)]
[else (loop (cdr lst))]))])))
(define (rule->lws rule)
(syntax-case rule ()
[(arrow lhs rhs stuff ...)
(let-values ([(label scs fvars wheres)
(let loop ([stuffs (syntax->list #'(stuff ...))]
[label #f]
[scs null]
[fvars null]
[wheres null])
(cond
[(null? stuffs) (values label (reverse scs) (reverse fvars) (reverse wheres))]
[else
(syntax-case (car stuffs) (where fresh variable-not-in)
[(fresh xs ...)
(loop (cdr stuffs)
label
scs
(append
(reverse (map (λ (x)
(syntax-case x ()
[x
(identifier? #'x)
#'x]
[(x whatever)
(identifier? #'x)
#'x]
[((y dots) (x dots2))
(datum->syntax-object
#f
`(,(syntax-object->datum #'y) ...)
#'y)]
[((y dots) (x dots2) whatever)
(datum->syntax-object
#f
`(,(syntax-object->datum #'y) ...)
#'y)]))
(syntax->list #'(xs ...))))
fvars)
wheres)]
[(where x e)
(loop (cdr stuffs)
label
scs
fvars
(cons #'(x e) wheres))]
[(side-condition sc)
(loop (cdr stuffs)
label
(cons #'sc scs)
fvars
wheres)]
[x
(identifier? #'x)
(loop (cdr stuffs)
#''x
scs
fvars
wheres)]
[x
(string? (syntax-e #'x))
(loop (cdr stuffs)
#'x
scs
fvars
wheres)])]))])
(with-syntax ([(scs ...) scs]
[(fvars ...) fvars]
[((where-id where-expr) ...) wheres]
[((bind-id . bind-pat) ...)
(append (extract-pattern-binds #'lhs)
(extract-term-let-binds #'rhs))])
#`(make-rule-pict 'arrow
(to-loc-wrapper lhs)
(to-loc-wrapper rhs)
#,label
(list (to-loc-wrapper/uq scs) ...)
(list (to-loc-wrapper fvars) ...)
(list (cons (to-loc-wrapper bind-id)
(to-loc-wrapper bind-pat))
...
(cons (to-loc-wrapper where-id)
(to-loc-wrapper where-expr))
...))))]))
(define (reduction-relation/helper stx lang-exp rules shortcuts lws)
(let ([ht (make-module-identifier-mapping)]
[all-top-levels '()]
[wheres (make-module-identifier-mapping)])
(for-each (λ (shortcut)
(syntax-case shortcut ()
[((lhs-arrow lhs-from lhs-to)
(rhs-arrow rhs-from rhs-to))
(begin
(table-cons! wheres #'lhs-arrow #'rhs-arrow)
(table-cons! ht (syntax rhs-arrow) shortcut))]
[((a b c) d)
(raise-syntax-error
'reduction-relation
"malformed shortcut, expected right-hand side to have three sub-expressions"
stx (syntax d))]
[(a b)
(raise-syntax-error
'reduction-relation
"malformed shortcut, expected left-hand side to have three sub-expressions"
stx (syntax a))]
[(a b c d ...)
(raise-syntax-error 'reduction-relation
"malformed shortcut, expected only two subparts for a shortcut definition, found an extra one"
stx
(syntax c))]
[_ (raise-syntax-error 'reduction-relation
"malformed shortcut"
stx shortcut)]))
shortcuts)
(for-each (λ (rule)
(syntax-case rule ()
[(arrow . rst)
(begin
(set! all-top-levels (cons #'arrow all-top-levels))
(table-cons! ht (syntax arrow) rule))]))
rules)
(unless (module-identifier-mapping-get ht (syntax -->) (λ () #f))
(raise-syntax-error 'reduction-relation "no --> rules" stx))
(for-each (λ (tl)
(let loop ([id tl])
(unless (module-identifier=? #'--> id)
(let ([nexts
(module-identifier-mapping-get
wheres id
(λ ()
(raise-syntax-error
'reduction-relation
(format "the ~s relation is not defined"
(syntax-object->datum id))
stx
id)))])
(for-each loop nexts)))))
all-top-levels)
(let ([name-ht (make-hash-table)])
(with-syntax ([lang-exp lang-exp]
[(top-level ...) (get-choices stx ht (syntax lang-x) (syntax -->) name-ht)]
[(rule-names ...) (hash-table-map name-ht (λ (k v) k))]
[lws lws])
(syntax
(let ([lang-x lang-exp])
(make-reduction-relation
lang-x
(list top-level ...)
'(rule-names ...)
lws)))))))
(define (get-choices stx bm lang id name-table)
(reverse
(map (λ (x) (get-tree stx bm lang x name-table))
(module-identifier-mapping-get
bm id
(λ ()
(raise-syntax-error 'reduction-relation
(format "no rules use ~a" (syntax-object->datum id))
stx
id))))))
(define (get-tree stx bm lang case-stx name-table)
(syntax-case case-stx ()
[(arrow from to extras ...)
(do-leaf stx
lang
name-table
(syntax from)
(syntax to)
(syntax->list (syntax (extras ...))))]
[((lhs-arrow lhs-frm-id lhs-to-id) (rhs-arrow rhs-from rhs-to))
(let-values ([(names names/ellipses) (extract-names 'reduction-relation (syntax rhs-from))])
(with-syntax ([(names ...) names]
[(names/ellipses ...) names/ellipses]
[side-conditions-rewritten (rewrite-side-conditions/check-errs
'reduction-relation
(rewrite-node-pat (syntax-e (syntax lhs-frm-id))
(syntax-object->datum (syntax rhs-from))))]
[lang lang]
[(child-procs ...) (get-choices stx bm lang (syntax lhs-arrow) name-table)])
(syntax
(do-node-match
lang
'lhs-frm-id
'lhs-to-id
`side-conditions-rewritten
(λ (bindings rhs-binder)
(term-let ([lhs-to-id rhs-binder]
[names/ellipses (lookup-binding bindings 'names)] ...)
(term rhs-to)))
(list child-procs ...)))))]))
(define (rewrite-node-pat id term)
(let loop ([term term])
(cond
[(eq? id term) `(name ,id any)]
[(pair? term) (cons (loop (car term))
(loop (cdr term)))]
[else term])))
(define (do-leaf stx lang name-table from to extras)
(let-values ([(name fresh-vars side-conditions wheres) (process-extras stx name-table extras)])
(let-values ([(names names/ellipses) (extract-names 'reduction-relation from)])
(with-syntax ([side-conditions-rewritten
(rewrite-side-conditions/check-errs
'reduction-relation
(if (null? side-conditions)
from
(with-syntax ([(sc ...) side-conditions]
[from from])
(syntax (side-condition from (and sc ...))))))]
[to to]
[name name]
[lang lang]
[(names ...) names]
[(names/ellipses ...) names/ellipses]
[(fresh-var-clauses ...)
(map (λ (fv-clause)
(syntax-case fv-clause ()
[x
(identifier? #'x)
#'[x (variable-not-in main 'x)]]
[(x name)
(identifier? #'x)
#'[x (let ([the-name (term name)])
(verify-name-ok the-name)
(variable-not-in main the-name))]]
[((y) (x ...))
#`[(y #,'...)
(variables-not-in main
(map (λ (_ignore_) 'y)
(term (x ...))))]]
[((y) (x ...) names)
#`[(y #,'...)
(let ([the-names (term names)]
[len-counter (term (x ...))])
(verify-names-ok the-names len-counter)
(variables-not-in main the-names))]]))
fresh-vars)])
#`(do-leaf-match
lang
name
`side-conditions-rewritten
(λ (main bindings)
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
(term-let (fresh-var-clauses ...)
#,(bind-wheres wheres
#'(term to))))))))))
(define (bind-wheres stx body)
(let loop ([stx stx]
[body body])
(syntax-case stx ()
[() body]
[((x e) y ...) (loop #'(y ...) #`(term-let ([x (term e)]) #,body))])))
(define (process-extras stx name-table extras)
(let ([the-name #f]
[the-name-stx #f]
[fresh-vars '()]
[side-conditions '()]
[wheres '()])
(let loop ([extras extras])
(cond
[(null? extras) (values the-name fresh-vars side-conditions wheres)]
[else
(syntax-case (car extras) (side-condition fresh where)
[name
(or (identifier? (car extras))
(string? (syntax-e (car extras))))
(begin
(let* ([raw-name (syntax-e (car extras))]
[name-sym
(if (symbol? raw-name)
raw-name
(string->symbol raw-name))])
(when (hash-table-get name-table name-sym #f)
(raise-syntax-errors 'reduction-relation
"same name on multiple rules"
stx
(list (hash-table-get name-table name-sym)
(syntax name))))
(hash-table-put! name-table name-sym (syntax name))
(when the-name
(raise-syntax-errors 'reduction-relation "expected only a single name"
stx
(list the-name-stx (car extras))))
(set! the-name (if (symbol? raw-name)
(symbol->string raw-name)
raw-name))
(set! the-name-stx (car extras))
(loop (cdr extras))))]
[(fresh var ...)
(begin
(set! fresh-vars
(append
(map (λ (x)
(syntax-case x ()
[x
(identifier? #'x)
#'x]
[(x name)
(identifier? #'x)
#'(x name)]
[((ys dots2) (xs dots1))
(and (eq? (syntax-e #'dots1) (string->symbol "..."))
(eq? (syntax-e #'dots2) (string->symbol "...")))
#'((ys) (xs dots1))]
[((ys dots2) (xs dots1) names)
(and (eq? (syntax-e #'dots1) (string->symbol "..."))
(eq? (syntax-e #'dots2) (string->symbol "...")))
#'((ys) (xs dots1) names)]
[x
(raise-syntax-error 'reduction-relation
"malformed fresh variable clause"
stx
#'x)]))
(syntax->list #'(var ...)))
fresh-vars))
(loop (cdr extras)))]
[(side-condition exp ...)
(begin
(set! side-conditions
(append (syntax->list (syntax (exp ...))) side-conditions))
(loop (cdr extras)))]
[(where x e)
(begin
(set! wheres (cons #'(x e) wheres))
(loop (cdr extras)))]
[(where . x)
(raise-syntax-error 'reduction-relation "malformed where clause" stx (car extras))]
[_
(raise-syntax-error 'reduction-relation "unknown extra" stx (car extras))])]))))
(define (table-cons! ht key hd)
(module-identifier-mapping-put! ht key (cons hd (module-identifier-mapping-get ht key (λ () '())))))
(define (raise-syntax-errors sym str stx stxs)
(raise (make-exn:fail:syntax
(string->immutable-string (format "~a: ~a~a"
sym
str
(if (error-print-source-location)
(string-append ":" (stxs->list stxs))
"")))
(current-continuation-marks)
(apply list-immutable stxs))))
(define (stxs->list stxs)
(apply
string-append
(let loop ([stxs stxs])
(cond
[(null? stxs) '()]
[else
(cons (format " ~s" (syntax-object->datum (car stxs)))
(loop (cdr stxs)))])))))
(define (verify-name-ok the-name)
(unless (symbol? the-name)
(error 'reduction-relation "expected a single name, got ~s" the-name)))
(define (verify-names-ok the-names len-counter)
(unless (and (list? the-names)
(andmap symbol? the-names))
(error 'reduction-relation
"expected a sequence of names, got ~s"
the-names))
(unless (= (length len-counter)
(length the-names))
(error 'reduction-relation
"expected the length of the sequence of names to be ~a, got ~s"
(length len-counter)
the-names)))
(define (union-reduction-relations fst snd . rst)
(let ([name-ht (make-hash-table)]
[lst (list* fst snd rst)]
[first-lang (reduction-relation-lang fst)])
(for-each
(λ (red)
(unless (eq? first-lang (reduction-relation-lang red))
(error 'union-reduction-relations
"expected all of the reduction relations to use the same language"))
(for-each (λ (name)
(when (hash-table-get name-ht name #f)
(error 'union-reduction-relations "multiple rules with the name ~s" name))
(hash-table-put! name-ht name #t))
(reduction-relation-rule-names red)))
lst)
(make-reduction-relation
first-lang
(reverse (apply append (map reduction-relation-procs lst)))
(hash-table-map name-ht (λ (k v) k))
(apply append (map reduction-relation-lws lst)))))
(define (do-node-match lang lhs-frm-id lhs-to-id pat rhs-proc child-procs)
(let ([cp (compile-pattern lang pat)])
(λ (main-exp exp f other-matches)
(let ([mtchs (match-pattern cp exp)])
(if mtchs
(let o-loop ([mtchs mtchs]
[acc other-matches])
(cond
[(null? mtchs) acc]
[else
(let ([sub-exp (lookup-binding (mtch-bindings (car mtchs)) lhs-frm-id)])
(let i-loop ([child-procs child-procs]
[acc acc])
(cond
[(null? child-procs) (o-loop (cdr mtchs) acc)]
[else (i-loop (cdr child-procs)
((car child-procs) main-exp
sub-exp
(λ (x) (f (rhs-proc (mtch-bindings (car mtchs)) x)))
acc))])))]))
other-matches)))))
(define (do-leaf-match lang name pat proc)
(let ([cp (compile-pattern lang pat)])
(λ (main-exp exp f other-matches)
(let ([mtchs (match-pattern cp exp)])
(if mtchs
(map/mt (λ (mtch) (list name (f (proc main-exp (mtch-bindings mtch)))))
mtchs
other-matches)
other-matches)))))
(define-syntax (test-match stx)
(syntax-case stx ()
[(_ lang-exp pattern)
(with-syntax ([side-condition-rewritten (rewrite-side-conditions/check-errs 'test-match (syntax pattern))])
(syntax
(do-test-match lang-exp `side-condition-rewritten)))]
[(_ lang-exp pattern expression)
(syntax
((test-match lang-exp pattern) expression))]))
(define-values (struct:metafunc-proc make-metafunc-proc metafunc-proc? metafunc-proc-ref metafunc-proc-set!)
(make-struct-type 'metafunc-proc #f 7 0 #f null (current-inspector) 0))
(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-multi-arg? (make-struct-field-accessor metafunc-proc-ref 3))
(define metafunc-proc-name (make-struct-field-accessor metafunc-proc-ref 4))
(define metafunc-proc-cps (make-struct-field-accessor metafunc-proc-ref 5))
(define metafunc-proc-rhss (make-struct-field-accessor metafunc-proc-ref 6))
(define-struct metafunction (proc))
(define-syntax (define-metafunction stx)
(syntax-case stx ()
[(_ name lang-exp [lhs roc ...] ...)
(syntax/loc stx
(internal-define-metafunction
#f #f name lang-exp
[(lhs) roc ...] ...))]))
(define-syntax (define-metafunction/extension stx)
(syntax-case stx ()
[(_ name lang-exp prev [lhs roc ...] ...)
(identifier? #'name)
(syntax/loc stx
(internal-define-metafunction
prev #f name lang-exp
[(lhs) 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 a name" 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 (internal-define-metafunction stx)
(syntax-case stx (side-condition)
[(_ prev-metafunction multi-args? name lang-exp (lhs rhs (side-condition tl-side-conds) ...) ...)
(identifier? #'name)
(with-syntax ([(side-conditions-rewritten ...)
(map (λ (x) (rewrite-side-conditions/check-errs 'define-metafunction x))
(syntax->list (syntax ((side-condition lhs (and tl-side-conds ...)) ...))))]
[(rhs-fns ...)
(map (λ (lhs rhs)
(let-values ([(names names/ellipses) (extract-names 'define-metafunction lhs)])
(with-syntax ([(names ...) names]
[(names/ellipses ...) names/ellipses]
[rhs rhs])
(syntax
(λ (name bindings)
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
(term-let-fn ((name name))
(term rhs))))))))
(syntax->list (syntax (lhs ...)))
(syntax->list (syntax (rhs ...))))]
[(name2) (generate-temporaries (syntax (name)))]
[((side-cond ...) ...)
(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) ...) ...)
(map extract-pattern-binds (syntax->list #'(lhs ...)))]
[(lhs-app ...) (if (syntax-e #'multi-args?)
(syntax->list (syntax (lhs ...)))
(map (λ (x) (car (syntax-e x)))
(syntax->list (syntax (lhs ...)))))])
#`(begin
(define name2
(let ([lang lang-exp])
(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 cps rhss)
(make-metafunc-proc
(let ([name (lambda (x) (f x))]) name)
(list (list (to-loc-wrapper lhs-app)
(list (to-loc-wrapper/uq side-cond) ...)
(list (cons (to-loc-wrapper bind-id)
(to-loc-wrapper bind-pat))
...)
(to-loc-wrapper rhs))
...)
lang
multi-args?
'name
cps
rhss))
'name)))
(term-define-fn name name2 multi-args?)))]
[(_ prev-metafunction multi-args? name lang-exp clauses ...)
(begin
(unless (identifier? #'name)
(raise-syntax-error 'define-metafunction "expected a name" stx #'name))
(for-each
(λ (clause)
(syntax-case clause ()
[(a b) (void)]
[else
(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 (build-metafunction lang patterns rhss old-cps old-rhss wrap name)
(let ([compiled-patterns (append old-cps
(map (λ (pat) (compile-pattern lang pat)) patterns))])
(wrap
(letrec ([metafunc
(λ (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" 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
(rhs metafunc (mtch-bindings (car mtchs)))])))])))])
metafunc)
compiled-patterns
rhss)))
(define-syntax (metafunction-form stx)
(syntax-case stx ()
[(_ id)
(identifier? #'id)
(let ([v (syntax-local-value #'id (lambda () #f))])
(if (term-fn? v)
#`(make-metafunction #,(term-fn-get-id v))
(raise-syntax-error
#f
"not bound as a metafunction"
stx
#'id)))]))
(define-syntax (language stx)
(syntax-case stx ()
[(_ (name rhs ...) ...)
(andmap identifier? (syntax->list (syntax/loc stx (name ...))))
(begin
(for-each
(λ (name)
(let ([x (syntax-object->datum name)])
(when (memq x '(any number string variable variable-except variable-prefix hole name in-hole in-named-hole hide-hole side-condition cross ...))
(raise-syntax-error 'language
(format "cannot use pattern language keyword ~a as non-terminal"
x)
stx
name))
(when (regexp-match #rx"_" (symbol->string x))
(raise-syntax-error 'language
"non-terminals cannot have _ in their names"
stx
name))))
(syntax->list (syntax (name ...))))
(with-syntax ([((r-rhs ...) ...) (map (lambda (rhss) (map (λ (x) (rewrite-side-conditions/check-errs 'language x)) (syntax->list rhss)))
(syntax->list (syntax ((rhs ...) ...))))]
[(refs ...)
(let loop ([stx (syntax ((rhs ...) ...))])
(cond
[(identifier? stx)
(if (ormap (λ (x) (module-identifier=? x stx))
(syntax->list (syntax (name ...))))
(list stx)
'())]
[(syntax? stx)
(loop (syntax-e stx))]
[(pair? stx)
(append (loop (car stx))
(loop (cdr stx)))]
[else '()]))])
(with-syntax ([(the-stx ...) (cdr (syntax-e stx))])
(syntax/loc stx
(begin
(begin
(let ([name 1] ...)
(begin (void) refs ...))
(compile-language (list (list 'name (to-loc-wrapper rhs) ...) ...)
(list (make-nt 'name (list (make-rhs `r-rhs) ...)) ...))))))))]
[(_ (name rhs ...) ...)
(for-each
(lambda (name)
(unless (identifier? name)
(raise-syntax-error 'language "expected name" stx name)))
(syntax->list (syntax (name ...))))]
[(_ x ...)
(for-each
(lambda (x)
(syntax-case x ()
[(name rhs ...)
(void)]
[_
(raise-syntax-error 'language "malformed non-terminal" stx x)]))
(syntax->list (syntax (x ...))))]))
(define-syntax (extend-language stx)
(syntax-case stx ()
[(_ lang (name rhs ...) ...)
(andmap identifier? (syntax->list (syntax/loc stx (name ...))))
(with-syntax ([((r-rhs ...) ...) (map (lambda (rhss) (map (λ (x) (rewrite-side-conditions/check-errs 'extend-language x)) (syntax->list rhss)))
(syntax->list (syntax ((rhs ...) ...))))])
(syntax/loc stx
(do-extend-language lang
(list (make-nt 'name (list (make-rhs `r-rhs) ...)) ...)
(list (list 'name (to-loc-wrapper rhs) ...) ...))))]
[(_ lang (name rhs ...) ...)
(for-each
(lambda (name)
(unless (identifier? name)
(raise-syntax-error 'extend-language "expected name" stx name)))
(syntax->list (syntax (name ...))))]
[(_ lang x ...)
(for-each
(lambda (x)
(syntax-case x ()
[(name rhs ...)
(void)]
[_
(raise-syntax-error 'extend-language "malformed non-terminal" stx x)]))
(syntax->list (syntax (x ...))))]))
(define extend-nt-ellipses '(....))
(define (do-extend-language old-lang new-nts new-pict-infos)
(unless (compiled-lang? old-lang)
(error 'extend-language "expected a language as first argument, got ~e" old-lang))
(let ([old-nts (compiled-lang-lang old-lang)]
[old-ht (make-hash-table)]
[new-ht (make-hash-table)])
(for-each (λ (nt)
(hash-table-put! old-ht (nt-name nt) nt)
(hash-table-put! new-ht (nt-name nt) nt))
old-nts)
(for-each (λ (nt)
(cond
[(ormap (λ (rhs) (member (rhs-pattern rhs) extend-nt-ellipses))
(nt-rhs nt))
(unless (hash-table-get old-ht (nt-name nt) #f)
(error 'extend-language "the language extends the ~s non-terminal, but that non-terminal is not in the old language"
(nt-name nt)))
(hash-table-put! new-ht
(nt-name nt)
(make-nt
(nt-name nt)
(append (nt-rhs (hash-table-get old-ht (nt-name nt)))
(filter (λ (rhs) (not (member (rhs-pattern rhs) extend-nt-ellipses)))
(nt-rhs nt)))))]
[else
(hash-table-put! new-ht (nt-name nt) nt)]))
new-nts)
(compile-language (vector (compiled-lang-pict-builder old-lang)
new-pict-infos)
(hash-table-map new-ht (λ (x y) y)))))
(define (apply-reduction-relation* reductions exp)
(let ([answers (make-hash-table 'equal)])
(let loop ([exp exp])
(let ([nexts (apply-reduction-relation reductions exp)])
(let ([uniq (mk-uniq nexts)])
(unless (= (length uniq) (length nexts))
(error 'apply-reduction-relation*
"term ~s produced non unique results:~a"
exp
(apply
string-append
(map (λ (x) (format "\n~s" x)) nexts))))
(cond
[(null? uniq) (hash-table-put! answers exp #t)]
[else (for-each loop uniq)]))))
(hash-table-map answers (λ (x y) x))))
(define (mk-uniq terms)
(let ([ht (make-hash-table 'equal)])
(for-each (λ (x) (hash-table-put! ht x #t)) terms)
(hash-table-map ht (λ (k v) k))))
(define (map/mt f l mt-l)
(let loop ([l l])
(cond
[(null? l) mt-l]
[else (cons (f (car l)) (loop (cdr l)))])))
(define re:gen-d #rx".*[^0-9]([0-9]+)$")
(define (variable-not-in sexp var)
(let* ([var-str (symbol->string var)]
[var-prefix (let ([m (regexp-match #rx"^(.*[^0-9])[0-9]+$" var-str)])
(if m
(cadr m)
var-str))]
[found-exact-var? #f]
[nums (let loop ([sexp sexp]
[nums null])
(cond
[(pair? sexp) (loop (cdr sexp) (loop (car sexp) nums))]
[(symbol? sexp)
(when (eq? sexp var)
(set! found-exact-var? #t))
(let* ([str (symbol->string sexp)]
[match (regexp-match re:gen-d str)])
(if (and match
(is-prefix? var-prefix str))
(cons (string->number (cadr match)) nums)
nums))]
[else nums]))])
(cond
[(not found-exact-var?) var]
[(null? nums) (string->symbol (format "~a1" var))]
[else (string->symbol (format "~a~a" var-prefix (+ 1 (apply max nums))))])))
(define (variables-not-in sexp vars)
(let loop ([vars vars]
[sexp sexp])
(cond
[(null? vars) null]
[else
(let ([new-var (variable-not-in sexp (car vars))])
(cons new-var
(loop (cdr vars)
(cons new-var sexp))))])))
(define (is-prefix? str1 str2)
(and (<= (string-length str1) (string-length str2))
(equal? str1 (substring str2 0 (string-length str1)))))
(define (reduction-relation->rule-names x)
(reverse (reduction-relation-rule-names x)))
(provide (rename -reduction-relation reduction-relation)
--> fresh where
compatible-closure
context-closure
language
extend-language
define-metafunction
define-metafunction/extension
define-multi-args-metafunction
define-multi-args-metafunction/extension
(rename metafunction-form metafunction)
metafunction? metafunction-proc
metafunc-proc-lang
metafunc-proc-pict-info
metafunc-proc-name
metafunc-proc-multi-arg?
metafunc-proc-cps
metafunc-proc-rhss
reduction-relation->rule-names)
(provide test-match
term-match
term-match/single
make-bindings bindings-table bindings?
mtch? mtch-bindings mtch-context mtch-hole
make-rib rib? rib-name rib-exp
reduction-relation?)
(provide language-nts
apply-reduction-relation
apply-reduction-relation/tag-with-names
apply-reduction-relation*
union-reduction-relations
variable-not-in
variables-not-in))
![[logo]](/logo.png){kind=logo}