tamarin-prover-term 0.4.0.0 → 0.4.1.0
raw patch · 2 files changed
+6/−6 lines, 2 filesdep ~tamarin-prover-utilsPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: tamarin-prover-utils
API changes (from Hackage documentation)
- Term.LTerm: instance Binary v_1627480100 => Binary (BVar v_1627480100)
- Term.LTerm: instance NFData v_1627480100 => NFData (BVar v_1627480100)
- Term.VTerm: instance (Binary c_1627456936, Binary v_1627456937) => Binary (Lit c_1627456936 v_1627456937)
- Term.VTerm: instance (NFData c_1627456936, NFData v_1627456937) => NFData (Lit c_1627456936 v_1627456937)
+ Term.LTerm: instance Binary v_1627480102 => Binary (BVar v_1627480102)
+ Term.LTerm: instance NFData v_1627480102 => NFData (BVar v_1627480102)
+ Term.VTerm: instance (Binary c_1627456938, Binary v_1627456939) => Binary (Lit c_1627456938 v_1627456939)
+ Term.VTerm: instance (NFData c_1627456938, NFData v_1627456939) => NFData (Lit c_1627456938 v_1627456939)
Files
- src/Term/UnitTests.hs +4/−4
- tamarin-prover-term.cabal +2/−2
src/Term/UnitTests.hs view
@@ -90,7 +90,7 @@ testsSubst = TestLabel "Tests for Substitution" $ TestList [ -- introduce renaming for x3- testEqual "a" (substFromListVFresh [(lx1, p1), (lx2, x9), (lx3,x9), (lx5, p1)])+ testEqual "a" (substFromListVFresh [(lx1, p1), (lx2, x6), (lx3,x6), (lx5, p1)]) (composeVFresh (substFromListVFresh [(lx5, p1)]) (substFromList [(lx1, x5), (lx2, x3)])) -- rename (fresh) x6 in s1b and do not mix up with x6 in s3f@@ -105,7 +105,7 @@ , testEqual "g" (substFromListVFresh [(lx1, f1)]) (extendWithRenaming [lx1] (substFromListVFresh [(lx1, f1)])) - , testEqual "h" (substFromListVFresh [(lx2, x1), (lx1, x3)])+ , testEqual "h" (substFromListVFresh [(lx2, x1), (lx1, x2)]) (extendWithRenaming [lx1] (substFromListVFresh [(lx2, x1)])) -- trivial, increase coverage , testTrue "i" ((>0) . length $ show s1b)@@ -121,10 +121,10 @@ s1b = substFromListVFresh [(lx1, p1), (lx2, x6), (lx3, x6), (lx4, f1)] s3f = substFromList [(lx8, x6), (lx2, pair(x2,x1))] s1b_o_s3f = substFromListVFresh -- x2 not identified with x8- [(lx1, p1), (lx2, pair(x15, p1)), (lx3, x15), (lx4, f1), (lx6, x22), (lx8, x22)]+ [(lx1, p1), (lx2, pair(x9, p1)), (lx3, x9), (lx4, f1), (lx6, x10), (lx8, x10)] s4f = substFromList [(lx1, x6), (lx2, pair(x3,x1))] s1b_o_s4f = substFromListVFresh- [(lx1, x20), (lx2, pair(x13, p1)), (lx3, x13), (lx4, f1), (lx6, x20)]+ [(lx1, x8), (lx2, pair(x7, p1)), (lx3, x7), (lx4, f1), (lx6, x8)] s4f_o_s3f = substFromList [(lx1, x6), (lx2, pair(pair(x3,x1),x6)), (lx8, x6)] x15 = varTerm $ LVar "x" LSortMsg 15
tamarin-prover-term.cabal view
@@ -2,7 +2,7 @@ cabal-version: >= 1.8 build-type: Simple-version: 0.4.0.0+version: 0.4.1.0 license: GPL license-file: LICENSE category: Theorem Provers@@ -52,7 +52,7 @@ , HUnit == 1.2.* - , tamarin-prover-utils == 0.4.*+ , tamarin-prover-utils == 0.4.1.* hs-source-dirs: src