Add Extern and Intrinsic body types

[N1ark]

Add two variants to Body: Extern(string) and Intrinsic(string)! On the OCaml side, a body isn't just a 'body option anymore: we instead properly translate the Body enum, to give more information to the client.

For now intrinsics are just strings rather than an enum, as I don't have the time to do that part. There is also the question of how we make this enum make sense: some intrinsics actually never get lowered into a function call, and a few of them disappear through the compilation pipeline.

One thing we lose with this change is that we can't get the name of the intrinsic's arguments. This isn't a big deal but in Soteria I generate intrinsic definitions from the ULLBC output, and having names for the arguments is super useful. Maybe we could make a new Argument type that stores a type, optional name (and an ArgAbi?) to keep this information? And then FunSig.inputs would be a Vec<Arg> instead. Let me know.

Fixes #982
First step towards #864

ci: use AeneasVerif/aeneas#919
ci: use AeneasVerif/eurydice#395

[Nadrieril]

Love this, tyvm :)

[Nadrieril]

Re argument names, we can't change FunSig because it's used in TyKind::FnPtr. I'm open to finding a solution though, argument names are useful documentation to preseve.

[N1ark]

Re argument names, we can't change FunSig because it's used in TyKind::FnPtr. I'm open to finding a solution though, argument names are useful documentation to preseve.

options:

1. we could make Arg.name an Option<String>; we don't always have names for locals anyways so it's consistent
2. FnSig<Meta> with inputs: Vec<(Ty, Meta)> where Meta is either () or String
3. add a field arg_names: Vec<String> to FunDecl

i think I am happy with either of the three options

[Nadrieril]

How about arg_names: Vec<String> inside Body::Extern and Body::Intrinsic? We could even unify the two variants if useful since they're semantically pretty similar (you tell me what's most useful for you).

[N1ark]

i think i prefer both as separate variants just because it makes matching on the enum easier, and i handle both cases separately anyways

yes this sounds good, ill do it now :)

[N1ark]

This is ready :D @Nadrieril

[Nadrieril]

you could derive that visitor on body, no?

[N1ark]

hmm probably, but anyways this will change in #1102 where the visitor won't be possible, so i'd rather leave this as is

[Nadrieril]

sounds good

[N1ark]

Re argument names, we can't change FunSig because it's used in TyKind::FnPtr. I'm open to finding a solution though, argument names are useful documentation to preseve.

maybe that could change ?
rust-lang/rfcs#3955