From cb99c7921372d05d21289be1df8ac315af185e99 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <stan@hb.dhhbw-stuttgart.de>
Date: Tue, 18 Jun 2024 18:44:11 +0200
Subject: [PATCH] Start Implementation of the Algorithm described in the paper

---
 src/main/asp/unifyPaper.pl | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)
 create mode 100644 src/main/asp/unifyPaper.pl

diff --git a/src/main/asp/unifyPaper.pl b/src/main/asp/unifyPaper.pl
new file mode 100644
index 0000000..1754fbc
--- /dev/null
+++ b/src/main/asp/unifyPaper.pl
@@ -0,0 +1,30 @@
+
+type("Name", paramList).
+type("Name", params()).
+params(paramList, tph(a), 1).
+
+% subst:
+subst(tph(A), type(N,P)) :- equalcons(tph(A), type(N, P)).
+
+% subst-L:
+substcons(B,C) :- subst(A, B), substcons(A, C).
+%subst-R:
+substcons(B,C) :- subst(A, B), substcons(C, A).
+%subst-Equal:
+equalcons(B,C) :- subst(A, B), substcons(A, C).
+
+%swap:
+equalcons(A,B) :- equalcons(B,A).
+
+%unfold:
+equalcons(T, T) :- equalcons(tph(_), type(_, params(T, _, _))).
+equalcons(T, T) :- equalcons(tph(_), type(_, params(_, T, _))).
+equalcons(T, T) :- equalcons(tph(_), type(_, params(_, _, T))).
+
+% here we check if there is a constraint a <. C, where there is no other Constraint. This is the solution-Gen rule
+%Solution-Subst:
+hasNoSupertype(tph(A), type(D,P2)) :- substcons(tph(A), type(C,P)), substcons(tph(A), type(D,P2)), not super(D, C).
+equalcons(tph(A), type(C,P)) :- substcons(tph(A), type(C,P)), hasNoSupertype(tph(A), type(C,P)).
+
+%Solution:
+sigma(tph(A), tpye(C,P)) :- equalcons(tph(A), type(C, P)), not tphs(_, P).
\ No newline at end of file