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

OMDoc.Import

Contents

Import Environment Interface
IRI Functions
Main translation functions
OMDoc traversal
- Utils to compute DGNodes from OMDoc Theories
Development Graph and LibEnv interface
Theory-utils

Description

Given an OMDoc file, a Library Environment is constructed from it by following all library links.

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

Signature Category: ide, cod

Sentences: symmap_of

StaticAnalysis: id_to_raw, symbol_to_raw, induced_from_morphism, induced_from_to_morphism , signature_union, empty_signature, add_symb_to_sign

Logic: omdoc_metatheory, omdocToSym, omdocToSen

These functions have default implementations which are sufficient in many cases: addOMadtToTheory, addOmdocToTheory

Synopsis

Import Environment Interface

type NameSymbolMap = G_mapofsymbol OMName

There are three important maps for each theory: 1. OMName -> symbol, the NameSymbolMap stores for each OMDoc name the translated hets symbol 2. OMName -> String, the NameMap stores the notation information of the OMDoc names, identity mappings are NOT stored here! 3. SigMapI symbol, this signature map is just a container to store map 1 and 2

data ImpEnv

The keys of libMap consist of the filepaths without suffix!

Constructors

ImpEnv
Fields libMap :: Map FilePath (LibName, DGraph) nsymbMap :: Map (LibName, String) NameSymbolMap hetsOptions :: HetcatsOpts

initialEnv :: HetcatsOpts -> ImpEnv

getLibEnv :: ImpEnv -> LibEnv

addDGToEnv :: ImpEnv -> LibName -> DGraph -> ImpEnv

addNSMapToEnv :: ImpEnv -> LibName -> String -> NameSymbolMap -> ImpEnv

lookupLib :: ImpEnv -> IRI -> Maybe (LibName, DGraph)

lookupNode :: ImpEnv -> CurrentLib -> IriCD -> Maybe (LibName, LNode DGNodeLab)

lookupNSMap :: ImpEnv -> LibName -> Maybe LibName -> String -> NameSymbolMap

rPutIfVerbose :: ImpEnv -> Int -> String -> ResultT IO ()

rPut :: ImpEnv -> String -> ResultT IO ()

rPut2 :: ImpEnv -> String -> ResultT IO ()

IRI Functions

readFromURL :: (FilePath -> IO a) -> IRI -> IO a

toIRI :: String -> IRI

libNameFromURL :: String -> IRI -> LibName

resolveIRI :: IRI -> FilePath -> IRI

Compute an absolute IRI for a supplied IRI relative to the given filepath.

isFileIRI :: IRI -> Bool

Is the scheme of the iri empty or file?

type IriCD = (Maybe IRI, String)

showIriCD :: IriCD -> String

getIri :: IriCD -> Maybe IRI

getModule :: IriCD -> String

toIriCD :: OMCD -> LibName -> IriCD

Compute an absolute IRI for a supplied CD relative to the given LibName

getLogicFromMeta :: Maybe OMCD -> AnyLogic

cdInLib :: IriCD -> LibName -> Bool

Main translation functions

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

Translates an OMDoc file to a LibEnv

OMDoc traversal

importLib

Arguments

:: ImpEnv	The import environment
-> IRI	The url of the OMDoc file
-> ResultT IO (ImpEnv, LibName, DGraph)

If the lib is not already in the environment, the OMDoc file and the closure of its imports is added to the environment.

readLib

Arguments

:: ImpEnv	The import environment
-> IRI	The url of the OMDoc file
-> ResultT IO (ImpEnv, LibName, DGraph)

The OMDoc file and the closure of its imports is added to the environment.

importTheory

Arguments

:: ImpEnv	The import environment
-> CurrentLib	The current lib
-> OMCD	The cd which points to the Theory
-> ResultT IO (ImpEnv, LibName, DGraph, LNode DGNodeLab)

Adds the Theory in the OMCD and the containing lib to the environment

addTLToDGraph :: LibName -> (ImpEnv, DGraph) -> TLElement -> ResultT IO (ImpEnv, DGraph)

Adds a view or theory to the DG, the ImpEnv may also be modified.

Utils to compute DGNodes from OMDoc Theories

completeMorphisms

Arguments

:: G_sign	the complete target signature
-> [LinkInfo]	the incomplete morphisms
-> Result [LinkInfo]

completeMorphism

Arguments

:: GMorphism	the target signature id morphism
-> GMorphism	the incomplete morphism
-> Result GMorphism

computeMorphisms

Arguments

:: ImpEnv
-> LibName
-> Map OMName String	Notations
-> (NameSymbolMap, G_sign)
-> [ImportInfo LinkNode]
-> ResultT IO ((NameSymbolMap, G_sign), [LinkInfo])

