mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-08-16 03:40:33 +03:00
fix: some fixes and cargo fmt
This commit is contained in:
felipegchi
parent
c7f9db59ba
commit
2c9285ab94
128
Cargo.lock
generated
128
Cargo.lock
generated
@ -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"
|
||||
|
||||
@ -1 +0,0 @@
|
||||
max_width = 180
|
||||
@ -60,7 +60,9 @@ fn mk_ctr(name: String, args: Vec<Box<Term>>) -> Box<Term> {
|
||||
}
|
||||
|
||||
fn mk_var(ident: &str) -> Box<Term> {
|
||||
Box::new(Term::Var { name: ident.to_string() })
|
||||
Box::new(Term::Var {
|
||||
name: ident.to_string(),
|
||||
})
|
||||
}
|
||||
|
||||
fn mk_u60(numb: u64) -> Box<Term> {
|
||||
@ -68,7 +70,10 @@ fn mk_u60(numb: u64) -> Box<Term> {
|
||||
}
|
||||
|
||||
fn mk_single_ctr(head: String) -> Box<Term> {
|
||||
Box::new(Term::Ctr { name: head, args: vec![] })
|
||||
Box::new(Term::Ctr {
|
||||
name: head,
|
||||
args: vec![],
|
||||
})
|
||||
}
|
||||
|
||||
fn mk_ctr_name(ident: &QualifiedIdent) -> Box<Term> {
|
||||
@ -77,15 +82,26 @@ fn mk_ctr_name(ident: &QualifiedIdent) -> Box<Term> {
|
||||
}
|
||||
|
||||
fn span_to_num(span: Span) -> Box<Term> {
|
||||
Box::new(Term::Num { numb: span.encode().0 })
|
||||
Box::new(Term::Num {
|
||||
numb: span.encode().0,
|
||||
})
|
||||
}
|
||||
|
||||
fn set_origin(ident: &Ident) -> Box<Term> {
|
||||
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<Term>) -> Box<Term> {
|
||||
Box::new(Term::Lam { name: name.to_string(), body })
|
||||
Box::new(Term::Lam {
|
||||
name: name.to_string(),
|
||||
body,
|
||||
})
|
||||
}
|
||||
|
||||
fn codegen_str(input: &str) -> Box<Term> {
|
||||
@ -103,12 +119,20 @@ fn codegen_str(input: &str) -> Box<Term> {
|
||||
)
|
||||
}
|
||||
|
||||
fn codegen_all_expr(lhs_rule: bool, lhs: bool, num: &mut usize, quote: bool, expr: &Expr) -> Box<Term> {
|
||||
fn codegen_all_expr(
|
||||
lhs_rule: bool,
|
||||
lhs: bool,
|
||||
num: &mut usize,
|
||||
quote: bool,
|
||||
expr: &Expr,
|
||||
) -> Box<Term> {
|
||||
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<Box<Term>> = spine.iter().cloned().map(|x| codegen_all_expr(lhs_rule, lhs, num, quote, &x)).collect();
|
||||
let new_spine: Vec<Box<Term>> = 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<T>(exprs: T) -> Box<Term>
|
||||
where
|
||||
T: Iterator<Item = Box<Term>>,
|
||||
{
|
||||
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::<Vec<Box<lang::Term>>>());
|
||||
let base_vars = lift_spine(
|
||||
(0..rule.pats.len())
|
||||
.map(|x| mk_var(&format!("x{}", x)))
|
||||
.collect::<Vec<Box<lang::Term>>>(),
|
||||
);
|
||||
|
||||
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::<Vec<Box<Term>>>();
|
||||
let lhs_args = rule
|
||||
.pats
|
||||
.iter()
|
||||
.map(|x| codegen_pattern(&mut count, false, x))
|
||||
.collect::<Vec<Box<Term>>>();
|
||||
|
||||
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<Box<Term>>, entry: &desugared::Rule, pats: &[Box<desugared::Expr>]) -> Box<Term> {
|
||||
fn codegen_entry_rules(
|
||||
count: &mut usize,
|
||||
index: usize,
|
||||
args: &mut Vec<Box<Term>>,
|
||||
entry: &desugared::Rule,
|
||||
pats: &[Box<desugared::Expr>],
|
||||
) -> Box<Term> {
|
||||
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<Box<Term>
|
||||
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::<Vec<Box<lang::Term>>>();
|
||||
let base_vars = (0..entry.args.len())
|
||||
.map(|x| mk_var(&format!("x{}", x)))
|
||||
.collect::<Vec<Box<lang::Term>>>();
|
||||
|
||||
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)]),
|
||||
|
||||
@ -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<DiagnosticFrame>) -> 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 {
|
||||
|
||||
@ -15,16 +15,12 @@ type Entry = (String, Box<Expr>, Vec<Box<Expr>>);
|
||||
pub struct Context(pub Vec<Entry>);
|
||||
|
||||
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<Range, String> {
|
||||
@ -70,8 +66,14 @@ fn parse_name(term: &Term) -> Result<String, String> {
|
||||
|
||||
fn parse_qualified(term: &Term) -> Result<QualifiedIdent, String> {
|
||||
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<Box<desugared::Expr>, String> {
|
||||
parse_all_expr(Default::default(), term)
|
||||
}
|
||||
|
||||
fn parse_all_expr(names: im::HashMap<String, String>, term: &Term) -> Result<Box<desugared::Expr>, String> {
|
||||
fn parse_all_expr(
|
||||
names: im::HashMap<String, String>,
|
||||
term: &Term,
|
||||
) -> Result<Box<desugared::Expr>, 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<String, String>, term: &Term) -> Result<Box
|
||||
parse_orig(&args[0])?,
|
||||
Ident::generate(&parse_name(&args[1])?),
|
||||
parse_all_expr(names, &args[2])?,
|
||||
false // TODO: Fix
|
||||
false, // TODO: Fix
|
||||
)),
|
||||
"Kind.Quoted.let" => Ok(Expr::let_(
|
||||
parse_orig(&args[0])?,
|
||||
@ -102,40 +107,53 @@ fn parse_all_expr(names: im::HashMap<String, String>, term: &Term) -> Result<Box
|
||||
parse_all_expr(names, &args[3])?,
|
||||
)),
|
||||
"Kind.Quoted.typ" => 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<String, String>, term: &Term) -> Result<Box
|
||||
parse_all_expr(names.clone(), &args[2])?,
|
||||
parse_all_expr(names, &args[3])?,
|
||||
)),
|
||||
tag => 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<TypeError, String> {
|
||||
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,
|
||||
|
||||
@ -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<T>(
|
||||
}
|
||||
|
||||
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);
|
||||
|
||||
@ -3,4 +3,4 @@ use kind_cli::{run_cli, Cli};
|
||||
|
||||
pub fn main() {
|
||||
run_cli(Cli::parse())
|
||||
}
|
||||
}
|
||||
|
||||
@ -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::<Vec<DiagnosticFrame>>();
|
||||
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::<Diagnostic>::into(&diagnostic);
|
||||
diag.render(&mut session, &render, &mut res_string).unwrap();
|
||||
}
|
||||
|
||||
res_string
|
||||
}
|
||||
}
|
||||
})?;
|
||||
Ok(())
|
||||
}
|
||||
|
||||
25
src/kind-cli/tests/suite/checker/derive/Eq.golden
Normal file
25
src/kind-cli/tests/suite/checker/derive/Eq.golden
Normal file
@ -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 <t: Type> (a: t) ~ (b: t) {
|
||||
2 | refl : Equal t a a
|
||||
| v---
|
||||
| \ Here!
|
||||
3 | }
|
||||
|
||||
6
src/kind-cli/tests/suite/checker/derive/Eq.kind2
Normal file
6
src/kind-cli/tests/suite/checker/derive/Eq.kind2
Normal file
@ -0,0 +1,6 @@
|
||||
Equal.match <t: Type> <a: t> <b: t> (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 <t: Type> (a: t) (b: t) : Type
|
||||
|
||||
Equal.refl <t: Type> <a: t> : (Equal t a a)
|
||||
1
src/kind-cli/tests/suite/checker/derive/Nat.golden
Normal file
1
src/kind-cli/tests/suite/checker/derive/Nat.golden
Normal file
@ -0,0 +1 @@
|
||||
Ok!
|
||||
8
src/kind-cli/tests/suite/checker/derive/Nat.kind2
Normal file
8
src/kind-cli/tests/suite/checker/derive/Nat.kind2
Normal file
@ -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
|
||||
1
src/kind-cli/tests/suite/checker/derive/Vec.golden
Normal file
1
src/kind-cli/tests/suite/checker/derive/Vec.golden
Normal file
@ -0,0 +1 @@
|
||||
Ok!
|
||||
10
src/kind-cli/tests/suite/checker/derive/Vec.kind2
Normal file
10
src/kind-cli/tests/suite/checker/derive/Vec.kind2
Normal file
@ -0,0 +1,10 @@
|
||||
type Nat {
|
||||
succ (pred: Nat)
|
||||
zero
|
||||
}
|
||||
|
||||
type Vec (t: Type) ~ (n: Nat) {
|
||||
cons <size: Nat> (x: t) (xs: Vec t size) : Vec t (Nat.succ size)
|
||||
nil : Vec t Nat.zero
|
||||
}
|
||||
|
||||
@ -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<Expr> { Box::new(Expr { data: ExprKind::Var(name), range }) };
|
||||
let mk_var = |name: Ident| -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::Var(name),
|
||||
range,
|
||||
})
|
||||
};
|
||||
|
||||
let mk_cons = |name: QualifiedIdent, spine: Vec<Binding>| -> Box<Expr> {
|
||||
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<AppBinding> = sum.parameters.iter().map(|x| AppBinding::explicit(mk_var(x.name.clone()))).collect();
|
||||
|
||||
let indice_names: Vec<AppBinding> = sum.indices.iter().map(|x| AppBinding::explicit(mk_var(x.name.clone()))).collect();
|
||||
let indice_names: Vec<AppBinding> = 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<Binding> = cons.args.iter().map(|x| Binding::Positional(mk_var(x.name.clone()))).collect();
|
||||
let vars: Vec<Binding> = 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<AppBinding> = [parameter_names.as_slice(), indice_names.as_slice()].concat();
|
||||
let mut res: Vec<AppBinding> = [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 {
|
||||
|
||||
@ -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(),
|
||||
);
|
||||
|
||||
|
||||
@ -23,33 +23,34 @@ impl From<DriverError> 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::<Vec<String>>().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::<Vec<String>>().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<DriverError> 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<DriverError> for DiagnosticFrame {
|
||||
title: format!("Cannot find file '{}'", file),
|
||||
subtitles: vec![],
|
||||
hints: vec![],
|
||||
positions: vec![]
|
||||
}
|
||||
positions: vec![],
|
||||
},
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@ -46,7 +46,7 @@ pub fn to_book(session: &mut Session, path: &PathBuf) -> Option<concrete::Book>
|
||||
let failed = resolution::check_unbound_top_level(session, &mut concrete_book);
|
||||
|
||||
if failed {
|
||||
return None
|
||||
return None;
|
||||
}
|
||||
|
||||
Some(concrete_book)
|
||||
|
||||
@ -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<PathBuf>) {
|
||||
fn accumulate_neighbour_paths(ident: &QualifiedIdent, raw_path: &Path) -> Result<Option<PathBuf>, 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<Boo
|
||||
}
|
||||
}
|
||||
|
||||
pub fn check_unbound_top_level(session: &mut Session, book : &mut Book) -> 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<Ident> = 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
|
||||
}
|
||||
}
|
||||
|
||||
@ -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]
|
||||
@ -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);
|
||||
}
|
||||
}
|
||||
@ -228,7 +228,7 @@ impl From<SyntaxError> 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 {
|
||||
|
||||
@ -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<QualifiedIdent, SyntaxError> {
|
||||
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<Box<Expr>, 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<Box<Expr>, SyntaxError> {
|
||||
@ -346,6 +364,17 @@ impl<'a> Parser<'a> {
|
||||
}))
|
||||
}
|
||||
|
||||
pub fn parse_num_lit(&mut self) -> Result<usize, SyntaxError> {
|
||||
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<Box<Expr>, SyntaxError> {
|
||||
self.ignore_docs();
|
||||
match self.get().clone() {
|
||||
@ -381,16 +410,16 @@ impl<'a> Parser<'a> {
|
||||
|
||||
fn parse_app_binding(&mut self) -> Result<AppBinding, SyntaxError> {
|
||||
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<Binding>), SyntaxError> {
|
||||
fn parse_call_tail(
|
||||
&mut self,
|
||||
start: Range,
|
||||
multiline: bool,
|
||||
) -> Result<(Range, Vec<Binding>), 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<Range>, Vec<CaseBinding>, Option<Range>), SyntaxError> {
|
||||
pub fn parse_pat_destruct_bindings(
|
||||
&mut self,
|
||||
) -> Result<(Option<Range>, Vec<CaseBinding>, Option<Range>), 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_),
|
||||
|
||||
@ -18,11 +18,7 @@ pub struct Lexer<'a> {
|
||||
}
|
||||
|
||||
impl<'a> Lexer<'a> {
|
||||
pub fn new(
|
||||
input: &'a str,
|
||||
peekable: Peekable<Chars<'a>>,
|
||||
ctx: SyntaxCtxIndex,
|
||||
) -> Lexer<'a> {
|
||||
pub fn new(input: &'a str, peekable: Peekable<Chars<'a>>, ctx: SyntaxCtxIndex) -> Lexer<'a> {
|
||||
Lexer {
|
||||
input,
|
||||
pos: 0,
|
||||
|
||||
@ -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"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@ -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)
|
||||
|
||||
@ -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<Ident> = sum.parameters.extend(&sum.indices).iter().map(|x| x.name.clone()).collect();
|
||||
let mut idx: Vec<Ident> = 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)
|
||||
|
||||
@ -33,7 +33,7 @@ impl<'a> DesugarState<'a> {
|
||||
range,
|
||||
sub.name.clone(),
|
||||
sub.indx,
|
||||
sub.redx.clone(),
|
||||
sub.redx,
|
||||
self.desugar_expr(&sub.expr),
|
||||
)
|
||||
}
|
||||
|
||||
@ -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
|
||||
|
||||
@ -42,7 +42,11 @@ pub struct ErasureState<'a> {
|
||||
failed: bool,
|
||||
}
|
||||
|
||||
pub fn erase_book(book: &Book, errs: Sender<DiagnosticFrame>, entrypoint: FxHashSet<String>) -> Option<Book> {
|
||||
pub fn erase_book(
|
||||
book: &Book,
|
||||
errs: Sender<DiagnosticFrame>,
|
||||
entrypoint: FxHashSet<String>,
|
||||
) -> Option<Book> {
|
||||
let mut state = ErasureState {
|
||||
errs,
|
||||
book,
|
||||
@ -61,7 +65,9 @@ pub fn erase_book(book: &Book, errs: Sender<DiagnosticFrame>, 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<Range>, used: Range, declared_ty: Option<Range>) {
|
||||
self.errs.send(PassError::CannotUseIrrelevant(declared_val, used, declared_ty).into()).unwrap();
|
||||
pub fn err_irrelevant(
|
||||
&mut self,
|
||||
declared_val: Option<Range>,
|
||||
used: Range,
|
||||
declared_ty: Option<Range>,
|
||||
) {
|
||||
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<Range>, Relevance), right: (Option<Range>, Relevance), visited: &mut FxHashSet<usize>, relevance_unify: bool) -> bool {
|
||||
pub fn unify_loop(
|
||||
&mut self,
|
||||
range: Range,
|
||||
left: (Option<Range>, Relevance),
|
||||
right: (Option<Range>, Relevance),
|
||||
visited: &mut FxHashSet<usize>,
|
||||
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<Range>, Relevance), right: (Option<Range>, Relevance), relevance_unify: bool) -> bool {
|
||||
pub fn unify(
|
||||
&mut self,
|
||||
range: Range,
|
||||
left: (Option<Range>, Relevance),
|
||||
right: (Option<Range>, 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<Range>, Relevance), name: &QualifiedIdent, spine: &Vec<Box<Expr>>) -> Vec<Box<Expr>> {
|
||||
pub fn erase_pat_spine(
|
||||
&mut self,
|
||||
on: (Option<Range>, Relevance),
|
||||
name: &QualifiedIdent,
|
||||
spine: &Vec<Box<Expr>>,
|
||||
) -> Vec<Box<Expr>> {
|
||||
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<Range>, Relevance), args: Vec<(Range, bool)>, rule: &Rule) -> Rule {
|
||||
pub fn erase_rule(
|
||||
&mut self,
|
||||
place: &(Option<Range>, 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::<Vec<Rule>>();
|
||||
let rules = entry
|
||||
.rules
|
||||
.iter()
|
||||
.map(|rule| self.erase_rule(&place, args.clone(), rule))
|
||||
.collect::<Vec<Rule>>();
|
||||
Box::new(Entry {
|
||||
name: entry.name.clone(),
|
||||
args: entry.args.clone(),
|
||||
|
||||
@ -95,30 +95,29 @@ impl From<PassError> 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<PassError> 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<PassError> 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<PassError> 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<PassError> 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<PassError> 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<PassError> 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<PassError> 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<PassError> 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<PassError> 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<PassError> 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::<Vec<String>>().join(", "))],
|
||||
hints: vec![format!(
|
||||
"Need variables for {}",
|
||||
other.iter().map(|x| format!("'{}'", x)).collect::<Vec<String>>().join(", ")
|
||||
)],
|
||||
positions: vec![Marker {
|
||||
position: place,
|
||||
color: Color::Fst,
|
||||
@ -435,20 +438,22 @@ impl From<PassError> 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,
|
||||
},
|
||||
],
|
||||
},
|
||||
}
|
||||
}
|
||||
|
||||
@ -6,6 +6,6 @@
|
||||
|
||||
pub mod desugar;
|
||||
pub mod erasure;
|
||||
mod errors;
|
||||
pub mod expand;
|
||||
pub mod unbound;
|
||||
mod errors;
|
||||
|
||||
@ -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<DiagnosticFrame>,
|
||||
pub context_vars: Vec<(Range, String)>,
|
||||
pub top_level_defs: FxHashMap<String, Range>,
|
||||
pub unbound_top_level: FxHashMap<String, FxHashSet<QualifiedIdent>>,
|
||||
pub unbound: FxHashMap<String, Vec<Ident>>,
|
||||
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::<String, Range>::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
|
||||
|
||||
@ -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)?;
|
||||
}
|
||||
|
||||
|
||||
@ -38,8 +38,12 @@ pub fn compile_term(expr: &desugared::Expr) -> Box<Term> {
|
||||
}),
|
||||
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"),
|
||||
|
||||
@ -27,7 +27,7 @@ pub type Spine = Vec<Binding>;
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
pub struct AppBinding {
|
||||
pub data: Box<Expr>,
|
||||
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<Expr>,
|
||||
}
|
||||
@ -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::<String>()
|
||||
),
|
||||
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::<Vec<String>>()
|
||||
.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),
|
||||
|
||||
@ -20,7 +20,7 @@ pub type Spine = Vec<Box<Expr>>;
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
pub struct AppBinding {
|
||||
pub data: Box<Expr>,
|
||||
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<Expr>, Box<Expr>),
|
||||
/// Substitution
|
||||
Sub(Ident, usize, Ident, Box<Expr>),
|
||||
Sub(Ident, usize, usize, Box<Expr>),
|
||||
/// 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<Expr>) -> Box<Expr> {
|
||||
pub fn sub(range: Range, ident: Ident, idx: usize, rdx: usize, body: Box<Expr>) -> Box<Expr> {
|
||||
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<Expr>, spine: Vec<AppBinding>) -> Box<Expr> {
|
||||
@ -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,
|
||||
"({}{})",
|
||||
|
||||
@ -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,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user