{- |
Module      :  ./Propositional/ProveWithTruthTable.hs
Description :  Provers for propositional logic
Copyright   :  (c) Till Mossakowski, Uni Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  experimental
Portability :  portable

A truth table prover for propositional logic.
Inefficient, but useful for learning purposes.
-}

module Propositional.ProveWithTruthTable
  ( ttProver
  , ttConsistencyChecker
  , ttConservativityChecker
  , allModels
  ) where

import Common.Lib.Tabular

import Propositional.AS_BASIC_Propositional
import Propositional.Sign
import qualified Propositional.Morphism as PMorphism
import qualified Propositional.ProverState as PState
import qualified Propositional.Sign as Sig
import Propositional.Sublogic (PropSL, top)

import qualified Logic.Prover as LP

import qualified Interfaces.GenericATPState as ATPState
import GUI.GenericATP
import GUI.Utils (infoDialog, createTextSaveDisplay)

import Common.ProofTree
import qualified Common.AS_Annotation as AS_Anno
import qualified Common.Id as Id

import qualified Data.Set as Set
import qualified Common.OrderedMap as OMap

import Common.Consistency
import qualified Common.Result as Result

import Data.Time (midnight)

-- * Prover implementation

-- | the name of the prover
ttS :: String
ttS :: String
ttS = "truth tables"

-- maximal size of the signature
maxSigSize :: Int
maxSigSize :: Int
maxSigSize = 17

-- display error message when signature is too large
sigTooLarge :: Int -> String
sigTooLarge :: Int -> String
sigTooLarge sigSize :: Int
sigSize = [String] -> String
unlines
  [ "Signature is too large."
  , "It should contain < " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
maxSigSize String -> String -> String
forall a. [a] -> [a] -> [a]
++ " symbols,"
  , "but it contains " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
sigSize String -> String -> String
forall a. [a] -> [a] -> [a]
++ " symbols." ]

ttHelpText :: String
ttHelpText :: String
ttHelpText = "An implementation of the truth table method.\n"
             String -> String -> String
forall a. [a] -> [a] -> [a]
++ "Very inefficient, but useful for learning and teaching\n"
             String -> String -> String
forall a. [a] -> [a] -> [a]
++ "Works well for signatures with less than " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
maxSigSize
             String -> String -> String
forall a. [a] -> [a] -> [a]
++ " symbols."

{- |
  Models and evaluation of sentences
-}

type Model = Set.Set Id.Id -- a model specifies which propositions are true

-- | show Bools in truth table
showBool :: Bool -> String
showBool :: Bool -> String
showBool True = "T"
showBool False = "F"

-- | evaluation of sentences in a model
eval :: Model -> FORMULA -> Bool
eval :: Model -> FORMULA -> Bool
eval m :: Model
m (Negation phi :: FORMULA
phi _) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Model -> FORMULA -> Bool
eval Model
m FORMULA
phi
eval m :: Model
m (Conjunction phis :: [FORMULA]
phis _) = (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Model -> FORMULA -> Bool
eval Model
m) [FORMULA]
phis
eval m :: Model
m (Disjunction phis :: [FORMULA]
phis _) = (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Model -> FORMULA -> Bool
eval Model
m) [FORMULA]
phis
eval m :: Model
m (Implication phi1 :: FORMULA
phi1 phi2 :: FORMULA
phi2 _) = Bool -> Bool
not (Model -> FORMULA -> Bool
eval Model
m FORMULA
phi1) Bool -> Bool -> Bool
|| Model -> FORMULA -> Bool
eval Model
m FORMULA
phi2
eval m :: Model
m (Equivalence phi1 :: FORMULA
phi1 phi2 :: FORMULA
phi2 _) = Model -> FORMULA -> Bool
eval Model
m FORMULA
phi1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Model -> FORMULA -> Bool
eval Model
m FORMULA
phi2
eval _ (True_atom _) = Bool
True
eval _ (False_atom _) = Bool
False
eval m :: Model
m (Predication ident :: Token
ident) = Token -> Id
Id.simpleIdToId Token
ident Id -> Model -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Model
m

evalNamed :: Model -> AS_Anno.Named FORMULA -> Bool
evalNamed :: Model -> Named FORMULA -> Bool
evalNamed m :: Model
m = Model -> FORMULA -> Bool
eval Model
m (FORMULA -> Bool)
-> (Named FORMULA -> FORMULA) -> Named FORMULA -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named FORMULA -> FORMULA
forall s a. SenAttr s a -> s
AS_Anno.sentence

{- |
  Evaluation of (co)freeness constraints
-}

-- | amalgamation of models
amalg :: Model -> Model -> Model
amalg :: Model -> Model -> Model
amalg = Model -> Model -> Model
forall a. Ord a => Set a -> Set a -> Set a
Set.union

data FormulaOrFree =
     Formula FORMULA
   | FreeConstraint (LP.FreeDefMorphism FORMULA PMorphism.Morphism)

evalNamedFormulaOrFree :: Model -> AS_Anno.Named FormulaOrFree -> Bool
evalNamedFormulaOrFree :: Model -> Named FormulaOrFree -> Bool
evalNamedFormulaOrFree m :: Model
m = Model -> FormulaOrFree -> Bool
evalFormulaOrFree Model
m (FormulaOrFree -> Bool)
-> (Named FormulaOrFree -> FormulaOrFree)
-> Named FormulaOrFree
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named FormulaOrFree -> FormulaOrFree
forall s a. SenAttr s a -> s
AS_Anno.sentence

evalFormulaOrFree :: Model -> FormulaOrFree -> Bool
evalFormulaOrFree :: Model -> FormulaOrFree -> Bool
evalFormulaOrFree m :: Model
m (Formula phi :: FORMULA
phi) = Model -> FORMULA -> Bool
eval Model
m FORMULA
phi
evalFormulaOrFree m :: Model
m (FreeConstraint freedef :: FreeDefMorphism FORMULA Morphism
freedef) = Model -> FreeDefMorphism FORMULA Morphism -> Bool
evalFree Model
m FreeDefMorphism FORMULA Morphism
freedef

reduceModel :: Sig.Sign -> Model -> Model
reduceModel :: Sign -> Model -> Model
reduceModel sig :: Sign
sig m :: Model
m = Model -> Model -> Model
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Model
m (Sign -> Model
items Sign
sig)

