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