Function nat_env

crates/kernel/src/whnf.rs:3637–3803

Build a Nat env with Nat, Nat.zero, Nat.succ, Nat.rec, and Nat.sub. Nat.sub is defined as a primitive that the kernel's try_reduce_nat handles, but also has a delta-unfoldable body using Nat.rec (to test reduction order).

()

  fn walk_literal_char_list(
    &mut self,
    list: &KExpr<M>,
    out: &mut String,
  ) -> Result<bool, TcError<M>> {
    let mut cur = list.clone();
    loop {
      let Some(w) = self.whnf_prim_arg(&cur)? else {
        return Ok(false);
      };
      let (head, args) = collect_app_spine(&w);
      let ExprData::Const(id, _, _) = head.data() else {
        return Ok(false);
      };
      // List.nil.{u} α
      if id.addr == self.prims.list_nil.addr {
        return Ok(args.len() == 1);
      }
      // List.cons.{u} α head tail
      if id.addr != self.prims.list_cons.addr || args.len() != 3 {
        return Ok(false);
      }
      let elem = match self.char_lit_value(&args[1]) {
        Some(c) => Some(c),
        None => match self.whnf_prim_arg(&args[1])? {
          Some(we) => self.char_lit_value(&we),
          None => None,
        },
      };
      let Some(c) = elem else {
        return Ok(false);
      };
      out.push(c);
      cur = args[2].clone();
    }
  }

  /// Recognize the kernel's native char-value form: `Char.ofNat
  /// <Nat-lit>` where the literal is a valid Unicode scalar value.
  /// (`char::from_u32` rejects exactly the complement of
  /// `Nat.isValidChar`: surrogates and codepoints above `0x10FFFF`.)
  /// Purely syntactic — no reduction, and no spine allocation: this
  /// runs on every main-whnf-loop iteration.
  pub(super) fn char_lit_value(&self, e: &KExpr<M>) -> Option<char> {
    // Exactly `App(Const(Char.ofNat), Nat-lit)` — a nested App head
    // (over-application) or any other shape is not a char value.
    let ExprData::App(f, arg, _) = e.data() else {
      return None;
    };
    let ExprData::Const(id, _, _) = f.data() else {
      return None;
    };
    if id.addr != self.prims.char_of_nat.addr {
      return None;
    }
    let ExprData::Nat(n, _, _) = arg.data() else {
      return None;
    };
    let cp = n.to_u64()?;
    u32::try_from(cp).ok().and_then(char::from_u32)