(module front-end mzscheme
  (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 3 9))
           (planet "environment.ss" ("cobbe" "environment.plt" 3 0))
           (lib "match.ss")
           "static-semantics.ss")

  (define-struct semantics (language reduction-relation coercion-function value-predicate) #f)

  (define (type-check s x)
    ((insert-casts (semantics-coercion-function s)) x (make-empty-env)))

  (define (next relation term)
    (let ([results (apply-reduction-relation relation term)])
      (cond
        [(null? results)
         (error 'next (format "stuck term: ~a" term))]
        [(not (null? (cdr results)))
         (error 'next (format "non-determinism: ~a" term))]
        [else
         (car results)])))

  (provide (all-defined)))