## cool / src / lib / ALCFormula.ml @ de84f40d

History | View | Annotate | Download (54.2 KB)

1 | 4fd28192 | Thorsten Wißmann | (** This module implements ALC formulae |
---|---|---|---|

2 | including inverse roles |
||

3 | (e.g. parsing, printing, (de-)constructing, ...). |
||

4 | @author Florian Widmann |
||

5 | *) |
||

6 | |||

7 | |||

8 | module HC = HashConsing |
||

9 | module A = AltGenlex |
||

10 | |||

11 | |||

12 | (** A general exception for all kinds of errors |
||

13 | that can happen in the tableau procedure. |
||

14 | More specific information is given in the argument. |
||

15 | *) |
||

16 | exception ALCException of string |
||

17 | |||

18 | |||

19 | (** Defines ALC formulae. |
||

20 | *) |
||

21 | type formula = |
||

22 | | TRUE |
||

23 | | FALSE |
||

24 | | AP of string |
||

25 | | NOT of formula |
||

26 | | EX of string * bool * formula |
||

27 | | AX of string * bool * formula |
||

28 | | MIN of int * string * bool * formula |
||

29 | | MAX of int * string * bool * formula |
||

30 | | EQU of formula * formula |
||

31 | | IMP of formula * formula |
||

32 | | OR of formula * formula |
||

33 | | AND of formula * formula |
||

34 | |||

35 | (** Defines TBox definitions. |
||

36 | It can either be a primitive definition |
||

37 | of the form cn <= f, |
||

38 | or a necessary and sufficient definition |
||

39 | of the form cn = f |
||

40 | (where cn is a concept name and f a concept). |
||

41 | *) |
||

42 | type definition = |
||

43 | | PRIMITIVE of string * formula |
||

44 | | NECANDSUFF of string * formula |
||

45 | |||

46 | (** The number of constructors of type formula. |
||

47 | *) |
||

48 | let numberOfTypes = 12 |
||

49 | |||

50 | (** Maps a formula to an integer representing its type (e.g. or-formula). |
||

51 | The assignment of integers to types is arbitrary, |
||

52 | but it is guaranteed that different types |
||

53 | map to different integers |
||

54 | and that the codomain of this function is [0..numberOfTypes-1]. |
||

55 | @param f A formula. |
||

56 | @return An integer that represents the type of f. |
||

57 | *) |
||

58 | let getTypeFormula f = |
||

59 | match f with |
||

60 | | TRUE -> 0 |
||

61 | | FALSE -> 1 |
||

62 | | AP _ -> 2 |
||

63 | | NOT _ -> 3 |
||

64 | | EX _ -> 4 |
||

65 | | AX _ -> 5 |
||

66 | | EQU _ -> 6 |
||

67 | | IMP _ -> 7 |
||

68 | | OR _ -> 8 |
||

69 | | AND _ -> 9 |
||

70 | | MIN _ -> 10 |
||

71 | | MAX _ -> 11 |
||

72 | |||

73 | (** Generates a function comp that compares two formula. |
||

74 | The order that is defined by comp is lexicograhic. |
||

75 | It depends on the given ranking of types of formulae. |
||

76 | @param order A list containing exactly the numbers 0 to numberOfTypes-1. |
||

77 | Each number represents a type |
||

78 | and the list therefore induces a ranking on the types |
||

79 | with the smallest type being the first in the list. |
||

80 | @return A function comp that compares two formula. |
||

81 | comp f1 f2 returns 0 iff f1 is equal to f2, |
||

82 | -1 if f1 is smaller than f2, and |
||

83 | 1 if f1 is greater than f2. |
||

84 | @raise Failure if order is not of the required form. |
||

85 | *) |
||

86 | let generateCompare order = |
||

87 | let rec listOK = function |
||

88 | | 0 -> true |
||

89 | | n -> |
||

90 | let nn = pred n in |
||

91 | if List.mem nn order then listOK nn |
||

92 | else false |
||

93 | in |
||

94 | let _ = |
||

95 | if (List.length order <> numberOfTypes) || not (listOK numberOfTypes) then |
||

96 | raise (Failure "generateCompare: argument is not in the correct form") |
||

97 | in |
||

98 | let arrayOrder = Array.make numberOfTypes 0 in |
||

99 | let _ = |
||

100 | for i = 0 to (numberOfTypes - 1) do |
||

101 | let ty = List.nth order i in |
||

102 | arrayOrder.(ty) <- i |
||

103 | done |
||

104 | in |
||

105 | let rec comp f1 f2 = |
||

106 | match f1, f2 with |
||

107 | | TRUE, TRUE |
||

108 | | FALSE, FALSE -> 0 |
||

109 | | AP s1, AP s2 -> compare s1 s2 |
||

110 | | NOT f1a, NOT f2a -> comp f1a f2a |
||

111 | | EX (s1, i1, f1a), EX (s2, i2, f2a) |
||

112 | | AX (s1, i1, f1a), AX (s2, i2, f2a) -> |
||

113 | let res1 = compare s1 s2 in |
||

114 | if res1 <> 0 then res1 |
||

115 | else |
||

116 | let res2 = compare i1 i2 in |
||

117 | if res2 <> 0 then res2 |
||

118 | else comp f1a f2a |
||

119 | | MIN (n1, s1, i1, f1a), MIN (n2, s2, i2, f2a) |
||

120 | | MAX (n1, s1, i1, f1a), MAX (n2, s2, i2, f2a) -> |
||

121 | let res0 = compare n1 n2 in |
||

122 | if res0 <> 0 then res0 |
||

123 | else |
||

124 | let res1 = compare s1 s2 in |
||

125 | if res1 <> 0 then res1 |
||

126 | else |
||

127 | let res2 = compare i1 i2 in |
||

128 | if res2 <> 0 then res2 |
||

129 | else comp f1a f2a |
||

130 | | OR (f1a, f1b), OR (f2a, f2b) |
||

131 | | AND (f1a, f1b), AND (f2a, f2b) |
||

132 | | EQU (f1a, f1b), EQU (f2a, f2b) |
||

133 | | IMP (f1a, f1b), IMP (f2a, f2b) -> |
||

134 | let res1 = comp f1a f2a in |
||

135 | if res1 <> 0 then res1 |
||

136 | else comp f1b f2b |
||

137 | | _ -> |
||

138 | let t1 = getTypeFormula f1 in |
||

139 | let r1 = arrayOrder.(t1) in |
||

140 | let t2 = getTypeFormula f2 in |
||

141 | let r2 = arrayOrder.(t2) in |
||

142 | if r1 < r2 then (-1) else 1 |
||

143 | in |
||

144 | comp |
||

145 | |||

146 | (** Defines a ranking of the different types of formulae |
||

147 | such that the ranking of the types corresponds |
||

148 | to the ranking of the tableau rules. |
||

149 | *) |
||

150 | let aRanking = [ getTypeFormula (OR (TRUE, TRUE)); |
||

151 | getTypeFormula (EX ("", false, TRUE)); |
||

152 | getTypeFormula (AX ("", false, TRUE)); |
||

153 | getTypeFormula TRUE; |
||

154 | getTypeFormula FALSE; |
||

155 | getTypeFormula (AP ""); |
||

156 | getTypeFormula (NOT TRUE); |
||

157 | getTypeFormula (AND (TRUE, TRUE)); |
||

158 | getTypeFormula (EQU (TRUE, TRUE)); |
||

159 | getTypeFormula (IMP (TRUE, TRUE)); |
||

160 | getTypeFormula (MIN (0, "", false, TRUE)); |
||

161 | getTypeFormula (MAX (0, "", false, TRUE)) ] |
||

162 | |||

163 | |||

164 | (** Determines the size of a formula. |
||

165 | Basically, it counts the symbols (without parentheses) of a formula, |
||

166 | where <r> _ etc. is treated as one symbol. |
||

167 | @param f A formula. |
||

168 | @return The size of f. |
||

169 | *) |
||

170 | let rec sizeFormula f = |
||

171 | match f with |
||

172 | | TRUE |
||

173 | | FALSE |
||

174 | | AP _ -> 1 |
||

175 | | NOT f1 |
||

176 | | EX (_, _, f1) |
||

177 | | AX (_, _, f1) |
||

178 | | MIN (_, _, _, f1) |
||

179 | | MAX (_, _, _, f1) -> succ (sizeFormula f1) |
||

180 | | EQU (f1, f2) |
||

181 | | IMP (f1, f2) |
||

182 | | OR (f1, f2) |
||

183 | | AND (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2) |
||

184 | |||

185 | |||

186 | (** Appends a string representation of a formula to a string buffer. |
||

187 | Parentheses are ommited where possible |
||

188 | where the preference rules are defined as usual. |
||

189 | @param sb A string buffer. |
||

190 | @param f A formula. |
||

191 | *) |
||

192 | let rec exportFormula_buffer sb f = |
||

193 | let prio n lf = |
||

194 | let prionr = function |
||

195 | | EQU _ -> 0 |
||

196 | | IMP _ -> 1 |
||

197 | | OR _ -> 2 |
||

198 | | AND _ -> 3 |
||

199 | | _ -> 4 |
||

200 | in |
||

201 | if prionr lf < n then begin |
||

202 | Buffer.add_char sb '('; |
||

203 | exportFormula_buffer sb lf; |
||

204 | Buffer.add_char sb ')' |
||

205 | end |
||

206 | else exportFormula_buffer sb lf |
||

207 | in |
||

208 | match f with |
||

209 | | TRUE -> Buffer.add_string sb "True" |
||

210 | | FALSE -> Buffer.add_string sb "False" |
||

211 | | AP s -> Buffer.add_string sb s |
||

212 | | NOT f1 -> |
||

213 | Buffer.add_string sb "~"; |
||

214 | prio 4 f1 |
||

215 | | EX (s, i1, f1) -> |
||

216 | Buffer.add_string sb "<"; |
||

217 | Buffer.add_string sb s; |
||

218 | if i1 then Buffer.add_string sb "-" else (); |
||

219 | Buffer.add_string sb ">"; |
||

220 | prio 4 f1 |
||

221 | | AX (s, i1, f1) -> |
||

222 | Buffer.add_string sb "["; |
||

223 | Buffer.add_string sb s; |
||

224 | if i1 then Buffer.add_string sb "-" else (); |
||

225 | Buffer.add_string sb "]"; |
||

226 | prio 4 f1 |
||

227 | | MIN (n, s, i1, f1) -> |
||

228 | Buffer.add_string sb "{>="; |
||

229 | Buffer.add_string sb (string_of_int n); |
||

230 | Buffer.add_string sb " "; |
||

231 | Buffer.add_string sb s; |
||

232 | if i1 then Buffer.add_string sb "-" else (); |
||

233 | Buffer.add_string sb "}"; |
||

234 | prio 4 f1 |
||

235 | | MAX (n, s, i1, f1) -> |
||

236 | Buffer.add_string sb "{<="; |
||

237 | Buffer.add_string sb (string_of_int n); |
||

238 | Buffer.add_string sb " "; |
||

239 | Buffer.add_string sb s; |
||

240 | if i1 then Buffer.add_string sb "-" else (); |
||

241 | Buffer.add_string sb "}"; |
||

