A few notes on Lean4 => C

Lean4ToC.md

Simple Arithmetic

This Lean4 program

instance FloatHasNeg : HasNeg Float := ⟨λ x => 0 - x⟩
instance HasPowFloatNat : HasPow Float Nat := ⟨λ x y => x ^ (y.toFloat)⟩


def addNats : Nat → Nat → Nat
| x, y => x + y

def addInts : Int → Int → Int
| x, y => x + y

-- N.B., no signed bounded Int types currently
def addUInt64s : UInt64 → UInt64 → UInt64
| x, y => x + y

-- N.B., Float = 64bit float
def addFloats : Float → Float → Float
| x, y => x + y

def quadraticFormula (a b c: Float) : (Float × Float) :=
let ans1 := (-b + (b ^ 2 - 4 * a * c).sqrt) / (2 * a);
let ans2 := (-b - (b ^ 2 - 4 * a * c).sqrt) / (2 * a);
(ans1, ans2)


def main : IO Unit := do
IO.println (addNats 0 1);
IO.println (addInts 0 1);
IO.println (addUInt64s 0 1);
IO.println (addFloats 0 1);
IO.println (quadraticFormula 1 (-2) (-3));
pure ()

compiles to this C file.

Interestingly, where applicable you get versions of the functions for either boxed or unboxed arguments.

Arithmetic with Structs

This Lean4 program

instance HasPowFloatNat : HasPow Float Nat := ⟨λ x y => x ^ (y.toFloat)⟩


structure Cartesian :=
(x : Float)
(y : Float)

structure Polar :=
(r : Float)
(θ : Float)



namespace Cartesian

def distance (p1 p2 : Cartesian) : Float :=
((p1.x - p2.x) ^ 2 + (p1.y - p2.y) ^ 2).sqrt

def toPolar (p : Cartesian) : Polar :=
{r := (p.x ^ 2 + p.y ^ 2).sqrt,
 θ := if p.x == 0 then 90 else (p.y / p.x).atan
}

end Cartesian

namespace Polar

def distance (p1 p2 : Polar) : Float :=
(p1.r ^ 2 + p2.r ^ 2 - (2 * p1.r * p2.r * (p2.θ - p1.θ).cos)).sqrt

def toCartesian (p : Polar) : Cartesian :=
{x := p.r * p.θ.cos, 
 y := p.r * p.θ.sin
}

end Polar

def main : IO Unit := do
let p1 : Cartesian := {x := 3, y := 4};
let p2 : Polar := p1.toPolar;
IO.println $ "(3,4) in cartesian is (" ++ p2.r.toString ++ ", " ++ p2.θ.toString ++ ") in polar";
pure ()

compiles to this C file.

Lean4 Core C Files

All the generated C programs appear to import lean.h and obviously depend on the Lean4 runtime.

I'd have to spend more time understanding the constraints we're hoping to meet w.r.t. dependencies/design/etc for an embedded system/robot. (Years ago I tinkered around with getting a project running in an SGX enclave, which obviously has lots of restrictions on what can be used, but I haven't actually written embedded C or similar in about a decade as a Freshman xD).

32 bit support?

Yes? It seems like things are set up to work on 32- or 64-bit systems: see C function lean_system_platform_nbits and the Lean4 function System.Platform.getNumBits which uses it under the hood.

However, there are no 32-bit floats at the moment in Lean4 =\ Float is implicitly a double. Probably not that hard to add to Lean4 though.