Project

General

Profile

Statistics
| Branch: | Revision:

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
(** Hash-consed 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 hash-consing 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 hash-consed version.
378
    @param hcF A hash-cons table for formulae.
379
    @param f A formula in negation normal form.
380
    @return The hash-consed 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 hash-consed 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)