diff options
| -rw-r--r-- | .gitignore | 5 | ||||
| -rw-r--r-- | Library/GraphPart.hs | 13 | ||||
| -rw-r--r-- | Library/ProofGraph.hs | 4 | ||||
| -rw-r--r-- | Library/WriteProof.hs | 200 | ||||
| -rw-r--r-- | Library/alternate_multi_command.hs | 315 | ||||
| -rw-r--r-- | TermNetTest.hs | 17 | ||||
| -rw-r--r-- | Test/name.art | 2 | ||||
| -rw-r--r-- | Test/timer.sh | 2 | ||||
| -rw-r--r-- | bin/.gitignore | 5 | ||||
| -rw-r--r-- | makefile | 2 | ||||
| -rw-r--r-- | test.sh | 3 | ||||
| -rw-r--r-- | writetest.hs | 55 |
12 files changed, 462 insertions, 161 deletions
diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..08bbf3b --- /dev/null +++ b/.gitignore @@ -0,0 +1,5 @@ + +# ignore files generated by GHC + +*.hi +*.o diff --git a/Library/GraphPart.hs b/Library/GraphPart.hs index 97503eb..02a95c0 100644 --- a/Library/GraphPart.hs +++ b/Library/GraphPart.hs @@ -80,8 +80,8 @@ outputLab gpart = do -graphAdd :: GraphPart -> Maybe (Node,Int) -> [(Node,Int)] -> PGraph -> PGraph -graphAdd gpart i o graph = +graphAddImp :: GraphPart -> Maybe (Node,Int) -> [(Node,Int)] -> PGraph -> PGraph +graphAddImp gpart i o graph = let (resolved, dict) = resolveNodeClash graph (getGraph gpart) base = (Graph.insEdges (Graph.labEdges resolved)) . (Graph.insNodes (Graph.labNodes resolved)) $ graph @@ -98,14 +98,21 @@ graphAdd gpart i o graph = in Graph.insEdges outEdge inputAdded graph' = outputAdded + in graph' + + +graphAdd :: GraphPart -> Maybe (Node,Int) -> [(Node,Int)] -> PGraph -> PGraph +graphAdd gpart i o graph = + let graph' = graphAddImp gpart i o graph in checkDupe graph' graphAddList :: [(GraphPart, Maybe (Node,Int), [(Node,Int)])] -> PGraph -> PGraph graphAddList partList graph = - foldl' (\g (x,y,z) -> graphAdd x y z g) graph partList + let graph' = foldl' (\g (x,y,z) -> graphAddImp x y z g) graph partList + in checkDupe graph' diff --git a/Library/ProofGraph.hs b/Library/ProofGraph.hs index 621b962..217e40c 100644 --- a/Library/ProofGraph.hs +++ b/Library/ProofGraph.hs @@ -4,7 +4,9 @@ module Library.ProofGraph ( checkDupe, nodeEquals, - resolveNodeClash + resolveNodeClash, + + argMap ) where diff --git a/Library/WriteProof.hs b/Library/WriteProof.hs index 1057199..c7e0a5f 100644 --- a/Library/WriteProof.hs +++ b/Library/WriteProof.hs @@ -29,149 +29,63 @@ import Library.Usage -reuse :: PGraph -> Node -> Int -reuse graph node = - let labels = map snd (Graph.lpre graph node) - f = (\x y -> length (filter (\z -> fst y == fst z) x)) - reuseList = map (f labels) labels - in maximum reuseList - - - -next :: Int -> PGraph -> [String] -next num graph = - let nodeList = filter (isNumber . snd) (Graph.labNodes graph) - numList = nub . (map (read . snd)) $ nodeList - f = (\x y -> if (x `elem` y) then f (x + 1) y else x) - g = (\x y -> if (x == 0) then y else g (x - 1) (f 0 (y ++ numList) : y)) - in map show (g num []) - - - -subGraph :: Gr a b -> Node -> [Node] -subGraph graph node = - let sucList = nub (Graph.suc graph node) - in nub (node : (foldl' (++) [] (map (subGraph graph) sucList))) - - - orderNodes :: PGraph -> [Node] -> [Node] orderNodes graph nodeList = nodeList --placeholder -removeOverlap :: PGraph -> Node -> [Node] -> [Node] -removeOverlap graph node list = - let nubFunc = (\x y -> (getArg graph node x) == (getArg graph node y)) - in nubBy nubFunc list - - - ---rightmostEdge :: Gr String (Int,Int) -> LEdge (Int,Int) -> Bool ---rightmostEdge graph edge = - - - - ---crossEdge :: Gr String (Int,Int) -> LEdge (Int,Int) -> Bool - - - ---trace :: Gr String (Int,Int) -> Node -> [Node] -> Maybe (Int,Node,Int) ---trace graph node history = --- let tr = (\g n curnode curarg hist -> --- if (curarg > output g n) --- then Nothing --- else let argToFollow = if (n == curnode) then curarg else 1 --- outputsFromArg = filter (\(x,y) -> snd y == argToFollow) (Graph.lpre g curnode) --- --- in case outputFromCurArg of --- 0 -> --- if (filter (\(x,y) -> snd y == curarg) (Graph.lpre g n) > 1) --- if (curarg > output g n) --- then Nothing --- else if (n == curnode) --- then let curnode' = filter (\(x,y) -> ) (Graph.lpre g n) --- in tr g n curnode' curarg --- else ) --- --- f = (\g n curarg h -> --- if (curarg > output g n) --- then Nothing --- else let hist = if --- place = tr g n n hist --- in if (isJust place) --- then place --- else f g n (curarg+1) hist --- --- in f graph node 1 history +-- buggy +multiCommandsSimple :: PGraph -> UsageMap -> [Node] -> PGraph +multiCommandsSimple graph usemap nodeList = + let multiNodes = filter (\x -> nodeOutput graph x > 1 && x `notElem` nodeList) (Graph.nodes graph) + umap = Map.filterWithKey (\n _ -> n `elem` multiNodes) usemap --- higher numbers -> deeper in the stack - ---multiCommands :: Gr String (Int,Int) -> [Node] -> (Gr String (Int,Int), [Node]) ---multiCommands graph nodeList = --- let f = (\g n p -> --- if ((output g n) <= 1) --- then g --- else let changed = do (argToUseDict, place, placeArg) <- trace g n --- let edgesToRemove = --- edgesRemoved = foldl' (\x y -> Graph.delLEdge y x) g edgesToRemove --- defSubGraph = --- edgesToRef = --- new = --- refsToAdd = --- return (foldl' insertSubGraph edgesRemoved refsToAdd) --- in if (isNothing changed) then g else fromJust changed --- --- multiOutputNodes = filter (\x -> output graph x > 1) (Graph.nodes graph) --- bestCase = foldl' f graph multiOutputNodes --- --- in - - - -multiCommandsSimple :: PGraph -> [Node] -> PGraph -multiCommandsSimple graph nodeList = - let r = (\g n p -> let g' = if ((nodeOutput g n) <= 1) - then g - else let ou = nodeOutput g n - index = next ou g - new = Graph.newNodes (5 * ou + 2) g -- 3 for num/def/pop, 2 for num/ref, per output plus an extra num/ref - (defNew,refNew) = splitAt (3 * ou + 2) new + f = (\gr node edgemap -> + let out = nodeOutput gr node + index = next out gr - edgeCheck x y = compare (snd . thd3 $ x) (snd . thd3 $ y) + edgeList = Map.toList edgemap + edgeToNode = (\x -> (fst3 x, fst . thd3 $ x)) - oldEdge = maximumBy edgeCheck (filter (\x -> fst3 x == p) (Graph.inn g n)) - toConvert = delete oldEdge (Graph.inn g n) + sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ c)) edgeList + grouped = groupBy (\x y -> (snd . thd3 . fst $ x) == (snd . thd3 . fst $ y)) sorted - defNodeGen = (\i j x lim -> if (x >= lim) - then [] - else [(j!!(x*3), i!!x), (j!!(x*3+1), "def"), - (j!!(x*3+2), "pop")] ++ (defNodeGen i j (x+1) lim)) - defNodes = (defNodeGen index defNew 0 ou) ++ [(defNew!!(3*ou), index!!((snd . thd3 $ oldEdge)-1)), (defNew!!(3*ou+1), "ref")] - defEdgeGen = (\x b -> let x' = [(fst b, fst . snd $ x, (1,1))] ++ (fst x) - in (x',b)) - defEdges = [(p, (fst . last $ defNodes), thd3 oldEdge), ((fst . head $ defNodes), n, (1,1))] ++ - (fst (foldl' defEdgeGen ([], head defNodes) (tail defNodes))) - defAdded = (Graph.insEdges defEdges) . (Graph.insNodes defNodes) . (Graph.delLEdge oldEdge) $ g + defEdge = fst (minimumBy useSort edgeList) + removeEdges = map (fst . (maximumBy useSort)) grouped + refEdges = map (filter (\x -> x /= defEdge && x `notElem` removeEdges) . (map fst)) grouped + + usedArgs = filter (\x -> x `elem` (map (snd . thd3) removeEdges)) [1..out] + + defGen = (\num -> + if (num > out) + then let reqEdges = filter (\x -> (snd . thd3 . fst $ x) == (snd . thd3 $ defEdge) && fst x /= defEdge) edgeList + refArg = (snd . thd3 $ defEdge) - 1 + in if (reqEdges == []) + then [index!!refArg, "ref"] --remove + else [index!!refArg, "ref"] + else if (num == (snd . thd3 $ defEdge) && num == out) + then if (filter (\x -> x /= defEdge && (snd . thd3 $ x) == num) (map fst edgeList) == []) + then [] + else [index!!(num-1), "def"] + else if (num `elem` usedArgs) + then [index!!(num-1), "def", "pop"] ++ defGen (num+1) + else ["pop"] ++ defGen (num+1)) + + defPart = (genPart (defGen 1) True, Just (node,1), [edgeToNode defEdge]) + + removeList = filter (\(x,y) -> y /= defEdge) (zip usedArgs removeEdges) + removeParts = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, [edgeToNode y])) removeList + + refList = filter (\(x,y) -> y /= []) (zip usedArgs refEdges) + refParts = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, map edgeToNode y)) refList + + partList = defPart:(removeParts ++ refParts) + edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) gr edgeList + partsAdded = graphAddList partList edgesRemoved + in partsAdded) - refGen = (\i lab -> [(i!!(2*(lab-1)), index!!(lab-1)), (i!!(2*(lab-1)+1), "ref")]) - refNodes = map (refGen refNew) [1 .. (ou)] - refEdges = map (\[x,y] -> (fst y, fst x,(1,1))) refNodes - refAdded = (Graph.insEdges refEdges) . (Graph.insNodes (concat refNodes)) $ defAdded - - convertEdge = (\g e -> let new = (fst3 e, fst . last $ (refNodes!!(snd . thd3 $ e)), thd3 e) - in (Graph.insEdge new) . (Graph.delLEdge e) $ g) - - done = foldl' convertEdge refAdded toConvert - in done - in f g' n) - - f = (\g n -> let argList = reverse $ [1 .. (Graph.outdeg g n)] - in foldl' (\x y -> r x (fromJust (getArg x n y)) n) g argList) - - in foldl' f graph nodeList + in foldl' (\g n -> f g n (fromJust (Map.lookup n umap))) graph multiNodes @@ -180,8 +94,8 @@ singleCommands graph usemap nodeList = let singleNodes = filter (\x -> nodeOutput graph x == 1 && Graph.indeg graph x > 1) (Graph.nodes graph) umap = Map.filterWithKey (\n _ -> n `elem` singleNodes) usemap - s = (\graph node edgemap -> - let index = head (next 1 graph) + s = (\gr node edgemap -> + let index = head (next 1 gr) edgeList = Map.toList edgemap defEdge = fst (minimumBy useSort edgeList) @@ -190,7 +104,7 @@ singleCommands graph usemap nodeList = defPart = genPart [index, "def"] True refPart = genPart [index, "ref"] False - removePart = genPart [index, "remove"] False + removePart = genPart [index, "ref"] False defNode = (fst3 defEdge, fst . thd3 $ defEdge) removeNode = (fst3 removeEdge, fst . thd3 $ removeEdge) @@ -199,7 +113,7 @@ singleCommands graph usemap nodeList = partList = [(defPart, Just (node, 1), [defNode]), (removePart, Nothing, [removeNode])] partList' = if (refNodeList == []) then partList else (refPart, Nothing, refNodeList):partList - edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) graph edgeList + edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) gr edgeList partsAdded = graphAddList partList' edgesRemoved in partsAdded) @@ -230,6 +144,16 @@ genPart labels hasInput = +next :: Int -> PGraph -> [String] +next num graph = + let nodeList = filter (isNumber . snd) (Graph.labNodes graph) + numList = nub . (map (read . snd)) $ nodeList + f = (\x y -> if (x `elem` y) then f (x + 1) y else x) + g = (\x y -> if (x == 0) then y else g (x - 1) (f 0 (y ++ numList) : y)) + in map show (g num []) + + + removeUnused :: PGraph -> [Node] -> PGraph removeUnused graph nodeList = let unused = filter (\x -> Graph.indeg graph x == 0 && x `notElem` nodeList) (Graph.nodes graph) @@ -243,7 +167,9 @@ resolve :: PGraph -> [Node] -> PGraph resolve graph nodeList = let liveGraph = removeUnused graph nodeList umap = usageMap graph nodeList (Set.fromList (Graph.nodes liveGraph)) - in foldl' (\g f -> f g umap nodeList) liveGraph [singleCommands] + singlesDone = singleCommands liveGraph umap nodeList + multisDone = multiCommandsSimple singlesDone umap nodeList + in multisDone diff --git a/Library/alternate_multi_command.hs b/Library/alternate_multi_command.hs new file mode 100644 index 0000000..da49a7d --- /dev/null +++ b/Library/alternate_multi_command.hs @@ -0,0 +1,315 @@ +multiCommands :: PGraph -> UsageMap -> [Node] -> PGraph +multiCommands graph usemap nodeList = + let multiNodes = filter (\x -> nodeOutput graph x > 1) (Graph.nodes graph) + umap = Map.filterWithKey (\n _ -> n `elem` multiNodes) usemap + + before = (\gr node edgemap arg indexList -> + let edges = filter (\x -> snd . thd3 . fst $ x < arg) edgemap + + -- sorts and groups by which output of the command each edge is using + sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ c)) edges + grouped = groupBy (\x y -> snd . thd3 . fst $ x == snd . thd3 . fst $ y) sorted + + -- makes a list of pairs of (maximum, restOfList) + maxSplit = map (\x -> partition (\y -> y == maximumBy useSort x)) grouped + + refNodeEdges = map (fst . snd) maxSplit + removeNodeEdges = concat (map (fst . fst) maxSplit) + + usedArgs = filter (\x -> x `elem` (map (snd . thd3) removeNodeEdges)) [1..(arg-1)] + + -- creates a graphpart to define and pop all the initial outputs to get to the used one in the middle + defGen = (\num -> + if (num == arg) + then [] + else if (index!!num `elem` usedArgs) + then [index!!num, "def", "pop"] ++ defGen (num+1) + else ["pop"] ++ defGen (num+1)) + defPart = genPart (defGen 0) True + + -- creates graphparts for removing all the items stored in the dictionary, including node attachments + removeList = zip usedArgs removeNodeEdges + removePart = map (\(x,y) -> (genPart [index!!(x-1), "remove"] False, Nothing, [edgeToNode y])) removeList + + -- creates graphparts to reference all the items stored in the dictionary, including node attachments + refList = zip usedArgs refNodeEdges + refPart = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, (map edgeToNode y))) refList + + in (defPart, refPart ++ removePart)) + + + after = (\gr node edgemap arg indexList -> + let -- obtain edges after the cutoff argument + edges = filter (\x -> snd . thd3 . fst $ x > arg) edgemap + + -- sort and group by which output of the command each edge is using + sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ c)) edges + grouped = groupBy (\x y -> snd . thd3 . fst $ x == snd . thd3 . fst $ y) sorted + + mins = map (minimumBy useSort) grouped + initEdge = minimumBy useSort (Map.toList edgemap) + + usedArgs = filter (\x -> x `elem` (map (snd . thd3 . fst) mins)) [(arg+1)..(nodeOutput gr node)] + edgeToNode = (\x -> (fst3 x, fst . thd3 $ x)) + + -- finds the argument where you have to pop everything and store it all in the dictionary before + -- proceeding + findAttach = (\x y -> + if (x == []) + then nodeOutput gr node + else let allZero = all (=0) (snd . snd . head $ x) + headIsMin = (head x) == (minimumBy useSort x) + headThmLowestStrict = let testList = map (fst . snd) x + in all (> head testList) (tail testList) + nextUsedArg = snd . thd3 . fst . head . tail $ x + in if (allZero && headIsMin && headThmLowestStrict) + then findAttach (tail x) nextUsedArg + else y) + + argToAttach = findAttach initEdge:mins arg + + process = (\attach curArg modp ordp -> + case (compare arg argToAttach) of + LT -> + EQ -> + GT ->) + + (modParts, ordinaryParts) = process argToAttach arg [] [] + + -- calculate the def/pop/ref defPart + afterPartInit = + afterPart = + if (argToAttach == arg) + then + else + + -- calculate def nodes/parts for outputs before the argToAttach + defs = + makeDefList = + defPart = map (\(x,y) -> (genPart [index!!(x-1), "def"] False, Nothing, [edgeToNode y])) makeDefList + + -- calculate ref and remove nodes/parts + maxes = map (maximumBy useSort) grouped + refs = map (filter (\x -> x `notElem` maxes && x `notElem` defs)) grouped + + removeList = zip usedArgs maxes + removePart = map (\(x,y) -> (genPart [index!!(x-1), "remove"] False, Nothing, [edgeToNode y])) removeList + + -- creates graphparts to reference all the items stored in the dictionary, including node attachments + refList = zip usedArgs refs + refPart = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, (map edgeToNode y))) refList + + in (modParts, ordinaryParts)) + + addPreserveNodeParts = (\partList graph -> + ) + + f = (\gr node edgemap -> + let edgeList = Map.toList edgemap + + out = nodeOutput gr node + index = next (out + 1) gr + + initEdge = fst (minimumBy useSort edgeList) + initArg = snd . thd3 $ initEdge + (defBefore, beforeParts) = before gr node edgemap initArg (take (initArg-1) index) + (defAfter, afterParts) = after gr node edgemap initArg (drop initArg index) + edgesToRemove = filter (\x -> x /= initEdge) (map fst edgeList) + + gr' = addPreserveNodeParts defAfter gr + + edgesRemoved = foldl' (\x y -> Graph.delLEdge y x) gr' edgesToRemove + partsAdded = graphAddList partList edgesRemoved + in partsAdded) + + in foldl' (\g n -> f g n (fromJust (Map.lookup n umap))) graph multiNodes + + + + + + + + + + + + + +multiCommands :: PGraph -> PGraph -> UsageMap -> [Node] -> PGraph +multiCommands graph orig usemap nodeList = + let process = (\gr stack dict workmap edge -> + let node = snd3 edge + label = fromJust (Graph.lab gr node) + in if (label == "def" || label == "ref" || label == "remove" || isNumber label) + then dictProcess gr stack dict workmap edge + else regProcess gr stack dict workmap edge + + + dictProcess = (\gr stack dict workmap edge -> + let node = snd3 edge + label = fromJust (Graph.lab gr node) + index = fromJust (Graph.lab gr (head (Graph.suc gr node))) + + in if (label == "def") + then let dict' = Map.insert index (head stack) dict + in (gr, stack, dict', workmap) + + else if (label == "ref") + then let stack' = (fromJust (Map.lookup index dict)):stack + in (gr, stack', dict, workmap) + + else if (label == "remove") + then let stack' = (fromJust (Map.lookup index dict)):stack + dict' = Map.delete index dict + in (gr, stack', dict', workmap) + else -- isNumber label + (gr, stack, dict, workmap) + + + regProcess = (\gr stack dict workmap edge -> + let node = snd3 edge + label = fromJust (Graph.lab gr node) + + io = argMap label + sortedIns = sortBy (\x y -> compare (fst . thd3 $ x) (fst . thd3 $ y)) (Graph.out orig node) + expectedInput = map (\(a,b,(c,d)) -> (b,d)) sortedIns + + consume = (\(g,s,d,w) inList -> + if (inList == []) + then if (nodeOutput == 1) + then (g, (node,1):s, d, w) + else initial (g,s,d,w) + else let i = head inList + in if (head s == i) + then consume (g, tail s, d, w) (tail inList) + else store (g, s, d, w) inList) + + initial = (\(g,s,d,w) inList -> + let edgemap = Map.toList (fromJust (Map.lookup node usemap)) + sorted = sortBy (\(a,b) (c,d) -> compare (snd . thd3 $ a) (snd . thd3 $ b)) edgemap + grouped = groupBy (\x y -> (snd . thd3 . fst $ x) == (snd . thd3 . fst $ y)) sorted + minimals = map (minimumBy useSort) grouped + usedArgs = filter (\x -> x `elem` (map (snd . thd3 . fst) minimals)) [1..nodeOutput] + atArg = snd . thd3 $ edge + atArgReuse = length (filter (\x -> (snd . thd3 . fst $ x) == atArg) edgemap) + fromStart = fst . snd $ (head (filter (\x -> ((snd . thd3 . fst $ x) == atArg)) minimals)) + edgesToRemove = filter (\x -> (snd . thd3 $ x) < upTo) (map fst edgemap) + + upTo = let shortList = filter (\x -> (snd . thd3 . fst $ x) > atArg && (fst . snd $ x) > fromStart) minimals + in if (shortList == []) + then nodeOutput + 1 + else let shortNum = snd . thd3 . fst . head $ shortList + calc = (\num -> + if (filter (\x -> (snd . thd3 . fst $ x) == num - 1) edgemap == []) + then calc (num - 1) + else num) + in calc shortNum + index = next upTo g + + defPartGen = (\num -> + if (num == upTo) + then if (atArg + 1 < upTo) + then if (atArgReuse > 1) + then [index!!atArg, "ref"] + else [index!!atArg, "remove"] + else [] + else if (num `elem` usedArgs) + then if (num + 1 == atArg &&) + else if (num == atArg) + then if (atArgReuse <= 1 && atArg + 1 == upTo) + then defPartGen (num+1) + else if (atArg + 1 < upTo) + then [index!!num, "def", "pop"] ++ (defPartGen (num+1)) + else [index!!num, "def"] ++ (defPartGen (num+1)) + else [index!!num, "def", "pop"] ++ (defPartGen (num+1)) + else ["pop"] ++ (defPartGen (num+1))) + defPart = genPart (defPartGen 1) True + + maxSplit = map (\x -> partition (\y -> y == maximumBy useSort x)) grouped + refNodeEdges = map (fst . snd) maxSplit + removeNodeEdges = concat (map (fst . fst) maxSplit) + + removeList = zip usedArgs removeNodeEdges + removePart = map (\(x,y) -> (genPart [index!!(x-1), "remove"] False, Nothing, [edgeToNode y])) removeList + + refList = zip usedArgs refNodeEdges + refPart = map (\(x,y) -> (genPart [index!!(x-1), "ref"] False, Nothing, (map edgeToNode y))) refPart + + workingEdge = + let atArgEdges = filter (\x -> (snd . thd3 . fst $ x) == atArg) edgemap + initEdge = fst . head $ (filter (\x -> (snd . thd3 $ x) == atArg && + (x `notElem` (delete (minimumBy useSort atArgEdges) + atArgEdges))) (Graph.inn g' node)) + calc = (\e -> + if (fst3 e == fst3 edge) + then e + else calc (head (Graph.inn g' (fst3 e)))) + in calc initEdge + w' = Map.insert node workingEdge + + storedArgs = if (atArgReuse > 1 || atArg + 1 < upTo) + then filter (< upTo) usedArgs + else delete atArg (filter (< upTo) usedArgs) + dictAddList = map (\x -> (index!!(x-1), (node,x))) storedArgs + d' = foldl' (\x (y,z) -> Map.insert y z x) d dictAddList + + stackArgs = atArg:(filter (>= upTo) usedArgs) + stackAddList = map (\x -> (node,x)) stackArgs + s' = stackArgs ++ s + + edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) g edgesToRemove + g' = graphAddList (defPart:(refPart ++ removePart)) edgesRemoved + + in (g', s', d', w')) + + + store = (\(g,s,d,w) inList -> + let s' = tail s + (node, arg) = head s -- the thing on the stack that shouldnt be there + workEdge = Map.lookup node w + (reqNode, reqArg) = head inList -- what we want on the stack instead + + index = head (next 1 g) + edgemap = Map.toList (Map.lookup node usemap) -- map of the edges leading into the node + edgesOfArg = filter (\(x,y) -> (snd . thd3 $ x) == arg) edgemap -- edges using the arg we want to get rid of + + removeEdge = maximumBy useSort edgesOfArg + refEdgeList = delete removeEdge edgesOfArg + + defPart = genPart [index, "def"] True + refPart = genPart [index, "ref"] False + removePart = genPart [index, "remove" False + popPart = genPart ["pop"] True + + in consume (g', s', d', w') inList + + in consume (gr,stack,dict,workmap) expectedInput) + + + h = (\gr st di ma edge -> + let node = snd3 edge + (gr',st',di',ma') = f gr st di ma node + in process gr' st' di' ma' edge) + + f = (\gr st di ma no -> + let args = reverse [1..(nodeOutput gr no)] + func = (\(g,s,d,m) a -> + let edge = filter (\x -> fst . thd3 $ x == a) (Graph.out g no) + in if (edge == []) + then (g,s,d,m) + else h gr st di ma (head edge) + in foldl' func (gr,st,di,ma) args + + stack = [] + dictionary = Map.empty + workmap = Map.empty + + (graph',stack',dictionary',workmap') = + foldl' (\(g,s,d,m) n -> f g s d m n) (graph, stack, dictionary, workmap) nodeList + + in graph' + + + +
\ No newline at end of file diff --git a/TermNetTest.hs b/TermNetTest.hs index 6588a93..57eb06f 100644 --- a/TermNetTest.hs +++ b/TermNetTest.hs @@ -11,15 +11,16 @@ main = do let thm1 = Theorem (Set.empty) stdConstTerm thm2 = Theorem (Set.empty) (stdVarTerm "b") thm3 = Theorem (Set.empty) (stdVarTerm "c") + thm4 = Theorem (Set.empty) (stdAbsTerm "h") - (net1, matches1) = Net.addThm Net.empty thm1 0 - (net2, matches2) = Net.addThm net1 thm2 1 - (net3, matches3) = Net.addThm net2 thm3 2 + net1 = Net.addThm Net.empty thm1 0 + net2 = Net.addThm net1 thm2 1 + net3 = Net.addThm net2 thm3 2 + net4 = Net.addThm net3 thm4 3 + match = Net.matchThm net4 thm4 + - putStrLn (show net3) + putStrLn (show net4) putStrLn "" - putStrLn (show matches3) - putStrLn (intercalate " " . Net.thmToTermString $ thm1) - putStrLn (intercalate " " . Net.thmToTermString $ thm2) - putStrLn (intercalate " " . Net.thmToTermString $ thm3) + putStrLn (show match) diff --git a/Test/name.art b/Test/name.art index 7cc35dd..bb89c74 100644 --- a/Test/name.art +++ b/Test/name.art @@ -1 +1 @@ -"name" +"bool" diff --git a/Test/timer.sh b/Test/timer.sh index c95aff5..2a1e7c3 100644 --- a/Test/timer.sh +++ b/Test/timer.sh @@ -1,6 +1,6 @@ #!/bin/bash -for i in {1..1000} +for i in {1..1} do $1 $2 > /dev/null done diff --git a/bin/.gitignore b/bin/.gitignore new file mode 100644 index 0000000..ce82cfb --- /dev/null +++ b/bin/.gitignore @@ -0,0 +1,5 @@ + +# directory for binaries; no files will be tracked here + +* +!.gitignore @@ -1,5 +1,5 @@ -OUTPUTDIR = ./bin +OUTPUTDIR = bin @@ -0,0 +1,3 @@ +#!/bin/bash + +/usr/bin/time -f "%E" ./Test/timer.sh $1 $2 diff --git a/writetest.hs b/writetest.hs index 81df3d7..0a05ccb 100644 --- a/writetest.hs +++ b/writetest.hs @@ -1,9 +1,20 @@ import Library.WriteProof import Library.ProofGraph +import Library.GraphPart +import Data.Graph.Inductive.Graph( Node, LNode, Edge, LEdge ) +import qualified Data.Graph.Inductive.Graph as Graph +import Data.Map( Map ) +import qualified Data.Map as Map +import Data.Set( Set ) +import qualified Data.Set as Set +import Data.List +import Library.Usage +import Library.Parse + list = [-- create a var term, define a constant to it - "\"const\"","\"x\"","const","\"t1\"","typeOp","nil","opType","1","def","constTerm","0","def","defineConst", + "\"c\"","\"x\"","const","\"t1\"","typeOp","nil","opType","1","def","constTerm","0","def","defineConst", -- hypothesis list for theorem "nil", @@ -19,7 +30,7 @@ list = [-- create a var term, define a constant to it "constTerm", -- the constant - "\"const\"","const","1","remove","constTerm", + "\"c\"","const","1","remove","constTerm", -- construct the equation of constant = variable "appTerm", @@ -28,16 +39,42 @@ list = [-- create a var term, define a constant to it "thm","pop"] -graph = doGraphGen list +list2 = ["\"x\"", "const", "\"bool\"", "typeOp", "nil", "opType", "constTerm", "assume", "1", "def", "1", "remove", "deductAntisym"] + -fst3 :: (a,b,c) -> a -fst3 (a,_,_) = a +singleNodes = (\g -> filter (\x -> nodeOutput g x == 1 && Graph.indeg g x > 1) (Graph.nodes g)) +singleNodeSet = (\g -> Set.fromList (singleNodes g)) -snd3 :: (a,b,c) -> b -snd3 (_,b,_) = b -thd3 :: (a,b,c) -> c -thd3 (_,_,c) = c +graph = doGraphGen list +graph2 = doGraphGen list2 + edgeCheck :: (Ord d) => (a,b,(c,d)) -> (e,f,(g,d)) -> Ordering edgeCheck = (\a b -> compare (snd . thd3 $ a) (snd . thd3 $ b)) + + +f :: PGraph -> Node -> Map (LEdge (Int,Int)) Int -> PGraph +f = (\graph node edgemap -> + let index = head (next 1 graph) + edgeList = Map.toList edgemap + + sortFunc = (\(w,x) (y,z) -> compare x z) + + defEdge = fst (minimumBy sortFunc edgeList) + refEdgeList = map fst (filter (\x -> fst x /= defEdge && fst x /= removeEdge) edgeList) + removeEdge = fst (maximumBy sortFunc edgeList) + + defPart = genPart [index, "def"] True + refPart = genPart [index, "ref"] False + removePart = genPart [index, "remove"] False + + defNode = (fst3 defEdge,1) + refNodeList = map (\x -> (fst3 x,1)) refEdgeList + removeNode = (fst3 removeEdge,1) + + edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) graph edgeList + partsAdded = graphAddList [(defPart, Just (node,1) , [defNode]), + (refPart, Nothing, refNodeList), + (removePart, Nothing, [removeNode])] edgesRemoved + in partsAdded) |