mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-11 08:45:32 +03:00
fix: fixed bugs with resolution and erasure
This commit is contained in:
parent
a68a8a90b2
commit
b17046aa9d
@ -206,7 +206,7 @@ fn codegen_all_expr(lhs_rule: bool, lhs: bool, num: &mut usize, quote: bool, exp
|
||||
span_to_num(expr.span),
|
||||
mk_u60(name.encode()),
|
||||
mk_u60(*idx as u64),
|
||||
mk_u60(*rdx as u64),
|
||||
mk_var(rdx.to_str()),
|
||||
codegen_all_expr(lhs_rule, lhs, num, quote, expr),
|
||||
],
|
||||
),
|
||||
|
@ -13,9 +13,13 @@ pub struct Context(pub Vec<Entry>);
|
||||
|
||||
macro_rules! match_opt {
|
||||
($expr:expr, $pat:pat => $end:expr) => {
|
||||
{
|
||||
match $expr {
|
||||
$pat => Ok($end),
|
||||
_ => Err("Error while matching opt".to_string()),
|
||||
_ => {
|
||||
Err("Error while matching opt".to_string())
|
||||
},
|
||||
}
|
||||
}
|
||||
};
|
||||
}
|
||||
@ -57,7 +61,7 @@ fn parse_name(term: &Term) -> Result<String, String> {
|
||||
match term {
|
||||
Term::Num { numb } => Ok(Ident::decode(*numb)),
|
||||
Term::Ctr { name, args: _ } => Ok(name.to_string()),
|
||||
_ => Err("Error while matching opt".to_string()),
|
||||
_ => Err("Error while matching ident".to_string()),
|
||||
}
|
||||
}
|
||||
|
||||
@ -65,7 +69,7 @@ fn parse_qualified(term: &Term) -> Result<QualifiedIdent, String> {
|
||||
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()),
|
||||
_ => Err("Error while matching qualified".to_string()),
|
||||
}
|
||||
}
|
||||
|
||||
@ -102,7 +106,7 @@ fn parse_all_expr(names: im::HashMap<String, String>, term: &Term) -> Result<Box
|
||||
parse_orig(&args[0])?,
|
||||
Ident::generate(&parse_name(&args[1])?),
|
||||
parse_num(&args[2])? as usize,
|
||||
parse_num(&args[3])? as usize,
|
||||
Ident::new(parse_name(&args[1])?, parse_orig(&args[0])?),
|
||||
parse_all_expr(names, &args[4])?,
|
||||
)),
|
||||
"Kind.Quoted.app" => Ok(Expr::app(
|
||||
@ -122,10 +126,10 @@ fn parse_all_expr(names: im::HashMap<String, String>, term: &Term) -> Result<Box
|
||||
}
|
||||
res
|
||||
})),
|
||||
"Kind.Quoted.fun" => Ok(Expr::fun(parse_orig(&args[0])?, parse_qualified(&args[1])?, {
|
||||
"Kind.Quoted.fun" => Ok(Expr::fun(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
|
||||
})),
|
||||
|
@ -141,6 +141,7 @@ pub fn compile_in_session<T>(
|
||||
if diagnostics.is_empty() {
|
||||
render_to_stderr(&render_config, &session, &Log::Checked(start.elapsed()));
|
||||
eprintln!();
|
||||
res
|
||||
} else {
|
||||
render_to_stderr(&render_config, &session, &Log::Failed(start.elapsed()));
|
||||
eprintln!();
|
||||
@ -148,8 +149,8 @@ pub fn compile_in_session<T>(
|
||||
let diagnostic: Diagnostic = (&diagnostic).into();
|
||||
render_to_stderr(&render_config, &session, &diagnostic)
|
||||
}
|
||||
None
|
||||
}
|
||||
res
|
||||
}
|
||||
|
||||
fn main() {
|
||||
|
@ -152,7 +152,7 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
|
||||
let spine: Vec<Ident>;
|
||||
|
||||
if cons.typ.is_none() {
|
||||
irrelev = sum.indices.extend(&cons.args).map(|x| x.hidden).to_vec();
|
||||
irrelev = sum.indices.extend(&cons.args).map(|x| x.erased).to_vec();
|
||||
spine_params = sum
|
||||
.parameters
|
||||
.extend(&sum.indices)
|
||||
@ -161,7 +161,7 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry {
|
||||
.to_vec();
|
||||
spine = sum.indices.extend(&cons.args).map(|x| x.name.with_name(|f| format!("{}_", f))).to_vec();
|
||||
} else {
|
||||
irrelev = cons.args.map(|x| x.hidden).to_vec();
|
||||
irrelev = cons.args.map(|x| x.erased).to_vec();
|
||||
spine_params = sum.parameters.extend(&cons.args).map(|x| x.name.with_name(|f| format!("{}_", f))).to_vec();
|
||||
spine = cons.args.map(|x| x.name.with_name(|f| format!("{}_", f))).to_vec();
|
||||
}
|
||||
|
@ -152,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
|
||||
@ -165,7 +165,7 @@ fn parse_and_store_book_by_path<'a>(
|
||||
path: &PathBuf,
|
||||
book: &'a mut Book,
|
||||
) -> bool {
|
||||
if session.loaded_paths_map.contains_key(path) {
|
||||
if session.loaded_paths_map.contains_key(&fs::canonicalize(path).unwrap()) {
|
||||
return false;
|
||||
}
|
||||
|
||||
@ -181,13 +181,13 @@ fn parse_and_store_book_by_path<'a>(
|
||||
};
|
||||
|
||||
let ctx_id = session.book_counter;
|
||||
session.add_path(Rc::new(path.to_path_buf()), input.clone());
|
||||
session.add_path(Rc::new(fs::canonicalize(path).unwrap()), input.clone());
|
||||
|
||||
let (mut module, mut failed) =
|
||||
kind_parser::parse_book(session.diagnostic_sender.clone(), ctx_id, &input);
|
||||
|
||||
let (unbound_vars, unbound_top_level) =
|
||||
unbound::get_module_unbound(session.diagnostic_sender.clone(), &mut module);
|
||||
unbound::get_module_unbound(session.diagnostic_sender.clone(), &mut module, false);
|
||||
|
||||
for idents in unbound_vars.values() {
|
||||
unbound_variable(session, book, idents);
|
||||
@ -195,10 +195,8 @@ fn parse_and_store_book_by_path<'a>(
|
||||
}
|
||||
|
||||
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);
|
||||
}
|
||||
}
|
||||
|
||||
expand_uses(&mut module, session.diagnostic_sender.clone());
|
||||
|
||||
@ -223,7 +221,17 @@ 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 failed = parse_and_store_book_by_path(session, path, &mut book);
|
||||
let mut failed = parse_and_store_book_by_path(session, path, &mut book);
|
||||
|
||||
let (_, unbound_tops) = unbound::get_book_unbound(session.diagnostic_sender.clone(), &mut book, true);
|
||||
|
||||
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() {
|
||||
unbound_variable(session, &book, &res);
|
||||
failed = true;
|
||||
}
|
||||
}
|
||||
|
||||
if failed {
|
||||
None
|
||||
|
@ -95,13 +95,13 @@ impl<'a> Parser<'a> {
|
||||
self.advance(); // '##'
|
||||
let name = self.parse_id()?;
|
||||
self.eat_variant(Token::Slash)?;
|
||||
let redx = self.parse_num_lit()?;
|
||||
let redx = self.parse_id()?;
|
||||
let expr = self.parse_expr(false)?;
|
||||
let range = start.mix(expr.range);
|
||||
Ok(Box::new(Expr {
|
||||
data: ExprKind::Subst(Substitution {
|
||||
name,
|
||||
redx: redx as usize,
|
||||
redx,
|
||||
indx: 0,
|
||||
expr,
|
||||
}),
|
||||
@ -311,7 +311,7 @@ impl<'a> Parser<'a> {
|
||||
let range = self.range();
|
||||
self.advance(); // '('
|
||||
let mut expr = self.parse_expr(true)?;
|
||||
if self.get().same_variant(&Token::Colon) {
|
||||
if self.get().same_variant(&Token::ColonColon) {
|
||||
self.advance(); // ':'
|
||||
let typ = self.parse_expr(false)?;
|
||||
let range = range.mix(self.range());
|
||||
|
@ -170,7 +170,13 @@ impl<'a> Lexer<'a> {
|
||||
_ => (Token::Slash, self.mk_range(start)),
|
||||
}
|
||||
}
|
||||
':' => self.single_token(Token::Colon, start),
|
||||
':' => {
|
||||
self.next_char();
|
||||
match self.peekable.peek() {
|
||||
Some(':') => self.single_token(Token::ColonColon, start),
|
||||
_ => (Token::Colon, self.mk_range(start)),
|
||||
}
|
||||
}
|
||||
';' => self.single_token(Token::Semi, start),
|
||||
'$' => self.single_token(Token::Dollar, start),
|
||||
',' => self.single_token(Token::Comma, start),
|
||||
|
@ -21,6 +21,7 @@ pub enum Token {
|
||||
DotDot, // ..
|
||||
Dot, // .
|
||||
Tilde, // ~
|
||||
ColonColon, // ::
|
||||
|
||||
Help(String),
|
||||
LowerId(String),
|
||||
|
@ -33,7 +33,7 @@ impl<'a> DesugarState<'a> {
|
||||
range,
|
||||
sub.name.clone(),
|
||||
sub.indx,
|
||||
sub.redx,
|
||||
sub.redx.clone(),
|
||||
self.desugar_expr(&sub.expr),
|
||||
)
|
||||
}
|
||||
|
@ -255,6 +255,7 @@ impl<'a> DesugarState<'a> {
|
||||
pub fn desugar_pat(&mut self, pat: &concrete::pat::Pat) -> Box<desugared::Expr> {
|
||||
match &pat.data {
|
||||
concrete::pat::PatKind::App(head, spine) => {
|
||||
// TODO: Fix lol
|
||||
let entry = self
|
||||
.old_book
|
||||
.count
|
||||
@ -282,7 +283,6 @@ impl<'a> DesugarState<'a> {
|
||||
}
|
||||
}
|
||||
} else if entry.arguments.len() != spine.len() {
|
||||
println!("Ata {} {:?}", head, spine.iter().map(|x| x.to_string()).collect::<Vec<String>>());
|
||||
self.send_err(PassError::IncorrectArity(
|
||||
head.range,
|
||||
spine.iter().map(|x| x.range).collect(),
|
||||
|
@ -9,6 +9,8 @@
|
||||
// Not the best algorithm... it should not be trusted for
|
||||
// dead code elimination.
|
||||
|
||||
// TODO: Cannot pattern match on erased
|
||||
|
||||
use std::sync::mpsc::Sender;
|
||||
|
||||
use fxhash::{FxHashMap, FxHashSet};
|
||||
@ -16,7 +18,10 @@ use fxhash::{FxHashMap, FxHashSet};
|
||||
use kind_report::data::DiagnosticFrame;
|
||||
|
||||
use kind_span::Range;
|
||||
use kind_tree::{desugared::{Book, Entry, Expr, ExprKind, Rule, self}, symbol::{QualifiedIdent}};
|
||||
use kind_tree::{
|
||||
desugared::{self, Book, Entry, Expr, ExprKind, Rule},
|
||||
symbol::QualifiedIdent,
|
||||
};
|
||||
|
||||
use crate::errors::PassError;
|
||||
|
||||
@ -37,11 +42,7 @@ pub struct ErasureState<'a> {
|
||||
failed: bool,
|
||||
}
|
||||
|
||||
pub fn erase_book(
|
||||
book: &Book,
|
||||
errs: Sender<DiagnosticFrame>,
|
||||
entrypoint: FxHashSet<String>,
|
||||
) -> Option<Book> {
|
||||
pub fn erase_book(book: &Book, errs: Sender<DiagnosticFrame>, entrypoint: FxHashSet<String>) -> Option<Book> {
|
||||
let mut state = ErasureState {
|
||||
errs,
|
||||
book,
|
||||
@ -60,9 +61,7 @@ pub fn erase_book(
|
||||
|
||||
for name in entrypoint {
|
||||
let count = state.holes.len();
|
||||
state
|
||||
.names
|
||||
.insert(name.to_string(), (None, Relevance::Hole(count)));
|
||||
state.names.insert(name.to_string(), (None, Relevance::Hole(count)));
|
||||
state.holes.push(Some(Relevance::Relevant));
|
||||
}
|
||||
|
||||
@ -102,15 +101,8 @@ impl<'a> ErasureState<'a> {
|
||||
local_relevance
|
||||
}
|
||||
|
||||
pub fn err_irrelevant(
|
||||
&mut self,
|
||||
declared_val: Option<Range>,
|
||||
used: Range,
|
||||
declared_ty: Option<Range>,
|
||||
) {
|
||||
self.errs
|
||||
.send(PassError::CannotUseIrrelevant(declared_val, used, declared_ty).into())
|
||||
.unwrap();
|
||||
pub fn err_irrelevant(&mut self, declared_val: Option<Range>, used: Range, declared_ty: Option<Range>) {
|
||||
self.errs.send(PassError::CannotUseIrrelevant(declared_val, used, declared_ty).into()).unwrap();
|
||||
self.failed = true;
|
||||
}
|
||||
|
||||
@ -131,83 +123,38 @@ impl<'a> ErasureState<'a> {
|
||||
}
|
||||
}
|
||||
|
||||
pub fn unify_hole(
|
||||
&mut self,
|
||||
range: Range,
|
||||
hole: (Option<Range>, usize),
|
||||
right: (Option<Range>, Relevance),
|
||||
visited: &mut FxHashSet<usize>,
|
||||
inverted: bool,
|
||||
relevance_unify: bool,
|
||||
) -> bool {
|
||||
match (self.holes[hole.1], right.1) {
|
||||
(Some(Relevance::Hole(n)), t) => {
|
||||
visited.insert(n);
|
||||
if visited.contains(&n) {
|
||||
self.holes[hole.1] = Some(t);
|
||||
true
|
||||
} else {
|
||||
self.unify_hole(
|
||||
range,
|
||||
(hole.0, n),
|
||||
right,
|
||||
visited,
|
||||
inverted,
|
||||
relevance_unify,
|
||||
)
|
||||
}
|
||||
}
|
||||
(_, Relevance::Relevant) => true,
|
||||
(Some(l), _) => {
|
||||
if inverted {
|
||||
self.unify_loop(range, right, (hole.0, l), visited, relevance_unify)
|
||||
} else {
|
||||
self.unify_loop(range, (hole.0, l), right, visited, relevance_unify)
|
||||
}
|
||||
}
|
||||
(None, r) => {
|
||||
self.holes[hole.1] = Some(r);
|
||||
true
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
pub fn unify_loop(
|
||||
&mut self,
|
||||
range: Range,
|
||||
left: (Option<Range>, Relevance),
|
||||
right: (Option<Range>, Relevance),
|
||||
visited: &mut FxHashSet<usize>,
|
||||
relevance_unify: bool,
|
||||
) -> bool {
|
||||
pub fn unify_loop(&mut self, range: Range, left: (Option<Range>, Relevance), right: (Option<Range>, Relevance), visited: &mut FxHashSet<usize>, relevance_unify: bool) -> bool {
|
||||
match (left.1, right.1) {
|
||||
(_, Relevance::Hole(hole)) => {
|
||||
self.unify_hole(range, (right.0, hole), left, visited, true, relevance_unify)
|
||||
(Relevance::Hole(hole), t) => match (self.holes[hole], t) {
|
||||
(Some(res), _) if !visited.contains(&hole) => {
|
||||
visited.insert(hole);
|
||||
self.unify_loop(range, (left.0, res), right, visited, 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)
|
||||
| (Relevance::Relevant, Relevance::Relevant) => true,
|
||||
|
||||
(None, Relevance::Irrelevant) => {
|
||||
self.holes[hole] = Some(t);
|
||||
true
|
||||
}
|
||||
(_, _) => true,
|
||||
},
|
||||
(Relevance::Relevant, Relevance::Hole(hole)) => match self.holes[hole] {
|
||||
Some(res) if !visited.contains(&hole) => {
|
||||
visited.insert(hole);
|
||||
self.unify_loop(range, left, (right.0, res), visited, relevance_unify)
|
||||
}
|
||||
_ => {
|
||||
self.holes[hole] = Some(Relevance::Relevant);
|
||||
true
|
||||
}
|
||||
},
|
||||
(Relevance::Irrelevant, Relevance::Hole(_))
|
||||
| (Relevance::Relevant, Relevance::Relevant)
|
||||
| (Relevance::Irrelevant, Relevance::Irrelevant)
|
||||
| (Relevance::Irrelevant, Relevance::Relevant) => true,
|
||||
(Relevance::Relevant, Relevance::Irrelevant) => false,
|
||||
}
|
||||
}
|
||||
|
||||
pub fn unify(
|
||||
&mut self,
|
||||
range: Range,
|
||||
left: (Option<Range>, Relevance),
|
||||
right: (Option<Range>, Relevance),
|
||||
relevance_unify: bool,
|
||||
) -> bool {
|
||||
pub fn unify(&mut self, range: Range, left: (Option<Range>, Relevance), right: (Option<Range>, Relevance), relevance_unify: bool) -> bool {
|
||||
self.unify_loop(range, left, right, &mut Default::default(), relevance_unify)
|
||||
}
|
||||
|
||||
@ -224,15 +171,7 @@ 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 on.1 == Relevance::Irrelevant {
|
||||
on
|
||||
} else if arg.erased {
|
||||
(Some(arg.span), Relevance::Irrelevant)
|
||||
} else {
|
||||
(Some(arg.span), Relevance::Relevant)
|
||||
}
|
||||
});
|
||||
let irrelevances = erased.map(|arg| if arg.erased { (Some(arg.span), Relevance::Irrelevant) } else { on });
|
||||
|
||||
spine
|
||||
.iter()
|
||||
@ -340,30 +279,28 @@ impl<'a> ErasureState<'a> {
|
||||
}
|
||||
App(head, spine) => {
|
||||
let head = self.erase_expr(on, head);
|
||||
let spine = spine.iter().map(|x| {
|
||||
let spine = spine
|
||||
.iter()
|
||||
.map(|x| {
|
||||
let on = if x.erased {
|
||||
(x.data.span.to_range(), Relevance::Irrelevant)
|
||||
} else {
|
||||
on.clone()
|
||||
(x.data.span.to_range(), Relevance::Relevant)
|
||||
};
|
||||
desugared::AppBinding {
|
||||
data: self.erase_expr(&on, &x.data),
|
||||
erased: x.erased
|
||||
erased: x.erased,
|
||||
}
|
||||
}).filter(|x| !x.erased).collect();
|
||||
})
|
||||
.filter(|x| !x.erased)
|
||||
.collect();
|
||||
Box::new(Expr {
|
||||
span: expr.span,
|
||||
data: ExprKind::App(head, spine),
|
||||
})
|
||||
}
|
||||
Fun(head, spine) => {
|
||||
let args = self
|
||||
.book
|
||||
.entrs
|
||||
.get(head.to_string().as_str())
|
||||
.unwrap()
|
||||
.args
|
||||
.iter();
|
||||
let args = self.book.entrs.get(head.to_string().as_str()).unwrap().args.iter();
|
||||
|
||||
let fun = match self.names.get(&head.to_string()) {
|
||||
Some(res) => *res,
|
||||
@ -378,13 +315,11 @@ impl<'a> ErasureState<'a> {
|
||||
.iter()
|
||||
.zip(args)
|
||||
.map(|(expr, arg)| {
|
||||
(
|
||||
self.erase_expr(
|
||||
&(Some(arg.span), erasure_to_relevance(arg.erased)),
|
||||
expr,
|
||||
),
|
||||
arg,
|
||||
)
|
||||
if arg.erased {
|
||||
(self.erase_expr(&(Some(arg.span), Relevance::Irrelevant), expr), arg)
|
||||
} else {
|
||||
(self.erase_expr(on, expr), arg)
|
||||
}
|
||||
})
|
||||
.filter(|(_, arg)| !arg.erased);
|
||||
|
||||
@ -394,13 +329,7 @@ impl<'a> ErasureState<'a> {
|
||||
})
|
||||
}
|
||||
Ctr(head, spine) => {
|
||||
let args = self
|
||||
.book
|
||||
.entrs
|
||||
.get(head.to_string().as_str())
|
||||
.unwrap()
|
||||
.args
|
||||
.iter();
|
||||
let args = self.book.entrs.get(head.to_string().as_str()).unwrap().args.iter();
|
||||
|
||||
let fun = match self.names.get(&head.to_string()) {
|
||||
Some(res) => *res,
|
||||
@ -415,13 +344,11 @@ impl<'a> ErasureState<'a> {
|
||||
.iter()
|
||||
.zip(args)
|
||||
.map(|(expr, arg)| {
|
||||
(
|
||||
self.erase_expr(
|
||||
&(Some(arg.span), erasure_to_relevance(arg.erased)),
|
||||
expr,
|
||||
),
|
||||
arg,
|
||||
)
|
||||
if arg.erased {
|
||||
(self.erase_expr(&(Some(arg.span), Relevance::Irrelevant), expr), arg)
|
||||
} else {
|
||||
(self.erase_expr(on, expr), arg)
|
||||
}
|
||||
})
|
||||
.filter(|(_, arg)| !arg.erased);
|
||||
|
||||
@ -443,19 +370,13 @@ impl<'a> ErasureState<'a> {
|
||||
}
|
||||
}
|
||||
|
||||
pub fn erase_rule(
|
||||
&mut self,
|
||||
place: &(Option<Range>, Relevance),
|
||||
args: Vec<(Range, bool)>,
|
||||
rule: &Rule,
|
||||
) -> Rule {
|
||||
pub fn erase_rule(&mut self, place: &(Option<Range>, Relevance), args: Vec<(Range, bool)>, rule: &Rule) -> Rule {
|
||||
let ctx = self.ctx.clone();
|
||||
|
||||
let new_pats : Vec<_> = args.iter()
|
||||
let new_pats: Vec<_> = args
|
||||
.iter()
|
||||
.zip(rule.pats.iter())
|
||||
.map(|((range, erased), expr)| {
|
||||
(erased, self.erase_pat((Some(*range), erasure_to_relevance(*erased)), expr))
|
||||
})
|
||||
.map(|((range, erased), expr)| (erased, self.erase_pat((Some(*range), erasure_to_relevance(*erased)), expr)))
|
||||
.filter(|(erased, _)| !*erased)
|
||||
.map(|res| res.1)
|
||||
.collect();
|
||||
@ -480,15 +401,12 @@ impl<'a> ErasureState<'a> {
|
||||
};
|
||||
|
||||
let args: Vec<(Range, bool)> = entry.args.iter().map(|x| (x.span, x.erased)).collect();
|
||||
let rules = entry
|
||||
.rules
|
||||
.iter()
|
||||
.map(|rule| self.erase_rule(&place, args.clone(), rule));
|
||||
let rules = entry.rules.iter().map(|rule| self.erase_rule(&place, args.clone(), rule)).collect::<Vec<Rule>>();
|
||||
Box::new(Entry {
|
||||
name: entry.name.clone(),
|
||||
args: entry.args.clone(),
|
||||
typ: entry.typ.clone(),
|
||||
rules: rules.collect(),
|
||||
rules,
|
||||
attrs: entry.attrs.clone(),
|
||||
span: entry.span,
|
||||
})
|
||||
|
@ -30,15 +30,17 @@ pub struct UnboundCollector {
|
||||
pub context_vars: Vec<(Range, String)>,
|
||||
pub unbound_top_level: FxHashMap<String, Vec<QualifiedIdent>>,
|
||||
pub unbound: FxHashMap<String, Vec<Ident>>,
|
||||
pub emit_errs: bool
|
||||
}
|
||||
|
||||
impl UnboundCollector {
|
||||
pub fn new(diagnostic_sender: Sender<DiagnosticFrame>) -> UnboundCollector {
|
||||
pub fn new(diagnostic_sender: Sender<DiagnosticFrame>, emit_errs: bool) -> UnboundCollector {
|
||||
Self {
|
||||
errors: diagnostic_sender,
|
||||
context_vars: Default::default(),
|
||||
unbound_top_level: Default::default(),
|
||||
unbound: Default::default(),
|
||||
emit_errs
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -46,11 +48,12 @@ impl UnboundCollector {
|
||||
pub fn get_module_unbound(
|
||||
diagnostic_sender: Sender<DiagnosticFrame>,
|
||||
module: &mut Module,
|
||||
emit_errs: bool,
|
||||
) -> (
|
||||
FxHashMap<String, Vec<Ident>>,
|
||||
FxHashMap<String, Vec<QualifiedIdent>>,
|
||||
) {
|
||||
let mut state = UnboundCollector::new(diagnostic_sender);
|
||||
let mut state = UnboundCollector::new(diagnostic_sender, emit_errs);
|
||||
state.visit_module(module);
|
||||
(state.unbound, state.unbound_top_level)
|
||||
}
|
||||
@ -58,11 +61,12 @@ pub fn get_module_unbound(
|
||||
pub fn get_book_unbound(
|
||||
diagnostic_sender: Sender<DiagnosticFrame>,
|
||||
book: &mut Book,
|
||||
emit_errs: bool,
|
||||
) -> (
|
||||
FxHashMap<String, Vec<Ident>>,
|
||||
FxHashMap<String, Vec<QualifiedIdent>>,
|
||||
) {
|
||||
let mut state = UnboundCollector::new(diagnostic_sender);
|
||||
let mut state = UnboundCollector::new(diagnostic_sender, emit_errs);
|
||||
state.visit_book(book);
|
||||
(state.unbound, state.unbound_top_level)
|
||||
}
|
||||
@ -100,9 +104,11 @@ impl Visitor for UnboundCollector {
|
||||
.iter()
|
||||
.find(|x| x.1 == ident.0.data.to_string())
|
||||
{
|
||||
if self.emit_errs {
|
||||
self.errors
|
||||
.send(PassError::RepeatedVariable(fst.0, ident.0.range).into())
|
||||
.unwrap()
|
||||
}
|
||||
} else {
|
||||
self.context_vars.push((ident.0.range, ident.0.to_string()))
|
||||
}
|
||||
@ -120,9 +126,11 @@ impl Visitor for UnboundCollector {
|
||||
.find(|x| x.1 == argument.name.to_string());
|
||||
|
||||
if let Some(fst) = res {
|
||||
if self.emit_errs {
|
||||
self.errors
|
||||
.send(PassError::RepeatedVariable(fst.0, argument.name.range).into())
|
||||
.unwrap()
|
||||
}
|
||||
} else {
|
||||
self.context_vars
|
||||
.push((argument.name.range, argument.name.to_string()))
|
||||
@ -412,6 +420,7 @@ impl Visitor for UnboundCollector {
|
||||
}
|
||||
ExprKind::Subst(subst) => {
|
||||
self.visit_ident(&mut subst.name);
|
||||
self.visit_ident(&mut subst.redx);
|
||||
|
||||
if let Some(pos) = self
|
||||
.context_vars
|
||||
|
@ -74,7 +74,7 @@ pub struct Match {
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
pub struct Substitution {
|
||||
pub name: Ident,
|
||||
pub redx: usize,
|
||||
pub redx: Ident,
|
||||
pub indx: usize,
|
||||
pub expr: Box<Expr>,
|
||||
}
|
||||
|
@ -42,7 +42,7 @@ pub enum ExprKind {
|
||||
/// Type ascription (x : y)
|
||||
Ann(Box<Expr>, Box<Expr>),
|
||||
/// Substitution
|
||||
Sub(Ident, usize, usize, Box<Expr>),
|
||||
Sub(Ident, usize, Ident, Box<Expr>),
|
||||
/// Type Literal
|
||||
Typ,
|
||||
/// Primitive numeric types
|
||||
@ -91,7 +91,7 @@ impl Expr {
|
||||
})
|
||||
}
|
||||
|
||||
pub fn sub(range: Range, ident: Ident, idx: usize, rdx: usize, body: Box<Expr>) -> Box<Expr> {
|
||||
pub fn sub(range: Range, ident: Ident, idx: usize, rdx: Ident, body: Box<Expr>) -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
span: Span::Locatable(range),
|
||||
data: ExprKind::Sub(ident, idx, rdx, body),
|
||||
@ -337,7 +337,7 @@ impl Display for Expr {
|
||||
Var(name) => write!(f, "{}", name),
|
||||
Lambda(binder, body, false) => write!(f, "({} => {})", binder, body),
|
||||
Lambda(binder, body, true) => write!(f, "({{{}}} => {})", binder, body),
|
||||
Sub(name, _, redx, expr) => write!(f, "({} ## {}/{})", expr, name, redx),
|
||||
Sub(name, _, redx, expr) => write!(f, "(## {}/{} {})",name, redx, expr),
|
||||
App(head, spine) => write!(
|
||||
f,
|
||||
"({}{})",
|
||||
|
Loading…
Reference in New Issue
Block a user