leq :: Model -> Model -> Bool
leq :: Model -> Model -> Bool
leq = Model -> Model -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf

isMin :: Bool -> Model -> [Model] -> Bool
isMin :: Bool -> Model -> [Model] -> Bool
isMin isCo :: Bool
isCo m :: Model
m = (Model -> Bool) -> [Model] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ m' :: Model
m' -> if Bool
isCo then Model -> Model -> Bool
leq Model
m' Model
m else Model -> Model -> Bool
leq Model
m Model
m')

evalFree :: Model
         -> LP.FreeDefMorphism FORMULA PMorphism.Morphism
         -> Bool
evalFree :: Model -> FreeDefMorphism FORMULA Morphism -> Bool
evalFree m :: Model
m freedef :: FreeDefMorphism FORMULA Morphism
freedef =
  let diffsig :: Sign
diffsig = Model -> Sign
Sign (Sign -> Model
items Sign
freetar Model -> Model -> Model
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Sign -> Model
items Sign
freesrc)
      mred :: Model
mred = Sign -> Model -> Model
reduceModel Sign
freesrc Model
m
      modelsOverMred :: [Model]
modelsOverMred = (Model -> Model) -> [Model] -> [Model]
forall a b. (a -> b) -> [a] -> [b]
map (Model
mred Model -> Model -> Model
`amalg`) (Sign -> [Model]
allModels Sign
diffsig)
      modelClass :: [Model]
modelClass = (FORMULA -> [Model] -> [Model]) -> [Model] -> [FORMULA] -> [Model]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Model -> Bool) -> [Model] -> [Model]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Model -> Bool) -> [Model] -> [Model])
-> (FORMULA -> Model -> Bool) -> FORMULA -> [Model] -> [Model]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Model -> FORMULA -> Bool) -> FORMULA -> Model -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Model -> FORMULA -> Bool
eval) [Model]
modelsOverMred [FORMULA]
freeth
  in (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Model -> FORMULA -> Bool
eval Model
m) [FORMULA]
freeth        -- the model satisfies the axioms ...
     Bool -> Bool -> Bool
&& Bool -> Model -> [Model] -> Bool
isMin Bool
isCo Model
m [Model]
modelClass -- ... and is the minimal one that does so
  where freemor :: Morphism
freemor = FreeDefMorphism FORMULA Morphism -> Morphism
forall sentence morphism.
FreeDefMorphism sentence morphism -> morphism
LP.freeDefMorphism FreeDefMorphism FORMULA Morphism
freedef
        freesrc :: Sign
freesrc = Morphism -> Sign
PMorphism.source Morphism
freemor
        freetar :: Sign
freetar = Morphism -> Sign
PMorphism.target Morphism
freemor
        freeth :: [FORMULA]
