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