d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder{- |

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Module : $Header$

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Author : Maciek Makowski

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Year : 2004

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Copyright : (c) Maciek Makowski, Warsaw University 2004

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Maintainer : hets@tzi.de

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Stability : provisional

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Portability : non-portable (via imports)

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Analysis of architectural specifications.

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder

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

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder of the CASL Reference Manual.

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder-}

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maedermodule Static.AnalysisArchitecture (ana_ARCH_SPEC, ana_UNIT_SPEC)

e84c877ad38ce9312eab222a79f44da2015572d2Christian Maederwhere

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maederimport Maybe

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maederimport Logic.Logic

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maederimport Logic.Grothendieck

945e82ed7877917f3ab1657f555e71991372546aChristian Maederimport Common.Lib.Graph

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Static.DevGraph

945e82ed7877917f3ab1657f555e71991372546aChristian Maederimport Static.ArchDiagram

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Syntax.AS_Architecture

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Syntax.AS_Structured

d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian Maederimport Static.AnalysisStructured

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Common.AS_Annotation

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maederimport Common.Id (Token)

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maederimport Common.Result

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maederimport Common.Id

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Common.Lib.Graph

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Common.PrettyPrint

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport qualified Common.Lib.Map as Map

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Syntax.Print_AS_Architecture

945e82ed7877917f3ab1657f555e71991372546aChristian Maederimport List

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder-- import Debug.Trace

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder-- | Analyse an architectural specification

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder-- @

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder-- ARCH-SPEC ::= BASIC-ARCH-SPEC | GROUP-ARCH-SPEC | ARCH-SPEC-NAME

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder-- @

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maederana_ARCH_SPEC :: LogicGraph -> AnyLogic -- ^ the default logic

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder -> GlobalContext -> AnyLogic -- ^ current logic

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder -> Bool -- ^ should only the structure be analysed?

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder -> ARCH_SPEC -> Result (ArchSig, DGraph, ARCH_SPEC)

c1bca76471ad22ac47f05b03576974762d364339Christian Maeder-- ^ returns 1. the architectural signature of given ARCH-SPEC 2. development graph resulting from

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder-- structured specs within the arch spec and 3. ARCH_SPEC after possible conversions

7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder-- BASIC-ARCH-SPEC

945e82ed7877917f3ab1657f555e71991372546aChristian Maederana_ARCH_SPEC lgraph defl gctx@(gannos, genv, _) curl justStruct (Basic_arch_spec udd uexpr pos) =

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder do (uctx, dg', udd') <- ana_UNIT_DECL_DEFNS lgraph defl gctx curl justStruct udd

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder (_, usig, _, dg'', uexpr') <- ana_UNIT_EXPRESSION lgraph defl (gannos, genv, dg') curl justStruct uctx (item uexpr)

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder return ((ctx uctx, usig), dg'', Basic_arch_spec udd' (replaceAnnoted uexpr' uexpr) pos)

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder-- GROUP-ARCH-SPEC

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederana_ARCH_SPEC lgraph defl gctx curl justStruct (Group_arch_spec asp _) =

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder ana_ARCH_SPEC lgraph defl gctx curl justStruct (item asp)

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder-- ARCH-SPEC-NAME

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maederana_ARCH_SPEC _ defl (_, genv, dg) _ _ asp@(Arch_spec_name asn@(Token _ pos)) =

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder do case Map.lookup asn genv of

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder Nothing -> plain_error ((emptyStUnitCtx, (emptyUnitSig defl)), dg, asp)

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder ("Undefined architectural specification " ++ showPretty asn "")

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder pos

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder Just (ArchEntry asig) -> return (asig, dg, asp)

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder _ -> plain_error ((emptyStUnitCtx, (emptyUnitSig defl)), dg, asp)

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder ((showPretty asn "") ++ " is not an architectural specification")

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder pos

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder-- | Analyse a list of unit declarations and definitions

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maederana_UNIT_DECL_DEFNS :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder -> Bool -> [Annoted UNIT_DECL_DEFN]

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder -> Result (ExtStUnitCtx, DGraph, [Annoted UNIT_DECL_DEFN])

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder-- ^ returns 1. extended static unit context 2. possibly modified development graph

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder-- 3. possibly modified list of unit declarations and definitions

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maederana_UNIT_DECL_DEFNS lgraph defl gctx curl justStruct udds =

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder ana_UNIT_DECL_DEFNS' lgraph defl gctx curl justStruct emptyExtStUnitCtx udds

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maederana_UNIT_DECL_DEFNS' :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic -> Bool

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder -> ExtStUnitCtx -> [Annoted UNIT_DECL_DEFN]

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder -> Result (ExtStUnitCtx, DGraph, [Annoted UNIT_DECL_DEFN])

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maederana_UNIT_DECL_DEFNS' _ _ (_, _, dg) _ _ uctx [] =

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder do return (uctx, dg, [])

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maederana_UNIT_DECL_DEFNS' lgraph defl gctx@(gannos, genv, _) curl justStruct uctx (udd : udds) =

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder do (uctx', dg', udd') <- ana_UNIT_DECL_DEFN lgraph defl gctx curl justStruct uctx (item udd)

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder (uctx'', dg'', udds') <- ana_UNIT_DECL_DEFNS' lgraph defl (gannos, genv, dg') curl justStruct uctx' udds

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder return (uctx'', dg'', (replaceAnnoted udd' udd) : udds')

e84c877ad38ce9312eab222a79f44da2015572d2Christian Maeder

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder-- | Analyse unit declaration or definition

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maederana_UNIT_DECL_DEFN :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder -> Bool -> ExtStUnitCtx -> UNIT_DECL_DEFN -> Result (ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)

c1bca76471ad22ac47f05b03576974762d364339Christian Maeder-- ^ returns 1. extended static unit context 2. possibly modified development graph

c1bca76471ad22ac47f05b03576974762d364339Christian Maeder-- 3. possibly modified UNIT_DECL_DEFN

c1bca76471ad22ac47f05b03576974762d364339Christian Maeder

c1bca76471ad22ac47f05b03576974762d364339Christian Maeder-- unit declaration

c1bca76471ad22ac47f05b03576974762d364339Christian Maederana_UNIT_DECL_DEFN lgraph defl gctx@(gannos, genv, _) curl justStruct

c1bca76471ad22ac47f05b03576974762d364339Christian Maeder uctx@(buc, _) (Unit_decl un@(Token _ unpos) usp uts pos) =

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder do (dns, diag', dg', uts') <- ana_UNIT_IMPORTED lgraph defl gctx curl justStruct uctx pos uts

e84c877ad38ce9312eab222a79f44da2015572d2Christian Maeder let impSig = getSigFromDiag dns

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder (usig, dg'', usp') <- ana_UNIT_SPEC lgraph defl (gannos, genv, dg') curl justStruct impSig usp

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder let ud' = Unit_decl un usp' uts' pos

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder if Map.member un buc

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder then

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder plain_error (uctx, dg'', ud')

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder ("Unit " ++ showPretty un " already declared/defined")

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder unpos

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder else

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder case usig of

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder Par_unit_sig (argSigs, resultSig) ->

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder do (resultSig', dg''') <- nodeSigUnion lgraph dg'' (resultSig : [impSig]) DGImports

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder let basedParUSig = Based_par_unit_sig (dns, (argSigs, resultSig'))

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder return ((Map.insert un basedParUSig buc, diag'), dg''', ud')

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder Unit_sig nsig ->

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder do (nsig', dg''') <- nodeSigUnion lgraph dg'' (impSig : [nsig]) DGImports

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder (dn', diag'') <- extendDiagram lgraph diag' [dns] nsig' (renderText Nothing (printText un))

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder return ((Map.insert un (Based_unit_sig dn') buc, diag''), dg''', ud')

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder-- unit definition

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maederana_UNIT_DECL_DEFN lgraph defl gctx curl justStruct uctx@(buc, _)

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder (Unit_defn un@(Token _ unpos) uexp poss) =

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder do (p, usig, diag, dg', uexp') <- ana_UNIT_EXPRESSION lgraph defl gctx curl justStruct uctx uexp

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder let ud' = Unit_defn un uexp' poss

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder {- it's sufficient to check that un is not mapped in buc, we don't need

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder to convert the ExtStUnitCtx to StUnitCtx as the domain will be preserved -}

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder if Map.member un buc

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder then

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder plain_error (uctx, dg', ud')

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder ("Unit " ++ showPretty un " already defined/declared")

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder unpos

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder else

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder case usig of

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder {- we can use Map.insert as there are no mappings for un in ps and bs

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder (otherwise there would have been a mapping in (ctx uctx)) -}

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder Unit_sig _ -> return ((Map.insert un (Based_unit_sig p) buc, diag),

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder dg', ud')

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder Par_unit_sig parusig -> return ((Map.insert un (Based_par_unit_sig (p, parusig)) buc, diag),

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder dg', ud')

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder-- | Analyse unit imports

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maederana_UNIT_IMPORTED :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder -> Bool -> ExtStUnitCtx -> [Pos] -> [Annoted UNIT_TERM]

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

d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian Maederana_UNIT_IMPORTED _ _ (_, _, dg) curl _ (_, diag) _ [] =

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder do return (Empty_node curl, diag, dg, [])

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maederana_UNIT_IMPORTED lgraph defl gctx curl justStruct uctx poss terms =

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder do (dnsigs, diag', dg', terms') <- ana_UNIT_IMPORTED' lgraph defl gctx curl justStruct uctx terms

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder (sig, dg'') <- nodeSigUnion lgraph dg' (map getSigFromDiag dnsigs) DGImports

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder -- check amalgamability conditions

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder -- let incl s = propagateErrors (ginclusion lgraph (getSig (getSigFromDiag s)) (getSig sig))

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder (dnsig@(Diag_node_sig n _), diag'') <- extendDiagram lgraph diag' dnsigs sig (renderText Nothing (printText terms))

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder let pos = getPos_UNIT_IMPORTED poss

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder () <- assertAmalgamability pos diag'' (inn diag'' n)

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder return (dnsig, diag'', dg'', terms')

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maederana_UNIT_IMPORTED' :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder -> Bool -> ExtStUnitCtx -> [Annoted UNIT_TERM]

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

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maederana_UNIT_IMPORTED' _ _ (_, _, dg) _ _ (_, diag) [] =

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder do return ([], diag, dg, [])

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maederana_UNIT_IMPORTED' lgraph defl gctx@(gannos, genv, _) curl justStruct uctx@(buc, _) (ut : uts) =

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder do (dnsig, diag', dg', ut') <- ana_UNIT_TERM lgraph defl gctx curl justStruct uctx (item ut)

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder (dnsigs, diag'', dg'', uts') <- ana_UNIT_IMPORTED' lgraph defl (gannos, genv, dg') curl justStruct (buc, diag') uts

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

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder

19ee4b7a88b9d410cb73bd81f7289410c71557c1Christian Maeder

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder-- | Analyse an unit expression

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maederana_UNIT_EXPRESSION :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic

19ee4b7a88b9d410cb73bd81f7289410c71557c1Christian Maeder -> Bool -> ExtStUnitCtx -> UNIT_EXPRESSION

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder -> Result (DiagNodeSig, UnitSig, Diag, DGraph, UNIT_EXPRESSION)

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maederana_UNIT_EXPRESSION lgraph defl gctx curl justStruct uctx (Unit_expression [] ut poss) =

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder do (dnsig, diag', dg', ut') <- ana_UNIT_TERM lgraph defl gctx curl justStruct uctx (item ut)

4ed68712ee368cbebfeaa327968583cb022e3c72Christian Maeder return (dnsig, Unit_sig (getSigFromDiag dnsig), diag', dg',

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder Unit_expression [] (replaceAnnoted ut' ut) poss)

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maederana_UNIT_EXPRESSION lgraph defl gctx@(gannos, genv, _) curl justStruct

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder uctx@(buc, diag) exp@(Unit_expression ubs ut poss) =

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder do (args, dg', ubs') <- ana_UNIT_BINDINGS lgraph defl gctx curl justStruct uctx ubs

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder (resnsig, dg'') <- nodeSigUnion lgraph dg' (map snd args) DGFormalParams

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder -- build the extended diagram and new based unit context

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder let insNodes diag [] buc = do return ([], diag, buc)

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder insNodes diag ((un, nsig) : args) buc =

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder do (dnsig, diag') <- extendDiagram lgraph diag [] nsig (renderText Nothing (printText exp))

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder {- we made sure in ana_UNIT_BINDINGS that there's no mapping for un in buc

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder so we can just use Map.insert -}

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder let buc' = Map.insert un (Based_unit_sig dnsig) buc

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder (dnsigs, diag'', buc'') <- insNodes diag' args buc'

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder return (dnsig : dnsigs, diag'', buc'')

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder (pardnsigs, diag', buc') <- insNodes diag args buc

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder (_, diag'') <- extendDiagram lgraph diag' pardnsigs resnsig (renderText Nothing (printText exp))

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder -- analyse the unit term

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder (p@(Diag_node_sig n _), diag''', dg''', ut') <- ana_UNIT_TERM lgraph defl (gannos, genv, dg'')

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder curl justStruct (buc', diag'') (item ut)

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder -- insert diagram edges from the parameter nodes to the node representing unit term

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder diag4 <- insInclusionEdges lgraph diag''' pardnsigs p

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder -- check amalgamability conditions

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder let pos = getPos_UNIT_EXPRESSION exp

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder () <- assertAmalgamability pos diag4 (inn diag4 n)

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder -- add new node to the diagram

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder (z, diag5) <- extendDiagram lgraph diag4 [] (EmptyNode curl) (renderText Nothing (printText exp))

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder return (z, Par_unit_sig (map snd args, getSigFromDiag p), diag5, dg''',

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder Unit_expression ubs' (replaceAnnoted ut' ut) poss)

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder-- | Analyse a list of unit bindings. Ensures that the unit names are not present

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder-- in extended static unit context and that there are no duplicates among them.

945e82ed7877917f3ab1657f555e71991372546aChristian Maederana_UNIT_BINDINGS :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder -> Bool -> ExtStUnitCtx -> [UNIT_BINDING]

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder -> Result ([(SIMPLE_ID, NodeSig)], DGraph, [UNIT_BINDING])

945e82ed7877917f3ab1657f555e71991372546aChristian Maederana_UNIT_BINDINGS _ _ (_, _, dg) _ _ _ [] =

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder do return ([], dg, [])

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maederana_UNIT_BINDINGS lgraph defl gctx@(gannos, genv, _) curl justStruct uctx@(buc, _)

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder ((Unit_binding un@(Token _ unpos) usp poss) : ubs) =

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder do (usig, dg', usp') <- ana_UNIT_SPEC lgraph defl gctx curl justStruct (EmptyNode curl) usp

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder let ub' = Unit_binding un usp' poss

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder case usig of

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder Par_unit_sig _ -> plain_error ([], dg', [])

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder ("An argument unit " ++ showPretty un " must not be parameterized")

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder unpos

f0221ee7b9f8660e7c7add896e151f7a4ac8b4adChristian Maeder Unit_sig nsig ->

f0221ee7b9f8660e7c7add896e151f7a4ac8b4adChristian Maeder do (args, dg'', ubs') <- ana_UNIT_BINDINGS lgraph defl (gannos, genv, dg') curl justStruct uctx ubs

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder let args' = (un, nsig) : args

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder if Map.member un buc

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder then

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

7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder ("Unit " ++ showPretty un " already declared/defined")

b579e1a98aa30fb6093cbbdfeae51edbd5ba26adChristian Maeder unpos

b579e1a98aa30fb6093cbbdfeae51edbd5ba26adChristian Maeder else

b579e1a98aa30fb6093cbbdfeae51edbd5ba26adChristian Maeder case lookup un args of

187e09da24d6ed264eeeef48eb3fcc2b8663ca46Christian Maeder Just _ -> plain_error (args', dg'', ub' : ubs')

187e09da24d6ed264eeeef48eb3fcc2b8663ca46Christian Maeder ("Unit " ++ showPretty un " already declared/defined")

7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder unpos

7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder Nothing -> return (args', dg'', ub' : ubs')

7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder

7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder

7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder-- | Analyse a list of unit terms

7710f7c3425e45af11af124ff37bec27229d24f7Christian Maederana_UNIT_TERMS :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic

7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder -> Bool -> ExtStUnitCtx -> [Annoted UNIT_TERM]

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

b579e1a98aa30fb6093cbbdfeae51edbd5ba26adChristian Maederana_UNIT_TERMS _ _ (_, _, dg) _ _ (_, diag) [] =

b579e1a98aa30fb6093cbbdfeae51edbd5ba26adChristian Maeder do return ([], diag, dg, [])

b579e1a98aa30fb6093cbbdfeae51edbd5ba26adChristian Maederana_UNIT_TERMS lgraph defl gctx@(gannos, genv, _) curl justStruct uctx@(buc, _) (ut : uts) =

f0221ee7b9f8660e7c7add896e151f7a4ac8b4adChristian Maeder do (dnsig, diag', dg', ut') <- ana_UNIT_TERM lgraph defl gctx curl justStruct uctx (item ut)

b579e1a98aa30fb6093cbbdfeae51edbd5ba26adChristian Maeder (dnsigs, diag'', dg'', uts') <- ana_UNIT_TERMS lgraph defl (gannos, genv, dg') curl justStruct (buc, diag') uts

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

f0221ee7b9f8660e7c7add896e151f7a4ac8b4adChristian Maeder

d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian Maeder

b579e1a98aa30fb6093cbbdfeae51edbd5ba26adChristian Maeder-- | Analyse an unit term

c1bca76471ad22ac47f05b03576974762d364339Christian Maederana_UNIT_TERM :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic

d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian Maeder -> Bool -> ExtStUnitCtx -> UNIT_TERM

d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian Maeder -> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)

fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder

d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian Maeder-- UNIT-REDUCTION

d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian Maederana_UNIT_TERM lgraph defl gctx curl justStruct uctx red@(Unit_reduction ut restr) =

d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian Maeder do (p, diag, dg, ut') <- ana_UNIT_TERM lgraph defl gctx curl justStruct uctx (item ut)

f0221ee7b9f8660e7c7add896e151f7a4ac8b4adChristian Maeder (incl, msigma) <- ana_RESTRICTION dg (emptyG_sign curl) (getSig (getSigFromDiag p)) justStruct restr

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder let pos = getPos_UNIT_TERM red

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder (q, diag', dg') <- extendDiagramWithMorphismRev pos lgraph diag dg p incl

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder (renderText Nothing (printText red))

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder (case restr of

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder (Hidden _ _) -> DGHiding

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder (Revealed _ _) -> DGRevealing)

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder case msigma of

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder Nothing ->

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder -- the renaming morphism is just identity, so there's no need

c1bca76471ad22ac47f05b03576974762d364339Christian Maeder -- to extend the diagram

c1bca76471ad22ac47f05b03576974762d364339Christian Maeder do return (q, diag', dg', Unit_reduction (replaceAnnoted ut' ut) restr)

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder Just sigma ->

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder do (q'@(Diag_node_sig n _), diag'', dg'') <- extendDiagramWithMorphism pos lgraph diag' dg' q sigma

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder (renderText Nothing (printText red))

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder (case restr of

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder (Hidden _ _) -> DGHiding

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder (Revealed _ _) -> DGRevealing)

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder -- check amalgamability conditions

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder () <- assertAmalgamability pos diag'' (inn diag'' n)

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder return (q', diag'', dg'', Unit_reduction (replaceAnnoted ut' ut) restr)

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder-- UNIT-TRANSLATION

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maederana_UNIT_TERM lgraph defl gctx curl justStruct uctx tr@(Unit_translation ut ren) =

c1bca76471ad22ac47f05b03576974762d364339Christian Maeder do (dnsig, diag, dg, ut') <- ana_UNIT_TERM lgraph defl gctx curl justStruct uctx (item ut)

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder gMorph <- ana_RENAMING dg (getSig (getSigFromDiag dnsig)) justStruct ren

-- create an edge in the diagram that represents gMorph

let pos = getPos_UNIT_TERM tr

(dnsig'@(Diag_node_sig n _), diag', dg') <- extendDiagramWithMorphism pos lgraph diag dg dnsig gMorph

(renderText Nothing (printText tr))

DGTranslation

-- check amalamability conditions

() <- assertAmalgamability pos diag' (inn diag' n)

return (dnsig', diag', dg', Unit_translation (replaceAnnoted ut' ut) ren)

-- AMALGAMATION

ana_UNIT_TERM lgraph defl gctx curl justStruct uctx am@(Amalgamation uts poss) =

do (dnsigs, diag, dg', uts') <- ana_UNIT_TERMS lgraph defl gctx curl justStruct uctx uts

-- compute sigma

(sig, dg'') <- nodeSigUnion lgraph dg' (map getSigFromDiag dnsigs) DGUnion

(q@(Diag_node_sig n _), diag') <- extendDiagram lgraph diag dnsigs sig (renderText Nothing (printText am))

-- check amalgamability conditions

() <- assertAmalgamability (headPos poss) diag' (inn diag' n)

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

-- LOCAL-UNIT

ana_UNIT_TERM lgraph defl gctx@(gannos, genv, _) curl justStruct uctx (Local_unit udds ut poss) =

do (uctx', dg, udds') <- ana_UNIT_DECL_DEFNS' lgraph defl gctx curl justStruct uctx udds

(dnsig, diag, dg', ut') <- ana_UNIT_TERM lgraph defl (gannos, genv, dg) curl justStruct uctx' (item ut)

return (dnsig, diag, dg', Local_unit udds' (replaceAnnoted ut' ut) poss)

-- UNIT-APPL

ana_UNIT_TERM lgraph defl (gannos, genv, dg) curl justStruct uctx@(buc, diag)

uappl@(Unit_appl un fargus _) =

do let pos = getPos_UNIT_TERM uappl

case Map.lookup un buc of

Just (Based_unit_sig dnsig) ->

do case fargus of

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

_ -> -- arguments have been given for a parameterless unit

do plain_error (dnsig, diag, dg, uappl)

(showPretty un " is a parameterless unit, but arguments have been given: " ++

showPretty fargus "")

pos

Just (Based_par_unit_sig (pI, (argSigs, resultSig))) ->

do (sigF, dg') <- nodeSigUnion lgraph dg ((getSigFromDiag pI) : argSigs) DGFormalParams

(morphSigs, dg'', diagA) <- ana_FIT_ARG_UNITS lgraph defl (gannos, genv, dg') curl justStruct uctx

uappl pos argSigs fargus

let first (e, _, _) = e

second (_, e, _) = e

third (_, _, e) = e

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

((getSigFromDiag pI) : (map second morphSigs))

DGFitSpec

-- compute morphA (\sigma^A)

G_sign lidI sigI <- return (getSig (getSigFromDiag pI))

let idI = G_morphism lidI (ide lidI sigI)

morphA <- homogeneousMorManyUnion (idI : (map first morphSigs))

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

(_, sigMorExt) <- extendMorphism (getSig sigF) (getSig resultSig) (getSig sigA) morphA

(qB, diag') <- extendDiagram lgraph diagA [pI] resultSig ""

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

let ins diag dg [] = do return (diag, dg)

ins diag dg ((morph, _, targetNode) : morphNodes) =

do (dnsig, diag', dg') <- extendDiagramWithMorphismRev pos lgraph diag

dg targetNode (gEmbed morph)

(renderText Nothing (printText fargus))

DGFormalParams

diag'' <- insInclusionEdges lgraph diag' [dnsig] qB

ins diag'' dg' morphNodes

(diag'', dg4) <- ins diag' dg''' morphSigs

(q@(Diag_node_sig n _), diag''', dg5) <- extendDiagramWithMorphism pos lgraph diag'' dg4 qB (gEmbed sigMorExt)

(renderText Nothing (printText uappl))

DGExtension

diag4 <- insInclusionEdges lgraph diag''' (map third morphSigs) q

-- check amalgamability conditions

() <- assertAmalgamability pos diag4 (inn diag4 n)

return (q, diag4, dg5, uappl)

Nothing -> plain_error (emptyDiagNodeSig defl, diag, dg, uappl)

("Undefined unit " ++ showPretty un "")

pos

-- group unit term

ana_UNIT_TERM lgraph defl gctx curl justStruct uctx (Group_unit_term ut poss) =

do (dnsig, diag, dg, ut') <- ana_UNIT_TERM lgraph defl gctx curl justStruct uctx (item ut)

return (dnsig, diag, dg, Group_unit_term (replaceAnnoted ut' ut) poss)

-- | Analyse unit arguments

ana_FIT_ARG_UNITS :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic

-> Bool -> ExtStUnitCtx

-> UNIT_TERM -- ^ the whole application for diagnostic purposes

-> Pos -- ^ 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)

ana_FIT_ARG_UNITS _ _ (_, _, dg) _ _ (_, diag) _ _ [] [] =

do return ([], dg, diag)

ana_FIT_ARG_UNITS lgraph defl gctx@(gannos, genv, _) curl justStruct uctx@(buc, _)

appl pos (nsig : nsigs) (fau : faus) =

do (gmorph, nsig', dnsig, dg, diag) <- ana_FIT_ARG_UNIT lgraph defl gctx curl justStruct

uctx nsig fau

(morphSigs, dg', diag') <- ana_FIT_ARG_UNITS lgraph defl (gannos, genv, dg) curl justStruct

(buc, diag) appl pos nsigs faus

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

ana_FIT_ARG_UNITS _ _ (_, _, dg) _ _ (_, diag) appl pos [] _ =

do plain_error ([], dg, diag)

("Too many arguments given in application\n" ++ showPretty appl "")

pos

ana_FIT_ARG_UNITS _ _ (_, _, dg) _ _ (_, diag) appl pos _ [] =

do plain_error ([], dg, diag)

("Too few arguments given in application\n" ++ showPretty appl "")

pos

-- | Analyse unit argument

ana_FIT_ARG_UNIT :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic

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

ana_FIT_ARG_UNIT lgraph defl gctx curl justStruct uctx nsig (Fit_arg_unit ut symbMap poss) =

do (p, diag', dg', _) <- ana_UNIT_TERM lgraph defl gctx curl justStruct uctx (item ut)

-- compute gMorph (the morphism r|sigma/D(p))

let adj = adjustPos (headPos poss)

gsigmaS = getSig nsig

gsigmaT = getSig (getSigFromDiag p)

G_sign lidS sigmaS <- return gsigmaS

G_sign lidT sigmaT <- return gsigmaT

G_symb_map_items_list lid sis <- return symbMap

sigmaT' <- rcoerce lidT lidS (headPos poss) sigmaT

mor <- if justStruct then return (ide lidS sigmaS)

else do rmap <- adj $ stat_symb_map_items lid sis

rmap' <- rcoerce lid lidS (headPos poss) rmap

adj $ induced_from_to_morphism lidS rmap' sigmaS sigmaT'

let gMorph = G_morphism lidS mor

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

return (gMorph, nsig', p, dg'', diag')

-- | Analyse unit specification

ana_UNIT_SPEC :: LogicGraph -> AnyLogic -- ^ the default logic

-> GlobalContext -> AnyLogic -- ^ current logic

-> Bool -- ^ should only the structure be analysed?

-> NodeSig -- ^ the signature of imports

-> UNIT_SPEC -> Result (UnitSig, 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.

-- UNIT-TYPE

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

should be converted to a Spec_name -}

ana_UNIT_SPEC lgraph defl gctx@(_, genv, _) curl just_struct

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

| case Map.lookup spn genv of Just (UnitEntry _) -> True

_ -> False =

ana_UNIT_SPEC lgraph defl gctx curl just_struct impsig (Spec_name spn)

-- a trivial unit type

ana_UNIT_SPEC lgraph _ gctx _ just_struct impsig (Unit_type [] resultSpec poss) =

do (resultSpec', resultSig, dg') <- ana_SPEC lgraph gctx impsig Nothing

just_struct (item resultSpec)

return (Unit_sig resultSig, dg', Unit_type [] (replaceAnnoted resultSpec' resultSpec) poss)

-- a non-trivial unit type

ana_UNIT_SPEC lgraph defl gctx@(gannos, genv, _) _ justStruct impSig (Unit_type argSpecs resultSpec poss) =

do (argSigs, dg1, argSpecs') <- ana_argSpecs lgraph defl gctx justStruct argSpecs

(sigUnion, dg2) <- nodeSigUnion lgraph dg1 (impSig : argSigs) DGFormalParams

(resultSpec', resultSig, dg3) <- ana_SPEC lgraph (gannos, genv, dg2) sigUnion

Nothing justStruct (item resultSpec)

return (Par_unit_sig (argSigs, resultSig), dg3,

Unit_type argSpecs' (replaceAnnoted resultSpec' resultSpec) poss)

-- SPEC-NAME (an alias)

ana_UNIT_SPEC _ _ (_, genv, dg) _ _ impsig usp@(Spec_name usn@(Token _ pos)) =

do case Map.lookup usn genv of

Nothing -> plain_error (Unit_sig impsig, dg, usp)

("Undefined unit specification " ++ showPretty usn "")

pos

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

_ -> plain_error (Unit_sig impsig, dg, usp)

((showPretty usn "") ++ " is not an unit specification")

pos

-- ARCH-UNIT-SPEC

ana_UNIT_SPEC lgraph defl gctx curl just_struct _ (Arch_unit_spec asp poss) =

do ((_, usig), dg', asp') <- ana_ARCH_SPEC lgraph defl gctx curl just_struct (item asp)

return (usig, dg', Arch_unit_spec (replaceAnnoted asp' asp) poss)

-- CLOSED-UNIT-SPEC

ana_UNIT_SPEC lgraph defl gctx curl just_struct _ (Closed_unit_spec usp' _) =

ana_UNIT_SPEC lgraph defl gctx curl just_struct (EmptyNode curl) usp'

-- | Analyse a list of argument specifications

ana_argSpecs :: LogicGraph -> AnyLogic -> GlobalContext -> Bool -> [Annoted SPEC]

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

ana_argSpecs _ _ (_, _, dg) _ [] =

do return ([], dg, [])

ana_argSpecs lgraph defl gctx@(gannos, genv, _) justStruct (argSpec : argSpecs) =

do (argSpec', argSig, dg') <- ana_SPEC lgraph gctx (EmptyNode defl) Nothing

justStruct (item argSpec)

(argSigs, dg'', argSpecs') <- ana_argSpecs lgraph defl (gannos, genv, dg') justStruct argSpecs

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

-- | Check that given diagram ensures amalgamability along given set of morphisms

assertAmalgamability :: Pos -- ^ the position (for diagnostics)

-> Diag -- ^ the diagram to be checked

-> [LEdge DiagLinkLab] -- ^ the sink

-> Result ()

assertAmalgamability pos diag sink =

do ensAmalg <- homogeneousEnsuresAmalgamability pos diag sink

case ensAmalg of

Yes -> return ()

No msg -> plain_error () ("Amalgamability is not ensured: " ++ msg) pos

DontKnow -> warning () "Unable to assert that amalgamability is ensured" pos

-- | Check the amalgamability assuming common logic for whole diagram

homogeneousEnsuresAmalgamability :: Pos -- ^ the position (for diagnostics)

-> Diag -- ^ the diagram to be checked

-> [LEdge DiagLinkLab] -- ^ the sink

-> Result Amalgamates

homogeneousEnsuresAmalgamability pos diag sink =

do case sink of

[] -> plain_error DontKnow "homogeneousEnsuresAmalgamability: Empty sink" pos

lab:_ -> do let (_,_,edgeLab) = lab

sig = cod Grothendieck (dl_morphism edgeLab)

G_sign lid _ <- return sig

hDiag <- homogeniseDiagram lid diag

hSink <- homogeniseEdges lid sink

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

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

getPos_UNIT_TERM :: UNIT_TERM

-> Pos

-- UNIT-REDUCTION

getPos_UNIT_TERM (Unit_reduction _ restr) =

-- obtain position from RESTRICTION

case restr of

(Hidden _ poss) -> headPos poss

(Revealed _ poss) -> headPos poss

-- UNIT-TRANSLATION

getPos_UNIT_TERM (Unit_translation _ (Renaming _ poss)) =

headPos poss

-- AMALGAMATION

getPos_UNIT_TERM (Amalgamation _ poss) =

headPos poss

-- LOCAL-UNIT

getPos_UNIT_TERM (Local_unit _ _ poss) =

headPos poss

-- UNIT-APPLICATION

getPos_UNIT_TERM (Unit_appl (Token _ unpos) _ _) =

unpos

-- GROUP-UNIT-TERM

getPos_UNIT_TERM (Group_unit_term _ poss) =

headPos poss

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

getPos_UNIT_IMPORTED :: [Pos]

-> Pos

getPos_UNIT_IMPORTED (_ : (pos : _)) = pos

getPos_UNIT_IMPORTED _ = nullPos

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

getPos_UNIT_EXPRESSION :: UNIT_EXPRESSION

-> Pos

getPos_UNIT_EXPRESSION (Unit_expression _ (Annoted ut _ _ _) []) =

getPos_UNIT_TERM ut

getPos_UNIT_EXPRESSION (Unit_expression _ _ poss) =

headPos poss