Working prototype of unused-reference remover

AgdaUnusedOpens.App/Program.fs

@@ -1,11 +1,41 @@
-open System
+open AgdaUnusedOpens
+open System.IO
 
 [<EntryPoint>]
 let main argv =
-    printfn "Hello World from F#!"
-    0 // return an integer exit code
-
     // TODO - get the complete dependency graph by getting all the agda files
     // Then from the leaves inwards, get all their open statements;
     // try compiling without each one.
-    // Finally write out the file with unnecessary open statements removed.
+    // Finally write out the file with unnecessary open statements removed.
+
+    let agdaRoot = argv.[0]
+    let compiler = argv.[1]
+
+    let config =
+        {
+            AgdaRoot = DirectoryInfo agdaRoot
+            Compiler = FileInfo compiler
+        }
+
+    let everything = FileInfo (Path.Join(agdaRoot, "Everything", "Safe.agda"))
+
+    let graph =
+        match Graph.load config (AgdaFile.makeFromFile everything) with
+        | ParseResult.Success g -> g
+        | ParseResult.Error e -> failwithf "%+A" e
+
+    printfn "Loaded dependency graph."
+
+    graph
+    |> Graph.cata (fun node _ ->
+        if node <> Path.make ["Agda"; "Primitive"] then
+            Path.combine config.AgdaRoot node
+            |> AgdaFile.makeFromFile
+            |> OpenStatement.getAll
+            |> OpenStatement.selectUnused config
+            |> Seq.toList
+            |> OpenStatement.removeAll
+            |> Option.map (AgdaFile.flush config.AgdaRoot)
+            |> ignore<unit option>)
+
+    0

AgdaUnusedOpens.Test/AgdaUnusedOpens.Test.fsproj

@@ -4,7 +4,6 @@
         <TargetFramework>netcoreapp3.0</TargetFramework>
 
         <IsPackable>false</IsPackable>
-        <GenerateProgramFile>false</GenerateProgramFile>
     </PropertyGroup>
 
     <ItemGroup>

AgdaUnusedOpens.Test/TestGraph.fs

@@ -4,6 +4,8 @@ open NUnit.Framework
 open FsUnitTyped
 
 open AgdaUnusedOpens
+open AgdaUnusedOpens.Types
+open AgdaUnusedOpens.Internals
 
 [<TestFixture>]
 module TestGraph =
@@ -12,9 +14,9 @@ module TestGraph =
         let g =
             "Example.dot"
             |> Utils.getResource
-            |> Graph.parse
+            |> AdjacencyList.parse
         match g with
-        | Success (Graph g) ->
+        | Ok (AdjacencyList g) ->
             let m0 = Path.make ["Sequences"]
             let m1 = Path.make ["Setoids" ; "Setoids"]
             let m2 = Path.make ["LogicalFormulae"]
@@ -44,3 +46,104 @@ module TestGraph =
                 |> Set.ofList
             actual |> shouldEqual expected
         | x -> failwithf "oh no: %O" x
