cool / src / lib / FuzzyALCABox.ml @ b75e5a66
History  View  Annotate  Download (15.6 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 rec print_fuzzyDL concept = 
40 
match concept with 
41 
 TRUE > "*top*" 
42 
 FALSE > "*bottom*" 
43 
 AP(s) > s 
44 
 NOT(s) > "(not " ^ print_fuzzyDL s ^ ")" 
45 
 EXISTS(a, b) > "(some R" ^ string_of_int a ^ " " ^ print_fuzzyDL b ^ ")" 
46 
 FORALL(a, b) > "(all R" ^ string_of_int a ^ " " ^ print_fuzzyDL b ^ ")" 
47 
 AND(a, b) > "(and " ^ print_fuzzyDL a ^ " " ^ print_fuzzyDL b ^ ")" 
48 
 OR(a, b) > "(or " ^ print_fuzzyDL a ^ " " ^ print_fuzzyDL b ^ ")" 
49  
50 
let rec random_concept depth count atoms (weights : int list) = 
51 
snd (random_concept_int depth count atoms weights) 
52 
(* Returns: (Number of operators used, concept) *) 
53 
and random_concept_int depth count atoms weights = 
54 
let random_atomic a = 
55 
match (Random.int a) with 
56 
 0 > TRUE 
57 
 1 > AP("A") 
58 
 2 > AP("B") 
59 
 3 > AP("C") 
60 
 4 > AP("D") 
61 
 5 > AP("E") 
62 
 6 > AP("F") 
63 
 7 > AP("G") 
64 
 8 > AP("H") 
65 
 9 > AP("I") 
66 
 _ > AP("J") 
67 
in 
68 
let sumweights = List.fold_left (+) 0 weights in 
69 
(* 
70 
let f (sum, ret) elem = 
71 
(sum + elem, (sum+elem)::ret) 
72 
in 
73 
let summed = snd (List.fold_left f (0, []) weights) in 
74 
*) 
75 
let rnd = Random.int sumweights in 
76 
if (depth = 0  count = 0  (rnd < List.hd weights)) then 
77 
(0, random_atomic atoms) 
78 
else ( 
79 
let (u1, con1) = random_concept_int (depth  1) (count1) atoms weights in 
80 
let l2 = List.tl weights in 
81 
let s2 = List.hd weights in 
82 
if rnd < (s2 + List.hd l2) then 
83 
(u1+1, NOT(con1)) 
84 
else 
85 
(* Two operands of our operator *) 
86 
let l3 = List.tl l2 in 
87 
let s3 = s2 + List.hd l2 in 
88 
if rnd < (s3 + List.hd l3) then 
89 
let (u2, con2) = random_concept_int (depth  1) (count1u1) atoms weights in 
90 
(u1+u2+1, AND(con1, con2)) 
91 
else 
92 
(u1+1, EXISTS(Random.int 42, con1)) 
93 
) 
94  
95 
let rec count_operators concept = 
96 
match concept with 
97 
 TRUE > 0 
98 
 AP(_) > 0 
99 
 NOT(x) > 1 + count_operators x 
100 
 AND(x, y) > (count_operators x) + (count_operators y) + 1 
101 
 EXISTS(_, y) > 1 + (count_operators y) 
102  
103 
let rec random_concept_opcount depth count atoms weights = 
104 
let rec helper p = 
105 
let con = random_concept depth count atoms weights in 
106 
if (count_operators con) = count then con 
107 
else helper p 
108 
in 
109 
helper 1 
110  
111 
(* 
112 
let rec random_ABox depth_left depth_right = 
113 
let left = 
114 
if depth_left <> 0 then 
115 
[CONCEPT(0, random_concept (Random.int depth_left))] 
116 
else 
117 
[] 
118 
in 
119 
let right = 
120 
if depth_right <> 0 then 
121 
[CONCEPT(0, random_concept (Random.int depth_right))] 
122 
else 
123 
[] 
124 
in 
125 
(left, 0, right) 
126 
*) 
127  
128 
let lexer = A.make_lexer 
129 
[":";"(";")";"";"&";"~";"True";"False";"[";"]";"<";">";"+";".";";";","] 
130  
131 
let mk_exn s = CoAlgException s 
132  
133 
(** These functions parse a token stream to obtain a formula. 
134 
It is a standard recursive descent procedure. 
135 
@param ts A token stream. 
136 
@return The resulting (sub)formula. 
137 
@raise CoAlgException if ts does not represent a formula. 
138 
*) 
139 
let rec parse_asst ts = 
140 
let cur = match (Stream.next ts, Stream.next ts, Stream.peek ts) with 
141 
(* Concept *) 
142 
 (A.Int id, A.Kwd ":", _) > 
143 
CONCEPT(id, parse_or ts) 
144 
(* Role *) 
145 
 (A.Int i, A.Kwd ",", Some (A.Int j)) > 
146 
((* Discard j *) 
147 
Stream.junk ts; 
148 
(* Discard ":", TODO: Check this *) 
149 
Stream.junk ts; 
150 
let (A.Int k) = Stream.next ts in 
151 
ROLE(i, j, k)) 
152 
 _ > A.printError mk_exn ~ts ("Invalid concept.") 
153 
in 
154 
match Stream.peek ts with 
155 
 Some (A.Kwd "+") > 
156 
Stream.junk ts; 
157 
cur :: (parse_asst ts) 
158 
 _ > [cur] 
159  
160 
(** These functions parse a token stream to obtain a formula. 
161 
It is a standard recursive descent procedure. 
162 
@param ts A token stream. 
163 
@return The resulting (sub)formula. 
164 
@raise CoAlgException if ts does not represent a formula. 
165 
*) 
166 
and parse_or ts = 
167 
let f1 = parse_and ts in 
168 
match Stream.peek ts with 
169 
 None > f1 
170 
 Some (A.Kwd "") > 
171 
Stream.junk ts; 
172 
let f2 = parse_or ts in 
173 
OR (f1, f2) 
174 
 _ > f1 
175  
176 
(** These functions parse a token stream to obtain a formula. 
177 
It is a standard recursive descent procedure. 
178 
@param ts A token stream. 
179 
@return The resulting (sub)formula. 
180 
@raise CoAlgException if ts does not represent a formula. 
181 
*) 
182 
and parse_and ts = 
183 
let f1 = parse_rest ts in 
184 
match Stream.peek ts with 
185 
 None > f1 
186 
 Some (A.Kwd "&") > 
187 
Stream.junk ts; 
188 
let f2 = parse_and ts in 
189 
AND (f1, f2) 
190 
 _ > f1 
191  
192 
(** These functions parse a token stream to obtain a formula. 
193 
It is a standard recursive descent procedure. 
194 
@param ts A token stream. 
195 
@return The resulting (sub)formula. 
196 
@raise CoAlgException if ts does not represent a formula. 
197 
*) 
198 
and parse_rest ts = 
199 
match Stream.next ts with 
200 
 A.Kwd "True" > TRUE 
201 
 A.Kwd "False" > FALSE 
202 
 A.Ident s > AP s 
203 
 A.Kwd "~" > 
204 
let f = parse_rest ts in 
205 
NOT f 
206 
 A.Kwd "<" > 
207 
let name = 
208 
match Stream.next ts with 
209 
 A.Int sl > sl 
210 
 _ > A.printError mk_exn ~ts ("role id expected") 
211 
in 
212 
let f1 = parse_or ts in 
213 
let _ = 
214 
match Stream.next ts with 
215 
 A.Kwd c when c = ">" > "" 
216 
 _ > A.printError mk_exn ~ts ("\">\" expected: ") 
217 
in 
218 
EXISTS (name, f1) 
219 
 A.Kwd "[" > 
220 
let name = 
221 
match Stream.next ts with 
222 
 A.Int sl > sl 
223 
 _ > A.printError mk_exn ~ts ("role id expected") 
224 
in 
225 
let f1 = parse_or ts in 
226 
let _ = 
227 
match Stream.next ts with 
228 
 A.Kwd c when c = "]" > "" 
229 
 _ > A.printError mk_exn ~ts ("\"]\" expected: ") 
230 
in 
231 
FORALL (name, f1) 
232 
 A.Kwd "(" > begin 
233 
let f = parse_or ts in 
234 
match Stream.next ts with 
235 
 A.Kwd ")" > f 
236 
 t > A.printError mk_exn ~t ~ts "\")\" expected: " 
237 
end 
238 
 t > A.printError mk_exn ~t ~ts 
239 
"\"<\", \"[\", \"{>=\", \"{<=\", \"@\", \"~\", \"(\", \"True\", \"False\", or <ident> expected: " 
240  
241 
(** Parsees a assertion of the form "(role/concept assertions) >n (role/concept assertions)" *) 
242 
let rec parse_assertion ts = 
243 
(* Left side *) 
244 
let left = 
245 
match Stream.peek ts with 
246 
 Some (A.Kwd ">") > [] 
247 
 _ > parse_asst ts 
248 
in 
249 
(* Greater sign *) 
250 
let gr = 
251 
match (Stream.next ts, Stream.next ts) with 
252 
 (A.Kwd ">", A.Int i) > i 
253 
 _ > A.printError mk_exn ~ts ("Invalid assertion, \">(num)\" expected") 
254 
in 
255 
(* Right side *) 
256 
let right = 
257 
match Stream.peek ts with 
258 
 None > [] 
259 
 _ > parse_asst ts 
260 
in 
261 
(left, gr, right) 
262 

263 
(** Parses a sorted formula. 
264 
@param ts A token stream. 
265 
@return A sorted formula. 
266 
@raise CoAlgException If ts does not represent a sorted formula. 
267 
*) 
268 
let parse_sortedFormula ts = 
269 
parse_assertion ts 
270  
271 
(** Parses a list of sorted formulae separated by ";". 
272 
@param ts A token stream. 
273 
@param acc The list of sorted formulae parsed so far. 
274 
@return The resulting list of sorted formula. 
275 
@raise CoAlgException if ts does not represent a list of sorted formulae. 
276 
*) 
277 
let rec parse_SortedFormulaList ts acc = 
278 
let f1 = parse_sortedFormula ts in 
279 
match Stream.peek ts with 
280 
 Some (A.Kwd ";") > 
281 
Stream.junk ts; 
282 
if (Stream.peek ts) == None then 
283 
acc 
284 
else 
285 
parse_SortedFormulaList ts (f1::acc) 
286 
 _ > List.rev (f1::acc) 
287  
288 
(** A common wrapper for import functions. 
289 
@param fkt An import function. 
290 
@param s A string. 
291 
@return The object imported from s using fkt. 
292 
@raise CoAlgException If ts is not empty. 
293 
*) 
294 
let importWrapper fkt s = 
295 
let ts = lexer s in 
296 
try 
297 
let res = fkt ts [] in 
298 
let _ = 
299 
match Stream.peek ts with 
300 
 None > () 
301 
 Some _ > A.printError mk_exn ~ts "EOS expected: " 
302 
in 
303 
res 
304 
with Stream.Failure > A.printError mk_exn ~ts "unexpected EOS" 
305  
306 
(** Parses a string to obtain a formula. 
307 
@param s A string representing a formula. 
308 
@return The resulting formula. 
309 
@raise CoAlgException if s does not represent a formula. 
310 
*) 
311 
(*let importFormula s = importWrapper parse_asst s*) 
312  
313 
(** Parses a string to obtain a sorted formula. 
314 
@param s A string representing a sorted formula. 
315 
@return The sorted formula. 
316 
@raise CoAlgException If s does not represent a sorted formula. 
317 
*) 
318 
(*let importSortedFormula s = importWrapper parse_sortedFormula s*) 
319  
320 
(** Parses a string to obtain a (sorted) formula query. 
321 
@param s A string representing a formula query. 
322 
@return A pair (tbox, f) where 
323 
tbox is a list of sorted formulae representing the TBox; and 
324 
f is a sorted formula. 
325 
@raise CoAlgException if s does not represent a formula query. 
326 
*) 
327 
let importQuery s = 
328 
importWrapper parse_SortedFormulaList s 
329  
330 
let rec printConcept x = 
331 
match x with 
332 
 AP(a) > a 
333 
 OR (a, b) > "(" ^ printConcept a ^ "  " ^ printConcept b ^ ")" 
334 
 AND (a, b) > "(" ^ printConcept a ^ " & " ^ printConcept b ^ ")" 
335 
 NOT (a) > "~" ^ printConcept a 
336 
 FORALL (a, b) > "[" ^ (string_of_int a) ^ " " ^ printConcept b ^ "]" 
337 
 EXISTS (a, b) > "<" ^ (string_of_int a) ^ " " ^ printConcept b ^ ">" 
338 
 TRUE > "True" 
339 
 FALSE > "False" 
340  
341 
let rec printAsst s = 
342 
let convert ts = 
343 
match ts with 
344 
 CONCEPT(x, y) > (string_of_int x) ^ ":(" ^ (printConcept y) ^ ")" 
345 
 ROLE(a, b, c) > (string_of_int a) ^ "," ^ (string_of_int b) ^ ":" ^ (string_of_int c) 
346 
in 
347 
match s with 
348 
 [] > "" 
349 
 _ > List.fold_left (fun acc ts > acc ^ " + " ^ convert ts) (convert (List.hd s)) (List.tl s) 
350  
351 
let rec printAssertion s = 
352 
match s with 
353 
 (left, gr, right) > (printAsst left) ^ " >" ^ (string_of_int gr) ^ " " ^ (printAsst right) 
354  
355 
let rec assertionMap a f = 
356 
let g x = 
357 
match x with 
358 
 CONCEPT (a, b) > CONCEPT (a, f b) 
359 
 a > a 
360 
in 
361 
match a with 
362 
 (left, gr, right) > (List.map g left, gr, List.map g right) 
363  
364 
let rec replaceOrForall s = 
365 
let rec g x = 
366 
match x with 
367 
 FORALL (a, b) > NOT(EXISTS(a, NOT(g b))) 
368 
 OR (a, b) > NOT(AND(NOT a, NOT (g b))) 
369 
(* We don't touch these *) 
370 
 AP(a) > AP(a) 
371 
 AND(a, b) > AND(g a, g b) 
372 
 NOT(a) > NOT(g a) 
373 
 EXISTS(a, b) > EXISTS(a, g b) 
374 
 TRUE > TRUE 
375 
 FALSE > FALSE 
376 
in 
377 
assertionMap s g 
378  
379 
let rec collapseNeg s = 
380 
let rec f x = 
381 
match x with 
382 
 NOT(NOT(a)) > f a 
383 
 NOT(a) > NOT (f a) 
384 
 AP(a) > AP(a) 
385 
 OR(a, b) > OR(f a, f b) 
386 
 AND(a, b) > AND(f a, f b) 
387 
 FORALL(a, b) > FORALL(a, f b) 
388 
 EXISTS(a, b) > EXISTS(a, f b) 
389 
 a > a 
390 
in 
391 
assertionMap s f 
392  
393 
(** Hashconsed formulae, which are in negation normal form, 
394 
such that structural and physical equality coincide. 
395 
*) 
396 
type hcConcept = (hcConcept_node, concept) HC.hash_consed 
397 
and hcConcept_node = 
398 
 HCTRUE 
399 
 HCFALSE 
400 
 HCAP of string 
401 
 HCNOT of hcConcept 
402 
 HCOR of hcConcept * hcConcept 
403 
 HCAND of hcConcept * hcConcept 
404 
 HCEXISTS of int * hcConcept 
405 
 HCFORALL of int * hcConcept 
406  
407 
(** Determines whether two formula nodes are structurally equal. 
408 
@param f1 The first formula node. 
409 
@param f2 The second formula node. 
410 
@return True iff f1 and f2 are structurally equal. 
411 
*) 
412 
let equal_hcConcept_node f1 f2 = 
413 
match f1, f2 with 
414 
 HCTRUE, HCTRUE > true 
415 
 HCFALSE, HCFALSE > true 
416 
 HCAP s1, HCAP s2 > compare s1 s2 = 0 
417 
 HCNOT s1, HCNOT s2 > compare s1 s2 = 0 
418 
 HCOR (f1a, f1b), HCOR (f2a, f2b) 
419 
 HCAND (f1a, f1b), HCAND (f2a, f2b) > f1a == f2a && f1b == f2b 
420 
 HCEXISTS (s1, f1), HCEXISTS (s2, f2) 
421 
 HCFORALL (s1, f1), HCFORALL (s2, f2) > compare s1 s2 = 0 && f1 == f2 
422 
(* The rest could be shortened to  _ > false, 
423 
but then the compiler would not warn if the formula type is extended 
424 
and this function is not updated accordingly.*) 
425 
 HCTRUE, _ 
426 
 HCFALSE, _ 
427 
 HCAP _, _ 
428 
 HCNOT _, _ 
429 
 HCOR _, _ 
430 
 HCAND _, _ 
431 
 HCEXISTS _, _ 
432 
 HCFORALL _, _ > false 
433  
434 
(** Computes the hash value of a formula node. 
435 
@param f A formula node. 
436 
@return The hash value of f. 
437 
*) 
438 
let hash_hcConcept_node f = 
439 
match f with 
440 
 HCTRUE > 0 
441 
 HCFALSE > 1 
442 
 HCAP s > 19 * Hashtbl.hash s + 0 
443 
 HCNOT s > 19 * Hashtbl.hash s + 1 
444 
 HCOR (f1, f2) > 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 2 
445 
 HCAND (f1, f2) > 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 3 
446 
 HCEXISTS (s, f1) > 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 4 
447 
 HCFORALL (s, f1) > 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 5 
448  
449 
(** Determines the "real" formula of a formula node. 
450 
@param f A formula node. 
451 
@return The formula (in negation normal form) which corresponds to f. 
452 
*) 
453 
let toFml_hcConcept_node f = 
454 
match f with 
455 
 HCTRUE > TRUE 
456 
 HCFALSE > FALSE 
457 
 HCAP s > AP s 
458 
 HCNOT s > NOT s.HC.fml 
459 
 HCOR (f1, f2) > OR (f1.HC.fml, f2.HC.fml) 
460 
 HCAND (f1, f2) > AND (f1.HC.fml, f2.HC.fml) 
461 
 HCEXISTS (s, f1) > EXISTS (s, f1.HC.fml) 
462 
 HCFORALL (s, f1) > FORALL (s, f1.HC.fml) 
463  
464 
(** An instantiation of hashconsing for formulae. 
465 
*) 
466 
module HcFormula = HC.Make( 
467 
struct 
468 
type nde = hcConcept_node 
469 
type fml = concept 
470 
let equal (n1 : nde) n2 = equal_hcConcept_node n1 n2 
471 
let hash (n : nde) = hash_hcConcept_node n 
472 
let negNde (n : nde) = n (*negNde_hcConcept_node n*) 
473 
let toFml (n : nde) = toFml_hcConcept_node n 
474 
end 
475 
) 
476  
477 
(** Converts a formula into its hashconsed version. 
478 
@param hcF A hashcons table for formulae. 
479 
@param f A formula in negation normal form. 
480 
@return The hashconsed version of f. 
481 
@raise CoAlgException if f is not in negation normal form. 
482 
*) 
483 
let rec hc_formula hcF f = 
484 
match f with 
485 
 TRUE > HcFormula.hashcons hcF HCTRUE 
486 
 FALSE > HcFormula.hashcons hcF HCFALSE 
487 
 AP s > HcFormula.hashcons hcF (HCAP s) 
488 
 NOT s > HcFormula.hashcons hcF (HCNOT (hc_formula hcF s)) 
489 
 OR (f1, f2) > 
490 
let tf1 = hc_formula hcF f1 in 
491 
let tf2 = hc_formula hcF f2 in 
492 
HcFormula.hashcons hcF (HCOR (tf1, tf2)) 
493 
 AND (f1, f2) > 
494 
let tf1 = hc_formula hcF f1 in 
495 
let tf2 = hc_formula hcF f2 in 
496 
HcFormula.hashcons hcF (HCAND (tf1, tf2)) 
497 
 EXISTS (s, f1) > 
498 
let tf1 = hc_formula hcF f1 in 
499 
HcFormula.hashcons hcF (HCEXISTS (s, tf1)) 
500 
 FORALL (s, f1) > 
501 
let tf1 = hc_formula hcF f1 in 
502 
HcFormula.hashcons hcF (HCFORALL (s, tf1)) 
503  
504  
505 
(** An instantiation of a hash table (of the standard library) 
506 
for hashconsed formulae. The test for equality 
507 
and computing the hash value is done in constant time. 
508 
*) 
509 
module HcFHt = Hashtbl.Make( 
510 
struct 
511 
type t = hcConcept 
512 
let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag 
513 
let hash (f : t) = f.HC.tag 
514 
end 
515 
) 
516  
517 
type hcAsst = 
518 
 HCROLE of int * int * int 
519 
 HCCONCEPT of int * hcConcept 
520 
type hcAssertion = (hcAsst list) * int * (hcAsst list) 
521  
522 
let toAsst asst = 
523 
match asst with 
524 
 HCROLE(a, b, c) > ROLE(a, b, c) 
525 
 HCCONCEPT(a, hcFml) > CONCEPT(a, hcFml.fml) 
526  
527 
(* 
528 
let toAsst xs = 
529 
let f (left, gr, right) = 
530 
let g hcasst = 
531 
match hcasst with 
532 
 HCROLE(a, b, c) > ROLE(a, b, c) 
533 
 HCCONCEPT(a, hcFml) > CONCEPT(a, hcFml.fml) 
534 
in 
535 
(List.map g left, gr, List.map g right) 
536 
in 
537 
List.map f xs 
538 
*) 
539  
540 
let toHcAsst hcF asst = 
541 
match asst with 
542 
 ROLE(a, b, c) > HCROLE(a, b, c) 
543 
 CONCEPT(a, c) > HCCONCEPT(a, hc_formula hcF c) 