tamarin-prover-theory 0.8.4.0 → 0.8.5.0

raw patch · 4 files changed

+48/−37 lines, 4 filesdep ~HUnitdep ~arraydep ~bytestring

Dependency ranges changed: HUnit, array, bytestring, containers, deepseq, directory, dlist, fclabels, filepath, mtl, parallel, process, syb, tamarin-prover-term, tamarin-prover-utils, time, transformers

src/Theory/Constraint/System.hs view

@@ -140,6 +140,18 @@     show UntypedCaseDist = "untyped"     show TypedCaseDist   = "typed" +-- Adapted from the output of 'derive'.+instance Read CaseDistKind where+        readsPrec p0 r+          = readParen (p0 > 10)+              (\ r0 ->+                 [(UntypedCaseDist, r1) | ("untyped", r1) <- lex r0])+              r+              +++              readParen (p0 > 10)+                (\ r0 -> [(TypedCaseDist, r1) | ("typed", r1) <- lex r0])+                r+ instance Ord CaseDistKind where     compare UntypedCaseDist UntypedCaseDist = EQ     compare UntypedCaseDist TypedCaseDist   = LT

src/Theory/Text/Parser.hs view

@@ -47,7 +47,8 @@  -- | Parse a security protocol theory file. parseOpenTheory :: [String] -- ^ Defined flags-                -> FilePath -> IO OpenTheory+                -> FilePath+                -> IO OpenTheory parseOpenTheory flags = parseFile (theory flags)  -- | Parse DH intruder rules.@@ -57,11 +58,11 @@ -- | Parse a security protocol theory from a string. parseOpenTheoryString :: [String]  -- ^ Defined flags.                       -> String -> Either ParseError OpenTheory-parseOpenTheoryString flags = parseFromString (theory flags)+parseOpenTheoryString flags = parseString "<unknown source>" (theory flags)  -- | Parse a lemma for an open theory from a string. parseLemma :: String -> Either ParseError (Lemma ProofSkeleton)-parseLemma = parseFromString lemma+parseLemma = parseString "<unknown source>" lemma  ------------------------------------------------------------------------------ -- Parsing Terms

src/Theory/Text/Parser/Token.hs view

@@ -81,7 +81,7 @@     -- * Basic Parsing   , Parser   , parseFile-  , parseFromString+  , parseString   ) where  import           Prelude             hiding (id, (.))@@ -99,10 +99,6 @@ import           Theory  ---- ------------------------------------------------------------------------------ -- Parser ------------------------------------------------------------------------------@@ -129,20 +125,22 @@       , T.caseSensitive  = True       } --- | Parse a file.+-- | Run a parser on the contents of a file. parseFile :: Parser a -> FilePath -> IO a-parseFile parser f = do-  s <- readFile f-  case runParser (T.whiteSpace spthy *> parser) minimalMaudeSig f s of-    Right p -> return p-    Left err -> error $ show err+parseFile parser inFile = do+    inp <- readFile inFile+    case parseString inFile parser inp of+        Right x  -> return x+        Left err -> error $ show err  -- | Run a given parser on a given string.-parseFromString :: Parser a -> String -> Either ParseError a-parseFromString parser =-    runParser (T.whiteSpace spthy *> parser) minimalMaudeSig dummySource-  where-    dummySource = "<interactive>"+parseString :: FilePath+            -- ^ Description of the source file. (For error reporting.)"+            -> Parser a+            -> String         -- ^ Input string.+            -> Either ParseError a+parseString srcDesc parser =+    runParser (T.whiteSpace spthy *> parser) minimalMaudeSig srcDesc   -- Token parsers

tamarin-prover-theory.cabal view

@@ -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@@ -38,30 +38,30 @@      build-depends:         base              == 4.*-      , bytestring        == 0.9.*-      , deepseq           == 1.3.*-      , array             >= 0.3   && < 0.5-      , containers        >= 0.4.2 && < 0.5-      , dlist             == 0.5.*-      , mtl               == 2.0.*+      , bytestring        >= 0.9+      , deepseq           >= 1.3+      , array             >= 0.3  +      , containers        >= 0.4.2+      , dlist             >= 0.5+      , mtl               >= 2.1       , cmdargs           == 0.10.*-      , filepath          >= 1.1   && < 1.4-      , directory         >= 1.0   && < 1.2-      , process           == 1.1.*+      , filepath          >= 1.1+      , directory         >= 1.0+      , process           >= 1.1       , parsec            == 3.1.*       , safe              >= 0.2  && < 0.4-      , transformers      == 0.2.*-      , fclabels          == 1.1.*+      , transformers      >= 0.3+      , fclabels          == 1.*       , uniplate          == 1.6.*-      , syb               == 0.3.* && >= 0.3.3+      , syb               >= 0.3.3       , binary            == 0.5.*       , derive            == 2.5.*-      , time              >= 1.2   && < 1.5-      , parallel          == 3.2.*-      , HUnit             == 1.2.*+      , time              >= 1.2 +      , parallel          >= 3.2+      , HUnit             >= 1.2 -      , tamarin-prover-utils >= 0.8.4  && < 0.9-      , tamarin-prover-term  >= 0.8.4  && < 0.9+      , tamarin-prover-utils >= 0.8.5  && < 0.9+      , tamarin-prover-term  >= 0.8.5  && < 0.9       hs-source-dirs: src