Switch Lambda and Pi constructors to use Text instead of String.

We introduce a type synonym `LocalName = Text` for this purpose.

This is a step toward removing all uses of `String` in saw-core
(#44).

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

@@ -43,7 +43,7 @@ import qualified Cryptol.TypeCheck.Subst as C (Subst, apSubst, singleTParamSubst
 import qualified Cryptol.ModuleSystem.Name as C
   (asPrim, nameUnique, nameIdent, nameInfo, NameInfo(..))
 import qualified Cryptol.Utils.Ident as C
-  ( Ident, PrimIdent(..), mkIdent, unpackIdent, prelPrim, floatPrim, arrayPrim
+  ( Ident, PrimIdent(..), mkIdent, prelPrim, floatPrim, arrayPrim
   , ModName, modNameToText, identText, interactiveName
   )
 import qualified Cryptol.Utils.RecordMap as C
@@ -58,7 +58,7 @@ import Verifier.SAW.Prim (BitVector(..))
 import Verifier.SAW.Rewriter
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.Simulator.MonadLazy (force)
-import Verifier.SAW.TypedAST (mkSort, mkModuleName, FieldName)
+import Verifier.SAW.TypedAST (mkSort, mkModuleName, FieldName, LocalName)
 
 import GHC.Stack
 
@@ -294,23 +294,22 @@ importPropsType sc env (prop : props) ty
        t <- importPropsType sc env props ty
        scFun sc p t
 
-nameToString :: C.Name -> String
-nameToString = C.unpackIdent . C.nameIdent
+nameToLocalName :: C.Name -> LocalName
+nameToLocalName = C.identText . C.nameIdent
 
 nameToFieldName :: C.Name -> FieldName
 nameToFieldName = C.identText . C.nameIdent
 
-tparamToString :: C.TParam -> String
---tparamToString tp = maybe "_" nameToString (C.tpName tp)
-tparamToString tp = maybe ("u" ++ show (C.tpUnique tp)) nameToString (C.tpName tp)
+tparamToLocalName :: C.TParam -> LocalName
+tparamToLocalName tp = maybe (Text.pack ("u" ++ show (C.tpUnique tp))) nameToLocalName (C.tpName tp)
 
 importPolyType :: SharedContext -> Env -> [C.TParam] -> [C.Prop] -> C.Type -> IO Term
 importPolyType sc env [] props ty = importPropsType sc env props ty
 importPolyType sc env (tp : tps) props ty =
   do k <- importKind sc (C.tpKind tp)
      env' <- bindTParam sc tp env
      t <- importPolyType sc env' tps props ty
-     scPi sc (tparamToString tp) k t
+     scPi sc (tparamToLocalName tp) k t
 
 importSchema :: SharedContext -> Env -> C.Schema -> IO Term
 importSchema sc env (C.Forall tparams props ty) = importPolyType sc env tparams props ty
@@ -870,7 +869,7 @@ importExpr sc env expr =
       do env' <- bindTParam sc tp env
          k <- importKind sc (C.tpKind tp)
          e' <- importExpr sc env' e
-         scLambda sc (tparamToString tp) k e'
+         scLambda sc (tparamToLocalName tp) k e'
 
     C.ETApp e t ->
       do e' <- importExpr sc env e
@@ -891,7 +890,7 @@ importExpr sc env expr =
       do t' <- importType sc env t
          env' <- bindName sc x (C.tMono t) env
          e' <- importExpr sc env' e
-         scLambda sc (nameToString x) t' e'
+         scLambda sc (nameToLocalName x) t' e'
 
     C.EProofAbs prop e
       | isErasedProp prop -> importExpr sc env e
@@ -958,15 +957,15 @@ importExpr' sc env schema expr =
          env' <- bindTParam sc tp env
          k <- importKind sc (C.tpKind tp)
          e' <- importExpr' sc env' schema' e
-         scLambda sc (tparamToString tp) k e'
+         scLambda sc (tparamToLocalName tp) k e'
 
     C.EAbs x _ e ->
       do ty <- the (C.isMono schema)
          (a, b) <- the (C.tIsFun ty)
          a' <- importType sc env a
          env' <- bindName sc x (C.tMono a) env
          e' <- importExpr' sc env' (C.tMono b) e
-         scLambda sc (nameToString x) a' e'
+         scLambda sc (nameToLocalName x) a' e'
 
     C.EProofAbs _ e ->
       do (prop, schema') <-
@@ -1203,7 +1202,7 @@ importDeclGroup isTopLevel sc env (C.Recursive [decl]) =
       do env1 <- bindName sc (C.dName decl) (C.dSignature decl) env
          t' <- importSchema sc env (C.dSignature decl)
          e' <- importExpr' sc env1 (C.dSignature decl) expr
-         let x = nameToString (C.dName decl)
+         let x = nameToLocalName (C.dName decl)
          f' <- scLambda sc x t' e'
          rhs <- scGlobalApply sc "Prelude.fix" [t', f']
          rhs' <- if isTopLevel then
@@ -1409,7 +1408,7 @@ lambdaTuple sc env ty expr argss ((x, t) : args) =
   do a <- importType sc env t
      env' <- bindName sc x (C.Forall [] [] t) env
      e <- lambdaTuple sc env' ty expr argss args
-     f <- scLambda sc (nameToString x) a e
+     f <- scLambda sc (nameToLocalName x) a e
      if null args
         then return f
         else do b <- importType sc env (tNestedTuple (map snd args))
@@ -1447,7 +1446,7 @@ importMatches sc env (C.From name _len _eltty expr : matches) = do
   (body, len2, ty2, args) <- importMatches sc env' matches
   n <- importType sc env len2
   b <- importType sc env ty2
-  f <- scLambda sc (nameToString name) a body
+  f <- scLambda sc (nameToLocalName name) a body
   result <- scGlobalApply sc "Cryptol.from" [a, b, m, n, xs, f]
   return (result, C.tMul len1 len2, C.tTuple [ty1, ty2], (name, ty1) : args)
 
@@ -1477,7 +1476,7 @@ importMatches sc env (C.Let decl : matches) =
      (body, len, ty2, args) <- importMatches sc env' matches
      n <- importType sc env len
      b <- importType sc env ty2
-     f <- scLambda sc (nameToString (C.dName decl)) a body
+     f <- scLambda sc (nameToLocalName (C.dName decl)) a body
      result <- scGlobalApply sc "Cryptol.mlet" [a, b, n, e, f]
      return (result, len, C.tTuple [ty1, ty2], (C.dName decl, ty1) : args)
 

saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs

@@ -463,7 +463,7 @@ asAIGType :: SharedContext -> Term -> IO [(String, Term)]
 asAIGType sc t = do
   t' <- scWhnf sc t
   case t' of
-    (R.asPi -> Just (n, t1, t2)) -> ((n, t1) :) <$> asAIGType sc t2
+    (R.asPi -> Just (n, t1, t2)) -> ((Text.unpack n, t1) :) <$> asAIGType sc t2
     (R.asBoolType -> Just ())    -> return []
     (R.asVecType -> Just _)      -> return []
     (R.asTupleType -> Just _)    -> return []

saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs

@@ -669,7 +669,7 @@ sbvSolve :: SharedContext
 sbvSolve sc addlPrims unintSet t = do
   let eval = sbvSolveBasic sc addlPrims unintSet
   ty <- eval =<< scTypeOf sc t
-  let lamNames = map fst (fst (R.asLambdaList t))
+  let lamNames = map (Text.unpack . fst) (fst (R.asLambdaList t))
   let varNames = [ "var" ++ show (i :: Integer) | i <- [0 ..] ]
   let argNames = zipWith (++) varNames (map ("_" ++) lamNames ++ repeat "")
   argTs <- asPredType (toTValue ty)

saw-core-what4/src/Verifier/SAW/Simulator/What4.hs

@@ -875,7 +875,7 @@ w4SolveAny sym sc ps unintSet t = give sym $ do
   ty <- eval =<< scTypeOf sc t
 
   -- get the names of the arguments to the function
-  let argNames = map fst (fst (R.asLambdaList t))
+  let argNames = map (Text.unpack . fst) (fst (R.asLambdaList t))
   let moreNames = [ "var" ++ show (i :: Integer) | i <- [0 ..] ]
 
   -- and their types
@@ -1082,7 +1082,7 @@ w4EvalAny sym sc ps unintSet t =
      ty <- eval =<< scTypeOf sc t
 
      -- get the names of the arguments to the function
-     let lamNames = map fst (fst (R.asLambdaList t))
+     let lamNames = map (Text.unpack . fst) (fst (R.asLambdaList t))
      let varNames = [ "var" ++ show (i :: Integer) | i <- [0 ..] ]
      let argNames = zipWith (++) varNames (map ("_" ++) lamNames ++ repeat "")
 

saw-core/src/Verifier/SAW/ExternalFormat.hs

@@ -124,8 +124,8 @@ scWriteExternal t0 =
     writeTermF tf =
       case tf of
         App e1 e2      -> pure $ unwords ["App", show e1, show e2]
-        Lambda s t e   -> pure $ unwords ["Lam", s, show t, show e]
-        Pi s t e       -> pure $ unwords ["Pi", s, show t, show e]
+        Lambda s t e   -> pure $ unwords ["Lam", Text.unpack s, show t, show e]
+        Pi s t e       -> pure $ unwords ["Pi", Text.unpack s, show t, show e]
         LocalVar i     -> pure $ unwords ["Var", show i]
         Constant ec e  ->
             do stashName ec
@@ -225,8 +225,8 @@ scReadExternal sc input =
     parse tokens =
       case tokens of
         ["App", e1, e2]     -> App <$> readIdx e1 <*> readIdx e2
-        ["Lam", x, t, e]    -> Lambda x <$> readIdx t <*> readIdx e
-        ["Pi", s, t, e]     -> Pi s <$> readIdx t <*> readIdx e
+        ["Lam", x, t, e]    -> Lambda (Text.pack x) <$> readIdx t <*> readIdx e
+        ["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))

saw-core/src/Verifier/SAW/Module.hs

@@ -191,9 +191,9 @@ data DataType =
   DataType
   { dtName :: Ident
     -- ^ The name of this datatype
-  , dtParams :: [(String,Term)]
+  , dtParams :: [(LocalName, Term)]
     -- ^ The context of parameters of this datatype
-  , dtIndices :: [(String,Term)]
+  , dtIndices :: [(LocalName, Term)]
     -- ^ The context of indices of this datatype
   , dtSort :: Sort
     -- ^ The universe of this datatype

saw-core/src/Verifier/SAW/OpenTerm.hs

@@ -107,20 +107,20 @@ openTermTopVar =
 
 -- | Build an open term inside a binder of a variable with the given name and
 -- type, where the binder is represented as a Haskell function on 'OpenTerm's
-bindOpenTerm :: String -> TypedTerm -> (OpenTerm -> OpenTerm) -> TCM TypedTerm
+bindOpenTerm :: LocalName -> TypedTerm -> (OpenTerm -> OpenTerm) -> TCM TypedTerm
 bindOpenTerm x tp body_f =
   do tp_whnf <- typeCheckWHNF $ typedVal tp
      withVar x tp_whnf (openTermTopVar >>= (unOpenTerm . body_f))
 
 -- | Build a lambda abstraction as an 'OpenTerm'
-lambdaOpenTerm :: String -> OpenTerm -> (OpenTerm -> OpenTerm) -> OpenTerm
+lambdaOpenTerm :: LocalName -> OpenTerm -> (OpenTerm -> OpenTerm) -> OpenTerm
 lambdaOpenTerm x (OpenTerm tpM) body_f = OpenTerm $
   do tp <- tpM
      body <- bindOpenTerm x tp body_f
      typeInferComplete $ Lambda x tp body
 
 -- | Build a Pi abstraction as an 'OpenTerm'
-piOpenTerm :: String -> OpenTerm -> (OpenTerm -> OpenTerm) -> OpenTerm
+piOpenTerm :: LocalName -> OpenTerm -> (OpenTerm -> OpenTerm) -> OpenTerm
 piOpenTerm x (OpenTerm tpM) body_f = OpenTerm $
   do tp <- tpM
      body <- bindOpenTerm x tp body_f
@@ -154,9 +154,10 @@ dedupOpenTermM (OpenTerm trmM) =
 -- 'OpenTerm's that also returns an auxiliary value. Returns the normalized type
 -- and the body, along with the auxiliary result returned by the body-generating
 -- function.
-bindOpenTermAuxM :: String -> OpenTerm ->
-                    (OpenTerm -> OpenTermM (OpenTerm, a)) ->
-                    OpenTermM (TypedTerm, TypedTerm, a)
+bindOpenTermAuxM ::
+  LocalName -> OpenTerm ->
+  (OpenTerm -> OpenTermM (OpenTerm, a)) ->
+  OpenTermM (TypedTerm, TypedTerm, a)
 bindOpenTermAuxM x (OpenTerm tpM) body_f =
   OpenTermM $
   do TypedTerm tp tp_tp <- tpM
@@ -167,30 +168,34 @@ bindOpenTermAuxM x (OpenTerm tpM) body_f =
      return (TypedTerm tp_whnf tp_tp, body, a)
 
 -- | Build a lambda abstraction in the 'OpenTermM' monad
-lambdaOpenTermM :: String -> OpenTerm -> (OpenTerm -> OpenTermM OpenTerm) ->
-                   OpenTermM OpenTerm
+lambdaOpenTermM ::
+  LocalName -> OpenTerm -> (OpenTerm -> OpenTermM OpenTerm) ->
+  OpenTermM OpenTerm
 lambdaOpenTermM x tp body_f =
   fst <$> lambdaOpenTermAuxM x tp (body_f >=> (\t -> return (t, ())))
 
 -- | Build a pi abstraction in the 'OpenTermM' monad
-piOpenTermM :: String -> OpenTerm -> (OpenTerm -> OpenTermM OpenTerm) ->
-               OpenTermM OpenTerm
+piOpenTermM ::
+  LocalName -> OpenTerm -> (OpenTerm -> OpenTermM OpenTerm) ->
+  OpenTermM OpenTerm
 piOpenTermM x tp body_f =
   fst <$> piOpenTermAuxM x tp (body_f >=> (\t -> return (t, ())))
 
 -- | Build a lambda abstraction with an auxiliary return value in the
 -- 'OpenTermM' monad
-lambdaOpenTermAuxM :: String -> OpenTerm ->
-                      (OpenTerm -> OpenTermM (OpenTerm, a)) ->
-                      OpenTermM (OpenTerm, a)
+lambdaOpenTermAuxM ::
+  LocalName -> OpenTerm ->
+  (OpenTerm -> OpenTermM (OpenTerm, a)) ->
+  OpenTermM (OpenTerm, a)
 lambdaOpenTermAuxM x tp body_f =
   do (tp', body, a) <- bindOpenTermAuxM x tp body_f
      return (OpenTerm (typeInferComplete $ Lambda x tp' body), a)
 
 -- | Build a pi abstraction with an auxiliary return value in the 'OpenTermM'
 -- monad
-piOpenTermAuxM :: String -> OpenTerm -> (OpenTerm -> OpenTermM (OpenTerm, a)) ->
-                  OpenTermM (OpenTerm, a)
+piOpenTermAuxM ::
+  LocalName -> OpenTerm -> (OpenTerm -> OpenTermM (OpenTerm, a)) ->
+  OpenTermM (OpenTerm, a)
 piOpenTermAuxM x tp body_f =
   do (tp', body, a) <- bindOpenTermAuxM x tp body_f
      return (OpenTerm (typeInferComplete $ Pi x tp' body), a)

saw-core/src/Verifier/SAW/Recognizer.hs

@@ -290,22 +290,22 @@ asUnsignedConcreteBv term = do
 asStringLit :: Recognizer Term String
 asStringLit t = do StringLit i <- asFTermF t; return i
 
-asLambda :: Recognizer Term (String, Term, Term)
+asLambda :: Recognizer Term (LocalName, Term, Term)
 asLambda (unwrapTermF -> Lambda s ty body) = return (s, ty, body)
 asLambda _ = Nothing
 
-asLambdaList :: Term -> ([(String, Term)], Term)
+asLambdaList :: Term -> ([(LocalName, Term)], Term)
 asLambdaList = go []
   where go r (asLambda -> Just (nm,tp,rhs)) = go ((nm,tp):r) rhs
         go r rhs = (reverse r, rhs)
 
-asPi :: Recognizer Term (String, Term, Term)
+asPi :: Recognizer Term (LocalName, Term, Term)
 asPi (unwrapTermF -> Pi nm tp body) = return (nm, tp, body)
 asPi _ = Nothing
 
 -- | Decomposes a term into a list of pi bindings, followed by a right
 -- term that is not a pi binding.
-asPiList :: Term -> ([(String, Term)], Term)
+asPiList :: Term -> ([(LocalName, Term)], Term)
 asPiList = go []
   where go r (asPi -> Just (nm,tp,rhs)) = go ((nm,tp):r) rhs
         go r rhs = (reverse r, rhs)

saw-core/src/Verifier/SAW/Rewriter.hs

@@ -68,6 +68,7 @@ import qualified Data.List as List
 import qualified Data.Map as Map
 import Data.Set (Set)
 import qualified Data.Set as Set
+import qualified Data.Text as Text
 import Control.Monad.Trans.Writer.Strict
 import Numeric.Natural
 
@@ -205,7 +206,7 @@ scMatch sc pat term =
               | j < depth -> go (j : js) t
             _ -> Nothing
 
-    match :: Int -> [(String, Term)] -> Term -> Term -> MatchState -> MaybeT IO MatchState
+    match :: Int -> [(LocalName, Term)] -> Term -> Term -> MatchState -> MaybeT IO MatchState
     match _ _ (STApp i fv _) (STApp j _ _) s
       | fv == emptyBitSet && i == j = return s
     match depth env x y s@(MatchState m cs) =
@@ -221,7 +222,7 @@ scMatch sc pat term =
              let fvy = looseVars y `intersectBitSets` (completeBitSet depth)
              guard (fvy `unionBitSets` fvj == fvj)
              let fixVar t (nm, ty) =
-                   do v <- scFreshGlobal sc nm ty
+                   do v <- scFreshGlobal sc (Text.unpack nm) ty
                       let Just ec = R.asExtCns v
                       t' <- instantiateVar sc 0 v t
                       return (t', ec)
@@ -481,7 +482,7 @@ listRules ss = [ r | Left r <- Net.content ss ]
 ----------------------------------------------------------------------
 -- Destructors for terms
 
-asBetaRedex :: R.Recognizer Term (String, Term, Term, Term)
+asBetaRedex :: R.Recognizer Term (LocalName, Term, Term, Term)
 asBetaRedex t =
     do (f, arg) <- R.asApp t
        (s, ty, body) <- R.asLambda f
@@ -821,7 +822,7 @@ doHoistIfs sc ss hoistCache itePat = go
        goF _ (Pi nm tp body) = goBinder scPi nm tp body
 
        goBinder close nm tp body = do
-           (ec, body') <- scOpenTerm sc nm tp 0 body
+           (ec, body') <- scOpenTerm sc (Text.unpack nm) tp 0 body
            (body'', conds) <- go body'
            let (stuck, float) = List.partition (\(_,ecs) -> Set.member ec ecs) conds