freeth = (Named FORMULA -> FORMULA) -> [Named FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map Named FORMULA -> FORMULA
forall s a. SenAttr s a -> s
AS_Anno.sentence ([Named FORMULA] -> [FORMULA]) -> [Named FORMULA] -> [FORMULA]
forall a b. (a -> b) -> a -> b
$ FreeDefMorphism FORMULA Morphism -> [Named FORMULA]
forall sentence morphism.
FreeDefMorphism sentence morphism -> [Named sentence]
LP.freeTheory FreeDefMorphism FORMULA Morphism
freedef
        isCo :: Bool
isCo = FreeDefMorphism FORMULA Morphism -> Bool
forall sentence morphism. FreeDefMorphism sentence morphism -> Bool
LP.isCofree FreeDefMorphism FORMULA Morphism
freedef

-- | generate all models for a signature
allModels :: Sign -> [Model]
allModels :: Sign -> [Model]
allModels sig :: Sign
sig = [Id] -> [Model]
forall a. Ord a => [a] -> [Set a]
allModels1 ([Id] -> [Model]) -> [Id] -> [Model]
forall a b. (a -> b) -> a -> b
$ Model -> [Id]
forall a. Set a -> [a]
Set.toList (Model -> [Id]) -> Model -> [Id]
forall a b. (a -> b) -> a -> b
$ Sign -> Model
items Sign
sig
  where allModels1 :: [a] -> [Set a]
allModels1 [] = [Set a
forall a. Set a
Set.empty]
        allModels1 (p :: a
p : rest :: [a]
rest) =
          let models :: [Set a]
models = [a] -> [Set a]
allModels1 [a]
rest
           in [Set a]
models [Set a] -> [Set a] -> [Set a]
forall a. [a] -> [a] -> [a]
++ (Set a -> Set a) -> [Set a] -> [Set a]
forall a b. (a -> b) -> [a] -> [b]
map (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
p) [Set a]
models

data TTExtRow =
     TTExtRow { TTExtRow -> [Bool]
rextprops, TTExtRow -> [Bool]
rextaxioms :: [Bool]
              , TTExtRow -> Bool
rextIsModel :: Bool
              }

data TTRow =
     TTRow { TTRow -> [Bool]
rprops, TTRow -> [Bool]
raxioms :: [Bool]
           , TTRow -> Maybe Bool
rgoal :: Maybe Bool
           , TTRow -> [TTExtRow]
rextrows :: [TTExtRow]
           , TTRow -> Bool
rIsModel :: Bool
           , TTRow -> Bool
rIsOK :: Bool
           }

data TTHead =
     TTHead { TTHead -> [String]
hprops, TTHead -> [String]
haxioms, TTHead -> [String]
hextprops, TTHead -> [String]
hextaxioms :: [String]
            , TTHead -> Maybe String
hgoal :: Maybe String
            }

data TruthTable =
     TruthTable { TruthTable -> TTHead
thead :: TTHead
                , TruthTable -> [TTRow]
trows :: [TTRow]
                }

renderTT :: TruthTable -> Table String String String
renderTT :: TruthTable -> Table String String String
renderTT tt :: TruthTable
tt = Header String
-> Header String -> [[String]] -> Table String String String
forall rh ch a. Header rh -> Header ch -> [[a]] -> Table rh ch a
Table Header String
rowHeaders Header String
header [[String]]
table
  where
  hextpropsTT :: [String]
hextpropsTT = TTHead -> [String]
hextprops (TruthTable -> TTHead
thead TruthTable
tt)
  hextaxiomsTT :: [String]
hextaxiomsTT = TTHead -> [String]
hextaxioms (TruthTable -> TTHead
thead TruthTable
tt)
  rowsTT :: [TTRow]
rowsTT = TruthTable -> [TTRow]
trows TruthTable
tt
  header :: Header String
header = Properties -> [Header String] -> Header String
forall h. Properties -> [Header h] -> Header h
Group Properties
DoubleLine
           ( [ Properties -> [Header String] -> Header String
forall h. Properties -> [Header h] -> Header h
Group Properties
SingleLine ((String -> Header String) -> [String] -> [Header String]
forall a b. (a -> b) -> [a] -> [b]
map String -> Header String
forall h. h -> Header h
Header (TTHead -> [String]
hprops (TruthTable -> TTHead
thead TruthTable
tt)))
             , Properties -> [Header String] -> Header String
forall h. Properties -> [Header h] -> Header h
Group Properties
SingleLine ((String -> Header String) -> [String] -> [Header String]
forall a b. (a -> b) -> [a] -> [b]
map String -> Header String
forall h. h -> Header h
Header (TTHead -> [String]
haxioms (TruthTable -> TTHead
thead TruthTable
tt)))]
             [Header String] -> [Header String] -> [Header String]
forall a. [a] -> [a] -> [a]
++ (if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
hextpropsTT Bool -> Bool -> Bool
&& [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
hextaxiomsTT then []
                 else [ String -> Header String
forall h. h -> Header h
Header ""
                      , Properties -> [Header String] -> Header String
forall h. Properties -> [Header h] -> Header h
Group Properties
SingleLine ((String -> Header String) -> [String] -> [Header String]
forall a b. (a -> b) -> [a] -> [b]
map String -> Header String
forall h. h -> Header h
Header [String]
hextpropsTT)
                      , Properties -> [Header String] -> Header String
forall h. Properties -> [Header h] -> Header h
Group Properties
SingleLine ((String -> Header String) -> [String] -> [Header String]
forall a b. (a -> b) -> [a] -> [b]
map String -> Header String
forall h. h -> Header h
Header [String]
hextaxiomsTT)])
             [Header String] -> [Header String] -> [Header String]
forall a. [a] -> [a] -> [a]
++ case TTHead -> Maybe String
hgoal (TruthTable -> TTHead
thead TruthTable
tt) of
                 Nothing -> []
                 Just g :: String
g -> [Properties -> [Header String] -> Header String
forall h. Properties -> [Header h] -> Header h
Group Properties
DoubleLine [String -> Header String
forall h. h -> Header h
Header String
g]])
  rowtype :: TTRow -> String
rowtype r :: TTRow
r = (if TTRow -> Bool
rIsModel TTRow
r then "M" else " ")
              String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if TTRow -> Bool
rIsOK TTRow
r then (if TTRow -> Bool
rIsModel TTRow
r then "+" else "o")
                            else "-")
  rowHeader :: TTRow -> Header String
rowHeader r :: TTRow
r = Properties -> [Header String] -> Header String
forall h. Properties -> [Header h] -> Header h
Group Properties
NoLine
    ([Header String] -> Header String)
-> [Header String] -> Header String
forall a b. (a -> b) -> a -> b
$ String -> Header String
forall h. h -> Header h
Header (TTRow -> String
rowtype TTRow
r) Header String -> [Header String] -> [Header String]
forall a. a -> [a] -> [a]
: (Int -> Header String) -> [Int] -> [Header String]
forall a b. (a -> b) -> [a] -> [b]
map (Header String -> Int -> Header String
forall a b. a -> b -> a
const (String -> Header String
forall h. h -> Header h
Header "")) [2 .. [TTExtRow] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (TTRow -> [TTExtRow]
rextrows TTRow
r)]
  rowHeaders :: Header String
rowHeaders = if (TTRow -> Bool) -> [TTRow] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([TTExtRow] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([TTExtRow] -> Bool) -> (TTRow -> [TTExtRow]) -> TTRow -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TTRow -> [TTExtRow]
rextrows) [TTRow]
rowsTT
    then Properties -> [Header String] -> Header String
forall h. Properties -> [Header h] -> Header h
Group Properties
NoLine ((TTRow -> Header String) -> [TTRow] -> [Header String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Header String
forall h. h -> Header h
Header (String -> Header String)
-> (TTRow -> String) -> TTRow -> Header String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TTRow -> String
rowtype) [TTRow]
rowsTT)
    else Properties -> [Header String] -> Header String
forall h. Properties -> [Header h] -> Header h
Group Properties
SingleLine ((TTRow -> Header String) -> [TTRow] -> [Header String]
forall a b. (a -> b) -> [a] -> [b]
map TTRow -> Header String
rowHeader [TTRow]
rowsTT)
  makeExtRow :: TTExtRow -> [String]
makeExtRow e :: TTExtRow
e = (if TTExtRow -> Bool
rextIsModel TTExtRow
e then "M" else "") String -> [String] -> [String]
forall a. a -> [a] -> [a]
:
    (Bool -> String) -> [Bool] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Bool -> String
showBool (TTExtRow -> [Bool]
rextprops TTExtRow
e) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Bool -> String) -> [Bool] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Bool -> String
showBool (TTExtRow -> [Bool]
rextaxioms TTExtRow
e)
  makeRow :: TTRow -> [[String]]
makeRow r :: TTRow
r =
    let common :: [String]
common = (Bool -> String) -> [Bool] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Bool -> String
showBool (TTRow -> [Bool]
rprops TTRow
r) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Bool -> String) -> [Bool] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Bool -> String
showBool (TTRow -> [Bool]
raxioms TTRow
r) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                 case TTRow -> Maybe Bool
rgoal TTRow
r of
                   Nothing -> []
                   Just g :: Bool
g -> [Bool -> String
showBool Bool
g]
        emptyPrefix :: [String]
