Macro stepper:
cleaned up representation of big (localaction) contexts unitized hiding impl added (broken/experimental) navigation tools (jump, zoom) svn: r5468 original commit: ef1f77c33fc8082c80b6beea80f6f149ac7f8031
This commit is contained in:
parent
df346e3044
commit
ee080b92eb
|
@ -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
|
||||||
|
|
Loading…
Reference in New Issue
Block a user