PropLogic を使う

CNF を自動計算するモジュールがほしかったのだけど，なかなか見つからなくて，ProcLogic にいきついた．ただProcLogic がバグだらけで理想どおりに使おうとすると苦労したんだけど，とりあえず以下のように書くととりあえず，できたので，メモ程度に残しておく．この内容はまたちゃんと書くとする．

-- toCNF.hs
import PropLogic
import qualified TextDisplay as D
--import TextDisplay -- なぜかTextDisplay が含まれていないので，ここに書く．
import System.IO
-- import Text.Regex.Posix
-- import Data.ByteString.Char8 (pack)

activateTask = "[[[a <-> [b * c]] * [b <-> [d * e]] * [d <-> [[f + g] * -[f * g]]] * [e <-> [[h + i] * -[h * i]]] * [c <-> [j * k]]]  * [j <-> [[l + m] * -[l * m]]] *  [k <-> [[n + o + p] * -[n * o]  * -[o * p]  * -[p * n]]] * -[g * e] * -[m * k]]"
at1 = spcnf activateTask
at2 = pcnf activateTask

x = "[-[rain * snow] * [wet <-> [rain + snow]] * [rain -> hot] * [snow -> -hot]]"
y = "[wet <-> snow]"
p = DJ [EJ [A "x", A "y"], N (A "z")]  ::  PropForm String

activateTaskCNF = pcnf' $ stringToProp activateTask

size1 = PropLogic.size 

hoge = pcnf' $ stringToProp x
fuga = spcnf' $ stringToProp x


--fuga1 = D.display $ spcnf' $ stringToProp x 

-- spcnf :: String -> IO ()
--spcnf = D.display . spcnf' . stringToProp

foo  = pcnf' $ stringToProp activateTask
boo  = spcnf' $ stringToProp activateTask

--stringToProp :: String -> PropForm String
x1 = stringToProp x 

--
toMiniSatStyle :: String -> String
toMiniSatStyle x = undefined

atomsList = irrAtoms $ stringToProp activateTask

aPair = (zip atomsList  (map show [1..])) ++ [("*", "\r")]