242 | prio 4 f1 |
||

243 | | EQU (f1, f2) -> |
||

244 | prio 0 f1; |
||

245 | Buffer.add_string sb " <=> "; |
||

246 | prio 0 f2 |
||

247 | | IMP (f1, f2) -> |
||

248 | prio 2 f1; |
||

249 | Buffer.add_string sb " => "; |
||

250 | prio 2 f2 |
||

251 | | OR (f1, f2) -> |
||

252 | prio 2 f1; |
||

253 | Buffer.add_string sb " | "; |
||

254 | prio 2 f2 |
||

255 | | AND (f1, f2) -> |
||

256 | prio 3 f1; |
||

257 | Buffer.add_string sb " & "; |
||

258 | prio 3 f2 |
||

259 | |||

260 | (** Converts a formula into a string representation. |
||

261 | Parentheses are ommited where possible |
||

262 | where the preference rules are defined as usual. |
||

263 | @param f A formula. |
||

264 | @return A string representing f. |
||

265 | *) |
||

266 | let exportFormula f = |
||

267 | let size = sizeFormula f in |
||

268 | let sb = Buffer.create (2 * size) in |
||

269 | exportFormula_buffer sb f; |
||

270 | Buffer.contents sb |
||

271 | |||

272 | (** Converts a formula query into a string representation. |
||

273 | @param fl A list of formulae representing the initial input. |
||

274 | @param tboxND A list of formulae representing |
||

275 | the non-definitional part of a TBox. |
||

276 | @param tboxD A list of definitions |
||

277 | representing the definitional part of a TBox. |
||

278 | @return A string representing tboxND; tboxD |- fl. |
||

279 | @raise ALCException Iff one of the defined formulae in tboxD |
||

280 | is not a concept. |
||

281 | *) |
||

282 | let exportQuery fl tboxND tboxD = |
||

283 | let sb = Buffer.create 1000 in |
||

284 | let exportDef = function |
||

285 | | PRIMITIVE (s, f) -> |
||

286 | Buffer.add_string sb s; |
||

287 | Buffer.add_string sb " # "; |
||

288 | exportFormula_buffer sb f |
||

289 | | NECANDSUFF (s, f) -> |
||

290 | Buffer.add_string sb s; |
||

291 | Buffer.add_string sb " = "; |
||

292 | exportFormula_buffer sb f |
||

293 | in |
||

294 | let rec expFl fkt = function |
||

295 | | [] -> () |
||

296 | | h::tl -> |
||

297 | fkt h; |
||

298 | if tl <> [] then Buffer.add_string sb "; " else (); |
||

299 | expFl fkt tl |
||

300 | in |
||

301 | expFl (exportFormula_buffer sb) tboxND; |
||

302 | if tboxND <> [] && tboxD <> [] then Buffer.add_string sb "; " else (); |
||

303 | expFl exportDef tboxD; |
||

304 | Buffer.add_string sb " |- "; |
||

305 | expFl (exportFormula_buffer sb) fl; |
||

306 | Buffer.contents sb |
||

307 | |||

308 | |||

309 | let lexer = A.make_lexer |
||

310 | ["#";"=";"|-";";";"(";")";"=>";"<=>";"|";"&";"~";"True";"False";"<";">";"[";"]";"-";"{<=";"{>=";"}"] |
||

311 | |||

312 | let mk_exn s = ALCException s |
||

313 | |||

314 | (** These functions parse a token stream to obtain a formula. |
||

315 | It is a standard recursive descent procedure. |
||

316 | @param ts A token stream. |
||

317 | @return The resulting (sub-)formula. |
||

318 | @raise ALCException if ts does not represent a formula. |
||

319 | *) |
||

320 | let rec parse_equ ts = |
||

321 | let f1 = parse_imp ts in |
||

322 | match Stream.peek ts with |
||

323 | | None -> f1 |
||

324 | | Some (A.Kwd "<=>") -> |
||

325 | Stream.junk ts; |
||

326 | let f2 = parse_equ ts in |
||

327 | EQU (f1, f2) |
||

328 | | _ -> f1 |
||

329 | |||

330 | (** These functions parse a token stream to obtain a formula. |
||

331 | It is a standard recursive descent procedure. |
||

332 | @param ts A token stream. |
||

333 | @return The resulting (sub-)formula. |
||

334 | @raise ALCException if ts does not represent a formula. |
||

335 | *) |
||

336 | and parse_imp ts = |
||

337 | let f1 = parse_or ts in |
||

338 | match Stream.peek ts with |
||

339 | | None -> f1 |
||

340 | | Some (A.Kwd "=>") -> |
||

341 | Stream.junk ts; |
||

342 | let f2 = parse_imp ts in |
||

343 | IMP (f1, f2) |
||

344 | | _ -> f1 |
||

345 | |||

346 | (** These functions parse a token stream to obtain a formula. |
||

347 | It is a standard recursive descent procedure. |
||

348 | @param ts A token stream. |
||

349 | @return The resulting (sub-)formula. |
||

350 | @raise ALCException if ts does not represent a formula. |
||

351 | *) |
||

352 | and parse_or ts = |
||

353 | let f1 = parse_and ts in |
||

354 | match Stream.peek ts with |
||

355 | | None -> f1 |
||

356 | | Some (A.Kwd "|") -> |
||

357 | Stream.junk ts; |
||

358 | let f2 = parse_or ts in |
||

359 | OR (f1, f2) |
||

360 | | _ -> f1 |
||

361 | |||

362 | (** These functions parse a token stream to obtain a formula. |
||

363 | It is a standard recursive descent procedure. |
||

364 | @param ts A token stream. |
||

365 | @return The resulting (sub-)formula. |
||

366 | @raise ALCException if ts does not represent a formula. |
||

367 | *) |
||

368 | and parse_and ts = |
||

369 | let f1 = parse_rest ts in |
||

370 | match Stream.peek ts with |
||

371 | | None -> f1 |
||

372 | | Some (A.Kwd "&") -> |
||

373 | Stream.junk ts; |
||

374 | let f2 = parse_and ts in |
||

375 | AND (f1, f2) |
||

376 | | _ -> f1 |
||

377 | |||

378 | (** These functions parse a token stream to obtain a formula. |
||

379 | It is a standard recursive descent procedure. |
||

380 | @param ts A token stream. |
||

381 | @return The resulting (sub-)formula. |
||

382 | @raise ALCException if ts does not represent a formula. |
||

383 | *) |
||

384 | and parse_rest ts = |
||

385 | let boxinternals noNo es = |
||

386 | let n = |
||

387 | if noNo then 0 |
||

388 | else |
||

389 | match Stream.next ts with |
||

390 | | A.Int n when n >= 0 -> n |
||

391 | | t -> A.printError mk_exn ~t ~ts "<non-negative number> expected: " |
||

392 | in |
||

393 | let s = |
||

394 | match Stream.peek ts with |
||

395 | | Some (A.Ident s1) -> Stream.junk ts; s1 |
||

396 | | Some (A.Kwd c) when c = es -> "" |
||

397 | | Some (A.Kwd "-") -> "" |
||

398 | | Some t -> A.printError mk_exn ~ts ("role name, \"-\", or \"" ^ es ^ "\" expected: ") |
||

399 | | None -> A.printError mk_exn ~ts ("role name, \"-\", or \"" ^ es ^ "\" expected: ") |
||

400 | in |
||

401 | let isInv = |
||

402 | match Stream.next ts with |
||

403 | | A.Kwd c when c = es -> false |
||

404 | | A.Kwd "-" -> begin |
||

405 | match Stream.next ts with |
||

406 | | A.Kwd c when c = es -> true |
||

407 | | t -> A.printError mk_exn ~t ~ts ("\"" ^ es ^ "\" expected: ") |
||

408 | end |
||

409 | | t -> A.printError mk_exn ~t ~ts ("\"-\" or \"" ^ es ^ "\" expected: ") |
||

410 | in |
||

411 | (n, s, isInv) |
||

412 | in |
||

413 | match Stream.next ts with |
||

414 | | A.Kwd "<" -> |
||

415 | let (_, s, isInv) = boxinternals true ">" in |
||

416 | let f1 = parse_rest ts in |
||

417 | EX (s, isInv, f1) |
||

418 | | A.Kwd "[" -> |
||

419 | let (_, s, isInv) = boxinternals true "]" in |
||

420 | let f1 = parse_rest ts in |
||

421 | AX (s, isInv, f1) |
||

422 | | A.Kwd "{>=" -> |
||

423 | let (n, s, isInv) = boxinternals false "}" in |
||

424 | let f1 = parse_rest ts in |
||

425 | MIN (n, s, isInv, f1) |
||

426 | | A.Kwd "{<=" -> |
||

427 | let (n, s, isInv) = boxinternals false "}" in |
||

428 | let f1 = parse_rest ts in |
||

429 | MAX (n, s, isInv, f1) |
||

430 | | A.Kwd "(" -> |
||

431 | let f = parse_equ ts in |
||

432 | let _ = |
||

433 | match Stream.next ts with |
||

434 | | A.Kwd ")" -> () |
||

435 | | t -> A.printError mk_exn ~t ~ts "\")\" expected: " |
||

436 | in |
||

437 | f |
||

438 | | A.Kwd "~" -> |
||

439 | let f = parse_rest ts in |
||

440 | NOT f |
||

441 | | A.Kwd "True" -> TRUE |
||

442 | | A.Kwd "False" -> FALSE |
||

443 | | A.Ident s -> AP s |
||

444 | | t -> A.printError mk_exn ~t ~ts |
||

445 | "\"<\", \"[\", \"~\", \"(\", \"True\", \"False\", or <ident> expected: " |
||

446 | |||

447 | (** Parses a string to obtain a formula. |
||

448 | @param s A string representing a formula. |
||

449 | @return The resulting formula. |
||

450 | @raise ALCException if s does not represent a formula. |
||

451 | *) |
||

452 | let importFormula s = |
||

453 | let ts = lexer s in |
||

454 | try |
||

455 | begin |
||

456 | let f = parse_equ ts in |
||

457 | let _ = |
||

458 | match Stream.peek ts with |
||

459 | | None -> () |
||

460 | | Some _ -> A.printError mk_exn ~ts "EOS expected: " |
||

461 | in |
||

462 | f |
||

463 | end |
||

464 | with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS" |
||

465 | |||

466 | |||

467 | (** Parses a list of formulae separated by ";". |
||

468 | @param wDef Iff set to true then definitions are allowed. |
||

469 | @param ts A token stream. |
||

470 | @param accF The list of formulae parsed so far. |
||

471 | @param accD The list of definitions parsed so far. |
||

472 | @return The resulting lists of formulae and definitions. |
||

473 | @raise ALCException if ts does not represent a list of formulae |
||

474 | and definitions (if allowed). |
||

475 | *) |
||

476 | let rec parse_formulaeDefList wDef ts (accF, accD) = |
||

477 | let defopt = |
||

478 | if not wDef then None |
||

479 | else |
||

480 | let p2 = Stream.npeek 2 ts in |
||

481 | if List.length p2 < 2 then None |
||

482 | else |
||

483 | match List.hd p2 with |
||

484 | | A.Ident s1 -> begin |
||

485 | match List.nth p2 1 with |
||

