tamarin-prover-term 0.8.5.0 → 0.8.5.1
raw patch · 6 files changed
+25/−19 lines, 6 filesdep ~tamarin-prover-utils
Dependency ranges changed: tamarin-prover-utils
Files
- src/Term/LTerm.hs +8/−3
- src/Term/Rewriting/Norm.hs +8/−7
- src/Term/Term.hs +1/−1
- src/Term/Term/Raw.hs +3/−3
- src/Term/Unification.hs +3/−3
- tamarin-prover-term.cabal +2/−2
src/Term/LTerm.hs view
@@ -99,9 +99,6 @@ , module Term.VTerm ) where -import Term.Rewriting.Definitions-import Term.VTerm- import Text.PrettyPrint.Class import Control.Applicative@@ -126,8 +123,12 @@ import Extension.Data.Monoid import Extension.Prelude + import Logic.Connectives +import Term.Rewriting.Definitions+import Term.VTerm+ ------------------------------------------------------------------------------ -- Sorts. ------------------------------------------------------------------------------@@ -278,6 +279,10 @@ isFreshVar :: LNTerm -> Bool isFreshVar (viewTerm -> Lit (Var v)) = (lvarSort v == LSortFresh) isFreshVar _ = False+++-- Utility functions for constraint solving+------------------------------------------- -- | The non-inverse factors of a term. niFactors :: LNTerm -> [LNTerm]
src/Term/Rewriting/Norm.hs view
@@ -15,13 +15,6 @@ , maybeNotNfSubterms ) where -import Term.LTerm-import Term.Maude.Process-import Term.Maude.Signature-import Term.Substitution-import Term.SubtermRule-import Term.Unification- import Utils.Misc import Control.Basics@@ -31,6 +24,14 @@ import qualified Data.Set as S import System.IO.Unsafe (unsafePerformIO)+++import Term.LTerm+import Term.Maude.Process+import Term.Maude.Signature+import Term.Substitution+import Term.SubtermRule+import Term.Unification ---------------------------------------------------------------------- -- Normalization using Maude
src/Term/Term.hs view
@@ -76,8 +76,8 @@ import qualified Data.ByteString.Char8 as BC import Extension.Data.ByteString () - import Text.PrettyPrint.Class+ import Term.Term.Classes import Term.Term.FunctionSymbols import Term.Term.Raw
src/Term/Term/Raw.hs view
@@ -82,7 +82,7 @@ fApp (AC acSym) ts = fAppAC acSym ts fApp (C o) ts = fAppC o ts fApp List ts = FAPP List ts-fApp s@(NoEq _) ts = FAPP s ts+fApp s@(NoEq _) ts = FAPP s ts -- | Smart constructor for AC terms. fAppAC :: Ord a => ACSym -> [Term a] -> Term a@@ -97,11 +97,11 @@ (o_as0, non_o_as) = partition isOTerm as o_as = [ a | FAPP _ ts <- o_as0, a <- ts ] --- | Smart constructor for AC terms.+-- | Smart constructor for C terms. fAppC :: Ord a => CSym -> [Term a] -> Term a fAppC nacsym as = FAPP (C nacsym) (sort as) --- | Smart constructor for non-AC terms.+-- | Smart constructor for non-AC/C terms. {-# INLINE fAppNoEq #-} fAppNoEq :: NoEqSym -> [Term a] -> Term a fAppNoEq freesym = FAPP (NoEq freesym)
src/Term/Unification.hs view
@@ -68,6 +68,7 @@ import System.IO.Unsafe (unsafePerformIO) + import Term.Rewriting.Definitions import Term.Substitution import qualified Term.Maude.Process as UM@@ -75,7 +76,6 @@ (MaudeHandle, WithMaude, startMaude, getMaudeStats, mhMaudeSig, mhFilePath) import Term.Maude.Signature import Debug.Trace.Ignore--- import qualified Debug.Trace as DT -- Unification modulo AC ----------------------------------------------------------------------@@ -112,7 +112,6 @@ -- | @unifyLNTerm eqs@ returns a complete set of unifiers for @eqs@ modulo AC. unifyLNTerm :: [Equal LNTerm] -> WithMaude [SubstVFresh Name LVar]--- unifyLNTerm eqs = reader $ \hnd -> (\res -> DT.trace (show ("unify", res, eqs)) res) $ unifyLTerm sortOfName eqs `runReader` hnd unifyLNTerm = unifyLTerm sortOfName -- | 'True' iff the terms are unifiable.@@ -121,7 +120,8 @@ -- | Flatten a factored substitution to a list of substitutions. flattenUnif :: IsConst c => (LSubst c, [LSubstVFresh c]) -> [LSubstVFresh c]-flattenUnif (subst, substs) = (\res -> trace (show ("flattenUnif",subst, substs,res )) res) $ map (`composeVFresh` subst) substs+flattenUnif (subst, substs) = + (\res -> trace (show ("flattenUnif",subst, substs,res )) res) $ map (`composeVFresh` subst) substs -- Matching modulo AC ----------------------------------------------------------------------
tamarin-prover-term.cabal view
@@ -2,7 +2,7 @@ cabal-version: >= 1.8 build-type: Simple-version: 0.8.5.0+version: 0.8.5.1 license: GPL license-file: LICENSE category: Theorem Provers@@ -58,7 +58,7 @@ , HUnit == 1.* - , tamarin-prover-utils >= 0.8.5 && < 0.9+ , tamarin-prover-utils >= 0.8.5.1 && < 0.9 hs-source-dirs: src