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.

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

Top-level abstract clafer extending a nested abstract clafer #67

Closed
ross2jd opened this issue May 13, 2015 · 2 comments
Closed

Top-level abstract clafer extending a nested abstract clafer #67

ross2jd opened this issue May 13, 2015 · 2 comments
Assignees
Milestone

Comments

@ross2jd
Copy link

ross2jd commented May 13, 2015

The is a feature request to allow extending nested abstract Clafers. Consider the following example:

abstract Person
    abstract Hand

abstract Hook : Hand

CptHook : Person
    left : Hook
    right : Hand

Currently, this code would not compile as Hook is not nested under Person. It would be nice to be able to say things like

abstract  Hook : Hand

So that large models can be broken into smaller pieces. Semantically this could work if when you had an abstract Clafer with inheritance it would also inherit the relation (if it exists) between the parent and the Clafer being inherited. I.e. in our example:

Person = {(root, _Person)}
Hand = {(_Person, _Hand)}
Hook = {(_Person, _Hook)}
@mantkiew mantkiew added this to the 0.4.1 milestone Jul 23, 2015
@mantkiew mantkiew self-assigned this Jul 23, 2015
@mantkiew mantkiew modified the milestones: 0.4.2, 0.4.1 Sep 8, 2015
@mantkiew
Copy link
Member

My first stab at implementing it reveals a few problems, the biggest one being that I would have to change the analyses to always keep track of the whole inheritance hierarchy of a clafer to determine valid nesting and generate correct output. Currently, the code generated for left is incorrect:

one sig c0_CptHook extends c0_Person
{ r_c0_left : one c0_left
, r_c0_right : one c0_right }
{ r_c0_right in r_c0_Hand }

The correct code should be

one sig c0_CptHook extends c0_Person
{ r_c0_left : one c0_left
, r_c0_right : one c0_right }
{ r_c0_left in r_c0_Hand
  r_c0_right in r_c0_Hand }

The reason that the constraint r_c0_left in r_c0_Hand is missing now is because in order to generate it one must go up to Person, which defines Hand but we only go to Hook, which does not have a parent.

There's onc trick we could do: always interpret abstract top-level clafers which extend nested abstract clafers as actually their siblings. So, our example would actually be represented in IR as

abstract Person
    abstract Hand
    abstract Hook : Hand

that is the real semantics of allowing to define abstract Hook : Hand as a top-level. Doing so, will not require any changes to code analysis nor code generation. It's a simple transformation that can be done after unique ids are generated. The positive is that desugared clafer will show that semantics.

@mantkiew mantkiew changed the title Extending a nested abstract Clafer Top-level abstract clafer extending a nested abstract clafer Sep 30, 2015
@mantkiew
Copy link
Member

Implementation. We execute the transformation in two phases:

  1. in ResolverInheritance.resolveNClafer, we change the parentUID of a top-level abstract clafers to point to the parent of their superClafer. This makes these clafers logically siblings of their super.
  2. in ResolverInheritance.relocateTopLevelAbstractToParents, we physically move the top-level clafers to their respecitive parents. This makes these clafers physically siblings of their super.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants