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
32c8a6f2c2
62
Cargo.lock
generated
62
Cargo.lock
generated
@ -69,9 +69,9 @@ checksum = "ec8a7b6a70fde80372154c65702f00a0f56f3e1c36abbc6c440484be248856db"
|
||||
|
||||
[[package]]
|
||||
name = "cc"
|
||||
version = "1.0.73"
|
||||
version = "1.0.76"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "2fff2a6927b3bb87f9595d67196a70493f627687a71d87a0d692242c33f58c11"
|
||||
checksum = "76a284da2e6fe2092f2353e51713435363112dfd60030e22add80be333fb928f"
|
||||
|
||||
[[package]]
|
||||
name = "cfg-if"
|
||||
@ -98,13 +98,13 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "clap"
|
||||
version = "4.0.15"
|
||||
version = "4.0.22"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "6bf8832993da70a4c6d13c581f4463c2bdda27b9bf1c5498dc4365543abe6d6f"
|
||||
checksum = "91b9970d7505127a162fdaa9b96428d28a479ba78c9ec7550a63a5d9863db682"
|
||||
dependencies = [
|
||||
"atty",
|
||||
"bitflags",
|
||||
"clap_derive 4.0.13",
|
||||
"clap_derive 4.0.21",
|
||||
"clap_lex 0.3.0",
|
||||
"once_cell",
|
||||
"strsim",
|
||||
@ -126,9 +126,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "clap_derive"
|
||||
version = "4.0.13"
|
||||
version = "4.0.21"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "c42f169caba89a7d512b5418b09864543eeb4d497416c917d7137863bd2076ad"
|
||||
checksum = "0177313f9f02afc995627906bbd8967e2be069f5261954222dac78290c2b9014"
|
||||
dependencies = [
|
||||
"heck",
|
||||
"proc-macro-error",
|
||||
@ -444,9 +444,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "hyper"
|
||||
version = "0.14.20"
|
||||
version = "0.14.23"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "02c929dc5c39e335a03c405292728118860721b10190d98c2a0f0efd5baafbac"
|
||||
checksum = "034711faac9d2166cb1baf1a2fb0b60b1f277f8492fd72176c17f3515e1abd3c"
|
||||
dependencies = [
|
||||
"bytes",
|
||||
"futures-channel",
|
||||
@ -553,9 +553,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "ipnet"
|
||||
version = "2.5.0"
|
||||
version = "2.5.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "879d54834c8c76457ef4293a689b2a8c59b076067ad77b15efafbb05f92a592b"
|
||||
checksum = "f88c5561171189e69df9d98bcf18fd5f9558300f7ea7b801eb8a0fd748bd8745"
|
||||
|
||||
[[package]]
|
||||
name = "itertools"
|
||||
@ -597,7 +597,7 @@ dependencies = [
|
||||
name = "kind-cli"
|
||||
version = "0.3.0"
|
||||
dependencies = [
|
||||
"clap 4.0.15",
|
||||
"clap 4.0.22",
|
||||
"kind-checker",
|
||||
"kind-driver",
|
||||
"kind-report",
|
||||
@ -619,6 +619,7 @@ dependencies = [
|
||||
"dashmap",
|
||||
"eyre",
|
||||
"fxhash",
|
||||
"hvm",
|
||||
"kind-checker",
|
||||
"kind-parser",
|
||||
"kind-pass",
|
||||
@ -634,6 +635,7 @@ dependencies = [
|
||||
name = "kind-parser"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"fxhash",
|
||||
"kind-report",
|
||||
"kind-span",
|
||||
"kind-tree",
|
||||
@ -718,9 +720,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
|
||||
|
||||
[[package]]
|
||||
name = "libc"
|
||||
version = "0.2.135"
|
||||
version = "0.2.137"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "68783febc7782c6c5cb401fbda4de5a9898be1762314da0bb2c10ced61f18b0c"
|
||||
checksum = "fc7fcc620a3bff7cdd7a365be3376c97191aeaccc2a603e600951e452615bf89"
|
||||
|
||||
[[package]]
|
||||
name = "linked-hash-map"
|
||||
@ -773,9 +775,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "native-tls"
|
||||
version = "0.2.10"
|
||||
version = "0.2.11"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "fd7e2f3618557f980e0b17e8856252eee3c97fa12c54dff0ca290fb6266ca4a9"
|
||||
checksum = "07226173c32f2926027b63cce4bcd8076c3552846cbe7925f3aaffeac0a3b92e"
|
||||
dependencies = [
|
||||
"lazy_static",
|
||||
"libc",
|
||||
@ -819,9 +821,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "num_cpus"
|
||||
version = "1.13.1"
|
||||
version = "1.14.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "19e64526ebdee182341572e50e9ad03965aa510cd94427a4549448f285e957a1"
|
||||
checksum = "f6058e64324c71e02bc2b150e4f3bc8286db6c83092132ffa3f6b1eab0f9def5"
|
||||
dependencies = [
|
||||
"hermit-abi",
|
||||
"libc",
|
||||
@ -829,9 +831,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "once_cell"
|
||||
version = "1.15.0"
|
||||
version = "1.16.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e82dad04139b71a90c080c8463fe0dc7902db5192d939bd0950f074d014339e1"
|
||||
checksum = "86f0b0d4bf799edbc74508c1e8bf170ff5f41238e5f8225603ca7caaae2b7860"
|
||||
|
||||
[[package]]
|
||||
name = "openssl"
|
||||
@ -880,9 +882,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "os_str_bytes"
|
||||
version = "6.3.0"
|
||||
version = "6.3.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9ff7415e9ae3fff1225851df9e0d9e4e5479f947619774677a63572e55e80eff"
|
||||
checksum = "3baf96e39c5359d2eb0dd6ccb42c62b91d9678aa68160d261b9e0ccbf9e9dea9"
|
||||
|
||||
[[package]]
|
||||
name = "parking_lot_core"
|
||||
@ -947,9 +949,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "proc-macro2"
|
||||
version = "1.0.46"
|
||||
version = "1.0.47"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "94e2ef8dbfc347b10c094890f778ee2e36ca9bb4262e86dc99cd217e35f3470b"
|
||||
checksum = "5ea3d908b0e36316caf9e9e2c4625cdde190a7e6f440d794667ed17a1855e725"
|
||||
dependencies = [
|
||||
"unicode-ident",
|
||||
]
|
||||
@ -989,9 +991,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "regex"
|
||||
version = "1.6.0"
|
||||
version = "1.7.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4c4eb3267174b8c6c2f654116623910a0fef09c4753f8dd83db29c48a0df988b"
|
||||
checksum = "e076559ef8e241f2ae3479e36f97bd5741c0330689e217ad51ce2c76808b868a"
|
||||
dependencies = [
|
||||
"aho-corasick",
|
||||
"memchr",
|
||||
@ -1000,9 +1002,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "regex-syntax"
|
||||
version = "0.6.27"
|
||||
version = "0.6.28"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a3f87b73ce11b1619a3c6332f45341e0047173771e8b8b73f87bfeefb7b56244"
|
||||
checksum = "456c603be3e8d448b072f410900c09faf164fbce2d480456f50eea6e25f9c848"
|
||||
|
||||
[[package]]
|
||||
name = "remove_dir_all"
|
||||
@ -1176,9 +1178,9 @@ checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623"
|
||||
|
||||
[[package]]
|
||||
name = "syn"
|
||||
version = "1.0.102"
|
||||
version = "1.0.103"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3fcd952facd492f9be3ef0d0b7032a6e442ee9b361d4acc2b1d0c4aaa5f613a1"
|
||||
checksum = "a864042229133ada95abf3b54fdc62ef5ccabe9515b64717bcb9a1919e59445d"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
|
@ -80,7 +80,7 @@ fn mk_single_ctr(head: String) -> Box<Term> {
|
||||
|
||||
fn mk_ctr_name(ident: &QualifiedIdent) -> Box<Term> {
|
||||
// Adds an empty segment (so it just appends a dot in the end)
|
||||
mk_single_ctr(format!("{}.", ident.to_string()))
|
||||
mk_single_ctr(format!("{}.", ident))
|
||||
}
|
||||
|
||||
fn span_to_num(span: Span) -> Box<Term> {
|
||||
|
@ -20,10 +20,13 @@ pub(crate) enum TypeError {
|
||||
|
||||
pub fn context_to_subtitles(ctx: Context, subtitles: &mut Vec<Subtitle>) {
|
||||
subtitles.push(Subtitle::LineBreak);
|
||||
|
||||
if !ctx.0.is_empty() {
|
||||
subtitles.push(Subtitle::Phrase(
|
||||
Color::Snd,
|
||||
vec![Word::White("Context:".to_string())],
|
||||
));
|
||||
}
|
||||
|
||||
let biggest = ctx
|
||||
.0
|
||||
|
@ -4,6 +4,7 @@ pub mod report;
|
||||
|
||||
use std::sync::mpsc::Sender;
|
||||
|
||||
use hvm::Term;
|
||||
use kind_report::data::DiagnosticFrame;
|
||||
use kind_tree::desugared::Book;
|
||||
|
||||
@ -13,11 +14,19 @@ const CHECKER_HVM: &str = include_str!("checker.hvm");
|
||||
|
||||
/// Type checks a dessugared book. It spawns an HVM instance in order
|
||||
/// to run a compiled version of the book
|
||||
pub fn type_check(book: &Book, tx: Sender<DiagnosticFrame>) -> bool {
|
||||
pub fn gen_checker(book: &Book) -> String {
|
||||
let base_check_code = compiler::codegen_book(book);
|
||||
let mut check_code = CHECKER_HVM.to_string();
|
||||
check_code.push_str(&base_check_code.to_string());
|
||||
|
||||
check_code
|
||||
}
|
||||
|
||||
/// Type checks a dessugared book. It spawns an HVM instance in order
|
||||
/// to run a compiled version of the book
|
||||
pub fn type_check(book: &Book, tx: Sender<DiagnosticFrame>) -> bool {
|
||||
let check_code = gen_checker(book);
|
||||
|
||||
let mut runtime = hvm::Runtime::from_code(&check_code).unwrap();
|
||||
let main = runtime.alloc_code("Kind.API.check_all").unwrap();
|
||||
runtime.run_io(main);
|
||||
@ -34,3 +43,15 @@ pub fn type_check(book: &Book, tx: Sender<DiagnosticFrame>) -> bool {
|
||||
|
||||
succeeded
|
||||
}
|
||||
|
||||
/// Type checks a dessugared book. It spawns an HVM instance in order
|
||||
/// to run a compiled version of the book
|
||||
pub fn eval_api(book: &Book) -> Box<Term> {
|
||||
let check_code = gen_checker(book);
|
||||
|
||||
let mut runtime = hvm::Runtime::from_code(&check_code).unwrap();
|
||||
let main = runtime.alloc_code("Kind.API.eval_main").unwrap();
|
||||
runtime.run_io(main);
|
||||
runtime.normalize(main);
|
||||
runtime.readback(main)
|
||||
}
|
||||
|
@ -6,6 +6,11 @@ use kind_tree::{desugared, Operator};
|
||||
use crate::errors::TypeError;
|
||||
use desugared::Expr;
|
||||
|
||||
type Entry = (String, Box<Expr>, Vec<Box<Expr>>);
|
||||
|
||||
#[derive(Debug)]
|
||||
pub struct Context(pub Vec<Entry>);
|
||||
|
||||
macro_rules! match_opt {
|
||||
($expr:expr, $pat:pat => $end:expr) => {
|
||||
match $expr {
|
||||
@ -15,11 +20,6 @@ macro_rules! match_opt {
|
||||
};
|
||||
}
|
||||
|
||||
type Entry = (String, Box<Expr>, Vec<Box<Expr>>);
|
||||
|
||||
#[derive(Debug)]
|
||||
pub struct Context(pub Vec<Entry>);
|
||||
|
||||
fn parse_orig(term: &Term) -> Result<Range, String> {
|
||||
match_opt!(term, Term::Num { numb } => EncodedSpan(*numb).to_range())
|
||||
}
|
||||
@ -54,11 +54,25 @@ fn parse_op(term: &Term) -> Result<Operator, String> {
|
||||
}
|
||||
|
||||
fn parse_name(term: &Term) -> Result<String, String> {
|
||||
match_opt!(*term, Term::Num { numb } => Ident::decode(numb))
|
||||
match term {
|
||||
Term::Num { numb } => Ok(Ident::decode(*numb)),
|
||||
Term::Ctr { name, args: _ } => Ok(name.to_string()),
|
||||
_ => Err("Error while matching opt".to_string()),
|
||||
}
|
||||
}
|
||||
|
||||
fn parse_qualified(term: &Term) -> Result<QualifiedIdent, String> {
|
||||
todo!()
|
||||
match term {
|
||||
Term::Num { numb } => Ok(QualifiedIdent::new_static(
|
||||
&Ident::decode(*numb),
|
||||
None,
|
||||
Range::ghost_range(),
|
||||
)),
|
||||
Term::Ctr { name, args: _ } => {
|
||||
Ok(QualifiedIdent::new_static(name, None, Range::ghost_range()))
|
||||
}
|
||||
_ => Err("Error while matching opt".to_string()),
|
||||
}
|
||||
}
|
||||
|
||||
fn parse_expr(term: &Term) -> Result<Box<desugared::Expr>, String> {
|
||||
@ -112,12 +126,12 @@ fn parse_all_expr(
|
||||
vec![parse_all_expr(names, &args[2])?],
|
||||
)),
|
||||
"Kind.Quoted.ctr" => Ok(Expr::ctr(
|
||||
parse_orig(&args[0])?,
|
||||
parse_qualified(&args[1])?,
|
||||
parse_orig(&args[1])?,
|
||||
parse_qualified(&args[0])?,
|
||||
{
|
||||
let mut res = Vec::new();
|
||||
for arg in &args[1..] {
|
||||
res.push(parse_all_expr(names.clone(), arg)?);
|
||||
for arg in parse_list(&args[2])? {
|
||||
res.push(parse_all_expr(names.clone(), &arg)?);
|
||||
}
|
||||
res
|
||||
},
|
||||
@ -142,7 +156,10 @@ fn parse_all_expr(
|
||||
parse_all_expr(names.clone(), &args[2])?,
|
||||
parse_all_expr(names, &args[3])?,
|
||||
)),
|
||||
_ => Err("Unexpected tag on transforming quoted term".to_string()),
|
||||
tag => Err(format!(
|
||||
"Unexpected tag on transforming quoted term {:?}",
|
||||
tag
|
||||
)),
|
||||
},
|
||||
_ => Err("Unexpected term on transforming quoted term".to_string()),
|
||||
}
|
||||
@ -160,7 +177,7 @@ fn parse_list(term: &Term) -> Result<Vec<Box<Term>>, String> {
|
||||
vec.push(args[0].clone());
|
||||
cur = &args[1];
|
||||
} else {
|
||||
return Err("Unexpected constructor on list".to_string());
|
||||
return Err(format!("Unexpected constructor on list '{:?}'", name));
|
||||
}
|
||||
}
|
||||
_ => return Err("Unexpected value on list".to_string()),
|
||||
|
@ -3,12 +3,13 @@ use std::time::Instant;
|
||||
use std::{fmt, io};
|
||||
|
||||
use clap::{Parser, Subcommand};
|
||||
use kind_driver::resolution::{compile_book, type_check_book};
|
||||
use kind_driver::{session::Session};
|
||||
use kind_driver::session::Session;
|
||||
use kind_report::data::{Diagnostic, DiagnosticFrame, Log};
|
||||
use kind_report::report::{FileCache, Report};
|
||||
use kind_report::RenderConfig;
|
||||
|
||||
use kind_driver as driver;
|
||||
|
||||
#[derive(Parser, Debug)]
|
||||
#[command(author, version, about, long_about = None)]
|
||||
#[clap(propagate_version = true)]
|
||||
@ -49,6 +50,9 @@ enum Command {
|
||||
#[clap(aliases = &["e"])]
|
||||
Eval { file: String },
|
||||
|
||||
#[clap(aliases = &["k"])]
|
||||
ToKindCore { file : String },
|
||||
|
||||
/// Runs Main on the HVM
|
||||
#[clap(aliases = &["r"])]
|
||||
Run { file: String },
|
||||
@ -110,22 +114,15 @@ where
|
||||
.unwrap();
|
||||
}
|
||||
|
||||
fn main() {
|
||||
let config = Cli::parse();
|
||||
|
||||
kind_report::check_if_colors_are_supported(config.no_color);
|
||||
|
||||
let render_config = if config.ascii {
|
||||
RenderConfig::ascii(2)
|
||||
} else {
|
||||
RenderConfig::unicode(2)
|
||||
};
|
||||
|
||||
match config.command {
|
||||
Command::Check { file } => {
|
||||
pub fn compile_in_session<T>(
|
||||
render_config: RenderConfig,
|
||||
root: PathBuf,
|
||||
file: String,
|
||||
fun: &mut dyn FnMut(&mut Session) -> Option<T>,
|
||||
) -> Option<T> {
|
||||
let (rx, tx) = std::sync::mpsc::channel();
|
||||
|
||||
let mut session = Session::new(PathBuf::from("."), rx);
|
||||
let mut session = Session::new(root, rx);
|
||||
|
||||
eprintln!();
|
||||
|
||||
@ -137,12 +134,13 @@ fn main() {
|
||||
|
||||
let start = Instant::now();
|
||||
|
||||
type_check_book(&mut session, &PathBuf::from(file));
|
||||
let res = fun(&mut session);
|
||||
|
||||
let diagnostics = tx.try_iter().collect::<Vec<DiagnosticFrame>>();
|
||||
|
||||
if diagnostics.is_empty() {
|
||||
render_to_stderr(&render_config, &session, &Log::Checked(start.elapsed()));
|
||||
eprintln!();
|
||||
} else {
|
||||
render_to_stderr(&render_config, &session, &Log::Failed(start.elapsed()));
|
||||
eprintln!();
|
||||
@ -151,15 +149,82 @@ fn main() {
|
||||
render_to_stderr(&render_config, &session, &diagnostic)
|
||||
}
|
||||
}
|
||||
eprintln!();
|
||||
res
|
||||
}
|
||||
Command::Eval { file } => todo!(),
|
||||
Command::Run { file } => todo!(),
|
||||
Command::GenChecker { file } => todo!(),
|
||||
Command::Show { file } => todo!(),
|
||||
Command::ToKDL { file, namespace } => todo!(),
|
||||
Command::ToHVM { file } => todo!(),
|
||||
Command::Watch { file } => todo!(),
|
||||
|
||||
fn main() {
|
||||
let config = Cli::parse();
|
||||
|
||||
kind_report::check_if_colors_are_supported(config.no_color);
|
||||
|
||||
let render_config = kind_report::check_if_utf8_is_supported(config.ascii, 2);
|
||||
let root = PathBuf::from(".");
|
||||
|
||||
match config.command {
|
||||
Command::Check { file } => {
|
||||
compile_in_session(render_config, root, file.clone(), &mut |session| {
|
||||
driver::type_check_book(session, &PathBuf::from(file.clone()))
|
||||
});
|
||||
}
|
||||
Command::ToHVM { file } => {
|
||||
compile_in_session(render_config, root, file.clone(), &mut |session| {
|
||||
driver::compile_book_to_hvm(session, &PathBuf::from(file.clone()))
|
||||
})
|
||||
.map(|res| {
|
||||
println!("{}", res);
|
||||
res
|
||||
});
|
||||
}
|
||||
Command::Run { file } => {
|
||||
compile_in_session(render_config, root, file.clone(), &mut |session| {
|
||||
driver::compile_book_to_hvm(session, &PathBuf::from(file.clone()))
|
||||
})
|
||||
.map(|res| {
|
||||
println!("{}", driver::execute_file(&res));
|
||||
res
|
||||
});
|
||||
}
|
||||
Command::Eval { file } => {
|
||||
compile_in_session(render_config, root, file.clone(), &mut |session| {
|
||||
driver::erase_book(session, &PathBuf::from(file.clone()))
|
||||
})
|
||||
.map(|res| {
|
||||
println!("{}", driver::eval_in_checker(&res));
|
||||
res
|
||||
});
|
||||
}
|
||||
Command::Show { file } => {
|
||||
compile_in_session(render_config, root, file.clone(), &mut |session| {
|
||||
driver::to_book(session, &PathBuf::from(file.clone()))
|
||||
})
|
||||
.map(|res| {
|
||||
print!("{}", res);
|
||||
res
|
||||
});
|
||||
}
|
||||
Command::ToKindCore { file } => {
|
||||
compile_in_session(render_config, root, file.clone(), &mut |session| {
|
||||
driver::desugar_book(session, &PathBuf::from(file.clone()))
|
||||
})
|
||||
.map(|res| {
|
||||
print!("{}", res);
|
||||
res
|
||||
});
|
||||
}
|
||||
Command::GenChecker { file } => {
|
||||
compile_in_session(render_config, root, file.clone(), &mut |session| {
|
||||
driver::check_erasure_book(session, &PathBuf::from(file.clone()))
|
||||
})
|
||||
.map(|res| {
|
||||
print!("{}", driver::generate_checker(&res));
|
||||
res
|
||||
});
|
||||
}
|
||||
Command::ToKDL {
|
||||
file: _,
|
||||
namespace: _,
|
||||
} => todo!(),
|
||||
Command::Watch { file: _ } => todo!(),
|
||||
Command::Repl => todo!(),
|
||||
}
|
||||
}
|
||||
|
@ -17,14 +17,14 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
|
||||
})
|
||||
};
|
||||
|
||||
let mk_cons = |name: QualifiedIdent| -> Box<Expr> {
|
||||
let mk_cons = |name: QualifiedIdent, spine: Vec<Binding>| -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::Constr(name),
|
||||
data: ExprKind::Constr(name, spine),
|
||||
range,
|
||||
})
|
||||
};
|
||||
|
||||
let mk_app = |left: Box<Expr>, right: Vec<Binding>| -> Box<Expr> {
|
||||
let mk_app = |left: Box<Expr>, right: Vec<Binding>, range: Range| -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::App(left, right),
|
||||
range,
|
||||
@ -60,8 +60,8 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
|
||||
// The type
|
||||
|
||||
let all_args = sum.parameters.extend(&sum.indices);
|
||||
let res_motive_ty = mk_app(
|
||||
mk_cons(sum.name.clone()),
|
||||
let res_motive_ty = mk_cons(
|
||||
sum.name.clone(),
|
||||
all_args
|
||||
.iter()
|
||||
.cloned()
|
||||
@ -69,6 +69,12 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
|
||||
.collect(),
|
||||
);
|
||||
|
||||
let parameter_names: Vec<Binding> = sum
|
||||
.parameters
|
||||
.iter()
|
||||
.map(|x| Binding::Positional(mk_var(x.name.clone())))
|
||||
.collect();
|
||||
|
||||
let indice_names: Vec<Binding> = sum
|
||||
.indices
|
||||
.iter()
|
||||
@ -89,9 +95,15 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
|
||||
|
||||
let motive_ident = Ident::new_static("motive", range);
|
||||
|
||||
let motive_type = sum.indices.iter().rfold(
|
||||
let motive_type = sum.parameters.extend(&sum.indices).iter().rfold(
|
||||
mk_pi(Ident::new_static("_val", range), res_motive_ty, mk_typ()),
|
||||
|out, arg| mk_pi(arg.name.clone(), arg.typ.clone().unwrap_or(mk_typ()), out),
|
||||
|out, arg| {
|
||||
mk_pi(
|
||||
arg.name.clone(),
|
||||
arg.typ.clone().unwrap_or_else(mk_typ),
|
||||
out,
|
||||
)
|
||||
},
|
||||
);
|
||||
|
||||
types.push(Argument {
|
||||
@ -102,28 +114,36 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
|
||||
range,
|
||||
});
|
||||
|
||||
let params = sum
|
||||
.parameters
|
||||
.map(|x| Binding::Positional(mk_var(x.name.clone())));
|
||||
|
||||
// Constructors type
|
||||
for cons in &sum.constructors {
|
||||
let vars = cons
|
||||
let vars: Vec<Binding> = cons
|
||||
.args
|
||||
.iter()
|
||||
.map(|x| Binding::Positional(mk_var(x.name.clone())))
|
||||
.collect();
|
||||
|
||||
let cons_inst = mk_app(mk_cons(sum.name.add_segment(cons.name.to_str())), vars);
|
||||
let cons_inst = mk_cons(
|
||||
sum.name.add_segment(cons.name.to_str()),
|
||||
[params.as_slice(), vars.as_slice()].concat(),
|
||||
);
|
||||
|
||||
let mut indices_of_cons = match cons.typ.clone().map(|x| x.data) {
|
||||
Some(ExprKind::App(_, spine)) => spine[sum.parameters.len()..].to_vec(),
|
||||
_ => indice_names.clone(),
|
||||
Some(ExprKind::Constr(_, spine)) => spine.to_vec(),
|
||||
_ => [parameter_names.as_slice(), indice_names.as_slice()].concat(),
|
||||
};
|
||||
|
||||
indices_of_cons.push(Binding::Positional(cons_inst));
|
||||
let cons_tipo = mk_app(mk_var(motive_ident.clone()), indices_of_cons);
|
||||
|
||||
let cons_tipo = mk_app(mk_var(motive_ident.clone()), indices_of_cons, range);
|
||||
|
||||
let cons_type = cons.args.iter().rfold(cons_tipo, |out, arg| {
|
||||
mk_pi(
|
||||
arg.name.clone(),
|
||||
arg.typ.clone().unwrap_or_else(|| mk_typ()),
|
||||
arg.typ.clone().unwrap_or_else(mk_typ),
|
||||
out,
|
||||
)
|
||||
});
|
||||
@ -131,15 +151,15 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
|
||||
types.push(Argument {
|
||||
hidden: false,
|
||||
erased: false,
|
||||
name: Ident::new_static("_", range),
|
||||
name: Ident::new_static(&format!("_{}", cons.name.to_string()), range),
|
||||
typ: Some(cons_type),
|
||||
range,
|
||||
});
|
||||
}
|
||||
|
||||
let mut res: Vec<Binding> = indice_names;
|
||||
let mut res: Vec<Binding> = [parameter_names.as_slice(), indice_names.as_slice()].concat();
|
||||
res.push(Binding::Positional(mk_var(Ident::generate("scrutinizer"))));
|
||||
let ret_ty = mk_app(mk_var(motive_ident), res);
|
||||
let ret_ty = mk_app(mk_var(motive_ident), res, range);
|
||||
|
||||
let mut rules = Vec::new();
|
||||
|
||||
@ -147,16 +167,21 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
|
||||
let cons_ident = sum.name.add_segment(cons.name.to_str());
|
||||
let mut pats: Vec<Box<Pat>> = Vec::new();
|
||||
|
||||
let spine_params: Vec<Ident> = sum
|
||||
.parameters
|
||||
.extend(&cons.args)
|
||||
.map(|x| x.name.with_name(|f| format!("{}_", f)))
|
||||
.to_vec();
|
||||
|
||||
let spine: Vec<Ident> = cons
|
||||
.args
|
||||
.iter()
|
||||
.map(|x| x.name.with_name(|f| format!("{}_", f)))
|
||||
.collect();
|
||||
.to_vec();
|
||||
|
||||
pats.push(Box::new(Pat {
|
||||
data: concrete::pat::PatKind::App(
|
||||
cons_ident.clone(),
|
||||
spine
|
||||
spine_params
|
||||
.iter()
|
||||
.cloned()
|
||||
.map(|x| {
|
||||
@ -188,18 +213,19 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
|
||||
.iter()
|
||||
.map(|arg| Binding::Positional(mk_var(arg.clone())))
|
||||
.collect(),
|
||||
cons.name.range,
|
||||
);
|
||||
|
||||
rules.push(Box::new(Rule {
|
||||
name: name.clone(),
|
||||
pats,
|
||||
body,
|
||||
range,
|
||||
range: cons.name.range,
|
||||
}))
|
||||
}
|
||||
// Rules
|
||||
|
||||
Entry {
|
||||
let entry = Entry {
|
||||
name,
|
||||
docs: Vec::new(),
|
||||
args: types,
|
||||
@ -207,5 +233,7 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
|
||||
rules,
|
||||
range,
|
||||
attrs: Vec::new(),
|
||||
}
|
||||
};
|
||||
|
||||
entry
|
||||
}
|
||||
|
@ -1 +1,149 @@
|
||||
///! 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_open(range: Range, sum: &RecordDecl) -> concrete::Entry {
|
||||
let mk_var = |name: Ident| -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::Var(name),
|
||||
range,
|
||||
})
|
||||
};
|
||||
|
||||
let mk_cons = |name: QualifiedIdent, spine: Vec<Binding>| -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::Constr(name, spine),
|
||||
range,
|
||||
})
|
||||
};
|
||||
|
||||
let mk_app = |left: Box<Expr>, right: Vec<Binding>| -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::App(left, right),
|
||||
range,
|
||||
})
|
||||
};
|
||||
|
||||
let mk_pi = |name: Ident, left: Box<Expr>, right: Box<Expr>| -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
data: ExprKind::All(Some(name), left, right),
|
||||
range,
|
||||
})
|
||||
};
|
||||
|
||||
let name = sum.name.add_segment("open");
|
||||
|
||||
let mut types = Telescope::default();
|
||||
|
||||
for arg in sum.parameters.iter() {
|
||||
types.push(arg.to_implicit())
|
||||
}
|
||||
|
||||
// The type
|
||||
|
||||
let all_args = sum.parameters.clone();
|
||||
let res_motive_ty = mk_cons(
|
||||
sum.name.clone(),
|
||||
all_args
|
||||
.iter()
|
||||
.cloned()
|
||||
.map(|x| Binding::Positional(mk_var(x.name)))
|
||||
.collect(),
|
||||
);
|
||||
|
||||
types.push(Argument {
|
||||
hidden: true,
|
||||
erased: true,
|
||||
name: Ident::generate("_res"),
|
||||
typ: None,
|
||||
range,
|
||||
});
|
||||
|
||||
let cons_tipo = mk_var(Ident::generate("_res"));
|
||||
|
||||
let cons_type = sum.fields.iter().rfold(cons_tipo, |out, (name, _, typ)| {
|
||||
mk_pi(name.clone(), typ.clone(), out)
|
||||
});
|
||||
|
||||
// Sccrutinzies
|
||||
|
||||
types.push(Argument {
|
||||
hidden: false,
|
||||
erased: false,
|
||||
name: Ident::generate("scrutinizer"),
|
||||
typ: Some(res_motive_ty),
|
||||
range,
|
||||
});
|
||||
|
||||
types.push(Argument {
|
||||
hidden: false,
|
||||
erased: false,
|
||||
name: Ident::generate("fun"),
|
||||
typ: Some(cons_type),
|
||||
range,
|
||||
});
|
||||
|
||||
// Motive with indices
|
||||
|
||||
let ret_ty = mk_var(Ident::generate("_res"));
|
||||
|
||||
let mut pats: Vec<Box<Pat>> = Vec::new();
|
||||
|
||||
let spine: Vec<Ident> = sum
|
||||
.fields
|
||||
.iter()
|
||||
.map(|(name, _, _)| name.with_name(|f| format!("{}_", f)))
|
||||
.collect();
|
||||
|
||||
pats.push(Box::new(Pat {
|
||||
data: concrete::pat::PatKind::App(
|
||||
sum.name.add_segment(sum.constructor.to_str()),
|
||||
spine
|
||||
.iter()
|
||||
.cloned()
|
||||
.map(|x| {
|
||||
Box::new(Pat {
|
||||
data: concrete::pat::PatKind::Var(PatIdent(x)),
|
||||
range,
|
||||
})
|
||||
})
|
||||
.collect(),
|
||||
),
|
||||
range,
|
||||
}));
|
||||
|
||||
pats.push(Box::new(Pat {
|
||||
data: concrete::pat::PatKind::Var(PatIdent(Ident::generate("fun_"))),
|
||||
range,
|
||||
}));
|
||||
|
||||
let body = mk_app(
|
||||
mk_var(Ident::generate("fun_")),
|
||||
spine
|
||||
.iter()
|
||||
.map(|arg| Binding::Positional(mk_var(arg.clone())))
|
||||
.collect(),
|
||||
);
|
||||
|
||||
let rules = vec![Box::new(Rule {
|
||||
name: name.clone(),
|
||||
pats,
|
||||
body,
|
||||
range,
|
||||
})];
|
||||
|
||||
Entry {
|
||||
name,
|
||||
docs: Vec::new(),
|
||||
args: types,
|
||||
typ: ret_ty,
|
||||
rules,
|
||||
range,
|
||||
attrs: Vec::new(),
|
||||
}
|
||||
}
|
||||
|
@ -14,6 +14,7 @@ kind-checker = { path = "../kind-checker" }
|
||||
kind-pass = { path = "../kind-pass" }
|
||||
kind-target-hvm = { path = "../kind-target-hvm" }
|
||||
|
||||
hvm = "0.1.81"
|
||||
strsim = "0.10.0"
|
||||
fxhash = "0.2.1"
|
||||
dashmap = "5.4.0"
|
||||
|
@ -61,7 +61,7 @@ impl From<DriverError> for DiagnosticFrame {
|
||||
DriverError::DefinedMultipleTimes(fst, snd) => DiagnosticFrame {
|
||||
code: 102,
|
||||
severity: Severity::Error,
|
||||
title: "Multiple paths for the same name".to_string(),
|
||||
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()
|
||||
|
@ -1,8 +1,12 @@
|
||||
use kind_pass::{desugar, erasure, expand};
|
||||
use kind_report::report::FileCache;
|
||||
use kind_span::SyntaxCtxIndex;
|
||||
|
||||
use kind_tree::{backend, concrete, desugared};
|
||||
use session::Session;
|
||||
use std::path::PathBuf;
|
||||
use std::{collections::HashSet, path::PathBuf};
|
||||
|
||||
use kind_checker as checker;
|
||||
|
||||
pub mod errors;
|
||||
pub mod resolution;
|
||||
@ -14,3 +18,78 @@ impl FileCache for Session {
|
||||
Some((path, &self.loaded_sources[ctx.0]))
|
||||
}
|
||||
}
|
||||
|
||||
pub fn type_check_book(session: &mut Session, path: &PathBuf) -> Option<desugared::Book> {
|
||||
let concrete_book = to_book(session, path)?;
|
||||
let desugared_book = desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)?;
|
||||
|
||||
let succeeded = checker::type_check(&desugared_book, session.diagnostic_sender.clone());
|
||||
|
||||
if !succeeded {
|
||||
return None;
|
||||
}
|
||||
|
||||
let erased = erasure::erase_book(
|
||||
&desugared_book,
|
||||
session.diagnostic_sender.clone(),
|
||||
HashSet::from_iter(vec!["Main".to_string()]),
|
||||
)?;
|
||||
|
||||
Some(erased)
|
||||
}
|
||||
|
||||
pub fn to_book(session: &mut Session, path: &PathBuf) -> Option<concrete::Book> {
|
||||
let mut concrete_book = resolution::parse_and_store_book(session, path)?;
|
||||
|
||||
expand::expand_book(&mut concrete_book);
|
||||
|
||||
Some(concrete_book)
|
||||
}
|
||||
|
||||
pub fn erase_book(session: &mut Session, path: &PathBuf) -> Option<desugared::Book> {
|
||||
let concrete_book = to_book(session, path)?;
|
||||
let desugared_book = desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)?;
|
||||
println!("Desugared: {}", desugared_book);
|
||||
erasure::erase_book(
|
||||
&desugared_book,
|
||||
session.diagnostic_sender.clone(),
|
||||
HashSet::from_iter(vec!["Main".to_string()]),
|
||||
)
|
||||
}
|
||||
|
||||
pub fn desugar_book(session: &mut Session, path: &PathBuf) -> Option<desugared::Book> {
|
||||
let concrete_book = to_book(session, path)?;
|
||||
desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)
|
||||
}
|
||||
|
||||
pub fn check_erasure_book(session: &mut Session, path: &PathBuf) -> Option<desugared::Book> {
|
||||
let concrete_book = to_book(session, path)?;
|
||||
let desugared_book = desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)?;
|
||||
erasure::erase_book(
|
||||
&desugared_book,
|
||||
session.diagnostic_sender.clone(),
|
||||
HashSet::from_iter(vec!["Main".to_string()]),
|
||||
)?;
|
||||
Some(desugared_book)
|
||||
}
|
||||
|
||||
pub fn compile_book_to_hvm(session: &mut Session, path: &PathBuf) -> Option<backend::File> {
|
||||
erase_book(session, path).map(kind_target_hvm::compile_book)
|
||||
}
|
||||
|
||||
pub fn execute_file(file: &backend::File) -> Box<backend::Term> {
|
||||
// TODO: Change to from_file when hvm support it
|
||||
let mut runtime = hvm::Runtime::from_code(&file.to_string()).unwrap();
|
||||
let main = runtime.alloc_code("Main").unwrap();
|
||||
runtime.run_io(main);
|
||||
runtime.normalize(main);
|
||||
runtime.readback(main)
|
||||
}
|
||||
|
||||
pub fn eval_in_checker(book: &desugared::Book) -> Box<backend::Term> {
|
||||
checker::eval_api(book)
|
||||
}
|
||||
|
||||
pub fn generate_checker(book: &desugared::Book) -> String {
|
||||
checker::gen_checker(book)
|
||||
}
|
||||
|
@ -3,8 +3,7 @@
|
||||
//! it returns a desugared book of all of the
|
||||
//! depedencies.
|
||||
|
||||
use kind_pass::erasure::{self};
|
||||
use kind_tree::desugared;
|
||||
use kind_pass::expand::uses::expand_uses;
|
||||
use std::collections::HashSet;
|
||||
use std::fs;
|
||||
use std::path::{Path, PathBuf};
|
||||
@ -12,7 +11,6 @@ use std::rc::Rc;
|
||||
use strsim::jaro;
|
||||
|
||||
use kind_pass::unbound::{self};
|
||||
use kind_pass::{desugar, expand};
|
||||
use kind_report::data::DiagnosticFrame;
|
||||
use kind_tree::concrete::{Book, Module, TopLevel};
|
||||
use kind_tree::symbol::{Ident, QualifiedIdent};
|
||||
@ -74,18 +72,22 @@ fn ident_to_path(
|
||||
}
|
||||
}
|
||||
|
||||
fn try_to_insert_new_name<'a>(session: &'a Session, ident: QualifiedIdent, book: &'a mut Book) {
|
||||
fn try_to_insert_new_name<'a>(failed: &mut bool, session: &'a Session, ident: QualifiedIdent, book: &'a mut Book) -> bool {
|
||||
if let Some(first_occorence) = book.names.get(ident.to_string().as_str()) {
|
||||
session
|
||||
.diagnostic_sender
|
||||
.send(DriverError::DefinedMultipleTimes(first_occorence.clone(), ident).into())
|
||||
.unwrap();
|
||||
*failed = true;
|
||||
false
|
||||
} else {
|
||||
book.names.insert(ident.to_string(), ident);
|
||||
true
|
||||
}
|
||||
}
|
||||
|
||||
fn module_to_book<'a>(
|
||||
failed: &mut bool,
|
||||
session: &'a Session,
|
||||
module: &Module,
|
||||
book: &'a mut Book,
|
||||
@ -96,25 +98,25 @@ fn module_to_book<'a>(
|
||||
match &entry {
|
||||
TopLevel::SumType(sum) => {
|
||||
public_names.insert(sum.name.to_string());
|
||||
try_to_insert_new_name(session, sum.name.clone(), book);
|
||||
book.count
|
||||
.insert(sum.name.to_string(), sum.extract_book_info());
|
||||
|
||||
if try_to_insert_new_name(failed, session, sum.name.clone(), book) {
|
||||
book.count.insert(sum.name.to_string(), sum.extract_book_info());
|
||||
book.entries.insert(sum.name.to_string(), entry.clone());
|
||||
}
|
||||
|
||||
for cons in &sum.constructors {
|
||||
let cons_ident = sum.name.add_segment(cons.name.to_str());
|
||||
let mut cons_ident = sum.name.add_segment(cons.name.to_str());
|
||||
cons_ident.range = cons.name.range.clone();
|
||||
if try_to_insert_new_name(failed, session, cons_ident.clone(), book) {
|
||||
public_names.insert(cons_ident.to_string());
|
||||
book.count
|
||||
.insert(cons_ident.to_string(), cons.extract_book_info(sum));
|
||||
try_to_insert_new_name(session, cons_ident, book);
|
||||
book.count.insert(cons_ident.to_string(), cons.extract_book_info(sum));
|
||||
}
|
||||
}
|
||||
}
|
||||
TopLevel::RecordType(rec) => {
|
||||
public_names.insert(rec.name.to_string());
|
||||
book.count
|
||||
.insert(rec.name.to_string(), rec.extract_book_info());
|
||||
try_to_insert_new_name(session, rec.name.clone(), book);
|
||||
try_to_insert_new_name(failed, session, rec.name.clone(), book);
|
||||
|
||||
book.entries.insert(rec.name.to_string(), entry.clone());
|
||||
|
||||
@ -124,10 +126,10 @@ fn module_to_book<'a>(
|
||||
cons_ident.to_string(),
|
||||
rec.extract_book_info_of_constructor(),
|
||||
);
|
||||
try_to_insert_new_name(session, cons_ident, book);
|
||||
try_to_insert_new_name(failed, session, cons_ident, book);
|
||||
}
|
||||
TopLevel::Entry(entr) => {
|
||||
try_to_insert_new_name(session, entr.name.clone(), book);
|
||||
try_to_insert_new_name(failed, session, entr.name.clone(), book);
|
||||
public_names.insert(entr.name.to_string());
|
||||
book.count
|
||||
.insert(entr.name.to_string(), entr.extract_book_info());
|
||||
@ -150,7 +152,7 @@ fn parse_and_store_book_by_identifier<'a>(
|
||||
|
||||
match ident_to_path(&session.root, ident, true) {
|
||||
Ok(Some(path)) => parse_and_store_book_by_path(session, &path, book),
|
||||
Ok(None) => false,
|
||||
Ok(None) => true,
|
||||
Err(err) => {
|
||||
session.diagnostic_sender.send(err).unwrap();
|
||||
true
|
||||
@ -184,14 +186,23 @@ fn parse_and_store_book_by_path<'a>(
|
||||
let (mut module, mut failed) =
|
||||
kind_parser::parse_book(session.diagnostic_sender.clone(), ctx_id, &input);
|
||||
|
||||
let (_, unbound_top_level) =
|
||||
let (unbound_vars, unbound_top_level) =
|
||||
unbound::get_module_unbound(session.diagnostic_sender.clone(), &mut module);
|
||||
|
||||
for idents in unbound_top_level.values() {
|
||||
failed |= parse_and_store_book_by_identifier(session, &idents[0], book);
|
||||
for idents in unbound_vars.values() {
|
||||
unbound_variable(session, book, idents);
|
||||
failed = true;
|
||||
}
|
||||
|
||||
module_to_book(session, &module, book);
|
||||
for idents in unbound_top_level.values() {
|
||||
if idents.iter().any(|x| !x.used_by_sugar) {
|
||||
failed |= parse_and_store_book_by_identifier(session, &idents[0], book);
|
||||
}
|
||||
}
|
||||
|
||||
failed |= expand_uses(&mut module, session.diagnostic_sender.clone());
|
||||
|
||||
module_to_book(&mut failed, session, &module, book);
|
||||
|
||||
failed
|
||||
}
|
||||
@ -212,59 +223,11 @@ fn unbound_variable(session: &mut Session, book: &Book, idents: &[Ident]) {
|
||||
pub fn parse_and_store_book(session: &mut Session, path: &PathBuf) -> Option<Book> {
|
||||
let mut book = Book::default();
|
||||
|
||||
let mut failed = parse_and_store_book_by_path(session, path, &mut book);
|
||||
let failed = parse_and_store_book_by_path(session, path, &mut book);
|
||||
|
||||
let (unbounds, unbounded_top) = unbound::get_book_unbound(session.diagnostic_sender.clone(), &mut book);
|
||||
|
||||
for idents in unbounds.values() {
|
||||
unbound_variable(session, &book, idents);
|
||||
failed = true;
|
||||
}
|
||||
|
||||
for idents in unbounded_top.values() {
|
||||
if !book.entries.contains_key(&idents[0].to_string()) {
|
||||
let vec = idents.iter().map(|x| x.to_ident()).collect::<Vec<Ident>>();
|
||||
unbound_variable(session, &book, vec.as_slice());
|
||||
failed = true;
|
||||
}
|
||||
}
|
||||
|
||||
if !unbounds.is_empty() || failed {
|
||||
if failed {
|
||||
None
|
||||
} else {
|
||||
Some(book)
|
||||
}
|
||||
}
|
||||
|
||||
pub fn type_check_book(session: &mut Session, path: &PathBuf) -> Option<desugared::Book> {
|
||||
let mut concrete_book = parse_and_store_book(session, path)?;
|
||||
|
||||
expand::expand_book(&mut concrete_book);
|
||||
|
||||
let desugared_book = desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)?;
|
||||
|
||||
let succeeded = kind_checker::type_check(&desugared_book, session.diagnostic_sender.clone());
|
||||
|
||||
if !succeeded {
|
||||
return None;
|
||||
}
|
||||
|
||||
let erased = erasure::erase_book(
|
||||
&desugared_book,
|
||||
session.diagnostic_sender.clone(),
|
||||
HashSet::from_iter(vec!["Main".to_string()]),
|
||||
)?;
|
||||
|
||||
Some(erased)
|
||||
}
|
||||
|
||||
pub fn compile_book(session: &mut Session, path: &PathBuf) -> Option<()> {
|
||||
let book = type_check_book(session, path);
|
||||
match book {
|
||||
None => None,
|
||||
Some(book) => {
|
||||
println!("{}", kind_target_hvm::compile_book(book));
|
||||
Some(())
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -9,3 +9,5 @@ edition = "2021"
|
||||
kind-span = { path = "../kind-span" }
|
||||
kind-tree = { path = "../kind-tree" }
|
||||
kind-report = { path = "../kind-report" }
|
||||
|
||||
fxhash = "0.2.1"
|
@ -28,6 +28,8 @@ pub enum SyntaxError {
|
||||
Unclosed(Range),
|
||||
IgnoreRestShouldBeOnTheEnd(Range),
|
||||
UnusedDocString(Range),
|
||||
CannotUseUse(Range),
|
||||
ImportsCannotHaveAlias(Range),
|
||||
}
|
||||
|
||||
fn encode_name(encode: EncodeSequence) -> &'static str {
|
||||
@ -223,10 +225,10 @@ impl From<SyntaxError> for DiagnosticFrame {
|
||||
main: true,
|
||||
}],
|
||||
},
|
||||
SyntaxError::UnexpectedToken(_token, range, _expect) => DiagnosticFrame {
|
||||
SyntaxError::UnexpectedToken(token, range, _expect) => DiagnosticFrame {
|
||||
code: 13,
|
||||
severity: Severity::Error,
|
||||
title: "Unexpected token.".to_string(),
|
||||
title: format!("Unexpected token {:?}.", token),
|
||||
subtitles: vec![],
|
||||
hints: vec![],
|
||||
positions: vec![Marker {
|
||||
@ -251,6 +253,34 @@ impl From<SyntaxError> for DiagnosticFrame {
|
||||
main: true,
|
||||
}],
|
||||
},
|
||||
SyntaxError::CannotUseUse(range) => DiagnosticFrame {
|
||||
code: 14,
|
||||
severity: Severity::Error,
|
||||
title: "Can only use the 'use' statement in the beggining of the file".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![],
|
||||
positions: vec![Marker {
|
||||
position: range,
|
||||
color: Color::Fst,
|
||||
text: "Move it to the beggining".to_string(),
|
||||
no_code: false,
|
||||
main: true,
|
||||
}],
|
||||
},
|
||||
SyntaxError::ImportsCannotHaveAlias(range) => DiagnosticFrame {
|
||||
code: 14,
|
||||
severity: Severity::Error,
|
||||
title: "The upper cased name cannot have an alias".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![],
|
||||
positions: vec![Marker {
|
||||
position: range,
|
||||
color: Color::Fst,
|
||||
text: "Use the entire name here!".to_string(),
|
||||
no_code: false,
|
||||
main: true,
|
||||
}],
|
||||
},
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -78,7 +78,7 @@ impl<'a> Parser<'a> {
|
||||
&& self.peek(2).same_variant(&Token::Colon)
|
||||
}
|
||||
|
||||
pub fn is_named(&self) -> bool {
|
||||
pub fn is_named_parameter(&self) -> bool {
|
||||
self.get().same_variant(&Token::LPar)
|
||||
&& self.peek(1).is_lower_id()
|
||||
&& self.peek(2).same_variant(&Token::Eq)
|
||||
@ -128,7 +128,7 @@ impl<'a> Parser<'a> {
|
||||
let range = self.range();
|
||||
let (start, end) =
|
||||
eat_single!(self, Token::UpperId(start, end) => (start.clone(), end.clone()))?;
|
||||
let ident = QualifiedIdent::new_static(start.clone(), end.clone(), range);
|
||||
let ident = QualifiedIdent::new_static(start.as_str(), end, range);
|
||||
Ok(ident)
|
||||
}
|
||||
|
||||
@ -210,12 +210,12 @@ impl<'a> Parser<'a> {
|
||||
}))
|
||||
}
|
||||
|
||||
fn parse_data(&mut self) -> Result<Box<Expr>, SyntaxError> {
|
||||
fn parse_single_upper(&mut self) -> Result<Box<Expr>, SyntaxError> {
|
||||
let id = self.parse_upper_id()?;
|
||||
let data = match id.to_string().as_str() {
|
||||
"Type" => ExprKind::Lit(Literal::Type),
|
||||
"U60" => ExprKind::Lit(Literal::U60),
|
||||
_ => ExprKind::Constr(id.clone()),
|
||||
_ => ExprKind::Constr(id.clone(), vec![]),
|
||||
};
|
||||
Ok(Box::new(Expr {
|
||||
range: id.range,
|
||||
@ -223,6 +223,21 @@ impl<'a> Parser<'a> {
|
||||
}))
|
||||
}
|
||||
|
||||
fn parse_data(&mut self, multiline: bool) -> Result<Box<Expr>, SyntaxError> {
|
||||
let id = self.parse_upper_id()?;
|
||||
let mut range = id.range;
|
||||
let data = match id.to_string().as_str() {
|
||||
"Type" => ExprKind::Lit(Literal::Type),
|
||||
"U60" => ExprKind::Lit(Literal::U60),
|
||||
_ => {
|
||||
let (range_end, spine) = self.parse_call_tail(id.range, multiline)?;
|
||||
range = range_end;
|
||||
ExprKind::Constr(id, spine)
|
||||
}
|
||||
};
|
||||
Ok(Box::new(Expr { range, data }))
|
||||
}
|
||||
|
||||
fn parse_num(&mut self, num: u64) -> Result<Box<Expr>, SyntaxError> {
|
||||
let range = self.range();
|
||||
self.advance();
|
||||
@ -355,14 +370,15 @@ impl<'a> Parser<'a> {
|
||||
pub fn parse_atom(&mut self) -> Result<Box<Expr>, SyntaxError> {
|
||||
self.ignore_docs();
|
||||
match self.get().clone() {
|
||||
Token::UpperId(_, _) => self.parse_single_upper(),
|
||||
Token::LowerId(_) => self.parse_var(),
|
||||
Token::UpperId(_, _) => self.parse_data(),
|
||||
Token::Num(num) => self.parse_num(num),
|
||||
Token::Char(chr) => self.parse_char(chr),
|
||||
Token::Str(str) => self.parse_str(str),
|
||||
Token::Help(str) => self.parse_help(str),
|
||||
Token::LBracket => self.parse_list(),
|
||||
Token::LPar => self.parse_paren(),
|
||||
Token::Hole => self.parse_hole(),
|
||||
Token::Float(_, _) => todo!(),
|
||||
_ => self.fail(vec![Token::LowerId("".to_string())]),
|
||||
}
|
||||
@ -370,7 +386,7 @@ impl<'a> Parser<'a> {
|
||||
|
||||
fn parse_binding(&mut self) -> Result<Binding, SyntaxError> {
|
||||
self.ignore_docs();
|
||||
if self.is_named() {
|
||||
if self.is_named_parameter() {
|
||||
let start = self.range();
|
||||
self.advance(); // '('
|
||||
let name = self.parse_id()?;
|
||||
@ -385,10 +401,30 @@ impl<'a> Parser<'a> {
|
||||
}
|
||||
|
||||
fn parse_call(&mut self, multiline: bool) -> Result<Box<Expr>, SyntaxError> {
|
||||
if self.get().is_upper_id() {
|
||||
self.parse_data(multiline)
|
||||
} else {
|
||||
let head = self.parse_atom()?;
|
||||
let start = head.range;
|
||||
let (end, spine) = self.parse_call_tail(start, multiline)?;
|
||||
if spine.is_empty() {
|
||||
Ok(head)
|
||||
} else {
|
||||
Ok(Box::new(Expr {
|
||||
data: ExprKind::App(head, spine),
|
||||
range: start.mix(end),
|
||||
}))
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn parse_call_tail(
|
||||
&mut self,
|
||||
start: Range,
|
||||
multiline: bool,
|
||||
) -> Result<(Range, Vec<Binding>), SyntaxError> {
|
||||
let mut spine = Vec::new();
|
||||
let mut end = head.range;
|
||||
let mut end = start;
|
||||
while (!self.is_linebreak() || multiline) && !self.get().same_variant(&Token::Eof) {
|
||||
let res = self.try_single(&|parser| parser.parse_binding())?;
|
||||
match res {
|
||||
@ -399,14 +435,7 @@ impl<'a> Parser<'a> {
|
||||
None => break,
|
||||
}
|
||||
}
|
||||
if spine.is_empty() {
|
||||
Ok(head)
|
||||
} else {
|
||||
Ok(Box::new(Expr {
|
||||
data: ExprKind::App(head, spine),
|
||||
range: start.mix(end),
|
||||
}))
|
||||
}
|
||||
Ok((end, spine))
|
||||
}
|
||||
|
||||
fn parse_arrow(&mut self, multiline: bool) -> Result<Box<Expr>, SyntaxError> {
|
||||
@ -640,6 +669,15 @@ impl<'a> Parser<'a> {
|
||||
}))
|
||||
}
|
||||
|
||||
fn parse_hole(&mut self) -> Result<Box<Expr>, SyntaxError> {
|
||||
let start = self.range();
|
||||
self.advance(); // '_'
|
||||
Ok(Box::new(Expr {
|
||||
data: ExprKind::Hole,
|
||||
range: start,
|
||||
}))
|
||||
}
|
||||
|
||||
fn parse_if(&mut self) -> Result<Box<Expr>, SyntaxError> {
|
||||
let start = self.range();
|
||||
self.advance(); // 'if'
|
||||
|
@ -56,9 +56,9 @@ impl<'a> Lexer<'a> {
|
||||
|
||||
/// Lex a base-10 digit.
|
||||
fn lex_digit(&mut self, start: usize) -> (Token, Range) {
|
||||
let num = self.accumulate_while(&|x| x.is_ascii_digit());
|
||||
let num = self.accumulate_while(&|x| x.is_ascii_digit() || x == '_');
|
||||
(
|
||||
Token::Num(num.parse::<u64>().unwrap()),
|
||||
Token::Num(num.replace('_', "").parse::<u64>().unwrap()),
|
||||
self.mk_range(start),
|
||||
)
|
||||
}
|
||||
@ -67,8 +67,8 @@ impl<'a> Lexer<'a> {
|
||||
/// character that indicates the encoding
|
||||
fn lex_base(&mut self, start: usize, base: u32, err: EncodeSequence) -> (Token, Range) {
|
||||
self.next_char();
|
||||
let num = self.accumulate_while(&|x| x.is_digit(base));
|
||||
if let Ok(res) = u64::from_str_radix(num, base) {
|
||||
let num = self.accumulate_while(&|x| x.is_digit(base) || x == '_');
|
||||
if let Ok(res) = u64::from_str_radix(&num.replace('_', ""), base) {
|
||||
(Token::Num(res), self.mk_range(start))
|
||||
} else {
|
||||
(
|
||||
|
@ -29,7 +29,7 @@ fn is_valid_id(chr: char) -> bool {
|
||||
}
|
||||
|
||||
fn is_valid_upper_start(chr: char) -> bool {
|
||||
matches!(chr, 'A'..='Z' | '_')
|
||||
matches!(chr, 'A'..='Z')
|
||||
}
|
||||
|
||||
fn is_valid_id_start(chr: char) -> bool {
|
||||
@ -51,13 +51,15 @@ impl<'a> Lexer<'a> {
|
||||
|
||||
pub fn to_keyword(data: &str) -> Token {
|
||||
match data {
|
||||
"_" => Token::Hole,
|
||||
"ask" => Token::Ask,
|
||||
"do" => Token::Do,
|
||||
"if" => Token::If,
|
||||
"else" => Token::Else,
|
||||
"match" => Token::Match,
|
||||
"let" => Token::Let,
|
||||
"open" => Token::Open,
|
||||
"use" => Token::Use,
|
||||
"as" => Token::As,
|
||||
"return" => Token::Return,
|
||||
"type" => Token::Type,
|
||||
"record" => Token::Record,
|
||||
@ -102,7 +104,7 @@ impl<'a> Lexer<'a> {
|
||||
}
|
||||
}
|
||||
c if c.is_ascii_digit() => self.lex_number(),
|
||||
c if is_valid_upper_start(*c).clone() => {
|
||||
c if is_valid_upper_start(*c) => {
|
||||
let first_part = self.accumulate_while(&is_valid_id).to_string();
|
||||
let peek = self.peekable.peek().cloned();
|
||||
let auxiliar_part = match peek {
|
||||
@ -114,7 +116,7 @@ impl<'a> Lexer<'a> {
|
||||
_ => None,
|
||||
};
|
||||
(
|
||||
Token::UpperId(first_part.to_string(), auxiliar_part),
|
||||
Token::UpperId(first_part, auxiliar_part),
|
||||
self.mk_range(start),
|
||||
)
|
||||
}
|
||||
|
@ -34,10 +34,11 @@ pub enum Token {
|
||||
Ask,
|
||||
Return,
|
||||
Let,
|
||||
Open,
|
||||
Type,
|
||||
Record,
|
||||
Constructor,
|
||||
Use,
|
||||
As,
|
||||
|
||||
// Literals
|
||||
Char(char),
|
||||
@ -100,4 +101,8 @@ impl Token {
|
||||
pub fn is_num(&self) -> bool {
|
||||
matches!(self, Token::Num(_))
|
||||
}
|
||||
|
||||
pub fn is_eof(&self) -> bool {
|
||||
matches!(self, Token::Eof)
|
||||
}
|
||||
}
|
||||
|
@ -68,6 +68,15 @@ impl<'a> Parser<'a> {
|
||||
}))
|
||||
}
|
||||
|
||||
pub fn parse_pat_hole(&mut self) -> Result<Box<Pat>, SyntaxError> {
|
||||
let range = self.range();
|
||||
self.eat_variant(Token::Hole)?;
|
||||
Ok(Box::new(Pat {
|
||||
range,
|
||||
data: PatKind::Hole,
|
||||
}))
|
||||
}
|
||||
|
||||
fn parse_pat_list(&mut self) -> Result<Box<Pat>, SyntaxError> {
|
||||
let range = self.range();
|
||||
self.advance(); // '['
|
||||
@ -123,6 +132,8 @@ impl<'a> Parser<'a> {
|
||||
self.parse_pat_single_cons()
|
||||
} else if self.check_actual(Token::LBrace) {
|
||||
self.parse_pat_list()
|
||||
} else if self.check_actual(Token::Hole) {
|
||||
self.parse_pat_hole()
|
||||
} else {
|
||||
self.fail(vec![])
|
||||
}
|
||||
|
@ -86,8 +86,12 @@ impl<'a> Parser<'a> {
|
||||
}
|
||||
|
||||
pub fn eat_closing_keyword(&mut self, expect: Token, range: Range) -> Result<(), SyntaxError> {
|
||||
if !self.check_and_eat(expect) {
|
||||
if !self.check_and_eat(expect.clone()) {
|
||||
if self.get().is_eof() {
|
||||
Err(SyntaxError::Unclosed(range))
|
||||
} else {
|
||||
self.fail(vec![expect])
|
||||
}
|
||||
} else {
|
||||
Ok(())
|
||||
}
|
||||
|
@ -1,3 +1,5 @@
|
||||
use fxhash::FxHashMap;
|
||||
use kind_tree::concrete::pat::{Pat, PatIdent, PatKind};
|
||||
/// Parses all of the top level structures
|
||||
/// like Book, Entry, Rule and Argument.
|
||||
use kind_tree::concrete::{Argument, Attribute, Entry, Module, Rule, Telescope, TopLevel};
|
||||
@ -18,6 +20,7 @@ impl<'a> Parser<'a> {
|
||||
pub fn is_top_level_entry_continuation(&self) -> bool {
|
||||
self.peek(1).same_variant(&Token::Colon) // ':'
|
||||
|| self.peek(1).same_variant(&Token::LPar) // '('
|
||||
|| self.peek(1).same_variant(&Token::LBrace) // '{'
|
||||
|| self.peek(1).same_variant(&Token::Less) // '<'
|
||||
|| self.peek(1).same_variant(&Token::Minus) // '-'
|
||||
|| self.peek(1).same_variant(&Token::Plus) // '+'
|
||||
@ -81,7 +84,7 @@ impl<'a> Parser<'a> {
|
||||
let start = self.range();
|
||||
let ident;
|
||||
if let Token::UpperId(name_id, ext) = self.get() {
|
||||
let qual = QualifiedIdent::new_static(name_id.clone(), ext.clone(), start);
|
||||
let qual = QualifiedIdent::new_static(name_id.as_str(), ext.clone(), start);
|
||||
if qual.to_string() == name {
|
||||
ident = self.parse_upper_id()?;
|
||||
} else {
|
||||
@ -148,6 +151,55 @@ impl<'a> Parser<'a> {
|
||||
|
||||
self.eat_variant(Token::Colon)?;
|
||||
let typ = self.parse_expr(false)?;
|
||||
|
||||
if self.check_actual(Token::LBrace) {
|
||||
let start = self.range();
|
||||
|
||||
self.eat_variant(Token::LBrace)?;
|
||||
|
||||
let body = self.parse_expr(true)?;
|
||||
|
||||
let end = self.range();
|
||||
self.eat_closing_keyword(Token::RBrace, start)?;
|
||||
|
||||
let mut rules = vec![Box::new(Rule {
|
||||
name: ident.clone(),
|
||||
pats: args
|
||||
.iter()
|
||||
.map(|x| {
|
||||
Box::new(Pat {
|
||||
range: x.range,
|
||||
data: PatKind::Var(PatIdent(x.name.clone())),
|
||||
})
|
||||
})
|
||||
.collect(),
|
||||
body,
|
||||
range: end,
|
||||
})];
|
||||
loop {
|
||||
let res = self.try_single(&|parser| parser.parse_rule(ident.to_string()))?;
|
||||
match res {
|
||||
Some(res) => rules.push(res),
|
||||
None => break,
|
||||
}
|
||||
}
|
||||
let end = rules.last().as_ref().map(|x| x.range).unwrap_or(typ.range);
|
||||
|
||||
// Better error message when you have change the name of the function
|
||||
if self.get().is_upper_id() && !self.is_top_level_entry_continuation() {
|
||||
return Err(SyntaxError::NotAClauseOfDef(ident.range, self.range()));
|
||||
}
|
||||
|
||||
Ok(Entry {
|
||||
name: ident,
|
||||
docs,
|
||||
args: Telescope::new(args),
|
||||
typ,
|
||||
rules,
|
||||
attrs,
|
||||
range: start.mix(end),
|
||||
})
|
||||
} else {
|
||||
let mut rules = Vec::new();
|
||||
loop {
|
||||
let res = self.try_single(&|parser| parser.parse_rule(ident.to_string()))?;
|
||||
@ -173,6 +225,7 @@ impl<'a> Parser<'a> {
|
||||
range: start.mix(end),
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
pub fn parse_top_level(&mut self) -> Result<TopLevel, SyntaxError> {
|
||||
let docs = self.parse_docs()?;
|
||||
@ -184,13 +237,56 @@ impl<'a> Parser<'a> {
|
||||
Ok(TopLevel::RecordType(self.parse_record_def(docs, attrs)?))
|
||||
} else if self.is_top_level_entry_continuation() {
|
||||
Ok(TopLevel::Entry(self.parse_entry(docs, attrs)?))
|
||||
} else if self.check_actual(Token::Use) {
|
||||
Err(SyntaxError::CannotUseUse(self.range()))
|
||||
} else {
|
||||
self.fail(vec![])
|
||||
}
|
||||
}
|
||||
|
||||
pub fn parse_use(&mut self) -> Result<(String, String), SyntaxError> {
|
||||
self.eat_variant(Token::Use)?;
|
||||
let origin = self.parse_upper_id()?;
|
||||
self.eat_variant(Token::As)?;
|
||||
let alias = self.parse_upper_id()?;
|
||||
|
||||
match (origin, alias) {
|
||||
(
|
||||
QualifiedIdent {
|
||||
aux: Some(_),
|
||||
range,
|
||||
..
|
||||
},
|
||||
_,
|
||||
)
|
||||
| (
|
||||
_,
|
||||
QualifiedIdent {
|
||||
aux: Some(_),
|
||||
range,
|
||||
..
|
||||
},
|
||||
) => Err(SyntaxError::ImportsCannotHaveAlias(range)),
|
||||
(origin, alias) => Ok((origin.to_string(), alias.to_string())),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn parse_module(&mut self) -> Module {
|
||||
let mut entries: Vec<TopLevel> = Vec::new();
|
||||
let mut uses: FxHashMap<String, String> = Default::default();
|
||||
|
||||
while self.get().same_variant(&Token::Use) {
|
||||
match self.parse_use() {
|
||||
Ok((origin, alias)) => {
|
||||
uses.insert(alias, origin);
|
||||
}
|
||||
Err(err) => {
|
||||
self.errs.send(err.into()).unwrap();
|
||||
self.failed = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
while !self.get().same_variant(&Token::Eof) {
|
||||
match self.parse_top_level() {
|
||||
@ -216,6 +312,6 @@ impl<'a> Parser<'a> {
|
||||
}
|
||||
}
|
||||
|
||||
Module { entries }
|
||||
Module { entries, uses }
|
||||
}
|
||||
}
|
||||
|
@ -4,7 +4,7 @@ use kind_tree::concrete::expr::Expr;
|
||||
|
||||
use kind_tree::concrete::{Binding, ExprKind};
|
||||
use kind_tree::desugared;
|
||||
use kind_tree::symbol::{QualifiedIdent};
|
||||
use kind_tree::symbol::QualifiedIdent;
|
||||
|
||||
use crate::errors::PassError;
|
||||
|
||||
@ -16,6 +16,7 @@ impl<'a> DesugarState<'a> {
|
||||
range: Range,
|
||||
head: QualifiedIdent,
|
||||
spine: Vec<Box<desugared::Expr>>,
|
||||
create_var: bool,
|
||||
) -> Option<Vec<Box<desugared::Expr>>> {
|
||||
let entry = self.old_book.get_count_garanteed(head.to_string().as_str());
|
||||
|
||||
@ -27,7 +28,11 @@ impl<'a> DesugarState<'a> {
|
||||
let mut spine_iter = spine.iter();
|
||||
for arg in entry.arguments.iter() {
|
||||
if arg.hidden {
|
||||
if create_var {
|
||||
arguments.push(desugared::Expr::var(self.gen_name(arg.range)))
|
||||
} else {
|
||||
arguments.push(self.gen_hole_expr())
|
||||
}
|
||||
} else {
|
||||
arguments.push(spine_iter.next().unwrap().to_owned())
|
||||
}
|
||||
@ -49,8 +54,9 @@ impl<'a> DesugarState<'a> {
|
||||
range: Range,
|
||||
head: QualifiedIdent,
|
||||
spine: Vec<Box<desugared::Expr>>,
|
||||
create_var_on_hidden: bool,
|
||||
) -> Box<desugared::Expr> {
|
||||
match self.make_desugared_spine(range, head.clone(), spine) {
|
||||
match self.make_desugared_spine(range, head.clone(), spine, create_var_on_hidden) {
|
||||
Some(spine) => desugared::Expr::ctr(range, head, spine),
|
||||
None => desugared::Expr::err(range),
|
||||
}
|
||||
@ -61,21 +67,17 @@ impl<'a> DesugarState<'a> {
|
||||
range: Range,
|
||||
head: QualifiedIdent,
|
||||
spine: Vec<Box<desugared::Expr>>,
|
||||
create_var_on_hidden: bool,
|
||||
) -> Box<desugared::Expr> {
|
||||
match self.make_desugared_spine(range, head.clone(), spine) {
|
||||
match self.make_desugared_spine(range, head.clone(), spine, create_var_on_hidden) {
|
||||
Some(spine) => desugared::Expr::fun(range, head, spine),
|
||||
None => desugared::Expr::err(range),
|
||||
}
|
||||
}
|
||||
|
||||
pub(crate) fn desugar_app(
|
||||
&mut self,
|
||||
range: Range,
|
||||
head: &Expr,
|
||||
spine: &[Binding],
|
||||
) -> Box<desugared::Expr> {
|
||||
pub(crate) fn desugar_app(&mut self, range: Range, head: &Expr) -> Box<desugared::Expr> {
|
||||
match &head.data {
|
||||
ExprKind::Constr(entry_name) => {
|
||||
ExprKind::Constr(entry_name, spine) => {
|
||||
let entry = self
|
||||
.old_book
|
||||
.get_count_garanteed(entry_name.to_string().as_str());
|
||||
@ -98,7 +100,8 @@ impl<'a> DesugarState<'a> {
|
||||
}
|
||||
} else if entry.arguments.len() != spine.len() {
|
||||
self.send_err(PassError::IncorrectArity(
|
||||
head.locate(),
|
||||
entry_name.range,
|
||||
spine.iter().map(|x| x.locate()).collect(),
|
||||
entry.arguments.len(),
|
||||
hidden,
|
||||
));
|
||||
@ -168,7 +171,7 @@ impl<'a> DesugarState<'a> {
|
||||
span: Span::Locatable(range),
|
||||
})
|
||||
}
|
||||
_ => {
|
||||
ExprKind::App(head, spine) => {
|
||||
let mut new_spine = Vec::new();
|
||||
let new_head = self.desugar_expr(head);
|
||||
for arg in spine {
|
||||
@ -182,6 +185,7 @@ impl<'a> DesugarState<'a> {
|
||||
}
|
||||
desugared::Expr::app(range, new_head, new_spine)
|
||||
}
|
||||
_ => panic!("Internal Error: This function should be used with app and constr"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -52,7 +52,7 @@ impl<'a> DesugarState<'a> {
|
||||
.collect();
|
||||
|
||||
if !jump_rest && !names.is_empty() {
|
||||
self.send_err(PassError::NoCoverage(type_info.0.clone(), names))
|
||||
self.send_err(PassError::NoFieldCoverage(*type_info.0, names))
|
||||
}
|
||||
|
||||
ordered_fields
|
||||
@ -60,16 +60,17 @@ impl<'a> DesugarState<'a> {
|
||||
|
||||
pub(crate) fn desugar_destruct(
|
||||
&mut self,
|
||||
range: Range,
|
||||
binding: &expr::Destruct,
|
||||
val: Box<desugared::Expr>,
|
||||
next: &dyn Fn(&mut Self) -> Box<desugared::Expr>,
|
||||
on_ident: &dyn Fn(&mut Self, &Ident) -> Box<desugared::Expr>,
|
||||
) -> Box<desugared::Expr> {
|
||||
match binding {
|
||||
Destruct::Destruct(destruct_range, typ, case, jump_rest) => {
|
||||
let entry = self.old_book.get_entry_garanteed(&typ.to_string());
|
||||
Destruct::Destruct(_, typ, case, jump_rest) => {
|
||||
let entry = self.old_book.entries.get(&typ.to_string());
|
||||
|
||||
let record = if let TopLevel::RecordType(record) = entry {
|
||||
let record = if let Some(TopLevel::RecordType(record)) = entry {
|
||||
record
|
||||
} else {
|
||||
self.send_err(PassError::LetDestructOnlyForRecord(typ.range));
|
||||
@ -101,10 +102,10 @@ impl<'a> DesugarState<'a> {
|
||||
|
||||
let spine = vec![
|
||||
val,
|
||||
desugared::Expr::unfold_lambda(*destruct_range, &arguments, next(self)),
|
||||
desugared::Expr::unfold_lambda(range, &arguments, next(self)),
|
||||
];
|
||||
|
||||
self.mk_desugared_fun(*destruct_range, open_id, spine)
|
||||
self.mk_desugared_fun(range, open_id, spine, false)
|
||||
}
|
||||
Destruct::Ident(name) => on_ident(self, name),
|
||||
}
|
||||
@ -119,6 +120,7 @@ impl<'a> DesugarState<'a> {
|
||||
) -> Box<desugared::Expr> {
|
||||
let res_val = self.desugar_expr(val);
|
||||
self.desugar_destruct(
|
||||
next.range,
|
||||
binding,
|
||||
res_val,
|
||||
&|this| this.desugar_expr(next),
|
||||
@ -138,7 +140,7 @@ impl<'a> DesugarState<'a> {
|
||||
range: Range,
|
||||
match_: &expr::Match,
|
||||
) -> Box<desugared::Expr> {
|
||||
let entry = self.old_book.get_entry_garanteed(&match_.typ.to_string());
|
||||
let entry = self.old_book.entries.get(&match_.typ.to_string()).unwrap();
|
||||
|
||||
let sum = if let TopLevel::SumType(sum) = entry {
|
||||
sum
|
||||
@ -234,6 +236,7 @@ impl<'a> DesugarState<'a> {
|
||||
match_.typ.range,
|
||||
match_id,
|
||||
[prefix.as_slice(), lambdas.as_slice()].concat(),
|
||||
false,
|
||||
)
|
||||
}
|
||||
}
|
||||
|
@ -52,6 +52,7 @@ impl<'a> DesugarState<'a> {
|
||||
range,
|
||||
bind_ident.clone(),
|
||||
vec![expr, desugared::Expr::lambda(range, name, next)],
|
||||
false,
|
||||
)
|
||||
};
|
||||
|
||||
@ -68,6 +69,7 @@ impl<'a> DesugarState<'a> {
|
||||
let name = self.gen_name(sttm.range);
|
||||
|
||||
let res_destruct = self.desugar_destruct(
|
||||
next.range,
|
||||
&concrete::Destruct::Destruct(*a, b.to_owned(), c.to_owned(), *d),
|
||||
desugared::Expr::var(name.clone()),
|
||||
&|this| this.desugar_sttm(bind_ident, pure_ident, next),
|
||||
@ -84,6 +86,7 @@ impl<'a> DesugarState<'a> {
|
||||
concrete::SttmKind::Let(destruct, val, next) => {
|
||||
let res_val = self.desugar_expr(&val.clone());
|
||||
self.desugar_destruct(
|
||||
next.range,
|
||||
destruct,
|
||||
res_val,
|
||||
&|this| this.desugar_sttm(bind_ident, pure_ident, next),
|
||||
@ -99,7 +102,7 @@ impl<'a> DesugarState<'a> {
|
||||
}
|
||||
concrete::SttmKind::Return(expr) => {
|
||||
let res_expr = self.desugar_expr(expr);
|
||||
self.mk_desugared_fun(expr.locate(), pure_ident.clone(), vec![res_expr])
|
||||
self.mk_desugared_fun(expr.locate(), pure_ident.clone(), vec![res_expr], false)
|
||||
}
|
||||
concrete::SttmKind::RetExpr(expr) => self.desugar_expr(expr),
|
||||
}
|
||||
@ -132,7 +135,7 @@ impl<'a> DesugarState<'a> {
|
||||
typ: &expr::Expr,
|
||||
body: &expr::Expr,
|
||||
) -> Box<desugared::Expr> {
|
||||
let sigma = QualifiedIdent::new_static("Sigma".to_string(), None, range);
|
||||
let sigma = QualifiedIdent::new_static("Sigma", None, range);
|
||||
|
||||
let entry = self.old_book.entries.get(sigma.to_string().as_str());
|
||||
if entry.is_none() {
|
||||
@ -142,7 +145,7 @@ impl<'a> DesugarState<'a> {
|
||||
|
||||
let name = match name {
|
||||
Some(ident) => ident.clone(),
|
||||
None => Ident::generate("_"),
|
||||
None => Ident::generate("_var"),
|
||||
};
|
||||
|
||||
let spine = vec![
|
||||
@ -150,7 +153,7 @@ impl<'a> DesugarState<'a> {
|
||||
desugared::Expr::lambda(range, name, self.desugar_expr(body)),
|
||||
];
|
||||
|
||||
self.mk_desugared_ctr(range, sigma, spine)
|
||||
self.mk_desugared_ctr(range, sigma, spine, false)
|
||||
}
|
||||
|
||||
pub(crate) fn desugar_list(
|
||||
@ -158,7 +161,7 @@ impl<'a> DesugarState<'a> {
|
||||
range: Range,
|
||||
expr: &[expr::Expr],
|
||||
) -> Box<desugared::Expr> {
|
||||
let list_ident = QualifiedIdent::new_static("List".to_string(), None, range);
|
||||
let list_ident = QualifiedIdent::new_static("List", None, range);
|
||||
let cons_ident = list_ident.add_segment("cons");
|
||||
let nil_ident = list_ident.add_segment("nil");
|
||||
|
||||
@ -172,10 +175,10 @@ impl<'a> DesugarState<'a> {
|
||||
}
|
||||
|
||||
expr.iter().rfold(
|
||||
self.mk_desugared_ctr(range, nil_ident, Vec::new()),
|
||||
self.mk_desugared_ctr(range, nil_ident, Vec::new(), false),
|
||||
|res, elem| {
|
||||
let spine = vec![self.desugar_expr(elem), res];
|
||||
self.mk_desugared_ctr(range, cons_ident.clone(), spine)
|
||||
self.mk_desugared_ctr(range, cons_ident.clone(), spine, false)
|
||||
},
|
||||
)
|
||||
}
|
||||
@ -187,8 +190,7 @@ impl<'a> DesugarState<'a> {
|
||||
if_: &expr::Expr,
|
||||
else_: &expr::Expr,
|
||||
) -> Box<desugared::Expr> {
|
||||
let bool_ident =
|
||||
QualifiedIdent::new_static("Bool".to_string(), Some("if".to_string()), range);
|
||||
let bool_ident = QualifiedIdent::new_sugared("Bool", "if", range);
|
||||
|
||||
let bool_if = self.old_book.entries.get(bool_ident.to_string().as_str());
|
||||
|
||||
@ -203,7 +205,7 @@ impl<'a> DesugarState<'a> {
|
||||
self.desugar_expr(else_),
|
||||
];
|
||||
|
||||
self.mk_desugared_fun(range, bool_ident, spine)
|
||||
self.mk_desugared_fun(range, bool_ident, spine, false)
|
||||
}
|
||||
|
||||
pub(crate) fn desugar_pair(
|
||||
@ -212,8 +214,7 @@ impl<'a> DesugarState<'a> {
|
||||
fst: &expr::Expr,
|
||||
snd: &expr::Expr,
|
||||
) -> Box<desugared::Expr> {
|
||||
let sigma_new =
|
||||
QualifiedIdent::new_static("Sigma".to_string(), Some("new".to_string()), range);
|
||||
let sigma_new = QualifiedIdent::new_sugared("Sigma", "new", range);
|
||||
|
||||
let entry = self.old_book.entries.get(sigma_new.to_string().as_str());
|
||||
|
||||
@ -224,13 +225,13 @@ impl<'a> DesugarState<'a> {
|
||||
|
||||
let spine = vec![self.desugar_expr(fst), self.desugar_expr(snd)];
|
||||
|
||||
self.mk_desugared_ctr(range, sigma_new, spine)
|
||||
self.mk_desugared_ctr(range, sigma_new, spine, false)
|
||||
}
|
||||
|
||||
pub(crate) fn desugar_expr(&mut self, expr: &expr::Expr) -> Box<desugared::Expr> {
|
||||
use expr::ExprKind::*;
|
||||
match &expr.data {
|
||||
Constr(_) => self.desugar_app(expr.range, expr, &[]),
|
||||
Constr(_, _) | App(_, _) => self.desugar_app(expr.range, expr),
|
||||
All(ident, typ, body) => desugared::Expr::all(
|
||||
expr.range,
|
||||
ident.clone().unwrap_or_else(|| self.gen_name(expr.range)),
|
||||
@ -251,7 +252,6 @@ impl<'a> DesugarState<'a> {
|
||||
}
|
||||
Var(ident) => desugared::Expr::var(ident.clone()),
|
||||
Hole => desugared::Expr::hole(expr.range, self.gen_hole()),
|
||||
App(head, spine) => self.desugar_app(expr.range, head, spine),
|
||||
Lit(literal) => self.desugar_literal(expr.range, literal),
|
||||
Match(matcher) => self.desugar_match(expr.range, matcher),
|
||||
Let(destruct, val, next) => self.desugar_let(expr.range, destruct, val, next),
|
||||
|
@ -1,7 +1,7 @@
|
||||
use kind_span::{Range, Span};
|
||||
use kind_tree::concrete::{self, Telescope};
|
||||
use kind_tree::desugared;
|
||||
use kind_tree::symbol::{QualifiedIdent};
|
||||
use kind_tree::desugared::{self, ExprKind};
|
||||
use kind_tree::symbol::QualifiedIdent;
|
||||
|
||||
use crate::errors::{PassError, Sugar};
|
||||
|
||||
@ -82,7 +82,32 @@ impl<'a> DesugarState<'a> {
|
||||
};
|
||||
|
||||
let typ = match cons.typ.clone() {
|
||||
Some(expr) => self.desugar_expr(&expr),
|
||||
Some(expr) => {
|
||||
let res = self.desugar_expr(&expr);
|
||||
match &res.data {
|
||||
ExprKind::Ctr(name, spine)
|
||||
if name.to_string() == sum_type.name.to_string() =>
|
||||
{
|
||||
for (i, parameter) in sum_type.parameters.iter().enumerate() {
|
||||
match &spine[i].data {
|
||||
ExprKind::Var(name)
|
||||
if name.to_string() == parameter.name.to_string() => {}
|
||||
_ => {
|
||||
self.send_err(PassError::ShouldBeAParameter(
|
||||
spine[i].span,
|
||||
parameter.range,
|
||||
));
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
_ => self.send_err(PassError::NotATypeConstructor(
|
||||
expr.range,
|
||||
sum_type.name.range,
|
||||
)),
|
||||
}
|
||||
res
|
||||
}
|
||||
None => {
|
||||
let args = [irrelevant_params.as_slice(), pre_indices]
|
||||
.concat()
|
||||
@ -90,7 +115,7 @@ impl<'a> DesugarState<'a> {
|
||||
.map(|x| desugared::Expr::var(x.name.clone()))
|
||||
.collect::<Vec<Box<desugared::Expr>>>();
|
||||
|
||||
desugared::Expr::ctr(sum_type.name.range, sum_type.name.clone(), args)
|
||||
desugared::Expr::ctr(cons.name.range, sum_type.name.clone(), args)
|
||||
}
|
||||
};
|
||||
|
||||
@ -105,7 +130,7 @@ impl<'a> DesugarState<'a> {
|
||||
typ,
|
||||
rules: Vec::new(),
|
||||
attrs: Vec::new(),
|
||||
span: Span::Locatable(sum_type.name.range),
|
||||
span: Span::Locatable(cons.name.range),
|
||||
};
|
||||
|
||||
self.new_book
|
||||
@ -187,8 +212,7 @@ impl<'a> DesugarState<'a> {
|
||||
fst: &concrete::pat::Pat,
|
||||
snd: &concrete::pat::Pat,
|
||||
) -> Box<desugared::Expr> {
|
||||
let sigma_new =
|
||||
QualifiedIdent::new_static("Sigma".to_string(), Some("new".to_string()), range);
|
||||
let sigma_new = QualifiedIdent::new_static("Sigma", Some("new".to_string()), range);
|
||||
|
||||
let entry = self.old_book.entries.get(sigma_new.to_string().as_str());
|
||||
if entry.is_none() {
|
||||
@ -198,7 +222,7 @@ impl<'a> DesugarState<'a> {
|
||||
|
||||
let spine = vec![self.desugar_pat(fst), self.desugar_pat(snd)];
|
||||
|
||||
self.mk_desugared_ctr(range, sigma_new, spine)
|
||||
self.mk_desugared_ctr(range, sigma_new, spine, true)
|
||||
}
|
||||
|
||||
pub fn desugar_list_pat(
|
||||
@ -206,7 +230,7 @@ impl<'a> DesugarState<'a> {
|
||||
range: Range,
|
||||
expr: &[concrete::pat::Pat],
|
||||
) -> Box<desugared::Expr> {
|
||||
let list_ident = QualifiedIdent::new_static("List".to_string(), None, range);
|
||||
let list_ident = QualifiedIdent::new_static("List", None, range);
|
||||
let cons_ident = list_ident.add_segment("cons");
|
||||
let nil_ident = list_ident.add_segment("nil");
|
||||
|
||||
@ -220,10 +244,10 @@ impl<'a> DesugarState<'a> {
|
||||
}
|
||||
|
||||
expr.iter().rfold(
|
||||
self.mk_desugared_ctr(range, nil_ident, Vec::new()),
|
||||
self.mk_desugared_ctr(range, nil_ident, Vec::new(), true),
|
||||
|res, elem| {
|
||||
let spine = vec![self.desugar_pat(elem), res];
|
||||
self.mk_desugared_ctr(range, cons_ident.clone(), spine)
|
||||
self.mk_desugared_ctr(range, cons_ident.clone(), spine, true)
|
||||
},
|
||||
)
|
||||
}
|
||||
@ -235,12 +259,11 @@ impl<'a> DesugarState<'a> {
|
||||
.old_book
|
||||
.count
|
||||
.get(head.to_string().as_str())
|
||||
.expect("Cannot find definition");
|
||||
.expect("Internal Error: Cannot find definition");
|
||||
|
||||
if !entry.is_ctr {
|
||||
// TODO: Not sure if i should just throw an error?
|
||||
// We are not requiring that the thing is specifically a constructor
|
||||
panic!("Incomplete Design: Oh no!")
|
||||
// TODO: Check if only data constructors declared inside
|
||||
// inductive types can be used in patterns.
|
||||
}
|
||||
|
||||
let (hidden, _erased) = entry.arguments.count_implicits();
|
||||
@ -253,15 +276,18 @@ impl<'a> DesugarState<'a> {
|
||||
let mut count = 0;
|
||||
for i in 0..entry.arguments.len() {
|
||||
if entry.arguments[i].hidden {
|
||||
new_spine.push(self.gen_hole_expr())
|
||||
let name = self.gen_name(entry.arguments[i].range);
|
||||
new_spine.push(desugared::Expr::var(name))
|
||||
} else {
|
||||
new_spine.push(self.desugar_pat(&spine[count]));
|
||||
count += 1;
|
||||
}
|
||||
}
|
||||
} else if entry.arguments.len() != spine.len() {
|
||||
println!("{}", pat);
|
||||
self.send_err(PassError::IncorrectArity(
|
||||
head.range,
|
||||
spine.iter().map(|x| x.range).collect(),
|
||||
entry.arguments.len(),
|
||||
hidden,
|
||||
));
|
||||
@ -273,10 +299,13 @@ impl<'a> DesugarState<'a> {
|
||||
}
|
||||
desugared::Expr::ctr(pat.range, head.clone(), new_spine)
|
||||
}
|
||||
concrete::pat::PatKind::Hole => {
|
||||
let name = self.gen_name(pat.range);
|
||||
desugared::Expr::var(name)
|
||||
}
|
||||
concrete::pat::PatKind::Var(ident) => desugared::Expr::var(ident.0.clone()),
|
||||
// TODO: Add u120 pattern literals
|
||||
concrete::pat::PatKind::Num(n) => desugared::Expr::num60(pat.range, *n),
|
||||
concrete::pat::PatKind::Hole => desugared::Expr::hole(pat.range, self.gen_hole()),
|
||||
concrete::pat::PatKind::Pair(fst, snd) => self.desugar_pair_pat(pat.range, fst, snd),
|
||||
concrete::pat::PatKind::List(ls) => self.desugar_list_pat(pat.range, ls),
|
||||
concrete::pat::PatKind::Str(string) => {
|
||||
@ -339,6 +368,8 @@ impl<'a> DesugarState<'a> {
|
||||
}
|
||||
|
||||
pub fn desugar_entry(&mut self, entry: &concrete::Entry) {
|
||||
self.name_count = 0;
|
||||
|
||||
let rules = entry
|
||||
.rules
|
||||
.iter()
|
||||
|
@ -60,8 +60,9 @@ pub fn erase_book(
|
||||
|
||||
for name in entrypoint {
|
||||
let count = state.holes.len();
|
||||
let ty = (None, Relevance::Hole(count));
|
||||
state.names.insert(name.to_string(), ty.clone());
|
||||
state
|
||||
.names
|
||||
.insert(name.to_string(), (None, Relevance::Hole(count)));
|
||||
state.holes.push(Some(Relevance::Relevant));
|
||||
}
|
||||
|
||||
@ -95,10 +96,10 @@ pub fn erasure_to_relevance(erased: bool) -> Relevance {
|
||||
impl<'a> ErasureState<'a> {
|
||||
pub fn new_hole(&mut self, range: Range, name: String) -> (Option<Range>, Relevance) {
|
||||
let count = self.holes.len();
|
||||
let ty = (Some(range), Relevance::Hole(count));
|
||||
self.names.insert(name.to_string(), ty.clone());
|
||||
let local_relevance = (Some(range), Relevance::Hole(count));
|
||||
self.names.insert(name, local_relevance);
|
||||
self.holes.push(None);
|
||||
ty
|
||||
local_relevance
|
||||
}
|
||||
|
||||
pub fn err_irrelevant(
|
||||
@ -146,7 +147,14 @@ impl<'a> ErasureState<'a> {
|
||||
self.holes[hole.1] = Some(t);
|
||||
true
|
||||
} else {
|
||||
self.unify_hole(range, (hole.0, n), right, visited, inverted, relevance_unify)
|
||||
self.unify_hole(
|
||||
range,
|
||||
(hole.0, n),
|
||||
right,
|
||||
visited,
|
||||
inverted,
|
||||
relevance_unify,
|
||||
)
|
||||
}
|
||||
}
|
||||
(_, Relevance::Relevant) => true,
|
||||
@ -176,9 +184,14 @@ impl<'a> ErasureState<'a> {
|
||||
(_, Relevance::Hole(hole)) => {
|
||||
self.unify_hole(range, (right.0, hole), left, visited, true, relevance_unify)
|
||||
}
|
||||
(Relevance::Hole(hole), _) => {
|
||||
self.unify_hole(range, (left.0, hole), right, visited, false, relevance_unify)
|
||||
}
|
||||
(Relevance::Hole(hole), _) => self.unify_hole(
|
||||
range,
|
||||
(left.0, hole),
|
||||
right,
|
||||
visited,
|
||||
false,
|
||||
relevance_unify,
|
||||
),
|
||||
|
||||
(Relevance::Irrelevant, Relevance::Irrelevant)
|
||||
| (Relevance::Irrelevant, Relevance::Relevant)
|
||||
@ -208,7 +221,7 @@ impl<'a> ErasureState<'a> {
|
||||
}
|
||||
Fun(name, spine) | Ctr(name, spine) => {
|
||||
let fun = match self.names.get(&name.to_string()) {
|
||||
Some(res) => res.clone(),
|
||||
Some(res) => *res,
|
||||
None => self.new_hole(name.range, name.to_string()),
|
||||
};
|
||||
|
||||
@ -234,7 +247,7 @@ impl<'a> ErasureState<'a> {
|
||||
.zip(irrelevances)
|
||||
.for_each(|(arg, relev)| self.erase_pat(relev, arg));
|
||||
}
|
||||
_ => panic!("Internal Error: Not a pattern"),
|
||||
res => panic!("Internal Error: Not a pattern {:?}", res),
|
||||
}
|
||||
}
|
||||
|
||||
@ -243,12 +256,20 @@ impl<'a> ErasureState<'a> {
|
||||
|
||||
match &expr.data {
|
||||
Typ | NumType(_) | Num(_) | Str(_) | Err => Box::new(expr.clone()),
|
||||
Hole(_) | Hlp(_) => Box::new(expr.clone()),
|
||||
Hole(_) | Hlp(_) => match &expr.span {
|
||||
kind_span::Span::Generated => Box::new(expr.clone()),
|
||||
kind_span::Span::Locatable(span) => {
|
||||
if !self.unify(*span, *on, (None, Relevance::Irrelevant), false) {
|
||||
self.err_irrelevant(None, *span, None)
|
||||
}
|
||||
Box::new(expr.clone())
|
||||
}
|
||||
},
|
||||
Var(name) => {
|
||||
let relev = self.ctx.get(&name.to_string()).unwrap();
|
||||
let declared_ty = (relev.1).0;
|
||||
let declared_val = relev.0;
|
||||
if !self.unify(name.range, on.clone(), relev.1, false) {
|
||||
if !self.unify(name.range, *on, relev.1, false) {
|
||||
self.err_irrelevant(Some(declared_val), name.range, declared_ty)
|
||||
}
|
||||
Box::new(expr.clone())
|
||||
@ -257,7 +278,7 @@ impl<'a> ErasureState<'a> {
|
||||
let ctx = self.ctx.clone();
|
||||
|
||||
// Relevant inside the context that is it's being used?
|
||||
self.ctx.insert(name.to_string(), (name.range, on.clone()));
|
||||
self.ctx.insert(name.to_string(), (name.range, *on));
|
||||
|
||||
self.erase_expr(&(on.0, Relevance::Irrelevant), typ);
|
||||
self.erase_expr(&(on.0, Relevance::Irrelevant), body);
|
||||
@ -267,7 +288,7 @@ impl<'a> ErasureState<'a> {
|
||||
}
|
||||
Lambda(name, body) => {
|
||||
let ctx = self.ctx.clone();
|
||||
self.ctx.insert(name.to_string(), (name.range, on.clone()));
|
||||
self.ctx.insert(name.to_string(), (name.range, *on));
|
||||
let body = self.erase_expr(on, body);
|
||||
self.ctx = ctx;
|
||||
|
||||
@ -278,7 +299,7 @@ impl<'a> ErasureState<'a> {
|
||||
}
|
||||
Let(name, val, body) => {
|
||||
let ctx = self.ctx.clone();
|
||||
self.ctx.insert(name.to_string(), (name.range, on.clone()));
|
||||
self.ctx.insert(name.to_string(), (name.range, *on));
|
||||
|
||||
let val = self.erase_expr(on, val);
|
||||
let body = self.erase_expr(on, body);
|
||||
@ -308,21 +329,31 @@ impl<'a> ErasureState<'a> {
|
||||
.iter();
|
||||
|
||||
let fun = match self.names.get(&head.to_string()) {
|
||||
Some(res) => res.clone(),
|
||||
Some(res) => *res,
|
||||
None => self.new_hole(head.range, head.to_string()),
|
||||
};
|
||||
|
||||
if !self.unify(head.range, on.clone(), fun, true) {
|
||||
if !self.unify(head.range, *on, fun, true) {
|
||||
self.err_irrelevant(None, head.range, None)
|
||||
}
|
||||
|
||||
let spine = spine.iter().zip(args).map(|(expr, arg)| {
|
||||
self.erase_expr(&(Some(arg.span), erasure_to_relevance(arg.erased)), expr)
|
||||
});
|
||||
let spine = spine
|
||||
.iter()
|
||||
.zip(args)
|
||||
.map(|(expr, arg)| {
|
||||
(
|
||||
self.erase_expr(
|
||||
&(Some(arg.span), erasure_to_relevance(arg.erased)),
|
||||
expr,
|
||||
),
|
||||
arg,
|
||||
)
|
||||
})
|
||||
.filter(|(_, arg)| !arg.erased);
|
||||
|
||||
Box::new(Expr {
|
||||
span: expr.span,
|
||||
data: ExprKind::Fun(head.clone(), spine.collect()),
|
||||
data: ExprKind::Fun(head.clone(), spine.map(|(expr, _)| expr).collect()),
|
||||
})
|
||||
}
|
||||
Ctr(head, spine) => {
|
||||
@ -335,21 +366,31 @@ impl<'a> ErasureState<'a> {
|
||||
.iter();
|
||||
|
||||
let fun = match self.names.get(&head.to_string()) {
|
||||
Some(res) => res.clone(),
|
||||
Some(res) => *res,
|
||||
None => self.new_hole(head.range, head.to_string()),
|
||||
};
|
||||
|
||||
if !self.unify(head.range, on.clone(), fun, true) {
|
||||
if !self.unify(head.range, *on, fun, true) {
|
||||
self.err_irrelevant(None, head.range, None)
|
||||
}
|
||||
|
||||
let spine = spine.iter().zip(args).map(|(expr, arg)| {
|
||||
self.erase_expr(&(Some(arg.span), erasure_to_relevance(arg.erased)), expr)
|
||||
});
|
||||
let spine = spine
|
||||
.iter()
|
||||
.zip(args)
|
||||
.map(|(expr, arg)| {
|
||||
(
|
||||
self.erase_expr(
|
||||
&(Some(arg.span), erasure_to_relevance(arg.erased)),
|
||||
expr,
|
||||
),
|
||||
arg,
|
||||
)
|
||||
})
|
||||
.filter(|(_, arg)| !arg.erased);
|
||||
|
||||
Box::new(Expr {
|
||||
span: expr.span,
|
||||
data: ExprKind::Ctr(head.clone(), spine.collect()),
|
||||
data: ExprKind::Ctr(head.clone(), spine.map(|(expr, _)| expr).collect()),
|
||||
})
|
||||
}
|
||||
Ann(relev, irrel) => {
|
||||
@ -400,7 +441,7 @@ impl<'a> ErasureState<'a> {
|
||||
|
||||
pub fn erase_entry(&mut self, entry: &Entry) -> Box<Entry> {
|
||||
let place = if let Some(res) = self.names.get(&entry.name.to_string()) {
|
||||
res.clone()
|
||||
*res
|
||||
} else {
|
||||
self.new_hole(entry.name.range, entry.name.to_string())
|
||||
};
|
||||
|
@ -1,5 +1,5 @@
|
||||
use kind_report::data::{Color, DiagnosticFrame, Marker, Severity};
|
||||
use kind_span::Range;
|
||||
use kind_span::{Range, Span};
|
||||
|
||||
pub enum Sugar {
|
||||
DoNotation,
|
||||
@ -14,7 +14,7 @@ pub enum Sugar {
|
||||
pub enum PassError {
|
||||
RepeatedVariable(Range, Range),
|
||||
CannotUseNamed(Range, Range),
|
||||
IncorrectArity(Range, usize, usize),
|
||||
IncorrectArity(Range, Vec<Range>, usize, usize),
|
||||
DuplicatedNamed(Range, Range),
|
||||
LetDestructOnlyForRecord(Range),
|
||||
LetDestructOnlyForSum(Range),
|
||||
@ -26,6 +26,11 @@ pub enum PassError {
|
||||
RulesWithInconsistentArity(Vec<(Range, usize)>),
|
||||
SugarIsBadlyImplemented(Range, Range, usize),
|
||||
CannotUseIrrelevant(Option<Range>, Range, Option<Range>),
|
||||
CannotFindAlias(String, Range),
|
||||
NotATypeConstructor(Range, Range),
|
||||
ShouldBeAParameter(Span, Range),
|
||||
NoFieldCoverage(Range, Vec<String>),
|
||||
DuplicatedConstructor(Range, Range),
|
||||
}
|
||||
|
||||
// TODO: A way to build an error message with methods
|
||||
@ -212,28 +217,32 @@ impl From<PassError> for DiagnosticFrame {
|
||||
main: true,
|
||||
}],
|
||||
},
|
||||
PassError::IncorrectArity(head_range, expected, hidden) => DiagnosticFrame {
|
||||
code: 210,
|
||||
severity: Severity::Error,
|
||||
title: "Incorrect arity".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![
|
||||
if expected == 0 {
|
||||
"This function expects no arguments".to_string()
|
||||
} else if hidden == 0 {
|
||||
format!("This function expects {} arguments", expected)
|
||||
} else {
|
||||
format!("This function expects {} arguments or {} (without hidden ones)", expected, expected - hidden)
|
||||
}
|
||||
],
|
||||
positions: vec![Marker {
|
||||
PassError::IncorrectArity(head_range, got, expected, hidden) => {
|
||||
let positions = vec![Marker {
|
||||
position: head_range,
|
||||
color: Color::Fst,
|
||||
text: "This function requires a fixed number of arguments".to_string(),
|
||||
no_code: false,
|
||||
main: true,
|
||||
}],
|
||||
},
|
||||
}];
|
||||
|
||||
DiagnosticFrame {
|
||||
code: 210,
|
||||
severity: Severity::Error,
|
||||
title: "Incorrect arity.".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![
|
||||
if expected == 0 {
|
||||
format!("This function expects no arguments but got {}", got.len())
|
||||
} else if hidden == 0 {
|
||||
format!("This function expects {} arguments but got {}", expected, got.len())
|
||||
} else {
|
||||
format!("This function expects {} arguments or {} (without hidden ones) but got {}.", expected, expected - hidden, got.len())
|
||||
}
|
||||
],
|
||||
positions
|
||||
}
|
||||
}
|
||||
PassError::SugarIsBadlyImplemented(head_range, place_range, expected) => DiagnosticFrame {
|
||||
code: 211,
|
||||
severity: Severity::Error,
|
||||
@ -312,9 +321,9 @@ impl From<PassError> for DiagnosticFrame {
|
||||
PassError::RepeatedVariable(first_decl, last_decl) => DiagnosticFrame {
|
||||
code: 214,
|
||||
severity: Severity::Error,
|
||||
title: "Repeated variable".to_string(),
|
||||
title: "Repeated name".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec!["Rename one of the variables".to_string()],
|
||||
hints: vec!["Rename one of the occurences".to_string()],
|
||||
positions: vec![
|
||||
Marker {
|
||||
position: last_decl,
|
||||
@ -332,6 +341,115 @@ impl From<PassError> for DiagnosticFrame {
|
||||
},
|
||||
],
|
||||
},
|
||||
PassError::CannotFindAlias(name, range) => DiagnosticFrame {
|
||||
code: 214,
|
||||
severity: Severity::Error,
|
||||
title: "Cannot find alias".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![],
|
||||
positions: vec![
|
||||
Marker {
|
||||
position: range,
|
||||
color: Color::Fst,
|
||||
text: format!("Cannot find alias for '{}'", name),
|
||||
no_code: false,
|
||||
main: true,
|
||||
}
|
||||
],
|
||||
},
|
||||
PassError::ShouldBeAParameter(error_range, declaration_range) => {
|
||||
let mut positions = vec![];
|
||||
|
||||
match error_range {
|
||||
Span::Generated => (),
|
||||
Span::Locatable(error_range) => {
|
||||
positions.push(Marker {
|
||||
position: error_range,
|
||||
color: Color::Fst,
|
||||
text: "This expression is not the parameter".to_string(),
|
||||
no_code: false,
|
||||
main: true,
|
||||
})
|
||||
},
|
||||
}
|
||||
|
||||
positions.push(
|
||||
Marker {
|
||||
position: declaration_range,
|
||||
color: Color::Snd,
|
||||
text: "This is the parameter that should be used".to_string(),
|
||||
no_code: false,
|
||||
main: false,
|
||||
}
|
||||
);
|
||||
|
||||
DiagnosticFrame {
|
||||
code: 214,
|
||||
severity: Severity::Error,
|
||||
title: "The expression is not the parameter declared in the type constructor".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![],
|
||||
positions
|
||||
}
|
||||
}
|
||||
PassError::NotATypeConstructor(error_range, declaration_range) => DiagnosticFrame {
|
||||
code: 214,
|
||||
severity: Severity::Error,
|
||||
title: "This is not the type that is being declared.".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![],
|
||||
positions: vec![
|
||||
Marker {
|
||||
position: error_range,
|
||||
color: Color::Fst,
|
||||
text: "This is not the type that is being declared".to_string(),
|
||||
no_code: false,
|
||||
main: true,
|
||||
},
|
||||
Marker {
|
||||
position: declaration_range,
|
||||
color: Color::Snd,
|
||||
text: "This is the type that should be used instead".to_string(),
|
||||
no_code: false,
|
||||
main: false,
|
||||
}
|
||||
],
|
||||
},
|
||||
PassError::NoFieldCoverage(place, other) => DiagnosticFrame {
|
||||
code: 209,
|
||||
severity: Severity::Error,
|
||||
title: "The case is not covering all the values inside of it!".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![format!("Need variables for {}", other.iter().map(|x| format!("'{}'", x)).collect::<Vec<String>>().join(", "))],
|
||||
positions: vec![Marker {
|
||||
position: place,
|
||||
color: Color::Fst,
|
||||
text: "This is the incomplete case".to_string(),
|
||||
no_code: false,
|
||||
main: true,
|
||||
}],
|
||||
},
|
||||
PassError::DuplicatedConstructor(place, other) => DiagnosticFrame {
|
||||
code: 209,
|
||||
severity: Severity::Error,
|
||||
title: "Duplicated constructor name".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![],
|
||||
positions: vec![Marker {
|
||||
position: place,
|
||||
color: Color::Fst,
|
||||
text: "Here".to_string(),
|
||||
no_code: false,
|
||||
main: true,
|
||||
},
|
||||
Marker {
|
||||
position: other,
|
||||
color: Color::Fst,
|
||||
text: "Here".to_string(),
|
||||
no_code: false,
|
||||
main: false,
|
||||
}],
|
||||
},
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -1,22 +1,160 @@
|
||||
use std::collections::HashMap;
|
||||
|
||||
use fxhash::FxHashMap;
|
||||
use kind_derive::matching::derive_match;
|
||||
use kind_tree::concrete::{Book, TopLevel};
|
||||
use kind_derive::open::derive_open;
|
||||
use kind_tree::concrete::{
|
||||
self, expr::Expr, Argument, Binding, Book, Entry, EntryMeta, ExprKind, Literal, RecordDecl,
|
||||
SumTypeDecl, Telescope, TopLevel,
|
||||
};
|
||||
/// Expands sum type and record definitions to a lot of
|
||||
/// helper definitions like eliminators and replace qualified identifiers
|
||||
/// by their module names.
|
||||
pub mod uses;
|
||||
|
||||
pub fn expand_record_type(book: &mut FxHashMap<String, (Entry, EntryMeta)>, rec_type: &RecordDecl) {
|
||||
let type_constructor = Entry {
|
||||
name: rec_type.name.clone(),
|
||||
args: rec_type.parameters.clone(),
|
||||
docs: rec_type.docs.clone(),
|
||||
typ: Box::new(Expr {
|
||||
data: ExprKind::Lit(Literal::Type),
|
||||
range: rec_type.name.range,
|
||||
}),
|
||||
rules: Vec::new(),
|
||||
range: rec_type.name.range,
|
||||
attrs: rec_type.attrs.clone(),
|
||||
};
|
||||
|
||||
book.insert(
|
||||
rec_type.name.to_string(),
|
||||
(type_constructor, rec_type.extract_book_info()),
|
||||
);
|
||||
|
||||
let irrelevant_params = rec_type.parameters.map(|x| x.to_implicit());
|
||||
|
||||
let args = irrelevant_params
|
||||
.iter()
|
||||
.map(|x| {
|
||||
Binding::Positional(Box::new(Expr {
|
||||
data: ExprKind::Var(x.name.clone()),
|
||||
range: x.range,
|
||||
}))
|
||||
})
|
||||
.collect::<Vec<Binding>>();
|
||||
|
||||
let typ = Box::new(Expr {
|
||||
data: ExprKind::Constr(rec_type.name.clone(), args),
|
||||
range: rec_type.name.range,
|
||||
});
|
||||
|
||||
let cons_ident = rec_type.name.add_segment(rec_type.constructor.to_str());
|
||||
|
||||
let data_constructor = Entry {
|
||||
name: cons_ident.clone(),
|
||||
args: irrelevant_params.extend(&Telescope::new(rec_type.fields.clone()).map(
|
||||
|(ident, _, ty)| Argument {
|
||||
hidden: false,
|
||||
erased: false,
|
||||
name: ident.clone(),
|
||||
typ: Some(ty.clone()),
|
||||
range: ident.range,
|
||||
},
|
||||
)),
|
||||
typ,
|
||||
rules: Vec::new(),
|
||||
range: rec_type.constructor.range,
|
||||
attrs: Vec::new(),
|
||||
docs: vec![],
|
||||
};
|
||||
|
||||
book.insert(
|
||||
cons_ident.to_string(),
|
||||
(
|
||||
data_constructor,
|
||||
rec_type.extract_book_info_of_constructor(),
|
||||
),
|
||||
);
|
||||
}
|
||||
|
||||
pub fn expand_sum_type(book: &mut FxHashMap<String, (Entry, EntryMeta)>, sum_type: &SumTypeDecl) {
|
||||
let params = sum_type.parameters.clone();
|
||||
let indices = sum_type.indices.clone();
|
||||
|
||||
let type_constructor = Entry {
|
||||
name: sum_type.name.clone(),
|
||||
args: sum_type.parameters.extend(&sum_type.indices),
|
||||
docs: sum_type.docs.clone(),
|
||||
typ: Box::new(Expr {
|
||||
data: ExprKind::Lit(Literal::Type),
|
||||
range: sum_type.name.range,
|
||||
}),
|
||||
rules: Vec::new(),
|
||||
range: sum_type.name.range,
|
||||
attrs: sum_type.attrs.clone(),
|
||||
};
|
||||
|
||||
let extracted = sum_type.extract_book_info();
|
||||
book.insert(sum_type.name.to_string(), (type_constructor, extracted));
|
||||
|
||||
let irrelevant_params = params.map(|x| x.to_implicit());
|
||||
let irelevant_indices = indices.map(|x| x.to_implicit());
|
||||
|
||||
for cons in &sum_type.constructors {
|
||||
let cons_ident = sum_type.name.add_segment(cons.name.to_str());
|
||||
|
||||
let pre_indices = if cons.typ.is_none() {
|
||||
irelevant_indices.clone()
|
||||
} else {
|
||||
Telescope::new(vec![])
|
||||
};
|
||||
|
||||
let typ = cons.typ.clone().unwrap_or_else(|| {
|
||||
let args = params.extend(&pre_indices).map(|x| {
|
||||
concrete::Binding::Positional(Box::new(Expr {
|
||||
data: ExprKind::Var(x.name.clone()),
|
||||
range: x.range,
|
||||
}))
|
||||
});
|
||||
|
||||
Box::new(Expr {
|
||||
data: ExprKind::Constr(sum_type.name.clone(), args.to_vec()),
|
||||
range: sum_type.name.range,
|
||||
})
|
||||
});
|
||||
|
||||
let data_constructor = Entry {
|
||||
name: cons_ident.clone(),
|
||||
args: irrelevant_params.extend(&pre_indices).extend(&cons.args),
|
||||
typ,
|
||||
rules: Vec::new(),
|
||||
attrs: Vec::new(),
|
||||
docs: vec![],
|
||||
range: cons_ident.range,
|
||||
};
|
||||
|
||||
let book_info = cons.extract_book_info(sum_type);
|
||||
book.insert(cons_ident.to_string(), (data_constructor, book_info));
|
||||
}
|
||||
}
|
||||
|
||||
pub fn expand_book(book: &mut Book) {
|
||||
let mut entries = HashMap::new();
|
||||
for entry in book.entries.values_mut() {
|
||||
let mut entries = FxHashMap::default();
|
||||
for entry in book.entries.values() {
|
||||
match entry {
|
||||
TopLevel::SumType(sum) => {
|
||||
let res = derive_match(sum.name.range, sum);
|
||||
entries.insert(res.name.to_string(), res);
|
||||
let info = res.extract_book_info();
|
||||
entries.insert(res.name.to_string(), (res, info));
|
||||
}
|
||||
TopLevel::RecordType(rec) => {
|
||||
let res = derive_open(rec.name.range, rec);
|
||||
let info = res.extract_book_info();
|
||||
entries.insert(res.name.to_string(), (res, info));
|
||||
}
|
||||
TopLevel::RecordType(_) => (),
|
||||
TopLevel::Entry(_) => (),
|
||||
}
|
||||
}
|
||||
for (name, tl) in entries {
|
||||
book.count.insert(name.clone(), tl.extract_book_info());
|
||||
for (name, (tl, count)) in entries {
|
||||
book.count.insert(name.clone(), count);
|
||||
book.names.insert(name.clone().to_string(), tl.name.clone());
|
||||
book.entries.insert(name.clone(), TopLevel::Entry(tl));
|
||||
}
|
||||
|
52
src/kind-pass/src/expand/uses.rs
Normal file
52
src/kind-pass/src/expand/uses.rs
Normal file
@ -0,0 +1,52 @@
|
||||
use fxhash::FxHashMap;
|
||||
use kind_report::data::DiagnosticFrame;
|
||||
use kind_tree::concrete::{visitor::Visitor, Module};
|
||||
/// Expands sum type and record definitions to a lot of
|
||||
/// helper definitions like eliminators and replace qualified identifiers
|
||||
/// by their module names.
|
||||
use std::sync::mpsc::Sender;
|
||||
|
||||
use crate::errors::PassError;
|
||||
|
||||
pub struct Expand {
|
||||
pub names: FxHashMap<String, String>,
|
||||
pub errors: Sender<DiagnosticFrame>,
|
||||
pub failed: bool,
|
||||
}
|
||||
|
||||
impl Visitor for Expand {
|
||||
fn visit_qualified_ident(&mut self, ident: &mut kind_tree::symbol::QualifiedIdent) {
|
||||
if ident.aux.is_none() {
|
||||
return;
|
||||
}
|
||||
let alias = match self.names.get(&ident.root.to_string()) {
|
||||
Some(path) => path,
|
||||
None => {
|
||||
self.errors
|
||||
.send(PassError::CannotFindAlias(ident.root.to_string(), ident.range).into())
|
||||
.unwrap();
|
||||
self.failed = true;
|
||||
return;
|
||||
}
|
||||
};
|
||||
match &ident.aux {
|
||||
Some(post) => {
|
||||
ident.change_root(format!("{}.{}", alias, post));
|
||||
ident.aux = None;
|
||||
}
|
||||
None => ident.change_root(alias.clone()),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
pub fn expand_uses(module: &mut Module, errors: Sender<DiagnosticFrame>) -> bool {
|
||||
let mut session = Expand {
|
||||
names: module.uses.clone(),
|
||||
errors,
|
||||
failed: false,
|
||||
};
|
||||
for entry in module.entries.iter_mut() {
|
||||
session.visit_top_level(entry)
|
||||
}
|
||||
session.failed
|
||||
}
|
@ -79,7 +79,17 @@ impl Visitor for UnboundCollector {
|
||||
let entry = self
|
||||
.unbound
|
||||
.entry(ident.to_string())
|
||||
.or_insert_with(|| Vec::new());
|
||||
.or_insert_with(Vec::new);
|
||||
entry.push(ident.clone());
|
||||
}
|
||||
}
|
||||
|
||||
fn visit_qualified_ident(&mut self, ident: &mut QualifiedIdent) {
|
||||
if !self.context_vars.iter().any(|x| x.1 == ident.to_string()) {
|
||||
let entry = self
|
||||
.unbound_top_level
|
||||
.entry(ident.to_string())
|
||||
.or_insert_with(Vec::new);
|
||||
entry.push(ident.clone());
|
||||
}
|
||||
}
|
||||
@ -103,6 +113,21 @@ impl Visitor for UnboundCollector {
|
||||
Some(res) => self.visit_expr(res),
|
||||
None => (),
|
||||
}
|
||||
|
||||
let res = self
|
||||
.context_vars
|
||||
.iter()
|
||||
.find(|x| x.1 == argument.name.to_string());
|
||||
|
||||
if let Some(fst) = res {
|
||||
self.errors
|
||||
.send(PassError::RepeatedVariable(fst.0, argument.name.range).into())
|
||||
.unwrap()
|
||||
} else {
|
||||
self.context_vars
|
||||
.push((argument.name.range, argument.name.to_string()))
|
||||
}
|
||||
|
||||
self.context_vars
|
||||
.push((argument.name.range, argument.name.to_string()));
|
||||
}
|
||||
@ -117,6 +142,9 @@ impl Visitor for UnboundCollector {
|
||||
}
|
||||
|
||||
fn visit_entry(&mut self, entry: &mut Entry) {
|
||||
self.context_vars
|
||||
.push((entry.name.range, entry.name.to_string()));
|
||||
|
||||
let vars = self.context_vars.clone();
|
||||
|
||||
for arg in entry.args.iter_mut() {
|
||||
@ -124,6 +152,7 @@ impl Visitor for UnboundCollector {
|
||||
}
|
||||
|
||||
self.visit_expr(&mut entry.typ);
|
||||
|
||||
self.context_vars = vars;
|
||||
|
||||
for rule in &mut entry.rules {
|
||||
@ -136,10 +165,27 @@ impl Visitor for UnboundCollector {
|
||||
TopLevel::SumType(entr) => {
|
||||
self.context_vars
|
||||
.push((entr.name.range, entr.name.to_string()));
|
||||
|
||||
let mut repeated_names = FxHashMap::<String, Range>::default();
|
||||
let mut failed = false;
|
||||
|
||||
for cons in &entr.constructors {
|
||||
|
||||
match repeated_names.get(&cons.name.to_string()) {
|
||||
Some(_) => {
|
||||
failed = true;
|
||||
},
|
||||
None => {
|
||||
repeated_names.insert(cons.name.to_string(), cons.name.range);
|
||||
},
|
||||
}
|
||||
|
||||
let name_cons = entr.name.add_segment(cons.name.to_str());
|
||||
self.context_vars
|
||||
.push((name_cons.range, name_cons.to_string()));
|
||||
self.context_vars.push((name_cons.range, name_cons.to_string()));
|
||||
}
|
||||
|
||||
if failed {
|
||||
return;
|
||||
}
|
||||
|
||||
let vars = self.context_vars.clone();
|
||||
@ -176,10 +222,7 @@ impl Visitor for UnboundCollector {
|
||||
|
||||
self.context_vars = inside_vars;
|
||||
}
|
||||
TopLevel::Entry(entr) => {
|
||||
self.context_vars.push((entr.range, entr.to_string()));
|
||||
self.visit_entry(entr)
|
||||
}
|
||||
TopLevel::Entry(entr) => self.visit_entry(entr),
|
||||
}
|
||||
}
|
||||
|
||||
@ -203,7 +246,7 @@ impl Visitor for UnboundCollector {
|
||||
fn visit_destruct(&mut self, destruct: &mut Destruct) {
|
||||
match destruct {
|
||||
Destruct::Destruct(range, ty, bindings, _) => {
|
||||
self.visit_ident(&mut Ident::new_by_sugar(&format!("{}.open", ty), *range));
|
||||
self.visit_qualified_ident(QualifiedIdent::add_segment(ty, "open").to_sugar());
|
||||
self.visit_range(range);
|
||||
self.visit_qualified_ident(ty);
|
||||
for bind in bindings {
|
||||
@ -304,14 +347,9 @@ impl Visitor for UnboundCollector {
|
||||
fn visit_expr(&mut self, expr: &mut Expr) {
|
||||
match &mut expr.data {
|
||||
ExprKind::Var(ident) => self.visit_ident(ident),
|
||||
ExprKind::Constr(ident) => {
|
||||
if !self.context_vars.iter().any(|x| x.1 == ident.to_string()) {
|
||||
let entry = self
|
||||
.unbound_top_level
|
||||
.entry(ident.to_string())
|
||||
.or_insert_with(|| Vec::new());
|
||||
entry.push(ident.clone());
|
||||
}
|
||||
ExprKind::Constr(ident, spine) => {
|
||||
self.visit_qualified_ident(ident);
|
||||
visit_vec!(spine.iter_mut(), arg => self.visit_binding(arg));
|
||||
}
|
||||
ExprKind::All(None, typ, body) => {
|
||||
self.visit_expr(typ);
|
||||
@ -353,22 +391,23 @@ impl Visitor for UnboundCollector {
|
||||
self.context_vars = vars;
|
||||
}
|
||||
ExprKind::Sigma(None, typ, body) => {
|
||||
self.visit_ident(&mut Ident::new_by_sugar("Sigma", expr.range));
|
||||
self.visit_qualified_ident(
|
||||
QualifiedIdent::new_static("Sigma", None, expr.range).to_sugar(),
|
||||
);
|
||||
self.visit_expr(typ);
|
||||
self.visit_expr(body);
|
||||
}
|
||||
ExprKind::Sigma(Some(ident), typ, body) => {
|
||||
self.visit_ident(&mut Ident::new_by_sugar("Sigma", expr.range));
|
||||
self.visit_qualified_ident(
|
||||
QualifiedIdent::new_static("Sigma", None, expr.range).to_sugar(),
|
||||
);
|
||||
self.visit_expr(typ);
|
||||
self.context_vars.push((ident.range, ident.to_string()));
|
||||
self.visit_expr(body);
|
||||
self.context_vars.pop();
|
||||
}
|
||||
ExprKind::Match(matcher) => {
|
||||
self.visit_ident(&mut Ident::new_by_sugar(
|
||||
&format!("{}.match", matcher.typ.to_string().as_str()),
|
||||
expr.range,
|
||||
));
|
||||
self.visit_qualified_ident(matcher.typ.add_segment("match").to_sugar());
|
||||
self.visit_match(matcher)
|
||||
}
|
||||
ExprKind::Subst(subst) => {
|
||||
@ -386,30 +425,32 @@ impl Visitor for UnboundCollector {
|
||||
}
|
||||
ExprKind::Hole => {}
|
||||
ExprKind::Do(typ, sttm) => {
|
||||
self.visit_ident(&mut Ident::new_by_sugar(
|
||||
&format!("{}.pure", typ),
|
||||
expr.range,
|
||||
));
|
||||
self.visit_ident(&mut Ident::new_by_sugar(
|
||||
&format!("{}.bind", typ),
|
||||
expr.range,
|
||||
));
|
||||
self.visit_qualified_ident(typ.add_segment("pure").to_sugar());
|
||||
self.visit_qualified_ident(typ.add_segment("bind").to_sugar());
|
||||
self.visit_sttm(sttm)
|
||||
}
|
||||
ExprKind::If(cond, if_, else_) => {
|
||||
self.visit_ident(&mut Ident::new_by_sugar("Bool.if", expr.range));
|
||||
self.visit_qualified_ident(&mut QualifiedIdent::new_sugared(
|
||||
"Bool", "if", expr.range,
|
||||
));
|
||||
self.visit_expr(cond);
|
||||
self.visit_expr(if_);
|
||||
self.visit_expr(else_);
|
||||
}
|
||||
ExprKind::Pair(l, r) => {
|
||||
self.visit_ident(&mut Ident::new_by_sugar("Pair.new", expr.range));
|
||||
self.visit_qualified_ident(&mut QualifiedIdent::new_sugared(
|
||||
"Pair", "new", expr.range,
|
||||
));
|
||||
self.visit_expr(l);
|
||||
self.visit_expr(r);
|
||||
}
|
||||
ExprKind::List(spine) => {
|
||||
self.visit_ident(&mut Ident::new_by_sugar("List.nil", expr.range));
|
||||
self.visit_ident(&mut Ident::new_by_sugar("List.cons", expr.range));
|
||||
self.visit_qualified_ident(&mut QualifiedIdent::new_sugared(
|
||||
"List", "nil", expr.range,
|
||||
));
|
||||
self.visit_qualified_ident(&mut QualifiedIdent::new_sugared(
|
||||
"List", "cons", expr.range,
|
||||
));
|
||||
visit_vec!(spine.iter_mut(), arg => self.visit_expr(arg));
|
||||
}
|
||||
}
|
||||
|
@ -14,6 +14,7 @@ pub struct Chars {
|
||||
pub bxline: char,
|
||||
pub brline: char,
|
||||
pub ylline: char,
|
||||
pub bullet: char,
|
||||
}
|
||||
|
||||
impl Chars {
|
||||
@ -26,6 +27,7 @@ impl Chars {
|
||||
bxline: '┬',
|
||||
brline: '┌',
|
||||
ylline: '├',
|
||||
bullet: '•',
|
||||
}
|
||||
}
|
||||
pub fn ascii() -> &'static Chars {
|
||||
@ -37,6 +39,7 @@ impl Chars {
|
||||
bxline: 'v',
|
||||
brline: '/',
|
||||
ylline: '-',
|
||||
bullet: '*',
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -63,7 +66,15 @@ impl<'a> RenderConfig<'a> {
|
||||
}
|
||||
|
||||
pub fn check_if_colors_are_supported(disable: bool) {
|
||||
if cfg!(windows) && !Paint::enable_windows_ascii() || disable {
|
||||
if disable || (cfg!(windows) && !Paint::enable_windows_ascii()) {
|
||||
Paint::disable();
|
||||
}
|
||||
}
|
||||
|
||||
pub fn check_if_utf8_is_supported<'a>(disable: bool, indent: usize) -> RenderConfig<'a> {
|
||||
if disable || (cfg!(windows) && !Paint::enable_windows_ascii()) {
|
||||
RenderConfig::ascii(indent)
|
||||
} else {
|
||||
RenderConfig::unicode(indent)
|
||||
}
|
||||
}
|
||||
|
@ -277,7 +277,10 @@ fn write_code_block<'a, T: Write + Sized>(
|
||||
}
|
||||
|
||||
let code_lines: Vec<&'a str> = group_code.lines().collect();
|
||||
let mut lines = lines_set.iter().collect::<Vec<&usize>>();
|
||||
let mut lines = lines_set
|
||||
.iter()
|
||||
.filter(|x| **x < code_lines.len())
|
||||
.collect::<Vec<&usize>>();
|
||||
lines.sort();
|
||||
|
||||
for i in 0..lines.len() {
|
||||
@ -409,7 +412,13 @@ impl<'a> Report for Diagnostic<'a> {
|
||||
match subtitle {
|
||||
Subtitle::Normal(color, phr) => {
|
||||
let colorizer = get_colorizer(color);
|
||||
writeln!(fmt, "{:>5} {} {}", "", colorizer("•"), Paint::new(phr))?;
|
||||
writeln!(
|
||||
fmt,
|
||||
"{:>5} {} {}",
|
||||
"",
|
||||
colorizer(config.chars.bullet),
|
||||
Paint::new(phr)
|
||||
)?;
|
||||
}
|
||||
Subtitle::Bold(color, phr) => {
|
||||
let colorizer = get_colorizer(color);
|
||||
@ -417,13 +426,13 @@ impl<'a> Report for Diagnostic<'a> {
|
||||
fmt,
|
||||
"{:>5} {} {}",
|
||||
"",
|
||||
colorizer("•"),
|
||||
colorizer(config.chars.bullet),
|
||||
Paint::new(phr).bold()
|
||||
)?;
|
||||
}
|
||||
Subtitle::Phrase(color, words) => {
|
||||
let colorizer = get_colorizer(color);
|
||||
write!(fmt, "{:>5} {} ", "", colorizer("•"))?;
|
||||
write!(fmt, "{:>5} {} ", "", colorizer(config.chars.bullet))?;
|
||||
for word in words {
|
||||
match word {
|
||||
Word::Normal(str) => write!(fmt, "{} ", Paint::new(str))?,
|
||||
@ -444,7 +453,7 @@ impl<'a> Report for Diagnostic<'a> {
|
||||
}
|
||||
|
||||
let groups = group_markers(&self.frame.positions);
|
||||
let is_empty = groups.len() == 0;
|
||||
let is_empty = groups.is_empty();
|
||||
|
||||
for (ctx, group) in groups {
|
||||
writeln!(fmt)?;
|
||||
|
@ -11,7 +11,7 @@ pub fn compile_term(expr: &desugared::Expr) -> Box<Term> {
|
||||
}),
|
||||
Lambda(binder, body) => Box::new(Term::Lam {
|
||||
name: binder.to_string(),
|
||||
body: compile_term(&body),
|
||||
body: compile_term(body),
|
||||
}),
|
||||
App(head, spine) => spine.iter().fold(compile_term(head), |func, arg| {
|
||||
Box::new(Term::App {
|
||||
@ -36,14 +36,14 @@ pub fn compile_term(expr: &desugared::Expr) -> Box<Term> {
|
||||
name: op.to_string(),
|
||||
args: vec![compile_term(l), compile_term(r)],
|
||||
}),
|
||||
Hole(_) => unreachable!("Internal Error: 'Hole' cannot be a relevant term"),
|
||||
Typ => unreachable!("Internal Error: 'Typ' cannot be a relevant term"),
|
||||
NumType(desugared::NumType::U60) => unreachable!("Internal Error: 'U60' cannot be a relevant term"),
|
||||
NumType(desugared::NumType::U120) => unreachable!("Internal Error: 'U120' cannot be a relevant term"),
|
||||
All(_, _, _) => unreachable!("Internal Error: 'All' cannot be a relevant term"),
|
||||
Str(_) => unreachable!("Internal Error: 'Str' cannot be a relevant term"),
|
||||
Hole(_) => unreachable!("Internal Error: 'Hole' cannot be a relevant term"),
|
||||
Hlp(_) => unreachable!("Internal Error: 'Hlp' cannot be a relevant term"),
|
||||
Err => unreachable!("Internal Error: 'Err' cannot be a relevant term"),
|
||||
All(_, _, _) => unreachable!("Internal Error: 'All' cannot be a relevant term"),
|
||||
}
|
||||
}
|
||||
|
||||
@ -57,7 +57,7 @@ pub fn compile_rule(rule: desugared::Rule) -> Rule {
|
||||
}
|
||||
}
|
||||
|
||||
pub fn compile_entry(file: &mut File, entry: Box<desugared::Entry>) {
|
||||
pub fn compile_entry(file: &mut File, entry: desugared::Entry) {
|
||||
for rule in entry.rules {
|
||||
file.rules.push(compile_rule(rule))
|
||||
}
|
||||
@ -68,7 +68,7 @@ pub fn compile_book(book: desugared::Book) -> File {
|
||||
rules: Default::default(),
|
||||
};
|
||||
for (_, entry) in book.entrs {
|
||||
compile_entry(&mut file, entry);
|
||||
compile_entry(&mut file, *entry);
|
||||
}
|
||||
file
|
||||
}
|
||||
|
@ -113,7 +113,7 @@ pub enum ExprKind {
|
||||
/// Name of a variable
|
||||
Var(Ident),
|
||||
/// Name of a function/constructor
|
||||
Constr(QualifiedIdent),
|
||||
Constr(QualifiedIdent, Spine),
|
||||
/// The dependent function space (e.g. (x : Int) -> y)
|
||||
All(Option<Ident>, Box<Expr>, Box<Expr>),
|
||||
/// The dependent product space (e.g. [x : Int] -> y)
|
||||
@ -371,7 +371,12 @@ impl Display for Expr {
|
||||
Sigma(_, _, _) => write!(f, "({})", self.traverse_pi_types()),
|
||||
Lit(lit) => write!(f, "{}", lit),
|
||||
Var(name) => write!(f, "{}", name),
|
||||
Constr(name) => write!(f, "{}", name),
|
||||
Constr(head, spine) => write!(
|
||||
f,
|
||||
"({}{})",
|
||||
head,
|
||||
spine.iter().map(|x| format!(" {}", x)).collect::<String>()
|
||||
),
|
||||
Lambda(binder, None, body) => write!(f, "({} => {})", binder, body),
|
||||
Lambda(binder, Some(typ), body) => write!(f, "(({} : {}) => {})", binder, typ, body),
|
||||
Pair(fst, snd) => write!(f, "($ {} {})", fst, snd),
|
||||
|
@ -170,9 +170,10 @@ impl TopLevel {
|
||||
/// A module is a collection of top level entries
|
||||
/// that contains syntatic sugars. In the future
|
||||
/// it will contain a HashMap to local renames.
|
||||
#[derive(Clone, Debug, Default, Hash, PartialEq, Eq)]
|
||||
#[derive(Clone, Debug, PartialEq, Eq)]
|
||||
pub struct Module {
|
||||
pub entries: Vec<TopLevel>,
|
||||
pub uses: FxHashMap<String, String>,
|
||||
}
|
||||
|
||||
/// Metadata about entries, it's really useful when we
|
||||
@ -251,7 +252,7 @@ impl Display for TopLevel {
|
||||
}
|
||||
writeln!(f, " {{")?;
|
||||
for cons in &sum.constructors {
|
||||
writeln!(f, " {},", cons)?;
|
||||
writeln!(f, " {}", cons)?;
|
||||
}
|
||||
writeln!(f, "}}\n")
|
||||
}
|
||||
@ -275,7 +276,7 @@ impl Display for TopLevel {
|
||||
}
|
||||
writeln!(f, "}}\n")
|
||||
}
|
||||
TopLevel::Entry(entr) => writeln!(f, "{}\n", entr),
|
||||
TopLevel::Entry(entr) => writeln!(f, "{}", entr),
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -283,7 +284,16 @@ impl Display for TopLevel {
|
||||
impl Display for Module {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
for entr in &self.entries {
|
||||
writeln!(f, "{}", entr)?;
|
||||
write!(f, "{}", entr)?;
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Book {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
for entr in self.entries.values() {
|
||||
write!(f, "{}", entr)?;
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
@ -320,10 +330,10 @@ impl Display for Entry {
|
||||
write!(f, " {}", arg)?;
|
||||
}
|
||||
|
||||
write!(f, " : {}", &self.typ)?;
|
||||
writeln!(f, " : {}", &self.typ)?;
|
||||
|
||||
for rule in &self.rules {
|
||||
write!(f, "\n{}", rule)?
|
||||
writeln!(f, "{}", rule)?
|
||||
}
|
||||
|
||||
Ok(())
|
||||
@ -582,7 +592,7 @@ impl Entry {
|
||||
hiddens,
|
||||
erased,
|
||||
arguments,
|
||||
is_ctr: false,
|
||||
is_ctr: self.rules.is_empty(),
|
||||
range: self.name.range,
|
||||
}
|
||||
}
|
||||
|
@ -365,7 +365,12 @@ pub fn walk_expr<T: Visitor>(ctx: &mut T, expr: &mut Expr) {
|
||||
ctx.visit_range(&mut expr.range);
|
||||
match &mut expr.data {
|
||||
ExprKind::Var(ident) => ctx.visit_ident(ident),
|
||||
ExprKind::Constr(ident) => ctx.visit_qualified_ident(ident),
|
||||
ExprKind::Constr(ident, spine) => {
|
||||
ctx.visit_qualified_ident(ident);
|
||||
for arg in spine {
|
||||
ctx.visit_binding(arg);
|
||||
}
|
||||
}
|
||||
ExprKind::All(None, typ, body) => {
|
||||
ctx.visit_expr(typ);
|
||||
ctx.visit_expr(body);
|
||||
|
@ -3,6 +3,7 @@
|
||||
|
||||
use std::fmt::{Display, Error, Formatter};
|
||||
|
||||
use fxhash::FxHashMap;
|
||||
use kind_span::{Range, Span};
|
||||
use linked_hash_map::LinkedHashMap;
|
||||
|
||||
@ -279,6 +280,7 @@ pub struct Entry {
|
||||
#[derive(Clone, Debug, Default)]
|
||||
pub struct Book {
|
||||
pub entrs: LinkedHashMap<String, Box<Entry>>,
|
||||
pub names: FxHashMap<String, usize>,
|
||||
pub holes: u64,
|
||||
}
|
||||
|
||||
|
@ -42,6 +42,10 @@ impl QualifiedIdent {
|
||||
}
|
||||
}
|
||||
|
||||
pub fn change_root(&mut self, str: String) {
|
||||
self.root = Symbol(str);
|
||||
}
|
||||
|
||||
/// Avoid this function. It transforms a QualifiedIdent into a Ident
|
||||
pub fn to_ident(&self) -> Ident {
|
||||
Ident {
|
||||
@ -50,27 +54,37 @@ impl QualifiedIdent {
|
||||
}
|
||||
}
|
||||
|
||||
pub fn new_static(root: String, aux: Option<String>, range: Range) -> QualifiedIdent {
|
||||
pub fn new_static(root: &str, aux: Option<String>, range: Range) -> QualifiedIdent {
|
||||
QualifiedIdent {
|
||||
root: Symbol(root),
|
||||
root: Symbol(root.to_string()),
|
||||
aux: aux.map(Symbol),
|
||||
range,
|
||||
used_by_sugar: false,
|
||||
}
|
||||
}
|
||||
|
||||
pub fn add_segment(&self, extension: &str) -> QualifiedIdent {
|
||||
let aux = match self.aux.clone() {
|
||||
Some(res) => Symbol(format!("{}.{}", res.0, extension)),
|
||||
None => Symbol(extension.to_string()),
|
||||
};
|
||||
pub fn new_sugared(root: &str, aux: &str, range: Range) -> QualifiedIdent {
|
||||
QualifiedIdent {
|
||||
root: self.root.clone(),
|
||||
aux: Some(aux),
|
||||
range: self.range.clone(),
|
||||
root: Symbol(root.to_string()),
|
||||
aux: Some(Symbol(aux.to_string())),
|
||||
range,
|
||||
used_by_sugar: true,
|
||||
}
|
||||
}
|
||||
|
||||
pub fn add_segment(&self, extension: &str) -> QualifiedIdent {
|
||||
QualifiedIdent {
|
||||
root: Symbol(format!("{}.{}", self.root.0, extension)),
|
||||
aux: self.aux.clone(),
|
||||
range: self.range,
|
||||
used_by_sugar: self.used_by_sugar,
|
||||
}
|
||||
}
|
||||
|
||||
pub fn to_sugar(&mut self) -> &mut QualifiedIdent {
|
||||
self.used_by_sugar = true;
|
||||
self
|
||||
}
|
||||
}
|
||||
|
||||
impl Ident {
|
||||
|
Loading…
Reference in New Issue
Block a user