Warning: preg_match() [function.preg-match]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 1384
Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700
Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707
Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700
Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707
While the grammar from the previous post on parsing puts some restrictions on the form of a valid Kalami programme, it doesn’t reject all invalid programmes. In particular, it doesn’t ensure that all variables are bound (declared) before use. Defining a simple type system to check for this is straight forward, but will also serve to illustrate how easy it is to work with an abstract syntax tree in Caml.
To quickly illustrate the problem, consider programmes such as:
if x == 5 then accept otherwise reject
which are meaningless since x is unbound. Now, since I don’t know any good way to present the rules of the type system here on the blog in the usual visual style of inference rules (see the appendix in my master’s thesis for instance), I’m just going to give the code implementing them. Fortunately though, Caml allows us to express such rules so concisely that not much is lost this way anyway — a legacy of ML (its distant father) being a language for formulating logical rules for theorem provers!
Starting with expressions, we assume that a list definedvars
of variables have already been bound (by outer statements) and by recursion on the structure of expression expr
check that all variables it mentions are in the list. The code looks as follows:
let rec wellformed_expr definedvars expr = match expr with ExprNumber(n) -> true | ExprVariable(id) -> List.mem id definedvars | ExprProduct(expr1, expr2) -> (wellformed_expr definedvars expr1) && (wellformed_expr definedvars expr2) | ExprDivision(expr1, expr2) -> (wellformed_expr definedvars expr1) && (wellformed_expr definedvars expr2) | ExprSum(expr1, expr2) -> (wellformed_expr definedvars expr1) && (wellformed_expr definedvars expr2) | ExprSubtraction(expr1, expr2) -> (wellformed_expr definedvars expr1) && (wellformed_expr definedvars expr2) | ExprPower(expr1, expr2) -> (wellformed_expr definedvars expr1) && (wellformed_expr definedvars expr2)
with the most interesting case being for ExprVariable
where a call to standard library function List.mem
checks the id
is a member of the list. Checking a condition is similar, again assuming a list of variables that have already been bound; notice that it calls the above function for cases CndEqual
and CndLessthan
:
let rec wellformed_cnd definedvars cnd = match cnd with CndTrue -> true | CndFalse -> true | CndEqual(expr1, expr2) -> (wellformed_expr definedvars expr1) && (wellformed_expr definedvars expr2) | CndLessthan(expr1, expr2) -> (wellformed_expr definedvars expr1) && (wellformed_expr definedvars expr2) | CndNegation(cnd) -> wellformed_cnd definedvars cnd | CndOr(cnd1, cnd2) -> (wellformed_cnd definedvars cnd1) && (wellformed_cnd definedvars cnd2) | CndAnd(cnd1, cnd2) -> (wellformed_cnd definedvars cnd1) && (wellformed_cnd definedvars cnd2)
Now, for statements it finally gets slightly more interesting. The function still takes a list definedvars
as input since it calls itself recursively, and hence some variables may be bound by outer statements. But it now also extends this list when a let
– or guess
-statement is encountered; in these cases it also ensures that no variable is re-bound:
let rec wellformed_stmt definedvars stmt = match stmt with StmtLet(id, expr, stmt) -> (not (List.mem id definedvars)) && (wellformed_expr definedvars expr) && (wellformed_stmt (id::definedvars) stmt) | StmtIf(cnd, stmt_true, stmt_false) -> (wellformed_cnd definedvars cnd) && (wellformed_stmt definedvars stmt_true) && (wellformed_stmt definedvars stmt_false) | StmtGuess(id, stmt) -> (not (List.mem id definedvars)) && (wellformed_stmt (id::definedvars) stmt) | StmtGuessLowerBound(id, _, stmt) -> (not (List.mem id definedvars)) && (wellformed_stmt (id::definedvars) stmt) | StmtGuessLowerUpperBound(id, _, _, stmt) -> (not (List.mem id definedvars)) && (wellformed_stmt (id::definedvars) stmt) | StmtAccept -> true | StmtReject -> true
The above functions are all that is needed to perform our validation check: simply invoke wellformed_stmt
on the main programme statement with an empty list, and check that it returns true. We may wrap this in function:
let wellformed stmt = wellformed_stmt [] stmt
in order to hide some of the implementation details.