From 6073c3d6bac564dccafe2799bc247e87490178af Mon Sep 17 00:00:00 2001 From: Jed Barber Date: Thu, 26 Jul 2012 09:27:31 +1000 Subject: Linearisation of multi-output commands (has a few compile errors) --- WriteProof.hs | 101 ++++++++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 92 insertions(+), 9 deletions(-) diff --git a/WriteProof.hs b/WriteProof.hs index 00c4802..aed7f6a 100644 --- a/WriteProof.hs +++ b/WriteProof.hs @@ -24,6 +24,8 @@ output :: Gr String (Int,Int) -> Node -> Int output graph node = let label = fromJust (Graph.lab graph node) in case label of + "thm" -> 0 + "pop" -> 0 "defineConst" -> 2 "defineTypeOp" -> 5 x -> 1 @@ -45,12 +47,13 @@ cost graph node = -next :: Gr String (Int,Int) -> String -next graph = +next :: Int -> Gr String (Int,Int) -> [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) - in show (f 0 numList) + g = (\x y -> if (x == 0) then y else g (x - 1) (f 0 (y ++ numList) : y)) + in map show (g num []) @@ -78,9 +81,89 @@ orderNodes graph nodeList = nodeList -multiCommands :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int) -multiCommands graph nodeList = graph ---placeholder +removeOverlap :: Gr String (Int,Int) -> 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 + + + +--multiCommands :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int) +--multiCommands graph nodeList = +-- let trace = (\g n cn ca ->) +-- +-- r = (\g n p -> let g' = if ((output g n) <= 1) +-- then g +-- else let (argToUseDict, (place, placeArg)) = trace g n n 1 +-- edgesToRemove = +-- edgesRemoved = foldl' (\x y -> Graph.delLEdge y x) g edgesToRemove +-- defSubGraph = +-- edgesToRef = +-- new = +-- refsToAdd = +-- done = foldl' insertSubGraph edgesRemoved refsToAdd +-- in done +-- in f g' n) +-- +-- f = (\g n -> let argList = (removeOverlap g) . reverse $ [1 .. (Graph.outdeg g n)] +-- in foldl' (\x y -> r x (getArg x n y) n) g argList) +-- +-- in foldl' f graph nodeList + + + +multiCommandsSimple :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int) +multiCommandsSimple graph nodeList = + let r = (\g n p -> let g' = if (output g n <= 1) + then g + else let ou = output 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 + + edgeCheck = (\x y -> if ((snd . thd3 $ x) > (snd . thd3 $ y)) then GT + else if ((snd . thd3 $ x) < (snd . thd3 $ y)) then LT + else EQ) + oldEdge = maximumBy edgeCheck (filter (\x -> fst3 == p) (Graph.inn g n)) + toConvert = delete oldEdge (Graph.inn g n) + + defNodeGen = (\i n x lim -> if (x >= lim) + then [] + else [(n!!(x*3), i!!x), (n!!(x*3+1), "def"), + (n!!(x*3+2), "pop")] ++ (defNodeGen i n (x+1) lim)) + defNodes = (defNodeGen index defNew 0 ou) ++ [(3*ou, index!!(snd . thd3 $ oldEdge)), (3*ou+1, "ref")] + defEdgeGen = (\x b -> let x' = [(fst . snd $ x, fst b, (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 + + refGen = (\n lab -> [(n!!(2*lab), index!!lab), (n!!(2*lab+1), "ref")]) + refNodes = map (refGen refNew) [1 .. (ou)] + refEdges = map (\[x,y] -> (y,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 (getArg x n y) n) g argList) + + in foldl' f graph nodeList @@ -88,7 +171,7 @@ singleCommands :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int) singleCommands graph nodeList = let r = (\g n p -> let g' = if (((output g n) /= 1) || ((Graph.indeg g n) == 1) || ((cost g n) < 3) || ((cost g n) == 3 && (Graph.indeg g n) < 3)) then g - else let index = next g --show . length . (nubBy (\x y -> snd x == snd y)) $ (filter (isNumber . snd) (Graph.labNodes g)) + else let index = head (next 1 g) new = Graph.newNodes 4 g -- 2 new nodes for def and 2 new nodes for ref oldEdge = head $ (filter (\x -> fst3 x == p) (Graph.inn g n)) @@ -107,7 +190,7 @@ singleCommands graph nodeList = in done in f g' n) - f = (\g n -> let argList = reverse [1 .. (Graph.outdeg g n)] + f = (\g n -> let argList = reverse $ [1 .. (Graph.outdeg g n)] in foldl' (\x y -> r x (getArg x n y) n) g argList) in foldl' f graph nodeList @@ -125,7 +208,7 @@ removeUnused graph nodeList = resolve :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int) resolve graph nodeList = - foldl' (\g f -> f g nodeList) graph [removeUnused, singleCommands, multiCommands] + foldl' (\g f -> f g nodeList) graph [removeUnused, singleCommands, multiCommandsSimple] -- cgit