cool / src / lib / FuzzyALCABox.ml @ 17dae482
History  View  Annotate  Download (12.9 KB)
1 
(* 

2 
* vim: ts=2 sw=2 
3 
*) 
4 
(** This module implements fuzzy ALC formulae 
5 
(e.g. parsing, printing, (de)constructing, ...). 
6 
@author Florian Widmann / Dominik Paulus 
7 
*) 
8  
9 
module HC = HashConsing 
10 
module A = AltGenlex 
11 
module L = List 
12 
module Str = String 
13  
14 
(** A general exception for all kinds of errors 
15 
that can happen in the tableau procedure. 
16 
More specific information is given in the argument. 
17 
*) 
18 
exception CoAlgException of string 
19  
20 
(** Defines (unsorted) coalgebraic formulae. 
21 
*) 
22 
type concept = 
23 
 TRUE 
24 
 FALSE 
25 
 AP of string 
26 
 NOT of concept 
27 
 OR of concept * concept 
28 
 AND of concept * concept 
29 
 EXISTS of int * concept 
30 
 FORALL of int * concept 
31  
32 
type asst = 
33 
 ROLE of int * int * int 
34 
 CONCEPT of int * concept 
35 
type assertion = (asst list) * int * (asst list) 
36  
37 
exception ConversionException of concept 
38  
39 
let lexer = A.make_lexer 
40 
[":";"(";")";"";"&";"~";"True";"False";"[";"]";"<";">";"+";".";";";","] 
41  
42 
let mk_exn s = CoAlgException s 
43  
44 
(** These functions parse a token stream to obtain a formula. 
45 
It is a standard recursive descent procedure. 
46 
@param ts A token stream. 
47 
@return The resulting (sub)formula. 
48 
@raise CoAlgException if ts does not represent a formula. 
49 
*) 
50 
let rec parse_asst ts = 
51 
let cur = match (Stream.next ts, Stream.next ts, Stream.peek ts) with 
52 
(* Concept *) 
53 
 (A.Int id, A.Kwd ":", _) > 
54 
CONCEPT(id, parse_or ts) 
55 
(* Role *) 
56 
 (A.Int i, A.Kwd ",", Some (A.Int j)) > 
57 
((* Discard j *) 
58 
Stream.junk ts; 
59 
(* Discard ":", TODO: Check this *) 
60 
Stream.junk ts; 
61 
let (A.Int k) = Stream.next ts in 
62 
ROLE(i, j, k)) 
63 
 _ > A.printError mk_exn ~ts ("Invalid concept.") 
64 
in 
65 
match Stream.peek ts with 
66 
 Some (A.Kwd "+") > 
67 
Stream.junk ts; 
68 
cur :: (parse_asst ts) 
69 
 _ > [cur] 
70  
71 
(** These functions parse a token stream to obtain a formula. 
72 
It is a standard recursive descent procedure. 
73 
@param ts A token stream. 
74 
@return The resulting (sub)formula. 
75 
@raise CoAlgException if ts does not represent a formula. 
76 
*) 
77 
and parse_or ts = 
78 
let f1 = parse_and ts in 
79 
match Stream.peek ts with 
80 
 None > f1 
81 
 Some (A.Kwd "") > 
82 
Stream.junk ts; 
83 
let f2 = parse_or ts in 
84 
OR (f1, f2) 
85 
 _ > f1 
86  
87 
(** These functions parse a token stream to obtain a formula. 
88 
It is a standard recursive descent procedure. 
89 
@param ts A token stream. 
90 
@return The resulting (sub)formula. 
91 
@raise CoAlgException if ts does not represent a formula. 
92 
*) 
93 
and parse_and ts = 
94 
let f1 = parse_rest ts in 
95 
match Stream.peek ts with 
96 
 None > f1 
97 
 Some (A.Kwd "&") > 
98 
Stream.junk ts; 
99 
let f2 = parse_and ts in 
100 
AND (f1, f2) 
101 
 _ > f1 
