atp-haskell 1.9 → 1.10

raw patch · 3 files changed

+85/−44 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• .travis.yml +60/−22
• atp-haskell.cabal +2/−1
• src/Data/Logic/ATP/Unif.hs +23/−21

@@ -1,44 +1,82 @@+# This file has been generated -- see https://github.com/hvr/multi-ghc-travis+language: c sudo: false +cache:+  directories:+    - $HOME/.cabsnap+    - $HOME/.cabal/packages++before_cache:+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/build-reports.log+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/00-index.tar+ matrix:   include:-    - env: CABALVER=1.22 GHCVER=7.10.2-      addons: {apt: {packages: [cabal-install-1.22,ghc-7.10.2],sources: [hvr-ghc]}}+    - env: CABALVER=1.22 GHCVER=7.10.3+      compiler: ": #GHC 7.10.3"+      addons: {apt: {packages: [cabal-install-1.22,ghc-7.10.3], sources: [hvr-ghc]}}     - env: CABALVER=head GHCVER=head-      addons: {apt: {packages: [cabal-install-head,ghc-head],  sources: [hvr-ghc]}}+      compiler: ": #GHC head"+      addons: {apt: {packages: [cabal-install-head,ghc-head], sources: [hvr-ghc]}}    allow_failures:-   - env: CABALVER=head GHCVER=head+    - env: CABALVER=head GHCVER=head  before_install:+ - unset CC  - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH  install:  - cabal --version  - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]"- - travis_retry cabal update- - cabal install --only-dependencies --enable-tests --enable-benchmarks+ - if [ -f $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz ];+   then+     zcat $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz >+          $HOME/.cabal/packages/hackage.haskell.org/00-index.tar;+   fi+ - travis_retry cabal update -v+ - sed -i 's/^jobs:/-- jobs:/' ${HOME}/.cabal/config+ - cabal install --only-dependencies --enable-tests --enable-benchmarks --dry -v > installplan.txt+ - sed -i -e '1,/^Resolving /d' installplan.txt; cat installplan.txt -# Here starts the actual work to be performed for the package under-# test; any command which exits with a non-zero exit code causes the-# build to fail.+# check whether current requested install-plan matches cached package-db snapshot+ - if diff -u installplan.txt $HOME/.cabsnap/installplan.txt;+   then+     echo "cabal build-cache HIT";+     rm -rfv .ghc;+     cp -a $HOME/.cabsnap/ghc $HOME/.ghc;+     cp -a $HOME/.cabsnap/lib $HOME/.cabsnap/share $HOME/.cabsnap/bin $HOME/.cabal/;+   else+     echo "cabal build-cache MISS";+     rm -rf $HOME/.cabsnap;+     mkdir -p $HOME/.ghc $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin;+     cabal install --only-dependencies --enable-tests --enable-benchmarks;+   fi +# snapshot package-db on cache miss+ - if [ ! -d $HOME/.cabsnap ];+   then+      echo "snapshotting package-db to build-cache";+      mkdir $HOME/.cabsnap;+      cp -a $HOME/.ghc $HOME/.cabsnap/ghc;+      cp -a $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin installplan.txt $HOME/.cabsnap/;+   fi++# Here starts the actual work to be performed for the package under test;+# any command which exits with a non-zero exit code causes the build to fail. script:- - cabal configure --enable-tests -v2  # -v2 provides useful information for debugging+ - if [ -f configure.ac ]; then autoreconf -i; fi+ - cabal configure --enable-tests --enable-benchmarks -v2  # -v2 provides useful information for debugging  - cabal build   # this builds all libraries and executables (including tests/benchmarks)  - cabal test- # - cabal check+# - cabal check  - cabal sdist   # tests that a source-distribution can be generated -# The following scriptlet checks that the resulting source distribution can be built & installed- - export SRC_TGZ=$(cabal info . | awk '{print $2 ".tar.gz";exit}') ;-   cd dist/;-   if [ -f "$SRC_TGZ" ]; then-      cabal install --force-reinstalls "$SRC_TGZ";-   else-      echo "expected '$SRC_TGZ' not found";-      exit 1;-   fi+# Check that the resulting source distribution can be built & installed.+# If there are no other `.tar.gz` files in `dist`, this can be even simpler:+# `cabal install --force-reinstalls dist/*-*.tar.gz`+ - SRC_TGZ=$(cabal info . | awk '{print $2;exit}').tar.gz &&+   (cd dist && cabal install --force-reinstalls "$SRC_TGZ") -after_script:-  - cat dist/test/*.log+# EOF

@@ -1,5 +1,5 @@ Name:             atp-haskell-Version:          1.9+Version:          1.10 Synopsis:         Translation from Ocaml to Haskell of John Harrison's ATP code Description:      This package is a liberal translation from OCaml to Haskell of                   the automated theorem prover written in OCaml in@@ -15,6 +15,7 @@ Cabal-version:    >= 1.9 Build-Type:       Simple Extra-Source-Files: tests/Extra.hs, .travis.yml, .ghci+Tested-With:      GHC == 7.10.3, GHC == 7.11.*  Source-Repository head   type: git

