{-# 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 :: NumberedSigMap a -> SigMap a
nSigMapToSigMap (nMap :: Map a (Int, UniqName)
nMap, sMap :: NameMap String
sMap) = NameMap a -> NameMap String -> SigMap a
forall a. NameMap a -> NameMap String -> SigMap a
SigMap (((Int, UniqName) -> UniqName) -> Map a (Int, UniqName) -> NameMap a
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Int, UniqName) -> UniqName
forall a b. (a, b) -> b
snd Map a (Int, UniqName)
nMap) NameMap String
sMap

-- | Computes a dependency sorted (symbol - unique name) list
nSigMapToOrderedList :: NumberedSigMap a -> [(a, UniqName)]
nSigMapToOrderedList :: NumberedSigMap a -> [(a, UniqName)]
nSigMapToOrderedList (nMap :: Map a (Int, UniqName)
nMap, _) = let
    compByPos :: (a, (a, b)) -> (a, (a, b)) -> Ordering
compByPos (_, (pos1 :: a
pos1, _)) (_, (pos2 :: a
pos2, _)) = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
pos1 a
pos2
    sortedList :: [(a, (Int, UniqName))]
sortedList = ((a, (Int, UniqName)) -> (a, (Int, UniqName)) -> Ordering)
-> [(a, (Int, UniqName))] -> [(a, (Int, UniqName))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (a, (Int, UniqName)) -> (a, (Int, UniqName)) -> Ordering
forall a a b a b. Ord a => (a, (a, b)) -> (a, (a, b)) -> Ordering
compByPos ([(a, (Int, UniqName))] -> [(a, (Int, UniqName))])
-> [(a, (Int, UniqName))] -> [(a, (Int, UniqName))]
forall a b. (a -> b) -> a -> b
$ Map a (Int, UniqName) -> [(a, (Int, UniqName))]
forall k a. Map k a -> [(k, a)]
Map.toList Map a (Int, UniqName)
nMap
    in ((a, (Int, UniqName)) -> (a, UniqName))
-> [(a, (Int, UniqName))] -> [(a, UniqName)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: a
a, x :: (Int, UniqName)
x) -> (a
a, (Int, UniqName) -> UniqName
forall a b. (a, b) -> b
snd (Int, UniqName)
x)) [(a, (Int, UniqName))]
sortedList


-- | Mapping of Specs to SigMaps
newtype SpecSymNames = SpecSymNames (Map.Map (LibName, String) GSigMap)


-- | The export environment
data ExpEnv = ExpEnv { ExpEnv -> SpecSymNames
getSSN :: SpecSymNames
                     , ExpEnv -> LibName
getInitialLN :: LibName
                     , ExpEnv -> Map LibName String
getFilePathMapping :: Map.Map LibName FilePath }

fmapNM :: (Ord a, Ord b) => (a -> b) -> NameMap a -> NameMap b
fmapNM :: (a -> b) -> NameMap a -> NameMap b
fmapNM = (a -> b) -> NameMap a -> NameMap b
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys

