(in-package :cs325-user)

;;; Change Log
;;; 10-15-2011 CKR removed ad hoc file loading in favor of QuickLisp


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Sample client-side code for xml-rpc
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(eval-when (:compile-toplevel :load-toplevel :execute)
  (include "xml-rpc-utils")
  )

;;; lisp.getTime
;;;
;;; lisp.getTime => list of 9 values
;;;   Returns server's current time, using values returned by Lisp's
;;;   get-decoded-time.
;;;
;;; Sample call to localhost and result:
;;;
;;; (xml-rpc-call (encode-xml-rpc-call "lisp.getTime"))
;;;  => (53 58 11 5 10 2009 0 "T" 6)
;;;
;;; That result is Monday, 10/5/2009, 11:58:53AM CDT.
;;;
;;; Sample call to another host:
;;;
;;; (xml-rpc-call (encode-xml-rpc-call "lisp.getTime")
;;;               :host "myserver.org


;;; lisp.GCD
;;;
;;; lisp.GCD m n => greatest common divisor of m and n
;;;
;;; Sample call to localhost and expected result:
;;;
;;; (xml-rpc-call (encode-xml-rpc-call "lisp.GCD" 36 63))
;;;  => 9


;;; CALL-FOR-PROOF
;;;
;;; CALL-FOR-PROOF claim assertions [XML-RPC-CALL keywords] => proof
;;;    Returns the subset of assertions (facts and implications) 
;;;    that prove claim, if any. Calls lisp.getProof and
;;;    interns all strings in the result returned into
;;;    the current package. Standard XML-RPC-CALL keyword
;;;    parameters such as :HOST and :PORT are allowed.
;;;
;;; Sample call to a fictional remote host and expected result:
;;;
;;; (call-for-proof 'r '(p (-> q r) (-> p q)) :host "logicserver.net")
;;;  => ((-> q r) (-> p q) p)

;;; Note that CALL-FOR-PROOF knows nothing about how lisp.getProof()
;;; works. It doesn't even know if it's talking to a 
;;; Lisp system or not.

(defun call-for-proof (claim given &rest args)
  (intern-strings
   (apply #'xml-rpc-call
          (encode-xml-rpc-call "lisp.getProof" claim given)
          args)))