{- |
Module      :  ./Static/ComputeTheory.hs
Description :  compute the theory of a node
Copyright   :  (c) Christian Maeder and DFKI GmbH 2009
License     :  GPLv2 or higher, see LICENSE.txt

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

compute the theory of a node
-}

module Static.ComputeTheory
    ( computeTheory
    , globalNodeTheory
    , getGlobalTheory
    , recomputeNodeLabel
    , theoremsToAxioms
    , computeDGraphTheories
    , computeLibEnvTheories
    , computeLabelTheory
    , updateLabelTheory
    , markHiding
    , markFree
    , renumberDGLinks
    , getImportNames
    ) where

import Logic.Prover

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

import Common.LibName
import Common.Result
import Common.AS_Annotation
import qualified Common.OrderedMap as OMap
import qualified Control.Monad.Fail as Fail

import Data.Graph.Inductive.Graph as Graph
import Data.List (sortBy)
import qualified Data.Map as Map
import qualified Data.Set as Set (fromList, toList)
import Data.Ord

-- * nodes with incoming hiding definition links

nodeHasHiding :: DGraph -> Node -> Bool
nodeHasHiding :: DGraph -> Node -> Bool
nodeHasHiding dg :: DGraph
dg = DGNodeLab -> Bool
labelHasHiding (DGNodeLab -> Bool) -> (Node -> DGNodeLab) -> Node -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Node -> DGNodeLab
labDG DGraph
dg

nodeHasFree :: DGraph -> Node -> Bool
nodeHasFree :: DGraph -> Node -> Bool
nodeHasFree dg :: DGraph
dg = DGNodeLab -> Bool
labelHasFree (DGNodeLab -> Bool) -> (Node -> DGNodeLab) -> Node -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Node -> DGNodeLab
labDG DGraph
dg

{- | mark all nodes if they have incoming hiding edges.
   Assume reference nodes to other libraries being properly marked already.
-}
markFree :: LibEnv -> DGraph -> DGraph
markFree :: LibEnv -> DGraph -> DGraph
markFree le :: LibEnv
le dgraph :: DGraph
dgraph =
  (DGraph -> (Node, DGNodeLab) -> DGraph)
-> DGraph -> [(Node, DGNodeLab)] -> DGraph
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ dg :: DGraph
dg (n :: Node
n, lbl :: DGNodeLab
lbl) -> let
     ingoingEdges :: [LEdge DGLinkLab]
ingoingEdges = DGraph -> Node -> [LEdge DGLinkLab]
innDG DGraph
dg Node
n
     defEdges :: [LEdge DGLinkLab]
defEdges = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE DGLinkType -> Bool
isDefEdge) [LEdge DGLinkLab]
ingoingEdges
     freeDefEdges :: [LEdge DGLinkLab]
freeDefEdges = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE DGLinkType -> Bool
isFreeEdge ) [LEdge DGLinkLab]
defEdges
     in (DGraph, DGNodeLab) -> DGraph
forall a b. (a, b) -> a
fst ((DGraph, DGNodeLab) -> DGraph) -> (DGraph, DGNodeLab) -> DGraph
forall a b. (a -> b) -> a -> b
$ (Node, DGNodeLab) -> DGraph -> (DGraph, DGNodeLab)
labelNodeDG (Node
n, DGNodeLab
lbl { labelHasFree :: Bool
labelHasFree =
            if DGNodeLab -> Bool
isDGRef DGNodeLab
lbl
            then DGraph -> Node -> Bool
nodeHasFree (LibName -> LibEnv -> DGraph
lookupDGraph (DGNodeLab -> LibName
dgn_libname DGNodeLab
lbl) LibEnv
le)
                 (Node -> Bool) -> Node -> Bool
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> Node
dgn_node DGNodeLab
lbl
            else Bool -> Bool
not ([LEdge DGLinkLab] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LEdge DGLinkLab]
freeDefEdges) }) DGraph
dg)
     DGraph
dgraph ([(Node, DGNodeLab)] -> DGraph) -> [(Node, DGNodeLab)] -> DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> [(Node, DGNodeLab)]
topsortedNodes DGraph
dgraph

markHiding :: LibEnv -> DGraph -> DGraph
markHiding :: LibEnv -> DGraph -> DGraph
markHiding le :: LibEnv
le dgraph :: DGraph
dgraph =
  (DGraph -> (Node, DGNodeLab) -> DGraph)
