AnalysisArchitecture.hs revision ad270004874ce1d0697fb30d7309f180553bb315
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederModule : $Header$
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederDescription : static analysis of CASL architectural specifications
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederCopyright : (c) Maciek Makowski, Warsaw University, C. Maeder 2004-2006
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederMaintainer : till@tzi.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : non-portable (via imports)
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederStatic analysis of CASL architectural specifications
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Follows the extended static semantics sketched in Chap. III:5.6
d8c71aacc9f1c8cd40a8ad8dcdad9be8854b849fChristian Maeder of the CASL Reference Manual.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -- EmptyNode undefined should be replaced with local env!
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettichmodule Static.AnalysisArchitecture (ana_ARCH_SPEC, ana_UNIT_SPEC)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederimport qualified Data.Map as Map
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederimport Data.Graph.Inductive.Graph as Graph(Node)
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder-- | Analyse an architectural specification
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder-- ARCH-SPEC ::= BASIC-ARCH-SPEC | GROUP-ARCH-SPEC | ARCH-SPEC-NAME
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettichana_ARCH_SPEC :: LogicGraph -> AnyLogic -- ^ the default logic
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder -> GlobalContext -> AnyLogic -- ^ current logic
4cb215739e9ab13447fa21162482ebe485b47455Christian Maeder -> HetcatsOpts -- ^ should only the structure be analysed?
8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maeder -> ARCH_SPEC -> Result (ArchSig, GlobalContext, ARCH_SPEC)
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich{- ^ returns 1. the architectural signature of given ARCH-SPEC
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder2. development graph resulting from structured specs within the arch
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maederspec and 3. ARCH_SPEC after possible conversions -}
55adfe57a4de1f36adc3e3bfc16f342e44a7d444Christian Maeder-- BASIC-ARCH-SPEC
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederana_ARCH_SPEC lgraph defl gctx curl opts (Basic_arch_spec udd uexpr pos) =
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder do (uctx, dg', udd') <- ana_UNIT_DECL_DEFNS lgraph defl gctx curl opts udd
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder (_, usig, _, dg'', uexpr') <- ana_UNIT_EXPRESSION lgraph defl
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder dg' curl opts uctx (item uexpr)
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder return (ArchSig (ctx uctx) usig, dg'', Basic_arch_spec udd'
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (replaceAnnoted uexpr' uexpr) pos)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- GROUP-ARCH-SPEC
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maederana_ARCH_SPEC lgraph defl gctx curl opts (Group_arch_spec asp _) =
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder ana_ARCH_SPEC lgraph defl gctx curl opts (item asp)
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder-- ARCH-SPEC-NAME
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maederana_ARCH_SPEC _ _ gctx _ _ asp@(Arch_spec_name asn@(Token astr pos)) =
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder do case Map.lookup asn $ globalEnv gctx of
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder Nothing -> fatal_error ("Undefined architectural specification "
c3053d57f642ca507cdf79512e604437c4546cb9Christian Maeder Just (ArchEntry asig) -> return (asig, gctx, asp)
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder _ -> fatal_error (astr ++
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder " is not an architectural specification") pos
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder-- | Analyse a list of unit declarations and definitions
c2fcc35abb03cf0b4ca4b050efeb10827f38c322Christian Maederana_UNIT_DECL_DEFNS :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder -> HetcatsOpts -> [Annoted UNIT_DECL_DEFN]
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder -> Result (ExtStUnitCtx, GlobalContext, [Annoted UNIT_DECL_DEFN])
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder{- ^ returns 1. extended static unit context 2. possibly modified
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maederdevelopment graph 3. possibly modified list of unit declarations and
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maederdefinitions -}
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maederana_UNIT_DECL_DEFNS lgraph defl gctx curl opts udds =
0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder ana_UNIT_DECL_DEFNS' lgraph defl gctx curl opts emptyExtStUnitCtx udds
c2a4d8ae266aa37cc922eba97077520229a19902Christian Maederana_UNIT_DECL_DEFNS' :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic
757e6c79ec40491d45dc72c82b5eb59a386634b0Jian Chun Wang -> HetcatsOpts -> ExtStUnitCtx -> [Annoted UNIT_DECL_DEFN]
757e6c79ec40491d45dc72c82b5eb59a386634b0Jian Chun Wang -> Result (ExtStUnitCtx, GlobalContext, [Annoted UNIT_DECL_DEFN])
757e6c79ec40491d45dc72c82b5eb59a386634b0Jian Chun Wangana_UNIT_DECL_DEFNS' _ _ gctx _ _ uctx [] =
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder do return (uctx, gctx, [])
c6fcd42c6d6d9dae8c7835c24fcb7ce8531a9050Christian Maederana_UNIT_DECL_DEFNS' lgraph defl gctx curl opts uctx (udd : udds) =
31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till Mossakowski do (uctx', dg', udd') <- ana_UNIT_DECL_DEFN lgraph defl
c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus Luettich gctx curl opts uctx (item udd)
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich (uctx'', dg'', udds') <- ana_UNIT_DECL_DEFNS' lgraph defl
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich dg' curl opts uctx' udds
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder return (uctx'', dg'', (replaceAnnoted udd' udd) : udds')
8cacad2a09782249243b80985f28e9387019fe40Christian MaederalreadyDefinedUnit :: SIMPLE_ID -> String
363939beade943a02b31004cea09dec34fa8a6d9Christian MaederalreadyDefinedUnit u = "Unit " ++ tokStr u ++ " already declared/defined"
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder-- | Analyse unit refs
8a28707e9155465c6f2236a06eac6580a65c7025Christian Maederana_UNIT_REF :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic
df35538fec1d9135602308d577255c0d466b6365Christian Maeder -> HetcatsOpts -> ExtStUnitCtx -> UNIT_REF
df35538fec1d9135602308d577255c0d466b6365Christian Maeder -> Result (ExtStUnitCtx, GlobalContext, UNIT_REF)
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder{- ^ returns 1. extended static unit context 2. possibly modified
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederdevelopment graph 3. possibly modified UNIT_DECL_DEFN -}
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder-- unit declaration
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederana_UNIT_REF lgraph defl gctx curl opts
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder uctx@(buc, _) (Unit_ref un@(Token ustr unpos) usp pos) =
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder do (dns, diag', dg', _) <- ana_UNIT_IMPORTED lgraph defl
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder gctx curl opts uctx pos []
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder let impSig = toMaybeNode dns
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (usig, gctx'', usp') <- ana_REF_SPEC lgraph defl dg'
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder curl opts impSig usp
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder let ud' = Unit_ref un usp' pos
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder dg'' = devGraph gctx''
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder plain_error (uctx, gctx'', ud') (alreadyDefinedUnit un) unpos
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder Par_unit_sig argSigs resultSig ->
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder do (resultSig', dg''') <- nodeSigUnion lgraph dg''
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder (JustNode resultSig : [impSig]) DGImports
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder let basedParUSig = Based_par_unit_sig dns $
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Par_unit_sig argSigs resultSig'
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder return ((Map.insert un basedParUSig buc, diag'),
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder gctx'' { devGraph = dg''' }, ud')
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Unit_sig nsig ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder do (nsig', dg''') <- nodeSigUnion lgraph dg''
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (impSig : [JustNode nsig]) DGImports
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (dn', diag'') <- extendDiagramIncl lgraph diag' []
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder return ((Map.insert un (Based_unit_sig dn') buc, diag'')
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , gctx'' { devGraph = dg''' }, ud')
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- | Analyse unit declaration or definition
0769e2a25732dc2544b2a7425dfa284e24d23b71Christian Maederana_UNIT_DECL_DEFN :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> HetcatsOpts -> ExtStUnitCtx -> UNIT_DECL_DEFN
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder -> Result (ExtStUnitCtx, GlobalContext, UNIT_DECL_DEFN)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder{- ^ returns 1. extended static unit context 2. possibly modified
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederdevelopment graph 3. possibly modified UNIT_DECL_DEFN -}
ad4889ebb40efae8595b0969dd6ba1162d52bac3Christian Maeder-- unit declaration
4017ebc0f692820736d796af3110c3b3018c108aChristian Maederana_UNIT_DECL_DEFN lgraph defl gctx curl opts uctx@(buc, _)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (Unit_decl un@(Token ustr unpos) usp uts pos) =
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder do (dns, diag', dg', uts') <- ana_UNIT_IMPORTED lgraph defl
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder gctx curl opts uctx pos uts
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder let impSig = toMaybeNode dns
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (usig, gctx'', usp') <- ana_REF_SPEC lgraph defl
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder dg' curl opts impSig usp
a9b59eb2ce961014974276cdae0e9df4419bd212Christian Maeder let ud' = Unit_decl un usp' uts' pos
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder dg'' = devGraph gctx''
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder plain_error (uctx, gctx'', ud') (alreadyDefinedUnit un) unpos
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder Par_unit_sig argSigs resultSig ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder do (resultSig', dg''') <- nodeSigUnion lgraph dg''
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (JustNode resultSig : [impSig]) DGImports
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let basedParUSig = Based_par_unit_sig dns $
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder Par_unit_sig argSigs resultSig'
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder return ((Map.insert un basedParUSig buc, diag'),
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder gctx'' { devGraph = dg''' }, ud')
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Unit_sig nsig ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder do (nsig', dg''') <- nodeSigUnion lgraph dg''
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (impSig : [JustNode nsig]) DGImports
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (dn', diag'') <- extendDiagramIncl lgraph diag'
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder JustDiagNode dn -> [dn]
b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder _ -> []) nsig' ustr
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder return ((Map.insert un (Based_unit_sig dn') buc, diag'')
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich , gctx'' { devGraph = dg''' }, ud')
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder-- unit definition
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederana_UNIT_DECL_DEFN lgraph defl gctx curl opts uctx@(buc, _)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (Unit_defn un uexp poss) =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder do (p, usig, diag, dg', uexp') <- ana_UNIT_EXPRESSION lgraph defl
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder gctx curl opts uctx uexp
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder let ud' = Unit_defn un uexp' poss
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder {- it's sufficient to check that un is not mapped in buc, we
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder don't need to convert the ExtStUnitCtx to StUnitCtx as the
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder domain will be preserved -}
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder plain_error (uctx, dg', ud') (alreadyDefinedUnit un) $ tokPos un
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder {- we can use Map.insert as there are no mappings for
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder un in ps and bs (otherwise there would have been a
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder mapping in (ctx uctx)) -}
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Unit_sig _ -> case p of
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder JustDiagNode dn -> return ((Map.insert un
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (Based_unit_sig dn) buc, diag), dg', ud')
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder _ -> error "ana_UNIT_DECL_DEFN"
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Par_unit_sig _ _ -> return ((Map.insert un
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder (Based_par_unit_sig p usig) buc
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder , diag), dg', ud')
89f7631cbfbd1bb99fc152b434bd362a7799d295Christian Maeder-- | Analyse unit imports
363939beade943a02b31004cea09dec34fa8a6d9Christian Maederana_UNIT_IMPORTED :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder -> HetcatsOpts -> ExtStUnitCtx -> Range -> [Annoted UNIT_TERM]
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder -> Result (MaybeDiagNode, Diag, GlobalContext, [Annoted UNIT_TERM])
363939beade943a02b31004cea09dec34fa8a6d9Christian Maederana_UNIT_IMPORTED _ _ gctx curl _ (_, diag) _ [] =
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder do return (EmptyDiagNode curl, diag, gctx, [])
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettichana_UNIT_IMPORTED lgraph defl gctx curl opts uctx poss terms =
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder do (dnsigs, diag', gctx', terms') <- ana_UNIT_IMPORTED' lgraph defl
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder gctx curl opts uctx terms
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich let dg' = devGraph gctx'
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder (sig, dg'') <- nodeSigUnion lgraph dg'
6b6773cf587b74259178641d811746a235faf056Christian Maeder (map (JustNode . getSigFromDiag) dnsigs) DGImports
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -- check amalgamability conditions
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder {- let incl s = propagateErrors (ginclusion lgraph (getSig
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich (getSigFromDiag s)) (getSig sig)) -}
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let pos = getPos_UNIT_IMPORTED poss
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder sink <- inclusionSink lgraph dnsigs sig
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder () <- assertAmalgamability opts pos diag' sink
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (dnsig, diag'') <- extendDiagramIncl lgraph diag' dnsigs
01b16c4bdd2a3577214f79a64aed02f54e8a204eChristian Maeder sig $ showDoc terms ""
7c5c311d67e187280877c45bd89dcba9038bc0a3Christian Maeder return (JustDiagNode dnsig, diag'', gctx' { devGraph = dg'' }, terms')
7c5c311d67e187280877c45bd89dcba9038bc0a3Christian Maederana_UNIT_IMPORTED' :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic
7c5c311d67e187280877c45bd89dcba9038bc0a3Christian Maeder -> HetcatsOpts -> ExtStUnitCtx -> [Annoted UNIT_TERM]
7c5c311d67e187280877c45bd89dcba9038bc0a3Christian Maeder -> Result ([DiagNodeSig], Diag, GlobalContext, [Annoted UNIT_TERM])
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederana_UNIT_IMPORTED' _ _ gctx _ _ (_, diag) [] =
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder do return ([], diag, gctx, [])
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederana_UNIT_IMPORTED' lgraph defl gctx curl opts uctx@(buc, _) (ut : uts) =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder do (dnsig, diag', dg', ut') <- ana_UNIT_TERM lgraph defl
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder gctx curl opts uctx (item ut)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (dnsigs, diag'', dg'', uts') <- ana_UNIT_IMPORTED' lgraph defl
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder dg' curl opts (buc, diag') uts
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder return (dnsig : dnsigs, diag'', dg'', (replaceAnnoted ut' ut) : uts')
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | Analyse an unit expression
9df11f85fd7f8c4745d64464876e84ec4e263692Christian Maederana_UNIT_EXPRESSION :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers -> HetcatsOpts -> ExtStUnitCtx -> UNIT_EXPRESSION
010c56c4cf12dd7977ca36efe85219b91e265ee3Christian Maeder -> Result (MaybeDiagNode, UnitSig, Diag, GlobalContext, UNIT_EXPRESSION)
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettichana_UNIT_EXPRESSION lgraph defl gctx curl opts uctx
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski (Unit_expression [] ut poss) =
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder do (dnsig@(Diag_node_sig _ ns'), diag', dg', ut') <-
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers ana_UNIT_TERM lgraph defl gctx curl opts uctx (item ut)
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder return (JustDiagNode dnsig, Unit_sig ns', diag', dg',
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Unit_expression [] (replaceAnnoted ut' ut) poss)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederana_UNIT_EXPRESSION lgraph defl gctx curl opts
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder uctx@(buc, diag) uexp@(Unit_expression ubs ut poss) =
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers do (args, gctx', ubs') <- ana_UNIT_BINDINGS lgraph defl
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder gctx curl opts uctx ubs
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (resnsig, _dg'') <- nodeSigUnion lgraph (devGraph gctx')
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder (map (JustNode . snd) args) DGFormalParams
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder -- build the extended diagram and new based unit context
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder let dexp = showDoc uexp ""
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder insNodes diag0 [] buc0 = do return ([], diag0, buc0)
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder insNodes diag0 ((un, nsig) : args0) buc0 =
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder do (dnsig, diag') <- extendDiagramIncl lgraph diag0 []
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder {- we made sure in ana_UNIT_BINDINGS that there's no
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder mapping for un in buc so we can just use
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder let buc' = Map.insert un (Based_unit_sig dnsig) buc0
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder (dnsigs, diag'', buc'') <- insNodes diag' args0 buc'
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder return (dnsig : dnsigs, diag'', buc'')
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder (pardnsigs, diag', buc') <- insNodes diag args buc
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder (_, diag'') <- extendDiagramIncl lgraph diag' pardnsigs
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder -- analyse the unit term
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder (p@(Diag_node_sig _ pnsig), diag''', dg''', ut') <-
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder ana_UNIT_TERM lgraph defl
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder gctx' curl opts (buc', diag'') (item ut)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder -- check amalgamability conditions
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder let pos = getPos_UNIT_EXPRESSION uexp
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder checkSubSign [] _ = True
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder checkSubSign (dnsub : dnsigs) nsup =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder if isSubGsign lgraph (getSig $ getSigFromDiag dnsub) $ getSig nsup
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder then checkSubSign dnsigs nsup else False
ac34194a668399bb8ef238da77c3a09e93fb253bChristian Maeder -- check that signatures in pardnsigs are subsignatures of pnsig
ac34194a668399bb8ef238da77c3a09e93fb253bChristian Maeder if checkSubSign pardnsigs pnsig
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder do sink <- inclusionSink lgraph (p : pardnsigs) pnsig
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder () <- assertAmalgamability opts pos diag''' sink
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder -- add new node to the diagram
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder return (EmptyDiagNode curl, Par_unit_sig (map snd args) pnsig,
6fe9628743562678acf97d6730ebcfee5e9e50c2Christian Maeder diag''', dg''',
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder Unit_expression ubs' (replaceAnnoted ut' ut) poss)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder else -- report an error
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski ("The body signature does not extend the parameter signatures in\n"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder{- | Analyse a list of unit bindings. Ensures that the unit names are
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maedernot present in extended static unit context and that there are no
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettichduplicates among them. -}
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettichana_UNIT_BINDINGS :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic
e96a0bf4040fd789339958c01f145c5057d26db6René Wagner -> HetcatsOpts -> ExtStUnitCtx -> [UNIT_BINDING]
e96a0bf4040fd789339958c01f145c5057d26db6René Wagner -> Result ([(SIMPLE_ID, NodeSig)], GlobalContext, [UNIT_BINDING])
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettichana_UNIT_BINDINGS _ _ gctx _ _ _ [] =
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich do return ([], gctx, [])
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maederana_UNIT_BINDINGS lgraph defl gctx curl opts uctx@(buc, _)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder ((Unit_binding un@(Token ustr unpos) usp poss) : ubs) =
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder do (usig, dg', usp') <- ana_UNIT_SPEC lgraph defl
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers gctx curl opts (EmptyNode curl) usp
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder let ub' = Unit_binding un usp' poss
b9b960bc75e34658e70c4a0231dbc6a6e7373f2dChristian Maeder Par_unit_sig _ _ -> plain_error ([], dg', [])
18a4d5cb6828f080db9c5f9551785c5151027271Christian Maeder ("An argument unit " ++
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich ustr ++ " must not be parameterized") unpos
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder Unit_sig nsig ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder do (args, dg'', ubs') <- ana_UNIT_BINDINGS lgraph defl
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski dg' curl opts uctx ubs
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder let args' = (un, nsig) : args
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski then plain_error (args', dg'', ub' : ubs')
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder (alreadyDefinedUnit un) unpos
c9acb8681bcc512245b4f0d1a9f2b189c60e10d4Christian Maeder case lookup un args of
38352346eb1a67ba0f4eab8ad6f718528cf0cde0Christian Maeder Just _ -> plain_error (args', dg'', ub' : ubs')
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder (alreadyDefinedUnit un) unpos
63e50b4c36074d5fb9de872c4007b688b4bce534Christian Maeder Nothing -> return (args', dg'', ub' : ubs')
bd54a9917cd87169b8e40bcc5616c537fed85815Christian Maeder-- | Analyse a list of unit terms
11b55e6fbbc397b9fa41a7d61be53c6f4f027824Christian Maederana_UNIT_TERMS :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic
7dfbfdd1c4175dc0f640b1731a70854526c0e5c6Christian Maeder -> HetcatsOpts -> ExtStUnitCtx -> [Annoted UNIT_TERM]
11b55e6fbbc397b9fa41a7d61be53c6f4f027824Christian Maeder -> Result ([DiagNodeSig], Diag, GlobalContext, [Annoted UNIT_TERM])
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederana_UNIT_TERMS _ _ gctx _ _ (_, diag) [] =
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder do return ([], diag, gctx, [])
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederana_UNIT_TERMS lgraph defl gctx curl opts uctx@(buc, _) (ut : uts) =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder do (dnsig, diag', dg', ut') <- ana_UNIT_TERM lgraph defl
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder gctx curl opts uctx (item ut)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (dnsigs, diag'', dg'', uts') <- ana_UNIT_TERMS lgraph defl
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder dg' curl opts (buc, diag') uts
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return (dnsig : dnsigs, diag'', dg'', (replaceAnnoted ut' ut) : uts')
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | Analyse an unit term
6bf24e5eb644064ad650eb3fd9774483fccbf601Christian Maederana_UNIT_TERM :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> HetcatsOpts -> ExtStUnitCtx -> UNIT_TERM
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> Result (DiagNodeSig, Diag, GlobalContext, UNIT_TERM)
e8db9a65830cf71504e33c6f441a67b4d184a3caChristian Maeder-- UNIT-REDUCTION
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederana_UNIT_TERM lgraph defl gctx curl opts uctx red@(Unit_reduction ut restr) =
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder do (p, diag, gctx1, ut') <- ana_UNIT_TERM lgraph defl
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder gctx curl opts uctx (item ut)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder let dg = devGraph gctx1
6bf24e5eb644064ad650eb3fd9774483fccbf601Christian Maeder (incl, msigma) <- ana_RESTRICTION dg (emptyG_sign curl)
dbe752ee940baae7f9f231f29c62284bb0f90a25Christian Maeder (getSig (getSigFromDiag p)) opts restr
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke let pos = getPos_UNIT_TERM red
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (q@(Diag_node_sig qn _), diag', dg') <-
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke extendDiagramWithMorphismRev pos lgraph diag dg p incl
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (showDoc red "")
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke (case restr of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Hidden _ _ -> DGHiding
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Revealed _ _ -> DGRevealing)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder case msigma of
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder {- the renaming morphism is just identity, so
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder there's no need to extend the diagram -}
f443a57f2a8e0ca3daa7431b0c89a18ba52c337aChristian Maeder do return (q, diag', gctx1 { devGraph = dg' },
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder Unit_reduction (replaceAnnoted ut' ut) restr)
1f63599faaa311cd024d6413f82bff8caae8de24Christian Maeder Just sigma ->
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski -- check amalgamability conditions
7c99e334446bb97120e30e967baeeddfdd1278deKlaus Luettich let sink = [(qn, sigma)]
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder () <- assertAmalgamability opts pos diag' sink
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder (q', diag'', dg'') <- extendDiagramWithMorphism pos
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder lgraph diag' dg' q sigma
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder (showDoc red "")
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder (case restr of
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder Hidden _ _ -> DGHiding
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder Revealed _ _ -> DGRevealing)
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder return (q', diag'', gctx1 { devGraph = dg'' },
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder Unit_reduction
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder (replaceAnnoted ut' ut) restr)
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder-- UNIT-TRANSLATION
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederana_UNIT_TERM lgraph defl gctx curl opts uctx tr@(Unit_translation ut ren) =
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder do (dnsig@(Diag_node_sig p _), diag, gctx1, ut') <- ana_UNIT_TERM lgraph
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder defl gctx curl opts uctx (item ut)
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder -- EmptyNode undefined should be replaced with local env!
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder gMorph <- ana_RENAMING lgraph (EmptyNode $ error "Static.AnalysisArchitecture")
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder (getSig (getSigFromDiag dnsig)) opts ren
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder let pos = getPos_UNIT_TERM tr
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder sink = [(p, gMorph)]
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder dg = devGraph gctx1
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder -- check amalamability conditions
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder () <- assertAmalgamability opts pos diag sink
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder (dnsig', diag', dg') <- extendDiagramWithMorphism pos lgraph
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder diag dg dnsig gMorph (showDoc tr "")
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder DGTranslation
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder return (dnsig', diag', gctx1 { devGraph = dg' }, Unit_translation
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder (replaceAnnoted ut' ut) ren)
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder-- AMALGAMATION
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederana_UNIT_TERM lgraph defl gctx curl opts uctx am@(Amalgamation uts poss) =
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder do (dnsigs, diag, gctx', uts') <- ana_UNIT_TERMS lgraph defl
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder gctx curl opts uctx uts
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder let dg' = devGraph gctx'
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder -- compute sigma
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder (sig, dg'') <- nodeSigUnion lgraph dg'
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder (map (JustNode . getSigFromDiag) dnsigs) DGUnion
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder -- check amalgamability conditions
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder sink <- inclusionSink lgraph dnsigs sig
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder () <- assertAmalgamability opts poss diag sink
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder (q, diag') <- extendDiagramIncl lgraph diag dnsigs
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder sig $ showDoc am ""
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder return (q, diag', gctx' { devGraph = dg'' }, Amalgamation uts' poss)
4017ebc0f692820736d796af3110c3b3018c108aChristian Maederana_UNIT_TERM lgraph defl gctx curl opts uctx (Local_unit udds ut poss) =
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder do (uctx', dg, udds') <- ana_UNIT_DECL_DEFNS' lgraph defl
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder gctx curl opts uctx udds
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian Maeder (dnsig, diag, dg', ut') <- ana_UNIT_TERM lgraph defl
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder dg curl opts uctx' (item ut)
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder return (dnsig, diag, dg', Local_unit udds' (replaceAnnoted ut' ut) poss)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederana_UNIT_TERM lgraph defl gctx curl opts uctx@(buc, diag)
0c355dd0b739631ee472f9a656e266be27fa4e64Christian Maeder uappl@(Unit_appl un fargus _) =
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder do let pos = getPos_UNIT_TERM uappl
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maeder dg = devGraph gctx
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder ustr = tokStr un
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder Just (Based_unit_sig dnsig) ->
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder do case fargus of
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder [] -> return (dnsig, diag, gctx, uappl)
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich -- arguments have been given for a parameterless unit
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich do plain_error (dnsig, diag, gctx, uappl)
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich (ustr ++ " is a parameterless unit, "
c7ec85d1103173e089aa5048fd7afb2f9b505124Klaus Luettich ++ "but arguments have been given: " ++
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich showDoc fargus "") pos
a883cd4d01fe39d23219cf5333425f195be24d8bChristian Maeder Just (Based_par_unit_sig pI (Par_unit_sig argSigs resultSig)) ->
5c69cef4668bbd959d721668313a779126014d1eKlaus Luettich do (sigF, dg') <- nodeSigUnion lgraph dg
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich (toMaybeNode pI : map JustNode argSigs) DGFormalParams
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich (morphSigs, gctx'', diagA) <- ana_FIT_ARG_UNITS lgraph defl
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich gctx { devGraph = dg' } curl opts
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich uctx uappl pos argSigs fargus
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich let first (e, _, _) = e
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich second (_, e, _) = e
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich third (_, _, e) = e
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich dg'' = devGraph gctx''
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich (sigA, dg''') <- nodeSigUnion lgraph dg''
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich (toMaybeNode pI : (map (JustNode . second) morphSigs))
c4ef79587a902327f36277c45a8d91d1e67bd6d5Klaus Luettich -- compute morphA (\sigma^A)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder G_sign lidI sigI _ <- return (getMaybeSig (toMaybeNode pI))
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich let idI = G_morphism lidI (ide lidI sigI) 0
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich morphA <- homogeneousMorManyUnion
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich (idI : (map first morphSigs))
b905126bab9454b89041f92b3c50bb9efc85e427Klaus Luettich -- compute sigMorExt (\sigma^A(\Delta))
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (_, sigMorExt) <- extendMorphism (getSig sigF)
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian Maeder (getSig resultSig) (getSig sigA) morphA
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -- check amalgamability conditions
dbe752ee940baae7f9f231f29c62284bb0f90a25Christian Maeder let pIL = case pI of
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder JustDiagNode dn -> [dn]
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder sink <- inclusionSink lgraph (pIL ++
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder map third morphSigs) sigA
68aab98a58d1460c77a1573a86c32a891756a420Christian Maeder () <- assertAmalgamability opts pos diagA sink
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder (qB@(Diag_node_sig nqB _), diag') <-
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder extendDiagramIncl lgraph diagA pIL resultSig ""
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder -- insert nodes p^F_i and appropriate edges to the diagram
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder let ins diag0 dg0 [] = do return (diag0, dg0)
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder ins diag0 dg0 ((morph, _, targetNode) : morphNodes) =
3a7788e09dd23b364a46c9488cbd1522369113dbChristian Maeder do (dnsig, diag1, dg1) <-
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder extendDiagramWithMorphismRev pos lgraph diag0
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich dg0 targetNode (gEmbed morph)
dbe752ee940baae7f9f231f29c62284bb0f90a25Christian Maeder (showDoc fargus "")
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich DGFormalParams
462d9dc583444aab82732e14a75610684d2dc7e9Christian Maeder diag'' <- insInclusionEdges lgraph diag1 [dnsig]
e7e1ab2ac3f1fded8611bb92ae00e8f3b8c693fbKlaus Luettich ins diag'' dg1 morphNodes
ef67402074be14deb95e4ff564737d5593144130Klaus Luettich (diag'', dg4) <- ins diag' dg''' morphSigs
1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus Luettich -- check amalgamability conditions
a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich (sigR, dg5) <- extendDGraph dg4 resultSig
d784803f9c752667b4fcf7393d698002bedf3f89Klaus Luettich (gEmbed sigMorExt) DGExtension
1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus Luettich incSink <- inclusionSink lgraph (map third morphSigs) sigR
1323eba62fc519b068f5aaec4f9d2be05ffabea9Klaus Luettich let sink' = (nqB, gEmbed sigMorExt) : incSink
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder assertAmalgamability opts pos diag'' sink'
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder (q, diag''') <- extendDiagram diag'' qB
462d9dc583444aab82732e14a75610684d2dc7e9Christian Maeder (gEmbed sigMorExt) sigR
5d39c60274aaa76506292d2d9e885fccd27e1eabChristian Maeder $ showDoc uappl ""
5d39c60274aaa76506292d2d9e885fccd27e1eabChristian Maeder diag4 <- insInclusionEdges lgraph diag'''
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder (map third morphSigs) q
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder return (q, diag4, gctx'' { devGraph = dg5 }, uappl)
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder _ -> fatal_error ("Undefined unit " ++ ustr) pos
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder-- group unit term
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maederana_UNIT_TERM lgraph defl gctx curl opts uctx (Group_unit_term ut poss) =
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder do (dnsig, diag, dg, ut') <- ana_UNIT_TERM lgraph defl
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder gctx curl opts uctx (item ut)
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich return (dnsig, diag, dg, Group_unit_term (replaceAnnoted ut' ut) poss)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | Analyse unit arguments
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maederana_FIT_ARG_UNITS :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich -> HetcatsOpts -> ExtStUnitCtx -> UNIT_TERM
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder -- ^ the whole application for diagnostic purposes
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- ^ the position of the application (for diagnostic purposes)
f2d9352f2999f82c36b4b65535d14a6a40ae5a82Christian Maeder -- ^ the signatures of unit's formal parameters
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder -> [FIT_ARG_UNIT] -- ^ the arguments for the unit
43bb71dfe7ec405f563864d57c1cacdaa8ce9a80Christian Maeder -> Result ([(G_morphism, NodeSig, DiagNodeSig)], GlobalContext, Diag)
f2d9352f2999f82c36b4b65535d14a6a40ae5a82Christian Maederana_FIT_ARG_UNITS _ _ gctx _ _ (_, diag) _ _ [] [] =
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder do return ([], gctx, diag)
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowskiana_FIT_ARG_UNITS lgraph defl gctx curl opts uctx@(buc, _)
aa6c527682224a4e1434f80eae8bc2ef67fb6ca6Christian Maeder appl pos (nsig : nsigs) (fau : faus) =
aa6c527682224a4e1434f80eae8bc2ef67fb6ca6Christian Maeder do (gmorph, nsig', dnsig, dg, diag) <- ana_FIT_ARG_UNIT lgraph defl
37951dbd8e5f2418a07f072d9bf551d0c3a1eafcChristian Maeder gctx curl opts uctx nsig fau
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder (morphSigs, dg', diag') <- ana_FIT_ARG_UNITS lgraph defl
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder (buc, diag) appl pos nsigs faus
aa6c527682224a4e1434f80eae8bc2ef67fb6ca6Christian Maeder return ((gmorph, nsig', dnsig) : morphSigs, dg', diag')
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maederana_FIT_ARG_UNITS _ _ gctx _ _ (_, diag) appl pos [] _ =
c22d75ec3ea1306219d1c09a5b3e8ff04f753ad6Christian Maeder do plain_error ([], gctx, diag)
9c3edf2b283c09d33b2820696886d1ed32fcadc8Christian Maeder ("Too many arguments given in application\n"
c22d75ec3ea1306219d1c09a5b3e8ff04f753ad6Christian Maeder ++ showDoc appl "") pos
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederana_FIT_ARG_UNITS _ _ gctx _ _ (_, diag) appl pos _ [] =
68b77966b2cf7bf2e340bf0fb6b9efc3e6a00467Christian Maeder do plain_error ([], gctx, diag)
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder ("Too few arguments given in application\n"
5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder ++ showDoc appl "") pos
5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder-- | Analyse unit argument
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederana_FIT_ARG_UNIT :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic
5bb7eeaca10ea76595229375f907a5a388b7c882Christian Maeder -> HetcatsOpts -> ExtStUnitCtx -> NodeSig -> FIT_ARG_UNIT
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder -> Result (G_morphism, NodeSig, DiagNodeSig, GlobalContext, Diag)
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder-- ^ returns 1. the signature morphism 2. the target signature of the morphism
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder-- 3. the diagram node 4. the modified DGraph 5. the modified diagram
ddc9315cc0b1f5dd3d8f99a77f1c75064db33b48Christian Maederana_FIT_ARG_UNIT lgraph defl gctx curl opts uctx nsig
ddc9315cc0b1f5dd3d8f99a77f1c75064db33b48Christian Maeder (Fit_arg_unit ut symbMap poss) =
5d522dff4d0fabf57dd476d4c3de15d354a89f62Christian Maeder do (p, diag', gctx', _) <- ana_UNIT_TERM lgraph defl
5d522dff4d0fabf57dd476d4c3de15d354a89f62Christian Maeder gctx curl opts uctx (item ut)
5d522dff4d0fabf57dd476d4c3de15d354a89f62Christian Maeder -- compute gMorph (the morphism r|sigma/D(p))
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder let adj = adjustPos poss
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder gsigmaS = getSig nsig
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder gsigmaT = getSig (getSigFromDiag p)
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder dg' = devGraph gctx'
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich G_sign lidS sigmaS _ <- return gsigmaS
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich G_sign lidT sigmaT _ <- return gsigmaT
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich G_symb_map_items_list lid sis <- adj $ homogenizeGM (Logic lidS) symbMap
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich sigmaT' <- adj $ coerceSign lidT lidS "" sigmaT
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich mor <- if isStructured opts then return (ide lidS sigmaS)
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich else do rmap <- adj $ stat_symb_map_items lid sis
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich rmap' <- adj $ coerceRawSymbolMap lid lidS "" rmap
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich adj $ induced_from_to_morphism lidS rmap'
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich sigmaS sigmaT'
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich let gMorph = G_morphism lidS mor 0
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich (nsig', dg'') <- extendDGraph dg' nsig (gEmbed gMorph) DGFitSpec
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich return (gMorph, nsig', p, gctx' { devGraph = dg'' }, diag')
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich-- | Analyse unit specification
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettichana_UNIT_SPEC :: LogicGraph -> AnyLogic -- ^ the default logic
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich -> GlobalContext -> AnyLogic -- ^ current logic
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich -> HetcatsOpts -- ^ should only the structure be analysed?
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich -> MaybeNode -- ^ the signature of imports
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich -> UNIT_SPEC -> Result (UnitSig, GlobalContext, UNIT_SPEC)
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich-- ^ returns 1. unit signature 2. the development graph resulting from
ac43fa22d2d3f91a17674ac164cba3cf39a17795Klaus Luettich-- structred specs inside the unit spec and 3. a UNIT_SPEC after possible
ac43fa22d2d3f91a17674ac164cba3cf39a17795Klaus Luettich-- conversions.
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers{- if argspecs are empty and resultspec is a name of unit spec then this
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder should be converted to a Spec_name -}
18c1d987ce5818ecf0bfc8af3f43aed2ce86e1eaChristian Maederana_UNIT_SPEC lgraph defl gctx curl just_struct
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder impsig (Unit_type [] (Annoted (Spec_inst spn [] _) _ _ _) _)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder | case Map.lookup spn $ globalEnv gctx of
1c9a63e4f7c6879f51fe0f32154a9116f2c126dbChristian Maeder Just (UnitEntry _) -> True
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder ana_UNIT_SPEC lgraph defl gctx curl just_struct impsig (Spec_name spn)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- a trivial unit type
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maederana_UNIT_SPEC lgraph _ gctx _ just_struct impsig
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder (Unit_type [] resultSpec poss) =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder do (resultSpec', resultSig, dg') <- ana_SPEC lgraph
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich gctx impsig emptyNodeName just_struct (item resultSpec)
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski return (Unit_sig resultSig, dg', Unit_type []
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski (replaceAnnoted resultSpec' resultSpec) poss)
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski-- a non-trivial unit type
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederana_UNIT_SPEC lgraph defl gctx _ opts impSig
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder (Unit_type argSpecs resultSpec poss) =
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder do (argSigs, gctx1, argSpecs') <- ana_argSpecs lgraph defl gctx
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder opts argSpecs
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder let dg1 = devGraph gctx1
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder (sigUnion, dg2) <- nodeSigUnion lgraph dg1
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder (impSig : map JustNode argSigs) DGFormalParams
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder (resultSpec', resultSig, dg3) <- ana_SPEC lgraph
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers gctx1 { devGraph = dg2 } (JustNode sigUnion)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder emptyNodeName opts (item resultSpec)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder return (Par_unit_sig argSigs resultSig, dg3, Unit_type argSpecs'
e96a0bf4040fd789339958c01f145c5057d26db6René Wagner (replaceAnnoted resultSpec' resultSpec) poss)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- SPEC-NAME (an alias)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederana_UNIT_SPEC _ _ gctx _ _ _impsig usp@(Spec_name usn@(Token ustr pos)) =
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich do case Map.lookup usn $ globalEnv gctx of
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich Nothing -> fatal_error ("Undefined unit specification "
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich Just (UnitEntry usig) -> return (usig, gctx, usp)
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers _ -> fatal_error (ustr ++ " is not an unit specification")
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder-- CLOSED-UNIT-SPEC
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maederana_UNIT_SPEC lgraph defl gctx curl just_struct _ (Closed_unit_spec usp' _) =
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers ana_UNIT_SPEC lgraph defl gctx curl just_struct (EmptyNode curl) usp'
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | Analyse refinement specification
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederana_REF_SPEC :: LogicGraph -> AnyLogic -- ^ the default logic
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich -> GlobalContext -> AnyLogic -- ^ current logic
a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich -> HetcatsOpts -- ^ should only the structure be analysed?
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -> MaybeNode -- ^ the signature of imports
a80c28bb8b7a23ccdf7e08d0fe216fc19cc97273Klaus Luettich -> REF_SPEC -> Result (UnitSig, GlobalContext, REF_SPEC)
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maederana_REF_SPEC lgraph defl gctx curl just_struct nsig (Unit_spec asp) =
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder do (usig, dg', asp') <- ana_UNIT_SPEC lgraph defl
b9625461755578f3eed04676d42a63fd2caebd0cChristian Maeder gctx curl just_struct nsig asp
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder return (usig, dg', Unit_spec asp')
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- ARCH-UNIT-SPEC
d0652648f9879c67a194f8b03baafe2700c68eb4Christian Maederana_REF_SPEC lgraph defl gctx curl just_struct _ (Arch_unit_spec asp poss) =
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder do (ArchSig _ usig, dg', asp') <- ana_ARCH_SPEC lgraph defl
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder gctx curl just_struct (item asp)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder return (usig, dg', Arch_unit_spec (replaceAnnoted asp' asp) poss)
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder-- dummy implementation for the rest
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettichana_REF_SPEC _ _ _ _ _ _ _ = error "ana_REF_SPEC"
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich-- | Analyse a list of argument specifications
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maederana_argSpecs :: LogicGraph -> AnyLogic -> GlobalContext -> HetcatsOpts
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich -> [Annoted SPEC]
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -> Result ([NodeSig], GlobalContext, [Annoted SPEC])
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederana_argSpecs _ _ gctx _ [] =
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder do return ([], gctx, [])
27785f379d6810811b4e6d23feab18845fde9a98Christian Maederana_argSpecs lgraph defl gctx opts (argSpec : argSpecs) =
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder do (argSpec', argSig, dg') <- ana_SPEC lgraph
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder gctx (EmptyNode defl) emptyNodeName
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder opts (item argSpec)
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder (argSigs, dg'', argSpecs') <- ana_argSpecs lgraph defl
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder dg' opts argSpecs
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder return (argSig : argSigs, dg'', replaceAnnoted argSpec' argSpec
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder{- | Check that given diagram ensures amalgamability along given set
27785f379d6810811b4e6d23feab18845fde9a98Christian Maederof morphisms -}
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaederassertAmalgamability :: HetcatsOpts -- ^ the program options
c5e3fc166373b0d90f6e36e8aa234396a1dcd879Christian Maeder -> Range -- ^ the position (for diagnostics)
340706b6c0c6e3dbacdd7003e20e9cab7f9aa765Christian Maeder -> Diag -- ^ the diagram to be checked
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich -> [(Node, GMorphism)] -- ^ the sink
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederassertAmalgamability opts pos diag sink =
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder do ensAmalg <- homogeneousEnsuresAmalgamability opts pos diag sink
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder case ensAmalg of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Amalgamates -> return ()
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder NoAmalgamation msg -> plain_error ()
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder ("Amalgamability is not ensured: " ++ msg) pos
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder DontKnow msg -> warning () msg pos
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | Check the amalgamability assuming common logic for whole diagram
50515239e7e190f4a34ca581dd685d002148fbddChristian MaederhomogeneousEnsuresAmalgamability :: HetcatsOpts -- ^ the program options
50515239e7e190f4a34ca581dd685d002148fbddChristian Maeder -> Range -- ^ the position (for diagnostics)
50515239e7e190f4a34ca581dd685d002148fbddChristian Maeder -> Diag -- ^ the diagram to be checked
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -> [(Node, GMorphism)] -- ^ the sink
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -> Result Amalgamates
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederhomogeneousEnsuresAmalgamability opts pos diag sink =
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder do case sink of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder [] -> plain_error defaultDontKnow
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder "homogeneousEnsuresAmalgamability: Empty sink" pos
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski lab:_ -> do let (_, mor) = lab
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski sig = cod Grothendieck mor
8b4c68db8b465107cabef8b9cd5b6bc216e1b156Till Mossakowski G_sign lid _ _<- return sig
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini hDiag <- homogeniseDiagram lid diag
df29370ae8d8b41587957f6bcdcb43a3f1927e47Christian Maeder hSink <- homogeniseSink lid sink
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo Torrini ensures_amalgamability lid (caslAmalg opts,
5ce19352a9cc47d982819cc889a71cd0a61ac171Christian Maeder hDiag, hSink, (diagDesc diag))
5ce19352a9cc47d982819cc889a71cd0a61ac171Christian Maeder-- | Get a position within the source file of a UNIT-TERM
bcaf979d9babe6346aa343687aa7d596e2894cccPaolo TorrinigetPos_UNIT_TERM :: UNIT_TERM -> Range
23ab8855c58adfbd03a0730584b917b24c603901Christian Maeder-- UNIT-REDUCTION
df29370ae8d8b41587957f6bcdcb43a3f1927e47Christian MaedergetPos_UNIT_TERM (Unit_reduction _ restr) =
23ab8855c58adfbd03a0730584b917b24c603901Christian Maeder -- obtain position from RESTRICTION
e50e41135ece589f7202bd4ef8d6b97531c2a56eKlaus Luettich case restr of
47b0e9f3cb008cb7997f4e3bae26e4d62dcc887aChristian Maeder (Hidden _ poss) -> poss
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (Revealed _ poss) -> poss
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- UNIT-TRANSLATION
431d34c7007a787331c4e5ec997badb0f8190fc7Christian MaedergetPos_UNIT_TERM (Unit_translation _ (Renaming _ poss)) =
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- AMALGAMATION
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedergetPos_UNIT_TERM (Amalgamation _ poss) =
88318aafc287e92931dceffbb943d58a9310001dChristian MaedergetPos_UNIT_TERM (Local_unit _ _ poss) =
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder-- UNIT-APPLICATION
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedergetPos_UNIT_TERM (Unit_appl u _ poss) =
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder appRange (tokPos u) poss
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder-- GROUP-UNIT-TERM
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaedergetPos_UNIT_TERM (Group_unit_term _ poss) =
9096f6c6aaded6cd8288656ceccd4c7b3bd0747eChristian Maeder-- | Get a position within the source file of UNIT-IMPORTED
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus LuettichgetPos_UNIT_IMPORTED :: Range -> Range
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus LuettichgetPos_UNIT_IMPORTED (Range ps) = Range $ case ps of
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich _ : qs -> if null qs then ps else qs
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich-- | Get a position within the source file of UNIT-EXPRESSION
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus LuettichgetPos_UNIT_EXPRESSION :: UNIT_EXPRESSION -> Range
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedergetPos_UNIT_EXPRESSION (Unit_expression _ (Annoted ut _ _ _) poss) =
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder appRange (getPos_UNIT_TERM ut) poss