summaryrefslogtreecommitdiff
path: root/Library/Usage.hs
diff options
context:
space:
mode:
Diffstat (limited to 'Library/Usage.hs')
-rw-r--r--Library/Usage.hs80
1 files changed, 0 insertions, 80 deletions
diff --git a/Library/Usage.hs b/Library/Usage.hs
deleted file mode 100644
index a307274..0000000
--- a/Library/Usage.hs
+++ /dev/null
@@ -1,80 +0,0 @@
-module Library.Usage(
- UsageMap,
- usageMap,
- useSort,
- nodeOutput,
- getArg
- ) where
-
-
-
-import Data.Map( Map )
-import qualified Data.Map as Map
-import Data.Set( Set )
-import qualified Data.Set as Set
-import Data.List
-import Data.Maybe
-import Data.Graph.Inductive.Graph( Node, LNode, Edge, LEdge )
-import qualified Data.Graph.Inductive.Graph as Graph
-import Library.Parse
-import Library.ProofGraph
-
-
-
-type UsageMap = Map Node (Map (LEdge (Int,Int)) (Int,[Int]))
-
-
--- Takes a graph, a starting list of nodes, a set of nodes of interest, and
--- follows the starting nodes up the graph to find which edges the starting nodes
--- will encounter the nodes of interest through.
-usageMap :: PGraph -> [Node] -> Set Node -> UsageMap
-usageMap graph order interest =
- let unionFunc a b = Map.unionWith min a b
-
- addFunc index prev umap edge =
- let node = snd3 edge
- curIn = Graph.outdeg graph (fst3 edge)
- prev' = (curIn - (fst . thd3 $ edge)):prev
- toAdd = Map.singleton node (Map.singleton edge (index,prev'))
- in if (Set.member node interest)
- then Map.unionWith unionFunc toAdd umap
- else umap
-
- f umap (index,node,prev) =
- let edgeList = Graph.out graph node
- sucMapList = map (f Map.empty) (map (\x -> (index, snd3 x, (length edgeList - (fst . thd3 $ x)):prev)) edgeList)
- umap' = foldl' (addFunc index prev) umap edgeList
- in Map.unionsWith unionFunc (umap':sucMapList)
-
- in foldl' f Map.empty (zip3 [1..] order (repeat []))
-
-
-
-useSort :: (LEdge a, (Int,[Int])) -> (LEdge a, (Int,[Int])) -> Ordering
-useSort (_,(w,x)) (_,(y,z)) =
- let check = compare w y
- in if (check == EQ)
- then compare (reverse x) (reverse z)
- else check
-
-
-
-nodeOutput :: PGraph -> Node -> Int
-nodeOutput graph node =
- let label = fromJust (Graph.lab graph node)
- in case label of
- "thm" -> 0
- "pop" -> 0
- "defineConst" -> 2
- "defineTypeOp" -> 5
- x -> 1
-
-
-
-getArg :: PGraph -> Node -> Int -> Maybe Node
-getArg graph node arg =
- let edge = filter (\x -> (fst . thd3 $ x) == arg) (Graph.out graph node)
- in if (edge == [])
- then Nothing
- else Just (snd3 . head $ edge)
-