{- |

Module : $Header$

Author : Maciek Makowski

Year : 2004

Copyright : (c) Maciek Makowski, Warsaw University 2004

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

Maintainer : hets@tzi.de

Stability : provisional

Portability : non-portable (via imports)

Analysis of architectural specifications.

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

of the CASL Reference Manual.

-}

module Static.AnalysisArchitecture (ana_ARCH_SPEC, ana_UNIT_SPEC)

where

import Driver.Options

import Logic.Logic

import Logic.Grothendieck

import Static.DevGraph

import Static.ArchDiagram

import Static.AnalysisStructured

import Syntax.Print_AS_Architecture

import Syntax.AS_Architecture

import Syntax.AS_Structured

import Common.AS_Annotation

import Common.Id

import Common.Result

import Common.Amalgamate

import Common.PrettyPrint

import qualified Common.Lib.Map as Map

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

-- | Analyse an architectural specification

-- @

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

-- @

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

-> GlobalContext -> AnyLogic -- ^ current logic

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

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

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

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

-- BASIC-ARCH-SPEC

ana_ARCH_SPEC lgraph defl gctx@(gannos, genv, _) curl opts (Basic_arch_spec udd uexpr pos) =

do (uctx, dg', udd') <- ana_UNIT_DECL_DEFNS lgraph defl gctx curl opts udd

(_, usig, _, dg'', uexpr') <- ana_UNIT_EXPRESSION lgraph defl (gannos, genv, dg') curl opts uctx (item uexpr)

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

-- GROUP-ARCH-SPEC

ana_ARCH_SPEC lgraph defl gctx curl opts (Group_arch_spec asp _) =

ana_ARCH_SPEC lgraph defl gctx curl opts (item asp)

-- ARCH-SPEC-NAME

ana_ARCH_SPEC _ defl (_, genv, dg) _ _ asp@(Arch_spec_name asn@(Token _ pos)) =

do case Map.lookup asn genv of

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

("Undefined architectural specification " ++ showPretty asn "")

pos

Just (ArchEntry asig) -> return (asig, dg, asp)

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

((showPretty asn "") ++ " is not an architectural specification")

pos

-- | Analyse a list of unit declarations and definitions

ana_UNIT_DECL_DEFNS :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic

-> HetcatsOpts -> [Annoted UNIT_DECL_DEFN]

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

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

-- 3. possibly modified list of unit declarations and definitions

ana_UNIT_DECL_DEFNS lgraph defl gctx curl opts udds =

ana_UNIT_DECL_DEFNS' lgraph defl gctx curl opts emptyExtStUnitCtx udds

ana_UNIT_DECL_DEFNS' :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic -> HetcatsOpts

-> ExtStUnitCtx -> [Annoted UNIT_DECL_DEFN]

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

ana_UNIT_DECL_DEFNS' _ _ (_, _, dg) _ _ uctx [] =

do return (uctx, dg, [])

ana_UNIT_DECL_DEFNS' lgraph defl gctx@(gannos, genv, _) curl opts uctx (udd : udds) =

