{- |
Module      :  ./Static/CheckGlobalContext.hs
Description :  checking consistency of indices
Copyright   :  (c) Jianchun Wang, C. Maeder, Uni Bremen 2002-2007
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(Logic)

compare indices from development graphs to the corresponding maps of
the global context
-}

module Static.CheckGlobalContext where

import Static.DevGraph
import Static.GTheory
import Logic.Grothendieck
import Logic.Comorphism

import Common.Lib.State

data Statistics = Statistics
    { Statistics -> SigId
zeroSign, Statistics -> SigId
wrongSign, Statistics -> SigId
rightSign :: SigId
    , Statistics -> MorId
zeroMor, Statistics -> MorId
wrongMor, Statistics -> MorId
rightMor :: MorId
    , Statistics -> ThId
zeroTh, Statistics -> ThId
wrongTh, Statistics -> ThId
rightTh :: ThId }
    deriving Int -> Statistics -> ShowS
[Statistics] -> ShowS
Statistics -> String
(Int -> Statistics -> ShowS)
-> (Statistics -> String)
-> ([Statistics] -> ShowS)
-> Show Statistics
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Statistics] -> ShowS
$cshowList :: [Statistics] -> ShowS
show :: Statistics -> String
$cshow :: Statistics -> String
showsPrec :: Int -> Statistics -> ShowS
$cshowsPrec :: Int -> Statistics -> ShowS
Show

initStat :: Statistics
initStat :: Statistics
initStat = Statistics :: SigId
-> SigId
-> SigId
-> MorId
-> MorId
-> MorId
-> ThId
-> ThId
-> ThId
-> Statistics
Statistics
  { zeroSign :: SigId
zeroSign = SigId
startSigId
  , wrongSign :: SigId
wrongSign = SigId
startSigId
  , rightSign :: SigId
rightSign = SigId
startSigId
  , zeroMor :: MorId
zeroMor = MorId
startMorId
  , wrongMor :: MorId
wrongMor = MorId
startMorId
  , rightMor :: MorId
rightMor = MorId
startMorId
  , zeroTh :: ThId
zeroTh = ThId
startThId
  , wrongTh :: ThId
wrongTh = ThId
startThId
  , rightTh :: ThId
rightTh = ThId
startThId }

incrZeroSign :: Statistics -> Statistics
incrZeroSign :: Statistics -> Statistics
incrZeroSign s :: Statistics
s = Statistics
s { zeroSign :: SigId
zeroSign = SigId -> SigId
forall a. Enum a => a -> a
succ (SigId -> SigId) -> SigId -> SigId
forall a b. (a -> b) -> a -> b
$ Statistics -> SigId
zeroSign Statistics
s }

incrWrongSign :: Statistics -> Statistics
incrWrongSign :: Statistics -> Statistics
incrWrongSign s :: Statistics
s = Statistics
s { wrongSign :: SigId
wrongSign = SigId -> SigId
forall a. Enum a => a -> a
succ (SigId -> SigId) -> SigId -> SigId
forall a b. (a -> b) -> a -> b
$ Statistics -> SigId
wrongSign Statistics
s }

incrRightSign :: Statistics -> Statistics
incrRightSign :: Statistics -> Statistics
incrRightSign s :: Statistics
s = Statistics
s { rightSign :: SigId
rightSign = SigId -> SigId
forall a. Enum a => a -> a
succ (SigId -> SigId) -> SigId -> SigId
forall a b. (a -> b) -> a -> b
$ Statistics -> SigId
rightSign Statistics
s }

incrZeroG_theory :: Statistics -> Statistics
incrZeroG_theory :: Statistics -> Statistics
incrZeroG_theory s :: Statistics
s = Statistics
s { zeroTh :: ThId
zeroTh = ThId -> ThId
forall a. Enum a => a -> a
succ (ThId -> ThId) -> ThId -> ThId
forall a b. (a -> b) -> a -> b
$ Statistics -> ThId
zeroTh Statistics
s }

incrWrongG_theory :: Statistics -> Statistics
incrWrongG_theory :: Statistics -> Statistics
incrWrongG_theory s :: Statistics
s = Statistics
s { wrongTh :: ThId
wrongTh = ThId -> ThId
forall a. Enum a => a -> a
succ (ThId -> ThId) -> ThId -> ThId
forall a b. (a -> b) -> a -> b
$ Statistics -> ThId
wrongTh Statistics
s }

incrRightG_theory :: Statistics -> Statistics
incrRightG_theory :: Statistics -> Statistics
incrRightG_theory s :: Statistics
s = Statistics
s { rightTh :: ThId
rightTh = ThId -> ThId
forall a. Enum a => a -> a
succ (ThId -> ThId) -> ThId -> ThId
forall a b. (a -> b) -> a -> b
$ Statistics -> ThId
rightTh Statistics
s }

