From 58684b874b85d76a2ed39360a1228967e7ec8034 Mon Sep 17 00:00:00 2001 From: felipegchi Date: Fri, 18 Nov 2022 08:52:27 -0300 Subject: [PATCH] fix: bug fixes in erasure --- src/kind-cli/src/lib.rs | 41 ++++++-- src/kind-driver/src/lib.rs | 9 +- src/kind-driver/src/resolution.rs | 42 +++++---- src/kind-driver/src/session.rs | 7 +- src/kind-parser/src/expr.rs | 3 + src/kind-parser/src/top_level/type_decl.rs | 2 + src/kind-pass/src/desugar/destruct.rs | 3 +- src/kind-pass/src/erasure/mod.rs | 39 ++++---- src/kind-pass/src/unbound/mod.rs | 10 +- src/kind-query/src/errors.rs | 105 +++++++++++++++++++++ src/kind-query/src/graph.rs | 44 +++++++-- src/kind-query/src/lib.rs | 15 ++- src/kind-query/src/names.rs | 37 ++++++++ src/kind-report/src/report.rs | 6 +- src/kind-tree/src/concrete/expr.rs | 14 +-- src/kind-tree/src/concrete/mod.rs | 9 +- src/kind-tree/src/symbol.rs | 1 + 17 files changed, 302 insertions(+), 85 deletions(-) create mode 100644 src/kind-query/src/errors.rs create mode 100644 src/kind-query/src/names.rs diff --git a/src/kind-cli/src/lib.rs b/src/kind-cli/src/lib.rs index b5f26ec8..eeae1121 100644 --- a/src/kind-cli/src/lib.rs +++ b/src/kind-cli/src/lib.rs @@ -36,6 +36,12 @@ pub struct Cli { #[arg(short, long)] pub ascii: bool, + #[arg(short, long)] + entrypoint: Option, + + #[arg(short, long, value_name = "FILE")] + pub root: Option, + #[command(subcommand)] pub command: Command, } @@ -47,12 +53,15 @@ pub enum Command { Check { file: String }, /// Evaluates Main on Kind2 - #[clap(aliases = &["e"])] + #[clap(aliases = &["er"])] Eval { file: String }, #[clap(aliases = &["k"])] ToKindCore { file: String }, + #[clap(aliases = &["e"])] + Erase { file: String }, + /// Runs Main on the HVM #[clap(aliases = &["r"])] Run { file: String }, @@ -76,7 +85,9 @@ pub enum Command { /// Compiles a file to HVM (.hvm) #[clap(aliases = &["hvm"])] - ToHVM { file: String }, + ToHVM { + file: String + }, /// Watch for file changes and then /// check when some file change. @@ -156,7 +167,13 @@ pub fn run_cli(config: Cli) { 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("."); + let root = config.root.unwrap_or_else(|| PathBuf::from(".")); + + let mut entrypoints = vec!["Main".to_string()]; + + if let Some(res) = &config.entrypoint { + entrypoints.push(res.clone()) + } match config.command { Command::Check { file } => { @@ -166,8 +183,7 @@ pub fn run_cli(config: Cli) { } Command::ToHVM { file } => { compile_in_session(render_config, root, file.clone(), &mut |session| { - // TODO: Who sets the entrypoint? - let book = driver::erase_book(session, &PathBuf::from(file.clone()), &["Main".to_string()])?; + let book = driver::erase_book(session, &PathBuf::from(file.clone()), &entrypoints)?; Some(driver::compile_book_to_hvm(book)) }) .map(|res| { @@ -177,7 +193,11 @@ pub fn run_cli(config: Cli) { } Command::Run { file } => { compile_in_session(render_config, root, file.clone(), &mut |session| { - let book = driver::desugar_book(session, &PathBuf::from(file.clone()))?; + let book = driver::erase_book( + session, + &PathBuf::from(file.clone()), + &["Main".to_string()], + )?; driver::check_main_entry(session, &book)?; Some(driver::compile_book_to_hvm(book)) }) @@ -210,6 +230,15 @@ pub fn run_cli(config: Cli) { compile_in_session(render_config, root, file.clone(), &mut |session| { driver::desugar_book(session, &PathBuf::from(file.clone())) }) + .map(|res| { + print!("Ok"); + res + }); + } + Command::Erase { file } => { + compile_in_session(render_config, root, file.clone(), &mut |session| { + driver::erase_book(session, &PathBuf::from(file.clone()), &entrypoints) + }) .map(|res| { print!("{}", res); res diff --git a/src/kind-driver/src/lib.rs b/src/kind-driver/src/lib.rs index 0bd5227b..36a936b2 100644 --- a/src/kind-driver/src/lib.rs +++ b/src/kind-driver/src/lib.rs @@ -1,11 +1,12 @@ use errors::DriverError; +use fxhash::FxHashSet; 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::{collections::HashSet, path::PathBuf}; +use std::{path::PathBuf}; use kind_checker as checker; @@ -33,7 +34,7 @@ pub fn type_check_book(session: &mut Session, path: &PathBuf) -> Option Option( book: &'a mut Book, ) -> bool { if let Some(first_occorence) = book.names.get(ident.to_string().as_str()) { - session + /*session .diagnostic_sender .send(Box::new(DriverError::DefinedMultipleTimes( first_occorence.clone(), ident, ))) .unwrap(); - *failed = true; - false + *failed = true;*/ + true } else { book.names.insert(ident.to_string(), ident); true @@ -98,20 +98,15 @@ fn try_to_insert_new_name<'a>( fn module_to_book<'a>( failed: &mut bool, session: &'a Session, - module: &Module, + module: Module, book: &'a mut Book, -) -> HashSet { - let mut public_names = HashSet::new(); +) -> FxHashSet { + let mut public_names = FxHashSet::default(); - for entry in &module.entries { - match &entry { + for entry in module.entries { + match entry { TopLevel::SumType(sum) => { public_names.insert(sum.name.to_string()); - 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 mut cons_ident = sum.name.add_segment(cons.name.to_str()); @@ -119,18 +114,22 @@ fn module_to_book<'a>( 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)); + .insert(cons_ident.to_string(), cons.extract_book_info(&sum)); } } + + 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(), TopLevel::SumType(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(failed, session, rec.name.clone(), book); - - book.entries.insert(rec.name.to_string(), entry.clone()); - + let cons_ident = rec.name.add_segment(rec.constructor.to_str()); public_names.insert(cons_ident.to_string()); book.count.insert( @@ -138,13 +137,15 @@ fn module_to_book<'a>( rec.extract_book_info_of_constructor(), ); try_to_insert_new_name(failed, session, cons_ident, book); + + book.entries.insert(rec.name.to_string(), TopLevel::RecordType(rec)); } TopLevel::Entry(entr) => { 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()); - book.entries.insert(entr.name.to_string(), entry.clone()); + book.entries.insert(entr.name.to_string(), TopLevel::Entry(entr)); } } } @@ -226,7 +227,7 @@ fn parse_and_store_book_by_path<'a>( expand_uses(&mut module, session.diagnostic_sender.clone()); - module_to_book(&mut failed, session, &module, book); + module_to_book(&mut failed, session, module, book); failed } @@ -268,6 +269,7 @@ pub fn check_unbound_top_level(session: &mut Session, book: &mut Book) -> bool { for (_, unbound) in unbound_tops { let res: Vec = unbound .iter() + .filter(|x| !x.used_by_sugar) .map(|x| x.to_ident()) .collect(); if !res.is_empty() { diff --git a/src/kind-driver/src/session.rs b/src/kind-driver/src/session.rs index 27fc2abd..e0333da9 100644 --- a/src/kind-driver/src/session.rs +++ b/src/kind-driver/src/session.rs @@ -2,12 +2,11 @@ //! model because I want to change it to a query based compiler //! later. -use std::collections::HashSet; use std::path::PathBuf; use std::rc::Rc; use std::sync::mpsc::Sender; -use fxhash::FxHashMap; +use fxhash::{FxHashMap, FxHashSet}; use kind_report::data::Diagnostic; #[derive(Debug, Clone)] @@ -18,7 +17,7 @@ pub struct Session { /// It will be useful in the future /// to make the public and private decls - pub public_names: FxHashMap>, + pub public_names: FxHashSet, pub diagnostic_sender: Sender>, pub root: PathBuf, @@ -32,7 +31,7 @@ impl Session { loaded_paths: Vec::new(), loaded_sources: Vec::new(), loaded_paths_map: FxHashMap::default(), - public_names: FxHashMap::default(), + public_names: FxHashSet::default(), root, book_counter: 0, diagnostic_sender: sender, diff --git a/src/kind-parser/src/expr.rs b/src/kind-parser/src/expr.rs index da4fd620..3d5a419f 100644 --- a/src/kind-parser/src/expr.rs +++ b/src/kind-parser/src/expr.rs @@ -553,6 +553,7 @@ impl<'a> Parser<'a> { self.advance(); // 'return' let expr = self.parse_expr(false)?; let end = expr.range; + self.check_and_eat(Token::Semi); Ok(Box::new(Sttm { data: SttmKind::Return(expr), range: start.mix(end), @@ -576,6 +577,7 @@ impl<'a> Parser<'a> { range: start.mix(end), })) } else { + self.check_and_eat(Token::Semi); let next = self.parse_sttm()?; let end = next.range; Ok(Box::new(Sttm { @@ -654,6 +656,7 @@ impl<'a> Parser<'a> { let (_range, bindings, ignore_rest) = self.parse_pat_destruct_bindings()?; self.eat_variant(Token::FatArrow)?; let value = self.parse_expr(false)?; + self.check_and_eat(Token::Semi); cases.push(Case { constructor, diff --git a/src/kind-parser/src/top_level/type_decl.rs b/src/kind-parser/src/top_level/type_decl.rs index 03057a70..6b0a047d 100644 --- a/src/kind-parser/src/top_level/type_decl.rs +++ b/src/kind-parser/src/top_level/type_decl.rs @@ -16,6 +16,8 @@ impl<'a> Parser<'a> { None }; + self.check_and_eat(Token::Semi); + Ok(Constructor { name, docs, diff --git a/src/kind-pass/src/desugar/destruct.rs b/src/kind-pass/src/desugar/destruct.rs index 1e0f2cf3..a59b36e7 100644 --- a/src/kind-pass/src/desugar/destruct.rs +++ b/src/kind-pass/src/desugar/destruct.rs @@ -108,7 +108,8 @@ impl<'a> DesugarState<'a> { } } - let irrelev = count.arguments.map(|x| x.erased).to_vec(); + let mut irrelev = count.arguments.map(|x| x.erased).to_vec(); + irrelev = irrelev[record.parameters.len()..].to_vec(); let spine = vec![ val, diff --git a/src/kind-pass/src/erasure/mod.rs b/src/kind-pass/src/erasure/mod.rs index ab21fe0e..9f55882a 100644 --- a/src/kind-pass/src/erasure/mod.rs +++ b/src/kind-pass/src/erasure/mod.rs @@ -74,7 +74,7 @@ pub fn erase_book( for (name, v) in &book.entrs { entries.insert(name, state.erase_entry(v)); } - + if state.failed { return None; } @@ -90,13 +90,6 @@ pub fn erase_book( Some(new_book) } -pub fn erasure_to_relevance(erased: bool) -> Relevance { - if erased { - Relevance::Irrelevant - } else { - Relevance::Relevant - } -} impl<'a> ErasureState<'a> { pub fn new_hole(&mut self, range: Range, name: String) -> (Option, Relevance) { @@ -159,6 +152,12 @@ impl<'a> ErasureState<'a> { // "erased" in the sense that we can just remove them from the runtime and it'll // be fine. (None, Relevance::Irrelevant) => false, + + (None, Relevance::Hole(n)) => { + self.holes[hole] = Some(Relevance::Hole(n)); + true + }, + (_, _) => true, }, (Relevance::Relevant, Relevance::Hole(hole)) => match self.holes[hole] { @@ -195,6 +194,7 @@ impl<'a> ErasureState<'a> { name: &QualifiedIdent, spine: &Vec>, ) -> Vec> { + let fun = match self.names.get(&name.to_string()) { Some(res) => *res, None => self.new_hole(name.range, name.to_string()), @@ -207,19 +207,18 @@ impl<'a> ErasureState<'a> { let entry = self.book.entrs.get(name.to_string().as_str()).unwrap(); let erased = entry.args.iter(); - let irrelevances = erased.map(|arg| { - if arg.erased { - (Some(arg.span), Relevance::Irrelevant) - } else { - on - } - }); - spine .iter() - .zip(irrelevances) - .map(|(arg, relev)| (self.erase_pat(relev, arg), relev.1.clone())) - .filter(|res| res.1 == Relevance::Relevant) + .zip(erased) + .map(|(elem, arg)| { + let relev = if arg.erased { + (Some(arg.span), Relevance::Irrelevant) + } else { + on.clone() + }; + (self.erase_pat(relev, elem), arg.erased) + }) + .filter(|res| !res.1) .map(|res| res.0) .collect() } @@ -456,7 +455,7 @@ impl<'a> ErasureState<'a> { .map(|((range, erased), expr)| { ( erased, - self.erase_pat((Some(*range), erasure_to_relevance(*erased)), expr), + self.erase_pat((Some(*range), if *erased { Relevance::Irrelevant} else { place.1.clone() }), expr), ) }) .filter(|(erased, _)| !*erased) diff --git a/src/kind-pass/src/unbound/mod.rs b/src/kind-pass/src/unbound/mod.rs index c56398eb..3ba17911 100644 --- a/src/kind-pass/src/unbound/mod.rs +++ b/src/kind-pass/src/unbound/mod.rs @@ -110,14 +110,15 @@ impl Visitor for UnboundCollector { fn visit_attr(&mut self, _: &mut kind_tree::concrete::Attribute) {} fn visit_ident(&mut self, ident: &mut Ident) { + let name = ident.to_str(); if self .context_vars .iter() - .all(|x| x.1 != ident.data.to_string()) + .all(|x| x.1 != name) { let entry = self .unbound - .entry(ident.to_string()) + .entry(name.to_string()) .or_insert_with(Vec::new); entry.push(ident.clone()); } @@ -131,10 +132,11 @@ impl Visitor for UnboundCollector { } fn visit_pat_ident(&mut self, ident: &mut PatIdent) { + let name = ident.0.to_str(); if let Some(fst) = self .context_vars .iter() - .find(|x| x.1 == ident.0.data.to_string()) + .find(|x| x.1 == name) { if self.emit_errs { self.errors @@ -142,7 +144,7 @@ impl Visitor for UnboundCollector { .unwrap() } } else { - self.context_vars.push((ident.0.range, ident.0.to_string())) + self.context_vars.push((ident.0.range, name.to_string())) } } diff --git a/src/kind-query/src/errors.rs b/src/kind-query/src/errors.rs new file mode 100644 index 00000000..c8d4183a --- /dev/null +++ b/src/kind-query/src/errors.rs @@ -0,0 +1,105 @@ +//! Errors created by the driver. All of them +//! are related with paths and unbounded variables. + +use std::path::PathBuf; + +use kind_report::data::{Color, Diagnostic, DiagnosticFrame, Marker, Severity, Subtitle, Word}; +use kind_tree::symbol::{Ident, QualifiedIdent}; + +/// Describes all of the possible errors inside each +/// of the passes inside this crate. +pub(crate) enum DriverError { + CannotFindFile(String), + UnboundVariable(Vec, Vec), + MultiplePaths(QualifiedIdent, Vec), + DefinedMultipleTimes(QualifiedIdent, QualifiedIdent), + ThereIsntAMain, +} + +impl Diagnostic for DriverError { + fn to_diagnostic_frame(&self) -> DiagnosticFrame { + match self { + DriverError::UnboundVariable(idents, suggestions) => DiagnosticFrame { + code: 100, + severity: Severity::Error, + title: format!("Cannot find the definition '{}'.", idents[0].to_str()), + subtitles: vec![], + hints: vec![if !suggestions.is_empty() { + format!( + "Maybe you're looking for {}", + suggestions.iter().map(|x| format!("'{}'", x)).collect::>().join(", ") + ) + } else { + "Take a look at the rules for name searching at https://kind.kindelia.org/hints/name-search".to_string() + }], + positions: idents + .iter() + .map(|ident| Marker { + position: ident.range, + color: Color::Fst, + text: "Here!".to_string(), + no_code: false, + main: true, + }) + .collect(), + }, + DriverError::MultiplePaths(ident, paths) => DiagnosticFrame { + code: 101, + severity: Severity::Error, + title: "Multiple definitions for the same name".to_string(), + subtitles: paths + .iter() + .map(|path| Subtitle::Phrase(Color::Fst, vec![Word::White(path.display().to_string())])) + .collect(), + hints: vec!["Take a look at the rules for name searching at https://kind.kindelia.org/hints/name-search".to_string()], + positions: vec![Marker { + position: ident.range, + color: Color::Fst, + text: "Here!".to_string(), + no_code: false, + main: true, + }], + }, + DriverError::DefinedMultipleTimes(fst, snd) => DiagnosticFrame { + code: 102, + severity: Severity::Error, + title: "Defined multiple times for the same name".to_string(), + subtitles: vec![], + hints: vec!["Rename one of the definitions or remove and look at how names work in Kind at https://kind.kindelia.org/hints/names".to_string()], + positions: vec![ + Marker { + position: fst.range, + color: Color::Fst, + text: "The first ocorrence".to_string(), + no_code: false, + main: true, + }, + Marker { + position: snd.range, + color: Color::Snd, + text: "Second occorrence here!".to_string(), + no_code: false, + main: false, + }, + ], + }, + DriverError::CannotFindFile(file) => DiagnosticFrame { + code: 103, + severity: Severity::Error, + title: format!("Cannot find file '{}'", file), + subtitles: vec![], + hints: vec![], + positions: vec![], + }, + + DriverError::ThereIsntAMain => DiagnosticFrame { + code: 103, + severity: Severity::Error, + title: format!("Cannot find 'Main' function to run the file."), + subtitles: vec![], + hints: vec![], + positions: vec![], + }, + } + } +} diff --git a/src/kind-query/src/graph.rs b/src/kind-query/src/graph.rs index 0ca3584a..d4613229 100644 --- a/src/kind-query/src/graph.rs +++ b/src/kind-query/src/graph.rs @@ -1,43 +1,63 @@ use std::collections::HashMap; -use fxhash::FxHashSet; +use fxhash::{FxHashSet, FxHashMap}; struct Node { data: T, invalidated: bool, children: FxHashSet, parents: FxHashSet, + root: bool, } -#[derive(Default)] pub struct Graph { // Using a hashmap to make it easier to add or remove node.s - nodes: HashMap>, + nodes: FxHashMap>, count: usize, } +impl Default for Graph { + fn default() -> Self { + Self { nodes: Default::default(), count: Default::default() } + } +} + impl Graph { - pub fn add(&mut self, data: T, parent: usize) { + pub fn add(&mut self, data: T, root: bool) { self.nodes.insert( self.count, Node { data, invalidated: false, children: FxHashSet::default(), - parents: FxHashSet::from_iter(vec![parent]), + parents: FxHashSet::default(), + root }, ); self.count += 1; } - pub fn remove(&mut self, node_idx: usize) { - if let Some(node) = self.nodes.get(&node_idx) { + pub fn connect(&mut self, parent: usize, child: usize) { + if let Some(parent) = self.nodes.get_mut(&parent) { + parent.children.insert(child); + } + if let Some(child) = self.nodes.get_mut(&child) { + child.parents.insert(parent); + } + } + + fn remove_recursive(&mut self, node_idx: usize, to_delete: &mut FxHashSet) { + if let Some(node) = self.nodes.remove(&node_idx) { let children = node.children.clone(); let parents = node.parents.clone(); - for child in children { - if let Some(child) = self.nodes.get_mut(&child) { + for child_idx in children { + if let Some(child) = self.nodes.get_mut(&child_idx) { child.parents.remove(&node_idx); + if child.parents.is_empty() && !child.root { + to_delete.insert(child_idx); + self.remove_recursive(child_idx, to_delete) + } } } @@ -50,6 +70,12 @@ impl Graph { } } + pub fn remove(&mut self, node_idx: usize) -> FxHashSet { + let mut fx = Default::default(); + self.remove_recursive(node_idx, &mut fx); + fx + } + fn flood_invalidation(&mut self, node: usize) { if let Some(node) = self.nodes.get_mut(&node) { if node.invalidated { diff --git a/src/kind-query/src/lib.rs b/src/kind-query/src/lib.rs index bef0956e..b1817e60 100644 --- a/src/kind-query/src/lib.rs +++ b/src/kind-query/src/lib.rs @@ -2,32 +2,37 @@ //! module. It is useful both for LSPs, Watch, Repl //! and many other things. +mod graph; +mod names; +mod errors; + use std::path::PathBuf; use fxhash::FxHashMap; use graph::Graph; -mod graph; use kind_report::data::Diagnostic; use kind_tree::concrete; pub struct Resource { path: PathBuf, + hash: usize, concrete_tree: concrete::Module, /// Useful for LSP URIs - ext: T, + ext_info: T, } #[derive(Default)] pub struct Session { - /// Stores graph: Graph, - /// Useful for removing and adding resources + paths: FxHashMap, resources: FxHashMap>, } impl Session { - pub fn check() {} + pub fn check(&mut self, path: PathBuf) { + + } } diff --git a/src/kind-query/src/names.rs b/src/kind-query/src/names.rs new file mode 100644 index 00000000..b04ac895 --- /dev/null +++ b/src/kind-query/src/names.rs @@ -0,0 +1,37 @@ +use std::path::{PathBuf, Path}; + +use kind_report::data::Diagnostic; +use kind_tree::symbol::QualifiedIdent; + +use crate::errors::DriverError; + +const EXT: &str = "kind2"; + +/// Tries to accumulate on a buffer all of the +/// paths that exists (so we can just throw an +/// error about ambiguous resolution to the user) +pub(crate) fn accumulate_neighbour_paths( + ident: &QualifiedIdent, + raw_path: &Path, +) -> Result, Box> { + let mut canon_path = raw_path.to_path_buf(); + let mut dir_file_path = raw_path.to_path_buf(); + let dir_path = raw_path.to_path_buf(); + + canon_path.set_extension(EXT); + dir_file_path.push("_"); + dir_file_path.set_extension(EXT); + + if canon_path.exists() && dir_path.exists() && canon_path.is_file() && dir_path.is_dir() { + Err(Box::new(DriverError::MultiplePaths( + ident.clone(), + vec![canon_path, dir_path], + ))) + } else if canon_path.is_file() { + Ok(Some(canon_path)) + } else if dir_file_path.is_file() { + Ok(Some(dir_file_path)) + } else { + Ok(None) + } +} \ No newline at end of file diff --git a/src/kind-report/src/report.rs b/src/kind-report/src/report.rs index b8eaff7b..f218b8c1 100644 --- a/src/kind-report/src/report.rs +++ b/src/kind-report/src/report.rs @@ -4,14 +4,12 @@ // pretty printers are always a disaster to write. expect // that in the future i can rewrite it in a better way. -use std::collections::HashSet; - use std::fmt::{Display, Write}; use std::path::{Path, PathBuf}; use std::str; -use fxhash::FxHashMap; +use fxhash::{FxHashMap, FxHashSet}; use kind_span::{Pos, SyntaxCtxIndex}; use unicode_width::UnicodeWidthStr; use yansi::Paint; @@ -235,7 +233,7 @@ fn write_code_block<'a, T: Write + Sized>( writeln!(fmt, "{:>5} {}", "", paint_line(config.chars.vbar))?; - let mut lines_set = HashSet::new(); + let mut lines_set = FxHashSet::default(); let mut markers_by_line: FxHashMap> = FxHashMap::default(); diff --git a/src/kind-tree/src/concrete/expr.rs b/src/kind-tree/src/concrete/expr.rs index 49c93f05..48f7c590 100644 --- a/src/kind-tree/src/concrete/expr.rs +++ b/src/kind-tree/src/concrete/expr.rs @@ -300,20 +300,20 @@ impl Display for SttmKind { fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> { match self { SttmKind::Ask(name, block, next) => { - write!(f, "ask {} = {}; {}", name, block, next) + write!(f, "ask {} = {};\n {}", name, block, next) } SttmKind::Let(name, block, next) => { - write!(f, "let {} = {}; {}", name, block, next) + write!(f, "let {} = {};\n {}", name, block, next) } SttmKind::Expr(expr, next) => { - write!(f, "{};{}", expr, next) + write!(f, "{};\n{}", expr, next) } SttmKind::Return(ret) => { - write!(f, "return {}", ret) + write!(f, "return {}\n", ret) } SttmKind::RetExpr(ret) => { - write!(f, "{}", ret) + write!(f, "{}\n", ret) } } } @@ -343,7 +343,7 @@ impl Display for Case { if self.ignore_rest.is_some() { write!(f, " ..")?; } - write!(f, " => {}; ", self.value) + write!(f, " => {}", self.value) } } @@ -393,7 +393,7 @@ impl Display for Expr { fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> { use ExprKind::*; match &self.data { - Do(id, sttms) => write!(f, "do {} {{{}}}", id, sttms), + Do(id, sttms) => write!(f, "(do {} {{{}}})", id, sttms), All(_, _, _) => write!(f, "({})", self.traverse_pi_types()), Sigma(_, _, _) => write!(f, "({})", self.traverse_pi_types()), Lit(lit) => write!(f, "{}", lit), diff --git a/src/kind-tree/src/concrete/mod.rs b/src/kind-tree/src/concrete/mod.rs index 63715d9a..7fb4da1c 100644 --- a/src/kind-tree/src/concrete/mod.rs +++ b/src/kind-tree/src/concrete/mod.rs @@ -51,6 +51,12 @@ impl Telescope { } } +impl Telescope where T : Clone { + pub fn drop(self, num: usize) -> Telescope { + Telescope(self.0[num..].to_vec()) + } +} + /// A value of a attribute #[derive(Clone, Debug, Hash, PartialEq, Eq)] pub enum AttributeStyle { @@ -270,11 +276,12 @@ impl Display for TopLevel { write!(f, " {}", arg)?; } writeln!(f, " {{")?; + writeln!(f, " constructor {}", rec.constructor.to_str())?; for (name, docs, cons) in &rec.fields { for doc in docs { writeln!(f, " /// {}", doc)?; } - writeln!(f, " {}: {}, ", name, cons)?; + writeln!(f, " {} : {} ", name, cons)?; } writeln!(f, "}}\n") } diff --git a/src/kind-tree/src/symbol.rs b/src/kind-tree/src/symbol.rs index 1a9f823f..e0795f4b 100644 --- a/src/kind-tree/src/symbol.rs +++ b/src/kind-tree/src/symbol.rs @@ -137,6 +137,7 @@ impl Ident { new } + #[inline] pub fn to_str(&self) -> &str { &self.data.0 }