5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder{- |

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederModule : $Header$

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederDescription : static analysis of CASL architectural specifications

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

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederMaintainer : till@informatik.uni-bremen.de

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksaStability : provisional

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederPortability : non-portable (via imports)

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederStatic analysis of CASL architectural specifications

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

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder of the CASL Reference Manual.

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-}

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder

75067b1beba1380cde707c30e7fc050d86f6927fKarl Lucmodule Static.AnalysisArchitecture

7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc ( anaArchSpec

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , anaUnitSpec

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , anaUnitRef

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder ) where

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Driver.Options

e036e115761fe7c09c210c337440a1864d794093Martha Rohte

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Logic.Logic

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Logic.ExtSign

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Logic.Coerce

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Logic.Grothendieck

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Static.GTheory

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Static.DevGraph

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Static.ArchDiagram

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Static.AnalysisStructured

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Syntax.Print_AS_Architecture ()

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Syntax.AS_Architecture

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Syntax.AS_Structured

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksaimport Common.AS_Annotation

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Common.Id

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Common.Result

7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Lucimport Common.Amalgamate

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Common.DocUtils

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport qualified Data.Map as Map

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Data.Graph.Inductive.Graph as Graph (Node)

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- | Analyse an architectural specification

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- @

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- ARCH-SPEC ::= BASIC-ARCH-SPEC | GROUP-ARCH-SPEC | ARCH-SPEC-NAME

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- @

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederanaArchSpec :: LogicGraph -> DGraph

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

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder -> ARCH_SPEC -> Result (ArchSig, DGraph, ARCH_SPEC)

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

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder2. development graph resulting from structured specs within the arch

656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maederspec and 3. ARCH_SPEC after possible conversions -}

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederanaArchSpec lgraph dg opts archSp = case archSp of

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa Basic_arch_spec udd uexpr pos ->

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa do (uctx, dg', udd') <- anaUnitDeclDefns lgraph dg opts udd

