Make ruleOfProp return a Maybe instead of calling error.

This is to facilitate a fix for GaloisInc/saw-script#319.

saw-core/src/Verifier/SAW/Rewriter.hs

@@ -299,27 +299,30 @@ ruleOfTerm t =
 ruleOfTerms :: Term -> Term -> RewriteRule
 ruleOfTerms l r = RewriteRule { ctxt = [], lhs = l, rhs = r }
 
--- | Converts a parameterized equality predicate to a RewriteRule.
-ruleOfProp :: Term -> RewriteRule
+-- | Converts a parameterized equality predicate to a RewriteRule,
+-- returning 'Nothing' if the predicate is not an equation.
+ruleOfProp :: Term -> Maybe RewriteRule
 ruleOfProp (R.asPi -> Just (_, ty, body)) =
-  let rule = ruleOfProp body in rule { ctxt = ty : ctxt rule }
+  do rule <- ruleOfProp body
+     Just $ rule { ctxt = ty : ctxt rule }
 ruleOfProp (R.asLambda -> Just (_, ty, body)) =
-  let rule = ruleOfProp body in rule { ctxt = ty : ctxt rule }
+  do rule <- ruleOfProp body
+     Just $ rule { ctxt = ty : ctxt rule }
 ruleOfProp (R.asApplyAll -> (R.isGlobalDef eqIdent' -> Just (), [_, x, y])) =
-  RewriteRule { ctxt = [], lhs = x, rhs = y }
+  Just $ RewriteRule { ctxt = [], lhs = x, rhs = y }
 ruleOfProp (R.asApplyAll -> (R.isGlobalDef ecEqIdent -> Just (), [_, _, x, y])) =
-  RewriteRule { ctxt = [], lhs = x, rhs = y }
+  Just $ RewriteRule { ctxt = [], lhs = x, rhs = y }
 ruleOfProp (R.asApplyAll -> (R.isGlobalDef bvEqIdent -> Just (), [_, x, y])) =
-  RewriteRule { ctxt = [], lhs = x, rhs = y }
+  Just $ RewriteRule { ctxt = [], lhs = x, rhs = y }
 ruleOfProp (R.asApplyAll -> (R.isGlobalDef boolEqIdent -> Just (), [x, y])) =
-  RewriteRule { ctxt = [], lhs = x, rhs = y }
+  Just $ RewriteRule { ctxt = [], lhs = x, rhs = y }
 ruleOfProp (R.asApplyAll -> (R.isGlobalDef vecEqIdent -> Just (), [_, _, _, x, y])) =
-  RewriteRule { ctxt = [], lhs = x, rhs = y }
+  Just $ RewriteRule { ctxt = [], lhs = x, rhs = y }
 ruleOfProp (unwrapTermF -> Constant _ body) = ruleOfProp body
 ruleOfProp (R.asEq -> Just (_, x, y)) =
-  RewriteRule { ctxt = [], lhs = x, rhs = y }
+  Just $ RewriteRule { ctxt = [], lhs = x, rhs = y }
 ruleOfProp (R.asEqTrue -> Just body) = ruleOfProp body
-ruleOfProp t = error $ "ruleOfProp: Predicate not an equation: " ++ scPrettyTerm defaultPPOpts t
+ruleOfProp _ = Nothing
 
 -- | Generate a rewrite rule from the type of an identifier, using 'ruleOfTerm'
 scEqRewriteRule :: SharedContext -> Ident -> IO RewriteRule