delay the construction of the compatible-closure grammar (the 'cross' thing)

until it is actually used. (This can make a big difference for large grammars
in models that don't actually use the compatible closure stuff.)
This commit is contained in:
Robby Findler 2011-10-30 22:35:23 -05:00
parent 1dade8ee1d
commit 41f68af64a
2 changed files with 73 additions and 43 deletions

View File

@ -2,18 +2,19 @@
#| #|
Note: the patterns described in the doc.txt file are Note: the patterns described in the documentation are
slightly different than the patterns processed here. slightly different than the patterns processed here.
The difference is in the form of the side-condition The difference is in the form of the side-condition
expressions. Here they are procedures that accept expressions. Here they are procedures that accept
binding structures, instead of expressions. The binding structures, instead of expressions. The
reduction (And other) macros do this transformation rewrite-side-conditions/check-errs macro does this
before the pattern compiler is invoked. transformation before the pattern compiler is invoked.
|# |#
(require scheme/list (require scheme/list
scheme/match scheme/match
scheme/contract scheme/contract
racket/promise
"underscore-allowed.rkt") "underscore-allowed.rkt")
(define-struct compiled-pattern (cp)) (define-struct compiled-pattern (cp))
@ -85,9 +86,16 @@ before the pattern compiler is invoked.
;; (listof symbol) ;; (listof symbol)
;; (listof (listof symbol))) -- keeps track of `primary' non-terminals ;; (listof (listof symbol))) -- keeps track of `primary' non-terminals
(define-struct compiled-lang (lang cclang ht list-ht across-ht across-list-ht (define-struct compiled-lang (lang delayed-cclang ht list-ht raw-across-ht raw-across-list-ht
has-hole-ht cache bind-names-cache pict-builder has-hole-ht cache bind-names-cache pict-builder
literals nt-map)) literals nt-map))
(define (compiled-lang-cclang x) (force (compiled-lang-delayed-cclang x)))
(define (compiled-lang-across-ht x)
(compiled-lang-cclang x) ;; ensure this is computed
(compiled-lang-raw-across-ht x))
(define (compiled-lang-across-list-ht x)
(compiled-lang-cclang x) ;; ensure this is computed
(compiled-lang-raw-across-list-ht x))
;; lookup-binding : bindings (union sym (cons sym sym)) [(-> any)] -> any ;; lookup-binding : bindings (union sym (cons sym sym)) [(-> any)] -> any
(define (lookup-binding bindings (define (lookup-binding bindings
@ -160,15 +168,18 @@ before the pattern compiler is invoked.
(when (has-underscore? nt) (when (has-underscore? nt)
(error 'compile-language "cannot use underscore in nonterminal name, ~s" nt)))) (error 'compile-language "cannot use underscore in nonterminal name, ~s" nt))))
(let ([compatible-context-language (define compatible-context-language
(build-compatible-context-language clang-ht lang)]) (delay
(for-each (lambda (nt) (let ([compatible-context-language
(hash-set! across-ht (nt-name nt) null) (build-compatible-context-language clang-ht lang)])
(hash-set! across-list-ht (nt-name nt) null)) (for-each (lambda (nt)
compatible-context-language) (hash-set! across-ht (nt-name nt) null)
(do-compilation clang-ht clang-list-ht lang #t) (hash-set! across-list-ht (nt-name nt) null))
(do-compilation across-ht across-list-ht compatible-context-language #f) compatible-context-language)
(struct-copy compiled-lang clang [cclang compatible-context-language])))) (do-compilation across-ht across-list-ht compatible-context-language #f)
compatible-context-language)))
(do-compilation clang-ht clang-list-ht lang #t)
(struct-copy compiled-lang clang [delayed-cclang compatible-context-language])))
;; extract-literals : (listof nt) -> (listof symbol) ;; extract-literals : (listof nt) -> (listof symbol)
(define (extract-literals nts) (define (extract-literals nts)
@ -633,8 +644,6 @@ before the pattern compiler is invoked.
(define clang-ht (compiled-lang-ht clang)) (define clang-ht (compiled-lang-ht clang))
(define clang-list-ht (compiled-lang-list-ht clang)) (define clang-list-ht (compiled-lang-list-ht clang))
(define has-hole-ht (compiled-lang-has-hole-ht clang)) (define has-hole-ht (compiled-lang-has-hole-ht clang))
(define across-ht (compiled-lang-across-ht clang))
(define across-list-ht (compiled-lang-across-list-ht clang))
(define (compile-pattern/default-cache pattern) (define (compile-pattern/default-cache pattern)
(compile-pattern/cache pattern (compile-pattern/cache pattern
@ -709,19 +718,21 @@ before the pattern compiler is invoked.
match-raw-name) match-raw-name)
has-hole?))])] has-hole?))])]
[`(cross ,(? symbol? pre-id)) [`(cross ,(? symbol? pre-id))
(let ([id (if prefix-cross? (define across-ht (compiled-lang-across-ht clang))
(symbol-append pre-id '- pre-id) (define across-list-ht (compiled-lang-across-list-ht clang))
pre-id)]) (define id (if prefix-cross?
(cond (symbol-append pre-id '- pre-id)
[(hash-maps? across-ht id) pre-id))
(values (cond
(lambda (exp hole-info) [(hash-maps? across-ht id)
(match-nt (hash-ref across-list-ht id) (values
(hash-ref across-ht id) (lambda (exp hole-info)
id exp hole-info)) (match-nt (hash-ref across-list-ht id)
#t)] (hash-ref across-ht id)
[else id exp hole-info))
(error 'compile-pattern "unknown cross reference ~a" id)]))] #t)]
[else
(error 'compile-pattern "unknown cross reference ~a" id)])]
[`(name ,name ,pat) [`(name ,name ,pat)
(let-values ([(match-pat has-hole?) (compile-pattern/default-cache pat)]) (let-values ([(match-pat has-hole?) (compile-pattern/default-cache pat)])
@ -1613,6 +1624,7 @@ before the pattern compiler is invoked.
(provide (struct-out nt) (provide (struct-out nt)
(struct-out rhs) (struct-out rhs)
(struct-out compiled-lang) (struct-out compiled-lang)
compiled-lang-cclang
lookup-binding lookup-binding

View File

@ -1,4 +1,4 @@
#lang scheme #lang scheme/base
(require "matcher.rkt" (require "matcher.rkt"
"reduction-semantics.rkt" "reduction-semantics.rkt"
@ -6,10 +6,18 @@
"term.rkt" "term.rkt"
"error.rkt" "error.rkt"
"struct.rkt" "struct.rkt"
(for-syntax "rewrite-side-conditions.rkt") (for-syntax scheme/base
(for-syntax "term-fn.rkt") "rewrite-side-conditions.rkt"
(for-syntax "reduction-semantics.rkt") "term-fn.rkt"
(for-syntax "keyword-macros.rkt") "reduction-semantics.rkt"
"keyword-macros.rkt")
scheme/dict
scheme/contract
scheme/promise
scheme/unit
scheme/match
scheme/pretty
scheme/function
mrlib/tex-table) mrlib/tex-table)
(define redex-pseudo-random-generator (define redex-pseudo-random-generator
@ -149,7 +157,8 @@
[min-size (apply min/f sizes)]) [min-size (apply min/f sizes)])
(map cadr (filter (λ (x) (equal? min-size (car x))) (map list sizes prods))))) (map cadr (filter (λ (x) (equal? min-size (car x))) (map list sizes prods)))))
(define-struct rg-lang (non-cross cross base-cases)) (define-struct rg-lang (non-cross delayed-cross base-cases))
(define (rg-lang-cross x) (force (rg-lang-delayed-cross x)))
(define (prepare-lang lang) (define (prepare-lang lang)
(let ([parsed (parse-language lang)]) (let ([parsed (parse-language lang)])
(values parsed (map symbol->string (compiled-lang-literals lang)) (find-base-cases parsed)))) (values parsed (map symbol->string (compiled-lang-literals lang)) (find-base-cases parsed))))
@ -405,7 +414,7 @@
(λ (lang bases any?) (λ (lang bases any?)
(make-rg-lang (make-rg-lang
(compile-non-terminals (compiled-lang-lang lang) any?) (compile-non-terminals (compiled-lang-lang lang) any?)
(compile-non-terminals (compiled-lang-cclang lang) any?) (delay (compile-non-terminals (compiled-lang-cclang lang) any?))
bases))] bases))]
[(langc sexpc compile-pattern) [(langc sexpc compile-pattern)
(values (values
@ -422,7 +431,8 @@
[else t])) [else t]))
(bindings e))))))))) (bindings e)))))))))
(define-struct base-cases (cross non-cross)) (define-struct base-cases (delayed-cross non-cross))
(define (base-cases-cross x) (force (base-cases-delayed-cross x)))
;; find-base-cases : (list/c nt) -> base-cases ;; find-base-cases : (list/c nt) -> base-cases
(define (find-base-cases lang) (define (find-base-cases lang)
@ -469,7 +479,7 @@
(loop a) (loop a)
(loop b)] (loop b)]
[_ (void)])) [_ (void)]))
nts)) nts))
;; build-table : (listof nt) -> hash ;; build-table : (listof nt) -> hash
(define (build-table nts) (define (build-table nts)
@ -479,15 +489,23 @@
nts) nts)
tbl)) tbl))
;; we can delay the work of computing the base cases for
;; the cross part of the language since none of the productions
;; refer to it (as that's not allowed in general and would be
;; quite confusing if it were...)
(let loop () (let loop ()
(set! changed? #f) (set! changed? #f)
(for-each (process-nt #f) (compiled-lang-lang lang)) (for-each (process-nt #f) (compiled-lang-lang lang))
(for-each (process-nt #t) (compiled-lang-cclang lang))
(when changed? (when changed?
(loop))) (loop)))
(make-base-cases (make-base-cases
(build-table (compiled-lang-cclang lang)) (delay (begin
(let loop ()
(set! changed? #f)
(for-each (process-nt #t) (compiled-lang-cclang lang))
(when changed?
(loop)))
(build-table (compiled-lang-cclang lang))))
(build-table (compiled-lang-lang lang)))) (build-table (compiled-lang-lang lang))))
(define min/f (define min/f
@ -623,10 +641,10 @@
(define ((parse-rhs mode) rhs) (define ((parse-rhs mode) rhs)
(make-rhs (reassign-classes (parse-pattern (rhs-pattern rhs) lang mode)))) (make-rhs (reassign-classes (parse-pattern (rhs-pattern rhs) lang mode))))
(struct-copy (struct-copy
compiled-lang lang compiled-lang lang
[lang (map (parse-nt 'grammar) (compiled-lang-lang lang))] [lang (map (parse-nt 'grammar) (compiled-lang-lang lang))]
[cclang (map (parse-nt 'cross) (compiled-lang-cclang lang))])) [delayed-cclang (delay (map (parse-nt 'cross) (compiled-lang-cclang lang)))]))
;; unparse-pattern: parsed-pattern -> pattern ;; unparse-pattern: parsed-pattern -> pattern
(define unparse-pattern (define unparse-pattern
@ -1051,7 +1069,7 @@
(struct-out class) (struct-out class)
(struct-out binder) (struct-out binder)
(struct-out rg-lang) (struct-out rg-lang)
(struct-out base-cases) (struct-out base-cases) base-cases-cross
(struct-out counterexample) (struct-out counterexample)
(struct-out exn:fail:redex:test)) (struct-out exn:fail:redex:test))