From 333c2a0063ee9556f9f0c67cadf6caae9b21c01f Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Sun, 17 Jan 2021 09:10:09 -0800 Subject: [PATCH] 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 | 31 ++++++++-------- .../src/Verifier/SAW/Simulator/BitBlast.hs | 2 +- .../src/Verifier/SAW/Simulator/SBV.hs | 2 +- .../src/Verifier/SAW/Simulator/What4.hs | 4 +-- saw-core/src/Verifier/SAW/ExternalFormat.hs | 8 ++--- saw-core/src/Verifier/SAW/Module.hs | 4 +-- saw-core/src/Verifier/SAW/OpenTerm.hs | 35 +++++++++++-------- saw-core/src/Verifier/SAW/Recognizer.hs | 8 ++--- saw-core/src/Verifier/SAW/Rewriter.hs | 9 ++--- saw-core/src/Verifier/SAW/SCTypeCheck.hs | 31 ++++++++-------- saw-core/src/Verifier/SAW/SharedTerm.hs | 16 ++++----- saw-core/src/Verifier/SAW/Term/CtxTerm.hs | 20 ++++++----- saw-core/src/Verifier/SAW/Term/Functor.hs | 6 ++-- saw-core/src/Verifier/SAW/Term/Pretty.hs | 31 ++++++++-------- saw-core/src/Verifier/SAW/Typechecker.hs | 18 +++++----- saw-core/src/Verifier/SAW/TypedAST.hs | 1 + saw-core/src/Verifier/SAW/UntypedAST.hs | 8 +++++ 17 files changed, 129 insertions(+), 105 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 40a3f263..366d8116 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/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,15 +294,14 @@ 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 @@ -310,7 +309,7 @@ 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,7 +957,7 @@ 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) @@ -966,7 +965,7 @@ importExpr' sc env schema expr = 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) diff --git a/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs b/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs index bc3ca88a..6685290e 100644 --- a/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs +++ b/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 [] diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs index 5ddcdf59..85d515c2 100644 --- a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs +++ b/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) diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index c33751c7..81fffe3f 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/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 "") diff --git a/saw-core/src/Verifier/SAW/ExternalFormat.hs b/saw-core/src/Verifier/SAW/ExternalFormat.hs index 2455dbe0..ba0d380c 100644 --- a/saw-core/src/Verifier/SAW/ExternalFormat.hs +++ b/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)) diff --git a/saw-core/src/Verifier/SAW/Module.hs b/saw-core/src/Verifier/SAW/Module.hs index 982308ba..ae1d815e 100644 --- a/saw-core/src/Verifier/SAW/Module.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/OpenTerm.hs b/saw-core/src/Verifier/SAW/OpenTerm.hs index ef9997fe..ce5fd273 100644 --- a/saw-core/src/Verifier/SAW/OpenTerm.hs +++ b/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) diff --git a/saw-core/src/Verifier/SAW/Recognizer.hs b/saw-core/src/Verifier/SAW/Recognizer.hs index 8190f949..d49c6ae1 100644 --- a/saw-core/src/Verifier/SAW/Recognizer.hs +++ b/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) diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs index e2dc6165..981d483a 100644 --- a/saw-core/src/Verifier/SAW/Rewriter.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/SCTypeCheck.hs b/saw-core/src/Verifier/SAW/SCTypeCheck.hs index c90bba7e..a74326fd 100644 --- a/saw-core/src/Verifier/SAW/SCTypeCheck.hs +++ b/saw-core/src/Verifier/SAW/SCTypeCheck.hs @@ -76,18 +76,19 @@ type TCState = Map TermIndex Term -- -- * Can throw 'TCError's type TCM a = - ReaderT (SharedContext, Maybe ModuleName, [(String,Term)]) + ReaderT (SharedContext, Maybe ModuleName, [(LocalName, Term)]) (StateT TCState (ExceptT TCError IO)) a -- | Run a type-checking computation in a given context, starting from the empty -- memoization table -runTCM :: TCM a -> SharedContext -> Maybe ModuleName -> [(String,Term)] -> - IO (Either TCError a) +runTCM :: + TCM a -> SharedContext -> Maybe ModuleName -> [(LocalName, Term)] -> + IO (Either TCError a) runTCM m sc mnm ctx = runExceptT $ evalStateT (runReaderT m (sc, mnm, ctx)) Map.empty -- | Read the current typing context -askCtx :: TCM [(String,Term)] +askCtx :: TCM [(LocalName, Term)] askCtx = (\(_,_,ctx) -> ctx) <$> ask -- | Read the current module name @@ -101,7 +102,7 @@ askModName = (\(_,mnm,_) -> mnm) <$> ask -- -- NOTE: the type given for the variable should be in WHNF, so that we do not -- have to normalize the types of variables each time we see them. -withVar :: String -> Term -> TCM a -> TCM a +withVar :: LocalName -> Term -> TCM a -> TCM a withVar x tp m = flip catchError (throwError . ErrorCtx x tp) $ do saved_table <- get @@ -112,7 +113,7 @@ withVar x tp m = -- | Run a type-checking computation in a typing context extended by a list of -- variables and their types. See 'withVar'. -withCtx :: [(String,Term)] -> TCM a -> TCM a +withCtx :: [(LocalName, Term)] -> TCM a -> TCM a withCtx = flip (foldr (\(x,tp) -> withVar x tp)) @@ -159,13 +160,13 @@ data TCError | MalformedRecursor Term String | DeclError String String | ErrorPos Pos TCError - | ErrorCtx String Term TCError + | ErrorCtx LocalName Term TCError -- | Throw a type-checking error throwTCError :: TCError -> TCM a throwTCError = throwError -type PPErrM = Reader ([String], Maybe Pos) +type PPErrM = Reader ([LocalName], Maybe Pos) -- | Pretty-print a type-checking error prettyTCError :: TCError -> [String] @@ -256,8 +257,9 @@ scTypeCheck sc mnm = scTypeCheckInCtx sc mnm [] -- | Like 'scTypeCheck', but type-check the term relative to a typing context, -- which assigns types to free variables in the term -scTypeCheckInCtx :: TypeInfer a => SharedContext -> Maybe ModuleName -> - [(String,Term)] -> a -> IO (Either TCError Term) +scTypeCheckInCtx :: + TypeInfer a => SharedContext -> Maybe ModuleName -> + [(LocalName, Term)] -> a -> IO (Either TCError Term) scTypeCheckInCtx sc mnm ctx t0 = runTCM (typeInfer t0) sc mnm ctx -- | A pair of a 'Term' and its type @@ -285,9 +287,9 @@ typeInferCompleteWHNF a = -- while @a@ is the type of types. This will give us 'Term's for each type, as -- well as their 'Sort's, since the type of any type is a 'Sort'. class TypeInferCtx var a where - typeInferCompleteCtx :: [(var,a)] -> TCM [(String, Term, Sort)] + typeInferCompleteCtx :: [(var,a)] -> TCM [(LocalName, Term, Sort)] -instance TypeInfer a => TypeInferCtx String a where +instance TypeInfer a => TypeInferCtx LocalName a where typeInferCompleteCtx [] = return [] typeInferCompleteCtx ((x,tp):ctx) = do typed_tp <- typeInferComplete tp @@ -298,8 +300,9 @@ instance TypeInfer a => TypeInferCtx String a where -- | Perform type inference on a context via 'typeInferCompleteCtx', and then -- run a computation in that context via 'withCtx', also passing in that context -- to the computation -typeInferCompleteInCtx :: TypeInferCtx var tp => [(var, tp)] -> - ([(String,Term,Sort)] -> TCM a) -> TCM a +typeInferCompleteInCtx :: + TypeInferCtx var tp => [(var, tp)] -> + ([(LocalName, Term, Sort)] -> TCM a) -> TCM a typeInferCompleteInCtx ctx f = do typed_ctx <- typeInferCompleteCtx ctx withCtx (map (\(x,tp,_) -> (x,tp)) typed_ctx) (f typed_ctx) diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs index b08a4a4a..aee7241c 100644 --- a/saw-core/src/Verifier/SAW/SharedTerm.hs +++ b/saw-core/src/Verifier/SAW/SharedTerm.hs @@ -1360,7 +1360,7 @@ scFunAll sc argTypes resultType = foldrM (scFun sc) resultType argTypes -- (as a 'Term'), and a body. Regarding deBruijn indices, in the body of the -- function, an index of 0 refers to the bound parameter. scLambda :: SharedContext - -> String -- ^ The parameter name + -> LocalName -- ^ The parameter name -> Term -- ^ The parameter type -> Term -- ^ The body -> IO Term @@ -1372,7 +1372,7 @@ scLambda sc varname ty body = scTermF sc (Lambda varname ty body) -- parameter in the list, and n-1 (where n is the list length) refers to the -- first. scLambdaList :: SharedContext - -> [(String, Term)] -- ^ List of parameter / parameter type pairs + -> [(LocalName, Term)] -- ^ List of parameter / parameter type pairs -> Term -- ^ The body -> IO Term scLambdaList _ [] rhs = return rhs @@ -1383,7 +1383,7 @@ scLambdaList sc ((nm,tp):r) rhs = -- type (as a 'Term'), and a body. This function follows the same deBruijn -- index convention as 'scLambda'. scPi :: SharedContext - -> String -- ^ The parameter name + -> LocalName -- ^ The parameter name -> Term -- ^ The parameter type -> Term -- ^ The body -> IO Term @@ -1393,7 +1393,7 @@ scPi sc nm tp body = scTermF sc (Pi nm tp body) -- from a list associating parameter names to types (as 'Term's) and a body. -- This function follows the same deBruijn index convention as 'scLambdaList'. scPiList :: SharedContext - -> [(String, Term)] -- ^ List of parameter / parameter type pairs + -> [(LocalName, Term)] -- ^ List of parameter / parameter type pairs -> Term -- ^ The body -> IO Term scPiList _ [] rhs = return rhs @@ -2274,7 +2274,7 @@ scExtsToLocals sc exts x = instantiateVars sc fn 0 x scAbstractExts :: SharedContext -> [ExtCns Term] -> Term -> IO Term scAbstractExts _ [] x = return x scAbstractExts sc exts x = - do let lams = [ (Text.unpack (toShortName (ecName ec)), ecType ec) | ec <- exts ] + do let lams = [ (toShortName (ecName ec), ecType ec) | ec <- exts ] scLambdaList sc lams =<< scExtsToLocals sc exts x -- | Generalize over the given list of external constants by wrapping @@ -2283,7 +2283,7 @@ scAbstractExts sc exts x = scGeneralizeExts :: SharedContext -> [ExtCns Term] -> Term -> IO Term scGeneralizeExts _ [] x = return x scGeneralizeExts sc exts x = - do let pis = [ (Text.unpack (toShortName (ecName ec)), ecType ec) | ec <- exts ] + do let pis = [ (toShortName (ecName ec), ecType ec) | ec <- exts ] scPiList sc pis =<< scExtsToLocals sc exts x scUnfoldConstants :: SharedContext -> [VarIndex] -> Term -> IO Term @@ -2383,7 +2383,7 @@ scOpenTerm sc nm tp idx body = do -- | `closeTerm closer sc ec body` replaces the external constant `ec` in `body` by -- a new deBruijn variable and binds it using the binding form given by 'close'. -- The name and type of the new bound variable are given by the name and type of `ec`. -scCloseTerm :: (SharedContext -> String -> Term -> Term -> IO Term) +scCloseTerm :: (SharedContext -> LocalName -> Term -> Term -> IO Term) -> SharedContext -> ExtCns Term -> Term @@ -2391,4 +2391,4 @@ scCloseTerm :: (SharedContext -> String -> Term -> Term -> IO Term) scCloseTerm close sc ec body = do lv <- scLocalVar sc 0 body' <- scInstantiateExt sc (Map.insert (ecVarIndex ec) lv Map.empty) =<< incVars sc 0 1 body - close sc (Text.unpack (toShortName (ecName ec))) (ecType ec) body' + close sc (toShortName (ecName ec)) (ecType ec) body' diff --git a/saw-core/src/Verifier/SAW/Term/CtxTerm.hs b/saw-core/src/Verifier/SAW/Term/CtxTerm.hs index 2427c56c..a08dd684 100644 --- a/saw-core/src/Verifier/SAW/Term/CtxTerm.hs +++ b/saw-core/src/Verifier/SAW/Term/CtxTerm.hs @@ -25,6 +25,7 @@ right when you finally get GHC to accept your code. :) {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} @@ -118,7 +119,7 @@ type CtxInv as = CtxInvApp EmptyCtx as -- and just write "represent" in quotes. data Bindings (tp :: Ctx Type -> Type -> Type) (ctx :: Ctx Type) (as :: [Type]) where NoBind :: Bindings tp ctx '[] - Bind :: String -> tp ctx (Typ a) -> Bindings tp (ctx ::> a) as -> + Bind :: LocalName -> tp ctx (Typ a) -> Bindings tp (ctx ::> a) as -> Bindings tp ctx (a ': as) -- | Compute the number of bindings in a bindings list @@ -129,7 +130,7 @@ bindingsLength (Bind _ _ bs) = 1 + bindingsLength bs -- | An inverted list of bindings, seen from the "inside out" data InvBindings (tp :: Ctx Type -> Type -> Type) (ctx :: Ctx Type) (as :: Ctx Type) where InvNoBind :: InvBindings tp ctx EmptyCtx - InvBind :: InvBindings tp ctx as -> String -> tp (ctx <+> as) (Typ a) -> + InvBind :: InvBindings tp ctx as -> LocalName -> tp (ctx <+> as) (Typ a) -> InvBindings tp ctx (as ::> a) -- | Compute the number of bindings in an inverted bindings list @@ -251,7 +252,7 @@ data ExistsTp tp ctx = forall a. ExistsTp (tp ctx a) -- the Haskell type system is not powerful enough to represent all the SAW types -- anyway, and any code that consumes this 'Bindings' list cannot know that -- anyway. See also the comments for 'CtxTerm'. -ctxBindingsOfTerms :: [(String,Term)] -> ExistsTp (Bindings CtxTerm) ctx +ctxBindingsOfTerms :: [(LocalName, Term)] -> ExistsTp (Bindings CtxTerm) ctx ctxBindingsOfTerms [] = ExistsTp NoBind ctxBindingsOfTerms ((x,tp):ctx) = case ctxBindingsOfTerms ctx of @@ -423,7 +424,7 @@ ctxApplyMulti fm argsm = helper f' args -- | Form a lambda-abstraction as a 'CtxTerm' -ctxLambda1 :: MonadTerm m => String -> CtxTerm ctx (Typ a) -> +ctxLambda1 :: MonadTerm m => LocalName -> CtxTerm ctx (Typ a) -> (CtxTerm (ctx ::> a) a -> m (CtxTerm (ctx ::> a) b)) -> m (CtxTerm ctx (a -> b)) ctxLambda1 x (CtxTerm tp) body_f = @@ -444,7 +445,7 @@ ctxLambda (Bind x tp xs) body_f = body_f (CtxTermsCons var vars) -- | Form a pi-abstraction as a 'CtxTerm' -ctxPi1 :: MonadTerm m => String -> CtxTerm ctx (Typ a) -> +ctxPi1 :: MonadTerm m => LocalName -> CtxTerm ctx (Typ a) -> (CtxTerm (ctx ::> a) a -> m (CtxTerm (ctx ::> a) (Typ b))) -> m (CtxTerm ctx (Typ (a -> b))) @@ -476,7 +477,7 @@ ctxPiProxy _ = ctxPi -- | Existential return type of 'ctxAsPi' data CtxPi ctx = forall b c. - CtxPi String (CtxTerm ctx (Typ b)) (CtxTerm (ctx ::> b) (Typ c)) + CtxPi LocalName (CtxTerm ctx (Typ b)) (CtxTerm (ctx ::> b) (Typ c)) -- | Test if a 'CtxTerm' is a pi-abstraction, returning its components if so. -- Note that we are not returning any equality constraints on the input type, @@ -758,8 +759,9 @@ ctxPRetTp (_ :: Proxy (Typ a)) (d :: DataIdent d) params ixs s = -- | Like 'ctxPRetTp', but also take in a list of parameters and substitute them -- for the parameter variables returned by that function -mkPRetTp :: MonadTerm m => Ident -> [(String,Term)] -> [(String,Term)] -> - [Term] -> Sort -> m Term +mkPRetTp :: + MonadTerm m => Ident -> [(LocalName, Term)] -> [(LocalName, Term)] -> + [Term] -> Sort -> m Term mkPRetTp d untyped_p_ctx untyped_ix_ctx untyped_params s = case ctxBindingsOfTerms untyped_p_ctx of ExistsTp p_ctx -> @@ -1082,7 +1084,7 @@ asCtorArg _ _ _ _ _ = Nothing -- | Existential return type of 'asPiCtorArg' data CtxPiCtorArg d ixs ctx = forall a b . - CtxPiCtorArg String (CtorArg d ixs ctx (Typ a)) + CtxPiCtorArg LocalName (CtorArg d ixs ctx (Typ a)) (CtxTerm (ctx ::> a) (Typ b)) -- | Check that a constructor type is a pi-abstraction that takes as input an diff --git a/saw-core/src/Verifier/SAW/Term/Functor.hs b/saw-core/src/Verifier/SAW/Term/Functor.hs index c4c7224c..6599c290 100644 --- a/saw-core/src/Verifier/SAW/Term/Functor.hs +++ b/saw-core/src/Verifier/SAW/Term/Functor.hs @@ -34,6 +34,7 @@ module Verifier.SAW.Term.Functor -- * Data types and definitions , DeBruijnIndex , FieldName + , LocalName , ExtCns(..) , VarIndex , NameInfo(..) @@ -89,6 +90,7 @@ import Verifier.SAW.Utils (internalError) type DeBruijnIndex = Int type FieldName = Text +type LocalName = Text instance (Hashable k, Hashable a) => Hashable (Map k a) where hashWithSalt x m = hashWithSalt x (Map.assocs m) @@ -409,9 +411,9 @@ data TermF e -- ^ The atomic, or builtin, term constructs | App !e !e -- ^ Applications of functions - | Lambda !String !e !e + | Lambda !LocalName !e !e -- ^ Function abstractions - | Pi !String !e !e + | Pi !LocalName !e !e -- ^ The type of a (possibly) dependent function | LocalVar !DeBruijnIndex -- ^ Local variables are referenced by deBruijn index. diff --git a/saw-core/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs index 20d94950..eb82d4df 100644 --- a/saw-core/src/Verifier/SAW/Term/Pretty.hs +++ b/saw-core/src/Verifier/SAW/Term/Pretty.hs @@ -43,6 +43,7 @@ import Control.Monad.State.Strict as State import Data.Foldable (Foldable) #endif import qualified Data.Foldable as Fold +import qualified Data.Text as Text import qualified Data.Text.Lazy as Text.Lazy import qualified Data.Vector as V import Numeric (showIntAtBase) @@ -154,7 +155,7 @@ ppParensPrec p1 p2 d -- | Local variable namings, which map each deBruijn index in scope to a unique -- string to be used to print it. This mapping is given by position in a list. -newtype VarNaming = VarNaming [String] +newtype VarNaming = VarNaming [LocalName] -- | The empty local variable context emptyVarNaming :: VarNaming @@ -162,24 +163,24 @@ emptyVarNaming = VarNaming [] -- | Look up a string to use for a variable, if the first argument is 'True', or -- just print the variable number if the first argument is 'False' -lookupVarName :: Bool -> VarNaming -> DeBruijnIndex -> String +lookupVarName :: Bool -> VarNaming -> DeBruijnIndex -> LocalName lookupVarName True (VarNaming names) i - | i >= length names = '!' : show (i - length names) + | i >= length names = Text.pack ('!' : show (i - length names)) lookupVarName True (VarNaming names) i = names!!i -lookupVarName False _ i = '!' : show i +lookupVarName False _ i = Text.pack ('!' : show i) -- | Generate a fresh name from a base name that does not clash with any names -- already in a given list, unless it is "_", in which case return it as is -freshName :: [String] -> String -> String +freshName :: [LocalName] -> LocalName -> LocalName freshName used name | name == "_" = name - | elem name used = freshName used (name ++ "'") + | elem name used = freshName used (name <> "'") | otherwise = name -- | Add a new variable with the given base name to the local variable list, -- returning both the fresh name actually used and the new variable list. As a -- special case, if the base name is "_", it is not modified. -consVarNaming :: VarNaming -> String -> (String, VarNaming) +consVarNaming :: VarNaming -> LocalName -> (LocalName, VarNaming) consVarNaming (VarNaming names) name = let nm = freshName names name in (nm, VarNaming (nm : names)) @@ -231,7 +232,7 @@ instance MonadReader PPState PPM where local f (PPM m) = PPM $ local f m -- | Look up the given local variable by deBruijn index to get its name -varLookupM :: DeBruijnIndex -> PPM String +varLookupM :: DeBruijnIndex -> PPM LocalName varLookupM idx = lookupVarName <$> (ppShowLocalNames <$> ppOpts <$> ask) <*> (ppNaming <$> ask) <*> return idx @@ -261,7 +262,7 @@ atNextDepthM dflt m = -- also erasing the local memoization table (which is no longer valid in an -- extended variable context) during that computation. Return the result of the -- computation and also the name that was actually used for the bound variable. -withBoundVarM :: String -> PPM a -> PPM (String, a) +withBoundVarM :: LocalName -> PPM a -> PPM (LocalName, a) withBoundVarM basename m = do st <- ask let (var, naming) = consVarNaming (ppNaming st) basename @@ -369,14 +370,14 @@ ppArrayValue = list -- | Pretty-print a lambda abstraction as @\(x :: tp) -> body@, where the -- variable name to use for @x@ is bundled with @body@ -ppLambda :: SawDoc -> (String, SawDoc) -> SawDoc +ppLambda :: SawDoc -> (LocalName, SawDoc) -> SawDoc ppLambda tp (name, body) = group $ hang 2 $ vsep ["\\" <> parens (ppTypeConstraint (pretty name) tp) <+> "->", body] -- | Pretty-print a pi abstraction as @(x :: tp) -> body@, or as @tp -> body@ if -- @x == "_"@ -ppPi :: SawDoc -> (String, SawDoc) -> SawDoc +ppPi :: SawDoc -> (LocalName, SawDoc) -> SawDoc ppPi tp (name, body) = vsep [lhs, "->" <+> body] where lhs = if name == "_" then tp else parens (ppTypeConstraint (pretty name) tp) @@ -585,7 +586,7 @@ ppTermWithMemoTable prec global_p trm = ppLets occ_map_elems [] where -- -- Also, pretty-print let-bindings around the term for all subterms that occur -- more than once at the same binding level. -ppTermInBinder :: Prec -> String -> Term -> PPM (String, SawDoc) +ppTermInBinder :: Prec -> LocalName -> Term -> PPM (LocalName, SawDoc) ppTermInBinder prec basename trm = let nm = if basename == "_" && inBitSet 0 (looseVars trm) then "_x" else basename in @@ -596,7 +597,7 @@ ppTermInBinder prec basename trm = -- pretty-printing of the context. Note: we do not use any local memoization -- tables for the inner computation; the justification is that this function is -- only used for printing datatypes, which we assume are not very big. -ppWithBoundCtx :: [(String, Term)] -> PPM a -> PPM (SawDoc, a) +ppWithBoundCtx :: [(LocalName, Term)] -> PPM a -> PPM (SawDoc, a) ppWithBoundCtx [] m = (mempty ,) <$> m ppWithBoundCtx ((x,tp):ctx) m = (\tp_d (x', (ctx_d, ret)) -> @@ -626,7 +627,7 @@ scPrettyTerm opts t = -- | Like 'scPrettyTerm', but also supply a context of bound names, where the -- most recently-bound variable is listed first in the context -scPrettyTermInCtx :: PPOpts -> [String] -> Term -> String +scPrettyTermInCtx :: PPOpts -> [LocalName] -> Term -> String scPrettyTermInCtx opts ctx trm = renderSawDoc opts $ runPPM opts $ @@ -649,7 +650,7 @@ showTerm t = scPrettyTerm defaultPPOpts t data PPModule = PPModule [ModuleName] [PPDecl] data PPDecl - = PPTypeDecl Ident [(String,Term)] [(String,Term)] Sort [(Ident,Term)] + = PPTypeDecl Ident [(LocalName, Term)] [(LocalName, Term)] Sort [(Ident, Term)] | PPDefDecl Ident Term (Maybe Term) -- | Pretty-print a 'PPModule' diff --git a/saw-core/src/Verifier/SAW/Typechecker.hs b/saw-core/src/Verifier/SAW/Typechecker.hs index b0439fe8..de4dc059 100644 --- a/saw-core/src/Verifier/SAW/Typechecker.hs +++ b/saw-core/src/Verifier/SAW/Typechecker.hs @@ -35,6 +35,7 @@ import Control.Applicative #endif import Control.Monad.State import Data.List (findIndex) +import qualified Data.Text as Text import qualified Data.Vector as V import Prettyprinter hiding (Doc) @@ -61,8 +62,9 @@ inferCompleteTerm sc mnm t = inferCompleteTermCtx sc mnm [] t -- | Infer the type of an untyped term and complete it to a 'Term' in a given -- typing context -inferCompleteTermCtx :: SharedContext -> Maybe ModuleName -> [(String,Term)] -> - Un.Term -> IO (Either SawDoc Term) +inferCompleteTermCtx :: + SharedContext -> Maybe ModuleName -> [(LocalName, Term)] -> + Un.Term -> IO (Either SawDoc Term) inferCompleteTermCtx sc mnm ctx t = do res <- runTCM (typeInferComplete t) sc mnm ctx case res of @@ -95,7 +97,7 @@ inferResolveNameApp :: String -> [TypedTerm] -> TCM TypedTerm inferResolveNameApp n args = do ctx <- askCtx m <- getModule - case (findIndex ((== n) . fst) ctx, resolveName m n) of + case (findIndex ((== Text.pack n) . fst) ctx, resolveName m n) of (Just i, _) -> do t <- typeInferComplete (LocalVar i :: TermF TypedTerm) inferApplyAll t args @@ -201,7 +203,7 @@ typeInferCompleteTerm (Un.App f arg) = (App <$> typeInferComplete f <*> typeInferComplete arg) >>= typeInferComplete typeInferCompleteTerm (Un.Lambda _ [] t) = typeInferComplete t -typeInferCompleteTerm (Un.Lambda p ((Un.termVarString -> x,tp):ctx) t) = +typeInferCompleteTerm (Un.Lambda p ((Un.termVarLocalName -> x, tp) : ctx) t) = do tp_trm <- typeInferCompleteWHNF tp -- Normalize (the Term value of) tp before putting it into the context. See -- the documentation for withVar. @@ -209,7 +211,7 @@ typeInferCompleteTerm (Un.Lambda p ((Un.termVarString -> x,tp):ctx) t) = typeInferComplete $ Un.Lambda p ctx t typeInferComplete (Lambda x tp_trm body) typeInferCompleteTerm (Un.Pi _ [] t) = typeInferComplete t -typeInferCompleteTerm (Un.Pi p ((Un.termVarString -> x,tp):ctx) t) = +typeInferCompleteTerm (Un.Pi p ((Un.termVarLocalName -> x, tp) : ctx) t) = do tp_trm <- typeInferComplete tp -- NOTE: we need the type of x to be normalized when we add it to the -- context in withVar, but we do not want to normalize this type in the @@ -281,7 +283,7 @@ typeInferCompleteTerm (Un.BadTerm _) = instance TypeInferCtx Un.TermVar Un.Term where typeInferCompleteCtx = - typeInferCompleteCtx . map (\(x,tp) -> (Un.termVarString x, tp)) + typeInferCompleteCtx . map (\(x,tp) -> (Un.termVarLocalName x, tp)) -- @@ -309,7 +311,7 @@ processDecls (Un.TypeDecl NoQualifier (PosPair p nm) tp : -- peeling off the pi-abstraction variables in the type annotation. Any -- remaining body of the pi-type is the required type for the def body. (ctx, req_body_tp) <- - case matchPiWithNames (map Un.termVarString vars) def_tp_whnf of + case matchPiWithNames (map Un.termVarLocalName vars) def_tp_whnf of Just x -> return x Nothing -> throwTCError $ @@ -445,7 +447,7 @@ tcInsertModule sc (Un.Module (PosPair _ mnm) imports decls) = do -- | Pattern match a nested pi-abstraction, like 'asPiList', but only match as -- far as the supplied list of variables, and use them as the new names -matchPiWithNames :: [String] -> Term -> Maybe ([(String,Term)],Term) +matchPiWithNames :: [LocalName] -> Term -> Maybe ([(LocalName, Term)], Term) matchPiWithNames [] tp = return ([], tp) matchPiWithNames (var:vars) (asPi -> Just (_, arg_tp, body_tp)) = do (ctx,body) <- matchPiWithNames vars body_tp diff --git a/saw-core/src/Verifier/SAW/TypedAST.hs b/saw-core/src/Verifier/SAW/TypedAST.hs index 87090724..f6290824 100644 --- a/saw-core/src/Verifier/SAW/TypedAST.hs +++ b/saw-core/src/Verifier/SAW/TypedAST.hs @@ -73,6 +73,7 @@ module Verifier.SAW.TypedAST , isIdent , DeBruijnIndex , FieldName + , LocalName , ExtCns(..) , VarIndex -- * Utility functions diff --git a/saw-core/src/Verifier/SAW/UntypedAST.hs b/saw-core/src/Verifier/SAW/UntypedAST.hs index f105b6ab..29356a3a 100644 --- a/saw-core/src/Verifier/SAW/UntypedAST.hs +++ b/saw-core/src/Verifier/SAW/UntypedAST.hs @@ -23,6 +23,7 @@ module Verifier.SAW.UntypedAST , Term(..) , TermVar(..) , termVarString + , termVarLocalName , TermCtx , asApp , asPiList @@ -44,6 +45,7 @@ module Verifier.SAW.UntypedAST #if !MIN_VERSION_base(4,8,0) import Control.Applicative ((<$>)) #endif +import qualified Data.Text as Text import qualified Language.Haskell.TH.Syntax as TH import Numeric.Natural @@ -53,6 +55,7 @@ import Verifier.SAW.TypedAST ( ModuleName, mkModuleName , Sort, mkSort, propSort, sortOf , FieldName, DefQualifier + , LocalName ) data Term @@ -93,6 +96,11 @@ termVarString :: TermVar -> String termVarString (TermVar (PosPair _ str)) = str termVarString (UnusedVar _) = "_" +-- | Return the 'LocalName' associated with a 'TermVar' +termVarLocalName :: TermVar -> LocalName +termVarLocalName (TermVar (PosPair _ str)) = Text.pack str +termVarLocalName (UnusedVar _) = Text.pack "_" + -- | A context of 0 or more variable bindings, with types type TermCtx = [(TermVar,Term)]