Creating boundless subtype hierarchy
Hey!
There should be integer type with exact bit width in my language. Therefore I have types like int<1>, int<2>, int<3> and so on. I just defined one concept with an integer attribute. The subtyping hierarchy is as expected int<1> :<=: int<2> :<=: int<3> ...
It's easy to define this as a subtyping rule, which leads on the one hand to the expected behavior. But on the other hand it results to endless type checking run times for some models. This wasn't a big surprise, since I wrote something like 'return int<width + 1>' in the subtyping rule. This will end up in an infinite recursion.
So tried to represent this by a replacement and a comparision rule. But I failed. I don't really understand how this rules a executed compared with the subtyping rule.
Can anybody give me an example how he/she would express something like this in any type rule?
Many thanks!
There should be integer type with exact bit width in my language. Therefore I have types like int<1>, int<2>, int<3> and so on. I just defined one concept with an integer attribute. The subtyping hierarchy is as expected int<1> :<=: int<2> :<=: int<3> ...
It's easy to define this as a subtyping rule, which leads on the one hand to the expected behavior. But on the other hand it results to endless type checking run times for some models. This wasn't a big surprise, since I wrote something like 'return int<width + 1>' in the subtyping rule. This will end up in an infinite recursion.
So tried to represent this by a replacement and a comparision rule. But I failed. I don't really understand how this rules a executed compared with the subtyping rule.
Can anybody give me an example how he/she would express something like this in any type rule?
Many thanks!
Please sign in to leave a comment.
When you for example write the following code, then there is a rule that says: The initializer of a variable declaration has to be a subtype of the declared variable.
The second line will produce the following inequation, that has to be solved by the typesystem.
Your goal is to tell the typesystem, that an int is a subtype of another int, if the width is lower or equal. Or in other words, every inequation like the one in this example with a lower or equal width on the left side should be marked as solved.
An InequationReplacementRule allows you to remove an inequation from the list of unsolved inequation and replace it with others. These new inequations are specified in the rule block.
In your case you simply want to remove the inequation completly, if the width on the left side is lower/equal, therefor just leave the rule block empty.
replacement rule replace_Int applicable for concept = Int as int1 <: concept = Int as int2 custom condition: ()->boolean { int1.width <= int2.width; } rule { <no statements> }Thanks for your reply!
That's the way I've already tried. But things are not so easy as I described above. There are two concept for signed and unsigned integers, where the unsigned concept is a subconcept of the signed one. This reflects also the subtyping hierarchy. And there are also unconstrained types without any width, which are super types of every contrained type.
So the replacement condition is a bit more advanced. After describing this rule, I recognized that it has no influence to the comparison of two types (:~: operation). So I added a comparison rule with the same condition as in the first rule. So I extract the condition to an utility function. Then I could use my types for example in the CastExpression.
But there are still statements where are type errors, when there should not be any, or the way round. I created some test case where I call my utility function directly for some erroneous nodes. The function works as expected but the type system behaves different. Do I make something wrong? Is there any way to debug the typesystem? Perhaps I could promote a minimal example where this behavior can be recognized the next days.
A sample project would make it much easier to help you.