K-user mailing list

[Traian Florin Șerbănuță <traian.serbanuta AT info.uaic.ro>]

Hi Soha,

The problem you are experienced is that X is actually being renamed (though alpha-conversion) during the evaluation process.  Therefore, the id you have is actually #symId("local",, 1), which is a symbolic identifier.

Now, I guess we could have a behavior of Id2String( #symId("local",, 1)) built-in into K (for example, one which would work for Prolog would be transforming it into "_1") , but it is not certain that you would want that for any language,

Something which worked for me (but it's kind of hackish) was to add customized rules for  

things like #tokenToString (  #symId("local",, 1)) to my definition.

For example, 

rule #tokenToString( #symId("local",, N:Int)) => "_" +String IntToString(N)

should give you a Prolog-like behavior.  The main issue with this is that now String2Id(Id2String(Id)) will not always give you back Id, and this could lead to some problems with alpha-substitution if it gets abused.

hope this helps.

best wishes,

Traian

2014/1/8 soha hussein <husseinsoh AT gmail.com>

Hello,

I am trying to print the derivations for a fix, which is defined as a [binder], and where a lambda in my language is also defined as [binder]. The K tool in this definition is taking care of the scope and alpha renaming of internal Ids, when multiple recursive calls happen.
The problem is that, Ids defined inside say a lambda in a fix gets a new name internally in K, so when i try to print it by finding Id2String(X), where X is an Id, i get : #tokenToString (  #symId("local",, 1)) which i think is the internal representation of the Id. Is there any way i can refer to the X in the outer scope ( or find what this token symId refers to), without having to handle variables myself.


thanks

Soha
_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user