Adapt to GaloisInc/saw-core#119.

This switched lambda and pi binders in the saw-core AST from
String to Text (introducing a new type synonym LocalName).

src/Verifier/SAW/Translation/Coq/Term.hs

@@ -230,7 +230,7 @@ flatTermFToExpr tf = -- traceFTermF "flatTermFToExpr" tf $
                    )
         in
         foldM addElement (Coq.App (Coq.Var "Vector.nil") [Coq.Var "_"]) (Vector.reverse vec)
-    StringLit s -> pure (Coq.Scope (Coq.StringLit s) "string")
+    StringLit s -> pure (Coq.Scope (Coq.StringLit (Text.unpack s)) "string")
     ExtCns (EC _ _ _) -> errorTermM "External constants not supported"
 
     -- The translation of a record type {fld1:tp1, ..., fldn:tpn} is
@@ -293,7 +293,7 @@ mkDefinition name t = Coq.Definition name [] Nothing 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 => String -> m Coq.Ident
+freshenAndBindName :: TermTranslationMonad m => LocalName -> m Coq.Ident
 freshenAndBindName n =
   do n' <- translateLocalIdent n
      modify $ over localEnvironment (n' :)
@@ -304,15 +304,15 @@ mkLet (name, rhs) body = Coq.Let name [] Nothing rhs body
 
 translateParams ::
   TermTranslationMonad m =>
-  [(String, Term)] -> m [Coq.Binder]
+  [(LocalName, Term)] -> m [Coq.Binder]
 translateParams [] = return []
 translateParams ((n, ty):ps) = do
   ty' <- translateTerm ty
   n' <- freshenAndBindName n
   ps' <- translateParams ps
   return (Coq.Binder n' (Just ty') : ps')
 
-translatePi :: TermTranslationMonad m => [(String, Term)] -> Term -> m Coq.Term
+translatePi :: TermTranslationMonad m => [(LocalName, Term)] -> Term -> m Coq.Term
 translatePi binders body = withLocalLocalEnvironment $ do
   bindersT <- forM binders $ \ (b, bType) -> do
     bTypeT <- translateTerm bType
@@ -323,10 +323,15 @@ translatePi binders body = withLocalLocalEnvironment $ do
   return $ Coq.Pi bindersT bodyT
 
 -- | Translate a local name from a saw-core binder into a fresh Coq identifier.
-translateLocalIdent :: TermTranslationMonad m => String -> m Coq.Ident
-translateLocalIdent x =
+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
+
+-- | 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 -- TODO: use some string encoding to ensure lexically valid Coq identifiers
+     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)
@@ -358,7 +363,7 @@ translateTermLet t =
     keep (t', n) = n > 1 && shouldMemoizeTerm t'
     nextName =
       do x <- view nextSharedName <$> get
-         x' <- translateLocalIdent x
+         x' <- freshVariant x
          modify $ set nextSharedName (nextVariant x')
          pure x'