LP-25-26

Rusty V2 Interpreter

A proof-of-concept interpreter for Rusty V2, a statically typed functional-imperative language implemented in Java using JavaCC.

How to Compile

Run the top-level build script:

./makeit.sh

This will generate the parser from the .jj grammar file and compile all Java source files.

How to Run

Interactive mode

./rs2

The interpreter reads programs from standard input. Type your program and end it with ;; to evaluate. Press Ctrl+D to exit.

Run from file

./rs2 hello.rs2

Disable type checker

./rs2 -types

With -types, the static type checker is skipped and programs are evaluated dynamically. Type errors will only be caught at runtime.

./rs2 -types hello.rs2

Both flags can be combined in any order.

Tests

Sample test programs are provided in the directory /examples, covering 16 structural test cases:

• alias_safety.rs2: Verifies safe mutation via address pointers (&a) within valid block scopes.
• closure_escape_ko.rs2: [Should Fail] Aborts compilation if a local stack address escapes its function scope via a return value.
• contravariance.rs2: Validates arrow subtyping by substituting a function with a broader input domain.
• depth_subtype_recursive.rs2: Proves deep structural subtyping constraints on nested fields of matching width.
• depth_width_combined.rs2: Validates passing a variant tag with extra positional arguments, discarding excess data.
• double_alias_ko.rs2: [Should Fail] Rejects extracting the address of a variable unless explicitly declared as mut.
• exhaustive_ko.rs2: [Should Fail] Aborts compilation if a match expression fails to cover all possible enum tags.
• lub_enum_width.rs2: Computes the Least Upper Bound of two enum types sharing a common tag but with different field counts.
• lub_inference.rs2: Infers the exact structural Enum layout returned by a recursive match branch on the fly.
• mut_in_closure.rs2: Permits capturing and mutating local variables in nested closures within safe lifetimes.
• recursive_mut.rs2: Integrates recursive variants, state mutation (:=), and loops via a linked list reversal algorithm.
• recursive_subtype.rs2: Proves structural compatibility between distinct recursive list definitions via co-induction.
• ref_invariance_vs_subtype.rs2: Allows covariance during cell initialization while enforcing reference invariance during mutation.
• subtype_through_alias.rs2: Resolves structural type equivalence between mutually dependent enums without looping.
• type_alias_chain.rs2: Traverses, unwinds, and flattens a deep multi-level chain of nested type aliases.
• width_subtype_function_arg.rs2: Proves arrow parameter contravariance by passing a broad handler into a restricted signature.

Report

A detailed theoretical analysis and architecture overview of the type checker can also be found in the accompanying document report.pdf.