suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

added preliminary acl2 support

Browse Source 
svn: r2414
This commit is contained in:
John Clements 2006-03-11 00:21:19 +00:00
parent 566bcba4d5
commit 289e076893
3 changed files with 277 additions and 248 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
collects/stepper/private/annotate.ss
View File

@ -27,6 +27,7 @@
(list?)
(any/c)) ; procedure for runtime break
boolean? ; track-inferred-name?
string? ; language-level-name : not a nice way to abstract.
syntax?)] ; results
#;[top-level-rewrite (-> syntax? syntax?)])
@ -106,7 +107,7 @@
[let-bound-bindings null]
[cond-test (lx #f)])
(if (or (syntax-property stx 'stepper-skip-completely)
(syntax-property stx '.stepper-define-struct-hint))
(syntax-property stx 'stepper-define-struct-hint))
stx
(let* ([recur-regular
(lambda (stx)
@ -258,7 +259,7 @@
; c) a boolean indicating whether to store inferred names.
;
(define (annotate main-exp break track-inferred-names?)
(define (annotate main-exp break track-inferred-names? language-level-name)
#;(define _ (fprintf (current-error-port) "input to annotate: ~v\n" (syntax-object->datum main-exp)))
(define binding-indexer
@ -1059,7 +1060,25 @@
(lambda () . rest2)
(lambda () . rest3)))
exp]
[else (error `annotate/top-level "unexpected top-level expression: ~a\n" (syntax-object->datum exp))])))
[else (begin
(fprintf (current-error-port) "~v\n" (syntax-object->datum exp))
(error `annotate/top-level "unexpected top-level expression: ~a\n" (syntax-object->datum exp)))])))
(define/contract annotate/top-level/acl2
(syntax? . -> . syntax?)
(lambda (exp)
(syntax-case exp (begin define-values #%app)
[(begin contract-thingy
(begin body (begin)))
#`(begin contract-thingy (begin #,(annotate/module-top-level #`body) (begin)))]
[else (annotate/module-top-level exp)]
#;[else (begin
(fprintf (current-error-port) "~v\n" (syntax-object->datum exp))
(error `annotate/top-level "unexpected top-level expression: ~a\n" (syntax-object->datum exp)))])))
(define/contract annotate/module-top-level
(syntax? . -> . syntax?)
@ -1111,6 +1130,10 @@
; body of local
#;(printf "input: ~a\n" exp)
(let* ([annotated-exp (annotate/top-level main-exp)])
(let* ([annotated-exp (cond
[(string=? language-level-name "ACL2 Beginner (beta 8)")
(annotate/top-level/acl2 main-exp)]
[else
(annotate/top-level main-exp)])])
#;(printf "annotated: \n~a\n" (syntax-object->datum annotated-exp))
annotated-exp)))

13
collects/stepper/private/model.ss
View File

@ -56,16 +56,17 @@
(step-result? . -> . void?) ; receive-result
(or/c render-settings? false/c) ; render-settings
boolean? ; track-inferred-names?
string? ; language-level-name
. -> .
void?)])
; go starts a stepper instance
; see provide stmt for contract
(define (go program-expander receive-result render-settings track-inferred-names?)
(define (go program-expander receive-result render-settings track-inferred-names? language-level-name)
(local
(;; finished-exps: (listof (list/c syntax-object? (or/c number? false?)( -> any)))
;; finished-exps: (listof (list/c syntax-object? (or/c number? false?)( -> any)))
;; because of mutation, these cannot be fixed renderings, but must be re-rendered at each step.
(define finished-exps null)
(define/contract add-to-finished
@ -278,7 +279,7 @@
(define (step-through-expression expanded expand-next-expression)
(let* ([annotated (a:annotate expanded break track-inferred-names?)])
(let* ([annotated (a:annotate expanded break track-inferred-names? language-level-name)])
(eval-syntax annotated)
(expand-next-expression)))
@ -288,7 +289,7 @@
(receive-result (make-before-error-result (append held-finished-list held-exp-list)
message))
(set! held-exp-list no-sexp))
(receive-result (make-error-result message)))))
(receive-result (make-error-result message))))
(program-expander
(lambda ()
@ -300,7 +301,7 @@
(if (eof-object? expanded)
(begin
(receive-result (make-finished-stepping)))
(step-through-expression expanded continue-thunk))))))
(step-through-expression expanded continue-thunk)))))
(define (first-of-one x)

11
collects/stepper/stepper-tool.ss
View File

@ -147,6 +147,7 @@
(define language-level-name
(car (last-pair (send language get-language-position))))
;; VALUE CONVERSION CODE:
(define simple-settings
@ -190,12 +191,15 @@
;; render-to-sexp : TST -> sexp
(define (render-to-sexp val)
(parameterize ([current-print-convert-hook (make-print-convert-hook simple-settings)])
(cond
[(string=? language-level-name "ACL2 Beginner (beta 8)")
(simple-module-based-language-convert-value val simple-settings)]
[else (parameterize ([current-print-convert-hook (make-print-convert-hook simple-settings)])
(set-print-settings
language
simple-settings
(lambda ()
(simple-module-based-language-convert-value val simple-settings)))))
(simple-module-based-language-convert-value val simple-settings))))]))
(define (>>> x)
(fprintf (current-error-port) ">>> ~v\n" x)
@ -433,7 +437,8 @@
(model:go program-expander-prime receive-result (get-render-settings render-to-string render-to-sexp #t)
(not (member language-level-name
(list (string-constant intermediate-student/lambda)
(string-constant advanced-student)))))
(string-constant advanced-student))))
language-level-name)
(send s-frame show #t)
s-frame)