3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari{- |

3980fec332f0cc3d65051ce86f11c357686ed784Daniel CalegariModule : $Header$

3980fec332f0cc3d65051ce86f11c357686ed784Daniel CalegariDescription : static analysis of heterogeneous structured specifications

3980fec332f0cc3d65051ce86f11c357686ed784Daniel CalegariCopyright : (c) Till Mossakowski and Uni Bremen 2003-2006

3980fec332f0cc3d65051ce86f11c357686ed784Daniel CalegariLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

3980fec332f0cc3d65051ce86f11c357686ed784Daniel CalegariMaintainer : till@informatik.uni-bremen.de

3980fec332f0cc3d65051ce86f11c357686ed784Daniel CalegariStability : provisional

3980fec332f0cc3d65051ce86f11c357686ed784Daniel CalegariPortability : non-portable (imports Logic.Grothendieck)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari

3980fec332f0cc3d65051ce86f11c357686ed784Daniel CalegariStatic analysis of CASL (heterogeneous) structured specifications

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari Follows the verfication semantic rules in Chap. IV:4.7

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari of the CASL Reference Manual.

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari-}

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegarimodule Static.AnalysisStructured

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari ( ana_SPEC

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari , isStructured

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari , ana_RENAMING

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari , ana_RESTRICTION

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari , homogenizeGM

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari , insGSig

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari , insLink

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari , extendMorphism

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari ) where

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Driver.Options

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Logic.Logic

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Logic.ExtSign

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Logic.Coerce

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Logic.Comorphism

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Logic.Grothendieck

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Logic.Prover

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Static.DevGraph

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Static.GTheory

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Syntax.AS_Structured

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Common.Result

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Common.Id

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Common.ExtSign

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Common.AS_Annotation hiding (isAxiom, isDef)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport qualified Data.Set as Set

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport qualified Data.Map as Map

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport qualified Common.Lib.Rel as Rel(image, setInsert)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Data.Graph.Inductive.Graph as Graph (Node)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Common.DocUtils

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Data.Maybe

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Data.List (find)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariimport Control.Monad

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari

3980fec332f0cc3d65051ce86f11c357686ed784Daniel CalegariinsGTheory :: DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel CalegariinsGTheory dg name orig (G_theory lid sig ind sens tind) =

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari let (sgMap, s) = sigMapI dg

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (tMap, t) = thMapI dg

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari nind = if ind == startSigId then succ s else ind

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari tb = tind == startThId && not (Map.null sens)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari ntind = if tb then succ t else tind

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari nsig = G_sign lid sig nind

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari nth = G_theory lid sig nind sens ntind

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari node_contents = newNodeLab name orig nth

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari node = getNewNodeDG dg

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari in (NodeSig node nsig,

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (if tb then setThMapDG $ Map.insert (succ t) nth tMap else id) $

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (if ind == startSigId

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari then setSigMapDG $ Map.insert (succ s) nsig sgMap else id)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari $ insNodeDG (node, node_contents) dg)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari

3980fec332f0cc3d65051ce86f11c357686ed784Daniel CalegariinsGSig :: DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel CalegariinsGSig dg name orig (G_sign lid sig ind) =

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari insGTheory dg name orig $ noSensGTheory lid sig ind

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari

3980fec332f0cc3d65051ce86f11c357686ed784Daniel CalegariinsLink :: DGraph -> GMorphism -> DGLinkType -> DGLinkOrigin -> Node -> Node

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari -> DGraph

