tamarin-prover-term 0.8.4.0 → 0.8.5.0

raw patch · 7 files changed

+31/−32 lines, 7 filesdep ~HUnitdep ~binarydep ~bytestring

Dependency ranges changed: HUnit, binary, bytestring, containers, deepseq, derive, directory, mtl, process, safe, syb, tamarin-prover-utils

Files

• src/Term/Maude/Types.hs +2/−2
• src/Term/Narrowing/Variants/Compute.hs +13/−14
• src/Term/Positions.hs +1/−1
• src/Term/Substitution/SubstVFree.hs +1/−0
• src/Term/Unification.hs +0/−1
• src/Term/UnitTests.hs +1/−1
• tamarin-prover-term.cabal +13/−13

@@ -2,7 +2,7 @@ -- | -- Copyright   : (c) 2010-2012 Benedikt Schmidt -- License     : GPL v3 (see LICENSE)--- +-- -- Maintainer  : Benedikt Schmidt <beschmi@gmail.com> -- -- Types for communicating with Maude.@@ -62,7 +62,7 @@   -- | Convert an @LNTerm@ with arbitrary names to an @MTerm@.-lTermToMTerm :: (MonadBind (Lit c LVar) MaudeLit m, MonadFresh m, Show (Lit c LVar), Ord c)+lTermToMTerm :: (MonadBind (Lit c LVar) MaudeLit m, MonadFresh m, Show c, Show (Lit c LVar), Ord c)              => (c -> LSort) -- ^ A function that returns the sort of a constant.              -> VTerm c LVar -- ^ The term to translate.              -> m MTerm

@@ -59,23 +59,22 @@ instance Sized Variant where     size = size . varSubst --- | @narrowVariant rules t maxdepth@ either returns @Left (explored, unexplored)@+-- | @narrowVariant rules t maxdepth@ either returns @Nothing@ --   if variant narrrowing hit the bound and there are still unexplored steps---   or @Right (stepnum, explored)@ if the search finished before hitting the+--   or @Just explored@ if the search finished before hitting the --   bound. narrowVariant :: LNTerm -- ^ The term.               -> Maybe Int -- ^ The step bound.-              -> WithMaude (Either ([Variant], [Variant]) (Int, [Variant]))-narrowVariant tstart maxdepth0 =+              -> WithMaude (Maybe [Variant])+narrowVariant tstart maxdepth =     reader $ \hnd -> go maxdepth [ Variant [] emptySubstVFresh ] [] hnd   where-    maxdepth = fromMaybe (-1) maxdepth0-    go :: Int -> [Variant] -> [Variant] -> MaudeHandle-       -> Either ([Variant], [Variant]) (Int, [Variant])-    go n []         explored _ = Right (maxdepth-n, explored)-    go 0 unexplored explored _ = Left (explored, unexplored)-    go n unexplored explored hnd = (\res -> (trace (show (n,unexplored, explored, res)) res)) $-        go (n-1) new explored' hnd+    go :: Maybe Int -> [Variant] -> [Variant] -> MaudeHandle+       -> Maybe [Variant]+    go _        []           explored _ = Just explored+    go (Just 0) _unexplored _explored _ = Nothing+    go n unexplored explored hnd = (\res -> (trace (show (n, unexplored, explored, res, new0, explored', new)) res)) $+        go (fmap pred n) new explored' hnd       where         runWithMaude = (`runReader` hnd)         explored0 = explored++unexplored@@ -108,7 +107,7 @@     go x (y:todo,done)       -- x and y have already been filtered earlier and are therefore incomparable       | alreadyFiltered x && alreadyFiltered y = go x (todo,y:done)-      -- either x or y is new, so we have to comparison the two+      -- either x or y is new, so we have to compare the two       | otherwise       = case cmp x y of           Nothing -> go x (todo,y:done)@@ -132,8 +131,8 @@                      -> WithMaude (Maybe [LNSubstVFresh]) computeVariantsBound t d = reader $ \hnd -> (\res -> trace (show ("ComputeVariantsBound", t, res)) res) $     case (`runReader` hnd) $ narrowVariant t d of-      Left _ -> Nothing-      Right (_,explored) ->+      Nothing -> Nothing+      Just explored ->         Just (map varSubst (sortBy (comparing size) explored))  -- | @variantsList ts@ computes all variants of @ts@ considered as a single term

@@ -33,7 +33,7 @@ atPos (viewTerm -> FApp fsym@(AC _) (_:as)) (1:ps) =     (fApp fsym as) `atPos` ps atPos (viewTerm -> FApp (AC _) [])          _      =-    error $ "Term.Positions.positionsNonVar: impossible, "+    error $ "Term.Positions.atPos: impossible, "             ++"nullary AC symbol appliction" atPos (viewTerm -> FApp  _ as)              (i:ps) = case atMay as i of     Nothing -> error "Term.Positions.atPos: invalid position given"

@@ -2,6 +2,7 @@ {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeSynonymInstances #-} -- | -- Copyright   : (c) 2010-2012 Benedikt Schmidt & Simon Meier -- License     : GPL v3 (see LICENSE)

@@ -61,7 +61,6 @@  import           Control.Applicative import           Control.Monad.RWS-import           Control.Monad.Reader import           Control.Monad.Error import           Control.Monad.State import qualified Data.Map as M

@@ -22,7 +22,7 @@  import Data.List import Data.Maybe-import Prelude hiding ( catch )+import Prelude import Test.HUnit import Control.Monad.Reader import Data.Monoid

@@ -2,7 +2,7 @@  cabal-version:      >= 1.8 build-type:         Simple-version:            0.8.4.0+version:            0.8.5.0 license:            GPL license-file:       LICENSE category:           Theorem Provers@@ -41,24 +41,24 @@      build-depends:         base                 == 4.*-      , mtl                  == 2.0.*-      , bytestring           == 0.9.*+      , mtl                  == 2.*+      , bytestring           >= 0.9       , attoparsec           == 0.10.*-      , containers           >= 0.4.2   && < 0.5+      , containers           >= 0.4.2          , dlist                == 0.5.*-      , safe                 >= 0.2     && < 0.4+      , safe                 >= 0.2           , split                == 0.1.*       , parsec               == 3.1.*-      , syb                  >= 0.3.3   && < 0.4-      , directory            == 1.1.*-      , process              == 1.1.*-      , deepseq              == 1.3.*-      , binary               == 0.5.*-      , derive               == 2.5.*+      , syb                  >= 0.3.3+      , directory            >= 1.1+      , process              >= 1.1+      , deepseq              >= 1.3+      , binary               == 0.*+      , derive               == 2.* -      , HUnit                == 1.2.*+      , HUnit                == 1.* -      , tamarin-prover-utils >= 0.8.4  && < 0.9+      , tamarin-prover-utils >= 0.8.5  && < 0.9       hs-source-dirs: src