{-# LANGUAGE ExistentialQuantification #-}

{- |

Module : $Header$

Description : Exports a development graph to an omdoc structure

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)

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

-}

module OMDoc.Export where

import Logic.Logic ( Logic ( omdoc_metatheory, export_theoryToOmdoc

, export_symToOmdoc, export_senToOmdoc)

, Sentences (sym_name, symmap_of), symlist_of

, SyntaxTable, syntaxTable)

import Logic.Coerce

import Logic.Prover

import Logic.Grothendieck

import Logic.Comorphism

import Static.DevGraph

import Static.DgUtils

import Static.GTheory

import Common.Result

import Common.ExtSign

import Common.Id

import Common.Utils

import Common.LibName

import Common.AS_Annotation

import Common.Prec (maxWeight, precMap)

import Driver.Options (downloadExtensions)

import Driver.WriteLibDefn (getFilePrefixGeneric)

import OMDoc.DataTypes

import Data.Graph.Inductive.Graph

import Data.Maybe

import Data.List

import qualified Data.Map as Map

import qualified Data.Set as Set

import Control.Monad (liftM)

import System.FilePath

-- * 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. -}

data GSigMap = GSigMap (G_symbolmap (Int, UniqName)) (NameMap String)

{- | We need this type to store the original dependency order.

This type is the logic dependent analogue to the GSigMap -}

type NumberedSigMap a = (Map.Map a (Int, UniqName), NameMap String)

-- | Removes the numbering from the symbol map

nSigMapToSigMap :: NumberedSigMap a -> SigMap a

nSigMapToSigMap (nMap, sMap) = SigMap (Map.map snd nMap) sMap

-- | Computes a dependency sorted (symbol - unique name) list

nSigMapToOrderedList :: NumberedSigMap a -> [(a, UniqName)]

nSigMapToOrderedList (nMap, _) = let

compByPos (_, (pos1, _)) (_, (pos2, _)) = compare pos1 pos2

sortedList = sortBy compByPos $ Map.toList nMap

in map (\ (a, x) -> (a, snd x)) sortedList

-- | Mapping of Specs to SigMaps

newtype SpecSymNames = SpecSymNames (Map.Map (LibName, String) GSigMap)

-- | The export environment

data ExpEnv = ExpEnv { getSSN :: SpecSymNames

, getInitialLN :: LibName

, getFilePathMapping :: Map.Map LibName FilePath }

fmapNM :: (Ord a, Ord b) => (a -> b) -> NameMap a -> NameMap b

fmapNM = Map.mapKeys

emptyEnv :: LibName -> ExpEnv

emptyEnv ln = ExpEnv { getSSN = SpecSymNames Map.empty

, getInitialLN = ln

, getFilePathMapping = Map.empty }

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

fromSignAndNamedSens lid sig nsens =

let syms = symlist_of lid sig

{- The accumulator var is a map of names to integer values designating

the next identifier to use for this name to make it unique.

acc: Map String Int -}

newName acc s =

