HigherOrderCO/Kind1
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind1.git synced 2024-08-15 19:30:41 +03:00
Code Issues Packages Projects Releases Wiki Activity

fix: bug fixes in erasure

Browse Source
This commit is contained in:
felipegchi 2022-11-18 08:52:27 -03:00
parent 56f5d88d4f
commit 58684b874b
17 changed files with 302 additions and 85 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
src/kind-cli/src/lib.rs
View File

@ -36,6 +36,12 @@ pub struct Cli {
#[arg(short, long)]
pub ascii: bool,
#[arg(short, long)]
entrypoint: Option<String>,
#[arg(short, long, value_name = "FILE")]
pub root: Option<PathBuf>,
#[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

9
src/kind-driver/src/lib.rs
View File

@ -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<desugare
let erased = erasure::erase_book(
&desugared_book,
session.diagnostic_sender.clone(),
HashSet::from_iter(vec!["Main".to_string()]),
FxHashSet::from_iter(vec!["Main".to_string()]),
)?;
Some(erased)
@ -63,7 +64,7 @@ pub fn erase_book(
erasure::erase_book(
&desugared_book,
session.diagnostic_sender.clone(),
HashSet::from_iter(entrypoint.to_owned()),
FxHashSet::from_iter(entrypoint.to_owned()),
)
}
@ -78,7 +79,7 @@ pub fn check_erasure_book(session: &mut Session, path: &PathBuf) -> Option<desug
erasure::erase_book(
&desugared_book,
session.diagnostic_sender.clone(),
HashSet::from_iter(vec!["Main".to_string()]),
FxHashSet::from_iter(vec!["Main".to_string()]),
)?;
Some(desugared_book)
}

42
src/kind-driver/src/resolution.rs
View File

@ -3,8 +3,8 @@
//! it returns a desugared book of all of the
//! depedencies.
use fxhash::FxHashSet;
use kind_pass::expand::uses::expand_uses;
use std::collections::HashSet;
use std::fs;
use std::path::{Path, PathBuf};
use std::rc::Rc;
@ -80,15 +80,15 @@ fn try_to_insert_new_name<'a>(
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<String> {
let mut public_names = HashSet::new();
) -> FxHashSet<String> {
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<Ident> = unbound
.iter()
.filter(|x| !x.used_by_sugar)
.map(|x| x.to_ident())
.collect();
if !res.is_empty() {

7
src/kind-driver/src/session.rs
View File

@ -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<PathBuf, HashSet<String>>,
pub public_names: FxHashSet<String>,
pub diagnostic_sender: Sender<Box<dyn Diagnostic>>,
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,

3
src/kind-parser/src/expr.rs
View File

@ -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,

2
src/kind-parser/src/top_level/type_decl.rs
View File

@ -16,6 +16,8 @@ impl<'a> Parser<'a> {
None
};
self.check_and_eat(Token::Semi);
Ok(Constructor {
name,
docs,

3
src/kind-pass/src/desugar/destruct.rs
View File

@ -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,

39
src/kind-pass/src/erasure/mod.rs
View File

@ -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<Range>, 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<Box<Expr>>,
) -> Vec<Box<Expr>> {
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)

10
src/kind-pass/src/unbound/mod.rs
View File

@ -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()))
}
}

105
src/kind-query/src/errors.rs Normal file
View File

@ -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<Ident>, Vec<String>),
MultiplePaths(QualifiedIdent, Vec<PathBuf>),
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::<Vec<String>>().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![],
},
}
}
}

44
src/kind-query/src/graph.rs
View File

@ -1,43 +1,63 @@
use std::collections::HashMap;
use fxhash::FxHashSet;
use fxhash::{FxHashSet, FxHashMap};
struct Node<T> {
data: T,
invalidated: bool,
children: FxHashSet<usize>,
parents: FxHashSet<usize>,
root: bool,
}
#[derive(Default)]
pub struct Graph<T> {
// Using a hashmap to make it easier to add or remove node.s
nodes: HashMap<usize, Node<T>>,
nodes: FxHashMap<usize, Node<T>>,
count: usize,
}
impl<T> Default for Graph<T> {
fn default() -> Self {
Self { nodes: Default::default(), count: Default::default() }
}
}
impl<T> Graph<T> {
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<usize>) {
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<T> Graph<T> {
}
}
pub fn remove(&mut self, node_idx: usize) -> FxHashSet<usize> {
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 {

15
src/kind-query/src/lib.rs
View File

@ -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<T> {
path: PathBuf,
hash: usize,
concrete_tree: concrete::Module,
/// Useful for LSP URIs
ext: T,
ext_info: T,
}
#[derive(Default)]
pub struct Session<T> {
/// Stores
graph: Graph<usize>,
/// Useful for removing and adding resources
paths: FxHashMap<String, usize>,
resources: FxHashMap<usize, Resource<T>>,
}
impl<T> Session<T> {
pub fn check() {}
pub fn check(&mut self, path: PathBuf) {
}
}

37
src/kind-query/src/names.rs Normal file
View File

@ -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<Option<PathBuf>, Box<dyn Diagnostic>> {
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)
}
}

6
src/kind-report/src/report.rs
View File

@ -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<usize, Vec<(Point, Point, &Marker)>> = FxHashMap::default();

14
src/kind-tree/src/concrete/expr.rs
View File

@ -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),

9
src/kind-tree/src/concrete/mod.rs
View File

@ -51,6 +51,12 @@ impl<T> Telescope<T> {
}
}
impl<T> Telescope<T> where T : Clone {
pub fn drop(self, num: usize) -> Telescope<T> {
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")
}

1
src/kind-tree/src/symbol.rs
View File

@ -137,6 +137,7 @@ impl Ident {
new
}
#[inline]
pub fn to_str(&self) -> &str {
&self.data.0
}