content: {- |
  Module      :  ./Static/AnalysisStructured.hs
  Description :  static analysis of DOL OMS and heterogeneous structured specifications
  Copyright   :  (c) Till Mossakowski and Uni Magdeburg 2003-2016
  License     :  GPLv2 or higher, see LICENSE.txt
  Maintainer  :  till@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  non-portable (imports Logic.Grothendieck)
  
  Static analysis of DOL OMS and networks and
         CASL (heterogeneous) structured specifications
    Follows the semantics of DOL OMS and networks,
     DOL OMG standard, clauses 10.2.2 and 10.2.3
  -}
  
  module Static.AnalysisStructured
      ( anaSpec
      , anaSpecTop
      , anaUnion
      , anaIntersect
      , anaSublogic
      , getSpecAnnos
      , anaRenaming
      , anaRestriction
      , partitionGmaps
      , homogenizeGM
      , anaGmaps
      , insGSig
      , insLink
      , extendMorphism
      , insGTheory
      , expCurie
      , expCurieR
      , expandCurieByPath
      , ExpOverrides
      , notFoundError
      , prefixErrorIRI
      , networkDiagram
      ) where
  
  import Driver.Options
  
  import Logic.Logic
  import Logic.ExtSign
  import Logic.Coerce
  import Logic.Comorphism
  import Logic.Grothendieck
  import Logic.Prover
  
  import Static.DevGraph
  import Static.DgUtils
  import Static.GTheory
  
  import Syntax.AS_Structured
  import Syntax.Print_AS_Structured
  
  import Common.AS_Annotation hiding (isAxiom, isDef)
  import Common.Consistency
  import Common.DocUtils
  import Common.ExtSign
  import Common.GlobalAnnotations
  import Common.Id
  import Common.IRI
  import Common.LibName
  import Common.Result
  import Common.Utils (number)
  import Common.Lib.MapSet (imageSet, setInsert)
  import qualified Control.Monad.Fail as Fail
  
  import Data.Graph.Inductive.Graph
  import qualified Data.Set as Set
  import qualified Data.Map as Map
  import Data.Maybe
  import Data.List
  import Data.Function
  
  import Control.Monad
  import Proofs.ComputeColimit (insertColimitInGraph)
  
  import Common.Lib.Graph
  
  import Static.ComputeTheory
  
  -- overrides CUIRIE expansion for Download_items
  type ExpOverrides = Map.Map IRI FilePath
  
  coerceMaybeNode :: LogicGraph -> LibEnv -> LibName ->
                     DGraph -> MaybeNode -> NodeName -> AnyLogic
                  -> Result (MaybeNode, DGraph)
  coerceMaybeNode lg libEnv ln dg mn nn l2 = case mn of
    EmptyNode _ -> return (EmptyNode l2, dg)
    JustNode ns -> do
      (ms, dg2) <- coerceNode lg libEnv ln dg ns nn l2
      return (JustNode ms, dg2)
  
  coerceNode :: LogicGraph -> LibEnv -> LibName ->
                DGraph -> NodeSig -> NodeName -> AnyLogic
             -> Result (NodeSig, DGraph)
  coerceNode lg libEnv ln dg ns@(NodeSig _ (G_sign lid1 _ _)) nn l2@(Logic lid2) =
      if language_name lid1 == language_name lid2 then return (ns, dg)
      else do
        c <- logicInclusion lg (Logic lid1) l2
        coerceNodeByComorph libEnv ln c dg ns nn
  
  coerceNodeByComorph :: LibEnv -> LibName -> AnyComorphism -> DGraph -> NodeSig -> NodeName
             -> Result (NodeSig, DGraph)
  coerceNodeByComorph libEnv ln c@(Comorphism cid) dg (NodeSig n s) nn = do
        (dg', gmor) <- if isGTC cid then do
                         let dg0 = computeDGraphTheories libEnv ln dg
                             Just l = lab (dgBody dg0) n 
                             Just gth = globalTheory l
                         gm <- gEmbedGTC c gth
                         return (dg0, gm)
                       else do 
                        gm <- gEmbedComorphism c s
                        return (dg, gm)      
        case find (\ (_, _, l) -> dgl_origin l == SeeTarget
            && dgl_type l == globalDef
            && dgl_morphism l == gmor) $ outDG dg' n of
          Nothing -> do
            let (ms@(NodeSig m _), dg2) =
                  insGSig dg' (extName "XCoerced" nn) DGLogicCoercion $ cod gmor
                dg3 = insLink dg2 gmor globalDef SeeTarget n m
            return (ms, dg3)
          Just (_, t, _) ->
              return (NodeSig t $ signOf $ dgn_theory $ labDG dg' t, dg')
  
  insGTheory :: DGraph -> NodeName -> DGOrigin -> G_theory -> (NodeSig, DGraph)
  insGTheory dg name orig (G_theory lid syn sig ind sens tind) =
      let (sgMap, s) = sigMapI dg
          (tMap, t) = thMapI dg
          nind = if ind == startSigId then succ s else ind
          tb = tind == startThId && not (Map.null sens)
          ntind = if tb then succ t else tind
          nsig = G_sign lid sig nind
          nth = G_theory lid syn sig nind sens ntind
          node_contents = newNodeLab name orig nth
          node = getNewNodeDG dg
      in (NodeSig node nsig,
          (if tb then setThMapDG $ Map.insert (succ t) nth tMap else id) $
          (if ind == startSigId
           then setSigMapDG $ Map.insert (succ s) nsig sgMap else id)
           $ insNodeDG (node, node_contents) dg)
  
  insGSig :: DGraph -> NodeName -> DGOrigin -> G_sign -> (NodeSig, DGraph)
  insGSig dg name orig (G_sign lid sig ind) =
      insGTheory dg name orig $ noSensGTheory lid sig ind
  
  insLink :: DGraph -> GMorphism -> DGLinkType -> DGLinkOrigin -> Node -> Node
          -> DGraph
  insLink dg (GMorphism cid sign si mor mi) ty orig n t =
      let (sgMap, s) = sigMapI dg
          (mrMap, m) = morMapI dg
          nsi = if si == startSigId then succ s else si
          nmi = if mi == startMorId then succ m else mi
          nmor = GMorphism cid sign nsi mor nmi
          link = defDGLink nmor ty orig
      in (if mi == startMorId then setMorMapDG $ Map.insert (succ m)
           (toG_morphism nmor) mrMap else id) $
         (if si == startSigId then setSigMapDG $ Map.insert (succ s)
          (G_sign (sourceLogic cid) sign nsi) sgMap else id)
         $ insLEdgeNubDG (n, t, link) dg
  
  createConsLink :: LinkKind -> Conservativity -> LogicGraph -> DGraph
    -> MaybeNode -> NodeSig -> DGLinkOrigin -> Result DGraph
  createConsLink lk conser lg dg nsig (NodeSig node gsig) orig = case nsig of
      EmptyNode _ | conser == None -> return dg
      _ -> case nsig of
        JustNode (NodeSig n sig) -> do
          incl <- ginclusion lg sig gsig
          return $ insLink dg incl
                (ScopedLink Global lk $ mkConsStatus conser) orig n node
        EmptyNode _ -> -- add conservativity to the target node
          return $ let lbl = labDG dg node
          in if isDGRef lbl then dg else
           fst $ labelNodeDG
             (node, lbl
              { nodeInfo =
                 (nodeInfo lbl)
                   { node_cons_status = case getNodeConsStatus lbl of
                       ConsStatus c d th -> ConsStatus (max c conser) d th }}) dg
  
  getNamedSpec :: SPEC_NAME -> LibName -> DGraph -> LibEnv
    -> Result (ExtGenSig, (LibName, DGraph, LNode DGNodeLab))
  getNamedSpec sp ln dg libenv = case lookupGlobalEnvDG sp dg of
            Just (SpecEntry s@(ExtGenSig (GenSig _ ps _) (NodeSig n _))) -> do
              unless (null ps)
                $ mkError "base theory must not be parameterized" sp
              let t@(refLib, refDG, (_, lbl)) = lookupRefNode libenv ln dg n
                  refTok = getName $ dgn_name lbl
              unless (sp == refTok)
                $ appendDiags [mkDiag Warning "renamed base theory" sp]
              if refLib == ln then return (s, t) else
                  case lookupGlobalEnvDG refTok refDG of
                    Just (SpecEntry s2) -> return (s2, t)
                    _ -> mkError "theory reference error" sp
            _ -> mkError "unknown theory" sp
  
  anaSublogic :: HetcatsOpts -> LogicDescr -> LibName -> DGraph -> LibEnv
    -> LogicGraph
    -> Result (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
  anaSublogic _opts itm ln dg libenv lG
    = case itm of
    LogicDescr (Logic_name lt ms mt) _ _ -> do
      logN@(Logic lid) <- lookupLogic "" lt lG
      mgs <- case ms of
        Nothing -> return Nothing
        Just subL -> do
          let s = tokStr subL
          case parseSublogic lid s of
            Nothing -> Fail.fail $ "unknown sublogic of logic " ++ show logN
              ++ ": " ++ s
            Just sl ->
              if sublogicName (top_sublogic lid) == s then do
                warning () ("not a proper sublogic: " ++ s) $ tokPos subL
                return Nothing
                else return $ Just $ G_sublogics lid sl
      let logicLibN = emptyLibName "Logics"
          lG1 = setCurSublogic mgs $ setLogicName itm lG
      case mt of
        Nothing -> return (Nothing, lG1 { currentTargetBase = Nothing })
        Just sp -> do
          let ssp = iriToStringUnsecure sp
          (s, t@(libName, _, (_, lbl))) <- case Map.lookup logicLibN libenv of
            Just dg2 | logicLibN /= ln -> getNamedSpec sp logicLibN dg2 libenv
            _ -> getNamedSpec sp ln dg libenv
          case sublogicOfTh $ globOrLocTh lbl of
            gs2@(G_sublogics lid2 _) -> do
              unless (logN == Logic lid2)
                $ Fail.fail $ "the logic of '" ++ ssp
                    ++ "' is '" ++ language_name lid2
                    ++ "' and not '" ++ shows logN "'!"
              case mgs of
                Nothing -> return ()
                Just gs -> unless (isSublogic gs2 gs)
                  $ Fail.fail $ "theory '" ++ ssp
                    ++ "' has sublogic '" ++ shows gs2 "' and not '"
                    ++ shows gs "'!"
              let sbMap = sublogicBasedTheories lG1
                  lMap = Map.findWithDefault Map.empty logN sbMap
                  nName = getDGNodeName lbl
              nMap <- case Map.lookup sp lMap of
                Nothing -> return $ Map.insert sp (libName, nName) lMap
                Just (prevLib, prevName) -> do
                  unless (libName == prevLib)
                    $ Fail.fail $ "theory '" ++ ssp
                      ++ "' should come from library '"
                      ++ showDoc prevLib "' and not from '"
                      ++ showDoc libName "'!"
                  unless (nName == prevName)
                    $ Fail.fail $ "the original theory name for '" ++ ssp
                      ++ "' should be '"
                      ++ prevName ++ "' and not '"
                      ++ nName ++ "'!"
                  return lMap
              return (Just (s, t), lG1
                { sublogicBasedTheories = Map.insert logN nMap sbMap
                , currentTargetBase = Just (libName, nName) })
    _ -> return (Nothing, lG)
  
  anaSpecTop :: Conservativity -> Bool -> LogicGraph -> LibEnv -> LibName -> DGraph
    -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> SPEC -> Range
    -> Result (SPEC, NodeSig, DGraph)
  anaSpecTop conser addSyms lg libEnv ln dg nsig name opts eo sp pos =
   if conser == None || case sp of
        -- for these cases def-links are re-used
      Basic_spec _ _ -> True
      Closed_spec _ _ -> True
      Spec_inst {} -> True
      Group _ _ -> True -- in this case we recurse
      _ -> False
      then anaSpecAux conser addSyms True lg libEnv ln 
                      dg nsig name opts eo sp pos 
      else do
    let provenThmLink =
          ThmLink $ Proven (DGRule "static analysis") emptyProofBasis
    (rsp, ns, rdg) <- anaSpec addSyms True lg libEnv ln 
                              dg nsig name opts eo sp pos
    ndg <- createConsLink provenThmLink conser lg rdg nsig ns SeeTarget
    return (rsp, ns, ndg)
  
  anaFreeOrCofreeSpec :: Bool -> LogicGraph -> LibEnv -> HetcatsOpts -> LibName -> DGraph
    -> MaybeNode -> NodeName -> FreeOrCofree -> ExpOverrides -> Annoted SPEC
    -> Range -> Result (Annoted SPEC, NodeSig, DGraph)
  anaFreeOrCofreeSpec addSyms lg libEnv opts ln dg nsig name dglType eo asp pos =
    adjustPos pos $ do
        let sp = item asp
            iPos = getRange sp
        (sp', NodeSig n' gsigma, dg') <-
            anaSpec addSyms True lg libEnv ln 
                    dg nsig (extName (show dglType) name) opts eo
              sp iPos
        let (ns@(NodeSig node _), dg2) =
                insGSig dg' (setSrcRange pos name) (DGFreeOrCofree dglType) gsigma
            nsigma = case nsig of
              EmptyNode cl -> emptyG_sign cl
              JustNode nds -> getSig nds
        incl <- ginclusion lg nsigma gsigma
        return (replaceAnnoted sp' asp, ns,
                insLink dg2 incl (FreeOrCofreeDefLink dglType nsig)
                SeeTarget n' node)
  
  {- | analyze a SPEC. The first Bool Parameter determines if incoming symbols shall
  be ignored while the second determines if the nodes should be optimized away for specifications without parameters. The options are needed to check: shall only the structure be
  analysed? -}
  anaSpec :: Bool -> Bool-> LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> NodeName
    -> HetcatsOpts -> ExpOverrides -> SPEC -> Range
    -> Result (SPEC, NodeSig, DGraph)
  anaSpec = anaSpecAux None
  
  anaSpecAux :: Conservativity -> Bool -> Bool 
    -> LogicGraph -> LibEnv -> LibName -> DGraph
    -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> SPEC -> Range
    -> Result (SPEC, NodeSig, DGraph)
  anaSpecAux conser addSyms optNodes lg 
             libEnv ln dg nsig name opts eo sp rg = case sp of
    Basic_spec (G_basic_spec lid bspec) pos -> adjustPos pos $ do
         let curLogic = Logic lid
             curSL = currentSublogic lg
             bsSL = G_sublogics lid $ minSublogic bspec
         when (maybe False (`isProperSublogic` bsSL) curSL)
           $ Fail.fail $ "sublogic expected: " ++ maybe "" show curSL
                 ++ " found: " ++ show bsSL
         (nsig', dg0) <- coerceMaybeNode lg libEnv ln dg nsig name curLogic
         G_sign lid' sigma' _ <- return $ case nsig' of
             EmptyNode cl -> emptyG_sign cl
             JustNode ns -> getSig ns
         ExtSign sig sys <-
             coerceSign lid' lid "Analysis of basic spec" sigma'
         (bspec', ExtSign sigma_complete sysd, ax) <-
            if isStructured opts
             then return (bspec, mkExtSign $ empty_signature lid, [])
             else
               let res@(Result ds mb) = extBasicAnalysis lid (getName name)
                     ln bspec sig $ globalAnnos dg0
               in case mb of
                 Nothing | null ds ->
                   Fail.fail "basic analysis failed without giving a reason"
                 _ -> res
         diffSig <- case signatureDiff lid sigma_complete sig of
           Result _ (Just ds) -> return ds
           _ -> warning sigma_complete
             "signature difference could not be computed using full one" pos
         let gsysd = Set.map (G_symbol lid) sysd
             (ns, dg') = insGTheory dg0 (setSrcRange rg name)
               (DGBasicSpec (Just $ G_basic_spec lid bspec')
               (G_sign lid (mkExtSign diffSig) startSigId) gsysd)
                 $ G_theory lid (currentSyntax lg) (ExtSign sigma_complete
                 $ Set.intersection
                       (if addSyms then Set.union sys sysd else sysd)
                 $ symset_of lid sigma_complete)
               startSigId (toThSens ax) startThId
         dg'' <- createConsLink DefLink conser lg dg' nsig' ns DGLinkExtension
         return (Basic_spec (G_basic_spec lid bspec') pos, ns, dg'')
    EmptySpec pos -> case nsig of
        EmptyNode _ -> do
          warning () "empty spec" pos
          let (ns, dg') = insGSig dg (setSrcRange rg name) DGEmpty
                (getMaybeSig nsig)
          return (sp, ns, dg')
          {- anaSpec should be changed to return a MaybeNode!
             Then this duplicate dummy node could be avoided.
             Also empty unions could be treated then -}
        JustNode ns -> return (sp, ns , dg)
    Translation asp ren ->
     do let sp1 = item asp
            rPos = getRange ren
        (sp1', ns'@(NodeSig n' gsigma), dg') <- 
          anaSpec addSyms optNodes lg libEnv ln dg nsig
           (extName "Translation" name) opts eo sp1 rPos
        mor <- anaRenaming lg nsig gsigma opts ren
        -- ??? check that mor is identity on local env
        when (isIdentity mor) $ warning ()
           ("nothing renamed by:\n" ++ showDoc ren "") rPos
        (fs, dgf) <- if isIdentity mor && isInternal name then return (ns', dg')
           else do
           let (ns@(NodeSig node _), dg'') = insGSig dg' (setSrcRange rg name)
                 (DGTranslation $ Renamed ren) $ cod mor
             -- ??? too simplistic for non-comorphism inter-logic translations
           return (ns, insLink dg'' mor globalDef SeeTarget n' node)
        return (Translation (replaceAnnoted sp1' asp) ren, fs, dgf)
    Extraction asp extr -> do
      let sp0 = item asp
          rname = extName "Extension" name
      (sp', nsig', dg0) <- anaSpec addSyms optNodes lg libEnv 
                                   ln dg nsig rname opts eo sp0 rg
      (ns', dg1) <- anaExtraction lg libEnv ln dg0 nsig' name rg extr
      return (Extraction (replaceAnnoted sp' asp) extr, ns', dg1)
    Reduction asp restr ->
     do let sp1 = item asp
            rname = extName "Restriction" name
        (sp1', ns0, dg0) <- anaSpec addSyms optNodes lg libEnv 
                             ln dg nsig rname opts eo sp1 rg
        rLid <- getRestrLogic restr
        p1@(NodeSig n' gsigma', dg') <- coerceNode lg libEnv ln dg0 ns0 rname rLid
        (hmor, tmor) <- anaRestriction lg (getMaybeSig nsig) gsigma' opts restr
        let noRename = maybe True isIdentity tmor
            noHide = isIdentity hmor
        when noHide $ (if noRename then warning else hint) ()
          ("nothing hidden by:\n" ++ showDoc restr "") $ getRange restr
        p2@(NodeSig node1 _, dg2) <- if noHide && isInternal name then return p1
            else do
             let trgSg = dom hmor
                 hidSyms = Set.difference (symsOfGsign gsigma')
                   $ symsOfGsign trgSg
                 orig = DGRestriction (Restricted restr) hidSyms
                 (ns@(NodeSig node _), dg'') = insGSig dg'
                   (if noRename then name else extName "Hiding" name)
                   orig trgSg
             -- ??? too simplistic for non-comorphism inter-logic reductions
             return (ns, insLink dg'' hmor HidingDefLink SeeTarget n' node)
        {- we treat hiding and revealing differently
        in order to keep the dg as simple as possible -}
        (fs, dgf) <- case tmor of
          Just tmor' | not noRename -> do
            let (ns@(NodeSig node2 _), dg3) =
                     insGSig dg2 name DGRevealTranslation $ cod tmor'
            return (ns, insLink dg3 tmor' globalDef SeeTarget node1 node2)
          Nothing -> return p2
          _ -> hint p2 ("nothing renamed by:\n" ++ showDoc restr "")
              $ getRange restr
        return (Reduction (replaceAnnoted sp1' asp) restr, fs, dgf)
    Filtering asp filtering -> do
         let sp1 = item asp
             rname = extName "Filtering" name
         (sp', nsig', dg') <- anaSpec addSyms optNodes lg libEnv ln dg 
                                      nsig rname opts eo sp1 rg
         (nf, dgF) <- anaFiltering lg libEnv ln dg' nsig' name filtering
         return (Filtering (replaceAnnoted sp' asp) filtering, nf, dgF)
         -- error "analysis of filterings not yet implemented"
    Minimization asp (Mini kw cm cv poss) -> do
        (nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg libEnv opts ln dg nsig
          name Minimize eo asp poss
        return (Minimization nasp (Mini kw cm cv poss), nsig', dg')
    Union asps pos -> do
      (newAsps, _, ns, dg') <- adjustPos pos $ anaUnion addSyms lg libEnv ln dg nsig
        name opts eo asps rg
      return (Union newAsps pos, ns, dg')
    Intersection asps pos -> do
      (newAsps, _, ns, dg') <- adjustPos pos $ anaIntersect addSyms lg libEnv ln dg nsig
        name opts eo asps rg
      return (Intersection newAsps pos, ns, dg')
    Extension asps pos -> do
     let namedSps = map (\ (asp, n) ->
           let nn = incBy n (extName "Extension" name) in
           if n < length asps then (nn, asp)
           else (name { xpath = xpath nn }, asp)) $ number asps
     (sps', nsig1', dg1, _, _) <- foldM (anaExtension lg libEnv opts eo ln pos)
       ([], nsig, dg, conser, addSyms) namedSps
     case nsig1' of
         EmptyNode _ -> Fail.fail "empty extension"
         JustNode nsig1 -> return (Extension (zipWith replaceAnnoted
                            (reverse sps') asps)
                                   pos, nsig1, dg1)
    Free_spec asp poss -> do
        (nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg libEnv opts ln dg nsig
          name Free eo asp poss
        return (Free_spec nasp poss, nsig', dg')
    Cofree_spec asp poss -> do
        (nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg libEnv opts ln dg nsig
          name Cofree eo asp poss
        return (Cofree_spec nasp poss, nsig', dg')
    Minimize_spec asp poss -> do
        (nasp, nsig', dg') <- anaFreeOrCofreeSpec addSyms lg libEnv opts ln dg nsig
            name Minimize eo asp poss
        return (Minimize_spec nasp poss, nsig', dg')
    Local_spec asp asp' poss -> adjustPos poss $ do
        let sp1 = item asp
            pos1 = getRange sp1
            sp1' = item asp'
            pos1' = getRange sp1'
            lname = extName "Local" name
        (sp2, nsig'@(NodeSig _ gsig1), dg') <-
          anaSpec False True lg libEnv ln 
                  dg nsig (extName "Spec" lname) opts eo sp1 pos1
        (sp2', NodeSig n'' gsig2@(G_sign lid2 sigma2 _), dg'') <- 
            anaSpec False True lg libEnv ln 
                  dg' (JustNode nsig') (extName "Within" lname) opts eo sp1' pos1'
        let gSigN = getMaybeSig nsig
        (G_sign lid sigmaN _, _) <- gSigCoerce lg gSigN (Logic lid2)
        sigma <- coerceSign lid lid2 "Analysis of local spec1" sigmaN
        (G_sign lid' sigma' _, _) <- gSigCoerce lg gsig1 (Logic lid2)
        sigma1 <- coerceSign lid' lid2 "Analysis of local spec2" sigma'
        let sys = ext_sym_of lid2 sigma
            sys1 = ext_sym_of lid2 sigma1
            sys2 = ext_sym_of lid2 sigma2
        mor3 <- if isStructured opts then return (ext_ide sigma2)
                 else ext_cogenerated_sign lid2
                        (sys1 `Set.difference` sys) sigma2
        let sigma3 = dom mor3
            gsigma3 = G_sign lid2 (makeExtSign lid2 sigma3) startSigId
            sys3 = symset_of lid2 sigma3
        unless (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 hidSyms = Set.difference (symsOfGsign gsig2) $ symsOfGsign gsigma3
            orig = DGRestriction NoRestriction hidSyms
            (ns@(NodeSig node _), dg2) = insGSig dg'' name orig gsigma3
        return (Local_spec (replaceAnnoted sp2 asp)
                           (replaceAnnoted sp2' asp')
                           poss, ns,
                insLink dg2 (gEmbed2 gsigma3 $ mkG_morphism lid2 mor3)
                    HidingDefLink SeeTarget n'' node)
    Closed_spec asp pos -> adjustPos pos $ do
        let sp1 = item asp
            pos1 = getRange sp1
            l = getLogic nsig
        -- analyse spec with empty local env
        (sp', NodeSig n' gsigma', dg') <- anaSpec False True lg libEnv ln dg
          (EmptyNode l) (extName "Closed" name) opts eo sp1 pos1
        gsigma2 <- gsigUnionMaybe lg addSyms nsig gsigma'
        let (ns@(NodeSig node _), dg2) = insGSig dg' name DGClosed gsigma2
        incl2 <- ginclusion lg gsigma' gsigma2
        let dg3 = insLink dg2 incl2 globalDef SeeTarget n' node
        dg4 <- createConsLink DefLink conser lg dg3 nsig ns DGLinkClosedLenv
        return (Closed_spec (replaceAnnoted sp' asp) pos, ns, dg4)
    Qualified_spec lognm asp pos -> adjustPos pos $ do
        let newLG = setLogicName lognm lg
        l <- lookupCurrentLogic "Qualified_spec" newLG
        let newNSig = case nsig of
              EmptyNode _ -> EmptyNode l
              _ -> nsig
            qname = extName "Qualified" name
        (sp', ns', dg') <- anaSpec addSyms optNodes newLG libEnv ln 
                                   dg newNSig qname opts eo
          (item asp) pos
        (ns, dg2) <- coerceNode lg libEnv ln dg' ns' qname l
        return (Qualified_spec lognm asp { item = sp' } pos, ns, dg2)
    Group asp pos -> do
        (sp', nsig', dg') <-
            anaSpecTop conser addSyms lg libEnv ln 
                       dg nsig name opts eo (item asp) rg
        return (Group (replaceAnnoted sp' asp) pos, nsig', dg')
    Spec_inst spname' afitargs mImp pos0 -> do
     spname <- expCurieR (globalAnnos dg) eo spname'
     let pos = if null afitargs then iriPos spname else pos0
     adjustPos pos $ case lookupGlobalEnvDG spname dg of
      Just (SpecEntry gs@(ExtGenSig (GenSig _ params _)
                          body@(NodeSig nB gsigmaB))) ->
       case (length afitargs, length params) of
        -- the case without parameters leads to a simpler dg
        (0, 0) -> case nsig of
            -- if the node shall not be named and the logic does not change,
          EmptyNode _ | isInternal name && optNodes -> do
            dg2 <- createConsLink DefLink conser lg dg nsig body SeeTarget
               -- then just return the body
            return (sp, body, dg2)
               -- otherwise, we need to create a new one
          _ -> do
             gsigma <- gsigUnionMaybe lg addSyms nsig gsigmaB
             let (fsig@(NodeSig node _), dg2) =
                   insGSig dg name (DGInst spname) gsigma
             incl <- ginclusion lg gsigmaB gsigma
             let dg3 = case nsig of
                   JustNode (NodeSig nI _) | nI == nB -> dg2
                   _ -> insLink dg2 incl globalDef (DGLinkMorph spname) nB node
             dg4 <- createConsLink DefLink conser lg dg3 nsig fsig SeeTarget
             return (sp, fsig, dg4)
        -- now the case with parameters
        (la, lp) | la == lp -> do
         (ffitargs, dg', (morDelta, gsigmaA, ns@(NodeSig nA gsigmaRes))) <-
                 anaAllFitArgs lg libEnv opts eo ln dg nsig name spname gs afitargs
         GMorphism cid _ _ _ _ <- return morDelta
         morDelta' <- case nsig of
           EmptyNode _
             | logicOfGsign gsigmaA == logicOfGsign gsigmaRes
               -> return morDelta
           _ -> ginclusion lg gsigmaA gsigmaRes >>= comp morDelta
         (_, imor) <- gSigCoerce lg gsigmaB $ Logic $ sourceLogic cid
         tmor <- gEmbedComorphism imor gsigmaB
         morDelta'' <- comp tmor morDelta'
         let dg4 = case nsig of
               JustNode (NodeSig nI _) | nI == nB -> dg'
               _ -> insLink dg' morDelta'' globalDef (DGLinkMorph spname) nB nA
         dg5 <- createConsLink DefLink conser lg dg4 nsig ns SeeTarget
         return (Spec_inst spname ffitargs mImp pos, ns, dg5)
         | otherwise -> instMismatchError spname lp la pos
      _ | null afitargs -> do
       warning () ("ignoring missing spec " ++ showDoc spname' "") pos
       case nsig of
        EmptyNode _ -> do -- copied from EmptySpec case
          let (ns, dg') = insGSig dg name DGEmpty (getMaybeSig nsig)
          return (sp, ns, dg')
        JustNode ns -> return (sp, ns , dg)
      _ -> notFoundError "structured spec" spname
  
    -- analyse "data SPEC1 SPEC2"
    Data lD@(Logic lidD) lP asp1 asp2 pos -> adjustPos pos $ do
        let sp1 = item asp1
            pos1 = getRange sp1
            sp2 = item asp2
        {- look for the inclusion comorphism from the current logic's data logic
        into the current logic itself -}
        c <- logicInclusion lg lD lP
        let dname = extName "Data" name
        -- analyse SPEC1
        (sp1', ns', dg') <- anaSpec False True (setCurLogic (language_name lidD) lg)
           libEnv ln dg (EmptyNode lD) dname opts eo sp1 pos1
        -- force the result to be in the data logic
        (ns'', dg'') <- coerceNode lg libEnv ln dg' ns' (extName "Qualified" dname) lD
        -- translate SPEC1's signature along the comorphism
        (nsig2@(NodeSig node gsigmaD), dg2) <- 
           coerceNodeByComorph libEnv ln c dg'' ns'' dname
        (usig, udg) <- case nsig of
          EmptyNode _ -> return (nsig2, dg2)
          JustNode ns2 -> do
            gsigma2 <- gsigUnion lg addSyms (getSig ns2) gsigmaD
            let (ns@(NodeSig node2a _), dg2a) =
                  insGSig dg2 (extName "Union" name) DGUnion gsigma2
            incl2 <- ginclusion lg gsigmaD gsigma2
            let dg3 = insLink dg2a incl2 globalDef SeeTarget node node2a
            dg4 <- createConsLink DefLink conser lg dg3 nsig ns SeeTarget
            return (ns, dg4)
        -- analyse SPEC2
        (sp2', nsig3, udg3) <-
            anaSpec addSyms optNodes lg libEnv ln 
                    udg (JustNode usig) name opts eo sp2 rg
        return (Data lD lP
                     (replaceAnnoted sp1' asp1)
                     (replaceAnnoted sp2' asp2)
                     pos, nsig3, udg3)
    Combination (Network cItems eItems _) pos -> adjustPos pos $ do
      let (cNodes', cEdges') = networkDiagram dg cItems eItems
      (ns, dg') <- insertColimitInGraph libEnv ln dg cNodes' cEdges' name
      return (sp, ns, dg')
    _ -> Fail.fail $ "AnalysisStructured: " ++ show (prettyLG lg sp)
  
  
  -- | build the diagram of a network specified as a list of network elements to be added
  -- | and a list of network elements to be removed
  
  networkDiagram :: DGraph
                          -> [LABELED_ONTO_OR_INTPR_REF]
                          -> [IRI]
                          -> ([Node], [(Node, Node, DGLinkLab)])
  networkDiagram dg cItems eItems = let 
          -- add to/remove from a list of nodes and a list of edges
          -- the graph of a network element
          -- if remove is true, nElem gets removed 
          getNodes remove (cN, cE) nElem = let
              cEntry = fromMaybe (error $ "No entry for " ++ show nElem)
                       $ lookupGlobalEnvDG nElem dg
              bgraph = dgBody dg
              lEdge x y m = case filter (\ (_, z, l) -> (z == y) &&
                                           (dgl_morphism l == m) ) $
                                 out bgraph x of
                               [] -> error $ "No edge found:\n x:" ++ show x ++ "\n y: " ++ show y
                               lE : _ -> lE
             in case cEntry of
                 SpecEntry extGenSig -> let
                     n = getNode $ extGenBody extGenSig
                    in if remove then
                       (n:cN, nub $ cE ++ out bgraph n ++ inn bgraph n) 
                       -- remove all incoming and outgoing edges of n 
                       else if elem n cN then (cN, cE) else (n : cN, cE)
                 ViewOrStructEntry True (ExtViewSig ns gm eGS) -> let
                     s = getNode ns
                     t = getNode $ extGenBody eGS
                   in if remove 
                       then (cN, lEdge s t gm : cE) 
                       -- keep the nodes and remove just the edge 
                       else(nub $ s : t : cN, lEdge s t gm : cE)
                 AlignEntry asig ->
                    case asig of
                     AlignMor src gmor tar ->  let
                       s = getNode src
                       t = getNode tar
                      in (nub $ s : t : cN, lEdge s t gmor : cE)
                     AlignSpan src phi1 tar1 phi2 tar2 ->  let
                       s = getNode src
                       t1 = getNode tar1
                       t2 = getNode tar2
                      in (nub $ [s, t1, t2] ++ cN,
                                [lEdge s t1 phi1, lEdge s t2 phi2] ++ cE)
                     WAlign src1 i1 sig1 src2 i2 sig2 tar1 tar2 bri -> let
                        s1 = getNode src1
                        s2 = getNode src2
                        t1 = getNode tar1
                        t2 = getNode tar2
                        b = getNode bri
                       in if remove then
                           (nub $ s1 : s2 : b : cN,
                           [lEdge s1 b i1, lEdge s1 t1 sig1,
                            lEdge s2 b i2, lEdge s2 t2 sig2] ++ cE) 
                          else (nub $ s1 : s2 : t1 : t2 : b : cN,
                           [lEdge s1 b i1, lEdge s1 t1 sig1,
                            lEdge s2 b i2, lEdge s2 t2 sig2] ++ cE)
                 NetworkEntry diag -> let
                      dnodes = nodes diag
                      ledges = labEdges diag
                      dgedges = map (\(x,y, (_, m)) -> lEdge x y m) ledges
                     in (dnodes, dgedges)
                 _ -> error $ show nElem
                      ++ " is not an OMS, a view, a network or an alignment"
          -- also add the implicit elements: paths of global def. links,
          -- hiding def. links, inclusions of DOL intersections
          addGDefLinks (cN, iN, cE) n = let
             g = dgBody dg
             allGDef = all $ \ (_, _, l) -> isGlobalDef $ dgl_type l
             gDefPaths x y = filter allGDef $ getPathsTo x y g
             nPaths = concat $ concatMap (gDefPaths n) cN
             nNodes = concatMap (\ (x, y, _) -> [x, y]) nPaths
             hideLinks = filter (\ (_, _, l) -> dgl_type l == HidingDefLink)
                $ concatMap (inn g) $ cN ++ nNodes
             hNodes = map (\ (x, _, _) -> x) hideLinks
             implicitNodes = nub $ iN ++ nNodes ++ hNodes
             intersectLinks = filter (\ (_, _, l) -> dgl_origin l == DGLinkIntersect)
                              $ concatMap (inn g) $ cN ++ implicitNodes
             in (cN, implicitNodes
                , nub $ nPaths ++ cE ++ hideLinks ++ intersectLinks)
          addLinks (cN, cE) = foldl addGDefLinks (cN, [], cE) cN
          (cNodes, iNodes, cEdges) =
             addLinks . foldl (getNodes False) ([], []) $ getItems cItems
          (eNodes, eEdges) = foldl (getNodes True) ([], []) eItems
          (cNodes', cEdges') = (nub (cNodes ++ iNodes) \\ eNodes,
                                cEdges \\ eEdges)
   in (cNodes', cEdges')
    
  getItems :: [LABELED_ONTO_OR_INTPR_REF] -> [IRI]
  getItems [] = []
  getItems (Labeled _ i : r) = i : getItems r
  
  instMismatchError :: IRI -> Int -> Int -> Range -> Result a
  instMismatchError spname lp la = fatal_error $ iriToStringUnsecure spname
      ++ " expects " ++ show lp ++ " arguments" ++ " but was given " ++ show la
  
  notFoundError :: String -> IRI -> Result a
  notFoundError str sid = fatal_error (str ++ " '" ++ iriToStringUnsecure sid
      ++ "' or '" ++ iriToStringShortUnsecure sid ++ "' not found") $ iriPos sid
  
  gsigUnionMaybe :: LogicGraph -> Bool -> MaybeNode -> G_sign -> Result G_sign
  gsigUnionMaybe lg both mn gsig = case mn of
    EmptyNode _ -> return gsig
    JustNode ns -> gsigUnion lg both (getSig ns) gsig
  
  anaExtraction :: LogicGraph -> LibEnv -> LibName -> DGraph -> NodeSig -> NodeName -> Range ->
                EXTRACTION -> Result (NodeSig, DGraph)
  anaExtraction lg libEnv ln dg nsig name rg (ExtractOrRemove b iris _) = if not b then
    Fail.fail "analysis of remove not implemented yet"
   else do
    let dg0 = markHiding libEnv dg
        n = getNode nsig
    if labelHasHiding $ labDG dg0 n then
      Fail.fail "cannot extract module from a non-flattenable OMS"
     else do
      let dgThm = computeDGraphTheories libEnv ln dg0
          gth = case (globalTheory . labDG dgThm) n  of
                 Nothing -> error "not able to compute theory"
                 Just th -> th
      mTh <- case gth of
          G_theory lid syntax (ExtSign sig _) _ gsens _ -> do
            let nsens = toNamedList gsens
            (msig, msens) <- extract_module lid iris (sig, nsens)
            return $ G_theory lid syntax
                              (ExtSign msig $ foldl Set.union Set.empty $ sym_of lid msig) startSigId
                              (toThSens msens) startThId
      let (nsig', dg') = insGTheory dg (setSrcRange rg name) DGExtract mTh
      incl <- ginclusion lg (getSig nsig') (getSig nsig)
      let  dg'' = insLink dg' incl globalThm SeeSource (getNode nsig') n
      return (nsig', dg'')
  
  anaUnion :: Bool -> LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> NodeName
    -> HetcatsOpts -> ExpOverrides -> [Annoted SPEC] -> Range
    -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
  anaUnion addSyms lg libEnv ln dg nsig name opts eo asps rg = case asps of
    [] -> Fail.fail "empty union"
    _ -> do
        let sps = map item asps
        (sps', nsigs, dg', _) <-
            let ana (sps1, nsigs, dg', n) sp' = do
                  let n1 = inc n
                  (sp1, nsig', dg1) <-
                    anaSpec addSyms True lg libEnv ln 
                            dg' nsig n1 opts eo sp' $ getRange sp'
                  return (sp1 : sps1, nsig' : nsigs, dg1, n1)
             in foldM ana ([], [], dg, extName "Union" name) sps
        let newAsps = zipWith replaceAnnoted (reverse sps') asps
        case nsigs of
          [ns] -> return (newAsps, nsigs, ns, dg')
          _ -> do
            let nsigs' = reverse nsigs
            gbigSigma <- gsigManyUnion lg (map getSig nsigs')
            let (ns@(NodeSig node _), dg2) = insGSig dg' (setSrcRange rg name)
                  DGUnion gbigSigma
                insE dgl (NodeSig n gsigma) = do
                  incl <- ginclusion lg gsigma gbigSigma
                  return $ insLink dgl incl globalDef SeeTarget n node
            dg3 <- foldM insE dg2 nsigs'
            return (newAsps, nsigs', ns, dg3)
  
  anaIntersect :: Bool -> LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> NodeName
    -> HetcatsOpts -> ExpOverrides -> [Annoted SPEC] -> Range
    -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
  anaIntersect addSyms lg libEnv ln dg nsig name opts eo asps rg = case asps of
    [] -> Fail.fail "empty intersection"
    _ -> do
        let sps = map item asps
            ana (sps1, nsigs, dg', n) sp' = do
                  let n1 = inc n
                  (sp1, nsig', dg1) <-
                    anaSpec addSyms True lg libEnv ln dg' nsig n1 opts eo sp' $
                            getRange sp'
                  return (sp1 : sps1, nsig' : nsigs, dg1, n1)
        (sps', nsigs, dg', _) <-
          foldM ana ([], [], dg, extName "Intersect" name) sps
        let newAsps = zipWith replaceAnnoted (reverse sps') asps
        case nsigs of
          [ns] -> return (newAsps, nsigs, ns, dg')
          _ -> do
            let nsigs' = reverse nsigs
                labelHidings = map labelHasHiding $ map (\n -> labDG (markHiding libEnv dg) $ getNode n) nsigs'
                hasHiding = foldl (\x y -> x || y) False labelHidings
            case hasHiding of
              True -> Fail.fail "Intersection is defined only for flattenable theories"
              False -> do
               let dgThm = computeDGraphTheories libEnv ln dg
                   theo:theos = map (\x -> case (globalTheory . labDG dgThm . getNode) x of
                                              Nothing -> error $ "not able to compute theory of node" ++ (show $ getNode x)
                                              Just th -> th) nsigs'
               gbigSigma <- gsigManyIntersect lg (map getSig nsigs')
               gth <- foldM (intersectG_sentences gbigSigma) theo theos
               let (ns@(NodeSig node _), dg2) = insGTheory dg' (setSrcRange rg name)
                      DGIntersect gth
                   insE dgl (NodeSig n gsigma) = do
                     incl <- ginclusion lg gbigSigma gsigma
                     return $ insLink dgl incl globalThm DGLinkIntersect node n
               dg3 <- foldM insE dg2 nsigs'
               return (newAsps, nsigs', ns, dg3)
  
  anaFiltering :: LogicGraph -> LibEnv -> LibName -> DGraph -> NodeSig -> NodeName-> FILTERING
     -> Result (NodeSig, DGraph)
  anaFiltering lg libEnv ln dg nsig nname filtering = case filtering of
    FilterSymbolList selectOrReject (G_symb_items_list lidS sItems) _ ->
     if not selectOrReject then do
       let strs = concatMap (symb_items_name lidS) sItems
           dgThm = computeDGraphTheories libEnv ln dg
           th =
              case (globalTheory . labDG dgThm . getNode) nsig of
                    Nothing -> error "error computing theory"
                    Just t -> t
       case th of
        G_theory l1 ser1 sig1 ind1 sens1 ind1' -> do
           let gth' = G_theory l1 ser1 sig1 ind1
                      (foldl (\m x -> Map.delete x m) sens1 strs) ind1'
           let (ns@(NodeSig node gsigma), dg') = insGTheory dg nname DGEmpty gth'
           gmor <- ginclusion lg gsigma $ getSig nsig
           let dg2 = insLink dg' gmor globalThm SeeSource node $ getNode nsig
           return (ns, dg2)
      else error "analysis of select not implemented yet"
    FilterBasicSpec _ _ _ -> error "filtering a basic spec not implemented yet"
  
  
  -- analysis of renamings
  anaRen :: LogicGraph -> HetcatsOpts -> MaybeNode -> Range -> GMorphism
    -> G_mapping -> Result GMorphism
  anaRen lg opts lenv pos gmor@(GMorphism r sigma ind1 mor _) gMapping =
    adjustPos pos $ case gMapping of
    G_symb_map (G_symb_map_items_list lid sis) ->
      let lid2 = targetLogic r in
      if language_name lid2 == language_name lid then
       if isStructured opts then return gmor else do
        sis1 <- coerceSymbMapItemsList lid lid2 "Analysis of renaming" sis
        src@(ExtSign sig _) <- return $ makeExtSign lid2 $ cod mor
        rmap <- stat_symb_map_items lid2 sig Nothing sis1
        mor1 <- ext_induced_from_morphism lid2 rmap src
        case lenv of
          EmptyNode _ -> return ()
          JustNode (NodeSig _ sigLenv) -> do
            -- needs to be changed for logic translations
            (G_sign lid1 sigmaLenv1 _, _) <-
                gSigCoerce lg sigLenv (Logic lid2)
            sigmaLenv' <- coerceSign lid1 lid2 "" sigmaLenv1
            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
            unless (Set.null forbiddenSys) $ plain_error () (
              "attempt to rename the following symbols from " ++
              "the local environment:\n" ++ showDoc forbiddenSys "") pos
        mor2 <- comp mor mor1
        return $ GMorphism r sigma ind1 mor2 startMorId
      else do
        comor <- logicInclusion lg (Logic lid2) (Logic lid)
        gmorTrans <- gEmbedComorphism comor $ cod gmor
        newMor <- comp gmor gmorTrans
        anaRen lg opts lenv pos newMor gMapping
    G_logic_translation (Logic_code tok src tar pos1) ->
      let pos2 = if pos1 == nullRange then pos else pos1
          adj1 = adjustPos pos2
      in adj1 $ do
      G_sign srcLid srcSig ind <- return (cod gmor)
      c <- case tok of
              Just c -> lookupComorphism c lg
              Nothing -> case tar of
                 Just (Logic_name l _ _) ->
                   lookupLogic "with logic: " l lg
                   >>= logicInclusion lg (Logic srcLid)
                 Nothing -> Fail.fail "with logic: cannot determine comorphism"
      checkSrcOrTarLogic pos2 True c src
      checkSrcOrTarLogic pos2 False c tar
      mor1 <- gEmbedComorphism c (G_sign srcLid srcSig ind)
      comp gmor mor1
  
  checkSrcOrTarLogic :: Range -> Bool -> AnyComorphism -> Maybe Logic_name
                        -> Result ()
  checkSrcOrTarLogic pos b (Comorphism cid) ml = case ml of
    Nothing -> return ()
    Just (Logic_name s _ _) ->
        when (s /= if b then language_name $ sourceLogic cid
                   else language_name $ targetLogic cid)
          $ plain_error () (s ++ " is is not the "
             ++ (if b then "source" else "target") ++ " logic of "
             ++ language_name cid) pos
  
  anaRenaming :: LogicGraph -> MaybeNode -> G_sign -> HetcatsOpts -> RENAMING
    -> Result GMorphism
  anaRenaming lg lenv gSigma opts (Renaming ren pos) =
        foldM (anaRen lg opts lenv pos) (ide gSigma) ren
  
  getRestrLogic :: RESTRICTION -> Result AnyLogic
  getRestrLogic restr = case restr of
    Revealed (G_symb_map_items_list lid _) _ -> return $ Logic lid
    Hidden l _ -> case l of
      [] -> error "getRestrLogic"
      h : _ -> case h of
        G_symb_list (G_symb_items_list lid _) -> return $ Logic lid
        G_logic_projection (Logic_code _ _ _ pos1) ->
          fatal_error "no analysis of logic projections yet" pos1
  
  -- analysis of restrictions
  anaRestr :: LogicGraph -> G_sign -> Range -> GMorphism -> G_hiding
    -> Result GMorphism
  anaRestr lg sigEnv 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
          sis1 <- coerceSymbItemsList lid' lid1 "Analysis of restriction1" sis'
          rsys <- stat_symb_items lid1 sigma1 sis1
          let sys = symset_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
          unless (null unmatched)
            $ plain_error () ("attempt to hide unknown symbols:\n"
                            ++ showDoc unmatched "") pos
          -- needs to be changed when logic projections are implemented
          (G_sign lidE sigmaLenv0 _, _) <- gSigCoerce lg sigEnv (Logic lid1)
          sigmaLenv' <- coerceSign lidE lid1 "" sigmaLenv0
          let sysLenv = ext_sym_of lid1 sigmaLenv'
              forbiddenSys = sys' `Set.intersection` sysLenv
          unless (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 mor1' mor
          return $ GMorphism cid (ExtSign (dom 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 _ _ _ pos1) ->
          fatal_error "no analysis of logic projections yet" pos1
  
  anaRestriction :: LogicGraph -> G_sign -> G_sign -> HetcatsOpts -> RESTRICTION
    -> Result (GMorphism, Maybe GMorphism)
  anaRestriction lg gSigma gSigma'@(G_sign lid0 sig0 _) opts restr =
    if isStructured opts then return (ide gSigma, Nothing) else
    case restr of
      Hidden rstr pos -> do
        mor <- foldM (anaRestr lg gSigma pos) (ide gSigma') rstr
        return (mor, Nothing)
      Revealed (G_symb_map_items_list lid1 sis) pos -> adjustPos pos $ do
        (G_sign lid sigma _, _) <- gSigCoerce lg gSigma (Logic lid1)
        sigma0 <- coerceSign lid lid1 "reveal1" sigma
        sigma1 <- coerceSign lid0 lid1 "reveal2" sig0
        let sys = ext_sym_of lid1 sigma0 -- local env
            sys' = ext_sym_of lid1 sigma1 -- "big" signature
        rmap <- stat_symb_map_items lid1 (plainSign sigma1) Nothing sis
        let sys'' = Set.fromList
             [sy | sy <- Set.toList sys', rsy <-
                         Map.keys rmap, matches lid1 sy rsy]
            {- domain of rmap intersected with sys'
            rmap is checked by ext_induced_from_morphism below -}
        mor1 <- ext_generated_sign lid1 (sys `Set.union` sys'') sigma1
        let extsig1 = makeExtSign lid1 $ dom mor1
        mor2 <- ext_induced_from_morphism lid1 rmap extsig1
        return (gEmbed2 (G_sign lid1 extsig1 startSigId)
                        $ G_morphism lid1 mor1 startMorId
               , Just $ gEmbed $ mkG_morphism lid1 mor2)
  
  partitionGmaps :: [G_mapping] -> ([G_mapping], [G_mapping])
  partitionGmaps l = let
    (hs, rs) = span (\ sm -> case sm of
      G_symb_map _ -> True
      G_logic_translation _ -> False) $ reverse l
    in (reverse rs, reverse hs)
  
  anaGmaps :: LogicGraph -> HetcatsOpts -> Range -> G_sign -> G_sign
    -> [G_mapping] -> Result G_morphism
  anaGmaps lg opts pos psig@(G_sign lidP sigmaP _) asig@(G_sign lidA sigmaA _)
    gsis = adjustPos pos $ if isStructured opts
      then return $ mkG_morphism lidP $ ext_ide sigmaP
      else if null gsis then do
          (G_sign lidP' sigmaP' _, _) <- gSigCoerce lg psig (Logic lidA)
          sigmaA' <- coerceSign lidA lidP' "anaGmaps" sigmaA
          fmap (mkG_morphism lidP') $
            ext_induced_from_to_morphism lidP' Map.empty sigmaP' sigmaA'
        else do
        cl <- lookupCurrentLogic "anaGmaps" lg
        G_symb_map_items_list lid sis <- homogenizeGM cl gsis
        (G_sign lidP' sigmaP'' _, _) <- gSigCoerce lg psig (Logic lid)
        sigmaP' <- coerceSign lidP' lid "anaGmaps1" sigmaP''
        (G_sign lidA' sigmaA'' _, _) <- gSigCoerce lg asig (Logic lid)
        sigmaA' <- coerceSign lidA' lid "anaGmaps2" sigmaA''
        rmap <- stat_symb_map_items lid (plainSign sigmaP')
          (Just $ plainSign sigmaA') sis
        fmap (mkG_morphism lid)
          $ ext_induced_from_to_morphism lid rmap sigmaP' sigmaA'
  
     {-
     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 symbols that are affected
     -}
  
  anaFitArg :: LogicGraph -> LibEnv -> LibName -> DGraph -> IRI -> MaybeNode
    -> NodeSig -> HetcatsOpts -> NodeName -> ExpOverrides -> FIT_ARG
    -> Result (FIT_ARG, DGraph, (G_morphism, NodeSig))
  anaFitArg lg libEnv ln dg spname nsigI nsigP@(NodeSig nP gsigmaP) opts name eo fv =
    let ga = globalAnnos dg in
    case fv of
    Fit_spec asp gsis pos -> do
     (sp', nsigA, dg') <- anaSpec False True lg libEnv ln 
                                  dg nsigI name opts eo (item asp) pos
     (_, Comorphism aid) <-
         logicUnion lg (getNodeLogic nsigP) (getNodeLogic nsigA)
     let tl = Logic $ targetLogic aid
     (nsigA'@(NodeSig nA' gsigA'), dg'') <- coerceNode lg libEnv ln dg' nsigA name tl
     (gsigmaP', pmor) <- gSigCoerce lg gsigmaP tl
     tmor <- gEmbedComorphism pmor gsigmaP
     gmor <- anaGmaps lg opts pos gsigmaP' gsigA' gsis
     eGmor <- comp tmor $ gEmbed gmor
     return ( Fit_spec (replaceAnnoted sp' asp) gsis pos
            , if nP == nA' && isInclusion eGmor then dg'' else
                  insLink dg'' eGmor globalThm
                     (DGLinkInst spname $ Fitted gsis) nP nA'
            , (gmor, nsigA'))
    Fit_view vn' afitargs pos -> do
     vn <- expCurieR ga eo vn'
     case lookupGlobalEnvDG vn dg of
      Just (ViewOrStructEntry _ (ExtViewSig (NodeSig nSrc gsigmaS) mor
        gs@(ExtGenSig (GenSig _ params _) target@(NodeSig nTar _))))
          -> adjustPos pos $ do
        GMorphism cid _ _ morHom ind <- return mor
        let lid = targetLogic cid
            pname = dgn_name $ labDG dg nP
            gsigmaI = getMaybeSig nsigI
        dg5 <- do
          gsigmaIS <- gsigUnionMaybe lg True nsigI gsigmaS
          unless (isSubGsign lg gsigmaP gsigmaIS
                  && isSubGsign lg gsigmaIS gsigmaP)
               (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)
          (dg4, iSrc) <- case nsigI of
            EmptyNode _ -> return (dg, nSrc)
            JustNode (NodeSig nI _) -> do
              inclI <- ginclusion lg gsigmaI gsigmaIS
              inclS <- ginclusion lg gsigmaS gsigmaIS
              let (NodeSig n' _, dg1) = insGSig dg (extName "View" name)
                    {xpath = xpath pname} (DGFitView vn) gsigmaIS
                  dg2 = insLink dg1 inclI globalDef
                        (DGLinkFitViewImp vn) nI n'
              return (insLink dg2 inclS globalDef
                      (DGLinkFitViewImp vn) nSrc n', n')
          if nP == iSrc then return dg4 else do
            gmor <- ginclusion lg gsigmaP gsigmaIS
            return $ insLink dg4 gmor globalThm (DGLinkFitView vn) nP iSrc
        case (length afitargs, length params) of
        -- the case without parameters leads to a simpler dg
          (0, 0) -> return (fv, dg5, (G_morphism lid morHom ind, target))
          -- now the case with parameters
          (la, lp) | la == lp -> do
            (ffitargs, dg', (gmor_f, _, ns@(NodeSig nA _))) <-
              anaAllFitArgs lg libEnv opts eo ln dg5 (EmptyNode $ Logic lid)
                name vn gs afitargs
            mor1 <- comp mor gmor_f
            GMorphism cid1 _ _ theta _ <- return mor1
            let lid1 = targetLogic cid1
            when (language_name (sourceLogic cid1) /= language_name lid1)
              $ fatal_error "heterogeneous fitting views not yet implemented"
                pos
            let dg9 = insLink dg' gmor_f globalDef (DGLinkMorph vn) nTar nA
            return (Fit_view vn ffitargs pos, dg9, (mkG_morphism lid1 theta, ns))
           | otherwise -> instMismatchError spname lp la pos
      _ -> notFoundError "view" vn
  
  anaFitArgs :: LogicGraph -> LibEnv -> HetcatsOpts -> ExpOverrides -> LibName -> IRI
    -> MaybeNode
    -> ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NodeName)
    -> (NodeSig, FIT_ARG)
    -> Result ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NodeName)
  anaFitArgs lg libEnv opts eo ln spname imps (fas', dg1, args, name') (nsig', fa) = do
      let n1 = inc name'
      (fa', dg', arg) <- anaFitArg lg libEnv ln dg1 spname imps nsig' opts n1 eo fa
      return (fa' : fas', dg', arg : args, n1)
  
  anaAllFitArgs :: LogicGraph -> LibEnv -> HetcatsOpts -> ExpOverrides -> LibName -> DGraph
    -> MaybeNode
    -> NodeName -> IRI -> ExtGenSig -> [Annoted FIT_ARG]
    -> Result ([Annoted FIT_ARG], DGraph, (GMorphism, G_sign, NodeSig))
  anaAllFitArgs lg libEnv opts eo ln dg nsig name spname
    gs@(ExtGenSig (GenSig imps params _) _)
    afitargs = do
    let fitargs = map item afitargs
    (fitargs', dg', args, _) <- foldM (anaFitArgs lg libEnv opts eo ln spname imps)
             ([], dg, [], extName "Actuals" name) (zip params fitargs)
    let actualargs = reverse args
    (gsigma', morDelta) <- applyGS lg gs actualargs
    gsigmaRes <- gsigUnionMaybe lg True nsig gsigma'
    let (ns, dg2) = insGSig dg' name (DGInst spname) gsigmaRes
    dg3 <- foldM (parLink lg nsig (DGLinkInstArg spname) ns) dg2
      $ map snd actualargs
    return ( zipWith replaceAnnoted (reverse fitargs') afitargs, dg3
           , (morDelta, gsigma', ns))
  
  parLink :: LogicGraph -> MaybeNode -> DGLinkOrigin -> NodeSig -> DGraph
             -> NodeSig -> Result DGraph
  parLink lg nsig orig (NodeSig node gsigma') dg (NodeSig nA_i sigA_i) =
    case nsig of
      JustNode (NodeSig nI _) | nI == nA_i -> return dg
        -- actual parameter will be included via import
      _ -> do
        incl <- ginclusion lg sigA_i gsigma'
        return $ insLink dg incl globalDef orig nA_i node
  
  {- 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 <- mapM (mapID idmap) comps
        return (Id toks compsnew pos1)
      Just ids -> case Set.toList ids of
        [] -> return i
        [h] -> return h
        _ -> 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 <- mapM (mapID idmap) comps
    return $ if comps == compsnew then m1 else
      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 :: Bool -- ^ check sharing (False for lambda expressions)
                 -> G_sign      -- ^ formal parameter
                 -> G_sign      -- ^ body
                 -> G_sign      -- ^ actual parameter
                 -> G_morphism  -- ^ fitting morphism
                 -> Result (G_sign, G_morphism)
  extendMorphism sharing (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 map1" sigmaB1
    sigmaA <- coerceSign lidA lid "Extension of symbol map2" sigmaA1
    fittingMor <- coerceMorphism lidM lid "Extension of symbol map3" 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.foldrWithKey
            (on Map.insert $ symbol_to_raw lid) Map.empty
        rh = symbMapToRawSymbMap h
        idh = Map.foldrWithKey (on setInsert $ sym_name lid) Map.empty h
    idhExt <- extID idsB idh
    let rIdExt = Map.foldrWithKey (on Map.insert $ id_to_raw lid) Map.empty
                  (foldr Map.delete 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 mor) $ Set.map (\ sy ->
          Map.findWithDefault sy sy hmor) sysB
    sigma <- ext_signature_union lid sigmaA sigmaAD
    let illShared = (ext_sym_of lid sigmaA `Set.intersection`
                                ext_sym_of lid sigmaAD )
                     Set.\\ imageSet h symsP
    unless (Set.null illShared || not sharing)
      $ plain_error () ("Symbols shared between actual parameter and body"
                       ++ "\nmust be in formal parameter:\n"
                       ++ showDoc illShared "") nullRange
    let myKernel = Set.fromDistinctAscList . comb1 . Map.toList
        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
    unless (Set.null newIdentifications)
      $ warning () (
       "Fitting morphism may lead to forbidden identifications:\n"
       ++ showDoc newIdentifications "") nullRange
    incl <- ext_inclusion lid sigmaAD sigma
    mor1 <- comp mor incl
    return (G_sign lid sigma startSigId, mkG_morphism lid mor1)
  
  applyGS :: LogicGraph -> ExtGenSig -> [(G_morphism, NodeSig)]
           -> Result (G_sign, GMorphism)
  applyGS lg (ExtGenSig (GenSig nsigI _ gsigmaP) nsigB) args = do
    let mor_i = map fst args
        gsigmaA_i = map (getSig . snd) args
        gsigmaB = getSig nsigB
    gsigmaA@(G_sign lidA _ _) <- gsigManyUnion lg gsigmaA_i
    (Comorphism bid, Comorphism uid) <-
      logicUnion lg (getNodeLogic nsigB) (Logic lidA)
    let cl = Logic $ targetLogic uid
    G_morphism lidG mor0 _ <- case nsigI of
      EmptyNode _ -> homogeneousMorManyUnion mor_i
      JustNode (NodeSig _ gsigmaI) -> do
        (G_sign lidI sigmaI _, _) <- gSigCoerce lg gsigmaI (Logic lidA)
        let idI = ext_ide sigmaI
        homogeneousMorManyUnion $ mkG_morphism lidI idI : mor_i
    (gsigmaP', _) <- gSigCoerce lg (getMaybeSig gsigmaP) cl
    (gsigmaB', _) <- gSigCoerce lg gsigmaB cl
    (gsigmaA', Comorphism aid) <- gSigCoerce lg gsigmaA cl
    mor1 <- coerceMorphism lidG (sourceLogic aid) "applyGS" mor0
    mor2 <- map_morphism aid mor1
    (gsig, G_morphism gid mor3 mId) <- extendMorphism True gsigmaP' gsigmaB'
      gsigmaA' $ G_morphism (targetLogic aid) mor2 startMorId
    case gsigmaB of
      G_sign lidB sigB indB -> do
        sigB' <- coerceSign lidB (sourceLogic bid) "applyGS2" sigB
        mor4 <- coerceMorphism gid (targetLogic bid) "applyGS3" mor3
        return (gsig, GMorphism bid sigB' indB mor4 mId)
  
  homogenizeGM :: AnyLogic -> [G_mapping] -> Result G_symb_map_items_list
  homogenizeGM (Logic lid) =
    foldM homogenize1 (G_symb_map_items_list lid [])
    where
    homogenize1 (G_symb_map_items_list lid2 sis) sm = case sm of
      G_symb_map (G_symb_map_items_list lid1 sis1) -> do
           sis1' <- coerceSymbMapItemsList lid1 lid2 "homogenizeGM" sis1
           return $ G_symb_map_items_list lid2 $ sis ++ sis1'
      G_logic_translation lc ->
           Fail.fail $ "translation not supported by " ++ showDoc lc ""
  
  getSpecAnnos :: Range -> Annoted a -> Result (Conservativity, Bool)
  getSpecAnnos pos a = do
    let sannos = filter isSemanticAnno $ l_annos a
        (sanno1, conflict, impliesA) = case sannos of
          f@(Semantic_anno anno1 _) : r -> (case anno1 of
                  SA_cons -> Cons
                  SA_def -> Def
                  SA_mono -> Mono
                  _ -> None, any (/= f) r,
                       anno1 == SA_implies || anno1 == SA_implied)
          _ -> (None, False, False)
    when conflict $ plain_error () "Conflicting semantic annotations" pos
    return (sanno1, impliesA)
  
  -- only consider addSyms for the first spec
  anaExtension :: LogicGraph -> LibEnv -> HetcatsOpts -> ExpOverrides -> LibName -> Range
      -> ([SPEC], MaybeNode, DGraph, Conservativity, Bool)
      -> (NodeName, Annoted SPEC)
      -> Result ([SPEC], MaybeNode, DGraph, Conservativity, Bool)
  anaExtension lg libEnv opts eo ln pos (sps', nsig', dg', conser, addSyms) (name', asp')
    = do
    (sanno1, impliesA) <- getSpecAnnos pos asp'
    -- attach conservativity to definition link
    let sp = item asp'
    (sp1', nsig1@(NodeSig n1 sig1), dg1) <- anaSpecTop (max conser sanno1)
      addSyms lg libEnv ln dg' nsig' name' opts eo sp $ getRange sp
    dg2 <- if impliesA then case nsig' of
      JustNode (NodeSig n' sig') -> do
        -- is the extension going between real nodes?
        unless (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 sig1) globalThm DGImpliesLink n1 n'
      _ -> return dg1
     else return dg1
    return (sp1' : sps', JustNode nsig1, dg2, None, True)
  
  
  -- BEGIN CURIE expansion
  
  expCurieR :: GlobalAnnos -> ExpOverrides -> IRI -> Result IRI
  expCurieR ga eo i = maybe (prefixErrorIRI i) return $ expCurie ga eo i
  
  expCurie :: GlobalAnnos -> ExpOverrides -> IRI -> Maybe IRI
  expCurie ga eo i =
    let pm = prefix_map ga
    in case Map.lookup i eo of
          Nothing -> expandCurie pm i
          Just path -> expandCurieByPath path i
  
  expandCurieByPath :: FilePath -> IRI -> Maybe IRI
  expandCurieByPath path i = case parseIRIReference $ path ++ "?" of
            Nothing -> Nothing
            Just p -> expandCurie (Map.singleton "" p) i
  
  prefixErrorIRI :: IRI -> Result a
  prefixErrorIRI i = fatal_error ("No prefix found for CURIE " ++
      iriToStringUnsecure i ++ " or expansion does not yield a valid IRI.")
      $ iriPos i
  
  -- END CURIE expansion
  