macro debugger:
underline definite binders add rename/shift mapping so module final term retains binding info svn: r12843
This commit is contained in:
parent
340b193571
commit
6fdba44edc
|
@ -2,12 +2,14 @@
|
||||||
#lang scheme/base
|
#lang scheme/base
|
||||||
(require scheme/match
|
(require scheme/match
|
||||||
scheme/list
|
scheme/list
|
||||||
|
syntax/stx
|
||||||
"deriv-c.ss"
|
"deriv-c.ss"
|
||||||
"deriv-util.ss")
|
"deriv-util.ss")
|
||||||
(provide find-derivs
|
(provide find-derivs
|
||||||
find-deriv
|
find-deriv
|
||||||
find-derivs/syntax
|
find-derivs/syntax
|
||||||
extract-all-fresh-names
|
extract-all-fresh-names
|
||||||
|
compute-shift-table
|
||||||
flatten-identifiers)
|
flatten-identifiers)
|
||||||
|
|
||||||
;; Utilities for finding subderivations
|
;; Utilities for finding subderivations
|
||||||
|
@ -126,8 +128,12 @@
|
||||||
(lambda _ #f)
|
(lambda _ #f)
|
||||||
d))
|
d))
|
||||||
|
|
||||||
;; extract-all-fresh-names : Derivation -> syntaxlike
|
;; extract-all-fresh-names : Derivation -> (listof identifier)
|
||||||
(define (extract-all-fresh-names d)
|
(define (extract-all-fresh-names d)
|
||||||
|
(define ht (make-hasheq))
|
||||||
|
(define (add stxish)
|
||||||
|
(for-each (lambda (id) (hash-set! ht id #t))
|
||||||
|
(flatten-identifiers stxish)))
|
||||||
(define (renaming-node? x)
|
(define (renaming-node? x)
|
||||||
(or (p:lambda? x)
|
(or (p:lambda? x)
|
||||||
;;(p:case-lambda? x)
|
;;(p:case-lambda? x)
|
||||||
|
@ -142,69 +148,83 @@
|
||||||
(define (extract-fresh-names d)
|
(define (extract-fresh-names d)
|
||||||
(match d
|
(match d
|
||||||
[(Wrap p:lambda (e1 e2 rs ?1 renames body))
|
[(Wrap p:lambda (e1 e2 rs ?1 renames body))
|
||||||
(if renames
|
(when renames
|
||||||
(with-syntax ([(?formals . ?body) renames])
|
(with-syntax ([(?formals . ?body) renames])
|
||||||
#'?formals)
|
(add #'?formals)))]
|
||||||
null)]
|
|
||||||
[(Wrap clc (_ renames _))
|
[(Wrap clc (_ renames _))
|
||||||
(if renames
|
(when renames
|
||||||
(with-syntax ([(?formals . ?body) renames])
|
(with-syntax ([(?formals . ?body) renames])
|
||||||
#'?formals)
|
(add #'?formals)))]
|
||||||
null)]
|
|
||||||
[(Wrap p:let-values (e1 e2 rs ?1 renames rhss body))
|
[(Wrap p:let-values (e1 e2 rs ?1 renames rhss body))
|
||||||
(if renames
|
(when renames
|
||||||
(with-syntax ([(((?vars ?rhs) ...) . ?body) renames])
|
(with-syntax ([(((?vars ?rhs) ...) . ?body) renames])
|
||||||
#'(?vars ...))
|
(add #'(?vars ...))))]
|
||||||
null)]
|
|
||||||
[(Wrap p:letrec-values (e1 e2 rs ?1 renames rhss body))
|
[(Wrap p:letrec-values (e1 e2 rs ?1 renames rhss body))
|
||||||
(if renames
|
(when renames
|
||||||
(with-syntax ([(((?vars ?rhs) ...) . ?body) renames])
|
(with-syntax ([(((?vars ?rhs) ...) . ?body) renames])
|
||||||
#'(?vars ...))
|
(add #'(?vars ...))))]
|
||||||
null)]
|
[(Wrap p:letrec-syntaxes+values (e1 e2 rs ?1 srenames srhss vrenames _ _ _))
|
||||||
[(Wrap p:letrec-syntaxes+values (e1 e2 rs ?1 srenames srhss vrenames vrhss body _))
|
(when srenames
|
||||||
(cons
|
|
||||||
(if srenames
|
|
||||||
(with-syntax ([(((?svars ?srhs) ...) ((?vvars ?vrhs) ...) . ?body)
|
(with-syntax ([(((?svars ?srhs) ...) ((?vvars ?vrhs) ...) . ?body)
|
||||||
srenames])
|
srenames])
|
||||||
#'(?svars ... ?vvars ...))
|
(add #'(?svars ... ?vvars ...))))
|
||||||
null)
|
(when vrenames
|
||||||
(if vrenames
|
|
||||||
(with-syntax ([(((?vvars ?vrhs) ...) . ?body) vrenames])
|
(with-syntax ([(((?vvars ?vrhs) ...) . ?body) vrenames])
|
||||||
#'(?vvars ...))
|
(add #'(?vvars ...))))]
|
||||||
null))]
|
|
||||||
[(Wrap b:defvals (rename head ?1 rename2 ?2))
|
[(Wrap b:defvals (rename head ?1 rename2 ?2))
|
||||||
(let ([head-e2 (wderiv-e2 head)])
|
(let ([head-e2 (wderiv-e2 head)])
|
||||||
(if head-e2
|
(when head-e2
|
||||||
(with-syntax ([(?dv ?vars ?rhs) head-e2])
|
(with-syntax ([(?dv ?vars ?rhs) head-e2])
|
||||||
#'?vars)
|
(add #'?vars))))]
|
||||||
null))]
|
|
||||||
[(Wrap b:defstx (rename head ?1 rename2 ?2 rhs))
|
[(Wrap b:defstx (rename head ?1 rename2 ?2 rhs))
|
||||||
(let ([head-e2 (wderiv-e2 head)])
|
(let ([head-e2 (wderiv-e2 head)])
|
||||||
(if head-e2
|
(when head-e2
|
||||||
(with-syntax ([(?ds ?svars ?rhs) head-e2])
|
(with-syntax ([(?ds ?svars ?rhs) head-e2])
|
||||||
#'?svars)
|
(add #'?svars))))]
|
||||||
null))]
|
|
||||||
[(Wrap p:define-values (e1 e2 rs ?1 rhs))
|
[(Wrap p:define-values (e1 e2 rs ?1 rhs))
|
||||||
(if rhs
|
(when rhs
|
||||||
(with-syntax ([(?dv ?vars ?rhs) e1])
|
(with-syntax ([(?dv ?vars ?rhs) e1])
|
||||||
#'?vars)
|
(add #'?vars)))]
|
||||||
null)]
|
|
||||||
[(Wrap p:define-syntaxes (e1 e2 rs ?1 rhs _))
|
[(Wrap p:define-syntaxes (e1 e2 rs ?1 rhs _))
|
||||||
(if rhs
|
(when rhs
|
||||||
(with-syntax ([(?ds ?svars ?srhs) e1])
|
(with-syntax ([(?ds ?svars ?srhs) e1])
|
||||||
#'?svars)
|
(add #'?svars)))]
|
||||||
null)]
|
[_ (void)]))
|
||||||
[_ null]))
|
(define renaming-forms
|
||||||
|
(find-deriv/unit+join+zero renaming-node?
|
||||||
(let ([all-renaming-forms
|
|
||||||
(find-deriv/unit+join+zero
|
|
||||||
renaming-node?
|
|
||||||
(lambda (d) #f)
|
(lambda (d) #f)
|
||||||
d
|
d
|
||||||
list
|
list
|
||||||
append
|
append
|
||||||
null)])
|
null))
|
||||||
(flatten-identifiers (map extract-fresh-names all-renaming-forms))))
|
(for ([rf renaming-forms])
|
||||||
|
(extract-fresh-names rf))
|
||||||
|
(hash-map ht (lambda (k v) k)))
|
||||||
|
|
||||||
|
;; compute-shift-table : deriv -> hash[id => (listof id)]
|
||||||
|
(define (compute-shift-table d)
|
||||||
|
(define ht (make-hasheq))
|
||||||
|
(define module-forms
|
||||||
|
(find-derivs p:module? (lambda _ #f) d))
|
||||||
|
(define module-shift-renamers
|
||||||
|
(for/list ([mf module-forms])
|
||||||
|
(let ([shift (p:module-shift mf)]
|
||||||
|
[body (p:module-body mf)])
|
||||||
|
(and shift body
|
||||||
|
(with-syntax ([(_module _name _lang shifted-body) shift])
|
||||||
|
(add-rename-mapping ht (wderiv-e2 body) #'shifted-body))))))
|
||||||
|
ht)
|
||||||
|
|
||||||
|
(define (add-rename-mapping ht from to)
|
||||||
|
(define (loop from to)
|
||||||
|
(cond [(and (stx-pair? from) (stx-pair? to))
|
||||||
|
(loop (stx-car from) (stx-car to))
|
||||||
|
(loop (stx-cdr from) (stx-cdr to))]
|
||||||
|
[(and (identifier? from) (identifier? to))
|
||||||
|
(hash-set! ht from (cons to (hash-ref ht from null)))]
|
||||||
|
[else (void)]))
|
||||||
|
(loop from to)
|
||||||
|
(void))
|
||||||
|
|
||||||
;; flatten-identifiers : syntaxlike -> (list-of identifier)
|
;; flatten-identifiers : syntaxlike -> (list-of identifier)
|
||||||
(define (flatten-identifiers stx)
|
(define (flatten-identifiers stx)
|
||||||
|
|
|
@ -79,18 +79,28 @@
|
||||||
;; highlight-syntaxes : (list-of syntax) string -> void
|
;; highlight-syntaxes : (list-of syntax) string -> void
|
||||||
(define/public (highlight-syntaxes stxs hi-color)
|
(define/public (highlight-syntaxes stxs hi-color)
|
||||||
(let ([style-delta (highlight-style-delta hi-color #f)])
|
(let ([style-delta (highlight-style-delta hi-color #f)])
|
||||||
(for-each (lambda (stx) (hash-set! extra-styles stx style-delta))
|
(for ([stx stxs])
|
||||||
stxs))
|
(add-extra-styles stx (list style-delta))))
|
||||||
(refresh))
|
(refresh))
|
||||||
|
|
||||||
|
;; underline-syntaxes : (listof syntax) -> void
|
||||||
|
(define/public (underline-syntaxes stxs)
|
||||||
|
(for ([stx stxs])
|
||||||
|
(add-extra-styles stx (list underline-style-delta)))
|
||||||
|
(refresh))
|
||||||
|
|
||||||
|
(define/public (add-extra-styles stx styles)
|
||||||
|
(hash-set! extra-styles stx
|
||||||
|
(append (hash-ref extra-styles stx null)
|
||||||
|
styles)))
|
||||||
|
|
||||||
;; apply-extra-styles : -> void
|
;; apply-extra-styles : -> void
|
||||||
;; Applies externally-added styles (such as highlighting)
|
;; Applies externally-added styles (such as highlighting)
|
||||||
(define/private (apply-extra-styles)
|
(define/private (apply-extra-styles)
|
||||||
(hash-for-each
|
(for ([(stx style-deltas) extra-styles])
|
||||||
extra-styles
|
(for ([r (send range get-ranges stx)])
|
||||||
(lambda (hi-stx style-delta)
|
(for ([style-delta style-deltas])
|
||||||
(let ([rs (send range get-ranges hi-stx)])
|
(restyle-range r style-delta)))))
|
||||||
(for-each (lambda (r) (restyle-range r style-delta)) rs)))))
|
|
||||||
|
|
||||||
;; apply-secondary-partition-styles : selected-syntax -> void
|
;; apply-secondary-partition-styles : selected-syntax -> void
|
||||||
;; If the selected syntax is an identifier, then styles all identifiers
|
;; If the selected syntax is an identifier, then styles all identifiers
|
||||||
|
@ -243,6 +253,11 @@
|
||||||
(send sd set-weight-off 'bold))
|
(send sd set-weight-off 'bold))
|
||||||
sd))
|
sd))
|
||||||
|
|
||||||
|
(define underline-style-delta
|
||||||
|
(let ([sd (new style-delta%)])
|
||||||
|
(send sd set-underlined-on #t)
|
||||||
|
sd))
|
||||||
|
|
||||||
(define selection-color "yellow")
|
(define selection-color "yellow")
|
||||||
(define subselection-color "yellow")
|
(define subselection-color "yellow")
|
||||||
|
|
||||||
|
|
|
@ -105,61 +105,72 @@
|
||||||
(send -text change-style clickback-style a b)))))
|
(send -text change-style clickback-style a b)))))
|
||||||
|
|
||||||
(define/public (add-syntax stx
|
(define/public (add-syntax stx
|
||||||
#:alpha-table alpha-table
|
#:binder-table [alpha-table #f]
|
||||||
|
#:shift-table [shift-table #f]
|
||||||
#:definites [definites null]
|
#:definites [definites null]
|
||||||
#:hi-colors [hi-colors null]
|
#:hi-colors [hi-colors null]
|
||||||
#:hi-stxss [hi-stxss null])
|
#:hi-stxss [hi-stxss null])
|
||||||
(define (get-binder id)
|
(define (get-binders id)
|
||||||
|
(define binder
|
||||||
(module-identifier-mapping-get alpha-table id (lambda () #f)))
|
(module-identifier-mapping-get alpha-table id (lambda () #f)))
|
||||||
|
(if shift-table
|
||||||
|
(cons binder (hash-ref shift-table binder null))
|
||||||
|
(list binder)))
|
||||||
(let ([display (internal-add-syntax stx)]
|
(let ([display (internal-add-syntax stx)]
|
||||||
[definite-table (make-hasheq)])
|
[definite-table (make-hasheq)])
|
||||||
(for-each (lambda (hi-stxs hi-color)
|
(for-each (lambda (hi-stxs hi-color)
|
||||||
(send display highlight-syntaxes hi-stxs hi-color))
|
(send display highlight-syntaxes hi-stxs hi-color))
|
||||||
hi-stxss
|
hi-stxss
|
||||||
hi-colors)
|
hi-colors)
|
||||||
(for-each (lambda (x) (hash-set! definite-table x #t)) definites)
|
(for ([definite definites])
|
||||||
|
(hash-set! definite-table definite #t)
|
||||||
|
(when shift-table
|
||||||
|
(for ([shifted-definite (hash-ref shift-table definite null)])
|
||||||
|
(hash-set! definite-table shifted-definite #t))))
|
||||||
(when alpha-table
|
(when alpha-table
|
||||||
(let ([range (send display get-range)]
|
(let ([range (send display get-range)]
|
||||||
[start (send display get-start-position)])
|
[start (send display get-start-position)])
|
||||||
(define (adjust n) (+ start n))
|
(let* ([binders0
|
||||||
(for-each
|
(module-identifier-mapping-map alpha-table (lambda (k v) k))]
|
||||||
(lambda (id)
|
[binders
|
||||||
|
(apply append (map get-binders binders0))])
|
||||||
|
(send display underline-syntaxes binders))
|
||||||
|
(for ([id (send range get-identifier-list)])
|
||||||
|
(define definite? (hash-ref definite-table id #f))
|
||||||
(when #f ;; DISABLED
|
(when #f ;; DISABLED
|
||||||
(match (identifier-binding id)
|
(add-binding-billboard start range id definite?))
|
||||||
[(list src-mod src-name nom-mod nom-name _)
|
(for ([binder (get-binders id)])
|
||||||
(for-each (lambda (id-r)
|
(for ([binder-r (send range get-ranges binder)])
|
||||||
(send -text add-billboard
|
(for ([id-r (send range get-ranges id)])
|
||||||
(adjust (car id-r))
|
(add-binding-arrow start binder-r id-r definite?)))))))
|
||||||
(adjust (cdr id-r))
|
display))
|
||||||
(string-append "from "
|
|
||||||
(mpi->string src-mod))
|
(define/private (add-binding-arrow start binder-r id-r definite?)
|
||||||
(if (hash-ref definite-table id #f)
|
(if definite?
|
||||||
"blue"
|
|
||||||
"purple")))
|
|
||||||
(send range get-ranges id))]
|
|
||||||
[_ (void)]))
|
|
||||||
(let ([binder (get-binder id)])
|
|
||||||
(when binder
|
|
||||||
(for-each
|
|
||||||
(lambda (binder-r)
|
|
||||||
(for-each (lambda (id-r)
|
|
||||||
(if (hash-ref definite-table id #f)
|
|
||||||
(send -text add-arrow
|
(send -text add-arrow
|
||||||
(adjust (car binder-r))
|
(+ start (car binder-r))
|
||||||
(adjust (cdr binder-r))
|
(+ start (cdr binder-r))
|
||||||
(adjust (car id-r))
|
(+ start (car id-r))
|
||||||
(adjust (cdr id-r))
|
(+ start (cdr id-r))
|
||||||
"blue")
|
"blue")
|
||||||
(send -text add-question-arrow
|
(send -text add-question-arrow
|
||||||
(adjust (car binder-r))
|
(+ start (car binder-r))
|
||||||
(adjust (cdr binder-r))
|
(+ start (cdr binder-r))
|
||||||
(adjust (car id-r))
|
(+ start (car id-r))
|
||||||
(adjust (cdr id-r))
|
(+ start (cdr id-r))
|
||||||
"purple")))
|
"purple")))
|
||||||
(send range get-ranges id)))
|
|
||||||
(send range get-ranges binder)))))
|
(define/private (add-binding-billboard start range id definite?)
|
||||||
(send range get-identifier-list))))
|
(match (identifier-binding id)
|
||||||
display))
|
[(list-rest src-mod src-name nom-mod nom-name _)
|
||||||
|
(for-each (lambda (id-r)
|
||||||
|
(send -text add-billboard
|
||||||
|
(+ start (car id-r))
|
||||||
|
(+ start (cdr id-r))
|
||||||
|
(string-append "from " (mpi->string src-mod))
|
||||||
|
(if definite? "blue" "purple")))
|
||||||
|
(send range get-ranges id))]
|
||||||
|
[_ (void)]))
|
||||||
|
|
||||||
(define/public (add-separator)
|
(define/public (add-separator)
|
||||||
(with-unlock -text
|
(with-unlock -text
|
||||||
|
|
|
@ -95,36 +95,41 @@
|
||||||
(send sbview add-text "\n"))
|
(send sbview add-text "\n"))
|
||||||
|
|
||||||
(define/public (add-step step
|
(define/public (add-step step
|
||||||
#:binders binders)
|
#:binders binders
|
||||||
|
#:shift-table [shift-table #f])
|
||||||
(cond [(step? step)
|
(cond [(step? step)
|
||||||
(show-step step binders)]
|
(show-step step binders shift-table)]
|
||||||
[(misstep? step)
|
[(misstep? step)
|
||||||
(show-misstep step binders)]
|
(show-misstep step binders shift-table)]
|
||||||
[(prestep? step)
|
[(prestep? step)
|
||||||
(show-prestep step binders)]
|
(show-prestep step binders shift-table)]
|
||||||
[(poststep? step)
|
[(poststep? step)
|
||||||
(show-poststep step binders)]))
|
(show-poststep step binders shift-table)]))
|
||||||
|
|
||||||
(define/public (add-syntax stx
|
(define/public (add-syntax stx
|
||||||
#:binders binders
|
#:binders binders
|
||||||
|
#:shift-table [shift-table #f]
|
||||||
#:definites definites)
|
#:definites definites)
|
||||||
(send sbview add-syntax stx
|
(send sbview add-syntax stx
|
||||||
#:alpha-table binders
|
#:binder-table binders
|
||||||
|
#:shift-table shift-table
|
||||||
#:definites (or definites null)))
|
#:definites (or definites null)))
|
||||||
|
|
||||||
(define/public (add-final stx error
|
(define/public (add-final stx error
|
||||||
#:binders binders
|
#:binders binders
|
||||||
|
#:shift-table [shift-table #f]
|
||||||
#:definites definites)
|
#:definites definites)
|
||||||
(when stx
|
(when stx
|
||||||
(send sbview add-text "Expansion finished\n")
|
(send sbview add-text "Expansion finished\n")
|
||||||
(send sbview add-syntax stx
|
(send sbview add-syntax stx
|
||||||
#:alpha-table binders
|
#:binder-table binders
|
||||||
|
#:shift-table shift-table
|
||||||
#:definites (or definites null)))
|
#:definites (or definites null)))
|
||||||
(when error
|
(when error
|
||||||
(add-error error)))
|
(add-error error)))
|
||||||
|
|
||||||
;; show-lctx : Step -> void
|
;; show-lctx : Step -> void
|
||||||
(define/private (show-lctx step binders)
|
(define/private (show-lctx step binders shift-table)
|
||||||
(define state (protostep-s1 step))
|
(define state (protostep-s1 step))
|
||||||
(define lctx (state-lctx state))
|
(define lctx (state-lctx state))
|
||||||
(when (pair? lctx)
|
(when (pair? lctx)
|
||||||
|
@ -135,6 +140,7 @@
|
||||||
(insert-syntax/redex (bigframe-term bf)
|
(insert-syntax/redex (bigframe-term bf)
|
||||||
(bigframe-foci bf)
|
(bigframe-foci bf)
|
||||||
binders
|
binders
|
||||||
|
shift-table
|
||||||
(state-uses state)
|
(state-uses state)
|
||||||
(state-frontier state)))
|
(state-frontier state)))
|
||||||
(reverse lctx))))
|
(reverse lctx))))
|
||||||
|
@ -149,72 +155,81 @@
|
||||||
(step-type->string (protostep-type step))))
|
(step-type->string (protostep-type step))))
|
||||||
|
|
||||||
;; show-step : Step -> void
|
;; show-step : Step -> void
|
||||||
(define/private (show-step step binders)
|
(define/private (show-step step binders shift-table)
|
||||||
(show-state/redex (protostep-s1 step) binders)
|
(show-state/redex (protostep-s1 step) binders shift-table)
|
||||||
(separator step)
|
(separator step)
|
||||||
(show-state/contractum (step-s2 step) binders)
|
(show-state/contractum (step-s2 step) binders shift-table)
|
||||||
(show-lctx step binders))
|
(show-lctx step binders shift-table))
|
||||||
|
|
||||||
(define/private (show-state/redex state binders)
|
(define/private (show-state/redex state binders shift-table)
|
||||||
(insert-syntax/redex (state-term state)
|
(insert-syntax/redex (state-term state)
|
||||||
(state-foci state)
|
(state-foci state)
|
||||||
binders
|
binders
|
||||||
|
shift-table
|
||||||
(state-uses state)
|
(state-uses state)
|
||||||
(state-frontier state)))
|
(state-frontier state)))
|
||||||
|
|
||||||
(define/private (show-state/contractum state binders)
|
(define/private (show-state/contractum state binders shift-table)
|
||||||
(insert-syntax/contractum (state-term state)
|
(insert-syntax/contractum (state-term state)
|
||||||
(state-foci state)
|
(state-foci state)
|
||||||
binders
|
binders
|
||||||
|
shift-table
|
||||||
(state-uses state)
|
(state-uses state)
|
||||||
(state-frontier state)))
|
(state-frontier state)))
|
||||||
|
|
||||||
;; show-prestep : Step -> void
|
;; show-prestep : Step -> void
|
||||||
(define/private (show-prestep step binders)
|
(define/private (show-prestep step binders shift-table)
|
||||||
(separator/small step)
|
(separator/small step)
|
||||||
(show-state/redex (protostep-s1 step) binders)
|
(show-state/redex (protostep-s1 step) binders shift-table)
|
||||||
(show-lctx step binders))
|
(show-lctx step binders shift-table))
|
||||||
|
|
||||||
;; show-poststep : Step -> void
|
;; show-poststep : Step -> void
|
||||||
(define/private (show-poststep step binders)
|
(define/private (show-poststep step binders shift-table)
|
||||||
(separator/small step)
|
(separator/small step)
|
||||||
(show-state/contractum (protostep-s1 step) binders)
|
(show-state/contractum (protostep-s1 step) binders shift-table)
|
||||||
(show-lctx step binders))
|
(show-lctx step binders shift-table))
|
||||||
|
|
||||||
;; show-misstep : Step -> void
|
;; show-misstep : Step -> void
|
||||||
(define/private (show-misstep step binders)
|
(define/private (show-misstep step binders shift-table)
|
||||||
(define state (protostep-s1 step))
|
(define state (protostep-s1 step))
|
||||||
(show-state/redex state binders)
|
(show-state/redex state binders shift-table)
|
||||||
(separator step)
|
(separator step)
|
||||||
(send sbview add-error-text (exn-message (misstep-exn step)))
|
(send sbview add-error-text (exn-message (misstep-exn step)))
|
||||||
(send sbview add-text "\n")
|
(send sbview add-text "\n")
|
||||||
(when (exn:fail:syntax? (misstep-exn step))
|
(when (exn:fail:syntax? (misstep-exn step))
|
||||||
(for-each (lambda (e)
|
(for-each (lambda (e)
|
||||||
(send sbview add-syntax e
|
(send sbview add-syntax e
|
||||||
#:alpha-table binders
|
#:binder-table binders
|
||||||
|
#:shift-table shift-table
|
||||||
#:definites (or (state-uses state) null)))
|
#:definites (or (state-uses state) null)))
|
||||||
(exn:fail:syntax-exprs (misstep-exn step))))
|
(exn:fail:syntax-exprs (misstep-exn step))))
|
||||||
(show-lctx step binders))
|
(show-lctx step binders shift-table))
|
||||||
|
|
||||||
;; insert-syntax/color : syntax syntaxes identifiers syntaxes string -> void
|
;; insert-syntax/color
|
||||||
(define/private (insert-syntax/color stx foci binders definites frontier hi-color)
|
(define/private (insert-syntax/color stx foci binders shift-table
|
||||||
|
definites frontier hi-color)
|
||||||
(define highlight-foci? (send config get-highlight-foci?))
|
(define highlight-foci? (send config get-highlight-foci?))
|
||||||
(define highlight-frontier? (send config get-highlight-frontier?))
|
(define highlight-frontier? (send config get-highlight-frontier?))
|
||||||
(send sbview add-syntax stx
|
(send sbview add-syntax stx
|
||||||
#:definites (or definites null)
|
#:definites (or definites null)
|
||||||
#:alpha-table binders
|
#:binder-table binders
|
||||||
|
#:shift-table shift-table
|
||||||
#:hi-colors (list hi-color
|
#:hi-colors (list hi-color
|
||||||
"WhiteSmoke")
|
"WhiteSmoke")
|
||||||
#:hi-stxss (list (if highlight-foci? foci null)
|
#:hi-stxss (list (if highlight-foci? foci null)
|
||||||
(if highlight-frontier? frontier null))))
|
(if highlight-frontier? frontier null))))
|
||||||
|
|
||||||
;; insert-syntax/redex : syntax syntaxes identifiers syntaxes -> void
|
;; insert-syntax/redex
|
||||||
(define/private (insert-syntax/redex stx foci binders definites frontier)
|
(define/private (insert-syntax/redex stx foci binders shift-table
|
||||||
(insert-syntax/color stx foci binders definites frontier "MistyRose"))
|
definites frontier)
|
||||||
|
(insert-syntax/color stx foci binders shift-table
|
||||||
|
definites frontier "MistyRose"))
|
||||||
|
|
||||||
;; insert-syntax/contractum : syntax syntaxes identifiers syntaxes -> void
|
;; insert-syntax/contractum
|
||||||
(define/private (insert-syntax/contractum stx foci binders definites frontier)
|
(define/private (insert-syntax/contractum stx foci binders shift-table
|
||||||
(insert-syntax/color stx foci binders definites frontier "LightCyan"))
|
definites frontier)
|
||||||
|
(insert-syntax/color stx foci binders shift-table
|
||||||
|
definites frontier "LightCyan"))
|
||||||
|
|
||||||
;; insert-step-separator : string -> void
|
;; insert-step-separator : string -> void
|
||||||
(define/private (insert-step-separator text)
|
(define/private (insert-step-separator text)
|
||||||
|
|
|
@ -46,6 +46,7 @@
|
||||||
(define deriv #f)
|
(define deriv #f)
|
||||||
(define deriv-hidden? #f)
|
(define deriv-hidden? #f)
|
||||||
(define binders #f)
|
(define binders #f)
|
||||||
|
(define shift-table #f)
|
||||||
|
|
||||||
(define raw-steps #f)
|
(define raw-steps #f)
|
||||||
(define raw-steps-estx #f) ;; #f if raw-steps-exn is exn
|
(define raw-steps-estx #f) ;; #f if raw-steps-exn is exn
|
||||||
|
@ -72,7 +73,8 @@
|
||||||
(define-guarded-getters (recache-deriv!)
|
(define-guarded-getters (recache-deriv!)
|
||||||
[get-deriv deriv]
|
[get-deriv deriv]
|
||||||
[get-deriv-hidden? deriv-hidden?]
|
[get-deriv-hidden? deriv-hidden?]
|
||||||
[get-binders binders])
|
[get-binders binders]
|
||||||
|
[get-shift-table shift-table])
|
||||||
(define-guarded-getters (recache-raw-steps!)
|
(define-guarded-getters (recache-raw-steps!)
|
||||||
[get-raw-steps-definites raw-steps-definites]
|
[get-raw-steps-definites raw-steps-definites]
|
||||||
[get-raw-steps-exn raw-steps-exn]
|
[get-raw-steps-exn raw-steps-exn]
|
||||||
|
@ -104,7 +106,8 @@
|
||||||
(invalidate-synth!)
|
(invalidate-synth!)
|
||||||
(set! deriv #f)
|
(set! deriv #f)
|
||||||
(set! deriv-hidden? #f)
|
(set! deriv-hidden? #f)
|
||||||
(set! binders #f))
|
(set! binders #f)
|
||||||
|
(set! shift-table #f))
|
||||||
|
|
||||||
;; recache! : -> void
|
;; recache! : -> void
|
||||||
(define/public (recache!)
|
(define/public (recache!)
|
||||||
|
@ -130,12 +133,14 @@
|
||||||
(when (not d)
|
(when (not d)
|
||||||
(set! deriv-hidden? #t))
|
(set! deriv-hidden? #t))
|
||||||
(when d
|
(when d
|
||||||
(let ([alpha-table (make-module-identifier-mapping)])
|
(let ([alpha-table (make-module-identifier-mapping)]
|
||||||
|
[binder-ids (extract-all-fresh-names d)])
|
||||||
(for-each (lambda (id)
|
(for-each (lambda (id)
|
||||||
(module-identifier-mapping-put! alpha-table id id))
|
(module-identifier-mapping-put! alpha-table id id))
|
||||||
(extract-all-fresh-names d))
|
binder-ids)
|
||||||
(set! deriv d)
|
(set! deriv d)
|
||||||
(set! binders alpha-table))))))))
|
(set! binders alpha-table)
|
||||||
|
(set! shift-table (compute-shift-table d)))))))))
|
||||||
|
|
||||||
;; recache-synth! : -> void
|
;; recache-synth! : -> void
|
||||||
(define/private (recache-synth!)
|
(define/private (recache-synth!)
|
||||||
|
@ -277,6 +282,7 @@
|
||||||
(cond [(syntax? raw-steps-estx)
|
(cond [(syntax? raw-steps-estx)
|
||||||
(send displayer add-syntax raw-steps-estx
|
(send displayer add-syntax raw-steps-estx
|
||||||
#:binders binders
|
#:binders binders
|
||||||
|
#:shift-table shift-table
|
||||||
#:definites raw-steps-definites)]
|
#:definites raw-steps-definites)]
|
||||||
[(exn? raw-steps-exn)
|
[(exn? raw-steps-exn)
|
||||||
(send displayer add-error raw-steps-exn)]
|
(send displayer add-error raw-steps-exn)]
|
||||||
|
@ -289,9 +295,11 @@
|
||||||
(let ([step (cursor:next steps)])
|
(let ([step (cursor:next steps)])
|
||||||
(if step
|
(if step
|
||||||
(send displayer add-step step
|
(send displayer add-step step
|
||||||
#:binders binders)
|
#:binders binders
|
||||||
|
#:shift-table shift-table)
|
||||||
(send displayer add-final raw-steps-estx raw-steps-exn
|
(send displayer add-final raw-steps-estx raw-steps-exn
|
||||||
#:binders binders
|
#:binders binders
|
||||||
|
#:shift-table shift-table
|
||||||
#:definites raw-steps-definites)))]
|
#:definites raw-steps-definites)))]
|
||||||
[else (display-oops #t)]))
|
[else (display-oops #t)]))
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user