Conditional compilation

[stepancheg]

trafficstars

Rust

Rust has AST-level preprocessor, e. g.

#[cfg(unix)]
struct UnixSocket {}

or

#[cfg(target_pointer_width = 32)]
fn copy_memory() {}

Which means that element is dropped from AST before typechecking if configuration does not match.

Sometimes it leads to problems like program is compiled on one OS and cannot be compiled on other, but generally it is needed because not everything can be implemented everywhere.

Idris

For Idris it would be helpful to be able to able to specify AST filters at least by

• codegen (to implement functions differently for different codegens)
• compiler version (to be able to implement backwards-incompatible changes in the standard library)
• perhaps OS/CPU filters, but they should be used carefully because generally generated code is identical for any target environment, even for RefC codegen

Why

To have more flexibility implementing low level utilities.

Consider Buffer type. Currently it is implemented as a compiler builtin in all three codegens (node, RefC, scheme). But it does not have to be. For example, on RefC we could implement it purely in Idris. So if we had cfg filters we could do something like this:

%cfg "cg = RefC"
export
record Buffer where
  data: GCPtr Bits8
  size: Size

%cfg "cg != RefC"
export
data Buffer : Type where [external]

[Russoul]

I wonder how much one can do already making use of this file: https://github.com/idris-lang/Idris2/blob/efcf44e8ba0770c234952b7a65c2d78ce725b197/libs/base/System/Info.idr#L1 and elaborator reflection.

[edwinb]

One thing I've wanted in the past is the ability to pick a definition according to the code generator in use. I've never worked out the details though.

One difficulty with the example given is that code generation happens after type checking, and type checking is independent of which code generator will be used. So having alternative data types according to the code generator in use will be tricky.