From 421fe4bcb7d861225f4937134c07fd070358d02a Mon Sep 17 00:00:00 2001 From: Smaug123 Date: Tue, 24 Dec 2019 09:35:06 +0000 Subject: [PATCH] Initial commit of the bones of an unused-open-removing Agda tool --- .gitignore | 3 + .idea/.idea.AgdaUnusedOpens/.idea/.gitignore | 2 + .../.idea/indexLayout.xml | 8 ++ .../.idea/projectSettingsUpdater.xml | 6 + .../AgdaUnusedOpens.App.fsproj | 17 +++ AgdaUnusedOpens.App/Program.fs | 11 ++ .../AgdaUnusedOpens.Test.fsproj | 31 +++++ AgdaUnusedOpens.Test/Example.agda | 122 ++++++++++++++++++ AgdaUnusedOpens.Test/Example.dot | 23 ++++ AgdaUnusedOpens.Test/TestAgdaFile.fs | 35 +++++ AgdaUnusedOpens.Test/TestGraph.fs | 46 +++++++ AgdaUnusedOpens.Test/TestSeq.fs | 17 +++ AgdaUnusedOpens.Test/Utils.fs | 25 ++++ AgdaUnusedOpens.sln | 28 ++++ AgdaUnusedOpens.sln.DotSettings | 3 + AgdaUnusedOpens/AgdaCompiler.fs | 23 ++++ AgdaUnusedOpens/AgdaFile.fs | 87 +++++++++++++ AgdaUnusedOpens/AgdaUnusedOpens.fsproj | 17 +++ AgdaUnusedOpens/AssemblyInfo.fs | 8 ++ AgdaUnusedOpens/Graph.fs | 76 +++++++++++ AgdaUnusedOpens/OpenStatement.fs | 28 ++++ AgdaUnusedOpens/Seq.fs | 19 +++ AgdaUnusedOpens/Types.fs | 9 ++ 23 files changed, 644 insertions(+) create mode 100644 .gitignore create mode 100644 .idea/.idea.AgdaUnusedOpens/.idea/.gitignore create mode 100644 .idea/.idea.AgdaUnusedOpens/.idea/indexLayout.xml create mode 100644 .idea/.idea.AgdaUnusedOpens/.idea/projectSettingsUpdater.xml create mode 100644 AgdaUnusedOpens.App/AgdaUnusedOpens.App.fsproj create mode 100644 AgdaUnusedOpens.App/Program.fs create mode 100644 AgdaUnusedOpens.Test/AgdaUnusedOpens.Test.fsproj create mode 100644 AgdaUnusedOpens.Test/Example.agda create mode 100644 AgdaUnusedOpens.Test/Example.dot create mode 100644 AgdaUnusedOpens.Test/TestAgdaFile.fs create mode 100644 AgdaUnusedOpens.Test/TestGraph.fs create mode 100644 AgdaUnusedOpens.Test/TestSeq.fs create mode 100644 AgdaUnusedOpens.Test/Utils.fs create mode 100644 AgdaUnusedOpens.sln create mode 100644 AgdaUnusedOpens.sln.DotSettings create mode 100644 AgdaUnusedOpens/AgdaCompiler.fs create mode 100644 AgdaUnusedOpens/AgdaFile.fs create mode 100644 AgdaUnusedOpens/AgdaUnusedOpens.fsproj create mode 100644 AgdaUnusedOpens/AssemblyInfo.fs create mode 100644 AgdaUnusedOpens/Graph.fs create mode 100644 AgdaUnusedOpens/OpenStatement.fs create mode 100644 AgdaUnusedOpens/Seq.fs create mode 100644 AgdaUnusedOpens/Types.fs diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..b230ab5 --- /dev/null +++ b/.gitignore @@ -0,0 +1,3 @@ +bin/ +obj/ +/packages/ \ No newline at end of file diff --git a/.idea/.idea.AgdaUnusedOpens/.idea/.gitignore b/.idea/.idea.AgdaUnusedOpens/.idea/.gitignore new file mode 100644 index 0000000..5c98b42 --- /dev/null +++ b/.idea/.idea.AgdaUnusedOpens/.idea/.gitignore @@ -0,0 +1,2 @@ +# Default ignored files +/workspace.xml \ No newline at end of file diff --git a/.idea/.idea.AgdaUnusedOpens/.idea/indexLayout.xml b/.idea/.idea.AgdaUnusedOpens/.idea/indexLayout.xml new file mode 100644 index 0000000..27ba142 --- /dev/null +++ b/.idea/.idea.AgdaUnusedOpens/.idea/indexLayout.xml @@ -0,0 +1,8 @@ + + + + + + + + \ No newline at end of file diff --git a/.idea/.idea.AgdaUnusedOpens/.idea/projectSettingsUpdater.xml b/.idea/.idea.AgdaUnusedOpens/.idea/projectSettingsUpdater.xml new file mode 100644 index 0000000..7515e76 --- /dev/null +++ b/.idea/.idea.AgdaUnusedOpens/.idea/projectSettingsUpdater.xml @@ -0,0 +1,6 @@ + + + + + \ No newline at end of file diff --git a/AgdaUnusedOpens.App/AgdaUnusedOpens.App.fsproj b/AgdaUnusedOpens.App/AgdaUnusedOpens.App.fsproj new file mode 100644 index 0000000..e335fd7 --- /dev/null +++ b/AgdaUnusedOpens.App/AgdaUnusedOpens.App.fsproj @@ -0,0 +1,17 @@ + + + + Exe + netcoreapp3.0 + AgdaUnusedOpens + + + + + + + + + + + diff --git a/AgdaUnusedOpens.App/Program.fs b/AgdaUnusedOpens.App/Program.fs new file mode 100644 index 0000000..d0ebd29 --- /dev/null +++ b/AgdaUnusedOpens.App/Program.fs @@ -0,0 +1,11 @@ +open System + +[] +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. \ No newline at end of file diff --git a/AgdaUnusedOpens.Test/AgdaUnusedOpens.Test.fsproj b/AgdaUnusedOpens.Test/AgdaUnusedOpens.Test.fsproj new file mode 100644 index 0000000..f74ca34 --- /dev/null +++ b/AgdaUnusedOpens.Test/AgdaUnusedOpens.Test.fsproj @@ -0,0 +1,31 @@ + + + + netcoreapp3.0 + + false + false + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/AgdaUnusedOpens.Test/Example.agda b/AgdaUnusedOpens.Test/Example.agda new file mode 100644 index 0000000..c5e923f --- /dev/null +++ b/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) 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; +} diff --git a/AgdaUnusedOpens.Test/TestAgdaFile.fs b/AgdaUnusedOpens.Test/TestAgdaFile.fs new file mode 100644 index 0000000..8e78497 --- /dev/null +++ b/AgdaUnusedOpens.Test/TestAgdaFile.fs @@ -0,0 +1,35 @@ +namespace AgdaUnusedOpens.Test + +open AgdaUnusedOpens +open NUnit.Framework +open FsUnitTyped + +[] +module TestAgdaFile = + + [] + 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"] + + [] + 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 diff --git a/AgdaUnusedOpens.Test/TestGraph.fs b/AgdaUnusedOpens.Test/TestGraph.fs new file mode 100644 index 0000000..4ff514d --- /dev/null +++ b/AgdaUnusedOpens.Test/TestGraph.fs @@ -0,0 +1,46 @@ +namespace AgdaUnusedOpens.Test + +open NUnit.Framework +open FsUnitTyped + +open AgdaUnusedOpens + +[] +module TestGraph = + [] + 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 diff --git a/AgdaUnusedOpens.Test/TestSeq.fs b/AgdaUnusedOpens.Test/TestSeq.fs new file mode 100644 index 0000000..3b6a52d --- /dev/null +++ b/AgdaUnusedOpens.Test/TestSeq.fs @@ -0,0 +1,17 @@ +namespace AgdaUnusedOpens.Test + +open AgdaUnusedOpens.Internals +open NUnit.Framework +open FsUnitTyped +open FsCheck + +[] +module TestSeq = + [] + 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 diff --git a/AgdaUnusedOpens.Test/Utils.fs b/AgdaUnusedOpens.Test/Utils.fs new file mode 100644 index 0000000..d5434db --- /dev/null +++ b/AgdaUnusedOpens.Test/Utils.fs @@ -0,0 +1,25 @@ +namespace AgdaUnusedOpens.Test + +open System.IO +open System.Text.RegularExpressions + +type Dummy = Dummy + +[] +module Utils = + + /// E.g. getResource "Example.dot" for the .dot embedded resource + let getResource (filename : string) : string = + let assembly = typeof.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.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 + diff --git a/AgdaUnusedOpens.sln b/AgdaUnusedOpens.sln new file mode 100644 index 0000000..0a141cb --- /dev/null +++ b/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 diff --git a/AgdaUnusedOpens.sln.DotSettings b/AgdaUnusedOpens.sln.DotSettings new file mode 100644 index 0000000..b6b4953 --- /dev/null +++ b/AgdaUnusedOpens.sln.DotSettings @@ -0,0 +1,3 @@ + + True + True \ No newline at end of file diff --git a/AgdaUnusedOpens/AgdaCompiler.fs b/AgdaUnusedOpens/AgdaCompiler.fs new file mode 100644 index 0000000..07def37 --- /dev/null +++ b/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 + } + +[] +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 diff --git a/AgdaUnusedOpens/AgdaFile.fs b/AgdaUnusedOpens/AgdaFile.fs new file mode 100644 index 0000000..f7a2452 --- /dev/null +++ b/AgdaUnusedOpens/AgdaFile.fs @@ -0,0 +1,87 @@ +namespace AgdaUnusedOpens + +open AgdaUnusedOpens.Internals +open System.IO +open System.Text.RegularExpressions +open AgdaUnusedOpens.Types + +[] +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 + } + +[] +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 + } + diff --git a/AgdaUnusedOpens/AgdaUnusedOpens.fsproj b/AgdaUnusedOpens/AgdaUnusedOpens.fsproj new file mode 100644 index 0000000..ead0c26 --- /dev/null +++ b/AgdaUnusedOpens/AgdaUnusedOpens.fsproj @@ -0,0 +1,17 @@ + + + + netcoreapp3.0 + + + + + + + + + + + + + diff --git a/AgdaUnusedOpens/AssemblyInfo.fs b/AgdaUnusedOpens/AssemblyInfo.fs new file mode 100644 index 0000000..99f5bb3 --- /dev/null +++ b/AgdaUnusedOpens/AssemblyInfo.fs @@ -0,0 +1,8 @@ +module AssemblyInfo + +open System.Runtime.CompilerServices + +[] +do + () + diff --git a/AgdaUnusedOpens/Graph.fs b/AgdaUnusedOpens/Graph.fs new file mode 100644 index 0000000..bb56fd4 --- /dev/null +++ b/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 + +[] +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 = + 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 = + 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 diff --git a/AgdaUnusedOpens/OpenStatement.fs b/AgdaUnusedOpens/OpenStatement.fs new file mode 100644 index 0000000..5b7d16c --- /dev/null +++ b/AgdaUnusedOpens/OpenStatement.fs @@ -0,0 +1,28 @@ +namespace AgdaUnusedOpens + +open AgdaUnusedOpens.Internals + +type OpenStatement = + { + File : AgdaFile + LineNumber : int + } + +[] +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 + } + diff --git a/AgdaUnusedOpens/Seq.fs b/AgdaUnusedOpens/Seq.fs new file mode 100644 index 0000000..cfe9c63 --- /dev/null +++ b/AgdaUnusedOpens/Seq.fs @@ -0,0 +1,19 @@ +namespace AgdaUnusedOpens.Internals + +[] +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 \ No newline at end of file diff --git a/AgdaUnusedOpens/Types.fs b/AgdaUnusedOpens/Types.fs new file mode 100644 index 0000000..6318b4d --- /dev/null +++ b/AgdaUnusedOpens/Types.fs @@ -0,0 +1,9 @@ +namespace AgdaUnusedOpens.Types + +type Path = + internal + { + Head : string + Tail : string list + } +