#lang hackett

(require (only-in racket module quote let-syntax define-for-syntax define-syntax for-syntax)
         (for-syntax racket syntax/parse))

; Helper for syntax stuff later
(module deflang racket
  (require (for-syntax syntax/parse))
  (provide define-language define-language-syntax)

  (begin-for-syntax
    (struct language (introducer)
      #:property prop:procedure
      (lambda (inst stx)
        (syntax-parse stx
          [(_ e)
           ((language-introducer inst) #'e)]))))

  (define-syntax define-language
    (syntax-parser
      [(_ name)
       #'(define-syntax name
           (language (make-syntax-introducer)))]))

  (define-syntax define-language-syntax
    (syntax-parser
      [(_ lang form transformer)
       (define intro
         (language-introducer
          (syntax-local-value #'lang)))
       #`(define-syntax #,(intro #'form)
           transformer)])))

(require 'deflang)

; Define a language interface with tagless final

(class (Symantics repr)
  [int : (-> Integer (repr Integer))]
  [add : (-> (repr Integer)
             (-> (repr Integer)
                 (repr Integer)))]
  [lam : (∀ (a b)
            (-> (-> (repr a) (repr b))
                (repr (-> a b))))]
  [app : (∀ (a b)
            (-> (repr (-> a b))
                (-> (repr a)
                    (repr b))))])

; An interpretation that evaluates terms
;  metacircularly with Hackett

(data (R a) (R a))

(defn unR : (∀ (a) (-> (R a) a))
  [[(R x)] x])

(instance (Symantics R)
          [int (λ [x] (R x))]
          [add (λ [e1 e2] (R (+ (unR e1)
                                (unR e2))))]
          [lam (λ [f] (R (λ [x] (unR (f (R x))))))]
          [app (λ [e1 e2] (R ((unR e1) (unR e2))))])

(def foo : (∀ [repr] (Symantics repr) => (repr Integer))
  (app
   (lam (λ [x] (add (app x (int 1)) (int 2))))
   (lam (λ [x] (int 1)))))

; Add syntactic sugar

(define-language tagless-lang)

(define-language-syntax tagless-lang λ
  (syntax-parser
    [(_ (x) body)
     #'(#%app lam (λ [x] body))]))

(define-language-syntax tagless-lang #%datum
  (syntax-parser
    [(_ ~rest e)
     #`(#%app int #,(cons #'#%datum #'e))]))

(define-language-syntax tagless-lang #%app
  (syntax-parser
    [(_ e1 e2)
     #'(#%app app e1 e2)]))

(define-language-syntax tagless-lang +
  (syntax-parser
    [(_ e1 e2)
     #`(#%app add e1 e2)]))

; Now we can write terms of the tagless final DSL
;  with nice syntax
(def foo2 : (∀ [repr] (Symantics repr) => (repr Integer))
  (tagless-lang
   ((λ [x] (+ (x 1) 2))
    (λ [x] 1))))

; Extend the language with multiplication

; Interface
(class (MulSym repr)
  [mul : (-> (repr Integer)
             (-> (repr Integer)
                 (repr Integer)))])

; Interpreter
(instance (MulSym R)
          [mul (λ [e1 e2] (R (* (unR e1) (unR e2))))])

; Syntax
(define-language-syntax tagless-lang *
  (syntax-parser
    [(_ e1 e2)
     #`(#%app mul e1 e2)]))

; And an example program. With better inference
; we wouldn't have to write the type.
(def foo3 : (∀ [repr] (Symantics repr) (MulSym repr) => (repr Integer))
  (tagless-lang
   (* 5
      ((λ [x] (+ (x 1) 2))
       (λ [x] 1)))))