-----------------------------------------------------------------------------
-- Copyright 2013, Open Universiteit Nederland. This file is distributed
-- under the terms of the GNU General Public License. For more information,
-- see the file "LICENSE.txt", which is included in the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer  :  josje.lodder@ou.nl
-- Stability   :  provisional
-- Portability :  portable (depends on ghc)
--
-- A set of example proofs
--
-----------------------------------------------------------------------------
module Domain.Logic.Examples
   ( exampleProofs
   ) where

import Domain.Logic.Formula
import Ideas.Common.Exercise
import Ideas.Common.Utils (ShowString(..))

exampleProofs :: [(Difficulty, (SLogic, SLogic))]
exampleProofs =
   [ {-  1 -} ok        (Not(p :||: (Not p :&&: q)), Not(p :||: q))
   , {-  2 -} ok        ((p :->: q):||: Not p, (p :->: q) :||: q)
   , {-  3 -} difficult ((p :&&: Not q):||:(q :&&: Not p), (p :||:q):&&:Not(p :&&: q))
   , {-  4 -} ok        (Not(p :||: Not(p :||: Not q)), Not(p :||: q))
   , {-  5 -} difficult (p :<->: q, (p :->: q) :&&: (q :->: p))
   , {-  6 -} ok        ((p :&&: q) :->: p, T)
   , {-  7 -} ok        ((p :->: q) :||: (q :->: p), T)
   , {-  8 -} difficult ((q :->: (Not p :->: q)) :->: p, Not p :->: (q :&&: ((p :&&: q) :&&: q)))
   , {-  9 -} ok        ((p :->: Not q):->:q, (s :||:(s :->:(q :||: p))) :&&: q)
   , {- 10 -} difficult (p :->: (q :->: r), (p :->: q) :->: (p :->:r))
   , {- 11 -} difficult (Not((p :->: q) :->: Not(q :->: p)), p :<->: q)
   , {- 12 -} ok        ((p :->: q):->: (p :->: s), (Not q :->: Not p) :->: (Not s :->: Not p))
   , {- 13 -} ok        (Not((p :->:q) :->: (p:&&:q)), (p :->: q) :&&: (Not p :||: Not q))
   , {- 14 -} ok        (Not((p :<->: q) :->: (p :||: (p :<->: q))), F)
   , {- 15 -} easy      (q :&&: p, p :&&: (q :||: q))
   , {- 16 -} easy      (Not(p :&&: q) :||: (s :||: Not r), (p :&&: q) :->: (r :->: s))
   , {- 17 -} easy      (Not(Not p :&&: Not(q :||: r)),  p :||: (q :||: r))
   , {- 18 -} easy      (Not (p :&&: (q :||: r)), Not p :||: (Not q :&&: Not r))
   , {- 19 -} easy      (p :&&: q, Not(p :->: Not q))
   , {- 20 -} difficult (p :<->: (q :<->: p),q)
   , {- 21 -} ok        ((p :->: q) :->: Not p, (p :->: (q :->: Not p)))
   , {- 22 -} ok        ((Not q :&&: p) :->: p, (Not q :<->: q) :->: p)
   , {- 23 -} easy      (p :<->: q, Not p :<->: Not q)
   , {- 24 -} difficult ((p :->: q) :<->: (p :->: r), (p :->: (q :&&: r)) :||: Not(p :->: (q :||: r)))
   , {- 25 -} ok        ((p :<->: (p :&&: q), p :->: q))
   , {- 26 -} ok        (p :<->: (p :->: q), p :&&: q)
   , {- 27 -} ok        ((p :->: q ) :&&: (r :->: q), (p :||: r) :->: q)
   , {- 28 -} difficult ((p :&&: (q :&&: r)) :||: (Not p :&&: q), (Not p :&&: (q :&&: Not r)) :||: ( q :&&: r))
   , {- 29 -} difficult (p :||: (q :&&: r), ( p :&&: Not q) :||: ( p :&&: Not r):||: ( q :&&: r))
   , {- 30 -} difficult ((p :&&: q) :||: (Not q :&&: r), ( p :&&: r) :||: ( p :&&: q :&&: Not r):||: (Not p :&&: Not q :&&: r))
   ]
 where
   easy      x = (Easy, x)
   ok        x = (Medium, x)
   difficult x = (Difficult, x)

   p = Var (ShowString "p")
   q = Var (ShowString "q")
   s = Var (ShowString "s")
   r = Var (ShowString "r")

{-
makeTestCases :: IO ()
makeTestCases = zipWithM_ makeTestCase [0..] exampleProofs

makeTestCase :: Int -> (SLogic, SLogic) -> IO ()
makeTestCase n (p, q) =
   writeFile ("proof" ++ show n ++ ".json")
      (json $ show p ++ " == " ++ show q)

json :: String -> String
json s = unlines
   [ "{ \"method\" : \"derivation\""
   , ", \"params\" : [[\"logic.proof\", \"[]\", " ++ show s ++ ", \"\"]]"
   , ", \"id\"     : 42"
   , "}"
   ] -}