fix: safe encode bits to check for 2^num_bits <= byte we are encoding

fix: I thought namedDeBruijn takes advantage of Binder for encoding and decoding.
It does not...
fix: Debruijn was being converted to NamedDeBruijn incorrectly
This commit is contained in:
microproofs 2023-06-30 23:06:38 -04:00
parent d641f731b7
commit 42544af799
3 changed files with 5 additions and 4 deletions

View File

@ -320,6 +320,6 @@ impl Encoder {
self.buffer.push(chunk.len() as u8); self.buffer.push(chunk.len() as u8);
self.buffer.extend(chunk); self.buffer.extend(chunk);
} }
self.buffer.push(0); self.buffer.push(0_u8);
} }
} }

View File

@ -251,7 +251,7 @@ impl Converter {
match term { match term {
Term::Var(name) => Term::Var( Term::Var(name) => Term::Var(
NamedDeBruijn { NamedDeBruijn {
text: format!("i_{name}"), text: "i".to_string(),
index: *name.as_ref(), index: *name.as_ref(),
} }
.into(), .into(),

View File

@ -676,6 +676,7 @@ impl<'b> Decode<'b> for NamedDeBruijn {
impl<'b> Binder<'b> for NamedDeBruijn { impl<'b> Binder<'b> for NamedDeBruijn {
fn binder_encode(&self, e: &mut Encoder) -> Result<(), en::Error> { fn binder_encode(&self, e: &mut Encoder) -> Result<(), en::Error> {
self.text.encode(e)?; self.text.encode(e)?;
self.index.encode(e)?;
Ok(()) Ok(())
} }
@ -683,7 +684,7 @@ impl<'b> Binder<'b> for NamedDeBruijn {
fn binder_decode(d: &mut Decoder) -> Result<Self, de::Error> { fn binder_decode(d: &mut Decoder) -> Result<Self, de::Error> {
Ok(NamedDeBruijn { Ok(NamedDeBruijn {
text: String::decode(d)?, text: String::decode(d)?,
index: DeBruijn::new(0), index: DeBruijn::decode(d)?,
}) })
} }
@ -778,7 +779,7 @@ fn decode_term_tag(d: &mut Decoder) -> Result<u8, de::Error> {
} }
fn safe_encode_bits(num_bits: u32, byte: u8, e: &mut Encoder) -> Result<(), en::Error> { fn safe_encode_bits(num_bits: u32, byte: u8, e: &mut Encoder) -> Result<(), en::Error> {
if 2_u8.pow(num_bits) < byte { if 2_u8.pow(num_bits) <= byte {
Err(en::Error::Message(format!( Err(en::Error::Message(format!(
"Overflow detected, cannot fit {byte} in {num_bits} bits." "Overflow detected, cannot fit {byte} in {num_bits} bits."
))) )))