Rename "newtype" to "nominal type" after type checker

Fixes #1607

src/Cryptol/Eval.hs

@@ -11,7 +11,6 @@
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE ParallelListComp #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE ViewPatterns #-}
@@ -28,7 +27,7 @@ module Cryptol.Eval (
   , emptyEnv
   , evalExpr
   , evalDecls
-  , evalNewtypeDecls
+  , evalNominalDecls
   , evalSel
   , evalSetSel
   , evalEnumCon
@@ -99,7 +98,8 @@ moduleEnv ::
   Module         {- ^ Module containing declarations to evaluate -} ->
   GenEvalEnv sym {- ^ Environment to extend -} ->
   SEval sym (GenEvalEnv sym)
-moduleEnv sym m env = evalDecls sym (mDecls m) =<< evalNewtypeDecls sym (mNewtypes m) env
+moduleEnv sym m env = evalDecls sym (mDecls m) =<<
+                          evalNominalDecls sym (mNominalTypes m) env
 
 {-# SPECIALIZE evalExpr ::
   (?range :: Range, ConcPrims) =>
@@ -314,30 +314,30 @@ cacheCallStack sym v = case v of
 
 -- Newtypes --------------------------------------------------------------------
 
-{-# SPECIALIZE evalNewtypeDecls ::
+{-# SPECIALIZE evalNominalDecls ::
   ConcPrims =>
   Concrete ->
-  Map.Map Name Newtype ->
+  Map.Map Name NominalType ->
   GenEvalEnv Concrete ->
   SEval Concrete (GenEvalEnv Concrete)
   #-}
 
-evalNewtypeDecls ::
+evalNominalDecls ::
   EvalPrims sym =>
   sym ->
-  Map.Map Name Newtype ->
+  Map.Map Name NominalType ->
   GenEvalEnv sym ->
   SEval sym (GenEvalEnv sym)
-evalNewtypeDecls sym nts env = foldM (flip (evalNewtypeDecl sym)) env $ Map.elems nts
+evalNominalDecls sym nts env = foldM (flip (evalNominalDecl sym)) env $ Map.elems nts
 
 -- | Introduce the constructor function for a newtype.
-evalNewtypeDecl ::
+evalNominalDecl ::
   EvalPrims sym =>
   sym ->
-  Newtype ->
+  NominalType ->
   GenEvalEnv sym ->
   SEval sym (GenEvalEnv sym)
-evalNewtypeDecl sym nt env0 =
+evalNominalDecl sym nt env0 =
   case ntDef nt of
     Struct c -> pure (bindVarDirect (ntConName c) (mkCon structCon) env0)
     Enum cs  -> foldM enumCon env0 cs
@@ -361,7 +361,7 @@ evalNewtypeDecl sym nt env0 =
                                     , show (pp k)
                                     ]
 
-{-# INLINE evalNewtypeDecl #-}
+{-# INLINE evalNominalDecl #-}
 
 -- | Make the function for a known constructor
 evalEnumCon ::

src/Cryptol/Eval/Concrete.hs

@@ -79,7 +79,7 @@ toExpr prims t0 v0 = findOne (go t0 v0)
              Left _ -> mismatch -- different fields
              Right efs -> pure (ERec efs)
 
-      (TVNewtype nt ts (TVStruct tfs), VRecord vfs) ->
+      (TVNominal nt ts (TVStruct tfs), VRecord vfs) ->
         do -- NB, vfs first argument to keep their display order
            res <- zipRecordsM (\_lbl v t -> go t =<< lift v) vfs tfs
            case res of
@@ -90,7 +90,7 @@ 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))
-      (TVNewtype nt ts (TVEnum tfss), VEnum i' vf_map) ->
+      (TVNominal nt ts (TVEnum tfss), VEnum i' vf_map) ->
         let i = fromInteger i'
         in
         case tfss Vector.!? i of

src/Cryptol/Eval/Generic.hs

@@ -253,8 +253,8 @@ ringBinary sym opw opi opz opq opfp = loop
     TVAbstract {} ->
       evalPanic "ringBinary" ["Abstract type not in `Ring`"]
 
-    TVNewtype {} ->
-      evalPanic "ringBinary" ["Newtype not in `Ring`"]
+    TVNominal {} ->
+      evalPanic "ringBinary" ["Nominal type not in `Ring`"]
 
 type UnaryWord sym = Integer -> SWord sym -> SEval sym (SWord sym)
 
@@ -332,7 +332,7 @@ ringUnary sym opw opi opz opq opfp = loop
 
     TVAbstract {} -> evalPanic "ringUnary" ["Abstract type not in `Ring`"]
 
-    TVNewtype {} -> evalPanic "ringUnary" ["Newtype not in `Ring`"]
+    TVNominal {} -> evalPanic "ringUnary" ["Nominal type not in `Ring`"]
 
 
 {-# SPECIALIZE ringNullary ::
@@ -401,8 +401,8 @@ ringNullary sym opw opi opz opq opfp = loop
         TVAbstract {} ->
           evalPanic "ringNullary" ["Abstract type not in `Ring`"]
 
-        TVNewtype {} ->
-          evalPanic "ringNullary" ["Newtype not in `Ring`"]
+        TVNominal {} ->
+          evalPanic "ringNullary" ["Nominal type not in `Ring`"]
 
 {-# SPECIALIZE integralBinary :: Concrete -> BinWord Concrete ->
       (SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
@@ -780,8 +780,8 @@ cmpValue sym fb fw fi fz fq ff = cmp
         TVAbstract {} -> evalPanic "cmpValue"
                           [ "Abstract type not in `Cmp`" ]
 
-        TVNewtype {} -> evalPanic "cmpValue"
-                          [ "Newtype not in `Cmp`" ]
+        TVNominal {} -> evalPanic "cmpValue"
+                          [ "Nominal type not in `Cmp`" ]
 
     cmpValues (t : ts) (x1 : xs1) (x2 : xs2) k =
       do x1' <- x1
@@ -953,7 +953,7 @@ zeroV sym ty = case ty of
 
   TVAbstract {} -> evalPanic "zeroV" [ "Abstract type not in `Zero`" ]
 
-  TVNewtype {} -> evalPanic "zeroV" [ "Newtype not in `Zero`" ]
+  TVNominal {} -> evalPanic "zeroV" [ "Nominal type not in `Zero`" ]
 
 
 {-# SPECIALIZE joinSeq ::
@@ -1295,8 +1295,8 @@ logicBinary sym opb opw = loop
     TVAbstract {} -> evalPanic "logicBinary"
                         [ "Abstract type not in `Logic`" ]
 
-    TVNewtype {} -> evalPanic "logicBinary"
-                        [ "Newtype not in `Logic`" ]
+    TVNominal {} -> evalPanic "logicBinary"
+                        [ "Nominal type not in `Logic`" ]
 
 {-# SPECIALIZE logicUnary ::
   Concrete ->
@@ -1354,7 +1354,7 @@ logicUnary sym opb opw = loop
 
     TVAbstract {} -> evalPanic "logicUnary" [ "Abstract type not in `Logic`" ]
 
-    TVNewtype {} -> evalPanic "logicUnary" [ "Newtype not in `Logic`" ]
+    TVNominal {} -> evalPanic "logicUnary" [ "Nominal type not in `Logic`" ]
 
 
 {-# INLINE assertIndexInBounds #-}

src/Cryptol/Eval/Reference.lhs

@@ -43,7 +43,7 @@
 > import qualified Cryptol.Backend.FloatHelpers as FP
 > import Cryptol.Backend.Monad (EvalError(..))
 > import Cryptol.Eval.Type
->   (TValue(..), TNewtypeValue(..),
+>   (TValue(..), TNominalTypeValue(..),
 >    isTBit, evalValType, evalNumType, TypeEnv, bindTypeVar)
 > import Cryptol.Eval.Concrete (mkBv, ppBV, lg2)
 > import Cryptol.Utils.Ident (Ident,PrimIdent, prelPrim, floatPrim, unpackIdent)
@@ -54,7 +54,7 @@
 > import Cryptol.Eval.Type (evalType, lookupTypeVar, tNumTy, tValTy)
 >
 > import qualified Cryptol.ModuleSystem as M
-> import qualified Cryptol.ModuleSystem.Env as M (loadedModules,loadedNewtypes)
+> import qualified Cryptol.ModuleSystem.Env as M (loadedModules,loadedNominalTypes)
 
 Overview
 ========
@@ -408,7 +408,7 @@ types and on newtypes.
 >   case (tyv, sel) of
 >     (TVTuple ts, TupleSel n _) -> updTupleAt ts n
 >     (TVRec fs, RecordSel n _)  -> updRecAt fs n
->     (TVNewtype _ _ (TVStruct fs), RecordSel n _) -> updRecAt fs n
+>     (TVNominal _ _ (TVStruct fs), RecordSel n _) -> updRecAt fs n
 >     (TVSeq len _, ListSel n _) -> updSeqAt len n
 >     (_, _) -> evalPanic "evalSet" ["type/selector mismatch", show tyv, show sel]
 >   where
@@ -567,18 +567,18 @@ the new bindings.
 Nominal Types
 -------------
 
-We have two forms of nominal types: newtypes and enumerations.
+We have two forms of nominal types: newtypes and enums.
 
 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
+Enums 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 =
+> evalNominalDecl :: Env -> NominalType -> Env
+> evalNominalDecl env nt =
 >   case ntDef nt of
 >     Struct c -> bindVar (ntConName c, mkCon newtypeCon) env
 >     Enum cs  -> foldr enumCon env cs
@@ -1060,7 +1060,7 @@ For functions, `zero` returns the constant function that returns
 >                               | (f, fty) <- canonicalFields fields ]
 > zero (TVFun _ bty)  = VFun (\_ -> pure (zero bty))
 > zero (TVAbstract{}) = evalPanic "zero" ["Abstract type not in `Zero`"]
-> zero (TVNewtype{})  = evalPanic "zero" ["Newtype not in `Zero`"]
+> zero (TVNominal {})  = evalPanic "zero" ["Nominal type not in `Zero`"]
 
 Literals
 --------
@@ -1129,7 +1129,7 @@ at the same positions.
 >         TVRational   -> evalPanic "logicUnary" ["Rational not in class Logic"]
 >         TVFloat{}    -> evalPanic "logicUnary" ["Float not in class Logic"]
 >         TVAbstract{} -> evalPanic "logicUnary" ["Abstract type not in `Logic`"]
->         TVNewtype{}  -> evalPanic "logicUnary" ["Newtype not in `Logic`"]
+>         TVNominal {}  -> evalPanic "logicUnary" ["Nominal type not in `Logic`"]
 
 > logicBinary :: (Bool -> Bool -> Bool) -> TValue -> E Value -> E Value -> E Value
 > logicBinary op = go
@@ -1168,7 +1168,7 @@ at the same positions.
 >         TVRational   -> evalPanic "logicBinary" ["Rational not in class Logic"]
 >         TVFloat{}    -> evalPanic "logicBinary" ["Float not in class Logic"]
 >         TVAbstract{} -> evalPanic "logicBinary" ["Abstract type not in `Logic`"]
->         TVNewtype{}  -> evalPanic "logicBinary" ["Newtype not in `Logic`"]
+>         TVNominal {} -> evalPanic "logicBinary" ["Nominal type not in `Logic`"]
 
 
 Ring Arithmetic
@@ -1216,7 +1216,7 @@ False]`, but to `error "foo"`.
 >           pure $ VRecord [ (f, go fty) | (f, fty) <- canonicalFields fs ]
 >         TVAbstract {} ->
 >           evalPanic "arithNullary" ["Abstract type not in `Ring`"]
->         TVNewtype {} ->
+>         TVNominal {} ->
 >           evalPanic "arithNullary" ["Newtype type not in `Ring`"]
 
 > ringUnary ::
@@ -1256,8 +1256,8 @@ False]`, but to `error "foo"`.
 >                             | (f, fty) <- canonicalFields fs ]
 >         TVAbstract {} ->
 >           evalPanic "arithUnary" ["Abstract type not in `Ring`"]
->         TVNewtype {} ->
->           evalPanic "arithUnary" ["Newtype not in `Ring`"]
+>         TVNominal {} ->
+>           evalPanic "arithUnary" ["Nominal type not in `Ring`"]
 
 > ringBinary ::
 >   (Integer -> Integer -> E Integer) ->
@@ -1306,8 +1306,8 @@ False]`, but to `error "foo"`.
 >                | (f, fty) <- canonicalFields fs ]
 >         TVAbstract {} ->
 >           evalPanic "arithBinary" ["Abstract type not in class `Ring`"]
->         TVNewtype {} ->
->           evalPanic "arithBinary" ["Newtype not in class `Ring`"]
+>         TVNominal {} ->
+>           evalPanic "arithBinary" ["Nominal type not in class `Ring`"]
 
 
 Integral
@@ -1486,8 +1486,8 @@ bits to the *left* of that position are equal.
 >          lexList (zipWith3 lexCompare tys ls rs)
 >     TVAbstract {} ->
 >       evalPanic "lexCompare" ["Abstract type not in `Cmp`"]
->     TVNewtype {} ->
->       evalPanic "lexCompare" ["Newtype not in `Cmp`"]
+>     TVNominal {} ->
+>       evalPanic "lexCompare" ["Nominal type not in `Cmp`"]
 >
 > lexList :: [E Ordering] -> E Ordering
 > lexList [] = pure EQ
@@ -1542,8 +1542,8 @@ fields are compared in alphabetical order.
 >          lexList (zipWith3 lexSignedCompare tys ls rs)
 >     TVAbstract {} ->
 >       evalPanic "lexSignedCompare" ["Abstract type not in `Cmp`"]
->     TVNewtype {} ->
->       evalPanic "lexSignedCompare" ["Newtype type not in `Cmp`"]
+>     TVNominal {} ->
+>       evalPanic "lexSignedCompare" ["Nominal type not in `Cmp`"]
 
 
 Sequences
@@ -1863,6 +1863,6 @@ running the reference evaluator on an expression.
 >   where
 >     modEnv = M.minpModuleEnv minp
 >     extDgs = concatMap mDecls (M.loadedModules modEnv) ++ M.deDecls (M.meDynEnv modEnv)
->     nts    = Map.elems (M.loadedNewtypes modEnv)
->     env    = foldl evalDeclGroup (foldl evalNewtypeDecl mempty nts) extDgs
+>     nts    = Map.elems (M.loadedNominalTypes modEnv)
+>     env    = foldl evalDeclGroup (foldl evalNominalDecl mempty nts) extDgs
 >     val    = evalExpr env expr

src/Cryptol/Eval/Type.hs

@@ -44,13 +44,13 @@ data TValue
   | TVTuple [TValue]          -- ^ @ (a, b, c )@
   | TVRec (RecordMap Ident TValue) -- ^ @ { x : a, y : b, z : c } @
   | TVFun TValue TValue       -- ^ @ a -> b @
-  | TVNewtype Newtype
+  | TVNominal NominalType
               [Either Nat' TValue]
-              TNewtypeValue    -- ^ a named newtype
+              TNominalTypeValue    -- ^ a named newtype
   | TVAbstract UserTC [Either Nat' TValue] -- ^ an abstract type
     deriving (Generic, NFData, Eq)
 
-data TNewtypeValue =
+data TNominalTypeValue =
     TVStruct (RecordMap Ident TValue)
   | TVEnum   (Vector (ConInfo TValue))  -- ^ Indexed by constructor number
     deriving (Generic, NFData, Eq)
@@ -88,7 +88,7 @@ tValTy tv =
     TVTuple ts  -> tTuple (map tValTy ts)
     TVRec fs    -> tRec (fmap tValTy fs)
     TVFun t1 t2 -> tFun (tValTy t1) (tValTy t2)
-    TVNewtype nt vs _ -> tNewtype nt (map tNumValTy vs)
+    TVNominal nt vs _ -> tNominal nt (map tNumValTy vs)
     TVAbstract u vs -> tAbstract u (map tNumValTy vs)
 
 tNumTy :: Nat' -> Type
@@ -160,7 +160,7 @@ evalType env ty =
     TUser _ _ ty'  -> evalType env ty'
     TRec fields    -> Right $ TVRec (fmap val fields)
 
-    TNewtype nt ts -> Right $ TVNewtype nt tvs $ evalNewtypeBody env nt tvs
+    TNominal nt ts -> Right $ TVNominal nt tvs $ evalNominalTypeBody env nt tvs
         where tvs = map (evalType env) ts
 
     TCon (TC c) ts ->
@@ -201,9 +201,9 @@ evalType env ty =
                                   ["Expecting a finite size, but got `inf`"]
 
 -- | Evaluate the body of a newtype, given evaluated arguments
-evalNewtypeBody ::
-  TypeEnv -> Newtype -> [Either Nat' TValue] -> TNewtypeValue
-evalNewtypeBody env0 nt args =
+evalNominalTypeBody ::
+  TypeEnv -> NominalType -> [Either Nat' TValue] -> TNominalTypeValue
+evalNominalTypeBody env0 nt args =
   case ntDef nt of
     Struct c -> TVStruct (fmap (evalValType env') (ntFields c))
     Enum cs  -> TVEnum (Vector.fromList (map doEnum (sortOn ecNumber cs)))

src/Cryptol/IR/FreeVars.hs

@@ -148,7 +148,7 @@ instance FreeVars Type where
 
       TUser _ _ t -> freeVars t
       TRec fs     -> freeVars (recordElements fs)
-      TNewtype nt ts -> freeVars nt <> freeVars ts
+      TNominal nt ts -> freeVars nt <> freeVars ts
 
 instance FreeVars TVar where
   freeVars tv = case tv of
@@ -158,11 +158,11 @@ instance FreeVars TVar where
 instance FreeVars TCon where
   freeVars _tc = mempty
 
-instance FreeVars Newtype where
+instance FreeVars NominalType where
   freeVars nt = foldr rmTParam base (ntParams nt)
     where base = freeVars (ntConstraints nt) <> freeVars (ntDef nt)
 
-instance FreeVars NewtypeDef where
+instance FreeVars NominalTypeDef where
   freeVars def =
     case def of
       Struct c -> freeVars c