From 33b4710dac9708b9631458243aba413af7801c1a Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Wed, 19 Jun 2024 23:15:52 +0200 Subject: [PATCH] New Algorithm with Matrix input --- src/main/asp/unifyPaper.pl | 148 +++++++++++++++++++++++++++++++++++-- 1 file changed, 140 insertions(+), 8 deletions(-) diff --git a/src/main/asp/unifyPaper.pl b/src/main/asp/unifyPaper.pl index 1754fbc..216e048 100644 --- a/src/main/asp/unifyPaper.pl +++ b/src/main/asp/unifyPaper.pl @@ -1,7 +1,70 @@ +% TEST INPUT +orCons(undCons(substcons(tph("_BG"),type("java.lang.Number",null)),undCons(equalcons(tph("_BE"),type("java.lang.Boolean",null)),undCons(equalcons(type("java.lang.Boolean",null),tph("_AH")),undCons(substcons(tph("_BC"),type("java.lang.Number",null)),undCons(substcons(tph("_G"),type("java.lang.Integer",null)),undCons(substcons(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_AS")),undCons(equalcons(type("java.lang.Boolean",null),tph("_H")),undCons(substcons(tph("_AP"),tph("_AM")),undCons(substcons(tph("_AV"),tph("_AU")),undCons(equalcons(tph("_AI"),type("Matrix",null)),undCons(substcons(tph("_AD"),tph("_AB")),undCons(substcons(type("Matrix",null),tph("_AD")),undCons(substcons(tph("_AF"),type("java.lang.Number",null)),undCons(equalcons(tph("_AU"),tph("_CD")),undCons(equalcons(tph("_H"),type("java.lang.Boolean",null)),undCons(substcons(tph("_BV"),tph("_BA")),undCons(substcons(tph("_V"),type("java.lang.Integer",null)),undCons(substcons(tph("_J"),type("java.lang.Number",null)),undCons(substcons(tph("_AY"),type("java.lang.Number",null)),undCons(equalcons(tph("_AH"),type("java.lang.Boolean",null)),undCons(equalcons(type("java.lang.Boolean",null),tph("_BE")),undCons(equalcons(tph("_AF"),tph("_CK")),undCons(equalcons(type("java.lang.Boolean",null),tph("_AW")),undCons(substcons(tph("_AU"),type("java.lang.Number",null)),undCons(substcons(tph("_BD"),tph("_BC")),undCons(equalcons(tph("_AW"),type("java.lang.Boolean",null)),undCons(substcons(tph("_BB"),tph("_BA")),undCons(substcons(tph("_AG"),tph("_AF")),undCons(equalcons(tph("_S"),type("Matrix",null)),undCons(equalcons(type("java.util.Vector",params(type("java.util.Vector",params(type("java.lang.Integer",null))))),type("java.util.Vector",params(tph("_ANQ")))),undCons(substcons(type("java.lang.Integer",null),type("java.lang.Number",null)),undCons(equalcons(type("java.util.Vector",params(type("java.util.Vector",params(type("java.lang.Integer",null))))),type("java.util.Vector",params(tph("_ANR")))),undCons(equalcons(tph("_BC"),tph("_BW")),undCons(equalcons(tph("_AQ"),type("Matrix",null)),undCons(substcons(tph("_AK"),type("java.lang.Number",null)), null))))))))))))))))))))))))))))))))))), null). +orCons(undCons(equalcons(tph("_AE"),type("Matrix",null)),undCons(substcons(type("Matrix",null),type("Matrix",null)), null)), null). +orCons(undCons(equalcons(tph("_AG"),type("java.lang.Integer",null)), null), null). +orCons(undCons(equalcons(tph("_AI"),type("java.util.AbstractList",params(tph("_AMV")))),undCons(substcons(type("java.lang.Integer",null),tph("_AK")), null)),orCons(undCons(equalcons(tph("_AI"),type("Matrix",null)),undCons(substcons(type("java.lang.Integer",null),tph("_AK")), null)),orCons(undCons(substcons(type("java.lang.Integer",null),tph("_AK")),undCons(equalcons(tph("_AI"),type("java.util.List",params(tph("_AMU")))), null)),orCons(undCons(equalcons(tph("_AI"),type("java.util.AbstractList",params(tph("_AMV")))),undCons(substcons(type("java.lang.Integer",null),tph("_AK")), null)),orCons(undCons(substcons(type("java.lang.Integer",null),tph("_AK")),undCons(equalcons(tph("_AI"),type("java.util.Vector",params(tph("_AMW")))), null)),orCons(undCons(equalcons(tph("_AI"),type("java.util.List",params(tph("_AMU")))),undCons(substcons(type("java.lang.Integer",null),tph("_AK")), null)),orCons(undCons(substcons(type("java.lang.Integer",null),tph("_AK")),undCons(equalcons(tph("_AI"),type("java.util.Vector",params(tph("_AMW")))), null)),orCons(undCons(equalcons(tph("_AI"),type("Matrix",null)),undCons(substcons(type("java.lang.Integer",null),tph("_AK")), null)), null)))))))). +orCons(undCons(substcons(tph("_AF"),type("java.lang.Integer",null)),undCons(equalcons(tph("_AQ"),type("java.util.Vector",params(tph("_AMX")))),undCons(substcons(tph("_AMX"),tph("_AP")), null))),orCons(undCons(substcons(tph("_AF"),type("java.lang.Integer",null)),undCons(equalcons(tph("_AQ"),type("Matrix",null)),undCons(substcons(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_AP")), null))),orCons(undCons(substcons(tph("_AF"),type("java.lang.Integer",null)),undCons(equalcons(tph("_AQ"),type("java.util.Vector",params(tph("_AMX")))),undCons(substcons(tph("_AMX"),tph("_AP")), null))),orCons(undCons(substcons(tph("_AF"),type("java.lang.Integer",null)),undCons(equalcons(tph("_AQ"),type("Matrix",null)),undCons(substcons(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_AP")), null))), null)))). +orCons(undCons(substcons(type("java.util.Vector",params(tph("_AMY"))),type("java.util.Vector",params(type("java.lang.Integer",null)))),undCons(equalcons(tph("_AT"),type("java.util.Vector",params(type("GE",null)))), null)), null). +orCons(undCons(equalcons(tph("_AV"),type("java.lang.Integer",null)), null), null). +orCons(undCons(substcons(type("java.lang.Integer",null),tph("_AY")),undCons(equalcons(tph("_AM"),type("Matrix",null)), null)),orCons(undCons(substcons(type("java.lang.Integer",null),tph("_AY")),undCons(equalcons(tph("_AM"),type("java.util.List",params(tph("_AMZ")))), null)),orCons(undCons(substcons(type("java.lang.Integer",null),tph("_AY")),undCons(equalcons(tph("_AM"),type("java.util.Vector",params(tph("_ANB")))), null)),orCons(undCons(substcons(type("java.lang.Integer",null),tph("_AY")),undCons(equalcons(tph("_AM"),type("java.util.List",params(tph("_AMZ")))), null)),orCons(undCons(substcons(type("java.lang.Integer",null),tph("_AY")),undCons(equalcons(tph("_AM"),type("java.util.AbstractList",params(tph("_ANA")))), null)),orCons(undCons(substcons(type("java.lang.Integer",null),tph("_AY")),undCons(equalcons(tph("_AM"),type("java.util.AbstractList",params(tph("_ANA")))), null)),orCons(undCons(substcons(type("java.lang.Integer",null),tph("_AY")),undCons(equalcons(tph("_AM"),type("Matrix",null)), null)),orCons(undCons(substcons(type("java.lang.Integer",null),tph("_AY")),undCons(equalcons(tph("_AM"),type("java.util.Vector",params(tph("_ANB")))), null)), null)))))))). +orCons(undCons(equalcons(tph("_BB"),type("java.lang.Integer",null)), null), null). +orCons(undCons(equalcons(tph("_BD"),type("java.lang.Integer",null)), null), null). +orCons(undCons(equalcons(tph("_AM"),type("java.util.Vector",params(tph("_ANE")))),undCons(substcons(type("java.lang.Integer",null),tph("_BG")), null)),orCons(undCons(substcons(type("java.lang.Integer",null),tph("_BG")),undCons(equalcons(tph("_AM"),type("Matrix",null)), null)),orCons(undCons(equalcons(tph("_AM"),type("java.util.Vector",params(tph("_ANE")))),undCons(substcons(type("java.lang.Integer",null),tph("_BG")), null)),orCons(undCons(substcons(type("java.lang.Integer",null),tph("_BG")),undCons(equalcons(tph("_AM"),type("java.util.AbstractList",params(tph("_AND")))), null)),orCons(undCons(substcons(type("java.lang.Integer",null),tph("_BG")),undCons(equalcons(tph("_AM"),type("Matrix",null)), null)),orCons(undCons(equalcons(tph("_AM"),type("java.util.List",params(tph("_ANC")))),undCons(substcons(type("java.lang.Integer",null),tph("_BG")), null)),orCons(undCons(equalcons(tph("_AM"),type("java.util.List",params(tph("_ANC")))),undCons(substcons(type("java.lang.Integer",null),tph("_BG")), null)),orCons(undCons(substcons(type("java.lang.Integer",null),tph("_BG")),undCons(equalcons(tph("_AM"),type("java.util.AbstractList",params(tph("_AND")))), null)), null)))))))). +orCons(undCons(substcons(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_BK")),undCons(substcons(tph("_BC"),type("java.lang.Integer",null)),undCons(equalcons(tph("_AM"),type("Matrix",null)), null))),orCons(undCons(substcons(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_BK")),undCons(substcons(tph("_BC"),type("java.lang.Integer",null)),undCons(equalcons(tph("_AM"),type("Matrix",null)), null))),orCons(undCons(substcons(tph("_BC"),type("java.lang.Integer",null)),undCons(substcons(tph("_ANG"),tph("_BK")),undCons(equalcons(tph("_AM"),type("java.util.AbstractList",params(tph("_ANG")))), null))),orCons(undCons(substcons(tph("_BC"),type("java.lang.Integer",null)),undCons(equalcons(tph("_AM"),type("java.util.Vector",params(tph("_ANH")))),undCons(substcons(tph("_ANH"),tph("_BK")), null))),orCons(undCons(substcons(tph("_BC"),type("java.lang.Integer",null)),undCons(substcons(tph("_ANG"),tph("_BK")),undCons(equalcons(tph("_AM"),type("java.util.AbstractList",params(tph("_ANG")))), null))),orCons(undCons(substcons(tph("_ANF"),tph("_BK")),undCons(substcons(tph("_BC"),type("java.lang.Integer",null)),undCons(equalcons(tph("_AM"),type("java.util.List",params(tph("_ANF")))), null))),orCons(undCons(substcons(tph("_ANF"),tph("_BK")),undCons(substcons(tph("_BC"),type("java.lang.Integer",null)),undCons(equalcons(tph("_AM"),type("java.util.List",params(tph("_ANF")))), null))),orCons(undCons(substcons(tph("_BC"),type("java.lang.Integer",null)),undCons(substcons(tph("_ANH"),tph("_BK")),undCons(equalcons(tph("_AM"),type("java.util.Vector",params(tph("_ANH")))), null))), null)))))))). +orCons(undCons(substcons(tph("_BC"),type("java.lang.Integer",null)),undCons(substcons(tph("_ANI"),tph("_BR")),undCons(equalcons(tph("_AC"),type("java.util.List",params(tph("_ANI")))), null))),orCons(undCons(substcons(tph("_BC"),type("java.lang.Integer",null)),undCons(equalcons(tph("_AC"),type("Matrix",null)),undCons(substcons(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_BR")), null))),orCons(undCons(substcons(tph("_BC"),type("java.lang.Integer",null)),undCons(equalcons(tph("_AC"),type("Matrix",null)),undCons(substcons(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_BR")), null))),orCons(undCons(substcons(tph("_BC"),type("java.lang.Integer",null)),undCons(substcons(tph("_ANJ"),tph("_BR")),undCons(equalcons(tph("_AC"),type("java.util.AbstractList",params(tph("_ANJ")))), null))),orCons(undCons(equalcons(tph("_AC"),type("java.util.Vector",params(tph("_ANK")))),undCons(substcons(tph("_BC"),type("java.lang.Integer",null)),undCons(substcons(tph("_ANK"),tph("_BR")), null))),orCons(undCons(equalcons(tph("_AC"),type("java.util.Vector",params(tph("_ANK")))),undCons(substcons(tph("_BC"),type("java.lang.Integer",null)),undCons(substcons(tph("_ANK"),tph("_BR")), null))),orCons(undCons(substcons(tph("_BC"),type("java.lang.Integer",null)),undCons(substcons(tph("_ANI"),tph("_BR")),undCons(equalcons(tph("_AC"),type("java.util.List",params(tph("_ANI")))), null))),orCons(undCons(substcons(tph("_BC"),type("java.lang.Integer",null)),undCons(substcons(tph("_ANJ"),tph("_BR")),undCons(equalcons(tph("_AC"),type("java.util.AbstractList",params(tph("_ANJ")))), null))), null)))))))). +orCons(undCons(substcons(tph("_ANM"),tph("_BO")),undCons(equalcons(tph("_BR"),type("java.util.AbstractList",params(tph("_ANM")))),undCons(substcons(tph("_AU"),type("java.lang.Integer",null)), null))),orCons(undCons(substcons(tph("_AU"),type("java.lang.Integer",null)),undCons(equalcons(tph("_BR"),type("Matrix",null)),undCons(substcons(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_BO")), null))),orCons(undCons(equalcons(tph("_BR"),type("java.util.List",params(tph("_ANL")))),undCons(substcons(tph("_ANL"),tph("_BO")),undCons(substcons(tph("_AU"),type("java.lang.Integer",null)), null))),orCons(undCons(equalcons(tph("_BR"),type("java.util.List",params(tph("_ANL")))),undCons(substcons(tph("_ANL"),tph("_BO")),undCons(substcons(tph("_AU"),type("java.lang.Integer",null)), null))),orCons(undCons(substcons(tph("_ANN"),tph("_BO")),undCons(equalcons(tph("_BR"),type("java.util.Vector",params(tph("_ANN")))),undCons(substcons(tph("_AU"),type("java.lang.Integer",null)), null))),orCons(undCons(substcons(tph("_ANM"),tph("_BO")),undCons(equalcons(tph("_BR"),type("java.util.AbstractList",params(tph("_ANM")))),undCons(substcons(tph("_AU"),type("java.lang.Integer",null)), null))),orCons(undCons(substcons(tph("_ANN"),tph("_BO")),undCons(equalcons(tph("_BR"),type("java.util.Vector",params(tph("_ANN")))),undCons(substcons(tph("_AU"),type("java.lang.Integer",null)), null))),orCons(undCons(substcons(tph("_AU"),type("java.lang.Integer",null)),undCons(equalcons(tph("_BR"),type("Matrix",null)),undCons(substcons(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_BO")), null))), null)))))))). +orCons(undCons(substcons(tph("_BO"),type("java.lang.Integer",null)),undCons(equalcons(type("java.lang.Integer",null),tph("_BU")),undCons(substcons(tph("_BK"),type("java.lang.Integer",null)), null))), null). +orCons(undCons(substcons(tph("_BU"),type("java.lang.Integer",null)),undCons(substcons(tph("_BA"),type("java.lang.Integer",null)),undCons(equalcons(type("java.lang.Integer",null),tph("_BV")), null))), null). +orCons(undCons(substcons(tph("_BA"),type("java.util.Vector",params(type("java.lang.Integer",null)))),undCons(equalcons(tph("_AS"),type("Matrix",null)), null)),orCons(undCons(substcons(tph("_BA"),type("java.util.Vector",params(type("java.lang.Integer",null)))),undCons(equalcons(tph("_AS"),type("Matrix",null)), null)),orCons(undCons(equalcons(tph("_AS"),type("java.util.Vector",params(tph("_ANO")))),undCons(substcons(tph("_BA"),tph("_ANO")), null)),orCons(undCons(equalcons(tph("_AS"),type("java.util.Vector",params(tph("_ANO")))),undCons(substcons(tph("_BA"),tph("_ANO")), null)), null)))). +orCons(undCons(substcons(tph("_AS"),type("java.util.Vector",params(type("java.lang.Integer",null)))),undCons(equalcons(tph("_AD"),type("Matrix",null)), null)),orCons(undCons(equalcons(tph("_AD"),type("java.util.Vector",params(tph("_ANP")))),undCons(substcons(tph("_AS"),tph("_ANP")), null)),orCons(undCons(substcons(tph("_AS"),type("java.util.Vector",params(type("java.lang.Integer",null)))),undCons(equalcons(tph("_AD"),type("Matrix",null)), null)),orCons(undCons(equalcons(tph("_AD"),type("java.util.Vector",params(tph("_ANP")))),undCons(substcons(tph("_AS"),tph("_ANP")), null)), null)))). +orCons(undCons(equalcons(tph("_G"),type("java.lang.Integer",null)), null), null). +orCons(undCons(substcons(type("java.lang.Integer",null),tph("_J")),undCons(equalcons(tph("_F"),type("java.util.List",params(tph("_ANS")))), null)),orCons(undCons(equalcons(tph("_F"),type("java.util.AbstractList",params(tph("_ANT")))),undCons(substcons(type("java.lang.Integer",null),tph("_J")), null)),orCons(undCons(substcons(type("java.lang.Integer",null),tph("_J")),undCons(equalcons(tph("_F"),type("java.util.Vector",params(tph("_ANU")))), null)),orCons(undCons(equalcons(tph("_F"),type("Matrix",null)),undCons(substcons(type("java.lang.Integer",null),tph("_J")), null)),orCons(undCons(equalcons(tph("_F"),type("Matrix",null)),undCons(substcons(type("java.lang.Integer",null),tph("_J")), null)),orCons(undCons(substcons(type("java.lang.Integer",null),tph("_J")),undCons(equalcons(tph("_F"),type("java.util.List",params(tph("_ANS")))), null)),orCons(undCons(substcons(type("java.lang.Integer",null),tph("_J")),undCons(equalcons(tph("_F"),type("java.util.Vector",params(tph("_ANU")))), null)),orCons(undCons(equalcons(tph("_F"),type("java.util.AbstractList",params(tph("_ANT")))),undCons(substcons(type("java.lang.Integer",null),tph("_J")), null)), null)))))))). +orCons(undCons(substcons(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(substcons(tph("_ANV"),tph("_N")),undCons(equalcons(tph("_F"),type("java.util.Vector",params(tph("_ANV")))), null))),orCons(undCons(equalcons(tph("_F"),type("Matrix",null)),undCons(substcons(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(substcons(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_N")), null))),orCons(undCons(substcons(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(substcons(tph("_ANV"),tph("_N")),undCons(equalcons(tph("_F"),type("java.util.Vector",params(tph("_ANV")))), null))),orCons(undCons(equalcons(tph("_F"),type("Matrix",null)),undCons(substcons(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(substcons(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_N")), null))), null)))). +orCons(undCons(equalcons(tph("_F"),type("Matrix",null)),undCons(substcons(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(substcons(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_N")), null))),orCons(undCons(equalcons(tph("_F"),type("java.util.Vector",params(tph("_ANX")))),undCons(substcons(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(substcons(tph("_ANX"),tph("_N")), null))),orCons(undCons(equalcons(tph("_F"),type("java.util.Vector",params(tph("_ANX")))),undCons(substcons(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(substcons(tph("_ANX"),tph("_N")), null))),orCons(undCons(equalcons(tph("_F"),type("Matrix",null)),undCons(substcons(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(substcons(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_N")), null))), null)))). +orCons(undCons(equalcons(tph("_F"),type("Matrix",null)),undCons(substcons(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(substcons(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_N")), null))),orCons(undCons(substcons(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(equalcons(tph("_F"),type("Matrix",null)),undCons(substcons(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_N")), null))),orCons(undCons(equalcons(tph("_F"),type("java.util.Vector",params(tph("_ANZ")))),undCons(substcons(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(substcons(tph("_ANZ"),tph("_N")), null))),orCons(undCons(equalcons(tph("_F"),type("java.util.Vector",params(tph("_ANZ")))),undCons(substcons(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(substcons(tph("_ANZ"),tph("_N")), null))), null)))). +orCons(undCons(equalcons(tph("_F"),type("Matrix",null)),undCons(substcons(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(substcons(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_N")), null))),orCons(undCons(substcons(tph("_AOB"),tph("_N")),undCons(substcons(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(equalcons(tph("_F"),type("java.util.Vector",params(tph("_AOB")))), null))),orCons(undCons(substcons(tph("_AOB"),tph("_N")),undCons(substcons(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(equalcons(tph("_F"),type("java.util.Vector",params(tph("_AOB")))), null))),orCons(undCons(substcons(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(equalcons(tph("_F"),type("Matrix",null)),undCons(substcons(type("java.util.Vector",params(type("java.lang.Integer",null))),tph("_N")), null))), null)))). +orCons(undCons(substcons(type("java.lang.Boolean",null),tph("_R")),undCons(substcons(tph("_N"),tph("_AOA")),undCons(equalcons(tph("_S"),type("java.util.Vector",params(tph("_AOA")))), null))),orCons(undCons(substcons(type("java.lang.Boolean",null),tph("_R")),undCons(substcons(tph("_N"),tph("_ANW")),undCons(equalcons(tph("_S"),type("java.util.List",params(tph("_ANW")))), null))),orCons(undCons(substcons(type("java.lang.Boolean",null),tph("_R")),undCons(substcons(tph("_N"),tph("_ANW")),undCons(equalcons(tph("_S"),type("java.util.List",params(tph("_ANW")))), null))),orCons(undCons(substcons(type("java.lang.Boolean",null),tph("_R")),undCons(substcons(tph("_N"),tph("_AOA")),undCons(equalcons(tph("_S"),type("java.util.Vector",params(tph("_AOA")))), null))),orCons(undCons(substcons(type("java.lang.Boolean",null),tph("_R")),undCons(equalcons(tph("_S"),type("Matrix",null)),undCons(substcons(tph("_N"),type("java.util.Vector",params(type("java.lang.Integer",null)))), null))),orCons(undCons(substcons(type("java.lang.Boolean",null),tph("_R")),undCons(equalcons(tph("_S"),type("Matrix",null)),undCons(substcons(tph("_N"),type("java.util.Vector",params(type("java.lang.Integer",null)))), null))),orCons(undCons(substcons(type("java.lang.Boolean",null),tph("_R")),undCons(equalcons(tph("_S"),type("java.util.AbstractList",params(tph("_ANY")))),undCons(substcons(tph("_N"),tph("_ANY")), null))),orCons(undCons(substcons(type("java.lang.Boolean",null),tph("_R")),undCons(equalcons(tph("_S"),type("java.util.AbstractList",params(tph("_ANY")))),undCons(substcons(tph("_N"),tph("_ANY")), null))), null)))))))). +orCons(undCons(equalcons(tph("_U"),type("java.lang.Integer",null)), null), null). +orCons(undCons(substcons(type("java.lang.Integer",null),type("java.lang.Integer",null)),undCons(substcons(tph("_U"),type("java.lang.Integer",null)),undCons(equalcons(type("java.lang.Integer",null),tph("_V")), null))), null). -type("Name", paramList). -type("Name", params()). -params(paramList, tph(a), 1). +subtype(type("java.lang.Boolean",null),type("Object",null)):-subtype(type("java.lang.Boolean",null)). +subtype(type("java.lang.Integer",null),type("java.lang.Number",null)):-subtype(type("java.lang.Integer",null)). +subtype(type("java.lang.Number",null),type("Object",null)):-subtype(type("java.lang.Number",null)). +subtype(type("java.util.Vector",params(XX)),type("Object",null)):-subtype(type("java.util.Vector",params(XX))). +subtype(type("Matrix",null),type("java.util.Vector",params(type("java.util.Vector",params(type("java.lang.Integer",null)))))):-subtype(type("Matrix",null)). + + +%%%%% + +subtype(type("MyPair", params(X, Y)), type("Pair", params(Y, X))) :- subtype(type("MyPair", params(X, Y))). +subtype(type("ArrayList", params(X)), type("List", params(X))) :- subtype(type("ArrayList", params(X))). +subtype(type("List", params(X)), type("Object", null)) :- subtype(type("List", params(X))). +subtype(type("Integer", null), type("Object", null)) :- subtype(type("Integer", null)). +subtype(type("Matrix", null), type("Vector", params(type("Vector", params(type("Integer", null)))))) :- subtype(type("Matrix", null)). +subtype(type("Vector", params(X)), type("Object", null)) :- subtype(type("Vector", params(X))). + + +% Or-Constraints +undCons(A,B) :- orCons(undCons(A,B), null). +undCons(A,B); orCons(C,D) :- orCons(undCons(A,B), orCons(C,D)). +substcons(A,B) :- undCons(substcons(A,B), _). +undCons(B,C) :- undCons(A, undCons(B, C)). + +% undCons +substcons(A,B) :- undCons(substcons(A,B), _). +undCons(C,D) :- undCons(_, undCons(C,D)). + +% Subtyping +subtype(A, A) :- subtype(A, B). % reflexive +subtype(B) :- subtype(A, B). % transitive +subtype(A, C) :- subtype(A, B), subtype(B, C). % transitive +% named Subtyping +namedSubtype(A,B) :- subtype(type(A, AP), type(B, BP)). +% is reflexive and transitive because subtype it stems from subtype + +% generate the subtype relations for every constraint where one is needed: (this could be optimized) +subtype(type(A, P)) :- substcons(_, type(A, P)). +subtype(type(A, P)) :- substcons(type(A, P), _). % subst: subst(tph(A), type(N,P)) :- equalcons(tph(A), type(N, P)). @@ -9,22 +72,91 @@ 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). +substcons(C,B) :- subst(A, B), substcons(C, A). %subst-Equal: -equalcons(B,C) :- subst(A, B), substcons(A, C). +equalcons(B,C) :- subst(A, B), equalcons(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))). equalcons(T, T) :- equalcons(tph(_), type(_, params(T, _, _))). equalcons(T, T) :- equalcons(tph(_), type(_, params(_, T, _))). equalcons(T, T) :- equalcons(tph(_), type(_, params(_, _, T))). +% Subst-Param: +substcons(A, type(C, params(T2))) :- substcons(A, type(C, params(T))), subst(T, T2). +substcons(A, type(C, params(T2, P2))) :- substcons(A, type(C, params(T, P2))), subst(T, T2). +substcons(A, type(C, params(P1, T2))) :- substcons(A, type(C, params(P1, T))), subst(T, T2). +substcons(A, type(C, params(T2, P2, P3))) :- substcons(A, type(C, params(T, P2, P3))), subst(T, T2). +substcons(A, type(C, params(P1, T2, P3))) :- substcons(A, type(C, params(P1, T, P3))), subst(T, T2). +substcons(A, type(C, params( P1, P2, T2))) :- substcons(A, type(C, params(P1, P2, T))), subst(T, T2). + +% match +substcons(type(C, P1), type(D, P2)) :- substcons(tph(A), type(C, P1)), substcons(tph(A), type(D, P2)), namedSubtype(C, D). + +% adopt +substcons(tph(A), type(C,P)) :- substcons(tph(A), tph(B)), substcons(tph(B), type(C,P)). + +% adapt +equalcons(type(D,P3), type(D,P2)) :- substcons(type(C,P), type(D, P2)), subtype(type(C, P), type(D, P3)). + +% reduce +equalcons(P1, PP1) :- equalcons(type(C, params(P1)), type(C, params(PP1))). +equalcons(P1, PP1) :- equalcons(type(C, params(P1, P2)), type(C, params(PP1, PP2))). +equalcons(P2, PP2) :- equalcons(type(C, params(P1, P2)), type(C, params(PP1, PP2))). +equalcons(P1, PP1) :- equalcons(type(C, params(P1, P2, P3)), type(C, params(PP1, PP2, PP3))). +equalcons(P2, PP2) :- equalcons(type(C, params(P1, P2, P3)), type(C, params(PP1, PP2, PP3))). +equalcons(P3, PP3) :- equalcons(type(C, params(P1, P2, P3)), type(C, params(PP1, PP2, PP3))). + +% super +{ equalcons(tph(A), type(D, DP)): subtype(type(C, CP), type(D, DP)) } == 1 :- substcons(type(C, CP), tph(A)). +%equalcons(tph(A), type(C, CP)) :- substcons(type(C, CP), tph(A)), not subtype(type(C, CP),_). + + + % 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)). +hasASubtype(tph(A), type(D,P2)) :- substcons(tph(A), type(C,P)), substcons(tph(A), type(D,P2)), namedSubtype(C, D), C != D. +equalcons(tph(A), type(C,P)) :- substcons(tph(A), type(C,P)), not hasASubtype(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 +tphs( P ) :- equalcons(tph(A), type(C, P)). +sigma(tph(A), type(C,P)) :- equalcons(tph(A), type(C, P)), not tphs(_, P). + +% Fail +:- equalcons(tph(A), type(C, P)), tphs(tph(A), P). % fail for subst + +:- equalcons(type(C, CP), type(D, DP)), C != D. % fail for reduce +:- substcons(type(C, CP), type(D, DP)), not namedSubtype(C, D). % fail for adapt +:- substcons(tph(A), type(D, DP)), substcons(tph(A), type(C, CP)), not namedSubtype(C, D), not namedSubtype(D, C). %Fail for match + +%% Helpers +%tphs: +tphs(tph(P), params(tph(P))) :- tphs( params(tph(P))). +tphs(P) :- tphs( params(type(C, P))). +tphs(tph(A), params(type(C, P))) :- tphs( params(type(C, P))), tphs(tph(A), P). + +tphs(tph(P), params(X, tph(P))) :- tphs( params(X, tph(P))). +tphs(tph(P), params(tph(P), X)) :- tphs( params(tph(P), X)). +tphs(P) :- tphs( params(X, type(C, P))). +tphs(P) :- tphs( params(type(C, P), X)). +tphs(tph(A), params(X, type(C, P))) :- tphs( params(X, type(C, P))), tphs(tph(A), P). +tphs(tph(A), params(type(C, P), X)) :- tphs( params(type(C, P), X)), tphs(tph(A), P). + + +tphs(tph(P), params(tph(P), X, Y)) :- tphs( params(tph(P), X, Y)). +tphs(tph(P), params(X, tph(P), Y)) :- tphs( params(X, tph(P), Y)). +tphs(tph(P), params(X,Y,tph(P))) :- tphs( params(X, Y, tph(P))). +tphs(P) :- tphs( params(type(C, P), X, Y)). +tphs(P) :- tphs( params(X, type(C, P),Y)). +tphs(P) :- tphs( params(X,Y,type(C, P))). +tphs(tph(A), params(type(C, P), X, Y)) :- tphs( params(type(C, P), X, Y)), tphs(tph(A), P). +tphs(tph(A), params(X, type(C, P), Y)) :- tphs( params(X, type(C, P), Y)), tphs(tph(A), P). +tphs(tph(A), params(X, Y, type(C, P))) :- tphs( params(X, Y, type(C, P))), tphs(tph(A), P). + + +#show sigma/2. \ No newline at end of file