{- |
Module      :  $EmptyHeader$
Description :  <optional short description entry>
Copyright   :  (c) <Authors or Affiliations>
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  <email>
Stability   :  unstable | experimental | provisional | stable | frozen
Portability :  portable | non-portable (<reason>)

<optional description>
-}
module Proof where
--   ((-->), (<-->), (\/), (/\), true, false, box, dia, neg, var,  provable)

import Data.List (delete, intersect, nub)

-- data type for fomulas
data Form = Var Int --Var Char (Maybe Int)  -- variables
          | Not !Form             -- ¬A
          | Box !Form             -- [] A
          | Conj !Form !Form      -- A/\B
  deriving (Eq)

type Sequent =  [Form]     -- defines a sequent

-- pretty printing (sort of)
instance Show Form where
  show f = case f of
            Var i    -> "p" ++ show i
            Not g    -> "~" ++ show g
            Box g    -> "[]" ++ show g
            Conj g h -> "(" ++ show g ++ "&" ++ show h ++ ")"

-- syntactic sugar
p = Var 0
q = Var 1
r = Var 2

(-->) :: Form -> Form -> Form
infixr 5 -->
p --> q = Not (Conj p (Not q)) -- ~p\/q

(<-->) :: Form -> Form -> Form
infixr 4 <-->
p <--> q = Conj (p-->q) (q-->p) --Not (Conj (Not (Conj p q)) (Not(Conj (Not p) (Not q))))

box :: Form -> Form
box p = Box p

dia :: Form -> Form
dia p = Not(Box(Not p))

(/\) :: Form -> Form -> Form
infix 7 /\
p /\ q = Conj p q

(\/) :: Form -> Form -> Form
infix 6 \/
p \/ q = neg ((neg p) /\ (neg q))

neg :: Form -> Form
neg p = Not p

false :: Form
false = (Var 0) /\ (Not (Var 0))

true :: Form
true = neg false

var :: Int -> Form
var n = Var n

-- the rank of a modal formula
rank :: Form -> Int
rank (Box p) = 1 + (rank p)
rank (Conj p q) =  (max (rank p) (rank q))
rank (Not p) = rank p
rank (Var p) = 0

-- expand applies all sequent rules that do not induce branching
expand :: Sequent -> Sequent
expand s | seq s $ False = undefined -- force strictness
expand [] = []
expand ((Not (Not p)):as) = expand  (p:as)
expand ((Not (Conj p q)):as) = expand ((Not p):(Not q):as)
expand (a:as) = a:(expand as)

----------------------------------------------------------------------------------------------------

--Inference Rules
-- map a sequent the list of all lists of all premises that derive
-- the sequent. Note that a premise is a list of sequents:
-- * to prove Gamma, A /\ B we need both Gamma, A and Gamma, B as premises.
-- * to prove Gamma, neg(A /\ B), we need Gamma, neg A, neg B as premise.
-- * to prove A, neg A, Gamma we need no premises
-- So a premise is a list of sequents, and the list of all possible
-- premises therefore has type [[ Sequent ]]

-- the functions below compute the list of all possible premises
-- that allow to derive a given sequent using the rule that
-- lends its name to the function.
axiom :: Sequent -> [[Sequent]]
-- faster to check for atomic axioms
-- axiom1 xs = [ []  | p <- xs, (Not q) <- xs, p==q]
axiom xs = nub [ []  | (Var n) <- xs, (Not (Var m)) <- xs, m==n]

negI :: Sequent -> [[Sequent]]
negI  xs = [ [(p: delete f xs)] | f@(Not(Not p)) <- xs]

negConj :: Sequent -> [[Sequent]]
negConj (as) = [[( (Not(p)): (Not(q)) : delete f as )]| f@(Not(Conj p q)) <- as]


-- two variants here: use @-patterns or ``plain'' recursion.
conj :: Sequent -> [[ Sequent ]]
conj s | seq s $ False = undefined -- force strictness
conj (as) = [ [ (p: delete f as) , ( q: delete f as )] | f@(Conj p q ) <- as]

boxI :: Sequent -> [[Sequent]]
boxI (xs) = let as = [ (Not p) | (Not(Box p)) <- xs]
            in [ [ p:as] | (Box p) <- xs ]  ++
                                                   [ [ (Not q):delete g xs] | g@(Not (Box q)) <- xs ] -- T rule
tRule :: Sequent -> [[ Sequent ]]
tRule (xs) = [ [ (Not p):delete f xs] | f@(Not (Box p)) <- xs ] -- T rule

-- collect all possible premises, i.e. the union of the possible
-- premises taken over the set of all rules in one to  get the
-- recursion off the ground.

-- CAVEAT: the order of axioms /rules has a HUGE impact on performance.
allRules :: Sequent -> [[Sequent]]
-- this is as good as it gets if we apply the individual rules
-- message for the afterworld: if you want to find proofs quickly,
-- first look at the rules that induce branching.
-- allRules s =   (axiom1 s) ++ (axiom2 s) ++ (boxI s) ++ (conj s) ++ (negDisj s) ++ (negI s) ++  (negConj s) ++  (disj s)


-- we can do slightly better if we apply all rules that do not
-- induce branching in one single step.
allRules s = let t = expand s in (axiom $ t) ++ (boxI $ t) ++ (conj $ t) -- ++ (tRule  t)


-- A sequent is provable iff there exists a set of premises that
-- prove the sequent such that all elements in the list of premises are
-- themselves provable.
sprovable :: Sequent -> Bool
sprovable s | seq s $ False = undefined -- force strictness
sprovable s = any  (\p -> (all sprovable p)) (allRules s)

-- specialisatino to formulas
provable :: Form -> Bool
provable p = sprovable [ p ]

--  test cases:
dp1 =   (neg (neg p)) \/ ((neg (neg q)) \/ r)   -- not provable

dp2 = box p \/ neg(box p) -- provable
dp3 = box p \/ neg(box(neg(neg p))) -- provable

dp4 = neg( neg(box p /\ neg(box p)) --> (box q /\ box p) /\ neg(box q))
dp5 = neg( neg(box p /\ neg(box p)) --> (box q /\ box p) /\ dia(neg q))

dp6 = (box p) /\ (dia q) --> (dia (p /\ q))  -- true?
dp7 = (box (dia (box p))) --> (dia (box (neg p)))  -- false?

level :: Int -> [Form]
level 0 = [var 0, var 1, neg $ var 0, neg $ var 1 ]
level n = let pbox = map box [ x | i <- [0 .. (n-1)], x <- (level i)]
              nbox = map (neg . box)  [ x | i <- [0 .. (n-1)], x <- (level i)]
          in
                                        pbox ++ nbox ++ [ p /\ q | p <- pbox, q <- nbox] ++ [neg (p /\ q) | p <- pbox, q <- nbox ]

tforms :: [ (Sequent, Sequent) ]
tforms = [ ([neg a, neg $ box a, b ], [neg $ box a, b])  | a <- level 2, b <- level 2]

ttest :: [ (Sequent, Sequent) ] -> String
ttest [] = []
ttest ( (s1, s2):as ) =
  let s1p = (sprovable s1) ;
            s2p = (sprovable s2)
  in if (s1p /= s2p) then "GOTCHA: " ++ (show s1) ++ (show s2) ++ "<"
                           else "*" ++ (ttest as)
