- Haskell-Cafe - Haskell.org

Re: [Haskell-cafe] ANN: CPSA - Cryptographic Protocol Shapes Analyzer
by John D. Ramsdell 28 Apr '10

28 Apr '10

>> We are working towards a version of CPSA with the property that >> whenever it successfully terminates, every possible execution is >> described by its output. However, the current implementation >> occasionally fails to find some executions. > > That is concerning - is it due to ... We have formally specified the algorithm, but we haven't been able to prove the algorithm finds all solutions. In fact, we now have an example in the test suite that shows it misses an answer. The example is in the source distribution in tst/missing-contraction.scm. There should be two answers, but CPSA only finds one. We have a fix you can try out in 2.0.4. In src/CPSA/Lib/Strand.hs, you can change the flag useDisplacement from False to True, and CPSA will find both answers. We don't know if this fix is all one needs to ensure CPSA finds every answer. By the way, the algorithm is in doc/cpsaspec.pdf, which can be build from a source distribution of CPSA. > What is the current status of development both wrt openness and future direction? Our highest priority is to resolve the correctness issue you just raised. As for openness, the sources are available to you. We haven't thought about other forms of openness. > I'm wondering if you plan to add MQV or other non-trivial primitives. I don't know what MQV is, so I can't say. Thanks for your interest, Thomas. John

1 0

Lazy Parsing (ANN: vcd-0.1.4)
by Tom Hawkins 28 Apr '10

28 Apr '10

I had been using Parsec to parse VCD files, but needed to lazily parse streaming data. After stumbling on this thread below, I switch to polyparse. What a great library! I was able to migrate from a strict to a semi-lazy parser and many of my parse reductions didn't even need to change. Thanks Malcolm! In addition to lazy VCD parsing, this version of vcd [1] also includes step', which forces a step regardless if variables have changed or not -- helpful for realtime simulation. (BTW, parsec is a great library too.) -Tom [1] http://hackage.haskell.org/package/vcd-0.1.4 On Sun, May 31, 2009 at 6:41 AM, Malcolm Wallace <malcolm.wallace(a)cs.york.ac.uk> wrote: > > I don't know whether you will be willing to change over to polyparse > library, but here are some hints about how you might use it. > > Given that you want the input to be a simple character stream, rather than > use a more elaborate lexer, the first thing to do is to specialise the > parser type for your purposes: > >> type TextParser a = Parser Char a > > Now, to recognise a "mere digit", > >> digit :: TextParser Char >> digit = satisfy Char.isDigit > > and for a sequence of digits forming an unsigned integer: > >> integer :: TextParser Integer >> integer = do ds <- many1 digit >> return (foldl1 (\n d-> n*10+d) >> (map (fromIntegral.digitToInt) ds)) >> `adjustErr` (++("expected one or more digits")) > >> I mean I'd like to be able to turn "12.05.2009" into something like (12, >> 5, 2009) and got no clue what the code would have to look like. I do know >> almost every variation what the code must not look like :). > >> date = do a <- integer >> satisfy (=='.') >> b <- integer >> satisfy (=='.') >> c <- integer >> return (a,b,c) > > Of course, that is just the standard (strict) monadic interface used by many > combinator libraries. Your original desire was for lazy parsing, and to > achieve that, you must move over to the applicative interface. The key > difference is that you cannot name intermediate values, but must construct > larger values directly from smaller ones by something like function > application. > >> lazydate = return (,,) `apply` integer `discard` dot >> `apply` integer `discard` dot >> `apply` integer >> where dot = satisfy (=='.') > > The (,,) is the constructor function for triples. The `discard` combinator > ensures that its second argument parses OK, but throws away its result, > keeping only the result of its first argument. > > Apart from lazy space behaviour, the main observable difference between > "date" and "lazydate" is when errors are reported on incorrect input. For > instance: > > > fst $ runParser date "12.05..2009" > *** Exception: In a sequence: > Parse.satisfy: failed > expected one or more digits > > > fst $ runParser lazydate "12.05..2009" > (12,5,*** Exception: In a sequence: > Parse.satisfy: failed > expected one or more digits > > Notice how the lazy parser managed to build the first two elements of the > triple, whilst the strict parser gave no value at all. > > I know that the error messages shown here are not entirely satisfactory, but > they can be improved significantly just by making greater use of the > `adjustErr` combinator in lots more places (it is rather like Parsec's <?>). > Errors containing positional information about the input can be constructed > by introducing a separate lexical tokenizer, which is also not difficult. > > Regards, > Malcolm > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe(a)haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe >

