Make abstract type a special kind of nomainal type.

Fixes #1604

cryptol-remote-api/src/CryptolServer/Data/Expression.hs

@@ -618,7 +618,6 @@ readBack ty val =
         TVRec{} -> "record"
         TVFun{} -> "fun"
         TVNominal nt _ _ -> identText $ nameIdent $ TC.ntName nt
-        TVAbstract{} -> "abstract"
 
 
 -- | Given a suggested `name` and a type and value, attempt to bind the value

cryptol-remote-api/src/CryptolServer/Data/Type.hs

@@ -220,6 +220,7 @@ instance JSON.ToJSON JSONType where
         JSON.object [ "type" .= case ntDef nt of
                                   Struct {} -> T.pack "newtype"
                                   Enum {}   -> T.pack "enum"
+                                  Abstract  -> T.pack "primitive"
                     , "name" .= show (pp (ntName nt))
                     , "arguments" .= map (JSONType ns) ts
                     ]

src/Cryptol/Eval.hs

@@ -341,6 +341,7 @@ evalNominalDecl sym nt env0 =
   case ntDef nt of
     Struct c -> pure (bindVarDirect (ntConName c) (mkCon structCon) env0)
     Enum cs  -> foldM enumCon env0 cs
+    Abstract -> pure env0
   where
   structCon = PFun PPrim
   mkCon c   = foldr tabs c (ntParams nt)

src/Cryptol/Eval/Concrete.hs

@@ -88,6 +88,7 @@ toExpr prims t0 v0 = findOne (go t0 v0)
                let c = case ntDef nt of
                          Struct co -> ntConName co
                          Enum {} -> panic "toExpr" ["Enum vs Record"]
