config.toml

rustc_args = "$RUST_SRC_PATH/libcore/lib.rs"

targets = [
  'core.«\[T\] as core.slice.SliceExt».(binary_search|get)',
  #fixedbitset
  "core.marker.PhantomData", "core.marker.Copy", "core.iter.iterator.Iterator",
  "core.«&'a u32 as core.ops.BitAnd<u32>»",
  "core.«u32 as core.clone.Clone»",
  #ref
  "core.«i32 as core.default.Default»",
  'core.ops.Range\w*',
]

# items axiomatized in pre.lean
ignore = [
  # items axiomatized in pre.lean
  "core.ops.FnOnce", "core.ops.FnMut", "core.ops.Fn",
  'core.option.Option',
  'core.intrinsics.(.*_with_overflow|overflowing_.*)',
  "core.mem.swap",
  'core.«\[T\] as core.slice.SliceExt».len',
  'core.[iu]size.(min_value|overflowing_sh.)',
  'core.num.wrapping.shift_max.platform.[iu]size',
]

fail = [
  # marker traits that influence static semantics
  "core.marker.Unsize", "core.ops.CoerceUnsized",
  # big caches, won't work anyway without floats
  "core.num.flt2dec.strategy.grisu.CACHED_POW10", "core.num.dec2flt.table.POWERS",
  # way too big with naive if compilation
  'core.«\(A, B, C, D, E.*',
  'core.«.* as core.iter.range.Step».steps_between',
  'core.«core.iter.range.StepBy<A, core.ops.Range<A>> as core.iter.iterator.Iterator».next',
  'core.«core.num.flt2dec.decoder.Decoded as core.cmp.PartialEq».*',
  'core.num.dec2flt.parse.eat_digits',
  'core.str.next_code_point(_reverse)?',
  'core.str.pattern.TwoWaySearcher.(reverse_)?maximal_suffix',
  'core.«core.hash.sip.Sip..Rounds as core.hash.sip.Sip».[cd]_rounds',
  'core.num.diy_float.Fp.normalize',
  # broken recursion detection -- would fail anyway
  'core.ops.Carrier',
  # field/method name clash
  'core.str.Utf8Error.valid_up_to'
]

# unsafe functions that rely on other definitions and thus have to be replaced inline
[replace]
"core.«[T] as core.ops.Index<core.ops.Range<usize>>».index" = """
section
open core.ops

/-
/// Implements slicing with syntax `&self[begin .. end]`.
///
/// Returns a slice of self for the index range [`begin`..`end`).
///
/// This operation is `O(1)`.
///
/// # Panics
///
/// Requires that `begin <= end` and `end <= self.len()`,
/// otherwise slicing will panic.
-/
definition core.«[T] as core.ops.Index<core.ops.Range<usize>>».index {T : Type₁} (self : slice T) (index : Range usize) : sem (slice T) :=
sem.guard (Range.start index ≤ Range.«end» index ∧ Range.«end» index ≤ list.length self)
$ return (list.firstn (Range.«end» index - Range.start index) (list.dropn (Range.start index) self))

end"""

"core.«[T] as core.ops.IndexMut<core.ops.Range<usize>>».index_mut" = """
section
open core.ops

/-
/// Implements mutable slicing with syntax `&mut self[begin .. end]`.
///
/// Returns a slice of self for the index range [`begin`..`end`).
///
/// This operation is `O(1)`.
///
/// # Panics
///
/// Requires that `begin <= end` and `end <= self.len()`,
/// otherwise slicing will panic.
-/
definition core.«[T] as core.ops.IndexMut<core.ops.Range<usize>>».index_mut {T : Type₁} (self : slice T) (index : Range usize) : sem (lens (slice T) (slice T) × slice T) :=
sem.guard (Range.start index ≤ Range.«end» index ∧ Range.«end» index ≤ list.length self)
$ return (lens.mk
    (λ self, return $ list.firstn (Range.«end» index - Range.start index) (list.dropn (Range.start index) self))
    (λ self new, return $ list.firstn (Range.start index) self ++ new ++ list.dropn (Range.end index) self),
    self)

end"""

[traits."core.slice.SliceExt"]
# only method called from default methods (`is_empty`), everything else should be static calls
only = ["len"]