Make constructors work

src/Cryptol/Eval.hs

@@ -322,19 +322,27 @@ evalNewtypeDecl ::
 evalNewtypeDecl _sym nt =
   case ntDef nt of
     Struct c ->
-      pure . bindVarDirect (ntConName c) val
+      pure . bindVarDirect (ntConName c) (mkCon structCon)
     Enum cs -> pure . foldr (\c f -> enumCon c . f) id cs
   where
-  con           = PFun PPrim -- XXX: WRONG f
-  val           = foldr tabs con (ntParams nt) 
+  structCon = PFun PPrim
+  mkCon c   = foldr tabs c (ntParams nt)
 
-  enumCon c = bindVarDirect (ecName c) val
+  enumCon c =
+    let i           = nameIdent (ecName c)
+        done        = PVal . VEnum i . reverse
+        fu _t f xs  = PFun (\v -> f (v:xs))
+    in
+    bindVarDirect (ecName c) (mkCon (foldr fu done (ecFields c) []))
 
   tabs tp body =
     case tpKind tp of
       KType -> PTyPoly  (\ _ -> body)
       KNum  -> PNumPoly (\ _ -> body)
-      k -> evalPanic "evalNewtypeDecl" ["illegal newtype parameter kind", show (pp k)]
+      k ->
+        evalPanic "evalNewtypeDecl" [ "illegal newtype parameter kind"
+                                    , show (pp k)
+                                    ]
 
 {-# INLINE evalNewtypeDecl #-}
 

src/Cryptol/Eval/Reference.lhs

@@ -36,7 +36,7 @@
 > import qualified GHC.Num.Compat as Integer
 > import qualified Data.List as List
 >
-> import Cryptol.ModuleSystem.Name (asPrim)
+> import Cryptol.ModuleSystem.Name (asPrim,nameIdent)
 > import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul)
 > import Cryptol.TypeCheck.AST
 > import Cryptol.Backend.FloatHelpers (BF(..))
@@ -46,7 +46,7 @@
 >   (TValue(..), TNewtypeValue(..),
 >    isTBit, evalValType, evalNumType, TypeEnv, bindTypeVar)
 > import Cryptol.Eval.Concrete (mkBv, ppBV, lg2)
-> import Cryptol.Utils.Ident (Ident,PrimIdent, prelPrim, floatPrim)
+> import Cryptol.Utils.Ident (Ident,PrimIdent, prelPrim, floatPrim, unpackIdent)
 > import Cryptol.Utils.Panic (panic)
 > import Cryptol.Utils.PP
 > import Cryptol.Utils.RecordMap
@@ -177,7 +177,7 @@ terms by providing an evaluator to an appropriate `Value` type.
 >   | VList Nat' [E Value]       -- ^ @ [n]a   @ finite or infinite lists
 >   | VTuple [E Value]           -- ^ @ ( .. ) @ tuples
 >   | VRecord [(Ident, E Value)] -- ^ @ { .. } @ records
