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

type NameSymbolMap = G_mapofsymbol OMName
data ImpEnv = ImpEnv {
- 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 ()
readFromURL :: (FilePath -> IO a) -> IRI -> IO a
toIRI :: String -> IRI
libNameFromURL :: String -> IRI -> LibName
resolveIRI :: IRI -> FilePath -> IRI
isFileIRI :: IRI -> Bool
type IriCD = (Maybe IRI, String)
showIriCD :: IriCD -> String
getIri :: IriCD -> Maybe IRI
getModule :: IriCD -> String
toIriCD :: OMCD -> LibName -> IriCD
getLogicFromMeta :: Maybe OMCD -> AnyLogic
cdInLib :: IriCD -> LibName -> Bool
anaOMDocFile :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
importLib :: ImpEnv -> IRI -> ResultT IO (ImpEnv, LibName, DGraph)
readLib :: ImpEnv -> IRI -> ResultT IO (ImpEnv, LibName, DGraph)
importTheory :: ImpEnv -> CurrentLib -> OMCD -> ResultT IO (ImpEnv, LibName, DGraph, LNode DGNodeLab)
addTLToDGraph :: LibName -> (ImpEnv, DGraph) -> TLElement -> ResultT IO (ImpEnv, DGraph)
completeMorphisms :: G_sign -> [LinkInfo] -> Result [LinkInfo]
completeMorphism :: GMorphism -> GMorphism -> Result GMorphism
computeMorphisms :: ImpEnv -> LibName -> Map OMName String -> (NameSymbolMap, G_sign) -> [ImportInfo LinkNode] -> ResultT IO ((NameSymbolMap, G_sign), [LinkInfo])
computeMorphism :: ImpEnv -> LibName -> Map OMName String -> (NameSymbolMap, G_sign) -> ImportInfo LinkNode -> ResultT IO ((NameSymbolMap, G_sign), LinkInfo)
computeViewMorphism :: ImpEnv -> LibName -> ImportInfo (LinkNode, LinkNode) -> ResultT IO LinkInfo
mkLinkOrigin :: String -> DGLinkOrigin
updateSymbolMap :: 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 -> NameSymbolMap -> [(symbol, OMName)] -> NameSymbolMap
computeSymbolMap :: 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) -> NameSymbolMap -> NameSymbolMap -> TCMorphism -> lid -> ResultT IO [(symbol, Either (OMName, raw_symbol) symbol)]
followImports :: LibName -> (ImpEnv, DGraph) -> [ImportInfo OMCD] -> ResultT IO ((ImpEnv, DGraph), [ImportInfo LinkNode])
followImport :: LibName -> (ImpEnv, DGraph) -> ImportInfo OMCD -> ResultT IO ((ImpEnv, DGraph), ImportInfo LinkNode)
followTheories :: LibName -> (ImpEnv, DGraph) -> [OMCD] -> ResultT IO ((ImpEnv, DGraph), [LinkNode])
followTheory :: LibName -> (ImpEnv, DGraph) -> OMCD -> ResultT IO ((ImpEnv, DGraph), LinkNode)
sigmapAccumFun :: (Monad m, Show a) => (SigMapI a -> TCElement -> String -> m a) -> SigMapI a -> TCElement -> m (SigMapI a, a)
initialSig :: AnyLogic -> (NameSymbolMap, G_sign)
localSig :: TCClassification -> NameSymbolMap -> G_sign -> Result (NameSymbolMap, G_sign)
addSentences :: TCClassification -> NameSymbolMap -> G_sign -> Result G_theory
addLinksToDG :: Node -> DGraph -> [LinkInfo] -> DGraph
addLinkToDG :: Node -> DGraph -> LinkInfo -> DGraph
addNodeToDG :: DGraph -> String -> G_theory -> (LNode DGNodeLab, DGraph)
addNodeAsRefToDG :: LNode DGNodeLab -> LibName -> DGraph -> (LNode DGNodeLab, DGraph)
type CurrentLib = (LibName, DGraph)
type LinkNode = (Maybe LibName, LNode DGNodeLab)
type LinkInfo = (GMorphism, DGLinkType, DGLinkOrigin, Node, Maybe Node)
data ImportInfo a = ImportInfo a String TCMorphism
iInfoVal :: ImportInfo a -> a
fmapLI :: Monad m => (GMorphism -> m GMorphism) -> LinkInfo -> m LinkInfo
data TCClassification = TCClf {
- importInfo :: [ImportInfo OMCD]
- sigElems :: [TCElement]
- sentences :: [TCElement]
- adts :: [[OmdADT]]
- notations :: Map OMName String
}
emptyClassification :: TCClassification
classifyTCs :: [TCElement] -> TCClassification
classifyTC :: TCElement -> TCClassification -> TCClassification

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 libMap :: Map FilePath (LibName, DGraph) nsymbMap :: Map (LibName, String) NameSymbolMap hetsOptions :: HetcatsOpts

initialEnv :: HetcatsOpts -> ImpEnv Source #

getLibEnv :: ImpEnv -> LibEnv Source #

addDGToEnv :: ImpEnv -> LibName -> DGraph -> ImpEnv Source #

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

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

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

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 #

libNameFromURL :: String -> IRI -> LibName 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

getLogicFromMeta :: Maybe OMCD -> AnyLogic Source #

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

mkLinkOrigin :: String -> DGLinkOrigin Source #

updateSymbolMap Source #

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

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

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

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

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.

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

Theory-utils

type CurrentLib = (LibName, DGraph) Source #

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

Instances details

Functor ImportInfo Source #
Instance details Defined in OMDoc.Import Methods fmap :: (a -> b) -> ImportInfo a -> ImportInfo b (<$) :: a -> ImportInfo b -> ImportInfo a
Show a => Show (ImportInfo a) Source #
Instance details Defined in OMDoc.Import Methods showsPrec :: Int -> ImportInfo a -> ShowS show :: ImportInfo a -> String showList :: [ImportInfo a] -> ShowS

iInfoVal :: ImportInfo a -> a Source #

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

data TCClassification Source #

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

classifyTCs :: [TCElement] -> TCClassification Source #

classifyTC :: TCElement -> TCClassification -> TCClassification Source #