{-# LANGUAGE CPP #-}

{- |

Module : ./Proofs/VSE.hs

Description : Interface to send structured theories to the VSE prover

Copyright : (c) C. Maeder, DFKI 2009

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : needs POSIX

call an adaption of VSE II to hets

the prover should be attached to a node's menu (if applicable) but take the

whole library environment as in- and output like development graph rules.

-}

module Proofs.VSE where

import Static.GTheory

import Static.DevGraph

import Static.DgUtils

import Static.PrintDevGraph

import Static.DGTranslation

import Static.History

import Static.ComputeTheory

import Proofs.QualifyNames

import Common.AS_Annotation

import Common.ExtSign

import Common.Id

import Common.LibName

import Common.Result

import Common.ResultT

import Common.SExpr

import qualified Common.OrderedMap as OMap

import Logic.Logic

import Logic.Prover

import Logic.Comorphism

import Logic.Coerce

import Logic.Grothendieck

import VSE.Logic_VSE

import VSE.Prove

import VSE.ToSExpr

import Comorphisms.CASL2VSE

import CASL.ToSExpr

import CASL.Logic_CASL

import Data.Char

import Data.List

import Data.Maybe

import qualified Data.Map as Map

import qualified Data.Set as Set

import Data.Graph.Inductive.Basic (elfilter, gfold)

import Data.Graph.Inductive.Graph hiding (out)

import Control.Monad.Trans

thName :: LibName -> LNode DGNodeLab -> String

thName ln (n, lbl) = map (\ c -> if elem c "/,[]: " then '-' else c)

$ libToFileName ln ++ "_" ++ getDGNodeName lbl ++ "_" ++ show n

getSubGraph :: Node -> DGraph -> DGraph

getSubGraph n dg =

let g = dgBody dg

ns = nodes g

sns = gfold pre' (\ c s -> Set.insert (node' c) s)

(\ m s -> Set.union s $ fromMaybe Set.empty m, Set.empty) [n] g

in delNodesDG (Set.toList $ Set.difference (Set.fromList ns) sns) dg

-- | applies basic inference to a given node and whole import tree above

prove :: (LibName, Node) -> LibEnv -> IO (Result LibEnv)

prove (ln, node) libEnv =

runResultT $ do

qLibEnv <- liftR $ qualifyLibEnv libEnv

let dg1 = lookupDGraph ln qLibEnv

dg2 = dg1 { dgBody = elfilter (isGlobalEdge . dgl_type) $ dgBody dg1 }

dg3 = getSubGraph node dg2

oLbl = labDG dg3 node

ostr = thName ln (node, oLbl)

G_theory olid _ _ _ _ _ <- return $ dgn_theory oLbl

let mcm = if Logic CASL == Logic olid then Just (Comorphism CASL2VSE) else

Nothing

dGraph <- liftR $ maybe return (flip $ dg_translation qLibEnv ln) mcm dg3

let nls = topsortedNodes dGraph

ns = map snd nls

ts <- liftR $ mapM

(\ lbl -> do

let lbln = getDGNodeName lbl

G_theory lid _ (ExtSign sign0 _) _ sens0 _ <- return $ dgn_theory lbl

(sign1, sens1) <-

addErrorDiag "failure when proving VSE nodes of" ln

$ coerceBasicTheory lid VSE

("cannot cast untranslated node '" ++ lbln ++ "'")

(sign0, toNamedList sens0)

let (sign2, sens2) = addUniformRestr sign1 sens1

return

( show $ prettySExpr

$ qualVseSignToSExpr (mkSimpleId lbln) ln sign2

, show $ prettySExpr

$ SList $ map (namedSenToSExpr sign2) sens2)) ns

lift $ do

#ifdef TAR_PACKAGE

moveVSEFiles ostr

#endif

(inp, out, cp) <- prepareAndCallVSE

sendMyMsg inp $ "(" ++ unlines (map (thName ln) nls) ++ ")"

mapM_ (\ nl -> do

readMyMsg cp out linksP

str <- getLinksTo ln dGraph nl

sendMyMsg inp str) nls

mapM_ (\ (fsig, _) -> do

readMyMsg cp out sigP

sendMyMsg inp fsig) ts

mapM_ (\ (_, sens) -> do

readMyMsg cp out lemsP

sendMyMsg inp sens) ts

ms <- readFinalVSEOutput cp out

#ifdef TAR_PACKAGE

createVSETarFile ostr

#endif

case ms of

Nothing -> return libEnv

Just lemMap -> return $ foldr (\ (n, lbl) le ->

let str = map toUpper $ thName ln (n, lbl)

lems = Set.fromList $ Map.findWithDefault [] str lemMap

in if Set.null lems then le else let

dg = lookupDGraph ln le

in case lab (dgBody dg) n of

Nothing -> le -- node missing in original graph

Just olbl -> case dgn_theory olbl of

G_theory lid syn sig sigId sens _ -> let

axs = Map.keys $ OMap.filter isAxiom sens

nsens = OMap.mapWithKey (\ name sen ->

if not (isAxiom sen) && Set.member

(map toUpper $ transString name) lems

then sen {

senAttr = ThmStatus $

(Comorphism CASL2VSE,

BasicProof VSE $

mkVseProofStatus name axs)

: thmStatus sen }

else sen) sens

nlbl = olbl { dgn_theory

= G_theory lid syn sig sigId nsens startThId }

flbl = nlbl { globalTheory

= computeLabelTheory le ln dg (n, nlbl) }

ndg = changeDGH dg $ SetNodeLab olbl (n, flbl)

in Map.insert ln ndg le) libEnv nls

getLinksTo :: LibName -> DGraph -> LNode DGNodeLab -> IO String

getLinksTo ln dg (n, lbl) = do

let (ls, rs) = partition (\ (s, _, el) -> s /= n

&& isGlobalDef (dgl_type el)

&& isInc (getRealDGLinkType el)) $ innDG dg n

mapM_ (\ e -> putStrLn

$ "ignored unsupported link (non-inclusion or theorem link):\n "

++ show (prettyLEdge e)) rs

return $ show $ prettySExpr $ SList

$ map (\ (s, _, el) -> let

ltype = dgl_type el

defl = isGlobalDef ltype

in SList $

[ SSymbol $ (if defl then "definition" else "theorem") ++ "-link"

, SSymbol $ "edge" ++ showEdgeId (dgl_id el)

, SSymbol $ thName ln (s, labDG dg s)

, SSymbol $ thName ln (n, lbl)

, SSymbol "global"

, SList $ SSymbol "morphism" : hetMorToSSexpr (dgl_morphism el)]

++ if defl then [] else

[SSymbol $ if isProven ltype then "proven" else "open"]) ls

hetMorToSSexpr :: GMorphism -> [SExpr]

hetMorToSSexpr (GMorphism cid _ _ mor _) =

let tlid = targetLogic cid

in case coerceMorphism tlid VSE "" mor of

Just vsemor -> morToSExprs vsemor

Nothing -> case coerceMorphism tlid CASL "" mor of

Just cmor -> morToSExprs cmor

Nothing -> []