{- |
Module      :  ./Static/PrintDevGraph.hs
Description :  pretty printing (parts of) a LibEnv
Copyright   :  (c) C. Maeder, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(DevGraph)

pretty printing (parts of) a LibEnv
-}

module Static.PrintDevGraph
    ( prettyLibEnv
    , printTh
    , prettyHistElem
    , prettyHistory
    , prettyGr
    , prettyLEdge
    , showLEdge
    , dgOriginHeader
    , dgOriginSpec
    , showXPath
    , dgLinkOriginHeader
    , dgLinkOriginSpec
    , dgRuleHeader
    , dgRuleEdges
    ) where

import Syntax.Print_AS_Structured
import Syntax.AS_Structured

import Static.DgUtils
import Static.GTheory
import Static.DevGraph
import Static.History

import Common.GlobalAnnotations
import Common.LibName
import Common.Id
import Common.IRI
import Common.Consistency
import Common.Doc as Doc
import Common.DocUtils
import Common.Result
import Common.Keywords
import Common.ConvertGlobalAnnos
import Common.AnalyseAnnos
import qualified Common.Lib.SizedList as SizedList
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.Graph as Tree

import Data.Graph.Inductive.Graph as Graph
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.List
import Data.Char

printTh :: GlobalAnnos -> IRI -> G_theory -> Doc
printTh oga sn g =
    let ga = removeProblematicListAnnos oga in
    useGlobalAnnos ga $ pretty ga $+$ prettyGTheorySL g $+$
    sep [ if sn == nullIRI then Doc.empty else
             keyword specS <+> structIRI sn <+> equals
        , prettyGTheory (gTheorySyntax g) g]

removeProblematicListAnnos :: GlobalAnnos -> GlobalAnnos
removeProblematicListAnnos ga = let
    is = Map.keysSet $ Rel.toMap $ prec_annos ga
    la = literal_annos ga
    nla = la { list_lit = Map.filterWithKey ( \ li _ ->
        let (op, cl, cs) = getListBrackets li in
          Set.null $ Set.filter ( \ (Id ts ics _) ->
              cs == ics && isPrefixOf op ts && isSuffixOf cl ts) is)
        $ list_lit la }
    Result _ (Just lm) = store_literal_map Map.empty $ convertLiteralAnnos nla
    in ga { literal_annos = nla
          , literal_map = lm }

-- * pretty instances

showXPathComp :: XPathPart -> String
showXPathComp c = case c of
  ElemName s -> s
  ChildIndex i -> "Spec[" ++ show i ++ "]"

showXPath :: [XPathPart] -> String
showXPath l = case l of
  [] -> "/"
  _ -> concatMap (('/' :) . showXPathComp) l

showNodeId :: Node -> String
showNodeId i = "node " ++ show i

instance Pretty NodeSig where
  pretty (NodeSig n sig) = fsep [ text (showNodeId n) <> colon, pretty sig ]

instance Pretty NodeName where
  pretty n = text $ showName n

dgOriginSpec :: DGOrigin -> Maybe IRI
dgOriginSpec o = case o of
    DGInst n -> Just n
    DGFitView n -> Just n
    _ -> Nothing

dgOriginHeader :: DGOrigin -> String
dgOriginHeader o = case o of
    DGEmpty -> "empty-spec"
    DGBasic -> "foreign-basic-spec"
    DGBasicSpec {} -> "basic-spec"
    DGExtension -> "extension"
    DGLogicCoercion -> "logic-translation"
    DGTranslation _ -> "translation"
    DGUnion -> "union"
    DGIntersect -> "intersection"
    DGExtract -> "extraction"
    DGRestriction _ _ -> "restriction"
    DGRevealTranslation -> "translation part of a revealing"
    DGFreeOrCofree v -> map toLower (show v) ++ "-spec"
    DGLocal -> "local-spec"
    DGClosed -> "closed-spec"
    DGLogicQual -> "spec with logic qualifier"
    DGData -> "data-spec"
    DGFormalParams -> "formal parameters"
    DGImports -> "arch import"
    DGInst _ -> "instantiation"
    DGFitSpec -> "fitting-spec"
    DGFitView _ -> "fitting-view"
    DGProof -> "proof-construct"
    DGNormalForm n -> "normal-form(" ++ shows n ")"
    DGintegratedSCC -> "OWL spec with integrated strongly connected components"
    DGFlattening -> "flattening"
    DGTest -> "testing"
    DGAlignment -> "alignment"