emptyEnv :: LibName -> ExpEnv
emptyEnv :: LibName -> ExpEnv
emptyEnv ln :: LibName
ln = ExpEnv :: SpecSymNames -> LibName -> Map LibName String -> ExpEnv
ExpEnv { getSSN :: SpecSymNames
getSSN = Map (LibName, String) GSigMap -> SpecSymNames
SpecSymNames Map (LibName, String) GSigMap
forall k a. Map k a
Map.empty
                     , getInitialLN :: LibName
getInitialLN = LibName
ln
                     , getFilePathMapping :: Map LibName String
getFilePathMapping = Map LibName String
forall k a. Map k a
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 -> sign -> [Named sentence] -> NumberedSigMap symbol
fromSignAndNamedSens lid :: lid
lid sig :: sign
sig nsens :: [Named sentence]
nsens =
    let syms :: [symbol]
syms = lid -> sign -> [symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> [symbol]
symlist_of lid
lid sign
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 :: Map b b -> b -> (Map b b, (b, b))
newName acc :: Map b b
acc s :: b
s =
            let (v :: Maybe b
v, acc' :: Map b b
acc') = (b -> b -> b -> b) -> b -> b -> Map b b -> (Maybe b, Map b b)
forall k a.
Ord k =>
(k -> a -> a -> a) -> k -> a -> Map k a -> (Maybe a, Map k a)
Map.insertLookupWithKey ((b -> b -> b) -> b -> b -> b -> b
forall a b. a -> b -> a
const b -> b -> b
forall a. Num a => a -> a -> a
(+)) b
s 1 Map b b
acc
            in (Map b b
acc', (b
s, b -> Maybe b -> b
forall a. a -> Maybe a -> a
fromMaybe 0 Maybe b
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 :: (a, Map String b)
-> symbol -> ((a, Map String b), (symbol, (a, (String, b))))
symF (i :: a
i, acc :: Map String b
acc) x :: symbol
x = let (acc' :: Map String b
acc', nn :: (String, b)
nn) = Map String b -> String -> (Map String b, (String, b))
forall b b. (Ord b, Num b) => Map b b -> b -> (Map b b, (b, b))
newName Map String b
acc (String -> (Map String b, (String, b)))
-> String -> (Map String b, (String, b))
forall a b. (a -> b) -> a -> b
$ Id -> String
forall a. Show a => a -> String
show (Id -> String) -> Id -> String
forall a b. (a -> b) -> a -> b
$ lid -> symbol -> Id
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Id
sym_name lid
lid symbol
x
                          in ((a
i a -> a -> a
forall a. Num a => a -> a -> a
+ 1, Map String b
acc'), (symbol
x, (a
i, (String, b)
nn)))
        sensF :: Map a b -> SenAttr s a -> (Map a b, (a, (a, b)))
sensF acc :: Map a b
acc x :: SenAttr s a
x = let n :: a
n = SenAttr s a -> a
forall s a. SenAttr s a -> a
senAttr SenAttr s a
x
                          (acc' :: Map a b
acc', nn :: (a, b)
nn) = Map a b -> a -> (Map a b, (a, b))
forall b b. (Ord b, Num b) => Map b b -> b -> (Map b b, (b, b))
newName Map a b
acc a
n in (Map a b
acc', (a
n, (a, b)
nn))
        (cm :: (Int, Map String Int)
cm, symL :: [(symbol, (Int, UniqName))]
symL) = ((Int, Map String Int)
 -> symbol -> ((Int, Map String Int), (symbol, (Int, UniqName))))
-> (Int, Map String Int)
-> [symbol]
-> ((Int, Map String Int), [(symbol, (Int, UniqName))])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL (Int, Map String Int)
-> symbol -> ((Int, Map String Int), (symbol, (Int, UniqName)))
forall a b sentence sign morphism symbol.
(Num a, Num b, Sentences lid sentence sign morphism symbol) =>
(a, Map String b)
-> symbol -> ((a, Map String b), (symbol, (a, (String, b))))
symF (0, Map String Int
forall k a. Map k a
Map.empty) [symbol]
syms
        (_, sensL :: [(String, UniqName)]
sensL) = (Map String Int
 -> Named sentence -> (Map String Int, (String, UniqName)))
-> Map String Int
-> [Named sentence]
-> (Map String Int, [(String, UniqName)])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL Map String Int
-> Named sentence -> (Map String Int, (String, UniqName))
forall a b s.
(Ord a, Num b) =>
Map a b -> SenAttr s a -> (Map a b, (a, (a, b)))
sensF ((Int, Map String Int) -> Map String Int
forall a b. (a, b) -> b
snd (Int, Map String Int)
cm) [Named sentence]
nsens
    in ([(symbol, (Int, UniqName))] -> Map symbol (Int, UniqName)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(symbol, (Int, UniqName))]
symL, [(String, UniqName)] -> NameMap String
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(String, UniqName)]
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
-> sign
-> [Named sentence]
-> ExpEnv
-> (LibName, String)
-> (ExpEnv, NumberedSigMap symbol)
lookupWithInsert lid :: lid
lid sig :: sign
sig sens :: [Named sentence]
sens s :: ExpEnv
s k :: (LibName, String)
k =
    let SpecSymNames m :: Map (LibName, String) GSigMap
m = ExpEnv -> SpecSymNames
getSSN ExpEnv
s in
    case (LibName, String) -> Map (LibName, String) GSigMap -> Maybe GSigMap
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (LibName, String)
k Map (LibName, String) GSigMap
m of
      Just (GSigMap (G_symbolmap lid1 :: lid
lid1 sm :: Map symbol (Int, UniqName)
sm) nm :: NameMap String
nm) ->
          (ExpEnv
s, (lid
-> lid -> Map symbol (Int, UniqName) -> Map symbol (Int, UniqName)
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 a.
(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,
 Typeable a) =>
lid1 -> lid2 -> Map symbol1 a -> Map symbol2 a
coerceSymbolmap lid
lid1 lid
lid Map symbol (Int, UniqName)
sm, NameMap String
nm))
      Nothing -> let nsigm :: NumberedSigMap symbol
nsigm@(sm :: Map symbol (Int, UniqName)
sm, nm :: NameMap String
nm) = lid -> sign -> [Named sentence] -> NumberedSigMap symbol
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
lid sign
sig [Named sentence]
sens
                     gsm :: GSigMap
gsm = G_symbolmap (Int, UniqName) -> NameMap String -> GSigMap
GSigMap (lid -> Map symbol (Int, UniqName) -> G_symbolmap (Int, UniqName)
forall a 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 -> Map symbol a -> G_symbolmap a
G_symbolmap lid
lid Map symbol (Int, UniqName)
sm) NameMap String
nm
                 in ( ExpEnv
s { getSSN :: SpecSymNames
getSSN = Map (LibName, String) GSigMap -> SpecSymNames
SpecSymNames (Map (LibName, String) GSigMap -> SpecSymNames)
-> Map (LibName, String) GSigMap -> SpecSymNames
forall a b. (a -> b) -> a -> b
$ (LibName, String)
-> GSigMap
-> Map (LibName, String) GSigMap
-> Map (LibName, String) GSigMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (LibName, String)
k GSigMap
gsm Map (LibName, String) GSigMap
m }, NumberedSigMap symbol
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 :: Bool -> String -> LibName -> LibEnv -> Result [(LibName, OMDoc)]
exportLibEnv b :: Bool
b odir :: String
odir ln :: LibName
ln le :: LibEnv
le =
    let cmbnF :: (a, b) -> b -> (a, b)
cmbnF (x :: a
x, _) y :: b
y = (a
x, b
y)
        inputList :: [(LibName, DGraph)]
inputList = if Bool
b then LibEnv -> [(LibName, DGraph)]
forall k a. Map k a -> [(k, a)]
Map.toList LibEnv
le else [(LibName
ln, LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le)]
        fpm :: Map LibName String
fpm = String -> LibEnv -> Map LibName String
initFilePathMapping String
odir LibEnv
le
        im :: ExpEnv
im = (LibName -> ExpEnv
emptyEnv LibName
ln) { getFilePathMapping :: Map LibName String
getFilePathMapping = Map LibName String
fpm }
        f :: (LibName, b) -> (LibName, b)
f (ln' :: LibName
ln', o :: b
o) = let fp :: String
fp = String -> LibName -> Map LibName String -> String
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
                              (String -> String
forall a. HasCallStack => String -> a
error "exportLibEnv: filepath not mapped")
                              LibName
ln' Map LibName String
fpm
                     in (String -> LibName -> LibName
setFilePath String
fp LibName
ln', b
o)
    in do
      [(LibName, OMDoc)]
l <- ((ExpEnv, [(LibName, OMDoc)]) -> [(LibName, OMDoc)])
-> Result (ExpEnv, [(LibName, OMDoc)]) -> Result [(LibName, OMDoc)]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (ExpEnv, [(LibName, OMDoc)]) -> [(LibName, OMDoc)]
forall a b. (a, b) -> b
snd (Result (ExpEnv, [(LibName, OMDoc)]) -> Result [(LibName, OMDoc)])
-> Result (ExpEnv, [(LibName, OMDoc)]) -> Result [(LibName, OMDoc)]
forall a b. (a -> b) -> a -> b
$ ((LibName, DGraph) -> OMDoc -> (LibName, OMDoc))
-> (ExpEnv -> (LibName, DGraph) -> Result (ExpEnv, OMDoc))
-> ExpEnv
-> [(LibName, DGraph)]
-> Result (ExpEnv, [(LibName, OMDoc)])
forall (m :: * -> *) a b c acc.
Monad m =>
(a -> b -> c)
-> (acc -> a -> m (acc, b)) -> acc -> [a] -> m (acc, [c])
mapAccumLCM (LibName, DGraph) -> OMDoc -> (LibName, OMDoc)
forall a b b. (a, b) -> b -> (a, b)
cmbnF (LibEnv -> ExpEnv -> (LibName, DGraph) -> Result (ExpEnv, OMDoc)
exportDGraph LibEnv
le) ExpEnv
im [(LibName, DGraph)]
inputList
      [(LibName, OMDoc)] -> Result [(LibName, OMDoc)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(LibName, OMDoc)] -> Result [(LibName, OMDoc)])
-> [(LibName, OMDoc)] -> Result [(LibName, OMDoc)]
forall a b. (a -> b) -> a -> b
$ ((LibName, OMDoc) -> (LibName, OMDoc))
-> [(LibName, OMDoc)] -> [(LibName, OMDoc)]
forall a b. (a -> b) -> [a] -> [b]
map (LibName, OMDoc) -> (LibName, OMDoc)
forall b. (LibName, b) -> (LibName, b)
f [(LibName, OMDoc)]
l

initFilePathMapping :: FilePath -> LibEnv -> Map.Map LibName FilePath
initFilePathMapping :: String -> LibEnv -> Map LibName String
initFilePathMapping fp :: String
fp le :: LibEnv
le =
    let f :: LibName -> p -> String
f k :: LibName
k _ = (String, String) -> String
forall a b. (a, b) -> b
snd ([String] -> String -> String -> (String, String)
getFilePrefixGeneric [String]
downloadExtensions String
fp
                         (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ LibName -> String
getFilePath LibName
k) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".omdoc"
    in (LibName -> DGraph -> String) -> LibEnv -> Map LibName String
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey LibName -> DGraph -> String
forall p. LibName -> p -> String
f LibEnv
le

-- | DGraph to OMDoc translation
exportDGraph :: LibEnv -> ExpEnv -> (LibName, DGraph) -> Result (ExpEnv, OMDoc)
exportDGraph :: LibEnv -> ExpEnv -> (LibName, DGraph) -> Result (ExpEnv, OMDoc)
exportDGraph le :: LibEnv
le s :: ExpEnv
s (ln :: LibName
ln, dg :: DGraph
dg) = do
  (s' :: ExpEnv
s', theories :: [Maybe TLElement]
theories) <- (ExpEnv -> LNode DGNodeLab -> Result (ExpEnv, Maybe TLElement))
-> ExpEnv
-> [LNode DGNodeLab]
-> Result (ExpEnv, [Maybe TLElement])
forall (m :: * -> *) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
mapAccumLM (LibEnv
-> LibName
-> DGraph
-> ExpEnv
-> LNode DGNodeLab
-> Result (ExpEnv, Maybe TLElement)
exportNodeLab LibEnv
le LibName
ln DGraph
dg) ExpEnv
s
                    ([LNode DGNodeLab] -> Result (ExpEnv, [Maybe TLElement]))
-> [LNode DGNodeLab] -> Result (ExpEnv, [Maybe TLElement])
forall a b. (a -> b) -> a -> b
$ DGraph -> [LNode DGNodeLab]
topsortedNodes DGraph
dg
  (s'' :: ExpEnv
s'', views :: [Maybe TLElement]
views) <- (ExpEnv -> LEdge DGLinkLab -> Result (ExpEnv, Maybe TLElement))
-> ExpEnv
-> [LEdge DGLinkLab]
-> Result (ExpEnv, [Maybe TLElement])
forall (m :: * -> *) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
mapAccumLM (LibEnv
-> LibName
-> DGraph
-> ExpEnv
-> LEdge DGLinkLab
-> Result (ExpEnv, Maybe TLElement)
exportLinkLab LibEnv
le LibName
ln DGraph
dg) ExpEnv
s' ([LEdge DGLinkLab] -> Result (ExpEnv, [Maybe TLElement]))
-> [LEdge DGLinkLab] -> Result (ExpEnv, [Maybe TLElement])
forall a b. (a -> b) -> a -> b
$ DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dg
  (ExpEnv, OMDoc) -> Result (ExpEnv, OMDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExpEnv
s'', String -> [TLElement] -> OMDoc
OMDoc (IRI -> String
forall a. Show a => a -> String
show (IRI -> String) -> IRI -> String
forall a b. (a -> b) -> a -> b
$ LibName -> IRI
getLibId LibName
ln)
                 ([TLElement] -> OMDoc) -> [TLElement] -> OMDoc
forall a b. (a -> b) -> a -> b
$ [Maybe TLElement] -> [TLElement]
forall a. [Maybe a] -> [a]
catMaybes [Maybe TLElement]
theories [TLElement] -> [TLElement] -> [TLElement]
forall a. [a] -> [a] -> [a]
++ [Maybe TLElement] -> [TLElement]
forall a. [Maybe a] -> [a]
catMaybes [Maybe TLElement]
views)


-- | DGNodeLab to TLTheory translation
exportNodeLab :: LibEnv -> LibName -> DGraph -> ExpEnv -> LNode DGNodeLab
              -> Result (ExpEnv, Maybe TLElement)
exportNodeLab :: LibEnv
-> LibName
-> DGraph
-> ExpEnv
-> LNode DGNodeLab
-> Result (ExpEnv, Maybe TLElement)
exportNodeLab le :: LibEnv
le ln :: LibName
ln dg :: DGraph
dg s :: ExpEnv
s (n :: Int
n, lb :: DGNodeLab
lb) =
  if DGNodeLab -> Bool
isDGRef DGNodeLab
lb then (ExpEnv, Maybe TLElement) -> Result (ExpEnv, Maybe TLElement)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExpEnv
s, Maybe TLElement
forall a. Maybe a
Nothing) else
      let (lb' :: DGNodeLab
lb', ln' :: LibName
ln') = LibEnv -> LibName -> DGNodeLab -> (DGNodeLab, LibName)
getNodeData LibEnv
le LibName
ln DGNodeLab
lb in
      case DGNodeLab -> G_theory
dgn_theory DGNodeLab
lb' of
        G_theory lid :: lid
lid _ (ExtSign sig :: sign
sig _) _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _ ->
            do
              let sn :: String
sn = DGNodeLab -> String
getDGNodeName DGNodeLab
lb'
                  nsens :: [Named sentence]
nsens = ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sens
                  (s' :: ExpEnv
s', nsigm :: NumberedSigMap symbol
nsigm) = lid
-> sign
-> [Named sentence]
-> ExpEnv
-> (LibName, String)
-> (ExpEnv, NumberedSigMap symbol)
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
lid sign
sig [Named sentence]
nsens ExpEnv
s (LibName
ln', String
sn)
                  sigm :: SigMap symbol
sigm@(SigMap nm :: NameMap symbol
nm _) = NumberedSigMap symbol -> SigMap symbol
forall a. NumberedSigMap a -> SigMap a
nSigMapToSigMap NumberedSigMap symbol
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'' :: ExpEnv
s'', imports :: [Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol)]
imports) <-
                  (ExpEnv
 -> LEdge DGLinkLab
 -> Result
      (ExpEnv, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol)))