102  
103 
(** These functions parse a token stream to obtain a formula. 
104 
It is a standard recursive descent procedure. 
105 
@param ts A token stream. 
106 
@return The resulting (sub)formula. 
107 
@raise CoAlgException if ts does not represent a formula. 
108 
*) 
109 
and parse_rest ts = 
110 
match Stream.next ts with 
111 
 A.Kwd "True" > TRUE 
112 
 A.Kwd "False" > FALSE 
113 
 A.Ident s > AP s 
114 
 A.Kwd "~" > 
115 
let f = parse_rest ts in 
116 
NOT f 
117 
 A.Kwd "<" > 
118 
let name = 
119 
match Stream.next ts with 
120 
 A.Int sl > sl 
121 
 _ > A.printError mk_exn ~ts ("role id expected") 
122 
in 
123 
let f1 = parse_or ts in 
124 
let _ = 
125 
match Stream.next ts with 
126 
 A.Kwd c when c = ">" > "" 
127 
 _ > A.printError mk_exn ~ts ("\">\" expected: ") 
128 
in 
129 
EXISTS (name, f1) 
130 
 A.Kwd "[" > 
131 
let name = 
132 
match Stream.next ts with 
133 
 A.Int sl > sl 
134 
 _ > A.printError mk_exn ~ts ("role id expected") 
135 
in 
136 
let f1 = parse_or ts in 
137 
let _ = 
138 
match Stream.next ts with 
139 
 A.Kwd c when c = "]" > "" 
140 
 _ > A.printError mk_exn ~ts ("\"]\" expected: ") 
141 
in 
142 
FORALL (name, f1) 
143 
 A.Kwd "(" > begin 
144 
let f = parse_or ts in 
145 
match Stream.next ts with 
146 
 A.Kwd ")" > f 
147 
 t > A.printError mk_exn ~t ~ts "\")\" expected: " 
148 
end 
149 
 t > A.printError mk_exn ~t ~ts 
150 
"\"<\", \"[\", \"{>=\", \"{<=\", \"@\", \"~\", \"(\", \"True\", \"False\", or <ident> expected: " 
151  
152 
(** Parsees a assertion of the form "(role/concept assertions) >n (role/concept assertions)" *) 
153 
let rec parse_assertion ts = 
154 
let getLeft = 
155 
match Stream.peek ts with 
156 
 Some (A.Kwd ">") > [] 
157 
 _ > parse_asst ts 
158 
in 
159 
let left = getLeft in 
160 
let gr = 
161 
match (Stream.next ts, Stream.next ts) with 
162 
 (A.Kwd ">", A.Int i) > i 
163 
 _ > A.printError mk_exn ~ts ("Invalid assertion, \">(num)\" expected") 
164 
in let right = parse_asst ts in 
165 
(left, gr, right) 
166 

167 
(** Parses a sorted formula. 
168 
@param ts A token stream. 
169 
@return A sorted formula. 
170 
@raise CoAlgException If ts does not represent a sorted formula. 
171 
*) 
172 
let parse_sortedFormula ts = 
173 
parse_assertion ts 
174  
175 
(** Parses a list of sorted formulae separated by ";". 
176 
@param ts A token stream. 
177 
@param acc The list of sorted formulae parsed so far. 
178 
@return The resulting list of sorted formula. 
179 
@raise CoAlgException if ts does not represent a list of sorted formulae. 
180 
*) 
181 
let rec parse_SortedFormulaList ts acc = 
182 
let f1 = parse_sortedFormula ts in 
183 
match Stream.peek ts with 
184 
 Some (A.Kwd ";") > 
185 
Stream.junk ts; 
186 
parse_SortedFormulaList ts (f1::acc) 
187 
 _ > List.rev (f1::acc) 
