;;; Alef Lazily Evaluates Functions
;;; (C) 2008-2009 Dr. Gergo ERDI <http://gergo.erdi.hu/>

(in-package :alef)

(defun subst-typedesc (substs type)
  (declare (list substs) (typedesc type))
  (cond ((typevar-p type)
         (let ((type* (cdr (assoc type substs))))
           (if type*
               (subst-typedesc substs type*)
               type)))
        ((consp type)
         (cons (car type) (mapcar #'(lambda (type) (subst-typedesc substs type)) (cdr type))))
        (t
         type)))

(defun subst-equations (substs equations)
  (loop for (left right) in equations
        collect (list (subst-typedesc substs left) (subst-typedesc substs right))))

(defun subst-requirement (substs req)
  (declare (list substs) (requirement req))
  (destructuring-bind (fun discr) req
    (list fun (subst-typedesc substs discr))))

(defun flatten-requirement (req)
  (declare (requirement req))
  (destructuring-bind (fun discr) req
    (if (typevar-p discr)
        (list req)
        (with-nice-types 
          (loop for supertype/override in (list-overrides fun)
                do (handler-case (let ((signature (signature-from-function (list fun supertype/override))))
                                   (return (mapcan #'(lambda (req) (flatten-requirement req)) (signature-reqs signature))))
                     (typecheck-error () ()))
                finally (error 'typecheck-error/overload :requirement req))))))

(defun subst-signature (substs signature)
  (make-signature
   (subst-typedesc substs (signature-type signature))
   (mapcan #'(lambda (req) (flatten-requirement req)) (mapcar #'(lambda (req) (subst-requirement substs req)) (signature-reqs signature)))))

(defun equal-length (list1 list2)
  (declare (list list1 list2))
  (or
   (and (null list1) (null list2))
   (and (not (null list1)) (not (null list2))
        (equal-length (cdr list1) (cdr list2)))))

(defun hindley-milner (equations)
  "Equations are in the form ((left1 right1) (left2 right2) ...).
Returns an alist of typevar->typedesc substitutions.

When both left and right are typevars, left is chosen"
  (labels ((substs-from-match (left right)
             (let ((left (curry-type left))
                   (right (curry-type right)))
               (cond
                 ;; Tautological equation
                 ((and (typevar-p left) (typevar-p right) (eql left right))
                  (list))
                 
                 ;; Trivial equation
                 ((typevar-p right)
                  (occur-check right left)
                  (list (cons right left)))
                 ((typevar-p left)
                  (occur-check left right)
                  (list (cons left right)))
                 
                 ((and (consp left) (consp right) (eql (car left) (car right)))                      
                  (unless (equal-length left right)
                    (error 'typecheck-error/unify :left left :right right))
                  (hindley-milner (loop for left-part in (cdr left)
                                        for right-part in (cdr right)
                                        collect (list left-part right-part))))

                 ;; TODO: Is this needed?
                 ((eq left right)
                  (list))
                 
                 (t
                  (error 'typecheck-error/unify :left left :right right)))))

           (occur-check (typevar typeexpr)
             (labels ((occur-check* (typeexpr*)
                        (if (eql typeexpr* typevar)
                            (error 'typecheck-error/occur :typevar typevar :typeexpr typeexpr)
                            (when (consp typeexpr*)
                              (mapc #'occur-check* typeexpr*)))))
               (occur-check* typeexpr))))
    
    (when equations      
      (destructuring-bind ((left right) &rest rest) equations
        (let ((substs (substs-from-match left right)))
          (nconc substs (hindley-milner (subst-equations substs rest))))))))

;;; TODO
(defun simplify-requirements (reqs)
  reqs)

(defun unify (typing)
  (declare (typing typing))
  (let ((substs (hindley-milner (typing-equations typing))))
    (values
     (subst-signature substs (typing-signature typing))
     substs)))