{-# LANGUAGE ExistentialQuantification #-}

{- |

Module : $Header$

Description : Transforms an OMDoc file into a development graph

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)

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

-}

module OMDoc.Import where

import Common.Result

import Common.ResultT

import Common.ExtSign

import Common.Id

import Common.IRI

import Common.LibName

import Common.Utils

import Common.XmlParser (readXmlFile)

import Driver.ReadFn (libNameToFile)

import Driver.Options (rmSuffix, HetcatsOpts, putIfVerbose, showDiags)

import Logic.Logic

( AnyLogic (Logic)

, Logic ( omdoc_metatheory, omdocToSym, omdocToSen, addOMadtToTheory

, addOmdocToTheory)

, Category (ide, cod)

, StaticAnalysis ( induced_from_morphism, induced_from_to_morphism

, signature_union, empty_signature, add_symb_to_sign

, symbol_to_raw, id_to_raw )

, Sentences (symmap_of) )

import Logic.ExtSign

import Logic.Coerce

import Logic.Prover

import Logic.Grothendieck

import Comorphisms.LogicList

import Comorphisms.LogicGraph

import Static.DevGraph

import Static.DgUtils

import Static.GTheory

import Static.AnalysisStructured

import Static.ComputeTheory

import OMDoc.DataTypes

import OMDoc.XmlInterface (xmlIn)

import System.Directory

import Data.Graph.Inductive.Graph (LNode, Node)

import Data.Maybe

import Data.List

import qualified Data.Map as Map

import Control.Monad

import Control.Monad.Trans

-- * Import Environment Interface

{- | 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

-}

type NameSymbolMap = G_mapofsymbol OMName

-- | The keys of libMap consist of the filepaths without suffix!

data ImpEnv =

ImpEnv {

libMap :: Map.Map FilePath (LibName, DGraph)

, nsymbMap :: Map.Map (LibName, String) NameSymbolMap

, hetsOptions :: HetcatsOpts

}

initialEnv :: HetcatsOpts -> ImpEnv

initialEnv opts = ImpEnv { libMap = Map.empty

, nsymbMap = Map.empty

, hetsOptions = opts }

getLibEnv :: ImpEnv -> LibEnv

getLibEnv e = computeLibEnvTheories $

Map.fromList $ Map.elems $ libMap e

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

addDGToEnv e ln dg =

e { libMap = Map.insert (libNameToFile ln) (ln, dg) $ libMap e }

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

addNSMapToEnv e ln nm nsm =

e { nsymbMap = Map.insert (ln, nm) nsm $ nsymbMap e }

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

lookupLib e u = Map.lookup (rmSuffix $ iriPath u) $ libMap e

lookupNode :: ImpEnv -> CurrentLib -> IriCD

-> Maybe ( LibName -- the origin libname of the theory

, LNode DGNodeLab -- the (eventually reference) node

)

lookupNode e (ln, dg) ucd =

let mn = getModule ucd in

if cdInLib ucd ln then

case filterLocalNodesByName mn dg of

[] -> error $ "lookupNode: Node not found: " ++ mn

lnode : _ -> Just (ln, lnode)

else case lookupLib e $ fromJust $ getIri ucd of

Nothing -> Nothing

Just (ln', dg') ->

case filterRefNodesByName mn ln' dg of

