Add a #pragma safe
. The programmer can add #pragma safe
to function application expressions.
#pragma safe
causes type pattern checks on function applications to be skipped by renaming calls to wrapper functions with direct calls to implementation functions. The bypasses the pre- and post- conditions but everything still works out.
As a shortcut you can also put #pragma safe
behind blocks. This flags every function application inside the block as safe.
You can also put #pragma safe
at the start of a files.
This will flag every function body block as safe. A shortcut for the block shortcut.
Read much more about this and see examples about #pragma safe
on the wiki.
This merge request also cleans up general pragma parsing to use the handle_pragma
function now everywhere pragma are parsed.