let (v, acc') = Map.insertLookupWithKey (const (+)) s 1 acc

in (acc', (s, fromMaybe 0 v))

{- We need to store in addition to the name-int-map an integer to

increment in order to remember the original order of the signature

elements after having destroyed it by making a map from the list.

for that reason we use the following accumvar:

acc: (Int, Map String Int) -}

symF (i, acc) x = let (acc', nn) = newName acc $ show $ sym_name lid x

in ((i + 1, acc'), (x, (i, nn)))

sensF acc x = let n = senAttr x

(acc', nn) = newName acc n in (acc', (n, nn))

(cm, symL) = mapAccumL symF (0, Map.empty) syms

(_, sensL) = mapAccumL sensF (snd cm) nsens

in (Map.fromList symL, Map.fromList sensL)

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

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)

lookupWithInsert lid sig sens s k =

let SpecSymNames m = getSSN s in

case Map.lookup k m of

Just (GSigMap (G_symbolmap lid1 sm) nm) ->

(s, (coerceSymbolmap lid1 lid sm, nm))

Nothing -> let nsigm@(sm, nm) = fromSignAndNamedSens lid sig sens

gsm = GSigMap (G_symbolmap lid sm) nm

in ( s { getSSN = SpecSymNames $ Map.insert k gsm m }, nsigm)

-- * LibEnv traversal

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

exportLibEnv :: Bool -- recursive

-> FilePath -- outdir

-> LibName -> LibEnv

-> Result [(LibName, OMDoc)]

exportLibEnv b odir ln le =

let cmbnF (x, _) y = (x, y)

inputList = if b then Map.toList le else [(ln, lookupDGraph ln le)]

fpm = initFilePathMapping odir le

im = (emptyEnv ln) { getFilePathMapping = fpm }

f (ln', o) = let fp = Map.findWithDefault

(error "exportLibEnv: filepath not mapped")

ln' fpm

in (setFilePath fp ln', o)

in do

l <- liftM snd $ mapAccumLCM cmbnF (exportDGraph le) im inputList

return $ map f l

initFilePathMapping :: FilePath -> LibEnv -> Map.Map LibName FilePath

initFilePathMapping fp le =

let f k _ = snd (getFilePrefixGeneric downloadExtensions fp

$ getFilePath k) ++ ".omdoc"

in Map.mapWithKey f le

-- | DGraph to OMDoc translation

exportDGraph :: LibEnv -> ExpEnv -> (LibName, DGraph) -> Result (ExpEnv, OMDoc)

exportDGraph le s (ln, dg) = do

(s', theories) <- mapAccumLM (exportNodeLab le ln dg) s

$ topsortedNodes dg

(s'', views) <- mapAccumLM (exportLinkLab le ln dg) s' $ labEdgesDG dg

return (s'', OMDoc (show $ getLibId ln)

$ catMaybes theories ++ catMaybes views)

-- | DGNodeLab to TLTheory translation

exportNodeLab :: LibEnv -> LibName -> DGraph -> ExpEnv -> LNode DGNodeLab

-> Result (ExpEnv, Maybe TLElement)

exportNodeLab le ln dg s (n, lb) =

if isDGRef lb then return (s, Nothing) else

let (lb', ln') = getNodeData le ln lb in

case dgn_theory lb' of

G_theory lid _ (ExtSign sig _) _ sens _ ->

do

let sn = getDGNodeName lb'

nsens = toNamedList sens

(s', nsigm) = lookupWithInsert lid sig nsens s (ln', sn)

sigm@(SigMap nm _) = nSigMapToSigMap nsigm

{- imports is a list of Maybe (triples, exported-symbol

set) pairs as described in 'makeImportMapping'. We

construct the concrete OMImages later (see

makeImport) in order to prevent multiple imported

constants to be declared by open as a new constant.

We must use open for the first occurence and conass

for the others, i.e., Left resp. Right constructors

of the OMImage datatype -}

(s'', imports) <-

mapAccumLM (makeImportMapping le ln dg (lid, nm)) s'

$ innDG dg n

{- mappingL: list of the triples described above

symsetL: used to compute the local symbols (not imported) -}

let (mappingL, symsetL) = unzip $ catMaybes imports

(_, importL) = mapAccumL makeImport Set.empty mappingL

mSynTbl = syntaxTable lid sig

extra <- export_theoryToOmdoc lid sigm sig nsens

consts <- mapR (uncurry $ exportSymbol lid sigm mSynTbl symsetL)

$ nSigMapToOrderedList nsigm

-- create the OMDoc elements for the sentences

thms <- mapR (exportSentence lid sigm) nsens

return (s'', Just $ TLTheory sn (omdoc_metatheory lid)

$ concat

[importL, concat consts, extra, concat thms])

-- * Views and Morphisms

-- Node lookup for handling ref nodes

getNodeData :: LibEnv -> LibName -> DGNodeLab -> (DGNodeLab, LibName)

getNodeData le ln lb =

if isDGRef lb then

let ni = nodeInfo lb

lnRef = ref_libname ni

dg' = Map.findWithDefault

(error $ "getNodeData: Lib not found: " ++ show lnRef)

lnRef le

in (labDG dg' $ ref_node ni, lnRef)

else (lb, ln)

{- See the comment in exportNodeLab for details about this function.

The set is only to accumulate the mapped symbols (the targets, not

the sources!) in order to decide whether to just map the symbol to

a previously mapped symbol or to create an alias! -}

makeImport :: Set.Set UniqName -> (String, OMCD, [(OMName, UniqName)])

-> (Set.Set UniqName, TCElement)

makeImport s (n, cd, mapping) =

let f s' p@(_, un)

| Set.notMember un s' =

(Set.insert un s', makeMorphismEntry True p)

| otherwise = (s', makeMorphismEntry False p)

(s'', morph) = mapAccumL f s mapping

in (s'', TCImport n cd morph)

{- | If the link is a global definition link we compute the Import

and return also the set of (by the link) exported symbols. -}

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

{- the triple consists of:

name of the import

target CD

actual mapping as returned by makeMorphism -}

, Maybe ( (String, OMCD, [(OMName, UniqName)])

-- symbols exported by the morphism

, Set.Set symbol))

makeImportMapping le ln dg toInfo s (from, _, lbl)

| isHidingEdge $ dgl_type lbl =

warning () (concat [ "Hiding link with ", show (dgl_id lbl)

, " not exported."]) nullRange

>> return (s, Nothing)

| isLocalDef $ dgl_type lbl =

warning () (concat [ "Local def-link with ", show (dgl_id lbl)

, " not exported."]) nullRange

>> return (s, Nothing)

| isGlobalDef $ dgl_type lbl =

let (lb', ln') = getNodeData le ln $ labDG dg from

edgName = dglName lbl

impname = if null edgName

then "gn_imp_" ++ showEdgeId (dgl_id lbl)

else edgName

in

case dgn_theory lb' of

G_theory lid _ (ExtSign sig _) _ sens _ ->

do

let sn = getDGNodeName lb'

nsens = toNamedList sens

(s', nsigm) = lookupWithInsert lid sig nsens s (ln', sn)

SigMap nm _ = nSigMapToSigMap nsigm

(morph, expSymbs) <-

makeMorphism (lid, nm) toInfo $ dgl_morphism lbl

cd <- mkCD s' ln ln' sn

return (s', Just ((impname, cd, morph), expSymbs))

| otherwise = return (s, Nothing)

-- | Given a TheoremLink we output the view

exportLinkLab :: LibEnv -> LibName -> DGraph -> ExpEnv -> LEdge DGLinkLab

-> Result (ExpEnv, Maybe TLElement)

exportLinkLab le ln dg s (from, to, lbl) =

let ltyp = dgl_type lbl

gmorph = dgl_morphism lbl

edgName = dglName lbl

viewname = if null edgName

then "gn_vn_" ++ showEdgeId (dgl_id lbl)

else edgName

(lb1, ln1) = getNodeData le ln $ labDG dg from

(lb2, ln2) = getNodeData le ln $ labDG dg to

noExport = return (s, Nothing)

withWarning lt = warning () (concat [ "exportLinkLab: ", lt

, " link with ", show (dgl_id lbl)

, " not exported."])

nullRange >> noExport

in case (isDefEdge ltyp, isLocalEdge ltyp, isHidingEdge ltyp) of

(True, _, _) -> noExport

(_, True, _) -> withWarning "Local"

(_, _, True) -> withWarning "Hiding"

_ ->

case (dgn_theory lb1, dgn_theory lb2) of

{ (G_theory lid1 _ (ExtSign sig1 _) _ sens1 _ ,

G_theory lid2 _ (ExtSign sig2 _) _ sens2 _ ) ->

do

let sn1 = getDGNodeName lb1

sn2 = getDGNodeName lb2

nsens1 = toNamedList sens1

nsens2 = toNamedList sens2

(s', nsigm1) =

lookupWithInsert lid1 sig1 nsens1 s (ln1, sn1)

(s'', nsigm2) =

lookupWithInsert lid2 sig2 nsens2 s' (ln2, sn2)

SigMap nm1 _ = nSigMapToSigMap nsigm1

SigMap nm2 _ = nSigMapToSigMap nsigm2

(preMorph, _) <-

makeMorphism (lid1, nm1) (lid2, nm2) gmorph

let morph = map (makeMorphismEntry False) preMorph

cd1 <- mkCD s'' ln ln1 sn1

cd2 <- mkCD s'' ln ln2 sn2

return (s'', Just $ TLView viewname cd1 cd2 morph) }

makeMorphismEntry :: Bool -> (OMName, UniqName)

-> (OMName, OMImage)

makeMorphismEntry useOpen (n, un) =

(n, if useOpen then Left $ nameToString un else Right $ simpleOMS un)

{- | From the given GMorphism we compute the symbol-mapping and return

also the set of (by the morphism) exported symbols (= image of morphism) -}

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.Set symbol2)

makeMorphism (l1, symM1) (l2, symM2)

(GMorphism cid (ExtSign sig _) _ mor _)

{- l1 = logic1

l2 = logic2

lS = source-logic-cid

lT = target-logic-cid -}

-- metaknowledge: l1 = lS, l2 = lT

{- sigmap1 :: l1

sigmap2 :: l2 -}

{- mor :: of target-logic-cid

symmap_of lT mor :: EndoMap symbolT -}

{- comorphism based map:

(sglElem (show cid) . map_symbol cid sig . coerceSymbol l1 lS)

:: symbol1 -> symbolT -}

{- we need sigmap1 :: lT

we need sigmap2 :: lT

for sigmap2 we take a simple coerce

for sigmap1 we take a simple coerce if we know that l1 = l2

otherwise a comorphism fmap composed with a simple coerce -}

= let lS = sourceLogic cid

lT = targetLogic cid

f = if isIdComorphism (Comorphism cid)

then coerceSymbol l1 lT

else sglElem (show cid) . map_symbol cid sig . coerceSymbol l1 lS

symM1' = fmapNM f symM1

symM2' = fmapNM (coerceSymbol l2 lT) symM2

mormap = symmap_of lT mor

expSymbs = Set.fromList $ Map.elems $ coerceMapofsymbol lT l2 mormap

in return (map (mapEntry lT symM1' symM2')

$ Map.toList mormap, expSymbs)

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)

mapEntry _ m1 m2 (s1, s2) =

let e = error "mapEntry: symbolmapping is missing"

un1 = Map.findWithDefault e s1 m1

un2 = Map.findWithDefault e s2 m2

in (omName un1, un2)

-- | extracts the single element from singleton sets, fails otherwise

sglElem :: String -> Set.Set a -> a

sglElem s sa

| Set.size sa > 1 =

error $ "OMDocExport: comorphism symbol image > 1 in " ++ s

| Set.null sa =

error $ "OMDocExport: empty comorphism symbol image in " ++ s

| otherwise = Set.findMin sa

-- * Names and CDs

mkCD :: ExpEnv -> LibName -> LibName -> String -> Result OMCD

mkCD s lnCurr ln sn =

let m = getFilePathMapping s

fp = Map.findWithDefault

(error $ "mkCD: no entry for " ++ show ln) ln m

fpCurr = Map.findWithDefault

(error $ "mkCD: no current entry for " ++ show lnCurr) lnCurr m

-- compute the relative path

fpRel = makeRelativeDesc (takeDirectory fpCurr) fp

fpRel' = if isAbsolute fpRel then "file://" ++ fpRel else fpRel

base = if lnCurr == ln then [] else [fpRel']

in return $ CD $ sn : base

-- * 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.Set symbol] -> symbol

-> UniqName -> Result [TCElement]

exportSymbol lid (SigMap sm _) mSynTbl sl sym n =

let symNotation = mkNotation n $ fmap (\ x -> (sym_name lid sym, x)) mSynTbl

in if all (Set.notMember sym) sl

then do

symConst <- export_symToOmdoc lid sm sym $ nameToString n

return $ symConst : symNotation

else return symNotation

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]

exportSentence lid (SigMap sm thm) nsen = do

omobjOrAdt <- export_senToOmdoc lid sm $ sentence nsen

let symRole = if isAxiom nsen && not (wasTheorem nsen) then Axiom

else Theorem

thmName = senAttr nsen

un = Map.findWithDefault

(error $ concat [ "exportSentence: mapping for "

, thmName, " is missing!"]) thmName thm

omname = nameToString un

case omobjOrAdt of

Left adt ->

warning () ("Name for adt not exported: " ++ show omname) nullRange

>> return [adt]

Right omobj ->

return $ TCSymbol omname omobj symRole Nothing :

mkNotation un Nothing

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

mkNotation :: UniqName -> Maybe (Id, SyntaxTable) -> [TCElement]

mkNotation un mIdSTbl =

let n = nameToString un

orign = fst un

qn = mkSimpleQualName un

l = if n == orign then []

else [TCNotation qn orign $ Just "hets"]

in case mIdSTbl of

Just (symid, (pMap, aMap))

| isMixfix symid ->

let p = Map.findWithDefault (maxWeight pMap) symid

$ precMap pMap

-- we use numbers instead of associativity values

a = case Map.lookup symid aMap of

Just ALeft -> LeftAssoc

Just ARight -> RightAssoc

_ -> NoneAssoc

(appNotation, opStr) = mkApplicationNotation qn symid p a

l' = appNotation : l

l'' = TCNotation qn opStr Nothing : l'

in if null opStr then l' else l''

| otherwise -> l

_ -> l

{- | This function requires mixfix Ids as input and generates Notation

structures, see 'OMDoc.DataTypes'. If smart notations are produced we also

provide a string for a constant notation. -}

mkApplicationNotation :: OMQualName -> Id -> Int -> Assoc -> (TCElement, String)

mkApplicationNotation qn symid@(Id toks _ _) prec asc

| placeCount symid == 1 = case toks of

[a, b]

| isPlace a ->

(mkSmartNotation qn (tokStr b) Postfix prec asc, tokStr b)

| otherwise ->

(mkSmartNotation qn (tokStr a) Prefix prec asc, tokStr a)

_ -> (mkFlexibleNotation qn symid prec, "")

| placeCount symid == 2 = case toks of

[_, b, _]

| not (isPlace b) ->

(mkSmartNotation qn (tokStr b) Infix prec asc, tokStr b)

| otherwise -> (mkFlexibleNotation qn symid prec, "")

_ -> (mkFlexibleNotation qn symid prec, "")

| otherwise = (mkFlexibleNotation qn symid prec, "")

{- | See OMDoc.DataTypes for a description of SmartNotation. We set

the number of implicit arguments to 0. -}

mkSmartNotation :: OMQualName -> String -> Fixity -> Int -> Assoc -> TCElement

mkSmartNotation qn _ fx prec asc = TCSmartNotation qn fx asc prec 0

mkFlexibleNotation :: OMQualName -> Id -> Int -> TCElement

mkFlexibleNotation qn opid prec =

let f acc tok = if isPlace tok then (acc + 1, ArgComp acc prec)

else (acc, TextComp $ tokStr tok)

in TCFlexibleNotation qn prec $ snd $ mapAccumL f 1 $ getTokens opid