(in-package :cl-user)

(defun euler-proof (q loads &key (output-format :n3)
		      (think t think-supplied-p)
		      (steps nil steps-supplied-p)
		      (proof nil)
		      (debug nil debug-supplied-p)
		      (trace nil trace-supplied-p))
  (unless (#"matches" q "(?si)^(data|file|http):.*")
    (setq q (concatenate 'string "data:," q)))
  (when proof
    (assert (eq output-format :n3) () "Can only see proof if output format is n3"))
  (let ((config (#"getInstance" 'Euler.Configuration)))
    (#"setProofExplanation"  config proof)
    (when think-supplied-p (#"setThink" config think))
    (when steps-supplied-p (#"setSteps" config steps))
    (when debug-supplied-p
      (when debug
	(#"setLogLevel" (#"getInstance" 'euler.output.StdOutputter)
	 (get-java-field 'euler.output.ILogger "FINE"))))
    (when trace-supplied-p 
      (when trace
	(#"setLogLevel" (#"getInstance" 'euler.output.StdOutputter)
	 (get-java-field 'euler.output.ILogger "FINER"))))
    (let ((e (new 'euler)))
      (loop for l in loads do
	    (unless (#"matches" l "(?si)^(data|file|http):.*")
	      (setq l (concatenate 'string "data:," l)))
	    (#"load" e l))
      (#"prepare" e)
      (unwind-protect
	  (ecase output-format
	    (:n3 (#"proof" e q))
	    ((:rdf/xml  :rdf/xml-abbrev :n-triple :turtle)
	     (let ((model (#"createDefaultModel" 'ModelFactory))
		   (s (new 'stringreader (#"proof" e q)))
		   (w (new 'stringwriter)))
	       (#"read" model s "" "N3")
	       (#"write" model w (string output-format))
	       (#"toString" w)
	       )))
	(#"setLogLevel" (#"getInstance" 'euler.output.StdOutputter)
	 (get-java-field 'euler.output.ILogger "WARNING"))))))

(defun to-n3 (url)
  (let ((model (#"createDefaultModel" 'ModelFactory))
	(w (new 'stringwriter)))
    (#"read" model url)
    (#"write" model w "N3")
    (#"toString" w)))

(defun rdfxml-to-n3 (string)
  (let ((model (#"createDefaultModel" 'ModelFactory))
	(s (new 'stringreader string))
	(w (new 'stringwriter)))
    (#"read" model s "" "RDF/XML")
    (#"write" model w "N3")
    (#"toString" w)))

;(euler-proof  "_:sub rdfs:subClassOf _:super. _:super a _:what. _:what log:notEqualTo owl:Restriction."
;	      (list (to-n3 "http://www.biopax.org/release/biopax-level2.owl")))

;(euler-proof "http://www.agfa.com/w3c/euler/authen.lemma.n3" (list "http://www.agfa.com/w3c/euler/authen.axiom.n3"))