{- |
Module      :  ./Static/AnalysisArchitecture.hs
Description :  static analysis of CASL architectural specifications
Copyright   :  (c) Maciek Makowski, Warsaw University, C. Maeder 2004-2006
               Mihai Codescu, DFKI GmbH Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (via imports)

Static analysis of CASL architectural specifications
   Follows the extended static semantics sketched in Chap. III:5.6
   of the CASL Reference Manual.
-}

module Static.AnalysisArchitecture
    ( anaArchSpec
    , anaUnitSpec
    , anaRefSpec
    ) where

import Driver.Options

import Logic.Logic
import Logic.ExtSign
import Logic.Coerce
import Logic.Grothendieck

import Static.GTheory
import Static.DevGraph
import Static.DgUtils
import Static.ArchDiagram
import Static.AnalysisStructured

import Syntax.Print_AS_Architecture ()
import Syntax.AS_Architecture
import Syntax.Print_AS_Structured
import Syntax.AS_Structured

import Common.AS_Annotation
import Common.ExtSign
import Common.Id
import Common.IRI
import Common.LibName
import Common.Result
import Common.Amalgamate
import Common.Doc
import qualified Data.Map as Map

import Data.Maybe
import Data.Graph.Inductive.Graph as Graph (Node, lab)
import qualified Data.Set as Set
import Control.Monad (foldM)

first :: (a, b, c) -> a
first :: (a, b, c) -> a
first (a :: a
a, _, _) = a
a

second :: (a, b, c) -> b
second :: (a, b, c) -> b
second (_, b :: b
b, _) = b
b

third :: (a, b, c) -> c
third :: (a, b, c) -> c
third (_, _, c :: c
c) = c
c

{- | Analyse an architectural specification
@
ARCH-SPEC ::= BASIC-ARCH-SPEC | GROUP-ARCH-SPEC | ARCH-SPEC-NAME
@ -}
anaArchSpec :: LogicGraph -> LibEnv -> LibName -> DGraph
  -> HetcatsOpts  -- ^ should only the structure be analysed?
  -> ExpOverrides
  -> ExtStUnitCtx -- ^ for visibility levels
  -> Maybe Node
  -> ARCH_SPEC -> Result ([DiagNodeSig], Maybe DiagNodeSig,
                          Diag, RefSig, DGraph, ARCH_SPEC)
{- ^ returns 1. the architectural signature of given ARCH-SPEC
2. development graph resulting from structured specs within the arch
spec and 3. ARCH_SPEC after possible conversions -}
anaArchSpec :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> Maybe Node
-> ARCH_SPEC
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph, ARCH_SPEC)
anaArchSpec lgraph :: LogicGraph
lgraph libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo sharedCtx :: ExtStUnitCtx
sharedCtx nP :: Maybe Node
nP archSp :: ARCH_SPEC
archSp = case ARCH_SPEC
archSp of
  Basic_arch_spec udd :: [Annoted UNIT_DECL_DEFN]
udd uexpr :: Annoted UNIT_EXPRESSION
uexpr pos :: Range
pos ->
    do (branchMap :: Map IRI RTPointer
branchMap, uctx :: ExtStUnitCtx
uctx, dg' :: DGraph
dg', udd' :: [Annoted UNIT_DECL_DEFN]
udd') <-
         LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> [Annoted UNIT_DECL_DEFN]
-> Result
     (Map IRI RTPointer, ExtStUnitCtx, DGraph, [Annoted UNIT_DECL_DEFN])
anaUnitDeclDefns LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
sharedCtx [Annoted UNIT_DECL_DEFN]
udd
       (nodes :: [DiagNodeSig]
nodes, usig :: UnitSig
usig, diag'' :: Diag
diag'', dg'' :: DGraph
dg'', uexpr' :: UNIT_EXPRESSION
uexpr') <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_EXPRESSION
-> Result ([DiagNodeSig], UnitSig, Diag, DGraph, UNIT_EXPRESSION)
anaUnitExpression LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg' HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
uctx (UNIT_EXPRESSION
 -> Result ([DiagNodeSig], UnitSig, Diag, DGraph, UNIT_EXPRESSION))
-> UNIT_EXPRESSION
-> Result ([DiagNodeSig], UnitSig, Diag, DGraph, UNIT_EXPRESSION)
forall a b. (a -> b) -> a -> b
$ Annoted UNIT_EXPRESSION -> UNIT_EXPRESSION
forall a. Annoted a -> a
item Annoted UNIT_EXPRESSION
uexpr
       let (nodes' :: [DiagNodeSig]
nodes', maybeRes :: Maybe DiagNodeSig
maybeRes) = case [DiagNodeSig]
nodes of
                [] -> ([], Maybe DiagNodeSig
forall a. Maybe a
Nothing) -- don't think its possible
                [x :: DiagNodeSig
x] -> ([], DiagNodeSig -> Maybe DiagNodeSig
forall a. a -> Maybe a
Just DiagNodeSig
x)
                _ -> ([DiagNodeSig]
nodes, Maybe DiagNodeSig
forall a. Maybe a
Nothing)
           rNodes :: [Node]
rNodes = (RTPointer -> Node) -> [RTPointer] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map RTPointer -> Node
refSource ([RTPointer] -> [Node]) -> [RTPointer] -> [Node]
forall a b. (a -> b) -> a -> b
$ Map IRI RTPointer -> [RTPointer]
forall k a. Map k a -> [a]
Map.elems Map IRI RTPointer
branchMap
           (rN :: Node
rN, dg3 :: DGraph
dg3) =
              case Maybe Node
nP of
               Nothing -> let
                   (n :: Node
n, dgI :: DGraph
dgI) = DGraph -> UnitSig -> String -> (Node, DGraph)
addNodeRT DGraph
dg'' UnitSig
usig "ArchSpec"
                          in (Node
n, DGraph -> [Node] -> Node -> DGraph
addEdgesToNodeRT DGraph
dgI [Node]
rNodes Node
n)
               Just x :: Node
x -> (Node
x, DGraph -> [Node] -> Node -> DGraph
addEdgesToNodeRT DGraph
dg' [Node]
rNodes Node
x)
           rP :: RTPointer
rP = Node -> Map IRI RTPointer -> RTPointer
NPBranch Node
rN Map IRI RTPointer
branchMap
       ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph, ARCH_SPEC)
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph, ARCH_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return ([DiagNodeSig]
nodes', Maybe DiagNodeSig
maybeRes, Diag
diag'',
                RTPointer -> (UnitSig, Maybe BranchSig) -> RefSig
BranchRefSig RTPointer
rP (UnitSig
usig, BranchSig -> Maybe BranchSig
forall a. a -> Maybe a
Just (BranchSig -> Maybe BranchSig) -> BranchSig -> Maybe BranchSig
forall a b. (a -> b) -> a -> b
$ BStContext -> BranchSig
BranchStaticContext (ExtStUnitCtx -> BStContext
ctx ExtStUnitCtx
uctx)),
                DGraph
dg3, [Annoted UNIT_DECL_DEFN]
-> Annoted UNIT_EXPRESSION -> Range -> ARCH_SPEC
Basic_arch_spec [Annoted UNIT_DECL_DEFN]
udd'
                           (UNIT_EXPRESSION
-> Annoted UNIT_EXPRESSION -> Annoted UNIT_EXPRESSION
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted UNIT_EXPRESSION
uexpr' Annoted UNIT_EXPRESSION
uexpr) Range
pos)
  Group_arch_spec asp :: Annoted ARCH_SPEC
asp _ ->
      LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> Maybe Node
-> ARCH_SPEC
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph, ARCH_SPEC)
anaArchSpec LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
sharedCtx Maybe Node
nP (Annoted ARCH_SPEC -> ARCH_SPEC
forall a. Annoted a -> a
item Annoted ARCH_SPEC
asp)
  Arch_spec_name un' :: IRI
un' -> do
    IRI
asi <- GlobalAnnos -> ExpOverrides -> IRI -> Result IRI
expCurieR (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
un'
    case IRI -> DGraph -> Maybe GlobalEntry
lookupGlobalEnvDG IRI
asi DGraph
dg of
            Just (ArchOrRefEntry True asig :: RefSig
asig@(BranchRefSig
                        (NPBranch n :: Node
n f :: Map IRI RTPointer
f) (UnitSig nsList :: [NodeSig]
nsList resNs :: NodeSig
resNs _, _))) -> do
              let (rN :: Node
rN, dg' :: DGraph
dg', asig' :: RefSig
asig') =
                        case Maybe Node
nP of
                         Nothing -> let
                           (dg0 :: DGraph
dg0, g :: Map Node Node
g) = DGraph -> Node -> Maybe Node -> (DGraph, Map Node Node)
copySubTree DGraph
dg Node
n Maybe Node
forall a. Maybe a
Nothing
                           n0 :: Node
n0 = Node -> Node -> Map Node Node -> Node
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Node
forall a. HasCallStack => String -> a
error "copy") Node
n Map Node Node
g
                           (r1 :: Node
r1, d1 :: DGraph
d1) = (Node
n0, DGraph
dg0) -- TODO: this is not needed
                           a1 :: RefSig
a1 = RefSig -> RTPointer -> RefSig
setPointerInRef RefSig
asig (Node -> Map IRI RTPointer -> RTPointer
NPBranch Node
r1 (Map IRI RTPointer -> RTPointer) -> Map IRI RTPointer -> RTPointer
forall a b. (a -> b) -> a -> b
$
                                 (RTPointer -> RTPointer) -> Map IRI RTPointer -> Map IRI RTPointer
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Map Node Node -> RTPointer -> RTPointer
mapRTNodes Map Node Node
g) Map IRI RTPointer
f)
                          in (Node
r1, DGraph
d1, RefSig
a1)
                         Just x :: Node
x -> let
                           (dg0 :: DGraph
dg0, g :: Map Node Node
g) = DGraph -> Node -> Maybe Node -> (DGraph, Map Node Node)
copySubTree DGraph
dg Node
n Maybe Node
forall a. Maybe a
Nothing
                           n0 :: Node
n0 = Node -> Node -> Map Node Node -> Node
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Node
forall a. HasCallStack => String -> a
error "copy") Node
n Map Node Node
g
                           d1 :: DGraph
d1 = DGraph -> Node -> Node -> DGraph
addRefEdgeRT DGraph
dg0 Node
x Node
n0
                           a1 :: RefSig
a1 = RefSig -> RTPointer -> RefSig
setPointerInRef RefSig
asig (Node -> Map IRI RTPointer -> RTPointer
NPBranch Node
rN (Map IRI RTPointer -> RTPointer) -> Map IRI RTPointer -> RTPointer
forall a b. (a -> b) -> a -> b
$
                                 (RTPointer -> RTPointer) -> Map IRI RTPointer -> Map IRI RTPointer
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Map Node Node -> RTPointer -> RTPointer
mapRTNodes Map Node Node
g) Map IRI RTPointer
f)
                          in (Node
x, DGraph
d1, RefSig
a1)
              case [NodeSig]
nsList of
               [] ->
                 ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph, ARCH_SPEC)
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph, ARCH_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Maybe DiagNodeSig
forall a. Maybe a
Nothing, ExtStUnitCtx -> Diag
forall a b. (a, b) -> b
snd ExtStUnitCtx
sharedCtx, RefSig
asig', DGraph
dg', ARCH_SPEC
archSp)
               _ -> do
                (dnsigs :: [DiagNodeSig]
dnsigs, diag' :: Diag
diag') <- (([DiagNodeSig], Diag) -> NodeSig -> Result ([DiagNodeSig], Diag))
-> ([DiagNodeSig], Diag)
-> [NodeSig]
-> Result ([DiagNodeSig], Diag)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ (l :: [DiagNodeSig]
l, d :: Diag
d) ns :: NodeSig
ns -> do
                        (dns :: DiagNodeSig
dns, d' :: Diag
d') <- LogicGraph
-> Diag
-> [DiagNodeSig]
-> NodeSig
-> String
-> Result (DiagNodeSig, Diag)
extendDiagramIncl LogicGraph
lgraph Diag
d [] NodeSig
ns "Arch Sig"
                        ([DiagNodeSig], Diag) -> Result ([DiagNodeSig], Diag)
forall (m :: * -> *) a. Monad m => a -> m a
return (DiagNodeSig
dns DiagNodeSig -> [DiagNodeSig] -> [DiagNodeSig]
forall a. a -> [a] -> [a]
: [DiagNodeSig]
l, Diag
d'))
                      ([], ExtStUnitCtx -> Diag
forall a b. (a, b) -> b
snd ExtStUnitCtx
sharedCtx) ([NodeSig] -> Result ([DiagNodeSig], Diag))
-> [NodeSig] -> Result ([DiagNodeSig], Diag)
forall a b. (a -> b) -> a -> b
$ [NodeSig] -> [NodeSig]
forall a. [a] -> [a]
reverse [NodeSig]
nsList
                (dns :: DiagNodeSig
dns, diag'' :: Diag
diag'') <-
                   LogicGraph
-> Diag
-> [DiagNodeSig]
-> NodeSig
-> String
-> Result (DiagNodeSig, Diag)
extendDiagramIncl LogicGraph
lgraph Diag
diag' [DiagNodeSig]
dnsigs NodeSig
resNs "arch sig"
                ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph, ARCH_SPEC)
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph, ARCH_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return (DiagNodeSig
dns DiagNodeSig -> [DiagNodeSig] -> [DiagNodeSig]
forall a. a -> [a] -> [a]
: [DiagNodeSig]
dnsigs, Maybe DiagNodeSig
forall a. Maybe a
Nothing, Diag
diag'', RefSig
asig', DGraph
dg', ARCH_SPEC
archSp)
            _ -> String
-> IRI
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph, ARCH_SPEC)
forall a. String -> IRI -> Result a
notFoundError "architectural specification" IRI
asi

-- | Analyse a list of unit declarations and definitions
anaUnitDeclDefns :: LogicGraph -> LibEnv -> LibName -> DGraph
    -> HetcatsOpts
    -> ExpOverrides
    -> ExtStUnitCtx -> [Annoted UNIT_DECL_DEFN]
    -> Result (Map.Map IRI RTPointer, ExtStUnitCtx,
               DGraph, [Annoted UNIT_DECL_DEFN])
{- ^ returns 1. extended static unit context 2. possibly modified
development graph 3. possibly modified list of unit declarations and
definitions -}
anaUnitDeclDefns :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> [Annoted UNIT_DECL_DEFN]
-> Result
     (Map IRI RTPointer, ExtStUnitCtx, DGraph, [Annoted UNIT_DECL_DEFN])
anaUnitDeclDefns lgraph :: LogicGraph
lgraph libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo sharedCtx :: ExtStUnitCtx
sharedCtx =
  LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> Map IRI RTPointer
-> [Annoted UNIT_DECL_DEFN]
-> Result
     (Map IRI RTPointer, ExtStUnitCtx, DGraph, [Annoted UNIT_DECL_DEFN])
anaUnitDeclDefns' LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
sharedCtx Map IRI RTPointer
forall k a. Map k a
Map.empty

anaUnitDeclDefns' :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts
    -> ExpOverrides
    -> ExtStUnitCtx -> Map.Map IRI RTPointer
    -> [Annoted UNIT_DECL_DEFN]
    -> Result (Map.Map IRI RTPointer, ExtStUnitCtx,
               DGraph, [Annoted UNIT_DECL_DEFN])
anaUnitDeclDefns' :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> Map IRI RTPointer
-> [Annoted UNIT_DECL_DEFN]
-> Result
     (Map IRI RTPointer, ExtStUnitCtx, DGraph, [Annoted UNIT_DECL_DEFN])
anaUnitDeclDefns' lgraph :: LogicGraph
lgraph libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo uctx :: ExtStUnitCtx
uctx rNodes :: Map IRI RTPointer
rNodes uds :: [Annoted UNIT_DECL_DEFN]
uds = case [Annoted UNIT_DECL_DEFN]
uds of
  udd :: Annoted UNIT_DECL_DEFN
udd : udds :: [Annoted UNIT_DECL_DEFN]
udds -> do
    (rNodes1 :: Map IRI RTPointer
rNodes1, uctx' :: ExtStUnitCtx
uctx', dg' :: DGraph
dg', udd' :: UNIT_DECL_DEFN
udd') <-
        LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_DECL_DEFN
-> Result (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
anaUnitDeclDefn LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
uctx (Annoted UNIT_DECL_DEFN -> UNIT_DECL_DEFN
forall a. Annoted a -> a
item Annoted UNIT_DECL_DEFN
udd)
    (rNodes2 :: Map IRI RTPointer
rNodes2, uctx'' :: ExtStUnitCtx
uctx'', dg'' :: DGraph
dg'', udds' :: [Annoted UNIT_DECL_DEFN]
udds') <- LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> Map IRI RTPointer
-> [Annoted UNIT_DECL_DEFN]
-> Result
     (Map IRI RTPointer, ExtStUnitCtx, DGraph, [Annoted UNIT_DECL_DEFN])
anaUnitDeclDefns' LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg' HetcatsOpts
opts ExpOverrides
eo
      ExtStUnitCtx
uctx' (Map IRI RTPointer -> Map IRI RTPointer -> Map IRI RTPointer
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map IRI RTPointer
rNodes1 Map IRI RTPointer
rNodes) [Annoted UNIT_DECL_DEFN]
udds
    (Map IRI RTPointer, ExtStUnitCtx, DGraph, [Annoted UNIT_DECL_DEFN])
-> Result
     (Map IRI RTPointer, ExtStUnitCtx, DGraph, [Annoted UNIT_DECL_DEFN])
forall (m :: * -> *) a. Monad m => a -> m a
return (Map IRI RTPointer
rNodes2, ExtStUnitCtx
uctx'', DGraph
dg'', UNIT_DECL_DEFN -> Annoted UNIT_DECL_DEFN -> Annoted UNIT_DECL_DEFN
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted UNIT_DECL_DEFN
udd' Annoted UNIT_DECL_DEFN
udd Annoted UNIT_DECL_DEFN
-> [Annoted UNIT_DECL_DEFN] -> [Annoted UNIT_DECL_DEFN]
forall a. a -> [a] -> [a]
: [Annoted UNIT_DECL_DEFN]
udds')
  [] -> (Map IRI RTPointer, ExtStUnitCtx, DGraph, [Annoted UNIT_DECL_DEFN])
-> Result
     (Map IRI RTPointer, ExtStUnitCtx, DGraph, [Annoted UNIT_DECL_DEFN])
forall (m :: * -> *) a. Monad m => a -> m a
return (Map IRI RTPointer
rNodes, ExtStUnitCtx
uctx, DGraph
dg, [])

alreadyDefinedUnit :: IRI -> String
alreadyDefinedUnit :: IRI -> String
alreadyDefinedUnit u :: IRI
u =
    "Unit " String -> String -> String
forall a. [a] -> [a] -> [a]
++ IRI -> String
iriToStringUnsecure IRI
u String -> String -> String
forall a. [a] -> [a] -> [a]
++ " already declared/defined"

-- | Create a node that represents a union of signatures
nodeSigUnion :: LogicGraph -> DGraph -> [MaybeNode] -> DGOrigin -> SPEC_NAME
             -> Result (NodeSig, DGraph)
nodeSigUnion :: LogicGraph
-> DGraph
-> [MaybeNode]
-> DGOrigin
-> IRI
-> Result (NodeSig, DGraph)
nodeSigUnion lgraph :: LogicGraph
lgraph dg :: DGraph
dg nodeSigs :: [MaybeNode]
nodeSigs orig :: DGOrigin
orig sname :: IRI
sname =
  do sigUnion :: G_sign
sigUnion@(G_sign lid :: lid
lid sigU :: ExtSign sign symbol
sigU ind :: SigId
ind) <- LogicGraph -> [G_sign] -> Result G_sign
gsigManyUnion LogicGraph
lgraph
                                   ([G_sign] -> Result G_sign) -> [G_sign] -> Result G_sign
forall a b. (a -> b) -> a -> b
$ (MaybeNode -> G_sign) -> [MaybeNode] -> [G_sign]
forall a b. (a -> b) -> [a] -> [b]
map MaybeNode -> G_sign
getMaybeSig [MaybeNode]
nodeSigs
     let unionName :: NodeName
unionName = DGraph -> IRI -> Node -> NodeName
ensureUniqueNames DGraph
dg (String -> IRI -> IRI
addSuffixToIRI "_union" IRI
sname) 1
         nodeContents :: DGNodeLab
nodeContents = NodeName -> DGOrigin -> G_theory -> DGNodeLab
newNodeLab 
                        (NodeName
unionName{extIndex :: Node
extIndex = 1}) 
                        DGOrigin
orig
                        (G_theory -> DGNodeLab) -> G_theory -> DGNodeLab
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
sigU SigId
ind
         node :: Node
node = DGraph -> Node
getNewNodeDG DGraph
dg
         dg' :: DGraph
dg' = LNode DGNodeLab -> DGraph -> DGraph
insNodeDG (Node
node, DGNodeLab
nodeContents) DGraph
dg
         inslink :: Result DGraph -> MaybeNode -> Result DGraph
inslink dgres :: Result DGraph
dgres nsig :: MaybeNode
nsig = do
             DGraph
dgv <- Result DGraph
dgres
             case MaybeNode
nsig of
                 EmptyNode _ -> Result DGraph
dgres
                 JustNode (NodeSig n :: Node
n sig :: G_sign
sig) -> do
                     GMorphism
incl <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lgraph G_sign
sig G_sign
sigUnion
                     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
$ LEdge DGLinkLab -> DGraph -> DGraph
insLEdgeNubDG
                       (Node
n, Node
node, GMorphism -> DGLinkOrigin -> DGLinkLab
globDefLink GMorphism
incl DGLinkOrigin
SeeTarget) DGraph
dgv
     DGraph
dg'' <- (Result DGraph -> MaybeNode -> Result DGraph)
-> Result DGraph -> [MaybeNode] -> Result DGraph
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Result DGraph -> MaybeNode -> Result DGraph
inslink (DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return DGraph
dg') [MaybeNode]
nodeSigs
     (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Node -> G_sign -> NodeSig
NodeSig Node
node G_sign
sigUnion, DGraph
dg'')

-- | Analyse unit declaration or definition
anaUnitDeclDefn :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts
  -> ExpOverrides
  -> ExtStUnitCtx -> UNIT_DECL_DEFN
  -> Result (Map.Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
{- ^ returns 1. extended static unit context 2. possibly modified
development graph 3. possibly modified UNIT_DECL_DEFN -}
anaUnitDeclDefn :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_DECL_DEFN
-> Result (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
anaUnitDeclDefn lgraph :: LogicGraph
lgraph libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo uctx :: ExtStUnitCtx
uctx@(buc :: StBasedUnitCtx
buc, _) udd :: UNIT_DECL_DEFN
udd = case UNIT_DECL_DEFN
udd of
  Unit_decl un' :: IRI
un' usp :: REF_SPEC
usp uts :: [Annoted UNIT_TERM]
uts pos :: Range
pos -> do
       IRI
unIRI <- GlobalAnnos -> ExpOverrides -> IRI -> Result IRI
expCurieR (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
un'
       let ustr :: String
ustr = IRI -> String
iriToStringShortUnsecure IRI
unIRI
       (dns :: MaybeDiagNode
dns, diag' :: Diag
diag', dg' :: DGraph
dg', uts' :: [Annoted UNIT_TERM]
uts') <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> Range
-> [Annoted UNIT_TERM]
-> Result (MaybeDiagNode, Diag, DGraph, [Annoted UNIT_TERM])
anaUnitImported LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
uctx Range
pos [Annoted UNIT_TERM]
uts
       let impSig :: MaybeNode
impSig = MaybeDiagNode -> MaybeNode
toMaybeNode MaybeDiagNode
dns
       (nodes :: [DiagNodeSig]
nodes, maybeRes :: Maybe DiagNodeSig
maybeRes, mDiag :: Maybe Diag
mDiag, rsig' :: RefSig
rsig', dg0 :: DGraph
dg0, usp' :: REF_SPEC
usp') <- 
           Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> MaybeNode
-> IRI
-> ExtStUnitCtx
-> Maybe RTPointer
-> REF_SPEC
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
      REF_SPEC)
anaRefSpec Bool
True LogicGraph
lgraph LibEnv
libEnv LibName
ln
           DGraph
dg' HetcatsOpts
opts ExpOverrides
eo MaybeNode
impSig IRI
unIRI (StBasedUnitCtx
buc, Diag
diag') Maybe RTPointer
forall a. Maybe a
Nothing REF_SPEC
usp
       usig :: UnitSig
usig@(UnitSig argSigs :: [NodeSig]
argSigs resultSig :: NodeSig
resultSig unionSig :: Maybe NodeSig
unionSig) <- RefSig -> Result UnitSig
getUnitSigFromRef RefSig
rsig'
       let (n :: Node
n, dg1 :: DGraph
dg1, rsig0 :: RefSig
rsig0) =
              case RefSig -> RTPointer
getPointerFromRef RefSig
rsig' of
               RTNone -> let
                             (n' :: Node
n', d' :: DGraph
d') = DGraph -> UnitSig -> String -> (Node, DGraph)
addNodeRT DGraph
dg0 UnitSig
usig String
ustr
                             r' :: RefSig
r' = RefSig -> RTPointer -> RefSig
setPointerInRef RefSig
rsig' (Node -> RTPointer
NPUnit Node
n')
                         in (Node
n', DGraph
d', RefSig
r')
               _ -> (RTPointer -> Node
refSource (RTPointer -> Node) -> RTPointer -> Node
forall a b. (a -> b) -> a -> b
$ RefSig -> RTPointer
getPointerFromRef RefSig
rsig', DGraph
dg0, RefSig
rsig')
{- is this above needed? when can rsig' have no pointer?
ANSWER: when it's just a unit sig -}
       (dg'' :: DGraph
dg'', rsig :: RefSig
rsig) <- case MaybeNode
impSig of
         EmptyNode _ -> do
          (resultSig' :: NodeSig
resultSig', dg2 :: DGraph
dg2) <- case Maybe NodeSig
unionSig of
              Just x :: NodeSig
x -> LogicGraph
-> DGraph
-> [MaybeNode]
-> DGOrigin
-> IRI
-> Result (NodeSig, DGraph)
nodeSigUnion LogicGraph
lgraph DGraph
dg1
                          [NodeSig -> MaybeNode
JustNode NodeSig
x, NodeSig -> MaybeNode
JustNode NodeSig
resultSig] DGOrigin
DGImports IRI
unIRI
              _ -> (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeSig
resultSig, DGraph
dg1)
          (DGraph, RefSig) -> Result (DGraph, RefSig)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph -> Node -> Bool -> String -> DGraph
updateNodeNameRT DGraph
dg2 Node
n Bool
False String
ustr,
                  RefSig -> UnitSig -> RefSig
setUnitSigInRef RefSig
rsig0 (UnitSig -> RefSig) -> UnitSig -> RefSig
forall a b. (a -> b) -> a -> b
$ [NodeSig] -> NodeSig -> Maybe NodeSig -> UnitSig
UnitSig [NodeSig]
argSigs NodeSig
resultSig' Maybe NodeSig
unionSig)
              -- S -> T becomes S -> S \cup T
         JustNode ns :: NodeSig
ns -> do
           let dg2 :: DGraph
dg2 = DGraph -> Node -> Bool -> String -> DGraph
updateNodeNameRT DGraph
dg1 Node
n Bool
False String
ustr
                -- this changes the name of the node in the RT
           (argUnion :: NodeSig
argUnion, dg3 :: DGraph
dg3) <- LogicGraph
-> DGraph
-> [MaybeNode]
-> DGOrigin
-> IRI
-> Result (NodeSig, DGraph)
nodeSigUnion LogicGraph
lgraph DGraph
dg2
                              ((NodeSig -> MaybeNode) -> [NodeSig] -> [MaybeNode]
forall a b. (a -> b) -> [a] -> [b]
map NodeSig -> MaybeNode
JustNode [NodeSig]
argSigs [MaybeNode] -> [MaybeNode] -> [MaybeNode]
forall a. [a] -> [a] -> [a]
++ [MaybeNode
impSig])
                              DGOrigin
DGImports IRI
unIRI
                -- union of the arguments with the imports
           (resultSig' :: NodeSig
resultSig', dg4 :: DGraph
dg4) <- LogicGraph
-> DGraph
-> [MaybeNode]
-> DGOrigin
-> IRI
-> Result (NodeSig, DGraph)
nodeSigUnion LogicGraph
lgraph DGraph
dg3
                          [NodeSig -> MaybeNode
JustNode NodeSig
resultSig, NodeSig -> MaybeNode
JustNode NodeSig
argUnion] DGOrigin
DGImports
                                IRI
unIRI
                {- union of the arguments with the result
                   F : S -> T given M
                   becomes F : M * S -> S_M \cup S \cup T -}
           let dgU :: DGraph
dgU = DGraph -> Node -> UnitSig -> DGraph
updateSigRT DGraph
dg4 Node
n (UnitSig -> DGraph) -> UnitSig -> DGraph
forall a b. (a -> b) -> a -> b
$ [NodeSig] -> NodeSig -> Maybe NodeSig -> UnitSig
UnitSig [] NodeSig
resultSig' Maybe NodeSig
forall a. Maybe a
Nothing
                -- now stores S \cup T
               usig' :: UnitSig
usig' = [NodeSig] -> NodeSig -> Maybe NodeSig -> UnitSig
UnitSig (NodeSig
ns NodeSig -> [NodeSig] -> [NodeSig]
forall a. a -> [a] -> [a]
: [NodeSig]
argSigs) NodeSig
resultSig' (Maybe NodeSig -> UnitSig) -> Maybe NodeSig -> UnitSig
forall a b. (a -> b) -> a -> b
$ NodeSig -> Maybe NodeSig
forall a. a -> Maybe a
Just NodeSig
argUnion
               (newN :: Node
newN, dgU' :: DGraph
dgU') = DGraph -> UnitSig -> String -> (Node, DGraph)
addNodeRT DGraph
dgU UnitSig
usig' ""
               newP :: RTPointer
newP = Node -> Map IRI RTPointer -> RTPointer
NPBranch Node
n (Map IRI RTPointer -> RTPointer) -> Map IRI RTPointer -> RTPointer
forall a b. (a -> b) -> a -> b
$ [(IRI, RTPointer)] -> Map IRI RTPointer
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
                      [(SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ String -> SIMPLE_ID
mkSimpleId "a", Node -> RTPointer
NPUnit Node
newN)]
               rUnit :: UnitSig
rUnit = [NodeSig] -> NodeSig -> Maybe NodeSig -> UnitSig
UnitSig [NodeSig]
argSigs NodeSig
resultSig' (Maybe NodeSig -> UnitSig) -> Maybe NodeSig -> UnitSig
forall a b. (a -> b) -> a -> b
$ NodeSig -> Maybe NodeSig
forall a. a -> Maybe a
Just NodeSig
argUnion
               rSig :: RefSig
rSig = RTPointer -> (UnitSig, Maybe BranchSig) -> RefSig
BranchRefSig RTPointer
newP (UnitSig
rUnit, BranchSig -> Maybe BranchSig
forall a. a -> Maybe a
Just (BranchSig -> Maybe BranchSig) -> BranchSig -> Maybe BranchSig
forall a b. (a -> b) -> a -> b
$ BStContext -> BranchSig
BranchStaticContext (BStContext -> BranchSig) -> BStContext -> BranchSig
forall a b. (a -> b) -> a -> b
$
                         IRI -> RefSig -> BStContext -> BStContext
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ String -> SIMPLE_ID
mkSimpleId "a")
                                (UnitSig -> RefSig
mkRefSigFromUnit UnitSig
usig')
                            BStContext
forall k a. Map k a
Map.empty)
           (DGraph, RefSig) -> Result (DGraph, RefSig)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph -> [Node] -> Node -> DGraph
addEdgesToNodeRT DGraph
dgU' [Node
newN] Node
n, RefSig
rSig)
             -- check the pointer
       let diag :: Diag
diag = Diag -> Maybe Diag -> Diag
forall a. a -> Maybe a -> a
fromMaybe Diag
diag' Maybe Diag
mDiag
           ud' :: UNIT_DECL_DEFN
ud' = IRI -> REF_SPEC -> [Annoted UNIT_TERM] -> Range -> UNIT_DECL_DEFN
Unit_decl IRI
unIRI REF_SPEC
usp' [Annoted UNIT_TERM]
uts' Range
pos
       case RefSig
rsig of
          ComponentRefSig _ _ -> String
-> Result (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
forall a. HasCallStack => String -> a
error (String
 -> Result
      (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN))
-> String
-> Result (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
forall a b. (a -> b) -> a -> b
$
                     "component refinement forbidden in arch spec: unit"
                     String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ustr
          _ ->
           if IRI -> StBasedUnitCtx -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member IRI
unIRI StBasedUnitCtx
buc
            then (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
-> String
-> Range
-> Result (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
forall a. a -> String -> Range -> Result a
plain_error (Map IRI RTPointer
forall k a. Map k a
Map.empty, ExtStUnitCtx
uctx, DGraph
dg'', UNIT_DECL_DEFN
ud')
               (IRI -> String
alreadyDefinedUnit IRI
unIRI) (IRI -> Range
iriPos IRI
unIRI)
            else do
                      _usigN :: UnitSig
_usigN@(UnitSig argSigsN :: [NodeSig]
argSigsN resultSig' :: NodeSig
resultSig' unionSigN :: Maybe NodeSig
unionSigN) <-
                          RefSig -> Result UnitSig
getUnitSigFromRef RefSig
rsig
                      (basedParUSig :: BasedUnitSig
basedParUSig, diag''' :: Diag
diag''') <- if [NodeSig] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NodeSig]
argSigsN then do
                          (dn' :: DiagNodeSig
dn', diag'' :: Diag
diag'') <- LogicGraph
-> Diag
-> [DiagNodeSig]
-> NodeSig
-> String
-> Result (DiagNodeSig, Diag)
extendDiagramIncl LogicGraph
lgraph Diag
diag
                             ((case MaybeDiagNode
dns of
                                JustDiagNode dn :: DiagNodeSig
dn -> [DiagNodeSig
dn]
                                _ -> []) [DiagNodeSig] -> [DiagNodeSig] -> [DiagNodeSig]
forall a. [a] -> [a] -> [a]
++
                              (case Maybe DiagNodeSig
maybeRes of
                                 Just x :: DiagNodeSig
x -> [DiagNodeSig
x]
                                 _ -> [])) NodeSig
resultSig' String
ustr
                          (BasedUnitSig, Diag) -> Result (BasedUnitSig, Diag)
forall (m :: * -> *) a. Monad m => a -> m a
return (DiagNodeSig -> RefSig -> BasedUnitSig
Based_unit_sig DiagNodeSig
dn' RefSig
rsig, Diag
diag'')
                          else if [DiagNodeSig] -> Node
forall (t :: * -> *) a. Foldable t => t a -> Node
length [DiagNodeSig]
nodes Node -> Node -> Bool
forall a. Ord a => a -> a -> Bool
< 2 then do
                                -- clarify the pointers here
                                 let rsig'' :: RefSig
rsig'' =
                                      RefSig -> RTPointer -> RefSig
setPointerInRef
                                       (RefSig -> UnitSig -> RefSig
setUnitSigInRef RefSig
rsig (UnitSig -> RefSig) -> UnitSig -> RefSig
forall a b. (a -> b) -> a -> b
$
                                         [NodeSig] -> NodeSig -> Maybe NodeSig -> UnitSig
UnitSig [NodeSig]
argSigsN NodeSig
resultSig' Maybe NodeSig
unionSigN)
                                       (Node -> RTPointer
NPUnit Node
n)
                                 (BasedUnitSig, Diag) -> Result (BasedUnitSig, Diag)
forall (m :: * -> *) a. Monad m => a -> m a
return (MaybeDiagNode -> RefSig -> BasedUnitSig
Based_par_unit_sig MaybeDiagNode
dns RefSig
rsig''
                                         , Diag
diag)
                                else do
             -- here we handle U : arch spec ASP with ASP parametric
                                 let rsig'' :: RefSig
rsig'' = RefSig -> RTPointer -> RefSig
setPointerInRef
                                              (RefSig -> UnitSig -> RefSig
setUnitSigInRef RefSig
rsig UnitSig
usig)
                                              (Node -> RTPointer
NPUnit Node
n)
                                 (BasedUnitSig, Diag) -> Result (BasedUnitSig, Diag)
forall (m :: * -> *) a. Monad m => a -> m a
return ([DiagNodeSig] -> RefSig -> BasedUnitSig
Based_lambda_unit_sig [DiagNodeSig]
nodes RefSig
rsig'',
                                         Diag
diag)
                      (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
-> Result (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(IRI, RTPointer)] -> Map IRI RTPointer
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(IRI
unIRI, RefSig -> RTPointer
getPointerFromRef RefSig
rsig)],
                       (IRI -> BasedUnitSig -> StBasedUnitCtx -> StBasedUnitCtx
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
unIRI BasedUnitSig
basedParUSig StBasedUnitCtx
buc, Diag
diag'''),
                                  DGraph
dg'', UNIT_DECL_DEFN
ud')
  Unit_defn un' :: IRI
un' uexp :: UNIT_EXPRESSION
uexp poss :: Range
poss -> do
       IRI
un <- GlobalAnnos -> ExpOverrides -> IRI -> Result IRI
expCurieR (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
un'
       (nodes :: [DiagNodeSig]
nodes, usig :: UnitSig
usig, diag :: Diag
diag, dg'' :: DGraph
dg'', uexp' :: UNIT_EXPRESSION
uexp') <-
         LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_EXPRESSION
-> Result ([DiagNodeSig], UnitSig, Diag, DGraph, UNIT_EXPRESSION)
anaUnitExpression LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
uctx UNIT_EXPRESSION
uexp
       let ud' :: UNIT_DECL_DEFN
ud' = IRI -> UNIT_EXPRESSION -> Range -> UNIT_DECL_DEFN
Unit_defn IRI
un UNIT_EXPRESSION
uexp' Range
poss
       if IRI -> StBasedUnitCtx -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member IRI
un StBasedUnitCtx
buc then
          (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
-> String
-> Range
-> Result (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
forall a. a -> String -> Range -> Result a
plain_error (Map IRI RTPointer
forall k a. Map k a
Map.empty, ExtStUnitCtx
uctx, DGraph
dg'', UNIT_DECL_DEFN
ud')
                      (IRI -> String
alreadyDefinedUnit IRI
un) (Range
 -> Result
      (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN))
-> Range
-> Result (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
forall a b. (a -> b) -> a -> b
$ IRI -> Range
iriPos IRI
un
          else case UnitSig
usig of
               {- we can use Map.insert as there are no mappings for
                  un in ps and bs (otherwise there would have been a
                  mapping in (ctx uctx)) -}
               UnitSig args :: [NodeSig]
args _ _ -> case [NodeSig]
args of
                 [] -> case [DiagNodeSig]
nodes of
                     [dn :: DiagNodeSig
dn] -> do
                              let bsig :: BasedUnitSig
bsig = DiagNodeSig -> RefSig -> BasedUnitSig
Based_unit_sig DiagNodeSig
dn (RefSig -> BasedUnitSig) -> RefSig -> BasedUnitSig
forall a b. (a -> b) -> a -> b
$
                                           UnitSig -> RefSig
mkBotSigFromUnit UnitSig
usig
                              (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
-> Result (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map IRI RTPointer
forall k a. Map k a
Map.empty,
                                      (IRI -> BasedUnitSig -> StBasedUnitCtx -> StBasedUnitCtx
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
un BasedUnitSig
bsig StBasedUnitCtx
buc, Diag
diag),
                                        DGraph
dg'', UNIT_DECL_DEFN
ud')
                     _ -> String
-> Result (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
forall a. HasCallStack => String -> a
error "anaUnitDeclDefn"
                 _ -> case [DiagNodeSig]
nodes of
                   _ : _ : _ ->
                     (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
-> Result (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map IRI RTPointer
forall k a. Map k a
Map.empty , (IRI -> BasedUnitSig -> StBasedUnitCtx -> StBasedUnitCtx
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
un
                             ([DiagNodeSig] -> RefSig -> BasedUnitSig
Based_lambda_unit_sig [DiagNodeSig]
nodes (RefSig -> BasedUnitSig) -> RefSig -> BasedUnitSig
forall a b. (a -> b) -> a -> b
$
                              UnitSig -> RefSig
mkBotSigFromUnit UnitSig
usig)
                             StBasedUnitCtx
buc, Diag
diag), DGraph
dg'', UNIT_DECL_DEFN
ud')
                   _ -> String
-> Result (Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
forall a. HasCallStack => String -> a
error "anaUnitDeclDefn:lambda expression"

-- | Analyse unit refs
anaUnitRef :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts
             -> ExpOverrides
             -> ExtStUnitCtx -> Maybe RTPointer -> UNIT_REF
             -> Result ((UNIT_NAME, RefSig), DGraph, UNIT_REF)
{- ^ returns 1. extended static unit context 2. possibly modified
development graph 3. possibly modified UNIT_DECL_DEFN -}
anaUnitRef :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> Maybe RTPointer
-> UNIT_REF
-> Result ((IRI, RefSig), DGraph, UNIT_REF)
anaUnitRef lgraph :: LogicGraph
lgraph libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo _uctx :: ExtStUnitCtx
_uctx@(_ggbuc :: StBasedUnitCtx
_ggbuc, _diag' :: Diag
_diag') rN :: Maybe RTPointer
rN
    (Unit_ref un' :: IRI
un' usp :: REF_SPEC
usp pos :: Range
pos) = do
  IRI
un <- GlobalAnnos -> ExpOverrides -> IRI -> Result IRI
expCurieR (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
un'
  let n :: Maybe RTPointer
n = case Maybe RTPointer
rN of
           Nothing -> Maybe RTPointer
forall a. Maybe a
Nothing
           Just (NPComp f :: Map IRI RTPointer
f) -> RTPointer -> Maybe RTPointer
forall a. a -> Maybe a
Just (RTPointer -> Maybe RTPointer) -> RTPointer -> Maybe RTPointer
forall a b. (a -> b) -> a -> b
$ RTPointer -> IRI -> Map IRI RTPointer -> RTPointer
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
                  (String -> RTPointer
forall a. HasCallStack => String -> a
error "component not in map!") IRI
un Map IRI RTPointer
f
           Just (NPBranch _ f :: Map IRI RTPointer
f) -> RTPointer -> Maybe RTPointer
forall a. a -> Maybe a
Just (RTPointer -> Maybe RTPointer) -> RTPointer -> Maybe RTPointer
forall a b. (a -> b) -> a -> b
$ RTPointer -> IRI -> Map IRI RTPointer -> RTPointer
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
                  (String -> RTPointer
forall a. HasCallStack => String -> a
error "component not in map!") IRI
un Map IRI RTPointer
f
           _ -> String -> Maybe RTPointer
forall a. HasCallStack => String -> a
error "components!"
  AnyLogic
curl <- String -> LogicGraph -> Result AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyLogic
lookupCurrentLogic "UNIT_REF" LogicGraph
lgraph
  let impSig :: MaybeNode
impSig = AnyLogic -> MaybeNode
EmptyNode AnyLogic
curl
  ( _, _, _, rsig :: RefSig
rsig, dg'' :: DGraph
dg'', usp' :: REF_SPEC
usp') <- 
         Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> MaybeNode
-> IRI
-> ExtStUnitCtx
-> Maybe RTPointer
-> REF_SPEC
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
      REF_SPEC)
anaRefSpec Bool
True LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo MaybeNode
impSig IRI
un
                    ExtStUnitCtx
emptyExtStUnitCtx Maybe RTPointer
n REF_SPEC
usp
  let ud' :: UNIT_REF
ud' = IRI -> REF_SPEC -> Range -> UNIT_REF
Unit_ref IRI
un REF_SPEC
usp' Range
pos
  ((IRI, RefSig), DGraph, UNIT_REF)
-> Result ((IRI, RefSig), DGraph, UNIT_REF)
forall (m :: * -> *) a. Monad m => a -> m a
return ((IRI
un, RefSig
rsig), DGraph
dg'', UNIT_REF
ud')


-- | Analyse unit imports
anaUnitImported :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts
    -> ExpOverrides
    -> ExtStUnitCtx -> Range -> [Annoted UNIT_TERM]
    -> Result (MaybeDiagNode, Diag, DGraph, [Annoted UNIT_TERM])
anaUnitImported :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> Range
-> [Annoted UNIT_TERM]
-> Result (MaybeDiagNode, Diag, DGraph, [Annoted UNIT_TERM])
anaUnitImported lgraph :: LogicGraph
lgraph libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo uctx :: ExtStUnitCtx
uctx@(_, diag :: Diag
diag) poss :: Range
poss terms :: [Annoted UNIT_TERM]
terms =
  case [Annoted UNIT_TERM]
terms of
  [] -> do
    AnyLogic
curl <- String -> LogicGraph -> Result AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyLogic
lookupCurrentLogic "UnitImported" LogicGraph
lgraph
    (MaybeDiagNode, Diag, DGraph, [Annoted UNIT_TERM])
-> Result (MaybeDiagNode, Diag, DGraph, [Annoted UNIT_TERM])
forall (m :: * -> *) a. Monad m => a -> m a
return (AnyLogic -> MaybeDiagNode
EmptyDiagNode AnyLogic
curl, Diag
diag, DGraph
dg, [])
  _ -> do
       (dnsigs :: [DiagNodeSig]
dnsigs, diag' :: Diag
diag', dg' :: DGraph
dg', terms' :: [Annoted UNIT_TERM]
terms') <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> [Annoted UNIT_TERM]
-> Result ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])
anaUnitImported' LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
uctx [Annoted UNIT_TERM]
terms
       (sig :: NodeSig
sig, dg'' :: DGraph
dg'') <- LogicGraph
-> DGraph
-> [MaybeNode]
-> DGOrigin
-> IRI
-> Result (NodeSig, DGraph)
nodeSigUnion LogicGraph
lgraph DGraph
dg'
                      ((DiagNodeSig -> MaybeNode) -> [DiagNodeSig] -> [MaybeNode]
forall a b. (a -> b) -> [a] -> [b]
map (NodeSig -> MaybeNode
JustNode (NodeSig -> MaybeNode)
-> (DiagNodeSig -> NodeSig) -> DiagNodeSig -> MaybeNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DiagNodeSig -> NodeSig
getSigFromDiag) [DiagNodeSig]
dnsigs) DGOrigin
DGImports
                      (SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ String -> SIMPLE_ID
mkSimpleId "imports")
       let pos :: Range
pos = Range -> Range
getPosUnitImported Range
poss
       [(Node, GMorphism)]
sink <- LogicGraph
-> [DiagNodeSig] -> NodeSig -> Result [(Node, GMorphism)]
inclusionSink LogicGraph
lgraph [DiagNodeSig]
dnsigs NodeSig
sig
       () <- HetcatsOpts
-> Range -> Diag -> [(Node, GMorphism)] -> String -> Result ()
assertAmalgamability HetcatsOpts
opts Range
pos Diag
diag' [(Node, GMorphism)]
sink ("imports:" String -> String -> String
forall a. [a] -> [a] -> [a]
++
              (String -> Annoted UNIT_TERM -> String)
-> String -> [Annoted UNIT_TERM] -> String
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ x :: String
x y :: Annoted UNIT_TERM
y -> String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (LogicGraph -> Annoted UNIT_TERM -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lgraph Annoted UNIT_TERM
y)) "" [Annoted UNIT_TERM]
terms)
       (dnsig :: DiagNodeSig
dnsig, diag'' :: Diag
diag'') <- LogicGraph
-> Diag
-> [DiagNodeSig]
-> NodeSig
-> String
-> Result (DiagNodeSig, Diag)
extendDiagramIncl LogicGraph
lgraph Diag
diag' [DiagNodeSig]
dnsigs NodeSig
sig
         (String -> Result (DiagNodeSig, Diag))
-> ([Doc] -> String) -> [Doc] -> Result (DiagNodeSig, Diag)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> ([Doc] -> Doc) -> [Doc] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
sepByCommas ([Doc] -> Result (DiagNodeSig, Diag))
-> [Doc] -> Result (DiagNodeSig, Diag)
forall a b. (a -> b) -> a -> b
$ (Annoted UNIT_TERM -> Doc) -> [Annoted UNIT_TERM] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (LogicGraph -> Annoted UNIT_TERM -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lgraph) [Annoted UNIT_TERM]
terms
       (MaybeDiagNode, Diag, DGraph, [Annoted UNIT_TERM])
-> Result (MaybeDiagNode, Diag, DGraph, [Annoted UNIT_TERM])
forall (m :: * -> *) a. Monad m => a -> m a
return (DiagNodeSig -> MaybeDiagNode
JustDiagNode DiagNodeSig
dnsig, Diag
diag'', DGraph
dg'', [Annoted UNIT_TERM]
terms')

anaUnitImported' :: LogicGraph -> LibEnv -> LibName -> DGraph
    -> HetcatsOpts
    -> ExpOverrides
    -> ExtStUnitCtx -> [Annoted UNIT_TERM]
    -> Result ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])
anaUnitImported' :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> [Annoted UNIT_TERM]
-> Result ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])
anaUnitImported' lgraph :: LogicGraph
lgraph libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo uctx :: ExtStUnitCtx
uctx@(buc :: StBasedUnitCtx
buc, diag :: Diag
diag) ts :: [Annoted UNIT_TERM]
ts = case [Annoted UNIT_TERM]
ts of
    [] -> ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])
-> Result ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Diag
diag, DGraph
dg, [])
    ut :: Annoted UNIT_TERM
ut : uts :: [Annoted UNIT_TERM]
uts -> do
       (dnsig :: DiagNodeSig
dnsig, diag' :: Diag
diag', dg' :: DGraph
dg', ut' :: UNIT_TERM
ut') <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_TERM
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
anaUnitTerm LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
uctx (Annoted UNIT_TERM -> UNIT_TERM
forall a. Annoted a -> a
item Annoted UNIT_TERM
ut)
       (dnsigs :: [DiagNodeSig]
dnsigs, diag'' :: Diag
diag'', dg'' :: DGraph
dg'', uts' :: [Annoted UNIT_TERM]
uts') <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> [Annoted UNIT_TERM]
-> Result ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])
anaUnitImported' LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg' HetcatsOpts
opts ExpOverrides
eo (StBasedUnitCtx
buc, Diag
diag') [Annoted UNIT_TERM]
uts
       ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])
-> Result ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])
forall (m :: * -> *) a. Monad m => a -> m a
return (DiagNodeSig
dnsig DiagNodeSig -> [DiagNodeSig] -> [DiagNodeSig]
forall a. a -> [a] -> [a]
: [DiagNodeSig]
dnsigs, Diag
diag'', DGraph
dg'', UNIT_TERM -> Annoted UNIT_TERM -> Annoted UNIT_TERM
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted UNIT_TERM
ut' Annoted UNIT_TERM
ut Annoted UNIT_TERM -> [Annoted UNIT_TERM] -> [Annoted UNIT_TERM]
forall a. a -> [a] -> [a]
: [Annoted UNIT_TERM]
uts')

-- | Analyse an unit expression
anaUnitExpression :: LogicGraph -> LibEnv -> LibName -> DGraph
    -> HetcatsOpts
    -> ExpOverrides
    -> ExtStUnitCtx -> UNIT_EXPRESSION
    -> Result ([DiagNodeSig], UnitSig, Diag, DGraph, UNIT_EXPRESSION)
anaUnitExpression :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_EXPRESSION
-> Result ([DiagNodeSig], UnitSig, Diag, DGraph, UNIT_EXPRESSION)
anaUnitExpression lgraph :: LogicGraph
lgraph libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo uctx :: ExtStUnitCtx
uctx@(buc :: StBasedUnitCtx
buc, diag :: Diag
diag)
    uexp :: UNIT_EXPRESSION
uexp@(Unit_expression ubs :: [UNIT_BINDING]
ubs ut :: Annoted UNIT_TERM
ut poss :: Range
poss) = case [UNIT_BINDING]
ubs of
  [] -> do
       (dnsig :: DiagNodeSig
dnsig@(Diag_node_sig _ ns' :: NodeSig
ns'), diag' :: Diag
diag', dg' :: DGraph
dg', ut' :: UNIT_TERM
ut') <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_TERM
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
anaUnitTerm LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
uctx (Annoted UNIT_TERM -> UNIT_TERM
forall a. Annoted a -> a
item Annoted UNIT_TERM
ut)
       ([DiagNodeSig], UnitSig, Diag, DGraph, UNIT_EXPRESSION)
-> Result ([DiagNodeSig], UnitSig, Diag, DGraph, UNIT_EXPRESSION)
forall (m :: * -> *) a. Monad m => a -> m a
return ([DiagNodeSig
dnsig], [NodeSig] -> NodeSig -> Maybe NodeSig -> UnitSig
UnitSig [] NodeSig
ns' Maybe NodeSig
forall a. Maybe a
Nothing, Diag
diag', DGraph
dg',
               [UNIT_BINDING] -> Annoted UNIT_TERM -> Range -> UNIT_EXPRESSION
Unit_expression [] (UNIT_TERM -> Annoted UNIT_TERM -> Annoted UNIT_TERM
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted UNIT_TERM
ut' Annoted UNIT_TERM
ut) Range
poss)
  _ -> do
       (args :: [(IRI, NodeSig)]
args, dg' :: DGraph
dg', ubs' :: [UNIT_BINDING]
ubs') <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> [UNIT_BINDING]
-> Result ([(IRI, NodeSig)], DGraph, [UNIT_BINDING])
anaUnitBindings LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
uctx [UNIT_BINDING]
ubs
       let dexp :: String
dexp = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ LogicGraph -> UNIT_EXPRESSION -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lgraph UNIT_EXPRESSION
uexp
           insNodes :: Diag
-> [(a, NodeSig)]
-> Map a BasedUnitSig
-> Result ([DiagNodeSig], Diag, Map a BasedUnitSig)
insNodes diag0 :: Diag
diag0 [] buc0 :: Map a BasedUnitSig
buc0 = ([DiagNodeSig], Diag, Map a BasedUnitSig)
-> Result ([DiagNodeSig], Diag, Map a BasedUnitSig)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Diag
diag0, Map a BasedUnitSig
buc0)
           insNodes diag0 :: Diag
diag0 ((un :: a
un, nsig :: NodeSig
nsig) : args0 :: [(a, NodeSig)]
args0) buc0 :: Map a BasedUnitSig
buc0 =
               do (dnsig :: DiagNodeSig
dnsig, diag' :: Diag
diag') <- LogicGraph
-> Diag
-> [DiagNodeSig]
-> NodeSig
-> String
-> Result (DiagNodeSig, Diag)
extendDiagramIncl LogicGraph
lgraph Diag
diag0 []
                           NodeSig
nsig (String -> Result (DiagNodeSig, Diag))
-> String -> Result (DiagNodeSig, Diag)
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
un
                  {- we made sure in anaUnitBindings that there's no
                     mapping for un in buc so we can just use
                     Map.insert;
                   here RTNone actually makes sense -}
                  let rsig :: RefSig
rsig = RTPointer -> (UnitSig, Maybe BranchSig) -> RefSig
BranchRefSig RTPointer
RTNone
                               ([NodeSig] -> NodeSig -> Maybe NodeSig -> UnitSig
UnitSig [] NodeSig
nsig Maybe NodeSig
forall a. Maybe a
Nothing, Maybe BranchSig
forall a. Maybe a
Nothing)
                      buc' :: Map a BasedUnitSig
buc' = a -> BasedUnitSig -> Map a BasedUnitSig -> Map a BasedUnitSig
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
un (DiagNodeSig -> RefSig -> BasedUnitSig
Based_unit_sig DiagNodeSig
dnsig RefSig
rsig) Map a BasedUnitSig
buc0
                  (dnsigs :: [DiagNodeSig]
dnsigs, diag'' :: Diag
diag'', buc'' :: Map a BasedUnitSig
buc'') <- Diag
-> [(a, NodeSig)]
-> Map a BasedUnitSig
-> Result ([DiagNodeSig], Diag, Map a BasedUnitSig)
insNodes Diag
diag' [(a, NodeSig)]
args0 Map a BasedUnitSig
buc'
                  ([DiagNodeSig], Diag, Map a BasedUnitSig)
-> Result ([DiagNodeSig], Diag, Map a BasedUnitSig)
forall (m :: * -> *) a. Monad m => a -> m a
return (DiagNodeSig
dnsig DiagNodeSig -> [DiagNodeSig] -> [DiagNodeSig]
forall a. a -> [a] -> [a]
: [DiagNodeSig]
dnsigs, Diag
diag'', Map a BasedUnitSig
buc'')
       (pardnsigs :: [DiagNodeSig]
pardnsigs, diag'' :: Diag
diag'', buc' :: StBasedUnitCtx
buc') <- Diag
-> [(IRI, NodeSig)]
-> StBasedUnitCtx
-> Result ([DiagNodeSig], Diag, StBasedUnitCtx)
forall a.
(Show a, Ord a) =>
Diag
-> [(a, NodeSig)]
-> Map a BasedUnitSig
-> Result ([DiagNodeSig], Diag, Map a BasedUnitSig)
insNodes Diag
diag [(IRI, NodeSig)]
args StBasedUnitCtx
buc
       (resnsig :: NodeSig
resnsig, _) <- LogicGraph
-> DGraph
-> [MaybeNode]
-> DGOrigin
-> IRI
-> Result (NodeSig, DGraph)
nodeSigUnion LogicGraph
lgraph DGraph
dg'
                              (((IRI, NodeSig) -> MaybeNode) -> [(IRI, NodeSig)] -> [MaybeNode]
forall a b. (a -> b) -> [a] -> [b]
map (NodeSig -> MaybeNode
JustNode (NodeSig -> MaybeNode)
-> ((IRI, NodeSig) -> NodeSig) -> (IRI, NodeSig) -> MaybeNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IRI, NodeSig) -> NodeSig
forall a b. (a, b) -> b
snd) [(IRI, NodeSig)]
args) DGOrigin
DGFormalParams
                              (SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ String -> SIMPLE_ID
mkSimpleId "union")
       (Diag_node_sig nU :: Node
nU _, diagI :: Diag
diagI) <-
                             LogicGraph
-> Diag
-> [DiagNodeSig]
-> NodeSig
-> String
-> Result (DiagNodeSig, Diag)
extendDiagramIncl LogicGraph
lgraph Diag
diag''
                             [DiagNodeSig]
pardnsigs NodeSig
resnsig String
dexp
               {- only add the union to ensure compatibility of
               formal parameters
               but remove afterwards to be able to check
               compatibility of actual parameters: matchDiagram below -}
       (p :: DiagNodeSig
p@(Diag_node_sig _ pnsig :: NodeSig
pnsig), diag''' :: Diag
diag''', dg''' :: DGraph
dg''', ut' :: UNIT_TERM
ut') <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_TERM
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
anaUnitTerm LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg' HetcatsOpts
opts ExpOverrides
eo (StBasedUnitCtx
buc', Diag
diagI) (Annoted UNIT_TERM -> UNIT_TERM
forall a. Annoted a -> a
item Annoted UNIT_TERM
ut)
       -- check amalgamability conditions
       let pos :: Range
pos = UNIT_EXPRESSION -> Range
getPosUnitExpression UNIT_EXPRESSION
uexp
           checkSubSign :: t DiagNodeSig -> NodeSig -> Bool
checkSubSign dnsigs :: t DiagNodeSig
dnsigs nsup :: NodeSig
nsup =
             (DiagNodeSig -> Bool) -> t DiagNodeSig -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ dnsub :: DiagNodeSig
dnsub -> LogicGraph -> G_sign -> G_sign -> Bool
isSubGsign LogicGraph
lgraph (NodeSig -> G_sign
getSig (NodeSig -> G_sign) -> NodeSig -> G_sign
forall a b. (a -> b) -> a -> b
$ DiagNodeSig -> NodeSig
getSigFromDiag DiagNodeSig
dnsub)
                  (G_sign -> Bool) -> G_sign -> Bool
forall a b. (a -> b) -> a -> b
$ NodeSig -> G_sign
getSig NodeSig
nsup) t DiagNodeSig
dnsigs
       -- check that signatures in pardnsigs are subsignatures of pnsig
       if [DiagNodeSig] -> NodeSig -> Bool
forall (t :: * -> *).
Foldable t =>
t DiagNodeSig -> NodeSig -> Bool
checkSubSign [DiagNodeSig]
pardnsigs NodeSig
pnsig
          then
            do
               [(Node, GMorphism)]
sink <- LogicGraph
-> [DiagNodeSig] -> NodeSig -> Result [(Node, GMorphism)]
inclusionSink LogicGraph
lgraph (DiagNodeSig
p DiagNodeSig -> [DiagNodeSig] -> [DiagNodeSig]
forall a. a -> [a] -> [a]
: [DiagNodeSig]
pardnsigs) NodeSig
pnsig
               () <-
                     HetcatsOpts
-> Range -> Diag -> [(Node, GMorphism)] -> String -> Result ()
assertAmalgamability HetcatsOpts
opts Range
pos Diag
diag''' [(Node, GMorphism)]
sink
                      ("subsignature test for: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                       Doc -> String
forall a. Show a => a -> String
show (LogicGraph -> UNIT_EXPRESSION -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lgraph UNIT_EXPRESSION
uexp))
               -- add new node to the diagram
               let (_, diag4 :: Diag
diag4) = Node -> Diag -> (MContext DiagNodeLab DiagLinkLab, Diag)
matchDiagram Node
nU Diag
diag'''
               ([DiagNodeSig], UnitSig, Diag, DGraph, UNIT_EXPRESSION)
-> Result ([DiagNodeSig], UnitSig, Diag, DGraph, UNIT_EXPRESSION)
forall (m :: * -> *) a. Monad m => a -> m a
return (DiagNodeSig
p DiagNodeSig -> [DiagNodeSig] -> [DiagNodeSig]
forall a. a -> [a] -> [a]
: [DiagNodeSig]
pardnsigs,
                        [NodeSig] -> NodeSig -> Maybe NodeSig -> UnitSig
UnitSig (((IRI, NodeSig) -> NodeSig) -> [(IRI, NodeSig)] -> [NodeSig]
forall a b. (a -> b) -> [a] -> [b]
map (IRI, NodeSig) -> NodeSig
forall a b. (a, b) -> b
snd [(IRI, NodeSig)]
args) NodeSig
pnsig (Maybe NodeSig -> UnitSig) -> Maybe NodeSig -> UnitSig
forall a b. (a -> b) -> a -> b
$ NodeSig -> Maybe NodeSig
forall a. a -> Maybe a
Just NodeSig
resnsig,
                          -- check!
                        Diag
diag4, DGraph
dg''',
                       [UNIT_BINDING] -> Annoted UNIT_TERM -> Range -> UNIT_EXPRESSION
Unit_expression [UNIT_BINDING]
ubs' (UNIT_TERM -> Annoted UNIT_TERM -> Annoted UNIT_TERM
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted UNIT_TERM
ut' Annoted UNIT_TERM
ut) Range
poss)
          else -- report an error
              String
-> Range
-> Result ([DiagNodeSig], UnitSig, Diag, DGraph, UNIT_EXPRESSION)
forall a. String -> Range -> Result a
fatal_error
          ("The body signature does not extend the parameter signatures in\n"
           String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
dexp) Range
pos

{- | Analyse a list of unit bindings. Ensures that the unit names are
not present in extended static unit context and that there are no
duplicates among them. -}
anaUnitBindings :: LogicGraph -> LibEnv ->  LibName -> DGraph
    -> HetcatsOpts
    -> ExpOverrides
    -> ExtStUnitCtx -> [UNIT_BINDING]
    -> Result ([(IRI, NodeSig)], DGraph, [UNIT_BINDING])
anaUnitBindings :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> [UNIT_BINDING]
-> Result ([(IRI, NodeSig)], DGraph, [UNIT_BINDING])
anaUnitBindings lgraph :: LogicGraph
lgraph libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo uctx :: ExtStUnitCtx
uctx@(buc :: StBasedUnitCtx
buc, _) bs :: [UNIT_BINDING]
bs = case [UNIT_BINDING]
bs of
          [] -> ([(IRI, NodeSig)], DGraph, [UNIT_BINDING])
-> Result ([(IRI, NodeSig)], DGraph, [UNIT_BINDING])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], DGraph
dg, [])
          Unit_binding un' :: IRI
un' usp :: UNIT_SPEC
usp poss :: Range
poss : ubs :: [UNIT_BINDING]
ubs -> do
               IRI
un <- GlobalAnnos -> ExpOverrides -> IRI -> Result IRI
expCurieR (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
un'
               let unpos :: Range
unpos = IRI -> Range
iriPos IRI
un
               AnyLogic
curl <- String -> LogicGraph -> Result AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyLogic
lookupCurrentLogic "UNIT_BINDINGS" LogicGraph
lgraph
               (BranchRefSig _ (UnitSig argSigs :: [NodeSig]
argSigs nsig :: NodeSig
nsig _, _), dg' :: DGraph
dg', usp' :: UNIT_SPEC
usp') <-
                   LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> IRI
-> MaybeNode
-> Maybe RTPointer
-> UNIT_SPEC
-> Result (RefSig, DGraph, UNIT_SPEC)
anaUnitSpec LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo 
                               IRI
un (AnyLogic -> MaybeNode
EmptyNode AnyLogic
curl) Maybe RTPointer
forall a. Maybe a
Nothing UNIT_SPEC
usp
                         -- TODO: is un OK above? MC: yes, names are unique
               let ub' :: UNIT_BINDING
ub' = IRI -> UNIT_SPEC -> Range -> UNIT_BINDING
Unit_binding IRI
un UNIT_SPEC
usp' Range
poss
               case [NodeSig]
argSigs of
                    _ : _ -> ([(IRI, NodeSig)], DGraph, [UNIT_BINDING])
-> String
-> Range
-> Result ([(IRI, NodeSig)], DGraph, [UNIT_BINDING])
forall a. a -> String -> Range -> Result a
plain_error ([], DGraph
dg', [])
                             ("An argument unit "
                              String -> String -> String
forall a. [a] -> [a] -> [a]
++ IRI -> String
iriToStringUnsecure IRI
un
                              String -> String -> String
forall a. [a] -> [a] -> [a]
++ " must not be parameterized") Range
unpos
                    [] ->
                        do (args :: [(IRI, NodeSig)]
args, dg'' :: DGraph
dg'', ubs' :: [UNIT_BINDING]
ubs') <- LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> [UNIT_BINDING]
-> Result ([(IRI, NodeSig)], DGraph, [UNIT_BINDING])
anaUnitBindings LogicGraph
lgraph LibEnv
libEnv LibName
ln
                               DGraph
dg' HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
uctx [UNIT_BINDING]
ubs
                           let args' :: [(IRI, NodeSig)]
args' = (IRI
un, NodeSig
nsig) (IRI, NodeSig) -> [(IRI, NodeSig)] -> [(IRI, NodeSig)]
forall a. a -> [a] -> [a]
: [(IRI, NodeSig)]
args
                           if IRI -> StBasedUnitCtx -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member IRI
un StBasedUnitCtx
buc
                              then ([(IRI, NodeSig)], DGraph, [UNIT_BINDING])
-> String
-> Range
-> Result ([(IRI, NodeSig)], DGraph, [UNIT_BINDING])
forall a. a -> String -> Range -> Result a
plain_error ([(IRI, NodeSig)]
args', DGraph
dg'', UNIT_BINDING
ub' UNIT_BINDING -> [UNIT_BINDING] -> [UNIT_BINDING]
forall a. a -> [a] -> [a]
: [UNIT_BINDING]
ubs')
                                   (IRI -> String
alreadyDefinedUnit IRI
un) Range
unpos
                              else case IRI -> [(IRI, NodeSig)] -> Maybe NodeSig
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup IRI
un [(IRI, NodeSig)]
args of
                                    Just _ ->
                                          ([(IRI, NodeSig)], DGraph, [UNIT_BINDING])
-> String
-> Range
-> Result ([(IRI, NodeSig)], DGraph, [UNIT_BINDING])
forall a. a -> String -> Range -> Result a
plain_error ([(IRI, NodeSig)]
args', DGraph
dg'', UNIT_BINDING
ub' UNIT_BINDING -> [UNIT_BINDING] -> [UNIT_BINDING]
forall a. a -> [a] -> [a]
: [UNIT_BINDING]
ubs')
                                          (IRI -> String
alreadyDefinedUnit IRI
un) Range
unpos
                                    Nothing -> ([(IRI, NodeSig)], DGraph, [UNIT_BINDING])
-> Result ([(IRI, NodeSig)], DGraph, [UNIT_BINDING])
forall (m :: * -> *) a. Monad m => a -> m a
return ([(IRI, NodeSig)]
args', DGraph
dg'', UNIT_BINDING
ub' UNIT_BINDING -> [UNIT_BINDING] -> [UNIT_BINDING]
forall a. a -> [a] -> [a]
: [UNIT_BINDING]
ubs')

-- | Analyse a list of unit terms
anaUnitTerms :: LogicGraph -> LibEnv -> LibName -> DGraph
    -> HetcatsOpts
    -> ExpOverrides
    -> ExtStUnitCtx -> [Annoted UNIT_TERM]
    -> Result ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])
anaUnitTerms :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> [Annoted UNIT_TERM]
-> Result ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])
anaUnitTerms lgraph :: LogicGraph
lgraph libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo uctx :: ExtStUnitCtx
uctx@(buc :: StBasedUnitCtx
buc, diag :: Diag
diag) ts :: [Annoted UNIT_TERM]
ts = case [Annoted UNIT_TERM]
ts of
  [] -> ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])
-> Result ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Diag
diag, DGraph
dg, [])
  ut :: Annoted UNIT_TERM
ut : uts :: [Annoted UNIT_TERM]
uts -> do
       (dnsig :: DiagNodeSig
dnsig, diag' :: Diag
diag', dg' :: DGraph
dg', ut' :: UNIT_TERM
ut') <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_TERM
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
anaUnitTerm LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
uctx (Annoted UNIT_TERM -> UNIT_TERM
forall a. Annoted a -> a
item Annoted UNIT_TERM
ut)
       (dnsigs :: [DiagNodeSig]
dnsigs, diag'' :: Diag
diag'', dg'' :: DGraph
dg'', uts' :: [Annoted UNIT_TERM]
uts') <- LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> [Annoted UNIT_TERM]
-> Result ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])
anaUnitTerms LogicGraph
lgraph LibEnv
libEnv LibName
ln
               DGraph
dg' HetcatsOpts
opts ExpOverrides
eo (StBasedUnitCtx
buc, Diag
diag') [Annoted UNIT_TERM]
uts
       ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])
-> Result ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])
forall (m :: * -> *) a. Monad m => a -> m a
return (DiagNodeSig
dnsig DiagNodeSig -> [DiagNodeSig] -> [DiagNodeSig]
forall a. a -> [a] -> [a]
: [DiagNodeSig]
dnsigs, Diag
diag'', DGraph
dg'', UNIT_TERM -> Annoted UNIT_TERM -> Annoted UNIT_TERM
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted UNIT_TERM
ut' Annoted UNIT_TERM
ut Annoted UNIT_TERM -> [Annoted UNIT_TERM] -> [Annoted UNIT_TERM]
forall a. a -> [a] -> [a]
: [Annoted UNIT_TERM]
uts')

-- | Analyse an unit term
anaUnitTerm :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts
  -> ExpOverrides
  -> ExtStUnitCtx -> UNIT_TERM -> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
anaUnitTerm :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_TERM
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
anaUnitTerm lgraph :: LogicGraph
lgraph libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo uctx :: ExtStUnitCtx
uctx@(buc :: StBasedUnitCtx
buc, diag :: Diag
diag) utrm :: UNIT_TERM
utrm =
  let pos :: Range
pos = UNIT_TERM -> Range
getPosUnitTerm UNIT_TERM
utrm
      utStr :: String
utStr = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ LogicGraph -> UNIT_TERM -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lgraph UNIT_TERM
utrm
  in case UNIT_TERM
utrm of
  Unit_reduction ut :: Annoted UNIT_TERM
ut restr :: RESTRICTION
restr -> do
       let orig :: DGOrigin
orig = MaybeRestricted -> Set G_symbol -> DGOrigin
DGRestriction (RESTRICTION -> MaybeRestricted
Restricted RESTRICTION
restr) Set G_symbol
forall a. Set a
Set.empty
       (p :: DiagNodeSig
p@(Diag_node_sig iNode :: Node
iNode _), diag1 :: Diag
diag1, dg1 :: DGraph
dg1, ut' :: UNIT_TERM
ut') <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_TERM
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
anaUnitTerm LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
uctx (Annoted UNIT_TERM -> UNIT_TERM
forall a. Annoted a -> a
item Annoted UNIT_TERM
ut)
       AnyLogic
curl <- String -> LogicGraph -> Result AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyLogic
lookupCurrentLogic "UnitTerm" LogicGraph
lgraph
       (incl :: GMorphism
incl, msigma :: Maybe GMorphism
msigma) <- LogicGraph
-> G_sign
-> G_sign
-> HetcatsOpts
-> RESTRICTION
-> Result (GMorphism, Maybe GMorphism)
anaRestriction LogicGraph
lgraph (AnyLogic -> G_sign
emptyG_sign AnyLogic
curl)
                         (NodeSig -> G_sign
getSig (DiagNodeSig -> NodeSig
getSigFromDiag DiagNodeSig
p)) HetcatsOpts
opts RESTRICTION
restr
       let i :: IRI
i = String -> Node -> IRI
addSuffixToNode "_reduction" Node
iNode
       (q :: DiagNodeSig
q@(Diag_node_sig qn :: Node
qn _), diag' :: Diag
diag', dg' :: DGraph
dg') <-
           Range
-> LogicGraph
-> Diag
-> DGraph
-> DiagNodeSig
-> GMorphism
-> IRI
-> String
-> DGOrigin
-> Result (DiagNodeSig, Diag, DGraph)
extendDiagramWithMorphismRevHide Range
pos LogicGraph
lgraph Diag
diag1 DGraph
dg1 DiagNodeSig
p GMorphism
incl IRI
i String
utStr
            DGOrigin
orig
       case Maybe GMorphism
msigma of
                  Nothing ->
                  {- the renaming morphism is just identity, so
                  there's no need to extend the diagram
                   -}
                      (DiagNodeSig, Diag, DGraph, UNIT_TERM)
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
forall (m :: * -> *) a. Monad m => a -> m a
return (DiagNodeSig
q, Diag
diag', DGraph
dg',
                                  Annoted UNIT_TERM -> RESTRICTION -> UNIT_TERM
Unit_reduction (UNIT_TERM -> Annoted UNIT_TERM -> Annoted UNIT_TERM
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted UNIT_TERM
ut' Annoted UNIT_TERM
ut) RESTRICTION
restr)
                  Just sigma :: GMorphism
sigma ->
                      do
                         -- check amalgamability conditions
                         let sink :: [(Node, GMorphism)]
sink = [(Node
qn, GMorphism
sigma)]
                             iN :: IRI
iN = String -> Node -> IRI
addSuffixToNode "_amalg_reduct" Node
qn
                         () <- HetcatsOpts
-> Range -> Diag -> [(Node, GMorphism)] -> String -> Result ()
assertAmalgamability HetcatsOpts
opts Range
pos Diag
diag' [(Node, GMorphism)]
sink String
utStr
                         (q' :: DiagNodeSig
q', diag'' :: Diag
diag'', dg'' :: DGraph
dg'') <- Range
-> LogicGraph
-> Diag
-> DGraph
-> DiagNodeSig
-> GMorphism
-> IRI
-> String
-> DGOrigin
-> Result (DiagNodeSig, Diag, DGraph)
extendDiagramWithMorphism Range
pos
                            LogicGraph
lgraph Diag
diag' DGraph
dg' DiagNodeSig
q GMorphism
sigma IRI
iN String
utStr DGOrigin
orig
                         (DiagNodeSig, Diag, DGraph, UNIT_TERM)
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
forall (m :: * -> *) a. Monad m => a -> m a
return (DiagNodeSig
q', Diag
diag'', DGraph
dg'',
                                   Annoted UNIT_TERM -> RESTRICTION -> UNIT_TERM
Unit_reduction
                                   (UNIT_TERM -> Annoted UNIT_TERM -> Annoted UNIT_TERM
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted UNIT_TERM
ut' Annoted UNIT_TERM
ut) RESTRICTION
restr)
  Unit_translation ut :: Annoted UNIT_TERM
ut ren :: RENAMING
ren -> do
       (dnsig :: DiagNodeSig
dnsig@(Diag_node_sig p :: Node
p _), diag1 :: Diag
diag1, dg1 :: DGraph
dg1, ut' :: UNIT_TERM
ut') <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_TERM
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
anaUnitTerm LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
uctx (Annoted UNIT_TERM -> UNIT_TERM
forall a. Annoted a -> a
item Annoted UNIT_TERM
ut)
       -- EmptyNode $ error ... should be replaced with local env!
       GMorphism
gMorph <- LogicGraph
-> MaybeNode
-> G_sign
-> HetcatsOpts
-> RENAMING
-> Result GMorphism
anaRenaming LogicGraph
lgraph
                 (AnyLogic -> MaybeNode
EmptyNode (AnyLogic -> MaybeNode) -> AnyLogic -> MaybeNode
forall a b. (a -> b) -> a -> b
$ String -> AnyLogic
forall a. HasCallStack => String -> a
error "Static.AnalysisArchitecture")
                    (NodeSig -> G_sign
getSig (DiagNodeSig -> NodeSig
getSigFromDiag DiagNodeSig
dnsig)) HetcatsOpts
opts RENAMING
ren
       let sink :: [(Node, GMorphism)]
sink = [(Node
p, GMorphism
gMorph)]
           iN :: IRI
iN = String -> Node -> IRI
addSuffixToNode "_amalg_transl" Node
p
       -- check amalamability conditions
       () <- HetcatsOpts
-> Range -> Diag -> [(Node, GMorphism)] -> String -> Result ()
assertAmalgamability HetcatsOpts
opts Range
pos Diag
diag1 [(Node, GMorphism)]
sink String
utStr
       (dnsig' :: DiagNodeSig
dnsig', diag' :: Diag
diag', dg' :: DGraph
dg') <- Range
-> LogicGraph
-> Diag
-> DGraph
-> DiagNodeSig
-> GMorphism
-> IRI
-> String
-> DGOrigin
-> Result (DiagNodeSig, Diag, DGraph)
extendDiagramWithMorphism Range
pos LogicGraph
lgraph
           Diag
diag1 DGraph
dg1 DiagNodeSig
dnsig GMorphism
gMorph IRI
iN String
utStr
                (Renamed -> DGOrigin
DGTranslation (Renamed -> DGOrigin) -> Renamed -> DGOrigin
forall a b. (a -> b) -> a -> b
$ RENAMING -> Renamed
Renamed RENAMING
ren)
       (DiagNodeSig, Diag, DGraph, UNIT_TERM)
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
forall (m :: * -> *) a. Monad m => a -> m a
return (DiagNodeSig
dnsig', Diag
diag', DGraph
dg', Annoted UNIT_TERM -> RENAMING -> UNIT_TERM
Unit_translation
                         (UNIT_TERM -> Annoted UNIT_TERM -> Annoted UNIT_TERM
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted UNIT_TERM
ut' Annoted UNIT_TERM
ut) RENAMING
ren)
  Amalgamation uts :: [Annoted UNIT_TERM]
uts poss :: Range
poss -> do
       (dnsigs :: [DiagNodeSig]
dnsigs, diag1 :: Diag
diag1, dg' :: DGraph
dg', uts' :: [Annoted UNIT_TERM]
uts') <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> [Annoted UNIT_TERM]
-> Result ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])
anaUnitTerms LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
uctx [Annoted UNIT_TERM]
uts
       -- compute sigma
       (sig :: NodeSig
sig, dg'' :: DGraph
dg'') <- LogicGraph
-> DGraph
-> [MaybeNode]
-> DGOrigin
-> IRI
-> Result (NodeSig, DGraph)
nodeSigUnion LogicGraph
lgraph DGraph
dg'
                      ((DiagNodeSig -> MaybeNode) -> [DiagNodeSig] -> [MaybeNode]
forall a b. (a -> b) -> [a] -> [b]
map (NodeSig -> MaybeNode
JustNode (NodeSig -> MaybeNode)
-> (DiagNodeSig -> NodeSig) -> DiagNodeSig -> MaybeNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DiagNodeSig -> NodeSig
getSigFromDiag) [DiagNodeSig]
dnsigs) DGOrigin
DGUnion
                      (SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ String -> SIMPLE_ID
mkSimpleId "imports")
       -- check amalgamability conditions
       [(Node, GMorphism)]
sink <- LogicGraph
-> [DiagNodeSig] -> NodeSig -> Result [(Node, GMorphism)]
inclusionSink LogicGraph
lgraph [DiagNodeSig]
dnsigs NodeSig
sig
       () <- HetcatsOpts
-> Range -> Diag -> [(Node, GMorphism)] -> String -> Result ()
assertAmalgamability HetcatsOpts
opts Range
poss Diag
diag1 [(Node, GMorphism)]
sink String
utStr
       (q :: DiagNodeSig
q, diag' :: Diag
diag') <- LogicGraph
-> Diag
-> [DiagNodeSig]
-> NodeSig
-> String
-> Result (DiagNodeSig, Diag)
extendDiagramIncl LogicGraph
lgraph Diag
diag1 [DiagNodeSig]
dnsigs
                     NodeSig
sig String
utStr
       (DiagNodeSig, Diag, DGraph, UNIT_TERM)
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
forall (m :: * -> *) a. Monad m => a -> m a
return (DiagNodeSig
q, Diag
diag', DGraph
dg'', [Annoted UNIT_TERM] -> Range -> UNIT_TERM
Amalgamation [Annoted UNIT_TERM]
uts' Range
poss)
  Local_unit udds :: [Annoted UNIT_DECL_DEFN]
udds ut :: Annoted UNIT_TERM
ut poss :: Range
poss -> do
       (_, uctx' :: ExtStUnitCtx
uctx', dg1 :: DGraph
dg1, udds' :: [Annoted UNIT_DECL_DEFN]
udds') <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> Map IRI RTPointer
-> [Annoted UNIT_DECL_DEFN]
-> Result
     (Map IRI RTPointer, ExtStUnitCtx, DGraph, [Annoted UNIT_DECL_DEFN])
anaUnitDeclDefns' LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
uctx Map IRI RTPointer
forall k a. Map k a
Map.empty [Annoted UNIT_DECL_DEFN]
udds
       (dnsig :: DiagNodeSig
dnsig, diag' :: Diag
diag', dg' :: DGraph
dg', ut' :: UNIT_TERM
ut') <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_TERM
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
anaUnitTerm LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg1 HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
uctx' (Annoted UNIT_TERM -> UNIT_TERM
forall a. Annoted a -> a
item Annoted UNIT_TERM
ut)
       (DiagNodeSig, Diag, DGraph, UNIT_TERM)
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
forall (m :: * -> *) a. Monad m => a -> m a
return (DiagNodeSig
dnsig, Diag
diag', DGraph
dg',
               [Annoted UNIT_DECL_DEFN] -> Annoted UNIT_TERM -> Range -> UNIT_TERM
Local_unit [Annoted UNIT_DECL_DEFN]
udds' (UNIT_TERM -> Annoted UNIT_TERM -> Annoted UNIT_TERM
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted UNIT_TERM
ut' Annoted UNIT_TERM
ut) Range
poss)
  Unit_appl un' :: IRI
un' fargus :: [FIT_ARG_UNIT]
fargus _ -> do
       IRI
un <- GlobalAnnos -> ExpOverrides -> IRI -> Result IRI
expCurieR (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
un'
       let ustr :: String
ustr = IRI -> String
iriToStringUnsecure IRI
un
           argStr :: String
argStr = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> ([Doc] -> Doc) -> [Doc] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
sepByCommas ([Doc] -> String) -> [Doc] -> String
forall a b. (a -> b) -> a -> b
$ (FIT_ARG_UNIT -> Doc) -> [FIT_ARG_UNIT] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (LogicGraph -> FIT_ARG_UNIT -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lgraph) [FIT_ARG_UNIT]
fargus
       case IRI -> StBasedUnitCtx -> Maybe BasedUnitSig
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IRI
un StBasedUnitCtx
buc of
            Just (Based_unit_sig dnsig :: DiagNodeSig
dnsig _rsig :: RefSig
_rsig) -> case [FIT_ARG_UNIT]
fargus of
              [] -> (DiagNodeSig, Diag, DGraph, UNIT_TERM)
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
forall (m :: * -> *) a. Monad m => a -> m a
return (DiagNodeSig
dnsig, Diag
diag, DGraph
dg, UNIT_TERM
utrm)
              _ -> (DiagNodeSig, Diag, DGraph, UNIT_TERM)
-> String -> Range -> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
forall a. a -> String -> Range -> Result a
plain_error (DiagNodeSig
dnsig, Diag
diag, DGraph
dg, UNIT_TERM
utrm)
                  (String
ustr String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is a parameterless unit, "
                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ "but arguments have been given: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
argStr) Range
pos
            Just (Based_par_unit_sig pI :: MaybeDiagNode
pI
                     (BranchRefSig _ (UnitSig argSigs :: [NodeSig]
argSigs resultSig :: NodeSig
resultSig _, _))) ->
                do (sigF :: NodeSig
sigF, dg' :: DGraph
dg') <- LogicGraph
-> DGraph
-> [MaybeNode]
-> DGOrigin
-> IRI
-> Result (NodeSig, DGraph)
nodeSigUnion LogicGraph
lgraph DGraph
dg
                       (MaybeDiagNode -> MaybeNode
toMaybeNode MaybeDiagNode
pI MaybeNode -> [MaybeNode] -> [MaybeNode]
forall a. a -> [a] -> [a]
: (NodeSig -> MaybeNode) -> [NodeSig] -> [MaybeNode]
forall a b. (a -> b) -> [a] -> [b]
map NodeSig -> MaybeNode
JustNode [NodeSig]
argSigs) DGOrigin
DGFormalParams
                       (SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ String -> SIMPLE_ID
mkSimpleId ("sigF_"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
argStr))
                   (morphSigs :: [(G_morphism, NodeSig, DiagNodeSig)]
morphSigs, dg'' :: DGraph
dg'', diagA :: Diag
diagA) <-
                       LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_TERM
-> Range
-> [NodeSig]
-> [FIT_ARG_UNIT]
-> Result ([(G_morphism, NodeSig, DiagNodeSig)], DGraph, Diag)
anaFitArgUnits LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg' HetcatsOpts
opts ExpOverrides
eo
                            ExtStUnitCtx
uctx UNIT_TERM
utrm Range
pos [NodeSig]
argSigs [FIT_ARG_UNIT]
fargus
                   (sigA :: NodeSig
sigA, dg''' :: DGraph
dg''') <- LogicGraph
-> DGraph
-> [MaybeNode]
-> DGOrigin
-> IRI
-> Result (NodeSig, DGraph)
nodeSigUnion LogicGraph
lgraph DGraph
dg''
                       (MaybeDiagNode -> MaybeNode
toMaybeNode MaybeDiagNode
pI MaybeNode -> [MaybeNode] -> [MaybeNode]
forall a. a -> [a] -> [a]
: ((G_morphism, NodeSig, DiagNodeSig) -> MaybeNode)
-> [(G_morphism, NodeSig, DiagNodeSig)] -> [MaybeNode]
forall a b. (a -> b) -> [a] -> [b]
map (NodeSig -> MaybeNode
JustNode (NodeSig -> MaybeNode)
-> ((G_morphism, NodeSig, DiagNodeSig) -> NodeSig)
-> (G_morphism, NodeSig, DiagNodeSig)
-> MaybeNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (G_morphism, NodeSig, DiagNodeSig) -> NodeSig
forall a b c. (a, b, c) -> b
second) [(G_morphism, NodeSig, DiagNodeSig)]
morphSigs)
                              DGOrigin
DGFitSpec
                              (SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ String -> SIMPLE_ID
mkSimpleId ("sigA_"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
argStr))
                   -- compute morphA (\sigma^A)
                   G_sign lidI :: lid
lidI sigI :: ExtSign sign symbol
sigI _ <- G_sign -> Result G_sign
forall (m :: * -> *) a. Monad m => a -> m a
return (MaybeNode -> G_sign
getMaybeSig (MaybeDiagNode -> MaybeNode
toMaybeNode MaybeDiagNode
pI))
                   let idI :: G_morphism
idI = 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
lidI (ExtSign sign symbol -> morphism
forall symbol sign morphism.
(Ord symbol, Category sign morphism) =>
ExtSign sign symbol -> morphism
ext_ide ExtSign sign symbol
sigI)
                   G_morphism
morphA <- [G_morphism] -> Result G_morphism
homogeneousMorManyUnion
                             ([G_morphism] -> Result G_morphism)
-> [G_morphism] -> Result G_morphism
forall a b. (a -> b) -> a -> b
$ G_morphism
idI G_morphism -> [G_morphism] -> [G_morphism]
forall a. a -> [a] -> [a]
: ((G_morphism, NodeSig, DiagNodeSig) -> G_morphism)
-> [(G_morphism, NodeSig, DiagNodeSig)] -> [G_morphism]
forall a b. (a -> b) -> [a] -> [b]
map (G_morphism, NodeSig, DiagNodeSig) -> G_morphism
forall a b c. (a, b, c) -> a
first [(G_morphism, NodeSig, DiagNodeSig)]
morphSigs
                   -- compute sigMorExt (\sigma^A(\Delta))
                   (_, gSigMorExt :: G_morphism
gSigMorExt) <- Bool
-> G_sign
-> G_sign
-> G_sign
-> G_morphism
-> Result (G_sign, G_morphism)
extendMorphism Bool
True (NodeSig -> G_sign
getSig NodeSig
sigF)
                                     (NodeSig -> G_sign
getSig NodeSig
resultSig) (NodeSig -> G_sign
getSig NodeSig
sigA) G_morphism
morphA
                   -- check amalgamability conditions
                   let sigMorExt :: GMorphism
sigMorExt = G_morphism -> GMorphism
gEmbed G_morphism
gSigMorExt
                       pIL :: [DiagNodeSig]
pIL = case MaybeDiagNode
pI of
                           JustDiagNode dn :: DiagNodeSig
dn -> [DiagNodeSig
dn]
                           _ -> []
                   [(Node, GMorphism)]
sink <- LogicGraph
-> [DiagNodeSig] -> NodeSig -> Result [(Node, GMorphism)]
inclusionSink LogicGraph
lgraph ([DiagNodeSig]
pIL [DiagNodeSig] -> [DiagNodeSig] -> [DiagNodeSig]
forall a. [a] -> [a] -> [a]
++
                                                 ((G_morphism, NodeSig, DiagNodeSig) -> DiagNodeSig)
-> [(G_morphism, NodeSig, DiagNodeSig)] -> [DiagNodeSig]
forall a b. (a -> b) -> [a] -> [b]
map (G_morphism, NodeSig, DiagNodeSig) -> DiagNodeSig
forall a b c. (a, b, c) -> c
third [(G_morphism, NodeSig, DiagNodeSig)]
morphSigs) NodeSig
sigA
                   () <- HetcatsOpts
-> Range -> Diag -> [(Node, GMorphism)] -> String -> Result ()
assertAmalgamability HetcatsOpts
opts Range
pos Diag
diagA [(Node, GMorphism)]
sink String
utStr
                   (qB :: DiagNodeSig
qB@(Diag_node_sig nqB :: Node
nqB _), diag' :: Diag
diag') <-
                       LogicGraph
-> Diag
-> [DiagNodeSig]
-> NodeSig
-> String
-> Result (DiagNodeSig, Diag)
extendDiagramIncl LogicGraph
lgraph Diag
diagA [DiagNodeSig]
pIL NodeSig
resultSig ""
                   -- insert nodes p^F_i and appropriate edges to the diagram
                   let ins :: Diag
-> DGraph
-> [(NodeSig, (G_morphism, b, DiagNodeSig))]
-> Result (Diag, DGraph)
ins diag0 :: Diag
diag0 dg0 :: DGraph
dg0 [] = (Diag, DGraph) -> Result (Diag, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Diag
diag0, DGraph
dg0)
                       ins diag0 :: Diag
diag0 dg0 :: DGraph
dg0 ((fpi :: NodeSig
fpi, (morph :: G_morphism
morph, _, tar :: DiagNodeSig
tar)) : morphNodes :: [(NodeSig, (G_morphism, b, DiagNodeSig))]
morphNodes) =
                           do
                              (diag'' :: Diag
diag'', dg2 :: DGraph
dg2) <-
                                Range
-> LogicGraph
-> Diag
-> DGraph
-> DiagNodeSig
-> NodeSig
-> DiagNodeSig
-> GMorphism
-> String
-> DGOrigin
-> Result (Diag, DGraph)
insertFormalParamAndVerifCond
                                 Range
pos LogicGraph
lgraph
                                 Diag
diag0 DGraph
dg0
                                 DiagNodeSig
tar NodeSig
fpi DiagNodeSig
qB
                                 (G_morphism -> GMorphism
gEmbed G_morphism
morph)
                                 String
argStr DGOrigin
DGTest
                              Diag
-> DGraph
-> [(NodeSig, (G_morphism, b, DiagNodeSig))]
-> Result (Diag, DGraph)
ins Diag
diag'' DGraph
dg2 [(NodeSig, (G_morphism, b, DiagNodeSig))]
morphNodes
                   (diag'' :: Diag
diag'', dg4 :: DGraph
dg4) <- Diag
-> DGraph
-> [(NodeSig, (G_morphism, NodeSig, DiagNodeSig))]
-> Result (Diag, DGraph)
forall b.
Diag
-> DGraph
-> [(NodeSig, (G_morphism, b, DiagNodeSig))]
-> Result (Diag, DGraph)
ins Diag
diag' DGraph
dg''' ([(NodeSig, (G_morphism, NodeSig, DiagNodeSig))]
 -> Result (Diag, DGraph))
-> [(NodeSig, (G_morphism, NodeSig, DiagNodeSig))]
-> Result (Diag, DGraph)
forall a b. (a -> b) -> a -> b
$ [NodeSig]
-> [(G_morphism, NodeSig, DiagNodeSig)]
-> [(NodeSig, (G_morphism, NodeSig, DiagNodeSig))]
forall a b. [a] -> [b] -> [(a, b)]
zip [NodeSig]
argSigs [(G_morphism, NodeSig, DiagNodeSig)]
morphSigs
                   -- check amalgamability conditions
                   let i :: IRI
i = String -> IRI -> IRI
addSuffixToIRI ("_amalg_"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
argStr) IRI
un
                   (sigR :: NodeSig
sigR, dg5 :: DGraph
dg5) <- DGraph
-> NodeSig
-> GMorphism
-> IRI
-> DGOrigin
-> Result (NodeSig, DGraph)
extendDGraph DGraph
dg4 NodeSig
resultSig
                                  GMorphism
sigMorExt IRI
i DGOrigin
DGExtension
                   -- make the union of sigR with all specs of arguments
                   let nsigs' :: [NodeSig]
nsigs' = [NodeSig] -> [NodeSig]
forall a. [a] -> [a]
reverse ([NodeSig] -> [NodeSig]) -> [NodeSig] -> [NodeSig]
forall a b. (a -> b) -> a -> b
$ ((G_morphism, NodeSig, DiagNodeSig) -> NodeSig)
-> [(G_morphism, NodeSig, DiagNodeSig)] -> [NodeSig]
forall a b. (a -> b) -> [a] -> [b]
map (DiagNodeSig -> NodeSig
getSigFromDiag (DiagNodeSig -> NodeSig)
-> ((G_morphism, NodeSig, DiagNodeSig) -> DiagNodeSig)
-> (G_morphism, NodeSig, DiagNodeSig)
-> NodeSig
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (G_morphism, NodeSig, DiagNodeSig) -> DiagNodeSig
forall a b c. (a, b, c) -> c
third) [(G_morphism, NodeSig, DiagNodeSig)]
morphSigs
                   G_sign
gbigSigma <- LogicGraph -> [G_sign] -> Result G_sign
gsigManyUnion LogicGraph
lgraph ([G_sign] -> Result G_sign) -> [G_sign] -> Result G_sign
forall a b. (a -> b) -> a -> b
$ (NodeSig -> G_sign) -> [NodeSig] -> [G_sign]
forall a b. (a -> b) -> [a] -> [b]
map NodeSig -> G_sign
getSig
                     ([NodeSig] -> [G_sign]) -> [NodeSig] -> [G_sign]
forall a b. (a -> b) -> a -> b
$ NodeSig
sigR NodeSig -> [NodeSig] -> [NodeSig]
forall a. a -> [a] -> [a]
: [NodeSig]
nsigs'
                   let xIRI :: IRI
xIRI = String -> IRI -> IRI
addSuffixToIRI ("_union_"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
argStr) IRI
un
                       xName :: NodeName
xName = DGraph -> IRI -> Node -> NodeName
ensureUniqueNames DGraph
dg5 IRI
xIRI 1
                       (ns :: NodeSig
ns@(NodeSig node :: Node
node _), dg6 :: DGraph
dg6) = DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
insGSig DGraph
dg5 NodeName
xName
                                                     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
lgraph 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
dg7 <- (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
dg6 ([NodeSig] -> Result DGraph) -> [NodeSig] -> Result DGraph
forall a b. (a -> b) -> a -> b
$ NodeSig
sigR NodeSig -> [NodeSig] -> [NodeSig]
forall a. a -> [a] -> [a]
: [NodeSig]
nsigs'
                   [(Node, GMorphism)]
incSink <- LogicGraph
-> [DiagNodeSig] -> NodeSig -> Result [(Node, GMorphism)]
inclusionSink LogicGraph
lgraph (((G_morphism, NodeSig, DiagNodeSig) -> DiagNodeSig)
-> [(G_morphism, NodeSig, DiagNodeSig)] -> [DiagNodeSig]
forall a b. (a -> b) -> [a] -> [b]
map (G_morphism, NodeSig, DiagNodeSig) -> DiagNodeSig
forall a b c. (a, b, c) -> c
third [(G_morphism, NodeSig, DiagNodeSig)]
morphSigs) NodeSig
sigR
                   let sink' :: [(Node, GMorphism)]
sink' = (Node
nqB, GMorphism
sigMorExt) (Node, GMorphism) -> [(Node, GMorphism)] -> [(Node, GMorphism)]
forall a. a -> [a] -> [a]
: [(Node, GMorphism)]
incSink
                   HetcatsOpts
-> Range -> Diag -> [(Node, GMorphism)] -> String -> Result ()
assertAmalgamability HetcatsOpts
opts Range
pos Diag
diag'' [(Node, GMorphism)]
sink' String
utStr
                   {- for lambda applications below
                   the node qB is not added, but only the edge from r
                   here we use ns instead of sigR -}
                   (q :: DiagNodeSig
q, diag''' :: Diag
diag''') <- Diag
-> DiagNodeSig
-> GMorphism
-> NodeSig
-> String
-> Result (DiagNodeSig, Diag)
extendDiagram Diag
diag'' DiagNodeSig
qB
                                   GMorphism
sigMorExt NodeSig
ns String
utStr
                   Diag
diag4 <- LogicGraph -> Diag -> [DiagNodeSig] -> DiagNodeSig -> Result Diag
insInclusionEdges LogicGraph
lgraph Diag
diag'''
                            (((G_morphism, NodeSig, DiagNodeSig) -> DiagNodeSig)
-> [(G_morphism, NodeSig, DiagNodeSig)] -> [DiagNodeSig]
forall a b. (a -> b) -> [a] -> [b]
map (G_morphism, NodeSig, DiagNodeSig) -> DiagNodeSig
forall a b c. (a, b, c) -> c
third [(G_morphism, NodeSig, DiagNodeSig)]
morphSigs) DiagNodeSig
q
                   (DiagNodeSig, Diag, DGraph, UNIT_TERM)
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
forall (m :: * -> *) a. Monad m => a -> m a
return (DiagNodeSig
q, Diag
diag4, DGraph
dg7, UNIT_TERM
utrm)
            Just (Based_lambda_unit_sig nodes :: [DiagNodeSig]
nodes
              (BranchRefSig _ (UnitSig argSigs :: [NodeSig]
argSigs resultSig :: NodeSig
resultSig _, _))) ->
              case [DiagNodeSig]
nodes of
               [] -> String -> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
forall a. HasCallStack => String -> a
error "error in lambda expression"
               _r :: DiagNodeSig
_r@(Diag_node_sig rn :: Node
rn _) : fs :: [DiagNodeSig]
fs ->
                do let fnodes :: [Node]
fnodes = (DiagNodeSig -> Node) -> [DiagNodeSig] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Diag_node_sig x :: Node
x _) -> Node
x) [DiagNodeSig]
fs
                   (diagC :: Diag
diagC, copyFun :: Map Node Node
copyFun) <- LogicGraph -> [Node] -> Diag -> Result (Diag, Map Node Node)
copyDiagram LogicGraph
lgraph [Node]
fnodes (Diag -> Result (Diag, Map Node Node))
-> Diag -> Result (Diag, Map Node Node)
forall a b. (a -> b) -> a -> b
$ ExtStUnitCtx -> Diag
forall a b. (a, b) -> b
snd ExtStUnitCtx
uctx
                   let getCopy :: Node -> DiagNodeSig
getCopy x :: Node
x =
                        let
                         x' :: Node
x' = Node -> Node -> Map Node Node -> Node
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Node
forall a. HasCallStack => String -> a
error "getCopy") Node
x Map Node Node
copyFun
                         y :: Maybe DiagNodeLab
y = Gr DiagNodeLab DiagLinkLab -> Node -> Maybe DiagNodeLab
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> Maybe a
lab (Diag -> Gr DiagNodeLab DiagLinkLab
diagGraph Diag
diagC) Node
x'
                        in
                            case Maybe DiagNodeLab
y of
                             Nothing -> String -> DiagNodeSig
forall a. HasCallStack => String -> a
error "node not found"
                             Just (DiagNode ns :: NodeSig
ns _) -> Node -> NodeSig -> DiagNodeSig
Diag_node_sig Node
x' NodeSig
ns
                       r' :: DiagNodeSig
r' = Node -> DiagNodeSig
getCopy Node
rn
                       fs' :: [DiagNodeSig]
fs' = (Node -> DiagNodeSig) -> [Node] -> [DiagNodeSig]
forall a b. (a -> b) -> [a] -> [b]
map Node -> DiagNodeSig
getCopy [Node]
fnodes
                   (sigF :: NodeSig
sigF, dg' :: DGraph
dg') <- LogicGraph
-> DGraph
-> [MaybeNode]
-> DGOrigin
-> IRI
-> Result (NodeSig, DGraph)
nodeSigUnion LogicGraph
lgraph DGraph
dg
                       ((NodeSig -> MaybeNode) -> [NodeSig] -> [MaybeNode]
forall a b. (a -> b) -> [a] -> [b]
map NodeSig -> MaybeNode
JustNode [NodeSig]
argSigs) DGOrigin
DGFormalParams
                                  (SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ String -> SIMPLE_ID
mkSimpleId ("sigF_"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
argStr))
                   (morphSigs :: [(G_morphism, NodeSig, DiagNodeSig)]
morphSigs, dg'' :: DGraph
dg'', diagA :: Diag
diagA) <-
                       LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_TERM
-> Range
-> [NodeSig]
-> [FIT_ARG_UNIT]
-> Result ([(G_morphism, NodeSig, DiagNodeSig)], DGraph, Diag)
anaFitArgUnits LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg' HetcatsOpts
opts ExpOverrides
eo
                            (ExtStUnitCtx -> StBasedUnitCtx
forall a b. (a, b) -> a
fst ExtStUnitCtx
uctx, Diag
diagC) UNIT_TERM
utrm Range
pos [NodeSig]
argSigs [FIT_ARG_UNIT]
fargus
                   (sigA :: NodeSig
sigA, dg''' :: DGraph
dg''') <- LogicGraph
-> DGraph
-> [MaybeNode]
-> DGOrigin
-> IRI
-> Result (NodeSig, DGraph)
nodeSigUnion LogicGraph
lgraph DGraph
dg''
                       (((G_morphism, NodeSig, DiagNodeSig) -> MaybeNode)
-> [(G_morphism, NodeSig, DiagNodeSig)] -> [MaybeNode]
forall a b. (a -> b) -> [a] -> [b]
map (NodeSig -> MaybeNode
JustNode (NodeSig -> MaybeNode)
-> ((G_morphism, NodeSig, DiagNodeSig) -> NodeSig)
-> (G_morphism, NodeSig, DiagNodeSig)
-> MaybeNode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (G_morphism, NodeSig, DiagNodeSig) -> NodeSig
forall a b c. (a, b, c) -> b
second) [(G_morphism, NodeSig, DiagNodeSig)]
morphSigs)
                              DGOrigin
DGFitSpec
                              (SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ String -> SIMPLE_ID
mkSimpleId ("sigA_"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
argStr))
                   -- compute morphA (\sigma^A)
                   G_morphism
morphA <- [G_morphism] -> Result G_morphism
homogeneousMorManyUnion
                             ([G_morphism] -> Result G_morphism)
-> [G_morphism] -> Result G_morphism
forall a b. (a -> b) -> a -> b
$ ((G_morphism, NodeSig, DiagNodeSig) -> G_morphism)
-> [(G_morphism, NodeSig, DiagNodeSig)] -> [G_morphism]
forall a b. (a -> b) -> [a] -> [b]
map (G_morphism, NodeSig, DiagNodeSig) -> G_morphism
forall a b c. (a, b, c) -> a
first [(G_morphism, NodeSig, DiagNodeSig)]
morphSigs
                   {- compute sigMorExt (\sigma^A(\Delta))
                   but allow sharing between body and parameter -}
                   (_, gSigMorExt :: G_morphism
gSigMorExt) <- Bool
-> G_sign
-> G_sign
-> G_sign
-> G_morphism
-> Result (G_sign, G_morphism)
extendMorphism Bool
False (NodeSig -> G_sign
getSig NodeSig
sigF)
                                     (NodeSig -> G_sign
getSig NodeSig
resultSig) (NodeSig -> G_sign
getSig NodeSig
sigA) G_morphism
morphA
                   -- check amalgamability conditions
                   let sigMorExt :: GMorphism
sigMorExt = G_morphism -> GMorphism
gEmbed G_morphism
gSigMorExt
                   [(Node, GMorphism)]
sink <- LogicGraph
-> [DiagNodeSig] -> NodeSig -> Result [(Node, GMorphism)]
inclusionSink LogicGraph
lgraph (((G_morphism, NodeSig, DiagNodeSig) -> DiagNodeSig)
-> [(G_morphism, NodeSig, DiagNodeSig)] -> [DiagNodeSig]
forall a b. (a -> b) -> [a] -> [b]
map (G_morphism, NodeSig, DiagNodeSig) -> DiagNodeSig
forall a b c. (a, b, c) -> c
third [(G_morphism, NodeSig, DiagNodeSig)]
morphSigs) NodeSig
sigA
                   () <- HetcatsOpts
-> Range -> Diag -> [(Node, GMorphism)] -> String -> Result ()
assertAmalgamability HetcatsOpts
opts Range
pos Diag
diagA [(Node, GMorphism)]
sink String
utStr
                   let eI :: [(DiagNodeSig, (G_morphism, DiagNodeSig))]
eI = [DiagNodeSig]
-> [(G_morphism, DiagNodeSig)]
-> [(DiagNodeSig, (G_morphism, DiagNodeSig))]
forall a b. [a] -> [b] -> [(a, b)]
zip [DiagNodeSig]
fs' ([(G_morphism, DiagNodeSig)]
 -> [(DiagNodeSig, (G_morphism, DiagNodeSig))])
-> [(G_morphism, DiagNodeSig)]
-> [(DiagNodeSig, (G_morphism, DiagNodeSig))]
forall a b. (a -> b) -> a -> b
$ ((G_morphism, NodeSig, DiagNodeSig) -> (G_morphism, DiagNodeSig))
-> [(G_morphism, NodeSig, DiagNodeSig)]
-> [(G_morphism, DiagNodeSig)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: G_morphism
x, _, z :: DiagNodeSig
z) -> (G_morphism
x, DiagNodeSig
z)) [(G_morphism, NodeSig, DiagNodeSig)]
morphSigs
                   {- insert an edge from f_i to targetNode_i
                   extendDiagramWithEdge does it
                   and then call it for pairs (f_i, targetNode_i) -}
                   let ins :: Diag
-> DGraph
-> [(DiagNodeSig, (G_morphism, DiagNodeSig))]
-> Result (Diag, DGraph)
ins diag0 :: Diag
diag0 dg0 :: DGraph
dg0 [] = (Diag, DGraph) -> Result (Diag, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Diag
diag0, DGraph
dg0)
                       ins diag0 :: Diag
diag0 dg0 :: DGraph
dg0 ((fI :: DiagNodeSig
fI, (morph :: G_morphism
morph, pIA :: DiagNodeSig
pIA)) : eIS :: [(DiagNodeSig, (G_morphism, DiagNodeSig))]
eIS) =
                           do (diag1 :: Diag
diag1, dg1 :: DGraph
dg1) <-
                                Range
-> LogicGraph
-> Diag
-> DGraph
-> DiagNodeSig
-> DiagNodeSig
-> GMorphism
-> DGLinkOrigin
-> Result (Diag, DGraph)
extendDiagramWithEdge Range
pos LogicGraph
lgraph Diag
diag0
                                DGraph
dg0 DiagNodeSig
fI DiagNodeSig
pIA (G_morphism -> GMorphism
gEmbed G_morphism
morph) DGLinkOrigin
TEST
                              Diag
-> DGraph
-> [(DiagNodeSig, (G_morphism, DiagNodeSig))]
-> Result (Diag, DGraph)
ins Diag
diag1 DGraph
dg1 [(DiagNodeSig, (G_morphism, DiagNodeSig))]
eIS
                   (diag' :: Diag
diag', dg4 :: DGraph
dg4) <- Diag
-> DGraph
-> [(DiagNodeSig, (G_morphism, DiagNodeSig))]
-> Result (Diag, DGraph)
ins Diag
diagA DGraph
dg''' [(DiagNodeSig, (G_morphism, DiagNodeSig))]
eI
                   -- check amalgamability conditions
                   let i :: IRI
i = String -> IRI -> IRI
addSuffixToIRI ("_amalg_"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
argStr) IRI
un
                   (sigR :: NodeSig
sigR, dg5 :: DGraph
dg5) <- DGraph
-> NodeSig
-> GMorphism
-> IRI
-> DGOrigin
-> Result (NodeSig, DGraph)
extendDGraph DGraph
dg4 NodeSig
resultSig
                                   GMorphism
sigMorExt IRI
i DGOrigin
DGExtension
                   [(Node, GMorphism)]
incSink <- LogicGraph
-> [DiagNodeSig] -> NodeSig -> Result [(Node, GMorphism)]
inclusionSink LogicGraph
lgraph (((G_morphism, NodeSig, DiagNodeSig) -> DiagNodeSig)
-> [(G_morphism, NodeSig, DiagNodeSig)] -> [DiagNodeSig]
forall a b. (a -> b) -> [a] -> [b]
map (G_morphism, NodeSig, DiagNodeSig) -> DiagNodeSig
forall a b c. (a, b, c) -> c
third [(G_morphism, NodeSig, DiagNodeSig)]
morphSigs) NodeSig
sigR
                   HetcatsOpts
-> Range -> Diag -> [(Node, GMorphism)] -> String -> Result ()
assertAmalgamability HetcatsOpts
opts Range
pos Diag
diag' [(Node, GMorphism)]
incSink String
utStr
                   {- -- for lambda applications
                   -- the node qB is not added, but only the edge from r -}
                   (q :: DiagNodeSig
q, diag'' :: Diag
diag'') <- Diag
-> DiagNodeSig
-> GMorphism
-> NodeSig
-> String
-> Result (DiagNodeSig, Diag)
extendDiagram Diag
diag' DiagNodeSig
r'
                                    GMorphism
sigMorExt NodeSig
sigR String
utStr
                   Diag
diag3 <- LogicGraph -> Diag -> [DiagNodeSig] -> DiagNodeSig -> Result Diag
insInclusionEdges LogicGraph
lgraph Diag
diag''
                             (((G_morphism, NodeSig, DiagNodeSig) -> DiagNodeSig)
-> [(G_morphism, NodeSig, DiagNodeSig)] -> [DiagNodeSig]
forall a b. (a -> b) -> [a] -> [b]
map (G_morphism, NodeSig, DiagNodeSig) -> DiagNodeSig
forall a b c. (a, b, c) -> c
third [(G_morphism, NodeSig, DiagNodeSig)]
morphSigs) DiagNodeSig
q
                   (DiagNodeSig, Diag, DGraph, UNIT_TERM)
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
forall (m :: * -> *) a. Monad m => a -> m a
return (DiagNodeSig
q, Diag
diag3, DGraph
dg5, UNIT_TERM
utrm)
            _ -> String -> Range -> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
forall a. String -> Range -> Result a
fatal_error ("Undefined unit " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ustr) Range
pos
  Group_unit_term ut :: Annoted UNIT_TERM
ut poss :: Range
poss -> do
       (dnsig :: DiagNodeSig
dnsig, diag1 :: Diag
diag1, dg1 :: DGraph
dg1, ut' :: UNIT_TERM
ut') <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_TERM
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
anaUnitTerm LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
uctx (Annoted UNIT_TERM -> UNIT_TERM
forall a. Annoted a -> a
item Annoted UNIT_TERM
ut)
       (DiagNodeSig, Diag, DGraph, UNIT_TERM)
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
forall (m :: * -> *) a. Monad m => a -> m a
return (DiagNodeSig
dnsig, Diag
diag1, DGraph
dg1, Annoted UNIT_TERM -> Range -> UNIT_TERM
Group_unit_term (UNIT_TERM -> Annoted UNIT_TERM -> Annoted UNIT_TERM
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted UNIT_TERM
ut' Annoted UNIT_TERM
ut) Range
poss)


-- | Analyse unit arguments
anaFitArgUnits :: LogicGraph -> LibEnv -> LibName -> DGraph
    -> HetcatsOpts -> ExpOverrides -> ExtStUnitCtx -> UNIT_TERM
    -- ^ the whole application for diagnostic purposes
    -> Range
    -- ^ the position of the application (for diagnostic purposes)
    -> [NodeSig]
    -- ^ the signatures of unit's formal parameters
    -> [FIT_ARG_UNIT] -- ^ the arguments for the unit
    -> Result ([(G_morphism, NodeSig, DiagNodeSig)], DGraph, Diag)
anaFitArgUnits :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_TERM
-> Range
-> [NodeSig]
-> [FIT_ARG_UNIT]
-> Result ([(G_morphism, NodeSig, DiagNodeSig)], DGraph, Diag)
anaFitArgUnits lgraph :: LogicGraph
lgraph libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo uctx :: ExtStUnitCtx
uctx@(buc :: StBasedUnitCtx
buc, diag :: Diag
diag)
                  appl :: UNIT_TERM
appl pos :: Range
pos nodeSigs :: [NodeSig]
nodeSigs fArgs :: [FIT_ARG_UNIT]
fArgs = case ([NodeSig]
nodeSigs, [FIT_ARG_UNIT]
fArgs) of
  (nsig :: NodeSig
nsig : nsigs :: [NodeSig]
nsigs, fau :: FIT_ARG_UNIT
fau : faus :: [FIT_ARG_UNIT]
faus) -> do
       (gmorph :: G_morphism
gmorph, nsig' :: NodeSig
nsig', dnsig :: DiagNodeSig
dnsig, dg1 :: DGraph
dg1, diag1 :: Diag
diag1) <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> NodeSig
-> FIT_ARG_UNIT
-> Result (G_morphism, NodeSig, DiagNodeSig, DGraph, Diag)
anaFitArgUnit LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
uctx NodeSig
nsig FIT_ARG_UNIT
fau
       (morphSigs :: [(G_morphism, NodeSig, DiagNodeSig)]
morphSigs, dg' :: DGraph
dg', diag' :: Diag
diag') <- LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_TERM
-> Range
-> [NodeSig]
-> [FIT_ARG_UNIT]
-> Result ([(G_morphism, NodeSig, DiagNodeSig)], DGraph, Diag)
anaFitArgUnits LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg1 HetcatsOpts
opts ExpOverrides
eo
           (StBasedUnitCtx
buc, Diag
diag1) UNIT_TERM
appl Range
pos [NodeSig]
nsigs [FIT_ARG_UNIT]
faus
       ([(G_morphism, NodeSig, DiagNodeSig)], DGraph, Diag)
-> Result ([(G_morphism, NodeSig, DiagNodeSig)], DGraph, Diag)
forall (m :: * -> *) a. Monad m => a -> m a
return ((G_morphism
gmorph, NodeSig
nsig', DiagNodeSig
dnsig) (G_morphism, NodeSig, DiagNodeSig)
-> [(G_morphism, NodeSig, DiagNodeSig)]
-> [(G_morphism, NodeSig, DiagNodeSig)]
forall a. a -> [a] -> [a]
: [(G_morphism, NodeSig, DiagNodeSig)]
morphSigs, DGraph
dg', Diag
diag')
  ([], []) -> ([(G_morphism, NodeSig, DiagNodeSig)], DGraph, Diag)
-> Result ([(G_morphism, NodeSig, DiagNodeSig)], DGraph, Diag)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], DGraph
dg, Diag
diag)
  _ -> ([(G_morphism, NodeSig, DiagNodeSig)], DGraph, Diag)
-> String
-> Range
-> Result ([(G_morphism, NodeSig, DiagNodeSig)], DGraph, Diag)
forall a. a -> String -> Range -> Result a
plain_error ([], DGraph
dg, Diag
diag)
       ("non-matching number of arguments given in application\n"
                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (LogicGraph -> UNIT_TERM -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lgraph UNIT_TERM
appl)) Range
pos

-- | Analyse unit argument
anaFitArgUnit :: LogicGraph -> LibEnv -> LibName -> DGraph
    -> HetcatsOpts
    -> ExpOverrides
    -> ExtStUnitCtx -> NodeSig -> FIT_ARG_UNIT
    -> Result (G_morphism, NodeSig, DiagNodeSig, DGraph, Diag)
{- ^ returns 1. the signature morphism 2. the target signature of the morphism
3. the diagram node 4. the modified DGraph 5. the modified diagram -}
anaFitArgUnit :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> NodeSig
-> FIT_ARG_UNIT
-> Result (G_morphism, NodeSig, DiagNodeSig, DGraph, Diag)
anaFitArgUnit lgraph :: LogicGraph
lgraph libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo uctx :: ExtStUnitCtx
uctx nsig :: NodeSig
nsig
                     a :: FIT_ARG_UNIT
a@(Fit_arg_unit ut :: Annoted UNIT_TERM
ut symbMap :: [G_mapping]
symbMap poss :: Range
poss) = Range
-> Result (G_morphism, NodeSig, DiagNodeSig, DGraph, Diag)
-> Result (G_morphism, NodeSig, DiagNodeSig, DGraph, Diag)
forall a. Range -> Result a -> Result a
adjustPos Range
poss (Result (G_morphism, NodeSig, DiagNodeSig, DGraph, Diag)
 -> Result (G_morphism, NodeSig, DiagNodeSig, DGraph, Diag))
-> Result (G_morphism, NodeSig, DiagNodeSig, DGraph, Diag)
-> Result (G_morphism, NodeSig, DiagNodeSig, DGraph, Diag)
forall a b. (a -> b) -> a -> b
$ do
       let argStr :: String
argStr = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ LogicGraph -> FIT_ARG_UNIT -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lgraph FIT_ARG_UNIT
a
       (p :: DiagNodeSig
p, diag' :: Diag
diag', dg' :: DGraph
dg', _) <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> UNIT_TERM
-> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
anaUnitTerm LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
uctx (Annoted UNIT_TERM -> UNIT_TERM
forall a. Annoted a -> a
item Annoted UNIT_TERM
ut)
       let gsigmaS :: G_sign
gsigmaS = NodeSig -> G_sign
getSig NodeSig
nsig
           gsigmaT :: G_sign
gsigmaT = NodeSig -> G_sign
getSig (DiagNodeSig -> NodeSig
getSigFromDiag DiagNodeSig
p)
       G_sign lidS :: lid
lidS sigmaS :: ExtSign sign symbol
sigmaS _ <- G_sign -> Result G_sign
forall (m :: * -> *) a. Monad m => a -> m a
return G_sign
gsigmaS
       G_sign lidT :: lid
lidT sigmaT :: ExtSign sign symbol
sigmaT _ <- G_sign -> Result G_sign
forall (m :: * -> *) a. Monad m => a -> m a
return G_sign
gsigmaT
       AnyLogic
cl <- String -> LogicGraph -> Result AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyLogic
lookupCurrentLogic "anaFitArgUnit" LogicGraph
lgraph
       G_symb_map_items_list lid :: lid
lid sis :: [symb_map_items]
sis <- AnyLogic -> [G_mapping] -> Result G_symb_map_items_list
homogenizeGM AnyLogic
cl [G_mapping]
symbMap
       ExtSign sign symbol
sigmaS' <- 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
lidS lid
lid "anaFitArgUnit1" ExtSign sign symbol
sigmaS
       ExtSign sign symbol
sigmaT' <- 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
lidT lid
lid "anaFitArgUnit2" ExtSign sign symbol
sigmaT
       morphism
mor <- 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
sigmaS') else do
         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
lid (ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symbol
sigmaS')
           (sign -> Maybe sign
forall a. a -> Maybe a
Just (sign -> Maybe sign) -> sign -> Maybe sign
forall a b. (a -> b) -> a -> b
$ ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symbol
sigmaT') [symb_map_items]
sis
         lid
-> EndoMap raw_symbol
-> ExtSign sign 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
-> ExtSign sign symbol
-> Result morphism
ext_induced_from_to_morphism lid
lid EndoMap raw_symbol
rmap ExtSign sign symbol
sigmaS' ExtSign sign symbol
sigmaT'
       let gMorph :: G_morphism
gMorph = 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
lid morphism
mor
           i :: IRI
i = String -> Node -> IRI
addSuffixToNode ("_fit_"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
argStr) (Node -> IRI) -> Node -> IRI
forall a b. (a -> b) -> a -> b
$ NodeSig -> Node
getNode NodeSig
nsig
              --  ^ this ensures unique names
       (nsig' :: NodeSig
nsig', dg'' :: DGraph
dg'') <- DGraph
-> NodeSig
-> GMorphism
-> IRI
-> DGOrigin
-> Result (NodeSig, DGraph)
extendDGraph DGraph
dg' NodeSig
nsig (G_morphism -> GMorphism
gEmbed G_morphism
gMorph) IRI
i DGOrigin
DGFitSpec
       (G_morphism, NodeSig, DiagNodeSig, DGraph, Diag)
-> Result (G_morphism, NodeSig, DiagNodeSig, DGraph, Diag)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_morphism
gMorph, NodeSig
nsig', DiagNodeSig
p, DGraph
dg'', Diag
diag')

-- | Analyse unit specification
anaUnitSpec :: LogicGraph -> LibEnv -> LibName -> DGraph
  -> HetcatsOpts    -- ^ should only the structure be analysed?
  -> ExpOverrides   -- for expanding CURIEs
  -> SPEC_NAME      -- the name of the unit spec, for node names
  -> MaybeNode      -- ^ the signature of imports
  -> Maybe RTPointer -- for building refinement trees
  -> UNIT_SPEC -> Result (RefSig, DGraph, UNIT_SPEC)
{- ^ returns 1. unit signature 2. the development graph resulting from
structred specs inside the unit spec and 3. a UNIT_SPEC after possible
conversions. -}
anaUnitSpec :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> IRI
-> MaybeNode
-> Maybe RTPointer
-> UNIT_SPEC
-> Result (RefSig, DGraph, UNIT_SPEC)
anaUnitSpec lgraph :: LogicGraph
lgraph libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo usName :: IRI
usName impsig :: MaybeNode
impsig rN :: Maybe RTPointer
rN usp :: UNIT_SPEC
usp = case UNIT_SPEC
usp of
  Unit_type argSpecs :: [Annoted SPEC]
argSpecs resultSpec :: Annoted SPEC
resultSpec poss :: Range
poss ->
   case [Annoted SPEC]
argSpecs of
    [] -> case Annoted SPEC
resultSpec of
      Annoted (Spec_inst spn :: IRI
spn [] _ _) _ _ _
        | case IRI -> DGraph -> Maybe GlobalEntry
lookupGlobalEnvDG (IRI -> Maybe IRI -> IRI
forall a. a -> Maybe a -> a
fromMaybe IRI
spn
                                 (Maybe IRI -> IRI) -> Maybe IRI -> IRI
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> ExpOverrides -> IRI -> Maybe IRI
expCurie (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
spn) DGraph
dg of
            Just (UnitEntry _) -> Bool
True
            Just (SpecEntry _) -> Bool
True
              -- this is needed because there are no REF_NAME in REF_SPEC
            Just (ArchOrRefEntry False _) -> Bool
True
            _ -> Bool
False ->
       {- if argspecs are empty and resultspec is a name of unit spec
          then this should be converted to a Spec_name -}
        LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> IRI
-> MaybeNode
-> Maybe RTPointer
-> UNIT_SPEC
-> Result (RefSig, DGraph, UNIT_SPEC)
anaUnitSpec LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo IRI
usName MaybeNode
impsig Maybe RTPointer
rN (IRI -> UNIT_SPEC
Spec_name IRI
spn)
      _ -> do -- a trivial unit type
       (resultSpec' :: SPEC
resultSpec', resultSig :: NodeSig
resultSig, 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
lgraph LibEnv
libEnv LibName
ln
           DGraph
dg MaybeNode
impsig 
           (DGraph -> IRI -> Node -> NodeName
ensureUniqueNames DGraph
dg IRI
usName 1) 
           HetcatsOpts
opts ExpOverrides
eo (Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
resultSpec) Range
poss
       let usig :: UnitSig
usig = [NodeSig] -> NodeSig -> Maybe NodeSig -> UnitSig
UnitSig [] NodeSig
resultSig Maybe NodeSig
forall a. Maybe a
Nothing
       (RefSig, DGraph, UNIT_SPEC) -> Result (RefSig, DGraph, UNIT_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnitSig -> RefSig
mkRefSigFromUnit UnitSig
usig , DGraph
dg', [Annoted SPEC] -> Annoted SPEC -> Range -> UNIT_SPEC
Unit_type []
                            (SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted SPEC
resultSpec' Annoted SPEC
resultSpec) Range
poss)
    _ -> do -- a non-trivial unit type
       let 
       (argSigs :: [NodeSig]
argSigs, dg1 :: DGraph
dg1, argSpecs' :: [Annoted SPEC]
argSpecs') <- 
          LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> IRI
-> [Annoted SPEC]
-> Result ([NodeSig], DGraph, [Annoted SPEC])
anaArgSpecs LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo IRI
usName [Annoted SPEC]
argSpecs
       (sigUnion :: NodeSig
sigUnion, dg2 :: DGraph
dg2) <- 
         case [NodeSig]
argSigs of 
           [argSig :: NodeSig
argSig] -> (NodeSig, DGraph) -> Result (NodeSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeSig
argSig, DGraph
dg1) -- the optimization mentioned below
           _ -> LogicGraph
-> DGraph
-> [MaybeNode]
-> DGOrigin
-> IRI
-> Result (NodeSig, DGraph)
nodeSigUnion LogicGraph
lgraph DGraph
dg1
                          (MaybeNode
impsig MaybeNode -> [MaybeNode] -> [MaybeNode]
forall a. a -> [a] -> [a]
: (NodeSig -> MaybeNode) -> [NodeSig] -> [MaybeNode]
forall a b. (a -> b) -> [a] -> [b]
map NodeSig -> MaybeNode
JustNode [NodeSig]
argSigs) DGOrigin
DGFormalParams IRI
usName
        {- if i have no imports, i can optimize?
        in that case, an identity morphism is introduced -}
       let resName :: NodeName
resName = DGraph -> IRI -> Node -> NodeName
ensureUniqueNames DGraph
dg2 (String -> IRI -> IRI
addSuffixToIRI "_res" IRI
usName) 1 
       (resultSpec' :: SPEC
resultSpec', resultSig :: NodeSig
resultSig, dg3 :: DGraph
dg3) <- Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
True Bool
True LogicGraph
lgraph LibEnv
libEnv LibName
ln
           DGraph
dg2 (NodeSig -> MaybeNode
JustNode NodeSig
sigUnion)
               (NodeName
resName {extIndex :: Node
extIndex = 1}) 
               HetcatsOpts
opts ExpOverrides
eo (Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
resultSpec) Range
poss
       let usig :: UnitSig
usig = [NodeSig] -> NodeSig -> Maybe NodeSig -> UnitSig
UnitSig [NodeSig]
argSigs NodeSig
resultSig (Maybe NodeSig -> UnitSig) -> Maybe NodeSig -> UnitSig
forall a b. (a -> b) -> a -> b
$ NodeSig -> Maybe NodeSig
forall a. a -> Maybe a
Just NodeSig
sigUnion
           rsig :: RefSig
rsig = UnitSig -> RefSig
mkRefSigFromUnit UnitSig
usig
       (RefSig, DGraph, UNIT_SPEC) -> Result (RefSig, DGraph, UNIT_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return (RefSig
rsig, DGraph
dg3, [Annoted SPEC] -> Annoted SPEC -> Range -> UNIT_SPEC
Unit_type [Annoted SPEC]
argSpecs'
                                (SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted SPEC
resultSpec' Annoted SPEC
resultSpec) Range
poss)
  Spec_name un' :: IRI
un' -> do
   IRI
usn <- GlobalAnnos -> ExpOverrides -> IRI -> Result IRI
expCurieR (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
un'
   case IRI -> DGraph -> Maybe GlobalEntry
lookupGlobalEnvDG IRI
usn DGraph
dg of
    Just (UnitEntry usig :: UnitSig
usig) -> (RefSig, DGraph, UNIT_SPEC) -> Result (RefSig, DGraph, UNIT_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnitSig -> RefSig
mkRefSigFromUnit UnitSig
usig, DGraph
dg, UNIT_SPEC
usp)
    Just (SpecEntry (ExtGenSig _gsig :: GenSig
_gsig@(GenSig _ args :: [NodeSig]
args unSig :: MaybeNode
unSig) nsig :: NodeSig
nsig) ) -> do
      let uSig :: Maybe NodeSig
uSig = case MaybeNode
unSig of
                  JustNode n :: NodeSig
n -> NodeSig -> Maybe NodeSig
forall a. a -> Maybe a
Just NodeSig
n
                  _ -> Maybe NodeSig
forall a. Maybe a
Nothing
      (RefSig, DGraph, UNIT_SPEC) -> Result (RefSig, DGraph, UNIT_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return (UnitSig -> RefSig
mkRefSigFromUnit (UnitSig -> RefSig) -> UnitSig -> RefSig
forall a b. (a -> b) -> a -> b
$ [NodeSig] -> NodeSig -> Maybe NodeSig -> UnitSig
UnitSig [NodeSig]
args NodeSig
nsig Maybe NodeSig
uSig, DGraph
dg, UNIT_SPEC
usp)
    Just (ArchOrRefEntry False rsig :: RefSig
rsig) ->
      case Maybe RTPointer
rN of
       Nothing -> let
             p :: RTPointer
p = RefSig -> RTPointer
getPointerFromRef RefSig
rsig
             (dg' :: DGraph
dg', newP :: RTPointer
newP) = DGraph -> Maybe RTLeaves -> RTPointer -> (DGraph, RTPointer)
addSubTree DGraph
dg Maybe RTLeaves
forall a. Maybe a
Nothing RTPointer
p
            in (RefSig, DGraph, UNIT_SPEC) -> Result (RefSig, DGraph, UNIT_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return (RefSig -> RTPointer -> RefSig
setPointerInRef RefSig
rsig RTPointer
newP , DGraph
dg', UNIT_SPEC
usp)
       Just p0 :: RTPointer
p0 -> let l :: RTLeaves
l = RTPointer -> RTLeaves
refTarget RTPointer
p0 in
          case RTLeaves
l of
           RTLeaf x :: Node
x -> let
                       p :: RTPointer
p = RefSig -> RTPointer
getPointerFromRef RefSig
rsig
                       (dg' :: DGraph
dg', p' :: RTPointer
p') = DGraph -> Maybe RTLeaves -> RTPointer -> (DGraph, RTPointer)
addSubTree DGraph
dg (RTLeaves -> Maybe RTLeaves
forall a. a -> Maybe a
Just RTLeaves
l) RTPointer
p
                       np' :: RTPointer
np' = RTPointer -> RTPointer -> RTPointer
compPointer (Node -> RTPointer
NPUnit Node
x) RTPointer
p'
                     in (RefSig, DGraph, UNIT_SPEC) -> Result (RefSig, DGraph, UNIT_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return (RefSig -> RTPointer -> RefSig
setPointerInRef RefSig
rsig RTPointer
np', DGraph
dg', UNIT_SPEC
usp)
           RTLeaves leaves :: Map IRI RTLeaves
leaves -> let
               p :: RTPointer
p = RefSig -> RTPointer
getPointerFromRef RefSig
rsig
             in case RTPointer
p of
                  NPComp _ -> let
                    (dg' :: DGraph
dg', p' :: RTPointer
p') = DGraph -> Maybe RTLeaves -> RTPointer -> (DGraph, RTPointer)
addSubTree DGraph
dg (RTLeaves -> Maybe RTLeaves
forall a. a -> Maybe a
Just RTLeaves
l) RTPointer
p
                    np' :: RTPointer
np' = RTPointer -> RTPointer -> RTPointer
compPointer RTPointer
p0 RTPointer
p'
                    in (RefSig, DGraph, UNIT_SPEC) -> Result (RefSig, DGraph, UNIT_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return (RefSig -> RTPointer -> RefSig
setPointerInRef RefSig
rsig RTPointer
np', DGraph
dg', UNIT_SPEC
usp)
                  _ ->
                     case Map IRI RTLeaves -> Node
forall k a. Map k a -> Node
Map.size Map IRI RTLeaves
leaves of
                       1 ->
                             let (_, h :: RTLeaves
h@(RTLeaf x :: Node
x)) = [(IRI, RTLeaves)] -> (IRI, RTLeaves)
forall a. [a] -> a
head ([(IRI, RTLeaves)] -> (IRI, RTLeaves))
-> [(IRI, RTLeaves)] -> (IRI, RTLeaves)
forall a b. (a -> b) -> a -> b
$ Map IRI RTLeaves -> [(IRI, RTLeaves)]
forall k a. Map k a -> [(k, a)]
Map.toList Map IRI RTLeaves
leaves
                                 (dg' :: DGraph
dg', p' :: RTPointer
p') = DGraph -> Maybe RTLeaves -> RTPointer -> (DGraph, RTPointer)
addSubTree DGraph
dg (RTLeaves -> Maybe RTLeaves
forall a. a -> Maybe a
Just RTLeaves
h) RTPointer
p
                                 np' :: RTPointer
np' = RTPointer -> RTPointer -> RTPointer
compPointer (Node -> RTPointer
NPUnit Node
x) RTPointer
p'
                             in (RefSig, DGraph, UNIT_SPEC) -> Result (RefSig, DGraph, UNIT_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return (RefSig -> RTPointer -> RefSig
setPointerInRef RefSig
rsig RTPointer
np', DGraph
dg', UNIT_SPEC
usp)
                       _ -> String -> Result (RefSig, DGraph, UNIT_SPEC)
forall a. HasCallStack => String -> a
error "can't compose signatures!"
    _ -> String -> IRI -> Result (RefSig, DGraph, UNIT_SPEC)
forall a. String -> IRI -> Result a
notFoundError "unit specification" IRI
usn
  Closed_unit_spec usp' :: UNIT_SPEC
usp' _ -> do
    AnyLogic
curl <- String -> LogicGraph -> Result AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyLogic
lookupCurrentLogic "UnitSpec" LogicGraph
lgraph
    LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> IRI
-> MaybeNode
-> Maybe RTPointer
-> UNIT_SPEC
-> Result (RefSig, DGraph, UNIT_SPEC)
anaUnitSpec LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo IRI
usName (AnyLogic -> MaybeNode
EmptyNode AnyLogic
curl) Maybe RTPointer
rN UNIT_SPEC
usp'

-- | Analyse refinement specification
anaRefSpec :: 
   Bool -- True is the refinement is source of a refinement
   -> LogicGraph -> LibEnv -> LibName -> DGraph
   -> HetcatsOpts      -- ^ should only the structure be analysed?
   -> ExpOverrides
   -> MaybeNode        -- ^ the signature of imports
   -> SPEC_NAME        -- for origin
   -> ExtStUnitCtx
   -> Maybe RTPointer
   -> REF_SPEC
   -> Result ([DiagNodeSig], -- for lambda expressions
              Maybe DiagNodeSig, -- for tracing between levels
              Maybe Diag, RefSig, DGraph, REF_SPEC)
anaRefSpec :: Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> MaybeNode
-> IRI
-> ExtStUnitCtx
-> Maybe RTPointer
-> REF_SPEC
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
      REF_SPEC)
anaRefSpec src :: Bool
src lgraph :: LogicGraph
lgraph libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo nsig :: MaybeNode
nsig rn :: IRI
rn sharedCtx :: ExtStUnitCtx
sharedCtx nP :: Maybe RTPointer
nP rsp :: REF_SPEC
rsp =
 case REF_SPEC
rsp of
  Unit_spec asp :: UNIT_SPEC
asp ->
     do 
       let rn' :: IRI
rn' = if Bool
src then IRI
rn else String -> IRI -> IRI
addSuffixToIRI "_target" IRI
rn
       (rsig :: RefSig
rsig, dg' :: DGraph
dg', asp' :: UNIT_SPEC
asp') <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> IRI
-> MaybeNode
-> Maybe RTPointer
-> UNIT_SPEC
-> Result (RefSig, DGraph, UNIT_SPEC)
anaUnitSpec LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo IRI
rn' MaybeNode
nsig Maybe RTPointer
nP UNIT_SPEC
asp
       case RefSig
rsig of
         BranchRefSig _ _ -> do
          UnitSig
usig <- RefSig -> Result UnitSig
getUnitSigFromRef RefSig
rsig
          let rP :: RTPointer
rP = RefSig -> RTPointer
getPointerFromRef RefSig
rsig
              (rsig' :: RefSig
rsig', dg3 :: DGraph
dg3) = case RTPointer
rP of
                           RTNone ->
                             let
                             (n :: Node
n, dg'' :: DGraph
dg'') = DGraph -> UnitSig -> String -> (Node, DGraph)
addNodeRT DGraph
dg' UnitSig
usig (UNIT_SPEC -> String
name UNIT_SPEC
asp)
                             r' :: RefSig
r' = RefSig -> RTPointer -> RefSig
setPointerInRef RefSig
rsig (Node -> RTPointer
NPUnit Node
n)
                            in (RefSig
r', DGraph
dg'')
                           _ -> (RefSig
rsig, DGraph
dg')
          ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
 REF_SPEC)
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
      REF_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Maybe DiagNodeSig
forall a. Maybe a
Nothing, Diag -> Maybe Diag
forall a. a -> Maybe a
Just (ExtStUnitCtx -> Diag
forall a b. (a, b) -> b
snd ExtStUnitCtx
sharedCtx), RefSig
rsig', DGraph
dg3, UNIT_SPEC -> REF_SPEC
Unit_spec UNIT_SPEC
asp')
         _ ->
          ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
 REF_SPEC)
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
      REF_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Maybe DiagNodeSig
forall a. Maybe a
Nothing, Diag -> Maybe Diag
forall a. a -> Maybe a
Just (ExtStUnitCtx -> Diag
forall a b. (a, b) -> b
snd ExtStUnitCtx
sharedCtx), RefSig
rsig, DGraph
dg', UNIT_SPEC -> REF_SPEC
Unit_spec UNIT_SPEC
asp')
  Arch_unit_spec asp :: Annoted ARCH_SPEC
asp poss :: Range
poss ->
     do
       let x :: Maybe Node
x = case Maybe RTPointer
nP of
                Nothing -> Maybe Node
forall a. Maybe a
Nothing
                Just p :: RTPointer
p ->
                 case RTPointer -> RTLeaves
refTarget RTPointer
p of
                  RTLeaf y :: Node
y -> Node -> Maybe Node
forall a. a -> Maybe a
Just Node
y
                  _ -> String -> Maybe Node
forall a. HasCallStack => String -> a
error "nyi"
       (nodes :: [DiagNodeSig]
nodes, maybeRes :: Maybe DiagNodeSig
maybeRes, diag :: Diag
diag, rsig :: RefSig
rsig, dg' :: DGraph
dg', asp' :: ARCH_SPEC
asp') <-
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> Maybe Node
-> ARCH_SPEC
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph, ARCH_SPEC)
anaArchSpec LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
sharedCtx Maybe Node
x (ARCH_SPEC
 -> Result
      ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph,
       ARCH_SPEC))
-> ARCH_SPEC
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph, ARCH_SPEC)
forall a b. (a -> b) -> a -> b
$ Annoted ARCH_SPEC -> ARCH_SPEC
forall a. Annoted a -> a
item Annoted ARCH_SPEC
asp
       ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
 REF_SPEC)
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
      REF_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return ([DiagNodeSig]
nodes, Maybe DiagNodeSig
maybeRes, Diag -> Maybe Diag
forall a. a -> Maybe a
Just Diag
diag, RefSig
rsig, DGraph
dg',
               Annoted ARCH_SPEC -> Range -> REF_SPEC
Arch_unit_spec (ARCH_SPEC -> Annoted ARCH_SPEC -> Annoted ARCH_SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted ARCH_SPEC
asp' Annoted ARCH_SPEC
asp) Range
poss)
{- check whether it is indeed correct
to ignore the nodes of the
lambda expressions, like you do in the following -}
  Compose_ref rslist :: [REF_SPEC]
rslist range :: Range
range ->
    do
       (dg' :: DGraph
dg', anaSpecs :: [(RefSig, REF_SPEC)]
anaSpecs, _) <- ((DGraph, [(RefSig, REF_SPEC)], Maybe RTPointer)
 -> REF_SPEC
 -> Result (DGraph, [(RefSig, REF_SPEC)], Maybe RTPointer))
-> (DGraph, [(RefSig, REF_SPEC)], Maybe RTPointer)
-> [REF_SPEC]
-> Result (DGraph, [(RefSig, REF_SPEC)], Maybe RTPointer)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ (dgr :: DGraph
dgr, rList :: [(RefSig, REF_SPEC)]
rList, rN' :: Maybe RTPointer
rN') rsp0 :: REF_SPEC
rsp0 ->
                                        do
          (_, _, _, rsig' :: RefSig
rsig', dgr' :: DGraph
dgr', rsp' :: REF_SPEC
rsp') <-
                               Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> MaybeNode
-> IRI
-> ExtStUnitCtx
-> Maybe RTPointer
-> REF_SPEC
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
      REF_SPEC)
anaRefSpec Bool
False LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dgr HetcatsOpts
opts ExpOverrides
eo MaybeNode
nsig
                               (SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ String -> SIMPLE_ID
mkSimpleId (String -> SIMPLE_ID) -> String -> SIMPLE_ID
forall a b. (a -> b) -> a -> b
$
                                             IRI -> String
forall a. Show a => a -> String
show IRI
rn String -> String -> String
forall a. [a] -> [a] -> [a]
++ "gen_ref_name" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                             Node -> String
forall a. Show a => a -> String
show ([(RefSig, REF_SPEC)] -> Node
forall (t :: * -> *) a. Foldable t => t a -> Node
length [(RefSig, REF_SPEC)]
rList) )
                               ExtStUnitCtx
sharedCtx Maybe RTPointer
rN' REF_SPEC
rsp0
          (DGraph, [(RefSig, REF_SPEC)], Maybe RTPointer)
-> Result (DGraph, [(RefSig, REF_SPEC)], Maybe RTPointer)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph
dgr', [(RefSig, REF_SPEC)]
rList [(RefSig, REF_SPEC)]
-> [(RefSig, REF_SPEC)] -> [(RefSig, REF_SPEC)]
forall a. [a] -> [a] -> [a]
++ [(RefSig
rsig', REF_SPEC
rsp')],
                        RTPointer -> Maybe RTPointer
forall a. a -> Maybe a
Just (RTPointer -> Maybe RTPointer) -> RTPointer -> Maybe RTPointer
forall a b. (a -> b) -> a -> b
$ RefSig -> RTPointer
getPointerFromRef RefSig
rsig')
                           ) (DGraph
dg, [], Maybe RTPointer
nP) [REF_SPEC]
rslist
       -- compose signatures in csig
       let refSigs :: [RefSig]
refSigs = ((RefSig, REF_SPEC) -> RefSig) -> [(RefSig, REF_SPEC)] -> [RefSig]
forall a b. (a -> b) -> [a] -> [b]
map (RefSig, REF_SPEC) -> RefSig
forall a b. (a, b) -> a
fst [(RefSig, REF_SPEC)]
anaSpecs
       RefSig
csig <- (RefSig -> RefSig -> Result RefSig)
-> RefSig -> [RefSig] -> Result RefSig
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM RefSig -> RefSig -> Result RefSig
refSigComposition ([RefSig] -> RefSig
forall a. [a] -> a
head [RefSig]
refSigs) ([RefSig] -> Result RefSig) -> [RefSig] -> Result RefSig
forall a b. (a -> b) -> a -> b
$ [RefSig] -> [RefSig]
forall a. [a] -> [a]
tail [RefSig]
refSigs
       let compRef :: REF_SPEC
compRef = [REF_SPEC] -> Range -> REF_SPEC
Compose_ref (((RefSig, REF_SPEC) -> REF_SPEC)
-> [(RefSig, REF_SPEC)] -> [REF_SPEC]
forall a b. (a -> b) -> [a] -> [b]
map (RefSig, REF_SPEC) -> REF_SPEC
forall a b. (a, b) -> b
snd [(RefSig, REF_SPEC)]
anaSpecs) Range
range
       ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
 REF_SPEC)
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
      REF_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Maybe DiagNodeSig
forall a. Maybe a
Nothing, Maybe Diag
forall a. Maybe a
Nothing, RefSig
csig, DGraph
dg', REF_SPEC
compRef)
  Component_ref urlist :: [UNIT_REF]
urlist range :: Range
range -> do
       (dg' :: DGraph
dg', anaRefs :: [UNIT_REF]
anaRefs, resultMap :: BStContext
resultMap, pMap :: Map IRI RTPointer
pMap) <-
         ((DGraph, [UNIT_REF], BStContext, Map IRI RTPointer)
 -> UNIT_REF
 -> Result (DGraph, [UNIT_REF], BStContext, Map IRI RTPointer))
-> (DGraph, [UNIT_REF], BStContext, Map IRI RTPointer)
-> [UNIT_REF]
-> Result (DGraph, [UNIT_REF], BStContext, Map IRI RTPointer)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ (dgr :: DGraph
dgr, rList :: [UNIT_REF]
rList, cx :: BStContext
cx, ps :: Map IRI RTPointer
ps) uref0 :: UNIT_REF
uref0 -> do
          ((n :: IRI
n, rs :: RefSig
rs), dgr' :: DGraph
dgr', uref' :: UNIT_REF
uref') <-
                    LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> Maybe RTPointer
-> UNIT_REF
-> Result ((IRI, RefSig), DGraph, UNIT_REF)
anaUnitRef LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dgr HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
emptyExtStUnitCtx Maybe RTPointer
nP UNIT_REF
uref0
          (DGraph, [UNIT_REF], BStContext, Map IRI RTPointer)
-> Result (DGraph, [UNIT_REF], BStContext, Map IRI RTPointer)
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph
dgr', UNIT_REF
uref' UNIT_REF -> [UNIT_REF] -> [UNIT_REF]
forall a. a -> [a] -> [a]
: [UNIT_REF]
rList , IRI -> RefSig -> BStContext -> BStContext
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
n RefSig
rs BStContext
cx,
                  IRI -> RTPointer -> Map IRI RTPointer -> Map IRI RTPointer
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
n (RefSig -> RTPointer
getPointerFromRef RefSig
rs) Map IRI RTPointer
ps)
                           ) (DGraph
dg, [], BStContext
forall k a. Map k a
Map.empty, Map IRI RTPointer
forall k a. Map k a
Map.empty) [UNIT_REF]
urlist
       {- here:
        insert a dummy node labeled with the name of the component
        insert a refinement link from the dummy node to the
        source of refinement -}
       ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
 REF_SPEC)
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
      REF_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Maybe DiagNodeSig
forall a. Maybe a
Nothing, Maybe Diag
forall a. Maybe a
Nothing,
               RTPointer -> BStContext -> RefSig
ComponentRefSig (Map IRI RTPointer -> RTPointer
NPComp Map IRI RTPointer
pMap) BStContext
resultMap, DGraph
dg',
               [UNIT_REF] -> Range -> REF_SPEC
Component_ref ([UNIT_REF] -> [UNIT_REF]
forall a. [a] -> [a]
reverse [UNIT_REF]
anaRefs) Range
range)
  Refinement beh :: Bool
beh uspec :: UNIT_SPEC
uspec gMapList :: [G_mapping]
gMapList rspec :: REF_SPEC
rspec range :: Range
range ->
   do
     let rn' :: IRI
rn' = if Bool
src then String -> IRI -> IRI
addSuffixToIRI "_source" IRI
rn
                      else IRI
rn
     -- beh will be ignored for now
     (_rsig :: RefSig
_rsig@(BranchRefSig _ (usig :: UnitSig
usig, _)), dg' :: DGraph
dg', asp' :: UNIT_SPEC
asp') <- 
           LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> IRI
-> MaybeNode
-> Maybe RTPointer
-> UNIT_SPEC
-> Result (RefSig, DGraph, UNIT_SPEC)
anaUnitSpec LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo IRI
rn' MaybeNode
nsig Maybe RTPointer
nP UNIT_SPEC
uspec 
     (_, _, _, _rsig' :: RefSig
_rsig'@(BranchRefSig n2 :: RTPointer
n2 (usig' :: UnitSig
usig', bsig :: Maybe BranchSig
bsig)), dgr' :: DGraph
dgr', rsp' :: REF_SPEC
rsp') <-
       Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> MaybeNode
-> IRI
-> ExtStUnitCtx
-> Maybe RTPointer
-> REF_SPEC
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
      REF_SPEC)
anaRefSpec Bool
False LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
dg' HetcatsOpts
opts ExpOverrides
eo MaybeNode
nsig IRI
rn ExtStUnitCtx
emptyExtStUnitCtx Maybe RTPointer
forall a. Maybe a
Nothing REF_SPEC
rspec
             -- here Nothing is fine
     case (UnitSig
usig, UnitSig
usig') of
       (UnitSig _ls :: [NodeSig]
_ls ns :: NodeSig
ns _, UnitSig _ls' :: [NodeSig]
_ls' ns' :: NodeSig
ns' _) -> do
               DGraph
dg'' <- LogicGraph
-> DGraph
-> NodeSig
-> NodeSig
-> [G_mapping]
-> IRI
-> Result DGraph
anaSymbMapRef LogicGraph
lgraph DGraph
dgr' NodeSig
ns NodeSig
ns' [G_mapping]
gMapList IRI
rn
               let (s :: Node
s, dg3 :: DGraph
dg3) = case Maybe RTPointer
nP of
                               Nothing -> DGraph -> UnitSig -> String -> (Node, DGraph)
addNodeRT DGraph
dg'' UnitSig
usig (UNIT_SPEC -> String
name UNIT_SPEC
uspec)
                               Just p :: RTPointer
p ->
                                 case RTPointer -> RTLeaves
refTarget RTPointer
p of
                                  RTLeaf x :: Node
x -> (Node
x, DGraph
dg'')
                                  _ -> String -> (Node, DGraph)
forall a. HasCallStack => String -> a
error "can't refine to component!"
                   dg4 :: DGraph
dg4 = DGraph -> Node -> Node -> DGraph
addRefEdgeRT DGraph
dg3 Node
s (RTPointer -> Node
refSource RTPointer
n2)
               ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
 REF_SPEC)
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
      REF_SPEC)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Maybe DiagNodeSig
forall a. Maybe a
Nothing, Maybe Diag
forall a. Maybe a
Nothing,
                       RTPointer -> (UnitSig, Maybe BranchSig) -> RefSig
BranchRefSig (RTPointer -> RTPointer -> RTPointer
compPointer (Node -> RTPointer
NPUnit Node
s) RTPointer
n2)
                                    (UnitSig
usig, Maybe BranchSig
bsig) , DGraph
dg4,
                    Bool -> UNIT_SPEC -> [G_mapping] -> REF_SPEC -> Range -> REF_SPEC
Refinement Bool
beh UNIT_SPEC
asp' [G_mapping]
gMapList REF_SPEC
rsp' Range
range)

 where
  name :: UNIT_SPEC -> String
name usp :: UNIT_SPEC
usp = case UNIT_SPEC
usp of
              Spec_name x :: IRI
x -> IRI -> String
iriToStringShortUnsecure IRI
x
              Unit_type argSpecs :: [Annoted SPEC]
argSpecs resultSpec :: Annoted SPEC
resultSpec _ ->
                case [Annoted SPEC]
argSpecs of
                 [] -> case Annoted SPEC
resultSpec of
                        Annoted (Spec_inst spn :: IRI
spn [] _ _) _ _ _ ->
                            IRI -> String
iriToStringShortUnsecure IRI
spn
                        _ -> ""
                 _ -> ""
              _ -> ""


anaSymbMapRef :: LogicGraph -> DGraph -> NodeSig -> NodeSig -> [G_mapping]
  -> SPEC_NAME -> Result DGraph
anaSymbMapRef :: LogicGraph
-> DGraph
-> NodeSig
-> NodeSig
-> [G_mapping]
-> IRI
-> Result DGraph
anaSymbMapRef lg :: LogicGraph
lg dg' :: DGraph
dg' ns :: NodeSig
ns ns' :: NodeSig
ns' symbMap :: [G_mapping]
symbMap rn :: IRI
rn = do
   let gSigS :: G_sign
gSigS = NodeSig -> G_sign
getSig NodeSig
ns
       nodeS :: Node
nodeS = NodeSig -> Node
getNode NodeSig
ns
       gSigT :: G_sign
gSigT = NodeSig -> G_sign
getSig NodeSig
ns'
       nodeT :: Node
nodeT = NodeSig -> Node
getNode NodeSig
ns'
   G_sign lidS :: lid
lidS sigS :: ExtSign sign symbol
sigS _ <- G_sign -> Result G_sign
forall (m :: * -> *) a. Monad m => a -> m a
return G_sign
gSigS
   G_sign lidT :: lid
lidT sigT :: ExtSign sign symbol
sigT _ <- G_sign -> Result G_sign
forall (m :: * -> *) a. Monad m => a -> m a
return G_sign
gSigT
   AnyLogic
cl <- String -> LogicGraph -> Result AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> LogicGraph -> m AnyLogic
lookupCurrentLogic "anaSymbMapRef" LogicGraph
lg
   G_symb_map_items_list lid :: lid
lid sis :: [symb_map_items]
sis <- AnyLogic -> [G_mapping] -> Result G_symb_map_items_list
homogenizeGM AnyLogic
cl [G_mapping]
symbMap
   ExtSign sign symbol
sigS' <- 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
lidS lid
lid "anaSymbMapRef1" ExtSign sign symbol
sigS
   ExtSign sign symbol
sigT' <- 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
lidT lid
lid "anaSymbMapRef2" ExtSign sign symbol
sigT
   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
lid (ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symbol
sigS')
     (sign -> Maybe sign
forall a. a -> Maybe a
Just (sign -> Maybe sign) -> sign -> Maybe sign
forall a b. (a -> b) -> a -> b
$ ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symbol
sigT') [symb_map_items]
sis
   morphism
mor <- lid
-> EndoMap raw_symbol
-> ExtSign sign 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
-> ExtSign sign symbol
-> Result morphism
ext_induced_from_to_morphism lid
lid EndoMap raw_symbol
rmap ExtSign sign symbol
sigS' ExtSign sign symbol
sigT'
   let gm :: GMorphism
gm = 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
lid morphism
mor
       -- for now we stay in the homogeneous case
       linkLabel :: DGLinkLab
linkLabel = GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink GMorphism
gm DGLinkType
globalThm (IRI -> DGLinkOrigin
DGLinkRefinement IRI
rn)
       (_, dg'' :: DGraph
dg'') = LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG (Node
nodeS, Node
nodeT, DGLinkLab
linkLabel) DGraph
dg'
   DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return DGraph
dg''

addSuffixToNode :: String -> Node -> IRI
addSuffixToNode :: String -> Node -> IRI
addSuffixToNode s :: String
s n :: Node
n = String -> IRI -> IRI
addSuffixToIRI String
s (IRI -> IRI) -> IRI -> IRI
forall a b. (a -> b) -> a -> b
$ SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ String -> SIMPLE_ID
mkSimpleId (String -> SIMPLE_ID) -> String -> SIMPLE_ID
forall a b. (a -> b) -> a -> b
$
                      Node -> String
forall a. Show a => a -> String
show Node
n

-- | Analyse a list of argument specifications
anaArgSpecs :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts
  -> ExpOverrides -> SPEC_NAME
  -> [Annoted SPEC] -> Result ([NodeSig], DGraph, [Annoted SPEC])
anaArgSpecs :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> IRI
-> [Annoted SPEC]
-> Result ([NodeSig], DGraph, [Annoted SPEC])
anaArgSpecs lgraph :: LogicGraph
lgraph libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo usName :: IRI
usName args :: [Annoted SPEC]
args = let
 anaArgSpecsAux :: DGraph
-> Node
-> [Annoted SPEC]
-> Result ([NodeSig], DGraph, [Annoted SPEC])
anaArgSpecsAux aDG :: DGraph
aDG x :: Node
x args' :: [Annoted SPEC]
args' = case [Annoted SPEC]
args' of
  [] -> ([NodeSig], DGraph, [Annoted SPEC])
-> Result ([NodeSig], DGraph, [Annoted SPEC])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], DGraph
aDG, [])
  argSpec :: Annoted SPEC
argSpec : argSpecs :: [Annoted SPEC]
argSpecs -> do
       AnyLogic
l <- String -> String -> LogicGraph -> Result AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> String -> LogicGraph -> m AnyLogic
lookupLogic "anaArgSpecs " (LogicGraph -> String
currentLogic LogicGraph
lgraph) LogicGraph
lgraph
       let sp :: SPEC
sp = Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
argSpec
           xIRI :: IRI
xIRI = String -> IRI -> IRI
addSuffixToIRI ("_arg" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Node -> String
forall a. Show a => a -> String
show Node
x) IRI
usName
           xName :: NodeName
xName = DGraph -> IRI -> Node -> NodeName
ensureUniqueNames DGraph
aDG IRI
xIRI 1
       (argSpec' :: SPEC
argSpec', argSig :: NodeSig
argSig, dg' :: DGraph
dg') <- 
           Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
False Bool
False -- don't optimize the node out 
              LogicGraph
lgraph LibEnv
libEnv LibName
ln DGraph
aDG (AnyLogic -> MaybeNode
EmptyNode AnyLogic
l) 
              (NodeName
xName{extIndex :: Node
extIndex = Node
x Node -> Node -> Node
forall a. Num a => a -> a -> a
+ 1})
              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
       (argSigs :: [NodeSig]
argSigs, dg'' :: DGraph
dg'', argSpecs' :: [Annoted SPEC]
argSpecs') <-
           DGraph
-> Node
-> [Annoted SPEC]
-> Result ([NodeSig], DGraph, [Annoted SPEC])
anaArgSpecsAux DGraph
dg' (Node
x Node -> Node -> Node
forall a. Num a => a -> a -> a
+ 1 ::Int) [Annoted SPEC]
argSpecs
       ([NodeSig], DGraph, [Annoted SPEC])
-> Result ([NodeSig], DGraph, [Annoted SPEC])
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeSig
argSig NodeSig -> [NodeSig] -> [NodeSig]
forall a. a -> [a] -> [a]
: [NodeSig]
argSigs, DGraph
dg'', SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted SPEC
argSpec' Annoted SPEC
argSpec
                          Annoted SPEC -> [Annoted SPEC] -> [Annoted SPEC]
forall a. a -> [a] -> [a]
: [Annoted SPEC]
argSpecs')
 in DGraph
-> Node
-> [Annoted SPEC]
-> Result ([NodeSig], DGraph, [Annoted SPEC])
anaArgSpecsAux DGraph
dg 0 [Annoted SPEC]
args

{- | Check that given diagram ensures amalgamability along given set
of morphisms -}
assertAmalgamability
  :: HetcatsOpts         -- ^ the program options
  -> Range               -- ^ the position (for diagnostics)
  -> Diag                -- ^ the diagram to be checked
  -> [(Node, GMorphism)] -- ^ the sink
  -> String              -- ^ the unit expr as a string
  -> Result ()
assertAmalgamability :: HetcatsOpts
-> Range -> Diag -> [(Node, GMorphism)] -> String -> Result ()
assertAmalgamability opts :: HetcatsOpts
opts pos :: Range
pos diag :: Diag
diag sink :: [(Node, GMorphism)]
sink uexp :: String
uexp = do
  Amalgamates
ensAmalg <- HetcatsOpts
-> Range -> Diag -> [(Node, GMorphism)] -> Result Amalgamates
homogeneousEnsuresAmalgamability HetcatsOpts
opts Range
pos Diag
diag [(Node, GMorphism)]
sink
  case Amalgamates
ensAmalg of
    Amalgamates -> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    NoAmalgamation msg :: String
msg -> () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
plain_error ()
      ("Amalgamability is not ensured: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
uexp) Range
pos
    DontKnow msg :: String
msg -> () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
warning () String
msg Range
pos

-- | Check the amalgamability assuming common logic for whole diagram
homogeneousEnsuresAmalgamability
  :: HetcatsOpts  -- ^ the program options
  -> Range  -- ^ the position (for diagnostics)
  -> Diag   -- ^ the diagram to be checked
  -> [(Node, GMorphism)] -- ^ the sink
  -> Result Amalgamates
homogeneousEnsuresAmalgamability :: HetcatsOpts
-> Range -> Diag -> [(Node, GMorphism)] -> Result Amalgamates
homogeneousEnsuresAmalgamability opts :: HetcatsOpts
opts pos :: Range
pos diag :: Diag
diag sink :: [(Node, GMorphism)]
sink = case [(Node, GMorphism)]
sink of
  [] -> Amalgamates -> String -> Range -> Result Amalgamates
forall a. a -> String -> Range -> Result a
plain_error Amalgamates
defaultDontKnow
        "homogeneousEnsuresAmalgamability: Empty sink" Range
pos
  lab' :: (Node, GMorphism)
lab' : _ -> do
    let (_, mor :: GMorphism
mor) = (Node, GMorphism)
lab'
        sig :: G_sign
sig = GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
mor
    G_sign lid :: lid
lid _ _ <- G_sign -> Result G_sign
forall (m :: * -> *) a. Monad m => a -> m a
return G_sign
sig
    Gr sign (Node, morphism)
hDiag <- lid -> Diag -> Result (Gr sign (Node, 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 -> Diag -> Result (Gr sign (Node, morphism))
homogeniseDiagram lid
lid Diag
diag
    [(Node, morphism)]
hSink <- lid -> [(Node, GMorphism)] -> Result [(Node, 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 -> [(Node, GMorphism)] -> Result [(Node, morphism)]
homogeniseSink lid
lid [(Node, GMorphism)]
sink
    lid
-> ([CASLAmalgOpt], Gr sign (Node, morphism), [(Node, morphism)],
    Gr String String)
-> Result Amalgamates
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
-> ([CASLAmalgOpt], Gr sign (Node, morphism), [(Node, morphism)],
    Gr String String)
-> Result Amalgamates
ensures_amalgamability lid
lid (HetcatsOpts -> [CASLAmalgOpt]
caslAmalg HetcatsOpts
opts, Gr sign (Node, morphism)
hDiag, [(Node, morphism)]
hSink, Diag -> Gr String String
diagDesc Diag
diag)

-- | Get a position within the source file of a UNIT-TERM
getPosUnitTerm :: UNIT_TERM -> Range
getPosUnitTerm :: UNIT_TERM -> Range
getPosUnitTerm ut :: UNIT_TERM
ut = case UNIT_TERM
ut of
  Unit_reduction _ restr :: RESTRICTION
restr -> case RESTRICTION
restr of
    -- obtain position from RESTRICTION
    Hidden _ poss :: Range
poss -> Range
poss
    Revealed _ poss :: Range
poss -> Range
poss
  Unit_translation _ (Renaming _ poss :: Range
poss) -> Range
poss
  Amalgamation _ poss :: Range
poss -> Range
poss
  Local_unit _ _ poss :: Range
poss -> Range
poss
  Unit_appl u :: IRI
u _ poss :: Range
poss -> Range -> Range -> Range
appRange (IRI -> Range
iriPos IRI
u) Range
poss
  Group_unit_term _ poss :: Range
poss -> Range
poss

-- | Get a position within the source file of UNIT-IMPORTED
getPosUnitImported :: Range -> Range
getPosUnitImported :: Range -> Range
getPosUnitImported (Range ps :: [Pos]
ps) = [Pos] -> Range
Range ([Pos] -> Range) -> [Pos] -> Range
forall a b. (a -> b) -> a -> b
$ case [Pos]
ps of
  [] -> []
  _ : qs :: [Pos]
qs -> if [Pos] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pos]
qs then [Pos]
ps else [Pos]
qs

-- | Get a position within the source file of UNIT-EXPRESSION
getPosUnitExpression :: UNIT_EXPRESSION -> Range
getPosUnitExpression :: UNIT_EXPRESSION -> Range
getPosUnitExpression (Unit_expression _ (Annoted ut :: UNIT_TERM
ut _ _ _) poss :: Range
poss) =
    Range -> Range -> Range
appRange (UNIT_TERM -> Range
getPosUnitTerm UNIT_TERM
ut) Range
poss