{- |
Module      :  ./Static/AnalysisStructured.hs
Description :  static analysis of DOL OMS and heterogeneous structured specifications
Copyright   :  (c) Till Mossakowski and Uni Magdeburg 2003-2016
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Grothendieck)

Static analysis of DOL OMS and networks and
       CASL (heterogeneous) structured specifications
  Follows the semantics of DOL OMS and networks,
   DOL OMG standard, clauses 10.2.2 and 10.2.3
-}

module Static.AnalysisStructured
    ( anaSpec
    , anaSpecTop
    , anaUnion
    , anaIntersect
    , anaSublogic
    , getSpecAnnos
    , anaRenaming
    , anaRestriction
    , partitionGmaps
    , homogenizeGM
    , anaGmaps
    , insGSig
    , insLink
    , extendMorphism
    , insGTheory
    , expCurie
    , expCurieR
    , expandCurieByPath
    , ExpOverrides
    , notFoundError
    , prefixErrorIRI
    , networkDiagram
    ) where

import Driver.Options

import Logic.Logic
import Logic.ExtSign
import Logic.Coerce
import Logic.Comorphism
import Logic.Grothendieck
import Logic.Prover

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

import Syntax.AS_Structured
import Syntax.Print_AS_Structured

import Common.AS_Annotation hiding (isAxiom, isDef)
import Common.Consistency
import Common.DocUtils
import Common.ExtSign
import Common.GlobalAnnotations
import Common.Id
import Common.IRI
import Common.LibName
import Common.Result
import Common.Utils (number)
import Common.Lib.MapSet (imageSet, setInsert)
import qualified Control.Monad.Fail as Fail

import Data.Graph.Inductive.Graph
import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.Maybe
import Data.List
import Data.Function

import Control.Monad
import Proofs.ComputeColimit (insertColimitInGraph)

import Common.Lib.Graph

import Static.ComputeTheory

-- overrides CUIRIE expansion for Download_items
type ExpOverrides = Map.Map IRI FilePath

coerceMaybeNode :: LogicGraph -> LibEnv -> LibName ->
                   DGraph -> MaybeNode -> NodeName -> AnyLogic
                -> Result (MaybeNode, DGraph)
coerceMaybeNode :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> AnyLogic
-> Result (MaybeNode, DGraph)
coerceMaybeNode lg :: LogicGraph
lg libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg mn :: MaybeNode
mn nn :: NodeName
nn l2 :: AnyLogic
l2 = case MaybeNode
mn of
  EmptyNode _ -> (MaybeNode, DGraph) -> Result (MaybeNode, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (AnyLogic -> MaybeNode
EmptyNode AnyLogic
l2, DGraph
dg)
  JustNode ns :: NodeSig
ns -> do
    (ms :: NodeSig
ms, dg2 :: DGraph
dg2) <- LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> NodeSig
-> NodeName
-> AnyLogic
-> Result (NodeSig, DGraph)
coerceNode LogicGraph
lg LibEnv
libEnv LibName
ln DGraph
dg NodeSig
ns NodeName
nn AnyLogic
l2
    (MaybeNode, DGraph) -> Result (MaybeNode, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeSig -> MaybeNode
JustNode NodeSig
ms, DGraph
dg2)

coerceNode :: LogicGraph -> LibEnv -> LibName ->
              DGraph -> NodeSig -> NodeName -> AnyLogic
           -> Result (NodeSig, DGraph)
coerceNode :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> NodeSig
-> NodeName
-> AnyLogic
-> Result (NodeSig, DGraph)
coerceNode lg :: LogicGraph
lg libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg ns :: NodeSig
ns@(NodeSig _ (G_sign lid1 :: lid
lid1 _ _)) nn :: NodeName
nn l2 :: AnyLogic
l2@(Logic lid2 :: lid
lid2) =
    if lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid2 then (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeSig
ns, DGraph
dg)
    else do
      AnyComorphism
c <- LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
logicInclusion LogicGraph
lg (lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid1) AnyLogic
l2
      LibEnv
-> LibName
-> AnyComorphism
-> DGraph
-> NodeSig
-> NodeName
-> Result (NodeSig, DGraph)
coerceNodeByComorph LibEnv
libEnv LibName
ln AnyComorphism
c DGraph
dg NodeSig
ns NodeName
nn

coerceNodeByComorph :: LibEnv -> LibName -> AnyComorphism -> DGraph -> NodeSig -> NodeName
           -> Result (NodeSig, DGraph)
coerceNodeByComorph :: LibEnv
-> LibName
-> AnyComorphism
-> DGraph
-> NodeSig
-> NodeName
-> Result (NodeSig, DGraph)
coerceNodeByComorph libEnv :: LibEnv
libEnv ln :: LibName
ln c :: AnyComorphism
c@(Comorphism cid :: cid
cid) dg :: DGraph
dg (NodeSig n :: Node
n s :: G_sign
s) nn :: NodeName
nn = do
      (dg' :: DGraph
dg', gmor :: GMorphism
gmor) <- if cid -> Bool
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 -> Bool
isGTC cid
cid then do
                       let dg0 :: DGraph
dg0 = LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheories LibEnv
libEnv LibName
ln DGraph
dg
                           Just l :: DGNodeLab
l = Gr DGNodeLab DGLinkLab -> Node -> Maybe DGNodeLab
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> Maybe a
lab (DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg0) Node
n 
                           Just gth :: G_theory
gth = DGNodeLab -> Maybe G_theory
globalTheory DGNodeLab
l
                       GMorphism
gm <- AnyComorphism -> G_theory -> Result GMorphism
gEmbedGTC AnyComorphism
c G_theory
gth
                       (DGraph, GMorphism) -> Result (DGraph, GMorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph
dg0, GMorphism
gm)
                     else do 
                      GMorphism
gm <- AnyComorphism -> G_sign -> Result GMorphism
gEmbedComorphism AnyComorphism
c G_sign
s
                      (DGraph, GMorphism) -> Result (DGraph, GMorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph
dg, GMorphism
gm)      
      case ((Node, Node, DGLinkLab) -> Bool)
-> [(Node, Node, DGLinkLab)] -> Maybe (Node, Node, DGLinkLab)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\ (_, _, l :: DGLinkLab
l) -> DGLinkLab -> DGLinkOrigin
dgl_origin DGLinkLab
l DGLinkOrigin -> DGLinkOrigin -> Bool
forall a. Eq a => a -> a -> Bool
== DGLinkOrigin
SeeTarget
          Bool -> Bool -> Bool
&& DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l DGLinkType -> DGLinkType -> Bool
forall a. Eq a => a -> a -> Bool
== DGLinkType
globalDef
          Bool -> Bool -> Bool
&& DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
l GMorphism -> GMorphism -> Bool
forall a. Eq a => a -> a -> Bool
== GMorphism
gmor) ([(Node, Node, DGLinkLab)] -> Maybe (Node, Node, DGLinkLab))
-> [(Node, Node, DGLinkLab)] -> Maybe (Node, Node, DGLinkLab)
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> [(Node, Node, DGLinkLab)]
outDG DGraph
dg' Node
n of
        Nothing -> do
          let (ms :: NodeSig
ms@(NodeSig m :: Node
m _), dg2 :: DGraph
dg2) =
                DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
insGSig DGraph
dg' (String -> NodeName -> NodeName
extName "XCoerced" NodeName
nn) DGOrigin
DGLogicCoercion (G_sign -> (NodeSig, DGraph)) -> G_sign -> (NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
gmor
              dg3 :: DGraph
dg3 = DGraph
-> GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Node
-> Node
-> DGraph
insLink DGraph
dg2 GMorphism
gmor DGLinkType
globalDef DGLinkOrigin
SeeTarget Node
n Node
m
          (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeSig
ms, DGraph
dg3)
        Just (_, t :: Node
t, _) ->
            (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Node -> G_sign -> NodeSig
NodeSig Node
t (G_sign -> NodeSig) -> G_sign -> NodeSig
forall a b. (a -> b) -> a -> b
$ G_theory -> G_sign
signOf (G_theory -> G_sign) -> G_theory -> G_sign
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory (DGNodeLab -> G_theory) -> DGNodeLab -> G_theory
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> DGNodeLab
labDG DGraph
dg' Node
t, DGraph
dg')

insGTheory :: DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)
insGTheory :: DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)
insGTheory dg :: DGraph
dg name :: NodeName
name orig :: DGOrigin
orig (G_theory lid :: lid
lid syn :: Maybe IRI
syn sig :: ExtSign sign symbol
sig ind :: SigId
ind sens :: ThSens sentence (AnyComorphism, BasicProof)
sens tind :: ThId
tind) =
    let (sgMap :: Map SigId G_sign
sgMap, s :: SigId
s) = DGraph -> (Map SigId G_sign, SigId)
sigMapI DGraph
dg
        (tMap :: Map ThId G_theory
tMap, t :: ThId
t) = DGraph -> (Map ThId G_theory, ThId)
thMapI DGraph
dg
        nind :: SigId
nind = if SigId
ind SigId -> SigId -> Bool
forall a. Eq a => a -> a -> Bool
== SigId
startSigId then SigId -> SigId
forall a. Enum a => a -> a
succ SigId
s else SigId
ind
        tb :: Bool
tb = ThId
tind ThId -> ThId -> Bool
forall a. Eq a => a -> a -> Bool
== ThId
startThId Bool -> Bool -> Bool
&& Bool -> Bool
not (ThSens sentence (AnyComorphism, BasicProof) -> Bool
forall k a. Map k a -> Bool
Map.null ThSens sentence (AnyComorphism, BasicProof)
sens)
        ntind :: ThId
ntind = if Bool
tb then ThId -> ThId
forall a. Enum a => a -> a
succ ThId
t else ThId
tind
        nsig :: G_sign
nsig = lid -> ExtSign sign symbol -> 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 lid
lid ExtSign sign symbol
sig SigId
nind
        nth :: G_theory
nth = 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
nind ThSens sentence (AnyComorphism, BasicProof)
sens ThId
ntind
        node_contents :: DGNodeLab
node_contents = NodeName -> DGOrigin -> G_theory -> DGNodeLab
newNodeLab NodeName
name DGOrigin
orig G_theory
nth
        node :: Node
node = DGraph -> Node
getNewNodeDG DGraph
dg
    in (Node -> G_sign -> NodeSig
NodeSig Node
node G_sign
nsig,
        (if Bool
tb then Map ThId G_theory -> DGraph -> DGraph
setThMapDG (Map ThId G_theory -> DGraph -> DGraph)
-> Map ThId G_theory -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ ThId -> G_theory -> Map ThId G_theory -> Map ThId G_theory
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (ThId -> ThId
forall a. Enum a => a -> a
succ ThId
t) G_theory
nth Map ThId G_theory
tMap else DGraph -> DGraph
forall a. a -> a
id) (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$
        (if SigId
ind SigId -> SigId -> Bool
forall a. Eq a => a -> a -> Bool
== SigId
startSigId
         then Map SigId G_sign -> DGraph -> DGraph
setSigMapDG (Map SigId G_sign -> DGraph -> DGraph)
-> Map SigId G_sign -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ SigId -> G_sign -> Map SigId G_sign -> Map SigId G_sign
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SigId -> SigId
forall a. Enum a => a -> a
succ SigId
s) G_sign
nsig Map SigId G_sign
sgMap else DGraph -> DGraph
forall a. a -> a
id)
         (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ LNode DGNodeLab -> DGraph -> DGraph
insNodeDG (Node
node, DGNodeLab
node_contents) DGraph
dg)

insGSig :: DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
insGSig :: DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
insGSig dg :: DGraph
dg name :: NodeName
name orig :: DGOrigin
orig (G_sign lid :: lid
lid sig :: ExtSign sign symbol
sig ind :: SigId
ind) =
    DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)
insGTheory DGraph
dg NodeName
name DGOrigin
orig (G_theory -> (NodeSig, DGraph)) -> G_theory -> (NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ lid -> ExtSign sign symbol -> SigId -> 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 -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory lid
lid ExtSign sign symbol
sig SigId
ind

insLink :: DGraph -> GMorphism -> DGLinkType -> DGLinkOrigin -> Node -> Node
        -> DGraph
insLink :: DGraph
-> GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Node
-> Node
-> DGraph
insLink dg :: DGraph
dg (GMorphism cid :: cid
cid sign :: ExtSign sign1 symbol1
sign si :: SigId
si mor :: morphism2
mor mi :: MorId
mi) ty :: DGLinkType
ty orig :: DGLinkOrigin
orig n :: Node
n t :: Node
t =
    let (sgMap :: Map SigId G_sign
sgMap, s :: SigId
s) = DGraph -> (Map SigId G_sign, SigId)
sigMapI DGraph
dg
        (mrMap :: Map MorId G_morphism
mrMap, m :: MorId
m) = DGraph -> (Map MorId G_morphism, MorId)
morMapI DGraph
dg
        nsi :: SigId
nsi = if SigId
si SigId -> SigId -> Bool
forall a. Eq a => a -> a -> Bool
== SigId
startSigId then SigId -> SigId
forall a. Enum a => a -> a
succ SigId
s else SigId
si
        nmi :: MorId
nmi = if MorId
mi MorId -> MorId -> Bool
forall a. Eq a => a -> a -> Bool
== MorId
startMorId then MorId -> MorId
forall a. Enum a => a -> a
succ MorId
m else MorId
mi
        nmor :: GMorphism
nmor = cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
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
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism cid
cid ExtSign sign1 symbol1
sign SigId
nsi morphism2
mor MorId
nmi
        link :: DGLinkLab
link = GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink GMorphism
nmor DGLinkType
ty DGLinkOrigin
orig
    in (if MorId
mi MorId -> MorId -> Bool
forall a. Eq a => a -> a -> Bool
== MorId
startMorId then Map MorId G_morphism -> DGraph -> DGraph
setMorMapDG (Map MorId G_morphism -> DGraph -> DGraph)
-> Map MorId G_morphism -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ MorId -> G_morphism -> Map MorId G_morphism -> Map MorId G_morphism
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (MorId -> MorId
forall a. Enum a => a -> a
succ MorId
m)
         (GMorphism -> G_morphism
toG_morphism GMorphism
nmor) Map MorId G_morphism
mrMap else DGraph -> DGraph
forall a. a -> a
id) (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$
       (if SigId
si SigId -> SigId -> Bool
forall a. Eq a => a -> a -> Bool
== SigId
startSigId then Map SigId G_sign -> DGraph -> DGraph
setSigMapDG (Map SigId G_sign -> DGraph -> DGraph)
-> Map SigId G_sign -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ SigId -> G_sign -> Map SigId G_sign -> Map SigId G_sign
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SigId -> SigId
forall a. Enum a => a -> a
succ SigId
s)
        (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
nsi) Map SigId G_sign
sgMap else DGraph -> DGraph
forall a. a -> a
id)
       (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ (Node, Node, DGLinkLab) -> DGraph -> DGraph
insLEdgeNubDG (Node
n, Node
t, DGLinkLab
link) DGraph
dg

createConsLink :: LinkKind -> Conservativity -> LogicGraph -> DGraph
  -> MaybeNode -> NodeSig -> DGLinkOrigin -> Result DGraph
createConsLink :: LinkKind
-> Conservativity
-> LogicGraph
-> DGraph
-> MaybeNode
-> NodeSig
-> DGLinkOrigin
-> Result DGraph
createConsLink lk :: LinkKind
lk conser :: Conservativity
conser lg :: LogicGraph
lg dg :: DGraph
dg nsig :: MaybeNode
nsig (NodeSig node :: Node
node gsig :: G_sign
gsig) orig :: DGLinkOrigin
orig = case MaybeNode
nsig of
    EmptyNode _ | Conservativity
conser Conservativity -> Conservativity -> Bool
forall a. Eq a => a -> a -> Bool
== Conservativity
None -> DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return DGraph
dg
    _ -> case MaybeNode
nsig of
      JustNode (NodeSig n :: Node
n sig :: G_sign
sig) -> do
        GMorphism
incl <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lg G_sign
sig G_sign
gsig
        DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph -> Result DGraph) -> DGraph -> Result DGraph
forall a b. (a -> b) -> a -> b
$ DGraph
-> GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Node
-> Node
-> DGraph
insLink DGraph
dg GMorphism
incl
              (Scope -> LinkKind -> ConsStatus -> DGLinkType
ScopedLink Scope
Global LinkKind
lk (ConsStatus -> DGLinkType) -> ConsStatus -> DGLinkType
forall a b. (a -> b) -> a -> b
$ Conservativity -> ConsStatus
mkConsStatus Conservativity
conser) DGLinkOrigin
orig Node
n Node
node
      EmptyNode _ -> -- add conservativity to the target node
        DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph -> Result DGraph) -> DGraph -> Result DGraph
forall a b. (a -> b) -> a -> b
$ let lbl :: DGNodeLab
lbl = DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
node
        in if DGNodeLab -> Bool
isDGRef DGNodeLab
lbl then DGraph
dg else
         (DGraph, DGNodeLab) -> DGraph
forall a b. (a, b) -> a
fst ((DGraph, DGNodeLab) -> DGraph) -> (DGraph, DGNodeLab) -> DGraph
forall a b. (a -> b) -> a -> b
$ LNode DGNodeLab -> DGraph -> (DGraph, DGNodeLab)
labelNodeDG
           (Node
node, DGNodeLab
lbl
            { nodeInfo :: DGNodeInfo
nodeInfo =
               (DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
lbl)
                 { node_cons_status :: ConsStatus
node_cons_status = case DGNodeLab -> ConsStatus
getNodeConsStatus DGNodeLab
lbl of
                     ConsStatus c :: Conservativity
c d :: Conservativity
d th :: ThmLinkStatus
th -> Conservativity -> Conservativity -> ThmLinkStatus -> ConsStatus
ConsStatus (Conservativity -> Conservativity -> Conservativity
forall a. Ord a => a -> a -> a
max Conservativity
c Conservativity
conser) Conservativity
d ThmLinkStatus
th }}) DGraph
dg

getNamedSpec :: SPEC_NAME -> LibName -> DGraph -> LibEnv
  -> Result (ExtGenSig, (LibName, DGraph, LNode DGNodeLab))
getNamedSpec :: IRI
-> LibName
-> DGraph
-> LibEnv
-> Result (ExtGenSig, (LibName, DGraph, LNode DGNodeLab))
getNamedSpec sp :: IRI
sp ln :: LibName
ln dg :: DGraph
dg libenv :: LibEnv
libenv = case IRI -> DGraph -> Maybe GlobalEntry
lookupGlobalEnvDG IRI
sp DGraph
dg of
          Just (SpecEntry s :: ExtGenSig
s@(ExtGenSig (GenSig _ ps :: [NodeSig]
ps _) (NodeSig n :: Node
n _))) -> do
            Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([NodeSig] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NodeSig]
ps)
              (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> IRI -> Result ()
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "base theory must not be parameterized" IRI
sp
            let t :: (LibName, DGraph, LNode DGNodeLab)
t@(refLib :: LibName
refLib, refDG :: DGraph
refDG, (_, lbl :: DGNodeLab
lbl)) = LibEnv
-> LibName -> DGraph -> Node -> (LibName, DGraph, LNode DGNodeLab)
lookupRefNode LibEnv
libenv LibName
ln DGraph
dg Node
n
                refTok :: IRI
refTok = NodeName -> IRI
getName (NodeName -> IRI) -> NodeName -> IRI
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> NodeName
dgn_name DGNodeLab
lbl
            Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (IRI
sp IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== IRI
refTok)
              (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Result ()
appendDiags [DiagKind -> String -> IRI -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "renamed base theory" IRI
sp]
            if LibName
refLib LibName -> LibName -> Bool
forall a. Eq a => a -> a -> Bool
== LibName
ln then (ExtGenSig, (LibName, DGraph, LNode DGNodeLab))
-> Result (ExtGenSig, (LibName, DGraph, LNode DGNodeLab))
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtGenSig
s, (LibName, DGraph, LNode DGNodeLab)
t) else
                case IRI -> DGraph -> Maybe GlobalEntry
lookupGlobalEnvDG IRI
refTok DGraph
refDG of
                  Just (SpecEntry s2 :: ExtGenSig
s2) -> (ExtGenSig, (LibName, DGraph, LNode DGNodeLab))
-> Result (ExtGenSig, (LibName, DGraph, LNode DGNodeLab))
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtGenSig
s2, (LibName, DGraph, LNode DGNodeLab)
t)
                  _ -> String
-> IRI -> Result (ExtGenSig, (LibName, DGraph, LNode DGNodeLab))
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "theory reference error" IRI
sp
          _ -> String
-> IRI -> Result (ExtGenSig, (LibName, DGraph, LNode DGNodeLab))
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "unknown theory" IRI
sp

