Tables in lambda functions?

[LeventErkok]

Currently we don't support tables in lambda-generated functions:

Data.SBV> putStrLn =<< sbv2smt (smtFunction "foo" (\x -> select [1] (0 :: SInteger) (x::SInteger)))
*** Exception: *** Data.SBV.lambda: Unsupported construct.
***
*** Tables.
***   Saw: table0 :: SInteger -> SInteger
***
*** Please request this as a feature at https://github.com/LeventErkok/sbv/issues

This can be supported if we're willing to spit out more than just the function definition itself, but also the table values too. This is a bit difficult since SMTLib doesn't really have a way of creating literal arrays; one declares an array and then asserts certain entries contain the relevant values. But this isn't entirely trivial, since those constants will need to be declared too.

But perhaps we can still support some of these tables, if they're complete constants: By a sequence of array-updates. We should look into this.

Note that another way to do this is to not generate tables at all if we're in Lambda mode. And indeed this is not terribly hard to implement. But it generates horrible code: Every lookup turns into a giant tie-chain. So, it should be avoided. (Try with aes128 encryption for instance, where the output is enormous.)

[LeventErkok]

Need to rethink this

[LeventErkok]

Related issue #666