emptyPrefix = (Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Int -> String
forall a b. a -> b -> a
const "") [1 .. [String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
common]
    in case (TTExtRow -> [String]) -> [TTExtRow] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map TTExtRow -> [String]
makeExtRow (TTRow -> [TTExtRow]
rextrows TTRow
r) of
       [] -> [[String]
common]
       e :: [String]
e : extrows :: [[String]]
extrows -> ([String]
common [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
e) [String] -> [[String]] -> [[String]]
forall a. a -> [a] -> [a]
: ([String] -> [String]) -> [[String]] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map ([String]
emptyPrefix [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++) [[String]]
extrows
  table :: [[String]]
table = (TTRow -> [[String]]) -> [TTRow] -> [[String]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TTRow -> [[String]]
makeRow [TTRow]
rowsTT

{- |
  The Prover implementation.

  Implemented are: a prover GUI.
-}
ttProver :: LP.Prover Sig.Sign FORMULA PMorphism.Morphism PropSL ProofTree
ttProver :: Prover Sign FORMULA Morphism PropSL ProofTree
ttProver = String
-> PropSL
-> (String
    -> Theory Sign FORMULA ProofTree
    -> [FreeDefMorphism FORMULA Morphism]
    -> IO [ProofStatus ProofTree])
-> Prover Sign FORMULA Morphism PropSL ProofTree
forall sublogics theory sentence morphism proof_tree.
String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO [ProofStatus proof_tree])
-> ProverTemplate theory sentence morphism sublogics proof_tree
LP.mkProverTemplate String
ttS PropSL
top String
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO [ProofStatus ProofTree]
ttProveGUI

{- |
   The Consistency Cheker.
-}
ttConsistencyChecker :: LP.ConsChecker Sig.Sign FORMULA PropSL
                                  PMorphism.Morphism ProofTree
ttConsistencyChecker :: ConsChecker Sign FORMULA PropSL Morphism ProofTree
ttConsistencyChecker = String
-> PropSL
-> (String
    -> TacticScript
    -> TheoryMorphism Sign FORMULA Morphism ProofTree
    -> [FreeDefMorphism FORMULA Morphism]
    -> IO (CCStatus ProofTree))
-> ConsChecker Sign FORMULA PropSL Morphism ProofTree
forall sublogics sign sentence morphism proof_tree.
String
-> sublogics
-> (String
    -> TacticScript
    -> TheoryMorphism sign sentence morphism proof_tree
    -> [FreeDefMorphism sentence morphism]
    -> IO (CCStatus proof_tree))
-> ConsChecker sign sentence sublogics morphism proof_tree
LP.mkConsChecker String
ttS PropSL
top String
-> TacticScript
-> TheoryMorphism Sign FORMULA Morphism ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO (CCStatus ProofTree)
consCheck

consCheck :: String -> LP.TacticScript
          -> LP.TheoryMorphism Sig.Sign FORMULA PMorphism.Morphism ProofTree
          -> [LP.FreeDefMorphism FORMULA PMorphism.Morphism]
          -- ^ free definitions
          -> IO (LP.CCStatus ProofTree)
consCheck :: String
-> TacticScript
-> TheoryMorphism Sign FORMULA Morphism ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO (CCStatus ProofTree)
consCheck _ _ tm :: TheoryMorphism Sign FORMULA Morphism ProofTree
tm _freedefs :: [FreeDefMorphism FORMULA Morphism]
_freedefs = case TheoryMorphism Sign FORMULA Morphism ProofTree
-> Theory Sign FORMULA ProofTree
forall sign sen mor proof_tree.
TheoryMorphism sign sen mor proof_tree
-> Theory sign sen proof_tree
LP.tTarget TheoryMorphism Sign FORMULA Morphism ProofTree
tm of
  LP.Theory sig :: Sign
sig nSens :: ThSens FORMULA (ProofStatus ProofTree)
nSens ->
    let sigSize :: Int
sigSize = Model -> Int
forall a. Set a -> Int
Set.size (Sign -> Model
items Sign
sig) in
    if Int
sigSize Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
maxSigSize then
      CCStatus ProofTree -> IO (CCStatus ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (CCStatus ProofTree -> IO (CCStatus ProofTree))
-> CCStatus ProofTree -> IO (CCStatus ProofTree)
forall a b. (a -> b) -> a -> b
$ ProofTree -> TimeOfDay -> Maybe Bool -> CCStatus ProofTree
forall proof_tree.
proof_tree -> TimeOfDay -> Maybe Bool -> CCStatus proof_tree
LP.CCStatus (String -> ProofTree
ProofTree (String -> ProofTree) -> String -> ProofTree
forall a b. (a -> b) -> a -> b
$ Int -> String
sigTooLarge Int
sigSize) TimeOfDay
midnight Maybe Bool
forall a. Maybe a
Nothing
    else do
      let axs :: [(String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))]
axs = ((String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))
 -> Bool)
-> [(String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))]
-> [(String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))]
forall a. (a -> Bool) -> [a] -> [a]
filter (SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)) -> Bool
forall s a. SenAttr s a -> Bool
AS_Anno.isAxiom (SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)) -> Bool)
-> ((String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))
    -> SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))
-> (String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))
-> SenAttr FORMULA (ThmStatus (ProofStatus ProofTree))
forall a b. (a, b) -> b
snd) ([(String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))]
 -> [(String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))])
-> [(String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))]
-> [(String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))]
forall a b. (a -> b) -> a -> b
$ ThSens FORMULA (ProofStatus ProofTree)
-> [(String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))]
forall k a. Ord k => OMap k a -> [(k, a)]
OMap.toList ThSens FORMULA (ProofStatus ProofTree)
nSens
          models :: [Model]
models = Sign -> [Model]
allModels Sign
sig
          sigList :: [Id]
sigList = Model -> [Id]
forall a. Set a -> [a]
Set.toList (Model -> [Id]) -> Model -> [Id]
forall a b. (a -> b) -> a -> b
$ Sign -> Model
items Sign
sig
          heading :: TTHead
heading = TTHead :: [String]
-> [String] -> [String] -> [String] -> Maybe String -> TTHead
TTHead { hprops :: [String]
hprops = (Id -> String) -> [Id] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Id -> String
forall a. Show a => a -> String
show [Id]
sigList
                           , haxioms :: [String]
haxioms = ((String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))
 -> String)
-> [(String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))]
-> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))
-> String
forall a b. (a, b) -> a
fst [(String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))]
axs
                           , hextprops :: [String]
hextprops = [], hextaxioms :: [String]
hextaxioms = []
                           , hgoal :: Maybe String
hgoal = Maybe String
forall a. Maybe a
Nothing
                           }
          mkRow :: Model -> TTRow
mkRow m :: Model
m =
            let evalAx :: [Bool]
evalAx = ((String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))
 -> Bool)