anaSublogic :: HetcatsOpts -> LogicDescr -> LibName -> DGraph -> LibEnv
  -> LogicGraph
  -> Result (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
anaSublogic :: HetcatsOpts
-> LogicDescr
-> LibName
-> DGraph
-> LibEnv
-> LogicGraph
-> Result
     (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
anaSublogic _opts :: HetcatsOpts
_opts itm :: LogicDescr
itm ln :: LibName
ln dg :: DGraph
dg libenv :: LibEnv
libenv lG :: LogicGraph
lG
  = case LogicDescr
itm of
  LogicDescr (Logic_name lt :: String
lt ms :: Maybe Token
ms mt :: Maybe IRI
mt) _ _ -> do
    logN :: AnyLogic
logN@(Logic lid :: lid
lid) <- String -> String -> LogicGraph -> Result AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> String -> LogicGraph -> m AnyLogic
lookupLogic "" String
lt LogicGraph
lG
    Maybe G_sublogics
mgs <- case Maybe Token
ms of
      Nothing -> Maybe G_sublogics -> Result (Maybe G_sublogics)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe G_sublogics
forall a. Maybe a
Nothing
      Just subL :: Token
subL -> do
        let s :: String
s = Token -> String
tokStr Token
subL
        case lid -> String -> Maybe sublogics
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 -> String -> Maybe sublogics
parseSublogic lid
lid String
s of
          Nothing -> String -> Result (Maybe G_sublogics)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result (Maybe G_sublogics))
-> String -> Result (Maybe G_sublogics)
forall a b. (a -> b) -> a -> b
$ "unknown sublogic of logic " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AnyLogic -> String
forall a. Show a => a -> String
show AnyLogic
logN
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
          Just sl :: sublogics
sl ->
            if sublogics -> String
forall l. SublogicName l => l -> String
sublogicName (lid -> sublogics
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 -> sublogics
top_sublogic lid
lid) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
s then do
              () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
warning () ("not a proper sublogic: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s) (Range -> Result ()) -> Range -> Result ()
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
subL
              Maybe G_sublogics -> Result (Maybe G_sublogics)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe G_sublogics
forall a. Maybe a
Nothing
              else Maybe G_sublogics -> Result (Maybe G_sublogics)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe G_sublogics -> Result (Maybe G_sublogics))
-> Maybe G_sublogics -> Result (Maybe G_sublogics)
forall a b. (a -> b) -> a -> b
$ G_sublogics -> Maybe G_sublogics
forall a. a -> Maybe a
Just (G_sublogics -> Maybe G_sublogics)
-> G_sublogics -> Maybe G_sublogics
forall a b. (a -> b) -> a -> b
$ lid -> sublogics -> G_sublogics
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 -> sublogics -> G_sublogics
G_sublogics lid
lid sublogics
sl
    let logicLibN :: LibName
logicLibN = String -> LibName
emptyLibName "Logics"
        lG1 :: LogicGraph
lG1 = Maybe G_sublogics -> LogicGraph -> LogicGraph
setCurSublogic Maybe G_sublogics
mgs (LogicGraph -> LogicGraph) -> LogicGraph -> LogicGraph
forall a b. (a -> b) -> a -> b
$ LogicDescr -> LogicGraph -> LogicGraph
setLogicName LogicDescr
itm LogicGraph
lG
    case Maybe IRI
mt of
      Nothing -> (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
-> Result
     (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab))
forall a. Maybe a
Nothing, LogicGraph
lG1 { currentTargetBase :: Maybe (LibName, String)
currentTargetBase = Maybe (LibName, String)
forall a. Maybe a
Nothing })
      Just sp :: IRI
sp -> do
        let ssp :: String
ssp = IRI -> String
iriToStringUnsecure IRI
sp
        (s :: ExtGenSig
s, t :: (LibName, DGraph, LNode DGNodeLab)
t@(libName :: LibName
libName, _, (_, lbl :: DGNodeLab
lbl))) <- case LibName -> LibEnv -> Maybe DGraph
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LibName
logicLibN LibEnv
libenv of
          Just dg2 :: DGraph
dg2 | LibName
logicLibN LibName -> LibName -> Bool
forall a. Eq a => a -> a -> Bool
/= LibName
ln -> IRI
-> LibName
-> DGraph
-> LibEnv
-> Result (ExtGenSig, (LibName, DGraph, LNode DGNodeLab))
getNamedSpec IRI
sp LibName
logicLibN DGraph
dg2 LibEnv
libenv
          _ -> IRI
-> LibName
-> DGraph
-> LibEnv
-> Result (ExtGenSig, (LibName, DGraph, LNode DGNodeLab))
getNamedSpec IRI
sp LibName
ln DGraph
dg LibEnv
libenv
        case G_theory -> G_sublogics
sublogicOfTh (G_theory -> G_sublogics) -> G_theory -> G_sublogics
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
globOrLocTh DGNodeLab
lbl of
          gs2 :: G_sublogics
gs2@(G_sublogics lid2 :: lid
lid2 _) -> do
            Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (AnyLogic
logN AnyLogic -> AnyLogic -> Bool
forall a. Eq a => a -> a -> Bool
== lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid2)
              (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result ()) -> String -> Result ()
forall a b. (a -> b) -> a -> b
$ "the logic of '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ssp
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ "' is '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid2
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ "' and not '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ AnyLogic -> String -> String
forall a. Show a => a -> String -> String
shows AnyLogic
logN "'!"
            case Maybe G_sublogics
mgs of
              Nothing -> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Just gs :: G_sublogics
gs -> Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (G_sublogics -> G_sublogics -> Bool
isSublogic G_sublogics
gs2 G_sublogics
gs)
                (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result ()) -> String -> Result ()
forall a b. (a -> b) -> a -> b
$ "theory '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ssp
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ "' has sublogic '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ G_sublogics -> String -> String
forall a. Show a => a -> String -> String
shows G_sublogics
gs2 "' and not '"
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ G_sublogics -> String -> String
forall a. Show a => a -> String -> String
shows G_sublogics
gs "'!"
            let sbMap :: Map AnyLogic SublogicBasedTheories
sbMap = LogicGraph -> Map AnyLogic SublogicBasedTheories
sublogicBasedTheories LogicGraph
lG1
                lMap :: SublogicBasedTheories
lMap = SublogicBasedTheories
-> AnyLogic
-> Map AnyLogic SublogicBasedTheories
-> SublogicBasedTheories
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault SublogicBasedTheories
forall k a. Map k a
Map.empty AnyLogic
logN Map AnyLogic SublogicBasedTheories
sbMap
                nName :: String
nName = DGNodeLab -> String
getDGNodeName DGNodeLab
lbl
            SublogicBasedTheories
nMap <- case IRI -> SublogicBasedTheories -> Maybe (LibName, String)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IRI
sp SublogicBasedTheories
lMap of
              Nothing -> SublogicBasedTheories -> Result SublogicBasedTheories
forall (m :: * -> *) a. Monad m => a -> m a
return (SublogicBasedTheories -> Result SublogicBasedTheories)
-> SublogicBasedTheories -> Result SublogicBasedTheories
forall a b. (a -> b) -> a -> b
$ IRI
-> (LibName, String)
-> SublogicBasedTheories
-> SublogicBasedTheories
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
sp (LibName
libName, String
nName) SublogicBasedTheories
lMap
              Just (prevLib :: LibName
prevLib, prevName :: String
prevName) -> do
                Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (LibName
libName LibName -> LibName -> Bool
forall a. Eq a => a -> a -> Bool
== LibName
prevLib)
                  (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result ()) -> String -> Result ()
forall a b. (a -> b) -> a -> b
$ "theory '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ssp
                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ "' should come from library '"
                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ LibName -> String -> String
forall a. Pretty a => a -> String -> String
showDoc LibName
prevLib "' and not from '"
                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ LibName -> String -> String
forall a. Pretty a => a -> String -> String
showDoc LibName
libName "'!"
                Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (String
nName String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
prevName)
                  (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result ()) -> String -> Result ()
forall a b. (a -> b) -> a -> b
$ "the original theory name for '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ssp
                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ "' should be '"
                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
prevName String -> String -> String
forall a. [a] -> [a] -> [a]
++ "' and not '"
                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nName String -> String -> String
forall a. [a] -> [a] -> [a]
++ "'!"
                SublogicBasedTheories -> Result SublogicBasedTheories
forall (m :: * -> *) a. Monad m => a -> m a
return SublogicBasedTheories
lMap
            (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
-> Result
     (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ExtGenSig, (LibName, DGraph, LNode DGNodeLab))
-> Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab))
forall a. a -> Maybe a
Just (ExtGenSig
s, (LibName, DGraph, LNode DGNodeLab)
t), LogicGraph
lG1
              { sublogicBasedTheories :: Map AnyLogic SublogicBasedTheories
sublogicBasedTheories = AnyLogic
-> SublogicBasedTheories
-> Map AnyLogic SublogicBasedTheories
-> Map AnyLogic SublogicBasedTheories
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert AnyLogic
logN SublogicBasedTheories
nMap Map AnyLogic SublogicBasedTheories
sbMap
              , currentTargetBase :: Maybe (LibName, String)
currentTargetBase = (LibName, String) -> Maybe (LibName, String)
forall a. a -> Maybe a
Just (LibName
libName, String
nName) })
  _ -> (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
-> Result
     (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab))
forall a. Maybe a
Nothing, LogicGraph
lG)

anaSpecTop :: Conservativity -> Bool -> LogicGraph -> LibEnv -> LibName -> DGraph
  -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> SPEC -> Range
  -> Result (SPEC, NodeSig, DGraph)
anaSpecTop :: Conservativity
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpecTop conser :: Conservativity
conser addSyms :: Bool
addSyms lg :: LogicGraph
lg libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg nsig :: MaybeNode
nsig name :: NodeName
name opts :: HetcatsOpts
opts eo :: ExpOverrides
eo sp :: SPEC
sp pos :: Range
pos =
 if Conservativity
conser Conservativity -> Conservativity -> Bool
forall a. Eq a => a -> a -> Bool
== Conservativity
None Bool -> Bool -> Bool
|| case SPEC
sp of
      -- for these cases def-links are re-used
    Basic_spec _ _ -> Bool
True
    Closed_spec _ _ -> Bool
True
    Spec_inst {} -> Bool
True
    Group _ _ -> Bool
True -- in this case we recurse
    _ -> Bool
False
    then Conservativity
-> Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpecAux Conservativity
conser Bool
addSyms Bool
True LogicGraph
lg LibEnv
libEnv LibName
ln 
                    DGraph
dg MaybeNode
nsig NodeName
name HetcatsOpts
opts ExpOverrides
eo SPEC
sp Range
pos 
    else do
  let provenThmLink :: LinkKind
provenThmLink =
        ThmLinkStatus -> LinkKind
ThmLink (ThmLinkStatus -> LinkKind) -> ThmLinkStatus -> LinkKind
forall a b. (a -> b) -> a -> b
$ DGRule -> ProofBasis -> ThmLinkStatus
Proven (String -> DGRule
DGRule "static analysis") ProofBasis
emptyProofBasis
  (rsp :: SPEC
rsp, ns :: NodeSig
ns, rdg :: DGraph
rdg) <- Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
addSyms Bool
True LogicGraph
lg LibEnv
libEnv LibName
ln 
                            DGraph
dg MaybeNode
nsig NodeName
name HetcatsOpts
opts ExpOverrides
eo SPEC
sp Range
pos
  DGraph
ndg <- LinkKind
-> Conservativity
-> LogicGraph
-> DGraph
-> MaybeNode
-> NodeSig
-> DGLinkOrigin
-> Result DGraph
createConsLink LinkKind
provenThmLink Conservativity
conser LogicGraph
lg DGraph
rdg MaybeNode
nsig NodeSig
ns DGLinkOrigin
SeeTarget
  (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (SPEC
rsp, NodeSig
ns, DGraph
ndg)

anaFreeOrCofreeSpec :: Bool -> LogicGraph -> LibEnv -> HetcatsOpts -> LibName -> DGraph
  -> MaybeNode -> NodeName -> FreeOrCofree -> ExpOverrides -> Annoted SPEC
  -> Range -> Result (Annoted SPEC, NodeSig, DGraph)
anaFreeOrCofreeSpec :: Bool
-> LogicGraph
-> LibEnv
-> HetcatsOpts
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> FreeOrCofree
-> ExpOverrides
-> Annoted SPEC
-> Range
-> Result (Annoted SPEC, NodeSig, DGraph)
anaFreeOrCofreeSpec addSyms :: Bool
addSyms lg :: LogicGraph
lg libEnv :: LibEnv
libEnv opts :: HetcatsOpts
opts ln :: LibName
ln dg :: DGraph
dg nsig :: MaybeNode
nsig name :: NodeName
name dglType :: FreeOrCofree
dglType eo :: ExpOverrides
eo asp :: Annoted SPEC
asp pos :: Range
pos =
  Range
-> Result (Annoted SPEC, NodeSig, DGraph)
-> Result (Annoted SPEC, NodeSig, DGraph)
forall a. Range -> Result a -> Result a
adjustPos Range
pos (Result (Annoted SPEC, NodeSig, DGraph)
 -> Result (Annoted SPEC, NodeSig, DGraph))
-> Result (Annoted SPEC, NodeSig, DGraph)
-> Result (Annoted SPEC, NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ do
      let sp :: SPEC
sp = Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
asp
          iPos :: Range
iPos = SPEC -> Range
forall a. GetRange a => a -> Range
getRange SPEC
sp
      (sp' :: SPEC
sp', NodeSig n' :: Node
n' gsigma :: G_sign
gsigma, dg' :: DGraph
dg') <-
          Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
addSyms Bool
True LogicGraph
lg LibEnv
libEnv LibName
ln 
                  DGraph
dg MaybeNode
nsig (String -> NodeName -> NodeName
extName (FreeOrCofree -> String
forall a. Show a => a -> String
show FreeOrCofree
dglType) NodeName
name) HetcatsOpts
opts ExpOverrides
eo
            SPEC
sp Range
iPos
      let (ns :: NodeSig
ns@(NodeSig node :: Node
node _), dg2 :: DGraph
dg2) =
              DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
insGSig DGraph
dg' (Range -> NodeName -> NodeName
setSrcRange Range
pos NodeName
name) (FreeOrCofree -> DGOrigin
DGFreeOrCofree FreeOrCofree
dglType) G_sign
gsigma
          nsigma :: G_sign
nsigma = case MaybeNode
nsig of
            EmptyNode cl :: AnyLogic
cl -> AnyLogic -> G_sign
emptyG_sign AnyLogic
cl
            JustNode nds :: NodeSig
nds -> NodeSig -> G_sign
getSig NodeSig
nds
      GMorphism
incl <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lg G_sign
nsigma G_sign
gsigma
      (Annoted SPEC, NodeSig, DGraph)
-> Result (Annoted SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted SPEC
sp' Annoted SPEC
asp, NodeSig
ns,
              DGraph
-> GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Node
-> Node
-> DGraph
insLink DGraph
dg2 GMorphism
incl (FreeOrCofree -> MaybeNode -> DGLinkType
FreeOrCofreeDefLink FreeOrCofree
dglType MaybeNode
nsig)
              DGLinkOrigin
SeeTarget Node
n' Node
node)

{- | analyze a SPEC. The first Bool Parameter determines if incoming symbols shall
be ignored while the second determines if the nodes should be optimized away for specifications without parameters. The options are needed to check: shall only the structure be
analysed? -}
anaSpec :: Bool -> Bool-> LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> NodeName
  -> HetcatsOpts -> ExpOverrides -> SPEC -> Range
  -> Result (SPEC, NodeSig, DGraph)
anaSpec :: Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec = Conservativity
-> Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpecAux Conservativity
None

anaSpecAux :: Conservativity -> Bool -> Bool 
  -> LogicGraph -> LibEnv -> LibName -> DGraph
  -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> SPEC -> Range
  -> Result (SPEC, NodeSig, DGraph)
anaSpecAux :: Conservativity
-> Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpecAux conser :: Conservativity
conser addSyms :: Bool
addSyms optNodes :: Bool
optNodes lg :: LogicGraph
lg 
           libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg nsig :: MaybeNode
nsig name :: NodeName
name opts :: HetcatsOpts
opts eo :: ExpOverrides
eo sp :: SPEC
sp rg :: Range
rg = case SPEC
sp of
  Basic_spec (G_basic_spec lid :: lid
lid bspec :: basic_spec
bspec) pos :: Range
pos -> Range
-> Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall a. Range -> Result a -> Result a
adjustPos Range
pos (Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph))
-> Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ do
       let curLogic :: AnyLogic
curLogic = lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid
           curSL :: Maybe G_sublogics
curSL = LogicGraph -> Maybe G_sublogics
currentSublogic LogicGraph
lg
           bsSL :: G_sublogics
bsSL = lid -> sublogics -> G_sublogics
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 -> sublogics -> G_sublogics
G_sublogics lid
lid (sublogics -> G_sublogics) -> sublogics -> G_sublogics
forall a b. (a -> b) -> a -> b
$ basic_spec -> sublogics
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic basic_spec
bspec
       Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> (G_sublogics -> Bool) -> Maybe G_sublogics -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (G_sublogics -> G_sublogics -> Bool
`isProperSublogic` G_sublogics
bsSL) Maybe G_sublogics
curSL)
         (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result ()) -> String -> Result ()
forall a b. (a -> b) -> a -> b
$ "sublogic expected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> (G_sublogics -> String) -> Maybe G_sublogics -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" G_sublogics -> String
forall a. Show a => a -> String
show Maybe G_sublogics
curSL
               String -> String -> String
forall a. [a] -> [a] -> [a]
++ " found: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ G_sublogics -> String
forall a. Show a => a -> String
show G_sublogics
bsSL
       (nsig' :: MaybeNode
nsig', dg0 :: DGraph
dg0) <- LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> AnyLogic
-> Result (MaybeNode, DGraph)
coerceMaybeNode LogicGraph
lg LibEnv
libEnv LibName
ln DGraph
dg MaybeNode
nsig NodeName
name AnyLogic
curLogic
       G_sign lid' :: lid
lid' sigma' :: ExtSign sign symbol
sigma' _ <- G_sign -> Result G_sign
forall (m :: * -> *) a. Monad m => a -> m a
return (G_sign -> Result G_sign) -> G_sign -> Result G_sign
forall a b. (a -> b) -> a -> b
$ case MaybeNode
nsig' of
           EmptyNode cl :: AnyLogic
cl -> AnyLogic -> G_sign
emptyG_sign AnyLogic
cl
           JustNode ns :: NodeSig
ns -> NodeSig -> G_sign
getSig NodeSig
ns
       ExtSign sig :: sign
sig sys :: Set symbol
sys <-
           lid
