42 lines
899 B
Scheme
42 lines
899 B
Scheme
#lang scheme
|
|
(require redex)
|
|
|
|
(define-language lang
|
|
(e (binop e e)
|
|
(sqrt e)
|
|
number)
|
|
(binop +
|
|
-
|
|
*
|
|
/)
|
|
|
|
(e-ctxt (binop e e-ctxt)
|
|
(binop e-ctxt e)
|
|
(sqrt e-ctxt)
|
|
hole)
|
|
(v number))
|
|
|
|
(define reductions
|
|
(reduction-relation
|
|
lang
|
|
(c--> (+ number_1 number_2)
|
|
,(+ (term number_1) (term number_2))
|
|
"add")
|
|
(c--> (- number_1 number_2)
|
|
,(- (term number_1) (term number_2))
|
|
"subtract")
|
|
(c--> (* number_1 number_2)
|
|
,(* (term number_1) (term number_2))
|
|
"multiply")
|
|
(c--> (/ number_1 number_2)
|
|
,(/ (term number_1) (term number_2))
|
|
"divide")
|
|
(c-->(sqrt number_1)
|
|
,(sqrt (term number_1))
|
|
"sqrt")
|
|
with
|
|
[(--> (in-hole e-ctxt_1 a) (in-hole e-ctxt_1 b))
|
|
(c--> a b)]))
|
|
|
|
(traces reductions (term (- (* (sqrt 36) (/ 1 2)) (+ 1 2))))
|