hgen-1.5.0: src/hgen.hs
{-# LANGUAGE CPP #-}
-- TODO : deep binding of downarrow
-- TODO : Maximum depth exceded (check arguments prob=0 => maxdepth=0)
-- TODO : Whe one operator reaches maximum depth we distribute its probability
-- to the other operators. Other possibility is to also increase the probability
-- of atoms.
-- TODO : We are not checking for repeated clauses. We may have to come up with a normal form
-- that sorts the atoms, or maybe reuse the trie functions
module Main (main)
where
import Debug.Trace(trace)
import System.Random(StdGen,randomR,newStdGen)
import Control.Monad.State(get,put,State,evalState)
import Control.Monad(unless, when)
import qualified HyLo.Formula as F (Formula(..))
import Prelude hiding ( mod )
import System.Console.CmdArgs
( details, summary, (+=), cmdArgs_ )
import Data.Version ( showVersion )
import Paths_hgen ( version )
import Params
data Formula
= Fprop Int
| Fnom Int
| Fvar Int
| Fnot Formula
| Fand [Formula]
| For [Formula]
| Fbox Int Formula
| Fubox Formula
| Fdubox Formula
| Fibox Int Formula
| Fat Int Formula
| Fatv Int Formula
| Fdown Int Formula
deriving Show
data Shape =
Shp Int [Shape]
deriving Show
-- probsOp : Given the set of parameters (which varies as the formula grows)
-- it returns the probability of appearance for every operator
-- TODO:Downarrow requires another operator as argument: if we run out, no downarrow.
-- This can cause downarrow depth problems!
probsOp :: Params -> [Int]
probsOp p =
let dzero x = if x==0 then 0 else 1
in if not (forceDepths p)
then [dzero (mdepth p) * pmod p,
dzero (atdepth p) * pat p,
dzero (dwdepth p) * pdown p,
dzero (umdepth p) * puniv p,
dzero (dumdepth p) * pduniv p,
dzero (invdepth p) * pinv p]
else [pmod p, pat p, pdown p, puniv p, pduniv p, pinv p]
-- probsProp : Given the set of parameters (which varies as the
-- formula grows) and a list of atoms, it returns the probability of an
-- atom of being of each type, the probability being zero if all the
-- possible different atoms of that type are already present on the list
probsProp :: Params -> [Formula] -> [Int] -> [Int]
probsProp p flist vlist =
let dzero x = if x<=0 then 0 else 1
stillPs = dzero $ (pvars p) - (sum $ map hmpro flist)
stillNs = dzero $ (nomvars p) - (sum $ map hmnom flist)
stillVs = dzero $ (length vlist) - (sum $ map isVar flist)
in [ pprop p * stillPs, pnom p * stillNs, psvar p * stillVs]
main :: IO ()
main = do params <- cmdArgs_ $ defaultParams += summary header += details gplTag
runWithParams params
runWithParams :: Params -> IO ()
runWithParams params =
do unless (hidesummary params) $ putStrLn $ "Setting the following parameters:\n" ++ show params
(frmList,d1frmList,d2frmList) <- evalState (generateFormulaList (numinst params) params) `fmap` newStdGen
let name = getName params
let d1name = "d1" ++ name
let d2name = "d2" ++ name
writeList name (numinst params) frmList
when (gendefaults params) $ writeList d1name (numinst params) d1frmList
when (gendefaults params) $ writeList d2name (numinst params) d2frmList
getName :: Params -> String
getName params
= "hcnf" ++
"C" ++ show (numclauses params) ++ "-" ++
"S" ++ (csize params) ++ "-" ++
"M" ++ show (mods params) ++ "-" ++
"GD" ++ show (gdepth params) ++ "-" ++
-- "@D" ++ show (atdepth params) ++ "-" ++
-- "DD" ++ show (dwdepth params) ++ "-" ++
-- "UD" ++ show (umdepth params) ++ "-" ++
-- "ID" ++ show (invdepth params) ++ "-" ++
"NP" ++ show (pvars params) ++ "-" ++
"NN" ++ show (nomvars params) ++ "-" ++
"NS" ++ show (stvars params)
header :: String
header = unlines ["hgen " ++ showVersion version,
"Compiled on " ++ __DATE__ ++ ", at " ++ __TIME__,
"C. Areces, D. Gorin, G. Hoffmann and J. Heguiabehere."]
gplTag :: [String]
gplTag = [
"This program is distributed in the hope that it will be useful,",
"but WITHOUT ANY WARRANTY; without even the implied warranty of",
"MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the",
"GNU General Public License for more details."]
{- choose: Given
- a list of natural numbers l
- an integer n in [1:100]
returns the index in l corresponding to n, when we consider l
as a probability distribution and n is a random number -}
choose :: [Int] -> Int -> Int
choose l n =
let select arg@(what,idx) here
| what<=0 = arg
| here>=what = (0,idx)
| otherwise = (what-here,idx+1)
maxProb = sum l
indexValue = ceiling $ fromIntegral (n * maxProb) * (0.01::Double)
in
snd $ foldl select (indexValue,1) l
{- genShape: Given the number of disjuncts wanted,
the remaining depth to go,
and the current set of parameters,
it returns a list of structures (shapes) containing
- the number of atoms
- a list of arguments for operators (also shapes) -}
genShape:: Int -> Int -> Params -> State StdGen [Shape]
genShape 0 _ _ = return []
genShape n 0 p =
do r <- nextR
let numDisj = choose (read $ csize p) r
rest <- genShape (n-1) 0 p
return $ (Shp numDisj []):rest
genShape n maxdepth p =
do r <- nextR
r2 <- nextR
let numDisj = choose (read $ csize p) r
let pc = fromIntegral (pop p * numDisj) * (0.01::Double)
let floorpc = floor pc
let ceilingpc = ceiling pc
let numProps = if floorpc == ceilingpc || ((fromIntegral r2 * 0.01) < (fromIntegral ceilingpc - pc))
then floorpc
else ceilingpc
rest <- genShape (n-1) maxdepth p
restint <- genShape (numDisj - numProps) (maxdepth-1) p
return $ (Shp numProps restint):rest
{- genDisjunct : Given a shape,
the current set of parameters,
a list of available variables and
an atom,
it chooses the atoms and the operators to fill the shape and turn it into a formula,
which will not include said atom in its top level -}
genDisjunct:: Shape -> Params -> [Int] -> Formula -> State StdGen Formula
genDisjunct (Shp nump sh) p l bannedAtom =
let
end = sum (probsOp p) == 0
finalnump = if end then nump + length sh else nump
finalsh = if end then [] else sh
in do
props <- genProp finalnump p l bannedAtom
ops <- genOps finalsh p l
return $ For (props++ops)
{- genProp : given the number of atoms wanted,
the set of parameters
the available variables,
and an atom which is not allowed,
it returns the required number of atoms -}
genProp :: Int -> Params -> [Int] -> Formula -> State StdGen [Formula]
genProp 0 _ _ _ = return []
genProp nump p vlist bannedAtom =
do
rn <- nextR
rn2 <- nextR
res <- genProp (nump-1) p vlist bannedAtom
posVar <- nextRn $ length vlist
let probs = probsProp p res vlist -- only symbols for available categories
if sum probs == 0
then return (trace "Too few atomic symbols!!\n" res)
else
case choose probs rn of -- [prop, nom, svar]
1 -> do let avail = takeUsedP (replicate (pvars p) 1) (bannedAtom:res)
let prop = choose avail rn2
f <- randNeg (Fprop prop) (pneg p)
return (f:res)
2 -> do let avail = takeUsedN (replicate (nomvars p) 1) (bannedAtom:res)
let nom = choose avail rn2
f <- randNeg (Fnom nom) (pneg p)
return (f:res)
3 -> do let avail = takeUsedV (addPresent (replicate (stvars p) 0) vlist) (bannedAtom:res)
let var = if all (== 0) avail
then vlist !! (posVar - 1)
else choose avail rn2
f<- randNeg (Fvar var) (pneg p)
return (f:res)
_ -> error "genProp"
-- takeUsedP : Removes from the bitmap of all possible proposition symbols those already used
takeUsedP :: [Int] -> [Formula] -> [Int]
takeUsedP l [] = l
takeUsedP l (Fprop n:fl) = takeUsedP ( take (n-1) l ++(0:drop n l)) fl
takeUsedP l (Fnot (Fprop n):fl) = takeUsedP ( take (n-1) l ++ (0:drop n l)) fl
takeUsedP l (_:fl) = takeUsedP l fl
-- takeUsedN : Removes from the bitmap of all possible nominals those already used
takeUsedN :: [Int] -> [Formula] -> [Int]
takeUsedN l [] = l
takeUsedN l (Fnom n:fl) = takeUsedN ( take (n-1) l ++(0:drop n l)) fl
takeUsedN l (Fnot (Fnom n):fl) = takeUsedN (take (n-1) l ++(0:drop n l)) fl
takeUsedN l (_:fl) = takeUsedN l fl
-- takeUsedV : Removes from the bitmap of all possible variables symbols those already used
takeUsedV :: [Int] -> [Formula] -> [Int]
takeUsedV l [] = l
takeUsedV l (Fvar n:fl) = takeUsedV (take (n-1) l ++(0:drop n l)) fl
takeUsedV l (Fnot (Fvar n):fl) = takeUsedV (take (n-1) l ++(0:drop n l)) fl
takeUsedV l (_:fl) = takeUsedV l fl
remove :: [Int] -> [Int] -> [Int]
remove l [] = l
remove list (n:nl) = remove ( take (n-1) list ++ (0:drop n list)) nl
-- addPresent : Adds to a bitmap
addPresent :: [Int] -> [Int] -> [Int]
addPresent l [] = l
addPresent list (n:l) = if n==0 || n > length list
then addPresent list l
else addPresent ( take (n-1) list ++ (1:drop n list)) l
-- genOps : Given a list of shapes (formula structures), returns the
-- formulas resulting from filling in the blanks in the shapes.
genOps :: [Shape] -> Params -> [Int] -> State StdGen [Formula]
genOps [] _ _ = return []
genOps sh@(s:shapes) p vlist =
do
rn <- nextR
rn2 <- nextR
posVar <- nextRn $ length vlist
let probs = probsOp p
if sum probs == 0
then return []
else case choose probs rn of
1 -> do -- BOX Case
let p' = p{mdepth = mdepth p -1}
orform <- genDisjunct s p' vlist (For [])
mod <- nextRn (mods p)
f <- randNeg (Fbox mod orform) (pneg p)
res <- genOps shapes p' vlist
return (f:res)
2 -> do -- AT Case
let p' = p{atdepth = atdepth p -1}
nom <- nextRn (nomvars p)
chanceV' <- nextR
let chanceV = if (pnom p == 0) || (nomvars p == 0) then 100 else chanceV'
let atV = (pdown p /= 0) && (chanceV > 50)
let avail = addPresent (replicate (stvars p) 0) vlist
let var = if all (== 0) avail
then vlist !! (posVar - 1)
else choose avail rn2
let forbAtom = if atV && (sum avail /= 0)
then Fvar var
else Fnom nom
let orf = genDisjunct s
p'
vlist
forbAtom
if atV && (sum avail /= 0)
then do orform <- orf
f <- randNeg (Fatv var orform) (pneg p)
res <- genOps shapes p' vlist
return (f:res)
else if not ((pnom p == 0) || (nomvars p == 0))
then do orform <- orf
f <- randNeg (Fat nom orform) (pneg p)
res <- genOps shapes p' vlist
return (f:res)
else genOps sh p vlist
3 -> do -- DOWN Case
-- the generation of \down x.\down y. is allowed
let p' = p{dwdepth = dwdepth p - 1}
let avail = remove (replicate (stvars p) 1) vlist
let var = choose avail rn2
orform <- genDisjunct s
p'
(var:vlist)
(For [])
f <- randNeg (Fdown var orform) (pneg p)
res <- genOps shapes p' vlist
return (f:res)
4 -> do -- UNIV Case
let p' = p{umdepth = umdepth p - 1}
orform <- genDisjunct s
p'
vlist
(For [])
f <- randNeg (Fubox orform)(pneg p)
res <- genOps shapes p' vlist
return (f:res)
5 -> do -- DIFF UNIV Case
let p' = p{dumdepth = dumdepth p - 1}
orform <- genDisjunct s
p'
vlist
(For [])
f <- randNeg (Fdubox orform)(pneg p)
res <- genOps shapes p' vlist
return (f:res)
6 -> do -- INV Case
let p' = p{invdepth = invdepth p - 1}
orform <- genDisjunct s
p'
vlist
(For [])
mod <- nextRn (mods p)
f <- randNeg (Fibox mod orform) (pneg p)
res <- genOps shapes p' vlist
return (f:res)
other -> error $ "Operator unknown: " ++ show other
randNeg:: Formula -> Int -> State StdGen Formula
randNeg f n = do rn <- nextR
return $ if n > rn then f else Fnot f
genDisjunctList :: [Shape] -> Params -> State StdGen [Formula]
genDisjunctList [] _ = return []
genDisjunctList (s:shapes) p =
do disj <- genDisjunct s p [] (For [])
rdisj <- genDisjunctList shapes p
return (disj:rdisj)
generateFormula :: Params -> State StdGen (String,String,String)
generateFormula p =
do shapes <- genShape (numclauses p) (gdepth p) p
gd <- genDisjunctList shapes p
newf <- mapM (sanitize2 p) gd
let forms = map toHyLoFormula newf
return (simpleOutput forms, defaultOutput1 forms,defaultOutput2 forms)
hmpro :: Formula -> Int
hmpro (Fprop _) = 1
hmpro (Fnom _) = 0
hmpro (Fvar _) = 0
hmpro (Fnot f) = hmpro f
hmpro (Fubox f) = hmpro f
hmpro (Fdubox f) = hmpro f
hmpro (For fl) = sum (map hmpro fl)
hmpro (Fbox _ f) = hmpro f
hmpro (Fibox _ f) = hmpro f
hmpro (Fat _ f) = hmpro f
hmpro (Fatv _ f) = hmpro f
hmpro (Fdown _ f) = hmpro f
hmpro _ = error "hmpro"
hmnom :: Formula -> Int
hmnom (Fprop _) = 0
hmnom (Fnom _) = 1
hmnom (Fvar _) = 0
hmnom (Fnot f) = hmnom f
hmnom (Fubox f) = hmnom f
hmnom (Fdubox f) = hmnom f
hmnom (For fl) = sum (map hmnom fl)
hmnom (Fbox _ f) = hmnom f
hmnom (Fibox _ f) = hmnom f
hmnom (Fat _ f) = hmnom f
hmnom (Fatv _ f) = hmnom f
hmnom (Fdown _ f) = hmnom f
hmnom _ = error "hmnom"
hmat :: Formula -> Int
hmat (Fprop _) = 0
hmat (Fnom _) = 0
hmat (Fvar _) = 0
hmat (Fnot f) = hmat f
hmat (Fubox f) = hmat f
hmat (Fdubox f) = hmat f
hmat (For fl) = sum (map hmat fl)
hmat (Fbox _ f) = hmat f
hmat (Fibox _ f) = hmat f
hmat (Fat _ f) = 1 + hmat f
hmat (Fatv _ f) = hmat f
hmat (Fdown _ f) = hmat f
hmat _ = error "hmat"
-- isVar:: Whether an atom is a state variable (1 if yes, 0 if no)
isVar :: Formula -> Int
isVar (Fvar _) = 1
isVar (Fnot (Fvar _)) = 1
isVar _ = 0
-- If a variable at a downarrow operator does not appear
-- in the scope, a prop. variable, nominal, or at is changed
sanitize2 :: Params -> Formula -> State StdGen Formula
sanitize2 p (Fdown n f) =
if looseVar n f
then do rn <- nextR
let c = [hmpro f, hmnom f, hmat f]
let nz x = if x == 0 then 0 else 1
let nzc = map nz c
let ch = choose nzc rn
rnp <- nextRn (c!!0)
rnn <- nextRn (c!!1)
rna <- nextRn (c!!2)
case ch of
1 -> return (Fdown n (changeProp rnp n f))
2 -> return (Fdown n (changeNom rnn n f))
3 -> return (Fdown n (changeAt rna n f))
_ -> error "sanitize2"
else Fdown n `fmap` sanitize2 p f
sanitize2 p (Fnot f) = Fnot `fmap` sanitize2 p f
sanitize2 p (Fubox f) = Fubox `fmap` sanitize2 p f
sanitize2 p (Fdubox f) = Fdubox `fmap` sanitize2 p f
sanitize2 p (Fibox n f)= Fibox n `fmap` sanitize2 p f
sanitize2 p (Fbox n f) = Fbox n `fmap` sanitize2 p f
sanitize2 p (Fat n f) = Fat n `fmap` sanitize2 p f
sanitize2 p (Fatv n f) = Fatv n `fmap` sanitize2 p f
sanitize2 p (For fl) = For `fmap` mapM (sanitize2 p) fl
sanitize2 _ f = return f
looseVar :: Int -> Formula -> Bool
looseVar n f = n `notElem` listVars f
listVars :: Formula -> [Int]
listVars (Fprop _) = []
listVars (Fnom _) = []
listVars (Fvar n) = [n]
listVars (Fnot f) = listVars f
listVars (Fubox f) = listVars f
listVars (Fdubox f) = listVars f
listVars (Fibox _ f) = listVars f
listVars (For fl) = concatMap listVars fl
listVars (Fbox _ f) = listVars f
listVars (Fat _ f) = listVars f
listVars (Fatv n f) = n:listVars f
listVars (Fdown _ f) = listVars f
listVars _ = error "listVars"
changeProp :: Int -> Int -> Formula -> Formula
changeProp _ n (Fprop _) = Fvar n
changeProp _ _ (Fnom n) = Fnom n
changeProp _ _ (Fvar n) = Fvar n
changeProp pos n (Fnot f) = Fnot (changeProp pos n f)
changeProp pos n (Fbox m f) = Fbox m (changeProp pos n f)
changeProp pos n (Fubox f) = Fubox (changeProp pos n f)
changeProp pos n (Fdubox f) = Fdubox (changeProp pos n f)
changeProp pos n (Fibox m f) = Fibox m (changeProp pos n f)
changeProp pos n (Fat m f) = Fat m (changeProp pos n f)
changeProp pos n (Fatv m f) = Fatv m (changeProp pos n f)
changeProp pos n (Fdown m f) = Fdown m (changeProp pos n f)
changeProp pos n (For [f1]) = For [changeProp pos n f1]
changeProp pos n (For (f1:(f2:fl)))
| hmpro f1 < pos = For (f1:[changeProp (pos - hmpro f1) n (For (f2:fl))])
| otherwise = For (changeProp pos n f1:(f2:fl))
changeProp _ _ _ = error "changeProp"
changeNom :: Int -> Int -> Formula -> Formula
changeNom _ n (Fnom _) = Fvar n
changeNom _ _ (Fprop n) = Fprop n
changeNom _ _ (Fvar n) = Fvar n
changeNom pos n (Fnot f) = Fnot (changeNom pos n f)
changeNom pos n (Fbox m f) = Fbox m (changeNom pos n f)
changeNom pos n (Fubox f) = Fubox (changeNom pos n f)
changeNom pos n (Fdubox f) = Fdubox (changeNom pos n f)
changeNom pos n (Fibox m f) = Fibox m (changeNom pos n f)
changeNom pos n (Fat m f) = Fat m (changeNom pos n f)
changeNom pos n (Fatv m f) = Fatv m (changeNom pos n f)
changeNom pos n (Fdown m f) = Fdown m (changeNom pos n f)
changeNom pos n (For [f1]) = For [changeNom pos n f1]
changeNom pos n (For (f1:(f2:fl)))
| hmnom f1 < pos = For (f1:[changeNom (pos - hmnom f1) n (For (f2:fl))])
| otherwise = For (changeNom pos n f1:(f2:fl))
changeNom _ _ _ = error "changeNom"
changeAt :: Int -> Int -> Formula -> Formula
changeAt _ _ (Fnom n) = Fvar n
changeAt _ _ (Fprop n) = Fprop n
changeAt _ _ (Fvar n) = Fvar n
changeAt pos n (Fnot f) = Fnot (changeAt pos n f)
changeAt pos n (Fbox m f) = Fbox m (changeAt pos n f)
changeAt pos n (Fubox f) = Fubox (changeAt pos n f)
changeAt pos n (Fdubox f) = Fdubox (changeAt pos n f)
changeAt pos n (Fibox m f) = Fibox m (changeAt pos n f)
changeAt _ n (Fat _ f) = Fatv n f
changeAt pos n (Fatv m f) = Fatv m (changeAt pos n f)
changeAt pos n (Fdown m f) = Fdown m (changeAt pos n f)
changeAt pos n (For [f1]) = For [changeAt pos n f1]
changeAt pos n (For (f1:(f2:fl)))
| hmat f1 < pos = For (f1:[changeAt (pos - hmat f1) n (For (f2:fl))])
| otherwise = For (changeAt pos n f1:(f2:fl))
changeAt _ _ _ = error "changeAt"
generateFormulaList :: Int -> Params -> State StdGen ([String],[String],[String])
generateFormulaList 0 _ = return ([],[],[])
generateFormulaList n p =
do (frm, d1frm, d2frm) <- generateFormula p
(lfrm, ld1frm, ld2frm) <- generateFormulaList (n-1) p
return (frm:lfrm, d1frm:ld1frm, d2frm:ld2frm)
-- writeList : Given a filename, and a list of strings,
-- writes the strings to a file with that name
writeList :: String -> Int -> [String] -> IO ()
writeList _ _ [] = return ()
writeList fname n (f:fl)
= do writeFile (fname ++ "." ++ show n ++ ".cnf") f
writeList fname (n-1) fl
-- nextR : Returns a fresh random number, range 1-100
nextR :: State StdGen Int
nextR = do gen <- get
let (num, newgen) = randomR (1,100) gen
put newgen
return num
-- nextR : Returns a fresh random number, range 1-n
nextRn :: Int -> State StdGen Int
nextRn n = do gen <- get
let (num, newgen) = randomR (1,n) gen
put newgen
return num
type HyLoFormula = F.Formula NomSymbol PropSymbol RelSymbol
toHyLoFormula :: Formula -> HyLoFormula
toHyLoFormula (Fprop v) = F.Prop (PropSymbol v)
toHyLoFormula (Fnom v) = F.Nom (NomSymbol v)
toHyLoFormula (Fvar v) = F.Nom (NomSymbol v)
toHyLoFormula (Fand fs) = foldr1 (F.:&:) $ map toHyLoFormula fs
toHyLoFormula (For fs) = foldr1 (F.:|:) $ map toHyLoFormula fs
toHyLoFormula (Fnot f) = F.Neg $ toHyLoFormula f
toHyLoFormula (Fubox f) = F.A $ toHyLoFormula f
toHyLoFormula (Fdubox f) = F.D $ toHyLoFormula f
toHyLoFormula (Fbox i f) = F.Box (RelSymbol i) $ toHyLoFormula f
toHyLoFormula (Fibox i f) = F.Box (InvRelSymbol i) $ toHyLoFormula f
toHyLoFormula (Fat i f) = F.At (NomSymbol i) $ toHyLoFormula f
toHyLoFormula (Fatv i f) = F.At (NomSymbol i) $ toHyLoFormula f
toHyLoFormula (Fdown i f) = F.Down (NomSymbol i) $ toHyLoFormula f
-- special signature so that formulas are printed with N1, P1 and R1 names
newtype PropSymbol = PropSymbol Int deriving(Eq, Ord)
instance Show PropSymbol where
show (PropSymbol i) = 'P':show i
newtype NomSymbol = NomSymbol Int deriving(Eq, Ord)
instance Show NomSymbol where
show (NomSymbol i) = 'N':show i
data RelSymbol = RelSymbol Int
| InvRelSymbol Int
deriving(Eq, Ord)
instance Show RelSymbol where
show (RelSymbol i) = 'R' : show i
show (InvRelSymbol i) = "-R" ++ show i
simpleOutput :: [HyLoFormula] -> String
simpleOutput input = unlines $ "begin":addSemicolon (map show input) ++ ["end"]
defaultOutput2 :: [HyLoFormula] -> String
defaultOutput2 fs
| length fs < 3 = error "For default output, at least 3 clauses needed."
| otherwise = unlines $
"classical":"facts:":"true":["defaults:"] ++ toDefs1 fs ++ toDefs2 fs ++ ["consequence:", show $ last fs ]
where
toDefs1 fs = map (\(x,y) -> "T --> " ++ show (x F.:|: y) ++ ";") $ zip fs $ tail fs
toDefs2 fs = map (\(x,y) -> show (x F.:|: y) ++ " --> " ++ show (x F.:&: y) ++ ";") $ zip fs $ tail fs
defaultOutput1 :: [HyLoFormula] -> String
defaultOutput1 fs
| length fs < 3 = error "For default output, at least 3 clauses needed."
| otherwise = unlines $
"classical":"facts:":"true":"defaults:":toDefault (map show fs) ++ ["consequence:","false"]
addSemicolon :: [String] -> [String]
addSemicolon xs = map (\x -> x ++ ";") xs
toDefault :: [String] -> [String]
toDefault xs = map (\x -> "T --> " ++ x ++ ";") xs