| 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
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
- data GSigMap = GSigMap (G_symbolmap (Int, UniqName)) (NameMap String)
- type NumberedSigMap a = (Map a (Int, UniqName), NameMap String)
- nSigMapToSigMap :: NumberedSigMap a -> SigMap a
- nSigMapToOrderedList :: NumberedSigMap a -> [(a, UniqName)]
- newtype SpecSymNames = SpecSymNames (Map (LibName, String) GSigMap)
- data ExpEnv = ExpEnv {
- 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)
- exportLibEnv :: Bool -> FilePath -> LibName -> LibEnv -> Result [(LibName, OMDoc)]
- initFilePathMapping :: FilePath -> LibEnv -> Map LibName FilePath
- exportDGraph :: LibEnv -> ExpEnv -> (LibName, DGraph) -> Result (ExpEnv, OMDoc)
- exportNodeLab :: LibEnv -> LibName -> DGraph -> ExpEnv -> LNode DGNodeLab -> Result (ExpEnv, Maybe TLElement)
- 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))
- exportLinkLab :: LibEnv -> LibName -> DGraph -> ExpEnv -> LEdge DGLinkLab -> Result (ExpEnv, Maybe TLElement)
- 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)
- 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
- mkCD :: ExpEnv -> LibName -> LibName -> String -> Result OMCD
- 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]
- mkApplicationNotation :: OMQualName -> Id -> Int -> Assoc -> (TCElement, String)
- mkSmartNotation :: OMQualName -> String -> Fixity -> Int -> Assoc -> TCElement
- mkFlexibleNotation :: OMQualName -> Id -> Int -> TCElement
Name Mapping interface
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) Source #
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 Source #
Removes the numbering from the symbol map
nSigMapToOrderedList :: NumberedSigMap a -> [(a, UniqName)] Source #
Computes a dependency sorted (symbol - unique name) list
newtype SpecSymNames Source #
Mapping of Specs to SigMaps
Constructors
| SpecSymNames (Map (LibName, String) GSigMap) |
The export environment
Constructors
| ExpEnv | |
Fields
| |
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 Source #
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) Source #
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)] Source #
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 Source #
exportDGraph :: LibEnv -> ExpEnv -> (LibName, DGraph) -> Result (ExpEnv, OMDoc) Source #
DGraph to OMDoc translation
exportNodeLab :: LibEnv -> LibName -> DGraph -> ExpEnv -> LNode DGNodeLab -> Result (ExpEnv, Maybe TLElement) Source #
DGNodeLab to TLTheory translation
Views and Morphisms
makeImport :: Set UniqName -> (String, OMCD, [(OMName, UniqName)]) -> (Set UniqName, TCElement) Source #
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)) Source #
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) Source #
Given a TheoremLink we output the view
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) Source #
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) Source #
sglElem :: String -> Set a -> a Source #
extracts the single element from singleton sets, fails otherwise
Names and CDs
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] Source #
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] Source #
mkNotation :: UniqName -> Maybe (Id, SyntaxTable) -> [TCElement] Source #
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) Source #
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 Source #
See OMDoc.DataTypes for a description of SmartNotation. We set the number of implicit arguments to 0.
mkFlexibleNotation :: OMQualName -> Id -> Int -> TCElement Source #