core-language.ss
(module core-language mzscheme
  (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 3 9))
           (planet "subst.ss" ("robby" "redex.plt" 3 9))
           (lib "match.ss"))

  ;; ===========================================================================
  ;; AST MANIPULATION
  ;; ===========================================================================

  (define (operator? x)
    (and (memq x '(+ - =)) #t))

  (define (ground-type? t)
    (and (symbol? t)
         (not (eq? t 'dynamic))))

  (define (function-type? t)
    (match t
      [`(,_ -> ,_) #t]
      [_ #f]))

  (define (function-type-domain t)
    (match t
      [`(,dom -> ,_) dom]))

  (define (function-type-range t)
    (match t
      [`(,_ -> ,rng) rng]))

  (define (binding? x)
    (match x
      [`(,_ : ,_ = ,_) #t]
      [`(,_ = ,_) #t]
      [_ #f]))

  (define (binding-variable x)
    (match x
      [`(,var : ,_ = ,_) var]
      [`(,var = ,_) var]))

  (define (binding-type x)
    (match x
      [`(,_ : ,t = ,_) t]
      [`(,_ = ,_) 'dynamic]))

  (define (binding-init x)
    (match x
      [`(,_ : ,_ = ,init) init]
      [`(,_ = ,init) init]))

  (define (occurs-free? x e)
    (match e
      [(? symbol?) (eq? x e)]
      [(? number?) #f]
      [(? boolean?) #f]
      [`(lambda (,y : ,t) ,b)
        (and (not (eq? x y))
             (occurs-free? x b))]
      [`(let (,y : ,t = ,e1) ,e2)
        (or (occurs-free? x e1)
            (and (not (eq? x y))
                 (occurs-free? x e2)))]
      [`(letrec ([,ys : ,ts = ,vs] ...) ,b)
        (and (not (memq x ys))
             (ormap (lambda (e)
                      (occurs-free? x e))
                    (cons b vs)))]
      [`(,(and op (? operator?)) ,e1 ,e2)
        (or (occurs-free? x e1)
            (occurs-free? x e2))]
      [`(if ,e1 ,e2 ,e3)
        (or (occurs-free? x e1)
            (occurs-free? x e2)
            (occurs-free? x e3))]
      [`(cast ,_ ,e)
        (occurs-free? x e)]
      [`(,e1 ,e2)
        (or (occurs-free? x e1)
            (occurs-free? x e2))]))

  (define (live-letrec? x)
    (match x
      [`(letrec ([,xs : ,_ = ,_] ...) ,body)
        (ormap (lambda (x)
                 (occurs-free? x body))
               xs)]))

  ;; ===========================================================================
  ;; LANGUAGE
  ;; ===========================================================================

  (define core-language
    (language [x (variable-except lambda + - = if error cast int bool dynamic -> : let succ fail function  ! ? <=)]
              [e (e e)
                 (+ e e)
                 (- e e)
                 (= e e)
                 (if e e e)
                 (let (x : t = e) e)
                 (letrec ([x : t = v] ...) e)
                 x
                 s]
              [F (v hole)
                 ((hole #f) e)
                 (+ hole e)
                 (+ v hole)
                 (- hole e)
                 (- v hole)
                 (= hole e)
                 (= v hole)
                 (if hole e e)
                 (let (x : t = hole) e)
                 (letrec ([x : t = v] ...) hole)]
              ;; Core evaluation contexts:
              [C hole (in-hole F E)]
              ;; Surface evaluation contexts:
              [E C]
              [s number
                 #t #f
                 (lambda (x : t) e)]
              [v s
                 (side-condition (name form (letrec ([x : t = v] ...) v))
                                 (live-letrec? (term form)))]
              [t dynamic
                 int
                 bool
                 (t -> t)]
              ))

  (define language/st
    (extend-language core-language
      [e .... (cast t e)]
      ;; NOTE: cast frames can nest arbitrarily, so core evaluation contexts
      ;;       are not distinguished from surface evaluation contexts
      [C .... (cast t E)] ;; TODO: exclude (cast dynamic E)?
      [v .... (cast dynamic s)]))

  (define language/htf
    (extend-language core-language
      [D int
         bool
         function]
      [c succ
         fail
         (! D)
         (? D)
         (function c c)
         ( c c)]
      [e .... (cast (t <= c) e)]
      ;; NOTE: we disallow nesting of adjacent cast frames by distinguishing
      ;;       core evaluation contexts from surface evaluation contexts
      [E .... (cast (t <= c) C)]
      [v .... (side-condition (cast (t <= c_0) s) (not (test-match language/htf succ (term c_0))))]))

  ;; ===========================================================================
  ;; SUBSTITUTION
  ;; ===========================================================================

  ;; TODO: replace all this stuff with a simpler define-metafunction

  ;; TODO: this appears to be broken in some cases
  (define (substitute* vars vals expr)
    (cond
      [(and (null? vars) (null? vals))
       expr]
      [(or (null? vars) (null? vals))
       (error 'eval "formal and actual parameter lists of different length: " vars vals)]
      [else
       (substitute* (cdr vars) (cdr vals) (substitute (car vars) (car vals) expr))]))

  (define substitute
    (plt-subst
     [(? symbol?) (variable)]
     [(? number?) (constant)]
     [(? boolean?) (constant)]
     [`(lambda (,x : ,t) ,b)
       (all-vars (list x))
       (build (lambda (vars body) `(lambda (,(car vars) : ,t) ,body)))
       (subterm (list x) b)]
     [`(let (,x : ,t = ,e1) ,e2)
       (all-vars (list x))
       (build (lambda (vars binding body) `(let (,(car vars) : ,t = ,binding) ,body)))
       (subterm '() e1)
       (subterm (list x) e2)]
     [`(letrec ([,xs : ,ts = ,vs] ...) ,b)
       (all-vars xs)
       (build (lambda (vars vs body)
                `(letrec ,(map (lambda (x t v)
                                 `[,x : ,t = ,v])
                               vars ts vs)
                   ,body)))
       (subterm xs vs)
       (subterm xs b)]
     [`(,(and op (? operator?)) ,e1 ,e2)
       (all-vars '())
       (build (lambda (vars e1 e2) `(,op ,e1 ,e2)))
       (subterm '() e1)
       (subterm '() e2)]
     [`(if ,e1 ,e2 ,e3)
       (all-vars '())
       (build (lambda (vars e1 e2 e3) `(if ,e1 ,e2 ,e3)))
       (subterm '() e1)
       (subterm '() e2)
       (subterm '() e3)]
     [`(cast ,x ,e)
       (all-vars '())
       (build (lambda (vars e) `(cast ,x ,e)))
       (subterm '() e)]
     [`(,f ,x)
       (all-vars '())
       (build (lambda (vars f x) `(,f ,x)))
       (subterm '() f)
       (subterm '() x)]
     ))

  ;; ===========================================================================
  ;; BASIC REDUCTIONS
  ;; ===========================================================================

  (define (core-reductions lang)
    ;; lookup-letrec : looks up a letrec-bound variable in the context
    (define-metafunction lookup-letrec
      lang
      [((in-hole E_0 (letrec ([x_0 : t_0 = v_0] ... [x_1 : t_1 = v_1] [x_2 : t_2 = v_2] ...) hole)) x_1)
       v_1]
      [((in-hole E_0 F_0) x_0)
       (lookup-letrec (E_0 x_0))]
      [((in-hole E_0 (cast any hole)) x_0)
       (lookup-letrec (E_0 x_0))]
      [((hole #f) x_0)
       "error: free variable"])

    (reduction-relation lang
      [==> ((lambda (x_0 : t_0) e_0) v_0)
           ,(substitute (term x_0)
                           (term v_0)
                           (term e_0))
           "βv"]
      [==> (let (variable_x : t_xt = v_binding) e_body)
           ,(substitute (term variable_x)
                           (term v_binding)
                           (term e_body))
           "ELet"]
      ;; variable references are allowed for letrec-bound variables:
      [--> (in-hole E_0 variable_x)
           (in-hole E_0 (lookup-letrec (E_0 variable_x)))
           "ERec"]
      [==> (+ number_m number_n)
           ,(+ (term number_m) (term number_n))
           "EAdd"]
      [==> (- number_m number_n)
           ,(- (term number_m) (term number_n))
           "ESub"]
      [==> (= number_m number_n)
           ,(= (term number_m) (term number_n))
           "EEq"]
      [==> (if #t e_consequent e_alternate)
           e_consequent
           "EIfT"]
      [==> (if #f e_consequent e_alternate)
           e_alternate
           "EIfF"]
      ;; dead letrecs can be garbage-collected:
      [==> (letrec ([variable_xs : t_ts = v_bindings] ...) v_result)
           v_result
           "EGC"]
      where
      [(==> a b) (--> (in-hole E_1 a) (in-hole E_1 b))]))

  (provide (all-defined)))