1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
module
imports
signatures/Poosl-sig
signatures/Common-sig
statics-bool
statics-names
rules // === Are compatible =======
// public
maps compatibleType(list(*), list(*))
: TypeDataClass * TypeDataClass
compatibleType(T1, T2) :- boolCompatibleType(T1, T2) == TRUE().
// private
boolCompatibleTypes maps boolCompatibleType(list(*), list(*)) = list(*)
: TypeDataClass * TypeDataClass -> TYPE_BOOL
boolCompatibleType(T1, T2) = or(subType(T1, T2), subType(T2, T1)).
rules // === Filter compatible =======
// public
: list(TypeDataMethod) * TypeDataClass * list(TypeDataClass) -> list(TypeDataMethod)
filterCompatible(Ts, target, pars) = filterDataMethods(Ts, inputCompatibles(Ts, target, pars)).
// private
: list(TypeDataMethod) * list(TYPE_BOOL) -> list(TypeDataMethod)
filterDataMethods([], []) = [].
filterDataMethods([M|Ms], [TRUE()|Bs]) = [M|filterDataMethods(Ms, Bs)].
filterDataMethods([M|Ms], [FALSE()|Bs]) = filterDataMethods(Ms, Bs).
// private
inputCompatibles maps inputCompatible(list(*), *, *) = list(*)
: TypeDataMethod * TypeDataClass * list(TypeDataClass) -> TYPE_BOOL
inputCompatible(TypeDataMethod(receiver, args, _), target, pars) = forall(boolCompatibleTypes([receiver|args], [target|pars])).
rules // === Subtype =======
// private
: TypeDataClass * TypeDataClass -> TYPE_BOOL
subType(T1, TypeDataClassRoot()) = TRUE().
subType(TypeDataClassRoot(), TypeDataClass(_, _)) = FALSE().
subType(TypeDataClass(s, T), TypeDataClass(s, T)) = TRUE().
subType(TypeDataClass(_, ST1), T2) = subType(ST1, T2).
rules // === Greatest Common Ancestor =======
// public
: list(TypeDataClass) -> TypeDataClass
gcaList([T|Ts]) = gcaListImpl(T, Ts).
gcaList([]) = TypeDataClassRoot(). // Only defined to avoid follow-up errors
// private
: TypeDataClass * list(TypeDataClass) -> TypeDataClass
gcaListImpl(G, []) = G.
gcaListImpl(G, [T|Ts]) = gcaListImpl(gca(G, T), Ts).
// public
: TypeDataClass * TypeDataClass -> TypeDataClass
gca(T1, T2) = lastTDC(largestCommonPrefixTDC(reverseAncestors(T1), reverseAncestors(T2))).
rules
// private
: TypeDataClass -> list(TypeDataClass)
reverseAncestors(T) = reverseAncestorsImpl(T, []).
// private
: TypeDataClass * list(TypeDataClass) -> list(TypeDataClass)
reverseAncestorsImpl(TypeDataClassRoot(), Rs) = Rs.
reverseAncestorsImpl(TypeDataClass(s, T), Rs) = reverseAncestorsImpl(T, [TypeDataClass(s, T) | Rs]).
rules
// private
: list(TypeDataClass) * list(TypeDataClass) -> list(TypeDataClass)
largestCommonPrefixTDC([T|xs], [T|ys]) = [T|largestCommonPrefixTDC(xs, ys)].
largestCommonPrefixTDC(xs, ys) = [].
// private
: list(TypeDataClass) -> TypeDataClass
lastTDC([x]) = x.
lastTDC([x|[y|zs]]) = lastTDC([y|zs]).
|