-> lid
-> String
-> ExtSign sign symbol
-> Result (ExtSign sign 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 (m :: * -> *).
(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,
 MonadFail m) =>
lid1
-> lid2
-> String
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid' lid
lid "Analysis of basic spec" ExtSign sign symbol
sigma'
       (bspec' :: basic_spec
bspec', ExtSign sigma_complete :: sign
sigma_complete sysd :: Set symbol
sysd, ax :: [Named sentence]
ax) <-
          if HetcatsOpts -> Bool
isStructured HetcatsOpts
opts
           then (basic_spec, ExtSign sign symbol, [Named sentence])
-> Result (basic_spec, ExtSign sign symbol, [Named sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return (basic_spec
bspec, sign -> ExtSign sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign (sign -> ExtSign sign symbol) -> sign -> ExtSign sign symbol
forall a b. (a -> b) -> a -> b
$ lid -> sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign
empty_signature lid
lid, [])
           else
             let res :: Result (basic_spec, ExtSign sign symbol, [Named sentence])
res@(Result ds :: [Diagnosis]
ds mb :: Maybe (basic_spec, ExtSign sign symbol, [Named sentence])
mb) = lid
-> IRI
-> LibName
-> basic_spec
-> sign
-> GlobalAnnos
-> Result (basic_spec, ExtSign sign symbol, [Named sentence])
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid
-> IRI
-> LibName
-> basic_spec
-> sign
-> GlobalAnnos
-> Result (basic_spec, ExtSign sign symbol, [Named sentence])
extBasicAnalysis lid
lid (NodeName -> IRI
getName NodeName
name)
                   LibName
ln basic_spec
bspec sign
sig (GlobalAnnos
 -> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
-> GlobalAnnos
-> Result (basic_spec, ExtSign sign symbol, [Named sentence])
forall a b. (a -> b) -> a -> b
$ DGraph -> GlobalAnnos
globalAnnos DGraph
dg0
             in case Maybe (basic_spec, ExtSign sign symbol, [Named sentence])
mb of
               Nothing | [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds ->
                 String
-> Result (basic_spec, ExtSign sign symbol, [Named sentence])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "basic analysis failed without giving a reason"
               _ -> Result (basic_spec, ExtSign sign symbol, [Named sentence])
res
       sign
diffSig <- case lid -> sign -> sign -> Result sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result sign
signatureDiff lid
lid sign
sigma_complete sign
sig of
         Result _ (Just ds :: sign
ds) -> sign -> Result sign
forall (m :: * -> *) a. Monad m => a -> m a
return sign
ds
         _ -> sign -> String -> Range -> Result sign
forall a. a -> String -> Range -> Result a
warning sign
sigma_complete
           "signature difference could not be computed using full one" Range
pos
       let gsysd :: Set G_symbol
gsysd = (symbol -> G_symbol) -> Set symbol -> Set G_symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (lid -> symbol -> G_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 -> symbol -> G_symbol
G_symbol lid
lid) Set symbol
sysd
           (ns :: NodeSig
ns, dg' :: DGraph
dg') = DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)
insGTheory DGraph
dg0 (Range -> NodeName -> NodeName
setSrcRange Range
rg NodeName
name)
             (Maybe G_basic_spec -> G_sign -> Set G_symbol -> DGOrigin
DGBasicSpec (G_basic_spec -> Maybe G_basic_spec
forall a. a -> Maybe a
Just (G_basic_spec -> Maybe G_basic_spec)
-> G_basic_spec -> Maybe G_basic_spec
forall a b. (a -> b) -> a -> b
$ lid -> basic_spec -> G_basic_spec
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 -> basic_spec -> G_basic_spec
G_basic_spec lid
lid basic_spec
bspec')
             (lid -> ExtSign sign symbol -> 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 lid
lid (sign -> ExtSign sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign
diffSig) SigId
startSigId) Set G_symbol
gsysd)
               (G_theory -> (NodeSig, DGraph)) -> G_theory -> (NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ 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 (LogicGraph -> Maybe IRI
currentSyntax LogicGraph
lg) (sign -> Set symbol -> ExtSign sign symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign sign
sigma_complete
               (Set symbol -> ExtSign sign symbol)
-> Set symbol -> ExtSign sign symbol
forall a b. (a -> b) -> a -> b
$ Set symbol -> Set symbol -> Set symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
                     (if Bool
addSyms then Set symbol -> Set symbol -> Set symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set symbol
sys Set symbol
sysd else Set symbol
sysd)
               (Set symbol -> Set symbol) -> Set symbol -> Set symbol
forall a b. (a -> b) -> a -> b
$ lid -> sign -> Set symbol
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid
lid sign
sigma_complete)
             SigId
startSigId ([Named sentence] -> ThSens sentence (AnyComorphism, BasicProof)
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named sentence]
ax) ThId
startThId
       DGraph
dg'' <- LinkKind
-> Conservativity
-> LogicGraph
-> DGraph
-> MaybeNode
-> NodeSig
-> DGLinkOrigin
-> Result DGraph
createConsLink LinkKind
DefLink Conservativity
conser LogicGraph
lg DGraph
dg' MaybeNode
nsig' NodeSig
ns DGLinkOrigin
DGLinkExtension
       (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_basic_spec -> Range -> SPEC
Basic_spec (lid -> basic_spec -> G_basic_spec
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 -> basic_spec -> G_basic_spec
G_basic_spec lid
lid basic_spec
bspec') Range
pos, NodeSig
ns, DGraph
dg'')
  EmptySpec pos :: Range
pos -> case MaybeNode
nsig of
      EmptyNode _ -> do
        () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
warning () "empty spec" Range
pos
        let (ns :: NodeSig
ns, dg' :: DGraph
dg') = DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
insGSig DGraph
dg (Range -> NodeName -> NodeName
setSrcRange Range
rg NodeName
name) DGOrigin
DGEmpty
              (MaybeNode -> G_sign
getMaybeSig MaybeNode
nsig)
        (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (SPEC
sp, NodeSig
ns, DGraph
dg')
        {- anaSpec should be changed to return a MaybeNode!
           Then this duplicate dummy node could be avoided.
           Also empty unions could be treated then -}
      JustNode ns :: NodeSig
ns -> (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (SPEC
sp, NodeSig
ns , DGraph
dg)
  Translation asp :: Annoted SPEC
asp ren :: RENAMING
ren ->
   do let sp1 :: SPEC
sp1 = Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
asp
          rPos :: Range
rPos = RENAMING -> Range
forall a. GetRange a => a -> Range
getRange RENAMING
ren
      (sp1' :: SPEC
sp1', ns' :: NodeSig
ns'@(NodeSig n' :: Node
n' gsigma :: G_sign
gsigma), dg' :: DGraph
dg') <- 
        Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
addSyms Bool
optNodes LogicGraph
lg LibEnv
libEnv LibName
ln DGraph
dg MaybeNode
nsig
         (String -> NodeName -> NodeName
extName "Translation" NodeName
name) HetcatsOpts
opts ExpOverrides
eo SPEC
sp1 Range
rPos
      GMorphism
mor <- LogicGraph
-> MaybeNode
-> G_sign
-> HetcatsOpts
-> RENAMING
-> Result GMorphism
anaRenaming LogicGraph
lg MaybeNode
nsig G_sign
gsigma HetcatsOpts
opts RENAMING
ren
      -- ??? check that mor is identity on local env
      Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (GMorphism -> Bool
forall object morphism.
Category object morphism =>
morphism -> Bool
isIdentity GMorphism
mor) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
warning ()
         ("nothing renamed by:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ RENAMING -> String -> String
forall a. Pretty a => a -> String -> String
showDoc RENAMING
ren "") Range
rPos
      (fs :: NodeSig
fs, dgf :: DGraph
dgf) <- if GMorphism -> Bool
forall object morphism.
Category object morphism =>
morphism -> Bool
isIdentity GMorphism
mor Bool -> Bool -> Bool
&& NodeName -> Bool
isInternal NodeName
name then (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeSig
ns', DGraph
dg')
         else do
         let (ns :: NodeSig
ns@(NodeSig node :: Node
node _), dg'' :: DGraph
dg'') = DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
insGSig DGraph
dg' (Range -> NodeName -> NodeName
setSrcRange Range
rg NodeName
name)
               (Renamed -> DGOrigin
DGTranslation (Renamed -> DGOrigin) -> Renamed -> DGOrigin
forall a b. (a -> b) -> a -> b
$ RENAMING -> Renamed
Renamed RENAMING
ren) (G_sign -> (NodeSig, DGraph)) -> G_sign -> (NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
mor
           -- ??? too simplistic for non-comorphism inter-logic translations
         (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeSig
ns, DGraph
-> GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Node
-> Node
-> DGraph
insLink DGraph
dg'' GMorphism
mor DGLinkType
globalDef DGLinkOrigin
SeeTarget Node
n' Node
node)
      (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> RENAMING -> SPEC
Translation (SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted SPEC
sp1' Annoted SPEC
asp) RENAMING
ren, NodeSig
fs, DGraph
dgf)
  Extraction asp :: Annoted SPEC
asp extr :: EXTRACTION
extr -> do
    let sp0 :: SPEC
sp0 = Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
asp
        rname :: NodeName
rname = String -> NodeName -> NodeName
extName "Extension" NodeName
name
    (sp' :: SPEC
sp', nsig' :: NodeSig
nsig', dg0 :: DGraph
dg0) <- Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
addSyms Bool
optNodes LogicGraph
lg LibEnv
libEnv 
                                 LibName
ln DGraph
dg MaybeNode
nsig NodeName
rname HetcatsOpts
opts ExpOverrides
eo SPEC
sp0 Range
rg
    (ns' :: NodeSig
ns', dg1 :: DGraph
dg1) <- LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> NodeSig
-> NodeName
-> Range
-> EXTRACTION
-> Result (NodeSig, DGraph)
anaExtraction LogicGraph
lg LibEnv
libEnv LibName
ln DGraph
dg0 NodeSig
nsig' NodeName
name Range
rg EXTRACTION
extr
    (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> EXTRACTION -> SPEC
Extraction (SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted SPEC
sp' Annoted SPEC
asp) EXTRACTION
extr, NodeSig
ns', DGraph
dg1)
  Reduction asp :: Annoted SPEC
asp restr :: RESTRICTION
restr ->
   do let sp1 :: SPEC
sp1 = Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
asp
          rname :: NodeName
rname = String -> NodeName -> NodeName
extName "Restriction" NodeName
name
      (sp1' :: SPEC
sp1', ns0 :: NodeSig
ns0, dg0 :: DGraph
dg0) <- Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
addSyms Bool
optNodes LogicGraph
lg LibEnv
libEnv 
                           LibName
ln DGraph
dg MaybeNode
nsig NodeName
rname HetcatsOpts
opts ExpOverrides
eo SPEC
sp1 Range
rg
      AnyLogic
rLid <- RESTRICTION -> Result AnyLogic
getRestrLogic RESTRICTION
restr
      p1 :: (NodeSig, DGraph)
p1@(NodeSig n' :: Node
n' gsigma' :: G_sign
gsigma', dg' :: DGraph
dg') <- LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> NodeSig
-> NodeName
-> AnyLogic
-> Result (NodeSig, DGraph)
coerceNode LogicGraph
lg LibEnv
libEnv LibName
ln DGraph
dg0 NodeSig
ns0 NodeName
rname AnyLogic
rLid
      (hmor :: GMorphism
hmor, tmor :: Maybe GMorphism
tmor) <- LogicGraph
-> G_sign
-> G_sign
-> HetcatsOpts
-> RESTRICTION
-> Result (GMorphism, Maybe GMorphism)
anaRestriction LogicGraph
lg (MaybeNode -> G_sign
getMaybeSig MaybeNode
nsig) G_sign
gsigma' HetcatsOpts
opts RESTRICTION
restr
      let noRename :: Bool
noRename = Bool -> (GMorphism -> Bool) -> Maybe GMorphism -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True GMorphism -> Bool
forall object morphism.
Category object morphism =>
morphism -> Bool
isIdentity Maybe GMorphism
tmor
          noHide :: Bool
noHide = GMorphism -> Bool
forall object morphism.
Category object morphism =>
morphism -> Bool
isIdentity GMorphism
hmor
      Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
noHide (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ (if Bool
noRename then () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
warning else () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
hint) ()
        ("nothing hidden by:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ RESTRICTION -> String -> String
forall a. Pretty a => a -> String -> String
showDoc RESTRICTION
restr "") (Range -> Result ()) -> Range -> Result ()
forall a b. (a -> b) -> a -> b
$ RESTRICTION -> Range
forall a. GetRange a => a -> Range
getRange RESTRICTION
restr
      p2 :: (NodeSig, DGraph)
p2@(NodeSig node1 :: Node
node1 _, dg2 :: DGraph
dg2) <- if Bool
noHide Bool -> Bool -> Bool
&& NodeName -> Bool
isInternal NodeName
name then (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeSig, DGraph)
p1
          else do
           let trgSg :: G_sign
trgSg = GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
dom GMorphism
hmor
               hidSyms :: Set G_symbol
hidSyms = Set G_symbol -> Set G_symbol -> Set G_symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (G_sign -> Set G_symbol
symsOfGsign G_sign
gsigma')
                 (Set G_symbol -> Set G_symbol) -> Set G_symbol -> Set G_symbol
forall a b. (a -> b) -> a -> b
$ G_sign -> Set G_symbol
symsOfGsign G_sign
trgSg
               orig :: DGOrigin
orig = MaybeRestricted -> Set G_symbol -> DGOrigin
DGRestriction (RESTRICTION -> MaybeRestricted
Restricted RESTRICTION
restr) Set G_symbol
hidSyms
               (ns :: NodeSig
ns@(NodeSig node :: Node
node _), dg'' :: DGraph
dg'') = DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
insGSig DGraph
dg'
                 (if Bool
noRename then NodeName
name else String -> NodeName -> NodeName
extName "Hiding" NodeName
name)
                 DGOrigin
orig G_sign
trgSg
           -- ??? too simplistic for non-comorphism inter-logic reductions
           (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeSig
ns, DGraph
-> GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Node
-> Node
-> DGraph
insLink DGraph
dg'' GMorphism
hmor DGLinkType
HidingDefLink DGLinkOrigin
SeeTarget Node
n' Node
node)
      {- we treat hiding and revealing differently
      in order to keep the dg as simple as possible -}
      (fs :: NodeSig
fs, dgf :: DGraph
dgf) <- case Maybe GMorphism
tmor of
        Just tmor' :: GMorphism
tmor' | Bool -> Bool
not Bool
noRename -> do
          let (ns :: NodeSig
ns@(NodeSig node2 :: Node
node2 _), dg3 :: DGraph
dg3) =
                   DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
insGSig DGraph
dg2 NodeName
name DGOrigin
DGRevealTranslation (G_sign -> (NodeSig, DGraph)) -> G_sign -> (NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
tmor'
          (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeSig
ns, DGraph
-> GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Node
-> Node
-> DGraph
insLink DGraph
dg3 GMorphism
tmor' DGLinkType
globalDef DGLinkOrigin
SeeTarget Node
node1 Node
node2)
        Nothing -> (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeSig, DGraph)
p2
        _ -> (NodeSig, DGraph) -> String -> Range -> Result (NodeSig, DGraph)
forall a. a -> String -> Range -> Result a
hint (NodeSig, DGraph)
p2 ("nothing renamed by:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ RESTRICTION -> String -> String
forall a. Pretty a => a -> String -> String
showDoc RESTRICTION
restr "")
            (Range -> Result (NodeSig, DGraph))
-> Range -> Result (NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ RESTRICTION -> Range
forall a. GetRange a => a -> Range
getRange RESTRICTION
restr
      (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> RESTRICTION -> SPEC
Reduction (SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted SPEC
sp1' Annoted SPEC
asp) RESTRICTION
restr, NodeSig
fs, DGraph
dgf)
  Filtering asp :: Annoted SPEC
asp filtering :: FILTERING
filtering -> do
       let sp1 :: SPEC
sp1 = Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
asp
           rname :: NodeName
rname = String -> NodeName -> NodeName
extName "Filtering" NodeName
name
       (sp' :: SPEC
sp', nsig' :: NodeSig
nsig', dg' :: DGraph
dg') <- Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
addSyms Bool
optNodes LogicGraph
lg LibEnv
libEnv LibName
ln DGraph
dg 
                                    MaybeNode
nsig NodeName
rname HetcatsOpts
opts ExpOverrides
eo SPEC
sp1 Range
rg
       (nf :: NodeSig
nf, dgF :: DGraph
dgF) <- LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> NodeSig
-> NodeName
-> FILTERING
-> Result (NodeSig, DGraph)
anaFiltering LogicGraph
lg LibEnv
libEnv LibName
ln DGraph
dg' NodeSig
nsig' NodeName
name FILTERING
filtering
       (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> FILTERING -> SPEC
Filtering (SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted SPEC
sp' Annoted SPEC
asp) FILTERING
filtering, NodeSig
nf, DGraph
dgF)
       -- error "analysis of filterings not yet implemented"
  Minimization asp :: Annoted SPEC
asp (Mini kw :: Token
kw cm :: [IRI]
cm cv :: [IRI]
cv poss :: Range
poss) -> do
      (nasp :: Annoted SPEC
nasp, nsig' :: NodeSig
nsig', dg' :: DGraph
dg') <- Bool
-> LogicGraph
-> LibEnv
-> HetcatsOpts
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> FreeOrCofree
-> ExpOverrides
-> Annoted SPEC
-> Range
-> Result (Annoted SPEC, NodeSig, DGraph)
anaFreeOrCofreeSpec Bool
addSyms LogicGraph
lg LibEnv
libEnv HetcatsOpts
opts LibName
ln DGraph
dg MaybeNode
nsig
        NodeName
name FreeOrCofree
Minimize ExpOverrides
eo Annoted SPEC
asp Range
poss
      (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> MINIMIZATION -> SPEC
Minimization Annoted SPEC
nasp (Token -> [IRI] -> [IRI] -> Range -> MINIMIZATION
Mini Token
kw [IRI]
cm [IRI]
cv Range
poss), NodeSig
nsig', DGraph
dg')
  Union asps :: [Annoted SPEC]
asps pos :: Range
pos -> do
    (newAsps :: [Annoted SPEC]
newAsps, _, ns :: NodeSig
ns, dg' :: DGraph
dg') <- Range
-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
forall a. Range -> Result a -> Result a
adjustPos Range
pos (Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
 -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph))
-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> [Annoted SPEC]
-> Range
-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
anaUnion Bool
addSyms LogicGraph
lg LibEnv
libEnv LibName
ln DGraph
dg MaybeNode
nsig
      NodeName
name HetcatsOpts
opts ExpOverrides
eo [Annoted SPEC]
asps Range
rg
    (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted SPEC] -> Range -> SPEC
Union [Annoted SPEC]
newAsps Range
pos, NodeSig
ns, DGraph
dg')
  Intersection asps :: [Annoted SPEC]
asps pos :: Range
pos -> do
    (newAsps :: [Annoted SPEC]
newAsps, _, ns :: NodeSig
ns, dg' :: DGraph
dg') <- Range
-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
forall a. Range -> Result a -> Result a
adjustPos Range
pos (Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
 -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph))
-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> [Annoted SPEC]
-> Range
-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
anaIntersect Bool
addSyms LogicGraph
lg LibEnv
libEnv LibName
ln DGraph
dg MaybeNode
nsig
      NodeName
name HetcatsOpts
opts ExpOverrides
eo [Annoted SPEC]
asps Range
rg
    (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted SPEC] -> Range -> SPEC
Intersection [Annoted SPEC]
newAsps Range
pos, NodeSig
ns, DGraph
dg')
  Extension asps :: [Annoted SPEC]
asps pos :: Range
pos -> do
   let namedSps :: [(NodeName, Annoted SPEC)]
namedSps = ((Annoted SPEC, Node) -> (NodeName, Annoted SPEC))
-> [(Annoted SPEC, Node)] -> [(NodeName, Annoted SPEC)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (asp :: Annoted SPEC
asp, n :: Node
n) ->
         let nn :: NodeName
nn = Node -> NodeName -> NodeName
incBy Node
n (String -> NodeName -> NodeName
extName "Extension" NodeName
name) in
         if Node
n Node -> Node -> Bool
forall a. Ord a => a -> a -> Bool
< [Annoted SPEC] -> Node
forall (t :: * -> *) a. Foldable t => t a -> Node
length [Annoted SPEC]
asps then (NodeName
nn, Annoted SPEC
asp)
         else (NodeName
name { xpath :: [XPathPart]
xpath = NodeName -> [XPathPart]
xpath NodeName
nn }, Annoted SPEC
asp)) ([(Annoted SPEC, Node)] -> [(NodeName, Annoted SPEC)])
-> [(Annoted SPEC, Node)] -> [(NodeName, Annoted SPEC)]
forall a b. (a -> b) -> a -> b
$ [Annoted SPEC] -> [(Annoted SPEC, Node)]
forall a. [a] -> [(a, Node)]
number [Annoted SPEC]
asps
   (sps' :: [SPEC]
sps', nsig1' :: MaybeNode
nsig1', dg1 :: DGraph
dg1, _, _) <- (([SPEC], MaybeNode, DGraph, Conservativity, Bool)
 -> (NodeName, Annoted SPEC)
 -> Result ([SPEC], MaybeNode, DGraph, Conservativity, Bool))
-> ([SPEC], MaybeNode, DGraph, Conservativity, Bool)
-> [(NodeName, Annoted SPEC)]
-> Result ([SPEC], MaybeNode, DGraph, Conservativity, Bool)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (LogicGraph
-> LibEnv
-> HetcatsOpts
-> ExpOverrides
-> LibName
-> Range
-> ([SPEC], MaybeNode, DGraph, Conservativity, Bool)
-> (NodeName, Annoted SPEC)
-> Result ([SPEC], MaybeNode, DGraph, Conservativity, Bool)
anaExtension LogicGraph
lg LibEnv
libEnv HetcatsOpts
opts ExpOverrides
eo LibName
ln Range
pos)
     ([], MaybeNode
nsig, DGraph
dg, Conservativity
conser, Bool
addSyms) [(NodeName, Annoted SPEC)]
namedSps
   case MaybeNode
nsig1' of
       EmptyNode _ -> String -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "empty extension"
       JustNode nsig1 :: NodeSig
nsig1 -> (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted SPEC] -> Range -> SPEC
Extension ((SPEC -> Annoted SPEC -> Annoted SPEC)
-> [SPEC] -> [Annoted SPEC] -> [Annoted SPEC]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted
                          ([SPEC] -> [SPEC]
forall a. [a] -> [a]
reverse [SPEC]
sps') [Annoted SPEC]
asps)
                                 Range
pos, NodeSig
nsig1, DGraph
dg1)
  Free_spec asp :: Annoted SPEC
asp poss :: Range
poss -> do
      (nasp :: Annoted SPEC
nasp, nsig' :: NodeSig
nsig', dg' :: DGraph
dg') <- Bool
-> LogicGraph
-> LibEnv
-> HetcatsOpts
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> FreeOrCofree
-> ExpOverrides
-> Annoted SPEC
-> Range
-> Result (Annoted SPEC, NodeSig, DGraph)
anaFreeOrCofreeSpec Bool
addSyms LogicGraph
lg LibEnv
libEnv HetcatsOpts
opts LibName
ln DGraph
dg MaybeNode
nsig
        NodeName
name FreeOrCofree
Free ExpOverrides
eo Annoted SPEC
asp Range
poss
      (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> Range -> SPEC
Free_spec Annoted SPEC
nasp Range
poss, NodeSig
nsig', DGraph
dg')
  Cofree_spec asp :: Annoted SPEC
asp poss :: Range
poss -> do
      (nasp :: Annoted SPEC
nasp, nsig' :: NodeSig
nsig', dg' :: DGraph
dg') <- Bool
-> LogicGraph
-> LibEnv
-> HetcatsOpts
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> FreeOrCofree
-> ExpOverrides
-> Annoted SPEC
-> Range
-> Result (Annoted SPEC, NodeSig, DGraph)
anaFreeOrCofreeSpec Bool
addSyms LogicGraph
lg LibEnv
libEnv HetcatsOpts
opts LibName
ln DGraph
dg MaybeNode
nsig
        NodeName
name FreeOrCofree
Cofree ExpOverrides
eo Annoted SPEC
asp Range
poss
      (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> Range -> SPEC
Cofree_spec Annoted SPEC
nasp Range
poss, NodeSig
nsig', DGraph
dg')
  Minimize_spec asp :: Annoted SPEC
asp poss :: Range
poss -> do
      (nasp :: Annoted SPEC
nasp, nsig' :: NodeSig
nsig', dg' :: DGraph
dg') <- Bool
-> LogicGraph
-> LibEnv
-> HetcatsOpts
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> FreeOrCofree
-> ExpOverrides
-> Annoted SPEC
-> Range
-> Result (Annoted SPEC, NodeSig, DGraph)
anaFreeOrCofreeSpec Bool
addSyms LogicGraph
lg LibEnv
libEnv HetcatsOpts
opts LibName
ln DGraph
dg MaybeNode
nsig
          NodeName
name FreeOrCofree
Minimize ExpOverrides
eo Annoted SPEC
asp Range
poss
      (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> Range -> SPEC
Minimize_spec Annoted SPEC
nasp Range
poss, NodeSig
nsig', DGraph
dg')
  Local_spec asp :: Annoted SPEC
asp asp' :: Annoted SPEC
asp' poss :: Range
poss -> Range
-> Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall a. Range -> Result a -> Result a
adjustPos Range
poss (Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph))
-> Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ do
      let sp1 :: SPEC
sp1 = Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
asp
          pos1 :: Range
pos1 = SPEC -> Range
forall a. GetRange a => a -> Range
getRange SPEC
sp1
          sp1' :: SPEC
sp1' = Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
asp'
          pos1' :: Range
pos1' = SPEC -> Range
forall a. GetRange a => a -> Range
getRange SPEC
sp1'
          lname :: NodeName
lname = String -> NodeName -> NodeName
extName "Local" NodeName
name
      (sp2 :: SPEC
sp2, nsig' :: NodeSig
nsig'@(NodeSig _ gsig1 :: G_sign
gsig1), dg' :: DGraph
dg') <-
        Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
False Bool
True LogicGraph
lg LibEnv
libEnv LibName
ln 
                DGraph
dg MaybeNode
nsig (String -> NodeName -> NodeName
extName "Spec" NodeName
lname) HetcatsOpts
opts ExpOverrides
eo SPEC
sp1 Range
pos1
      (sp2' :: SPEC
sp2', NodeSig n'' :: Node
n'' gsig2 :: G_sign
gsig2@(G_sign lid2 :: lid
lid2 sigma2 :: ExtSign sign symbol
sigma2 _), dg'' :: DGraph
dg'') <- 
          Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
False Bool
True LogicGraph
lg LibEnv
libEnv LibName
ln 
                DGraph
dg' (NodeSig -> MaybeNode
JustNode NodeSig
nsig') (String -> NodeName -> NodeName
extName "Within" NodeName
lname) HetcatsOpts
opts ExpOverrides
eo SPEC
sp1' Range
pos1'
      let gSigN :: G_sign
gSigN = MaybeNode -> G_sign
getMaybeSig MaybeNode
nsig
      (G_sign lid :: lid
lid sigmaN :: ExtSign sign symbol
sigmaN _, _) <- LogicGraph -> G_sign -> AnyLogic -> Result (G_sign, AnyComorphism)
gSigCoerce LogicGraph
lg G_sign
gSigN (lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid2)
      ExtSign sign symbol
sigma <- lid
-> lid
-> String
-> ExtSign sign symbol
-> Result (ExtSign sign 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 (m :: * -> *).
(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,
 MonadFail m) =>
lid1
-> lid2
-> String
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid lid
lid2 "Analysis of local spec1" ExtSign sign symbol
sigmaN
      (G_sign lid' :: lid
lid' sigma' :: ExtSign sign symbol
sigma' _, _) <- LogicGraph -> G_sign -> AnyLogic -> Result (G_sign, AnyComorphism)
gSigCoerce LogicGraph
lg G_sign
gsig1 (lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid2)
      ExtSign sign symbol
sigma1 <- lid
-> lid
-> String
-> ExtSign sign symbol
-> Result (ExtSign sign 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 (m :: * -> *).
(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,
 MonadFail m) =>
lid1
-> lid2
-> String
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid' lid
lid2 "Analysis of local spec2" ExtSign sign symbol
sigma'
      let sys :: Set symbol
sys = lid -> ExtSign sign symbol -> 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 =>
lid -> ExtSign sign symbol -> Set symbol
ext_sym_of lid
lid2 ExtSign sign symbol
sigma
          sys1 :: Set symbol
sys1 = lid -> ExtSign sign symbol -> 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 =>
lid -> ExtSign sign symbol -> Set symbol
ext_sym_of lid
lid2 ExtSign sign symbol
sigma1
          sys2 :: Set symbol
sys2 = lid -> ExtSign sign symbol -> 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 =>
lid -> ExtSign sign symbol -> Set symbol
ext_sym_of lid
lid2 ExtSign sign symbol
sigma2
      morphism
mor3 <- if HetcatsOpts -> Bool
isStructured HetcatsOpts
opts then morphism -> Result morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtSign sign symbol -> morphism
forall symbol sign morphism.
(Ord symbol, Category sign morphism) =>
ExtSign sign symbol -> morphism
ext_ide ExtSign sign symbol
sigma2)
               else lid -> Set symbol -> ExtSign sign symbol -> Result morphism
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 -> Set symbol -> ExtSign sign symbol -> Result morphism
ext_cogenerated_sign lid
lid2
                      (Set symbol
sys1 Set symbol -> Set symbol -> Set symbol
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set symbol
sys) ExtSign sign symbol
sigma2
      let sigma3 :: sign
sigma3 = morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
dom morphism
mor3
          gsigma3 :: G_sign
gsigma3 = lid -> ExtSign sign symbol -> 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 lid
lid2 (lid -> sign -> ExtSign sign 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 -> ExtSign sign symbol
makeExtSign lid
lid2 sign
sigma3) SigId
startSigId
          sys3 :: Set symbol
sys3 = lid -> sign -> Set symbol
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid
lid2 sign
sigma3
      Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (HetcatsOpts -> Bool
isStructured HetcatsOpts
opts
              Bool -> Bool -> Bool
|| Set symbol
sys2 Set symbol -> Set symbol -> Set symbol
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set symbol
sys1 Set symbol -> Set symbol -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set symbol
sys3)
        (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
plain_error () (
          "illegal use of locally declared symbols: "
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set symbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc ((Set symbol
sys2 Set symbol -> Set symbol -> Set symbol
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set symbol
sys1) Set symbol -> Set symbol -> Set symbol
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set symbol
sys3) "")
         Range
poss
      let hidSyms :: Set G_symbol
hidSyms = Set G_symbol -> Set G_symbol -> Set G_symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (G_sign -> Set G_symbol
symsOfGsign G_sign
gsig2) (Set G_symbol -> Set G_symbol) -> Set G_symbol -> Set G_symbol
forall a b. (a -> b) -> a -> b
$ G_sign -> Set G_symbol
symsOfGsign G_sign
gsigma3
          orig :: DGOrigin
orig = MaybeRestricted -> Set G_symbol -> DGOrigin
DGRestriction MaybeRestricted
NoRestriction Set G_symbol
hidSyms
          (ns :: NodeSig
ns@(NodeSig node :: Node
node _), dg2 :: DGraph
dg2) = DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
insGSig DGraph
dg'' NodeName
name DGOrigin
orig G_sign
gsigma3
      (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> Annoted SPEC -> Range -> SPEC
Local_spec (SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted SPEC
sp2 Annoted SPEC
asp)
                         (SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted SPEC
sp2' Annoted SPEC
asp')
                         Range
poss, NodeSig
ns,
              DGraph
-> GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Node
-> Node
-> DGraph
insLink DGraph
dg2 (G_sign -> G_morphism -> GMorphism
gEmbed2 G_sign
gsigma3 (G_morphism -> GMorphism) -> G_morphism -> GMorphism
forall a b. (a -> b) -> a -> b
$ lid -> morphism -> G_morphism
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 -> morphism -> G_morphism
mkG_morphism lid
lid2 morphism
mor3)
                  DGLinkType
HidingDefLink DGLinkOrigin
SeeTarget Node
n'' Node
node)
  Closed_spec asp :: Annoted SPEC
asp pos :: Range
pos -> Range
-> Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall a. Range -> Result a -> Result a
adjustPos Range
pos (Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph))
-> Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ do
      let sp1 :: SPEC
sp1 = Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
asp
          pos1 :: Range
pos1 = SPEC -> Range
forall a. GetRange a => a -> Range
getRange SPEC
sp1
          l :: AnyLogic
l = MaybeNode -> AnyLogic
getLogic MaybeNode
nsig
      -- analyse spec with empty local env
      (sp' :: SPEC
sp', NodeSig n' :: Node
n' gsigma' :: G_sign
gsigma', dg' :: DGraph
dg') <- Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
False Bool
True LogicGraph
lg LibEnv
libEnv LibName
ln DGraph
dg
        (AnyLogic -> MaybeNode
EmptyNode AnyLogic
l) (String -> NodeName -> NodeName
extName "Closed" NodeName
name) HetcatsOpts
opts ExpOverrides
eo SPEC
sp1 Range
pos1
      G_sign
gsigma2 <- LogicGraph -> Bool -> MaybeNode -> G_sign -> Result G_sign
gsigUnionMaybe LogicGraph
lg Bool
addSyms MaybeNode
nsig G_sign
gsigma'
      let (ns :: NodeSig
ns@(NodeSig node :: Node
node _), dg2 :: DGraph
dg2) = DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
insGSig DGraph
dg' NodeName
name DGOrigin
DGClosed G_sign
gsigma2
      GMorphism
incl2 <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lg G_sign
gsigma' G_sign
gsigma2
      let dg3 :: DGraph
dg3 = DGraph
-> GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Node
-> Node
-> DGraph
insLink DGraph
dg2 GMorphism
incl2 DGLinkType
globalDef DGLinkOrigin
SeeTarget Node
n' Node
node
      DGraph
dg4 <- LinkKind
-> Conservativity
-> LogicGraph
-> DGraph
-> MaybeNode
-> NodeSig
-> DGLinkOrigin
-> Result DGraph
createConsLink LinkKind
DefLink Conservativity
conser LogicGraph
lg DGraph
dg3 MaybeNode
nsig NodeSig
ns DGLinkOrigin
DGLinkClosedLenv
      (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> Range -> SPEC
Closed_spec (SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted SPEC
sp' Annoted SPEC
asp) Range
pos, NodeSig
ns, DGraph
dg4)
  Qualified_spec lognm :: LogicDescr
lognm asp :: Annoted SPEC
asp pos :: Range
pos -> Range
-> Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall a. Range -> Result a -> Result a
adjustPos Range
pos (Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph))
-> Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ do
      let newLG :: LogicGraph
newLG = LogicDescr -> LogicGraph -> LogicGraph
setLogicName LogicDescr
lognm LogicGraph
lg
      AnyLogic
l <- String -> LogicGraph -> Result AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyLogic
lookupCurrentLogic "Qualified_spec" LogicGraph
newLG
      let newNSig :: MaybeNode
newNSig = case MaybeNode
nsig of
            EmptyNode _ -> AnyLogic -> MaybeNode
EmptyNode AnyLogic
l
            _ -> MaybeNode
nsig
          qname :: NodeName
qname = String -> NodeName -> NodeName
extName "Qualified" NodeName
name
      (sp' :: SPEC
sp', ns' :: NodeSig
ns', dg' :: DGraph
dg') <- Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
addSyms Bool
optNodes LogicGraph
newLG LibEnv
libEnv LibName
ln 
                                 DGraph
dg MaybeNode
newNSig NodeName
qname HetcatsOpts
opts ExpOverrides
eo
        (Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
asp) Range
pos
      (ns :: NodeSig
ns, dg2 :: DGraph
dg2) <- LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> NodeSig
-> NodeName
-> AnyLogic
-> Result (NodeSig, DGraph)
coerceNode LogicGraph
lg LibEnv
libEnv LibName
ln DGraph
dg' NodeSig
ns' NodeName
qname AnyLogic
l
      (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (LogicDescr -> Annoted SPEC -> Range -> SPEC
Qualified_spec LogicDescr
lognm Annoted SPEC
asp { item :: SPEC
item = SPEC
sp' } Range
pos, NodeSig
ns, DGraph
dg2)
  Group asp :: Annoted SPEC
asp pos :: Range
pos -> do
      (sp' :: SPEC
sp', nsig' :: NodeSig
nsig', dg' :: DGraph
dg') <-
          Conservativity
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpecTop Conservativity
conser Bool
addSyms LogicGraph
lg LibEnv
libEnv LibName
ln 
                     DGraph
dg MaybeNode
nsig NodeName
name HetcatsOpts
opts ExpOverrides
eo (Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
asp) Range
rg
      (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> Range -> SPEC
Group (SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted SPEC
sp' Annoted SPEC
asp) Range
pos, NodeSig
nsig', DGraph
dg')
  Spec_inst spname' :: IRI
spname' afitargs :: [Annoted FIT_ARG]
afitargs mImp :: Maybe IRI
mImp pos0 :: Range
pos0 -> do
   IRI
spname <- GlobalAnnos -> ExpOverrides -> IRI -> Result IRI
expCurieR (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
spname'
   let pos :: Range
pos = if [Annoted FIT_ARG] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted FIT_ARG]
afitargs then IRI -> Range
iriPos IRI
spname else Range
pos0
   Range
-> Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall a. Range -> Result a -> Result a
adjustPos Range
pos (Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph))
-> Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ case IRI -> DGraph -> Maybe GlobalEntry
lookupGlobalEnvDG IRI
spname DGraph
dg of
    Just (SpecEntry gs :: ExtGenSig
gs@(ExtGenSig (GenSig _ params :: [NodeSig]
params _)
                        body :: NodeSig
body@(NodeSig nB :: Node
nB gsigmaB :: G_sign
gsigmaB))) ->
     case ([Annoted FIT_ARG] -> Node
forall (t :: * -> *) a. Foldable t => t a -> Node
length [Annoted FIT_ARG]
afitargs, [NodeSig] -> Node
forall (t :: * -> *) a. Foldable t => t a -> Node
length [NodeSig]
params) of
      -- the case without parameters leads to a simpler dg
      (0, 0) -> case MaybeNode
nsig of
          -- if the node shall not be named and the logic does not change,
        EmptyNode _ | NodeName -> Bool
isInternal NodeName
name Bool -> Bool -> Bool
&& Bool
optNodes -> do
          DGraph
dg2 <- LinkKind
-> Conservativity
-> LogicGraph
-> DGraph
-> MaybeNode
-> NodeSig
-> DGLinkOrigin
-> Result DGraph
createConsLink LinkKind
DefLink Conservativity
conser LogicGraph
lg DGraph
dg MaybeNode
nsig NodeSig
body DGLinkOrigin
SeeTarget
             -- then just return the body
          (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (SPEC
sp, NodeSig
body, DGraph
dg2)
             -- otherwise, we need to create a new one
        _ -> do
           G_sign
gsigma <- LogicGraph -> Bool -> MaybeNode -> G_sign -> Result G_sign
gsigUnionMaybe LogicGraph
lg Bool
addSyms MaybeNode
nsig G_sign
gsigmaB
           let (fsig :: NodeSig
fsig@(NodeSig node :: Node
node _), dg2 :: DGraph
dg2) =
                 DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
insGSig DGraph
dg NodeName
name (IRI -> DGOrigin
DGInst IRI
spname) G_sign
gsigma
           GMorphism
incl <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lg G_sign
gsigmaB G_sign
gsigma
           let dg3 :: DGraph
dg3 = case MaybeNode
nsig of
                 JustNode (NodeSig nI :: Node
nI _) | Node
nI Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
nB -> DGraph
dg2
                 _ -> DGraph
-> GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Node
-> Node
-> DGraph
insLink DGraph
dg2 GMorphism
incl DGLinkType
globalDef (IRI -> DGLinkOrigin
DGLinkMorph IRI
spname) Node
nB Node
node
           DGraph
dg4 <- LinkKind
-> Conservativity
-> LogicGraph
-> DGraph
-> MaybeNode
-> NodeSig
-> DGLinkOrigin
-> Result DGraph
createConsLink LinkKind
DefLink Conservativity
conser LogicGraph
lg DGraph
dg3 MaybeNode
nsig NodeSig
fsig DGLinkOrigin
SeeTarget
           (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (SPEC
sp, NodeSig
fsig, DGraph
dg4)
      -- now the case with parameters
      (la :: Node
la, lp :: Node
lp) | Node
la Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
lp -> do
       (ffitargs :: [Annoted FIT_ARG]
ffitargs, dg' :: DGraph
dg', (morDelta :: GMorphism
morDelta, gsigmaA :: G_sign
gsigmaA, ns :: NodeSig
ns@(NodeSig nA :: Node
nA gsigmaRes :: G_sign
gsigmaRes))) <-
               LogicGraph
-> LibEnv
-> HetcatsOpts
-> ExpOverrides
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> IRI
-> ExtGenSig
-> [Annoted FIT_ARG]
-> Result ([Annoted FIT_ARG], DGraph, (GMorphism, G_sign, NodeSig))
anaAllFitArgs LogicGraph
lg LibEnv
libEnv HetcatsOpts
opts ExpOverrides
eo LibName
ln DGraph
dg MaybeNode
nsig NodeName
name IRI
spname ExtGenSig
gs [Annoted FIT_ARG]
afitargs
       GMorphism cid :: cid
cid _ _ _ _ <- GMorphism -> Result GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return GMorphism
morDelta
       GMorphism
morDelta' <- case MaybeNode
nsig of
         EmptyNode _
           | G_sign -> AnyLogic
logicOfGsign G_sign
gsigmaA AnyLogic -> AnyLogic -> Bool
forall a. Eq a => a -> a -> Bool
== G_sign -> AnyLogic
logicOfGsign G_sign
gsigmaRes
             -> GMorphism -> Result GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return GMorphism
morDelta
         _ -> LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lg G_sign
gsigmaA G_sign
gsigmaRes Result GMorphism
-> (GMorphism -> Result GMorphism) -> Result GMorphism
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= GMorphism -> GMorphism -> Result GMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp GMorphism
morDelta
       (_, imor :: AnyComorphism
imor) <- LogicGraph -> G_sign -> AnyLogic -> Result (G_sign, AnyComorphism)
gSigCoerce LogicGraph
lg G_sign
gsigmaB (AnyLogic -> Result (G_sign, AnyComorphism))
-> AnyLogic -> Result (G_sign, AnyComorphism)
forall a b. (a -> b) -> a -> b
$ lid1 -> AnyLogic
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 -> AnyLogic
Logic (lid1 -> AnyLogic) -> lid1 -> AnyLogic
forall a b. (a -> b) -> a -> b
$ 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
       GMorphism
tmor <- AnyComorphism -> G_sign -> Result GMorphism
gEmbedComorphism AnyComorphism
imor G_sign
gsigmaB
       GMorphism
morDelta'' <- GMorphism -> GMorphism -> Result GMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp GMorphism
tmor GMorphism
morDelta'
       let dg4 :: DGraph
dg4 = case MaybeNode
nsig of
             JustNode (NodeSig nI :: Node
nI _) | Node
nI Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
nB -> DGraph
dg'
             _ -> DGraph
-> GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Node
-> Node
-> DGraph
insLink DGraph
dg' GMorphism
morDelta'' DGLinkType
globalDef (IRI -> DGLinkOrigin
DGLinkMorph IRI
spname) Node
nB Node
nA
       DGraph
dg5 <- LinkKind
-> Conservativity
-> LogicGraph
-> DGraph
-> MaybeNode
-> NodeSig
-> DGLinkOrigin
-> Result DGraph
createConsLink LinkKind
DefLink Conservativity
conser LogicGraph
lg DGraph
dg4 MaybeNode
nsig NodeSig
ns DGLinkOrigin
SeeTarget
       (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (IRI -> [Annoted FIT_ARG] -> Maybe IRI -> Range -> SPEC
Spec_inst IRI
spname [Annoted FIT_ARG]
ffitargs Maybe IRI
mImp Range
pos, NodeSig
ns, DGraph
dg5)
       | Bool
otherwise -> IRI -> Node -> Node -> Range -> Result (SPEC, NodeSig, DGraph)
forall a. IRI -> Node -> Node -> Range -> Result a
instMismatchError IRI
spname Node
lp Node
la Range
pos
    _ | [Annoted FIT_ARG] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted FIT_ARG]
afitargs -> do
     () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
warning () ("ignoring missing spec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ IRI -> String -> String
forall a. Pretty a => a -> String -> String
showDoc IRI
spname' "") Range
pos
     case MaybeNode
nsig of
      EmptyNode _ -> do -- copied from EmptySpec case
        let (ns :: NodeSig
ns, dg' :: DGraph
dg') = DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
insGSig DGraph
dg NodeName
name DGOrigin
DGEmpty (MaybeNode -> G_sign
getMaybeSig MaybeNode
nsig)
        (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (SPEC
sp, NodeSig
ns, DGraph
dg')
      JustNode ns :: NodeSig
ns -> (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (SPEC
sp, NodeSig
ns , DGraph
dg)
    _ -> String -> IRI -> Result (SPEC, NodeSig, DGraph)
forall a. String -> IRI -> Result a
notFoundError "structured spec" IRI
spname

  -- analyse "data SPEC1 SPEC2"
  Data lD :: AnyLogic
lD@(Logic lidD :: lid
lidD) lP :: AnyLogic
lP asp1 :: Annoted SPEC
asp1 asp2 :: Annoted SPEC
asp2 pos :: Range
pos -> Range
-> Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall a. Range -> Result a -> Result a
adjustPos Range
pos (Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph))
-> Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ do
      let sp1 :: SPEC
sp1 = Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
asp1
          pos1 :: Range
pos1 = SPEC -> Range
forall a. GetRange a => a -> Range
getRange SPEC
sp1
          sp2 :: SPEC
sp2 = Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
asp2
      {- look for the inclusion comorphism from the current logic's data logic
      into the current logic itself -}
      AnyComorphism
c <- LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
logicInclusion LogicGraph
lg AnyLogic
lD AnyLogic
lP
      let dname :: NodeName
dname = String -> NodeName -> NodeName
extName "Data" NodeName
name
      -- analyse SPEC1
      (sp1' :: SPEC
sp1', ns' :: NodeSig
ns', dg' :: DGraph
dg') <- Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
False Bool
True (String -> LogicGraph -> LogicGraph
setCurLogic (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lidD) LogicGraph
lg)
         LibEnv
libEnv LibName
ln DGraph
dg (AnyLogic -> MaybeNode
EmptyNode AnyLogic
lD) NodeName
dname HetcatsOpts
opts ExpOverrides
eo SPEC
sp1 Range
pos1
      -- force the result to be in the data logic
      (ns'' :: NodeSig
ns'', dg'' :: DGraph
dg'') <- LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> NodeSig
-> NodeName
-> AnyLogic
-> Result (NodeSig, DGraph)
coerceNode LogicGraph
lg LibEnv
libEnv LibName
ln DGraph
dg' NodeSig
ns' (String -> NodeName -> NodeName
extName "Qualified" NodeName
dname) AnyLogic
lD
      -- translate SPEC1's signature along the comorphism
      (nsig2 :: NodeSig
nsig2@(NodeSig node :: Node
node gsigmaD :: G_sign
gsigmaD), dg2 :: DGraph
dg2) <- 
         LibEnv
-> LibName
-> AnyComorphism
-> DGraph
-> NodeSig
-> NodeName
-> Result (NodeSig, DGraph)
coerceNodeByComorph LibEnv
libEnv LibName
ln AnyComorphism
c DGraph
dg'' NodeSig
ns'' NodeName
dname
      (usig :: NodeSig
usig, udg :: DGraph
udg) <- case MaybeNode
nsig of
        EmptyNode _ -> (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeSig
nsig2, DGraph
dg2)
        JustNode ns2 :: NodeSig
ns2 -> do
          G_sign
gsigma2 <- LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign
gsigUnion LogicGraph
lg Bool
addSyms (NodeSig -> G_sign
getSig NodeSig
ns2) G_sign
gsigmaD
          let (ns :: NodeSig
ns@(NodeSig node2a :: Node
node2a _), dg2a :: DGraph
dg2a) =
                DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
insGSig DGraph
dg2 (String -> NodeName -> NodeName
extName "Union" NodeName
name) DGOrigin
DGUnion G_sign
gsigma2
          GMorphism
incl2 <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lg G_sign
gsigmaD G_sign
gsigma2
          let dg3 :: DGraph
dg3 = DGraph
-> GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Node
-> Node
-> DGraph
insLink DGraph
dg2a GMorphism
incl2 DGLinkType
globalDef DGLinkOrigin
SeeTarget Node
node Node
node2a
          DGraph
dg4 <- LinkKind
-> Conservativity
-> LogicGraph
-> DGraph
-> MaybeNode
-> NodeSig
-> DGLinkOrigin
-> Result DGraph
createConsLink LinkKind
DefLink Conservativity
conser LogicGraph
lg DGraph
dg3 MaybeNode
nsig NodeSig
ns DGLinkOrigin
SeeTarget
          (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeSig
ns, DGraph
dg4)
      -- analyse SPEC2
      (sp2' :: SPEC
sp2', nsig3 :: NodeSig
nsig3, udg3 :: DGraph
udg3) <-
          Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
addSyms Bool
optNodes LogicGraph
lg LibEnv
libEnv LibName
ln 
                  DGraph
udg (NodeSig -> MaybeNode
JustNode NodeSig
usig) NodeName
name HetcatsOpts
opts ExpOverrides
eo SPEC
sp2 Range
rg
      (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (AnyLogic
-> AnyLogic -> Annoted SPEC -> Annoted SPEC -> Range -> SPEC
Data AnyLogic
lD AnyLogic
lP
                   (SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted SPEC
sp1' Annoted SPEC
asp1)
                   (SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted SPEC
sp2' Annoted SPEC
asp2)
                   Range
pos, NodeSig
nsig3, DGraph
udg3)
  Combination (Network cItems :: [LABELED_ONTO_OR_INTPR_REF]
cItems eItems :: [IRI]
eItems _) pos :: Range
pos -> Range
-> Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall a. Range -> Result a -> Result a
adjustPos Range
pos (Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph))
-> Result (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ do
    let (cNodes' :: [Node]
cNodes', cEdges' :: [(Node, Node, DGLinkLab)]
cEdges') = DGraph
-> [LABELED_ONTO_OR_INTPR_REF]
-> [IRI]
-> ([Node], [(Node, Node, DGLinkLab)])
networkDiagram DGraph
dg [LABELED_ONTO_OR_INTPR_REF]
cItems [IRI]
eItems
    (ns :: NodeSig
ns, dg' :: DGraph
dg') <- LibEnv
-> LibName
-> DGraph
-> [Node]
-> [(Node, Node, DGLinkLab)]
-> NodeName
-> Result (NodeSig, DGraph)
insertColimitInGraph LibEnv
libEnv LibName
ln DGraph
dg [Node]
cNodes' [(Node, Node, DGLinkLab)]
cEdges' NodeName
name
    (SPEC, NodeSig, DGraph) -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (SPEC
sp, NodeSig
ns, DGraph
dg')
  _ -> String -> Result (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result (SPEC, NodeSig, DGraph))
-> String -> Result (SPEC, NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ "AnalysisStructured: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (LogicGraph -> SPEC -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg SPEC
sp)


-- | build the diagram of a network specified as a list of network elements to be added
-- | and a list of network elements to be removed

networkDiagram :: DGraph
                        -> [LABELED_ONTO_OR_INTPR_REF]
                        -> [IRI]
                        -> ([Node], [(Node, Node, DGLinkLab)])
networkDiagram :: DGraph
-> [LABELED_ONTO_OR_INTPR_REF]
-> [IRI]
-> ([Node], [(Node, Node, DGLinkLab)])
networkDiagram dg :: DGraph
dg cItems :: [LABELED_ONTO_OR_INTPR_REF]
cItems eItems :: [IRI]
eItems = let 
        -- add to/remove from a list of nodes and a list of edges
        -- the graph of a network element
        -- if remove is true, nElem gets removed 
        getNodes :: Bool
-> ([Node], [(Node, Node, DGLinkLab)])
-> IRI
-> ([Node], [(Node, Node, DGLinkLab)])
getNodes remove :: Bool
remove (cN :: [Node]
cN, cE :: [(Node, Node, DGLinkLab)]
cE) nElem :: IRI
nElem = let
            cEntry :: GlobalEntry
cEntry = GlobalEntry -> Maybe GlobalEntry -> GlobalEntry
forall a. a -> Maybe a -> a
fromMaybe (String -> GlobalEntry
forall a. HasCallStack => String -> a
error (String -> GlobalEntry) -> String -> GlobalEntry
forall a b. (a -> b) -> a -> b
$ "No entry for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ IRI -> String
forall a. Show a => a -> String
show IRI
nElem)
                     (Maybe GlobalEntry -> GlobalEntry)
-> Maybe GlobalEntry -> GlobalEntry
forall a b. (a -> b) -> a -> b
$ IRI -> DGraph -> Maybe GlobalEntry
lookupGlobalEnvDG IRI
nElem DGraph
dg
            bgraph :: Gr DGNodeLab DGLinkLab
bgraph = DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg
            lEdge :: Node -> Node -> GMorphism -> (Node, Node, DGLinkLab)
lEdge x :: Node
x y :: Node
y m :: GMorphism
m = case ((Node, Node, DGLinkLab) -> Bool)
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, z :: Node
z, l :: DGLinkLab
l) -> (Node
z Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
y) Bool -> Bool -> Bool
&&
                                         (DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
l GMorphism -> GMorphism -> Bool
forall a. Eq a => a -> a -> Bool
== GMorphism
m) ) ([(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)])
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a b. (a -> b) -> a -> b
$
                               Gr DGNodeLab DGLinkLab -> Node -> [(Node, Node, DGLinkLab)]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> [LEdge b]
out Gr DGNodeLab DGLinkLab
bgraph Node
x of
                             [] -> String -> (Node, Node, DGLinkLab)
forall a. HasCallStack => String -> a
error (String -> (Node, Node, DGLinkLab))
-> String -> (Node, Node, DGLinkLab)
forall a b. (a -> b) -> a -> b
$ "No edge found:\n x:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Node -> String
forall a. Show a => a -> String
show Node
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n y: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Node -> String
forall a. Show a => a -> String
show Node
y
                             lE :: (Node, Node, DGLinkLab)
lE : _ -> (Node, Node, DGLinkLab)
lE
           in case GlobalEntry
cEntry of
               SpecEntry extGenSig :: ExtGenSig
extGenSig -> let
                   n :: Node
n = NodeSig -> Node
getNode (NodeSig -> Node) -> NodeSig -> Node
forall a b. (a -> b) -> a -> b
$ ExtGenSig -> NodeSig
extGenBody ExtGenSig
extGenSig
                  in if Bool
remove then
                     (Node
nNode -> [Node] -> [Node]
forall a. a -> [a] -> [a]
:[Node]
cN, [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. Eq a => [a] -> [a]
nub ([(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)])
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a b. (a -> b) -> a -> b
$ [(Node, Node, DGLinkLab)]
cE [(Node, Node, DGLinkLab)]
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. [a] -> [a] -> [a]
++ Gr DGNodeLab DGLinkLab -> Node -> [(Node, Node, DGLinkLab)]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> [LEdge b]
out Gr DGNodeLab DGLinkLab
bgraph Node
n [(Node, Node, DGLinkLab)]
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. [a] -> [a] -> [a]
++ Gr DGNodeLab DGLinkLab -> Node -> [(Node, Node, DGLinkLab)]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> [LEdge b]
inn Gr DGNodeLab DGLinkLab
bgraph Node
n) 
                     -- remove all incoming and outgoing edges of n 
                     else if Node -> [Node] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Node
n [Node]
cN then ([Node]
cN, [(Node, Node, DGLinkLab)]
cE) else (Node
n Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: [Node]
cN, [(Node, Node, DGLinkLab)]
cE)
               ViewOrStructEntry True (ExtViewSig ns :: NodeSig
ns gm :: GMorphism
gm eGS :: ExtGenSig
eGS) -> let
                   s :: Node
s = NodeSig -> Node
getNode NodeSig
ns
                   t :: Node
t = NodeSig -> Node
getNode (NodeSig -> Node) -> NodeSig -> Node
forall a b. (a -> b) -> a -> b
$ ExtGenSig -> NodeSig
extGenBody ExtGenSig
eGS
                 in if Bool
remove 
                     then ([Node]
cN, Node -> Node -> GMorphism -> (Node, Node, DGLinkLab)
lEdge Node
s Node
t GMorphism
gm (Node, Node, DGLinkLab)
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. a -> [a] -> [a]
: [(Node, Node, DGLinkLab)]
cE) 
                     -- keep the nodes and remove just the edge 
                     else([Node] -> [Node]
forall a. Eq a => [a] -> [a]
nub ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Node
s Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: Node
t Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: [Node]
cN, Node -> Node -> GMorphism -> (Node, Node, DGLinkLab)
lEdge Node
s Node
t GMorphism
gm (Node, Node, DGLinkLab)
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. a -> [a] -> [a]
: [(Node, Node, DGLinkLab)]
cE)
               AlignEntry asig :: AlignSig
asig ->
                  case AlignSig
asig of
                   AlignMor src :: NodeSig
src gmor :: GMorphism
gmor tar :: NodeSig
tar ->  let
                     s :: Node
s = NodeSig -> Node
getNode NodeSig
src
                     t :: Node
t = NodeSig -> Node
getNode NodeSig
tar
                    in ([Node] -> [Node]
forall a. Eq a => [a] -> [a]
nub ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Node
s Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: Node
t Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: [Node]
cN, Node -> Node -> GMorphism -> (Node, Node, DGLinkLab)
lEdge Node
s Node
t GMorphism
gmor (Node, Node, DGLinkLab)
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. a -> [a] -> [a]
: [(Node, Node, DGLinkLab)]
cE)
                   AlignSpan src :: NodeSig
src phi1 :: GMorphism
phi1 tar1 :: NodeSig
tar1 phi2 :: GMorphism
phi2 tar2 :: NodeSig
tar2 ->  let
                     s :: Node
s = NodeSig -> Node
getNode NodeSig
src
                     t1 :: Node
t1 = NodeSig -> Node
getNode NodeSig
tar1
                     t2 :: Node
t2 = NodeSig -> Node
getNode NodeSig
tar2
                    in ([Node] -> [Node]
forall a. Eq a => [a] -> [a]
nub ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [Node
s, Node
t1, Node
t2] [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ [Node]
cN,
                              [Node -> Node -> GMorphism -> (Node, Node, DGLinkLab)
lEdge Node
s Node
t1 GMorphism
phi1, Node -> Node -> GMorphism -> (Node, Node, DGLinkLab)
lEdge Node
s Node
t2 GMorphism
phi2] [(Node, Node, DGLinkLab)]
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. [a] -> [a] -> [a]
++ [(Node, Node, DGLinkLab)]
cE)
                   WAlign src1 :: NodeSig
src1 i1 :: GMorphism
i1 sig1 :: GMorphism
sig1 src2 :: NodeSig
src2 i2 :: GMorphism
i2 sig2 :: GMorphism
sig2 tar1 :: NodeSig
tar1 tar2 :: NodeSig
tar2 bri :: NodeSig
bri -> let
                      s1 :: Node
s1 = NodeSig -> Node
getNode NodeSig
src1
                      s2 :: Node
s2 = NodeSig -> Node
getNode NodeSig
src2
                      t1 :: Node
t1 = NodeSig -> Node
getNode NodeSig
tar1
                      t2 :: Node
t2 = NodeSig -> Node
getNode NodeSig
tar2
                      b :: Node
b = NodeSig -> Node
getNode NodeSig
bri
                     in if Bool
remove then
                         ([Node] -> [Node]
forall a. Eq a => [a] -> [a]
nub ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Node
s1 Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: Node
s2 Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: Node
b Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: [Node]
cN,
                         [Node -> Node -> GMorphism -> (Node, Node, DGLinkLab)
lEdge Node
s1 Node
b GMorphism
i1, Node -> Node -> GMorphism -> (Node, Node, DGLinkLab)
lEdge Node
s1 Node
t1 GMorphism
sig1,
                          Node -> Node -> GMorphism -> (Node, Node, DGLinkLab)
lEdge Node
s2 Node
b GMorphism
i2, Node -> Node -> GMorphism -> (Node, Node, DGLinkLab)
lEdge Node
s2 Node
t2 GMorphism
sig2] [(Node, Node, DGLinkLab)]
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. [a] -> [a] -> [a]
++ [(Node, Node, DGLinkLab)]
cE) 
                        else ([Node] -> [Node]
forall a. Eq a => [a] -> [a]
nub ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ Node
s1 Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: Node
s2 Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: Node
t1 Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: Node
t2 Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: Node
b Node -> [Node] -> [Node]
forall a. a -> [a] -> [a]
: [Node]
cN,
                         [Node -> Node -> GMorphism -> (Node, Node, DGLinkLab)
lEdge Node
s1 Node
b GMorphism
i1, Node -> Node -> GMorphism -> (Node, Node, DGLinkLab)
lEdge Node
s1 Node
t1 GMorphism
sig1,
                          Node -> Node -> GMorphism -> (Node, Node, DGLinkLab)
lEdge Node
s2 Node
b GMorphism
i2, Node -> Node -> GMorphism -> (Node, Node, DGLinkLab)
lEdge Node
s2 Node
t2 GMorphism
sig2] [(Node, Node, DGLinkLab)]
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. [a] -> [a] -> [a]
++ [(Node, Node, DGLinkLab)]
cE)
               NetworkEntry diag :: GDiagram
diag -> let
                    dnodes :: [Node]
dnodes = GDiagram -> [Node]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [Node]
nodes GDiagram
diag
                    ledges :: [LEdge (Node, GMorphism)]
ledges = GDiagram -> [LEdge (Node, GMorphism)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges GDiagram
diag
                    dgedges :: [(Node, Node, DGLinkLab)]
dgedges = (LEdge (Node, GMorphism) -> (Node, Node, DGLinkLab))
-> [LEdge (Node, GMorphism)] -> [(Node, Node, DGLinkLab)]
forall a b. (a -> b) -> [a] -> [b]
map (\(x :: Node
x,y :: Node
y, (_, m :: GMorphism
m)) -> Node -> Node -> GMorphism -> (Node, Node, DGLinkLab)
lEdge Node
x Node
y GMorphism
m) [LEdge (Node, GMorphism)]
ledges
                   in ([Node]
dnodes, [(Node, Node, DGLinkLab)]
dgedges)
               _ -> String -> ([Node], [(Node, Node, DGLinkLab)])
forall a. HasCallStack => String -> a
error (String -> ([Node], [(Node, Node, DGLinkLab)]))
-> String -> ([Node], [(Node, Node, DGLinkLab)])
forall a b. (a -> b) -> a -> b
$ IRI -> String
forall a. Show a => a -> String
show IRI
nElem
                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is not an OMS, a view, a network or an alignment"
        -- also add the implicit elements: paths of global def. links,
        -- hiding def. links, inclusions of DOL intersections
        addGDefLinks :: ([Node], [Node], [(Node, Node, DGLinkLab)])
-> Node -> ([Node], [Node], [(Node, Node, DGLinkLab)])
addGDefLinks (cN :: [Node]
cN, iN :: [Node]
iN, cE :: [(Node, Node, DGLinkLab)]
cE) n :: Node
n = let
           g :: Gr DGNodeLab DGLinkLab
g = DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg
           allGDef :: [(a, b, DGLinkLab)] -> Bool
allGDef = ((a, b, DGLinkLab) -> Bool) -> [(a, b, DGLinkLab)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (((a, b, DGLinkLab) -> Bool) -> [(a, b, DGLinkLab)] -> Bool)
-> ((a, b, DGLinkLab) -> Bool) -> [(a, b, DGLinkLab)] -> Bool
forall a b. (a -> b) -> a -> b
$ \ (_, _, l :: DGLinkLab
l) -> DGLinkType -> Bool
isGlobalDef (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l
           gDefPaths :: Node -> Node -> [[(Node, Node, DGLinkLab)]]
gDefPaths x :: Node
x y :: Node
y = ([(Node, Node, DGLinkLab)] -> Bool)
-> [[(Node, Node, DGLinkLab)]] -> [[(Node, Node, DGLinkLab)]]
forall a. (a -> Bool) -> [a] -> [a]
filter [(Node, Node, DGLinkLab)] -> Bool
forall a b. [(a, b, DGLinkLab)] -> Bool
allGDef ([[(Node, Node, DGLinkLab)]] -> [[(Node, Node, DGLinkLab)]])
-> [[(Node, Node, DGLinkLab)]] -> [[(Node, Node, DGLinkLab)]]
forall a b. (a -> b) -> a -> b
$ Node
-> Node -> Gr DGNodeLab DGLinkLab -> [[(Node, Node, DGLinkLab)]]
forall a b. Node -> Node -> Gr a b -> [[LEdge b]]
getPathsTo Node
x Node
y Gr DGNodeLab DGLinkLab
g
           nPaths :: [(Node, Node, DGLinkLab)]
nPaths = [[(Node, Node, DGLinkLab)]] -> [(Node, Node, DGLinkLab)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Node, Node, DGLinkLab)]] -> [(Node, Node, DGLinkLab)])
-> [[(Node, Node, DGLinkLab)]] -> [(Node, Node, DGLinkLab)]
forall a b. (a -> b) -> a -> b
$ (Node -> [[(Node, Node, DGLinkLab)]])
-> [Node] -> [[(Node, Node, DGLinkLab)]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Node -> Node -> [[(Node, Node, DGLinkLab)]]
gDefPaths Node
n) [Node]
cN
           nNodes :: [Node]
nNodes = ((Node, Node, DGLinkLab) -> [Node])
-> [(Node, Node, DGLinkLab)] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (x :: Node
x, y :: Node
y, _) -> [Node
x, Node
y]) [(Node, Node, DGLinkLab)]
nPaths
           hideLinks :: [(Node, Node, DGLinkLab)]
hideLinks = ((Node, Node, DGLinkLab) -> Bool)
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, _, l :: DGLinkLab
l) -> DGLinkLab -> DGLinkType
dgl_type DGLinkLab
l DGLinkType -> DGLinkType -> Bool
forall a. Eq a => a -> a -> Bool
== DGLinkType
HidingDefLink)
              ([(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)])
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a b. (a -> b) -> a -> b
$ (Node -> [(Node, Node, DGLinkLab)])
-> [Node] -> [(Node, Node, DGLinkLab)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Gr DGNodeLab DGLinkLab -> Node -> [(Node, Node, DGLinkLab)]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> [LEdge b]
inn Gr DGNodeLab DGLinkLab
g) ([Node] -> [(Node, Node, DGLinkLab)])
-> [Node] -> [(Node, Node, DGLinkLab)]
forall a b. (a -> b) -> a -> b
$ [Node]
cN [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ [Node]
nNodes
           hNodes :: [Node]
hNodes = ((Node, Node, DGLinkLab) -> Node)
-> [(Node, Node, DGLinkLab)] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: Node
x, _, _) -> Node
x) [(Node, Node, DGLinkLab)]
hideLinks
           implicitNodes :: [Node]
implicitNodes = [Node] -> [Node]
forall a. Eq a => [a] -> [a]
nub ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [Node]
iN [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ [Node]
nNodes [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ [Node]
hNodes
           intersectLinks :: [(Node, Node, DGLinkLab)]
intersectLinks = ((Node, Node, DGLinkLab) -> Bool)
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, _, l :: DGLinkLab
l) -> DGLinkLab -> DGLinkOrigin
dgl_origin DGLinkLab
l DGLinkOrigin -> DGLinkOrigin -> Bool
forall a. Eq a => a -> a -> Bool
== DGLinkOrigin
DGLinkIntersect)
                            ([(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)])
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a b. (a -> b) -> a -> b
$ (Node -> [(Node, Node, DGLinkLab)])
-> [Node] -> [(Node, Node, DGLinkLab)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Gr DGNodeLab DGLinkLab -> Node -> [(Node, Node, DGLinkLab)]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> [LEdge b]
inn Gr DGNodeLab DGLinkLab
g) ([Node] -> [(Node, Node, DGLinkLab)])
-> [Node] -> [(Node, Node, DGLinkLab)]
forall a b. (a -> b) -> a -> b
$ [Node]
cN [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ [Node]
implicitNodes
           in ([Node]
cN, [Node]
implicitNodes
              , [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. Eq a => [a] -> [a]
nub ([(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)])
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a b. (a -> b) -> a -> b
$ [(Node, Node, DGLinkLab)]
nPaths [(Node, Node, DGLinkLab)]
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. [a] -> [a] -> [a]
++ [(Node, Node, DGLinkLab)]
cE [(Node, Node, DGLinkLab)]
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. [a] -> [a] -> [a]
++ [(Node, Node, DGLinkLab)]
hideLinks [(Node, Node, DGLinkLab)]
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. [a] -> [a] -> [a]
++ [(Node, Node, DGLinkLab)]
intersectLinks)
        addLinks :: ([Node], [(Node, Node, DGLinkLab)])
-> ([Node], [Node], [(Node, Node, DGLinkLab)])
addLinks (cN :: [Node]
cN, cE :: [(Node, Node, DGLinkLab)]
cE) = (([Node], [Node], [(Node, Node, DGLinkLab)])
 -> Node -> ([Node], [Node], [(Node, Node, DGLinkLab)]))
-> ([Node], [Node], [(Node, Node, DGLinkLab)])
-> [Node]
-> ([Node], [Node], [(Node, Node, DGLinkLab)])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ([Node], [Node], [(Node, Node, DGLinkLab)])
-> Node -> ([Node], [Node], [(Node, Node, DGLinkLab)])
addGDefLinks ([Node]
cN, [], [(Node, Node, DGLinkLab)]
cE) [Node]
cN
        (cNodes :: [Node]
cNodes, iNodes :: [Node]
iNodes, cEdges :: [(Node, Node, DGLinkLab)]
cEdges) =
           ([Node], [(Node, Node, DGLinkLab)])
-> ([Node], [Node], [(Node, Node, DGLinkLab)])
addLinks (([Node], [(Node, Node, DGLinkLab)])
 -> ([Node], [Node], [(Node, Node, DGLinkLab)]))
-> ([IRI] -> ([Node], [(Node, Node, DGLinkLab)]))
-> [IRI]
-> ([Node], [Node], [(Node, Node, DGLinkLab)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Node], [(Node, Node, DGLinkLab)])
 -> IRI -> ([Node], [(Node, Node, DGLinkLab)]))
-> ([Node], [(Node, Node, DGLinkLab)])
-> [IRI]
-> ([Node], [(Node, Node, DGLinkLab)])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Bool
-> ([Node], [(Node, Node, DGLinkLab)])
-> IRI
-> ([Node], [(Node, Node, DGLinkLab)])
getNodes Bool
False) ([], []) ([IRI] -> ([Node], [Node], [(Node, Node, DGLinkLab)]))
-> [IRI] -> ([Node], [Node], [(Node, Node, DGLinkLab)])
forall a b. (a -> b) -> a -> b
$ [LABELED_ONTO_OR_INTPR_REF] -> [IRI]
getItems [LABELED_ONTO_OR_INTPR_REF]
cItems
        (eNodes :: [Node]
eNodes, eEdges :: [(Node, Node, DGLinkLab)]
eEdges) = (([Node], [(Node, Node, DGLinkLab)])
 -> IRI -> ([Node], [(Node, Node, DGLinkLab)]))
-> ([Node], [(Node, Node, DGLinkLab)])
-> [IRI]
-> ([Node], [(Node, Node, DGLinkLab)])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Bool
-> ([Node], [(Node, Node, DGLinkLab)])
-> IRI
-> ([Node], [(Node, Node, DGLinkLab)])
getNodes Bool
True) ([], []) [IRI]
eItems
        (cNodes' :: [Node]
cNodes', cEdges' :: [(Node, Node, DGLinkLab)]
cEdges') = ([Node] -> [Node]
forall a. Eq a => [a] -> [a]
nub ([Node]
cNodes [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ [Node]
iNodes) [Node] -> [Node] -> [Node]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Node]
eNodes,
                              [(Node, Node, DGLinkLab)]
cEdges [(Node, Node, DGLinkLab)]
-> [(Node, Node, DGLinkLab)] -> [(Node, Node, DGLinkLab)]
forall a. Eq a => [a] -> [a] -> [a]
\\ [(Node, Node, DGLinkLab)]
eEdges)
 in ([Node]
cNodes', [(Node, Node, DGLinkLab)]
cEdges')
  
getItems :: [LABELED_ONTO_OR_INTPR_REF] -> [IRI]
getItems :: [LABELED_ONTO_OR_INTPR_REF] -> [IRI]
getItems [] = []
getItems (Labeled _ i :: IRI
i : r :: [LABELED_ONTO_OR_INTPR_REF]
r) = IRI
i IRI -> [IRI] -> [IRI]
forall a. a -> [a] -> [a]
: [LABELED_ONTO_OR_INTPR_REF] -> [IRI]
getItems [LABELED_ONTO_OR_INTPR_REF]
r

instMismatchError :: IRI -> Int -> Int -> Range -> Result a
instMismatchError :: IRI -> Node -> Node -> Range -> Result a
instMismatchError spname :: IRI
spname lp :: Node
lp la :: Node
la = String -> Range -> Result a
forall a. String -> Range -> Result a
fatal_error (String -> Range -> Result a) -> String -> Range -> Result a
forall a b. (a -> b) -> a -> b
$ IRI -> String
iriToStringUnsecure IRI
spname
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ " expects " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Node -> String
forall a. Show a => a -> String
show Node
lp String -> String -> String
forall a. [a] -> [a] -> [a]
++ " arguments" String -> String -> String
forall a. [a] -> [a] -> [a]
++ " but was given " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Node -> String
forall a. Show a => a -> String
show Node
la

notFoundError :: String -> IRI -> Result a
notFoundError :: String -> IRI -> Result a
notFoundError str :: String
str sid :: IRI
sid = String -> Range -> Result a
forall a. String -> Range -> Result a
fatal_error (String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ " '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ IRI -> String
iriToStringUnsecure IRI
sid
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ "' or '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ IRI -> String
iriToStringShortUnsecure IRI
sid String -> String -> String
forall a. [a] -> [a] -> [a]
++ "' not found") (Range -> Result a) -> Range -> Result a
forall a b. (a -> b) -> a -> b
$ IRI -> Range
iriPos IRI
sid

gsigUnionMaybe :: LogicGraph -> Bool -> MaybeNode -> G_sign -> Result G_sign
gsigUnionMaybe :: LogicGraph -> Bool -> MaybeNode -> G_sign -> Result G_sign
gsigUnionMaybe lg :: LogicGraph
lg both :: Bool
both mn :: MaybeNode
mn gsig :: G_sign
gsig = case MaybeNode
mn of
  EmptyNode _ -> G_sign -> Result G_sign
forall (m :: * -> *) a. Monad m => a -> m a
return G_sign
gsig
  JustNode ns :: NodeSig
ns -> LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign
gsigUnion LogicGraph
lg Bool
both (NodeSig -> G_sign
getSig NodeSig
ns) G_sign
gsig

anaExtraction :: LogicGraph -> LibEnv -> LibName -> DGraph -> NodeSig -> NodeName -> Range ->
              EXTRACTION -> Result (NodeSig, DGraph)
anaExtraction :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> NodeSig
-> NodeName
-> Range
-> EXTRACTION
-> Result (NodeSig, DGraph)
anaExtraction lg :: LogicGraph
lg libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg nsig :: NodeSig
nsig name :: NodeName
name rg :: Range
rg (ExtractOrRemove b :: Bool
b iris :: [IRI]
iris _) = if Bool -> Bool
not Bool
b then
  String -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "analysis of remove not implemented yet"
 else do
  let dg0 :: DGraph
dg0 = LibEnv -> DGraph -> DGraph
markHiding LibEnv
libEnv DGraph
dg
      n :: Node
n = NodeSig -> Node
getNode NodeSig
nsig
  if DGNodeLab -> Bool
labelHasHiding (DGNodeLab -> Bool) -> DGNodeLab -> Bool
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> DGNodeLab
labDG DGraph
dg0 Node
n then
    String -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "cannot extract module from a non-flattenable OMS"
   else do
    let dgThm :: DGraph
dgThm = LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheories LibEnv
libEnv LibName
ln DGraph
dg0
        gth :: G_theory
gth = case (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
dgThm) Node
n  of
               Nothing -> String -> G_theory
forall a. HasCallStack => String -> a
error "not able to compute theory"
               Just th :: G_theory
th -> G_theory
th
    G_theory
mTh <- case G_theory
gth of
        G_theory lid :: lid
lid syntax :: Maybe IRI
syntax (ExtSign sig :: sign
sig _) _ gsens :: ThSens sentence (AnyComorphism, BasicProof)
gsens _ -> do
          let nsens :: [Named sentence]
nsens = ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
gsens
          (msig :: sign
msig, msens :: [Named sentence]
msens) <- lid
-> [IRI]
-> (sign, [Named sentence])
-> Result (sign, [Named sentence])
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid
-> [IRI]
-> (sign, [Named sentence])
-> Result (sign, [Named sentence])
extract_module lid
lid [IRI]
iris (sign
sig, [Named sentence]
nsens)
          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
$ 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
syntax
                            (sign -> Set symbol -> ExtSign sign symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign sign
msig (Set symbol -> ExtSign sign symbol)
-> Set symbol -> ExtSign sign symbol
forall a b. (a -> b) -> a -> b
$ (Set symbol -> Set symbol -> Set symbol)
-> Set symbol -> [Set symbol] -> Set symbol
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Set symbol -> Set symbol -> Set symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set symbol
forall a. Set a
Set.empty ([Set symbol] -> Set symbol) -> [Set symbol] -> Set symbol
forall a b. (a -> b) -> a -> b
$ lid -> sign -> [Set symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> [Set symbol]
sym_of lid
lid sign
msig) SigId
startSigId
                            ([Named sentence] -> ThSens sentence (AnyComorphism, BasicProof)
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named sentence]
msens) ThId
startThId
    let (nsig' :: NodeSig
nsig', dg' :: DGraph
dg') = DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)
insGTheory DGraph
dg (Range -> NodeName -> NodeName
setSrcRange Range
rg NodeName
name) DGOrigin
DGExtract G_theory
mTh
    GMorphism
incl <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lg (NodeSig -> G_sign
getSig NodeSig
nsig') (NodeSig -> G_sign
getSig NodeSig
nsig)
    let  dg'' :: DGraph
dg'' = DGraph
-> GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Node
-> Node
-> DGraph
insLink DGraph
dg' GMorphism
incl DGLinkType
globalThm DGLinkOrigin
SeeSource (NodeSig -> Node
getNode NodeSig
nsig') Node
n
    (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeSig
nsig', DGraph
dg'')

anaUnion :: Bool -> LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> NodeName
  -> HetcatsOpts -> ExpOverrides -> [Annoted SPEC] -> Range
  -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
anaUnion :: Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> [Annoted SPEC]
-> Range
-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
anaUnion addSyms :: Bool
addSyms lg :: LogicGraph
lg libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg nsig :: MaybeNode
nsig name :: NodeName
name opts :: HetcatsOpts
opts eo :: ExpOverrides
eo asps :: [Annoted SPEC]
asps rg :: Range
rg = case [Annoted SPEC]
asps of
  [] -> String -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "empty union"
  _ -> do
      let sps :: [SPEC]
sps = (Annoted SPEC -> SPEC) -> [Annoted SPEC] -> [SPEC]
forall a b. (a -> b) -> [a] -> [b]
map Annoted SPEC -> SPEC
forall a. Annoted a -> a
item [Annoted SPEC]
asps
      (sps' :: [SPEC]
sps', nsigs :: [NodeSig]
nsigs, dg' :: DGraph
dg', _) <-
          let ana :: ([SPEC], [NodeSig], DGraph, NodeName)
-> SPEC -> Result ([SPEC], [NodeSig], DGraph, NodeName)
ana (sps1 :: [SPEC]
sps1, nsigs :: [NodeSig]
nsigs, dg' :: DGraph
dg', n :: NodeName
n) sp' :: SPEC
sp' = do
                let n1 :: NodeName
n1 = NodeName -> NodeName
inc NodeName
n
                (sp1 :: SPEC
sp1, nsig' :: NodeSig
nsig', dg1 :: DGraph
dg1) <-
                  Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
addSyms Bool
True LogicGraph
lg LibEnv
libEnv LibName
ln 
                          DGraph
dg' MaybeNode
nsig NodeName
n1 HetcatsOpts
opts ExpOverrides
eo SPEC
sp' (Range -> Result (SPEC, NodeSig, DGraph))
-> Range -> Result (SPEC, NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ SPEC -> Range
forall a. GetRange a => a -> Range
getRange SPEC
sp'
                ([SPEC], [NodeSig], DGraph, NodeName)
-> Result ([SPEC], [NodeSig], DGraph, NodeName)
forall (m :: * -> *) a. Monad m => a -> m a
return (SPEC
sp1 SPEC -> [SPEC] -> [SPEC]
forall a. a -> [a] -> [a]
: [SPEC]
sps1, NodeSig
nsig' NodeSig -> [NodeSig] -> [NodeSig]
forall a. a -> [a] -> [a]
: [NodeSig]
nsigs, DGraph
dg1, NodeName
n1)
           in (([SPEC], [NodeSig], DGraph, NodeName)
 -> SPEC -> Result ([SPEC], [NodeSig], DGraph, NodeName))
-> ([SPEC], [NodeSig], DGraph, NodeName)
-> [SPEC]
-> Result ([SPEC], [NodeSig], DGraph, NodeName)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ([SPEC], [NodeSig], DGraph, NodeName)
-> SPEC -> Result ([SPEC], [NodeSig], DGraph, NodeName)
ana ([], [], DGraph
dg, String -> NodeName -> NodeName
extName "Union" NodeName
name) [SPEC]
sps
      let newAsps :: [Annoted SPEC]
newAsps = (SPEC -> Annoted SPEC -> Annoted SPEC)
-> [SPEC] -> [Annoted SPEC] -> [Annoted SPEC]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted ([SPEC] -> [SPEC]
forall a. [a] -> [a]
reverse [SPEC]
sps') [Annoted SPEC]
asps
      case [NodeSig]
nsigs of
        [ns :: NodeSig
ns] -> ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted SPEC]
newAsps, [NodeSig]
nsigs, NodeSig
ns, DGraph
dg')
        _ -> do
          let nsigs' :: [NodeSig]
nsigs' = [NodeSig] -> [NodeSig]
forall a. [a] -> [a]
reverse [NodeSig]
nsigs
          G_sign
gbigSigma <- LogicGraph -> [G_sign] -> Result G_sign
gsigManyUnion LogicGraph
lg ((NodeSig -> G_sign) -> [NodeSig] -> [G_sign]
forall a b. (a -> b) -> [a] -> [b]
map NodeSig -> G_sign
getSig [NodeSig]
nsigs')
          let (ns :: NodeSig
ns@(NodeSig node :: Node
node _), dg2 :: DGraph
dg2) = DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
insGSig DGraph
dg' (Range -> NodeName -> NodeName
setSrcRange Range
rg NodeName
name)
                DGOrigin
DGUnion G_sign
gbigSigma
              insE :: DGraph -> NodeSig -> Result DGraph
insE dgl :: DGraph
dgl (NodeSig n :: Node
n gsigma :: G_sign
gsigma) = do
                GMorphism
incl <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lg G_sign
gsigma G_sign
gbigSigma
                DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph -> Result DGraph) -> DGraph -> Result DGraph
forall a b. (a -> b) -> a -> b
$ DGraph
-> GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Node
-> Node
-> DGraph
insLink DGraph
dgl GMorphism
incl DGLinkType
globalDef DGLinkOrigin
SeeTarget Node
n Node
node
          DGraph
dg3 <- (DGraph -> NodeSig -> Result DGraph)
-> DGraph -> [NodeSig] -> Result DGraph
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM DGraph -> NodeSig -> Result DGraph
insE DGraph
dg2 [NodeSig]
nsigs'
          ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted SPEC]
newAsps, [NodeSig]
nsigs', NodeSig
ns, DGraph
dg3)

anaIntersect :: Bool -> LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> NodeName
  -> HetcatsOpts -> ExpOverrides -> [Annoted SPEC] -> Range
  -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
anaIntersect :: Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> [Annoted SPEC]
-> Range
-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
anaIntersect addSyms :: Bool
addSyms lg :: LogicGraph
lg libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg nsig :: MaybeNode
nsig name :: NodeName
name opts :: HetcatsOpts
opts eo :: ExpOverrides
eo asps :: [Annoted SPEC]
asps rg :: Range
rg = case [Annoted SPEC]
asps of
  [] -> String -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "empty intersection"
  _ -> do
      let sps :: [SPEC]
sps = (Annoted SPEC -> SPEC) -> [Annoted SPEC] -> [SPEC]
forall a b. (a -> b) -> [a] -> [b]
map Annoted SPEC -> SPEC
forall a. Annoted a -> a
item [Annoted SPEC]
asps
          ana :: ([SPEC], [NodeSig], DGraph, NodeName)
-> SPEC -> Result ([SPEC], [NodeSig], DGraph, NodeName)
ana (sps1 :: [SPEC]
sps1, nsigs :: [NodeSig]
nsigs, dg' :: DGraph
dg', n :: NodeName
n) sp' :: SPEC
sp' = do
                let n1 :: NodeName
n1 = NodeName -> NodeName
inc NodeName
n
                (sp1 :: SPEC
sp1, nsig' :: NodeSig
nsig', dg1 :: DGraph
dg1) <-
                  Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
addSyms Bool
True LogicGraph
lg LibEnv
libEnv LibName
ln DGraph
dg' MaybeNode
nsig NodeName
n1 HetcatsOpts
opts ExpOverrides
eo SPEC
sp' (Range -> Result (SPEC, NodeSig, DGraph))
-> Range -> Result (SPEC, NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$
                          SPEC -> Range
forall a. GetRange a => a -> Range
getRange SPEC
sp'
                ([SPEC], [NodeSig], DGraph, NodeName)
-> Result ([SPEC], [NodeSig], DGraph, NodeName)
forall (m :: * -> *) a. Monad m => a -> m a
return (SPEC
sp1 SPEC -> [SPEC] -> [SPEC]
forall a. a -> [a] -> [a]
: [SPEC]
sps1, NodeSig
nsig' NodeSig -> [NodeSig] -> [NodeSig]
forall a. a -> [a] -> [a]
: [NodeSig]
nsigs, DGraph
dg1, NodeName
n1)
      (sps' :: [SPEC]
sps', nsigs :: [NodeSig]
nsigs, dg' :: DGraph
dg', _) <-
        (([SPEC], [NodeSig], DGraph, NodeName)
 -> SPEC -> Result ([SPEC], [NodeSig], DGraph, NodeName))
-> ([SPEC], [NodeSig], DGraph, NodeName)
-> [SPEC]
-> Result ([SPEC], [NodeSig], DGraph, NodeName)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ([SPEC], [NodeSig], DGraph, NodeName)
-> SPEC -> Result ([SPEC], [NodeSig], DGraph, NodeName)
ana ([], [], DGraph
dg, String -> NodeName -> NodeName
extName "Intersect" NodeName
name) [SPEC]
sps
      let newAsps :: [Annoted SPEC]
newAsps = (SPEC -> Annoted SPEC -> Annoted SPEC)
-> [SPEC] -> [Annoted SPEC] -> [Annoted SPEC]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted ([SPEC] -> [SPEC]
forall a. [a] -> [a]
reverse [SPEC]
sps') [Annoted SPEC]
asps
      case [NodeSig]
nsigs of
        [ns :: NodeSig
ns] -> ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted SPEC]
newAsps, [NodeSig]
nsigs, NodeSig
ns, DGraph
dg')
        _ -> do
          let nsigs' :: [NodeSig]
nsigs' = [NodeSig] -> [NodeSig]
forall a. [a] -> [a]
reverse [NodeSig]
nsigs
              labelHidings :: [Bool]
labelHidings = (DGNodeLab -> Bool) -> [DGNodeLab] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map DGNodeLab -> Bool
labelHasHiding ([DGNodeLab] -> [Bool]) -> [DGNodeLab] -> [Bool]
forall a b. (a -> b) -> a -> b
$ (NodeSig -> DGNodeLab) -> [NodeSig] -> [DGNodeLab]
forall a b. (a -> b) -> [a] -> [b]
map (\n :: NodeSig
n -> DGraph -> Node -> DGNodeLab
labDG (LibEnv -> DGraph -> DGraph
markHiding LibEnv
libEnv DGraph
dg) (Node -> DGNodeLab) -> Node -> DGNodeLab
forall a b. (a -> b) -> a -> b
$ NodeSig -> Node
getNode NodeSig
n) [NodeSig]
nsigs'
              hasHiding :: Bool
hasHiding = (Bool -> Bool -> Bool) -> Bool -> [Bool] -> Bool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\x :: Bool
x y :: Bool
y -> Bool
x Bool -> Bool -> Bool
|| Bool
y) Bool
False [Bool]
labelHidings
          case Bool
hasHiding of
            True -> String -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Intersection is defined only for flattenable theories"
            False -> do
             let dgThm :: DGraph
dgThm = LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheories LibEnv
libEnv LibName
ln DGraph
dg
                 theo :: G_theory
theo:theos :: [G_theory]
theos = (NodeSig -> G_theory) -> [NodeSig] -> [G_theory]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: NodeSig
x -> case (DGNodeLab -> Maybe G_theory
globalTheory (DGNodeLab -> Maybe G_theory)
-> (NodeSig -> DGNodeLab) -> NodeSig -> Maybe G_theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Node -> DGNodeLab
labDG DGraph
dgThm (Node -> DGNodeLab) -> (NodeSig -> Node) -> NodeSig -> DGNodeLab
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NodeSig -> Node
getNode) NodeSig
x of
                                            Nothing -> String -> G_theory
forall a. HasCallStack => String -> a
error (String -> G_theory) -> String -> G_theory
forall a b. (a -> b) -> a -> b
$ "not able to compute theory of node" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Node -> String
forall a. Show a => a -> String
show (Node -> String) -> Node -> String
forall a b. (a -> b) -> a -> b
$ NodeSig -> Node
getNode NodeSig
x)
                                            Just th :: G_theory
th -> G_theory
th) [NodeSig]
nsigs'
             G_sign
gbigSigma <- LogicGraph -> [G_sign] -> Result G_sign
gsigManyIntersect LogicGraph
lg ((NodeSig -> G_sign) -> [NodeSig] -> [G_sign]
forall a b. (a -> b) -> [a] -> [b]
map NodeSig -> G_sign
getSig [NodeSig]
nsigs')
             G_theory
gth <- (G_theory -> G_theory -> Result G_theory)
-> G_theory -> [G_theory] -> Result G_theory
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (G_sign -> G_theory -> G_theory -> Result G_theory
forall (m :: * -> *).
MonadFail m =>
G_sign -> G_theory -> G_theory -> m G_theory
intersectG_sentences G_sign
gbigSigma) G_theory
theo [G_theory]
theos
             let (ns :: NodeSig
ns@(NodeSig node :: Node
node _), dg2 :: DGraph
dg2) = DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)
insGTheory DGraph
dg' (Range -> NodeName -> NodeName
setSrcRange Range
rg NodeName
name)
                    DGOrigin
DGIntersect G_theory
gth
                 insE :: DGraph -> NodeSig -> Result DGraph
insE dgl :: DGraph
dgl (NodeSig n :: Node
n gsigma :: G_sign
gsigma) = do
                   GMorphism
incl <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lg G_sign
gbigSigma G_sign
gsigma
                   DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph -> Result DGraph) -> DGraph -> Result DGraph
forall a b. (a -> b) -> a -> b
$ DGraph
-> GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Node
-> Node
-> DGraph
insLink DGraph
dgl GMorphism
incl DGLinkType
globalThm DGLinkOrigin
DGLinkIntersect Node
node Node
n
             DGraph
dg3 <- (DGraph -> NodeSig -> Result DGraph)
-> DGraph -> [NodeSig] -> Result DGraph
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM DGraph -> NodeSig -> Result DGraph
insE DGraph
dg2 [NodeSig]
nsigs'
             ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted SPEC]
newAsps, [NodeSig]
nsigs', NodeSig
ns, DGraph
dg3)

anaFiltering :: LogicGraph -> LibEnv -> LibName -> DGraph -> NodeSig -> NodeName-> FILTERING
   -> Result (NodeSig, DGraph)
anaFiltering :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> NodeSig
-> NodeName
-> FILTERING
-> Result (NodeSig, DGraph)
anaFiltering lg :: LogicGraph
lg libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg nsig :: NodeSig
nsig nname :: NodeName
nname filtering :: FILTERING
filtering = case FILTERING
filtering of
  FilterSymbolList selectOrReject :: Bool
selectOrReject (G_symb_items_list lidS :: lid
lidS sItems :: [symb_items]
sItems) _ ->
   if Bool -> Bool
not Bool
selectOrReject then do
     let strs :: [String]
strs = (symb_items -> [String]) -> [symb_items] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (lid -> symb_items -> [String]
forall lid basic_spec symbol symb_items symb_map_items.
Syntax lid basic_spec symbol symb_items symb_map_items =>
lid -> symb_items -> [String]
symb_items_name lid
lidS) [symb_items]
sItems
         dgThm :: DGraph
dgThm = LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheories LibEnv
libEnv LibName
ln DGraph
dg
         th :: G_theory
th =
            case (DGNodeLab -> Maybe G_theory
globalTheory (DGNodeLab -> Maybe G_theory)
-> (NodeSig -> DGNodeLab) -> NodeSig -> Maybe G_theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGraph -> Node -> DGNodeLab
labDG DGraph
dgThm (Node -> DGNodeLab) -> (NodeSig -> Node) -> NodeSig -> DGNodeLab
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NodeSig -> Node
getNode) NodeSig
nsig of
                  Nothing -> String -> G_theory
forall a. HasCallStack => String -> a
error "error computing theory"
                  Just t :: G_theory
t -> G_theory
t
     case G_theory
th of
      G_theory l1 :: lid
l1 ser1 :: Maybe IRI
ser1 sig1 :: ExtSign sign symbol
sig1 ind1 :: SigId
ind1 sens1 :: ThSens sentence (AnyComorphism, BasicProof)
sens1 ind1' :: ThId
ind1' -> do
         let gth' :: G_theory
gth' = 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
l1 Maybe IRI
ser1 ExtSign sign symbol
sig1 SigId
ind1
                    ((ThSens sentence (AnyComorphism, BasicProof)
 -> String -> ThSens sentence (AnyComorphism, BasicProof))
-> ThSens sentence (AnyComorphism, BasicProof)
-> [String]
-> ThSens sentence (AnyComorphism, BasicProof)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\m :: ThSens sentence (AnyComorphism, BasicProof)
m x :: String
x -> String
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete String
x ThSens sentence (AnyComorphism, BasicProof)
m) ThSens sentence (AnyComorphism, BasicProof)
sens1 [String]
strs) ThId
ind1'
         let (ns :: NodeSig
ns@(NodeSig node :: Node
node gsigma :: G_sign
gsigma), dg' :: DGraph
dg') = DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)
insGTheory DGraph
dg NodeName
nname DGOrigin
DGEmpty G_theory
gth'
         GMorphism
gmor <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lg G_sign
gsigma (G_sign -> Result GMorphism) -> G_sign -> Result GMorphism
forall a b. (a -> b) -> a -> b
$ NodeSig -> G_sign
getSig NodeSig
nsig
         let dg2 :: DGraph
dg2 = DGraph
-> GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Node
-> Node
-> DGraph
insLink DGraph
dg' GMorphism
gmor DGLinkType
globalThm DGLinkOrigin
SeeSource Node
node (Node -> DGraph) -> Node -> DGraph
forall a b. (a -> b) -> a -> b
$ NodeSig -> Node
getNode NodeSig
nsig
         (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeSig
ns, DGraph
dg2)
    else String -> Result (NodeSig, DGraph)
forall a. HasCallStack => String -> a
error "analysis of select not implemented yet"
  FilterBasicSpec _ _ _ -> String -> Result (NodeSig, DGraph)
forall a. HasCallStack => String -> a
error "filtering a basic spec not implemented yet"


-- analysis of renamings
anaRen :: LogicGraph -> HetcatsOpts -> MaybeNode -> Range -> GMorphism
  -> G_mapping -> Result GMorphism
anaRen :: LogicGraph
-> HetcatsOpts
-> MaybeNode
-> Range
-> GMorphism
-> G_mapping
-> Result GMorphism
anaRen lg :: LogicGraph
lg opts :: HetcatsOpts
opts lenv :: MaybeNode
lenv pos :: Range
pos gmor :: GMorphism
gmor@(GMorphism r :: cid
r sigma :: ExtSign sign1 symbol1
sigma ind1 :: SigId
ind1 mor :: morphism2
mor _) gMapping :: G_mapping
gMapping =
  Range -> Result GMorphism -> Result GMorphism
forall a. Range -> Result a -> Result a
adjustPos Range
pos (Result GMorphism -> Result GMorphism)
-> Result GMorphism -> Result GMorphism
forall a b. (a -> b) -> a -> b
$ case G_mapping
gMapping of
  G_symb_map (G_symb_map_items_list lid :: lid
lid sis :: [symb_map_items]
sis) ->
    let lid2 :: lid2
lid2 = 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
r in
    if lid2 -> String
forall lid. Language lid => lid -> String
language_name lid2
lid2 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid then
     if HetcatsOpts -> Bool
isStructured HetcatsOpts
opts then GMorphism -> Result GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return GMorphism
gmor else do
      [symb_map_items2]
sis1 <- lid
-> lid2 -> String -> [symb_map_items] -> Result [symb_map_items2]
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 (m :: * -> *).
(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,
 MonadFail m) =>
lid1 -> lid2 -> String -> [symb_map_items1] -> m [symb_map_items2]
coerceSymbMapItemsList lid
lid lid2
lid2 "Analysis of renaming" [symb_map_items]
sis
      src :: ExtSign sign2 symbol2
src@(ExtSign sig :: sign2
sig _) <- ExtSign sign2 symbol2 -> Result (ExtSign sign2 symbol2)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtSign sign2 symbol2 -> Result (ExtSign sign2 symbol2))
-> ExtSign sign2 symbol2 -> Result (ExtSign sign2 symbol2)
forall a b. (a -> b) -> a -> b
$ lid2 -> sign2 -> ExtSign sign2 symbol2
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 -> ExtSign sign symbol
makeExtSign lid2
lid2 (sign2 -> ExtSign sign2 symbol2) -> sign2 -> ExtSign sign2 symbol2
forall a b. (a -> b) -> a -> b
$ morphism2 -> sign2
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism2
mor
      EndoMap raw_symbol2
rmap <- lid2
-> sign2
-> Maybe sign2
-> [symb_map_items2]
-> Result (EndoMap raw_symbol2)
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid
-> sign
-> Maybe sign
-> [symb_map_items]
-> Result (EndoMap raw_symbol)
stat_symb_map_items lid2
lid2 sign2
sig Maybe sign2
forall a. Maybe a
Nothing [symb_map_items2]
sis1
      morphism2
mor1 <- lid2
-> EndoMap raw_symbol2 -> ExtSign sign2 symbol2 -> Result morphism2
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 -> EndoMap raw_symbol -> ExtSign sign symbol -> Result morphism
ext_induced_from_morphism lid2
lid2 EndoMap raw_symbol2
rmap ExtSign sign2 symbol2
src
      case MaybeNode
lenv of
        EmptyNode _ -> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        JustNode (NodeSig _ sigLenv :: G_sign
sigLenv) -> do
          -- needs to be changed for logic translations
          (G_sign lid1 :: lid
lid1 sigmaLenv1 :: ExtSign sign symbol
sigmaLenv1 _, _) <-
              LogicGraph -> G_sign -> AnyLogic -> Result (G_sign, AnyComorphism)
gSigCoerce LogicGraph
lg G_sign
sigLenv (lid2 -> AnyLogic
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 -> AnyLogic
Logic lid2
lid2)
          ExtSign sign2 symbol2
sigmaLenv' <- lid
-> lid2
-> String
-> ExtSign sign symbol
-> Result (ExtSign sign2 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 (m :: * -> *).
(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,
 MonadFail m) =>
lid1
-> lid2
-> String
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid1 lid2
lid2 "" ExtSign sign symbol
sigmaLenv1
          let sysLenv :: Set symbol2
sysLenv = lid2 -> ExtSign sign2 symbol2 -> Set symbol2
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 -> Set symbol
ext_sym_of lid2
lid2 ExtSign sign2 symbol2
sigmaLenv'
              m :: EndoMap symbol2
m = lid2 -> morphism2 -> EndoMap symbol2
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> morphism -> EndoMap symbol
symmap_of lid2
lid2 morphism2
mor1
              isChanged :: symbol2 -> Bool
isChanged sy :: symbol2
sy = case symbol2 -> EndoMap symbol2 -> Maybe symbol2
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup symbol2
sy EndoMap symbol2
m of
                Just sy' :: symbol2
sy' -> symbol2
sy symbol2 -> symbol2 -> Bool
forall a. Eq a => a -> a -> Bool
/= symbol2
sy'
                Nothing -> Bool
False
              forbiddenSys :: Set symbol2
forbiddenSys = (symbol2 -> Bool) -> Set symbol2 -> Set symbol2
forall a. (a -> Bool) -> Set a -> Set a
Set.filter symbol2 -> Bool
isChanged Set symbol2
sysLenv
          Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set symbol2 -> Bool
forall a. Set a -> Bool
Set.null Set symbol2
forbiddenSys) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
plain_error () (
            "attempt to rename the following symbols from " String -> String -> String
forall a. [a] -> [a] -> [a]
++
            "the local environment:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set symbol2 -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Set symbol2
forbiddenSys "") Range
pos
      morphism2
mor2 <- morphism2 -> morphism2 -> Result morphism2
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp morphism2
mor morphism2
mor1
      GMorphism -> Result GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (GMorphism -> Result GMorphism) -> GMorphism -> Result GMorphism
forall a b. (a -> b) -> a -> b
$ cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
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
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism cid
r ExtSign sign1 symbol1
sigma SigId
ind1 morphism2
mor2 MorId
startMorId
    else do
      AnyComorphism
comor <- LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
logicInclusion LogicGraph
lg (lid2 -> AnyLogic
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 -> AnyLogic
Logic lid2
lid2) (lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid)
      GMorphism
gmorTrans <- AnyComorphism -> G_sign -> Result GMorphism
gEmbedComorphism AnyComorphism
comor (G_sign -> Result GMorphism) -> G_sign -> Result GMorphism
forall a b. (a -> b) -> a -> b
$ GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
gmor
      GMorphism
newMor <- GMorphism -> GMorphism -> Result GMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp GMorphism
gmor GMorphism
gmorTrans
      LogicGraph
-> HetcatsOpts
-> MaybeNode
-> Range
-> GMorphism
-> G_mapping
-> Result GMorphism
anaRen LogicGraph
lg HetcatsOpts
opts MaybeNode
lenv Range
pos GMorphism
newMor G_mapping
gMapping
  G_logic_translation (Logic_code tok :: Maybe String
tok src :: Maybe Logic_name
src tar :: Maybe Logic_name
tar pos1 :: Range
pos1) ->
    let pos2 :: Range
pos2 = if Range
pos1 Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Range
nullRange then Range
pos else Range
pos1
        adj1 :: Result a -> Result a
adj1 = Range -> Result a -> Result a
forall a. Range -> Result a -> Result a
adjustPos Range
pos2
    in Result GMorphism -> Result GMorphism
forall a. Result a -> Result a
adj1 (Result GMorphism -> Result GMorphism)
-> Result GMorphism -> Result GMorphism
forall a b. (a -> b) -> a -> b
$ do
    G_sign srcLid :: lid
srcLid srcSig :: ExtSign sign symbol
srcSig ind :: SigId
ind <- G_sign -> Result G_sign
forall (m :: * -> *) a. Monad m => a -> m a
return (GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
gmor)
    AnyComorphism
c <- case Maybe String
tok of
            Just c :: String
c -> String -> LogicGraph -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyComorphism
lookupComorphism String
c LogicGraph
lg
            Nothing -> case Maybe Logic_name
tar of
               Just (Logic_name l :: String
l _ _) ->
                 String -> String -> LogicGraph -> Result AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> String -> LogicGraph -> m AnyLogic
lookupLogic "with logic: " String
l LogicGraph
lg
                 Result AnyLogic
-> (AnyLogic -> Result AnyComorphism) -> Result AnyComorphism
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
logicInclusion LogicGraph
lg (lid -> AnyLogic
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 -> AnyLogic
Logic lid
srcLid)
               Nothing -> String -> Result AnyComorphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "with logic: cannot determine comorphism"
    Range -> Bool -> AnyComorphism -> Maybe Logic_name -> Result ()
checkSrcOrTarLogic Range
pos2 Bool
True AnyComorphism
c Maybe Logic_name
src
    Range -> Bool -> AnyComorphism -> Maybe Logic_name -> Result ()
checkSrcOrTarLogic Range
pos2 Bool
False AnyComorphism
c Maybe Logic_name
tar
    GMorphism
mor1 <- AnyComorphism -> G_sign -> Result GMorphism
gEmbedComorphism AnyComorphism
c (lid -> ExtSign sign symbol -> 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 lid
srcLid ExtSign sign symbol
srcSig SigId
ind)
    GMorphism -> GMorphism -> Result GMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp GMorphism
gmor GMorphism
mor1

checkSrcOrTarLogic :: Range -> Bool -> AnyComorphism -> Maybe Logic_name
                      -> Result ()
checkSrcOrTarLogic :: Range -> Bool -> AnyComorphism -> Maybe Logic_name -> Result ()
checkSrcOrTarLogic pos :: Range
pos b :: Bool
b (Comorphism cid :: cid
cid) ml :: Maybe Logic_name
ml = case Maybe Logic_name
ml of
  Nothing -> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  Just (Logic_name s :: String
s _ _) ->
      Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= if Bool
b then lid1 -> String
forall lid. Language lid => lid -> String
language_name (lid1 -> String) -> lid1 -> String
forall a b. (a -> b) -> a -> b
$ 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
                 else lid2 -> String
forall lid. Language lid => lid -> String
language_name (lid2 -> String) -> lid2 -> String
forall a b. (a -> b) -> a -> b
$ 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)
        (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
plain_error () (String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is is not the "
           String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
b then "source" else "target") String -> String -> String
forall a. [a] -> [a] -> [a]
++ " logic of "
           String -> String -> String
forall a. [a] -> [a] -> [a]
++ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid) Range
pos

anaRenaming :: LogicGraph -> MaybeNode -> G_sign -> HetcatsOpts -> RENAMING
  -> Result GMorphism
anaRenaming :: LogicGraph
-> MaybeNode
-> G_sign
-> HetcatsOpts
-> RENAMING
-> Result GMorphism
anaRenaming lg :: LogicGraph
lg lenv :: MaybeNode
lenv gSigma :: G_sign
gSigma opts :: HetcatsOpts
opts (Renaming ren :: [G_mapping]
ren pos :: Range
pos) =
      (GMorphism -> G_mapping -> Result GMorphism)
-> GMorphism -> [G_mapping] -> Result GMorphism
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (LogicGraph
-> HetcatsOpts
-> MaybeNode
-> Range
-> GMorphism
-> G_mapping
-> Result GMorphism
anaRen LogicGraph
lg HetcatsOpts
opts MaybeNode
lenv Range
pos) (G_sign -> GMorphism
forall object morphism.
Category object morphism =>
object -> morphism
ide G_sign
gSigma) [G_mapping]
ren

getRestrLogic :: RESTRICTION -> Result AnyLogic
getRestrLogic :: RESTRICTION -> Result AnyLogic
getRestrLogic restr :: RESTRICTION
restr = case RESTRICTION
restr of
  Revealed (G_symb_map_items_list lid :: lid
lid _) _ -> AnyLogic -> Result AnyLogic
forall (m :: * -> *) a. Monad m => a -> m a
return (AnyLogic -> Result AnyLogic) -> AnyLogic -> Result AnyLogic
forall a b. (a -> b) -> a -> b
$ lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid
  Hidden l :: [G_hiding]
l _ -> case [G_hiding]
l of
    [] -> String -> Result AnyLogic
forall a. HasCallStack => String -> a
error "getRestrLogic"
    h :: G_hiding
h : _ -> case G_hiding
h of
      G_symb_list (G_symb_items_list lid :: lid
lid _) -> AnyLogic -> Result AnyLogic
forall (m :: * -> *) a. Monad m => a -> m a
return (AnyLogic -> Result AnyLogic) -> AnyLogic -> Result AnyLogic
forall a b. (a -> b) -> a -> b
$ lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid
      G_logic_projection (Logic_code _ _ _ pos1 :: Range
pos1) ->
        String -> Range -> Result AnyLogic
forall a. String -> Range -> Result a
fatal_error "no analysis of logic projections yet" Range
pos1

-- analysis of restrictions
anaRestr :: LogicGraph -> G_sign -> Range -> GMorphism -> G_hiding
  -> Result GMorphism
anaRestr :: LogicGraph
-> G_sign -> Range -> GMorphism -> G_hiding -> Result GMorphism
anaRestr lg :: LogicGraph
lg sigEnv :: G_sign
sigEnv pos :: Range
pos (GMorphism cid :: cid
cid (ExtSign sigma1 :: sign1
sigma1 sys1 :: Set symbol1
sys1) _ mor :: morphism2
mor _) gh :: G_hiding
gh =
    case G_hiding
gh of
      G_symb_list (G_symb_items_list lid' :: lid
lid' sis' :: [symb_items]
sis') -> do
        let lid1 :: lid1
lid1 = 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
        [symb_items1]
sis1 <- lid -> lid1 -> String -> [symb_items] -> Result [symb_items1]
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 (m :: * -> *).
(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,
 MonadFail m) =>
lid1 -> lid2 -> String -> [symb_items1] -> m [symb_items2]
coerceSymbItemsList lid
lid' lid1
lid1 "Analysis of restriction1" [symb_items]
sis'
        [raw_symbol1]
rsys <- lid1 -> sign1 -> [symb_items1] -> Result [raw_symbol1]
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> [symb_items] -> Result [raw_symbol]
stat_symb_items lid1
lid1 sign1
sigma1 [symb_items1]
sis1
        let sys :: Set symbol1
sys = lid1 -> sign1 -> Set symbol1
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid1
lid1 sign1
sigma1
            sys' :: Set symbol1
sys' = (symbol1 -> Bool) -> Set symbol1 -> Set symbol1
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ sy :: symbol1
sy -> (raw_symbol1 -> Bool) -> [raw_symbol1] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (lid1 -> symbol1 -> raw_symbol1 -> Bool
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> symbol -> raw_symbol -> Bool
matches lid1
lid1 symbol1
sy) [raw_symbol1]
rsys) Set symbol1
sys
            unmatched :: [raw_symbol1]
unmatched = (raw_symbol1 -> Bool) -> [raw_symbol1] -> [raw_symbol1]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ rsy :: raw_symbol1
rsy -> Set symbol1 -> Bool
forall a. Set a -> Bool
Set.null (Set symbol1 -> Bool) -> Set symbol1 -> Bool
forall a b. (a -> b) -> a -> b
$ (symbol1 -> Bool) -> Set symbol1 -> Set symbol1
forall a. (a -> Bool) -> Set a -> Set a
Set.filter
                                 ( \ sy :: symbol1
sy -> lid1 -> symbol1 -> raw_symbol1 -> Bool
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> symbol -> raw_symbol -> Bool
matches lid1
lid1 symbol1
sy raw_symbol1
rsy) Set symbol1
sys') [raw_symbol1]
rsys
        Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([raw_symbol1] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [raw_symbol1]
unmatched)
          (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
plain_error () ("attempt to hide unknown symbols:\n"
                          String -> String -> String
forall a. [a] -> [a] -> [a]
++ [raw_symbol1] -> String -> String
forall a. Pretty a => a -> String -> String
showDoc [raw_symbol1]
unmatched "") Range
pos
        -- needs to be changed when logic projections are implemented
        (G_sign lidE :: lid
lidE sigmaLenv0 :: ExtSign sign symbol
sigmaLenv0 _, _) <- LogicGraph -> G_sign -> AnyLogic -> Result (G_sign, AnyComorphism)
gSigCoerce LogicGraph
lg G_sign
sigEnv (lid1 -> AnyLogic
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 -> AnyLogic
Logic lid1
lid1)
        ExtSign sign1 symbol1
sigmaLenv' <- lid
-> lid1
-> String
-> ExtSign sign symbol
-> Result (ExtSign sign1 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 (m :: * -> *).
(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,
 MonadFail m) =>
lid1
-> lid2
-> String
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lidE lid1
lid1 "" ExtSign sign symbol
sigmaLenv0
        let sysLenv :: Set symbol1
sysLenv = lid1 -> ExtSign sign1 symbol1 -> Set symbol1
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 -> Set symbol
ext_sym_of lid1
lid1 ExtSign sign1 symbol1
sigmaLenv'
            forbiddenSys :: Set symbol1
forbiddenSys = Set symbol1
sys' Set symbol1 -> Set symbol1 -> Set symbol1
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set symbol1
sysLenv
        Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set symbol1 -> Bool
forall a. Set a -> Bool
Set.null Set symbol1
forbiddenSys)
          (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
plain_error () (
         "attempt to hide the following symbols from the local environment:\n"
         String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set symbol1 -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Set symbol1
forbiddenSys "") Range
pos
        morphism1
mor1 <- lid1 -> Set symbol1 -> sign1 -> Result morphism1
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> Set symbol -> sign -> Result morphism
cogenerated_sign lid1
lid1 Set symbol1
sys' sign1
sigma1
        morphism2
mor1' <- cid -> morphism1 -> Result morphism2
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 -> morphism1 -> Result morphism2
map_morphism cid
cid morphism1
mor1
        morphism2
mor2 <- morphism2 -> morphism2 -> Result morphism2
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp morphism2
mor1' morphism2
mor
        GMorphism -> Result GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (GMorphism -> Result GMorphism) -> GMorphism -> Result GMorphism
forall a b. (a -> b) -> a -> b
$ cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
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
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism cid
cid (sign1 -> Set symbol1 -> ExtSign sign1 symbol1
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign (morphism1 -> sign1
forall object morphism.
Category object morphism =>
morphism -> object
dom morphism1
mor1) (Set symbol1 -> ExtSign sign1 symbol1)
-> Set symbol1 -> ExtSign sign1 symbol1
forall a b. (a -> b) -> a -> b
$ (symbol1 -> Set symbol1 -> Set symbol1)
-> Set symbol1 -> Set symbol1 -> Set symbol1
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ sy :: symbol1
sy ->
          case symbol1 -> Map symbol1 symbol1 -> Maybe symbol1
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup symbol1
sy (Map symbol1 symbol1 -> Maybe symbol1)
-> Map symbol1 symbol1 -> Maybe symbol1
forall a b. (a -> b) -> a -> b
$ lid1 -> morphism1 -> Map symbol1 symbol1
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> morphism -> EndoMap symbol
symmap_of lid1
lid1 morphism1
mor1 of
            Nothing -> Set symbol1 -> Set symbol1
forall a. a -> a
id
            Just sy1 :: symbol1
sy1 -> symbol1 -> Set symbol1 -> Set symbol1
forall a. Ord a => a -> Set a -> Set a
Set.insert symbol1
sy1) Set symbol1
forall a. Set a
Set.empty Set symbol1
sys1)
          SigId
startSigId morphism2
mor2 MorId
startMorId
      G_logic_projection (Logic_code _ _ _ pos1 :: Range
pos1) ->
        String -> Range -> Result GMorphism
forall a. String -> Range -> Result a
fatal_error "no analysis of logic projections yet" Range
pos1

anaRestriction :: LogicGraph -> G_sign -> G_sign -> HetcatsOpts -> RESTRICTION
  -> Result (GMorphism, Maybe GMorphism)
anaRestriction :: LogicGraph
-> G_sign
-> G_sign
-> HetcatsOpts
-> RESTRICTION
-> Result (GMorphism, Maybe GMorphism)
anaRestriction lg :: LogicGraph
lg gSigma :: G_sign
gSigma gSigma' :: G_sign
gSigma'@(G_sign lid0 :: lid
lid0 sig0 :: ExtSign sign symbol
sig0 _) opts :: HetcatsOpts
opts restr :: RESTRICTION
restr =
  if HetcatsOpts -> Bool
isStructured HetcatsOpts
opts then (GMorphism, Maybe GMorphism) -> Result (GMorphism, Maybe GMorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_sign -> GMorphism
forall object morphism.
Category object morphism =>
object -> morphism
ide G_sign
gSigma, Maybe GMorphism
forall a. Maybe a
Nothing) else
  case RESTRICTION
restr of
    Hidden rstr :: [G_hiding]
rstr pos :: Range
pos -> do
      GMorphism
mor <- (GMorphism -> G_hiding -> Result GMorphism)
-> GMorphism -> [G_hiding] -> Result GMorphism
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (LogicGraph
-> G_sign -> Range -> GMorphism -> G_hiding -> Result GMorphism
anaRestr LogicGraph
lg G_sign
gSigma Range
pos) (G_sign -> GMorphism
forall object morphism.
Category object morphism =>
object -> morphism
ide G_sign
gSigma') [G_hiding]
rstr
      (GMorphism, Maybe GMorphism) -> Result (GMorphism, Maybe GMorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (GMorphism
mor, Maybe GMorphism
forall a. Maybe a
Nothing)
    Revealed (G_symb_map_items_list lid1 :: lid
lid1 sis :: [symb_map_items]
sis) pos :: Range
pos -> Range
-> Result (GMorphism, Maybe GMorphism)
-> Result (GMorphism, Maybe GMorphism)
forall a. Range -> Result a -> Result a
adjustPos Range
pos (Result (GMorphism, Maybe GMorphism)
 -> Result (GMorphism, Maybe GMorphism))
-> Result (GMorphism, Maybe GMorphism)
-> Result (GMorphism, Maybe GMorphism)
forall a b. (a -> b) -> a -> b
$ do
      (G_sign lid :: lid
lid sigma :: ExtSign sign symbol
sigma _, _) <- LogicGraph -> G_sign -> AnyLogic -> Result (G_sign, AnyComorphism)
gSigCoerce LogicGraph
lg G_sign
gSigma (lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid1)
      ExtSign sign symbol
sigma0 <- lid
-> lid
-> String
-> ExtSign sign symbol
-> Result (ExtSign sign 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 (m :: * -> *).
(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,
 MonadFail m) =>
lid1
-> lid2
-> String
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid lid
lid1 "reveal1" ExtSign sign symbol
sigma
      ExtSign sign symbol
sigma1 <- lid
-> lid
-> String
-> ExtSign sign symbol
-> Result (ExtSign sign 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 (m :: * -> *).
(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,
 MonadFail m) =>
lid1
-> lid2
-> String
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid0 lid
lid1 "reveal2" ExtSign sign symbol
sig0
      let sys :: Set symbol
sys = lid -> ExtSign sign symbol -> 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 =>
lid -> ExtSign sign symbol -> Set symbol
ext_sym_of lid
lid1 ExtSign sign symbol
sigma0 -- local env
          sys' :: Set symbol
sys' = lid -> ExtSign sign symbol -> 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 =>
lid -> ExtSign sign symbol -> Set symbol
ext_sym_of lid
lid1 ExtSign sign symbol
sigma1 -- "big" signature
      EndoMap raw_symbol
rmap <- lid
-> sign
-> Maybe sign
-> [symb_map_items]
-> Result (EndoMap raw_symbol)
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid
-> sign
-> Maybe sign
-> [symb_map_items]
-> Result (EndoMap raw_symbol)
stat_symb_map_items lid
lid1 (ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symbol
sigma1) Maybe sign
forall a. Maybe a
Nothing [symb_map_items]
sis
      let sys'' :: Set symbol
sys'' = [symbol] -> Set symbol
forall a. Ord a => [a] -> Set a
Set.fromList
           [symbol
sy | symbol
sy <- Set symbol -> [symbol]
forall a. Set a -> [a]
Set.toList Set symbol
sys', raw_symbol
rsy <-
                       EndoMap raw_symbol -> [raw_symbol]
forall k a. Map k a -> [k]
Map.keys EndoMap raw_symbol
rmap, lid -> symbol -> raw_symbol -> Bool
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> symbol -> raw_symbol -> Bool
matches lid
lid1 symbol
sy raw_symbol
rsy]
          {- domain of rmap intersected with sys'
          rmap is checked by ext_induced_from_morphism below -}
      morphism
mor1 <- lid -> Set symbol -> ExtSign sign symbol -> Result morphism
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 -> Set symbol -> ExtSign sign symbol -> Result morphism
ext_generated_sign lid
lid1 (Set symbol
sys Set symbol -> Set symbol -> Set symbol
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set symbol
sys'') ExtSign sign symbol
sigma1
      let extsig1 :: ExtSign sign symbol
extsig1 = lid -> sign -> ExtSign sign 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 -> ExtSign sign symbol
makeExtSign lid
lid1 (sign -> ExtSign sign symbol) -> sign -> ExtSign sign symbol
forall a b. (a -> b) -> a -> b
$ morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
dom morphism
mor1
      morphism
mor2 <- lid -> EndoMap raw_symbol -> ExtSign sign symbol -> Result morphism
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 -> EndoMap raw_symbol -> ExtSign sign symbol -> Result morphism
ext_induced_from_morphism lid
lid1 EndoMap raw_symbol
rmap ExtSign sign symbol
extsig1
      (GMorphism, Maybe GMorphism) -> Result (GMorphism, Maybe GMorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_sign -> G_morphism -> GMorphism
gEmbed2 (lid -> ExtSign sign symbol -> 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 lid
lid1 ExtSign sign symbol
extsig1 SigId
startSigId)
                      (G_morphism -> GMorphism) -> G_morphism -> GMorphism
forall a b. (a -> b) -> a -> b
$ lid -> morphism -> MorId -> G_morphism
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 -> morphism -> MorId -> G_morphism
G_morphism lid
lid1 morphism
mor1 MorId
startMorId
             , GMorphism -> Maybe GMorphism
forall a. a -> Maybe a
Just (GMorphism -> Maybe GMorphism) -> GMorphism -> Maybe GMorphism
forall a b. (a -> b) -> a -> b
$ G_morphism -> GMorphism
gEmbed (G_morphism -> GMorphism) -> G_morphism -> GMorphism
forall a b. (a -> b) -> a -> b
$ lid -> morphism -> G_morphism
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 -> morphism -> G_morphism
mkG_morphism lid
lid1 morphism
mor2)

partitionGmaps :: [G_mapping] -> ([G_mapping], [G_mapping])
partitionGmaps :: [G_mapping] -> ([G_mapping], [G_mapping])
partitionGmaps l :: [G_mapping]
l = let
  (hs :: [G_mapping]
hs, rs :: [G_mapping]
rs) = (G_mapping -> Bool) -> [G_mapping] -> ([G_mapping], [G_mapping])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\ sm :: G_mapping
sm -> case G_mapping
sm of
    G_symb_map _ -> Bool
True
    G_logic_translation _ -> Bool
False) ([G_mapping] -> ([G_mapping], [G_mapping]))
-> [G_mapping] -> ([G_mapping], [G_mapping])
forall a b. (a -> b) -> a -> b
$ [G_mapping] -> [G_mapping]
forall a. [a] -> [a]
reverse [G_mapping]
l
  in ([G_mapping] -> [G_mapping]
forall a. [a] -> [a]
reverse [G_mapping]
rs, [G_mapping] -> [G_mapping]
forall a. [a] -> [a]
reverse [G_mapping]
hs)

anaGmaps :: LogicGraph -> HetcatsOpts -> Range -> G_sign -> G_sign
  -> [G_mapping] -> Result G_morphism
anaGmaps :: LogicGraph
-> HetcatsOpts
-> Range
-> G_sign
-> G_sign
-> [G_mapping]
-> Result G_morphism
anaGmaps lg :: LogicGraph
lg opts :: HetcatsOpts
opts pos :: Range
pos psig :: G_sign
psig@(G_sign lidP :: lid
lidP sigmaP :: ExtSign sign symbol
sigmaP _) asig :: G_sign
asig@(G_sign lidA :: lid
lidA sigmaA :: ExtSign sign symbol
sigmaA _)
  gsis :: [G_mapping]
gsis = Range -> Result G_morphism -> Result G_morphism
forall a. Range -> Result a -> Result a
adjustPos Range
pos (Result G_morphism -> Result G_morphism)
-> Result G_morphism -> Result G_morphism
forall a b. (a -> b) -> a -> b
$ if HetcatsOpts -> Bool
isStructured HetcatsOpts
opts
    then G_morphism -> Result G_morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (G_morphism -> Result G_morphism)
-> G_morphism -> Result G_morphism
forall a b. (a -> b) -> a -> b
$ lid -> morphism -> G_morphism
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 -> morphism -> G_morphism
mkG_morphism lid
lidP (morphism -> G_morphism) -> morphism -> G_morphism
forall a b. (a -> b