Macro stepper: started tracking definite uses, added definite arrows
svn: r5700 original commit: 75a0a02355816860e9e1ed4e8cf064d5d3c9299d
This commit is contained in:
parent
a7a568ad42
commit
bdbee3601c
|
@ -8,6 +8,8 @@
|
||||||
(provide context
|
(provide context
|
||||||
big-context
|
big-context
|
||||||
current-derivation
|
current-derivation
|
||||||
|
current-definites
|
||||||
|
learn-definites
|
||||||
with-context
|
with-context
|
||||||
with-derivation
|
with-derivation
|
||||||
with-new-local-context
|
with-new-local-context
|
||||||
|
@ -28,6 +30,9 @@
|
||||||
;; current-derivation : parameter of Derivation
|
;; current-derivation : parameter of Derivation
|
||||||
(define current-derivation (make-parameter #f))
|
(define current-derivation (make-parameter #f))
|
||||||
|
|
||||||
|
;; current-definites : parameter of (list-of identifier)
|
||||||
|
(define current-definites (make-parameter null))
|
||||||
|
|
||||||
(define-syntax with-context
|
(define-syntax with-context
|
||||||
(syntax-rules ()
|
(syntax-rules ()
|
||||||
[(with-context f . body)
|
[(with-context f . body)
|
||||||
|
@ -49,6 +54,9 @@
|
||||||
[context null])
|
[context null])
|
||||||
. body)]))
|
. body)]))
|
||||||
|
|
||||||
|
(define (learn-definites ids)
|
||||||
|
(current-definites (append ids (current-definites))))
|
||||||
|
|
||||||
;; -----------------------------------
|
;; -----------------------------------
|
||||||
|
|
||||||
;; CC
|
;; CC
|
||||||
|
@ -62,7 +70,7 @@
|
||||||
;; the threaded reductions engine
|
;; the threaded reductions engine
|
||||||
(define-syntax R
|
(define-syntax R
|
||||||
(syntax-rules ()
|
(syntax-rules ()
|
||||||
[(R form pattern . clauses)
|
[(R form . clauses)
|
||||||
(R** #f _ [#:set-syntax form] [#:pattern pattern] . clauses)]))
|
(R** #f _ [#:set-syntax form] [#:pattern pattern] . clauses)]))
|
||||||
|
|
||||||
(define-syntax (R** stx)
|
(define-syntax (R** stx)
|
||||||
|
@ -106,6 +114,9 @@
|
||||||
(values form2 description))])
|
(values form2 description))])
|
||||||
(cons (walk f form2-var description-var)
|
(cons (walk f form2-var description-var)
|
||||||
(R** form2-var p . more)))]
|
(R** form2-var p . more)))]
|
||||||
|
[(R** f p [#:learn ids] . more)
|
||||||
|
#'(begin (learn-definites ids)
|
||||||
|
(R** f p . more))]
|
||||||
|
|
||||||
;; Conditional
|
;; Conditional
|
||||||
[(R** f p [#:if test consequent ...] . more)
|
[(R** f p [#:if test consequent ...] . more)
|
||||||
|
@ -178,22 +189,22 @@
|
||||||
;; walk : syntax(es) syntax(es) StepType -> Reduction
|
;; walk : syntax(es) syntax(es) StepType -> Reduction
|
||||||
;; Lifts a local step into a term step.
|
;; Lifts a local step into a term step.
|
||||||
(define (walk e1 e2 type)
|
(define (walk e1 e2 type)
|
||||||
(make-step (current-derivation) (big-context) type (context)
|
(make-step (current-derivation) (big-context) type (context) (current-definites)
|
||||||
(foci e1) (foci e2) e1 e2))
|
(foci e1) (foci e2) e1 e2))
|
||||||
|
|
||||||
;; walk/foci : syntaxes syntaxes syntax syntax StepType -> Reduction
|
;; walk/foci : syntaxes syntaxes syntax syntax StepType -> Reduction
|
||||||
(define (walk/foci foci1 foci2 Ee1 Ee2 type)
|
(define (walk/foci foci1 foci2 Ee1 Ee2 type)
|
||||||
(make-step (current-derivation) (big-context) type (context)
|
(make-step (current-derivation) (big-context) type (context) (current-definites)
|
||||||
(foci foci1) (foci foci2) Ee1 Ee2))
|
(foci foci1) (foci foci2) Ee1 Ee2))
|
||||||
|
|
||||||
;; stumble : syntax exception -> Reduction
|
;; stumble : syntax exception -> Reduction
|
||||||
(define (stumble stx exn)
|
(define (stumble stx exn)
|
||||||
(make-misstep (current-derivation) (big-context) 'error (context)
|
(make-misstep (current-derivation) (big-context) 'error (context) (current-definites)
|
||||||
(foci stx) stx exn))
|
(foci stx) stx exn))
|
||||||
|
|
||||||
;; stumble/E : syntax(s) syntax exn -> Reduction
|
;; stumble/E : syntax(s) syntax exn -> Reduction
|
||||||
(define (stumble/E focus Ee1 exn)
|
(define (stumble/E focus Ee1 exn)
|
||||||
(make-misstep (current-derivation) (big-context) 'error (context)
|
(make-misstep (current-derivation) (big-context) 'error (context) (current-definites)
|
||||||
(foci focus) Ee1 exn))
|
(foci focus) Ee1 exn))
|
||||||
|
|
||||||
;; ------------------------------------
|
;; ------------------------------------
|
||||||
|
|
|
@ -13,7 +13,7 @@
|
||||||
|
|
||||||
(define-syntax Expr
|
(define-syntax Expr
|
||||||
(syntax-id-rules ()
|
(syntax-id-rules ()
|
||||||
[Expr (values reductions deriv-e1 deriv-e2)]))
|
[Expr (values reductions* deriv-e1 deriv-e2)]))
|
||||||
(define-syntax List
|
(define-syntax List
|
||||||
(syntax-id-rules ()
|
(syntax-id-rules ()
|
||||||
[List (values list-reductions lderiv-es1 lderiv-es2)]))
|
[List (values list-reductions lderiv-es1 lderiv-es2)]))
|
||||||
|
@ -34,6 +34,14 @@
|
||||||
|
|
||||||
;; reductions : Derivation -> ReductionSequence
|
;; reductions : Derivation -> ReductionSequence
|
||||||
(define (reductions d)
|
(define (reductions d)
|
||||||
|
(parameterize ((current-definites null))
|
||||||
|
(reductions* d)))
|
||||||
|
|
||||||
|
(define (reductions* d)
|
||||||
|
(match d
|
||||||
|
[(AnyQ prule (e1 e2 rs))
|
||||||
|
(and rs (learn-definites rs))]
|
||||||
|
[_ (void)])
|
||||||
(match/with-derivation d
|
(match/with-derivation d
|
||||||
|
|
||||||
;; Primitives
|
;; Primitives
|
||||||
|
@ -47,12 +55,12 @@
|
||||||
[body-e1 (match body [(AnyQ deriv (body-e1 _)) body-e1])])
|
[body-e1 (match body [(AnyQ deriv (body-e1 _)) body-e1])])
|
||||||
(cons (walk e1 (ctx body-e1) 'tag-module-begin)
|
(cons (walk e1 (ctx body-e1) 'tag-module-begin)
|
||||||
(with-context ctx
|
(with-context ctx
|
||||||
(reductions body)))))]
|
(reductions* body)))))]
|
||||||
[(IntQ p:module (e1 e2 rs #t body))
|
[(IntQ p:module (e1 e2 rs #t body))
|
||||||
(with-syntax ([(?module name language . BODY) e1])
|
(with-syntax ([(?module name language . BODY) e1])
|
||||||
(let ([ctx (lambda (x) (d->so e1 `(,#'?module ,#'name ,#'language ,x)))])
|
(let ([ctx (lambda (x) (d->so e1 `(,#'?module ,#'name ,#'language ,x)))])
|
||||||
(with-context ctx
|
(with-context ctx
|
||||||
(reductions body))))]
|
(reductions* body))))]
|
||||||
[(AnyQ p:#%module-begin (e1 e2 rs pass1 pass2))
|
[(AnyQ p:#%module-begin (e1 e2 rs pass1 pass2))
|
||||||
(with-syntax ([(?#%module-begin form ...) e1])
|
(with-syntax ([(?#%module-begin form ...) e1])
|
||||||
(let ([frame (lambda (x) (d->so e1 (cons #'?#%module-begin x)))])
|
(let ([frame (lambda (x) (d->so e1 (cons #'?#%module-begin x)))])
|
||||||
|
@ -67,57 +75,58 @@
|
||||||
(list (stumble (frame final-stxs2) (error-wrap-exn d))))
|
(list (stumble (frame final-stxs2) (error-wrap-exn d))))
|
||||||
(append reductions1 reductions2))))))]
|
(append reductions1 reductions2))))))]
|
||||||
[(AnyQ p:define-syntaxes (e1 e2 rs rhs) exni)
|
[(AnyQ p:define-syntaxes (e1 e2 rs rhs) exni)
|
||||||
(R e1 _
|
(R e1
|
||||||
[! exni]
|
[! exni]
|
||||||
[#:pattern (?define-syntaxes formals RHS)]
|
[#:pattern (?define-syntaxes formals RHS)]
|
||||||
[Expr RHS rhs])]
|
[Expr RHS rhs])]
|
||||||
[(AnyQ p:define-values (e1 e2 rs rhs) exni)
|
[(AnyQ p:define-values (e1 e2 rs rhs) exni)
|
||||||
(R e1 _
|
(R e1
|
||||||
[! exni]
|
[! exni]
|
||||||
[#:pattern (?define-values formals RHS)]
|
[#:pattern (?define-values formals RHS)]
|
||||||
[#:if rhs
|
[#:if rhs
|
||||||
[Expr RHS rhs]])]
|
[Expr RHS rhs]])]
|
||||||
[(AnyQ p:if (e1 e2 rs full? test then else) exni)
|
[(AnyQ p:if (e1 e2 rs full? test then else) exni)
|
||||||
(if full?
|
(if full?
|
||||||
(R e1 _
|
(R e1
|
||||||
[! exni]
|
[! exni]
|
||||||
[#:pattern (?if TEST THEN ELSE)]
|
[#:pattern (?if TEST THEN ELSE)]
|
||||||
[Expr TEST test]
|
[Expr TEST test]
|
||||||
[Expr THEN then]
|
[Expr THEN then]
|
||||||
[Expr ELSE else])
|
[Expr ELSE else])
|
||||||
(R e1 _
|
(R e1
|
||||||
[! exni]
|
[! exni]
|
||||||
[#:pattern (?if TEST THEN)]
|
[#:pattern (?if TEST THEN)]
|
||||||
[Expr TEST test]
|
[Expr TEST test]
|
||||||
[Expr THEN then]))]
|
[Expr THEN then]))]
|
||||||
[(AnyQ p:wcm (e1 e2 rs key mark body) exni)
|
[(AnyQ p:wcm (e1 e2 rs key mark body) exni)
|
||||||
(R e1 _
|
(R e1
|
||||||
[! exni]
|
[! exni]
|
||||||
[#:pattern (?wcm KEY MARK BODY)]
|
[#:pattern (?wcm KEY MARK BODY)]
|
||||||
[Expr KEY key]
|
[Expr KEY key]
|
||||||
[Expr MARK mark]
|
[Expr MARK mark]
|
||||||
[Expr BODY body])]
|
[Expr BODY body])]
|
||||||
[(AnyQ p:begin (e1 e2 rs lderiv) exni)
|
[(AnyQ p:begin (e1 e2 rs lderiv) exni)
|
||||||
(R e1 _
|
(R e1
|
||||||
[! exni]
|
[! exni]
|
||||||
[#:pattern (?begin . LDERIV)]
|
[#:pattern (?begin . LDERIV)]
|
||||||
[List LDERIV lderiv])]
|
[List LDERIV lderiv])]
|
||||||
[(AnyQ p:begin0 (e1 e2 rs first lderiv) exni)
|
[(AnyQ p:begin0 (e1 e2 rs first lderiv) exni)
|
||||||
(R e1 _
|
(R e1
|
||||||
[! exni]
|
[! exni]
|
||||||
[#:pattern (?begin0 FIRST . LDERIV)]
|
[#:pattern (?begin0 FIRST . LDERIV)]
|
||||||
[Expr FIRST first]
|
[Expr FIRST first]
|
||||||
[List LDERIV lderiv])]
|
[List LDERIV lderiv])]
|
||||||
[(AnyQ p:#%app (e1 e2 rs tagged-stx lderiv) exni)
|
[(AnyQ p:#%app (e1 e2 rs tagged-stx lderiv) exni)
|
||||||
(let ([tail
|
(let ([tail
|
||||||
(R tagged-stx (?#%app . LDERIV)
|
(R tagged-stx
|
||||||
[! exni]
|
[! exni]
|
||||||
|
[#:pattern (?#%app . LDERIV)]
|
||||||
[List LDERIV lderiv])])
|
[List LDERIV lderiv])])
|
||||||
(if (eq? tagged-stx e1)
|
(if (eq? tagged-stx e1)
|
||||||
tail
|
tail
|
||||||
(cons (walk e1 tagged-stx 'tag-app) tail)))]
|
(cons (walk e1 tagged-stx 'tag-app) tail)))]
|
||||||
[(AnyQ p:lambda (e1 e2 rs renames body) exni)
|
[(AnyQ p:lambda (e1 e2 rs renames body) exni)
|
||||||
(R e1 _
|
(R e1
|
||||||
[! exni]
|
[! exni]
|
||||||
[#:bind (?formals* . ?body*) renames]
|
[#:bind (?formals* . ?body*) renames]
|
||||||
[#:pattern (?lambda ?formals . ?body)]
|
[#:pattern (?lambda ?formals . ?body)]
|
||||||
|
@ -127,7 +136,7 @@
|
||||||
[Block ?body body])]
|
[Block ?body body])]
|
||||||
[(struct p:case-lambda (e1 e2 rs renames+bodies))
|
[(struct p:case-lambda (e1 e2 rs renames+bodies))
|
||||||
#;
|
#;
|
||||||
(R e1 _
|
(R e1
|
||||||
[! exni]
|
[! exni]
|
||||||
[#:pattern (?case-lambda [?formals . ?body] ...)]
|
[#:pattern (?case-lambda [?formals . ?body] ...)]
|
||||||
[#:bind [(?formals* . ?body*) ...] (map car renames+bodies)]
|
[#:bind [(?formals* . ?body*) ...] (map car renames+bodies)]
|
||||||
|
@ -144,10 +153,11 @@
|
||||||
(syntax->list #'(?formals* ...))
|
(syntax->list #'(?formals* ...))
|
||||||
e1 mid 'rename-case-lambda)
|
e1 mid 'rename-case-lambda)
|
||||||
;; FIXME: Missing renames frames here
|
;; FIXME: Missing renames frames here
|
||||||
(R mid (CASE-LAMBDA [FORMALS . BODY] ...)
|
(R mid
|
||||||
|
[#:pattern (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)
|
||||||
(R e1 _
|
(R e1
|
||||||
[! exni]
|
[! exni]
|
||||||
[#:pattern (?let-values ([?vars ?rhs] ...) . ?body)]
|
[#:pattern (?let-values ([?vars ?rhs] ...) . ?body)]
|
||||||
[#:bind (([?vars* ?rhs*] ...) . ?body*) renames]
|
[#:bind (([?vars* ?rhs*] ...) . ?body*) renames]
|
||||||
|
@ -159,7 +169,7 @@
|
||||||
[Expr (?rhs ...) rhss]
|
[Expr (?rhs ...) rhss]
|
||||||
[Block ?body body])]
|
[Block ?body body])]
|
||||||
[(AnyQ p:letrec-values (e1 e2 rs renames rhss body) exni)
|
[(AnyQ p:letrec-values (e1 e2 rs renames rhss body) exni)
|
||||||
(R e1 _
|
(R e1
|
||||||
[! exni]
|
[! exni]
|
||||||
[#:pattern (?letrec-values ([?vars ?rhs] ...) . ?body)]
|
[#:pattern (?letrec-values ([?vars ?rhs] ...) . ?body)]
|
||||||
[#:bind (([?vars* ?rhs*] ...) . ?body*) renames]
|
[#:bind (([?vars* ?rhs*] ...) . ?body*) renames]
|
||||||
|
@ -172,7 +182,7 @@
|
||||||
[Block ?body body])]
|
[Block ?body body])]
|
||||||
[(AnyQ p:letrec-syntaxes+values
|
[(AnyQ p:letrec-syntaxes+values
|
||||||
(e1 e2 rs srenames srhss vrenames vrhss body) exni)
|
(e1 e2 rs srenames srhss vrenames vrhss body) exni)
|
||||||
(R e1 _
|
(R e1
|
||||||
[! exni]
|
[! exni]
|
||||||
[#:pattern (?lsv ([?svars ?srhs] ...) ([?vvars ?vrhs] ...) . ?body)]
|
[#:pattern (?lsv ([?svars ?srhs] ...) ([?vvars ?vrhs] ...) . ?body)]
|
||||||
[#:bind (([?svars* ?srhs*] ...) ([?vvars* ?vrhs] ...) . ?body*) srenames]
|
[#:bind (([?svars* ?srhs*] ...) ([?vvars* ?vrhs] ...) . ?body*) srenames]
|
||||||
|
@ -216,18 +226,19 @@
|
||||||
|
|
||||||
;; The rest of the automatic primitives
|
;; The rest of the automatic primitives
|
||||||
[(AnyQ p::STOP (e1 e2 rs) exni)
|
[(AnyQ p::STOP (e1 e2 rs) exni)
|
||||||
(R e1 _
|
(R e1
|
||||||
[! exni])]
|
[! exni])]
|
||||||
|
|
||||||
[(AnyQ p:set!-macro (e1 e2 rs deriv) exni)
|
[(AnyQ p:set!-macro (e1 e2 rs deriv) exni)
|
||||||
(R e1 _
|
(R e1
|
||||||
[! exni]
|
[! exni]
|
||||||
=> (lambda (mid)
|
=> (lambda (mid)
|
||||||
(reductions deriv)))]
|
(reductions* deriv)))]
|
||||||
[(AnyQ p:set! (e1 e2 rs id-rs rhs) exni)
|
[(AnyQ p:set! (e1 e2 rs id-rs rhs) exni)
|
||||||
(R e1 _
|
(R e1
|
||||||
[! exni]
|
[! exni]
|
||||||
[#:pattern (SET! VAR RHS)]
|
[#:pattern (SET! VAR RHS)]
|
||||||
|
[#:learn id-rs]
|
||||||
[Expr RHS rhs])]
|
[Expr RHS rhs])]
|
||||||
|
|
||||||
;; Synthetic primitives
|
;; Synthetic primitives
|
||||||
|
@ -245,7 +256,7 @@
|
||||||
[deriv0 (s:subterm-deriv subterm0)])
|
[deriv0 (s:subterm-deriv subterm0)])
|
||||||
(let ([ctx (lambda (x) (path-replace term path0 x))])
|
(let ([ctx (lambda (x) (path-replace term path0 x))])
|
||||||
(append (with-context ctx
|
(append (with-context ctx
|
||||||
(reductions deriv0))
|
(reductions* deriv0))
|
||||||
(loop (and (deriv? deriv0)
|
(loop (and (deriv? deriv0)
|
||||||
(path-replace term path0 (deriv-e2 deriv0)))
|
(path-replace term path0 (deriv-e2 deriv0)))
|
||||||
(cdr subterms)))))]
|
(cdr subterms)))))]
|
||||||
|
@ -260,21 +271,21 @@
|
||||||
|
|
||||||
;; FIXME
|
;; FIXME
|
||||||
[(IntQ p:rename (e1 e2 rs rename inner))
|
[(IntQ p:rename (e1 e2 rs rename inner))
|
||||||
(reductions inner)]
|
(reductions* inner)]
|
||||||
|
|
||||||
;; Error
|
;; Error
|
||||||
|
|
||||||
;; Macros
|
;; Macros
|
||||||
[(IntQ mrule (e1 e2 transformation next))
|
[(IntQ mrule (e1 e2 transformation next))
|
||||||
(append (reductions-transformation transformation)
|
(append (reductions-transformation transformation)
|
||||||
(reductions next))]
|
(reductions* next))]
|
||||||
|
|
||||||
;; Lifts
|
;; Lifts
|
||||||
|
|
||||||
[(IntQ lift-deriv (e1 e2 first lifted-stx second))
|
[(IntQ lift-deriv (e1 e2 first lifted-stx second))
|
||||||
(append (reductions first)
|
(append (reductions* first)
|
||||||
(list (walk (deriv-e2 first) lifted-stx 'capture-lifts))
|
(list (walk (deriv-e2 first) lifted-stx 'capture-lifts))
|
||||||
(reductions second))]
|
(reductions* second))]
|
||||||
|
|
||||||
;; Skipped
|
;; Skipped
|
||||||
|
|
||||||
|
@ -287,13 +298,17 @@
|
||||||
(define (reductions-transformation tx)
|
(define (reductions-transformation tx)
|
||||||
(match tx
|
(match tx
|
||||||
[(struct transformation (e1 e2 rs me1 me2 locals seq))
|
[(struct transformation (e1 e2 rs me1 me2 locals seq))
|
||||||
|
(learn-definites rs)
|
||||||
(append (reductions-locals e1 locals)
|
(append (reductions-locals e1 locals)
|
||||||
(list (walk e1 e2 'macro-step)))]
|
(list (walk e1 e2 'macro-step)))]
|
||||||
[(IntW transformation (e1 e2 rs me1 me2 locals seq) 'locals)
|
[(IntW transformation (e1 e2 rs me1 me2 locals seq) 'locals)
|
||||||
|
(learn-definites rs)
|
||||||
(reductions-locals e1 locals)]
|
(reductions-locals e1 locals)]
|
||||||
[(ErrW transformation (e1 e2 rs me1 me2 locals seq) 'bad-transformer exn)
|
[(ErrW transformation (e1 e2 rs me1 me2 locals seq) 'bad-transformer exn)
|
||||||
|
(learn-definites rs)
|
||||||
(list (stumble e1 exn))]
|
(list (stumble e1 exn))]
|
||||||
[(ErrW transformation (e1 e2 rs me1 me2 locals seq) 'transform exn)
|
[(ErrW transformation (e1 e2 rs me1 me2 locals seq) 'transform exn)
|
||||||
|
(learn-definites rs)
|
||||||
(append (reductions-locals e1 locals)
|
(append (reductions-locals e1 locals)
|
||||||
(list (stumble e1 exn)))]))
|
(list (stumble e1 exn)))]))
|
||||||
|
|
||||||
|
@ -306,13 +321,13 @@
|
||||||
(define (reductions-local local)
|
(define (reductions-local local)
|
||||||
(match/with-derivation local
|
(match/with-derivation local
|
||||||
[(struct local-expansion (e1 e2 me1 me2 deriv))
|
[(struct local-expansion (e1 e2 me1 me2 deriv))
|
||||||
(reductions deriv)]
|
(reductions* deriv)]
|
||||||
[(struct local-lift (expr id))
|
[(struct local-lift (expr id))
|
||||||
(list (walk expr id 'local-lift))]
|
(list (walk expr id 'local-lift))]
|
||||||
[(struct local-lift-end (decl))
|
[(struct local-lift-end (decl))
|
||||||
(list (walk decl decl 'module-lift))]
|
(list (walk decl decl 'module-lift))]
|
||||||
[(struct local-bind (deriv))
|
[(struct local-bind (deriv))
|
||||||
(reductions deriv)]))
|
(reductions* deriv)]))
|
||||||
|
|
||||||
;; list-reductions : ListDerivation -> ReductionSequence
|
;; list-reductions : ListDerivation -> ReductionSequence
|
||||||
(define (list-reductions ld)
|
(define (list-reductions ld)
|
||||||
|
@ -322,7 +337,7 @@
|
||||||
(cond [(pair? derivs)
|
(cond [(pair? derivs)
|
||||||
(append
|
(append
|
||||||
(with-context (lambda (x) (cons x (stx-cdr suffix)))
|
(with-context (lambda (x) (cons x (stx-cdr suffix)))
|
||||||
(reductions (car derivs)))
|
(reductions* (car derivs)))
|
||||||
(with-context (lambda (x) (cons (deriv-e2 (car derivs)) x))
|
(with-context (lambda (x) (cons (deriv-e2 (car derivs)) x))
|
||||||
(loop (cdr derivs) (stx-cdr suffix))))]
|
(loop (cdr derivs) (stx-cdr suffix))))]
|
||||||
[(null? derivs)
|
[(null? derivs)
|
||||||
|
@ -362,17 +377,17 @@
|
||||||
(let ([estx (deriv-e2 head)])
|
(let ([estx (deriv-e2 head)])
|
||||||
(loop next (stx-cdr suffix) (cons estx prefix)
|
(loop next (stx-cdr suffix) (cons estx prefix)
|
||||||
(cons (with-context (lambda (x) (revappend prefix (cons x (stx-cdr suffix))))
|
(cons (with-context (lambda (x) (revappend prefix (cons x (stx-cdr suffix))))
|
||||||
(reductions head))
|
(reductions* head))
|
||||||
rss)))]
|
rss)))]
|
||||||
[(IntW b:expr (renames head) tag)
|
[(IntW b:expr (renames head) tag)
|
||||||
(loop next #f #f
|
(loop next #f #f
|
||||||
(cons (with-context (lambda (x) (revappend prefix (cons x (stx-cdr suffix))))
|
(cons (with-context (lambda (x) (revappend prefix (cons x (stx-cdr suffix))))
|
||||||
(reductions head))
|
(reductions* head))
|
||||||
rss))]
|
rss))]
|
||||||
[(struct b:defvals (renames head))
|
[(struct b:defvals (renames head))
|
||||||
(let ([head-rs
|
(let ([head-rs
|
||||||
(with-context (lambda (x) (revappend prefix (cons x (stx-cdr suffix))))
|
(with-context (lambda (x) (revappend prefix (cons x (stx-cdr suffix))))
|
||||||
(reductions head))])
|
(reductions* head))])
|
||||||
(loop next (stx-cdr suffix) (cons (deriv-e2 head) prefix)
|
(loop next (stx-cdr suffix) (cons (deriv-e2 head) prefix)
|
||||||
(cons head-rs rss)))]
|
(cons head-rs rss)))]
|
||||||
[(AnyQ b:defstx (renames head rhs))
|
[(AnyQ b:defstx (renames head rhs))
|
||||||
|
@ -386,8 +401,8 @@
|
||||||
(loop next (stx-cdr suffix) (cons estx2 prefix)
|
(loop next (stx-cdr suffix) (cons estx2 prefix)
|
||||||
(with-context (lambda (x) (revappend prefix (cons x (stx-cdr suffix))))
|
(with-context (lambda (x) (revappend prefix (cons x (stx-cdr suffix))))
|
||||||
(cons (with-context (CC ?rhs estx (?ds ?vars ?rhs))
|
(cons (with-context (CC ?rhs estx (?ds ?vars ?rhs))
|
||||||
(reductions rhs))
|
(reductions* rhs))
|
||||||
(cons (reductions head)
|
(cons (reductions* head)
|
||||||
rss)))))]
|
rss)))))]
|
||||||
[(struct b:splice (renames head tail))
|
[(struct b:splice (renames head tail))
|
||||||
(loop next tail prefix
|
(loop next tail prefix
|
||||||
|
@ -401,7 +416,7 @@
|
||||||
'splice-block))
|
'splice-block))
|
||||||
(cons (with-context (lambda (x)
|
(cons (with-context (lambda (x)
|
||||||
(revappend prefix (cons x (stx-cdr suffix))))
|
(revappend prefix (cons x (stx-cdr suffix))))
|
||||||
(reductions head))
|
(reductions* head))
|
||||||
rss)))]
|
rss)))]
|
||||||
[(struct b:begin (renames head derivs))
|
[(struct b:begin (renames head derivs))
|
||||||
;; FIXME
|
;; FIXME
|
||||||
|
@ -430,24 +445,24 @@
|
||||||
[(struct mod:skip ())
|
[(struct mod:skip ())
|
||||||
(loop next (stx-cdr suffix) (cons (stx-car suffix) prefix))]
|
(loop next (stx-cdr suffix) (cons (stx-car suffix) prefix))]
|
||||||
[(struct mod:cons (head))
|
[(struct mod:cons (head))
|
||||||
(append (with-context the-context (append (reductions head)))
|
(append (with-context the-context (append (reductions* head)))
|
||||||
(let ([estx (and (deriv? head) (deriv-e2 head))])
|
(let ([estx (and (deriv? head) (deriv-e2 head))])
|
||||||
(loop next (stx-cdr suffix) (cons estx prefix))))]
|
(loop next (stx-cdr suffix) (cons estx prefix))))]
|
||||||
[(AnyQ mod:prim (head prim))
|
[(AnyQ mod:prim (head prim))
|
||||||
(append (with-context the-context
|
(append (with-context the-context
|
||||||
(append (reductions head)
|
(append (reductions* head)
|
||||||
(reductions prim)))
|
(reductions* prim)))
|
||||||
(let ([estx
|
(let ([estx
|
||||||
(if prim
|
(if prim
|
||||||
(lift/deriv-e2 prim)
|
(lift/deriv-e2 prim)
|
||||||
(and (deriv? head) (deriv-e2 head)))])
|
(and (deriv? head) (deriv-e2 head)))])
|
||||||
(loop next (stx-cdr suffix) (cons estx prefix))))]
|
(loop next (stx-cdr suffix) (cons estx prefix))))]
|
||||||
[(ErrW mod:splice (head stxs) exn)
|
[(ErrW mod:splice (head stxs) exn)
|
||||||
(append (with-context the-context (reductions head))
|
(append (with-context the-context (reductions* head))
|
||||||
(list (stumble (deriv-e2 head) exn)))]
|
(list (stumble (deriv-e2 head) exn)))]
|
||||||
[(struct mod:splice (head stxs))
|
[(struct mod:splice (head stxs))
|
||||||
(append
|
(append
|
||||||
(with-context the-context (reductions head))
|
(with-context the-context (reductions* head))
|
||||||
(let ([suffix-tail (stx-cdr suffix)]
|
(let ([suffix-tail (stx-cdr suffix)]
|
||||||
[head-e2 (deriv-e2 head)])
|
[head-e2 (deriv-e2 head)])
|
||||||
(cons (walk/foci head-e2
|
(cons (walk/foci head-e2
|
||||||
|
@ -460,7 +475,7 @@
|
||||||
(loop next stxs prefix))))]
|
(loop next stxs prefix))))]
|
||||||
[(struct mod:lift (head stxs))
|
[(struct mod:lift (head stxs))
|
||||||
(append
|
(append
|
||||||
(with-context the-context (reductions head))
|
(with-context the-context (reductions* head))
|
||||||
(let ([suffix-tail (stx-cdr suffix)]
|
(let ([suffix-tail (stx-cdr suffix)]
|
||||||
[head-e2 (deriv-e2 head)])
|
[head-e2 (deriv-e2 head)])
|
||||||
(let ([new-suffix (append stxs (cons head-e2 suffix-tail))])
|
(let ([new-suffix (append stxs (cons head-e2 suffix-tail))])
|
||||||
|
|
|
@ -5,7 +5,7 @@
|
||||||
|
|
||||||
;; 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 Definites)
|
||||||
|
|
||||||
;; A Context is a list of Frames
|
;; A Context is a list of Frames
|
||||||
;; A Frame is either:
|
;; A Frame is either:
|
||||||
|
@ -14,6 +14,8 @@
|
||||||
;; - 'phase-up
|
;; - 'phase-up
|
||||||
(define-struct renames (old new))
|
(define-struct renames (old new))
|
||||||
|
|
||||||
|
;; A Definite is a (list-of identifier)
|
||||||
|
|
||||||
;; 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)
|
||||||
(define-struct bigframe (deriv ctx foci e))
|
(define-struct bigframe (deriv ctx foci e))
|
||||||
|
@ -22,7 +24,7 @@
|
||||||
;; - (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 definites) #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)
|
||||||
|
|
|
@ -57,7 +57,8 @@
|
||||||
|
|
||||||
(define text:arrows<%>
|
(define text:arrows<%>
|
||||||
(interface (text:mouse-drawings<%>)
|
(interface (text:mouse-drawings<%>)
|
||||||
add-arrow))
|
add-arrow
|
||||||
|
add-question-arrow))
|
||||||
|
|
||||||
(define text:drawings-mixin
|
(define text:drawings-mixin
|
||||||
(mixin (text:basic<%>) (text:drawings<%>)
|
(mixin (text:basic<%>) (text:drawings<%>)
|
||||||
|
@ -136,8 +137,14 @@
|
||||||
(define (?-font dc)
|
(define (?-font dc)
|
||||||
(let ([size (send (send dc get-font) get-point-size)])
|
(let ([size (send (send dc get-font) get-point-size)])
|
||||||
(send the-font-list find-or-create-font size 'default 'normal 'bold)))
|
(send the-font-list find-or-create-font size 'default 'normal 'bold)))
|
||||||
|
|
||||||
(define/public (add-arrow from1 from2 to1 to2 color)
|
(define/public (add-arrow from1 from2 to1 to2 color)
|
||||||
|
(internal-add-arrow from1 from2 to1 to2 color #f))
|
||||||
|
|
||||||
|
(define/public (add-question-arrow from1 from2 to1 to2 color)
|
||||||
|
(internal-add-arrow from1 from2 to1 to2 color #t))
|
||||||
|
|
||||||
|
(define/private (internal-add-arrow from1 from2 to1 to2 color question?)
|
||||||
(unless (and (= from1 to1) (= from2 to2))
|
(unless (and (= from1 to1) (= from2 to2))
|
||||||
(let ([draw
|
(let ([draw
|
||||||
(lambda (text dc left top right bottom dx dy)
|
(lambda (text dc left top right bottom dx dy)
|
||||||
|
@ -158,15 +165,16 @@
|
||||||
(send dc set-brush arrow-brush)
|
(send dc set-brush arrow-brush)
|
||||||
(draw-arrow dc startx starty endx endy dx dy)
|
(draw-arrow dc startx starty endx endy dx dy)
|
||||||
#;(send dc set-text-mode 'solid)
|
#;(send dc set-text-mode 'solid)
|
||||||
(send dc set-font (?-font dc))
|
(when question?
|
||||||
(send dc set-text-foreground
|
(send dc set-font (?-font dc))
|
||||||
(send the-color-database find-color color))
|
(send dc set-text-foreground
|
||||||
(send dc draw-text "?"
|
(send the-color-database find-color color))
|
||||||
(+ (+ startx dx) fw)
|
(send dc draw-text "?"
|
||||||
(- (+ starty dy) fh)))))))])
|
(+ (+ startx dx) fw)
|
||||||
|
(- (+ starty dy) fh))))))))])
|
||||||
(add-mouse-drawing from1 from2 draw)
|
(add-mouse-drawing from1 from2 draw)
|
||||||
(add-mouse-drawing to1 to2 draw))))
|
(add-mouse-drawing to1 to2 draw))))
|
||||||
|
|
||||||
(define/private (position->location p)
|
(define/private (position->location p)
|
||||||
(define xbox (box 0.0))
|
(define xbox (box 0.0))
|
||||||
(define ybox (box 0.0))
|
(define ybox (box 0.0))
|
||||||
|
|
|
@ -96,10 +96,12 @@
|
||||||
(send -text insert text)))
|
(send -text insert text)))
|
||||||
|
|
||||||
(define/public add-syntax
|
(define/public add-syntax
|
||||||
(lambda/kw (stx #:key [hi-stxs null] hi-color alpha-table)
|
(lambda/kw (stx #:key [hi-stxs null] hi-color alpha-table [definites null])
|
||||||
(when (and (pair? hi-stxs) (not hi-color))
|
(when (and (pair? hi-stxs) (not hi-color))
|
||||||
(error 'syntax-widget%::add-syntax "no highlight color specified"))
|
(error 'syntax-widget%::add-syntax "no highlight color specified"))
|
||||||
(let ([colorer (internal-add-syntax stx hi-stxs hi-color)])
|
(let ([colorer (internal-add-syntax stx hi-stxs hi-color)]
|
||||||
|
[definite-table (make-hash-table)])
|
||||||
|
(for-each (lambda (x) (hash-table-put! definite-table x #t)) definites)
|
||||||
(when alpha-table
|
(when alpha-table
|
||||||
(let ([range (send colorer get-range)])
|
(let ([range (send colorer get-range)])
|
||||||
(for-each (lambda (id)
|
(for-each (lambda (id)
|
||||||
|
@ -111,10 +113,15 @@
|
||||||
(for-each
|
(for-each
|
||||||
(lambda (binder-r)
|
(lambda (binder-r)
|
||||||
(for-each (lambda (id-r)
|
(for-each (lambda (id-r)
|
||||||
(send -text add-arrow
|
(if (hash-table-get definite-table id #f)
|
||||||
(car id-r) (cdr id-r)
|
(send -text add-arrow
|
||||||
(car binder-r) (cdr binder-r)
|
(car id-r) (cdr id-r)
|
||||||
"purple"))
|
(car binder-r) (cdr binder-r)
|
||||||
|
"blue")
|
||||||
|
(send -text add-question-arrow
|
||||||
|
(car id-r) (cdr id-r)
|
||||||
|
(car binder-r) (cdr binder-r)
|
||||||
|
"purple")))
|
||||||
(send range get-ranges id)))
|
(send range get-ranges id)))
|
||||||
(send range get-ranges binder)))))
|
(send range get-ranges binder)))))
|
||||||
(send colorer get-identifier-list))))
|
(send colorer get-identifier-list))))
|
||||||
|
|
Loading…
Reference in New Issue
Block a user