-> [(String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))]
-> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Model -> FORMULA -> Bool
eval Model
m (FORMULA -> Bool)
-> ((String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))
    -> FORMULA)
-> (String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)) -> FORMULA
forall s a. SenAttr s a -> s
AS_Anno.sentence (SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)) -> FORMULA)
-> ((String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))
    -> SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))
-> (String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))
-> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))
-> SenAttr FORMULA (ThmStatus (ProofStatus ProofTree))
forall a b. (a, b) -> b
snd) [(String, SenAttr FORMULA (ThmStatus (ProofStatus ProofTree)))]
axs
                isModel :: Bool
isModel = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
evalAx
            in TTRow :: [Bool]
-> [Bool] -> Maybe Bool -> [TTExtRow] -> Bool -> Bool -> TTRow
TTRow { rprops :: [Bool]
rprops = (Id -> Bool) -> [Id] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Id -> Model -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Model
m) [Id]
sigList
                     , raxioms :: [Bool]
raxioms = [Bool]
evalAx
                     , rextrows :: [TTExtRow]
rextrows = []
                     , rgoal :: Maybe Bool
rgoal = Maybe Bool
forall a. Maybe a
Nothing
                     , rIsModel :: Bool
rIsModel = Bool
isModel
                     , rIsOK :: Bool
rIsOK = Bool
isModel
                     }
          rows :: [TTRow]
rows = (Model -> TTRow) -> [Model] -> [TTRow]
forall a b. (a -> b) -> [a] -> [b]
map Model -> TTRow
mkRow [Model]
models
          isOK :: Bool
isOK = (TTRow -> Bool) -> [TTRow] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TTRow -> Bool
rIsOK [TTRow]
rows
          table :: TruthTable
table = TruthTable :: TTHead -> [TTRow] -> TruthTable
TruthTable { thead :: TTHead
thead = TTHead
heading
                             , trows :: [TTRow]
trows = [TTRow]
rows
                             }
          legend :: String
legend = "Legend:\nM+ = model of the axioms\n"
                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ " - = not a model of the axioms\n"
          body :: String
