Skip to content

Commit 7193b99

Browse files
hyperpolymathclaude
andcommitted
Type checker: Kategoria L1-L3 + L7 linear types + @Budget tracking
typechecker.rs (~2650 lines): - Type IR covering all Kategoria levels (concrete L1-7, extension L8-10) - Three-pass architecture: declaration gathering, type checking, linear verification - L1: primitive inference, binop rules, Harvard violation detection - L2: constructor typing, pattern exhaustiveness, enum registration - L3: unification engine with occurs check, generic instantiation, purity subtyping - L7: linear binding tracking — use exactly once, branch-consistent merging, send_final consumption, exchange handle swap, spawn handle creation - @Budget: token budget as linear quantity, cost deduction per operation, cached branch (0 cost), @neural (0 cost), BudgetExceeded errors - resolve_type_str: recursive-descent parser bridging String→Type IR - Public API: check_program(), infer_expr(), infer_data() typechecker_tests.rs (36 tests, 141 total): - L1: literals, binop rules, Harvard violation - L2: constructor typing, exhaustiveness checking - L3: function calls, unification, purity enforcement - L7: linear use-once/twice/never, branch consistent/inconsistent - Budget: within/exceed, cached zero-cost, neural zero-cost CLI: `oo7 typecheck <file>` command added. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 3b78b5f commit 7193b99

4 files changed

Lines changed: 3618 additions & 5 deletions

File tree

crates/oo7-cli/src/main.rs

Lines changed: 32 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -12,13 +12,15 @@
1212
use oo7_core::ast::*;
1313
use oo7_core::eval::Evaluator;
1414
use oo7_core::parser;
15+
use oo7_core::typechecker;
1516

1617
fn main() {
1718
let args: Vec<String> = std::env::args().collect();
1819

1920
match args.get(1).map(|s| s.as_str()) {
2021
Some("parse") => cmd_parse(&args),
2122
Some("check") => cmd_check(&args),
23+
Some("typecheck") => cmd_typecheck(&args),
2224
Some("eval") => cmd_eval(&args),
2325
Some("demo") => run_demo(),
2426
Some("--help") | Some("-h") | None => print_usage(),
@@ -34,11 +36,12 @@ fn print_usage() {
3436
println!("007 Agent Meta-Language — Reference Evaluator");
3537
println!();
3638
println!("Usage:");
37-
println!(" oo7 parse <file.007> Parse a .007 file and print AST as JSON");
38-
println!(" oo7 check <file.007> Validate syntax (no output on success)");
39-
println!(" oo7 eval <file.007> Parse and evaluate (parse-only for now)");
40-
println!(" oo7 demo Run built-in demo producing decision traces");
41-
println!(" oo7 --help Show this help message");
39+
println!(" oo7 parse <file.007> Parse a .007 file and print AST as JSON");
40+
println!(" oo7 check <file.007> Validate syntax (no output on success)");
41+
println!(" oo7 typecheck <file.007> Type-check a .007 file (L1-3, L7)");
42+
println!(" oo7 eval <file.007> Parse and evaluate (parse-only for now)");
43+
println!(" oo7 demo Run built-in demo producing decision traces");
44+
println!(" oo7 --help Show this help message");
4245
println!();
4346
println!("The telescope is on. We're looking.");
4447
}
@@ -102,6 +105,30 @@ fn cmd_check(args: &[String]) {
102105
}
103106
}
104107

108+
/// `oo7 typecheck <file.007>` — parse and type-check.
109+
fn cmd_typecheck(args: &[String]) {
110+
let source = read_source_file(args);
111+
let path = args.get(2).unwrap();
112+
113+
match parser::parse_program(&source) {
114+
Ok(program) => match typechecker::check_program(&program) {
115+
Ok(()) => {
116+
eprintln!("OK: type check passed");
117+
}
118+
Err(errors) => {
119+
for e in &errors {
120+
eprintln!("Type error: {}", e.message);
121+
}
122+
std::process::exit(1);
123+
}
124+
},
125+
Err(e) => {
126+
eprintln!("{}", format_parse_error(path, &e));
127+
std::process::exit(1);
128+
}
129+
}
130+
}
131+
105132
/// `oo7 eval <file.007>` — parse and evaluate.
106133
///
107134
/// Currently this only parses and reports the structure, since the

crates/oo7-core/src/lib.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,11 @@ pub mod parser;
1919
#[cfg(test)]
2020
mod parser_tests;
2121
pub mod trace;
22+
pub mod typechecker;
2223

2324
// Re-export key types for convenience.
2425
pub use ast::*;
2526
pub use eval::{BranchStrategy, Evaluator, PredicateFirstStrategy, RtValue};
2627
pub use parser::{parse_program, ParseError};
2728
pub use trace::{DecisionTrace, TraceRecord};
29+
pub use typechecker::{check_program, Type, TypeError};

0 commit comments

Comments
 (0)