188  
189 
(** A common wrapper for import functions. 
190 
@param fkt An import function. 
191 
@param s A string. 
192 
@return The object imported from s using fkt. 
193 
@raise CoAlgException If ts is not empty. 
194 
*) 
195 
let importWrapper fkt s = 
196 
let ts = lexer s in 
197 
try 
198 
let res = fkt ts [] in 
199 
let _ = 
200 
match Stream.peek ts with 
201 
 None > () 
202 
 Some _ > A.printError mk_exn ~ts "EOS expected: " 
203 
in 
204 
res 
205 
with Stream.Failure > A.printError mk_exn ~ts "unexpected EOS" 
206  
207 
(** Parses a string to obtain a formula. 
208 
@param s A string representing a formula. 
209 
@return The resulting formula. 
210 
@raise CoAlgException if s does not represent a formula. 
211 
*) 
212 
(*let importFormula s = importWrapper parse_asst s*) 
213  
214 
(** Parses a string to obtain a sorted formula. 
215 
@param s A string representing a sorted formula. 
216 
@return The sorted formula. 
217 
@raise CoAlgException If s does not represent a sorted formula. 
218 
*) 
219 
(*let importSortedFormula s = importWrapper parse_sortedFormula s*) 
220  
221 
(** Parses a string to obtain a (sorted) formula query. 
222 
@param s A string representing a formula query. 
223 
@return A pair (tbox, f) where 
224 
tbox is a list of sorted formulae representing the TBox; and 
225 
f is a sorted formula. 
226 
@raise CoAlgException if s does not represent a formula query. 
227 
*) 
228 
let importQuery s = 
229 
importWrapper parse_SortedFormulaList s 
230  
231 
let rec printConcept x = 
232 
match x with 
233 
 AP(a) > a 
234 
 OR (a, b) > "(" ^ printConcept a ^ ")  (" ^ printConcept b ^ ")" 
235 
 AND (a, b) > "(" ^ printConcept a ^ ") & (" ^ printConcept b ^ ")" 
236 
 NOT (a) > "~(" ^ printConcept a ^ ")" 
237 
 FORALL (a, b) > "[" ^ (string_of_int a) ^ " " ^ printConcept b ^ "]" 
238 
 EXISTS (a, b) > "<" ^ (string_of_int a) ^ " " ^ printConcept b ^ ">" 
239 
 _ > "wtf" 
240  
241 
let rec printAsst s = 
242 
let convert ts = 
243 
match ts with 
244 
 CONCEPT(x, y) > (string_of_int x) ^ ":(" ^ (printConcept y) ^ ")" 
245 
 ROLE(a, b, c) > (string_of_int a) ^ "," ^ (string_of_int b) ^ ":" ^ (string_of_int c) 
246 
in 
247 
match s with 
248 
 [] > "0" 
249 
 _ > List.fold_left (fun acc ts > acc ^ " + " ^ convert ts) (convert (List.hd s)) (List.tl s) 
250  
251 
let rec printAssertion s = 
252 
match s with 
253 
 (left, gr, right) > (printAsst left) ^ " >" ^ (string_of_int gr) ^ " " ^ (printAsst right) 
254  
255 
let rec assertionMap a f = 
256 
let g x = 
257 
match x with 
258 
 CONCEPT (a, b) > CONCEPT (a, f b) 
259 
 a > a 
260 
in 
261 
match a with 
262 
 (left, gr, right) > (List.map g left, gr, List.map g right) 
263  
264 
let rec replaceOrForall s = 
265 
let rec g x = 
266 
match x with 
267 
 FORALL (a, b) > NOT(EXISTS(a, NOT(g b))) 
268 
 OR (a, b) > NOT(AND(NOT a, NOT (g b))) 
