;;; $Id: tc-error-output.scm,v 1.28 2006/04/04 17:33:59 leavens Exp $
;;; Copyright (C) 2006 Iowa State University
;;;
;;; This file is part of Typedscm.
;;;
;;; This library is free software; you can redistribute it and/or
;;; modify it under the terms of the GNU Lesser General Public License
;;; as published by the Free Software Foundation; either version 2.1,
;;; of the License, or (at your option) any later version.
;;;
;;; This library is distributed in the hope that it will be useful,
;;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
;;; Lesser General Public License for more details.
;;;
;;; You should have received a copy of the GNU Lesser General Public
;;; License along with Typedscm; see the file LesserGPL.txt.  If not,
;;; write to the Free Software Foundation, Inc., 51 Franklin St, Fifth
;;; Floor, Boston, MA 02110-1301 USA.

(module tc-error-output (lib "typedscm.ss" "typedscm")

(provide tc:output-error-message tc:displayln-output-type)

(require (lib "tc-types.scm" "typedscm")
         (lib "tc-type-translate.scm" "typedscm")
         (lib "tc-util.scm" "typedscm")
         (lib "tc-position.scm" "typedscm")
         (lib "tc-scheme-abstract-syntax.scm" "typedscm")
         (lib "tc-scheme-unparser.scm" "typedscm")
         (lib "tc-output-type-expr.scm" "typedscm"))

(define tc:output-error-message
  (lambda (err)
    (tc:output-error-record-message (tc:error-type-expr->error-record err))))


(define tc:output-error-record-message
  (lambda (err-rec)
    (cases tc:error-record err-rec
	   (tc:varref-error-record
	    (syn)
	    (cases tc:scheme-exp syn
		   (tc:varref
		    (position variable)
		    (tc:small-error
		     (tc:position->error-string position)
		     "Unknown variable: "
		     (symbol->string variable)))
		   (else (error "Invalid syntax for error"))))
	   (tc:composite-error-record
	    (errors)
	    (map tc:output-error-record-message errors))
	   (tc:badtest-error-record
	    (test-record)
	    (cases tc:error-record test-record
		   (tc:mismatch-error-record
		    (syn expected inferred)
		    (tc:small-report
		     "Wrong type for test expression"
		     "Test expression"
		     syn
		     "Expected"
		     (tc:type-unparse expected)
		     "Inferred"
		     (tc:type-unparse inferred)))
		   (else (error "Bad test-record!"))))
	   (tc:duplicate-let-binding-error-record
	    (syn dups)
	    (tc:small-error
	     (tc:position->error-string (tc:scheme-syntax->position syn))
	     "Repeated declaration of variable names"
	     (string-append
	      tc:nl-indent "Repeatedly declared variable names(s): ")
	     dups))
	   (tc:defined-lambda-mismatch-error-record
	    (syn declared-type)
	    (tc:smaller-report
	     "Procedure definition does not match existing type declaration"
	     "Procedure"
	     syn
	     "Declared type"
	     (tc:type-unparse declared-type)
	     (cond
	      ((tc:intersection-type-expr? declared-type)
	       (string-append
		"The type checker requires you to use has-type-trusted "
		"for definitions with all-of (intersection) types."))
	      ((not (tc:function-type-expr? declared-type))
	       (string-append "Declared type must be a function type "
			      "with the same number of arguments."))
	      (else ""))))
	   (tc:named-lambda-subtyping-error-record
	    (syn name declared-type)
	    (tc:smaller-report
	     (string-append
	      "Definition of procedure "
	      (symbol->string name)
	      " does not match existing type declaration")
	     "Offending procedure"
	     syn
	     "Declared type"
	     (tc:type-unparse declared-type)
	     "The body's type must be a subtype of the declared return type."
	     ))
	   (tc:cases-clause-bad-fields-error-record
	    (syn fields fields-types)
	    (let ((dups (tc:find-duplicates fields)))
	      (if (not (null? dups))
		  ;; Repeated declaration
		  (tc:small-error
		   (tc:position->error-string (tc:scheme-syntax->position syn))
		   "Repeated declaration of variable names in cases clause"
		   (string-append
		    tc:nl-indent "Repeatedly declared variable names(s): ")
		   dups)
		  ;; Mismatch in number of fields
		  (tc:small-error
		   (tc:position->error-string (tc:scheme-syntax->position syn))
		   "Mismatch in number of fields to cases clause"
		   (string-append
		    tc:nl-indent "Clause: ")
		   (tc:unparse-scheme-syntax syn)
		   (string-append
		    tc:nl-indent "Number of fields from define-datatype: ")
		   (length fields-types)
		   (string-append
		    tc:nl-indent "Number of fields from clause: ")
		   (length fields)))))
	   (tc:cases-on-non-variant-error-record
	    (syn sym)
	    (tc:small-error
	     (tc:position->error-string (tc:scheme-syntax->position syn))
	     "Cases called with non-variant type as argument"
	     (string-append
	      tc:nl-indent "Offending argument type name: " (symbol->string sym))))
	   (tc:cases-with-bad-clause-usage-error-record
	    (syn variant-type)
	    (tc:small-error
	     (tc:position->error-string (tc:scheme-syntax->position syn))
	     "Improper clause usage in cases statement"
	     (string-append
	      tc:nl-indent "A case must appear for each variant without duplicates.")))
	   (tc:if-subtype-error-record
	    (left-exp left-type right-exp right-type)
	    (tc:different-types-report
	     "Arms of if expression have different types"
	     "Left  arm"
	     left-exp
	     "Right arm"
	     right-exp
	     (tc:type-unparse left-type)
	     (tc:type-unparse right-type)))
	   (tc:mismatch-error-record
	    (syn expected inferred)
	    (tc:small-report
	     "Type mismatch between inferred and expected types"
	     "Syntax"
	     syn
	     "Expected"
	     (tc:type-unparse expected)
	     "Inferred"
	     (tc:type-unparse inferred)))
	   (tc:op-arg-mismatch-error-record
	    (oper-exp args-list operator-type args-types)
	    (tc:application-small-report
	     "Operator and argument types don't match"
	     "Offending call" oper-exp args-list
	     "Operator type "
	     (tc:type-unparse operator-type)
	     "Argument type list"
	     (map tc:type-unparse args-types)))
	   (tc:apply-non-proc-error-record
	    (exp type)
	    (tc:smallest-report
	     "Attempt to apply non-procedure"
	     "Not a procedure"
	     exp
	     "Inferred type"
	     (tc:type-unparse type)))
	   (tc:duplicate-formals-error-record
	    (sfs dups)
	    (tc:small-error
	     (tc:position->error-string (tc:scheme-syntax->position sfs))
	     "Duplicate formal parameters: " dups
	     (string-append tc:nl-indent "Offending formals: ")
	     (tc:unparse-scheme-formals sfs)))
	   (tc:non-void-body-error-record
	    (syn inferred)
	    (tc:small-report
	     "If statement (no false part) has body with non-void type"
	     "Offending body" syn
	     "Expected" "void"
	     "Inferred" (tc:type-unparse inferred)))
	   (tc:set!-mismatch-error-record
	    (variable exp decl-type inf-type)
	    (tc:small-report
	     (string-append
	      "Type mismatch in set! between variable '"
	      (symbol->string variable)
	      "' and expression")
	     "Offending expression" exp
	     "Declared" (tc:type-unparse decl-type)
	     "Inferred" (tc:type-unparse inf-type)))
	   (tc:cond-clauses-mismatch-error-record
	    (exp clause-types)
	    (tc:small-error
	     (tc:position->error-string (tc:scheme-syntax->position exp))
	     "Clauses of cond expression have different types"
	     (string-append tc:nl-indent "Inferred clause types: ")
	     (map tc:type-unparse clause-types)))
	   (tc:cases-clauses-mismatch-error-record
	    (exp clause-types)
	    (tc:small-error
	     (tc:position->error-string (tc:scheme-syntax->position exp))
	     "Clauses of cases expression have different types"
	     (string-append tc:nl-indent "Inferred clause types: ")
	     (map tc:type-unparse clause-types)))
	   (tc:has-type-mismatch-error-record
	    (exp decl-type inf-type)
	    (tc:small-report
	     "Expression inside has-type is not a subtype of the given type"
	     "Offending expression"
	     exp
	     "Expected"
	     (tc:type-unparse decl-type)
	     "Inferred"
	     (tc:type-unparse inf-type)))	    
	    (tc:forall-bad-body-error-record
	     (exp inf-type exp-type)
	     (tc:small-report
	      "Body expression in a forall is not a type predicate"
	      "Offending body expression"
	      exp
	      "Expected"
	      (tc:type-unparse exp-type)
	      "Inferred"
	      (tc:type-unparse inf-type)))

	    (tc:define-type-mismatch-error-record
	     (variable exp type)
	     (tc:smaller-report
	      (string-append
	       "Type mismatch in define of variable '"
	       (symbol->string variable)
	       "' and expression")
	      "Offending definition"
	      exp
	      "Inferred"
	      (tc:type-unparse type)
	      "Refer to a previous definition expression for expected type"))
	    (tc:define-datatype-name-conflict-error-record
	     (syn type-name)
	     (tc:small-error
	      (tc:position->error-string (tc:scheme-syntax->position syn))
	      "Define-datatype's type-name already used in environment"
	      (string-append
	       tc:nl-indent "Type-name: ")
	      type-name))
	    (tc:unknown-module-error-record
	     (syn mod-name)
	     (tc:small-error
	      (tc:position->error-string (tc:scheme-syntax->position syn))
	      "Unknown module-name used in require form"
	      (string-append
	       tc:nl-indent "Module name: ")
	      mod-name))
	    (tc:bad-file-error-record
	     (pos path)
	     (tc:small-error
	      (tc:position->error-string pos)
	      "File is not readable (perhaps the path is wrong)"
	      (string-append
	       tc:nl-indent "File path: ")
	      path))
	    (tc:deftype-redeclaration-error-record
	     (syn identifier)
	     (tc:small-error
	      (tc:position->error-string (tc:scheme-syntax->position syn))
	      "Deftype redeclaration for identifier already bound in the current environment"
	      (string-append
	       tc:nl-indent "Identifier: ")
	      identifier
	      (string-append
	       tc:nl-indent "You may need to use (type-check-reset-env!) to clean up old definitions.")
	      ))
	    (tc:module-missing-deftype-error-record
	     (syn mod-name path)
	     (tc:small-error
	      (tc:position->error-string (tc:scheme-syntax->position syn))
	      "A required module definition is missing one or more deftypes for provided identifiers"
	      (string-append
	       tc:nl-indent "Module: ")
	      mod-name
	      (string-append
	       tc:nl-indent "Module Path: ")
	      path))
	    
	    ;; For testing, commented out so that we don't see generic errors
	    ;; when a file has multiple errors.
	    ;;(tc:simple-error-record
	    ;; (msg)
	    ;; (displayln msg))

	   (else (error "tc:output-error-message-record has no case for: "
			err-rec)))))


;;[[[FIXME: correct deftype]]]
(deftype tc:small-report
  (-> (string string tc:scheme-exp string tc:output-type-expr
	      string tc:output-type-expr)
      void))
(define tc:small-report
  (lambda (context-msg exp-label-msg syn left-desc left-type right-desc right-type)
    ;; EFFECT: print a small-error report, but
    ;; only print the error if we haven't printed something for a subpart
    (if (not (or (tc:output-error-type? left-type)
		 (tc:output-error-type? right-type)))
	(tc:small-error
	 (tc:position->error-string (tc:scheme-syntax->position syn))
	 context-msg
	 (string-append tc:nl-indent exp-label-msg ": ")
	 (tc:unparse-watching-for-body syn)
	 (string-append tc:nl-indent left-desc ": ")
	 left-type
	 (string-append tc:nl-indent right-desc ": ")
	 right-type))))

(deftype tc:unparse-watching-for-body
  (-> (datum) datum))
(define tc:unparse-watching-for-body
  (lambda (syn)
    ;; unparse in such a way as to make bodies look good if presented alone
    (let ((unparsed-syn (tc:unparse-scheme-syntax syn)))
      (if (not (tc:scheme-body? syn))
	  unparsed-syn
	  (if (= (length unparsed-syn) 1)
	      ;; unwrap it, so doesn't look strange
	      (car unparsed-syn)
	      (cons 'begin unparsed-syn))))))

(deftype tc:smaller-report
  (-> (string string tc:scheme-exp string tc:output-type-expr
	      string)
      void))
(define tc:smaller-report
  (lambda (context-msg exp-label-msg syn left-desc left-type desc)
    ;; EFFECT: print a small-error report, but
    ;; only print the error if we haven't printed something for a subpart
    (if (not (tc:output-error-type? left-type))
	(tc:small-error
	 (tc:position->error-string (tc:scheme-syntax->position syn))
	  context-msg
	 (string-append tc:nl-indent exp-label-msg ": ")
	 (tc:unparse-watching-for-body syn)
	 (string-append tc:nl-indent left-desc ": ")
	 left-type
	 (string-append tc:nl-indent desc)
	 ))))

(define tc:smallest-report
  (lambda (context-msg exp-label-msg syn left-desc left-type)
    ;; EFFECT: print a small-error report, but
    ;; only print the error if we haven't printed something for a subpart
    (if (not (tc:output-error-type? left-type))
	(tc:small-error
	 (tc:position->error-string (tc:scheme-syntax->position syn))
	  context-msg
	 (string-append tc:nl-indent exp-label-msg ": ")
	 (tc:unparse-watching-for-body syn)
	 (string-append tc:nl-indent left-desc ": ")
	 left-type
	 ))))

(deftype tc:small-error (-> (datum ...) void))
(define tc:small-error
  (lambda args
    (apply displayln args)))
	    
(deftype tc:different-types-report
  (-> (string string tc:scheme-exp string tc:scheme-exp
	      tc:output-type-expr tc:output-type-expr)
      void))
(define tc:different-types-report
  (lambda (context-msg left-msg left-exp right-msg right-exp
		       left-type-out right-type-out)
    (if (not (or (tc:output-error-type? left-type-out)
		 (tc:output-error-type? right-type-out)))
	(tc:small-error
	 (tc:position->error-string (tc:scheme-exp->position left-exp))
	 context-msg
	 (string-append tc:nl-indent
			(tc:position->error-lines-string
			 (tc:scheme-exp->position left-exp))
			left-msg ": ")
	 (tc:strings-with-quotes (tc:unparse-scheme-exp left-exp))
	 (string-append tc:nl-indent
			(tc:position->error-lines-string
			 (tc:scheme-exp->position right-exp))
			right-msg ": ")
	 (tc:strings-with-quotes (tc:unparse-scheme-exp right-exp))
	 (string-append tc:nl-indent left-msg "'s type: ")
	 left-type-out
	 (string-append tc:nl-indent right-msg "'s type: ")
	 right-type-out))))

(deftype tc:application-small-report
  (-> (string string tc:scheme-exp string tc:output-type-expr
	      string (list-of tc:output-type-expr))
      void))
(define tc:application-small-report
  (lambda (context-msg exp-label-msg oper-exp args-list
		   left-desc left-type right-desc right-type-ls)
    ;; EFFECT: print a small-error report, but
    ;; only print the error if we haven't printed something for a subpart
    (tc:small-error
     (tc:position->error-string (tc:scheme-exp->position oper-exp))
     context-msg
     (string-append tc:nl-indent exp-label-msg ": ")
     (map tc:strings-with-quotes (cons (tc:unparse-scheme-exp oper-exp)
				       (map tc:unparse-scheme-exp args-list)))
     (string-append tc:nl-indent left-desc ": ")
     left-type
     (string-append tc:nl-indent right-desc ": ")
     right-type-ls)))

(deftype tc:strings-with-quotes (-> (datum) datum))
(define tc:strings-with-quotes
  (lambda (x)
    ;; EFFECT: Return a datum that is like x, but if x is a string,
    ;;         the returned string is such that the string when displayed
    ;;         looks as if it would look when written using write.
    ;; [[[Bug: This should account for internal double quotes in strings
    ;;    and put out a string that shows a backslash in front of them.]]]
    (cond
     ((string? x)
      (has-type datum (string-append "\"" (test-type string? x) "\"")))
     ((list? x)
      (has-type datum (map tc:strings-with-quotes
			   (test-type (list-of datum?) x))))
     (else x))))

(deftype tc:cannot-be-typed string)
(define tc:cannot-be-typed "cannot be typed")

(deftype tc:displayln-output-type (-> (tc:output-type-expr) void))
(define tc:displayln-output-type
  (lambda (ot)
    (if (tc:output-error-type? ot)
	(displayln tc:cannot-be-typed)
	(displayln ot))))

(deftype tc:output-error-type? (-> (tc:output-type-expr) boolean))
(define tc:output-error-type?
  (lambda (typ)
    (tc:occurs-in-output-type-expr? 'type-error typ)))

) ;; end module