1
0

New Algorithm with Matrix input

This commit is contained in:
JanUlrich 2024-06-19 23:15:52 +02:00
parent cb99c79213
commit 33b4710dac

View File

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