{-|

Module : $Header$

Copyright : (c) Jorina F. Gerken, Till Mossakowski, Uni Bremen 2002-2004

Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

Maintainer : jfgerken@tzi.de

Stability : provisional

Portability : non-portable(Logic)

Proofs in development graphs.

Follows Sect. IV:4.4 of the CASL Reference Manual.

-}

{-

References:

T. Mossakowski, S. Autexier and D. Hutter:

Extending Development Graphs With Hiding.

H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,

Lecture Notes in Computer Science 2029, p. 269-283,

Springer-Verlag 2001.

todo in general:

Order of rule application: try to use local links induced by %implies

for subsumption proofs (such that the %implied formulas need not be

re-proved)

Integrate stuff from Saarbr�cken

Add proof status information

what should be in proof status:

- proofs of thm links according to rules

- cons, def and mono annos, and their proofs

-}

module Proofs.InferBasic (automatic, basicInferenceNode) where

import Logic.Logic

import Logic.Prover

import Logic.Grothendieck

import Logic.Comorphism

import Static.DevGraph

import Static.DGToSpec

import Common.Result

import Common.PrettyPrint

import Data.Graph.Inductive.Graph

import qualified Common.Lib.Map as Map

import Common.Id

import Common.AS_Annotation

import Syntax.AS_Library

import Syntax.Print_AS_Library

import Proofs.Proofs

import Proofs.EdgeUtils

import Proofs.StatusUtils

import Proofs.Global

import Proofs.Local

import Proofs.HideTheoremShift

import GUI.Utils

{- todo: implement apply for GlobDecomp and Subsumption

the list of DGChage must be constructed in parallel to the

new DGraph -}

applyRule :: DGRule -> DGraph -> Maybe ([DGChange],DGraph)

applyRule = error "Proofs.hs:applyRule"

{- automatically applies all rules to the library

denoted by the library name of the given proofstatus-}

automatic :: ProofStatus -> IO ProofStatus

automatic = automaticRecursive 0

{- applies the rules recursively until no further changes can be made -}

automaticRecursive :: Int -> ProofStatus -> IO ProofStatus

automaticRecursive cnt proofstatus = do

auxProofstatus@(ln, libEnv, historyMap) <- automaticApplyRules proofstatus

finalProofstatus <- mergeHistories cnt auxProofstatus

case finalProofstatus of

Nothing -> return proofstatus

Just p -> automaticRecursive 1 p

{- sequentially applies all rules to the given proofstatus,

ie to the library denoted by the library name of the proofstatus -}

automaticApplyRules :: ProofStatus -> IO ProofStatus

automaticApplyRules p = do

p1 <- globSubsume p

p2 <- globDecomp p1

p3 <- locSubsume p2

p4 <- locDecomp p3

hideTheoremShift True p4

{- merges for every library the new history elements

to one new history element -}

mergeHistories :: Int -> ProofStatus -> IO (Maybe ProofStatus)

mergeHistories cnt proofstatus@(ln,libEnv,_) = do

(numChanges,newProofstatus) <- mergeHistoriesAux cnt (libNames) proofstatus

if (numChanges > 0) then

return (Just (changeCurrentLibName ln newProofstatus))

else return Nothing

where

libNames = Map.keys libEnv

{- auxiliary method for mergeHistories:

determined the library names and recursively applies mergeHistory -}

mergeHistoriesAux :: Int -> [LIB_NAME] -> ProofStatus -> IO (Int,ProofStatus)

mergeHistoriesAux cnt [] proofstatus = return (0,proofstatus)

mergeHistoriesAux cnt (ln:list) proofstatus = do

ps <- mergeHistory cnt (changeCurrentLibName ln proofstatus)

case ps of

Just newProofstatus -> do

(i,finalProofstatus) <- mergeHistoriesAux cnt list newProofstatus

return (i+1,finalProofstatus)

Nothing -> mergeHistoriesAux cnt list proofstatus

{- merges the new history elements of a single library

to one new history elemebt-}

mergeHistory :: Int -> ProofStatus -> IO (Maybe ProofStatus)

mergeHistory cnt proofstatus@(ln,libEnv,historyMap) = do

let history = lookupHistory ln proofstatus

dgraph = lookupDGraph ln proofstatus

let (newHistoryPart, oldHistory) = splitAt (5+cnt) history

if (null (concat (map snd (take 5 newHistoryPart)))) && (cnt == 1) then

return Nothing

else do

let (rules, changes) = concatHistoryElems (reverse newHistoryPart)

newHistoryElem = (rules, removeContraryChanges changes)

newHistory = newHistoryElem:oldHistory

return (Just (ln,libEnv,Map.insert ln newHistory historyMap))

{- concats the given history elements to one history element-}

concatHistoryElems :: [([DGRule],[DGChange])] -> ([DGRule],[DGChange])

concatHistoryElems [] = ([],[])

concatHistoryElems ((rules,changes):elems) =

(rules++(fst (concatHistoryElems elems)),changes++(snd (concatHistoryElems elems)))

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

-- basic inference

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

getGoals :: LibEnv -> DGraph -> LEdge DGLinkLab -> Result G_l_sentence_list

getGoals libEnv dg (n,_,edge) = do

th <- maybeToMonad ("Could node find node "++show n)

$ computeLocalTheory libEnv dg n

let mor = dgl_morphism edge

fmap sensOf $ translateG_theory mor th

getProvers :: Bool -> LogicGraph -> G_sublogics -> [(G_prover,AnyComorphism)]

getProvers consCheck lg gsub =

if consCheck then

