K-user mailing list

["Rosu, Grigore" <grosu AT illinois.edu>]

Unfortunately, there is no manual yet.  The tutorial is the best material to learn K.

In your first example, as you saw, K didn't know where to get the `Id` sort from.  It is defined in the prelude. You can define your own Ids if you do not like those in the prelude, but take a look at how they are defined in the prelude first to understand the syntax of the lexer.

In your second example, K expects one module in your defintion which has the same name as the file: lambda.k tells K that it should look for module LAMBDA.  Somewhat similar to Java.  Otherwise it cannot know which of the modules is the main one.

Grigore

 

 

---

From: dongbiao830415 AT foxmail.com [dongbiao830415 AT foxmail.com]
Sent: Saturday, July 22, 2017 6:48 PM
To: k-user
Subject: [[K-user] ] Error while compiling lambda.k

When using kompile(runtimeverification/k), it fails to compile the lambda.k(a very simple example).

cat lambda.k

[root@localhost hello]# cat lambda.k 
// Copyright (c) 2012-2016 K Team. All Rights Reserved.
module LAMBDA-SYNTAX
  syntax Val ::= Id
               | "lambda" Id "." Exp
  syntax Exp ::= Val
               | Exp Exp      [left]
               | "(" Exp ")"  [bracket]
endmodule

(1) kompile --no-prelude lambda.k. Output:

[root@localhost hello]# kompile --no-prelude lambda.k 
[Error] Compiler: Could not find sorts: [Id]
	Source(/root/src/c-semantics/hello/./lambda.k)
	Location(4,18,4,19)

(2) kompile lambda.k. Output:

[root@localhost hello]# kompile lambda.k
[Error] Compiler: Could not find main module with name LAMBDA in definition.
Use --main-module to specify one.

I don't know what the reason is.
Who has the latest K manual?
Thank you.

---

dongbiao830415 AT foxmail.com