mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-11 08:45:32 +03:00
Merge remote-tracking branch 'origin/experimental' into experimental
This commit is contained in:
commit
242f5324dc
36
Cargo.lock
generated
36
Cargo.lock
generated
@ -445,6 +445,20 @@ dependencies = [
|
||||
"version_check",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "im-rc"
|
||||
version = "15.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "af1955a75fa080c677d3972822ec4bad316169ab1cfc6c257a942c2265dbe5fe"
|
||||
dependencies = [
|
||||
"bitmaps",
|
||||
"rand_core 0.6.4",
|
||||
"rand_xoshiro",
|
||||
"sized-chunks",
|
||||
"typenum",
|
||||
"version_check",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "impl-codec"
|
||||
version = "0.6.0"
|
||||
@ -530,7 +544,7 @@ version = "0.1.0"
|
||||
dependencies = [
|
||||
"fxhash",
|
||||
"hvm",
|
||||
"im",
|
||||
"im-rc",
|
||||
"kind-report",
|
||||
"kind-span",
|
||||
"kind-tree",
|
||||
@ -545,9 +559,6 @@ dependencies = [
|
||||
"kind-driver",
|
||||
"kind-query",
|
||||
"kind-report",
|
||||
"ntest",
|
||||
"pretty_assertions",
|
||||
"walkdir",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
@ -555,7 +566,7 @@ name = "kind-derive"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"fxhash",
|
||||
"im",
|
||||
"im-rc",
|
||||
"kind-report",
|
||||
"kind-span",
|
||||
"kind-tree",
|
||||
@ -594,7 +605,7 @@ name = "kind-pass"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"fxhash",
|
||||
"im",
|
||||
"im-rc",
|
||||
"kind-derive",
|
||||
"kind-report",
|
||||
"kind-span",
|
||||
@ -658,6 +669,19 @@ dependencies = [
|
||||
"tiny-keccak",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "kind-tests"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"kind-checker",
|
||||
"kind-driver",
|
||||
"kind-query",
|
||||
"kind-report",
|
||||
"ntest",
|
||||
"pretty_assertions",
|
||||
"walkdir",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "kind-tree"
|
||||
version = "0.1.0"
|
||||
|
@ -12,11 +12,9 @@ members = [
|
||||
"crates/kind-target-kdl",
|
||||
"crates/kind-target-hvm",
|
||||
"crates/kind-derive",
|
||||
"crates/kind-tests",
|
||||
# "crates/kind-optimization",
|
||||
# "crates/kind-lint",
|
||||
# "crates/kind-query",
|
||||
# "crates/kind-macros",
|
||||
]
|
||||
|
||||
[profile.release]
|
||||
debug = true
|
@ -13,4 +13,4 @@ kind-report = { path = "../kind-report" }
|
||||
hvm = { git = "https://github.com/Kindelia/HVM.git" }
|
||||
|
||||
fxhash = "0.2.1"
|
||||
im = "15.1.0"
|
||||
im-rc = "15.1.0"
|
File diff suppressed because it is too large
Load Diff
@ -85,49 +85,49 @@ fn parse_expr(term: &Term) -> Result<Box<desugared::Expr>, String> {
|
||||
}
|
||||
|
||||
fn parse_all_expr(
|
||||
names: im::HashMap<String, String>,
|
||||
names: im_rc::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(
|
||||
"Kind.Term.Quoted.all" => Ok(Expr::all(
|
||||
parse_orig(&args[0])?,
|
||||
Ident::generate(&parse_name(&args[1])?),
|
||||
parse_all_expr(names.clone(), &args[2])?,
|
||||
parse_all_expr(names, &args[3])?,
|
||||
false, // TODO: Fix
|
||||
)),
|
||||
"Kind.Quoted.lam" => Ok(Expr::lambda(
|
||||
"Kind.Term.Quoted.lam" => Ok(Expr::lambda(
|
||||
parse_orig(&args[0])?,
|
||||
Ident::generate(&parse_name(&args[1])?),
|
||||
parse_all_expr(names, &args[2])?,
|
||||
false, // TODO: Fix
|
||||
)),
|
||||
"Kind.Quoted.let" => Ok(Expr::let_(
|
||||
"Kind.Term.Quoted.let" => Ok(Expr::let_(
|
||||
parse_orig(&args[0])?,
|
||||
Ident::generate(&parse_name(&args[1])?),
|
||||
parse_all_expr(names.clone(), &args[2])?,
|
||||
parse_all_expr(names, &args[3])?,
|
||||
)),
|
||||
"Kind.Quoted.typ" => Ok(Expr::typ(parse_orig(&args[0])?)),
|
||||
"Kind.Quoted.var" => Ok(Expr::var(Ident::new(
|
||||
"Kind.Term.Quoted.typ" => Ok(Expr::typ(parse_orig(&args[0])?)),
|
||||
"Kind.Term.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(
|
||||
"Kind.Term.Quoted.hol" => Ok(Expr::hole(parse_orig(&args[0])?, parse_num(&args[1])?)),
|
||||
"Kind.Term.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(
|
||||
"Kind.Term.Quoted.sub" => Ok(Expr::sub(
|
||||
parse_orig(&args[0])?,
|
||||
Ident::generate(&parse_name(&args[1])?),
|
||||
parse_num(&args[2])? as usize,
|
||||
parse_num(&args[3])? as usize,
|
||||
parse_all_expr(names, &args[4])?,
|
||||
)),
|
||||
"Kind.Quoted.app" => Ok(Expr::app(
|
||||
"Kind.Term.Quoted.app" => Ok(Expr::app(
|
||||
parse_orig(&args[0])?,
|
||||
parse_all_expr(names.clone(), &args[1])?,
|
||||
vec![desugared::AppBinding {
|
||||
@ -135,7 +135,7 @@ fn parse_all_expr(
|
||||
erased: false,
|
||||
}],
|
||||
)),
|
||||
"Kind.Quoted.ctr" => {
|
||||
"Kind.Term.Quoted.ctr" => {
|
||||
let name = parse_qualified(&args[0])?;
|
||||
let orig = parse_orig(&args[1])?;
|
||||
let mut res = Vec::new();
|
||||
@ -144,7 +144,7 @@ fn parse_all_expr(
|
||||
}
|
||||
Ok(Expr::ctr(orig, name, res))
|
||||
}
|
||||
"Kind.Quoted.fun" => Ok(Expr::fun(
|
||||
"Kind.Term.Quoted.fun" => Ok(Expr::fun(
|
||||
parse_orig(&args[1])?,
|
||||
parse_qualified(&args[0])?,
|
||||
{
|
||||
@ -155,11 +155,11 @@ fn parse_all_expr(
|
||||
res
|
||||
},
|
||||
)),
|
||||
"Kind.Quoted.hlp" => Ok(Expr::hlp(parse_orig(&args[0])?, Ident::generate("?"))),
|
||||
"Kind.Quoted.u60" => Ok(Expr::type_u60(parse_orig(&args[0])?)),
|
||||
"Kind.Term.Quoted.hlp" => Ok(Expr::hlp(parse_orig(&args[0])?, Ident::generate("?"))),
|
||||
"Kind.Term.Quoted.u60" => Ok(Expr::type_u60(parse_orig(&args[0])?)),
|
||||
"Kind.Term.Quoted.num" => Ok(Expr::num_u60(parse_orig(&args[0])?, parse_num(&args[1])?)),
|
||||
// TODO: Change quoting to support floats
|
||||
"Kind.Quoted.num" => Ok(Expr::num_u60(parse_orig(&args[0])?, parse_num(&args[1])?)),
|
||||
"Kind.Quoted.op2" => Ok(Expr::binary(
|
||||
"Kind.Term.Quoted.op2" => Ok(Expr::binary(
|
||||
parse_orig(&args[0])?,
|
||||
parse_op(&args[1])?,
|
||||
parse_all_expr(names.clone(), &args[2])?,
|
||||
@ -232,13 +232,13 @@ fn parse_type_error(expr: &Term) -> Result<TypeError, String> {
|
||||
"Kind.Error.Quoted.impossible_case" => Ok(TypeError::ImpossibleCase(
|
||||
ctx,
|
||||
orig,
|
||||
parse_all_expr(im::HashMap::new(), &args[2])?,
|
||||
parse_all_expr(im::HashMap::new(), &args[3])?,
|
||||
parse_all_expr(im_rc::HashMap::new(), &args[2])?,
|
||||
parse_all_expr(im_rc::HashMap::new(), &args[3])?,
|
||||
)),
|
||||
"Kind.Error.Quoted.inspection" => Ok(TypeError::Inspection(
|
||||
ctx,
|
||||
orig,
|
||||
parse_all_expr(im::HashMap::new(), &args[2])?,
|
||||
parse_all_expr(im_rc::HashMap::new(), &args[2])?,
|
||||
)),
|
||||
"Kind.Error.Quoted.too_many_arguments" => {
|
||||
Ok(TypeError::TooManyArguments(ctx, orig))
|
||||
@ -246,8 +246,8 @@ fn parse_type_error(expr: &Term) -> Result<TypeError, String> {
|
||||
"Kind.Error.Quoted.type_mismatch" => Ok(TypeError::TypeMismatch(
|
||||
ctx,
|
||||
orig,
|
||||
parse_all_expr(im::HashMap::new(), &args[2])?,
|
||||
parse_all_expr(im::HashMap::new(), &args[3])?,
|
||||
parse_all_expr(im_rc::HashMap::new(), &args[2])?,
|
||||
parse_all_expr(im_rc::HashMap::new(), &args[3])?,
|
||||
)),
|
||||
_ => Err("Unexpected tag on quoted value".to_string()),
|
||||
}
|
||||
|
@ -20,9 +20,3 @@ kind-checker = { path = "../kind-checker" }
|
||||
kind-query = { path = "../kind-query" }
|
||||
|
||||
clap = { version = "4.0.10", features = ["derive"] }
|
||||
|
||||
[dev-dependencies]
|
||||
|
||||
pretty_assertions = "1.3.0"
|
||||
ntest = "0.8.1"
|
||||
walkdir = "2"
|
||||
|
@ -32,6 +32,10 @@ pub struct Cli {
|
||||
#[arg(short, long)]
|
||||
pub no_color: bool,
|
||||
|
||||
/// Prints all of the functions and their evaluation
|
||||
#[arg(short, long)]
|
||||
pub trace: bool,
|
||||
|
||||
/// Only ascii characters in error messages
|
||||
#[arg(short, long)]
|
||||
pub ascii: bool,
|
||||
@ -149,6 +153,7 @@ pub fn compile_in_session<T>(
|
||||
Log::Checked(start.elapsed())
|
||||
},
|
||||
);
|
||||
eprintln!();
|
||||
res
|
||||
} else {
|
||||
render_to_stderr(&render_config, &session, &Log::Failed(start.elapsed()));
|
||||
@ -175,13 +180,14 @@ pub fn run_cli(config: Cli) {
|
||||
match config.command {
|
||||
Command::Check { file } => {
|
||||
compile_in_session(render_config, root, file.clone(), false, &mut |session| {
|
||||
driver::type_check_book(session, &PathBuf::from(file.clone()))
|
||||
driver::type_check_book(session, &PathBuf::from(file.clone()), entrypoints.clone())
|
||||
});
|
||||
}
|
||||
Command::ToHVM { file } => {
|
||||
compile_in_session(render_config, root, file.clone(), true, &mut |session| {
|
||||
let book = driver::erase_book(session, &PathBuf::from(file.clone()))?;
|
||||
Some(driver::compile_book_to_hvm(book))
|
||||
let book =
|
||||
driver::erase_book(session, &PathBuf::from(file.clone()), entrypoints.clone())?;
|
||||
Some(driver::compile_book_to_hvm(book, config.trace))
|
||||
})
|
||||
.map(|res| {
|
||||
println!("{}", res);
|
||||
@ -190,9 +196,10 @@ pub fn run_cli(config: Cli) {
|
||||
}
|
||||
Command::Run { file } => {
|
||||
let res = compile_in_session(render_config, root, file.clone(), true, &mut |session| {
|
||||
let book = driver::erase_book(session, &PathBuf::from(file.clone()))?;
|
||||
let book =
|
||||
driver::erase_book(session, &PathBuf::from(file.clone()), entrypoints.clone())?;
|
||||
driver::check_main_entry(session, &book)?;
|
||||
Some(driver::compile_book_to_hvm(book))
|
||||
Some(driver::compile_book_to_hvm(book, config.trace))
|
||||
});
|
||||
|
||||
if let Some(res) = res {
|
||||
@ -222,7 +229,7 @@ pub fn run_cli(config: Cli) {
|
||||
}
|
||||
Command::Erase { file } => {
|
||||
compile_in_session(render_config, root, file.clone(), true, &mut |session| {
|
||||
driver::erase_book(session, &PathBuf::from(file.clone()))
|
||||
driver::erase_book(session, &PathBuf::from(file.clone()), entrypoints.clone())
|
||||
})
|
||||
.map(|res| {
|
||||
print!("{}", res);
|
||||
@ -252,6 +259,7 @@ pub fn run_cli(config: Cli) {
|
||||
&PathBuf::from(file.clone()),
|
||||
session,
|
||||
&namespace.clone().unwrap_or("".to_string()),
|
||||
entrypoints.clone(),
|
||||
)
|
||||
})
|
||||
.map(|res| {
|
||||
|
@ -1,24 +0,0 @@
|
||||
ERROR Required functions are not implemented for this type.
|
||||
|
||||
/--[tests/suite/checker/derive/fail/WrongU120.kind2:5:12]
|
||||
|
|
||||
4 |
|
||||
5 | Teste : Eq 123u120 124u120
|
||||
| v------
|
||||
| \You cannot use this expression!
|
||||
6 | Teste = Eq.rfl
|
||||
|
||||
Hint: You must implement 'U120.new' in order to use the u120 notation.
|
||||
|
||||
ERROR Required functions are not implemented for this type.
|
||||
|
||||
/--[tests/suite/checker/derive/fail/WrongU120.kind2:5:20]
|
||||
|
|
||||
4 |
|
||||
5 | Teste : Eq 123u120 124u120
|
||||
| v------
|
||||
| \You cannot use this expression!
|
||||
6 | Teste = Eq.rfl
|
||||
|
||||
Hint: You must implement 'U120.new' in order to use the u120 notation.
|
||||
|
@ -1,6 +0,0 @@
|
||||
type Eq <t: Type> (a: t) ~ (b: t) {
|
||||
rfl: Eq t a a
|
||||
}
|
||||
|
||||
Teste : Eq 123u120 124u120
|
||||
Teste = Eq.rfl
|
@ -10,4 +10,4 @@ kind-span = { path = "../kind-span" }
|
||||
kind-tree = { path = "../kind-tree" }
|
||||
kind-report = { path = "../kind-report" }
|
||||
fxhash = "0.2.1"
|
||||
im = "*"
|
||||
im-rc = "*"
|
117
crates/kind-derive/src/getters.rs
Normal file
117
crates/kind-derive/src/getters.rs
Normal file
@ -0,0 +1,117 @@
|
||||
//! Module to derive a "open" function for records.
|
||||
|
||||
use kind_span::Range;
|
||||
|
||||
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, QualifiedIdent};
|
||||
|
||||
pub fn derive_getters(range: Range, rec: &RecordDecl) -> Vec<concrete::Entry> {
|
||||
let mk_var = |name: Ident| -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::Var { name },
|
||||
range,
|
||||
})
|
||||
};
|
||||
|
||||
let mk_cons = |name: QualifiedIdent, args: Vec<Binding>| -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::Constr { name, args },
|
||||
range,
|
||||
})
|
||||
};
|
||||
|
||||
let mut types = Telescope::default();
|
||||
|
||||
for arg in rec.parameters.iter() {
|
||||
types.push(arg.to_implicit())
|
||||
}
|
||||
|
||||
// The type
|
||||
|
||||
let all_args = rec.parameters.clone();
|
||||
|
||||
let res_motive_ty = mk_cons(
|
||||
rec.name.clone(),
|
||||
all_args
|
||||
.iter()
|
||||
.cloned()
|
||||
.map(|x| Binding::Positional(mk_var(x.name)))
|
||||
.collect(),
|
||||
);
|
||||
|
||||
// Sccrutinzies
|
||||
|
||||
types.push(Argument {
|
||||
hidden: false,
|
||||
erased: false,
|
||||
name: Ident::generate("scrutinizer"),
|
||||
typ: Some(res_motive_ty),
|
||||
range,
|
||||
});
|
||||
|
||||
// Motive with indices
|
||||
|
||||
let mut pats: Vec<Box<Pat>> = Vec::new();
|
||||
|
||||
let spine: Vec<_> = rec
|
||||
.fields
|
||||
.iter()
|
||||
.map(|(name, _, ty)| (name, ty))
|
||||
.collect();
|
||||
|
||||
pats.push(Box::new(Pat {
|
||||
data: concrete::pat::PatKind::App(
|
||||
rec.name.add_segment(rec.constructor.to_str()),
|
||||
spine
|
||||
.iter()
|
||||
.cloned()
|
||||
.map(|x| {
|
||||
Box::new(Pat {
|
||||
data: concrete::pat::PatKind::Var(PatIdent(x.0.clone().with_name(|f| format!("{}_", f)))),
|
||||
range,
|
||||
})
|
||||
})
|
||||
.collect(),
|
||||
),
|
||||
range,
|
||||
}));
|
||||
|
||||
let mut entries = vec![];
|
||||
|
||||
for (arg, typ) in spine {
|
||||
let body = mk_var(arg.with_name(|f| format!("{}_", f)).clone());
|
||||
|
||||
let mut name = rec
|
||||
.name
|
||||
.add_segment(arg.to_str())
|
||||
.add_segment("get");
|
||||
|
||||
name.range = rec.constructor.range;
|
||||
|
||||
|
||||
let rules = vec![Box::new(Rule {
|
||||
name: name.clone(),
|
||||
pats: pats.clone(),
|
||||
body,
|
||||
range: rec.constructor.range,
|
||||
})];
|
||||
|
||||
let entry = Entry {
|
||||
name: name.clone(),
|
||||
docs: Vec::new(),
|
||||
args: types.clone(),
|
||||
typ: typ.clone(),
|
||||
rules,
|
||||
range: rec.constructor.range,
|
||||
attrs: Vec::new(),
|
||||
generated_by: Some(rec.name.to_string().clone()),
|
||||
};
|
||||
|
||||
entries.push(entry)
|
||||
}
|
||||
|
||||
entries
|
||||
}
|
@ -4,3 +4,5 @@ pub mod errors;
|
||||
pub mod matching;
|
||||
pub mod open;
|
||||
pub mod subst;
|
||||
pub mod getters;
|
||||
pub mod setters;
|
@ -42,11 +42,13 @@ pub fn derive_open(range: Range, rec: &RecordDecl) -> concrete::Entry {
|
||||
})
|
||||
};
|
||||
|
||||
let name = rec
|
||||
let mut name = rec
|
||||
.name
|
||||
.add_segment(rec.constructor.to_str())
|
||||
.add_segment("open");
|
||||
|
||||
name.range = rec.constructor.range;
|
||||
|
||||
let mut types = Telescope::default();
|
||||
|
||||
for arg in rec.parameters.iter() {
|
||||
@ -146,7 +148,7 @@ pub fn derive_open(range: Range, rec: &RecordDecl) -> concrete::Entry {
|
||||
name: name.clone(),
|
||||
pats,
|
||||
body,
|
||||
range,
|
||||
range: rec.constructor.range,
|
||||
})];
|
||||
|
||||
let entry = Entry {
|
||||
@ -155,7 +157,7 @@ pub fn derive_open(range: Range, rec: &RecordDecl) -> concrete::Entry {
|
||||
args: types,
|
||||
typ: ret_ty,
|
||||
rules,
|
||||
range,
|
||||
range: rec.constructor.range,
|
||||
attrs: Vec::new(),
|
||||
generated_by: Some(rec.name.to_string().clone()),
|
||||
};
|
||||
|
@ -1,3 +0,0 @@
|
||||
//! Derives getters and setters for record
|
||||
//! types.
|
||||
|
174
crates/kind-derive/src/setters.rs
Normal file
174
crates/kind-derive/src/setters.rs
Normal file
@ -0,0 +1,174 @@
|
||||
//! Module to derive a "open" function for records.
|
||||
|
||||
use kind_span::Range;
|
||||
|
||||
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, QualifiedIdent};
|
||||
|
||||
pub fn derive_setters(range: Range, rec: &RecordDecl) -> Vec<concrete::Entry> {
|
||||
let mk_var = |name: Ident| -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::Var { name },
|
||||
range,
|
||||
})
|
||||
};
|
||||
|
||||
let mk_cons = |name: QualifiedIdent, args: Vec<Binding>| -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::Constr { name, args },
|
||||
range,
|
||||
})
|
||||
};
|
||||
|
||||
let typ = |range: Range| -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::Lit { lit: Literal::Type },
|
||||
range,
|
||||
})
|
||||
};
|
||||
|
||||
let mk_pat_var = |name: Ident| {
|
||||
Box::new(Pat {
|
||||
range: name.range,
|
||||
data: concrete::pat::PatKind::Var(PatIdent(name)),
|
||||
})
|
||||
};
|
||||
|
||||
let mut types = Telescope::default();
|
||||
|
||||
for arg in rec.parameters.iter() {
|
||||
types.push(arg.to_implicit())
|
||||
}
|
||||
|
||||
// The type
|
||||
|
||||
let all_args = rec.parameters.clone();
|
||||
|
||||
let res_motive_ty = mk_cons(
|
||||
rec.name.clone(),
|
||||
all_args
|
||||
.iter()
|
||||
.cloned()
|
||||
.map(|x| Binding::Positional(mk_var(x.name)))
|
||||
.collect(),
|
||||
);
|
||||
|
||||
// Sccrutinzies
|
||||
|
||||
types.push(Argument {
|
||||
hidden: false,
|
||||
erased: false,
|
||||
name: Ident::generate("scrutinizer"),
|
||||
typ: Some(res_motive_ty.clone()),
|
||||
range,
|
||||
});
|
||||
|
||||
// Motive with indices
|
||||
|
||||
let mut pats: Vec<Box<Pat>> = Vec::new();
|
||||
|
||||
let fields_spine: Vec<_> = rec
|
||||
.fields
|
||||
.iter()
|
||||
.map(|(name, _, typ)| (name.clone(), typ.clone()))
|
||||
.collect();
|
||||
|
||||
let params_spine: Vec<_> = rec
|
||||
.parameters
|
||||
.iter()
|
||||
.map(|arg| {
|
||||
(
|
||||
arg.name.clone(),
|
||||
arg.typ.clone().unwrap_or_else(|| typ(arg.range.clone())),
|
||||
)
|
||||
})
|
||||
.collect();
|
||||
|
||||
let spine = [params_spine.as_slice(), fields_spine.as_slice()].concat();
|
||||
|
||||
pats.push(Box::new(Pat {
|
||||
data: concrete::pat::PatKind::App(
|
||||
rec.name.add_segment(rec.constructor.to_str()),
|
||||
spine
|
||||
.iter()
|
||||
.cloned()
|
||||
.map(|(name, _)| mk_pat_var(name))
|
||||
.collect(),
|
||||
),
|
||||
range,
|
||||
}));
|
||||
|
||||
let mut entries = vec![];
|
||||
|
||||
let mut cons_name = rec.name.add_segment(rec.constructor.to_str());
|
||||
|
||||
cons_name.range = rec.constructor.range;
|
||||
|
||||
for (i, (arg, cons_typ)) in fields_spine.iter().enumerate() {
|
||||
let mut types = types.clone();
|
||||
|
||||
let place = rec.parameters.len() + i;
|
||||
|
||||
types.push(Argument {
|
||||
hidden: false,
|
||||
erased: false,
|
||||
name: Ident::generate("set"),
|
||||
typ: Some(cons_typ.clone()),
|
||||
range,
|
||||
});
|
||||
|
||||
let new_var = Ident::generate("_new_var");
|
||||
|
||||
let mut pats = pats.clone();
|
||||
|
||||
pats.push(Box::new(Pat {
|
||||
data: concrete::pat::PatKind::Var(PatIdent(new_var.clone())),
|
||||
range,
|
||||
}));
|
||||
|
||||
let mut args: Vec<_> = spine
|
||||
.iter()
|
||||
.cloned()
|
||||
.map(|x| Binding::Positional(mk_var(x.0)))
|
||||
.collect();
|
||||
|
||||
args[place] = Binding::Positional(mk_var(new_var));
|
||||
|
||||
let body = Box::new(Expr {
|
||||
data: ExprKind::Constr {
|
||||
name: cons_name.clone(),
|
||||
args,
|
||||
},
|
||||
range,
|
||||
});
|
||||
|
||||
let mut name = rec.name.add_segment(arg.to_str()).add_segment("set");
|
||||
|
||||
name.range = rec.constructor.range;
|
||||
|
||||
let rules = vec![Box::new(Rule {
|
||||
name: name.clone(),
|
||||
pats: pats.clone(),
|
||||
body,
|
||||
range: rec.constructor.range,
|
||||
})];
|
||||
|
||||
let entry = Entry {
|
||||
name: name.clone(),
|
||||
docs: Vec::new(),
|
||||
args: types.clone(),
|
||||
typ: res_motive_ty.clone(),
|
||||
rules,
|
||||
range: rec.constructor.range,
|
||||
attrs: Vec::new(),
|
||||
generated_by: Some(rec.name.to_string().clone()),
|
||||
};
|
||||
|
||||
entries.push(entry)
|
||||
}
|
||||
|
||||
entries
|
||||
}
|
@ -40,7 +40,7 @@ impl Diagnostic for DriverError {
|
||||
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()
|
||||
"Take a look at the rules for name searching at https://github.com/Kindelia/Kind2/blob/master/guide/naming.md".to_string()
|
||||
}],
|
||||
positions: idents
|
||||
.iter()
|
||||
@ -61,7 +61,7 @@ impl Diagnostic for DriverError {
|
||||
.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()],
|
||||
hints: vec!["Take a look at the rules for name searching at https://github.com/Kindelia/Kind2/blob/master/guide/naming.md".to_string()],
|
||||
positions: vec![Marker {
|
||||
position: ident.range,
|
||||
color: Color::Fst,
|
||||
@ -75,7 +75,7 @@ impl Diagnostic for DriverError {
|
||||
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://github.com/Kindelia/Kind2/blob/master/guide/naming.md".to_string()],
|
||||
positions: vec![
|
||||
Marker {
|
||||
position: fst.range,
|
||||
|
@ -21,7 +21,11 @@ impl FileCache for Session {
|
||||
}
|
||||
}
|
||||
|
||||
pub fn type_check_book(session: &mut Session, path: &PathBuf) -> Option<untyped::Book> {
|
||||
pub fn type_check_book(
|
||||
session: &mut Session,
|
||||
path: &PathBuf,
|
||||
entrypoints: Vec<String>,
|
||||
) -> Option<untyped::Book> {
|
||||
let concrete_book = to_book(session, path)?;
|
||||
let desugared_book = desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)?;
|
||||
|
||||
@ -33,7 +37,11 @@ pub fn type_check_book(session: &mut Session, path: &PathBuf) -> Option<untyped:
|
||||
return None;
|
||||
}
|
||||
|
||||
let mut book = erasure::erase_book(&desugared_book, session.diagnostic_sender.clone())?;
|
||||
let mut book = erasure::erase_book(
|
||||
&desugared_book,
|
||||
session.diagnostic_sender.clone(),
|
||||
entrypoints,
|
||||
)?;
|
||||
inline_book(&mut book);
|
||||
|
||||
Some(book)
|
||||
@ -53,10 +61,18 @@ pub fn to_book(session: &mut Session, path: &PathBuf) -> Option<concrete::Book>
|
||||
Some(concrete_book)
|
||||
}
|
||||
|
||||
pub fn erase_book(session: &mut Session, path: &PathBuf) -> Option<untyped::Book> {
|
||||
pub fn erase_book(
|
||||
session: &mut Session,
|
||||
path: &PathBuf,
|
||||
entrypoints: Vec<String>,
|
||||
) -> Option<untyped::Book> {
|
||||
let concrete_book = to_book(session, path)?;
|
||||
let desugared_book = desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)?;
|
||||
let mut book = erasure::erase_book(&desugared_book, session.diagnostic_sender.clone())?;
|
||||
let mut book = erasure::erase_book(
|
||||
&desugared_book,
|
||||
session.diagnostic_sender.clone(),
|
||||
entrypoints,
|
||||
)?;
|
||||
inline_book(&mut book);
|
||||
Some(book)
|
||||
}
|
||||
@ -73,18 +89,23 @@ pub fn check_erasure_book(session: &mut Session, path: &PathBuf) -> Option<desug
|
||||
Some(desugared_book)
|
||||
}
|
||||
|
||||
pub fn compile_book_to_hvm(book: untyped::Book) -> backend::File {
|
||||
kind_target_hvm::compile_book(book)
|
||||
pub fn compile_book_to_hvm(book: untyped::Book, trace: bool) -> backend::File {
|
||||
kind_target_hvm::compile_book(book, trace)
|
||||
}
|
||||
|
||||
pub fn compile_book_to_kdl(
|
||||
path: &PathBuf,
|
||||
session: &mut Session,
|
||||
namespace: &str,
|
||||
entrypoints: Vec<String>,
|
||||
) -> Option<kind_target_kdl::File> {
|
||||
let concrete_book = to_book(session, path)?;
|
||||
let desugared_book = desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)?;
|
||||
let mut book = erasure::erase_book(&desugared_book, session.diagnostic_sender.clone())?;
|
||||
let mut book = erasure::erase_book(
|
||||
&desugared_book,
|
||||
session.diagnostic_sender.clone(),
|
||||
entrypoints,
|
||||
)?;
|
||||
|
||||
inline_book(&mut book);
|
||||
|
||||
|
@ -100,7 +100,7 @@ impl Diagnostic for SyntaxDiagnostic {
|
||||
severity: Severity::Warning,
|
||||
title: "This entire documentation comment is in a invalid position".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec!["Take a look at the rules for doc comments at https://kind.kindelia.org/hints/documentation-strings".to_string()],
|
||||
hints: vec!["Take a look at the rules for doc comments at https://github.com/Kindelia/Kind2/blob/master/guide/doc_strings.md".to_string()],
|
||||
positions: vec![Marker {
|
||||
position: *range,
|
||||
color: Color::For,
|
||||
|
@ -380,23 +380,10 @@ impl<'a> Parser<'a> {
|
||||
let range = self.range();
|
||||
self.advance(); // '('
|
||||
let mut expr = self.parse_expr(true)?;
|
||||
if self.get().same_variant(&Token::ColonColon) {
|
||||
self.advance(); // ':'
|
||||
let typ = self.parse_expr(false)?;
|
||||
let range = range.mix(self.range());
|
||||
|
||||
self.eat_closing_keyword(Token::RPar, range)?;
|
||||
|
||||
Ok(Box::new(Expr {
|
||||
data: ExprKind::Ann { val: expr, typ },
|
||||
range,
|
||||
}))
|
||||
} else {
|
||||
let end = self.range();
|
||||
self.eat_closing_keyword(Token::RPar, range)?;
|
||||
expr.range = range.mix(end);
|
||||
Ok(expr)
|
||||
}
|
||||
let end = self.range();
|
||||
self.eat_closing_keyword(Token::RPar, range)?;
|
||||
expr.range = range.mix(end);
|
||||
Ok(expr)
|
||||
}
|
||||
}
|
||||
|
||||
@ -530,26 +517,43 @@ impl<'a> Parser<'a> {
|
||||
}
|
||||
|
||||
fn parse_arrow(&mut self, multiline: bool) -> Result<Box<Expr>, SyntaxDiagnostic> {
|
||||
let mut typ = self.parse_call(multiline)?;
|
||||
let mut expr = self.parse_call(multiline)?;
|
||||
|
||||
while self.check_and_eat(Token::RightArrow) {
|
||||
let body = self.parse_expr(false)?;
|
||||
let range = typ.range.mix(body.range);
|
||||
typ = Box::new(Expr {
|
||||
let range = expr.range.mix(body.range);
|
||||
expr = Box::new(Expr {
|
||||
data: ExprKind::All {
|
||||
param: None,
|
||||
typ,
|
||||
typ: expr,
|
||||
body,
|
||||
erased: false,
|
||||
},
|
||||
range,
|
||||
});
|
||||
}
|
||||
Ok(typ)
|
||||
|
||||
Ok(expr)
|
||||
}
|
||||
|
||||
fn parse_ann(&mut self, multiline: bool) -> Result<Box<Expr>, SyntaxDiagnostic> {
|
||||
let expr = self.parse_arrow(multiline)?;
|
||||
|
||||
if self.check_and_eat(Token::ColonColon) {
|
||||
let typ = self.parse_arrow(multiline)?;
|
||||
let range = expr.range.mix(typ.range);
|
||||
Ok(Box::new(Expr {
|
||||
data: ExprKind::Ann { val: expr, typ },
|
||||
range,
|
||||
}))
|
||||
} else {
|
||||
Ok(expr)
|
||||
}
|
||||
}
|
||||
|
||||
fn parse_ask(&mut self) -> Result<Box<Sttm>, SyntaxDiagnostic> {
|
||||
let start = self.range();
|
||||
self.advance();
|
||||
self.advance(); // 'ask'
|
||||
let name = self.parse_destruct()?;
|
||||
self.eat_variant(Token::Eq)?;
|
||||
let expr = self.parse_expr(false)?;
|
||||
@ -607,9 +611,9 @@ impl<'a> Parser<'a> {
|
||||
|
||||
fn parse_sttm(&mut self) -> Result<Box<Sttm>, SyntaxDiagnostic> {
|
||||
let start = self.range();
|
||||
if self.check_actual_id("ask") {
|
||||
if self.check_actual(Token::Ask) {
|
||||
self.parse_ask()
|
||||
} else if self.check_actual_id("return") {
|
||||
} else if self.check_actual(Token::Return) {
|
||||
self.parse_return()
|
||||
} else if self.check_actual_id("let") {
|
||||
self.parse_monadic_let()
|
||||
@ -825,7 +829,7 @@ impl<'a> Parser<'a> {
|
||||
} else if self.check_actual(Token::Tilde) {
|
||||
self.parse_erased()
|
||||
} else {
|
||||
self.parse_arrow(multiline)
|
||||
self.parse_ann(multiline)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -50,7 +50,11 @@ impl<'a> Lexer<'a> {
|
||||
}
|
||||
|
||||
pub fn to_keyword(data: &str) -> Token {
|
||||
Token::LowerId(data.to_string())
|
||||
match data {
|
||||
"return" => Token::Return,
|
||||
"ask" => Token::Ask,
|
||||
_ => Token::LowerId(data.to_string()),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn get_next_no_error(&mut self, vec: Sender<Box<dyn Diagnostic>>) -> (Token, Range) {
|
||||
|
@ -29,13 +29,16 @@ pub enum Token {
|
||||
LowerId(String),
|
||||
UpperId(String, Option<String>),
|
||||
|
||||
// Strong keywords because they lead to better
|
||||
// error messages.
|
||||
Return,
|
||||
Ask,
|
||||
|
||||
// Keywords
|
||||
// Do,
|
||||
// If,
|
||||
// Else,
|
||||
// Match,
|
||||
// Ask,
|
||||
// Return,
|
||||
// Let,
|
||||
// Type,
|
||||
// Record,
|
||||
@ -166,9 +169,11 @@ impl fmt::Display for Token {
|
||||
Token::Bang => write!(f, "!"),
|
||||
Token::HashHash => write!(f, "##"),
|
||||
Token::Hash => write!(f, "#"),
|
||||
Token::Comment(_, _) => write!(f, "Comment"),
|
||||
Token::Comment(_, _) => write!(f, "docstring comment"),
|
||||
Token::Eof => write!(f, "End of file"),
|
||||
Token::Error(_) => write!(f, "ERROR"),
|
||||
Token::Return => write!(f, "return"),
|
||||
Token::Ask => write!(f, "ask"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -13,4 +13,4 @@ kind-derive = { path = "../kind-derive" }
|
||||
|
||||
linked-hash-map = "0.5.6"
|
||||
fxhash = "0.2.1"
|
||||
im = "15.1.0"
|
||||
im-rc = "15.1.0"
|
@ -1,3 +1,4 @@
|
||||
use kind_span::Locatable;
|
||||
use kind_tree::concrete::{self, Attribute, AttributeStyle};
|
||||
use kind_tree::Attributes;
|
||||
|
||||
@ -43,6 +44,11 @@ impl<'a> DesugarState<'a> {
|
||||
self.attr_without_value(attr);
|
||||
attributes.inlined = true;
|
||||
}
|
||||
"keep" => {
|
||||
self.args_should_be_empty(attr);
|
||||
self.attr_without_value(attr);
|
||||
attributes.keep = true;
|
||||
}
|
||||
"kdl_run" => {
|
||||
self.args_should_be_empty(attr);
|
||||
self.attr_without_value(attr);
|
||||
@ -73,6 +79,23 @@ impl<'a> DesugarState<'a> {
|
||||
None => self.attr_expects_a_value(attr),
|
||||
}
|
||||
}
|
||||
"trace" => {
|
||||
self.args_should_be_empty(attr);
|
||||
match &attr.value {
|
||||
Some(AttributeStyle::Ident(_, id)) if id.to_string() == "true" => {
|
||||
attributes.trace = Some(true);
|
||||
}
|
||||
Some(AttributeStyle::Ident(_, id)) if id.to_string() == "false" => {
|
||||
attributes.trace = Some(false);
|
||||
}
|
||||
Some(other) => {
|
||||
self.send_err(PassError::InvalidAttributeArgument(other.locate()))
|
||||
}
|
||||
None => {
|
||||
attributes.trace = Some(false);
|
||||
}
|
||||
}
|
||||
}
|
||||
_ => self.send_err(PassError::AttributeDoesNotExists(attr.range)),
|
||||
}
|
||||
}
|
||||
|
@ -197,11 +197,11 @@ impl<'a> DesugarState<'a> {
|
||||
if let Some((range, _, _)) = cases_args[index] {
|
||||
self.send_err(PassError::DuplicatedNamed(range, case.constructor.range));
|
||||
} else {
|
||||
let sum_c = &sum.constructors[index];
|
||||
let sum_constructor = &sum.constructors[index];
|
||||
|
||||
let ordered = self.order_case_arguments(
|
||||
(&case.constructor.range, case.constructor.to_string()),
|
||||
&sum_c
|
||||
&sum_constructor
|
||||
.args
|
||||
.iter()
|
||||
.map(|x| (x.name.to_string(), x.hidden))
|
||||
|
@ -140,8 +140,8 @@ impl<'a> DesugarState<'a> {
|
||||
let bind_ident = typ.add_segment("bind");
|
||||
let pure_ident = typ.add_segment("pure");
|
||||
|
||||
let bind = self.old_book.entries.get(bind_ident.to_string().as_str());
|
||||
let pure = self.old_book.entries.get(pure_ident.to_string().as_str());
|
||||
let bind = self.old_book.names.get(bind_ident.to_str());
|
||||
let pure = self.old_book.names.get(pure_ident.to_str());
|
||||
|
||||
if bind.is_none() || pure.is_none() {
|
||||
self.send_err(PassError::NeedToImplementMethods(range, Sugar::DoNotation));
|
||||
@ -186,9 +186,9 @@ impl<'a> DesugarState<'a> {
|
||||
let cons_ident = list_ident.add_segment("cons");
|
||||
let nil_ident = list_ident.add_segment("nil");
|
||||
|
||||
let list = self.old_book.entries.get(list_ident.to_string().as_str());
|
||||
let nil = self.old_book.entries.get(cons_ident.to_string().as_str());
|
||||
let cons = self.old_book.entries.get(nil_ident.to_string().as_str());
|
||||
let list = self.old_book.names.get(list_ident.to_str());
|
||||
let nil = self.old_book.names.get(cons_ident.to_str());
|
||||
let cons = self.old_book.names.get(nil_ident.to_str());
|
||||
|
||||
if list.is_none() || nil.is_none() || cons.is_none() {
|
||||
self.send_err(PassError::NeedToImplementMethods(range, Sugar::List));
|
||||
@ -214,10 +214,7 @@ impl<'a> DesugarState<'a> {
|
||||
let boolean = QualifiedIdent::new_static("Bool", None, range);
|
||||
let bool_if_ident = boolean.add_segment("if");
|
||||
|
||||
let bool_if = self
|
||||
.old_book
|
||||
.entries
|
||||
.get(bool_if_ident.to_string().as_str());
|
||||
let bool_if = self.old_book.names.get(bool_if_ident.to_str());
|
||||
|
||||
if bool_if.is_none() {
|
||||
self.send_err(PassError::NeedToImplementMethods(range, Sugar::BoolIf));
|
||||
|
@ -29,7 +29,6 @@ pub struct DesugarState<'a> {
|
||||
pub old_book: &'a concrete::Book,
|
||||
pub new_book: desugared::Book,
|
||||
pub name_count: u64,
|
||||
pub holes: u64,
|
||||
pub failed: bool,
|
||||
}
|
||||
|
||||
@ -42,7 +41,6 @@ pub fn desugar_book(
|
||||
old_book: book,
|
||||
new_book: Default::default(),
|
||||
name_count: 0,
|
||||
holes: 0,
|
||||
failed: false,
|
||||
};
|
||||
state.desugar_book(book);
|
||||
@ -55,8 +53,8 @@ pub fn desugar_book(
|
||||
|
||||
impl<'a> DesugarState<'a> {
|
||||
fn gen_hole(&mut self) -> u64 {
|
||||
self.holes += 1;
|
||||
self.holes - 1
|
||||
self.new_book.holes += 1;
|
||||
self.new_book.holes - 1
|
||||
}
|
||||
|
||||
fn gen_name(&mut self, range: Range) -> Ident {
|
||||
|
@ -5,7 +5,7 @@ use kind_report::data::Diagnostic;
|
||||
use kind_span::Range;
|
||||
|
||||
use kind_tree::desugared;
|
||||
use kind_tree::symbol::{Ident, QualifiedIdent};
|
||||
use kind_tree::symbol::QualifiedIdent;
|
||||
use kind_tree::untyped::{self};
|
||||
|
||||
use crate::errors::PassError;
|
||||
@ -45,7 +45,7 @@ pub struct ErasureState<'a> {
|
||||
edges: Vec<Edge>,
|
||||
names: FxHashMap<String, (Range, usize)>,
|
||||
|
||||
ctx: im::HashMap<String, Relevance>,
|
||||
ctx: im_rc::HashMap<String, Relevance>,
|
||||
|
||||
failed: bool,
|
||||
}
|
||||
@ -53,6 +53,7 @@ pub struct ErasureState<'a> {
|
||||
pub fn erase_book<'a>(
|
||||
book: &'a desugared::Book,
|
||||
errs: Sender<Box<dyn Diagnostic>>,
|
||||
entrypoints: Vec<String>,
|
||||
) -> Option<untyped::Book> {
|
||||
let mut state = ErasureState {
|
||||
errs,
|
||||
@ -63,7 +64,7 @@ pub fn erase_book<'a>(
|
||||
failed: Default::default(),
|
||||
};
|
||||
|
||||
state.erase_book(book)
|
||||
state.erase_book(book, entrypoints)
|
||||
}
|
||||
|
||||
impl<'a> ErasureState<'a> {
|
||||
@ -94,15 +95,21 @@ impl<'a> ErasureState<'a> {
|
||||
entry.push((name.range, ambient))
|
||||
}
|
||||
|
||||
pub fn erase_book(&mut self, book: &'a desugared::Book) -> Option<untyped::Book> {
|
||||
pub fn erase_book(
|
||||
&mut self,
|
||||
book: &'a desugared::Book,
|
||||
named_entrypoints: Vec<String>,
|
||||
) -> Option<untyped::Book> {
|
||||
let mut vals = FxHashMap::default();
|
||||
|
||||
let mut entrypoints = Vec::new();
|
||||
|
||||
if let Some(entr) = book.entrs.get("Main") {
|
||||
let id = self.get_edge_or_create(&entr.name);
|
||||
self.set_relevance(id, Relevance::Relevant, entr.name.range);
|
||||
entrypoints.push(id);
|
||||
for name in named_entrypoints {
|
||||
if let Some(entr) = book.entrs.get(&name) {
|
||||
let id = self.get_edge_or_create(&entr.name);
|
||||
self.set_relevance(id, Relevance::Relevant, entr.name.range);
|
||||
entrypoints.push(id);
|
||||
}
|
||||
}
|
||||
|
||||
// Kdl specific things.
|
||||
@ -115,7 +122,7 @@ impl<'a> ErasureState<'a> {
|
||||
}
|
||||
}
|
||||
|
||||
if entr.attrs.kdl_run {
|
||||
if entr.attrs.kdl_run || entr.attrs.keep {
|
||||
let id = self.get_edge_or_create(&entr.name);
|
||||
self.set_relevance(id, Relevance::Relevant, entr.name.range);
|
||||
entrypoints.push(id);
|
||||
@ -141,7 +148,7 @@ impl<'a> ErasureState<'a> {
|
||||
while !queue.is_empty() {
|
||||
let (fst, relev) = queue.pop().unwrap();
|
||||
|
||||
if visited.contains(&fst) {
|
||||
if visited.contains(fst) {
|
||||
continue;
|
||||
}
|
||||
|
||||
@ -157,13 +164,15 @@ impl<'a> ErasureState<'a> {
|
||||
}
|
||||
}
|
||||
|
||||
let entry = vals.get(&edge.name).cloned().unwrap();
|
||||
let entry = vals.remove(&edge.name).unwrap();
|
||||
|
||||
new_book
|
||||
.names
|
||||
.insert(entry.name.to_string(), new_book.entrs.len());
|
||||
.insert(entry.name.to_str().to_string(), new_book.entrs.len());
|
||||
|
||||
new_book.entrs.insert(entry.name.to_string(), entry);
|
||||
new_book
|
||||
.entrs
|
||||
.insert(entry.name.to_str().to_string(), entry);
|
||||
|
||||
for (to, relevs) in &edge.connections {
|
||||
for (_, relev) in relevs.iter() {
|
||||
@ -196,7 +205,7 @@ impl<'a> ErasureState<'a> {
|
||||
for arg in &entry.args {
|
||||
self.erase_expr(Ambient::Irrelevant, id, &arg.typ);
|
||||
self.ctx.insert(arg.name.to_string(), Relevance::Irrelevant);
|
||||
if !arg.hidden {
|
||||
if !arg.erased {
|
||||
args.push((arg.name.to_string(), arg.range, false))
|
||||
}
|
||||
}
|
||||
@ -246,7 +255,7 @@ impl<'a> ErasureState<'a> {
|
||||
.pats
|
||||
.iter()
|
||||
.zip(&entr.args)
|
||||
.map(|(pat, arg)| (self.erase_pat(relev(arg.hidden), edge, pat), arg))
|
||||
.map(|(pat, arg)| (self.erase_pat(relev(arg.erased), edge, pat), arg))
|
||||
.filter(|(_, arg)| !arg.erased)
|
||||
.map(|res| res.0)
|
||||
.collect::<Vec<_>>();
|
||||
@ -292,7 +301,7 @@ impl<'a> ErasureState<'a> {
|
||||
|
||||
untyped::Expr::var(name.clone())
|
||||
}
|
||||
Hole { num } => untyped::Expr::var(Ident::generate(&format!("_x{}", num))),
|
||||
Hole { num: _ } => untyped::Expr::err(expr.range),
|
||||
Fun { name, args } => {
|
||||
self.connect_with(edge, name, relevance);
|
||||
|
||||
@ -307,8 +316,8 @@ impl<'a> ErasureState<'a> {
|
||||
let args = args
|
||||
.iter()
|
||||
.zip(¶ms.args)
|
||||
.map(|(arg, param)| (self.erase_pat(relev(param.hidden), edge, arg), param))
|
||||
.filter(|(_, param)| !param.hidden)
|
||||
.map(|(arg, param)| (self.erase_pat(relev(param.erased), edge, arg), param))
|
||||
.filter(|(_, param)| !param.erased)
|
||||
.map(|x| x.0)
|
||||
.collect::<Vec<_>>();
|
||||
|
||||
@ -328,8 +337,8 @@ impl<'a> ErasureState<'a> {
|
||||
let args = args
|
||||
.iter()
|
||||
.zip(¶ms.args)
|
||||
.map(|(arg, param)| (self.erase_pat(relev(param.hidden), edge, arg), param))
|
||||
.filter(|(_, param)| !param.hidden)
|
||||
.map(|(arg, param)| (self.erase_pat(relev(param.erased), edge, arg), param))
|
||||
.filter(|(_, param)| !param.erased)
|
||||
.map(|x| x.0)
|
||||
.collect::<Vec<_>>();
|
||||
|
||||
@ -461,7 +470,7 @@ impl<'a> ErasureState<'a> {
|
||||
let var_rev = self
|
||||
.ctx
|
||||
.get(&name.to_string())
|
||||
.expect(&format!("Uwnraping {}", name.to_string()));
|
||||
.expect(&format!("Uwnraping {}", name));
|
||||
|
||||
if *var_rev == Relevance::Irrelevant && ambient != Ambient::Irrelevant {
|
||||
self.set_relevance(edge, Relevance::Irrelevant, name.range)
|
||||
@ -499,7 +508,7 @@ impl<'a> ErasureState<'a> {
|
||||
untyped::Expr::binary(expr.range, *op, left, right)
|
||||
}
|
||||
Typ | NumTypeU60 { .. } | NumTypeF60 { .. } | Hole { .. } | Hlp(_) | Err => {
|
||||
if ambient != Ambient::Irrelevant && ambient != Ambient::Irrelevant {
|
||||
if ambient != Ambient::Irrelevant {
|
||||
self.set_relevance(edge, Relevance::Irrelevant, expr.range);
|
||||
}
|
||||
untyped::Expr::err(expr.range)
|
||||
|
@ -89,7 +89,7 @@ impl Diagnostic for PassError {
|
||||
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()
|
||||
"Take a look at naming rules at https://github.com/Kindelia/Kind2/blob/master/guide/naming.md".to_string()
|
||||
}],
|
||||
positions: idents
|
||||
.iter()
|
||||
@ -324,7 +324,7 @@ impl Diagnostic for PassError {
|
||||
title: "Incorrect arity in the sugar definition".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![format!(
|
||||
"Take a look at how sugar functions should be implemented at https://kind2.kindelia.com/hints/sugars."
|
||||
"Take a look at how sugar functions should be implemented at https://github.com/Kindelia/Kind2/blob/master/guide/sugars.md"
|
||||
)],
|
||||
positions: vec![
|
||||
Marker {
|
||||
|
@ -6,8 +6,10 @@ use std::fmt::Display;
|
||||
use std::sync::mpsc::Sender;
|
||||
|
||||
use fxhash::FxHashMap;
|
||||
use kind_derive::getters::derive_getters;
|
||||
use kind_derive::matching::derive_match;
|
||||
use kind_derive::open::derive_open;
|
||||
use kind_derive::setters::derive_setters;
|
||||
use kind_report::data::Diagnostic;
|
||||
use kind_span::Locatable;
|
||||
use kind_span::Range;
|
||||
@ -23,6 +25,8 @@ pub mod uses;
|
||||
pub enum Derive {
|
||||
Match,
|
||||
Open,
|
||||
Getters,
|
||||
Setters
|
||||
}
|
||||
|
||||
impl Display for Derive {
|
||||
@ -30,6 +34,8 @@ impl Display for Derive {
|
||||
match self {
|
||||
Derive::Match => write!(f, "match"),
|
||||
Derive::Open => write!(f, "open"),
|
||||
Derive::Getters => write!(f, "getters"),
|
||||
Derive::Setters => write!(f, "setters"),
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -44,7 +50,7 @@ pub fn insert_or_report(
|
||||
Some(last_range) => {
|
||||
channel
|
||||
.send(Box::new(PassError::DuplicatedAttributeArgument(
|
||||
last_range.clone(),
|
||||
*last_range,
|
||||
range,
|
||||
)))
|
||||
.unwrap();
|
||||
@ -59,6 +65,8 @@ fn string_to_derive(name: &str) -> Option<Derive> {
|
||||
match name {
|
||||
"match" => Some(Derive::Match),
|
||||
"open" => Some(Derive::Open),
|
||||
"getters" => Some(Derive::Getters),
|
||||
"setters" => Some(Derive::Setters),
|
||||
_ => None,
|
||||
}
|
||||
}
|
||||
@ -89,7 +97,7 @@ pub fn expand_derive(
|
||||
match arg {
|
||||
Ident(range, ident) => match string_to_derive(ident.to_str()) {
|
||||
Some(key) => {
|
||||
insert_or_report(error_channel.clone(), &mut def, key, range.clone())
|
||||
insert_or_report(error_channel.clone(), &mut def, key, *range)
|
||||
}
|
||||
_ => {
|
||||
error_channel
|
||||
@ -160,6 +168,18 @@ pub fn expand_book(error_channel: Sender<Box<dyn Diagnostic>>, book: &mut Book)
|
||||
let info = res.extract_book_info();
|
||||
entries.insert(res.name.to_string(), (res, info));
|
||||
}
|
||||
Derive::Getters => {
|
||||
for res in derive_getters(rec.name.range, rec) {
|
||||
let info = res.extract_book_info();
|
||||
entries.insert(res.name.to_string(), (res, info));
|
||||
}
|
||||
}
|
||||
Derive::Setters => {
|
||||
for res in derive_setters(rec.name.range, rec) {
|
||||
let info = res.extract_book_info();
|
||||
entries.insert(res.name.to_string(), (res, info));
|
||||
}
|
||||
}
|
||||
other => {
|
||||
error_channel
|
||||
.send(Box::new(PassError::CannotDerive(other.to_string(), val)))
|
||||
|
@ -19,12 +19,12 @@ impl Visitor for Expand {
|
||||
if ident.get_aux().is_none() {
|
||||
return;
|
||||
}
|
||||
let alias = match self.names.get(&ident.get_root().to_string()) {
|
||||
let alias = match self.names.get(&ident.get_root()) {
|
||||
Some(path) => path,
|
||||
None => {
|
||||
self.errors
|
||||
.send(Box::new(PassError::CannotFindAlias(
|
||||
ident.get_root().to_string(),
|
||||
ident.get_root(),
|
||||
ident.range,
|
||||
)))
|
||||
.unwrap();
|
||||
|
@ -37,7 +37,7 @@ pub fn inline_book(book: &mut untyped::Book) {
|
||||
|
||||
for entr in book.entrs.values() {
|
||||
if entr.attrs.inlined {
|
||||
if let Some(inlinable) = inlinable(&entr) {
|
||||
if let Some(inlinable) = inlinable(entr) {
|
||||
funs.insert(entr.name.to_string(), inlinable);
|
||||
to_remove.push(entr.name.to_string());
|
||||
}
|
||||
|
@ -117,7 +117,6 @@ impl UnboundCollector {
|
||||
self.top_level_defs
|
||||
.insert(name_cons.get_root(), name_cons.range);
|
||||
}
|
||||
|
||||
TopLevel::Entry(entry) => {
|
||||
debug_assert!(entry.name.get_aux().is_none());
|
||||
self.top_level_defs
|
||||
@ -476,7 +475,7 @@ impl Visitor for UnboundCollector {
|
||||
self.context_vars.pop();
|
||||
}
|
||||
ExprKind::Match(matcher) => {
|
||||
self.visit_qualified_ident(&mut matcher.typ.add_segment("match"));
|
||||
self.visit_qualified_ident(&mut matcher.typ.add_segment("match").to_generated());
|
||||
self.visit_match(matcher)
|
||||
}
|
||||
ExprKind::Subst(subst) => {
|
||||
@ -499,27 +498,25 @@ impl Visitor for UnboundCollector {
|
||||
self.visit_sttm(sttm)
|
||||
}
|
||||
ExprKind::If { cond, then_, else_ } => {
|
||||
self.visit_qualified_ident(&mut QualifiedIdent::new_sugared(
|
||||
"Bool", "if", expr.range,
|
||||
));
|
||||
let typ = QualifiedIdent::new_static("Bool", None, expr.range);
|
||||
self.visit_qualified_ident(&mut typ.add_segment("if").to_generated());
|
||||
self.visit_expr(cond);
|
||||
self.visit_expr(then_);
|
||||
self.visit_expr(else_);
|
||||
}
|
||||
ExprKind::Pair { fst, snd } => {
|
||||
self.visit_qualified_ident(&mut QualifiedIdent::new_sugared(
|
||||
"Pair", "new", expr.range,
|
||||
));
|
||||
let typ = QualifiedIdent::new_static("Pair", None, expr.range);
|
||||
self.visit_qualified_ident(&mut typ.add_segment("new").to_generated());
|
||||
self.visit_expr(fst);
|
||||
self.visit_expr(snd);
|
||||
}
|
||||
ExprKind::List { args } => {
|
||||
self.visit_qualified_ident(&mut QualifiedIdent::new_sugared(
|
||||
"List", "nil", expr.range,
|
||||
));
|
||||
self.visit_qualified_ident(&mut QualifiedIdent::new_sugared(
|
||||
"List", "cons", expr.range,
|
||||
));
|
||||
let mut typ = QualifiedIdent::new_static("List", None, expr.range);
|
||||
|
||||
self.visit_qualified_ident(&mut typ);
|
||||
self.visit_qualified_ident(&mut typ.add_segment("nil").to_generated());
|
||||
self.visit_qualified_ident(&mut typ.add_segment("cons").to_generated());
|
||||
|
||||
visit_vec!(args.iter_mut(), arg => self.visit_expr(arg));
|
||||
}
|
||||
}
|
||||
|
@ -3,7 +3,7 @@ use kind_tree::untyped::*;
|
||||
|
||||
pub struct Subst {
|
||||
vars: FxHashMap<String, Box<Expr>>,
|
||||
ctx: im::HashSet<String>,
|
||||
ctx: im_rc::HashSet<String>,
|
||||
}
|
||||
|
||||
pub fn subst_on_expr(expr: &mut Box<Expr>, vars: FxHashMap<String, Box<Expr>>) {
|
||||
@ -63,7 +63,7 @@ impl Subst {
|
||||
return;
|
||||
}
|
||||
if let Some(res) = self.vars.get(name.to_str()) {
|
||||
*expr = res.clone().clone();
|
||||
*expr = res.clone();
|
||||
}
|
||||
}
|
||||
Lambda { param, body, .. } => {
|
||||
|
@ -36,7 +36,7 @@ impl Diagnostic for DriverError {
|
||||
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()
|
||||
"Take a look at the rules for name searching at https://github.com/Kindelia/Kind2/blob/master/guide/naming.md".to_string()
|
||||
}],
|
||||
positions: idents
|
||||
.iter()
|
||||
@ -57,7 +57,7 @@ impl Diagnostic for DriverError {
|
||||
.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()],
|
||||
hints: vec!["Take a look at the rules for name searching at https://github.com/Kindelia/Kind2/blob/master/guide/naming.md".to_string()],
|
||||
positions: vec![Marker {
|
||||
position: ident.range,
|
||||
color: Color::Fst,
|
||||
@ -71,7 +71,7 @@ impl Diagnostic for DriverError {
|
||||
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://github.com/Kindelia/Kind2/blob/master/guide/naming.md".to_string()],
|
||||
positions: vec![
|
||||
Marker {
|
||||
position: fst.range,
|
||||
|
@ -5,17 +5,33 @@ use kind_tree::{
|
||||
untyped,
|
||||
};
|
||||
|
||||
pub fn compile_book(book: untyped::Book) -> File {
|
||||
pub fn compile_book(book: untyped::Book, trace: bool) -> File {
|
||||
let mut file = File {
|
||||
rules: Default::default(),
|
||||
smaps: Default::default(),
|
||||
};
|
||||
for (_, entry) in book.entrs {
|
||||
compile_entry(&mut file, *entry);
|
||||
compile_entry(&mut file, *entry, trace);
|
||||
}
|
||||
file
|
||||
}
|
||||
|
||||
pub fn compile_str(val: &str) -> Box<Term> {
|
||||
let nil = Box::new(Term::Ctr {
|
||||
name: String::from("String.nil"),
|
||||
args: vec![],
|
||||
});
|
||||
|
||||
let cons = |numb, next| {
|
||||
Box::new(Term::Ctr {
|
||||
name: String::from("String.cons"),
|
||||
args: vec![Box::new(Term::U6O { numb }), next],
|
||||
})
|
||||
};
|
||||
|
||||
val.chars().rfold(nil, |rest, chr| cons(chr as u64, rest))
|
||||
}
|
||||
|
||||
pub fn compile_term(expr: &untyped::Expr) -> Box<Term> {
|
||||
use untyped::ExprKind::*;
|
||||
match &expr.data {
|
||||
@ -49,38 +65,61 @@ pub fn compile_term(expr: &untyped::Expr) -> Box<Term> {
|
||||
name: op.to_string(),
|
||||
args: vec![compile_term(left), compile_term(right)],
|
||||
}),
|
||||
Str { val } => {
|
||||
let nil = Box::new(Term::Ctr {
|
||||
name: String::from("String.nil"),
|
||||
args: vec![],
|
||||
});
|
||||
|
||||
let cons = |numb, next| {
|
||||
Box::new(Term::Ctr {
|
||||
name: String::from("String.cons"),
|
||||
args: vec![Box::new(Term::U6O { numb }), next],
|
||||
})
|
||||
};
|
||||
|
||||
val.chars().rfold(nil, |rest, chr| cons(chr as u64, rest))
|
||||
}
|
||||
Str { val } => compile_str(val),
|
||||
Err => unreachable!("Internal Error: 'ERR' cannot be a relevant term"),
|
||||
}
|
||||
}
|
||||
|
||||
fn compile_rule(rule: untyped::Rule) -> Rule {
|
||||
fn compile_rule(name: String, rule: untyped::Rule) -> Rule {
|
||||
Rule {
|
||||
lhs: Box::new(Term::Ctr {
|
||||
name: rule.name.to_string(),
|
||||
name,
|
||||
args: rule.pats.iter().map(|x| compile_term(x)).collect(),
|
||||
}),
|
||||
rhs: compile_term(&rule.body),
|
||||
}
|
||||
}
|
||||
|
||||
fn compile_entry(file: &mut File, entry: untyped::Entry) {
|
||||
// TODO: Add optimizations for some functions?
|
||||
for rule in entry.rules {
|
||||
file.rules.push(compile_rule(rule))
|
||||
fn compile_entry(file: &mut File, entry: 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());
|
||||
for rule in entry.rules {
|
||||
file.rules.push(compile_rule(name_trace.clone(), rule))
|
||||
}
|
||||
|
||||
let args = entry
|
||||
.args
|
||||
.iter()
|
||||
.enumerate()
|
||||
.map(|(i, x)| {
|
||||
Box::new(Term::Var {
|
||||
name: format!("_{}{}", i, x.0.clone()),
|
||||
})
|
||||
})
|
||||
.collect::<Vec<_>>();
|
||||
|
||||
file.rules.push(Rule {
|
||||
lhs: Box::new(Term::Ctr {
|
||||
name: entry.name.to_string(),
|
||||
args: args.clone(),
|
||||
}),
|
||||
rhs: Box::new(Term::Ctr {
|
||||
name: "HVM.log".to_string(),
|
||||
args: vec![
|
||||
compile_str(entry.name.to_str()),
|
||||
Box::new(Term::Ctr {
|
||||
name: name_trace,
|
||||
args,
|
||||
}),
|
||||
],
|
||||
}),
|
||||
})
|
||||
} else {
|
||||
let name = entry.name.to_string();
|
||||
for rule in entry.rules {
|
||||
file.rules.push(compile_rule(name.clone(), rule))
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -22,6 +22,9 @@ pub fn compile_book(
|
||||
let flattened = flatten(book);
|
||||
|
||||
let file = compile::compile_book(&flattened, sender, namespace)?;
|
||||
|
||||
println!("{}", file);
|
||||
|
||||
let file = linearize::linearize_file(file);
|
||||
Some(file)
|
||||
}
|
||||
|
15
crates/kind-tests/Cargo.toml
Normal file
15
crates/kind-tests/Cargo.toml
Normal file
@ -0,0 +1,15 @@
|
||||
[package]
|
||||
name = "kind-tests"
|
||||
version = "0.1.0"
|
||||
edition = "2021"
|
||||
|
||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||
|
||||
[dependencies]
|
||||
kind-driver = { path = "../kind-driver" }
|
||||
kind-report = { path = "../kind-report" }
|
||||
kind-checker = { path = "../kind-checker" }
|
||||
kind-query = { path = "../kind-query" }
|
||||
pretty_assertions = "1.3.0"
|
||||
ntest = "0.8.1"
|
||||
walkdir = "2"
|
2
crates/kind-tests/Teste.kind2
Normal file
2
crates/kind-tests/Teste.kind2
Normal file
@ -0,0 +1,2 @@
|
||||
Main : U60
|
||||
Main = HVM.log 222 2
|
@ -41,10 +41,11 @@ fn test_kind2(path: &Path, run: fn(&Path) -> String) -> Result<(), Error> {
|
||||
fn test_checker() -> Result<(), Error> {
|
||||
test_kind2(Path::new("./tests/suite/checker"), |path| {
|
||||
let (rx, tx) = std::sync::mpsc::channel();
|
||||
let root = PathBuf::from(".");
|
||||
let root = PathBuf::from("./tests/suite/lib").canonicalize().unwrap();
|
||||
let mut session = Session::new(root, rx);
|
||||
|
||||
let check = driver::type_check_book(&mut session, &PathBuf::from(path));
|
||||
let entrypoints = vec!["Main".to_string()];
|
||||
let check = driver::type_check_book(&mut session, &PathBuf::from(path), entrypoints);
|
||||
|
||||
let diagnostics = tx.try_iter().collect::<Vec<Box<dyn Diagnostic>>>();
|
||||
let render = RenderConfig::ascii(2);
|
||||
@ -72,11 +73,12 @@ fn test_checker() -> Result<(), Error> {
|
||||
fn test_eval() -> Result<(), Error> {
|
||||
test_kind2(Path::new("./tests/suite/eval"), |path| {
|
||||
let (rx, tx) = std::sync::mpsc::channel();
|
||||
let root = PathBuf::from(".");
|
||||
let root = PathBuf::from("./tests/suite/lib").canonicalize().unwrap();
|
||||
let mut session = Session::new(root, rx);
|
||||
|
||||
let check =
|
||||
driver::erase_book(&mut session, &PathBuf::from(path)).map(driver::compile_book_to_hvm);
|
||||
let entrypoints = vec!["Main".to_string()];
|
||||
let check = driver::erase_book(&mut session, &PathBuf::from(path), entrypoints)
|
||||
.map(|x| driver::compile_book_to_hvm(x, false));
|
||||
|
||||
let diagnostics = tx.try_iter().collect::<Vec<_>>();
|
||||
let render = RenderConfig::ascii(2);
|
||||
@ -100,3 +102,38 @@ fn test_eval() -> Result<(), Error> {
|
||||
})?;
|
||||
Ok(())
|
||||
}
|
||||
|
||||
|
||||
#[test]
|
||||
#[timeout(15000)]
|
||||
fn test_kdl() -> Result<(), Error> {
|
||||
test_kind2(Path::new("./tests/suite/kdl"), |path| {
|
||||
let (rx, tx) = std::sync::mpsc::channel();
|
||||
let root = PathBuf::from("./tests/suite/lib").canonicalize().unwrap();
|
||||
let mut session = Session::new(root, rx);
|
||||
|
||||
let entrypoints = vec!["Main".to_string()];
|
||||
let check = driver::compile_book_to_kdl(&PathBuf::from(path), &mut session, "", entrypoints);
|
||||
|
||||
let diagnostics = tx.try_iter().collect::<Vec<_>>();
|
||||
let render = RenderConfig::ascii(2);
|
||||
|
||||
kind_report::check_if_colors_are_supported(true);
|
||||
|
||||
match check {
|
||||
Some(file) if diagnostics.is_empty() => {
|
||||
file.to_string()
|
||||
}
|
||||
_ => {
|
||||
let mut res_string = String::new();
|
||||
|
||||
for diag in diagnostics {
|
||||
diag.render(&mut session, &render, &mut res_string).unwrap();
|
||||
}
|
||||
|
||||
res_string
|
||||
}
|
||||
}
|
||||
})?;
|
||||
Ok(())
|
||||
}
|
11
crates/kind-tests/tests/suite/checker/derive/Algebra.golden
Normal file
11
crates/kind-tests/tests/suite/checker/derive/Algebra.golden
Normal file
@ -0,0 +1,11 @@
|
||||
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
|
||||
|
||||
|
41
crates/kind-tests/tests/suite/checker/derive/Algebra.kind2
Normal file
41
crates/kind-tests/tests/suite/checker/derive/Algebra.kind2
Normal file
@ -0,0 +1,41 @@
|
||||
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
|
@ -0,0 +1,12 @@
|
||||
Main : Maybe U60
|
||||
Main =
|
||||
do Maybe {
|
||||
Maybe.some 3
|
||||
Maybe.pure 2
|
||||
ask res = Maybe.pure 2
|
||||
ask res2 = Maybe.pure 3
|
||||
match Maybe (Maybe.some 4) {
|
||||
some val => Maybe.pure (+ 1000 (+ val (+ res res2)))
|
||||
none => Maybe.none
|
||||
}
|
||||
}
|
@ -0,0 +1,13 @@
|
||||
INFO Inspection.
|
||||
|
||||
* Expected: U60
|
||||
|
||||
|
||||
/--[tests/suite/checker/derive/Inspection.kind2:3:3]
|
||||
|
|
||||
2 | Main =
|
||||
3 | ?
|
||||
| v
|
||||
| \Here!
|
||||
|
||||
|
@ -0,0 +1,3 @@
|
||||
Main : U60
|
||||
Main =
|
||||
?
|
55
crates/kind-tests/tests/suite/checker/derive/Quicksort.kind2
Normal file
55
crates/kind-tests/tests/suite/checker/derive/Quicksort.kind2
Normal file
@ -0,0 +1,55 @@
|
||||
// From: https://github.com/Kindelia/Functional-Benchmarks/blob/master/Runtime/quicksort.kind2
|
||||
|
||||
type List (t: Type) {
|
||||
Cons (head: t) (tail: List t)
|
||||
Nil
|
||||
}
|
||||
|
||||
type Tree (t: Type) {
|
||||
Empty
|
||||
Single (value: t)
|
||||
Concat (left: Tree t) (right: Tree t)
|
||||
}
|
||||
|
||||
// Generates a random list
|
||||
Randoms (s: U60) (n: U60) : List U60
|
||||
Randoms s 0 = List.Nil
|
||||
Randoms s l = List.Cons s (Randoms (% (+ (* s 1664525) 1013904223) 4294967296) (- l 1))
|
||||
|
||||
// Sums all elements in a concatenation tree
|
||||
Sum (tree: Tree U60) : U60
|
||||
Sum (Tree.Empty t) = 0
|
||||
Sum (Tree.Single t a) = a
|
||||
Sum (Tree.Concat t a b) = (+ (Sum a) (Sum b))
|
||||
|
||||
//// The initial pivot
|
||||
Pivot : U60
|
||||
Pivot = 2147483648
|
||||
|
||||
QSort (p: U60) (s: U60) (l: List U60): Tree U60
|
||||
QSort p s List.Nil = Tree.Empty
|
||||
QSort p s (List.Cons x List.Nil) = Tree.Single x
|
||||
QSort p s (List.Cons x xs) = Split p s (List.Cons x xs) List.Nil List.Nil
|
||||
|
||||
//// Splits list in two partitions
|
||||
Split (p: U60) (s: U60) (l: List U60) (min: List U60) (max: List U60) : Tree U60
|
||||
Split p s List.Nil min max =
|
||||
let s = (>> s 1)
|
||||
let min = (QSort (- p s) s min)
|
||||
let max = (QSort (+ p s) s max)
|
||||
Tree.Concat min max
|
||||
|
||||
Split p s (List.Cons x xs) min max =
|
||||
Place p s (< p x) x xs min max
|
||||
|
||||
//// Moves element to its partition
|
||||
|
||||
Place (p: U60) (s: U60) (y: U60) (x: U60) (xs: List U60) (min: List U60) (max: List U60) : Tree U60
|
||||
Place p s 0 x xs min max = Split p s xs (List.Cons x min) max
|
||||
Place p s 1 x xs min max = Split p s xs min (List.Cons x max)
|
||||
|
||||
//// Sorts and sums n random numbers
|
||||
Main : U60
|
||||
Main =
|
||||
let list = Randoms 1 254
|
||||
Sum (QSort Pivot Pivot list)
|
1
crates/kind-tests/tests/suite/checker/derive/User.golden
Normal file
1
crates/kind-tests/tests/suite/checker/derive/User.golden
Normal file
@ -0,0 +1 @@
|
||||
Ok!
|
1
crates/kind-tests/tests/suite/checker/derive/Vec.golden
Normal file
1
crates/kind-tests/tests/suite/checker/derive/Vec.golden
Normal file
@ -0,0 +1 @@
|
||||
Ok!
|
@ -12,5 +12,5 @@
|
||||
| v-------
|
||||
| \Second occorrence here!
|
||||
|
||||
Hint: Rename one of the definitions or remove and look at how names work in Kind at https://kind.kindelia.org/hints/names
|
||||
Hint: Rename one of the definitions or remove and look at how names work in Kind at https://github.com/Kindelia/Kind2/blob/master/guide/naming.md
|
||||
|
1
crates/kind-tests/tests/suite/eval/DoNotation.golden
Normal file
1
crates/kind-tests/tests/suite/eval/DoNotation.golden
Normal file
@ -0,0 +1 @@
|
||||
(Maybe.some 1009)
|
12
crates/kind-tests/tests/suite/eval/DoNotation.kind2
Normal file
12
crates/kind-tests/tests/suite/eval/DoNotation.kind2
Normal file
@ -0,0 +1,12 @@
|
||||
Main : Maybe U60
|
||||
Main =
|
||||
do Maybe {
|
||||
Maybe.some 3
|
||||
Maybe.pure 2
|
||||
ask res = Maybe.pure 2
|
||||
ask res2 = Maybe.pure 3
|
||||
match Maybe (Maybe.some 4) {
|
||||
some val => Maybe.pure (+ 1000 (+ val (+ res res2)))
|
||||
none => Maybe.none
|
||||
}
|
||||
}
|
1
crates/kind-tests/tests/suite/eval/Getters.golden
Normal file
1
crates/kind-tests/tests/suite/eval/Getters.golden
Normal file
@ -0,0 +1 @@
|
||||
300
|
10
crates/kind-tests/tests/suite/eval/Getters.kind2
Normal file
10
crates/kind-tests/tests/suite/eval/Getters.kind2
Normal file
@ -0,0 +1,10 @@
|
||||
#derive[getters]
|
||||
record Pair (a: Type) (b: Type) {
|
||||
fst : a
|
||||
snd : b
|
||||
}
|
||||
|
||||
Main : U60
|
||||
Main =
|
||||
let a = (Pair.new 100 200 :: Pair U60 U60)
|
||||
(+ (Pair.fst.get a) (Pair.snd.get a))
|
13
crates/kind-tests/tests/suite/eval/NoMatch.golden
Normal file
13
crates/kind-tests/tests/suite/eval/NoMatch.golden
Normal file
@ -0,0 +1,13 @@
|
||||
ERROR Required functions are not implemented for this type.
|
||||
|
||||
/--[tests/suite/eval/NoMatch.kind2:3:5]
|
||||
|
|
||||
| /
|
||||
3 | | match NoMatch NoMatch.pudding {
|
||||
4 | | pudding => 2
|
||||
5 | | }
|
||||
: |
|
||||
: \ You cannot use this expression!
|
||||
|
||||
Hint: You must implement 'NoMatch.match' in order to use the match notation (or derive match with #derive[match]).
|
||||
|
5
crates/kind-tests/tests/suite/eval/NoMatch.kind2
Normal file
5
crates/kind-tests/tests/suite/eval/NoMatch.kind2
Normal file
@ -0,0 +1,5 @@
|
||||
Main : U60
|
||||
Main =
|
||||
match NoMatch NoMatch.pudding {
|
||||
pudding => 2
|
||||
}
|
1
crates/kind-tests/tests/suite/eval/Setters.golden
Normal file
1
crates/kind-tests/tests/suite/eval/Setters.golden
Normal file
@ -0,0 +1 @@
|
||||
700
|
12
crates/kind-tests/tests/suite/eval/Setters.kind2
Normal file
12
crates/kind-tests/tests/suite/eval/Setters.kind2
Normal file
@ -0,0 +1,12 @@
|
||||
#derive[getters, setters]
|
||||
record Pair (a: Type) (b: Type) {
|
||||
fst : a
|
||||
snd : b
|
||||
}
|
||||
|
||||
Main : U60
|
||||
Main =
|
||||
let a = (Pair.new 100 200 :: Pair U60 U60)
|
||||
let b = Pair.fst.set a 500
|
||||
let c = Pair.snd.set a (+ (Pair.fst.get b) (Pair.snd.get b))
|
||||
Pair.snd.get c
|
0
crates/kind-tests/tests/suite/kdl/ChangeName.golden
Normal file
0
crates/kind-tests/tests/suite/kdl/ChangeName.golden
Normal file
3
crates/kind-tests/tests/suite/kdl/ChangeName.kind2
Normal file
3
crates/kind-tests/tests/suite/kdl/ChangeName.kind2
Normal file
@ -0,0 +1,3 @@
|
||||
#kdl_name = JOJO
|
||||
Jonathan.Joestar : U60
|
||||
Jonathan.Joestar = 42
|
0
crates/kind-tests/tests/suite/kdl/Lambda.golden
Normal file
0
crates/kind-tests/tests/suite/kdl/Lambda.golden
Normal file
8
crates/kind-tests/tests/suite/kdl/Lambda.kind2
Normal file
8
crates/kind-tests/tests/suite/kdl/Lambda.kind2
Normal file
@ -0,0 +1,8 @@
|
||||
CoolFn : U60 -> U60 {
|
||||
(x: U60) => (* 2 x)
|
||||
}
|
||||
|
||||
CoolFnApp (n: U60) : U60 {
|
||||
let lam = (x: U60) => ((CoolFn) x)
|
||||
(lam n)
|
||||
}
|
1
crates/kind-tests/tests/suite/kdl/NonInlineState.golden
Normal file
1
crates/kind-tests/tests/suite/kdl/NonInlineState.golden
Normal file
@ -0,0 +1 @@
|
||||
ctr {MyFn.state}
|
6
crates/kind-tests/tests/suite/kdl/NonInlineState.kind2
Normal file
6
crates/kind-tests/tests/suite/kdl/NonInlineState.kind2
Normal file
@ -0,0 +1,6 @@
|
||||
#kdl_state = MyFn.state
|
||||
MyFn : U60 {
|
||||
1
|
||||
}
|
||||
|
||||
MyFn.state : U60
|
3
crates/kind-tests/tests/suite/kdl/Operators.golden
Normal file
3
crates/kind-tests/tests/suite/kdl/Operators.golden
Normal file
@ -0,0 +1,3 @@
|
||||
run {
|
||||
(& (+ #2 (& (- #3 (& (* #4 (/ #5 (% #6 (& (+ #2 (| #8 (^ #9 (<< #10 (% (>> #23 (% (< #2 (>= #4 (<= (== #4 #4) (> #3 (!= #5 #3))))) #60)) #60))))) #1152921504606846975)))) #1152921504606846975)) #1152921504606846975)) #1152921504606846975)
|
||||
}
|
18
crates/kind-tests/tests/suite/kdl/Operators.kind2
Normal file
18
crates/kind-tests/tests/suite/kdl/Operators.kind2
Normal file
@ -0,0 +1,18 @@
|
||||
#kdl_run
|
||||
Main : U60
|
||||
Main =
|
||||
(+ 2
|
||||
(- 3
|
||||
(* 4
|
||||
(/ 5
|
||||
(% 6
|
||||
(& 2
|
||||
(| 8
|
||||
(^ 9
|
||||
(<< 10
|
||||
(>> 23
|
||||
(< 2
|
||||
(>= 4
|
||||
(<= (== 4 4)
|
||||
(> 3
|
||||
(!= 5 3)))))))))))))))
|
14
crates/kind-tests/tests/suite/kdl/RemoveNames.kind2
Normal file
14
crates/kind-tests/tests/suite/kdl/RemoveNames.kind2
Normal file
@ -0,0 +1,14 @@
|
||||
List <a> : Type
|
||||
List.nil <a> : List
|
||||
List.cons <a> (head: a) (tail: List a) : List
|
||||
|
||||
/*
|
||||
#keep
|
||||
Ora.Ora.ora (h: List U60) : List U60
|
||||
Ora.Ora.ora (List.cons x xs) =
|
||||
let aaa = 2
|
||||
let bbb = 3
|
||||
let ccc = 4
|
||||
let ddd = (+ ccc bbb)
|
||||
List.cons aaa xs
|
||||
*/
|
10
crates/kind-tests/tests/suite/kdl/Run.golden
Normal file
10
crates/kind-tests/tests/suite/kdl/Run.golden
Normal file
@ -0,0 +1,10 @@
|
||||
fun (A ) {
|
||||
{A} = #2
|
||||
}
|
||||
|
||||
run {
|
||||
(A)
|
||||
}
|
||||
run {
|
||||
#4
|
||||
}
|
13
crates/kind-tests/tests/suite/kdl/Run.kind2
Normal file
13
crates/kind-tests/tests/suite/kdl/Run.kind2
Normal file
@ -0,0 +1,13 @@
|
||||
#kdl_name = A
|
||||
Ata : U60
|
||||
Ata = 2
|
||||
|
||||
#kdl_name = B
|
||||
#kdl_run
|
||||
Be : U60
|
||||
Be = Ata
|
||||
|
||||
#kdl_name = C
|
||||
#kdl_run
|
||||
Ce : U60
|
||||
Ce = 4
|
0
crates/kind-tests/tests/suite/kdl/Shortener.golden
Normal file
0
crates/kind-tests/tests/suite/kdl/Shortener.golden
Normal file
3
crates/kind-tests/tests/suite/kdl/Shortener.kind2
Normal file
3
crates/kind-tests/tests/suite/kdl/Shortener.kind2
Normal file
@ -0,0 +1,3 @@
|
||||
FunctionWithAVeryLongName : U60 {
|
||||
0
|
||||
}
|
4
crates/kind-tests/tests/suite/kdl/StillCalable.golden
Normal file
4
crates/kind-tests/tests/suite/kdl/StillCalable.golden
Normal file
@ -0,0 +1,4 @@
|
||||
fun (A ) {
|
||||
{A} = (& (+ (B) #1) #1152921504606846975)
|
||||
}
|
||||
|
11
crates/kind-tests/tests/suite/kdl/StillCalable.kind2
Normal file
11
crates/kind-tests/tests/suite/kdl/StillCalable.kind2
Normal file
@ -0,0 +1,11 @@
|
||||
#kdl_name = A
|
||||
#keep
|
||||
FnA {
|
||||
(+ FnB 1)
|
||||
}
|
||||
|
||||
#kdl_name = B
|
||||
#kdl_erase
|
||||
FnB {
|
||||
2
|
||||
}
|
3
crates/kind-tests/tests/suite/kdl/U60.golden
Normal file
3
crates/kind-tests/tests/suite/kdl/U60.golden
Normal file
@ -0,0 +1,3 @@
|
||||
run {
|
||||
#2
|
||||
}
|
4
crates/kind-tests/tests/suite/kdl/U60.kind2
Normal file
4
crates/kind-tests/tests/suite/kdl/U60.kind2
Normal file
@ -0,0 +1,4 @@
|
||||
#kdl_run
|
||||
#keep
|
||||
Main: U60
|
||||
Main = 2
|
3
crates/kind-tests/tests/suite/kdl/WithAttr.golden
Normal file
3
crates/kind-tests/tests/suite/kdl/WithAttr.golden
Normal file
@ -0,0 +1,3 @@
|
||||
run {
|
||||
#0
|
||||
}
|
9
crates/kind-tests/tests/suite/kdl/WithAttr.kind2
Normal file
9
crates/kind-tests/tests/suite/kdl/WithAttr.kind2
Normal file
@ -0,0 +1,9 @@
|
||||
#kdl_state = MyFn.state
|
||||
MyFn : U60 {
|
||||
1
|
||||
}
|
||||
|
||||
#kdl_run
|
||||
MyFn.state : U60 {
|
||||
0
|
||||
}
|
5
crates/kind-tests/tests/suite/lib/Maybe/_.kind2
Normal file
5
crates/kind-tests/tests/suite/lib/Maybe/_.kind2
Normal file
@ -0,0 +1,5 @@
|
||||
#derive[match]
|
||||
type Maybe (a: Type) {
|
||||
some (val: a)
|
||||
none
|
||||
}
|
3
crates/kind-tests/tests/suite/lib/Maybe/bind.kind2
Normal file
3
crates/kind-tests/tests/suite/lib/Maybe/bind.kind2
Normal file
@ -0,0 +1,3 @@
|
||||
Maybe.bind <a> <b> (ma: Maybe a) (mb: a -> Maybe b) : Maybe b
|
||||
Maybe.bind a b (Maybe.none t) mb = Maybe.none
|
||||
Maybe.bind a b (Maybe.some t val) mb = (mb val)
|
2
crates/kind-tests/tests/suite/lib/Maybe/pure.kind2
Normal file
2
crates/kind-tests/tests/suite/lib/Maybe/pure.kind2
Normal file
@ -0,0 +1,2 @@
|
||||
Maybe.pure <a: Type> (x: a) : Maybe a
|
||||
Maybe.pure a x = Maybe.some x
|
3
crates/kind-tests/tests/suite/lib/NoMatch.kind2
Normal file
3
crates/kind-tests/tests/suite/lib/NoMatch.kind2
Normal file
@ -0,0 +1,3 @@
|
||||
type NoMatch {
|
||||
pudding
|
||||
}
|
4
crates/kind-tests/tests/suite/lib/String.kind2
Normal file
4
crates/kind-tests/tests/suite/lib/String.kind2
Normal file
@ -0,0 +1,4 @@
|
||||
type String {
|
||||
cons (x: U60) (xs: String)
|
||||
nil
|
||||
}
|
@ -31,6 +31,8 @@ pub struct Attributes {
|
||||
pub kdl_erase: bool,
|
||||
pub kdl_name: Option<Ident>,
|
||||
pub kdl_state: Option<Ident>,
|
||||
pub trace: Option<bool>, // Some is enabled and some(true) is enabled with arguments
|
||||
pub keep: bool
|
||||
}
|
||||
|
||||
/// Enum of binary operators.
|
||||
|
1
guide/doc_strings.md
Normal file
1
guide/doc_strings.md
Normal file
@ -0,0 +1 @@
|
||||
# TODO
|
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue
Block a user