Start on implementing abstract types/constants (module parameters)

src/Cryptol/ModuleSystem/Interface.hs

@@ -17,6 +17,7 @@ module Cryptol.ModuleSystem.Interface (
   , IfaceTySyn, ifTySynName
   , IfaceNewtype
   , IfaceDecl(..), mkIfaceDecl
+  , IfaceParams(..)
 
   , genIface
   , ifacePrimMap
@@ -37,9 +38,15 @@ import Prelude.Compat
 
 -- | The resulting interface generated by a module that has been typechecked.
 data Iface = Iface
-  { ifModName :: !ModName
+  { ifModName   :: !ModName     -- ^ Module name
-  , ifPublic  :: IfaceDecls
+  , ifPublic    :: IfaceDecls   -- ^ Exported definitions
-  , ifPrivate :: IfaceDecls
+  , ifPrivate   :: IfaceDecls   -- ^ Private defintiions
+  , ifAbstract  :: IfaceParams  -- ^ Uninterpreted constants (aka module params)
+  } deriving (Show, Generic, NFData)
+
+data IfaceParams = IfaceParams
+  { ifAbsTypes :: Map.Map Name TParam     -- ^ Uninterpreted types
+  , ifAbsFuns  :: Map.Map Name IfaceDecl  -- ^ Uninterpreted value constants
   } deriving (Show, Generic, NFData)
 
 data IfaceDecls = IfaceDecls
@@ -69,12 +76,12 @@ ifTySynName = tsName
 type IfaceNewtype = Newtype
 
 data IfaceDecl = IfaceDecl
-  { ifDeclName    :: !Name
+  { ifDeclName    :: !Name          -- ^ Name of thing
-  , ifDeclSig     :: Schema
+  , ifDeclSig     :: Schema         -- ^ Type
-  , ifDeclPragmas :: [Pragma]
+  , ifDeclPragmas :: [Pragma]       -- ^ Pragmas
-  , ifDeclInfix   :: Bool
+  , ifDeclInfix   :: Bool           -- ^ Is this an infix thing
-  , ifDeclFixity  :: Maybe Fixity
+  , ifDeclFixity  :: Maybe Fixity   -- ^ Fixity information
-  , ifDeclDoc     :: Maybe String
+  , ifDeclDoc     :: Maybe String   -- ^ Documentation
   } deriving (Show, Generic, NFData)
 
 mkIfaceDecl :: Decl -> IfaceDecl
@@ -91,23 +98,44 @@ mkIfaceDecl d = IfaceDecl
 genIface :: Module -> Iface
 genIface m = Iface
   { ifModName = mName m
-  , ifPublic  = IfaceDecls
+
-    { ifTySyns = tsPub
+  , ifPublic      = IfaceDecls
-    , ifNewtypes = ntPub
+    { ifTySyns    = tsPub
-    , ifDecls  = dPub
+    , ifNewtypes  = ntPub
+    , ifDecls     = dPub
     }
+
   , ifPrivate = IfaceDecls
-    { ifTySyns = tsPriv
+    { ifTySyns    = tsPriv
-    , ifNewtypes = ntPriv
+    , ifNewtypes  = ntPriv
-    , ifDecls  = dPriv
+    , ifDecls     = dPriv
+    }
+
+  , ifAbstract = IfaceParams
+    { ifAbsTypes = mAbsTypes m
+    , ifAbsFuns  = valParams
     }
   }
   where
 
+  valParams = Map.mapWithKey xxxDecl (mAbsFuns m)
+
+  xxxDecl qn s = IfaceDecl
+    { ifDeclName    = qn
+    , ifDeclSig     = s
+    , ifDeclPragmas = []
+    , ifDeclInfix   = False
+    , ifDeclFixity  = Nothing
+    , ifDeclDoc     = Nothing
+    }
+
+
   (tsPub,tsPriv) =
-      Map.partitionWithKey (\ qn _ -> qn `isExportedType` mExports m ) (mTySyns m)
+      Map.partitionWithKey (\ qn _ -> qn `isExportedType` mExports m )
+                          (mTySyns m)
   (ntPub,ntPriv) =
-      Map.partitionWithKey (\ qn _ -> qn `isExportedType` mExports m ) (mNewtypes m)
+      Map.partitionWithKey (\ qn _ -> qn `isExportedType` mExports m )
+                           (mNewtypes m)
 
   (dPub,dPriv) =
       Map.partitionWithKey (\ qn _ -> qn `isExportedBind` mExports m)

src/Cryptol/ModuleSystem/NamingEnv.hs

@@ -298,8 +298,22 @@ instance BindsNames (InModule (TopDecl PName)) where
     case td of
       Decl d      -> namingEnv (InModule ns (tlValue d))
       TDNewtype d -> namingEnv (InModule ns (tlValue d))
+      DAbstractType d -> namingEnv (InModule ns (tlValue d))
+      DAbstractFun d -> namingEnv (InModule ns (tlValue d))
       Include _   -> mempty
 
+instance BindsNames (InModule (AbstractFun PName)) where
+  namingEnv (InModule ns AbstractFun { .. }) = BuildNamingEnv $
+    do let Located { .. } = afName
+       ntName <- liftSupply (mkDeclared ns (getIdent thing) Nothing srcRange)
+       return (singletonE thing ntName)
+
+instance BindsNames (InModule (AbstractType PName)) where
+  namingEnv (InModule ns AbstractType { .. }) = BuildNamingEnv $
+    do let Located { .. } = atName
+       ntName <- liftSupply (mkDeclared ns (getIdent thing) Nothing srcRange)
+       return (singletonT thing ntName)
+
 -- NOTE: we use the same name at the type and expression level, as there's only
 -- ever one name introduced in the declaration. The names are only ever used in
 -- different namespaces, so there's no ambiguity.

src/Cryptol/ModuleSystem/Renamer.hs

@@ -360,6 +360,19 @@ instance Rename TopDecl where
     Decl d      -> Decl      <$> traverse rename d
     TDNewtype n -> TDNewtype <$> traverse rename n
     Include n   -> return (Include n)
+    DAbstractFun f -> DAbstractFun <$> traverse rename f
+    DAbstractType f -> DAbstractType <$> traverse rename f
+
+instance Rename AbstractType where
+  rename a =
+    do n' <- rnLocated renameType (atName a)
+       return a { atName = n' }
+
+instance Rename AbstractFun where
+  rename a =
+    do n'   <- rnLocated renameVar (afName a)
+       sig' <- renameSchema (afSchema a)
+       return a { afName = n', afSchema = snd sig' }
 
 rnLocated :: (a -> RenameM b) -> Located a -> RenameM (Located b)
 rnLocated f loc = withLoc loc $

src/Cryptol/Parser.y

@@ -56,6 +56,7 @@ import Paths_cryptol
   'as'        { Located $$ (Token (KW KW_as)        _)}
   'hiding'    { Located $$ (Token (KW KW_hiding)    _)}
   'private'   { Located $$ (Token (KW KW_private)   _)}
+  'abstract'  { Located $$ (Token (KW KW_abstract) _)}
   'property'  { Located $$ (Token (KW KW_property)  _)}
   'infix'     { Located $$ (Token (KW KW_infix)     _)}
   'infixl'    { Located $$ (Token (KW KW_infixl)    _)}
@@ -240,6 +241,8 @@ vtop_decl               :: { [TopDecl PName] }
   | mbDoc newtype          { [exportNewtype Public $2]                        }
   | prim_bind              { $1                                               }
   | private_decls          { $1                                               }
+  | abs_fun_decl           { $1 }
+  | abs_type_decl          { $1 }
 
 top_decl                :: { [TopDecl PName] }
   : decl                   { [Decl (TopLevel {tlExport = Public, tlValue = $1 })] }
@@ -256,6 +259,12 @@ prim_bind               :: { [TopDecl PName] }
   : mbDoc 'primitive' name  ':' schema       { mkPrimDecl $1 $3 $5 }
   | mbDoc 'primitive' '(' op ')' ':' schema  { mkPrimDecl $1 $4 $7 }
 
+abs_type_decl           :: { [TopDecl PName] }
+  : mbDoc 'abstract' 'type' name ':' kind_fun { [ mkAbsType $1 $4 $6 ] }
+
+abs_fun_decl           :: { [TopDecl PName] }
+  : mbDoc 'abstract' name ':' schema { [mkAbsFun $1 $3 $5] }
+
 doc                     :: { Located String }
   : DOC                    { mkDoc (fmap tokenText $1) }
 
@@ -563,6 +572,11 @@ kind                             :: { Located Kind      }
   : '#'                             { Located $1 KNum   }
   | '*'                             { Located $1 KType  }
 
+kind_fun                        :: { ([Located Kind], Located Kind) }
+  : kind                          { ([], $1) }
+  | kind '->' kind_fun            { let { (xs,x) = $3 } in ($1 : xs, x) }
+  
+
 schema_param                   :: { TParam PName }
   : ident                         {% mkTParam $1 Nothing           }
   | ident ':' kind                {% mkTParam (at ($1,$3) $1) (Just (thing $3)) }

src/Cryptol/Parser/AST.hs

@@ -48,6 +48,8 @@ module Cryptol.Parser.AST
   , TopLevel(..)
   , Import(..), ImportSpec(..)
   , Newtype(..)
+  , AbstractType(..)
+  , AbstractFun(..)
 
     -- * Interactive
   , ReplInput(..)
@@ -122,6 +124,8 @@ modRange m = rCombs $ catMaybes
 data TopDecl name = Decl (TopLevel (Decl name))
                   | TDNewtype (TopLevel (Newtype name))
                   | Include (Located FilePath)
+                  | DAbstractType (TopLevel (AbstractType name))
+                  | DAbstractFun  (TopLevel (AbstractFun name))
                     deriving (Show, Generic, NFData)
 
 data Decl name = DSignature [Located name] (Schema name)
@@ -133,6 +137,21 @@ data Decl name = DSignature [Located name] (Schema name)
                | DLocated (Decl name) Range
                  deriving (Eq, Show, Generic, NFData, Functor)
 
+
+-- XXX Infix ops
+data AbstractType name = AbstractType
+  { atName    :: Located name
+  , atParams  :: [Kind]
+  , atResult  :: Kind
+  } deriving (Eq,Show,Generic,NFData)
+
+-- XXX Infix ops
+data AbstractFun name = AbstractFun
+  { afName   :: Located name
+  , afSchema :: Schema name
+  } deriving (Eq,Show,Generic,NFData)
+
+
 -- | An import declaration.
 data Import = Import { iModule    :: !ModName
                      , iAs        :: Maybe ModName
@@ -468,6 +487,14 @@ instance HasLoc (TopDecl name) where
     Decl tld    -> getLoc tld
     TDNewtype n -> getLoc n
     Include lfp -> getLoc lfp
+    DAbstractType d -> getLoc d
+    DAbstractFun d  -> getLoc d
+
+instance HasLoc (AbstractType name) where
+  getLoc a = getLoc (atName a)
+
+instance HasLoc (AbstractFun name) where
+  getLoc a = getLoc (afName a)
 
 instance HasLoc (Module name) where
   getLoc m
@@ -518,6 +545,19 @@ instance (Show name, PPName name) => PP (TopDecl name) where
       Decl    d   -> pp d
       TDNewtype n -> pp n
       Include l   -> text "include" <+> text (show (thing l))
+      DAbstractFun d -> pp d
+      DAbstractType d -> pp d
+
+instance (Show name, PPName name) => PP (AbstractType name) where
+  ppPrec _ a = text "abstract" <+> text "type" <+>
+               ppPrefixName (atName a) <+> text ":" <+>
+               foldr ppKFun (pp (atResult a)) (atParams a)
+    where ppKFun x y = pp x <+> text "->" <+> y
+
+instance (Show name, PPName name) => PP (AbstractFun name) where
+  ppPrec _ a = text "abstract" <+> ppPrefixName (afName a) <+> text ":"
+                  <+> pp (afSchema a)
+
 
 instance (Show name, PPName name) => PP (Decl name) where
   ppPrec n decl =
@@ -865,6 +905,14 @@ instance NoPos (TopDecl name) where
       Decl    x   -> Decl     (noPos x)
       TDNewtype n -> TDNewtype(noPos n)
       Include x   -> Include  (noPos x)
+      DAbstractFun d -> DAbstractFun (noPos d)
+      DAbstractType d -> DAbstractType (noPos d)
+
+instance NoPos (AbstractType name) where
+  noPos a = a
+
+instance NoPos (AbstractFun x) where
+  noPos x = x { afSchema = noPos (afSchema x) }
 
 instance NoPos a => NoPos (TopLevel a) where
   noPos tl = tl { tlValue = noPos (tlValue tl) }

src/Cryptol/Parser/Lexer.x

@@ -117,6 +117,7 @@ $white+                   { emit $ White Space }
 "infix"                   { emit $ KW KW_infix  }
 
 "primitive"               { emit $ KW KW_primitive }
+"abstract"                { emit $ KW KW_abstract }
 
 @num2                     { emitS (numToken 2  . Text.drop 2) }
 @num8                     { emitS (numToken 8  . Text.drop 2) }

src/Cryptol/Parser/LexerUtils.hs

@@ -391,8 +391,10 @@ data TokenKW  = KW_Arith
               | KW_infixr
               | KW_infix
               | KW_primitive
+              | KW_abstract
                 deriving (Eq, Show, Generic, NFData)
 
+-- | The named operators are a special case for parsing types, and 'Other' is
 -- | The named operators are a special case for parsing types, and 'Other' is
 -- used for all other cases that lexed as an operator.
 data TokenOp  = Plus | Minus | Mul | Div | Exp | Mod

src/Cryptol/Parser/Names.hs

@@ -27,6 +27,8 @@ modExports m = fold (concat [ exportedNames d | d <- mDecls m ])
                          ++ map exportType (names tnamesD td)
   exportedNames (TDNewtype nt) = map exportType (names tnamesNT nt)
   exportedNames (Include {})  = []
+  exportedNames (DAbstractFun f) = [ exportBind ((thing . afName) <$> f) ]
+  exportedNames (DAbstractType f) = [ exportType ((thing . atName) <$> f) ]
 
 -- | The names defined by a newtype.
 tnamesNT :: Newtype name -> ([Located name], ())

src/Cryptol/Parser/NoInclude.hs

@@ -156,6 +156,8 @@ noIncTopDecl :: TopDecl PName -> NoIncM [TopDecl PName]
 noIncTopDecl td = case td of
   Decl _     -> return [td]
   TDNewtype _-> return [td]
+  DAbstractType {} -> return [td]
+  DAbstractFun {} -> return [td]
   Include lf -> resolveInclude lf
 
 -- | Resolve the file referenced by a include into a list of top-level

src/Cryptol/Parser/ParserUtils.hs

@@ -270,11 +270,39 @@ exportNewtype e n = TDNewtype TopLevel { tlExport = e
                                        , tlDoc    = Nothing
                                        , tlValue  = n }
 
+mkAbsFun :: Maybe (Located String) ->
+            Located PName ->
+            Schema PName ->
+            TopDecl PName
+mkAbsFun mbDoc n s =
+  DAbstractFun
+  TopLevel { tlExport = Public
+           , tlDoc = mbDoc
+           , tlValue = AbstractFun { afName = n, afSchema = s }
+           }
+
+mkAbsType :: Maybe (Located String) ->
+             Located PName ->
+             ([Located Kind],Located Kind) ->
+             TopDecl PName
+mkAbsType mbDoc n (ks,k) =
+  DAbstractType
+  TopLevel { tlExport = Public
+           , tlDoc = mbDoc
+           , tlValue = AbstractType { atName = n
+                                    , atParams = map thing ks
+                                    , atResult = thing k }
+           }
+
+
+
 changeExport :: ExportType -> [TopDecl PName] -> [TopDecl PName]
 changeExport e = map change
   where
   change (Decl d)      = Decl      d { tlExport = e }
   change (TDNewtype n) = TDNewtype n { tlExport = e }
+  change (DAbstractType a) = DAbstractType a { tlExport = e }
+  change (DAbstractFun a)  = DAbstractFun a { tlExport = e }
   change td@Include{}  = td
 
 mkTypeInst :: Named (Type PName) -> TypeInst PName

src/Cryptol/TypeCheck/AST.hs

@@ -45,18 +45,19 @@ import           Data.Map    (Map)
 import qualified Data.IntMap as IntMap
 
 
-
-
 -- | A Cryptol module.
 data Module = Module { mName     :: !ModName
                      , mExports  :: ExportSpec Name
                      , mImports  :: [Import]
                      , mTySyns   :: Map Name TySyn
                      , mNewtypes :: Map Name Newtype
+                     , mAbsTypes :: Map Name TParam
+                     , mAbsFuns  :: Map Name Schema
                      , mDecls    :: [DeclGroup]
                      } deriving (Show, Generic, NFData)
 
 
+
 data Expr   = EList [Expr] Type         -- ^ List value (with type of elements)
             | ETuple [Expr]             -- ^ Tuple value
             | ERec [(Ident,Expr)]       -- ^ Record value
@@ -302,5 +303,6 @@ instance PP (WithNames Module) where
     -- XXX: Print exports?
     vcat (map pp mImports) $$
     -- XXX: Print tysyns
+    -- XXX: Print abstarct types/functions
     vcat (map (ppWithNames nm) mDecls)
 

src/Cryptol/TypeCheck/Depends.hs

@@ -26,7 +26,9 @@ import           Data.Map (Map)
 import qualified Data.Map as Map
 import qualified Data.Set as Set
 
-data TyDecl = TS (P.TySyn Name) | NT (P.Newtype Name)
+data TyDecl = TS (P.TySyn Name)               -- ^ Type synonym
+            | NT (P.Newtype Name)             -- ^ Newtype
+            | AT (P.AbstractType Name)        -- ^ Abstract type
 
 -- | Check for duplicate and recursive type synonyms.
 -- Returns the type-synonyms in dependency order.
@@ -39,6 +41,10 @@ orderTyDecls ts =
      concat `fmap` mapM check ordered
 
   where
+  toMap _ ty@(AT a) =
+    let x = P.atName a
+    in ( thing x, x { thing = (ty, []) } )
+
   toMap vs ty@(NT (P.Newtype x as fs)) =
     ( thing x
     , x { thing = (ty, Set.toList $
@@ -59,6 +65,7 @@ orderTyDecls ts =
 
   getN (TS (P.TySyn x _ _)) = thing x
   getN (NT x)               = thing (P.nName x)
+  getN (AT x)               = thing (P.atName x)
 
   check (AcyclicSCC x) = return [x]
 
@@ -81,6 +88,7 @@ orderBinds bs = mkScc [ (b, map thing defs, Set.toList uses)
 
 class FromDecl d where
   toBind    :: d -> Maybe (P.Bind Name)
+  toAbsFun  :: d -> Maybe (P.AbstractFun Name)
   toTyDecl  :: d -> Maybe TyDecl
   isTopDecl :: d -> Bool
 
@@ -88,7 +96,11 @@ instance FromDecl (P.TopDecl Name) where
   toBind (P.Decl x)         = toBind (P.tlValue x)
   toBind _                  = Nothing
 
+  toAbsFun (P.DAbstractFun d) = Just (P.tlValue d)
+  toAbsFun _                  = Nothing
+
   toTyDecl (P.TDNewtype d)  = Just (NT (P.tlValue d))
+  toTyDecl (P.DAbstractType d) = Just (AT (P.tlValue d))
   toTyDecl (P.Decl x)       = toTyDecl (P.tlValue x)
   toTyDecl _                = Nothing
 
@@ -99,6 +111,8 @@ instance FromDecl (P.Decl Name) where
   toBind (P.DBind b)      = return b
   toBind _                = Nothing
 
+  toAbsFun _ = Nothing
+
   toTyDecl (P.DLocated d _) = toTyDecl d
   toTyDecl (P.DType x)      = Just (TS x)
   toTyDecl _                = Nothing

src/Cryptol/TypeCheck/Infer.hs

@@ -24,7 +24,7 @@ import           Cryptol.TypeCheck.Monad
 import           Cryptol.TypeCheck.Solve
 import           Cryptol.TypeCheck.SimpType(tSub,tMul,tExp)
 import           Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn,
-                                          checkNewtype)
+                                          checkNewtype, checkAbsType)
 import           Cryptol.TypeCheck.Instantiate
 import           Cryptol.TypeCheck.Depends
 import           Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@),emptySubst)
@@ -49,12 +49,16 @@ inferModule m =
     do simplifyAllConstraints
        ts <- getTSyns
        nts <- getNewtypes
-       return Module { mName    = thing (P.mName m)
+       absTs <- getAbsTypes
-                     , mExports = P.modExports m
+       absFuns <- getAbsFuns
-                     , mImports = map thing (P.mImports m)
+       return Module { mName      = thing (P.mName m)
-                     , mTySyns  = Map.mapMaybe onlyLocal ts
+                     , mExports   = P.modExports m
-                     , mNewtypes = Map.mapMaybe onlyLocal nts
+                     , mImports   = map thing (P.mImports m)
-                     , mDecls   = ds1
+                     , mTySyns    = Map.mapMaybe onlyLocal ts
+                     , mNewtypes  = Map.mapMaybe onlyLocal nts
+                     , mAbsTypes  = absTs
+                     , mAbsFuns   = absFuns
+                     , mDecls     = ds1
                      }
   where
   onlyLocal (IsLocal, x)    = Just x
@@ -830,6 +834,10 @@ inferDs ds continue = checkTyDecls =<< orderTyDecls (mapMaybe toTyDecl ds)
   where
   isTopLevel = isTopDecl (head ds)
 
+  checkTyDecls (AT t : ts) =
+    do t1 <- checkAbsType t
+       withAbsType t1 (checkTyDecls ts)
+
   checkTyDecls (TS t : ts) =
     do t1 <- checkTySyn t
        withTySyn t1 (checkTyDecls ts)
@@ -839,8 +847,19 @@ inferDs ds continue = checkTyDecls =<< orderTyDecls (mapMaybe toTyDecl ds)
        withNewtype t1 (checkTyDecls ts)
 
   -- We checked all type synonyms, now continue with value-level definitions:
-  checkTyDecls [] = checkBinds [] $ orderBinds $ mapMaybe toBind ds
+  checkTyDecls [] =
+    do xs <- mapM checkAbsFun (mapMaybe toAbsFun ds)
+       withAbsFuns xs $ checkBinds [] $ orderBinds $ mapMaybe toBind ds
 
+  checkAbsFun x =
+    do (s,gs) <- checkSchema (P.afSchema x)
+       case gs of
+         [] -> return ()
+         _  ->
+           recordError $ ErrorMsg $ text $
+                            "XXX: Left-over goals while validating schema"
+       let n = thing (P.afName x)
+       return (n,s)
 
   checkBinds decls (CyclicSCC bs : more) =
      do bs1 <- inferBinds isTopLevel True bs

src/Cryptol/TypeCheck/Kind.hs

@@ -13,11 +13,13 @@ module Cryptol.TypeCheck.Kind
   , checkSchema
   , checkNewtype
   , checkTySyn
+  , checkAbsType
   ) where
 
 import qualified Cryptol.Parser.AST as P
 import           Cryptol.Parser.AST (Named(..))
 import           Cryptol.Parser.Position
+import           Cryptol.ModuleSystem.Name(nameUnique)
 import           Cryptol.TypeCheck.AST
 import           Cryptol.TypeCheck.Monad hiding (withTParams)
 import           Cryptol.TypeCheck.SimpType(tRebuild)
@@ -52,6 +54,16 @@ checkSchema (P.Forall xs ps t mb) =
           Nothing -> id
           Just r  -> inRange r
 
+checkAbsType :: P.AbstractType Name -> InferM TParam
+checkAbsType a =
+  do let k = foldr (:->) (cvtK (P.atResult a)) (map cvtK (P.atParams a))
+         n = thing (P.atName a)
+     return TParam { tpUnique = nameUnique n -- XXX: ok to reuse?
+                   , tpKind = k
+                   , tpName = Just n
+                   }
+
+
 -- | Check a type-synonym declaration.
 checkTySyn :: P.TySyn Name -> InferM TySyn
 checkTySyn (P.TySyn x as t) =
@@ -151,13 +163,16 @@ withTParams allowWildCards xs m =
   zip' [] _           = []
   zip' (a:as) ~(t:ts) = (P.tpName a, fmap cvtK (P.tpKind a), t) : zip' as ts
 
-  cvtK P.KNum  = KNum
-  cvtK P.KType = KType
-
   duplicates = [ RepeatedTyParams ds
                     | ds@(_ : _ : _) <- groupBy ((==) `on` P.tpName)
                                       $ sortBy (compare `on` P.tpName) xs ]
 
+cvtK :: P.Kind -> Kind
+cvtK P.KNum  = KNum
+cvtK P.KType = KType
+
+
+
 -- | Check an application of a type constant.
 tcon :: TCon            -- ^ Type constant being applied
      -> [P.Type Name]   -- ^ Type parameters
@@ -167,7 +182,7 @@ tcon tc ts0 k =
   do (ts1,k1) <- appTy ts0 (kindOf tc)
      checkKind (TCon tc ts1) k k1
 
--- | Check a use of a type-synonym, newtype, or scoped-type variable.
+-- | Check a use of a type-synonym, newtype, abs type, or scoped-type variable.
 tySyn :: Bool         -- ^ Should we check for scoped type vars.
       -> Name         -- ^ Name of type sysnonym
       -> [P.Type Name]-- ^ Type synonym parameters
@@ -195,12 +210,26 @@ tySyn scoped x ts k =
                    ts2 <- checkParams (ntParams nt) ts1
                    return (TCon tc ts2)
 
-              -- Maybe it is a scoped type variable?
+              -- Maybe it is an abstract type?
-              Nothing
+              Nothing ->
-                | scoped -> kExistTVar x $ fromMaybe KNum k
+                do mbA <- kLookupAbsType x
-                | otherwise ->
+                   case mbA of
-                  do kRecordError $ UndefinedTypeSynonym x
+                     Just a ->
-                     kNewType (text "type synonym" <+> pp x) $ fromMaybe KNum k
+                       do let tc = abstractTypeTCon a
+                          (ts1,k1) <- appTy ts (kindOf tc)
+                          case k of
+                            Just ks
+                              | ks /= k1 -> kRecordError $ KindMismatch ks k1
+                            _ -> return ()
+                          return (TCon tc ts1)
+
+                     -- Maybe it is a scoped type variable?
+                     Nothing
+                       | scoped -> kExistTVar x $ fromMaybe KNum k
+                       | otherwise ->
+                          do kRecordError $ UndefinedTypeSynonym x
+                             kNewType (text "type synonym" <+> pp x) $
+                                                            fromMaybe KNum k
   where
   checkParams as ts1
     | paramHave == paramNeed = return ts1

src/Cryptol/TypeCheck/Monad.hs

@@ -59,6 +59,7 @@ data InferInput = InferInput
   , inpVars      :: Map Name Schema   -- ^ Variables that are in scope
   , inpTSyns     :: Map Name TySyn    -- ^ Type synonyms that are in scope
   , inpNewtypes  :: Map Name Newtype  -- ^ Newtypes in scope
+
   , inpNameSeeds :: NameSeeds         -- ^ Private state of type-checker
   , inpMonoBinds :: Bool              -- ^ Should local bindings without
                                       --   signatures be monomorphized?
@@ -67,9 +68,9 @@ data InferInput = InferInput
   , inpSearchPath :: [FilePath]
     -- ^ Where to look for Cryptol theory file.
 
-  , inpPrimNames :: !PrimMap          -- ^ The mapping from 'Ident' to 'Name',
+  , inpPrimNames :: !PrimMap
-                                      -- for names that the typechecker
+    -- ^ This is used when the type-checker needs to refer to a predefined
-                                      -- needs to refer to.
+    -- identifier (e.g., @demote@).
 
   , inpSupply :: !Supply              -- ^ The supply for fresh name generation
   } deriving Show
@@ -110,6 +111,9 @@ runInferM info (IM m) = CrySAT.withSolver (inpSolverConfig info) $ \solver ->
                      , iTVars         = []
                      , iTSyns         = fmap mkExternal (inpTSyns info)
                      , iNewtypes      = fmap mkExternal (inpNewtypes info)
+                     , iAbsTypes      = Map.empty
+                     , iAbsFuns       = Map.empty
+
                      , iSolvedHasLazy = iSolvedHas finalRW     -- RECURSION
                      , iMonoBinds     = inpMonoBinds info
                      , iSolver        = solver
@@ -206,6 +210,12 @@ data RO = RO
    -- at the top-level, but then there can't be a newtype with the
    -- same name (this should be caught by the renamer).
 
+  , iAbsTypes :: Map Name TParam
+    -- ^ Abstract types
+
+  , iAbsFuns :: Map Name Schema
+    -- ^ Abstract functions
+
   , iSolvedHasLazy :: Map Int (Expr -> Expr)
     -- ^ NOTE: This field is lazy in an important way!  It is the
     -- final version of `iSolvedHas` in `RW`, and the two are tied
@@ -524,9 +534,14 @@ lookupVar x =
          do mbNT <- lookupNewtype x
             case mbNT of
               Just nt -> return (ExtVar (newtypeConType nt))
-              Nothing -> do recordError $ UndefinedVariable x
+              Nothing ->
-                            a <- newType (text "type of" <+> pp x) KType
+                do mbAbsFun <- lookupAbsFun x
-                            return $ ExtVar $ Forall [] [] a
+                   case mbAbsFun of
+                     Just af -> return (ExtVar af)
+                     Nothing ->
+                       do recordError $ UndefinedVariable x
+                          a <- newType (text "type of" <+> pp x) KType
+                          return $ ExtVar $ Forall [] [] a
 
 -- | Lookup a type variable.  Return `Nothing` if there is no such variable
 -- in scope, in which case we must be dealing with a type constant.
@@ -542,6 +557,14 @@ lookupTSyn x = fmap (fmap snd . Map.lookup x) getTSyns
 lookupNewtype :: Name -> InferM (Maybe Newtype)
 lookupNewtype x = fmap (fmap snd . Map.lookup x) getNewtypes
 
+-- | Lookup the kind of an abstract type
+lookupAbsType :: Name -> InferM (Maybe TParam)
+lookupAbsType x = Map.lookup x <$> getAbsTypes
+
+-- | Lookup the schema for an abstract function.
+lookupAbsFun :: Name -> InferM (Maybe Schema)
+lookupAbsFun x = Map.lookup x <$> getAbsFuns
+
 -- | Check if we already have a name for this existential type variable and,
 -- if so, return the definition.  If not, try to create a new definition,
 -- if this is allowed.  If not, returns nothing.
@@ -574,6 +597,14 @@ getTSyns = IM $ asks iTSyns
 getNewtypes :: InferM (Map Name (DefLoc,Newtype))
 getNewtypes = IM $ asks iNewtypes
 
+-- | Returns the abstract type declarations
+getAbsFuns :: InferM (Map Name Schema)
+getAbsFuns = IM $ asks iAbsFuns
+
+-- | Returns the abstract function declarations
+getAbsTypes :: InferM (Map Name TParam)
+getAbsTypes = IM $ asks iAbsTypes
+
 -- | Get the set of bound type variables that are in scope.
 getTVars :: InferM (Set Name)
 getTVars = IM $ asks $ Set.fromList . mapMaybe tpName . iTVars
@@ -638,6 +669,14 @@ withNewtype t (IM m) =
   IM $ mapReader
         (\r -> r { iNewtypes = Map.insert (ntName t) (IsLocal,t)
                                                      (iNewtypes r) }) m
+withAbsType :: TParam -> InferM a -> InferM a
+withAbsType a (IM m) =
+  case tpName a of
+    Nothing -> panic "withAbsType" ["Abstract type without a name"]
+    Just n  ->
+      IM $ mapReader
+             (\r -> r { iAbsTypes = Map.insert n a (iAbsTypes r) })
+             m
 
 -- | The sub-computation is performed with the given variable in scope.
 withVarType :: Name -> VarType -> InferM a -> InferM a
@@ -650,6 +689,13 @@ withVarTypes xs m = foldr (uncurry withVarType) m xs
 withVar :: Name -> Schema -> InferM a -> InferM a
 withVar x s = withVarType x (ExtVar s)
 
+-- | The sub-computation is performed with the given abstract function in scope.
+withAbsFuns :: [(Name, Schema)] -> InferM a -> InferM a
+withAbsFuns xs (IM m) =
+  IM $ mapReader (\r -> r { iAbsFuns = foldr add (iAbsFuns r) xs }) m
+  where
+  add (x,s) = Map.insert x s
+
 
 -- | The sub-computation is performed with the given variables in scope.
 withMonoType :: (Name,Located Type) -> InferM a -> InferM a
@@ -770,6 +816,9 @@ kLookupTSyn x = kInInferM $ lookupTSyn x
 kLookupNewtype :: Name -> KindM (Maybe Newtype)
 kLookupNewtype x = kInInferM $ lookupNewtype x
 
+kLookupAbsType :: Name -> KindM (Maybe TParam)
+kLookupAbsType x = kInInferM $ lookupAbsType x
+
 kExistTVar :: Name -> Kind -> KindM Type
 kExistTVar x k = kInInferM $ existVar x k
 

src/Cryptol/TypeCheck/Type.hs

@@ -43,7 +43,10 @@ data Schema = Forall { sVars :: [TParam], sProps :: [Prop], sType :: Type }
 -- | Type parameters.
 data TParam = TParam { tpUnique :: !Int       -- ^ Parameter identifier
                      , tpKind   :: Kind       -- ^ Kind of parameter
-                     , tpName   :: Maybe Name -- ^ Name from source, if any.
+                     , tpName   :: Maybe Name
+                       -- ^ Name from source, if any.
+                       -- INVARIANT: if this arouse from an abstract type
+                       -- then the name will alwyas be defined.
                      }
               deriving (Generic, NFData, Show)
 
@@ -120,6 +123,15 @@ data UserTC = UserTC Name Kind
               deriving (Show, Generic, NFData)
 
 
+abstractTypeTCon :: TParam -> TCon
+abstractTypeTCon tp = TC $ TCNewtype $ UserTC nm k
+  where
+  nm = case tpName tp of
+         Just n  -> n
+         Nothing -> panic "abstractTypeTCon" ["Missing name"]
+  k = tpKind tp
+
+
 data TCErrorMessage = TCErrorMessage
   { tcErrorMessage :: !String
     -- XXX: Add location?