body = String
legend String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> String)
-> (String -> String)
-> (String -> String)
-> Table String String String
-> String
forall rh ch a.
(rh -> String)
-> (ch -> String) -> (a -> String) -> Table rh ch a -> String
render String -> String
forall a. a -> a
id String -> String
forall a. a -> a
id String -> String
forall a. a -> a
id (TruthTable -> Table String String String
renderTT TruthTable
table)
      CCStatus ProofTree -> IO (CCStatus ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (CCStatus ProofTree -> IO (CCStatus ProofTree))
-> CCStatus ProofTree -> IO (CCStatus ProofTree)
forall a b. (a -> b) -> a -> b
$ ProofTree -> TimeOfDay -> Maybe Bool -> CCStatus ProofTree
forall proof_tree.
proof_tree -> TimeOfDay -> Maybe Bool -> CCStatus proof_tree
LP.CCStatus (String -> ProofTree
ProofTree String
body) TimeOfDay
midnight (Maybe Bool -> CCStatus ProofTree)
-> Maybe Bool -> CCStatus ProofTree
forall a b. (a -> b) -> a -> b
$ Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
isOK

-- ** prover GUI

{- |
  Invokes the generic prover GUI.
-}
ttProveGUI :: String -- ^ theory name
          -> LP.Theory Sig.Sign FORMULA ProofTree
          -> [LP.FreeDefMorphism FORMULA PMorphism.Morphism]
          -- ^ free definitions
          -> IO [LP.ProofStatus ProofTree] -- ^ proof status for each goal
ttProveGUI :: String
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO [ProofStatus ProofTree]
ttProveGUI thName :: String
thName th :: Theory Sign FORMULA ProofTree
th freedefs :: [FreeDefMorphism FORMULA Morphism]
freedefs =
  ATPFunctions Sign FORMULA Morphism ProofTree PropProverState
-> Bool
-> String
-> String
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> ProofTree
-> IO [ProofStatus ProofTree]
forall sentence proof_tree sign mor pst.
(Show sentence, Ord proof_tree, Ord sentence) =>
ATPFunctions sign sentence mor proof_tree pst
-> Bool
-> String
-> String
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> IO [ProofStatus proof_tree]
genericATPgui (String
-> ATPFunctions Sign FORMULA Morphism ProofTree PropProverState
atpFun String
thName) Bool
True (Prover Sign FORMULA Morphism PropSL ProofTree -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
LP.proverName Prover Sign FORMULA Morphism PropSL ProofTree
ttProver) String
thName Theory Sign FORMULA ProofTree
th
                [FreeDefMorphism FORMULA Morphism]
freedefs ProofTree
emptyProofTree

{- |
  Record for prover specific functions. This is used by both GUI and command
  line interface.
-}
atpFun :: String -- ^ Theory name
  -> ATPState.ATPFunctions Sig.Sign FORMULA PMorphism.Morphism ProofTree
     PState.PropProverState
atpFun :: String
-> ATPFunctions Sign FORMULA Morphism ProofTree PropProverState
atpFun thName :: String
thName = ATPFunctions :: forall sign sentence morphism proof_tree pst.
InitialProverState sign sentence morphism pst
-> (String -> String)
-> (pst -> Named sentence -> pst)
-> (pst -> Named sentence -> [String] -> IO String)
-> String
-> String
-> FileExtensions
-> RunProver sentence proof_tree pst
-> (GenericConfig proof_tree -> [String])
-> ATPFunctions sign sentence morphism proof_tree pst
ATPState.ATPFunctions
                { initialProverState :: InitialProverState Sign FORMULA Morphism PropProverState
ATPState.initialProverState = InitialProverState Sign FORMULA Morphism PropProverState
PState.propProverState
                , goalOutput :: PropProverState -> Named FORMULA -> [String] -> IO String
ATPState.goalOutput = String -> PropProverState -> Named FORMULA -> [String] -> IO String
goalProblem String
thName
                , atpTransSenName :: String -> String
ATPState.atpTransSenName = String -> String
PState.transSenName
                , atpInsertSentence :: PropProverState -> Named FORMULA -> PropProverState
ATPState.atpInsertSentence = PropProverState -> Named FORMULA -> PropProverState
PState.insertSentence
                , proverHelpText :: String
ATPState.proverHelpText = String
ttHelpText
                , runProver :: RunProver FORMULA ProofTree PropProverState
ATPState.runProver = RunProver FORMULA ProofTree PropProverState
runTt
                , batchTimeEnv :: String
ATPState.batchTimeEnv = ""
                , fileExtensions :: FileExtensions
ATPState.fileExtensions = FileExtensions :: String -> String -> String -> FileExtensions
ATPState.FileExtensions
                    { problemOutput :: String
ATPState.problemOutput = ".tt"
                    , proverOutput :: String
ATPState.proverOutput = ".tt"
                    , theoryConfiguration :: String
ATPState.theoryConfiguration = ".tt"}
                , createProverOptions :: GenericConfig ProofTree -> [String]
ATPState.createProverOptions = GenericConfig ProofTree -> [String]
createTtOptions
                }

defaultProofStatus :: AS_Anno.Named FORMULA -> LP.ProofStatus ProofTree
defaultProofStatus :: Named FORMULA -> ProofStatus ProofTree
defaultProofStatus nGoal :: Named FORMULA
nGoal =
  String -> String -> ProofTree -> ProofStatus ProofTree
forall pt. Ord pt => String -> String -> pt -> ProofStatus pt
LP.openProofStatus (Named FORMULA -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named FORMULA
nGoal) (Prover Sign FORMULA Morphism PropSL ProofTree -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
LP.proverName Prover Sign FORMULA Morphism PropSL ProofTree
ttProver)
                     ProofTree
emptyProofTree

{- |
  Runs tt.
-}

runTt :: PState.PropProverState
      {- ^ logical part containing the input Sign and
      axioms and possibly goals that have been proved
      earlier as additional axioms -}
      -> ATPState.GenericConfig ProofTree
      -- ^ configuration to use
      -> Bool
      -- ^ True means save DIMACS file
      -> String
      -- ^ Name of the theory
      -> AS_Anno.Named FORMULA
      -- ^ Goal to prove
      -> IO (ATPState.ATPRetval, ATPState.GenericConfig ProofTree)
      -- ^ (retval, configuration with proof status and complete output)
runTt :: RunProver FORMULA ProofTree PropProverState
runTt pState :: PropProverState
pState cfg :: GenericConfig ProofTree
cfg _ _thName :: String
_thName nGoal :: Named FORMULA
nGoal =
  let sig :: Sign
sig = PropProverState -> Sign
PState.initialSignature PropProverState
pState
      sigSize :: Int
sigSize = Model -> Int
forall a. Set a -> Int
Set.size (Model -> Int) -> Model -> Int
forall a b. (a -> b) -> a -> b
$ Sign -> Model
items Sign
sig
   in if Int
sigSize Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
maxSigSize then do
        String -> String -> IO ()
infoDialog "Signature too large" (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> String
sigTooLarge Int
sigSize
        (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATPRetval
ATPState.ATPTLimitExceeded,
                GenericConfig ProofTree
cfg { proofStatus :: ProofStatus ProofTree
ATPState.proofStatus = Named FORMULA -> ProofStatus ProofTree
defaultProofStatus Named FORMULA
nGoal })
      else do
       let axs :: [Named FORMULA]
axs = PropProverState -> [Named FORMULA]
PState.initialAxioms PropProverState
pState
           freedefs :: [FreeDefMorphism FORMULA Morphism]
freedefs = PropProverState -> [FreeDefMorphism FORMULA Morphism]
PState.freeDefs PropProverState
pState
           nameFree :: FreeDefMorphism FORMULA Morphism -> Named FormulaOrFree
nameFree fd :: FreeDefMorphism FORMULA Morphism
fd =
              String -> FormulaOrFree -> Named FormulaOrFree
forall a s. a -> s -> SenAttr s a
AS_Anno.makeNamed (if FreeDefMorphism FORMULA Morphism -> Bool
forall sentence morphism. FreeDefMorphism sentence morphism -> Bool
LP.isCofree FreeDefMorphism FORMULA Morphism
fd then "cofree" else "free")
                                (FreeDefMorphism FORMULA Morphism -> FormulaOrFree
FreeConstraint FreeDefMorphism FORMULA Morphism
fd)
           sens :: [Named FormulaOrFree]
sens = (Named FORMULA -> Named FormulaOrFree)
-> [Named FORMULA] -> [Named FormulaOrFree]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA -> FormulaOrFree) -> Named FORMULA -> Named FormulaOrFree
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
AS_Anno.mapNamed FORMULA -> FormulaOrFree
Formula) [Named FORMULA]
axs [Named FormulaOrFree]
-> [Named FormulaOrFree] -> [Named FormulaOrFree]
forall a. [a] -> [a] -> [a]
++ (FreeDefMorphism FORMULA Morphism -> Named FormulaOrFree)
-> [FreeDefMorphism FORMULA Morphism] -> [Named FormulaOrFree]
forall a b. (a -> b) -> [a] -> [b]
map FreeDefMorphism FORMULA Morphism -> Named FormulaOrFree
nameFree [FreeDefMorphism FORMULA Morphism]
freedefs
           models :: [Model]
models = Sign -> [Model]
allModels Sign
sig
           sigList :: [Id]
sigList = Model -> [Id]
forall a. Set a -> [a]
Set.toList (Model -> [Id]) -> Model -> [Id]
forall a b. (a -> b) -> a -> b
$ Sign -> Model
items Sign
sig
           heading :: TTHead
heading =
             TTHead :: [String]
-> [String] -> [String] -> [String] -> Maybe String -> TTHead
TTHead { hprops :: [String]
hprops = (Id -> String) -> [Id] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Id -> String
forall a. Show a => a -> String
show [Id]
sigList
                    , haxioms :: [String]
haxioms = (Named FormulaOrFree -> String)
-> [Named FormulaOrFree] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Named FormulaOrFree -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr [Named FormulaOrFree]
sens
                    , hextprops :: [String]
hextprops = [], hextaxioms :: [String]
hextaxioms = []
                    , hgoal :: Maybe String
hgoal = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Named FORMULA -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named FORMULA
nGoal
                    }
           mkRow :: Model -> TTRow
mkRow m :: Model
m =
             let evalAx :: [Bool]
evalAx = (Named FormulaOrFree -> Bool) -> [Named FormulaOrFree] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Model -> Named FormulaOrFree -> Bool
evalNamedFormulaOrFree Model
m) [Named FormulaOrFree]
sens
                 evalGoal :: Bool
