LeventErkok/sbv — Issue #32: Easier code generation with uninterpreted functions
Author: LeventErkok
Created: 2011-11-28 19:28:34+00:00
State: open
Labels: Nice to have

For code generation with uninterpreted functions, it'd be nicer if we had a construct like:

foo x y z = cgUninterpret "foo" x y z $ (x+y)*z

which would uninterpret the function value during code generation, but otherwise would make it available during simulation/verification. We should be able to implement this with the existing machinery of uninterpreted functions, barring some design choices.. Would be nice to explore..