From b5636ac6c0bb47d6bad55ced5c1a7ba25a03e916 Mon Sep 17 00:00:00 2001 From: felipegchi Date: Mon, 28 Nov 2022 11:09:34 -0300 Subject: [PATCH] fix: erasure checker --- crates/kind-checker/src/lib.rs | 2 +- crates/kind-cli/tests/suite/eval/User.kind2 | 11 +- crates/kind-driver/src/lib.rs | 46 +- crates/kind-pass/src/desugar/app.rs | 4 +- crates/kind-pass/src/erasure/mod.rs | 827 ++++++++++---------- crates/kind-pass/src/errors.rs | 17 - crates/kind-target-kdl/src/flatten.rs | 2 +- crates/kind-tree/src/untyped/mod.rs | 3 +- 8 files changed, 427 insertions(+), 485 deletions(-) diff --git a/crates/kind-checker/src/lib.rs b/crates/kind-checker/src/lib.rs index d4d59cb9..dda6ce1f 100644 --- a/crates/kind-checker/src/lib.rs +++ b/crates/kind-checker/src/lib.rs @@ -70,7 +70,7 @@ pub fn type_check( succeeded } - Err(_) => panic!(), + Err(res) => panic!("{}", res), } } diff --git a/crates/kind-cli/tests/suite/eval/User.kind2 b/crates/kind-cli/tests/suite/eval/User.kind2 index 66950e1d..368cb9e8 100644 --- a/crates/kind-cli/tests/suite/eval/User.kind2 +++ b/crates/kind-cli/tests/suite/eval/User.kind2 @@ -1,11 +1,12 @@ + +#kdl_run +Main : U60 +Main = Teste List.nil + type List (t: Type) { cons (x: t) (xs: List t) nil } Teste (n: List U60) : U60 -Teste (List.cons 2 xs) = 2 - -#kdl_run -Main : U60 -Main = Teste List.nil \ No newline at end of file +Teste (List.cons 2 xs) = 2 \ No newline at end of file diff --git a/crates/kind-driver/src/lib.rs b/crates/kind-driver/src/lib.rs index c6269542..1040527d 100644 --- a/crates/kind-driver/src/lib.rs +++ b/crates/kind-driver/src/lib.rs @@ -1,16 +1,12 @@ use checker::eval; use errors::DriverError; -use fxhash::FxHashSet; use kind_pass::{desugar, erasure, expand}; -use kind_report::{data::Diagnostic, report::FileCache}; +use kind_report::{report::FileCache}; use kind_span::SyntaxCtxIndex; use kind_tree::{backend, concrete, desugared, untyped}; use session::Session; -use std::{ - path::{Path, PathBuf}, - sync::mpsc::Sender, -}; +use std::path::{PathBuf}; use kind_checker as checker; @@ -37,13 +33,7 @@ pub fn type_check_book(session: &mut Session, path: &PathBuf) -> Option Option { @@ -67,11 +57,7 @@ pub fn erase_book( ) -> Option { let concrete_book = to_book(session, path)?; let desugared_book = desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)?; - erasure::erase_book( - desugared_book, - session.diagnostic_sender.clone(), - FxHashSet::from_iter(entrypoint.to_owned()), - ) + erasure::erase_book(&desugared_book, session.diagnostic_sender.clone()) } pub fn desugar_book(session: &mut Session, path: &PathBuf) -> Option { @@ -82,11 +68,7 @@ pub fn desugar_book(session: &mut Session, path: &PathBuf) -> Option Option { let concrete_book = to_book(session, path)?; let desugared_book = desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)?; - erasure::erase_book( - desugared_book.clone(), - session.diagnostic_sender.clone(), - FxHashSet::from_iter(vec!["Main".to_string()]), - )?; + Some(desugared_book) } @@ -97,24 +79,12 @@ pub fn compile_book_to_hvm(book: untyped::Book) -> backend::File { pub fn compile_book_to_kdl( path: &PathBuf, session: &mut Session, - namespace: &str, + namespace: &str ) -> Option { let concrete_book = to_book(session, path)?; let desugared_book = desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)?; - - let entrypoints = desugared_book - .entrs - .iter() - .filter(|x| x.1.attrs.kdl_run) - .map(|x| x.0.clone()) - .collect::>(); - - let book = erasure::erase_book( - desugared_book, - session.diagnostic_sender.clone(), - FxHashSet::from_iter(entrypoints), - )?; - + let book = erasure::erase_book(&desugared_book, session.diagnostic_sender.clone())?; + println!("{} {}", book.entrs.len(), book.names.len()); kind_target_kdl::compile_book(book, session.diagnostic_sender.clone(), namespace) } diff --git a/crates/kind-pass/src/desugar/app.rs b/crates/kind-pass/src/desugar/app.rs index ad306b00..80887ec9 100644 --- a/crates/kind-pass/src/desugar/app.rs +++ b/crates/kind-pass/src/desugar/app.rs @@ -94,8 +94,8 @@ impl<'a> DesugarState<'a> { // It's not expected that positional arguments require the range so // it's the reason why we are using a terrible "ghost range" arguments[i] = Some(( - Range::ghost_range(), - self.gen_hole_expr(Range::ghost_range()), + range, + self.gen_hole_expr(range), )) } } diff --git a/crates/kind-pass/src/erasure/mod.rs b/crates/kind-pass/src/erasure/mod.rs index 84cbd049..9b42dddb 100644 --- a/crates/kind-pass/src/erasure/mod.rs +++ b/crates/kind-pass/src/erasure/mod.rs @@ -1,315 +1,377 @@ -//! Erases everything that is not relevant to the output. -//! It's a simpler version of what I want to do in order -//! to finish a stable version of the compiler. - -// FIX: Need to make a "constraint map" in order to check -// if a irrelevant thing is relevant in relation to the -// function that we are trying to check the irrelevance. - -// Not the best algorithm... it should not be trusted for -// dead code elimination. - -// TODO: Cannot pattern match on erased - use std::sync::mpsc::Sender; use fxhash::{FxHashMap, FxHashSet}; - use kind_report::data::Diagnostic; use kind_span::Range; -use kind_tree::desugared::{Book, Entry, Expr, Rule}; -use kind_tree::symbol::QualifiedIdent; -use kind_tree::{untyped, Number}; + +use kind_tree::desugared; +use kind_tree::symbol::{Ident, QualifiedIdent}; +use kind_tree::untyped::{self}; +use kind_tree::Number; use crate::errors::PassError; -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Relevance { +#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)] +enum Relevance { + Relevant, + Irrelevant, +} + +#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)] +enum Ambient { + Unknown, Irrelevant, Relevant, - Hole(usize), } + +impl Ambient { + pub fn to_relev(&self) -> Relevance { + match self { + Ambient::Irrelevant => Relevance::Irrelevant, + Ambient::Unknown | Ambient::Relevant => Relevance::Relevant, + } + } +} + +pub struct Edge { + name: String, + relevance: FxHashMap>, + connections: FxHashMap>, +} + pub struct ErasureState<'a> { errs: Sender>, - book: &'a Book, + book: &'a desugared::Book, - ctx: im::HashMap, Relevance))>, + edges: Vec, + names: FxHashMap, + + ctx: im::HashMap, - names: FxHashMap, Relevance)>, - holes: Vec>, failed: bool, } -pub fn erase_book( - book: Book, +pub fn erase_book<'a>( + book: &'a desugared::Book, errs: Sender>, - entrypoint: FxHashSet, ) -> Option { let mut state = ErasureState { errs, - book: &book, - ctx: Default::default(), + book, + edges: Default::default(), names: Default::default(), - holes: Default::default(), - failed: false, + ctx: Default::default(), + failed: Default::default(), }; - let mut new_book = untyped::Book { - holes: book.holes, - ..Default::default() - }; - - let mut entries = FxHashMap::default(); - - for name in entrypoint { - let count = state.holes.len(); - state - .names - .insert(name.to_string(), (None, Relevance::Hole(count))); - state.holes.push(Some(Relevance::Relevant)); - } - - for (name, v) in &book.entrs { - entries.insert(name, state.erase_entry(v)); - } - - if state.failed { - return None; - } - - for (name, (_, relev)) in &state.names { - if let Some(Relevance::Relevant) = state.normalize(*relev) { - if let Some(res) = entries.remove(name) { - new_book - .names - .insert(name.to_string(), new_book.entrs.len()); - new_book.entrs.insert(name.to_string(), res); - } - } - } - - Some(new_book) + state.erase_book(book) } impl<'a> ErasureState<'a> { - pub fn new_hole(&mut self, range: Range, name: String) -> (Option, Relevance) { - let count = self.holes.len(); - let local_relevance = (Some(range), Relevance::Hole(count)); - self.names.insert(name, local_relevance); - self.holes.push(None); - local_relevance + fn get_edge_or_create(&mut self, name: &QualifiedIdent) -> usize { + if let Some(id) = self.names.get(&name.to_string()) { + id.1 + } else { + let id = self.edges.len(); + self.names.insert(name.to_string(), (name.range, id)); + self.edges.push(Edge { + name: name.to_string(), + relevance: Default::default(), + connections: Default::default(), + }); + id + } } - pub fn send_err(&mut self, err: Box) { - self.errs.send(err).unwrap(); - self.failed = true; - } - pub fn err_irrelevant( - &mut self, - declared_val: Option, - used: Range, - declared_ty: Option, - ) { - self.send_err(Box::new(PassError::CannotUseIrrelevant( - declared_val, - used, - declared_ty, - ))); + fn set_relevance(&mut self, id: usize, relevance: Relevance, on: Range) { + let edge = self.edges.get_mut(id).unwrap(); + let entry = edge.relevance.entry(relevance).or_default(); + entry.push(on) } - pub fn get_normal(&self, hole: usize, visited: &mut FxHashSet) -> Option { - match self.holes[hole] { - Some(Relevance::Hole(r)) if !visited.contains(&hole) => { - visited.insert(hole); - self.get_normal(r, visited) + fn connect_with(&mut self, id: usize, name: &QualifiedIdent, ambient: Ambient) { + let new_id = self.get_edge_or_create(name); + let entry = self.edges[id].connections.entry(new_id).or_default(); + entry.push((name.range, ambient)) + } + + pub fn erase_book(&mut self, book: &'a desugared::Book) -> Option { + let mut vals = FxHashMap::default(); + + let mut entrypoints = Vec::new(); + + if let Some(entr) = book.entrs.get("Main") { + let id = self.get_edge_or_create(&entr.name); + self.set_relevance(id, Relevance::Relevant, entr.name.range); + entrypoints.push(id); + } + + for entr in book.entrs.values() { + if entr.attrs.kdl_run { + let id = self.get_edge_or_create(&entr.name); + self.set_relevance(id, Relevance::Relevant, entr.name.range); + entrypoints.push(id); } - other => other, } - } - pub fn normalize(&self, hole: Relevance) -> Option { - match hole { - Relevance::Hole(hole) => self.get_normal(hole, &mut Default::default()), - other => Some(other), + for entr in book.entrs.values() { + vals.insert(entr.name.to_string(), self.erase_entry(entr)); } - } - pub fn unify_loop( - &mut self, - range: Range, - left: (Option, Relevance), - right: (Option, Relevance), - visited: &mut FxHashSet, - relevance_unify: bool, - ) -> bool { - match (left.1, right.1) { - (Relevance::Hole(hole), t) => match (self.holes[hole], t) { - (Some(res), _) if !visited.contains(&hole) => { - visited.insert(hole); - self.unify_loop(range, (left.0, res), right, visited, relevance_unify) - } + let mut visited = FxHashSet::::default(); - // TODO: It should unify iff we want functions that are considered - // "erased" in the sense that we can just remove them from the runtime and it'll - // be fine. - (None, Relevance::Irrelevant) => { - self.holes[hole] = Some(Relevance::Irrelevant); - true - } - - (None, Relevance::Hole(n)) => { - self.holes[hole] = Some(Relevance::Hole(n)); - true - } - - (_, _) => true, - }, - (Relevance::Relevant, Relevance::Hole(hole)) => match self.holes[hole] { - Some(res) if !visited.contains(&hole) => { - visited.insert(hole); - self.unify_loop(range, left, (right.0, res), visited, relevance_unify) - } - _ => { - self.holes[hole] = Some(Relevance::Relevant); - true - } - }, - (Relevance::Irrelevant, Relevance::Hole(_)) - | (Relevance::Relevant, Relevance::Relevant) - | (Relevance::Irrelevant, Relevance::Irrelevant) - | (Relevance::Irrelevant, Relevance::Relevant) => true, - (Relevance::Relevant, Relevance::Irrelevant) => false, - } - } - - pub fn unify( - &mut self, - range: Range, - left: (Option, Relevance), - right: (Option, Relevance), - relevance_unify: bool, - ) -> bool { - self.unify_loop(range, left, right, &mut Default::default(), relevance_unify) - } - - pub fn erase_pat_spine( - &mut self, - on: (Option, Relevance), - name: &QualifiedIdent, - spine: &Vec>, - ) -> Vec> { - let fun = match self.names.get(name.to_str()) { - Some(res) => *res, - None => self.new_hole(name.range, name.to_string()), + let mut new_book = untyped::Book { + entrs: Default::default(), + names: Default::default(), }; - if !self.unify(name.range, on, fun, true) { - self.err_irrelevant(None, name.range, None) + let mut queue = entrypoints.iter().map(|x| (x, Ambient::Relevant)).collect::>(); + + while !queue.is_empty() { + let (fst, relev) = queue.pop().unwrap(); + + if visited.contains(&fst) { + continue; + } + + visited.insert(*fst); + + let edge = &self.edges[*fst]; + + if relev != Ambient::Irrelevant { + if let Some(res) = edge.relevance.get(&Relevance::Irrelevant) { + self.errs + .send(Box::new(PassError::CannotUseIrrelevant(None, res[0], None))) + .unwrap(); + } + } + + + let entry = vals.get(&edge.name).cloned().unwrap(); + + new_book.names.insert(entry.name.to_string(), new_book.entrs.len()); + + new_book.entrs.insert( + entry.name.to_string(), + entry + ); + + for (to, relevs) in &edge.connections { + for (_, relev) in relevs.iter() { + match relev { + Ambient::Irrelevant => (), + Ambient::Unknown | Ambient::Relevant => { + if !visited.contains(to) { + queue.push((to, *relev)); + } + } + } + } + } } - let entry = self.book.entrs.get(name.to_str()).unwrap(); - let erased = entry.args.iter(); - - spine - .iter() - .zip(erased) - .map(|(elem, arg)| { - let relev = if arg.erased { - (Some(arg.range), Relevance::Irrelevant) - } else { - on.clone() - }; - (self.erase_pat(relev, elem), arg.erased) - }) - .filter(|res| !res.1) - .map(|res| res.0) - .collect() + if self.failed { + None + } else { + Some(new_book) + } } - pub fn erase_pat(&mut self, on: (Option, Relevance), pat: &Expr) -> Box { - use kind_tree::desugared::ExprKind::*; + fn erase_entry(&mut self, entry: &'a desugared::Entry) -> Box { + let id = self.get_edge_or_create(&entry.name); - match &pat.data { - Num { - num: Number::U60(n), - } => untyped::Expr::num60(pat.range, *n), - Num { - num: Number::U120(n), - } => untyped::Expr::num120(pat.range, *n), + let mut args = Vec::new(); + + let backup = self.ctx.clone(); + + for arg in &entry.args { + self.erase_expr(Ambient::Irrelevant, id, &arg.typ); + self.ctx.insert(arg.name.to_string(), Relevance::Irrelevant); + if !arg.hidden { + args.push((arg.name.to_string(), arg.range, false)) + } + } + + self.erase_expr(Ambient::Irrelevant, id, &entry.typ); + + self.ctx = backup; + + let mut rules = Vec::new(); + + for rule in &entry.rules { + rules.push(self.erase_rule(entry, id, rule)); + } + + Box::new(untyped::Entry { + name: entry.name.clone(), + args, + rules, + attrs: entry.attrs.clone(), + range: entry.range, + }) + } + + fn erase_rule( + &mut self, + entr: &desugared::Entry, + edge: usize, + rule: &'a desugared::Rule, + ) -> untyped::Rule { + let backup = self.ctx.clone(); + + let has_relevance = self.edges[edge] + .relevance + .contains_key(&Relevance::Relevant); + + let relev = |hidden: bool| -> Ambient { + if hidden { + Ambient::Irrelevant + } else if has_relevance { + Ambient::Relevant + } else { + Ambient::Unknown + } + }; + + let pats = rule + .pats + .iter() + .zip(&entr.args) + .map(|(pat, arg)| (self.erase_pat(relev(arg.hidden), edge, pat), arg)) + .filter(|(_, arg)| !arg.erased) + .map(|res| res.0) + .collect::>(); + + + let body = self.erase_expr(relev(false), edge, &rule.body); + + self.ctx = backup; + + untyped::Rule { + name: entr.name.clone(), + pats, + body, + range: rule.range, + } + } + + fn erase_pat( + &mut self, + relevance: Ambient, + edge: usize, + expr: &'a desugared::Expr, + ) -> Box { + let relev = |hidden: bool| -> Ambient { + if hidden { + Ambient::Irrelevant + } else { + relevance + } + }; + + use desugared::ExprKind::*; + + match &expr.data { Var { name } => { - self.ctx.insert(name.to_string(), (name.range, on)); + self.ctx.insert( + name.to_string(), + if relevance == Ambient::Irrelevant { + Relevance::Irrelevant + } else { + Relevance::Relevant + }, + ); + untyped::Expr::var(name.clone()) } - Fun { name, args } | Ctr { name, args } if on.1 == Relevance::Irrelevant => { - let range = pat.range.clone(); - self.errs - .send(Box::new(PassError::CannotPatternMatchOnErased(range))) - .unwrap(); - self.failed = true; - self.erase_pat_spine(on, &name, args); - untyped::Expr::err(range) - } + Hole { num } => untyped::Expr::var(Ident::generate(&format!("_x{}", num))), Fun { name, args } => { - let args = self.erase_pat_spine(on, &name, args); - untyped::Expr::fun(pat.range.clone(), name.clone(), args) + self.connect_with(edge, name, relevance); + + // We cannot pattern match on functions in a relevant function. + // it would change its behaviour. + if relevance == Ambient::Irrelevant { + self.set_relevance(edge, Relevance::Irrelevant, expr.range) + } + + let params = self.book.entrs.get(name.to_str()).unwrap(); + + let args = args + .iter() + .zip(¶ms.args) + .map(|(arg, param)| (self.erase_pat(relev(param.hidden), edge, arg), param)) + .filter(|(_, param)| !param.hidden) + .map(|x| x.0) + .collect::>(); + + untyped::Expr::fun(expr.range, name.clone(), args) } Ctr { name, args } => { - let args = self.erase_pat_spine(on, &name, args); - untyped::Expr::ctr(pat.range.clone(), name.clone(), args) + self.connect_with(edge, name, relevance); + + // We cannot pattenr match on functions in a relevant function. + // it would change its behaviour. + if relevance == Ambient::Irrelevant { + self.set_relevance(edge, Relevance::Irrelevant, expr.range) + } + + let params = self.book.entrs.get(name.to_str()).unwrap(); + + let args = args + .iter() + .zip(¶ms.args) + .map(|(arg, param)| (self.erase_pat(relev(param.hidden), edge, arg), param)) + .filter(|(_, param)| !param.hidden) + .map(|x| x.0) + .collect::>(); + + untyped::Expr::ctr(expr.range, name.clone(), args) } - res => panic!("Internal Error: Not a pattern {:?}", res), + Num { + num: Number::U60(num), + } => untyped::Expr::num60(expr.range, *num), + Num { + num: Number::U120(num), + } => untyped::Expr::num120(expr.range, *num), + Str { val } => { + let nil = QualifiedIdent::new_static("String.nil", None, expr.range); + let cons = QualifiedIdent::new_static("String.cons", None, expr.range); + + self.connect_with(edge, &nil, relevance); + self.connect_with(edge, &cons, relevance); + + untyped::Expr::str(expr.range, val.clone()) + } + _ => todo!("Cannot be parsed {}", expr), } } - pub fn erase_expr( + fn erase_expr( &mut self, - on: &(Option, Relevance), - expr: &Expr, + ambient: Ambient, + edge: usize, + expr: &'a desugared::Expr, ) -> Box { - use kind_tree::desugared::ExprKind::*; - + use desugared::ExprKind::*; match &expr.data { - Typ | NumType { .. } | Err | Hole { .. } | Hlp(_) => { - if !self.unify(expr.range, *on, (None, Relevance::Irrelevant), false) { - self.err_irrelevant(None, expr.range, None) - } - // Used as sentinel value because all of these constructions - // should not end in the generated tree. - untyped::Expr::err(expr.range) - } - Num { - num: Number::U60(n), - } => untyped::Expr::num60(expr.range, *n), - Num { - num: Number::U120(n), - } => untyped::Expr::num120(expr.range, *n), - Str { val } => untyped::Expr::str(expr.range, val.clone()), - Var { name } => { - let relev = self.ctx.get(name.to_str()).unwrap(); - let declared_ty = (relev.1).0; - let declared_val = relev.0; - if !self.unify(name.range, *on, relev.1, false) { - self.err_irrelevant(Some(declared_val), name.range, declared_ty) - } - untyped::Expr::var(name.clone()) - } All { - param, typ, body, .. + param, + typ, + body, + erased: _, } => { - if !self.unify(expr.range, *on, (None, Relevance::Irrelevant), false) { - self.err_irrelevant(None, expr.range, None) + let backup = self.ctx.clone(); + self.ctx.insert(param.to_string(), Relevance::Irrelevant); + + if ambient != Ambient::Irrelevant { + self.set_relevance(edge, Relevance::Irrelevant, expr.range); } - let ctx = self.ctx.clone(); + self.erase_expr(Ambient::Irrelevant, edge, typ); + self.erase_expr(Ambient::Irrelevant, edge, body); - // Relevant inside the context that is it's being used? - self.ctx.insert(param.to_string(), (param.range, *on)); + self.ctx = backup; - self.erase_expr(&(on.0, Relevance::Irrelevant), typ); - self.erase_expr(&(on.0, Relevance::Irrelevant), body); - self.ctx = ctx; - - // Used as sentinel value because "All" should not end in a tree. untyped::Expr::err(expr.range) } Lambda { @@ -317,204 +379,131 @@ impl<'a> ErasureState<'a> { body, erased, } => { - let ctx = self.ctx.clone(); + let backup = self.ctx.clone(); - if *erased { - self.ctx.insert( - param.to_string(), - (param.range, (None, Relevance::Irrelevant)), - ); + let relev = if ambient == Ambient::Irrelevant || *erased { + Relevance::Irrelevant } else { - self.ctx.insert(param.to_string(), (param.range, *on)); - } + Relevance::Relevant + }; - let body = self.erase_expr(on, body); - self.ctx = ctx; + self.ctx.insert(param.to_string(), relev); - if *erased { - body - } else { - untyped::Expr::lambda(expr.range, param.clone(), body, *erased) - } + let body = self.erase_expr(ambient, edge, body); + + self.ctx = backup; + + untyped::Expr::lambda(expr.range, param.clone(), body, *erased) } Let { name, val, next } => { - let ctx = self.ctx.clone(); - self.ctx.insert(name.to_string(), (name.range, *on)); + let backup = self.ctx.clone(); - let val = self.erase_expr(on, val); - let next = self.erase_expr(on, next); + self.ctx.insert(name.to_string(), ambient.to_relev()); - self.ctx = ctx; + let val = self.erase_expr(ambient, edge, val); + let next = self.erase_expr(ambient, edge, next); + + self.ctx = backup; untyped::Expr::let_(expr.range, name.clone(), val, next) } - App { fun, args } => { - let head = self.erase_expr(on, fun); - let spine = args - .iter() - .map(|x| { - let on = if x.erased { - let span = expr.range; - if !self.unify(span, *on, (None, Relevance::Irrelevant), false) { - self.err_irrelevant(None, span, None) - } - (Some(x.data.range), Relevance::Irrelevant) - } else { - on.clone() - }; - (x.erased, self.erase_expr(&on, &x.data)) - }) - .filter(|x| !x.0) - .map(|x| x.1) - .collect(); - - untyped::Expr::app(expr.range, head, spine) - } Fun { name, args } => { - let spine = self.book.entrs.get(name.to_str()).unwrap().args.iter(); + self.connect_with(edge, name, ambient); - let fun = match self.names.get(name.to_str()) { - Some(res) => *res, - None => self.new_hole(name.range, name.to_string()), + let params = &self.book.entrs.get(name.to_str()).unwrap().args; + + let relev = |hidden| { + if hidden { + Ambient::Irrelevant + } else { + ambient + } }; - if !self.unify(name.range, *on, fun, true) { - self.err_irrelevant(None, name.range, None) - } - - let spine = args + let args = params .iter() - .zip(spine) - .map(|(expr, arg)| { - if arg.erased { - ( - self.erase_expr(&(Some(arg.range), Relevance::Irrelevant), expr), - arg, - ) - } else { - (self.erase_expr(on, expr), arg) - } - }) - .filter(|(_, arg)| !arg.erased); + .zip(args) + .map(|(param, arg)| (param, self.erase_expr(relev(param.erased), edge, arg))) + .filter(|(param, _)| !param.erased) + .map(|res| res.1) + .collect::>(); - untyped::Expr::fun( - expr.range, - name.clone(), - spine.map(|(expr, _)| expr).collect(), - ) + untyped::Expr::fun(expr.range, name.clone(), args) } Ctr { name, args } => { - let spine = self.book.entrs.get(name.to_str()).unwrap().args.iter(); + self.connect_with(edge, name, ambient); - let fun = match self.names.get(&name.to_string()) { - Some(res) => *res, - None => self.new_hole(name.range, name.to_string()), + let params = &self.book.entrs.get(name.to_str()).unwrap().args; + + let relev = |hidden| { + if hidden { + Ambient::Irrelevant + } else { + ambient + } }; - if !self.unify(name.range, *on, fun, true) { - self.err_irrelevant(None, name.range, None) + let args = params + .iter() + .zip(args) + .map(|(param, arg)| (param, self.erase_expr(relev(param.erased), edge, arg))) + .filter(|(param, _)| !param.erased) + .map(|res| res.1) + .collect::>(); + + untyped::Expr::ctr(expr.range, name.clone(), args) + } + Var { name } => { + let var_rev = self + .ctx + .get(&name.to_string()) + .expect(&format!("Uwnraping {}", name.to_string())); + + if *var_rev == Relevance::Irrelevant && ambient != Ambient::Irrelevant { + self.set_relevance(edge, Relevance::Irrelevant, name.range) } - let spine = args - .iter() - .zip(spine) - .map(|(expr, arg)| { - if arg.erased { - ( - self.erase_expr(&(Some(arg.range), Relevance::Irrelevant), expr), - arg, - ) - } else { - (self.erase_expr(on, expr), arg) - } - }) - .filter(|(_, arg)| !arg.erased); - - untyped::Expr::ctr( - expr.range, - name.clone(), - spine.map(|(expr, _)| expr).collect(), - ) + untyped::Expr::var(name.clone()) } Ann { expr, typ } => { - let res = self.erase_expr(on, expr); - self.erase_expr(&(None, Relevance::Irrelevant), typ); - res + let expr = self.erase_expr(ambient, edge, expr); + self.erase_expr(Ambient::Irrelevant, edge, typ); + expr + } + Num { + num: Number::U60(num), + } => untyped::Expr::num60(expr.range, *num), + Num { + num: Number::U120(num), + } => untyped::Expr::num120(expr.range, *num), + Str { val } => { + let nil = QualifiedIdent::new_static("String.nil", None, expr.range); + let cons = QualifiedIdent::new_static("String.cons", None, expr.range); + self.connect_with(edge, &nil, ambient); + self.connect_with(edge, &cons, ambient); + + untyped::Expr::str(expr.range, val.clone()) + } + App { fun, args } => { + let fun = self.erase_expr(ambient, edge, fun); + let mut spine = Vec::new(); + for arg in args { + spine.push(self.erase_expr(ambient, edge, &arg.data)) + } + untyped::Expr::app(expr.range, fun, spine) + } + Sub { expr, .. } => self.erase_expr(ambient, edge, expr), + Binary { op, left, right } => { + let left = self.erase_expr(ambient, edge, left); + let right = self.erase_expr(ambient, edge, right); + untyped::Expr::binary(expr.range, *op, left, right) + } + Typ | NumType { typ: _ } | Hole { num: _ } | Hlp(_) | Err => { + if ambient != Ambient::Irrelevant && ambient != Ambient::Irrelevant { + self.set_relevance(edge, Relevance::Irrelevant, expr.range); + } + untyped::Expr::err(expr.range) } - Sub { expr, .. } => self.erase_expr(on, expr), - Binary { op, left, right } => untyped::Expr::binary( - expr.range, - *op, - self.erase_expr(on, left), - self.erase_expr(on, right), - ), } } - - pub fn erase_rule( - &mut self, - place: &(Option, Relevance), - args: Vec<(Range, bool)>, - rule: &Rule, - ) -> untyped::Rule { - let ctx = self.ctx.clone(); - - let new_pats: Vec<_> = args - .iter() - .zip(rule.pats.iter()) - .map(|((range, erased), expr)| { - ( - erased, - self.erase_pat( - ( - Some(*range), - if *erased { - Relevance::Irrelevant - } else { - place.1.clone() - }, - ), - expr, - ), - ) - }) - .filter(|(erased, _)| !*erased) - .map(|res| res.1) - .collect(); - - let body = self.erase_expr(place, &rule.body); - - self.ctx = ctx; - - untyped::Rule { - name: rule.name.clone(), - pats: new_pats, - body, - range: rule.range, - } - } - - pub fn erase_entry(&mut self, entry: &Entry) -> Box { - let place = if let Some(res) = self.names.get(entry.name.to_str()) { - *res - } else { - self.new_hole(entry.name.range, entry.name.to_string()) - }; - - let args: Vec<(Range, bool)> = entry.args.iter().map(|x| (x.range, x.erased)).collect(); - - let rules = entry - .rules - .iter() - .map(|rule| self.erase_rule(&place, args.clone(), rule)) - .collect::>(); - - Box::new(untyped::Entry { - name: entry.name.clone(), - args: entry.args.iter().filter(|x| !x.erased).map(|x| (x.name.to_string(), x.range, false)).collect(), - rules, - attrs: entry.attrs.clone(), - range: entry.range, - }) - } } diff --git a/crates/kind-pass/src/errors.rs b/crates/kind-pass/src/errors.rs index 6cdc4735..bc3809fd 100644 --- a/crates/kind-pass/src/errors.rs +++ b/crates/kind-pass/src/errors.rs @@ -34,9 +34,7 @@ pub enum PassError { NotATypeConstructor(Range, Range), ShouldBeAParameter(Option, Range), NoFieldCoverage(Range, Vec), - CannotPatternMatchOnErased(Range), UnboundVariable(Vec, Vec), - AttributeDoesNotExpectEqual(Range), AttributeDoesNotExpectArgs(Range), InvalidAttributeArgument(Range), @@ -67,7 +65,6 @@ impl Diagnostic for PassError { PassError::NotATypeConstructor(range, _) => Some(range.ctx), PassError::ShouldBeAParameter(_, range) => Some(range.ctx), PassError::NoFieldCoverage(range, _) => Some(range.ctx), - PassError::CannotPatternMatchOnErased(range) => Some(range.ctx), PassError::UnboundVariable(ranges, _) => Some(ranges[0].range.ctx), PassError::AttributeDoesNotExpectEqual(range) => Some(range.ctx), PassError::AttributeDoesNotExpectArgs(range) => Some(range.ctx), @@ -157,20 +154,6 @@ impl Diagnostic for PassError { main: true, }], }, - PassError::CannotPatternMatchOnErased(place) => DiagnosticFrame { - code: 223, - severity: Severity::Error, - title: "Cannot pattern match on erased arguments.".to_string(), - subtitles: vec![], - hints: vec![], - positions: vec![Marker { - position: *place, - color: Color::Fst, - text: "Here!".to_string(), - no_code: false, - main: true, - }], - }, PassError::RulesWithInconsistentArity(arities) => DiagnosticFrame { code: 201, severity: Severity::Error, diff --git a/crates/kind-target-kdl/src/flatten.rs b/crates/kind-target-kdl/src/flatten.rs index 7bb86f80..3c058f79 100644 --- a/crates/kind-target-kdl/src/flatten.rs +++ b/crates/kind-target-kdl/src/flatten.rs @@ -229,7 +229,7 @@ pub fn flatten(book: untyped::Book) -> untyped::Book { } } - let book = Book { names, entrs, holes: book.holes }; + let book = Book { names, entrs }; book } diff --git a/crates/kind-tree/src/untyped/mod.rs b/crates/kind-tree/src/untyped/mod.rs index 8aec6d48..f600beb8 100644 --- a/crates/kind-tree/src/untyped/mod.rs +++ b/crates/kind-tree/src/untyped/mod.rs @@ -205,8 +205,7 @@ pub struct Entry { #[derive(Clone, Debug, Default)] pub struct Book { pub entrs: LinkedHashMap>, - pub names: FxHashMap, - pub holes: u64, + pub names: FxHashMap } impl Expr {