7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc (_, usig, _, dg'', uexpr') <-

7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc anaUnitExpression lgraph dg' opts uctx (item uexpr)

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

656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder (replaceAnnoted uexpr' uexpr) pos)

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder Group_arch_spec asp _ -> anaArchSpec lgraph dg opts (item asp)

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

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

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder _ -> fatal_error (astr ++

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder " is not an architectural specification") pos

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- | Analyse a list of unit declarations and definitions

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederanaUnitDeclDefns :: LogicGraph -> DGraph

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder -> HetcatsOpts -> [Annoted UNIT_DECL_DEFN]

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

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

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederdevelopment graph 3. possibly modified list of unit declarations and

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederdefinitions -}

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederanaUnitDeclDefns lgraph dg opts =

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder anaUnitDeclDefns' lgraph dg opts emptyExtStUnitCtx

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederanaUnitDeclDefns' :: LogicGraph -> DGraph

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder -> HetcatsOpts -> ExtStUnitCtx -> [Annoted UNIT_DECL_DEFN]

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

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederanaUnitDeclDefns' lgraph dg opts uctx uds = case uds of

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder udd : udds -> do

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder (uctx', dg', udd') <-

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa anaUnitDeclDefn lgraph dg opts uctx (item udd)

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder (uctx'', dg'', udds') <-

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder anaUnitDeclDefns' lgraph dg' opts uctx' udds

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

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder [] -> return (uctx, dg, [])

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederalreadyDefinedUnit :: SIMPLE_ID -> String

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederalreadyDefinedUnit u = "Unit " ++ tokStr u ++ " already declared/defined"

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- | Create a node that represents a union of signatures

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaedernodeSigUnion :: LogicGraph -> DGraph -> [MaybeNode] -> DGOrigin

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder -> Result (NodeSig, DGraph)

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaedernodeSigUnion lgraph dg nodeSigs orig =

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

e9e5281899ddaec4778ad14c64800975377630ecChristian Maeder $ map getMaybeSig nodeSigs

e9e5281899ddaec4778ad14c64800975377630ecChristian Maeder let nodeContents = newNodeLab emptyNodeName orig

e036e115761fe7c09c210c337440a1864d794093Martha Rohte $ noSensGTheory lid sigU ind

e9e5281899ddaec4778ad14c64800975377630ecChristian Maeder node = getNewNodeDG dg

e9e5281899ddaec4778ad14c64800975377630ecChristian Maeder dg' = insNodeDG (node, nodeContents) dg

e9e5281899ddaec4778ad14c64800975377630ecChristian Maeder inslink dgres nsig = do

e9e5281899ddaec4778ad14c64800975377630ecChristian Maeder dgv <- dgres

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder case nsig of

2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa EmptyNode _ -> dgres

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder JustNode (NodeSig n sig) -> do

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa incl <- ginclusion lgraph sig sigUnion

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa return $ insLEdgeNubDG

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa (n, node, globDefLink incl SeeTarget) dgv

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder dg'' <- foldl inslink (return dg') nodeSigs

2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa return (NodeSig node sigUnion, dg'')

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa-- | Analyse unit refs

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksaanaUnitRef :: LogicGraph -> DGraph

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa -> HetcatsOpts -> ExtStUnitCtx -> UNIT_REF

2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa -> Result (ExtStUnitCtx, DGraph, UNIT_REF)

2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa{- ^ returns 1. extended static unit context 2. possibly modified

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksadevelopment graph 3. possibly modified UNIT_DECL_DEFN -}

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa-- unit declaration

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksaanaUnitRef lgraph dg opts

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa uctx@(buc, _) (Unit_ref un usp pos) =

2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa do (dns, diag', dg', _) <-

2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa anaUnitImported lgraph dg opts uctx pos []

2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa let impSig = toMaybeNode dns

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa (usig, dg'', usp') <-

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa anaRefSpec lgraph dg' opts impSig usp

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa insertBasedUnit lgraph dg'' usig (buc, diag') dns un

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa $ Unit_ref un usp' pos

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksainsertBasedUnit :: LogicGraph -> DGraph -> UnitSig -> ExtStUnitCtx

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa -> MaybeDiagNode -> UNIT_NAME -> a

ea570f40967ef8bc16b76c54f9b867a8036cc750Soeren D. Schulze -> Result (ExtStUnitCtx, DGraph, a)

ea570f40967ef8bc16b76c54f9b867a8036cc750Soeren D. SchulzeinsertBasedUnit lgraph dg'' usig uctx@(buc, diag') dns un@(Token ustr unpos)

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa ud' =

d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulze if Map.member un buc

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa then plain_error (uctx, dg'', ud') (alreadyDefinedUnit un) unpos

d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulze else case usig of

d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulze UnitSig argSigs resultSig -> do

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa let impSig = toMaybeNode dns

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa (resultSig', dg''') <- nodeSigUnion lgraph dg''

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa (JustNode resultSig : [impSig]) DGImports

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa (basedParUSig, diag''') <- if null argSigs then do

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

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa (case dns of

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa JustDiagNode dn -> [dn]

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa _ -> []) resultSig' ustr

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa return (Based_unit_sig dn', diag'')

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa else return (Based_par_unit_sig dns $

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa UnitSig argSigs resultSig', diag')

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa return ((Map.insert un basedParUSig buc, diag'''),

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa dg''', ud')

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa

f03aa0b723e5545fddf7019e287368b9e208ca69Soeren D. Schulze-- | Analyse unit declaration or definition

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksaanaUnitDeclDefn :: LogicGraph -> DGraph

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa -> HetcatsOpts -> ExtStUnitCtx -> UNIT_DECL_DEFN

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa -> Result (ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa{- ^ returns 1. extended static unit context 2. possibly modified

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksadevelopment graph 3. possibly modified UNIT_DECL_DEFN -}

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksaanaUnitDeclDefn lgraph dg opts uctx@(buc, _) udd = case udd of

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa Unit_decl un usp uts pos -> do

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

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa anaUnitImported lgraph dg opts uctx pos uts

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa let impSig = toMaybeNode dns

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa (usig, dg'', usp') <-

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa anaRefSpec lgraph dg' opts impSig usp

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa insertBasedUnit lgraph dg'' usig (buc, diag') dns un

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder $ Unit_decl un usp' uts' pos

0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa Unit_defn un uexp poss -> do

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder (p, usig, diag, dg', uexp') <-

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder anaUnitExpression lgraph dg opts uctx uexp

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder let ud' = Unit_defn un uexp' poss

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

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder don't need to convert the ExtStUnitCtx to StUnitCtx as the

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder domain will be preserved -}

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa if Map.member un buc then

a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa plain_error (uctx, dg', ud') (alreadyDefinedUnit un) $ tokPos un

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder else case usig of

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder {- we can use Map.insert as there are no mappings for

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder un in ps and bs (otherwise there would have been a

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder mapping in (ctx uctx)) -}

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder UnitSig args _ -> if null args then case p of

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder JustDiagNode dn -> return ((Map.insert un

0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa (Based_unit_sig dn) buc, diag), dg', ud')

0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa _ -> error "anaUnitDeclDefn"

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder else return ((Map.insert un

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder (Based_par_unit_sig p usig) buc

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , diag), dg', ud')

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- | Analyse unit imports

5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederanaUnitImported :: LogicGraph -> DGraph

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

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

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

case terms of

[] -> do

curl <- lookupCurrentLogic "UnitImported" lgraph

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

_ -> do

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

anaUnitImported' lgraph dg opts uctx terms

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

(map (JustNode . getSigFromDiag) dnsigs) DGImports

-- check amalgamability conditions

{- let incl s = propagateErrors (ginclusion lgraph (getSig

(getSigFromDiag s)) (getSig sig)) -}

let pos = getPosUnitImported poss

sink <- inclusionSink lgraph dnsigs sig

() <- assertAmalgamability opts pos diag' sink

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

sig $ showDoc terms ""

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

anaUnitImported' :: LogicGraph -> DGraph

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

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

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

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

ut : uts -> do

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

anaUnitTerm lgraph dg opts uctx (item ut)

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

anaUnitImported' lgraph dg' opts (buc, diag') uts

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

-- | Analyse an unit expression

anaUnitExpression :: LogicGraph -> DGraph

-> HetcatsOpts -> ExtStUnitCtx -> UNIT_EXPRESSION

-> Result (MaybeDiagNode, UnitSig, Diag, DGraph, UNIT_EXPRESSION)

anaUnitExpression lgraph dg opts uctx@(buc, diag)

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

[] -> do

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

anaUnitTerm lgraph dg opts uctx (item ut)

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

Unit_expression [] (replaceAnnoted ut' ut) poss)

_ -> do

(args, dg', ubs') <-

anaUnitBindings lgraph dg opts uctx ubs

(resnsig, _dg'') <- nodeSigUnion lgraph dg'

(map (JustNode . snd) args) DGFormalParams

-- build the extended diagram and new based unit context

let dexp = showDoc uexp ""

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

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

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

nsig dexp

{- we made sure in anaUnitBindings 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') <-

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

-- check amalgamability conditions

let pos = getPosUnitExpression uexp

checkSubSign dnsigs nsup =

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

$ getSig nsup) dnsigs

-- check that signatures in pardnsigs are subsignatures of pnsig

if checkSubSign pardnsigs pnsig

then

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

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

-- add new node to the diagram

curl <- lookupCurrentLogic "UnitExpression" lgraph

return (EmptyDiagNode curl, UnitSig (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. -}

anaUnitBindings :: LogicGraph -> DGraph

-> HetcatsOpts -> ExtStUnitCtx -> [UNIT_BINDING]

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

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

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

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

curl <- lookupCurrentLogic "UnitBindings" lgraph

(usig, dg', usp') <-

anaUnitSpec lgraph dg opts (EmptyNode curl) usp

let ub' = Unit_binding un usp' poss

case usig of

UnitSig ups nsig -> if not $ null ups then

plain_error ([], dg', [])

("An argument unit " ++

ustr ++ " must not be parameterized") unpos

else

do (args, dg'', ubs') <- anaUnitBindings 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

anaUnitTerms :: LogicGraph -> DGraph

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

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

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

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

ut : uts -> do

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

anaUnitTerm lgraph dg opts uctx (item ut)

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

dg' opts (buc, diag') uts

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

-- | Analyse an unit term

anaUnitTerm :: LogicGraph -> DGraph -> HetcatsOpts -> ExtStUnitCtx

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

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

let pos = getPosUnitTerm utrm

utStr = showDoc utrm ""

in case utrm of

Unit_reduction ut restr -> do

let orig = DGRestriction $ Restricted restr

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

anaUnitTerm lgraph dg opts uctx (item ut)

curl <- lookupCurrentLogic "UnitTerm" lgraph

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

(getSig (getSigFromDiag p)) opts restr

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

extendDiagramWithMorphismRev pos lgraph diag1 dg1 p incl utStr

orig

case msigma of

Nothing ->

{- the renaming morphism is just identity, so

there's no need to extend the diagram -}

return (q, diag', dg',

Unit_reduction (replaceAnnoted ut' ut) restr)

Just sigma ->

do

-- check amalgamability conditions

let sink = [(qn, sigma)]

() <- assertAmalgamability opts pos diag' sink

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

lgraph diag' dg' q sigma utStr orig

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

Unit_reduction

(replaceAnnoted ut' ut) restr)

Unit_translation ut ren -> do

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

anaUnitTerm lgraph dg opts uctx (item ut)

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

gMorph <- anaRenaming lgraph

(EmptyNode $ error "Static.AnalysisArchitecture")

(getSig (getSigFromDiag dnsig)) opts ren

let sink = [(p, gMorph)]

-- check amalamability conditions

() <- assertAmalgamability opts pos diag1 sink

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

diag1 dg1 dnsig gMorph utStr

(DGTranslation $ Renamed ren)

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

(replaceAnnoted ut' ut) ren)

Amalgamation uts poss -> do

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

anaUnitTerms 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') <-

anaUnitDeclDefns' lgraph dg opts uctx udds

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

anaUnitTerm 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 (UnitSig argSigs resultSig)) ->

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

(toMaybeNode pI : map JustNode argSigs) DGFormalParams

(morphSigs, dg'', diagA) <-

anaFitArgUnits 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 sigI)

morphA <- homogeneousMorManyUnion

$ idI : map first morphSigs

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

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

(getSig resultSig) (getSig sigA) morphA

-- check amalgamability conditions

let sigMorExt = gEmbed gSigMorExt

pIL = case pI of

JustDiagNode dn -> [dn]

_ -> []

sink <- inclusionSink lgraph (pIL ++

map third morphSigs) sigA

() <- assertAmalgamability opts pos diagA sink

(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

sigMorExt DGExtension

incSink <- inclusionSink lgraph (map third morphSigs) sigR

let sink' = (nqB, sigMorExt) : incSink

assertAmalgamability opts pos diag'' sink'

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

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') <-

anaUnitTerm lgraph dg opts uctx (item ut)

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

-- | Analyse unit arguments

anaFitArgUnits :: 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)

anaFitArgUnits lgraph dg opts uctx@(buc, diag)

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

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

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

anaFitArgUnit lgraph dg opts uctx nsig fau

(morphSigs, dg', diag') <- anaFitArgUnits 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

anaFitArgUnit :: 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

anaFitArgUnit lgraph dg opts uctx nsig

(Fit_arg_unit ut symbMap poss) = do

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

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

anaUnitSpec :: 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.

anaUnitSpec 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 -}

anaUnitSpec lgraph dg opts impsig (Spec_name spn)

_ -> do -- a trivial unit type

(resultSpec', resultSig, dg') <- anaSpec 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') <- anaArgSpecs lgraph dg opts argSpecs

(sigUnion, dg2) <- nodeSigUnion lgraph dg1

(impsig : map JustNode argSigs) DGFormalParams

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

dg2 (JustNode sigUnion)

emptyNodeName opts (item resultSpec)

return (UnitSig 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 "UnitSpec" lgraph

anaUnitSpec lgraph dg opts (EmptyNode curl) usp'

-- | Analyse refinement specification

anaRefSpec :: LogicGraph -> DGraph

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

-> MaybeNode -- ^ the signature of imports

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

anaRefSpec lgraph dg just_struct nsig rsp = case rsp of

Unit_spec asp -> do

(usig, dg', asp') <-

anaUnitSpec lgraph dg just_struct nsig asp

return (usig, dg', Unit_spec asp')

Arch_unit_spec asp poss -> do

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

anaArchSpec lgraph dg just_struct (item asp)

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

-- dummy implementation for the rest

_ -> error "anaRefSpec"

-- | Analyse a list of argument specifications

anaArgSpecs :: LogicGraph -> DGraph -> HetcatsOpts

-> [Annoted SPEC]

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

anaArgSpecs lgraph dg opts args = case args of

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

argSpec : argSpecs -> do

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

(argSpec', argSig, dg') <-

anaSpec False lgraph dg (EmptyNode l) emptyNodeName

opts (item argSpec)

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

anaArgSpecs 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 = case sink of

[] -> plain_error defaultDontKnow

"homogeneousEnsuresAmalgamability: Empty sink" pos

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

sig = cod mor

G_sign lid _ _<- return sig

hDiag <- homogeniseDiagram lid diag

hSink <- homogeniseSink lid sink

ensures_amalgamability lid (caslAmalg opts,

hDiag, hSink, (diagDesc diag))

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

getPosUnitTerm :: UNIT_TERM -> Range

getPosUnitTerm ut = case ut of

Unit_reduction _ restr -> case restr of

-- obtain position from RESTRICTION

Hidden _ poss -> poss

Revealed _ poss -> poss

Unit_translation _ (Renaming _ poss) -> poss

Amalgamation _ poss -> poss

Local_unit _ _ poss -> poss

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

Group_unit_term _ poss -> poss

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

getPosUnitImported :: Range -> Range

getPosUnitImported (Range ps) = Range $ case ps of

[] -> []

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

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

getPosUnitExpression :: UNIT_EXPRESSION -> Range

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

appRange (getPosUnitTerm ut) poss