Update saw-core submodule to fix addsimp crash.

This patch includes PR GaloisInc/saw-core#112, which
implements error handling using the Maybe monad for
the creation of rewrite rules from equational theorems.

Fixes #319.

Author: Brian Huffman

deps/saw-core

@@ -1021,17 +1021,23 @@ beta_reduce_term (TypedTerm schema t) = do
   t' <- io $ betaNormalize sc t
   return (TypedTerm schema t')
 
-addsimp :: Theorem -> Simpset -> Simpset
-addsimp (Theorem (Prop t) _stats) ss = addRule (ruleOfProp t) ss
-
-addsimp' :: Term -> Simpset -> Simpset
-addsimp' t ss = addRule (ruleOfProp t) ss
-
-addsimps :: [Theorem] -> Simpset -> Simpset
-addsimps thms ss = foldr addsimp ss thms
-
-addsimps' :: [Term] -> Simpset -> Simpset
-addsimps' ts ss = foldr (\t -> addRule (ruleOfProp t)) ss ts
+addsimp :: Theorem -> Simpset -> TopLevel Simpset
+addsimp (Theorem (Prop t) _stats) ss =
+  case ruleOfProp t of
+    Nothing -> fail "addsimp: theorem not an equation"
+    Just rule -> pure (addRule rule ss)
+
+addsimp' :: Term -> Simpset -> TopLevel Simpset
+addsimp' t ss =
+  case ruleOfProp t of
+    Nothing -> fail "addsimp': theorem not an equation"
+    Just rule -> pure (addRule rule ss)
+
+addsimps :: [Theorem] -> Simpset -> TopLevel Simpset
+addsimps thms ss = foldM (flip addsimp) ss thms
+
+addsimps' :: [Term] -> Simpset -> TopLevel Simpset
+addsimps' ts ss = foldM (flip addsimp') ss ts
 
 print_type :: Term -> TopLevel ()
 print_type t = do

src/SAWScript/Builtins.hs

@@ -1427,22 +1427,22 @@ primitives = Map.fromList
     ]
 
   , prim "addsimp"             "Theorem -> Simpset -> Simpset"
-    (pureVal addsimp)
+    (funVal2 addsimp)
     Current
     [ "Add a proved equality theorem to a given simplification rule set." ]
 
   , prim "addsimp'"            "Term -> Simpset -> Simpset"
-    (pureVal addsimp')
+    (funVal2 addsimp')
     Current
     [ "Add an arbitrary equality term to a given simplification rule set." ]
 
   , prim "addsimps"            "[Theorem] -> Simpset -> Simpset"
-    (pureVal addsimps)
+    (funVal2 addsimps)
     Current
     [ "Add proved equality theorems to a given simplification rule set." ]
 
   , prim "addsimps'"           "[Term] -> Simpset -> Simpset"
-    (pureVal addsimps')
+    (funVal2 addsimps')
     Current
     [ "Add arbitrary equality terms to a given simplification rule set." ]