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

(in-package :alef)

(defun typevar-p (typedesc)
  (declare (typedesc typedesc))
  (not (or (consp typedesc)
           (eq typedesc 'fun)
           (type-p (type-supertype typedesc)))))

(defun signature-from-constructor (expr)
  (declare (pnode expr))
  (typecase (pnode-symbol expr)
    (integer (make-signature 'int))
    (string (make-signature 'string))
    (t
     (let ((constructor (cdr (assoc (pnode-symbol expr) *constructors*))))
       (declare (constructor-info constructor))
       (instantiate-signature (constructor-signature constructor))))))

(defun typecheck-function (fun)
  "If fun's type is explicitly declared, check that this type matches the function's definition.
If it's not declared explicitly, infer it."
  (let ((signature/decl (signature-from-function-decl fun))
        (signature/def (signature-from-function-def fun)))    
    (if signature/decl
        (progn
          (hindley-milner (list (list (curry-type (signature-type signature/def)) (curry-type (signature-type signature/decl)))))
          signature/decl)
        (progn
          (set-function-decl fun signature/def)
          signature/def))))

(defun signature-from-function-decl (fun)
  (declare (funspec fun))
  (if (native-function-p fun)
      (gethash fun *declarations/native*)
      (get-function-decl fun)))

(defun signature-from-function-def (fun)
  (declare (funspec fun))
  (signature-from-function-srcs fun (get-function-srcs fun)))

(defun signature-from-function (fun)
  (declare (funspec fun))
  (or (signature-from-function-decl fun) (signature-from-function-def fun)))

(defun apply-typetable (typetable substs)
  (declare (hash-table typetable) (list substs))
  (loop for pnode being the hash-keys of typetable using (hash-value signature/pnode)
        unless (pnode-signature pnode)
        do (setf (pnode-signature pnode) (subst-signature substs signature/pnode))))

(defun signature-from-function-srcs (fun srcs)
  (declare ((or symbol list) fun) (list srcs))
  (let ((type (make-typevar)))
    (with-symbol-table *declarations*
      (symbol-table-add *declarations* fun (list () (make-signature type)))
      (let ((typetable (make-hash-table)))
        (loop for (formals body) in srcs
              for arity* = (length formals)
              for arity = arity* then arity
              for typing = (typing-from-function-src (make-symbol-table) typetable formals body)
              for signature = (typing-signature typing)
              unless (= arity* arity) do (error 'typecheck-error/arity :fun-name fun)              
              append (signature-reqs signature) into reqs
              collect (list type (signature-type signature)) into eqs
              append (typing-equations typing) into eqs
              finally (multiple-value-bind (signature substs) (unify (make-typing (make-signature type reqs) eqs))
                        (apply-typetable typetable substs)
                        (return signature)))))))

(defun typing-from-function-src (ctxt typetable formals body)
  (declare (symbol-table ctxt) (hash-table typetable) (list formals) (pnode body))
  (with-symbol-table ctxt
    (let ((typings/formal (loop for formal in formals collect (typing-from-expr ctxt typetable formal :formalp t)))
          (typing/body (typing-from-expr ctxt typetable body)))
      (make-typing (make-signature `(fun ,@(mapcar #'(lambda (typing/formal) (signature-type (typing-signature typing/formal))) typings/formal)
                                         ,(signature-type (typing-signature typing/body)))
                                   (append (mapcan #'(lambda (typing/formal) (signature-reqs (typing-signature typing/formal))) typings/formal)
                                           (signature-reqs (typing-signature typing/body))))
                   (append (mapcan #'typing-equations typings/formal)
                           (typing-equations typing/body))))))

(defun typing-from-expr (ctxt typetable expr &key formalp)
  (declare (symbol-table ctxt) (hash-table typetable) (pnode expr) (boolean formalp))
  (labels ((typing-from-apply (typing/fun actuals)
             (declare (typing typing/fun) (list actuals))
             (loop for type/return = (make-typevar)
                   for actual in actuals
                   for typing/actual = (typing-from-expr ctxt typetable actual :formalp formalp)
                   append (typing-equations typing/actual) into eqs
                   append (signature-reqs (typing-signature typing/actual)) into reqs
                   collect (signature-type (typing-signature typing/actual)) into types/actual
                   finally (return (make-typing (make-signature type/return (append reqs (signature-reqs (typing-signature typing/fun))))
                                                (cons (list (curry-type `(fun ,@types/actual ,type/return))
                                                            (curry-type (signature-type (typing-signature typing/fun))))
                                                      (append eqs (typing-equations typing/fun))))))))          
    (let ((typing
           (case (pnode-symbol expr)
             ((lambda)
              (when formalp
                (error 'typecheck-error/pattern :pattern expr))
              (typing-from-function-src ctxt typetable (pnode-children expr :formals) (pnode-child expr :body)))

             ((let)
              (when formalp
                (error 'typecheck-error/pattern :pattern expr))
              (with-symbol-table ctxt
                (loop for let-decl in (pnode-children expr :decls)
                      for let-name = (pnode-symbol let-decl)
                      do (symbol-table-add ctxt let-name (make-typevar)))
                (loop for let-decl in (pnode-children expr :decls)
                      for let-name = (pnode-symbol let-decl)
                      for let-expr = (pnode-child let-decl :body)
                      for type = (symbol-table-get ctxt let-name)
                      for typing/expr = (typing-from-expr ctxt typetable let-expr)
                      collect (list type (signature-type (typing-signature typing/expr))) into eqs
                      append (typing-equations typing/expr) into eqs
                      append (signature-reqs (typing-signature typing/expr)) into reqs
                      finally (return
                                (let ((typing/body (typing-from-expr ctxt typetable (pnode-child expr :body))))
                                  (make-typing (make-signature (signature-type (typing-signature typing/body))
                                                               (append (signature-reqs (typing-signature typing/body)) reqs))
                                               (append (typing-equations typing/body) eqs)))))))
            
             ((:wildcard)
              (unless formalp
                (error 'typecheck-error/wildcard :expr expr))
              (make-typing (make-signature (make-typevar))))
            
             ((apply)
              (when formalp
                (error 'typecheck-error/pattern :pattern expr))
              (let ((typing/fun (typing-from-expr ctxt typetable (pnode-child expr :fun) :formalp formalp)))
                (typing-from-apply typing/fun (pnode-children expr :actuals))))
            
             (otherwise
              (cond ((constructor-p (pnode-symbol expr))
                     ;; TODO
                     (let ((signature/cons (signature-from-constructor expr)))
                       (typing-from-apply (make-typing signature/cons) (pnode-children expr :actuals))))
                    
                    ((function-p (pnode-symbol expr))
                     (let ((fun-name (pnode-symbol expr)))
                       (let ((signature (signature-from-function fun-name)))
                         (make-typing (instantiate-signature
                                       (if (virtual-function-p fun-name)
                                           (make-signature (signature-type signature) (cons (list fun-name (get-virtual-discriminator fun-name))
                                                                                            (signature-reqs signature)))
                                           signature))))))
                   
                    (t
                     (if formalp
                         (let ((typevar (make-typevar)))
                           (handler-case (progn
                                           (symbol-table-add ctxt (pnode-symbol expr) typevar)
                                           (make-typing (make-signature typevar)))
                             (symbol-table-conflict ()
                               (error 'typecheck-error/formal-conflict :pattern expr))))
                         (let ((typevar (symbol-table-get ctxt (pnode-symbol expr))))
                           (if typevar (make-typing (make-signature typevar))
                               (error 'typecheck-error/untyped :expr expr))))))))))
      (unless (gethash expr typetable)
        (setf (gethash expr typetable) (typing-signature typing)))
      typing)))