Add some basic OWL->CoAlg conversions

src/owl/OWL.ml

 
 open CoolUtils
 module L = List
+module CoAlg = CoAlgFormula
+
+exception ConversionError of string
 
 (* Just a copy'n'paste from the *.mli file *)
 type uri = string
@@ -108,4 +111,32 @@ let string_of_ontology (name,axioms) =
     String.concat "\n" (L.map (((^) "  ") << string_of_axiom) axioms)
     )^"\n}\n"
 
+let rec coalg_formula_of_owl (ce:class_exp): CoAlgFormula.formula =
+    let o2c = coalg_formula_of_owl in
+    let o2r r = match r with
+                | ROLE str -> str
+                | INVERSE _ -> raise (ConversionError "Can not express inverses with coalgebraic formulas")
+    in
+    match ce with
+    | THING -> CoAlg.TRUE
+    | NOTHING -> CoAlg.FALSE
+    | NAMED str -> CoAlg.AP str
+    | NOT ce -> CoAlg.NOT (o2c ce)
+    | AND l -> L.fold_left (fun x y -> CoAlg.AND (x, o2c y)) CoAlg.TRUE l
+    | OR l -> L.fold_left (fun x y -> CoAlg.OR (x, o2c y)) CoAlg.FALSE l
+    | SOME (r,c) -> CoAlg.EX (o2r r, o2c c)
+    | ALL (r,c) -> CoAlg.AX (o2r r, o2c c)
+    | MIN (i,r,c) -> CoAlg.MIN (i, o2r r, o2c c)
+    | MAX (i,r,c) -> CoAlg.MAX (i, o2r r, o2c c)
+
+
+let coalg_global_assumption_of_owl (ax:axiom): CoAlgFormula.formula =
+    let o2c = coalg_formula_of_owl in
+    match ax with
+    | 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")
+    | DISJOINTCLASSES l -> raise (ConversionError "not implemented yet")
+    | DISJOINTUNION (c,l) -> raise (ConversionError "not implemented yet")
 

src/owl/OWL.mli

 
+exception ConversionError of string
 
 type uri = string
 type role =
@@ -45,3 +46,5 @@ val string_of_ontology : ontology -> string
 val string_of_axiom : axiom -> string
 val string_of_class_exp : class_exp -> string
 
+val coalg_formula_of_owl : class_exp -> CoAlgFormula.formula
+val coalg_global_assumption_of_owl : axiom -> CoAlgFormula.formula