Export.hs revision c3f7e132e0c214b755c6c4b485f4748c4dd1595c
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerModule : $Header$
6bcc9da85b73c324e14365759791daf895b0738cChristian MaederDescription : export a development graph to an omdoc structure
8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyerCopyright : (c) Ewaryst Schulz, DFKI Bremen 2009
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerMaintainer : Ewaryst.Schulz@dfki.de
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerStability : provisional
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerPortability : non-portable(Logic)
8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyerA given development graph will be exported to an omdoc structure
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerwhich can then be output to XML via the XmlInterface.
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ( exportDGraph
8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , exportNodeLab
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | DGraph to OMDoc translation
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerexportDGraph :: LibName -> DGraph -> OMDoc
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerexportDGraph ln dg = let
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer libid = (getLibId ln)
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer in OMDoc (show ln) $
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer -- the theories
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer (catMaybes $ map (exportNodeLab libid dg) $ topsortedNodes dg)
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer (catMaybes $ map (exportLinkLab libid dg) $ labEdgesDG dg)
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | DGNodeLab to TLTheory translation
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerexportNodeLab :: LibId -> DGraph -> LNode DGNodeLab -> Maybe TLElement
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerexportNodeLab libid dg (n, lb) =
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer if isDGRef lb then Nothing else
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer let specid = mkSimpleId $ getDGNodeName lb
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer in case dgn_theory lb of
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer G_theory lid (ExtSign sig _) _ sens _ ->
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Just . TLTheory (show specid) (omdoc_metatheory lid)
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer $ catMaybes (map (makeImport libid dg) $ innDG dg n)
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ++ export_signToOmdoc lid specid libid sig
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ++ map (export_senToOmdoc lid specid libid sig) (toNamedList sens)
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermakeImport :: LibId -> DGraph -> LEdge DGLinkLab -> Maybe TCElement
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermakeImport libid dg (from, _, lbl) =
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer if isGlobalDef $ dgl_type lbl then
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Just . TCImport (cdFromNode libid $ labDG dg from) . makeMorphism libid
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer $ dgl_morphism lbl
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | Given a TheoremLink we compute the view
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerexportLinkLab :: LibId -> DGraph -> LEdge DGLinkLab -> Maybe TLElement
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerexportLinkLab libid dg (from, to, lbl) = case dgl_type lbl of
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ScopedLink Global (ThmLink _) _ ->
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Just . TLView (cdFromNode libid $ labDG dg from)
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer (cdFromNode libid $ labDG dg to)
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer . makeMorphism libid $ dgl_morphism lbl
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermakeMorphism :: LibId -> GMorphism -> TCElement
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermakeMorphism _ (GMorphism cid _ _ mor _) =
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer export_morphismToOmdoc (targetLogic cid) mor
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyercdFromNode :: LibId -> DGNodeLab -> OMCD
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyercdFromNode libid lb =
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- special handling for library entries !??
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer CD (getDGNodeName lb) $
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer let omcdbase = show $ if isDGRef lb
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer then getLibId $ ref_libname $ nodeInfo lb
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer in if omcdbase == "library" || omcdbase == ""
8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer then Nothing else Just omcdbase