Avoid unnecessary uses of GlobalDef constructor.

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/Rewriter.hs

@@ -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
@@ -465,7 +464,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

@@ -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