;;-*- Mode:LISP; Package:VERIFICATION-INTERNALS; Base:8 -*-
;; (C) Copyright 1983 LispMachineInc.
;; 11/08/83 11:13:01 -George Carrette

;; Copyright LISP Machine, Inc. 1984
;;   See filename "Copyright" for
;; licensing and release information.

;; A kind of BATCH processing of a file of lisp expressions, with "log output"
;; to file and terminal.

(defvar *showtime? nil)
(defvar *comment* nil)

(defvar *verify-file-comment* nil)


(defun (:property :verify-file fs:file-attribute-bindings) (ignore ignore value)
  (values (list '*verify-file-comment*)
	  (list value)))

(defun verify-file (&optional (input-filename "")
		    &key (output-filename "") (terminal-stream terminal-io)
		    (comment nil)
		    (showtime? nil) (driver 'verify-stream))
  "Reads expressions from the <input-filename>, evaluates them in the usual
load environment, and prints the results as in a read-eval-print loop.
Input and output is echoed to the <output-filename> and//or the <terminal-stream>.
Example: (verify-file /"ED:TEST.LISP/" :Output-filename /"ED-BUFFER:TEST.OUT/"."

  (or (get driver 'verify-pathname-defaults)
      (setf (get driver 'verify-pathname-defaults) (fs:make-pathname-defaults)))
  (if terminal-stream (send terminal-stream ':fresh-line))
  (let ((input-filename (fs:merge-pathname-defaults input-filename
						    (get driver 'verify-pathname-defaults)))
	(*showtime? showtime?)
	(*comment* comment))
    (with-open-stream (input-stream
			(file-retry-new-pathname (input-filename fs:file-error)
			  (send input-filename ':open-canonical-default-type ':LISP)))
      (setq input-filename (or (send input-stream ':pathname)
			       (fs:parse-pathname input-filename)))
      (fs:set-default-pathname input-filename (get driver 'verify-pathname-defaults))
      (let ((GENERIC-PATHNAME (SEND INPUT-FILENAME ':GENERIC-PATHNAME)))
	(FS:READ-ATTRIBUTE-LIST GENERIC-PATHNAME INPUT-STREAM)
	(MULTIPLE-VALUE-BIND (VARS VALS) (FS:FILE-ATTRIBUTE-BINDINGS GENERIC-PATHNAME)
	  (PROGV VARS VALS
	    (if output-filename
		(with-open-file (output-stream (send (fs:merge-pathname-defaults
						       output-filename
						       input-filename)
						     ':new-type "OUT")
					       ':OUT)
		  (funcall driver input-stream output-stream terminal-stream))
	      (funcall driver input-stream () terminal-stream))))))))

(defun verify-stream (input-stream  &rest output-streams)
  (let ((output-stream (apply #'make-broadcast-stream (delq () (copylist output-streams)))))
      (format output-stream
	      "; Verification of ~A by ~A using ~A~%;"
	      (send input-stream ':truename)
	      user-id
	      si:local-host-name)
      (time:print-current-date output-stream)
      (terpri output-stream)
      (when *comment*
	(princ *comment* output-stream)
	(terpri output-stream))
      (when *verify-file-comment*
	(format output-stream "~&Extra-Filename-Information ~A~%" *verify-file-comment*))
      (si:describe-system-versions output-stream)
      (terpri output-stream)
      (verify-repl (make-verify-stream input-stream output-stream) output-stream)))

(defconst *other-output-streams* '(error-output trace-output))

(defun verify-repl (standard-input standard-output)
  (progv *other-output-streams*
	 (circular-list standard-output)
    (let ((time-before-everything (time))
	  (time-eval-total 0))
      (do ((form)(eofp (list ()))(eval-time-inc))
	  ((eq (setq form (read standard-input eofp)) eofp))
	(unwind-protect
	    ;; maybe add some condition handling here. handle sys:abort etc
	    ;; like in a lisp listener.
	    (let ((time-before-eval (time)))
	      (setq * (eval form))
	      (let ((time-after-eval (time)))
		(setq eval-time-inc  (time-difference time-after-eval time-before-eval))
		(setq time-eval-total (+ time-eval-total eval-time-inc))))
	  (setq + form))
	(if *showtime?
	    (format standard-output "~&; Evaluation took ~S seconds." (// eval-time-inc 60.0)))
	(print * standard-output))
      (let ((time-after-everything (time)))
	(let ((time-total-total (time-difference time-after-everything
						 time-before-everything)))
	  (let ((tet (funcall (get ':realtime 'measure-convert) time-eval-total))
		(ttt (funcall (get ':realtime 'measure-convert) time-total-total)))
	    (format standard-output
		    "~&; End of test.~%; ~S seconds realtime total, ~S during evaluation.~%"
		    ttt tet)
	    (list (send standard-input ':truename)
		  ':total-realtime ttt
		  ':eval-realtime tet)))))))


;; this bidirection broadcast-stream hack could go with other system I/O functions.

;; i guess i really should be using flavorized streams here, even if it is hairier
;; to do so.

(defvar *verify-input-stream*)
(defvar *verify-output-stream*)
(defvar *verify-untyi-char*)

(defun verify-stream-closure-function (operation &optional arg1 &Rest args)
  (selectq operation
    (:which-operations
     '(:tyi :untyi :tyipeek))
    ((:tyi :tyipeek)
     (let (c)
       (if (null *verify-untyi-char*)
	   (or (eq arg1 (setq c (send *verify-input-stream* ':tyi arg1)))
	       (send *verify-output-stream* ':tyo c))
	 (setq c *verify-untyi-char*))
       (setq *verify-untyi-char* (and (eq operation ':tyipeek) c))
       c))
    (:untyi
     (setq *verify-untyi-char* arg1))
    (:truename
     (send *verify-input-stream* ':truename))
    (:otherwise
     (stream-default-handler #'verify-stream-closure-function operation arg1 args))))

(defun make-verify-stream (input-from output-to)
  "Makes a kind of bi-directional broadcast stream"
  (let ((*verify-input-stream* input-from)
	(*verify-output-stream* output-to)
	(*verify-untyi-char* ()))
  (closure '(*verify-input-stream* *verify-output-stream* *verify-untyi-char*)
	   #'verify-stream-closure-function)))