{- |

Module : ./Static/AnalysisArchitecture.hs

Description : static analysis of CASL architectural specifications

Copyright : (c) Maciek Makowski, Warsaw University, C. Maeder 2004-2006

Mihai Codescu, DFKI GmbH Bremen 2010

License : GPLv2 or higher, see LICENSE.txt

Maintainer : till@informatik.uni-bremen.de

Stability : provisional

Portability : non-portable (via imports)

Static analysis of CASL architectural specifications

Follows the extended static semantics sketched in Chap. III:5.6

of the CASL Reference Manual.

-}

module Static.AnalysisArchitecture

( anaArchSpec

, anaUnitSpec

, anaRefSpec

) where

import Driver.Options

import Logic.Logic

import Logic.ExtSign

import Logic.Coerce

import Logic.Grothendieck

import Static.GTheory

import Static.DevGraph

import Static.DgUtils

import Static.ArchDiagram

import Static.AnalysisStructured

import Syntax.Print_AS_Architecture ()

import Syntax.AS_Architecture

import Syntax.Print_AS_Structured

import Syntax.AS_Structured

import Common.AS_Annotation

import Common.ExtSign

import Common.Id

import Common.IRI

import Common.LibName

import Common.Result

import Common.Amalgamate

import Common.Doc

import qualified Data.Map as Map

import Data.Maybe

import Data.Graph.Inductive.Graph as Graph (Node, lab)

import qualified Data.Set as Set

import Control.Monad (foldM)

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

first (a, _, _) = a

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

second (_, b, _) = b

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

third (_, _, 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 lgraph libEnv ln dg opts eo sharedCtx nP archSp = case archSp of

Basic_arch_spec udd uexpr pos ->

do (branchMap, uctx, dg', udd') <-

anaUnitDeclDefns lgraph libEnv ln dg opts eo sharedCtx udd

(nodes, usig, diag'', dg'', uexpr') <-

anaUnitExpression lgraph libEnv ln dg' opts eo uctx $ item uexpr

let (nodes', maybeRes) = case nodes of

[] -> ([], Nothing) -- don't think its possible

[x] -> ([], Just x)

_ -> (nodes, Nothing)

rNodes = map refSource $ Map.elems branchMap

(rN, dg3) =

case nP of

Nothing -> let

(n, dgI) = addNodeRT dg'' usig "ArchSpec"

in (n, addEdgesToNodeRT dgI rNodes n)

Just x -> (x, addEdgesToNodeRT dg' rNodes x)

rP = NPBranch rN branchMap

return (nodes', maybeRes, diag'',

BranchRefSig rP (usig, Just $ BranchStaticContext (ctx uctx)),

dg3, Basic_arch_spec udd'

(replaceAnnoted uexpr' uexpr) pos)

Group_arch_spec asp _ ->

anaArchSpec lgraph libEnv ln dg opts eo sharedCtx nP (item asp)

Arch_spec_name un' -> do

asi <- expCurieR (globalAnnos dg) eo un'

case lookupGlobalEnvDG asi dg of

Just (ArchOrRefEntry True asig@(BranchRefSig

(NPBranch n f) (UnitSig nsList resNs _, _))) -> do

let (rN, dg', asig') =

case nP of

Nothing -> let

(dg0, g) = copySubTree dg n Nothing

n0 = Map.findWithDefault (error "copy") n g

(r1, d1) = (n0, dg0) -- TODO: this is not needed

a1 = setPointerInRef asig (NPBranch r1 $

Map.map (mapRTNodes g) f)

in (r1, d1, a1)

Just x -> let

(dg0, g) = copySubTree dg n Nothing

n0 = Map.findWithDefault (error "copy") n g

d1 = addRefEdgeRT dg0 x n0

a1 = setPointerInRef asig (NPBranch rN $

Map.map (mapRTNodes g) f)

in (x, d1, a1)

case nsList of

[] ->

return ([], Nothing, snd sharedCtx, asig', dg', archSp)

_ -> do

(dnsigs, diag') <- foldM (\ (l, d) ns -> do

(dns, d') <- extendDiagramIncl lgraph d [] ns "Arch Sig"

return (dns : l, d'))

([], snd sharedCtx) $ reverse nsList

(dns, diag'') <-

extendDiagramIncl lgraph diag' dnsigs resNs "arch sig"

return (dns : dnsigs, Nothing, diag'', asig', dg', archSp)

_ -> notFoundError "architectural specification" 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 lgraph libEnv ln dg opts eo sharedCtx =

anaUnitDeclDefns' lgraph libEnv ln dg opts eo sharedCtx 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' lgraph libEnv ln dg opts eo uctx rNodes uds = case uds of

udd : udds -> do

(rNodes1, uctx', dg', udd') <-

anaUnitDeclDefn lgraph libEnv ln dg opts eo uctx (item udd)

(rNodes2, uctx'', dg'', udds') <- anaUnitDeclDefns' lgraph libEnv ln dg' opts eo

uctx' (Map.union rNodes1 rNodes) udds

return (rNodes2, uctx'', dg'', replaceAnnoted udd' udd : udds')

[] -> return (rNodes, uctx, dg, [])

alreadyDefinedUnit :: IRI -> String

alreadyDefinedUnit u =

"Unit " ++ iriToStringUnsecure u ++ " already declared/defined"

-- | Create a node that represents a union of signatures

nodeSigUnion :: LogicGraph -> DGraph -> [MaybeNode] -> DGOrigin -> SPEC_NAME

-> Result (NodeSig, DGraph)

nodeSigUnion lgraph dg nodeSigs orig sname =

do sigUnion@(G_sign lid sigU ind) <- gsigManyUnion lgraph

$ map getMaybeSig nodeSigs

let unionName = makeName $ addSuffixToIRI "_union" sname

nodeContents = newNodeLab

(unionName{extIndex = 1})

orig

$ noSensGTheory lid sigU ind

node = getNewNodeDG dg

dg' = insNodeDG (node, nodeContents) dg

inslink dgres nsig = do

dgv <- dgres

case nsig of

EmptyNode _ -> dgres

JustNode (NodeSig n sig) -> do

incl <- ginclusion lgraph sig sigUnion

return $ insLEdgeNubDG

(n, node, globDefLink incl SeeTarget) dgv

dg'' <- foldl inslink (return dg') nodeSigs

return (NodeSig node sigUnion, 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 lgraph libEnv ln dg opts eo uctx@(buc, _) udd = case udd of

Unit_decl un' usp uts pos -> do

unIRI <- expCurieR (globalAnnos dg) eo un'

let ustr = iriToStringShortUnsecure unIRI

(dns, diag', dg', uts') <-

anaUnitImported lgraph libEnv ln dg opts eo uctx pos uts

let impSig = toMaybeNode dns

(nodes, maybeRes, mDiag, rsig', dg0, usp') <-

anaRefSpec True lgraph libEnv ln

dg' opts eo impSig unIRI (buc, diag') Nothing usp

usig@(UnitSig argSigs resultSig unionSig) <- getUnitSigFromRef rsig'

let (n, dg1, rsig0) =

case getPointerFromRef rsig' of

RTNone -> let

(n', d') = addNodeRT dg0 usig ustr

r' = setPointerInRef rsig' (NPUnit n')

in (n', d', r')

_ -> (refSource $ getPointerFromRef rsig', dg0, rsig')

{- is this above needed? when can rsig' have no pointer?

ANSWER: when it's just a unit sig -}

(dg'', rsig) <- case impSig of

EmptyNode _ -> do

(resultSig', dg2) <- case unionSig of

Just x -> nodeSigUnion lgraph dg1

[JustNode x, JustNode resultSig] DGImports unIRI

_ -> return (resultSig, dg1)

return (updateNodeNameRT dg2 n False ustr,

setUnitSigInRef rsig0 $ UnitSig argSigs resultSig' unionSig)

-- S -> T becomes S -> S \cup T

JustNode ns -> do

let dg2 = updateNodeNameRT dg1 n False ustr

-- this changes the name of the node in the RT

(argUnion, dg3) <- nodeSigUnion lgraph dg2

(map JustNode argSigs ++ [impSig])

DGImports unIRI

-- union of the arguments with the imports

(resultSig', dg4) <- nodeSigUnion lgraph dg3

[JustNode resultSig, JustNode argUnion] DGImports

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 = updateSigRT dg4 n $ UnitSig [] resultSig' Nothing

-- now stores S \cup T

usig' = UnitSig (ns : argSigs) resultSig' $ Just argUnion

(newN, dgU') = addNodeRT dgU usig' ""

newP = NPBranch n $ Map.fromList

[(simpleIdToIRI $ mkSimpleId "a", NPUnit newN)]

rUnit = UnitSig argSigs resultSig' $ Just argUnion

rSig = BranchRefSig newP (rUnit, Just $ BranchStaticContext $

Map.insert (simpleIdToIRI $ mkSimpleId "a")

(mkRefSigFromUnit usig')

Map.empty)

return (addEdgesToNodeRT dgU' [newN] n, rSig)

-- check the pointer

let diag = fromMaybe diag' mDiag

ud' = Unit_decl unIRI usp' uts' pos

case rsig of

ComponentRefSig _ _ -> error $

"component refinement forbidden in arch spec: unit"

++ ustr

_ ->

if Map.member unIRI buc

then plain_error (Map.empty, uctx, dg'', ud')

(alreadyDefinedUnit unIRI) (iriPos unIRI)

else do

_usigN@(UnitSig argSigsN resultSig' unionSigN) <-

getUnitSigFromRef rsig

(basedParUSig, diag''') <- if null argSigsN then do

(dn', diag'') <- extendDiagramIncl lgraph diag

((case dns of

JustDiagNode dn -> [dn]

_ -> []) ++

(case maybeRes of

Just x -> [x]

_ -> [])) resultSig' ustr

return (Based_unit_sig dn' rsig, diag'')

else if length nodes < 2 then do

-- clarify the pointers here

let rsig'' =

setPointerInRef

(setUnitSigInRef rsig $

UnitSig argSigsN resultSig' unionSigN)

(NPUnit n)

return (Based_par_unit_sig dns rsig''

, diag)

else do

-- here we handle U : arch spec ASP with ASP parametric

let rsig'' = setPointerInRef

(setUnitSigInRef rsig usig)

(NPUnit n)

return (Based_lambda_unit_sig nodes rsig'',

diag)

return (Map.fromList [(unIRI, getPointerFromRef rsig)],

(Map.insert unIRI basedParUSig buc, diag'''),

dg'', ud')

Unit_defn un' uexp poss -> do

un <- expCurieR (globalAnnos dg) eo un'

(nodes, usig, diag, dg'', uexp') <-

anaUnitExpression lgraph libEnv ln dg opts eo uctx uexp

let ud' = Unit_defn un uexp' poss

if Map.member un buc then

plain_error (Map.empty, uctx, dg'', ud')

(alreadyDefinedUnit un) $ iriPos un

else case 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 _ _ -> case args of

[] -> case nodes of

[dn] -> do

let bsig = Based_unit_sig dn $

mkBotSigFromUnit usig

return (Map.empty,

(Map.insert un bsig buc, diag),

dg'', ud')

_ -> error "anaUnitDeclDefn"

_ -> case nodes of

_ : _ : _ ->

return (Map.empty , (Map.insert un

(Based_lambda_unit_sig nodes $

mkBotSigFromUnit usig)

buc, diag), dg'', ud')

_ -> 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 lgraph libEnv ln dg opts eo _uctx@(_ggbuc, _diag') rN

(Unit_ref un' usp pos) = do

un <- expCurieR (globalAnnos dg) eo un'

let n = case rN of

Nothing -> Nothing

Just (NPComp f) -> Just $ Map.findWithDefault

(error "component not in map!") un f

Just (NPBranch _ f) -> Just $ Map.findWithDefault

(error "component not in map!") un f

_ -> error "components!"

curl <- lookupCurrentLogic "UNIT_REF" lgraph

let impSig = EmptyNode curl

( _, _, _, rsig, dg'', usp') <-

anaRefSpec True lgraph libEnv ln dg opts eo impSig un

emptyExtStUnitCtx n usp

let ud' = Unit_ref un usp' pos

return ((un, rsig), dg'', ud')

-- | Analyse unit imports

anaUnitImported :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts

-> ExpOverrides

-> ExtStUnitCtx -> Range -> [Annoted UNIT_TERM]

-> Result (MaybeDiagNode, Diag, DGraph, [Annoted UNIT_TERM])

anaUnitImported lgraph libEnv ln dg opts eo uctx@(_, diag) poss terms =

case terms of

[] -> do

curl <- lookupCurrentLogic "UnitImported" lgraph

return (EmptyDiagNode curl, diag, dg, [])

_ -> do

(dnsigs, diag', dg', terms') <-

anaUnitImported' lgraph libEnv ln dg opts eo uctx terms

(sig, dg'') <- nodeSigUnion lgraph dg'

(map (JustNode . getSigFromDiag) dnsigs) DGImports

(simpleIdToIRI $ mkSimpleId "imports")

let pos = getPosUnitImported poss

sink <- inclusionSink lgraph dnsigs sig

() <- assertAmalgamability opts pos diag' sink ("imports:" ++

foldl (\ x y -> x ++ " " ++ show (prettyLG lgraph y)) "" terms)

(dnsig, diag'') <- extendDiagramIncl lgraph diag' dnsigs sig

. show . sepByCommas $ map (prettyLG lgraph) terms

return (JustDiagNode dnsig, diag'', dg'', terms')

anaUnitImported' :: LogicGraph -> LibEnv -> LibName -> DGraph

-> HetcatsOpts

-> ExpOverrides

-> ExtStUnitCtx -> [Annoted UNIT_TERM]

-> Result ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])

anaUnitImported' lgraph libEnv ln dg opts eo uctx@(buc, diag) ts = case ts of

[] -> return ([], diag, dg, [])

ut : uts -> do

(dnsig, diag', dg', ut') <-

anaUnitTerm lgraph libEnv ln dg opts eo uctx (item ut)

(dnsigs, diag'', dg'', uts') <-

anaUnitImported' lgraph libEnv ln dg' opts eo (buc, diag') uts

return (dnsig : dnsigs, diag'', dg'', replaceAnnoted ut' ut : uts')

-- | Analyse an unit expression

anaUnitExpression :: LogicGraph -> LibEnv -> LibName -> DGraph

-> HetcatsOpts

-> ExpOverrides

-> ExtStUnitCtx -> UNIT_EXPRESSION

-> Result ([DiagNodeSig], UnitSig, Diag, DGraph, UNIT_EXPRESSION)

anaUnitExpression lgraph libEnv ln dg opts eo uctx@(buc, diag)

uexp@(Unit_expression ubs ut poss) = case ubs of

[] -> do

(dnsig@(Diag_node_sig _ ns'), diag', dg', ut') <-

anaUnitTerm lgraph libEnv ln dg opts eo uctx (item ut)

return ([dnsig], UnitSig [] ns' Nothing, diag', dg',

Unit_expression [] (replaceAnnoted ut' ut) poss)

_ -> do

(args, dg', ubs') <-

anaUnitBindings lgraph libEnv ln dg opts eo uctx ubs

let dexp = show $ prettyLG lgraph uexp

insNodes diag0 [] buc0 = return ([], diag0, buc0)

insNodes diag0 ((un, nsig) : args0) buc0 =

do (dnsig, diag') <- extendDiagramIncl lgraph diag0 []

nsig $ show 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 = BranchRefSig RTNone

(UnitSig [] nsig Nothing, Nothing)

buc' = Map.insert un (Based_unit_sig dnsig rsig) buc0

(dnsigs, diag'', buc'') <- insNodes diag' args0 buc'

return (dnsig : dnsigs, diag'', buc'')

(pardnsigs, diag'', buc') <- insNodes diag args buc

(resnsig, _) <- nodeSigUnion lgraph dg'

(map (JustNode . snd) args) DGFormalParams

(simpleIdToIRI $ mkSimpleId "union")

(Diag_node_sig nU _, diagI) <-

extendDiagramIncl lgraph diag''

pardnsigs resnsig 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@(Diag_node_sig _ pnsig), diag''', dg''', ut') <-

anaUnitTerm lgraph libEnv ln dg' opts eo (buc', diagI) (item ut)

-- check amalgamability conditions

let pos = getPosUnitExpression uexp

checkSubSign dnsigs nsup =

all (\ dnsub -> isSubGsign lgraph (getSig $ getSigFromDiag dnsub)

$ getSig nsup) dnsigs

-- check that signatures in pardnsigs are subsignatures of pnsig

if checkSubSign pardnsigs pnsig

then

do

sink <- inclusionSink lgraph (p : pardnsigs) pnsig

() <-

assertAmalgamability opts pos diag''' sink

("subsignature test for: " ++

show (prettyLG lgraph uexp))

-- add new node to the diagram

let (_, diag4) = matchDiagram nU diag'''

return (p : pardnsigs,

UnitSig (map snd args) pnsig $ Just resnsig,

-- check!

diag4, dg''',

Unit_expression ubs' (replaceAnnoted ut' ut) poss)

else -- report an error

fatal_error

("The body signature does not extend the parameter signatures in\n"

++ dexp) 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 lgraph libEnv ln dg opts eo uctx@(buc, _) bs = case bs of

[] -> return ([], dg, [])

Unit_binding un' usp poss : ubs -> do

un <- expCurieR (globalAnnos dg) eo un'

let unpos = iriPos un

curl <- lookupCurrentLogic "UNIT_BINDINGS" lgraph

(BranchRefSig _ (UnitSig argSigs nsig _, _), dg', usp') <-

anaUnitSpec lgraph libEnv ln dg opts eo

un (EmptyNode curl) Nothing usp

-- TODO: is un OK above? MC: yes, names are unique

let ub' = Unit_binding un usp' poss

case argSigs of

_ : _ -> plain_error ([], dg', [])

("An argument unit "

++ iriToStringUnsecure un

++ " must not be parameterized") unpos

[] ->

do (args, dg'', ubs') <- anaUnitBindings lgraph libEnv ln

dg' opts eo uctx ubs

let args' = (un, nsig) : args

if Map.member un buc

then plain_error (args', dg'', ub' : ubs')

(alreadyDefinedUnit un) unpos

else case lookup un args of

Just _ ->

plain_error (args', dg'', ub' : ubs')

(alreadyDefinedUnit un) unpos

Nothing -> return (args', dg'', ub' : 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 lgraph libEnv ln dg opts eo uctx@(buc, diag) ts = case ts of

[] -> return ([], diag, dg, [])

ut : uts -> do

(dnsig, diag', dg', ut') <-

anaUnitTerm lgraph libEnv ln dg opts eo uctx (item ut)

(dnsigs, diag'', dg'', uts') <- anaUnitTerms lgraph libEnv ln

dg' opts eo (buc, diag') uts

return (dnsig : dnsigs, diag'', dg'', replaceAnnoted ut' ut : uts')

-- | Analyse an unit term

anaUnitTerm :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts

-> ExpOverrides

-> ExtStUnitCtx -> UNIT_TERM -> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)

anaUnitTerm lgraph libEnv ln dg opts eo uctx@(buc, diag) utrm =

let pos = getPosUnitTerm utrm

utStr = show $ prettyLG lgraph utrm

in case utrm of

Unit_reduction ut restr -> do

let orig = DGRestriction (Restricted restr) Set.empty

(p@(Diag_node_sig iNode _), diag1, dg1, ut') <-

anaUnitTerm lgraph libEnv ln dg opts eo uctx (item ut)

curl <- lookupCurrentLogic "UnitTerm" lgraph

(incl, msigma) <- anaRestriction lgraph (emptyG_sign curl)

(getSig (getSigFromDiag p)) opts restr

let i = addSuffixToNode "_reduction" iNode

(q@(Diag_node_sig qn _), diag', dg') <-

extendDiagramWithMorphismRevHide pos lgraph diag1 dg1 p incl i utStr

orig

case msigma of

Nothing ->

{- the renaming morphism is just identity, so

there's no need to extend the diagram

-}

return (q, diag', dg',

Unit_reduction (replaceAnnoted ut' ut) restr)

Just sigma ->

do

-- check amalgamability conditions

let sink = [(qn, sigma)]

iN = addSuffixToNode "_amalg_reduct" qn

() <- assertAmalgamability opts pos diag' sink utStr

(q', diag'', dg'') <- extendDiagramWithMorphism pos

lgraph diag' dg' q sigma iN utStr orig

return (q', diag'', dg'',

Unit_reduction

(replaceAnnoted ut' ut) restr)

Unit_translation ut ren -> do

(dnsig@(Diag_node_sig p _), diag1, dg1, ut') <-

anaUnitTerm lgraph libEnv ln dg opts eo uctx (item ut)

-- EmptyNode $ error ... should be replaced with local env!

gMorph <- anaRenaming lgraph

(EmptyNode $ error "Static.AnalysisArchitecture")

(getSig (getSigFromDiag dnsig)) opts ren

let sink = [(p, gMorph)]

iN = addSuffixToNode "_amalg_transl" p

-- check amalamability conditions

() <- assertAmalgamability opts pos diag1 sink utStr

(dnsig', diag', dg') <- extendDiagramWithMorphism pos lgraph

diag1 dg1 dnsig gMorph iN utStr

(DGTranslation $ Renamed ren)

return (dnsig', diag', dg', Unit_translation

(replaceAnnoted ut' ut) ren)

Amalgamation uts poss -> do

(dnsigs, diag1, dg', uts') <-

anaUnitTerms lgraph libEnv ln dg opts eo uctx uts

-- compute sigma

(sig, dg'') <- nodeSigUnion lgraph dg'

(map (JustNode . getSigFromDiag) dnsigs) DGUnion

(simpleIdToIRI $ mkSimpleId "imports")

-- check amalgamability conditions

sink <- inclusionSink lgraph dnsigs sig

() <- assertAmalgamability opts poss diag1 sink utStr

(q, diag') <- extendDiagramIncl lgraph diag1 dnsigs

sig utStr

return (q, diag', dg'', Amalgamation uts' poss)

Local_unit udds ut poss -> do

(_, uctx', dg1, udds') <-

anaUnitDeclDefns' lgraph libEnv ln dg opts eo uctx Map.empty udds

(dnsig, diag', dg', ut') <-

anaUnitTerm lgraph libEnv ln dg1 opts eo uctx' (item ut)

return (dnsig, diag', dg',

Local_unit udds' (replaceAnnoted ut' ut) poss)

Unit_appl un' fargus _ -> do

un <- expCurieR (globalAnnos dg) eo un'

let ustr = iriToStringUnsecure un

argStr = show . sepByCommas $ map (prettyLG lgraph) fargus

case Map.lookup un buc of

Just (Based_unit_sig dnsig _rsig) -> case fargus of

[] -> return (dnsig, diag, dg, utrm)

_ -> plain_error (dnsig, diag, dg, utrm)

(ustr ++ " is a parameterless unit, "

++ "but arguments have been given: " ++ argStr) pos

Just (Based_par_unit_sig pI

(BranchRefSig _ (UnitSig argSigs resultSig _, _))) ->

do (sigF, dg') <- nodeSigUnion lgraph dg

(toMaybeNode pI : map JustNode argSigs) DGFormalParams

(simpleIdToIRI $ mkSimpleId ("sigF_"++argStr))

(morphSigs, dg'', diagA) <-

anaFitArgUnits lgraph libEnv ln dg' opts eo

uctx utrm pos argSigs fargus

(sigA, dg''') <- nodeSigUnion lgraph dg''

(toMaybeNode pI : map (JustNode . second) morphSigs)

DGFitSpec

(simpleIdToIRI $ mkSimpleId ("sigA_"++argStr))

-- compute morphA (\sigma^A)

G_sign lidI sigI _ <- return (getMaybeSig (toMaybeNode pI))

let idI = mkG_morphism lidI (ext_ide sigI)

morphA <- homogeneousMorManyUnion

$ idI : map first morphSigs

-- compute sigMorExt (\sigma^A(\Delta))

(_, gSigMorExt) <- extendMorphism True (getSig sigF)

(getSig resultSig) (getSig sigA) morphA

-- check amalgamability conditions

let sigMorExt = gEmbed gSigMorExt

pIL = case pI of

JustDiagNode dn -> [dn]

_ -> []

sink <- inclusionSink lgraph (pIL ++

map third morphSigs) sigA

() <- assertAmalgamability opts pos diagA sink utStr

(qB@(Diag_node_sig nqB _), diag') <-

extendDiagramIncl lgraph diagA pIL resultSig ""

-- insert nodes p^F_i and appropriate edges to the diagram

let ins diag0 dg0 [] = return (diag0, dg0)

ins diag0 dg0 ((fpi, (morph, _, tar)) : morphNodes) =

do

(diag'', dg2) <-

insertFormalParamAndVerifCond

pos lgraph

diag0 dg0

tar fpi qB

(gEmbed morph)

argStr DGTest

ins diag'' dg2 morphNodes

(diag'', dg4) <- ins diag' dg''' $ zip argSigs morphSigs

-- check amalgamability conditions

let i = addSuffixToIRI ("_amalg_"++argStr) un

(sigR, dg5) <- extendDGraph dg4 resultSig

sigMorExt i DGExtension

-- make the union of sigR with all specs of arguments

let nsigs' = reverse $ map (getSigFromDiag . third) morphSigs

gbigSigma <- gsigManyUnion lgraph $ map getSig

$ sigR : nsigs'

let xIRI = addSuffixToIRI ("_union_"++argStr) un

xName = makeName xIRI

(ns@(NodeSig node _), dg6) = insGSig dg5 xName

DGUnion gbigSigma

insE dgl (NodeSig n gsigma) = do

incl <- ginclusion lgraph gsigma gbigSigma

return $ insLink dgl incl globalDef SeeTarget n node

dg7 <- foldM insE dg6 $ sigR : nsigs'

incSink <- inclusionSink lgraph (map third morphSigs) sigR

let sink' = (nqB, sigMorExt) : incSink

assertAmalgamability opts pos diag'' sink' 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, diag''') <- extendDiagram diag'' qB

sigMorExt ns utStr

diag4 <- insInclusionEdges lgraph diag'''

(map third morphSigs) q

return (q, diag4, dg7, utrm)

Just (Based_lambda_unit_sig nodes

(BranchRefSig _ (UnitSig argSigs resultSig _, _))) ->

case nodes of

[] -> error "error in lambda expression"

_r@(Diag_node_sig rn _) : fs ->

do let fnodes = map (\ (Diag_node_sig x _) -> x) fs

(diagC, copyFun) <- copyDiagram lgraph fnodes $ snd uctx

let getCopy x =

let

x' = Map.findWithDefault (error "getCopy") x copyFun

y = lab (diagGraph diagC) x'

in

case y of

Nothing -> error "node not found"

Just (DiagNode ns _) -> Diag_node_sig x' ns

r' = getCopy rn

fs' = map getCopy fnodes

(sigF, dg') <- nodeSigUnion lgraph dg

(map JustNode argSigs) DGFormalParams

(simpleIdToIRI $ mkSimpleId ("sigF_"++argStr))

(morphSigs, dg'', diagA) <-

anaFitArgUnits lgraph libEnv ln dg' opts eo

(fst uctx, diagC) utrm pos argSigs fargus

(sigA, dg''') <- nodeSigUnion lgraph dg''

(map (JustNode . second) morphSigs)

DGFitSpec

(simpleIdToIRI $ mkSimpleId ("sigA_"++argStr))

-- compute morphA (\sigma^A)

morphA <- homogeneousMorManyUnion

$ map first morphSigs

{- compute sigMorExt (\sigma^A(\Delta))

but allow sharing between body and parameter -}

(_, gSigMorExt) <- extendMorphism False (getSig sigF)

(getSig resultSig) (getSig sigA) morphA

-- check amalgamability conditions

let sigMorExt = gEmbed gSigMorExt

sink <- inclusionSink lgraph (map third morphSigs) sigA

() <- assertAmalgamability opts pos diagA sink utStr

let eI = zip fs' $ map (\ (x, _, z) -> (x, z)) 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 diag0 dg0 [] = return (diag0, dg0)

ins diag0 dg0 ((fI, (morph, pIA)) : eIS) =

do (diag1, dg1) <-

extendDiagramWithEdge pos lgraph diag0

dg0 fI pIA (gEmbed morph) TEST

ins diag1 dg1 eIS

(diag', dg4) <- ins diagA dg''' eI

-- check amalgamability conditions

let i = addSuffixToIRI ("_amalg_"++argStr) un

(sigR, dg5) <- extendDGraph dg4 resultSig

sigMorExt i DGExtension

incSink <- inclusionSink lgraph (map third morphSigs) sigR

assertAmalgamability opts pos diag' incSink utStr

{- -- for lambda applications

-- the node qB is not added, but only the edge from r -}

(q, diag'') <- extendDiagram diag' r'

sigMorExt sigR utStr

diag3 <- insInclusionEdges lgraph diag''

(map third morphSigs) q

return (q, diag3, dg5, utrm)

_ -> fatal_error ("Undefined unit " ++ ustr) pos

Group_unit_term ut poss -> do

(dnsig, diag1, dg1, ut') <-

anaUnitTerm lgraph libEnv ln dg opts eo uctx (item ut)

return (dnsig, diag1, dg1, Group_unit_term (replaceAnnoted ut' ut) 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 lgraph libEnv ln dg opts eo uctx@(buc, diag)

appl pos nodeSigs fArgs = case (nodeSigs, fArgs) of

(nsig : nsigs, fau : faus) -> do

(gmorph, nsig', dnsig, dg1, diag1) <-

anaFitArgUnit lgraph libEnv ln dg opts eo uctx nsig fau

(morphSigs, dg', diag') <- anaFitArgUnits lgraph libEnv ln dg1 opts eo

(buc, diag1) appl pos nsigs faus

return ((gmorph, nsig', dnsig) : morphSigs, dg', diag')

([], []) -> return ([], dg, diag)

_ -> plain_error ([], dg, diag)

("non-matching number of arguments given in application\n"

++ show (prettyLG lgraph appl)) 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 lgraph libEnv ln dg opts eo uctx nsig

a@(Fit_arg_unit ut symbMap poss) = adjustPos poss $ do

let argStr = show $ prettyLG lgraph a

(p, diag', dg', _) <-

anaUnitTerm lgraph libEnv ln dg opts eo uctx (item ut)

let gsigmaS = getSig nsig

gsigmaT = getSig (getSigFromDiag p)

G_sign lidS sigmaS _ <- return gsigmaS

G_sign lidT sigmaT _ <- return gsigmaT

cl <- lookupCurrentLogic "anaFitArgUnit" lgraph

G_symb_map_items_list lid sis <- homogenizeGM cl symbMap

sigmaS' <- coerceSign lidS lid "anaFitArgUnit1" sigmaS

sigmaT' <- coerceSign lidT lid "anaFitArgUnit2" sigmaT

mor <- if isStructured opts then return (ext_ide sigmaS') else do

rmap <- stat_symb_map_items lid (plainSign sigmaS')

(Just $ plainSign sigmaT') sis

ext_induced_from_to_morphism lid rmap sigmaS' sigmaT'

let gMorph = mkG_morphism lid mor

i = addSuffixToNode ("_fit_"++argStr) $ getNode nsig

-- ^ this ensures unique names

(nsig', dg'') <- extendDGraph dg' nsig (gEmbed gMorph) i DGFitSpec

return (gMorph, nsig', p, dg'', 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 lgraph libEnv ln dg opts eo usName impsig rN usp = case usp of

Unit_type argSpecs resultSpec poss ->

case argSpecs of

[] -> case resultSpec of

Annoted (Spec_inst spn [] _ _) _ _ _

| case lookupGlobalEnvDG (fromMaybe spn

$ expCurie (globalAnnos dg) eo spn) dg of

Just (UnitEntry _) -> True

Just (SpecEntry _) -> True

-- this is needed because there are no REF_NAME in REF_SPEC

Just (ArchOrRefEntry False _) -> True

_ -> False ->

{- if argspecs are empty and resultspec is a name of unit spec

then this should be converted to a Spec_name -}

anaUnitSpec lgraph libEnv ln dg opts eo usName impsig rN (Spec_name spn)

_ -> do -- a trivial unit type

(resultSpec', resultSig, dg') <- anaSpec False True lgraph libEnv ln

dg impsig

(makeName usName)

opts eo (item resultSpec) poss

let usig = UnitSig [] resultSig Nothing

return (mkRefSigFromUnit usig , dg', Unit_type []

(replaceAnnoted resultSpec' resultSpec) poss)

_ -> do -- a non-trivial unit type

let

(argSigs, dg1, argSpecs') <-

anaArgSpecs lgraph libEnv ln dg opts eo usName argSpecs

(sigUnion, dg2) <-

case argSigs of

[argSig] -> return (argSig, dg1) -- the optimization mentioned below

_ -> nodeSigUnion lgraph dg1

(impsig : map JustNode argSigs) DGFormalParams usName

{- if i have no imports, i can optimize?

in that case, an identity morphism is introduced -}

let resName = makeName $ addSuffixToIRI "_res" usName

(resultSpec', resultSig, dg3) <- anaSpec True True lgraph libEnv ln

dg2 (JustNode sigUnion)

(resName {extIndex = 1})

opts eo (item resultSpec) poss

let usig = UnitSig argSigs resultSig $ Just sigUnion

rsig = mkRefSigFromUnit usig

return (rsig, dg3, Unit_type argSpecs'

(replaceAnnoted resultSpec' resultSpec) poss)

Spec_name un' -> do

usn <- expCurieR (globalAnnos dg) eo un'

case lookupGlobalEnvDG usn dg of

Just (UnitEntry usig) -> return (mkRefSigFromUnit usig, dg, usp)

Just (SpecEntry (ExtGenSig _gsig@(GenSig _ args unSig) nsig) ) -> do

let uSig = case unSig of

JustNode n -> Just n

_ -> Nothing

return (mkRefSigFromUnit $ UnitSig args nsig uSig, dg, usp)

Just (ArchOrRefEntry False rsig) ->

case rN of

Nothing -> let

p = getPointerFromRef rsig

(dg', newP) = addSubTree dg Nothing p

in return (setPointerInRef rsig newP , dg', usp)

Just p0 -> let l = refTarget p0 in

case l of

RTLeaf x -> let

p = getPointerFromRef rsig

(dg', p') = addSubTree dg (Just l) p

np' = compPointer (NPUnit x) p'

in return (setPointerInRef rsig np', dg', usp)

RTLeaves leaves -> let

p = getPointerFromRef rsig

in case p of

NPComp _ -> let

(dg', p') = addSubTree dg (Just l) p

np' = compPointer p0 p'

in return (setPointerInRef rsig np', dg', usp)

_ ->

case Map.size leaves of

1 ->

let (_, h@(RTLeaf x)) = head $ Map.toList leaves

(dg', p') = addSubTree dg (Just h) p

np' = compPointer (NPUnit x) p'

in return (setPointerInRef rsig np', dg', usp)

_ -> error "can't compose signatures!"

_ -> notFoundError "unit specification" usn

Closed_unit_spec usp' _ -> do

curl <- lookupCurrentLogic "UnitSpec" lgraph

anaUnitSpec lgraph libEnv ln dg opts eo usName (EmptyNode curl) rN 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 src lgraph libEnv ln dg opts eo nsig rn sharedCtx nP rsp =

case rsp of

Unit_spec asp ->

do

let rn' = if src then rn else addSuffixToIRI "_target" rn

(rsig, dg', asp') <-

anaUnitSpec lgraph libEnv ln dg opts eo rn' nsig nP asp

case rsig of

BranchRefSig _ _ -> do

usig <- getUnitSigFromRef rsig

let rP = getPointerFromRef rsig

(rsig', dg3) = case rP of

RTNone ->

let

(n, dg'') = addNodeRT dg' usig (name asp)

r' = setPointerInRef rsig (NPUnit n)

in (r', dg'')

_ -> (rsig, dg')

return ([], Nothing, Just (snd sharedCtx), rsig', dg3, Unit_spec asp')

_ ->

return ([], Nothing, Just (snd sharedCtx), rsig, dg', Unit_spec asp')

Arch_unit_spec asp poss ->

do

let x = case nP of

Nothing -> Nothing

Just p ->

case refTarget p of

RTLeaf y -> Just y

_ -> error "nyi"

(nodes, maybeRes, diag, rsig, dg', asp') <-

anaArchSpec lgraph libEnv ln dg opts eo sharedCtx x $ item asp

return (nodes, maybeRes, Just diag, rsig, dg',

Arch_unit_spec (replaceAnnoted asp' asp) poss)

{- check whether it is indeed correct

to ignore the nodes of the

lambda expressions, like you do in the following -}

Compose_ref rslist range ->

do

(dg', anaSpecs, _) <- foldM (\ (dgr, rList, rN') rsp0 ->

do

(_, _, _, rsig', dgr', rsp') <-

anaRefSpec False lgraph libEnv ln dgr opts eo nsig

(simpleIdToIRI $ mkSimpleId $

show rn ++ "gen_ref_name" ++

show (length rList) )

sharedCtx rN' rsp0

return (dgr', rList ++ [(rsig', rsp')],

Just $ getPointerFromRef rsig')

) (dg, [], nP) rslist

-- compose signatures in csig

let refSigs = map fst anaSpecs

csig <- foldM refSigComposition (head refSigs) $ tail refSigs

let compRef = Compose_ref (map snd anaSpecs) range

return ([], Nothing, Nothing, csig, dg', compRef)

Component_ref urlist range -> do

(dg', anaRefs, resultMap, pMap) <-

foldM (\ (dgr, rList, cx, ps) uref0 -> do

((n, rs), dgr', uref') <-

anaUnitRef lgraph libEnv ln dgr opts eo emptyExtStUnitCtx nP uref0

return (dgr', uref' : rList , Map.insert n rs cx,

Map.insert n (getPointerFromRef rs) ps)

) (dg, [], Map.empty, Map.empty) 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 -}

return ([], Nothing, Nothing,

ComponentRefSig (NPComp pMap) resultMap, dg',

Component_ref (reverse anaRefs) range)

Refinement beh uspec gMapList rspec range ->

do

let rn' = if src then addSuffixToIRI "_source" rn

else rn

-- beh will be ignored for now

(_rsig@(BranchRefSig _ (usig, _)), dg', asp') <-

anaUnitSpec lgraph libEnv ln dg opts eo rn' nsig nP uspec

(_, _, _, _rsig'@(BranchRefSig n2 (usig', bsig)), dgr', rsp') <-

anaRefSpec False lgraph libEnv ln dg' opts eo nsig rn emptyExtStUnitCtx Nothing rspec

-- here Nothing is fine

case (usig, usig') of

(UnitSig _ls ns _, UnitSig _ls' ns' _) -> do

dg'' <- anaSymbMapRef lgraph dgr' ns ns' gMapList rn

let (s, dg3) = case nP of

Nothing -> addNodeRT dg'' usig (name uspec)

Just p ->

case refTarget p of

RTLeaf x -> (x, dg'')

_ -> error "can't refine to component!"

dg4 = addRefEdgeRT dg3 s (refSource n2)

return ([], Nothing, Nothing,

BranchRefSig (compPointer (NPUnit s) n2)

(usig, bsig) , dg4,

Refinement beh asp' gMapList rsp' range)

where

name usp = case usp of

Spec_name x -> iriToStringShortUnsecure x

Unit_type argSpecs resultSpec _ ->

case argSpecs of

[] -> case resultSpec of

Annoted (Spec_inst spn [] _ _) _ _ _ ->

iriToStringShortUnsecure spn

_ -> ""

_ -> ""

_ -> ""

anaSymbMapRef :: LogicGraph -> DGraph -> NodeSig -> NodeSig -> [G_mapping]

-> SPEC_NAME -> Result DGraph

anaSymbMapRef lg dg' ns ns' symbMap rn = do

let gSigS = getSig ns

nodeS = getNode ns

gSigT = getSig ns'

nodeT = getNode ns'

G_sign lidS sigS _ <- return gSigS

G_sign lidT sigT _ <- return gSigT

cl <- lookupCurrentLogic "anaSymbMapRef" lg

G_symb_map_items_list lid sis <- homogenizeGM cl symbMap

sigS' <- coerceSign lidS lid "anaSymbMapRef1" sigS

sigT' <- coerceSign lidT lid "anaSymbMapRef2" sigT

rmap <- stat_symb_map_items lid (plainSign sigS')

(Just $ plainSign sigT') sis

mor <- ext_induced_from_to_morphism lid rmap sigS' sigT'

let gm = gEmbed $ mkG_morphism lid mor

-- for now we stay in the homogeneous case

linkLabel = defDGLink gm globalThm (DGLinkRefinement rn)

(_, dg'') = insLEdgeDG (nodeS, nodeT, linkLabel) dg'

return dg''

addSuffixToNode :: String -> Node -> IRI

addSuffixToNode s n = addSuffixToIRI s $ simpleIdToIRI $ mkSimpleId $

show n

-- | Analyse a list of argument specifications

anaArgSpecs :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts

-> ExpOverrides -> SPEC_NAME

-> [Annoted SPEC] -> Result ([NodeSig], DGraph, [Annoted SPEC])

anaArgSpecs lgraph libEnv ln dg opts eo usName args = let

anaArgSpecsAux aDG x args' = case args' of

[] -> return ([], aDG, [])

argSpec : argSpecs -> do

l <- lookupLogic "anaArgSpecs " (currentLogic lgraph) lgraph

let sp = item argSpec

xIRI = addSuffixToIRI ("_arg" ++ show x) usName

xName = makeName xIRI

(argSpec', argSig, dg') <-

anaSpec False False -- don't optimize the node out

lgraph libEnv ln aDG (EmptyNode l)

(xName{extIndex = x + 1})

opts eo sp $ getRange sp

(argSigs, dg'', argSpecs') <-

anaArgSpecsAux dg' (x + 1 ::Int) argSpecs

return (argSig : argSigs, dg'', replaceAnnoted argSpec' argSpec

: argSpecs')

in anaArgSpecsAux dg 0 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 opts pos diag sink uexp = do

ensAmalg <- homogeneousEnsuresAmalgamability opts pos diag sink

case ensAmalg of

Amalgamates -> return ()

NoAmalgamation msg -> plain_error ()

("Amalgamability is not ensured: " ++ msg ++ "\n for " ++ uexp) pos

DontKnow msg -> warning () msg 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 opts pos diag sink = case sink of

[] -> plain_error defaultDontKnow

"homogeneousEnsuresAmalgamability: Empty sink" pos

lab' : _ -> do

let (_, mor) = lab'

sig = cod mor

G_sign lid _ _ <- return sig

hDiag <- homogeniseDiagram lid diag

hSink <- homogeniseSink lid sink

ensures_amalgamability lid (caslAmalg opts, hDiag, hSink, diagDesc diag)

-- | Get a position within the source file of a UNIT-TERM

getPosUnitTerm :: UNIT_TERM -> Range

getPosUnitTerm ut = case ut of

Unit_reduction _ restr -> case restr of

-- obtain position from RESTRICTION

Hidden _ poss -> poss

Revealed _ poss -> poss

Unit_translation _ (Renaming _ poss) -> poss

Amalgamation _ poss -> poss

Local_unit _ _ poss -> poss

Unit_appl u _ poss -> appRange (iriPos u) poss

Group_unit_term _ poss -> poss

-- | Get a position within the source file of UNIT-IMPORTED

getPosUnitImported :: Range -> Range

getPosUnitImported (Range ps) = Range $ case ps of

[] -> []

_ : qs -> if null qs then ps else qs

-- | Get a position within the source file of UNIT-EXPRESSION

getPosUnitExpression :: UNIT_EXPRESSION -> Range

getPosUnitExpression (Unit_expression _ (Annoted ut _ _ _) poss) =

appRange (getPosUnitTerm ut) poss