Skip to content

Commit ef9f093

Browse files
SaltyPeppermintSaltyPeppermint
committed
Impl new specific shifts
1 parent 7c70b00 commit ef9f093

File tree

3 files changed

+152
-119
lines changed

3 files changed

+152
-119
lines changed

‎src/rewrite_system/rise/indices.rs‎

Lines changed: 118 additions & 83 deletions
Original file line numberDiff line numberDiff line change
@@ -93,12 +93,15 @@ impl Kindable for DBIndex {
9393
}
9494

9595
#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Hash, Copy, Serialize, Deserialize)]
96-
pub struct DBShift {
97-
expr: i32,
98-
nat: i32,
99-
data: i32,
100-
addr: i32,
101-
nat2nat: i32,
96+
pub enum DBShift {
97+
/// expr, nat, data, addr, nat2nat
98+
Expr((i32, i32, i32, i32, i32)),
99+
/// nat, nat2nat
100+
Nat((i32, i32)),
101+
/// nat, data, nat2nat
102+
Data((i32, i32, i32)),
103+
/// addr
104+
Addr(i32),
102105
}
103106

104107
impl DBShift {
@@ -110,85 +113,95 @@ impl DBShift {
110113
Self::new_with(kind, -1)
111114
}
112115

113-
pub fn get(&self, kind: Kind) -> i32 {
116+
fn get(&self, kind: Kind) -> i32 {
114117
match kind {
115-
Kind::Expr => self.expr,
116-
Kind::Nat => self.nat,
117-
Kind::Data => self.data,
118-
Kind::Addr => self.addr,
119-
Kind::Nat2Nat => self.nat2nat,
118+
Kind::Expr => self.expr_shift(),
119+
Kind::Nat => self.nat_shift(),
120+
Kind::Data => self.data_shift(),
121+
Kind::Addr => self.addr_shift(),
122+
Kind::Nat2Nat => self.nat2nat_shift(),
123+
}
124+
}
125+
126+
pub fn expr_shift(&self) -> i32 {
127+
match self {
128+
DBShift::Expr((expr_shift, _, _, _, _)) => *expr_shift,
129+
DBShift::Nat(_) | DBShift::Data(_) | DBShift::Addr(_) => 0,
130+
}
131+
}
132+
133+
pub fn nat_shift(&self) -> i32 {
134+
match self {
135+
DBShift::Expr((_, nat_shift, _, _, _))
136+
| DBShift::Nat((nat_shift, _))
137+
| DBShift::Data((nat_shift, _, _)) => *nat_shift,
138+
DBShift::Addr(_) => 0,
139+
}
140+
}
141+
142+
pub fn data_shift(&self) -> i32 {
143+
match self {
144+
DBShift::Expr((_, _, data_shift, _, _)) | DBShift::Data((_, data_shift, _)) => {
145+
*data_shift
146+
}
147+
DBShift::Nat(_) | DBShift::Addr(_) => 0,
148+
}
149+
}
150+
151+
pub fn addr_shift(&self) -> i32 {
152+
match self {
153+
DBShift::Expr((_, _, _, addr_shift, _)) | DBShift::Addr(addr_shift) => *addr_shift,
154+
DBShift::Nat(_) | DBShift::Data(_) => 0,
155+
}
156+
}
157+
158+
pub fn nat2nat_shift(&self) -> i32 {
159+
match self {
160+
DBShift::Expr((_, _, _, _, nat2nat_shift))
161+
| DBShift::Nat((_, nat2nat_shift))
162+
| DBShift::Data((_, _, nat2nat_shift)) => *nat2nat_shift,
163+
DBShift::Addr(_) => 0,
120164
}
121165
}
122166

123-
fn new_with(kind: Kind, value: i32) -> Self {
167+
fn new_with(kind: Kind, arg: i32) -> DBShift {
124168
match kind {
125-
Kind::Expr => Self {
126-
expr: value,
127-
nat: 0,
128-
data: 0,
129-
addr: 0,
130-
nat2nat: 0,
131-
},
132-
Kind::Nat => Self {
133-
expr: 0,
134-
nat: value,
135-
data: 0,
136-
addr: 0,
137-
nat2nat: 0,
138-
},
139-
Kind::Data => Self {
140-
expr: 0,
141-
nat: 0,
142-
data: value,
143-
addr: 0,
144-
nat2nat: 0,
145-
},
146-
Kind::Addr => Self {
147-
expr: 0,
148-
nat: 0,
149-
data: 0,
150-
addr: value,
151-
nat2nat: 0,
152-
},
153-
Kind::Nat2Nat => Self {
154-
expr: 0,
155-
nat: 0,
156-
data: 0,
157-
addr: 0,
158-
nat2nat: value,
159-
},
169+
Kind::Expr => DBShift::Expr((arg, 0, 0, 0, 0)),
170+
Kind::Nat => DBShift::Nat((arg, 0)),
171+
Kind::Data => DBShift::Data((arg, 0, 0)),
172+
Kind::Addr => DBShift::Addr(arg),
173+
Kind::Nat2Nat => panic!("No Nat2Nat shift is possible"),
160174
}
161175
}
162176
}
163177

164-
impl TryFrom<(i32, i32, i32, i32, i32)> for DBShift {
165-
type Error = IndexError;
178+
impl From<(i32, i32, i32, i32, i32)> for DBShift {
179+
fn from(value: (i32, i32, i32, i32, i32)) -> Self {
180+
Self::Expr(value)
181+
}
182+
}
166183

167-
fn try_from(value: (i32, i32, i32, i32, i32)) -> Result<Self, Self::Error> {
168-
if value.0 == 0 && value.1 == 0 && value.2 == 0 && value.3 == 0 && value.4 == 0 {
169-
return Err(IndexError::ZeroShift);
170-
}
171-
Ok(Self {
172-
expr: value.0,
173-
nat: value.1,
174-
data: value.2,
175-
addr: value.3,
176-
nat2nat: value.4,
177-
})
184+
impl From<(i32, i32, i32)> for DBShift {
185+
fn from(value: (i32, i32, i32)) -> Self {
186+
Self::Data(value)
178187
}
179188
}
180189

181-
impl std::fmt::Display for DBShift {
182-
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
183-
write!(
184-
f,
185-
"({}, {}, {}, {}, {})",
186-
self.expr, self.nat, self.data, self.addr, self.nat2nat
187-
)
190+
impl From<(i32, i32)> for DBShift {
191+
fn from(value: (i32, i32)) -> Self {
192+
Self::Nat(value)
188193
}
189194
}
190195

191-
#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Hash, Copy, Serialize, Deserialize)]
196+
impl From<i32> for DBShift {
197+
fn from(value: i32) -> Self {
198+
Self::Addr(value)
199+
}
200+
}
201+
202+
#[derive(
203+
Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Hash, Copy, Default, Serialize, Deserialize,
204+
)]
192205
pub struct DBCutoff {
193206
expr: u32,
194207
nat: u32,
@@ -217,13 +230,7 @@ impl DBCutoff {
217230
// }
218231

219232
pub fn zero() -> Self {
220-
Self {
221-
expr: 0,
222-
nat: 0,
223-
data: 0,
224-
addr: 0,
225-
nat2nat: 0,
226-
}
233+
DBCutoff::default()
227234
}
228235
}
229236

@@ -232,11 +239,11 @@ impl std::ops::Add<DBShift> for DBCutoff {
232239

233240
fn add(self, rhs: DBShift) -> Self::Output {
234241
Self {
235-
expr: self.expr.strict_add_signed(rhs.expr),
236-
nat: self.expr.strict_add_signed(rhs.nat),
237-
data: self.expr.strict_add_signed(rhs.data),
238-
addr: self.expr.strict_add_signed(rhs.addr),
239-
nat2nat: self.expr.strict_add_signed(rhs.nat2nat),
242+
expr: self.expr.strict_add_signed(rhs.expr_shift()),
243+
nat: self.nat.strict_add_signed(rhs.nat_shift()),
244+
data: self.data.strict_add_signed(rhs.data_shift()),
245+
addr: self.expr.strict_add_signed(rhs.addr_shift()),
246+
nat2nat: self.expr.strict_add_signed(rhs.nat2nat_shift()),
240247
}
241248
}
242249
}
@@ -253,6 +260,36 @@ impl From<(u32, u32, u32, u32, u32)> for DBCutoff {
253260
}
254261
}
255262

263+
impl From<(u32, u32)> for DBCutoff {
264+
fn from(value: (u32, u32)) -> Self {
265+
Self {
266+
nat: value.0,
267+
nat2nat: value.1,
268+
..Default::default()
269+
}
270+
}
271+
}
272+
273+
impl From<(u32, u32, u32)> for DBCutoff {
274+
fn from(value: (u32, u32, u32)) -> Self {
275+
Self {
276+
nat: value.0,
277+
data: value.1,
278+
nat2nat: value.2,
279+
..Default::default()
280+
}
281+
}
282+
}
283+
284+
impl From<u32> for DBCutoff {
285+
fn from(value: u32) -> Self {
286+
Self {
287+
addr: value,
288+
..Default::default()
289+
}
290+
}
291+
}
292+
256293
impl std::fmt::Display for DBCutoff {
257294
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
258295
write!(
@@ -271,8 +308,6 @@ pub enum IndexError {
271308
ImproperTag(String),
272309
#[error("Missing Tag {0}")]
273310
MissingTag(String),
274-
#[error("Invalide zero shift")]
275-
ZeroShift,
276311
#[error("Invalide Index: {0}")]
277312
InvalidIndex(#[from] std::num::ParseIntError),
278313
}

0 commit comments

Comments
 (0)