;;; $Id: typedscm-tool.ss,v 1.18 2006/01/29 01:50:01 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.

;;; AUTHOR: adapted by Gary T. Leavens from ../eopl/eopl-tool.ss,
;;;         extended by Brian Dorn to integrate the typechecker with
;;;           DrScheme GUI.

(module typedscm-tool mzscheme
  (require

   ;; Requires for being able to type-check things
   (lib "tc-scheme-parser.scm" "typedscm")
   (lib "tc-scheme-annotate.scm" "typedscm")
   (lib "tc-types.scm" "typedscm")
   (lib "tc-env.scm" "typedscm")
   (lib "displayln-mod.scm" "typedscm")
   (lib "tc-error-output.scm" "typedscm")
   (lib "tc-position.scm" "typedscm")
   (lib "tc-type-translate.scm" "typedscm")
   (lib "tc-type-check-and-eval-loop.scm" "typedscm")
   (lib "tc-util.scm" "typedscm")

   ;; Requires for the tool definition
   (lib "mred.ss" "mred")
   (lib "bitmap-label.ss" "mrlib")
   (lib "framework.ss" "framework")
   (lib "list.ss")
   (lib "unitsig.ss")
   (lib "class.ss")
   (lib "tool.ss" "drscheme")
   (lib "string-constant.ss" "string-constants"))
  
  (provide tool@)

  (define tool@
    (unit/sig drscheme:tool-exports^
      (import drscheme:tool^)

      ;; Stuff for setting up the language in the menus etc.
      (define language-base%
	(class* object% (drscheme:language:simple-module-based-language<%>)
	  (define/public (get-language-numbers)
	    '(-500 -300))
	  (define/public (get-language-position)
	    (list (string-constant teaching-languages)
                  "Typedscm, typed extension to EoPL(2e)"))
	  (define/public (get-module)
	    '(lib "typedscm.ss" "typedscm"))
	  (define/public (get-one-line-summary)
	    "A type notation for the Friedman, Wand, and Haynes text")
          (define/public (get-language-url)
	    "http://www.cs.iastate.edu/~leavens/typedscm/")
	  (define/public (get-reader)
	    (lambda (name port)
	      (let ([v (read-syntax name port)])
		(if (eof-object? v)
		    v
		    (namespace-syntax-introduce v)))))
	  (super-instantiate ())))

      ;; Stuff for manipulating the read-eval-print loop and initialization.
      ;; The most important initialization is to set up eopl-error-stop
      ;; which is done in on-execute below.
      (define language%
	(class (drscheme:language:module-based-language->language-mixin
		(drscheme:language:simple-module-based-language->module-based-language-mixin
		 language-base%))
	  (define/override (use-namespace-require/copy?) #t)
	  (define/override (on-execute settings run-in-user-thread)
	    (super on-execute settings run-in-user-thread)
	    (run-in-user-thread
	     (lambda ()
	       ((namespace-variable-value 'install-eopl-exception-handler)))))
	  (super-instantiate ())
          )
        )

      ;; The follow is for the GUI in the definitions window.
      (define unit-frame-mixin
	(mixin ((class->interface drscheme:unit:frame%)) ()
	       (inherit get-button-panel
			get-interactions-text
			get-definitions-text
			get-definitions-canvas
			begin-container-sequence
			end-container-sequence)

	       (super-instantiate ())

               (define get-filename
                 (lambda ()
                   ;; ENSURES: Result is the filename of the
                   ;; definitions window editor, if any
                   (let ((fn (send (get-definitions-text) get-filename #f)))
                     (if (eqv? fn #f)
                         "<definitions>"
                         (path->string fn)))))

	       ;; sets the current-directory
	       ;; and current-load-relative-directory
	       ;; based on the file saved in the definitions-text
	       (define/private (set-directory definitions-text)
		 (let* ([tmp-b (box #f)]
			[fn (send definitions-text get-filename tmp-b)])
		   (unless (unbox tmp-b)
			   (when fn
				 (let-values
				  ([(base name dir?) (split-path fn)])
				  (current-directory base)
				  (current-load-relative-directory base))))))
 
          
	       (define type-check-callback
		 (lambda (b e)
                   ;; EFFECT: Run the type checker on the
                   ;; definitions window.
                   ;; [[[TODO: look at ../drscheme/syncheck.ss
                   ;; to see how to output errors better.]]]
                   
		   ;; Setup the parser so we get nice positions
		   (set-directory (get-definitions-text))
		   (tc:start-input-filename! (get-filename))

		   ;; Typecheck the teachpacks that are loaded.
		   ;; However, this doesn't work on files that don't type check
		   ;; (like ../lib342/drscheme-342-teachpack.scm)
		   ;; so it's currently disabled.
		   ;;(for-each
		   ;; (lambda (path)
		   ;;   (type-check-and-require-file
                   ;;    (path->string path)))
		   ;; (drscheme:teachpack:teachpack-cache-filenames
		   ;;  (preferences:get 'drscheme:teachpacks)))

		   ;; Typecheck program
		   (let* ((scheme-pgm
			   (tc:character-string-program-parser
			    (send (get-definitions-text)
				  get-text 0 'eof #f #f)))
			  (result-type
			   (tc:annotation->type
			    (tc:scheme-top-level-annotate (tc:env-empty)
							  scheme-pgm)))
                          (is-error (tc:error-type-expr? result-type)))
                     (displayln "vvvvvvvv BEGIN "
                                (if is-error "ERROR" "SUCCESS")
                                " REPORT vvvvvvvvvv")
		     (cond
                       (is-error
			   (tc:output-error-message result-type))
                       ((tc:declaration-type-expr? result-type)
                        (tc:display-type-env 
                         (tc:declaration-type-expr->env result-type)))
                       (else
                        (display "<Definitions> : ")
                        (tc:displayln-output-type (tc:type-unparse result-type))))
                     (displayln "^^^^^^^^ END "
                                (if is-error "ERROR" "SUCCESS")
                                " REPORT ^^^^^^^^^^^")
                     (newline)
                     ) ;; end let

		   ;; Cleanup parser so things work next time
		   (tc:end-input-filename!)
		   ))
	       
               ;; Add the "Type Check" button to the panel
	       (send (get-button-panel) begin-container-sequence)
	       (define type-check-button
		 (let ((bo (make-bitmap-label
			    "Type Check"
			    (build-path (collection-path "typedscm")
					"typedscm-icon-small.gif"))))
		   (instantiate button% ()
				(label bo)
				(parent (get-button-panel))
			      (callback
			       (lambda (b e) (type-check-callback b e))))))
	       (send (get-button-panel) change-children
		     (lambda (loc)
		       (cons type-check-button
			     (filter
			      (lambda (c)
				(not (eq? type-check-button c))) loc))))
	       (send (get-button-panel) end-container-sequence)
	       ))

      ;; Start the tool running
      (define (phase1)
        (void))
      (define (phase2)
	(drscheme:language-configuration:add-language 
	 (make-object ((drscheme:language:get-default-mixin) language%))))

      (drscheme:get/extend:extend-unit-frame unit-frame-mixin)
      )
    )
  )