486 | | A.Kwd "=" -> |
||

487 | Stream.junk ts; |
||

488 | Stream.junk ts; |
||

489 | let f1 = parse_equ ts in |
||

490 | Some (NECANDSUFF (s1, f1)) |
||

491 | | A.Kwd "#" -> |
||

492 | Stream.junk ts; |
||

493 | Stream.junk ts; |
||

494 | let f1 = parse_equ ts in |
||

495 | Some (PRIMITIVE (s1, f1)) |
||

496 | | _ -> None |
||

497 | end |
||

498 | | _ -> None |
||

499 | in |
||

500 | let (accF1, accD1) as acc1 = |
||

501 | match defopt with |
||

502 | | None -> |
||

503 | let f1 = parse_equ ts in |
||

504 | (f1::accF, accD) |
||

505 | | Some def -> (accF, def::accD) |
||

506 | in |
||

507 | match Stream.peek ts with |
||

508 | | Some (A.Kwd ";") -> |
||

509 | Stream.junk ts; |
||

510 | parse_formulaeDefList wDef ts acc1 |
||

511 | | _ -> (List.rev accF1, List.rev accD1) |
||

512 | |||

513 | (** Parses a string to obtain a formula query. |
||

514 | @param s A string representing a formula query. |
||

515 | @return A triple (fl, tboxND, tboxD) where |
||

516 | fl is a list of formula representing the initial input; |
||

517 | tboxND is a list of formulae representing |
||

518 | the non-definitional part of a TBox; and |
||

519 | tboxD is a list of definitions |
||

520 | representing the definitional part of a TBox. |
||

521 | @raise ALCException if s does not represent a formula query. |
||

522 | *) |
||

523 | let importQuery s = |
||

524 | let ts = lexer s in |
||

525 | try |
||

526 | begin |
||

527 | let res = |
||

528 | match Stream.peek ts with |
||

529 | | Some (A.Kwd "|-") -> |
||

530 | Stream.junk ts; |
||

531 | let (fl1, _) = parse_formulaeDefList false ts ([], []) in |
||

532 | (fl1, [], []) |
||

533 | | _ -> |
||

534 | begin |
||

535 | let (fl1, dl1) = parse_formulaeDefList true ts ([], []) in |
||

536 | match Stream.peek ts with |
||

537 | | Some (A.Kwd "|-") -> |
||

538 | Stream.junk ts; |
||

539 | let (fl2, _) = parse_formulaeDefList false ts ([], []) in |
||

540 | (fl2, fl1, dl1) |
||

541 | | _ -> |
||

542 | if dl1 = [] then (fl1, [], []) |
||

543 | else A.printError mk_exn ~ts "\"|-\" expected: " |
||

544 | end |
||

545 | in |
||

546 | let _ = |
||

547 | match Stream.peek ts with |
||

548 | | None -> () |
||

549 | | Some _ -> A.printError mk_exn ~ts "EOS expected: " |
||

550 | in |
||

551 | res |
||

552 | end |
||

553 | with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS" |
||

554 | |||

555 | |||

556 | (** Substitutes some propositional variables in a formula. |
||

557 | @param subl A list of pairs (s, fp) |
||

558 | where s is the name of a propositional variable and fp is a formula. |
||

559 | @param f A formula. |
||

560 | @return A formula f' where each propositional variable p |
||

561 | such that (p, fp) is contained in subl is replaced by fp. |
||

562 | *) |
||

563 | let rec substFormula subl f = |
||

564 | match f with |
||

565 | | TRUE |
||

566 | | FALSE -> f |
||

567 | | AP s -> if List.mem_assoc s subl then List.assoc s subl else f |
||

568 | | NOT f1 -> |
||

569 | let ft = substFormula subl f1 in |
||

570 | if ft == f1 then f else NOT ft |
||

571 | | EX (s, i, f1) -> |
||

572 | let ft = substFormula subl f1 in |
||

573 | if ft == f1 then f else EX (s, i, ft) |
||

574 | | AX (s, i, f1) -> |
||

575 | let ft = substFormula subl f1 in |
||

576 | if ft == f1 then f else AX (s, i, ft) |
||

577 | | MIN (n, s, i, f1) -> |
||

578 | let ft = substFormula subl f1 in |
||

579 | if ft == f1 then f else MIN (n, s, i, ft) |
||

580 | | MAX (n, s, i, f1) -> |
||

581 | let ft = substFormula subl f1 in |
||

582 | if ft == f1 then f else MAX (n, s, i, ft) |
||

583 | | EQU (f1, f2) -> |
||

584 | let ft1 = substFormula subl f1 in |
||

585 | let ft2 = substFormula subl f2 in |
||

586 | if (f1 == ft1) && (f2 == ft2) then f |
||

587 | else EQU (ft1, ft2) |
||

588 | | IMP (f1, f2) -> |
||

589 | let ft1 = substFormula subl f1 in |
||

590 | let ft2 = substFormula subl f2 in |
||

591 | if (f1 == ft1) && (f2 == ft2) then f |
||

592 | else IMP (ft1, ft2) |
||

593 | | OR (f1, f2) -> |
||

594 | let ft1 = substFormula subl f1 in |
||

595 | let ft2 = substFormula subl f2 in |
||

596 | if (f1 == ft1) && (f2 == ft2) then f |
||

597 | else OR (ft1, ft2) |
||

598 | | AND (f1, f2) -> |
||

599 | let ft1 = substFormula subl f1 in |
||

600 | let ft2 = substFormula subl f2 in |
||

601 | if (f1 == ft1) && (f2 == ft2) then f |
||

602 | else AND (ft1, ft2) |
||

603 | |||

604 | |||

605 | (** Converts the negation of a formula to negation normal form |
||

606 | by "pushing in" the negations "~". |
||

607 | The symbols "<=>" and "=>" are substituted by their usual definitions. |
||

608 | @param f A formula. |
||

609 | @return A formula in negation normal form and not containing "<=>" or "=>" |
||

610 | that is equivalent to ~f. |
||

611 | *) |
||

612 | let rec nnfNeg f = |
||

613 | match f with |
||

614 | | TRUE -> FALSE |
||

615 | | FALSE -> TRUE |
||

616 | | AP _ -> NOT f |
||

617 | | NOT f1 -> nnf f1 |
||

618 | | EX (s, i, f1) -> AX (s, i, nnfNeg f1) |
||

619 | | AX (s, i, f1) -> EX (s, i, nnfNeg f1) |
||

620 | | MIN (n, s, i, f1) -> |
||

621 | if n = 0 then FALSE else MAX (n-1, s, i, nnf f1) |
||

622 | | MAX (n, s, i, f1) -> MIN (n+1, s, i, nnf f1) |
||

623 | | EQU (f1, f2) -> OR (AND (nnf f1, nnfNeg f2), AND (nnf f2, nnfNeg f1)) |
||

624 | | IMP (f1, f2) -> AND (nnf f1, nnfNeg f2) |
||

625 | | OR (f1, f2) -> AND (nnfNeg f1, nnfNeg f2) |
||

626 | | AND (f1, f2) -> OR (nnfNeg f1, nnfNeg f2) |
||

627 | |||

628 | (** Converts a formula to negation normal form |
||

629 | by "pushing in" the negations "~". |
||

630 | The symbols "<=>" and "=>" are substituted by their usual definitions. |
||

631 | @param f A formula. |
||

632 | @return A formula in negation normal form and not containing "<=>" or "=>" |
||

633 | that is equivalent to f. |
||

634 | *) |
||

635 | and nnf f = |
||

636 | match f with |
||

637 | | TRUE |
||

638 | | FALSE |
||

639 | | AP _ |
||

640 | | NOT (AP _) -> f |
||

641 | | NOT f1 -> nnfNeg f1 |
||

642 | | EX (s, i, f1) -> |
||

643 | let ft = nnf f1 in |
||

644 | if ft == f1 then f else EX (s, i, ft) |
||

645 | | AX (s, i, f1) -> |
||

646 | let ft = nnf f1 in |
||

647 | if ft == f1 then f else AX (s, i, ft) |
||

648 | | MIN (n, s, i, f1) -> |
||

649 | let ft = nnf f1 in |
||

650 | if ft == f1 then f else MIN (n, s, i, ft) |
||

651 | | MAX (n, s, i, f1) -> |
||

652 | let ft = nnf f1 in |
||

653 | if ft == f1 then f else MAX (n, s, i, ft) |
||

654 | | EQU (f1, f2) -> AND (OR (nnfNeg f1, nnf f2), OR (nnfNeg f2, nnf f1)) |
||

655 | | IMP (f1, f2) -> OR (nnfNeg f1, nnf f2) |
||

656 | | OR (f1, f2) -> |
||

657 | let ft1 = nnf f1 in |
||

658 | let ft2 = nnf f2 in |
||

659 | if ft1 == f1 && ft2 == f2 then f else OR (ft1, ft2) |
||

660 | | AND (f1, f2) -> |
||

661 | let ft1 = nnf f1 in |
||

662 | let ft2 = nnf f2 in |
||

663 | if ft1 == f1 && ft2 == f2 then f else AND (ft1, ft2) |
||

664 | |||

665 | |||

666 | (** Checks whether a formula contains inverse roles. |
||

667 | @param f A formula. |
||

668 | @return True iff f contains some inverse roles. |
||

669 | *) |
||

670 | let rec containsInverse f = |
||

671 | match f with |
||

672 | | TRUE |
||

673 | | FALSE |
||

674 | | AP _ -> false |
||

675 | | NOT f1 -> containsInverse f1 |
||

676 | | EX (_, i, f1) |
||

677 | | AX (_, i, f1) |
||

678 | | MIN (_, _, i, f1) |
||

679 | | MAX (_, _, i, f1) -> i || containsInverse f1 |
||

680 | | EQU (f1, f2) |
||

681 | | IMP (f1, f2) |
||

682 | | OR (f1, f2) |
||

683 | | AND (f1, f2) -> containsInverse f1 || containsInverse f2 |
||

684 | |||

685 | |||

686 | (** Simplifies a formula that is in negation normal form. |
||

687 | @param f A formula in negation normal form. |
||

688 | @return A formula in negation normal form that is equivalent to f. |
||

689 | @raise ALCException if f is not in negation normal form. |
||

690 | *) |
||

691 | let rec simplifyFormula f = |
||

692 | match f with |
||

693 | | TRUE |
||

694 | | FALSE |
||

695 | | AP _ |
||

696 | | NOT (AP _) -> f |
||

697 | | EX (s, i, f1) -> |
||

698 | let ft = simplifyFormula f1 in |
||

699 | begin |
||

700 | match ft with |
||

701 | | FALSE -> FALSE |
||

702 | | _ -> if ft == f1 then f else EX (s, i, ft) |
||

703 | end |
||

704 | | AX (s, i, f1) -> |
||

705 | let ft = simplifyFormula f1 in |
||

706 | begin |
||

707 | match ft with |
||

708 | | TRUE -> TRUE |
||

709 | | _ -> if ft == f1 then f else AX (s, i, ft) |
||

710 | end |
||

711 | | MIN (n, s, i, f1) -> |
||

712 | if n = 0 then TRUE |
||

713 | else |
||

