mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-20 21:29:06 +03:00
fix: erasure checker
This commit is contained in:
parent
42d8baf03d
commit
b5636ac6c0
@ -70,7 +70,7 @@ pub fn type_check(
|
|||||||
|
|
||||||
succeeded
|
succeeded
|
||||||
}
|
}
|
||||||
Err(_) => panic!(),
|
Err(res) => panic!("{}", res),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -1,11 +1,12 @@
|
|||||||
|
|
||||||
|
#kdl_run
|
||||||
|
Main : U60
|
||||||
|
Main = Teste List.nil
|
||||||
|
|
||||||
type List (t: Type) {
|
type List (t: Type) {
|
||||||
cons (x: t) (xs: List t)
|
cons (x: t) (xs: List t)
|
||||||
nil
|
nil
|
||||||
}
|
}
|
||||||
|
|
||||||
Teste (n: List U60) : U60
|
Teste (n: List U60) : U60
|
||||||
Teste (List.cons 2 xs) = 2
|
Teste (List.cons 2 xs) = 2
|
||||||
|
|
||||||
#kdl_run
|
|
||||||
Main : U60
|
|
||||||
Main = Teste List.nil
|
|
@ -1,16 +1,12 @@
|
|||||||
use checker::eval;
|
use checker::eval;
|
||||||
use errors::DriverError;
|
use errors::DriverError;
|
||||||
use fxhash::FxHashSet;
|
|
||||||
use kind_pass::{desugar, erasure, expand};
|
use kind_pass::{desugar, erasure, expand};
|
||||||
use kind_report::{data::Diagnostic, report::FileCache};
|
use kind_report::{report::FileCache};
|
||||||
use kind_span::SyntaxCtxIndex;
|
use kind_span::SyntaxCtxIndex;
|
||||||
|
|
||||||
use kind_tree::{backend, concrete, desugared, untyped};
|
use kind_tree::{backend, concrete, desugared, untyped};
|
||||||
use session::Session;
|
use session::Session;
|
||||||
use std::{
|
use std::path::{PathBuf};
|
||||||
path::{Path, PathBuf},
|
|
||||||
sync::mpsc::Sender,
|
|
||||||
};
|
|
||||||
|
|
||||||
use kind_checker as checker;
|
use kind_checker as checker;
|
||||||
|
|
||||||
@ -37,13 +33,7 @@ pub fn type_check_book(session: &mut Session, path: &PathBuf) -> Option<untyped:
|
|||||||
return None;
|
return None;
|
||||||
}
|
}
|
||||||
|
|
||||||
let erased = erasure::erase_book(
|
todo!()
|
||||||
desugared_book,
|
|
||||||
session.diagnostic_sender.clone(),
|
|
||||||
FxHashSet::from_iter(vec!["Main".to_string()]),
|
|
||||||
)?;
|
|
||||||
|
|
||||||
Some(erased)
|
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn to_book(session: &mut Session, path: &PathBuf) -> Option<concrete::Book> {
|
pub fn to_book(session: &mut Session, path: &PathBuf) -> Option<concrete::Book> {
|
||||||
@ -67,11 +57,7 @@ pub fn erase_book(
|
|||||||
) -> Option<untyped::Book> {
|
) -> Option<untyped::Book> {
|
||||||
let concrete_book = to_book(session, path)?;
|
let concrete_book = to_book(session, path)?;
|
||||||
let desugared_book = desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)?;
|
let desugared_book = desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)?;
|
||||||
erasure::erase_book(
|
erasure::erase_book(&desugared_book, session.diagnostic_sender.clone())
|
||||||
desugared_book,
|
|
||||||
session.diagnostic_sender.clone(),
|
|
||||||
FxHashSet::from_iter(entrypoint.to_owned()),
|
|
||||||
)
|
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn desugar_book(session: &mut Session, path: &PathBuf) -> Option<desugared::Book> {
|
pub fn desugar_book(session: &mut Session, path: &PathBuf) -> Option<desugared::Book> {
|
||||||
@ -82,11 +68,7 @@ pub fn desugar_book(session: &mut Session, path: &PathBuf) -> Option<desugared::
|
|||||||
pub fn check_erasure_book(session: &mut Session, path: &PathBuf) -> Option<desugared::Book> {
|
pub fn check_erasure_book(session: &mut Session, path: &PathBuf) -> Option<desugared::Book> {
|
||||||
let concrete_book = to_book(session, path)?;
|
let concrete_book = to_book(session, path)?;
|
||||||
let desugared_book = desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)?;
|
let desugared_book = desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)?;
|
||||||
erasure::erase_book(
|
|
||||||
desugared_book.clone(),
|
|
||||||
session.diagnostic_sender.clone(),
|
|
||||||
FxHashSet::from_iter(vec!["Main".to_string()]),
|
|
||||||
)?;
|
|
||||||
Some(desugared_book)
|
Some(desugared_book)
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -97,24 +79,12 @@ pub fn compile_book_to_hvm(book: untyped::Book) -> backend::File {
|
|||||||
pub fn compile_book_to_kdl(
|
pub fn compile_book_to_kdl(
|
||||||
path: &PathBuf,
|
path: &PathBuf,
|
||||||
session: &mut Session,
|
session: &mut Session,
|
||||||
namespace: &str,
|
namespace: &str
|
||||||
) -> Option<kind_target_kdl::File> {
|
) -> Option<kind_target_kdl::File> {
|
||||||
let concrete_book = to_book(session, path)?;
|
let concrete_book = to_book(session, path)?;
|
||||||
let desugared_book = desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)?;
|
let desugared_book = desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)?;
|
||||||
|
let book = erasure::erase_book(&desugared_book, session.diagnostic_sender.clone())?;
|
||||||
let entrypoints = desugared_book
|
println!("{} {}", book.entrs.len(), book.names.len());
|
||||||
.entrs
|
|
||||||
.iter()
|
|
||||||
.filter(|x| x.1.attrs.kdl_run)
|
|
||||||
.map(|x| x.0.clone())
|
|
||||||
.collect::<Vec<_>>();
|
|
||||||
|
|
||||||
let book = erasure::erase_book(
|
|
||||||
desugared_book,
|
|
||||||
session.diagnostic_sender.clone(),
|
|
||||||
FxHashSet::from_iter(entrypoints),
|
|
||||||
)?;
|
|
||||||
|
|
||||||
kind_target_kdl::compile_book(book, session.diagnostic_sender.clone(), namespace)
|
kind_target_kdl::compile_book(book, session.diagnostic_sender.clone(), namespace)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -94,8 +94,8 @@ impl<'a> DesugarState<'a> {
|
|||||||
// It's not expected that positional arguments require the range so
|
// It's not expected that positional arguments require the range so
|
||||||
// it's the reason why we are using a terrible "ghost range"
|
// it's the reason why we are using a terrible "ghost range"
|
||||||
arguments[i] = Some((
|
arguments[i] = Some((
|
||||||
Range::ghost_range(),
|
range,
|
||||||
self.gen_hole_expr(Range::ghost_range()),
|
self.gen_hole_expr(range),
|
||||||
))
|
))
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -1,315 +1,377 @@
|
|||||||
//! Erases everything that is not relevant to the output.
|
|
||||||
//! It's a simpler version of what I want to do in order
|
|
||||||
//! to finish a stable version of the compiler.
|
|
||||||
|
|
||||||
// FIX: Need to make a "constraint map" in order to check
|
|
||||||
// if a irrelevant thing is relevant in relation to the
|
|
||||||
// function that we are trying to check the irrelevance.
|
|
||||||
|
|
||||||
// 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 std::sync::mpsc::Sender;
|
||||||
|
|
||||||
use fxhash::{FxHashMap, FxHashSet};
|
use fxhash::{FxHashMap, FxHashSet};
|
||||||
|
|
||||||
use kind_report::data::Diagnostic;
|
use kind_report::data::Diagnostic;
|
||||||
use kind_span::Range;
|
use kind_span::Range;
|
||||||
use kind_tree::desugared::{Book, Entry, Expr, Rule};
|
|
||||||
use kind_tree::symbol::QualifiedIdent;
|
use kind_tree::desugared;
|
||||||
use kind_tree::{untyped, Number};
|
use kind_tree::symbol::{Ident, QualifiedIdent};
|
||||||
|
use kind_tree::untyped::{self};
|
||||||
|
use kind_tree::Number;
|
||||||
|
|
||||||
use crate::errors::PassError;
|
use crate::errors::PassError;
|
||||||
|
|
||||||
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
|
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
|
||||||
pub enum Relevance {
|
enum Relevance {
|
||||||
|
Relevant,
|
||||||
|
Irrelevant,
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
|
||||||
|
enum Ambient {
|
||||||
|
Unknown,
|
||||||
Irrelevant,
|
Irrelevant,
|
||||||
Relevant,
|
Relevant,
|
||||||
Hole(usize),
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
impl Ambient {
|
||||||
|
pub fn to_relev(&self) -> Relevance {
|
||||||
|
match self {
|
||||||
|
Ambient::Irrelevant => Relevance::Irrelevant,
|
||||||
|
Ambient::Unknown | Ambient::Relevant => Relevance::Relevant,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub struct Edge {
|
||||||
|
name: String,
|
||||||
|
relevance: FxHashMap<Relevance, Vec<Range>>,
|
||||||
|
connections: FxHashMap<usize, Vec<(Range, Ambient)>>,
|
||||||
|
}
|
||||||
|
|
||||||
pub struct ErasureState<'a> {
|
pub struct ErasureState<'a> {
|
||||||
errs: Sender<Box<dyn Diagnostic>>,
|
errs: Sender<Box<dyn Diagnostic>>,
|
||||||
book: &'a Book,
|
book: &'a desugared::Book,
|
||||||
|
|
||||||
ctx: im::HashMap<String, (Range, (Option<Range>, Relevance))>,
|
edges: Vec<Edge>,
|
||||||
|
names: FxHashMap<String, (Range, usize)>,
|
||||||
|
|
||||||
|
ctx: im::HashMap<String, Relevance>,
|
||||||
|
|
||||||
names: FxHashMap<String, (Option<Range>, Relevance)>,
|
|
||||||
holes: Vec<Option<Relevance>>,
|
|
||||||
failed: bool,
|
failed: bool,
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn erase_book(
|
pub fn erase_book<'a>(
|
||||||
book: Book,
|
book: &'a desugared::Book,
|
||||||
errs: Sender<Box<dyn Diagnostic>>,
|
errs: Sender<Box<dyn Diagnostic>>,
|
||||||
entrypoint: FxHashSet<String>,
|
|
||||||
) -> Option<untyped::Book> {
|
) -> Option<untyped::Book> {
|
||||||
let mut state = ErasureState {
|
let mut state = ErasureState {
|
||||||
errs,
|
errs,
|
||||||
book: &book,
|
book,
|
||||||
ctx: Default::default(),
|
edges: Default::default(),
|
||||||
names: Default::default(),
|
names: Default::default(),
|
||||||
holes: Default::default(),
|
ctx: Default::default(),
|
||||||
failed: false,
|
failed: Default::default(),
|
||||||
};
|
};
|
||||||
|
|
||||||
let mut new_book = untyped::Book {
|
state.erase_book(book)
|
||||||
holes: book.holes,
|
|
||||||
..Default::default()
|
|
||||||
};
|
|
||||||
|
|
||||||
let mut entries = FxHashMap::default();
|
|
||||||
|
|
||||||
for name in entrypoint {
|
|
||||||
let count = state.holes.len();
|
|
||||||
state
|
|
||||||
.names
|
|
||||||
.insert(name.to_string(), (None, Relevance::Hole(count)));
|
|
||||||
state.holes.push(Some(Relevance::Relevant));
|
|
||||||
}
|
|
||||||
|
|
||||||
for (name, v) in &book.entrs {
|
|
||||||
entries.insert(name, state.erase_entry(v));
|
|
||||||
}
|
|
||||||
|
|
||||||
if state.failed {
|
|
||||||
return None;
|
|
||||||
}
|
|
||||||
|
|
||||||
for (name, (_, relev)) in &state.names {
|
|
||||||
if let Some(Relevance::Relevant) = state.normalize(*relev) {
|
|
||||||
if let Some(res) = entries.remove(name) {
|
|
||||||
new_book
|
|
||||||
.names
|
|
||||||
.insert(name.to_string(), new_book.entrs.len());
|
|
||||||
new_book.entrs.insert(name.to_string(), res);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
Some(new_book)
|
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'a> ErasureState<'a> {
|
impl<'a> ErasureState<'a> {
|
||||||
pub fn new_hole(&mut self, range: Range, name: String) -> (Option<Range>, Relevance) {
|
fn get_edge_or_create(&mut self, name: &QualifiedIdent) -> usize {
|
||||||
let count = self.holes.len();
|
if let Some(id) = self.names.get(&name.to_string()) {
|
||||||
let local_relevance = (Some(range), Relevance::Hole(count));
|
id.1
|
||||||
self.names.insert(name, local_relevance);
|
} else {
|
||||||
self.holes.push(None);
|
let id = self.edges.len();
|
||||||
local_relevance
|
self.names.insert(name.to_string(), (name.range, id));
|
||||||
|
self.edges.push(Edge {
|
||||||
|
name: name.to_string(),
|
||||||
|
relevance: Default::default(),
|
||||||
|
connections: Default::default(),
|
||||||
|
});
|
||||||
|
id
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn send_err(&mut self, err: Box<PassError>) {
|
fn set_relevance(&mut self, id: usize, relevance: Relevance, on: Range) {
|
||||||
self.errs.send(err).unwrap();
|
let edge = self.edges.get_mut(id).unwrap();
|
||||||
self.failed = true;
|
let entry = edge.relevance.entry(relevance).or_default();
|
||||||
}
|
entry.push(on)
|
||||||
pub fn err_irrelevant(
|
|
||||||
&mut self,
|
|
||||||
declared_val: Option<Range>,
|
|
||||||
used: Range,
|
|
||||||
declared_ty: Option<Range>,
|
|
||||||
) {
|
|
||||||
self.send_err(Box::new(PassError::CannotUseIrrelevant(
|
|
||||||
declared_val,
|
|
||||||
used,
|
|
||||||
declared_ty,
|
|
||||||
)));
|
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn get_normal(&self, hole: usize, visited: &mut FxHashSet<usize>) -> Option<Relevance> {
|
fn connect_with(&mut self, id: usize, name: &QualifiedIdent, ambient: Ambient) {
|
||||||
match self.holes[hole] {
|
let new_id = self.get_edge_or_create(name);
|
||||||
Some(Relevance::Hole(r)) if !visited.contains(&hole) => {
|
let entry = self.edges[id].connections.entry(new_id).or_default();
|
||||||
visited.insert(hole);
|
entry.push((name.range, ambient))
|
||||||
self.get_normal(r, visited)
|
}
|
||||||
|
|
||||||
|
pub fn erase_book(&mut self, book: &'a desugared::Book) -> Option<untyped::Book> {
|
||||||
|
let mut vals = FxHashMap::default();
|
||||||
|
|
||||||
|
let mut entrypoints = Vec::new();
|
||||||
|
|
||||||
|
if let Some(entr) = book.entrs.get("Main") {
|
||||||
|
let id = self.get_edge_or_create(&entr.name);
|
||||||
|
self.set_relevance(id, Relevance::Relevant, entr.name.range);
|
||||||
|
entrypoints.push(id);
|
||||||
|
}
|
||||||
|
|
||||||
|
for entr in book.entrs.values() {
|
||||||
|
if entr.attrs.kdl_run {
|
||||||
|
let id = self.get_edge_or_create(&entr.name);
|
||||||
|
self.set_relevance(id, Relevance::Relevant, entr.name.range);
|
||||||
|
entrypoints.push(id);
|
||||||
}
|
}
|
||||||
other => other,
|
|
||||||
}
|
}
|
||||||
}
|
|
||||||
|
|
||||||
pub fn normalize(&self, hole: Relevance) -> Option<Relevance> {
|
for entr in book.entrs.values() {
|
||||||
match hole {
|
vals.insert(entr.name.to_string(), self.erase_entry(entr));
|
||||||
Relevance::Hole(hole) => self.get_normal(hole, &mut Default::default()),
|
|
||||||
other => Some(other),
|
|
||||||
}
|
}
|
||||||
}
|
|
||||||
|
|
||||||
pub fn unify_loop(
|
let mut visited = FxHashSet::<usize>::default();
|
||||||
&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), 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)
|
|
||||||
}
|
|
||||||
|
|
||||||
// TODO: It should unify iff we want functions that are considered
|
let mut new_book = untyped::Book {
|
||||||
// "erased" in the sense that we can just remove them from the runtime and it'll
|
entrs: Default::default(),
|
||||||
// be fine.
|
names: Default::default(),
|
||||||
(None, Relevance::Irrelevant) => {
|
|
||||||
self.holes[hole] = Some(Relevance::Irrelevant);
|
|
||||||
true
|
|
||||||
}
|
|
||||||
|
|
||||||
(None, Relevance::Hole(n)) => {
|
|
||||||
self.holes[hole] = Some(Relevance::Hole(n));
|
|
||||||
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 {
|
|
||||||
self.unify_loop(range, left, right, &mut Default::default(), relevance_unify)
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn erase_pat_spine(
|
|
||||||
&mut self,
|
|
||||||
on: (Option<Range>, Relevance),
|
|
||||||
name: &QualifiedIdent,
|
|
||||||
spine: &Vec<Box<Expr>>,
|
|
||||||
) -> Vec<Box<untyped::Expr>> {
|
|
||||||
let fun = match self.names.get(name.to_str()) {
|
|
||||||
Some(res) => *res,
|
|
||||||
None => self.new_hole(name.range, name.to_string()),
|
|
||||||
};
|
};
|
||||||
|
|
||||||
if !self.unify(name.range, on, fun, true) {
|
let mut queue = entrypoints.iter().map(|x| (x, Ambient::Relevant)).collect::<Vec<_>>();
|
||||||
self.err_irrelevant(None, name.range, None)
|
|
||||||
|
while !queue.is_empty() {
|
||||||
|
let (fst, relev) = queue.pop().unwrap();
|
||||||
|
|
||||||
|
if visited.contains(&fst) {
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
|
||||||
|
visited.insert(*fst);
|
||||||
|
|
||||||
|
let edge = &self.edges[*fst];
|
||||||
|
|
||||||
|
if relev != Ambient::Irrelevant {
|
||||||
|
if let Some(res) = edge.relevance.get(&Relevance::Irrelevant) {
|
||||||
|
self.errs
|
||||||
|
.send(Box::new(PassError::CannotUseIrrelevant(None, res[0], None)))
|
||||||
|
.unwrap();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
let entry = vals.get(&edge.name).cloned().unwrap();
|
||||||
|
|
||||||
|
new_book.names.insert(entry.name.to_string(), new_book.entrs.len());
|
||||||
|
|
||||||
|
new_book.entrs.insert(
|
||||||
|
entry.name.to_string(),
|
||||||
|
entry
|
||||||
|
);
|
||||||
|
|
||||||
|
for (to, relevs) in &edge.connections {
|
||||||
|
for (_, relev) in relevs.iter() {
|
||||||
|
match relev {
|
||||||
|
Ambient::Irrelevant => (),
|
||||||
|
Ambient::Unknown | Ambient::Relevant => {
|
||||||
|
if !visited.contains(to) {
|
||||||
|
queue.push((to, *relev));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
let entry = self.book.entrs.get(name.to_str()).unwrap();
|
if self.failed {
|
||||||
let erased = entry.args.iter();
|
None
|
||||||
|
} else {
|
||||||
spine
|
Some(new_book)
|
||||||
.iter()
|
}
|
||||||
.zip(erased)
|
|
||||||
.map(|(elem, arg)| {
|
|
||||||
let relev = if arg.erased {
|
|
||||||
(Some(arg.range), Relevance::Irrelevant)
|
|
||||||
} else {
|
|
||||||
on.clone()
|
|
||||||
};
|
|
||||||
(self.erase_pat(relev, elem), arg.erased)
|
|
||||||
})
|
|
||||||
.filter(|res| !res.1)
|
|
||||||
.map(|res| res.0)
|
|
||||||
.collect()
|
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn erase_pat(&mut self, on: (Option<Range>, Relevance), pat: &Expr) -> Box<untyped::Expr> {
|
fn erase_entry(&mut self, entry: &'a desugared::Entry) -> Box<untyped::Entry> {
|
||||||
use kind_tree::desugared::ExprKind::*;
|
let id = self.get_edge_or_create(&entry.name);
|
||||||
|
|
||||||
match &pat.data {
|
let mut args = Vec::new();
|
||||||
Num {
|
|
||||||
num: Number::U60(n),
|
let backup = self.ctx.clone();
|
||||||
} => untyped::Expr::num60(pat.range, *n),
|
|
||||||
Num {
|
for arg in &entry.args {
|
||||||
num: Number::U120(n),
|
self.erase_expr(Ambient::Irrelevant, id, &arg.typ);
|
||||||
} => untyped::Expr::num120(pat.range, *n),
|
self.ctx.insert(arg.name.to_string(), Relevance::Irrelevant);
|
||||||
|
if !arg.hidden {
|
||||||
|
args.push((arg.name.to_string(), arg.range, false))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
self.erase_expr(Ambient::Irrelevant, id, &entry.typ);
|
||||||
|
|
||||||
|
self.ctx = backup;
|
||||||
|
|
||||||
|
let mut rules = Vec::new();
|
||||||
|
|
||||||
|
for rule in &entry.rules {
|
||||||
|
rules.push(self.erase_rule(entry, id, rule));
|
||||||
|
}
|
||||||
|
|
||||||
|
Box::new(untyped::Entry {
|
||||||
|
name: entry.name.clone(),
|
||||||
|
args,
|
||||||
|
rules,
|
||||||
|
attrs: entry.attrs.clone(),
|
||||||
|
range: entry.range,
|
||||||
|
})
|
||||||
|
}
|
||||||
|
|
||||||
|
fn erase_rule(
|
||||||
|
&mut self,
|
||||||
|
entr: &desugared::Entry,
|
||||||
|
edge: usize,
|
||||||
|
rule: &'a desugared::Rule,
|
||||||
|
) -> untyped::Rule {
|
||||||
|
let backup = self.ctx.clone();
|
||||||
|
|
||||||
|
let has_relevance = self.edges[edge]
|
||||||
|
.relevance
|
||||||
|
.contains_key(&Relevance::Relevant);
|
||||||
|
|
||||||
|
let relev = |hidden: bool| -> Ambient {
|
||||||
|
if hidden {
|
||||||
|
Ambient::Irrelevant
|
||||||
|
} else if has_relevance {
|
||||||
|
Ambient::Relevant
|
||||||
|
} else {
|
||||||
|
Ambient::Unknown
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
let pats = rule
|
||||||
|
.pats
|
||||||
|
.iter()
|
||||||
|
.zip(&entr.args)
|
||||||
|
.map(|(pat, arg)| (self.erase_pat(relev(arg.hidden), edge, pat), arg))
|
||||||
|
.filter(|(_, arg)| !arg.erased)
|
||||||
|
.map(|res| res.0)
|
||||||
|
.collect::<Vec<_>>();
|
||||||
|
|
||||||
|
|
||||||
|
let body = self.erase_expr(relev(false), edge, &rule.body);
|
||||||
|
|
||||||
|
self.ctx = backup;
|
||||||
|
|
||||||
|
untyped::Rule {
|
||||||
|
name: entr.name.clone(),
|
||||||
|
pats,
|
||||||
|
body,
|
||||||
|
range: rule.range,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn erase_pat(
|
||||||
|
&mut self,
|
||||||
|
relevance: Ambient,
|
||||||
|
edge: usize,
|
||||||
|
expr: &'a desugared::Expr,
|
||||||
|
) -> Box<untyped::Expr> {
|
||||||
|
let relev = |hidden: bool| -> Ambient {
|
||||||
|
if hidden {
|
||||||
|
Ambient::Irrelevant
|
||||||
|
} else {
|
||||||
|
relevance
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
use desugared::ExprKind::*;
|
||||||
|
|
||||||
|
match &expr.data {
|
||||||
Var { name } => {
|
Var { name } => {
|
||||||
self.ctx.insert(name.to_string(), (name.range, on));
|
self.ctx.insert(
|
||||||
|
name.to_string(),
|
||||||
|
if relevance == Ambient::Irrelevant {
|
||||||
|
Relevance::Irrelevant
|
||||||
|
} else {
|
||||||
|
Relevance::Relevant
|
||||||
|
},
|
||||||
|
);
|
||||||
|
|
||||||
untyped::Expr::var(name.clone())
|
untyped::Expr::var(name.clone())
|
||||||
}
|
}
|
||||||
Fun { name, args } | Ctr { name, args } if on.1 == Relevance::Irrelevant => {
|
Hole { num } => untyped::Expr::var(Ident::generate(&format!("_x{}", num))),
|
||||||
let range = pat.range.clone();
|
|
||||||
self.errs
|
|
||||||
.send(Box::new(PassError::CannotPatternMatchOnErased(range)))
|
|
||||||
.unwrap();
|
|
||||||
self.failed = true;
|
|
||||||
self.erase_pat_spine(on, &name, args);
|
|
||||||
untyped::Expr::err(range)
|
|
||||||
}
|
|
||||||
Fun { name, args } => {
|
Fun { name, args } => {
|
||||||
let args = self.erase_pat_spine(on, &name, args);
|
self.connect_with(edge, name, relevance);
|
||||||
untyped::Expr::fun(pat.range.clone(), name.clone(), args)
|
|
||||||
|
// We cannot pattern match on functions in a relevant function.
|
||||||
|
// it would change its behaviour.
|
||||||
|
if relevance == Ambient::Irrelevant {
|
||||||
|
self.set_relevance(edge, Relevance::Irrelevant, expr.range)
|
||||||
|
}
|
||||||
|
|
||||||
|
let params = self.book.entrs.get(name.to_str()).unwrap();
|
||||||
|
|
||||||
|
let args = args
|
||||||
|
.iter()
|
||||||
|
.zip(¶ms.args)
|
||||||
|
.map(|(arg, param)| (self.erase_pat(relev(param.hidden), edge, arg), param))
|
||||||
|
.filter(|(_, param)| !param.hidden)
|
||||||
|
.map(|x| x.0)
|
||||||
|
.collect::<Vec<_>>();
|
||||||
|
|
||||||
|
untyped::Expr::fun(expr.range, name.clone(), args)
|
||||||
}
|
}
|
||||||
Ctr { name, args } => {
|
Ctr { name, args } => {
|
||||||
let args = self.erase_pat_spine(on, &name, args);
|
self.connect_with(edge, name, relevance);
|
||||||
untyped::Expr::ctr(pat.range.clone(), name.clone(), args)
|
|
||||||
|
// We cannot pattenr match on functions in a relevant function.
|
||||||
|
// it would change its behaviour.
|
||||||
|
if relevance == Ambient::Irrelevant {
|
||||||
|
self.set_relevance(edge, Relevance::Irrelevant, expr.range)
|
||||||
|
}
|
||||||
|
|
||||||
|
let params = self.book.entrs.get(name.to_str()).unwrap();
|
||||||
|
|
||||||
|
let args = args
|
||||||
|
.iter()
|
||||||
|
.zip(¶ms.args)
|
||||||
|
.map(|(arg, param)| (self.erase_pat(relev(param.hidden), edge, arg), param))
|
||||||
|
.filter(|(_, param)| !param.hidden)
|
||||||
|
.map(|x| x.0)
|
||||||
|
.collect::<Vec<_>>();
|
||||||
|
|
||||||
|
untyped::Expr::ctr(expr.range, name.clone(), args)
|
||||||
}
|
}
|
||||||
res => panic!("Internal Error: Not a pattern {:?}", res),
|
Num {
|
||||||
|
num: Number::U60(num),
|
||||||
|
} => untyped::Expr::num60(expr.range, *num),
|
||||||
|
Num {
|
||||||
|
num: Number::U120(num),
|
||||||
|
} => untyped::Expr::num120(expr.range, *num),
|
||||||
|
Str { val } => {
|
||||||
|
let nil = QualifiedIdent::new_static("String.nil", None, expr.range);
|
||||||
|
let cons = QualifiedIdent::new_static("String.cons", None, expr.range);
|
||||||
|
|
||||||
|
self.connect_with(edge, &nil, relevance);
|
||||||
|
self.connect_with(edge, &cons, relevance);
|
||||||
|
|
||||||
|
untyped::Expr::str(expr.range, val.clone())
|
||||||
|
}
|
||||||
|
_ => todo!("Cannot be parsed {}", expr),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn erase_expr(
|
fn erase_expr(
|
||||||
&mut self,
|
&mut self,
|
||||||
on: &(Option<Range>, Relevance),
|
ambient: Ambient,
|
||||||
expr: &Expr,
|
edge: usize,
|
||||||
|
expr: &'a desugared::Expr,
|
||||||
) -> Box<untyped::Expr> {
|
) -> Box<untyped::Expr> {
|
||||||
use kind_tree::desugared::ExprKind::*;
|
use desugared::ExprKind::*;
|
||||||
|
|
||||||
match &expr.data {
|
match &expr.data {
|
||||||
Typ | NumType { .. } | Err | Hole { .. } | Hlp(_) => {
|
|
||||||
if !self.unify(expr.range, *on, (None, Relevance::Irrelevant), false) {
|
|
||||||
self.err_irrelevant(None, expr.range, None)
|
|
||||||
}
|
|
||||||
// Used as sentinel value because all of these constructions
|
|
||||||
// should not end in the generated tree.
|
|
||||||
untyped::Expr::err(expr.range)
|
|
||||||
}
|
|
||||||
Num {
|
|
||||||
num: Number::U60(n),
|
|
||||||
} => untyped::Expr::num60(expr.range, *n),
|
|
||||||
Num {
|
|
||||||
num: Number::U120(n),
|
|
||||||
} => untyped::Expr::num120(expr.range, *n),
|
|
||||||
Str { val } => untyped::Expr::str(expr.range, val.clone()),
|
|
||||||
Var { name } => {
|
|
||||||
let relev = self.ctx.get(name.to_str()).unwrap();
|
|
||||||
let declared_ty = (relev.1).0;
|
|
||||||
let declared_val = relev.0;
|
|
||||||
if !self.unify(name.range, *on, relev.1, false) {
|
|
||||||
self.err_irrelevant(Some(declared_val), name.range, declared_ty)
|
|
||||||
}
|
|
||||||
untyped::Expr::var(name.clone())
|
|
||||||
}
|
|
||||||
All {
|
All {
|
||||||
param, typ, body, ..
|
param,
|
||||||
|
typ,
|
||||||
|
body,
|
||||||
|
erased: _,
|
||||||
} => {
|
} => {
|
||||||
if !self.unify(expr.range, *on, (None, Relevance::Irrelevant), false) {
|
let backup = self.ctx.clone();
|
||||||
self.err_irrelevant(None, expr.range, None)
|
self.ctx.insert(param.to_string(), Relevance::Irrelevant);
|
||||||
|
|
||||||
|
if ambient != Ambient::Irrelevant {
|
||||||
|
self.set_relevance(edge, Relevance::Irrelevant, expr.range);
|
||||||
}
|
}
|
||||||
|
|
||||||
let ctx = self.ctx.clone();
|
self.erase_expr(Ambient::Irrelevant, edge, typ);
|
||||||
|
self.erase_expr(Ambient::Irrelevant, edge, body);
|
||||||
|
|
||||||
// Relevant inside the context that is it's being used?
|
self.ctx = backup;
|
||||||
self.ctx.insert(param.to_string(), (param.range, *on));
|
|
||||||
|
|
||||||
self.erase_expr(&(on.0, Relevance::Irrelevant), typ);
|
|
||||||
self.erase_expr(&(on.0, Relevance::Irrelevant), body);
|
|
||||||
self.ctx = ctx;
|
|
||||||
|
|
||||||
// Used as sentinel value because "All" should not end in a tree.
|
|
||||||
untyped::Expr::err(expr.range)
|
untyped::Expr::err(expr.range)
|
||||||
}
|
}
|
||||||
Lambda {
|
Lambda {
|
||||||
@ -317,204 +379,131 @@ impl<'a> ErasureState<'a> {
|
|||||||
body,
|
body,
|
||||||
erased,
|
erased,
|
||||||
} => {
|
} => {
|
||||||
let ctx = self.ctx.clone();
|
let backup = self.ctx.clone();
|
||||||
|
|
||||||
if *erased {
|
let relev = if ambient == Ambient::Irrelevant || *erased {
|
||||||
self.ctx.insert(
|
Relevance::Irrelevant
|
||||||
param.to_string(),
|
|
||||||
(param.range, (None, Relevance::Irrelevant)),
|
|
||||||
);
|
|
||||||
} else {
|
} else {
|
||||||
self.ctx.insert(param.to_string(), (param.range, *on));
|
Relevance::Relevant
|
||||||
}
|
};
|
||||||
|
|
||||||
let body = self.erase_expr(on, body);
|
self.ctx.insert(param.to_string(), relev);
|
||||||
self.ctx = ctx;
|
|
||||||
|
|
||||||
if *erased {
|
let body = self.erase_expr(ambient, edge, body);
|
||||||
body
|
|
||||||
} else {
|
self.ctx = backup;
|
||||||
untyped::Expr::lambda(expr.range, param.clone(), body, *erased)
|
|
||||||
}
|
untyped::Expr::lambda(expr.range, param.clone(), body, *erased)
|
||||||
}
|
}
|
||||||
Let { name, val, next } => {
|
Let { name, val, next } => {
|
||||||
let ctx = self.ctx.clone();
|
let backup = self.ctx.clone();
|
||||||
self.ctx.insert(name.to_string(), (name.range, *on));
|
|
||||||
|
|
||||||
let val = self.erase_expr(on, val);
|
self.ctx.insert(name.to_string(), ambient.to_relev());
|
||||||
let next = self.erase_expr(on, next);
|
|
||||||
|
|
||||||
self.ctx = ctx;
|
let val = self.erase_expr(ambient, edge, val);
|
||||||
|
let next = self.erase_expr(ambient, edge, next);
|
||||||
|
|
||||||
|
self.ctx = backup;
|
||||||
|
|
||||||
untyped::Expr::let_(expr.range, name.clone(), val, next)
|
untyped::Expr::let_(expr.range, name.clone(), val, next)
|
||||||
}
|
}
|
||||||
App { fun, args } => {
|
|
||||||
let head = self.erase_expr(on, fun);
|
|
||||||
let spine = args
|
|
||||||
.iter()
|
|
||||||
.map(|x| {
|
|
||||||
let on = if x.erased {
|
|
||||||
let span = expr.range;
|
|
||||||
if !self.unify(span, *on, (None, Relevance::Irrelevant), false) {
|
|
||||||
self.err_irrelevant(None, span, None)
|
|
||||||
}
|
|
||||||
(Some(x.data.range), Relevance::Irrelevant)
|
|
||||||
} else {
|
|
||||||
on.clone()
|
|
||||||
};
|
|
||||||
(x.erased, self.erase_expr(&on, &x.data))
|
|
||||||
})
|
|
||||||
.filter(|x| !x.0)
|
|
||||||
.map(|x| x.1)
|
|
||||||
.collect();
|
|
||||||
|
|
||||||
untyped::Expr::app(expr.range, head, spine)
|
|
||||||
}
|
|
||||||
Fun { name, args } => {
|
Fun { name, args } => {
|
||||||
let spine = self.book.entrs.get(name.to_str()).unwrap().args.iter();
|
self.connect_with(edge, name, ambient);
|
||||||
|
|
||||||
let fun = match self.names.get(name.to_str()) {
|
let params = &self.book.entrs.get(name.to_str()).unwrap().args;
|
||||||
Some(res) => *res,
|
|
||||||
None => self.new_hole(name.range, name.to_string()),
|
let relev = |hidden| {
|
||||||
|
if hidden {
|
||||||
|
Ambient::Irrelevant
|
||||||
|
} else {
|
||||||
|
ambient
|
||||||
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
if !self.unify(name.range, *on, fun, true) {
|
let args = params
|
||||||
self.err_irrelevant(None, name.range, None)
|
|
||||||
}
|
|
||||||
|
|
||||||
let spine = args
|
|
||||||
.iter()
|
.iter()
|
||||||
.zip(spine)
|
.zip(args)
|
||||||
.map(|(expr, arg)| {
|
.map(|(param, arg)| (param, self.erase_expr(relev(param.erased), edge, arg)))
|
||||||
if arg.erased {
|
.filter(|(param, _)| !param.erased)
|
||||||
(
|
.map(|res| res.1)
|
||||||
self.erase_expr(&(Some(arg.range), Relevance::Irrelevant), expr),
|
.collect::<Vec<_>>();
|
||||||
arg,
|
|
||||||
)
|
|
||||||
} else {
|
|
||||||
(self.erase_expr(on, expr), arg)
|
|
||||||
}
|
|
||||||
})
|
|
||||||
.filter(|(_, arg)| !arg.erased);
|
|
||||||
|
|
||||||
untyped::Expr::fun(
|
untyped::Expr::fun(expr.range, name.clone(), args)
|
||||||
expr.range,
|
|
||||||
name.clone(),
|
|
||||||
spine.map(|(expr, _)| expr).collect(),
|
|
||||||
)
|
|
||||||
}
|
}
|
||||||
Ctr { name, args } => {
|
Ctr { name, args } => {
|
||||||
let spine = self.book.entrs.get(name.to_str()).unwrap().args.iter();
|
self.connect_with(edge, name, ambient);
|
||||||
|
|
||||||
let fun = match self.names.get(&name.to_string()) {
|
let params = &self.book.entrs.get(name.to_str()).unwrap().args;
|
||||||
Some(res) => *res,
|
|
||||||
None => self.new_hole(name.range, name.to_string()),
|
let relev = |hidden| {
|
||||||
|
if hidden {
|
||||||
|
Ambient::Irrelevant
|
||||||
|
} else {
|
||||||
|
ambient
|
||||||
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
if !self.unify(name.range, *on, fun, true) {
|
let args = params
|
||||||
self.err_irrelevant(None, name.range, None)
|
.iter()
|
||||||
|
.zip(args)
|
||||||
|
.map(|(param, arg)| (param, self.erase_expr(relev(param.erased), edge, arg)))
|
||||||
|
.filter(|(param, _)| !param.erased)
|
||||||
|
.map(|res| res.1)
|
||||||
|
.collect::<Vec<_>>();
|
||||||
|
|
||||||
|
untyped::Expr::ctr(expr.range, name.clone(), args)
|
||||||
|
}
|
||||||
|
Var { name } => {
|
||||||
|
let var_rev = self
|
||||||
|
.ctx
|
||||||
|
.get(&name.to_string())
|
||||||
|
.expect(&format!("Uwnraping {}", name.to_string()));
|
||||||
|
|
||||||
|
if *var_rev == Relevance::Irrelevant && ambient != Ambient::Irrelevant {
|
||||||
|
self.set_relevance(edge, Relevance::Irrelevant, name.range)
|
||||||
}
|
}
|
||||||
|
|
||||||
let spine = args
|
untyped::Expr::var(name.clone())
|
||||||
.iter()
|
|
||||||
.zip(spine)
|
|
||||||
.map(|(expr, arg)| {
|
|
||||||
if arg.erased {
|
|
||||||
(
|
|
||||||
self.erase_expr(&(Some(arg.range), Relevance::Irrelevant), expr),
|
|
||||||
arg,
|
|
||||||
)
|
|
||||||
} else {
|
|
||||||
(self.erase_expr(on, expr), arg)
|
|
||||||
}
|
|
||||||
})
|
|
||||||
.filter(|(_, arg)| !arg.erased);
|
|
||||||
|
|
||||||
untyped::Expr::ctr(
|
|
||||||
expr.range,
|
|
||||||
name.clone(),
|
|
||||||
spine.map(|(expr, _)| expr).collect(),
|
|
||||||
)
|
|
||||||
}
|
}
|
||||||
Ann { expr, typ } => {
|
Ann { expr, typ } => {
|
||||||
let res = self.erase_expr(on, expr);
|
let expr = self.erase_expr(ambient, edge, expr);
|
||||||
self.erase_expr(&(None, Relevance::Irrelevant), typ);
|
self.erase_expr(Ambient::Irrelevant, edge, typ);
|
||||||
res
|
expr
|
||||||
|
}
|
||||||
|
Num {
|
||||||
|
num: Number::U60(num),
|
||||||
|
} => untyped::Expr::num60(expr.range, *num),
|
||||||
|
Num {
|
||||||
|
num: Number::U120(num),
|
||||||
|
} => untyped::Expr::num120(expr.range, *num),
|
||||||
|
Str { val } => {
|
||||||
|
let nil = QualifiedIdent::new_static("String.nil", None, expr.range);
|
||||||
|
let cons = QualifiedIdent::new_static("String.cons", None, expr.range);
|
||||||
|
self.connect_with(edge, &nil, ambient);
|
||||||
|
self.connect_with(edge, &cons, ambient);
|
||||||
|
|
||||||
|
untyped::Expr::str(expr.range, val.clone())
|
||||||
|
}
|
||||||
|
App { fun, args } => {
|
||||||
|
let fun = self.erase_expr(ambient, edge, fun);
|
||||||
|
let mut spine = Vec::new();
|
||||||
|
for arg in args {
|
||||||
|
spine.push(self.erase_expr(ambient, edge, &arg.data))
|
||||||
|
}
|
||||||
|
untyped::Expr::app(expr.range, fun, spine)
|
||||||
|
}
|
||||||
|
Sub { expr, .. } => self.erase_expr(ambient, edge, expr),
|
||||||
|
Binary { op, left, right } => {
|
||||||
|
let left = self.erase_expr(ambient, edge, left);
|
||||||
|
let right = self.erase_expr(ambient, edge, right);
|
||||||
|
untyped::Expr::binary(expr.range, *op, left, right)
|
||||||
|
}
|
||||||
|
Typ | NumType { typ: _ } | Hole { num: _ } | Hlp(_) | Err => {
|
||||||
|
if ambient != Ambient::Irrelevant && ambient != Ambient::Irrelevant {
|
||||||
|
self.set_relevance(edge, Relevance::Irrelevant, expr.range);
|
||||||
|
}
|
||||||
|
untyped::Expr::err(expr.range)
|
||||||
}
|
}
|
||||||
Sub { expr, .. } => self.erase_expr(on, expr),
|
|
||||||
Binary { op, left, right } => untyped::Expr::binary(
|
|
||||||
expr.range,
|
|
||||||
*op,
|
|
||||||
self.erase_expr(on, left),
|
|
||||||
self.erase_expr(on, right),
|
|
||||||
),
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn erase_rule(
|
|
||||||
&mut self,
|
|
||||||
place: &(Option<Range>, Relevance),
|
|
||||||
args: Vec<(Range, bool)>,
|
|
||||||
rule: &Rule,
|
|
||||||
) -> untyped::Rule {
|
|
||||||
let ctx = self.ctx.clone();
|
|
||||||
|
|
||||||
let new_pats: Vec<_> = args
|
|
||||||
.iter()
|
|
||||||
.zip(rule.pats.iter())
|
|
||||||
.map(|((range, erased), expr)| {
|
|
||||||
(
|
|
||||||
erased,
|
|
||||||
self.erase_pat(
|
|
||||||
(
|
|
||||||
Some(*range),
|
|
||||||
if *erased {
|
|
||||||
Relevance::Irrelevant
|
|
||||||
} else {
|
|
||||||
place.1.clone()
|
|
||||||
},
|
|
||||||
),
|
|
||||||
expr,
|
|
||||||
),
|
|
||||||
)
|
|
||||||
})
|
|
||||||
.filter(|(erased, _)| !*erased)
|
|
||||||
.map(|res| res.1)
|
|
||||||
.collect();
|
|
||||||
|
|
||||||
let body = self.erase_expr(place, &rule.body);
|
|
||||||
|
|
||||||
self.ctx = ctx;
|
|
||||||
|
|
||||||
untyped::Rule {
|
|
||||||
name: rule.name.clone(),
|
|
||||||
pats: new_pats,
|
|
||||||
body,
|
|
||||||
range: rule.range,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn erase_entry(&mut self, entry: &Entry) -> Box<untyped::Entry> {
|
|
||||||
let place = if let Some(res) = self.names.get(entry.name.to_str()) {
|
|
||||||
*res
|
|
||||||
} else {
|
|
||||||
self.new_hole(entry.name.range, entry.name.to_string())
|
|
||||||
};
|
|
||||||
|
|
||||||
let args: Vec<(Range, bool)> = entry.args.iter().map(|x| (x.range, x.erased)).collect();
|
|
||||||
|
|
||||||
let rules = entry
|
|
||||||
.rules
|
|
||||||
.iter()
|
|
||||||
.map(|rule| self.erase_rule(&place, args.clone(), rule))
|
|
||||||
.collect::<Vec<untyped::Rule>>();
|
|
||||||
|
|
||||||
Box::new(untyped::Entry {
|
|
||||||
name: entry.name.clone(),
|
|
||||||
args: entry.args.iter().filter(|x| !x.erased).map(|x| (x.name.to_string(), x.range, false)).collect(),
|
|
||||||
rules,
|
|
||||||
attrs: entry.attrs.clone(),
|
|
||||||
range: entry.range,
|
|
||||||
})
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
@ -34,9 +34,7 @@ pub enum PassError {
|
|||||||
NotATypeConstructor(Range, Range),
|
NotATypeConstructor(Range, Range),
|
||||||
ShouldBeAParameter(Option<Range>, Range),
|
ShouldBeAParameter(Option<Range>, Range),
|
||||||
NoFieldCoverage(Range, Vec<String>),
|
NoFieldCoverage(Range, Vec<String>),
|
||||||
CannotPatternMatchOnErased(Range),
|
|
||||||
UnboundVariable(Vec<Ident>, Vec<String>),
|
UnboundVariable(Vec<Ident>, Vec<String>),
|
||||||
|
|
||||||
AttributeDoesNotExpectEqual(Range),
|
AttributeDoesNotExpectEqual(Range),
|
||||||
AttributeDoesNotExpectArgs(Range),
|
AttributeDoesNotExpectArgs(Range),
|
||||||
InvalidAttributeArgument(Range),
|
InvalidAttributeArgument(Range),
|
||||||
@ -67,7 +65,6 @@ impl Diagnostic for PassError {
|
|||||||
PassError::NotATypeConstructor(range, _) => Some(range.ctx),
|
PassError::NotATypeConstructor(range, _) => Some(range.ctx),
|
||||||
PassError::ShouldBeAParameter(_, range) => Some(range.ctx),
|
PassError::ShouldBeAParameter(_, range) => Some(range.ctx),
|
||||||
PassError::NoFieldCoverage(range, _) => Some(range.ctx),
|
PassError::NoFieldCoverage(range, _) => Some(range.ctx),
|
||||||
PassError::CannotPatternMatchOnErased(range) => Some(range.ctx),
|
|
||||||
PassError::UnboundVariable(ranges, _) => Some(ranges[0].range.ctx),
|
PassError::UnboundVariable(ranges, _) => Some(ranges[0].range.ctx),
|
||||||
PassError::AttributeDoesNotExpectEqual(range) => Some(range.ctx),
|
PassError::AttributeDoesNotExpectEqual(range) => Some(range.ctx),
|
||||||
PassError::AttributeDoesNotExpectArgs(range) => Some(range.ctx),
|
PassError::AttributeDoesNotExpectArgs(range) => Some(range.ctx),
|
||||||
@ -157,20 +154,6 @@ impl Diagnostic for PassError {
|
|||||||
main: true,
|
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 {
|
PassError::RulesWithInconsistentArity(arities) => DiagnosticFrame {
|
||||||
code: 201,
|
code: 201,
|
||||||
severity: Severity::Error,
|
severity: Severity::Error,
|
||||||
|
@ -229,7 +229,7 @@ pub fn flatten(book: untyped::Book) -> untyped::Book {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
let book = Book { names, entrs, holes: book.holes };
|
let book = Book { names, entrs };
|
||||||
|
|
||||||
book
|
book
|
||||||
}
|
}
|
||||||
|
@ -205,8 +205,7 @@ pub struct Entry {
|
|||||||
#[derive(Clone, Debug, Default)]
|
#[derive(Clone, Debug, Default)]
|
||||||
pub struct Book {
|
pub struct Book {
|
||||||
pub entrs: LinkedHashMap<String, Box<Entry>>,
|
pub entrs: LinkedHashMap<String, Box<Entry>>,
|
||||||
pub names: FxHashMap<String, usize>,
|
pub names: FxHashMap<String, usize>
|
||||||
pub holes: u64,
|
|
||||||
}
|
}
|
||||||
|
|
||||||
impl Expr {
|
impl Expr {
|
||||||
|
Loading…
Reference in New Issue
Block a user