Introduce newtype for Coq.Ident type.

Fixes #1253.

saw-core-coq/src/Language/Coq/AST.hs

@@ -9,7 +9,16 @@ Portability : portable
 
 module Language.Coq.AST where
 
-type Ident = String
+import Data.String (IsString(..))
+
+newtype Ident = Ident String
+  deriving (Eq, Ord)
+
+instance Show Ident where
+  show (Ident s) = show s
+
+instance IsString Ident where
+  fromString s = Ident s
 
 data Sort
   = Prop

saw-core-coq/src/Language/Coq/Pretty.hs

@@ -53,7 +53,7 @@ period :: Doc ann
 period = text "."
 
 ppIdent :: Ident -> Doc ann
-ppIdent = text
+ppIdent (Ident s) = pretty s
 
 ppBinder :: Binder -> Doc ann
 ppBinder (Binder x Nothing)  = ppIdent x
@@ -97,7 +97,7 @@ ppTerm p e =
       (text "fun" <+> ppBinders bs <+> text "=>" <+> ppTerm PrecLambda t)
     Fix ident binders returnType body ->
       parensIf (p > PrecLambda) $
-      (text "fix" <+> text ident <+> ppBinders binders <+> text ":"
+      (text "fix" <+> ppIdent ident <+> ppBinders binders <+> text ":"
              <+> ppTerm PrecNone returnType <+> text ":=" <+> ppTerm PrecLambda body)
     Pi bs t ->
       parensIf (p > PrecLambda) $
@@ -145,13 +145,13 @@ ppDecl :: Decl -> Doc ann
 ppDecl decl = case decl of
   Axiom nm ty ->
     (nest 2 $
-     hsep ([text "Axiom", text nm, text ":", ppTerm PrecNone ty, period])) <> hardline
+     hsep ([text "Axiom", ppIdent nm, text ":", ppTerm PrecNone ty, period])) <> hardline
   Comment s ->
     text "(*" <+> text s <+> text "*)" <> hardline
   Definition nm bs mty body ->
     (nest 2 $
      vsep
-     [ hsep ([text "Definition", text nm] ++
+     [ hsep ([text "Definition", ppIdent nm] ++
             map ppBinder bs ++
             [ppMaybeTy mty, text ":="])
      , ppTerm PrecNone body <> period
@@ -163,7 +163,7 @@ ppConstructor :: Constructor -> Doc ann
 ppConstructor (Constructor {..}) =
   nest 2 $
   hsep ([ text "|"
-        , text constructorName
+        , ppIdent constructorName
         , text ":"
         , ppTerm PrecNone constructorType
         ]
@@ -174,7 +174,7 @@ ppInductive (Inductive {..}) =
   (vsep
    ([ nest 2 $
       hsep ([ text "Inductive"
-            , text inductiveName
+            , ppIdent inductiveName
             ]
             ++ map ppBinder inductiveParameters
             ++ [ text ":" ]

saw-core-coq/src/Verifier/SAW/Translation/Coq.hs

@@ -131,7 +131,7 @@ translateSAWModule configuration m =
      ]
 
 translateCryptolModule ::
-  TranslationConfiguration -> [String] -> CryptolModule -> Either (TranslationError Term) (Doc ann)
+  TranslationConfiguration -> [Coq.Ident] -> CryptolModule -> Either (TranslationError Term) (Doc ann)
 translateCryptolModule configuration globalDecls m =
   let decls = CryptolModuleTranslation.translateCryptolModule
               configuration

saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs

@@ -7,6 +7,7 @@ import           Control.Lens                       (over, set, view)
 import           Control.Monad                      (forM)
 import           Control.Monad.State                (modify)
 import qualified Data.Map                           as Map
+import           Data.String                        (IsString(..))
 
 import           Cryptol.ModuleSystem.Name
 import           Cryptol.Utils.Ident
@@ -22,7 +23,7 @@ translateTypedTermMap tm = forM (Map.assocs tm) translateAndRegisterEntry
   where
     translateAndRegisterEntry (name, symbol) = do
       let t = ttTerm symbol
-      let nameStr = unpackIdent (nameIdent name)
+      let nameStr = fromString (unpackIdent (nameIdent name))
       term <- TermTranslation.withLocalLocalEnvironment $ do
         modify $ set TermTranslation.localEnvironment [nameStr]
         TermTranslation.translateTerm t
@@ -31,7 +32,7 @@ translateTypedTermMap tm = forM (Map.assocs tm) translateAndRegisterEntry
       return decl
 
 translateCryptolModule ::
-  TranslationConfiguration -> [String] -> CryptolModule -> Either (TranslationError Term) [Coq.Decl]
+  TranslationConfiguration -> [Coq.Ident] -> CryptolModule -> Either (TranslationError Term) [Coq.Decl]
 translateCryptolModule configuration globalDecls (CryptolModule _ tm) =
   case TermTranslation.runTermTranslationMonad
        configuration

saw-core-coq/src/Verifier/SAW/Translation/Coq/Monad.hs

@@ -30,6 +30,9 @@ import Verifier.SAW.SharedTerm
 --import Verifier.SAW.Term.Pretty
 -- import qualified Verifier.SAW.UntypedAST as Un
 
+import qualified Language.Coq.AST as Coq
+
+
 data TranslationError a
   = NotSupported a
   | NotExpr a
@@ -54,7 +57,7 @@ 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)]
+  { notations          :: [(String, Coq.Ident)]
   -- ^ 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.
@@ -66,7 +69,7 @@ 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]
+  , skipDefinitions    :: [Coq.Ident]
   , vectorModule       :: String
   -- ^ all vector operations will be prepended with this module name, i.e.
   -- "<VectorModule>.append", etc.  So that it can be retargeted easily.

saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs

@@ -28,6 +28,7 @@ import           Control.Lens                                  (makeLenses, view
 import qualified Control.Monad.Except                          as Except
 import           Control.Monad.Reader                          hiding (fail)
 import           Control.Monad.State                           hiding (fail)
+import           Data.String                                   (IsString(..))
 import           Prelude                                       hiding (fail)
 import           Prettyprinter                                 (Doc)
 
@@ -70,7 +71,7 @@ translateCtor inductiveParameters (Ctor {..}) = do
   maybe_constructorName <-
     liftTermTranslationMonad $ TermTranslation.translateIdentToIdent ctorName
   let constructorName = case maybe_constructorName of
-        Just n -> identName n
+        Just n -> fromString (identName n)
         Nothing -> error "translateCtor: unexpected translation for constructor"
   constructorType <-
     -- Unfortunately, `ctorType` qualifies the inductive type's name in the
@@ -95,9 +96,9 @@ translateDataType (DataType {..}) =
   DefReplace  str          -> return $ Coq.Snippet str
   DefSkip                  -> return $ skipped dtName
   where
-    translateNamed :: ModuleTranslationMonad m => Coq.Ident -> m Coq.Decl
+    translateNamed :: ModuleTranslationMonad m => String -> m Coq.Decl
     translateNamed name = do
-      let inductiveName = name
+      let inductiveName = fromString name
       (inductiveParameters, inductiveIndices) <-
         liftTermTranslationMonad $ do
         ps <- TermTranslation.translateParams dtParams
@@ -134,8 +135,8 @@ translateDef (Def {..}) = {- trace ("translateDef " ++ show defIdent) $ -} do
   where
 
     translateAccordingly :: ModuleTranslationMonad m => DefSiteTreatment -> m Coq.Decl
-    translateAccordingly  DefPreserve             = translateNamed $ identName defIdent
-    translateAccordingly (DefRename _ targetName) = translateNamed $ targetName
+    translateAccordingly  DefPreserve             = translateNamed $ fromString $ identName defIdent
+    translateAccordingly (DefRename _ targetName) = translateNamed $ fromString $ targetName
     translateAccordingly (DefReplace  str)        = return $ Coq.Snippet str
     translateAccordingly  DefSkip                 = return $ skipped defIdent
 

saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs

@@ -27,6 +27,7 @@ module Verifier.SAW.Translation.Coq.SpecialTreatment where
 import           Control.Lens                       (_1, _2, over)
 import           Control.Monad.Reader               (ask)
 import qualified Data.Map                           as Map
+import           Data.String                        (IsString(..))
 import           Data.String.Interpolate            (i)
 import qualified Data.Text                          as Text
 import           Prelude                            hiding (fail)
@@ -452,16 +453,16 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("letRecFuns", skip)
   ]
 
-constantsRenamingMap :: [(String, String)] -> Map.Map String String
+constantsRenamingMap :: [(String, Coq.Ident)] -> Map.Map String Coq.Ident
 constantsRenamingMap notations = Map.fromList notations
 
 -- 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 :: [(String, Coq.Ident)] -> ExtCns e -> Coq.Ident
 translateConstant notations (EC {..}) =
   Map.findWithDefault
-    (Text.unpack (toShortName ecName))
-    (Text.unpack (toShortName ecName))
+    (fromString (Text.unpack (toShortName ecName)))
+    (fromString (Text.unpack (toShortName ecName)))
     (constantsRenamingMap notations) -- TODO short name doesn't seem right
 
 zipSnippet :: String

saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs

@@ -38,6 +38,7 @@ import qualified Data.IntMap                                   as IntMap
 import           Data.List                                     (intersperse, sortOn)
 import           Data.Maybe                                    (fromMaybe)
 import qualified Data.Set                                      as Set
+import           Data.String                                   (IsString(..))
 import qualified Data.Text                                     as Text
 import           Prelude                                       hiding (fail)
 import           Prettyprinter
@@ -63,7 +64,7 @@ traceTerm ctx t a = trace (ctx ++ ": " ++ showTerm t) a
 
 data TranslationState = TranslationState
 
-  { _globalDeclarations :: [String]
+  { _globalDeclarations :: [Coq.Ident]
   -- ^ 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
@@ -106,6 +107,7 @@ makeLenses ''TranslationState
 reservedIdents :: Set.Set Coq.Ident
 reservedIdents =
   Set.fromList $
+  map fromString $
   concatMap words $
   [ "_ Axiom CoFixpoint Definition Fixpoint Hypothesis IF Parameter Prop"
   , "SProp Set Theorem Type Variable as at by cofix discriminated else"
@@ -115,10 +117,10 @@ reservedIdents =
 
 -- | Extract the list of names from a list of Coq declarations.  Not all
 -- declarations have names, e.g. comments and code snippets come without names.
-namedDecls :: [Coq.Decl] -> [String]
+namedDecls :: [Coq.Decl] -> [Coq.Ident]
 namedDecls = concatMap filterNamed
   where
-    filterNamed :: Coq.Decl -> [String]
+    filterNamed :: Coq.Decl -> [Coq.Ident]
     filterNamed (Coq.Axiom n _)                               = [n]
     filterNamed (Coq.Comment _)                               = []
     filterNamed (Coq.Definition n _ _ _)                      = [n]
@@ -129,7 +131,7 @@ namedDecls = concatMap filterNamed
 -- translation state.
 getNamesOfAllDeclarations ::
   TermTranslationMonad m =>
-  m [String]
+  m [Coq.Ident]
 getNamesOfAllDeclarations = view allDeclarations <$> get
   where
     allDeclarations =
@@ -140,7 +142,7 @@ type TermTranslationMonad m = TranslationMonad TranslationState m
 runTermTranslationMonad ::
   TranslationConfiguration ->
   Maybe ModuleName ->
-  [String] ->
+  [Coq.Ident] ->
   [Coq.Ident] ->
   (forall m. TermTranslationMonad m => m a) ->
   Either (TranslationError Term) (a, TranslationState)
@@ -162,6 +164,7 @@ translateIdentWithArgs :: TermTranslationMonad m => Ident -> [Term] -> m Coq.Ter
 translateIdentWithArgs i args =
   (view currentModule <$> get) >>= \cur_modname ->
   let identToCoq ident =
+        fromString $
         if Just (identModule ident) == cur_modname then identName ident else
           show (translateModuleName (identModule ident))
           ++ "." ++ identName ident in
@@ -221,7 +224,7 @@ flatTermFToExpr tf = -- traceFTermF "flatTermFToExpr" tf $
     RecursorApp d parameters motive eliminators indices termEliminated ->
       do maybe_d_trans <- translateIdentToIdent d
          rect_var <- case maybe_d_trans of
-           Just i -> return $ Coq.Var (show i ++ "_rect")
+           Just i -> return $ Coq.Var (fromString (show i ++ "_rect"))
            Nothing ->
              errorTermM ("Recursor for " ++ show d ++
                          " cannot be translated because the datatype " ++
@@ -338,7 +341,7 @@ translatePi binders body = withLocalLocalEnvironment $ do
 -- | Translate a local name from a saw-core binder into a fresh Coq identifier.
 translateLocalIdent :: TermTranslationMonad m => LocalName -> m Coq.Ident
 translateLocalIdent x = freshVariant ident0
-  where ident0 = Text.unpack x -- TODO: use some string encoding to ensure lexically valid Coq identifiers
+  where ident0 = fromString (Text.unpack x) -- TODO: use some string encoding to ensure lexically valid Coq identifiers
 
 -- | Find an fresh, as-yet-unused variant of the given Coq identifier.
 freshVariant :: TermTranslationMonad m => Coq.Ident -> m Coq.Ident
@@ -351,7 +354,7 @@ freshVariant x =
      return ident
 
 nextVariant :: Coq.Ident -> Coq.Ident
-nextVariant = reverse . go . reverse
+nextVariant (Coq.Ident s) = fromString (reverse (go (reverse s)))
   where
     go :: String -> String
     go (c : cs)
@@ -563,8 +566,8 @@ defaultTermForType typ = do
 translateTermToDocWith ::
   TranslationConfiguration ->
   Maybe ModuleName ->
-  [String] ->
-  [String] ->
+  [Coq.Ident] ->
+  [Coq.Ident] ->
   (Coq.Term -> Doc ann) ->
   Term ->
   Either (TranslationError Term) (Doc ann)
@@ -582,7 +585,7 @@ translateTermToDocWith configuration mn globalDecls localEnv f t = do
 translateDefDoc ::
   TranslationConfiguration ->
   Maybe ModuleName ->
-  [String] ->
+  [Coq.Ident] ->
   Coq.Ident -> Term ->
   Either (TranslationError Term) (Doc ann)
 translateDefDoc configuration mn globalDecls name =

src/SAWScript/Prover/Exporter.hs

@@ -52,6 +52,7 @@ import qualified Data.ByteString as BS
 import Data.Parameterized.Nonce (globalNonceGenerator)
 import Data.Parameterized.Some (Some(..))
 import Data.Set (Set)
+import Data.String (IsString(..))
 import qualified Data.SBV.Dynamic as SBV
 import System.Directory (removeFile)
 import System.IO
@@ -345,10 +346,10 @@ coqTranslationConfiguration ::
   [String] ->
   Coq.TranslationConfiguration
 coqTranslationConfiguration notations skips = Coq.TranslationConfiguration
-  { Coq.notations = notations
+  { Coq.notations = map (fmap fromString) notations
   , Coq.monadicTranslation = False
   , Coq.postPreamble = []
-  , Coq.skipDefinitions = skips
+  , Coq.skipDefinitions = map fromString skips
   , Coq.vectorModule = "SAWCoreVectorsAsCoqVectors"
   }
 
@@ -381,7 +382,7 @@ writeCoqTerm name notations skips path t = do
         withImportSAWCorePrelude $
         withImportCryptolPrimitivesForSAWCore $
         coqTranslationConfiguration notations skips
-  case Coq.translateTermAsDeclImports configuration name t of
+  case Coq.translateTermAsDeclImports configuration (fromString name) t of
     Left err -> throwTopLevel $ "Error translating: " ++ show err
     Right doc -> io $ case path of
       "" -> print doc
@@ -413,7 +414,7 @@ writeCoqCryptolModule inputFile outputFile notations skips = io $ do
   env <- initCryptolEnv sc
   cryptolPrimitivesForSAWCoreModule <- scFindModule sc nameOfCryptolPrimitivesForSAWCoreModule
   (cm, _) <- loadCryptolModule sc env inputFile
-  let cryptolPreludeDecls = map Coq.moduleDeclName (moduleDecls cryptolPrimitivesForSAWCoreModule)
+  let cryptolPreludeDecls = map (fromString . Coq.moduleDeclName) (moduleDecls cryptolPrimitivesForSAWCoreModule)
   let configuration =
         withImportSAWCorePrelude $
         withImportCryptolPrimitivesForSAWCore $