race.lisp

;;; Copyright (c) 2009, Joshua Taylor.  All rights reserved.

;;; Redistribution and use in source and binary forms, with or without
;;; modification, are permitted provided that the following conditions
;;; are met:

;;;   * Redistributions of source code must retain the above copyright
;;;     notice, this list of conditions and the following disclaimer.

;;;   * Redistributions in binary form must reproduce the above
;;;     copyright notice, this list of conditions and the following
;;;     disclaimer in the documentation and/or other materials
;;;     provided with the distribution.

;;; THIS SOFTWARE IS PROVIDED BY THE AUTHOR 'AS IS' AND ANY EXPRESSED
;;; OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
;;; WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
;;; ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
;;; DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
;;; DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE
;;; GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
;;; INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
;;; WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
;;; NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
;;; SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

(in-package #:race-webservice)

(defconstant +race-webservice-url+
  "http://attempto.ifi.uzh.ch/ws/race/racews.perl"
  "The URL of the RACE webservice.")

(defconstant +race-prefix-uri+
  "http://attempto.ifi.uzh.ch/race")

(defun invoke-race-webservice (&rest args
                                     &key axioms
                                     theorems
                                     mode
                                     si st ot sdt dodt iodt sti aux
                                     (uri +race-webservice-url+)
                                     (drakma-parameters '()))
  "* Syntax:
invoke-race-webservice &key axioms theorems mode
                            si st or sdt dodt iodt sti aux
                            drakma-parameters uri => result*
* Arguments and Values:
- axioms --- a string
- theorems --- a string or nil
- mode --- one of the symbols :check-consistency, :prove, :answer-query
- si, st, ot, sdt, dodt, iodt, sti, aux --- generalized booleans
- uri --- a string or PURI:URI object, defaults to +race-webservice-url+
- drakma-parameters --- a plist, passed to DRAKMA:HTTP-REQUEST
- results --- results of DRAKMA:HTTP-REQUEST
* Description:
invoke-race-webservice invokes the RACE Webservice by sending a SOAP
request to URI.  More documentation on the RACE Webservice is available [1].
* See Also:
- [1] {http://attempto.ifi.uzh.ch/site/docs/race_webservice.html}"
  (declare (ignore axioms theorems mode si st ot sdt dodt iodt sti aux))
  (remf* args :uri :drakma-parameters)
  (apply 'drakma:http-request uri
         :content (apply 'make-race-soap-request args)
         drakma-parameters))

(defun make-race-soap-request
       (&key axioms theorems mode si st ot sdt dodt iodt sti aux)
  (assert (stringp axioms) (axioms)
    "Axioms must be a string of ACE text, but was ~S." axioms)
  (assert (or (and (member mode '("prove" "answer-query" "answer_query")
                           :test 'string-equal)
                   (stringp theorems))
              (and (member mode '("check-consistency" "check_consistency")
                           :test 'string-equal)
                   (null theorems)))
      (mode theorems)
    "Mode must be a string designator string-equal to prove, ~
     answer-query \(or answer_query\), or check-consistency ~
     \(or check_consistency\).  If mode is prove or answer-query, ~
     then theorems much be a string.  If mode is check-consistency, ~
     then theorems must be null.  Mode was ~S.  Theorems was ~S."
    mode theorems)
  (with-soap-envelope ("env" ("race" +race-prefix-uri+))
    (cxml:with-element* ("race" "Request")
      ;; Axioms
      (cxml:with-element* ("race" "Axioms")
        (cxml:text axioms))
      ;; Theorems
      (unless (null theorems)
        (cxml:with-element* ("race" "Theorems")
          (cxml:text theorems)))
      ;; Mode
      (cxml:with-element* ("race" "Mode")
        (cxml:text
         (pcase mode #'string-equal
           (("prove")
            "prove")
           (("answer-query" "answer_query")
            "answer_query")
           (("check-consistency" "check_consistency")
            "check_consistency"))))
      ;; Parameters
      (loop for p in '("si" "st" "ot" "sdt" "dodt" "iodt" "sti" "aux")
            for pp in (list si st ot sdt dodt iodt sti aux)
            when pp do (cxml:with-element* ("race" "Parameter")
                         (cxml:text p))))))

(defun race (&rest args
                   &key
                   axioms theorems mode
                   si st ot sdt dodt iodt sti aux
                   (uri +race-webservice-url+)
                   (drakma-parameters '())
                   (signal-warning-messages t)
                   (signal-error-messages nil))
  "* Syntax:
race &rest args &key signal-warning-messags signal-error-messages => reply
* Arguments and Values:
- args --- a plist of args for {defun race-webservice:invoke-race-webservice}
- signal-warning-messages, signal-error-messages --- booleans,
defaults are t and nil respectively
- reply --- a {defclass race-webservice:race-reply} object
* Description:
Race applies {defun race-webservice:invoke-race-webservice} with args,
parses the reply, and signals warnings and errors depending on the
values of signal-warning-messages and signal-error messages.
  RACE messages that have importance type \"warning\" will, by default
be signalled, while messages with importance \"error\" will not.
* Notes:
Since CXML:PARSE may or may not be able to handle a stream returned by
DRAKMA:HTTP-REQUEST, any drakma-parameters is passed to
{defun race-webservice:invoke-race-webservice} with :want-stream nil.
  invoke-race-webservice is called with :allow-other-keys t \(so that
signal-warning-messages and signal-error-messsages can passed
through\) and as a result, arguments that would cause an unexpected
keyword error to be signalled will not do so."
  (declare (ignore axioms theorems mode si st ot
                   sdt dodt iodt sti aux uri))
  (remf* args :signal-warning-messages :signal-error-messages)
  (let ((reply (parse-race-output
                (apply' invoke-race-webservice
                      :drakma-parameters (list* :want-stream nil
                                                drakma-parameters)
                      args))))
    (prog1 reply
      (signal-race-reply-messages reply
       :signal-warning-messages signal-warning-messages
       :signal-error-messages signal-error-messages))))

(defun signal-race-reply-messages
       (reply &key signal-warning-messages signal-error-messages)
  (dolist (message (race-reply-messages reply))
    (etypecase message
      (race-error-message
       (when signal-error-messages
         (error message)))
      (race-warning-message
       (when signal-warning-messages
         (warn message))))))

;;;; Classes related to the RACE Reply

(defclass race-reply ()
  ((messages
    :type list
    :reader race-reply-messages
    :initform '()
    :initarg :messages)
   (runtime
    :type integer
    :reader race-reply-runtime
    :initarg :runtime)
   (proofs
    :type list 
    :reader race-reply-proofs
    :initform '()
    :initarg :proofs)
   (why-not
    :type list ; of strings
    :reader race-reply-why-not
    :initform '()
    :initarg :why-not
    :documentation
    "A list of strings, the content of the race:Word elements that
     were in the race:WhyNot element.")))

(define-condition race-message (condition)
  ((importance
    :type (member :warning :error)
    :reader race-message-importance
    :documentation "One of the symbols :warning, or :error.")
   (type
    :type string
    :reader race-message-type
    :initarg :type)
   (sentence-id
    :type (or null integer)
    :reader race-message-sentence-id
    :initarg :sentence-id
    :documentation "An integer \(or left unbound\).")
   (subject
    :type string
    :reader race-message-subject
    :initarg :subject)
   (description
    :type string
    :reader race-message-description
    :initarg :description))
  (:report report-race-message))

(defun report-race-message (condition stream)
  (format stream
          "~A ~A (This is a ~S message~@[, see sentence ~S~].)"
          (race-message-subject condition)
          (race-message-description condition)
          (race-message-type condition)
          (if (not (slot-boundp condition 'sentence-id)) nil
            (race-message-sentence-id condition))))

(define-condition race-warning-message (warning race-message)
  ((importance :initform :warning)))

(define-condition race-error-message (error race-message)
  ((importance :initform :error)))

(defclass race-proof ()
  ((used-axioms
    :type list
    :reader race-proof-used-axioms
    :initarg :used-axioms)
   (used-aux-axioms
    :type list
    :reader race-proof-used-aux-axioms
    :initarg :used-aux-axioms)))

;;;; Parsing the RACE Reply

;;; Some utility XML handling functions

(defun get-race-elements-by-tag-name (document tag-name)
  (dom:get-elements-by-tag-name-ns
   document +race-prefix-uri+ tag-name))

(defun get-race-element-by-tag-name (document tag-name)
  (let ((elements (get-race-elements-by-tag-name document tag-name)))
    (if (eql 0 (dom:length elements)) nil
      (dom:item elements 0))))

(defun element-text-content (element)
  (case (dom:length (dom:child-nodes element))
    (0 "")
    (1 (dom:data (dom:first-child element)))
    (t (error "Don't know how to extract text content from element ~
               ~S with more than one child." element))))

(defun mapnodes (fn nodelist &aux (results '()))
  (dom:do-node-list (x nodelist (nreverse results))
    (push (funcall fn x) results)))

;;; Parsing functions proper

(defun parse-race-output (blob)
  "* Arguments and Values:
- blob --- an XML blob that contains the SOAP envelope"
  (let* ((response (cxml:parse blob (cxml-dom:make-dom-builder)))
         (messages (get-race-elements-by-tag-name response "Message"))
         (runtime (get-race-element-by-tag-name response "Runtime"))
         (proofs (get-race-elements-by-tag-name response "Proof"))
         (words (get-race-elements-by-tag-name response "Word")))
    (make-instance 'race-reply
     :proofs (extract-proofs proofs)
     :messages (extract-messages messages)
     :runtime (extract-runtime runtime)
     :why-not (extract-words words))))

(defun extract-proofs (elements &aux (proofs '()))
  "* Arguments and Values:
- elements --- a node list of race:Proof elements"
  (dom:do-node-list (element elements (nreverse proofs))
    (push (make-instance 'race-proof
           :used-axioms     (mapnodes 'element-text-content
                                      (get-race-elements-by-tag-name
                                       element "Axiom"))
           :used-aux-axioms (mapnodes 'element-text-content
                                      (get-race-elements-by-tag-name
                                       element "AuxAxiom")))
          proofs)))

(defun extract-messages (elements &aux (messages '()))
  "* Arguments and Values:
- elements --- a node list of race:Message element nodes"
  (dom:do-node-list (element elements (nreverse messages))
    (push (extract-message element) messages)))

(defun extract-message (element)
  "* Arguments and Values:
- element --- a race:Message element node"
  (flet ((et (name)
           (element-text-content
            (get-race-element-by-tag-name
             element name))))
    (apply 'make-condition (pcase (et "Importance") #'string=
                             ("warning" 'race-warning-message)
                             ("error"   'race-error-message))
           :type (et "Type")
           :subject (et "Subject")
           :description (et "Description")
           (unless (string= "" (et "SentenceID"))
             (list :sentence-id (parse-integer (et "SentenceID")))))))

(defun extract-runtime (element)
  "* Arguments and Values:
- element --- an race:Runtime element node"
  (parse-integer (element-text-content element)))

(defun extract-words (elements)
  "* Arguments and Values:
- elements --- a node list of race:Word element nodes"
  (mapnodes 'element-text-content elements))