incrZeroGMorphism :: Statistics -> Statistics
incrZeroGMorphism :: Statistics -> Statistics
incrZeroGMorphism s :: Statistics
s = Statistics
s { zeroMor :: MorId
zeroMor = MorId -> MorId
forall a. Enum a => a -> a
succ (MorId -> MorId) -> MorId -> MorId
forall a b. (a -> b) -> a -> b
$ Statistics -> MorId
zeroMor Statistics
s }

incrWrongGMorphism :: Statistics -> Statistics
incrWrongGMorphism :: Statistics -> Statistics
incrWrongGMorphism s :: Statistics
s = Statistics
s { wrongMor :: MorId
wrongMor = MorId -> MorId
forall a. Enum a => a -> a
succ (MorId -> MorId) -> MorId -> MorId
forall a b. (a -> b) -> a -> b
$ Statistics -> MorId
wrongMor Statistics
s }

incrRightGMorphism :: Statistics -> Statistics
incrRightGMorphism :: Statistics -> Statistics
incrRightGMorphism s :: Statistics
s = Statistics
s { rightMor :: MorId
rightMor = MorId -> MorId
forall a. Enum a => a -> a
succ (MorId -> MorId) -> MorId -> MorId
forall a b. (a -> b) -> a -> b
$ Statistics -> MorId
rightMor Statistics
s }

checkG_theory :: G_theory -> DGraph -> State Statistics ()
checkG_theory :: G_theory -> DGraph -> State Statistics ()
checkG_theory g :: G_theory
g@(G_theory _ _ _ si :: SigId
si _ ti :: ThId
ti) dgraph :: DGraph
dgraph = do
    if SigId
si SigId -> SigId -> Bool
forall a. Eq a => a -> a -> Bool
== SigId
startSigId then (Statistics -> Statistics) -> State Statistics ()
forall s. (s -> s) -> State s ()
modify Statistics -> Statistics
incrZeroSign
       else case SigId -> DGraph -> Maybe G_sign
lookupSigMapDG SigId
si DGraph
dgraph of
          Nothing -> String -> State Statistics ()
forall a. HasCallStack => String -> a
error "checkG_theory: Sign"
          Just signErg :: G_sign
signErg -> (Statistics -> Statistics) -> State Statistics ()
forall s. (s -> s) -> State s ()
modify ((Statistics -> Statistics) -> State Statistics ())
-> (Statistics -> Statistics) -> State Statistics ()
forall a b. (a -> b) -> a -> b
$ if G_theory -> G_sign
signOf G_theory
g G_sign -> G_sign -> Bool
forall a. Eq a => a -> a -> Bool
/= G_sign
signErg then Statistics -> Statistics
incrWrongSign
                          else Statistics -> Statistics
incrRightSign
    if ThId
ti ThId -> ThId -> Bool
forall a. Eq a => a -> a -> Bool
== ThId
startThId then (Statistics -> Statistics) -> State Statistics ()
forall s. (s -> s) -> State s ()
modify Statistics -> Statistics
incrZeroG_theory
       else case ThId -> DGraph -> Maybe G_theory
lookupThMapDG ThId
ti DGraph
dgraph of
          Nothing -> String -> State Statistics ()
forall a. HasCallStack => String -> a
error "checkG_theory: Theory"
          Just thErg :: G_theory
thErg -> (Statistics -> Statistics) -> State Statistics ()
forall s. (s -> s) -> State s ()
modify ((Statistics -> Statistics) -> State Statistics ())
-> (Statistics -> Statistics) -> State Statistics ()
forall a b. (a -> b) -> a -> b
$ if G_theory
g G_theory -> G_theory -> Bool
forall a. Eq a => a -> a -> Bool
/= G_theory
thErg then Statistics -> Statistics
incrWrongG_theory
                        else Statistics -> Statistics
incrRightG_theory

checkG_theoryInNode :: DGraph -> DGNodeLab -> State Statistics ()
checkG_theoryInNode :: DGraph -> DGNodeLab -> State Statistics ()
checkG_theoryInNode dgraph :: DGraph
dgraph dg :: DGNodeLab
dg = G_theory -> DGraph -> State Statistics ()
checkG_theory (DGNodeLab -> G_theory
dgn_theory DGNodeLab
dg) DGraph
dgraph

checkG_theoryInNodes :: DGraph -> State Statistics ()
checkG_theoryInNodes :: DGraph -> State Statistics ()
checkG_theoryInNodes dgraph :: DGraph
dgraph =
    (DGNodeLab -> State Statistics ())