instance Pretty DGOrigin where
  pretty o = let prettySyms headr syms = if Set.null syms then Doc.empty
                   else text headr $+$ pretty syms
    in text (dgOriginHeader o) <+> pretty (dgOriginSpec o)
      $+$ case o of
          DGBasicSpec mgbs _ syms -> case mgbs of
              Nothing -> Doc.empty
              Just gbs -> specBraces (pretty gbs)
            $+$ prettySyms "new symbols:" syms
          DGTranslation (Renamed r) -> pretty r
          DGRestriction rst syms -> let
              prtS = prettySyms "hidden symbols:" syms
              in case rst of
                Restricted r -> pretty r $+$ prtS
                NoRestriction -> prtS
          _ -> Doc.empty

instance Pretty DGNodeInfo where
  pretty c = case c of
    DGNode {} -> pretty $ node_origin c
    DGRef {} ->
      pretty (getLibId $ ref_libname c) <+> text (showNodeId $ ref_node c)

prettyDGNodeLab :: DGNodeLab -> Doc
prettyDGNodeLab l = sep [ text $ getDGNodeName l, pretty $ nodeInfo l]

instance Pretty DGNodeLab where
  pretty l = vcat
    [ text $ "xpath: " ++ showXPath (reverse $ xpath $ dgn_name l)
    , pretty $ getNodeConsStatus l
    , if hasOpenGoals l then text "has open goals" else
      if hasSenKind (const True) l then Doc.empty else text "locally empty"
    , if labelHasHiding l then text "has ingoing hiding link" else Doc.empty
    , case dgn_nf l of
        Nothing -> Doc.empty
        Just n -> text "normal form:" <+> text (showNodeId n)
    , text "origin:" $+$ pretty (nodeInfo l)
    , case dgn_sigma l of
        Nothing -> Doc.empty
        Just gm -> text "normal form inclusion:" $+$ pretty gm
    , text "local theory:"
    , pretty $ dgn_theory l]

instance Pretty EdgeId where
   pretty (EdgeId i) = text $ show i

dgLinkOriginSpec :: DGLinkOrigin -> Maybe IRI
dgLinkOriginSpec o = case o of
    DGLinkMorph n -> Just n
    DGLinkInst n _ -> Just n
    DGLinkInstArg n -> Just n
    DGLinkView n _ -> Just n
    DGLinkFitView n -> Just n
    DGLinkFitViewImp n -> Just n
    DGLinkRefinement n -> Just n
    _ -> Nothing

dgLinkMapping :: DGLinkOrigin -> [G_mapping]
dgLinkMapping o = case o of
    DGLinkInst _ (Fitted l) -> l
    DGLinkView _ (Fitted l) -> l
    _ -> []

dgLinkOriginHeader :: DGLinkOrigin -> String
dgLinkOriginHeader o = case o of
    SeeTarget -> "see target"
    DGLinkVerif -> "architectural verification condition"
    SeeSource -> "see source"
    DGImpliesLink -> "reversed implies link of extension"
    DGLinkExtension -> "extension"
    DGLinkTranslation -> "OMDoc translation"
    DGLinkClosedLenv -> "closed spec and local environment"
    DGLinkImports -> "OWL import"
    DGLinkIntersect -> "inclusion of intersection"
    DGLinkMorph _ -> "instantiation morphism of"
    DGLinkInst _ _ -> "instantiation of"
    DGLinkInstArg _ -> "actual parameter of"
    DGLinkView _ _ -> "view"
    DGLinkAlign _ -> "alignment"
    DGLinkFitView _ -> "fit source of"
    DGLinkFitViewImp _ -> "add import to source of"
    DGLinkProof -> "proof-link"
    DGLinkFlatteningUnion -> "flattening non-disjoint union"
    DGLinkFlatteningRename -> "flattening renaming"
    DGLinkRefinement _ -> "refinement"
    TEST -> "test"

