lifting now controlled by language.

svn: r4424
This commit is contained in:
John Clements 2006-09-23 11:19:32 +00:00
parent 885b2fa8d3
commit f1c6776715
3 changed files with 62 additions and 35 deletions

View File

@ -28,8 +28,7 @@
. opt->* .
(any/c)) ; procedure for runtime break
boolean? ; track-inferred-name?
any/c ; language-level
;;string? ; language-level-name : not a nice way to abstract.
(union any/c (symbols 'testing)); language-level
. -> .
syntax?)] ; results
#;[top-level-rewrite (-> syntax? syntax?)])
@ -1149,7 +1148,8 @@
; body of local
(let* ([annotated-exp (cond
[(string=? (language-level->name language-level) "ACL2 Beginner (beta 8)")
[(and (not (eq? language-level 'testing))
(string=? (language-level->name language-level) "ACL2 Beginner (beta 8)"))
(annotate/top-level/acl2 main-exp)]
[else
(annotate/top-level main-exp)])])

View File

@ -63,7 +63,7 @@
(step-result? . -> . void?) ; receive-result
(or/c render-settings? false/c) ; render-settings
boolean? ; track-inferred-names?
object? ;; FIXME: can do better: subclass of language% ; the language level
(or/c object? (symbols 'testing)) ;; FIXME: can do better: subclass of language% ; the language level
(procedure? . -> . void?) ; run-on-drscheme-side
. -> .
void?)])
@ -299,7 +299,7 @@
[else (error 'break "unknown label on break")]))))))
(define maybe-lift
(if (send language-level stepper:enable-let-lifting?)
(if (render-settings-lifting? render-settings)
lift
;; ... oh dear; model.ss should disable the double-break & late-let break when lifting is off.
(lambda (stx dont-care) (list stx))))
@ -323,7 +323,7 @@
(lambda ()
;; swap these to allow errors to escape (e.g., when debugging)
(error-display-handler err-display-handler)
;; (void)
;;(void)
)
(lambda (expanded continue-thunk) ; iter
(r:reset-special-values)

View File

@ -90,13 +90,6 @@
finished-xml-box-table
language-level->name)
;; eli's debug operator:
;; (I'm sure his version is more elegant.)
(define (>>> x . extra)
(begin (fprintf (current-error-port) "~a >>> ~v\n"
(if extra (apply string-append extra) "")
x)
x))
; A step-result is either:
; (make-before-after-result finished-exps exp redex reduct)
@ -375,26 +368,60 @@
; functional update package
;; a trace is one of
;; (cons 'car trace)
;; (cons 'cdr trace)
;; (cons 'syntax-e trace)
;; (cons 'both (list trace trace))
;; null
(define (swap-args 2-arg-fun)
(lambda (x y)
(2-arg-fun y x)))
(define second-arg (lambda (dc y) y))
(define up-mappings
`((rebuild ((,car ,(lambda (stx new) (cons new (cdr stx))))
(,cdr ,(lambda (stx new) (cons (car stx) new)))
(,syntax-e ,(swap-args rebuild-stx))))
(discard ((,car ,second-arg)
(,cdr ,second-arg)
(,syntax-e ,second-arg)))))
(define (up-mapping traversal fn)
(case traversal
[(rebuild) (case fn
[(car) (lambda (stx new) (cons new (cdr stx)))]
[(cdr) (lambda (stx new) (cons (car stx) new))]
[(syntax-e) (swap-args rebuild-stx)]
[(both-l both-r) (lambda (stx a b) (cons a b))]
[else (error 'up-mapping "unexpected symbol in up-mapping (1)")])]
[(discard) (case fn
[(car) second-arg]
[(cdr) second-arg]
[(syntax-e) second-arg]
[(both-l) (lambda (stx a b) a)]
[(both-r) (lambda (stx a b) b)]
[else (error 'up-mapping "unexpected symbol in up-mapping (2)")])]))
(define (down-mapping fn)
(case fn
[(car) car]
[(cdr) cdr]
[(syntax-e) syntax-e]
[else (error 'down-mapping "called on something other than 'car, 'cdr, & 'syntax-e: ~v" fn)]))
(define (update fn-list val fn traversal)
(if (null? fn-list)
(fn val)
(let* ([down (car fn-list)]
[up (cadr (assq down (cadr (assq traversal up-mappings))))])
(up val (update (cdr fn-list) (down val) fn traversal)))))
(let ([up (up-mapping traversal (car fn-list))])
(case (car fn-list)
[(both-l both-r) (up val
(update (cadr fn-list) (car val) fn traversal)
(update (caddr fn-list) (cdr val) fn traversal))]
[else (let ([down (down-mapping (car fn-list))])
(up val (update (cdr fn-list) (down val) fn traversal)))]))))
#;(display (equal? (update '(cdr cdr car both-l (car) (cdr))
`(a . (b ((1) c . 2) d))
(lambda (x) (+ x 1))
'rebuild)
`(a . (b ((2) c . 3) d))))
;; skipto/auto : syntax-object?
;; (symbols 'rebuild 'discard)
@ -411,16 +438,16 @@
[else (transformer stx)]))
; small test case:
;(equal? (syntax-object->datum
; (skipto/auto (syntax-property #`(a #,(syntax-property #`(b c)
; 'stepper-skipto
; (list syntax-e cdr car)))
; 'stepper-skipto
; (list syntax-e cdr car))
; 'discard
; (lambda (x) x)))
; 'c)
#;(display (equal? (syntax-object->datum
(skipto/auto (syntax-property #`(a #,(syntax-property #`(b c)
'stepper-skipto
'(syntax-e cdr car)))
'stepper-skipto
'(syntax-e cdr car))
'discard
(lambda (x) x)))
'c))
; BINDING-/VARREF-SET FUNCTIONS
@ -447,7 +474,7 @@
;; (profiling-table-incr 2 1)
;;
;; (equal? (get-set-pair-union-stats)
;; `(((2 . 3) 1) ((2 . 1) 2) ((1 . 2) 2)))
; `(((2 . 3) 1) ((2 . 1) 2) ((1 . 2) 2)))
;; until this remove* goes into list.ss?