diff --git a/saw-core/src/Verifier/SAW/Conversion.hs b/saw-core/src/Verifier/SAW/Conversion.hs index 8fbd8d74e4..cd7783b4b1 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 (c == o) @@ -270,7 +270,7 @@ asCtor o = resolveArgs $ Matcher (Net.Atom (identText o)) match -- | Match a datatype. asDataType :: ArgsMatchable v a => Ident -> v a -> Matcher a -asDataType o = resolveArgs $ Matcher (Net.Atom (identText o)) match +asDataType o = resolveArgs $ Matcher (Net.Atom (identBaseName o)) match where match t = do DataTypeApp dt params l <- R.asFTermF t guard (dt == o) diff --git a/saw-core/src/Verifier/SAW/Term/Functor.hs b/saw-core/src/Verifier/SAW/Term/Functor.hs index ec18bac5b2..d30113f6c4 100644 --- a/saw-core/src/Verifier/SAW/Term/Functor.hs +++ b/saw-core/src/Verifier/SAW/Term/Functor.hs @@ -344,15 +344,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 ec) -> Net.Atom (toAbsoluteName (ecName ec)) + FTermF (Primitive ec) -> Net.Atom (toShortName (ecName ec)) FTermF (Sort s) -> Net.Atom (Text.pack ('*' : show s)) FTermF (NatLit _) -> Net.Var FTermF (DataTypeApp c ps ts) -> - foldl Net.App (Net.Atom (identText c)) (map termToPat (ps ++ ts)) + foldl Net.App (Net.Atom (identBaseName c)) (map termToPat (ps ++ ts)) FTermF (CtorApp c ps ts) -> - foldl Net.App (Net.Atom (identText c)) (map termToPat (ps ++ ts)) + foldl Net.App (Net.Atom (identBaseName c)) (map termToPat (ps ++ ts)) _ -> Net.Var unwrapTermF :: Term -> TermF Term