{- |

Module : ./Static/FromXml.hs

Description : xml input for Hets development graphs

Copyright : (c) Simon Ulbricht, DFKI GmbH 2011

License : GPLv2 or higher, see LICENSE.txt

Maintainer : tekknix@informatik.uni-bremen.de

Stability : provisional

Portability : non-portable (DevGraph)

create new or extend a Development Graph in accordance with an XML input

-}

module Static.FromXml where

import Static.ComputeTheory (computeLibEnvTheories)

import Static.DevGraph

import Static.DgUtils

import Static.GTheory

import Static.FromXmlUtils

import Static.XGraph

import Common.LibName

import Common.Result (Result (..))

import Common.ResultT

import Common.XmlParser

import Comorphisms.LogicGraph (logicGraph)

import Control.Monad.Trans (lift)

import Control.Monad (foldM, unless)

import qualified Data.Graph.Inductive.Graph as Graph (Node)

import qualified Data.Map as Map

import Data.Set (Set)

import qualified Data.Set as Set

import Driver.Options

import Driver.ReadFn (findFileOfLibNameAux)

import Logic.ExtSign (ext_empty_signature)

import Logic.Grothendieck

import Logic.Logic (AnyLogic (..), cod, composeMorphisms)

import Logic.Prover (noSens)

import Text.XML.Light (Element)

-- | top-level function

readDGXml :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))

readDGXml opts path = do

Result ds res <- runResultT $ readDGXmlR opts path Map.empty

showDiags opts ds

return res

{- | main function; receives a FilePath and calls fromXml upon that path,

using an initial LogicGraph. -}

readDGXmlR :: HetcatsOpts -> FilePath -> LibEnv -> ResultT IO (LibName, LibEnv)

readDGXmlR opts path lv = do

lift $ putIfVerbose opts 2 $ "Reading " ++ path

xml' <- lift $ readXmlFile path

res <- lift $ parseXml xml'

case res of

Right xml -> rebuiltDgXml opts lv xml

Left err -> fail $ "failed to parse XML file: " ++ path ++ "\n" ++ err

-- | call rebuiltDG with only a LibEnv and an Xml-Element

rebuiltDgXml :: HetcatsOpts -> LibEnv -> Element -> ResultT IO (LibName, LibEnv)

rebuiltDgXml opts lv xml = do

xg <- liftR $ xGraph xml

res <- rebuiltDG opts logicGraph xg lv

let ln = libName xg

return (ln, computeLibEnvTheories $ uncurry (Map.insert ln) res)

{- | reconstructs the Development Graph via a previously created XGraph-

structure. -}

rebuiltDG :: HetcatsOpts -> LogicGraph -> XGraph -> LibEnv

-> ResultT IO (DGraph, LibEnv)

rebuiltDG opts lg (XGraph _ ga i thmLk nds body) lv = do