-> ExpEnv
-> [LEdge DGLinkLab]
-> Result
     (ExpEnv,
      [Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol)])
forall (m :: * -> *) acc x y.
Monad m =>
(acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, [y])
mapAccumLM (LibEnv
-> LibName
-> DGraph
-> (lid, NameMap symbol)
-> ExpEnv
-> LEdge DGLinkLab
-> Result
     (ExpEnv, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol))
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, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol))
makeImportMapping LibEnv
le LibName
ln DGraph
dg (lid
lid, NameMap symbol
nm)) ExpEnv
s'
                                 ([LEdge DGLinkLab]
 -> Result
      (ExpEnv,
       [Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol)]))
-> [LEdge DGLinkLab]
-> Result
     (ExpEnv,
      [Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol)])
forall a b. (a -> b) -> a -> b
$ DGraph -> Int -> [LEdge DGLinkLab]
innDG DGraph
dg Int
n

              {- mappingL: list of the triples described above
              symsetL: used to compute the local symbols (not imported) -}
              let (mappingL :: [(String, OMCD, [(OMName, UniqName)])]
mappingL, symsetL :: [Set symbol]
symsetL) = [((String, OMCD, [(OMName, UniqName)]), Set symbol)]
-> ([(String, OMCD, [(OMName, UniqName)])], [Set symbol])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((String, OMCD, [(OMName, UniqName)]), Set symbol)]
 -> ([(String, OMCD, [(OMName, UniqName)])], [Set symbol]))
-> [((String, OMCD, [(OMName, UniqName)]), Set symbol)]
-> ([(String, OMCD, [(OMName, UniqName)])], [Set symbol])
forall a b. (a -> b) -> a -> b
$ [Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol)]
-> [((String, OMCD, [(OMName, UniqName)]), Set symbol)]
forall a. [Maybe a] -> [a]
catMaybes [Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol)]
imports
                  (_, importL :: [TCElement]
importL) = (Set UniqName
 -> (String, OMCD, [(OMName, UniqName)])
 -> (Set UniqName, TCElement))
-> Set UniqName
-> [(String, OMCD, [(OMName, UniqName)])]
-> (Set UniqName, [TCElement])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL Set UniqName
-> (String, OMCD, [(OMName, UniqName)])
-> (Set UniqName, TCElement)
makeImport Set UniqName
forall a. Set a
Set.empty [(String, OMCD, [(OMName, UniqName)])]
mappingL
                  mSynTbl :: Maybe SyntaxTable
mSynTbl = lid -> sign -> Maybe SyntaxTable
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 -> Maybe SyntaxTable
syntaxTable lid
lid sign
sig
              [TCElement]
extra <- lid
-> SigMap symbol -> sign -> [Named sentence] -> Result [TCElement]
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 -> sign -> [Named sentence] -> Result [TCElement]
export_theoryToOmdoc lid
lid SigMap symbol
sigm sign
sig [Named sentence]
nsens
              [[TCElement]]
