module Main where
import System.Environment (getArgs)
import qualified TextDisplay as D
import qualified Costack as C
import PropLogic
briefHelpMessage = D.correctTextFrame
[ "Syntax of the PropLogic command: ",
" PropLogic -- print this help ",
" PropLogic help -- print a more detailed help (with more options) ",
" PropLogic pdnf PROPFORM -- the Prime Disjunctive Normal Form of PROPFORM ",
" PropLogic pcnf PROPFORM -- the Prime Conjunctive Normal Form of PROPFORM ",
" PropLogic spdnf PROPFORM -- the Simplified Prime Disjunctive Normal Form ",
" PropLogic scdnf PROPFORM -- the Simplified Prime Conjunctive Normal Form ",
" PropLogic xpdnf PROPFORM -- the Extended/Indexed Prime Disjunctive Normal Form ",
" PropLogic xpcnf PROPFORM -- the Extended/Indexed Prime Conjunctive Normal Form ",
"where in each case, PROPFORM is a propositional formula in fancy notation and ",
"wrapped in double quotes \"...\"." ]
fullHelpMessage = D.correctTextFrame
[ "+---------------------------------------------------------------------------+",
"| (Fancy) Syntax of Propositional Formulas: |",
"+---------------------+-----------------------------+-----------------------+",
"| w | for every atom w | (atomic formula) |",
"| false | | (zero or false value) |",
"| true | | (unit or true value) |",
"| -p | for every formula p | (negation) |",
"| [p1 * ... * pN] | for N>=0 formulas p1,...,pN | (conjunction) |",
"| [p1 + ... + pN] | for N>=0 formulas p1,...,pN | (disjunction) |",
"| [p1 -> ... -> pN] | for N>=0 formulas p1,...,pN | (subjunction) |",
"| [p1 <-> ... <-> pN] | for N>=0 formulas p1,...,pN | (equijunction) |",
"+---------------------+-----------------------------+-----------------------+",
"| where an atom w is any non-empty sequence of letters and digits, except |",
"| the keywords 'true' and 'false'. |",
"+---------------------------------------------------------------------------|",
"",
"Example formulas are:",
"",
" [-x + [z <-> true] + -x + 23 + -y + -[x -> y] + [z * -7]]",
"",
" [[-x + y] <-> [x -> y] <-> -[x * -y] <-> [false -> x -> y -> true]]",
"",
"+----------------------------------------------------------------------+",
"| Definition of I-Forms |",
"+----------------------------------------------------------------------+",
"| An I-Form is a list [L1,...,Ln] of n I-Lines. Each I-Line is a list |",
"| [I1,...,Im] of integers, so that their absolute values are in strict |",
"| ascending order, i.e. abs(I1) < ... < abs(Im). |",
"+----------------------------------------------------------------------+",
"",
"Example I-Forms are:",
"",
" [[-2,4,6],[1,3,5,7],[-1,2,-3,4,-5,6],[],[-3],[3],[1,2,3,4,5,6,7]]",
"",
" [[]]",
"",
"+------------------------------------------------------------------------------------+",
"| Syntax of the PropLogic command |",
"+---------------------------+--------------------------------------------------------+",
"| PropLogic | print a brief overview of important command options |",
"| PropLogic help | print a more detailed help (namely this one)lp |",
"| PropLogic pdnf PROPFORM | the Prime Disjunctive Normal Form of PROPFORM |",
"| PropLogic pcnf PROPFORM | the Prime Conjunctive Normal Form of PROPFORM |",
"| PropLogic spdnf PROPFORM | the Simplified Prime Disjunctive Normal Form |",
"| PropLogic scdnf PROPFORM | the Simplified Prime Conjunctive Normal Form |",
"| PropLogic xpdnf PROPFORM | the Extended/Indexed Prime Disjunctive Normal Form |",
"| PropLogic xpcnf PROPFORM | the Extended/Indexed Prime Conjunctive Normal Form |",
"| PropLogic primForm IFORM | the Prime Normal Form of the given IFORM |",
"| PropLogic testing X Y Z N | performs test runs of Prime Form with randomly |",
"| | generated I-Forms. The four integer parameters are: |",
"| | X is the number of (different) atoms of the I-Form |",
"| | Y is the length of the randomly generated I-Form |",
"| | Z is the average length of the I-Lines in the I-Form |",
"| | N is the number of test runs. |",
"+---------------------------+--------------------------------------------------------+",
"| where |",
"| PROPFORM is a propositional formula (see below) surrounded by double quotes, |",
"| IFORM is an I-Form (see below) surrounded by double quotes. |",
"+------------------------------------------------------------------------------------+",
"",
"Legal example calls of the PropLogic command are:",
"",
" PropLogic spdnf \"[-x + [z <-> true] + -x + 23 + -y + -[x -> y] + [z * -7]]\" ",
"",
" PropLogic primForm \"[[-2,3],[1,2,3],[1,2,-3],[-1,4],[-2,4]]\"",
"",
" PropLogic testing 5 20 4 100",
"",
"More help and other material:",
" http://www.bucephalus.org/PropLogic",
"" ]
main :: IO ()
main = do args <- getArgs
let act = case args of
[] -> D.printTextFrame briefHelpMessage
["help"] -> D.printTextFrame fullHelpMessage
["pdnf", form] -> pdnf form
["pcnf", form] -> pcnf form
["spdnf", form] -> spdnf form
["spcnf", form] -> spcnf form
["xpdnf", form] -> xpdnf form
["xpcnf", form] -> xpcnf form
["primForm", intLL] -> print (prim intLL)
["testing", x, y, z, n] -> do t <- verboseRandomPrimeTesting (read x, read y, read z) (read n)
print t
otherwise -> do print "Unknown arguments for PropLogic!"
D.printTextFrame briefHelpMessage
act
return ()
where prim intLL = let intLL' = (read intLL) :: [[Int]]
iform = iForm intLL'
pform = primForm iform
intLL'' = map C.toList (C.toList pform)
in intLL''