Initial commit of the bones of an unused-open-removing Agda tool

.gitignore

@@ -0,0 +1,3 @@
+bin/
+obj/
+/packages/

.idea/.idea.AgdaUnusedOpens/.idea/.gitignore

@@ -0,0 +1,2 @@
+# Default ignored files
+/workspace.xml

.idea/.idea.AgdaUnusedOpens/.idea/indexLayout.xml

@@ -0,0 +1,8 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project version="4">
+  <component name="ContentModelUserStore">
+    <attachedFolders />
+    <explicitIncludes />
+    <explicitExcludes />
+  </component>
+</project>

.idea/.idea.AgdaUnusedOpens/.idea/projectSettingsUpdater.xml

@@ -0,0 +1,6 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project version="4">
+  <component name="RiderProjectSettingsUpdater">
+    <option name="vcsConfiguration" value="1" />
+  </component>
+</project>

AgdaUnusedOpens.App/AgdaUnusedOpens.App.fsproj

@@ -0,0 +1,17 @@
+<Project Sdk="Microsoft.NET.Sdk">
+
+    <PropertyGroup>
+        <OutputType>Exe</OutputType>
+        <TargetFramework>netcoreapp3.0</TargetFramework>
+        <RootNamespace>AgdaUnusedOpens</RootNamespace>
+    </PropertyGroup>
+
+    <ItemGroup>
+        <Compile Include="Program.fs" />
+    </ItemGroup>
+
+    <ItemGroup>
+      <ProjectReference Include="..\AgdaUnusedOpens\AgdaUnusedOpens.fsproj" />
+    </ItemGroup>
+
+</Project>

AgdaUnusedOpens.App/Program.fs

