{-# LANGUAGE DeriveDataTypeable #-}

{- |

Module : ./Logic/Prover.hs

Description : General datastructures for theorem prover interfaces

Copyright : (c) Till Mossakowski, Klaus Luettich, Uni Bremen 2002-2005

License : GPLv2 or higher, see LICENSE.txt

Maintainer : till@informatik.uni-bremen.de

Stability : provisional

Portability : non-portable (deriving Typeable)

General datastructures for theorem prover interfaces

-}

module Logic.Prover where

import Common.AS_Annotation as AS_Anno

import Common.Doc

import Common.DocUtils

import Common.Result

import Common.ProofUtils

import Common.ProverTools

import qualified Common.OrderedMap as OMap

import qualified Data.Map as Map

import qualified Data.Set as Set

import Data.List

import Data.Maybe (isJust)

import Data.Time (TimeOfDay, midnight)

import Data.Typeable

import Control.Monad

import qualified Control.Concurrent as Concurrent

-- * pack sentences with their proofs

{- | instead of the sentence name (that will be the key into the order map)

the theorem status will be stored as attribute. The theorem status will be a

(wrapped) list of pairs (AnyComorphism, BasicProof) in G_theory, but a wrapped

list of (ProofStatus proof_tree) in a logic specific 'Theory'. -}

type SenStatus a tStatus = SenAttr a (ThmStatus tStatus)

thmStatus :: SenStatus a tStatus -> [tStatus]

thmStatus = getThmStatus . senAttr

-- | the wrapped list of proof scripts or (AnyComorphism, BasicProof) pairs

data ThmStatus a = ThmStatus { getThmStatus :: [a] }

deriving (Show, Eq, Ord, Typeable)

emptySenStatus :: SenStatus a b

emptySenStatus = makeNamed (ThmStatus []) $ error "emptySenStatus"

instance Pretty a => Pretty (OMap.ElemWOrd a) where

pretty = printOMapElemWOrd pretty

printOMapElemWOrd :: (a -> Doc) -> OMap.ElemWOrd a -> Doc

printOMapElemWOrd = (. OMap.ele)

-- | the map from labels to the theorem plus status (and position)

type ThSens a b = OMap.OMap String (SenStatus a b)

noSens :: ThSens a b

noSens = Map.empty

mapThSensValueM :: Monad m => (a -> m b) -> ThSens a c -> m (ThSens b c)

mapThSensValueM f = foldM (\ m (k, v) -> do

let oe = OMap.ele v

ns <- f $ sentence oe

let ne = oe { sentence = ns }

return $ Map.insert k v { OMap.ele = ne } m) Map.empty . Map.toList

{- | join and disambiguate

* separate Axioms from Theorems

* don't merge sentences with same key but different contents?

-}

joinSensAux :: (Ord a, Eq b) => ThSens a b -> ThSens a b

-> (ThSens a b, [(String, String)])

joinSensAux s1 s2 = let

l1 = Map.toList s1

updN n (_, e) = (n, e)

m = if null l1 then 0 else maximum $ map (OMap.order . snd) l1

l2 = map (\ (x, e) -> (x, e {OMap.order = m + OMap.order e }))

$ Map.toList s2

sl2 = genericDisambigSens m fst updN (Map.keysSet s1) l2

in (Map.fromList $ l1 ++ sl2,

zipWith (\ (n1, _) (n2, _) -> (n1, n2)) l2 sl2)

joinSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b

joinSens s1 = fst . joinSensAux s1

intersectSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b

intersectSens s1 s2 = let

sens1 = map sentence $ OMap.elems s1

sens2 = map sentence $ OMap.elems s2

sensI = Set.intersection (Set.fromList sens1) (Set.fromList sens2)

in toThSens $ map (AS_Anno.makeNamed "") $ Set.toList sensI

reduceSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b

reduceSens =

Map.fromList

. map head

. groupBy (\ (_, a) (_, b) -> sentence (OMap.ele a) == sentence (OMap.ele b))

. sortBy cmpSnd

. Map.toList

cmpSnd :: (Ord a1) => (String, OMap.ElemWOrd (SenStatus a1 b))

-> (String, OMap.ElemWOrd (SenStatus a1 b)) -> Ordering

cmpSnd (_, a) (_, b) = cmpSenEle a b

cmpSenEle :: (Ord a1) => OMap.ElemWOrd (SenStatus a1 b)

-> OMap.ElemWOrd (SenStatus a1 b) -> Ordering

cmpSenEle x y = case (OMap.ele x, OMap.ele y) of

(d1, d2) -> compare

(sentence d1, isAxiom d2, isDef d2) (sentence d2, isAxiom d1, isDef d1)

mapValue :: (a -> b) -> SenStatus a c -> SenStatus b c

mapValue f d = d { sentence = f $ sentence d }

{- | sets the field isAxiom according to the boolean value;

if isAxiom is False for a sentence and set to True,

the field wasTheorem is set to True.

-}

markAsAxiom :: Ord a => Bool -> ThSens a b -> ThSens a b

markAsAxiom b = OMap.map $ \ d -> d

{ isAxiom = b

, wasTheorem = b && (not (isAxiom d) || wasTheorem d) }

markAsGoal :: Ord a => ThSens a b -> ThSens a b

markAsGoal = markAsAxiom False

toNamedList :: ThSens a b -> [AS_Anno.Named a]

toNamedList = map (uncurry toNamed) . OMap.toList

toNamed :: String -> SenStatus a b -> AS_Anno.Named a

toNamed k s = s { AS_Anno.senAttr = k }

-- | putting Sentences from a list into a map

toThSens :: Ord a => [AS_Anno.Named a] -> ThSens a b

toThSens = OMap.fromList . map

( \ v -> (AS_Anno.senAttr v, v { senAttr = ThmStatus [] }))

. nameAndDisambiguate

-- | theories with a signature and sentences with proof states

data Theory sign sen proof_tree =

Theory sign (ThSens sen (ProofStatus proof_tree))

deriving Typeable

-- e.g. the file name, or the script itself, or a configuration string

data TacticScript = TacticScript String deriving (Eq, Ord, Show, Typeable)

-- | failure reason

data Reason = Reason [String] deriving Typeable

instance Ord Reason where

compare _ _ = EQ

instance Eq Reason where

a == b = compare a b == EQ

-- | enumeration type representing the status of a goal

data GoalStatus =

Open Reason -- ^ failure reason

| Disproved

| Proved Bool -- ^ True means consistent; False inconsistent

deriving (Eq, Ord, Typeable)

instance Show GoalStatus where

show gs = case gs of

Open (Reason l) -> unlines $ "Open" : l

Disproved -> "Disproved"

Proved c -> "Proved" ++ if c then "" else "(inconsistent)"

isOpenGoal :: GoalStatus -> Bool

isOpenGoal gs = case gs of

Open _ -> True

_ -> False

openGoalStatus :: GoalStatus

openGoalStatus = Open $ Reason []

-- | data type representing the proof status for a goal

data ProofStatus proof_tree = ProofStatus

{ goalName :: String

, goalStatus :: GoalStatus

, usedAxioms :: [String] -- ^ used axioms

, usedProver :: String -- ^ name of prover

, proofTree :: proof_tree

, usedTime :: TimeOfDay

, tacticScript :: TacticScript

, proofLines :: [String] }

deriving (Show, Eq, Ord, Typeable)

{- | constructs an open proof status with basic information filled in;

make sure to set proofTree to a useful value before you access it. -}

openProofStatus :: Ord pt => String -- ^ name of the goal

-> String -- ^ name of the prover

-> pt -> ProofStatus pt

openProofStatus goalname provername proof_tree = ProofStatus

{ goalName = goalname

, goalStatus = openGoalStatus

, usedAxioms = []

, usedProver = provername

, proofTree = proof_tree

, usedTime = midnight

, tacticScript = TacticScript ""

, proofLines = [] }

isProvedStat :: ProofStatus proof_tree -> Bool

isProvedStat = isProvedGStat . goalStatus

isProvedGStat :: GoalStatus -> Bool

isProvedGStat gs = case gs of

Proved _ -> True

_ -> False

-- | different kinds of prover interfaces

data ProverKind = ProveGUI | ProveCMDLautomatic deriving Typeable

-- | determine if a prover kind is implemented

hasProverKind :: ProverKind -> ProverTemplate x s m y z -> Bool

hasProverKind pk pt = case pk of

ProveGUI -> isJust $ proveGUI pt

ProveCMDLautomatic -> isJust $ proveCMDLautomaticBatch pt

data FreeDefMorphism sentence morphism = FreeDefMorphism

{ freeDefMorphism :: morphism

, pathFromFreeDef :: morphism

, freeTheory :: [AS_Anno.Named sentence]

, isCofree :: Bool }

deriving (Show, Eq, Ord, Typeable)

-- | prover or consistency checker

data ProverTemplate theory sentence morphism sublogics proof_tree = Prover

{ proverName :: String,

proverUsable :: IO (Maybe String),

-- are required binaries or jars installed, Nothing if yes

proverSublogic :: sublogics,

proveGUI :: Maybe (String -> theory -> [FreeDefMorphism sentence morphism]

-> IO ( [ProofStatus proof_tree]

, [(Named sentence, ProofStatus proof_tree)])),

{- input: imported theories, theory name, theory (incl. goals)

output:

fst --> proof status for goals and lemmas

snd --> new lemmas (with proofs) -}

proveCMDLautomaticBatch ::

Maybe (Bool -- 1.

-> Bool -- 2.

-> Concurrent.MVar (Result [ProofStatus proof_tree]) -- 3.

-> String -- 4.

-> TacticScript -- 5.

-> theory -- 6.

-> [FreeDefMorphism sentence morphism]

-> IO (Concurrent.ThreadId, Concurrent.MVar ())) {- output

input:

1. True means include proven theorems in subsequent proof attempts;

2. True means save problem file for each goal;

3. MVar reference to a Result [] or empty MVar,

used to store the result of each attempt in the batch run;

4. theory name;

5. default TacticScript;

6. theory

(incl. goals and Open SenStatus for individual tactic_scripts)

7. ingoing free def morphisms

output:

fst --> identifier of the batch thread for killing it,

after each proof attempt the result is stored in the IOref

snd --> MVar to wait for the end of the thread -}

} deriving Typeable

type Prover sign sentence morphism sublogics proof_tree =

ProverTemplate (Theory sign sentence proof_tree)

sentence morphism sublogics proof_tree

mkProverTemplate :: String -> sublogics

-> (String -> theory -> [FreeDefMorphism sentence morphism]

-> IO [ProofStatus proof_tree])

-> ProverTemplate theory sentence morphism sublogics proof_tree

mkProverTemplate str sl fct = Prover

{ proverName = str

, proverUsable = return Nothing

, proverSublogic = sl

, proveGUI = Just $ \ s t fs -> do

ps <- fct s t fs

return (ps, [])

, proveCMDLautomaticBatch = Nothing }

mkUsableProver :: String -> String -> sublogics

-> (String -> theory -> [FreeDefMorphism sentence morphism]

-> IO [ProofStatus proof_tree])

-> ProverTemplate theory sentence morphism sublogics proof_tree

mkUsableProver bin str sl fct =

(mkProverTemplate str sl fct) { proverUsable = checkBinary bin }

mkAutomaticProver :: String -> String -> sublogics

-> (String -> theory -> [FreeDefMorphism sentence morphism]

-> IO [ProofStatus proof_tree])

-> (Bool -> Bool -> Concurrent.MVar (Result [ProofStatus proof_tree])

-> String -> TacticScript -> theory -> [FreeDefMorphism sentence morphism]

-> IO (Concurrent.ThreadId, Concurrent.MVar ()))

-> ProverTemplate theory sentence morphism sublogics proof_tree

mkAutomaticProver bin str sl fct bFct =

(mkUsableProver bin str sl fct)

{ proveCMDLautomaticBatch = Just bFct }

-- | theory morphisms between two theories

data TheoryMorphism sign sen mor proof_tree = TheoryMorphism

{ tSource :: Theory sign sen proof_tree

, tTarget :: Theory sign sen proof_tree

, tMorphism :: mor }

deriving Typeable

data CCStatus proof_tree = CCStatus

{ ccProofTree :: proof_tree

, ccUsedTime :: TimeOfDay

, ccResult :: Maybe Bool }

deriving Typeable

data ConsChecker sign sentence sublogics morphism proof_tree = ConsChecker

{ ccName :: String

, ccUsable :: IO (Maybe String)

, ccSublogic :: sublogics

, ccBatch :: Bool -- True for batch checkers

, ccNeedsTimer :: Bool -- True for checkers that ignore time limits

, ccAutomatic :: String -- 1.

-> TacticScript -- 2.

-> TheoryMorphism sign sentence morphism proof_tree -- 3.

-> [FreeDefMorphism sentence morphism] -- 4.

-> IO (CCStatus proof_tree) -- output

} deriving Typeable

{- input: 1. theory name

2. default TacticScript

3. theory morphism

5. ingoing free definition morphisms

output: consistency result status -}

mkConsChecker :: String -> sublogics

-> (String -> TacticScript -> TheoryMorphism sign sentence morphism proof_tree

-> [FreeDefMorphism sentence morphism] -> IO (CCStatus proof_tree))

-> ConsChecker sign sentence sublogics morphism proof_tree

mkConsChecker n sl f = ConsChecker

{ ccName = n

, ccUsable = return Nothing

, ccSublogic = sl

, ccBatch = True

, ccNeedsTimer = True

, ccAutomatic = f }

mkUsableConsChecker :: String -> String -> sublogics

-> (String -> TacticScript -> TheoryMorphism sign sentence morphism proof_tree

-> [FreeDefMorphism sentence morphism] -> IO (CCStatus proof_tree))

-> ConsChecker sign sentence sublogics morphism proof_tree

mkUsableConsChecker bin n sl f =

(mkConsChecker n sl f) { ccUsable = checkBinary bin }