From 18ca05ad89b74f2c4c79937e3b83e695f1965bd0 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Fri, 1 Sep 2023 18:38:29 -0700 Subject: [PATCH] Refactored saw-core-coq (#1928) * Changed the type-checker to *not* normalize argument types in lambdas and pis when they are type-checked, in order to make the Coq translation work in cases where these argument types have identifiers that translate to alternate Coq definitions * added the termIsClosed function to test if a SAW core term is closed * refactored the saw-core-coq translator so that all the local variable information is in a reader effect and not a state effect, making it clearer where in the translator code variables are bound; also fixed #1927 * replaced llvmZeroInitValue with a new function translateZeroInit that directly translates an LLVM zero initializer to a Heapster permission + SAW core term, so that we use repeatBVVec in the SAW term rather than a giant vector literal * updated mbox_proofs.v after changes to the Coq translator * renamed askTrr and localTrr to askTR and localTR * replaced a number of equality tests on the free variables of terms against emptyBitSet with the new termIsClosed function * replaced checkGroundTerm with the now standard termIsClosed function * whoops, fixed a few lingering bugs related to using termIsClosed * made a few fixes to make the code more readable * a few more tweaks to make the code look nicer * finished writing a comment on withSAWVar * indentation change requested by review --- heapster-saw/examples/mbox_proofs.v | 2 +- .../Verifier/SAW/Heapster/LLVMGlobalConst.hs | 45 +- .../src/Verifier/SAW/Translation/Coq.hs | 2 +- .../SAW/Translation/Coq/CryptolModule.hs | 8 +- .../Verifier/SAW/Translation/Coq/SAWModule.hs | 14 +- .../src/Verifier/SAW/Translation/Coq/Term.hs | 482 ++++++++++-------- saw-core/src/Verifier/SAW/Rewriter.hs | 7 +- saw-core/src/Verifier/SAW/SCTypeCheck.hs | 22 +- saw-core/src/Verifier/SAW/SharedTerm.hs | 8 +- saw-core/src/Verifier/SAW/Simulator.hs | 12 +- saw-core/src/Verifier/SAW/Term/Functor.hs | 6 +- saw-core/src/Verifier/SAW/Term/Pretty.hs | 2 +- saw-core/src/Verifier/SAW/Typechecker.hs | 11 +- saw-core/src/Verifier/SAW/TypedAST.hs | 2 +- saw-core/tests/src/Tests/Parser.hs | 7 +- src/SAWScript/Builtins.hs | 11 +- src/SAWScript/Proof.hs | 10 +- 17 files changed, 366 insertions(+), 285 deletions(-) diff --git a/heapster-saw/examples/mbox_proofs.v b/heapster-saw/examples/mbox_proofs.v index 7cba5315ee..6c3cc37968 100644 --- a/heapster-saw/examples/mbox_proofs.v +++ b/heapster-saw/examples/mbox_proofs.v @@ -64,7 +64,7 @@ Proof. (bvSub 64 i strt) len (bvSub 64 bv64_128 strt) - e + _1 pf1)) as H. rewrite bvAdd_Sub_cancel. intros H. rewrite (UIP_bool _ _ H pf). diff --git a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs index f470783359..66f301fca4 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs @@ -54,6 +54,14 @@ bvVecValueOpenTerm w tp ts def_tm = def_tm, natOpenTerm (natValue w), bvLitOfIntOpenTerm (intValue w) (fromIntegral $ length ts)] +-- | Helper function to build a SAW core term of type @BVVec w len a@, i.e., a +-- bitvector-indexed vector, containing a single repeated value +repeatBVVecOpenTerm :: NatRepr w -> OpenTerm -> OpenTerm -> OpenTerm -> + OpenTerm +repeatBVVecOpenTerm w len tp t = + applyOpenTermMulti (globalOpenTerm "Prelude.repeatBVVec") + [natOpenTerm (natValue w), len, tp, t] + -- | The information needed to translate an LLVM global to Heapster data LLVMTransInfo = LLVMTransInfo { llvmTransInfoEnv :: PermEnv, @@ -111,8 +119,7 @@ translateLLVMValue w _ (L.ValArray tp elems) = -- Generate a default element of type tp using the zero initializer; this is -- currently needed by bvVecValueOpenTerm - def_v <- llvmZeroInitValue tp - (_,def_tm) <- translateLLVMValue w tp def_v + (_,def_tm) <- translateZeroInit w tp -- Finally, build our array shape and SAW core value return (PExpr_ArrayShape (bvInt $ fromIntegral $ length elems) sh_len sh, @@ -150,7 +157,7 @@ translateLLVMValue w tp (L.ValString bytes) = translateLLVMValue w _ (L.ValConstExpr ce) = translateLLVMConstExpr w ce translateLLVMValue w tp L.ValZeroInit = - llvmZeroInitValue tp >>= translateLLVMValue w tp + translateZeroInit w tp translateLLVMValue _ _ v = traceAndZeroM ("translateLLVMValue does not yet handle:\n" ++ ppLLVMValue v) @@ -218,14 +225,30 @@ translateLLVMGEP _ tp vtrans ixs isZeroIdx _ = False -- | Build an LLVM value for a @zeroinitializer@ field of the supplied type -llvmZeroInitValue :: L.Type -> LLVMTransM (L.Value) -llvmZeroInitValue (L.PrimType (L.Integer _)) = return $ L.ValInteger 0 -llvmZeroInitValue (L.Array len tp) = - L.ValArray tp <$> replicate (fromIntegral len) <$> llvmZeroInitValue tp -llvmZeroInitValue (L.PackedStruct tps) = - L.ValPackedStruct <$> zipWith L.Typed tps <$> mapM llvmZeroInitValue tps -llvmZeroInitValue tp = - traceAndZeroM ("llvmZeroInitValue cannot handle type:\n" +translateZeroInit :: (1 <= w, KnownNat w) => NatRepr w -> L.Type -> + LLVMTransM (PermExpr (LLVMShapeType w), OpenTerm) +translateZeroInit w tp@(L.PrimType (L.Integer _)) = + translateLLVMValue w tp (L.ValInteger 0) +translateZeroInit w (L.Array len tp) = + -- First, translate the zero element and its type + do (sh, elem_tm) <- translateZeroInit w tp + (_, saw_tp) <- translateLLVMType w tp + + -- Compute the array stride as the length of the element shape + sh_len_expr <- lift $ llvmShapeLength sh + sh_len <- fromInteger <$> lift (bvMatchConstInt sh_len_expr) + + let arr_len = bvInt $ fromIntegral len + let saw_len = bvLitOfIntOpenTerm (intValue w) (fromIntegral len) + return (PExpr_ArrayShape arr_len sh_len sh, + repeatBVVecOpenTerm w saw_len saw_tp elem_tm) + +translateZeroInit w (L.PackedStruct tps) = + mapM (translateZeroInit w) tps >>= \(unzip -> (shs,ts)) -> + return (foldr PExpr_SeqShape PExpr_EmptyShape shs, tupleOpenTerm ts) + +translateZeroInit _ tp = + traceAndZeroM ("translateZeroInit cannot handle type:\n" ++ show (L.ppType tp)) -- | Top-level call to 'translateLLVMValue', running the 'LLVMTransM' monad diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs index 1d8c99bbd7..fd781cd27c 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs +++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs @@ -121,7 +121,7 @@ translateTermAsDeclImports configuration name t tp = do doc <- TermTranslation.translateDefDoc configuration - (TermTranslation.TranslationReader Nothing) + Nothing [] name t tp return $ vcat [preamble configuration, hardline <> doc] diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs index 5af77b41ea..c736b7a65c 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs +++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs @@ -3,7 +3,7 @@ module Verifier.SAW.Translation.Coq.CryptolModule where -import Control.Lens (over, set, view) +import Control.Lens (over, view) import Control.Monad (forM) import Control.Monad.State (modify) import qualified Data.Map as Map @@ -27,9 +27,7 @@ translateTypedTermMap defs = forM defs translateAndRegisterEntry translateAndRegisterEntry (name, t, tp) = do let nameStr = unpackIdent (nameIdent name) decl <- - TermTranslation.withLocalTranslationState $ - do modify $ set TermTranslation.localEnvironment [nameStr] - t_trans <- TermTranslation.translateTerm t + do t_trans <- TermTranslation.translateTerm t tp_trans <- TermTranslation.translateTerm tp return $ TermTranslation.mkDefinition nameStr t_trans tp_trans modify $ over TermTranslation.globalDeclarations (nameStr :) @@ -55,7 +53,7 @@ translateCryptolModule sc env configuration globalDecls (CryptolModule _ tm) = (reverse . view TermTranslation.topLevelDeclarations . snd <$> TermTranslation.runTermTranslationMonad configuration - (TermTranslation.TranslationReader Nothing) -- TODO: this should be Just no? + Nothing -- TODO: this should be Just no? globalDecls [] (translateTypedTermMap defs)) diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs index 60c7c617c9..eca5a410f3 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs +++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs @@ -42,14 +42,14 @@ import Verifier.SAW.Translation.Coq.Monad -- import Debug.Trace type ModuleTranslationMonad m = - M.TranslationMonad TermTranslation.TranslationReader () m + M.TranslationMonad (Maybe ModuleName) () m runModuleTranslationMonad :: M.TranslationConfiguration -> Maybe ModuleName -> (forall m. ModuleTranslationMonad m => m a) -> Either (M.TranslationError Term) (a, ()) runModuleTranslationMonad configuration modName = - M.runTranslationMonad configuration (TermTranslation.TranslationReader modName) () + M.runTranslationMonad configuration modName () dropPi :: Coq.Term -> Coq.Term dropPi (Coq.Pi (_ : t) r) = Coq.Pi t r @@ -93,22 +93,22 @@ translateDataType (DataType {..}) = translateNamed name = do let inductiveName = name (inductiveParameters, inductiveIndices) <- - liftTermTranslationMonad $ do - ps <- TermTranslation.translateParams dtParams - ixs <- TermTranslation.translateParams dtIndices + liftTermTranslationMonad $ + TermTranslation.translateParams dtParams $ \ps -> + TermTranslation.translateParams dtIndices $ \ixs -> -- Translating the indices of a data type should never yield -- Inhabited constraints, so the result of calling -- `translateParams dtIndices` above should only return Binders and not -- any ImplicitBinders. Moreover, `translateParams` always returns -- Binders where the second field is `Just t`, where `t` is the type. - let errorBecause msg = error $ "translateDataType.translateNamed: " ++ msg + let errorBecause msg = error $ "translateDataType.translateNamed: " ++ msg in let bs = map (\case Coq.Binder s (Just t) -> Coq.PiBinder (Just s) t Coq.Binder _ Nothing -> errorBecause "encountered a Binder without a Type" Coq.ImplicitBinder{} -> errorBecause "encountered an implicit binder") - ixs + ixs in return (ps, bs) let inductiveSort = TermTranslation.translateSort dtSort inductiveConstructors <- mapM (translateCtor inductiveParameters) dtCtors diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs index 07af2861b8..1afaf91218 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs +++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs @@ -35,7 +35,8 @@ import qualified Control.Monad.Fail as Fail import Control.Monad.Reader hiding (fail, fix) import Control.Monad.State hiding (fail, fix, state) import Data.Char (isDigit) -import qualified Data.IntMap as IntMap +import Data.IntMap.Strict (IntMap) +import qualified Data.IntMap.Strict as IntMap import Data.List (intersperse, sortOn) import Data.Maybe (fromMaybe) import qualified Data.Map as Map @@ -63,8 +64,34 @@ traceTerm :: String -> Term -> a -> a traceTerm ctx t a = trace (ctx ++ ": " ++ showTerm t) a -} -newtype TranslationReader = TranslationReader +-- | A Coq identifier used for sharing subterms through let-bindings, annotated +-- with a 'Bool' flag indicating whether the shared subterm is closed, i.e., has +-- no free variables +data SharedName = SharedName { sharedNameIdent :: Coq.Ident, + sharedNameIsClosed :: Bool } + deriving Show + +-- | The read-only state for translating terms +data TranslationReader = TranslationReader { _currentModule :: Maybe ModuleName + -- ^ The current Coq module for the translation + + , _localEnvironment :: [Coq.Ident] + -- ^ The list of Coq identifiers associated with the current SAW core + -- Bruijn-indexed local variables in scope, innermost (index 0) first + + , _unavailableIdents :: Set.Set Coq.Ident + -- ^ The set of Coq identifiers that are either reserved or already in use. + -- To avoid shadowing, fresh identifiers should be chosen to be disjoint + -- from this set. + + , _sharedNames :: IntMap SharedName + -- ^ Index of identifiers for repeated subterms that have been lifted out + -- into a let expression + + , _nextSharedName :: Coq.Ident + -- ^ The next available name to be used for a let-bound shared + -- sub-expression } deriving (Show) @@ -73,44 +100,115 @@ makeLenses ''TranslationReader data TranslationState = TranslationState { _globalDeclarations :: [String] - -- ^ Some Cryptol terms seem to capture the name and body of some functions - -- they use (whether from the Cryptol prelude, or previously defined in the - -- same file). We want to translate those exactly once, so we need to keep - -- track of which ones have already been translated. + -- ^ Some Cryptol terms seem to capture the name and body of some functions + -- they use (whether from the Cryptol prelude, or previously defined in the + -- same file). We want to translate those exactly once, so we need to keep + -- track of which ones have already been translated. , _topLevelDeclarations :: [Coq.Decl] - -- ^ Because some terms capture their dependencies, translating one term may - -- result in multiple declarations: one for the term itself, but also zero or - -- many for its dependencies. We store all of those in this, so that a caller - -- of the translation may retrieve all the declarations needed to translate - -- the term. The translation function itself will return only the declaration - -- for the term being translated. - - , _localEnvironment :: [Coq.Ident] - -- ^ The list of Coq identifiers for de Bruijn-indexed local - -- variables, innermost (index 0) first. - - , _unavailableIdents :: Set.Set Coq.Ident - -- ^ The set of Coq identifiers that are either reserved or already - -- in use. To avoid shadowing, fresh identifiers should be chosen to - -- be disjoint from this set. - - , _sharedNames :: IntMap.IntMap Coq.Ident - -- ^ Index of identifiers for repeated subterms that have been - -- lifted out into a let expression. - - , _nextSharedName :: Coq.Ident - -- ^ The next available name to be used for a let-bound shared - -- sub-expression. + -- ^ Because some terms capture their dependencies, translating one term may + -- result in multiple declarations: one for the term itself, but also zero + -- or many for its dependencies. We store all of those in this, so that a + -- caller of the translation may retrieve all the declarations needed to + -- translate the term. The translation function itself will return only the + -- declaration for the term being translated. } deriving (Show) makeLenses ''TranslationState +-- | The constraint stating that 'm' can be used for term translation. This +-- requires that it have reader effects for 'TranslationReader' and state +-- effects for 'TranslationState'. type TermTranslationMonad m = TranslationMonad TranslationReader TranslationState m +-- | Get just the 'TranslationReader' component of the reader value +askTR :: TermTranslationMonad m => m TranslationReader +askTR = otherConfiguration <$> ask + +-- | Modify just the 'TranslationReader' component of the reader value +localTR :: TermTranslationMonad m => + (TranslationReader -> TranslationReader) -> m a -> m a +localTR f = + local (\r -> r { otherConfiguration = f (otherConfiguration r) }) + +-- | Take a Coq identifier that ends in a number (i.e., a sequence of digits) +-- and add 1 to that number, viewing an identifier with no trailing number as +-- ending in 0 +nextVariant :: Coq.Ident -> Coq.Ident +nextVariant = reverse . go . reverse + where + go :: String -> String + go (c : cs) + | c == '9' = '0' : go cs + | isDigit c = succ c : cs + go cs = '1' : cs + +-- | Find an fresh, as-yet-unused variant of the given Coq identifier +freshVariant :: TermTranslationMonad m => Coq.Ident -> m Coq.Ident +freshVariant x = + do used <- view unavailableIdents <$> askTR + let ident0 = x + let findVariant i = if Set.member i used then findVariant (nextVariant i) else i + return $ findVariant ident0 + +-- | Locally mark a Coq identifier as being used in the translation during a +-- translation computation, so that computation does not shadow it +withUsedCoqIdent :: TermTranslationMonad m => Coq.Ident -> m a -> m a +withUsedCoqIdent ident m = + localTR (over unavailableIdents (Set.insert ident)) m + +-- | Translate a local name from a saw-core binder into a fresh Coq identifier +translateLocalIdent :: TermTranslationMonad m => LocalName -> m Coq.Ident +translateLocalIdent x = freshVariant (escapeIdent (Text.unpack x)) + +-- | Generate a fresh, unused Coq identifier from a SAW core name and mark it as +-- unavailable in the supplied translation computation +withFreshIdent :: TermTranslationMonad m => LocalName -> (Coq.Ident -> m a) -> + m a +withFreshIdent n f = + do n_coq <- translateLocalIdent n + withUsedCoqIdent n_coq $ f n_coq + +-- | Invalidate all shared subterms that are not closed in a translation +invalidateOpenSharing :: TermTranslationMonad m => m a -> m a +invalidateOpenSharing = + localTR (over sharedNames $ IntMap.filter sharedNameIsClosed) + +-- | Run a translation in a context with one more SAW core variable with the +-- given name. Pass the corresponding Coq identifier used for this SAW core +-- variable to the computation in which it is bound. This invalidates all shared +-- terms that are not closed, since these shared terms now correspond to +-- different terms (with greater deBruijn indices) that have different +-- 'TermIndex'es. +withSAWVar :: TermTranslationMonad m => LocalName -> (Coq.Ident -> m a) -> m a +withSAWVar n m = + invalidateOpenSharing $ withFreshIdent n $ \n_coq -> + localTR (over localEnvironment (n_coq :)) $ m n_coq + +-- | Find a fresh name generated from 'nextSharedName' to use in place of the +-- supplied 'Term' with the supplied index, and associate that index with the +-- fresh name in the 'sharedNames' sharing map. Pass the name that was generated +-- to the computation. +withSharedTerm :: TermTranslationMonad m => TermIndex -> Term -> + (Coq.Ident -> m a) -> m a +withSharedTerm idx t f = + do ident <- (view nextSharedName <$> askTR) >>= freshVariant + let sh_nm = SharedName ident $ termIsClosed t + localTR (set nextSharedName (nextVariant ident) . + over sharedNames (IntMap.insert idx sh_nm)) $ + withUsedCoqIdent ident $ f ident + +-- | Use 'withSharedTerm' to mark a list of terms as being shared +withSharedTerms :: TermTranslationMonad m => [(TermIndex,Term)] -> + ([Coq.Ident] -> m a) -> m a +withSharedTerms [] f = f [] +withSharedTerms ((idx,t):ts) f = + withSharedTerm idx t $ \n -> withSharedTerms ts $ \ns -> f (n:ns) + + -- | The set of reserved identifiers in Coq, obtained from section -- "Gallina Specification Language" of the Coq reference manual. -- @@ -149,23 +247,27 @@ getNamesOfAllDeclarations = view allDeclarations <$> get allDeclarations = to (\ (TranslationState {..}) -> namedDecls _topLevelDeclarations ++ _globalDeclarations) +-- | Run a term translation computation runTermTranslationMonad :: TranslationConfiguration -> - TranslationReader -> + Maybe ModuleName -> [String] -> [Coq.Ident] -> (forall m. TermTranslationMonad m => m a) -> Either (TranslationError Term) (a, TranslationState) -runTermTranslationMonad configuration r globalDecls localEnv = - runTranslationMonad configuration r +runTermTranslationMonad configuration mname globalDecls localEnv = + runTranslationMonad configuration + (TranslationReader { + _currentModule = mname + , _localEnvironment = localEnv + , _unavailableIdents = Set.union reservedIdents (Set.fromList localEnv) + , _sharedNames = IntMap.empty + , _nextSharedName = "var__0" }) (TranslationState { _globalDeclarations = globalDecls , _topLevelDeclarations = [] - , _localEnvironment = localEnv - , _unavailableIdents = Set.union reservedIdents (Set.fromList localEnv) - , _sharedNames = IntMap.empty - , _nextSharedName = "var__0" }) +-- | Return a Coq term for an error computation with the given string message errorTermM :: TermTranslationMonad m => String -> m Coq.Term errorTermM str = return $ Coq.App (Coq.Var "error") [Coq.StringLit str] @@ -294,13 +396,10 @@ flatTermFToExpr tf = -- traceFTermF "flatTermFToExpr" tf $ -- (ix1 : _) -> ... -> (ixn : _) -> d ps ixs -> sort -- to get the type of the recursor, we compute -- (ix1 : _) -> ... -> (ixn : _) -> (x:d ps ixs) -> motive ixs x - do let (bs, _srt) = asPiList motiveTy - (varsT,bindersT) <- unzip <$> - (forM bs $ \ (b, bType) -> do - bTypeT <- translateTerm bType - b' <- freshenAndBindName b - return (Coq.Var b', Coq.PiBinder (Just b') bTypeT)) - + let (bs, _srt) = asPiList motiveTy in + translateBinders bs $ \bndrs -> + do let varsT = map (Coq.Var . bindTransIdent) bndrs + let bindersT = concat $ map bindTransToPiBinder bndrs motiveT <- translateTerm motive let bodyT = Coq.App motiveT varsT return $ Coq.Pi bindersT bodyT @@ -388,45 +487,17 @@ asApplyAllRecognizer :: Recognizer Term (Term, [Term]) asApplyAllRecognizer t = do _ <- asApp t return $ asApplyAll t --- | Run a translation, but keep some changes to the translation state local to --- that computation, restoring parts of the original translation state before --- returning. -withLocalTranslationState :: TermTranslationMonad m => m a -> m a -withLocalTranslationState action = do - before <- get - result <- action - after <- get - put (TranslationState - -- globalDeclarations is **not** restored, because we want to translate each - -- global declaration exactly once! - { _globalDeclarations = view globalDeclarations after - -- topLevelDeclarations is **not** restored, because it accumulates the - -- declarations witnessed in a given module so that we can extract it. - , _topLevelDeclarations = view topLevelDeclarations after - -- localEnvironment **is** restored, because the identifiers added to it - -- during translation are local to the term that was being translated. - , _localEnvironment = view localEnvironment before - -- unavailableIdents **is** restored, because the extra identifiers - -- unavailable in the term that was translated are local to it. - , _unavailableIdents = view unavailableIdents before - -- sharedNames **is** restored, because we are leaving the scope of the - -- locally shared names. - , _sharedNames = view sharedNames before - -- nextSharedName **is** restored, because we are leaving the scope of the - -- last names used. - , _nextSharedName = view nextSharedName before - }) - return result - --- | Run a translation in the top-level translation state +-- | Run a translation in the top-level translation state with no free SAW +-- variables and no bound Coq identifiers withTopTranslationState :: TermTranslationMonad m => m a -> m a withTopTranslationState m = - withLocalTranslationState $ - do modify $ set localEnvironment [] - modify $ set unavailableIdents reservedIdents - modify $ set sharedNames IntMap.empty - modify $ set nextSharedName "var__0" - m + localTR (\r -> + TranslationReader { + _currentModule = view currentModule r, + _localEnvironment = [], + _unavailableIdents = reservedIdents, + _sharedNames = IntMap.empty, + _nextSharedName = "var__0" }) m -- | Generate a Coq @Definition@ with a given name, body, and type, using the -- lambda-bound variable names for the variables if they are available @@ -443,85 +514,66 @@ mkDefinition name (Coq.Lambda bs t) (Coq.Pi bs' tp) Coq.Definition name bs (Just tp) t mkDefinition name t tp = Coq.Definition name [] (Just tp) t --- | Make sure a name is not used in the current environment, adding --- or incrementing a numeric suffix until we find an unused name. When --- we get one, add it to the current environment and return it. -freshenAndBindName :: TermTranslationMonad m => LocalName -> m Coq.Ident -freshenAndBindName n = - do n' <- translateLocalIdent n - modify $ over localEnvironment (n' :) - pure n' - mkLet :: (Coq.Ident, Coq.Term) -> Coq.Term -> Coq.Term mkLet (name, rhs) body = Coq.Let name [] Nothing rhs body --- | Given a list of 'LocalName's and their corresponding types (as 'Term's), --- return a list of explicit 'Binder's, for use representing the bound --- variables in 'Lambda's, 'Let's, etc. -translateParams :: - TermTranslationMonad m => - [(LocalName, Term)] -> m [Coq.Binder] -translateParams bs = concat <$> mapM translateParam bs - --- | Given a 'LocalName' and its type (as a 'Term'), return an explicit --- 'Binder', for use representing a bound variable in a 'Lambda', --- 'Let', etc. -translateParam :: - TermTranslationMonad m => - (LocalName, Term) -> m [Coq.Binder] -translateParam (n, ty) = - translateBinder n ty >>= \(n',ty',nhs) -> - return $ Coq.Binder n' (Just ty') : - map (\(nh,nhty) -> Coq.ImplicitBinder nh (Just nhty)) nhs - --- | Given a list of 'LocalName's and their corresponding types (as 'Term's) --- representing argument types and a 'Term' representing the return type, --- return the resulting 'Pi', with additional implicit arguments added after --- each instance of @isort@, @qsort@, etc. -translatePi :: TermTranslationMonad m => [(LocalName, Term)] -> Term -> m Coq.Term -translatePi binders body = withLocalTranslationState $ do - bindersT <- concat <$> mapM translatePiBinder binders - bodyT <- translateTermLet body - return $ Coq.Pi bindersT bodyT - --- | Given a 'LocalName' and its type (as a 'Term'), return an explicit --- 'PiBinder' followed by zero or more implicit 'PiBinder's representing --- additonal implicit typeclass arguments, added if the given type is @isort@, --- @qsort@, etc. -translatePiBinder :: - TermTranslationMonad m => (LocalName, Term) -> m [Coq.PiBinder] -translatePiBinder (n, ty) = - translateBinder n ty >>= \case - (n',ty',[]) - | n == "_" -> return [Coq.PiBinder Nothing ty'] - | otherwise -> return [Coq.PiBinder (Just n') ty'] - (n',ty',nhs) -> - return $ Coq.PiBinder (Just n') ty' : - map (\(nh,nhty) -> Coq.PiImplicitBinder (Just nh) nhty) nhs - --- | Given a 'LocalName' and its type (as a 'Term'), return the translation of --- the 'LocalName' as an 'Ident', the translation of the type as a 'Type', --- and zero or more additional 'Ident's and 'Type's representing additonal --- implicit typeclass arguments, added if the given type is @isort@, etc. -translateBinder :: - TermTranslationMonad m => - LocalName -> - Term -> - m (Coq.Ident,Coq.Type,[(Coq.Ident,Coq.Type)]) -translateBinder n ty@(asPiList -> (args, asSortWithFlags -> mb_sort)) = +-- | The result of translating a SAW core variable binding to Coq, including the +-- Coq identifier for the variable, the Coq translation of its type, and 0 or +-- more implicit Coq arguments that apply to the variable +data BindTrans = BindTrans { bindTransIdent :: Coq.Ident, + bindTransType :: Coq.Type, + bindTransImps :: [(Coq.Ident,Coq.Type)] } + +-- | Convert a 'BindTrans' to a list of Coq term-level binders +bindTransToBinder :: BindTrans -> [Coq.Binder] +bindTransToBinder (BindTrans {..}) = + Coq.Binder bindTransIdent (Just bindTransType) : + map (\(n,ty) -> Coq.ImplicitBinder n (Just ty)) bindTransImps + +-- | Convert a 'BindTrans' to a list of Coq type-level pi-abstraction binders +bindTransToPiBinder :: BindTrans -> [Coq.PiBinder] +bindTransToPiBinder (BindTrans { .. }) = + case bindTransImps of + [] | bindTransIdent == "_" -> [Coq.PiBinder Nothing bindTransType] + [] -> [Coq.PiBinder (Just bindTransIdent) bindTransType] + _ -> + Coq.PiBinder (Just bindTransIdent) bindTransType : + map (\(n,ty) -> Coq.PiImplicitBinder (Just n) ty) bindTransImps + +-- | Given a 'LocalName' and its type (as a 'Term'), translate the 'LocalName' +-- to a Coq identifier, translate the type to a Coq term, and generate zero or +-- more additional 'Ident's and 'Type's representing additonal implicit +-- typeclass arguments, added if the given type is @isort@, etc. Pass all of +-- this information to the supplied computation, in which the SAW core variable +-- is bound to its Coq identifier. +translateBinder :: TermTranslationMonad m => LocalName -> Term -> + (BindTrans -> m a) -> m a +translateBinder n ty@(asPiList -> (args, pi_body)) f = do ty' <- translateTerm ty - n' <- freshenAndBindName n - let flagValues = sortFlagsToList $ maybe noFlags snd mb_sort + let mb_sort = asSortWithFlags pi_body + flagValues = sortFlagsToList $ maybe noFlags snd mb_sort flagLocalNames = [("Inh", "SAWCoreScaffolding.Inhabited"), ("QT", "QuantType")] - nhs <- forM (zip flagValues flagLocalNames) $ \(fi,(prefix,tc)) -> - if not fi then return [] - else do nhty <- translateImplicitHyp (Coq.Var tc) args (Coq.Var n') - nh <- translateLocalIdent (prefix <> "_" <> n) - return [(nh,nhty)] - return (n',ty',concat nhs) - --- | Given a typeclass (as a 'Term'), a list of 'LocalName's and their + withSAWVar n $ \n' -> + helper n' (zip flagValues flagLocalNames) (\imps -> + f $ BindTrans n' ty' imps) + where + helper _ [] g = g [] + helper n' ((True,(prefix,tc)):rest) g = + do nhty <- translateImplicitHyp (Coq.Var tc) args (Coq.Var n') + withFreshIdent (prefix <> "_" <> n) $ \nh -> + helper n' rest (g . ((nh,nhty) :)) + helper n' ((False,_):rest) g = helper n' rest g + +-- | Call 'translateBinder' on a list of SAW core bindings +translateBinders :: TermTranslationMonad m => [(LocalName,Term)] -> + ([BindTrans] -> m a) -> m a +translateBinders [] f = f [] +translateBinders ((n,ty):ns_tys) f = + translateBinder n ty $ \bnd -> + translateBinders ns_tys $ \bnds -> f (bnd : bnds) + +-- | Given a typeclass (as a Coq term), a list of 'LocalName's and their -- corresponding types (as 'Term's), and a type-level function with argument -- types given by the prior list, return a 'Pi' of the given arguments, inside -- of which is an 'App' of the typeclass to the fully-applied type-level @@ -530,92 +582,94 @@ translateImplicitHyp :: TermTranslationMonad m => Coq.Term -> [(LocalName, Term)] -> Coq.Term -> m Coq.Term translateImplicitHyp tc [] tm = return (Coq.App tc [tm]) -translateImplicitHyp tc args tm = withLocalTranslationState $ - do args' <- mapM (uncurry translateBinder) args - return $ Coq.Pi (concatMap mkPi args') - (Coq.App tc [Coq.App tm (map mkArg args')]) - where - mkPi (nm,ty,nhs) = - Coq.PiBinder (Just nm) ty : - map (\(nh,nhty) -> Coq.PiImplicitBinder (Just nh) nhty) nhs - mkArg (nm,_,_) = Coq.Var nm - --- | Translate a local name from a saw-core binder into a fresh Coq identifier. -translateLocalIdent :: TermTranslationMonad m => LocalName -> m Coq.Ident -translateLocalIdent x = freshVariant (escapeIdent (Text.unpack x)) +translateImplicitHyp tc args tm = + translateBinders args $ \args' -> + return $ Coq.Pi (concatMap mkPi args') (Coq.App tc [Coq.App tm (map mkArg args')]) + where + mkPi (BindTrans nm ty nhs) = + Coq.PiBinder (Just nm) ty : + map (\(nh,nhty) -> Coq.PiImplicitBinder (Just nh) nhty) nhs + mkArg b = Coq.Var $ bindTransIdent b --- | Find an fresh, as-yet-unused variant of the given Coq identifier. -freshVariant :: TermTranslationMonad m => Coq.Ident -> m Coq.Ident -freshVariant x = - do used <- view unavailableIdents <$> get - let ident0 = x - let findVariant i = if Set.member i used then findVariant (nextVariant i) else i - let ident = findVariant ident0 - modify $ over unavailableIdents (Set.insert ident) - return ident +-- | Given a list of 'LocalName's and their corresponding types (as 'Term's), +-- return a list of explicit 'Binder's, for use representing the bound variables +-- in 'Lambda's, 'Let's, etc. +translateParams :: TermTranslationMonad m => [(LocalName, Term)] -> + ([Coq.Binder] -> m a) -> m a +translateParams bs m = + translateBinders bs (m . concat . map bindTransToBinder) -nextVariant :: Coq.Ident -> Coq.Ident -nextVariant = reverse . go . reverse - where - go :: String -> String - go (c : cs) - | c == '9' = '0' : go cs - | isDigit c = succ c : cs - go cs = '1' : cs +-- | Given a list of 'LocalName's and their corresponding types (as 'Term's) +-- representing argument types and a 'Term' representing the return type, +-- return the resulting 'Pi', with additional implicit arguments added after +-- each instance of @isort@, @qsort@, etc. +translatePi :: TermTranslationMonad m => [(LocalName, Term)] -> Term -> m Coq.Term +translatePi binders body = + translatePiBinders binders $ \bindersT -> + do bodyT <- translateTermLet body + return $ Coq.Pi bindersT bodyT +-- | Given a 'LocalName' and its type (as a 'Term'), return an explicit +-- 'PiBinder' followed by zero or more implicit 'PiBinder's representing +-- additonal implicit typeclass arguments, added if the given type is @isort@, +-- @qsort@, etc. +translatePiBinders :: TermTranslationMonad m => [(LocalName, Term)] -> + ([Coq.PiBinder] -> m a) -> m a +translatePiBinders bs m = + translateBinders bs (m . concat . map bindTransToPiBinder) + +-- | Find all subterms of a SAW core term that should be shared, and generate +-- let-bindings in Coq to bind them to local variables. Translate SAW core term +-- using those let-bindings for the shared subterms. translateTermLet :: TermTranslationMonad m => Term -> m Coq.Term translateTermLet t = - withLocalTranslationState $ - do let counts = scTermCount False t - let locals = fmap fst $ IntMap.filter keep counts - names <- traverse (const nextName) locals - modify $ set sharedNames names - defs <- traverse translateTermUnshared locals + let occ_map = scTermCount False t + shares = IntMap.assocs $ fmap fst $ IntMap.filter keep occ_map + share_tms = map snd shares in + -- NOTE: larger terms always have later stAppIndices than their subterms, so + -- IntMap.assocs above is guaranteed to return subterms before superterms; + -- this ensures that the right-hand sides in our nested let-bindings below + -- only refer to variables bound earlier, not later + withSharedTerms shares $ \names -> + do defs <- traverse translateTermUnshared share_tms body <- translateTerm t - -- NOTE: Larger terms always have later IDs than their subterms, - -- so ordering by VarIndex is a valid dependency order. - let binds = IntMap.elems (IntMap.intersectionWith (,) names defs) - pure (foldr mkLet body binds) + pure (foldr mkLet body $ zip names defs) where keep (t', n) = n > 1 && shouldMemoizeTerm t' - nextName = - do x <- view nextSharedName <$> get - x' <- freshVariant x - modify $ set nextSharedName (nextVariant x') - pure x' +-- | Translate a SAW core 'Term' to Coq, using let-bound Coq names when they are +-- associated with the given term for sharing translateTerm :: TermTranslationMonad m => Term -> m Coq.Term translateTerm t = case t of Unshared {} -> translateTermUnshared t STApp { stAppIndex = i } -> - do shared <- view sharedNames <$> get + do shared <- view sharedNames <$> askTR case IntMap.lookup i shared of Nothing -> translateTermUnshared t - Just x -> pure (Coq.Var x) + Just sh -> pure (Coq.Var $ sharedNameIdent sh) +-- | Translate a SAW core 'Term' to Coq without using sharing translateTermUnshared :: TermTranslationMonad m => Term -> m Coq.Term -translateTermUnshared t = withLocalTranslationState $ do +translateTermUnshared t = do -- traceTerm "translateTerm" t $ -- NOTE: env is in innermost-first order - env <- view localEnvironment <$> get + env <- view localEnvironment <$> askTR -- let t' = trace ("translateTerm: " ++ "env = " ++ show env ++ ", t =" ++ showTerm t) t -- case t' of case unwrapTermF t of FTermF ftf -> flatTermFToExpr ftf - Pi {} -> translatePi params e - where - (params, e) = asPiList t + Pi {} -> + let (params, e) = asPiList t in + translatePi params e - Lambda {} -> do - paramTerms <- translateParams params - e' <- translateTermLet e - pure (Coq.Lambda paramTerms e') - where - -- params are in normal, outermost first, order - (params, e) = asLambdaList t + Lambda {} -> + let (params, e) = asLambdaList t in + translateParams params $ \paramTerms -> + do e' <- translateTermLet e + return (Coq.Lambda paramTerms e') App {} -> -- asApplyAll: innermost argument first @@ -701,7 +755,7 @@ defaultTermForType typ = do -- type, and pass the results to the supplied function translateTermToDocWith :: TranslationConfiguration -> - TranslationReader -> + Maybe ModuleName -> [String] -> -- ^ globals that have already been translated [String] -> -- ^ string names of local variables in scope (Coq.Term -> Coq.Term -> Doc ann) -> @@ -723,7 +777,7 @@ translateTermToDocWith configuration r globalDecls localEnv f t tp_trm = do -- definition with the supplied name translateDefDoc :: TranslationConfiguration -> - TranslationReader -> + Maybe ModuleName -> [String] -> Coq.Ident -> Term -> Term -> Either (TranslationError Term) (Doc ann) diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs index 4017917745..dc1119875d 100644 --- a/saw-core/src/Verifier/SAW/Rewriter.hs +++ b/saw-core/src/Verifier/SAW/Rewriter.hs @@ -245,8 +245,8 @@ scMatch sc pat term = -- saves the names associated with those bound variables. match :: Int -> [(LocalName, Term)] -> Term -> Term -> MatchState -> MaybeT IO MatchState - match _ _ (STApp i _ fv _) (STApp j _ _ _) s - | fv == emptyBitSet && i == j = return s + match _ _ t@(STApp i _ _ _) (STApp j _ _ _) s + | termIsClosed t && i == j = return s match depth env x y s@(MatchState m cs) = -- (lift $ putStrLn $ "matching (lhs): " ++ scPrettyTerm defaultPPOpts x) >> -- (lift $ putStrLn $ "matching (rhs): " ++ scPrettyTerm defaultPPOpts y) >> @@ -875,8 +875,7 @@ replaceTerm :: Ord a => Term {- ^ the term in which to perform the replacement -} -> IO (Set a, Term) replaceTerm sc ss (pat, repl) t = do - let fvs = looseVars pat - unless (fvs == emptyBitSet) $ fail $ unwords + unless (termIsClosed pat) $ fail $ unwords [ "replaceTerm: term to replace has free variables!", scPrettyTerm defaultPPOpts t ] let rule = ruleOfTerms pat repl let ss' = addRule rule ss diff --git a/saw-core/src/Verifier/SAW/SCTypeCheck.hs b/saw-core/src/Verifier/SAW/SCTypeCheck.hs index 9d94d5eef2..20700dac03 100644 --- a/saw-core/src/Verifier/SAW/SCTypeCheck.hs +++ b/saw-core/src/Verifier/SAW/SCTypeCheck.hs @@ -79,9 +79,9 @@ type TCState = Map TermIndex Term -- * Memoizes the most general type inferred for each expression; AND -- -- * Can throw 'TCError's -type TCM a = +type TCM = ReaderT (SharedContext, Maybe ModuleName, [(LocalName, Term)]) - (StateT TCState (ExceptT TCError IO)) a + (StateT TCState (ExceptT TCError IO)) -- | Run a type-checking computation in a given context, starting from the empty -- memoization table @@ -400,16 +400,22 @@ instance TypeInfer (TermF Term) where -- special-case handling itself typeInfer ftf typeInfer (Lambda x a rhs) = - do a_tptrm <- typeInferCompleteWHNF a + do a_whnf <- typeInferCompleteWHNF a -- NOTE: before adding a type to the context, we want to be sure it is in - -- WHNF, so we don't have to normalize each time we look up a var type - rhs_tptrm <- withVar x (typedVal a_tptrm) $ typeInferComplete rhs + -- WHNF, so we don't have to normalize each time we look up a var type, + -- but we want to leave the non-normalized value of a in the returned + -- term, so we create a_tptrm with the type of a_whnf but the value of a + rhs_tptrm <- withVar x (typedVal a_whnf) $ typeInferComplete rhs + let a_tptrm = TypedTerm a (typedType a_whnf) typeInfer (Lambda x a_tptrm rhs_tptrm) typeInfer (Pi x a rhs) = - do a_tptrm <- typeInferCompleteWHNF a + do a_whnf <- typeInferCompleteWHNF a -- NOTE: before adding a type to the context, we want to be sure it is in - -- WHNF, so we don't have to normalize each time we look up a var type - rhs_tptrm <- withVar x (typedVal a_tptrm) $ typeInferComplete rhs + -- WHNF, so we don't have to normalize each time we look up a var type, + -- but we want to leave the non-normalized value of a in the returned + -- term, so we create a_typed with the type of a_whnf but the value of a + rhs_tptrm <- withVar x (typedVal a_whnf) $ typeInferComplete rhs + let a_tptrm = TypedTerm a (typedType a_whnf) typeInfer (Pi x a_tptrm rhs_tptrm) typeInfer (Constant ec _) = -- NOTE: this special case is to prevent us from re-type-checking the diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs index 0e0eb1cc76..c573994c76 100644 --- a/saw-core/src/Verifier/SAW/SharedTerm.hs +++ b/saw-core/src/Verifier/SAW/SharedTerm.hs @@ -1186,8 +1186,8 @@ instantiateLocalVars sc f initialLevel t0 = go l t = case t of Unshared tf -> go' l tf - STApp{ stAppIndex = tidx, stAppFreeVars = fv, stAppTermF = tf} - | fv == emptyBitSet -> return t -- closed terms map to themselves + STApp{ stAppIndex = tidx, stAppFreeVars = _, stAppTermF = tf} + | termIsClosed t -> return t -- closed terms map to themselves | otherwise -> useCache ?cache (tidx, l) (go' l tf) go' :: (?cache :: Cache IO (TermIndex, DeBruijnIndex) Term) => @@ -1547,7 +1547,7 @@ scConstant :: SharedContext -> Term -- ^ The type -> IO Term scConstant sc name rhs ty = - do unless (looseVars rhs == emptyBitSet) $ + do unless (termIsClosed rhs) $ fail "scConstant: term contains loose variables" let ecs = getAllExts rhs rhs' <- scAbstractExts sc ecs rhs @@ -1568,7 +1568,7 @@ scConstant' :: SharedContext -> Term -- ^ The type -> IO Term scConstant' sc nmi rhs ty = - do unless (looseVars rhs == emptyBitSet) $ + do unless (termIsClosed rhs) $ fail "scConstant: term contains loose variables" let ecs = getAllExts rhs rhs' <- scAbstractExts sc ecs rhs diff --git a/saw-core/src/Verifier/SAW/Simulator.hs b/saw-core/src/Verifier/SAW/Simulator.hs index 4a7e9886b5..f53f7b717f 100644 --- a/saw-core/src/Verifier/SAW/Simulator.hs +++ b/saw-core/src/Verifier/SAW/Simulator.hs @@ -507,8 +507,8 @@ mkMemoLocal cfg memoClosed t env = go mempty t where go :: IntMap (Thunk l) -> Term -> EvalM l (IntMap (Thunk l)) go memo (Unshared tf) = goTermF memo tf - go memo (STApp{ stAppIndex = i, stAppFreeVars = fv, stAppTermF = tf }) - | fv == emptyBitSet = pure memo + go memo (t'@STApp{ stAppIndex = i, stAppFreeVars = _, stAppTermF = tf }) + | termIsClosed t' = pure memo | otherwise = case IMap.lookup i memo of Just _ -> pure memo @@ -551,11 +551,11 @@ evalLocalTermF cfg memoClosed memoLocal tf0 env = evalTermF cfg lam recEval tf0 where lam = evalOpen cfg memoClosed recEval (Unshared tf) = evalTermF cfg lam recEval tf env - recEval (STApp{ stAppIndex = i, stAppFreeVars = fv, stAppTermF = tf }) = + recEval (t@STApp{ stAppIndex = i, stAppFreeVars = _, stAppTermF = tf }) = case IMap.lookup i memo of Just x -> force x Nothing -> evalTermF cfg lam recEval tf env - where memo = if fv == emptyBitSet then memoClosed else memoLocal + where memo = if termIsClosed t then memoClosed else memoLocal {-# SPECIALIZE evalOpen :: Show (Extra l) => @@ -580,11 +580,11 @@ evalOpen cfg memoClosed t env = do memoLocal <- mkMemoLocal cfg memoClosed t env let eval :: Term -> MValue l eval (Unshared tf) = evalF tf - eval (STApp{ stAppIndex = i, stAppFreeVars = fv, stAppTermF = tf }) = + eval (t'@STApp{ stAppIndex = i, stAppFreeVars = _, stAppTermF = tf }) = case IMap.lookup i memo of Just x -> force x Nothing -> evalF tf - where memo = if fv == emptyBitSet then memoClosed else memoLocal + where memo = if termIsClosed t' then memoClosed else memoLocal evalF :: TermF Term -> MValue l evalF tf = evalTermF cfg (evalOpen cfg memoClosed) eval tf env eval t diff --git a/saw-core/src/Verifier/SAW/Term/Functor.hs b/saw-core/src/Verifier/SAW/Term/Functor.hs index 581e1682ef..1caeca2369 100644 --- a/saw-core/src/Verifier/SAW/Term/Functor.hs +++ b/saw-core/src/Verifier/SAW/Term/Functor.hs @@ -60,7 +60,7 @@ module Verifier.SAW.Term.Functor , BitSet, emptyBitSet, inBitSet, unionBitSets, intersectBitSets , decrBitSet, multiDecrBitSet, completeBitSet, singletonBitSet, bitSetElems , smallestBitSetElem - , looseVars, smallestFreeVar + , looseVars, smallestFreeVar, termIsClosed ) where import Data.Bits @@ -609,3 +609,7 @@ looseVars (Unshared f) = freesTermF (fmap looseVars f) -- | Compute the value of the smallest variable in the term, if any. smallestFreeVar :: Term -> Maybe Int smallestFreeVar = smallestBitSetElem . looseVars + +-- | Test whether a 'Term' is closed, i.e., has no free variables +termIsClosed :: Term -> Bool +termIsClosed t = looseVars t == emptyBitSet diff --git a/saw-core/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs index 6f82c44cea..a06d930828 100644 --- a/saw-core/src/Verifier/SAW/Term/Pretty.hs +++ b/saw-core/src/Verifier/SAW/Term/Pretty.hs @@ -669,7 +669,7 @@ filterOccurenceMap min_occs global_p = IntMap.filter (\(t,cnt) -> cnt >= min_occs && shouldMemoizeTerm t && - (if global_p then looseVars t == emptyBitSet else True)) + (if global_p then termIsClosed t else True)) -- For each (TermIndex, Term) pair in the occurrence map, pretty-print the diff --git a/saw-core/src/Verifier/SAW/Typechecker.hs b/saw-core/src/Verifier/SAW/Typechecker.hs index a7c21ad96e..1ad0b42757 100644 --- a/saw-core/src/Verifier/SAW/Typechecker.hs +++ b/saw-core/src/Verifier/SAW/Typechecker.hs @@ -208,10 +208,13 @@ typeInferCompleteTerm (Un.App f arg) = >>= typeInferComplete typeInferCompleteTerm (Un.Lambda _ [] t) = typeInferComplete t typeInferCompleteTerm (Un.Lambda p ((Un.termVarLocalName -> x, tp) : ctx) t) = - do tp_trm <- typeInferCompleteWHNF tp - -- Normalize (the Term value of) tp before putting it into the context. See - -- the documentation for withVar. - body <- withVar x (typedVal tp_trm) $ + do tp_trm <- typeInferComplete tp + -- NOTE: we need the type of x to be normalized when we add it to the + -- context in withVar, but we do not want to normalize this type in the + -- output, as the contract for typeInferComplete only normalizes the type, + -- so we use the unnormalized tp_trm in the return + tp_whnf <- typeCheckWHNF $ typedVal tp_trm + body <- withVar x tp_whnf $ typeInferComplete $ Un.Lambda p ctx t typeInferComplete (Lambda x tp_trm body) typeInferCompleteTerm (Un.Pi _ [] t) = typeInferComplete t diff --git a/saw-core/src/Verifier/SAW/TypedAST.hs b/saw-core/src/Verifier/SAW/TypedAST.hs index 2ddfab2329..4f399e4131 100644 --- a/saw-core/src/Verifier/SAW/TypedAST.hs +++ b/saw-core/src/Verifier/SAW/TypedAST.hs @@ -83,7 +83,7 @@ module Verifier.SAW.TypedAST , VarIndex -- * Utility functions , BitSet, emptyBitSet, inBitSet, unionBitSets, intersectBitSets - , decrBitSet, completeBitSet + , decrBitSet, completeBitSet, termIsClosed ) where import Control.Exception (assert) diff --git a/saw-core/tests/src/Tests/Parser.hs b/saw-core/tests/src/Tests/Parser.hs index 29d9b5d439..1c1ee80356 100644 --- a/saw-core/tests/src/Tests/Parser.hs +++ b/saw-core/tests/src/Tests/Parser.hs @@ -16,9 +16,6 @@ import Verifier.SAW.SharedTerm import Verifier.SAW.Term.Functor -checkGroundTerm :: Term -> Bool -checkGroundTerm t = looseVars t == emptyBitSet - namedMsg :: Ident -> String -> String namedMsg sym msg = "In " ++ show sym ++ ": " ++ msg @@ -26,11 +23,11 @@ checkDef :: Def -> Assertion checkDef d = do let sym = defIdent d let tp = defType d - assertBool (namedMsg sym "Type is not ground.") (checkGroundTerm tp) + assertBool (namedMsg sym "Type is not ground.") (termIsClosed tp) case defBody d of Nothing -> return () Just body -> - assertBool (namedMsg sym "Body is not ground.") (checkGroundTerm body) + assertBool (namedMsg sym "Body is not ground.") (termIsClosed body) checkPrelude :: Assertion checkPrelude = diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 3ca9813a26..279c3acddd 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -292,13 +292,10 @@ replacePrim pat replace t = do let tpat = ttTerm pat let trepl = ttTerm replace - let fvpat = looseVars tpat - let fvrepl = looseVars trepl - - unless (fvpat == emptyBitSet) $ fail $ unlines + unless (termIsClosed tpat) $ fail $ unlines [ "pattern term is not closed", show tpat ] - unless (fvrepl == emptyBitSet) $ fail $ unlines + unless (termIsClosed trepl) $ fail $ unlines [ "replacement term is not closed", show trepl ] io $ do @@ -781,13 +778,13 @@ build_congruence sc tm = case asPiList ty of ([],_) -> fail "congruence_for: Term is not a function" (pis, body) -> - if looseVars body == emptyBitSet then + if termIsClosed body then loop pis [] else fail "congruence_for: cannot build congruence for dependent functions" where loop ((nm,tp):pis) vars = - if looseVars tp == emptyBitSet then + if termIsClosed tp then do l <- scFreshEC sc (nm <> "_1") tp r <- scFreshEC sc (nm <> "_2") tp loop pis ((l,r):vars) diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs index 10f0abe460..eb98ba95b2 100644 --- a/src/SAWScript/Proof.hs +++ b/src/SAWScript/Proof.hs @@ -292,7 +292,7 @@ splitImpl sc (Prop p) -- Handle the case of (H1 -> H2), where H1 and H2 are in Prop | Just (_nm, arg, c) <- asPi p - , looseVars c == emptyBitSet -- make sure this is a nondependent Pi (AKA arrow type) + , termIsClosed c -- make sure this is a nondependent Pi (AKA arrow type) = termToMaybeProp sc arg >>= \case Nothing -> return Nothing Just h -> return (Just (h, Prop c)) @@ -1459,7 +1459,7 @@ normalizeConcl sc p = case asPi t of Just (_nm, arg, body) -- check that this is non-dependent Pi (AKA arrow type) - | looseVars body == emptyBitSet -> + | termIsClosed body -> termToMaybeProp sc arg >>= \case Nothing -> return (RawSequent [] [p]) Just h -> @@ -1524,7 +1524,7 @@ checkEvidence sc = \e p -> do nenv <- scGetNamingEnv sc -- and the given evidence must match the expected prop. checkApply nenv mkSqt (Prop p) (Right e:es) | Just (_lnm, tp, body) <- asPi p - , looseVars body == emptyBitSet + , termIsClosed body = do (d1,sy1) <- check nenv e . mkSqt =<< termToProp sc tp (d2,sy2,p') <- checkApply nenv mkSqt (Prop body) es return (Set.union d1 d2, sy1 <> sy2, p') @@ -1959,7 +1959,7 @@ sequentToSATQuery sc unintSet sqt = body' <- instantiateVar sc 0 etm body processUnivAssert mmap ((ec,fot):vars) xs body' Nothing - | looseVars body == emptyBitSet -> + | termIsClosed body -> case asEqTrue tp' of Just x -> processUnivAssert mmap vars (x:xs) body Nothing -> @@ -1992,7 +1992,7 @@ sequentToSATQuery sc unintSet sqt = body' <- instantiateVar sc 0 etm body processConcl mmap (Map.insert ec fot vars, xs) body' Nothing - | looseVars body == emptyBitSet -> + | termIsClosed body -> do asrt <- processAssert mmap tp processConcl mmap (vars, asrt : xs) body | otherwise ->