Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fixes for overloadedAType in AType.rsc #16

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

Fixes for overloadedAType in AType.rsc #16

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
055b709
Changed the definitions of asubtype, aglb and alub on the cases for o…
jurgenvinju Jun 24, 2024
f7204e1
Update AType.rsc
jurgenvinju Jul 3, 2024
8338aec
Update AType.rsc
jurgenvinju Jul 3, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
73 changes: 66 additions & 7 deletions src/org/rascalmpl/core/library/lang/rascalcore/check/AType.rsc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,14 +29,17 @@ This function documents and implements the subtype relation of Rascal's type sys
bool asubtype(tvar(s), AType r) {
throw TypeUnavailable();
}

@synopis{optimized definition of asubtype}
default bool asubtype(AType l, AType r){
switch(r){
case l:
return true;
case tvar(_):
throw TypeUnavailable();
case overloadedAType(overloads):
return isEmpty(overloads) ? asubtype(l, avoid()) : any(<_, _, tp> <- overloads, asubtype(l, tp));
return asubtype(l, (\avoid() | alub(tp) | <_, _, tp> <- overloads));
// return isEmpty(overloads) ? asubtype(l, avoid()) : any(<_, _, tp> <- overloads, asubtype(l, tp));
case avalue():
return true;
case anum():
Expand Down Expand Up @@ -108,9 +111,19 @@ bool asubtypeParam(p1:aparameter(str n1, AType b1, closed=true), AType r) {
return res;
}

bool asubtype(overloadedAType(overloads), AType r) = isEmpty(overloads) ? asubtype(avoid(), r) : any(<_, _, tp> <- overloads, asubtype(tp, r));
@synopsis{Left-hand side case for overloadedAType mirrors right-hand-side case}
@description{
To achieve the properties of a type-lattice asubtype must be transitive, and so it can not
pick the best element from the overloadeds. It must first unify the overloads with lub
to achieve transitivity. See the optimized base-case of ((asubtype)) for an explanation.
}
bool asubtype(overloadedAType(overloads), AType r) = asubtype((\avoid() | lub(it, tp) | <_, _, tp> <- overloads));
// isEmpty(overloads) ? asubtype(avoid(), r) : any(<_, _, tp> <- overloads, asubtype(tp, r));

@synopsis{avoid is the bottom type, it is a subtype of every type, even itself.}
bool asubtype(avoid(), AType _) = true;

@synopsis{avalue is the top type, every type is its subtype, even itself.}
bool asubtype(AType _, avalue()) = true;

bool asubtype(ac:acons(AType a, list[AType] ap, list[Keyword] _), AType b){
Expand All @@ -119,24 +132,31 @@ bool asubtype(ac:acons(AType a, list[AType] ap, list[Keyword] _), AType b){
return comparableList(ap, bp);
case adt: aadt(str _, list[AType] _, _):
return asubtype(a,adt);
// TODO: this is a possible bug. Something is not both a tree node and the function that constructs that tree node.
case afunc(a,list[AType] bp, list[Keyword] _):
return comparableList(ap, bp);
// TODO: or otherwise this is a bug. Something is not both a tree node and the function that constructs that tree node.
case anode(_):
return true;
// TODO: same here. is an acons a tree node or the function that constructs it? I'd say the first, but then its _not_ the latter.
case afunc(AType b, list[AType] bp, list[Keyword] _):
return asubtype(a, b) && comparableList(ap, bp);
// TODO: this is a different bug. \start sorts wrap other sorts with a rule. The types are not substitutable.
case \start(AType t):
return asubtype(ac, t);
}
fail;
}

// TODO A production is not a type, but if it would be then definitely _not_ a subtype of start
bool asubtype(ap: aprod(AProduction p), AType b){
switch(b){
case aprod(AProduction q):
return asubtype(p.def, q.def);
// TODO: this is a bug: to make a start(t) you have to wrap the t with a start(t) production. One is not a substitute for the other
case \start(AType t):
return asubtype(ap, t);
// TODO: why is conditional wired in here? Every conditional sort is an alias for the non-terminal it wraps in the type-system.
case conditional(AType t, _):
return asubtype(ap, t);
case AType t:
Expand All @@ -149,18 +169,22 @@ bool asubtype(adt:aadt(str n, list[AType] l, SyntaxRole sr), AType b){
switch(b){
case anode(_):
return true;
// TODO: bug: an AST can never be a sub-type of a constructor. A constructor is more specific not the same.
// this code is probably dead because we can not type in constructor types in Rascal?
case acons(AType a, list[AType] _, list[Keyword] _):
return asubtype(adt, a);
case aadt(n, list[AType] r, _):
return asubtypeList(l, r);
case aadt("Tree", _, _):
if(isConcreteSyntaxRole(sr)) return true;
// TODO start bug like above
case \start(AType t):
if(isConcreteSyntaxRole(sr)) return asubtype(adt, t);
}
fail;
}

// TODO: probable bug: \start ryles must wrap something with a production to become start. The types are not substitutable.
bool asubtype(\start(AType a), AType b) = asubtype(a, b);

bool asubtype(i:\iter(AType s), AType b){
Expand All @@ -177,6 +201,7 @@ bool asubtype(i:\iter(AType s), AType b){
return asubtype(s,t) && isEmpty(removeLayout(seps));
case \iter-star-seps(AType t, list[AType] seps):
return asubtype(s,t) && isEmpty(removeLayout(seps));
// TODO: start bug
case \start(AType t):
return asubtype(i, t);
}
Expand All @@ -197,6 +222,7 @@ bool asubtype(i:\iter-seps(AType s, list[AType] seps), AType b){
return asubtype(s,t) && isEmpty(removeLayout(seps));
case \iter-star-seps(AType t, list[AType] seps2):
return asubtype(s,t) && asubtypeList(removeLayout(seps), removeLayout(seps2));
// TODO: start bug
case \start(AType t):
return asubtype(i, t);
}
Expand All @@ -213,6 +239,7 @@ bool asubtype(i:\iter-star(AType s), AType b){
return asubtype(s, t);
case \iter-star-seps(AType t, list[AType] seps):
return asubtype(s,t) && isEmpty(removeLayout(seps));
// TODO: start bug
case \start(AType t):
return asubtype(i, t);
}
Expand All @@ -227,6 +254,7 @@ bool asubtype(i:\iter-star-seps(AType s, list[AType] seps), AType b){
return true;
case \iter-star-seps(AType t, list[AType] seps2):
return asubtype(s,t) && asubtypeList(removeLayout(seps), removeLayout(seps2));
// TODO: start bug
case \start(AType t):
return asubtype(i, t);
}
Expand Down Expand Up @@ -255,6 +283,7 @@ bool asubtype(conditional(AType s, _), AType r /*conditional(AType t, _)*/) {
// bool asubtype(AType s, \opt(AType t)) = subtype(s,t);
// bool asubtype(AType s, \alt({AType t, *_}) = true when subtype(s, t); // backtracks over the alternatives

// TODO: why are these commented out? These are correct.
//bool asubtype(aint(), anum()) = true;
//bool asubtype(arat(), anum()) = true;
//bool asubtype(areal(), anum()) = true;
Expand Down Expand Up @@ -314,8 +343,9 @@ bool asubtype(AType l:afunc(AType a, list[AType] ap, list[Keyword] _), AType r){
case acons(b,list[AType] bp, list[Keyword] _):
return asubtype(a, b) && comparableList(ap, bp);
case afunc(AType b, list[AType] bp, list[Keyword] _): {
// note that comparability is enough for function argument sub-typing due to pattern matching semantics
// note that pair-wise parameter comparability is enough for function argument sub-typing due to pattern matching semantics
ares = asubtype(a,b);

bres = comparableList(ap, bp);
//println("asubtype(<l>, <r>) =\> <ares>, <bres>");
return ares && bres;
Expand All @@ -341,8 +371,10 @@ bool asubtype(a:anode(list[AType] l), AType b){
switch(b){
case anode(_):
return true;
// TODO: what is a parameterized `node` type?
case anode(list[AType] r):
return l <= r;
// TODO start bug
case \start(t):
return asubtype(a, t);
}
Expand All @@ -356,20 +388,26 @@ bool asubtype(l:\achar-class(_), AType r){
case \achar-class(_): {
if(l.ranges == r.ranges)
return true;
// TODO bug: this does not implement sub-class semantics. There could be more left `[a-z] <: [a-zA-Z]`
// the run-time implements sub-class semantics explicitly making use of the ordering and non-overlapping
// guarantees of the ranges.
if(difference(r, l) == \achar-class([]))
return false;
return true;
}
case aadt("Tree", _, _):
return true; // characters are Tree instances
// TODO start bug
case \start(t):
return asubtype(l, t);
}
fail;
}

// TODO: bug achar is not a type in Rascal. only singleton character classes [a]
bool asubtype(l:\achar-class(list[ACharRange] _), achar(int c)) = l == \achar-class([arange(c,c)]);

// TODO: bug achar is not a type in Rascal. only singleton character classes [a]
bool asubtype(achar(int c), \achar-class(list[ACharRange] ranges))
= difference(ranges, [arange(c,c)]) == [arange(c,c)];

Expand Down Expand Up @@ -515,11 +553,15 @@ default AType alub(AType s, AType t)

AType alub(atypeList(ts1), atypeList(ts2)) = atypeList(alubList(ts1, ts2));


@synopsis{in alub, an overloadedAType is always represented by the least covering type of the constituents}
AType alub(overloadedAType(overloads), AType t2)
= isEmpty(overloads) ? t2 : alub((avalue() | aglb(it, tp) | <_, _, tp> <- overloads), t2);
= alub((\avoid() | alub(it, tp) | <_, _, tp> <- overloads), t2);
// = isEmpty(overloads) ? t2 : alub((avalue() | aglb(it, tp) | <_, _, tp> <- overloads), t2);

AType alub(AType t1, overloadedAType(overloads))
= isEmpty(overloads) ? t1 : alub(t1, (avalue() | aglb(it, tp) | <_, _, tp> <- overloads));
= alub(t1, (\avoid() | alub(it, tp) | <_, _, tp> <- overloads));
// = isEmpty(overloads) ? t1 : alub(t1, (avalue() | aglb(it, tp) | <_, _, tp> <- overloads));

AType alub(avalue(), AType t) = avalue();
AType alub(AType s, avalue()) = avalue();
Expand Down Expand Up @@ -585,20 +627,28 @@ AType alub(acons(AType lr, list[AType] lp, list[Keyword] lkw), acons(AType rr, l
return avalue();
}

// TODO: bug! if acons is an instance of an ADT node, then it can not also be a function. The lub would be value().
// If on the other hand acons is indeed a constructor function that builds a constructor tree, then this is correct
// and we need to change the definition of `asubtype`
AType alub(acons(AType lr, list[AType] lp, list[Keyword] lkw), afunc(AType rr, list[AType] rp, list[Keyword] rkw)) {
if(size(lp) == size(rp)){
return afunc(alub(lr,rr), alubList(lp, rp), lkw + (rkw - lkw)); // TODO do we want to propagate the keyword parameters?
} else
return avalue();
}

// TODO: bug! if acons is an instance of an ADT node, then it can not also be a function. The lub would be value().
// If on the other hand acons is indeed a constructor function that builds a constructor tree, then this is correct
// and we need to change the definition of `asubtype`
AType alub(afunc(AType lr, list[AType] lp, list[Keyword] lkw), acons(AType rr, list[AType] rp, list[Keyword] rkw)) {
if(size(lp) == size(rp)){
return afunc(alub(lr,rr), alubList(lp, rp), lkw + (rkw - lkw)); // TODO how do we want to propagate the keyword parameters?
} else
return avalue();
}

// TODO: bug. here we see again that acons plays two roles at the same time, both as a type of tree nodes and
// as the function that constructs the same tree nodes.
AType alub(acons(AType a, list[AType] lp, list[Keyword] _), a2:aadt(str n, list[AType] rp, SyntaxRole _)) = alub(a,a2);
AType alub(acons(AType _, list[AType] _, list[Keyword] _), anode(_)) = anode([]);

Expand Down Expand Up @@ -706,11 +756,20 @@ public AType aglb(arel(AType s), aset(AType t)) = aset(aglb(atuple(s), t));

AType aglb(arel(atypeList(list[AType] l)), arel(atypeList(list[AType] r))) = size(l) == size(r) ? arel(atypeList(aglbList(l, r))) : aset(avalue());

@synopsis{Also for glb, an overloadedType is represented by the lub of its constituents.}
@description{
See ((asubtype)) for an explanation. An overloadedAType is not really a type in Rascal;
it is an intermediate representation of overloaded functions (multiple functions with the same name) used by the type-checker and
the compiler. In Rascal's type system, names or expressions that refer to multiple functions have the lub function-type of the
respective functions. If we compute with that, then subtype and lub keep their algebraic properties as a finite lattice.
}
AType aglb(overloadedAType(overloads), AType t2)
= isEmpty(overloads) ? t2 : aglb((avoid() | alub(it, tp) | <_, _, tp> <- overloads), t2);
= aglb((\avoid() | alub(it, tp) | <_, _, tp> <- overloads), t2);
// = isEmpty(overloads) ? t2 : aglb((avoid() | alub(it, tp) | <_, _, tp> <- overloads), t2);

AType aglb(AType t1, overloadedAType(overloads))
= isEmpty(overloads) ? t1 : aglb(t1, (avoid() | alub(it, tp) | <_, _, tp> <- overloads));
= aglb(t1, (\avoid() | alub(it, tp) | <_, _, tp> <- overloads));
// = isEmpty(overloads) ? t1 : aglb(t1, (avoid() | alub(it, tp) | <_, _, tp> <- overloads));

public AType aglb(alist(AType s), alist(AType t)) = alist(aglb(s, t));
public AType aglb(alist(AType s), alrel(AType t)) = alist(aglb(s,atuple(t)));
Expand Down