Skip to content

Commit

Permalink
Implement bidirectional typechecker
Browse files Browse the repository at this point in the history
This commit replaces the previous typechecker with a bidirectional one,
following the "algorithmic context" design in Complete & Easy
Bidirectional Typechecking by Dunfield & Krishnaswami.
  • Loading branch information
matthew-healy committed Oct 2, 2023
1 parent 00790aa commit 093d762
Show file tree
Hide file tree
Showing 10 changed files with 618 additions and 194 deletions.
5 changes: 2 additions & 3 deletions examples/fail/application_with_non_function.uplp
Original file line number Diff line number Diff line change
@@ -1,9 +1,8 @@
-- category = "error"
--
-- [metadata]
-- error = "Type.mismatch"
-- error = "Type.invalid_application"
--
-- [metadata.expectation]
-- expected = "?0 -> ?1"
-- got = "Num"
-- applied_type = "Num"
let a = 1 in a 5
5 changes: 5 additions & 0 deletions examples/pass/variable_shadowing.uplp
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
-- category = 'value'
--
-- [metadata]
-- type = 'Unit'
let f = |x: Num| |x: Unit| (x : Unit) in f 1 ()
18 changes: 2 additions & 16 deletions src/error.rs
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
use crate::{interner, parser::Token, typ::Type};
use crate::{interner, parser::Token, typ};
use lalrpop_util;

#[derive(Debug, PartialEq, Eq)]
pub enum Error {
ParseError(ParseError),
TypeError(TypeError),
TypeError(typ::Error),
EvaluationError(EvaluationError),
}

Expand Down Expand Up @@ -76,20 +76,6 @@ impl From<ParseError> for Error {
}
}

// Type Errors

#[derive(Debug, PartialEq, Eq)]
pub enum TypeError {
Mismatch { got: Type, expected: Type },
BadApplication,
}

impl From<TypeError> for Error {
fn from(e: TypeError) -> Self {
Error::TypeError(e)
}
}

// Evaluation Errors

#[derive(Debug, PartialEq, Eq)]
Expand Down
7 changes: 2 additions & 5 deletions src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -28,18 +28,15 @@ pub fn parse(input: &str) -> Result<Box<RawExpr>, Error> {
}

pub fn check_types(input: &str) -> Result<Type, Error> {
let mut type_checker = typ::check::er();

let expr = parse_and_scope_check(input)?;
let typ = type_checker.infer(&expr)?;
let typ = typ::infer(&expr)?;
Ok(typ)
}

pub fn evaluate(input: &str) -> Result<values::Val, error::Error> {
let expr = parse_and_scope_check(input)?;

let mut type_checker = typ::check::er();
let _ = type_checker.infer(&expr)?;
let _ = typ::infer(&expr)?;

let compiler = vm::Compiler::new();
let code = compiler.compile(&expr);
Expand Down
6 changes: 3 additions & 3 deletions src/parser.lalrpop
Original file line number Diff line number Diff line change
Expand Up @@ -96,9 +96,9 @@ Type: Type = {
}

PrimType: Type = {
"Bool" => Type::Bool,
"Num" => Type::Num,
"Unit" => Type::Unit,
"Bool" => Type::bool(),
"Num" => Type::num(),
"Unit" => Type::unit(),
"(" <Type> ")" => <>,
};

Expand Down
154 changes: 0 additions & 154 deletions src/typ/check.rs

This file was deleted.

Loading

0 comments on commit 093d762

Please sign in to comment.