twee 2.1.4 → 2.1.5
raw patch · 3 files changed
+16/−16 lines, 3 filesdep ~jukeboxdep ~twee-lib
Dependency ranges changed: jukebox, twee-lib
Files
- executable/Main.hs +3/−3
- misc/bench.hs +10/−10
- twee.cabal +3/−3
executable/Main.hs view
@@ -217,7 +217,7 @@ Main.isEquals fun isType :: Jukebox.Function -> Bool-isType fun = "$to_" `isPrefixOf` base (name fun)+isType fun = "$to_" `isPrefixOf` base (name fun) && Jukebox.arity fun == 1 isIfeq :: Jukebox.Function -> Bool isIfeq fun = "$ifeq" `isPrefixOf` base (name fun)@@ -437,7 +437,7 @@ pPrintTerm uncurried prettyNormal 0 (text f) xs step :: String -> [Doc] -> Doc- step f xs = traceApp "step" [traceApp f xs] <> text "."+ step f xs = traceApp "step" [traceApp f xs] <#> text "." say "Here is the input problem:" forM_ axioms $ \Axiom{..} ->@@ -460,7 +460,7 @@ sayTrace "" forM_ (pres_lemmas pres) $ \Lemma{..} -> sayTrace $ show $- traceApp "lemma" [traceEqn (equation lemma_proof)] <> text "."+ traceApp "lemma" [traceEqn (equation lemma_proof)] <#> text "." when tstp $ do putStrLn "% SZS output start CNFRefutation"
misc/bench.hs view
@@ -1,24 +1,24 @@ {-# LANGUAGE PatternGuards, FlexibleInstances #-} import Criterion.Main-import Twee.Term hiding (isFun)+import Twee.Term hiding (isFun, F) import qualified Twee.Term-import Test.QuickCheck+import Test.QuickCheck hiding (Fun) import Data.Int import Data.Maybe import Twee.Term.Core hiding (subst) -instance Num (Fun Int) where fromInteger n = F (fromInteger n) (fromInteger n)+instance Num (Fun Int) where fromInteger n = F (fromInteger n) instance Num Var where fromInteger = V . fromInteger t0, t1, u0, u1, t2, t, u :: Term Int-t0 = build $ fun 0 [var 0, fun 0 [var 0, fun 0 [fun 0 [var 0, var 1], var 2]]]-u0 = build $ fun 0 [fun 0 [fun 2 [fun 2 [var 2, var 2], var 1], fun 0 [fun 2 [var 2, var 2], var 3]], fun 0 [fun 0 [fun 2 [fun 2 [var 2, var 2], var 1], fun 0 [fun 2 [var 2, var 2], var 3]], fun 0 [fun 0 [fun 0 [fun 2 [fun 2 [var 2, var 2], var 1], fun 0 [fun 2 [var 2, var 2], var 3]], fun 2 [fun 2 [var 2, var 2], var 1]], fun 2 [var 2, var 2]]]]+t0 = build $ app 0 [var 0, app 0 [var 0, app 0 [app 0 [var 0, var 1], var 2]]]+u0 = build $ app 0 [app 0 [app 2 [app 2 [var 2, var 2], var 1], app 0 [app 2 [var 2, var 2], var 3]], app 0 [app 0 [app 2 [app 2 [var 2, var 2], var 1], app 0 [app 2 [var 2, var 2], var 3]], app 0 [app 0 [app 0 [app 2 [app 2 [var 2, var 2], var 1], app 0 [app 2 [var 2, var 2], var 3]], app 2 [app 2 [var 2, var 2], var 1]], app 2 [var 2, var 2]]]] -t1 = build $ fun 0 [fun 1 [var 0], fun 1 [var 1]]-u1 = build $ fun 0 [fun 1 [fun 0 [fun 2 emptyTermList, fun 3 emptyTermList]], fun 1 [fun 0 [fun 4 emptyTermList, fun 5 emptyTermList]]]+t1 = build $ app 0 [app 1 [var 0], app 1 [var 1]]+u1 = build $ app 0 [app 1 [app 0 [app 2 empty, app 3 empty]], app 1 [app 0 [app 4 empty, app 5 empty]]] -t2 = build $ fun 0 [var 0, fun 1 [var 1, fun 1 [var 1, var 1]]]-u2 = build $ fun 0 [fun 0 [var 2, var 2], var 2]+t2 = build $ app 0 [var 0, app 1 [var 1, app 1 [var 1, var 1]]]+u2 = build $ app 0 [app 0 [var 2, var 2], var 2] t = t0 u = u0@@ -61,7 +61,7 @@ bench "unify-subst-closed2" (whnf (build . uncurry subst) (csub', u2)), bench "mgu-tri" (whnf (uncurry mgu1) (t2, u2)), bench "mgu-close" (whnf (uncurry mgu2) (t2, u2)),- bench "make-constant" (whnf (build . uncurry fun) (F 0 0, emptyTermList)),+ bench "make-constant" (whnf (build . uncurry app) (F 0, empty)), bench "baseline" (whnf (uncurry (+)) (0 :: Int, 0))] prop :: Bool -> NonNegative (Small Int) -> NonNegative (Small Int) -> Property
twee.cabal view
@@ -1,5 +1,5 @@ name: twee-version: 2.1.4+version: 2.1.5 synopsis: An equational theorem prover homepage: http://github.com/nick8325/twee license: BSD3@@ -44,11 +44,11 @@ main-is: executable/Main.hs default-language: Haskell2010 build-depends: base < 5,- twee-lib == 2.1.4,+ twee-lib == 2.1.5, containers, pretty, split,- jukebox >= 0.3.2+ jukebox >= 0.3.5 ghc-options: -W -fno-warn-incomplete-patterns -O2 -fmax-worker-args=100 if flag(llvm)