packages feed

tamarin-prover-term 0.8.0.0 → 0.8.1.0

raw patch · 2 files changed

+19/−6 lines, 2 filesdep ~tamarin-prover-utilsPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: tamarin-prover-utils

API changes (from Hackage documentation)

- Term.LTerm: instance Binary v_1627481246 => Binary (BVar v_1627481246)
- Term.LTerm: instance NFData v_1627481246 => NFData (BVar v_1627481246)
- Term.VTerm: instance (Binary c_1627456989, Binary v_1627456990) => Binary (Lit c_1627456989 v_1627456990)
- Term.VTerm: instance (NFData c_1627456989, NFData v_1627456990) => NFData (Lit c_1627456989 v_1627456990)
+ Term.LTerm: instance Binary v_1627481569 => Binary (BVar v_1627481569)
+ Term.LTerm: instance NFData v_1627481569 => NFData (BVar v_1627481569)
+ Term.VTerm: instance (Binary c_1627457312, Binary v_1627457313) => Binary (Lit c_1627457312 v_1627457313)
+ Term.VTerm: instance (NFData c_1627457312, NFData v_1627457313) => NFData (Lit c_1627457312 v_1627457313)
+ Term.VTerm: isNullaryFunction :: Term a -> Bool
+ Term.VTerm: showFunSymName :: FunSym -> String

Files

src/Term/Term.hs view
@@ -6,7 +6,7 @@ -- | -- Copyright   : (c) 2010, 2011 Benedikt Schmidt & Simon Meier -- License     : GPL v3 (see LICENSE)--- +-- -- Maintainer  : Benedikt Schmidt <beschmi@gmail.com> -- -- Term Algebra and related notions.@@ -34,8 +34,9 @@     , fmapTerm     , bindTerm     , lits+    , showFunSymName     , prettyTerm-    +     -- ** Smart constructors     , lit     , fApp@@ -72,6 +73,7 @@     , isProduct     , isXor     , isUnion+    , isNullaryFunction      , module Term.Classes     ) where@@ -228,6 +230,11 @@ isUnion :: Term a -> Bool isUnion = isJust . destXor +-- | 'True' iff the term is a nullary, public function.+isNullaryFunction :: Term a -> Bool+isNullaryFunction (viewTerm -> FApp (NonAC (_, 0)) _) = True+isNullaryFunction _                                   = False+ -- | View on terms that corresponds to representation. data TermView a = Lit a                 | FApp FunSym [Term a]@@ -236,7 +243,7 @@ {-# INLINE viewTerm #-} -- | Return the 'TermView' of the given term. viewTerm :: Term a -> TermView a-viewTerm (LIT l) = Lit l+viewTerm (LIT l)       = Lit l viewTerm (FAPP sym ts) = FApp sym ts  -- | @fApp fsym as@ creates an application of @fsym@ to @as@. The function@@ -388,6 +395,12 @@ -- Pretty printing ---------------------------------------------------------------------- +-- | Convert a function symbol to its name.+showFunSymName :: FunSym -> String+showFunSymName (NonAC (bs, _)) = BC.unpack bs+showFunSymName (AC op)         = show op+showFunSymName List            = "List"+ -- | Pretty print a term. prettyTerm :: Document d => (l -> d) -> Term l -> d prettyTerm ppLit = ppTerm@@ -405,7 +418,7 @@     ppACOp Xor   = "+"      ppTerms sepa n lead finish ts =-        fcat . (text lead :) . (++[text finish]) . +        fcat . (text lead :) . (++[text finish]) .             map (nest n) . punctuate (text sepa) . map ppTerm $ ts      split (FAPP (NonAC ("pair",2)) [t1,t2]) = t1 : split t2
tamarin-prover-term.cabal view
@@ -2,7 +2,7 @@  cabal-version:      >= 1.8 build-type:         Simple-version:            0.8.0.0+version:            0.8.1.0 license:            GPL license-file:       LICENSE category:           Theorem Provers@@ -58,7 +58,7 @@        , HUnit                == 1.2.* -      , tamarin-prover-utils == 0.8.*+      , tamarin-prover-utils >= 0.8.1   && < 0.9       hs-source-dirs: src