Replace GlobalDef term constructor with Primitive.

saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs

@@ -202,7 +202,10 @@ flatTermFToExpr ::
   m Coq.Term
 flatTermFToExpr tf = -- traceFTermF "flatTermFToExpr" tf $
   case tf of
-    GlobalDef i   -> translateIdent i
+    Primitive (EC _ nmi _) ->
+      case nmi of
+        ModuleIdentifier i -> translateIdent i
+        ImportedName{} -> errorTermM "Invalid name for saw-core primitive"
     UnitValue     -> pure (Coq.Var "tt")
     UnitType      -> pure (Coq.Var "unit")
     PairValue x y -> Coq.App (Coq.Var "pair") <$> traverse translateTerm [x, y]

saw-core/src/Verifier/SAW/ExternalFormat.hs

@@ -132,7 +132,9 @@ scWriteExternal t0 =
                pure $ unwords ["Constant", show (ecVarIndex ec), show (ecType ec), show e]
         FTermF ftf     ->
           case ftf of
-            GlobalDef ident     -> pure $ unwords ["Global", show ident]
+            Primitive ec ->
+               do stashName ec
+                  pure $ unwords ["Primitive", show (ecVarIndex ec), show (ecType ec)]
             UnitValue           -> pure $ unwords ["Unit"]
             UnitType            -> pure $ unwords ["UnitT"]
             PairValue x y       -> pure $ unwords ["Pair", show x, show y]
@@ -229,7 +231,7 @@ scReadExternal sc input =
         ["Pi", s, t, e]     -> Pi (Text.pack s) <$> readIdx t <*> readIdx e
         ["Var", i]          -> pure $ LocalVar (read i)
         ["Constant",i,t,e]  -> Constant <$> readEC i t <*> readIdx e
-        ["Global", x]       -> pure $ FTermF (GlobalDef (parseIdent x))
+        ["Primitive", i, t] -> FTermF <$> (Primitive <$> readEC i t)
         ["Unit"]            -> pure $ FTermF UnitValue
         ["UnitT"]           -> pure $ FTermF UnitType
         ["Pair", x, y]      -> FTermF <$> (PairValue <$> readIdx x <*> readIdx y)

saw-core/src/Verifier/SAW/OpenTerm.hs

@@ -80,9 +80,10 @@ dataTypeOpenTerm d all_args = OpenTerm $ do
       Nothing -> throwTCError $ NoSuchDataType d
   typeInferComplete $ DataTypeApp d params args
 
--- | Build an 'OpenTermm' for a global name
+-- | Build an 'OpenTerm' for a global name.
 globalOpenTerm :: Ident -> OpenTerm
-globalOpenTerm = flatOpenTerm . GlobalDef
+globalOpenTerm ident =
+  OpenTerm (liftTCM scGlobalDef ident >>= typeInferComplete)
 
 -- | Apply an 'OpenTerm' to another
 applyOpenTerm :: OpenTerm -> OpenTerm -> OpenTerm

saw-core/src/Verifier/SAW/Prelude/Constants.hs

@@ -29,35 +29,17 @@ 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
-
 preludeArrayIdent :: Ident
 preludeArrayIdent =  mkIdent preludeModuleName "Array"
-
-preludeArrayTypeFun :: FlatTermF e
-preludeArrayTypeFun = GlobalDef preludeArrayIdent

saw-core/src/Verifier/SAW/Recognizer.hs

@@ -119,11 +119,17 @@ asFTermF :: Recognizer Term (FlatTermF Term)
 asFTermF (unwrapTermF -> FTermF ftf) = return ftf
 asFTermF _ = Nothing
 
+asModuleIdentifier :: Recognizer (ExtCns e) Ident
+asModuleIdentifier (EC _ nmi _) =
+  case nmi of
+    ModuleIdentifier ident -> Just ident
+    _ -> Nothing
+
 asGlobalDef :: Recognizer Term Ident
 asGlobalDef t =
   case unwrapTermF t of
