mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-10-04 00:37:39 +03:00
style: added a lot of tests, benchmarks and fixed code style
This commit is contained in:
parent
bd26cf3ce7
commit
9f94818d41
7
Cargo.lock
generated
7
Cargo.lock
generated
@ -675,8 +675,13 @@ version = "0.1.0"
|
||||
dependencies = [
|
||||
"kind-checker",
|
||||
"kind-driver",
|
||||
"kind-query",
|
||||
"kind-parser",
|
||||
"kind-pass",
|
||||
"kind-report",
|
||||
"kind-span",
|
||||
"kind-target-hvm",
|
||||
"kind-target-kdl",
|
||||
"kind-tree",
|
||||
"ntest",
|
||||
"pretty_assertions",
|
||||
"walkdir",
|
||||
|
@ -17,4 +17,10 @@ members = [
|
||||
# "crates/kind-lint",
|
||||
# "crates/kind-query",
|
||||
# "crates/kind-macros",
|
||||
]
|
||||
]
|
||||
|
||||
[profile.test.package.hvm]
|
||||
opt-level = 3
|
||||
|
||||
[profile.bench.package.hvm]
|
||||
opt-level = 3
|
||||
|
@ -525,14 +525,14 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) {
|
||||
vec_preppend![
|
||||
mk_ctr_name(&entry.name),
|
||||
mk_var("orig");
|
||||
base_vars.clone()
|
||||
base_vars
|
||||
],
|
||||
),
|
||||
rhs: mk_ctr(
|
||||
TermTag::HoasF(entry.name.to_string()).to_string(),
|
||||
vec_preppend![
|
||||
mk_var("orig");
|
||||
base_vars.clone()
|
||||
base_vars
|
||||
],
|
||||
),
|
||||
});
|
||||
@ -543,7 +543,7 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) {
|
||||
vec_preppend![
|
||||
mk_ctr_name(&entry.name),
|
||||
mk_var("orig");
|
||||
base_vars.clone()
|
||||
base_vars
|
||||
],
|
||||
),
|
||||
rhs: mk_ctr(
|
||||
@ -584,7 +584,7 @@ pub fn codegen_book(book: &Book, functions_to_check: Vec<String>) -> lang::File
|
||||
|
||||
let functions_entry = lang::Rule {
|
||||
lhs: mk_ctr("Functions".to_owned(), vec![]),
|
||||
rhs: codegen_vec(functions_to_check.iter().map(|x| mk_ctr_name_from_str(&x))),
|
||||
rhs: codegen_vec(functions_to_check.iter().map(|x| mk_ctr_name_from_str(x))),
|
||||
};
|
||||
|
||||
for entry in book.entrs.values() {
|
||||
|
@ -56,12 +56,14 @@ pub fn type_check(
|
||||
) -> bool {
|
||||
let file = gen_checker(book, functions_to_check);
|
||||
|
||||
match eval(&file.to_string(), "Main", false) {
|
||||
match eval(&file, "Main", false) {
|
||||
Ok(term) => {
|
||||
let errs = parse_report(&term).expect(&format!(
|
||||
"Internal Error: Cannot parse the report message from the type checker: {}",
|
||||
term
|
||||
));
|
||||
let errs = parse_report(&term).unwrap_or_else(|_| {
|
||||
panic!(
|
||||
"Internal Error: Cannot parse the report message from the type checker: {}",
|
||||
term
|
||||
)
|
||||
});
|
||||
let succeeded = errs.is_empty();
|
||||
|
||||
for err in errs {
|
||||
@ -80,7 +82,7 @@ pub fn type_check(
|
||||
pub fn eval_api(book: &Book) -> Box<Term> {
|
||||
let file = gen_checker(book, Vec::new());
|
||||
|
||||
let file = language::syntax::read_file(&file.to_string()).unwrap();
|
||||
let file = language::syntax::read_file(&file).unwrap();
|
||||
|
||||
let book = language::rulebook::gen_rulebook(&file);
|
||||
|
||||
|
@ -17,11 +17,11 @@ impl Diagnostic for DeriveError {
|
||||
DeriveError::CannotUseNamedVariable(range) => DiagnosticFrame {
|
||||
code: 103,
|
||||
severity: Severity::Error,
|
||||
title: format!("Cannot use named variable on match derivations"),
|
||||
title: "Cannot use named variable on match derivations".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![],
|
||||
positions: vec![Marker {
|
||||
position: range.clone(),
|
||||
position: *range,
|
||||
color: Color::Fst,
|
||||
text: "Here!".to_string(),
|
||||
no_code: false,
|
||||
|
@ -160,7 +160,7 @@ pub fn derive_match(
|
||||
new_args.push(match arg {
|
||||
Binding::Positional(expr) => AppBinding::explicit(expr.clone()),
|
||||
Binding::Named(range, _, expr) => {
|
||||
errs.push(Box::new(DeriveError::CannotUseNamedVariable(range.clone())));
|
||||
errs.push(Box::new(DeriveError::CannotUseNamedVariable(*range)));
|
||||
AppBinding::explicit(expr.clone())
|
||||
}
|
||||
});
|
||||
@ -191,7 +191,7 @@ pub fn derive_match(
|
||||
types.push(Argument {
|
||||
hidden: false,
|
||||
erased: false,
|
||||
name: Ident::new_static(&format!("{}_", cons.name.to_string()), range),
|
||||
name: Ident::new_static(&format!("{}_", cons.name), range),
|
||||
typ: Some(cons_type),
|
||||
range,
|
||||
});
|
||||
@ -209,7 +209,7 @@ pub fn derive_match(
|
||||
rules: vec![],
|
||||
range,
|
||||
attrs: Vec::new(),
|
||||
generated_by: Some(sum.name.to_string().clone()),
|
||||
generated_by: Some(sum.name.to_string()),
|
||||
};
|
||||
return (entry, errs);
|
||||
}
|
||||
@ -262,7 +262,7 @@ pub fn derive_match(
|
||||
let renames = FxHashMap::from_iter(
|
||||
sum.parameters
|
||||
.extend(&cons.args)
|
||||
.map(|x| (x.name.to_string(), format!("{}_", x.name.to_string())))
|
||||
.map(|x| (x.name.to_string(), format!("{}_", x.name)))
|
||||
.iter()
|
||||
.cloned(),
|
||||
);
|
||||
|
@ -151,7 +151,7 @@ pub fn derive_open(range: Range, rec: &RecordDecl) -> concrete::Entry {
|
||||
range: rec.constructor.range,
|
||||
})];
|
||||
|
||||
let entry = Entry {
|
||||
Entry {
|
||||
name,
|
||||
docs: Vec::new(),
|
||||
args: types,
|
||||
@ -159,8 +159,6 @@ pub fn derive_open(range: Range, rec: &RecordDecl) -> concrete::Entry {
|
||||
rules,
|
||||
range: rec.constructor.range,
|
||||
attrs: Vec::new(),
|
||||
generated_by: Some(rec.name.to_string().clone()),
|
||||
};
|
||||
|
||||
entry
|
||||
generated_by: Some(rec.name.to_string()),
|
||||
}
|
||||
}
|
||||
|
@ -105,7 +105,7 @@ impl Diagnostic for DriverError {
|
||||
DriverError::ThereIsntAMain => DiagnosticFrame {
|
||||
code: 103,
|
||||
severity: Severity::Error,
|
||||
title: format!("Cannot find 'Main' function to run the file."),
|
||||
title: "Cannot find 'Main' function to run the file.".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![],
|
||||
positions: vec![],
|
||||
|
@ -1,6 +1,6 @@
|
||||
use checker::eval;
|
||||
use errors::DriverError;
|
||||
use kind_pass::{desugar, erasure, expand, inline::inline_book};
|
||||
use kind_pass::{desugar, erasure, inline::inline_book};
|
||||
use kind_report::report::FileCache;
|
||||
use kind_span::SyntaxCtxIndex;
|
||||
|
||||
@ -50,8 +50,6 @@ pub fn type_check_book(
|
||||
pub fn to_book(session: &mut Session, path: &PathBuf) -> Option<concrete::Book> {
|
||||
let mut concrete_book = resolution::parse_and_store_book(session, path)?;
|
||||
|
||||
expand::expand_book(session.diagnostic_sender.clone(), &mut concrete_book);
|
||||
|
||||
let failed = resolution::check_unbound_top_level(session, &mut concrete_book);
|
||||
|
||||
if failed {
|
||||
|
@ -4,6 +4,7 @@
|
||||
//! depedencies.
|
||||
|
||||
use fxhash::FxHashSet;
|
||||
use kind_pass::expand::expand_module;
|
||||
use kind_pass::expand::uses::expand_uses;
|
||||
use std::fs;
|
||||
use std::path::{Path, PathBuf};
|
||||
@ -64,10 +65,10 @@ fn ident_to_path(
|
||||
let mut raw_path = root.to_path_buf();
|
||||
raw_path.push(PathBuf::from(segments.join("/")));
|
||||
|
||||
match accumulate_neighbour_paths(&ident, &raw_path) {
|
||||
match accumulate_neighbour_paths(ident, &raw_path) {
|
||||
Ok(None) if search_on_parent => {
|
||||
raw_path.pop();
|
||||
accumulate_neighbour_paths(&ident, &raw_path)
|
||||
accumulate_neighbour_paths(ident, &raw_path)
|
||||
}
|
||||
rest => rest,
|
||||
}
|
||||
@ -110,7 +111,7 @@ fn module_to_book<'a>(
|
||||
|
||||
for cons in &sum.constructors {
|
||||
let mut cons_ident = sum.name.add_segment(cons.name.to_str());
|
||||
cons_ident.range = cons.name.range.clone();
|
||||
cons_ident.range = cons.name.range;
|
||||
if try_to_insert_new_name(failed, session, cons_ident.clone(), book) {
|
||||
public_names.insert(cons_ident.to_string());
|
||||
book.count
|
||||
@ -156,10 +157,10 @@ fn module_to_book<'a>(
|
||||
public_names
|
||||
}
|
||||
|
||||
fn parse_and_store_book_by_identifier<'a>(
|
||||
fn parse_and_store_book_by_identifier(
|
||||
session: &mut Session,
|
||||
ident: &QualifiedIdent,
|
||||
book: &'a mut Book,
|
||||
book: &mut Book,
|
||||
) -> bool {
|
||||
if book.entries.contains_key(ident.to_string().as_str()) {
|
||||
return false;
|
||||
@ -175,10 +176,10 @@ fn parse_and_store_book_by_identifier<'a>(
|
||||
}
|
||||
}
|
||||
|
||||
fn parse_and_store_book_by_path<'a>(
|
||||
fn parse_and_store_book_by_path(
|
||||
session: &mut Session,
|
||||
path: &PathBuf,
|
||||
book: &'a mut Book,
|
||||
book: &mut Book,
|
||||
) -> bool {
|
||||
if !path.exists() {
|
||||
session
|
||||
@ -218,6 +219,8 @@ fn parse_and_store_book_by_path<'a>(
|
||||
|
||||
expand_uses(&mut module, session.diagnostic_sender.clone());
|
||||
|
||||
expand_module(session.diagnostic_sender.clone(), &mut module);
|
||||
|
||||
let mut state = UnboundCollector::new(session.diagnostic_sender.clone(), false);
|
||||
state.visit_module(&mut module);
|
||||
|
||||
@ -227,9 +230,12 @@ fn parse_and_store_book_by_path<'a>(
|
||||
}
|
||||
|
||||
module_to_book(&mut failed, session, module, book);
|
||||
|
||||
|
||||
for idents in state.unbound_top_level.values() {
|
||||
failed |= parse_and_store_book_by_identifier(session, &idents.iter().nth(0).unwrap(), book);
|
||||
let fst = idents.iter().next().unwrap();
|
||||
if !book.names.contains_key(&fst.to_string()) {
|
||||
failed |= parse_and_store_book_by_identifier(session, fst, book);
|
||||
}
|
||||
}
|
||||
|
||||
failed
|
||||
@ -276,7 +282,7 @@ pub fn check_unbound_top_level(session: &mut Session, book: &mut Book) -> bool {
|
||||
.map(|x| x.to_ident())
|
||||
.collect();
|
||||
if !res.is_empty() {
|
||||
unbound_variable(session, &book, &res);
|
||||
unbound_variable(session, book, &res);
|
||||
failed = true;
|
||||
}
|
||||
}
|
||||
|
@ -29,7 +29,7 @@ fn is_valid_id(chr: char) -> bool {
|
||||
}
|
||||
|
||||
fn is_valid_upper_start(chr: char) -> bool {
|
||||
matches!(chr, 'A'..='Z')
|
||||
chr.is_ascii_uppercase()
|
||||
}
|
||||
|
||||
fn is_valid_id_start(chr: char) -> bool {
|
||||
|
@ -143,7 +143,7 @@ impl<'a> DesugarState<'a> {
|
||||
if (fill_hidden && arg_decl.hidden) || arguments[i].is_some() {
|
||||
continue;
|
||||
}
|
||||
arguments[i] = Some((v.range, self.desugar_expr(&v)));
|
||||
arguments[i] = Some((v.range, self.desugar_expr(v)));
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
@ -20,13 +20,13 @@ impl<'a> DesugarState<'a> {
|
||||
}
|
||||
|
||||
fn attr_invalid_argument(&mut self, attr: &Attribute) {
|
||||
if !attr.value.is_some() {
|
||||
if attr.value.is_none() {
|
||||
self.send_err(PassError::InvalidAttributeArgument(attr.range))
|
||||
};
|
||||
}
|
||||
|
||||
fn attr_expects_a_value(&mut self, attr: &Attribute) {
|
||||
if !attr.value.is_some() {
|
||||
if attr.value.is_none() {
|
||||
self.send_err(PassError::AttributeExpectsAValue(attr.range))
|
||||
};
|
||||
}
|
||||
|
@ -25,7 +25,7 @@ enum Ambient {
|
||||
}
|
||||
|
||||
impl Ambient {
|
||||
pub fn to_relev(&self) -> Relevance {
|
||||
pub fn as_relevance(&self) -> Relevance {
|
||||
match self {
|
||||
Ambient::Irrelevant => Relevance::Irrelevant,
|
||||
Ambient::Unknown | Ambient::Relevant => Relevance::Relevant,
|
||||
@ -51,8 +51,8 @@ pub struct ErasureState<'a> {
|
||||
failed: bool,
|
||||
}
|
||||
|
||||
pub fn erase_book<'a>(
|
||||
book: &'a desugared::Book,
|
||||
pub fn erase_book(
|
||||
book: &desugared::Book,
|
||||
errs: Sender<Box<dyn Diagnostic>>,
|
||||
entrypoints: Vec<String>,
|
||||
) -> Option<untyped::Book> {
|
||||
@ -416,7 +416,7 @@ impl<'a> ErasureState<'a> {
|
||||
Let { name, val, next } => {
|
||||
let backup = self.ctx.clone();
|
||||
|
||||
self.ctx.insert(name.to_string(), ambient.to_relev());
|
||||
self.ctx.insert(name.to_string(), ambient.as_relevance());
|
||||
|
||||
let val = self.erase_expr(ambient, edge, val);
|
||||
let next = self.erase_expr(ambient, edge, next);
|
||||
@ -475,7 +475,7 @@ impl<'a> ErasureState<'a> {
|
||||
let var_rev = self
|
||||
.ctx
|
||||
.get(&name.to_string())
|
||||
.expect(&format!("Uwnraping {}", name));
|
||||
.unwrap();
|
||||
|
||||
if *var_rev == Relevance::Irrelevant && ambient != Ambient::Irrelevant {
|
||||
self.set_relevance(edge, Relevance::Irrelevant, name.range)
|
||||
|
@ -535,7 +535,7 @@ impl Diagnostic for PassError {
|
||||
PassError::AttributeExpectsAValue(place) => DiagnosticFrame {
|
||||
code: 209,
|
||||
severity: Severity::Error,
|
||||
title: format!("This attribute expects a value"),
|
||||
title: "This attribute expects a value".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![],
|
||||
positions: vec![Marker {
|
||||
@ -549,7 +549,7 @@ impl Diagnostic for PassError {
|
||||
PassError::AttributeDoesNotExists(place) => DiagnosticFrame {
|
||||
code: 209,
|
||||
severity: Severity::Error,
|
||||
title: format!("This attribute does not exists"),
|
||||
title: "This attribute does not exists".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![],
|
||||
positions: vec![Marker {
|
||||
|
@ -13,7 +13,8 @@ use kind_derive::setters::derive_setters;
|
||||
use kind_report::data::Diagnostic;
|
||||
use kind_span::Locatable;
|
||||
use kind_span::Range;
|
||||
use kind_tree::concrete::{Attribute, Book, TopLevel};
|
||||
use kind_tree::concrete::Module;
|
||||
use kind_tree::concrete::{Attribute, TopLevel};
|
||||
|
||||
use crate::errors::PassError;
|
||||
/// Expands sum type and record definitions to a lot of
|
||||
@ -127,12 +128,12 @@ pub fn expand_derive(
|
||||
}
|
||||
}
|
||||
|
||||
pub fn expand_book(error_channel: Sender<Box<dyn Diagnostic>>, book: &mut Book) -> bool {
|
||||
pub fn expand_module(error_channel: Sender<Box<dyn Diagnostic>>, module: &mut Module) -> bool {
|
||||
let mut failed = false;
|
||||
|
||||
let mut entries = FxHashMap::default();
|
||||
|
||||
for entry in book.entries.values() {
|
||||
for entry in &module.entries {
|
||||
match entry {
|
||||
TopLevel::SumType(sum) => {
|
||||
if let Some(derive) = expand_derive(error_channel.clone(), &sum.attrs) {
|
||||
@ -196,10 +197,8 @@ pub fn expand_book(error_channel: Sender<Box<dyn Diagnostic>>, book: &mut Book)
|
||||
}
|
||||
}
|
||||
|
||||
for (name, (tl, count)) in entries {
|
||||
book.count.insert(name.clone(), count);
|
||||
book.names.insert(name.clone().to_string(), tl.name.clone());
|
||||
book.entries.insert(name.clone(), TopLevel::Entry(tl));
|
||||
for (_, (tl, _)) in entries {
|
||||
module.entries.push(TopLevel::Entry(tl));
|
||||
}
|
||||
|
||||
failed
|
||||
|
@ -90,9 +90,9 @@ fn get_colorizer<T>(color: &Color) -> &dyn Fn(T) -> Paint<T> {
|
||||
|
||||
// TODO: Remove common indentation.
|
||||
// TODO: Prioritize inline marcations.
|
||||
fn colorize_code<'a, T: Write + Sized>(
|
||||
fn colorize_code<T: Write + Sized>(
|
||||
markers: &mut [&(Point, Point, &Marker)],
|
||||
code_line: &'a str,
|
||||
code_line: &str,
|
||||
modify: &dyn Fn(&str) -> String,
|
||||
fmt: &mut T,
|
||||
) -> std::fmt::Result {
|
||||
|
@ -11,7 +11,7 @@ pub fn compile_book(book: untyped::Book, trace: bool) -> File {
|
||||
smaps: Default::default(),
|
||||
};
|
||||
for (_, entry) in book.entrs {
|
||||
compile_entry(&mut file, *entry, trace);
|
||||
compile_entry(&mut file, entry, trace);
|
||||
}
|
||||
file
|
||||
}
|
||||
@ -46,7 +46,7 @@ pub fn compile_term(expr: &untyped::Expr) -> Box<Term> {
|
||||
App { fun, args } => args.iter().fold(compile_term(fun), |func, arg| {
|
||||
Box::new(Term::App {
|
||||
func,
|
||||
argm: compile_term(&arg),
|
||||
argm: compile_term(arg),
|
||||
})
|
||||
}),
|
||||
Fun { name, args } | Ctr { name, args } => Box::new(Term::Ctr {
|
||||
@ -96,11 +96,11 @@ fn compile_rule(name: String, rule: untyped::Rule) -> Rule {
|
||||
}
|
||||
}
|
||||
|
||||
fn compile_entry(file: &mut File, entry: untyped::Entry, trace: bool) {
|
||||
fn compile_entry(file: &mut File, entry: Box<untyped::Entry>, trace: bool) {
|
||||
if entry.attrs.trace.is_some() || trace {
|
||||
let _with_args = entry.attrs.trace.unwrap_or(false);
|
||||
|
||||
let name_trace = format!("{}__trace", entry.name.to_string());
|
||||
let name_trace = format!("{}__trace", entry.name);
|
||||
for rule in entry.rules {
|
||||
file.rules.push(compile_rule(name_trace.clone(), rule))
|
||||
}
|
||||
|
@ -65,8 +65,8 @@ fn encode_base64_u8(num: u8) -> char {
|
||||
|
||||
fn u128_to_kdl_name(mut num: u128) -> String {
|
||||
let mut encoded = [0 as char; 12];
|
||||
for i in 0..12 {
|
||||
encoded[i] = encode_base64_u8((num & 0x3f) as u8);
|
||||
for item in &mut encoded {
|
||||
*item = encode_base64_u8((num & 0x3f) as u8);
|
||||
num >>= 6;
|
||||
}
|
||||
encoded.into_iter().collect()
|
||||
@ -127,7 +127,7 @@ pub fn compile_book(
|
||||
}
|
||||
|
||||
pub fn compile_rule(ctx: &mut CompileCtx, rule: &untyped::Rule) -> kindelia_lang::ast::Rule {
|
||||
let name = ctx.kdl_names.get(rule.name.to_str()).unwrap().clone();
|
||||
let name = *ctx.kdl_names.get(rule.name.to_str()).unwrap();
|
||||
let mut args = Vec::new();
|
||||
for pat in &rule.pats {
|
||||
let arg = compile_expr(ctx, pat);
|
||||
@ -135,8 +135,8 @@ pub fn compile_rule(ctx: &mut CompileCtx, rule: &untyped::Rule) -> kindelia_lang
|
||||
}
|
||||
let lhs = kdl::Term::ctr(name, args);
|
||||
let rhs = compile_expr(ctx, &rule.body);
|
||||
let rule = kdl::Rule { lhs, rhs };
|
||||
rule
|
||||
|
||||
kdl::Rule { lhs, rhs }
|
||||
}
|
||||
|
||||
pub fn err_term() -> kindelia_lang::ast::Term {
|
||||
@ -152,7 +152,7 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kindelia_lang
|
||||
From::App { fun, args } => {
|
||||
let mut expr = compile_expr(ctx, fun);
|
||||
for binding in args {
|
||||
let body = compile_expr(ctx, &binding);
|
||||
let body = compile_expr(ctx, binding);
|
||||
expr = To::App {
|
||||
func: Box::new(expr),
|
||||
argm: Box::new(body),
|
||||
@ -306,14 +306,14 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kindelia_lang
|
||||
|
||||
// All other constructors have a normal compilation
|
||||
_ => {
|
||||
let name = ctx.kdl_names.get(name.to_str()).unwrap().clone();
|
||||
let args = args.iter().map(|x| compile_expr(ctx, &x)).collect();
|
||||
let name = *ctx.kdl_names.get(name.to_str()).unwrap();
|
||||
let args = args.iter().map(|x| compile_expr(ctx, x)).collect();
|
||||
To::Ctr { name, args }
|
||||
}
|
||||
}
|
||||
}
|
||||
From::Fun { name, args } => {
|
||||
let name = ctx.kdl_names.get(name.to_str()).unwrap().clone();
|
||||
let name = *ctx.kdl_names.get(name.to_str()).unwrap();
|
||||
let args = args.iter().map(|x| compile_expr(ctx, x)).collect();
|
||||
To::Fun { name, args }
|
||||
}
|
||||
@ -324,7 +324,7 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kindelia_lang
|
||||
} => {
|
||||
let name = kdl::Name::from_str(param.to_str());
|
||||
if let Ok(name) = name {
|
||||
let body = Box::new(compile_expr(ctx, &body));
|
||||
let body = Box::new(compile_expr(ctx, body));
|
||||
To::Lam { name, body }
|
||||
} else {
|
||||
ctx.send_err(Box::new(KdlError::InvalidVarName(param.range)));
|
||||
@ -334,7 +334,7 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kindelia_lang
|
||||
From::Let { name, val, next } => {
|
||||
let res_name = kdl::Name::from_str(name.to_str());
|
||||
if let Ok(name) = res_name {
|
||||
let expr = Box::new(compile_expr(ctx, &val));
|
||||
let expr = Box::new(compile_expr(ctx, val));
|
||||
let func = Box::new(To::Lam { name, body: expr });
|
||||
let argm = Box::new(compile_expr(ctx, next));
|
||||
To::App { func, argm }
|
||||
@ -364,14 +364,14 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kindelia_lang
|
||||
}
|
||||
From::Str { val } => {
|
||||
let nil = kdl::Term::Ctr {
|
||||
name: ctx.kdl_names.get("String.nil").unwrap().clone(),
|
||||
name: *ctx.kdl_names.get("String.nil").unwrap(),
|
||||
args: vec![],
|
||||
};
|
||||
|
||||
let cons_name = ctx.kdl_names.get("String.cons").unwrap().clone();
|
||||
let cons_name = *ctx.kdl_names.get("String.cons").unwrap();
|
||||
|
||||
let cons = |numb: u128, next| kdl::Term::Ctr {
|
||||
name: cons_name.clone(),
|
||||
name: cons_name,
|
||||
args: vec![
|
||||
kdl::Term::Num {
|
||||
numb: kdl::U120::new(numb).unwrap(),
|
||||
@ -414,7 +414,7 @@ pub fn compile_entry(ctx: &mut CompileCtx, entry: &untyped::Entry) {
|
||||
}
|
||||
}
|
||||
|
||||
if entry.rules.len() == 0 {
|
||||
if entry.rules.is_empty() {
|
||||
// Functions with no rules become Ctr
|
||||
let sttm = kdl::Statement::Ctr {
|
||||
name,
|
||||
@ -470,7 +470,7 @@ impl Display for File {
|
||||
writeln!(f, "{}", ctr.1)?;
|
||||
}
|
||||
|
||||
if self.ctrs.len() > 0 && self.funs.len() > 0 {
|
||||
if !self.ctrs.is_empty() && !self.funs.is_empty() {
|
||||
writeln!(f)?;
|
||||
}
|
||||
|
||||
|
@ -145,14 +145,14 @@ fn split_rule(
|
||||
|
||||
let new_ctr = Expr::ctr(name.range, name.clone(), new_ctr_args);
|
||||
|
||||
subst(&mut new_rule_body, &opat_name, &new_ctr);
|
||||
subst(&mut new_rule_body, opat_name, &new_ctr);
|
||||
}
|
||||
(ExprKind::Var { .. }, _) => {
|
||||
new_rule_pats.push(other_pat.clone());
|
||||
}
|
||||
(ExprKind::Num { .. }, ExprKind::Num { .. }) => (),
|
||||
(ExprKind::Num { .. }, ExprKind::Var { name }) => {
|
||||
subst(&mut new_rule_body, &name, rule_pat);
|
||||
subst(&mut new_rule_body, name, rule_pat);
|
||||
}
|
||||
_ => {
|
||||
panic!("Internal error. Please report."); // not possible since it matches
|
||||
@ -200,7 +200,7 @@ fn flatten_entry(entry: &Entry) -> Vec<Entry> {
|
||||
let rule = &entry.rules[i];
|
||||
if must_split(rule) {
|
||||
let (old_rule, split_entries) =
|
||||
split_rule(rule, &entry, i, &mut name_count, &mut skip);
|
||||
split_rule(rule, entry, i, &mut name_count, &mut skip);
|
||||
old_entry_rules.push(old_rule);
|
||||
new_entries.extend(split_entries);
|
||||
} else {
|
||||
@ -234,7 +234,5 @@ pub fn flatten(book: untyped::Book) -> untyped::Book {
|
||||
}
|
||||
}
|
||||
|
||||
let book = Book { names, entrs };
|
||||
|
||||
book
|
||||
Book { names, entrs }
|
||||
}
|
||||
|
@ -46,13 +46,13 @@ impl LinearizeCtx {
|
||||
match arg {
|
||||
Term::Var { name } => {
|
||||
let new_name = self.create_name();
|
||||
self.name_table.insert(name.clone(), new_name);
|
||||
self.name_table.insert(*name, new_name);
|
||||
}
|
||||
Term::Ctr { name: _, args } => {
|
||||
for arg in args {
|
||||
if let Term::Var { name } = arg {
|
||||
let new_name = self.create_name();
|
||||
self.name_table.insert(name.clone(), new_name);
|
||||
self.name_table.insert(*name, new_name);
|
||||
} else {
|
||||
unreachable!(); // We expect a flat rule
|
||||
}
|
||||
@ -128,7 +128,7 @@ pub fn linearize_rule(rule: Rule) -> Rule {
|
||||
let lhs = linearize_term(&mut ctx, &rule.lhs, true);
|
||||
let vals: Vec<Name> = ctx.name_table.values().map(Name::clone).collect();
|
||||
for val in vals {
|
||||
let expr = Box::new(Term::Var { name: val.clone() });
|
||||
let expr = Box::new(Term::Var { name: val });
|
||||
rhs = dup_var(&mut ctx, &val, expr, rhs);
|
||||
}
|
||||
Rule {
|
||||
@ -141,7 +141,7 @@ pub fn linearize_term(ctx: &mut LinearizeCtx, term: &Term, lhs: bool) -> Box<Ter
|
||||
let term = match term {
|
||||
Term::Var { name } => {
|
||||
if lhs {
|
||||
let mut name = ctx.name_table.get(name).unwrap_or(name).clone();
|
||||
let mut name = *ctx.name_table.get(name).unwrap_or(name);
|
||||
rename_erased(ctx, &mut name);
|
||||
Term::Var { name }
|
||||
} else {
|
||||
@ -150,7 +150,7 @@ pub fn linearize_term(ctx: &mut LinearizeCtx, term: &Term, lhs: bool) -> Box<Ter
|
||||
if let Some(name) = ctx.name_table.get(name) {
|
||||
let used = *ctx
|
||||
.uses
|
||||
.entry(name.clone())
|
||||
.entry(*name)
|
||||
.and_modify(|x| *x += 1)
|
||||
.or_insert(1);
|
||||
let name = Name::from_str(&format!("{}.{}", name, used - 1)).unwrap(); // TODO: Think if this errs or not
|
||||
@ -171,16 +171,16 @@ pub fn linearize_term(ctx: &mut LinearizeCtx, term: &Term, lhs: bool) -> Box<Ter
|
||||
let expr = linearize_term(ctx, expr, lhs);
|
||||
let got_0 = ctx.name_table.remove(nam0);
|
||||
let got_1 = ctx.name_table.remove(nam0);
|
||||
ctx.name_table.insert(nam0.clone(), new_nam0.clone());
|
||||
ctx.name_table.insert(nam1.clone(), new_nam1.clone());
|
||||
ctx.name_table.insert(*nam0, new_nam0);
|
||||
ctx.name_table.insert(*nam1, new_nam1);
|
||||
let body = linearize_term(ctx, body, lhs);
|
||||
ctx.name_table.remove(nam0);
|
||||
if let Some(x) = got_0 {
|
||||
ctx.name_table.insert(nam0.clone(), x);
|
||||
ctx.name_table.insert(*nam0, x);
|
||||
}
|
||||
ctx.name_table.remove(nam1);
|
||||
if let Some(x) = got_1 {
|
||||
ctx.name_table.insert(nam1.clone(), x);
|
||||
ctx.name_table.insert(*nam1, x);
|
||||
}
|
||||
let nam0 = Name::from_str(&format!("{}{}", new_nam0, ".0")).unwrap();
|
||||
let nam1 = Name::from_str(&format!("{}{}", new_nam1, ".0")).unwrap();
|
||||
@ -194,14 +194,14 @@ pub fn linearize_term(ctx: &mut LinearizeCtx, term: &Term, lhs: bool) -> Box<Ter
|
||||
Term::Lam { name, body } => {
|
||||
let mut new_name = ctx.create_name();
|
||||
let got_name = ctx.name_table.remove(name);
|
||||
ctx.name_table.insert(name.clone(), new_name.clone());
|
||||
ctx.name_table.insert(*name, new_name);
|
||||
let body = linearize_term(ctx, body, lhs);
|
||||
ctx.name_table.remove(name);
|
||||
if let Some(x) = got_name {
|
||||
ctx.name_table.insert(name.clone(), x);
|
||||
ctx.name_table.insert(*name, x);
|
||||
}
|
||||
let expr = Box::new(Term::Var {
|
||||
name: new_name.clone(),
|
||||
name: new_name,
|
||||
});
|
||||
let body = dup_var(ctx, &new_name, expr, body);
|
||||
rename_erased(ctx, &mut new_name);
|
||||
@ -222,7 +222,7 @@ pub fn linearize_term(ctx: &mut LinearizeCtx, term: &Term, lhs: bool) -> Box<Ter
|
||||
new_args.push(*arg);
|
||||
}
|
||||
Term::Ctr {
|
||||
name: name.clone(),
|
||||
name: *name,
|
||||
args: new_args,
|
||||
}
|
||||
}
|
||||
@ -233,7 +233,7 @@ pub fn linearize_term(ctx: &mut LinearizeCtx, term: &Term, lhs: bool) -> Box<Ter
|
||||
new_args.push(*arg);
|
||||
}
|
||||
Term::Fun {
|
||||
name: name.clone(),
|
||||
name: *name,
|
||||
args: new_args,
|
||||
}
|
||||
}
|
||||
|
@ -5,11 +5,18 @@ edition = "2021"
|
||||
|
||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||
|
||||
[dependencies]
|
||||
[dev-dependencies]
|
||||
kind-driver = { path = "../kind-driver" }
|
||||
kind-report = { path = "../kind-report" }
|
||||
kind-parser = { path = "../kind-parser" }
|
||||
kind-tree = { path = "../kind-tree" }
|
||||
kind-span = { path = "../kind-span" }
|
||||
kind-report = { path = "../kind-report" }
|
||||
kind-checker = { path = "../kind-checker" }
|
||||
kind-query = { path = "../kind-query" }
|
||||
kind-pass = { path = "../kind-pass" }
|
||||
|
||||
kind-target-hvm = { path = "../kind-target-hvm" }
|
||||
kind-target-kdl = { path = "../kind-target-kdl" }
|
||||
|
||||
pretty_assertions = "1.3.0"
|
||||
ntest = "0.8.1"
|
||||
walkdir = "2"
|
||||
walkdir = "2"
|
212
crates/kind-tests/benches/pure.rs
Normal file
212
crates/kind-tests/benches/pure.rs
Normal file
@ -0,0 +1,212 @@
|
||||
#![feature(test)]
|
||||
|
||||
extern crate test;
|
||||
use std::{fs, path::{PathBuf, Path}};
|
||||
|
||||
use driver::{resolution};
|
||||
use kind_driver::session::Session;
|
||||
use kind_pass::{expand::{self, uses::expand_uses}, desugar, erasure};
|
||||
use kind_tree::concrete;
|
||||
use test::Bencher;
|
||||
|
||||
use kind_checker as checker;
|
||||
use kind_driver as driver;
|
||||
|
||||
fn new_session() -> Session {
|
||||
let (rx, _) = std::sync::mpsc::channel();
|
||||
|
||||
let root = PathBuf::from("./suite/lib").canonicalize().unwrap();
|
||||
|
||||
Session::new(root, rx)
|
||||
}
|
||||
|
||||
fn get_book(session: &mut Session, path: &str) -> Result<concrete::Book, String> {
|
||||
let path = PathBuf::from(path);
|
||||
|
||||
match resolution::parse_and_store_book(session, &path) {
|
||||
Some(res) => Ok(res),
|
||||
None => Err("Cannot parse".to_string())
|
||||
}
|
||||
}
|
||||
|
||||
fn exp_paths() -> Vec<&'static str> {
|
||||
vec![
|
||||
"./suite/eval/Getters.kind2",
|
||||
"./suite/eval/Setters.kind2",
|
||||
"./suite/eval/DoNotation.kind2",
|
||||
"./suite/eval/User.kind2",
|
||||
]
|
||||
}
|
||||
|
||||
#[bench]
|
||||
fn bench_exp_pure_parsing(b: &mut Bencher) {
|
||||
|
||||
let paths = exp_paths();
|
||||
let paths: Vec<_> = paths.iter().map(|x| fs::read_to_string(x).unwrap()).collect();
|
||||
|
||||
b.iter(|| {
|
||||
paths.iter().map(|input| {
|
||||
let session = new_session();
|
||||
kind_parser::parse_book(session.diagnostic_sender.clone(), 0, &input)
|
||||
}).fold(0, |n, _| n + 1)
|
||||
})
|
||||
}
|
||||
|
||||
#[bench]
|
||||
fn bench_exp_pure_use_expansion(b: &mut Bencher) {
|
||||
|
||||
let paths = exp_paths();
|
||||
|
||||
let mut paths: Vec<_> = paths.iter().map(|x| {
|
||||
let input = fs::read_to_string(x).unwrap();
|
||||
let (rx, _) = std::sync::mpsc::channel();
|
||||
let (modu, failed) = kind_parser::parse_book(rx, 0, &input);
|
||||
assert!(!failed);
|
||||
modu
|
||||
}).collect();
|
||||
|
||||
b.iter(|| {
|
||||
paths.iter_mut().map(|module| {
|
||||
let (rx, _) = std::sync::mpsc::channel();
|
||||
expand_uses(module, rx);
|
||||
}).fold(0, |n, _| n + 1)
|
||||
})
|
||||
}
|
||||
|
||||
#[bench]
|
||||
fn bench_exp_pure_derive_expansion(b: &mut Bencher) {
|
||||
|
||||
let paths = exp_paths();
|
||||
|
||||
let mut books: Vec<_> = paths.iter().map(|x| {
|
||||
let input = fs::read_to_string(x).unwrap();
|
||||
let (rx, _) = std::sync::mpsc::channel();
|
||||
let (mut module, failed) = kind_parser::parse_book(rx.clone(), 0, &input);
|
||||
assert!(!failed);
|
||||
expand_uses(&mut module, rx);
|
||||
module
|
||||
}).collect();
|
||||
|
||||
b.iter(|| {
|
||||
books.iter_mut().map(|module| {
|
||||
let (rx, tx) = std::sync::mpsc::channel();
|
||||
expand::expand_module(rx, module);
|
||||
assert!(tx.iter().collect::<Vec<_>>().is_empty())
|
||||
}).fold(0, |n, _| n + 1)
|
||||
})
|
||||
}
|
||||
|
||||
#[bench]
|
||||
fn bench_exp_pure_check_unbound(b: &mut Bencher) {
|
||||
|
||||
let paths = exp_paths();
|
||||
let mut books: Vec<_> = paths.iter().map(|x| {
|
||||
let mut session = new_session();
|
||||
let book = resolution::parse_and_store_book(&mut session, &PathBuf::from(x)).unwrap();
|
||||
(session, book)
|
||||
}).collect();
|
||||
|
||||
b.iter(|| {
|
||||
books.iter_mut().map(|(session, book)| {
|
||||
let failed = resolution::check_unbound_top_level(session, book);
|
||||
assert!(!failed)
|
||||
}).fold(0, |n, _| n + 1)
|
||||
})
|
||||
}
|
||||
|
||||
#[bench]
|
||||
fn bench_exp_pure_desugar(b: &mut Bencher) {
|
||||
|
||||
let paths = exp_paths();
|
||||
let mut books: Vec<_> = paths.iter().map(|x| {
|
||||
let mut session = new_session();
|
||||
let mut book = resolution::parse_and_store_book(&mut session, &PathBuf::from(x)).unwrap();
|
||||
let failed = resolution::check_unbound_top_level(&mut session, &mut book);
|
||||
assert!(!failed);
|
||||
(session, book)
|
||||
}).collect();
|
||||
|
||||
b.iter(|| {
|
||||
books.iter_mut().map(|(session, book)| {
|
||||
desugar::desugar_book(session.diagnostic_sender.clone(), &book).unwrap()
|
||||
}).fold(0, |n, _| n + 1)
|
||||
})
|
||||
}
|
||||
|
||||
#[bench]
|
||||
fn bench_exp_pure_erase(b: &mut Bencher) {
|
||||
|
||||
let paths = exp_paths();
|
||||
|
||||
let books: Vec<_> = paths.iter().map(|x| {
|
||||
let mut session = new_session();
|
||||
let mut book = resolution::parse_and_store_book(&mut session, &PathBuf::from(x)).unwrap();
|
||||
let failed = resolution::check_unbound_top_level(&mut session, &mut book);
|
||||
let book = desugar::desugar_book(session.diagnostic_sender.clone(), &book).unwrap();
|
||||
assert!(!failed);
|
||||
|
||||
(session, book)
|
||||
}).collect();
|
||||
|
||||
b.iter(|| {
|
||||
books.iter().map(|(session, book)| {
|
||||
erasure::erase_book(
|
||||
book,
|
||||
session.diagnostic_sender.clone(),
|
||||
vec!["Main".to_string()],
|
||||
).unwrap();
|
||||
}).fold(0, |n, _| n + 1)
|
||||
})
|
||||
}
|
||||
|
||||
#[bench]
|
||||
fn bench_exp_pure_to_hvm(b: &mut Bencher) {
|
||||
|
||||
let paths = exp_paths();
|
||||
|
||||
let books: Vec<_> = paths.iter().map(|x| {
|
||||
let mut session = new_session();
|
||||
let mut book = resolution::parse_and_store_book(&mut session, &PathBuf::from(x)).unwrap();
|
||||
let failed = resolution::check_unbound_top_level(&mut session, &mut book);
|
||||
let book = desugar::desugar_book(session.diagnostic_sender.clone(), &book).unwrap();
|
||||
assert!(!failed);
|
||||
|
||||
let book = erasure::erase_book(
|
||||
&book,
|
||||
session.diagnostic_sender.clone(),
|
||||
vec!["Main".to_string()],
|
||||
).unwrap();
|
||||
|
||||
(session, book)
|
||||
}).collect();
|
||||
|
||||
b.iter(move || {
|
||||
books.iter().map(move |(_, book)| {
|
||||
kind_target_hvm::compile_book(book.to_owned(), false)
|
||||
}).fold(0, |n, _| n + 1)
|
||||
})
|
||||
}
|
||||
|
||||
|
||||
#[bench]
|
||||
fn bench_exp_pure_check_without_the_checker(b: &mut Bencher) {
|
||||
let mut paths = exp_paths();
|
||||
|
||||
let books: Vec<_> = paths.iter().map(|x| {
|
||||
let mut session = new_session();
|
||||
let mut book = resolution::parse_and_store_book(&mut session, &PathBuf::from(x)).unwrap();
|
||||
let failed = resolution::check_unbound_top_level(&mut session, &mut book);
|
||||
let book = desugar::desugar_book(session.diagnostic_sender.clone(), &book).unwrap();
|
||||
assert!(!failed);
|
||||
|
||||
(session, book)
|
||||
}).collect();
|
||||
|
||||
b.iter(move || {
|
||||
books.iter().map(move |(session, book)| {
|
||||
let all = book.entrs.iter().map(|x| x.0).cloned().collect();
|
||||
let succeeded = checker::type_check(book, session.diagnostic_sender.clone(), all);
|
||||
assert!(succeeded)
|
||||
}).fold(0, |n, _| n + 1)
|
||||
})
|
||||
}
|
44
crates/kind-tests/suite/checker/Algebra.kind2
Normal file
44
crates/kind-tests/suite/checker/Algebra.kind2
Normal file
@ -0,0 +1,44 @@
|
||||
#derive[match]
|
||||
type Algebra.Laws.Inverse <t> <concat: (t -> t -> t)> <inverse: (t -> t)> <empty: t> {
|
||||
new (left_inverse: ((x : t) -> (Equal empty (concat x (inverse x))))) (right_inverse: ((x : t) -> (Equal empty (concat (inverse x) x))))
|
||||
}
|
||||
|
||||
type Algebra.Magma <t: Type> {
|
||||
new (concat: (t -> t -> t))
|
||||
}
|
||||
|
||||
type Algebra.Semigroup <t: Type> {
|
||||
new (magma: (Algebra.Magma t)) (associativity: (Algebra.Laws.associativity.eta (Algebra.Magma.concat magma)))
|
||||
}
|
||||
|
||||
Algebra.Group.concat <t> (group: (Algebra.Group t)) : (t -> t -> t)
|
||||
Algebra.Group.concat t (Algebra.Group.new t_ monoid inverse inverse_proof) = (Algebra.Monoid.concat monoid)
|
||||
|
||||
Algebra.Laws.associativity.eta <t> (concat: (t -> t -> t)) : Type
|
||||
Algebra.Laws.associativity.eta t concat = ((a : t) -> (b : t) -> (c : t) -> (Equal (concat (concat a b) c) (concat a (concat b c))))
|
||||
|
||||
type Algebra.Laws.Identity <t> <concat: (t -> t -> t)> <empty: t> {
|
||||
new (left_identity: ((x : t) -> (Equal x (concat empty x)))) (right_identity: ((x : t) -> (Equal x (concat x empty))))
|
||||
}
|
||||
|
||||
Algebra.Monoid.empty <t> (monoid: (Algebra.Monoid t)) : t
|
||||
Algebra.Monoid.empty t (Algebra.Monoid.new t_ sg empty id) = empty
|
||||
|
||||
type Algebra.Monoid <t: Type> {
|
||||
new (sg: (Algebra.Semigroup t)) (empty: t) (identity: (Algebra.Laws.Identity t (Algebra.Semigroup.concat sg) empty))
|
||||
}
|
||||
|
||||
Algebra.Semigroup.concat <t> (semigroup: (Algebra.Semigroup t)) : (t -> t -> t)
|
||||
Algebra.Semigroup.concat t (Algebra.Semigroup.new t_ magma assoc) = (Algebra.Magma.concat magma)
|
||||
|
||||
Algebra.Monoid.concat <t> (monoid: (Algebra.Monoid t)) : (t -> t -> t)
|
||||
Algebra.Monoid.concat t (Algebra.Monoid.new t_ sg empty id) = (Algebra.Semigroup.concat sg)
|
||||
|
||||
Algebra.Magma.concat <t> (magma: (Algebra.Magma t)) : (t -> t -> t)
|
||||
Algebra.Magma.concat t (Algebra.Magma.new t_ concat) = concat
|
||||
|
||||
Equal <t> (a: t) (b: t) : Type
|
||||
|
||||
type Algebra.Group <t> {
|
||||
new (monoid: (Algebra.Monoid t)) (invert: (t -> t)) (inverse: (Algebra.Laws.Inverse t (Algebra.Monoid.concat monoid) invert (Algebra.Monoid.empty monoid)))
|
||||
}
|
1648
crates/kind-tests/suite/checker/Checker.kind2
Normal file
1648
crates/kind-tests/suite/checker/Checker.kind2
Normal file
File diff suppressed because it is too large
Load Diff
@ -3,7 +3,7 @@
|
||||
* Expected: U60
|
||||
|
||||
|
||||
/--[tests/suite/checker/derive/Inspection.kind2:3:3]
|
||||
/--[suite/checker/Inspection.kind2:3:3]
|
||||
|
|
||||
2 | Main =
|
||||
3 | ?
|
1
crates/kind-tests/suite/checker/derive/User.golden
Normal file
1
crates/kind-tests/suite/checker/derive/User.golden
Normal file
@ -0,0 +1 @@
|
||||
Ok!
|
1
crates/kind-tests/suite/checker/derive/Vec.golden
Normal file
1
crates/kind-tests/suite/checker/derive/Vec.golden
Normal file
@ -0,0 +1 @@
|
||||
Ok!
|
@ -1,6 +1,6 @@
|
||||
ERROR The case is not covering all the values inside of it!
|
||||
|
||||
/--[tests/suite/checker/derive/fail/IncompleteCase.kind2:12:9]
|
||||
/--[suite/checker/derive/fail/IncompleteCase.kind2:12:9]
|
||||
|
|
||||
11 | let User.new (ttt = e) e .. = User.new 2 4 1
|
||||
12 | let User.new (ttt = f) name = User.new 6 7 3
|
@ -1,6 +1,6 @@
|
||||
ERROR Repeated named variable
|
||||
|
||||
/--[tests/suite/checker/derive/fail/Repeated.kind2:12:19]
|
||||
/--[suite/checker/derive/fail/Repeated.kind2:12:19]
|
||||
|
|
||||
11 | let User.new (ttt = e) e .. = User.new 2 4 1
|
||||
12 | let User.new (ttt = f) ttt = User.new 6 7 3
|
||||
@ -12,7 +12,7 @@
|
||||
|
||||
ERROR The case is not covering all the values inside of it!
|
||||
|
||||
/--[tests/suite/checker/derive/fail/Repeated.kind2:12:9]
|
||||
/--[suite/checker/derive/fail/Repeated.kind2:12:9]
|
||||
|
|
||||
11 | let User.new (ttt = e) e .. = User.new 2 4 1
|
||||
12 | let User.new (ttt = f) ttt = User.new 6 7 3
|
@ -1,6 +1,6 @@
|
||||
ERROR Defined multiple times for the same name
|
||||
|
||||
/--[tests/suite/checker/derive/fail/RepeatedDef.kind2:2:5]
|
||||
/--[suite/checker/derive/fail/RepeatedDef.kind2:2:5]
|
||||
|
|
||||
1 | type Nat {
|
||||
2 | zero
|
@ -4,7 +4,7 @@
|
||||
* Expected : (Eq _ 123u120 124u120)
|
||||
|
||||
|
||||
/--[tests/suite/checker/derive/fail/WrongU120Eq.kind2:12:9]
|
||||
/--[suite/checker/derive/fail/WrongU120Eq.kind2:12:9]
|
||||
|
|
||||
11 | Teste : Eq 123u120 124u120
|
||||
12 | Teste = Eq.rfl
|
21
crates/kind-tests/suite/checker/fail/MismatchOne.golden
Normal file
21
crates/kind-tests/suite/checker/fail/MismatchOne.golden
Normal file
@ -0,0 +1,21 @@
|
||||
ERROR Type mismatch
|
||||
|
||||
* Got : ((x_1 : Type) -> (x_2 : Type) -> Type)
|
||||
* Expected : ((x_1 : t) -> (x_2 : t) -> t)
|
||||
|
||||
* Context:
|
||||
* t : Type
|
||||
* t_ : Type
|
||||
* t_ = t
|
||||
* magma : (Algebra.Magma Type)
|
||||
* assoc : ((a : _) -> (b : _) -> (c : _) -> (Equal _ (((Algebra.Magma.concat _ magma) (((Algebra.Magma.concat _ magma) a) b)) c) (((Algebra.Magma.concat _ magma) a) (((Algebra.Magma.concat _ magma) b) c))))
|
||||
|
||||
/--[suite/checker/fail/MismatchOne.kind2:32:69]
|
||||
|
|
||||
31 | Algebra.Semigroup.concat <t> (semigroup: (Algebra.Semigroup t)) : (t -> t -> t)
|
||||
32 | Algebra.Semigroup.concat t (Algebra.Semigroup.new t_ magma assoc) = (Algebra.Magma.concat magma)
|
||||
| v---------------------------
|
||||
| \Here!
|
||||
33 |
|
||||
|
||||
|
44
crates/kind-tests/suite/checker/fail/MismatchOne.kind2
Normal file
44
crates/kind-tests/suite/checker/fail/MismatchOne.kind2
Normal file
@ -0,0 +1,44 @@
|
||||
#derive[match]
|
||||
type Algebra.Laws.Inverse <t> <concat: (t -> t -> t)> <inverse: (t -> t)> <empty: t> {
|
||||
new (left_inverse: ((x : t) -> (Equal empty (concat x (inverse x))))) (right_inverse: ((x : t) -> (Equal empty (concat (inverse x) x))))
|
||||
}
|
||||
|
||||
type Algebra.Magma <t: Type> {
|
||||
new (concat: (t -> t -> t))
|
||||
}
|
||||
|
||||
type Algebra.Semigroup <t: Type> {
|
||||
new (magma: (Algebra.Magma Type)) (associativity: (Algebra.Laws.associativity.eta (Algebra.Magma.concat magma)))
|
||||
}
|
||||
|
||||
Algebra.Group.concat <t> (group: (Algebra.Group t)) : (t -> t -> t)
|
||||
Algebra.Group.concat t (Algebra.Group.new t_ monoid inverse inverse_proof) = (Algebra.Monoid.concat monoid)
|
||||
|
||||
Algebra.Laws.associativity.eta <t> (concat: (t -> t -> t)) : Type
|
||||
Algebra.Laws.associativity.eta t concat = ((a : t) -> (b : t) -> (c : t) -> (Equal (concat (concat a b) c) (concat a (concat b c))))
|
||||
|
||||
type Algebra.Laws.Identity <t> <concat: (t -> t -> t)> <empty: t> {
|
||||
new (left_identity: ((x : t) -> (Equal x (concat empty x)))) (right_identity: ((x : t) -> (Equal x (concat x empty))))
|
||||
}
|
||||
|
||||
Algebra.Monoid.empty <t> (monoid: (Algebra.Monoid t)) : t
|
||||
Algebra.Monoid.empty t (Algebra.Monoid.new t_ sg empty id) = empty
|
||||
|
||||
type Algebra.Monoid <t: Type> {
|
||||
new (sg: (Algebra.Semigroup t)) (empty: t) (identity: (Algebra.Laws.Identity t (Algebra.Semigroup.concat sg) empty))
|
||||
}
|
||||
|
||||
Algebra.Semigroup.concat <t> (semigroup: (Algebra.Semigroup t)) : (t -> t -> t)
|
||||
Algebra.Semigroup.concat t (Algebra.Semigroup.new t_ magma assoc) = (Algebra.Magma.concat magma)
|
||||
|
||||
Algebra.Monoid.concat <t> (monoid: (Algebra.Monoid t)) : (t -> t -> t)
|
||||
Algebra.Monoid.concat t (Algebra.Monoid.new t_ sg empty id) = (Algebra.Semigroup.concat sg)
|
||||
|
||||
Algebra.Magma.concat <t> (magma: (Algebra.Magma t)) : (t -> t -> t)
|
||||
Algebra.Magma.concat t (Algebra.Magma.new t_ concat) = concat
|
||||
|
||||
Equal <t> (a: t) (b: t) : Type
|
||||
|
||||
type Algebra.Group <t> {
|
||||
new (monoid: (Algebra.Monoid t)) (invert: (t -> t)) (inverse: (Algebra.Laws.Inverse t (Algebra.Monoid.concat monoid) invert (Algebra.Monoid.empty monoid)))
|
||||
}
|
16
crates/kind-tests/suite/checker/fail/MismatchTwo.golden
Normal file
16
crates/kind-tests/suite/checker/fail/MismatchTwo.golden
Normal file
@ -0,0 +1,16 @@
|
||||
ERROR Type mismatch
|
||||
|
||||
* Got : Type
|
||||
* Expected : U60
|
||||
|
||||
* Context:
|
||||
* a : U60
|
||||
|
||||
/--[suite/checker/fail/MismatchTwo.kind2:2:10]
|
||||
|
|
||||
1 | Main (a: U60): U60
|
||||
2 | Main a = Type
|
||||
| v---
|
||||
| \Here!
|
||||
|
||||
|
2
crates/kind-tests/suite/checker/fail/MismatchTwo.kind2
Normal file
2
crates/kind-tests/suite/checker/fail/MismatchTwo.kind2
Normal file
@ -0,0 +1,2 @@
|
||||
Main (a: U60): U60
|
||||
Main a = Type
|
@ -1,6 +1,6 @@
|
||||
ERROR Required functions are not implemented for this type.
|
||||
|
||||
/--[tests/suite/eval/NoMatch.kind2:3:5]
|
||||
/--[suite/eval/NoMatch.kind2:3:5]
|
||||
|
|
||||
| /
|
||||
3 | | match NoMatch NoMatch.pudding {
|
0
crates/kind-tests/suite/kdl/Shortener.golden
Normal file
0
crates/kind-tests/suite/kdl/Shortener.golden
Normal file
@ -37,11 +37,11 @@ fn test_kind2(path: &Path, run: fn(&Path) -> String) -> Result<(), Error> {
|
||||
}
|
||||
|
||||
#[test]
|
||||
#[timeout(15000)]
|
||||
#[timeout(30000)]
|
||||
fn test_checker() -> Result<(), Error> {
|
||||
test_kind2(Path::new("./tests/suite/checker"), |path| {
|
||||
test_kind2(Path::new("./suite/checker"), |path| {
|
||||
let (rx, tx) = std::sync::mpsc::channel();
|
||||
let root = PathBuf::from("./tests/suite/lib").canonicalize().unwrap();
|
||||
let root = PathBuf::from("./suite/lib").canonicalize().unwrap();
|
||||
let mut session = Session::new(root, rx);
|
||||
|
||||
let entrypoints = vec!["Main".to_string()];
|
||||
@ -71,9 +71,9 @@ fn test_checker() -> Result<(), Error> {
|
||||
#[test]
|
||||
#[timeout(15000)]
|
||||
fn test_eval() -> Result<(), Error> {
|
||||
test_kind2(Path::new("./tests/suite/eval"), |path| {
|
||||
test_kind2(Path::new("./suite/eval"), |path| {
|
||||
let (rx, tx) = std::sync::mpsc::channel();
|
||||
let root = PathBuf::from("./tests/suite/lib").canonicalize().unwrap();
|
||||
let root = PathBuf::from("./suite/lib").canonicalize().unwrap();
|
||||
let mut session = Session::new(root, rx);
|
||||
|
||||
let entrypoints = vec!["Main".to_string()];
|
||||
@ -107,9 +107,9 @@ fn test_eval() -> Result<(), Error> {
|
||||
#[test]
|
||||
#[timeout(15000)]
|
||||
fn test_kdl() -> Result<(), Error> {
|
||||
test_kind2(Path::new("./tests/suite/kdl"), |path| {
|
||||
test_kind2(Path::new("./suite/kdl"), |path| {
|
||||
let (rx, tx) = std::sync::mpsc::channel();
|
||||
let root = PathBuf::from("./tests/suite/lib").canonicalize().unwrap();
|
||||
let root = PathBuf::from("./suite/lib").canonicalize().unwrap();
|
||||
let mut session = Session::new(root, rx);
|
||||
|
||||
let entrypoints = vec!["Main".to_string()];
|
||||
@ -123,7 +123,7 @@ fn test_kdl() -> Result<(), Error> {
|
||||
match check {
|
||||
Some(file) if diagnostics.is_empty() => {
|
||||
file.to_string()
|
||||
}
|
||||
},
|
||||
_ => {
|
||||
let mut res_string = String::new();
|
||||
|
||||
|
@ -1,11 +0,0 @@
|
||||
ERROR Unexpected token ':'.
|
||||
|
||||
/--[tests/suite/checker/derive/Algebra.kind2:1:69]
|
||||
|
|
||||
1 | Algebra.Group.new <t: Type> (monoid: (Algebra.Monoid t)) (invert: (_: t) t) (inverse: (Algebra.Laws.Inverse t (Algebra.Monoid.concat _ monoid) invert (Algebra.Monoid.empty _ monoid))) : (Algebra.Group t)
|
||||
| v
|
||||
| \Here!
|
||||
2 |
|
||||
3 | Algebra.Group (t: Type) : Type
|
||||
|
||||
|
@ -1,41 +0,0 @@
|
||||
Algebra.Group.new <t: Type> (monoid: (Algebra.Monoid t)) (invert: (_: t) t) (inverse: (Algebra.Laws.Inverse t (Algebra.Monoid.concat _ monoid) invert (Algebra.Monoid.empty _ monoid))) : (Algebra.Group t)
|
||||
|
||||
Algebra.Group (t: Type) : Type
|
||||
|
||||
Algebra.Monoid.concat <t: Type> (monoid: (Algebra.Monoid t)) : (_: t) (_: t) t
|
||||
Algebra.Monoid.concat t (Algebra.Monoid.new t_ sg empty id) = (Algebra.Semigroup.concat _ sg)
|
||||
|
||||
|
||||
Algebra.Monoid.new <t: Type> (sg: (Algebra.Semigroup t)) (empty: t) (identity: (Algebra.Laws.Identity t (Algebra.Semigroup.concat _ sg) empty)) : (Algebra.Monoid t)
|
||||
|
||||
Algebra.Semigroup (t: Type) : Type
|
||||
|
||||
Algebra.Laws.Identity (t: Type) (concat: (_: t) (_: t) t) (empty: t) : Type
|
||||
|
||||
Algebra.Monoid (t: Type) : Type
|
||||
|
||||
Algebra.Semigroup.concat <t: Type> (semigroup: (Algebra.Semigroup t)) : (_: t) (_: t) t
|
||||
Algebra.Semigroup.concat t (Algebra.Semigroup.new t_ magma assoc) = (Algebra.Magma.concat _ magma)
|
||||
|
||||
|
||||
Algebra.Semigroup.new <t: Type> (magma: (Algebra.Magma t)) (associativity: (Algebra.Laws.associativity.eta _ (Algebra.Magma.concat _ magma))) : (Algebra.Semigroup t)
|
||||
|
||||
Algebra.Magma (t: Type) : Type
|
||||
|
||||
Algebra.Laws.associativity.eta <t: Type> (concat: (_: t) (_: t) t) : Type
|
||||
Algebra.Laws.associativity.eta t concat = (a: t) (b: t) (c: t) (Equal _ (concat (concat a b) c) (concat a (concat b c)))
|
||||
|
||||
|
||||
Equal <t: Type> (a: t) (b: t) : Type
|
||||
|
||||
Algebra.Magma.concat <t: Type> (magma: (Algebra.Magma t)) : (_: t) (_: t) t
|
||||
Algebra.Magma.concat t (Algebra.Magma.new t_ concat) = concat
|
||||
|
||||
|
||||
Algebra.Magma.new <t: Type> (concat: (_: t) (_: t) t) : (Algebra.Magma t)
|
||||
|
||||
Algebra.Monoid.empty <t: Type> (monoid: (Algebra.Monoid t)) : t
|
||||
Algebra.Monoid.empty t (Algebra.Monoid.new t_ sg empty id) = empty
|
||||
|
||||
|
||||
Algebra.Laws.Inverse (t: Type) (concat: (_: t) (_: t) t) (inverse: (_: t) t) (empty: t) : Type
|
@ -353,11 +353,10 @@ impl Display for SttmKind {
|
||||
write!(f, "{};\n{}", expr, next)
|
||||
}
|
||||
SttmKind::Return(ret) => {
|
||||
write!(f, "return {}\n", ret)
|
||||
writeln!(f, "return {}", ret)
|
||||
}
|
||||
|
||||
SttmKind::RetExpr(ret) => {
|
||||
write!(f, "{}\n", ret)
|
||||
writeln!(f, "{}", ret)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -174,14 +174,14 @@ impl Expr {
|
||||
|
||||
pub fn fun(range: Range, name: QualifiedIdent, args: Vec<Box<Expr>>) -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
range: range.into(),
|
||||
range,
|
||||
data: ExprKind::Fun { name, args },
|
||||
})
|
||||
}
|
||||
|
||||
pub fn ctr(range: Range, name: QualifiedIdent, args: Vec<Box<Expr>>) -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
range: range.into(),
|
||||
range,
|
||||
data: ExprKind::Ctr { name, args },
|
||||
})
|
||||
}
|
||||
|
@ -103,21 +103,21 @@ impl Expr {
|
||||
|
||||
pub fn fun(range: Range, name: QualifiedIdent, args: Vec<Box<Expr>>) -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
range: range.into(),
|
||||
range,
|
||||
data: ExprKind::Fun { name, args },
|
||||
})
|
||||
}
|
||||
|
||||
pub fn app(range: Range, fun: Box<Expr>, args: Vec<Box<Expr>>) -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
range: range.into(),
|
||||
range,
|
||||
data: ExprKind::App { fun, args },
|
||||
})
|
||||
}
|
||||
|
||||
pub fn ctr(range: Range, name: QualifiedIdent, args: Vec<Box<Expr>>) -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
range: range.into(),
|
||||
range,
|
||||
data: ExprKind::Ctr { name, args },
|
||||
})
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user