packages feed

picologic (empty) → 0.1

raw patch · 9 files changed

+515/−0 lines, 9 filesdep +basedep +containersdep +haskelinesetup-changed

Dependencies added: base, containers, haskeline, mtl, parsec, picosat, pretty, process

Files

+ LICENSE view
@@ -0,0 +1,19 @@+Copyright (c) 2014, Stephen Diehl++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to+deal in the Software without restriction, including without limitation the+rights to use, copy, modify, merge, publish, distribute, sublicense, and/or+sell copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in+all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING+FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS+IN THE SOFTWARE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ picologic.cabal view
@@ -0,0 +1,60 @@+name:                picologic+version:             0.1+synopsis:            Utilities for symbolic predicate logic expressions+homepage:            https://github.com/sdiehl/picologic+license:             MIT+license-file:        LICENSE+author:              Stephen Diehl+maintainer:          stephen.m.diehl@gmail.com+copyright:           2014 Stephen Diehl+category:            Logic+build-type:          Simple+cabal-version:       >=1.10+tested-with:         GHC == 7.6.3+Bug-Reports:         https://github.com/sdiehl/picologic/issues++description:+  `picologic` provides symbolic logic expressions that can be integrated with the `picosat` solver.+Source-Repository head+    type: git+    location: git@github.com:sdiehl/picologic.git++Flag shell+  description: Build the interactive shell+  default:     False++library+  exposed-modules:     +    Picologic,+    Picologic.Solver,+    Picologic.AST,+    Picologic.Parser+  hs-source-dirs:      src+  other-extensions:    DeriveDataTypeable, BangPatterns+  build-depends:       +    base        >= 4.6 && <4.7,+    picosat     >= 0.1 && <0.2,+    containers  >= 0.5 && <0.6,+    mtl         >= 2.1 && <2.2,+    pretty      >= 1.1 && <1.2,+    parsec      >= 3.1 && <3.2+  default-language:    Haskell2010++executable picologic+  main-is:     Picologic/Main.hs+  if flag(shell)+    hs-source-dirs:      src+    other-modules: Picologic.Repl+    other-extensions:    DeriveDataTypeable, BangPatterns+    build-depends:       +      base        >= 4.6 && <4.7,+      picosat     >= 0.1 && <0.2,+      containers  >= 0.5 && <0.6,+      mtl         >= 2.1 && <2.2,+      pretty      >= 1.1 && <1.2,+      parsec      >= 3.1 && <3.2,+      process     >= 1.1 && <1.2,+      haskeline   >= 0.7 && <0.8+    default-language:    Haskell2010+  else+    buildable: False
+ src/Picologic.hs view
@@ -0,0 +1,41 @@+{- |++Example usage:++@+import Picologic+p, q, r :: Expr+p = readExpr \"~(A | B)\"+q = readExpr \"(A | ~B | C) & (B | D | E) & (D | F)\"+r = readExpr \"(φ \<-\> ψ)\"+@++The expression can be pretty printed using logical symbols:++>>> ppExprU p+¬(A ∨ B)+>>> ppExprU q+((((A ∨ ¬B) ∨ C) ∧ ((B ∨ D) ∨ E)) ∧ (D ∨ F))+>>> ppExprU (cnf r)+((φ ∧ (φ ∨ ¬ψ)) ∧ ((ψ ∨ ¬φ) ∧ ψ))++To run the expression against the SAT solver run:++>>> solveProp p >>= putStrLn . ppSolutions+~A ~B+~A B+A ~B++-}++module Picologic (+  module Picologic.AST,+  module Picologic.Parser,+  module Picologic.Solver,+  module Picologic.Pretty,+) where++import Picologic.AST+import Picologic.Parser+import Picologic.Solver+import Picologic.Pretty
+ src/Picologic/AST.hs view
@@ -0,0 +1,106 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DeriveDataTypeable #-}++module Picologic.AST (+  Expr(..),+  Ident(..),+  Solutions(..),+  Ctx,++  variables,+  eval,++  cnf,+  nnf,+  simp,+) where++import Data.List+import Data.Data+import Data.Maybe+import qualified Data.Map as M+++newtype Ident = Ident String+  deriving (Eq, Ord, Show, Data, Typeable)++newtype Solutions = Solutions [[Expr]]++type Ctx = M.Map Ident Bool++data Expr+  = Var       Ident      -- ^ Variable+  | Neg       Expr       -- ^ Logical negation+  | Conj      Expr Expr  -- ^ Logical conjunction+  | Disj      Expr Expr  -- ^ Logical disjunction+  | Iff       Expr Expr  -- ^ Logical biconditional+  | Implies   Expr Expr  -- ^ Material implication+  deriving (Eq, Ord, Show, Data, Typeable)++-- | Evaluate expression.+eval :: Ctx -> Expr -> Bool+eval vs (Var v)           = fromMaybe False (M.lookup v vs)+eval vs (Neg expr)        = not $ eval vs expr+eval vs (Conj e1 e2)      = eval vs e1 && eval vs e2+eval vs (Disj   e1 e2)    = eval vs e1 || eval vs e2+eval vs (Implies   e1 e2) = not (eval vs e1) || eval vs e2+eval vs (Iff e1 e2)       = eval vs e1 == eval vs e2++-- | Variables in expression+variables :: Expr -> [Ident]+variables expr = map head . group . sort $ go expr []+  where+    go (Var v)         !vs = v : vs+    go (Neg e)         !vs = go e vs+    go (Conj e1 e2)    !vs = go e1 vs ++ go e2 vs+    go (Disj e1 e2)    !vs = go e1 vs ++ go e2 vs+    go (Iff e1 e2)     !vs = go e1 vs ++ go e2 vs+    go (Implies e1 e2) !vs = go e1 vs ++ go e2 vs++-- | Negation normal form.+nnf :: Expr -> Expr+nnf ex = case ex of+  e@(Var _)             -> e+  e@(Neg (Var _))       -> e+  Neg (Neg e)           -> e++  Conj e1 e2            -> nnf e1 `Conj` nnf e2+  Neg (Conj e1 e2)      -> nnf $ Neg e1 `Conj` Neg e2++  Disj e1 e2            -> nnf e1 `Disj` nnf e2+  Neg (Disj e1 e2)      -> nnf $ Neg e1 `Conj` Neg e2++  Implies e1 e2         -> nnf $ Neg e1 `Disj` e2+  Neg (Implies e1 e2)   -> nnf $ e1 `Conj` Neg e2++  Iff e1 e2             -> let a = e1 `Conj` e2+                               b = Neg e1 `Conj` Neg e2+                               in nnf $ a `Disj` b++  Neg (Iff e1 e2)       -> let a = e1 `Disj` e2+                               b = Neg e1 `Disj` Neg e2+                               in nnf $ a `Conj` b++-- | Conjunctive normal form.+cnf :: Expr -> Expr+cnf = simp . cnf' . nnf+  where+    cnf' :: Expr -> Expr+    cnf' (Conj e1 e2) = cnf' e1 `Conj` cnf' e2+    cnf' (Disj e1 e2) = cnf' e1 `dist` cnf' e2+    cnf' e            = e++    dist :: Expr -> Expr -> Expr+    dist (Conj e11 e12) e2 = (e11 `dist` e2) `Conj` (e12 `dist` e2)+    dist e1 (Conj e21 e22) = (e1 `dist` e21) `Conj` (e1 `dist` e22)+    dist e1 e2             = e1 `Disj` e2++-- | Remove tautologies.+simp :: Expr -> Expr+simp ex = case ex of+  Disj e1 (Neg e2) | e1 == e2 -> e1+  Disj (Neg e1) e2 | e1 == e2 -> e1+  Disj e1 e2 -> Disj (simp e1) (simp e2)+  Conj e1 e2       | e1 == e2 -> e1+                   | otherwise -> Conj (simp e1) (simp e2)+  e -> e
+ src/Picologic/Main.hs view
@@ -0,0 +1,14 @@+module Main where++import Picologic.Repl+import Control.Monad+import System.Environment++main :: IO ()+main = do+  args <- getArgs+  case args of+    []      -> void $ runRepl repl+    ["-"]   -> stdin+    [fname] -> void $ runRepl (file fname >> repl)+    _ -> putStrLn "invalid arguments"
+ src/Picologic/Parser.hs view
@@ -0,0 +1,53 @@+module Picologic.Parser (+  parseFile,+  parseExpr,+  readExpr,+) where++import Text.Parsec hiding (State)+import qualified Text.Parsec.Expr as Ex++import Picologic.AST+import Picologic.Lexer++infixOp :: String -> (a -> a -> a) -> Ex.Assoc -> Op a+infixOp x f = Ex.Infix (reservedOp x >> return f)++prefixOp :: String -> (a -> a) -> Op a+prefixOp x f = Ex.Prefix (reservedOp x >> return f)++operators :: [[Op Expr]]+operators = [+    [ prefixOp "~" Neg ],+    [+      infixOp "&" Conj Ex.AssocLeft,+      infixOp "|" Disj Ex.AssocLeft,+      infixOp "->" Implies Ex.AssocLeft,+      infixOp "<->" Iff Ex.AssocLeft+    ]+  ]++var :: Parser Expr+var = do+  x <- identifier+  return $ Var (Ident x)++cexpr :: Parser Expr+cexpr =  Ex.buildExpressionParser operators cfactor++cfactor :: Parser Expr+cfactor =  var+       <|> parens cexpr++parseExpr :: String -> Either ParseError Expr+parseExpr = parse (contents cexpr) "<stdin>"++readExpr :: String -> Expr+readExpr s = case parseExpr s of+  Left err -> error (show err)+  Right expr -> expr++parseFile :: FilePath -> IO (Either ParseError Expr)+parseFile fname = do+  fcontents <- readFile fname+  return $ parse (contents cexpr) fname fcontents
+ src/Picologic/Repl.hs view
@@ -0,0 +1,147 @@+module Picologic.Repl (+  repl,+  stdin,+  file,+  runRepl,+) where++import Picologic.AST+import Picologic.Parser+import Picologic.Solver+import Picologic.Pretty++import Text.PrettyPrint++import Control.Monad.State++import Data.List (isPrefixOf)+import System.Console.Haskeline++-------------------------------------------------------------------------------+-- REPL+-------------------------------------------------------------------------------++type Repl = StateT IState (InputT IO)++data IState = IState+  { _module :: Maybe Expr+  , _curFile :: Maybe FilePath+  }++initState :: IState+initState = IState Nothing Nothing++preamble :: Repl ()+preamble = liftIO $ do+  putStrLn "Picologic 0.1"+  putStrLn "Type :help for help"++runRepl :: Repl a -> IO IState+runRepl f = runInputT defaultSettings (execStateT (preamble >> f) initState)++-------------------------------------------------------------------------------+-- Commands+-------------------------------------------------------------------------------++load :: String -> Repl ()+load arg = do+  liftIO $ putStrLn $ "Loading " ++ arg+  file arg+  modify $ \s -> s { _curFile = Just arg }++reload :: Repl ()+reload = do+  fname <- gets _curFile+  case fname of+    Just fname' -> handleCommand "load" [fname']+    Nothing -> liftIO $ putStrLn "No such file"++run :: Repl ()+run = do+  mod <- gets _module+  case mod of+    Nothing -> liftIO $ putStrLn "No expression."+    Just ex -> liftIO $ do+      sols <- solveProp ex+      putStrLn "Solutions:"+      putStrLn (ppSolutions sols)++clauses :: Repl ()+clauses = do+  env <- gets _module+  case env of+    Just ex -> liftIO $ print (clausesExpr ex)+    Nothing -> liftIO $ putStrLn "No file loaded."++help :: Repl ()+help = liftIO $ do+  putStrLn ":clauses      Show the SAT solver clauses"+  putStrLn ":load <file>  Load a program from file"++-------------------------------------------------------------------------------+-- Test+-------------------------------------------------------------------------------++-- evaluate a module+modl :: FilePath -> Repl ()+modl fname = do+  mod <- liftIO $ parseFile fname+  case mod of+    Left  err -> liftIO $ print err+    Right res ->+      let ex = (simp . cnf $ res) in+      modify $ \s -> s { _module = Just ex }++-- evaluate an expression+exec :: String -> Repl ()+exec source = do+  let mod = parseExpr source+  case mod of+    Left  err -> liftIO $ print err+    Right res -> do+      let ex = (simp . cnf $ res)+      liftIO $ putStrLn (render $ ppExprU ex)+      liftIO $ do+        sols <- solveProp ex+        putStrLn "Solutions:"+        putStrLn (ppSolutions sols)+      modify $ \s -> s { _module = Just ex }++file :: FilePath -> Repl ()+file fname = modl fname++stdin :: IO ()+stdin = do+  contents <- getContents+  case parseExpr contents of+    Left err -> print err+    Right ex -> do+      sols <- solveProp ex+      putStrLn (ppSolutions sols)++handleCommand :: String -> [String] -> Repl ()+handleCommand cmd args+    | "ru"  `isPrefixOf` cmd = run+    | "r"   `isPrefixOf` cmd = reload+    | "cl"  `isPrefixOf` cmd = clauses+    | "h"   `isPrefixOf` cmd = help+    | length args == 0 = liftIO $ putStrLn "Not enough arguments"+    | "l"  `isPrefixOf` cmd = load arg+    | otherwise = liftIO $ putStrLn "Unknown command"+  where+    arg = head args++repl :: Repl ()+repl = do+  minput <- lift $ getInputLine "Logic> "+  case minput of+    Nothing -> lift $ outputStrLn "Goodbye."++    Just (':' : cmds) -> do+      let (cmd:args) = words cmds+      handleCommand cmd args+      repl++    Just input -> do+      exec input+      repl
+ src/Picologic/Solver.hs view
@@ -0,0 +1,73 @@+module Picologic.Solver (+  solveProp,+  clausesExpr,+) where++import Picologic.AST+import Picosat++import Data.List+import Data.Map as M+import Control.Monad.Writer++data Clause+  = CV Int       -- ^Clause variable ( a or -a )+  | CL [Clause]  -- ^Set of clause under disjuntion++instance Show Clause where+  show (CV i) = show i+  show (CL xs) = concat (intersperse " " (fmap show xs))++-- | Yield the soutions for an expressions using the PicosSAT solver.+solveProp :: Expr -> IO Solutions+solveProp p = solveAll cs >>= return . Solutions . fmap (backSubst vs')+  where+    cs = fmap toInts $ execWriter $ clauses vs (cnf p)+    vs  = M.fromList $ zip vars [1..]+    vs' = M.fromList $ zip [1..] vars+    vars = variables (cnf p)++-- | Yield the integer clauses given to the SAT solver.+clausesExpr :: Expr -> [[Int]]+clausesExpr p = fmap toInts $ execWriter $ clauses vs (cnf p)+  where+    vs = M.fromList $ zip vars [1..]+    vars = variables (cnf p)++backSubst :: Map Int Ident -> Solution -> [Expr]+backSubst env (Solution xs) = fmap go xs+  where+    go x | x >= 0 = Var (env M.! x)+    go x | x < 0 = Neg (Var (env M.! (abs x)))+backSubst _ Unsatisfiable = []+backSubst _ Unknown = []++toInts :: Clause -> [Int]+toInts (CL xs) = fmap (\(CV n) -> n) xs++neg :: Clause -> Clause+neg (CV n) = CV (-n)+neg (CL xs) = CL (fmap neg xs)++combine :: Clause -> Clause -> Clause+combine (CL x) (CL y) = CL (x++y)+combine (CL x) y = combine (CL x) (CL [y])+combine x (CL y) = combine (CL [x]) (CL y)+combine x y = CL [x, y]++clauses :: M.Map Ident Int -> Expr -> Writer [Clause] Clause+clauses env ex = case ex of+  Var v -> return $ CV (env M.! v)+  Neg x -> do+    cs <- clauses env x+    return (neg cs)+  Conj e1 e2 -> do+    cs1 <- clauses env e1+    cs2 <- clauses env e2+    tell [combine cs1 cs2]+    return (combine cs1 cs2)+  Disj e1 e2 -> do+    cs1 <- clauses env e1+    cs2 <- clauses env e2+    tell [combine cs1 cs2]+    return (combine cs1 cs2)