(module reduction-semantics mzscheme
(require "private/matcher.ss"
"private/term.ss"
(lib "contract.ss")
(lib "list.ss")
(lib "etc.ss"))
(require-for-syntax (lib "list.ss")
(lib "name.ss" "syntax")
"private/rewrite-side-conditions.ss"
(lib "boundmap.ss" "syntax"))
(define-struct red (contractum reduct name))
(define-syntax (compatible-closure stx)
(syntax-case stx ()
[(_ red lang nt)
(identifier? (syntax nt))
(with-syntax ([side-conditions-rewritten (rewrite-side-conditions '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 '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
(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))))
(define (build-metafunction lang patterns rhss wrap name)
(let ([compiled-patterns (map (λ (pat) (compile-pattern lang pat)) patterns)])
(wrap
(λ (exp)
(let loop ([patterns compiled-patterns]
[rhss rhss]
[num 0])
(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 "clause ~a matched ~s two different ways" num exp)]
[else
(rhs (mtch-bindings (car mtchs)))])))]))))))
(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-struct reduction-relation (procs rule-names))
(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-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 ...)))])
(reduction-relation/helper
stx
(syntax lang)
(syntax->list (syntax (rules ...)))
(syntax->list (syntax (shortcuts ...)))))]))
(define (before-where stx)
(let loop ([lst (syntax->list stx)])
(cond
[(null? lst) null]
[else
(let ([fst (car lst)])
(syntax-case* (car lst) (where) (λ (x y) (eq? (syntax-e x) (syntax-e y)))
[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) (λ (x y) (eq? (syntax-e x) (syntax-e y)))
[where (cdr lst)]
[else (loop (cdr lst))]))])))
(define (reduction-relation/helper stx lang-exp rules shortcuts)
(let ([ht (make-module-identifier-mapping)])
(for-each (λ (shortcut)
(syntax-case shortcut ()
[((lhs-arrow lhs-from lhs-to)
(rhs-arrow rhs-from rhs-to))
(table-cons! ht (syntax rhs-arrow) shortcut)]))
shortcuts)
(for-each (λ (rule)
(syntax-case rule ()
[(arrow . rst)
(table-cons! ht (syntax arrow) rule)]))
rules)
(unless (module-identifier-mapping-get ht (syntax -->) (λ () #f))
(raise-syntax-error 'reduction-relation "no --> rules" stx))
(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))])
(syntax
(make-reduction-relation
(let ([lang-x lang-exp])
(list top-level ...))
'(rule-names ...)))))))
(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 "found no rules for ~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 (syntax rhs-from))])
(with-syntax ([(names ...) names]
[(names/ellipses ...) names/ellipses]
[side-conditions-rewritten (rewrite-side-conditions
'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) (process-extras stx name-table extras)])
(let-values ([(names names/ellipses) (extract-names from)])
(with-syntax ([side-conditions-rewritten
(rewrite-side-conditions
'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-vars ...) fresh-vars])
(syntax (do-leaf-match
lang
name
`side-conditions-rewritten
(λ (main bindings)
(term-let ([names/ellipses (lookup-binding bindings 'names)]
...
[fresh-vars (variable-not-in main 'fresh-vars)]
...)
(term to)))))))))
(define (process-extras stx name-table extras)
(let ([the-name #f]
[the-name-stx #f]
[fresh-vars '()]
[side-conditions '()])
(let loop ([extras extras])
(cond
[(null? extras) (values the-name fresh-vars side-conditions)]
[else
(syntax-case (car extras) (fresh)
[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 ...)
(andmap identifier? (syntax->list (syntax (var ...))))
(begin
(set! fresh-vars (append (syntax->list (syntax (var ...))) fresh-vars))
(loop (cdr extras)))]
[(fresh exp ...)
(for-each
(λ (x) (unless (identifier? x)
(raise-syntax-error 'reduction-relation "expected variables in a fresh clause" stx x)))
(syntax->list (syntax (exp ...))))]
[(side-condition exp ...)
(begin
(set! side-conditions
(append (syntax->list (syntax (exp ...))) side-conditions))
(loop (cdr 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" sym str))
(current-continuation-marks)
(apply list-immutable stxs)))))
(define (union-reduction-relations fst snd . rst)
(let ([name-ht (make-hash-table)]
[lst (list* fst snd rst)])
(for-each
(λ (red)
(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
(reverse (apply append (map reduction-relation-procs lst)))
(hash-table-map name-ht (λ (k v) k)))))
(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 '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-syntax (define-metafunction stx)
(syntax-case stx ()
[(_ name lang-exp (lhs rhs) ...)
(with-syntax ([(side-conditions-rewritten ...) (map (λ (x) (rewrite-side-conditions 'define-metafunction x))
(syntax->list (syntax (lhs ...))))]
[(rhs-fns ...)
(map (λ (lhs rhs)
(let-values ([(names names/ellipses) (extract-names lhs)])
(with-syntax ([(names ...) names]
[(names/ellipses ...) names/ellipses]
[rhs rhs])
(syntax
(λ (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)))])
(syntax
(begin
(define name2
(build-metafunction
lang-exp
(list `side-conditions-rewritten ...)
(list rhs-fns ...)
(λ (f) (let ([name (lambda (x) (f x))]) name))
'name))
(term-define-fn name name2))))]))
(define-syntax (metafunction stx)
(syntax-case stx ()
[(_ lang-exp (lhs rhs) ...)
(with-syntax ([(side-conditions-rewritten ...) (map (λ (x) (rewrite-side-conditions 'metafunction))
(syntax->list (syntax (lhs ...))))]
[(rhs-fns ...)
(map (λ (lhs rhs)
(let-values ([(names names/ellipses) (extract-names lhs)])
(with-syntax ([(names ...) names]
[(names/ellipses ...) names/ellipses]
[rhs rhs])
(syntax
(λ (bindings) (term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
(term rhs)))))))
(syntax->list (syntax (lhs ...)))
(syntax->list (syntax (rhs ...))))]
[name (or (syntax-local-infer-name stx) 'metafunction)])
(syntax
(build-metafunction
lang-exp
(list `side-conditions-rewritten ...)
(list rhs-fns ...)
(λ (f) (let ([name (lambda (x) (f x))]) name))
'name)))]))
(define-syntax (language stx)
(syntax-case stx ()
[(_ (name rhs ...) ...)
(andmap identifier? (syntax->list (syntax/loc stx (name ...))))
(with-syntax ([((r-rhs ...) ...) (map (lambda (rhss) (map (λ (x) (rewrite-side-conditions '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 '()]))])
(syntax/loc stx
(begin
(begin
(let ([name 1] ...)
(begin (void) refs ...))
(compile-language (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 '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) ...)) ...))))]
[(_ 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)
(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 (hash-table-map new-ht (λ (x y) y)))))
(define (reduce reductions exp)
(reduce/internal reductions exp (λ (red) (λ (mtch) ((red-reduct red) (mtch-bindings mtch))))))
(define (reduce/tag-with-reduction reductions exp)
(reduce/internal reductions exp (λ (red) (λ (mtch) (list red ((red-reduct red) (mtch-bindings mtch)))))))
(define (reduce/internal reductions exp f)
(let loop ([reductions reductions]
[acc null])
(cond
[(null? reductions) acc]
[else (let* ([red (car reductions)]
[mtchs (match-pattern (red-contractum red) exp)])
(if mtchs
(loop (cdr reductions)
(map/mt (f red) mtchs acc))
(loop (cdr reductions) acc)))])))
(define (apply-reduction-relation* reductions exp)
(let ([answers (make-hash-table)])
(let loop ([exp exp])
(let ([nexts (apply-reduction-relation reductions exp)])
(let ([uniq (mk-uniq nexts)])
(unless (= (length uniq) (length nexts))
(error 'reduce-all "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)]
[nums (let loop ([sexp sexp]
[nums null])
(cond
[(pair? sexp) (loop (cdr sexp) (loop (car sexp) nums))]
[(symbol? sexp) (let* ([str (symbol->string sexp)]
[match (regexp-match re:gen-d str)])
(if (and match
(is-prefix? var-str str))
(cons (string->number (cadr match)) nums)
nums))]
[else nums]))])
(if (null? nums)
(string->symbol (format "~a1" var))
(string->symbol (format "~a~a" var (+ 1 (apply max nums)))))))
(define (is-prefix? str1 str2)
(and (<= (string-length str1) (string-length str2))
(equal? str1 (substring str2 0 (string-length str1)))))
(provide (rename -reduction-relation reduction-relation)
--> fresh
compatible-closure
context-closure
language
extend-language
plug
compiled-lang?
term
term-let
none?
define-metafunction)
(provide test-match
make-bindings bindings-table bindings?
mtch? mtch-bindings mtch-context mtch-hole
make-rib rib? rib-name rib-exp
reduction-relation?)
(provide/contract
[set-cache-size! (-> number? void?)]
[apply-reduction-relation (-> reduction-relation? any/c (listof any/c))]
[apply-reduction-relation/tag-with-names
(-> reduction-relation? any/c (listof (list/c (union false/c string?) any/c)))]
[apply-reduction-relation* (-> reduction-relation? any/c (listof any/c))]
[union-reduction-relations (->* (reduction-relation? reduction-relation?)
(listof reduction-relation?)
(reduction-relation?))]
[lookup-binding (case->
(-> bindings? symbol? any)
(-> bindings? symbol? (-> any) any))]
(variable-not-in (any/c symbol? . -> . symbol?))))