1
0

Start Implementation of the Algorithm described in the paper

This commit is contained in:
Andreas Stadelmeier 2024-06-18 18:44:11 +02:00
parent d82c4d3ebf
commit cb99c79213

View File

@ -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).