Lesson 1.2: Basics of Functional K
The purpose of this lesson is to explain the basics of productions and rules in K. These are two types of K sentences. A K file consists of one or more requires or modules in K. Each module consists of one or more imports or sentences. For more information on requires, modules, and sentences, refer to Lesson 1.4. However, for the time being, just think of a module as a container for sentences, and don't worry about requires or imports just yet.
Our first K program
To start with, input the following program into your editor as file
module LESSON-02-A syntax Color ::= Yellow() | Blue() syntax Fruit ::= Banana() | Blueberry() syntax Color ::= colorOf(Fruit) [function] rule colorOf(Banana()) => Yellow() rule colorOf(Blueberry()) => Blue() endmodule
Save this file and then run:
kompile is K's compiler. By default, it takes a program or specification
written in K and compiles it into an interpreter for that input. Right now we
are compiling a single file. A set of K files that are compiled together are
called a K definition. We will cover multiple file K definitions later on.
kompile will output a directory containing everything needed to execute
programs and perform proofs using that definition. In this case,
(by default) create the directory
lesson-02-a-kompiled under the current
Now, save the following input file in your editor as
banana.color in the same
We can now evaluate this K term by running (from the same directory):
krun will use the interpreter generated by the first call to
execute this program.
You will get the following output:
<k> Yellow ( ) ~> . </k>
For now, don't worry about the
~> . portions of this
You can also execute small programs directly by specifying them on the command line instead of putting them in a file. For example, the same program above could also have been executed by running the following command:
Now, let's look at what this definition and program did.
Productions, Constructors, and Functions
The first thing to realize is that this K definition contains 5 productions.
Productions are introduced with the syntax keyword, followed by a sort,
followed by the operator
::= followed by the definition of one or more
productions themselves, separated by the
| operator. There are different
types of productions, but for now we only care about constructors and
functions. Each declaration separated by the
| operator is individually
a single production, and the
| symbol simply groups together productions that
have the same sort. For example, we could equally have written an identical K
definition like so:
module LESSON-02-B syntax Color ::= Yellow() syntax Color ::= Blue() syntax Fruit ::= Banana() syntax Fruit ::= Blueberry() syntax Color ::= colorOf(Fruit) [function] rule colorOf(Banana()) => Yellow() rule colorOf(Blueberry()) => Blue() endmodule
module LESSON-02-C syntax Color ::= Yellow() | Blue() | colorOf(Fruit) [function] syntax Fruit ::= Banana() | Blueberry() rule colorOf(Banana()) => Yellow() rule colorOf(Blueberry()) => Blue() endmodule
Each of these types of productions named above has the same underlying syntax,
but context and attributes are used to distinguish between the different
types. Tokens, brackets, lists, macros, aliases, and anywhere productions will
be covered in a later lesson, but this lesson does introduce us to constructors
constructors. You can think of a constructor like a constructor for an
algebraic data type, if you're familiar with a functional language. The data
type itself is the sort that appears on the left of the
::= operator. Sorts
in K consist of uppercase identifiers.
Constructors can have arguments, but these ones do not. We will cover the
syntax of productions in detail in the next lesson, but for now, you can write
a production with no arguments as an uppercase or lowercase identifier followed
A function is distinguished from a constructor by the presence of the function attribute. Attributes appear in a comma separated list between square brackets after any sentence, including both productions and rules. Various attributes with built-in meanings exist in K and will be discussed throughout the tutorial.
krun to compute the return value of the
colorOf function on a
Rules, Matching, and Variables
Functions in K are given definitions using rules. A rule begins with the
keyword and contains at least one rewrite operator. The rewrite operator
is represented by the syntax
=>. The rewrite operator is one of the built-in
productions in K, and we will discuss in more detail how it can be used in
future lessons, but for now, you can think of a rule as consisting of a
left-hand side and a right-hand side, separated by the rewrite
operator. On the left-hand side is the name of the function and zero or more
patterns corresponding to the parameters of the function. On the right-hand
side is another pattern. The meaning of the rule is relatively simple, having
defined these components. If the function is called with arguments that
match the patterns on the left-hand side, then the return value of the
function is the pattern on the right-hand side.
For example, in the above example, if the argument of the
Banana(), then the return value of the function is
So far we have introduced that a constructor is a type of pattern in K. We will introduce more complex patterns in later lessons, but there is one other type of basic pattern: the variable. A variable, syntactically, consists of an uppercase identifier. However, unlike a constructor, a variable will match any pattern with one exception: Two variables with the same name must match the same pattern.
Here is a more complex example (
module LESSON-02-D syntax Container ::= Jar(Fruit) syntax Fruit ::= Apple() | Pear() syntax Fruit ::= contentsOfJar(Container) [function] rule contentsOfJar(Jar(F)) => F endmodule
Here we see that
Jar is a constructor with a single argument. You can write a
production with multiple arguments by putting the sorts of the arguments in a
comma-separated list inside the parentheses.
In this example,
F is a variable. It will match either
The return value of the function is created by substituting the matched
values of all of the variables into the variables on the right-hand side of
To demonstrate, compile this definition and execute the following program with krun:
You will see when you run it that the program returns
Apple(), because that
is the pattern that was matched by
- Extend the definition in
lesson-02-a.kwith the addition of blackberries and kiwis. For simplicity, blackberries are black and kiwis are green. Then compile your definition and test that your additional fruits are correctly handled by the
- Create a new definition which defines an outfit as a multi-argument
constructor consisting of a hat, shirt, pants, and shoes. Define a new sort,
Boolean, with two constructors, true and false. Each of hat, shirt, pants, and shoes will have a single argument (a color), either black or white. Then define an
outfitMatchingfunction that will return true if all the pieces of the outfit are the same color. You do not need to define the case that returns false. Write some tests that your function behaves the way you expect.
Once you have completed the above exercises, you can continue to Lesson 1.3: BNF Syntax and Parser Generation.