From 02f2be2eca3e6e04401a65179162771fce70aa2c Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Mon, 15 Feb 2021 19:19:39 -0800 Subject: [PATCH] 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. --- saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs | 5 ++++- saw-core/src/Verifier/SAW/ExternalFormat.hs | 6 ++++-- saw-core/src/Verifier/SAW/Recognizer.hs | 10 ++++++++-- saw-core/src/Verifier/SAW/Rewriter.hs | 2 +- saw-core/src/Verifier/SAW/SCTypeCheck.hs | 5 ++--- saw-core/src/Verifier/SAW/SharedTerm.hs | 2 +- saw-core/src/Verifier/SAW/Simulator.hs | 6 +++++- saw-core/src/Verifier/SAW/Term/Functor.hs | 8 +++++--- saw-core/src/Verifier/SAW/Term/Pretty.hs | 8 ++++---- saw-core/src/Verifier/SAW/Typechecker.hs | 7 ++++++- 10 files changed, 40 insertions(+), 19 deletions(-) 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 6acd5f1e46..4bbc3828d4 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs +++ b/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] diff --git a/saw-core/src/Verifier/SAW/ExternalFormat.hs b/saw-core/src/Verifier/SAW/ExternalFormat.hs index fc33de9368..8f989dcfc8 100644 --- a/saw-core/src/Verifier/SAW/ExternalFormat.hs +++ b/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) diff --git a/saw-core/src/Verifier/SAW/Recognizer.hs b/saw-core/src/Verifier/SAW/Recognizer.hs index 0023351884..28e9e9d6aa 100644 --- a/saw-core/src/Verifier/SAW/Recognizer.hs +++ b/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 () diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs index 61d76e9b04..05a4257e95 100644 --- a/saw-core/src/Verifier/SAW/Rewriter.hs +++ b/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) => diff --git a/saw-core/src/Verifier/SAW/SCTypeCheck.hs b/saw-core/src/Verifier/SAW/SCTypeCheck.hs index 772c83acb3..422511b607 100644 --- a/saw-core/src/Verifier/SAW/SCTypeCheck.hs +++ b/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)) = diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs index 9fc9c5fd07..f5dbe0f8fc 100644 --- a/saw-core/src/Verifier/SAW/SharedTerm.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/Simulator.hs b/saw-core/src/Verifier/SAW/Simulator.hs index e300b8a02e..cf670e72b9 100644 --- a/saw-core/src/Verifier/SAW/Simulator.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/Term/Functor.hs b/saw-core/src/Verifier/SAW/Term/Functor.hs index 930cb12eb5..ec18bac5b2 100644 --- a/saw-core/src/Verifier/SAW/Term/Functor.hs +++ b/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) -> diff --git a/saw-core/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs index e36e62b276..aa146b865b 100644 --- a/saw-core/src/Verifier/SAW/Term/Pretty.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/Typechecker.hs b/saw-core/src/Verifier/SAW/Typechecker.hs index 6beb06f728..0cce4600c1 100644 --- a/saw-core/src/Verifier/SAW/Typechecker.hs +++ b/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,