consts <- ((symbol, UniqName) -> Result [TCElement])
-> [(symbol, UniqName)] -> Result [[TCElement]]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR ((symbol -> UniqName -> Result [TCElement])
-> (symbol, UniqName) -> Result [TCElement]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((symbol -> UniqName -> Result [TCElement])
 -> (symbol, UniqName) -> Result [TCElement])
-> (symbol -> UniqName -> Result [TCElement])
-> (symbol, UniqName)
-> Result [TCElement]
forall a b. (a -> b) -> a -> b
$ lid
-> SigMap symbol
-> Maybe SyntaxTable
-> [Set symbol]
-> symbol
-> UniqName
-> Result [TCElement]
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 symbol]
-> symbol
-> UniqName
-> Result [TCElement]
exportSymbol lid
lid SigMap symbol
sigm Maybe SyntaxTable
mSynTbl [Set symbol]
symsetL)
                        ([(symbol, UniqName)] -> Result [[TCElement]])
-> [(symbol, UniqName)] -> Result [[TCElement]]
forall a b. (a -> b) -> a -> b
$ NumberedSigMap symbol -> [(symbol, UniqName)]
forall a. NumberedSigMap a -> [(a, UniqName)]
nSigMapToOrderedList NumberedSigMap symbol
nsigm
              -- create the OMDoc elements for the sentences
              [[TCElement]]
thms <- (Named sentence -> Result [TCElement])
-> [Named sentence] -> Result [[TCElement]]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (lid -> SigMap symbol -> Named sentence -> Result [TCElement]
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
lid SigMap symbol
sigm) [Named sentence]
nsens
              (ExpEnv, Maybe TLElement) -> Result (ExpEnv, Maybe TLElement)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExpEnv
s'', TLElement -> Maybe TLElement
forall a. a -> Maybe a
Just (TLElement -> Maybe TLElement) -> TLElement -> Maybe TLElement
forall a b. (a -> b) -> a -> b
$ String -> Maybe OMCD -> [TCElement] -> TLElement
TLTheory String
sn (lid -> Maybe OMCD
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 -> Maybe OMCD
omdoc_metatheory lid
lid)
                             ([TCElement] -> TLElement) -> [TCElement] -> TLElement
forall a b. (a -> b) -> a -> b
$ [[TCElement]] -> [TCElement]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
                                   [[TCElement]
importL, [[TCElement]] -> [TCElement]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[TCElement]]
consts, [TCElement]
extra, [[TCElement]] -> [TCElement]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[TCElement]]
thms])


-- * Views and Morphisms

-- Node lookup for handling ref nodes
getNodeData :: LibEnv -> LibName -> DGNodeLab -> (DGNodeLab, LibName)
getNodeData :: LibEnv -> LibName -> DGNodeLab -> (DGNodeLab, LibName)
getNodeData le :: LibEnv
le ln :: LibName
ln lb :: DGNodeLab
lb =
    if DGNodeLab -> Bool
isDGRef DGNodeLab
lb then
        let ni :: DGNodeInfo
ni = DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
lb
            lnRef :: LibName
lnRef = DGNodeInfo -> LibName
ref_libname DGNodeInfo
ni
            dg' :: DGraph
dg' = DGraph -> LibName -> LibEnv -> DGraph
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
                  (String -> DGraph
forall a. HasCallStack => String -> a
error (String -> DGraph) -> String -> DGraph
forall a b. (a -> b) -> a -> b
$ "getNodeData: Lib not found: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LibName -> String
forall a. Show a => a -> String
show LibName
lnRef)
                  LibName
lnRef LibEnv
le
        in (DGraph -> Int -> DGNodeLab
labDG DGraph
dg' (Int -> DGNodeLab) -> Int -> DGNodeLab
forall a b. (a -> b) -> a -> b
$ DGNodeInfo -> Int
ref_node DGNodeInfo
ni, LibName
lnRef)
    else (DGNodeLab
lb, LibName
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 :: Set UniqName
-> (String, OMCD, [(OMName, UniqName)])
-> (Set UniqName, TCElement)
makeImport s :: Set UniqName
s (n :: String
n, cd :: OMCD
cd, mapping :: [(OMName, UniqName)]
mapping) =
    let f :: Set UniqName
-> (OMName, UniqName) -> (Set UniqName, (OMName, OMImage))
f s' :: Set UniqName
s' p :: (OMName, UniqName)
p@(_, un :: UniqName
un)
            | UniqName -> Set UniqName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember UniqName
un Set UniqName
s' =
                (UniqName -> Set UniqName -> Set UniqName
forall a. Ord a => a -> Set a -> Set a
Set.insert UniqName
un Set UniqName
s', Bool -> (OMName, UniqName) -> (OMName, OMImage)
makeMorphismEntry Bool
True (OMName, UniqName)
p)
            | Bool
otherwise = (Set UniqName
s', Bool -> (OMName, UniqName) -> (OMName, OMImage)
makeMorphismEntry Bool
False (OMName, UniqName)
p)
        (s'' :: Set UniqName
s'', morph :: [(OMName, OMImage)]
morph) = (Set UniqName
 -> (OMName, UniqName) -> (Set UniqName, (OMName, OMImage)))
-> Set UniqName
-> [(OMName, UniqName)]
-> (Set UniqName, [(OMName, OMImage)])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL Set UniqName
-> (OMName, UniqName) -> (Set UniqName, (OMName, OMImage))
f Set UniqName
s [(OMName, UniqName)]
mapping
    in (Set UniqName
s'', String -> OMCD -> [(OMName, OMImage)] -> TCElement
TCImport String
n OMCD
cd [(OMName, OMImage)]
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 :: LibEnv
-> LibName
-> DGraph
-> (lid, NameMap symbol)
-> ExpEnv
-> LEdge DGLinkLab
-> Result
     (ExpEnv, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol))
makeImportMapping le :: LibEnv
le ln :: LibName
ln dg :: DGraph
dg toInfo :: (lid, NameMap symbol)
toInfo s :: ExpEnv
s (from :: Int
from, _, lbl :: DGLinkLab
lbl)
    | DGLinkType -> Bool
isHidingEdge (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lbl =
        () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
warning () ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ "Hiding link id ", EdgeId -> String
showEdgeId (DGLinkLab -> EdgeId
dgl_id DGLinkLab
lbl)
                           , " not exported."]) Range
nullRange
                    Result ()
-> Result
     (ExpEnv, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol))
-> Result
     (ExpEnv, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol))
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (ExpEnv, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol))
-> Result
     (ExpEnv, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol))
forall (m :: * -> *) a. Monad m => a -> m a
return (ExpEnv
s, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol)
forall a. Maybe a
Nothing)
    | DGLinkType -> Bool
isLocalDef (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lbl =
        () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
warning () ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ "Local def-link id ", EdgeId -> String
showEdgeId (DGLinkLab -> EdgeId
dgl_id DGLinkLab
lbl)
                           , " not exported."]) Range
nullRange
                    Result ()
-> Result
     (ExpEnv, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol))
-> Result
     (ExpEnv, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol))
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (ExpEnv, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol))
-> Result
     (ExpEnv, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol))
forall (m :: * -> *) a. Monad m => a -> m a
return (ExpEnv
s, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol)
forall a. Maybe a
Nothing)
    | DGLinkType -> Bool
