Concrete evaluation for case

src/Cryptol/Backend/Monad.hs

@@ -422,6 +422,7 @@ data EvalError
   | BadRoundingMode Integer              -- ^ Invalid rounding mode
   | BadValue String                      -- ^ Value outside the domain of a partial function.
   | NoMatchingPropGuardCase String    -- ^ No prop guard holds for the given type variables.
+  | NoMatchingConstructor String         -- ^ Missing `case` alternative
   | FFINotSupported Name                 -- ^ Foreign function cannot be called
   | FFITypeNumTooBig Name TParam Integer -- ^ Number passed to foreign function
                                          --   as a type argument is too large
@@ -455,6 +456,10 @@ instance PP EvalError where
         <+> integer n
       , text "in type parameter" <+> pp p <+> "of function" <+> pp f
       , text "type arguments must fit in a C `size_t`" ]
+    NoMatchingConstructor con -> vcat
+      [ "Missing `case` alternative for constructor" <+> backticks (text con)
+                                                     <.> "."
+      ]
 
 instance Show EvalError where
   show = show . pp

src/Cryptol/Eval.hs

@@ -161,6 +161,16 @@ evalExpr sym env expr = case expr of
      b <- fromVBit <$> eval c
      iteValue sym b (eval t) (eval f)
 
+  ECase e as d -> {-# SCC "evalExpr->ECase" #-} do
+    val <- eval e
+    let (con,fs) = fromVEnum val
+    case Map.lookup con as of
+      Just rhs -> evalCase rhs fs
+      Nothing ->
+        case d of
+          Just rhs -> evalCase rhs [pure val]
+          Nothing  -> raiseError sym (NoMatchingConstructor $! unpackIdent con)
+
   EComp n t h gs -> {-# SCC "evalExpr->EComp" #-} do
       let len  = evalNumType (envTypes env) n
       let elty = evalValType (envTypes env) t
@@ -230,6 +240,10 @@ evalExpr sym env expr = case expr of
   {-# INLINE eval #-}
   eval = evalExpr sym env
   ppV = ppValue sym defaultPPOpts
+  evalCase (CaseAlt xs e) vs =
+    do let addVar env' ((x,_),v) = bindVar sym x v env'
+       newEnv <- foldM addVar env (zip xs vs)
+       evalExpr sym newEnv e
 
 -- | Checks whether an evaluated `Prop` holds
 checkProp :: Prop -> Bool

src/Cryptol/Eval/Reference.lhs

@@ -224,6 +224,11 @@ Operations on Values
 > fromVRecord (VRecord fs) = fs
 > fromVRecord _            = evalPanic "fromVRecord" ["Expected a record"]
 >
+> -- | Destructor for @VEnum@.
+> fromVEnum :: Value -> (Ident,[E Value])
+> fromVEnum (VEnum i fs) = (i,fs)
+> fromVEnum _            = evalPanic "fromVEnum" ["Expected an enum value."]
+>
 > -- | Destructor for @VFun@.
 > fromVFun :: Value -> (E Value -> E Value)
 > fromVFun (VFun f) = f
@@ -312,6 +317,8 @@ assigns values to those variables.
 >     EIf c t f ->
 >       condValue (fromVBit <$> evalExpr env c) (evalExpr env t) (evalExpr env f)
 >
+>     ECase e alts dflt -> evalCase env (evalExpr env e) alts dflt
+>
 >     EComp _n _ty e branches -> evalComp env e branches
 >
 >     EVar n ->
@@ -434,6 +441,20 @@ are ignored.
 > condValue :: E Bool -> E Value -> E Value -> E Value
 > condValue c l r = c >>= \b -> if b then l else r
 
+> evalCase :: Env -> E Value -> Map Ident CaseAlt -> Maybe CaseAlt -> E Value
+> evalCase env e alts dflt =
+>   do val <- e
+>      let (tag,fields) = fromVEnum val
+>      case Map.lookup tag alts of
+>        Just alt -> evalCaseBranch alt fields
+>        Nothing  ->
+>          case dflt of
+>            Just alt -> evalCaseBranch alt [pure val]
+>            Nothing  -> Err (NoMatchingConstructor (unpackIdent tag))
+>   where
+>   evalCaseBranch (CaseAlt xs k) vs = evalExpr env' k
+>     where env' = foldr bindVar env (zip (map fst xs) vs)
+
 List Comprehensions
 -------------------
 

src/Cryptol/Eval/Value.hs

@@ -57,6 +57,7 @@ module Cryptol.Eval.Value
   , fromVTuple
   , fromVRecord
   , lookupRecord
+  , fromVEnum
     -- ** Pretty printing
   , defaultPPOpts
   , ppValue
@@ -445,6 +446,12 @@ fromVRecord val = case val of
   VRecord fs -> fs
   _          -> evalPanic "fromVRecord" ["not a record", show val]
 
+fromVEnum :: GenValue sym -> (Ident,[SEval sym (GenValue sym)])
+fromVEnum val =
+  case val of
+    VEnum c xs -> (c,xs)
+    _          -> evalPanic "fromVEnum" ["not an enum", show val]
+
 fromVFloat :: GenValue sym -> SFloat sym
 fromVFloat val =
   case val of