Something went wrong. Try again.
Newt - a dependent typed programming language
This is a mirror of the main github repository. newt.cloakedarrow.com
Something went wrong. Try again.
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788899091929394module Data.Graphimport Preludeimport Data.SortedMapimport Data.SnocList-- https://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm#The_algorithm_in_pseudocode-- Based on the wikipedia article, probably could use cleanup. Maybe switch to state monad.record TVertex k where constructor MkTV name : k out : List k index : Int lowLink : Int onStack : Boolrecord TState k where constructor MkTState lastIndex : Int stack : List k result : List (List k) graph : SortedMap k (TVertex k)strongConnect : ∀ k. {{Eq k}} {{Ord k}} → TState k → TVertex k → TState kstrongConnect {k} st vtx = let index' = st.lastIndex + 1 vtx' = MkTV vtx.name vtx.out index' index' True stack' = vtx.name :: st.stack graph' = updateMap vtx'.name vtx' st.graph st' = MkTState index' stack' st.result graph' in checkRoot $ foldl doEdge st' vtx.out where -- There is a lot in here because everything is public at the moment -- Although we do reach for `k` and `vtx.name` a few times min : Int → Int → Int min a b = if a < b then a else b splitComp : List k → List k → (List k × List k) splitComp acc Nil = (acc, Nil) splitComp acc (x :: xs) = if compare x vtx.name == EQ then (x :: acc, xs) else splitComp (x :: acc) xs updateNode : TState k → k → (TVertex k → TVertex k) → TState k updateNode st@(MkTState lastIndex stack result graph) name f = case lookupMap' name graph of Just v => MkTState lastIndex stack result (updateMap name (f v) graph) Nothing => st updateLowLink : TState k → k → Int → TState k updateLowLink st nm v = updateNode st nm $ \ vt => MkTV vt.name vt.out vt.index (min vt.lowLink v) vt.onStack offStack : TState k → k → TState k offStack st name = updateNode st name $ \ vt => MkTV vt.name vt.out vt.index vt.lowLink False doEdge : TState k → k → TState k doEdge st k = let (Just w) = lookupMap' k st.graph | _ => st in if w.onStack then updateLowLink st vtx.name w.index else if w.index == 0 then let st' = strongConnect st w in let (Just w) = lookupMap' k st'.graph | _ => st' in updateLowLink st' vtx.name w.lowLink else st checkRoot : TState k → TState k checkRoot st = let (Just v) = lookupMap' vtx.name st.graph | _ => st in if v.lowLink == v.index then let (comp,stack) = splitComp Nil st.stack in let st = foldl offStack st comp in -- as a variation on tarjan, we only return singletons that point to themselves if length' comp > 1 || elem v.name v.out then MkTState st.lastIndex stack (comp :: st.result) st.graph else MkTState st.lastIndex stack st.result st.graph else st -- leave on stack-- A variant of tarjan that only returns singletons that call themselves-- I'd like to have {{Ord k}} => {{Eq k}} but need to tweak the solver a little-- to ignore ambiguity from indirect solutionstarjan : ∀ k. {{Eq k}} {{Ord k}} → List (k × List k) → List (List k)tarjan {k} nodes = let g = foldMap const emptyMap $ map mkVertex nodes in .result $ foldl checkVertex (MkTState 0 Nil Nil g) $ map fst nodes where mkVertex : k × List k → k × TVertex k mkVertex (n,out) = (n, MkTV n out 0 0 False) checkVertex : TState k → k → TState k checkVertex st k = let (Just vtx) = lookupMap' k st.graph | _ => st in if vtx.index > 0 then st else strongConnect st vtx