d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder{- |

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederModule : $Header$

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederDescription : static analysis of CASL architectural specifications

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

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

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederMaintainer : till@informatik.uni-bremen.de

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederStability : provisional

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederPortability : non-portable (via imports)

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederStatic analysis of CASL architectural specifications

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

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder of the CASL Reference Manual.

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder-}

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maedermodule Static.AnalysisArchitecture

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder ( anaArchSpec

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder , anaUnitSpec

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder , anaUnitRef

e84c877ad38ce9312eab222a79f44da2015572d2Christian Maeder ) where

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maederimport Driver.Options

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maederimport Logic.Logic

945e82ed7877917f3ab1657f555e71991372546aChristian Maederimport Logic.ExtSign

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Logic.Coerce

945e82ed7877917f3ab1657f555e71991372546aChristian Maederimport Logic.Grothendieck

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Static.GTheory

d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian Maederimport Static.DevGraph

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Static.ArchDiagram

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Static.AnalysisStructured

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Syntax.Print_AS_Architecture ()

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Syntax.AS_Architecture

945e82ed7877917f3ab1657f555e71991372546aChristian Maederimport Syntax.AS_Structured

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Common.AS_Annotation

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Common.Id

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maederimport Common.Result

945e82ed7877917f3ab1657f555e71991372546aChristian Maederimport Common.Amalgamate

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Common.DocUtils

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maederimport qualified Data.Map as Map

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport Data.Graph.Inductive.Graph as Graph (Node)

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder-- | Analyse an architectural specification

c1bca76471ad22ac47f05b03576974762d364339Christian Maeder-- @

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder-- ARCH-SPEC ::= BASIC-ARCH-SPEC | GROUP-ARCH-SPEC | ARCH-SPEC-NAME

7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder-- @

df67ddf64192bfcae6ece65255ad796a17cbe532Christian MaederanaArchSpec :: LogicGraph -> DGraph

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

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder -> ARCH_SPEC -> Result (ArchSig, DGraph, ARCH_SPEC)

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

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder2. development graph resulting from structured specs within the arch

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maederspec and 3. ARCH_SPEC after possible conversions -}

