Function decode_syntax

crates/ffi/src/lean_env.rs:723–756

(obj: LeanBorrowed<'_>, cache: &mut Cache<'_>)

fn decode_substring(obj: LeanBorrowed<'_>) -> Substring {
  let s = LeanIxSubstring::from_ctor(obj.as_ctor());
  let str = s.get_obj(0).as_string().to_string();
  let start_pos = LeanNat::to_nat(&s.get_obj(1));
  let stop_pos = LeanNat::to_nat(&s.get_obj(2));
  Substring { str, start_pos, stop_pos }
}

fn decode_source_info(obj: LeanBorrowed<'_>) -> SourceInfo {
  if obj.is_scalar() {
    return SourceInfo::None;
  }
  let si = LeanIxSourceInfo::from_ctor(obj.as_ctor());
  match si.as_ctor().tag() {
    0 => {
      let leading = decode_substring(si.get_obj(0));
      let pos = LeanNat::to_nat(&si.get_obj(1));
      let trailing = decode_substring(si.get_obj(2));
      let end_pos = LeanNat::to_nat(&si.get_obj(3));
      SourceInfo::Original(leading, pos, trailing, end_pos)
    },
    1 => {
      let pos = LeanNat::to_nat(&si.get_obj(0));
      let end_pos = LeanNat::to_nat(&si.get_obj(1));
      let canonical = si.get_num_8(0) != 0;
      SourceInfo::Synthetic(pos, end_pos, canonical)
    },
    tag => unreachable!("Invalid Lean.SourceInfo tag: {tag}"),
  }
}

fn decode_syntax_preresolved(
  obj: LeanBorrowed<'_>,
  cache: &mut Cache<'_>,
) -> SyntaxPreresolved {
  let p = LeanIxSyntaxPreresolved::from_ctor(obj.as_ctor());
  match p.as_ctor().tag() {
    0 => {