3980fec332f0cc3d65051ce86f11c357686ed784Daniel CalegariinsLink dg (GMorphism cid sign si mor mi) ty orig n t =

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari let (sgMap, s) = sigMapI dg

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (mrMap, m) = morMapI dg

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari nsi = if si == startSigId then succ s else si

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari nmi = if mi == startMorId then succ m else mi

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari nmor = GMorphism cid sign nsi mor nmi

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari link = DGLink

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari { dgl_morphism = nmor

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari , dgl_type = ty

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari , dgl_origin = orig

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari , dgl_id = defaultEdgeId }

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari in (if mi == startMorId then setMorMapDG $ Map.insert (succ m)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (toG_morphism nmor) mrMap else id) $

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (if si == startSigId then setSigMapDG $ Map.insert (succ s)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (G_sign (sourceLogic cid) sign nsi) sgMap else id)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari $ insLEdgeNubDG (n, t, link) dg

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari-- | analyze a SPEC

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari-- first Parameter determines if incoming symbols shall be ignored

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari-- options: here we need the info: shall only the structure be analysed?

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariana_SPEC :: Bool -> LogicGraph -> DGraph -> MaybeNode -> NodeName ->

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari HetcatsOpts -> SPEC -> Result (SPEC, NodeSig, DGraph)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegariana_SPEC addSyms lg dg nsig name opts sp = case sp of

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari Basic_spec (G_basic_spec lid bspec) pos ->

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari do G_sign lid' sigma' i1 <- return (getMaybeSig nsig)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari let adj = adjustPos pos

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari sigma@(ExtSign sig sys) <-

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari adj $ coerceSign lid' lid "Analysis of basic spec" sigma'

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (bspec', ExtSign sigma_complete sysd, ax) <- adj $

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari if isStructured opts

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari then return (bspec, mkExtSign $ empty_signature lid, [])

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari else do b <- maybeToMonad

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari ("no basic analysis for logic "

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari ++ language_name lid)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (basic_analysis lid)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari b (bspec, sig, globalAnnos dg)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari let (ns@(NodeSig node gsig), dg') = insGTheory dg name DGBasic

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari $ G_theory lid (ExtSign sigma_complete

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari $ Set.intersection

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (if addSyms then Set.union sys sysd else sysd)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari $ sym_of lid sigma_complete) startSigId (toThSens ax) startThId

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari incl <- adj $ ginclusion lg (G_sign lid sigma i1) gsig

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari return (Basic_spec (G_basic_spec lid bspec') pos, ns, case nsig of

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari EmptyNode _ -> dg'

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari JustNode (NodeSig n _) ->

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari insLink dg' incl GlobalDef DGLinkExtension n node)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari EmptySpec pos -> case nsig of

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari EmptyNode _ -> do

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari warning () "empty spec" pos

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari let (ns, dg') = insGSig dg name DGEmpty (getMaybeSig nsig)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari return (sp, ns, dg')

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari {- ana_SPEC should be changed to return a MaybeNode!

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari Then this duplicate dummy node could be avoided.

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari Also empty unions could be treated then -}

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari JustNode ns -> return (sp, ns ,dg)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari Translation asp ren ->

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari do let sp1 = item asp

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (sp1', NodeSig n' gsigma, dg') <-

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari ana_SPEC addSyms lg dg nsig (inc name) opts sp1

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari mor <- ana_RENAMING lg nsig gsigma opts ren

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari -- ??? check that mor is identity on local env

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari let (ns@(NodeSig node _), dg'') =

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari insGSig dg' name DGTranslation $ cod Grothendieck mor

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari -- ??? too simplistic for non-comorphism inter-logic translations

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari return (Translation (replaceAnnoted sp1' asp) ren, ns,

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari insLink dg'' mor GlobalDef SeeTarget n' node)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari Reduction asp restr ->

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari do let sp1 = item asp

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (sp1', NodeSig n' gsigma', dg') <-

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari ana_SPEC addSyms lg dg nsig (inc name) opts sp1

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari let gsigma = getMaybeSig nsig

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (hmor, tmor) <- ana_RESTRICTION gsigma gsigma' opts restr

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari -- we treat hiding and revealing differently

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari -- in order to keep the dg as simple as possible

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari case tmor of

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari Nothing ->

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari do let (ns@(NodeSig node _), dg'') =

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari insGSig dg' name DGHiding $ dom Grothendieck hmor

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari -- ??? too simplistic for non-comorphism inter-logic reductions

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari return (Reduction (replaceAnnoted sp1' asp) restr, ns,

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari insLink dg'' hmor HidingDef SeeTarget n' node)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari Just tmor' -> do

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari let gsigma1 = dom Grothendieck tmor'

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari gsigma'' = cod Grothendieck tmor'

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari -- ??? too simplistic for non-comorphism inter-logic reductions

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari -- the case with identity translation leads to a simpler dg

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari if tmor' == ide Grothendieck (dom Grothendieck tmor')

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari then do

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari let (ns@(NodeSig node1 _), dg'') =

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari insGSig dg' name DGRevealing gsigma1

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari return (Reduction (replaceAnnoted sp1' asp) restr, ns,

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari insLink dg'' hmor HidingDef SeeTarget n' node1)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari else do

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari let (NodeSig node1 _, dg'') =

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari insGSig dg' (extName "T" name) DGRevealing gsigma1

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (ns@(NodeSig node2 _), dg3) =

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari insGSig dg'' name DGRevealTranslation gsigma''

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari dg4 = insLink dg3 hmor HidingDef SeeTarget n' node1

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari return (Reduction (replaceAnnoted sp1' asp) restr, ns,

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari insLink dg4 tmor' GlobalDef SeeTarget node1 node2)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari Union [] pos -> adjustPos pos $ fail $ "empty union"

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari Union asps pos ->

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari do let sps = map item asps

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (sps', nsigs, dg', _) <-

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari let ana (sps1, nsigs, dg', n) sp' = do

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (sp1, nsig', dg1) <- ana_SPEC addSyms lg dg' nsig n opts sp'

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari return (sp1 : sps1, nsig' : nsigs, dg1, inc n)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari in foldM ana ([], [], dg, extName "U" name) sps

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari let nsigs' = reverse nsigs

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari adj = adjustPos pos

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari gbigSigma <- adj $ gsigManyUnion lg (map getSig nsigs')

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari let (ns@(NodeSig node _), dg2) = insGSig dg' name DGUnion gbigSigma

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari insE dgl (NodeSig n gsigma) = do

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari incl <- adj $ ginclusion lg gsigma gbigSigma

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari return $ insLink dgl incl GlobalDef SeeTarget n node

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari dg3 <- foldM insE dg2 nsigs'

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari return (Union (map (uncurry replaceAnnoted)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (zip (reverse sps') asps))

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari pos, ns, dg3)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari Extension asps pos -> do

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (sps', nsig1', dg1, _, _, _, _) <-

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari foldM ana_Extension ([], nsig, dg, lg, opts, pos, addSyms) namedSps

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari case nsig1' of

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari EmptyNode _ -> fail "empty extension"

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari JustNode nsig1 -> return (Extension (map (uncurry replaceAnnoted)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (zip (reverse sps') asps))

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari pos, nsig1,dg1)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari where

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari namedSps = zip (reverse (name: tail (take (length asps)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (iterate inc (extName "E" name)))))

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari asps

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari Free_spec asp poss -> do

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (nasp, nsig', dg') <-

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari anaPlainSpec addSyms lg opts dg nsig name DGFree (FreeDef nsig)

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari asp poss

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari return (Free_spec nasp poss, nsig', dg')

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari Cofree_spec asp poss -> do

3980fec332f0cc3d65051ce86f11c357686ed784Daniel Calegari (nasp, nsig', dg') <-

anaPlainSpec addSyms lg opts dg nsig name DGCofree (CofreeDef nsig)

asp poss

return (Cofree_spec nasp poss, nsig', dg')

Local_spec asp asp' poss ->

do let sp1 = item asp

sp1' = item asp'

(sp2, nsig'@(NodeSig _ (G_sign lid' sigma' _)), dg') <-

ana_SPEC False lg dg nsig (extName "L" name) opts sp1

(sp2', NodeSig n'' (G_sign lid'' sigma'' _), dg'') <-

ana_SPEC False lg dg' (JustNode nsig') (inc name) opts sp1'

let gsigma = getMaybeSig nsig

G_sign lid sigma _ <- return gsigma

sigma1 <- coerceSign lid' lid "Analysis of local spec" sigma'

sigma2 <- coerceSign lid'' lid "Analysis of local spec" sigma''

let sys = ext_sym_of lid sigma

sys1 = ext_sym_of lid sigma1

sys2 = ext_sym_of lid sigma2

mor3 <- if isStructured opts then return (ext_ide lid sigma2)

else adjustPos poss $ ext_cogenerated_sign lid

(sys1 `Set.difference` sys) sigma2

let sigma3 = dom lid mor3

-- gsigma2 = G_sign lid sigma2

gsigma3 = G_sign lid (makeExtSign lid sigma3) startSigId

sys3 = sym_of lid sigma3

when (not( isStructured opts ||

sys2 `Set.difference` sys1 `Set.isSubsetOf` sys3))

$ plain_error () (

"illegal use of locally declared symbols: "

++ showDoc ((sys2 `Set.intersection` sys1) `Set.difference` sys3) "")

poss

let (ns@(NodeSig node _), dg2) = insGSig dg'' name DGLocal gsigma3

return (Local_spec (replaceAnnoted sp2 asp)

(replaceAnnoted sp2' asp')

poss, ns,

insLink dg2 (gEmbed2 gsigma3 $ mkG_morphism lid mor3)

HidingDef SeeTarget n'' node)

Closed_spec asp pos ->

do let sp1 = item asp

l = getLogic nsig

-- analyse spec with empty local env

(sp', NodeSig n' gsigma', dg') <-

ana_SPEC False lg dg (EmptyNode l) (inc name) opts sp1

let gsigma = getMaybeSig nsig

adj = adjustPos pos

gsigma'' <- adj $ gsigUnion lg gsigma gsigma'

let (ns@(NodeSig node gsigma2), dg2) = insGSig dg' name DGClosed gsigma''

incl1 <- adj $ ginclusion lg gsigma gsigma2

incl2 <- adj $ ginclusion lg gsigma' gsigma2

let dg3 = insLink dg2 incl2 GlobalDef SeeTarget n' node

return (Closed_spec (replaceAnnoted sp' asp) pos, ns, case nsig of

EmptyNode _ -> dg3

JustNode (NodeSig n _) ->

insLink dg3 incl1 GlobalDef DGLinkClosedLenv n node)

Qualified_spec lognm@(Logic_name ln _) asp pos -> do

let newLG = lg { currentLogic = tokStr ln }

l <- lookupCurrentLogic "Qualified_spec" newLG

let newNSig = case nsig of

EmptyNode _ -> EmptyNode l

_ -> nsig

(nasp, nsig', dg') <-

anaPlainSpec addSyms lg opts dg newNSig name DGLogicQual GlobalDef

asp pos

return (Qualified_spec lognm nasp pos, nsig', dg')

Group asp pos -> do

(sp', nsig', dg') <- ana_SPEC addSyms lg dg nsig name opts (item asp)

return (Group (replaceAnnoted sp' asp) pos, nsig', dg')

Spec_inst spname afitargs pos0 -> let

pos = if null afitargs then tokPos spname else pos0

adj = adjustPos pos

spstr = tokStr spname

in case lookupGlobalEnvDG spname dg of

Just (SpecEntry gs@(ExtGenSig imps params _ body@(NodeSig nB gsigmaB))) ->

case (\ x y -> (x , x - y)) (length afitargs) (length params) of

-- the case without parameters leads to a simpler dg

(0, 0) -> do

gsigma <- adj $ gsigUnion lg (getMaybeSig nsig) gsigmaB

let (fsig@(NodeSig node gsigma'), dg2) =

insGSig dg name (DGSpecInst spname) gsigma

incl <- adj $ ginclusion lg gsigmaB gsigma'

let dg3 = insLink dg2 incl GlobalDef SeeTarget nB node

case nsig of

-- the subcase with empty local env leads to an even simpler dg

EmptyNode _ ->

-- if the node shall not be named and the logic does not change,

if isInternal name && langNameSig gsigma' == langNameSig gsigmaB

-- then just return the body

then return (sp, body, dg)

-- otherwise, we need to create a new one

else return (sp, fsig, dg3)

-- the subcase with nonempty local env

JustNode (NodeSig n sigma) -> do

incl2 <- adj $ ginclusion lg sigma gsigma'

return (sp, fsig,

insLink dg3 incl2 GlobalDef SeeTarget n node)

-- now the case with parameters

(_, 0) -> do

let fitargs = map item afitargs

(fitargs', dg', args, _) <- adj $ foldM (anaFitArg lg opts spname imps)

([], dg, [], extName "A" name) (zip params fitargs)

let actualargs = reverse args

(gsigma', morDelta) <- adj $ apply_GS lg gs actualargs

gsigmaRes <- adj $ gsigUnion lg (getMaybeSig nsig) gsigma'

let (ns@(NodeSig node gsigmaRes'), dg2) =

insGSig dg' name (DGSpecInst spname) gsigmaRes

incl1 <- adj $ ginclusion lg (getMaybeSig nsig) gsigmaRes'

incl2 <- adj $ ginclusion lg gsigma' gsigmaRes'

morDelta' <- comp Grothendieck (gEmbed morDelta) incl2

dg3 <- foldM (parLink lg DGLinkFitSpec gsigmaRes' node) dg2

$ map snd args

let dg4 = insLink dg3 morDelta' GlobalDef SeeTarget nB node

dg5 = case nsig of

EmptyNode _ -> dg4

JustNode (NodeSig n _) ->

insLink dg4 incl1 GlobalDef SeeTarget n node

return (Spec_inst spname

(map (uncurry replaceAnnoted)

(zip (reverse fitargs') afitargs))

pos, ns, dg5)

-- finally the case with conflicting numbers of formal and actual parameters

_ ->

fatal_error

(spstr ++ " expects " ++ show (length params) ++ " arguments"

++ " but was given " ++ show (length afitargs)) pos

_ -> fatal_error

("Structured specification " ++ spstr ++ " not found") pos

Data (Logic lidD) (Logic lidP) asp1 asp2 pos -> do

let sp1 = item asp1

sp2 = item asp2

adj = adjustPos pos

Comorphism cid <- adj $ logicInclusion lg (Logic lidD) (Logic lidP)

let lidD' = sourceLogic cid

lidP' = targetLogic cid

(sp1', NodeSig n' (G_sign lid' sigma' _), dg') <-

ana_SPEC False lg dg (EmptyNode (Logic lidD)) (inc name) opts sp1

sigmaD <- adj $ coerceSign lid' lidD' "Analysis of data spec" sigma'

(sigmaD',sensD') <- adj $ ext_map_sign cid sigmaD

let (nsig2@(NodeSig node _), dg1) = insGTheory dg' name DGData

$ G_theory lidP' sigmaD' startSigId (toThSens sensD') startThId

dg2 = insLink dg1 (GMorphism cid sigmaD startSigId

(ext_ide lidP' sigmaD') startMorId)

GlobalDef SeeTarget n' node

(sp2', nsig3, dg3) <-

ana_SPEC addSyms lg dg2 (JustNode nsig2) name opts sp2

return (Data (Logic lidD) (Logic lidP)

(replaceAnnoted sp1' asp1)

(replaceAnnoted sp2' asp2)

pos, nsig3, dg3)

anaPlainSpec :: Bool -> LogicGraph -> HetcatsOpts -> DGraph -> MaybeNode

-> NodeName -> DGOrigin -> DGLinkType -> Annoted SPEC -> Range

-> Result (Annoted SPEC, NodeSig, DGraph)

anaPlainSpec addSyms lg opts dg nsig name orig dglType asp pos = do

(sp', NodeSig n' gsigma, dg') <-

ana_SPEC addSyms lg dg nsig (inc name) opts $ item asp

let (ns@(NodeSig node gsigma'), dg2) = insGSig dg' name orig gsigma

incl <- adjustPos pos $ ginclusion lg (getMaybeSig nsig) gsigma'

return (replaceAnnoted sp' asp, ns,

insLink dg2 incl dglType SeeTarget n' node)

anaFitArg :: LogicGraph -> HetcatsOpts -> SPEC_NAME -> MaybeNode

-> ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NodeName)

-> (NodeSig, FIT_ARG)

-> Result ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NodeName)

anaFitArg lg opts spname imps (fas', dg1, args, name') (nsig', fa) = do

(fa', dg', arg) <- ana_FIT_ARG lg dg1 spname imps nsig' opts name' fa

return (fa' : fas', dg', arg : args , inc name')

parLink :: LogicGraph -> DGLinkOrigin -> G_sign -> Node -> DGraph -> NodeSig

-> Result DGraph

parLink lg orig gsigma' node dg (NodeSig nA_i sigA_i)= do

incl <- ginclusion lg sigA_i gsigma'

return $ insLink dg incl GlobalDef orig nA_i node

-- analysis of renamings

ana_ren :: LogicGraph -> HetcatsOpts -> MaybeNode -> Range -> GMorphism

-> G_mapping -> Result GMorphism

ana_ren lg opts lenv pos gmor@(GMorphism r sigma ind1 mor _) gmap =

let adj = adjustPos pos in case gmap of

G_symb_map (G_symb_map_items_list lid sis) ->

if isStructured opts then return gmor else do

let lid2 = targetLogic r

sis1 <- adj $ coerceSymbMapItemsList lid lid2 "Analysis of renaming" sis

rmap <- adj $ stat_symb_map_items lid2 sis1

mor1 <- adj $ induced_from_morphism lid2 rmap (cod lid2 mor)

case lenv of

EmptyNode _ -> return ()

JustNode (NodeSig _ (G_sign lidLenv sigmaLenv _)) -> do

-- needs to be changed for logic translations

sigmaLenv' <- coerceSign lidLenv lid2

"Analysis of renaming: logic translations not properly handeled"

sigmaLenv

let sysLenv = ext_sym_of lid2 sigmaLenv'

m = symmap_of lid2 mor1

isChanged sy = case Map.lookup sy m of

Just sy' -> sy /= sy'

Nothing -> False

forbiddenSys = Set.filter isChanged sysLenv

when (not $ Set.null forbiddenSys) $ plain_error () (

"attempt to rename the following symbols from " ++

"the local environment:\n" ++ showDoc forbiddenSys "") pos

mor2 <- adj $ comp lid2 mor mor1

return $ GMorphism r sigma ind1 mor2 startMorId

G_logic_translation (Logic_code tok src tar pos1) -> do

let adj1 = adjustPos $ if pos1 == nullRange then pos else pos1

G_sign srcLid srcSig ind<- return (cod Grothendieck gmor)

c <- adj1 $ case tok of

Just ctok -> do

Comorphism cid <- lookupComorphism (tokStr ctok) lg

when (isJust src && getLogicStr (fromJust src) /=

language_name (sourceLogic cid))

(fail (getLogicStr (fromJust src) ++

"is not the source logic of "

++ language_name cid))

when (isJust tar && getLogicStr (fromJust tar) /=

language_name (targetLogic cid))

(fail (getLogicStr (fromJust tar) ++

"is not the target logic of "

++ language_name cid))

return (Comorphism cid)

Nothing -> case tar of

Just (Logic_name l _) -> do

tarL <- lookupLogic "with logic: " (tokStr l) lg

logicInclusion lg (Logic srcLid) tarL

Nothing -> fail "with logic: cannot determine comorphism"

mor1 <- adj1 $ gEmbedComorphism c (G_sign srcLid srcSig ind)

adj $ comp Grothendieck gmor mor1

where getLogicStr (Logic_name l _) = tokStr l

ana_RENAMING :: LogicGraph -> MaybeNode -> G_sign -> HetcatsOpts -> RENAMING

-> Result GMorphism

ana_RENAMING lg lenv gSigma opts (Renaming ren pos) =

foldM (ana_ren lg opts lenv pos) (ide Grothendieck gSigma) ren

-- analysis of restrictions

ana_restr :: G_sign -> Range -> GMorphism -> G_hiding -> Result GMorphism

ana_restr (G_sign lidLenv sigmaLenv _) pos

(GMorphism cid (ExtSign sigma1 sys1) _ mor _) gh =

case gh of

G_symb_list (G_symb_items_list lid' sis') -> do

let lid1 = sourceLogic cid

lid2 = targetLogic cid

sis1 <- coerceSymbItemsList lid' lid1 "Analysis of restriction" sis'

rsys <- stat_symb_items lid1 sis1

let sys = sym_of lid1 sigma1

sys' = Set.filter (\ sy -> any (matches lid1 sy) rsys) sys

unmatched = filter ( \ rsy -> Set.null $ Set.filter

( \ sy -> matches lid1 sy rsy) sys') rsys

when (not $ null unmatched)

$ plain_error () ("attempt to hide unknown symbols:\n"

++ showDoc unmatched "") pos

-- needs to be changed when logic projections are implemented

sigmaLenv' <- coerceSign lidLenv lid1

"Analysis of restriction: logic projections not properly handeled"

sigmaLenv

let sysLenv = ext_sym_of lid1 sigmaLenv'

forbiddenSys = sys' `Set.intersection` sysLenv

when (not $ Set.null forbiddenSys)

$ plain_error () (

"attempt to hide the following symbols from the local environment:\n"

++ showDoc forbiddenSys "") pos

mor1 <- cogenerated_sign lid1 sys' sigma1

mor1' <- map_morphism cid mor1

mor2 <- comp lid2 mor1' mor

return $ GMorphism cid (ExtSign (dom lid1 mor1) $ Set.fold (\ sy ->

case Map.lookup sy $ symmap_of lid1 mor1 of

Nothing -> id

Just sy1 -> Set.insert sy1) Set.empty sys1)

startSigId mor2 startMorId

G_logic_projection (Logic_code _tok _src _tar pos1) ->

fatal_error "no analysis of logic projections yet" pos1

ana_RESTRICTION :: G_sign -> G_sign -> HetcatsOpts -> RESTRICTION

-> Result (GMorphism, Maybe GMorphism)

ana_RESTRICTION gSigma@(G_sign lid sigma _)

gSigma'@(G_sign lid' sigma' _) opts restr =

if isStructured opts then return (ide Grothendieck gSigma, Nothing) else

case restr of

Hidden rstr pos -> do

mor <- foldM (ana_restr gSigma pos) (ide Grothendieck gSigma') rstr

return (mor, Nothing)

Revealed (G_symb_map_items_list lid1 sis) pos -> do

let sys = ext_sym_of lid sigma -- local env

sys' = ext_sym_of lid' sigma' -- "big" signature

adj = adjustPos pos

sis' <- adj $ coerceSymbMapItemsList lid1 lid'

"Analysis of restriction" sis

rmap <- adj $ stat_symb_map_items lid' sis'

let sys'' =

Set.fromList

[sy | sy <- Set.toList sys', rsy <-

Map.keys rmap, matches lid' sy rsy]

-- domain of rmap intersected with sys'

-- domain of rmap should be checked to match symbols from sys' ???

sys1 <- adj $ coerceSymbolSet lid lid' "Analysis of restriction" sys

-- ??? this is too simple in case that local env is translated

-- to a different logic

mor1 <- adj $ ext_generated_sign lid' (sys1 `Set.union` sys'') sigma'

mor2 <- adj $ induced_from_morphism lid' rmap (dom lid' mor1)

return (gEmbed (mkG_morphism lid' mor1),

Just (gEmbed (mkG_morphism lid' mor2)))

ana_FIT_ARG :: LogicGraph -> DGraph -> SPEC_NAME -> MaybeNode

-> NodeSig -> HetcatsOpts -> NodeName -> FIT_ARG

-> Result (FIT_ARG, DGraph, (G_morphism,NodeSig))

ana_FIT_ARG lg dg spname nsigI (NodeSig nP gsigmaP@(G_sign lidP sigmaP _))

opts name fv = case fv of

Fit_spec asp gsis pos -> do

let adj = adjustPos pos

(sp', nsigA@(NodeSig nA (G_sign lidA sigmaA _)), dg') <-

ana_SPEC False lg dg nsigI name opts (item asp)

G_symb_map_items_list lid sis <- homogenizeGM (Logic lidP) gsis

sigmaA' <- adj $ coerceSign lidA lidP "Analysis of fitting argument" sigmaA

mor <- adj $ if isStructured opts then return (ext_ide lidP sigmaP)

else do

rmap <- stat_symb_map_items lid sis

rmap' <- if null sis then return Map.empty

else coerceRawSymbolMap lid lidP

"Analysis of fitting argument" rmap

let noMatch sig r = Set.null $ Set.filter

(\ s -> matches lidP s r) $ ext_sym_of lidP sig

unknowns = filter (noMatch sigmaP) (Map.keys rmap')

++ filter (noMatch sigmaA') (Map.elems rmap')

if null unknowns then

ext_induced_from_to_morphism lidP rmap' sigmaP sigmaA'

else fatal_error ("unknown symbols " ++ showDoc unknowns "") pos

{-

let symI = sym_of lidP sigmaI'

symmap_mor = symmap_of lidP mor

-- are symbols of the imports left untouched?

if Set.all (\sy -> lookupFM symmap_mor sy == Just sy) symI

then return ()

else plain_error () "Fitting morphism must not affect import" pos

-} -- ??? does not work

-- ??? also output some symbol that is affected

let gmor = mkG_morphism lidP mor

return (Fit_spec (replaceAnnoted sp' asp) gsis pos,

insLink dg' (gEmbed gmor) (GlobalThm LeftOpen None LeftOpen)

(DGLinkSpecInst spname) nP nA, (gmor, nsigA))

Fit_view vn afitargs pos -> let

adj = adjustPos pos

spstr = tokStr spname

in case lookupGlobalEnvDG vn dg of

Just (ViewEntry (ExtViewSig src mor gs@(ExtGenSig imps params _ target)))

-> do

let nSrc = getNode src

nTar = getNode target

gsigmaS = getSig src

gsigmaT = getSig target

gsigmaI = getMaybeSig nsigI

GMorphism cid _ _ morHom ind <- return mor

let lid = targetLogic cid

when (not (language_name (sourceLogic cid) == language_name lid))

(fatal_error

"heterogeneous fitting views not yet implemented"

pos)

case (\ x y -> (x, x - y)) (length afitargs) (length params) of

-- the case without parameters leads to a simpler dg

(0, 0) -> case nsigI of

-- the subcase with empty import leads to a simpler dg

EmptyNode _ ->

return (fv, insLink dg (ide Grothendieck gsigmaP)

(GlobalThm LeftOpen None LeftOpen) (DGLinkFitView spname)

nP nSrc, (G_morphism lid morHom ind, target))

-- the subcase with nonempty import

JustNode (NodeSig nI _) -> do

gsigmaIS <- adj $ gsigUnion lg gsigmaI gsigmaS

when (not (isSubGsign lg gsigmaP gsigmaIS))

(plain_error ()

("Parameter does not match source of fittig view. "

++ "Parameter signature:\n"

++ showDoc gsigmaP

"\nSource signature of fitting view (united with import):\n"

++ showDoc gsigmaIS "") pos)

G_sign lidI sigI1 _<- return gsigmaI

sigI <- adj $ coerceSign lidI lid

"Analysis of instantiation with import" sigI1

mor_I <- adj $ morphism_union lid morHom $ ext_ide lid sigI

gsigmaA <- adj $ gsigUnion lg gsigmaI gsigmaT

incl1 <- adj $ ginclusion lg gsigmaI gsigmaA

incl2 <- adj $ ginclusion lg gsigmaT gsigmaA

incl3 <- adj $ ginclusion lg gsigmaI gsigmaP

incl4 <- adj $ ginclusion lg gsigmaS gsigmaP

let (ns@(NodeSig nA _), dg1) =

insGSig dg name (DGFitViewA spname) gsigmaA

(NodeSig n' _, dg2) =

insGSig dg1 (inc name) (DGFitView spname) gsigmaP

dg3 = insLink dg2 incl1 GlobalDef

(DGLinkFitViewAImp spname) nI nA

dg4 = insLink dg3 incl3 GlobalDef

(DGLinkFitViewImp spname) nI n'

dg5 = insLink dg4 incl2 GlobalDef SeeTarget nTar nA

dg6 = insLink dg5 incl4 GlobalDef SeeTarget nSrc n'

dg7 = insLink dg6 (ide Grothendieck gsigmaP)

(GlobalThm LeftOpen None LeftOpen) SeeTarget nP n'

return (fv, dg7, (mkG_morphism lid mor_I, ns))

-- now the case with parameters

(_, 0) -> do

let fitargs = map item afitargs

(fitargs', dg', args,_) <- foldM (anaFitArg lg opts spname imps)

([], dg, [], extName "A" name) (zip params fitargs)

let actualargs = reverse args

(gsigmaA,mor_f) <- adj $ apply_GS lg gs actualargs

let gmor_f = gEmbed mor_f

gsigmaRes <- adj $ gsigUnion lg gsigmaI gsigmaA

mor1 <- adj $ comp Grothendieck mor gmor_f

incl1 <- adj $ ginclusion lg gsigmaA gsigmaRes

mor' <- adj $ comp Grothendieck gmor_f incl1

GMorphism cid1 _ _ mor1Hom _<- return mor1

let lid1 = targetLogic cid1

when (not (language_name (sourceLogic cid1) == language_name lid1))

(fatal_error

("heterogeneous fitting views not yet implemented")

pos)

G_sign lidI sigI1 _<- return gsigmaI

sigI <- adj $ coerceSign lidI lid1

"Analysis of instantiation with parameters" sigI1

theta <- adj $ morphism_union lid1 mor1Hom (ext_ide lid1 sigI)

incl2 <- adj $ ginclusion lg gsigmaI gsigmaRes

incl3 <- adj $ ginclusion lg gsigmaI gsigmaP

incl4 <- adj $ ginclusion lg gsigmaS gsigmaP

let (ns@(NodeSig nA _), dg1) =

insGSig dg' name (DGFitViewA spname) gsigmaRes

(NodeSig n' _, dg2) =

insGSig dg1 (extName "V" name) (DGFitView spname) gsigmaP

dg3 <- foldM (parLink lg (DGLinkFitView spname) gsigmaRes nA) dg2

$ map snd args

let dg4 = case nsigI of

EmptyNode _ -> dg3

JustNode (NodeSig nI _) -> let

dg3a = insLink dg3 incl2 GlobalDef

(DGLinkFitViewAImp spname) nI nA

in insLink dg3a incl3 GlobalDef (DGLinkFitViewImp spname) nI n'

dg5 = insLink dg4 mor' GlobalDef SeeTarget nTar nA

dg6 = insLink dg5 incl4 GlobalDef SeeTarget nSrc n'

dg7 = insLink dg6 (ide Grothendieck gsigmaP)

(GlobalThm LeftOpen None LeftOpen) SeeTarget nP n'

return (Fit_view vn

(map (uncurry replaceAnnoted)

(zip (reverse fitargs') afitargs))

pos, dg7, (mkG_morphism lid1 theta, ns))

-- finally the case with conflicting numbers of formal and actual parameters

_ ->

fatal_error

(spstr ++ " expects " ++ show (length params) ++ " arguments"

++ " but was given " ++ show (length afitargs)) pos

_ -> fatal_error

("View " ++ tokStr vn ++ " not found") pos

-- Extension of signature morphisms (for instantitations)

-- first some auxiliary functions

mapID :: Map.Map Id (Set.Set Id) -> Id -> Result Id

mapID idmap i@(Id toks comps pos1) =

case Map.lookup i idmap of

Nothing -> do

compsnew <- sequence $ map (mapID idmap) comps

return (Id toks compsnew pos1)

Just ids -> if Set.null ids then return i else

if Set.null $ Set.deleteMin ids then return $ Set.findMin ids else

plain_error i

("Identifier component " ++ showId i

" can be mapped in various ways:\n"

++ showDoc ids "") $ getRange i

extID1 :: Map.Map Id (Set.Set Id) -> Id

-> Result (EndoMap Id) -> Result (EndoMap Id)

extID1 idmap i@(Id toks comps pos1) m = do

m1 <- m

compsnew <- sequence $ map (mapID idmap) comps

if comps==compsnew

then return m1

else return (Map.insert i (Id toks compsnew pos1) m1)

extID :: Set.Set Id -> Map.Map Id (Set.Set Id) -> Result (EndoMap Id)

extID ids idmap = Set.fold (extID1 idmap) (return Map.empty) ids

extendMorphism :: G_sign -- ^ formal parameter

-> G_sign -- ^ body

-> G_sign -- ^ actual parameter

-> G_morphism -- ^ fitting morphism

-> Result(G_sign,G_morphism)

extendMorphism (G_sign lid sigmaP _) (G_sign lidB sigmaB1 _)

(G_sign lidA sigmaA1 _) (G_morphism lidM fittingMor1 _) = do

-- for now, only homogeneous instantiations....

sigmaB@(ExtSign _ sysB) <-

coerceSign lidB lid "Extension of symbol map" sigmaB1

sigmaA <- coerceSign lidA lid "Extension of symbol map" sigmaA1

fittingMor <- coerceMorphism lidM lid "Extension of symbol map" fittingMor1

let symsP = ext_sym_of lid sigmaP

symsB = ext_sym_of lid sigmaB

idsB = Set.map (sym_name lid) symsB

h = symmap_of lid fittingMor

symbMapToRawSymbMap =

Map.foldWithKey (\sy1 sy2 -> Map.insert (symbol_to_raw lid sy1)

(symbol_to_raw lid sy2))

Map.empty

rh = symbMapToRawSymbMap h

idh = Map.foldWithKey

(\sy1 sy2 -> Rel.setInsert (sym_name lid sy1) (sym_name lid sy2))

Map.empty h

idhExt <- extID idsB idh

let rIdExt = Map.foldWithKey (\id1 id2 -> Map.insert

(id_to_raw lid id1) (id_to_raw lid id2))

Map.empty

(foldr (\i -> Map.delete i) idhExt $ Map.keys idh)

r = rh `Map.union` rIdExt

-- do we need combining function catching the clashes???

mor <- ext_induced_from_morphism lid r sigmaB

let hmor = symmap_of lid mor

sigmaAD = ExtSign (cod lid mor) $ Set.map (\ sy ->

Map.findWithDefault sy sy $ symmap_of lid mor) sysB

sigma <- ext_final_union lid sigmaA sigmaAD

let illShared = (ext_sym_of lid sigmaA `Set.intersection`

ext_sym_of lid sigmaAD )

Set.\\ Rel.image h symsP

when (not (Set.null illShared))

(plain_error () ("Symbols shared between actual parameter and body"

++ "\nmust be in formal parameter:\n"

++ showDoc illShared "") nullRange)

let myKernel m = Set.fromDistinctAscList $ comb1 $ Map.toList m

comb1 [] = []

comb1 (p : qs) =

comb2 p qs [] ++ comb1 qs

comb2 _ [] rs = rs

comb2 p@(a, b) ((c, d) : qs) rs =

comb2 p qs $ if b == d then (a, c) : rs else rs

newIdentifications = myKernel hmor Set.\\ myKernel h

when (not (Set.null newIdentifications))

(plain_error () (

"Fitting morphism leads to forbidden identifications:\n"

++ showDoc newIdentifications "") nullRange)

incl <- ext_inclusion lid sigmaAD sigma

mor1 <- comp lid mor incl

return (G_sign lid sigma startSigId, mkG_morphism lid mor1)

apply_GS :: LogicGraph -> ExtGenSig -> [(G_morphism,NodeSig)]

-> Result(G_sign,G_morphism)

apply_GS lg (ExtGenSig nsigI _ gsigmaP nsigB) args = do

let mor_i = map fst args

gsigmaA_i = map (getSig . snd) args

gsigmaB = getSig nsigB

gsigmaI = getMaybeSig nsigI

G_sign lidI sigmaI _<- return gsigmaI

let idI = ext_ide lidI sigmaI

gsigmaA <- gsigManyUnion lg gsigmaA_i

mor_f <- homogeneousMorManyUnion (mkG_morphism lidI idI : mor_i)

extendMorphism gsigmaP gsigmaB gsigmaA mor_f

homogenizeGM :: AnyLogic -> [Syntax.AS_Structured.G_mapping]

-> Result G_symb_map_items_list

homogenizeGM (Logic lid) gsis =

foldM homogenize1 (G_symb_map_items_list lid []) gsis

where

homogenize1 itl2@(G_symb_map_items_list lid2 sis) sm = case sm of

Syntax.AS_Structured.G_symb_map (G_symb_map_items_list lid1 sis1) -> do

sis1' <- coerceSymbMapItemsList lid1 lid2 "" sis1

return $ G_symb_map_items_list lid2 $ sis ++ sis1'

_ -> return itl2

-- | check if structured analysis should be performed

isStructured :: HetcatsOpts -> Bool

isStructured a = case analysis a of

Structured -> True

_ -> False

-- only consider addSyms for the first spec

ana_Extension

:: ([SPEC], MaybeNode, DGraph, LogicGraph, HetcatsOpts, Range, Bool)

-> (NodeName, Annoted SPEC)

-> Result ([SPEC], MaybeNode, DGraph, LogicGraph, HetcatsOpts, Range, Bool)

ana_Extension (sps', nsig', dg', lg, opts, pos, addSyms) (name',asp') = do

(sp1', nsig1@(NodeSig n1 sig1), dg1) <-

ana_SPEC addSyms lg dg' nsig' name' opts (item asp')

let anno = find isSemanticAnno $ l_annos asp'

-- is the extension going between real nodes?

dg2 <- case (anno, nsig') of

(Just anno0@(Semantic_anno anno1 _), JustNode (NodeSig n' sig')) -> do

-- any other semantic annotation? that's an error

when (any (\an -> isSemanticAnno an && an/=anno0) $ l_annos asp')

(plain_error () "Conflicting semantic annotations"

pos)

-- %implied should not occur here

when (anno1==SA_implied)

(plain_error ()

"Annotation %implied should come after a BASIC-ITEM"

pos)

if anno1==SA_implies then do

when (not (isHomSubGsign sig1 sig')) (plain_error ()

"Signature must not be extended in presence of %implies"

pos)

-- insert a theorem link according to p. 319 of the CASL Reference Manual

return $ insLink dg1 (ide Grothendieck sig1)

(GlobalThm LeftOpen None LeftOpen) DGLinkExtension n1 n'

else do

let anno2 = case anno1 of

SA_cons -> Cons

SA_def -> Def

SA_mono -> Mono

_ -> error "Static.AnalysisStructured: this cannot happen"

-- insert a theorem link according to p. 319 of the CASL Reference Manual

-- the theorem link is trivally proved by the parallel definition link,

-- but for clarity, we leave it open here

-- the interesting open proof obligation is anno2, of course

incl <- ginclusion lg sig' sig1

return $ insLink dg1 incl (GlobalThm LeftOpen anno2 LeftOpen)

DGLinkExtension n' n1

_ -> return dg1

return (sp1' : sps', JustNode nsig1, dg2, lg, opts, pos, True)