diff --git a/changelog.md b/changelog.md --- a/changelog.md +++ b/changelog.md @@ -1,5 +1,7 @@ # Changelog +## 0.1.6.7 + ## 0.1.6.6 - [compatibility] with ghc 8.0.1 diff --git a/src/UHC/Util/CHR/Base.hs b/src/UHC/Util/CHR/Base.hs --- a/src/UHC/Util/CHR/Base.hs +++ b/src/UHC/Util/CHR/Base.hs @@ -414,7 +414,7 @@ chrmatcherLift f = do [sl,sg] <- fmap unStackedVarLookup $ getl chrmatcherstateVarLookup -- gets (unStackedVarLookup . _chrmatcherstateVarLookup) maybe chrMatchFail (\snew -> chrmatcherstateVarLookup =$: (snew |+>)) $ f sg - + -- | Run a CHRMatcher chrmatcherRun' :: (CHREmptySubstitution subst) => (CHRMatcherFailure -> r) -> (subst -> CHRWaitForVarSet subst -> x -> r) -> CHRMatcher subst x -> CHRMatchEnv (VarLookupKey subst) -> StackedVarLookup subst -> r chrmatcherRun' fail succes mtch menv s = either diff --git a/src/UHC/Util/CHR/Solve/TreeTrie/Examples/Term/Main.hs b/src/UHC/Util/CHR/Solve/TreeTrie/Examples/Term/Main.hs --- a/src/UHC/Util/CHR/Solve/TreeTrie/Examples/Term/Main.hs +++ b/src/UHC/Util/CHR/Solve/TreeTrie/Examples/Term/Main.hs @@ -8,8 +8,10 @@ import Data.Maybe import System.IO +import Data.Time.Clock.POSIX import Control.Monad import Control.Monad.IO.Class +import Control.Monad.State.Class import qualified Data.Set as Set import UU.Parsing @@ -21,11 +23,14 @@ import UHC.Util.CHR.GTerm.Parser import UHC.Util.CHR.Solve.TreeTrie.MonoBacktrackPrio as MBP import UHC.Util.CHR.Solve.TreeTrie.Examples.Term.AST +-- import UHC.Util.CHR.Solve.TreeTrie.Examples.Term.Parser +import UHC.Util.CHR.Solve.TreeTrie.Visualizer data RunOpt = RunOpt_DebugTrace -- ^ include debugging trace in output | RunOpt_SucceedOnLeftoverWork -- ^ left over unresolvable (non residue) work is also a successful result | RunOpt_SucceedOnFailedSolve -- ^ failed solve is considered also a successful result, with the failed constraint as a residue + | RunOpt_WriteVisualization -- ^ write visualization (html file) to disk | RunOpt_Verbosity Verbosity deriving (Eq) @@ -62,9 +67,19 @@ r <- chrSolve sopts () let verbosity = maximum $ [Verbosity_Quiet] ++ maybeToList (mbRunOptVerbosity runopts) ++ (if RunOpt_DebugTrace `elem` runopts then [Verbosity_ALot] else []) ppSolverResult verbosity r >>= \sr -> liftIO $ putPPLn $ "Solution" >-< indent 2 sr + if (RunOpt_WriteVisualization `elem` runopts) + then + do + (CHRGlobState{_chrgstTrace = trace}, _) <- get + time <- liftIO getPOSIXTime + let fileName = "visualization-" ++ show (round time) ++ ".html" + liftIO $ writeFile fileName (showPP $ chrVisualize query trace) + liftIO $ msg "VISUALIZATION" + liftIO $ putStrLn $ "Written visualization as " ++ fileName + else (return ()) return r runCHRMonoBacktrackPrioT (emptyCHRGlobState) (emptyCHRBackState {- _chrbstBacktrackPrio=0 -}) {- 0 -} mbp - + -- done msg $ "DONE " ++ f diff --git a/src/UHC/Util/CHR/Solve/TreeTrie/Internal.hs b/src/UHC/Util/CHR/Solve/TreeTrie/Internal.hs --- a/src/UHC/Util/CHR/Solve/TreeTrie/Internal.hs +++ b/src/UHC/Util/CHR/Solve/TreeTrie/Internal.hs @@ -377,6 +377,7 @@ , stMatchCache :: !(SolveMatchCache' c sr s) , stHistoryCount :: WorkTime , stLastQuery :: (LastQuery c) + , stUsedRules :: [r] } stDoneCnstrs :: SolveState' c r sr s -> [c] @@ -384,7 +385,7 @@ {-# INLINE stDoneCnstrs #-} emptySolveState :: SolveState' c r sr s -emptySolveState = SolveState emptyWorkList Set.empty [] Map.empty Map.empty initWorkTime emptyLastQuery +emptySolveState = SolveState emptyWorkList Set.empty [] Map.empty Map.empty initWorkTime emptyLastQuery [] {-# INLINE emptySolveState #-} solveStateResetDone :: SolveState' c r sr s -> SolveState' c r sr s diff --git a/src/UHC/Util/CHR/Solve/TreeTrie/Internal/Shared.hs b/src/UHC/Util/CHR/Solve/TreeTrie/Internal/Shared.hs --- a/src/UHC/Util/CHR/Solve/TreeTrie/Internal/Shared.hs +++ b/src/UHC/Util/CHR/Solve/TreeTrie/Internal/Shared.hs @@ -110,6 +110,7 @@ = SolveStep { stepChr :: r , stepSubst :: s + , stepAlt :: Maybe [c] , stepNewTodo :: [c] , stepNewDone :: [c] } @@ -129,9 +130,9 @@ show _ = "SolveStep" instance (PP r, PP c) => {- (PP c, PP g) => -} PP (SolveStep' c r s) where - pp (SolveStep step _ todo done) = "STEP" >#< (step >-< "new todo:" >#< ppBracketsCommas todo >-< "new done:" >#< ppBracketsCommas done) - pp (SolveStats stats ) = "STATS" >#< (ppAssocLV (Map.toList stats)) - pp (SolveDbg p ) = "DBG" >#< p + pp (SolveStep step _ _ todo done) = "STEP" >#< (step >-< "new todo:" >#< ppBracketsCommas todo >-< "new done:" >#< ppBracketsCommas done) + pp (SolveStats stats ) = "STATS" >#< (ppAssocLV (Map.toList stats)) + pp (SolveDbg p ) = "DBG" >#< p ppSolveTrace :: (PP r, PP c) => {- (PP s, PP c, PP g) => -} SolveTrace' c r s -> PP_Doc ppSolveTrace tr = ppBracketsCommasBlock [ pp st | st <- tr ] diff --git a/src/UHC/Util/CHR/Solve/TreeTrie/Mono.hs b/src/UHC/Util/CHR/Solve/TreeTrie/Mono.hs --- a/src/UHC/Util/CHR/Solve/TreeTrie/Mono.hs +++ b/src/UHC/Util/CHR/Solve/TreeTrie/Mono.hs @@ -18,6 +18,8 @@ ( CHRStore , emptyCHRStore + , StoredCHR(..) + , chrStoreFromElems , chrStoreUnion , chrStoreUnions @@ -291,7 +293,7 @@ ) : tlMatch ) = do let b = ruleBody chr - st@(SolveState {stWorkList = wl, stHistoryCount = histCount}) <- get + st@(SolveState {stWorkList = wl, stHistoryCount = histCount, stUsedRules = usedRules }) <- get let (tlMatchY,tlMatchN) = partition (\(r@(_,(ks,_)),_) -> not (any (`elem` keysSimp) ks || slvIsUsedByPropPart (wlUsedIn wl') r)) tlMatch (keysSimp,keysProp) = splitAt simpSz keys usedIn = Map.singleton (Set.fromList keysProp) (Set.singleton chrId) @@ -309,6 +311,7 @@ , stDoneCnstrSet = Set.unions [Set.fromList bDone, Set.fromList $ map workCnstr $ take simpSz works, stDoneCnstrSet st] , stMatchCache = if List.null bTodo' then stMatchCache st else Map.empty , stHistoryCount = histCount + 1 + , stUsedRules = (chr : usedRules) } {- chr'= subst `varUpd` chr diff --git a/src/UHC/Util/CHR/Solve/TreeTrie/MonoBacktrackPrio.hs b/src/UHC/Util/CHR/Solve/TreeTrie/MonoBacktrackPrio.hs --- a/src/UHC/Util/CHR/Solve/TreeTrie/MonoBacktrackPrio.hs +++ b/src/UHC/Util/CHR/Solve/TreeTrie/MonoBacktrackPrio.hs @@ -44,6 +44,9 @@ , CHRSolveOpts(..) , defaultCHRSolveOpts + , StoredCHR + , storedChrRule' + , chrSolve , slvFreshSubst @@ -155,6 +158,8 @@ -- , storedIdent :: !(UsedByKey c) -- ^ the identification of a CHR, used for propagation rules (see remark at begin) } deriving (Typeable) +storedChrRule' :: StoredCHR c g bp p -> Rule c g bp p +storedChrRule' = _storedChrRule type instance TTKey (StoredCHR c g bp p) = TTKey c @@ -989,7 +994,7 @@ slv1 curbprio (FoundWorkSortedMatch { foundWorkSortedMatchInx = CHRConstraintInx {chrciInx = ci} - , foundWorkSortedMatchChr = StoredCHR {_storedChrRule = Rule {ruleSimpSz = simpSz}} + , foundWorkSortedMatchChr = chr@StoredCHR {_storedChrRule = Rule {ruleSimpSz = simpSz}} , foundWorkSortedMatchBodyAlts = alts , foundWorkSortedMatchWorkInx = workInxs , foundWorkSortedMatchSubst = matchSubst @@ -1000,19 +1005,30 @@ -- depending on nr of alts continue slightly different case alts of -- just continue if no alts - [] -> slv + [] -> do + log Nothing + slv -- just reschedule [alt@(FoundBodyAlt {foundBodyAltBacktrackPrio=bprio})] - | curbprio == bprio -> nextwork bprio alt + | curbprio == bprio -> do + log (Just alt) + nextwork bprio alt | otherwise -> do + log (Just alt) slvSchedule bprio $ nextwork bprio alt slvScheduleRun -- otherwise backtrack and schedule all and then reschedule alts -> do - forM alts $ \alt@(FoundBodyAlt {foundBodyAltBacktrackPrio=bprio}) -> (backtrack $ nextwork bprio alt) >>= slvSchedule bprio + forM alts $ \alt@(FoundBodyAlt {foundBodyAltBacktrackPrio=bprio}) -> do + log (Just alt) + (backtrack $ nextwork bprio alt) >>= slvSchedule bprio slvScheduleRun where + log alt = do + let a = (fmap (rbodyaltBody . foundBodyAltAlt) alt) + let step = SolveStep chr matchSubst a [] [] -- TODO: Set stepNewTodo, stepNewDone (last two arguments) + fstl ^* chrgstTrace =$: (step:) nextwork bprio alt@(FoundBodyAlt {foundBodyAltAlt=(RuleBodyAlt {rbodyaltBody=body})}) = do -- set prio for this alt sndl ^* chrbstBacktrackPrio =: bprio diff --git a/src/UHC/Util/CHR/Solve/TreeTrie/Visualizer.hs b/src/UHC/Util/CHR/Solve/TreeTrie/Visualizer.hs new file mode 100644 --- /dev/null +++ b/src/UHC/Util/CHR/Solve/TreeTrie/Visualizer.hs @@ -0,0 +1,568 @@ +{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-} + +module UHC.Util.CHR.Solve.TreeTrie.Visualizer + ( chrVisualize + ) + where + +import Prelude +import Data.Maybe +import Data.List +import qualified Data.Map as Map +import UHC.Util.Pretty +import UHC.Util.PrettySimple +import UHC.Util.CHR.Rule +import UHC.Util.CHR.GTerm.Parser +import UHC.Util.CHR.Solve.TreeTrie.Mono +import UHC.Util.CHR.Solve.TreeTrie.MonoBacktrackPrio as MBP +import UHC.Util.CHR.Solve.TreeTrie.Examples.Term.AST +import UHC.Util.CHR.Solve.TreeTrie.Internal +import UHC.Util.CHR.Solve.TreeTrie.Internal.Shared +import UHC.Util.Substitutable +import Data.Graph.Inductive.Graph +import Data.Graph.Inductive.Tree + +sortGroupOn :: Ord b => (a -> b) -> [a] -> [[a]] +sortGroupOn f = construct . sortOn f + where + construct [] = [] + construct (y:ys) = group : construct rest + where + group = y : takeWhile ((f y ==) . f) ys + rest = dropWhile ((f y ==) . f) ys + +data NodeData + -- Applied rule with first alt (if it exists) + = NodeRule + { nrLayer :: Int + , nrColumn :: Int + , nrName :: String + , nrRuleVars :: [Tm] + , nrFirstAlt :: Maybe C + } + -- Additional alts of a rule + | NodeAlt + { naLayer :: Int + , naColumn :: Int + , naConstraint :: C + } + -- Added node to make a proper layered graph + -- A proper layered graph is a graph in which all edges + -- go from a layer to the next layer. To satisfy this, + -- we add synthesized nodes on edges that do not skip one + -- or more layers + | NodeSynthesized + { nsLayer :: Int + , nsColumn :: Int + , nsEdgeKind :: EdgeKind + } + +data EdgeKind + = EdgeGuard -- Usage of term in guard of rule. + | EdgeHead -- Usage of term in head of rule. + | EdgeUnify -- Usage of some term that required unification of this node. + | EdgeAlt -- Link between NodeRule and NodeAlt. Both nodes have same layer. + deriving Eq + +type Node' = LNode NodeData +-- | Edge has a kind and a bool that says whether this edge is +-- the last edge of a sequence of edges. The last edge does not +-- end in a synthesized node, the others do. +type Edge' = LEdge (EdgeKind, Bool) +type NodeEdge = (Node', Node', EdgeKind, Bool) + +asEdge :: NodeEdge -> Edge' +asEdge ((from, _), (to, _), kind, isLast) = (from, to, (kind, isLast)) + +-- | Gets the layer of a node +nodeLayer :: Node' -> Int +nodeLayer (_, NodeRule{nrLayer = layer}) = layer +nodeLayer (_, NodeAlt{naLayer = layer}) = layer +nodeLayer (_, NodeSynthesized{nsLayer = layer}) = layer + +-- | Gets the column of a node +nodeColumn :: Node' -> Int +nodeColumn (_, NodeRule{nrColumn = col}) = col +nodeColumn (_, NodeAlt{naColumn = col}) = col +nodeColumn (_, NodeSynthesized{nsColumn = col}) = col + +-- | Sets the column of a node +nodeSetColumn :: Node' -> Int -> Node' +nodeSetColumn (n, d@NodeRule{}) col = (n, d{nrColumn = col}) +nodeSetColumn (n, d@NodeAlt{}) col = (n, d{naColumn = col}) +nodeSetColumn (n, d@NodeSynthesized{}) col = (n, d{nsColumn = col}) + +-- | A map between a term, and the location where it was found combined +-- with the required unifications +type NodeMap = Map.Map Tm (Node', [Node']) +-- | Contains all data needed to build the graph, during traversal of +-- the solve trace +data BuildState = BuildState [Node'] [NodeEdge] NodeMap Int Int +emptyBuildState :: BuildState +emptyBuildState = BuildState [] [] Map.empty 0 0 + +-- | Gives all terms that follow after a unification +replaceInTm :: Tm -> Tm -> Tm -> [Tm] +replaceInTm a b tm + | tm == a || tm == b = [a, b] + | otherwise = case tm of + Tm_Con name tms -> fmap (Tm_Con name) (replaceList tms) + Tm_Lst tms ltm -> do + tms' <- replaceList tms + ltm' <- replaceMaybe ltm + return $ Tm_Lst tms' ltm' + Tm_Op op tms -> fmap (Tm_Op op) (replaceList tms) + x -> [x] + where + replaceList = sequence . fmap (replaceInTm a b) + replaceMaybe Nothing = [Nothing] + replaceMaybe (Just y) = fmap Just $ replaceInTm a b y + +-- | Gives all terms in a constraint +tmsInC :: C -> [Tm] +tmsInC (C_Con s tms) = [Tm_Con s tms] +tmsInC _ = [] + +-- | Gives all terms in a guard +tmsInG :: G -> [Tm] +tmsInG (G_Tm tm) = tmsInTm tm +tmsInG _ = [] + +tmsInTm :: Tm -> [Tm] +tmsInTm tm = tm : children tm + where + children (Tm_Lst as Nothing) = as + children (Tm_Lst as (Just a)) = as ++ [a] + children _ = [] + +-- | Finds all terms that were used for this rule +-- Used by visualizer to draw edges to the origin of +-- these rules. +precedentTms :: Rule C G P P -> [(Tm, EdgeKind)] +precedentTms rule + = fmap (\n -> (n, EdgeHead)) (concatMap tmsInC $ ruleHead rule) + ++ fmap (\n -> (n, EdgeGuard)) (concatMap tmsInG $ ruleGuard rule) + +-- | Adds the constraint (of an alt) to the NodeMap +addConstraint :: C -> Node' -> NodeMap -> NodeMap +addConstraint (CB_Eq a b) = addUnify a b +addConstraint (C_Con s tms) = addTerm $ Tm_Con s tms +addConstraint c = const id + +addTerm :: Tm -> Node' -> NodeMap -> NodeMap +addTerm tm node = Map.insert tm (node, []) + +addUnify :: Tm -> Tm -> Node' -> NodeMap -> NodeMap +addUnify a b node map = Map.foldlWithKey cb map map + where + cb :: NodeMap -> Tm -> (Node', [Node']) -> NodeMap + cb map' tm (n, nodes) = foldl (\map'' key -> Map.insertWith compare key (n, node : nodes) map'') map' (replaceInTm a b tm) + compare x@(_, nodes1) y@(_, nodes2) + | length nodes1 <= length nodes2 = x + | otherwise = y + +-- | Generates nodes and edges for a SolveStep. +-- Stores the resulting terms in the NodeMap. +stepToNodes :: BuildState -> SolveStep' C (MBP.StoredCHR C G P P) S -> BuildState +stepToNodes state@(BuildState _ _ nodeMap nodeId layer) step + = BuildState + nodes + edges'' + nodeMap' + nodeId' + layer' + where + schr = stepChr step + rule = storedChrRule' schr + updRule = varUpd (stepSubst step) rule + alt = maybe [] (fmap $ varUpd $ stepSubst step) $ stepAlt step + (BuildState nodes edges' nodeMap' nodeId' layer', primaryNode) = + createNodes + (maybe "[untitled]" id (ruleName rule)) + (Map.elems (stepSubst step)) + alt + state + edges'' = + ( fmap (\(n, kind) -> (n, primaryNode, kind, True)) + $ concatMap (\(n, ns, kind) -> (n, kind) : fmap (\x -> (x, EdgeUnify)) ns) + $ mapMaybe + (\(tm, kind) -> fmap + (\(n, ns) -> (n, ns, kind)) + (Map.lookup tm nodeMap)) + (precedentTms updRule) + ) + ++ edges' + +createNodes :: String -> [Tm] -> [C] -> BuildState -> (BuildState, Node') +createNodes name vars alts (BuildState previousNodes previousEdges nodeMap nodeId layer) + = ( BuildState (nodes ++ previousNodes) (edges ++ previousEdges) nodeMap' (nodeId + max 1 (length alts)) (layer + 1) + , primaryNode + ) + where + primaryNode = + (nodeId, NodeRule + { nrLayer = layer + , nrColumn = 0 + , nrName = name + , nrRuleVars = vars + , nrFirstAlt = listToMaybe alts + } + ) + nodes = primaryNode : altNodes + altTms = concatMap tmsInC alts + nodeMap' = foldl updateMap nodeMap nodes + -- Updates node map for a new node + updateMap :: NodeMap -> Node' -> NodeMap + updateMap map node@(_, NodeRule{ nrFirstAlt = Just alt }) = addConstraint alt node map + updateMap map node@(_, NodeAlt{ naConstraint = alt }) = addConstraint alt node map + updateMap map _ = map + + altNode (constraint, i) = (nodeId + i, NodeAlt layer 0 constraint) + altNodes = fmap altNode (drop 1 $ addIndices alts) + edges = (fmap (\n -> (primaryNode, n, EdgeAlt, True)) altNodes) + +-- | Adds synthesized nodes to create a proper layered graph +createSynthesizedNodes :: [Node'] -> [NodeEdge] -> Int -> ([NodeEdge], [Node']) +createSynthesizedNodes nodes es firstNode + = create es firstNode [] [] + where + create :: [NodeEdge] -> Int -> [NodeEdge] -> [Node'] -> ([NodeEdge], [Node']) + create ((edge@(from, to, kind, _)):edges) id accumEdges accumNodes + = create edges id' (es ++ accumEdges) (ns ++ accumNodes) + where + (es, ns, id') = split (nodeLayer from) edge id + create _ _ accumEdges accumNodes = (accumEdges, accumNodes) + split :: Int -> NodeEdge -> Int -> ([NodeEdge], [Node'], Int) + split fromLayer edge@(from, to, kind, _) id + | fromLayer + 1 >= nodeLayer to = ([edge], [], id) + | otherwise = + ( (from, node, kind, False) : edges', + node : nodes', + id' + ) + where + node = (id, (NodeSynthesized (fromLayer + 1) 0 kind)) + (edges', nodes', id') = split (fromLayer + 1) (node, to, kind, True) (id + 1) + +-- | Creates a graph with the visualization +createGraph :: [C] -> [SolveStep' C (MBP.StoredCHR C G P P) S] -> Gr NodeData (EdgeKind, Bool) +createGraph query steps = mkGraph sortedLayers (fmap asEdge edges) + where + -- | Sort the layers by giving each node in a layer an unique nodeColumn value + sortedLayers = sortedFirstLayer ++ sortNodes maxLayerSize (sortedFirstLayer : layers) layeredEdges + -- | Set the nodeColumn values of each of the nodes in the query (the query forms the first layer) + sortedFirstLayer = uniqueColumns firstLayer ((maxLayerSize - length firstLayer) `div` 2) + -- | Extracting [[Node']] from layerNodes + firstLayer : layers = sortGroupOn nodeLayer nodes + -- firstLayer : layers = Map.elems $ layerNodes nodes + -- | For each layer we create a list with the nodes in that layer + -- layerNodes :: [Node'] -> Map.Map Int [Node'] + -- layerNodes ns = foldl (\m x -> Map.insertWith (++) (nodeLayer x) [x] m) Map.empty ns + (state, _) = createNodes "?" [] query emptyBuildState + BuildState nodes' edges' _ id _ = foldr (flip stepToNodes) state steps + (edges, synNodes) = createSynthesizedNodes nodes' edges' id + nodes = nodes' ++ synNodes + maxLayerSize = maximum $ fmap length (firstLayer : layers) + edgesCrossLayer = filter (\(from, to, _, _) -> nodeLayer from /= nodeLayer to) edges + layeredEdges = sortGroupOn (nodeLayer . fst') edgesCrossLayer + +-- | Sort the nodes using the median heuristic +-- | The first layer is left as it was, the second layer is sorted using the first etc. +sortNodes :: Int -> [[Node']] -> [[NodeEdge]] -> [Node'] +sortNodes _ (x:[]) _ = [] +sortNodes maxLayerSize (x:xs:xss) e = medianHeurstic maxLayerSize x xs edges ++ sortNodes maxLayerSize (xs:xss) rest + where + (edges, rest) = + if null e then + ([], []) + else if (nodeLayer $ fst' $ head $ head e) == nodeLayer (head x) then + (head e, tail e) + else + ([], e) + +-- | lowerLayer is the layer to be sorted, upperLayer is assumed to be sorted +-- | The maxLayerSize is used to center the graph (by altering the value given to uniqueColumns) +-- | Documentation for the median heuristic: +-- | https://cs.brown.edu/~rt/gdhandbook/chapters/hierarchical.pdf +-- | http://www.cs.usyd.edu.au/~shhong/fab.pdf +-- | https://books.google.nl/books?id=6hfsCAAAQBAJ&lpg=PA28&dq=median%20heuristic%20sorting%20vertices&hl=nl&pg=PA28#v=onepage&q&f=false +medianHeurstic :: Int -> [Node'] -> [Node'] -> [NodeEdge] -> [Node'] +medianHeurstic maxLayerSize upperLayer lowerLayer e = uniqueColumns sortedMedianList ((maxLayerSize - length lowerLayer) `div` 2) + where + -- | The medianList sorted on the median values + sortedMedianList = sortOn nodeColumn medianList + -- | The list of median values for each of the nodes in lowerLayer + medianList = map (\x -> nodeSetColumn x (median x)) lowerLayer + -- | The median value of the x coördinates of the neighbors + median n + | neighborCount == 0 = 0 + | otherwise = coords !! (ceiling (realToFrac neighborCount / 2) - 1) + where + coords = coordinates n + neighborCount = length coords + -- | The values of the x coördinates of the neighbors + coordinates n = map nodeColumn (neighbors n) + -- | The neighbor nodes of the given Node' n (on a higher layer) + neighbors n = map (fst') (edges n) + -- | All the edges connected to given Node' n + edges n = filter (\(_, (id, _), _, _) -> id == fst n) e + +-- | Ensure that each Node' has an unique nodeColumn (the x coördinate) +-- | The value of the nodeColumn is set to i +uniqueColumns :: [Node'] -> Int -> [Node'] +uniqueColumns (n:ns) i = nodeSetColumn n i : uniqueColumns ns (i + 1) +uniqueColumns _ _ = [] + +fst' :: (a, b, c, d) -> a +fst' (a, _, _, _) = a + +-- | Creates a HTML tag +tag :: String -> PP_Doc -> PP_Doc -> PP_Doc +tag name attr content = (text ("<" ++ name)) >|< attributes attr >|< body content + where + attributes Emp = Emp + attributes a = text " " >|< a + body Emp = text " />" + body content = text ">" >|< content >|< text ("") + +-- | Creates a HTML tag without attributes +tag' :: String -> PP_Doc -> PP_Doc +tag' name = tag name Emp + +-- | Add indices to an array as a tuple with value and index +addIndices :: [a] -> [(a, Int)] +addIndices = flip zip [0..] + +-- | Generates HTML for a node +showNode :: (Node' -> (Int, Int)) -> Node' -> PP_Doc +showNode pos node@(_, NodeRule{nrLayer = layer, nrName = name, nrRuleVars = vars, nrFirstAlt = alt}) = tag "div" + ( + text "class=\"rule\" style=\"top: " + >|< pp (y + 10) + >|< text "px; left: " + >|< pp x + >|< text "px;\"" + ) + ( + tag "span" (text "class=\"" >|< className >|< text "\"") ( + (text name) + >|< (hlist (fmap ((" " >|<) . pp) vars)) + ) + >|< tag' "br" Emp + >|< text "↳" + >|< tag "span" (text "class=\"rule-alt\"") altText + ) + where + (x, y) = pos node + altText = maybe (text ".") pp alt + className = text "rule-text" + showUsage name var = tag "div" (text $ "class=\"" ++ className ++ "\"") (text " ") + where + className = name ++ " var-" ++ var +showNode pos node@(_, NodeAlt{ naConstraint = constraint }) = tag "div" + ( + text "class=\"rule-additional-alt\" style=\"top: " + >|< pp (y + 10) + >|< text "px; left: " + >|< pp x + >|< text "px;\"" + ) + ( + text "↳" + >|< tag "span" (text "class=\"rule-alt\"") (pp constraint) + ) + where + (x, y) = pos node +showNode _ (_, NodeSynthesized{}) = Emp + +-- | Generates HTML for an edge +showEdge :: (Node -> (Int, Int)) -> Edge' -> PP_Doc +showEdge pos (from, to, (kind, isEnd)) = + if kind == EdgeAlt then + -- Edge between rule and alt of same rule + tag "div" + ( + text "class=\"edge-alt\" style=\"top: " + >|< pp y1 + >|< "px; left: " + >|< pp (min x1 x2) + >|< "px; width: " + >|< abs (x2 - x1 - 16) + >|< "px;\"" + ) + (text " ") + else + tag "div" + ( + text "class=\"edge-ver " + >|< text className + >|< text "\" style=\"top: " + >|< pp (y1 + 35) + >|< "px; left: " + >|< pp x1 + >|< "px; height: " + >|< (y2 - y1 - 60 - 6) + >|< "px;\"" + ) + (text " ") + >|< tag "div" + ( + text "class=\"edge-hor" + >|< text (if x2 > x1 then " edge-hor-left " else if x2 < x1 then " edge-hor-right " else " edge-hor-no-curve ") + >|< text className + >|< text "\" style=\"top: " + >|< pp (y2 - 19) + >|< "px; left: " + >|< pp (if x1 < x2 then x1 else x2 + (if isEnd then 0 else (abs (x2 - x1) + 1) `div` 2)) + >|< "px; width: " + >|< pp (abs (x2 - x1) `div` (if isEnd then 1 else 2)) + >|< "px;\"" + ) + (text " ") + >|< (if isEnd then Emp else tag "div" + ( + text "class=\"edge-end edge-end-" + >|< text (if x2 > x1 then "left " else if x2 < x1 then "right " else "no-curve ") + >|< text className + >|< text "\" style=\"top: " + >|< pp (y2 - 3 + 11) + >|< "px; left: " + >|< pp (if x1 < x2 then (x1 + x2) `div` 2 + 6 else x2) + >|< pp "px; width: " + >|< pp (if x1 == x2 then 0 else ((abs (x2 - x1) + 1) `div` 2) - 6) + >|< "px;\"" + ) + (text " ") + ) + where + (x1, y1) = pos from + (x2, y2) = pos to + className = case kind of + EdgeAlt -> "" + EdgeGuard -> "edge-guard" + EdgeHead -> "edge-head" + EdgeUnify -> "edge-unify" + +-- | Creates a visualization for the given query and solve trace. +-- Output is a PP_Doc containing a HTML file. +chrVisualize :: [C] -> SolveTrace' C (MBP.StoredCHR C G P P) S -> PP_Doc +chrVisualize query trace = tag' "html" $ + tag' "head" ( + tag' "title" (text "CHR visualization") + >|< tag' "style" styles + ) + >|< tag' "body" ( + body + ) + where + graph = createGraph query trace + body = ufold reduce Emp graph >|< hlist (fmap (showEdge posId) $ labEdges graph) + reduce (inn, id, node, out) right = showNode pos (id, node) >|< right + nodeCount = length $ nodes graph + pos :: Node' -> (Int, Int) + pos n = ((nodeColumn n) * 200, (nodeLayer n) * 60) + posId :: Node -> (Int, Int) + posId node = pos (node, fromJust $ lab graph node) + +-- | The stylesheet used in the visualization. +styles :: PP_Doc +styles = + text "body {\n\ + \ font-size: 9pt;\n\ + \ font-family: Arial;\n\ + \}\n\ + \.rule {\n\ + \ position: absolute;\n\ + \ white-space: nowrap;\n\ + \}\n\ + \.rule-text {\n\ + \ border: 1px solid #aaa;\n\ + \ background-color: #fff;\n\ + \ display: inline-block;\n\ + \ padding: 2px;\n\ + \ margin: 3px 1px 0;\n\ + \ min-width: 30px;\n\ + \ text-align: center;\n\ + \}\n\ + \.rule-alt {\n\ + \ display: inline-block;\n\ + \ color: #A89942;\n\ + \ background: #fff;\n\ + \}\n\ + \.rule-additional-alt {\n\ + \ position: absolute;\n\ + \ white-space: nowrap;\n\ + \ margin-top: 24px;\n\ + \}\n\ + \.edge-ver {\n\ + \ position: absolute;\n\ + \ width: 0px;\n\ + \ border-left: 6px solid #578999;\n\ + \ opacity: 0.4;\n\ + \ margin-left: 15px;\n\ + \ margin-top: 9px;\n\ + \ z-index: -1;\n\ + \}\n\ + \.edge-hor {\n\ + \ position: absolute;\n\ + \ height: 27px;\n\ + \ border-bottom: 6px solid #578999;\n\ + \ opacity: 0.4;\n\ + \ margin-left: 15px;\n\ + \ margin-top: 8px;\n\ + \ z-index: -1;\n\ + \}\n\ + \.edge-diag {\n\ + \ transform-origin: 50% 50%;\n\ + \ position: absolute;\n\ + \ height: 6px;\n\ + \}\n\ + \.edge-hor-left {\n\ + \ border-bottom-left-radius: 100% 33px;\n\ + \ border-left: 6px solid #578999;\n\ + \}\n\ + \.edge-hor-right {\n\ + \ border-bottom-right-radius: 100% 33px;\n\ + \ border-right: 6px solid #578999;\n\ + \}\n\ + \.edge-hor-no-curve {\n\ + \ border-right: 6px solid #578999;\n\ + \}\n\ + \.edge-end {\n\ + \ position: absolute;\n\ + \ height: 27px;\n\ + \ width: 16px;\n\ + \ border-top: 6px solid #578999;\n\ + \ opacity: 0.4;\n\ + \ margin-left: 15px;\n\ + \ margin-top: 8px;\n\ + \ z-index: -1;\n\ + \}\n\ + \.edge-end-left {\n\ + \ border-top-right-radius: 100% 33px;\n\ + \ border-right: 6px solid #578999;\n\ + \}\n\ + \.edge-end-no-curve {\n\ + \ border-right: 6px solid #578999;\n\ + \ margin-top: 14px;\n\ + \ height: 21px;\n\ + \}\n\ + \.edge-end-right {\n\ + \ border-top-left-radius: 100% 33px;\n\ + \ border-left: 6px solid #578999;\n\ + \}\n\ + \.edge-guard {\n\ + \ border-color: #69B5A7;\n\ + \}\n\ + \.edge-unify {\n\ + \ border-color: #8CBF7A;\n\ + \}\n\ + \.edge-alt {\n\ + \ height: 1px;\n\ + \ background-color: #aaa;\n\ + \ position: absolute;\n\ + \ margin-top: 19px;\n\ + \ z-index: -1;\n\ + \ padding-right: 22px;\n\ + \}\n\ + \" diff --git a/src/UHC/Util/PrettySimple.hs b/src/UHC/Util/PrettySimple.hs --- a/src/UHC/Util/PrettySimple.hs +++ b/src/UHC/Util/PrettySimple.hs @@ -8,10 +8,11 @@ ( PP_Doc, PP(..) , disp , hPut + , Doc(..) , (>|<), (>-<) , (>#<) - , hlist, vlist, hv + , hlist, hlistReverse, vlist, hv , fill , indent @@ -103,7 +104,7 @@ -- Derived combinators ------------------------------------------------------------------------- -hlist, vlist :: PP a => [a] -> PP_Doc +vlist, hlist, hlistReverse :: PP a => [a] -> PP_Doc -- | PP list horizontally vlist [] = empty vlist as = foldr (>-<) empty as @@ -111,6 +112,10 @@ -- | PP list vertically hlist [] = empty hlist as = foldr (>|<) empty as + +-- | PP list vertically reverse +hlistReverse [] = empty +hlistReverse as = foldr (flip (>|<)) empty as -- | PP list vertically, alias for 'vlist' hv :: PP a => [a] -> PP_Doc diff --git a/uhc-util.cabal b/uhc-util.cabal --- a/uhc-util.cabal +++ b/uhc-util.cabal @@ -1,5 +1,5 @@ Name: uhc-util -Version: 0.1.6.6 +Version: 0.1.6.7 cabal-version: >= 1.6 License: BSD3 Copyright: Utrecht University, Department of Information and Computing Sciences, Software Technology group @@ -49,6 +49,7 @@ UHC.Util.CHR.Solve.TreeTrie.Mono, UHC.Util.CHR.Solve.TreeTrie.MonoBacktrackPrio, UHC.Util.CHR.Solve.TreeTrie.Examples.Term.Main, + UHC.Util.CHR.Solve.TreeTrie.Visualizer, UHC.Util.CHR.GTerm, UHC.Util.CompileRun, UHC.Util.CompileRun2,