3 4

Control.Exception try and catch
by Mads Lindstrøm 28 Apr '10

28 Apr '10

Hi From http://haskell.org/ghc/docs/6.12.1/html/libraries/base-4.2.0.0/Control-Exce… "... The difference between using try and catch for recovery is that in catch the handler is inside an implicit block (see "Asynchronous Exceptions") which is important when catching asynchronous exceptions ..." However, 'try' is implemented by calling catch http://haskell.org/ghc/docs/6.12.1/html/libraries/base-4.2.0.0/src/Control-…: try :: Exception e => IO a -> IO (Either e a) try a = catch (a >>= \ v -> return (Right v)) (\e -> return (Left e)) Thus, I wonder, why do 'try' not "inherit" the implicit block mentioned above? Looking at catch: catch :: Exception e => IO a -- ^ The computation to run -> (e -> IO a) -- ^ Handler to invoke if an exception is raised -> IO a catch io h = H'98.catch io (h . fromJust . fromException . toException) I see no call to 'block'. But maybe it is hidden in H'98.catch? And is H'98.catch == Prelude.catch ? /Mads

2 1

Broken ghc documentation links
by haskell＠kudling.de 28 Apr '10

28 Apr '10

To reproduce: 1) Look for "data IO" on Hoogle, e.g. http://haskell.org/ghc/docs/6.12.1/html/libraries/base-4.2.0.0/Prelude.html… 2) Click "source", which redirects to http://haskell.org/ghc/docs/6.12.1/html/libraries/base-4.2.0.0/src/GHC-Type… 3) Observe a "Not Found" page Is there anyone interested in fixing this? Bye, Lenny

4 5

Seeking the correct quote
by Jacques Carette 28 Apr '10

28 Apr '10

I have heard generic programming described tongue-in-cheek as "the kind of polymorphism that a language does not (yet) have". I find this description rather apt, and it matches fairly what I see called 'generic' in various communities. But who said this, where and when? Jacques

3 5

Is XHT a good tool for parsing web pages?
by John Creighton 28 Apr '10

28 Apr '10

> Subject: Is XHT a good tool for parsing web pages? > I looked a little bit at XHT and it seems very elegant for writing > concise definitions of parsers by forms but I read that it fails if > the XML isn't strict and I know a lot of web pages don't use strict > XHTML. Therefore I wonder if it is an appropriate tool for web pages. > >

5 5

Getting used and available memory
by Mads Lindstrøm 28 Apr '10

28 Apr '10

Hi I have tried haskell.org, Google and Hoolge, but I cannot find any function to give me the available and/or used memory of a Haskell program. Is it just not there? Or am I missing it somehow? /Mads

4 5

happstack/SOAP
by Johannes Waldmann 28 Apr '10

28 Apr '10

Hi - I'm looking for an example/demo happstack server that handles SOAP requests. - Thanks, J.W.

2 1

A newbie question ?
by zaxis 28 Apr '10

28 Apr '10

newtype TypeMap = TypeMap (Map.Map TypeRep Dynamic) lookup :: Typeable a => TypeMap -> Maybe a lookup (TypeMap mp) = res where res = liftM (fromJust . fromDynamic) $ Map.lookup (typeOf $ fromJust res) mp It seems that the `res` in `fromJust res` has not been defined ? Sincerely! ----- fac n = let { f = foldr (*) 1 [1..n] } in f -- View this message in context: http://old.nabble.com/A-newbie-question---tp28383563p28383563.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

3 3

mtl design (was ``What do _you_ want to see in FGL?'')
by Bradford Larsen 28 Apr '10

28 Apr '10

On Mon, Apr 26, 2010 at 7:35 AM, Ivan Lazar Miljenovic <ivan.miljenovic(a)gmail.com> wrote: > Whilst freezing it is an option, I feel that this will lead to the same > problems that we already face with mtl: most people agree/know that the > approach/design is bad, but we keep using it because there's no (one) > viable alternative to be used (and thus mtl stays in the Platform, which > means more people use it, and thus we have this vicious cycle). Ivan, Could you elaborate on what you mean regarding the mtl approach & design? What makes them bad? Sincerely, Brad

2 1