From 2c9285ab94851c07c1858ee8a7425a0ccecf6d59 Mon Sep 17 00:00:00 2001 From: felipegchi Date: Tue, 15 Nov 2022 13:28:48 -0300 Subject: [PATCH] fix: some fixes and cargo fmt --- Cargo.lock | 128 +++++++++ rustfmt.toml | 1 - src/kind-checker/src/compiler/mod.rs | 158 ++++++++--- src/kind-checker/src/lib.rs | 5 +- src/kind-checker/src/report.rs | 105 +++++--- src/kind-cli/src/lib.rs | 3 +- src/kind-cli/src/main.rs | 2 +- src/kind-cli/tests/mod.rs | 48 ++-- .../tests/suite/checker/derive/Eq.golden | 25 ++ .../tests/suite/checker/derive/Eq.kind2 | 6 + .../tests/suite/checker/derive/Nat.golden | 1 + .../tests/suite/checker/derive/Nat.kind2 | 8 + .../tests/suite/checker/derive/Vec.golden | 1 + .../tests/suite/checker/derive/Vec.kind2 | 10 + src/kind-derive/src/matching.rs | 99 +++++-- src/kind-derive/src/open.rs | 5 +- src/kind-driver/src/errors.rs | 80 +++--- src/kind-driver/src/lib.rs | 2 +- src/kind-driver/src/resolution.rs | 79 +++--- src/kind-optimization/Cargo.toml | 8 - src/kind-optimization/src/lib.rs | 14 - src/kind-parser/src/errors.rs | 2 +- src/kind-parser/src/expr.rs | 83 ++++-- src/kind-parser/src/lexer/state.rs | 6 +- src/kind-parser/src/lexer/tokens.rs | 69 +++++ src/kind-pass/src/desugar/app.rs | 2 +- src/kind-pass/src/desugar/destruct.rs | 7 +- src/kind-pass/src/desugar/expr.rs | 2 +- src/kind-pass/src/desugar/mod.rs | 2 +- src/kind-pass/src/erasure/mod.rs | 106 ++++++-- src/kind-pass/src/errors.rs | 245 +++++++++--------- src/kind-pass/src/lib.rs | 2 +- src/kind-pass/src/unbound/mod.rs | 87 ++++--- src/kind-report/src/report.rs | 4 +- src/kind-target-hvm/src/lib.rs | 8 +- src/kind-tree/src/concrete/expr.rs | 16 +- src/kind-tree/src/desugared/mod.rs | 16 +- src/kind-tree/src/symbol.rs | 22 +- 38 files changed, 1008 insertions(+), 459 deletions(-) delete mode 100644 rustfmt.toml create mode 100644 src/kind-cli/tests/suite/checker/derive/Eq.golden create mode 100644 src/kind-cli/tests/suite/checker/derive/Eq.kind2 create mode 100644 src/kind-cli/tests/suite/checker/derive/Nat.golden create mode 100644 src/kind-cli/tests/suite/checker/derive/Nat.kind2 create mode 100644 src/kind-cli/tests/suite/checker/derive/Vec.golden create mode 100644 src/kind-cli/tests/suite/checker/derive/Vec.kind2 delete mode 100644 src/kind-optimization/Cargo.toml delete mode 100644 src/kind-optimization/src/lib.rs diff --git a/Cargo.lock b/Cargo.lock index e35de384..4792cb31 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -190,6 +190,16 @@ dependencies = [ "cfg-if", ] +[[package]] +name = "ctor" +version = "0.1.26" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6d2301688392eb071b0bf1a37be05c469d3cc4dbbd95df672fe28ab021e6a096" +dependencies = [ + "quote", + "syn", +] + [[package]] name = "dashmap" version = "5.4.0" @@ -203,6 +213,12 @@ dependencies = [ "parking_lot_core", ] +[[package]] +name = "diff" +version = "0.1.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "56254986775e3233ffa9c4d7d3faaf6d36a2c09d30b20687e9f88bc8bafc16c8" + [[package]] name = "either" version = "1.8.0" @@ -601,6 +617,9 @@ dependencies = [ "kind-checker", "kind-driver", "kind-report", + "ntest", + "pretty_assertions", + "walkdir", ] [[package]] @@ -660,6 +679,7 @@ version = "0.1.0" dependencies = [ "fxhash", "kind-span", + "pathdiff", "unicode-width", "yansi", ] @@ -819,6 +839,47 @@ dependencies = [ "notify", ] +[[package]] +name = "ntest" +version = "0.8.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e865500b46e35210765d62d549178c520badc018b2a71a827c29b305d680d1fb" +dependencies = [ + "ntest_proc_macro_helper", + "ntest_test_cases", + "ntest_timeout", +] + +[[package]] +name = "ntest_proc_macro_helper" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a0e328d267a679d683b55222b3d06c2fb7358220857945bfc4e65a6b531e9994" + +[[package]] +name = "ntest_test_cases" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6f7caf063242bb66721e74515dc01a915901063fa1f994bee7a2b9136f13370e" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "ntest_timeout" +version = "0.8.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bca6eaadc7c104fb2eb0c6d14782b9e33775aaf5584c3bcb0f87c89e3e6d6c07" +dependencies = [ + "ntest_proc_macro_helper", + "proc-macro-crate", + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "num_cpus" version = "1.14.0" @@ -886,6 +947,15 @@ version = "6.3.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3baf96e39c5359d2eb0dd6ccb42c62b91d9678aa68160d261b9e0ccbf9e9dea9" +[[package]] +name = "output_vt100" +version = "0.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "628223faebab4e3e40667ee0b2336d34a5b960ff60ea743ddfdbcf7770bcfb66" +dependencies = [ + "winapi", +] + [[package]] name = "parking_lot_core" version = "0.9.4" @@ -899,6 +969,12 @@ dependencies = [ "windows-sys 0.42.0", ] +[[package]] +name = "pathdiff" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8835116a5c179084a830efb3adc117ab007512b535bc1a21c991d3b32a6b44dd" + [[package]] name = "percent-encoding" version = "2.2.0" @@ -923,6 +999,29 @@ version = "0.3.26" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6ac9a59f73473f1b8d852421e59e64809f025994837ef743615c6d0c5b305160" +[[package]] +name = "pretty_assertions" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a25e9bcb20aa780fd0bb16b72403a9064d6b3f22f026946029acb941a50af755" +dependencies = [ + "ctor", + "diff", + "output_vt100", + "yansi", +] + +[[package]] +name = "proc-macro-crate" +version = "1.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "eda0fc3b0fb7c975631757e14d9049da17374063edb6ebbcbc54d880d4fe94e9" +dependencies = [ + "once_cell", + "thiserror", + "toml", +] + [[package]] name = "proc-macro-error" version = "1.0.4" @@ -1216,6 +1315,26 @@ version = "0.16.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "222a222a5bfe1bba4a77b45ec488a741b3cb8872e5e499451fd7d0129c9c7c3d" +[[package]] +name = "thiserror" +version = "1.0.37" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "10deb33631e3c9018b9baf9dcbbc4f737320d2b576bac10f6aefa048fa407e3e" +dependencies = [ + "thiserror-impl", +] + +[[package]] +name = "thiserror-impl" +version = "1.0.37" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "982d17546b47146b28f7c22e3d08465f6b8903d0ea13c1660d9d84a6e7adcdbb" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "tinyvec" version = "1.6.0" @@ -1272,6 +1391,15 @@ dependencies = [ "tracing", ] +[[package]] +name = "toml" +version = "0.5.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8d82e1a7758622a465f8cee077614c73484dac5b836c02ff6a40d5d1010324d7" +dependencies = [ + "serde", +] + [[package]] name = "tower-service" version = "0.3.2" diff --git a/rustfmt.toml b/rustfmt.toml deleted file mode 100644 index 37eebf90..00000000 --- a/rustfmt.toml +++ /dev/null @@ -1 +0,0 @@ -max_width = 180 \ No newline at end of file diff --git a/src/kind-checker/src/compiler/mod.rs b/src/kind-checker/src/compiler/mod.rs index 091dc3c1..24f24fc4 100644 --- a/src/kind-checker/src/compiler/mod.rs +++ b/src/kind-checker/src/compiler/mod.rs @@ -60,7 +60,9 @@ fn mk_ctr(name: String, args: Vec>) -> Box { } fn mk_var(ident: &str) -> Box { - Box::new(Term::Var { name: ident.to_string() }) + Box::new(Term::Var { + name: ident.to_string(), + }) } fn mk_u60(numb: u64) -> Box { @@ -68,7 +70,10 @@ fn mk_u60(numb: u64) -> Box { } fn mk_single_ctr(head: String) -> Box { - Box::new(Term::Ctr { name: head, args: vec![] }) + Box::new(Term::Ctr { + name: head, + args: vec![], + }) } fn mk_ctr_name(ident: &QualifiedIdent) -> Box { @@ -77,15 +82,26 @@ fn mk_ctr_name(ident: &QualifiedIdent) -> Box { } fn span_to_num(span: Span) -> Box { - Box::new(Term::Num { numb: span.encode().0 }) + Box::new(Term::Num { + numb: span.encode().0, + }) } fn set_origin(ident: &Ident) -> Box { - mk_quoted_ctr("Kind.Term.set_origin".to_owned(), vec![span_to_num(Span::Locatable(ident.range)), mk_var(ident.to_str())]) + mk_quoted_ctr( + "Kind.Term.set_origin".to_owned(), + vec![ + span_to_num(Span::Locatable(ident.range)), + mk_var(ident.to_str()), + ], + ) } fn lam(name: &Ident, body: Box) -> Box { - Box::new(Term::Lam { name: name.to_string(), body }) + Box::new(Term::Lam { + name: name.to_string(), + body, + }) } fn codegen_str(input: &str) -> Box { @@ -103,12 +119,20 @@ fn codegen_str(input: &str) -> Box { ) } -fn codegen_all_expr(lhs_rule: bool, lhs: bool, num: &mut usize, quote: bool, expr: &Expr) -> Box { +fn codegen_all_expr( + lhs_rule: bool, + lhs: bool, + num: &mut usize, + quote: bool, + expr: &Expr, +) -> Box { use kind_tree::desugared::ExprKind::*; match &expr.data { Typ => mk_quoted_ctr(eval_ctr(quote, TermTag::Typ), vec![span_to_num(expr.span)]), - NumType(desugared::NumType::U60) => mk_quoted_ctr(eval_ctr(quote, TermTag::U60), vec![span_to_num(expr.span)]), + NumType(desugared::NumType::U60) => { + mk_quoted_ctr(eval_ctr(quote, TermTag::U60), vec![span_to_num(expr.span)]) + } NumType(desugared::NumType::U120) => todo!(), Var(ident) => { if quote && !lhs { @@ -117,7 +141,11 @@ fn codegen_all_expr(lhs_rule: bool, lhs: bool, num: &mut usize, quote: bool, exp *num += 1; mk_quoted_ctr( eval_ctr(quote, TermTag::Var), - vec![span_to_num(expr.span), mk_u60(ident.encode()), mk_u60((*num - 1) as u64)], + vec![ + span_to_num(expr.span), + mk_u60(ident.encode()), + mk_u60((*num - 1) as u64), + ], ) } else { mk_var(ident.to_str()) @@ -134,24 +162,25 @@ fn codegen_all_expr(lhs_rule: bool, lhs: bool, num: &mut usize, quote: bool, exp ), Lambda(name, body, _erased) => mk_quoted_ctr( eval_ctr(quote, TermTag::Lambda), - vec![span_to_num(expr.span), mk_u60(name.encode()), lam(name, codegen_all_expr(lhs_rule, lhs, num, quote, body))], + vec![ + span_to_num(expr.span), + mk_u60(name.encode()), + lam(name, codegen_all_expr(lhs_rule, lhs, num, quote, body)), + ], + ), + App(head, spine) => spine.iter().fold( + codegen_all_expr(lhs_rule, lhs, num, quote, head), + |left, right| { + mk_quoted_ctr( + eval_ctr(quote, TermTag::App), + vec![ + span_to_num(expr.span), + left, + codegen_all_expr(lhs_rule, lhs, num, quote, &right.data), + ], + ) + }, ), - App(head, spine) => spine.iter().fold(codegen_all_expr(lhs_rule, lhs, num, quote, head), |left, right| { - mk_quoted_ctr( - eval_ctr(quote, TermTag::App), - vec![ - span_to_num(expr.span), - left, - codegen_all_expr( - lhs_rule, - lhs, - num, - quote, - &right.data - ), - ], - ) - }), Ctr(name, spine) => mk_quoted_ctr( eval_ctr(quote, TermTag::Ctr(spine.len())), vec_preppend![ @@ -161,7 +190,11 @@ fn codegen_all_expr(lhs_rule: bool, lhs: bool, num: &mut usize, quote: bool, exp ], ), Fun(name, spine) => { - let new_spine: Vec> = spine.iter().cloned().map(|x| codegen_all_expr(lhs_rule, lhs, num, quote, &x)).collect(); + let new_spine: Vec> = spine + .iter() + .cloned() + .map(|x| codegen_all_expr(lhs_rule, lhs, num, quote, &x)) + .collect(); if quote { mk_quoted_ctr( eval_ctr(quote, TermTag::Fun(new_spine.len())), @@ -198,17 +231,20 @@ fn codegen_all_expr(lhs_rule: bool, lhs: bool, num: &mut usize, quote: bool, exp codegen_all_expr(lhs_rule, lhs, num, quote, typ), ], ), - Sub(name, idx, rdx, expr) => mk_quoted_ctr( + Sub(name, idx, rdx, inside) => mk_quoted_ctr( eval_ctr(quote, TermTag::Sub), vec![ span_to_num(expr.span), mk_u60(name.encode()), mk_u60(*idx as u64), - mk_var(rdx.to_str()), - codegen_all_expr(lhs_rule, lhs, num, quote, expr), + mk_u60(*rdx as u64), + codegen_all_expr(lhs_rule, lhs, num, quote, inside), ], ), - Num(desugared::Num::U60(n)) => mk_quoted_ctr(eval_ctr(quote, TermTag::Num), vec![span_to_num(expr.span), mk_u60(*n)]), + Num(desugared::Num::U60(n)) => mk_quoted_ctr( + eval_ctr(quote, TermTag::Num), + vec![span_to_num(expr.span), mk_u60(*n)], + ), Num(desugared::Num::U120(_)) => todo!(), Binary(operator, left, right) => mk_quoted_ctr( eval_ctr(quote, TermTag::Binary), @@ -219,7 +255,10 @@ fn codegen_all_expr(lhs_rule: bool, lhs: bool, num: &mut usize, quote: bool, exp codegen_all_expr(lhs_rule, lhs, num, quote, right), ], ), - Hole(num) => mk_quoted_ctr(eval_ctr(quote, TermTag::Hole), vec![span_to_num(expr.span), mk_u60(*num)]), + Hole(num) => mk_quoted_ctr( + eval_ctr(quote, TermTag::Hole), + vec![span_to_num(expr.span), mk_u60(*num)], + ), Hlp(_) => mk_quoted_ctr(eval_ctr(quote, TermTag::Hlp), vec![span_to_num(expr.span)]), Str(input) => codegen_str(input), Err => panic!("Internal Error: Was not expecting an ERR node inside the HVM checker"), @@ -255,11 +294,17 @@ fn codegen_vec(exprs: T) -> Box where T: Iterator>, { - exprs.fold(mk_ctr("List.nil".to_string(), vec![]), |left, right| mk_ctr("List.cons".to_string(), vec![right, left])) + exprs.fold(mk_ctr("List.nil".to_string(), vec![]), |left, right| { + mk_ctr("List.cons".to_string(), vec![right, left]) + }) } fn codegen_rule_end(file: &mut lang::File, rule: &desugared::Rule) { - let base_vars = lift_spine((0..rule.pats.len()).map(|x| mk_var(&format!("x{}", x))).collect::>>()); + let base_vars = lift_spine( + (0..rule.pats.len()) + .map(|x| mk_var(&format!("x{}", x))) + .collect::>>(), + ); file.rules.push(lang::Rule { lhs: mk_ctr( @@ -301,7 +346,11 @@ fn codegen_rule_end(file: &mut lang::File, rule: &desugared::Rule) { fn codegen_rule(file: &mut lang::File, rule: &desugared::Rule) { let mut count = 0; - let lhs_args = rule.pats.iter().map(|x| codegen_pattern(&mut count, false, x)).collect::>>(); + let lhs_args = rule + .pats + .iter() + .map(|x| codegen_pattern(&mut count, false, x)) + .collect::>>(); file.rules.push(lang::Rule { lhs: mk_ctr( @@ -318,9 +367,21 @@ fn codegen_rule(file: &mut lang::File, rule: &desugared::Rule) { file.rules.push(lang::Rule { lhs: mk_ctr( TermTag::HoasF(rule.name.to_string()).to_string(), - vec![mk_var("orig"), mk_var("a"), mk_var("r"), mk_var("log"), mk_var("ret")], + vec![ + mk_var("orig"), + mk_var("a"), + mk_var("r"), + mk_var("log"), + mk_var("ret"), + ], + ), + rhs: mk_ctr( + "HVM.put".to_owned(), + vec![ + mk_ctr("Kind.Term.show".to_owned(), vec![mk_var("log")]), + mk_var("ret"), + ], ), - rhs: mk_ctr("HVM.put".to_owned(), vec![mk_ctr("Kind.Term.show".to_owned(), vec![mk_var("log")]), mk_var("ret")]), }); } else { file.rules.push(lang::Rule { @@ -336,7 +397,13 @@ fn codegen_rule(file: &mut lang::File, rule: &desugared::Rule) { } } -fn codegen_entry_rules(count: &mut usize, index: usize, args: &mut Vec>, entry: &desugared::Rule, pats: &[Box]) -> Box { +fn codegen_entry_rules( + count: &mut usize, + index: usize, + args: &mut Vec>, + entry: &desugared::Rule, + pats: &[Box], +) -> Box { if pats.is_empty() { mk_ctr( "Kind.Rule.rhs".to_owned(), @@ -353,7 +420,13 @@ fn codegen_entry_rules(count: &mut usize, index: usize, args: &mut Vec let pat = &pats[0]; let expr = codegen_all_expr(true, false, count, false, pat); args.push(expr.clone()); - mk_ctr("Kind.Rule.lhs".to_owned(), vec![expr, codegen_entry_rules(count, index + 1, args, entry, &pats[1..])]) + mk_ctr( + "Kind.Rule.lhs".to_owned(), + vec![ + expr, + codegen_entry_rules(count, index + 1, args, entry, &pats[1..]), + ], + ) } } @@ -373,7 +446,9 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) { rhs: codegen_type(&entry.args, &entry.typ), }); - let base_vars = (0..entry.args.len()).map(|x| mk_var(&format!("x{}", x))).collect::>>(); + let base_vars = (0..entry.args.len()) + .map(|x| mk_var(&format!("x{}", x))) + .collect::>>(); file.rules.push(lang::Rule { lhs: mk_ctr( @@ -419,7 +494,10 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) { codegen_rule_end(file, &entry.rules[0]) } - let rules = entry.rules.iter().map(|rule| codegen_entry_rules(&mut 0, 0, &mut Vec::new(), rule, &rule.pats)); + let rules = entry + .rules + .iter() + .map(|rule| codegen_entry_rules(&mut 0, 0, &mut Vec::new(), rule, &rule.pats)); file.rules.push(lang::Rule { lhs: mk_ctr("RuleOf".to_owned(), vec![mk_ctr_name(&entry.name)]), diff --git a/src/kind-checker/src/lib.rs b/src/kind-checker/src/lib.rs index 7e4fa17b..0776494f 100644 --- a/src/kind-checker/src/lib.rs +++ b/src/kind-checker/src/lib.rs @@ -4,8 +4,8 @@ //! version that the Rust side can manipulate. pub mod compiler; -pub mod report; mod errors; +pub mod report; use std::sync::mpsc::Sender; @@ -38,7 +38,8 @@ pub fn type_check(book: &Book, tx: Sender) -> bool { runtime.normalize(main); let term = runtime.readback(main); - let errs = parse_report(&term).expect("Internal Error: Cannot parse the report message from the type checker"); + let errs = parse_report(&term) + .expect("Internal Error: Cannot parse the report message from the type checker"); let succeeded = errs.is_empty(); for err in errs { diff --git a/src/kind-checker/src/report.rs b/src/kind-checker/src/report.rs index e3dba4ea..d140700b 100644 --- a/src/kind-checker/src/report.rs +++ b/src/kind-checker/src/report.rs @@ -15,16 +15,12 @@ type Entry = (String, Box, Vec>); 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()) - }, - } + ($expr:expr, $pat:pat => $end:expr) => {{ + match $expr { + $pat => Ok($end), + _ => Err("Error while matching opt".to_string()), } - }; + }}; } fn parse_orig(term: &Term) -> Result { @@ -70,8 +66,14 @@ fn parse_name(term: &Term) -> Result { 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())), + 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 qualified".to_string()), } } @@ -80,7 +82,10 @@ fn parse_expr(term: &Term) -> Result, String> { parse_all_expr(Default::default(), term) } -fn parse_all_expr(names: im::HashMap, term: &Term) -> Result, String> { +fn parse_all_expr( + names: im::HashMap, + term: &Term, +) -> Result, String> { match term { Term::Ctr { name, args } => match name.as_str() { "Kind.Quoted.all" => Ok(Expr::all( @@ -93,7 +98,7 @@ fn parse_all_expr(names: im::HashMap, term: &Term) -> Result Ok(Expr::let_( parse_orig(&args[0])?, @@ -102,40 +107,53 @@ fn parse_all_expr(names: im::HashMap, term: &Term) -> Result Ok(Expr::typ(parse_orig(&args[0])?)), - "Kind.Quoted.var" => Ok(Expr::var(Ident::new(parse_name(&args[1])?, parse_orig(&args[0])?))), + "Kind.Quoted.var" => Ok(Expr::var(Ident::new( + parse_name(&args[1])?, + parse_orig(&args[0])?, + ))), "Kind.Quoted.hol" => Ok(Expr::hole(parse_orig(&args[0])?, parse_num(&args[1])?)), - "Kind.Quoted.ann" => Ok(Expr::ann(parse_orig(&args[0])?, parse_all_expr(names.clone(), &args[1])?, parse_all_expr(names, &args[2])?)), + "Kind.Quoted.ann" => Ok(Expr::ann( + parse_orig(&args[0])?, + parse_all_expr(names.clone(), &args[1])?, + parse_all_expr(names, &args[2])?, + )), "Kind.Quoted.sub" => Ok(Expr::sub( parse_orig(&args[0])?, Ident::generate(&parse_name(&args[1])?), parse_num(&args[2])? as usize, - Ident::new(parse_name(&args[1])?, parse_orig(&args[0])?), + parse_num(&args[3])? as usize, parse_all_expr(names, &args[4])?, )), "Kind.Quoted.app" => Ok(Expr::app( parse_orig(&args[0])?, parse_all_expr(names.clone(), &args[1])?, - vec![ - desugared::AppBinding { - data: parse_all_expr(names, &args[2])?, - erased: false, - } - ], + vec![desugared::AppBinding { + data: parse_all_expr(names, &args[2])?, + erased: false, + }], + )), + "Kind.Quoted.ctr" => Ok(Expr::ctr( + parse_orig(&args[1])?, + parse_qualified(&args[0])?, + { + let mut res = Vec::new(); + for arg in parse_list(&args[2])? { + res.push(parse_all_expr(names.clone(), &arg)?); + } + res + }, + )), + "Kind.Quoted.fun" => Ok(Expr::fun( + parse_orig(&args[1])?, + parse_qualified(&args[0])?, + { + let mut res = Vec::new(); + for arg in parse_list(&args[2])? { + res.push(parse_all_expr(names.clone(), &arg)?); + } + res + }, )), - "Kind.Quoted.ctr" => Ok(Expr::ctr(parse_orig(&args[1])?, parse_qualified(&args[0])?, { - let mut res = Vec::new(); - for arg in parse_list(&args[2])? { - res.push(parse_all_expr(names.clone(), &arg)?); - } - res - })), - "Kind.Quoted.fun" => Ok(Expr::fun(parse_orig(&args[1])?, parse_qualified(&args[0])?, { - let mut res = Vec::new(); - for arg in parse_list(&args[2])? { - res.push(parse_all_expr(names.clone(), &arg)?); - } - res - })), "Kind.Quoted.hlp" => Ok(Expr::hlp(parse_orig(&args[0])?, Ident::generate("?"))), "Kind.Quoted.u60" => Ok(Expr::u60(parse_orig(&args[0])?)), "Kind.Quoted.num" => Ok(Expr::num60(parse_orig(&args[0])?, parse_num(&args[1])?)), // TODO: do something about u120? @@ -145,7 +163,10 @@ fn parse_all_expr(names: im::HashMap, term: &Term) -> Result Err(format!("Unexpected tag on transforming quoted term {:?}", tag)), + tag => Err(format!( + "Unexpected tag on transforming quoted term {:?}", + tag + )), }, _ => Err("Unexpected term on transforming quoted term".to_string()), } @@ -209,8 +230,14 @@ fn parse_type_error(expr: &Term) -> Result { parse_all_expr(im::HashMap::new(), &args[2])?, parse_all_expr(im::HashMap::new(), &args[3])?, )), - "Kind.Error.Quoted.inspection" => Ok(TypeError::Inspection(ctx, orig, parse_all_expr(im::HashMap::new(), &args[2])?)), - "Kind.Error.Quoted.too_many_arguments" => Ok(TypeError::TooManyArguments(ctx, orig)), + "Kind.Error.Quoted.inspection" => Ok(TypeError::Inspection( + ctx, + orig, + parse_all_expr(im::HashMap::new(), &args[2])?, + )), + "Kind.Error.Quoted.too_many_arguments" => { + Ok(TypeError::TooManyArguments(ctx, orig)) + } "Kind.Error.Quoted.type_mismatch" => Ok(TypeError::TypeMismatch( ctx, orig, diff --git a/src/kind-cli/src/lib.rs b/src/kind-cli/src/lib.rs index 410de237..196c8da4 100644 --- a/src/kind-cli/src/lib.rs +++ b/src/kind-cli/src/lib.rs @@ -51,7 +51,7 @@ pub enum Command { Eval { file: String }, #[clap(aliases = &["k"])] - ToKindCore { file : String }, + ToKindCore { file: String }, /// Runs Main on the HVM #[clap(aliases = &["r"])] @@ -154,7 +154,6 @@ pub fn compile_in_session( } pub fn run_cli(config: Cli) { - kind_report::check_if_colors_are_supported(config.no_color); let render_config = kind_report::check_if_utf8_is_supported(config.ascii, 2); diff --git a/src/kind-cli/src/main.rs b/src/kind-cli/src/main.rs index e2be27e2..0ca31a19 100644 --- a/src/kind-cli/src/main.rs +++ b/src/kind-cli/src/main.rs @@ -3,4 +3,4 @@ use kind_cli::{run_cli, Cli}; pub fn main() { run_cli(Cli::parse()) -} \ No newline at end of file +} diff --git a/src/kind-cli/tests/mod.rs b/src/kind-cli/tests/mod.rs index 34bde0b3..dc361847 100644 --- a/src/kind-cli/tests/mod.rs +++ b/src/kind-cli/tests/mod.rs @@ -1,12 +1,18 @@ -use kind_cli::{run_cli, Cli}; +use kind_driver::session::Session; +use kind_report::data::{Diagnostic, DiagnosticFrame}; +use kind_report::report::Report; +use kind_report::RenderConfig; -use ntest::timeout; -use pretty_assertions::assert_eq; use std::fs::{self, File}; use std::io::Write; use std::path::{Path, PathBuf}; + +use ntest::timeout; +use pretty_assertions::assert_eq; use walkdir::{Error, WalkDir}; +use kind_driver as driver; + fn golden_test(path: &Path, run: fn(&Path) -> String) { let result = run(path); @@ -30,24 +36,34 @@ fn test_kind2(path: &Path, run: fn(&Path) -> String) -> Result<(), Error> { Ok(()) } - #[test] #[timeout(15000)] fn test_checker() -> Result<(), Error> { test_kind2(Path::new("./tests/suite/checker"), |path| { - let config = Cli { - ascii: true, - no_color: true, - config: None, - command: kind_cli::Command::Check { file: path.to_str().unwrap().to_string() }, - debug: false, - warning: true, - }; - - // let (rx, tx) = std::sync::mpsc::channel(); + let (rx, tx) = std::sync::mpsc::channel(); let root = PathBuf::from("."); - run_cli(config); - todo!() + let mut session = Session::new(root, rx); + + let check = driver::type_check_book(&mut session, &PathBuf::from(path)); + + let diagnostics = tx.try_iter().collect::>(); + let render = RenderConfig::ascii(2); + + kind_report::check_if_colors_are_supported(true); + + match check { + Some(_) if diagnostics.is_empty() => "Ok!".to_string(), + _ => { + let mut res_string = String::new(); + + for diagnostic in diagnostics { + let diag = Into::::into(&diagnostic); + diag.render(&mut session, &render, &mut res_string).unwrap(); + } + + res_string + } + } })?; Ok(()) } diff --git a/src/kind-cli/tests/suite/checker/derive/Eq.golden b/src/kind-cli/tests/suite/checker/derive/Eq.golden new file mode 100644 index 00000000..8a9b5320 --- /dev/null +++ b/src/kind-cli/tests/suite/checker/derive/Eq.golden @@ -0,0 +1,25 @@ + ERROR Type mismatch + + * Expected : ((motive _x3) (Equal.refl. t_ a_)) + * Got : ((motive _x2) (Equal.refl. _x1 _x2)) + + * Context: + * _x1 : Type + * _x2 : _x1 + * _x3 : _x1 + * t_ : Type + * t_ = _x1 + * a_ : t_ + * a_ = _x3 + * a_ = _x2 + * motive : ((b : _x1) -> (Equal. _x1 _x2 b) -> Type) + * refl : ((motive _x2) (Equal.refl. _x1 _x2)) + + /--[tests/suite/checker/Eq.kind2:2:5] + | + 1 | type Equal (a: t) ~ (b: t) { + 2 | refl : Equal t a a + | v--- + | \ Here! + 3 | } + diff --git a/src/kind-cli/tests/suite/checker/derive/Eq.kind2 b/src/kind-cli/tests/suite/checker/derive/Eq.kind2 new file mode 100644 index 00000000..13a854d7 --- /dev/null +++ b/src/kind-cli/tests/suite/checker/derive/Eq.kind2 @@ -0,0 +1,6 @@ +Equal.match (scrutinizer: (Equal t a b)) -(motive: ((b : t) -> (Equal t a b) -> Type)) (_refl: (motive a (Equal.refl t a))) : (motive b scrutinizer) +Equal.match _x1 _x2 _x3 (Equal.refl t_ a_) motive refl = (refl :: ((motive a_) (Equal.refl t_ a_))) + +Equal (a: t) (b: t) : Type + +Equal.refl : (Equal t a a) \ No newline at end of file diff --git a/src/kind-cli/tests/suite/checker/derive/Nat.golden b/src/kind-cli/tests/suite/checker/derive/Nat.golden new file mode 100644 index 00000000..db814b93 --- /dev/null +++ b/src/kind-cli/tests/suite/checker/derive/Nat.golden @@ -0,0 +1 @@ +Ok! \ No newline at end of file diff --git a/src/kind-cli/tests/suite/checker/derive/Nat.kind2 b/src/kind-cli/tests/suite/checker/derive/Nat.kind2 new file mode 100644 index 00000000..6879f2ed --- /dev/null +++ b/src/kind-cli/tests/suite/checker/derive/Nat.kind2 @@ -0,0 +1,8 @@ +type Nat { + succ (pred: Nat) + zero +} + +Nat.pred (n: Nat) : Nat +Nat.pred Nat.zero = Nat.zero +Nat.pred (Nat.succ n) = n \ No newline at end of file diff --git a/src/kind-cli/tests/suite/checker/derive/Vec.golden b/src/kind-cli/tests/suite/checker/derive/Vec.golden new file mode 100644 index 00000000..db814b93 --- /dev/null +++ b/src/kind-cli/tests/suite/checker/derive/Vec.golden @@ -0,0 +1 @@ +Ok! \ No newline at end of file diff --git a/src/kind-cli/tests/suite/checker/derive/Vec.kind2 b/src/kind-cli/tests/suite/checker/derive/Vec.kind2 new file mode 100644 index 00000000..4066d213 --- /dev/null +++ b/src/kind-cli/tests/suite/checker/derive/Vec.kind2 @@ -0,0 +1,10 @@ +type Nat { + succ (pred: Nat) + zero +} + +type Vec (t: Type) ~ (n: Nat) { + cons (x: t) (xs: Vec t size) : Vec t (Nat.succ size) + nil : Vec t Nat.zero +} + diff --git a/src/kind-derive/src/matching.rs b/src/kind-derive/src/matching.rs index 14730787..0ab9b695 100644 --- a/src/kind-derive/src/matching.rs +++ b/src/kind-derive/src/matching.rs @@ -11,7 +11,12 @@ use kind_tree::symbol::{Ident, QualifiedIdent}; /// Derives an eliminator from a sum type declaration. pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry { - let mk_var = |name: Ident| -> Box { Box::new(Expr { data: ExprKind::Var(name), range }) }; + let mk_var = |name: Ident| -> Box { + Box::new(Expr { + data: ExprKind::Var(name), + range, + }) + }; let mk_cons = |name: QualifiedIdent, spine: Vec| -> Box { Box::new(Expr { @@ -56,11 +61,20 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry { // The type let all_args = sum.parameters.extend(&sum.indices); - let res_motive_ty = mk_cons(sum.name.clone(), all_args.iter().cloned().map(|x| Binding::Positional(mk_var(x.name))).collect()); + let res_motive_ty = mk_cons( + sum.name.clone(), + all_args + .iter() + .cloned() + .map(|x| Binding::Positional(mk_var(x.name))) + .collect(), + ); - let parameter_names: Vec = sum.parameters.iter().map(|x| AppBinding::explicit(mk_var(x.name.clone()))).collect(); - - let indice_names: Vec = sum.indices.iter().map(|x| AppBinding::explicit(mk_var(x.name.clone()))).collect(); + let indice_names: Vec = sum + .indices + .iter() + .map(|x| AppBinding::explicit(mk_var(x.name.clone()))) + .collect(); // Sccrutinzies @@ -76,13 +90,16 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry { let motive_ident = Ident::new_static("motive", range); - let motive_type = sum - .parameters - .extend(&sum.indices) - .iter() - .rfold(mk_pi(Ident::new_static("_val", range), res_motive_ty, mk_typ()), |out, arg| { - mk_pi(arg.name.clone(), arg.typ.clone().unwrap_or_else(mk_typ), out) - }); + let motive_type = sum.indices.iter().rfold( + mk_pi(Ident::new_static("_val", range), res_motive_ty, mk_typ()), + |out, arg| { + mk_pi( + arg.name.clone(), + arg.typ.clone().unwrap_or_else(mk_typ), + out, + ) + }, + ); types.push(Argument { hidden: false, @@ -92,27 +109,44 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry { range, }); - let params = sum.parameters.map(|x| Binding::Positional(mk_var(x.name.clone()))); - let indices = sum.indices.map(|x| Binding::Positional(mk_var(x.name.clone()))); + let params = sum + .parameters + .map(|x| Binding::Positional(mk_var(x.name.clone()))); + let indices = sum + .indices + .map(|x| Binding::Positional(mk_var(x.name.clone()))); // Constructors type for cons in &sum.constructors { - let vars: Vec = cons.args.iter().map(|x| Binding::Positional(mk_var(x.name.clone()))).collect(); + let vars: Vec = cons + .args + .iter() + .map(|x| Binding::Positional(mk_var(x.name.clone()))) + .collect(); let cons_inst = mk_cons( sum.name.add_segment(cons.name.to_str()), - [params.as_slice(), if cons.typ.is_none() { indices.as_slice() } else { &[] }, vars.as_slice()].concat(), + [ + params.as_slice(), + if cons.typ.is_none() { + indices.as_slice() + } else { + &[] + }, + vars.as_slice(), + ] + .concat(), ); let mut indices_of_cons = match cons.typ.clone().map(|x| x.data) { - Some(ExprKind::Constr(_, spine)) => spine + Some(ExprKind::Constr(_, spine)) => spine[sum.parameters.len()..] .iter() .map(|x| match x { Binding::Positional(expr) => AppBinding::explicit(expr.clone()), Binding::Named(_, _, _) => todo!("Incomplete feature: Need to reorder"), }) .collect(), - _ => [parameter_names.as_slice(), indice_names.as_slice()].concat(), + _ => [indice_names.as_slice()].concat(), }; indices_of_cons.push(AppBinding::explicit(cons_inst)); @@ -125,9 +159,13 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry { sum.indices.extend(&cons.args) }; - let cons_type = args - .iter() - .rfold(cons_tipo, |out, arg| mk_pi(arg.name.clone(), arg.typ.clone().unwrap_or_else(mk_typ), out)); + let cons_type = args.iter().rfold(cons_tipo, |out, arg| { + mk_pi( + arg.name.clone(), + arg.typ.clone().unwrap_or_else(mk_typ), + out, + ) + }); types.push(Argument { hidden: false, @@ -138,7 +176,7 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry { }); } - let mut res: Vec = [parameter_names.as_slice(), indice_names.as_slice()].concat(); + let mut res: Vec = [indice_names.as_slice()].concat(); res.push(AppBinding::explicit(mk_var(Ident::generate("scrutinizer")))); let ret_ty = mk_app(mk_var(motive_ident), res, range); @@ -160,11 +198,22 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry { .extend(&cons.args) .map(|x| x.name.with_name(|f| format!("{}_", f))) .to_vec(); - spine = sum.indices.extend(&cons.args).map(|x| x.name.with_name(|f| format!("{}_", f))).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.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(); + 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(); } pats.push(Box::new(Pat { diff --git a/src/kind-derive/src/open.rs b/src/kind-derive/src/open.rs index 581f5fbd..1ff8b28e 100644 --- a/src/kind-derive/src/open.rs +++ b/src/kind-derive/src/open.rs @@ -127,7 +127,10 @@ pub fn derive_open(range: Range, rec: &RecordDecl) -> concrete::Entry { mk_var(Ident::generate("fun_")), spine .iter() - .map(|arg| AppBinding { data: mk_var(arg.clone()), erased: false }) + .map(|arg| AppBinding { + data: mk_var(arg.clone()), + erased: false, + }) .collect(), ); diff --git a/src/kind-driver/src/errors.rs b/src/kind-driver/src/errors.rs index 81b35afb..27968fd2 100644 --- a/src/kind-driver/src/errors.rs +++ b/src/kind-driver/src/errors.rs @@ -23,33 +23,34 @@ impl From for DiagnosticFrame { severity: Severity::Error, title: format!("Cannot find the definition '{}'.", idents[0].to_str()), subtitles: vec![], - hints: vec![ - if !suggestions.is_empty() { - format!("Maybe you're looking for {}", suggestions.iter().map(|x| format!("'{}'", x)).collect::>().join(", ")) - } else { - "Take a look at the rules for name searching at https://kind.kindelia.org/hints/name-search".to_string() - } - ], - positions: - idents.iter().map(|ident| { - Marker { - position: ident.range, - color: Color::Fst, - text: "Here!".to_string(), - no_code: false, - main: true, - } - }).collect(), + hints: vec![if !suggestions.is_empty() { + format!( + "Maybe you're looking for {}", + suggestions.iter().map(|x| format!("'{}'", x)).collect::>().join(", ") + ) + } else { + "Take a look at the rules for name searching at https://kind.kindelia.org/hints/name-search".to_string() + }], + positions: idents + .iter() + .map(|ident| Marker { + position: ident.range, + color: Color::Fst, + text: "Here!".to_string(), + no_code: false, + main: true, + }) + .collect(), }, DriverError::MultiplePaths(ident, paths) => DiagnosticFrame { code: 101, severity: Severity::Error, title: "Multiple definitions for the same name".to_string(), - subtitles: paths.iter().map(|path| - Subtitle::Phrase(Color::Fst, vec![Word::White(path.display().to_string())])).collect(), - hints: vec![ - "Take a look at the rules for name searching at https://kind.kindelia.org/hints/name-search".to_string(), - ], + subtitles: paths + .iter() + .map(|path| Subtitle::Phrase(Color::Fst, vec![Word::White(path.display().to_string())])) + .collect(), + hints: vec!["Take a look at the rules for name searching at https://kind.kindelia.org/hints/name-search".to_string()], positions: vec![Marker { position: ident.range, color: Color::Fst, @@ -63,22 +64,23 @@ impl From for DiagnosticFrame { severity: Severity::Error, title: "Defined multiple times for the same name".to_string(), subtitles: vec![], - hints: vec![ - "Rename one of the definitions or remove and look at how names work in Kind at https://kind.kindelia.org/hints/names".to_string() + hints: vec!["Rename one of the definitions or remove and look at how names work in Kind at https://kind.kindelia.org/hints/names".to_string()], + positions: vec![ + Marker { + position: fst.range, + color: Color::Fst, + text: "The first ocorrence".to_string(), + no_code: false, + main: true, + }, + Marker { + position: snd.range, + color: Color::Snd, + text: "Second occorrence here!".to_string(), + no_code: false, + main: false, + }, ], - positions: vec![Marker { - position: fst.range, - color: Color::Fst, - text: "The first ocorrence".to_string(), - no_code: false, - main: true, - },Marker { - position: snd.range, - color: Color::Snd, - text: "Second occorrence here!".to_string(), - no_code: false, - main: false, - }], }, DriverError::CannotFindFile(file) => DiagnosticFrame { code: 103, @@ -86,8 +88,8 @@ impl From for DiagnosticFrame { title: format!("Cannot find file '{}'", file), subtitles: vec![], hints: vec![], - positions: vec![] - } + positions: vec![], + }, } } } diff --git a/src/kind-driver/src/lib.rs b/src/kind-driver/src/lib.rs index 5cbb3b50..6e485fab 100644 --- a/src/kind-driver/src/lib.rs +++ b/src/kind-driver/src/lib.rs @@ -46,7 +46,7 @@ pub fn to_book(session: &mut Session, path: &PathBuf) -> Option let failed = resolution::check_unbound_top_level(session, &mut concrete_book); if failed { - return None + return None; } Some(concrete_book) diff --git a/src/kind-driver/src/resolution.rs b/src/kind-driver/src/resolution.rs index d73067e3..52cfea1c 100644 --- a/src/kind-driver/src/resolution.rs +++ b/src/kind-driver/src/resolution.rs @@ -6,6 +6,7 @@ use kind_pass::expand::uses::expand_uses; use std::collections::HashSet; use std::fs; +use std::os::linux::raw; use std::path::{Path, PathBuf}; use std::rc::Rc; use strsim::jaro; @@ -23,20 +24,23 @@ const EXT: &str = "kind2"; /// Tries to accumulate on a buffer all of the /// paths that exists (so we can just throw an /// error about ambiguous resolution to the user) -fn accumulate_neighbour_paths(raw_path: &Path, other: &mut Vec) { +fn accumulate_neighbour_paths(ident: &QualifiedIdent, raw_path: &Path) -> Result, DiagnosticFrame> { let mut canon_path = raw_path.to_path_buf(); + let mut dir_file_path = raw_path.to_path_buf(); + let dir_path = raw_path.to_path_buf(); + canon_path.set_extension(EXT); + dir_file_path.push("_"); + dir_file_path.set_extension(EXT); - if canon_path.is_file() { - other.push(canon_path); - } - - let mut deferred_path = raw_path.to_path_buf(); - deferred_path.push("_"); - deferred_path.set_extension(EXT); - - if deferred_path.is_file() { - other.push(deferred_path); + if canon_path.exists() && dir_path.exists() && canon_path.is_file() && dir_path.is_dir() { + Err(DriverError::MultiplePaths(ident.clone(), vec![canon_path, dir_path]).into()) + } else if canon_path.is_file() { + Ok(Some(canon_path)) + } else if dir_file_path.is_file() { + Ok(Some(dir_file_path)) + } else { + Ok(None) } } @@ -54,25 +58,21 @@ fn ident_to_path( let mut raw_path = root.to_path_buf(); raw_path.push(PathBuf::from(segments.join("/"))); - let mut paths = Vec::new(); - accumulate_neighbour_paths(&raw_path, &mut paths); - - // TODO: Check if impacts too much while trying to search - if search_on_parent { - raw_path.pop(); - accumulate_neighbour_paths(&raw_path, &mut paths); - } - - if paths.is_empty() { - Ok(None) - } else if paths.len() == 1 { - Ok(Some(paths[0].clone())) - } else { - Err(DriverError::MultiplePaths(ident.clone(), paths).into()) + match accumulate_neighbour_paths(&ident, &raw_path) { + Ok(None) if search_on_parent => { + raw_path.pop(); + accumulate_neighbour_paths(&ident, &raw_path) + } + rest => rest } } -fn try_to_insert_new_name<'a>(failed: &mut bool, session: &'a Session, ident: QualifiedIdent, book: &'a mut Book) -> bool { +fn try_to_insert_new_name<'a>( + failed: &mut bool, + session: &'a Session, + ident: QualifiedIdent, + book: &'a mut Book, +) -> bool { if let Some(first_occorence) = book.names.get(ident.to_string().as_str()) { session .diagnostic_sender @@ -99,7 +99,8 @@ fn module_to_book<'a>( TopLevel::SumType(sum) => { public_names.insert(sum.name.to_string()); if try_to_insert_new_name(failed, session, sum.name.clone(), book) { - book.count.insert(sum.name.to_string(), sum.extract_book_info()); + book.count + .insert(sum.name.to_string(), sum.extract_book_info()); book.entries.insert(sum.name.to_string(), entry.clone()); } @@ -108,7 +109,8 @@ fn module_to_book<'a>( cons_ident.range = cons.name.range.clone(); if try_to_insert_new_name(failed, session, cons_ident.clone(), book) { public_names.insert(cons_ident.to_string()); - book.count.insert(cons_ident.to_string(), cons.extract_book_info(sum)); + book.count + .insert(cons_ident.to_string(), cons.extract_book_info(sum)); } } } @@ -165,16 +167,18 @@ fn parse_and_store_book_by_path<'a>( path: &PathBuf, book: &'a mut Book, ) -> bool { - if !path.exists() { session - .diagnostic_sender - .send(DriverError::CannotFindFile(path.to_str().unwrap().to_string()).into()) - .unwrap(); + .diagnostic_sender + .send(DriverError::CannotFindFile(path.to_str().unwrap().to_string()).into()) + .unwrap(); return true; } - if session.loaded_paths_map.contains_key(&fs::canonicalize(path).unwrap()) { + if session + .loaded_paths_map + .contains_key(&fs::canonicalize(path).unwrap()) + { return false; } @@ -236,10 +240,11 @@ pub fn parse_and_store_book(session: &mut Session, path: &PathBuf) -> Option bool { +pub fn check_unbound_top_level(session: &mut Session, book: &mut Book) -> bool { let mut failed = false; - let (_, unbound_tops) = unbound::get_book_unbound(session.diagnostic_sender.clone(), book, true); + let (_, unbound_tops) = + unbound::get_book_unbound(session.diagnostic_sender.clone(), book, true); for (_, unbound) in unbound_tops { let res: Vec = unbound.iter().map(|x| x.to_ident()).collect(); @@ -250,4 +255,4 @@ pub fn check_unbound_top_level(session: &mut Session, book : &mut Book) -> bool } failed -} \ No newline at end of file +} diff --git a/src/kind-optimization/Cargo.toml b/src/kind-optimization/Cargo.toml deleted file mode 100644 index 010cda19..00000000 --- a/src/kind-optimization/Cargo.toml +++ /dev/null @@ -1,8 +0,0 @@ -[package] -name = "kind-optimization" -version = "0.1.0" -edition = "2021" - -# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html - -[dependencies] diff --git a/src/kind-optimization/src/lib.rs b/src/kind-optimization/src/lib.rs deleted file mode 100644 index 7d12d9af..00000000 --- a/src/kind-optimization/src/lib.rs +++ /dev/null @@ -1,14 +0,0 @@ -pub fn add(left: usize, right: usize) -> usize { - left + right -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn it_works() { - let result = add(2, 2); - assert_eq!(result, 4); - } -} diff --git a/src/kind-parser/src/errors.rs b/src/kind-parser/src/errors.rs index 682bdc72..30b8224a 100644 --- a/src/kind-parser/src/errors.rs +++ b/src/kind-parser/src/errors.rs @@ -228,7 +228,7 @@ impl From for DiagnosticFrame { SyntaxError::UnexpectedToken(token, range, _expect) => DiagnosticFrame { code: 13, severity: Severity::Error, - title: format!("Unexpected token {:?}.", token), + title: format!("Unexpected token '{}'.", token), subtitles: vec![], hints: vec![], positions: vec![Marker { diff --git a/src/kind-parser/src/expr.rs b/src/kind-parser/src/expr.rs index 8c2ee5c0..51b76f96 100644 --- a/src/kind-parser/src/expr.rs +++ b/src/kind-parser/src/expr.rs @@ -66,16 +66,22 @@ impl<'a> Parser<'a> { unused = true; } if unused { - self.errs.send(SyntaxError::UnusedDocString(start.mix(last)).into()).unwrap() + self.errs + .send(SyntaxError::UnusedDocString(start.mix(last)).into()) + .unwrap() } } pub fn is_pi_type(&self) -> bool { - self.get().same_variant(&Token::LPar) && self.peek(1).is_lower_id() && self.peek(2).same_variant(&Token::Colon) + self.get().same_variant(&Token::LPar) + && self.peek(1).is_lower_id() + && self.peek(2).same_variant(&Token::Colon) } pub fn is_named_parameter(&self) -> bool { - self.get().same_variant(&Token::LPar) && self.peek(1).is_lower_id() && self.peek(2).same_variant(&Token::Eq) + self.get().same_variant(&Token::LPar) + && self.peek(1).is_lower_id() + && self.peek(2).same_variant(&Token::Eq) } pub fn is_lambda(&self) -> bool { @@ -83,7 +89,9 @@ impl<'a> Parser<'a> { } pub fn is_sigma_type(&self) -> bool { - self.get().same_variant(&Token::LBracket) && self.peek(1).is_lower_id() && self.peek(2).same_variant(&Token::Colon) + self.get().same_variant(&Token::LBracket) + && self.peek(1).is_lower_id() + && self.peek(2).same_variant(&Token::Colon) } pub fn is_substitution(&self) -> bool { @@ -95,7 +103,7 @@ impl<'a> Parser<'a> { self.advance(); // '##' let name = self.parse_id()?; self.eat_variant(Token::Slash)?; - let redx = self.parse_id()?; + let redx = self.parse_num_lit()?; let expr = self.parse_expr(false)?; let range = start.mix(expr.range); Ok(Box::new(Expr { @@ -118,7 +126,8 @@ impl<'a> Parser<'a> { pub fn parse_upper_id(&mut self) -> Result { let range = self.range(); - let (start, end) = eat_single!(self, Token::UpperId(start, end) => (start.clone(), end.clone()))?; + let (start, end) = + eat_single!(self, Token::UpperId(start, end) => (start.clone(), end.clone()))?; let ident = QualifiedIdent::new_static(start.as_str(), end, range); Ok(ident) } @@ -208,7 +217,10 @@ impl<'a> Parser<'a> { "U60" => ExprKind::Lit(Literal::U60), _ => ExprKind::Constr(id.clone(), vec![]), }; - Ok(Box::new(Expr { range: id.range, data })) + Ok(Box::new(Expr { + range: id.range, + data, + })) } fn parse_data(&mut self, multiline: bool) -> Result, SyntaxError> { @@ -267,7 +279,10 @@ impl<'a> Parser<'a> { if self.check_actual(Token::RBracket) { let range = self.advance().1.mix(range); - return Ok(Box::new(Expr { range, data: ExprKind::List(vec) })); + return Ok(Box::new(Expr { + range, + data: ExprKind::List(vec), + })); } vec.push(*self.parse_expr(false)?); @@ -298,7 +313,10 @@ impl<'a> Parser<'a> { let end = self.eat_variant(Token::RBracket)?.1; let range = range.mix(end); - Ok(Box::new(Expr { range, data: ExprKind::List(vec) })) + Ok(Box::new(Expr { + range, + data: ExprKind::List(vec), + })) } fn parse_paren(&mut self) -> Result, SyntaxError> { @@ -346,6 +364,17 @@ impl<'a> Parser<'a> { })) } + pub fn parse_num_lit(&mut self) -> Result { + self.ignore_docs(); + match self.get().clone() { + Token::Num(num) => { + self.advance(); + Ok(num as usize) + } + _ => self.fail(vec![]), + } + } + pub fn parse_atom(&mut self) -> Result, SyntaxError> { self.ignore_docs(); match self.get().clone() { @@ -381,16 +410,16 @@ impl<'a> Parser<'a> { fn parse_app_binding(&mut self) -> Result { self.ignore_docs(); - let (erased, data) = /*if self.get().same_variant(&Token::LBrace) { + let (erased, data) = if self.get().same_variant(&Token::Minus) { + self.advance(); let start = self.range(); - self.advance(); // '{' + self.eat_variant(Token::LPar)?; let atom = self.parse_atom()?; - self.eat_closing_keyword(Token::RBrace, start)?; + self.eat_closing_keyword(Token::RPar, start)?; (true, atom) - } else {*/ + } else { (false, self.parse_atom()?) - // } - ; + }; Ok(AppBinding { data, erased }) } @@ -424,7 +453,11 @@ impl<'a> Parser<'a> { } } - fn parse_call_tail(&mut self, start: Range, multiline: bool) -> Result<(Range, Vec), SyntaxError> { + fn parse_call_tail( + &mut self, + start: Range, + multiline: bool, + ) -> Result<(Range, Vec), SyntaxError> { let mut spine = Vec::new(); let mut end = start; while (!self.is_linebreak() || multiline) && !self.get().same_variant(&Token::Eof) { @@ -478,7 +511,12 @@ impl<'a> Parser<'a> { if self.get().is_upper_id() { let upper = self.parse_upper_id()?; let (range, bindings, ignore_rest) = self.parse_pat_destruct_bindings()?; - Ok(Destruct::Destruct(upper.range.mix(range.unwrap_or(upper.range)), upper, bindings, ignore_rest)) + Ok(Destruct::Destruct( + upper.range.mix(range.unwrap_or(upper.range)), + upper, + bindings, + ignore_rest, + )) } else { let name = self.parse_id()?; Ok(Destruct::Ident(name)) @@ -551,7 +589,9 @@ impl<'a> Parser<'a> { })) } - pub fn parse_pat_destruct_bindings(&mut self) -> Result<(Option, Vec, Option), SyntaxError> { + pub fn parse_pat_destruct_bindings( + &mut self, + ) -> Result<(Option, Vec, Option), SyntaxError> { let mut ignore_rest_range = None; let mut bindings = Vec::new(); let mut range = None; @@ -623,7 +663,12 @@ impl<'a> Parser<'a> { None }; - let match_ = Box::new(Match { typ, scrutinizer, cases, motive }); + let match_ = Box::new(Match { + typ, + scrutinizer, + cases, + motive, + }); Ok(Box::new(Expr { data: ExprKind::Match(match_), diff --git a/src/kind-parser/src/lexer/state.rs b/src/kind-parser/src/lexer/state.rs index 6c9fdaca..edf71591 100644 --- a/src/kind-parser/src/lexer/state.rs +++ b/src/kind-parser/src/lexer/state.rs @@ -18,11 +18,7 @@ pub struct Lexer<'a> { } impl<'a> Lexer<'a> { - pub fn new( - input: &'a str, - peekable: Peekable>, - ctx: SyntaxCtxIndex, - ) -> Lexer<'a> { + pub fn new(input: &'a str, peekable: Peekable>, ctx: SyntaxCtxIndex) -> Lexer<'a> { Lexer { input, pos: 0, diff --git a/src/kind-parser/src/lexer/tokens.rs b/src/kind-parser/src/lexer/tokens.rs index 6334084f..52571094 100644 --- a/src/kind-parser/src/lexer/tokens.rs +++ b/src/kind-parser/src/lexer/tokens.rs @@ -1,6 +1,8 @@ //! Describes all of the tokens required //! to parse kind2 after version 0.2.8. +use core::fmt; + use crate::errors::SyntaxError; #[derive(Debug, Clone)] @@ -107,3 +109,70 @@ impl Token { matches!(self, Token::Eof) } } + +impl fmt::Display for Token { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Token::LPar => write!(f, "("), + Token::RPar => write!(f, ")"), + Token::LBracket => write!(f, "["), + Token::RBracket => write!(f, "]"), + Token::LBrace => write!(f, "{{"), + Token::RBrace => write!(f, "}}"), + Token::Eq => write!(f, "="), + Token::Colon => write!(f, ":"), + Token::Semi => write!(f, ";"), + Token::FatArrow => write!(f, "=>"), + Token::Dollar => write!(f, "$"), + Token::Comma => write!(f, ","), + Token::RightArrow => write!(f, "<-"), + Token::DotDot => write!(f, ".."), + Token::Dot => write!(f, "."), + Token::Tilde => write!(f, "~"), + Token::ColonColon => write!(f, "::"), + Token::Help(text) => write!(f, "?{}", text), + Token::LowerId(id) => write!(f, "{}", id), + Token::UpperId(main, Some(aux)) => write!(f, "{}/{}", main, aux), + Token::UpperId(main, None) => write!(f, "{}", main), + Token::Do => write!(f, "do"), + Token::If => write!(f, "if"), + Token::Else => write!(f, "else"), + Token::Match => write!(f, "match"), + Token::Ask => write!(f, "ask"), + Token::Return => write!(f, "return"), + Token::Let => write!(f, "let"), + Token::Type => write!(f, "type"), + Token::Record => write!(f, "record"), + Token::Constructor => write!(f, "constructor"), + Token::Use => write!(f, "use"), + Token::As => write!(f, "as"), + Token::Char(c) => write!(f, "'{}'", c), + Token::Str(s) => write!(f, "\"{}\"", s), + Token::Num(n) => write!(f, "{}", n), + Token::Float(start, end) => write!(f, "{}.{}", start, end), + Token::Hole => write!(f, "-"), + Token::Plus => write!(f, "+"), + Token::Minus => write!(f, "-"), + Token::Star => write!(f, "*"), + Token::Slash => write!(f, "/"), + Token::Percent => write!(f, "%"), + Token::Ampersand => write!(f, "&"), + Token::Bar => write!(f, "|"), + Token::Hat => write!(f, "^"), + Token::GreaterGreater => write!(f, ">>"), + Token::LessLess => write!(f, "<<"), + Token::Less => write!(f, "<"), + Token::LessEq => write!(f, "<="), + Token::EqEq => write!(f, "=="), + Token::GreaterEq => write!(f, ">="), + Token::Greater => write!(f, ">"), + Token::BangEq => write!(f, "!="), + Token::Bang => write!(f, "!"), + Token::HashHash => write!(f, "##"), + Token::Hash => write!(f, "#"), + Token::Comment(_, _) => write!(f, "Comment"), + Token::Eof => write!(f, "End of file"), + Token::Error(_) => write!(f, "ERROR"), + } + } +} diff --git a/src/kind-pass/src/desugar/app.rs b/src/kind-pass/src/desugar/app.rs index 188b8765..f906a1d0 100644 --- a/src/kind-pass/src/desugar/app.rs +++ b/src/kind-pass/src/desugar/app.rs @@ -177,7 +177,7 @@ impl<'a> DesugarState<'a> { for arg in spine { new_spine.push(desugared::AppBinding { data: self.desugar_expr(&arg.data), - erased: arg.erased + erased: arg.erased, }) } desugared::Expr::app(range, new_head, new_spine) diff --git a/src/kind-pass/src/desugar/destruct.rs b/src/kind-pass/src/desugar/destruct.rs index 816419f0..5dc1d5f4 100644 --- a/src/kind-pass/src/desugar/destruct.rs +++ b/src/kind-pass/src/desugar/destruct.rs @@ -228,7 +228,12 @@ impl<'a> DesugarState<'a> { let motive = if let Some(res) = &match_.motive { self.desugar_expr(res) } else { - let mut idx: Vec = sum.parameters.extend(&sum.indices).iter().map(|x| x.name.clone()).collect(); + let mut idx: Vec = sum + .parameters + .extend(&sum.indices) + .iter() + .map(|x| x.name.clone()) + .collect(); idx.push(Ident::generate("_val")); idx.iter().rfold(self.gen_hole_expr(), |expr, l| { desugared::Expr::lambda(l.range, l.clone(), expr, false) diff --git a/src/kind-pass/src/desugar/expr.rs b/src/kind-pass/src/desugar/expr.rs index 643af9b7..7f567763 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.clone(), + sub.redx, self.desugar_expr(&sub.expr), ) } diff --git a/src/kind-pass/src/desugar/mod.rs b/src/kind-pass/src/desugar/mod.rs index 61a4bb47..8e0a2937 100644 --- a/src/kind-pass/src/desugar/mod.rs +++ b/src/kind-pass/src/desugar/mod.rs @@ -1,5 +1,5 @@ //! This pass transforms a sugared tree into a simpler tree. -//! +//! //! It does a lot of things like: //! * Setting an unique number for each of the holes //! * Desugar of lets and matchs diff --git a/src/kind-pass/src/erasure/mod.rs b/src/kind-pass/src/erasure/mod.rs index 2bbc76e3..d977a984 100644 --- a/src/kind-pass/src/erasure/mod.rs +++ b/src/kind-pass/src/erasure/mod.rs @@ -42,7 +42,11 @@ 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, @@ -61,7 +65,9 @@ pub fn erase_book(book: &Book, errs: Sender, entrypoint: FxHash 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)); } @@ -101,8 +107,15 @@ 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; } @@ -123,7 +136,14 @@ impl<'a> ErasureState<'a> { } } - 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), t) => match (self.holes[hole], t) { (Some(res), _) if !visited.contains(&hole) => { @@ -154,11 +174,22 @@ impl<'a> ErasureState<'a> { } } - 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) } - pub fn erase_pat_spine(&mut self, on: (Option, Relevance), name: &QualifiedIdent, spine: &Vec>) -> Vec> { + pub fn erase_pat_spine( + &mut self, + on: (Option, Relevance), + name: &QualifiedIdent, + spine: &Vec>, + ) -> Vec> { let fun = match self.names.get(&name.to_string()) { Some(res) => *res, None => self.new_hole(name.range, name.to_string()), @@ -171,7 +202,13 @@ 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 arg.erased { (Some(arg.span), Relevance::Irrelevant) } else { on }); + let irrelevances = erased.map(|arg| { + if arg.erased { + (Some(arg.span), Relevance::Irrelevant) + } else { + on + } + }); spine .iter() @@ -247,7 +284,10 @@ impl<'a> ErasureState<'a> { Lambda(name, body, erased) => { let ctx = self.ctx.clone(); if *erased { - self.ctx.insert(name.to_string(), (name.range, (None, Relevance::Irrelevant))); + self.ctx.insert( + name.to_string(), + (name.range, (None, Relevance::Irrelevant)), + ); } else { self.ctx.insert(name.to_string(), (name.range, *on)); } @@ -285,7 +325,7 @@ impl<'a> ErasureState<'a> { let on = if x.erased { (x.data.span.to_range(), Relevance::Irrelevant) } else { - (x.data.span.to_range(), Relevance::Relevant) + on.clone() }; desugared::AppBinding { data: self.erase_expr(&on, &x.data), @@ -300,7 +340,13 @@ impl<'a> ErasureState<'a> { }) } 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, @@ -316,7 +362,10 @@ impl<'a> ErasureState<'a> { .zip(args) .map(|(expr, arg)| { if arg.erased { - (self.erase_expr(&(Some(arg.span), Relevance::Irrelevant), expr), arg) + ( + self.erase_expr(&(Some(arg.span), Relevance::Irrelevant), expr), + arg, + ) } else { (self.erase_expr(on, expr), arg) } @@ -329,7 +378,13 @@ 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, @@ -345,7 +400,10 @@ impl<'a> ErasureState<'a> { .zip(args) .map(|(expr, arg)| { if arg.erased { - (self.erase_expr(&(Some(arg.span), Relevance::Irrelevant), expr), arg) + ( + self.erase_expr(&(Some(arg.span), Relevance::Irrelevant), expr), + arg, + ) } else { (self.erase_expr(on, expr), arg) } @@ -370,13 +428,23 @@ 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() .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(); @@ -401,7 +469,11 @@ 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)).collect::>(); + 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(), diff --git a/src/kind-pass/src/errors.rs b/src/kind-pass/src/errors.rs index 4f5f0ad0..09c32027 100644 --- a/src/kind-pass/src/errors.rs +++ b/src/kind-pass/src/errors.rs @@ -95,30 +95,29 @@ impl From for DiagnosticFrame { title: "All of the rules of a entry should have the same number of patterns.".to_string(), subtitles: vec![], hints: vec!["Check if you're trying to use a function that manipulats erased variables.".to_string()], - positions: arities.iter().map(|(range, size)| { - Marker { + positions: arities + .iter() + .map(|(range, size)| Marker { position: *range, color: Color::Fst, text: format!("This rule contains {} patterns", size), no_code: false, main: true, - } - }).collect(), + }) + .collect(), }, PassError::RuleWithIncorrectArity(place, _got, expected, hidden) => DiagnosticFrame { code: 203, severity: Severity::Error, title: "This rule is with the incorrect arity.".to_string(), subtitles: vec![], - hints: vec![ - if expected == 0 { - "This rule expects no arguments".to_string() - } else if hidden == 0 { - format!("This rule expects {} arguments", expected) - } else { - format!("This rule expects {} arguments or {} (without hidden ones)", expected, expected - hidden) - } - ], + hints: vec![if expected == 0 { + "This rule expects no arguments".to_string() + } else if hidden == 0 { + format!("This rule expects {} arguments", expected) + } else { + format!("This rule expects {} arguments or {} (without hidden ones)", expected, expected - hidden) + }], positions: vec![Marker { position: place, color: Color::Fst, @@ -132,15 +131,13 @@ impl From for DiagnosticFrame { severity: Severity::Error, title: "Required functions are not implemented for this type.".to_string(), subtitles: vec![], - hints: vec![ - match sugar { - Sugar::DoNotation => "You must implement 'bind' and 'pure' for this type in order to use the do notation.".to_string(), - Sugar::List => "You must implement 'List', 'List.cons' and 'List.nil' for this type in order to use the list notation.".to_string(), - Sugar::Sigma => "You must implement 'Sigma' in order to use the sigma notation.".to_string(), - Sugar::Pair => "You must implement 'Sigma' and 'Sigma.new' in order to use the sigma notation.".to_string(), - Sugar::BoolIf => "You must implement 'Bool.if' in order to use the if notation.".to_string(), - } - ], + hints: vec![match sugar { + Sugar::DoNotation => "You must implement 'bind' and 'pure' for this type in order to use the do notation.".to_string(), + Sugar::List => "You must implement 'List', 'List.cons' and 'List.nil' for this type in order to use the list notation.".to_string(), + Sugar::Sigma => "You must implement 'Sigma' in order to use the sigma notation.".to_string(), + Sugar::Pair => "You must implement 'Sigma' and 'Sigma.new' in order to use the sigma notation.".to_string(), + Sugar::BoolIf => "You must implement 'Bool.if' in order to use the if notation.".to_string(), + }], positions: vec![Marker { position: expr_place, color: Color::Fst, @@ -169,19 +166,22 @@ impl From for DiagnosticFrame { title: format!("Cannot find this field in the definition '{}'.", ty), subtitles: vec![], hints: vec![], - positions: vec![Marker { - position: place, - color: Color::Fst, - text: "Here!".to_string(), - no_code: false, - main: true, - },Marker { - position: def_name, - color: Color::Snd, - text: "This is the definition name".to_string(), - no_code: false, - main: false, - }], + positions: vec![ + Marker { + position: place, + color: Color::Fst, + text: "Here!".to_string(), + no_code: false, + main: true, + }, + Marker { + position: def_name, + color: Color::Snd, + text: "This is the definition name".to_string(), + no_code: false, + main: false, + }, + ], }, PassError::CannotFindConstructor(place, def_name, ty) => DiagnosticFrame { code: 208, @@ -189,19 +189,22 @@ impl From for DiagnosticFrame { title: format!("Cannot find this constructor in the type definition '{}'.", ty), subtitles: vec![], hints: vec![], - positions: vec![Marker { - position: place, - color: Color::Fst, - text: "Here!".to_string(), - no_code: false, - main: true, - },Marker { - position: def_name, - color: Color::Snd, - text: "This is the definition name".to_string(), - no_code: false, - main: false, - }], + positions: vec![ + Marker { + position: place, + color: Color::Fst, + text: "Here!".to_string(), + no_code: false, + main: true, + }, + Marker { + position: def_name, + color: Color::Snd, + text: "This is the definition name".to_string(), + no_code: false, + main: false, + }, + ], }, PassError::NoCoverage(place, other) => DiagnosticFrame { code: 209, @@ -231,16 +234,19 @@ impl From for DiagnosticFrame { severity: Severity::Error, title: "Incorrect arity.".to_string(), subtitles: vec![], - hints: vec![ - if expected == 0 { - format!("This function expects no arguments but got {}", got.len()) - } else if hidden == 0 { - format!("This function expects {} arguments but got {}", expected, got.len()) - } else { - format!("This function expects {} arguments or {} (without hidden ones) but got {}.", expected, expected - hidden, got.len()) - } - ], - positions + hints: vec![if expected == 0 { + format!("This function expects no arguments but got {}", got.len()) + } else if hidden == 0 { + format!("This function expects {} arguments but got {}", expected, got.len()) + } else { + format!( + "This function expects {} arguments or {} (without hidden ones) but got {}.", + expected, + expected - hidden, + got.len() + ) + }], + positions, } } PassError::SugarIsBadlyImplemented(head_range, place_range, expected) => DiagnosticFrame { @@ -251,25 +257,26 @@ impl From for DiagnosticFrame { hints: vec![format!( "Take a look at how sugar functions should be implemented at https://kind2.kindelia.com/hints/sugars." )], - positions: vec![Marker { - position: head_range, - color: Color::Fst, - text: - if expected == 0 { + positions: vec![ + Marker { + position: head_range, + color: Color::Fst, + text: if expected == 0 { "This rule expects no arguments".to_string() } else { format!("This rule expects {} explicit arguments", expected) - } - , - no_code: false, - main: true, - },Marker { - position: place_range, - color: Color::Snd, - text: "This is what triggers the sugar".to_string(), - no_code: false, - main: false, - }], + }, + no_code: false, + main: true, + }, + Marker { + position: place_range, + color: Color::Snd, + text: "This is what triggers the sugar".to_string(), + no_code: false, + main: false, + }, + ], }, PassError::DuplicatedNamed(first_decl, last_decl) => DiagnosticFrame { code: 212, @@ -297,8 +304,7 @@ impl From for DiagnosticFrame { PassError::CannotUseNamed(fun_range, binding_range) => DiagnosticFrame { code: 213, severity: Severity::Error, - title: "Cannot use named parameters in this type of function application" - .to_string(), + title: "Cannot use named parameters in this type of function application".to_string(), subtitles: vec![], hints: vec![], positions: vec![ @@ -347,41 +353,35 @@ impl From for DiagnosticFrame { title: "Cannot find alias".to_string(), subtitles: vec![], hints: vec![], - positions: vec![ - Marker { - position: range, - color: Color::Fst, - text: format!("Cannot find alias for '{}'", name), - no_code: false, - main: true, - } - ], + positions: vec![Marker { + position: range, + color: Color::Fst, + text: format!("Cannot find alias for '{}'", name), + no_code: false, + main: true, + }], }, PassError::ShouldBeAParameter(error_range, declaration_range) => { let mut positions = vec![]; match error_range { Span::Generated => (), - Span::Locatable(error_range) => { - positions.push(Marker { - position: error_range, - color: Color::Fst, - text: "This expression is not the parameter".to_string(), - no_code: false, - main: true, - }) - }, + Span::Locatable(error_range) => positions.push(Marker { + position: error_range, + color: Color::Fst, + text: "This expression is not the parameter".to_string(), + no_code: false, + main: true, + }), } - positions.push( - Marker { - position: declaration_range, - color: Color::Snd, - text: "This is the parameter that should be used".to_string(), - no_code: false, - main: false, - } - ); + positions.push(Marker { + position: declaration_range, + color: Color::Snd, + text: "This is the parameter that should be used".to_string(), + no_code: false, + main: false, + }); DiagnosticFrame { code: 214, @@ -389,7 +389,7 @@ impl From for DiagnosticFrame { title: "The expression is not the parameter declared in the type constructor".to_string(), subtitles: vec![], hints: vec![], - positions + positions, } } PassError::NotATypeConstructor(error_range, declaration_range) => DiagnosticFrame { @@ -412,7 +412,7 @@ impl From for DiagnosticFrame { text: "This is the type that should be used instead".to_string(), no_code: false, main: false, - } + }, ], }, PassError::NoFieldCoverage(place, other) => DiagnosticFrame { @@ -420,7 +420,10 @@ impl From for DiagnosticFrame { severity: Severity::Error, title: "The case is not covering all the values inside of it!".to_string(), subtitles: vec![], - hints: vec![format!("Need variables for {}", other.iter().map(|x| format!("'{}'", x)).collect::>().join(", "))], + hints: vec![format!( + "Need variables for {}", + other.iter().map(|x| format!("'{}'", x)).collect::>().join(", ") + )], positions: vec![Marker { position: place, color: Color::Fst, @@ -435,20 +438,22 @@ impl From for DiagnosticFrame { title: "Duplicated constructor name".to_string(), subtitles: vec![], hints: vec![], - positions: vec![Marker { - position: place, - color: Color::Fst, - text: "Here".to_string(), - no_code: false, - main: true, - }, - Marker { - position: other, - color: Color::Fst, - text: "Here".to_string(), - no_code: false, - main: false, - }], + positions: vec![ + Marker { + position: place, + color: Color::Fst, + text: "Here".to_string(), + no_code: false, + main: true, + }, + Marker { + position: other, + color: Color::Fst, + text: "Here".to_string(), + no_code: false, + main: false, + }, + ], }, } } diff --git a/src/kind-pass/src/lib.rs b/src/kind-pass/src/lib.rs index 879616d5..fd903051 100644 --- a/src/kind-pass/src/lib.rs +++ b/src/kind-pass/src/lib.rs @@ -6,6 +6,6 @@ pub mod desugar; pub mod erasure; +mod errors; pub mod expand; pub mod unbound; -mod errors; diff --git a/src/kind-pass/src/unbound/mod.rs b/src/kind-pass/src/unbound/mod.rs index ad9d1fab..1e0f34b7 100644 --- a/src/kind-pass/src/unbound/mod.rs +++ b/src/kind-pass/src/unbound/mod.rs @@ -5,7 +5,6 @@ //! by sugars because it's useful to name resolution //! phase. -use std::collections::HashSet; use std::sync::mpsc::Sender; use fxhash::{FxHashMap, FxHashSet}; @@ -29,9 +28,10 @@ use crate::errors::PassError; pub struct UnboundCollector { pub errors: Sender, pub context_vars: Vec<(Range, String)>, + pub top_level_defs: FxHashMap, pub unbound_top_level: FxHashMap>, pub unbound: FxHashMap>, - pub emit_errs: bool + pub emit_errs: bool, } impl UnboundCollector { @@ -39,9 +39,10 @@ impl UnboundCollector { Self { errors: diagnostic_sender, context_vars: Default::default(), + top_level_defs: Default::default(), unbound_top_level: Default::default(), unbound: Default::default(), - emit_errs + emit_errs, } } } @@ -72,6 +73,33 @@ pub fn get_book_unbound( (state.unbound, state.unbound_top_level) } +impl UnboundCollector { + fn visit_top_level_names(&mut self, toplevel: &mut TopLevel) { + match toplevel { + TopLevel::SumType(sum) => { + self.top_level_defs + .insert(sum.name.to_string(), sum.name.range); + for cons in &sum.constructors { + let name_cons = sum.name.add_segment(cons.name.to_str()); + self.top_level_defs + .insert(name_cons.to_string(), name_cons.range); + } + } + TopLevel::RecordType(rec) => { + self.top_level_defs + .insert(rec.name.to_string(), rec.name.range); + let name_cons = rec.name.add_segment(rec.constructor.to_str()); + self.top_level_defs + .insert(name_cons.to_string(), name_cons.range); + } + TopLevel::Entry(entry) => { + self.top_level_defs + .insert(entry.name.to_string(), entry.name.range); + } + } + } +} + impl Visitor for UnboundCollector { fn visit_attr(&mut self, _: &mut kind_tree::concrete::Attribute) {} @@ -90,11 +118,8 @@ impl Visitor for UnboundCollector { } fn visit_qualified_ident(&mut self, ident: &mut QualifiedIdent) { - if !self.context_vars.iter().any(|x| x.1 == ident.to_string()) { - let entry = self - .unbound_top_level - .entry(ident.to_string()) - .or_default(); + if !self.top_level_defs.contains_key(&ident.to_string()) { + let entry = self.unbound_top_level.entry(ident.to_string()).or_default(); entry.insert(ident.clone()); } } @@ -107,8 +132,8 @@ impl Visitor for UnboundCollector { { if self.emit_errs { self.errors - .send(PassError::RepeatedVariable(fst.0, ident.0.range).into()) - .unwrap() + .send(PassError::RepeatedVariable(fst.0, ident.0.range).into()) + .unwrap() } } else { self.context_vars.push((ident.0.range, ident.0.to_string())) @@ -129,8 +154,8 @@ impl Visitor for UnboundCollector { if let Some(fst) = res { if self.emit_errs { self.errors - .send(PassError::RepeatedVariable(fst.0, argument.name.range).into()) - .unwrap() + .send(PassError::RepeatedVariable(fst.0, argument.name.range).into()) + .unwrap() } } else { self.context_vars @@ -151,9 +176,6 @@ impl Visitor for UnboundCollector { } fn visit_entry(&mut self, entry: &mut Entry) { - self.context_vars - .push((entry.name.range, entry.name.to_string())); - let vars = self.context_vars.clone(); for arg in entry.args.iter_mut() { @@ -172,25 +194,21 @@ impl Visitor for UnboundCollector { fn visit_top_level(&mut self, toplevel: &mut TopLevel) { match toplevel { TopLevel::SumType(entr) => { - self.context_vars - .push((entr.name.range, entr.name.to_string())); - let mut repeated_names = FxHashMap::::default(); let mut failed = false; for cons in &entr.constructors { - match repeated_names.get(&cons.name.to_string()) { Some(_) => { failed = true; - }, + } None => { repeated_names.insert(cons.name.to_string(), cons.name.range); - }, + } } - let name_cons = entr.name.add_segment(cons.name.to_str()); - self.context_vars.push((name_cons.range, name_cons.to_string())); + self.context_vars + .push((name_cons.range, name_cons.to_string())); } if failed { @@ -214,16 +232,7 @@ impl Visitor for UnboundCollector { self.context_vars = vars; } TopLevel::RecordType(entr) => { - self.context_vars - .push((entr.name.range, entr.name.to_string())); - - let name_cons = entr.name.add_segment(entr.constructor.to_str()); - - self.context_vars - .push((name_cons.range, name_cons.to_string())); - let inside_vars = self.context_vars.clone(); - visit_vec!(entr.parameters.iter_mut(), arg => self.visit_argument(arg)); visit_vec!(entr.fields.iter_mut(), (_, _, typ) => { self.visit_expr(typ); @@ -236,17 +245,18 @@ impl Visitor for UnboundCollector { } fn visit_module(&mut self, book: &mut kind_tree::concrete::Module) { + for entr in &mut book.entries { + self.visit_top_level_names(entr); + } for entr in &mut book.entries { self.visit_top_level(entr) } } fn visit_book(&mut self, book: &mut Book) { - self.context_vars = book - .names - .values() - .map(|name| (name.range, name.to_string())) - .collect(); + for entr in book.entries.values_mut() { + self.visit_top_level_names(entr); + } for entr in book.entries.values_mut() { self.visit_top_level(entr) } @@ -370,7 +380,7 @@ impl Visitor for UnboundCollector { self.visit_expr(body); self.context_vars.pop(); } - ExprKind::Lambda(ident, binder, body, erased) => { + ExprKind::Lambda(ident, binder, body, _erased) => { match binder { Some(x) => self.visit_expr(x), None => (), @@ -421,7 +431,6 @@ 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-report/src/report.rs b/src/kind-report/src/report.rs index 844c5224..0a195120 100644 --- a/src/kind-report/src/report.rs +++ b/src/kind-report/src/report.rs @@ -458,7 +458,9 @@ impl<'a> Report for Diagnostic<'a> { for (ctx, group) in groups { writeln!(fmt)?; let (file, code) = cache.fetch(ctx).unwrap(); - let diff = pathdiff::diff_paths(&file.clone(), PathBuf::from(".").canonicalize().unwrap()).unwrap(); + let diff = + pathdiff::diff_paths(&file.clone(), PathBuf::from(".").canonicalize().unwrap()) + .unwrap(); write_code_block(&diff, config, &group, code, fmt)?; } diff --git a/src/kind-target-hvm/src/lib.rs b/src/kind-target-hvm/src/lib.rs index 98ec348b..b16ff8a0 100644 --- a/src/kind-target-hvm/src/lib.rs +++ b/src/kind-target-hvm/src/lib.rs @@ -38,8 +38,12 @@ pub fn compile_term(expr: &desugared::Expr) -> Box { }), Hole(_) => unreachable!("Internal Error: 'Hole' cannot be a relevant term"), Typ => unreachable!("Internal Error: 'Typ' cannot be a relevant term"), - NumType(desugared::NumType::U60) => unreachable!("Internal Error: 'U60' cannot be a relevant term"), - NumType(desugared::NumType::U120) => unreachable!("Internal Error: 'U120' cannot be a relevant term"), + NumType(desugared::NumType::U60) => { + unreachable!("Internal Error: 'U60' cannot be a relevant term") + } + NumType(desugared::NumType::U120) => { + unreachable!("Internal Error: 'U120' cannot be a relevant term") + } All(_, _, _) => unreachable!("Internal Error: 'All' cannot be a relevant term"), Str(_) => unreachable!("Internal Error: 'Str' cannot be a relevant term"), Hlp(_) => unreachable!("Internal Error: 'Hlp' cannot be a relevant term"), diff --git a/src/kind-tree/src/concrete/expr.rs b/src/kind-tree/src/concrete/expr.rs index 54daa5ce..edba65af 100644 --- a/src/kind-tree/src/concrete/expr.rs +++ b/src/kind-tree/src/concrete/expr.rs @@ -27,7 +27,7 @@ pub type Spine = Vec; #[derive(Clone, Debug, Hash, PartialEq, Eq)] pub struct AppBinding { pub data: Box, - pub erased: bool + pub erased: bool, } impl AppBinding { @@ -74,7 +74,7 @@ pub struct Match { #[derive(Clone, Debug, Hash, PartialEq, Eq)] pub struct Substitution { pub name: Ident, - pub redx: Ident, + pub redx: usize, pub indx: usize, pub expr: Box, } @@ -380,7 +380,7 @@ impl Display for Binding { impl Display for AppBinding { fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> { if self.erased { - write!(f, "{{{}}}", self.data) + write!(f, "-({})", self.data) } else { write!(f, "{}", self.data) } @@ -403,9 +403,13 @@ impl Display for Expr { spine.iter().map(|x| format!(" {}", x)).collect::() ), Lambda(binder, None, body, false) => write!(f, "({} => {})", binder, body), - Lambda(binder, Some(typ), body, false) => write!(f, "(({} : {}) => {})", binder, typ, body), + Lambda(binder, Some(typ), body, false) => { + write!(f, "(({} : {}) => {})", binder, typ, body) + } Lambda(binder, None, body, true) => write!(f, "({{{}}} => {})", binder, body), - Lambda(binder, Some(typ), body, true) => write!(f, "({{{} : {}}} => {})", binder, typ, body), + Lambda(binder, Some(typ), body, true) => { + write!(f, "({{{} : {}}} => {})", binder, typ, body) + } Pair(fst, snd) => write!(f, "($ {} {})", fst, snd), App(head, spine) => write!( f, @@ -423,7 +427,7 @@ impl Display for Expr { .collect::>() .join(" ") ), - Ann(expr, typ) => write!(f, "({} : {})", expr, typ), + Ann(expr, typ) => write!(f, "({} :: {})", expr, typ), Binary(op, expr, typ) => write!(f, "({} {} {})", op, expr, typ), Match(matcher) => write!(f, "({})", matcher), Subst(subst) => write!(f, "({})", subst), diff --git a/src/kind-tree/src/desugared/mod.rs b/src/kind-tree/src/desugared/mod.rs index d3dc5b54..680cc9f8 100644 --- a/src/kind-tree/src/desugared/mod.rs +++ b/src/kind-tree/src/desugared/mod.rs @@ -20,7 +20,7 @@ pub type Spine = Vec>; #[derive(Clone, Debug, Hash, PartialEq, Eq)] pub struct AppBinding { pub data: Box, - pub erased: bool + pub erased: bool, } #[derive(Clone, Debug, Hash, PartialEq, Eq)] @@ -42,7 +42,7 @@ pub enum ExprKind { /// Type ascription (x : y) Ann(Box, Box), /// Substitution - Sub(Ident, usize, Ident, Box), + Sub(Ident, usize, usize, Box), /// Type Literal Typ, /// Primitive numeric types @@ -91,7 +91,7 @@ impl Expr { }) } - pub fn sub(range: Range, ident: Ident, idx: usize, rdx: Ident, body: Box) -> Box { + pub fn sub(range: Range, ident: Ident, idx: usize, rdx: usize, body: Box) -> Box { Box::new(Expr { span: Span::Locatable(range), data: ExprKind::Sub(ident, idx, rdx, body), @@ -117,7 +117,9 @@ impl Expr { .iter() .rev() .zip(irrelev) - .fold(body, |body, (ident, irrelev)| Expr::lambda(ident.range, ident.clone(), body, *irrelev)) + .fold(body, |body, (ident, irrelev)| { + Expr::lambda(ident.range, ident.clone(), body, *irrelev) + }) } pub fn app(range: Range, ident: Box, spine: Vec) -> Box { @@ -235,7 +237,7 @@ pub enum Num { #[derive(Clone, Debug, Hash, PartialEq, Eq)] pub enum NumType { U60, - U120 + U120, } /// An argument is a 'binding' of a name to a type @@ -316,7 +318,7 @@ impl Expr { impl Display for AppBinding { fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { if self.erased { - write!(f, "{{{}}}", self.data) + write!(f, "-({})", self.data) } else { write!(f, "{}", self.data) } @@ -337,7 +339,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, "(## {}/{} {})",name, redx, expr), + Sub(name, _, redx, expr) => write!(f, "(## {}/{} {})", name, redx, expr), App(head, spine) => write!( f, "({}{})", diff --git a/src/kind-tree/src/symbol.rs b/src/kind-tree/src/symbol.rs index 9eb2e326..79100eda 100644 --- a/src/kind-tree/src/symbol.rs +++ b/src/kind-tree/src/symbol.rs @@ -41,7 +41,7 @@ impl QualifiedIdent { aux, range, used_by_sugar: false, - generated: false + generated: false, } } @@ -60,7 +60,7 @@ impl QualifiedIdent { Ident { data: Symbol(self.to_string()), range: self.range, - generated: self.generated + generated: self.generated, } } @@ -70,7 +70,7 @@ impl QualifiedIdent { aux: aux.map(Symbol), range, used_by_sugar: false, - generated: false + generated: false, } } @@ -80,7 +80,7 @@ impl QualifiedIdent { aux: Some(Symbol(aux.to_string())), range, used_by_sugar: true, - generated: true + generated: true, } } @@ -90,7 +90,7 @@ impl QualifiedIdent { aux: self.aux.clone(), range: self.range, used_by_sugar: self.used_by_sugar, - generated: self.generated + generated: self.generated, } } @@ -105,7 +105,7 @@ impl Ident { Ident { data: Symbol(data), range, - generated: false + generated: false, } } @@ -113,7 +113,7 @@ impl Ident { Ident { data: Symbol(data.to_string()), range, - generated: false + generated: false, } } @@ -121,7 +121,7 @@ impl Ident { Ident { data: Symbol(data.to_string()), range, - generated: true + generated: true, } } @@ -190,7 +190,7 @@ impl Ident { Ident { data: self.data.clone(), range, - generated: false + generated: false, } } @@ -198,7 +198,7 @@ impl Ident { Ident { data: Symbol(format!("{}.{}", self.data.0, name)), range: self.range, - generated: false + generated: false, } } @@ -206,7 +206,7 @@ impl Ident { Ident { data: Symbol(data.to_string()), range: Range::ghost_range(), - generated: true + generated: true, } } }