-    FTermF (GlobalDef ident) -> pure ident
-    Constant (EC _ (ModuleIdentifier ident) _) _ -> pure ident
+    FTermF (Primitive ec) -> asModuleIdentifier ec
+    Constant ec _ -> asModuleIdentifier ec
     _ -> Nothing
 
 isGlobalDef :: Ident -> Recognizer Term ()

saw-core/src/Verifier/SAW/Rewriter.hs

@@ -627,7 +627,7 @@ rewriteSharedTermTypeSafe sc ss t0 =
           Sort{}           -> return ftf -- doesn't matter
           NatLit{}         -> return ftf -- doesn't matter
           ArrayValue t es  -> ArrayValue t <$> traverse rewriteAll es
-          GlobalDef{}      -> return ftf
+          Primitive{}      -> return ftf
           StringLit{}      -> return ftf
           ExtCns{}         -> return ftf
     rewriteTop :: (?cache :: Cache IO TermIndex Term) =>
@@ -700,9 +700,9 @@ replaceTerm sc ss (pat, repl) t = do
 -- If/then/else hoisting
 
 -- | Find all instances of Prelude.ite in the given term and hoist them
---   higher.  An if/then/else floats upward until it hits a binder that
+--   higher.  An if-then-else floats upward until it hits a binder that
 --   binds one of its free variables, or until it bubbles to the top of
---   the term.  When multiple if/then/else branches bubble to the same
+--   the term.  When multiple if-then-else branches bubble to the same
 --   place, they will be nested via a canonical term ordering.  This transformation
 --   also does rewrites by basic boolean identities.
 hoistIfs :: SharedContext
@@ -713,15 +713,15 @@ hoistIfs sc t = do
 
    let app x y = join (scTermF sc <$> (pure App <*> x <*> y))
    itePat <-
-          (scFlatTermF sc $ GlobalDef $ "Prelude.ite")
+          (scGlobalDef sc "Prelude.ite")
           `app`
-          (scTermF sc $ LocalVar 0)
+          (scLocalVar sc 0)
           `app`
-          (scTermF sc $ LocalVar 1)
+          (scLocalVar sc 1)
           `app`
-          (scTermF sc $ LocalVar 2)
+          (scLocalVar sc 2)
           `app`
-          (scTermF sc $ LocalVar 3)
+          (scLocalVar sc 3)
 
    rules <- map ruleOfTerm <$> mapM (scTypeOfGlobal sc)
               [ "Prelude.ite_true"

saw-core/src/Verifier/SAW/SCTypeCheck.hs

@@ -56,7 +56,6 @@ import qualified Data.Vector as V
 import Prelude hiding (mapM, maximum)
 
 import Verifier.SAW.Conversion (natConversions)
-import Verifier.SAW.Prelude.Constants
 import Verifier.SAW.Recognizer
 import Verifier.SAW.Rewriter
 import Verifier.SAW.SharedTerm
@@ -390,9 +389,8 @@ instance TypeInfer (TermF TypedTerm) where
 -- terms. Intuitively, this represents the case where each immediate subterm of
 -- a term has already been labeled with its (most general) type.
 instance TypeInfer (FlatTermF TypedTerm) where
-  typeInfer (GlobalDef d) =
-    do ty <- liftTCM scTypeOfGlobal d
-       typeCheckWHNF ty
+  typeInfer (Primitive ec) =
+    typeCheckWHNF $ typedVal $ ecType ec
   typeInfer UnitValue = liftTCM scUnitType
   typeInfer UnitType = liftTCM scSort (mkSort 0)
   typeInfer (PairValue (TypedTerm _ tx) (TypedTerm _ ty)) =
@@ -465,7 +463,7 @@ instance TypeInfer (FlatTermF TypedTerm) where
        tp' <- typeCheckWHNF tp
        forM_ vs $ \v_elem -> checkSubtype v_elem tp'
        liftTCM scVecType n tp'
-  typeInfer (StringLit{}) = liftTCM scFlatTermF preludeStringType
+  typeInfer (StringLit{}) = liftTCM scStringType
   typeInfer (ExtCns ec) =
     -- FIXME: should we check that the type of ecType is a sort?
     typeCheckWHNF $ typedVal $ ecType ec

saw-core/src/Verifier/SAW/SharedTerm.hs

@@ -927,7 +927,7 @@ scTypeOf' sc env t0 = State.evalStateT (memo t0) Map.empty
            -> State.StateT (Map TermIndex Term) IO Term
     ftermf tf =
       case tf of
-        GlobalDef d -> lift $ scTypeOfGlobal sc d
+        Primitive ec -> return $ ecType ec
         UnitValue -> lift $ scUnitType sc
         UnitType -> lift $ scSort sc (mkSort 0)
         PairValue x y -> do
@@ -972,9 +972,8 @@ 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))
-          vec_f <- scFlatTermF sc preludeVecTypeFun
-          scApplyAll sc vec_f [n, tp]
-        StringLit{} -> lift $ scFlatTermF sc preludeStringType
+          scVecType sc n tp
+        StringLit{} -> lift $ scStringType sc
         ExtCns ec   -> return $ ecType ec
 
 --------------------------------------------------------------------------------
