;;;; -*-  Mode: LISP; Syntax: Common-Lisp; Base: 10                          -*-
;;;; ---------------------------------------------------------------------------
;;;; File name: expression-check.lsp
;;;;    System: 
;;;;    Author: Ken Forbus
;;;;   Created: November 20, 2003 12:26:21
;;;;   Purpose: 
;;;; ---------------------------------------------------------------------------
;;;;  Modified: #<Printer Error, obj=#x20001485: attempt to call `cgx:date*' which is an undefined function.>
;;;; ---------------------------------------------------------------------------

(in-package :fire)

;;;; Expression checking
;;;; It might seem that this would never be necessary.
;;;; But there are several cases where we need this:
;;;; 1. Importing KB contents from other sources.  There are a surprising number of
;;;;    errors in the Cyc KB contents, for example.
;;;; 2. If learning systems are generating new assertions, it is possible that they
;;;;    could generate syntactically incorrect expressions.
;;;; These two functionalities suggest two really different implementations.


;;;; Quick version

(defun legal-expression? (thing)
  (catch 'bailing-legal-expression?
         (check-expression-legality thing)))

(defun check-expression-legality (thing)
  (cond ((null thing) t)
        ((variable? thing) t)
        ((atom thing) (throw 'bailing-legal-expression? nil))
        ((listp thing)
         (cond ((variable? (car thing)) ;; Can't tell, assume it's okay
                (dolist (arg (cdr thing) t)
                  (check-argument-legality arg)))
               (t (case (predicate-type (car thing))
                    (:relation (check-relation-arg-constraints
                                (car thing) (cdr thing)))
                    (:logical (dolist (arg (if (introduces-local-variable? (car thing))
                                             (cddr thing)
                                             (cdr thing)) t)
                                (check-expression-legality arg)))
                    (:function (check-relation-arg-constraints 
                                (car thing) (cdr thing)))
                    (t (throw 'bailing-legal-expression? nil))))))
        (t (throw 'bailing-legal-expression? nil))))
        
(defun check-relation-arg-constraints (pred args)
  ;; To have gotten here, we know it is a relation.
  ;; Check arity first, then if arity is okay, check types of arguments.
  (let ((the-arity (arity pred)))
    (cond ((eq the-arity :n-ary) t)
          ((integerp the-arity)
           (let ((measured-arity (length args)))
             (unless (= the-arity measured-arity)
               (throw 'bailing-legal-expression? nil))
             ;; Now need to check the argument types.  We won't go very
             ;; far in this, just looking for syntactically stupid things.
             (let ((arg-type-signature (argument-type-signature pred the-arity)))
               (when (null arg-type-signature) (throw 'bailing-legal-expression? nil))
               (do ((sig arg-type-signature (cdr sig))
                    (the-args args (cdr the-args)))
                   ((null sig) t)
                 (argument-type-check-okay? (car sig) (car the-args))))))
          (t (throw 'bailing-legal-expression? nil)))))

(defun argument-type-signature (pred arity)
  (argument-type-signature1 pred 1 arity))

(defun argument-type-signature1 (pred n arity)
  (cond ((> n arity) nil)
        (t (let ((arg-type (arg-isa pred n)))
             (cond ((eq arg-type :unknown) (throw 'bailing-legal-expression? nil))
                   (t (cons arg-type 
                            (argument-type-signature1 pred (1+ n) arity))))))))

;;;(defun spec-of? (col1 col2 &optional (kb *kb*))
;;;  (member col2 (all-genls col1 :kb kb)))

(defun argument-type-check-okay? (expected-type arg)
  (cond ((variable? arg) t)
        ((spec-of? expected-type 'data::CycLVariable) 
         (throw 'bailing-legal-expression? nil))
        ((spec-of? expected-type 'data::ELExpression)
         ;; Should do real type check, but we're just being simple here.
         (check-argument-legality arg))
        ;; Should ensure that arguments are nats.
        ;; Next time..
        (t t)))

(defun check-argument-legality (arg)
  (cond ((null arg) t)
        ((atom arg) t)
        ((listp arg)
         (check-expression-legality arg))
        (t (throw 'bailing-legal-expression? nil))))
        



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; End of Code