[(G_cons_checker (targetLogic cid) p,Comorphism cid) |

Comorphism cid <- cms,

p <- cons_checkers (targetLogic cid)]

else

[(G_prover (targetLogic cid) p,Comorphism cid) |

Comorphism cid <- cms,

p <- provers (targetLogic cid)]

where cms = findComorphismPaths lg gsub

selectProver :: [(G_prover,AnyComorphism)] -> IOResult (G_prover,AnyComorphism)

selectProver [p] = return p

selectProver [] = resToIORes $ fatal_error "No pover available" nullPos

selectProver provers = do

sel <- ioToIORes $ listBox

"Choose a translation to a prover-supported logic"

(map (show.snd) provers)

i <- case sel of

Just j -> return j

_ -> resToIORes $ fatal_error "Proofs.Proofs: selection" nullPos

return (provers!!i)

cons_check :: Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

=> lid -> ConsChecker sign sentence morphism proof_tree

-> String -> TheoryMorphism sign sentence morphism

-> IO([Proof_status proof_tree])

cons_check _ = prove

proveTheory :: Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

=> lid -> Prover sign sentence proof_tree

-> String -> Theory sign sentence -> IO([Proof_status proof_tree])

proveTheory _ = prove

-- applies basic inference to a given node

basicInferenceNode :: Bool -> LogicGraph -> (LIB_NAME,Node) -> ProofStatus

-> IO (Result ProofStatus)

basicInferenceNode checkCons lg (ln,node)

proofStatus@(libname,libEnv,proofHistory) = do

let dGraph = lookupDGraph libname proofStatus

ioresToIO (do

-- compute the theory of the node, and its name

G_theory lid1 sign axs <-

resToIORes $ computeTheory libEnv ln dGraph node

ctx <- resToIORes

$ maybeToMonad ("Could node find node "++show node)

$ fst $ match node dGraph

let nlab = lab' ctx

nodeName = case nlab of

DGNode _ _ _ _ _ _-> dgn_name nlab

DGRef _ _ _ _ _ -> dgn_renamed nlab

thName = showPretty (getLIB_ID ln) "_"

++ {-maybe (show node)-} showName nodeName

-- compute the list of proof goals

let inEdges = inn dGraph node

localEdges = filter isUnprovenLocalThm inEdges

goalslist <- if checkCons then return []

else resToIORes $ mapM (getGoals libEnv dGraph) localEdges

G_l_sentence_list lid3 goals <-

if null goalslist then return $ G_l_sentence_list lid1 []

else resToIORes (maybeToMonad

"Logic mismatch for proof goals"

(flatG_l_sentence_list goalslist))

goals1 <- coerce lid1 lid3 goals

-- select a suitable translation and prover

let provers = getProvers checkCons lg $ sublogicOfTh $

(G_theory lid1 sign (axs++goals1))

(prover,Comorphism cid) <- selectProver provers

-- Borrowing: translate theory

let lidS = sourceLogic cid

lidT = targetLogic cid

sign' <- coerce lidS lid1 sign

axs' <- coerce lidS lid1 axs

(sign'',sens'') <- resToIORes $ map_theory cid (sign',axs')

case prover of

G_prover lid4 p -> do

-- Borrowing: translate goal

goals' <- coerce lidS lid3 goals

goals'' <- resToIORes $ mapM (mapNamedM $ map_sentence cid sign') goals'

-- call the prover

p' <- coerce lidT lid4 p

ps <- ioToIORes $ proveTheory lidT p' thName

$ Theory sign'' $ map (\ s -> s {isAxiom = True}) sens''

++ map (\ s -> s {isAxiom = False}) goals''

-- update the development graph

let (nextDGraph, nextHistoryElem) = proveLocalEdges dGraph localEdges

newProofStatus

= mkResultProofStatus proofStatus nextDGraph nextHistoryElem

return newProofStatus

G_cons_checker lid4 p -> do

incl <- resToIORes $ inclusion lidT (empty_signature lidT) sign''

let mor = TheoryMorphism { t_source = empty_theory lidT,

t_target = Theory sign'' sens'',

t_morphism = incl }

p' <- coerce lidT lid4 p

ps <- ioToIORes $ cons_check lidT p' thName mor

let nextHistoryElem = ([LocalInference],[])

-- ??? to be implemented

newProofStatus

= mkResultProofStatus proofStatus dGraph nextHistoryElem

return newProofStatus

)

proveLocalEdges :: DGraph -> [LEdge DGLinkLab] -> (DGraph,([DGRule],[DGChange]))

proveLocalEdges dGraph edges = (nextDGraph,([LocalInference],changes))

where (nextDGraph,(_,changes)) = proveLocalEdgesAux ([],[]) dGraph edges

proveLocalEdgesAux :: ([DGRule],[DGChange]) -> DGraph -> [LEdge DGLinkLab]

-> (DGraph,([DGRule],[DGChange]))

proveLocalEdgesAux historyElem dGraph [] = (dGraph, historyElem)

proveLocalEdgesAux (rules,changes) dGraph ((edge@(src, tgt, edgelab)):edges) =

if True then proveLocalEdgesAux (rules,(DeleteEdge edge):((InsertEdge provenEdge):changes)) (insEdge provenEdge(delLEdge edge dGraph)) edges

else proveLocalEdgesAux (rules,changes) dGraph edges

where

morphism = dgl_morphism edgelab

(LocalThm _ conservativity conservStatus) = (dgl_type edgelab)

proofBasis = [] -- to be implemented

provenEdge = (src,

tgt,

DGLink {dgl_morphism = morphism,

dgl_type =

(LocalThm (Proven LocalInference proofBasis)

conservativity conservStatus),

dgl_origin = DGProof}

)