-> [DGNodeLab] -> State Statistics ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (DGraph -> DGNodeLab -> State Statistics ()
checkG_theoryInNode DGraph
dgraph) ([DGNodeLab] -> State Statistics ())
-> [DGNodeLab] -> State Statistics ()
forall a b. (a -> b) -> a -> b
$ DGraph -> [DGNodeLab]
getDGNodeLab DGraph
dgraph

checkGMorphism :: GMorphism -> DGraph -> State Statistics ()
checkGMorphism :: GMorphism -> DGraph -> State Statistics ()
checkGMorphism g :: GMorphism
g@(GMorphism cid :: cid
cid sign :: ExtSign sign1 symbol1
sign si :: SigId
si _ mi :: MorId
mi) dgraph :: DGraph
dgraph = do
    if SigId
si SigId -> SigId -> Bool
forall a. Eq a => a -> a -> Bool
== SigId
startSigId then (Statistics -> Statistics) -> State Statistics ()
forall s. (s -> s) -> State s ()
modify Statistics -> Statistics
incrZeroSign
       else case SigId -> DGraph -> Maybe G_sign
lookupSigMapDG SigId
si DGraph
dgraph of
           Nothing -> String -> State Statistics ()
forall a. HasCallStack => String -> a
error "checkGMorphism: Sign"
           Just signErg :: G_sign
signErg -> (Statistics -> Statistics) -> State Statistics ()
forall s. (s -> s) -> State s ()
modify ((Statistics -> Statistics) -> State Statistics ())
-> (Statistics -> Statistics) -> State Statistics ()
forall a b. (a -> b) -> a -> b
$
                           if lid1 -> ExtSign sign1 symbol1 -> SigId -> G_sign
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 -> ExtSign sign symbol -> SigId -> G_sign
G_sign (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) ExtSign sign1 symbol1
sign SigId
si G_sign -> G_sign -> Bool
forall a. Eq a => a -> a -> Bool
/= G_sign
signErg
                           then Statistics -> Statistics
incrWrongSign else Statistics -> Statistics
incrRightSign
    if MorId
mi MorId -> MorId -> Bool
forall a. Eq a => a -> a -> Bool
== MorId
startMorId then (Statistics -> Statistics) -> State Statistics ()
forall s. (s -> s) -> State s ()
modify Statistics -> Statistics
incrZeroGMorphism
       else case MorId -> DGraph -> Maybe G_morphism
lookupMorMapDG MorId
mi DGraph
dgraph of
           Nothing -> String -> State Statistics ()
forall a. HasCallStack => String -> a
error "checkGMorphism: Morphism"
           Just morErg :: G_morphism
morErg -> (Statistics -> Statistics) -> State Statistics ()
forall s. (s -> s) -> State s ()
modify ((Statistics -> Statistics) -> State Statistics ())
-> (Statistics -> Statistics) -> State Statistics ()
forall a b. (a -> b) -> a -> b
$ if GMorphism
g GMorphism -> GMorphism -> Bool
forall a. Eq a => a -> a -> Bool
/= G_morphism -> GMorphism
gEmbed G_morphism
morErg then Statistics -> Statistics
incrWrongGMorphism
                          else Statistics -> Statistics
incrRightGMorphism

