Merge pull request #1272 from GaloisInc/issue1263

Avoid concatenating Text values in `termToPat`.
GaloisInc · Sep 15, 2021 · 58ca144 · 58ca144
2 parents 337ca6c + 1c74cf4
commit 58ca144
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/saw-core/src/Verifier/SAW/Conversion.hs b/saw-core/src/Verifier/SAW/Conversion.hs
@@ -205,7 +205,7 @@ resolveArgs (Matcher p m) (defaultArgsMatcher -> args@(ArgsMatcher pl _)) =
 
 -- | Match a global definition.
 asGlobalDef :: Ident -> Matcher ()
-asGlobalDef ident = Matcher (Net.Atom (identText ident)) f
+asGlobalDef ident = Matcher (Net.Atom (identBaseName ident)) f
   where f (R.asGlobalDef -> Just o) | ident == o = return ()
         f _ = Nothing
 
@@ -262,15 +262,15 @@ asRecordSelector m = asVar $ \t -> _1 (runMatcher m) =<< R.asRecordSelector t
 
 -- | Match a constructor
 asCtor :: ArgsMatchable v a => Ident -> v a -> Matcher a
-asCtor o = resolveArgs $ Matcher (Net.Atom (identText o)) match
+asCtor o = resolveArgs $ Matcher (Net.Atom (identBaseName o)) match
   where match t = do
           CtorApp c params l <- R.asFTermF t
           guard (o == primName c)
           return (params ++ l)
 
 -- | Match a datatype.
 asDataType :: ArgsMatchable v a => PrimName a -> v a -> Matcher a
-asDataType o = resolveArgs $ Matcher (Net.Atom (identText (primName o))) match
+asDataType o = resolveArgs $ Matcher (Net.Atom (identBaseName (primName o))) match
   where match t = do
           DataTypeApp dt params l <- R.asFTermF t
           guard (primVarIndex dt == primVarIndex o)

diff --git a/saw-core/src/Verifier/SAW/Term/Functor.hs b/saw-core/src/Verifier/SAW/Term/Functor.hs
@@ -401,15 +401,15 @@ instance Net.Pattern Term where
 termToPat :: Term -> Net.Pat
 termToPat t =
     case unwrapTermF t of
-      Constant ec _             -> Net.Atom (toAbsoluteName (ecName ec))
+      Constant ec _             -> Net.Atom (toShortName (ecName ec))
       App t1 t2                 -> Net.App (termToPat t1) (termToPat t2)
-      FTermF (Primitive pn)     -> Net.Atom (identText (primName pn))
+      FTermF (Primitive pn)     -> Net.Atom (identBaseName (primName pn))
       FTermF (Sort s)           -> Net.Atom (Text.pack ('*' : show s))
       FTermF (NatLit _)         -> Net.Var
       FTermF (DataTypeApp c ps ts) ->
-        foldl Net.App (Net.Atom (identText (primName c))) (map termToPat (ps ++ ts))
+        foldl Net.App (Net.Atom (identBaseName (primName c))) (map termToPat (ps ++ ts))
       FTermF (CtorApp c ps ts)   ->
-        foldl Net.App (Net.Atom (identText (primName c))) (map termToPat (ps ++ ts))
+        foldl Net.App (Net.Atom (identBaseName (primName c))) (map termToPat (ps ++ ts))
       _                         -> Net.Var
 
 unwrapTermF :: Term -> TermF Term