-> DGraph -> [(Node, DGNodeLab)] -> DGraph
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ dg :: DGraph
dg (n :: Node
n, lbl :: DGNodeLab
lbl) -> let
     ingoingEdges :: [LEdge DGLinkLab]
ingoingEdges = DGraph -> Node -> [LEdge DGLinkLab]
innDG DGraph
dg Node
n
     defEdges :: [LEdge DGLinkLab]
defEdges = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE DGLinkType -> Bool
isDefEdge) [LEdge DGLinkLab]
ingoingEdges
     hidingDefEdges :: [LEdge DGLinkLab]
hidingDefEdges = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE DGLinkType -> Bool
isHidingDef ) [LEdge DGLinkLab]
defEdges
     next :: [Node]
next = (LEdge DGLinkLab -> Node) -> [LEdge DGLinkLab] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: Node
s, _, _) -> Node
s) [LEdge DGLinkLab]
defEdges
     in (DGraph, DGNodeLab) -> DGraph
forall a b. (a, b) -> a
fst ((DGraph, DGNodeLab) -> DGraph) -> (DGraph, DGNodeLab) -> DGraph
forall a b. (a -> b) -> a -> b
$ (Node, DGNodeLab) -> DGraph -> (DGraph, DGNodeLab)
labelNodeDG (Node
n, DGNodeLab
lbl { labelHasHiding :: Bool
labelHasHiding =
            if DGNodeLab -> Bool
isDGRef DGNodeLab
lbl
            then DGraph -> Node -> Bool
nodeHasHiding (LibName -> LibEnv -> DGraph
lookupDGraph (DGNodeLab -> LibName
dgn_libname DGNodeLab
lbl) LibEnv
le)
                 (Node -> Bool) -> Node -> Bool
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> Node
dgn_node DGNodeLab
lbl
            else Bool -> Bool
not ([LEdge DGLinkLab] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LEdge DGLinkLab]
hidingDefEdges) Bool -> Bool -> Bool
|| (Node -> Bool) -> [Node] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (DGraph -> Node -> Bool
nodeHasHiding DGraph
dg) [Node]
next }) DGraph
dg)
     DGraph
dgraph ([(Node, DGNodeLab)] -> DGraph) -> [(Node, DGNodeLab)] -> DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> [(Node, DGNodeLab)]
topsortedNodes DGraph
dgraph

computeTheory :: LibEnv -> LibName -> Node -> Maybe G_theory
computeTheory :: LibEnv -> LibName -> Node -> Maybe G_theory
computeTheory libEnv :: LibEnv
libEnv ln :: LibName
ln = DGraph -> Node -> Maybe G_theory
globalNodeTheory (DGraph -> Node -> Maybe G_theory)
-> DGraph -> Node -> Maybe G_theory
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
libEnv

theoremsToAxioms :: G_theory -> G_theory
theoremsToAxioms :: G_theory -> G_theory
theoremsToAxioms (G_theory lid :: lid
lid syn :: Maybe IRI
syn sign :: ExtSign sign symbol
sign ind1 :: SigId
ind1 sens :: ThSens sentence (AnyComorphism, BasicProof)
sens ind2 :: ThId
ind2) =
     lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
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 IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid Maybe IRI
syn ExtSign sign symbol
sign SigId
ind1 (Bool
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall a b. Ord a => Bool -> ThSens a b -> ThSens a b
markAsAxiom Bool
True ThSens sentence (AnyComorphism, BasicProof)
sens) ThId
ind2

getGlobalTheory :: DGNodeLab -> Result G_theory
getGlobalTheory :: DGNodeLab -> Result G_theory
getGlobalTheory = Result G_theory
-> (G_theory -> Result G_theory)
-> Maybe G_theory
-> Result G_theory
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> Result G_theory
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "no global theory") G_theory -> Result G_theory
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe G_theory -> Result G_theory)
-> (DGNodeLab -> Maybe G_theory) -> DGNodeLab -> Result G_theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGNodeLab -> Maybe G_theory
globalTheory

globalNodeTheory :: DGraph -> Node -> Maybe G_theory
globalNodeTheory :: DGraph -> Node -> Maybe G_theory
globalNodeTheory dg :: DGraph
dg = DGNodeLab -> Maybe G_theory
globalTheory (DGNodeLab -> Maybe G_theory)
-> (Node -> DGNodeLab) -> Node -> Maybe G_theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Node -> DGNodeLab
labDG DGraph
dg