714 | let ft = simplifyFormula f1 in |
||

715 | begin |
||

716 | match ft with |
||

717 | | FALSE -> FALSE |
||

718 | | _ -> if ft == f1 then f else MIN (n, s, i, ft) |
||

719 | end |
||

720 | | MAX (n, s, i, f1) -> |
||

721 | let ft = simplifyFormula f1 in |
||

722 | begin |
||

723 | match ft with |
||

724 | | FALSE -> TRUE |
||

725 | | _ -> if ft == f1 then f else MAX (n, s, i, ft) |
||

726 | end |
||

727 | | OR (f1, f2) -> |
||

728 | let ft1 = simplifyFormula f1 in |
||

729 | let ft2 = simplifyFormula f2 in |
||

730 | begin |
||

731 | match ft1, ft2 with |
||

732 | | TRUE, _ -> TRUE |
||

733 | | FALSE, _ -> ft2 |
||

734 | | _, TRUE -> TRUE |
||

735 | | _, FALSE -> ft1 |
||

736 | | _, _ -> |
||

737 | if (f1 == ft1) && (f2 == ft2) then f |
||

738 | else OR (ft1, ft2) |
||

739 | end |
||

740 | | AND (f1, f2) -> |
||

741 | let ft1 = simplifyFormula f1 in |
||

742 | let ft2 = simplifyFormula f2 in |
||

743 | begin |
||

744 | match ft1, ft2 with |
||

745 | | TRUE, _ -> ft2 |
||

746 | | FALSE, _ -> FALSE |
||

747 | | _, TRUE -> ft1 |
||

748 | | _, FALSE -> FALSE |
||

749 | | _, _ -> |
||

750 | if (f1 == ft1) && (f2 == ft2) then f |
||

751 | else AND (ft1, ft2) |
||

752 | end |
||

753 | | _ -> raise (ALCException "Formula is not in negation normal form.") |
||

754 | |||

755 | |||

756 | (** Destructs an atomic proposition. |
||

757 | @param f An atomic proposition. |
||

758 | @return The name of the atomic proposition. |
||

759 | @raise ALCException if f is not an atomic proposition. |
||

760 | *) |
||

761 | let dest_ap f = |
||

762 | match f with |
||

763 | | AP s -> s |
||

764 | | _ -> raise (ALCException "Formula is not an atomic proposition.") |
||

765 | |||

766 | (** Destructs a negation. |
||

767 | @param f A negation. |
||

768 | @return The immediate subformula of the negation. |
||

769 | @raise ALCException if f is not a negation. |
||

770 | *) |
||

771 | let dest_not f = |
||

772 | match f with |
||

773 | | NOT f1 -> f1 |
||

774 | | _ -> raise (ALCException "Formula is not a negation.") |
||

775 | |||

776 | (** Destructs an EX-formula. |
||

777 | @param f An EX-formula. |
||

778 | @return The role name, whether it is an inverse role, |
||

779 | and the immediate subformula of the EX-formula. |
||

780 | @raise ALCException if f is not an EX-formula. |
||

781 | *) |
||

782 | let dest_ex f = |
||

783 | match f with |
||

784 | | EX (s, i, f1) -> (s, i, f1) |
||

785 | | _ -> raise (ALCException "Formula is not an EX-formula.") |
||

786 | |||

787 | (** Destructs an AX-formula. |
||

788 | @param f An AX-formula. |
||

789 | @return The role name, whether it is an inverse role, |
||

790 | and the immediate subformula of the AX-formula. |
||

791 | @raise ALCException if f is not an AX-formula. |
||

792 | *) |
||

793 | let dest_ax f = |
||

794 | match f with |
||

795 | | AX (s, i, f1) -> (s, i, f1) |
||

796 | | _ -> raise (ALCException "Formula is not an AX-formula.") |
||

797 | |||

798 | (** Destructs a MIN-formula. |
||

799 | @param f A MIN-formula. |
||

800 | @return The number restriction, role name, whether it is an inverse role, |
||

801 | and the immediate subformula of the MIN-formula. |
||

802 | @raise ALCException if f is not a MIN-formula. |
||

803 | *) |
||

804 | let dest_min f = |
||

805 | match f with |
||

806 | | MIN (n, s, i, f1) -> (n, s, i, f1) |
||

807 | | _ -> raise (ALCException "Formula is not a MIN-formula.") |
||

808 | |||

809 | (** Destructs a MAX-formula. |
||

810 | @param f A MAX-formula. |
||

811 | @return The number restriction, role name, whether it is an inverse role, |
||

812 | and the immediate subformula of the MAX-formula. |
||

813 | @raise ALCException if f is not a MAX-formula. |
||

814 | *) |
||

815 | let dest_max f = |
||

816 | match f with |
||

817 | | MAX (n, s, i, f1) -> (n, s, i, f1) |
||

818 | | _ -> raise (ALCException "Formula is not a MAX-formula.") |
||

819 | |||

820 | (** Destructs an equivalence. |
||

821 | @param f An equivalence. |
||

822 | @return The two immediate subformulae of the equivalence. |
||

823 | @raise ALCException if f is not an equivalence. |
||

824 | *) |
||

825 | let dest_equ f = |
||

826 | match f with |
||

827 | | EQU (f1, f2) -> (f1, f2) |
||

828 | | _ -> raise (ALCException "Formula is not an equivalence.") |
||

829 | |||

830 | (** Destructs an implication. |
||

831 | @param f An implication. |
||

832 | @return The two immediate subformulae of the implication. |
||

833 | @raise ALCException if f is not an implication. |
||

834 | *) |
||

835 | let dest_imp f = |
||

836 | match f with |
||

837 | | IMP (f1, f2) -> (f1, f2) |
||

838 | | _ -> raise (ALCException "Formula is not an implication.") |
||

839 | |||

840 | (** Destructs an or-formula. |
||

841 | @param f An or-formula. |
||

842 | @return The two immediate subformulae of the or-formula. |
||

843 | @raise ALCException if f is not an or-formula. |
||

844 | *) |
||

845 | let dest_or f = |
||

846 | match f with |
||

847 | | OR (f1, f2) -> (f1, f2) |
||

848 | | _ -> raise (ALCException "Formula is not an or-formula.") |
||

849 | |||

850 | (** Destructs an and-formula. |
||

851 | @param f An and-formula. |
||

852 | @return The two immediate subformulae of the and-formula. |
||

853 | @raise ALCException if f is not an and-formula. |
||

854 | *) |
||

855 | let dest_and f = |
||

856 | match f with |
||

857 | | AND (f1, f2) -> (f1, f2) |
||

858 | | _ -> raise (ALCException "Formula is not an and-formula.") |
||

859 | |||

860 | |||

861 | (** Tests whether a formula is the constant True. |
||

862 | @param f A formula. |
||

863 | @return True iff f is the constant True. |
||

864 | *) |
||

865 | let is_true f = |
||

866 | match f with |
||

867 | | TRUE -> true |
||

868 | | _ -> false |
||

869 | |||

870 | (** Tests whether a formula is the constant False. |
||

871 | @param f A formula. |
||

872 | @return True iff f is the constant False. |
||

873 | *) |
||

874 | let is_false f = |
||

875 | match f with |
||

876 | | FALSE -> true |
||

877 | | _ -> false |
||

878 | |||

879 | (** Tests whether a formula is an atomic proposition. |
||

880 | @param f A formula. |
||

881 | @return True iff f is an atomic proposition. |
||

882 | *) |
||

883 | let is_ap f = |
||

884 | match f with |
||

885 | | AP _ -> true |
||

886 | | _ -> false |
||

887 | |||

888 | (** Tests whether a formula is a negation. |
||

889 | @param f A formula. |
||

890 | @return True iff f is a negation. |
||

891 | *) |
||

892 | let is_not f = |
||

893 | match f with |
||

894 | | NOT _ -> true |
||

895 | | _ -> false |
||

896 | |||

897 | (** Tests whether a formula is an EX-formula. |
||

898 | @param f A formula. |
||

899 | @return True iff f is an EX-formula. |
||

900 | *) |
||

901 | let is_ex f = |
||

902 | match f with |
||

903 | | EX _ -> true |
||

904 | | _ -> false |
||

905 | |||

906 | (** Tests whether a formula is an AX-formula. |
||

907 | @param f A formula. |
||

908 | @return True iff f is an AX-formula. |
||

909 | *) |
||

910 | let is_ax f = |
||

911 | match f with |
||

912 | | AX _ -> true |
||

913 | | _ -> false |
||

914 | |||

915 | (** Tests whether a formula is a MIN-formula. |
||

916 | @param f A formula. |
||

917 | @return True iff f is a MIN-formula. |
||

918 | *) |
||

919 | let is_min f = |
||

920 | match f with |
||

921 | | MIN _ -> true |
||

922 | | _ -> false |
||

923 | |||

924 | (** Tests whether a formula is a MAX-formula. |
||

925 | @param f A formula. |
||

926 | @return True iff f is a MAX-formula. |
||

927 | *) |
||

928 | let is_max f = |
||

929 | match f with |
||

930 | | MAX _ -> true |
||

931 | | _ -> false |
||

932 | |||

933 | (** Tests whether a formula is an equivalence. |
||

934 | @param f A formula. |
||

935 | @return True iff f is an equivalence. |
||

936 | *) |
||

937 | let is_equ f = |
||

938 | match f with |
||

939 | | EQU _ -> true |
||

940 | | _ -> false |
||

941 | |||

942 | (** Tests whether a formula is an implication. |
||

943 | @param f A formula. |
||

944 | @return True iff f is an implication. |
||

945 | *) |
||

946 | let is_imp f = |
||

947 | match f with |
||

948 | | IMP _ -> true |
||

949 | | _ -> false |
||

950 | |||

951 | (** Tests whether a formula is an or-formula. |
||

952 | @param f A formula. |
||

953 | @return True iff f is an or-formula. |
||

954 | *) |
||

955 | let is_or f = |
||

956 | match f with |
||

957 | | OR _ -> true |
||

958 | | _ -> false |
||

959 | |||

960 | (** Tests whether a formula is an and-formula. |
||

961 | @param f A formula. |
||

962 | @return True iff f is an and-formula. |
||

963 | *) |
||

964 | let is_and f = |
||

965 | match f with |
||

966 | | AND _ -> true |
||

967 | | _ -> false |
||

968 | |||

969 | |||

970 | (** The constant True. |
||

971 | *) |
||

972 | let const_true = TRUE |
||

973 | |||

974 | (** The constant False. |
||

975 | *) |
||

976 | let const_false = FALSE |
||

977 | |||

978 | (** Constructs an atomic proposition. |
||

979 | @param s The name of the atomic proposition. |
||

980 | @return The atomic proposition with name s. |
||

981 | *) |
||

982 | let const_ap s = AP s |
||

983 | |||

984 | (** Negates a formula. |
||

985 | @param f A formula. |
||

986 | @return The negation of f. |
||

987 | *) |
||

988 | let const_not f = NOT f |
||

989 | |||

990 | (** Constructs an EX-formula from a formula. |
||

991 | @param s A role name. |
||

992 | @param i True if it is an inverse role, false otherwise. |
||

993 | @param f A formula. |
||

994 | @return The formula EX f. |
||

995 | *) |
||

