It’s been a while now since the last post in my little series on *Kalami*, but I’ve finally polished the code for evaluating programmes as I wanted to. Overall, it’s not that different from the `wellformed`

code of the previous post; in fact, the most challenging aspect is how to enumerate all guesses.

As earlier, we’re dealing with *statements*, *conditions*, and *expressions*. The first one is the tricky one, so to start off simple I’ll first look at the other two. The full source code is available in the **evalwoa** branch on GitHub.

Assuming bindings in *environment* `env`

for all identifiers in an **expression** `expr`

, it may be evaluated straight-forwardly by the following recursive function `eval_expr`

:

let rec eval_expr env expr =
match expr with
ExprNumber(n) ->
n
| ExprVariable(id) ->
List.assoc id env
| ExprProduct(expr1, expr2) ->
let val1 = eval_expr env expr1 in
let val2 = eval_expr env expr2 in
val1 * val2
| ExprDivision(expr1, expr2) ->
let val1 = eval_expr env expr1 in
let val2 = eval_expr env expr2 in
val1 / val2
| ExprSum(expr1, expr2) ->
let val1 = eval_expr env expr1 in
let val2 = eval_expr env expr2 in
val1 + val2
| ExprSubtraction(expr1, expr2) ->
let val1 = eval_expr env expr1 in
let val2 = eval_expr env expr2 in
val1 - val2
| ExprPower(expr1, expr2) ->
let val1 = eval_expr env expr1 in
let val2 = eval_expr env expr2 in
power val1 val2

Note first that since `env`

is just a list of pairs binding identifiers to integers

let env = [ (id1, n1); (id2, n2); ... (idk, nk) ];;

we may extract the latter using built-in function `List.assoc`

as in case `ExprVariable`

. Next, note that there’s no built-in function for integer exponentiation, hence the `power`

function used in case `ExprPower`

is implemented in **evaluation.ml** as a tail recursive repeated squaring (initially it was using the naive approach, but since I did do my PhD in crypto, this was one of the small changes needed; see separate file **power.ml** for the various implementations).

Evaluating **condition** `cnd`

is similar, with the small difference that for one reason or another (purist perhaps) I used the prefix notation for function invocation here:

let rec eval_cnd env cnd =
match cnd with
CndTrue ->
true
| CndFalse ->
false
| CndEqual(expr1, expr2) ->
let val1 = eval_expr env expr1 in
let val2 = eval_expr env expr2 in
(=) val1 val2
| CndLessthan(expr1, expr2) ->
let val1 = eval_expr env expr1 in
let val2 = eval_expr env expr2 in
(<) val1 val2
| CndNegation(cnd) ->
let val1 = eval_cnd env cnd in
(not) val1
| CndOr(cnd1, cnd2) ->
let val1 = eval_cnd env cnd1 in
let val2 = eval_cnd env cnd2 in
(||) val1 val2
| CndAnd(cnd1, cnd2) ->
let val1 = eval_cnd env cnd1 in
let val2 = eval_cnd env cnd2 in
(&&) val1 val2

For **statement** `stmt`

it finally gets a bit more interesting. Cases `StmtLet`

and `StmtIf`

are straight-forward, as are `StmtAccept`

and `StmtReject`

which respectively return the current environment and `None`

. However, for a guessing statement it’s a bit more involved. If the guess has an upper bound then we may just try all possibilities as in case `StmtGuessLowerUpperBound`

below. But this will of course not work when no upper bound is specified since an inner guess will prevent outer guesses from ever increasing. As an example, consider programme:

guess x in
guess y in
if x == y+1 then accept
otherwise reject

which has solution `[ ("x", 1); ("y", 0) ]`

, yet if we first let `x=0`

and then use the strategy of enumerating all values for `y`

then we’ll never make it back to incrementing `x`

.

Instead, for a programme with *n* (unbounded) guesses, i.e. guesses without an upper bound, the simple strategy used here is to enumerate all *n*-arity integer tuples in an outer loop, and for each evaluate the main statement with a second environment `guesses`

linking the tuples with the identifiers of the (unbounded) guesses. Statements may then be evaluated as follows, using an initial empty environment `env`

for the main statement:

let rec eval_stmt env guesses stmt =
match stmt with
StmtLet(id, expr, stmt) ->
let expr_value = eval_expr env expr in
let env' = (id, expr_value) :: env in
eval_stmt env' guesses stmt
| StmtIf(cnd, stmt_true, stmt_false) ->
let cnd_value = eval_cnd env cnd in
if cnd_value then
eval_stmt env guesses stmt_true
else
eval_stmt env guesses stmt_false
| StmtGuess(id, stmt) ->
let guess = List.assoc id guesses in
let env' = (id, guess) :: env in
eval_stmt env' guesses stmt
| StmtGuessLowerBound(id, lower_bound_expr, stmt) ->
let lower_bound = eval_expr env lower_bound_expr in
let guess = List.assoc id guesses in
if guess < lower_bound then
None
else
let env' = (id, guess) :: env in
eval_stmt env' guesses stmt
| StmtGuessLowerUpperBound(id, lb_expr, ub_expr, stmt) ->
let lower_bound = eval_expr env lb_expr in
let upper_bound = eval_expr env ub_expr in
let rec helper guess =
let env' = (id, guess) :: env in
let result = eval_stmt env' guesses stmt in
match result with
None ->
if guess < upper_bound then
helper (guess + 1)
else
None
| Some(_) ->
result
in
helper lower_bound
| StmtAccept ->
Some(env)
| StmtReject ->
None

where we see that in cases `StmtGuess`

and `StmtGuessLowerBound`

the guess performed in the outer enumeration is simply added to the environment.

The only thing missing is hence the outer enumeration. First we have a simple function collecting identifiers:

let rec get_unbounded_guesses stmt =
match stmt with
StmtLet(_, _, stmt) ->
get_unbounded_guesses stmt
| StmtIf(_, stmt_true, stmt_false) ->
(get_unbounded_guesses stmt_true)
@ (get_unbounded_guesses stmt_false)
| StmtGuess(id, stmt) ->
id :: (get_unbounded_guesses stmt)
| StmtGuessLowerBound(id, _, stmt) ->
id :: (get_unbounded_guesses stmt)
| StmtGuessLowerUpperBound(_, _, _, stmt) ->
get_unbounded_guesses stmt
| StmtAccept ->
[]
| StmtReject ->
[]

Next is a projection function `project arity number`

performing a one-to-one mapping of an integer into a integer tuple with the given arity (see also **projection.ml**). The code for this gets a bit messy so I won’t give it here, yet the main principle is to partition the digits in `number`

such that for instance:

# project 3 123456;;
- : (int * int) list = [(3, 14); (2, 25); (1, 36)]

It could definitely be done in other ways (as well as optimised), but I vaguely remember going with this simply because of it keeping the projected numbers slightly “balanced”.

Finally, we put this together to obtain:

let eval stmt =
let unb_guess_ids = get_unbounded_guesses stmt in
if (List.length unb_guess_ids) > 0 then
let projector = project (List.length unb_guess_ids) in
let rec helper number =
let projection = projector number in
let guesses = List.combine unb_guess_ids projection in
let result = eval_stmt [] guesses stmt in
match result with
None ->
helper (number + 1)
| Some(_) ->
result
in
helper 0
else
eval_stmt [] [] stmt

that will indeed find a solution to the example programme from above!

While this is now a working interpreter, it does have its shortcomings when used without any kind of static analysis thrown in. For example, on programme:

guess x in
reject

the interpreter will enter an infinite loop, despite the fact that the programme obviously doesn’t have any solutions. Fixing this will be the topic of the next post.