computeMorphism

Arguments

:: ImpEnv	The import environment for lookup purposes
-> LibName	Current libname
-> Map OMName String	Notations of target signature
-> (NameSymbolMap, G_sign)	OMDoc symbol to Hets symbol map and target signature
-> ImportInfo LinkNode	source label with OMDoc morphism
-> ResultT IO ((NameSymbolMap, G_sign), LinkInfo)

Computes the morphism for an import link and updates the signature and the name symbol map with the imported symbols

computeViewMorphism

Arguments

:: ImpEnv	The import environment for lookup purposes
-> LibName	Current libname
-> ImportInfo (LinkNode, LinkNode)	OMDoc morphism with source and target node
-> ResultT IO LinkInfo

Computes the morphism for a view

mkLinkOrigin :: String -> DGLinkOrigin

updateSymbolMap

Arguments

:: 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
-> morphism	a signature morphism m
-> NameSymbolMap
-> [(symbol, OMName)]	a list l of symbol to OMName mappings
-> NameSymbolMap

For each entry (s, n) in l we enter the mapping (n, m(s)) to the name symbol map

computeSymbolMap

Arguments

:: 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
=> Maybe (Map OMName String)	Notations for missing symbols in map
-> NameSymbolMap
-> NameSymbolMap
-> TCMorphism
-> lid
-> ResultT IO [(symbol, Either (OMName, raw_symbol) symbol)]

Computes a symbol map for the given TCMorphism. The symbols are looked up in the provided maps. For each symbol not found in the target map we return a OMName, raw symbol pair in order to insert the missing entries in the target name symbol map later. If notations are not present, all lookup failures end up in errors.

followImports :: LibName -> (ImpEnv, DGraph) -> [ImportInfo OMCD] -> ResultT IO ((ImpEnv, DGraph), [ImportInfo LinkNode])

followImport :: LibName -> (ImpEnv, DGraph) -> ImportInfo OMCD -> ResultT IO ((ImpEnv, DGraph), ImportInfo LinkNode)

Ensures that the theory for the given OMCD is available in the environment. See also followTheory

followTheories :: LibName -> (ImpEnv, DGraph) -> [OMCD] -> ResultT IO ((ImpEnv, DGraph), [LinkNode])

followTheory :: LibName -> (ImpEnv, DGraph) -> OMCD -> ResultT IO ((ImpEnv, DGraph), LinkNode)

We lookup the theory referenced by the cd in the environment and add it if neccessary to the environment.

Development Graph and LibEnv interface

sigmapAccumFun :: (Monad m, Show a) => (SigMapI a -> TCElement -> String -> m a) -> SigMapI a -> TCElement -> m (SigMapI a, a)

returns a function compatible with mapAccumLM for TCElement processing. Used in localSig.

initialSig :: AnyLogic -> (NameSymbolMap, G_sign)

Builds an initial signature and a name map of the given logic.

localSig :: TCClassification -> NameSymbolMap -> G_sign -> Result (NameSymbolMap, G_sign)

Adds the local signature to the given signature and name symbol map

addSentences :: TCClassification -> NameSymbolMap -> G_sign -> Result G_theory

Adds sentences and logic dependent signature elements to the given sig

addLinksToDG :: Node -> DGraph -> [LinkInfo] -> DGraph

Adds Edges from the LinkInfo list to the development graph.

addLinkToDG :: Node -> DGraph -> LinkInfo -> DGraph

Adds Edge from the LinkInfo to the development graph.

addNodeToDG :: DGraph -> String -> G_theory -> (LNode DGNodeLab, DGraph)

Adds a Node from the given G_theory to the development graph.

addNodeAsRefToDG :: LNode DGNodeLab -> LibName -> DGraph -> (LNode DGNodeLab, DGraph)

Theory-utils

type CurrentLib = (LibName, DGraph)

type LinkNode = (Maybe LibName, LNode DGNodeLab)

type LinkInfo = (GMorphism, DGLinkType, DGLinkOrigin, Node, Maybe Node)

data ImportInfo a

Constructors

ImportInfo a String TCMorphism

Instances

Functor ImportInfo
Show a => Show (ImportInfo a)

iInfoVal :: ImportInfo a -> a

fmapLI :: Monad m => (GMorphism -> m GMorphism) -> LinkInfo -> m LinkInfo

data TCClassification

Constructors

TCClf
Fields importInfo :: [ImportInfo OMCD] Import-info sigElems :: [TCElement] Signature symbols sentences :: [TCElement] Theory sentences adts :: [[OmdADT]] ADTs notations :: Map OMName String Notations

emptyClassification :: TCClassification

classifyTCs :: [TCElement] -> TCClassification

classifyTC :: TCElement -> TCClassification -> TCClassification