From e46dff42096550d860d210bd9cf6e435d8cd7ce5 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 6 Dec 2023 11:14:09 -0500 Subject: [PATCH] Remove `getUnannotatedTerm` case for bound variables --- what4/src/What4/Expr/Builder.hs | 1 - what4/src/What4/Interface.hs | 3 ++- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs index 2118ce72..258562c9 100644 --- a/what4/src/What4/Expr/Builder.hs +++ b/what4/src/What4/Expr/Builder.hs @@ -1646,7 +1646,6 @@ instance IsExprBuilder (ExprBuilder t st fs) where getUnannotatedTerm _sym e = case e of - BoundVarExpr {} -> Just e NonceAppExpr (nonceExprApp -> Annotation _ _ x) -> Just x _ -> Nothing diff --git a/what4/src/What4/Interface.hs b/what4/src/What4/Interface.hs index a99c853d..a6e04a14 100644 --- a/what4/src/What4/Interface.hs +++ b/what4/src/What4/Interface.hs @@ -691,7 +691,8 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym), HashableF (BoundVar sym) getAnnotation :: sym -> SymExpr sym tp -> Maybe (SymAnnotation sym tp) -- | Project the original, unannotated term from an annotated term. - -- This returns 'Nothing' for terms that do not have annotations. + -- This returns 'Nothing' for terms that do not have annotations, + -- or for terms that cannot be separated from their annotations. getUnannotatedTerm :: sym -> SymExpr sym tp -> Maybe (SymExpr sym tp) ----------------------------------------------------------------------