Macro stepper:
cleaned up representation of big (localaction) contexts unitized hiding impl added (broken/experimental) navigation tools (jump, zoom) svn: r5468
This commit is contained in:
parent
c7b622c537
commit
ef1f77c33f
|
@ -1,20 +1,24 @@
|
||||||
|
|
||||||
(module hide mzscheme
|
(module hide mzscheme
|
||||||
(require (lib "plt-match.ss")
|
(require (lib "plt-match.ss")
|
||||||
|
(lib "unit.ss")
|
||||||
(lib "list.ss")
|
(lib "list.ss")
|
||||||
"deriv.ss"
|
"deriv.ss"
|
||||||
"deriv-util.ss"
|
"deriv-util.ss"
|
||||||
"synth-engine.ss"
|
"synth-engine.ss"
|
||||||
"stx-util.ss"
|
"stx-util.ss"
|
||||||
"context.ss")
|
"context.ss")
|
||||||
(provide (all-defined))
|
|
||||||
|
|
||||||
#;
|
|
||||||
(provide hide/policy
|
(provide hide/policy
|
||||||
hide
|
seek/syntax
|
||||||
#;seek/syntax
|
|
||||||
macro-policy
|
macro-policy
|
||||||
current-hiding-warning-handler)
|
current-hiding-warning-handler
|
||||||
|
(struct nonlinearity (message paths))
|
||||||
|
(struct localactions ()))
|
||||||
|
|
||||||
|
(define-signature hide^ (hide))
|
||||||
|
(define-signature seek^ (seek/deriv seek subterm-derivations))
|
||||||
|
(define-signature seek-syntax^ (seek/syntax))
|
||||||
|
|
||||||
;; hide/policy : Derivation (identifier -> boolean) -> (values Derivation syntax)
|
;; hide/policy : Derivation (identifier -> boolean) -> (values Derivation syntax)
|
||||||
(define (hide/policy deriv show-macro?)
|
(define (hide/policy deriv show-macro?)
|
||||||
|
@ -87,6 +91,11 @@
|
||||||
; -$ @- ++ -@- $@- @+ -
|
; -$ @- ++ -@- $@- @+ -
|
||||||
; -$ @- ++ +@@+@- -@@@@-
|
; -$ @- ++ +@@+@- -@@@@-
|
||||||
|
|
||||||
|
(define hide@
|
||||||
|
(unit
|
||||||
|
(import seek^)
|
||||||
|
(export hide^)
|
||||||
|
|
||||||
;; Macro hiding:
|
;; Macro hiding:
|
||||||
;; The derivation is "visible" or "active" by default,
|
;; The derivation is "visible" or "active" by default,
|
||||||
;; but pieces of it may need to be hidden.
|
;; but pieces of it may need to be hidden.
|
||||||
|
@ -444,7 +453,7 @@
|
||||||
[#f (values #f #f)]))
|
[#f (values #f #f)]))
|
||||||
|
|
||||||
(for-deriv deriv))
|
(for-deriv deriv))
|
||||||
|
))
|
||||||
|
|
||||||
; -@@@$ -$
|
; -@@@$ -$
|
||||||
; @* - -$
|
; @* - -$
|
||||||
|
@ -457,28 +466,16 @@
|
||||||
; +- +@ @+ - @+ - -$ +@
|
; +- +@ @+ - @+ - -$ +@
|
||||||
; -@@@@- -@@@@- -@@@@- -$ $+
|
; -@@@@- -@@@@- -@@@@- -$ $+
|
||||||
|
|
||||||
|
(define seek@
|
||||||
|
(unit
|
||||||
|
(import hide^)
|
||||||
|
(export seek^)
|
||||||
|
|
||||||
;; Seek:
|
;; Seek:
|
||||||
;; The derivation is "inactive" or "hidden" by default,
|
;; The derivation is "inactive" or "hidden" by default,
|
||||||
;; but pieces of it can become visible if they correspond to subterms
|
;; but pieces of it can become visible if they correspond to subterms
|
||||||
;; of the hidden syntax.
|
;; of the hidden syntax.
|
||||||
|
|
||||||
;; seek/syntax : syntax Derivation -> (union (cons Derivation Derivation) #f)
|
|
||||||
;; Seeks for derivations of *exactly* the given syntax (not a subterm)
|
|
||||||
;; Does track the syntax through renaming, however.
|
|
||||||
;; Returns the whole derivation followed by the subterm derivation.
|
|
||||||
;; If there is no subderivation for that syntax, returns #f.
|
|
||||||
#;
|
|
||||||
(define (seek/syntax stx deriv)
|
|
||||||
(let ([subterms (gather-one-subterm (deriv-e1 deriv) stx)])
|
|
||||||
(parameterize ((subterms-table subterms))
|
|
||||||
(let ([subderivs (subterm-derivations deriv)])
|
|
||||||
(unless (and (pair? subderivs) (null? (cdr subderivs)))
|
|
||||||
(error 'seek/syntax "nonlinear subterm derivations"))
|
|
||||||
(if (pair? subderivs)
|
|
||||||
(values (create-synth-deriv (deriv-e1 deriv) subderivs)
|
|
||||||
(s:subterm-deriv (car subderivs)))
|
|
||||||
#f)))))
|
|
||||||
|
|
||||||
;; seek/deriv : Derivation -> (values Derivation syntax)
|
;; seek/deriv : Derivation -> (values Derivation syntax)
|
||||||
;; Seeks for derivations of all proper subterms of the derivation's
|
;; Seeks for derivations of all proper subterms of the derivation's
|
||||||
;; initial syntax.
|
;; initial syntax.
|
||||||
|
@ -714,6 +711,77 @@
|
||||||
|
|
||||||
(for-deriv d))
|
(for-deriv d))
|
||||||
|
|
||||||
|
))
|
||||||
|
|
||||||
|
(define-values/invoke-unit
|
||||||
|
(compound-unit
|
||||||
|
(import)
|
||||||
|
(export HIDE SEEK)
|
||||||
|
(link [((HIDE : hide^)) hide@ SEEK]
|
||||||
|
[((SEEK : seek^)) seek@ HIDE]))
|
||||||
|
(import)
|
||||||
|
(export hide^ seek^))
|
||||||
|
|
||||||
|
|
||||||
|
(define trivial-hide@
|
||||||
|
(unit
|
||||||
|
(import)
|
||||||
|
(export hide^)
|
||||||
|
|
||||||
|
(define (hide d)
|
||||||
|
(values d (lift/deriv-e2 d)))))
|
||||||
|
|
||||||
|
(define seek-syntax@
|
||||||
|
(unit
|
||||||
|
(import seek^)
|
||||||
|
(export seek-syntax^)
|
||||||
|
|
||||||
|
;; seek/syntax : syntax Derivation -> (listof Derivation)
|
||||||
|
;; Seeks for derivations of *exactly* the given syntax (not a subterm)
|
||||||
|
;; Does track the syntax through renaming, however.
|
||||||
|
(define (seek/syntax stx deriv)
|
||||||
|
(let ([subterms (gather-one-subterm (deriv-e1 deriv) stx)])
|
||||||
|
(parameterize ((subterms-table subterms))
|
||||||
|
(let ([subderivs (subterm-derivations deriv)])
|
||||||
|
(map s:subterm-deriv (filter s:subterm? subderivs))))))))
|
||||||
|
|
||||||
|
(define-values/invoke-unit
|
||||||
|
(compound-unit
|
||||||
|
(import)
|
||||||
|
(export SEEK-SYNTAX)
|
||||||
|
(link [((HIDE : hide^)) trivial-hide@]
|
||||||
|
[((SEEK : seek^)) seek@ HIDE]
|
||||||
|
[((SEEK-SYNTAX : seek-syntax^)) seek-syntax@ SEEK]))
|
||||||
|
(import)
|
||||||
|
(export seek-syntax^))
|
||||||
|
|
||||||
|
|
||||||
|
; +###+
|
||||||
|
; +@@ +@@: @+
|
||||||
|
; @+ @+ @+
|
||||||
|
; @+ @+ @+
|
||||||
|
; @+ @+ +###+ @+ :@@ +@+ +###+ :@$$ +@# -+###+:
|
||||||
|
; @+ @+ +#: #+ @+ +@+**@+ +#: #+ :+@++*@ #+ ++
|
||||||
|
; @@###@+ #+ +# @+ +@: +# #+ +# +@: + @+ ::
|
||||||
|
; @+ @+ @@###@# @+ +@ +@ @@###@# +@ +@#++
|
||||||
|
; @+ @+ @+ @+ +@ +@ @+ +@ ++#@+
|
||||||
|
; @+ @+ #+ @+ +@ ++ #+ +@ + +@
|
||||||
|
; @+ @+ :@+- :+ @+ +@- +@* :@+- :+ +@ @: ++
|
||||||
|
; +@# +@#- :+@@#+ +##@@## +@$$#+ :+@@#+ :#@@##+ +#@##+
|
||||||
|
; +@
|
||||||
|
; +@
|
||||||
|
; :###+
|
||||||
|
|
||||||
|
;; show-macro? : identifier -> boolean
|
||||||
|
(define (show-macro? id)
|
||||||
|
((macro-policy) id))
|
||||||
|
|
||||||
|
;; show-mrule? : MRule -> boolean
|
||||||
|
(define (show-transformation? tx)
|
||||||
|
(match tx
|
||||||
|
[(AnyQ transformation (e1 e2 rs me1 me2 locals _seq))
|
||||||
|
(ormap show-macro? rs)]))
|
||||||
|
|
||||||
|
|
||||||
;; check-nonlinear-subterms : (list-of Subterm) -> void
|
;; check-nonlinear-subterms : (list-of Subterm) -> void
|
||||||
;; FIXME: No checking on renamings... need to add
|
;; FIXME: No checking on renamings... need to add
|
||||||
|
@ -827,34 +895,6 @@
|
||||||
(loop stx0 null)
|
(loop stx0 null)
|
||||||
table))
|
table))
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
; +###+
|
|
||||||
; +@@ +@@: @+
|
|
||||||
; @+ @+ @+
|
|
||||||
; @+ @+ @+
|
|
||||||
; @+ @+ +###+ @+ :@@ +@+ +###+ :@$$ +@# -+###+:
|
|
||||||
; @+ @+ +#: #+ @+ +@+**@+ +#: #+ :+@++*@ #+ ++
|
|
||||||
; @@###@+ #+ +# @+ +@: +# #+ +# +@: + @+ ::
|
|
||||||
; @+ @+ @@###@# @+ +@ +@ @@###@# +@ +@#++
|
|
||||||
; @+ @+ @+ @+ +@ +@ @+ +@ ++#@+
|
|
||||||
; @+ @+ #+ @+ +@ ++ #+ +@ + +@
|
|
||||||
; @+ @+ :@+- :+ @+ +@- +@* :@+- :+ +@ @: ++
|
|
||||||
; +@# +@#- :+@@#+ +##@@## +@$$#+ :+@@#+ :#@@##+ +#@##+
|
|
||||||
; +@
|
|
||||||
; +@
|
|
||||||
; :###+
|
|
||||||
|
|
||||||
;; show-macro? : identifier -> boolean
|
|
||||||
(define (show-macro? id)
|
|
||||||
((macro-policy) id))
|
|
||||||
|
|
||||||
;; show-mrule? : MRule -> boolean
|
|
||||||
(define (show-transformation? tx)
|
|
||||||
(match tx
|
|
||||||
[(AnyQ transformation (e1 e2 rs me1 me2 locals _seq))
|
|
||||||
(ormap show-macro? rs)]))
|
|
||||||
|
|
||||||
(define (map/2values f items)
|
(define (map/2values f items)
|
||||||
(if (null? items)
|
(if (null? items)
|
||||||
(values null null)
|
(values null null)
|
||||||
|
|
|
@ -44,9 +44,7 @@
|
||||||
(syntax-rules ()
|
(syntax-rules ()
|
||||||
[(with-new-local-context e . body)
|
[(with-new-local-context e . body)
|
||||||
(parameterize ([big-context
|
(parameterize ([big-context
|
||||||
(cons (cons (current-derivation)
|
(cons (make-bigframe (current-derivation) (context) (list e) e)
|
||||||
(cons (list e)
|
|
||||||
(context)))
|
|
||||||
(big-context))]
|
(big-context))]
|
||||||
[context null])
|
[context null])
|
||||||
. body)]))
|
. body)]))
|
||||||
|
|
|
@ -9,8 +9,9 @@
|
||||||
;; A Context is a list of Frames
|
;; A Context is a list of Frames
|
||||||
;; A Frame is (syntax -> syntax)
|
;; A Frame is (syntax -> syntax)
|
||||||
|
|
||||||
;; A BigContext is (list-of (cons Derivation (cons Syntaxes Syntax)))
|
;; A BigContext is (list-of BigFrame)
|
||||||
;; local expansion contexts: deriv, foci, term
|
;; A BigFrame is (make-bigframe Derivation Context Syntaxes Syntax)
|
||||||
|
(define-struct bigframe (deriv ctx foci e))
|
||||||
|
|
||||||
;; A Reduction is one of
|
;; A Reduction is one of
|
||||||
;; - (make-step ... Syntaxes Syntaxes Syntax Syntax)
|
;; - (make-step ... Syntaxes Syntaxes Syntax Syntax)
|
||||||
|
@ -36,6 +37,9 @@
|
||||||
(define (misstep-term1 s)
|
(define (misstep-term1 s)
|
||||||
(context-fill (protostep-ctx s) (misstep-e1 s)))
|
(context-fill (protostep-ctx s) (misstep-e1 s)))
|
||||||
|
|
||||||
|
(define (bigframe-term 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
|
||||||
|
|
|
@ -326,11 +326,11 @@
|
||||||
(define nav:down
|
(define nav:down
|
||||||
(new button% (label "Next term") (parent navigator) (style '(deleted))
|
(new button% (label "Next term") (parent navigator) (style '(deleted))
|
||||||
(callback (lambda (b e) (navigate-down)))))
|
(callback (lambda (b e) (navigate-down)))))
|
||||||
#;
|
|
||||||
(define nav:zoom
|
(define nav:zoom
|
||||||
(new button% (label "Zoom in") (parent extra-navigator)
|
(new button% (label "Zoom in") (parent extra-navigator)
|
||||||
(callback (lambda (b e) (zoom)))))
|
(callback (lambda (b e) (zoom)))))
|
||||||
#;
|
|
||||||
(define nav:jump-to
|
(define nav:jump-to
|
||||||
(new button% (label "Jump to") (parent extra-navigator)
|
(new button% (label "Jump to") (parent extra-navigator)
|
||||||
(callback (lambda (b e) (jump-to)))))
|
(callback (lambda (b e) (jump-to)))))
|
||||||
|
@ -378,14 +378,13 @@
|
||||||
(refresh/move/cached-prefix))
|
(refresh/move/cached-prefix))
|
||||||
|
|
||||||
;; FIXME: selected stx must be in term1; doesn't work in term2
|
;; FIXME: selected stx must be in term1; doesn't work in term2
|
||||||
#;
|
|
||||||
(define/private (zoom)
|
(define/private (zoom)
|
||||||
(let* ([selected-syntax (send sbc get-selected-syntax)]
|
(let* ([selected-syntax (send sbc get-selected-syntax)]
|
||||||
[step (and steps (cursor:current steps))]
|
[step (and steps (cursor:current steps))]
|
||||||
[deriv (and step (protostep-deriv step))])
|
[deriv (and step (protostep-deriv step))])
|
||||||
(when (and selected-syntax deriv)
|
(when (and selected-syntax deriv)
|
||||||
(for-each go/deriv (seek/syntax selected-syntax deriv)))))
|
(for-each go/deriv (seek/syntax selected-syntax deriv)))))
|
||||||
#;
|
|
||||||
(define/public (jump-to)
|
(define/public (jump-to)
|
||||||
(let* ([selected-syntax (send sbc get-selected-syntax)]
|
(let* ([selected-syntax (send sbc get-selected-syntax)]
|
||||||
[step (and steps (cursor:current steps))]
|
[step (and steps (cursor:current steps))]
|
||||||
|
@ -400,7 +399,7 @@
|
||||||
[else
|
[else
|
||||||
(message-box "Macro stepper - Jump to"
|
(message-box "Macro stepper - Jump to"
|
||||||
"Subterm occurs non-linearly in the expansion")])))))
|
"Subterm occurs non-linearly in the expansion")])))))
|
||||||
#;
|
|
||||||
(define/private (jump-to/deriv subderiv)
|
(define/private (jump-to/deriv subderiv)
|
||||||
(define all-step-derivs
|
(define all-step-derivs
|
||||||
(let ([ht (make-hash-table)])
|
(let ([ht (make-hash-table)])
|
||||||
|
@ -408,6 +407,8 @@
|
||||||
(cursor-suffix->list steps))
|
(cursor-suffix->list steps))
|
||||||
ht))
|
ht))
|
||||||
(define target-deriv
|
(define target-deriv
|
||||||
|
subderiv
|
||||||
|
#;
|
||||||
(find-deriv
|
(find-deriv
|
||||||
(lambda (d) (hash-table-get all-step-derivs d (lambda () #f)))
|
(lambda (d) (hash-table-get all-step-derivs d (lambda () #f)))
|
||||||
(lambda (d) #f)
|
(lambda (d) #f)
|
||||||
|
@ -475,10 +476,10 @@
|
||||||
|
|
||||||
(define/private (update:show-lctx lctx)
|
(define/private (update:show-lctx lctx)
|
||||||
(when (pair? lctx)
|
(when (pair? lctx)
|
||||||
(for-each (lambda (bc)
|
(for-each (lambda (bf)
|
||||||
(send sbview add-text
|
(send sbview add-text
|
||||||
"While executing macro transformer in:\n")
|
"While executing macro transformer in:\n")
|
||||||
(insert-syntax/redex (cddr bc) (cadr bc)))
|
(insert-syntax/redex (bigframe-term bf) (bigframe-foci bf)))
|
||||||
lctx)
|
lctx)
|
||||||
(send sbview add-text "\n")))
|
(send sbview add-text "\n")))
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user