@@ -52,36 +52,38 @@ -- EqualityT a) b)@. class (IsTerm (UTermOf a), IsVariable (TVarOf (UTermOf a))) => Unify a where     type UTermOf a-    unify :: a -> StateT (Map (TVarOf (UTermOf a)) (UTermOf a)) Failing ()+    unify :: Monad m => a -> StateT (Map (TVarOf (UTermOf a)) (UTermOf a)) m () -unify_terms :: (IsTerm term, v ~ TVarOf term) => [(term,term)] -> StateT (Map v term) Failing ()+unify_terms :: (IsTerm term, v ~ TVarOf term, Monad m) =>+               [(term,term)] -> StateT (Map v term) m () unify_terms = mapM_ (uncurry unify_term_pair) -unify_term_pair :: forall term v f. (IsTerm term, v ~ TVarOf term, f ~ FunOf term) =>-                   term -> term -> StateT (Map v term) Failing ()+unify_term_pair :: forall term v f m.+                   (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) =>+                   term -> term -> StateT (Map v term) m () unify_term_pair a b =     foldTerm (vr b) (\ f fargs -> foldTerm (vr a) (fn f fargs) b) a     where-      vr :: term -> v -> StateT (Map v term) Failing ()+      vr :: term -> v -> StateT (Map v term) m ()       vr t x =           (Map.lookup x <$> get) >>=           maybe (istriv x t >>= bool (modify (Map.insert x t)) (return ()))                 (\y -> unify_term_pair y t)-      fn :: f -> [term] -> f -> [term] -> StateT (Map v term) Failing ()+      fn :: f -> [term] -> f -> [term] -> StateT (Map v term) m ()       fn f fargs g gargs =           if f == g && length fargs == length gargs           then mapM_ (uncurry unify_term_pair) (zip fargs gargs)           else fail "impossible unification" -istriv :: forall term v. (IsTerm term, v ~ TVarOf term) =>-          v -> term -> StateT (Map v term) Failing Bool+istriv :: forall term v m. (IsTerm term, v ~ TVarOf term, Monad m) =>+          v -> term -> StateT (Map v term) m Bool istriv x t =     foldTerm vr fn t     where-      -- vr :: v -> StateT (Map v term) Failing Bool+      vr :: v -> StateT (Map v term) m Bool       vr y | x == y = return True       vr y = (Map.lookup y <$> get) >>= maybe (return False) (istriv x)-      -- fn :: f -> [term] -> StateT (Map v term) Failing Bool+      fn :: f -> [term] -> StateT (Map v term) m Bool       fn _ args = mapM (istriv x) args >>= bool (return False) (fail "cyclic") . or  -- | Solve to obtain a single instantiation.@@ -92,13 +94,13 @@     where env' = Map.map (tsubst env) env  -- | Unification reaching a final solved form (often this isn't needed).-fullunify :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term) =>-             [(term,term)] -> Failing (Map v term)+fullunify :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) =>+             [(term,term)] -> m (Map v term) fullunify eqs = solve <$> execStateT (unify_terms eqs) Map.empty  -- | Examples.-unify_and_apply :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term) =>-                   [(term, term)] -> Failing [(term, term)]+unify_and_apply :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) =>+                   [(term, term)] -> m [(term, term)] unify_and_apply eqs =     fullunify eqs >>= \i -> return $ List.map (\ (t1, t2) -> (tsubst i t1, tsubst i t2)) eqs @@ -108,8 +110,8 @@ -- who cares. unify_literals :: (IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1, term ~ TermOf atom1,                    JustLiteral lit2, HasApply atom2, atom2 ~ AtomOf lit2, term ~ TermOf atom2,-                   Unify (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term) =>-                  lit1 -> lit2 -> StateT (Map v term) Failing ()+                   Unify (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term, Monad m) =>+                  lit1 -> lit2 -> StateT (Map v term) m () unify_literals f1 f2 =     fromMaybe (fail "Can't unify literals") (zipLiterals' ho ne tf at f1 f2)     where@@ -120,21 +122,21 @@  unify_atoms :: (JustApply atom1, term ~ TermOf atom1,                 JustApply atom2, term ~ TermOf atom2,-                v ~ TVarOf term, PredOf atom1 ~ PredOf atom2) =>-               (atom1, atom2) -> StateT (Map v term) Failing ()+                v ~ TVarOf term, PredOf atom1 ~ PredOf atom2, Monad m) =>+               (atom1, atom2) -> StateT (Map v term) m () unify_atoms (a1, a2) =     maybe (fail "unify_atoms") id (zipApplys (\_ tpairs -> Just (unify_terms tpairs)) a1 a2)  unify_atoms_eq :: (HasEquate atom1, term ~ TermOf atom1,                    HasEquate atom2, term ~ TermOf atom2,-                   PredOf atom1 ~ PredOf atom2, v ~ TVarOf term) =>-                  atom1 -> atom2 -> StateT (Map v term) Failing ()+                   PredOf atom1 ~ PredOf atom2, v ~ TVarOf term, Monad m) =>+                  atom1 -> atom2 -> StateT (Map v term) m () unify_atoms_eq a1 a2 =     maybe (fail "unify_atoms") id (zipEquates (\l1 r1 l2 r2 -> Just (unify_terms [(l1, l2), (r1, r2)]))                                               (\_ tpairs -> Just (unify_terms tpairs))                                               a1 a2) ---unify_and_apply' :: (v ~ TVarOf term, f ~ FunOf term, IsTerm term) => [(term, term)] -> Failing [(term, term)]+--unify_and_apply' :: (v ~ TVarOf term, f ~ FunOf term, IsTerm term, Monad m) => [(term, term)] -> m [(term, term)] --unify_and_apply' eqs = --    mapM app eqs --        where