From ca99d0c6b1dbb0f8b6a28ae4e6b92bc35ef12b62 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Tue, 6 May 2014 08:30:52 +0200
Subject: [PATCH] Improve OWL -> CoAlg conversion
---
src/lib/CoAlgFormula.ml | 25 ++++++++++++++++++-------
src/lib/CoAlgFormula.mli | 5 +++--
src/owl/OWL.ml | 14 +++++++++++---
3 files changed, 32 insertions(+), 12 deletions(-)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 8bcaef8..196a2d9 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -16,9 +16,6 @@ module Str = String
*)
exception CoAlgException of string
-exception ConversionException
-
-
(** Indicates the sort of a sorted formula
*)
type sort = int
@@ -47,6 +44,9 @@ type formula =
| CHCN of formula * formula
| FUS of bool * formula
+exception ConversionException of formula
+
+
(** Defines sorted coalgebraic formulae.
*)
type sortedFormula = sort * formula
@@ -137,24 +137,33 @@ let rec convert_post func formula = (* run over all subformulas in post order *)
let convertToK formula = (* tries to convert a formula to a pure K formula *)
let helper formula = match formula with
- | ENFORCES _ | ALLOWS _ -> raise ConversionException
+ | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula)
| MORETHAN (0,s,a) | MIN (1,s,a) -> EX (s,a)
| MAX (0,s,a) -> AX (s, NOT a)
| MAXEXCEPT (0,s,a) -> AX (s, a)
+ | TRUE | FALSE
+ | EQU _ | IMP _
+ | AND _ | OR _
+ | AP _ | NOT _
| AX _ | EX _
| CHC _ | CHCN _ | FUS _ -> formula
- | _ -> raise ConversionException
+ | _ -> raise (ConversionException formula)
in
convert_post helper formula
let convertToGML formula = (* tries to convert a formula to a pure GML formula *)
let helper formula = match formula with
- | ENFORCES _ | ALLOWS _ -> raise ConversionException
+ | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula)
| MORETHAN _ | MIN _ | MAX _ | MAXEXCEPT _ -> formula
+ | TRUE | FALSE
+ | EQU _ | IMP _
+ | AND _ | OR _
+ | AP _ | NOT _
+ | AX _ | EX _
| CHC _ | CHCN _ | FUS _ -> formula
| AX (r,a) -> MAXEXCEPT (0,r,a)
| EX (r,a) -> MORETHAN (0,r,a)
- | _ -> raise ConversionException
+ | _ -> raise (ConversionException formula)
in
convert_post helper formula
@@ -295,6 +304,8 @@ let exportFormula f =
exportFormula_buffer sb f;
Buffer.contents sb
+let string_of_formula = exportFormula
+
(** export (CL)-formula suitable for tatl-inputs *)
let rec exportTatlFormula_buffer sb f =
let negate = function
diff --git a/src/lib/CoAlgFormula.mli b/src/lib/CoAlgFormula.mli
index 87a6c6c..6b5484d 100644
--- a/src/lib/CoAlgFormula.mli
+++ b/src/lib/CoAlgFormula.mli
@@ -6,8 +6,6 @@
exception CoAlgException of string
-exception ConversionException
-
type sort = int
type formula =
@@ -32,6 +30,8 @@ type formula =
| CHCN of formula * formula
| FUS of bool * formula
+exception ConversionException of formula
+
type sortedFormula = sort * formula
val iter : (formula -> unit) -> formula -> unit (* iterate over all sub formulas *)
@@ -44,6 +44,7 @@ val isNominal : string -> bool
val sizeFormula : formula -> int
val sizeSortedFormula : sortedFormula -> int
+val string_of_formula : formula -> string
val exportFormula : formula -> string
val exportTatlFormula : formula -> string
val exportSortedFormula : sortedFormula -> string
diff --git a/src/owl/OWL.ml b/src/owl/OWL.ml
index 9406051..09efc4d 100644
--- a/src/owl/OWL.ml
+++ b/src/owl/OWL.ml
@@ -138,7 +138,13 @@ let coalg_global_assumption_of_owl (ax:axiom): CoAlgFormula.formula =
| ANNOTATION _ -> CoAlg.TRUE (* ignore annotations *)
| DECLARATION _ -> CoAlg.TRUE (* ignore declarations *)
| SUBCLASS (a,b) -> o2c (OR [NOT a; b])
- | EQUIVALENTCLASSES l -> raise (ConversionError "not implemented yet")
+ | EQUIVALENTCLASSES l ->
+ (* if a_1 ... a_n are equivalent, then at each point it is
+ a_1 ∧ … ∧ a_n (all hold) or ¬a_1 ∧ … ∧ ¬a_n (none holds) *)
+ let conjunction = L.fold_left (fun x y -> CoAlg.AND (x, y)) CoAlg.TRUE in
+ let allhold = conjunction (L.map o2c l) in
+ let nonehold = conjunction (L.map (CoAlg.const_not << o2c) l) in
+ CoAlg.OR (allhold, nonehold)
| DISJOINTCLASSES l -> raise (ConversionError "not implemented yet")
| DISJOINTUNION (c,l) -> raise (ConversionError "not implemented yet")
@@ -148,8 +154,10 @@ let to_coalg (uri,axioms): R.sortTable * R.nomTable * R.assumptions =
let (assumptions, fnctor) = (* ofcourse functor leads to "Error: pattern expected".. *)
try
(L.map CoAlg.convertToK assumptions, CM.MultiModalK)
- with CoAlg.ConversionException ->
- (L.map CoAlg.convertToGML assumptions, CM.GML)
+ with CoAlg.ConversionException _ ->
+ try (L.map CoAlg.convertToGML assumptions, CM.GML)
+ with CoAlg.ConversionException f ->
+ raise (ConversionError (CoAlg.string_of_formula f))
in
let sorts = [| (fnctor, [0]) |] in
let nomTable name =
--
GitLab