Lesson 1.18: Term Equality and the Ternary Operator
The purpose of this lesson is to introduce how to compare equality of terms in K, and how to put conditional expressions directly into the right-hand side of rules.
One major way you can compare whether two terms are equal in K is to simply
match both terms with a variable with the same name. This will only succeed
in matching if the two terms are equal structurally. However, sometimes this
is impractical, and it is useful to have access to a way to actually compare
whether two terms in K are equal. The operator for this is found in
domains.md in the
module. The operator is
==K and takes two terms of sort
K and returns a
Bool. It returns true if they are equal. This includes equality over builtin
types such as
Set where equality is not purely structural in
nature. However, it does not include any notion of semantic equality over
user-defined syntax. The inverse symbol for inequality is
One way to introduce conditional logic in K is to have two separate rules,
each with a side condition (or one rule with a side condition and another with
owise attribute). However, sometimes it is useful to explicitly write
a conditional expression directly in the right-hand side of a rule. For this
purpose, K defines one more operator in the
K-EQUAL module, which corresponds
to the usual ternary operator found in many languages. Here is an example of its
module LESSON-18 imports INT imports BOOL imports K-EQUAL syntax Exp ::= Int | Bool | "if" "(" Exp ")" Exp "else" Exp [strict(1)] syntax Bool ::= isKResult(K) [function, symbol] rule isKResult(_:Int) => true rule isKResult(_:Bool) => true rule if (B:Bool) E1:Exp else E2:Exp => #if B #then E1 #else E2 #fi endmodule
Note the symbol on the right-hand side of the final rule. This symbol is
B must be of sort
E2 could have been
any sort so long as both were of the same sort, and the sort of the entire
expression becomes equal to that sort. K supports polymorphic built-in
operators, but does not yet allow users to write their own polymorphic
The behavior of this function is to evaluate the Boolean expression to a Boolean, then pick one of the two children and return it based on whether the Boolean is true or false. Please note that it is not a good idea to use this symbol in cases where one or both of the children is potentially undefined (for example, an integer expression that divides by zero). While the default implementation is smart enough to only evaluate the branch that happens to be picked, this will not be true when we begin to do program verification. If you need short circuiting behavior, it is better to use a side condition.
Write a function in K that takes two terms of sort
Kand returns an
Intshould be 0 if the terms are equal and 1 if the terms are unequal.
Modify your solution to Lesson 1.16, Exercise 1 and introduce an
Stmtto the syntax of the language, then implement it using the
#ifsymbol. Make sure to write tests for the resulting interpreter.
Once you have completed the above exercises, you can continue to Lesson 1.19: Debugging with GDB.