computeLibEnvTheories :: LibEnv -> LibEnv
computeLibEnvTheories :: LibEnv -> LibEnv
computeLibEnvTheories le :: LibEnv
le =
    let lns :: [LibName]
lns = LibEnv -> [LibName]
getTopsortedLibs LibEnv
le
        upd :: LibEnv -> LibName -> LibEnv
upd le' :: LibEnv
le' ln :: LibName
ln = let dg0 :: DGraph
dg0 = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le
                         dg :: DGraph
dg = LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheories LibEnv
le' LibName
ln DGraph
dg0
                     in LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
dg LibEnv
le'
    in (LibEnv -> LibName -> LibEnv) -> LibEnv -> [LibName] -> LibEnv
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl LibEnv -> LibName -> LibEnv
upd LibEnv
forall k a. Map k a
Map.empty [LibName]
lns

computeDGraphTheories :: LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheories :: LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheories le :: LibEnv
le ln :: LibName
ln dgraph :: DGraph
dgraph =
  let newDg :: DGraph
newDg = LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheoriesAux LibEnv
le LibName
ln DGraph
dgraph
  in DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dgraph (String -> DGRule
DGRule "Compute theory") DGraph
newDg


computeDGraphTheoriesAux :: LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheoriesAux :: LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheoriesAux le :: LibEnv
le ln :: LibName
ln dgraph :: DGraph
dgraph =
  (DGraph -> (Node, DGNodeLab) -> DGraph)
-> DGraph -> [(Node, DGNodeLab)] -> DGraph
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ dg :: DGraph
dg l :: (Node, DGNodeLab)
l@(n :: Node
n, lbl :: DGNodeLab
lbl) -> DGraph -> DGNodeLab -> (Node, DGNodeLab) -> DGraph
updatePending DGraph
dg DGNodeLab
lbl
    (Node
n, LibEnv -> LibName -> DGraph -> (Node, DGNodeLab) -> DGNodeLab
recomputeNodeLabel LibEnv
le LibName
ln DGraph
dg (Node, DGNodeLab)
l))
     DGraph
dgraph ([(Node, DGNodeLab)] -> DGraph) -> [(Node, DGNodeLab)] -> DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> [(Node, DGNodeLab)]
topsortedNodes DGraph
dgraph

recomputeNodeLabel :: LibEnv -> LibName -> DGraph -> LNode DGNodeLab -> DGNodeLab
recomputeNodeLabel :: LibEnv -> LibName -> DGraph -> (Node, DGNodeLab) -> DGNodeLab
recomputeNodeLabel le :: LibEnv
le ln :: LibName
ln dg :: DGraph
dg l :: (Node, DGNodeLab)
l@(n :: Node
n, lbl :: DGNodeLab
lbl) =
  case LibEnv -> LibName -> DGraph -> (Node, DGNodeLab) -> Maybe G_theory
computeLabelTheory LibEnv
le LibName
ln DGraph
dg (Node, DGNodeLab)
l of
    gTh :: Maybe G_theory
gTh@(Just th :: G_theory
th) ->
      let (chg :: Bool
chg, lbl1 :: DGNodeLab
lbl1) = case DGNodeLab -> Maybe G_theory
globalTheory DGNodeLab
lbl of
            Nothing -> (Bool
False, DGNodeLab
lbl)
            Just oTh :: G_theory
oTh -> let
              (same :: Bool
same, nLocTh :: G_theory
nLocTh) = G_theory -> G_theory -> G_theory -> (Bool, G_theory)
invalidateProofs G_theory
oTh G_theory
th (G_theory -> (Bool, G_theory)) -> G_theory -> (Bool, G_theory)
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory DGNodeLab
lbl
              in (Bool -> Bool
not Bool
same, DGNodeLab
lbl { dgn_theory :: G_theory
dgn_theory = G_theory
nLocTh })
          ngTh :: Maybe G_theory
ngTh = if Bool
chg then LibEnv -> LibName -> DGraph -> (Node, DGNodeLab) -> Maybe G_theory
computeLabelTheory LibEnv
le LibName
ln DGraph
dg (Node
n, DGNodeLab
lbl1) else Maybe G_theory
gTh
      in case Maybe G_theory
