Arrays in Frml

Previous posts in this series introduced Frml, then explained how it checks simplar scalar code, handles contracts between functions, and deals with loops. This post shows how Frml handles arrays. What We’re Doing A minimal array program is: fn main() -> Int { let a: Array<Int> = [2, 3, 5]; assert a[2] == 5; return length(a); } The array type checker subclasses the loop type checker and adds visitors for the array syntax. Everything scalar and every while loop is checked exactly as before; the new visitors only handle array nodes. Array Access visit_ExprArrayAccess checks two things: the expression being indexed must have an array type, and the index must have type Int. It then returns the array’s element type. def visit_ExprArrayAccess(self, expr, expected, allow_old, result_type): arr = expr.array.accept(self, None, allow_old, result_type) FrmlTypeError.fail( not arr.is_array(), f"array access expects an array but found {arr}", expr.pos, ) idx = expr.index.accept(self, None,…