Do bound variables need annotations?

The annotation mechanism (annotateTerm) attaches Nonces to expressions via the Annotation constructor of NonceApp. Bound variables already have associated Nonces, their bvarIds. We should consider whether annotateTerm, when applied to a BoundExpr, should return the term as-is, and getAnnotation could just return the bvarId.

Yes, this seems wise. We already do something similar for NonceAppExprs here:

what4/what4/src/What4/Expr/Builder.hs

Lines 1640 to 1643 in 076f49b

    
           getAnnotation _sym e = 
        
             case e of 
        
               NonceAppExpr (nonceExprApp -> Annotation _ n _) -> Just n 
        
               _ -> Nothing

We already do something similar for NonceAppExprs here:

I'm not sure this is analogous, actually - that case seems to be for Annotation expressions, which are explicitly annotated (unlike BoundVarExprs, which are kind of "implicitly" annotated by virtue of already having a Nonce). However, we could probably special-case NonceAppExpr more generally in the same way - see #246.

	getAnnotation _sym e =
	case e of
	NonceAppExpr (nonceExprApp -> Annotation _ n _) -> Just n
	_ -> Nothing