diff --git a/src/Term/Maude/Types.hs b/src/Term/Maude/Types.hs --- a/src/Term/Maude/Types.hs +++ b/src/Term/Maude/Types.hs @@ -2,7 +2,7 @@ -- | -- Copyright : (c) 2010-2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) --- +-- -- Maintainer : Benedikt Schmidt -- -- 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 diff --git a/src/Term/Narrowing/Variants/Compute.hs b/src/Term/Narrowing/Variants/Compute.hs --- a/src/Term/Narrowing/Variants/Compute.hs +++ b/src/Term/Narrowing/Variants/Compute.hs @@ -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 diff --git a/src/Term/Positions.hs b/src/Term/Positions.hs --- a/src/Term/Positions.hs +++ b/src/Term/Positions.hs @@ -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" diff --git a/src/Term/Substitution/SubstVFree.hs b/src/Term/Substitution/SubstVFree.hs --- a/src/Term/Substitution/SubstVFree.hs +++ b/src/Term/Substitution/SubstVFree.hs @@ -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) diff --git a/src/Term/Unification.hs b/src/Term/Unification.hs --- a/src/Term/Unification.hs +++ b/src/Term/Unification.hs @@ -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 diff --git a/src/Term/UnitTests.hs b/src/Term/UnitTests.hs --- a/src/Term/UnitTests.hs +++ b/src/Term/UnitTests.hs @@ -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 diff --git a/tamarin-prover-term.cabal b/tamarin-prover-term.cabal --- a/tamarin-prover-term.cabal +++ b/tamarin-prover-term.cabal @@ -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