February 2011 - Haskell-Cafe

problem with instance method
by Patrick Browne 03 Feb '11

03 Feb '11

Hi, I am studying type classes using examples from the literature [1]. The attached code is a formalization of basic object oriented ideas. The particular approach seems to be built on the concepts of: thing, object, and identifier. I have no intension to implement anything or significantly change the code below. Rather, I am trying to understand the code as it stands. I include a number of test runs which seem OK, but I cannot get the *obj* function to work. obj :: t -> i -> o t i obj t i = Obj t i Any hints would be appreciated. Thanks, Pat [1] ftp://ftp.geoinfo.tuwien.ac.at/frank/frank97executableAxiomaticSpecification.pdf -- A property of a thing data Color = Blue | Green | Red | White deriving Show -- A thing class Cars c where car :: Color -> c getColor :: c -> Color putColor :: Color -> c -> c paint :: Color -> c -> c paint color car = putColor color car data Car = Car Color deriving Show instance Cars Car where car c = Car c putColor color (Car c) = Car color getColor (Car c) = c -- Identifiers for objects class (Integral i) => IDs i where startId :: i newId :: i -> i newId i = succ i sameId, notSameId :: i -> i -> Bool sameId i j = i == j notSameId i j = not (sameId i j) instance IDs Integer where startId = 1 -- Objects consist of Things, with Identifiers class (IDs i, Show i) => Objects o t i where obj :: t -> i -> o t i getId :: o t i -> i getThing :: o t i -> t doThing :: (t -> t) -> o t i -> o t i doThing f o = obj (f (getThing o)) (getId o) same :: o t i -> o t i -> Bool same i j = sameId (getId i) (getId j) isId :: i -> o t i -> Bool isId i o = sameId i (getId o) -- A general type of Obj data Object t i = Obj t i deriving Show -- A particular Car Obj, which an instance of Objects class (in Haskell terms, not OO terms) instance Objects Object Car Integer where obj t i = Obj t i getId (Obj t i) = i getThing (Obj t i) = t -- Create some actual Objects x = (Obj (Car Blue) (startId::Integer)) y = (Obj (Car Green) (newId startId::Integer)) -- Some tests on car thing, seem OK -- getColor (Car Blue) -- putColor Green (Car Blue) -- getColor (putColor Green (Car Blue)) -- Some tests on objects, seem OK -- same x y -- Obj (Car Blue) (newId startId::Integer) -- Obj (Car Blue) (startId::Integer) -- getThing (Obj (Car Blue) (startId::Integer)) -- getId (Obj (Car Blue) (startId::Integer)) -- isId 2 (Obj (Car Blue) (startId::Integer)) This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie

3 2

Re: [Haskell-cafe] Inheritance and Wrappers
by John Lato 03 Feb '11

03 Feb '11

> > From: Steffen Schuldenzucker <sschuldenzucker(a)uni-bonn.de> > > On 01/31/2011 08:58 PM, MattMan wrote: > > [...] > > > > data Wrapper a = Wrap a > > instance (Num a) => AbGroup (Wrapper a) where > > add (Wrap i) (Wrap j) = Wrap(i+j) > > > > However, this is clumsy. Is there something else I can do? Thanks > This is the normal approach. You can do funny things with the > OverlappingInstances extension, but it is probably not what you want. > > The problem is that the compiler only considers the heads of the > instance declarations when determining which instance to use for a > specific type. So an instance like this: > > > instance (Num a) => AbGroup a where ... > > means: Some type matching 'a' (that is, any type) is an instance of > 'AbGroup' if and only if it is an instance of 'Num'. > I would word this differently. I would say this instance means: Some type matching 'a' (that is, any type) is an instance of 'AbGroup'. It is an error to use AbGroup methods if 'a' does not have a Num instance in scope. The important point is that this declares an AbGroup instance for every type, not just types with Num instances. Which means that this instance is much less useful than you would hope. I would probably use either Henning's approach of separate functions or an automatic deriving mechanism. I've never understood why Haskellers are so averse to writing new instances anyway. John

5 8

Haskell procedure
by Houdini 03 Feb '11

03 Feb '11

One :Thank you Carsten Schultz,Daniel Fischer,Mihai and all the other for your help. Two:After my last post I wrote some function that should help me in the future,but I need some help with the followint as I'm tired and have to fit in a schedule.I know it is long so I'll try and explain it as short and consice as I can. The DPLL procedure has two main stages: a simplification stage and a search stage. In the simplification stage, functions are applied to the formula to assign truth values to certain propositional variables. The simplifications are made because if there is a satisfying assignment for the simplified formula then it is also a satisfying assignment for the original formula. This reduces the need for search which can take a long time. The search stage is performed when no more simplifications can be made. In this stage a literal is chosen and is assigned true or false leading to two new branches in the search space. I wrote some function wich should be helpfull,but I have to fit in a schedule and I'm getting tired I need some additional help if possible. module Algorithm where import System.Random import Data.Maybe import Data.List type Atom = String type Literal = (Bool,Atom) type Clause = [Literal] type Formula = [Clause] type Model = [(Atom, Bool)] type Node = (Formula, ([Atom], Model)) -- This function takess a Clause and return the set of Atoms of that Clause. atomsClause :: Clause -> [Atom] -- This function takes a Formula returns the set of Atoms of a Formula atoms :: Formula -> [Atom] -- This function returns True if the given Literal can be found within -- the Clause. isLiteral :: Literal -> Clause -> Bool -- this function takes a Model and an Atom and flip the truthvalue of -- the atom in the model flipSymbol :: Model -> Atom -> Model -- is this ok? Additional functions that I wrote: remove :: (Eq a) )a ->[a] ->[a] -This function removes an item from a list. neg :: Literal->Literal -This function flips a literal (ie. from P to :P and from :P to P). falseClause :: Model -> Clause -> Bool -This function takes a Model and a Clause and returns True if the clause is unsatisfied by the model or False otherwise. falseClauses :: Formula -> Model -> [Clause] -This function takes a Formula and a Model and returns the list of clauses of the formula that are not satisfied. assignModel :: Model -> Formula -> Formula -This function applies the assign function for all the assignments of a given model. checkFormula :: Formula -> Maybe Bool This function checks whether a formula can be decided to be satisfiable or unsatisfiable based on the effects of the assign function. satisfies :: Model -> Formula -. Bool This function checks whether a model satisfies a formula. This is done with the combination of the assignModel and checkFormula functions. --Where do I need help: removeTautologies :: Formula->Formula This function should output a simplified formula if tautologies can be found in one or more clauses in the input Notes: If in a clause, a literal and its negation are found, it means that the clause will be true, regardless of the value finally assigned to that propositional variable. Consider the following example: (A v B v -A) ^ (B v C v A) The first clause contains the literals A and -A. This means that the clause will always be true, in which case it can be simplify the whole set to simply (B v C v A) (the second clause alone) pureLiteralDeletion :: Formula->Formula This function is suppose to implement a simplification step that assumes as true any atom in a formula that appears exclusively in a positive or negative form (not both). Consider the formula: (P v Q v R) ^ (P v Q v -R) ^ (-Q v R) Note that in this formula P is present but -P is not. Using Pure Literal Deletion it can be assumed that the value of P will be True thus simplifying the formula to (-Q v R). If the literal were false then the literal would simply be deleted from the clauses it appears in. In that case any satisfying model for the resulting formula would also be a satisfying model for the formula when we assume that the literal is true. Hence this simplification is sound in that if there is a solution to the simplified formula then there is a solution to the original formula. propagateUnits :: Formula->Formula If a clause in a propositional formula contains only one literal, then that literal must be true (so that the particular clause can be satisfied). When this happens,we can remove the unit clauses (the ones that contain only one literal), all the clauses where the literal appears and also, from the remaining clauses, we can delete the negation of the literal (because if P is true, -P will be false).For example, in the formula (P v Q v R) ^ (-P v Q v -R) ^ (P) we have one unit clause (the third clause(P) ). Because this one has to be true for the whole formula to be true we assign True to P and try to find a satisfying assignment for the remaining formula. Finally because -P cannot be true (given the assigned value of P) then the second clause is reduced by eliminating the symbol -P . This simplification results in the revised formula (Q v -R). The resulting simplification can create other unit clauses. For example in the formula (-P v Q) ^ (P) is simplified to (Q) when the unit clause (P) is propagated. This makes (Q) a unit clause which can now also be simplified to give a satisfying assignment to the formula. The function should apply unit propagation until it can no longer make any further simplifications. Note that if both P and -P are unit clauses then the formula is unsatisfiable. In this case the function should return a formula with an empty clause in it to indicate that the formula could not be satisfied. update :: Node -> [Node] The update function should take in a Node and return a list of the Nodes that result from assigning True to an unassigned atom in one case and False in the other (ie. a case split). So the list returned should have two nodes as elements. One node should contain the formula with an atom assigned True and the model updated with this assignment, and the other should contain the formula with the atom assigned False and the model updated to show this. The lists of unassigned atoms of each node should also be updated accordingly. This function should use your implemented assign function to make the assignments. It should also use the chooseAtom function provided to select the literal to assign. search :: (Node -> [Node]) -> [Node] -> Int -> (Bool, Int) The search function should perform a backtracking search. The function takes the update function as input and uses it to generate nodes in the search space. The search function also takes in a list which has one element, the initial node consisting of the formula along with an initial model. It should generate nodes using the update function and check nodes using the given check function. If a node is unsatisfiable then it should abandon that branch of the search. If a node is satisfiable then a satisfying assignment has been found and so it should return True. If a node is neither satisfiable or unsatisfiable then it should generate new nodes from this node. If all possible branches of the search space have been tried, i.e. the list of nodes to try has become the empty list, then it should return False since all possible assignments have been tried. The search function also has an Int argument which should be an integer that tracks how many calls to the update function have been made. The search function should return a pair consisting of the truth value of the formula and the number of calls to update made. Thank you(because ,I'm anticipating your help),and until I get a reply I will continue to try an squize my exhausted brain. -- View this message in context: http://haskell.1045720.n5.nabble.com/Haskell-procedure-tp3369005p3369005.ht… Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

1 0

Re: [Haskell-cafe] Problems with iteratees
by oleg＠okmij.org 03 Feb '11

03 Feb '11

I agree with Maciej Wos' diagnosis and solution. I'd like to point out that the Tiff library has to do a similar processing: use an iteratee to read bytes from the outer stream and to produce elements for the inner stream (e.g., signed 32-bit integers). In your version of the Iteratee library, please look at Data/Iteratee/Codecs/Tiff.hs and search for the following fragment: -- Read the array of long integers -- of 1 element: the offset field contains the value read_value typ e' 1 | typ == TT_long || typ == TT_slong = ... -- of n elements read_value typ e' count | typ == TT_long || typ == TT_slong = do offset <- endianRead4 e' return . Just . TEN_INT $ \iter_int -> return $ do Iter.seek (fromIntegral offset) let iter = convStream (liftM (either (const Nothing) (Just . (:[]) . conv_long typ)) (checkErr (endianRead4 e'))) iter_int Iter.joinI $ Iter.joinI $ Iter.takeR (4*count) iter Of relevance is the line that contains convStream. Please notice (const Nothing) that Maciej was talking about. The newer version has a somewhat more convenient sequence_stream function, which creates a nested stream using the supplied iteratee to read from the outer stream and produce an element for the inner stream. The function is particularly useful if you read the inner stream all the way, until it is exhausted. Here is how the above read_value clause looks now -- of n elements read_value typ count | typ == TT_long || typ == TT_slong = do offset <- endian_read4 let converter = endian_read4 >>= return . conv_long typ return . Just . TEN_INT $ \iter_int -> do seek_stream (fromIntegral offset) runI =<< takeR (4*count) (sequence_stream converter iter_int)

1 0

timely shutdown of timer threads
by Warren Harris 02 Feb '11

02 Feb '11

I have an application that forks a thread to run an activity on a timer. (The activity happens to be Berkeley DB checkpointing, but that's actually beside the point here.) The problem is that when the application wants to quit, I would like my main thread to be able to tell the timer thread to shut down in a timely way. However, I don't see a primitive in haskell that allows me to both wait for a timeout, or a notification. (If I were to do this in java, I would use wait/notify.) Here's the code I wrote to attempt this shutdown procedure: import Control.Exception import Database.Berkeley.Db import Data.IORef import System.Posix.Unistd ... closeEnv :: Env -> IO () closeEnv env = do threadId <- readIORef (envCheckpointThread env) case threadId of Just tid -> killThread tid Nothing -> return () dbEnv_close [] (envDbEnv env) startCheckpointing :: Env -> IO ThreadId startCheckpointing env = do forkOS run where run = catch checkpoint handler checkpoint = checkpoint1 >> checkpoint checkpoint1 = unblock $ do let dbenv = envDbEnv env _ <- sleep checkpointInterval putStrLn "# checkpoint" dbEnv_txn_checkpoint [] dbenv 0 0 handler ThreadKilled = return () handler exn = throw exn However, there are several problems here: First, the checkpointInterval is 15 sec, so it takes at least 15 seconds for the thread to wake up and be interrupted. Second, it isn't clear to me whether the killThread call should interrupt the sleep or not. In practice, several checkpoints occur before the ThreadKilled message is delivered, and this can take up to 2 minutes to shut down. Is there a better way to do this? Suggestions would be greatly appreciated, Warren

3 5

Haskell Weekly News: Issue 167 - February 02, 2011
by Daniel Santa Cruz 02 Feb '11

02 Feb '11

Welcome to issue 167 of the HWN, a newsletter covering developments in the [1]Haskell community. This release covers the week of January 23 to 29, 2011. This week I've added a section which compiles a list of the top answers given in StackOverflow during the week. These seem to be of more interest to more experienced Haskell users than the newbie questions usually posted on the site. See what you think. Announcements R. Emre Basar [2]annouced the release of follower, a tool that allows you to follow people's tweets without having an account with Twitter. Alberto Ruiz [3]announced hmatrix version 0.11, a package for numerical computation based on LAPACK and SGL. Michael Snoyman [4]made some point updates for WAI and Warp. "They fix some documentation issues, add some status aliases, make it possible to handle exceptions more easily, and make things more responsive on Windows." Antoine Latter [5]announced a minor point release for Parsec 3.1.0. John Meacham [6]announced version 0.7.7 of jhc is out! "This release fixes a large number of bugs that cropped up when compiling haskell out in the wild as well as adds some more features. A major one being the garbage collector is enabled by default." Quotes of the Week * Twey: Maybe Bool: the Haskell equivalent to True/False/FileNotFound * elliott: Only two things in the universe are certain: Death, and two of the libraries you've decided to use taking different types of ByteString. * shapr: my personal heuristics judge Haskell as totally practical, perhaps too practical. * monochrom: the guys that I see when I look into the irc window believe that I'm just a bunch of text. * bernardh: Refactoring: spend a week to get where you were * Question: How do I use "fix", and how does it work? Answer (by TomMD): The prank answer is "fix has no real use, it's just there so you can type 'fix error' in ghci and feel good about yourself." Top Reddit Stories * Haskell at Bump Domain: devblog.bu.mp, Score: 44, Comments: 9 On Reddit: http://www.reddit.com/r/haskell/comments/f8cr8/haskell_at_bump/ Original: http://devblog.bu.mp/haskell-at-bump * How to write a simple TCP Server in Haskell Domain: catonmat.net, Score: 35, Comments: 5 On Reddit: http://www.reddit.com/r/haskell/comments/faa80/how_to_write_a_simple_tcp_se… Original: http://catonmat.net/blog/simple-haskell-tcp-server * Snap Framework article in IEEE Internet Computing Domain: steve.vinoski.net, Score: 32, Comments: 1 On Reddit: http://www.reddit.com/r/haskell/comments/fa0e0/snap_framework_article_in_ie… Original: http://steve.vinoski.net/blog/2011/01/21/column-on-the-snap-framework/ * My Dream GHCi Session, Take 2 Domain: cdsmith.wordpress.com, Score: 23, Comments: 5 On Reddit: http://www.reddit.com/r/haskell/comments/f8im5/my_dream_ghci_session_take_2/ Original: http://cdsmith.wordpress.com/2011/01/24/my-dream-ghci-session-take-2/ * Text: a visual programming language based on Haskell, demo Domain: vimeo.com, Score: 20, Comments: 3 On Reddit: http://www.reddit.com/r/haskell/comments/fbgxd/text_a_visual_programming_la… Original: http://vimeo.com/19273744 * Hoogle Embed Domain: neilmitchell.blogspot.com, Score: 16, Comments: 3 On Reddit: http://www.reddit.com/r/haskell/comments/f7iqa/hoogle_embed/ Original: http://neilmitchell.blogspot.com/2011/01/hoogle-embed.html * What does this mean for Haskell on Android? Domain: reddit.com, Score: 15, Comments: 12 On Reddit: http://www.reddit.com/r/haskell/comments/f9o67/what_does_this_mean_for_hask… Original: http://www.reddit.com/r/Android/comments/f97zh/google_not_happy_with_number… * Evolving a computer with Genprog (exercises from the TECS book) Domain: jpmoresmau.blogspot.com, Score: 13, Comments: On Reddit: http://www.reddit.com/r/haskell/comments/f7y6a/evolving_a_computer_with_gen… Original: http://jpmoresmau.blogspot.com/2011/01/evolving-computer-with-tecs-and-genp… * All about MVars : Inside T5 Domain: blog.ezyang.com, Score: 13, Comments: 4 On Reddit: http://www.reddit.com/r/haskell/comments/fduxb/all_about_mvars_inside_t5/ Original: http://blog.ezyang.com/2011/02/all-about-mvars/ * What textbooks would be useful to start approaching the low-hanging fruit on the ghc project? Domain: self.haskell, Score: 12, Comments: 8 On Reddit: http://www.reddit.com/r/haskell/comments/f8dm5/what_textbooks_would_be_usef… Original: /r/haskell/comments/f8dm5/what_textbooks_would_be_useful_to_start/ Top StackOverflow Answers * What is an idiomatic way to add lists in Haskell? Votes: 14 Read on SO: http://stackoverflow.com/questions/4776750/what-is-an-idiomatic-way-to-add-… There is a zipWith library function that combines two lists by using a supplied function. It does exactly what you want here and you get: addLists = zipWith (+) This uses (+) to combine the elements of lists given as further arguments. * Why don't the Haskell standard libraries make more use of polymorphism? Votes: 15 Read on SO: http://stackoverflow.com/questions/4779028/why-dont-the-haskell-standard-li… There is a very good pragmatic reason that "standard" Haskell (Prelude + base + maybe some more) doesn't use more polymorphism: Designing general-use type classes is hard. Good designs for classes that abstract over container types like lists, arrays and "bytestrings" (personally I don't really consider Bytestring a container) aren't floating round waiting … * How do I use fix, and how does it work? Votes: 17 Read on SO: http://stackoverflow.com/questions/4787421/how-do-i-use-fix-and-how-does-it… You are doing nothing wrong. fix id is an infinite loop. When we say that fix returns the least fixed point of a function, we mean that in the domain theory sense. So fix (\x -> 2*x-1) is not going to return 1, because although 1 is a fixed point of that function, it is not the least one in the domain ordering. I can't describe the domain ordering in … Top StackOverflow Questions * Why don't the Haskell standard libraries make more use of polymorphism? votes: 20, answers: 4 Read on SO: http://stackoverflow.com/questions/4779028/why-dont-the-haskell-standard-li… * How do I use fix, and how does it work? votes: 11, answers: 3 Read on SO: http://stackoverflow.com/questions/4787421/how-do-i-use-fix-and-how-does-it… * Why wrapping the Data.Binary.Put monad creates a memory leak? votes: 11, answers: 2 Read on SO: http://stackoverflow.com/questions/4828902/why-wrapping-the-data-binary-put… * Is there any kind of statistical natural language processing library for Haskell? votes: 9, answers: 1 Read on SO: http://stackoverflow.com/questions/4808702/is-there-any-kind-of-statistical… * How do you structure a stateful module in Haskell? votes: 8, answers: 2 Read on SO: http://stackoverflow.com/questions/4785379/how-do-you-structure-a-stateful-… About the Haskell Weekly News You can find an html version of this newsletter at my blog: http://contemplatecode.blogspot.com/2011/02/haskell-weekly-news-issue-167.h… Special thanks to Jean-Philippe Gariepy for sending in a quote for this week's quotes! We need more eyes! To help create new editions of this newsletter, please send stories to dstcruz(a)gmail.com. I'm in dire need of finding good "quotes of the week". If you happen to come across any, please don't hesitate to send it along. Until next time, Daniel Santa Cruz References 1. http://haskell.org/ 2. http://permalink.gmane.org/gmane.comp.lang.haskell.cafe/85566 3. http://permalink.gmane.org/gmane.comp.lang.haskell.cafe/85648 4. https://groups.google.com/d/topic/haskell-cafe/Yd2ADZzonSI/discussion 5. http://permalink.gmane.org/gmane.comp.lang.haskell.cafe/85761 6. https://groups.google.com/d/topic/fa.haskell/T6EM4jbhj8w/discussion

1 0

SYB: extending a generic reader with a type class
by Sugar Bzzz 02 Feb '11

02 Feb '11

Dear -cafe, Is it possible to extend a generic reader (extR / ext1R from syb) with a type class? For example, let foo :: (Integral a) => SomeMonad a I could write: reader = ... `extR` (foo :: SomeMonad Int) `extR` (foo :: SomeMonad Integer) However, that is tedious. Could I do something like reader = ... `extR` foo and have it apply to all instances of Integral? I hope I am being clear. Thank you.

2 1

Loading bitmap with xlib
by Francesco Mazzoli 02 Feb '11

02 Feb '11

I am trying to load a bitmap and display it with the Xlib bindings, but I wasn't able to find a way. The C Xlib functions would be XReadBitmapFile() of XReadBitmapFileData() to read the data, but it seems that those functions haven't been included in the haskell bindings. From http://hackage.haskell.org/packages/archive/X11/latest/doc/html/src/Graphic…: -- XCreateBitmapFromData omitted (awkward looking type) -- XReadBitmapFileData omitted (awkward looking type) Does anybody know how to do that?

3 4

Haskell DPLL
by Houdini 02 Feb '11

02 Feb '11

One :Thank you Carsten Schultz,Daniel Fischer and all the other for your help. Two:After my last post I wrote some function that should help me in the future,but I need some help with the followint as I'm tired and have to fit in a schedule.I know it is long so I'll try and explain it as short and consice as I can. The DPLL procedure has two main stages: a simplification stage and a search stage. In the simplification stage, functions are applied to the formula to assign truth values to certain propositional variables. The simplifications are made because if there is a satisfying assignment for the simplified formula then it is also a satisfying assignment for the original formula. This reduces the need for search which can take a long time. The search stage is performed when no more simplifications can be made. In this stage a literal is chosen and is assigned true or false leading to two new branches in the search space. I wrote some function wich should be helpfull,but I have to fit in a schedule and I'm getting tired I need some additional help if possible. module Algorithm where import System.Random import Data.Maybe import Data.List type Atom = String type Literal = (Bool,Atom) type Clause = [Literal] type Formula = [Clause] type Model = [(Atom, Bool)] type Node = (Formula, ([Atom], Model)) -- This function takess a Clause and return the set of Atoms of that Clause. atomsClause :: Clause -> [Atom] -- This function takes a Formula returns the set of Atoms of a Formula atoms :: Formula -> [Atom] -- This function returns True if the given Literal can be found within -- the Clause. isLiteral :: Literal -> Clause -> Bool -- this function takes a Model and an Atom and flip the truthvalue of -- the atom in the model flipSymbol :: Model -> Atom -> Model -- is this ok? Additional functions that I wrote: remove :: (Eq a) )a ->[a] ->[a] -This function removes an item from a list. neg :: Literal->Literal -This function flips a literal (ie. from P to :P and from :P to P). falseClause :: Model -> Clause -> Bool -This function takes a Model and a Clause and returns True if the clause is unsatisfied by the model or False otherwise. falseClauses :: Formula -> Model -> [Clause] -This function takes a Formula and a Model and returns the list of clauses of the formula that are not satisfied. assignModel :: Model -> Formula -> Formula -This function applies the assign function for all the assignments of a given model. checkFormula :: Formula -> Maybe Bool This function checks whether a formula can be decided to be satisfiable or unsatisfiable based on the effects of the assign function. satisfies :: Model -> Formula -. Bool This function checks whether a model satisfies a formula. This is done with the combination of the assignModel and checkFormula functions. --Where do I need help: removeTautologies :: Formula->Formula This function should output a simplified formula if tautologies can be found in one or more clauses in the input Notes: If in a clause, a literal and its negation are found, it means that the clause will be true, regardless of the value finally assigned to that propositional variable. Consider the following example: (A v B v -A) ^ (B v C v A) The first clause contains the literals A and -A. This means that the clause will always be true, in which case it can be simplify the whole set to simply (B v C v A) (the second clause alone) pureLiteralDeletion :: Formula->Formula This function is suppose to implement a simplification step that assumes as true any atom in a formula that appears exclusively in a positive or negative form (not both). Consider the formula: (P v Q v R) ^ (P v Q v -R) ^ (-Q v R) Note that in this formula P is present but -P is not. Using Pure Literal Deletion it can be assumed that the value of P will be True thus simplifying the formula to (-Q v R). If the literal were false then the literal would simply be deleted from the clauses it appears in. In that case any satisfying model for the resulting formula would also be a satisfying model for the formula when we assume that the literal is true. Hence this simplification is sound in that if there is a solution to the simplified formula then there is a solution to the original formula. propagateUnits :: Formula->Formula If a clause in a propositional formula contains only one literal, then that literal must be true (so that the particular clause can be satisfied). When this happens,we can remove the unit clauses (the ones that contain only one literal), all the clauses where the literal appears and also, from the remaining clauses, we can delete the negation of the literal (because if P is true, -P will be false).For example, in the formula (P v Q v R) ^ (-P v Q v -R) ^ (P) we have one unit clause (the third clause(P) ). Because this one has to be true for the whole formula to be true we assign True to P and try to find a satisfying assignment for the remaining formula. Finally because -P cannot be true (given the assigned value of P) then the second clause is reduced by eliminating the symbol -P . This simplification results in the revised formula (Q v -R). The resulting simplification can create other unit clauses. For example in the formula (-P v Q) ^ (P) is simplified to (Q) when the unit clause (P) is propagated. This makes (Q) a unit clause which can now also be simplified to give a satisfying assignment to the formula. The function should apply unit propagation until it can no longer make any further simplifications. Note that if both P and -P are unit clauses then the formula is unsatisfiable. In this case the function should return a formula with an empty clause in it to indicate that the formula could not be satisfied. update :: Node -> [Node] The update function should take in a Node and return a list of the Nodes that result from assigning True to an unassigned atom in one case and False in the other (ie. a case split). So the list returned should have two nodes as elements. One node should contain the formula with an atom assigned True and the model updated with this assignment, and the other should contain the formula with the atom assigned False and the model updated to show this. The lists of unassigned atoms of each node should also be updated accordingly. This function should use your implemented assign function to make the assignments. It should also use the chooseAtom function provided to select the literal to assign. search :: (Node -> [Node]) -> [Node] -> Int -> (Bool, Int) The search function should perform a backtracking search. The function takes the update function as input and uses it to generate nodes in the search space. The search function also takes in a list which has one element, the initial node consisting of the formula along with an initial model. It should generate nodes using the update function and check nodes using the given check function. If a node is unsatisfiable then it should abandon that branch of the search. If a node is satisfiable then a satisfying assignment has been found and so it should return True. If a node is neither satisfiable or unsatisfiable then it should generate new nodes from this node. If all possible branches of the search space have been tried, i.e. the list of nodes to try has become the empty list, then it should return False since all possible assignments have been tried. The search function also has an Int argument which should be an integer that tracks how many calls to the update function have been made. The search function should return a pair consisting of the truth value of the formula and the number of calls to update made. Thank you(because ,I'm anticipating your help),and until I get a reply I will continue to try an squize my exhausted brain. -- View this message in context: http://haskell.1045720.n5.nabble.com/Haskell-DPLL-tp3368123p3368123.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

1 1

Gedit Haskell mode plugin indentation
by yukkuri yu!yu!yu! 02 Feb '11

02 Feb '11

Here is my first try to write a Haskell mode layout indentation plugin for gedit - GNOME Text Editor: ftp://neverb.net/soft/mine/gedit_haskell_mode/haskell_indentation-latest.ta… Curent version: v0.4 To install the plugin 1) Create directory ~/.gnome2/gedit/plugins 2) Copy tarball/plugin/* contents to ~/.gnome2/gedit/plugins/ 3) In gedit go to Edit -> Preferences -> Plugins 4) Check the box left from "Haskell Indentation" plugin 5) (Possibly needed) Restart gedit.

1 4