feat: convet a named debruijn to a name

This commit is contained in:
rvcas 2022-06-15 20:12:12 -04:00
parent 7693da4bbf
commit 59a8f6477b
No known key found for this signature in database
GPG Key ID: C09B64E263F7D68C
3 changed files with 114 additions and 8 deletions

View File

@ -155,6 +155,10 @@ impl DeBruijn {
pub fn new(index: usize) -> Self {
DeBruijn(index)
}
pub fn inner(&self) -> usize {
self.0
}
}
impl From<usize> for DeBruijn {
@ -169,6 +173,12 @@ impl From<DeBruijn> for usize {
}
}
impl Display for DeBruijn {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
write!(f, "{}", self.0)
}
}
impl From<NamedDeBruijn> for DeBruijn {
fn from(n: NamedDeBruijn) -> Self {
n.index

View File

@ -1,28 +1,32 @@
use std::collections::HashMap;
use thiserror::Error;
use crate::ast::{DeBruijn, FakeNamedDeBruijn, Name, NamedDeBruijn, Term, Unique};
#[derive(Debug, Copy, Clone)]
mod bimap;
#[derive(Debug, Clone, PartialEq, Copy, Eq, Hash)]
struct Level(usize);
#[derive(Error, Debug)]
pub enum Error {
#[error("Free Unique `{0}`")]
FreeUnique(Unique),
#[error("Free Index `{0}`")]
FreeIndex(DeBruijn),
}
pub struct Converter {
current_level: Level,
levels: Vec<HashMap<Unique, Level>>,
levels: Vec<bimap::BiMap>,
current_unique: Unique,
}
impl Converter {
pub fn new() -> Self {
Converter {
current_level: Level(0),
levels: vec![HashMap::new()],
levels: vec![bimap::BiMap::new()],
current_unique: Unique::new(0),
}
}
@ -111,9 +115,49 @@ impl Converter {
pub fn named_debruijn_to_name(
&mut self,
_term: Term<NamedDeBruijn>,
term: Term<NamedDeBruijn>,
) -> Result<Term<Name>, Error> {
todo!()
let converted_term = match term {
Term::Var(NamedDeBruijn { text, index }) => Term::Var(Name {
text,
unique: self.get_unique(index)?,
}),
Term::Delay(term) => Term::Delay(Box::new(self.named_debruijn_to_name(*term)?)),
Term::Lambda {
parameter_name,
body,
} => {
self.declare_binder();
let unique = self.get_unique(parameter_name.index)?;
let name = Name {
text: parameter_name.text,
unique,
};
self.start_scope();
let body = self.named_debruijn_to_name(*body)?;
self.end_scope();
Term::Lambda {
parameter_name: name,
body: Box::new(body),
}
}
Term::Apply { function, argument } => Term::Apply {
function: Box::new(self.named_debruijn_to_name(*function)?),
argument: Box::new(self.named_debruijn_to_name(*argument)?),
},
Term::Constant(constant) => Term::Constant(constant),
Term::Force(term) => Term::Force(Box::new(self.named_debruijn_to_name(*term)?)),
Term::Error => Term::Error,
Term::Builtin(builtin) => Term::Builtin(builtin),
};
Ok(converted_term)
}
pub fn named_debruijn_to_debruijn(&mut self, term: Term<NamedDeBruijn>) -> Term<DeBruijn> {
@ -234,16 +278,36 @@ impl Converter {
Err(Error::FreeUnique(unique))
}
fn get_unique(&mut self, index: DeBruijn) -> Result<Unique, Error> {
for scope in self.levels.iter().rev() {
let index = Level(self.current_level.0 - index.inner());
if let Some(unique) = scope.get_right(&index) {
return Ok(*unique);
}
}
Err(Error::FreeIndex(index))
}
fn declare_unique(&mut self, unique: Unique) {
let scope = &mut self.levels[self.current_level.0];
scope.insert(unique, self.current_level);
}
fn declare_binder(&mut self) {
let scope = &mut self.levels[self.current_level.0];
scope.insert(self.current_unique, self.current_level);
self.current_unique.increment();
}
fn start_scope(&mut self) {
self.current_level = Level(self.current_level.0 + 1);
self.levels.push(HashMap::new());
self.levels.push(bimap::BiMap::new());
}
fn end_scope(&mut self) {

View File

@ -0,0 +1,32 @@
use std::collections::HashMap;
use crate::ast::Unique;
use super::Level;
pub struct BiMap {
left: HashMap<Unique, Level>,
right: HashMap<Level, Unique>,
}
impl BiMap {
pub(super) fn new() -> Self {
BiMap {
right: HashMap::new(),
left: HashMap::new(),
}
}
pub(super) fn insert(&mut self, unique: Unique, level: Level) {
self.left.insert(unique, level);
self.right.insert(level, unique);
}
pub(super) fn get(&self, unique: &Unique) -> Option<&Level> {
self.left.get(unique)
}
pub(super) fn get_right(&self, level: &Level) -> Option<&Unique> {
self.right.get(level)
}
}