(module callec mzscheme
  (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 2 0))
           (planet "gui.ss" ("robby" "redex.plt" 2 0))
           (planet "subst.ss" ("robby" "redex.plt" 2 0)))
  
  (reduction-steps-cutoff 50)
  
  (define lang
    (language (e (e e)
                 (error)
                 (+ e e)
                 v)
              (v call/ec
                 number
                 (lambda (x) e)
                 x)
              
              (E (v E)
                 (E e)
                 (+ v E)
                 (+ E e)
                 (call/ec (lambda (x) E))
                 hole)
              
              (x (variable-except lambda call/ec))))
  
  (define-syntax (--> stx)
    (syntax-case stx ()
      [(_ name frm to) (syntax (reduction/name name lang frm (term to)))]))
  
  (define reductions
    (list
     (--> "throw"
          (in-hole E_1 
                   (call/ec (lambda (x_1) (in-hole E_2 (x_1 v_1)))))
          (in-hole E_1 
                   v_1))
     (--> "invalidate"
          (in-hole E_1 
                   (call/ec (lambda (x_1) v_1)))
          (in-hole E_1 
                   ((lambda (x_1) v_1) (lambda (ignore) (error)))))
     (--> "error"
          (in-hole E_1 (error))
          "error")
     (--> "βv"
          (in-hole E_1 ((lambda (x_1) e_body) v_arg))
          (in-hole E_1 ,(lc-subst (term x_1)
                                  (term v_arg)
                                  (term e_body))))
     (--> "+"
          (in-hole E_1 (+ number_1 number_2))
          (in-hole E_1 ,(+ (term number_1) (term number_1))))))
  
  (define lc-subst
    (subst
     ['abort (constant)]
     ['void (constant)]
     ['call/cc (constant)]
     ['(error) (constant)]
     [(? symbol?) (variable)]
     [(? number?) (constant)]
     [`(lambda (,x) ,b)
      (all-vars (list x))
      (build (lambda (vars body) `(lambda (,(car vars)) ,body)))
      (subterm (list x) b)]
     [`(call/cc ,v)
      (all-vars '())
      (build (lambda (vars arg) `(call/cc ,arg)))
      (subterm '() v)]
     [`(begin ,@(es ...))
      (all-vars '())
      (build (lambda (vars . args) `(begin ,@args)))
      (subterms '() es)]
     [`(,f ,x)
      (all-vars '())
      (build (lambda (vars f x) `(,f ,x)))
      (subterm '() f)
      (subterm '() x)]))

  (define (show e) (traces lang reductions e))
  
  ;(show '(+ (call/ec (lambda (x) (+ (x 1) 2))) 3))
  (show '(+ 1 ((call/ec (lambda (x) x)) 1)))
  )