instance Pretty DGLinkOrigin where
  pretty o = text (dgLinkOriginHeader o) <+> pretty (dgLinkOriginSpec o)
    $+$ ppWithCommas (dgLinkMapping o)

-- | only shows the edge and node ids
showLEdge :: LEdge DGLinkLab -> String
showLEdge (s, t, l) = "edge " ++ showEdgeId (dgl_id l)
  ++ " " ++ dglName l
  ++ "(" ++ showNodeId s ++ " --> " ++ show t ++ ")"

-- | only print the origin and parts of the type
prettyDGLinkLab :: (DGLinkLab -> Doc) -> DGLinkLab -> Doc
prettyDGLinkLab f l = fsep
  [ case dgl_origin l of
      SeeTarget -> Doc.empty
      o -> pretty o
  , f l ]

-- | print short edge information
prettyLEdge :: LEdge DGLinkLab -> Doc
prettyLEdge e@(_, _, l) = fsep
  [ text $ showLEdge e
  , prettyDGLinkLab (text . getDGLinkType) l
  , prettyThmLinkStatus $ dgl_type l ]

dgRuleEdges :: DGRule -> [EdgeId]
dgRuleEdges r = case r of
    DGRuleWithEdge _ l -> [l]
    Composition ls -> ls
    _ -> []

dgRuleHeader :: DGRule -> String
dgRuleHeader r = case r of
    DGRule str -> str
    DGRuleWithEdge str _ -> str
    DGRuleLocalInference _ -> "local-inference"
    Composition _ -> "composition"

instance Pretty DGRule where
  pretty r = let es = dgRuleEdges r in fsep
    [ text (dgRuleHeader r) <> if null es then Doc.empty else colon, case r of
    DGRuleLocalInference m ->
        braces $ sepByCommas $ map (\ (s, t) ->
          let d = text s in if s == t then d else pairElems d $ text t) m
    _ -> case es of
      [] -> Doc.empty
      _ -> pretty $ Set.fromList es]

instance Pretty ThmLinkStatus where
  pretty tls = case tls of
        LeftOpen -> Doc.empty
        Proven r ls -> let s = proofBasis ls in
          fcat [parens (pretty r), if Set.null s then Doc.empty else pretty s]

prettyThmLinkStatus :: DGLinkType -> Doc
prettyThmLinkStatus = maybe Doc.empty pretty . thmLinkStatus

instance Pretty ConsStatus where
   pretty (ConsStatus cons pc thm) = case max cons pc of
     None -> Doc.empty
     c -> text (show c) <> pretty thm

instance Pretty DGLinkType where
    pretty t = (case t of
       FreeOrCofreeDefLink v _ -> text $ show v
       _ -> Doc.empty)
         <> text (getDGEdgeTypeModIncName $ getHomEdgeType False True t)
               <> prettyThmLinkStatus t
               $+$ pretty (getLinkConsStatus t)

instance Pretty DGLinkLab where
  pretty l = let mor = pretty $ dgl_morphism l in vcat
    [ text "Origin:" <+> pretty (dgl_origin l)
    , text "Type:" <+> pretty (dgl_type l)
    , if dglPending l then text "proof chain incomplete" else Doc.empty
    , case dgl_type l of
        HidingFreeOrCofreeThm k n gm _ -> let nstr = showNodeId n ++ ":" in
          text ("Signature morphism from " ++ nstr)
          $+$ mor
          $+$ text ("with " ++ (case k of
          Nothing -> "hiding"
          Just v -> map toLower (show v))
          ++ " morphism:") $+$ pretty gm
        _ -> text "Signature morphism:" $+$ mor ]

-- | pretty print a labelled node
prettyGenLNode :: (a -> Doc) -> LNode a -> Doc
prettyGenLNode f (n, l) = fsep [text (showNodeId n) <> colon, f l]

