diekmann
commented
8 years ago TODOs: Asses where safe versions of Isabelle-generated functions can be exported without cluttering the code with error handling. If Isabelle-generated functions are called wrongly, then this is a coding error and an exception is fine. If functions are given an unsupported input at runtime and we need to explain to the user what the error was, we probably want safe functions. What does Isabelle Monad syntax provide? Functions that should only be exported in their safe version:
- Isabelle.rewrite_Goto
- Isabelle.map_of_ipassmt
The fffuu Haskell tool fails with the error message "undefined" if some precondition of the Isabelle-generated code does not hold. For example, Isabelle assumes that an ipassmt does not have wildcard interface names in it. For safety reasons, the Isabelle-generated code checks preconditions at runtime. If it fails, it just aborts with "undefined". There are many different cases how this undefined can be triggered. It is almost impossible to debug which "undefined" triggered. Feature request: human-readable error messages for each undefined!