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

@@ -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)

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