From c2f171c0df38f2cee7e18d61fa21a0ddf4f4ec90 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 24 Aug 2021 16:50:32 -0700 Subject: [PATCH] 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 | 8 +++-- saw-core/src/Verifier/SAW/Recognizer.hs | 4 +-- saw-core/src/Verifier/SAW/Rewriter.hs | 2 +- saw-core/src/Verifier/SAW/SCTypeCheck.hs | 8 ++++- saw-core/src/Verifier/SAW/SharedTerm.hs | 36 ++++++++++++++------ saw-core/src/Verifier/SAW/Simulator.hs | 12 ++++--- saw-core/src/Verifier/SAW/Simulator/Value.hs | 6 ++++ saw-core/src/Verifier/SAW/Term/Functor.hs | 2 +- 8 files changed, 56 insertions(+), 22 deletions(-) diff --git a/saw-core/src/Verifier/SAW/ExternalFormat.hs b/saw-core/src/Verifier/SAW/ExternalFormat.hs index 80569f2a72..83de93cf47 100644 --- a/saw-core/src/Verifier/SAW/ExternalFormat.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/Recognizer.hs b/saw-core/src/Verifier/SAW/Recognizer.hs index 591e4304ad..999f8d2c7d 100644 --- a/saw-core/src/Verifier/SAW/Recognizer.hs +++ b/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) diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs index 9ef85e1a1c..0b5e47ba9a 100644 --- a/saw-core/src/Verifier/SAW/Rewriter.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/SCTypeCheck.hs b/saw-core/src/Verifier/SAW/SCTypeCheck.hs index 6eb506993f..5a37090879 100644 --- a/saw-core/src/Verifier/SAW/SCTypeCheck.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs index 79b9ce023b..14b131a950 100644 --- a/saw-core/src/Verifier/SAW/SharedTerm.hs +++ b/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 $ diff --git a/saw-core/src/Verifier/SAW/Simulator.hs b/saw-core/src/Verifier/SAW/Simulator.hs index 61e986c281..d90bda99ff 100644 --- a/saw-core/src/Verifier/SAW/Simulator.hs +++ b/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) => diff --git a/saw-core/src/Verifier/SAW/Simulator/Value.hs b/saw-core/src/Verifier/SAW/Simulator/Value.hs index dc23351e69..cf4f67a2f2 100644 --- a/saw-core/src/Verifier/SAW/Simulator/Value.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/Term/Functor.hs b/saw-core/src/Verifier/SAW/Term/Functor.hs index 5c47a2a42e..94e5de38c2 100644 --- a/saw-core/src/Verifier/SAW/Term/Functor.hs +++ b/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)