diff --git a/idris2api.ipkg b/idris2api.ipkg index d835ce258..aa9427f71 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -21,7 +21,6 @@ modules = Compiler.ES.ImperativeAst, Compiler.ES.Javascript, Compiler.ES.Node, - Compiler.ES.RemoveUnused, Compiler.ES.TailRec, Compiler.RefC.CC, @@ -117,6 +116,7 @@ modules = Libraries.Data.ANameMap, Libraries.Data.DList, Libraries.Data.Fin, + Libraries.Data.Graph, Libraries.Data.IMaybe, Libraries.Data.IntMap, Libraries.Data.IOMatrix, diff --git a/src/Compiler/ES/Imperative.idr b/src/Compiler/ES/Imperative.idr index 4fb718e4f..28844e895 100644 --- a/src/Compiler/ES/Imperative.idr +++ b/src/Compiler/ES/Imperative.idr @@ -14,7 +14,6 @@ import Compiler.CompileExpr import public Core.Context -import Compiler.ES.RemoveUnused import Compiler.ES.TailRec %default covering @@ -411,7 +410,7 @@ compileToImperative c tm = -- list of toplevel definitions (only those necessary -- to implement the main expression) - lst_defs <- traverse getImp (defsUsedByNamedCExp ctm ndefs) + lst_defs <- traverse getImp ndefs let defs = concat lst_defs diff --git a/src/Compiler/ES/RemoveUnused.idr b/src/Compiler/ES/RemoveUnused.idr deleted file mode 100644 index 1b8b3a111..000000000 --- a/src/Compiler/ES/RemoveUnused.idr +++ /dev/null @@ -1,94 +0,0 @@ -||| Functions in this module are responsible to -||| find those toplevel definitions that should -||| be included in the generated JS code since -||| they are (transitively) being invoked by the -||| main function. -module Compiler.ES.RemoveUnused - -import Libraries.Data.SortedSet -import Libraries.Data.SortedMap -import Data.Vect -import Data.List - -import Core.CompileExpr -import Core.Name -import Core.FC - -import Debug.Trace - -%default covering - -mutual - usedNames : NamedCExp -> SortedSet Name - usedNames (NmLocal fc n) = empty - usedNames (NmRef fc n) = insert n empty - usedNames (NmLam fc n e) = usedNames e - usedNames (NmApp fc x args) = usedNames x `union` concatMap usedNames args - usedNames (NmPrimVal fc c) = empty - usedNames (NmOp fc op args) = concatMap usedNames args - usedNames (NmConCase fc sc alts def) = - (usedNames sc `union` concatMap usedNamesConAlt alts) `union` - maybe empty usedNames def - usedNames (NmConstCase fc sc alts def) = - (usedNames sc `union` concatMap usedNamesConstAlt alts) - `union` maybe empty usedNames def - usedNames (NmExtPrim fc p args) = concatMap usedNames args - usedNames (NmCon fc x _ t args) = concatMap usedNames args - usedNames (NmDelay fc _ t) = usedNames t - usedNames (NmForce fc _ t) = usedNames t - usedNames (NmLet fc x val sc) = usedNames val `union` usedNames sc - usedNames (NmErased fc) = empty - usedNames (NmCrash fc msg) = empty - - usedNamesConAlt : NamedConAlt -> SortedSet Name - usedNamesConAlt (MkNConAlt n _ t args exp) = usedNames exp - - usedNamesConstAlt : NamedConstAlt -> SortedSet Name - usedNamesConstAlt (MkNConstAlt c exp) = usedNames exp - -usedNamesDef : NamedDef -> SortedSet Name -usedNamesDef (MkNmFun args exp) = usedNames exp -usedNamesDef (MkNmError exp) = usedNames exp -usedNamesDef (MkNmForeign cs args ret) = empty -usedNamesDef (MkNmCon _ _ _) = empty - -defsToUsedMap : List (Name, FC, NamedDef) - -> SortedMap Name (SortedSet Name) -defsToUsedMap defs = - fromList $ (\(n,_,d)=> (n, usedNamesDef d)) <$> defs - --- TODO: Should we use `SortedSet Name` instead of `List Name` here? -calcUsed : SortedSet Name - -> SortedMap Name (SortedSet Name) - -> List Name - -> SortedSet Name -calcUsed done d [] = done -calcUsed done d xs = - let used_in_xs = foldl f empty $ (\z => lookup z d) <$> xs - new_done = union done (fromList xs) - in calcUsed (new_done) d (SortedSet.toList $ difference used_in_xs new_done) - where - f : SortedSet Name -> Maybe (SortedSet Name) -> SortedSet Name - f x Nothing = x - f x (Just y) = union x y - -calcUsedDefs : List Name - -> List (Name, FC, NamedDef) - -> List (Name, FC, NamedDef) -calcUsedDefs names defs = - let usedNames = calcUsed empty (defsToUsedMap defs) names - in List.filter (\(n, fc, d) => contains n usedNames) defs - -||| Filters a list of toplevel definitions, keeping only those -||| that are (transitively) used by the given expression. -||| -||| @ exp : Expression invoking some of the toplevel -||| definitions. Typically, this is the expression implementing -||| a program's `main` function. -||| @ defs : List of toplevel definitions. -export -defsUsedByNamedCExp : (exp : NamedCExp) - -> (defs : List (Name, FC, NamedDef)) - -> List (Name, FC, NamedDef) -defsUsedByNamedCExp exp defs = - calcUsedDefs (SortedSet.toList $ usedNames exp) defs diff --git a/src/Compiler/ES/TailRec.idr b/src/Compiler/ES/TailRec.idr index a6d410009..815450fa3 100644 --- a/src/Compiler/ES/TailRec.idr +++ b/src/Compiler/ES/TailRec.idr @@ -84,6 +84,8 @@ import Data.Maybe import Data.List import Data.List1 import Data.Strings +import Libraries.Data.Graph +import Libraries.Data.SortedSet import Libraries.Data.List.Extra as L import Libraries.Data.SortedSet import Libraries.Data.SortedMap @@ -179,105 +181,33 @@ makeTailOptimToBody n argNames body = (Just loopReturn) in stepFn <+> createArgInit argNames <+> loop -||| A directed graph mapping function names -||| to the set of names they directly call and -||| to the set of names from which they are directly called -record CallGraph where - constructor MkCallGraph - ||| Map function names to function names they call - calls : SortedMap Name (SortedSet Name) - ||| Map function names to function names, from which they are called - callers : SortedMap Name (SortedSet Name) - -showCallGraph : CallGraph -> String -showCallGraph x = - let calls = unlines $ map - (\(x,y) => show x ++ ": " ++ show (SortedSet.toList y)) - (SortedMap.toList x.calls) - callers = unlines $ map - (\(x,y) => show x ++ ": " ++ show (SortedSet.toList y)) - (SortedMap.toList x.callers) - in calls ++ "\n----\n" ++ callers - -- when creating the tail call graph, we only process -- function declarations and we are only interested -- in calls being made at tail position -tailCallGraph : ImperativeStatement -> CallGraph +tailCallGraph : ImperativeStatement -> SortedMap Name (SortedSet Name) tailCallGraph (SeqStatement x y) = - let xg = tailCallGraph x - yg = tailCallGraph y - in MkCallGraph - (mergeWith union xg.calls yg.calls) - (mergeWith union xg.callers yg.callers) + mergeWith union (tailCallGraph x) (tailCallGraph y) tailCallGraph (FunDecl fc n args body) = - let calls = allTailCalls body - in MkCallGraph (singleton n calls) (toSortedMap calls $> singleton n) + singleton n $ allTailCalls body -tailCallGraph _ = MkCallGraph empty empty +tailCallGraph _ = empty -- lookup up the list of values associated with -- a given key (`Nil` if the key is not present in the list) lookupList : k -> SortedMap k (SortedSet b) -> List b lookupList v = maybe [] SortedSet.toList . lookup v --- look up the nodes transitively called from --- the given list of callers. already visited nodes --- (as indicated by `visited`) are ignored --- --- For the resulting list, the following post-condition holds: --- if x is callable from y, then y will appear before x in the list. -kosarajuL : (visited : SortedSet Name) - -> (callers : List Name) - -> (graph : CallGraph) - -> (SortedSet Name, List Name) -kosarajuL visited [] graph = (visited, []) -kosarajuL visited (x::xs) graph = - if contains x visited - then kosarajuL visited xs graph - else let outNeighbours = lookupList x (graph.calls) - (visited2, l2) = kosarajuL (insert x visited) outNeighbours graph - (visited3, l3) = kosarajuL visited2 xs graph - in (visited3, l3 ++ (x :: l2)) - -kosarajuAssign : CallGraph - -> (root : Name) - -> SortedMap Name Name - -> (u : Name) - -> SortedMap Name Name -kosarajuAssign graph root s u = - case lookup u s of - Just _ => s - Nothing => - let inNeighbours = lookupList u (graph.callers) - in foldl (kosarajuAssign graph root) (insert u root s) inNeighbours - --- associates every caller in a call graph with --- an arbitrary root node of its strongly connected --- component. --- --- This allows us to find the strongly connected components --- of a tail-call graph, by grouping nodes by their --- assigned root node. --- --- See https://en.wikipedia.org/wiki/Kosaraju%27s_algorithm -kosaraju : CallGraph -> SortedMap Name Name -kosaraju graph = - let l = snd $ kosarajuL empty (keys $ graph.calls) graph - in foldl (\acc, elem => kosarajuAssign graph elem acc elem) empty l - -recursiveTailCallGroups : CallGraph -> List (List Name) +recursiveTailCallGroups : SortedMap Name (SortedSet Name) -> List (List Name) recursiveTailCallGroups graph = - let roots = kosaraju graph - groups = map (map fst) . L.groupAllWith snd $ toList roots - in [forget x | x<-groups, hasTailCalls x] + [forget x | x <-tarjan graph, hasTailCalls x] -- in case of larger groups (more than one element) -- the group contains tailcalls by construction. In case -- of a single function, we need to check that at least one -- outgoing tailcall goes back to the function itself. where hasTailCalls : List1 Name -> Bool - hasTailCalls (x ::: Nil) = x `elem` lookupList x (graph.calls) + hasTailCalls (x ::: Nil) = x `elem` lookupList x graph hasTailCalls _ = True -- extracts the functions belonging to the given tailcall @@ -367,8 +297,7 @@ export tailRecOptim : ImperativeStatement -> Core ImperativeStatement tailRecOptim x = do ref <- newRef TailRecS (MkTailSt 0) - let graph = tailCallGraph x - let groups = recursiveTailCallGroups graph + let groups = recursiveTailCallGroups (tailCallGraph x) let functionsToOptimize = foldl SortedSet.union empty $ map SortedSet.fromList groups let (unchanged, defs) = extractFunctions functionsToOptimize x optimized <- traverse (tailRecOptimGroup defs) groups diff --git a/src/Compiler/Separate.idr b/src/Compiler/Separate.idr index 89c291539..bf27378aa 100644 --- a/src/Compiler/Separate.idr +++ b/src/Compiler/Separate.idr @@ -5,6 +5,7 @@ import public Core.Name import public Core.Name.Namespace import public Core.CompileExpr import public Compiler.VMCode +import public Libraries.Data.Graph import public Libraries.Data.SortedMap import public Libraries.Data.SortedSet import public Libraries.Data.StringMap @@ -83,99 +84,6 @@ splitByNS = SortedMap.toList . foldl addOne SortedMap.empty (SortedMap.singleton (getNS n) [ndef]) nss --- Mechanically transcribed from --- https://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm#The_algorithm_in_pseudocode -namespace Tarjan - private - record TarjanVertex where - constructor TV - index : Int - lowlink : Int - inStack : Bool - - private - record TarjanState cuid where - constructor TS - vertices : SortedMap cuid TarjanVertex - stack : List cuid - nextIndex : Int - components : List (List1 cuid) - impossibleHappened : Bool -- we should get at least some indication of broken assumptions - - ||| Find strongly connected components in the given graph. - ||| - ||| Input: map from vertex X to all vertices Y such that there is edge X->Y - ||| Output: list of strongly connected components, ordered by output degree descending - export - tarjan : Ord cuid => SortedMap cuid (SortedSet cuid) -> List (List1 cuid) - tarjan {cuid} deps = loop initialState (SortedMap.keys deps) - where - initialState : TarjanState cuid - initialState = - TS - SortedMap.empty - [] - 0 - [] - False - - strongConnect : TarjanState cuid -> cuid -> TarjanState cuid - strongConnect ts v = - let ts'' = case SortedMap.lookup v deps of - Nothing => ts' -- no edges - Just edgeSet => loop ts' (SortedSet.toList edgeSet) - in case SortedMap.lookup v ts''.vertices of - Nothing => record { impossibleHappened = True } ts'' - Just vtv => - if vtv.index == vtv.lowlink - then createComponent ts'' v [] - else ts'' - where - createComponent : TarjanState cuid -> cuid -> List cuid -> TarjanState cuid - createComponent ts v acc = - case ts.stack of - [] => record { impossibleHappened = True } ts - w :: ws => - let ts' : TarjanState cuid = record { - vertices $= SortedMap.adjust w record{ inStack = False }, - stack = ws - } ts - in if w == v - then record { components $= ((v ::: acc) ::) } ts' -- that's it - else createComponent ts' v (w :: acc) - - loop : TarjanState cuid -> List cuid -> TarjanState cuid - loop ts [] = ts - loop ts (w :: ws) = - loop ( - case SortedMap.lookup w ts.vertices of - Nothing => let ts' = strongConnect ts w in - case SortedMap.lookup w ts'.vertices of - Nothing => record { impossibleHappened = True } ts' - Just wtv => record { vertices $= SortedMap.adjust v record{ lowlink $= min wtv.lowlink } } ts' - - Just wtv => case wtv.inStack of - False => ts -- nothing to do - True => record { vertices $= SortedMap.adjust v record{ lowlink $= min wtv.index } } ts - ) ws - - ts' : TarjanState cuid - ts' = record { - vertices $= SortedMap.insert v (TV ts.nextIndex ts.nextIndex True), - stack $= (v ::), - nextIndex $= (1+) - } ts - - loop : TarjanState cuid -> List cuid -> List (List1 cuid) - loop ts [] = - if ts.impossibleHappened - then [] - else ts.components - loop ts (v :: vs) = - case SortedMap.lookup v ts.vertices of - Just _ => loop ts vs -- done, skip - Nothing => loop (strongConnect ts v) vs - public export interface HasNamespaces a where ||| Return the set of namespaces mentioned within diff --git a/src/Libraries/Data/Graph.idr b/src/Libraries/Data/Graph.idr new file mode 100644 index 000000000..f6fc831f3 --- /dev/null +++ b/src/Libraries/Data/Graph.idr @@ -0,0 +1,92 @@ +module Libraries.Data.Graph + +import Libraries.Data.SortedMap +import Libraries.Data.SortedSet + +import Data.List1 + +-- Mechanically transcribed from +-- https://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm#The_algorithm_in_pseudocode +private +record TarjanVertex where + constructor TV + index : Int + lowlink : Int + inStack : Bool + +private +record TarjanState cuid where + constructor TS + vertices : SortedMap cuid TarjanVertex + stack : List cuid + nextIndex : Int + components : List (List1 cuid) + impossibleHappened : Bool -- we should get at least some indication of broken assumptions + +initial : Ord cuid => TarjanState cuid +initial = TS empty [] 0 [] False + +||| Find strongly connected components in the given graph. +||| +||| Input: map from vertex X to all vertices Y such that there is edge X->Y +||| Output: list of strongly connected components, ordered by output degree descending +export +tarjan : Ord cuid => SortedMap cuid (SortedSet cuid) -> List (List1 cuid) +tarjan {cuid} deps = loop initial (SortedMap.keys deps) + where + strongConnect : TarjanState cuid -> cuid -> TarjanState cuid + strongConnect ts v = + let ts'' = case SortedMap.lookup v deps of + Nothing => ts' -- no edges + Just edgeSet => loop ts' (SortedSet.toList edgeSet) + in case SortedMap.lookup v ts''.vertices of + Nothing => record { impossibleHappened = True } ts'' + Just vtv => + if vtv.index == vtv.lowlink + then createComponent ts'' v [] + else ts'' + where + createComponent : TarjanState cuid -> cuid -> List cuid -> TarjanState cuid + createComponent ts v acc = + case ts.stack of + [] => record { impossibleHappened = True } ts + w :: ws => + let ts' : TarjanState cuid = record { + vertices $= SortedMap.adjust w record{ inStack = False }, + stack = ws + } ts + in if w == v + then record { components $= ((v ::: acc) ::) } ts' -- that's it + else createComponent ts' v (w :: acc) + + loop : TarjanState cuid -> List cuid -> TarjanState cuid + loop ts [] = ts + loop ts (w :: ws) = + loop ( + case SortedMap.lookup w ts.vertices of + Nothing => let ts' = strongConnect ts w in + case SortedMap.lookup w ts'.vertices of + Nothing => record { impossibleHappened = True } ts' + Just wtv => record { vertices $= SortedMap.adjust v record{ lowlink $= min wtv.lowlink } } ts' + + Just wtv => case wtv.inStack of + False => ts -- nothing to do + True => record { vertices $= SortedMap.adjust v record{ lowlink $= min wtv.index } } ts + ) ws + + ts' : TarjanState cuid + ts' = record { + vertices $= SortedMap.insert v (TV ts.nextIndex ts.nextIndex True), + stack $= (v ::), + nextIndex $= (1+) + } ts + + loop : TarjanState cuid -> List cuid -> List (List1 cuid) + loop ts [] = + if ts.impossibleHappened + then [] + else ts.components + loop ts (v :: vs) = + case SortedMap.lookup v ts.vertices of + Just _ => loop ts vs -- done, skip + Nothing => loop (strongConnect ts v) vs