(module arithmetic mzscheme
  (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 4))
           (planet "gui.ss" ("robby" "redex.plt" 4)))
  
  (define-language lang
    (e (binop e e)
       (sqrt e)
       number)
    (binop +
           -
           *
           /)
    
    (e-ctxt (binop e e-ctxt)
            (binop e-ctxt v)
            (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")
     where
     [(c--> a b) (--> (in-hole e-ctxt_1 a) (in-hole e-ctxt_1 b))]))
  
  (traces lang reductions (term (- (* (sqrt 36) (/ 1 2)) (+ 1 2)))))