do (uctx', dg', udd') <- ana_UNIT_DECL_DEFN lgraph defl gctx curl opts uctx (item udd)

(uctx'', dg'', udds') <- ana_UNIT_DECL_DEFNS' lgraph defl (gannos, genv, dg') curl opts uctx' udds

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

-- | Analyse unit refs

ana_UNIT_REF :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic

-> HetcatsOpts -> ExtStUnitCtx -> UNIT_REF -> Result (ExtStUnitCtx, DGraph, UNIT_REF)

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

-- 3. possibly modified UNIT_DECL_DEFN

-- unit declaration

ana_UNIT_REF lgraph defl gctx@(gannos, genv, _) curl opts

uctx@(buc, _) (Unit_ref un@(Token _ unpos) usp pos) =

do (dns, diag', dg', uts') <- ana_UNIT_IMPORTED lgraph defl gctx curl opts uctx pos []

let impSig = getSigFromDiag dns

(usig, dg'', usp') <- ana_REF_SPEC lgraph defl (gannos, genv, dg') curl opts impSig usp

let ud' = Unit_ref un usp' pos

if Map.member un buc

then

plain_error (uctx, dg'', ud')

("Unit " ++ showPretty un " already declared/defined")

unpos

else

case usig of

Par_unit_sig (argSigs, resultSig) ->

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

let basedParUSig = Based_par_unit_sig (dns, (argSigs, resultSig'))

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

Unit_sig nsig ->

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

(dn', diag'') <- extendDiagramIncl lgraph diag' [dns] nsig' (renderText Nothing (printText un))

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

-- | Analyse unit declaration or definition

ana_UNIT_DECL_DEFN :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic

-> HetcatsOpts -> ExtStUnitCtx -> UNIT_DECL_DEFN -> Result (ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)

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

-- 3. possibly modified UNIT_DECL_DEFN

-- unit declaration

ana_UNIT_DECL_DEFN lgraph defl gctx@(gannos, genv, _) curl opts

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

do (dns, diag', dg', uts') <- ana_UNIT_IMPORTED lgraph defl gctx curl opts uctx pos uts

let impSig = getSigFromDiag dns

(usig, dg'', usp') <- ana_REF_SPEC lgraph defl (gannos, genv, dg') curl opts impSig usp

let ud' = Unit_decl un usp' uts' pos

if Map.member un buc

then

plain_error (uctx, dg'', ud')

("Unit " ++ showPretty un " already declared/defined")

unpos

else

case usig of

Par_unit_sig (argSigs, resultSig) ->

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

let basedParUSig = Based_par_unit_sig (dns, (argSigs, resultSig'))

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

Unit_sig nsig ->

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

(dn', diag'') <- extendDiagramIncl lgraph diag' [dns] nsig' (renderText Nothing (printText un))

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

-- unit definition

ana_UNIT_DECL_DEFN lgraph defl gctx curl opts uctx@(buc, _)

(Unit_defn un@(Token _ unpos) uexp poss) =

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

let ud' = Unit_defn un uexp' poss

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

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

if Map.member un buc

then

plain_error (uctx, dg', ud')

("Unit " ++ showPretty un " already defined/declared")

unpos

else

case usig of

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

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

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

dg', ud')

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

dg', ud')

-- | Analyse unit imports

ana_UNIT_IMPORTED :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic

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

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

ana_UNIT_IMPORTED _ _ (_, _, dg) curl _ (_, diag) _ [] =

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

ana_UNIT_IMPORTED lgraph defl gctx curl opts uctx poss terms =

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

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

-- check amalgamability conditions

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

let pos = getPos_UNIT_IMPORTED poss

sink <- inclusionSink lgraph dnsigs sig

() <- assertAmalgamability opts pos diag' sink

(dnsig, diag'') <- extendDiagramIncl lgraph diag' dnsigs sig (renderText Nothing (printText terms))

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

ana_UNIT_IMPORTED' :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic

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

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

ana_UNIT_IMPORTED' _ _ (_, _, dg) _ _ (_, diag) [] =

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

ana_UNIT_IMPORTED' lgraph defl gctx@(gannos, genv, _) curl opts uctx@(buc, _) (ut : uts) =

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

(dnsigs, diag'', dg'', uts') <- ana_UNIT_IMPORTED' lgraph defl (gannos, genv, dg') curl opts (buc, diag') uts

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

-- | Analyse an unit expression

ana_UNIT_EXPRESSION :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic

-> HetcatsOpts -> ExtStUnitCtx -> UNIT_EXPRESSION

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

ana_UNIT_EXPRESSION lgraph defl gctx curl opts uctx (Unit_expression [] ut poss) =

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

return (dnsig, Unit_sig (getSigFromDiag dnsig), diag', dg',

Unit_expression [] (replaceAnnoted ut' ut) poss)

ana_UNIT_EXPRESSION lgraph defl gctx@(gannos, genv, _) curl opts

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

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

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

-- build the extended diagram and new based unit context

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

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

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

{- 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) buc

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

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

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

(_, diag'') <- extendDiagramIncl lgraph diag' pardnsigs resnsig (renderText Nothing (printText exp))

-- analyse the unit term

(p@(Diag_node_sig _ pnsig), diag''', dg''', ut') <- ana_UNIT_TERM lgraph defl (gannos, genv, dg'')

curl opts (buc', diag'') (item ut)

-- check amalgamability conditions

let pos = getPos_UNIT_EXPRESSION exp

checkSubSign [] _ = True

checkSubSign (dnsub : dnsigs) nsup =

if is_subgsign (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

(z, diag4) <- extendDiagramIncl lgraph diag''' [] (EmptyNode curl) (renderText Nothing (printText exp))

return (z, Par_unit_sig (map snd args, getSigFromDiag p), diag4, dg''',

Unit_expression ubs' (replaceAnnoted ut' ut) poss)

else -- report an error

do (z, diag4) <- extendDiagramIncl lgraph diag''' [] (EmptyNode curl) (renderText Nothing (printText exp))

plain_error (z, Par_unit_sig (map snd args, getSigFromDiag p), diag4, dg''',

Unit_expression ubs' (replaceAnnoted ut' ut) poss)

("The body signature does not extend the parameter signatures in\n" ++ (showPretty exp ""))

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 -> AnyLogic -> GlobalContext -> AnyLogic

-> HetcatsOpts -> ExtStUnitCtx -> [UNIT_BINDING]

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

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

do return ([], dg, [])

ana_UNIT_BINDINGS lgraph defl gctx@(gannos, genv, _) curl opts uctx@(buc, _)

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

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

let ub' = Unit_binding un usp' poss

case usig of

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

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

unpos

Unit_sig nsig ->

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

let args' = (un, nsig) : args

if Map.member un buc

then

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

("Unit " ++ showPretty un " already declared/defined")

unpos

else

case lookup un args of

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

("Unit " ++ showPretty un " already declared/defined")

unpos

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

-- | Analyse a list of unit terms

ana_UNIT_TERMS :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic

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

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

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

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

ana_UNIT_TERMS lgraph defl gctx@(gannos, genv, _) curl opts uctx@(buc, _) (ut : uts) =

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

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

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

-- | Analyse an unit term

ana_UNIT_TERM :: LogicGraph -> AnyLogic -> GlobalContext -> AnyLogic

-> HetcatsOpts -> ExtStUnitCtx -> UNIT_TERM

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

-- UNIT-REDUCTION

ana_UNIT_TERM lgraph defl gctx curl opts uctx red@(Unit_reduction ut restr) =

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

(incl, msigma) <- ana_RESTRICTION dg (emptyG_sign curl) (getSig (getSigFromDiag p)) opts restr

let pos = getPos_UNIT_TERM red

(q@(Diag_node_sig qn _), diag', dg') <- extendDiagramWithMorphismRev pos lgraph diag dg p incl

(renderText Nothing (printText red))

(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

do 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

(renderText Nothing (printText red))

(case restr of

(Hidden _ _) -> DGHiding

(Revealed _ _) -> DGRevealing)

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

-- UNIT-TRANSLATION

ana_UNIT_TERM lgraph defl gctx curl opts uctx tr@(Unit_translation ut ren) =

do (dnsig@(Diag_node_sig p _), diag, dg, ut') <- ana_UNIT_TERM lgraph defl gctx curl opts uctx (item ut)

gMorph <- ana_RENAMING lgraph (getSig (getSigFromDiag dnsig)) opts ren

let pos = getPos_UNIT_TERM tr

sink = [(p, gMorph)]

-- check amalamability conditions

() <- assertAmalgamability opts pos diag sink

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

(renderText Nothing (printText tr))

DGTranslation

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

-- AMALGAMATION

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

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

-- compute sigma

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

-- check amalgamability conditions

sink <- inclusionSink lgraph dnsigs sig

() <- assertAmalgamability opts poss diag sink

(q, diag') <- extendDiagramIncl lgraph diag dnsigs sig (renderText Nothing (printText am))

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

-- LOCAL-UNIT

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

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

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

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

-- UNIT-APPL

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

uappl@(Unit_appl un fargus _) =

do let pos = getPos_UNIT_TERM uappl

case Map.lookup un buc of

Just (Based_unit_sig dnsig) ->

do case fargus of

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

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

do plain_error (dnsig, diag, dg, uappl)

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

showPretty fargus "")

pos

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

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

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

uappl pos argSigs fargus

let first (e, _, _) = e

second (_, e, _) = e

third (_, _, e) = e

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

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

DGFitSpec

-- compute morphA (\sigma^A)

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

let idI = G_morphism lidI (ide lidI sigI)

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

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

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

-- check amalgamability conditions

sink <- inclusionSink lgraph (pI : (map third morphSigs)) sigA

() <- assertAmalgamability opts pos diagA sink

(qB@(Diag_node_sig nqB _), diag') <- extendDiagramIncl lgraph diagA [pI] resultSig ""

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

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

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

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

dg targetNode (gEmbed morph)

(renderText Nothing (printText fargus))

DGFormalParams

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

ins diag'' dg' morphNodes

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

-- check amalgamability conditions

(sigR, dg5) <- extendDGraph dg4 resultSig (gEmbed sigMorExt) DGExtension

sink <- inclusionSink lgraph (map third morphSigs) sigR

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

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

(q, diag''') <- extendDiagram diag'' qB (gEmbed sigMorExt) sigR

(renderText Nothing (printText uappl))

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

return (q, diag4, dg5, uappl)

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

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

pos

-- group unit term

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

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

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

-- | Analyse unit arguments

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

-> HetcatsOpts -> ExtStUnitCtx

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

-> [Pos] -- ^ the position of the application (for diagnostic purposes)

-> [NodeSig] -- ^ the signatures of unit's formal parameters

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

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

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

do return ([], dg, diag)

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

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

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

uctx nsig fau

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

(buc, diag) appl pos nsigs faus

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

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

do plain_error ([], dg, diag)

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

pos

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

do plain_error ([], dg, diag)

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

pos

-- | Analyse unit argument

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

-> 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 defl gctx curl opts uctx nsig (Fit_arg_unit ut symbMap poss) =

do (p, diag', dg', _) <- ana_UNIT_TERM lgraph defl gctx curl 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' <- rcoerce lidT lidS poss sigmaT

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

else do rmap <- adj $ stat_symb_map_items lid sis

rmap' <- rcoerce lid lidS poss rmap

adj $ induced_from_to_morphism lidS rmap' sigmaS sigmaT'

let gMorph = G_morphism lidS mor

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

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

-- | Analyse unit specification

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

-> GlobalContext -> AnyLogic -- ^ current logic

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

-> NodeSig -- ^ the signature of imports

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

-- ^ returns 1. unit signature 2. the development graph resulting from

-- structred specs inside the unit spec and 3. a UNIT_SPEC after possible

-- conversions.

-- UNIT-TYPE

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

should be converted to a Spec_name -}

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

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

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

_ -> False =

ana_UNIT_SPEC lgraph defl gctx curl just_struct impsig (Spec_name spn)

-- a trivial unit type

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

do (resultSpec', resultSig, dg') <- ana_SPEC lgraph gctx impsig Static.DevGraph.emptyName

just_struct (item resultSpec)

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

-- a non-trivial unit type

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

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

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

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

Static.DevGraph.emptyName opts (item resultSpec)

return (Par_unit_sig (argSigs, resultSig), dg3,

Unit_type argSpecs' (replaceAnnoted resultSpec' resultSpec) poss)

-- SPEC-NAME (an alias)

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

do case Map.lookup usn genv of

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

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

pos

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

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

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

pos

-- CLOSED-UNIT-SPEC

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

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

-- | Analyse refinement specification

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

-> GlobalContext -> AnyLogic -- ^ current logic

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

-> NodeSig -- ^ the signature of imports

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

-- UNIT-SPEC

ana_REF_SPEC lgraph defl gctx curl just_struct nsig (Unit_spec asp) =

do (usig, dg', asp') <- ana_UNIT_SPEC lgraph defl gctx curl just_struct nsig asp

return (usig, dg', Unit_spec asp')

-- ARCH-UNIT-SPEC

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

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

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

-- dummy implementation for the rest

ana_REF_SPEC lgraph defl gctx@(_,_,dg) curl just_struct nsig rsp =

return (Unit_sig nsig,dg,rsp)

-- | Analyse a list of argument specifications

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

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

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

do return ([], dg, [])

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

do (argSpec', argSig, dg') <- ana_SPEC lgraph gctx (EmptyNode defl) Static.DevGraph.emptyName

opts (item argSpec)

(argSigs, dg'', argSpecs') <- ana_argSpecs lgraph defl (gannos, genv, 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

-> [Pos] -- ^ 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

-> [Pos] -- ^ 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

-> [Pos]

-- UNIT-REDUCTION

getPos_UNIT_TERM (Unit_reduction _ restr) =

-- obtain position from RESTRICTION

case restr of

(Hidden _ poss) -> poss

(Revealed _ poss) -> poss

-- UNIT-TRANSLATION

getPos_UNIT_TERM (Unit_translation _ (Renaming _ poss)) =

poss

-- AMALGAMATION

getPos_UNIT_TERM (Amalgamation _ poss) =

poss

-- LOCAL-UNIT

getPos_UNIT_TERM (Local_unit _ _ poss) =

poss

-- UNIT-APPLICATION

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

unpos

-- GROUP-UNIT-TERM

getPos_UNIT_TERM (Group_unit_term _ poss) =

poss

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

getPos_UNIT_IMPORTED :: [Pos] -> [Pos]

getPos_UNIT_IMPORTED ps = 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 -> [Pos]

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

getPos_UNIT_TERM ut

getPos_UNIT_EXPRESSION (Unit_expression _ _ poss) =

poss