### Profile

Statistics
| Branch: | Revision:

## cool / src / lib / CoAlgFormula.ml @ 7c4d2eb4

 1 ```(** This module implements coalgebraic formulae ``` ``` (e.g. parsing, printing, (de-)constructing, ...). ``` ``` @author Florian Widmann ``` ``` *) ``` ```module HC = HashConsing ``` ```module A = AltGenlex ``` ```module L = List ``` ```module Str = String ``` ```(** A general exception for all kinds of errors ``` ``` that can happen in the tableau procedure. ``` ``` More specific information is given in the argument. ``` ``` *) ``` ```exception CoAlgException of string ``` ```(** Indicates the sort of a sorted formula ``` ``` *) ``` ```type sort = int ``` ```(** Defines (unsorted) coalgebraic formulae. ``` ``` *) ``` ```type formula = ``` ``` | TRUE ``` ``` | FALSE ``` ``` | AP of string ``` ``` | NOT of formula ``` ``` | AT of string * formula ``` ``` | OR of formula * formula ``` ``` | AND of formula * formula ``` ``` | EQU of formula * formula ``` ``` | IMP of formula * formula ``` ``` | EX of string * formula ``` ``` | AX of string * formula ``` ``` | ENFORCES of int list * formula ``` ``` | ALLOWS of int list * formula ``` ``` | MIN of int * string * formula ``` ``` | MAX of int * string * formula ``` ``` | MORETHAN of int * string * formula (* diamond of GML *) ``` ``` | MAXEXCEPT of int * string * formula (* box of GML *) ``` ``` | CHC of formula * formula ``` ``` | CHCN of formula * formula ``` ``` | FUS of bool * formula ``` ```(** Defines sorted coalgebraic formulae. ``` ``` *) ``` ```type sortedFormula = sort * formula ``` ```(** Determines whether a name indicates a nominal. ``` ``` @param A string s. ``` ``` @return True iff s contains a prime character. ``` ``` *) ``` ```let isNominal s = String.contains s '\'' ``` ```(** Determines the size of a formula. ``` ``` @param f A formula. ``` ``` @return The size of f. ``` ``` *) ``` ```let rec sizeFormula f = ``` ``` match f with ``` ``` | TRUE ``` ``` | FALSE ``` ``` | AP _ -> 1 ``` ``` | NOT f1 ``` ``` | AT (_, f1) -> succ (sizeFormula f1) ``` ``` | OR (f1, f2) ``` ``` | AND (f1, f2) ``` ``` | EQU (f1, f2) ``` ``` | IMP (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2) ``` ``` | EX (_, f1) ``` ``` | AX (_, f1) ``` ``` | ENFORCES (_, f1) ``` ``` | ALLOWS (_, f1) -> succ (sizeFormula f1) ``` ``` | MIN (_, _, f1) ``` ``` | MAX (_, _, f1) ``` ``` | MORETHAN (_, _, f1) ``` ``` | MAXEXCEPT (_, _, f1) -> succ (sizeFormula f1) ``` ``` | CHC (f1, f2) ``` ``` | CHCN (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2) ``` ``` | FUS (_, f1) -> succ (sizeFormula f1) ``` ```(** Determines the size of a sorted formula. ``` ``` @param f A sorted formula. ``` ``` @return The size of f. ``` ``` *) ``` ```let sizeSortedFormula f = sizeFormula (snd f) ``` ```(** 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 negate = function ``` ``` | NOT f -> f ``` ``` | f -> NOT f ``` ``` in ``` ``` 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 ``` ``` | AT (s, f1) -> ``` ``` Buffer.add_string sb "@ "; ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb " "; ``` ``` prio 4 f1 ``` ``` | 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 ``` ``` | 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 ``` ``` | EX (s, f1) -> ``` ``` Buffer.add_string sb "<"; ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb ">"; ``` ``` prio 4 f1 ``` ``` | AX (s, f1) -> ``` ``` Buffer.add_string sb "["; ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb "]"; ``` ``` prio 4 f1 ``` ``` | ALLOWS (s, f1) -> ``` ``` Buffer.add_string sb "<{"; ``` ``` Buffer.add_string sb ( ``` ``` match s with ``` ``` | [] -> " " ``` ``` | _ ->(Str.concat " " (L.map string_of_int s)) ``` ``` ); ``` ``` Buffer.add_string sb "}>"; ``` ``` prio 4 f1 ``` ``` | ENFORCES (s, f1) -> ``` ``` Buffer.add_string sb "[{"; ``` ``` Buffer.add_string sb ( ``` ``` match s with ``` ``` | [] -> " " ``` ``` | _ ->(Str.concat " " (L.map string_of_int s)) ``` ``` ); ``` ``` Buffer.add_string sb "}]"; ``` ``` prio 4 f1 ``` ``` | MIN (n, s, f1) -> ``` ``` Buffer.add_string sb "{>="; ``` ``` Buffer.add_string sb (string_of_int n); ``` ``` Buffer.add_string sb " "; ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb "}"; ``` ``` prio 4 f1 ``` ``` | MAX (n, s, f1) -> ``` ``` Buffer.add_string sb "{<="; ``` ``` Buffer.add_string sb (string_of_int n); ``` ``` Buffer.add_string sb " "; ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb "}"; ``` ``` prio 4 f1 ``` ``` | MORETHAN (n, s, f1) -> ``` ``` Buffer.add_string sb "{>"; ``` ``` Buffer.add_string sb (string_of_int n); ``` ``` Buffer.add_string sb " "; ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb "}"; ``` ``` prio 4 f1 ``` ``` | MAXEXCEPT (n, s, f1) -> ``` ``` Buffer.add_string sb "{<="; ``` ``` Buffer.add_string sb (string_of_int n); ``` ``` Buffer.add_string sb " ~ "; ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb "}"; ``` ``` prio 4 f1 (* actually is prio of ~ and not of <= *) ``` ``` | CHC (f1, f2) -> ``` ``` Buffer.add_string sb "("; ``` ``` exportFormula_buffer sb f1; ``` ``` Buffer.add_string sb " + "; ``` ``` exportFormula_buffer sb f2; ``` ``` Buffer.add_string sb ")" ``` ``` | CHCN (f1, f2) -> ``` ``` Buffer.add_string sb "~("; ``` ``` exportFormula_buffer sb (negate f1); ``` ``` Buffer.add_string sb " + "; ``` ``` exportFormula_buffer sb (negate f2); ``` ``` Buffer.add_string sb ")" ``` ``` | FUS (first, f1) -> ``` ``` Buffer.add_string sb (if first then "[pi1]" else "[pi2]"); ``` ``` prio 4 f1 ``` ```(** 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 sb = Buffer.create 128 in ``` ``` exportFormula_buffer sb f; ``` ``` Buffer.contents sb ``` ```(** export (CL)-formula suitable for tatl-inputs *) ``` ```let rec exportTatlFormula_buffer sb f = ``` ``` let negate = function ``` ``` | NOT f -> f ``` ``` | f -> NOT f ``` ``` in ``` ``` 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 '('; ``` ``` exportTatlFormula_buffer sb lf; ``` ``` Buffer.add_char sb ')' ``` ``` end ``` ``` else exportTatlFormula_buffer sb lf ``` ``` in ``` ``` match f with ``` ``` | TRUE -> Buffer.add_string sb "(p \\/ ~p)" ``` ``` | FALSE -> Buffer.add_string sb "(p /\\ ~p)" ``` ``` | AP s -> Buffer.add_string sb s ``` ``` | NOT f1 -> ``` ``` Buffer.add_string sb "~"; ``` ``` prio 4 f1 ``` ``` | 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 ``` ``` | EQU (f1, f2) -> ``` ``` prio 0 (AND (IMP (f1,f2), IMP (f2,f1))) ``` ``` | IMP (f1, f2) -> ``` ``` prio 2 f1; ``` ``` Buffer.add_string sb " -> "; ``` ``` prio 2 f2 ``` ``` | ALLOWS (s, f1) -> ``` ``` Buffer.add_string sb "<<"; ``` ``` Buffer.add_string sb ( ``` ``` match s with ``` ``` | [] -> " " ``` ``` | _ ->(Str.concat "," (L.map string_of_int s)) ``` ``` ); ``` ``` Buffer.add_string sb ">>X "; ``` ``` prio 4 f1 ``` ``` | ENFORCES (s, f1) -> ``` ``` Buffer.add_string sb "~<<"; ``` ``` Buffer.add_string sb ( ``` ``` match s with ``` ``` | [] -> " " ``` ``` | _ ->(Str.concat "," (L.map string_of_int s)) ``` ``` ); ``` ``` Buffer.add_string sb ">>X ~ "; ``` ``` prio 4 f1 ``` ``` | EX _ ``` ``` | AX _ ``` ``` | MIN _ ``` ``` | MAX _ ``` ``` | MORETHAN _ ``` ``` | MAXEXCEPT _ ``` ``` | AT _ ``` ``` | CHC _ ``` ``` | CHCN _ ``` ``` | FUS _ -> raise (CoAlgException ("export to tatl: Not connectives of CL")) ``` ```let exportTatlFormula f = ``` ``` let sb = Buffer.create 128 in ``` ``` exportTatlFormula_buffer sb f; ``` ``` Buffer.contents sb ``` ```(** Appends a string representation of a sorted formula to a string buffer. ``` ``` Parentheses are ommited where possible ``` ``` where the preference rules are defined as usual. ``` ``` @param sb A string buffer. ``` ``` @param (s, f) A sorted formula. ``` ``` *) ``` ```let rec exportSortedFormula_buffer sb (s, f) = ``` ``` Buffer.add_string sb (string_of_int s); ``` ``` Buffer.add_string sb ": "; ``` ``` exportFormula_buffer sb f ``` ```(** Converts a sorted formula into a string representation. ``` ``` Parentheses are ommited where possible ``` ``` where the preference rules are defined as usual. ``` ``` @param f A sorted formula. ``` ``` @return A string representing f. ``` ``` *) ``` ```let exportSortedFormula f = ``` ``` let sb = Buffer.create 128 in ``` ``` exportSortedFormula_buffer sb f; ``` ``` Buffer.contents sb ``` ```(** Converts a (sorted) formula query into a string representation. ``` ``` @param tbox A list of sorted formulae representing a TBox. ``` ``` @param f A sorted formula. ``` ``` @return A string representing tbox |- f. ``` ``` *) ``` ```let exportQuery tbox f = ``` ``` let sb = Buffer.create 1000 in ``` ``` let rec expFl = function ``` ``` | [] -> () ``` ``` | h::tl -> ``` ``` exportSortedFormula_buffer sb h; ``` ``` if tl <> [] then Buffer.add_string sb "; " else (); ``` ``` expFl tl ``` ``` in ``` ``` expFl tbox; ``` ``` Buffer.add_string sb " |- "; ``` ``` exportSortedFormula_buffer sb f; ``` ``` Buffer.contents sb ``` ```(** Converts a (sorted) formula query into a string representation. Such that ``` ``` coalg can read it again using importQuery ``` ``` @param tbox A list of sorted formulae representing a TBox. ``` ``` @param f A sorted formula. ``` ``` @return A string representing tbox |- f. ``` ``` *) ``` ```let exportQueryParsable tbox (_,f) = ``` ``` let sb = Buffer.create 1000 in ``` ``` let rec expFl = function ``` ``` | [] -> () ``` ``` | (_,h)::tl -> ``` ``` exportFormula_buffer sb h; ``` ``` if tl <> [] then Buffer.add_string sb "; " else (); ``` ``` expFl tl ``` ``` in ``` ``` expFl tbox; ``` ``` Buffer.add_string sb " |- "; ``` ``` exportFormula_buffer sb f; ``` ``` Buffer.contents sb ``` ```let lexer = A.make_lexer ``` ``` [":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]" ``` ``` ;"[{";"}]";"<{";"}>";"," ``` ``` ] ``` ```let mk_exn s = CoAlgException 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 CoAlgException if ts does not represent a formula. ``` ``` *) ``` ```let rec parse_formula ts = ``` ``` let f1 = parse_imp ts in ``` ``` match Stream.peek ts with ``` ``` | None -> f1 ``` ``` | Some (A.Kwd "<=>") -> ``` ``` Stream.junk ts; ``` ``` let f2 = parse_formula 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 CoAlgException 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 CoAlgException 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 CoAlgException 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 CoAlgException 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 -> "" ``` ``` | _ -> A.printError mk_exn ~ts ("role name or \"" ^ es ^ "\" expected: ") ``` ``` in ``` ``` let _ = ``` ``` match Stream.next ts with ``` ``` | A.Kwd c when c = es -> () ``` ``` | t -> A.printError mk_exn ~t ~ts ("\"" ^ es ^ "\" expected: ") ``` ``` in ``` ``` (n, s) ``` ``` in ``` ``` let rec agentlist es = ``` ``` let allAgents = CoolUtils.cl_get_agents () in ``` ``` match Stream.next ts with ``` ``` | A.Int n -> if CoolUtils.TArray.elem n allAgents ``` ``` then n::(agentlist es) ``` ``` else A.printError mk_exn ~ts ("agent name \"" ^ (string_of_int n) ^ "\" unknonwn, see --agents: ") ``` ``` | A.Kwd c when c = es -> [] ``` ``` | _ -> A.printError mk_exn ~ts ("agent name or " ^ es ^ "\" expected: ") ``` ``` in ``` ``` match Stream.next ts with ``` ``` | A.Kwd "True" -> TRUE ``` ``` | A.Kwd "False" -> FALSE ``` ``` | A.Ident s -> AP s ``` ``` | A.Kwd "~" -> ``` ``` let f = parse_rest ts in ``` ``` NOT f ``` ``` | A.Kwd "@" -> ``` ``` let s = ``` ``` match Stream.next ts with ``` ``` | A.Ident s when isNominal s -> s ``` ``` | t -> A.printError mk_exn ~t ~ts ("nominal expected: ") ``` ``` in ``` ``` let f = parse_rest ts in ``` ``` AT (s, f) ``` ``` | A.Kwd "<" -> ``` ``` let (_, s) = boxinternals true ">" in ``` ``` let f1 = parse_rest ts in ``` ``` EX (s, f1) ``` ``` | A.Kwd "[" -> ``` ``` let (_, s) = boxinternals true "]" in ``` ``` let f1 = parse_rest ts in ``` ``` AX (s, f1) ``` ``` | A.Kwd "[{" -> ``` ``` let ls = agentlist "}]" in ``` ``` let f1 = parse_rest ts in ``` ``` ENFORCES (ls, f1) ``` ``` | A.Kwd "<{" -> ``` ``` let ls = agentlist "}>" in ``` ``` let f1 = parse_rest ts in ``` ``` ALLOWS (ls, f1) ``` ``` | A.Kwd "{>=" -> ``` ``` let (n, s) = boxinternals false "}" in ``` ``` let f1 = parse_rest ts in ``` ``` MIN (n, s, f1) ``` ``` | A.Kwd "{<=" -> ``` ``` let (n, s) = boxinternals false "}" in ``` ``` let f1 = parse_rest ts in ``` ``` MAX (n, s, f1) ``` ``` | A.Kwd "(" -> begin ``` ``` let f = parse_formula ts in ``` ``` match Stream.next ts with ``` ``` | A.Kwd ")" -> f ``` ``` | A.Kwd "+" -> begin ``` ``` let f2 = parse_formula ts in ``` ``` match Stream.next ts with ``` ``` | A.Kwd ")" -> CHC (f, f2) ``` ``` | t -> A.printError mk_exn ~t ~ts "\")\" expected: " ``` ``` end ``` ``` | t -> A.printError mk_exn ~t ~ts "\")\" or \"+\" expected: " ``` ``` end ``` ``` | A.Kwd "[pi1]" -> ``` ``` let f = parse_rest ts in ``` ``` FUS (true, f) ``` ``` | A.Kwd "[pi2]" -> ``` ``` let f = parse_rest ts in ``` ``` FUS (false, f) ``` ``` | t -> A.printError mk_exn ~t ~ts ``` ``` "\"<\", \"[\", \"{>=\", \"{<=\", \"@\", \"~\", \"(\", \"True\", \"False\", or expected: " ``` ``` ``` ```(** Parses a sorted formula. ``` ``` @param ts A token stream. ``` ``` @return A sorted formula. ``` ``` @raise CoAlgException If ts does not represent a sorted formula. ``` ``` *) ``` ```let parse_sortedFormula ts = ``` ``` let nr = ``` ``` match Stream.peek ts with ``` ``` | Some (A.Int n) -> ``` ``` if n >= 0 then begin ``` ``` Stream.junk ts; ``` ``` let () = ``` ``` match Stream.next ts with ``` ``` | A.Kwd ":" -> () ``` ``` | t -> A.printError mk_exn ~t ~ts ("\":\" expected: ") ``` ``` in ``` ``` n ``` ``` end else ``` ``` A.printError mk_exn ~ts (" expected: ") ``` ``` | _ -> 0 ``` ``` in ``` ``` let f = parse_formula ts in ``` ``` (nr, f) ``` ```(** Parses a list of sorted formulae separated by ";". ``` ``` @param ts A token stream. ``` ``` @param acc The list of sorted formulae parsed so far. ``` ``` @return The resulting list of sorted formula. ``` ``` @raise CoAlgException if ts does not represent a list of sorted formulae. ``` ``` *) ``` ```let rec parse_sortedFormulaList ts acc = ``` ``` let f1 = parse_sortedFormula ts in ``` ``` match Stream.peek ts with ``` ``` | Some (A.Kwd ";") -> ``` ``` Stream.junk ts; ``` ``` parse_sortedFormulaList ts (f1::acc) ``` ``` | _ -> List.rev (f1::acc) ``` ```(** A common wrapper for import functions. ``` ``` @param fkt An import function. ``` ``` @param s A string. ``` ``` @return The object imported from s using fkt. ``` ``` @raise CoAlgException If ts is not empty. ``` ``` *) ``` ```let importWrapper fkt s = ``` ``` let ts = lexer s in ``` ``` try ``` ``` let res = fkt ts in ``` ``` let _ = ``` ``` match Stream.peek ts with ``` ``` | None -> () ``` ``` | Some _ -> A.printError mk_exn ~ts "EOS expected: " ``` ``` in ``` ``` res ``` ``` with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS" ``` ```(** Parses a string to obtain a formula. ``` ``` @param s A string representing a formula. ``` ``` @return The resulting formula. ``` ``` @raise CoAlgException if s does not represent a formula. ``` ``` *) ``` ```let importFormula s = importWrapper parse_formula s ``` ```(** Parses a string to obtain a sorted formula. ``` ``` @param s A string representing a sorted formula. ``` ``` @return The sorted formula. ``` ``` @raise CoAlgException If s does not represent a sorted formula. ``` ``` *) ``` ```let importSortedFormula s = importWrapper parse_sortedFormula s ``` ```(** Parses a string to obtain a (sorted) formula query. ``` ``` @param s A string representing a formula query. ``` ``` @return A pair (tbox, f) where ``` ``` tbox is a list of sorted formulae representing the TBox; and ``` ``` f is a sorted formula. ``` ``` @raise CoAlgException if s does not represent a formula query. ``` ``` *) ``` ```let importQuery s = ``` ``` let fkt ts = ``` ``` match Stream.peek ts with ``` ``` | Some (A.Kwd "|-") -> ``` ``` Stream.junk ts; ``` ``` let f = parse_sortedFormula ts in ``` ``` ([], f) ``` ``` | _ -> ``` ``` let fl = parse_sortedFormulaList ts [] in ``` ``` match Stream.peek ts with ``` ``` | Some (A.Kwd "|-") -> ``` ``` Stream.junk ts; ``` ``` let f = parse_sortedFormula ts in ``` ``` (fl, f) ``` ``` | _ -> ``` ``` if List.length fl = 1 then ([], List.hd fl) ``` ``` else A.printError mk_exn ~ts "\"|-\" expected: " ``` ``` in ``` ``` importWrapper fkt s ``` ```(** 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 ``` ``` | AT (s, f1) -> AT (s, nnfNeg f1) ``` ``` | OR (f1, f2) -> AND (nnfNeg f1, nnfNeg f2) ``` ``` | AND (f1, f2) -> OR (nnfNeg f1, nnfNeg f2) ``` ``` | EQU (f1, f2) -> OR (AND (nnf f1, nnfNeg f2), AND (nnf f2, nnfNeg f1)) ``` ``` | IMP (f1, f2) -> AND (nnf f1, nnfNeg f2) ``` ``` | EX (s, f1) -> AX (s, nnfNeg f1) ``` ``` | AX (s, f1) -> EX (s, nnfNeg f1) ``` ``` | ENFORCES (s, f1) -> ALLOWS (s, nnfNeg f1) ``` ``` | ALLOWS (s, f1) -> ENFORCES (s, nnfNeg f1) ``` ``` | MIN (n, s, f1) -> if n = 0 then FALSE else MAXEXCEPT (n-1, s, nnfNeg f1) ``` ``` | MAX (n, s, f1) -> MORETHAN (n, s, nnf f1) ``` ``` | MORETHAN (n, s, f1) -> MAXEXCEPT (n, s, nnfNeg f1) ``` ``` | MAXEXCEPT (n, s, f1) -> MORETHAN (n, s, nnfNeg f1) ``` ``` | CHC (f1, f2) -> CHCN (nnfNeg f1, nnfNeg f2) ``` ``` | CHCN (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2) ``` ``` | FUS (first, f1) -> FUS (first, nnfNeg f1) ``` ``` ``` ```(** 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 ``` ``` | AT (s, f1) -> ``` ``` let ft1 = nnf f1 in ``` ``` if ft1 == f1 then f else AT (s, ft1) ``` ``` | 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) ``` ``` | EQU (f1, f2) -> AND (OR (nnfNeg f1, nnf f2), OR (nnfNeg f2, nnf f1)) ``` ``` | IMP (f1, f2) -> OR (nnfNeg f1, nnf f2) ``` ``` | EX (s, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else EX (s, ft) ``` ``` | AX (s, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else AX (s, ft) ``` ``` | ENFORCES (s, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else ENFORCES (s, ft) ``` ``` | ALLOWS (s, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else ALLOWS (s, ft) ``` ``` | MIN (n, s, f1) -> ``` ``` if n = 0 then TRUE ``` ``` else ``` ``` let ft = nnf f1 in ``` ``` MORETHAN (n-1,s,ft) ``` ``` | MAX (n, s, f1) -> ``` ``` let ft = nnfNeg f1 in ``` ``` MAXEXCEPT (n,s, ft) ``` ``` | MORETHAN (n,s,f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft = f1 then f else MORETHAN (n,s,ft) ``` ``` | MAXEXCEPT (n,s,f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft = f1 then f else MAXEXCEPT (n,s,ft) ``` ``` | CHC (f1, f2) -> ``` ``` let ft1 = nnf f1 in ``` ``` let ft2 = nnf f2 in ``` ``` if ft1 == f1 && ft2 == f2 then f else CHC (ft1, ft2) ``` ``` | CHCN (f1, f2) -> ``` ``` let ft1 = nnf f1 in ``` ``` let ft2 = nnf f2 in ``` ``` if ft1 == f1 && ft2 == f2 then f else CHCN (ft1, ft2) ``` ``` | FUS (first, f1) -> ``` ``` let ft = nnf f1 in ``` ``` if ft == f1 then f else FUS (first, ft) ``` ```(** Simplifies a formula. ``` ``` @param f A formula which must be in negation normal form. ``` ``` @return A formula in negation normal form that is equivalent to f. ``` ``` @raise CoAlgException if f is not in negation normal form. ``` ``` *) ``` ```let rec simplify f = ``` ``` match f with ``` ``` | TRUE ``` ``` | FALSE ``` ``` | AP _ ``` ``` | NOT (AP _) -> f ``` ``` | AT (s, f1) -> ``` ``` let ft = simplify f1 in ``` ``` begin ``` ``` match ft with ``` ``` | FALSE -> FALSE ``` ``` | TRUE -> TRUE ``` ``` | AT _ -> ft ``` ``` | AP s1 when s = s1 -> TRUE ``` ``` | NOT (AP s1) when s = s1 -> FALSE ``` ``` | _ -> if ft == f1 then f else AT (s, ft) ``` ``` end ``` ``` | OR (f1, f2) -> ``` ``` let ft1 = simplify f1 in ``` ``` let ft2 = simplify 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 = simplify f1 in ``` ``` let ft2 = simplify 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 ``` ``` | NOT _ ``` ``` | EQU _ ``` ``` | IMP _ -> raise (CoAlgException "Formula is not in negation normal form.") ``` ``` | EX (s, f1) -> ``` ``` let ft = simplify f1 in ``` ``` begin ``` ``` match ft with ``` ``` | FALSE -> FALSE ``` ``` | _ -> if ft == f1 then f else EX (s, ft) ``` ``` end ``` ``` | AX (s, f1) -> ``` ``` let ft = simplify f1 in ``` ``` begin ``` ``` match ft with ``` ``` | TRUE -> TRUE ``` ``` | _ -> if ft == f1 then f else AX (s, ft) ``` ``` end ``` ``` | ENFORCES (s, f1) -> ``` ``` let ft = simplify f1 in ``` ``` begin ``` ``` match ft with ``` ``` (* Simplification rules are checked with dirks Generic.hs ``` ``` let enforce ls = M (C ls) ``` ``` let allow ls = Neg . M (C ls) . Neg ``` ``` provable \$ F <-> enforce [1,2] F ``` ``` *) ``` ``` | TRUE -> TRUE ``` ``` | FALSE -> FALSE ``` ``` | _ -> if ft == f1 then f else ENFORCES (s, ft) ``` ``` end ``` ``` | ALLOWS (s, f1) -> ``` ``` let ft = simplify f1 in ``` ``` begin ``` ``` match ft with ``` ``` (* Simplification rules are checked with dirks Generic.hs ``` ``` let enforce ls = M (C ls) ``` ``` let allow ls = Neg . M (C ls) . Neg ``` ``` provable \$ F <-> enforce [1,2] F ``` ``` *) ``` ``` | TRUE -> TRUE ``` ``` | FALSE -> FALSE ``` ``` | _ -> if ft == f1 then f else ALLOWS (s, ft) ``` ``` end ``` ``` | MIN (n, s, f1) -> ``` ``` if n = 0 then TRUE ``` ``` else ``` ``` let ft = simplify f1 in ``` ``` begin ``` ``` match ft with ``` ``` | FALSE -> FALSE ``` ``` | _ -> if ft == f1 then f else MIN (n, s, ft) ``` ``` end ``` ``` | MORETHAN (n,s,f1) -> ``` ``` let ft = simplify f1 in ``` ``` if ft == f1 then f else MORETHAN (n,s,ft) ``` ``` | MAXEXCEPT (n,s,f1) -> ``` ``` let ft = simplify f1 in ``` ``` if ft == f1 then f else MAXEXCEPT (n,s,ft) ``` ``` | MAX (n, s, f1) -> ``` ``` let ft = simplify f1 in ``` ``` begin ``` ``` match ft with ``` ``` | FALSE -> TRUE ``` ``` | _ -> if ft == f1 then f else MAX (n, s, ft) ``` ``` end ``` ``` | CHC (f1, f2) -> ``` ``` let ft1 = simplify f1 in ``` ``` let ft2 = simplify f2 in ``` ``` begin ``` ``` match ft1, ft2 with ``` ``` | TRUE, TRUE -> TRUE ``` ``` | FALSE, FALSE -> FALSE ``` ``` | _, _ -> ``` ``` if (f1 == ft1) && (f2 == ft2) then f ``` ``` else CHC (ft1, ft2) ``` ``` end ``` ``` | CHCN (f1, f2) -> ``` ``` let ft1 = simplify f1 in ``` ``` let ft2 = simplify f2 in ``` ``` begin ``` ``` match ft1, ft2 with ``` ``` | TRUE, TRUE -> TRUE ``` ``` | FALSE, FALSE -> FALSE ``` ``` | _, _ -> ``` ``` if (f1 == ft1) && (f2 == ft2) then f ``` ``` else CHCN (ft1, ft2) ``` ``` end ``` ``` | FUS (first, f1) -> ``` ``` let ft = simplify f1 in ``` ``` begin ``` ``` match ft with ``` ``` | FALSE -> FALSE ``` ``` | TRUE -> TRUE ``` ``` | _ -> if ft == f1 then f else FUS (first, ft) ``` ``` end ``` ```(** Destructs an atomic proposition. ``` ``` @param f An atomic proposition. ``` ``` @return The name of the atomic proposition. ``` ``` @raise CoAlgException if f is not an atomic proposition. ``` ``` *) ``` ```let dest_ap f = ``` ``` match f with ``` ``` | AP s when not (isNominal s) -> s ``` ``` | _ -> raise (CoAlgException "Formula is not an atomic proposition.") ``` ```(** Destructs a nominal. ``` ``` @param f A nominal. ``` ``` @return The name of the nominal ``` ``` @raise CoAlgException if f is not a nominal. ``` ``` *) ``` ```let dest_nom f = ``` ``` match f with ``` ``` | AP s when isNominal s -> s ``` ``` | _ -> raise (CoAlgException "Formula is not a nominal.") ``` ```(** Destructs a negation. ``` ``` @param f A negation. ``` ``` @return The immediate subformula of the negation. ``` ``` @raise CoAlgException if f is not a negation. ``` ``` *) ``` ```let dest_not f = ``` ``` match f with ``` ``` | NOT f1 -> f1 ``` ``` | _ -> raise (CoAlgException "Formula is not a negation.") ``` ```(** Destructs an @-formula. ``` ``` @param f An @-formula. ``` ``` @return The name of the nominal and the immediate subformula of the @-formula. ``` ``` @raise CoAlgException if f is not an @-formula. ``` ``` *) ``` ```let dest_at f = ``` ``` match f with ``` ``` | AT (s, f1) -> (s, f1) ``` ``` | _ -> raise (CoAlgException "Formula is not an @-formula.") ``` ```(** Destructs an or-formula. ``` ``` @param f An or-formula. ``` ``` @return The two immediate subformulae of the or-formula. ``` ``` @raise CoAlgException if f is not an or-formula. ``` ``` *) ``` ```let dest_or f = ``` ``` match f with ``` ``` | OR (f1, f2) -> (f1, f2) ``` ``` | _ -> raise (CoAlgException "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 CoAlgException if f is not an and-formula. ``` ``` *) ``` ```let dest_and f = ``` ``` match f with ``` ``` | AND (f1, f2) -> (f1, f2) ``` ``` | _ -> raise (CoAlgException "Formula is not an and-formula.") ``` ```(** Destructs an equivalence. ``` ``` @param f An equivalence. ``` ``` @return The two immediate subformulae of the equivalence. ``` ``` @raise CoAlgException if f is not an equivalence. ``` ``` *) ``` ```let dest_equ f = ``` ``` match f with ``` ``` | EQU (f1, f2) -> (f1, f2) ``` ``` | _ -> raise (CoAlgException "Formula is not an equivalence.") ``` ```(** Destructs an implication. ``` ``` @param f An implication. ``` ``` @return The two immediate subformulae of the implication. ``` ``` @raise CoAlgException if f is not an implication. ``` ``` *) ``` ```let dest_imp f = ``` ``` match f with ``` ``` | IMP (f1, f2) -> (f1, f2) ``` ``` | _ -> raise (CoAlgException "Formula is not an implication.") ``` ```(** Destructs an EX-formula. ``` ``` @param f An EX-formula. ``` ``` @return The role name and the immediate subformula of the EX-formula. ``` ``` @raise CoAlgException if f is not an EX-formula. ``` ``` *) ``` ```let dest_ex f = ``` ``` match f with ``` ``` | EX (s, f1) -> (s, f1) ``` ``` | _ -> raise (CoAlgException "Formula is not an EX-formula.") ``` ```(** Destructs an AX-formula. ``` ``` @param f An AX-formula. ``` ``` @return The role name and the immediate subformula of the AX-formula. ``` ``` @raise CoAlgException if f is not an AX-formula. ``` ``` *) ``` ```let dest_ax f = ``` ``` match f with ``` ``` | AX (s, f1) -> (s, f1) ``` ``` | _ -> raise (CoAlgException "Formula is not an AX-formula.") ``` ```(** Destructs a MIN-formula. ``` ``` @param f A MIN-formula. ``` ``` @return The number restriction, role name, ``` ``` and the immediate subformula of the MIN-formula. ``` ``` @raise CoAlgException if f is not a MIN-formula. ``` ``` *) ``` ```let dest_min f = ``` ``` match f with ``` ``` | MIN (n, s, f1) -> (n, s, f1) ``` ``` | _ -> raise (CoAlgException "Formula is not a MIN-formula.") ``` ```(** Destructs a MAX-formula. ``` ``` @param f A MAX-formula. ``` ``` @return The number restriction, role name, ``` ``` and the immediate subformula of the MAX-formula. ``` ``` @raise CoAlgException if f is not a MAX-formula. ``` ``` *) ``` ```let dest_max f = ``` ``` match f with ``` ``` | MAX (n, s, f1) -> (n, s, f1) ``` ``` | _ -> raise (CoAlgException "Formula is not a MAX-formula.") ``` ```(** Destructs a choice formula. ``` ``` @param f A choice formula. ``` ``` @return The two immediate subformulae of the choice formula. ``` ``` @raise CoAlgException if f is not a choice formula. ``` ``` *) ``` ```let dest_choice f = ``` ``` match f with ``` ``` | CHC (f1, f2) -> (f1, f2) ``` ``` | _ -> raise (CoAlgException "Formula is not a choice formula.") ``` ```(** Destructs a fusion formula. ``` ``` @param f A fusion formula. ``` ``` @return A pair (first, f1) where ``` ``` first is true iff f is a first projection; and ``` ``` f1 is the immediate subformulae of f. ``` ``` @raise CoAlgException if f is not a fusion formula. ``` ``` *) ``` ```let dest_fusion f = ``` ``` match f with ``` ``` | FUS (first, f1) -> (first, f1) ``` ``` | _ -> raise (CoAlgException "Formula is not a fusion 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 s when not (isNominal s) -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is a nominal. ``` ``` @param f A formula. ``` ``` @return True iff f is a nominal. ``` ``` *) ``` ```let is_nom f = ``` ``` match f with ``` ``` | AP s when isNominal s -> 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 @-formula. ``` ``` @param f A formula. ``` ``` @return True iff f is an @-formula. ``` ``` *) ``` ```let is_at f = ``` ``` match f with ``` ``` | AT _ -> 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 ``` ```(** 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 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 a choice formula. ``` ``` @param f A formula. ``` ``` @return True iff f is a choice formula. ``` ``` *) ``` ```let is_choice f = ``` ``` match f with ``` ``` | CHC _ -> true ``` ``` | _ -> false ``` ```(** Tests whether a formula is a fusion formula. ``` ``` @param f A formula. ``` ``` @return True iff f is a fusion formula. ``` ``` *) ``` ```let is_fusion f = ``` ``` match f with ``` ``` | FUS _ -> 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. ``` ``` @raise CoAlgException if s is a nominal name. ``` ``` *) ``` ```let const_ap s = ``` ``` if isNominal s then raise (CoAlgException "The name indicates a nominal.") ``` ``` else AP s ``` ```(** Constructs a nominal. ``` ``` @param s The name of the nominal. ``` ``` @return A nominal with name s. ``` ``` @raise CoAlgException if s is not a nominal name. ``` ``` *) ``` ```let const_nom s = ``` ``` if isNominal s then AP s ``` ``` else raise (CoAlgException "The name does not indicate a nominal.") ``` ```(** Negates a formula. ``` ``` @param f A formula. ``` ``` @return The negation of f. ``` ``` *) ``` ```let const_not f = NOT f ``` ``` ``` ```(** Constructs an @-formula from a name and a formula. ``` ``` @param s A nominal name. ``` ``` @param f A formula. ``` ``` @return The formula AT (s, f). ``` ``` *) ``` ```let const_at s f = AT (s, f) ``` ```(** 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) ``` ```(** 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 EX-formula from a formula. ``` ``` @param s A role name. ``` ``` @param f A formula. ``` ``` @return The formula EX (s, f). ``` ``` *) ``` ```let const_ex s f = EX (s, f) ``` ```(** Constructs an AX-formula from a formula. ``` ``` @param s A role name. ``` ``` @param f A formula. ``` ``` @return The formula AX (s, f). ``` ``` *) ``` ```let const_ax s f = AX (s, f) ``` ```(** Constructs a MIN-formula from a formula. ``` ``` @param n A non-negative integer. ``` ``` @param s A role name. ``` ``` @param f A formula. ``` ``` @return The formula MIN f. ``` ``` @raise CoAlgException Iff n is negative. ``` ``` *) ``` ```let const_min n s f = ``` ``` if n < 0 then raise (CoAlgException "Negative cardinality constraint.") ``` ``` else MIN (n, s, f) ``` ```(** Constructs a MAX-formula from a formula. ``` ``` @param n A non-negative integer. ``` ``` @param s A role name. ``` ``` @param f A formula. ``` ``` @return The formula MAX f. ``` ``` @raise CoAlgException Iff n is negative. ``` ``` *) ``` ```let const_max n s f = ``` ``` if n < 0 then raise (CoAlgException "Negative cardinality constraint.") ``` ``` else MAX (n, s, f) ``` ```let const_enforces p f = ``` ``` ENFORCES (p,f) ``` ```let const_allows p f = ``` ``` ALLOWS (p,f) ``` ```(** Constructs a choice formula from two formulae. ``` ``` @param f1 The first formula (LHS). ``` ``` @param f2 The second formula (LHS). ``` ``` @return The formula (f1 + f2). ``` ``` *) ``` ```let const_choice f1 f2 = CHC (f1, f2) ``` ```(** Constructs a fusion formula. ``` ``` @param first True iff the result is a first projection. ``` ``` @param f1 A formula. ``` ``` @return The formula [pi1] f1 or [pi2] f1 (depending on first). ``` ``` *) ``` ```let const_fusion first f1 = FUS (first, f1) ``` ```(** 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 ``` ``` | HCAT of string * hcFormula ``` ``` | HCOR of hcFormula * hcFormula ``` ``` | HCAND of hcFormula * hcFormula ``` ``` | HCEX of string * hcFormula ``` ``` | HCAX of string * hcFormula ``` ``` | HCENFORCES of int list * hcFormula ``` ``` | HCALLOWS of int list * hcFormula ``` ``` | HCMORETHAN of int * string * hcFormula (* GML Diamond *) ``` ``` | HCMAXEXCEPT of int * string * hcFormula (* GML Box *) ``` ``` | HCCHC of hcFormula * hcFormula ``` ``` | HCCHCN of hcFormula * hcFormula ``` ``` | HCFUS of bool * 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 ``` ``` | HCAT (s1, f1), HCAT (s2, f2) -> compare s1 s2 = 0 && f1 == f2 ``` ``` | HCOR (f1a, f1b), HCOR (f2a, f2b) ``` ``` | HCAND (f1a, f1b), HCAND (f2a, f2b) -> f1a == f2a && f1b == f2b ``` ``` | HCEX (s1, f1), HCEX (s2, f2) ``` ``` | HCAX (s1, f1), HCAX (s2, f2) -> compare s1 s2 = 0 && f1 == f2 ``` ``` | HCENFORCES (s1, f1), HCALLOWS (s2, f2) ``` ``` | HCENFORCES (s1, f1), HCALLOWS (s2, f2) -> compare s1 s2 = 0 && f1 == f2 ``` ``` | HCMORETHAN (n1, s1, f1), HCMORETHAN (n2, s2, f2) ``` ``` | HCMAXEXCEPT (n1, s1, f1), HCMAXEXCEPT (n2, s2, f2) -> ``` ``` n1 = n2 && compare s1 s2 = 0 && f1 == f2 ``` ``` | HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b ``` ``` | HCCHCN (f1a, f1b), HCCHCN (f2a, f2b) -> f1a == f2a && f1b == f2b ``` ``` | HCFUS (first1, f1), HCFUS (first2, f2) -> first1 = first2 && f1 == f2 ``` ```(* The rest could be shortened to | _ -> false, ``` ``` but then the compiler would not warn if the formula type is extended ``` ``` and this function is not updated accordingly.*) ``` ``` | HCTRUE, _ ``` ``` | HCFALSE, _ ``` ``` | HCAP _, _ ``` ``` | HCNOT _, _ ``` ``` | HCAT _, _ ``` ``` | HCOR _, _ ``` ``` | HCAND _, _ ``` ``` | HCEX _, _ ``` ``` | HCAX _, _ ``` ``` | HCENFORCES _, _ ``` ``` | HCALLOWS _, _ ``` ``` | HCMORETHAN _, _ ``` ``` | HCMAXEXCEPT _, _ ``` ``` | HCCHC _, _ ``` ``` | HCCHCN _, _ ``` ``` | HCFUS _, _ -> 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 ``` ``` | HCNOT s -> 19 * Hashtbl.hash s + 1 ``` ``` | HCAT (s, f1) -> 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 2 ``` ``` | HCOR (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 5 ``` ``` | HCAND (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 6 ``` ``` | HCEX (s, f1) -> 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 3 ``` ``` | HCAX (s, f1) -> 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 4 ``` ``` | HCMORETHAN (n, s, f1) -> 19 * (19 * (19 * (Hashtbl.hash s) + n) + f1.HC.hkey) + 7 ``` ``` | HCMAXEXCEPT (n, s, f1) -> 19 * (19 * (19 * (Hashtbl.hash s) + n) + f1.HC.hkey) + 8 ``` ``` | HCCHC (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 9 ``` ``` | HCCHCN (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 10 ``` ``` | HCFUS (first, f1) -> 19 * (19 * (Hashtbl.hash first) + f1.HC.hkey) + 11 ``` ``` | HCENFORCES (s, f1) -> 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 12 ``` ``` | HCALLOWS (s, f1) -> 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 13 ``` ```(** 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) ``` ``` | HCAT (s, f1) -> AT (s, f1.HC.fml) ``` ``` | HCOR (f1, f2) -> OR (f1.HC.fml, f2.HC.fml) ``` ``` | HCAND (f1, f2) -> AND (f1.HC.fml, f2.HC.fml) ``` ``` | HCEX (s, f1) -> EX (s, f1.HC.fml) ``` ``` | HCAX (s, f1) -> AX (s, f1.HC.fml) ``` ``` | HCENFORCES (s, f1) -> ENFORCES (s, f1.HC.fml) ``` ``` | HCALLOWS (s, f1) -> ALLOWS (s, f1.HC.fml) ``` ``` | HCMORETHAN (n, s, f1) -> MORETHAN (n, s, f1.HC.fml) ``` ``` | HCMAXEXCEPT (n, s, f1) -> MAXEXCEPT (n, s, f1.HC.fml) ``` ``` | HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml) ``` ``` | HCCHCN (f1, f2) -> CHCN (f1.HC.fml, f2.HC.fml) ``` ``` | HCFUS (first, f1) -> FUS (first, f1.HC.fml) ``` ```(** 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 ``` ``` | HCAT (s, f1) -> HCAT (s, f1.HC.neg) ``` ``` | HCOR (f1, f2) -> HCAND (f1.HC.neg, f2.HC.neg) ``` ``` | HCAND (f1, f2) -> HCOR (f1.HC.neg, f2.HC.neg) ``` ``` | HCEX (s, f2) -> HCAX (s, f2.HC.neg) ``` ``` | HCAX (s, f2) -> HCEX (s, f2.HC.neg) ``` ``` | HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg) ``` ``` | HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg) ``` ``` | HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg) ``` ``` | HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg) ``` ``` | HCCHC (f1, f2) -> HCCHCN (f1.HC.neg, f2.HC.neg) ``` ``` | HCCHCN (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg) ``` ``` | HCFUS (first, f1) -> HCFUS (first, f1.HC.neg) ``` ```(** 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 ``` ``` ) ``` ```(** 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 CoAlgException 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) ``` ``` | AT (s, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCAT (s, 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)) ``` ``` | NOT _ ``` ``` | EQU _ ``` ``` | MIN _ ``` ``` | MAX _ ``` ``` | IMP _ -> raise (CoAlgException "Formula is not in negation normal form.") ``` ``` | EX (s, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCEX (s, tf1)) ``` ``` | AX (s, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCAX (s, tf1)) ``` ``` | ENFORCES (s, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCENFORCES (s, tf1)) ``` ``` | ALLOWS (s, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCALLOWS (s, tf1)) ``` ``` | MORETHAN (n, s, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCMORETHAN (n, s, tf1)) ``` ``` | MAXEXCEPT (n, s, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCMAXEXCEPT (n, s, tf1)) ``` ``` | CHC (f1, f2) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` let tf2 = hc_formula hcF f2 in ``` ``` HcFormula.hashcons hcF (HCCHC (tf1, tf2)) ``` ``` | CHCN (f1, f2) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` let tf2 = hc_formula hcF f2 in ``` ``` HcFormula.hashcons hcF (HCCHCN (tf1, tf2)) ``` ``` | FUS (first, f1) -> ``` ``` let tf1 = hc_formula hcF f1 in ``` ``` HcFormula.hashcons hcF (HCFUS (first, tf1)) ``` ```(** 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 ``` ``` ) ```