(in-package #:coalton-user)

(named-readtables:in-readtable coalton:coalton)

(coalton-toplevel
  ;; Define Coalton `Symbol`s as Lisp `cl:keyword`s.
  (repr :native cl:keyword)
  (define-type Symbol)

  ;; Bind a Lisp function into Coalton.
  (declare sym (String -> Symbol))
  (define (sym s)
    "Create a new symbol named `s`."
    (lisp Symbol (s)
      (cl:intern s "KEYWORD")))

  ;; Define equality of `Symbol` types using CL's `eq`.
  (define-instance (Eq Symbol)
    (define (== a b)
      (lisp Boolean (a b)
        (cl:eq a b))))

  ;; Define a new parametric algebraic data type for simple
  ;; mathematical expressions.
  (define-type (Expr :t)
    "A symbolic expression of basic arithmetic."
    (EConst :t)
    (EVar   Symbol)
    (E+     (Expr :t) (Expr :t))
    (E*     (Expr :t) (Expr :t)))

  ;; The classic `diff` function, in Coalton.
  (declare diff (Num :t => Symbol -> Expr :t -> Expr :t))
  (define (diff x f)
    "Compute the derivative of `f` with respect to `x`."
    (match f
      ((EConst _)                       ; c' = 0
       (EConst 0))
      ((EVar s)                         ; x' = 1
       (if (== s x) (EConst 1) (EConst 0)))
      ((E+ a b)                         ; (a+b)' = a' + b'
       (E+ (diff x a) (diff x b)))
      ((E* a b)                         ; (ab)' = a'b + ab'
       (E+ (E* (diff x a) b)
           (E* a          (diff x b))))))

  ;; We can use `t` just fine since Coalton doesn't import `cl:t`.
  (define t (sym "t"))

  (declare dt (Num :t => Expr :t -> Expr :t))
  (define dt
    "The time derivative operator."
    (diff t)))

CL-USER> (in-package #:coalton-user)
COALTON-USER> (coalton-toplevel
                (define (square x) (E* x x)))
; No value
COALTON-USER> (coalton (dt (E+ (square (EVar t)) (EConst 1))))
#.(E+ #.(E+ #.(E* #.(ECONST 1) #.(EVAR |t|))
            #.(E* #.(EVAR |t|) #.(ECONST 1)))
      #.(ECONST 0))