upgrade to SBV 8

Language/Expression/Prop.hs

@@ -121,17 +121,17 @@ instance HFoldableAt Identity LogicOp where
     LogNot x -> not <$> x
     LogAnd x y -> liftA2 (&&) x y
     LogOr x y -> liftA2 (||) x y
-    LogImpl x y -> liftA2 (==>) x y
-    LogEquiv x y -> liftA2 (<=>) x y
+    LogImpl x y -> liftA2 (||) (not <$> x) y
+    LogEquiv x y -> liftA2 (&&) (liftA2 (||) (not <$> x) y) (liftA2 (||) (not <$> y) x)
 
 instance HFoldableAt SBV LogicOp where
   hfoldMap = implHfoldMap $ \case
     LogLit b -> fromBool b
-    LogNot x -> bnot x
-    LogAnd x y -> x &&& y
-    LogOr x y -> x ||| y
-    LogImpl x y -> x ==> y
-    LogEquiv x y -> x <=> y
+    LogNot x -> sNot x
+    LogAnd x y -> x .&& y
+    LogOr x y -> x .|| y
+    LogImpl x y -> x .=> y
+    LogEquiv x y -> x .<=> y
 
 -- instance HEq LogicOp where
 --   liftHEq _ _ (LogLit x) (LogLit y) = x == y

Language/While/Syntax.hs

@@ -79,10 +79,10 @@ instance EvalOpAt SBV WhileOpKind where
     OpGT -> runcurry (.>)
     OpGE -> runcurry (.>=)
 
-    OpAnd -> runcurry (&&&)
-    OpOr -> runcurry (|||)
+    OpAnd -> runcurry (.&&)
+    OpOr -> runcurry (.||)
 
-    OpNot -> runcurry bnot
+    OpNot -> runcurry sNot
 
 -- instance EqOpMany WhileOpKind where
 --   liftEqMany (OpLit x) (OpLit y) _ = \_ _ -> x == y

package.yaml

@@ -1,5 +1,5 @@
 name: verifiable-expressions
-version: '0.5.0'
+version: '0.6.0'
 category: Language
 author: Bradley Hardy
 maintainer: [email protected]
@@ -15,7 +15,7 @@ dependencies:
 - transformers >=0.5 && <0.6
 - mtl >=2.0 && <3
 - lens >=4.16.1 && <5
-- sbv >=7.0 && <8
+- sbv >=8.0 && <9
 - union >=0.1.1 && <0.2
 - vinyl >=0.8.1 && <0.9
 library:

stack.yaml

@@ -5,4 +5,4 @@ packages:
 extra-deps:
 - syz-0.2.0.0
 - vinyl-0.8.1
-resolver: lts-13.6
+resolver: lts-14.1