Syntactic, no-delta evaluator for Nat offset constants. This is intentionally weaker than WHNF: it only recognizes already exposed Nat literals/constructors and primitive Nat arithmetic whose arguments are themselves syntactically evaluable. It is used to avoid rewriting closed arithmetic offsets before `try_reduce_nat` can compute them, and to evaluate the literal offset side of `Nat.add`.
(
&mut self,
e: &KExpr<M>,
depth: u16,
)
| 1197 | } else { |
| 1198 | self.env.whnf_no_delta_cheap_cache.insert(key, cur.clone()); |
| 1199 | } |
| 1200 | } |
| 1201 | Ok(cur) |
| 1202 | } |
| 1203 | |
| 1204 | /// Delta unfold: unfold one defined constant. |
| 1205 | pub fn delta_unfold_one( |
| 1206 | &mut self, |
| 1207 | e: &KExpr<M>, |
| 1208 | ) -> Result<Option<KExpr<M>>, TcError<M>> { |
| 1209 | if let Some(unfolded) = self.try_delta_unfold(e)? { |
| 1210 | return Ok(Some(unfolded)); |
| 1211 | } |
| 1212 | // Bare constant |
| 1213 | if let ExprData::Const(id, us, _) = e.data() |
| 1214 | && let Some(KConst::Defn { kind, val, .. }) = self.try_get_const(id)? |
| 1215 | && matches!(kind, DefKind::Definition | DefKind::Theorem) |
| 1216 | { |
| 1217 | self.dump_delta_trace(id, 0, e); |
| 1218 | self.record_delta_target(id); |
| 1219 | let val = val.clone(); |
| 1220 | let us: Vec<_> = us.to_vec(); |
| 1221 | return Ok(Some(self.unfold_const_value(e, &val, &us)?)); |
| 1222 | } |
| 1223 | Ok(None) |
| 1224 | } |
| 1225 | |
| 1226 | /// Try delta-unfold on application head. |
| 1227 | fn try_delta_unfold( |
| 1228 | &mut self, |
| 1229 | e: &KExpr<M>, |
| 1230 | ) -> Result<Option<KExpr<M>>, TcError<M>> { |
| 1231 | let (head, args) = collect_app_spine(e); |
| 1232 | |
| 1233 | let (id, us) = match head.data() { |
| 1234 | ExprData::Const(id, us, _) => (id, us), |
| 1235 | _ => return Ok(None), |
| 1236 | }; |
| 1237 | |
| 1238 | let val = match self.try_get_const(id)? { |
no test coverage detected