K-user mailing list

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

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