Am Sonntag 20 Dezember 2009 23:25:02 schrieb Jamie Morgenstern: > Hello; > > > I am writing a parallel theorem prover using Haskell, and I am trying to > do several things. As a first cut, I want to try using the par construct to > attempt right and left rules simultaneously, and to evaluate both branches > of an and clause in parallel. My code (attached) does not seem to generate > sparks, however. When I run > > ./proposition +RTS -N2 -sstderr > > I get that no sparks are created. What am I doing wrong?
findProof ctx goal n = maybe where m1 = (tryRight ctx goal n) m2 = (tryLeft ctx goal n) m = m1 `par` m2 maybe = (m1 `mplus` m2) You never use m, so no threads are sparked. Put the par where it will actually be used: findProof ctx goal n = m2 `par` (m1 `mplus` m2) where m1 = (tryRight ctx goal n) m2 = (tryLeft ctx goal n) and you get sparks (5 (4 converted, 0 pruned)). You know that you get a pattern match error due to incomplete patterns in tryLeftHelper, though, do you? > > > Also, I was wondering if something akin to a "parallel or" exists. By this, > I mean I am looking for a function which, given x : a , y : a, returns > either, whichever computation returns first. This wouldn't be easy to reconcile with referential transparency. You can do that in IO, roughly m <- newEmptyMVar t1 <- forkIO $ method1 >>= putMVar m t2 <- forkIO $ method2 >>= putMVar m rs <- takeMVar m killThread t1 killThread t2 return rs But in pure code, I think not. > Can I use strategies to code up something like this? > I suppose this doesn't play nicely with the idea of determinism, but > thought it might be worth asking > anyway. > > Thanks, > -Jamie _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
