;; -*- Mode: LISP; -*-

;;;; JTRE -- a version of TRE which uses the JTMS
;;; Last Edited, 1/29/93, by KDF

;;; Copyright (c) 1992, Kenneth D. Forbus, Northwestern University,
;;; Johan de Kleer and Xerox Corporation.
;;; All rights reserved.

;;; See the file legal.txt for a paragraph stating scope of permission
;;; and disclaimer of warranty.  The above copyright notice and that
;;; paragraph must be included in any separate copy of this file.

(in-package :cl-user)

(defvar *jtre-path* nil "JTRE's path")
(defvar *jtre-files* nil "JTRE's files")
(defvar *jqueen-rule-file* nil "Rule for n-queens problem")
(defvar *jsaint-files* nil "JSAINT system files")
(defvar *jsaint-rules* nil "JSAINT rules, must be compiled in JSAINT context")
(defvar *jsaint-operators* nil "JSAINT operators, must be compiled in JSAINT context")

#+MCL (unintern 'rlet (find-package :ccl))

(setf *jtre-path* (make-bps-path "jtms"))

(setf *jtre-files*
      '("jtms"      ;; JTMS
        "jinter"    ;; Interface
        "jdata"     ;; Database
        "jrules"    ;; Rule system
        "unify"     ;; Unifier
        "funify"    ;; Open-coding unification
        "jtest"     ;; shakedown procedure for jtre
        "jqueens"   ;; JTRE version of N-queens puzzle
        ))

(setf *jqueen-rule-file* "jqrule")   ;; Contradiction detection rule

(setq *jsaint-files*
      '("jsaint"   ;; JSAINT main program
        "match"    ;; math-oriented pattern matcher
        "simplify" ;; Algebraic simplifier 
        ))

;; These two files can only be compiled after a JSAINT has been created
(setq *jsaint-rules*
      "jsrules")  ;; Bookkeeping rules

(setq *jsaint-operators* 
      "jsops")    ;; Sample integration library
      

(defun load-jtre (&key (action :compile-if-newer))
  (bps-load-files *jtre-path* *jtre-files* :action action))

(defun compile-jqueens ()
  (unless (and (boundp '*jtre*)
               (not (null (symbol-value '*jtre*))))
    (in-jtre (create-jtre "Jqueens-dummy")))
  (bps-load-file *jtre-path* *jqueen-rule-file* :action :compile))

(defun load-jsaint (&key (action :compile-if-newer))
  (load-jtre :action action)
  (cond ((eq action :compile)
         (bps-load-files *jtre-path* *jsaint-files* :action :compile)
         (compile-jsaint-rules))
        (t (bps-load-files *jtre-path* *jsaint-files* :action action))))

(defun compile-jsaint-rules ()
  (unless (and (boundp '*jsaint*)
               (not (null (symbol-value '*jsaint*))))
    (create-jsaint "Jsaint-dummy" nil))
  (bps-load-file *jtre-path* *jsaint-rules* :action :compile)
  (bps-load-file *jtre-path* *jsaint-operators* :action :compile))

(defparameter *jtre-help*
  '("JTRE:"
    "  To load JTRE, call (load-jtre)."
    "  For this help message, call (help-jtre)."
    "  To test JTRE, call (shakedown-jtre)."
    "  To test N-Queens problem, call (test-queens <from> <to>)."
    "  Additional JTMS tests available in jtms-ex.lsp."
    ""
    "  To load JSAINT, call (load-jsaint)."
    "    Sample problems:"
    "     (try-jsaint problem1)"
    "     (try-jsaint problem2)"
    "     (try-jsaint problem3)"
    ))
  
(defun help-jtre (&optional (stream t))
  "Print out helpful information about the JTMS/JTRE."
  (terpri stream)
  (dolist (line *jtre-help*)
    (format stream "~%~A" line))
  (terpri stream))
  
(help-jtre)