saw-core-coq: Define newtype for Coq Ident and ModuleName types.

saw-central/src/SAWCentral/Prover/Exporter.hs

@@ -86,6 +86,7 @@ import SAWCore.Recognizer (asPi)
 import SAWCore.SATQuery
 import SAWCore.SharedTerm as SC
 import qualified SAWCoreCoq.Coq as Coq
+import qualified Language.Coq.AST as Coq
 import CryptolSAWCore.TypedTerm
 import qualified SAWCoreAIG.BitBlast as BBSim
 import qualified SAWCore.Simulator.Value as Sim
@@ -490,7 +491,7 @@ writeCoqTerm name notations skips path t = do
   sc <- getSharedContext
   mm <- io $ scGetModuleMap sc
   tp <- io $ scTypeOf sc t
-  case Coq.translateTermAsDeclImports configuration mm (Text.unpack name) t tp of
+  case Coq.translateTermAsDeclImports configuration mm (Coq.Ident (Text.unpack name)) t tp of
     Left err -> throwTopLevel $ "Error translating: " ++ show err
     Right doc -> io $ case path of
       "" -> print doc
@@ -533,14 +534,16 @@ writeCoqCryptolModule mon inputFile outputFile notations skips = io $ do
   (cm, _) <- loadCryptolModule sc primOpts env inputFile
   cry_env <- mkCryEnv env
   cm' <- if mon then fst <$> monadifyCryptolModule sc cry_env defaultMonEnv cm else return cm
-  let cryptolPreludeDecls = mapMaybe Coq.moduleDeclName (moduleDecls cryptolPrimitivesForSAWCoreModule)
+  let cryptolPreludeDecls =
+        map Coq.Ident $
+        mapMaybe Coq.moduleDeclName (moduleDecls cryptolPrimitivesForSAWCoreModule)
   let configuration =
         withImportCryptolPrimitivesForSAWCoreExtra $
         withImportCryptolPrimitivesForSAWCore $
         withImportSAWCorePreludeExtra $
         withImportSAWCorePrelude $
         coqTranslationConfiguration notations skips
-  let nm = takeBaseName inputFile
+  let nm = Coq.Ident (takeBaseName inputFile)
   res <- Coq.translateCryptolModule sc cry_env nm configuration cryptolPreludeDecls cm'
   case res of
     Left e -> putStrLn $ show e

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

@@ -9,7 +9,22 @@ 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
+
+newtype ModuleName = ModuleName String
+  deriving (Eq, Ord)
+
+instance Show ModuleName where
+  show (ModuleName s) = show 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) = text s
 
 ppBinder :: Binder -> Doc ann
 ppBinder (Binder x Nothing)  = ppIdent x
