Method clone

crates/ixon/src/env.rs:345–379

(&self)

  /// The Lean compiler mirror applies the same rule.
  #[cfg(not(target_arch = "riscv64"))]
  pub fn register_hint(&self, addr: Address, hints: ReducibilityHints) {
    fn rank(h: &ReducibilityHints) -> (u8, u32) {
      match h {
        ReducibilityHints::Opaque => (0, 0),
        ReducibilityHints::Abbrev => (1, 0),
        ReducibilityHints::Regular(x) => (2, *x),
      }
    }
    match self.anon_hints.entry(addr) {
      dashmap::mapref::entry::Entry::Occupied(mut e) => {
        if rank(&hints) < rank(e.get()) {
          e.insert(hints);
        }
      },
      dashmap::mapref::entry::Entry::Vacant(e) => {
        e.insert(hints);
      },
    }
  }

  /// Store a structured constant under `addr`.
  ///
  /// Serializes the constant once. With demotion disabled,
  /// the [`LazyConstant`] cache is pre-populated so `get_const` is
  /// free; under [`DEMOTE`] (the default) the structured value is
  /// dropped and the entry costs only its bytes (`get_const` re-parses
  /// per access). Compilation never reads stored constants back, so the
  /// modes differ only in memory footprint and later readers' CPU cost.
  ///
  /// Host-only — see `store_blob`.
  #[cfg(not(target_arch = "riscv64"))]
  pub fn store_const(&self, addr: Address, constant: Constant) {
    self.store_const_demoted(addr, constant, *DEMOTE);
  }

  /// `store_const` with an explicit demotion choice, bypassing
  /// `IX_COMPILE_DEMOTE`. Exists so tests can drive both reprs without
  /// process-global env-var races.