+
+    [<Test>]
+    let ``Convert to a graph`` () =
+        let g = "Example.dot" |> Utils.getResource |> AdjacencyList.parse
+        let g = match g with | Error _ -> failwith "oh no" | Ok g -> g
+        let i = Graph.toGraph g
+        let m0 = Path.make ["Sequences"]
+        let m1 = Path.make ["Setoids" ; "Setoids"]
+        let m2 = Path.make ["LogicalFormulae"]
+        let m3 = Path.make ["Agda" ; "Primitive"]
+        let m4 = Path.make ["Functions"]
+        let m5 = Path.make ["Sets" ; "EquivalenceRelations"]
+        let m6 = Path.make ["Numbers" ; "Naturals" ; "Definition"]
+
+        let primitive =
+            {
+                Node = m3
+                Unblocks = Set.empty
+            }
+        let logical =
+            {
+                Node = m2
+                Unblocks = Set.singleton primitive
+            }
+        let functions =
+            {
+                Node = m4
+                Unblocks =
+                    [
+                        logical
+                        primitive
+                    ]
+                    |> Set.ofList
+            }
+        let numbers =
+            {
+                Node = m6
+                Unblocks = Set.singleton logical
+            }
+        let equivRel =
+            {
+                Node = m5
+                Unblocks =
+                    [
+                        functions
+                        primitive
+                        logical
+                    ]
+                    |> Set.ofList
+            }
+        let setoids =
+            {
+                Node = m1
+                Unblocks =
+                    [
+                        equivRel
+                        logical
+                        functions
+                        primitive
+                    ]
+                    |> Set.ofList
+            }
+        let sequences =
+            {
+                Node = m0
+                Unblocks =
+                    [
+                        numbers
+                        setoids
+                        logical
+                    ]
+                    |> Set.ofList
+            }
+
+        i
+        |> shouldEqual sequences
+
+    [<Test>]
+    let ``Cata traversal order`` () =
+        let g = "Example.dot" |> Utils.getResource |> AdjacencyList.parse
+        let g = match g with | Error _ -> failwith "oh no" | Ok g -> g
+        let i = Graph.toGraph g
+
+        let nodes = ResizeArray<Path> ()
+
+        i
+        |> Graph.cata (fun p _ -> nodes.Add p)
+
+        nodes
+        |> Seq.toList
+        |> List.map Path.toString
+        |> shouldEqual
+            [
+                "Agda.Primitive"
+                "LogicalFormulae"
+                "Numbers.Naturals.Definition"
+                "Functions"
+                "Sets.EquivalenceRelations"
+                "Setoids.Setoids"
+                "Sequences"
+            ]

AgdaUnusedOpens/AdjacencyList.fs

@@ -0,0 +1,61 @@
+namespace AgdaUnusedOpens.Internals
+
+open System.Text.RegularExpressions
+open AgdaUnusedOpens
+open AgdaUnusedOpens.Types
+
+type Arrow =
+    {
+        From : Path
+        To : Path
+    }
+
+type internal AdjacencyList = AdjacencyList of Arrow list
+
+[<RequireQualifiedAccess>]
+module AdjacencyList =
+
+    /// Given the contents of a dotfile, parse it.
+    let internal parse (dot : string) : Result<AdjacencyList, string> =
+        let dot = dot.Trim ()
+        if not <| dot.StartsWith "digraph dependencies {" then
+            Error <| sprintf "Unexpected start of string: %s" dot
+        else
+        if not <| dot.EndsWith "}" then
+            Error (sprintf "File did not end with a }: %s." dot)
+        else
+        let dot = dot.Substring(String.length "digraph dependencies {").TrimStart ()
+        let dot = dot.Remove(String.length dot - 1).TrimEnd ()
+        let lines = dot.Split ';' |> Array.map (fun i -> i.Trim ())
+        let nodeDef, arrowDef =
+            lines
+            |> List.ofArray
+            |> List.fold (fun (nD : string list, aD : string list) i ->
+                if i.Contains "]" then (i :: nD, aD) elif i.Contains " -> " then (nD, i :: aD) else (nD, aD)) ([], [])
+        let nodeRegex = Regex @"(.+)\[label=""(.+)""\]"
+        let arrowRegex = Regex @"(.+) -> (.+)"
+        let nodes : Map<string, Path> =
+            nodeDef
+            |> List.fold (fun m i ->
+                let matches = nodeRegex.Match i
+                let label = matches.Groups.[1].Value
+                let name =
+                    matches.Groups.[2].Value.Split('.')
+                    |> List.ofArray
+                    |> Path.make
+                Map.add label name m) Map.empty
+        let arrows : (string * string) list =
+            arrowDef
+            |> List.map (fun i ->
+                let matches = arrowRegex.Match i
+                matches.Groups.[1].Value, matches.Groups.[2].Value)
+
+        arrows
+        |> List.map (fun (from, to') ->
+            {
+                From = Map.find from nodes
+                To = Map.find to' nodes
+            })
+        |> AdjacencyList
+        |> Ok
+

AgdaUnusedOpens/AgdaFile.fs

@@ -7,6 +7,7 @@ open AgdaUnusedOpens.Types
 
 [<RequireQualifiedAccess>]
 module Path =
+
     let fold<'s> (f : 's -> string -> 's) (initial : 's) (p : Path) : 's =
         p.Tail
         |> List.fold f (f initial p.Head)
