Commit ca99d0c6 authored by Thorsten Wißmann's avatar Thorsten Wißmann 🐧
Browse files

Improve OWL -> CoAlg conversion

parent c78c1ce0
......@@ -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
......
......@@ -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
......
......@@ -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 =
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment