Skip to content

Commit

Permalink
Fmt + Clippy
Browse files Browse the repository at this point in the history
  • Loading branch information
JonathanBrouwer committed Apr 14, 2024
1 parent 6c5528c commit 8e901c2
Show file tree
Hide file tree
Showing 9 changed files with 98 additions and 81 deletions.
110 changes: 60 additions & 50 deletions prism-compiler/src/lang/error.rs
Original file line number Diff line number Diff line change
Expand Up @@ -23,82 +23,92 @@ pub enum TypeError {
}

impl TcEnv {
pub fn report(&mut self, error: &TypeError) -> Option<Report<'static, Span>> {
pub fn report(&mut self, error: &TypeError) -> Report<'static, Span> {
let report = Report::build(ReportKind::Error, (), 0);
Some(match error {
match error {
TypeError::ExpectType(i) => {
let label = match self.value_origins[i.0] {
ValueOrigin::TypeOf(j) => match self.value_origins[j.0] {
ValueOrigin::SourceCode(span) => Label::new(span).with_message(format!(
"Expected a type, found value of type: {}",
self.index_to_sm_string(self.value_types[&j])
)),
_ => unreachable!(),
},
_ => unreachable!(),
let ValueOrigin::TypeOf(j) = self.value_origins[i.0] else {
unreachable!()
};
let ValueOrigin::SourceCode(span) = self.value_origins[j.0] else {
unreachable!()
};
let label = Label::new(span).with_message(format!(
"Expected a type, found value of type: {}",
self.index_to_sm_string(self.value_types[&j])
));

report
.with_message("Expected type")
.with_label(label)
.finish()
}
TypeError::IndexOutOfBound(i) => {
let label = match self.value_origins[i.0] {
ValueOrigin::SourceCode(span) => {
Label::new(span).with_message("This index is out of bounds.")
}
_ => unreachable!(),
let ValueOrigin::SourceCode(span) = self.value_origins[i.0] else {
unreachable!()
};
let label = Label::new(span).with_message("This index is out of bounds.");

report
.with_message("De Bruijn index out of bounds")
.with_label(label)
.finish()
}
TypeError::ExpectFn(i) => {
let label = match self.value_origins[i.0] {
ValueOrigin::TypeOf(j) => match self.value_origins[j.0] {
ValueOrigin::SourceCode(span) => Label::new(span).with_message(format!(
"Expected a function, found value of type: {}",
self.index_to_sm_string(self.value_types[&j])
)),
_ => unreachable!(),
},
_ => unreachable!(),
let ValueOrigin::TypeOf(j) = self.value_origins[i.0] else {
unreachable!()
};
let ValueOrigin::SourceCode(span) = self.value_origins[j.0] else {
unreachable!()
};
let label = Label::new(span).with_message(format!(
"Expected a function, found value of type: {}",
self.index_to_sm_string(self.value_types[&j])
));
report
.with_message("Expected function")
.with_label(label)
.finish()
}
TypeError::ExpectFnArg { function_type, function_arg_type, arg_type } => {
let label_arg = match self.value_origins[arg_type.0] {
ValueOrigin::TypeOf(j) => match self.value_origins[j.0] {
ValueOrigin::SourceCode(span) => Label::new(span).with_message(format!(
"This argument has type: {}",
self.index_to_sm_string(*arg_type)
)),
_ => unreachable!(),
},
_ => unreachable!(),
TypeError::ExpectFnArg {
function_type,
function_arg_type,
arg_type,
} => {
let ValueOrigin::TypeOf(j) = self.value_origins[arg_type.0] else {
unreachable!()
};
let ValueOrigin::SourceCode(span) = self.value_origins[j.0] else {
unreachable!()
};
let label_arg = Label::new(span).with_message(format!(
"This argument has type: {}",
self.index_to_sm_string(*arg_type)
));

let label_fn = match self.value_origins[function_type.0] {
ValueOrigin::TypeOf(j) => match self.value_origins[j.0] {
ValueOrigin::SourceCode(span) => Label::new(span).with_message(format!(
"This function takes arguments of type: {}",
self.index_to_sm_string(*function_arg_type)
)).with_order(1).with_color(SECONDARY_COLOR),
_ => unreachable!(),
},
_ => unreachable!(),
let ValueOrigin::TypeOf(j) = self.value_origins[function_type.0] else {
unreachable!()
};
let ValueOrigin::SourceCode(span) = self.value_origins[j.0] else {
unreachable!()
};
let label_fn = Label::new(span)
.with_message(format!(
"This function takes arguments of type: {}",
self.index_to_sm_string(*function_arg_type)
))
.with_order(1)
.with_color(SECONDARY_COLOR);

report.with_message("Argument type mismatch in function application").with_label(label_arg).with_label(label_fn).finish()
},
TypeError::InfiniteType(_) => todo!(),
TypeError::BadInfer { .. } => todo!(),
})
report
.with_message("Argument type mismatch in function application")
.with_label(label_arg)
.with_label(label_fn)
.finish()
}
TypeError::InfiniteType(_) => report.finish(),
TypeError::BadInfer { .. } => report.finish(),
}
}
}

Expand All @@ -109,7 +119,7 @@ pub struct AggregatedTypeError {
impl AggregatedTypeError {
pub fn eprint(&self, env: &mut TcEnv, input: &str) -> io::Result<()> {
let mut input = Source::from(input);
for report in self.errors.iter().flat_map(|err| env.report(err)) {
for report in self.errors.iter().map(|err| env.report(err)) {
report.eprint(&mut input)?;
}
Ok(())
Expand Down
9 changes: 3 additions & 6 deletions prism-compiler/src/lang/expect_beq.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,9 @@ use crate::lang::env::Env;
use crate::lang::env::EnvEntry::*;
use crate::lang::error::TypeError;
use crate::lang::UnionIndex;
use crate::lang::ValueOrigin::FreeSub;
use crate::lang::{PartialExpr, TcEnv};
use std::collections::HashMap;
use crate::lang::ValueOrigin::FreeSub;

impl TcEnv {
/// Expect `io` to be equal to `Type`.
Expand Down Expand Up @@ -34,7 +34,6 @@ impl TcEnv {

match self.values[fr.0] {
PartialExpr::FnType(f_at, f_rt) => {

if !self.expect_beq_internal((f_at, &sr, &mut var_map1), (at, s, &mut var_map2)) {
self.errors.push(TypeError::ExpectFnArg {
function_type: ft,
Expand Down Expand Up @@ -70,15 +69,13 @@ impl TcEnv {
let id = self.new_tc_id();
var_map1.insert(id, sr.len());
var_map2.insert(id, s.len());

debug_assert!(self.expect_beq_free(
(f_rt, &sr.cons(RType(id)), &mut var_map1),
(rt, &s.cons(RType(id)), &mut var_map2),
));
}
_ => {
self.errors.push(TypeError::ExpectFn(ft))
}
_ => self.errors.push(TypeError::ExpectFn(ft)),
}

self.toxic_values.clear();
Expand Down
16 changes: 7 additions & 9 deletions prism-compiler/src/lang/expect_beq_internal.rs
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ impl TcEnv {
}
PartialExpr::Let(v1, b1) => self.expect_beq_free(
(b1, &s1.cons(RSubst(v1, s1.clone())), var_map1),
(i2, &s2, var_map2),
(i2, s2, var_map2),
),
PartialExpr::Var(v1) => {
let subst_equal = match &s1[v1] {
Expand Down Expand Up @@ -168,9 +168,7 @@ impl TcEnv {
self.values[i2.0] = PartialExpr::Var(v2);
true
}
RSubst(i1, s1) => {
self.expect_beq_free((*i1, &s1, var_map1), (i2, s2, var_map2))
}
RSubst(i1, s1) => self.expect_beq_free((*i1, s1, var_map1), (i2, s2, var_map2)),
};
let constraints_eq = self.handle_constraints(i2, s2);
subst_equal && constraints_eq
Expand All @@ -183,7 +181,7 @@ impl TcEnv {
let constraints_eq = self.handle_constraints(i2, s2);

self.toxic_values.insert(i2);
let a_eq = self.expect_beq_free((a1, &s1, var_map1), (a2, s2, var_map2));
let a_eq = self.expect_beq_free((a1, s1, var_map1), (a2, s2, var_map2));
let id = self.new_tc_id();
var_map1.insert(id, s1.len());
var_map2.insert(id, s2.len());
Expand All @@ -202,7 +200,7 @@ impl TcEnv {
let constraints_eq = self.handle_constraints(i2, s2);

self.toxic_values.insert(i2);
let a_eq = self.expect_beq_free((a1, &s1, var_map1), (a2, &s2, var_map2));
let a_eq = self.expect_beq_free((a1, s1, var_map1), (a2, s2, var_map2));

let id = self.new_tc_id();
var_map1.insert(id, s1.len());
Expand All @@ -222,8 +220,8 @@ impl TcEnv {
let constraints_eq = self.handle_constraints(i2, s2);

self.toxic_values.insert(i2);
let f_eq = self.expect_beq_free((f1, &s1, var_map1), (f2, &s2, var_map2));
let a_eq = self.expect_beq_free((a1, &s1, var_map1), (a2, &s2, var_map2));
let f_eq = self.expect_beq_free((f1, s1, var_map1), (f2, s2, var_map2));
let a_eq = self.expect_beq_free((a1, s1, var_map1), (a2, s2, var_map2));
constraints_eq && f_eq && a_eq
}
PartialExpr::Free => {
Expand All @@ -238,7 +236,7 @@ impl TcEnv {
true
}
PartialExpr::Shift(v1, i) => {
self.expect_beq_free((v1, &s1.shift(i), var_map1), (i2, &s2, var_map2))
self.expect_beq_free((v1, &s1.shift(i), var_map1), (i2, s2, var_map2))
}
};
}
Expand Down
21 changes: 12 additions & 9 deletions prism-compiler/src/lang/mod.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
use crate::lang::env::{Env, UniqueVariableId};
use crate::lang::error::TypeError;
use prism_parser::core::pos::Pos;
use prism_parser::core::span::Span;
use std::collections::{HashMap, HashSet};

Expand All @@ -15,6 +16,11 @@ pub mod is_beta_equal;
pub mod simplify;
pub mod type_check;

type QueuedConstraint = (
(Env, HashMap<UniqueVariableId, usize>),
(UnionIndex, Env, HashMap<UniqueVariableId, usize>),
);

#[derive(Default)]
pub struct TcEnv {
// uf: UnionFind,
Expand All @@ -27,13 +33,8 @@ pub struct TcEnv {
toxic_values: HashSet<UnionIndex>,

// Queues
queued_beq_free: HashMap<
UnionIndex,
Vec<(
(Env, HashMap<UniqueVariableId, usize>),
(UnionIndex, Env, HashMap<UniqueVariableId, usize>),
)>,
>, //TODO readd queued_tc: HashMap<UnionIndex, (Env, UnionIndex)>,
queued_beq_free: HashMap<UnionIndex, Vec<QueuedConstraint>>,
//TODO readd queued_tc: HashMap<UnionIndex, (Env, UnionIndex)>,
}

#[derive(Copy, Clone, Hash, Eq, PartialEq, Debug)]
Expand All @@ -43,7 +44,6 @@ pub enum ValueOrigin {
FreeSub(UnionIndex),
FreeValueFailure(UnionIndex),
FreeTypeFailure(UnionIndex),
Test,
}

#[derive(Copy, Clone, Hash, Eq, PartialEq, Debug)]
Expand All @@ -67,7 +67,10 @@ impl TcEnv {
}

pub fn store_test(&mut self, e: PartialExpr) -> UnionIndex {
self.store(e, ValueOrigin::Test)
self.store(
e,
ValueOrigin::SourceCode(Span::new(Pos::start(), Pos::start())),
)
}

fn store(&mut self, e: PartialExpr, origin: ValueOrigin) -> UnionIndex {
Expand Down
4 changes: 3 additions & 1 deletion prism-compiler/src/lang/simplify.rs
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,9 @@ impl TcEnv {
PartialExpr::FnDestruct(a, b)
}
PartialExpr::Free => PartialExpr::Free,
PartialExpr::Shift(b, i) => return self.simplify_inner(b, &s.shift(i), var_map),
PartialExpr::Shift(b, i) => {
return self.simplify_inner(b, &s.shift(i.min(s.len())), var_map)
}
};
self.store(e_new, self.value_origins[i.0])
}
Expand Down
6 changes: 3 additions & 3 deletions prism-compiler/src/lang/type_check.rs
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ impl TcEnv {
PartialExpr::FnType(mut a, b) => {
let err_count = self.errors.len();
let at = self._type_check(a, s);
self.expect_beq_type(at, &s);
self.expect_beq_type(at, s);
if self.errors.len() > err_count {
a = self.store(PartialExpr::Free, FreeValueFailure(a));
}
Expand All @@ -66,7 +66,7 @@ impl TcEnv {
PartialExpr::FnConstruct(mut a, b) => {
let err_count = self.errors.len();
let at = self._type_check(a, s);
self.expect_beq_type(at, &s);
self.expect_beq_type(at, s);
if self.errors.len() > err_count {
a = self.store(PartialExpr::Free, FreeValueFailure(a));
}
Expand All @@ -87,7 +87,7 @@ impl TcEnv {
let err_count = self.errors.len();
let ft = self._type_check(f, s);
if self.errors.len() == err_count {
self.expect_beq_fn_type(ft, at, rt, &s);
self.expect_beq_fn_type(ft, at, rt, s);
}

PartialExpr::Let(a, rt)
Expand Down
2 changes: 1 addition & 1 deletion prism-compiler/src/parser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ use prism_parser::rule_action::RuleAction;

lazy_static! {
pub static ref GRAMMAR: GrammarFile<'static, RuleAction<'static, 'static>> =
{ parse_grammar::<SetError>(include_str!("../resources/grammar")).unwrap_or_eprint() };
parse_grammar::<SetError>(include_str!("../resources/grammar")).unwrap_or_eprint();
}

pub fn parse_prism_in_env<'p>(
Expand Down
9 changes: 8 additions & 1 deletion prism-compiler/tests/exhaustive.rs
Original file line number Diff line number Diff line change
Expand Up @@ -50,5 +50,12 @@ impl Debug for ExprWithEnv {

#[exhaustive_test(9)]
fn test_exhaustive(ExprWithEnv(mut env, root): ExprWithEnv) {
let _ = env.type_check(root);
match env.type_check(root) {
Ok(_) => {}
Err(errs) => {
for err in errs.errors {
env.report(&err);
}
}
}
}
2 changes: 1 addition & 1 deletion prism-parser/src/error/tree_error.rs
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ impl<L: Eq + Hash + Clone> ErrorTree<L> {
subs.push(vec![l]);
} else {
subs.iter_mut().for_each(|v| {
v.push(&l);
v.push(l);
});
}
}
Expand Down

0 comments on commit 8e901c2

Please sign in to comment.