Add a notion of "opaque constants".

These are just `Constant` terms that have no definition.
They are similar to `ExtCns`, except that they are not subject
to substitution.  As a consequence, opaque constants are allowed
to appear in the definition of other constants without being
abstracted over.  Opauqe constants never reduce, and must be
treated as unintepreted in proofs.

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

@@ -134,9 +134,12 @@ scWriteExternal t0 =
         Lambda s t e   -> pure $ unwords ["Lam", Text.unpack s, show t, show e]
         Pi s t e       -> pure $ unwords ["Pi", Text.unpack s, show t, show e]
         LocalVar i     -> pure $ unwords ["Var", show i]
-        Constant ec e  ->
+        Constant ec (Just e)  ->
             do stashName ec
                pure $ unwords ["Constant", show (ecVarIndex ec), show (ecType ec), show e]
+        Constant ec Nothing ->
+            do stashName ec
+               pure $ unwords ["ConstantOpaque", show (ecVarIndex ec), show (ecType ec)]
         FTermF ftf     ->
           case ftf of
             Primitive ec ->
@@ -295,7 +298,8 @@ scReadExternal sc input =
         ["Lam", x, t, e]    -> Lambda (Text.pack x) <$> readIdx t <*> readIdx e
         ["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
+        ["Constant",i,t,e]  -> Constant <$> readEC i t <*> (Just <$> readIdx e)
+        ["ConstantOpaque",i,t]  -> Constant <$> readEC i t <*> pure Nothing
         ["Primitive", i, t] -> FTermF <$> (Primitive <$> readPrimName i t)
         ["Unit"]            -> pure $ FTermF UnitValue
         ["UnitT"]           -> pure $ FTermF UnitType

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

@@ -313,8 +313,8 @@ asLocalVar :: Recognizer Term DeBruijnIndex
 asLocalVar (unwrapTermF -> LocalVar i) = return i
 asLocalVar _ = Nothing
 
-asConstant :: Recognizer Term (ExtCns Term, Term)
-asConstant (unwrapTermF -> Constant ec t) = return (ec, t)
+asConstant :: Recognizer Term (ExtCns Term, Maybe Term)
+asConstant (unwrapTermF -> Constant ec mt) = return (ec, mt)
 asConstant _ = Nothing
 
 asExtCns :: Recognizer Term (ExtCns Term)

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

@@ -360,7 +360,7 @@ ruleOfProp (R.asApplyAll -> (R.isGlobalDef intEqIdent -> Just (), [x, y])) ann =
   Just $ mkRewriteRule [] x y ann
 ruleOfProp (R.asApplyAll -> (R.isGlobalDef intModEqIdent -> Just (), [_, x, y])) ann =
   Just $ mkRewriteRule [] x y ann
-ruleOfProp (unwrapTermF -> Constant _ body) ann = ruleOfProp body ann
+ruleOfProp (unwrapTermF -> Constant _ (Just body)) ann = ruleOfProp body ann
 ruleOfProp (R.asEq -> Just (_, x, y)) ann =
   Just $ mkRewriteRule [] x y ann
 ruleOfProp (R.asEqTrue -> Just body) ann = ruleOfProp body ann

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

@@ -439,13 +439,19 @@ instance TypeInfer (TermF TypedTerm) where
          else
          error ("Context = " ++ show ctx)
          -- throwTCError (DanglingVar (i - length ctx))
-  typeInfer (Constant (EC _ n (TypedTerm req_tp req_tp_sort)) (TypedTerm _ tp)) =
+  typeInfer (Constant (EC _ n (TypedTerm req_tp req_tp_sort)) (Just (TypedTerm _ tp))) =
     do void (ensureSort req_tp_sort)
        -- NOTE: we do the subtype check here, rather than call checkSubtype, so
        -- that we can throw the custom BadConstType error on failure
        ok <- isSubtype tp req_tp
        if ok then return tp else
          throwTCError $ BadConstType n tp req_tp
+
+  typeInfer (Constant (EC _ _ (TypedTerm req_tp req_tp_sort)) Nothing) =
+    -- Constant with no body, just return the EC type
+    do void (ensureSort req_tp_sort)
+       return req_tp
+
   typeInferComplete tf =
     TypedTerm <$> liftTCM scTermF (fmap typedVal tf) <*> typeInfer tf
 

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

@@ -101,6 +101,7 @@ module Verifier.SAW.SharedTerm
   , scLocalVar
   , scConstant
   , scConstant'
+  , scOpaqueConstant
   , scLookupDef
     -- *** Functions and function application
   , scApply
@@ -840,7 +841,7 @@ scWhnf sc t0 =
                                                                      args' <- mapM memo args
                                                                      t' <- scDataTypeAppParams sc d ps' args'
                                                                      foldM reapply t' xs
-    go xs                     (asConstant -> Just (_,body))     = do go xs body
+    go xs                     (asConstant -> Just (_,Just body)) = go xs body
     go xs                     t                                 = foldM reapply t xs
 
     betaReduce :: (?cache :: Cache IO TermIndex Term) =>
@@ -888,8 +889,9 @@ scConvertibleEval sc eval unfoldConst tm1 tm2 = do
 
        goF :: Cache IO TermIndex Term -> TermF Term -> TermF Term -> IO Bool
 
-       goF c (Constant _ x) y | unfoldConst = join (goF c <$> whnf c x <*> return y)
-       goF c x (Constant _ y) | unfoldConst = join (goF c <$> return x <*> whnf c y)
+       goF _c (Constant ecx _) (Constant ecy _) | ecVarIndex ecx == ecVarIndex ecy = pure True
+       goF c (Constant _ (Just x)) y | unfoldConst = join (goF c <$> whnf c x <*> return y)
+       goF c x (Constant _ (Just y)) | unfoldConst = join (goF c <$> return x <*> whnf c y)
 
        goF c (FTermF ftf1) (FTermF ftf2) =
                case zipWithFlatTermF (go c) ftf1 ftf2 of
@@ -1469,7 +1471,7 @@ scConstant sc name rhs ty =
      rhs' <- scAbstractExts sc ecs rhs
      ty' <- scFunAll sc (map ecType ecs) ty
      ec <- scFreshEC sc name ty'
-     t <- scTermF sc (Constant ec rhs')
+     t <- scTermF sc (Constant ec (Just rhs'))
      args <- mapM (scFlatTermF sc . ExtCns) ecs
      scApplyAll sc t args
 
@@ -1492,11 +1494,25 @@ scConstant' sc nmi rhs ty =
      i <- scFreshGlobalVar sc
      scRegisterName sc i nmi
      let ec = EC i nmi ty'
-     t <- scTermF sc (Constant ec rhs')
+     t <- scTermF sc (Constant ec (Just rhs'))
      args <- mapM (scFlatTermF sc . ExtCns) ecs
      scApplyAll sc t args
 
 
+-- | Create an abstract and opaque constant with the specified name and type.
+--   Such a constant has no definition and, unlike an @ExtCns@, is not subject
+--   to substitution.
+scOpaqueConstant ::
+  SharedContext ->
+  NameInfo ->
+  Term {- ^ type of the constant -} ->
+  IO Term
+scOpaqueConstant sc nmi ty =
+  do i <- scFreshGlobalVar sc
+     scRegisterName sc i nmi
+     let ec = EC i nmi ty
+     scTermF sc (Constant ec Nothing)
+
 -- | Create a function application term from a global identifier and a list of
 -- arguments (as 'Term's).
 scGlobalApply :: SharedContext -> Ident -> [Term] -> IO Term
@@ -2311,7 +2327,7 @@ getAllExtSet t = snd $ getExtCns (IntSet.empty, Set.empty) t
           getExtCns acc (Unshared tf') =
             foldl' getExtCns acc tf'
 
-getConstantSet :: Term -> Map VarIndex (NameInfo, Term, Term)
+getConstantSet :: Term -> Map VarIndex (NameInfo, Term, Maybe Term)
 getConstantSet t = snd $ go (IntSet.empty, Map.empty) t
   where
     go acc@(idxs, names) (STApp{ stAppIndex = i, stAppTermF = tf})
@@ -2481,13 +2497,13 @@ scUnfoldConstantSet sc b names t0 = do
   let go :: Term -> IO Term
       go t@(Unshared tf) =
         case tf of
-          Constant (EC idx _ _) rhs
+          Constant (EC idx _ _) (Just rhs)
             | Set.member idx names == b -> go rhs
             | otherwise                 -> return t
           _ -> Unshared <$> traverse go tf
       go t@(STApp{ stAppIndex = idx, stAppTermF = tf }) = useCache cache idx $
         case tf of
-          Constant (EC ecidx _ _) rhs
+          Constant (EC ecidx _ _) (Just rhs)
             | Set.member ecidx names == b -> go rhs
             | otherwise                   -> return t
           _ -> scTermF sc =<< traverse go tf
@@ -2505,13 +2521,13 @@ scUnfoldConstantSet' sc b names t0 = do
   let go :: Term -> ChangeT IO Term
       go t@(Unshared tf) =
         case tf of
-          Constant (EC idx _ _) rhs
+          Constant (EC idx _ _) (Just rhs)
             | Set.member idx names == b -> taint (go rhs)
             | otherwise                 -> pure t
           _ -> whenModified t (return . Unshared) (traverse go tf)
       go t@(STApp{ stAppIndex = idx, stAppTermF = tf }) =
         case tf of
-          Constant (EC ecidx _ _) rhs
+          Constant (EC ecidx _ _) (Just rhs)
             | Set.member ecidx names == b -> taint (go rhs)
             | otherwise                   -> pure t
           _ -> useChangeCache tcache idx $

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

@@ -31,9 +31,7 @@ module Verifier.SAW.Simulator
 
 import Prelude hiding (mapM)
 
-#if !MIN_VERSION_base(4,8,0)
-import Control.Applicative ((<$>))
-#endif
+import Control.Applicative ((<|>))
 import Control.Monad (foldM, liftM)
 import Control.Monad.Trans.Except
 import Control.Monad.Trans.Maybe
@@ -42,6 +40,7 @@ import Control.Monad.Identity (Identity)
 import qualified Control.Monad.State as State
 import Data.Foldable (foldlM)
 import qualified Data.Set as Set
+import Data.Maybe (fromMaybe)
 import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.IntMap (IntMap)
@@ -150,7 +149,9 @@ evalTermF cfg lam recEval tf env =
 
     LocalVar i              -> force (fst (env !! i))
     Constant ec t           -> do ec' <- traverse evalType ec
-                                  maybe (recEval t) id (simConstant cfg tf ec')
+                                  fromMaybe
+                                    (simNeutral cfg env (NeutralConstant ec))
+                                    (simConstant cfg tf ec' <|> (recEval <$> t))
     FTermF ftf              ->
       case ftf of
         Primitive pn ->
@@ -521,7 +522,8 @@ mkMemoLocal cfg memoClosed t env = go memoClosed t
         Lambda _ t1 _   -> go memo t1
         Pi _ t1 _       -> go memo t1
         LocalVar _      -> return memo
-        Constant _ t1   -> go memo t1
+        Constant _ Nothing -> return memo -- TODO? is this right?
+        Constant _ (Just t1) -> go memo t1
 
 {-# SPECIALIZE evalLocalTermF ::
   Show (Extra l) =>

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

@@ -117,6 +117,8 @@ data NeutralTerm
       Term   -- recursor value
       [Term] -- indices for the inductive type
       NeutralTerm -- argument being elminated
+  | NeutralConstant -- A constant value with no definition
+      (ExtCns Term)
 
 type Thunk l = Lazy (EvalM l) (Value l)
 
@@ -379,6 +381,8 @@ neutralToTerm = loop
     Unshared (FTermF (RecursorApp r ixs (loop x)))
   loop (NeutralRecursor r ixs x) =
     Unshared (FTermF (RecursorApp (loop r) ixs x))
+  loop (NeutralConstant ec) =
+    Unshared (Constant ec Nothing)
 
 neutralToSharedTerm :: SharedContext -> NeutralTerm -> IO Term
 neutralToSharedTerm sc = loop
@@ -400,6 +404,8 @@ neutralToSharedTerm sc = loop
   loop (NeutralRecursorArg r ixs nt) =
     do tm <- loop nt
        scFlatTermF sc (RecursorApp r ixs tm)
+  loop (NeutralConstant ec) =
+    do scTermF sc (Constant ec Nothing)
 
 ppNeutral :: PPOpts -> NeutralTerm -> SawDoc
 ppNeutral opts = ppTerm opts . neutralToTerm

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

@@ -333,7 +333,7 @@ data TermF e
       -- ^ The type of a (possibly) dependent function
     | LocalVar !DeBruijnIndex
       -- ^ Local variables are referenced by deBruijn index.
-    | Constant !(ExtCns e) !e
+    | Constant !(ExtCns e) !(Maybe e)
       -- ^ An abstract constant packaged with its type and definition.
       -- The body and type should be closed terms.
   deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic)