Parser for TUM.In.Fp.WS12.Form_8

FormHelpers.hs

{-
 - FormHelpers.hs
 -
 - Copyright (c) 2012  Julius Michaelis
 -
 - Permission to use, copy, modify, and/or distribute this software for any
 - purpose with or without fee is hereby granted, provided that the above
 - copyright notice and this permission notice appear in all copies.
 -
 - THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 - WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 - MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 - SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 - WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION
 - OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN
 - CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 -
 -}

module FormHelpers (readForm, IntCnf(IntCnf,getIntCnf), intCnfToCnf, cnfToIntCnf, reduceCnf) where

{-
 - Shortdoc:
 -
 - readForm "a b c | d ~e (f & (g h))"
 -     parses things made by show :: Form -> String
 -
 - IntCnf and getIntCnf can be used to wrap and unwrap an [[Int]]-cnf into a special type which supports:
 -
 - intCnfToCnf :: IntCnf -> Form
 - intCnfToCnf [[1],[2,-3,4]] is (x1 & ((x2 | (~x3)) | x4))
 -
 - cnfToIntCnf :: Form -> IntCnf
 - reverses intCnfToCnf
 -
 - If you want to get a hang of what the Arbitrary IntCnf instance does, try
 - import System.Random
 - import Test.QuickCheck.Gen
 - do { g <- newStdGen; return $ (unGen arbitrary g 4 :: IntCnf) }
 - Hint: It generates two kinds of CNFs
 -
 - reduceCnf maps from a cnf where all clauses contain all elements to an equivalent but shorter cnf
 - And it is slow as hell
 -
 -}

import Form_8
import Control.Monad (liftM, liftM2, mfilter, MonadPlus)
import Control.Exception
import qualified Debug.Trace (trace)
import Data.Maybe
import Data.List
import Test.QuickCheck

_warning_disable = Debug.Trace.trace
trace = flip const
--trace = Debug.Trace.trace

readForm :: String -> Form
readForm = parse_disj . check_parenthesis . annotate_depth
	where

	annotate_depth :: String -> [(Char, Int)]
	annotate_depth = ad 0
		where
		ad _ "" = []
		ad i (h:t) = (h, i + d') : ad (i + d) t
			where (d,d') = case h of { ('(') -> (1,0); (')') -> (-1,-1); (_) -> (0,0) }
	
	check_parenthesis :: [(Char, Int)] -> [(Char, Int)]
	check_parenthesis s = if last ds == 0 && all (>=0) ds then s else throw $ PatternMatchFail "Mismatched Parenthesis" -- "slight" exception misuse
		where ds = map snd s

	parse_disj :: [(Char, Int)] -> Form
	parse_disj a
		| trace ("pdisj: " ++ show a) False = undefined
		| elem ('|',0) a = 
			liftM2 (:|:) (parse_konj . fst) (parse_disj . tail . snd)
			$ break ((==)('|',0)) a
		| otherwise = parse_konj a

	parse_konj :: [(Char, Int)] -> Form
	parse_konj a
		| trace ("pkonj: " ++ show a) False = undefined
		| null a = throw $ PatternMatchFail "Pattern parsing: Tried to parse empty conjunction"
		| null f1 && fst (head f2) == '~' = Not $ parse_konj $ tail f2
		| null f1 = parse_konj $ tail f2
		| null $ trim f2 = parse_expr f1
		| otherwise = parse_expr f1 :&: parse_konj f2
		where (f1,f2) = break (liftM2 (&&) ((==) 0 . snd) (flip elem "~\t\n\v\f\r &" . fst)) a

	parse_expr :: [(Char, Int)] -> Form
	parse_expr a'
		| trace ("pexpr: " ++ show a) False = undefined
		| null a = throw $ PatternMatchFail "Pattern parsing: Tried to parse empty expression"
		| a == [('T',0)] = T
		| a == [('F',0)] = F
		| head a == ('(',0) = parse_disj $ map (liftM2 (,) fst (flip (-) 1 . snd)) $ init $ tail a
		| all (flip elem (['a'..'z'] ++ ['Z'..'Z'] ++ ['0'..'9'] ++ "_") . fst) a = Var $ map fst a
		| otherwise = throw $ PatternMatchFail $ "Pattern parsing: Tried to parse " ++ map fst a ++ " as expression."
		where a = trim a'
	
	trim = reverse . t . reverse . t
		where t = dropWhile (flip elem "\t\n\v\f\r " . fst)

newtype IntCnf = IntCnf { getIntCnf :: [[Int]] }

instance Show IntCnf where
	show = show . intCnfToCnf

instance Eq IntCnf where
	(==) = flip ((==) . eqlz) . eqlz
		where eqlz = sort . map sort . getIntCnf

instance Arbitrary IntCnf where
	arbitrary = oneof [sized cnf, liftM reduceCnf $ sized cnf]
		where
		cnf :: Int -> Gen IntCnf
		cnf size = return . IntCnf . nub =<< (sequence $ take size $ repeat $ clause $ ceiling $ logBase 2 $ fromIntegral size)
		clause :: Int -> Gen [Int]
		clause size = sequence $ map (\n-> oneof $ map return [n,-n])  [1..size]

reduceCnf :: IntCnf -> IntCnf
reduceCnf = IntCnf . fixpoint (==) rC' . getIntCnf
	where
	rC' c' = foldr deleteVar c deletions
		where
		c = nub c'
		vars = nub . map abs . concat $ c
		tup t = flip map vars (\x -> (x, map (delete (t x)) $ filter (elem $ t x) c))
		pos = tup id
		neg = tup (0-)
		deletions = liftM2 trace show id $ catMaybes $ map (\(k, l) -> do { c <- lookup k pos; return (k, intersect c l) } ) neg
		deleteBoth k f l = if elem (k : f) l && elem (-k : f) l then trace (show "delete " ++ show [k:f,-k:f] ++ " from " ++ show l) $ (l \\ [k:f,-k:f]) ++ [f] else l
		deleteVar (k, fs) l = foldr (deleteBoth k) l fs

fixpoint :: (a -> a -> Bool) -> (a -> a) -> a -> a
fixpoint c f a = if a `c` f a then a else fixpoint c f $ f a

intCnfToCnf :: IntCnf -> Form
intCnfToCnf = foldl0 (:&:) T . map toClause . getIntCnf
	where
	toClause = foldl0 (:|:) F . map toLiteral
	toLiteral l = if l < 0 then Not $ toAtom $ abs l else toAtom l
	toAtom = Var . ("x"++) . show

foldl0 fn def = fromMaybe def . liftM2 conditional (const.not.null) (foldl1 fn)

conditional :: MonadPlus m => (a -> Bool) -> a -> m a
conditional = flip (flip mfilter . return) -- ausflippen

cnfToIntCnf :: Form -> IntCnf
cnfToIntCnf f = IntCnf . unfoldr fromCnf $ f
	where
	fromCnf (f1 :&: f2) = Just (clauseToInt f1, f2)
	fromCnf T = Nothing
	fromCnf f = Just (clauseToInt f, T)
	clauseToInt = unfoldr fromClause
	fromClause (f1 :|: f2) = Just (fromLiteral f1, f2)
	fromClause F = Nothing
	fromClause f = Just (fromLiteral f, F)
	fromLiteral (Not v) = - fromLiteral v
	fromLiteral (Var v) = (+1) $ fromJust $ elemIndex v $ vars f
	fromLiteral _ = error("no parse")