ngTh of
        Just nth :: G_theory
nth@(G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) ->
          (if ThSens sentence (AnyComorphism, BasicProof) -> Bool
forall k a. Map k a -> Bool
Map.null ThSens sentence (AnyComorphism, BasicProof)
sens then String -> DGNodeLab -> DGNodeLab
markNodeConsistent "ByNoSentences" DGNodeLab
lbl1
           else DGNodeLab
lbl1 { dgn_theory :: G_theory
dgn_theory = G_theory -> G_theory -> G_theory
proveLocalSens G_theory
nth (DGNodeLab -> G_theory
dgn_theory DGNodeLab
lbl1) })
           { globalTheory :: Maybe G_theory
globalTheory = Maybe G_theory
ngTh }
        Nothing -> DGNodeLab
lbl1
    Nothing -> DGNodeLab
lbl

computeLabelTheory :: LibEnv -> LibName -> DGraph -> LNode DGNodeLab -> Maybe G_theory
computeLabelTheory :: LibEnv -> LibName -> DGraph -> (Node, DGNodeLab) -> Maybe G_theory
computeLabelTheory le :: LibEnv
le ln :: LibName
ln dg :: DGraph
dg (n :: Node
n, lbl :: DGNodeLab
lbl) = let 
  localTh :: G_theory
localTh = DGNodeLab -> G_theory
dgn_theory DGNodeLab
lbl 
  lblName :: LibName
lblName = DGNodeLab -> LibName
dgn_libname DGNodeLab
lbl 
  lblNode :: Node
lblNode = DGNodeLab -> Node
dgn_node DGNodeLab
lbl 
 in (G_theory -> G_theory) -> Maybe G_theory -> Maybe G_theory
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap G_theory -> G_theory
reduceTheory (Maybe G_theory -> Maybe G_theory)
-> (Result G_theory -> Maybe G_theory)
-> Result G_theory
-> Maybe G_theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result G_theory -> Maybe G_theory
forall a. Result a -> Maybe a
maybeResult (Result G_theory -> Maybe G_theory)
-> Result G_theory -> Maybe G_theory
forall a b. (a -> b) -> a -> b
$ if DGNodeLab -> Bool
isDGRef DGNodeLab
lbl then
        case LibName -> LibEnv -> Maybe DGraph
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LibName
lblName LibEnv
le of
          Nothing -> G_theory -> Result G_theory
forall (m :: * -> *) a. Monad m => a -> m a
return G_theory
localTh -- do not crash here
          Just dg' :: DGraph
dg' -> do
            _refTh :: G_theory
_refTh@(G_theory gtl :: lid
gtl gsub :: Maybe IRI
gsub gts :: ExtSign sign symbol
gts gind1 :: SigId
gind1 sens :: ThSens sentence (AnyComorphism, BasicProof)
sens gind2 :: ThId
gind2) <- DGNodeLab -> Result G_theory
getGlobalTheory (DGNodeLab -> Result G_theory) -> DGNodeLab -> Result G_theory
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> DGNodeLab
labDG DGraph
dg' Node
lblNode
            let refTh' :: G_theory
