Build a canonical-form Int literal expression: `Int.ofNat n` for n ≥ 0, `Int.negSucc (|n| - 1)` for n < 0. Used as the return form of native Int reductions so subsequent delta+iota steps see the value in its ctor-headed shape (letting `decNonneg` / `Int.rec` iota-reduce in the caller).
( tc: &mut TypeChecker<'_, M>, v: IntVal, )
| 3034 | args: &[KExpr<M>], |
| 3035 | ) -> Result<Option<KExpr<M>>, TcError<M>> { |
| 3036 | if args.len() < 2 { |
| 3037 | return Ok(None); |
| 3038 | } |
| 3039 | |
| 3040 | let wa = self.whnf(&args[0])?; |
| 3041 | let wb = self.whnf(&args[1])?; |
| 3042 | let Some(a_val) = extract_int_lit(&wa, &self.prims) else { |
| 3043 | return Ok(None); |
| 3044 | }; |
| 3045 | let Some(b_val) = extract_int_lit(&wb, &self.prims) else { |
| 3046 | return Ok(None); |
| 3047 | }; |
| 3048 | |
| 3049 | let a = intern_int_lit(self, a_val); |
| 3050 | let b = intern_int_lit(self, b_val); |
| 3051 | if a.hash_key() == args[0].hash_key() && b.hash_key() == args[1].hash_key() |
| 3052 | { |
| 3053 | return Ok(None); |
| 3054 | } |
| 3055 | |
| 3056 | let head_id = if *addr == self.prims.int_dec_eq.addr { |
| 3057 | self.prims.int_dec_eq.clone() |
| 3058 | } else if *addr == self.prims.int_dec_le.addr { |
| 3059 | self.prims.int_dec_le.clone() |
| 3060 | } else { |
| 3061 | self.prims.int_dec_lt.clone() |
| 3062 | }; |
| 3063 | let head = self.intern(KExpr::cnst(head_id, Box::new([]))); |
| 3064 | let mut result = self.intern(KExpr::app(head, a)); |