@@ -1214,7 +1213,7 @@ scString sc s = scFlatTermF sc (StringLit s)
 
 -- | Create a term representing the primitive saw-core type @String@.
 scStringType :: SharedContext -> IO Term
-scStringType sc = scFlatTermF sc preludeStringType
+scStringType sc = scGlobalDef sc preludeStringIdent
 
 -- | Create a vector term from a type (as a 'Term') and a list of 'Term's of
 -- that type.
@@ -1489,9 +1488,7 @@ scVecType :: SharedContext
           -> Term -- ^ The length of the vector
           -> Term -- ^ The element type
           -> IO Term
-scVecType sc n e =
-  do vec_f <- scFlatTermF sc preludeVecTypeFun
-     scApplyAll sc vec_f [n, e]
+scVecType sc n e = scGlobalApply sc preludeVecIdent [n, e]
 
 -- | Create a term applying @Prelude.not@ to the given term.
 --
@@ -1694,7 +1691,7 @@ scMaxNat sc x y = scGlobalApply sc "Prelude.maxNat" [x,y]
 
 -- | Create a term representing the prelude Integer type.
 scIntegerType :: SharedContext -> IO Term
-scIntegerType sc = scFlatTermF sc preludeIntegerType
+scIntegerType sc = scGlobalDef sc preludeIntegerIdent
 
 -- | Create an integer constant term from an 'Integer'.
 scIntegerConst :: SharedContext -> Integer -> IO Term

saw-core/src/Verifier/SAW/Simulator.hs

