Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix Coq translator for globals that are not applied #1749

Merged
merged 2 commits into from
Oct 6, 2022
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 6 additions & 5 deletions saw-core-coq/src/Verifier/SAW/Translation/Coq/Monad.hs
Original file line number Diff line number Diff line change
@@ -55,10 +55,12 @@ showError printer err = case err of
CannotCreateDefaultValue a -> "Unable to generate a default value of the given type: " ++ printer a

data TranslationConfiguration = TranslationConfiguration
{ notations :: [(String, String)]
-- ^ We currently don't have a nice way of mapping Cryptol notations to Coq
-- notations. Instead, we provide a mapping from the notation symbol to an
-- identifier to use instead.
{ constantRenaming :: [(String, String)]
-- ^ A map from 'ImportedName's of constants to names that should be used to
-- realize them in Coq; this is generally used to map cryptol operators like
-- @||@ or @&&@ to nicer names in Coq, but works on any imported names
, constantSkips :: [String]
-- ^ A list of 'ImportedName's to skip, i.e., not translate when encountered
, monadicTranslation :: Bool
-- ^ Whether to wrap everything in a free monad construction.
-- - Advantage: fixpoints can be readily represented
@@ -67,7 +69,6 @@ data TranslationConfiguration = TranslationConfiguration
-- ^ Text to be concatenated at the end of the Coq preamble, before the code
-- generated by the translation. Usually consists of extra file imports,
-- module imports, scopes openings.
, skipDefinitions :: [String]
, vectorModule :: String
-- ^ all vector operations will be prepended with this module name, i.e.
-- "<VectorModule>.append", etc. So that it can be retargeted easily.
13 changes: 0 additions & 13 deletions saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
Original file line number Diff line number Diff line change
@@ -499,26 +499,13 @@ sawCorePreludeSpecialTreatmentMap configuration =
, ("List__rec", replace (Coq.ExplVar "Datatypes.list_rect"))
]

constantsRenamingMap :: [(String, String)] -> Map.Map String String
constantsRenamingMap notations = Map.fromList notations

escapeIdent :: String -> String
escapeIdent str
| all okChar str = str
| otherwise = "Op_" ++ zEncodeString str
where
okChar x = isAlphaNum x || x `elem` ("_'" :: String)

-- TODO: Now that ExtCns contains a unique identifier, it might make sense
-- to check those here to avoid some captures?
translateConstant :: [(String, String)] -> ExtCns e -> String
translateConstant notations (EC {..}) =
escapeIdent $
Map.findWithDefault
(Text.unpack (toShortName ecName))
(Text.unpack (toShortName ecName))
(constantsRenamingMap notations) -- TODO short name doesn't seem right

zipSnippet :: String
zipSnippet = [i|
Fixpoint zip (a b : sort 0) (m n : Nat) (xs : Vec m a) (ys : Vec n b)
115 changes: 58 additions & 57 deletions saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs
Original file line number Diff line number Diff line change
@@ -168,6 +168,8 @@ runTermTranslationMonad configuration r globalDecls localEnv =
errorTermM :: TermTranslationMonad m => String -> m Coq.Term
errorTermM str = return $ Coq.App (Coq.Var "error") [Coq.StringLit str]

-- | Translate an 'Ident' with a given list of arguments to a Coq term, using
-- any special treatment for that identifier and qualifying it if necessary
translateIdentWithArgs :: TermTranslationMonad m => Ident -> [Term] -> m Coq.Term
translateIdentWithArgs i args = do
currentModuleName <- asks (view currentModule . otherConfiguration)
@@ -202,9 +204,52 @@ translateIdentWithArgs i args = do
]
)

-- | Helper for 'translateIdentWithArgs' with no arguments
translateIdent :: TermTranslationMonad m => Ident -> m Coq.Term
translateIdent i = translateIdentWithArgs i []

-- | Translate a constant with optional body to a Coq term. If the constant is
-- named with an 'Ident', then it already has a top-level translation from
-- translating the SAW core module containing that 'Ident'. If the constant is
-- an 'ImportedName', however, then it might not have a Coq definition already,
-- so add a definition of it to the top-level translation state.
translateConstant :: TermTranslationMonad m => ExtCns Term -> Maybe Term ->
m Coq.Term
translateConstant ec _
| ModuleIdentifier ident <- ecName ec = translateIdent ident
translateConstant ec maybe_body =
do -- First, apply the constant renaming to get the name for this constant
configuration <- asks translationConfiguration
-- TODO short name seems wrong
let nm_str = Text.unpack $ toShortName $ ecName ec
let renamed =
escapeIdent $ fromMaybe nm_str $
lookup nm_str $ constantRenaming configuration

-- Next, test if we should add a definition of this constant
alreadyTranslatedDecls <- getNamesOfAllDeclarations
let skip_def =
elem renamed alreadyTranslatedDecls ||
elem renamed (constantSkips configuration)

