K-user mailing list

["A. Palamariuc" <a.a.palamariuc AT student.rug.nl>]

Dear Sir or Madame,

I am following up on my previous email with some other questions regarding the Tutorial.

Tutorial 4 (IMP++)

Lesson 3:

When trying to run the div.imp program with —search, I get the following error: 

“[Error] Internal: Uncaught exception thrown of type

UnsupportedOperationException.

Please rerun your program with the --debug flag to generate a stack trace, and

file a bug report at https://github.com/kframework/k/issues

(UnsupportedOperationException: null)”

What should I do in this case?

Lesson 5
I have been trying to implement the code that ensures an IMP program does not have multiple declarations for the same variable. The suggestion says to use a new cell, so I was wondering if we are allowed to create as many cells as we want/need in a configuration, or if we need to use some pre-defined ones. Until now, I believed that the <k>, <env>, <store>, <state> cells are pre-defined, but now I am no longer sure of this.

Besides the previously mentioned cells, can one define another cell and name it after their preference? For example, can I have a cell <decl>, which would be used to keep track of declared variables?

I have tried this approach (using a cell called <decl>) in my language definition and everything seems fine, although I cannot figure out how to print an error in case a variable has already been defined. More specifically, I added a side condition to the declaration rule: requires notBool (X in Vars), such that the program gets stuck. However, this is not the desired behaviour. Could you please send me your implementation for this exercise? Below you can find my attempt.

This is the cell I use to store declared variables:  <decl color="blue"> .Set </decl>

This is the declaration rule I currently have:
rule <k> int (X, Xs => Xs); ... </k>

    <env> Rho => Rho[X <- !N:Int] </env>

    <store>... .Map => !N |-> 0 ... </store>

   <decl> Vars:Set (.Set => SetItem(X)) </decl>     requires notBool (X in Vars)

This is the rule for entering/exiting a block:

rule {} => .    [structural]

rule <k> {S} => S ~> pair(Rho, Vars) ... </k>

    <env> Rho </env> [structural]

   <decl> Vars => .Set </decl> 

And this is the rule for restoring the environment and set of variables once a block is exited:

rule <k> pair(Rho, Vars) => . ... </k> <env> _ => Rho </env> <decl> _ => Vars </decl>

Lesson 6

When kompiling, I get the following error:
“[Error] Compiler: LLVM Backend does not support multisets. If you are seeing

this error due to a configuration cell tagged with multiplicity="*", please add

either type="Map" or type="Set". If you still need the collection to not

contain duplicates, it is recommended you also add a unique identifier each

time a cell is created. You can do this with !X:Int.”

I decided to add “type=Set” when creating the cell (<thread multiplicity="*" color="blue" type="Set">) and after I kompile it, I receive the following warning: 

“ld: warning: could not create compact unwind for _step: stack subq instruction is too different from

dwarf stack size”

Could you please tell me what the problem is?

Tutorial 5 (Types)
Lesson 2
When trying to kompile lambda.k, I get an error due to parsing ambiguity for the “rule mu X : T . E => (T -> T) (E[T/X])”. I suppose the parser does not know whether to match (T->T) to Type->Type or Exp->Exp. To make sure I have the correct program, I copied everything from the lambda.k file that can be found on GitHub. Then, I changed the rule by adding the sorts of each term, obtaining “rule mu X : T:Type . E:Exp => (T:Type -> T:Type) (E[T/X])”. Following this modification, lambda.k does now compile, but running any program (factorial-letrec.lambda or ll.lambda) ends into a wrong output - more specifically, the programs get stuck.

Below you can find the aforementioned error:
[Error] Compiler: Had 1 parsing errors.

[Error] Inner Parser: Parsing ambiguity.

1: syntax Type ::= Type "->" Type

   

`_->__LAMBDA_Type_Type_Type`(#SemanticCastToType(#token("T","#KVariable")),#SemanticCastToType(#token("T","#KVariable")))

2: syntax Exp ::= Exp "->" Exp [strict]

   

`_->__LAMBDA_Exp_Exp_Exp`(#SemanticCastToType(#token("T","#KVariable")),#SemanticCastToType(#token("T","#KVariable")))

Source(/Applications/Uni/Year3/Bachelor Project/My tutorials/Tutorial 5 - Type

Systems/LAMBDA/./lambda.k)

Location(50,25,50,41)
Could you please help me solve this issue? Also, in case this problem is not occurring because of an individual mistake, could you update the tutorial to reflect the accurate implementation?

Lesson 3

The programs get stuck while running. The implementation of lambda.k is the one provided on the GitHub page. 

Could you please update the tutorial or send me a working version for the typed lambda language? 

I am looking forward to a response for both emails.

Kind regards,

Anda-Amelia Palamariuc

On 27 May 2020, at 15:41, A. Palamariuc <a.a.palamariuc AT student.rug.nl> wrote:

Dear Sir or Madame,

I have a few questions regarding certain parts of the Tutorial for the K Framework. 

TUTORIAL 1: LAMBDA

Lesson 1 and 2 

I have noticed that in the first lesson of the tutorial, you are defining the syntax of a value by using the term Id, while in lesson 2, you are switching to KVar. 

I was wondering what the difference between the two is and when should I use one or the other.

TUTORIAL 2: IMP

Lesson 4

Here, you propose two exercises: purely-syntactic and uninitialised-variables. I have tried to implement them by following the given suggestions, but I believe my solutions are not valid. Is there a chance you could send me the correct implementations? I believe it would help me better understand how to work with the framework.

TUTORIAL 3: LAMBDA++

Lesson 1

There are 3 proposed exercises: to define a callCC, to define callcc in terms of callCC and the other way around. I have defined callCC as follows:

  syntax Exp ::= "callCC" Exp [strict]
  rule <k> (callCC V:Val => V cc(K)) ~> (K => .) </k>
  rule <k> cc(K) V ~> _ =>  V ~> K </k>

The obtained output matches the one provided on GitHub, although I am unsure whether this was the right approach or not. Would you let me know if my implementation is correct? Moreover, I cannot seem to define callCC and callcc in terms of one another. Could you please provide me the implementation of these constructs?

Lesson 6

The program compiles, but when I try to run factorial-letrec.lambda (or factorial-let-fix.lambda), it fails due to the use of symbol ‘-‘ (Inner Parser: Scanner error: unexpected character sequence ‘-‘.). This error happens only in Lesson 6, where the Syntax and the Semantics of the LAMBDA++ language have been separated. If I run factorial-letrec.lambda with the program from Lesson 5, everything goes as planned. Considering that the only difference between Lesson 5 and Lesson 6 is the separation of modules (Syntax vs. Semantics), I suppose this somehow affects the parser. Could you please address this issue? Why is this happening?

In addition, I noticed that it is no longer possible to generate documentation for the defined languages when kompiling, as neither kompile —pdf nor kdoc —help works.

Is there any other method through which one can obtain the Latex documentation (including annotations, language constructs and so on)?

I am looking forward to hearing from you.

Kind regards,

Anda-Amelia Palamariuc