@@ -68,6 +69,12 @@ module AgdaFile =
             ModuleLine = moduleLineNo
         }
 
+    let makeFromFile (f : FileInfo) : AgdaFile =
+        f.FullName
+        |> File.ReadAllLines
+        |> List.ofArray
+        |> make
+
     let flush (agdaRoot : DirectoryInfo) (f : AgdaFile) : unit =
         let location = Path.combine agdaRoot f.Path
         File.WriteAllLines (location.FullName, f.Contents)

AgdaUnusedOpens/AgdaUnusedOpens.fsproj

@@ -10,6 +10,7 @@
         <Compile Include="Types.fs" />
         <Compile Include="AgdaFile.fs" />
         <Compile Include="AgdaCompiler.fs" />
+        <Compile Include="AdjacencyList.fs" />
         <Compile Include="Graph.fs" />
         <Compile Include="OpenStatement.fs" />
     </ItemGroup>

AgdaUnusedOpens/Graph.fs

@@ -1,77 +1,162 @@
 namespace AgdaUnusedOpens
 
+open System.Collections.Generic
 open System.Diagnostics
 open System.IO
-open System.Text.RegularExpressions
 open AgdaUnusedOpens.Types
+open AgdaUnusedOpens.Internals
 
-type Arrow =
+type Graph =
     {
-        From : Path
-        To : Path
+        Node : Path
+        Unblocks : Graph Set
     }
 
-type Graph = Graph of Arrow list
+type ParseError =
+    | NotDotFile of Path * string
+    | FailedToCompile of Path
 
+[<RequireQualifiedAccess>]
 type ParseResult =
-    | NotDotFile of string
+    | Error of ParseError list
     | Success of Graph
 
 [<RequireQualifiedAccess>]
 module Graph =
 
