1:- module(race, [
    2      check_consistency/1,
    3      check_consistency/2,
    4      ask/3,
    5      ask/4,
    6      ask_with_answers/3,
    7      prove/3,
    8      prove/4,
    9      prove_with_answers/3
   10   ]).   11
   12:- use_module(library(race/axiom)).   13:- use_module(library(race/sentence)).   14:- use_module(library(race/util)).   15
   16:- use_module(library(wsdl)).   17:- use_module(library(xpath)).   18:- use_module(library(soap)).   19:- use_module(library(http/http_open)).   20:- use_module(library(http/http_header)).   21
   22% :- debug(soap).
   23
   24% :- multifile sgml_write:xmlns/2.
   25% sgml_write:xmlns(race, 'http://attempto.ifi.uzh.ch/race').
   26
   27:- initialization wsdl_read(library(race/wsdl/'race.wsdl')).   28
   29
   30check_consistency(Knowledge) :-
   31   check_consistency(Knowledge, []).
   32
   33check_consistency(Knowledge, Result) :-
   34   Operation = ('http://attempto.ifi.uzh.ch/race':'RacePortType') /
   35               ('http://attempto.ifi.uzh.ch/race':'RunRace'),
   36   soap_call(Operation, [
   37      'Axioms'=Knowledge,
   38      'Mode'='check_consistency'
   39      %, 'Parameter'='raw'
   40   ], [ReplyDOM], [dom]),
   41   get_inconsistencies(ReplyDOM, Result).
   42
   43ask(Knowledge, Question, Result) :-
   44   ask(Knowledge, Question, Result, []).
   45
   46ask(Knowledge, Question, Result, Options) :-
   47   Operation = ('http://attempto.ifi.uzh.ch/race':'RacePortType') /
   48               ('http://attempto.ifi.uzh.ch/race':'RunRace'),
   49   soap_call(Operation, [
   50      'Axioms'=Knowledge,
   51      'Mode'='answer_query',
   52      'Theorems'=Question
   53      % , 'Parameter'='raw'
   54   ], ReplyDOM, [dom]),
   55   get_result(ReplyDOM, R, Options),
   56   ( memberchk(sentence(true), Options) ->
   57      ( R = results(Proofs) ->
   58        maplist(generate_answer, Proofs, Answers),
   59        Result = results(Answers)
   60      ; R = not(WhyNot) ->
   61        generate_answer(not(WhyNot), Answer),
   62        Result = not(Answer)
   63      ; Result = R)
   64   ; Result = R).
   65
   66ask_with_answers(Knowledge, Question, Result) :-
   67   ask(Knowledge, Question, Result, [sentence(true)]).
   68
   69prove(Knowledge, Theorem, Result) :-
   70   prove(Knowledge, Theorem, Result, []).
   71
   72prove(Knowledge, Theorem, Result, Options) :-
   73   Operation = ('http://attempto.ifi.uzh.ch/race':'RacePortType') /
   74               ('http://attempto.ifi.uzh.ch/race':'RunRace'),
   75   soap_call(Operation, [
   76      'Axioms'=Knowledge,
   77      'Mode'='prove',
   78      'Theorems'=Theorem
   79      % , 'Parameter'='raw'
   80   ], ReplyDOM, [dom]),
   81   get_result(ReplyDOM, R, Options),
   82   ( memberchk(sentence(true), Options) ->
   83      ( R = results(Proofs) ->
   84        maplist(generate_answer, Proofs, Answers),
   85        Result = results(Answers)
   86      ; R = not(WhyNot) ->
   87        generate_answer(not(WhyNot), Answer),
   88        Result = not(Answer)
   89      ; Result = R)
   90   ; Result = R).
   91
   92prove_with_answers(Knowledge, Theorem, Result) :-
   93   prove(Knowledge, Theorem, Result, [sentence(true)]).
   94
   95get_inconsistencies(ReplyDOM, Result) :-
   96   xpath_select(ReplyDOM, 'Message', FirstMessage),
   97   FirstMessage = element(_, _, Elements),
   98   member(element(_:'Subject', _, [Subject]), Elements),
   99   Subject = 'Axioms cannot be parsed.',
  100   !,
  101   Result = error(Subject).
  102
  103get_inconsistencies(ReplyDOM, Result) :-
  104   findall(Axiom, xpath_select(ReplyDOM, 'Axiom', element(_, _, [Axiom])), Axioms),
  105   maplist(axiom_to_entity, Axioms, Result).
  106
  107get_result(ReplyDOM, Result, _Options) :-
  108   findall(ProofDOM, xpath_select(ReplyDOM, 'Proof', ProofDOM), ProofDOMs),
  109   findall(WhyNotDOM, xpath_select(ReplyDOM, 'WhyNot', WhyNotDOM), WhyNotDOMs),
  110   ( ( ProofDOMs \= [], WhyNotDOMs = []) ->
  111     proof_list(ProofDOMs, Proof),
  112     Result = results(Proof)
  113   ; ( ProofDOMs = [], WhyNotDOMs \= []) ->
  114     why_not_list(WhyNotDOMs, WhyNot),
  115     Result = not(WhyNot)
  116   ; (xpath_select(ReplyDOM, 'Message', MessageDOM), MessageDOM \= []) ->
  117     Result = error('Sorry, this sentence was not in ACE.')
  118   ; Result = error('Sorry, there were some errors.')).
  119
  120proof_list(ProofDOMs, Result) :-
  121   maplist(proof, ProofDOMs, Result).
  122
  123proof(ProofDOM, proof(Entities)) :-
  124   findall(Axiom, xpath_select(ProofDOM, 'Axiom', element(_, _, [Axiom])), Axioms),
  125   maplist(axiom_to_entity, Axioms, Entities).
  126
  127why_not_list([WhyNotDOM], Entities) :-
  128   findall(Word, xpath_select(WhyNotDOM, 'Word', element(_, _, [Word])), Words),
  129   maplist(axiom_to_entity, Words, Entities).
  130
  131xpath_select(DOM, Element, Result) :-
  132   xpath(DOM, //(_:Element), Result),
  133   Result \= element(_, _, []).
  134
  135:- meta_predicate soap_call(:, +, -, +).  136soap_call(Operation, Input, Reply, Options) :-
  137   Operation = M:_,
  138%  Version = soap12,    % TBD: How to sort this out nicely
  139   wsdl_function(Operation, Version, URL, Action,
  140            InputElements, OutputElements), !,
  141   debug(soap, '~w: URL=~q', [Version, URL]),
  142   soap:soap_action(Action, Version, SoapOptions),
  143   assertion(length(InputElements, 1)),
  144   assertion(length(InputElements, 1)),
  145   InputElements = [arg(_Name, element(InputElement))],
  146   xml_schema:xsd_create_element(InputElement, M:Input, InputContentDOM0),
  147   soap:dom_local_ns(InputContentDOM0, InputContentDOM),
  148   soap:soap_version(Version, SoapPrefix, ContentType),
  149   InputDOM = element(SoapPrefix:'Envelope', [],
  150            [ element(SoapPrefix:'Body', [], [InputContentDOM])
  151            ]),
  152   (   debugging(soap)
  153   ->  http_post_data(xml(ContentType, InputDOM),
  154            user_error, [])
  155   ;   true
  156   ),
  157   setup_call_cleanup(
  158       http_open(URL, In,
  159            [ method(post),
  160         post(xml(ContentType, InputDOM)),
  161         cert_verify_hook(cert_verify),
  162         status_code(Code),
  163         header(content_type, ReplyContentType)
  164            | SoapOptions
  165            ]),
  166       soap:soap_read_reply(Code, ReplyContentType, In, ReplyDOM),
  167       close(In)),
  168   ( memberchk(dom, Options) ->
  169     Reply = ReplyDOM
  170   ; soap:soap_reply(Code, SoapPrefix, ReplyDOM, OutputElements, M, Reply))