content: {-# 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
  