|
do -- TODO, should get these from somewhere inside copilot instead of building these names directly |
|
let idxName = "s" ++ show nm ++ "_idx" |
|
let bufName = "s" ++ show nm |
|
let buflen = genericLength vs :: Integer |
As alluded to in the above comment, we are currently building the names of stream variables in the generated code from hidden, internal knowledge of the Copilot code generator. It would be better and more robust to have the Copilot library itself tell us this information instead. Currently no API exists for obtaining this information, so we will probably need to design something and open an upstream PR.
copilot-verifier/copilot-verifier/src/Copilot/Verifier.hs
Lines 548 to 551 in ea2c64e
As alluded to in the above comment, we are currently building the names of stream variables in the generated code from hidden, internal knowledge of the Copilot code generator. It would be better and more robust to have the Copilot library itself tell us this information instead. Currently no API exists for obtaining this information, so we will probably need to design something and open an upstream PR.