FFI bitflags

Stream: lean4

[Thomas Vigouroux]

Hey there,

I am trying to map a C bitflag construct to Lean.

What it the recommended way to do so ?

Let's assume the C side looks like so:

enum Foo {
  A = 1
  B = 2
  C = 4
}

[Thomas Vigouroux]

I have tried making an inductive on the Lean side, a marking constructors as extern:

inductive Foo where
| A
| B
| C

attribute [extern "A"] Foo.A;

[Henrik Böving]

I would probably write

inductive Foo where
| A
| B
| C

together with code to convert from and to Foo, https://github.com/tydeu/lean4-alloy has some machinery to make this more convenient. If that conversion function is your bottleneck you're going to have solved a lot of other problems already :D

[Mario Carneiro]

a bitflag does not have the same semantics as a lean inductive

[Mario Carneiro]

for example 7 is a legal value of enum Foo

[Thomas Vigouroux]

Henrik Böving said:

I would probably write

inductive Foo where
| A
| B
| C

together with code to convert from and to Foo, https://github.com/tydeu/lean4-alloy has some machinery to make this more convenient. If that conversion function is your bottleneck you're going to have solved a lot of other problems already :D

I'll look into that, i'll be probably easier this way

[Thomas Vigouroux]

Mario Carneiro said:

a bitflag does not have the same semantics as a lean inductive

How would you do it then ?

[Henrik Böving]

Yeah Mario is right, if you decide to | them together you porbably want to use UInt8 constants with some additional machinery

[Mario Carneiro]

so a more accurate lean representation would be

structure foo where
  A : Bool
  B : Bool
  C : Bool

[Thomas Vigouroux]

Oh, and have some conversion machinery on the C side ?

[Henrik Böving]

Though that would actually need to allocate unlike a UInt8 no?

[Mario Carneiro]

if you want to save space on the lean side you can use UIntN but there will be overhead regardless