lnode : _ -> Just (ln', lnode)

[] -> listToMaybe

$ map (\ n -> (ln', n)) $ filterLocalNodesByName mn dg'

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

lookupNSMap e ln mLn nm =

let ln' = fromMaybe ln mLn

mf = Map.findWithDefault

$ error $ concat [ "lookupNSMap: lookup failed for "

, show (ln', nm), "\n", show mLn, "\n"

, show $ nsymbMap e ]

in mf (ln', nm) $ nsymbMap e

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

rPutIfVerbose e n s = lift $ putIfVerbose (hetsOptions e) n s

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

rPut e = rPutIfVerbose e 1

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

rPut2 e = rPutIfVerbose e 2

-- * IRI Functions

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

readFromURL f u = if isFileIRI u then f $ iriPath u

else error $ "readFromURL: Unsupported IRI-scheme "

++ iriScheme u

toIRI :: String -> IRI

toIRI s = case parseIRIReference s of

Just u -> u

_ -> error $ "toIRI: can't parse as iri " ++ s

libNameFromURL :: String -> IRI -> LibName

libNameFromURL s u = setFilePath (iriPath u) $ emptyLibName s

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

resolveIRI :: IRI -> FilePath -> IRI

resolveIRI u fp = fromMaybe (error $ "toIRI: can't resolve iri " ++ show u)

$ relativeTo u $ toIRI fp

-- | Is the scheme of the iri empty or file?

isFileIRI :: IRI -> Bool

isFileIRI u = elem (iriScheme u) ["", "file:"]

type IriCD = (Maybe IRI, String)

showIriCD :: IriCD -> String

showIriCD (mIri, s) = case mIri of

Just u -> show u ++ "?" ++ s

_ -> s

getIri :: IriCD -> Maybe IRI

getIri = fst

getModule :: IriCD -> String

getModule = snd

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

toIriCD :: OMCD -> LibName -> IriCD

toIriCD cd ln =

let [base, m] = cdToList cd

fp = getFilePath ln

mU = if null base then Nothing

else Just $ resolveIRI (toIRI base) fp

in (mU, m)

getLogicFromMeta :: Maybe OMCD -> AnyLogic

getLogicFromMeta mCD =

let p (Logic lid) = case omdoc_metatheory lid of

Just cd' -> fromJust mCD == cd'

_ -> False

in if isNothing mCD then defaultLogic else

case find p logicList of

Just al -> al

_ -> defaultLogic

cdInLib :: IriCD -> LibName -> Bool

cdInLib ucd ln = case getIri ucd of

Nothing -> True

Just url -> isFileIRI url && getFilePath ln == iriPath url

-- * Main translation functions

-- | Translates an OMDoc file to a LibEnv

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

anaOMDocFile opts fp = do

dir <- getCurrentDirectory

putIfVerbose opts 2 $ "Importing OMDoc file " ++ fp

Result ds mEnvLn <- runResultT $ importLib (initialEnv opts)

$ resolveIRI (toIRI fp) $ dir ++ "/"

showDiags opts ds

return $ fmap (\ (env, ln, _) -> (ln, getLibEnv env)) mEnvLn

-- * OMDoc traversal

{- | If the lib is not already in the environment, the OMDoc file and

the closure of its imports is added to the environment. -}

importLib :: ImpEnv -- ^ The import environment

-> IRI -- ^ The url of the OMDoc file

-> ResultT IO (ImpEnv, LibName, DGraph)

importLib e u =

case lookupLib e u of

Just (ln, dg) -> return (e, ln, dg)

_ -> readLib e u

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

readLib :: ImpEnv -- ^ The import environment

-> IRI -- ^ The url of the OMDoc file

-> ResultT IO (ImpEnv, LibName, DGraph)

readLib e u = do

rPut e $ "Downloading " ++ show u ++ " ..."

xmlString <- lift $ readFromURL readXmlFile u

OMDoc n l <- liftR $ xmlIn xmlString

{- the name of the omdoc is used as the libname, no relationship between the

libname and the filepath! -}

let ln = libNameFromURL n u

rPut e $ "Importing library " ++ show ln

(e', dg) <- foldM (addTLToDGraph ln) (e, emptyDG) l

rPut e $ "... loaded " ++ show u

return (addDGToEnv e' ln dg, ln, dg)

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

importTheory :: ImpEnv -- ^ The import environment

-> CurrentLib -- ^ The current lib

-> OMCD -- ^ The cd which points to the Theory

-> ResultT IO ( ImpEnv -- the updated environment

, LibName -- the origin libname of the theory

, DGraph -- the updated devgraph of the current lib

, LNode DGNodeLab -- the corresponding node

)

importTheory e (ln, dg) cd = do

let ucd = toIriCD cd ln

rPut2 e $ "Looking up theory " ++ showIriCD ucd ++ " ..."

case lookupNode e (ln, dg) ucd of

Just (ln', nd)

| ln == ln' ->

do

rPut2 e "... found local node."

return (e, ln, dg, nd)

| isDGRef $ snd nd ->

do

rPut2 e "... found already referenced node."

return (e, ln', dg, nd)

| otherwise ->

do

rPut2 e "... found node, referencing it ..."

let (lnode, dg') = addNodeAsRefToDG nd ln' dg

rPut2 e "... done"

return (e, ln', dg', lnode)

-- if lookupNode finds nothing implies that ln is not the current libname!

_ -> do

let u = fromJust $ getIri ucd

rPut2 e "... node not found, reading lib."

(e', ln', refDg) <- readLib e u

case filterLocalNodesByName (getModule ucd) refDg of

-- don't add the node to the refDG but to the original DG!

nd : _ -> let (lnode, dg') = addNodeAsRefToDG nd ln' dg

in return (e', ln', dg', lnode)

[] -> error $ "importTheory: couldn't find node: " ++ show cd

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

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

-> ResultT IO (ImpEnv, DGraph)

-- adding a theory to the DG

addTLToDGraph ln (e, dg) (TLTheory n mCD l) = do

rPut e $ "Importing theory " ++ n

let clf = classifyTCs l

{- I. Lookup all imports (= follow and create them first),

and insert DGNodeRefs if neccessary. -}

((e', dg'), iIL) <- followImports ln (e, dg) $ importInfo clf

-- II. Compute morphisms and update initial sig and name symbol map stepwise.

((nsmap, gSig), iIWL) <-

computeMorphisms e' ln (notations clf)

(initialSig $ getLogicFromMeta mCD) iIL

-- III. Compute local signature

(nsmap', gSig') <- liftR $ localSig clf nsmap gSig

-- IV. Add the sentences to the Node.

gThy <- liftR $ addSentences clf nsmap' gSig'

-- V. Complete the morphisms with final signature

iIWL' <- liftR $ completeMorphisms (signOf gThy) iIWL

-- VI. Add the Node to the DGraph.

let ((nd, _), dg'') = addNodeToDG dg' n gThy

-- VII. Create links from the morphisms.

dg''' = addLinksToDG nd dg'' iIWL'

-- add the new name symbol map to the environment

e'' = addNSMapToEnv e' ln n nsmap'

return (e'', dg''')

addTLToDGraph ln (e, dg) (TLView n from to mMor) = do

rPut e $ "Importing view " ++ n

{- follow the source and target of the view and insert DGNodeRefs

if neccessary.

use followTheory for from and to. -}

((e', dg'), [lkNdFrom, lkNdTo]) <- followTheories ln (e, dg) [from, to]

lkInf <- computeViewMorphism e' ln $ ImportInfo (lkNdFrom, lkNdTo) n mMor

let dg'' = addLinkToDG

{- this error should never occur as the linkinfo contains

a to-node.

The error is used here as a "don't care element" of type Node -}

(error "addTLToDGraph: TLView - Default node not available")

dg' lkInf

return (e', dg'')

-- ** Utils to compute DGNodes from OMDoc Theories

{-

the morphisms are incomplete because the target signature

wasn't complete at the time of morphism computation.

we complete the morphisms by composing them with signature inclusions

to the complete target signature

-}

completeMorphisms :: G_sign -- ^ the complete target signature

-> [LinkInfo] -- ^ the incomplete morphisms

-> Result [LinkInfo]

completeMorphisms gsig = mapR (fmapLI $ completeMorphism $ ide gsig)

completeMorphism :: GMorphism -- ^ the target signature id morphism

-> GMorphism -- ^ the incomplete morphism

-> Result GMorphism

completeMorphism idT gmorph = compInclusion logicGraph gmorph idT

computeMorphisms :: ImpEnv -> LibName

-> Map.Map OMName String -- ^ Notations

-> (NameSymbolMap, G_sign)

-> [ImportInfo LinkNode]

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

computeMorphisms e ln nots = mapAccumLM (computeMorphism e ln nots)

{- | Computes the morphism for an import link and updates the signature

and the name symbol map with the imported symbols -}

computeMorphism :: ImpEnv -- ^ The import environment for lookup purposes

-> LibName -- ^ Current libname

-> Map.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)

computeMorphism e ln nots (nsmap, tGSig) (ImportInfo (mLn, (from, lbl)) n morph)

= case dgn_theory lbl of

G_theory sLid _ (ExtSign sSig _) _ _ _ ->

case tGSig of

G_sign tLid (ExtSign tSig _) sigId ->

do

let sourceNSMap = lookupNSMap e ln mLn $ getDGNodeName lbl

{- 1. build the morphism

compute first the symbol-map -}

symMap <- computeSymbolMap (Just nots) sourceNSMap nsmap

morph tLid

let

f = symbol_to_raw tLid

g (Left (_, rs)) = rs

g (Right s) = symbol_to_raw tLid s

rsMap = Map.fromList $ map (\ (x, y) -> (f x, g y) )

symMap

-- REMARK: Logic-homogeneous environment assumed

sSig' <- coercePlainSign sLid tLid "computeMorphism" sSig

mor <- liftR $ induced_from_morphism tLid rsMap sSig'

{- 2. build the GMorphism and update the signature

and the name symbol map -}

newSig <- liftR $ signature_union tLid tSig $ cod mor

let gMor = gEmbed $ mkG_morphism tLid mor

newGSig = G_sign tLid (makeExtSign tLid newSig) sigId

{- function for filtering the raw symbols in the

nsmap update -}

h (s, Left (n', _)) = Just (s, n')

h (_, Right _) = Nothing

nsmap' = updateSymbolMap tLid mor nsmap

$ mapMaybe h symMap

return ( (nsmap', newGSig)

, (gMor, globalDef, mkLinkOrigin n, from, Nothing))

-- | Computes the morphism for a view

computeViewMorphism :: ImpEnv -- ^ The import environment for lookup purposes

-> LibName -- ^ Current libname

-> ImportInfo (LinkNode, LinkNode)

-- ^ OMDoc morphism with source and target node

-> ResultT IO LinkInfo

computeViewMorphism e ln (ImportInfo ( (mSLn, (from, lblS))

, (mTLn, (to, lblT))) n morph)

= case (dgn_theory lblS, dgn_theory lblT) of

(G_theory sLid _ eSSig _ _ _, G_theory tLid _ eTSig _ _ _) ->

do

let nsmapS = lookupNSMap e ln mSLn $ getDGNodeName lblS

nsmapT = lookupNSMap e ln mTLn $ getDGNodeName lblT

{- 1. build the morphism

compute first the symbol-map -}

symMap <- computeSymbolMap Nothing nsmapS nsmapT morph tLid

let f = symbol_to_raw tLid

{- this can't occur as we do not provide a notation map

to computeSymbolMap -}

g (Left _) = error "computeViewMorphism: impossible case"

g (Right s) = symbol_to_raw tLid s

rsMap = Map.fromList

$ map (\ (x, y) -> (f x, g y) ) symMap

-- REMARK: Logic-homogeneous environment assumed

eSSig' <- coerceSign sLid tLid "computeViewMorphism" eSSig

mor <- liftR $ induced_from_to_morphism tLid rsMap eSSig' eTSig

-- 2. build the GMorphism

let gMor = gEmbed $ mkG_morphism tLid mor

return (gMor, globalThm, mkLinkOrigin n, from, Just to)

mkLinkOrigin :: String -> DGLinkOrigin

mkLinkOrigin s = DGLinkMorph $ simpleIdToIRI $ mkSimpleId s

{- | For each entry (s, n) in l we enter the mapping (n, m(s))

to the name symbol map -}

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 -- ^ a signature morphism m

-> NameSymbolMap

-> [(symbol, OMName)] -- ^ a list l of symbol to OMName mappings

-> NameSymbolMap

updateSymbolMap lid mor nsmap l =

case nsmap of

G_mapofsymbol lid' sm ->

let f nsm (s, n) = Map.insert n (g s) nsm -- fold function

g s = Map.findWithDefault

(error $ "updateSymbolMap: symbol not found " ++ show s)

s $ symmap_of lid mor

sm' = coerceMapofsymbol lid' lid sm

in G_mapofsymbol lid $ foldl f sm' l

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

-}

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.Map OMName String) -- ^ Notations for missing symbols in map

-> NameSymbolMap -> NameSymbolMap -> TCMorphism -> lid

-> ResultT IO [(symbol, Either (OMName, raw_symbol) symbol)]

computeSymbolMap mNots nsmapS nsmapT morph lid =

case (nsmapS, nsmapT) of

(G_mapofsymbol sLid sm, G_mapofsymbol tLid tm) ->

do

-- REMARK: Logic-homogeneous environment assumed

let sNSMap = coerceMapofsymbol sLid lid sm

tNSMap = coerceMapofsymbol tLid lid tm

mf msg = Map.findWithDefault

$ error $ "computeSymbolMap: lookup failed for " ++ msg

-- function for notation lookup

g = lookupNotationInMap

$ fromMaybe (error "computeSymbolMap: no notations") mNots

-- function for map

f (omn, omimg) =

let tSymName = case omimg of

Left s -> mkSimpleName s

Right (OMS qn) -> unqualName qn

_ -> error $ "computeSymbolMap: Nonsymbol "

++ "element mapped"

in ( mf (show omn) omn sNSMap

, case Map.lookup tSymName tNSMap of

Just ts -> Right ts

_ -> Left (tSymName, id_to_raw lid $ nameToId

$ g tSymName))

return $ map f morph

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

-> ResultT IO ((ImpEnv, DGraph), [ImportInfo LinkNode])

followImports ln = mapAccumLCM (curry snd) (followImport ln)

{- | Ensures that the theory for the given OMCD is available in the environment.

See also 'followTheory' -}

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

-> ResultT IO ((ImpEnv, DGraph), ImportInfo LinkNode)

followImport ln x iInfo = do

(x', linknode) <- followTheory ln x $ iInfoVal iInfo

return (x', fmap (const linknode) iInfo)

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

-> ResultT IO ((ImpEnv, DGraph), [LinkNode])

followTheories ln = mapAccumLCM (curry snd) (followTheory ln)

{- | We lookup the theory referenced by the cd in the environment

and add it if neccessary to the environment. -}

followTheory :: LibName -> (ImpEnv, DGraph) -> OMCD

-> ResultT IO ((ImpEnv, DGraph), LinkNode)

followTheory ln (e, dg) cd = do

(e', ln', dg', lnode) <- importTheory e (ln, dg) cd

let mLn = if ln == ln' then Nothing else Just ln'

return ((e', dg'), (mLn, lnode))

-- * Development Graph and LibEnv interface

{- | returns a function compatible with mapAccumLM for TCElement processing.

Used in localSig. -}

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

-> SigMapI a -> TCElement -> m (SigMapI a, a)

sigmapAccumFun f smi s = do

let n = tcName s

hetsname = lookupNotation smi n

s' <- f smi s hetsname

let smi' = smi { sigMapISymbs = Map.insert n s' $ sigMapISymbs smi }

return (smi', s')

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

initialSig :: AnyLogic -> (NameSymbolMap, G_sign)

initialSig lg =

case lg of

Logic lid ->

( G_mapofsymbol lid Map.empty

, G_sign lid (makeExtSign lid $ empty_signature lid) startSigId)

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

localSig :: TCClassification -> NameSymbolMap -> G_sign

-> Result (NameSymbolMap, G_sign)

localSig clf nsmap gSig =

case (gSig, nsmap) of

(G_sign lid _ _, G_mapofsymbol lid' sm) ->

do

let smi = SigMapI (coerceMapofsymbol lid' lid sm) $ notations clf

{- accumulates symbol mappings in the symbMap in SigMapI

while creating symbols from OMDoc symbols -}

(sm', symbs) <- mapAccumLM (sigmapAccumFun $ omdocToSym lid) smi

$ sigElems clf

-- adding the symbols to the empty signature

sig <- foldM (add_symb_to_sign lid) (empty_signature lid) symbs

let locGSig = G_sign lid (makeExtSign lid sig) startSigId

-- combining the local and the given signature

gSig' <- gsigUnion logicGraph True gSig locGSig

return (G_mapofsymbol lid $ sigMapISymbs sm', gSig')

-- | Adds sentences and logic dependent signature elements to the given sig

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

addSentences clf nsmap gsig =

case (nsmap, gsig) of

(G_mapofsymbol lidM sm, G_sign lid (ExtSign sig _) ind1) ->

do

let sigm = SigMapI (coerceMapofsymbol lidM lid sm)

$ notations clf

-- 1. translate sentences

mSens <- mapM (\ tc -> omdocToSen lid sigm tc

$ lookupNotation sigm $ tcName tc) $ sentences clf

-- 2. translate adts

(sig', sens') <- addOMadtToTheory lid sigm (sig, catMaybes mSens)

$ adts clf

{- 3. translate rest of theory

(all the sentences or just those which returned Nothing?) -}

(sig'', sens'') <- addOmdocToTheory lid sigm (sig', sens')

$ sentences clf

return $ G_theory lid Nothing (mkExtSign sig'') ind1

(toThSens sens'') startThId

-- | Adds Edges from the LinkInfo list to the development graph.

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

addLinksToDG nd = foldl (addLinkToDG nd)

-- | Adds Edge from the LinkInfo to the development graph.

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

addLinkToDG to dg (gMor, lt, lo, from, mTo) =

insLink dg gMor lt lo from $ fromMaybe to mTo

-- | Adds a Node from the given 'G_theory' to the development graph.

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

addNodeToDG dg n gth =

let nd = getNewNodeDG dg

ndName = parseNodeName n

ndInfo = newNodeInfo DGBasic

newNode = (nd, newInfoNodeLab ndName ndInfo gth)

in (newNode, insNodeDG newNode dg)

addNodeAsRefToDG :: LNode DGNodeLab -> LibName -> DGraph

-> (LNode DGNodeLab, DGraph)

addNodeAsRefToDG (nd, lbl) ln dg =

let info = newRefInfo ln nd

refNodeM = lookupInAllRefNodesDG info dg

nd' = getNewNodeDG dg

lnode = (nd', lbl { nodeInfo = info })

dg1 = insNodeDG lnode dg

in case refNodeM of

Just refNode -> ((refNode, labDG dg refNode), dg)

_ -> (lnode, dg1)

-- * Theory-utils

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 deriving Show

iInfoVal :: ImportInfo a -> a

iInfoVal (ImportInfo x _ _) = x

instance Functor ImportInfo where

fmap f (ImportInfo x y z) = ImportInfo (f x) y z

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

fmapLI f (gm, x, y, z, t) = do

gm' <- f gm

return (gm', x, y, z, t)

data TCClassification = TCClf {

importInfo :: [ImportInfo OMCD] -- ^ Import-info

, sigElems :: [TCElement] -- ^ Signature symbols

, sentences :: [TCElement] -- ^ Theory sentences

, adts :: [[OmdADT]] -- ^ ADTs

, notations :: Map.Map OMName String -- ^ Notations

}

emptyClassification :: TCClassification

emptyClassification = TCClf [] [] [] [] Map.empty

classifyTCs :: [TCElement] -> TCClassification

classifyTCs = foldr classifyTC emptyClassification

classifyTC :: TCElement -> TCClassification -> TCClassification

classifyTC tc clf =

case tc of

TCSymbol _ _ sr _

| elem sr [Obj, Typ] -> clf { sigElems = tc : sigElems clf }

| otherwise -> clf { sentences = tc : sentences clf }

TCNotation (cd, omn) n (Just "hets") ->

if cdIsEmpty cd then

clf { notations = Map.insert omn n $ notations clf }

else clf

TCADT l -> clf { adts = l : adts clf }

TCImport n from morph ->

clf { importInfo = ImportInfo from n morph : importInfo clf }

TCComment _ -> clf

TCSmartNotation {} -> error "classifyTC: unexpected SmartNotation"

TCFlexibleNotation {} ->

error "classifyTC: unexpected FlexibleNotation"

-- just for the case TCNotation with a style different from hets

_ -> clf