mit-plv / bbv

Bedrock Bit Vector Library
MIT License
27 stars 23 forks source link

Extracting [hexDigitToN] in Haskell creates Data.Bits.testBit and Data.Char.ord #11

Open vmurali opened 6 years ago

vmurali commented 6 years ago

Since the generated Haskell does not import Data.Bits.testBit and Data.Char.ord, the overall compilation of the Haskell program fails. Any ideas to avoid generating these functions during Extraction?

samuelgruetter commented 6 years ago

It looks like there's no option to specify additional imports to be put at the top of the generates haskell files, so you'd have to add the required imports yourself afterwards (eg like Tej).

But maybe if you're lucky you could just use something like Extract Constant Ox => someHaskellCode, where someHaskellCode only uses functions imported by default and converts a hex sring to an int, maybe using readHex?