getDGLinkLab :: DGraph -> [DGLinkLab]
getDGLinkLab :: DGraph -> [DGLinkLab]
getDGLinkLab dgraph :: DGraph
dgraph = ((Int, Int, DGLinkLab) -> DGLinkLab)
-> [(Int, Int, DGLinkLab)] -> [DGLinkLab]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, _, l :: DGLinkLab
l) -> DGLinkLab
l) ([(Int, Int, DGLinkLab)] -> [DGLinkLab])
-> [(Int, Int, DGLinkLab)] -> [DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> [(Int, Int, DGLinkLab)]
labEdgesDG DGraph
dgraph

getDGNodeLab :: DGraph -> [DGNodeLab]
getDGNodeLab :: DGraph -> [DGNodeLab]
getDGNodeLab dgraph :: DGraph
dgraph = ((Int, DGNodeLab) -> DGNodeLab)
-> [(Int, DGNodeLab)] -> [DGNodeLab]
forall a b. (a -> b) -> [a] -> [b]
map (Int, DGNodeLab) -> DGNodeLab
forall a b. (a, b) -> b
snd ([(Int, DGNodeLab)] -> [DGNodeLab])
-> [(Int, DGNodeLab)] -> [DGNodeLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> [(Int, DGNodeLab)]
labNodesDG DGraph
dgraph

checkGMorphismInNode :: DGraph -> DGNodeLab -> State Statistics ()
checkGMorphismInNode :: DGraph -> DGNodeLab -> State Statistics ()
checkGMorphismInNode dgraph :: DGraph
dgraph dg :: DGNodeLab
dg = case DGNodeLab -> Maybe GMorphism
dgn_sigma DGNodeLab
dg of
    Nothing -> () -> State Statistics ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just gmor :: GMorphism
gmor -> GMorphism -> DGraph -> State Statistics ()
checkGMorphism GMorphism
gmor DGraph
dgraph

checkGMorphismInNodes :: DGraph -> State Statistics ()
checkGMorphismInNodes :: DGraph -> State Statistics ()
checkGMorphismInNodes dgraph :: DGraph
dgraph =
    (DGNodeLab -> State Statistics ())
-> [DGNodeLab] -> State Statistics ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (DGraph -> DGNodeLab -> State Statistics ()
checkGMorphismInNode DGraph
dgraph) ([DGNodeLab] -> State Statistics ())
-> [DGNodeLab] -> State Statistics ()
forall a b. (a -> b) -> a -> b
$ DGraph -> [DGNodeLab]
getDGNodeLab DGraph
dgraph

checkGMorphismInEdge :: DGraph -> DGLinkLab -> State Statistics ()
checkGMorphismInEdge :: DGraph -> DGLinkLab -> State Statistics ()
checkGMorphismInEdge dgraph :: DGraph
dgraph (DGLink {dgl_morphism :: DGLinkLab -> GMorphism
dgl_morphism = GMorphism
dgmor}) =
    GMorphism -> DGraph -> State Statistics ()
checkGMorphism GMorphism
dgmor DGraph
dgraph

checkGMorphismInEdges :: DGraph -> State Statistics ()
checkGMorphismInEdges :: DGraph -> State Statistics ()
checkGMorphismInEdges dgraph :: DGraph
dgraph =
    (DGLinkLab -> State Statistics ())
-> [DGLinkLab] -> State Statistics ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (DGraph -> DGLinkLab -> State Statistics ()
checkGMorphismInEdge DGraph
dgraph) ([DGLinkLab] -> State Statistics ())
-> [DGLinkLab] -> State Statistics ()
forall a b. (a -> b) -> a -> b
$ DGraph -> [DGLinkLab]
getDGLinkLab DGraph
dgraph

checkDGraph :: DGraph -> State Statistics ()
checkDGraph :: DGraph -> State Statistics ()
checkDGraph dgraph :: DGraph
dgraph = do
    DGraph -> State Statistics ()
checkGMorphismInNodes DGraph
dgraph
    DGraph -> State Statistics ()
checkG_theoryInNodes DGraph
dgraph
    DGraph -> State Statistics ()
checkGMorphismInEdges DGraph
dgraph

printStatistics :: DGraph -> String
printStatistics :: DGraph -> String
printStatistics dgraph :: DGraph
dgraph = [String] -> String
unlines
    [ "maxSigIndex = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SigId -> String
forall a. Show a => a -> String
show ((Map SigId G_sign, SigId) -> SigId
forall a b. (a, b) -> b
snd ((Map SigId G_sign, SigId) -> SigId)
-> (Map SigId G_sign, SigId) -> SigId
forall a b. (a -> b) -> a -> b
$ DGraph -> (Map SigId G_sign, SigId)
sigMapI DGraph
dgraph)
    , "maxGMorphismIndex = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ MorId -> String
forall a. Show a => a -> String
show ((Map MorId G_morphism, MorId) -> MorId
forall a b. (a, b) -> b
snd ((Map MorId G_morphism, MorId) -> MorId)
-> (Map MorId G_morphism, MorId) -> MorId
forall a b. (a -> b) -> a -> b
$ DGraph -> (Map MorId G_morphism, MorId)
morMapI DGraph
dgraph)
    , "maxG_theoryIndex = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ThId -> String
forall a. Show a => a -> String
show ((Map ThId G_theory, ThId) -> ThId
forall a b. (a, b) -> b
snd ((Map ThId G_theory, ThId) -> ThId)
-> (Map ThId G_theory, ThId) -> ThId
forall a b. (a -> b) -> a -> b
$ DGraph -> (Map ThId G_theory, ThId)
thMapI DGraph
dgraph)
    , Statistics -> String
forall a. Show a => a -> String
show (Statistics -> String) -> Statistics -> String
forall a b. (a -> b) -> a -> b
$ State Statistics () -> Statistics -> Statistics
forall s a. State s a -> s -> s
execState (DGraph -> State Statistics ()
checkDGraph DGraph
dgraph) Statistics
initStat
    ]