(defpackage :infer-type
  (:use :cl :serapeum)
  (:export ))
(in-package :infer-type)

(defclass type-env ()
  ((%typedefs :initform (make-hash-table)
              :initarg :typedefs
              :reader typedefs)
   (%typebindings :initform (make-hash-table)
                  :initarg :type-bindings
                  :reader typebindings)
   (%values :initform (make-hash-table)
            :reader values-)))

(defparameter *type-env* (make-instance 'type-env))

(defmacro with-types ((&rest types) (&rest defs) &body body)
  `(let ((*type-env* (make-instance 'type-env
                                    :typedefs
                                    (alexandria:alist-hash-table ',(loop for (type def) in types
                                                                      collect (cons type def)))
                                    :type-bindings
                                    (alexandria:alist-hash-table ',defs))))
     ,@body))

(defun lookup-type (type)
  (gethash type (typedefs *type-env*)))

(defun get-function-type (expr)
  (gethash (car expr)
           (typebindings *type-env*)))

(defun is-type-variable (tyvar)
  (and (symbolp tyvar)
       (char= (elt (symbol-name tyvar)
                   0)
              #\?)))

(defun is-bound-type-variable (tyvar)
  (nth-value 1 (gethash tyvar (typebindings *type-env*))))

(defun lookup-type-variable (tyvar)
  (gethash tyvar (typebindings *type-env*)))

(defun infer-simple-type (expr)
  (loop for k being the hash-keys of (typebindings *type-env*)
     using (hash-value v)
     when (subtypep (type-of expr) v) do
       (return k)))

(defun infer-complex-type (expr)
  (destructuring-bind (ret-type arg-types) (get-function-type expr)
    ))

(defun infer-type (expr)
  (if (is-simple-expression expr)
      (infer-simple-type expr)
      (infer-complex-type expr)))

(defun bind-type-variable (expr tyvar)
  (setf (gethash tyvar (typebindings *type-env*))
        (infer-type expr)))

(defun check-type- (expr type)
  (if (is-type-variable type)
      (if (is-bound-type-variable type)
          (check-type- expr
                       (lookup-type-variable type))
          (bind-type-variable expr type))
      (if (is-simple-expression expr)
          (check-simple-type expr type)
          (check-complex-type expr type))))

(defun is-simple-expression (expr)
  (or (not (listp expr))
      (eql (car expr)
           'quote)))

(defun check-simple-type (expr type)
  (values (subtypep (type-of expr)
                    (lookup-type type))
          type))

(defun check-complex-type (expr type)
  (destructuring-bind (return-type arg-types) (get-function-type expr)
    (values (and (lookup-type return-type)
                 (subtypep (lookup-type return-type)
                           (lookup-type type))
                 (= (1- (length expr))
                    (length arg-types))
                 (every (lambda (arg-expr arg-type)
                          (and (lookup-type arg-type)
                               (check-type- arg-expr arg-type)))
                        (cdr expr)
                        arg-types))
            return-type)))


(defun foo (a b)
  (check-type a number)
  (check-type b number)
  (+ a b))

#+null
(defmacro with-implicit-conversions ((&rest conversions) &body body)
  `(let ((num-coercions 0)
         (coercion-limit 10))
     (handler-bind ((type-error (lambda (c)
                                  (incf num-coercions)
                                  (when (< num-coercions
                                           coercion-limit)
                                    (let ((datum (type-error-datum c))
                                          (expected-type (type-error-expected-type c)))
                                      (store-value
                                       (cond ,@(loop for (type handler) in conversions
                                                  collect `((subtypep ',type expected-type)
                                                            (,handler datum))))))))))
       ,@body)))