1#lang racket 2(require redex) 3 4(define-language lang 5 (e (binop e e) 6 (sqrt e) 7 number) 8 (binop + 9 - 10 * 11 /) 12 13 (e-ctxt (binop e e-ctxt) 14 (binop e-ctxt e) 15 (sqrt e-ctxt) 16 hole) 17 (v number)) 18 19(define reductions 20 (reduction-relation 21 lang 22 (c--> (+ number_1 number_2) 23 ,(+ (term number_1) (term number_2)) 24 "add") 25 (c--> (- number_1 number_2) 26 ,(- (term number_1) (term number_2)) 27 "subtract") 28 (c--> (* number_1 number_2) 29 ,(* (term number_1) (term number_2)) 30 "multiply") 31 (c--> (/ number_1 number_2) 32 ,(/ (term number_1) (term number_2)) 33 "divide") 34 (c--> (sqrt number_1) 35 ,(sqrt (term number_1)) 36 "sqrt") 37 with 38 [(--> (in-hole e-ctxt_1 a) (in-hole e-ctxt_1 b)) 39 (c--> a b)])) 40 41(define traces-file 42 (make-temporary-file "traces~a.ps")) 43 44(traces/ps reductions (term (- (* (sqrt 36) (/ 1 2)) (+ 1 2))) 45 traces-file) 46 47;; Check for the command line flag --no-print 48;; If it's set, don't print the temporary file name, 49;; This flag is so that DrDr can avoid seeing a change here. 50;; -- samth 51(define print-name? 52 (let ([print? #t]) 53 (command-line 54 #:once-each 55 ["--no-print" "omit printing of file name" (set! print? #f)]) 56 print?)) 57 58(when print-name? 59 (printf "Traces are in ~a\n" traces-file)) 60 61;; Test mode: no printing: 62(module test racket/base 63 (require syntax/location) 64 (parameterize ([current-command-line-arguments (vector "--no-print")]) 65 (dynamic-require (quote-module-path "..") #f))) 66