;;; -*- Syntax:Common-Lisp; Mode: LISP; Package: (TMS Lisp 1000.); Base: 10. -*-

(in-package 'tms)

"(c) Copyright 1986, 1987, 1988 Xerox Corporation.  All rights reserved.  Subject to
the following conditions, permission is granted to use and copy this
software and to prepare derivative works:  Such use, copying or
preparation of derivative works must be for non-commercial research or
educational purposes; each copy or derivative work must include this
copyright notice in full; a copy of each completed derivative work must
be returned to:  DEKLEER@XEROX.COM (Arpanet) or Johan de Kleer,
Xerox PARC, 3333 Coyote Hill Road, Palo Alto, CA 94304.  This software
is made available AS IS, and Xerox Corporation makes no warranty about
the software or its performance."

(defun begin-trace (file &optional (dump nil) (init-tms T) (reuse T))
  (when *trace-file*
    (error "Opening new trace file when old one hasn't been closed."))
  (setq *dump* nil)
  (if init-tms (init-tms reuse))
  (setq *trace-file* (open file :DIRECTION :OUTPUT)
	*dump* dump)
  (format *trace-file*
	  ";;; -*- Syntax:Common-Lisp; Mode: LISP; Package: (TMS Lisp 1000.); Base: 10. -*-")
  (format *trace-file*
	  "~%;;; *h4* = ~A, *h45* = ~A"
	  *h4* *h45*)
  (format *trace-file* "~%VERSION ~D" *version*)
  )

(defun end-trace ()
  (when *trace-file*
    (if *dump* (dump))
    (format *trace-file* "~%END~%")
    (close *trace-file*)
    (setq *trace-file* nil)))

(defun trace-node (n-a &optional (trace-file *trace-file*))
  (if (assumption? n-a)
      (format trace-file "(A . ~D)" (assumption-unique n-a))
      (format trace-file "(N . ~D)" (n-a-unique n-a))))

;;; Note that with some exotic switch settings the node numbers may change as
;;; the ATMS itself is creating various things.  Therefore we need our own maps.

(defvar *replay-node-array* nil)			; For faster unique->node mappings.

(defvar *replay-class-array* nil)			

(defvar *replay-assumption-array* nil)

(defmacro meter (flag form)
  #+Symbolics `(if ,flag (meter:with-monitoring nil ,form) ,form)
  #-Symbolics form
  )

(defmacro reset-meter (flag)
  #+Symbolics `(if ,flag (meter:with-monitoring T nil))
  #-Symbolics nil
  )

(defmacro meter-report (flag)
  #+Symbolics `(if ,flag (meter:report))
  #-Symbolics nil
  )

(defun dump ()
  (walk-nodes
    #'(lambda (n)
#+Symbolics	
	(declare (sys:downward-function))
	(dump-n-a n)))
  (dolist (a *assumptions*)
    (dump-n-a a)))

(defun dump-n-a (n-a)
  (cond ((i-false? n-a) (false? n-a))
	((i-true? n-a) (true? n-a))
	((i-out? n-a) (out? n-a))
	(t (label n-a))))

(defvar *tokens*)

(defvar *saved-tokens*)

(defun next-token () (pop *tokens*))
  
