From 2eafe7b1c5e93c375ffc42f0a9e8efbd64b69f54 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 30 Jan 2018 02:33:54 +0000
Subject: 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
---
 src/initial_check.mli | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/initial_check.mli')

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
-- 
cgit v1.2.3