8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer{-# LANGUAGE RankNTypes, GeneralizedNewtypeDeriving #-}

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer{- |

6bcc9da85b73c324e14365759791daf895b0738cChristian MaederModule : $Header$

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyerDescription : Central datastructures for development graphs

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerLicense : GPLv2 or higher, see LICENSE.txt

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerMaintainer : till@informatik.uni-bremen.de

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerStability : provisional

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerPortability : non-portable(Logic)

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerCentral datastructures for development graphs

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Follows Sect. IV:4.2 of the CASL Reference Manual.

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerWe also provide functions for constructing and modifying development graphs.

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerHowever note that these changes need to be propagated to the GUI if they

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyeralso shall be visible in the displayed development graph.

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-}

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer{-

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer References:

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer T. Mossakowski, S. Autexier and D. Hutter:

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Extending Development Graphs With Hiding.

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Lecture Notes in Computer Science 2029, p. 269-283,

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Springer-Verlag 2001.

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer T. Mossakowski, S. Autexier, D. Hutter, P. Hoffman:

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer CASL Proof calculus. In: CASL reference manual, part IV.

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Available from http://www.cofi.info

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-}

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyermodule Static.DevGraph where

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Syntax.AS_Structured

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Syntax.AS_Library

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Static.GTheory

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Logic.Logic

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Logic.ExtSign

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Logic.Comorphism

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Logic.Grothendieck

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Logic.Prover

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport qualified Common.Lib.Rel as Rel

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport qualified Common.Lib.Graph as Tree

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport qualified Common.Lib.SizedList as SizedList

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport qualified Common.OrderedMap as OMap

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Common.AS_Annotation

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Common.GlobalAnnotations

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Common.Id

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Common.Utils (numberSuffix, splitByList)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Common.LibName

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Common.Consistency

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Control.Concurrent.MVar

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Control.Exception (assert)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Data.Graph.Inductive.Basic

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Data.Graph.Inductive.Graph as Graph

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Data.Graph.Inductive.Query.DFS

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Data.List

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Data.Maybe

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Data.Ord

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport qualified Data.Map as Map

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport qualified Data.Set as Set

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerimport Common.Result

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- * types for structured specification analysis

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- ** basic types

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | Node with signature in a DG

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata NodeSig = NodeSig { getNode :: Node, getSig :: G_sign }

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer deriving (Eq, Show)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer{- | NodeSig or possibly the empty sig in a logic

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer (but since we want to avoid lots of vsacuous nodes with empty sig,

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer we do not assign a real node in the DG here) -}

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata MaybeNode = JustNode NodeSig | EmptyNode AnyLogic deriving (Show, Eq)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata BasicConsProof = BasicConsProof deriving (Show, Eq) -- needs more details

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- ** node label types

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata XPathPart = ElemName String | ChildIndex Int deriving (Show, Eq, Ord)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer{- | name of a node in a DG; auxiliary nodes may have extension string

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer and non-zero number (for these, names are usually hidden). -}

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata NodeName = NodeName

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer { getName :: SIMPLE_ID

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , extString :: String

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , extIndex :: Int

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , xpath :: [XPathPart]

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer } deriving (Show, Eq, Ord)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerisInternal :: NodeName -> Bool

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerisInternal n = extIndex n /= 0 || not (null $ extString n)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | a wrapper for renamings with a trivial Ord instance

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyernewtype Renamed = Renamed RENAMING deriving Show

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerinstance Ord Renamed where

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer compare _ _ = EQ

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerinstance Eq Renamed where

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer _ == _ = True

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | a wrapper for restrictions with a trivial Ord instance

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyernewtype Restricted = Restricted RESTRICTION deriving Show

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerinstance Ord Restricted where

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer compare _ _ = EQ

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerinstance Eq Restricted where

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer _ == _ = True

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer{- | Data type indicating the origin of nodes and edges in the input language

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer This is not used in the DG calculus, only may be used in the future

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer for reconstruction of input and management of change. -}

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata DGOrigin =

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer DGEmpty

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGBasic

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGBasicSpec (Maybe G_basic_spec) G_sign (Set.Set G_symbol)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGExtension

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGLogicCoercion

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGTranslation Renamed

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGUnion

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGRestriction Restricted

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGRevealTranslation

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGFreeOrCofree FreeOrCofree

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGLocal

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGClosed

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGLogicQual

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGData

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGFormalParams

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGImports

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGInst SIMPLE_ID

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGFitSpec

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGFitView SIMPLE_ID

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGProof

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGNormalForm Node

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGintegratedSCC

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGFlattening

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer deriving (Show, Eq, Ord)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer-- | node content or reference to another library's node

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata DGNodeInfo = DGNode

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer { node_origin :: DGOrigin -- origin in input language

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , node_cons_status :: ConsStatus } -- like a link from the empty signature

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGRef -- reference to node in a different DG

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer { ref_libname :: LibName -- pointer to DG where ref'd node resides

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , ref_node :: Node -- pointer to ref'd node

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer } deriving (Show, Eq)

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer{- | node inscriptions in development graphs.

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyerNothing entries indicate "not computed yet" -}

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyerdata DGNodeLab =

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer DGNodeLab

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer { dgn_name :: NodeName -- name in the input language

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , dgn_theory :: G_theory -- local theory

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , globalTheory :: Maybe G_theory -- global theory

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , labelHasHiding :: Bool -- has this node an ingoing hiding link

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , labelHasFree :: Bool -- has incoming free definition link

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , dgn_nf :: Maybe Node -- normal form, for Theorem-Hide-Shift

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , dgn_sigma :: Maybe GMorphism -- inclusion of signature into nf signature

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , dgn_freenf :: Maybe Node -- normal form for freeness

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , dgn_phi :: Maybe GMorphism -- morphism from signature to nffree signature

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , nodeInfo :: DGNodeInfo

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , dgn_lock :: Maybe (MVar ())

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , dgn_symbolpathlist :: G_symbolmap [SLinkPath]

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer } deriving (Show, Eq)

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyerinstance Show (MVar a) where

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer show _ = ""

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyerisDGRef :: DGNodeLab -> Bool

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyerisDGRef l = case nodeInfo l of

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer DGNode {} -> False

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer DGRef {} -> True

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyersensWithKind :: (forall a . SenStatus a (AnyComorphism, BasicProof) -> Bool)

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer -> G_theory -> [String]

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyersensWithKind f (G_theory _lid _sigma _ sens _) = Map.keys $ OMap.filter f sens

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyerhasSenKind :: (forall a . SenStatus a (AnyComorphism, BasicProof) -> Bool)

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer -> DGNodeLab -> Bool

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyerhasSenKind f = not . null . sensWithKind f . dgn_theory

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer-- | test if a given node label has local open goals

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyerhasOpenGoals :: DGNodeLab -> Bool

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyerhasOpenGoals = hasSenKind (\ s -> not (isAxiom s) && not (isProvenSenStatus s))

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer-- | check if the node has an internal name

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyerisInternalNode :: DGNodeLab -> Bool

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyerisInternalNode DGNodeLab {dgn_name = n} = isInternal n

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyergetNodeConsStatus :: DGNodeLab -> ConsStatus

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyergetNodeConsStatus lbl = case nodeInfo lbl of

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer DGRef {} -> mkConsStatus None

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer DGNode { node_cons_status = c } -> c

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyergetNodeCons :: DGNodeLab -> Conservativity

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetNodeCons = getConsOfStatus . getNodeConsStatus

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | returns the Conservativity if the given node has one, otherwise none

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyergetNodeConservativity :: LNode DGNodeLab -> Conservativity

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetNodeConservativity = getNodeCons . snd

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer{- | test if a node conservativity is open,

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerreturn input for refs or nodes with normal forms -}

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerhasOpenNodeConsStatus :: Bool -> DGNodeLab -> Bool

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyerhasOpenNodeConsStatus b lbl = if isJust $ dgn_nf lbl then b else

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer hasOpenConsStatus b $ getNodeConsStatus lbl

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermarkNodeConsistency :: Conservativity -> String -> DGNodeLab -> DGNodeLab

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermarkNodeConsistency newc str dgnode = dgnode

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer { nodeInfo = case nodeInfo dgnode of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ninfo@DGNode { node_cons_status = ConsStatus c pc thm } ->

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer if pc == newc && isProvenThmLinkStatus thm then ninfo else

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ninfo { node_cons_status = ConsStatus c newc

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer $ Proven (DGRule $ showConsistency newc ++ str)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer emptyProofBasis }

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer ninfo -> ninfo }

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyermarkNodeConsistent :: String -> DGNodeLab -> DGNodeLab

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyermarkNodeConsistent = markNodeConsistency Cons

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyermarkNodeInconsistent :: String -> DGNodeLab -> DGNodeLab

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermarkNodeInconsistent = markNodeConsistency Inconsistent

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer-- | test if a conservativity is open, return input for None

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyerhasOpenConsStatus :: Bool -> ConsStatus -> Bool

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyerhasOpenConsStatus b (ConsStatus cons _ thm) = case cons of

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer None -> b

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer _ -> not $ isProvenThmLinkStatus thm

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyerdata DGNodeType = DGNodeType

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer { isRefType :: Bool

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , isProvenNode :: Bool

1468136df5b66f8e94b60d3b1c00b245d40c4de0Thiemo Wiedemeyer , isProvenCons :: Bool

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , isInternalSpec :: Bool }

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer deriving (Eq, Ord, Show)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | creates a DGNodeType from a DGNodeLab

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetRealDGNodeType :: DGNodeLab -> DGNodeType

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyergetRealDGNodeType dgnlab = DGNodeType

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer { isRefType = isDGRef dgnlab

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , isProvenNode = not $ hasOpenGoals dgnlab

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isProvenCons = not $ hasOpenNodeConsStatus False dgnlab

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isInternalSpec = isInternalNode dgnlab }

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer-- | Creates a list with all DGNodeType types

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo WiedemeyerlistDGNodeTypes :: [DGNodeType]

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerlistDGNodeTypes = let bs = [False, True] in

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer [ DGNodeType

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer { isRefType = ref

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isProvenNode = isEmpty'

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , isProvenCons = proven

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , isInternalSpec = spec }

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | ref <- bs

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isEmpty' <- bs

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , proven <- bs

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , spec <- bs ]

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- ** edge label types

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer{- an edge id used to be represented as a list of ints.

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer the reason of an edge can have multiple ids is, for example, there exists

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer an proven edge e1 with id 1 and an unproven edge e2 with id 2 between

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer two nodes. Now after applying some rules e2 is proven, but it's actually

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer the same as the proven edge e1, then the proven e2 should not be inserted

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer into the graph again, but e1 will take e2's id 2 because 2 is probably

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer saved in some other places. As a result, e1 would have 1 and 2 as its id.

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer This type can be extended to a more complicated struture, like a tree

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer suggested by Till.

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-}

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | unique number for edges

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyernewtype EdgeId = EdgeId Int deriving (Show, Eq, Ord, Enum)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | the first edge in a graph

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerstartEdgeId :: EdgeId

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerstartEdgeId = EdgeId 0

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyershowEdgeId :: EdgeId -> String

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyershowEdgeId (EdgeId i) = show i

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | a set of used edges

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyernewtype ProofBasis = ProofBasis { proofBasis :: Set.Set EdgeId }

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer deriving (Show, Eq, Ord)

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | a wrapper for fitting morphisms with a trivial Eq instance

b70aa06df02d646ee391a984d69f6072711e60f4Thiemo Wiedemeyernewtype Fitted = Fitted [G_mapping] deriving Show

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerinstance Eq Fitted where

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer _ == _ = True

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata DGLinkOrigin =

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer SeeTarget

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | SeeSource

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | TEST

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer | DGImpliesLink

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGLinkExtension

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGLinkTranslation

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGLinkClosedLenv

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer | DGLinkImports

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGLinkMorph SIMPLE_ID

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer | DGLinkInst SIMPLE_ID Fitted

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer | DGLinkInstArg SIMPLE_ID

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer | DGLinkView SIMPLE_ID Fitted

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer | DGLinkFitView SIMPLE_ID

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer | DGLinkFitViewImp SIMPLE_ID

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer | DGLinkProof

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer | DGLinkFlatteningUnion

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer | DGLinkFlatteningRename

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer | DGLinkRefinement SIMPLE_ID

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer deriving (Show, Eq)

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer{- | Rules in the development graph calculus,

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer Sect. IV:4.4 of the CASL Reference Manual explains them in depth

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer mutual recursive with 'DGLinkLab', 'DGLinkType', and 'ThmLinkStatus'

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer-}

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata DGRule =

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer DGRule String

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | DGRuleWithEdge String (LEdge DGLinkLab)

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer | DGRuleLocalInference [(String, String)] -- renamed theorems

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer | Composition [LEdge DGLinkLab]

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer deriving (Show, Eq)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer-- | proof status of a link

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata ThmLinkStatus = LeftOpen | Proven DGRule ProofBasis deriving (Show, Eq)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerisProvenThmLinkStatus :: ThmLinkStatus -> Bool

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerisProvenThmLinkStatus tls = case tls of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer LeftOpen -> False

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer _ -> True

b18caa17663d4639c022611457bb9b759bc6e2c9Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata Scope = Local | Global deriving (Show, Eq, Ord)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata LinkKind = DefLink | ThmLink ThmLinkStatus deriving (Show, Eq)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata FreeOrCofree = Free | Cofree | NPFree deriving (Show, Eq, Ord)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | required and proven conservativity (with a proof)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata ConsStatus = ConsStatus Conservativity Conservativity ThmLinkStatus

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer deriving (Show, Eq)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerisProvenConsStatusLink :: ConsStatus -> Bool

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerisProvenConsStatusLink = not . hasOpenConsStatus False

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermkConsStatus :: Conservativity -> ConsStatus

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermkConsStatus c = ConsStatus c None LeftOpen

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetConsOfStatus :: ConsStatus -> Conservativity

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetConsOfStatus (ConsStatus c _ _) = c

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | to be displayed as edge label

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyershowConsStatus :: ConsStatus -> String

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyershowConsStatus cs = case cs of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ConsStatus None None _ -> ""

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ConsStatus None _ LeftOpen -> ""

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ConsStatus c _ LeftOpen -> show c ++ "?"

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ConsStatus _ cp _ -> show cp

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer{- | Link types of development graphs,

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Sect. IV:4.2 of the CASL Reference Manual explains them in depth. -}

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata DGLinkType =

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ScopedLink Scope LinkKind ConsStatus

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | HidingDefLink

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | FreeOrCofreeDefLink FreeOrCofree MaybeNode -- the "parameter" node

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | HidingFreeOrCofreeThm (Maybe FreeOrCofree) GMorphism ThmLinkStatus

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer {- DGLink S1 S2 m2 (DGLinkType m1 p) n

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer corresponds to a span of morphisms

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer S1 <--m1-- S --m2--> S2 -}

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer deriving (Show, Eq)

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | extract theorem link status from link type

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerthmLinkStatus :: DGLinkType -> Maybe ThmLinkStatus

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerthmLinkStatus t = case t of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ScopedLink _ (ThmLink s) _ -> Just s

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer HidingFreeOrCofreeThm _ _ s -> Just s

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer _ -> Nothing

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | link inscriptions in development graphs

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata DGLinkLab = DGLink

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer { dgl_morphism :: GMorphism -- signature morphism of link

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , dgl_type :: DGLinkType -- type: local, global, def, thm?

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , dgl_origin :: DGLinkOrigin -- origin in input language

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , dglPending :: Bool -- open proofs of edges in proof basis

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , dgl_id :: EdgeId -- id of the edge

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , dglName :: NodeName -- name of the edge

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer } deriving (Show, Eq)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermkDGLink :: GMorphism -> DGLinkType -> DGLinkOrigin -> NodeName -> EdgeId

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer -> DGLinkLab

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermkDGLink mor ty orig nn ei = DGLink

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer { dgl_morphism = mor

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , dgl_type = ty

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , dgl_origin = orig

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , dglPending = False

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , dgl_id = ei

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , dglName = nn }

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | name a link

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyernameDGLink :: NodeName -> DGLinkLab -> DGLinkLab

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyernameDGLink nn l = l { dglName = nn }

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerdefDGLink :: GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer{- See svn-version 13804 for a naming concept which unfortunately introduced

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyersame names for different links. -}

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerdefDGLink m ty orig = mkDGLink m ty orig (makeName $ mkSimpleId "")

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer defaultEdgeId

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerglobDefLink :: GMorphism -> DGLinkOrigin -> DGLinkLab

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerglobDefLink m = defDGLink m globalDef

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | describe the link type of the label

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetDGLinkType :: DGLinkLab -> String

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetDGLinkType = getDGEdgeTypeName . getRealDGLinkType

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | converts a DGEdgeType to a String

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetDGEdgeTypeName :: DGEdgeType -> String

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetDGEdgeTypeName e =

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer (if isInc e then (++ "Inc") else id)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer $ getDGEdgeTypeModIncName $ edgeTypeModInc e

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetDGEdgeTypeModIncName :: DGEdgeTypeModInc -> String

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetDGEdgeTypeModIncName et = case et of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ThmType thm isPrvn _ _ ->

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer let prvn = (if isPrvn then "P" else "Unp") ++ "roven" in

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer case thm of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer HidingThm -> prvn ++ "HidingThm"

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer FreeOrCofreeThm -> prvn ++ "Thm"

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer GlobalOrLocalThm scope isHom ->

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer let het = if isHom then id else ("Het" ++) in

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer het (case scope of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Local -> "Local"

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Global -> if isHom then "Global" else "") ++ prvn ++ "Thm"

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer FreeOrCofreeDef -> "Def"

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer _ -> show et

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata DGEdgeType = DGEdgeType

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer { edgeTypeModInc :: DGEdgeTypeModInc

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isInc :: Bool }

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer deriving (Eq, Ord, Show)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata DGEdgeTypeModInc =

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer GlobalDef

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | HetDef

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | HidingDef

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | LocalDef

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | FreeOrCofreeDef -- free or cofree

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | ThmType { thmEdgeType :: ThmTypes

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isProvenEdge :: Bool

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isConservativ :: Bool

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isPending :: Bool }

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer deriving (Eq, Ord, Show)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata ThmTypes =

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer HidingThm

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | FreeOrCofreeThm

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | GlobalOrLocalThm { isLocalThmType :: Scope

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isHomThm :: Bool }

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer deriving (Eq, Ord, Show)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetHomEdgeType :: Bool -> Bool -> DGLinkType -> DGEdgeTypeModInc

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetHomEdgeType isPend isHom lt = case lt of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ScopedLink scope lk cons -> case lk of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer DefLink -> case scope of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Local -> LocalDef

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Global -> if isHom then GlobalDef else HetDef

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ThmLink st -> ThmType

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer { thmEdgeType = GlobalOrLocalThm scope isHom

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isProvenEdge = isProvenThmLinkStatus st

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isConservativ = isProvenConsStatusLink cons

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isPending = isPend } -- needs to be checked

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer HidingDefLink -> HidingDef

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer FreeOrCofreeDefLink _ _ -> FreeOrCofreeDef

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer HidingFreeOrCofreeThm mh _ st -> ThmType

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer { thmEdgeType = case mh of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Nothing -> HidingThm

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer _ -> FreeOrCofreeThm

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isProvenEdge = isProvenThmLinkStatus st

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isConservativ = True

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isPending = isPend }

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | creates a DGEdgeType from a DGLinkLab

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetRealDGLinkType :: DGLinkLab -> DGEdgeType

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetRealDGLinkType lnk = let

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer gmor = dgl_morphism lnk

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer in DGEdgeType

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer { edgeTypeModInc = getHomEdgeType (dglPending lnk) (isHomogeneous gmor)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer $ dgl_type lnk

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isInc = case gmor of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer GMorphism cid _ _ mor _ -> isInclusionComorphism cid && isInclusion mor

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer }

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | Creates a list with all DGEdgeType types

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerlistDGEdgeTypes :: [DGEdgeType]

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerlistDGEdgeTypes =

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer [ DGEdgeType { edgeTypeModInc = modinc

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isInc = isInclusion' }

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | modinc <-

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer [ GlobalDef

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , HetDef

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , HidingDef

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , LocalDef

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , FreeOrCofreeDef ] ++

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer [ ThmType { thmEdgeType = thmType

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isProvenEdge = proven

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isConservativ = cons

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isPending = pending }

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | thmType <-

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer [ HidingThm

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , FreeOrCofreeThm] ++

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer [ GlobalOrLocalThm { isLocalThmType = local

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isHomThm = hom }

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | local <- [Local, Global]

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , hom <- [True, False]

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ]

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer , proven <- [True, False]

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , cons <- [True, False]

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , pending <- [True, False]

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ]

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer , isInclusion' <- [True, False]

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ]

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- ** types for global environments

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | import, formal parameters and united signature of formal params

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata GenSig = GenSig MaybeNode [NodeSig] MaybeNode deriving Show

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | genericity and body

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata ExtGenSig = ExtGenSig GenSig NodeSig deriving Show

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- | source, morphism, parameterized target

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata ExtViewSig = ExtViewSig NodeSig GMorphism ExtGenSig deriving Show

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer{- ** types for architectural and unit specification analysis

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer (as defined for basic static semantics in Chap. III:5.1) -}

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata UnitSig = UnitSig [NodeSig] NodeSig (Maybe NodeSig) deriving (Show, Eq)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer{- Maybe NodeSig stores the union of the parameters

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerthe node is needed for consistency checks -}

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata ImpUnitSigOrSig = ImpUnitSig MaybeNode UnitSig | Sig NodeSig

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer deriving (Show, Eq)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyertype StUnitCtx = Map.Map SIMPLE_ID ImpUnitSigOrSig

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyeremptyStUnitCtx :: StUnitCtx

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyeremptyStUnitCtx = Map.empty

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer{- data ArchSig = ArchSig StUnitCtx UnitSig deriving Show

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerthis type is superseeded by RefSig -}

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyertype RefSigMap = Map.Map SIMPLE_ID RefSig

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyertype BStContext = Map.Map SIMPLE_ID RefSig

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- there should be only BranchRefSigs

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata RefSig = BranchRefSig RTPointer (UnitSig, Maybe BranchSig)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | ComponentRefSig RTPointer RefSigMap

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer deriving (Eq)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerinstance Show RefSig where

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- made this instance for debugging purposes

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer show (BranchRefSig _ (usig, mbsig)) =

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer let bStr = case mbsig of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Nothing -> "Bottom\n "

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Just bsig -> case bsig of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer UnitSigAsBranchSig u ->

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer if u == usig then "same"

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer else "UnitSigAsBranch:" ++ shows u "\n "

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer BranchStaticContext bst ->

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer foldl (++) "branching: "

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer $ map (\ (n, s) -> shows n " mapped to\n" ++ shows s "\n")

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer $ Map.toList bst

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer in

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer "Branch: \n before refinement:\n " ++ show usig ++

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer "\n after refinement: \n" ++ bStr ++ "\n"

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer show (ComponentRefSig _ rsm) =

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer foldl (++) "CompRefSig:" $ map (\ n -> show n ++ "\n ") $

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Map.toList rsm

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetPointerFromRef :: RefSig -> RTPointer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetPointerFromRef (BranchRefSig p _) = p

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetPointerFromRef (ComponentRefSig p _) = p

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyersetPointerInRef :: RefSig -> RTPointer -> RefSig

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyersetPointerInRef (BranchRefSig _ x) y = BranchRefSig y x

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyersetPointerInRef (ComponentRefSig _ x) y = ComponentRefSig y x

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyersetUnitSigInRef :: RefSig -> UnitSig -> RefSig

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyersetUnitSigInRef (BranchRefSig x (_, y)) usig = BranchRefSig x (usig, y)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyersetUnitSigInRef _ _ = error "setUnitSigInRef"

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetUnitSigFromRef :: RefSig -> Result UnitSig

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetUnitSigFromRef (BranchRefSig _ (usig, _)) = return usig

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyergetUnitSigFromRef (ComponentRefSig _ rsm) =

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer error $ "getUnitSigFromRef:" ++ show (Map.keys rsm)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermkRefSigFromUnit :: UnitSig -> RefSig

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermkRefSigFromUnit usig = BranchRefSig RTNone

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer (usig, Just $ UnitSigAsBranchSig usig)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermkBotSigFromUnit :: UnitSig -> RefSig

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermkBotSigFromUnit usig = BranchRefSig RTNone (usig, Nothing)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyerdata BranchSig = UnitSigAsBranchSig UnitSig

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer | BranchStaticContext BStContext

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer deriving (Show, Eq)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyertype RefStUnitCtx = Map.Map SIMPLE_ID RefSig

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- only BranchRefSigs allowed

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyeremptyRefStUnitCtx :: RefStUnitCtx

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyeremptyRefStUnitCtx = Map.empty

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- Auxiliaries for refinament signatures composition

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermatchesContext :: RefSigMap -> BStContext -> Bool

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermatchesContext rsmap bstc =

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer not (any (`notElem` Map.keys bstc) $ Map.keys rsmap)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer && namesMatchCtx (Map.keys rsmap) bstc rsmap

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerequalSigs :: UnitSig -> UnitSig -> Bool

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerequalSigs (UnitSig ls1 ns1 _) (UnitSig ls2 ns2 _) =

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer length ls1 == length ls2 && getSig ns1 == getSig ns2

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer && all (\ (x1, x2) -> getSig x1 == getSig x2) (zip ls1 ls2)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyernamesMatchCtx :: [SIMPLE_ID] -> BStContext -> RefSigMap -> Bool

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyernamesMatchCtx [] _ _ = True

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyernamesMatchCtx (un : unitNames) bstc rsmap =

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer case Map.findWithDefault (error "namesMatchCtx")

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer un bstc of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer BranchRefSig _ (_usig, mbsig) -> case mbsig of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Nothing -> False -- should not be the case

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Just bsig -> case bsig of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer UnitSigAsBranchSig usig' ->

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer case Map.findWithDefault (error "USABS") un rsmap of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer BranchRefSig _ (usig'', _mbsig') -> equalSigs usig' usig'' &&

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer namesMatchCtx unitNames bstc rsmap

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer _ -> False

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer BranchStaticContext bstc' ->

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer case rsmap Map.! un of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ComponentRefSig _ rsmap' ->

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer matchesContext rsmap' bstc' &&

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer namesMatchCtx unitNames bstc rsmap

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer {- This is where I introduce something new wrt to the original paper:

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer if bstc' has only one element

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer it suffices to have the signature of that element

b70aa06df02d646ee391a984d69f6072711e60f4Thiemo Wiedemeyer matching the signature from rsmap' -}

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer _ -> Map.size bstc' == 1 &&

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer let un1 = head $ Map.keys bstc'

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer rsmap' = Map.mapKeys (\ x -> if x == un then un1 else x)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer rsmap

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer in namesMatchCtx [un1] bstc' rsmap' &&

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer namesMatchCtx unitNames bstc rsmap

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer _ -> False -- this should never be the case

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermodifyCtx :: [SIMPLE_ID] -> RefSigMap -> BStContext -> BStContext

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermodifyCtx [] _ bstc = bstc

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyermodifyCtx (un : unitNames) rsmap bstc =

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer case bstc Map.! un of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer BranchRefSig n1 (usig, mbsig) -> case mbsig of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Nothing -> modifyCtx unitNames rsmap bstc -- should not be the case

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Just bsig -> case bsig of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer UnitSigAsBranchSig usig' ->

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer case rsmap Map.! un of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer BranchRefSig n2 (usig'', bsig'') -> if equalSigs usig' usig'' then

8a09bb0d66c5be017e8eefeeea31ead5829ab202Thiemo Wiedemeyer modifyCtx unitNames rsmap $

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Map.insert un (BranchRefSig (compPointer n1 n2)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer (usig, bsig'')) bstc -- was usig'

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer else error "illegal composition"

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer _ -> modifyCtx unitNames rsmap bstc

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer BranchStaticContext bstc' ->

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer case rsmap Map.! un of

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer ComponentRefSig n2 rsmap' -> modifyCtx unitNames rsmap $

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer Map.insert un

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer (BranchRefSig (compPointer n1 n2) (usig, Just $

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer BranchStaticContext $ modifyCtx (Map.keys rsmap') rsmap' bstc'))

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer bstc

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer _ -> let f = if Map.size bstc' == 1 then

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer let un1 = head $ Map.keys bstc'

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer rsmap' = Map.mapKeys

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer (\ x -> if x == un then un1 else x)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer rsmap

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer bstc'' = modifyCtx [un1] rsmap' bstc'

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer in Map.singleton un $

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer BranchRefSig RTNone (usig, Just

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer $ BranchStaticContext bstc'')

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer else Map.empty

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer in Map.union f $ modifyCtx unitNames rsmap bstc

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer _ -> modifyCtx unitNames rsmap bstc -- same as above

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer-- Signature composition

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerrefSigComposition :: RefSig -> RefSig -> Result RefSig

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo WiedemeyerrefSigComposition (BranchRefSig n1 (usig1, Just (UnitSigAsBranchSig usig2)))

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer (BranchRefSig n2 (usig3, bsig)) =

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer if equalSigs usig2 usig3 then

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer return $ BranchRefSig (compPointer n1 n2) (usig1, bsig)

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer else fail $ "Signatures: \n" ++ show usig2 ++ "\n and \n " ++ show usig3 ++

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer " do not compose"

8f31d51d47da96200437dd3af1d785cd88a46f71Thiemo Wiedemeyer

refSigComposition _rsig1@(BranchRefSig n1

(usig1, Just (BranchStaticContext bstc)))

_rsig2@(ComponentRefSig n2 rsmap) =

if matchesContext rsmap bstc then

return $ BranchRefSig (compPointer n1 n2)

(usig1, Just $ BranchStaticContext $

modifyCtx (Map.keys rsmap) rsmap bstc)

else fail ("Signatures do not match:" ++ show (Map.keys bstc) ++ " "

++ show (Map.keys rsmap))

refSigComposition (ComponentRefSig n1 rsmap1) (ComponentRefSig n2 rsmap2) = do

upd <- mapM (\ x -> do

s <- refSigComposition (rsmap1 Map.! x) (rsmap2 Map.! x)

return (x, s))

$ filter (`elem` Map.keys rsmap1) $ Map.keys rsmap2

let unionMap = Map.union (Map.fromList upd) $

Map.union rsmap1 rsmap2

return $ ComponentRefSig (compPointer n1 n2) unionMap

refSigComposition _rsig1 _rsig2 =

fail "composition of refinement signatures"

-- | an entry of the global environment

data GlobalEntry =

SpecEntry ExtGenSig

| StructEntry ExtViewSig

| ViewEntry ExtViewSig

| ArchEntry RefSig

| UnitEntry UnitSig

| RefEntry RefSig

deriving Show

type GlobalEnv = Map.Map SIMPLE_ID GlobalEntry

-- ** change and history types

-- | the edit operations of the DGraph

data DGChange =

InsertNode (LNode DGNodeLab)

| DeleteNode (LNode DGNodeLab)

| InsertEdge (LEdge DGLinkLab)

| DeleteEdge (LEdge DGLinkLab)

-- it contains the old label and new label with node

| SetNodeLab DGNodeLab (LNode DGNodeLab)

deriving (Show, Eq)

data HistElem =

HistElem DGChange

| HistGroup DGRule ProofHistory

deriving (Show, Eq)

type ProofHistory = SizedList.SizedList HistElem

-- datatypes for the refinement tree

data RTNodeType = RTPlain UnitSig | RTRef Node deriving (Eq)

instance Show RTNodeType where

show (RTPlain u) = "RTPlain\n" ++ show u

show (RTRef n) = show n

data RTNodeLab = RTNodeLab

{ rtn_type :: RTNodeType

, rtn_name :: String

} deriving Eq

instance Show RTNodeLab where

show r =

let

name = rtn_name r

t = rtn_type r

t1 = case t of

RTPlain u -> "plain: " ++ show u

RTRef n -> show n

in name ++ " " ++ t1

data RTLinkType =

RTRefine

| RTComp

deriving (Show, Eq)

data RTLinkLab = RTLink

{ rtl_type :: RTLinkType

} deriving (Show, Eq)

-- utility functions for handling refinement tree

addNodeRT :: DGraph -> UnitSig -> String -> (Node, DGraph)

addNodeRT dg usig s =

let

g = refTree dg

n = Tree.getNewNode g

l = RTNodeLab {

rtn_type = RTPlain usig

, rtn_name = s

}

in (n, dg {refTree = insNode (n, l) g})

addSpecNodeRT :: DGraph -> UnitSig -> String -> (Node, DGraph)

addSpecNodeRT dg usig s =

let

(n, dg') = addNodeRT dg usig s

f = Map.insert s n $ specRoots dg'

in (n, dg' {specRoots = f})

updateNodeNameRT :: DGraph -> Node -> String -> DGraph

updateNodeNameRT dg n s =

let

g = refTree dg

l = Graph.lab g n

in case l of

Nothing -> dg

Just oldL -> let

newL = oldL {rtn_name = s}

(g', _) = Tree.labelNode (n, newL) g

in dg {refTree = g'}

updateSigRT :: DGraph -> Node -> UnitSig -> DGraph

updateSigRT dg n usig =

let

g = refTree dg

l = Graph.lab g n

in case l of

Nothing -> dg

Just oldL -> let

newL = oldL {rtn_type = RTPlain usig}

(g', _) = Tree.labelNode (n, newL) g

in dg {refTree = g'}

updateNodeNameSpecRT :: DGraph -> Node -> String -> DGraph

updateNodeNameSpecRT dg n s =

let dg' = updateNodeNameRT dg n s

in dg' {specRoots = Map.insert s n $ specRoots dg}

addSubTree :: DGraph -> Maybe RTLeaves -> RTPointer -> (DGraph, RTPointer)

addSubTree dg Nothing (NPComp h) =

foldl

(\ ~(d, NPComp cp) (k, p) -> let

(d', p') = addSubTree d Nothing p

in (d', NPComp (Map.insert k p' cp)))

(dg, NPComp Map.empty) $ Map.toList h

addSubTree dg Nothing p = let

s = refSource p

(dg', f) = copySubTree dg s Nothing

p' = mapRTNodes f p

in (dg', p')

addSubTree dg (Just (RTLeaf x)) p = let

s = refSource p

(dg', f) = copySubTree dg s $ Just x

p' = mapRTNodes f p

in (dg', p')

addSubTree dg (Just (RTLeaves g)) (NPComp h) =

foldl

(\ ~(d, NPComp cp) (k, p) -> let

l = Map.findWithDefault (error $ "addSubTree:" ++ show k) k g

(d', p') = addSubTree d (Just l) p

in (d', NPComp (Map.insert k p' cp)))

(dg, NPComp Map.empty) $ Map.toList h

addSubTree _ _ _ = error "addSubTree"

copySubTree :: DGraph -> Node -> Maybe Node -> (DGraph, Map.Map Node Node)

copySubTree dg n mN =

case mN of

Nothing -> let

rTree = refTree dg

n' = Tree.getNewNode rTree

nLab = fromMaybe (error "copyNode") $ lab rTree n

rTree' = insNode (n', nLab) rTree

in copySubTreeN dg {refTree = rTree'} [n] $ Map.fromList [(n, n')]

Just y -> copySubTreeN dg [n] $ Map.fromList [(n, y)]

copySubTreeN :: DGraph -> [Node] -> Map.Map Node Node

-> (DGraph, Map.Map Node Node)

copySubTreeN dg nList pairs =

case nList of

[] -> (dg, pairs)

n : nList' -> let

rTree = refTree dg

pairsN = Map.findWithDefault (error "copy") n pairs

descs = lsuc rTree n

(dg', pairs') = foldl (copyNode pairsN) (dg, pairs) descs

in copySubTreeN dg' (nub $ nList' ++ map fst descs) pairs'

copyNode :: Node -> (DGraph, Map.Map Node Node) -> LNode RTLinkLab

-> (DGraph, Map.Map Node Node)

copyNode s (dg, nMap) (n, eLab) = let

rTree = refTree dg

nLab = fromMaybe (error "copyNode") $ lab rTree n

n' = Tree.getNewNode rTree

rTree' = insNode (n', nLab) rTree

orderRT _ _ = GT

(rTree'', _) = Tree.insLEdge True orderRT (s, n', eLab) rTree'

in (dg {refTree = rTree''}, Map.insert n n' nMap)

addRefEdgeRT :: DGraph -> Node -> Node -> DGraph

addRefEdgeRT dg n1 n2 =

let

g = refTree dg

orderRT _ _ = GT

(g', b) = Tree.insLEdge True orderRT

(n1, n2, RTLink {rtl_type = RTRefine}) g

in if b then dg {refTree = g'}

else error "addRefEdgeRT"

addEdgesToNodeRT :: DGraph -> [Node] -> Node -> DGraph

addEdgesToNodeRT dg' rnodes n' =

let

g = refTree dg'

orderRT _ _ = GT

(g', b) = foldl (\ (g0, b0) n0 -> let

(g1, b1) = Tree.insLEdge True orderRT

(n', n0, RTLink {rtl_type = RTComp}) g0

in (g1, b1 && b0))

(g, True) rnodes

in if not b then error "addEdgesToNodeRT"

else dg' {refTree = g'}

-- datatypes for storing the nodes of the ref tree in the global env

data RTPointer =

RTNone

| NPUnit Node

| NPBranch Node (Map.Map SIMPLE_ID RTPointer)

-- here the leaves can be either NPUnit or NPComp

| NPRef Node Node

| NPComp (Map.Map SIMPLE_ID RTPointer)

{- here the leaves can be NPUnit or NPComp

and roots are needed for inserting edges -}

deriving (Show, Eq)

-- map nodes

mapRTNodes :: Map.Map Node Node -> RTPointer -> RTPointer

mapRTNodes f rtp = let app = flip $ Map.findWithDefault (error "mapRTNodes")

in case rtp of

RTNone -> RTNone

NPUnit x -> NPUnit (app f x)

NPRef x y -> NPRef (app f x) (app f y)

NPBranch x g -> NPBranch (app f x) (Map.map (mapRTNodes f) g)

NPComp g -> NPComp (Map.map (mapRTNodes f) g)

-- compositions

compPointer :: RTPointer -> RTPointer -> RTPointer

compPointer (NPUnit n1) (NPUnit n2) = NPRef n1 n2

compPointer (NPUnit n1) (NPBranch _ f) = NPBranch n1 f

compPointer (NPUnit n1) (NPRef _ n2) = NPRef n1 n2

compPointer (NPRef n1 _) (NPRef _ n2) = NPRef n1 n2

compPointer (NPRef n1 _) (NPBranch _ f) = NPBranch n1 f

compPointer (NPBranch n1 f1) (NPComp f2) =

NPBranch n1 (Map.unionWith (\ _ y -> y) f1 f2 )

compPointer (NPComp f1) (NPComp f2) =

NPComp (Map.unionWith (\ _ y -> y) f1 f2)

compPointer x y = error $ "compPointer:" ++ show x ++ " " ++ show y

-- sources

refSource :: RTPointer -> Node

refSource (NPUnit n) = n

refSource (NPBranch n _) = n

refSource (NPRef n _) = n

refSource x = error ("refSource:" ++ show x)

data RTLeaves = RTLeaf Node | RTLeaves (Map.Map SIMPLE_ID RTLeaves)

deriving Show

refTarget :: RTPointer -> RTLeaves

refTarget (NPUnit n) = RTLeaf n

refTarget (NPRef _ n) = RTLeaf n

refTarget (NPComp f) = RTLeaves $ Map.map refTarget f

refTarget (NPBranch _ f) = RTLeaves $ Map.map refTarget f

refTarget x = error ("refTarget:" ++ show x)

{- I copied these types from ArchDiagram

to store the diagrams of the arch specs in the dgraph -}

data DiagNodeLab = DiagNode { dn_sig :: NodeSig, dn_desc :: String }

deriving Show

data DiagLinkLab = DiagLink { dl_morphism :: GMorphism, dl_number :: Int }

instance Show DiagLinkLab where

show _ = ""

data Diag = Diagram {

diagGraph :: Tree.Gr DiagNodeLab DiagLinkLab,

numberOfEdges :: Int

}

deriving Show

{- | the actual development graph with auxiliary information. A

'G_sign' should be stored in 'sigMap' under its 'gSignSelfIdx'. The

same applies to 'G_morphism' with 'morMap' and 'gMorphismSelfIdx'

resp. 'G_theory' with 'thMap' and 'gTheorySelfIdx'. -}

data DGraph = DGraph

{ globalAnnos :: GlobalAnnos -- ^ global annos of library

, optLibDefn :: Maybe LIB_DEFN

, globalEnv :: GlobalEnv -- ^ name entities (specs, views) of a library

, dgBody :: Tree.Gr DGNodeLab DGLinkLab -- ^ actual 'DGraph` tree

, refTree :: Tree.Gr RTNodeLab RTLinkLab -- ^ the refinement tree

, specRoots :: Map.Map String Node -- ^ root nodes for named specs

, archSpecDiags :: Map.Map String Diag

-- ^ dependency diagrams between units

, getNewEdgeId :: EdgeId -- ^ edge counter

, refNodes :: Map.Map Node (LibName, Node) -- ^ unexpanded 'DGRef's

, allRefNodes :: Map.Map (LibName, Node) Node -- ^ all DGRef's

, sigMap :: Map.Map SigId G_sign -- ^ signature map

, thMap :: Map.Map ThId G_theory -- ^ morphism map

, morMap :: Map.Map MorId G_morphism -- ^ theory map

, proofHistory :: ProofHistory -- ^ applied proof steps

, redoHistory :: ProofHistory -- ^ undone proofs steps

} deriving Show

emptyDG :: DGraph

emptyDG = DGraph

{ globalAnnos = emptyGlobalAnnos

, optLibDefn = Nothing

, globalEnv = Map.empty

, dgBody = Graph.empty

, refTree = Graph.empty

, specRoots = Map.empty

, archSpecDiags = Map.empty

, getNewEdgeId = startEdgeId

, refNodes = Map.empty

, allRefNodes = Map.empty

, sigMap = Map.empty

, thMap = Map.empty

, morMap = Map.empty

, proofHistory = SizedList.empty

, redoHistory = SizedList.empty }

type LibEnv = Map.Map LibName DGraph

-- | an empty environment

emptyLibEnv :: LibEnv

emptyLibEnv = Map.empty

-- * utility functions

-- ** for node signatures

emptyG_sign :: AnyLogic -> G_sign

emptyG_sign (Logic lid) = G_sign lid (ext_empty_signature lid) startSigId

getMaybeSig :: MaybeNode -> G_sign

getMaybeSig (JustNode ns) = getSig ns

getMaybeSig (EmptyNode l) = emptyG_sign l

getLogic :: MaybeNode -> AnyLogic

getLogic (JustNode ns) = getNodeLogic ns

getLogic (EmptyNode l) = l

getNodeLogic :: NodeSig -> AnyLogic

getNodeLogic (NodeSig _ (G_sign lid _ _)) = Logic lid

-- ** for node names

emptyNodeName :: NodeName

emptyNodeName = NodeName (mkSimpleId "") "" 0 []

showExt :: NodeName -> String

showExt n = let i = extIndex n in extString n ++ if i == 0 then "" else show i

showName :: NodeName -> String

showName n = let ext = showExt n in

tokStr (getName n) ++ if null ext then ext else "__" ++ ext

makeName :: SIMPLE_ID -> NodeName

makeName n = NodeName n "" 0 [ElemName $ tokStr n]

parseNodeName :: String -> NodeName

parseNodeName s = case splitByList "__" s of

[i] ->

makeName $ mkSimpleId i

[i, e] ->

let n = makeName $ mkSimpleId i

mSf = numberSuffix e

(es, sf) = fromMaybe (e, 0) mSf

in n { extString = es

, extIndex = sf }

_ ->

error

$ "parseNodeName: malformed NodeName, too many __: "

++ s

incBy :: Int -> NodeName -> NodeName

incBy i n = n

{ extIndex = extIndex n + i

, xpath = case xpath n of

ChildIndex j : r -> ChildIndex (j + i) : r

l -> ChildIndex i : l }

inc :: NodeName -> NodeName

inc = incBy 1

extName :: String -> NodeName -> NodeName

extName s n = n

{ extString = showExt n ++ take 1 s

, extIndex = 0

, xpath = ElemName s : xpath n }

-- ** accessing node label

-- | get the origin of a non-reference node (partial)

dgn_origin :: DGNodeLab -> DGOrigin

dgn_origin = node_origin . nodeInfo

-- | get the referenced library (partial)

dgn_libname :: DGNodeLab -> LibName

dgn_libname = ref_libname . nodeInfo

-- | get the referenced node (partial)

dgn_node :: DGNodeLab -> Node

dgn_node = ref_node . nodeInfo

-- | get the signature of a node's theory (total)

dgn_sign :: DGNodeLab -> G_sign

dgn_sign dn = case dgn_theory dn of

G_theory lid sig ind _ _ -> G_sign lid sig ind

-- | gets the name of a development graph node as a string (total)

getDGNodeName :: DGNodeLab -> String

getDGNodeName = showName . dgn_name

-- | gets the name of a development graph link as a string (total)

getDGLinkName :: DGLinkLab -> String

getDGLinkName = showName . dglName

-- ** creating node content and label

-- | create default content

newNodeInfo :: DGOrigin -> DGNodeInfo

newNodeInfo orig = DGNode

{ node_origin = orig

, node_cons_status = mkConsStatus None }

-- | create a reference node part

newRefInfo :: LibName -> Node -> DGNodeInfo

newRefInfo ln n = DGRef

{ ref_libname = ln

, ref_node = n }

-- | create a new node label

newInfoNodeLab :: NodeName -> DGNodeInfo -> G_theory -> DGNodeLab

newInfoNodeLab name info gTh@(G_theory lid _ _ _ _) = DGNodeLab

{ dgn_name = name

, dgn_theory = gTh

, globalTheory = Nothing

, labelHasHiding = False

, labelHasFree = False

, dgn_nf = Nothing

, dgn_sigma = Nothing

, dgn_freenf = Nothing

, dgn_phi = Nothing

, nodeInfo = info

, dgn_lock = Nothing

, dgn_symbolpathlist = G_symbolmap lid Map.empty }

-- | create a new node label using 'newNodeInfo' and 'newInfoNodeLab'

newNodeLab :: NodeName -> DGOrigin -> G_theory -> DGNodeLab

newNodeLab name = newInfoNodeLab name . newNodeInfo

-- ** handle the lock of a node

-- | wrapper to access the maybe lock

treatNodeLock :: (MVar () -> a) -> DGNodeLab -> a

treatNodeLock f = maybe (error "MVar not initialised") f . dgn_lock

-- | Tries to acquire the local lock. Return False if already acquired.

tryLockLocal :: DGNodeLab -> IO Bool

tryLockLocal = treatNodeLock $ flip tryPutMVar ()

-- | Releases the local lock.

unlockLocal :: DGNodeLab -> IO ()

unlockLocal = treatNodeLock $ \ lock ->

tryTakeMVar lock >>= maybe (error "Local lock wasn't locked.") return

-- | checks if locking MVar is initialized

hasLock :: DGNodeLab -> Bool

hasLock = isJust . dgn_lock

-- ** handle edge numbers and proof bases

-- | create a default ID which has to be changed when inserting a certain edge.

defaultEdgeId :: EdgeId

defaultEdgeId = EdgeId (-1)

emptyProofBasis :: ProofBasis

emptyProofBasis = ProofBasis Set.empty

nullProofBasis :: ProofBasis -> Bool

nullProofBasis = Set.null . proofBasis

addEdgeId :: ProofBasis -> EdgeId -> ProofBasis

addEdgeId (ProofBasis s) e = ProofBasis $ Set.insert e s

-- | checks if the given edge is contained in the given proof basis..

roughElem :: LEdge DGLinkLab -> ProofBasis -> Bool

roughElem (_, _, label) = Set.member (dgl_id label) . proofBasis

-- ** edge label equalities

-- | equality without comparing the edge ids

eqDGLinkLabContent :: DGLinkLab -> DGLinkLab -> Bool

eqDGLinkLabContent l1 l2 = let

i1 = dgl_id l1

i2 = dgl_id l2

in if i1 <= defaultEdgeId || i2 <= defaultEdgeId then

dgl_morphism l1 == dgl_morphism l2

&& dgl_type l1 == dgl_type l2

&& dgl_origin l1 == dgl_origin l2

&& dglName l1 == dglName l2

else let r = eqDGLinkLabContent l1 l2 { dgl_id = defaultEdgeId}

s = i1 == i2

in assert (r == s) s

-- | equality comparing ids only

eqDGLinkLabById :: DGLinkLab -> DGLinkLab -> Bool

eqDGLinkLabById l1 l2 = let

i1 = dgl_id l1

i2 = dgl_id l2

in if i1 > defaultEdgeId && i2 > defaultEdgeId then i1 == i2 else

error "eqDGLinkLabById"

-- ** setting index maps

{- these index maps should be global for all libraries,

therefore their contents need to be copied -}

cpIndexMaps :: DGraph -> DGraph -> DGraph

cpIndexMaps from to =

to { sigMap = sigMap from

, thMap = thMap from

, morMap = morMap from }

setSigMapDG :: Map.Map SigId G_sign -> DGraph -> DGraph

setSigMapDG m dg = dg { sigMap = m }

setThMapDG :: Map.Map ThId G_theory -> DGraph -> DGraph

setThMapDG m dg = dg { thMap = m }

setMorMapDG :: Map.Map MorId G_morphism -> DGraph -> DGraph

setMorMapDG m dg = dg { morMap = m }

-- ** looking up in index maps

lookupSigMapDG :: SigId -> DGraph -> Maybe G_sign

lookupSigMapDG i = Map.lookup i . sigMap

lookupThMapDG :: ThId -> DGraph -> Maybe G_theory

lookupThMapDG i = Map.lookup i . thMap

lookupMorMapDG :: MorId -> DGraph -> Maybe G_morphism

lookupMorMapDG i = Map.lookup i . morMap

-- ** getting index maps and their maximal index

getMapAndMaxIndex :: Ord k => k -> (b -> Map.Map k a) -> b -> (Map.Map k a, k)

getMapAndMaxIndex c f gctx =

let m = f gctx in (m, if Map.null m then c else fst $ Map.findMax m)

sigMapI :: DGraph -> (Map.Map SigId G_sign, SigId)

sigMapI = getMapAndMaxIndex startSigId sigMap

thMapI :: DGraph -> (Map.Map ThId G_theory, ThId)

thMapI = getMapAndMaxIndex startThId thMap

morMapI :: DGraph -> (Map.Map MorId G_morphism, MorId)

morMapI = getMapAndMaxIndex startMorId morMap

-- ** lookup other graph parts

lookupGlobalEnvDG :: SIMPLE_ID -> DGraph -> Maybe GlobalEntry

lookupGlobalEnvDG sid = Map.lookup sid . globalEnv

-- | lookup a referenced library and node of a given reference node

lookupInRefNodesDG :: Node -> DGraph -> Maybe (LibName, Node)

lookupInRefNodesDG n = Map.lookup n . refNodes

-- | lookup a reference node for a given libname and node

lookupInAllRefNodesDG :: DGNodeInfo -> DGraph -> Maybe Node

lookupInAllRefNodesDG ref dg = case ref of

DGRef { ref_libname = libn, ref_node = refn } ->

Map.lookup (libn, refn) $ allRefNodes dg

_ -> Nothing

-- ** lookup nodes by their names or other properties

-- | lookup a node in the graph with a predicate.

lookupNodeWith :: (LNode DGNodeLab -> Bool) -> DGraph -> [LNode DGNodeLab]

lookupNodeWith f dg = filter f $ labNodesDG dg

{- | lookup a node in the graph by its name, using showName

to convert nodenames. -}

lookupNodeByName :: String -> DGraph -> [LNode DGNodeLab]

lookupNodeByName s dg = lookupNodeWith f dg where

f (_, lbl) = getDGNodeName lbl == s

{- | filters all local nodes in the graph by their names, using showName

to convert nodenames. See also 'lookupNodeByName'. -}

filterLocalNodesByName :: String -> DGraph -> [LNode DGNodeLab]

filterLocalNodesByName s dg = lookupNodeWith f dg where

f (_, lbl) = not (isDGRef lbl) && getDGNodeName lbl == s

{- | filter all ref nodes in the graph by their names, using showName

to convert nodenames. See also 'lookupNodeByName'. -}

filterRefNodesByName :: String -> LibName -> DGraph -> [LNode DGNodeLab]

filterRefNodesByName s ln dg = lookupNodeWith f dg where

f (_, lbl) = case nodeInfo lbl of

DGRef { ref_libname = libn } ->

libn == ln && getDGNodeName lbl == s

_ -> False

{- | Given a 'LibEnv' we search each DGraph in it for a (maybe referenced) node

with the given name. We return the labeled node and the Graph where this node

resides as local node. See also 'lookupLocalNode'. -}

lookupLocalNodeByNameInEnv :: LibEnv -> String

-> Maybe (DGraph, LNode DGNodeLab)

lookupLocalNodeByNameInEnv le s = f $ Map.elems le where

f [] = Nothing

f (dg : l) = case lookupNodeByName s dg of

(nd, _) : _ -> Just $ lookupLocalNode le dg nd

_ -> f l

{- | We search only the given 'DGraph' for a (maybe referenced) node with the

given name. We return the labeled node and the Graph where this node resides

as local node. See also 'lookupLocalNode'. -}

lookupLocalNodeByName :: LibEnv -> DGraph -> String

-> Maybe (DGraph, LNode DGNodeLab)

lookupLocalNodeByName le dg s =

case lookupNodeByName s dg of

(nd, _) : _ -> Just $ lookupLocalNode le dg nd

_ -> Nothing

{- | Given a Node and a 'DGraph' we follow the node to the graph where it is

defined as a local node. -}

lookupLocalNode :: LibEnv -> DGraph -> Node -> (DGraph, LNode DGNodeLab)

lookupLocalNode le = f

where

f dg n = case labDG dg n of

DGNodeLab { nodeInfo = DGRef { ref_libname = ln

, ref_node = n' } } ->

f (lookupDGraph ln le) n'

x -> (dg, (n, x))

-- ** treat reference nodes

-- | add a new referenced node into the refNodes map of the given DG

addToRefNodesDG :: Node -> DGNodeInfo -> DGraph -> DGraph

addToRefNodesDG n ref dg = case ref of

DGRef { ref_libname = libn, ref_node = refn } ->

dg { refNodes = Map.insert n (libn, refn) $ refNodes dg

, allRefNodes = Map.insert (libn, refn) n $ allRefNodes dg }

_ -> dg

-- | delete the given referenced node out of the refnodes map

deleteFromRefNodesDG :: Node -> DGraph -> DGraph

deleteFromRefNodesDG n dg = dg { refNodes = Map.delete n $ refNodes dg }

-- ** accessing the actual graph

-- | get the next available node id

getNewNodeDG :: DGraph -> Node

getNewNodeDG = Tree.getNewNode . dgBody

-- | get all the nodes

labNodesDG :: DGraph -> [LNode DGNodeLab]

labNodesDG = labNodes . dgBody

-- | get all the edges

labEdgesDG :: DGraph -> [LEdge DGLinkLab]

labEdgesDG = labEdges . dgBody

-- | checks if a DG is empty or not.

isEmptyDG :: DGraph -> Bool

isEmptyDG = isEmpty . dgBody

-- | checks if a given node belongs to a given DG

gelemDG :: Node -> DGraph -> Bool

gelemDG n = gelem n . dgBody

-- | get all the incoming ledges of the given node in a given DG

innDG :: DGraph -> Node -> [LEdge DGLinkLab]

innDG = inn . dgBody

-- | get all the outgoing ledges of the given node in a given DG

outDG :: DGraph -> Node -> [LEdge DGLinkLab]

outDG = out . dgBody

-- | get all the nodes of the given DG

nodesDG :: DGraph -> [Node]

nodesDG = nodes . dgBody

-- | tries to get the label of the given node in a given DG

labDG :: DGraph -> Node -> DGNodeLab

labDG dg = fromMaybe (error "labDG") . lab (dgBody dg)

-- | tries to get the label of the given node in a given RT

labRT :: DGraph -> Node -> RTNodeLab

labRT dg = fromMaybe (error "labRT") . lab (refTree dg)

-- | get the name of a node from the number of node

getNameOfNode :: Node -> DGraph -> String

getNameOfNode index gc = getDGNodeName $ labDG gc index

-- | gets the given number of new node-ids in a given DG.

newNodesDG :: Int -> DGraph -> [Node]

newNodesDG n = newNodes n . dgBody

-- | get the context and throw input string as error message

safeContextDG :: String -> DGraph -> Node -> Context DGNodeLab DGLinkLab

safeContextDG s = safeContext s . dgBody where

safeContext err g v = -- same as context with extra message

fromMaybe (error $ err ++ ": Match Exception, Node: " ++ show v)

. fst $ match v g

-- ** manipulate graph

-- | sets the node with new label and returns the new graph and the old label

labelNodeDG :: LNode DGNodeLab -> DGraph -> (DGraph, DGNodeLab)

labelNodeDG p g =

let (b, l) = Tree.labelNode p $ dgBody g in (g { dgBody = b }, l)

-- | delete the node out of the given DG

delNodeDG :: Node -> DGraph -> DGraph

delNodeDG n dg = dg { dgBody = delNode n $ dgBody dg }

-- | delete the LNode out of the given DG

delLNodeDG :: LNode DGNodeLab -> DGraph -> DGraph

delLNodeDG n dg = dg { dgBody = Tree.delLNode (==) n $ dgBody dg }

-- | delete a list of nodes out of the given DG

delNodesDG :: [Node] -> DGraph -> DGraph

delNodesDG ns dg = dg { dgBody = delNodes ns $ dgBody dg }

-- | insert a new node into given DGraph

insNodeDG :: LNode DGNodeLab -> DGraph -> DGraph

insNodeDG n dg = dg { dgBody = insNode n $ dgBody dg }

-- | inserts a lnode into a given DG

insLNodeDG :: LNode DGNodeLab -> DGraph -> DGraph

insLNodeDG n@(v, _) g =

if gelemDG v g then error $ "insLNodeDG " ++ show v else insNodeDG n g

-- | insert a new node with the given node content into a given DGraph

insNodesDG :: [LNode DGNodeLab] -> DGraph -> DGraph

insNodesDG ns dg = dg { dgBody = insNodes ns $ dgBody dg }

-- | delete a labeled edge out of the given DG

delLEdgeDG :: LEdge DGLinkLab -> DGraph -> DGraph

delLEdgeDG e g = g

{ dgBody = Tree.delLEdge (comparing dgl_id) e

$ dgBody g }

-- | inserts an edge between two nodes, labelled with inclusion

insInclEdgeDG :: LogicGraph -> DGraph -> NodeSig -> NodeSig ->

Result DGraph

insInclEdgeDG lgraph dg s t = do

incl <- ginclusion lgraph (getSig s) (getSig t)

let l = globDefLink incl DGLinkImports

(_, dg') = insLEdgeDG (getNode s, getNode t, l) dg

return dg'

-- | insert a labeled edge into a given DG, return possibly new id of edge

insLEdgeDG :: LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)

insLEdgeDG (s, t, l) g =

let eId = dgl_id l

nId = getNewEdgeId g

newId = eId == defaultEdgeId

e = (s, t, if newId then l { dgl_id = nId } else l)

in (e, g

{ getNewEdgeId = if newId then succ nId else max nId $ succ eId

, dgBody = fst $ Tree.insLEdge True compareLinks e $ dgBody g })

compareLinks :: DGLinkLab -> DGLinkLab -> Ordering

compareLinks l1 l2 = if eqDGLinkLabContent l1 { dgl_id = defaultEdgeId } l2

then EQ else comparing dgl_id l1 l2

{- | tries to insert a labeled edge into a given DG, but if this edge

already exists, then does nothing. -}

insLEdgeNubDG :: LEdge DGLinkLab -> DGraph -> DGraph

insLEdgeNubDG (v, w, l) g =

let oldEdgeId = getNewEdgeId g

(ng, change) = Tree.insLEdge False compareLinks

(v, w, l { dgl_id = oldEdgeId }) $ dgBody g

in

g { getNewEdgeId = if change then succ oldEdgeId else oldEdgeId

, dgBody = ng }

{- | insert an edge into the given DGraph, which updates

the graph body and the edge counter as well. -}

insEdgeDG :: LEdge DGLinkLab -> DGraph -> DGraph

insEdgeDG l oldDG =

oldDG { dgBody = insEdge l $ dgBody oldDG

, getNewEdgeId = succ $ getNewEdgeId oldDG }

-- | insert a list of labeled edge into a given DG

insEdgesDG :: [LEdge DGLinkLab] -> DGraph -> DGraph

insEdgesDG = flip $ foldr insLEdgeNubDG

-- | merge a list of lnodes and ledges into a given DG

mkGraphDG :: [LNode DGNodeLab] -> [LEdge DGLinkLab] -> DGraph -> DGraph

mkGraphDG ns ls = insEdgesDG ls . insNodesDG ns

-- | get links by id (inefficiently)

getDGLinksById :: EdgeId -> DGraph -> [LEdge DGLinkLab]

getDGLinksById e = filter (\ (_, _, l) -> e == dgl_id l) . labEdgesDG

-- ** top-level functions

-- | initializes the MVar for locking if nessesary

initLocking :: DGraph -> LNode DGNodeLab -> IO (DGraph, DGNodeLab)

initLocking dg (node, dgn) = do

lock <- newEmptyMVar

let dgn' = dgn { dgn_lock = Just lock }

return (fst $ labelNodeDG (node, dgn') dg, dgn')

-- | returns the DGraph that belongs to the given library name

lookupDGraph :: LibName -> LibEnv -> DGraph

lookupDGraph ln = Map.findWithDefault (error $ "lookupDGraph " ++ show ln) ln

{- | compute the theory of a given node.

If this node is a DGRef, the referenced node is looked up first. -}

computeLocalTheory :: Monad m => LibEnv -> LibName -> Node -> m G_theory

computeLocalTheory libEnv ln =

computeLocalNodeTheory libEnv $ lookupDGraph ln libEnv

computeLocalNodeTheory :: Monad m => LibEnv -> DGraph -> Node -> m G_theory

computeLocalNodeTheory libEnv dg = computeLocalLabelTheory libEnv . labDG dg

computeLocalLabelTheory :: Monad m => LibEnv -> DGNodeLab -> m G_theory

computeLocalLabelTheory libEnv nodeLab =

if isDGRef nodeLab

then

computeLocalTheory libEnv (dgn_libname nodeLab) $ dgn_node nodeLab

else return $ dgn_theory nodeLab

-- ** test link types

liftE :: (DGLinkType -> a) -> LEdge DGLinkLab -> a

liftE f (_, _, edgeLab) = f $ dgl_type edgeLab

-- | or two predicates

liftOr :: (a -> Bool) -> (a -> Bool) -> a -> Bool

liftOr f g x = f x || g x

isGlobalDef :: DGLinkType -> Bool

isGlobalDef lt = case lt of

ScopedLink Global DefLink _ -> True

_ -> False

isLocalDef :: DGLinkType -> Bool

isLocalDef lt = case lt of

ScopedLink Local DefLink _ -> True

_ -> False

isHidingDef :: DGLinkType -> Bool

isHidingDef lt = case lt of

HidingDefLink -> True

_ -> False

isDefEdge :: DGLinkType -> Bool

isDefEdge edge = case edge of

ScopedLink _ DefLink _ -> True

HidingDefLink -> True

FreeOrCofreeDefLink _ _ -> True

_ -> False

isLocalEdge :: DGLinkType -> Bool

isLocalEdge edge = case edge of

ScopedLink Local _ _ -> True

_ -> False

isHidingEdge :: DGLinkType -> Bool

isHidingEdge edge = case edge of

HidingDefLink -> True

HidingFreeOrCofreeThm Nothing _ _ -> True

_ -> False

-- ** create link types

hidingThm :: GMorphism -> DGLinkType

hidingThm m = HidingFreeOrCofreeThm Nothing m LeftOpen

globalThm :: DGLinkType

globalThm = localOrGlobalThm Global None

localThm :: DGLinkType

localThm = localOrGlobalThm Local None

globalConsThm :: Conservativity -> DGLinkType

globalConsThm = localOrGlobalThm Global

localConsThm :: Conservativity -> DGLinkType

localConsThm = localOrGlobalThm Local

localOrGlobalThm :: Scope -> Conservativity -> DGLinkType

localOrGlobalThm sc = ScopedLink sc (ThmLink LeftOpen) . mkConsStatus

localOrGlobalDef :: Scope -> Conservativity -> DGLinkType

localOrGlobalDef sc = ScopedLink sc DefLink . mkConsStatus

globalConsDef :: Conservativity -> DGLinkType

globalConsDef = localOrGlobalDef Global

globalDef :: DGLinkType

globalDef = localOrGlobalDef Global None

localDef :: DGLinkType

localDef = localOrGlobalDef Local None

-- ** link conservativity

getLinkConsStatus :: DGLinkType -> ConsStatus

getLinkConsStatus lt = case lt of

ScopedLink _ _ c -> c

_ -> mkConsStatus None

getEdgeConsStatus :: DGLinkLab -> ConsStatus

getEdgeConsStatus = getLinkConsStatus . dgl_type

getCons :: DGLinkType -> Conservativity

getCons = getConsOfStatus . getLinkConsStatus

-- | returns the Conservativity if the given edge has one, otherwise none

getConservativity :: LEdge DGLinkLab -> Conservativity

getConservativity (_, _, edgeLab) = getConsOfStatus $ getEdgeConsStatus edgeLab

-- | returns the conservativity of the given path

getConservativityOfPath :: [LEdge DGLinkLab] -> Conservativity

getConservativityOfPath path = minimum [getConservativity e | e <- path]

-- * bottom up traversal

-- | Creates a LibName relation wrt dependencies via reference nodes

getLibDepRel :: LibEnv -> Rel.Rel LibName

getLibDepRel = Rel.transClosure

. Rel.fromSet . Map.foldWithKey (\ ln dg s ->

foldr ((\ x -> if isDGRef x then Set.insert (ln, dgn_libname x) else id)

. snd) s $ labNodesDG dg) Set.empty

topsortedLibsWithImports :: Rel.Rel LibName -> [LibName]

topsortedLibsWithImports = concatMap Set.toList . Rel.topSort

getTopsortedLibs :: LibEnv -> [LibName]

getTopsortedLibs le = let

rel = getLibDepRel le

ls = reverse $ topsortedLibsWithImports rel

restLs = Set.toList $ Set.difference (Map.keysSet le) $ Rel.nodes rel

in ls ++ restLs

{- | Get imported libs in topological order, i.e. lib(s) without imports first.

The input lib-name will be last -}

dependentLibs :: LibName -> LibEnv -> [LibName]

dependentLibs ln le =

let rel = getLibDepRel le

ts = topsortedLibsWithImports rel

is = Set.toList (Rel.succs rel ln)

in reverse $ ln : intersect ts is

topsortedNodes :: DGraph -> [LNode DGNodeLab]

topsortedNodes dgraph = let dg = dgBody dgraph in

reverse $ postorderF $ dffWith (\ (_, n, nl, _) -> (n, nl)) (nodes dg)

$ efilter (\ (s, t, el) -> s /= t && isDefEdge (dgl_type el)) dg

changedPendingEdges :: DGraph -> [LEdge DGLinkLab]

changedPendingEdges dg = let

ls = filter (liftE $ not . isDefEdge) $ labEdgesDG dg

(ms, ps) = foldr (\ (s, t, l) (m, es) ->

let b = dglPending l

e = dgl_id l

in (Map.insert e

(b, s, t,

maybe Set.empty (\ ts -> case ts of

LeftOpen -> Set.empty

Proven _ pb -> proofBasis pb) . thmLinkStatus $ dgl_type l) m

, if b && isLocalEdge (dgl_type l) then Set.insert e es else es))

(Map.empty, Set.empty) ls

close known =

let nxt = Map.keysSet $ Map.filter

(\ (_, _, _, s) -> not $ Set.null $ Set.intersection s known)

ms

new = Set.union nxt known

in if new == known then new else close new

aPs = close ps

in filter (\ (_, _, l) -> dglPending l /= Set.member (dgl_id l) aPs) ls

changedLocalTheorems :: DGraph -> LNode DGNodeLab -> [LEdge DGLinkLab]

changedLocalTheorems dg (v, lbl) =

case dgn_theory lbl of

G_theory _ _ _ sens _ ->

foldr (\ e@(_, _, el) l ->

let pend = dglPending el

psens = Map.keysSet $ OMap.filter isProvenSenStatus sens

in case thmLinkStatus $ dgl_type el of

Just (Proven (DGRuleLocalInference nms) _) | pend

== Set.isSubsetOf (Set.fromList $ map snd nms) psens -> e : l

_ -> l

) []

$ filter (liftE $ \ e -> isLocalEdge e && not (isLocalDef e))

$ innDG dg v

duplicateDefEdges :: DGraph -> [Edge]

duplicateDefEdges = concat .

filter (not . isSingle) . group . map (\ (s, t, _) -> (s, t))

. filter (liftE isDefEdge) . labEdgesDG