isGlobalDef (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lbl =
        let (lb' :: DGNodeLab
lb', ln' :: LibName
ln') = LibEnv -> LibName -> DGNodeLab -> (DGNodeLab, LibName)
getNodeData LibEnv
le LibName
ln (DGNodeLab -> (DGNodeLab, LibName))
-> DGNodeLab -> (DGNodeLab, LibName)
forall a b. (a -> b) -> a -> b
$ DGraph -> Int -> DGNodeLab
labDG DGraph
dg Int
from
            edgName :: String
edgName = DGLinkLab -> String
dglName DGLinkLab
lbl
            impname :: String
impname = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
edgName
                      then "gn_imp_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ EdgeId -> String
showEdgeId (DGLinkLab -> EdgeId
dgl_id DGLinkLab
lbl)
                      else String
edgName
        in
         case DGNodeLab -> G_theory
dgn_theory DGNodeLab
lb' of
          G_theory lid :: lid
lid _ (ExtSign sig :: sign
sig _) _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _ ->
              do
                let sn :: String
sn = DGNodeLab -> String
getDGNodeName DGNodeLab
lb'
                    nsens :: [Named sentence]
nsens = ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sens
                    (s' :: ExpEnv
s', nsigm :: NumberedSigMap symbol
nsigm) = lid
-> sign
-> [Named sentence]
-> ExpEnv
-> (LibName, String)
-> (ExpEnv, NumberedSigMap symbol)
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
lid sign
sig [Named sentence]
nsens ExpEnv
s (LibName
ln', String
sn)
                    SigMap nm :: NameMap symbol
nm _ = NumberedSigMap symbol -> SigMap symbol
forall a. NumberedSigMap a -> SigMap a
nSigMapToSigMap NumberedSigMap symbol
nsigm
                (morph :: [(OMName, UniqName)]
morph, expSymbs :: Set symbol
expSymbs) <-
                    (lid, NameMap symbol)
-> (lid, NameMap symbol)
-> GMorphism
-> Result ([(OMName, UniqName)], Set symbol)
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 symbol2)
makeMorphism (lid
lid, NameMap symbol
nm) (lid, NameMap symbol)
toInfo (GMorphism -> Result ([(OMName, UniqName)], Set symbol))
-> GMorphism -> Result ([(OMName, UniqName)], Set symbol)
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
lbl
                OMCD
cd <- ExpEnv -> LibName -> LibName -> String -> Result OMCD
mkCD ExpEnv
s' LibName
ln LibName
ln' String
sn
                (ExpEnv, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol))
-> Result
     (ExpEnv, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol))
forall (m :: * -> *) a. Monad m => a -> m a
return (ExpEnv
s', ((String, OMCD, [(OMName, UniqName)]), Set symbol)
-> Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol)
forall a. a -> Maybe a
Just ((String
impname, OMCD
cd, [(OMName, UniqName)]
morph), Set symbol
expSymbs))
    | Bool
otherwise = (ExpEnv, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol))
-> Result
     (ExpEnv, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol))
forall (m :: * -> *) a. Monad m => a -> m a
return (ExpEnv
s, Maybe ((String, OMCD, [(OMName, UniqName)]), Set symbol)
forall a. Maybe a
Nothing)

-- | Given a TheoremLink we output the view
exportLinkLab :: LibEnv -> LibName -> DGraph -> ExpEnv -> LEdge DGLinkLab
              -> Result (ExpEnv, Maybe TLElement)
exportLinkLab :: LibEnv
-> LibName
-> DGraph
-> ExpEnv
-> LEdge DGLinkLab
-> Result (ExpEnv, Maybe TLElement)
exportLinkLab le :: LibEnv
le ln :: LibName
ln dg :: DGraph
dg s :: ExpEnv
s (from :: Int
from, to :: Int
to, lbl :: DGLinkLab
lbl) =
    let ltyp :: DGLinkType
ltyp = DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lbl
        gmorph :: GMorphism
gmorph = DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
lbl
        edgName :: String
edgName = DGLinkLab -> String
dglName DGLinkLab
lbl
        viewname :: String
viewname = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
edgName
                   then "gn_vn_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ EdgeId -> String
showEdgeId (DGLinkLab -> EdgeId
dgl_id DGLinkLab
lbl)
                   else String
edgName
        (lb1 :: DGNodeLab
lb1, ln1 :: LibName
ln1) = LibEnv -> LibName -> DGNodeLab -> (DGNodeLab, LibName)
getNodeData LibEnv
le LibName
ln (DGNodeLab -> (DGNodeLab, LibName))
-> DGNodeLab -> (DGNodeLab, LibName)
forall a b. (a -> b) -> a -> b
$ DGraph -> Int -> DGNodeLab
labDG DGraph
dg Int
from
        (lb2 :: DGNodeLab
lb2, ln2 :: LibName
ln2) = LibEnv -> LibName -> DGNodeLab -> (DGNodeLab, LibName)
getNodeData LibEnv
le LibName
ln (DGNodeLab -> (DGNodeLab, LibName))
-> DGNodeLab -> (DGNodeLab, LibName)
forall a b. (a -> b) -> a -> b
$ DGraph -> Int -> DGNodeLab
labDG DGraph
dg Int
to
        noExport :: Result (ExpEnv, Maybe a)
noExport = (ExpEnv, Maybe a) -> Result (ExpEnv, Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExpEnv
s, Maybe a
forall a. Maybe a
Nothing)
        withWarning :: String -> Result (ExpEnv, Maybe a)
withWarning lt :: String
lt = () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
warning () ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ "exportLinkLab: ", String
lt
                                           , " link with ", EdgeId -> String
forall a. Show a => a -> String
show (DGLinkLab -> EdgeId
dgl_id DGLinkLab
lbl)
                                           , " not exported."])
                        Range
nullRange Result () -> Result (ExpEnv, Maybe a) -> Result (ExpEnv, Maybe a)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Result (ExpEnv, Maybe a)
forall a. Result (ExpEnv, Maybe a)
noExport
    in case (DGLinkType -> Bool
isDefEdge DGLinkType
ltyp, DGLinkType -> Bool
isLocalEdge DGLinkType
ltyp, DGLinkType -> Bool
isHidingEdge DGLinkType
ltyp) of
         (True, _, _) -> Result (ExpEnv, Maybe TLElement)
forall a. Result (ExpEnv, Maybe a)
noExport
         (_, True, _) -> String -> Result (ExpEnv, Maybe TLElement)
forall a. String -> Result (ExpEnv, Maybe a)
withWarning "Local"
         (_, _, True) -> String -> Result (ExpEnv, Maybe TLElement)
forall a. String -> Result (ExpEnv, Maybe a)
withWarning "Hiding"
         _ ->
             case (DGNodeLab -> G_theory
dgn_theory DGNodeLab
lb1, DGNodeLab -> G_theory
dgn_theory DGNodeLab
lb2) of
               { (G_theory lid1 :: lid
lid1 _ (ExtSign sig1 :: sign
sig1 _) _ sens1 :: ThSens sentence (AnyComorphism, BasicProof)
sens1 _ ,
                  G_theory lid2 :: lid
lid2 _ (ExtSign sig2 :: sign
sig2 _) _ sens2 :: ThSens sentence (AnyComorphism, BasicProof)
sens2 _ ) ->
                 do
                   let sn1 :: String
sn1 = DGNodeLab -> String
getDGNodeName DGNodeLab
lb1
                       sn2 :: String
sn2 = DGNodeLab -> String
getDGNodeName DGNodeLab
lb2
                       nsens1 :: [Named sentence]
nsens1 = ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sens1
                       nsens2 :: [Named sentence]
nsens2 = ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sens2
                       (s' :: ExpEnv
s', nsigm1 :: NumberedSigMap symbol
nsigm1) =
                           lid
-> sign
-> [Named sentence]
-> ExpEnv
-> (LibName, String)
-> (ExpEnv, NumberedSigMap symbol)
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
lid1 sign
sig1 [Named sentence]
nsens1 ExpEnv
s (LibName
ln1, String
sn1)
                       (s'' :: ExpEnv
s'', nsigm2 :: NumberedSigMap symbol
nsigm2) =
                           lid
-> sign
-> [Named sentence]
-> ExpEnv
-> (LibName, String)
-> (ExpEnv, NumberedSigMap symbol)
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
lid2 sign
sig2 [Named sentence]
nsens2 ExpEnv
s' (LibName
ln2, String
sn2)
                       SigMap nm1 :: NameMap symbol
