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
23
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 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 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 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:_,
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))