Convert all enumerations to integers at runtime

We were just doing Bool/Ordering but now generalised to everything where
all the consructors are nullary after erasure

CHANGELOG.md

@@ -23,7 +23,8 @@ Syntax changes:
 Compiler changes:
 
 * Added more optimisations and transformations, particularly on case blocks,
-  and on list-shaped types, so generated code will often be slightly faster.
+  list-shaped types, and enumerations, so generated code will often be slightly
+  faster.
 * Racket codegen now always uses `blodwen-sleep` instead of `idris2_sleep` in
   order to not block the Racket runtime when `sleep` is called.
 * Added `--profile` flag, which generates profile data if supported by a back

src/Compiler/CompileExpr.idr

@@ -273,27 +273,18 @@ builtinNatTree = do
     let b = defs.builtinTransforms
     pure $ builtinNatTree' b.natZNames b.natSNames
 
--- Rewrite case trees on Bool/Ord to be case trees on Integer
--- TODO: Generalise to all finite enumerations
-isFiniteEnum : Name -> Bool
-isFiniteEnum (NS ns (UN n))
-   =  ((n == "True" || n == "False") && ns == basicsNS) -- booleans
-   || ((n == "LT" || n == "EQ" || n == "GT") && ns == eqOrdNS) -- comparison
-isFiniteEnum _ = False
-
-boolHackTree : CExp vars -> CExp vars
-boolHackTree (CConCase fc sc alts def)
-   = let x = traverse toBool alts
+enumTree : CExp vars -> CExp vars
+enumTree (CConCase fc sc alts def)
+   = let x = traverse toEnum alts
          Just alts' = x
               | Nothing => CConCase fc sc alts def in
          CConstCase fc sc alts' def
   where
-    toBool : CConAlt vars -> Maybe (CConstAlt vars)
-    toBool (MkConAlt nm _ (Just tag) [] sc)
-        = do guard (isFiniteEnum nm)
-             pure $ MkConstAlt (I tag) sc
-    toBool _ = Nothing
-boolHackTree t = t
+    toEnum : CConAlt vars -> Maybe (CConstAlt vars)
+    toEnum (MkConAlt nm ENUM (Just tag) [] sc)
+        = pure $ MkConstAlt (I tag) sc
+    toEnum _ = Nothing
+enumTree t = t
 
 -- See if the constructor is a special constructor type, e.g a nil or cons
 -- shaped thing.
@@ -318,13 +309,13 @@ mutual
              Core (CExp vars)
   toCExpTm m n (Local fc _ _ prf)
       = pure $ CLocal fc prf
-  -- TMP HACK: extend this to all types which look like enumerations after erasure
   toCExpTm m n (Ref fc (DataCon tag arity) fn)
-      = if arity == Z && isFiniteEnum fn
-        then pure $ CPrimVal fc (I tag)
-        else -- get full name for readability, and %builtin Natural
-              do cn <- getFullName fn
-                 pure $ CCon fc cn !(dconFlag cn) (Just tag) []
+      = do -- get full name for readability, and %builtin Natural
+           cn <- getFullName fn
+           fl <- dconFlag cn
+           case fl of
+                ENUM => pure $ CPrimVal fc (I tag)
+                _ => pure $ CCon fc cn fl (Just tag) []
   toCExpTm m n (Ref fc (TyCon tag arity) fn)
       = pure $ CCon fc fn TYCON Nothing []
   toCExpTm m n (Ref fc _ fn)
@@ -518,7 +509,7 @@ mutual
                def <- getDef n alts
                if isNil cases
                   then pure (fromMaybe (CErased fc) def)
-                  else pure $ boolHackTree $ !builtinNatTree $
+                  else pure $ enumTree $ !builtinNatTree $
                             CConCase fc (CLocal fc x) cases def
   toCExpTree' n (Case _ x scTy alts@(DelayCase _ _ _ :: _))
       = throw (InternalError "Unexpected DelayCase")

src/Core/CompileExpr.idr

@@ -20,6 +20,7 @@ data ConInfo = DATACON -- normal data constructor
              | TYCON -- normal type constructor
              | NIL -- nil of a list shaped thing
              | CONS -- cons of a list shaped thing
+             | ENUM -- part of an enumeration
 
 export
 Show ConInfo where
@@ -27,6 +28,7 @@ Show ConInfo where
   show TYCON   = "[tycon]"
   show NIL     = "[nil]"
   show CONS    = "[cons]"
+  show ENUM    = "[enum]"
 
 export
 Eq ConInfo where
@@ -34,6 +36,7 @@ Eq ConInfo where
   TYCON == TYCON = True
   NIL == NIL = True
   CONS == CONS = True
+  ENUM == ENUM = True
   _ == _ = False
 
 mutual

src/Core/TTC.idr

@@ -621,6 +621,7 @@ TTC ConInfo where
   toBuf b TYCON = tag 1
   toBuf b NIL = tag 2
   toBuf b CONS = tag 3
+  toBuf b ENUM = tag 4
 
   fromBuf b
       = case !getTag of
@@ -628,6 +629,7 @@ TTC ConInfo where
              1 => pure TYCON
              2 => pure NIL
              3 => pure CONS
+             4 => pure ENUM
              _ => corrupt "ConInfo"
 
 mutual

src/TTImp/ProcessData.idr

@@ -295,10 +295,27 @@ calcListy fc cs@[_, _]
          pure True
 calcListy _ _ = pure False
 
+calcEnum : {auto c : Ref Ctxt Defs} ->
+           FC -> List Constructor -> Core Bool
+calcEnum fc cs
+    = if !(allM isNullary cs)
+         then do traverse_ (\c => setFlag fc c (ConType ENUM)) (map name cs)
+                 pure True
+         else pure False
+  where
+    isNullary : Constructor -> Core Bool
+    isNullary c
+        = do defs <- get Ctxt
+             pure $ asNil !(normalise defs [] (type c))
+
 calcConInfo : {auto c : Ref Ctxt Defs} ->
               FC -> List Constructor -> Core ()
 calcConInfo fc cons
-   = ignore $ calcListy fc cons
+   = do False <- calcListy fc cons
+           | True => pure ()
+        False <- calcEnum fc cons
+           | True => pure ()
+        pure ()
      -- ... maybe more to come? The Bool just says when to stop looking
 
 export