### Profile

Statistics
| Branch: | Revision:

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

1 2 3 4fd28192 Thorsten Wißmann ```(** This module implements ALC formulae ``` ``` including inverse roles ``` ``` (e.g. parsing, printing, (de-)constructing, ...). ``` ``` @author Florian Widmann ``` ``` *) ``` ```module HC = HashConsing ``` ```module A = AltGenlex ``` ```(** A general exception for all kinds of errors ``` ``` that can happen in the tableau procedure. ``` ``` More specific information is given in the argument. ``` ``` *) ``` ```exception ALCException of string ``` ```(** Defines ALC formulae. ``` ``` *) ``` ```type formula = ``` ``` | TRUE ``` ``` | FALSE ``` ``` | AP of string ``` ``` | NOT of formula ``` ``` | EX of string * bool * formula ``` ``` | AX of string * bool * formula ``` ``` | MIN of int * string * bool * formula ``` ``` | MAX of int * string * bool * formula ``` ``` | EQU of formula * formula ``` ``` | IMP of formula * formula ``` ``` | OR of formula * formula ``` ``` | AND of formula * formula ``` ```(** Defines TBox definitions. ``` ``` It can either be a primitive definition ``` ``` of the form cn <= f, ``` ``` or a necessary and sufficient definition ``` ``` of the form cn = f ``` ``` (where cn is a concept name and f a concept). ``` ``` *) ``` ```type definition = ``` ``` | PRIMITIVE of string * formula ``` ``` | NECANDSUFF of string * formula ``` ```(** The number of constructors of type formula. ``` ``` *) ``` ```let numberOfTypes = 12 ``` ```(** Maps a formula to an integer representing its type (e.g. or-formula). ``` ``` The assignment of integers to types is arbitrary, ``` ``` but it is guaranteed that different types ``` ``` map to different integers ``` ``` and that the codomain of this function is [0..numberOfTypes-1]. ``` ``` @param f A formula. ``` ``` @return An integer that represents the type of f. ``` ``` *) ``` ```let getTypeFormula f = ``` ``` match f with ``` ``` | TRUE -> 0 ``` ``` | FALSE -> 1 ``` ``` | AP _ -> 2 ``` ``` | NOT _ -> 3 ``` ``` | EX _ -> 4 ``` ``` | AX _ -> 5 ``` ``` | EQU _ -> 6 ``` ``` | IMP _ -> 7 ``` ``` | OR _ -> 8 ``` ``` | AND _ -> 9 ``` ``` | MIN _ -> 10 ``` ``` | MAX _ -> 11 ``` ```(** Generates a function comp that compares two formula. ``` ``` The order that is defined by comp is lexicograhic. ``` ``` It depends on the given ranking of types of formulae. ``` ``` @param order A list containing exactly the numbers 0 to numberOfTypes-1. ``` ``` Each number represents a type ``` ``` and the list therefore induces a ranking on the types ``` ``` with the smallest type being the first in the list. ``` ``` @return A function comp that compares two formula. ``` ``` comp f1 f2 returns 0 iff f1 is equal to f2, ``` ``` -1 if f1 is smaller than f2, and ``` ``` 1 if f1 is greater than f2. ``` ``` @raise Failure if order is not of the required form. ``` ``` *) ``` ```let generateCompare order = ``` ``` let rec listOK = function ``` ``` | 0 -> true ``` ``` | n -> ``` ``` let nn = pred n in ``` ``` if List.mem nn order then listOK nn ``` ``` else false ``` ``` in ``` ``` let _ = ``` ``` if (List.length order <> numberOfTypes) || not (listOK numberOfTypes) then ``` ``` raise (Failure "generateCompare: argument is not in the correct form") ``` ``` in ``` ``` let arrayOrder = Array.make numberOfTypes 0 in ``` ``` let _ = ``` ``` for i = 0 to (numberOfTypes - 1) do ``` ``` let ty = List.nth order i in ``` ``` arrayOrder.(ty) <- i ``` ``` done ``` ``` in ``` ``` let rec comp f1 f2 = ``` ``` match f1, f2 with ``` ``` | TRUE, TRUE ``` ``` | FALSE, FALSE -> 0 ``` ``` | AP s1, AP s2 -> compare s1 s2 ``` ``` | NOT f1a, NOT f2a -> comp f1a f2a ``` ``` | EX (s1, i1, f1a), EX (s2, i2, f2a) ``` ``` | AX (s1, i1, f1a), AX (s2, i2, f2a) -> ``` ``` let res1 = compare s1 s2 in ``` ``` if res1 <> 0 then res1 ``` ``` else ``` ``` let res2 = compare i1 i2 in ``` ``` if res2 <> 0 then res2 ``` ``` else comp f1a f2a ``` ``` | MIN (n1, s1, i1, f1a), MIN (n2, s2, i2, f2a) ``` ``` | MAX (n1, s1, i1, f1a), MAX (n2, s2, i2, f2a) -> ``` ``` let res0 = compare n1 n2 in ``` ``` if res0 <> 0 then res0 ``` ``` else ``` ``` let res1 = compare s1 s2 in ``` ``` if res1 <> 0 then res1 ``` ``` else ``` ``` let res2 = compare i1 i2 in ``` ``` if res2 <> 0 then res2 ``` ``` else comp f1a f2a ``` ``` | OR (f1a, f1b), OR (f2a, f2b) ``` ``` | AND (f1a, f1b), AND (f2a, f2b) ``` ``` | EQU (f1a, f1b), EQU (f2a, f2b) ``` ``` | IMP (f1a, f1b), IMP (f2a, f2b) -> ``` ``` let res1 = comp f1a f2a in ``` ``` if res1 <> 0 then res1 ``` ``` else comp f1b f2b ``` ``` | _ -> ``` ``` let t1 = getTypeFormula f1 in ``` ``` let r1 = arrayOrder.(t1) in ``` ``` let t2 = getTypeFormula f2 in ``` ``` let r2 = arrayOrder.(t2) in ``` ``` if r1 < r2 then (-1) else 1 ``` ``` in ``` ``` comp ``` ```(** Defines a ranking of the different types of formulae ``` ``` such that the ranking of the types corresponds ``` ``` to the ranking of the tableau rules. ``` ``` *) ``` ```let aRanking = [ getTypeFormula (OR (TRUE, TRUE)); ``` ``` getTypeFormula (EX ("", false, TRUE)); ``` ``` getTypeFormula (AX ("", false, TRUE)); ``` ``` getTypeFormula TRUE; ``` ``` getTypeFormula FALSE; ``` ``` getTypeFormula (AP ""); ``` ``` getTypeFormula (NOT TRUE); ``` ``` getTypeFormula (AND (TRUE, TRUE)); ``` ``` getTypeFormula (EQU (TRUE, TRUE)); ``` ``` getTypeFormula (IMP (TRUE, TRUE)); ``` ``` getTypeFormula (MIN (0, "", false, TRUE)); ``` ``` getTypeFormula (MAX (0, "", false, TRUE)) ] ``` ```(** Determines the size of a formula. ``` ``` Basically, it counts the symbols (without parentheses) of a formula, ``` ``` where _ etc. is treated as one symbol. ``` ``` @param f A formula. ``` ``` @return The size of f. ``` ``` *) ``` ```let rec sizeFormula f = ``` ``` match f with ``` ``` | TRUE ``` ``` | FALSE ``` ``` | AP _ -> 1 ``` ``` | NOT f1 ``` ``` | EX (_, _, f1) ``` ``` | AX (_, _, f1) ``` ``` | MIN (_, _, _, f1) ``` ``` | MAX (_, _, _, f1) -> succ (sizeFormula f1) ``` ``` | EQU (f1, f2) ``` ``` | IMP (f1, f2) ``` ``` | OR (f1, f2) ``` ``` | AND (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2) ``` ```(** Appends a string representation of a formula to a string buffer. ``` ``` Parentheses are ommited where possible ``` ``` where the preference rules are defined as usual. ``` ``` @param sb A string buffer. ``` ``` @param f A formula. ``` ``` *) ``` ```let rec exportFormula_buffer sb f = ``` ``` let prio n lf = ``` ``` let prionr = function ``` ``` | EQU _ -> 0 ``` ``` | IMP _ -> 1 ``` ``` | OR _ -> 2 ``` ``` | AND _ -> 3 ``` ``` | _ -> 4 ``` ``` in ``` ``` if prionr lf < n then begin ``` ``` Buffer.add_char sb '('; ``` ``` exportFormula_buffer sb lf; ``` ``` Buffer.add_char sb ')' ``` ``` end ``` ``` else exportFormula_buffer sb lf ``` ``` in ``` ``` match f with ``` ``` | TRUE -> Buffer.add_string sb "True" ``` ``` | FALSE -> Buffer.add_string sb "False" ``` ``` | AP s -> Buffer.add_string sb s ``` ``` | NOT f1 -> ``` ``` Buffer.add_string sb "~"; ``` ``` prio 4 f1 ``` ``` | EX (s, i1, f1) -> ``` ``` Buffer.add_string sb "<"; ``` ``` Buffer.add_string sb s; ``` ``` if i1 then Buffer.add_string sb "-" else (); ``` ``` Buffer.add_string sb ">"; ``` ``` prio 4 f1 ``` ``` | AX (s, i1, f1) -> ``` ``` Buffer.add_string sb "["; ``` ``` Buffer.add_string sb s; ``` ``` if i1 then Buffer.add_string sb "-" else (); ``` ``` Buffer.add_string sb "]"; ``` ``` prio 4 f1 ``` ``` | MIN (n, s, i1, f1) -> ``` ``` Buffer.add_string sb "{>="; ``` ``` Buffer.add_string sb (string_of_int n); ``` ``` Buffer.add_string sb " "; ``` ``` Buffer.add_string sb s; ``` ``` if i1 then Buffer.add_string sb "-" else (); ``` ``` Buffer.add_string sb "}"; ``` ``` prio 4 f1 ``` ``` | MAX (n, s, i1, f1) -> ``` ``` Buffer.add_string sb "{<="; ``` ``` Buffer.add_string sb (string_of_int n); ``` ``` Buffer.add_string sb " "; ``` ``` Buffer.add_string sb s; ``` ``` if i1 then Buffer.add_string sb "-" else (); ``` ``` Buffer.add_string sb "}"; ``` ``` prio 4 f1 ``` ``` | EQU (f1, f2) -> ``` ``` prio 0 f1; ``` ``` Buffer.add_string sb " <=> "; ``` ``` prio 0 f2 ``` ``` | IMP (f1, f2) -> ``` ``` prio 2 f1; ``` ``` Buffer.add_string sb " => "; ``` ``` prio 2 f2 ``` ``` | OR (f1, f2) -> ``` ``` prio 2 f1; ``` ``` Buffer.add_string sb " | "; ``` ``` prio 2 f2 ``` ``` | AND (f1, f2) -> ``` ``` prio 3 f1; ``` ``` Buffer.add_string sb " & "; ``` ``` prio 3 f2 ``` ```(** Converts a formula into a string representation. ``` ``` Parentheses are ommited where possible ``` ``` where the preference rules are defined as usual. ``` ``` @param f A formula. ``` ``` @return A string representing f. ``` ``` *) ``` ```let exportFormula f = ``` ``` let size = sizeFormula f in ``` ``` let sb = Buffer.create (2 * size) in ``` ``` exportFormula_buffer sb f; ``` ``` Buffer.contents sb ``` ```(** Converts a formula query into a string representation. ``` ``` @param fl A list of formulae representing the initial input. ``` ``` @param tboxND A list of formulae representing ``` ``` the non-definitional part of a TBox. ``` ``` @param tboxD A list of definitions ``` ``` representing the definitional part of a TBox. ``` ``` @return A string representing tboxND; tboxD |- fl. ``` ``` @raise ALCException Iff one of the defined formulae in tboxD ``` ``` is not a concept. ``` ``` *) ``` ```let exportQuery fl tboxND tboxD = ``` ``` let sb = Buffer.create 1000 in ``` ``` let exportDef = function ``` ``` | PRIMITIVE (s, f) -> ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb " # "; ``` ``` exportFormula_buffer sb f ``` ``` | NECANDSUFF (s, f) -> ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb " = "; ``` ``` exportFormula_buffer sb f ``` ``` in ``` ``` let rec expFl fkt = function ``` ``` | [] -> () ``` ``` | h::tl -> ``` ``` fkt h; ``` ``` if tl <> [] then Buffer.add_string sb "; " else (); ``` ``` expFl fkt tl ``` ``` in ``` ``` expFl (exportFormula_buffer sb) tboxND; ``` ``` if tboxND <> [] && tboxD <> [] then Buffer.add_string sb "; " else (); ``` ``` expFl exportDef tboxD; ``` ``` Buffer.add_string sb " |- "; ``` ``` expFl (exportFormula_buffer sb) fl; ``` ``` Buffer.contents sb ``` ```let lexer = A.make_lexer ``` ``` ["#";"=";"|-";";";"(";")";"=>";"<=>";"|";"&";"~";"True";"False";"<";">";"[";"]";"-";"{<=";"{>=";"}"] ``` ```let mk_exn s = ALCException s ``` ```(** These functions parse a token stream to obtain a formula. ``` ``` It is a standard recursive descent procedure. ``` ``` @param ts A token stream. ``` ``` @return The resulting (sub-)formula. ``` ``` @raise ALCException if ts does not represent a formula. ``` ``` *) ``` ```let rec parse_equ ts = ``` ``` let f1 = parse_imp ts in ``` ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "<=>") -> ``` ``` Stream.junk ts; ``` ``` let f2 = parse_equ ts in ``` ``` EQU (f1, f2) ``` ``` | _ -> f1 ``` ```(** These functions parse a token stream to obtain a formula. ``` ``` It is a standard recursive descent procedure. ``` ``` @param ts A token stream. ``` ``` @return The resulting (sub-)formula. ``` ``` @raise ALCException if ts does not represent a formula. ``` ``` *) ``` ```and parse_imp ts = ``` ``` let f1 = parse_or ts in ``` ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "=>") -> ``` ``` Stream.junk ts; ``` ``` let f2 = parse_imp ts in ``` ``` IMP (f1, f2) ``` ``` | _ -> f1 ``` ```(** These functions parse a token stream to obtain a formula. ``` ``` It is a standard recursive descent procedure. ``` ``` @param ts A token stream. ``` ``` @return The resulting (sub-)formula. ``` ``` @raise ALCException if ts does not represent a formula. ``` ``` *) ``` ```and parse_or ts = ``` ``` let f1 = parse_and ts in ``` ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "|") -> ``` ``` Stream.junk ts; ``` ``` let f2 = parse_or ts in ``` ``` OR (f1, f2) ``` ``` | _ -> f1 ``` ```(** These functions parse a token stream to obtain a formula. ``` ``` It is a standard recursive descent procedure. ``` ``` @param ts A token stream. ``` ``` @return The resulting (sub-)formula. ``` ``` @raise ALCException if ts does not represent a formula. ``` ``` *) ``` ```and parse_and ts = ``` ``` let f1 = parse_rest ts in ``` ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "&") -> ``` ``` Stream.junk ts; ``` ``` let f2 = parse_and ts in ``` ``` AND (f1, f2) ``` ``` | _ -> f1 ``` ```(** These functions parse a token stream to obtain a formula. ``` ``` It is a standard recursive descent procedure. ``` ``` @param ts A token stream. ``` ``` @return The resulting (sub-)formula. ``` ``` @raise ALCException if ts does not represent a formula. ``` ``` *) ``` ```and parse_rest ts = ``` ``` let boxinternals noNo es = ``` ``` let n = ``` ``` if noNo then 0 ``` ``` else ``` ``` match Stream.next ts with ``` ``` | A.Int n when n >= 0 -> n ``` ``` | t -> A.printError mk_exn ~t ~ts " expected: " ``` ``` in ``` ``` let s = ``` ``` match Stream.peek ts with ``` ``` | Some (A.Ident s1) -> Stream.junk ts; s1 ``` ``` | Some (A.Kwd c) when c = es -> "" ``` ``` | Some (A.Kwd "-") -> "" ``` ``` | Some t -> A.printError mk_exn ~ts ("role name, \"-\", or \"" ^ es ^ "\" expected: ") ``` ``` | None -> A.printError mk_exn ~ts ("role name, \"-\", or \"" ^ es ^ "\" expected: ") ``` ``` in ``` ``` let isInv = ``` ``` match Stream.next ts with ``` ``` | A.Kwd c when c = es -> false ``` ``` | A.Kwd "-" -> begin ``` ``` match Stream.next ts with ``` ``` | A.Kwd c when c = es -> true ``` ``` | t -> A.printError mk_exn ~t ~ts ("\"" ^ es ^ "\" expected: ") ``` ``` end ``` ``` | t -> A.printError mk_exn ~t ~ts ("\"-\" or \"" ^ es ^ "\" expected: ") ``` ``` in ``` ``` (n, s, isInv) ``` ``` in ``` ``` match Stream.next ts with ``` ``` | A.Kwd "<" -> ``` ``` let (_, s, isInv) = boxinternals true ">" in ``` ``` let f1 = parse_rest ts in ``` ``` EX (s, isInv, f1) ``` ``` | A.Kwd "[" -> ``` ``` let (_, s, isInv) = boxinternals true "]" in ``` ``` let f1 = parse_rest ts in ``` ``` AX (s, isInv, f1) ``` ``` | A.Kwd "{>=" -> ``` ``` let (n, s, isInv) = boxinternals false "}" in ``` ``` let f1 = parse_rest ts in ``` ``` MIN (n, s, isInv, f1) ``` ``` | A.Kwd "{<=" -> ``` ``` let (n, s, isInv) = boxinternals false "}" in ``` ``` let f1 = parse_rest ts in ``` ``` MAX (n, s, isInv, f1) ``` ``` | A.Kwd "(" -> ``` ``` let f = parse_equ ts in ``` ``` let _ = ``` ``` match Stream.next ts with ``` ``` | A.Kwd ")" -> () ``` ``` | t -> A.printError mk_exn ~t ~ts "\")\" expected: " ``` ``` in ``` ``` f ``` ``` | A.Kwd "~" -> ``` ``` let f = parse_rest ts in ``` ``` NOT f ``` ``` | A.Kwd "True" -> TRUE ``` ``` | A.Kwd "False" -> FALSE ``` ``` | A.Ident s -> AP s ``` ``` | t -> A.printError mk_exn ~t ~ts ``` ``` "\"<\", \"[\", \"~\", \"(\", \"True\", \"False\", or expected: " ``` ``` ``` ```(** Parses a string to obtain a formula. ``` ``` @param s A string representing a formula. ``` ``` @return The resulting formula. ``` ``` @raise ALCException if s does not represent a formula. ``` ``` *) ``` ```let importFormula s = ``` ``` let ts = lexer s in ``` ``` try ``` ``` begin ``` ``` let f = parse_equ ts in ``` ``` let _ = ``` ``` match Stream.peek ts with ``` ``` | None -> () ``` ``` | Some _ -> A.printError mk_exn ~ts "EOS expected: " ``` ``` in ``` ``` f ``` ``` end ``` ``` with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS" ``` ```(** Parses a list of formulae separated by ";". ``` ``` @param wDef Iff set to true then definitions are allowed. ``` ``` @param ts A token stream. ``` ``` @param accF The list of formulae parsed so far. ``` ``` @param accD The list of definitions parsed so far. ``` ``` @return The resulting lists of formulae and definitions. ``` ``` @raise ALCException if ts does not represent a list of formulae ``` ``` and definitions (if allowed). ``` ``` *) ``` ```let rec parse_formulaeDefList wDef ts (accF, accD) = ``` ``` let defopt = ``` ``` if not wDef then None ``` ``` else ``` ``` let p2 = Stream.npeek 2 ts in ``` ``` if List.length p2 < 2 then None ``` ``` else ``` ``` match List.hd p2 with ``` ``` | A.Ident s1 -> begin ``` ``` match List.nth p2 1 with ``` ``` | A.Kwd "=" -> ``` ``` Stream.junk ts; ``` ``` Stream.junk ts; ``` ``` let f1 = parse_equ ts in ``` ``` Some (NECANDSUFF (s1, f1)) ``` ``` | A.Kwd "#" -> ``` ``` Stream.junk ts; ``` ``` Stream.junk ts; ``` ``` let f1 = parse_equ ts in ``` ``` Some (PRIMITIVE (s1, f1)) ``` ``` | _ -> None ``` ``` end ``` ``` | _ -> None ``` ``` in ``` ``` let (accF1, accD1) as acc1 = ``` ``` match defopt with ``` ``` | None -> ``` ``` let f1 = parse_equ ts in ``` ``` (f1::accF, accD) ``` ``` | Some def -> (accF, def::accD) ``` ``` in ``` ``` match Stream.peek ts with ``` ``` | Some (A.Kwd ";") -> ``` ``` Stream.junk ts; ``` ``` parse_formulaeDefList wDef ts acc1 ``` ``` | _ -> (List.rev accF1, List.rev accD1) ``` ```(** Parses a string to obtain a formula query. ``` ``` @param s A string representing a formula query. ``` ``` @return A triple (fl, tboxND, tboxD) where ``` ``` fl is a list of formula representing the initial input; ``` ``` tboxND is a list of formulae representing ``` ``` the non-definitional part of a TBox; and ``` ``` tboxD is a list of definitions ``` ``` representing the definitional part of a TBox. ``` ``` @raise ALCException if s does not represent a formula query. ``` ``` *) ``` ```let importQuery s = ``` ``` let ts = lexer s in ``` ``` try ``` ``` begin ``` ``` let res = ``` ``` match Stream.peek ts with ``` ``` | Some (A.Kwd "|-") -> ``` ``` Stream.junk ts; ``` ``` let (fl1, _) = parse_formulaeDefList false ts ([], []) in ``` ``` (fl1, [], []) ``` ``` | _ -> ``` ``` begin ``` ``` let (fl1, dl1) = parse_formulaeDefList true ts ([], []) in ``` ``` match Stream.peek ts with ``` ``` | Some (A.Kwd "|-") -> ``` ``` Stream.junk ts; ``` ``` let (fl2, _) = parse_formulaeDefList false ts ([], []) in ``` ``` (fl2, fl1, dl1) ``` ``` | _ -> ``` ``` if dl1 = [] then (fl1, [], []) ``` ``` else A.printError mk_exn ~ts "\"|-\" expected: " ``` ``` end ``` ``` in ``` ``` let _ = ``` ``` match Stream.peek ts with ``` ``` | None -> () ``` ``` | Some _ -> A.printError mk_exn ~ts "EOS expected: " ``` ``` in ``` ``` res ``` ``` end ``` ``` with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS" ``` ```(** Substitutes some propositional variables in a formula. ``` ``` @param subl A list of pairs (s, fp) ``` ``` where s is the name of a propositional variable and fp is a formula. ``` ``` @param f A formula. ``` ``` @return A formula f' where each propositional variable p ``` ``` such that (p, fp) is contained in subl is replaced by fp. ``` ``` *) ``` ```let rec substFormula subl f = ``` ``` match f with ``` ``` | TRUE ``` ``` | FALSE -> f ``` ``` | AP s -> if List.mem_assoc s subl then List.assoc s subl else f ``` ``` | NOT f1 -> ``` ``` let ft = substFormula subl f1 in ``` ``` if ft == f1 then f else NOT ft ``` ``` | EX (s, i, f1) -> ``` ``` let ft = substFormula subl f1 in ``` ``` if ft == f1 then f else EX (s, i, ft) ``` ``` | AX (s, i, f1) -> ``` ``` let ft = substFormula subl f1 in ``` ``` if ft == f1 then f else AX (s, i, ft) ``` ``` | MIN (n, s, i, f1) -> ``` ``` let ft = substFormula subl f1 in ``` ``` if ft == f1 then f else MIN (n, s, i, ft) ``` ``` | MAX (n, s, i, f1) -> ``` ``` let ft = substFormula subl f1 in ``` ``` if ft == f1 then f else MAX (n, s, i, ft) ``` ``` | EQU (f1, f2) -> ``` ``` let ft1 = substFormula subl f1 in ``` ``` let ft2 = substFormula subl f2 in ``` ``` if (f1 == ft1) && (f2 == ft2) then f ``` ``` else EQU (ft1, ft2) ``` ``` | IMP (f1, f2) -> ``` ``` let ft1 = substFormula subl f1 in ``` ``` let ft2 = substFormula subl f2 in ``` ``` if (f1 == ft1) && (f2 == ft2) then f ``` ``` else IMP (ft1, ft2) ``` ``` | OR (f1, f2) -> ``` ``` let ft1 = substFormula subl f1 in ``` ``` let ft2 = substFormula subl f2 in ``` ``` if (f1 == ft1) && (f2 == ft2) then f ``` ``` else OR (ft1, ft2) ``` ``` | AND (f1, f2) -> ``` ``` let ft1 = substFormula subl f1 in ``` ``` let ft2 = substFormula subl f2 in ``` ``` if (f1 == ft1) && (f2 == ft2) then f ``` ``` else AND (ft1, ft2) ``` ```(** Converts the negation of a formula to negation normal form ``` ``` by "pushing in" the negations "~". ``` ``` The symbols "<=>" and "=>" are substituted by their usual definitions. ``` ``` @param f A formula. ``` ``` @return A formula in negation normal form and not containing "<=>" or "=>" ``` ``` that is equivalent to ~f. ``` ``` *) ``` ```let rec nnfNeg f = ``` ``` match f with ``` ``` | TRUE -> FALSE ``` ``` | FALSE -> TRUE ``` ``` | AP _ -> NOT f ``` ``` | NOT f1 -> nnf f1 ``` ``` | EX (s, i, f1) -> AX (s, i, nnfNeg f1) ``` ``` | AX (s, i, f1) -> EX (s, i, nnfNeg f1) ``` ``` | MIN (n, s, i, f1) -> ``` ``` if n = 0 then FALSE else MAX (n-1, s, i, nnf f1) ``` ``` | MAX (n, s, i, f1) -> MIN (n+1, s, i, nnf f1) ``` ``` | EQU (f1, f2) -> OR (AND (nnf f1, nnfNeg f2), AND (nnf f2, nnfNeg f1)) ``` ``` | IMP (f1, f2) -> AND (nnf f1, nnfNeg f2) ``` ``` | OR (f1, f2) -> AND (nnfNeg f1, nnfNeg f2) ``` ``` | AND (f1, f2) -> OR (nnfNeg f1, nnfNeg f2) ``` ``` ``` ```(** Converts a formula to negation normal form ``` ``` by "pushing in" the negations "~". ``` ``` The symbols "<=>" and "=>" are substituted by their usual definitions. ``` ``` @param f A formula. ``` ``` @return A formula in negation normal form and not containing "<=>" or "=>" ``` ``` that is equivalent to f. ``` ``` *) ``` ```and nnf f = ``` ``` match f with ``` ``` | TRUE ``` ``` | FALSE ``` ``` | AP _ ``` ``` | NOT (AP _) -> f ``` ``` | NOT f1 -> nnfNeg f1 ``` ``` | EX (s, i, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else EX (s, i, ft) ``` ``` | AX (s, i, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else AX (s, i, ft) ``` ``` | MIN (n, s, i, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else MIN (n, s, i, ft) ``` ``` | MAX (n, s, i, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else MAX (n, s, i, ft) ``` ``` | EQU (f1, f2) -> AND (OR (nnfNeg f1, nnf f2), OR (nnfNeg f2, nnf f1)) ``` ``` | IMP (f1, f2) -> OR (nnfNeg f1, nnf f2) ``` ``` | OR (f1, f2) -> ``` ``` let ft1 = nnf f1 in ``` ``` let ft2 = nnf f2 in ``` ``` if ft1 == f1 && ft2 == f2 then f else OR (ft1, ft2) ``` ``` | AND (f1, f2) -> ``` ``` let ft1 = nnf f1 in ``` ``` let ft2 = nnf f2 in ``` ``` if ft1 == f1 && ft2 == f2 then f else AND (ft1, ft2) ``` ```(** Checks whether a formula contains inverse roles. ``` ``` @param f A formula. ``` ``` @return True iff f contains some inverse roles. ``` ``` *) ``` ```let rec containsInverse f = ``` ``` match f with ``` ``` | TRUE ``` ``` | FALSE ``` ``` | AP _ -> false ``` ``` | NOT f1 -> containsInverse f1 ``` ``` | EX (_, i, f1) ``` ``` | AX (_, i, f1) ``` ``` | MIN (_, _, i, f1) ``` ``` | MAX (_, _, i, f1) -> i || containsInverse f1 ``` ``` | EQU (f1, f2) ``` ``` | IMP (f1, f2) ``` ``` | OR (f1, f2) ``` ``` | AND (f1, f2) -> containsInverse f1 || containsInverse f2 ``` ```(** Simplifies a formula that is in negation normal form. ``` ``` @param f A formula in negation normal form. ``` ``` @return A formula in negation normal form that is equivalent to f. ``` ``` @raise ALCException if f is not in negation normal form. ``` ``` *) ``` ```let rec simplifyFormula f = ``` ``` match f with ``` ``` | TRUE ``` ``` | FALSE ``` ``` | AP _ ``` ``` | NOT (AP _) -> f ``` ``` | EX (s, i, f1) -> ``` ``` let ft = simplifyFormula f1 in ``` ``` begin ``` ``` match ft with ``` ``` | FALSE -> FALSE ``` ``` | _ -> if ft == f1 then f else EX (s, i, ft) ``` ``` end ``` ``` | AX (s, i, f1) -> ``` ``` let ft = simplifyFormula f1 in ``` ``` begin ``` ``` match ft with ``` ``` | TRUE -> TRUE ``` ``` | _ -> if ft == f1 then f else AX (s, i, ft) ``` ``` end ``` ``` | MIN (n, s, i, f1) -> ``` ``` if n = 0 then TRUE ``` ``` else ``` ``` let ft = simplifyFormula f1 in ``` ``` begin ``` ``` match ft with ``` ``` | FALSE -> FALSE ``` ``` | _ -> if ft == f1 then f else MIN (n, s, i, ft) ``` ``` end ``` ``` | MAX (n, s, i, f1) -> ``` ``` let ft = simplifyFormula f1 in ``` ``` begin ``` ``` match ft with ``` ``` | FALSE -> TRUE ``` ``` | _ -> if ft == f1 then f else MAX (n, s, i, ft) ``` ``` end ``` ``` | OR (f1, f2) -> ``` ``` let ft1 = simplifyFormula f1 in ``` ``` let ft2 = simplifyFormula f2 in ``` ``` begin ``` ``` match ft1, ft2 with ``` ``` | TRUE, _ -> TRUE ``` ``` | FALSE, _ -> ft2 ``` ``` | _, TRUE -> TRUE ``` ``` | _, FALSE -> ft1 ``` ``` | _, _ -> ``` ``` if (f1 == ft1) && (f2 == ft2) then f ``` ``` else OR (ft1, ft2) ``` ``` end ``` ``` | AND (f1, f2) -> ``` ``` let ft1 = simplifyFormula f1 in ``` ``` let ft2 = simplifyFormula f2 in ``` ``` begin ``` ``` match ft1, ft2 with ``` ``` | TRUE, _ -> ft2 ``` ``` | FALSE, _ -> FALSE ``` ``` | _, TRUE -> ft1 ``` ``` | _, FALSE -> FALSE ``` ``` | _, _ -> ``` ``` if (f1 == ft1) && (f2 == ft2) then f ``` ``` else AND (ft1, ft2) ``` ``` end ``` ``` | _ -> raise (ALCException "Formula is not in negation normal form.") ``` ```(** Destructs an atomic proposition. ``` ``` @param f An atomic proposition. ``` ``` @return The name of the atomic proposition. ``` ``` @raise ALCException if f is not an atomic proposition. ``` ``` *) ``` ```let dest_ap f = ``` ``` match f with ``` ``` | AP s -> s ``` ``` | _ -> raise (ALCException "Formula is not an atomic proposition.") ``` ```(** Destructs a negation. ``` ``` @param f A negation. ``` ``` @return The immediate subformula of the negation. ``` ``` @raise ALCException if f is not a negation. ``` ``` *) ``` ```let dest_not f = ``` ``` match f with ``` ``` | NOT f1 -> f1 ``` ``` | _ -> raise (ALCException "Formula is not a negation.") ``` ```(** Destructs an EX-formula. ``` ``` @param f An EX-formula. ``` ``` @return The role name, whether it is an inverse role, ``` ``` and the immediate subformula of the EX-formula. ``` ``` @raise ALCException if f is not an EX-formula. ``` ``` *) ``` ```let dest_ex f = ``` ``` match f with ``` ``` | EX (s, i, f1) -> (s, i, f1) ``` ``` | _ -> raise (ALCException "Formula is not an EX-formula.") ``` ```(** Destructs an AX-formula. ``` ``` @param f An AX-formula. ``` ``` @return The role name, whether it is an inverse role, ``` ``` and the immediate subformula of the AX-formula. ``` ``` @raise ALCException if f is not an AX-formula. ``` ``` *) ``` ```let dest_ax f = ``` ``` match f with ``` ``` | AX (s, i, f1) -> (s, i, f1) ``` ``` | _ -> raise (ALCException "Formula is not an AX-formula.") ``` ```(** Destructs a MIN-formula. ``` ``` @param f A MIN-formula. ``` ``` @return The number restriction, role name, whether it is an inverse role, ``` ``` and the immediate subformula of the MIN-formula. ``` ``` @raise ALCException if f is not a MIN-formula. ``` ``` *) ``` ```let dest_min f = ``` ``` match f with ``` ``` | MIN (n, s, i, f1) -> (n, s, i, f1) ``` ``` | _ -> raise (ALCException "Formula is not a MIN-formula.") ``` ```(** Destructs a MAX-formula. ``` ``` @param f A MAX-formula. ``` ``` @return The number restriction, role name, whether it is an inverse role, ``` ``` and the immediate subformula of the MAX-formula. ``` ``` @raise ALCException if f is not a MAX-formula. ``` ``` *) ``` ```let dest_max f = ``` ``` match f with ``` ``` | MAX (n, s, i, f1) -> (n, s, i, f1) ``` ``` | _ -> raise (ALCException "Formula is not a MAX-formula.") ``` ```(** Destructs an equivalence. ``` ``` @param f An equivalence. ``` ``` @return The two immediate subformulae of the equivalence. ``` ``` @raise ALCException if f is not an equivalence. ``` ``` *) ``` ```let dest_equ f = ``` ``` match f with ``` ``` | EQU (f1, f2) -> (f1, f2) ``` ``` | _ -> raise (ALCException "Formula is not an equivalence.") ``` ```(** Destructs an implication. ``` ``` @param f An implication. ``` ``` @return The two immediate subformulae of the implication. ``` ``` @raise ALCException if f is not an implication. ``` ``` *) ``` ```let dest_imp f = ``` ``` match f with ``` ``` | IMP (f1, f2) -> (f1, f2) ``` ``` | _ -> raise (ALCException "Formula is not an implication.") ``` ```(** Destructs an or-formula. ``` ``` @param f An or-formula. ``` ``` @return The two immediate subformulae of the or-formula. ``` ``` @raise ALCException if f is not an or-formula. ``` ``` *) ``` ```let dest_or f = ``` ``` match f with ``` ``` | OR (f1, f2) -> (f1, f2) ``` ``` | _ -> raise (ALCException "Formula is not an or-formula.") ``` ```(** Destructs an and-formula. ``` ``` @param f An and-formula. ``` ``` @return The two immediate subformulae of the and-formula. ``` ``` @raise ALCException if f is not an and-formula. ``` ``` *) ``` ```let dest_and f = ``` ``` match f with ``` ``` | AND (f1, f2) -> (f1, f2) ``` ``` | _ -> raise (ALCException "Formula is not an and-formula.") ``` ```(** Tests whether a formula is the constant True. ``` ``` @param f A formula. ``` ``` @return True iff f is the constant True. ``` ``` *) ``` ```let is_true f = ``` ``` match f with ``` ``` | TRUE -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is the constant False. ``` ``` @param f A formula. ``` ``` @return True iff f is the constant False. ``` ``` *) ``` ```let is_false f = ``` ``` match f with ``` ``` | FALSE -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is an atomic proposition. ``` ``` @param f A formula. ``` ``` @return True iff f is an atomic proposition. ``` ``` *) ``` ```let is_ap f = ``` ``` match f with ``` ``` | AP _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is a negation. ``` ``` @param f A formula. ``` ``` @return True iff f is a negation. ``` ``` *) ``` ```let is_not f = ``` ``` match f with ``` ``` | NOT _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is an EX-formula. ``` ``` @param f A formula. ``` ``` @return True iff f is an EX-formula. ``` ``` *) ``` ```let is_ex f = ``` ``` match f with ``` ``` | EX _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is an AX-formula. ``` ``` @param f A formula. ``` ``` @return True iff f is an AX-formula. ``` ``` *) ``` ```let is_ax f = ``` ``` match f with ``` ``` | AX _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is a MIN-formula. ``` ``` @param f A formula. ``` ``` @return True iff f is a MIN-formula. ``` ``` *) ``` ```let is_min f = ``` ``` match f with ``` ``` | MIN _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is a MAX-formula. ``` ``` @param f A formula. ``` ``` @return True iff f is a MAX-formula. ``` ``` *) ``` ```let is_max f = ``` ``` match f with ``` ``` | MAX _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is an equivalence. ``` ``` @param f A formula. ``` ``` @return True iff f is an equivalence. ``` ``` *) ``` ```let is_equ f = ``` ``` match f with ``` ``` | EQU _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is an implication. ``` ``` @param f A formula. ``` ``` @return True iff f is an implication. ``` ``` *) ``` ```let is_imp f = ``` ``` match f with ``` ``` | IMP _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is an or-formula. ``` ``` @param f A formula. ``` ``` @return True iff f is an or-formula. ``` ``` *) ``` ```let is_or f = ``` ``` match f with ``` ``` | OR _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is an and-formula. ``` ``` @param f A formula. ``` ``` @return True iff f is an and-formula. ``` ``` *) ``` ```let is_and f = ``` ``` match f with ``` ``` | AND _ -> true ``` ``` | _ -> false ``` ``` ``` ```(** The constant True. ``` ``` *) ``` ```let const_true = TRUE ``` ```(** The constant False. ``` ``` *) ``` ```let const_false = FALSE ``` ``` ``` ```(** Constructs an atomic proposition. ``` ``` @param s The name of the atomic proposition. ``` ``` @return The atomic proposition with name s. ``` ``` *) ``` ```let const_ap s = AP s ``` ```(** Negates a formula. ``` ``` @param f A formula. ``` ``` @return The negation of f. ``` ``` *) ``` ```let const_not f = NOT f ``` ```(** Constructs an EX-formula from a formula. ``` ``` @param s A role name. ``` ``` @param i True if it is an inverse role, false otherwise. ``` ``` @param f A formula. ``` ``` @return The formula EX f. ``` ``` *) ``` ```let const_ex s i f = EX (s, i, f) ``` ```(** Constructs an AX-formula from a formula. ``` ``` @param s A role name. ``` ``` @param i True if it is an inverse role, false otherwise. ``` ``` @param f A formula. ``` ``` @return The formula AX f. ``` ``` *) ``` ```let const_ax s i f = AX (s, i, f) ``` ```(** Constructs a MIN-formula from a formula. ``` ``` @param n A non-negative integer. ``` ``` @param s A role name. ``` ``` @param i True if it is an inverse role, false otherwise. ``` ``` @param f A formula. ``` ``` @return The formula MIN f. ``` ``` @raise ALCException Iff n is negative. ``` ``` *) ``` ```let const_min n s i f = ``` ``` if n < 0 then raise (ALCException "Negative cardinality constraint.") ``` ``` else MIN (n, s, i, f) ``` ```(** Constructs a MAX-formula from a formula. ``` ``` @param n A non-negative integer. ``` ``` @param s A role name. ``` ``` @param i True if it is an inverse role, false otherwise. ``` ``` @param f A formula. ``` ``` @return The formula MAX f. ``` ``` @raise ALCException Iff n is negative. ``` ``` *) ``` ```let const_max n s i f = ``` ``` if n < 0 then raise (ALCException "Negative cardinality constraint.") ``` ``` else MAX (n, s, i, f) ``` ```(** Constructs an equivalence from two formulae. ``` ``` @param f1 The first formula (LHS). ``` ``` @param f2 The second formula (LHS). ``` ``` @return The equivalence f1 <=> f2. ``` ``` *) ``` ```let const_equ f1 f2 = EQU (f1, f2) ``` ```(** Constructs an implication from two formulae. ``` ``` @param f1 The first formula (LHS). ``` ``` @param f2 The second formula (LHS). ``` ``` @return The implication f1 => f2. ``` ``` *) ``` ```let const_imp f1 f2 = IMP (f1, f2) ``` ```(** Constructs an or-formula from two formulae. ``` ``` @param f1 The first formula (LHS). ``` ``` @param f2 The second formula (LHS). ``` ``` @return The formula f1 | f2. ``` ``` *) ``` ```let const_or f1 f2 = OR (f1, f2) ``` ```(** Constructs an and-formula from two formulae. ``` ``` @param f1 The first formula (LHS). ``` ``` @param f2 The second formula (LHS). ``` ``` @return The formula f1 & f2. ``` ``` *) ``` ```let const_and f1 f2 = AND (f1, f2) ``` ```(** Calculates all formulae ``` ``` that may be created in the tableau procedure (i.e. a kind of Fischer-Ladner closure). ``` ``` @param compF A function that compares formulae. ``` ``` @param f The initial formula of the tableau procedure ``` ``` which must be in negation normal form. ``` ``` @return A list containing all formulae of the closure in increasing order. ``` ``` @raise ALCException if f is not in negation normal form. ``` ``` *) ``` ```let detClosure compF f = ``` ``` let module TSet = Set.Make( ``` ``` struct ``` ``` type t = formula ``` ``` let (compare : t -> t -> int) = compF ``` ``` end ``` ``` ) ``` ``` in ``` ``` let rec detC fs f = ``` ``` if TSet.mem f fs then fs ``` ``` else ``` ``` let nfs = TSet.add f fs in ``` ``` match f with ``` ``` | TRUE ``` ``` | FALSE -> nfs ``` ``` | AP _ -> TSet.add (NOT f) nfs ``` ``` | NOT (AP s) -> TSet.add (AP s) nfs ``` ``` | EX (_, _, f1) ``` ``` | AX (_, _, f1) -> detC nfs f1 ``` ``` | OR (f1, f2) ``` ``` | AND (f1, f2) -> ``` ``` let nfs = detC nfs f1 in ``` ``` detC nfs f2 ``` ``` | _ -> raise (ALCException "Formula is not in negation normal form.") ``` ``` in ``` ``` let tset = TSet.empty in ``` ``` let tset = TSet.add TRUE tset in ``` ``` let tset = TSet.add FALSE tset in ``` ``` let rset = detC tset f in ``` ``` TSet.elements rset ``` ```(** Hash-consed formulae, which are in negation normal form, ``` ``` such that structural and physical equality coincide. ``` ``` *) ``` ```type hcFormula = (hcFormula_node, formula) HC.hash_consed ``` ```and hcFormula_node = ``` ``` | HCTRUE ``` ``` | HCFALSE ``` ``` | HCAP of string ``` ``` | HCNOT of string ``` ``` | HCEX of string * bool * hcFormula ``` ``` | HCAX of string * bool * hcFormula ``` ``` | HCOR of hcFormula * hcFormula ``` ``` | HCAND of hcFormula * hcFormula ``` ```(** Determines whether two formula nodes are structurally equal. ``` ``` @param f1 The first formula node. ``` ``` @param f2 The second formula node. ``` ``` @return True iff f1 and f2 are structurally equal. ``` ``` *) ``` ```let equal_hcFormula_node f1 f2 = ``` ``` match f1, f2 with ``` ``` | HCTRUE, HCTRUE -> true ``` ``` | HCFALSE, HCFALSE -> true ``` ``` | HCAP s1, HCAP s2 ``` ``` | HCNOT s1, HCNOT s2 -> compare s1 s2 = 0 ``` ``` | HCEX (s1, i1, f1), HCEX (s2, i2, f2) ``` ``` | HCAX (s1, i1, f1), HCAX (s2, i2, f2) -> compare s1 s2 = 0 && i1 = i2 && f1 == f2 ``` ``` | HCOR (f1a, f1b), HCOR (f2a, f2b) ``` ``` | HCAND (f1a, f1b), HCAND (f2a, f2b) -> f1a == f2a && f1b == f2b ``` ``` | _ -> false ``` ```(** Computes the hash value of a formula node. ``` ``` @param f A formula node. ``` ``` @return The hash value of f. ``` ``` *) ``` ```let hash_hcFormula_node f = ``` ``` match f with ``` ``` | HCTRUE -> 0 ``` ``` | HCFALSE -> 1 ``` ``` | HCAP s -> Hashtbl.hash s ``` ``` | HCNOT s -> Hashtbl.hash s + 1 ``` ``` | HCEX (s, i, f1) -> 19 * (19 * (Hashtbl.hash s) + (if i then 1 else 0) + f1.HC.hkey) + 3 ``` ``` | HCAX (s, i, f1) -> 19 * (19 * (Hashtbl.hash s) + (if i then 1 else 0) + f1.HC.hkey) + 4 ``` ``` | HCOR (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 5 ``` ``` | HCAND (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 6 ``` ```(** Determines the "real" formula of a formula node. ``` ``` @param f A formula node. ``` ``` @return The formula (in negation normal form) which corresponds to f. ``` ``` *) ``` ```let toFml_hcFormula_node f = ``` ``` match f with ``` ``` | HCTRUE -> TRUE ``` ``` | HCFALSE -> FALSE ``` ``` | HCAP s -> AP s ``` ``` | HCNOT s -> NOT (AP s) ``` ``` | HCEX (s, i, f1) -> EX (s, i, f1.HC.fml) ``` ``` | HCAX (s, i, f1) -> AX (s, i, f1.HC.fml) ``` ``` | HCOR (f1, f2) -> ``` ``` let fml1 = f1.HC.fml in ``` ``` let fml2 = f2.HC.fml in ``` ``` OR (fml1, fml2) ``` ``` | HCAND (f1, f2) -> ``` ``` let fml1 = f1.HC.fml in ``` ``` let fml2 = f2.HC.fml in ``` ``` AND (fml1, fml2) ``` ```(** Determines the negation (in negation normal form) of a formula node. ``` ``` @param f A formula node. ``` ``` @return The negation (in negation normal form) of f. ``` ``` *) ``` ```let negNde_hcFormula_node f = ``` ``` match f with ``` ``` | HCTRUE -> HCFALSE ``` ``` | HCFALSE -> HCTRUE ``` ``` | HCAP s -> HCNOT s ``` ``` | HCNOT s -> HCAP s ``` ``` | HCEX (s, i, f2) -> HCAX (s, i, f2.HC.neg) ``` ``` | HCAX (s, i, f2) -> HCEX (s, i, f2.HC.neg) ``` ``` | HCOR (f1, f2) -> ``` ``` let notf1 = f1.HC.neg in ``` ``` let notf2 = f2.HC.neg in ``` ``` HCAND (notf1, notf2) ``` ``` | HCAND (f1, f2) -> ``` ``` let notf1 = f1.HC.neg in ``` ``` let notf2 = f2.HC.neg in ``` ``` HCOR (notf1, notf2) ``` ```(** An instantiation of hash-consing for formulae. ``` ``` *) ``` ```module HcFormula = HC.Make( ``` ``` struct ``` ``` type nde = hcFormula_node ``` ``` type fml = formula ``` ``` let equal (n1 : nde) n2 = equal_hcFormula_node n1 n2 ``` ``` let hash (n : nde) = hash_hcFormula_node n ``` ``` let negNde (n : nde) = negNde_hcFormula_node n ``` ``` let toFml (n : nde) = toFml_hcFormula_node n ``` ``` end ``` ``` ) ``` ```(** An instantiation of a hash table (of the standard library) ``` ``` for hash-consed formulae. The test for equality ``` ``` and computing the hash value is done in constant time. ``` ``` *) ``` ```module HcFHt = Hashtbl.Make( ``` ``` struct ``` ``` type t = hcFormula ``` ``` let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag ``` ``` let hash (f : t) = f.HC.tag ``` ``` end ``` ``` ) ``` ```(** Converts a formula into its hash-consed version. ``` ``` @param hcF A hash-cons table for formulae. ``` ``` @param f A formula in negation normal form. ``` ``` @return The hash-consed version of f. ``` ``` @raise ALCException if f is not in negation normal form. ``` ```*) ``` ```let rec hc_formula hcF f = ``` ``` match f with ``` ``` | TRUE -> HcFormula.hashcons hcF HCTRUE ``` ``` | FALSE -> HcFormula.hashcons hcF HCFALSE ``` ``` | AP s -> HcFormula.hashcons hcF (HCAP s) ``` ``` | NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s) ``` ``` | EX (s, i, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCEX (s, i, tf1)) ``` ``` | AX (s, i, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCAX (s, i, tf1)) ``` ``` | OR (f1, f2) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` let tf2 = hc_formula hcF f2 in ``` ``` HcFormula.hashcons hcF (HCOR (tf1, tf2)) ``` ``` | AND (f1, f2) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` let tf2 = hc_formula hcF f2 in ``` ``` HcFormula.hashcons hcF (HCAND (tf1, tf2)) ``` ``` | _ -> raise (ALCException "Formula is not in negation normal form.") ``` ```(** Calculates all formulae ``` ``` which may be created in the tableau procedure (i.e. a kind of Fischer-Ladner closure). ``` ``` @param hcF A hash-cons table for formulae. ``` ``` @param hcnnf The initial formula of the tableau procedure as hash-consed version. ``` ``` (which is in negation normal form). ``` ``` @return A list containing all hash-consed formulae of the closure (in arbitrary order). ``` ``` @raise ALCException if nnf is not in negation normal form. ``` ``` *) ``` ```let detClosureHc hcF hcnnf = ``` ``` let hcFht = HcFHt.create 100 in ``` ``` HcFHt.add hcFht (HcFormula.hashcons hcF HCTRUE) (); ``` ``` HcFHt.add hcFht (HcFormula.hashcons hcF HCFALSE) (); ``` ``` let rec detC f = ``` ``` if HcFHt.mem hcFht f then () ``` ``` else begin ``` ``` HcFHt.add hcFht f (); ``` ``` match f.HC.node with ``` ``` | HCTRUE ``` ``` | HCFALSE ``` ``` | HCAP _ ``` ``` | HCNOT _ -> () ``` ``` | HCOR (f1, f2) ``` ``` | HCAND (f1, f2) -> ``` ``` detC f1; ``` ``` detC f2 ``` ``` | HCEX (_, _, f1) ``` ``` | HCAX (_, _, f1) -> detC f1 ``` ``` end ``` ``` in ``` ``` detC hcnnf; ``` ``` let flist = HcFHt.fold (fun f () acc -> f::acc) hcFht [] in ``` ``` flist ``` ```(** Converts a formula into a string representation for alc-tableau. ``` ``` @param f A formula with no inverse roles. ``` ``` @return A string representing f for alc-tableau. ``` ``` @raise ALCException If f contains number restrictions or inverse roles, or ``` ``` if the name of an atomic program ``` ``` or a propositional variable in f is "tt" or "ff". ``` ``` *) ``` ```let exportFormulaAlcTableau f = ``` ``` let size = sizeFormula f in ``` ``` let sb = Buffer.create (2 * size) in ``` ``` let rec expF = function ``` ``` | TRUE -> Buffer.add_string sb "tt" ``` ``` | FALSE -> Buffer.add_string sb "ff" ``` ``` | AP s -> ``` ``` if s <> "tt" && s <> "ff" then Buffer.add_string sb s ``` ``` else raise (ALCException "Formula contains \"tt\" or \"ff\".") ``` ``` | NOT f1 -> ``` ``` Buffer.add_string sb "not("; ``` ``` expF f1; ``` ``` Buffer.add_string sb ")" ``` ``` | EX (s1, i1, f1) -> ``` ``` if i1 then raise (ALCException "Formula contains inverse roles.") ``` ``` else begin ``` ``` Buffer.add_string sb "some("; ``` ``` Buffer.add_string sb s1; ``` ``` Buffer.add_string sb ","; ``` ``` expF f1; ``` ``` Buffer.add_string sb ")" ``` ``` end ``` ``` | AX (s1, i1, f1) -> ``` ``` if i1 then raise (ALCException "Formula contains inverse roles.") ``` ``` else begin ``` ``` Buffer.add_string sb "all("; ``` ``` Buffer.add_string sb s1; ``` ``` Buffer.add_string sb ","; ``` ``` expF f1; ``` ``` Buffer.add_string sb ")" ``` ``` end ``` ``` | MIN _ ``` ``` | MAX _ -> raise (ALCException "Formula contains number restrictions.") ``` ``` | EQU (f1, f2) -> ``` ``` Buffer.add_string sb "equiv("; ``` ``` expF f1; ``` ``` Buffer.add_string sb ","; ``` ``` expF f2; ``` ``` Buffer.add_string sb ")" ``` ``` | IMP (f1, f2) -> ``` ``` Buffer.add_string sb "implies("; ``` ``` expF f1; ``` ``` Buffer.add_string sb ","; ``` ``` expF f2; ``` ``` Buffer.add_string sb ")" ``` ``` | OR (f1, f2) -> ``` ``` Buffer.add_string sb "disj("; ``` ``` expF f1; ``` ``` Buffer.add_string sb ","; ``` ``` expF f2; ``` ``` Buffer.add_string sb ")" ``` ``` | AND (f1, f2) -> ``` ``` Buffer.add_string sb "conj("; ``` ``` expF f1; ``` ``` Buffer.add_string sb ","; ``` ``` expF f2; ``` ``` Buffer.add_string sb ")" ``` ``` in ``` ``` expF f; ``` ``` Buffer.contents sb ``` ```(** Creates a file representing a TBox in FaCT++ format. ``` ``` The satisfiability query is the definition ``` ``` of the special concept name "SAT". ``` ``` @param The name of the output file. ``` ``` @param fl A list of formulae which are to be tested for joint satisfiability. ``` ``` @param tboxND A list of formulae representing ``` ``` the non-definitional part of a TBox. ``` ``` @param tboxD A list of definitions ``` ``` representing the definitional part of a TBox. ``` ``` The definitions must not be cyclic ``` ``` and each concept must not be defined more than once. ``` ``` *) ``` ```let createFactTBox filename fl tboxND tboxD = ``` ``` assert (fl <> []); ``` ``` let file = open_out filename in ``` ``` let ps s = output_string file s in ``` ``` let rec printFormula = function ``` ``` | TRUE -> ps "*TOP*" ``` ``` | FALSE -> ps "*BOTTOM*" ``` ``` | AP s -> ps s ``` ``` | NOT f1 -> ``` ``` ps "(not "; ``` ``` printFormula f1; ``` ``` ps ")" ``` ``` | EX (s, i1, f1) -> ``` ``` ps ("(some " ^ (if i1 then "(inv r" ^ s ^ ") " else "r" ^ s ^ " ")); ``` ``` printFormula f1; ``` ``` ps ")" ``` ``` | AX (s, i1, f1) -> ``` ``` ps ("(all " ^ (if i1 then "(inv r" ^ s ^ ") " else "r" ^ s ^ " ")); ``` ``` printFormula f1; ``` ``` ps ")" ``` ``` | MIN (n, s, i1, f1) -> ``` ``` ps ("(min " ^ (string_of_int n) ^ (if i1 then " (inv r" ^ s ^ ") " else " r" ^ s ^ " ")); ``` ``` printFormula f1; ``` ``` ps ")" ``` ``` | MAX (n, s, i1, f1) -> ``` ``` ps ("(max " ^ (string_of_int n) ^ (if i1 then " (inv r" ^ s ^ ") " else " r" ^ s ^ " ")); ``` ``` printFormula f1; ``` ``` ps ")" ``` ``` | EQU (f1, f2) -> printFormula (AND (OR (NOT f1, f2), OR (NOT f2, f1))) ``` ``` | IMP (f1, f2) -> printFormula (OR (NOT f1, f2)) ``` ``` | OR (f1, f2) -> ``` ``` ps "(or "; ``` ``` printFormula f1; ``` ``` ps " "; ``` ``` printFormula f2; ``` ``` ps ")" ``` ``` | AND (f1, f2) -> ``` ``` ps "(and "; ``` ``` printFormula f1; ``` ``` ps " "; ``` ``` printFormula f2; ``` ``` ps ")" ``` ``` in ``` ``` let printTBoxD = function ``` ``` | PRIMITIVE (s, f) -> ``` ``` ps ("(implies_c " ^ s ^ " "); ``` ``` printFormula f; ``` ``` ps ")\n" ``` ``` | NECANDSUFF (s, f) -> ``` ``` ps ("(equal_c " ^ s ^ " "); ``` ``` printFormula f; ``` ``` ps ")\n" ``` ``` in ``` ``` let f = List.fold_left (fun res f -> AND (res, f)) (List.hd fl) (List.tl fl) in ``` ``` let printTBoxND f = ``` ``` ps "(implies_c *TOP* "; ``` ``` printFormula f; ``` ``` ps ")\n" ``` ``` in ``` ``` List.iter printTBoxD tboxD; ``` ``` List.iter printTBoxND tboxND; ``` ``` ps "(equal_c SAT "; ``` ``` printFormula f; ``` ``` ps ")\n"; ``` ``` close_out file ``` ```(** Determines all propositional variables and roles ``` ``` occurring in a list of formulae. ``` ``` @param fl A list of formulae. ``` ``` @return A list containing all propositional variables in fl ``` ``` and a list containing all roles occurring in fl. ``` ``` *) ``` ```let detVars fl = ``` ``` let module PSet = Set.Make(String) in ``` ``` let rec detPR ((ps, rs) as pr) = function ``` ``` | TRUE ``` ``` | FALSE -> pr ``` ``` | AP s -> (PSet.add s ps, rs) ``` ``` | NOT f1 -> detPR pr f1 ``` ``` | EX (s, _, f1) ``` ``` | AX (s, _, f1) ``` ``` | MIN (_, s, _, f1) ``` ``` | MAX (_, s, _, f1) -> detPR (ps, PSet.add s rs) f1 ``` ``` | EQU (f1, f2) ``` ``` | IMP (f1, f2) ``` ``` | OR (f1, f2) ``` ``` | AND (f1, f2) -> ``` ``` let npr = detPR pr f1 in ``` ``` detPR npr f2 ``` ``` in ``` ``` let (pset, rset) = List.fold_left (fun acc f -> detPR acc f) (PSet.empty, PSet.empty) fl in ``` ``` (PSet.elements pset, PSet.elements rset) ``` ```(** Creates a file representing a formula for Will's prover. ``` ``` @param The name of the output file. ``` ``` @param f A formula which must not contain inverse roles and ``` ``` must not contain more than one role. ``` ``` @raise ALCException If f contains inverse roles or more than one role. ``` ``` *) ``` ```let createWill filename f = ``` ``` if containsInverse f then raise (ALCException "Formula contains inverse roles.") else (); ``` ``` let (_, pl) = detVars [f] in ``` ``` if List.length pl > 1 then raise (ALCException "Formula contains more than one role.") else (); ``` ``` let file = open_out filename in ``` ``` let ps s = output_string file s in ``` ``` let isProperName s = ``` ``` let len = String.length s in ``` ``` let rec isNumber i = ``` ``` if i <= 0 then true ``` ``` else ``` ``` let c = Char.code s.[i] in ``` ``` c >= Char.code '0' && c <= Char.code '9' && isNumber (i-1) ``` ``` in ``` ``` len >= 2 && s.[0] = 'p' && isNumber (len-1) ``` ``` in ``` ``` let rec printFormula = function ``` ``` | TRUE -> printFormula (NOT FALSE) ``` ``` | FALSE -> ``` ``` (* prerr_endline "Will's prover does not support constants true/false natively"; *) ``` ``` printFormula (AND (AP "p0", NOT (AP "p0"))) ``` ``` | AP s -> ``` ``` if isProperName s then ps s ``` ``` else raise (ALCException "Propositional variables have to be of the form p0, p1, etc.") ``` ``` | NOT f1 -> ``` ``` ps "(~ "; ``` ``` printFormula f1; ``` ``` ps ")" ``` ``` | EX (_, _, f1) -> ``` ``` ps ("(<0> "); ``` ``` printFormula f1; ``` ``` ps ")" ``` ``` | AX (s, i1, f1) -> printFormula (NOT (EX (s, i1, NOT f1))) ``` ``` | MIN (n, _, _, f1) -> ``` ``` if n = 0 then printFormula TRUE ``` ``` else begin ``` ``` ps ("(<" ^ (string_of_int (n-1)) ^ "> "); ``` ``` printFormula f1; ``` ``` ps ")" ``` ``` end ``` ``` | MAX (n, s, i1, f1) -> printFormula (NOT (MIN (n+1, s, i1, f1))) ``` ``` | EQU (f1, f2) -> printFormula (AND (OR (NOT f1, f2), OR (NOT f2, f1))) ``` ``` | IMP (f1, f2) -> printFormula (OR (NOT f1, f2)) ``` ``` | OR (f1, f2) -> ``` ``` ps "("; ``` ``` printFormula f1; ``` ``` ps " v "; ``` ``` printFormula f2; ``` ``` ps ")" ``` ``` | AND (f1, f2) -> ``` ``` ps "("; ``` ``` printFormula f1; ``` ``` ps " & "; ``` ``` printFormula f2; ``` ``` ps ")" ``` ``` in ``` ``` ps "Logic: GML\n"; ``` ``` printFormula f; ``` ``` close_out file ``` ```(** Creates a file representing a TBox in OWL format. ``` ``` The satisfiability query is added as an anonymous assertion (ABox constraint). ``` ``` @param The name of the output file. ``` ``` @param fl A list of formulae which are to be tested for joint satisfiability. ``` ``` @param tboxND A list of formulae representing ``` ``` the non-definitional part of a TBox. ``` ``` @param tboxD A list of definitions ``` ``` representing the definitional part of a TBox. ``` ``` The definitions must not be cyclic ``` ``` and each concept must not be defined more than once. ``` ``` *) ``` ```let createOWL filename fl tboxND tboxD = ``` ``` assert (fl <> []); ``` ``` let file = open_out filename in ``` ``` let addTBoxD acc = function ``` ``` | PRIMITIVE (s, f) ``` ``` | NECANDSUFF (s, f) -> (AP s)::(f::acc) ``` ``` in ``` ``` let f = List.fold_left (fun res f -> AND (res, f)) (List.hd fl) (List.tl fl) in ``` ``` let tfl = List.fold_left addTBoxD (f :: tboxND) tboxD in ``` ``` let (pl,rl) = detVars tfl in ``` ``` let ps n s = ``` ``` for i = 1 to n do ``` ``` output_string file " " ``` ``` done; ``` ``` output_string file s ``` ``` in ``` ``` let rec exall n c s i f popt = ``` ``` ps n "\n"; ``` ``` ps (n+1) "\n"; ``` ``` if i then begin ``` ``` ps (n+2) "\n"; ``` ``` ps (n+3) ("\n"); ``` ``` ps (n+2) "\n" ``` ``` end ``` ``` else ps (n+2) ("\n"); ``` ``` ps (n+1) "\n"; ``` ``` let _ = ``` ``` match popt with ``` ``` | None -> () ``` ``` | Some (c2, no) -> ``` ``` ps (n+1) ("<" ^ c2 ^ " rdf:datatype=\"&xsd;nonNegativeInteger\">\n"); ``` ``` ps (n+2) ((string_of_int no) ^ "\n"); ``` ``` ps (n+1) ("\n") ``` ``` in ``` ``` ps (n+1) ("<" ^ c ^ ">\n"); ``` ``` printFormula (n+2) f; ``` ``` ps (n+1) ("\n"); ``` ``` ps n "\n"; ``` ``` and andor n c f1 f2 = ``` ``` ps n "\n"; ``` ``` ps (n+1) ("<" ^ c ^ " rdf:parseType=\"Collection\">\n"); ``` ``` printFormula (n+2) f1; ``` ``` printFormula (n+2) f2; ``` ``` ps (n+1) ("\n"); ``` ``` ps n "\n"; ``` ``` and printFormula n f = ``` ``` match f with ``` ``` | TRUE -> ps n "\n"; ``` ``` | FALSE -> ps n "\n"; ``` ``` | AP s -> ps n ("\n"); ``` ``` | NOT f1 -> ``` ``` ps n "\n"; ``` ``` ps (n+1) "\n"; ``` ``` printFormula (n+2) f1; ``` ``` ps (n+1) "\n"; ``` ``` ps n "\n"; ``` ``` | EQU (f1, f2) -> printFormula n (AND (OR (NOT f1, f2), OR (NOT f2, f1))) ``` ``` | IMP (f1, f2) -> printFormula n (OR (NOT f1, f2)) ``` ``` | EX (s, i1, f1) -> exall n "owl:someValuesFrom" s i1 f1 None ``` ``` | AX (s, i1, f1) -> exall n "owl:allValuesFrom" s i1 f1 None ``` ``` | MIN (card, s, i1, f1) -> ``` ``` exall n "owl:onClass" s i1 f1 (Some ("owl:minQualifiedCardinality", card)) ``` ``` | MAX (card, s, i1, f1) -> ``` ``` exall n "owl:onClass" s i1 f1 (Some ("owl:maxQualifiedCardinality", card)) ``` ``` | OR (f1, f2) -> andor n "owl:unionOf" f1 f2 ``` ``` | AND (f1, f2) -> andor n "owl:intersectionOf" f1 f2 ``` ``` in ``` ``` let printAxiom c1 c2 s f = ``` ``` ps 2 ("\n"); ``` ``` ps 3 ("<" ^ c2 ^ ">\n"); ``` ``` printFormula 4 f; ``` ``` ps 3 ("\n"); ``` ``` ps 2 "\n\n"; ``` ``` in ``` ``` let printTBoxD = function ``` ``` | PRIMITIVE (s, f) -> printAxiom "rdf:about" "rdfs:subClassOf" ("#p" ^ s) f ``` ``` | NECANDSUFF (s, f) -> printAxiom "rdf:about" "owl:equivalentClass" ("#p" ^ s) f ``` ``` in ``` ``` let printTBoxND f = printAxiom "rdf:about" "rdfs:subClassOf" "&owl;Thing" f in ``` ``` ps 0 "\n\n"; ``` ``` ps 0 "\n"; ``` ``` ps 5 "\n"; ``` ``` (* ps 5 "\n"; *) ``` ``` ps 0 "]>\n\n"; ``` ``` ps 0 "\n\n"; ``` ``` ps 2 "\n\n"; ``` ``` List.iter (fun s -> ps 2 ("\n")) pl; ``` ``` List.iter (fun s -> ps 2 ("\n")) rl; ``` ``` ps 0 "\n"; ``` ``` List.iter printTBoxD tboxD; ``` ``` List.iter printTBoxND tboxND; ``` ``` ps 0 "\n"; ``` ``` printAxiom "rdf:nodeID" "rdf:type" "_:a" f; ``` ``` ps 0 "\n"; ``` ``` close_out file ``` ```let lexerf = A.make_lexer_file ~comment:"%" ``` ``` ["(";")";".";",";"inputformula";"hypothesis";"axiom";"conjecture"; ``` ``` "-";"~";"&";"|";"=>";"pos";"box";":";"true";"false"] ``` ```(** These functions parse a TANCS token stream to obtain a formula. ``` ``` It is a standard recursive descent procedure. ``` ``` @param ts A token stream. ``` ``` @return The resulting (sub-)formula. ``` ``` @raise ALCException if ts does not represent a formula. ``` ``` *) ``` ```let rec parseTancs_equ ts = ``` ``` let f1 = parseTancs_imp ts in ``` ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "<=>") -> ``` ``` Stream.junk ts; ``` ``` let f2 = parseTancs_equ ts in ``` ``` EQU (f1, f2) ``` ``` | _ -> f1 ``` ```(** These functions parse a TANCS token stream to obtain a formula. ``` ``` It is a standard recursive descent procedure. ``` ``` @param ts A token stream. ``` ``` @return The resulting (sub-)formula. ``` ``` @raise ALCException if ts does not represent a formula. ``` ``` *) ``` ```and parseTancs_imp ts = ``` ``` let f1 = parseTancs_or ts in ``` ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "=>") -> ``` ``` Stream.junk ts; ``` ``` let f2 = parseTancs_imp ts in ``` ``` IMP (f1, f2) ``` ``` | _ -> f1 ``` ```(** These functions parse a TANCS token stream to obtain a formula. ``` ``` It is a standard recursive descent procedure. ``` ``` @param ts A token stream. ``` ``` @return The resulting (sub-)formula. ``` ``` @raise ALCException if ts does not represent a formula. ``` ``` *) ``` ```and parseTancs_or ts = ``` ``` let f1 = parseTancs_and ts in ``` ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "|") -> ``` ``` Stream.junk ts; ``` ``` let f2 = parseTancs_or ts in ``` ``` OR (f1, f2) ``` ``` | _ -> f1 ``` ```(** These functions parse a TANCS token stream to obtain a formula. ``` ``` It is a standard recursive descent procedure. ``` ``` @param ts A token stream. ``` ``` @return The resulting (sub-)formula. ``` ``` @raise ALCException if ts does not represent a formula. ``` ``` *) ``` ```and parseTancs_and ts = ``` ``` let f1 = parseTancs_rest ts in ``` ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "&") -> ``` ``` Stream.junk ts; ``` ``` let f2 = parseTancs_and ts in ``` ``` AND (f1, f2) ``` ``` | _ -> f1 ``` ```(** These functions parse a TANCS token stream to obtain a formula. ``` ``` It is a standard recursive descent procedure. ``` ``` @param ts A token stream. ``` ``` @return The resulting (sub-)formula. ``` ``` @raise ALCException if ts does not represent a formula. ``` ``` *) ``` ```and parseTancs_rest ts = ``` ``` let token = Stream.next ts in ``` ``` match token with ``` ``` | A.Kwd "pos" ``` ``` | A.Kwd "box" -> begin ``` ``` let s = ``` ``` match Stream.peek ts with ``` ``` | Some (A.Ident s1) -> Stream.junk ts; s1 ``` ``` | Some (A.Kwd ":") -> "" ``` ``` | Some (A.Kwd "-") -> "" ``` ``` | Some t -> A.printError mk_exn ~t ~ts "role name, \"-\", or \":\" expected: " ``` ``` | None -> A.printError mk_exn ~ts "role name, \"-\", or \":\" expected: " ``` ``` in ``` ``` let isInv = ``` ``` match Stream.next ts with ``` ``` | A.Kwd ":" -> false ``` ``` | A.Kwd "-" -> begin ``` ``` match Stream.next ts with ``` ``` | A.Kwd ":" -> true ``` ``` | t -> A.printError mk_exn ~t ~ts "\":\" expected: " ``` ``` end ``` ``` | t -> A.printError mk_exn ~t ~ts "\":\" or \"-\" expected: " ``` ``` in ``` ``` let f1 = parseTancs_rest ts in ``` ``` match token with ``` ``` | A.Kwd "pos" -> EX (s, isInv, f1) ``` ``` | _ -> AX (s, isInv, f1) ``` ``` end ``` ``` | A.Kwd "(" -> ``` ``` let f = parseTancs_equ ts in ``` ``` let _ = ``` ``` match Stream.next ts with ``` ``` | A.Kwd ")" -> () ``` ``` | t -> A.printError mk_exn ~t ~ts "\")\" expected: " ``` ``` in ``` ``` f ``` ``` | A.Kwd "~" -> ``` ``` let f = parseTancs_rest ts in ``` ``` NOT f ``` ``` | A.Kwd "true" -> TRUE ``` ``` | A.Kwd "false" -> FALSE ``` ``` | A.Ident s -> AP s ``` ``` | t -> A.printError mk_exn ~t ~ts ``` ``` "\"pos\", \"box\", \"~\", \"(\", \"true\", \"false\", or expected: " ``` ```(** These functions parse a TANCS token stream to obtain a set of clauses. ``` ``` It is a standard recursive descent procedure. ``` ``` @param ts A token stream. ``` ``` @param axl The axioms parsed so far. ``` ``` @param hypl The hyptheses parsed so far. ``` ``` @param conl The conjectures parsed so far. ``` ``` @return A triple (axl, hypl, conl) where ``` ``` axl is a list of formula representing axioms; ``` ``` hypl is a list of formula representing hypotheses; ``` ``` conl is a list of formula representing conjectures; ``` ``` @raise ALCException if s does not represent a set of clauses. ``` ``` *) ``` ```let rec parseTancs_clauses ts axl hypl conl = ``` ``` match Stream.peek ts with ``` ``` | Some (A.Kwd "inputformula") -> begin ``` ``` Stream.junk ts; ``` ``` A.getKws mk_exn ts ["("]; ``` ``` let _ = ``` ``` match Stream.next ts with ``` ``` | A.Ident s -> s ``` ``` | t -> A.printError mk_exn ~t "clause name expected: " ``` ``` in ``` ``` A.getKws mk_exn ts [","]; ``` ``` let ty = ``` ``` match Stream.next ts with ``` ``` | A.Kwd "axiom" -> 1 ``` ``` | A.Kwd "hypothesis" -> 2 ``` ``` | A.Kwd "conjecture" -> 3 ``` ``` | t -> A.printError mk_exn ~t ``` ``` "clause type (i.e. \"hypothesis\", \"axiom\", or \"conjecture\") expected: " ``` ``` in ``` ``` A.getKws mk_exn ts [","]; ``` ``` let cl = parseTancs_equ ts in ``` ``` A.getKws mk_exn ts [")";"."]; ``` ``` match ty with ``` ``` | 1 -> parseTancs_clauses ts (cl::axl) hypl conl ``` ``` | 2 -> parseTancs_clauses ts axl (cl::hypl) conl ``` ``` | _ -> parseTancs_clauses ts axl hypl (cl::conl) ``` ``` end ``` ``` | _ -> (axl, hypl, conl) ``` ```(** Imports queries in TAMCS2000 style. ``` ``` @param filename The name of the input file. ``` ``` @return A triple (fl, tboxND, tboxD) where ``` ``` fl is a list of formula representing the initial input; ``` ``` tboxND is a list of formulae representing ``` ``` the non-definitional part of a TBox; and ``` ``` tboxD is a list of definitions ``` ``` representing the definitional part of a TBox. ``` ``` @raise ALCException if s does not represent a formula query. ``` ``` *) ``` ```let importTancs2000 filename = ``` ``` let file = open_in filename in ``` ``` let ts = lexerf file in ``` ``` try ``` ``` begin ``` ``` let (axl, hypl, conl) = parseTancs_clauses ts [] [] [] in ``` ``` let _ = ``` ``` match Stream.peek ts with ``` ``` | None -> () ``` ``` | Some _ -> A.printError mk_exn ~ts "EOS expected: " ``` ``` in ``` ``` assert (conl <> []); ``` ``` let conc = ``` ``` List.fold_left (fun res f -> OR (res, NOT f)) (NOT (List.hd conl)) (List.tl conl) ``` ``` in ``` ``` close_in file; ``` ``` (conc::hypl, axl, []) ``` ``` end ``` ``` with Stream.Failure -> ``` ``` close_in file; ``` ` A.printError mk_exn ~ts "unexpected EOS"`