feat: use a stack for scope
This commit is contained in:
parent
946937f945
commit
2ad630de90
|
@ -1,3 +1,3 @@
|
||||||
(program 11.22.33
|
(program 11.22.33
|
||||||
(lam x x)
|
(lam x (lam x y))
|
||||||
)
|
)
|
|
@ -86,15 +86,15 @@ pub struct NamedDeBruijn {
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Debug, Clone, PartialEq, Copy)]
|
#[derive(Debug, Clone, PartialEq, Copy)]
|
||||||
pub struct DeBruijn(u64);
|
pub struct DeBruijn(usize);
|
||||||
|
|
||||||
impl From<u64> for DeBruijn {
|
impl From<usize> for DeBruijn {
|
||||||
fn from(i: u64) -> Self {
|
fn from(i: usize) -> Self {
|
||||||
DeBruijn(i)
|
DeBruijn(i)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl From<DeBruijn> for u64 {
|
impl From<DeBruijn> for usize {
|
||||||
fn from(d: DeBruijn) -> Self {
|
fn from(d: DeBruijn) -> Self {
|
||||||
d.0
|
d.0
|
||||||
}
|
}
|
||||||
|
|
|
@ -3,18 +3,18 @@ use std::collections::HashMap;
|
||||||
use crate::ast::{DeBruijn, Name, NamedDeBruijn, Term, Unique};
|
use crate::ast::{DeBruijn, Name, NamedDeBruijn, Term, Unique};
|
||||||
|
|
||||||
#[derive(Debug, Copy, Clone)]
|
#[derive(Debug, Copy, Clone)]
|
||||||
struct Level(u64);
|
struct Level(usize);
|
||||||
|
|
||||||
pub(crate) struct Converter {
|
pub(crate) struct Converter {
|
||||||
current_level: Level,
|
current_level: Level,
|
||||||
levels: HashMap<Unique, Level>,
|
levels: Vec<HashMap<Unique, Level>>,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl Converter {
|
impl Converter {
|
||||||
pub(crate) fn new() -> Self {
|
pub(crate) fn new() -> Self {
|
||||||
Converter {
|
Converter {
|
||||||
current_level: Level(0),
|
current_level: Level(0),
|
||||||
levels: HashMap::new(),
|
levels: vec![HashMap::new()],
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -41,11 +41,15 @@ impl Converter {
|
||||||
index,
|
index,
|
||||||
};
|
};
|
||||||
|
|
||||||
self.with_scope();
|
self.start_scope();
|
||||||
|
|
||||||
|
let body = self.name_to_named_debruijn(*body)?;
|
||||||
|
|
||||||
|
self.end_scope();
|
||||||
|
|
||||||
Term::Lambda {
|
Term::Lambda {
|
||||||
parameter_name: name,
|
parameter_name: name,
|
||||||
body: Box::new(self.name_to_named_debruijn(*body)?),
|
body: Box::new(body),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
Term::Apply { function, argument } => Term::Apply {
|
Term::Apply { function, argument } => Term::Apply {
|
||||||
|
@ -69,20 +73,32 @@ impl Converter {
|
||||||
}
|
}
|
||||||
|
|
||||||
fn get_index(&mut self, unique: Unique) -> anyhow::Result<DeBruijn> {
|
fn get_index(&mut self, unique: Unique) -> anyhow::Result<DeBruijn> {
|
||||||
if let Some(found_level) = self.levels.get(&unique) {
|
for scope in self.levels.iter().rev() {
|
||||||
|
if let Some(found_level) = scope.get(&unique) {
|
||||||
let index = self.current_level.0 - found_level.0;
|
let index = self.current_level.0 - found_level.0;
|
||||||
|
|
||||||
Ok(index.into())
|
return Ok(index.into());
|
||||||
} else {
|
|
||||||
anyhow::bail!("Free unique: {}", isize::from(unique));
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
anyhow::bail!("Free unique: {}", isize::from(unique))
|
||||||
|
}
|
||||||
|
|
||||||
fn declare_unique(&mut self, unique: Unique) {
|
fn declare_unique(&mut self, unique: Unique) {
|
||||||
self.levels.insert(unique, self.current_level);
|
let scope = &mut self.levels[self.current_level.0];
|
||||||
|
|
||||||
|
scope.insert(unique, self.current_level);
|
||||||
}
|
}
|
||||||
|
|
||||||
fn with_scope(&mut self) {
|
fn start_scope(&mut self) {
|
||||||
self.current_level = Level(self.current_level.0 + 1);
|
self.current_level = Level(self.current_level.0 + 1);
|
||||||
|
|
||||||
|
self.levels.push(HashMap::new());
|
||||||
|
}
|
||||||
|
|
||||||
|
fn end_scope(&mut self) {
|
||||||
|
self.current_level = Level(self.current_level.0 - 1);
|
||||||
|
|
||||||
|
self.levels.pop();
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in New Issue