d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder{- |

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederModule : $Header$

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederDescription : static analysis of CASL architectural specifications

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Maciek Makowski, Warsaw University, C. Maeder 2004-2006

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : till@informatik.uni-bremen.de

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederStability : provisional

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederPortability : non-portable (via imports)

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederStatic analysis of CASL architectural specifications

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

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder of the CASL Reference Manual.

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder-}

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maedermodule Static.AnalysisArchitecture

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder ( ana_ARCH_SPEC

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder , ana_UNIT_SPEC

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder , ana_UNIT_REF

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder ) where

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Driver.Options

02a2037f53b925617df45eb62ca743d777672265Klaus Luettich

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Logic.Logic

fe216849cef7b87c6800aad21178d1e686575d8fChristian Maederimport Logic.ExtSign

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Logic.Coerce

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maederimport Logic.Grothendieck

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Static.GTheory

7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian Maederimport Static.DevGraph

b7b2eb9d574f5ed3ac3e9e1d7a5f168ed78a0604Till Mossakowskiimport Static.ArchDiagram

0678d323bee844db79af13113ae252546629a594Christian Maederimport Static.AnalysisStructured

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Syntax.Print_AS_Architecture ()

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Syntax.AS_Architecture

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederimport Syntax.AS_Structured

fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder

7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian Maederimport Common.AS_Annotation

7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian Maederimport Common.Id

7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian Maederimport Common.Result

7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian Maederimport Common.Amalgamate

7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian Maederimport Common.DocUtils

7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian Maederimport qualified Data.Map as Map

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maederimport Data.Graph.Inductive.Graph as Graph (Node)

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder-- | Analyse an architectural specification

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder-- @

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder-- ARCH-SPEC ::= BASIC-ARCH-SPEC | GROUP-ARCH-SPEC | ARCH-SPEC-NAME

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder-- @

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maederana_ARCH_SPEC :: LogicGraph

7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian Maeder -> DGraph

fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder -> HetcatsOpts -- ^ should only the structure be analysed?

fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder -> ARCH_SPEC -> Result (ArchSig, DGraph, ARCH_SPEC)

fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder{- ^ returns 1. the architectural signature of given ARCH-SPEC

fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder2. development graph resulting from structured specs within the arch

fe216849cef7b87c6800aad21178d1e686575d8fChristian Maederspec and 3. ARCH_SPEC after possible conversions -}

fe216849cef7b87c6800aad21178d1e686575d8fChristian Maederana_ARCH_SPEC lgraph dg opts archSp = case archSp of

fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder Basic_arch_spec udd uexpr pos ->

fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder do (uctx, dg', udd') <- ana_UNIT_DECL_DEFNS lgraph dg opts udd

fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder (_, usig, _, dg'', uexpr') <-

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder ana_UNIT_EXPRESSION lgraph dg' opts uctx (item uexpr)

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder return (ArchSig (ctx uctx) usig, dg'', Basic_arch_spec udd'

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder (replaceAnnoted uexpr' uexpr) pos)

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder Group_arch_spec asp _ -> ana_ARCH_SPEC lgraph dg opts (item asp)

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder Arch_spec_name asn@(Token astr pos) -> case lookupGlobalEnvDG asn dg of

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder Just (ArchEntry asig) -> return (asig, dg, archSp)

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder _ -> fatal_error (astr ++

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder " is not an architectural specification") pos

bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder-- | Analyse a list of unit declarations and definitions

a255351561838b3743d03c1629d335cfb8b83804Christian Maederana_UNIT_DECL_DEFNS :: LogicGraph -> DGraph

fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder -> HetcatsOpts -> [Annoted UNIT_DECL_DEFN]

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

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder{- ^ returns 1. extended static unit context 2. possibly modified

a255351561838b3743d03c1629d335cfb8b83804Christian Maederdevelopment graph 3. possibly modified list of unit declarations and

a255351561838b3743d03c1629d335cfb8b83804Christian Maederdefinitions -}

a255351561838b3743d03c1629d335cfb8b83804Christian Maederana_UNIT_DECL_DEFNS lgraph dg opts udds =

f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder ana_UNIT_DECL_DEFNS' lgraph dg opts emptyExtStUnitCtx udds

a255351561838b3743d03c1629d335cfb8b83804Christian Maeder

fe216849cef7b87c6800aad21178d1e686575d8fChristian Maederana_UNIT_DECL_DEFNS' :: LogicGraph -> DGraph

f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder -> HetcatsOpts -> ExtStUnitCtx -> [Annoted UNIT_DECL_DEFN]

02a2037f53b925617df45eb62ca743d777672265Klaus Luettich -> Result (ExtStUnitCtx, DGraph, [Annoted UNIT_DECL_DEFN])

02a2037f53b925617df45eb62ca743d777672265Klaus Luettichana_UNIT_DECL_DEFNS' lgraph dg opts uctx uds = case uds of

02a2037f53b925617df45eb62ca743d777672265Klaus Luettich udd : udds -> do

02a2037f53b925617df45eb62ca743d777672265Klaus Luettich (uctx', dg', udd') <-

02a2037f53b925617df45eb62ca743d777672265Klaus Luettich ana_UNIT_DECL_DEFN lgraph dg opts uctx (item udd)

f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder (uctx'', dg'', udds') <-

5908cc06d7a3f4dd46d2d7c7fe0fad43b6cd921fChristian Maeder ana_UNIT_DECL_DEFNS' lgraph dg' opts uctx' udds

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

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder [] -> return (uctx, dg, [])

5908cc06d7a3f4dd46d2d7c7fe0fad43b6cd921fChristian Maeder

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederalreadyDefinedUnit :: SIMPLE_ID -> String

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederalreadyDefinedUnit u = "Unit " ++ tokStr u ++ " already declared/defined"

02a2037f53b925617df45eb62ca743d777672265Klaus Luettich

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

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaedernodeSigUnion :: LogicGraph -> DGraph -> [MaybeNode] -> DGOrigin

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -> Result (NodeSig, DGraph)

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaedernodeSigUnion lgraph dg nodeSigs orig =

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

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder $ map getMaybeSig nodeSigs

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder let nodeContents = newNodeLab emptyNodeName orig

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder $ noSensGTheory lid sigU ind

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder node = getNewNodeDG dg

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder dg' = insNodeDG (node, nodeContents) dg

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder inslink dgres nsig = do

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder dgv <- dgres

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder case nsig of

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder EmptyNode _ -> dgres

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder JustNode (NodeSig n sig) -> do

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder incl <- ginclusion lgraph sig sigUnion

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder return $ insEdgeDG (n, node, DGLink

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder { dgl_morphism = incl

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder , dgl_type = GlobalDef

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder , dgl_origin = SeeTarget

f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder , dgl_id = getNewEdgeId dgv

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder }) dgv

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

f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder return (NodeSig node sigUnion, dg'')

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder-- | Analyse unit refs

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederana_UNIT_REF :: LogicGraph -> DGraph

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder -> HetcatsOpts -> ExtStUnitCtx -> UNIT_REF

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder -> Result (ExtStUnitCtx, DGraph, UNIT_REF)

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder{- ^ returns 1. extended static unit context 2. possibly modified

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maederdevelopment graph 3. possibly modified UNIT_DECL_DEFN -}

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder-- unit declaration

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maederana_UNIT_REF lgraph dg opts

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder uctx@(buc, _) (Unit_ref un@(Token ustr unpos) usp pos) =

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder do (dns, diag', dg', _) <-

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder ana_UNIT_IMPORTED lgraph dg opts uctx pos []

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder let impSig = toMaybeNode dns

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder (usig, dg'', usp') <-

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder ana_REF_SPEC lgraph dg' opts impSig usp

e935423c16e00af45bffbe131f4bd9ae01853fcbChristian Maeder let ud' = Unit_ref un usp' pos

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder if Map.member un buc

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder then plain_error (uctx, dg'', ud') (alreadyDefinedUnit un) unpos

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder else case usig of

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder ParUnitSig argSigs resultSig ->

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder do (resultSig', dg''') <- nodeSigUnion lgraph dg''

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder (JustNode resultSig : [impSig]) DGImports

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder let basedParUSig = Based_par_unit_sig dns $

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder ParUnitSig argSigs resultSig'

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder return ((Map.insert un basedParUSig buc, diag'),

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder dg''', ud')

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder UnitSig nsig ->

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder do (nsig', dg''') <- nodeSigUnion lgraph dg''

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder (impSig : [JustNode nsig]) DGImports

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder (dn', diag'') <- extendDiagramIncl lgraph diag' []

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder nsig' ustr

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder return ((Map.insert un (Based_unit_sig dn') buc, diag'')

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder , dg''', ud')

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder-- | Analyse unit declaration or definition

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maederana_UNIT_DECL_DEFN :: LogicGraph -> DGraph

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder -> HetcatsOpts -> ExtStUnitCtx -> UNIT_DECL_DEFN

91f4f0335ac32768d819e202263f713aef5d7fe6Christian Maeder -> Result (ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder{- ^ returns 1. extended static unit context 2. possibly modified

36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maederdevelopment graph 3. possibly modified UNIT_DECL_DEFN -}

0678d323bee844db79af13113ae252546629a594Christian Maederana_UNIT_DECL_DEFN lgraph dg opts uctx@(buc, _) udd = case udd of

0678d323bee844db79af13113ae252546629a594Christian Maeder Unit_decl un@(Token ustr unpos) usp uts pos -> do

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder (dns, diag', dg', uts') <-

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder ana_UNIT_IMPORTED lgraph dg opts uctx pos uts

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder let impSig = toMaybeNode dns

0678d323bee844db79af13113ae252546629a594Christian Maeder (usig, dg'', usp') <-

0678d323bee844db79af13113ae252546629a594Christian Maeder ana_REF_SPEC lgraph dg' opts impSig usp

0678d323bee844db79af13113ae252546629a594Christian Maeder let ud' = Unit_decl un usp' uts' pos

0678d323bee844db79af13113ae252546629a594Christian Maeder if Map.member un buc

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder then plain_error (uctx, dg'', ud') (alreadyDefinedUnit un) unpos

36fcac4cf0f6a1f8a0fee696ac7f4b91d769843cChristian Maeder else case usig of

0678d323bee844db79af13113ae252546629a594Christian Maeder ParUnitSig argSigs resultSig ->

0678d323bee844db79af13113ae252546629a594Christian Maeder do (resultSig', dg''') <- nodeSigUnion lgraph dg''

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder (JustNode resultSig : [impSig]) DGImports

b7b2eb9d574f5ed3ac3e9e1d7a5f168ed78a0604Till Mossakowski let basedParUSig = Based_par_unit_sig dns $

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder ParUnitSig argSigs resultSig'

0678d323bee844db79af13113ae252546629a594Christian Maeder return ((Map.insert un basedParUSig buc, diag'),

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder dg''', ud')

0678d323bee844db79af13113ae252546629a594Christian Maeder UnitSig nsig ->

0678d323bee844db79af13113ae252546629a594Christian Maeder do (nsig', dg''') <- nodeSigUnion lgraph dg''

0678d323bee844db79af13113ae252546629a594Christian Maeder (impSig : [JustNode nsig]) DGImports

0678d323bee844db79af13113ae252546629a594Christian Maeder (dn', diag'') <- extendDiagramIncl lgraph diag'

0678d323bee844db79af13113ae252546629a594Christian Maeder (case dns of

0678d323bee844db79af13113ae252546629a594Christian Maeder JustDiagNode dn -> [dn]

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder _ -> []) nsig' ustr

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder return ((Map.insert un (Based_unit_sig dn') buc, diag'')

b7b2eb9d574f5ed3ac3e9e1d7a5f168ed78a0604Till Mossakowski , dg''', ud')

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Unit_defn un uexp poss -> do

0678d323bee844db79af13113ae252546629a594Christian Maeder (p, usig, diag, dg', uexp') <-

0678d323bee844db79af13113ae252546629a594Christian Maeder ana_UNIT_EXPRESSION lgraph dg opts uctx uexp

0678d323bee844db79af13113ae252546629a594Christian Maeder let ud' = Unit_defn un uexp' poss

0678d323bee844db79af13113ae252546629a594Christian Maeder {- it's sufficient to check that un is not mapped in buc, we

0678d323bee844db79af13113ae252546629a594Christian Maeder don't need to convert the ExtStUnitCtx to StUnitCtx as the

d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder domain will be preserved -}

0678d323bee844db79af13113ae252546629a594Christian Maeder if Map.member un buc then

0678d323bee844db79af13113ae252546629a594Christian Maeder plain_error (uctx, dg', ud') (alreadyDefinedUnit un) $ tokPos un

0678d323bee844db79af13113ae252546629a594Christian Maeder else case usig of

0678d323bee844db79af13113ae252546629a594Christian Maeder {- we can use Map.insert as there are no mappings for

0678d323bee844db79af13113ae252546629a594Christian Maeder un in ps and bs (otherwise there would have been a

0678d323bee844db79af13113ae252546629a594Christian Maeder mapping in (ctx uctx)) -}

0678d323bee844db79af13113ae252546629a594Christian Maeder UnitSig _ -> case p of

0678d323bee844db79af13113ae252546629a594Christian Maeder JustDiagNode dn -> return ((Map.insert un

0678d323bee844db79af13113ae252546629a594Christian Maeder (Based_unit_sig dn) buc, diag), dg', ud')

fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder _ -> error "ana_UNIT_DECL_DEFN"

fe216849cef7b87c6800aad21178d1e686575d8fChristian Maeder ParUnitSig _ _ -> return ((Map.insert un

0678d323bee844db79af13113ae252546629a594Christian Maeder (Based_par_unit_sig p usig) buc

0678d323bee844db79af13113ae252546629a594Christian Maeder , diag), dg', ud')

0678d323bee844db79af13113ae252546629a594Christian Maeder

0678d323bee844db79af13113ae252546629a594Christian Maeder-- | Analyse unit imports

0678d323bee844db79af13113ae252546629a594Christian Maederana_UNIT_IMPORTED :: LogicGraph -> DGraph

0678d323bee844db79af13113ae252546629a594Christian Maeder -> HetcatsOpts -> ExtStUnitCtx -> Range -> [Annoted UNIT_TERM]

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

0678d323bee844db79af13113ae252546629a594Christian Maederana_UNIT_IMPORTED lgraph dg opts uctx@(_, diag) poss terms =

0678d323bee844db79af13113ae252546629a594Christian Maeder case terms of

0678d323bee844db79af13113ae252546629a594Christian Maeder [] -> do

0678d323bee844db79af13113ae252546629a594Christian Maeder curl <- lookupCurrentLogic "UNIT_IMPORTED" lgraph

0678d323bee844db79af13113ae252546629a594Christian Maeder return (EmptyDiagNode curl, diag, dg, [])

0678d323bee844db79af13113ae252546629a594Christian Maeder _ -> do

0678d323bee844db79af13113ae252546629a594Christian Maeder (dnsigs, diag', dg', terms') <-

0678d323bee844db79af13113ae252546629a594Christian Maeder ana_UNIT_IMPORTED' lgraph dg opts uctx terms

0678d323bee844db79af13113ae252546629a594Christian Maeder (sig, dg'') <- nodeSigUnion lgraph dg'

0678d323bee844db79af13113ae252546629a594Christian Maeder (map (JustNode . getSigFromDiag) dnsigs) DGImports

0678d323bee844db79af13113ae252546629a594Christian Maeder -- check amalgamability conditions

0678d323bee844db79af13113ae252546629a594Christian Maeder {- let incl s = propagateErrors (ginclusion lgraph (getSig

0678d323bee844db79af13113ae252546629a594Christian Maeder (getSigFromDiag s)) (getSig sig)) -}

0678d323bee844db79af13113ae252546629a594Christian Maeder let pos = getPos_UNIT_IMPORTED poss

0678d323bee844db79af13113ae252546629a594Christian Maeder sink <- inclusionSink lgraph dnsigs sig

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder () <- assertAmalgamability opts pos diag' sink

0678d323bee844db79af13113ae252546629a594Christian Maeder (dnsig, diag'') <- extendDiagramIncl lgraph diag' dnsigs

f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder sig $ showDoc terms ""

0678d323bee844db79af13113ae252546629a594Christian Maeder return (JustDiagNode dnsig, diag'', dg'', terms')

0678d323bee844db79af13113ae252546629a594Christian Maeder

0678d323bee844db79af13113ae252546629a594Christian Maederana_UNIT_IMPORTED' :: LogicGraph -> DGraph

0678d323bee844db79af13113ae252546629a594Christian Maeder -> HetcatsOpts -> ExtStUnitCtx -> [Annoted UNIT_TERM]

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

0678d323bee844db79af13113ae252546629a594Christian Maederana_UNIT_IMPORTED' lgraph dg opts uctx@(buc, diag) ts = case ts of

0678d323bee844db79af13113ae252546629a594Christian Maeder [] -> return ([], diag, dg, [])

0678d323bee844db79af13113ae252546629a594Christian Maeder ut : uts -> do

0678d323bee844db79af13113ae252546629a594Christian Maeder (dnsig, diag', dg', ut') <-

0678d323bee844db79af13113ae252546629a594Christian Maeder ana_UNIT_TERM lgraph dg opts uctx (item ut)

0678d323bee844db79af13113ae252546629a594Christian Maeder (dnsigs, diag'', dg'', uts') <-

0678d323bee844db79af13113ae252546629a594Christian Maeder ana_UNIT_IMPORTED' lgraph dg' opts (buc, diag') uts

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

0678d323bee844db79af13113ae252546629a594Christian Maeder

0678d323bee844db79af13113ae252546629a594Christian Maeder-- | Analyse an unit expression

0678d323bee844db79af13113ae252546629a594Christian Maederana_UNIT_EXPRESSION :: LogicGraph -> DGraph

0678d323bee844db79af13113ae252546629a594Christian Maeder -> HetcatsOpts -> ExtStUnitCtx -> UNIT_EXPRESSION

0678d323bee844db79af13113ae252546629a594Christian Maeder -> Result (MaybeDiagNode, UnitSig, Diag, DGraph, UNIT_EXPRESSION)

0678d323bee844db79af13113ae252546629a594Christian Maederana_UNIT_EXPRESSION lgraph dg opts uctx@(buc, diag)

0678d323bee844db79af13113ae252546629a594Christian Maeder uexp@(Unit_expression ubs ut poss) = case ubs of

0678d323bee844db79af13113ae252546629a594Christian Maeder [] -> do

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

0678d323bee844db79af13113ae252546629a594Christian Maeder ana_UNIT_TERM lgraph dg opts uctx (item ut)

0678d323bee844db79af13113ae252546629a594Christian Maeder return (JustDiagNode dnsig, UnitSig ns', diag', dg',

0678d323bee844db79af13113ae252546629a594Christian Maeder Unit_expression [] (replaceAnnoted ut' ut) poss)

0678d323bee844db79af13113ae252546629a594Christian Maeder _ -> do

0678d323bee844db79af13113ae252546629a594Christian Maeder (args, dg', ubs') <-

0678d323bee844db79af13113ae252546629a594Christian Maeder ana_UNIT_BINDINGS lgraph dg opts uctx ubs

0678d323bee844db79af13113ae252546629a594Christian Maeder (resnsig, _dg'') <- nodeSigUnion lgraph dg'

0678d323bee844db79af13113ae252546629a594Christian Maeder (map (JustNode . snd) args) DGFormalParams

0678d323bee844db79af13113ae252546629a594Christian Maeder -- build the extended diagram and new based unit context

f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder let dexp = showDoc uexp ""

0678d323bee844db79af13113ae252546629a594Christian Maeder insNodes diag0 [] buc0 = return ([], diag0, buc0)

0678d323bee844db79af13113ae252546629a594Christian Maeder insNodes diag0 ((un, nsig) : args0) buc0 =

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

0678d323bee844db79af13113ae252546629a594Christian Maeder nsig dexp

{- we made sure in ana_UNIT_BINDINGS that there's no

mapping for un in buc so we can just use

Map.insert -}

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

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

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

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

(_, diag'') <- extendDiagramIncl lgraph diag' pardnsigs

resnsig dexp

-- analyse the unit term

(p@(Diag_node_sig _ pnsig), diag''', dg''', ut') <-

ana_UNIT_TERM lgraph dg' opts (buc', diag'') (item ut)

-- check amalgamability conditions

let pos = getPos_UNIT_EXPRESSION uexp

checkSubSign [] _ = True

checkSubSign (dnsub : dnsigs) nsup =

if isSubGsign lgraph (getSig $ getSigFromDiag dnsub) $ getSig nsup

then checkSubSign dnsigs nsup else False

-- check that signatures in pardnsigs are subsignatures of pnsig

if checkSubSign pardnsigs pnsig

then

do sink <- inclusionSink lgraph (p : pardnsigs) pnsig

() <- assertAmalgamability opts pos diag''' sink

-- add new node to the diagram

curl <- lookupCurrentLogic "UNIT_EXPRESSION" lgraph

return (EmptyDiagNode curl, ParUnitSig (map snd args) pnsig,

diag''', dg''',

Unit_expression ubs' (replaceAnnoted ut' ut) poss)

else -- report an error

fatal_error

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

++ dexp) pos

{- | Analyse a list of unit bindings. Ensures that the unit names are

not present in extended static unit context and that there are no

duplicates among them. -}

ana_UNIT_BINDINGS :: LogicGraph -> DGraph

-> HetcatsOpts -> ExtStUnitCtx -> [UNIT_BINDING]

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

ana_UNIT_BINDINGS lgraph dg opts uctx@(buc, _) bs = case bs of

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

Unit_binding un@(Token ustr unpos) usp poss : ubs -> do

curl <- lookupCurrentLogic "UNIT_BINDINGS" lgraph

(usig, dg', usp') <-

ana_UNIT_SPEC lgraph dg opts (EmptyNode curl) usp

let ub' = Unit_binding un usp' poss

case usig of

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

("An argument unit " ++

ustr ++ " must not be parameterized") unpos

UnitSig nsig ->

do (args, dg'', ubs') <- ana_UNIT_BINDINGS lgraph

dg' opts uctx ubs

let args' = (un, nsig) : args

if Map.member un buc

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

(alreadyDefinedUnit un) unpos

else case lookup un args of

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

(alreadyDefinedUnit un) unpos

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

-- | Analyse a list of unit terms

ana_UNIT_TERMS :: LogicGraph -> DGraph

-> HetcatsOpts -> ExtStUnitCtx -> [Annoted UNIT_TERM]

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

ana_UNIT_TERMS lgraph dg opts uctx@(buc, diag) ts = case ts of

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

ut : uts -> do

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

ana_UNIT_TERM lgraph dg opts uctx (item ut)

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

dg' opts (buc, diag') uts

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

-- | Analyse an unit term

ana_UNIT_TERM :: LogicGraph -> DGraph

-> HetcatsOpts -> ExtStUnitCtx -> UNIT_TERM

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

ana_UNIT_TERM lgraph dg opts uctx@(buc, diag) utrm =

let pos = getPos_UNIT_TERM utrm

utStr = showDoc utrm ""

in case utrm of

Unit_reduction ut restr -> do

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

ana_UNIT_TERM lgraph dg opts uctx (item ut)

curl <- lookupCurrentLogic "UNIT_TERM" lgraph

(incl, msigma) <- ana_RESTRICTION (emptyG_sign curl)

(getSig (getSigFromDiag p)) opts restr

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

extendDiagramWithMorphismRev pos lgraph diag1 dg1 p incl utStr

(case restr of

Hidden _ _ -> DGHiding

Revealed _ _ -> DGRevealing)

case msigma of

Nothing ->

{- the renaming morphism is just identity, so

there's no need to extend the diagram -}

return (q, diag', dg',

Unit_reduction (replaceAnnoted ut' ut) restr)

Just sigma ->

do

-- check amalgamability conditions

let sink = [(qn, sigma)]

() <- assertAmalgamability opts pos diag' sink

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

lgraph diag' dg' q sigma utStr

(case restr of

Hidden _ _ -> DGHiding

Revealed _ _ -> DGRevealing)

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

Unit_reduction

(replaceAnnoted ut' ut) restr)

Unit_translation ut ren -> do

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

ana_UNIT_TERM lgraph dg opts uctx (item ut)

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

gMorph <- ana_RENAMING lgraph

(EmptyNode $ error "Static.AnalysisArchitecture")

(getSig (getSigFromDiag dnsig)) opts ren

let sink = [(p, gMorph)]

-- check amalamability conditions

() <- assertAmalgamability opts pos diag1 sink

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

diag1 dg1 dnsig gMorph utStr

DGTranslation

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

(replaceAnnoted ut' ut) ren)

Amalgamation uts poss -> do

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

ana_UNIT_TERMS lgraph dg opts uctx uts

-- compute sigma

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

(map (JustNode . getSigFromDiag) dnsigs) DGUnion

-- check amalgamability conditions

sink <- inclusionSink lgraph dnsigs sig

() <- assertAmalgamability opts poss diag1 sink

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

sig utStr

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

Local_unit udds ut poss -> do

(uctx', dg1, udds') <-

ana_UNIT_DECL_DEFNS' lgraph dg opts uctx udds

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

ana_UNIT_TERM lgraph dg1 opts uctx' (item ut)

return (dnsig, diag', dg',

Local_unit udds' (replaceAnnoted ut' ut) poss)

Unit_appl un fargus _ -> do

let ustr = tokStr un

argStr = showDoc fargus ""

case Map.lookup un buc of

Just (Based_unit_sig dnsig) -> case fargus of

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

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

plain_error (dnsig, diag, dg, utrm)

(ustr ++ " is a parameterless unit, "

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

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

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

(toMaybeNode pI : map JustNode argSigs) DGFormalParams

(morphSigs, dg'', diagA) <-

ana_FIT_ARG_UNITS lgraph dg' opts

uctx utrm pos argSigs fargus

let first (e, _, _) = e

second (_, e, _) = e

third (_, _, e) = e

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

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

DGFitSpec

-- compute morphA (\sigma^A)

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

let idI = mkG_morphism lidI (ext_ide lidI sigI)

morphA <- homogeneousMorManyUnion

(idI : (map first morphSigs))

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

(_, sigMorExt) <- extendMorphism (getSig sigF)

(getSig resultSig) (getSig sigA) morphA

-- check amalgamability conditions

let pIL = case pI of

JustDiagNode dn -> [dn]

_ -> []

sink <- inclusionSink lgraph (pIL ++

map third morphSigs) sigA

() <- assertAmalgamability opts pos diagA sink

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

extendDiagramIncl lgraph diagA pIL resultSig ""

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

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

ins diag0 dg0 ((morph, _, targetNode) : morphNodes) =

do (dnsig, diag1, dg1) <-

extendDiagramWithMorphismRev pos lgraph diag0

dg0 targetNode (gEmbed morph) argStr

DGFormalParams

diag'' <- insInclusionEdges lgraph diag1 [dnsig]

qB

ins diag'' dg1 morphNodes

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

-- check amalgamability conditions

(sigR, dg5) <- extendDGraph dg4 resultSig

(gEmbed sigMorExt) DGExtension

incSink <- inclusionSink lgraph (map third morphSigs) sigR

let sink' = (nqB, gEmbed sigMorExt) : incSink

assertAmalgamability opts pos diag'' sink'

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

(gEmbed sigMorExt) sigR utStr

diag4 <- insInclusionEdges lgraph diag'''

(map third morphSigs) q

return (q, diag4, dg5, utrm)

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

Group_unit_term ut poss -> do

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

ana_UNIT_TERM lgraph dg opts uctx (item ut)

return (dnsig, diag1, dg1, Group_unit_term (replaceAnnoted ut' ut) poss)

-- | Analyse unit arguments

ana_FIT_ARG_UNITS :: LogicGraph -> DGraph

-> HetcatsOpts -> ExtStUnitCtx -> UNIT_TERM

-- ^ the whole application for diagnostic purposes

-> Range

-- ^ the position of the application (for diagnostic purposes)

-> [NodeSig]

-- ^ the signatures of unit's formal parameters

-> [FIT_ARG_UNIT] -- ^ the arguments for the unit

-> Result ([(G_morphism, NodeSig, DiagNodeSig)], DGraph, Diag)

ana_FIT_ARG_UNITS lgraph dg opts uctx@(buc, diag)

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

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

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

ana_FIT_ARG_UNIT lgraph dg opts uctx nsig fau

(morphSigs, dg', diag') <- ana_FIT_ARG_UNITS lgraph dg1 opts

(buc, diag1) appl pos nsigs faus

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

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

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

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

++ showDoc appl "") pos

-- | Analyse unit argument

ana_FIT_ARG_UNIT :: LogicGraph -> DGraph

-> HetcatsOpts -> 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 dg opts uctx nsig

(Fit_arg_unit ut symbMap poss) = do

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

ana_UNIT_TERM lgraph dg opts uctx (item ut)

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

let adj = adjustPos 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 <- adj $ homogenizeGM (Logic lidS) symbMap

sigmaT' <- adj $ coerceSign lidT lidS "" sigmaT

mor <- if isStructured opts then return (ext_ide lidS sigmaS)

else do rmap <- adj $ stat_symb_map_items lid sis

rmap' <- adj $ coerceRawSymbolMap lid lidS "" rmap

adj $ ext_induced_from_to_morphism lidS rmap'

sigmaS sigmaT'

let gMorph = mkG_morphism lidS mor

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

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

-- | Analyse unit specification

ana_UNIT_SPEC :: LogicGraph

-> DGraph

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

-> MaybeNode -- ^ 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.

ana_UNIT_SPEC lgraph dg opts impsig usp = case usp of

Unit_type argSpecs resultSpec poss -> case argSpecs of

[] -> case resultSpec of

Annoted (Spec_inst spn [] _) _ _ _

| case lookupGlobalEnvDG spn dg of

Just (UnitEntry _) -> True

_ -> False ->

{- 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 dg opts impsig (Spec_name spn)

_ -> do -- a trivial unit type

(resultSpec', resultSig, dg') <- ana_SPEC False lgraph

dg impsig emptyNodeName opts (item resultSpec)

return (UnitSig resultSig, dg', Unit_type []

(replaceAnnoted resultSpec' resultSpec) poss)

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

(argSigs, dg1, argSpecs') <- ana_argSpecs lgraph dg opts argSpecs

(sigUnion, dg2) <- nodeSigUnion lgraph dg1

(impsig : map JustNode argSigs) DGFormalParams

(resultSpec', resultSig, dg3) <- ana_SPEC True lgraph

dg2 (JustNode sigUnion)

emptyNodeName opts (item resultSpec)

return (ParUnitSig argSigs resultSig, dg3, Unit_type argSpecs'

(replaceAnnoted resultSpec' resultSpec) poss)

Spec_name usn@(Token ustr pos) -> case lookupGlobalEnvDG usn dg of

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

_ -> fatal_error (ustr ++ " is not an unit specification") pos

Closed_unit_spec usp' _ -> do

curl <- lookupCurrentLogic "UNIT_SPEC" lgraph

ana_UNIT_SPEC lgraph dg opts (EmptyNode curl) usp'

-- | Analyse refinement specification

ana_REF_SPEC :: LogicGraph

-> DGraph

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

-> MaybeNode -- ^ the signature of imports

-> REF_SPEC -> Result (UnitSig, DGraph, REF_SPEC)

ana_REF_SPEC lgraph dg just_struct nsig rsp = case rsp of

Unit_spec asp -> do

(usig, dg', asp') <-

ana_UNIT_SPEC lgraph dg just_struct nsig asp

return (usig, dg', Unit_spec asp')

Arch_unit_spec asp poss -> do

(ArchSig _ usig, dg', asp') <-

ana_ARCH_SPEC lgraph dg just_struct (item asp)

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

-- dummy implementation for the rest

_ -> error "ana_REF_SPEC"

-- | Analyse a list of argument specifications

ana_argSpecs :: LogicGraph -> DGraph -> HetcatsOpts

-> [Annoted SPEC]

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

ana_argSpecs lgraph dg opts args = case args of

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

argSpec : argSpecs -> do

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

(argSpec', argSig, dg') <-

ana_SPEC False lgraph dg (EmptyNode l) emptyNodeName

opts (item argSpec)

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

ana_argSpecs lgraph dg' opts argSpecs

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

: argSpecs')

{- | Check that given diagram ensures amalgamability along given set

of morphisms -}

assertAmalgamability :: HetcatsOpts -- ^ the program options

-> Range -- ^ the position (for diagnostics)

-> Diag -- ^ the diagram to be checked

-> [(Node, GMorphism)] -- ^ the sink

-> Result ()

assertAmalgamability opts pos diag sink =

do ensAmalg <- homogeneousEnsuresAmalgamability opts pos diag sink

case ensAmalg of

Amalgamates -> return ()

NoAmalgamation msg -> plain_error ()

("Amalgamability is not ensured: " ++ msg) pos

DontKnow msg -> warning () msg pos

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

homogeneousEnsuresAmalgamability :: HetcatsOpts -- ^ the program options

-> Range -- ^ the position (for diagnostics)

-> Diag -- ^ the diagram to be checked

-> [(Node, GMorphism)] -- ^ the sink

-> Result Amalgamates

homogeneousEnsuresAmalgamability opts pos diag sink =

do case sink of

[] -> plain_error defaultDontKnow

"homogeneousEnsuresAmalgamability: Empty sink" pos

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

sig = cod Grothendieck mor

G_sign lid _ _<- return sig

hDiag <- homogeniseDiagram lid diag

hSink <- homogeniseSink lid sink

ensures_amalgamability lid (caslAmalg opts,

hDiag, hSink, (diagDesc diag))

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

getPos_UNIT_TERM :: UNIT_TERM -> Range

getPos_UNIT_TERM ut = case ut of

Unit_reduction _ restr -> case restr of

-- obtain position from RESTRICTION

(Hidden _ poss) -> poss

(Revealed _ poss) -> poss

Unit_translation _ (Renaming _ poss) -> poss

Amalgamation _ poss -> poss

Local_unit _ _ poss -> poss

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

Group_unit_term _ poss -> poss

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

getPos_UNIT_IMPORTED :: Range -> Range

getPos_UNIT_IMPORTED (Range ps) = Range $ case ps of

[] -> []

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

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

getPos_UNIT_EXPRESSION :: UNIT_EXPRESSION -> Range

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

appRange (getPos_UNIT_TERM ut) poss