If i understand correctly the LHS of a relation may not be (or contain) a use site. I think this means that currently it is not possible to specify a relation between sorts in say Stratego signatures with injections. For example for the following:

	signature constructors
	  : Id -> RuleNames

i would write the following NaBL + TS rule:

  InjDecl(ty, p-ty, _) :-
  where store ty <: p-ty

  InjDecl(ty, p-ty, annos) :
    defines Sort ty
      of cons-annos annos
    refers to Sort p-ty

But this triggers an exception because ty is a use-site and cannot be indexed.

It may be useful to be able to specify relations between defined entities by creating a relation on the use-sites. For now, is there a way i could define a relation for the case above? Thanks.

Submitted by Vlad Vergu on 18 April 2014 at 12:49

Why is ty a use site? According to the NaBL rule, it is a definition site.

You’re right, i posted an old NaBL rule. What is above works but only because the LHS is a Def. The problem is that the NaBL rule above is incorrect in my use case and the LHS needs to be a Ref, namely ty is a Ref.

I can see this desire, but this will not work as long as we work with the index. Base facts are stored in the index, and by this, we need to have a key to look them up. When you want to store a relation for a reference, the key is the resolution task, i.e., unknown at the moment it is stored. Thus, relations on references will only happen if someone comes up with a different index mechanism, which is the solid base all our work is based on so far.

You might find another way to model what you want to achieve here. In SDF3, I model injections as non-unique definitions of constructor Inj(), which is associated with a function type, just as an ordinary constructor. You should be able to do the same for injections in Stratego signatures. The interesting question is how to model this in the type-checking rules for terms, where you don’t have the Inj() constructor available. I assume where definition of Inj(): FunTy(ty1, ty2) does not work in this case. But I would suggest this as the most promising direction.

Are both ty and p-ty references in the new NaBL rule? If p-ty is a definition in the new rule, this might also allow for some alternative approaches.

Thank you for the clarification. Unfortunately both ty and p-ty are references. I’m open to suggestions on how to model this. What i’m trying to model is (a simplified version of) the signatures from Stratego. So i interpret something like:

Foo : Bar -> Baz

as Constructor Foo of type ([Bar], Baz). Corresponding NaBL rule:

  ConsDecl(c, ty*, ty, annos) :
  	defines Constructor c
  	 of type (ty*, ty)
  	 of cons-annos annos

For an injection:

: Bar -> Baz

I interpret this as the referred sort Bar is a subtype of referred sort Baz.

Do you have a suggestion for how to model this? It’s not immediately apparent to me why desugaring to Inj: Bar -> Baz would solve the issue. My only restriction is preserving the Stratego concrete syntax without change.

Guido, Gabriel, no ideas on how i could work around this limitation?

This is a fundamental issue. The only short term solution I see is to establish several analyses passes. Your problem would require first a basic name and type analysis, before you can store relations. I am not sure if this is actually possible for the problem you like to solve.