content: {- | Module     : ./GMP/GMP-CoLoSS/GMP/Prover.hs
   -  Description : Implementation of the generic sequent calculus
   -  Copyright   : (c) Daniel Hausmann & Lutz Schroeder, DFKI Lab Bremen,
   -                Rob Myers & Dirk Pattinson, Department of Computing, ICL
   -  License     : GPLv2 or higher, see LICENSE.txt
   -  Maintainer  : hausmann@dfki.de
   -  Stability   : provisional
   -  Portability : portable
   -
   - Provides the implementation of the generic proving function.
   - Also contains an optimized version of the proving function (using so-called
   - 'memoizing')
   -}
  
  module GMP.Prover where
  import Data.List
  import Data.Ratio
  import Data.Maybe
  
  import Debug.Trace
  
  import GMP.Logics.Generic
  import GMP.Logics.K
  
  {- ------------------------------------------------------------------------------
  sequent calculus implementation
  ------------------------------------------------------------------------------ -}
  
  {- Inference Rules
  map a sequent to the list 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. -}
  
  {- faster to check for atomic axioms
  axiom1 xs = [ []  | p <- xs, (Not q) <- xs, p==q] -}
  axiom_rule :: Sequent -> Premises
  axiom_rule (Sequent xs) = [ [[Sequent ([] :: [Formula (K (K (K ())))])]] |
                              (Atom n) <- xs, (Neg (Atom m)) <- xs, m == n]
  
  true_rule :: Sequent -> Premises
  true_rule (Sequent xs) = [ [[Sequent ([] :: [Formula (K (K (K ())))])]] | T <- xs]
  
  negfalse_rule :: Sequent -> Premises
  negfalse_rule (Sequent xs) = [ [[Sequent ([] :: [Formula (K (K (K ())))])]] |
                                 (Neg F) <- xs]
  
  conj_rule :: Sequent -> Premises
  conj_rule (Sequent as) = [ [[Sequent (p : delete f as)],
                              [Sequent (q : delete f as)]] | f@(And p q) <- as]
  
  -- the rule for the modal operator
  modal_rule :: [Bool] -> Sequent -> Premises
  modal_rule flags (Sequent xs) = emptify (fMatch flags xs)
  
  -- the rule for the modal operator - optimised version
  omodal_rule :: [Bool] -> [Sequent] -> Sequent -> Premises
  omodal_rule flags [Sequent ec] (Sequent xs) = emptify (fMatchOptimised flags xs [])
  
  {- 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.
  this is as good as it gets if we apply the individual rules
  message for the afterworld: if youm want to find proofs quickly,
  first look at the rules that induce branching.
  we can do slightly better if we apply all rules that do not
  induce branching in one single step. -}
  allRules :: [Bool] -> Sequent -> Premises
  allRules flags (Sequent seq) = let t = Sequent (expand seq)
                                     axioms = axiom_rule t
                                     trues = true_rule t
                                     negfalses = negfalse_rule t
                                     modals = modal_rule flags t
                                     conjs = conj_rule t
                                 in if flags !! 1 then
                                     trace ("\n  Axiom-rule: " ++ prettylll axioms ++
                                            "  True-rule: " ++ prettylll trues ++
                                            "  NegFalse-rule: " ++ prettylll negfalses ++
                                            "  Modal-rule: " ++ prettylll modals ++
                                            "  Conj-rule: " ++ prettylll conjs )
                                      (axioms ++ trues ++ negfalses ++ conjs ++ modals)
                                     else
                                      axioms ++ trues ++ negfalses ++ conjs ++ modals
  
  oallRules :: [Bool] -> [Sequent] -> Sequent -> Premises
  oallRules flags ec (Sequent seq) = let t = Sequent (expand seq)
                                         axioms = axiom_rule t
                                         trues = true_rule t
                                         negfalses = negfalse_rule t
                                         modals = omodal_rule flags ec t
                                         conjs = conj_rule t
                                     in trace
                                         ("\n  Axiom-rule: " ++ prettylll axioms ++
                                          "  True-rule: " ++ prettylll trues ++
                                          "  NegFalse-rule: " ++ prettylll negfalses ++
                                          "  Modal-rule: " ++ prettylll modals ++
                                          "  Conj-rule: " ++ prettylll conjs )
                                       (axioms ++ trues ++ negfalses ++ conjs ++ modals)
  
  {- 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 :: [Bool] -> Sequent -> Bool
  sprovable flags (Sequent []) = True
  sprovable flags (Sequent seq) = if flags !! 1 then
    trace ("\n  <Current Sequent:> " ++ pretty_seq (Sequent (expand seq))) $
      any (all (any (sprovable flags))) (allRules flags (Sequent seq))
    else any (all (any (sprovable flags))) (allRules flags (Sequent seq))
  
  -- optimized, alla
  osprovable :: [Bool] -> [Sequent] -> Sequent -> Bool
  osprovable flags ec (Sequent []) = True
  osprovable flags ec (Sequent seq) =
    trace ("\n  <Current Sequent:> " ++ pretty_seq (Sequent (expand seq))) $
    any (all (any (osprovable flags ec))) (oallRules flags ec (Sequent seq))
  
  -- specialisation to formulae
  provable :: (SigFeature a b (c d), Eq (a (b (c d)))) => Formula (a (b (c d))) -> [Bool] -> Bool
  provable phi flags = sprovable flags (Sequent [phi])
  
  oprovable :: (SigFeature a b (c d), Eq (a (b (c d)))) => [Bool] -> [Sequent] -> Formula (a (b (c d))) -> Bool
  oprovable flags ec phi = osprovable flags ec (Sequent [phi])
  
  -- a formula is satisfiable iff it's negation is not provable
  satisfiable :: (SigFeature a b (c d), Eq (a (b (c d)))) => Formula (a (b (c d))) -> [Bool] -> Bool
  satisfiable phi flags = not (provable (neg phi) flags)
  
  osatisfiable :: (SigFeature a b (c d), Eq (a (b (c d)))) => [Bool] -> [Sequent] -> Formula (a (b (c d))) -> Bool
  osatisfiable flags ec phi = not (oprovable flags ec (neg phi))
  