From 5ec97220879a247b3d8233baa92bd5d95b667668 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Tue, 1 Dec 2015 17:01:13 +0100
Subject: [PATCH] =?UTF-8?q?Implement=20initTables=20for=20=CE=BC-Calculus?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Make following state of a fixpoint it's unfold
---
src/lib/CoAlgMisc.ml | 10 ++++++++++
1 file changed, 10 insertions(+)
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 54ff973..6b1e98e 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -1047,6 +1047,16 @@ let initTables nomTbl hcF htF htR s f n =
let s1 = List.nth sortlst (if first then 0 else 1) in
!arrayDest1.(s).(n) <- C.HcFHt.find htF.(s1) f1;
!arrayDest3.(s).(n) <- if first then 0 else 1
+ | C.HCMU (name, f1) ->
+ !arrayType.(s).(n) <- MuF;
+ let unfold = C.hc_replace hcF name f f1 in
+ !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold
+ | C.HCNU (name, f1) ->
+ !arrayType.(s).(n) <- NuF;
+ let unfold = C.hc_replace hcF name f f1 in
+ !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold
+ | C.HCVAR _ -> !arrayType.(s).(n) <- Other
+
let initTablesAt hcF htF name sort =
let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
--
GitLab