From 1c74cf4c10ec62d434e2600e5114e6940ea731a0 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Tue, 14 Sep 2021 15:22:39 -0700
Subject: [PATCH] Avoid concatenating Text values in `termToPat`.

Fixes #1263.

We now use `identBaseName` instead of `identText` in the `termToPat`
definition. While `identText` concatenates the module name and base
name, `identBaseName` just returns the base name directly.

Using only the base name means that there is a chance of name collisions
between constants that differ only by module name. However, term nets
are only used as an approximate filter prior to term matching; it is
not a problem if a few extra hits are returned from time to time.

Ultimately it might be better to replace the use of `Text` in the term
net `Atom` constructor with a more specialized key type; for example
with `ExtCns` names we could use the `VarIndex` for matching. However,
this would require modifying the term net library.
---
 saw-core/src/Verifier/SAW/Conversion.hs   | 6 +++---
 saw-core/src/Verifier/SAW/Term/Functor.hs | 8 ++++----
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/saw-core/src/Verifier/SAW/Conversion.hs b/saw-core/src/Verifier/SAW/Conversion.hs
index c5ca026625..f30c1cf74d 100644
--- 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,7 +262,7 @@ 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)
@@ -270,7 +270,7 @@ asCtor o = resolveArgs $ Matcher (Net.Atom (identText o)) match
 
 -- | 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
index 94e5de38c2..7d6361f9f7 100644
--- 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