(module core-calculi mzscheme
  
  (require (planet "reduction-semantics.ss" ("robby" "redex.plt" 2))
           (planet "subst.ss" ("robby" "redex.plt" 2))
           (lib "match.ss")
           "language-composer-tools.ss")
  
  (provide base
           base-types
           base-scheme-reductions/no-wrong
           base-scheme-reductions
           base-ml-reductions
           α-equivalent?
           error-message?)
  
  ;; ============================================================
  ;; CORE GRAMMARS
  (define-pre-grammar base
    ;; scheme
    (s:e (s:e s:e)
          x
          (lambda (x) s:e)
          number
          (op s:e s:e)
          (ifzero s:e s:e s:e)
          (pr s:e)
          (wrong string)
          )
     (s:v (lambda (x) s:e)
          number)
     (op + -)
     (pr proc? nat?)
     
     (sc (hole s) 
         (sc s:e) 
         (s:v sc)
         (op sc s:e)
         (op s:v sc)
         (ifzero sc s:e s:e)
         (pr sc))
     
     ;; ml
     (m:e (m:e m:e) 
          x 
          (lambda (x : m:ty) m:e)
          (op m:e m:e)
          number
          (ifzero m:e m:e m:e))
     (m:v (lambda (x : m:ty) m:e)
          number)
     (m:ty num (m:ty -> m:ty))
     
     (mc (hole m) 
         (mc m:e)
         (m:v mc)
         (op mc m:e)
         (op m:v mc)
         (ifzero mc m:e m:e))
     
    (x (variable-except lambda SM MS -> num L wrong proc? nat? ifzero + - forall tyapp)))
  
  ;; ============================================================
  ;; TYPING JUDGEMENTS
  
  (define-type-judgements base-types 
    (m:typeof Γ
     [(? symbol? x) (lookup x Γ)]
     [(? number?) 'num]
     [`(,e_1 ,e_2)
       (match (list (m:typeof e_1 Γ) (m:typeof e_2 Γ))
         [`((,ty_dom -> ,ty_rng) ,ty_arg)
           (if (equal? ty_dom ty_arg)
               ty_rng
               #f)]
         [_ #f])]
     [`(lambda (,x : ,dom_ty) ,e)
       (let ((rng_ty (m:typeof e (extend Γ x dom_ty))))
         (if rng_ty
             `(,dom_ty -> ,rng_ty)
             #f))]
     [`(,(? op?) ,e_1 ,e_2)
       (match (list (m:typeof e_1 Γ) (m:typeof e_2 Γ))
         [`(num num)
           'num]
         [_ #f])]
     [`(ifzero ,e1 ,e2 ,e3)
       (let ((t1 (m:typeof e1 Γ))
             (t2 (m:typeof e2 Γ))
             (t3 (m:typeof e2 Γ)))
         (if (and (equal? t1 'num)
                  (equal? t2 t3))
             t2
             #f))])
    (s:typeof Γ
     [(? number?) 'TST]
     [(? symbol?) 'TST]
     [`(,(? pr?) ,e)
       (if (s:typeof e Γ) 'TST #f)]
     [`(wrong ,(? string?)) 'TST]
     [`(,e_1 ,e_2)
       (if (and (s:typeof e_1 Γ) (s:typeof e_2 Γ))
           'TST
           #f)]
     [`(lambda (,_) ,e)
       (if (s:typeof e Γ)
           'TST
           #f)]
     [`(,(? op?) ,e1 ,e2)
       (if (and (s:typeof e1 Γ) (s:typeof e2 Γ))
           'TST
           #f)]
     [`(ifzero ,e1 ,e2 ,e3)
       (if (and (s:typeof e1 Γ) (s:typeof e2 Γ) (s:typeof e3 Γ))
           'TST
           #f)]))
  
  ;; ============================================================
  ;; REDUCTIONS
  ;; note the reliance on the E nonterminal, which is not defined
  ;; here. The intention is that extensions will define a top-level
  ;; evaluation context elsewhere.
  (define (lambda-term? t)
    (match t
      [`(lambda (,x) ,e) #t]
      [_ #f]))
  (define (op? op) (memq op '(+ -)))
  (define (pr? pr) (memq pr '(proc? nat?)))
  
  (define (base-scheme-reductions/no-wrong ms)
    (list
     ;; beta
     (reduction ms
                (in-named-hole s 
                               E_1
                               ((lambda (x_a) s:e_b) s:v_a))
                (term
                 (in-hole 
                  E_1 
                  ,(substitute (term x_a) (term s:v_a) (term s:e_b)))))
     (reduction ms
                (side-condition
                 (in-named-hole s E_1 (s:v_1 s:v))
                 (not (lambda-term? (term s:v_1))))
                (term (in-hole E_1 (wrong "non-procedure"))))
     
     ;; sum
     (reduction ms
                (in-named-hole s 
                               E_1
                               (+ number_1 number_2))
                (term
                 (in-hole 
                  E_1 
                  ,(+ (term number_1) (term number_2)))))
     (reduction ms
                (in-named-hole s 
                               E_1
                               (- number_1 number_2))
                (term
                 (in-hole 
                  E_1 
                  ,(max (- (term number_1) (term number_2)) 0))))
     (reduction ms
                (side-condition
                 (in-named-hole s 
                                E_1
                                (op s:v_1 s:v_2))
                 (not (and (number? (term s:v_1)) (number? (term s:v_2)))))
                (term (in-hole E_1 (wrong "non-number"))))
     
     ;; ifzero
     (reduction ms
                (in-named-hole s
                               E_1
                               (ifzero s:v_1 s:e_1 s:e_2))
                (cond
                  [(eqv? (term s:v_1) 0)
                   (term (in-hole E_1 s:e_1))]
                  [else
                   (term (in-hole E_1 s:e_2))]))
     
     ;; predicates
     (reduction ms
                (in-named-hole s
                               E_1
                               (proc? (lambda (x) s:e)))
                (term (in-hole E_1 0)))
     (reduction ms
                (side-condition
                 (in-named-hole s
                                E_1
                                (proc? s:v_1))
                 (not (lambda-term? (term s:v_1))))
                (term (in-hole E_1 1)))
     (reduction ms
                (in-named-hole s
                               E_1
                               (nat? number))
                (term (in-hole E_1 0)))
     (reduction ms
                (side-condition
                 (in-named-hole s
                                E_1
                                (nat? s:v_1))
                 (not (number? (term s:v_1))))
                (term (in-hole E_1 1)))))
  
  (define (base-scheme-reductions ms)
    (cons
     ;; wrong
     (reduction ms
                (in-named-hole s
                               E_1
                               (wrong string_1))
                (term string_1))
     (base-scheme-reductions/no-wrong ms)))

  (define (base-ml-reductions ms)
    (list
     
     ;; beta
     (reduction ms
                (in-named-hole m 
                               E_1
                               ((lambda (x_a : m:ty) m:e_b) m:v_a))
                (term (in-hole E_1 
                               ,(substitute (term x_a) (term m:v_a) (term m:e_b)))))
     
     ;; sum
     (reduction ms
                (in-named-hole m
                               E_1
                               (+ number_1 number_2))
                (term
                 (in-hole 
                  E_1 
                  ,(+ (term number_1) (term number_2)))))
     (reduction ms
                (in-named-hole m
                               E_1
                               (- number_1 number_2))
                (term
                 (in-hole 
                  E_1 
                  ,(max (- (term number_1) (term number_2)) 0))))
     
     ;; ifzero
     (reduction ms
                (in-named-hole m
                               E_1
                               (ifzero number_1 m:e_1 m:e_2))
                (cond
                  [(eqv? (term number_1) 0)
                   (term (in-hole E_1 m:e_1))]
                  [else
                   (term (in-hole E_1 m:e_2))]))))
  
  
  
  ;; ============================================================
  ;; HELPERS
  
  (define substitute
    (subst
     [(? symbol?) (variable)]
     [(? number?) (constant)]
     [(? string?) (constant)]
     [`(lambda (,x) ,b)
      (all-vars (list x))
      (build (lambda (vars body) `(lambda (,(car vars)) ,body)))
      (subterm (list x) b)]
     [`(LAMBDA (,x) ,e)
       (all-vars '())
       (build (lambda (vars body) `(LAMBDA (,x) ,body)))
       (subterm '() e)]
     [`(lambda (,x : ,ty) ,b)
      (all-vars (list x))
      (build (lambda (vars body) `(lambda (,(car vars) : ,ty) ,body)))
      (subterm (list x) b)]
     [`(SM ,ty ,e)
      (all-vars '())
      (build (lambda (vars eb) `(SM ,ty ,eb)))
      (subterm '() e)]
     [`(MS ,ty ,e)
      (all-vars '())
      (build (lambda (vars eb) `(MS ,ty ,eb)))
      (subterm '() e)]
     [`(GSM ,ty ,e)
      (all-vars '())
      (build (lambda (vars eb) `(GSM ,ty ,eb)))
      (subterm '() e)]
     [`(MSG ,ty ,e)
      (all-vars '())
      (build (lambda (vars eb) `(MSG ,ty ,eb)))
      (subterm '() e)]
     [`(GSM ,ty ,eqs ,e)
      (all-vars '())
      (build (lambda (vars eb) `(GSM ,ty ,eqs ,eb)))
      (subterm '() e)]
     [`(MSG ,ty ,eqs ,e)
      (all-vars '())
      (build (lambda (vars eb) `(MSG ,ty ,eqs ,eb)))
      (subterm '() e)]
     [`(g ,mty ,e)
       (all-vars '())
       (build (lambda (vars e) `(g ,mty ,e)))
       (subterm '() e)]
     [`(g+ ,mty ,e)
       (all-vars '())
       (build (lambda (vars e) `(g+ ,mty ,e)))
       (subterm '() e)]
     [`(g- ,mty ,e)
       (all-vars '())
       (build (lambda (vars e) `(g- ,mty ,e)))
       (subterm '() e)]
     [`(wrong (? string?))
       (constant)]
     [`(,(? op? o) ,e1 ,e2)
      (all-vars '())
      (build (lambda (vars e1 e2) `(,o ,e1 ,e2)))
      (subterm '() e1)
      (subterm '() e2)]
     [`(ifzero ,e1 ,e2 ,e3)
      (all-vars '())
      (build (lambda (vars e1 e2 e3) `(ifzero ,e1 ,e2 ,e3)))
      (subterm '() e1)
      (subterm '() e2)
      (subterm '() e3)]
     [`(handle ,e1 ,e2)
       (all-vars '())
       (build (lambda (vars e1 e2) `(handle ,e1 ,e2)))
       (subterm '() e1)
       (subterm '() e2)]
     [`(raise ,_ ,_)
       (constant)]
     [`(tyapp ,e ,ty)
       (all-vars '())
       (build (lambda (vars body) `(tyapp ,body ,ty)))
       (subterm '() e)]
     [`(,f ,x)
      (all-vars '())
      (build (lambda (vars f x) `(,f ,x)))
      (subterm '() f)
      (subterm '() x)]))
  
  (define (α-equivalent? p1 p2)
    
    (define free (gensym))
    (define (mt var) free)
    (define (extend env var depth)
      (lambda (v)
        (if (eq? v var) depth (env v))))
    
    (define (s:α-equivalent? p1 p2 depth m1 m2)
      (match (list p1 p2)
        [`(,(? symbol?) ,(? symbol?))
          (eq? (m1 p1) (m2 p2))]
        [`(,(? number?) ,(? number?))
         (= p1 p2)]
        [`(,(? string?) ,(? string?))
         (string=? p1 p2)]
        [`((lambda (,x1) ,b1) (lambda (,x2) ,b2))
          (s:α-equivalent? b1 b2 (add1 depth) (extend m1 x1 depth) (extend m2 x2 depth))]
        [`((wrong ,s1) (wrong ,s2))
          (string=? s1 s2)]
        [`((,(? op? o1) ,a1 ,b1) (,(? op? o2) ,a2 ,b2))
         (and (eqv? o1 o2)
              (s:α-equivalent? a1 a2 depth m1 m2)
              (s:α-equivalent? b1 b2 depth m1 m2))]
        [`((,(? pr? p1) ,e1) (,(? pr? p2) ,e2))
          (and (eqv? p1 p2)
               (s:α-equivalent? e1 e2 depth m1 m2))]
        [`((SM ,ty1 ,mlt1) (SM ,ty2 ,mlt2))
          (and (equal? ty1 ty2)
               (m:α-equivalent? mlt1 mlt2 depth m1 m2))]
        [`((GSM ,ty1 ,mlt1) (GSM ,ty2 ,mlt2))
          (and (equal? ty1 ty2)
               (m:α-equivalent? mlt1 mlt2 depth m1 m2))]
        [`((GSM ,ty1 ,eqs1 ,mlt1) (GSM ,ty2 ,eqs2 ,mlt2))
          (and (equal? ty1 ty2)
               (equal? eqs1 eqs2)
               (m:α-equivalent? mlt1 mlt2 depth m1 m2))]
        [`((g ,ty1 ,e1) (g ,ty2 ,e2))
          (and (equal? ty1 ty2)
               (s:α-equivalent? e1 e2 depth m1 m2))]
        [`((g+ ,ty1 ,e1) (g+ ,ty2 ,e2))
          (and (equal? ty1 ty2)
               (s:α-equivalent? e1 e2 depth m1 m2))]
        [`((g- ,ty1 ,e1) (g- ,ty2 ,e2))
          (and (equal? ty1 ty2)
               (s:α-equivalent? e1 e2 depth m1 m2))]
        [`((handle ,e11 ,e12) (handle ,e21 ,e22))
          (and (s:α-equivalent? e11 e21 depth m1 m2)
               (s:α-equivalent? e12 e22 depth m1 m2))]
        [`((,p1f ,p1a) (,p2f ,p2a))
         (and (s:α-equivalent? p1f p2f depth m1 m2)
              (s:α-equivalent? p1a p2a depth m1 m2))]
        [_ #f]))
    
    (define (m:α-equivalent? p1 p2 depth m1 m2)
      (match (list p1 p2)
        [`(,(? symbol?) ,(? symbol?))
          (eq? (m1 p1) (m2 p2))]
        [`(,(? number?) ,(? number?))
         (= p1 p2)]
        [`(,(? string?) ,(? string?))
         (string=? p1 p2)]
        [`((lambda (,x1 : ,ty1) ,b1) (lambda (,x2 : ,ty2) ,b2))
          (m:α-equivalent? b1 b2 (add1 depth) (extend m1 x1 depth) (extend m2 x2 depth))]
        [`((handle ,e11 ,e12) (handle ,e21 ,e22))
          (and (m:α-equivalent? e11 e21 depth m1 m2)
               (m:α-equivalent? e12 e22 depth m1 m2))]
        [`((raise ,tau1 ,s1) (raise ,tau2 ,s2))
          (and (string=? s1 s2)
               (equal? tau1 tau2))]
        [`((,p1f ,p1a) (,p2f ,p2a))
          (and (m:α-equivalent? p1f p2f depth m1 m2)
               (m:α-equivalent? p1a p2a depth m1 m2))]
        [`((MSG ,ty1 ,st1) (MSG ,ty2 ,st2))
          (and (equal? ty1 ty2)
               (s:α-equivalent? st1 st2 depth m1 m2))]
        [`((MSG ,ty1 ,eqs1 ,st1) (MSG ,ty2 ,eqs2 ,st2))
          (and (equal? ty1 ty2)
               (equal? eqs1 eqs2)
               (s:α-equivalent? st1 st2 depth m1 m2))]
        [`((MS ,ty1 ,st1) (MS ,ty2 ,st2))
          (and (equal? ty1 ty2)
               (s:α-equivalent? st1 st2 depth m1 m2))]
        [_ #f]))
    
    (m:α-equivalent? p1 p2 0 mt mt))
  
  
   ;; ============================================================
  ;; TESTING APPARATUS
  (define error-message? string?))