import Base
import ./bits.bend as Bits
import ./math.bend as Math
import ./num.bend as Nm
import ./rat.bend as Rt
import ./set.bend as Se
import ./series.bend as Sr
import ./mlib_linalg.bend as M2

# Mathlib.bend — Lean Mathlib finite-fragment facade over this repo.
#
# What this is: a single publishable entry point that maps the translatable
# part of Lean's Mathlib to Bend2 definitions in this repo. See
# MATHLIB_COVERAGE.md for the full area-by-area table (have / missing /
# impossible). Anything about reals, topology, measure, or infinite
# structures is honestly out of scope (Bend2 has only Nat/U32/F32; F32 is
# axiomatic and unprovable; see README + BEND2_GAP_ANALYSIS.md).
#
# What this file does:
# - thin Mathlib-named wrappers (mlib_*) over existing checked defs
#   (no re-proofs, no redefinitions — import and call);
# - one U32 smoke checksum (mlib_selftest) combining one closed value
#   from each wrapped area, so `bend mathlib.bend` normalizes it;
# - closed-instance laws with definitional proofs ({==}).
#
# Publish: `bend mathlib.bend --publish` (bundles this file + its imports).

# --- wrappers (names are globally unique by mlib_ prefix) ---

def mlib_pop(+x: U32) -> U32:
  Bits.pop(x)

def mlib_pow(+base: U32, +exp: U32) -> U32:
  Math.pow_u32(base, exp)

def mlib_gcd(+a: U32, +b: U32) -> U32:
  Math.gcd(a, b)

def mlib_is_prime(+n: U32) -> Bool:
  Nm.is_prime(n)

def mlib_mod_pow(+base: U32, +exp: U32, +m: U32) -> U32:
  Nm.mod_pow(base, exp, m)

def mlib_trisum_u32(n: Nat) -> U32:
  U32.from_nat(Sr.trisum(n))

def mlib_radd_num(a: Rt.Rat, b: Rt.Rat) -> U32:
  Rt.num_of(Rt.radd(a, b))

def mlib_mat_det_u32(m: M2.Mat2) -> U32:
  U32.from_nat(M2.mmat_det(m))

def mlib_set_size(s: Se.USet) -> U32:
  Se.ssize(s)

# --- smoke checksum: one closed value per area (expected 324) ---
# 3 (pop) + 243 (pow) + 4 (gcd) + 1 (modpow) + 2 (set) + 55 (trisum)
#   + 1 (prime) + 5 (rat 1/2+1/3=5/6 num) + 10 (mat det) = 324.

def mlib_selftest() -> U32:
  a = Bits.pop(7)
  b = Math.pow_u32(3, 5)
  c = Math.gcd(12, 8)
  d = Nm.mod_pow(3, 4, 5)
  e = Se.ssize(Se.sinsert(Se.sinsert(Se.sempty(), 1), 2))
  f = U32.from_nat(Sr.trisum(10n))
  g = Bool.to_u32(Nm.is_prime(7))
  h = Rt.num_of(Rt.radd(Rt.mk_rat(False{}, 1, 2), Rt.mk_rat(False{}, 1, 3)))
  i = U32.from_nat(M2.mmat_det(M2.mmat_example()))
  (a + b + c + d + e + f + g + h + i : U32)

# --- closed laws (all definitional) ---

law mlib_pop_7:
  {mlib_pop(7) == 3 : U32}

def mlib_pop_7():
  {==}

law mlib_pow_3_5:
  {mlib_pow(3, 5) == 243 : U32}

def mlib_pow_3_5():
  {==}

law mlib_gcd_12_8:
  {mlib_gcd(12, 8) == 4 : U32}

def mlib_gcd_12_8():
  {==}

law mlib_prime_7:
  {mlib_is_prime(7) == True{} : Bool}

def mlib_prime_7():
  {==}

law mlib_modpow_345:
  {mlib_mod_pow(3, 4, 5) == 1 : U32}

def mlib_modpow_345():
  {==}

law mlib_trisum_10:
  {mlib_trisum_u32(10n) == 55 : U32}

def mlib_trisum_10():
  {==}

law mlib_radd_1_2_1_3_num:
  {mlib_radd_num(Rt.mk_rat(False{}, 1, 2), Rt.mk_rat(False{}, 1, 3)) == 5 : U32}

def mlib_radd_1_2_1_3_num():
  {==}

law mlib_mat_det_example:
  {mlib_mat_det_u32(M2.mmat_example()) == 10 : U32}

def mlib_mat_det_example():
  {==}

law mlib_set_size_two:
  {mlib_set_size(Se.sinsert(Se.sinsert(Se.sempty(), 1), 2)) == 2 : U32}

def mlib_set_size_two():
  {==}

law mlib_selftest_value:
  {mlib_selftest() == 324 : U32}

def mlib_selftest_value():
  {==}