evalGoal = Model -> Named FORMULA -> Bool
evalNamed Model
m Named FORMULA
nGoal
                 isModel :: Bool
isModel = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
evalAx
             in TTRow :: [Bool]
-> [Bool] -> Maybe Bool -> [TTExtRow] -> Bool -> Bool -> TTRow
TTRow { rprops :: [Bool]
rprops = (Id -> Bool) -> [Id] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Id -> Model -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Model
m) [Id]
sigList
                      , raxioms :: [Bool]
raxioms = [Bool]
evalAx
                      , rextrows :: [TTExtRow]
rextrows = []
                      , rgoal :: Maybe Bool
rgoal = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
evalGoal
                      , rIsModel :: Bool
rIsModel = Bool
isModel
                      , rIsOK :: Bool
rIsOK = Bool -> Bool
not Bool
isModel Bool -> Bool -> Bool
|| Bool
evalGoal
                      }
           rows :: [TTRow]
rows = (Model -> TTRow) -> [Model] -> [TTRow]
forall a b. (a -> b) -> [a] -> [b]
map Model -> TTRow
mkRow [Model]
models
           isOK :: Bool
isOK = (TTRow -> Bool) -> [TTRow] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TTRow -> Bool
rIsOK [TTRow]
rows
           consistent :: Bool
consistent = (TTRow -> Bool) -> [TTRow] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TTRow -> Bool
rIsModel [TTRow]
rows
           table :: TruthTable
table = TruthTable :: TTHead -> [TTRow] -> TruthTable
TruthTable { thead :: TTHead
thead = TTHead
heading
                              , trows :: [TTRow]
trows = [TTRow]
rows
                              }
           legend :: String
legend = "Legend:\nM = model of the premises\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
             "+ = OK, model fulfills conclusion\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
             "- = not OK, counterexample for logical consequence\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
             "o = OK, premises are not fulfilled, hence conclusion is "
             String -> String -> String
forall a. [a] -> [a] -> [a]
++ "irrelevant\n"
           body :: String
body = String
legend String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> String)
-> (String -> String)
-> (String -> String)
-> Table String String String
-> String
forall rh ch a.
(rh -> String)
-> (ch -> String) -> (a -> String) -> Table rh ch a -> String
render String -> String
forall a. a -> a
id String -> String
forall a. a -> a
id String -> String
forall a. a -> a
id (TruthTable -> Table String String String
renderTT TruthTable
table)
       let status :: ProofStatus ProofTree
status = (Named FORMULA -> ProofStatus ProofTree
defaultProofStatus Named FORMULA
nGoal)
                     { goalStatus :: GoalStatus
LP.goalStatus = if Bool
isOK then Bool -> GoalStatus
LP.Proved Bool
consistent
                                               else GoalStatus
LP.Disproved
                     , usedAxioms :: [String]
LP.usedAxioms = (Named FormulaOrFree -> String)
-> [Named FormulaOrFree] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Named FormulaOrFree -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr [Named FormulaOrFree]
sens
                     }
       (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATPRetval
ATPState.ATPSuccess,
               GenericConfig ProofTree
cfg { proofStatus :: ProofStatus ProofTree
ATPState.proofStatus = ProofStatus ProofTree
status
                   , resultOutput :: [String]
ATPState.resultOutput = [String
body] })

{- |
  Creates a list of all options the truth table prover runs with.
  Only Option is the timelimit
-}
createTtOptions :: ATPState.GenericConfig ProofTree -> [String]
createTtOptions :: GenericConfig ProofTree -> [String]
createTtOptions _cfg :: GenericConfig ProofTree
_cfg = [] -- [(show $ configTimeLimit cfg)]

goalProblem :: String -- ^ name of the theory
            -> PState.PropProverState -- ^ initial Prover state
            -> AS_Anno.Named FORMULA -- ^ goal to prove
            -> [String] -- ^ Options (ignored)
            -> IO String
goalProblem :: String -> PropProverState -> Named FORMULA -> [String] -> IO String
goalProblem _ _ _ _ = String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return ""

{- |
  Conservativity check
-}

-- | Conservativity Check via truth table

-- TODO: check for injectivity!

ttConservativityChecker ::
              (Sign, [AS_Anno.Named FORMULA]) -- ^ Initial sign and formulas
           -> PMorphism.Morphism              -- ^ morhpism between specs
           -> [AS_Anno.Named FORMULA]         -- ^ Formulas of extended spec
           -> IO (Result.Result (Conservativity, [FORMULA]))
ttConservativityChecker :: (Sign, [Named FORMULA])
-> Morphism
-> [Named FORMULA]
-> IO (Result (Conservativity, [FORMULA]))
ttConservativityChecker (_, srcSens :: [Named FORMULA]
srcSens) mor :: Morphism
mor tarAxs :: [Named FORMULA]
tarAxs =
  let srcAxs :: [Named FORMULA]
srcAxs = (Named FORMULA -> Bool) -> [Named FORMULA] -> [Named FORMULA]
forall a. (a -> Bool) -> [a] -> [a]
filter Named FORMULA -> Bool
forall s a. SenAttr s a -> Bool
AS_Anno.isAxiom [Named FORMULA]
srcSens
      srcSig :: Model
srcSig = Sign -> Model
items (Sign -> Model) -> Sign -> Model
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
PMorphism.source Morphism
mor
      imageSig :: Model
imageSig = (Id -> Id) -> Model -> Model
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Morphism -> Id -> Id
PMorphism.applyMorphism Morphism
mor) Model
srcSig
      imageSigList :: [Id]
imageSigList = Model -> [Id]
forall a. Set a -> [a]
Set.toList Model
imageSig
      tarSig :: Model
tarSig = Sign -> Model
items (Sign -> Model) -> Sign -> Model
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
PMorphism.target Morphism
mor
      newSig :: Model
newSig = Model -> Model -> Model
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Model
tarSig Model
imageSig
      sigSize :: Int
sigSize = Model -> Int
forall a. Set a -> Int
Set.size Model
tarSig
  in if Int
sigSize Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
maxSigSize
    then Result (Conservativity, [FORMULA])
-> IO (Result (Conservativity, [FORMULA]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Conservativity, [FORMULA])
 -> IO (Result (Conservativity, [FORMULA])))
