From b17046aa9d83fb547366a8de68da0ba0845ec684 Mon Sep 17 00:00:00 2001 From: Felipe g Date: Fri, 11 Nov 2022 15:23:56 -0300 Subject: [PATCH] fix: fixed bugs with resolution and erasure --- src/kind-checker/src/compiler/mod.rs | 2 +- src/kind-checker/src/report.rs | 22 ++- src/kind-cli/src/main.rs | 3 +- src/kind-derive/src/matching.rs | 4 +- src/kind-driver/src/resolution.rs | 24 ++- src/kind-parser/src/expr.rs | 6 +- src/kind-parser/src/lexer/mod.rs | 8 +- src/kind-parser/src/lexer/tokens.rs | 1 + src/kind-pass/src/desugar/expr.rs | 2 +- src/kind-pass/src/desugar/top_level.rs | 2 +- src/kind-pass/src/erasure/mod.rs | 224 ++++++++----------------- src/kind-pass/src/unbound/mod.rs | 19 ++- src/kind-tree/src/concrete/expr.rs | 2 +- src/kind-tree/src/desugared/mod.rs | 6 +- 14 files changed, 136 insertions(+), 189 deletions(-) diff --git a/src/kind-checker/src/compiler/mod.rs b/src/kind-checker/src/compiler/mod.rs index c20b1946..a5de0665 100644 --- a/src/kind-checker/src/compiler/mod.rs +++ b/src/kind-checker/src/compiler/mod.rs @@ -206,7 +206,7 @@ fn codegen_all_expr(lhs_rule: bool, lhs: bool, num: &mut usize, quote: bool, exp span_to_num(expr.span), mk_u60(name.encode()), mk_u60(*idx as u64), - mk_u60(*rdx as u64), + mk_var(rdx.to_str()), codegen_all_expr(lhs_rule, lhs, num, quote, expr), ], ), diff --git a/src/kind-checker/src/report.rs b/src/kind-checker/src/report.rs index 830ad2c1..7cb05880 100644 --- a/src/kind-checker/src/report.rs +++ b/src/kind-checker/src/report.rs @@ -13,9 +13,13 @@ pub struct Context(pub Vec); macro_rules! match_opt { ($expr:expr, $pat:pat => $end:expr) => { - match $expr { - $pat => Ok($end), - _ => Err("Error while matching opt".to_string()), + { + match $expr { + $pat => Ok($end), + _ => { + Err("Error while matching opt".to_string()) + }, + } } }; } @@ -57,7 +61,7 @@ fn parse_name(term: &Term) -> Result { match term { Term::Num { numb } => Ok(Ident::decode(*numb)), Term::Ctr { name, args: _ } => Ok(name.to_string()), - _ => Err("Error while matching opt".to_string()), + _ => Err("Error while matching ident".to_string()), } } @@ -65,7 +69,7 @@ fn parse_qualified(term: &Term) -> Result { match term { Term::Num { numb } => Ok(QualifiedIdent::new_static(&Ident::decode(*numb), None, Range::ghost_range())), Term::Ctr { name, args: _ } => Ok(QualifiedIdent::new_static(name, None, Range::ghost_range())), - _ => Err("Error while matching opt".to_string()), + _ => Err("Error while matching qualified".to_string()), } } @@ -102,7 +106,7 @@ fn parse_all_expr(names: im::HashMap, term: &Term) -> Result Ok(Expr::app( @@ -122,10 +126,10 @@ fn parse_all_expr(names: im::HashMap, term: &Term) -> Result Ok(Expr::fun(parse_orig(&args[0])?, parse_qualified(&args[1])?, { + "Kind.Quoted.fun" => Ok(Expr::fun(parse_orig(&args[1])?, parse_qualified(&args[0])?, { let mut res = Vec::new(); - for arg in &args[1..] { - res.push(parse_all_expr(names.clone(), arg)?); + for arg in parse_list(&args[2])? { + res.push(parse_all_expr(names.clone(), &arg)?); } res })), diff --git a/src/kind-cli/src/main.rs b/src/kind-cli/src/main.rs index a4cc8018..4f7774e9 100644 --- a/src/kind-cli/src/main.rs +++ b/src/kind-cli/src/main.rs @@ -141,6 +141,7 @@ pub fn compile_in_session( if diagnostics.is_empty() { render_to_stderr(&render_config, &session, &Log::Checked(start.elapsed())); eprintln!(); + res } else { render_to_stderr(&render_config, &session, &Log::Failed(start.elapsed())); eprintln!(); @@ -148,8 +149,8 @@ pub fn compile_in_session( let diagnostic: Diagnostic = (&diagnostic).into(); render_to_stderr(&render_config, &session, &diagnostic) } + None } - res } fn main() { diff --git a/src/kind-derive/src/matching.rs b/src/kind-derive/src/matching.rs index 537e7cb4..865382e8 100644 --- a/src/kind-derive/src/matching.rs +++ b/src/kind-derive/src/matching.rs @@ -152,7 +152,7 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry { let spine: Vec; if cons.typ.is_none() { - irrelev = sum.indices.extend(&cons.args).map(|x| x.hidden).to_vec(); + irrelev = sum.indices.extend(&cons.args).map(|x| x.erased).to_vec(); spine_params = sum .parameters .extend(&sum.indices) @@ -161,7 +161,7 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry { .to_vec(); spine = sum.indices.extend(&cons.args).map(|x| x.name.with_name(|f| format!("{}_", f))).to_vec(); } else { - irrelev = cons.args.map(|x| x.hidden).to_vec(); + irrelev = cons.args.map(|x| x.erased).to_vec(); spine_params = sum.parameters.extend(&cons.args).map(|x| x.name.with_name(|f| format!("{}_", f))).to_vec(); spine = cons.args.map(|x| x.name.with_name(|f| format!("{}_", f))).to_vec(); } diff --git a/src/kind-driver/src/resolution.rs b/src/kind-driver/src/resolution.rs index f12238cc..0fdab9c5 100644 --- a/src/kind-driver/src/resolution.rs +++ b/src/kind-driver/src/resolution.rs @@ -152,7 +152,7 @@ fn parse_and_store_book_by_identifier<'a>( match ident_to_path(&session.root, ident, true) { Ok(Some(path)) => parse_and_store_book_by_path(session, &path, book), - Ok(None) => false, + Ok(None) => true, Err(err) => { session.diagnostic_sender.send(err).unwrap(); true @@ -165,7 +165,7 @@ fn parse_and_store_book_by_path<'a>( path: &PathBuf, book: &'a mut Book, ) -> bool { - if session.loaded_paths_map.contains_key(path) { + if session.loaded_paths_map.contains_key(&fs::canonicalize(path).unwrap()) { return false; } @@ -181,13 +181,13 @@ fn parse_and_store_book_by_path<'a>( }; let ctx_id = session.book_counter; - session.add_path(Rc::new(path.to_path_buf()), input.clone()); + session.add_path(Rc::new(fs::canonicalize(path).unwrap()), input.clone()); let (mut module, mut failed) = kind_parser::parse_book(session.diagnostic_sender.clone(), ctx_id, &input); let (unbound_vars, unbound_top_level) = - unbound::get_module_unbound(session.diagnostic_sender.clone(), &mut module); + unbound::get_module_unbound(session.diagnostic_sender.clone(), &mut module, false); for idents in unbound_vars.values() { unbound_variable(session, book, idents); @@ -195,9 +195,7 @@ fn parse_and_store_book_by_path<'a>( } for idents in unbound_top_level.values() { - if idents.iter().any(|x| !x.used_by_sugar) { - failed |= parse_and_store_book_by_identifier(session, &idents[0], book); - } + failed |= parse_and_store_book_by_identifier(session, &idents[0], book); } expand_uses(&mut module, session.diagnostic_sender.clone()); @@ -223,7 +221,17 @@ fn unbound_variable(session: &mut Session, book: &Book, idents: &[Ident]) { pub fn parse_and_store_book(session: &mut Session, path: &PathBuf) -> Option { let mut book = Book::default(); - let failed = parse_and_store_book_by_path(session, path, &mut book); + let mut failed = parse_and_store_book_by_path(session, path, &mut book); + + let (_, unbound_tops) = unbound::get_book_unbound(session.diagnostic_sender.clone(), &mut book, true); + + for (_, unbound) in unbound_tops { + let res: Vec = unbound.iter().filter(|x| !x.used_by_sugar).map(|x| x.to_ident()).collect(); + if !res.is_empty() { + unbound_variable(session, &book, &res); + failed = true; + } + } if failed { None diff --git a/src/kind-parser/src/expr.rs b/src/kind-parser/src/expr.rs index a35fb661..d00f25ce 100644 --- a/src/kind-parser/src/expr.rs +++ b/src/kind-parser/src/expr.rs @@ -95,13 +95,13 @@ impl<'a> Parser<'a> { self.advance(); // '##' let name = self.parse_id()?; self.eat_variant(Token::Slash)?; - let redx = self.parse_num_lit()?; + let redx = self.parse_id()?; let expr = self.parse_expr(false)?; let range = start.mix(expr.range); Ok(Box::new(Expr { data: ExprKind::Subst(Substitution { name, - redx: redx as usize, + redx, indx: 0, expr, }), @@ -311,7 +311,7 @@ impl<'a> Parser<'a> { let range = self.range(); self.advance(); // '(' let mut expr = self.parse_expr(true)?; - if self.get().same_variant(&Token::Colon) { + if self.get().same_variant(&Token::ColonColon) { self.advance(); // ':' let typ = self.parse_expr(false)?; let range = range.mix(self.range()); diff --git a/src/kind-parser/src/lexer/mod.rs b/src/kind-parser/src/lexer/mod.rs index 7b1482e7..5c9011a4 100644 --- a/src/kind-parser/src/lexer/mod.rs +++ b/src/kind-parser/src/lexer/mod.rs @@ -170,7 +170,13 @@ impl<'a> Lexer<'a> { _ => (Token::Slash, self.mk_range(start)), } } - ':' => self.single_token(Token::Colon, start), + ':' => { + self.next_char(); + match self.peekable.peek() { + Some(':') => self.single_token(Token::ColonColon, start), + _ => (Token::Colon, self.mk_range(start)), + } + } ';' => self.single_token(Token::Semi, start), '$' => self.single_token(Token::Dollar, start), ',' => self.single_token(Token::Comma, start), diff --git a/src/kind-parser/src/lexer/tokens.rs b/src/kind-parser/src/lexer/tokens.rs index facfaf96..6334084f 100644 --- a/src/kind-parser/src/lexer/tokens.rs +++ b/src/kind-parser/src/lexer/tokens.rs @@ -21,6 +21,7 @@ pub enum Token { DotDot, // .. Dot, // . Tilde, // ~ + ColonColon, // :: Help(String), LowerId(String), diff --git a/src/kind-pass/src/desugar/expr.rs b/src/kind-pass/src/desugar/expr.rs index 7f567763..643af9b7 100644 --- a/src/kind-pass/src/desugar/expr.rs +++ b/src/kind-pass/src/desugar/expr.rs @@ -33,7 +33,7 @@ impl<'a> DesugarState<'a> { range, sub.name.clone(), sub.indx, - sub.redx, + sub.redx.clone(), self.desugar_expr(&sub.expr), ) } diff --git a/src/kind-pass/src/desugar/top_level.rs b/src/kind-pass/src/desugar/top_level.rs index 2e7301fe..b9d89a42 100644 --- a/src/kind-pass/src/desugar/top_level.rs +++ b/src/kind-pass/src/desugar/top_level.rs @@ -255,6 +255,7 @@ impl<'a> DesugarState<'a> { pub fn desugar_pat(&mut self, pat: &concrete::pat::Pat) -> Box { match &pat.data { concrete::pat::PatKind::App(head, spine) => { + // TODO: Fix lol let entry = self .old_book .count @@ -282,7 +283,6 @@ impl<'a> DesugarState<'a> { } } } else if entry.arguments.len() != spine.len() { - println!("Ata {} {:?}", head, spine.iter().map(|x| x.to_string()).collect::>()); self.send_err(PassError::IncorrectArity( head.range, spine.iter().map(|x| x.range).collect(), diff --git a/src/kind-pass/src/erasure/mod.rs b/src/kind-pass/src/erasure/mod.rs index 26893e68..2bbc76e3 100644 --- a/src/kind-pass/src/erasure/mod.rs +++ b/src/kind-pass/src/erasure/mod.rs @@ -9,6 +9,8 @@ // 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}; @@ -16,7 +18,10 @@ use fxhash::{FxHashMap, FxHashSet}; use kind_report::data::DiagnosticFrame; use kind_span::Range; -use kind_tree::{desugared::{Book, Entry, Expr, ExprKind, Rule, self}, symbol::{QualifiedIdent}}; +use kind_tree::{ + desugared::{self, Book, Entry, Expr, ExprKind, Rule}, + symbol::QualifiedIdent, +}; use crate::errors::PassError; @@ -37,11 +42,7 @@ pub struct ErasureState<'a> { failed: bool, } -pub fn erase_book( - book: &Book, - errs: Sender, - entrypoint: FxHashSet, -) -> Option { +pub fn erase_book(book: &Book, errs: Sender, entrypoint: FxHashSet) -> Option { let mut state = ErasureState { errs, book, @@ -60,9 +61,7 @@ pub fn erase_book( for name in entrypoint { let count = state.holes.len(); - state - .names - .insert(name.to_string(), (None, Relevance::Hole(count))); + state.names.insert(name.to_string(), (None, Relevance::Hole(count))); state.holes.push(Some(Relevance::Relevant)); } @@ -102,15 +101,8 @@ impl<'a> ErasureState<'a> { local_relevance } - pub fn err_irrelevant( - &mut self, - declared_val: Option, - used: Range, - declared_ty: Option, - ) { - self.errs - .send(PassError::CannotUseIrrelevant(declared_val, used, declared_ty).into()) - .unwrap(); + pub fn err_irrelevant(&mut self, declared_val: Option, used: Range, declared_ty: Option) { + self.errs.send(PassError::CannotUseIrrelevant(declared_val, used, declared_ty).into()).unwrap(); self.failed = true; } @@ -131,83 +123,38 @@ impl<'a> ErasureState<'a> { } } - pub fn unify_hole( - &mut self, - range: Range, - hole: (Option, usize), - right: (Option, Relevance), - visited: &mut FxHashSet, - inverted: bool, - relevance_unify: bool, - ) -> bool { - match (self.holes[hole.1], right.1) { - (Some(Relevance::Hole(n)), t) => { - visited.insert(n); - if visited.contains(&n) { - self.holes[hole.1] = Some(t); - true - } else { - self.unify_hole( - range, - (hole.0, n), - right, - visited, - inverted, - relevance_unify, - ) - } - } - (_, Relevance::Relevant) => true, - (Some(l), _) => { - if inverted { - self.unify_loop(range, right, (hole.0, l), visited, relevance_unify) - } else { - self.unify_loop(range, (hole.0, l), right, visited, relevance_unify) - } - } - (None, r) => { - self.holes[hole.1] = Some(r); - true - } - } - } - - pub fn unify_loop( - &mut self, - range: Range, - left: (Option, Relevance), - right: (Option, Relevance), - visited: &mut FxHashSet, - relevance_unify: bool, - ) -> bool { + 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)) => { - self.unify_hole(range, (right.0, hole), left, visited, true, relevance_unify) - } - (Relevance::Hole(hole), _) => self.unify_hole( - range, - (left.0, hole), - right, - visited, - false, - relevance_unify, - ), - - (Relevance::Irrelevant, Relevance::Irrelevant) - | (Relevance::Irrelevant, Relevance::Relevant) - | (Relevance::Relevant, Relevance::Relevant) => true, - + (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) + } + (None, Relevance::Irrelevant) => { + self.holes[hole] = Some(t); + 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 { + 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) } @@ -224,15 +171,7 @@ impl<'a> ErasureState<'a> { let entry = self.book.entrs.get(name.to_string().as_str()).unwrap(); let erased = entry.args.iter(); - let irrelevances = erased.map(|arg| { - if on.1 == Relevance::Irrelevant { - on - } else if arg.erased { - (Some(arg.span), Relevance::Irrelevant) - } else { - (Some(arg.span), Relevance::Relevant) - } - }); + let irrelevances = erased.map(|arg| if arg.erased { (Some(arg.span), Relevance::Irrelevant) } else { on }); spine .iter() @@ -340,30 +279,28 @@ impl<'a> ErasureState<'a> { } App(head, spine) => { let head = self.erase_expr(on, head); - let spine = spine.iter().map(|x| { - let on = if x.erased { - (x.data.span.to_range(), Relevance::Irrelevant) - } else { - on.clone() - }; - desugared::AppBinding { - data: self.erase_expr(&on, &x.data), - erased: x.erased - } - }).filter(|x| !x.erased).collect(); + let spine = spine + .iter() + .map(|x| { + let on = if x.erased { + (x.data.span.to_range(), Relevance::Irrelevant) + } else { + (x.data.span.to_range(), Relevance::Relevant) + }; + desugared::AppBinding { + data: self.erase_expr(&on, &x.data), + erased: x.erased, + } + }) + .filter(|x| !x.erased) + .collect(); Box::new(Expr { span: expr.span, data: ExprKind::App(head, spine), }) } Fun(head, spine) => { - let args = self - .book - .entrs - .get(head.to_string().as_str()) - .unwrap() - .args - .iter(); + let args = self.book.entrs.get(head.to_string().as_str()).unwrap().args.iter(); let fun = match self.names.get(&head.to_string()) { Some(res) => *res, @@ -378,13 +315,11 @@ impl<'a> ErasureState<'a> { .iter() .zip(args) .map(|(expr, arg)| { - ( - self.erase_expr( - &(Some(arg.span), erasure_to_relevance(arg.erased)), - expr, - ), - arg, - ) + if arg.erased { + (self.erase_expr(&(Some(arg.span), Relevance::Irrelevant), expr), arg) + } else { + (self.erase_expr(on, expr), arg) + } }) .filter(|(_, arg)| !arg.erased); @@ -394,13 +329,7 @@ impl<'a> ErasureState<'a> { }) } Ctr(head, spine) => { - let args = self - .book - .entrs - .get(head.to_string().as_str()) - .unwrap() - .args - .iter(); + let args = self.book.entrs.get(head.to_string().as_str()).unwrap().args.iter(); let fun = match self.names.get(&head.to_string()) { Some(res) => *res, @@ -415,13 +344,11 @@ impl<'a> ErasureState<'a> { .iter() .zip(args) .map(|(expr, arg)| { - ( - self.erase_expr( - &(Some(arg.span), erasure_to_relevance(arg.erased)), - expr, - ), - arg, - ) + if arg.erased { + (self.erase_expr(&(Some(arg.span), Relevance::Irrelevant), expr), arg) + } else { + (self.erase_expr(on, expr), arg) + } }) .filter(|(_, arg)| !arg.erased); @@ -443,19 +370,13 @@ impl<'a> ErasureState<'a> { } } - pub fn erase_rule( - &mut self, - place: &(Option, Relevance), - args: Vec<(Range, bool)>, - rule: &Rule, - ) -> Rule { + pub fn erase_rule(&mut self, place: &(Option, Relevance), args: Vec<(Range, bool)>, rule: &Rule) -> Rule { let ctx = self.ctx.clone(); - let new_pats : Vec<_> = args.iter() + let new_pats: Vec<_> = args + .iter() .zip(rule.pats.iter()) - .map(|((range, erased), expr)| { - (erased, self.erase_pat((Some(*range), erasure_to_relevance(*erased)), expr)) - }) + .map(|((range, erased), expr)| (erased, self.erase_pat((Some(*range), erasure_to_relevance(*erased)), expr))) .filter(|(erased, _)| !*erased) .map(|res| res.1) .collect(); @@ -480,15 +401,12 @@ impl<'a> ErasureState<'a> { }; let args: Vec<(Range, bool)> = entry.args.iter().map(|x| (x.span, x.erased)).collect(); - let rules = entry - .rules - .iter() - .map(|rule| self.erase_rule(&place, args.clone(), rule)); + let rules = entry.rules.iter().map(|rule| self.erase_rule(&place, args.clone(), rule)).collect::>(); Box::new(Entry { name: entry.name.clone(), args: entry.args.clone(), typ: entry.typ.clone(), - rules: rules.collect(), + rules, attrs: entry.attrs.clone(), span: entry.span, }) diff --git a/src/kind-pass/src/unbound/mod.rs b/src/kind-pass/src/unbound/mod.rs index 26996354..b69397d4 100644 --- a/src/kind-pass/src/unbound/mod.rs +++ b/src/kind-pass/src/unbound/mod.rs @@ -30,15 +30,17 @@ pub struct UnboundCollector { pub context_vars: Vec<(Range, String)>, pub unbound_top_level: FxHashMap>, pub unbound: FxHashMap>, + pub emit_errs: bool } impl UnboundCollector { - pub fn new(diagnostic_sender: Sender) -> UnboundCollector { + pub fn new(diagnostic_sender: Sender, emit_errs: bool) -> UnboundCollector { Self { errors: diagnostic_sender, context_vars: Default::default(), unbound_top_level: Default::default(), unbound: Default::default(), + emit_errs } } } @@ -46,11 +48,12 @@ impl UnboundCollector { pub fn get_module_unbound( diagnostic_sender: Sender, module: &mut Module, + emit_errs: bool, ) -> ( FxHashMap>, FxHashMap>, ) { - let mut state = UnboundCollector::new(diagnostic_sender); + let mut state = UnboundCollector::new(diagnostic_sender, emit_errs); state.visit_module(module); (state.unbound, state.unbound_top_level) } @@ -58,11 +61,12 @@ pub fn get_module_unbound( pub fn get_book_unbound( diagnostic_sender: Sender, book: &mut Book, + emit_errs: bool, ) -> ( FxHashMap>, FxHashMap>, ) { - let mut state = UnboundCollector::new(diagnostic_sender); + let mut state = UnboundCollector::new(diagnostic_sender, emit_errs); state.visit_book(book); (state.unbound, state.unbound_top_level) } @@ -100,9 +104,11 @@ impl Visitor for UnboundCollector { .iter() .find(|x| x.1 == ident.0.data.to_string()) { - self.errors + if self.emit_errs { + self.errors .send(PassError::RepeatedVariable(fst.0, ident.0.range).into()) .unwrap() + } } else { self.context_vars.push((ident.0.range, ident.0.to_string())) } @@ -120,9 +126,11 @@ impl Visitor for UnboundCollector { .find(|x| x.1 == argument.name.to_string()); if let Some(fst) = res { - self.errors + if self.emit_errs { + self.errors .send(PassError::RepeatedVariable(fst.0, argument.name.range).into()) .unwrap() + } } else { self.context_vars .push((argument.name.range, argument.name.to_string())) @@ -412,6 +420,7 @@ impl Visitor for UnboundCollector { } ExprKind::Subst(subst) => { self.visit_ident(&mut subst.name); + self.visit_ident(&mut subst.redx); if let Some(pos) = self .context_vars diff --git a/src/kind-tree/src/concrete/expr.rs b/src/kind-tree/src/concrete/expr.rs index b219ee6c..54daa5ce 100644 --- a/src/kind-tree/src/concrete/expr.rs +++ b/src/kind-tree/src/concrete/expr.rs @@ -74,7 +74,7 @@ pub struct Match { #[derive(Clone, Debug, Hash, PartialEq, Eq)] pub struct Substitution { pub name: Ident, - pub redx: usize, + pub redx: Ident, pub indx: usize, pub expr: Box, } diff --git a/src/kind-tree/src/desugared/mod.rs b/src/kind-tree/src/desugared/mod.rs index 0e9d7b47..d3dc5b54 100644 --- a/src/kind-tree/src/desugared/mod.rs +++ b/src/kind-tree/src/desugared/mod.rs @@ -42,7 +42,7 @@ pub enum ExprKind { /// Type ascription (x : y) Ann(Box, Box), /// Substitution - Sub(Ident, usize, usize, Box), + Sub(Ident, usize, Ident, Box), /// Type Literal Typ, /// Primitive numeric types @@ -91,7 +91,7 @@ impl Expr { }) } - pub fn sub(range: Range, ident: Ident, idx: usize, rdx: usize, body: Box) -> Box { + pub fn sub(range: Range, ident: Ident, idx: usize, rdx: Ident, body: Box) -> Box { Box::new(Expr { span: Span::Locatable(range), data: ExprKind::Sub(ident, idx, rdx, body), @@ -337,7 +337,7 @@ impl Display for Expr { Var(name) => write!(f, "{}", name), Lambda(binder, body, false) => write!(f, "({} => {})", binder, body), Lambda(binder, body, true) => write!(f, "({{{}}} => {})", binder, body), - Sub(name, _, redx, expr) => write!(f, "({} ## {}/{})", expr, name, redx), + Sub(name, _, redx, expr) => write!(f, "(## {}/{} {})",name, redx, expr), App(head, spine) => write!( f, "({}{})",