Hets - the Heterogeneous Tool Set

Copyright(c) Ewaryst Schulz DFKI Bremen 2010
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerEwaryst.Schulz@dfki.de
Stabilityprovisional
Portabilitynon-portable(Logic)
Safe HaskellNone

OMDoc.Import

Contents

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 Source #

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 Source #

The keys of libMap consist of the filepaths without suffix!

Constructors

ImpEnv 

Fields

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

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

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

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

IRI Functions

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

toIRI :: String -> IRI Source #

resolveIRI :: IRI -> FilePath -> IRI Source #

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

isFileIRI :: IRI -> Bool Source #

Is the scheme of the iri empty or file?

type IriCD = (Maybe IRI, String) Source #

showIriCD :: IriCD -> String Source #

getIri :: IriCD -> Maybe IRI Source #

getModule :: IriCD -> String Source #

toIriCD :: OMCD -> LibName -> IriCD Source #

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

cdInLib :: IriCD -> LibName -> Bool Source #

Main translation functions

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

Translates an OMDoc file to a LibEnv

OMDoc traversal

importLib Source #

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 Source #

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 Source #

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) Source #

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

Utils to compute DGNodes from OMDoc Theories

completeMorphisms Source #

Arguments

:: G_sign

the complete target signature

-> [LinkInfo]

the incomplete morphisms

-> Result [LinkInfo] 

completeMorphism Source #

Arguments

:: GMorphism

the target signature id morphism

-> GMorphism

the incomplete morphism

-> Result GMorphism 

computeMorphisms Source #

Arguments

:: ImpEnv 
-> LibName 
-> Map OMName String

Notations

-> (NameSymbolMap, G_sign) 
-> [ImportInfo LinkNode] 
-> ResultT IO ((NameSymbolMap, G_sign), [LinkInfo]) 

computeMorphism Source #

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 Source #

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

updateSymbolMap Source #

Arguments

:: 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 Source #

Arguments

:: 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.

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

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

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

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) Source #

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

initialSig :: AnyLogic -> (NameSymbolMap, G_sign) Source #

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

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

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

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

Adds sentences and logic dependent signature elements to the given sig

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

Adds Edges from the LinkInfo list to the development graph.

addLinkToDG :: Node -> DGraph -> LinkInfo -> DGraph Source #

Adds Edge from the LinkInfo to the development graph.

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

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

Theory-utils

type LinkNode = (Maybe LibName, LNode DGNodeLab) Source #

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

data ImportInfo a Source #

Constructors

ImportInfo a String TCMorphism 

Instances

Functor ImportInfo Source # 

Methods

fmap :: (a -> b) -> ImportInfo a -> ImportInfo b

(<$) :: a -> ImportInfo b -> ImportInfo a

Show a => Show (ImportInfo a) Source # 

Methods

showsPrec :: Int -> ImportInfo a -> ShowS

show :: ImportInfo a -> String

showList :: [ImportInfo a] -> ShowS

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

data TCClassification Source #

Constructors

TCClf 

Fields