275698320a734a6fd647ea6a461d6ce38862da1dChristian MaederanaArchSpec lgraph dg opts archSp = case archSp of

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder Basic_arch_spec udd uexpr pos ->

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder do (uctx, dg', udd') <- anaUnitDeclDefns lgraph dg opts udd

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder (_, usig, _, dg'', uexpr') <-

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder anaUnitExpression lgraph dg' opts uctx (item uexpr)

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

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder (replaceAnnoted uexpr' uexpr) pos)

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder Group_arch_spec asp _ -> anaArchSpec lgraph dg opts (item asp)

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

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

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder _ -> fatal_error (astr ++

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder " is not an architectural specification") pos

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder-- | Analyse a list of unit declarations and definitions

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian MaederanaUnitDeclDefns :: LogicGraph -> DGraph

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder -> HetcatsOpts -> [Annoted UNIT_DECL_DEFN]

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

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

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maederdevelopment graph 3. possibly modified list of unit declarations and

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maederdefinitions -}

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian MaederanaUnitDeclDefns lgraph dg opts =

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder anaUnitDeclDefns' lgraph dg opts emptyExtStUnitCtx

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian MaederanaUnitDeclDefns' :: LogicGraph -> DGraph

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder -> HetcatsOpts -> ExtStUnitCtx -> [Annoted UNIT_DECL_DEFN]

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

526e7f36639cb58e3c99a54bea082499a6b04a25Christian MaederanaUnitDeclDefns' lgraph dg opts uctx uds = case uds of

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder udd : udds -> do

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder (uctx', dg', udd') <-

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder anaUnitDeclDefn lgraph dg opts uctx (item udd)

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder (uctx'', dg'', udds') <-

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder anaUnitDeclDefns' lgraph dg' opts uctx' udds

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

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder [] -> return (uctx, dg, [])

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder

e84c877ad38ce9312eab222a79f44da2015572d2Christian MaederalreadyDefinedUnit :: SIMPLE_ID -> String

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian MaederalreadyDefinedUnit u = "Unit " ++ tokStr u ++ " already declared/defined"

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder-- | Create a node that represents a union of signatures

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian MaedernodeSigUnion :: LogicGraph -> DGraph -> [MaybeNode] -> DGOrigin

c1bca76471ad22ac47f05b03576974762d364339Christian Maeder -> Result (NodeSig, DGraph)

c1bca76471ad22ac47f05b03576974762d364339Christian MaedernodeSigUnion lgraph dg nodeSigs orig =

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

c1bca76471ad22ac47f05b03576974762d364339Christian Maeder $ map getMaybeSig nodeSigs

c1bca76471ad22ac47f05b03576974762d364339Christian Maeder let nodeContents = newNodeLab emptyNodeName orig

c1bca76471ad22ac47f05b03576974762d364339Christian Maeder $ noSensGTheory lid sigU ind

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder node = getNewNodeDG dg

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

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder inslink dgres nsig = do

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder dgv <- dgres

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder case nsig of

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder EmptyNode _ -> dgres

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder JustNode (NodeSig n sig) -> do

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder incl <- ginclusion lgraph sig sigUnion

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder return $ insLEdgeNubDG

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder (n, node, globDefLink incl SeeTarget) dgv

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder dg'' <- foldl inslink (return dg') nodeSigs

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder return (NodeSig node sigUnion, dg'')

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder-- | Analyse unit refs

526e7f36639cb58e3c99a54bea082499a6b04a25Christian MaederanaUnitRef :: LogicGraph -> DGraph

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder -> HetcatsOpts -> ExtStUnitCtx -> UNIT_REF

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder -> Result (ExtStUnitCtx, DGraph, UNIT_REF)

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

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maederdevelopment graph 3. possibly modified UNIT_DECL_DEFN -}

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder-- unit declaration

a7cb01ac1824bde5bdc997c8e294a1ed821dd21bChristian MaederanaUnitRef lgraph dg opts

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder uctx@(buc, _) (Unit_ref un usp pos) =

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder do (dns, diag', dg', _) <-

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder anaUnitImported lgraph dg opts uctx pos []

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder let impSig = toMaybeNode dns

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder (usig, dg'', usp') <-

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder anaRefSpec lgraph dg' opts impSig usp

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder insertBasedUnit lgraph dg'' usig (buc, diag') dns un

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder $ Unit_ref un usp' pos

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder

df67ddf64192bfcae6ece65255ad796a17cbe532Christian MaederinsertBasedUnit :: LogicGraph -> DGraph -> UnitSig -> ExtStUnitCtx

d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian Maeder -> MaybeDiagNode -> UNIT_NAME -> a

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder -> Result (ExtStUnitCtx, DGraph, a)

df67ddf64192bfcae6ece65255ad796a17cbe532Christian MaederinsertBasedUnit lgraph dg'' usig uctx@(buc, diag') dns un@(Token ustr unpos)

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder ud' =

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder if Map.member un buc

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

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder else case usig of

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder UnitSig argSigs resultSig -> do

275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder let impSig = toMaybeNode dns

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder (resultSig', dg''') <- nodeSigUnion lgraph dg''

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder (JustNode resultSig : [impSig]) DGImports

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder (basedParUSig, diag''') <- if null argSigs then do

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder (dn', diag'') <- extendDiagramIncl lgraph diag'

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder (case dns of

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder JustDiagNode dn -> [dn]

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder _ -> []) resultSig' ustr

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder return (Based_unit_sig dn', diag'')

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder else return (Based_par_unit_sig dns $

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder UnitSig argSigs resultSig', diag')

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder return ((Map.insert un basedParUSig buc, diag'''),

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder dg''', ud')

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder-- | Analyse unit declaration or definition

df67ddf64192bfcae6ece65255ad796a17cbe532Christian MaederanaUnitDeclDefn :: LogicGraph -> DGraph

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder -> HetcatsOpts -> ExtStUnitCtx -> UNIT_DECL_DEFN

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder -> Result (ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)

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

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maederdevelopment graph 3. possibly modified UNIT_DECL_DEFN -}

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian MaederanaUnitDeclDefn lgraph dg opts uctx@(buc, _) udd = case udd of

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder Unit_decl un usp uts pos -> do

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder (dns, diag', dg', uts') <-

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder anaUnitImported lgraph dg opts uctx pos uts

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder let impSig = toMaybeNode dns

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder (usig, dg'', usp') <-

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder anaRefSpec lgraph dg' opts impSig usp

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder insertBasedUnit lgraph dg'' usig (buc, diag') dns un

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder $ Unit_decl un usp' uts' pos

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder Unit_defn un uexp poss -> do

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder (p, usig, diag, dg', uexp') <-

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder anaUnitExpression lgraph dg opts uctx uexp

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder let ud' = Unit_defn un uexp' poss

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

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder don't need to convert the ExtStUnitCtx to StUnitCtx as the

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder domain will be preserved -}

6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder if Map.member un buc then

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder plain_error (uctx, dg', ud') (alreadyDefinedUnit un) $ tokPos un

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder else case usig of

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder {- we can use Map.insert as there are no mappings for

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder un in ps and bs (otherwise there would have been a

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder mapping in (ctx uctx)) -}

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder UnitSig args _ -> if null args then case p of

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder JustDiagNode dn -> return ((Map.insert un

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder (Based_unit_sig dn) buc, diag), dg', ud')

945e82ed7877917f3ab1657f555e71991372546aChristian Maeder _ -> error "anaUnitDeclDefn"

df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder else return ((Map.insert un

f0221ee7b9f8660e7c7add896e151f7a4ac8b4adChristian Maeder (Based_par_unit_sig p usig) buc

f0221ee7b9f8660e7c7add896e151f7a4ac8b4adChristian Maeder , diag), dg', ud')

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder-- | Analyse unit imports

526e7f36639cb58e3c99a54bea082499a6b04a25Christian MaederanaUnitImported :: LogicGraph -> DGraph

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

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

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

b579e1a98aa30fb6093cbbdfeae51edbd5ba26adChristian Maeder case terms of

b579e1a98aa30fb6093cbbdfeae51edbd5ba26adChristian Maeder [] -> do

187e09da24d6ed264eeeef48eb3fcc2b8663ca46Christian Maeder curl <- lookupCurrentLogic "UnitImported" lgraph

187e09da24d6ed264eeeef48eb3fcc2b8663ca46Christian Maeder return (EmptyDiagNode curl, diag, dg, [])

7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder _ -> do

7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder (dnsigs, diag', dg', terms') <-

7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder anaUnitImported' lgraph dg opts uctx terms

7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder (sig, dg'') <- nodeSigUnion lgraph dg'

7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder (map (JustNode . getSigFromDiag) dnsigs) DGImports

7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder -- check amalgamability conditions

7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder {- let incl s = propagateErrors (ginclusion lgraph (getSig

7710f7c3425e45af11af124ff37bec27229d24f7Christian Maeder (getSigFromDiag s)) (getSig sig)) -}

b579e1a98aa30fb6093cbbdfeae51edbd5ba26adChristian Maeder let pos = getPosUnitImported poss

b579e1a98aa30fb6093cbbdfeae51edbd5ba26adChristian Maeder sink <- inclusionSink lgraph dnsigs sig

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

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

b579e1a98aa30fb6093cbbdfeae51edbd5ba26adChristian Maeder sig $ showDoc terms ""

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder return (JustDiagNode dnsig, diag'', dg'', terms')

f0221ee7b9f8660e7c7add896e151f7a4ac8b4adChristian Maeder

d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian MaederanaUnitImported' :: LogicGraph -> DGraph

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

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

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

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

d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian Maeder ut : uts -> do

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

d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian Maeder anaUnitTerm lgraph dg opts uctx (item ut)

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

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

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

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder-- | Analyse an unit expression

526e7f36639cb58e3c99a54bea082499a6b04a25Christian MaederanaUnitExpression :: LogicGraph -> DGraph

526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder -> HetcatsOpts -> ExtStUnitCtx -> UNIT_EXPRESSION

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder -> Result (MaybeDiagNode, UnitSig, Diag, DGraph, UNIT_EXPRESSION)

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian MaederanaUnitExpression lgraph dg opts uctx@(buc, diag)

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder uexp@(Unit_expression ubs ut poss) = case ubs of

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder [] -> do

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

c1bca76471ad22ac47f05b03576974762d364339Christian Maeder anaUnitTerm lgraph dg opts uctx (item ut)

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

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder Unit_expression [] (replaceAnnoted ut' ut) poss)

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder _ -> do

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder (args, dg', ubs') <-

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder anaUnitBindings lgraph dg opts uctx ubs

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder (resnsig, _dg'') <- nodeSigUnion lgraph dg'

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder (map (JustNode . snd) args) DGFormalParams

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder -- build the extended diagram and new based unit context

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder let dexp = showDoc uexp ""

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder insNodes diag0 [] buc0 = return ([], diag0, buc0)

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder insNodes diag0 ((un, nsig) : args0) buc0 =

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

31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder 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