Replace GlobalDef term constructor with Primitive.

The new `Primitive` constructor is for global constants that do
not have definitions. Instead of an `Ident`, they are identified
with an `ExtCns`, which includes a `NameInfo` and a type.

Fixes #162.

Author: Brian Huffman

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/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) =>

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

@@ -389,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)) =

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

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,