Kindelia/Kind2
1
1
Fork 0
mirror of https://github.com/Kindelia/Kind2.git synced 2024-07-14 18:40:27 +03:00
Code Issues Projects Releases Wiki Activity

style: Apply some clippy and fmt suggestions

Browse Source
This commit is contained in:
Nicolas Abril 2023-05-09 17:45:33 +02:00
parent 16d062e73a
commit f1979a2021
21 changed files with 397 additions and 287 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
crates/kind-checker/src/compiler/mod.rs
View File

@ -587,7 +587,7 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) {
"Kind.Axiom.Family.Constructors".to_owned(),
vec![mk_ctr_name(&family.name)],
),
rhs: mk_ctr("Maybe.some".to_string(), vec![codegen_vec(family.constructors.iter().map(|x| mk_ctr_name(x)))]),
rhs: mk_ctr("Maybe.some".to_string(), vec![codegen_vec(family.constructors.iter().map(mk_ctr_name))]),
});
file.rules.push(lang::Rule {
@ -643,7 +643,7 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) {
lhs: mk_ctr(
"Kind.Coverage.Maker.Mk".to_owned(),
vec![
mk_ctr_name(&constructor),
mk_ctr_name(constructor),
mk_var("orig"),
mk_lifted_ctr(
eval_ctr(true, TermTag::Ctr(args.len())),
@ -661,7 +661,7 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) {
file.rules.push(lang::Rule {
lhs: mk_ctr(
"Kind.Axiom.Compare".to_owned(),
vec![mk_ctr_name(&constructor), mk_ctr_name(&constructor)],
vec![mk_ctr_name(constructor), mk_ctr_name(constructor)],
),
rhs: mk_single_ctr("Bool.true".to_string()),
});
@ -669,7 +669,7 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) {
file.rules.push(lang::Rule {
lhs: mk_ctr(
"Kind.Axiom.ArgsCount".to_owned(),
vec![mk_ctr_name(&constructor)],
vec![mk_ctr_name(constructor)],
),
rhs: mk_u60(entry.args.len() as u64),
});
@ -677,7 +677,7 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) {
file.rules.push(lang::Rule {
lhs: mk_ctr(
"Kind.Axiom.Compare".to_owned(),
vec![mk_ctr_name(&constructor), mk_ctr_name(&constructor)],
vec![mk_ctr_name(constructor), mk_ctr_name(constructor)],
),
rhs: mk_single_ctr("Bool.true".to_string()),
});

8
crates/kind-derive/src/matching.rs
View File

@ -24,7 +24,9 @@ pub fn to_app_binding(errs: &mut Errs, binding: &Binding) -> AppBinding {
data: expr.clone(),
},
Binding::Named(_, name, expr) => {
errs.push(Box::new(DeriveDiagnostic::CannotUseNamedVariable(name.range)));
errs.push(Box::new(DeriveDiagnostic::CannotUseNamedVariable(
name.range,
)));
AppBinding::explicit(expr.clone())
}
}
@ -195,7 +197,7 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> (concrete::Entry, Errs)
let scrutinee_ident = Expr::var(Ident::generate("scrutinee"));
let mut return_args = indice_names.clone();
let mut return_args = indice_names;
return_args.push(AppBinding::explicit(scrutinee_ident));
let return_type = Expr::app(Expr::var(motive_ident.clone()), return_args, range);
@ -329,7 +331,7 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> (concrete::Entry, Errs)
rules,
range,
attrs: Vec::new(),
generated_by: Some(sum.name.to_string().clone()),
generated_by: Some(sum.name.to_string()),
};
(entry, errs)

20
crates/kind-derive/src/mutters.rs
View File

@ -6,7 +6,7 @@ use kind_tree::concrete::expr::Expr;
use kind_tree::concrete::pat::{Pat, PatIdent};
use kind_tree::concrete::*;
use kind_tree::concrete::{self};
use kind_tree::symbol::{Ident};
use kind_tree::symbol::Ident;
use kind_tree::telescope::Telescope;
pub fn derive_mutters(range: Range, rec: &RecordDecl) -> Vec<concrete::Entry> {
@ -27,7 +27,7 @@ pub fn derive_mutters(range: Range, rec: &RecordDecl) -> Vec<concrete::Entry> {
.cloned()
.map(|x| Binding::Positional(Expr::var(x.name)))
.collect(),
range
range,
);
// Sccrutinzies
@ -56,7 +56,7 @@ pub fn derive_mutters(range: Range, rec: &RecordDecl) -> Vec<concrete::Entry> {
.map(|arg| {
(
arg.name.clone(),
arg.typ.clone().unwrap_or_else(|| Expr::typ(arg.range.clone())),
arg.typ.clone().unwrap_or_else(|| Expr::typ(arg.range)),
)
})
.collect();
@ -90,7 +90,13 @@ pub fn derive_mutters(range: Range, rec: &RecordDecl) -> Vec<concrete::Entry> {
hidden: false,
erased: false,
name: Ident::generate("mut"),
typ: Some(Expr::all(Ident::generate("_"), cons_typ.clone(), cons_typ.clone(), false, range)),
typ: Some(Expr::all(
Ident::generate("_"),
cons_typ.clone(),
cons_typ.clone(),
false,
range,
)),
range,
});
@ -109,7 +115,11 @@ pub fn derive_mutters(range: Range, rec: &RecordDecl) -> Vec<concrete::Entry> {
.map(|x| Binding::Positional(Expr::var(x.0)))
.collect();
args[place] = Binding::Positional(Expr::app(Expr::var(new_var), vec![args[place].to_app_binding()], range));
args[place] = Binding::Positional(Expr::app(
Expr::var(new_var),
vec![args[place].to_app_binding()],
range,
));
let body = Box::new(Expr {
data: ExprKind::Constr {

2
crates/kind-derive/src/setters.rs
View File

@ -83,7 +83,7 @@ pub fn derive_setters(range: Range, rec: &RecordDecl) -> Vec<concrete::Entry> {
.map(|arg| {
(
arg.name.clone(),
arg.typ.clone().unwrap_or_else(|| typ(arg.range.clone())),
arg.typ.clone().unwrap_or_else(|| typ(arg.range)),
)
})
.collect();

13
crates/kind-pass/src/desugar/destruct.rs
View File

@ -199,7 +199,10 @@ impl<'a> DesugarState<'a> {
};
if let Some((range, _, _)) = cases_args[index] {
self.send_err(PassDiagnostic::DuplicatedNamed(range, case.constructor.range));
self.send_err(PassDiagnostic::DuplicatedNamed(
range,
case.constructor.range,
));
} else {
let sum_constructor = &constructors[index];
@ -220,7 +223,8 @@ impl<'a> DesugarState<'a> {
if let Some((_, name)) = arg.1 {
arguments.push(name)
} else {
let mut id = Ident::generate(&format!("{}.{}", matcher.scrutinee.to_str(), arg.0));
let mut id =
Ident::generate(&format!("{}.{}", matcher.scrutinee.to_str(), arg.0));
id.range = case.constructor.range;
arguments.push(id);
}
@ -267,7 +271,7 @@ impl<'a> DesugarState<'a> {
self.gen_hole_expr(matcher.typ.range)
};
let desugared_value = matcher.value.as_ref().map(|f| self.desugar_expr(&f));
let desugared_value = matcher.value.as_ref().map(|f| self.desugar_expr(f));
let irrelev = matcher.with_vars.iter().map(|_| false).collect::<Vec<_>>();
@ -277,7 +281,8 @@ impl<'a> DesugarState<'a> {
.map(|x| {
(
x.0.clone(),
x.1.clone().map(|x| self.desugar_expr(&x))
x.1.clone()
.map(|x| self.desugar_expr(&x))
.unwrap_or_else(|| self.gen_hole_expr(range)),
)
})

53
crates/kind-pass/src/desugar/expr.rs
View File

@ -87,27 +87,33 @@ impl<'a> DesugarState<'a> {
self.desugar_record_field_sequence(range, &mut value, typ, &sub.fields);
if self.failed {
return Expr::err(range)
return Expr::err(range);
}
match &sub.operation {
Set(expr) => {
let value_ident = Ident::generate("_value");
let expr = self.desugar_expr(&expr);
let expr = self.desugar_expr(expr);
let mut result = value.iter().rfold(expr, |acc, (typ, field)| {
let name = typ.add_segment(field.to_str()).add_segment("mut");
if self.failed || !self.check_implementation(name.to_str(), range, Sugar::Mutter(typ.to_string())) {
if self.failed
|| !self.check_implementation(
name.to_str(),
range,
Sugar::Mutter(typ.to_string()),
)
{
return desugared::Expr::err(range);
}
self.mk_desugared_ctr(
range,
name,
vec![
Expr::var(value_ident.clone()),
Expr::lambda(range.clone(), value_ident.clone(), acc, false),
Expr::lambda(range, value_ident.clone(), acc, false),
],
false,
)
@ -121,17 +127,23 @@ impl<'a> DesugarState<'a> {
}
Mut(expr) => {
let value_ident = Ident::generate("_value");
let expr = self.desugar_expr(&expr);
let expr = self.desugar_expr(expr);
let result = value.iter().rfold(expr, |acc, (typ, field)| {
let name = typ.add_segment(field.to_str()).add_segment("mut");
if self.failed || !self.check_implementation(name.to_str(), range, Sugar::Mutter(typ.to_string())) {
if self.failed
|| !self.check_implementation(
name.to_str(),
range,
Sugar::Mutter(typ.to_string()),
)
{
return desugared::Expr::err(range);
}
Expr::lambda(
name.range.clone(),
name.range,
value_ident.clone(),
self.mk_desugared_ctr(
range,
@ -144,23 +156,18 @@ impl<'a> DesugarState<'a> {
});
if self.failed {
return Expr::err(range)
return Expr::err(range);
}
let mut result = if let desugared::ExprKind::Lambda { body, .. } = result.data {
body
} else {
self.send_err(PassDiagnostic::NeedsAField(
sub.expr.range.clone()
));
return Expr::err(range)
self.send_err(PassDiagnostic::NeedsAField(sub.expr.range));
return Expr::err(range);
};
match &mut result.data {
desugared::ExprKind::Ctr { args, .. } => {
args[0] = self.desugar_expr(&sub.expr);
}
_ => (),
if let desugared::ExprKind::Ctr { args, .. } = &mut result.data {
args[0] = self.desugar_expr(&sub.expr);
}
result
@ -170,7 +177,13 @@ impl<'a> DesugarState<'a> {
.fold(self.desugar_expr(&sub.expr), |acc, (typ, field)| {
let name = typ.add_segment(field.to_str()).add_segment("get");
if self.failed || !self.check_implementation(name.to_str(), range, Sugar::Getter(typ.to_string())) {
if self.failed
|| !self.check_implementation(
name.to_str(),
range,
Sugar::Getter(typ.to_string()),
)
{
return desugared::Expr::err(range);
}
@ -487,7 +500,7 @@ impl<'a> DesugarState<'a> {
var_name,
motive,
next,
} => self.desugar_open(expr.range, type_name, var_name, motive, &next),
} => self.desugar_open(expr.range, type_name, var_name, motive, next),
SeqRecord(sec) => self.desugar_seq(expr.range, sec),
}
}

8
crates/kind-pass/src/desugar/record_field.rs
View File

@ -7,7 +7,7 @@ use kind_tree::{
telescope::Telescope,
};
use crate::{subst::subst_on_expr, diagnostic::PassDiagnostic};
use crate::{diagnostic::PassDiagnostic, subst::subst_on_expr};
use super::DesugarState;
@ -55,7 +55,7 @@ impl<'a> DesugarState<'a> {
return true;
}
if let Some((name, params, record_fields, args)) = self.specialize_on_field(typ.clone()) {
if let Some((name, params, record_fields, args)) = self.specialize_on_field(typ) {
if let Some(field) = record_fields
.iter()
.find(|x| x.name.to_str() == fields[0].to_str())
@ -82,13 +82,13 @@ impl<'a> DesugarState<'a> {
} else {
self.send_err(PassDiagnostic::CannotFindTheField(
fields[0].range,
fields[0].to_string()
fields[0].to_string(),
));
}
} else {
self.send_err(PassDiagnostic::CannotAccessType(
fields[0].range,
fields[0].to_string()
fields[0].to_string(),
));
}

19
crates/kind-pass/src/desugar/top_level.rs
View File

@ -76,7 +76,7 @@ impl<'a> DesugarState<'a> {
let mut family = Family {
name: sum_type.name.clone(),
constructors: Vec::with_capacity(sum_type.constructors.len()),
parameters: desugared_params.clone(),
parameters: desugared_params,
};
for cons in &sum_type.constructors {
@ -147,7 +147,9 @@ impl<'a> DesugarState<'a> {
.insert(cons_ident.to_string(), Box::new(data_constructor));
}
self.new_book.families.insert(sum_type.name.to_string(), family);
self.new_book
.families
.insert(sum_type.name.to_string(), family);
}
pub fn desugar_record_type(&mut self, rec_type: &concrete::RecordDecl) {
@ -180,11 +182,14 @@ impl<'a> DesugarState<'a> {
let cons_ident = rec_type.name.add_segment(rec_type.constructor.to_str());
self.new_book.families.insert(rec_type.name.to_string(), Family {
name: rec_type.name.clone(),
constructors: vec![cons_ident.clone()],
parameters: desugared_params.clone()
});
self.new_book.families.insert(
rec_type.name.to_string(),
Family {
name: rec_type.name.clone(),
constructors: vec![cons_ident.clone()],
parameters: desugared_params,
},
);
let fields_args = rec_type
.fields

46
crates/kind-pass/src/subst.rs
View File

@ -5,7 +5,11 @@ pub fn subst_on_expr(expr: &mut Expr, substs: FxHashMap<String, Box<Expr>>) {
subst(Default::default(), expr, &substs)
}
fn subst(bindings: im_rc::HashSet<String>, expr: &mut Expr, substs: &FxHashMap<String, Box<Expr>>) {
fn subst(
mut bindings: im_rc::HashSet<String>,
expr: &mut Expr,
substs: &FxHashMap<String, Box<Expr>>,
) {
use ExprKind::*;
match &mut expr.data {
@ -15,47 +19,43 @@ fn subst(bindings: im_rc::HashSet<String>, expr: &mut Expr, substs: &FxHashMap<S
*expr = *res.clone();
}
}
},
}
All { param, typ, body, .. } => {
subst(bindings.clone(), typ, substs);
let mut on_body = bindings.clone();
on_body.insert(param.to_string());
subst(on_body.clone(), body, substs);
},
bindings.insert(param.to_string());
subst(bindings, body, substs);
}
Lambda { param, body, .. } => {
let mut on_body = bindings.clone();
on_body.insert(param.to_string());
subst(on_body.clone(), body, substs);
},
bindings.insert(param.to_string());
subst(bindings, body, substs);
}
App { fun, args } => {
subst(bindings.clone(), fun, substs);
for arg in args.iter_mut() {
subst(bindings.clone(), &mut arg.data, substs);
}
},
}
Fun { name: _, args } | Ctr { name: _, args } => {
for arg in args.iter_mut() {
subst(bindings.clone(), arg, substs);
}
},
}
Let { name, val, next } => {
subst(bindings.clone(), val, substs);
let mut on_body = bindings.clone();
on_body.insert(name.to_string());
subst(on_body.clone(), next, substs);
},
bindings.insert(name.to_string());
subst(bindings, next, substs);
}
Ann { expr, typ } => {
subst(bindings.clone(), expr, substs);
subst(bindings.clone(), typ, substs);
},
subst(bindings, typ, substs);
}
Sub { expr, .. } => {
subst(bindings.clone(), expr, substs);
},
subst(bindings, expr, substs);
}
Binary { left, right, .. } => {
subst(bindings.clone(), left, substs);
subst(bindings, right, substs);
},
_ => ()
}
_ => (),
}
}

8
crates/kind-pass/src/unbound/mod.rs
View File

@ -169,8 +169,7 @@ impl Visitor for UnboundCollector {
}
fn visit_qualified_ident(&mut self, ident: &mut QualifiedIdent) {
if !ident.get_aux().is_none() {
if ident.get_aux().is_some() {
panic!("problem with 'use' desugaring")
}
@ -260,7 +259,7 @@ impl Visitor for UnboundCollector {
match repeated_names.get(&cons.name.to_string()) {
None => {
repeated_names.insert(cons.name.to_string(), cons.name.range);
},
}
Some(_) => {
failed = true;
}
@ -648,8 +647,7 @@ impl Visitor for UnboundCollector {
Mut(expr) => self.visit_expr(expr),
Get => (),
}
},
}
}
}
}

8
crates/kind-report/src/report/code.rs
View File

@ -123,13 +123,13 @@ pub fn group_marker_lines<'a>(
let end = guide.find(marker.position.end);
if let Some(row) = markers_by_line.get_mut(&start.line) {
row.push((start.clone(), end.clone(), &marker))
row.push((start, end, marker))
} else {
markers_by_line.insert(start.line, vec![(start.clone(), end.clone(), &marker)]);
markers_by_line.insert(start.line, vec![(start, end, marker)]);
}
if end.line != start.line {
multi_line_markers.push((start.clone(), end.clone(), &marker));
multi_line_markers.push((start, end, marker));
} else if marker.main {
// Just to make errors a little bit better
let start = start.line.saturating_sub(1);
@ -154,4 +154,4 @@ pub fn group_marker_lines<'a>(
}
(lines_set, markers_by_line, multi_line_markers)
}
}

6
crates/kind-report/src/report/mode/classic.rs
View File

@ -193,7 +193,7 @@ impl Renderable<Classic> for Subtitle {
}
}
impl<'a> Renderable<Classic> for Word {
impl Renderable<Classic> for Word {
fn render(&self, fmt: &mut dyn Write, _: &dyn FileCache, _: &RenderConfig) -> Res {
match self {
Word::Normal(str) => write!(fmt, "{} ", Paint::new(str)),
@ -390,14 +390,14 @@ impl Renderable<Classic> for Log {
u64
)
}
Log::Empty => writeln!(fmt, ""),
Log::Empty => writeln!(fmt),
}
}
}
impl<'a> Renderable<Classic> for Markers<'a> {
fn render(&self, fmt: &mut dyn Write, cache: &dyn FileCache, config: &RenderConfig) -> Res {
let groups = group_markers(&self.0);
let groups = group_markers(self.0);
let is_empty = groups.is_empty();
let current = PathBuf::from(".").canonicalize().unwrap();

4
crates/kind-report/src/report/mode/compact.rs
View File

@ -41,7 +41,7 @@ fn mark_code(
Ok(())
}
impl<'a> Renderable<Compact> for Word {
impl Renderable<Compact> for Word {
fn render(&self, fmt: &mut dyn Write, _: &dyn FileCache, _: &RenderConfig) -> Res {
match self {
Word::Normal(str) => write!(fmt, "{} ", str),
@ -134,7 +134,7 @@ impl<'a> Renderable<Compact> for CodeBlock<'a> {
impl<'a> Renderable<Compact> for Markers<'a> {
fn render(&self, fmt: &mut dyn Write, cache: &dyn FileCache, config: &RenderConfig) -> Res {
let groups = group_markers(&self.0);
let groups = group_markers(self.0);
let current = PathBuf::from(".").canonicalize().unwrap();
for (ctx, markers) in groups.iter() {

2
crates/kind-report/src/report/mode/mod.rs
View File

@ -47,7 +47,7 @@ pub trait Renderable<T> {
fn render(&self, fmt: &mut dyn Write, cache: &dyn FileCache, config: &RenderConfig) -> Res;
}
impl<'a, T, E> Renderable<T> for Vec<E>
impl<T, E> Renderable<T> for Vec<E>
where
E: Renderable<T>,
{

75
crates/kind-target-kdl/src/compile.rs
View File

@ -16,14 +16,14 @@ const U60_MAX: kdl::U120 = kdl::U120(0xFFFFFFFFFFFFFFF);
fn char_to_code(chr: char) -> Result<u128, String> {
let num = match chr {
'.' => 0,
'0'..='9' => 1 + chr as u128 - '0' as u128,
'A'..='Z' => 11 + chr as u128 - 'A' as u128,
'a'..='z' => 37 + chr as u128 - 'a' as u128,
'_' => 63,
_ => {
return Err(format!("Invalid Kindelia Name letter '{}'.", chr));
}
'.' => 0,
'0'..='9' => 1 + chr as u128 - '0' as u128,
'A'..='Z' => 11 + chr as u128 - 'A' as u128,
'a'..='z' => 37 + chr as u128 - 'a' as u128,
'_' => 63,
_ => {
return Err(format!("Invalid Kindelia Name letter '{}'.", chr));
}
};
Ok(num)
}
@ -32,7 +32,7 @@ pub fn from_str(name_txt: &str) -> Result<Name, String> {
let mut num: u128 = 0;
for (i, chr) in name_txt.chars().enumerate() {
if i >= Name::MAX_CHARS {
return Err("Too big".to_string())
return Err("Too big".to_string());
}
num = (num << 6) + char_to_code(chr)?;
}
@ -140,7 +140,10 @@ pub fn compile_book(
if let Ok(new_name) = from_str(&new_name) {
ctx.kdl_names.insert(name.clone(), new_name);
} else {
ctx.send_err(Box::new(KdlDiagnostic::InvalidVarName(entry.name.to_string(), entry.name.range)));
ctx.send_err(Box::new(KdlDiagnostic::InvalidVarName(
entry.name.to_string(),
entry.name.range,
)));
}
}
@ -185,7 +188,10 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kdl::Term {
if let Ok(name) = res_name {
To::Var { name }
} else {
ctx.send_err(Box::new(KdlDiagnostic::InvalidVarName(name.to_string(), name.range)));
ctx.send_err(Box::new(KdlDiagnostic::InvalidVarName(
name.to_string(),
name.range,
)));
err_term()
}
}
@ -203,7 +209,11 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kdl::Term {
let body = Box::new(compile_expr(ctx, body));
let not_used_now = ctx.kdl_used_names.contains(param.to_str());
let name = if not_used_now { Ok(from_str("").unwrap()) } else { name };
let name = if not_used_now {
Ok(from_str("").unwrap())
} else {
name
};
if not_used_now {
ctx.kdl_used_names.remove(param.to_str());
@ -216,11 +226,18 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kdl::Term {
if let Ok(name) = name {
To::Lam { name, body }
} else {
ctx.send_err(Box::new(KdlDiagnostic::InvalidVarName(param.to_string(), param.range)));
ctx.send_err(Box::new(KdlDiagnostic::InvalidVarName(
param.to_string(),
param.range,
)));
err_term()
}
}
From::Let { name: param, val, next } => {
From::Let {
name: param,
val,
next,
} => {
let res_name = from_str(param.to_str());
let not_used = ctx.kdl_used_names.contains(param.to_str());
@ -241,13 +258,16 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kdl::Term {
ctx.kdl_used_names.insert(param.to_string());
}
let argm = Box::new(compile_expr(ctx, &val));
let argm = Box::new(compile_expr(ctx, val));
if let Ok(name) = res_name {
let func = Box::new(To::Lam { name, body: expr });
To::App { func, argm }
} else {
ctx.send_err(Box::new(KdlDiagnostic::InvalidVarName(param.to_string(), param.range)));
ctx.send_err(Box::new(KdlDiagnostic::InvalidVarName(
param.to_string(),
param.range,
)));
err_term()
}
}
@ -314,8 +334,8 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kdl::Term {
return To::Num { numb };
}
}
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 } => {
@ -420,7 +440,7 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kdl::Term {
val1: Box::new(compile_expr(ctx, &args[1])),
},
_ => {
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 }
}
@ -488,7 +508,10 @@ fn compile_common_function(ctx: &mut CompileCtx, entry: &untyped::Entry) {
if let Ok(name) = from_str(name) {
args.push(name)
} else {
ctx.send_err(Box::new(KdlDiagnostic::InvalidVarName(name.to_string(), *range)));
ctx.send_err(Box::new(KdlDiagnostic::InvalidVarName(
name.to_string(),
*range,
)));
}
}
@ -545,17 +568,13 @@ fn compile_u120_new(ctx: &mut CompileCtx, entry: &untyped::Entry) {
// U120.new hi lo = (hi << 60) | lo
let hi_name = from_str("hi").unwrap();
let lo_name = from_str("lo").unwrap();
let hi_var = kdl::Term::Var {
name: hi_name.clone(),
};
let lo_var = kdl::Term::Var {
name: lo_name.clone(),
};
let hi_var = kdl::Term::Var { name: hi_name };
let lo_var = kdl::Term::Var { name: lo_name };
let name = ctx.kdl_names.get(entry.name.to_str()).cloned().unwrap();
let args = vec![hi_name, lo_name];
let rules = vec![kdl::Rule {
lhs: kdl::Term::Fun {
name: name.clone(),
name,
args: vec![hi_var.clone(), lo_var.clone()],
},
rhs: kdl::Term::Op2 {
@ -622,4 +641,4 @@ fn compile_oper(oper: &kind_tree::Operator) -> kdl::Oper {
From::Xor => To::Xor,
From::Or => To::Or,
}
}
}

4
crates/kind-target-kdl/src/flatten.rs
View File

@ -178,10 +178,10 @@ fn split_rule(
(ExprKind::U60 { .. }, ExprKind::U60 { .. }) => (),
(ExprKind::F60 { .. }, ExprKind::F60 { .. }) => (),
(ExprKind::U60 { .. }, ExprKind::Var { name }) => {
subst(&mut new_rule_body, &name, rule_pat);
subst(&mut new_rule_body, name, rule_pat);
}
(ExprKind::F60 { .. }, 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

277
crates/kind-tests/benches/pure.rs
View File

@ -1,20 +1,23 @@
#![feature(test)]
extern crate test;
use std::{fs, path::{PathBuf}};
use std::{fs, path::PathBuf};
use driver::{resolution};
use driver::resolution;
use kind_driver::session::Session;
use kind_pass::{expand::{self, uses::expand_uses}, desugar, erasure};
use kind_pass::{
desugar, erasure,
expand::{self, uses::expand_uses},
};
use test::Bencher;
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, false)
}
@ -29,173 +32,211 @@ fn exp_paths() -> Vec<&'static str> {
#[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();
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)
paths
.iter()
.map(|input| {
let session = new_session();
kind_parser::parse_book(session.diagnostic_sender.clone(), 0, input)
})
.count()
})
}
#[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();
let mut paths: Vec<_> = paths
.iter()
.map(|path| {
let input = fs::read_to_string(path).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)
paths
.iter_mut()
.map(|module| {
let (rx, _) = std::sync::mpsc::channel();
expand_uses(module, rx);
})
.count()
})
}
#[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();
let mut books: Vec<_> = paths
.iter()
.map(|path| {
let input = fs::read_to_string(path).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)
books
.iter_mut()
.map(|module| {
let (rx, tx) = std::sync::mpsc::channel();
expand::expand_module(rx, module);
assert!(tx.iter().collect::<Vec<_>>().is_empty())
})
.count()
})
}
#[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();
let mut books: Vec<_> = paths
.iter()
.map(|path| {
let mut session = new_session();
let book = resolution::parse_and_store_book(&mut session, &path.into()).unwrap();
(session, book)
})
.collect();
b.iter(|| {
books.iter_mut().map(|(session, book)| {
let result = resolution::check_unbound_top_level(session, book);
assert!(result.is_ok());
}).fold(0, |n, _| n + 1)
books
.iter_mut()
.map(|(session, book)| {
let result = resolution::check_unbound_top_level(session, book);
assert!(result.is_ok());
})
.count()
})
}
#[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 result = resolution::check_unbound_top_level(&mut session, &mut book);
assert!(result.is_ok());
(session, book)
}).collect();
let mut books: Vec<_> = paths
.iter()
.map(|path| {
let mut session = new_session();
let mut book = resolution::parse_and_store_book(&mut session, &path.into()).unwrap();
let result = resolution::check_unbound_top_level(&mut session, &mut book);
assert!(result.is_ok());
(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)
books
.iter_mut()
.map(|(session, book)| {
desugar::desugar_book(session.diagnostic_sender.clone(), book).unwrap()
})
.count()
})
}
#[bench]
fn bench_exp_pure_erase(b: &mut Bencher) {
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 result = resolution::check_unbound_top_level(&mut session, &mut book);
let book = desugar::desugar_book(session.diagnostic_sender.clone(), &book).unwrap();
assert!(result.is_ok());
let books: Vec<_> = paths
.iter()
.map(|path| {
let mut session = new_session();
let mut book = resolution::parse_and_store_book(&mut session, &path.into()).unwrap();
let result = resolution::check_unbound_top_level(&mut session, &mut book);
let book = desugar::desugar_book(session.diagnostic_sender.clone(), &book).unwrap();
assert!(result.is_ok());
(session, book)
}).collect();
(session, book)
})
.collect();
b.iter(|| {
books.iter().map(|(session, book)| {
erasure::erase_book(
book,
books
.iter()
.map(|(session, book)| {
erasure::erase_book(
book,
session.diagnostic_sender.clone(),
vec!["Main".to_string()],
)
.unwrap();
})
.count()
})
}
#[bench]
fn bench_exp_pure_to_hvm(b: &mut Bencher) {
let paths = exp_paths();
let books: Vec<_> = paths
.iter()
.map(|path| {
let mut session = new_session();
let mut book = resolution::parse_and_store_book(&mut session, &path.into()).unwrap();
let result = resolution::check_unbound_top_level(&mut session, &mut book);
let book = desugar::desugar_book(session.diagnostic_sender.clone(), &book).unwrap();
assert!(result.is_ok());
let book = erasure::erase_book(
&book,
session.diagnostic_sender.clone(),
vec!["Main".to_string()],
).unwrap();
}).fold(0, |n, _| n + 1)
)
.unwrap();
(session, book)
})
.collect();
b.iter(move || {
books
.iter()
.map(move |(_, book)| kind_target_hvm::compile_book(book.to_owned(), false))
.count()
})
}
#[bench]
fn bench_exp_pure_to_hvm(b: &mut Bencher) {
fn bench_exp_pure_gen_checker(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 result = resolution::check_unbound_top_level(&mut session, &mut book);
let book = desugar::desugar_book(session.diagnostic_sender.clone(), &book).unwrap();
assert!(result.is_ok());
let books: Vec<_> = paths
.iter()
.map(|path| {
let mut session = new_session();
let mut book = resolution::parse_and_store_book(&mut session, &path.into()).unwrap();
let result = resolution::check_unbound_top_level(&mut session, &mut book);
let book = desugar::desugar_book(session.diagnostic_sender.clone(), &book).unwrap();
assert!(result.is_ok());
let book = erasure::erase_book(
&book,
session.diagnostic_sender.clone(),
vec!["Main".to_string()],
).unwrap();
(session, book)
}).collect();
(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_gen_checker(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 result = resolution::check_unbound_top_level(&mut session, &mut book);
let book = desugar::desugar_book(session.diagnostic_sender.clone(), &book).unwrap();
assert!(result.is_ok());
(session, book)
}).collect();
b.iter(move || {
books.iter().map(move |(_, book)| {
kind_checker::gen_checker(book, true, book.names.keys().cloned().collect())
}).fold(0, |n, _| n + 1)
books
.iter()
.map(move |(_, book)| {
kind_checker::gen_checker(book, true, book.names.keys().cloned().collect())
})
.count()
})
}

57
crates/kind-tree/src/concrete/expr.rs
View File

@ -140,7 +140,7 @@ pub struct Sttm {
pub enum SeqOperation {
Set(Box<Expr>),
Mut(Box<Expr>),
Get
Get,
}
#[derive(Clone, Debug)]
@ -148,7 +148,7 @@ pub struct SeqRecord {
pub typ: Box<Expr>,
pub expr: Box<Expr>,
pub fields: Vec<Ident>,
pub operation: SeqOperation
pub operation: SeqOperation,
}
#[derive(Clone, Debug)]
@ -225,10 +225,10 @@ pub enum ExprKind {
type_name: QualifiedIdent,
var_name: Ident,
motive: Option<Box<Expr>>,
next: Box<Expr>
next: Box<Expr>,
},
SeqRecord(SeqRecord)
SeqRecord(SeqRecord),
}
/// Describes a single expression inside Kind2.
@ -241,7 +241,7 @@ pub struct Expr {
impl Expr {
pub fn var(name: Ident) -> Box<Expr> {
Box::new(Expr {
range: name.range.clone(),
range: name.range,
data: ExprKind::Var { name },
})
}
@ -309,7 +309,6 @@ impl Expr {
range,
})
}
}
impl Locatable for Binding {
@ -573,8 +572,18 @@ impl Display for Expr {
args.iter().map(|x| format!(" {}", x)).collect::<String>()
),
Let { name, val, next } => write!(f, "(let {} = {}; {})", name, val, next),
Open { type_name, var_name, motive: Some(motive), next } => write!(f, "(open {} {} : {motive}; {})", type_name, var_name, next),
Open { type_name, var_name, motive: None, next } => write!(f, "(open {} {}; {})", type_name, var_name, next),
Open {
type_name,
var_name,
motive: Some(motive),
next,
} => write!(f, "(open {} {} : {motive}; {})", type_name, var_name, next),
Open {
type_name,
var_name,
motive: None,
next,
} => write!(f, "(open {} {}; {})", type_name, var_name, next),
If { cond, then_, else_ } => {
write!(f, "(if {} {{{}}} else {{{}}})", cond, then_, else_)
}
@ -593,13 +602,23 @@ impl Display for Expr {
Hole => write!(f, "_"),
SeqRecord(rec) => {
use SeqOperation::*;
write!(f, "(!({}) {} {}", rec.typ, rec.expr, rec.fields.iter().map(|x| format!(".{}", x.to_str())).collect::<Vec<_>>().join(","))?;
write!(
f,
"(!({}) {} {}",
rec.typ,
rec.expr,
rec.fields
.iter()
.map(|x| format!(".{}", x.to_str()))
.collect::<Vec<_>>()
.join(",")
)?;
match &rec.operation {
Set(expr) => write!(f, "+= {})", expr),
Mut(expr) => write!(f, "@= {})", expr),
Get => write!(f, ")")
Get => write!(f, ")"),
}
},
}
}
}
}
@ -607,17 +626,13 @@ impl Display for Expr {
impl Binding {
pub fn to_app_binding(&self) -> AppBinding {
match self {
Binding::Positional(expr) => {
AppBinding {
data: expr.clone(),
erased: false,
}
Binding::Positional(expr) => AppBinding {
data: expr.clone(),
erased: false,
},
Binding::Named(_, _, expr) => {
AppBinding {
data: expr.clone(),
erased: false,
}
Binding::Named(_, _, expr) => AppBinding {
data: expr.clone(),
erased: false,
},
}
}

14
crates/kind-tree/src/concrete/mod.rs
View File

@ -121,7 +121,13 @@ pub struct RecordDecl {
impl RecordDecl {
pub fn get_constructor(&self) -> Constructor {
Constructor { name: self.constructor.clone(), docs: vec![], attrs: self.cons_attrs.clone(), args: self.fields_to_arguments(), typ: None }
Constructor {
name: self.constructor.clone(),
docs: vec![],
attrs: self.cons_attrs.clone(),
args: self.fields_to_arguments(),
typ: None,
}
}
}
@ -296,9 +302,7 @@ impl Display for Module {
impl Display for Book {
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
for entr in self.entries.values() {
match entr {
_ => write!(f, "{}", entr)?,
}
write!(f, "{}", entr)?
}
Ok(())
}
@ -598,4 +602,4 @@ impl Argument {
range: self.range,
}
}
}
}

48
crates/kind-tree/src/desugared/mod.rs
View File

@ -11,7 +11,8 @@ pub use crate::Operator;
use crate::{
symbol::{Ident, QualifiedIdent},
Attributes, telescope::Telescope,
telescope::Telescope,
Attributes,
};
/// Just a vector of expressions. It is called spine because
@ -170,8 +171,11 @@ impl Expr {
})
}
pub fn unfold_all(irrelev: &[bool], idents: &[(Ident, Box<Expr>)], body: Box<Expr>) -> Box<Expr> {
pub fn unfold_all(
irrelev: &[bool],
idents: &[(Ident, Box<Expr>)],
body: Box<Expr>,
) -> Box<Expr> {
idents
.iter()
.rev()
@ -345,7 +349,7 @@ pub struct Entry {
pub struct Family {
pub name: QualifiedIdent,
pub parameters: Telescope<Argument>,
pub constructors: Vec<QualifiedIdent>
pub constructors: Vec<QualifiedIdent>,
}
/// A book is a collection of desugared entries.
@ -397,17 +401,13 @@ impl Display for AppBinding {
}
pub fn try_desugar_to_nat(name: &QualifiedIdent, spine: &[Box<Expr>], acc: u128) -> Option<u128> {
match name.to_str() {
"Nat.zero" if spine.len() == 0 => {
Some(acc)
}
"Nat.succ" if spine.len() == 1 => {
match &spine[0].data {
ExprKind::Ctr { name, args } => try_desugar_to_nat(name, args, acc + 1),
_ => None
}
}
_ => None
match (name.to_str(), spine) {
("Nat.zero", []) => Some(acc),
("Nat.succ", [spine]) => match &spine.data {
ExprKind::Ctr { name, args } => try_desugar_to_nat(name, args, acc + 1),
_ => None,
},
_ => None,
}
}
@ -445,17 +445,15 @@ impl Display for Expr {
Fun { name, args } | Ctr { name, args } => {
if let Some(res) = try_desugar_to_nat(name, args, 0) {
write!(f, "{res}n")
} else if args.is_empty() {
write!(f, "{}", name)
} else {
if args.is_empty() {
write!(f, "{}", name)
} else {
write!(
f,
"({}{})",
name,
args.iter().map(|x| format!(" {}", x)).collect::<String>()
)
}
write!(
f,
"({}{})",
name,
args.iter().map(|x| format!(" {}", x)).collect::<String>()
)
}
}
Let { name, val, next } => write!(f, "(let {} = {}; {})", name, val, next),

2
crates/kind-tree/src/symbol.rs
View File

@ -135,7 +135,7 @@ impl QualifiedIdent {
}
pub fn pop_last_segment(&self) -> QualifiedIdent {
let mut segments = self.root.data.split(".").collect::<Vec<_>>();
let mut segments = self.root.data.split('.').collect::<Vec<_>>();
segments.pop();
QualifiedIdent {
root: Symbol::new(segments.join(".")),