{- |
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
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

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)
dg'' UnitSig
usig "ArchSpec"
in (Node
n, DGraph -> [Node] -> Node -> DGraph
dgI [Node]
rNodes Node
n)
Just x :: Node
x -> (Node
x, DGraph -> [Node] -> Node -> 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
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, [])

u =
"Unit " String -> String -> String
forall a. [a] -> [a] -> [a]
++ IRI -> String
iriToStringUnsecure IRI
u String -> String -> String
forall a. [a] -> [a] -> [a]

-- | 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
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
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 :: * -> *).
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 :: * -> *).
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 :: * -> *).
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
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
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
-> Node
-> Node
-> DGraph
dgl GMorphism
SeeTarget Node
n Node
node
DGraph
dg7 <- (DGraph -> NodeSig -> Result DGraph)
-> DGraph -> [NodeSig] -> Result DGraph
forall (t :: * -> *) (m :: * -> *) b a.
(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
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
-> Result (Diag, DGraph)
extendDiagramWithEdge Range
pos LogicGraph
lgraph Diag
diag0
DGraph
dg0 DiagNodeSig
fI DiagNodeSig
pIA (G_morphism -> GMorphism
gEmbed G_morphism
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
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 :: * -> *).
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,
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,
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)
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 :: * -> *).
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
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)
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.
(b -> a -> m b) -> b -> t a -> m b
foldM RefSig -> RefSig -> Result RefSig
refSigComposition ([RefSig] -> RefSig
forall a. [a] -> a
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])
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
argSpec :: Annoted SPEC
argSpec : argSpecs :: [Annoted SPEC]
argSpecs -> do
AnyLogic
l <- String -> String -> LogicGraph -> Result AnyLogic
forall (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
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
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