mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
feat: transformed into a comment
This commit is contained in:
parent
f1979a2021
commit
5105ebf09c
@ -115,6 +115,10 @@ pub enum Command {
|
|||||||
#[clap(aliases = &["s"])]
|
#[clap(aliases = &["s"])]
|
||||||
Show { file: String },
|
Show { file: String },
|
||||||
|
|
||||||
|
/// Gets direct dependencies of a file
|
||||||
|
#[clap(aliases = &["gd"])]
|
||||||
|
GetDeps { file: String },
|
||||||
|
|
||||||
/// Compiles a file to Kindelia (.kdl)
|
/// Compiles a file to Kindelia (.kdl)
|
||||||
#[clap(aliases = &["kdl"])]
|
#[clap(aliases = &["kdl"])]
|
||||||
ToKDL {
|
ToKDL {
|
||||||
@ -160,11 +164,21 @@ pub fn run_in_session<T>(
|
|||||||
root: PathBuf,
|
root: PathBuf,
|
||||||
file: String,
|
file: String,
|
||||||
compiled: bool,
|
compiled: bool,
|
||||||
|
silent: bool,
|
||||||
action: &mut dyn FnMut(&mut Session) -> anyhow::Result<T>,
|
action: &mut dyn FnMut(&mut Session) -> anyhow::Result<T>,
|
||||||
) -> anyhow::Result<T> {
|
) -> anyhow::Result<T> {
|
||||||
let log =
|
let log =
|
||||||
|session: &Session, report: &dyn Report| render_to_stderr(render_config, session, report);
|
|session: &Session, report: &dyn Report| render_to_stderr(render_config, session, report);
|
||||||
driver::run_in_session(render_config, root, file, compiled, action, &log)
|
let sil = |_: &Session, _: &dyn Report| ();
|
||||||
|
|
||||||
|
driver::run_in_session(
|
||||||
|
render_config,
|
||||||
|
root,
|
||||||
|
file,
|
||||||
|
compiled,
|
||||||
|
action,
|
||||||
|
if silent { &sil } else { &log },
|
||||||
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn run_cli(config: Cli) -> anyhow::Result<()> {
|
pub fn run_cli(config: Cli) -> anyhow::Result<()> {
|
||||||
@ -182,7 +196,7 @@ pub fn run_cli(config: Cli) -> anyhow::Result<()> {
|
|||||||
config.hide_vals,
|
config.hide_vals,
|
||||||
mode,
|
mode,
|
||||||
config.hide_deps,
|
config.hide_deps,
|
||||||
config.get_deps
|
config.get_deps,
|
||||||
);
|
);
|
||||||
|
|
||||||
let root = config.root.unwrap_or_else(|| PathBuf::from("."));
|
let root = config.root.unwrap_or_else(|| PathBuf::from("."));
|
||||||
@ -195,97 +209,172 @@ pub fn run_cli(config: Cli) -> anyhow::Result<()> {
|
|||||||
|
|
||||||
match config.command {
|
match config.command {
|
||||||
Command::Check { file, coverage } => {
|
Command::Check { file, coverage } => {
|
||||||
run_in_session(&render_config, root, file.clone(), false, &mut |session| {
|
run_in_session(
|
||||||
let (_, rewrites) = driver::type_check_book(
|
&render_config,
|
||||||
session,
|
root,
|
||||||
&PathBuf::from(file.clone()),
|
file.clone(),
|
||||||
entrypoints.clone(),
|
false,
|
||||||
config.tids,
|
false,
|
||||||
coverage,
|
&mut |session| {
|
||||||
)?;
|
let (_, rewrites) = driver::type_check_book(
|
||||||
|
session,
|
||||||
|
&PathBuf::from(file.clone()),
|
||||||
|
entrypoints.clone(),
|
||||||
|
config.tids,
|
||||||
|
coverage,
|
||||||
|
)?;
|
||||||
|
|
||||||
render_to_stderr(&render_config, session, &Log::Rewrites(rewrites));
|
render_to_stderr(&render_config, session, &Log::Rewrites(rewrites));
|
||||||
|
|
||||||
Ok(())
|
Ok(())
|
||||||
})?;
|
},
|
||||||
|
)?;
|
||||||
}
|
}
|
||||||
Command::ToHVM { file } => {
|
Command::ToHVM { file } => {
|
||||||
let result =
|
let result = run_in_session(
|
||||||
run_in_session(&render_config, root, file.clone(), true, &mut |session| {
|
&render_config,
|
||||||
|
root,
|
||||||
|
file.clone(),
|
||||||
|
true,
|
||||||
|
false,
|
||||||
|
&mut |session| {
|
||||||
let book = driver::erase_book(
|
let book = driver::erase_book(
|
||||||
session,
|
session,
|
||||||
&PathBuf::from(file.clone()),
|
&PathBuf::from(file.clone()),
|
||||||
entrypoints.clone(),
|
entrypoints.clone(),
|
||||||
)?;
|
)?;
|
||||||
Ok(driver::compile_book_to_hvm(book, config.trace))
|
Ok(driver::compile_book_to_hvm(book, config.trace))
|
||||||
})?;
|
},
|
||||||
|
)?;
|
||||||
|
|
||||||
println!("{}", result);
|
println!("{}", result);
|
||||||
}
|
}
|
||||||
Command::Run { file } => {
|
Command::Run { file } => {
|
||||||
let res = run_in_session(&render_config, root, file.clone(), true, &mut |session| {
|
let res = run_in_session(
|
||||||
let path = PathBuf::from(file.clone());
|
&render_config,
|
||||||
let book = driver::erase_book(session, &path, entrypoints.clone())?;
|
root,
|
||||||
driver::check_main_entry(session, &book)?;
|
file.clone(),
|
||||||
let book = driver::compile_book_to_hvm(book, config.trace);
|
true,
|
||||||
let (result, rewrites) = driver::execute_file(&book.to_string(), config.tids)?;
|
false,
|
||||||
|
&mut |session| {
|
||||||
|
let path = PathBuf::from(file.clone());
|
||||||
|
let book = driver::erase_book(session, &path, entrypoints.clone())?;
|
||||||
|
driver::check_main_entry(session, &book)?;
|
||||||
|
let book = driver::compile_book_to_hvm(book, config.trace);
|
||||||
|
let (result, rewrites) = driver::execute_file(&book.to_string(), config.tids)?;
|
||||||
|
|
||||||
render_to_stderr(&render_config, session, &Log::Rewrites(rewrites));
|
render_to_stderr(&render_config, session, &Log::Rewrites(rewrites));
|
||||||
|
|
||||||
Ok(result)
|
Ok(result)
|
||||||
})?;
|
},
|
||||||
|
)?;
|
||||||
println!("{}", res);
|
println!("{}", res);
|
||||||
}
|
}
|
||||||
Command::Show { file } => {
|
Command::Show { file } => {
|
||||||
run_in_session(&render_config, root, file.clone(), true, &mut |session| {
|
run_in_session(
|
||||||
driver::to_book(session, &PathBuf::from(file.clone()))
|
&render_config,
|
||||||
})
|
root,
|
||||||
|
file.clone(),
|
||||||
|
true,
|
||||||
|
false,
|
||||||
|
&mut |session| driver::to_book(session, &PathBuf::from(file.clone())),
|
||||||
|
)
|
||||||
.map(|res| {
|
.map(|res| {
|
||||||
print!("{}", res);
|
print!("{}", res);
|
||||||
res
|
res
|
||||||
})?;
|
})?;
|
||||||
}
|
}
|
||||||
Command::ToKindCore { file } => {
|
Command::ToKindCore { file } => {
|
||||||
let res = run_in_session(&render_config, root, file.clone(), true, &mut |session| {
|
let res = run_in_session(
|
||||||
driver::desugar_book(session, &PathBuf::from(file.clone()))
|
&render_config,
|
||||||
})?;
|
root,
|
||||||
|
file.clone(),
|
||||||
|
true,
|
||||||
|
false,
|
||||||
|
&mut |session| driver::desugar_book(session, &PathBuf::from(file.clone())),
|
||||||
|
)?;
|
||||||
print!("{}", res);
|
print!("{}", res);
|
||||||
}
|
}
|
||||||
Command::Erase { file } => {
|
Command::Erase { file } => {
|
||||||
let res = run_in_session(&render_config, root, file.clone(), true, &mut |session| {
|
let res = run_in_session(
|
||||||
driver::erase_book(session, &PathBuf::from(file.clone()), entrypoints.clone())
|
&render_config,
|
||||||
})?;
|
root,
|
||||||
|
file.clone(),
|
||||||
|
true,
|
||||||
|
false,
|
||||||
|
&mut |session| {
|
||||||
|
driver::erase_book(session, &PathBuf::from(file.clone()), entrypoints.clone())
|
||||||
|
},
|
||||||
|
)?;
|
||||||
print!("{}", res);
|
print!("{}", res);
|
||||||
}
|
}
|
||||||
Command::GenChecker { file, coverage } => {
|
Command::GenChecker { file, coverage } => {
|
||||||
let res = run_in_session(&render_config, root, file.clone(), true, &mut |session| {
|
let res = run_in_session(
|
||||||
driver::check_erasure_book(session, &PathBuf::from(file.clone()))
|
&render_config,
|
||||||
})?;
|
root,
|
||||||
|
file.clone(),
|
||||||
|
true,
|
||||||
|
false,
|
||||||
|
&mut |session| driver::check_erasure_book(session, &PathBuf::from(file.clone())),
|
||||||
|
)?;
|
||||||
print!("{}", driver::generate_checker(&res, coverage));
|
print!("{}", driver::generate_checker(&res, coverage));
|
||||||
}
|
}
|
||||||
Command::Eval { file } => {
|
Command::Eval { file } => {
|
||||||
let res = run_in_session(&render_config, root, file.clone(), true, &mut |session| {
|
let res = run_in_session(
|
||||||
let book = driver::desugar_book(session, &PathBuf::from(file.clone()))?;
|
&render_config,
|
||||||
driver::check_main_desugared_entry(session, &book)?;
|
root,
|
||||||
let (res, rewrites) = driver::eval_in_checker(&book);
|
file.clone(),
|
||||||
|
true,
|
||||||
|
false,
|
||||||
|
&mut |session| {
|
||||||
|
let book = driver::desugar_book(session, &PathBuf::from(file.clone()))?;
|
||||||
|
driver::check_main_desugared_entry(session, &book)?;
|
||||||
|
let (res, rewrites) = driver::eval_in_checker(&book);
|
||||||
|
|
||||||
render_to_stderr(&render_config, session, &Log::Rewrites(rewrites));
|
render_to_stderr(&render_config, session, &Log::Rewrites(rewrites));
|
||||||
|
|
||||||
Ok(res)
|
Ok(res)
|
||||||
})?;
|
},
|
||||||
|
)?;
|
||||||
println!("{}", res);
|
println!("{}", res);
|
||||||
}
|
}
|
||||||
Command::ToKDL { file, namespace } => {
|
Command::ToKDL { file, namespace } => {
|
||||||
let res = run_in_session(&render_config, root, file.clone(), true, &mut |session| {
|
let res = run_in_session(
|
||||||
driver::compile_book_to_kdl(
|
&render_config,
|
||||||
&PathBuf::from(file.clone()),
|
root,
|
||||||
session,
|
file.clone(),
|
||||||
&namespace.clone().unwrap_or("".to_string()),
|
true,
|
||||||
entrypoints.clone(),
|
false,
|
||||||
)
|
&mut |session| {
|
||||||
})?;
|
driver::compile_book_to_kdl(
|
||||||
|
&PathBuf::from(file.clone()),
|
||||||
|
session,
|
||||||
|
&namespace.clone().unwrap_or("".to_string()),
|
||||||
|
entrypoints.clone(),
|
||||||
|
)
|
||||||
|
},
|
||||||
|
)?;
|
||||||
println!("{}", res);
|
println!("{}", res);
|
||||||
}
|
}
|
||||||
|
Command::GetDeps { file } => {
|
||||||
|
let res = run_in_session(
|
||||||
|
&render_config,
|
||||||
|
root,
|
||||||
|
file.clone(),
|
||||||
|
true,
|
||||||
|
true,
|
||||||
|
&mut |session| {
|
||||||
|
Ok(driver::get_unbound_variables(
|
||||||
|
session,
|
||||||
|
&PathBuf::from(file.clone()),
|
||||||
|
))
|
||||||
|
},
|
||||||
|
)?;
|
||||||
|
|
||||||
|
if let Some(res) = res {
|
||||||
|
println!("{}", res.join(" "));
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
Ok(())
|
Ok(())
|
||||||
|
@ -20,6 +20,8 @@ pub mod diagnostic;
|
|||||||
pub mod resolution;
|
pub mod resolution;
|
||||||
pub mod session;
|
pub mod session;
|
||||||
|
|
||||||
|
pub use resolution::get_unbound_variables;
|
||||||
|
|
||||||
impl FileCache for Session {
|
impl FileCache for Session {
|
||||||
fn fetch(&self, ctx: SyntaxCtxIndex) -> Option<(PathBuf, &String)> {
|
fn fetch(&self, ctx: SyntaxCtxIndex) -> Option<(PathBuf, &String)> {
|
||||||
let path = self.loaded_paths[ctx.0].as_ref().to_owned();
|
let path = self.loaded_paths[ctx.0].as_ref().to_owned();
|
||||||
|
@ -191,6 +191,21 @@ fn parse_and_store_book_by_identifier(
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn read_file(session: &mut Session, path: &Path) -> Option<String> {
|
||||||
|
match fs::read_to_string(path) {
|
||||||
|
Ok(res) => Some(res),
|
||||||
|
Err(_) => {
|
||||||
|
session
|
||||||
|
.diagnostic_sender
|
||||||
|
.send(Box::new(DriverDiagnostic::CannotFindFile(
|
||||||
|
path.to_str().unwrap().to_string(),
|
||||||
|
)))
|
||||||
|
.unwrap();
|
||||||
|
None
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
fn parse_and_store_book_by_path(session: &mut Session, path: &PathBuf, book: &mut Book, immediate: bool) -> bool {
|
fn parse_and_store_book_by_path(session: &mut Session, path: &PathBuf, book: &mut Book, immediate: bool) -> bool {
|
||||||
if !path.exists() {
|
if !path.exists() {
|
||||||
let err = Box::new(DriverDiagnostic::CannotFindFile(
|
let err = Box::new(DriverDiagnostic::CannotFindFile(
|
||||||
@ -207,18 +222,7 @@ fn parse_and_store_book_by_path(session: &mut Session, path: &PathBuf, book: &mu
|
|||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
let input = match fs::read_to_string(path) {
|
let Some(input) = read_file(session, path) else { return true };
|
||||||
Ok(res) => res,
|
|
||||||
Err(_) => {
|
|
||||||
session
|
|
||||||
.diagnostic_sender
|
|
||||||
.send(Box::new(DriverDiagnostic::CannotFindFile(
|
|
||||||
path.to_str().unwrap().to_string(),
|
|
||||||
)))
|
|
||||||
.unwrap();
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
let ctx_id = session.book_counter;
|
let ctx_id = session.book_counter;
|
||||||
session.add_path(Rc::new(fs::canonicalize(path).unwrap()), input.clone());
|
session.add_path(Rc::new(fs::canonicalize(path).unwrap()), input.clone());
|
||||||
@ -250,6 +254,23 @@ fn parse_and_store_book_by_path(session: &mut Session, path: &PathBuf, book: &mu
|
|||||||
failed
|
failed
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub fn get_unbound_variables(session: &mut Session, path: &Path) -> Option<Vec<String>> {
|
||||||
|
let tx = session.diagnostic_sender.clone();
|
||||||
|
|
||||||
|
let Some(input) = read_file(session, path) else { return None };
|
||||||
|
|
||||||
|
let (mut module, _) = kind_parser::parse_book(tx.clone(), 0, &input);
|
||||||
|
|
||||||
|
expand_uses(&mut module, tx.clone());
|
||||||
|
expand_module(tx.clone(), &mut module);
|
||||||
|
|
||||||
|
let mut state = UnboundCollector::new(tx.clone(), false);
|
||||||
|
state.visit_module(&mut module);
|
||||||
|
|
||||||
|
Some(state.unbound_top_level.keys().cloned().collect())
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
fn unbound_variable(session: &mut Session, book: &Book, idents: &[Ident]) {
|
fn unbound_variable(session: &mut Session, book: &Book, idents: &[Ident]) {
|
||||||
let mut similar_names = book
|
let mut similar_names = book
|
||||||
.names
|
.names
|
||||||
|
@ -322,20 +322,20 @@ impl Diagnostic for PassDiagnostic {
|
|||||||
DiagnosticFrame {
|
DiagnosticFrame {
|
||||||
code: 210,
|
code: 210,
|
||||||
severity: Severity::Error,
|
severity: Severity::Error,
|
||||||
title: "Incorrect arity.".to_string(),
|
title: if *expected == 0 {
|
||||||
subtitles: vec![],
|
|
||||||
hints: vec![if *expected == 0 {
|
|
||||||
format!("This function expects no arguments but got {}", got.len())
|
format!("This function expects no arguments but got {}", got.len())
|
||||||
} else if *hidden == 0 {
|
} else if *hidden == 0 {
|
||||||
format!("This function expects {} arguments but got {}", expected, got.len())
|
format!("This function expects exactly {} arguments but got {}", expected, got.len())
|
||||||
} else {
|
} else {
|
||||||
format!(
|
format!(
|
||||||
"This function expects {} arguments or {} (without hidden ones) but got {}.",
|
"This function expects exactly {} arguments or {} (without hidden ones) but got {}.",
|
||||||
expected,
|
expected,
|
||||||
expected - hidden,
|
expected - hidden,
|
||||||
got.len()
|
got.len()
|
||||||
)
|
)
|
||||||
}],
|
},
|
||||||
|
subtitles: vec![],
|
||||||
|
hints: vec![],
|
||||||
positions,
|
positions,
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
ERROR Incorrect arity.
|
ERROR This function expects exactly 1 arguments but got 0
|
||||||
|
|
||||||
/--[suite/issues/checker/ArityOnLet.kind2:6:13]
|
/--[suite/issues/checker/ArityOnLet.kind2:6:13]
|
||||||
|
|
|
|
||||||
@ -8,5 +8,4 @@
|
|||||||
| \This function requires a fixed number of arguments
|
| \This function requires a fixed number of arguments
|
||||||
7 | 2
|
7 | 2
|
||||||
|
|
||||||
Hint: This function expects 1 arguments but got 0
|
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user