nm1 _ = NumberedSigMap symbol -> SigMap symbol
forall a. NumberedSigMap a -> SigMap a
nSigMapToSigMap NumberedSigMap symbol
nsigm1
                       SigMap nm2 :: NameMap symbol
nm2 _ = NumberedSigMap symbol -> SigMap symbol
forall a. NumberedSigMap a -> SigMap a
nSigMapToSigMap NumberedSigMap symbol
nsigm2
                   (preMorph :: [(OMName, UniqName)]
preMorph, _) <-
                       (lid, NameMap symbol)
-> (lid, NameMap symbol)
-> GMorphism
-> Result ([(OMName, UniqName)], Set symbol)
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 symbol2)
makeMorphism (lid
lid1, NameMap symbol
nm1) (lid
lid2, NameMap symbol
nm2) GMorphism
gmorph
                   let morph :: [(OMName, OMImage)]
morph = ((OMName, UniqName) -> (OMName, OMImage))
-> [(OMName, UniqName)] -> [(OMName, OMImage)]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> (OMName, UniqName) -> (OMName, OMImage)
makeMorphismEntry Bool
False) [(OMName, UniqName)]
preMorph
                   OMCD
cd1 <- ExpEnv -> LibName -> LibName -> String -> Result OMCD
mkCD ExpEnv
s'' LibName
ln LibName
ln1 String
sn1
                   OMCD
cd2 <- ExpEnv -> LibName -> LibName -> String -> Result OMCD
mkCD ExpEnv
s'' LibName
ln LibName
ln2 String
sn2
                   (ExpEnv, Maybe TLElement) -> Result (ExpEnv, Maybe TLElement)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExpEnv
s'', TLElement -> Maybe TLElement
forall a. a -> Maybe a
Just (TLElement -> Maybe TLElement) -> TLElement -> Maybe TLElement
forall a b. (a -> b) -> a -> b
$ String -> OMCD -> OMCD -> [(OMName, OMImage)] -> TLElement
TLView String
viewname OMCD
cd1 OMCD
cd2 [(OMName, OMImage)]
morph) }


makeMorphismEntry :: Bool -> (OMName, UniqName)
                -> (OMName, OMImage)