269 
(* We don't touch these *) 
270 
 AP(a) > AP(a) 
271 
 AND(a, b) > AND(g a, g b) 
272 
 NOT(a) > NOT(g a) 
273 
 EXISTS(a, b) > EXISTS(a, g b) 
274 
 TRUE > TRUE 
275 
 FALSE > FALSE 
276 
in 
277 
assertionMap s g 
278  
279 
let rec collapseNeg s = 
280 
let rec f x = 
281 
match x with 
282 
 NOT(NOT(a)) > f a 
283 
 NOT(a) > NOT (f a) 
284 
 AP(a) > AP(a) 
285 
 OR(a, b) > OR(f a, f b) 
286 
 AND(a, b) > AND(f a, f b) 
287 
 FORALL(a, b) > FORALL(a, f b) 
288 
 EXISTS(a, b) > EXISTS(a, f b) 
289 
 a > a 
290 
in 
291 
assertionMap s f 
292  
293 
(** Hashconsed formulae, which are in negation normal form, 
294 
such that structural and physical equality coincide. 
295 
*) 
296 
type hcConcept = (hcConcept_node, concept) HC.hash_consed 
297 
and hcConcept_node = 
298 
 HCTRUE 
299 
 HCFALSE 
300 
 HCAP of string 
301 
 HCNOT of hcConcept 
302 
 HCOR of hcConcept * hcConcept 
303 
 HCAND of hcConcept * hcConcept 
304 
 HCEXISTS of int * hcConcept 
305 
 HCFORALL of int * hcConcept 
306  
307 
(** Determines whether two formula nodes are structurally equal. 
308 
@param f1 The first formula node. 
309 
@param f2 The second formula node. 
310 
@return True iff f1 and f2 are structurally equal. 
311 
*) 
312 
let equal_hcConcept_node f1 f2 = 
313 
match f1, f2 with 
314 
 HCTRUE, HCTRUE > true 
315 
 HCFALSE, HCFALSE > true 
316 
 HCAP s1, HCAP s2 > compare s1 s2 = 0 
317 
 HCNOT s1, HCNOT s2 > compare s1 s2 = 0 
318 
 HCOR (f1a, f1b), HCOR (f2a, f2b) 
319 
 HCAND (f1a, f1b), HCAND (f2a, f2b) > f1a == f2a && f1b == f2b 
320 
 HCEXISTS (s1, f1), HCEXISTS (s2, f2) 
321 
 HCFORALL (s1, f1), HCFORALL (s2, f2) > compare s1 s2 = 0 && f1 == f2 
322 
(* The rest could be shortened to  _ > false, 
323 
but then the compiler would not warn if the formula type is extended 
324 
and this function is not updated accordingly.*) 
325 
 HCTRUE, _ 
326 
 HCFALSE, _ 
327 
 HCAP _, _ 
328 
 HCNOT _, _ 
329 
 HCOR _, _ 
330 
 HCAND _, _ 
331 
 HCEXISTS _, _ 
332 
 HCFORALL _, _ > false 
333  
334 
(** Computes the hash value of a formula node. 
335 
@param f A formula node. 
336 
@return The hash value of f. 
337 
*) 
338 
let hash_hcConcept_node f = 
339 
match f with 
340 
 HCTRUE > 0 
341 
 HCFALSE > 1 
342 
 HCAP s > 19 * Hashtbl.hash s + 0 
343 
 HCNOT s > 19 * Hashtbl.hash s + 1 
344 
 HCOR (f1, f2) > 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 2 
345 
 HCAND (f1, f2) > 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 3 
346 
 HCEXISTS (s, f1) > 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 4 
347 
 HCFORALL (s, f1) > 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 5 
348  
349 
(** Determines the "real" formula of a formula node. 
350 
@param f A formula node. 
351 
@return The formula (in negation normal form) which corresponds to f. 
352 
*) 
353 
let toFml_hcConcept_node f = 
354 
match f with 
355 
 HCTRUE > TRUE 
356 
 HCFALSE > FALSE 
357 
 HCAP s > AP s 
358 
 HCNOT s > NOT s.HC.fml 
359 
 HCOR (f1, f2) > OR (f1.HC.fml, f2.HC.fml) 
360 
 HCAND (f1, f2) > AND (f1.HC.fml, f2.HC.fml) 
361 
 HCEXISTS (s, f1) > EXISTS (s, f1.HC.fml) 
362 
 HCFORALL (s, f1) > FORALL (s, f1.HC.fml) 
363  
364 
(** An instantiation of hashconsing for formulae. 
365 
*) 
366 
module HcFormula = HC.Make( 
367 
struct 
368 
type nde = hcConcept_node 
369 
type fml = concept 
370 
let equal (n1 : nde) n2 = equal_hcConcept_node n1 n2 
371 
let hash (n : nde) = hash_hcConcept_node n 
372 
let negNde (n : nde) = n (*negNde_hcConcept_node n*) 
373 
let toFml (n : nde) = toFml_hcConcept_node n 
374 
end 
375 
) 
376  
377 
(** Converts a formula into its hashconsed version. 
378 
@param hcF A hashcons table for formulae. 
379 
@param f A formula in negation normal form. 
380 
@return The hashconsed version of f. 
381 
@raise CoAlgException if f is not in negation normal form. 
382 
*) 
383 
let rec hc_formula hcF f = 
384 
match f with 
385 
 TRUE > HcFormula.hashcons hcF HCTRUE 
386 
 FALSE > HcFormula.hashcons hcF HCFALSE 
387 
 AP s > HcFormula.hashcons hcF (HCAP s) 
388 
 NOT s > HcFormula.hashcons hcF (HCNOT (hc_formula hcF s)) 
389 
 OR (f1, f2) > 
390 
let tf1 = hc_formula hcF f1 in 
391 
let tf2 = hc_formula hcF f2 in 
392 
HcFormula.hashcons hcF (HCOR (tf1, tf2)) 
393 
 AND (f1, f2) > 
394 
let tf1 = hc_formula hcF f1 in 
395 
let tf2 = hc_formula hcF f2 in 
396 
HcFormula.hashcons hcF (HCAND (tf1, tf2)) 
397 
 EXISTS (s, f1) > 
398 
let tf1 = hc_formula hcF f1 in 
399 
HcFormula.hashcons hcF (HCEXISTS (s, tf1)) 
400 
 FORALL (s, f1) > 
401 
let tf1 = hc_formula hcF f1 in 
402 
HcFormula.hashcons hcF (HCFORALL (s, tf1)) 
403  
404  
405 
(** An instantiation of a hash table (of the standard library) 
406 
for hashconsed formulae. The test for equality 
407 
and computing the hash value is done in constant time. 
408 
*) 
409 
module HcFHt = Hashtbl.Make( 
410 
struct 
411 
type t = hcConcept 
412 
let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag 
413 
let hash (f : t) = f.HC.tag 
414 
end 
415 
) 
416  
417 
type hcAsst = 
418 
 HCROLE of int * int * int 
419 
 HCCONCEPT of int * hcConcept 
420 
type hcAssertion = (hcAsst list) * int * (hcAsst list) 
421  
422 
let toAsst asst = 
423 
match asst with 
424 
 HCROLE(a, b, c) > ROLE(a, b, c) 
425 
 HCCONCEPT(a, hcFml) > CONCEPT(a, hcFml.fml) 
426  
427 
(* 
428 
let toAsst xs = 
429 
let f (left, gr, right) = 
430 
let g hcasst = 
431 
match hcasst with 
432 
 HCROLE(a, b, c) > ROLE(a, b, c) 
433 
 HCCONCEPT(a, hcFml) > CONCEPT(a, hcFml.fml) 
434 
in 
435 
(List.map g left, gr, List.map g right) 
436 
in 
437 
List.map f xs 
438 
*) 
439  
440 
let toHcAsst hcF asst = 
441 
match asst with 
442 
 ROLE(a, b, c) > HCROLE(a, b, c) 
443 
 CONCEPT(a, c) > HCCONCEPT(a, hc_formula hcF c) 