Handling primitive Fortran values symbolically.

There are a few challenges that this module attempts to solve:

Fortran uses fixed-width machine integers and floating point reals. Sometimes we might want to reason about these directly (which is supported by SBV and therefore feasible). However, sometimes they get in the way of the logic and we just want to pretend that they're the pure mathematical values that they approximate. For example floating point addition obeys very few algebraic laws, so most theorems about real numbers don't hold at all for floating point numbers.

In addition, Fortran's boolean values are actually arbitrary signed integers. If we treat all boolean values symbolically as bit-vectors, logic can become very slow; so it might be best to pretend that all booleans are single bits. However, sometimes we might want to verify properties that rely on the actual bit-vector representation of booleans.

This module deals with these problems by abstracting over the choices: the user should be able to choose which representation they want to use for each primitive data type.

The user provides a PrimReprSpec which specifies how each data type should be treated. Some examples are provided: prsPrecise treats all values precisely as they are represented in the Fortran program. This makes logic slow and makes it very difficult to prove many things, but it is most accurate. On the other hand, prsIdealized treats all values as their idealized mathematical equivalents. This makes logic fast and lots intuitive properties can be proved easily. However, these properties often will not hold in actual running Fortran programs: sometimes in weird edge cases and sometimes in sensible-seeming executions. It would be interesting future work to provide an analysis that helps to determine which of the two applies to a particular program!