prettyLNode :: LNode DGNodeLab -> Doc
prettyLNode = prettyGenLNode prettyDGNodeLab

dgChangeType :: DGChange -> String
dgChangeType c = case c of
    InsertNode _ -> "insert"
    DeleteNode _ -> "delete"
    InsertEdge _ -> "insert"
    DeleteEdge _ -> "delete"
    SetNodeLab _ _ -> "change"

instance Pretty DGChange where
  pretty c = text (dgChangeType c) <+> case c of
    InsertNode n -> prettyLNode n
    DeleteNode n -> prettyLNode n
    InsertEdge e -> prettyLEdge e
    DeleteEdge e -> prettyLEdge e
    SetNodeLab _ n -> prettyLNode n

prettyGr :: Tree.Gr DGNodeLab DGLinkLab -> Doc
prettyGr g = vcat (map prettyLNode $ labNodes g)
  $+$ vcat (map prettyLEdge $ labEdges g)

prettyImport :: MaybeNode -> Doc
prettyImport imp = case imp of
  EmptyNode _ -> Doc.empty
  JustNode n -> keyword givenS <+> pretty (getNode n)

prettyAllParams :: MaybeNode -> Doc
prettyAllParams ps = case ps of
  EmptyNode _ -> Doc.empty
  JustNode n -> pretty (getNode n)

instance Pretty ExtGenSig where
  pretty (ExtGenSig (GenSig imp params allParamSig) body) = fsep $
    pretty (getNode body) :
    (if null params then [] else
         [ pretty $ map getNode params
         , prettyAllParams allParamSig ]) ++
    [ prettyImport imp ]

instance Pretty ExtViewSig where
  pretty (ExtViewSig src gmor ptar) = fsep
    [ pretty (getNode src) <+> text toS
    , pretty ptar
    , pretty gmor ]

instance Pretty UnitSig where
  pretty (UnitSig params usig _) =
    (if null params then Doc.empty else pretty $ map getSig params)
    <+> pretty (getSig usig)

instance Pretty ImpUnitSigOrSig where
  pretty iu = case iu of
    ImpUnitSig imp usig -> fsep
      [ pretty usig, prettyImport imp ]
    Sig n -> keyword specS <+> pretty (getNode n)

instance Pretty RTNodeType where
 pretty (RTPlain usig) = pretty usig
 pretty (RTRef n) = pretty n

instance Pretty RTNodeLab where
 pretty rlab = fsep [text $ show $ rtn_name rlab,
                     text $ show $ rtn_diag rlab,
                     pretty $ rtn_type rlab
                     ]

instance Pretty RefSig where
  pretty = text . show -- missing

instance Pretty AlignSig where
  pretty = text . show -- missing

instance Pretty GlobalEntry where
  pretty ge = case ge of
    SpecEntry se -> topKey specS <+> pretty se
    ViewOrStructEntry b ve -> topKey (if b then viewS else structS)
      <+> pretty ve
    UnitEntry ue -> topKey unitS <+> pretty ue
    AlignEntry ae -> pretty ae
    ArchOrRefEntry b ae -> (if b then topKey archS else keyword refinementS)
      <+> pretty ae

instance Pretty DGraph where
  pretty dg = vcat
    [ prettyGr $ dgBody dg
    , text "global environment:"
    , printMap id vcat (\ k v -> fsep [k <+> mapsto, v]) $ globalEnv dg
    , text "history:"
    , prettyHistory $ reverseHistory $ proofHistory dg
    , text "redoable history:"
    , prettyHistory $ SizedList.reverse $ reverseHistory $ redoHistory dg
    , text "next edge:" <+> pretty (getNewEdgeId dg) ]

prettyHistElem :: HistElem -> Doc
prettyHistElem he = case he of
  HistElem c -> pretty c
  HistGroup r l -> text "rule:" <+> pretty r $+$ space <+> prettyHistory l

prettyHistory :: ProofHistory -> Doc
prettyHistory = vcat . map prettyHistElem . SizedList.toList

prettyLibEnv :: LibEnv -> Doc
prettyLibEnv = printMap id vsep ($+$)
