Removed the concept of primitive data types, replacing them instead w…

…ith primitives that happen to be types; changed all of the SAW internals that deal with types that used to be primitive data types to handle this change

prelude/Prelude.sawcore

@@ -99,7 +99,7 @@ RecordType__rec _ _ _ _ f1 (RecordValue _ _ _ x y) = f1 x y;
 --------------------------------------------------------------------------------
 -- String values
 
-primitive data String :: sort 0;
+primitive String :: sort 0;
 
 primitive error :: (a :: sort 1) -> String -> a;
 
@@ -916,7 +916,7 @@ natCase p z s = Nat__rec p z (\ (n::Nat) -> \ (r::p n) -> s n);
 
 --------------------------------------------------------------------------------
 -- "Vec n a" is an array of n elements, each with type "a".
-primitive data Vec :: Nat -> sort 0 -> sort 0;
+primitive Vec :: Nat -> sort 0 -> sort 0;
 
 -- Primitive function for generating an array.
 primitive gen :: (n :: Nat) -> (a :: sort 0) -> (Nat -> a) -> Vec n a;
@@ -1388,7 +1388,7 @@ bvStreamShiftR a w x xs i = streamAppend a (bvToNat w i) (replicate (bvToNat w i
 -- Integer values
 --   integer values of unbounded precision
 
-primitive data Integer :: sort 0;
+primitive Integer :: sort 0;
 
 primitive intAdd :: Integer -> Integer -> Integer;
 primitive intSub :: Integer -> Integer -> Integer;
@@ -1432,12 +1432,12 @@ updBvFun n a f i v x = ite a (bvEq n i x) v (f x);
 -- Floating-point values
 --    Currently commented out because they are not implemented...
 
-primitive data Float :: sort 0;
+primitive Float :: sort 0;
 
 -- primitive bvToFloat :: bitvector 32 -> Float;
 -- primitive floatToBV :: Float -> bitvector 32;
 
-primitive data Double :: sort 0;
+primitive Double :: sort 0;
 
 -- primitive bvToDouble :: bitvector 64 -> Double;
 -- primitive doubleToBV :: Double -> bitvector 64;

src/Verifier/SAW/Grammar.y

@@ -101,7 +101,6 @@ Import : 'import' opt('qualified') ModuleName opt(AsName) opt(ModuleImports) ';'
 
 SAWDecl :: { Decl }
 SAWDecl : 'data' Con '::' LTerm 'where' '{' list(CtorDecl) '}' { DataDecl $2 $4 $7 }
-          | 'primitive' 'data' Con '::' LTerm ';'  { PrimDataDecl $3 $5 }
           | 'primitive' DeclLhs '::' LTerm ';'
                {% mkTypeDecl PrimitiveQualifier $2 $4 }
           | 'axiom' DeclLhs '::' LTerm ';'

src/Verifier/SAW/Module.hs

@@ -181,7 +181,6 @@ data DataType =
   { dtName :: Ident
   , dtType :: Term
   , dtCtors :: [Ctor Term]
-  , dtIsPrimitive :: Bool
   }
 
 instance Eq DataType where

src/Verifier/SAW/Prelude/Constants.hs

@@ -17,20 +17,41 @@ preludeModuleName = mkModuleName ["Prelude"]
 preludeNatIdent :: Ident
 preludeNatIdent =  mkIdent preludeModuleName "Nat"
 
+preludeNatType :: FlatTermF e
+preludeNatType =  DataTypeApp preludeNatIdent []
+
 preludeZeroIdent :: Ident
 preludeZeroIdent =  mkIdent preludeModuleName "Zero"
 
 preludeSuccIdent :: Ident
 preludeSuccIdent =  mkIdent preludeModuleName "Succ"
 
+preludeIntegerIdent :: Ident
+preludeIntegerIdent =  mkIdent preludeModuleName "Integer"
+
+preludeIntegerType :: FlatTermF e
+preludeIntegerType = GlobalDef preludeIntegerIdent
+
 preludeVecIdent :: Ident
 preludeVecIdent =  mkIdent preludeModuleName "Vec"
 
+preludeVecTypeFun :: FlatTermF e
+preludeVecTypeFun = GlobalDef preludeVecIdent
+
 preludeFloatIdent :: Ident
 preludeFloatIdent =  mkIdent preludeModuleName "Float"
 
+preludeFloatType :: FlatTermF e
+preludeFloatType = GlobalDef preludeFloatIdent
+
 preludeDoubleIdent :: Ident
 preludeDoubleIdent =  mkIdent preludeModuleName "Double"
 
+preludeDoubleType :: FlatTermF e
+preludeDoubleType = GlobalDef preludeDoubleIdent
+
 preludeStringIdent :: Ident
 preludeStringIdent =  mkIdent preludeModuleName "String"
+
+preludeStringType :: FlatTermF e
+preludeStringType = GlobalDef preludeStringIdent

src/Verifier/SAW/Recognizer.hs

@@ -16,7 +16,7 @@ Portability : non-portable (language extensions)
 
 module Verifier.SAW.Recognizer
   ( Recognizer
-  , (<:), emptyl, endl
+  , (<:>), (<:), emptyl, endl
   , (:*:)(..)
   , asFTermF
 
@@ -134,6 +134,12 @@ asApp _ = fail "not app"
   (x, y) <- asApp t
   liftM2 (const id) (f x) (g y)
 
+-- | Recognizes a function application, and returns the function
+(<@) :: (Monad f) => Recognizer f Term a -> Recognizer f Term () -> Recognizer f Term a
+(<@) f g t = do
+  (x, y) <- asApp t
+  liftM2 const (f x) (g y)
+
 asApplyAll :: Term -> (Term, [Term])
 asApplyAll = go []
   where go xs t =
@@ -296,25 +302,26 @@ asBoolType :: (Monad f) => Recognizer f Term ()
 asBoolType = isDataType "Prelude.Bool" emptyl
 
 asIntegerType :: (Monad f) => Recognizer f Term ()
-asIntegerType = isDataType "Prelude.Integer" emptyl
+asIntegerType = isGlobalDef "Prelude.Integer"
 
 asVectorType :: (Monad f) => Recognizer f Term (Term, Term)
-asVectorType = isDataType "Prelude.Vec" r
-  where r [n, t] = return (n, t)
-        r _ = fail "asVectorType: wrong number of arguments"
+asVectorType = helper ((isGlobalDef "Prelude.Vec" @> return) <@> return) where
+  helper r t =
+    do (n :*: a) <- r t
+       return (n, a)
 
 isVecType :: (Monad f)
           => Recognizer f Term a -> Recognizer f Term (Nat :*: a)
-isVecType tp = isDataType "Prelude.Vec" (asNatLit <:> endl tp)
+isVecType tp = (isGlobalDef "Prelude.Vec" @> asNatLit) <@> tp
 
 asVecType :: (Monad f) => Recognizer f Term (Nat :*: Term)
 asVecType = isVecType return
 
 asBitvectorType :: (Alternative f, Monad f) => Recognizer f Term Nat
 asBitvectorType =
   (isGlobalDef "Prelude.bitvector" @> asNatLit)
-  <> isDataType "Prelude.Vec"
-                (asNatLit <: endl (isDataType "Prelude.Bool" emptyl))
+  <> ((isGlobalDef "Prelude.Vec" @> asNatLit)
+      <@ isDataType "Prelude.Bool" emptyl)
 
 asMux :: (Monad f) => Recognizer f Term (Term :*: Term :*: Term :*: Term)
 asMux = isGlobalDef "Prelude.ite" @> return <@> return <@> return <@> return

src/Verifier/SAW/SCTypeCheck.hs

@@ -215,10 +215,10 @@ scTypeCheck' sc env t0 = State.evalStateT (memo t0) Map.empty
           tp' <- whnf tp
           tys <- traverse memo vs
           V.mapM_ (\ty -> checkEqTy ty tp' (ArrayTypeMismatch tp' ty)) tys
-          io $ scFlatTermF sc (DataTypeApp preludeVecIdent [n, tp'])
-        FloatLit{}  -> io $ scFlatTermF sc (DataTypeApp preludeFloatIdent  [])
-        DoubleLit{} -> io $ scFlatTermF sc (DataTypeApp preludeDoubleIdent [])
-        StringLit{} -> io $ scFlatTermF sc (DataTypeApp preludeStringIdent [])
+          io $ scVecType sc n tp'
+        FloatLit{}  -> io $ scFlatTermF sc preludeFloatType
+        DoubleLit{} -> io $ scFlatTermF sc preludeDoubleType
+        StringLit{} -> io $ scFlatTermF sc preludeStringType
         ExtCns ec   -> whnf $ ecType ec
 
 argMatch :: SharedContext -> Term -> Term -> IO Bool

src/Verifier/SAW/SharedTerm.hs

@@ -584,10 +584,11 @@ scTypeOf' sc env t0 = State.evalStateT (memo t0) Map.empty
         NatLit _ -> lift $ scNatType sc
         ArrayValue tp vs -> lift $ do
           n <- scNat sc (fromIntegral (V.length vs))
-          scFlatTermF sc (DataTypeApp preludeVecIdent [n, tp])
-        FloatLit{}  -> lift $ scFlatTermF sc (DataTypeApp preludeFloatIdent  [])
-        DoubleLit{} -> lift $ scFlatTermF sc (DataTypeApp preludeDoubleIdent [])
-        StringLit{} -> lift $ scFlatTermF sc (DataTypeApp preludeStringIdent [])
+          vec_f <- scFlatTermF sc preludeVecTypeFun
+          scApplyAll sc vec_f [n, tp]
+        FloatLit{}  -> lift $ scFlatTermF sc preludeFloatType
+        DoubleLit{} -> lift $ scFlatTermF sc preludeDoubleType
+        StringLit{} -> lift $ scFlatTermF sc preludeStringType
         ExtCns ec   -> return $ ecType ec
 
 --------------------------------------------------------------------------------
@@ -1046,10 +1047,12 @@ scBoolType :: SharedContext -> IO Term
 scBoolType sc = scDataTypeApp sc "Prelude.Bool" []
 
 scNatType :: SharedContext -> IO Term
-scNatType sc = scDataTypeApp sc preludeNatIdent []
+scNatType sc = scFlatTermF sc preludeNatType
 
 scVecType :: SharedContext -> Term -> Term -> IO Term
-scVecType sc n e = scDataTypeApp sc "Prelude.Vec" [n, e]
+scVecType sc n e =
+  do vec_f <- scFlatTermF sc preludeVecTypeFun
+     scApplyAll sc vec_f [n, e]
 
 scNot :: SharedContext -> Term -> IO Term
 scNot sc t = scGlobalApply sc "Prelude.not" [t]
@@ -1137,7 +1140,7 @@ scMaxNat sc x y = scGlobalApply sc "Prelude.maxNat" [x,y]
 -- Primitive operations on Integer
 
 scIntegerType :: SharedContext -> IO Term
-scIntegerType sc = scDataTypeApp sc "Prelude.Integer" []
+scIntegerType sc = scFlatTermF sc preludeIntegerType
 
 -- primitive intAdd/intSub/intMul/intDiv/intMod :: Integer -> Integer -> Integer;
 scIntAdd, scIntSub, scIntMul, scIntDiv, scIntMod, scIntMax, scIntMin

src/Verifier/SAW/Simulator/Prims.hs

@@ -173,6 +173,7 @@ constMap bp = Map.fromList
   , ("Prelude.equalNat", equalNatOp (bpBool bp))
   , ("Prelude.ltNat", ltNatOp (bpBool bp))
   -- Integers
+  , ("Prelude.Integer", VIntType)
   , ("Prelude.intAdd", intBinOp "intAdd" (bpIntAdd bp))
   , ("Prelude.intSub", intBinOp "intSub" (bpIntSub bp))
   , ("Prelude.intMul", intBinOp "intMul" (bpIntMul bp))
@@ -194,6 +195,7 @@ constMap bp = Map.fromList
   , ("Prelude.intMin", intBinOp "intMin" (bpIntMin bp))
   , ("Prelude.intMax", intBinOp "intMax" (bpIntMax bp))
   -- Vectors
+  , ("Prelude.Vec", vecTypeOp)
   , ("Prelude.gen", genOp)
   , ("Prelude.atWithDefault", atWithDefaultOp bp)
   , ("Prelude.upd", updOp bp)
@@ -473,6 +475,10 @@ natCaseOp =
 
 --------------------------------------------------------------------------------
 
+-- Vec :: (n :: Nat) -> (a :: sort 0) -> sort 0;
+vecTypeOp :: VMonad l => Value l
+vecTypeOp = pureFun $ \n -> pureFun $ \a -> VVecType n a
+
 -- gen :: (n :: Nat) -> (a :: sort 0) -> (Nat -> a) -> Vec n a;
 genOp :: VMonadLazy l => Value l
 genOp =

src/Verifier/SAW/Simulator/Value.hs

@@ -63,6 +63,8 @@ data Value l
   | VEmptyType
   | VFieldType FieldName !(Value l) !(Value l)
   | VDataType !Ident [Value l]
+  | VIntType
+  | VVecType (Value l) (Value l)
   | VType -- ^ Other unknown type
   | VExtra (Extra l)
 
@@ -143,6 +145,9 @@ instance Show (Extra l) => Show (Value l) where
       VDataType s vs
         | null vs    -> shows s
         | otherwise  -> shows s . showList vs
+      VIntType       -> showString "Integer"
+      VVecType n a   -> showString "Vec " . showParen True (showsPrec p n)
+                        . showString " " . showParen True (showsPrec p a)
       VType          -> showString "_"
       VExtra x       -> showsPrec p x
     where
@@ -192,7 +197,7 @@ asFiniteTypeValue :: Value l -> Maybe FiniteType
 asFiniteTypeValue v =
   case v of
     VDataType "Prelude.Bool" [] -> return FTBit
-    VDataType "Prelude.Vec" [VNat n, v1] -> do
+    VVecType (VNat n) v1 -> do
       t1 <- asFiniteTypeValue v1
       return (FTVec (fromInteger n) t1)
     VUnitType -> return (FTTuple [])

src/Verifier/SAW/Typechecker.hs

@@ -294,16 +294,16 @@ inferTerm tc uut = do
     Un.Paren _ t -> uncurry TypedValue <$> inferTypedValue tc t
     Un.NatLit p i | i < 0 -> fail $ ppPos p ++ " Unexpected negative natural number literal."
                   | otherwise -> pure $ TypedValue (TCF (NatLit i)) nattp
-      where nattp = TCF (DataTypeApp preludeNatIdent [])
+      where nattp = TCF preludeNatType
     Un.StringLit _ s -> pure $ TypedValue (TCF (StringLit s)) strtp
-      where strtp = TCF (DataTypeApp preludeStringIdent [])
+      where strtp = TCF preludeStringType
     Un.VecLit p [] -> tcFail p "SAWCore parser does not support empty array literals."
     Un.VecLit _ (h:l) -> do
       (v,tp) <- inferTypedValue tc h
       vl <- traverse (\ u -> tcTerm tc u tp) l
       let vals = V.fromList (v:vl)
       let n = TCF (NatLit (toInteger (V.length vals)))
-      return $ TypedValue (TCF (ArrayValue tp vals)) (TCF (DataTypeApp preludeVecIdent [n,tp]))
+      return $ TypedValue (TCF (ArrayValue tp vals)) (TCApp (TCApp (TCF preludeVecTypeFun) n) tp)
     Un.BadTerm p -> fail $ "Encountered bad term from position " ++ show p
 
 -- | @checkTypeSubtype tc p x y@ checks that @x@ is a subtype of @y@.
@@ -363,10 +363,9 @@ topEval :: TCRef s v -> TC s v
 topEval r = eval (internalError $ "Cyclic error in top level" ++ show r) r
 
 evalDataType :: TCRefDataType s -> TC s TCDataType
-evalDataType (DataTypeGen n tp ctp isPrim) =
+evalDataType (DataTypeGen n tp ctp) =
   DataTypeGen n <$> topEval tp
                 <*> traverse (traverse topEval) ctp
-                <*> pure isPrim
 
 evalDef :: TCRefDef s -> TC s TCDef
 evalDef (DefGen nm qual tpr elr) =
@@ -381,11 +380,10 @@ data CompletionContext
 completeDataType :: CompletionContext
                  -> TCDataType
                  -> DataType
-completeDataType cc (DataTypeGen dt tp cl isPrim) =
+completeDataType cc (DataTypeGen dt tp cl) =
   DataType { dtName = dt
            , dtType = completeTerm cc (termFromTCDTType tp)
            , dtCtors = fmap (completeTerm cc . termFromTCCtorType dt) <$> cl
-           , dtIsPrimitive = isPrim
            }
 
 completeDef :: CompletionContext -> TCDef -> Def
@@ -684,19 +682,13 @@ parseDecl eqnMap d = do
         let def = DefGen (mkIdent mnm nm) qual rtp eqs
         isCtx  %= insertDef [Nothing] True (LocalLoc p) def
         isDefs %= (def:)
-    Un.PrimDataDecl psym utp -> do
-      let dti = mkIdent mnm (val psym)
-      dtp <- addPending (val psym) (\tc -> tcDTType tc utp)
-      let dt = DataTypeGen dti dtp [] True
-      isCtx %= insertDataType [Nothing] True (LocalLoc (pos psym)) dt
-      isTypes %= (DataTypeGen dti dtp [] True :)
     Un.DataDecl psym utp ucl -> do
       let dti = mkIdent mnm (val psym)
       dtp <- addPending (val psym) (\tc -> tcDTType tc utp)
       cl  <- traverse (parseCtor dti) ucl
-      let dt = DataTypeGen dti dtp cl False
+      let dt = DataTypeGen dti dtp cl
       isCtx   %= insertDataType [Nothing] True (LocalLoc (pos psym)) dt
-      isTypes %= (DataTypeGen dti dtp (view _3 <$> cl) False :)
+      isTypes %= (DataTypeGen dti dtp (view _3 <$> cl) :)
     Un.TermDef{} -> return ()
 
 parseImport :: Map ModuleName Module
@@ -726,7 +718,7 @@ parseImport moduleMap (Un.Import q (PosPair p nm) mAsName mcns) = do
           let addInModule = includeNameInModule mcns cnm
           (addInModule,loc,) . Ctor cnm <$> addPending (identName cnm) cfn
         let dtuse = includeNameInModule mcns dtnm
-        isCtx %= insertDataType mnml dtuse loc (DataTypeGen dtnm dtr cl (dtIsPrimitive dt))
+        isCtx %= insertDataType mnml dtuse loc (DataTypeGen dtnm dtr cl)
       -- Add definitions to module.
       forOf_ folded (moduleDefs m) $ \def -> do
         let inm = identName (defIdent def)

src/Verifier/SAW/Typechecker/Context.hs

@@ -189,7 +189,6 @@ data DataTypeGen t c =
    DataTypeGen { dtgName :: Ident
                , dtgType :: t
                , dtgCtors :: [c]
-               , dtgIsPrimitive :: Bool
                }
 
 type TCDataTypeGen r = DataTypeGen (r TCDTType) (Ctor (r TCCtorType))
@@ -403,9 +402,9 @@ insertDataType :: [Maybe ModuleName] -- ^ List of namespaces for symbols.
                -> DataTypeGen (TCRef s TCDTType) (Bool, Loc, TCRefCtor s)
                -> GlobalContext s
                -> GlobalContext s
-insertDataType mnml vis loc (DataTypeGen dtnm dtp cl isPrim) gc =
+insertDataType mnml vis loc (DataTypeGen dtnm dtp cl) gc =
     gc { gcMap = insertAllBindings bindings (gcMap gc) }
-  where dt = DataTypeGen dtnm dtp (view _3 <$> cl) isPrim
+  where dt = DataTypeGen dtnm dtp (view _3 <$> cl)
         dtBindings = untypedBindings vis mnml (identName dtnm) (DataTypeBinding loc dt)
         cBindings (b, cloc, c@(Ctor cnm _)) =
           untypedBindings b mnml (identName cnm) (CtorBinding cloc dt c)
@@ -533,7 +532,7 @@ resolveIdent tc0 (PosPair p ident) = go tc0
         go (TopContext gc) = do
           gb <- resolveGlobalIdent gc (PosPair p ident)
           case gb of
-            DataTypeBinding _ (DataTypeGen dt rtp _ _) -> do
+            DataTypeBinding _ (DataTypeGen dt rtp _) -> do
               ftp <- eval p rtp
               case ftp of
                 FPResult s -> pure $ TypedValue (TCF (DataTypeApp dt [])) (TCF (Sort s))

src/Verifier/SAW/Typechecker/Unification.hs

@@ -53,6 +53,7 @@ import Verifier.SAW.Typechecker.Context
 import Verifier.SAW.Typechecker.Monad
 import Verifier.SAW.Typechecker.Simplification
 import Verifier.SAW.TypedAST (ppParens, zipWithFlatTermF, ppFlatTermF, defaultPPOpts, Prec(..))
+import Verifier.SAW.Prelude.Constants
 import qualified Verifier.SAW.UntypedAST as Un
 
 -- | Return true if set has duplicates.
@@ -287,7 +288,7 @@ indexUnPat upat =
       let vfn upl = UPatF (pos pnm) (UPCtor c upl)
       first vfn <$> indexPiPats pl tp
     Un.PString p s -> do
-      tpv <- mkVar (show (Un.ppPat PrecNone upat)) (UTF (DataTypeApp "Prelude.String" []))
+      tpv <- mkVar (show (Un.ppPat PrecNone upat)) (UTF preludeStringType)
       return (UPatF p (UPString s), tpv)
 
 -- | Variable, the type, and name, and type.

src/Verifier/SAW/UntypedAST.hs

@@ -244,7 +244,6 @@ data DeclQualifier
 data Decl
    = TypeDecl DeclQualifier [(PosPair String)] Term
    | DataDecl (PosPair String) Term [CtorDecl]
-   | PrimDataDecl (PosPair String) Term
    | TermDef (PosPair String) [Pat] Term
   deriving (Show)