->   | VEnum Ident Value          -- ^ @ Just x @, sum types
+>   | VEnum Ident [E Value]      -- ^ @ Just x @, sum types
 >   | VFun (E Value -> E Value)  -- ^ functions
 >   | VPoly (TValue -> E Value)  -- ^ polymorphic values (kind *)
 >   | VNumPoly (Nat' -> E Value) -- ^ polymorphic values (kind #)
@@ -543,27 +543,39 @@ the new bindings.
 >     DExpr e       -> (dName d, evalExpr env e)
 >
 
-Newtypes
---------
+Nominal Types
+-------------
+
+We have two forms of nominal types: newtypes and enumerations.
 
 At runtime, newtypes values are represented in exactly
 the same way as records.  The constructor function for
 newtypes is thus basically just an identity function
 that consumes and ignores its type arguments.
 
+Enumarations are represented with a tag, which indicates what constructor
+was used to create a value, and the values of stored 
+
 > evalNewtypeDecl :: Env -> Newtype -> Env
 > evalNewtypeDecl env nt =
 >   case ntDef nt of
->     Struct c -> bindVar (ntConName c, pure val) env
->     Enum cs  -> undefined   -- XXX
+>     Struct c -> bindVar (ntConName c, mkCon newtypeCon) env
+>     Enum cs  -> foldr enumCon env cs
 >   where
->     val = foldr tabs con (ntParams nt)
->     con = VFun (\x -> x)
+>     mkCon con  = pure (foldr tabs con (ntParams nt))
+>     newtypeCon = VFun id
+>     enumCon c  =
+>       bindVar (ecName c, mkCon (foldr addField tag (ecFields c) []))
+>       where
+>       tag                 = VEnum (nameIdent (ecName c)) . reverse
+>       addField _t mk args = VFun (\v -> pure (mk (v:args)))
+>
 >     tabs tp body =
 >       case tpKind tp of
 >         KType -> VPoly (\_ -> pure body)
 >         KNum  -> VNumPoly (\_ -> pure body)
->         k -> evalPanic "evalNewtypeDecl" ["illegal newtype parameter kind", show k]
+>         k -> evalPanic "evalNewtypeDecl"
+>                                   ["illegal newtype parameter kind", show k]
 
 Primitives
 ==========
@@ -1809,6 +1821,11 @@ Pretty Printing
 >     VTuple vs  -> ppTuple (map (ppEValue opts) vs)
 >     VRecord fs -> ppRecord (map ppField fs)
 >       where ppField (f,r) = pp f <+> char '=' <+> ppEValue opts r
+>     VEnum tag vs ->
+>       case vs of
+>         [] -> tagT
+>         _  -> parens (tagT <+> hsep (map (ppEValue opts) vs))
+>       where tagT = text (unpackIdent tag)
 >     VFun _     -> text "<function>"
 >     VPoly _    -> text "<polymorphic value>"
 >     VNumPoly _ -> text "<polymorphic value>"

src/Cryptol/Eval/Value.hs

@@ -80,7 +80,7 @@ import Cryptol.Eval.Type
 
 import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
 
-import Cryptol.Utils.Ident (Ident)
+import Cryptol.Utils.Ident (Ident,unpackIdent)
 import Cryptol.Utils.Logger(Logger)
 import Cryptol.Utils.Panic(panic)
 import Cryptol.Utils.PP
@@ -105,6 +105,7 @@ data EvalOpts = EvalOpts
 data GenValue sym
   = VRecord !(RecordMap Ident (SEval sym (GenValue sym))) -- ^ @ { .. } @
   | VTuple ![SEval sym (GenValue sym)]              -- ^ @ ( .. ) @
+  | VEnum !Ident ![SEval sym (GenValue sym)]    -- ^ @ Just 2 @
   | VBit !(SBit sym)                           -- ^ @ Bit    @
   | VInteger !(SInteger sym)                   -- ^ @ Integer @ or @ Z n @
   | VRational !(SRational sym)                 -- ^ @ Rational @
@@ -124,6 +125,7 @@ forceValue :: Backend sym => GenValue sym -> SEval sym ()
 forceValue v = case v of
   VRecord fs  -> mapM_ (forceValue =<<) fs
   VTuple xs   -> mapM_ (forceValue =<<) xs
+  VEnum _ xs  -> mapM_ (forceValue =<<) xs
   VSeq n xs   -> mapM_ (forceValue =<<) (enumerateSeqMap n xs)
   VBit b      -> seq b (return ())
   VInteger i  -> seq i (return ())
@@ -141,6 +143,7 @@ instance Show (GenValue sym) where
   show v = case v of
     VRecord fs -> "record:" ++ show (displayOrder fs)
     VTuple xs  -> "tuple:" ++ show (length xs)
+    VEnum c _  -> "enum:" ++ unpackIdent c
     VBit _     -> "bit"
     VInteger _ -> "integer"
     VRational _ -> "rational"
@@ -160,23 +163,28 @@ ppValue :: forall sym.
   PPOpts ->
   GenValue sym ->
   SEval sym Doc
-ppValue x opts = loop
+ppValue x opts = loop 0
   where
-  loop :: GenValue sym -> SEval sym Doc
-  loop val = case val of
-    VRecord fs         -> do fs' <- traverse (>>= loop) fs
+  loop :: Int -> GenValue sym -> SEval sym Doc
+  loop prec val = case val of
+    VRecord fs         -> do fs' <- traverse (>>= loop 0) fs
                              return $ ppRecord (map ppField (fields fs'))
       where
       ppField (f,r) = pp f <+> char '=' <+> r
-    VTuple vals        -> do vals' <- traverse (>>=loop) vals
+    VTuple vals        -> do vals' <- traverse (>>=loop 0) vals
                              return $ ppTuple vals'
+    VEnum c vs         -> case vs of
+                            [] -> pure (pp c)
+                            _ -> do vds <- traverse (>>= loop 1) vs
+                                    let d = pp c <+> hsep vds
+                                    pure (if prec > 0 then parens d else d)
     VBit b             -> ppSBit x b
     VInteger i         -> ppSInteger x i
     VRational q        -> ppSRational x q
     VFloat i           -> ppSFloat x opts i
     VSeq sz vals       -> ppWordSeq sz vals
     VWord _ wv         -> ppWordVal wv
-    VStream vals       -> do vals' <- traverse (>>=loop) $ enumerateSeqMap (useInfLength opts) vals
+    VStream vals       -> do vals' <- traverse (>>=loop 0) $ enumerateSeqMap (useInfLength opts) vals
                              return $ ppList ( vals' ++ [text "..."] )
     VFun{}             -> return $ text "<function>"
     VPoly{}            -> return $ text "<polymorphic value>"
@@ -202,7 +210,7 @@ ppValue x opts = loop
                 Just str -> return $ text (show str)
                 _ -> do vs' <- mapM (ppSWord x opts) vs
                         return $ ppList vs'
-      _ -> do ws' <- traverse loop ws
+      _ -> do ws' <- traverse (loop 0) ws
               return $ ppList ws'
 
 ppSBit :: Backend sym => sym -> SBit sym -> SEval sym Doc

src/Cryptol/ModuleSystem/Base.hs

@@ -617,10 +617,11 @@ checkModule isrc m = do
   renMod <- renameModule epgm
 
 
-  -- dump renamed
+  {- dump renamed
   unless (thing (mName (R.rmModule renMod)) == preludeName)
        do (io $ print (T.pp renMod))
           -- io $ exitSuccess
+  --}
 
 
   -- when generating the prim map for the typechecker, if we're checking the

src/Cryptol/REPL/Help.hs

@@ -242,7 +242,10 @@ showTypeHelp ctxparams env nameEnv name =
 
   fromNewtype =
     do nt <- Map.lookup name (M.ifNewtypes env)
-       let decl = pp nt $$ (pp name <+> text ":" <+> pp (T.newtypeConType nt))
+       let decl = pp nt $$
+                  vcat
+                    [ pp x <+> text ":" <+> pp t
+                    | (x,t) <- T.newtypeConTypes nt ]
        return $ doShowTyHelp nameEnv decl (T.ntDoc nt)
 
   fromPrimType =
@@ -321,6 +324,7 @@ showValHelp ctxparams env nameEnv qname name =
 
             doShowDocString ifDeclDoc
 
+  -- XXX: enum constructors
   fromNewtype =
     do _ <- Map.lookup name (M.ifNewtypes env)
        return $ return ()

src/Cryptol/TypeCheck/Infer.hs

@@ -43,7 +43,7 @@ import           Cryptol.TypeCheck.Error
 import           Cryptol.TypeCheck.Solve
 import           Cryptol.TypeCheck.SimpType(tMul)
 import           Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn,
-                                        checkPropSyn,checkNewtype,
+                                        checkPropSyn,checkNewtype,checkEnum,
                                         checkParameterType,
                                         checkPrimType,
                                         checkParameterConstraints,
@@ -1312,6 +1312,10 @@ checkTopDecls = mapM_ checkTopDecl
         do t <- checkNewtype (P.tlValue tl) (thing <$> P.tlDoc tl)
            addNewtype t
 
+      P.TDEnum tl ->
+        do t <- checkEnum (P.tlValue tl) (thing <$> P.tlDoc tl)
+           addNewtype t
+
       P.DPrimType tl ->
         do t <- checkPrimType (P.tlValue tl) (thing <$> P.tlDoc tl)
            addPrimType t

src/Cryptol/TypeCheck/Kind.hs

@@ -14,6 +14,7 @@ module Cryptol.TypeCheck.Kind
   ( checkType
   , checkSchema
   , checkNewtype
+  , checkEnum
   , checkPrimType
   , checkTySyn
   , checkPropSyn
@@ -39,7 +40,7 @@ import           Data.List(sortBy,groupBy)
 import           Data.Maybe(fromMaybe)
 import           Data.Function(on)
 import           Data.Text (Text)
-import           Control.Monad(unless,when,mplus)
+import           Control.Monad(unless,when,mplus,forM)
 
 -- | Check a type signature.  Returns validated schema, and any implicit
 -- constraints that we inferred.
@@ -150,6 +151,32 @@ checkNewtype (P.Newtype x as con fs) mbD =
                     , ntDoc = mbD
                     }
 
+checkEnum :: P.EnumDecl Name -> Maybe Text -> InferM Newtype
+checkEnum ed mbD =
+  do let x = P.eName ed
+     ((as1,cons1),gs) <- collectGoals $
+       inRange (srcRange x) $
+       do r <- withTParams NoWildCards newtypeParam (P.eParams ed) $
+               forM (P.eCons ed) \tlC ->
+                 do let con = P.tlValue tlC
+                        cname = P.ecName con
+                    ts <- kInRange (srcRange cname)
+                            (mapM (`doCheckType` Just KType) (P.ecFields con))
+                    pure EnumCon
+                          { ecName   = thing cname
+                          , ecFields = ts
+                          , ecPublic = P.tlExport tlC == P.Public
+                          , ecDoc    = thing <$> P.tlDoc tlC
+                          }
+          simplifyAllConstraints
+          pure r
+     pure Newtype { ntName = thing x
+                  , ntParams = as1
+                  , ntConstraints = map goal gs
+                  , ntDef = Enum cons1
+                  , ntDoc = mbD
+                  }
+
 checkPrimType :: P.PrimType Name -> Maybe Text -> InferM AbstractType
 checkPrimType p mbD =
   do let (as,cs) = P.primTCts p