-    /// Given the contents of a dotfile, parse it.
-    let parse (dot : string) : ParseResult =
-        let dot = dot.Trim ()
-        if not <| dot.StartsWith "digraph dependencies {" then
-            NotDotFile <| sprintf "Unexpected start of string: %s" dot
-        else
-        if not <| dot.EndsWith "}" then
-            NotDotFile (sprintf "File did not end with a }: %s." dot)
-        else
-        let dot = dot.Substring(String.length "digraph dependencies {").TrimStart ()
-        let dot = dot.Remove(String.length dot - 1).TrimEnd ()
-        let lines = dot.Split ';' |> Array.map (fun i -> i.Trim ())
-        let nodeDef, arrowDef =
-            lines
-            |> List.ofArray
-            |> List.fold (fun (nD : string list, aD : string list) i ->
-                if i.Contains "]" then (i :: nD, aD) elif i.Contains " -> " then (nD, i :: aD) else (nD, aD)) ([], [])
-        let nodeRegex = Regex @"(.+)\[label=""(.+)""\]"
-        let arrowRegex = Regex @"(.+) -> (.+)"
-        let nodes : Map<string, Path> =
-            nodeDef
-            |> List.fold (fun m i ->
-                let matches = nodeRegex.Match i
-                let label = matches.Groups.[1].Value
-                let name =
-                    matches.Groups.[2].Value.Split('.')
-                    |> List.ofArray
-                    |> Path.make
-                Map.add label name m) Map.empty
-        let arrows : List<string * string> =
-            arrowDef
-            |> List.map (fun i ->
-                let matches = arrowRegex.Match i
-                matches.Groups.[1].Value, matches.Groups.[2].Value)
+    /// A graph that is under construction.
+    type private Construct =
+        {
+            /// The label of this node.
+            Node : Path
+            /// The outgoing edges, together with the nodes at their ends
+            To : Map<Path, Construct>
 
-        arrows
-        |> List.map (fun (from, to') ->
-            {
-                From = Map.find from nodes
-                To = Map.find to' nodes
-            })
-        |> Graph
-        |> Success
+            HasIncoming : bool ref
+        }
+
+    /// A map of path to which constructed graph that path is the root of.
+    type private Constructing = Constructing of Map<Path, Construct>
+
+    let private addEdge (from : Path) (toNode : Path) (Constructing constructing) =
+        let imageNode, constructing =
+            match Map.tryFind toNode constructing with
+            | None ->
+                let node =
+                    { Node = toNode ; To = Map.empty ; HasIncoming = ref true }
+                node, constructing |> Map.add toNode node
+            | Some node ->
+                node.HasIncoming := true
+                node, constructing
+        match Map.tryFind from constructing with
+        | None ->
+            constructing
+            |> Map.add from { Node = from ; To = Map.empty |> Map.add toNode imageNode ; HasIncoming = ref false }
+        | Some existingGraph ->
+            let newFrom = { existingGraph with To = existingGraph.To |> Map.add toNode imageNode }
+
+            constructing
+            |> Map.add from newFrom
+        |> Constructing
+
+    let private addEdges (from : Path) (toNode : Path Set) (constructing : Constructing) =
+        if Path.toString from = "Setoids.Setoids" then
+            ()
+        match Set.toList toNode with
+        | [] ->
+            let (Constructing c) = constructing
+            match Map.tryFind from c with
+            | None ->
+                c
+                |> Map.add from { Node = from ; To = Map.empty ; HasIncoming = ref false }
+            | Some _ -> c
+            |> Constructing
+        | l ->
+            l
+            |> List.fold (fun state s -> addEdge from s state) constructing
+
+    let private concretise (Constructing overallConstruction) : Graph =
+        let memo = Dictionary<Path, Graph> ()
+        let rec go (c : Construct) : Graph =
+            match memo.TryGetValue c.Node with
+            | true, v -> v
+            | false, _ ->
+                let u =
+                    {
+                        Node = c.Node
+                        Unblocks =
+                            c.To
+                            |> Seq.map (fun kvp -> Map.find kvp.Key overallConstruction)
+                            |> Seq.map go
+                            |> Set.ofSeq
+                    }
+                memo.Add (c.Node, u)
+                u
+
+        let topNode =
+            overallConstruction
+            |> Map.toSeq
+            |> Seq.map snd
+            |> Seq.filter (fun v -> v.HasIncoming.Value = false)
+            |> Seq.toList
+        match topNode with
+        | [] -> failwith "Circular dependency detected"
+        | x :: y :: _ -> failwithf "Multiple nodes are at the root! %i many, at least '%s', '%s' (%+A)" (List.length topNode) (Path.toString x.Node) (Path.toString y.Node) (topNode |> List.map (fun i -> Path.toString i.Node))
+        | [v] ->
+            go v
+
+    let internal toGraph (AdjacencyList g) : Graph =
+        // If there are no outgoing nodes, the node will not appear as a key in this map.
+        let reduced : Map<Path, Path Set> =
+            g
+            |> List.fold (fun m { From = from ; To = toPath } ->
+                match Map.tryFind from m with
+                | Some xs -> Map.add from (Set.add toPath xs) m
+                | None -> Map.add from (Set.singleton toPath) m
+                ) Map.empty
+
+        let constructed =
+            reduced
+            |> Map.fold (fun inConstruction from toPaths ->
+                addEdges from toPaths inConstruction
+                ) (Constructing Map.empty)
+
+        constructed
+        |> concretise
+
+    let parse (dot : string) : Result<Graph, string> =
+        AdjacencyList.parse dot
+        |> Result.map toGraph
 
     let load (agda : AgdaCompiler) (f : AgdaFile) : ParseResult =
         let tmp = Path.GetTempFileName ()
         use proc = new Process ()
         proc.StartInfo.FileName <- agda.Compiler.FullName
+        proc.StartInfo.WorkingDirectory <- agda.AgdaRoot.FullName
         proc.StartInfo.Arguments <- sprintf "%s --dependency-graph=%s" (Path.combine agda.AgdaRoot f.Path).FullName tmp
         let res = proc.Start ()
         assert (res = true)
         proc.WaitForExit ()
-        tmp
-        |> File.ReadAllText
-        |> parse
+        if proc.ExitCode = 0 then
+            match tmp |> File.ReadAllText |> parse with
+            | Ok g -> ParseResult.Success g
+            | Error err -> ParseResult.Error (ParseError.NotDotFile (f.Path, err) |> List.singleton)
+        else
+            ParseResult.Error (ParseError.FailedToCompile f.Path |> List.singleton)
+
+    let cata<'a> (f : Path -> 'a list -> 'a) (g : Graph) : 'a =
+        let store = Dictionary<Path, 'a> ()
+
+        let rec go (g : Graph) =
+            match store.TryGetValue g.Node with
+            | false, _ ->
+                let u =
+                    g.Unblocks
+                    |> Set.toList
+                    |> List.map go
+                    |> f g.Node
+                store.Add (g.Node, u)
+                u
+            | true, v -> v
+
+        go g

AgdaUnusedOpens/OpenStatement.fs

@@ -10,13 +10,17 @@ type OpenStatement =
 
 [<RequireQualifiedAccess>]
 module OpenStatement =
-    let get (file : AgdaFile) : OpenStatement list =
+    let getAll (file : AgdaFile) : OpenStatement list =
         file.Contents
         |> List.indexed
         |> List.choose (fun (i, line) -> if line.TrimStart().StartsWith("open import ") then Some i else None)
         |> List.map (fun i -> { File = file ; LineNumber = i })
 
-    let remove (f : AgdaFile) (s : OpenStatement) : AgdaFile =
+    /// Private version allowing us to remove multiple open statements from a file.
+    /// This is unsafe in general - make sure removing lines from the right files,
+    /// and you're not doing it in a bad order (e.g. removing the first line and thereby
+    /// causing all the other lines to bump up one before you remove a later line)!
+    let private remove' (f : AgdaFile) (s : OpenStatement) : AgdaFile =
         {
             Path = f.Path
             Contents = f.Contents |> Seq.omit s.LineNumber |> Seq.toList
@@ -26,3 +30,31 @@ module OpenStatement =
                 else f.ModuleLine - 1
         }
 
+    let remove (s : OpenStatement) : AgdaFile =
+        remove' s.File s
+
+    /// Returns None iff there were no elements in the list.
+    /// Throws if the open statements are not all from the same file.
+    let removeAll (s : OpenStatement list) : AgdaFile option =
+        match s with
+        | [] -> None
+        | x :: xs ->
+            xs
+            |> List.sortBy (fun i -> -i.LineNumber)
+            |> List.fold (fun (currFile : AgdaFile) newToRemove ->
+                if newToRemove.File.Path <> currFile.Path then
+                    failwithf
+                        "Attempted to remove open statement in %s from file %s"
+                        (Path.toString newToRemove.File.Path)
+                        (Path.toString currFile.Path)
+                remove' currFile newToRemove) (remove x)
+            |> Some
+
+    let rec selectUnused (config : AgdaCompiler) (opens : OpenStatement list) : OpenStatement seq =
+        seq {
+            for o in opens do
+                let f = remove o
+                if AgdaCompiler.compiles config f then
+                    yield o
+        }
+

AgdaUnusedOpens/Types.fs

@@ -6,4 +6,3 @@ type Path =
             Head : string
             Tail : string list
         }
-