refTh' = lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
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 IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
gtl Maybe IRI
gsub ExtSign sign symbol
gts SigId
gind1 
                            ((String
 -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a b. (k -> a -> b) -> OMap k a -> OMap k b
OMap.mapWithKey (\k :: String
k a :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
a -> IRI
-> Node
-> String
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
forall s a. IRI -> Node -> String -> SenAttr s a -> SenAttr s a
setOriginIfLocal (String -> IRI
filePathToLibId (String -> IRI) -> String -> IRI
forall a b. (a -> b) -> a -> b
$ LibName -> String
libToFileName LibName
lblName) Node
lblNode String
k SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
a) ThSens sentence (AnyComorphism, BasicProof)
sens) 
                             ThId
gind2
            G_theory -> G_theory -> Result G_theory
forall (m :: * -> *).
MonadFail m =>
G_theory -> G_theory -> m G_theory
joinG_sentences G_theory
refTh' G_theory
localTh
    else do
      [G_theory]
ths <- (LEdge DGLinkLab -> Result G_theory)
-> [LEdge DGLinkLab] -> Result [G_theory]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (s :: Node
s, _, l :: DGLinkLab
l) -> do
         _th :: G_theory
_th@(G_theory gtl :: lid
gtl gsub :: Maybe IRI
gsub gts :: ExtSign sign symbol
gts gind1 :: SigId
gind1 sens :: ThSens sentence (AnyComorphism, BasicProof)
sens gind2 :: ThId
gind2) <- let sl :: DGNodeLab
sl = DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
s in if DGLinkType -> Bool
isLocalDef (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l then
                   G_theory -> Result G_theory
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory -> Result G_theory) -> G_theory -> Result G_theory
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory DGNodeLab
sl
               else DGNodeLab -> Result G_theory
getGlobalTheory DGNodeLab
sl
         let th :: G_theory
th = lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
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 IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
gtl Maybe IRI
gsub ExtSign sign symbol
gts SigId
gind1 
                   ((String
 -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a b. (k -> a -> b) -> OMap k a -> OMap k b
OMap.mapWithKey (\k :: String
k a :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
a -> IRI
-> Node
-> String
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
forall s a. IRI -> Node -> String -> SenAttr s a -> SenAttr s a
setOriginIfLocal (String -> IRI
filePathToLibId (String -> IRI) -> String -> IRI
forall a b. (a -> b) -> a -> b
$ LibName -> String
libToFileName LibName
ln) Node
s String
k SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
a) ThSens sentence (AnyComorphism, BasicProof)
sens) 
                   ThId
gind2
         -- translate theory and turn all imported theorems into axioms
         GMorphism -> G_theory -> Result G_theory
translateG_theory (DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
l) (G_theory -> Result G_theory) -> G_theory -> Result G_theory
forall a b. (a -> b) -> a -> b
$ G_theory -> G_theory
theoremsToAxioms G_theory
th)
         ([LEdge DGLinkLab] -> Result [G_theory])
-> [LEdge DGLinkLab] -> Result [G_theory]
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> LEdge DGLinkLab -> Ordering)
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy
            ((LEdge DGLinkLab -> LEdge DGLinkLab -> Ordering)
-> LEdge DGLinkLab -> LEdge DGLinkLab -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((LEdge DGLinkLab -> LEdge DGLinkLab -> Ordering)
 -> LEdge DGLinkLab -> LEdge DGLinkLab -> Ordering)
-> (LEdge DGLinkLab -> LEdge DGLinkLab -> Ordering)
-> LEdge DGLinkLab
-> LEdge DGLinkLab
-> Ordering
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> EdgeId)
-> LEdge DGLinkLab -> LEdge DGLinkLab -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (\ (_, _, l :: DGLinkLab
l) -> DGLinkLab -> EdgeId
dgl_id DGLinkLab
l))
            ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> [LEdge DGLinkLab]
getImports DGraph
dg Node
n
      G_theory -> [G_theory] -> Result G_theory
forall (m :: * -> *).
MonadFail m =>
G_theory -> [G_theory] -> m G_theory
flatG_sentences G_theory
localTh [G_theory]
ths

getImports :: DGraph -> Node -> [LEdge DGLinkLab]
getImports :: DGraph -> Node -> [LEdge DGLinkLab]
getImports dg :: DGraph
dg = (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a. (DGLinkType -> a) -> LEdge DGLinkLab -> a
liftE ((DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool)
-> (DGLinkType -> Bool) -> LEdge DGLinkLab -> Bool
forall a b. (a -> b) -> a -> b
$ (DGLinkType -> Bool) -> (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
liftOr DGLinkType -> Bool
isGlobalDef DGLinkType -> Bool
isLocalDef) ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> (Node -> [LEdge DGLinkLab]) -> Node -> [LEdge DGLinkLab]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Node -> [LEdge DGLinkLab]
innDG DGraph
dg

getImportNames :: DGraph -> Node -> [String]
getImportNames :: DGraph -> Node -> [String]
getImportNames dg :: DGraph
dg = (LEdge DGLinkLab -> String) -> [LEdge DGLinkLab] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: Node
s, _, _) -> DGNodeLab -> String
getDGNodeName (DGNodeLab -> String) -> DGNodeLab -> String
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
s)
  ([LEdge DGLinkLab] -> [String])
-> (Node -> [LEdge DGLinkLab]) -> Node -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Node -> [LEdge DGLinkLab]
getImports DGraph
dg