@@ -102,7 +102,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) $
@@ -157,22 +157,22 @@ ppDecl :: Decl -> Doc ann
 ppDecl decl = case decl of
   Axiom nm ty ->
     nest 2 (
-      hsep [text "Axiom", text nm, text ":", ppTerm PrecNone ty, period]
+      hsep [text "Axiom", ppIdent nm, text ":", ppTerm PrecNone ty, period]
     ) <> hardline
   Parameter nm ty ->
     nest 2 (
-     hsep [text "Parameter", text nm, text ":", ppTerm PrecNone ty, period]
+     hsep [text "Parameter", ppIdent nm, text ":", ppTerm PrecNone ty, period]
     ) <> hardline
   Variable nm ty ->
     nest 2 (
-      hsep [text "Variable", text nm, text ":", ppTerm PrecNone ty, period]
+      hsep [text "Variable", 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
@@ -181,17 +181,17 @@ ppDecl decl = case decl of
   InductiveDecl ind -> ppInductive ind
   Section nm ds ->
     vsep $ concat
-     [ [ hsep [text "Section", text nm, period] ]
+     [ [ hsep [text "Section", ppIdent nm, period] ]
      , map (indent 2 . ppDecl) ds
-     , [ hsep [text "End", text nm, period] ]
+     , [ hsep [text "End", ppIdent nm, period] ]
      ]
   Snippet s -> text s
 
 ppConstructor :: Constructor -> Doc ann
 ppConstructor (Constructor {..}) =
   nest 2 $
   hsep [ text "|"
-       , text constructorName
+       , ppIdent constructorName
        , text ":"
        , ppTerm PrecNone constructorType
        ]
@@ -201,7 +201,7 @@ ppInductive (Inductive {..}) =
   (vsep
    ([ nest 2 $
       hsep ([ text "Inductive"
-            , text inductiveName
+            , ppIdent inductiveName
             ]
             ++ map ppBinder inductiveParameters
             ++ [ text ":" ]

saw-core-coq/src/SAWCoreCoq/Coq.hs

@@ -97,7 +97,7 @@ translateCryptolModule ::
   Coq.Ident {- ^ Section name -} ->
   TranslationConfiguration ->
   -- | List of already translated global declarations
-  [String] ->
+  [Coq.Ident] ->
   CryptolModule ->
   IO (Either (TranslationError Term) (Doc ann))
 translateCryptolModule sc env nm configuration globalDecls m = do

saw-core-coq/src/SAWCoreCoq/CryptolModule.hs

@@ -25,7 +25,7 @@ translateTypedTermMap ::
 translateTypedTermMap defs = forM defs translateAndRegisterEntry
   where
     translateAndRegisterEntry (name, t, tp) = do
-      let nameStr = unpackIdent (nameIdent name)
+      let nameStr = Coq.Ident (unpackIdent (nameIdent name))
       decl <-
         do t_trans <- TermTranslation.translateTerm t
            tp_trans <- TermTranslation.translateTerm tp
@@ -41,7 +41,7 @@ translateCryptolModule ::
   SharedContext -> Env ->
   TranslationConfiguration ->
   -- | List of already translated global declarations
-  [String] ->
+  [Coq.Ident] ->
   CryptolModule ->
   IO (Either (TranslationError Term) [Coq.Decl])
 translateCryptolModule sc env configuration globalDecls (CryptolModule _ tm) =

saw-core-coq/src/SAWCoreCoq/SAWModule.hs

@@ -69,7 +69,7 @@ translateCtor inductiveParameters (Ctor {..}) = do
       ModuleIdentifier ident -> liftTermTranslationMonad $ TermTranslation.translateIdentToIdent ident
       ImportedName{} -> pure Nothing
   let constructorName = case maybe_constructorName of
-        Just n -> identName n
+        Just n -> n
         Nothing -> error "translateCtor: unexpected translation for constructor"
   constructorType <-
     -- Unfortunately, `ctorType` qualifies the inductive type's name in the
@@ -91,12 +91,12 @@ translateDataType (DataType {..}) =
   case dtNameInfo of
     ModuleIdentifier dtName ->
       atDefSite <$> findSpecialTreatment dtName >>= \case
-      DefPreserve            -> translateNamed $ identName dtName
+      DefPreserve            -> translateNamed $ Coq.Ident (identName dtName)
       DefRename   targetName -> translateNamed $ targetName
       DefReplace  str        -> return $ Coq.Snippet str
       DefSkip                -> return $ skipped dtName
     ImportedName{} ->
-      translateNamed $ Text.unpack (toShortName dtNameInfo)
+      translateNamed $ Coq.Ident (Text.unpack (toShortName dtNameInfo))
   where
     translateNamed :: ModuleTranslationMonad m => Coq.Ident -> m Coq.Decl
     translateNamed name = do
@@ -154,7 +154,7 @@ translateDef (Def {..}) = {- trace ("translateDef " ++ show defIdent) $ -} do
   where
 
     translateAccordingly :: ModuleTranslationMonad m => DefSiteTreatment -> m Coq.Decl
-    translateAccordingly  DefPreserve           = translateNamed $ Text.unpack (toShortName defNameInfo)
+    translateAccordingly  DefPreserve           = translateNamed $ Coq.Ident (Text.unpack (toShortName defNameInfo))
     translateAccordingly (DefRename targetName) = translateNamed $ targetName
     translateAccordingly (DefReplace  str)      = return $ Coq.Snippet str
     translateAccordingly  DefSkip               = return $ skipped' defNameInfo

saw-core-coq/src/SAWCoreCoq/SpecialTreatment.hs

@@ -50,7 +50,7 @@ data DefSiteTreatment
     DefPreserve
   | -- | Translate the identifier into the given Coq identifer,
     --   and otherwise directly translate the associated SAWCore declaration.
-    DefRename String
+    DefRename Coq.Ident
   | -- | Replace the declaration of the identifier with the given text.
     DefReplace  String
     -- | Skip the declartion of the identifier altogether.
@@ -65,7 +65,7 @@ data UseSiteTreatment
     --   identifier should be an "explicit" identifier with a leading \"\@\"
     --   symbol, which indicates to Coq that all implicit arguments should be
     --   treated as explicit.
-  | UseRename   (Maybe ModuleName) String Bool
+  | UseRename (Maybe Coq.ModuleName) Coq.Ident Bool
     -- | Apply a macro function to the translations of the first @n@ SAWCore
     -- arguments of this identifier
   | UseMacro Int ([Coq.Term] -> Coq.Term)
@@ -75,17 +75,18 @@ data IdentSpecialTreatment = IdentSpecialTreatment
   , atUseSite :: UseSiteTreatment
   }
 
-moduleRenamingMap :: Map.Map ModuleName ModuleName
+moduleRenamingMap :: Map.Map ModuleName Coq.ModuleName
 moduleRenamingMap = Map.fromList $
   over _1 (mkModuleName . (: [])) <$>
-  over _2 (mkModuleName . (: [])) <$>
+  over _2 Coq.ModuleName <$>
   [ ("Cryptol", "CryptolPrimitivesForSAWCore")
   , ("Prelude", "SAWCorePrelude")
   ]
 
-translateModuleName :: ModuleName -> ModuleName
+translateModuleName :: ModuleName -> Coq.ModuleName
 translateModuleName mn =
-  Map.findWithDefault mn mn moduleRenamingMap
+  Map.findWithDefault def mn moduleRenamingMap
+  where def = Coq.ModuleName (Text.unpack (moduleNameText mn))
 
 findSpecialTreatment' ::
   TranslationConfigurationMonad r m =>
@@ -112,22 +113,22 @@ findSpecialTreatment ident = do
 -- | Use `mapsTo` for identifiers whose definition has a matching definition
 -- already on the Coq side.  As such, their definition can be skipped, and use
 -- sites can be replaced by the appropriate call.
-mapsTo :: ModuleName -> String -> IdentSpecialTreatment
+mapsTo :: Coq.ModuleName -> Coq.Ident -> IdentSpecialTreatment
 mapsTo targetModule targetName = IdentSpecialTreatment
   { atDefSite = DefSkip
   , atUseSite = UseRename (Just targetModule) targetName False
   }
 
 -- | Like 'mapsTo' but use an explicit variable reference so
 -- that all implicit arguments must be provided.
-mapsToExpl :: ModuleName -> String -> IdentSpecialTreatment
+mapsToExpl :: Coq.ModuleName -> Coq.Ident -> IdentSpecialTreatment
 mapsToExpl targetModule targetName = IdentSpecialTreatment
   { atDefSite = DefSkip
   , atUseSite = UseRename (Just targetModule) targetName True
   }
 
 -- | Like 'mapsToExpl' but add an @n@th argument that is inferred by Coq
-mapsToExplInferArg :: String -> Int -> IdentSpecialTreatment
+mapsToExplInferArg :: Coq.Ident -> Int -> IdentSpecialTreatment
 mapsToExplInferArg targetName argNum = IdentSpecialTreatment
   { atDefSite = DefSkip
   , atUseSite = UseMacro argNum (\args ->
@@ -152,7 +153,7 @@ realize code = IdentSpecialTreatment
 -- SAWCore/Cryptol side clashes with names on the Coq side. For instance, `at`
 -- is a reserved Coq keyword, but is used as a function name in SAWCore Prelude.
 -- Also useful for translation notations, until they are better supported.
-rename :: String -> IdentSpecialTreatment
+rename :: Coq.Ident -> IdentSpecialTreatment
 rename ident = IdentSpecialTreatment
   { atDefSite = DefRename ident
   , atUseSite = UseRename Nothing ident False
@@ -181,44 +182,41 @@ skip = IdentSpecialTreatment
   }
 
 -- | The Coq built-in @Datatypes@ module
-datatypesModule :: ModuleName
-datatypesModule =
-  mkModuleName ["Coq", "Init", "Datatypes"]
+datatypesModule :: Coq.ModuleName
+datatypesModule = Coq.ModuleName "Coq.Init.Datatypes"
 
 -- | The Coq built-in @Logic@ module
-logicModule :: ModuleName
-logicModule =
-  mkModuleName ["Coq", "Init", "Logic"]
+logicModule :: Coq.ModuleName
+logicModule = Coq.ModuleName "Coq.Init.Logic"
 
 -- | The Coq built-in @String@ module.
-stringModule :: ModuleName
-stringModule =
-  mkModuleName ["Coq", "Strings", "String"]
+stringModule :: Coq.ModuleName
+stringModule = Coq.ModuleName "Coq.Strings.String"
 
 -- | The @SAWCoreScaffolding@ module
-sawDefinitionsModule :: ModuleName
-sawDefinitionsModule = mkModuleName ["SAWCoreScaffolding"]
+sawDefinitionsModule :: Coq.ModuleName
+sawDefinitionsModule = Coq.ModuleName "SAWCoreScaffolding"
 
-specMModule :: ModuleName
-specMModule = mkModuleName ["SpecM"]
+specMModule :: Coq.ModuleName
+specMModule = Coq.ModuleName "SpecM"
 
-tpDescModule :: ModuleName
-tpDescModule = mkModuleName ["TpDesc"]
+tpDescModule :: Coq.ModuleName
+tpDescModule = Coq.ModuleName "TpDesc"
 
 {-
-polyListModule :: ModuleName
-polyListModule = mkModuleName ["PolyList"]
+polyListModule :: Coq.ModuleName
+polyListModule = Coq.ModuleName "PolyList"
 -}
 
-sawVectorDefinitionsModule :: TranslationConfiguration -> ModuleName
+sawVectorDefinitionsModule :: TranslationConfiguration -> Coq.ModuleName
 sawVectorDefinitionsModule (TranslationConfiguration {..}) =
-  mkModuleName [Text.pack vectorModule]
+  Coq.ModuleName vectorModule
 
 cryptolPrimitivesModule :: ModuleName
 cryptolPrimitivesModule = mkModuleName ["CryptolPrimitivesForSAWCore"]
 
-preludeExtraModule :: ModuleName
-preludeExtraModule = mkModuleName ["SAWCorePreludeExtra"]
+preludeExtraModule :: Coq.ModuleName
+preludeExtraModule = Coq.ModuleName "SAWCorePreludeExtra"
 
 specialTreatmentMap :: TranslationConfiguration ->
                        Map.Map ModuleName (Map.Map String IdentSpecialTreatment)
@@ -555,7 +553,7 @@ specMSpecialTreatmentMap _configuration =
   Map.fromList $
 
   -- Type descriptions
-  map (\str -> (str, mapsTo specMModule str))
+  map (\str -> (str, mapsTo specMModule (Coq.Ident str)))
   [ "ExprKind", "Kind_unit", "Kind_bool", "Kind_nat", "Kind_bv"
   , "TpExprUnOp", "UnOp_BVToNat", "UnOp_NatToBV"
   , "TpExprBinOp", "BinOp_AddNat", "BinOp_MulNat", "BinOp_AddBV", "BinOp_MulBV"
@@ -598,10 +596,10 @@ specMSpecialTreatmentMap _configuration =
 
 
 
-escapeIdent :: String -> String
-escapeIdent str
-  | all okChar str = str
-  | otherwise      = "Op_" ++ zEncodeString str
+escapeIdent :: Coq.Ident -> Coq.Ident
+escapeIdent (Coq.Ident str)
+  | all okChar str = Coq.Ident str
+  | otherwise      = Coq.Ident ("Op_" ++ zEncodeString str)
  where
    okChar x = isAlphaNum x || x `elem` ("_'" :: String)