Implement toExpr for enums

src/Cryptol/Eval/Concrete.hs

@@ -20,6 +20,8 @@ module Cryptol.Eval.Concrete
   ) where
 
 import Control.Monad (guard, zipWithM, foldM, mzero)
+import Data.Foldable (foldl')
+import Data.List (find)
 import Data.Ratio(numerator,denominator)
 import Data.Word(Word32, Word64)
 import MonadLib( ChoiceT, findOne, lift )
@@ -86,8 +88,19 @@ toExpr prims t0 v0 = findOne (go t0 v0)
                          Enum {} -> panic "toExpr" ["Enum vs Record"]
                    f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar c) ts
                 in pure (EApp f (ERec efs))
-      -- XXX: enum types
-      -- (TVNewtype nt ts (TVEnum cs), VEnum) -> ...
+      (TVNewtype nt ts (TVEnum tfss), VEnum i vfs) ->
+        case Map.lookup i tfss of
+          Nothing -> mismatch -- enum constructor not found
+          Just tfs ->
+            do guard (length tfs == length vfs)
+               c <- case ntDef nt of
+                      Struct {} -> panic "toExpr" ["Enum vs Record"]
+                      Enum cons ->
+                        case find (\con -> nameIdent (ecName con) == i) cons of
+                          Just con -> pure (ecName con)
+                          Nothing -> mismatch
+               let f = foldl' (\x t -> ETApp x (tNumValTy t)) (EVar c) ts
+               foldl' EApp f <$> (zipWithM go tfs =<< lift (sequence vfs))
 
       (TVTuple ts, VTuple tvs) ->
         do guard (length ts == length tvs)

tests/enum/CheckEnumPartialError.cry

@@ -0,0 +1,35 @@
+enum Maybe a = Nothing | Just a
+
+maybeEqual : {a} (Eq a) => Maybe a -> Maybe a -> Bit
+maybeEqual m1 m2 =
+  case m1 of
+    Just x1 ->
+      case m2 of
+        Just x2 -> x1 == x2
+        Nothing -> False
+    Nothing ->
+      case m2 of
+        Just x2 -> False
+        Nothing -> True
+
+maybeMapBad1 : {a, b} (a -> b) -> Maybe a -> Maybe b
+maybeMapBad1 f m =
+  case m of
+    Just x -> Just (f x)
+
+maybeMapBad2 : {a, b} (a -> b) -> Maybe a -> Maybe b
+maybeMapBad2 f m =
+  case m of
+    Nothing -> Nothing
+
+maybeMapBad1Prop : Maybe [8] -> Bit
+property maybeMapBad1Prop m =
+  maybeEqual
+    (maybeMapBad1 (\x -> x + 1) (maybeMapBad1 (\x -> x + 1) m))
+    (maybeMapBad1 (\x -> x + 2) m)
+
+maybeMapBad2Prop : Maybe [8] -> Bit
+property maybeMapBad2Prop m =
+  maybeEqual
+    (maybeMapBad2 (\x -> x + 1) (maybeMapBad2 (\x -> x + 1) m))
+    (maybeMapBad2 (\x -> x + 2) m)

tests/enum/CheckEnumPartialError.icry

@@ -0,0 +1,3 @@
+:l CheckEnumPartialError.cry
+:set-seed 42
+:check

tests/enum/CheckEnumPartialError.icry.stdout

@@ -0,0 +1,23 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+property maybeMapBad1Prop Using random testing.
+Testing... ERROR for the following inputs:
+maybeMapBad1Prop Nothing ~> ERROR
+Missing `case` alternative for constructor `Nothing`.
+-- Backtrace --
+Main::maybeMapBad1 called at CheckEnumPartialError.cry:28:34--28:46
+Main::maybeMapBad1 called at CheckEnumPartialError.cry:28:6--28:18
+Main::maybeEqual called at CheckEnumPartialError.cry:27:3--27:13
+Main::maybeMapBad1Prop
+<interactive>::it
+property maybeMapBad2Prop Using random testing.
+Testing... ERROR for the following inputs:
+maybeMapBad2Prop Just 0xa6 ~> ERROR
+Missing `case` alternative for constructor `Just`.
+-- Backtrace --
+Main::maybeMapBad2 called at CheckEnumPartialError.cry:34:34--34:46
+Main::maybeMapBad2 called at CheckEnumPartialError.cry:34:6--34:18
+Main::maybeEqual called at CheckEnumPartialError.cry:33:3--33:13
+Main::maybeMapBad2Prop
+<interactive>::it