mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-11 08:45:32 +03:00
fix: some problems with name resolution
This commit is contained in:
parent
9714dad33c
commit
2f14cc1267
@ -219,11 +219,15 @@ pub fn run_cli(config: Cli) {
|
||||
res
|
||||
});
|
||||
}
|
||||
Command::Watch { file: _ } => {
|
||||
todo!()
|
||||
},
|
||||
Command::Repl => {
|
||||
todo!()
|
||||
},
|
||||
Command::ToKDL {
|
||||
file: _,
|
||||
namespace: _,
|
||||
} => todo!(),
|
||||
Command::Watch { file: _ } => todo!(),
|
||||
Command::Repl => todo!(),
|
||||
}
|
||||
}
|
||||
|
@ -1,10 +1,7 @@
|
||||
type Nat {
|
||||
succ (pred: Nat)
|
||||
zero
|
||||
succ
|
||||
}
|
||||
|
||||
type Vec (t: Type) ~ (n: Nat) {
|
||||
cons <size: Nat> (x: t) (xs: Vec t size) : Vec t (Nat.succ size)
|
||||
nil : Vec t Nat.zero
|
||||
}
|
||||
|
||||
Nat.zero : U60
|
||||
Nat.zero = 2
|
3
src/kind-derive/src/record.rs
Normal file
3
src/kind-derive/src/record.rs
Normal file
@ -0,0 +1,3 @@
|
||||
//! Derives getters and setters for record
|
||||
//! types.
|
||||
|
@ -43,6 +43,8 @@ pub fn to_book(session: &mut Session, path: &PathBuf) -> Option<concrete::Book>
|
||||
|
||||
expand::expand_book(&mut concrete_book);
|
||||
|
||||
println!("{}", concrete_book);
|
||||
|
||||
let failed = resolution::check_unbound_top_level(session, &mut concrete_book);
|
||||
|
||||
if failed {
|
||||
|
@ -249,7 +249,7 @@ pub fn check_unbound_top_level(session: &mut Session, book: &mut Book) -> bool {
|
||||
unbound::get_book_unbound(session.diagnostic_sender.clone(), book, true);
|
||||
|
||||
for (_, unbound) in unbound_tops {
|
||||
let res: Vec<Ident> = unbound.iter().map(|x| x.to_ident()).collect();
|
||||
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;
|
||||
|
@ -492,16 +492,8 @@ impl<'a> Parser<'a> {
|
||||
range,
|
||||
});
|
||||
}
|
||||
if self.check_and_eat(Token::Colon) {
|
||||
let expr = self.parse_expr(false)?;
|
||||
Ok(Box::new(Expr {
|
||||
range: head.range.mix(expr.range),
|
||||
data: ExprKind::Ann(head, expr),
|
||||
}))
|
||||
} else {
|
||||
Ok(head)
|
||||
}
|
||||
}
|
||||
|
||||
pub fn parse_ask(&mut self) -> Result<Box<Sttm>, SyntaxError> {
|
||||
let start = self.range();
|
||||
|
@ -295,7 +295,9 @@ impl<'a> Parser<'a> {
|
||||
self.advance();
|
||||
self.errs.send(err.into()).unwrap();
|
||||
self.failed = true;
|
||||
while !self.is_top_level_start() && !self.get().same_variant(&Token::Eof) && !self.is_linebreak() {
|
||||
while (!self.is_top_level_start() || !self.is_linebreak())
|
||||
&& !self.get().same_variant(&Token::Eof)
|
||||
{
|
||||
self.advance();
|
||||
}
|
||||
}
|
||||
|
@ -150,10 +150,11 @@ impl<'a> ErasureState<'a> {
|
||||
visited.insert(hole);
|
||||
self.unify_loop(range, (left.0, res), right, visited, relevance_unify)
|
||||
}
|
||||
(None, Relevance::Irrelevant) => {
|
||||
self.holes[hole] = Some(t);
|
||||
true
|
||||
}
|
||||
|
||||
// TODO: It should unify iff we want functions that are considered
|
||||
// "erased" in the sense that we can just remove them from the runtime and it'll
|
||||
// be fine.
|
||||
(None, Relevance::Irrelevant) => false,
|
||||
(_, _) => true,
|
||||
},
|
||||
(Relevance::Relevant, Relevance::Hole(hole)) => match self.holes[hole] {
|
||||
@ -228,6 +229,15 @@ impl<'a> ErasureState<'a> {
|
||||
self.ctx.insert(name.to_string(), (name.range, on));
|
||||
Box::new(pat.clone())
|
||||
}
|
||||
Fun(name, spine) | Ctr(name, spine) if on.1 == Relevance::Irrelevant => {
|
||||
let range = pat.span.to_range().unwrap_or_else(|| name.range.clone());
|
||||
self.errs
|
||||
.send(PassError::CannotPatternMatchOnErased(range).into())
|
||||
.unwrap();
|
||||
self.failed = true;
|
||||
self.erase_pat_spine(on, &name, spine);
|
||||
desugared::Expr::err(range)
|
||||
}
|
||||
Fun(name, spine) => {
|
||||
let spine = self.erase_pat_spine(on, &name, spine);
|
||||
Box::new(Expr {
|
||||
|
@ -31,6 +31,7 @@ pub enum PassError {
|
||||
ShouldBeAParameter(Span, Range),
|
||||
NoFieldCoverage(Range, Vec<String>),
|
||||
DuplicatedConstructor(Range, Range),
|
||||
CannotPatternMatchOnErased(Range),
|
||||
}
|
||||
|
||||
// TODO: A way to build an error message with methods
|
||||
@ -89,6 +90,20 @@ impl From<PassError> for DiagnosticFrame {
|
||||
main: true,
|
||||
}],
|
||||
},
|
||||
PassError::CannotPatternMatchOnErased(place) => DiagnosticFrame {
|
||||
code: 223,
|
||||
severity: Severity::Error,
|
||||
title: "Cannot pattern match on erased arguments.".to_string(),
|
||||
subtitles: vec![],
|
||||
hints: vec![],
|
||||
positions: vec![Marker {
|
||||
position: place,
|
||||
color: Color::Fst,
|
||||
text: "Here!".to_string(),
|
||||
no_code: false,
|
||||
main: true,
|
||||
}],
|
||||
},
|
||||
PassError::RulesWithInconsistentArity(arities) => DiagnosticFrame {
|
||||
code: 201,
|
||||
severity: Severity::Error,
|
||||
|
@ -268,7 +268,7 @@ impl Visitor for UnboundCollector {
|
||||
fn visit_destruct(&mut self, destruct: &mut Destruct) {
|
||||
match destruct {
|
||||
Destruct::Destruct(range, ty, bindings, _) => {
|
||||
self.visit_qualified_ident(QualifiedIdent::add_segment(ty, "open").to_sugar());
|
||||
self.visit_qualified_ident(&mut QualifiedIdent::add_segment(ty, "open").to_sugar().to_generated());
|
||||
self.visit_range(range);
|
||||
self.visit_qualified_ident(ty);
|
||||
for bind in bindings {
|
||||
|
8
src/kind-query/Cargo.toml
Normal file
8
src/kind-query/Cargo.toml
Normal file
@ -0,0 +1,8 @@
|
||||
[package]
|
||||
name = "kind-query"
|
||||
version = "0.1.0"
|
||||
edition = "2021"
|
||||
|
||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||
|
||||
[dependencies]
|
3
src/kind-query/src/lib.rs
Normal file
3
src/kind-query/src/lib.rs
Normal file
@ -0,0 +1,3 @@
|
||||
fn main() {
|
||||
println!("Hello, world!");
|
||||
}
|
@ -347,7 +347,7 @@ impl Display for Expr {
|
||||
}
|
||||
}
|
||||
Let(name, expr, body) => write!(f, "(let {} = {}; {})", name, expr, body),
|
||||
Ann(expr, typ) => write!(f, "({} : {})", expr, typ),
|
||||
Ann(expr, typ) => write!(f, "({} :: {})", expr, typ),
|
||||
Binary(op, expr, typ) => write!(f, "({} {} {})", op, expr, typ),
|
||||
Hole(_) => write!(f, "_"),
|
||||
Hlp(name) => write!(f, "?{}", name),
|
||||
|
Loading…
Reference in New Issue
Block a user