Generate functions from enums to numbers and vice versa

For an enumeration type T, we can create a function T_of_num and num_of_T which convert from the enum to and from a numeric type. The numeric type is range(0, n) where n is the number of constructors in the enum minus one. This makes sure the conversion is type safe, but maybe this is too much of a hassle.

It would be possible to automatically overload all these functions into generic to_enum and from_enum as in Haskell's Enum typeclass, but we don't do this yet.

Currently these functions affect a few lem test cases, but I think that is only because they are tested without any prelude functions and pattern rewrites require a few functions to be defined

What is really broken is if one tries to generate these functions like

enum x = A | B | C

function f A = 0
function f B = 1
function f C = 2

the rewriter really doesn't like function clauses like this, and it seems really hard to fix properly (I tried and gave up), this is a shame as the generation code is much more succinct with definitions like above

1 files changed, 8 insertions, 0 deletions

diff --git a/src/initial_check.mli b/src/initial_check.mli
index 755da523..197139f4 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -51,9 +51,17 @@
 open Ast
 open Ast_util
 
+(* Generate undefined_T functions for every type T *)
 val opt_undefined_gen : bool ref
+
+(* Allow # in identifiers when set, like the GHC option of the same name *)
 val opt_magic_hash : bool ref
 
+(* When true enums can be automatically casted to range types and
+   back.  Otherwise generated T_of_num and num_of_T functions must be
+   manually used for each enum T *)
+val opt_enum_casts : bool ref
+                          
 (* This is a bit of a hack right now - it ensures that the undefiend
    builtins (undefined_vector etc), only get added to the ast
    once. The original assumption in sail is that the whole AST gets