Macro stepper: added env/renaming tracking
svn: r5669 original commit: 0a194c3eae0582026112b294e05fe32565af0b71
This commit is contained in:
parent
41538c81f5
commit
a169d49e04
|
@ -19,7 +19,9 @@
|
||||||
|
|
||||||
find-derivs
|
find-derivs
|
||||||
find-deriv
|
find-deriv
|
||||||
find-derivs/syntax)
|
find-derivs/syntax
|
||||||
|
extract-all-fresh-names
|
||||||
|
flatten-identifiers)
|
||||||
|
|
||||||
;; IntW
|
;; IntW
|
||||||
;; Matches only interrupted wraps
|
;; Matches only interrupted wraps
|
||||||
|
@ -138,20 +140,25 @@
|
||||||
|
|
||||||
;; find-derivs : (deriv -> boolean) (deriv -> boolean) deriv -> (list-of deriv)
|
;; find-derivs : (deriv -> boolean) (deriv -> boolean) deriv -> (list-of deriv)
|
||||||
(define (find-derivs pred stop-short d)
|
(define (find-derivs pred stop-short d)
|
||||||
(find-deriv/unit+join+zero pred stop-short d list append null))
|
(let ([stop (lambda (x) (or (pred x) (stop-short x)))])
|
||||||
|
(find-deriv/unit+join+zero pred stop d list append null)))
|
||||||
|
|
||||||
;; find-deriv : (deriv -> boolean) (deriv -> boolean) deriv -> deriv/#f
|
;; find-deriv : (deriv -> boolean) (deriv -> boolean) deriv -> deriv/#f
|
||||||
;; Finds the first deriv that matches; throws the rest away
|
;; Finds the first deriv that matches; throws the rest away
|
||||||
(define (find-deriv pred stop-short d)
|
(define (find-deriv pred stop-short d)
|
||||||
(let/ec return (find-deriv/unit+join+zero pred stop-short d return (lambda _ #f) #f)))
|
(let ([stop (lambda (x) (or (pred x) (stop-short x)))])
|
||||||
|
(let/ec return (find-deriv/unit+join+zero pred stop d return (lambda _ #f) #f))))
|
||||||
|
|
||||||
;; find-deriv/unit+join+zero
|
;; find-deriv/unit+join+zero
|
||||||
;; Parameterized over monad operations for combining the results
|
;; Parameterized over monad operations for combining the results
|
||||||
;; For example, <list, append, null> collects the results into a list
|
;; For example, <list, append, null> collects the results into a list
|
||||||
(define (find-deriv/unit+join+zero pred stop-short d unit join zero)
|
(define (find-deriv/unit+join+zero pred stop-short d unit join zero)
|
||||||
(define (loop d)
|
(define (loop d)
|
||||||
|
(if (pred d)
|
||||||
|
(join (unit d) (loop-inner d))
|
||||||
|
(loop-inner d)))
|
||||||
|
(define (loop-inner d)
|
||||||
(match d
|
(match d
|
||||||
[(? pred d) (unit d)]
|
|
||||||
[(? stop-short d) zero]
|
[(? stop-short d) zero]
|
||||||
[(AnyQ mrule (_ _ tx next))
|
[(AnyQ mrule (_ _ tx next))
|
||||||
(join (loop tx) (loop next))]
|
(join (loop tx) (loop next))]
|
||||||
|
@ -246,4 +253,66 @@
|
||||||
[(AnyQ lift-deriv (_ _ _ _ _)) #t]
|
[(AnyQ lift-deriv (_ _ _ _ _)) #t]
|
||||||
[_ #f])
|
[_ #f])
|
||||||
d))
|
d))
|
||||||
)
|
|
||||||
|
;; extract-all-fresh-names : Derivation -> syntaxlike
|
||||||
|
;; FIXME: Missing case-lambda
|
||||||
|
(define (extract-all-fresh-names d)
|
||||||
|
(define (renaming-node? x)
|
||||||
|
(or (p:lambda? x)
|
||||||
|
(p:case-lambda? x)
|
||||||
|
(p:let-values? x)
|
||||||
|
(p:letrec-values? x)
|
||||||
|
(p:letrec-syntaxes+values? x)
|
||||||
|
(p:rename? x)))
|
||||||
|
(define (extract-fresh-names d)
|
||||||
|
(match d
|
||||||
|
[(struct p:lambda (e1 e2 rs renames body))
|
||||||
|
(if renames
|
||||||
|
(with-syntax ([(?formals . ?body) renames])
|
||||||
|
#'?formals)
|
||||||
|
null)]
|
||||||
|
[(struct p:let-values (e1 e2 rs renames rhss body))
|
||||||
|
(if renames
|
||||||
|
(with-syntax ([(((?vars ?rhs) ...) . ?body) renames])
|
||||||
|
#'(?vars ...))
|
||||||
|
null)]
|
||||||
|
[(struct p:letrec-values (e1 e2 rs renames rhss body))
|
||||||
|
(if renames
|
||||||
|
(with-syntax ([(((?vars ?rhs) ...) . ?body) renames])
|
||||||
|
#'(?vars ...))
|
||||||
|
null)]
|
||||||
|
[(struct p:letrec-syntaxes+values (e1 e2 rs srenames srhss vrenames vrhss body))
|
||||||
|
(cons
|
||||||
|
(if srenames
|
||||||
|
(with-syntax ([(((?svars ?srhs) ...) ((?vvars ?vrhs) ...) . ?body)
|
||||||
|
srenames])
|
||||||
|
#'(?svars ... ?vvars ...))
|
||||||
|
null)
|
||||||
|
(if vrenames
|
||||||
|
(with-syntax ([(((?vvars ?vrhs) ...) . ?body) vrenames])
|
||||||
|
#'(?vvars ...))
|
||||||
|
null))]
|
||||||
|
[_ null]))
|
||||||
|
|
||||||
|
(let ([all-renaming-forms
|
||||||
|
(find-deriv/unit+join+zero
|
||||||
|
renaming-node?
|
||||||
|
(lambda (d) #f)
|
||||||
|
d
|
||||||
|
list
|
||||||
|
append
|
||||||
|
null)])
|
||||||
|
(flatten-identifiers (map extract-fresh-names all-renaming-forms))))
|
||||||
|
|
||||||
|
;; flatten-identifiers : syntaxlike -> (list-of identifier)
|
||||||
|
(define (flatten-identifiers stx)
|
||||||
|
(syntax-case stx ()
|
||||||
|
[id (identifier? #'id) (list #'id)]
|
||||||
|
[() null]
|
||||||
|
[(x . y) (append (flatten-identifiers #'x) (flatten-identifiers #'y))]
|
||||||
|
[else (error 'flatten-identifers "neither syntax list nor identifier: ~s"
|
||||||
|
(if (syntax? stx)
|
||||||
|
(syntax-object->datum stx)
|
||||||
|
stx))]))
|
||||||
|
|
||||||
|
)
|
||||||
|
|
|
@ -27,7 +27,7 @@
|
||||||
|
|
||||||
;; current-derivation : parameter of Derivation
|
;; current-derivation : parameter of Derivation
|
||||||
(define current-derivation (make-parameter #f))
|
(define current-derivation (make-parameter #f))
|
||||||
|
|
||||||
(define-syntax with-context
|
(define-syntax with-context
|
||||||
(syntax-rules ()
|
(syntax-rules ()
|
||||||
[(with-context f . body)
|
[(with-context f . body)
|
||||||
|
@ -95,10 +95,11 @@
|
||||||
#'(let-values ([(form2-var foci1-var foci2-var description-var)
|
#'(let-values ([(form2-var foci1-var foci2-var description-var)
|
||||||
(with-syntax ([p f])
|
(with-syntax ([p f])
|
||||||
(values form2 foci1 foci2 description))])
|
(values form2 foci1 foci2 description))])
|
||||||
(cons (walk/foci foci1-var foci2-var
|
(with-context (make-renames foci1-var foci2-var)
|
||||||
f form2-var
|
(cons (walk/foci foci1-var foci2-var
|
||||||
description-var)
|
f form2-var
|
||||||
(R** form2-var p . more)))]
|
description-var)
|
||||||
|
(R** form2-var p . more))))]
|
||||||
[(R** f p [#:walk form2 description] . more)
|
[(R** f p [#:walk form2 description] . more)
|
||||||
#'(let-values ([(form2-var description-var)
|
#'(let-values ([(form2-var description-var)
|
||||||
(with-syntax ([p f])
|
(with-syntax ([p f])
|
||||||
|
|
|
@ -143,6 +143,7 @@
|
||||||
(cons (walk/foci (syntax->list #'(?formals ...))
|
(cons (walk/foci (syntax->list #'(?formals ...))
|
||||||
(syntax->list #'(?formals* ...))
|
(syntax->list #'(?formals* ...))
|
||||||
e1 mid 'rename-case-lambda)
|
e1 mid 'rename-case-lambda)
|
||||||
|
;; FIXME: Missing renames frames here
|
||||||
(R mid (CASE-LAMBDA [FORMALS . BODY] ...)
|
(R mid (CASE-LAMBDA [FORMALS . BODY] ...)
|
||||||
[Block (BODY ...) (map cdr renames+bodies)]))))]
|
[Block (BODY ...) (map cdr renames+bodies)]))))]
|
||||||
[(AnyQ p:let-values (e1 e2 rs renames rhss body) exni)
|
[(AnyQ p:let-values (e1 e2 rs renames rhss body) exni)
|
||||||
|
|
|
@ -1,13 +1,18 @@
|
||||||
|
|
||||||
(module steps mzscheme
|
(module steps mzscheme
|
||||||
(require "deriv.ss")
|
(require "deriv.ss"
|
||||||
|
"deriv-util.ss")
|
||||||
|
|
||||||
;; A ReductionSequence is a (list-of Reduction)
|
;; A ReductionSequence is a (list-of Reduction)
|
||||||
|
|
||||||
;; A ProtoStep is (make-protostep Derivation BigContext StepType Context)
|
;; A ProtoStep is (make-protostep Derivation BigContext StepType Context)
|
||||||
|
|
||||||
;; A Context is a list of Frames
|
;; A Context is a list of Frames
|
||||||
;; A Frame is (syntax -> syntax)
|
;; A Frame is either:
|
||||||
|
;; - (syntax -> syntax)
|
||||||
|
;; - (make-renames syntax syntax)
|
||||||
|
;; - 'phase-up
|
||||||
|
(define-struct renames (old new))
|
||||||
|
|
||||||
;; A BigContext is (list-of BigFrame)
|
;; A BigContext is (list-of BigFrame)
|
||||||
;; A BigFrame is (make-bigframe Derivation Context Syntaxes Syntax)
|
;; A BigFrame is (make-bigframe Derivation Context Syntaxes Syntax)
|
||||||
|
@ -16,9 +21,9 @@
|
||||||
;; A Reduction is one of
|
;; A Reduction is one of
|
||||||
;; - (make-step ... Syntaxes Syntaxes Syntax Syntax)
|
;; - (make-step ... Syntaxes Syntaxes Syntax Syntax)
|
||||||
;; - (make-misstep ... Syntax Syntax Exception)
|
;; - (make-misstep ... Syntax Syntax Exception)
|
||||||
|
|
||||||
(define-struct protostep (deriv lctx type ctx) #f)
|
(define-struct protostep (deriv lctx type ctx) #f)
|
||||||
|
|
||||||
(define-struct (step protostep) (foci1 foci2 e1 e2) #f)
|
(define-struct (step protostep) (foci1 foci2 e1 e2) #f)
|
||||||
(define-struct (misstep protostep) (foci1 e1 exn) #f)
|
(define-struct (misstep protostep) (foci1 e1 exn) #f)
|
||||||
|
|
||||||
|
@ -27,7 +32,22 @@
|
||||||
(let loop ([ctx ctx] [stx stx])
|
(let loop ([ctx ctx] [stx stx])
|
||||||
(if (null? ctx)
|
(if (null? ctx)
|
||||||
stx
|
stx
|
||||||
(loop (cdr ctx) ((car ctx) stx)))))
|
(let ([frame0 (car ctx)])
|
||||||
|
(if (procedure? frame0)
|
||||||
|
(loop (cdr ctx) (frame0 stx))
|
||||||
|
(loop (cdr ctx) stx))))))
|
||||||
|
|
||||||
|
;; context-env : Context -> (list-of identifier)
|
||||||
|
(define (context-env ctx)
|
||||||
|
(let loop ([ctx ctx] [env null])
|
||||||
|
(if (null? ctx)
|
||||||
|
env
|
||||||
|
(let ([frame0 (car ctx)])
|
||||||
|
(if (renames? frame0)
|
||||||
|
(loop (cdr ctx)
|
||||||
|
(append (flatten-identifiers (renames-new frame0))
|
||||||
|
env))
|
||||||
|
(loop (cdr ctx) env))))))
|
||||||
|
|
||||||
(define (step-term1 s)
|
(define (step-term1 s)
|
||||||
(context-fill (protostep-ctx s) (step-e1 s)))
|
(context-fill (protostep-ctx s) (step-e1 s)))
|
||||||
|
@ -39,7 +59,7 @@
|
||||||
|
|
||||||
(define (bigframe-term bf)
|
(define (bigframe-term bf)
|
||||||
(context-fill (bigframe-ctx bf) (bigframe-e bf)))
|
(context-fill (bigframe-ctx bf) (bigframe-e bf)))
|
||||||
|
|
||||||
;; A StepType is a simple in the following alist.
|
;; A StepType is a simple in the following alist.
|
||||||
|
|
||||||
(define step-type-meanings
|
(define step-type-meanings
|
||||||
|
|
Loading…
Reference in New Issue
Block a user