(dg, lv') <- rebuiltBody body lv

dg' <- insertThmLinks lg dg $ mkEdgeMap thmLk

return (dg', lv') where

rebuiltBody bd lv' = case bd of

[] ->

foldM (flip $ insertFirstNode opts lg)

(emptyDG { globalAnnos = ga, getNewEdgeId = i }, lv') nds

bs : bd' -> do

res0 <- rebuiltBody bd' lv'

foldM (\ dl (lKs, nd) ->

insertStep opts lg nd lKs dl)

res0 bs

-- | inserts a new node as well as all definition links pointing at that node

insertStep :: HetcatsOpts -> LogicGraph -> XNode -> [XLink] -> (DGraph, LibEnv)

-> ResultT IO (DGraph, LibEnv)

insertStep opts lg xNd lks (dg, lv) = do

mrs <- mapM (getTypeAndMorphism lg dg) lks

G_sign lid sg sId <- getSigForXNode lg dg mrs

let j = getNewNodeDG dg

(gt2, dg', lv') <-

insertNode opts lg (Just $ noSensGTheory lid sg sId) xNd j (dg, lv)

dg'' <- foldM (insertLink lg j (signOf gt2)) dg' mrs

return (dg'', lv')

insertLink :: LogicGraph -> Graph.Node -> G_sign -> DGraph

-> (Graph.Node, GMorphism, DGLinkType, XLink) -> ResultT IO DGraph

insertLink lg j gs dg (i, mr, tp, lk) = do

lkLab <- finalizeLink lg lk mr gs tp

return $ insEdgeAsIs (i, j, lkLab) dg

-- | inserts theorem links

insertThmLinks :: LogicGraph -> DGraph -> EdgeMap -> ResultT IO DGraph

insertThmLinks lg p = foldM (\ dg (tgt, sm) -> do

(j, gsig) <- signOfNode tgt dg

insertTarThmLinks lg j gsig dg sm) p . Map.toList

insertTarThmLinks :: LogicGraph -> Graph.Node -> G_sign

-> DGraph -> Map.Map String [XLink] -> ResultT IO DGraph

insertTarThmLinks lg j tgt p = foldM (\ dg (src, ls) -> do

(i, gsig) <- signOfNode src dg

foldM (\ dg' xLk -> do

(mr, tp) <- getTypeAndMorphism1 lg dg gsig xLk

insertLink lg j tgt dg' (i, mr, tp, xLk)) dg ls) p . Map.toList

{- | given a links intermediate morphism and its target nodes signature,

this function calculates the final morphism for this link -}

finalizeLink :: LogicGraph -> XLink -> GMorphism -> G_sign -> DGLinkType

-> ResultT IO DGLinkLab

finalizeLink lg xLk mr sg tp = do

mr' <- liftR $ case edgeTypeModInc $ lType xLk of

HidingDef -> ginclusion lg sg (cod mr)

_ -> do

mr1 <- ginclusion lg (cod mr) sg

composeMorphisms mr mr1

return $ defDGLinkId mr' tp SeeTarget $ edgeId xLk

{- | based upon the morphisms of ingoing deflinks, calculate the initial

signature to be used for node insertion -}

getSigForXNode :: LogicGraph -> DGraph

-> [(Graph.Node, GMorphism, DGLinkType, XLink)]

-> ResultT IO G_sign

getSigForXNode lg dg mrs = case mrs of

[] -> fail "insertStep: empty link list"

(_, _, FreeOrCofreeDefLink _ _, xLk) : rt -> do

unless (null rt)

$ fail "unexpected non-singleton free or cofree def link"

fmap snd $ signOfNode (source xLk) dg

_ -> liftR $ gsigManyUnion lg $ map (\ (_, m, _, _) -> cod m) mrs

-- | gathers information for an XLink using its source nodes signature

getTypeAndMorphism :: LogicGraph -> DGraph -> XLink

-> ResultT IO (Graph.Node, GMorphism, DGLinkType, XLink)

getTypeAndMorphism lg dg xLk = do

(i, sg1) <- signOfNode (source xLk) dg

(mr', lTp) <- getTypeAndMorphism1 lg dg sg1 xLk

return (i, mr', lTp, xLk)

getTypeAndMorphism1 :: LogicGraph -> DGraph -> G_sign -> XLink

-> ResultT IO (GMorphism, DGLinkType)

getTypeAndMorphism1 lg dg sg1 xLk = do

(sg2, lTp) <- getTypeAndMorAux lg dg sg1 xLk

mr' <- liftR $ getGMorphism lg sg2 (mr_name xLk) (mapping xLk)

return (mr', lTp)

{- depending on the type of the link, the correct DGLinkType and the signature

for the (external) morphism are extracted here -}

getTypeAndMorAux :: LogicGraph -> DGraph -> G_sign -> XLink

-> ResultT IO (G_sign, DGLinkType)

getTypeAndMorAux lg dg sg@(G_sign slid _ _) xLk = let

emptySig = G_sign slid (ext_empty_signature slid) startSigId

mkRtVAL sg' tp = return (sg', tp)

cc = cons xLk

in case edgeTypeModInc $ lType xLk of

HidingDef -> mkRtVAL sg HidingDefLink

GlobalDef -> mkRtVAL sg $ localOrGlobalDef Global cc

HetDef -> mkRtVAL sg $ localOrGlobalDef Global cc

LocalDef -> mkRtVAL sg $ localOrGlobalDef Local cc

FreeOrCofreeDef fc -> do

(sg', mNd) <- case mr_source xLk of

Nothing -> return (emptySig, EmptyNode $ Logic slid)

Just ms -> do

(j, sg') <- signOfNode ms dg

return (sg', JustNode $ NodeSig j sg')

mkRtVAL sg' $ FreeOrCofreeDefLink fc mNd

ThmType thTp prv _ _ -> let

lStat = if not prv then LeftOpen

else Proven (rule xLk) $ prBasis xLk in

case thTp of

HidingThm -> do

(i', sg') <- case mr_source xLk of

Just ms -> signOfNode ms dg

Nothing -> fail "no morphism source declaration for HidingThmLink"

mr' <- liftR $ ginclusion lg sg' sg

mkRtVAL sg' $ HidingFreeOrCofreeThm Nothing i' mr' lStat

FreeOrCofreeThm fc -> do

(i', sg') <- case mr_source xLk of

Just ms -> signOfNode ms dg

Nothing -> return (-1, emptySig)

mr' <- liftR $ ginclusion lg sg' sg

mkRtVAL sg' $ HidingFreeOrCofreeThm (Just fc) i' mr' lStat

GlobalOrLocalThm sc _ -> mkRtVAL sg

$ ScopedLink sc (ThmLink lStat) $ mkConsStatus cc

{- | Generates and inserts a new DGNodeLab with a startoff-G_theory, an Element

and the the DGraphs Global Annotations. The caller has to ensure that the

chosen nodeId is not used in dgraph. -}

insertNode :: HetcatsOpts -> LogicGraph -> Maybe G_theory -> XNode -> Graph.Node

-> (DGraph, LibEnv) -> ResultT IO (G_theory, DGraph, LibEnv)

insertNode opts lg mGt xNd n (dg, lv) = do

(lbl, lv') <- generateNodeLab opts lg mGt xNd (dg, lv)

return (dgn_theory lbl, insNodeDG (n, lbl) dg, lv')

{- | generate nodelab with startoff-gtheory and xnode information (a new libenv

is returned in case it was extended due to reference node insertion) -}

generateNodeLab :: HetcatsOpts -> LogicGraph -> Maybe G_theory -> XNode

-> (DGraph, LibEnv) -> ResultT IO (DGNodeLab, LibEnv)

generateNodeLab opts lg mGt xNd (dg, lv) = case xNd of

-- Case #1: Reference Node

XRef nm rfNd rfLb spc -> do

(dg', lv') <- case Map.lookup (emptyLibName rfLb) lv of

Just dg' -> return (dg', lv)

Nothing -> loadRefLib opts rfLb lv

(i, gt) <- case lookupUniqueNodeByName rfNd dg' of

Just (i, lbl) -> case signOf $ dgn_theory lbl of

G_sign lid sign sId -> return (i, noSensGTheory lid sign sId)

Nothing -> fail $ "reference node " ++ rfNd ++ " was not found"

(gt', _) <- parseSpecs gt nm dg spc

let nInf = newRefInfo (emptyLibName rfLb) i

return (newInfoNodeLab nm nInf gt', lv')

-- Case #2: Regular Node

XNode nm lN (hid, syb) spc cc -> do

-- StartOff-Theory. Taken from LogicGraph for initial Nodes

gt0 <- case mGt of

Nothing -> fmap emptyTheory $ lookupLogic "generateNodeLab " lN lg

Just gt -> return gt

-- hidden symbols use a different parser

gt1 <- if hid then parseHidden gt0 syb

else fmap fst $ parseSpecs gt0 nm dg syb

(gt2, syb') <- parseSpecs gt1 nm dg spc

-- the DGOrigin is also different for nodes with hidden symbols

lOrig <- if hid then let

syms = Set.difference (symsOfGsign $ signOf gt0)

$ symsOfGsign $ signOf gt2

in return $ DGRestriction NoRestriction syms

else do

diffSig <- liftR $ homGsigDiff (signOf gt2) $ signOf gt0

return $ DGBasicSpec Nothing diffSig syb'

return (newInfoNodeLab nm (newConsNodeInfo lOrig cc) gt2, lv)

insertFirstNode :: HetcatsOpts -> LogicGraph -> XNode -> (DGraph, LibEnv)

-> ResultT IO (DGraph, LibEnv)

insertFirstNode opts lg xNd p@(dg', _) = let n = getNewNodeDG dg' in do

(_, dg, lv) <- insertNode opts lg Nothing xNd n p

return (dg, lv)

parseHidden :: G_theory -> String -> ResultT IO G_theory

parseHidden gt s' = do

gs <- liftR $ deleteHiddenSymbols s' $ signOf gt

return $ case gs of

G_sign lid sg sId -> noSensGTheory lid sg sId

parseSpecs :: G_theory -> NodeName -> DGraph -> String

-> ResultT IO (G_theory, Set G_symbol)

parseSpecs gt' nm dg spec = let

(response, msg) = extendByBasicSpec (globalAnnos dg) spec gt'

in case response of

Success gt'' _ smbs _ -> return (gt'', smbs)

Failure _ -> fail $ "[ " ++ showName nm ++ " ]\n" ++ msg

loadRefLib :: HetcatsOpts -> String -> LibEnv -> ResultT IO (DGraph, LibEnv)

loadRefLib opts ln lv = do

mPath <- lift $ findFileOfLibNameAux opts { intype = DgXml } ln

case mPath of

Just path -> do

(ln', lv') <- readDGXmlR opts path lv

return (lookupDGraph ln' lv', lv')

_ -> fail $ "no file exists for reference library " ++ ln

-- | creates an entirely empty theory

emptyTheory :: AnyLogic -> G_theory

emptyTheory (Logic lid) =

G_theory lid Nothing (ext_empty_signature lid) startSigId noSens startThId

{- | A Node is looked up via its name in the DGraph. Returns the nodes

signature, but only if one single node is found for the respective name.

Otherwise an error is thrown. -}

signOfNode :: String -> DGraph -> ResultT IO (Graph.Node, G_sign)

signOfNode nd dg = case lookupUniqueNodeByName nd dg of

Nothing -> fail $ "required node [" ++ nd ++ "] was not found in DGraph!"

Just (j, lbl) ->

return (j, signOf (dgn_theory lbl))