Copyright	(c) Ewaryst Schulz, DFKI Bremen 2009
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Ewaryst.Schulz@dfki.de
Stability	provisional
Portability	non-portable(Logic)
Safe Haskell	None

OMDoc.Export

Contents

Name Mapping interface
LibEnv traversal
Views and Morphisms
Names and CDs
Symbols and Sentences

Description

Export of a given development graph to an OMDoc structure which can then be stored as xml via the OMDoc.XmlInterface.

The export requires the following interface functions to be instantiated for each logic

Sentences: sym_of (needed for symlist_of), sym_name, symmap_of

Logic: omdoc_metatheory, export_symToOmdoc, export_senToOmdoc

This function has a default implementation which is sufficient in many cases: export_theoryToOmdoc

Synopsis

Name Mapping interface

data GSigMap

A structure similar to SigMap but with a Grothendieck map instead. The numbered UniqName just stores the original position of the symbol in the signature, and will be exploited in order to output the symbols in the correct dependency order.

Constructors

GSigMap (G_symbolmap (Int, UniqName)) (NameMap String)

type NumberedSigMap a = (Map a (Int, UniqName), NameMap String)

We need this type to store the original dependency order. This type is the logic dependent analogue to the GSigMap

nSigMapToSigMap :: NumberedSigMap a -> SigMap a

Removes the numbering from the symbol map

nSigMapToOrderedList :: NumberedSigMap a -> [(a, UniqName)]

Computes a dependency sorted (symbol - unique name) list

newtype SpecSymNames

Mapping of Specs to SigMaps

Constructors

SpecSymNames (Map (LibName, String) GSigMap)

data ExpEnv

The export environment

Constructors

ExpEnv
Fields getSSN :: SpecSymNames getInitialLN :: LibName getFilePathMapping :: Map LibName FilePath

fmapNM :: (Ord a, Ord b) => (a -> b) -> NameMap a -> NameMap b

emptyEnv :: LibName -> ExpEnv

fromSignAndNamedSens :: forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree. Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> sign -> [Named sentence] -> NumberedSigMap symbol

lookupWithInsert :: forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree. Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> sign -> [Named sentence] -> ExpEnv -> (LibName, String) -> (ExpEnv, NumberedSigMap symbol)

Looks up the key in the map and if it doesn't exist adds the value for this key which results from the given sign and sentences.

LibEnv traversal

exportLibEnv :: Bool -> FilePath -> LibName -> LibEnv -> Result [(LibName, OMDoc)]

Translates the given LibEnv to a list of OMDocs. If the first argument is false only the DG to the given LibName is translated and returned.

initFilePathMapping :: FilePath -> LibEnv -> Map LibName FilePath

exportDGraph :: LibEnv -> ExpEnv -> (LibName, DGraph) -> Result (ExpEnv, OMDoc)

DGraph to OMDoc translation

exportNodeLab :: LibEnv -> LibName -> DGraph -> ExpEnv -> LNode DGNodeLab -> Result (ExpEnv, Maybe TLElement)

DGNodeLab to TLTheory translation

Views and Morphisms

getNodeData :: LibEnv -> LibName -> DGNodeLab -> (DGNodeLab, LibName)

makeImport :: Set UniqName -> (String, OMCD, [(OMName, UniqName)]) -> (Set UniqName, TCElement)

makeImportMapping :: forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree. Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => LibEnv -> LibName -> DGraph -> (lid, NameMap symbol) -> ExpEnv -> LEdge DGLinkLab -> Result (ExpEnv, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol))

If the link is a global definition link we compute the Import and return also the set of (by the link) exported symbols.

exportLinkLab :: LibEnv -> LibName -> DGraph -> ExpEnv -> LEdge DGLinkLab -> Result (ExpEnv, Maybe TLElement)

Given a TheoremLink we output the view

makeMorphismEntry :: Bool -> (OMName, UniqName) -> (OMName, OMImage)

makeMorphism :: forall lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2. (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2) => (lid1, NameMap symbol1) -> (lid2, NameMap symbol2) -> GMorphism -> Result ([(OMName, UniqName)], Set symbol2)

From the given GMorphism we compute the symbol-mapping and return also the set of (by the morphism) exported symbols (= image of morphism)

mapEntry :: forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree. Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> NameMap symbol -> NameMap symbol -> (symbol, symbol) -> (OMName, UniqName)

sglElem :: String -> Set a -> a

extracts the single element from singleton sets, fails otherwise

Names and CDs

mkCD :: ExpEnv -> LibName -> LibName -> String -> Result OMCD

Symbols and Sentences

exportSymbol :: forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree. Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> SigMap symbol -> Maybe SyntaxTable -> [Set symbol] -> symbol -> UniqName -> Result [TCElement]

exportSentence :: forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree. Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> SigMap symbol -> Named sentence -> Result [TCElement]

mkNotation :: UniqName -> Maybe (Id, SyntaxTable) -> [TCElement]

We only export simple constant-notations if the OMDoc element name differs from the hets-name. If the placecount of the id (if provided) is nonzero then we export the application-notation elements for pretty printing in OMDoc.

mkApplicationNotation :: OMQualName -> Id -> Int -> Assoc -> (TCElement, String)

This function requires mixfix Ids as input and generates Notation structures, see DataTypes. If smart notations are produced we also provide a string for a constant notation.

mkSmartNotation :: OMQualName -> String -> Fixity -> Int -> Assoc -> TCElement

See OMDoc.DataTypes for a description of SmartNotation. We set the number of implicit arguments to 0.

mkFlexibleNotation :: OMQualName -> Id -> Int -> TCElement