(module arithmetic mzscheme
  (require "../reduction-semantics.ss"
           "../gui.ss")
  
  (define lang
    (language 
     (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 '(- (* (sqrt 36) (/ 1 2)) (+ 1 2))))