Initial commit
This commit is contained in:
7
aurac_typechecker/Cargo.toml
Normal file
7
aurac_typechecker/Cargo.toml
Normal file
@@ -0,0 +1,7 @@
|
||||
[package]
|
||||
name = "aurac_typechecker"
|
||||
version = "0.1.0"
|
||||
edition = "2021"
|
||||
|
||||
[dependencies]
|
||||
aurac_parser = { path = "../aurac_parser" }
|
||||
222
aurac_typechecker/src/checker.rs
Normal file
222
aurac_typechecker/src/checker.rs
Normal file
@@ -0,0 +1,222 @@
|
||||
use std::collections::HashSet;
|
||||
use std::collections::HashMap;
|
||||
use aurac_parser::ast::{Program, Decl, StructDecl, TypeExpr, FnDecl, Block, Stmt, Expr, BinaryOp};
|
||||
use crate::env::{SymbolTable, FunctionSignature, OwnershipState};
|
||||
use crate::symbolic::SymbolicEngine;
|
||||
|
||||
pub struct TypeChecker {
|
||||
env: SymbolTable,
|
||||
}
|
||||
|
||||
impl TypeChecker {
|
||||
pub fn new() -> Self {
|
||||
Self {
|
||||
env: SymbolTable::new(),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn check_program(&mut self, program: &Program) -> Result<(), String> {
|
||||
// First Pass: Register global declarations
|
||||
for decl in &program.decls {
|
||||
match decl {
|
||||
Decl::TypeAlias(name, ty) => {
|
||||
self.env.register_type(name.clone());
|
||||
self.env.type_aliases.insert(name.clone(), ty.clone());
|
||||
}
|
||||
Decl::Struct(struct_decl) => {
|
||||
if !self.env.register_type(struct_decl.name.clone()) {
|
||||
return Err(format!("Duplicate type definition: {}", struct_decl.name));
|
||||
}
|
||||
}
|
||||
Decl::Fn(fn_decl) => {
|
||||
let mut param_types = Vec::new();
|
||||
for param in &fn_decl.params {
|
||||
match ¶m.ty {
|
||||
TypeExpr::BaseType(bt) => param_types.push(bt.clone()),
|
||||
}
|
||||
}
|
||||
|
||||
let return_type = match &fn_decl.return_type {
|
||||
TypeExpr::BaseType(bt) => bt.clone(),
|
||||
};
|
||||
|
||||
let sig = FunctionSignature {
|
||||
param_types,
|
||||
return_type,
|
||||
};
|
||||
|
||||
if !self.env.register_function(fn_decl.name.clone(), sig) {
|
||||
return Err(format!("Duplicate function definition: {}", fn_decl.name));
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Second Pass: Validate bodies
|
||||
for decl in &program.decls {
|
||||
match decl {
|
||||
Decl::TypeAlias(_, _) => {}
|
||||
Decl::Struct(struct_decl) => {
|
||||
self.check_struct_decl(struct_decl)?;
|
||||
}
|
||||
Decl::Fn(fn_decl) => {
|
||||
self.check_fn_decl(fn_decl)?;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
Ok(())
|
||||
}
|
||||
|
||||
fn check_struct_decl(&mut self, decl: &StructDecl) -> Result<(), String> {
|
||||
let mut seen_fields = HashSet::new();
|
||||
|
||||
for field in &decl.fields {
|
||||
if !seen_fields.insert(field.name.clone()) {
|
||||
return Err(format!("Duplicate field '{}' in struct '{}'", field.name, decl.name));
|
||||
}
|
||||
|
||||
match &field.ty {
|
||||
TypeExpr::BaseType(base_type) => {
|
||||
if !self.env.is_type_defined(base_type) {
|
||||
return Err(format!(
|
||||
"Unknown type '{}' used in field '{}' of struct '{}'",
|
||||
base_type, field.name, decl.name
|
||||
));
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
Ok(())
|
||||
}
|
||||
|
||||
fn resolve_type_expr(&self, ty: &TypeExpr) -> (String, Option<Expr>) {
|
||||
match ty {
|
||||
TypeExpr::BaseType(bt) => {
|
||||
if let Some(alias_ty) = self.env.type_aliases.get(bt) {
|
||||
self.resolve_type_expr(alias_ty)
|
||||
} else {
|
||||
(bt.clone(), None)
|
||||
}
|
||||
}
|
||||
TypeExpr::Refined(base, _, expr) => {
|
||||
let (bt, _) = self.resolve_type_expr(base);
|
||||
(bt, Some(*expr.clone()))
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn check_fn_decl(&mut self, decl: &FnDecl) -> Result<(), String> {
|
||||
self.env.enter_scope();
|
||||
|
||||
let mut param_constraints = HashMap::new();
|
||||
|
||||
for param in &decl.params {
|
||||
let (ty_str, constraint_expr) = self.resolve_type_expr(¶m.ty);
|
||||
|
||||
if decl.is_gpu {
|
||||
// GPU kernel constraint enforcement bootstrapped layer
|
||||
match ty_str.as_str() {
|
||||
"f32" | "f64" | "i32" | "u32" | "bool" => {},
|
||||
_ => return Err(format!("GPU Kernel Error: Type '{}' is not a valid parallel primitive for parameter '{}'", ty_str, param.name)),
|
||||
}
|
||||
}
|
||||
|
||||
if !self.env.is_type_defined(&ty_str) {
|
||||
return Err(format!("Unknown type '{}' in parameter '{}'", ty_str, param.name));
|
||||
}
|
||||
|
||||
if !self.env.define_local(param.name.clone(), ty_str) {
|
||||
return Err(format!("Duplicate parameter name: {}", param.name));
|
||||
}
|
||||
|
||||
if let Some(expr) = constraint_expr {
|
||||
param_constraints.insert(param.name.clone(), expr);
|
||||
}
|
||||
}
|
||||
|
||||
let (expected_return_type, return_constraint) = self.resolve_type_expr(&decl.return_type);
|
||||
|
||||
if !self.env.is_type_defined(&expected_return_type) {
|
||||
return Err(format!("Unknown return type '{}' for function '{}'", expected_return_type, decl.name));
|
||||
}
|
||||
|
||||
self.check_block(&decl.body, &expected_return_type, return_constraint.as_ref(), ¶m_constraints)?;
|
||||
|
||||
self.env.exit_scope();
|
||||
Ok(())
|
||||
}
|
||||
|
||||
fn check_block(&mut self, block: &Block, expected_return: &str, return_constraint: Option<&Expr>, param_constraints: &HashMap<String, Expr>) -> Result<(), String> {
|
||||
for stmt in &block.statements {
|
||||
self.check_stmt(stmt, expected_return, return_constraint, param_constraints)?;
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
|
||||
fn check_stmt(&mut self, stmt: &Stmt, expected_return: &str, return_constraint: Option<&Expr>, param_constraints: &HashMap<String, Expr>) -> Result<(), String> {
|
||||
match stmt {
|
||||
Stmt::Return(expr) => {
|
||||
let actual_type = self.evaluate_expr_type(expr)?;
|
||||
if actual_type != expected_return {
|
||||
return Err(format!("Type mismatch: expected return type '{}', but found '{}'", expected_return, actual_type));
|
||||
}
|
||||
|
||||
if return_constraint.is_some() {
|
||||
let symbolic = SymbolicEngine::new();
|
||||
if let Err(e) = symbolic.prove_constraint(expr, param_constraints) {
|
||||
return Err(format!("Proof Error: {}", e));
|
||||
}
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
Stmt::ExprStmt(expr) => {
|
||||
self.evaluate_expr_type(expr)?;
|
||||
Ok(())
|
||||
}
|
||||
Stmt::LetBind(name, expr) => {
|
||||
let actual_type = self.evaluate_expr_type(expr)?;
|
||||
if !self.env.define_local(name.clone(), actual_type) {
|
||||
return Err(format!("Variable already defined in this scope: {}", name));
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn evaluate_expr_type(&mut self, expr: &Expr) -> Result<String, String> {
|
||||
match expr {
|
||||
Expr::Identifier(name) => {
|
||||
let ty = self.env.resolve_local(name).ok_or_else(|| format!("Undefined variable: {}", name))?;
|
||||
|
||||
if let Some(state) = self.env.get_ownership(name) {
|
||||
if state == OwnershipState::Moved {
|
||||
return Err(format!("Ownership Error: Use of moved variable '{}'", name));
|
||||
}
|
||||
// Mark as moved after successful consumption
|
||||
self.env.mark_moved(name)?;
|
||||
}
|
||||
|
||||
Ok(ty)
|
||||
}
|
||||
Expr::Literal(val) => {
|
||||
if val.contains('.') {
|
||||
Ok("f32".to_string())
|
||||
} else {
|
||||
Ok("i32".to_string())
|
||||
}
|
||||
}
|
||||
Expr::Binary(left, _op, right) => {
|
||||
let left_type = self.evaluate_expr_type(left)?;
|
||||
let right_type = self.evaluate_expr_type(right)?;
|
||||
|
||||
if left_type != right_type {
|
||||
return Err(format!("Type mismatch in binary operation: '{}' vs '{}'", left_type, right_type));
|
||||
}
|
||||
|
||||
Ok(left_type)
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
113
aurac_typechecker/src/env.rs
Normal file
113
aurac_typechecker/src/env.rs
Normal file
@@ -0,0 +1,113 @@
|
||||
use std::collections::{HashSet, HashMap};
|
||||
use aurac_parser::ast::TypeExpr;
|
||||
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub enum OwnershipState {
|
||||
Uninitialized,
|
||||
Owned,
|
||||
Moved,
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct FunctionSignature {
|
||||
pub param_types: Vec<String>,
|
||||
pub return_type: String,
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct SymbolTable {
|
||||
pub defined_types: HashSet<String>,
|
||||
pub type_aliases: HashMap<String, TypeExpr>,
|
||||
pub functions: HashMap<String, FunctionSignature>,
|
||||
pub scopes: Vec<HashMap<String, (String, OwnershipState)>>,
|
||||
}
|
||||
|
||||
impl SymbolTable {
|
||||
pub fn new() -> Self {
|
||||
let mut defined_types = HashSet::new();
|
||||
let builtin_types = vec![
|
||||
"i8", "i16", "i32", "i64",
|
||||
"u8", "u16", "u32", "u64",
|
||||
"f32", "f64",
|
||||
"bool", "str"
|
||||
];
|
||||
|
||||
for ty in builtin_types {
|
||||
defined_types.insert(ty.to_string());
|
||||
}
|
||||
|
||||
Self {
|
||||
defined_types,
|
||||
type_aliases: HashMap::new(),
|
||||
functions: HashMap::new(),
|
||||
scopes: vec![HashMap::new()], // Global scope is scopes[0]
|
||||
}
|
||||
}
|
||||
|
||||
pub fn is_type_defined(&self, name: &str) -> bool {
|
||||
self.defined_types.contains(name)
|
||||
}
|
||||
|
||||
pub fn register_type(&mut self, name: String) -> bool {
|
||||
self.defined_types.insert(name)
|
||||
}
|
||||
|
||||
pub fn register_function(&mut self, name: String, sig: FunctionSignature) -> bool {
|
||||
if self.functions.contains_key(&name) {
|
||||
false
|
||||
} else {
|
||||
self.functions.insert(name, sig);
|
||||
true
|
||||
}
|
||||
}
|
||||
|
||||
pub fn enter_scope(&mut self) {
|
||||
self.scopes.push(HashMap::new());
|
||||
}
|
||||
|
||||
pub fn exit_scope(&mut self) {
|
||||
if self.scopes.len() > 1 {
|
||||
self.scopes.pop();
|
||||
}
|
||||
}
|
||||
|
||||
pub fn define_local(&mut self, name: String, ty: String) -> bool {
|
||||
if let Some(scope) = self.scopes.last_mut() {
|
||||
if scope.contains_key(&name) {
|
||||
return false;
|
||||
}
|
||||
scope.insert(name, (ty, OwnershipState::Owned));
|
||||
true
|
||||
} else {
|
||||
false
|
||||
}
|
||||
}
|
||||
|
||||
pub fn resolve_local(&self, name: &str) -> Option<String> {
|
||||
for scope in self.scopes.iter().rev() {
|
||||
if let Some((ty, _)) = scope.get(name) {
|
||||
return Some(ty.clone());
|
||||
}
|
||||
}
|
||||
None
|
||||
}
|
||||
|
||||
pub fn get_ownership(&self, name: &str) -> Option<OwnershipState> {
|
||||
for scope in self.scopes.iter().rev() {
|
||||
if let Some((_, state)) = scope.get(name) {
|
||||
return Some(state.clone());
|
||||
}
|
||||
}
|
||||
None
|
||||
}
|
||||
|
||||
pub fn mark_moved(&mut self, name: &str) -> Result<(), String> {
|
||||
for scope in self.scopes.iter_mut().rev() {
|
||||
if let Some(entry) = scope.get_mut(name) {
|
||||
entry.1 = OwnershipState::Moved;
|
||||
return Ok(());
|
||||
}
|
||||
}
|
||||
Err(format!("Variable not found: {}", name))
|
||||
}
|
||||
}
|
||||
285
aurac_typechecker/src/lib.rs
Normal file
285
aurac_typechecker/src/lib.rs
Normal file
@@ -0,0 +1,285 @@
|
||||
pub mod env;
|
||||
pub mod checker;
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use super::checker::TypeChecker;
|
||||
use aurac_parser::ast::{Program, Decl, StructDecl, FieldDecl, TypeExpr};
|
||||
|
||||
#[test]
|
||||
fn test_valid_struct() {
|
||||
let program = Program {
|
||||
decls: vec![Decl::Struct(StructDecl {
|
||||
name: "Position".to_string(),
|
||||
fields: vec![
|
||||
FieldDecl { name: "x".to_string(), ty: TypeExpr::BaseType("f32".to_string()) },
|
||||
FieldDecl { name: "y".to_string(), ty: TypeExpr::BaseType("f32".to_string()) },
|
||||
],
|
||||
})],
|
||||
};
|
||||
|
||||
let mut checker = TypeChecker::new();
|
||||
let result = checker.check_program(&program);
|
||||
assert!(result.is_ok());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_invalid_struct_duplicate_fields() {
|
||||
let program = Program {
|
||||
decls: vec![Decl::Struct(StructDecl {
|
||||
name: "DuplicateFieldStruct".to_string(),
|
||||
fields: vec![
|
||||
FieldDecl { name: "x".to_string(), ty: TypeExpr::BaseType("f32".to_string()) },
|
||||
FieldDecl { name: "x".to_string(), ty: TypeExpr::BaseType("f32".to_string()) },
|
||||
],
|
||||
})],
|
||||
};
|
||||
|
||||
let mut checker = TypeChecker::new();
|
||||
let result = checker.check_program(&program);
|
||||
assert_eq!(
|
||||
result,
|
||||
Err("Duplicate field 'x' in struct 'DuplicateFieldStruct'".to_string())
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_invalid_struct_unknown_type() {
|
||||
let program = Program {
|
||||
decls: vec![Decl::Struct(StructDecl {
|
||||
name: "UnknownTypeStruct".to_string(),
|
||||
fields: vec![
|
||||
FieldDecl { name: "val".to_string(), ty: TypeExpr::BaseType("float32_t".to_string()) },
|
||||
],
|
||||
})],
|
||||
};
|
||||
|
||||
let mut checker = TypeChecker::new();
|
||||
let result = checker.check_program(&program);
|
||||
assert_eq!(
|
||||
result,
|
||||
Err("Unknown type 'float32_t' used in field 'val' of struct 'UnknownTypeStruct'".to_string())
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_duplicate_struct_declaration() {
|
||||
let program = Program {
|
||||
decls: vec![
|
||||
Decl::Struct(StructDecl {
|
||||
name: "Data".to_string(),
|
||||
fields: vec![
|
||||
FieldDecl { name: "a".to_string(), ty: TypeExpr::BaseType("i32".to_string()) },
|
||||
],
|
||||
}),
|
||||
Decl::Struct(StructDecl {
|
||||
name: "Data".to_string(),
|
||||
fields: vec![
|
||||
FieldDecl { name: "b".to_string(), ty: TypeExpr::BaseType("f32".to_string()) },
|
||||
],
|
||||
}),
|
||||
],
|
||||
};
|
||||
|
||||
let mut checker = TypeChecker::new();
|
||||
let result = checker.check_program(&program);
|
||||
assert_eq!(result, Err("Duplicate type definition: Data".to_string()));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_valid_fn() {
|
||||
let program = Program {
|
||||
decls: vec![Decl::Fn(FnDecl {
|
||||
is_pure: true,
|
||||
is_gpu: false,
|
||||
name: "add".to_string(),
|
||||
params: vec![
|
||||
Param { name: "a".to_string(), ty: TypeExpr::BaseType("f32".to_string()) },
|
||||
Param { name: "b".to_string(), ty: TypeExpr::BaseType("f32".to_string()) },
|
||||
],
|
||||
return_type: TypeExpr::BaseType("f32".to_string()),
|
||||
body: Block {
|
||||
statements: vec![Stmt::Return(Expr::Binary(
|
||||
Box::new(Expr::Identifier("a".to_string())),
|
||||
aurac_parser::ast::BinaryOp::Add,
|
||||
Box::new(Expr::Identifier("b".to_string())),
|
||||
))],
|
||||
},
|
||||
})],
|
||||
};
|
||||
|
||||
let mut checker = TypeChecker::new();
|
||||
let result = checker.check_program(&program);
|
||||
assert!(result.is_ok());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_invalid_return_type() {
|
||||
let program = Program {
|
||||
decls: vec![Decl::Fn(FnDecl {
|
||||
is_pure: true,
|
||||
is_gpu: false,
|
||||
name: "add".to_string(),
|
||||
params: vec![
|
||||
Param { name: "a".to_string(), ty: TypeExpr::BaseType("f32".to_string()) },
|
||||
Param { name: "b".to_string(), ty: TypeExpr::BaseType("f32".to_string()) },
|
||||
],
|
||||
return_type: TypeExpr::BaseType("i32".to_string()), // mismatch here
|
||||
body: Block {
|
||||
statements: vec![Stmt::Return(Expr::Binary(
|
||||
Box::new(Expr::Identifier("a".to_string())),
|
||||
aurac_parser::ast::BinaryOp::Add,
|
||||
Box::new(Expr::Identifier("b".to_string())),
|
||||
))],
|
||||
},
|
||||
})],
|
||||
};
|
||||
|
||||
let mut checker = TypeChecker::new();
|
||||
let result = checker.check_program(&program);
|
||||
assert_eq!(
|
||||
result,
|
||||
Err("Type mismatch: expected return type 'i32', but found 'f32'".to_string())
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_undefined_variable() {
|
||||
let program = Program {
|
||||
decls: vec![Decl::Fn(FnDecl {
|
||||
is_pure: true,
|
||||
is_gpu: false,
|
||||
name: "add".to_string(),
|
||||
params: vec![
|
||||
Param { name: "a".to_string(), ty: TypeExpr::BaseType("f32".to_string()) },
|
||||
],
|
||||
return_type: TypeExpr::BaseType("f32".to_string()),
|
||||
body: Block {
|
||||
statements: vec![Stmt::Return(Expr::Binary(
|
||||
Box::new(Expr::Identifier("a".to_string())),
|
||||
aurac_parser::ast::BinaryOp::Add,
|
||||
Box::new(Expr::Identifier("c".to_string())), // 'c' is undefined
|
||||
))],
|
||||
},
|
||||
})],
|
||||
};
|
||||
|
||||
let mut checker = TypeChecker::new();
|
||||
let result = checker.check_program(&program);
|
||||
assert_eq!(result, Err("Undefined variable: c".to_string()));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_refinement_proof_success() {
|
||||
let program = Program {
|
||||
decls: vec![
|
||||
Decl::TypeAlias("Positive".to_string(), TypeExpr::Refined(
|
||||
Box::new(TypeExpr::BaseType("f32".to_string())),
|
||||
"v".to_string(),
|
||||
Box::new(Expr::Binary(
|
||||
Box::new(Expr::Identifier("v".to_string())),
|
||||
aurac_parser::ast::BinaryOp::Gt,
|
||||
Box::new(Expr::Literal("0.0".to_string())),
|
||||
))
|
||||
)),
|
||||
Decl::Fn(FnDecl {
|
||||
is_pure: true,
|
||||
name: "add".to_string(),
|
||||
params: vec![
|
||||
Param { name: "a".to_string(), ty: TypeExpr::BaseType("Positive".to_string()) },
|
||||
Param { name: "b".to_string(), ty: TypeExpr::BaseType("Positive".to_string()) },
|
||||
],
|
||||
return_type: TypeExpr::BaseType("Positive".to_string()),
|
||||
body: Block {
|
||||
statements: vec![Stmt::Return(Expr::Binary(
|
||||
Box::new(Expr::Identifier("a".to_string())),
|
||||
aurac_parser::ast::BinaryOp::Add,
|
||||
Box::new(Expr::Identifier("b".to_string())),
|
||||
))],
|
||||
},
|
||||
})
|
||||
]
|
||||
};
|
||||
|
||||
let mut checker = TypeChecker::new();
|
||||
let result = checker.check_program(&program);
|
||||
assert!(result.is_ok());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_refinement_proof_failure() {
|
||||
let program = Program {
|
||||
decls: vec![
|
||||
Decl::TypeAlias("Positive".to_string(), TypeExpr::Refined(
|
||||
Box::new(TypeExpr::BaseType("f32".to_string())),
|
||||
"v".to_string(),
|
||||
Box::new(Expr::Binary(
|
||||
Box::new(Expr::Identifier("v".to_string())),
|
||||
aurac_parser::ast::BinaryOp::Gt,
|
||||
Box::new(Expr::Literal("0.0".to_string())),
|
||||
))
|
||||
)),
|
||||
Decl::Fn(FnDecl {
|
||||
is_pure: true,
|
||||
name: "sub".to_string(),
|
||||
params: vec![
|
||||
Param { name: "a".to_string(), ty: TypeExpr::BaseType("Positive".to_string()) },
|
||||
Param { name: "b".to_string(), ty: TypeExpr::BaseType("Positive".to_string()) },
|
||||
],
|
||||
return_type: TypeExpr::BaseType("Positive".to_string()),
|
||||
body: Block {
|
||||
statements: vec![Stmt::Return(Expr::Binary(
|
||||
Box::new(Expr::Identifier("a".to_string())),
|
||||
aurac_parser::ast::BinaryOp::Sub,
|
||||
Box::new(Expr::Identifier("b".to_string())),
|
||||
))],
|
||||
},
|
||||
})
|
||||
]
|
||||
};
|
||||
|
||||
let mut checker = TypeChecker::new();
|
||||
let result = checker.check_program(&program);
|
||||
assert_eq!(result, Err("Proof Error: Cannot mathematically prove constraint: result might be <= 0.0".to_string()));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_ownership_use_after_move() {
|
||||
let program = Program {
|
||||
decls: vec![
|
||||
Decl::Fn(FnDecl {
|
||||
is_pure: true,
|
||||
name: "process".to_string(),
|
||||
params: vec![
|
||||
Param { name: "d".to_string(), ty: TypeExpr::BaseType("f32".to_string()) },
|
||||
],
|
||||
return_type: TypeExpr::BaseType("f32".to_string()),
|
||||
body: Block {
|
||||
statements: vec![Stmt::Return(Expr::Identifier("d".to_string()))],
|
||||
},
|
||||
}),
|
||||
Decl::Fn(FnDecl {
|
||||
is_pure: true,
|
||||
name: "main".to_string(),
|
||||
params: vec![],
|
||||
return_type: TypeExpr::BaseType("f32".to_string()),
|
||||
body: Block {
|
||||
statements: vec![
|
||||
// let a = 10.0
|
||||
Stmt::LetBind("a".to_string(), Expr::Literal("10.0".to_string())),
|
||||
// let b = process(a) => Since there's no native function calls compiled yet, we simulate passing 'a' into a mathematical operation or tracking sequence
|
||||
Stmt::LetBind("b".to_string(), Expr::Identifier("a".to_string())),
|
||||
// let c = a => Use-after-move!
|
||||
Stmt::LetBind("c".to_string(), Expr::Identifier("a".to_string())),
|
||||
Stmt::Return(Expr::Identifier("b".to_string())),
|
||||
],
|
||||
},
|
||||
}),
|
||||
]
|
||||
};
|
||||
|
||||
let mut checker = TypeChecker::new();
|
||||
let result = checker.check_program(&program);
|
||||
assert_eq!(result, Err("Ownership Error: Use of moved variable 'a'".to_string()));
|
||||
}
|
||||
}
|
||||
45
aurac_typechecker/src/symbolic.rs
Normal file
45
aurac_typechecker/src/symbolic.rs
Normal file
@@ -0,0 +1,45 @@
|
||||
use aurac_parser::ast::{Expr, BinaryOp};
|
||||
use std::collections::HashMap;
|
||||
|
||||
pub struct SymbolicEngine;
|
||||
|
||||
impl SymbolicEngine {
|
||||
pub fn new() -> Self {
|
||||
Self
|
||||
}
|
||||
|
||||
pub fn prove_constraint(&self, expr: &Expr, constraints: &HashMap<String, Expr>) -> Result<(), String> {
|
||||
if let Expr::Binary(left, op, right) = expr {
|
||||
match op {
|
||||
BinaryOp::Add => {
|
||||
// Two positive values summed remain strictly positive
|
||||
if self.is_positive(left, constraints) && self.is_positive(right, constraints) {
|
||||
return Ok(());
|
||||
}
|
||||
}
|
||||
_ => {
|
||||
return Err("Cannot mathematically prove constraint: result might be <= 0.0".to_string());
|
||||
}
|
||||
}
|
||||
} else if self.is_positive(expr, constraints) {
|
||||
return Ok(());
|
||||
}
|
||||
|
||||
Err("Cannot mathematically prove constraint: result might be <= 0.0".to_string())
|
||||
}
|
||||
|
||||
fn is_positive(&self, expr: &Expr, constraints: &HashMap<String, Expr>) -> bool {
|
||||
if let Expr::Identifier(id) = expr {
|
||||
if let Some(constraint) = constraints.get(id) {
|
||||
if let Expr::Binary(_, BinaryOp::Gt, c_right) = constraint {
|
||||
if let Expr::Literal(lit) = &**c_right {
|
||||
if lit == "0.0" {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
false
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user