makeMorphismEntry :: Bool -> (OMName, UniqName) -> (OMName, OMImage)
makeMorphismEntry useOpen :: Bool
useOpen (n :: OMName
n, un :: UniqName
un) =
    (OMName
n, if Bool
useOpen then String -> OMImage
forall a b. a -> Either a b
Left (String -> OMImage) -> String -> OMImage
forall a b. (a -> b) -> a -> b
$ UniqName -> String
nameToString UniqName
un else OMElement -> OMImage
forall a b. b -> Either a b
Right (OMElement -> OMImage) -> OMElement -> OMImage
forall a b. (a -> b) -> a -> b
$ UniqName -> OMElement
simpleOMS UniqName
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 :: (lid1, NameMap symbol1)
-> (lid2, NameMap symbol2)
-> GMorphism
-> Result ([(OMName, UniqName)], Set symbol2)
makeMorphism (l1 :: lid1
l1, symM1 :: NameMap symbol1
symM1) (l2 :: lid2
l2, symM2 :: NameMap symbol2
symM2)
                 (GMorphism cid :: cid
cid (ExtSign sig :: sign1
sig _) _ mor :: morphism2
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 :: lid1
lS = cid -> lid1
forall cid 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.
Comorphism
  cid
  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 =>
cid -> lid1
sourceLogic cid
cid
          lT :: lid2
lT = cid -> lid2
forall cid 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.
Comorphism
  cid
  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 =>
cid -> lid2
targetLogic cid
cid
          f :: symbol1 -> symbol2
f = if AnyComorphism -> Bool
isIdComorphism (cid -> AnyComorphism
forall cid 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.
Comorphism
  cid
  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 =>
cid -> AnyComorphism
Comorphism cid
cid)
              then lid1 -> lid2 -> symbol1 -> symbol2
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 -> lid2 -> symbol1 -> symbol2
coerceSymbol lid1
l1 lid2
lT
              else String -> Set symbol2 -> symbol2
forall a. String -> Set a -> a
sglElem (cid -> String
forall a. Show a => a -> String
show cid
cid) (Set symbol2 -> symbol2)
-> (symbol1 -> Set symbol2) -> symbol1 -> symbol2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. cid -> sign1 -> symbol1 -> Set symbol2
forall cid 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.
Comorphism
  cid
  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 =>
cid -> sign1 -> symbol1 -> Set symbol2
map_symbol cid
cid sign1
sig (symbol1 -> Set symbol2)
-> (symbol1 -> symbol1) -> symbol1 -> Set symbol2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. lid1 -> lid1 -> symbol1 -> symbol1
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 -> lid2 -> symbol1 -> symbol2
coerceSymbol lid1
l1 lid1
lS
          symM1' :: NameMap symbol2
symM1' = (symbol1 -> symbol2) -> NameMap symbol1 -> NameMap symbol2
forall a b. (Ord a, Ord b) => (a -> b) -> NameMap a -> NameMap b
fmapNM symbol1 -> symbol2
f NameMap symbol1
symM1
          symM2' :: NameMap symbol2
symM2' = (symbol2 -> symbol2) -> NameMap symbol2 -> NameMap symbol2
forall a b. (Ord a, Ord b) => (a -> b) -> NameMap a -> NameMap b
fmapNM (lid2 -> lid2 -> symbol2 -> symbol2
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 -> lid2 -> symbol1 -> symbol2
coerceSymbol lid2
l2 lid2
lT) NameMap symbol2
symM2
          mormap :: EndoMap symbol2
mormap = lid2 -> morphism2 -> EndoMap symbol2
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> morphism -> EndoMap symbol
symmap_of lid2
lT morphism2
mor
          expSymbs :: Set symbol2
expSymbs = [symbol2] -> Set symbol2
forall a. Ord a => [a] -> Set a
Set.fromList ([symbol2] -> Set symbol2) -> [symbol2] -> Set symbol2
forall a b. (a -> b) -> a -> b
$ Map symbol2 symbol2 -> [symbol2]
forall k a. Map k a -> [a]
Map.elems (Map symbol2 symbol2 -> [symbol2])
-> Map symbol2 symbol2 -> [symbol2]
forall a b. (a -> b) -> a -> b
$ lid2 -> lid2 -> EndoMap symbol2 -> Map symbol2 symbol2
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 a.
(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,
 Typeable a) =>
lid1 -> lid2 -> Map a symbol1 -> Map a symbol2
coerceMapofsymbol lid2
lT lid2
l2 EndoMap symbol2
mormap
      in ([(OMName, UniqName)], Set symbol2)
-> Result ([(OMName, UniqName)], Set symbol2)
forall (m :: * -> *) a. Monad m => a -> m a
return (((symbol2, symbol2) -> (OMName, UniqName))
-> [(symbol2, symbol2)] -> [(OMName, UniqName)]
forall a b. (a -> b) -> [a] -> [b]
map (lid2
-> NameMap symbol2
-> NameMap symbol2
-> (symbol2, symbol2)
-> (OMName, UniqName)
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 lid2
lT NameMap symbol2
symM1' NameMap symbol2
symM2')
                         ([(symbol2, symbol2)] -> [(OMName, UniqName)])
-> [(symbol2, symbol2)] -> [(OMName, UniqName)]
forall a b. (a -> b) -> a -> b
$ EndoMap symbol2 -> [(symbol2, symbol2)]
forall k a. Map k a -> [(k, a)]
Map.toList EndoMap symbol2
mormap, Set symbol2
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 :: lid
-> NameMap symbol
-> NameMap symbol
-> (symbol, symbol)
-> (OMName, UniqName)
mapEntry _ m1 :: NameMap symbol
m1 m2 :: NameMap symbol
m2 (s1 :: symbol
s1, s2 :: symbol
s2) =
    let e :: a
e = String -> a
forall a. HasCallStack => String -> a
error "mapEntry: symbolmapping is missing"
        un1 :: UniqName
un1 = UniqName -> symbol -> NameMap symbol -> UniqName
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault UniqName
forall a. a
e symbol
s1 NameMap symbol
m1
        un2 :: UniqName
un2 = UniqName -> symbol -> NameMap symbol -> UniqName
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault UniqName
forall a. a
e symbol
s2 NameMap symbol
m2
    in (UniqName -> OMName
omName UniqName
un1, UniqName
un2)


-- | extracts the single element from singleton sets, fails otherwise
sglElem :: String -> Set.Set a -> a
sglElem :: String -> Set a -> a
sglElem s :: String
s sa :: Set a
sa
    | Set a -> Int
forall a. Set a -> Int
Set.size Set a
sa Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 =
        String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ "OMDocExport: comorphism symbol image > 1 in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
    | Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
sa =
        String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ "OMDocExport: empty comorphism symbol image in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
    | Bool
otherwise = Set a -> a
forall a. Set a -> a
Set.findMin Set a
sa


-- * Names and CDs
mkCD :: ExpEnv -> LibName -> LibName -> String -> Result OMCD
mkCD :: ExpEnv -> LibName -> LibName -> String -> Result OMCD
mkCD s :: ExpEnv
s lnCurr :: LibName
lnCurr ln :: LibName
ln sn :: String
sn =
    let m :: Map LibName String
m = ExpEnv -> Map LibName String
getFilePathMapping ExpEnv
s
        fp :: String
fp = String -> LibName -> Map LibName String -> String
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
             (String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "mkCD: no entry for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LibName -> String
forall a. Show a => a -> String
show LibName
ln) LibName
ln Map LibName String
m
        fpCurr :: String
fpCurr = String -> LibName -> Map LibName String -> String
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
                 (String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "mkCD: no current entry for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LibName -> String
forall a. Show a => a -> String
show LibName
lnCurr) LibName
lnCurr Map LibName String
m
        -- compute the relative path
        fpRel :: String
fpRel = String -> String -> String
makeRelativeDesc (String -> String
takeDirectory String
fpCurr) String
fp
        fpRel' :: String
fpRel' = if String -> Bool
isAbsolute String
fpRel then "file://" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fpRel else String
fpRel
        base :: [String]
base = if LibName
lnCurr LibName -> LibName -> Bool
forall a. Eq a => a -> a -> Bool
== LibName
ln then [] else [String
fpRel']
    in OMCD -> Result OMCD
forall (m :: * -> *) a. Monad m => a -> m a
return (OMCD -> Result OMCD) -> OMCD -> Result OMCD
forall a b. (a -> b) -> a -> b
$ [String] -> OMCD
CD ([String] -> OMCD) -> [String] -> OMCD
forall a b. (a -> b) -> a -> b
$ String
sn String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
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 symbol
-> Maybe SyntaxTable
-> [Set symbol]
-> symbol
-> UniqName
-> Result [TCElement]
exportSymbol lid :: lid
lid (SigMap sm :: NameMap symbol
sm _) mSynTbl :: Maybe SyntaxTable
mSynTbl sl :: [Set symbol]
sl sym :: symbol
sym n :: UniqName
n =
    let symNotation :: [TCElement]
symNotation = UniqName -> Maybe (Id, SyntaxTable) -> [TCElement]
mkNotation UniqName
n (Maybe (Id, SyntaxTable) -> [TCElement])
-> Maybe (Id, SyntaxTable) -> [TCElement]
forall a b. (a -> b) -> a -> b
$ (SyntaxTable -> (Id, SyntaxTable))
-> Maybe SyntaxTable -> Maybe (Id, SyntaxTable)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ x :: SyntaxTable
x -> (lid -> symbol -> Id
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Id
sym_name lid
lid symbol
sym, SyntaxTable
x)) Maybe SyntaxTable
mSynTbl
    in if (Set symbol -> Bool) -> [Set symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (symbol -> Set symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember symbol
sym) [Set symbol]
sl
       then do
         TCElement
symConst <- lid -> NameMap symbol -> symbol -> String -> Result TCElement
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 -> symbol -> String -> Result TCElement
export_symToOmdoc lid
lid NameMap symbol
sm symbol
sym (String -> Result TCElement) -> String -> Result TCElement
forall a b. (a -> b) -> a -> b
$ UniqName -> String
nameToString UniqName
n
         [TCElement] -> Result [TCElement]
forall (m :: * -> *) a. Monad m => a -> m a
return ([TCElement] -> Result [TCElement])
-> [TCElement] -> Result [TCElement]
forall a b. (a -> b) -> a -> b
$ TCElement
symConst TCElement -> [TCElement] -> [TCElement]
forall a. a -> [a] -> [a]
: [TCElement]
symNotation
       else [TCElement] -> Result [TCElement]
forall (m :: * -> *) a. Monad m => a -> m a
return [TCElement]
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 symbol -> Named sentence -> Result [TCElement]
exportSentence lid :: lid
lid (SigMap sm :: NameMap symbol
sm thm :: NameMap String
thm) nsen :: Named sentence
nsen = do
  TCorOMElement
omobjOrAdt <- lid -> NameMap symbol -> sentence -> Result TCorOMElement
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 -> sentence -> Result TCorOMElement
export_senToOmdoc lid
lid NameMap symbol
sm (sentence -> Result TCorOMElement)
-> sentence -> Result TCorOMElement
forall a b. (a -> b) -> a -> b
$ Named sentence -> sentence
forall s a. SenAttr s a -> s
sentence Named sentence
nsen
  let symRole :: SymbolRole
symRole = if Named sentence -> Bool
forall s a. SenAttr s a -> Bool
isAxiom Named sentence
nsen Bool -> Bool -> Bool
&& Bool -> Bool
not (Named sentence -> Bool
forall s a. SenAttr s a -> Bool
wasTheorem Named sentence
nsen) then SymbolRole
Axiom
                else SymbolRole
Theorem
      thmName :: String
thmName = Named sentence -> String
forall s a. SenAttr s a -> a
senAttr Named sentence
nsen
      un :: UniqName
un = UniqName -> String -> NameMap String -> UniqName
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
           (String -> UniqName
forall a. HasCallStack => String -> a
error (String -> UniqName) -> String -> UniqName
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ "exportSentence: mapping for "
                           , String
thmName, " is missing!"]) String
thmName NameMap String
thm
      omname :: String
omname = UniqName -> String
nameToString UniqName
un
  case TCorOMElement
omobjOrAdt of
    Left adt :: TCElement
adt ->
        () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
warning () ("Name for adt not exported: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
omname) Range
nullRange
                    Result () -> Result [TCElement] -> Result [TCElement]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [TCElement] -> Result [TCElement]
forall (m :: * -> *) a. Monad m => a -> m a
return [TCElement
adt]
    Right omobj :: OMElement
omobj ->
        [TCElement] -> Result [TCElement]
forall (m :: * -> *) a. Monad m => a -> m a
return ([TCElement] -> Result [TCElement])
-> [TCElement] -> Result [TCElement]
forall a b. (a -> b) -> a -> b
$ String -> OMElement -> SymbolRole -> Maybe OMElement -> TCElement
TCSymbol String
omname OMElement
omobj SymbolRole
symRole Maybe OMElement
forall a. Maybe a
Nothing TCElement -> [TCElement] -> [TCElement]
forall a. a -> [a] -> [a]
:
                 UniqName -> Maybe (Id, SyntaxTable) -> [TCElement]
mkNotation UniqName
un Maybe (Id, SyntaxTable)
forall a. Maybe a
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 :: UniqName -> Maybe (Id, SyntaxTable) -> [TCElement]
mkNotation un :: UniqName
un mIdSTbl :: Maybe (Id, SyntaxTable)
mIdSTbl =
    let n :: String
n = UniqName -> String
nameToString UniqName
un
        orign :: String
orign = UniqName -> String
forall a b. (a, b) -> a
fst UniqName
un
        qn :: OMQualName
qn = UniqName -> OMQualName
mkSimpleQualName UniqName
un
        l :: [TCElement]
l = if String
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
orign then []
            else [OMQualName -> String -> Maybe String -> TCElement
TCNotation OMQualName
qn String
orign (Maybe String -> TCElement) -> Maybe String -> TCElement
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just "hets"]
    in case Maybe (Id, SyntaxTable)
mIdSTbl of
         Just (symid :: Id
symid, (pMap :: PrecMap
pMap, aMap :: AssocMap
aMap))
             | Id -> Bool
isMixfix Id
symid ->
                 let p :: Int
p = Int -> Id -> Map Id Int -> Int
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (PrecMap -> Int
maxWeight PrecMap
pMap) Id
symid
                         (Map Id Int -> Int) -> Map Id Int -> Int
forall a b. (a -> b) -> a -> b
$ PrecMap -> Map Id Int
precMap PrecMap
pMap
                     -- we use numbers instead of associativity values
                     a :: Assoc
a = case Id -> AssocMap -> Maybe AssocEither
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
symid AssocMap
aMap of
                           Just ALeft -> Assoc
LeftAssoc
                           Just ARight -> Assoc
RightAssoc
                           _ -> Assoc
NoneAssoc
                     (appNotation :: TCElement
appNotation, opStr :: String
opStr) = OMQualName -> Id -> Int -> Assoc -> (TCElement, String)
mkApplicationNotation OMQualName
qn Id
symid Int
p Assoc
a
                     l' :: [TCElement]
l' = TCElement
appNotation TCElement -> [TCElement] -> [TCElement]
forall a. a -> [a] -> [a]
: [TCElement]
l
                     l'' :: [TCElement]
l'' = OMQualName -> String -> Maybe String -> TCElement
TCNotation OMQualName
qn String
opStr Maybe String
forall a. Maybe a
Nothing TCElement -> [TCElement] -> [TCElement]
forall a. a -> [a] -> [a]
: [TCElement]
l'
                 in if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
opStr then [TCElement]
l' else [TCElement]
l''
             | Bool
otherwise -> [TCElement]
l
         _ -> [TCElement]
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 :: OMQualName -> Id -> Int -> Assoc -> (TCElement, String)
mkApplicationNotation qn :: OMQualName
qn symid :: Id
symid@(Id toks :: [Token]
toks _ _) prec :: Int
prec asc :: Assoc
asc
    | Id -> Int
placeCount Id
symid Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 = case [Token]
toks of
       [a :: Token
a, b :: Token
b]
           | Token -> Bool
isPlace Token
a ->
               (OMQualName -> String -> Fixity -> Int -> Assoc -> TCElement
mkSmartNotation OMQualName
qn (Token -> String
tokStr Token
b) Fixity
Postfix Int
prec Assoc
asc, Token -> String
tokStr Token
b)
           | Bool
otherwise ->
               (OMQualName -> String -> Fixity -> Int -> Assoc -> TCElement
mkSmartNotation OMQualName
qn (Token -> String
tokStr Token
a) Fixity
Prefix Int
prec Assoc
asc, Token -> String
tokStr Token
a)
       _ -> (OMQualName -> Id -> Int -> TCElement
mkFlexibleNotation OMQualName
qn Id
symid Int
prec, "")
    | Id -> Int
placeCount Id
symid Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 2 = case [Token]
toks of
       [_, b :: Token
b, _]
           | Bool -> Bool
not (Token -> Bool
isPlace Token
b) ->
               (OMQualName -> String -> Fixity -> Int -> Assoc -> TCElement
mkSmartNotation OMQualName
qn (Token -> String
tokStr Token
b) Fixity
Infix Int
prec Assoc
asc, Token -> String
tokStr Token
b)
           | Bool
otherwise -> (OMQualName -> Id -> Int -> TCElement
mkFlexibleNotation OMQualName
qn Id
symid Int
prec, "")
       _ -> (OMQualName -> Id -> Int -> TCElement
mkFlexibleNotation OMQualName
qn Id
symid Int
prec, "")
    | Bool
otherwise = (OMQualName -> Id -> Int -> TCElement
mkFlexibleNotation OMQualName
qn Id
symid Int
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 :: OMQualName -> String -> Fixity -> Int -> Assoc -> TCElement
mkSmartNotation qn :: OMQualName
qn _ fx :: Fixity
fx prec :: Int
prec asc :: Assoc
asc = OMQualName -> Fixity -> Assoc -> Int -> Int -> TCElement
TCSmartNotation OMQualName
qn Fixity
fx Assoc
asc Int
prec 0

mkFlexibleNotation :: OMQualName -> Id -> Int -> TCElement
mkFlexibleNotation :: OMQualName -> Id -> Int -> TCElement
mkFlexibleNotation qn :: OMQualName
qn opid :: Id
opid prec :: Int
prec =
    let f :: Int -> Token -> (Int, NotationComponent)
f acc :: Int
acc tok :: Token
tok = if Token -> Bool
isPlace Token
tok then (Int
acc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1, Int -> Int -> NotationComponent
ArgComp Int
acc Int
prec)
                    else (Int
acc, String -> NotationComponent
TextComp (String -> NotationComponent) -> String -> NotationComponent
forall a b. (a -> b) -> a -> b
$ Token -> String
tokStr Token
tok)
    in OMQualName -> Int -> [NotationComponent] -> TCElement
TCFlexibleNotation OMQualName
qn Int
prec ([NotationComponent] -> TCElement)
-> [NotationComponent] -> TCElement
forall a b. (a -> b) -> a -> b
$ (Int, [NotationComponent]) -> [NotationComponent]
forall a b. (a, b) -> b
snd ((Int, [NotationComponent]) -> [NotationComponent])
-> (Int, [NotationComponent]) -> [NotationComponent]
forall a b. (a -> b) -> a -> b
$ (Int -> Token -> (Int, NotationComponent))
-> Int -> [Token] -> (Int, [NotationComponent])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL Int -> Token -> (Int, NotationComponent)
f 1 ([Token] -> (Int, [NotationComponent]))
-> [Token] -> (Int, [NotationComponent])
forall a b. (a -> b) -> a -> b
$ Id -> [Token]
getTokens Id
opid