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

(in-package :alef)

(defun curry-type (type)
  "Converts (fun a b c d) into (fun a (fun b (fun c d))"
  (declare (typedesc type))
  (cond ((type-fun-p type)
         (destructuring-bind (left &rest right) (cdr type)
           (if right
               (cons 'fun (list left (curry-type (cons 'fun right))))
               left)))
        ((and (consp type) (not (cdr type)))
         (car type))
        (t
         type)))

(defun uncurry-type (type)
  "Converts (fun a b (fun c d)) into (fun a b c d)"
  (declare (typedesc type))
  (if (type-fun-p type)
      (let ((tail (last (cdr type))))
        (if (and tail (type-fun-p (car tail)))
            (uncurry-type (cons 'fun (append (butlast (cdr type)) (cdr (car tail)))))
            type))
      type))

(defvar *num-typevars*)
(defvar *typevar-readable-mapping* nil)

(defmacro with-nice-types (&body body)
  `(if *typevar-readable-mapping*
       (progn ,@body)       
       (let ((*num-typevars* 0)
             (*typevar-readable-mapping* (make-hash-table)))
         ,@body)))

(defun show-type (type)  
  (declare (typedesc type))  
  (let ((funp))
    (declare (special funp))
    (labels ((show-type/rec (type)
               (cond ((typevar-p type)
                      (let ((typevar (type-supertype type)))
                        (if *typevar-readable-mapping*
                            (or (gethash typevar *typevar-readable-mapping*)
                                (if (< *num-typevars* 26)
                                    (setf (gethash typevar *typevar-readable-mapping*)
                                          (princ-to-string (code-char (+ (char-code #\a) (1- (incf *num-typevars*))))))
                                    (symbol-name typevar)))
                            (symbol-name typevar))))
                     ((and (consp type) (eq (car type) 'fun))
                      (let ((str (format nil "~{~A~^ -> ~}"
                                         (let ((funp t))
                                           (declare (special funp))
                                           (mapcar #'show-type/rec (cdr type))))))
                        (if funp (format nil "(~A)" str) str)))
                     ((consp type)
                      (if (cdr type)
                          (format nil "(~A ~{~A~^ ~})" (show-type/rec (car type)) (mapcar #'show-type/rec (cdr type)))
                          (show-type/rec (car type))))
                     (t
                      (string-capitalize (symbol-name type))))))
      (show-type/rec (uncurry-type type)))))

(defun show-requirement (req)
  (declare (requirement req))
  (destructuring-bind (fun discr) req
    (format nil "(~A ~A)" fun (show-type discr))))

(defun show-signature (signature)
  (declare (signature signature))
  (format nil "~:[~;~:*~{~A~^, ~} => ~]~A" (mapcar #'show-requirement (signature-reqs signature)) (show-type (signature-type signature))))

(defmethod print-object ((signature signature) s)
  (print-unreadable-object (signature s :type t)
    (princ (show-signature signature) s)))

(defun show-eqs (eqs)
  (format nil "{~{~A~^, ~}}"
          (loop for (left right) in eqs
                collect (format nil "~A = ~A" (show-type left) (show-type right)))))

(defun show-substs (eqs)
  (format nil "{~{~A~^, ~}}"
          (loop for (left . right) in eqs
                collect (format nil "~A -> ~A" (show-type left) (show-type right)))))

(defmethod print-object ((typing typing) s)
  (print-unreadable-object (typing s :type t)
    (format s "~A |- ~A" (show-eqs (typing-equations typing)) (show-signature (typing-signature typing)))))

(defun instantiate-typevars (type &optional (mapping (make-hash-table)))
  (declare (typedesc type) (hash-table mapping))
  (cond ((typevar-p type)
         (or (gethash type mapping)
             (setf (gethash type mapping) (make-typevar))))
        ((consp type)
         (mapcar #'(lambda (type) (instantiate-typevars type mapping)) type))
        (t
         type)))

(defun instantiate-signature (signature)
  (declare (signature signature))
  (let ((hash-table (make-hash-table)))
    (make-signature (curry-type (instantiate-typevars (signature-type signature) hash-table))
                    (loop for (fun discr) in (signature-reqs signature)
                          collect (list fun
                                        (if (typevar-p discr)
                                            (instantiate-typevars discr hash-table)
                                            discr))))))