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.