-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
*Binder*: this trait is for generically handling the encoding and decoding of Var and Lambda.parameter. *Eval*: this trait is for generically looking up Var in Env Eval is implemented on DeBruijn but not for Name because Name is not evaluatable there is no way to look it up in the environment. All Name, NamedDeBruijn, and DeBruijn implement Binder because they are all technically encodable. **Note**: only DeBruijn actually ever goes on chain.
- Loading branch information
Showing
27 changed files
with
620 additions
and
365 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,57 @@ | ||
use bumpalo::Bump; | ||
|
||
use super::{Binder, Eval}; | ||
|
||
#[derive(Debug, Eq, PartialEq)] | ||
pub struct DeBruijn(usize); | ||
|
||
impl DeBruijn { | ||
pub fn new<'a>(arena: &'a Bump, i: usize) -> &'a Self { | ||
arena.alloc(DeBruijn(i)) | ||
} | ||
|
||
pub fn zero<'a>(arena: &'a Bump) -> &'a Self { | ||
arena.alloc(DeBruijn(0)) | ||
} | ||
} | ||
|
||
impl Binder for DeBruijn { | ||
fn var_encode(&self, e: &mut crate::flat::Encoder) -> Result<(), crate::flat::FlatEncodeError> { | ||
e.word(self.0); | ||
|
||
Ok(()) | ||
} | ||
|
||
fn var_decode<'a>( | ||
arena: &'a bumpalo::Bump, | ||
d: &mut crate::flat::Decoder, | ||
) -> Result<&'a Self, crate::flat::FlatDecodeError> { | ||
let i = d.word()?; | ||
|
||
let d = DeBruijn::new(arena, i); | ||
|
||
Ok(d) | ||
} | ||
|
||
fn parameter_encode( | ||
&self, | ||
_e: &mut crate::flat::Encoder, | ||
) -> Result<(), crate::flat::FlatEncodeError> { | ||
Ok(()) | ||
} | ||
|
||
fn parameter_decode<'a>( | ||
arena: &'a bumpalo::Bump, | ||
_d: &mut crate::flat::Decoder, | ||
) -> Result<&'a Self, crate::flat::FlatDecodeError> { | ||
let d = DeBruijn::new(arena, 0); | ||
|
||
Ok(d) | ||
} | ||
} | ||
|
||
impl Eval for DeBruijn { | ||
fn index(&self) -> usize { | ||
self.0 | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,31 @@ | ||
use bumpalo::Bump; | ||
|
||
mod debruijn; | ||
mod name; | ||
mod named_debruijn; | ||
|
||
pub use debruijn::*; | ||
pub use name::*; | ||
pub use named_debruijn::*; | ||
|
||
use crate::flat; | ||
|
||
pub trait Binder: std::fmt::Debug { | ||
// this might not need to return a Result | ||
fn var_encode(&self, e: &mut flat::Encoder) -> Result<(), flat::FlatEncodeError>; | ||
fn var_decode<'a>( | ||
arena: &'a Bump, | ||
d: &mut flat::Decoder, | ||
) -> Result<&'a Self, flat::FlatDecodeError>; | ||
|
||
// this might not need to return a Result | ||
fn parameter_encode(&self, e: &mut flat::Encoder) -> Result<(), flat::FlatEncodeError>; | ||
fn parameter_decode<'a>( | ||
arena: &'a Bump, | ||
d: &mut flat::Decoder, | ||
) -> Result<&'a Self, flat::FlatDecodeError>; | ||
} | ||
|
||
pub trait Eval: Binder { | ||
fn index(&self) -> usize; | ||
} |
File renamed without changes.
Empty file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.