996 | let const_ex s i f = EX (s, i, f) |
||

997 | |||

998 | (** Constructs an AX-formula from a formula. |
||

999 | @param s A role name. |
||

1000 | @param i True if it is an inverse role, false otherwise. |
||

1001 | @param f A formula. |
||

1002 | @return The formula AX f. |
||

1003 | *) |
||

1004 | let const_ax s i f = AX (s, i, f) |
||

1005 | |||

1006 | (** Constructs a MIN-formula from a formula. |
||

1007 | @param n A non-negative integer. |
||

1008 | @param s A role name. |
||

1009 | @param i True if it is an inverse role, false otherwise. |
||

1010 | @param f A formula. |
||

1011 | @return The formula MIN f. |
||

1012 | @raise ALCException Iff n is negative. |
||

1013 | *) |
||

1014 | let const_min n s i f = |
||

1015 | if n < 0 then raise (ALCException "Negative cardinality constraint.") |
||

1016 | else MIN (n, s, i, f) |
||

1017 | |||

1018 | (** Constructs a MAX-formula from a formula. |
||

1019 | @param n A non-negative integer. |
||

1020 | @param s A role name. |
||

1021 | @param i True if it is an inverse role, false otherwise. |
||

1022 | @param f A formula. |
||

1023 | @return The formula MAX f. |
||

1024 | @raise ALCException Iff n is negative. |
||

1025 | *) |
||

1026 | let const_max n s i f = |
||

1027 | if n < 0 then raise (ALCException "Negative cardinality constraint.") |
||

1028 | else MAX (n, s, i, f) |
||

1029 | |||

1030 | (** Constructs an equivalence from two formulae. |
||

1031 | @param f1 The first formula (LHS). |
||

1032 | @param f2 The second formula (LHS). |
||

1033 | @return The equivalence f1 <=> f2. |
||

1034 | *) |
||

1035 | let const_equ f1 f2 = EQU (f1, f2) |
||

1036 | |||

1037 | (** Constructs an implication from two formulae. |
||

1038 | @param f1 The first formula (LHS). |
||

1039 | @param f2 The second formula (LHS). |
||

1040 | @return The implication f1 => f2. |
||

1041 | *) |
||

1042 | let const_imp f1 f2 = IMP (f1, f2) |
||

1043 | |||

1044 | (** Constructs an or-formula from two formulae. |
||

1045 | @param f1 The first formula (LHS). |
||

1046 | @param f2 The second formula (LHS). |
||

1047 | @return The formula f1 | f2. |
||

1048 | *) |
||

1049 | let const_or f1 f2 = OR (f1, f2) |
||

1050 | |||

1051 | (** Constructs an and-formula from two formulae. |
||

1052 | @param f1 The first formula (LHS). |
||

1053 | @param f2 The second formula (LHS). |
||

1054 | @return The formula f1 & f2. |
||

1055 | *) |
||

1056 | let const_and f1 f2 = AND (f1, f2) |
||

1057 | |||

1058 | |||

1059 | (** Calculates all formulae |
||

1060 | that may be created in the tableau procedure (i.e. a kind of Fischer-Ladner closure). |
||

1061 | @param compF A function that compares formulae. |
||

1062 | @param f The initial formula of the tableau procedure |
||

1063 | which must be in negation normal form. |
||

1064 | @return A list containing all formulae of the closure in increasing order. |
||

1065 | @raise ALCException if f is not in negation normal form. |
||

1066 | *) |
||

1067 | let detClosure compF f = |
||

1068 | let module TSet = Set.Make( |
||

1069 | struct |
||

1070 | type t = formula |
||

1071 | let (compare : t -> t -> int) = compF |
||

1072 | end |
||

1073 | ) |
||

1074 | in |
||

1075 | let rec detC fs f = |
||

1076 | if TSet.mem f fs then fs |
||

1077 | else |
||

1078 | let nfs = TSet.add f fs in |
||

1079 | match f with |
||

1080 | | TRUE |
||

1081 | | FALSE -> nfs |
||

1082 | | AP _ -> TSet.add (NOT f) nfs |
||

1083 | | NOT (AP s) -> TSet.add (AP s) nfs |
||

1084 | | EX (_, _, f1) |
||

1085 | | AX (_, _, f1) -> detC nfs f1 |
||

1086 | | OR (f1, f2) |
||

1087 | | AND (f1, f2) -> |
||

1088 | let nfs = detC nfs f1 in |
||

1089 | detC nfs f2 |
||

1090 | | _ -> raise (ALCException "Formula is not in negation normal form.") |
||

1091 | in |
||

1092 | let tset = TSet.empty in |
||

1093 | let tset = TSet.add TRUE tset in |
||

1094 | let tset = TSet.add FALSE tset in |
||

1095 | let rset = detC tset f in |
||

1096 | TSet.elements rset |
||

1097 | |||

1098 | |||

1099 | (** Hash-consed formulae, which are in negation normal form, |
||

1100 | such that structural and physical equality coincide. |
||

1101 | *) |
||

1102 | type hcFormula = (hcFormula_node, formula) HC.hash_consed |
||

1103 | and hcFormula_node = |
||

1104 | | HCTRUE |
||

1105 | | HCFALSE |
||

1106 | | HCAP of string |
||

1107 | | HCNOT of string |
||

1108 | | HCEX of string * bool * hcFormula |
||

1109 | | HCAX of string * bool * hcFormula |
||

1110 | | HCOR of hcFormula * hcFormula |
||

1111 | | HCAND of hcFormula * hcFormula |
||

1112 | |||

1113 | (** Determines whether two formula nodes are structurally equal. |
||

1114 | @param f1 The first formula node. |
||

1115 | @param f2 The second formula node. |
||

1116 | @return True iff f1 and f2 are structurally equal. |
||

1117 | *) |
||

1118 | let equal_hcFormula_node f1 f2 = |
||

1119 | match f1, f2 with |
||

1120 | | HCTRUE, HCTRUE -> true |
||

1121 | | HCFALSE, HCFALSE -> true |
||

1122 | | HCAP s1, HCAP s2 |
||

1123 | | HCNOT s1, HCNOT s2 -> compare s1 s2 = 0 |
||

1124 | | HCEX (s1, i1, f1), HCEX (s2, i2, f2) |
||

1125 | | HCAX (s1, i1, f1), HCAX (s2, i2, f2) -> compare s1 s2 = 0 && i1 = i2 && f1 == f2 |
||

1126 | | HCOR (f1a, f1b), HCOR (f2a, f2b) |
||

1127 | | HCAND (f1a, f1b), HCAND (f2a, f2b) -> f1a == f2a && f1b == f2b |
||

1128 | | _ -> false |
||

1129 | |||

1130 | (** Computes the hash value of a formula node. |
||

1131 | @param f A formula node. |
||

1132 | @return The hash value of f. |
||

1133 | *) |
||

1134 | let hash_hcFormula_node f = |
||

1135 | match f with |
||

1136 | | HCTRUE -> 0 |
||

1137 | | HCFALSE -> 1 |
||

1138 | | HCAP s -> Hashtbl.hash s |
||

1139 | | HCNOT s -> Hashtbl.hash s + 1 |
||

1140 | | HCEX (s, i, f1) -> 19 * (19 * (Hashtbl.hash s) + (if i then 1 else 0) + f1.HC.hkey) + 3 |
||

1141 | | HCAX (s, i, f1) -> 19 * (19 * (Hashtbl.hash s) + (if i then 1 else 0) + f1.HC.hkey) + 4 |
||

