{-# LANGUAGE ExistentialQuantification #-}
{- |
Module : ./OMDoc/Export.hs
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 id ", showEdgeId (dgl_id lbl)
, " not exported."]) nullRange
>> return (s, Nothing)
| isLocalDef $ dgl_type lbl =
warning () (concat [ "Local def-link id ", showEdgeId (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