@@ -139,7 +139,11 @@ evalTermF cfg lam recEval tf env =
                                   maybe (recEval t) id (simUninterpreted cfg tf ec')
     FTermF ftf              ->
       case ftf of
-        GlobalDef ident     -> simGlobal cfg ident
+        Primitive ec ->
+          do ec' <- traverse (fmap toTValue . recEval) ec
+             case ecName ec' of
+               ModuleIdentifier ident -> simGlobal cfg ident
+               _ -> simExtCns cfg tf ec'
         UnitValue           -> return VUnit
         UnitType            -> return $ TValue VUnitType
         PairValue x y       -> do tx <- recEvalDelay x

saw-core/src/Verifier/SAW/Term/Functor.hs

@@ -140,7 +140,8 @@ maxSort ss = maximum ss
 -- NB: If you add constructors to FlatTermF, make sure you update
 --     zipWithFlatTermF!
 data FlatTermF e
-  = GlobalDef !Ident  -- ^ Global variables are referenced by label.
+    -- | A primitive or axiom without a definition.
+  = Primitive !(ExtCns e)
 
     -- Tuples are represented as nested pairs, grouped to the right,
     -- terminated with unit at the end.
@@ -219,7 +220,8 @@ zipWithFlatTermF :: (x -> y -> z) -> FlatTermF x -> FlatTermF y ->
                     Maybe (FlatTermF z)
 zipWithFlatTermF f = go
   where
-    go (GlobalDef x) (GlobalDef y) | x == y = Just $ GlobalDef x
+    go (Primitive (EC xi xn xt)) (Primitive (EC yi _ yt))
+      | xi == yi = Just (Primitive (EC xi xn (f xt yt)))
 
     go UnitValue UnitValue = Just UnitValue
     go UnitType UnitType = Just UnitType
@@ -344,7 +346,7 @@ termToPat t =
     case unwrapTermF t of
       Constant ec _             -> Net.Atom (toAbsoluteName (ecName ec))
       App t1 t2                 -> Net.App (termToPat t1) (termToPat t2)
-      FTermF (GlobalDef d)      -> Net.Atom (identText d)
+      FTermF (Primitive ec)     -> Net.Atom (toAbsoluteName (ecName ec))
       FTermF (Sort s)           -> Net.Atom (Text.pack ('*' : show s))
       FTermF (NatLit _)         -> Net.Var
       FTermF (DataTypeApp c ps ts) ->

saw-core/src/Verifier/SAW/Term/Pretty.hs

@@ -63,7 +63,7 @@ import Verifier.SAW.Term.Functor
 -- * Doc annotations
 
 data SawStyle
-  = GlobalDefStyle
+  = PrimitiveStyle
   | ConstantStyle
   | ExtCnsStyle
   | LocalVarStyle
@@ -76,7 +76,7 @@ data SawStyle
 colorStyle :: SawStyle -> AnsiStyle
 colorStyle =
   \case
-    GlobalDefStyle -> mempty
+    PrimitiveStyle -> mempty
     ConstantStyle -> colorDull Blue
     ExtCnsStyle -> colorDull Red
     LocalVarStyle -> colorDull Green
@@ -422,7 +422,7 @@ ppDataType d (params, ((d_ctx,d_tp), ctors)) =
 ppFlatTermF :: Prec -> FlatTermF Term -> PPM SawDoc
 ppFlatTermF prec tf =
   case tf of
-    GlobalDef i   -> return $ annotate GlobalDefStyle $ ppIdent i
+    Primitive ec  -> annotate PrimitiveStyle <$> ppBestName (ecName ec)
     UnitValue     -> return "(-empty-)"
     UnitType      -> return "#(-empty-)"
     PairValue x y -> ppPair prec <$> ppTerm' PrecLambda x <*> ppTerm' PrecNone y
@@ -542,7 +542,7 @@ scTermCount doBinders t0 = execState (go [t0]) IntMap.empty
 shouldMemoizeTerm :: Term -> Bool
 shouldMemoizeTerm t =
   case unwrapTermF t of
-    FTermF GlobalDef{} -> False
+    FTermF Primitive{} -> False
     FTermF UnitValue -> False
     FTermF UnitType -> False
     FTermF (CtorApp _ [] []) -> False

saw-core/src/Verifier/SAW/Typechecker.hs

@@ -350,7 +350,12 @@ processDecls (Un.TypeDecl q (PosPair p nm) tp : rest) =
       void $ ensureSort $ typedType typed_tp
       mnm <- getModuleName
       let ident = mkIdent mnm nm
-      t <- liftTCM scFlatTermF (GlobalDef ident)
+      let nmi = ModuleIdentifier ident
+      i <- liftTCM scFreshGlobalVar
+      liftTCM scRegisterName i nmi
+      let def_tp = typedVal typed_tp
+      let ec = EC i nmi def_tp
+      t <- liftTCM scFlatTermF (Primitive ec)
       liftTCM scRegisterGlobal ident t
       liftTCM scModifyModule mnm $ \m ->
         insDef m $ Def { defIdent = ident,