1142 | | HCOR (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 5 |
||

1143 | | HCAND (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 6 |
||

1144 | |||

1145 | (** Determines the "real" formula of a formula node. |
||

1146 | @param f A formula node. |
||

1147 | @return The formula (in negation normal form) which corresponds to f. |
||

1148 | *) |
||

1149 | let toFml_hcFormula_node f = |
||

1150 | match f with |
||

1151 | | HCTRUE -> TRUE |
||

1152 | | HCFALSE -> FALSE |
||

1153 | | HCAP s -> AP s |
||

1154 | | HCNOT s -> NOT (AP s) |
||

1155 | | HCEX (s, i, f1) -> EX (s, i, f1.HC.fml) |
||

1156 | | HCAX (s, i, f1) -> AX (s, i, f1.HC.fml) |
||

1157 | | HCOR (f1, f2) -> |
||

1158 | let fml1 = f1.HC.fml in |
||

1159 | let fml2 = f2.HC.fml in |
||

1160 | OR (fml1, fml2) |
||

1161 | | HCAND (f1, f2) -> |
||

1162 | let fml1 = f1.HC.fml in |
||

1163 | let fml2 = f2.HC.fml in |
||

1164 | AND (fml1, fml2) |
||

1165 | |||

1166 | (** Determines the negation (in negation normal form) of a formula node. |
||

1167 | @param f A formula node. |
||

1168 | @return The negation (in negation normal form) of f. |
||

1169 | *) |
||

1170 | let negNde_hcFormula_node f = |
||

1171 | match f with |
||

1172 | | HCTRUE -> HCFALSE |
||

1173 | | HCFALSE -> HCTRUE |
||

1174 | | HCAP s -> HCNOT s |
||

1175 | | HCNOT s -> HCAP s |
||

1176 | | HCEX (s, i, f2) -> HCAX (s, i, f2.HC.neg) |
||

1177 | | HCAX (s, i, f2) -> HCEX (s, i, f2.HC.neg) |
||

1178 | | HCOR (f1, f2) -> |
||

1179 | let notf1 = f1.HC.neg in |
||

1180 | let notf2 = f2.HC.neg in |
||

1181 | HCAND (notf1, notf2) |
||

1182 | | HCAND (f1, f2) -> |
||

1183 | let notf1 = f1.HC.neg in |
||

1184 | let notf2 = f2.HC.neg in |
||

1185 | HCOR (notf1, notf2) |
||

1186 | |||

1187 | (** An instantiation of hash-consing for formulae. |
||

1188 | *) |
||

1189 | module HcFormula = HC.Make( |
||

1190 | struct |
||

1191 | type nde = hcFormula_node |
||

1192 | type fml = formula |
||

1193 | let equal (n1 : nde) n2 = equal_hcFormula_node n1 n2 |
||

1194 | let hash (n : nde) = hash_hcFormula_node n |
||

1195 | let negNde (n : nde) = negNde_hcFormula_node n |
||

1196 | let toFml (n : nde) = toFml_hcFormula_node n |
||

1197 | end |
||

1198 | ) |
||

1199 | |||

1200 | |||

1201 | (** An instantiation of a hash table (of the standard library) |
||

1202 | for hash-consed formulae. The test for equality |
||

1203 | and computing the hash value is done in constant time. |
||

1204 | *) |
||

1205 | module HcFHt = Hashtbl.Make( |
||

1206 | struct |
||

1207 | type t = hcFormula |
||

1208 | let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag |
||

1209 | let hash (f : t) = f.HC.tag |
||

1210 | end |
||

1211 | ) |
||

1212 | |||

1213 | |||

1214 | (** Converts a formula into its hash-consed version. |
||

1215 | @param hcF A hash-cons table for formulae. |
||

1216 | @param f A formula in negation normal form. |
||

1217 | @return The hash-consed version of f. |
||

1218 | @raise ALCException if f is not in negation normal form. |
||

1219 | *) |
||

1220 | let rec hc_formula hcF f = |
||

1221 | match f with |
||

1222 | | TRUE -> HcFormula.hashcons hcF HCTRUE |
||

1223 | | FALSE -> HcFormula.hashcons hcF HCFALSE |
||

1224 | | AP s -> HcFormula.hashcons hcF (HCAP s) |
||

1225 | | NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s) |
||

1226 | | EX (s, i, f1) -> |
||

1227 | let tf1 = hc_formula hcF f1 in |
||

1228 | HcFormula.hashcons hcF (HCEX (s, i, tf1)) |
||

1229 | | AX (s, i, f1) -> |
||

1230 | let tf1 = hc_formula hcF f1 in |
||

1231 | HcFormula.hashcons hcF (HCAX (s, i, tf1)) |
||

1232 | | OR (f1, f2) -> |
||

1233 | let tf1 = hc_formula hcF f1 in |
||

1234 | let tf2 = hc_formula hcF f2 in |
||

1235 | HcFormula.hashcons hcF (HCOR (tf1, tf2)) |
||

1236 | | AND (f1, f2) -> |
||

1237 | let tf1 = hc_formula hcF f1 in |
||

1238 | let tf2 = hc_formula hcF f2 in |
||

1239 | HcFormula.hashcons hcF (HCAND (tf1, tf2)) |
||

1240 | | _ -> raise (ALCException "Formula is not in negation normal form.") |
||

1241 | |||

1242 | |||

1243 | (** Calculates all formulae |
||

1244 | which may be created in the tableau procedure (i.e. a kind of Fischer-Ladner closure). |
||

1245 | @param hcF A hash-cons table for formulae. |
||

1246 | @param hcnnf The initial formula of the tableau procedure as hash-consed version. |
||

1247 | (which is in negation normal form). |
||

1248 | @return A list containing all hash-consed formulae of the closure (in arbitrary order). |
||

1249 | @raise ALCException if nnf is not in negation normal form. |
||

1250 | *) |
||

1251 | let detClosureHc hcF hcnnf = |
||

1252 | let hcFht = HcFHt.create 100 in |
||

1253 | HcFHt.add hcFht (HcFormula.hashcons hcF HCTRUE) (); |
||

1254 | HcFHt.add hcFht (HcFormula.hashcons hcF HCFALSE) (); |
||

1255 | let rec detC f = |
||

1256 | if HcFHt.mem hcFht f then () |
||

1257 | else begin |
||

1258 | HcFHt.add hcFht f (); |
||

1259 | match f.HC.node with |
||

1260 | | HCTRUE |
||

1261 | | HCFALSE |
||

1262 | | HCAP _ |
||

1263 | | HCNOT _ -> () |
||

1264 | | HCOR (f1, f2) |
||

1265 | | HCAND (f1, f2) -> |
||

1266 | detC f1; |
||

1267 | detC f2 |
||

1268 | | HCEX (_, _, f1) |
||

1269 | | HCAX (_, _, f1) -> detC f1 |
||

1270 | end |
||

1271 | in |
||

1272 | detC hcnnf; |
||

1273 | let flist = HcFHt.fold (fun f () acc -> f::acc) hcFht [] in |
||

1274 | flist |
||

1275 | |||

1276 | |||

1277 | (** Converts a formula into a string representation for alc-tableau. |
||

1278 | @param f A formula with no inverse roles. |
||

1279 | @return A string representing f for alc-tableau. |
||

1280 | @raise ALCException If f contains number restrictions or inverse roles, or |
||

1281 | if the name of an atomic program |
||

1282 | or a propositional variable in f is "tt" or "ff". |
||

1283 | *) |
||

1284 | let exportFormulaAlcTableau f = |
||

1285 | let size = sizeFormula f in |
||

1286 | let sb = Buffer.create (2 * size) in |
||

1287 | let rec expF = function |
||

1288 | | TRUE -> Buffer.add_string sb "tt" |
||

1289 | | FALSE -> Buffer.add_string sb "ff" |
||

1290 | | AP s -> |
||

1291 | if s <> "tt" && s <> "ff" then Buffer.add_string sb s |
||

1292 | else raise (ALCException "Formula contains \"tt\" or \"ff\".") |
||

1293 | | NOT f1 -> |
||

1294 | Buffer.add_string sb "not("; |
||

1295 | expF f1; |
||

1296 | Buffer.add_string sb ")" |
||

1297 | | EX (s1, i1, f1) -> |
||

1298 | if i1 then raise (ALCException "Formula contains inverse roles.") |
||

1299 | else begin |
||

1300 | Buffer.add_string sb "some("; |
||

1301 | Buffer.add_string sb s1; |
||

1302 | Buffer.add_string sb ","; |
||

1303 | expF f1; |
||

1304 | Buffer.add_string sb ")" |
||

1305 | end |
||

1306 | | AX (s1, i1, f1) -> |
||

1307 | if i1 then raise (ALCException "Formula contains inverse roles.") |
||

1308 | else begin |
||

1309 | Buffer.add_string sb "all("; |
||

1310 | Buffer.add_string sb s1; |
||

1311 | Buffer.add_string sb ","; |
||

1312 | expF f1; |
||

1313 | Buffer.add_string sb ")" |
||

1314 | end |
||

1315 | | MIN _ |
||

1316 | | MAX _ -> raise (ALCException "Formula contains number restrictions.") |
||

1317 | | EQU (f1, f2) -> |
||

1318 | Buffer.add_string sb "equiv("; |
||

1319 | expF f1; |
||

1320 | Buffer.add_string sb ","; |
||

1321 | expF f2; |
||

1322 | Buffer.add_string sb ")" |
||

1323 | | IMP (f1, f2) -> |
||

1324 | Buffer.add_string sb "implies("; |
||

1325 | expF f1; |
||

1326 | Buffer.add_string sb ","; |
||

1327 | expF f2; |
||

1328 | Buffer.add_string sb ")" |
||

1329 | | OR (f1, f2) -> |
||

1330 | Buffer.add_string sb "disj("; |
||

1331 | expF f1; |
||

1332 | Buffer.add_string sb ","; |
||

1333 | expF f2; |
||

1334 | Buffer.add_string sb ")" |
||

1335 | | AND (f1, f2) -> |
||

1336 | Buffer.add_string sb "conj("; |
||

1337 | expF f1; |
||

1338 | Buffer.add_string sb ","; |
||

1339 | expF f2; |
||

1340 | Buffer.add_string sb ")" |
||

1341 | in |
||

1342 | expF f; |
||

1343 | Buffer.contents sb |
||

1344 | |||

1345 | |||

1346 | (** Creates a file representing a TBox in FaCT++ format. |
||

1347 | The satisfiability query is the definition |
||

1348 | of the special concept name "SAT". |
||

1349 | @param The name of the output file. |
||

1350 | @param fl A list of formulae which are to be tested for joint satisfiability. |
||

1351 | @param tboxND A list of formulae representing |
||

1352 | the non-definitional part of a TBox. |
||

1353 | @param tboxD A list of definitions |
||

1354 | representing the definitional part of a TBox. |
||

1355 | The definitions must not be cyclic |
||

1356 | and each concept must not be defined more than once. |
||

1357 | *) |
||

1358 | let createFactTBox filename fl tboxND tboxD = |
||

1359 | assert (fl <> []); |
||

1360 | let file = open_out filename in |
||

1361 | let ps s = output_string file s in |
||

1362 | let rec printFormula = function |
||

1363 | | TRUE -> ps "*TOP*" |
||

1364 | | FALSE -> ps "*BOTTOM*" |
||

1365 | | AP s -> ps s |
||

1366 | | NOT f1 -> |
||

1367 | ps "(not "; |
||

1368 | printFormula f1; |
||

1369 | ps ")" |
||

1370 | | EX (s, i1, f1) -> |
||

1371 | ps ("(some " ^ (if i1 then "(inv r" ^ s ^ ") " else "r" ^ s ^ " ")); |
||

1372 | printFormula f1; |
||

1373 | ps ")" |
||

1374 | | AX (s, i1, f1) -> |
||

1375 | ps ("(all " ^ (if i1 then "(inv r" ^ s ^ ") " else "r" ^ s ^ " ")); |
||

1376 | printFormula f1; |
||

1377 | ps ")" |
||

1378 | | MIN (n, s, i1, f1) -> |
||

1379 | ps ("(min " ^ (string_of_int n) ^ (if i1 then " (inv r" ^ s ^ ") " else " r" ^ s ^ " ")); |
||

1380 | printFormula f1; |
||

1381 | ps ")" |
||

1382 | | MAX (n, s, i1, f1) -> |
||

1383 | ps ("(max " ^ (string_of_int n) ^ (if i1 then " (inv r" ^ s ^ ") " else " r" ^ s ^ " ")); |
||

1384 | printFormula f1; |
||

1385 | ps ")" |
||

1386 | | EQU (f1, f2) -> printFormula (AND (OR (NOT f1, f2), OR (NOT f2, f1))) |
||

1387 | | IMP (f1, f2) -> printFormula (OR (NOT f1, f2)) |
||

1388 | | OR (f1, f2) -> |
||

1389 | ps "(or "; |
||

1390 | printFormula f1; |
||

1391 | ps " "; |
||

1392 | printFormula f2; |
||

1393 | ps ")" |
||

1394 | | AND (f1, f2) -> |
||

1395 | ps "(and "; |
||

1396 | printFormula f1; |
||

1397 | ps " "; |
||

1398 | printFormula f2; |
||

1399 | ps ")" |
||

1400 | in |
||

1401 | let printTBoxD = function |
||

1402 | | PRIMITIVE (s, f) -> |
||

1403 | ps ("(implies_c " ^ s ^ " "); |
||

1404 | printFormula f; |
||

1405 | ps ")\n" |
||

1406 | | NECANDSUFF (s, f) -> |
||

1407 | ps ("(equal_c " ^ s ^ " "); |
||

1408 | printFormula f; |
||

1409 | ps ")\n" |
||

1410 | in |
||

1411 | let f = List.fold_left (fun res f -> AND (res, f)) (List.hd fl) (List.tl fl) in |
||

1412 | let printTBoxND f = |
||

1413 | ps "(implies_c *TOP* "; |
||

1414 | printFormula f; |
||

1415 | ps ")\n" |
||

1416 | in |
||

1417 | List.iter printTBoxD tboxD; |
||

1418 | List.iter printTBoxND tboxND; |
||

1419 | ps "(equal_c SAT "; |
||

1420 | printFormula f; |
||

1421 | ps ")\n"; |
||

1422 | close_out file |
||

1423 | |||

1424 | (** Determines all propositional variables and roles |
||

1425 | occurring in a list of formulae. |
||

1426 | @param fl A list of formulae. |
||

1427 | @return A list containing all propositional variables in fl |
||

1428 | and a list containing all roles occurring in fl. |
||

1429 | *) |
||

1430 | let detVars fl = |
||

1431 | let module PSet = Set.Make(String) in |
||

1432 | let rec detPR ((ps, rs) as pr) = function |
||

1433 | | TRUE |
||

1434 | | FALSE -> pr |
||

1435 | | AP s -> (PSet.add s ps, rs) |
||

1436 | | NOT f1 -> detPR pr f1 |
||

1437 | | EX (s, _, f1) |
||

1438 | | AX (s, _, f1) |
||

1439 | | MIN (_, s, _, f1) |
||

1440 | | MAX (_, s, _, f1) -> detPR (ps, PSet.add s rs) f1 |
||

1441 | | EQU (f1, f2) |
||

1442 | | IMP (f1, f2) |
||

1443 | | OR (f1, f2) |
||

1444 | | AND (f1, f2) -> |
||

1445 | let npr = detPR pr f1 in |
||

1446 | detPR npr f2 |
||

1447 | in |
||

1448 | let (pset, rset) = List.fold_left (fun acc f -> detPR acc f) (PSet.empty, PSet.empty) fl in |
||

1449 | (PSet.elements pset, PSet.elements rset) |
||

1450 | |||

1451 | (** Creates a file representing a formula for Will's prover. |
||

1452 | @param The name of the output file. |
||

1453 | @param f A formula which must not contain inverse roles and |
||

1454 | must not contain more than one role. |
||

1455 | @raise ALCException If f contains inverse roles or more than one role. |
||

1456 | *) |
||

1457 | let createWill filename f = |
||

1458 | if containsInverse f then raise (ALCException "Formula contains inverse roles.") else (); |
||

1459 | let (_, pl) = detVars [f] in |
||

1460 | if List.length pl > 1 then raise (ALCException "Formula contains more than one role.") else (); |
||

1461 | let file = open_out filename in |
||

1462 | let ps s = output_string file s in |
||

1463 | let isProperName s = |
||

1464 | let len = String.length s in |
||

1465 | let rec isNumber i = |
||

1466 | if i <= 0 then true |
||

1467 | else |
||

1468 | let c = Char.code s.[i] in |
||

1469 | c >= Char.code '0' && c <= Char.code '9' && isNumber (i-1) |
||

1470 | in |
||

1471 | len >= 2 && s.[0] = 'p' && isNumber (len-1) |
||

1472 | in |
||

1473 | let rec printFormula = function |
||

1474 | | TRUE -> printFormula (NOT FALSE) |
||

1475 | | FALSE -> |
||

1476 | (* prerr_endline "Will's prover does not support constants true/false natively"; *) |
||

1477 | printFormula (AND (AP "p0", NOT (AP "p0"))) |
||

1478 | | AP s -> |
||

1479 | if isProperName s then ps s |
||

1480 | else raise (ALCException "Propositional variables have to be of the form p0, p1, etc.") |
||

1481 | | NOT f1 -> |
||

1482 | ps "(~ "; |
||

1483 | printFormula f1; |
||

1484 | ps ")" |
||

1485 | | EX (_, _, f1) -> |
||

1486 | ps ("(<0> "); |
||

1487 | printFormula f1; |
||

1488 | ps ")" |
||

1489 | | AX (s, i1, f1) -> printFormula (NOT (EX (s, i1, NOT f1))) |
||

1490 | | MIN (n, _, _, f1) -> |
||

1491 | if n = 0 then printFormula TRUE |
||

1492 | else begin |
||

1493 | ps ("(<" ^ (string_of_int (n-1)) ^ "> "); |
||

1494 | printFormula f1; |
||

1495 | ps ")" |
||

1496 | end |
||

1497 | | MAX (n, s, i1, f1) -> printFormula (NOT (MIN (n+1, s, i1, f1))) |
||

1498 | | EQU (f1, f2) -> printFormula (AND (OR (NOT f1, f2), OR (NOT f2, f1))) |
||

1499 | | IMP (f1, f2) -> printFormula (OR (NOT f1, f2)) |
||

1500 | | OR (f1, f2) -> |
||

1501 | ps "("; |
||

1502 | printFormula f1; |
||

1503 | ps " v "; |
||

1504 | printFormula f2; |
||

1505 | ps ")" |
||

1506 | | AND (f1, f2) -> |
||

1507 | ps "("; |
||

1508 | printFormula f1; |
||

1509 | ps " & "; |
||

1510 | printFormula f2; |
||

1511 | ps ")" |
||

1512 | in |
||

1513 | ps "Logic: GML\n"; |
||

1514 | printFormula f; |
||

1515 | close_out file |
||

1516 | |||

1517 | (** Creates a file representing a TBox in OWL format. |
||

1518 | The satisfiability query is added as an anonymous assertion (ABox constraint). |
||

1519 | @param The name of the output file. |
||

1520 | @param fl A list of formulae which are to be tested for joint satisfiability. |
||

1521 | @param tboxND A list of formulae representing |
||

1522 | the non-definitional part of a TBox. |
||

1523 | @param tboxD A list of definitions |
||

1524 | representing the definitional part of a TBox. |
||

1525 | The definitions must not be cyclic |
||

1526 | and each concept must not be defined more than once. |
||

1527 | *) |
||

1528 | let createOWL filename fl tboxND tboxD = |
||

1529 | assert (fl <> []); |
||

1530 | let file = open_out filename in |
||

1531 | let addTBoxD acc = function |
||

1532 | | PRIMITIVE (s, f) |
||

1533 | | NECANDSUFF (s, f) -> (AP s)::(f::acc) |
||

1534 | in |
||

1535 | let f = List.fold_left (fun res f -> AND (res, f)) (List.hd fl) (List.tl fl) in |
||

1536 | let tfl = List.fold_left addTBoxD (f :: tboxND) tboxD in |
||

1537 | let (pl,rl) = detVars tfl in |
||

1538 | let ps n s = |
||

1539 | for i = 1 to n do |
||

1540 | output_string file " " |
||

1541 | done; |
||

1542 | output_string file s |
||

1543 | in |
||

1544 | let rec exall n c s i f popt = |
||

1545 | ps n "<owl:Restriction>\n"; |
||

1546 | ps (n+1) "<owl:onProperty>\n"; |
||

1547 | if i then begin |
||

1548 | ps (n+2) "<rdf:Description>\n"; |
||

1549 | ps (n+3) ("<owl:inverseOf rdf:resource=\"#r" ^ s ^ "\"/>\n"); |
||

1550 | ps (n+2) "</rdf:Description>\n" |
||

1551 | end |
||

1552 | else ps (n+2) ("<rdf:Description rdf:about=\"#r" ^ s ^ "\"/>\n"); |
||

1553 | ps (n+1) "</owl:onProperty>\n"; |
||

1554 | let _ = |
||

1555 | match popt with |
||

1556 | | None -> () |
||

1557 | | Some (c2, no) -> |
||

1558 | ps (n+1) ("<" ^ c2 ^ " rdf:datatype=\"&xsd;nonNegativeInteger\">\n"); |
||

1559 | ps (n+2) ((string_of_int no) ^ "\n"); |
||

1560 | ps (n+1) ("</" ^ c2 ^ ">\n") |
||

1561 | in |
||

1562 | ps (n+1) ("<" ^ c ^ ">\n"); |
||

1563 | printFormula (n+2) f; |
||

1564 | ps (n+1) ("</" ^ c ^ ">\n"); |
||

1565 | ps n "</owl:Restriction>\n"; |
||

1566 | and andor n c f1 f2 = |
||

1567 | ps n "<owl:Class>\n"; |
||

1568 | ps (n+1) ("<" ^ c ^ " rdf:parseType=\"Collection\">\n"); |
||

1569 | printFormula (n+2) f1; |
||

1570 | printFormula (n+2) f2; |
||

1571 | ps (n+1) ("</" ^ c ^ ">\n"); |
||

1572 | ps n "</owl:Class>\n"; |
||

1573 | and printFormula n f = |
||

1574 | match f with |
||

1575 | | TRUE -> ps n "<rdf:Description rdf:about=\"&owl;Thing\"/>\n"; |
||

1576 | | FALSE -> ps n "<rdf:Description rdf:about=\"&owl;Nothing\"/>\n"; |
||

1577 | | AP s -> ps n ("<rdf:Description rdf:about=\"#p" ^ s ^ "\"/>\n"); |
||

1578 | | NOT f1 -> |
||

1579 | ps n "<owl:Class>\n"; |
||

1580 | ps (n+1) "<owl:complementOf>\n"; |
||

1581 | printFormula (n+2) f1; |
||

1582 | ps (n+1) "</owl:complementOf>\n"; |
||

1583 | ps n "</owl:Class>\n"; |
||

1584 | | EQU (f1, f2) -> printFormula n (AND (OR (NOT f1, f2), OR (NOT f2, f1))) |
||

1585 | | IMP (f1, f2) -> printFormula n (OR (NOT f1, f2)) |
||

1586 | | EX (s, i1, f1) -> exall n "owl:someValuesFrom" s i1 f1 None |
||

1587 | | AX (s, i1, f1) -> exall n "owl:allValuesFrom" s i1 f1 None |
||

1588 | | MIN (card, s, i1, f1) -> |
||

1589 | exall n "owl:onClass" s i1 f1 (Some ("owl:minQualifiedCardinality", card)) |
||

1590 | | MAX (card, s, i1, f1) -> |
||

1591 | exall n "owl:onClass" s i1 f1 (Some ("owl:maxQualifiedCardinality", card)) |
||

1592 | | OR (f1, f2) -> andor n "owl:unionOf" f1 f2 |
||

1593 | | AND (f1, f2) -> andor n "owl:intersectionOf" f1 f2 |
||

1594 | in |
||

1595 | let printAxiom c1 c2 s f = |
||

1596 | ps 2 ("<rdf:Description " ^ c1 ^ "=\"" ^ s ^ "\">\n"); |
||

1597 | ps 3 ("<" ^ c2 ^ ">\n"); |
||

1598 | printFormula 4 f; |
||

1599 | ps 3 ("</" ^ c2 ^ ">\n"); |
||

1600 | ps 2 "</rdf:Description>\n\n"; |
||

1601 | in |
||

1602 | let printTBoxD = function |
||

1603 | | PRIMITIVE (s, f) -> printAxiom "rdf:about" "rdfs:subClassOf" ("#p" ^ s) f |
||

1604 | | NECANDSUFF (s, f) -> printAxiom "rdf:about" "owl:equivalentClass" ("#p" ^ s) f |
||

1605 | in |
||

1606 | let printTBoxND f = printAxiom "rdf:about" "rdfs:subClassOf" "&owl;Thing" f in |
||

1607 | ps 0 "<?xml version=\"1.0\"?>\n\n"; |
||

1608 | ps 0 "<!DOCTYPE rdf:RDF [\n"; |
||

1609 | ps 5 "<!ENTITY owl \"http://www.w3.org/2002/07/owl#\" >\n"; |
||

1610 | ps 5 "<!ENTITY xsd \"http://www.w3.org/2001/XMLSchema#\" >\n"; |
||

1611 | (* ps 5 "<!ENTITY rdfs \"http://www.w3.org/2000/01/rdf-schema#\" >\n"; *) |
||

1612 | ps 0 "]>\n\n"; |
||

1613 | ps 0 "<rdf:RDF xml:base=\"http://example.com/tmp\"\n"; |
||

1614 | ps 1 "xmlns=\"http://example.com/tmp\"\n"; |
||

1615 | ps 1 "xmlns:rdf=\"http://www.w3.org/1999/02/22-rdf-syntax-ns#\"\n"; |
||

1616 | ps 1 "xmlns:rdfs=\"http://www.w3.org/2000/01/rdf-schema#\"\n"; |
||

1617 | ps 1 "xmlns:owl=\"http://www.w3.org/2002/07/owl#\"\n"; |
||

1618 | ps 1 "xmlns:xsd=\"http://www.w3.org/2001/XMLSchema#\">\n\n"; |
||

1619 | ps 2 "<owl:Ontology rdf:about=\"\"/>\n\n"; |
||

1620 | List.iter (fun s -> ps 2 ("<owl:Class rdf:about=\"#p" ^ s ^ "\"/>\n")) pl; |
||

1621 | List.iter (fun s -> ps 2 ("<owl:ObjectProperty rdf:about=\"#r" ^ s ^ "\"/>\n")) rl; |
||

1622 | ps 0 "\n"; |
||

1623 | List.iter printTBoxD tboxD; |
||

1624 | List.iter printTBoxND tboxND; |
||

1625 | ps 0 "\n"; |
||

1626 | printAxiom "rdf:nodeID" "rdf:type" "_:a" f; |
||

1627 | ps 0 "</rdf:RDF>\n"; |
||

1628 | close_out file |
||

1629 | |||

1630 | |||

1631 | let lexerf = A.make_lexer_file ~comment:"%" |
||

1632 | ["(";")";".";",";"inputformula";"hypothesis";"axiom";"conjecture"; |
||

1633 | "-";"~";"&";"|";"=>";"pos";"box";":";"true";"false"] |
||

1634 | |||

1635 | (** These functions parse a TANCS token stream to obtain a formula. |
||

1636 | It is a standard recursive descent procedure. |
||

1637 | @param ts A token stream. |
||

1638 | @return The resulting (sub-)formula. |
||

1639 | @raise ALCException if ts does not represent a formula. |
||

1640 | *) |
||

1641 | let rec parseTancs_equ ts = |
||

1642 | let f1 = parseTancs_imp ts in |
||

1643 | match Stream.peek ts with |
||

1644 | | None -> f1 |
||

1645 | | Some (A.Kwd "<=>") -> |
||

1646 | Stream.junk ts; |
||

1647 | let f2 = parseTancs_equ ts in |
||

1648 | EQU (f1, f2) |
||

1649 | | _ -> f1 |
||

1650 | |||

1651 | (** These functions parse a TANCS token stream to obtain a formula. |
||

1652 | It is a standard recursive descent procedure. |
||

1653 | @param ts A token stream. |
||

1654 | @return The resulting (sub-)formula. |
||

1655 | @raise ALCException if ts does not represent a formula. |
||

1656 | *) |
||

1657 | and parseTancs_imp ts = |
||

1658 | let f1 = parseTancs_or ts in |
||

1659 | match Stream.peek ts with |
||

1660 | | None -> f1 |
||

1661 | | Some (A.Kwd "=>") -> |
||

1662 | Stream.junk ts; |
||

1663 | let f2 = parseTancs_imp ts in |
||

1664 | IMP (f1, f2) |
||

1665 | | _ -> f1 |
||

1666 | |||

1667 | (** These functions parse a TANCS token stream to obtain a formula. |
||

1668 | It is a standard recursive descent procedure. |
||

1669 | @param ts A token stream. |
||

1670 | @return The resulting (sub-)formula. |
||

1671 | @raise ALCException if ts does not represent a formula. |
||

1672 | *) |
||

1673 | and parseTancs_or ts = |
||

1674 | let f1 = parseTancs_and ts in |
||

1675 | match Stream.peek ts with |
||

1676 | | None -> f1 |
||

1677 | | Some (A.Kwd "|") -> |
||

1678 | Stream.junk ts; |
||

1679 | let f2 = parseTancs_or ts in |
||

1680 | OR (f1, f2) |
||

1681 | | _ -> f1 |
||

1682 | |||

1683 | (** These functions parse a TANCS token stream to obtain a formula. |
||

1684 | It is a standard recursive descent procedure. |
||

1685 | @param ts A token stream. |
||

1686 | @return The resulting (sub-)formula. |
||

1687 | @raise ALCException if ts does not represent a formula. |
||

1688 | *) |
||

1689 | and parseTancs_and ts = |
||

1690 | let f1 = parseTancs_rest ts in |
||

1691 | match Stream.peek ts with |
||

1692 | | None -> f1 |
||

1693 | | Some (A.Kwd "&") -> |
||

1694 | Stream.junk ts; |
||

1695 | let f2 = parseTancs_and ts in |
||

1696 | AND (f1, f2) |
||

1697 | | _ -> f1 |
||

1698 | |||

1699 | (** These functions parse a TANCS token stream to obtain a formula. |
||

1700 | It is a standard recursive descent procedure. |
||

1701 | @param ts A token stream. |
||

1702 | @return The resulting (sub-)formula. |
||

1703 | @raise ALCException if ts does not represent a formula. |
||

1704 | *) |
||

1705 | and parseTancs_rest ts = |
||

1706 | let token = Stream.next ts in |
||

1707 | match token with |
||

1708 | | A.Kwd "pos" |
||

1709 | | A.Kwd "box" -> begin |
||

1710 | let s = |
||

1711 | match Stream.peek ts with |
||

1712 | | Some (A.Ident s1) -> Stream.junk ts; s1 |
||

1713 | | Some (A.Kwd ":") -> "" |
||

1714 | | Some (A.Kwd "-") -> "" |
||

1715 | | Some t -> A.printError mk_exn ~t ~ts "role name, \"-\", or \":\" expected: " |
||

1716 | | None -> A.printError mk_exn ~ts "role name, \"-\", or \":\" expected: " |
||

1717 | in |
||

1718 | let isInv = |
||

1719 | match Stream.next ts with |
||

1720 | | A.Kwd ":" -> false |
||

1721 | | A.Kwd "-" -> begin |
||

1722 | match Stream.next ts with |
||

1723 | | A.Kwd ":" -> true |
||

1724 | | t -> A.printError mk_exn ~t ~ts "\":\" expected: " |
||

1725 | end |
||

1726 | | t -> A.printError mk_exn ~t ~ts "\":\" or \"-\" expected: " |
||

1727 | in |
||

1728 | let f1 = parseTancs_rest ts in |
||

1729 | match token with |
||

1730 | | A.Kwd "pos" -> EX (s, isInv, f1) |
||

1731 | | _ -> AX (s, isInv, f1) |
||

1732 | end |
||

1733 | | A.Kwd "(" -> |
||

1734 | let f = parseTancs_equ ts in |
||

1735 | let _ = |
||

1736 | match Stream.next ts with |
||

1737 | | A.Kwd ")" -> () |
||

1738 | | t -> A.printError mk_exn ~t ~ts "\")\" expected: " |
||

1739 | in |
||

1740 | f |
||

1741 | | A.Kwd "~" -> |
||

1742 | let f = parseTancs_rest ts in |
||

1743 | NOT f |
||

1744 | | A.Kwd "true" -> TRUE |
||

1745 | | A.Kwd "false" -> FALSE |
||

1746 | | A.Ident s -> AP s |
||

1747 | | t -> A.printError mk_exn ~t ~ts |
||

1748 | "\"pos\", \"box\", \"~\", \"(\", \"true\", \"false\", or <ident> expected: " |
||

1749 | |||

1750 | (** These functions parse a TANCS token stream to obtain a set of clauses. |
||

1751 | It is a standard recursive descent procedure. |
||

1752 | @param ts A token stream. |
||

1753 | @param axl The axioms parsed so far. |
||

1754 | @param hypl The hyptheses parsed so far. |
||

1755 | @param conl The conjectures parsed so far. |
||

1756 | @return A triple (axl, hypl, conl) where |
||

1757 | axl is a list of formula representing axioms; |
||

1758 | hypl is a list of formula representing hypotheses; |
||

1759 | conl is a list of formula representing conjectures; |
||

1760 | @raise ALCException if s does not represent a set of clauses. |
||

1761 | *) |
||

1762 | let rec parseTancs_clauses ts axl hypl conl = |
||

1763 | match Stream.peek ts with |
||

1764 | | Some (A.Kwd "inputformula") -> begin |
||

1765 | Stream.junk ts; |
||

1766 | A.getKws mk_exn ts ["("]; |
||

1767 | let _ = |
||

1768 | match Stream.next ts with |
||

1769 | | A.Ident s -> s |
||

1770 | | t -> A.printError mk_exn ~t "clause name expected: " |
||

1771 | in |
||

1772 | A.getKws mk_exn ts [","]; |
||

1773 | let ty = |
||

1774 | match Stream.next ts with |
||

1775 | | A.Kwd "axiom" -> 1 |
||

1776 | | A.Kwd "hypothesis" -> 2 |
||

1777 | | A.Kwd "conjecture" -> 3 |
||

1778 | | t -> A.printError mk_exn ~t |
||

1779 | "clause type (i.e. \"hypothesis\", \"axiom\", or \"conjecture\") expected: " |
||

1780 | in |
||

1781 | A.getKws mk_exn ts [","]; |
||

1782 | let cl = parseTancs_equ ts in |
||

1783 | A.getKws mk_exn ts [")";"."]; |
||

1784 | match ty with |
||

1785 | | 1 -> parseTancs_clauses ts (cl::axl) hypl conl |
||

1786 | | 2 -> parseTancs_clauses ts axl (cl::hypl) conl |
||

1787 | | _ -> parseTancs_clauses ts axl hypl (cl::conl) |
||

1788 | end |
||

1789 | | _ -> (axl, hypl, conl) |
||

1790 | |||

1791 | (** Imports queries in TAMCS2000 style. |
||

1792 | @param filename The name of the input file. |
||

1793 | @return A triple (fl, tboxND, tboxD) where |
||

1794 | fl is a list of formula representing the initial input; |
||

1795 | tboxND is a list of formulae representing |
||

1796 | the non-definitional part of a TBox; and |
||

1797 | tboxD is a list of definitions |
||

1798 | representing the definitional part of a TBox. |
||

1799 | @raise ALCException if s does not represent a formula query. |
||

1800 | *) |
||

1801 | let importTancs2000 filename = |
||

1802 | let file = open_in filename in |
||

1803 | let ts = lexerf file in |
||

1804 | try |
||

1805 | begin |
||

1806 | let (axl, hypl, conl) = parseTancs_clauses ts [] [] [] in |
||

1807 | let _ = |
||

1808 | match Stream.peek ts with |
||

1809 | | None -> () |
||

1810 | | Some _ -> A.printError mk_exn ~ts "EOS expected: " |
||

1811 | in |
||

1812 | assert (conl <> []); |
||

1813 | let conc = |
||

1814 | List.fold_left (fun res f -> OR (res, NOT f)) (NOT (List.hd conl)) (List.tl conl) |
||

1815 | in |
||

1816 | close_in file; |
||

1817 | (conc::hypl, axl, []) |
||

1818 | end |
||

1819 | with Stream.Failure -> |
||

1820 | close_in file; |
||

1821 | A.printError mk_exn ~ts "unexpected EOS" |