FStarLang / karamel

KaRaMeL is a tool for extracting low-level F* programs to readable C code
Apache License 2.0
394 stars 58 forks source link

Extend support for type abbreviations #439

Closed R1kM closed 2 months ago

R1kM commented 2 months ago

This PR extends support for type abbreviations to support aliases to other types that are lifetime parametric.

Consider the following output, which is similar to what happens in HACL-rs

pub type uint8_4p <`a> = &'a mut [u8];
pub type bufx4 = uint8_4p;

This will not compile, as both bufx4 and uint8_4p should be indexed by a lifetime. This PR will detect that uint8_4p is parametric in a lifetime, and therefore generate pub type bufx4 <'a> = uint8_4p <'a>;.