Normalize a level (reduce max/imax where possible)
(&mut self, id: LevelId)
| 144 | |
| 145 | /// Normalize a level (reduce max/imax where possible) |
| 146 | pub fn normalize(&mut self, id: LevelId) -> LevelId { |
| 147 | let level = self.get(id).unwrap().clone(); |
| 148 | |
| 149 | match level { |
| 150 | Level::Succ(inner) => { |
| 151 | let normalized = self.normalize(inner); |
| 152 | if let Some(Level::Const(n)) = self.get(normalized) { |
| 153 | return self.constant(n + 1); |
| 154 | } |
| 155 | self.succ(normalized) |
| 156 | } |
| 157 | Level::Max(a, b) => { |
| 158 | let a_norm = self.normalize(a); |
| 159 | let b_norm = self.normalize(b); |
| 160 | |
| 161 | // max(n, m) = max(n, m) for constants |
| 162 | if let (Some(Level::Const(n)), Some(Level::Const(m))) = |
| 163 | (self.get(a_norm), self.get(b_norm)) |
| 164 | { |
| 165 | return self.constant((*n).max(*m)); |
| 166 | } |
| 167 | |
| 168 | self.max(a_norm, b_norm) |
| 169 | } |
| 170 | Level::IMax(a, b) => { |
| 171 | let a_norm = self.normalize(a); |
| 172 | let b_norm = self.normalize(b); |
| 173 | |
| 174 | // imax(0, u) = 0 |
| 175 | if let Some(Level::Zero) = self.get(b_norm) { |
| 176 | return self.zero(); |
| 177 | } |
| 178 | |
| 179 | // imax(n, m) = max(n, m) for constants |
| 180 | if let (Some(Level::Const(n)), Some(Level::Const(m))) = |
| 181 | (self.get(a_norm), self.get(b_norm)) |
| 182 | { |
| 183 | return self.constant((*n).max(*m)); |
| 184 | } |
| 185 | |
| 186 | self.imax(a_norm, b_norm) |
| 187 | } |
| 188 | _ => id, |
| 189 | } |
| 190 | } |
| 191 | } |
| 192 | |
| 193 | impl Default for LevelArena { |