+                         Abstract -> panic "toExp" ["Asbtract vs Record"]
                    f = foldl (\x t -> ETApp x (tNumValTy t)) (EVar c) ts
                 in pure (EApp f (ERec efs))
       (TVNominal nt ts (TVEnum tfss), VEnum i' vf_map) ->
@@ -103,6 +104,7 @@ toExpr prims t0 v0 = findOne (go t0 v0)
                guard (Vector.length tfs == Vector.length vfs)
                c <- case ntDef nt of
                       Struct {} -> panic "toExpr" ["Enum vs Record"]
+                      Abstract {} -> panic "toExpr" ["Enum vs Abstract"]
                       Enum cons ->
                         case find (\con -> ecNumber con == i) cons of
                           Just con -> pure (ecName con)

src/Cryptol/Eval/Generic.hs

@@ -250,9 +250,6 @@ ringBinary sym opw opi opz opq opfp = loop
               (\f fty -> sDelay sym (loop' fty (lookupRecord f l) (lookupRecord f r)))
               fs
 
-    TVAbstract {} ->
-      evalPanic "ringBinary" ["Abstract type not in `Ring`"]
-
     TVNominal {} ->
       evalPanic "ringBinary" ["Nominal type not in `Ring`"]
 
@@ -330,8 +327,6 @@ ringUnary sym opw opi opz opq opfp = loop
           (\f fty -> sDelay sym (loop' fty (lookupRecord f v)))
           fs
 
-    TVAbstract {} -> evalPanic "ringUnary" ["Abstract type not in `Ring`"]
-
     TVNominal {} -> evalPanic "ringUnary" ["Nominal type not in `Ring`"]
 
 
@@ -398,9 +393,6 @@ ringNullary sym opw opi opz opq opfp = loop
              do xs <- traverse (sDelay sym . loop) fs
                 pure $ VRecord xs
 
-        TVAbstract {} ->
-          evalPanic "ringNullary" ["Abstract type not in `Ring`"]
-
         TVNominal {} ->
           evalPanic "ringNullary" ["Nominal type not in `Ring`"]
 
@@ -777,8 +769,6 @@ cmpValue sym fb fw fi fz fq ff = cmp
                             (recordElements (fromVRecord v1))
                             (recordElements (fromVRecord v2))
                             k
-        TVAbstract {} -> evalPanic "cmpValue"
-                          [ "Abstract type not in `Cmp`" ]
 
         TVNominal {} -> evalPanic "cmpValue"
                           [ "Nominal type not in `Cmp`" ]
@@ -951,8 +941,6 @@ zeroV sym ty = case ty of
       do xs <- traverse (sDelay sym . zeroV sym) fields
          pure $ VRecord xs
 
-  TVAbstract {} -> evalPanic "zeroV" [ "Abstract type not in `Zero`" ]
-
   TVNominal {} -> evalPanic "zeroV" [ "Nominal type not in `Zero`" ]
 
 
@@ -1292,9 +1280,6 @@ logicBinary sym opb opw = loop
           (\f fty -> sDelay sym (loop' fty (lookupRecord f l) (lookupRecord f r)))
           fields
 
-    TVAbstract {} -> evalPanic "logicBinary"
-                        [ "Abstract type not in `Logic`" ]
-
     TVNominal {} -> evalPanic "logicBinary"
                         [ "Nominal type not in `Logic`" ]
 
@@ -1352,8 +1337,6 @@ logicUnary sym opb opw = loop
           (\f fty -> sDelay sym (loop' fty (lookupRecord f val)))
           fields
 
-    TVAbstract {} -> evalPanic "logicUnary" [ "Abstract type not in `Logic`" ]
-
     TVNominal {} -> evalPanic "logicUnary" [ "Nominal type not in `Logic`" ]
 
 

src/Cryptol/Eval/Reference.lhs

@@ -567,7 +567,7 @@ the new bindings.
 Nominal Types
 -------------
 
-We have two forms of nominal types: newtypes and enums.
+We have three forms of nominal types: newtypes, enums, and abstract types.
 
 At runtime, newtypes values are represented in exactly
 the same way as records.  The constructor function for
@@ -582,6 +582,7 @@ was used to create a value, and the values of stored
 >   case ntDef nt of
 >     Struct c -> bindVar (ntConName c, mkCon newtypeCon) env
 >     Enum cs  -> foldr enumCon env cs
+>     Abstract -> env
 >   where
 >     mkCon con  = pure (foldr tabs con (ntParams nt))
 >     newtypeCon = VFun id
@@ -1059,7 +1060,6 @@ For functions, `zero` returns the constant function that returns
 > zero (TVRec fields) = VRecord [ (f, pure (zero fty))
 >                               | (f, fty) <- canonicalFields fields ]
 > zero (TVFun _ bty)  = VFun (\_ -> pure (zero bty))
-> zero (TVAbstract{}) = evalPanic "zero" ["Abstract type not in `Zero`"]
 > zero (TVNominal {})  = evalPanic "zero" ["Nominal type not in `Zero`"]
 
 Literals
@@ -1128,7 +1128,6 @@ at the same positions.
 >         TVArray{}    -> evalPanic "logicUnary" ["Array not in class Logic"]
 >         TVRational   -> evalPanic "logicUnary" ["Rational not in class Logic"]
 >         TVFloat{}    -> evalPanic "logicUnary" ["Float not in class Logic"]
->         TVAbstract{} -> evalPanic "logicUnary" ["Abstract type not in `Logic`"]
 >         TVNominal {}  -> evalPanic "logicUnary" ["Nominal type not in `Logic`"]
 
 > logicBinary :: (Bool -> Bool -> Bool) -> TValue -> E Value -> E Value -> E Value
@@ -1167,7 +1166,6 @@ at the same positions.
 >         TVArray{}    -> evalPanic "logicBinary" ["Array not in class Logic"]
 >         TVRational   -> evalPanic "logicBinary" ["Rational not in class Logic"]
 >         TVFloat{}    -> evalPanic "logicBinary" ["Float not in class Logic"]
->         TVAbstract{} -> evalPanic "logicBinary" ["Abstract type not in `Logic`"]
 >         TVNominal {} -> evalPanic "logicBinary" ["Nominal type not in `Logic`"]
 
 
@@ -1214,8 +1212,6 @@ False]`, but to `error "foo"`.
 >           pure $ VTuple (map go tys)
 >         TVRec fs ->
 >           pure $ VRecord [ (f, go fty) | (f, fty) <- canonicalFields fs ]
->         TVAbstract {} ->
->           evalPanic "arithNullary" ["Abstract type not in `Ring`"]
 >         TVNominal {} ->
 >           evalPanic "arithNullary" ["Newtype type not in `Ring`"]
 
@@ -1254,8 +1250,6 @@ False]`, but to `error "foo"`.
 >           do val' <- val
 >              pure $ VRecord [ (f, go fty (lookupRecord f val'))
 >                             | (f, fty) <- canonicalFields fs ]
->         TVAbstract {} ->
->           evalPanic "arithUnary" ["Abstract type not in `Ring`"]
 >         TVNominal {} ->
 >           evalPanic "arithUnary" ["Nominal type not in `Ring`"]
 
@@ -1304,8 +1298,6 @@ False]`, but to `error "foo"`.
 >              pure $ VRecord
 >                [ (f, go fty (lookupRecord f l') (lookupRecord f r'))
 >                | (f, fty) <- canonicalFields fs ]
->         TVAbstract {} ->
->           evalPanic "arithBinary" ["Abstract type not in class `Ring`"]
 >         TVNominal {} ->
 >           evalPanic "arithBinary" ["Nominal type not in class `Ring`"]
 
@@ -1484,8 +1476,6 @@ bits to the *left* of that position are equal.
 >          ls <- map snd . sortBy (comparing fst) . fromVRecord <$> l
 >          rs <- map snd . sortBy (comparing fst) . fromVRecord <$> r
 >          lexList (zipWith3 lexCompare tys ls rs)
->     TVAbstract {} ->
->       evalPanic "lexCompare" ["Abstract type not in `Cmp`"]
 >     TVNominal {} ->
 >       evalPanic "lexCompare" ["Nominal type not in `Cmp`"]
 >
@@ -1540,8 +1530,6 @@ fields are compared in alphabetical order.
 >          ls <- map snd . sortBy (comparing fst) . fromVRecord <$> l
 >          rs <- map snd . sortBy (comparing fst) . fromVRecord <$> r
 >          lexList (zipWith3 lexSignedCompare tys ls rs)
->     TVAbstract {} ->
->       evalPanic "lexSignedCompare" ["Abstract type not in `Cmp`"]
 >     TVNominal {} ->
 >       evalPanic "lexSignedCompare" ["Nominal type not in `Cmp`"]
 

src/Cryptol/Eval/Type.hs

@@ -47,12 +47,12 @@ data TValue
   | TVNominal NominalType
               [Either Nat' TValue]
               TNominalTypeValue    -- ^ a named newtype
-  | TVAbstract UserTC [Either Nat' TValue] -- ^ an abstract type
     deriving (Generic, NFData, Eq)
 
 data TNominalTypeValue =
     TVStruct (RecordMap Ident TValue)
   | TVEnum   (Vector (ConInfo TValue))  -- ^ Indexed by constructor number
+  | TVAbstract
     deriving (Generic, NFData, Eq)
 
 data ConInfo a = ConInfo
@@ -89,7 +89,6 @@ tValTy tv =
     TVRec fs    -> tRec (fmap tValTy fs)
     TVFun t1 t2 -> tFun (tValTy t1) (tValTy t2)
     TVNominal nt vs _ -> tNominal nt (map tNumValTy vs)
-    TVAbstract u vs -> tAbstract u (map tNumValTy vs)
 
 tNumTy :: Nat' -> Type
 tNumTy Inf     = tInf
@@ -178,15 +177,6 @@ evalType env ty =
         (TCTuple _, _)  -> Right $ TVTuple (map val ts)
         (TCNum n, [])   -> Left $ Nat n
         (TCInf, [])     -> Left $ Inf
-        (TCAbstract u,vs) ->
-            case kindOf ty of
-              KType -> Right $ TVAbstract u (map (evalType env) vs)
-              k -> evalPanic "evalType"
-                [ "Unsupported"
-                , "*** Abstract type of kind: " ++ show (pp k)
-                , "*** Name: " ++ show (pp u)
-                ]
-
         _ -> evalPanic "evalType" ["not a value type", show ty]
     TCon (TF f) ts      -> Left $ evalTF f (map num ts)
     TCon (PC p) _       -> evalPanic "evalType" ["invalid predicate symbol", show p]
@@ -207,6 +197,7 @@ 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)))
+    Abstract -> TVAbstract
   where
   env' = loop env0 (ntParams nt) args
 

src/Cryptol/IR/TraverseNames.hs

@@ -185,7 +185,7 @@ instance TraverseNames ArgDescr where
 instance TraverseNames Type where
   traverseNamesIP ty =
     case ty of
-      TCon tc ts    -> TCon <$> traverseNamesIP tc <*> traverseNamesIP ts
+      TCon tc ts    -> TCon tc <$> traverseNamesIP ts
       TVar x        -> TVar <$> traverseNamesIP x
       TUser x ts t  -> TUser <$> traverseNamesIP x
                              <*> traverseNamesIP ts
@@ -194,21 +194,6 @@ instance TraverseNames Type where
       TNominal nt ts -> TNominal <$> traverseNamesIP nt <*> traverseNamesIP ts
 
 
-instance TraverseNames TCon where
-  traverseNamesIP tcon =
-    case tcon of
-      TC tc -> TC <$> traverseNamesIP tc
-      _     -> pure tcon
-
-instance TraverseNames TC where
-  traverseNamesIP tc =
-    case tc of
-      TCAbstract ut -> TCAbstract <$> traverseNamesIP ut
-      _             -> pure tc
-
-instance TraverseNames UserTC where
-  traverseNamesIP (UserTC x k) = UserTC <$> traverseNamesIP x <*> pure k
-
 instance TraverseNames TVar where
   traverseNamesIP tvar =
     case tvar of
@@ -220,15 +205,18 @@ instance TraverseNames NominalType where
     NominalType
       <$> traverseNamesIP (ntName nt)
       <*> traverseNamesIP (ntParams nt)
+      <*> pure (ntKind nt)
       <*> traverseNamesIP (ntConstraints nt)
       <*> traverseNamesIP (ntDef nt)
+      <*> pure (ntFixity nt)
       <*> pure (ntDoc nt)
 
 instance TraverseNames NominalTypeDef where
   traverseNamesIP def =
     case def of
       Struct c -> Struct <$> traverseNamesIP c
       Enum cs  -> Enum   <$> traverseNamesIP cs
+      Abstract -> pure Abstract
 
 instance TraverseNames StructCon where
   traverseNamesIP c =

src/Cryptol/ModuleSystem/Base.hs

@@ -758,7 +758,6 @@ genInferInput r prims params env = do
     , T.inpVars             = Map.map ifDeclSig (ifDecls env)
     , T.inpTSyns            = ifTySyns env
     , T.inpNominalTypes     = ifNominalTypes env
-    , T.inpAbstractTypes    = ifAbstractTypes env
     , T.inpSignatures       = ifSignatures env
     , T.inpNameSeeds        = seeds
     , T.inpMonoBinds        = monoBinds

src/Cryptol/ModuleSystem/Env.hs

@@ -625,7 +625,6 @@ deIfaceDecls :: DynamicEnv -> IfaceDecls
 deIfaceDecls DEnv { deDecls = dgs, deTySyns = tySyns } =
     IfaceDecls { ifTySyns = tySyns
                , ifNominalTypes = Map.empty
-               , ifAbstractTypes = Map.empty
                , ifDecls = decls
                , ifModules = Map.empty
                , ifFunctors = Map.empty

src/Cryptol/ModuleSystem/Interface.hs

@@ -98,7 +98,6 @@ emptyIface nm = Iface
 data IfaceDecls = IfaceDecls
   { ifTySyns        :: Map.Map Name TySyn
   , ifNominalTypes  :: Map.Map Name NominalType
-  , ifAbstractTypes :: Map.Map Name AbstractType
   , ifDecls         :: Map.Map Name IfaceDecl
   , ifModules       :: !(Map.Map Name (IfaceNames Name))
   , ifSignatures    :: !(Map.Map Name ModParamNames)
@@ -118,7 +117,6 @@ filterIfaceDecls :: (Name -> Bool) -> IfaceDecls -> IfaceDecls
 filterIfaceDecls p ifs = IfaceDecls
   { ifTySyns        = filterMap (ifTySyns ifs)
   , ifNominalTypes  = filterMap (ifNominalTypes ifs)
-  , ifAbstractTypes = filterMap (ifAbstractTypes ifs)
   , ifDecls         = filterMap (ifDecls ifs)
   , ifModules       = filterMap (ifModules ifs)
   , ifFunctors      = filterMap (ifFunctors ifs)
@@ -131,7 +129,6 @@ filterIfaceDecls p ifs = IfaceDecls
 ifaceDeclsNames :: IfaceDecls -> Set Name
 ifaceDeclsNames i = Set.unions [ Map.keysSet (ifTySyns i)
                                , Map.keysSet (ifNominalTypes i)
-                               , Map.keysSet (ifAbstractTypes i)
                                , Map.keysSet (ifDecls i)
                                , Map.keysSet (ifModules i)
                                , Map.keysSet (ifFunctors i)
@@ -143,7 +140,6 @@ instance Semigroup IfaceDecls where
   l <> r = IfaceDecls
     { ifTySyns   = Map.union (ifTySyns l)   (ifTySyns r)
     , ifNominalTypes = Map.union (ifNominalTypes l) (ifNominalTypes r)
-    , ifAbstractTypes = Map.union (ifAbstractTypes l) (ifAbstractTypes r)
     , ifDecls    = Map.union (ifDecls l)    (ifDecls r)
     , ifModules  = Map.union (ifModules l)  (ifModules r)
     , ifFunctors = Map.union (ifFunctors l) (ifFunctors r)
@@ -154,7 +150,6 @@ instance Monoid IfaceDecls where
   mempty      = IfaceDecls
                   { ifTySyns = mempty
                   , ifNominalTypes = mempty
-                  , ifAbstractTypes = mempty
                   , ifDecls = mempty
                   , ifModules = mempty
                   , ifFunctors = mempty
@@ -164,7 +159,6 @@ instance Monoid IfaceDecls where
   mconcat ds  = IfaceDecls
     { ifTySyns   = Map.unions (map ifTySyns   ds)
     , ifNominalTypes = Map.unions (map ifNominalTypes ds)
-    , ifAbstractTypes = Map.unions (map ifAbstractTypes ds)
     , ifDecls    = Map.unions (map ifDecls    ds)
     , ifModules  = Map.unions (map ifModules ds)
     , ifFunctors = Map.unions (map ifFunctors ds)
@@ -231,8 +225,7 @@ ifaceOrigNameMap ifa = Map.unionsWith Map.union (here : nested)
 
   decls       = ifDefines ifa
   from f      = Map.keysSet (f decls)
-  tyNames     = Set.unions [ from ifTySyns
-                           , from ifNominalTypes, from ifAbstractTypes ]
+  tyNames     = Set.unions [ from ifTySyns, from ifNominalTypes ]
   moNames     = Set.unions [ from ifModules, from ifSignatures, from ifFunctors ]
   vaNames     = Set.unions [ newtypeCons, from ifDecls ]
   newtypeCons = Set.fromList

src/Cryptol/ModuleSystem/NamingEnv.hs

@@ -242,7 +242,7 @@ modParamNamingEnv mp = maybe id qualify (T.mpQual mp) $
 -- the names are qualified.
 unqualifiedEnv :: IfaceDecls -> NamingEnv
 unqualifiedEnv IfaceDecls { .. } =
-  mconcat [ exprs, tySyns, ntTypes, absTys, ntExprs, mods, sigs ]
+  mconcat [ exprs, tySyns, ntTypes, ntExprs, mods, sigs ]
   where
   toPName n = mkUnqual (nameIdent n)
 
@@ -261,9 +261,6 @@ unqualifiedEnv IfaceDecls { .. } =
                             ]
                     ]
 
-  absTys  = mconcat [ singletonNS NSType (toPName n) n
-                    | n <- Map.keys ifAbstractTypes ]
-
   ntExprs = mconcat [ singletonNS NSValue (toPName n) n
                     | n <- Map.keys ifNominalTypes ]
 

src/Cryptol/REPL/Browse.hs

@@ -110,13 +110,15 @@ browseTSyns disp decls =
 
 browsePrimTys :: DispInfo -> IfaceDecls -> [Doc]
 browsePrimTys disp decls =
-  ppSection disp "Primitive Types" ppA (ifAbstractTypes decls)
+  ppSection disp "Primitive Types" ppA ats
   where
-  ppA a = nest 2 (sep [pp (T.atName a) <+> ":", pp (T.atKind a)])
+  ats = Map.filter T.nominalTypeIsAbstract (ifNominalTypes decls)
+  ppA a = nest 2 (sep [pp (T.ntName a) <+> ":", pp (T.kindOf a)])
 
 browseNominalTypes :: DispInfo -> IfaceDecls -> [Doc]
 browseNominalTypes disp decls =
-  ppSection disp "Nominal Types" T.ppNominalShort (ifNominalTypes decls)
+  ppSection disp "Nominal Types" T.ppNominalShort
+    (Map.filter (not . T.nominalTypeIsAbstract) (ifNominalTypes decls))
 
 browseVars :: DispInfo -> IfaceDecls -> [Doc]
 browseVars disp decls =