Folly 0.1.3.0 → 0.1.4.0

raw patch · 4 files changed

+26/−20 lines, 4 files

Files

Folly.cabal +1/−1
src/Folly/Formula.hs +7/−10
src/Folly/Resolution.hs +9/−9
src/Folly/Utils.hs +9/−0

Folly.cabal view

@@ -2,7 +2,7 @@ --  see http://haskell.org/cabal/users-guide/  name:                Folly-version:             0.1.3.0+version:             0.1.4.0 synopsis:            A first order logic library in Haskell description:         An implementation of first order logic in Haskell that 		     includes a library of modules for incorporating first

src/Folly/Formula.hs view

@@ -10,7 +10,6 @@   applyToTerms,   literalArgs,   toPNF, toSkolemForm, skf,-  Clause,   toClausalForm,   isTautology,   matchingLiterals) where@@ -86,7 +85,7 @@ showFormula T = "True" showFormula F = "False" showFormula (P predName args) = predName ++ "[" ++ (concat $ intersperse ", " $ L.map showTerm args)  ++ "]"-showFormula (N (P name args)) = "~" ++ show (P name args)+--showFormula (N (P name args)) = "~" ++ show (P name args) showFormula (N f) = "~(" ++ show f ++ ")" showFormula (B op f1 f2) = "(" ++ show f1 ++ " " ++ op ++ " "  ++ show f2 ++ ")" showFormula (Q q t f) = "(" ++ q ++ " "  ++ show t ++ " . " ++ show f ++ ")"@@ -274,15 +273,13 @@ skf n vars = Func ("skl" ++ show n) vars  -- Conversion to clausal form-type Clause = [Formula]--toClausalForm :: Formula -> [Clause]+toClausalForm :: Formula -> [[Formula]] toClausalForm = splitClauses . removeUniversals . distributeDisjunction . toSkolemForm -distributeDisjunction :: Formula -> Formula+distributeDisjunction :: (Formula) -> (Formula) distributeDisjunction f = transformFormula distrDis f -distrDis :: Formula -> Formula+distrDis :: (Formula) -> (Formula) distrDis (B "|" (B "&" l r) f) = (B "&" (B "|" l f) (B "|" r f)) distrDis (B "|" f (B "&" l r)) = (B "&" (B "|" f l) (B "|" f r)) distrDis f = f@@ -291,15 +288,15 @@ removeUniversals (Q "V" v f) = removeUniversals f removeUniversals f = f -splitClauses :: Formula -> [Clause]+splitClauses :: Formula -> [[Formula]] splitClauses (B "&" l r) = (splitClauses l) ++ (splitClauses r) splitClauses f = [splitDis f] -splitDis :: Formula -> Clause+splitDis :: Formula -> [Formula] splitDis (B "|" l r) = (splitDis l) ++ (splitDis r) splitDis f = [f] -isTautology :: Clause -> Bool+isTautology :: [Formula] -> Bool isTautology c = L.length (L.intersect atoms negAtoms) > 0   where     atoms = L.filter isAtom c

src/Folly/Resolution.hs view

@@ -16,12 +16,12 @@     clauses = uniqueVarNames $ L.concat $ L.map toClausalForm formulas     clauseSet = S.fromList clauses -resolve :: Set Clause -> Bool+resolve :: Set [Formula] -> Bool resolve cls = case S.member [] cls of   True -> True   False -> resolveIter [cls] -resolveIter :: [Set Clause] -> Bool+resolveIter :: [Set [Formula]] -> Bool resolveIter [] = error "Empty list of clause sets" resolveIter clauseSets = case S.size newClauses == 0 of   True -> True@@ -33,37 +33,37 @@       1 -> generateNewClauses (head clauseSets) (head clauseSets)       _ -> generateNewClauses (head clauseSets) (L.foldl S.union S.empty (tail clauseSets)) -generateNewClauses :: Set Clause -> Set Clause -> Set Clause+generateNewClauses :: Set [Formula] -> Set [Formula] -> Set [Formula] generateNewClauses recent old = deleteTautologies $ newClauses   where     newClauses = S.fold S.union S.empty $ S.map (\ c -> genNewClauses c old) recent     genNewClauses c cs = S.fold S.union S.empty $ S.map (\ x -> resolvedClauses c x) cs -resolvedClauses :: Clause -> Clause -> Set Clause+resolvedClauses :: [Formula] -> [Formula] -> Set [Formula] resolvedClauses left right = S.fromList resClauses   where     mResClauses = L.map (\ x -> (L.map (\ y -> tryToResolve x left y right) right)) left     resClauses = L.map fromJust $ L.filter (/= Nothing) $ L.concat mResClauses  -tryToResolve :: Formula -> Clause -> Formula -> Clause -> Maybe Clause+tryToResolve :: Formula -> [Formula] -> Formula -> [Formula] -> Maybe [Formula] tryToResolve leftLiteral leftClause rightLiteral rightClause =   case matchingLiterals leftLiteral rightLiteral of     True -> unifiedResolvedClause leftLiteral leftClause rightLiteral rightClause     False -> Nothing -unifiedResolvedClause :: Formula -> Clause -> Formula -> Clause -> Maybe Clause+unifiedResolvedClause :: Formula -> [Formula] -> Formula -> [Formula] -> Maybe [Formula] unifiedResolvedClause lLit lc rLit rc = case mostGeneralUnifier $ zip (literalArgs lLit) (literalArgs rLit) of   Just mgu -> Just $ L.map (\ lit -> applyToTerms lit (applyUnifier mgu)) ((L.delete lLit lc) ++ (L.delete rLit rc))   Nothing -> Nothing -uniqueVarNames :: [Clause] -> [Clause]+uniqueVarNames :: [[Formula]] -> [[Formula]] uniqueVarNames cls = zipWith attachSuffix cls (L.map show [1..length cls]) -attachSuffix :: Clause -> String -> Clause+attachSuffix :: [Formula] -> String -> [Formula] attachSuffix cls suffix = L.map (addSuffixToVarNames suffix) cls  addSuffixToVarNames :: String -> Formula -> Formula addSuffixToVarNames suffix form = applyToTerms form (appendVarName suffix) -deleteTautologies :: Set Clause -> Set Clause+deleteTautologies :: Set [Formula] -> Set [Formula] deleteTautologies clauses = S.filter (not . isTautology) clauses

src/Folly/Utils.hs view

@@ -9,6 +9,15 @@   Failed String   deriving (Show) +instance Applicative Error where+  pure = Succeeded+  (Succeeded f) <*> (Succeeded x) = Succeeded (f x)+  (Failed m) <*> _ = Failed m++instance Functor Error where+  fmap f (Succeeded a) = Succeeded (f a)+  fmap _ (Failed m) = Failed m+ instance Monad Error where   return a = Succeeded a   (Succeeded a) >>= f = f a