-> Result (Conservativity, [FORMULA])
-> IO (Result (Conservativity, [FORMULA]))
forall a b. (a -> b) -> a -> b
$ (Conservativity, [FORMULA]) -> Result (Conservativity, [FORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Conservativity
Unknown "signature too big", [])
    else do
      let imageAxs :: [Named FORMULA]
imageAxs = (Named FORMULA -> Named FORMULA)
-> [Named FORMULA] -> [Named FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA -> FORMULA) -> Named FORMULA -> Named FORMULA
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
AS_Anno.mapNamed (Morphism -> FORMULA -> FORMULA
PMorphism.mapSentenceH Morphism
mor)) [Named FORMULA]
srcAxs
          models :: [Model]
models = Sign -> [Model]
allModels (Model -> Sign
Sign Model
imageSig)
          newSigList :: [Id]
newSigList = Model -> [Id]
forall a. Set a -> [a]
Set.toList Model
newSig
          heading :: TTHead
heading =
            TTHead :: [String]
-> [String] -> [String] -> [String] -> Maybe String -> TTHead
TTHead { hprops :: [String]
hprops = (Id -> String) -> [Id] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Id -> String
forall a. Show a => a -> String
show [Id]
imageSigList,
                     haxioms :: [String]
haxioms = (Named FORMULA -> String) -> [Named FORMULA] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Named FORMULA -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr [Named FORMULA]
srcAxs,
                     hextprops :: [String]
hextprops = (Id -> String) -> [Id] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Id -> String
forall a. Show a => a -> String
show [Id]
newSigList,
                     hextaxioms :: [String]
hextaxioms = (Named FORMULA -> String) -> [Named FORMULA] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Named FORMULA -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr [Named FORMULA]
tarAxs,
                     hgoal :: Maybe String
hgoal = Maybe String
forall a. Maybe a
Nothing
                   }
          mkRow :: Model -> TTRow
mkRow m :: Model
m =
            let evalAx :: [Bool]
evalAx = (Named FORMULA -> Bool) -> [Named FORMULA] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Model -> Named FORMULA -> Bool
evalNamed Model
m) [Named FORMULA]
imageAxs
                isModel :: Bool
isModel = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
evalAx
                extmodels :: [Model]
extmodels = Sign -> [Model]
allModels (Model -> Sign
Sign Model
newSig)
                extrow :: Model -> TTExtRow
extrow m' :: Model
m' =
                  let evalExtAx :: [Bool]
evalExtAx = (Named FORMULA -> Bool) -> [Named FORMULA] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Model -> Named FORMULA -> Bool
evalNamed (Model
m Model -> Model -> Model
`amalg` Model
m')) [Named FORMULA]
tarAxs
                      isExtModel :: Bool
isExtModel = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
evalExtAx
                   in TTExtRow :: [Bool] -> [Bool] -> Bool -> TTExtRow
TTExtRow { rextprops :: [Bool]
rextprops = (Id -> Bool) -> [Id] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Id -> Model -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Model
m') [Id]
newSigList,
                                rextaxioms :: [Bool]
rextaxioms = [Bool]
evalExtAx,
                                rextIsModel :: Bool
rextIsModel = Bool
isExtModel
                              }
                extrows :: [TTExtRow]
extrows = (Model -> TTExtRow) -> [Model] -> [TTExtRow]
forall a b. (a -> b) -> [a] -> [b]
map Model -> TTExtRow
extrow [Model]
extmodels
            in TTRow :: [Bool]
-> [Bool] -> Maybe Bool -> [TTExtRow] -> Bool -> Bool -> TTRow
TTRow { rprops :: [Bool]
rprops = (Id -> Bool) -> [Id] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Id -> Model -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Model
m) [Id]
imageSigList,
                       raxioms :: [Bool]
raxioms = [Bool]
evalAx,
                       rgoal :: Maybe Bool
rgoal = Maybe Bool
forall a. Maybe a
Nothing,
                       rextrows :: [TTExtRow]
rextrows = if Bool
isModel then [TTExtRow]
extrows else [],
                       rIsModel :: Bool
rIsModel = Bool
isModel,
                       rIsOK :: Bool
rIsOK = Bool -> Bool
not Bool
isModel Bool -> Bool -> Bool
|| (TTExtRow -> Bool) -> [TTExtRow] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TTExtRow -> Bool
rextIsModel [TTExtRow]
extrows
                     }
          rows :: [TTRow]
rows = (Model -> TTRow) -> [Model] -> [TTRow]
forall a b. (a -> b) -> [a] -> [b]
map Model -> TTRow
mkRow [Model]
models
          isOK :: Bool
isOK = (TTRow -> Bool) -> [TTRow] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TTRow -> Bool
rIsOK [TTRow]
rows
          table :: TruthTable
table = TruthTable :: TTHead -> [TTRow] -> TruthTable
TruthTable { thead :: TTHead
thead = TTHead
heading,
                               trows :: [TTRow]
trows = [TTRow]
rows
                             }
          title :: String
title = "The extension is " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
isOK then "" else "not ")
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ "conservative"
          legend :: String
legend = "Legend:\n"
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ "M = model of the axioms\n"
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ "+ = OK, has expansion\n"
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ "- = not OK, has no expansion, hence conservativity fails\n"
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ "o = OK, not a model of the axioms, hence no expansion needed\n"
          body :: String
body = String
legend String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> String)
-> (String -> String)
-> (String -> String)
-> Table String String String
-> String
forall rh ch a.
(rh -> String)
-> (ch -> String) -> (a -> String) -> Table rh ch a -> String
render String -> String
forall a. a -> a
id String -> String
forall a. a -> a
id String -> String
forall a. a -> a
id (TruthTable -> Table String String String
renderTT TruthTable
table)
          res :: Conservativity
res = if Bool
isOK then Conservativity
Cons else Conservativity
Inconsistent
      String -> String -> String -> IO ()
createTextSaveDisplay String
title "unnamed" String
body
      Result (Conservativity, [FORMULA])
-> IO (Result (Conservativity, [FORMULA]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Conservativity, [FORMULA])
 -> IO (Result (Conservativity, [FORMULA])))
-> Result (Conservativity, [FORMULA])
-> IO (Result (Conservativity, [FORMULA]))
forall a b. (a -> b) -> a -> b
$ (Conservativity, [FORMULA]) -> Result (Conservativity, [FORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (Conservativity
res, [])