VerifiedCompilation Untyped Purity functions

[ramsay-t]

The UFloatDelay translation relation requires a test that a term isPure. This exists in Haskell but needs defining in Agda. Currently it is a null type that accepts any term, so this needs to be improved to match the Haskell definition at least (and perhaps be more carefully considered?)