Starting typechecking work again
This commit is contained in:
parent
f3f1dcc0a4
commit
170cf349d7
@ -6,7 +6,7 @@ use crate::util::ScopeStack;
|
|||||||
pub type TypeName = Rc<String>;
|
pub type TypeName = Rc<String>;
|
||||||
|
|
||||||
pub struct TypeContext<'a> {
|
pub struct TypeContext<'a> {
|
||||||
variable_map: ScopeStack<'a, Rc<String>, Type<TVar>>,
|
variable_map: ScopeStack<'a, Rc<String>, ()>,
|
||||||
evar_count: u32
|
evar_count: u32
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -22,6 +22,7 @@ impl TypeError {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/*
|
||||||
/// `Type` is parameterized by whether the type variables can be just universal, or universal or
|
/// `Type` is parameterized by whether the type variables can be just universal, or universal or
|
||||||
/// existential.
|
/// existential.
|
||||||
#[derive(Debug, Clone)]
|
#[derive(Debug, Clone)]
|
||||||
@ -104,6 +105,7 @@ impl TConst {
|
|||||||
TConst::User(Rc::new(name.to_string()))
|
TConst::User(Rc::new(name.to_string()))
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
*/
|
||||||
|
|
||||||
impl<'a> TypeContext<'a> {
|
impl<'a> TypeContext<'a> {
|
||||||
pub fn new() -> TypeContext<'a> {
|
pub fn new() -> TypeContext<'a> {
|
||||||
@ -114,141 +116,6 @@ impl<'a> TypeContext<'a> {
|
|||||||
}
|
}
|
||||||
|
|
||||||
pub fn typecheck(&mut self, ast: &AST) -> Result<String, String> {
|
pub fn typecheck(&mut self, ast: &AST) -> Result<String, String> {
|
||||||
match self.infer_ast(ast) {
|
Ok(format!("UNIT"))
|
||||||
Ok(t) => Ok(format!("{:?}", t)),
|
|
||||||
Err(err) => Err(format!("Type error: {:?}", err))
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<'a> TypeContext<'a> {
|
|
||||||
fn infer_ast(&mut self, ast: &AST) -> InferResult<Type<UVar>> {
|
|
||||||
self.infer_block(&ast.0)
|
|
||||||
}
|
|
||||||
|
|
||||||
fn infer_statement(&mut self, stmt: &Statement) -> InferResult<Type<UVar>> {
|
|
||||||
match stmt {
|
|
||||||
Statement::ExpressionStatement(ref expr) => self.infer_expr(expr.node()),
|
|
||||||
Statement::Declaration(ref decl) => self.infer_decl(decl),
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
fn infer_expr(&mut self, expr: &Expression) -> InferResult<Type<UVar>> {
|
|
||||||
match expr {
|
|
||||||
Expression(expr_type, Some(type_anno)) => {
|
|
||||||
let tx = self.infer_expr_type(expr_type)?;
|
|
||||||
let ty = type_anno.to_monotype();
|
|
||||||
self.unify(&ty.to_tvar(), &tx.to_tvar()).map(|x| x.skolemize())
|
|
||||||
},
|
|
||||||
Expression(expr_type, None) => self.infer_expr_type(expr_type)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
fn infer_decl(&mut self, _decl: &Declaration) -> InferResult<Type<UVar>> {
|
|
||||||
Ok(Type::Const(TConst::user("unimplemented")))
|
|
||||||
}
|
|
||||||
|
|
||||||
fn infer_expr_type(&mut self, expr_type: &ExpressionType) -> InferResult<Type<UVar>> {
|
|
||||||
use self::ExpressionType::*;
|
|
||||||
Ok(match expr_type {
|
|
||||||
NatLiteral(_) => Type::Const(TConst::Nat),
|
|
||||||
FloatLiteral(_) => Type::Const(TConst::Float),
|
|
||||||
StringLiteral(_) => Type::Const(TConst::StringT),
|
|
||||||
BoolLiteral(_) => Type::Const(TConst::Bool),
|
|
||||||
Value(name) => {
|
|
||||||
//TODO handle the distinction between 0-arg constructors and variables at some point
|
|
||||||
// need symbol table for that
|
|
||||||
match self.variable_map.lookup(name) {
|
|
||||||
Some(ty) => ty.clone().skolemize(),
|
|
||||||
None => return TypeError::new(&format!("Variable {} not found", name))
|
|
||||||
}
|
|
||||||
},
|
|
||||||
IfExpression { discriminator, body } => self.infer_if_expr(discriminator, body)?,
|
|
||||||
Call { f, arguments } => {
|
|
||||||
let tf = self.infer_expr(f)?; //has to be an Arrow Type
|
|
||||||
let targ = self.infer_expr(&arguments[0].node())?; // TODO make this work with functions with more than one arg
|
|
||||||
match tf {
|
|
||||||
Type::Arrow(t1, t2) => {
|
|
||||||
self.unify(&t1.to_tvar(), &targ.to_tvar())?;
|
|
||||||
*t2.clone()
|
|
||||||
},
|
|
||||||
_ => return TypeError::new("not a function")
|
|
||||||
}
|
|
||||||
},
|
|
||||||
|
|
||||||
Lambda { params, .. } => {
|
|
||||||
|
|
||||||
let _arg_type = match ¶ms[0] {
|
|
||||||
(_, Some(type_anno)) => type_anno.to_monotype().to_tvar(),
|
|
||||||
(_, None) => self.allocate_existential(),
|
|
||||||
};
|
|
||||||
//let _result_type = unimplemented!();
|
|
||||||
return TypeError::new("Unimplemented");
|
|
||||||
|
|
||||||
//Type::Arrow(Box::new(arg_type), Box::new(result_type))
|
|
||||||
}
|
|
||||||
_ => Type::Const(TConst::user("unimplemented"))
|
|
||||||
})
|
|
||||||
}
|
|
||||||
|
|
||||||
fn infer_if_expr(&mut self, discriminator: &Discriminator, body: &IfExpressionBody) -> InferResult<Type<UVar>> {
|
|
||||||
let _test = match discriminator {
|
|
||||||
Discriminator::Simple(expr) => expr,
|
|
||||||
_ => return TypeError::new("Dame desu")
|
|
||||||
};
|
|
||||||
|
|
||||||
let (_then_clause, _maybe_else_clause) = match body {
|
|
||||||
IfExpressionBody::SimpleConditional(a, b) => (a, b),
|
|
||||||
_ => return TypeError::new("Dont work")
|
|
||||||
};
|
|
||||||
|
|
||||||
TypeError::new("Not implemented")
|
|
||||||
}
|
|
||||||
|
|
||||||
fn infer_block(&mut self, block: &Block) -> InferResult<Type<UVar>> {
|
|
||||||
let mut output = Type::Const(TConst::Unit);
|
|
||||||
for statement in block.iter() {
|
|
||||||
output = self.infer_statement(statement.node())?;
|
|
||||||
}
|
|
||||||
Ok(output)
|
|
||||||
}
|
|
||||||
|
|
||||||
fn unify(&mut self, _t1: &Type<TVar>, _t2: &Type<TVar>) -> InferResult<Type<TVar>> {
|
|
||||||
TypeError::new("not implemented")
|
|
||||||
}
|
|
||||||
|
|
||||||
fn allocate_existential(&mut self) -> Type<TVar> {
|
|
||||||
let n = self.evar_count;
|
|
||||||
self.evar_count += 1;
|
|
||||||
Type::Var(TVar::Exist(ExistentialVar(n)))
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
#[cfg(test)]
|
|
||||||
mod tests {
|
|
||||||
use super::*;
|
|
||||||
|
|
||||||
fn parse(input: &str) -> AST {
|
|
||||||
let tokens: Vec<crate::tokenizing::Token> = crate::tokenizing::tokenize(input);
|
|
||||||
let mut parser = crate::parsing::Parser::new(tokens);
|
|
||||||
parser.parse().unwrap()
|
|
||||||
}
|
|
||||||
|
|
||||||
macro_rules! type_test {
|
|
||||||
($input:expr, $correct:expr) => {
|
|
||||||
{
|
|
||||||
let mut tc = TypeContext::new();
|
|
||||||
let ast = parse($input);
|
|
||||||
tc.add_symbols(&ast);
|
|
||||||
assert_eq!($correct, tc.type_check(&ast).unwrap())
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn basic_inference() {
|
|
||||||
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user