;;; This really assumes INIT-TMS is the first thing in the file, and END is the last.
(defun replay (file &optional meter-p (check T)  profile define
	       &aux *tokens* token (*package* (find-package 'TMS)) output)
  #+Symbolics
  (and (null check)
       sys:gc-on
       (format T "~% Warning GC status is ~A" sys:gc-on))
  (with-open-file (input file)
    (do nil (nil)
      (setq token (read input))
      (push token *tokens*)
      (if (eq token 'END) (return))))
  (setq *tokens* (nreverse *tokens*))
  (setq output *standard-output*)
  (format output "~% Replaying ~A" file)
  #+Symbolics (si:print-herald :STREAM output)
  (format T "~% Replaying on version ~D of the ATMS" *version*)
  (setq *saved-tokens* *tokens*)
  (if profile
      (format T "~% Do :profile (profile-replay)")
      (time (replay-it output meter-p check define))))

(defun profile-replay (&optional meter-p check define &aux *tokens*)
  (setq *tokens* *saved-tokens*)
  (replay-it *standard-output* meter-p check define))

(defun replay-it (output meter-p check define
		  &aux command n start-time m u j (version 0) last-command check-labels
		       update-atms)
  ;; Useful for debugging.
  last-command

  ;; Convention soon should be *foci*=NIL means focussing is not used.
  (setq *foci* nil)

  (if check (setq define T))
  
  (unless *simple-hybrid* (setq check-labels check))

  (do nil (nil)
    (setq last-command *tokens*
	  command (next-token)
	  update-atms T)
    (selectq command
      (START (setq start-time (get-internal-run-time) update-atms nil))
      (INIT-TMS (when start-time (replay-end output start-time meter-p))
		(format T "~% Replay is initializing the ATMS")
		(zf *replay-node-array*
		    (fill *replay-node-array* nil)
		    (setq *replay-node-array*
			  (make-array 10000. #+:CL :ADJUSTABLE #+:CL T)))
		(zf *replay-assumption-array*
		    (fill *replay-assumption-array* nil)
		    (setq *replay-assumption-array*
			  (make-array 1000. #+:CL :ADJUSTABLE #+:CL T)))
		(zf *replay-class-array*
		    (fill *replay-class-array* nil)
		    (setq *replay-class-array*
			  (make-array 2000. #+:CL :ADJUSTABLE #+:CL T)))
		(when meter-p (ensure-monitoring) (reset-meter meter-p))
		(setq update-atms nil start-time (get-internal-run-time))
		(meter meter-p (init-tms T))
		(setf (aref *replay-node-array* 2) *contra-node*)
		(if *simple-hybrid* (change-foci (list *empty-env*))))
      (VERSION (setq update-atms nil version (next-token)))
      (END (replay-end output start-time meter-p)
	   (return 'DONE))
      ((CREATE-NODE C-N)
       (setq n (next-token))
       (unless (< n (array-length *replay-node-array*))
	 (setq *replay-node-array*
	       (adjust-array *replay-node-array*
			     (floor (* 1.5 (array-length *replay-node-array*))))))
       (setf (aref *replay-node-array* n)
	     (progn (setq n (format nil "R~D" n)) (meter meter-p (create-node n)))))
      (BASIC-MAKE-ASSUMPTION
	(setq n (next-token))
	(setf (aref *replay-assumption-array* n)
	      (cond ((and (>= version 5) (setq m (next-token)))
		     (setq m (unique-to-class m))
		     (meter meter-p (basic-make-assumption m "Replay" "Replay")))
		    (t (meter meter-p
			      (basic-make-assumption "Replay" "Replay" "Replay"))))))
      ;; CS id class passumption nassumption pnode nnode
      ;; Assumes no interim symbols are being created.
      (CS1 
	  (setq n (next-token))
	  (setq u (next-token) j (next-token))
	  (multiple-value-setq (n m)
	    (meter meter-p (create-symbol "Replay" 'IGNORE (eq (car u) 'A) (eq (car j) 'A))))
	  (zf (assumption? n)
	      (setf (aref *replay-assumption-array* (cdr u)) n)
	      (setf (aref *replay-node-array* (cdr u)) n))
	  (zf (assumption? m)
	      (setf (aref *replay-assumption-array* (cdr j)) m)
	      (setf (aref *replay-node-array* (cdr j)) m)))

      (CS (next-token)
	  (setq n (next-token))
	  (setq u (next-token) j (next-token))
	  (multiple-value-setq (n m)
	    (meter meter-p (create-symbol "Replay" 'IGNORE (eq (car u) 'A) (eq (car j) 'A))))
	  (zf (assumption? n)
	      (setf (aref *replay-assumption-array* (cdr u)) n)
	      (setf (aref *replay-node-array* (cdr u)) n))
	  (zf (assumption? m)
	      (setf (aref *replay-assumption-array* (cdr j)) m)
	      (setf (aref *replay-node-array* (cdr j)) m)))
      ;; Obsolete, occurs only in old trace files.
      (DE (zf define
	      (setf (gethash (next-token) *trace-read-hash*) (read-env))
	      (next-token)
	      (next-token)))
      (DE1 (zf define
	       (setf (gethash (next-token) *trace-read-hash*) (read-env1))
	       (next-token)
	       (next-token)))
      (L (cond (check-labels
		(setq n (next-token)
		      u (unique-to-n-a (car n) (cdr n))
		      j (read-label))
		(unless (same-setp (n-a-envs u) j)
		  (format T "~% Faulty label detected on replay for node ~A" n)))
	       (T (next-token) (next-token))))
      ;; Change-focus.
      (CF (change-foci (read-label)))
      ;; Obsolete:
      ((CREATE-CLASS C-C)
       (setq n (next-token))
       (setf (aref *replay-class-array* n)
	     (progn (setq n (format nil "C~D" n)) (meter meter-p (create-class n)))))
      (C-C1
       (setq n (next-token) u (next-token) m (next-token))
       (setf (aref *replay-class-array* n)
	     (progn (setq n (format nil "C~D" n))
		    (meter meter-p (create-class n u m)))))
      (AC (setq n (aref *replay-class-array* (next-token))
		m (next-token)
		u (unique-to-n-a (car m) (cdr m)))
	  (meter meter-p (add-class-to-node u n)))
      (CLOSE-CLASS (setq m (unique-to-class (next-token)))
		   (meter meter-p (close-variable-class m)))
      (CL (setq n (read-n-a-list)
		u (read-n-a-list))
	  (clause '(replay) n u))
      ((JUSTIFY-NODE J-N IJ-N)
       (setq n (next-token)
	     u (unique-to-n-a (car n) (cdr n))
	     j (cons 'REPLAY (read-n-a-list)))
       (zf (eq command 'IJ-N)
	   (meter meter-p (inactive-justify-node u j))
	   (meter meter-p (justify-node u j))))
      (ADD-XOR-ASSUMPTION-TO-CLASS
	(setq n (unique-to-n-a 'A (next-token)) m (unique-to-class (next-token)))
	(meter meter-p (add-xor-assumption-to-class n m)))
      (ASY (setq n (aref *replay-node-array* (next-token))
		 m (aref *replay-node-array* (next-token))
		 u (next-token))
	   (zf u (setq u (aref *replay-class-array* u)))
	   (meter meter-p (assume-symbol n m u)))
      (C-X-C-F-N2
	(setq n (read-n-a-list))
	(meter meter-p (assume-oneof n 'REPLAY)))
      ;; Obsolete.
      (C-X-C-F-N
	(setq n (next-token))
	(or (setq m (unique-to-class n))
	    (setf (aref *replay-class-array* n)
		  (progn (setq m (format nil "C~D" n)) (meter meter-p (create-class n)))))
	(setq n (read-n-a-list))
	(meter meter-p (create-xor-class-from-nodes n m)))
      ;; Obsolete.
      (V-I-D-S-S (setq n (read-env)
		       m (mapcar #'(lambda (choice-set)
				     (mapcar #'(lambda (pair)
						 (unique-to-n-a (car pair) (cdr pair)))
					     choice-set))
				 (next-token)))
		 (meter meter-p (variable-interpretations-depth-stack-sets n m)))
      ;; Obsolete.
      (V-I-D-S-S1 (setq n (gethash (next-token) *trace-read-hash*)
			m (mapcar #'(lambda (choice-set)
				      (mapcar #'(lambda (unique)
						  (or (aref *assumption-array* unique)
						      (error "Assumption does not exist")))
					      choice-set))
				  (next-token)))
		  (meter meter-p (setq u (variable-interpretations-depth-stack-sets n m)))
		  (cond (check (setq j (read-label))
			       (unless (same-setp j u)
				 (error "V-I-D-S-S1 mismatch between ~A and ~A" u j)))
			(t (next-token))))
      (V-I-D-S-S2 (setq n (read-env1)
			m (mapcar #'(lambda (choice-set)
				      (mapcar #'(lambda (unique)
						  (or (aref *assumption-array* unique)
						      (error "Assumption does not exist")))
					      choice-set))
				  (next-token)))
		  (meter meter-p (setq u
				       (if *simple-hybrid*
				      (variable-interpretations-depth-stack-sets-focus n m)
				      (variable-interpretations-depth-stack-sets n m))))
				      
		  

		  (cond (T check (setq j (read-label))
			       (unless (same-setp j u)
				 (error "V-I-D-S-S1 mismatch between ~A and ~A" u j)))
			(t (next-token))))
      
      (NF (setq n (next-token))
	  (setq j (unique-to-n-a (car n) (cdr n)))
	  (and check
	       (i-false? j)
	       (error "Node ~A was not false now is false" n)))
      (F (setq n (next-token))
	 (setq j (unique-to-n-a (car n) (cdr n)))
	 (and check
	      (not (i-false? j))
	      (error "Node ~A was false now is not false" j)))
      (TR (setq n (next-token))
	  (setq j (unique-to-n-a (car n) (cdr n)))
	  (and check
	       (not (i-true? j))
	       (error "Node was true now is not true")))
      (NT (setq n (next-token))
	  (setq j (unique-to-n-a (car n) (cdr n)))
	  (and check
	       (i-true? j)
	       (error "Node was not true now is now is  true")))
      (IN (setq n (next-token))
	  (setq j (unique-to-n-a (car n) (cdr n)))
	  (and check
	       (not (i-in? j))
	       (error "Node was in now is now is not in")))
      (OUT (setq n (next-token))
	   (setq j (unique-to-n-a (car n) (cdr n)))
	   (and check
		(not (i-out? j))
		(error "Node ~A was out now is not out with label ~A" n (n-a-envs j))))
      (S (setq m (next-token)
	       n (next-token)
	       j (unique-to-n-a (car n) (cdr n)))
	 (and check
	      ;;*** kludge -fix. package problem.
	      (not (equal (string m) (string (setq u (status-of-node j)))))
	      (error "Node ~A's status was ~A but now is ~A" n m u)))
      (T (error "Unknown op: ~A" command)))
    (and *simple-hybrid* update-atms (update-atms))
    ))

(defun replay-end (output start-time meter-p)
  (format output "~% Replay time (processing queued nogoods) is:~D seconds"
	  (time-taken start-time))
  (meter-report meter-p))

;;; Obsolete.
(defun read-env () (find-or-make-env (read-n-a-list)))

(defun read-env1 () (find-or-make-env (read-a-list)))

;;; Just here for debugign.
;(defun read-env1 () (let* ((as (read-a-list))
;			   (env (find-or-make-env as)))
;		      (if (env-contradictory env) (error "Can't happen"))
;		      env))

(defun read-a-list ()
  (mapcar #'(lambda (unique) (aref *assumption-array* unique)) (next-token)))

(defun read-n-a-list ()
  (mapcar #'(lambda (pair) (unique-to-n-a (car pair) (cdr pair))) (next-token)))

;;;**** fx this sometime.  C-X-C-F-N should fill in the assumption aray.
(defun unique-to-n-a (type unique)
  (or (selectq type
	(A (or (aref *replay-assumption-array* unique)
	       (aref *assumption-array* unique)))
	(N (aref *replay-node-array* unique)))
      (error "Unknown n-a")))

(defun unique-to-class (unique) (aref *replay-class-array* unique))

(defun trace-env (env)
  (unless (gethash (env-unique env) *trace-write-hash*)
    (format *trace-file* "~%DE1 ~D (" (env-unique env))
    (dolist (a (env-assumptions env))
      (format *trace-file* " ~D" (assumption-unique a)))
    (format *trace-file* ")")
    (setf (gethash (env-unique env) *trace-write-hash*) T)
    ))

(defun read-label ()
  (mapcar #'(lambda (number) (or (gethash number *trace-read-hash*)
				 (error "Trace environment ~A not defined" number)))
	  (next-token)))