-- Add the definition if we aren't skipping it
case maybe_body of
_ | skip_def -> return ()
Just body ->
-- If the definition has a body, add it as a definition
do b <- withTopTranslationState $ translateTermLet body
modify $ over topLevelDeclarations $ (mkDefinition renamed b :)
Nothing ->
-- If not, add it as a Coq Variable declaration
do tp <- withTopTranslationState $ translateTermLet (ecType ec)
modify (over topLevelDeclarations (Coq.Variable renamed tp :))

-- Finally, return the constant as a Coq variable
pure (Coq.Var renamed)


-- | Translate an 'Ident' and see if the result maps to a SAW core 'Ident',
-- returning the latter 'Ident' if so
translateIdentToIdent :: TermTranslationMonad m => Ident -> m (Maybe Ident)
translateIdentToIdent i =
(atUseSite <$> findSpecialTreatment i) >>= \case
@@ -294,24 +339,7 @@ flatTermFToExpr tf = -- traceFTermF "flatTermFToExpr" tf $
return (Coq.App (Coq.Var "Vector.of_list") [Coq.List elems])
StringLit s -> pure (Coq.Scope (Coq.StringLit (Text.unpack s)) "string")

ExtCns ec ->
do configuration <- asks translationConfiguration
let renamed = translateConstant (notations configuration) ec
alreadyTranslatedDecls <- getNamesOfAllDeclarations
let definitionsToSkip = skipDefinitions configuration
if elem renamed alreadyTranslatedDecls || elem renamed definitionsToSkip
then Coq.Var <$> pure renamed
else do
tp <-
-- Translate type in a top-level name scope
withLocalTranslationState $
do modify $ set localEnvironment []
modify $ set unavailableIdents reservedIdents
modify $ set sharedNames IntMap.empty
modify $ set nextSharedName "var__0"
translateTermLet (ecType ec)
modify $ over topLevelDeclarations $ (Coq.Variable renamed tp :)
Coq.Var <$> pure renamed
ExtCns ec -> translateConstant ec Nothing

-- The translation of a record type {fld1:tp1, ..., fldn:tpn} is
-- RecordTypeCons fld1 tp1 (... (RecordTypeCons fldn tpn RecordTypeNil)...).
@@ -385,6 +413,16 @@ withLocalTranslationState action = do
})
return result

-- | Run a translation in the top-level translation state
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

mkDefinition :: Coq.Ident -> Coq.Term -> Coq.Decl
mkDefinition name (Coq.Lambda bs t) = Coq.Definition name bs Nothing t
mkDefinition name t = Coq.Definition name [] Nothing t
@@ -581,45 +619,8 @@ translateTermUnshared t = withLocalTranslationState $ do
| n < length env -> Coq.Var <$> pure (env !! n)
| otherwise -> Except.throwError $ LocalVarOutOfBounds t

-- Constants with no body
Constant n Nothing -> do
configuration <- asks translationConfiguration
let renamed = translateConstant (notations configuration) n
alreadyTranslatedDecls <- getNamesOfAllDeclarations
let definitionsToSkip = skipDefinitions configuration
if elem renamed alreadyTranslatedDecls || elem renamed definitionsToSkip
then Coq.Var <$> pure renamed
else do
tp <-
-- Translate type in a top-level name scope
withLocalTranslationState $
do modify $ set localEnvironment []
modify $ set unavailableIdents reservedIdents
modify $ set sharedNames IntMap.empty
modify $ set nextSharedName "var__0"
translateTermLet (ecType n)
modify $ over topLevelDeclarations $ (Coq.Variable renamed tp :)
Coq.Var <$> pure renamed

-- Constants with a body
Constant n (Just body) -> do
configuration <- asks translationConfiguration
let renamed = translateConstant (notations configuration) n
alreadyTranslatedDecls <- getNamesOfAllDeclarations
let definitionsToSkip = skipDefinitions configuration
if elem renamed alreadyTranslatedDecls || elem renamed definitionsToSkip
then Coq.Var <$> pure renamed
else do
b <-
-- Translate body in a top-level name scope
withLocalTranslationState $
do modify $ set localEnvironment []
modify $ set unavailableIdents reservedIdents
modify $ set sharedNames IntMap.empty
modify $ set nextSharedName "var__0"
translateTermLet body
modify $ over topLevelDeclarations $ (mkDefinition renamed b :)
Coq.Var <$> pure renamed
-- Constants
Constant n maybe_body -> translateConstant n maybe_body

where
badTerm = Except.throwError $ BadTerm t
6 changes: 3 additions & 3 deletions src/SAWScript/Prover/Exporter.hs
Original file line number Diff line number Diff line change
@@ -400,11 +400,11 @@ coqTranslationConfiguration ::
[(String, String)] ->
[String] ->
Coq.TranslationConfiguration
coqTranslationConfiguration notations skips = Coq.TranslationConfiguration
{ Coq.notations = notations
coqTranslationConfiguration renamings skips = Coq.TranslationConfiguration
{ Coq.constantRenaming = renamings
, Coq.constantSkips = skips
, Coq.monadicTranslation = False
, Coq.postPreamble = []
, Coq.skipDefinitions = skips
, Coq.vectorModule = "SAWCoreVectorsAsCoqVectors"
}