calc.rkt

#lang racket
(require redex)

(define-language calc
  (e ::= n (e + e) (e - e) (e * e) (e / e) (- e))
  (n ::= number))

(define-metafunction calc
  ⊢ : e -> n
  [(⊢ n)                 n]
  [(⊢ (- e_1))           n_2
                         (where n_1 (⊢ e_1))
                         (where n_2 ,(- (term n_1)))]
  [(⊢ (e_1 + e_2))       n_3
                         (where n_1 (⊢ e_1))
                         (where n_2 (⊢ e_2))
                         (where n_3 ,(+ (term n_1) (term n_2)))]
  [(⊢ (e_1 - e_2))       n_3
                         (where n_1 (⊢ e_1))
                         (where n_2 (⊢ e_2))
                         (where n_3 ,(- (term n_1) (term n_2)))]
  [(⊢ (e_1 * e_2))       n_3
                         (where n_1 (⊢ e_1))
                         (where n_2 (⊢ e_2))
                         (where n_3 ,(* (term n_1) (term n_2)))]
  [(⊢ (e_1 / e_2))       n_3
                         (where n_1 (⊢ e_1))
                         (where n_2 (⊢ e_2))
                         (where n_3 ,(/ (term n_1) (term n_2)))]
  )

(test-equal (term (⊢ ((1 + 2) + (3 + 4))))
            (term 10))
(test-equal (term (⊢ ((1 + 2) * (3 + 4))))
            (term 21))

(test-equal (term (⊢ (- ((1 + 2) * (3 + 4)))))
            (term -21))

(test-results)

calc2.rkt

#lang racket
(require redex)

(define-language calc2
  (e ::= t (e * e) (e / e))
  (t ::= f (t + t) (t - t))
  (f ::= n (- e) (e))
  (n ::= number))

(define-metafunction calc2
  ⊢ : e -> n
  [(⊢ n)                 n]
  [(⊢ (- e_1))           n_2
                         (where n_1 (⊢ e_1))
                         (where n_2 ,(- (term n_1)))]
  [(⊢ (e_1 + e_2))       n_3
                         (where n_1 (⊢ e_1))
                         (where n_2 (⊢ e_2))
                         (where n_3 ,(+ (term n_1) (term n_2)))]
  [(⊢ (e_1 - e_2))       n_3
                         (where n_1 (⊢ e_1))
                         (where n_2 (⊢ e_2))
                         (where n_3 ,(- (term n_1) (term n_2)))]
  [(⊢ (e_1 * e_2))       n_3
                         (where n_1 (⊢ e_1))
                         (where n_2 (⊢ e_2))
                         (where n_3 ,(* (term n_1) (term n_2)))]
  [(⊢ (e_1 / e_2))       n_3
                         (where n_1 (⊢ e_1))
                         (where n_2 (⊢ e_2))
                         (where n_3 ,(/ (term n_1) (term n_2)))]
  [(⊢ (e_1))             n_1
                         (where n_1 (⊢ e_1))]
  )

(test-equal (term (⊢ ((1 + 2) + (3 + 4))))
            (term 10))
(test-equal (term (⊢ ((1 + 2) * (3 + 4))))
            (term 21))
(test-equal (term (⊢ (- ((1 + 2) * (3 + 4)))))
            (term -21))
(test-equal (term (⊢ (1 + (2 - {(3 * (4 / 2))}))))
            (term -3))


(test-results)