summaryrefslogtreecommitdiff
path: root/source
diff options
context:
space:
mode:
authorSimon-Kor <52245124+Simon-Kor@users.noreply.github.com>2024-08-24 11:44:10 +0200
committerSimon-Kor <52245124+Simon-Kor@users.noreply.github.com>2024-08-24 11:44:10 +0200
commit98ba67c72d4959d0a22cedfd5ac6d4b37ed47658 (patch)
tree4006ae98e775db3e7b0b345d823f82ad8f001259 /source
parent29027c9d2cdbdfe59e48b5aa28eb2d32d1a4c1f7 (diff)
Added/Fixed comments
Diffstat (limited to 'source')
-rw-r--r--source/TheoryGraph.hs10
1 files changed, 7 insertions, 3 deletions
diff --git a/source/TheoryGraph.hs b/source/TheoryGraph.hs
index c4887ea..e49bc1f 100644
--- a/source/TheoryGraph.hs
+++ b/source/TheoryGraph.hs
@@ -67,12 +67,12 @@ member :: FilePath -> TheoryGraph -> Bool
member n (TheoryGraph g) = Map.member n g
--- | Add a node to the TheoryGraph. This is a noop if the node is already present in the graph.
+-- | Add a node to the TheoryGraph.
addNode :: FilePath -> TheoryGraph -> TheoryGraph
addNode a (TheoryGraph g) = TheoryGraph (Map.insertWith Set.union a Set.empty g)
--- | Add an edge to the TheoryGraph. This is a noop if the edge is already present in the graph.
+-- | Add an edge to the TheoryGraph. This is a loop if the edge is already present in the graph.
addPrecedes :: Precedes FilePath -> TheoryGraph -> TheoryGraph
addPrecedes e@(Precedes _ a') (TheoryGraph g) = addNode a' (TheoryGraph (insertTail e g))
where
@@ -85,7 +85,9 @@ addPrecedes e@(Precedes _ a') (TheoryGraph g) = addNode a' (TheoryGraph (insertT
singleton :: FilePath -> TheoryGraph
singleton a = TheoryGraph (Map.singleton a Set.empty)
-
+-- | Construct a graph, from a list of nodes and edges.
+-- It takes all nodes a and add the pair (a, emptyset) to the Theorygraph,
+-- afterwards it add all edges between the nodes.
makeTheoryGraph :: [Precedes FilePath] -> [FilePath] -> TheoryGraph
makeTheoryGraph es as = List.foldl' (flip addPrecedes) (TheoryGraph trivial) es
where
@@ -94,6 +96,8 @@ makeTheoryGraph es as = List.foldl' (flip addPrecedes) (TheoryGraph trivial) es
{-# INLINE makeTheoryGraph #-}
+-- | Construct a graph, from a list @x:xs@,
+-- where @x@ is a pair of theorys @(a,b)@ with @a@ gets imported in @b@.
fromList :: [Precedes FilePath] -> TheoryGraph
fromList es = TheoryGraph (Map.fromListWith Set.union es')
where