@@ -0,0 +1,11 @@
+open System
+
+[<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.

AgdaUnusedOpens.Test/AgdaUnusedOpens.Test.fsproj

@@ -0,0 +1,31 @@
+<Project Sdk="Microsoft.NET.Sdk">
+
+    <PropertyGroup>
+        <TargetFramework>netcoreapp3.0</TargetFramework>
+
+        <IsPackable>false</IsPackable>
+        <GenerateProgramFile>false</GenerateProgramFile>
+    </PropertyGroup>
+
+    <ItemGroup>
+        <PackageReference Include="FsUnit" Version="3.8.0" />
+        <PackageReference Include="nunit" Version="3.12.0" />
+        <PackageReference Include="NUnit3TestAdapter" Version="3.13.0" />
+        <PackageReference Include="Microsoft.NET.Test.Sdk" Version="16.2.0" />
+        <PackageReference Include="FsCheck" Version="2.14.0" />
+    </ItemGroup>
+
+    <ItemGroup>
+        <Compile Include="Utils.fs" />
+        <Compile Include="TestSeq.fs" />
+        <Compile Include="TestGraph.fs" />
+        <Compile Include="TestAgdaFile.fs" />
+        <EmbeddedResource Include="Example.dot" />
+        <EmbeddedResource Include="Example.agda" />
+    </ItemGroup>
+
+    <ItemGroup>
+      <ProjectReference Include="..\AgdaUnusedOpens\AgdaUnusedOpens.fsproj" />
+    </ItemGroup>
+
+</Project>

AgdaUnusedOpens.Test/Example.agda

@@ -0,0 +1,122 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Homomorphisms.Definition
+open import Groups.Definition
+open import Numbers.Naturals.Definition
+open import Numbers.Naturals.Order
+open import Setoids.Orders
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Rings.Definition
+open import Rings.Homomorphisms.Definition
+open import Groups.Homomorphisms.Lemmas
+open import Rings.IntegralDomains.Definition
+open import Orders
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Rings.EuclideanDomains.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
+
+open import Rings.Divisible.Definition R
+open Setoid S
+open Equivalence eq
+open Ring R
+open Group additiveGroup
+
+record DivisionAlgorithmResult (norm : {a : A} → ((a ∼ 0R) → False) → ℕ) {x y : A} (x!=0 : (x ∼ 0R) → False) (y!=0 : (y ∼ 0R) → False) : Set (a ⊔ b) where
+  field
+    quotient : A
+    rem : A
+    remSmall : (rem ∼ 0R) || Sg ((rem ∼ 0R) → False) (λ rem!=0 → (norm rem!=0) <N (norm y!=0))
+    divAlg : x ∼ ((quotient * y) + rem)
+
+record DivisionAlgorithmResult' (norm : (a : A) → ℕ) (x y : A) : Set (a ⊔ b) where
+  field
+    quotient : A
+    rem : A
+    remSmall : (rem ∼ 0R) || ((norm rem) <N (norm y))
+    divAlg : x ∼ ((quotient * y) + rem)
+
+record EuclideanDomain : Set (a ⊔ lsuc b) where
+  field
+    isIntegralDomain : IntegralDomain R
+    norm : {a : A} → ((a ∼ 0R) → False) → ℕ
+    normSize : {a b : A} → (a!=0 : (a ∼ 0R) → False) → (b!=0 : (b ∼ 0R) → False) → (c : A) → b ∼ (a * c) → (norm a!=0) ≤N (norm b!=0)
+    divisionAlg : {a b : A} → (a!=0 : (a ∼ 0R) → False) → (b!=0 : (b ∼ 0R) → False) → DivisionAlgorithmResult norm a!=0 b!=0
+  normWellDefined : {a : A} → (p1 p2 : (a ∼ 0R) → False) → norm p1 ≡ norm p2
+  normWellDefined {a} p1 p2 with normSize p1 p2 1R (symmetric (transitive *Commutative identIsIdent))
+  normWellDefined {a} p1 p2 | inl n1<n2 with normSize p2 p1 1R (symmetric (transitive *Commutative identIsIdent))
+  normWellDefined {a} p1 p2 | inl n1<n2 | inl n2<n1 = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder n1<n2 n2<n1))
+  normWellDefined {a} p1 p2 | inl n1<n2 | inr n2=n1 = equalityCommutative n2=n1
+  normWellDefined {a} p1 p2 | inr n1=n2 = n1=n2
+  normWellDefined' : {a b : A} → (a ∼ b) → (a!=0 : (a ∼ 0R) → False) → (b!=0 : (b ∼ 0R) → False) → norm a!=0 ≡ norm b!=0
+  normWellDefined' a=b a!=0 b!=0 with normSize a!=0 b!=0 1R (symmetric (transitive *Commutative (transitive identIsIdent a=b)))
+  normWellDefined' a=b a!=0 b!=0 | inl a<b with normSize b!=0 a!=0 1R (symmetric (transitive *Commutative (transitive identIsIdent (symmetric a=b))))
+  normWellDefined' a=b a!=0 b!=0 | inl a<b | inl b<a = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder a<b b<a))
+  normWellDefined' a=b a!=0 b!=0 | inl a<b | inr n= = equalityCommutative n=
+  normWellDefined' a=b a!=0 b!=0 | inr n= = n=
+
+record EuclideanDomain' : Set (a ⊔ lsuc b) where
+  field
+    isIntegralDomain : IntegralDomain R
+    norm : A → ℕ
+    normWellDefined : {a b : A} → (a ∼ b) → norm a ≡ norm b
+    normSize : (a b : A) → (a ∣ b) → ((b ∼ 0R) → False) → norm a ≤N (norm b)
+    divisionAlg : (a b : A) → ((b ∼ 0R) → False) → DivisionAlgorithmResult' norm a b
+
+normEquiv : (e : EuclideanDomain) (decidableZero : (a : A) → (a ∼ 0R) || ((a ∼ 0R) → False)) → A → ℕ
+normEquiv e decidableZero a with decidableZero a
+... | inl a=0 = 0
+... | inr a!=0 = EuclideanDomain.norm e a!=0
+
+normSizeEquiv : (e : EuclideanDomain) (decidableZero : (a : A) → (a ∼ 0R) || ((a ∼ 0R) → False)) (a b : A) → (a ∣ b) → ((b ∼ 0R) → False) → normEquiv e decidableZero a ≤N normEquiv e decidableZero b
+normSizeEquiv e decidableZero a b (c , ac=b) b!=0 = ans
+  where
+    abstract
+      a!=0 : (a ∼ 0R) → False
+      a!=0 a=0 = b!=0 (transitive (symmetric ac=b) (transitive (*WellDefined a=0 reflexive) (transitive *Commutative timesZero)))
+    normIs : normEquiv e decidableZero a ≡ EuclideanDomain.norm e a!=0
+    normIs with decidableZero a
+    normIs | inl a=0 = exFalso (a!=0 a=0)
+    normIs | inr a!=0' = EuclideanDomain.normWellDefined e a!=0' a!=0
+    normIs' : normEquiv e decidableZero b ≡ EuclideanDomain.norm e b!=0
+    normIs' with decidableZero b
+    normIs' | inl b=0 = exFalso (b!=0 b=0)
+    normIs' | inr b!=0' = EuclideanDomain.normWellDefined e b!=0' b!=0
+    ans : (normEquiv e decidableZero a) ≤N (normEquiv e decidableZero b)
+    ans with EuclideanDomain.normSize e a!=0 b!=0 c (symmetric ac=b)
+    ans | inl n<Nn = inl (identityOfIndiscernablesLeft _<N_ (identityOfIndiscernablesRight _<N_ n<Nn (equalityCommutative normIs')) (equalityCommutative normIs))
+    ans | inr n=n = inr (transitivity normIs (transitivity n=n (equalityCommutative normIs')))
+
+divisionAlgEquiv : (e : EuclideanDomain) (decidableZero : (a : A) → (a ∼ 0R) || ((a ∼ 0R) → False)) → (a b : A) → ((b ∼ 0R) → False) → DivisionAlgorithmResult' (normEquiv e decidableZero) a b
+divisionAlgEquiv e decidableZero a b b!=0 with decidableZero a
+divisionAlgEquiv e decidableZero a b b!=0 | inl a=0 = record { quotient = 0R ; rem = 0R ; remSmall = inl reflexive ; divAlg = transitive a=0 (transitive (symmetric identLeft) (+WellDefined (symmetric (transitive *Commutative timesZero)) reflexive)) }
+divisionAlgEquiv e decidableZero a b b!=0 | inr a!=0 with EuclideanDomain.divisionAlg e a!=0 b!=0
+divisionAlgEquiv e decidableZero a b b!=0 | inr a!=0 | record { quotient = quotient ; rem = rem ; remSmall = inl x ; divAlg = divAlg } = record { quotient = quotient ; rem = rem ; remSmall = inl x ; divAlg = divAlg }
+divisionAlgEquiv e decidableZero a b b!=0 | inr a!=0 | record { quotient = quotient ; rem = rem ; remSmall = inr (rem!=0 , pr) ; divAlg = divAlg } = record { quotient = quotient ; rem = rem ; remSmall = inr (identityOfIndiscernablesLeft _<N_ (identityOfIndiscernablesRight _<N_ pr (equalityCommutative normIs')) (equalityCommutative normIs)) ; divAlg = divAlg }
+  where
+    normIs : normEquiv e decidableZero rem ≡ EuclideanDomain.norm e rem!=0
+    normIs with decidableZero rem
+    normIs | inl rem=0 = exFalso (rem!=0 rem=0)
+    normIs | inr rem!=0' = EuclideanDomain.normWellDefined e rem!=0' rem!=0
+    normIs' : normEquiv e decidableZero b ≡ EuclideanDomain.norm e b!=0
+    normIs' with decidableZero b
+    normIs' | inl b=0 = exFalso (b!=0 b=0)
+    normIs' | inr b!=0' = EuclideanDomain.normWellDefined e b!=0' b!=0
+
+normWellDefined : (e : EuclideanDomain) (decidableZero : (a : A) → (a ∼ 0R) || ((a ∼ 0R) → False)) {a b : A} (a=b : a ∼ b) → normEquiv e decidableZero a ≡ normEquiv e decidableZero b
+normWellDefined e decidableZero {a} {b} a=b with decidableZero a
+normWellDefined e decidableZero {a} {b} a=b | inl a=0 with decidableZero b
+normWellDefined e decidableZero {a} {b} a=b | inl a=0 | inl b=0 = refl
+normWellDefined e decidableZero {a} {b} a=b | inl a=0 | inr b!=0 = exFalso (b!=0 (transitive (symmetric a=b) a=0))
+normWellDefined e decidableZero {a} {b} a=b | inr a!=0 with decidableZero b
+normWellDefined e decidableZero {a} {b} a=b | inr a!=0 | inl b=0 = exFalso (a!=0 (transitive a=b b=0))
+normWellDefined e decidableZero {a} {b} a=b | inr a!=0 | inr b!=0 = EuclideanDomain.normWellDefined' e a=b a!=0 b!=0
+
+eucDomsEquiv : (decidableZero : (a : A) → (a ∼ 0R) || ((a ∼ 0R) → False)) → EuclideanDomain → EuclideanDomain'
+eucDomsEquiv decidableZero e = record { isIntegralDomain = EuclideanDomain.isIntegralDomain e ; norm = normEquiv e decidableZero ; normSize = normSizeEquiv e decidableZero ; divisionAlg = divisionAlgEquiv e decidableZero ; normWellDefined = normWellDefined e decidableZero }
+
+

AgdaUnusedOpens.Test/Example.dot

@@ -0,0 +1,23 @@
+digraph dependencies {
+   m0[label="Sequences"];
+   m1[label="Setoids.Setoids"];
+   m6[label="Numbers.Naturals.Definition"];
+   m2[label="LogicalFormulae"];
+   m3[label="Agda.Primitive"];
+   m4[label="Functions"];
+   m5[label="Sets.EquivalenceRelations"];
+   m0 -> m1;
+   m0 -> m2;
+   m0 -> m6;
+   m1 -> m2;
+   m1 -> m3;
+   m1 -> m4;
+   m1 -> m5;
+   m2 -> m3;
+   m4 -> m2;
+   m4 -> m3;
+   m5 -> m2;
+   m5 -> m3;
+   m5 -> m4;
+   m6 -> m2;
+}

AgdaUnusedOpens.Test/TestAgdaFile.fs

@@ -0,0 +1,35 @@
+namespace AgdaUnusedOpens.Test
+
+open AgdaUnusedOpens
+open NUnit.Framework
+open FsUnitTyped
+
+[<TestFixture>]
+module TestAgdaFile =
+
+    [<Test>]
+    let ``Make example`` () =
+        let agdaFile =
+            "Example.agda"
+            |> Utils.getResource'
+            |> AgdaFile.make
+        agdaFile.ModuleLine
+        |> shouldEqual 20
+        agdaFile.Path.Head
+        |> shouldEqual "Rings"
+        agdaFile.Path.Tail
+        |> shouldEqual ["EuclideanDomains" ; "Definition"]
+
+    [<Test>]
+    let ``Rename example`` () =
+        let agdaFile =
+            "Example.agda"
+            |> Utils.getResource'
+            |> AgdaFile.make
+        let newFile = AgdaFile.rename "NewModule" agdaFile
+        newFile.ModuleLine |> shouldEqual 20
+        newFile.Path.Head |> shouldEqual "Rings"
+        newFile.Path.Tail |> shouldEqual ["EuclideanDomains" ; "NewModule"]
+
+        let expected = "module Rings.EuclideanDomains.NewModule {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where"
+        newFile.Contents.[20] |> shouldEqual expected

AgdaUnusedOpens.Test/TestGraph.fs

@@ -0,0 +1,46 @@
+namespace AgdaUnusedOpens.Test
+
+open NUnit.Framework
+open FsUnitTyped
+
+open AgdaUnusedOpens
+
+[<TestFixture>]
+module TestGraph =
+    [<Test>]
+    let ``Hard-coded example`` () =
+        let g =
+            "Example.dot"
+            |> Utils.getResource
+            |> Graph.parse
+        match g with
+        | Success (Graph 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 actual = g |> Set.ofList
+            let expected =
+                [
+                    (m0, m1)
+                    (m0, m2)
+                    (m0, m6)
+                    (m1, m2)
+                    (m1, m3)
+                    (m1, m4)
+                    (m1, m5)
+                    (m2, m3)
+                    (m4, m2)
+                    (m4, m3)
+                    (m5, m2)
+                    (m5, m3)
+                    (m5, m4)
+                    (m6, m2)
+                ]
+                |> List.map (fun (a, b) -> { From = a ; To = b })
+                |> Set.ofList
+            actual |> shouldEqual expected
+        | x -> failwithf "oh no: %O" x

AgdaUnusedOpens.Test/TestSeq.fs

@@ -0,0 +1,17 @@
+namespace AgdaUnusedOpens.Test
+
+open AgdaUnusedOpens.Internals
+open NUnit.Framework
+open FsUnitTyped
+open FsCheck
+
+[<TestFixture>]
+module TestSeq =
+    [<Test>]
+    let ``PBT for Seq.omit`` () =
+        let property (l1 : byte list) (x : byte) (l2 : byte list) =
+            Seq.omit (List.length l1) (l1 @ (x :: l2))
+            |> List.ofSeq
+            |> shouldEqual (l1 @ l2)
+
+        Check.QuickThrowOnFailure property

AgdaUnusedOpens.Test/Utils.fs

@@ -0,0 +1,25 @@
+namespace AgdaUnusedOpens.Test
+
+open System.IO
+open System.Text.RegularExpressions
+
+type Dummy = Dummy
+
+[<RequireQualifiedAccess>]
+module Utils =
+
+    /// E.g. getResource "Example.dot" for the .dot embedded resource
+    let getResource (filename : string) : string =
+        let assembly = typeof<Dummy>.Assembly
+        let resource = assembly.GetManifestResourceStream(sprintf "AgdaUnusedOpens.Test.%s" filename)
+        use tr = new StreamReader(resource)
+        tr.ReadToEnd ()
+
+    let getResource' (filename : string) : string list =
+        let assembly = typeof<Dummy>.Assembly
+        let resource = assembly.GetManifestResourceStream(sprintf "AgdaUnusedOpens.Test.%s" filename)
+        use tr = new StreamReader(resource)
+        tr.ReadToEnd ()
+        |> fun i -> Regex.Split(i, "\r\n|\r|\n")
+        |> Array.toList
+

AgdaUnusedOpens.sln

@@ -0,0 +1,28 @@
+
+Microsoft Visual Studio Solution File, Format Version 12.00
+Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "AgdaUnusedOpens.App", "AgdaUnusedOpens.App\AgdaUnusedOpens.App.fsproj", "{CF6D84A6-2880-47D5-9004-13FF7CE0A7D6}"
+EndProject
+Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "AgdaUnusedOpens", "AgdaUnusedOpens\AgdaUnusedOpens.fsproj", "{282FC324-B5FE-4B8C-AC2A-A7EB4212E302}"
+EndProject
+Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "AgdaUnusedOpens.Test", "AgdaUnusedOpens.Test\AgdaUnusedOpens.Test.fsproj", "{C3886141-F280-48FA-860F-CBC1696B58C7}"
+EndProject
+Global
+	GlobalSection(SolutionConfigurationPlatforms) = preSolution
+		Debug|Any CPU = Debug|Any CPU
+		Release|Any CPU = Release|Any CPU
+	EndGlobalSection
+	GlobalSection(ProjectConfigurationPlatforms) = postSolution
+		{CF6D84A6-2880-47D5-9004-13FF7CE0A7D6}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+		{CF6D84A6-2880-47D5-9004-13FF7CE0A7D6}.Debug|Any CPU.Build.0 = Debug|Any CPU
+		{CF6D84A6-2880-47D5-9004-13FF7CE0A7D6}.Release|Any CPU.ActiveCfg = Release|Any CPU
+		{CF6D84A6-2880-47D5-9004-13FF7CE0A7D6}.Release|Any CPU.Build.0 = Release|Any CPU
+		{282FC324-B5FE-4B8C-AC2A-A7EB4212E302}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+		{282FC324-B5FE-4B8C-AC2A-A7EB4212E302}.Debug|Any CPU.Build.0 = Debug|Any CPU
+		{282FC324-B5FE-4B8C-AC2A-A7EB4212E302}.Release|Any CPU.ActiveCfg = Release|Any CPU
+		{282FC324-B5FE-4B8C-AC2A-A7EB4212E302}.Release|Any CPU.Build.0 = Release|Any CPU
+		{C3886141-F280-48FA-860F-CBC1696B58C7}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+		{C3886141-F280-48FA-860F-CBC1696B58C7}.Debug|Any CPU.Build.0 = Debug|Any CPU
+		{C3886141-F280-48FA-860F-CBC1696B58C7}.Release|Any CPU.ActiveCfg = Release|Any CPU
+		{C3886141-F280-48FA-860F-CBC1696B58C7}.Release|Any CPU.Build.0 = Release|Any CPU
+	EndGlobalSection
+EndGlobal

AgdaUnusedOpens.sln.DotSettings

@@ -0,0 +1,3 @@
+<wpf:ResourceDictionary xml:space="preserve" xmlns:x="http://schemas.microsoft.com/winfx/2006/xaml" xmlns:s="clr-namespace:System;assembly=mscorlib" xmlns:ss="urn:shemas-jetbrains-com:settings-storage-xaml" xmlns:wpf="http://schemas.microsoft.com/winfx/2006/xaml/presentation">
+	<s:Boolean x:Key="/Default/UserDictionary/Words/=agda/@EntryIndexedValue">True</s:Boolean>
+	<s:Boolean x:Key="/Default/UserDictionary/Words/=Setoids/@EntryIndexedValue">True</s:Boolean></wpf:ResourceDictionary>

AgdaUnusedOpens/AgdaCompiler.fs

@@ -0,0 +1,23 @@
+namespace AgdaUnusedOpens
+
+open System.IO
+
+type AgdaCompiler =
+    {
+        Compiler : FileInfo
+        /// The directory which your Agda modules are defined relative to
+        AgdaRoot : DirectoryInfo
+    }
+
+[<RequireQualifiedAccess>]
+module AgdaCompiler =
+
+    let compiles (config : AgdaCompiler) (f : AgdaFile) : bool =
+        // Write it out with a different, temporary name, and then run the compiler.
+        // Delete the temporary file afterwards.
+        let tempName = failwith ""
+        let newFile = AgdaFile.rename tempName f
+        AgdaFile.flush config.AgdaRoot newFile
+        // run the compiler
+        (Path.combine config.AgdaRoot newFile.Path).Delete()
+        true

AgdaUnusedOpens/AgdaFile.fs

@@ -0,0 +1,87 @@
+namespace AgdaUnusedOpens
+
+open AgdaUnusedOpens.Internals
+open System.IO
+open System.Text.RegularExpressions
+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)
+
+    let toString (p : Path) : string =
+        match p.Tail with
+        | [] ->
+            p.Head
+        | _ ->
+            sprintf "%s.%s" p.Head (String.concat "." p.Tail)
+
+    let combine (agdaRoot : DirectoryInfo) (p : Path) : FileInfo =
+        p
+        |> fold (fun soFar next -> Path.Combine (soFar, next)) agdaRoot.FullName
+        |> FileInfo
+
+    let rename (newModule : string) (p : Path) =
+        match p.Tail with
+        | [] -> { Head = newModule ; Tail = [] }
+        | t -> { Head = p.Head ; Tail = t |> List.rev |> List.tail |> (fun i -> newModule :: i) |> List.rev }
+
+    let make (p : string list) =
+        match p with
+        | [] -> failwith "You fool"
+        | x :: xs ->
+            {
+                Head = x
+                Tail = xs
+            }
+
+/// An in-memory representation of an Agda file.
+type AgdaFile =
+    internal
+        {
+            Path : Path
+            Contents : string list
+            /// Line number of the line which contains the module statement
+            ModuleLine : int
+        }
+
+[<RequireQualifiedAccess>]
+module AgdaFile =
+    let make (lines : string list) : AgdaFile =
+        let moduleLineNo, moduleLine =
+            lines
+            |> List.indexed
+            |> List.filter (fun (_, line) -> line.TrimStart().StartsWith "module ")
+            |> List.exactlyOne
+        let pathRegex = Regex ".*module ([^ ]+) .*where"
+        let path =
+            (pathRegex.Match moduleLine).Groups.[1].Value.Split('.')
+            |> Array.toList
+            |> Path.make
+
+        {
+            Path = path
+            Contents = lines
+            ModuleLine = moduleLineNo
+        }
+
+    let flush (agdaRoot : DirectoryInfo) (f : AgdaFile) : unit =
+        let location = Path.combine agdaRoot f.Path
+        File.WriteAllLines (location.FullName, f.Contents)
+
+    let rename (newName : string) (f : AgdaFile) : AgdaFile =
+        let newPath = Path.rename newName f.Path
+        {
+            Path = newPath
+            Contents =
+                let currentLine = f.Contents.[f.ModuleLine]
+                let newLine =
+                    let i = currentLine.IndexOf "module " + String.length "module "
+                    sprintf "%s%s%s" (currentLine.Substring(0, i)) (Path.toString newPath) (currentLine.Substring(currentLine.IndexOf(' ', i)))
+                f.Contents
+                |> List.replaceAt f.ModuleLine newLine
+            ModuleLine = f.ModuleLine
+        }
+

AgdaUnusedOpens/AgdaUnusedOpens.fsproj

@@ -0,0 +1,17 @@
+<Project Sdk="Microsoft.NET.Sdk">
+
+    <PropertyGroup>
+        <TargetFramework>netcoreapp3.0</TargetFramework>
+    </PropertyGroup>
+
+    <ItemGroup>
+        <Compile Include="AssemblyInfo.fs" />
+        <Compile Include="Seq.fs" />
+        <Compile Include="Types.fs" />
+        <Compile Include="AgdaFile.fs" />
+        <Compile Include="AgdaCompiler.fs" />
+        <Compile Include="Graph.fs" />
+        <Compile Include="OpenStatement.fs" />
+    </ItemGroup>
+
+</Project>

AgdaUnusedOpens/AssemblyInfo.fs

@@ -0,0 +1,8 @@
+module AssemblyInfo
+
+open System.Runtime.CompilerServices
+
+[<assembly: InternalsVisibleTo("AgdaUnusedOpens.Test")>]
+do
+    ()
+

AgdaUnusedOpens/Graph.fs

@@ -0,0 +1,76 @@
+namespace AgdaUnusedOpens
+
+open System.Diagnostics
+open System.IO
+open System.Text.RegularExpressions
+open AgdaUnusedOpens.Types
+
+type Arrow =
+    {
+        From : Path
+        To : Path
+    }
+
+type Graph = Graph of Arrow list
+
+type ParseResult =
+    | NotDotFile of string
+    | 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)
+
+        arrows
+        |> List.map (fun (from, to') ->
+            {
+                From = Map.find from nodes
+                To = Map.find to' nodes
+            })
+        |> Graph
+        |> Success
+
+    let load (agda : AgdaCompiler) (f : AgdaFile) : ParseResult =
+        let tmp = Path.GetTempFileName ()
+        use proc = new Process ()
+        proc.StartInfo.FileName <- agda.Compiler.FullName
+        proc.StartInfo.Arguments <- sprintf "%s --dependency-graph=%s" (Path.combine agda.AgdaRoot f.Path).FullName tmp
+        let res = proc.Start ()
+        assert (res = true)
+        tmp
+        |> File.ReadAllText
+        |> parse

AgdaUnusedOpens/OpenStatement.fs

@@ -0,0 +1,28 @@
+namespace AgdaUnusedOpens
+
+open AgdaUnusedOpens.Internals
+
+type OpenStatement =
+    {
+        File : AgdaFile
+        LineNumber : int
+    }
+
+[<RequireQualifiedAccess>]
+module OpenStatement =
+    let get (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 =
+        {
+            Path = f.Path
+            Contents = f.Contents |> Seq.omit s.LineNumber |> Seq.toList
+            ModuleLine =
+                if f.ModuleLine < s.LineNumber then f.ModuleLine
+                elif f.ModuleLine = s.LineNumber then failwith "This is unexpected"
+                else f.ModuleLine - 1
+        }
+

AgdaUnusedOpens/Seq.fs

@@ -0,0 +1,19 @@
+namespace AgdaUnusedOpens.Internals
+
+[<RequireQualifiedAccess>]
+module internal Seq =
+    let omit<'a> (n : int) (s : 'a seq) : 'a seq =
+        seq {
+            let enumerator = s.GetEnumerator ()
+            let mutable i = 0
+            while enumerator.MoveNext () do
+                if i <> n then
+                    yield enumerator.Current
+                i <- i + 1
+        }
+
+module internal List =
+    let replaceAt<'a> (n : int) (replacement : 'a) (s : 'a list) : 'a list =
+        let arr = List.toArray s
+        arr.[n] <- replacement
+        Array.toList arr

AgdaUnusedOpens/Types.fs

@@ -0,0 +1,9 @@
+namespace AgdaUnusedOpens.Types
+
+type Path =
+    internal
+        {
+            Head : string
+            Tail : string list
+        }
+