;;; -*- Mode:Lisp; Syntax:Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*-

;;; If you load this file (with translation into the "KIF" implementation
;;; -- the default ), then the definitions are saved on property lists
;;; and can be used for online documentation and in cross-reference reports.

(in-package "ONTOLINGUA-USER")   ;inherits from the KIF package
                                 ;all constants defined here are exported
                                 ;from the KIF package.

(define-theory KIF-LISTS (kif-numbers)
  "The KIF vocabulary for lists as defined in the KIF 3.0 specification.")


(in-theory 'kif-lists)

(define-class LIST (?x)
  "A list is a sequence --- an ordered bag --- of elements.
It is KIF primitive.")

(define-class NULL (?list)
  "True of the list with no items."

  :iff-def (and (list ?list)
                (= (length ?list) 0)))


(define-instance NIL (null)
  "The list with no items, of length 0.
All null lists are equal to this object, called NIL.")


(define-function LISTOF (@items) :-> ?list
  "LISTOF is the sequence constructor function for KIF. It takes any finite
number of arguments and denotes the list (i.e., sequence, tuple) of
those items.
  LISTOF is an operator in KIF."
  :def (list ?list))


(define-relation SINGLE (?list)
  "A list of length 1."

  :iff-def (and (list ?list)
                (= (length ?list) 1)))


(define-relation DOUBLE (?list)
  "A list of length 2."

  :iff-def (and (list ?list)
                (= (length ?list) 2)))


(define-relation TRIPLE (?list)
  "A list of length 3."

  :iff-def (and (list ?list)
                (= (length ?list) 3)))

(define-function FIRST (?list)
  :def (list ?list)
  :lambda-body (if (exists @items 
                     (= (listof ?x @items) ?list))
                   ?x))

(define-function REST (?list) :-> ?rest-list
  :iff-def (or (and (null ?list)
                    (= ?rest-list ?list))
               (exists (?x @items)
                 (and (= ?list (listof ?x @items))
                      (= ?rest-list (listof @items))))))

(define-function LAST (?list)
  :def (list ?list)
  :lambda-body (cond ((null ?list) bottom)
                     ((null (rest ?list)) (first ?list))
                     (true (last (rest ?list)))))


(define-function BUTLAST (?list)
  :lambda-body (cond ((null ?list) bottom)
                     ((null (rest ?list)) nil)
                     (true (cons (first ?list) (butlast (rest ?list))))))


(define-relation ITEM (?x ?list)
  "The sentence {\tt (item $\tau_1$ $\tau_2$)} is true if and only if
the object denoted by $\tau_2$ is a non-empty list and the object
denoted by $\tau_1$ is either the first item of that list or an item in
the rest of the list."

  :def (and (list ?list)
            (not (null ?list))
            (or (= ?x (first ?list)) (item ?x (rest ?list)))))


(define-relation SUBLIST (?l1 ?l2)
  "The sentence {\tt (sublist $\tau_1$ $\tau_2$)} is true if and only if
the object denoted by $\tau_1$ is a final segment of the list denoted by
$\tau_2$."

  :def (and (list ?l1)
            (list ?l2)
            (or (= ?l1 ?l2)
                (sublist ?l1 (rest ?l2)))))


(define-function CONS (?x ?list) :-> ?new-list
 "The function {\tt cons} adds the object specified as its first
argument to the front of the list specified as its second argument."
 
 :def (and (list ?list)
           (list ?new-list))
 :lambda-body (if (= ?list (listof @l)) (listof ?x @l)))

(define-function APPEND (?l1 ?l2) :-> ?new-list
  "The function {\tt append} adds the items in the list specified as its first
argument to the list specified as its second argument.  ."
                 
  :def (and (list ?l1)
            (list ?l2)
            (list ?new-list))
  :lambda-body (if (null ?l1)
                   (if (list ?l2) ?l2)
                   (cons (first ?l1) (append (rest ?l1) ?l2))))

(define-function REVAPPEND (?l1 ?l2) :-> ?new-list
 "The function {\tt revappend} is similar to append, except that it
adds the items in reverse order."
  :def (and (list ?l1)
            (list ?l2)
            (list ?new-list))
  :lambda-body (if (null ?l1)
                   (if (list ?l2) ?l2)
                   (revappend (rest ?l1) (cons (first ?l1) ?l2))))


(define-function REVERSE (?list) :-> ?new-list
  "The function {\tt reverse} produces a list in which the order of items is the
reverse of that in the list supplied as its single argument."
  :def (and (list ?list)
            (list ?new-list))
  :lambda-body (revappend ?list (listof)))


(define-function ADJOIN (?x ?list) :-> ?new-list
   "The functions {\tt adjoin} and {\tt remove} construct lists by adding or
removing objects from the lists specified as their arguments."
  :def (and (list ?list)
            (list ?new-list))
  :lambda-body (if (item ?x ?list) ?list (cons ?x ?list)))

(define-function REMOVE (?x ?list) :-> ?new-list
   "The functions {\tt adjoin} and {\tt remove} construct lists by adding or
removing objects from the lists specified as their arguments."
  :def (and (list ?list)
            (list ?new-list))
  :lambda-body (cond ((null ?list) nil)
                     ((and (= ?x (first ?list)) (list ?list))
                      (remove ?x (rest ?list)))
                     ((list ?list) (cons ?x (remove ?x (rest ?list))))))


(define-function SUBST (?x ?y ?z)
   "The value of {\tt subst} is the object or list obtained by
substituting the object supplied as first argument for all occurrences
of the object supplied as second argument in the object or list
supplied as third argument."
  :lambda-body (cond ((= ?y ?z) ?x)
                     ((null ?z) nil)
                     ((list ?z) (cons (subst ?x ?y (first ?z))
                                      (subst ?x ?y (rest ?z))))
                     (true ?z)))

  

(define-function LENGTH (?list) :-> ?n
 "The function constant {\tt length} gives the number of items in a list."
  :def (and (list ?list)
            (nonnegative-integer ?n))
  :lambda-body (cond ((null ?list) 0)
                     ((list ?list) (1+ (length (rest ?list))))))

(define-function NTH (?list ?n)
   "{\tt nth} returns the item in the list specified as its first
argument in the position specified as its second argument."
  :def (and (list ?list)
            (natural ?n))
  :lambda-body (cond ((= ?n 1) (first ?list))
                     ((positive ?n) (nth (rest ?list) (1- ?n)))))


(define-function NTHREST (?list ?n) :-> ?new-list
  "{\tt nthrest} returns the list specified as its first argument
minus the first $n$ items, where $n$ is the number specified as its
second argument."
  :def (and (list ?list)
            (natural ?n)
            (list ?new-list))
  :lambda-body (cond ((= ?n 0) (if (list ?list) ?list))
                     ((positive ?n) (nthrest (rest ?list) (1- ?n)))))