| 203 | }, |
| 204 | ExprData::LetE(_, t, v, b, ..) => { |
| 205 | ground_expr(t, env, univs, binds, stt)?; |
| 206 | ground_expr(v, env, univs, binds, stt)?; |
| 207 | ground_expr(b, env, univs, binds + 1, stt) |
| 208 | }, |
| 209 | ExprData::Proj(name, _, e, _) => { |
| 210 | if !env.contains_key(name) { |
| 211 | return Err(GroundError::Ref(name.clone())); |
| 212 | } |
| 213 | ground_expr(e, env, univs, binds, stt) |
| 214 | }, |
| 215 | ExprData::Lit(..) => Ok(()), |
| 216 | ExprData::Mvar(..) => Err(GroundError::MVar(expr.clone())), |
| 217 | ExprData::Fvar(..) => Err(GroundError::Var(expr.clone(), binds)), |
| 218 | } |
| 219 | } |
| 220 | |
| 221 | fn ground_level( |
| 222 | level: &Level, |
| 223 | univs: &[Name], |
| 224 | stt: &mut GroundState, |
| 225 | ) -> Result<(), GroundError> { |
| 226 | let key = level.clone(); |
| 227 | if stt.univ_cache.contains(&key) { |
| 228 | return Ok(()); |
| 229 | } |
| 230 | stt.univ_cache.insert(key); |
| 231 | match level.as_data() { |
| 232 | LevelData::Zero(_) => Ok(()), |
| 233 | LevelData::Succ(x, _) => ground_level(x, univs, stt), |
| 234 | LevelData::Max(x, y, _) | LevelData::Imax(x, y, _) => { |
| 235 | ground_level(x, univs, stt)?; |