packages feed

opentheory-parser 1.117 → 1.160

raw patch · 6 files changed

Files

Setup.hs view
@@ -1,4 +1,4 @@-module Main(main)+module Main ( main ) where  import Distribution.Simple
opentheory-parser.cabal view
@@ -1,43 +1,37 @@ name: opentheory-parser-version: 1.117+version: 1.160 category: Parsing synopsis: Stream parsers license: MIT license-file: LICENSE-cabal-version: >= 1.8.0.6+cabal-version: >= 1.8.0.2 build-type: Simple author: Joe Leslie-Hurd <joe@gilith.com> maintainer: Joe Leslie-Hurd <joe@gilith.com>+homepage: http://opentheory.gilith.com/?pkg=parser description:-  Stream parsers - automatically generated from the opentheory package-  haskell-parser-1.117+  Stream parsers - this package was automatically generated from the+  OpenTheory package parser-1.160  library   build-depends:     base >= 4.0 && < 5.0,-    random >= 1.0.1.1 && < 2.0,     QuickCheck >= 2.4.0.1 && < 3.0,-    opentheory-primitive >= 1.0 && < 2.0,-    opentheory >= 1.73 && <= 1.76-+    opentheory-primitive >= 1.6 && < 2.0,+    opentheory >= 1.195 && < 1.201   hs-source-dirs: src-   ghc-options: -Wall-   exposed-modules:-    OpenTheory.Parser+    OpenTheory.Parser,     OpenTheory.Parser.Stream -executable opentheory-parser-test+test-suite opentheory-parser-test+  type: exitcode-stdio-1.0   build-depends:     base >= 4.0 && < 5.0,-    random >= 1.0.1.1 && < 2.0,     QuickCheck >= 2.4.0.1 && < 3.0,-    opentheory-primitive >= 1.0 && < 2.0,-    opentheory >= 1.73 && <= 1.76--  hs-source-dirs: src, testsrc-+    opentheory-primitive >= 1.6 && < 2.0,+    opentheory >= 1.195 && < 1.201+  hs-source-dirs: src   ghc-options: -Wall-   main-is: Test.hs
src/OpenTheory/Parser.hs view
@@ -7,72 +7,111 @@ stability: provisional portability: portable -}+ module OpenTheory.Parser where  import qualified OpenTheory.Parser.Stream as Stream+import qualified OpenTheory.Primitive.Natural as Natural  newtype Parser a b =   Parser { unParser :: a -> Stream.Stream a -> Maybe (b, Stream.Stream a) } -partialMap :: (b -> Maybe c) -> Parser a b -> Parser a c-partialMap f p =-  Parser pf+token :: (a -> Maybe b) -> Parser a b+token f =+  Parser prs   where-  {-pf :: a -> Stream.Stream a -> Maybe (c, Stream.Stream a)-}-    pf a s =-      case unParser p a s of+  {-prs :: a -> Stream.Stream a -> Maybe (b, Stream.Stream a)-}+    prs x xs =+      case f x of         Nothing -> Nothing-        Just (b, s') ->-          case f b of-            Nothing -> Nothing-            Just c -> Just (c, s')+        Just y -> Just (y, xs) -map :: (b -> c) -> Parser a b -> Parser a c-map f p = partialMap (\b -> Just (f b)) p+some :: (a -> Bool) -> Parser a a+some p = token (\x -> if p x then Just x else Nothing) -parse :: Parser a b -> Stream.Stream a -> Maybe (b, Stream.Stream a)-parse _ Stream.Error = Nothing-parse _ Stream.Eof = Nothing-parse p (Stream.Cons a s) = unParser p a s+anyToken :: Parser a a+anyToken = some (const True) -parseAll :: Parser a a-parseAll =-  Parser pa+apply :: Parser a b -> Stream.Stream a -> Maybe (b, Stream.Stream a)+apply _ Stream.Error = Nothing+apply _ Stream.Eof = Nothing+apply p (Stream.Cons x xs) = unParser p x xs++mapPartial :: Parser a b -> (b -> Maybe c) -> Parser a c+mapPartial p f =+  Parser prs   where-  {-pa :: a -> Stream.Stream a -> Maybe (a, Stream.Stream a)-}-    pa a s = Just (a, s)+  {-prs :: a -> Stream.Stream a -> Maybe (c, Stream.Stream a)-}+    prs x xs =+      case unParser p x xs of+        Nothing -> Nothing+        Just (y, ys) ->+          case f y of+            Nothing -> Nothing+            Just z -> Just (z, ys) -parseNone :: Parser a b-parseNone =-  Parser pn+filterParser :: Parser a b -> (b -> Bool) -> Parser a b+filterParser p f = mapPartial p (\x -> if f x then Just x else Nothing)++fold :: (a -> c -> Maybe (Either b c)) -> c -> Parser a b+fold f =+  Parser . prs   where-  {-pn :: a -> Stream.Stream a -> Maybe (b, Stream.Stream a)-}-    pn _ _ = Nothing+  {-prs :: c -> a -> Stream.Stream a -> Maybe (b, Stream.Stream a)-}+    prs s x xs =+      case f x s of+        Nothing -> Nothing+        Just y ->+          case y of+            Left z -> Just (z, xs)+            Right t ->+              case xs of+                Stream.Error -> Nothing+                Stream.Eof -> Nothing+                Stream.Cons z zs -> prs t z zs -parseOption :: (a -> Maybe b) -> Parser a b-parseOption f = partialMap f parseAll+foldN :: (a -> b -> Maybe b) -> Natural.Natural -> b -> Parser a b+foldN f n s =+  fold+    (\x (m, t) ->+       fmap (\u -> if m == 0 then Left u else Right (m - 1, u)) (f x t))+    (n, s) -parsePair :: Parser a b -> Parser a c -> Parser a (b, c)-parsePair pb pc =-  Parser pbc+mapParser :: Parser a b -> (b -> c) -> Parser a c+mapParser p f = mapPartial p (\x -> Just (f x))++none :: Parser a b+none = token (const Nothing)++orelse :: Parser a b -> Parser a b -> Parser a b+orelse p1 p2 =+  Parser prs   where-  {-pbc :: a -> Stream.Stream a -> Maybe ((b, c), Stream.Stream a)-}-    pbc a s =-      case unParser pb a s of+  {-prs :: a -> Stream.Stream a -> Maybe (b, Stream.Stream a)-}+    prs x xs =+      case unParser p1 x xs of+        Nothing -> unParser p2 x xs+        Just yys -> Just yys++sequenceParser :: Parser a (Parser a b) -> Parser a b+sequenceParser p =+  Parser prs+  where+  {-prs :: a -> Stream.Stream a -> Maybe (b, Stream.Stream a)-}+    prs x xs =+      case unParser p x xs of         Nothing -> Nothing-        Just (b, s') ->-          case parse pc s' of-            Nothing -> Nothing-            Just (c, s'') -> Just ((b, c), s'')+        Just (q, ys) -> apply q ys -parseSome :: (a -> Bool) -> Parser a a-parseSome p = parseOption (\a -> if p a then Just a else Nothing)+pair :: Parser a b -> Parser a c -> Parser a (b, c)+pair p1 p2 =+  sequenceParser (mapParser p1 (\x -> mapParser p2 (\y -> (x, y)))) -parseStream :: Parser a b -> Stream.Stream a -> Stream.Stream b-parseStream _ Stream.Error = Stream.Error-parseStream _ Stream.Eof = Stream.Eof-parseStream p (Stream.Cons a s) =-  case unParser p a s of+parse :: Parser a b -> Stream.Stream a -> Stream.Stream b+parse _ Stream.Error = Stream.Error+parse _ Stream.Eof = Stream.Eof+parse p (Stream.Cons x xs) =+  case unParser p x xs of     Nothing -> Stream.Error-    Just (b, s') -> Stream.Cons b (parseStream p s')+    Just (y, ys) -> Stream.Cons y (parse p ys)
src/OpenTheory/Parser/Stream.hs view
@@ -7,42 +7,42 @@ stability: provisional portability: portable -}+ module OpenTheory.Parser.Stream where -import qualified OpenTheory.Data.List.Geometric as Data.List.Geometric-import qualified OpenTheory.Primitive.Natural as Primitive.Natural-import qualified OpenTheory.Primitive.Random as Primitive.Random+import qualified OpenTheory.Primitive.Natural as Natural+import qualified Test.QuickCheck as QuickCheck  data Stream a =     Error   | Eof   | Cons a (Stream a)+  deriving (Eq, Ord, Show)  append :: [a] -> Stream a -> Stream a-append [] s = s-append (h : t) s = Cons h (append t s)+append [] xs = xs+append (h : t) xs = Cons h (append t xs)  fromList :: [a] -> Stream a fromList l = append l Eof -fromRandom ::-  (Primitive.Random.Random -> (a, Primitive.Random.Random)) ->-    Primitive.Random.Random -> (Stream a, Primitive.Random.Random)-fromRandom d r =-  let (l, r') = Data.List.Geometric.fromRandom d r in-  let (b, r'') = Primitive.Random.bit r' in-  (append l (if b then Error else Eof), r'')+lengthStream :: Stream a -> Natural.Natural+lengthStream Error = 0+lengthStream Eof = 0+lengthStream (Cons _ xs) = lengthStream xs + 1 -size :: Stream a -> Primitive.Natural.Natural-size Error = 0-size Eof = 0-size (Cons _ s) = size s + 1+mapStream :: (a -> b) -> Stream a -> Stream b+mapStream _ Error = Error+mapStream _ Eof = Eof+mapStream f (Cons x xs) = Cons (f x) (mapStream f xs) -toList :: Stream a -> Maybe [a]-toList Error = Nothing-toList Eof = Just []-toList (Cons a s) =-  case toList s of-    Nothing -> Nothing-    Just l -> Just (a : l)+toList :: Stream a -> ([a], Bool)+toList Error = ([], True)+toList Eof = ([], False)+toList (Cons x xs) = let (l, e) = toList xs in (x : l, e)++instance QuickCheck.Arbitrary a => QuickCheck.Arbitrary (Stream a) where+  arbitrary =+    fmap (\(l, b) -> append l (if b then Error else Eof))+      QuickCheck.arbitrary
+ src/Test.hs view
@@ -0,0 +1,29 @@+{- |+module: Main+description: Stream parsers - testing+license: MIT++maintainer: Joe Leslie-Hurd <joe@gilith.com>+stability: provisional+portability: portable+-}+module Main+  ( main )+where++import qualified OpenTheory.List as List+import qualified OpenTheory.Parser.Stream as Stream+import OpenTheory.Primitive.Test++proposition0 :: [Bool] -> Bool+proposition0 l = Stream.toList (Stream.fromList l) == (l, False)++proposition1 :: Stream.Stream Bool -> Bool+proposition1 xs =+  Stream.lengthStream xs == List.naturalLength (fst (Stream.toList xs))++main :: IO ()+main =+    do check "Proposition 0:\n  !l. toList (fromList l) = (l, F)\n  " proposition0+       check "Proposition 1:\n  !xs. length xs = length (fst (toList xs))\n  " proposition1+       return ()
− testsrc/Test.hs 
@@ -1,68 +0,0 @@-{- |-module: Main-description: Stream parsers - testing-license: MIT--maintainer: Joe Leslie-Hurd <joe@gilith.com>-stability: provisional-portability: portable--}-module Main-  ( main )-where--import qualified OpenTheory.Data.List as Data.List-import qualified OpenTheory.Data.List.Geometric as Data.List.Geometric-import qualified OpenTheory.Data.Option as Data.Option-import qualified OpenTheory.Number.Natural as Number.Natural-import qualified OpenTheory.Parser.Stream as Parser.Stream-import qualified OpenTheory.Primitive.Random as Primitive.Random-import qualified OpenTheory.Primitive.Test as Primitive.Test--proposition0 :: Primitive.Random.Random -> Bool-proposition0 r =-  let (l, _) =-        Data.List.Geometric.fromRandom Number.Natural.fromRandom r in-  Parser.Stream.size (Parser.Stream.fromList l) == Data.List.length' l--proposition1 :: Primitive.Random.Random -> Bool-proposition1 r =-  let (l, _) =-        Data.List.Geometric.fromRandom Number.Natural.fromRandom r in-  Data.Option.equal (Data.List.equal (==))-    (Parser.Stream.toList (Parser.Stream.fromList l)) (Just l)--proposition2 :: Primitive.Random.Random -> Bool-proposition2 r =-  let (s, _) = Parser.Stream.fromRandom Number.Natural.fromRandom r in-  case Parser.Stream.toList s of-    Nothing -> True-    Just l -> Data.List.length' l == Parser.Stream.size s--proposition3 :: Primitive.Random.Random -> Bool-proposition3 r =-  let (l, r') =-        Data.List.Geometric.fromRandom Number.Natural.fromRandom r in-  let (s, _) = Parser.Stream.fromRandom Number.Natural.fromRandom r' in-  Parser.Stream.size (Parser.Stream.append l s) ==-  Data.List.length' l + Parser.Stream.size s--proposition4 :: Primitive.Random.Random -> Bool-proposition4 r =-  let (l, r') =-        Data.List.Geometric.fromRandom Number.Natural.fromRandom r in-  let (s, _) = Parser.Stream.fromRandom Number.Natural.fromRandom r' in-  Data.Option.equal (Data.List.equal (==))-    (Parser.Stream.toList (Parser.Stream.append l s))-    (case Parser.Stream.toList s of-       Nothing -> Nothing-       Just ls -> Just (l ++ ls))--main :: IO ()-main =-    do Primitive.Test.check "Proposition 0:\n  !r.\n    let (l, r') <- H.Geometric.fromRandom H.fromRandom r in\n    H.Stream.size (H.Stream.fromList l) = H.length' l\n  " proposition0-       Primitive.Test.check "Proposition 1:\n  !r.\n    let (l, r') <- H.Geometric.fromRandom H.fromRandom r in\n    H.equal (H.equal (=)) (H.Stream.toList (H.Stream.fromList l)) (some l)\n  " proposition1-       Primitive.Test.check "Proposition 2:\n  !r.\n    let (s, r') <- H.Stream.fromRandom H.fromRandom r in\n    case H.Stream.toList s of\n      none -> T\n    | some l -> H.length' l = H.Stream.size s\n  " proposition2-       Primitive.Test.check "Proposition 3:\n  !r.\n    let (l, r') <- H.Geometric.fromRandom H.fromRandom r in\n    let (s, r'') <- H.Stream.fromRandom H.fromRandom r' in\n    H.Stream.size (H.Stream.append l s) = H.length' l + H.Stream.size s\n  " proposition3-       Primitive.Test.check "Proposition 4:\n  !r.\n    let (l, r') <- H.Geometric.fromRandom H.fromRandom r in\n    let (s, r'') <- H.Stream.fromRandom H.fromRandom r' in\n    H.equal (H.equal (=)) (H.Stream.toList (H.Stream.append l s))\n      (case H.Stream.toList s of none -> none | some ls -> some (l @ ls))\n  " proposition4-       return ()