search

au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

Shallow embedding of ArrayPut and ArrayTake #383

Open amblafont opened 4 years ago

amblafont commented 4 years ago

This PR implements the shallow embedding of ArrayPut, which is enough to compile the shallow embedding the led driver..

This PR also implements the shallow embedding of ArrayTake, but it couldn't be tested, as it seems the compilation of ArrayTake is not yet implemented (yielding TODO fvIP: PArrayTake unimplemented)

zilinc commented 3 years ago

Many of the missing things are on my wip-reftypes branch. Since on master there's no typechecking for array operations, many things were left out as they weren't needed or didn't make sense.