From d29d35f73f3439c7e91ccccda22a3f2a59c50892 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Fri, 6 Nov 2015 22:36:53 +0100
Subject: [PATCH] =?UTF-8?q?Actually=20represent=20variable=20under=20?=
=?UTF-8?q?=CE=BC/=CE=BD=20as=20string?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
so it's `MU of string * formula` again. The variable within the formula
is still represented as `VAR s`
---
src/lib/CoAlgFormula.ml | 24 ++++++++++++------------
src/lib/CoAlgFormula.mli | 4 ++--
2 files changed, 14 insertions(+), 14 deletions(-)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 14e2806..63e59e9 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -58,8 +58,8 @@ type formula =
| NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *)
| CHC of formula * formula (* Choice is self-dual *)
| FUS of bool * formula
- | MU of formula * formula
- | NU of formula * formula
+ | MU of string * formula
+ | NU of string * formula
| VAR of string
| AF of formula
| EF of formula
@@ -231,17 +231,17 @@ let convertToMu formula =
let symbol = Stream.next gensym in
match formula with
| AF f1 ->
- MU ((VAR symbol), (OR (f1, (AX ("", (VAR symbol))))))
+ MU (symbol, (OR (f1, (AX ("", (VAR symbol))))))
| EF f1 ->
- MU ((VAR symbol), (OR (f1, (AX ("", (VAR symbol))))))
+ MU (symbol, (OR (f1, (EX ("", (VAR symbol))))))
| AG f1 ->
- NU ((VAR symbol), (AND (f1, (AX ("", (VAR symbol))))))
+ NU (symbol, (AND (f1, (AX ("", (VAR symbol))))))
| EG f1 ->
- NU ((VAR symbol), (AND (f1, (AX ("", (VAR symbol))))))
+ NU (symbol, (AND (f1, (EX ("", (VAR symbol))))))
| AU (f1, f2) ->
- MU ((VAR symbol), (OR (f2, (AND (f1, (AX ("", (VAR symbol))))))))
+ MU (symbol, (OR (f2, (AND (f1, (AX ("", (VAR symbol))))))))
| EU (f1, f2) ->
- MU ((VAR symbol), (OR (f2, (AND (f1, (EX ("", (VAR symbol))))))))
+ MU (symbol, (OR (f2, (AND (f1, (EX ("", (VAR symbol))))))))
| _ -> formula
in
convert_post helper formula
@@ -396,12 +396,12 @@ let rec exportFormula_buffer sb f =
prio 4 f1
| MU (s, f1) ->
Buffer.add_string sb "μ";
- prio 4 s;
+ Buffer.add_string sb s;
Buffer.add_string sb ".";
prio 4 f1
| NU (s, f1) ->
Buffer.add_string sb "ν";
- prio 4 s;
+ Buffer.add_string sb s;
Buffer.add_string sb ".";
prio 4 f1
| VAR s ->
@@ -820,11 +820,11 @@ and parse_rest ts =
| A.Kwd "μ" ->
let (_, _, s) = boxinternals true "." in
let f1 = parse_rest ts in
- MU (VAR s, f1)
+ MU (s, f1)
| A.Kwd "ν" ->
let (_, _, s) = boxinternals true "." in
let f1 = parse_rest ts in
- NU (VAR s, f1)
+ NU (s, f1)
| A.Kwd "AF" ->
let f = parse_rest ts in
AF f
diff --git a/src/lib/CoAlgFormula.mli b/src/lib/CoAlgFormula.mli
index c807b4e..b133f86 100644
--- a/src/lib/CoAlgFormula.mli
+++ b/src/lib/CoAlgFormula.mli
@@ -41,8 +41,8 @@ type formula =
| NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *)
| CHC of formula * formula
| FUS of bool * formula
- | MU of formula * formula
- | NU of formula * formula
+ | MU of string * formula
+ | NU of string * formula
| VAR of string
| AF of formula
| EF of formula
--
GitLab