mirror of
https://github.com/idris-lang/Idris2.git
synced 2025-01-01 16:12:26 +03:00
[ cleanup ] Reuse Tarjan's algorithm in JS backend and some other cleanups (#1504)
This commit is contained in:
Stefan Höck
GitHub
parent
41c3fd2632
commit
c04835c436
@ -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,
|
||||
|
||||
@ -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
|
||||
|
||||
|
||||
@ -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
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
92
src/Libraries/Data/Graph.idr
Normal file
92
src/Libraries/Data/Graph.idr
Normal file
@ -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
|
||||
Loading…
Reference in New Issue
Block a user