From b707d044d2fdd9a831f488ed3f7e55d2301f9337 Mon Sep 17 00:00:00 2001 From: Nilstrieb <48135649+Nilstrieb@users.noreply.github.com> Date: Sun, 7 Nov 2021 21:44:29 +0100 Subject: [PATCH] ice ice baby (god no) --- rust-toolchain | 1 + src/count.rs | 25 ++------------------- src/helper.rs | 60 ++++++++++++++++++++++++++++++++++++++++++++++++++ src/index.rs | 21 ++++++++++++++++++ src/main.rs | 15 +++++++++++++ 5 files changed, 99 insertions(+), 23 deletions(-) create mode 100644 rust-toolchain create mode 100644 src/helper.rs create mode 100644 src/index.rs diff --git a/rust-toolchain b/rust-toolchain new file mode 100644 index 0000000..07ade69 --- /dev/null +++ b/rust-toolchain @@ -0,0 +1 @@ +nightly \ No newline at end of file diff --git a/src/count.rs b/src/count.rs index c1e6db6..8e07c8b 100644 --- a/src/count.rs +++ b/src/count.rs @@ -1,25 +1,4 @@ -use std::marker::PhantomData; - -trait Nat { - fn int() -> i32; -} - -struct Z; - -impl Nat for Z { - fn int() -> i32 { - 0 - } -} - -struct S(PhantomData); - -impl Nat for S { - fn int() -> i32 { - N::int() + 1 - } -} - +use crate::helper::{Nat, S, Z}; trait Count: Nat { fn count() -> String; @@ -39,4 +18,4 @@ impl Count for S { pub fn count() { println!("{}", >> as Count>::count()); -} \ No newline at end of file +} diff --git a/src/helper.rs b/src/helper.rs new file mode 100644 index 0000000..b8e77c5 --- /dev/null +++ b/src/helper.rs @@ -0,0 +1,60 @@ +use std::marker::PhantomData; + +/////////// type level arithmetic + +pub trait Nat { + fn int() -> i32; +} + +pub struct Z; + +impl Nat for Z { + fn int() -> i32 { + 0 + } +} + +pub struct S(PhantomData); + +impl Nat for S { + fn int() -> i32 { + N::int() + 1 + } +} + +/////////// bound numbers + +#[derive(Debug, Copy, Clone, Ord, PartialOrd, Eq, PartialEq, Hash)] +pub struct Bound(usize); + +impl Bound { + pub fn new(num: usize) -> Option> { + if num < UPPER { + Some(Self(num)) + } else { + None + } + } +} + +impl Bound { + pub fn inner(&self) -> usize { + self.0 + } +} + +//////////// boolean expression testing + +pub trait True {} + +pub trait False {} + +pub struct Test(); + +impl True for Test {} +impl False for Test {} + +pub struct Not(PhantomData); + +impl True for Not where B: False {} +impl False for Not where B: True {} diff --git a/src/index.rs b/src/index.rs new file mode 100644 index 0000000..fde1436 --- /dev/null +++ b/src/index.rs @@ -0,0 +1,21 @@ +use crate::helper::{Bound, Test, True}; + +pub trait SafeIdx { + type Output; + + fn safe_idx(&self, num: Bound) -> &Self::Output; +} + +impl SafeIdx for [T; SIZE] +where + Test<{ BOUND <= SIZE }>: True, +{ + type Output = T; + + fn safe_idx(&self, num: Bound) -> &Self::Output { + // SAFETY: We can be sure that we are not out of bounds because + // `num` will always be less than `BOUND`, and `BOUND` will always + // be less than or equal to our SIZE + unsafe { self.get_unchecked(num.inner()) } + } +} diff --git a/src/main.rs b/src/main.rs index a47ddb2..90a8003 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,5 +1,20 @@ +#![feature(generic_const_exprs)] +#![allow(incomplete_features)] + +use crate::helper::Bound; +use crate::index::SafeIdx; + mod count; +mod helper; +mod index; fn main() { count::count(); + + let array = [1, 2, 3]; + let bound_1 = Bound::<3>::new(2).unwrap(); + let bound_2 = Bound::<1>::new(0).unwrap(); + + println!("{}", array.safe_idx(bound_1)); + println!("{}", array.safe_idx(bound_2)); }