reduceTheory :: G_theory -> G_theory
reduceTheory :: G_theory -> G_theory
reduceTheory (G_theory lid :: lid
lid syn :: Maybe IRI
syn sig :: ExtSign sign symbol
sig ind :: SigId
ind sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) =
  lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
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 IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid Maybe IRI
syn ExtSign sign symbol
sig SigId
ind (ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall a b. (Ord a, Eq b) => ThSens a b -> ThSens a b
reduceSens ThSens sentence (AnyComorphism, BasicProof)
sens) ThId
startThId

updateLabelTheory :: LibEnv -> LibName -> DGraph -> LNode DGNodeLab -> G_theory -> DGraph
updateLabelTheory :: LibEnv
-> LibName -> DGraph -> (Node, DGNodeLab) -> G_theory -> DGraph
updateLabelTheory le :: LibEnv
le ln :: LibName
ln dg :: DGraph
dg (i :: Node
i, l :: DGNodeLab
l) gth :: G_theory
gth = let
    l' :: DGNodeLab
l' = DGNodeLab
l { dgn_theory :: G_theory
dgn_theory = G_theory
gth }
    n :: (Node, DGNodeLab)
n = (Node
i, DGNodeLab
l' { globalTheory :: Maybe G_theory
globalTheory = LibEnv -> LibName -> DGraph -> (Node, DGNodeLab) -> Maybe G_theory
computeLabelTheory LibEnv
le LibName
ln DGraph
dg (Node
i, DGNodeLab
l') })
    in DGraph -> DGNodeLab -> (Node, DGNodeLab) -> DGraph
updatePending DGraph
dg DGNodeLab
l (Node, DGNodeLab)
n

updatePending :: DGraph
  -> DGNodeLab -- ^ old label
  -> LNode DGNodeLab -- ^ node with new label
  -> DGraph
updatePending :: DGraph -> DGNodeLab -> (Node, DGNodeLab) -> DGraph
updatePending dg :: DGraph
dg l :: DGNodeLab
l n :: (Node, DGNodeLab)
n = let
    dg0 :: DGraph
dg0 = DGraph -> DGChange -> DGraph
changeDGH DGraph
dg (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> (Node, DGNodeLab) -> DGChange
SetNodeLab DGNodeLab
l (Node, DGNodeLab)
n
    dg1 :: DGraph
dg1 = DGraph -> [LEdge DGLinkLab] -> DGraph
togglePending DGraph
dg0 ([LEdge DGLinkLab] -> DGraph) -> [LEdge DGLinkLab] -> DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> (Node, DGNodeLab) -> [LEdge DGLinkLab]
changedLocalTheorems DGraph
dg0 (Node, DGNodeLab)
n
    dg2 :: DGraph
dg2 = DGraph -> [LEdge DGLinkLab] -> DGraph
togglePending DGraph
dg1 ([LEdge DGLinkLab] -> DGraph) -> [LEdge DGLinkLab] -> DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> [LEdge DGLinkLab]
changedPendingEdges DGraph
dg1
    in DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg (String -> DGRule
DGRule "Node proof") DGraph
dg2

{- | iterate all edgeId entries of the dg and increase all that are equal or
above the old lId (1st param) so they will be above the desired nextLId
(2nd param) -}
renumberDGLinks :: EdgeId -> EdgeId -> DGraph -> DGraph
renumberDGLinks :: EdgeId -> EdgeId -> DGraph -> DGraph
renumberDGLinks (EdgeId i1 :: Node
i1) (EdgeId i2 :: Node
i2) dg :: DGraph
dg = if Node
i1 Node -> Node -> Bool
forall a. Ord a => a -> a -> Bool
>= Node
i2 then DGraph
dg else
  DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg ([DGChange] -> DGraph) -> [DGChange] -> DGraph
forall a b. (a -> b) -> a -> b
$ (LEdge DGLinkLab -> [DGChange]) -> [LEdge DGLinkLab] -> [DGChange]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap LEdge DGLinkLab -> [DGChange]
mkRenumberChange ([LEdge DGLinkLab] -> [DGChange])
-> [LEdge DGLinkLab] -> [DGChange]
forall a b. (a -> b) -> a -> b
$ DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dg where
  needUpd :: EdgeId -> Bool
needUpd (EdgeId x :: Node
x) = Node
x Node -> Node -> Bool
forall a. Ord a => a -> a -> Bool
>= Node
i1
  offset :: Node
offset = Node
i2 Node -> Node -> Node
forall a. Num a => a -> a -> a
- Node
i1
  add :: EdgeId -> EdgeId
add (EdgeId x :: Node
x) = Node -> EdgeId
EdgeId (Node -> EdgeId) -> Node -> EdgeId
forall a b. (a -> b) -> a -> b
$ Node
x Node -> Node -> Node
forall a. Num a => a -> a -> a
+ Node
offset
  mkRenumberChange :: LEdge DGLinkLab -> [DGChange]
mkRenumberChange e :: LEdge DGLinkLab
e@(s :: Node
s, t :: Node
t, l :: DGLinkLab
l) = let
    ei :: EdgeId
ei = DGLinkLab -> EdgeId
dgl_id DGLinkLab
l
    -- update links own id if required
    (upd :: Bool
upd, newId :: EdgeId
newId) = let b :: Bool
b = EdgeId -> Bool
needUpd EdgeId
ei in (Bool
b, if Bool
b then EdgeId -> EdgeId
add EdgeId
ei else EdgeId
ei)
    -- make updates to links proof basis if required
    (upd' :: Bool
upd', newTp :: DGLinkType
newTp) = let
      pB :: ProofBasis
pB = DGLinkLab -> ProofBasis
getProofBasis DGLinkLab
l
      (b :: Bool
b, pBids :: [EdgeId]
pBids) = ((Bool, [EdgeId]) -> EdgeId -> (Bool, [EdgeId]))
-> (Bool, [EdgeId]) -> [EdgeId] -> (Bool, [EdgeId])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ (bR :: Bool
bR, eiR :: [EdgeId]
eiR) ei' :: EdgeId
ei' -> let bi :: Bool
bi = EdgeId -> Bool
needUpd EdgeId
ei' in
        (Bool
bR Bool -> Bool -> Bool
|| Bool
bi, if Bool
bi then EdgeId -> EdgeId
add EdgeId
ei' EdgeId -> [EdgeId] -> [EdgeId]
forall a. a -> [a] -> [a]
: [EdgeId]
eiR else EdgeId
ei' EdgeId -> [EdgeId] -> [EdgeId]
forall a. a -> [a] -> [a]
: [EdgeId]
eiR))
          (Bool
False, []) ([EdgeId] -> (Bool, [EdgeId])) -> [EdgeId] -> (Bool, [EdgeId])
forall a b. (a -> b) -> a -> b
$ Set EdgeId -> [EdgeId]
forall a. Set a -> [a]
Set.toList (Set EdgeId -> [EdgeId]) -> Set EdgeId -> [EdgeId]
forall a b. (a -> b) -> a -> b
$ ProofBasis -> Set EdgeId
proofBasis ProofBasis
pB
      in (Bool
b, (if Bool
b then (DGLinkType -> ProofBasis -> DGLinkType)
-> ProofBasis -> DGLinkType -> DGLinkType
forall a b c. (a -> b -> c) -> b -> a -> c
flip DGLinkType -> ProofBasis -> DGLinkType
updThmProofBasis
        (ProofBasis -> DGLinkType -> DGLinkType)
-> (Set EdgeId -> ProofBasis)
-> Set EdgeId
-> DGLinkType
-> DGLinkType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set EdgeId -> ProofBasis
ProofBasis (Set EdgeId -> DGLinkType -> DGLinkType)
-> Set EdgeId -> DGLinkType -> DGLinkType
forall a b. (a -> b) -> a -> b
$ [EdgeId] -> Set EdgeId
forall a. Ord a => [a] -> Set a
Set.fromList [EdgeId]
pBids else DGLinkType -> DGLinkType
forall a. a -> a
id) (DGLinkType -> DGLinkType) -> DGLinkType -> DGLinkType
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l)
    -- update in dg unless no updates conducted
    in if Bool
upd Bool -> Bool -> Bool
|| Bool
upd' then [LEdge DGLinkLab -> DGChange
DeleteEdge LEdge DGLinkLab
e, LEdge DGLinkLab -> DGChange
InsertEdge (Node
s, Node
t, DGLinkLab
l
      { dgl_id :: EdgeId
dgl_id = EdgeId
newId, dgl_type :: DGLinkType
dgl_type = DGLinkType
newTp })] else []