Internalized contrib libraries and removed dependency

CONTRIBUTORS

@@ -20,6 +20,7 @@ Fabián Heredia Montiel
 Felix Springer
 George Pollard
 GhiOm
+Giuseppe Lomurno
 Guillaume Allais
 Ilya Rezvov
 Jan de Muijnck-Hughes

idris2.ipkg

@@ -1,6 +1,6 @@
 package idris2app
 
-depends = idris2, contrib, network
+depends = idris2, network
 
 sourcedir = "src"
 

idris2api.ipkg

@@ -61,18 +61,6 @@ modules =
     Core.UnifyState,
     Core.Value,
 
-    Data.ANameMap,
-    Data.IntMap,
-    Data.LengthMatch,
-    Data.NameMap,
-    Data.StringMap,
-    Data.StringTrie,
-
-    Data.Bool.Extra,
-
-    Data.List.Extra,
-    Data.DList,
-
     IdrisPaths,
 
     Idris.CommandLine,
@@ -107,6 +95,51 @@ modules =
     Idris.IDEMode.SyntaxHighlight,
     Idris.IDEMode.TokenLine,
 
+    Libraries.Control.ANSI,
+    Libraries.Control.ANSI.CSI,
+    Libraries.Control.ANSI.SGR,
+    Libraries.Control.Delayed,
+
+    Libraries.Data.ANameMap,
+    Libraries.Data.Bool.Extra,
+    Libraries.Data.DList,
+    Libraries.Data.IntMap,
+    Libraries.Data.LengthMatch,
+    Libraries.Data.List.Extra,
+    Libraries.Data.List.Lazy,
+    Libraries.Data.NameMap,
+    Libraries.Data.SortedMap,
+    Libraries.Data.SortedSet,
+    Libraries.Data.String.Extra,
+    Libraries.Data.String.Iterator,
+    Libraries.Data.StringMap,
+    Libraries.Data.StringTrie,
+
+    Libraries.Text.Bounded,
+    Libraries.Text.Lexer,
+    Libraries.Text.Lexer.Core,
+    Libraries.Text.Literate,
+    Libraries.Text.Parser,
+    Libraries.Text.Parser.Core,
+    Libraries.Text.PrettyPrint.Prettyprinter,
+    Libraries.Text.PrettyPrint.Prettyprinter.Doc,
+    Libraries.Text.PrettyPrint.Prettyprinter.Render.String,
+    Libraries.Text.PrettyPrint.Prettyprinter.Render.Terminal,
+    Libraries.Text.PrettyPrint.Prettyprinter.SimpleDocTree,
+    Libraries.Text.PrettyPrint.Prettyprinter.Symbols,
+    Libraries.Text.PrettyPrint.Prettyprinter.Util,
+    Libraries.Text.Quantity,
+    Libraries.Text.Token,
+
+    Libraries.Utils.Binary,
+    Libraries.Utils.Either,
+    Libraries.Utils.Hex,
+    Libraries.Utils.Octal,
+    Libraries.Utils.Path,
+    Libraries.Utils.Shunting,
+    Libraries.Utils.String,
+    Libraries.Utils.Term,
+
     Parser.Package,
     Parser.Source,
     Parser.Support,
@@ -120,17 +153,6 @@ modules =
     Parser.Rule.Package,
     Parser.Rule.Source,
 
-    Text.Bounded,
-    Text.Literate,
-    Text.Quantity,
-    Text.Token,
-
-    Text.Lexer,
-    Text.Lexer.Core,
-
-    Text.Parser,
-    Text.Parser.Core,
-
     TTImp.BindImplicits,
     TTImp.Elab,
     TTImp.Impossible,
@@ -175,18 +197,9 @@ modules =
     TTImp.Interactive.GenerateDef,
     TTImp.Interactive.MakeLemma,
 
-    Utils.Binary,
-    Utils.Either,
-    Utils.Hex,
-    Utils.Octal,
-    Utils.Path,
-    Utils.Shunting,
-    Utils.String,
-    Utils.Term,
-
     Yaffle.Main,
     Yaffle.REPL
 
-depends = contrib, network
+depends = network
 
 sourcedir = "src"

src/Compiler/Common.idr

@@ -12,11 +12,11 @@ import Core.Directory
 import Core.Options
 import Core.TT
 import Core.TTC
-import Utils.Binary
+import Libraries.Utils.Binary
 
 import Data.IOArray
 import Data.List
-import Data.NameMap
+import Libraries.Data.NameMap
 import Data.Strings
 
 import System.Directory

src/Compiler/CompileExpr.idr

@@ -11,7 +11,7 @@ import Core.Value
 
 import Data.List
 import Data.Maybe
-import Data.NameMap
+import Libraries.Data.NameMap
 import Data.Vect
 
 %default covering

src/Compiler/ES/ES.idr

@@ -1,11 +1,11 @@
 module Compiler.ES.ES
 
 import Compiler.ES.Imperative
-import Utils.Hex
+import Libraries.Utils.Hex
 import Data.List1
 import Data.Strings
-import Data.SortedMap
-import Data.String.Extra
+import Libraries.Data.SortedMap
+import Libraries.Data.String.Extra
 
 import Core.Directory
 

src/Compiler/ES/Javascript.idr

@@ -7,14 +7,14 @@ import Compiler.CompileExpr
 
 import Core.Context
 import Core.TT
-import Utils.Path
+import Libraries.Utils.Path
 
 import System
 import System.File
 
 import Data.Maybe
 import Data.Strings
-import Data.String.Extra
+import Libraries.Data.String.Extra
 
 
 ||| Compile a TT expression to Javascript

src/Compiler/ES/Node.idr

@@ -9,7 +9,7 @@ import Compiler.CompileExpr
 
 import Core.Context
 import Core.TT
-import Utils.Path
+import Libraries.Utils.Path
 
 import System
 import System.File

src/Compiler/ES/RemoveUnused.idr

@@ -1,7 +1,7 @@
 module Compiler.ES.RemoveUnused
 
-import Data.SortedSet
-import Data.SortedMap
+import Libraries.Data.SortedSet
+import Libraries.Data.SortedMap
 import Data.Vect
 import Data.List
 

src/Compiler/ES/TailRec.idr

@@ -3,8 +3,8 @@ module Compiler.ES.TailRec
 import Data.Maybe
 import Data.List
 import Data.Strings
-import Data.SortedSet
-import Data.SortedMap
+import Libraries.Data.SortedSet
+import Libraries.Data.SortedMap
 import Core.Name
 import Core.Context
 import Compiler.ES.ImperativeAst

src/Compiler/Inline.idr

@@ -8,9 +8,9 @@ import Core.Context.Log
 import Core.FC
 import Core.TT
 
-import Data.LengthMatch
+import Libraries.Data.LengthMatch
 import Data.Maybe
-import Data.NameMap
+import Libraries.Data.NameMap
 import Data.List
 import Data.Vect
 

src/Compiler/RefC/RefC.idr

@@ -14,8 +14,8 @@ import Core.TT
 
 import Data.IORef
 import Data.List
-import Data.DList
-import Data.NameMap
+import Libraries.Data.DList
+import Libraries.Data.NameMap
 import Data.Nat
 import Data.Strings
 import Data.Vect
@@ -26,8 +26,8 @@ import System.File
 
 import Idris.Env
 import Idris.Version
-import Utils.Hex
-import Utils.Path
+import Libraries.Utils.Hex
+import Libraries.Utils.Path
 
 findCC : IO String
 findCC

src/Compiler/Scheme/Chez.idr

@@ -11,13 +11,13 @@ import Core.Directory
 import Core.Name
 import Core.Options
 import Core.TT
-import Utils.Hex
-import Utils.Path
+import Libraries.Utils.Hex
+import Libraries.Utils.Path
 
 import Data.List
 import Data.List1
 import Data.Maybe
-import Data.NameMap
+import Libraries.Data.NameMap
 import Data.Strings
 import Data.Vect
 

src/Compiler/Scheme/Common.idr

@@ -8,7 +8,7 @@ import Core.Context
 import Core.Name
 import Core.TT
 
-import Data.Bool.Extra
+import Libraries.Data.Bool.Extra
 import Data.List
 import Data.Vect
 

src/Compiler/Scheme/Gambit.idr

@@ -10,12 +10,12 @@ import Core.Directory
 import Core.Name
 import Core.Options
 import Core.TT
-import Utils.Hex
-import Utils.Path
+import Libraries.Utils.Hex
+import Libraries.Utils.Path
 
 import Data.List
 import Data.Maybe
-import Data.NameMap
+import Libraries.Data.NameMap
 import Data.Strings
 import Data.Vect
 

src/Compiler/Scheme/Racket.idr

@@ -11,12 +11,12 @@ import Core.Context.Log
 import Core.Directory
 import Core.Name
 import Core.TT
-import Utils.Hex
-import Utils.Path
+import Libraries.Utils.Hex
+import Libraries.Utils.Path
 
 import Data.List
 import Data.Maybe
-import Data.NameMap
+import Libraries.Data.NameMap
 import Data.Nat
 import Data.Strings
 import Data.Vect

src/Core/AutoSearch.idr

@@ -9,7 +9,7 @@ import Core.TT
 import Core.Unify
 import Core.Value
 
-import Data.Bool.Extra
+import Libraries.Data.Bool.Extra
 import Data.Either
 import Data.List
 import Data.Maybe

src/Core/Binary.idr

@@ -10,9 +10,9 @@ import Core.TT
 import Core.TTC
 import Core.UnifyState
 
-import Data.IntMap
+import Libraries.Data.IntMap
 import Data.List
-import Data.NameMap
+import Libraries.Data.NameMap
 
 import System.File
 
@@ -21,7 +21,7 @@ import System.File
 -- (Otherwise we'd save out everything, not just the things in the current
 -- file).
 
-import public Utils.Binary
+import public Libraries.Utils.Binary
 
 import Data.Buffer
 

src/Core/CaseBuilder.idr

@@ -9,12 +9,12 @@ import Core.Normalise
 import Core.TT
 import Core.Value
 
-import Data.LengthMatch
+import Libraries.Data.LengthMatch
 import Data.List
 
 import Decidable.Equality
 
-import Text.PrettyPrint.Prettyprinter
+import Libraries.Text.PrettyPrint.Prettyprinter
 
 %default covering
 

src/Core/CaseTree.idr

@@ -2,11 +2,11 @@ module Core.CaseTree
 
 import Core.TT
 
-import Data.Bool.Extra
+import Libraries.Data.Bool.Extra
 import Data.List
-import Data.NameMap
+import Libraries.Data.NameMap
 
-import Text.PrettyPrint.Prettyprinter
+import Libraries.Text.PrettyPrint.Prettyprinter
 
 %default covering
 

src/Core/CompileExpr.idr

@@ -7,7 +7,7 @@ import Core.Name
 import Core.TT
 
 import Data.List
-import Data.NameMap
+import Libraries.Data.NameMap
 import Data.Vect
 
 %default covering

src/Core/Context.idr

@@ -10,13 +10,13 @@ import        Core.Options
 import public Core.Options.Log
 import public Core.TT
 
-import Utils.Binary
+import Libraries.Utils.Binary
 
-import Data.IntMap
+import Libraries.Data.IntMap
 import Data.IOArray
 import Data.List
-import Data.NameMap
-import Data.StringMap
+import Libraries.Data.NameMap
+import Libraries.Data.StringMap
 
 import System
 import System.Directory

src/Core/Context/Log.idr

@@ -3,7 +3,7 @@ module Core.Context.Log
 import Core.Context
 import Core.Options
 
-import Data.StringMap
+import Libraries.Data.StringMap
 
 import System.Clock
 

src/Core/Core.idr

@@ -7,8 +7,8 @@ import Data.List
 import Data.List1
 import Data.Vect
 import Parser.Source
-import Text.PrettyPrint.Prettyprinter
-import Text.PrettyPrint.Prettyprinter.Util
+import Libraries.Text.PrettyPrint.Prettyprinter
+import Libraries.Text.PrettyPrint.Prettyprinter.Util
 
 import public Data.IORef
 import System

src/Core/Coverage.idr

@@ -8,11 +8,11 @@ import Core.Normalise
 import Core.TT
 import Core.Value
 
-import Data.Bool.Extra
+import Libraries.Data.Bool.Extra
 import Data.List
-import Data.NameMap
+import Libraries.Data.NameMap
 
-import Text.PrettyPrint.Prettyprinter
+import Libraries.Text.PrettyPrint.Prettyprinter
 
 %default covering
 

src/Core/Directory.idr

@@ -5,7 +5,7 @@ import Core.Core
 import Core.FC
 import Core.Name
 import Core.Options
-import Utils.Path
+import Libraries.Utils.Path
 
 import Data.List
 import Data.Strings

src/Core/FC.idr

@@ -1,7 +1,7 @@
 module Core.FC
 
-import Text.Bounded
-import Text.PrettyPrint.Prettyprinter
+import Libraries.Text.Bounded
+import Libraries.Text.PrettyPrint.Prettyprinter
 
 %default total
 

src/Core/Hash.idr

@@ -5,9 +5,9 @@ import Core.TT
 
 import Data.List
 import Data.List1
-import Data.List.Lazy
+import Libraries.Data.List.Lazy
 import Data.Strings
-import Data.String.Iterator
+import Libraries.Data.String.Iterator
 
 %default covering
 

src/Core/LinearCheck.idr

@@ -11,7 +11,7 @@ import Core.UnifyState
 import Core.Value
 import Core.TT
 
-import Data.Bool.Extra
+import Libraries.Data.Bool.Extra
 import Data.List
 
 %default covering

src/Core/Metadata.idr

@@ -11,7 +11,7 @@ import Core.TTC
 
 import Data.List
 import System.File
-import Utils.Binary
+import Libraries.Utils.Binary
 
 %default covering
 

src/Core/Name.idr

@@ -3,8 +3,8 @@ module Core.Name
 import Data.List
 import Data.Strings
 import Decidable.Equality
-import Text.PrettyPrint.Prettyprinter
-import Text.PrettyPrint.Prettyprinter.Util
+import Libraries.Text.PrettyPrint.Prettyprinter
+import Libraries.Text.PrettyPrint.Prettyprinter.Util
 
 import public Core.Name.Namespace
 

src/Core/Name/Namespace.idr

@@ -4,8 +4,8 @@ import Data.List
 import Data.List1
 import Data.Strings
 import Decidable.Equality
-import Text.PrettyPrint.Prettyprinter
-import Text.PrettyPrint.Prettyprinter.Util
+import Libraries.Text.PrettyPrint.Prettyprinter
+import Libraries.Text.PrettyPrint.Prettyprinter.Util
 
 %default total
 

src/Core/Normalise.idr

@@ -10,7 +10,7 @@ import Core.Primitives
 import Core.TT
 import Core.Value
 
-import Data.IntMap
+import Libraries.Data.IntMap
 import Data.List
 import Data.Maybe
 import Data.Nat

src/Core/Options.idr

@@ -4,8 +4,8 @@ import Core.Core
 import Core.Name
 import public Core.Options.Log
 import Core.TT
-import Utils.Binary
-import Utils.Path
+import Libraries.Utils.Binary
+import Libraries.Utils.Path
 
 import Data.List
 import Data.Maybe

src/Core/Options/Log.idr

@@ -3,11 +3,11 @@ module Core.Options.Log
 import Data.List
 import Data.List1
 import Data.Maybe
-import Data.StringMap
-import Data.StringTrie
+import Libraries.Data.StringMap
+import Libraries.Data.StringTrie
 import Data.Strings
 import Data.These
-import Text.PrettyPrint.Prettyprinter
+import Libraries.Text.PrettyPrint.Prettyprinter
 
 %default total
 

src/Core/Primitives.idr

@@ -4,7 +4,7 @@ import Core.Core
 import Core.Context
 import Core.TT
 import Core.Value
-import Utils.String
+import Libraries.Utils.String
 
 import Data.Vect
 

src/Core/TT.idr

@@ -3,14 +3,14 @@ module Core.TT
 import public Core.FC
 import public Core.Name
 
-import Data.Bool.Extra
+import Libraries.Data.Bool.Extra
 import Data.List
 import Data.Nat
-import Data.NameMap
+import Libraries.Data.NameMap
 import Data.Vect
 import Decidable.Equality
-import Text.PrettyPrint.Prettyprinter
-import Text.PrettyPrint.Prettyprinter.Util
+import Libraries.Text.PrettyPrint.Prettyprinter
+import Libraries.Text.PrettyPrint.Prettyprinter.Util
 
 import public Algebra
 

src/Core/TTC.idr

@@ -10,10 +10,10 @@ import Core.Name
 import Core.Options
 import Core.TT
 
-import Data.NameMap
+import Libraries.Data.NameMap
 import Data.Vect
 
-import Utils.Binary
+import Libraries.Utils.Binary
 
 %default covering
 

src/Core/Termination.idr

@@ -10,7 +10,7 @@ import Core.Value
 
 import Control.Monad.State
 
-import Data.NameMap
+import Libraries.Data.NameMap
 import Data.List
 
 %default covering

src/Core/Transform.idr

@@ -5,7 +5,7 @@ import Core.Env
 import Core.Normalise
 import Core.TT
 
-import Data.NameMap
+import Libraries.Data.NameMap
 
 %default total
 

src/Core/Unify.idr

@@ -11,11 +11,11 @@ import Core.TT
 import public Core.UnifyState
 import Core.Value
 
-import Data.Bool.Extra
-import Data.IntMap
+import Libraries.Data.Bool.Extra
+import Libraries.Data.IntMap
 import Data.List
 import Data.List.Views
-import Data.NameMap
+import Libraries.Data.NameMap
 
 %default covering
 

src/Core/UnifyState.idr

@@ -10,12 +10,12 @@ import Core.Normalise
 import Core.Options
 import Core.TT
 import Core.TTC
-import Utils.Binary
+import Libraries.Utils.Binary
 
-import Data.IntMap
+import Libraries.Data.IntMap
 import Data.List
-import Data.NameMap
-import Data.StringMap
+import Libraries.Data.NameMap
+import Libraries.Data.StringMap
 
 %default covering
 

src/Core/Value.idr

@@ -5,7 +5,7 @@ import Core.Core
 import Core.Env
 import Core.TT
 
-import Data.IntMap
+import Libraries.Data.IntMap
 
 %default covering
 

src/Idris/Desugar.idr

@@ -9,8 +9,8 @@ import Core.Options
 import Core.TT
 import Core.Unify
 
-import Data.StringMap
-import Data.ANameMap
+import Libraries.Data.StringMap
+import Libraries.Data.ANameMap
 
 import Idris.DocString
 import Idris.Syntax
@@ -25,8 +25,8 @@ import TTImp.Parser
 import TTImp.TTImp
 import TTImp.Utils
 
-import Utils.Shunting
-import Utils.String
+import Libraries.Utils.Shunting
+import Libraries.Utils.String
 
 import Control.Monad.State
 import Data.List

src/Idris/DocString.idr

@@ -10,10 +10,10 @@ import Idris.Syntax
 
 import TTImp.TTImp
 
-import Data.ANameMap
+import Libraries.Data.ANameMap
 import Data.List
 import Data.Maybe
-import Data.NameMap
+import Libraries.Data.NameMap
 import Data.Strings
 
 -- Add a doc string for a name in the current namespace

src/Idris/Driver.idr

@@ -29,8 +29,8 @@ import Data.Strings
 import System
 import System.Directory
 import System.File
-import Utils.Path
-import Utils.Term
+import Libraries.Utils.Path
+import Libraries.Utils.Term
 
 import Yaffle.Main
 

src/Idris/Elab/Implementation.idr

@@ -21,9 +21,9 @@ import TTImp.Unelab
 import TTImp.Utils
 
 import Control.Monad.State
-import Data.ANameMap
+import Libraries.Data.ANameMap
 import Data.List
-import Data.NameMap
+import Libraries.Data.NameMap
 
 %default covering
 

src/Idris/Elab/Interface.idr

@@ -21,7 +21,7 @@ import TTImp.Unelab
 import TTImp.TTImp
 import TTImp.Utils
 
-import Data.ANameMap
+import Libraries.Data.ANameMap
 import Data.List
 import Data.Maybe
 

src/Idris/Error.idr

@@ -16,15 +16,15 @@ import Parser.Source
 
 import Data.List
 import Data.List1
-import Data.List.Extra
+import Libraries.Data.List.Extra
 import Data.Maybe
 import Data.Stream
 import Data.Strings
-import Data.String.Extra
-import Text.PrettyPrint.Prettyprinter
-import Text.PrettyPrint.Prettyprinter.Util
+import Libraries.Data.String.Extra
+import Libraries.Text.PrettyPrint.Prettyprinter
+import Libraries.Text.PrettyPrint.Prettyprinter.Util
 import System.File
-import Utils.String
+import Libraries.Utils.String
 
 %default covering
 

src/Idris/IDEMode/CaseSplit.idr

@@ -19,7 +19,7 @@ import Idris.Resugar
 import Idris.Syntax
 
 import Data.List
-import Data.List.Extra
+import Libraries.Data.List.Extra
 import Data.Strings
 import System.File
 

src/Idris/IDEMode/Commands.idr

@@ -3,7 +3,7 @@ module Idris.IDEMode.Commands
 import Core.Core
 import Core.Name
 import public Idris.REPLOpts
-import Utils.Hex
+import Libraries.Utils.Hex
 
 import System.File
 

src/Idris/IDEMode/Holes.idr

@@ -8,8 +8,8 @@ import Idris.Pretty
 
 import Idris.IDEMode.Commands
 
-import Data.String.Extra
-import Utils.Term
+import Libraries.Data.String.Extra
+import Libraries.Utils.Term
 
 %default covering
 

src/Idris/IDEMode/Parser.idr

@@ -11,10 +11,10 @@ import Data.Strings
 import Parser.Lexer.Source
 import Parser.Source
 import Parser.Support
-import Text.Lexer
-import Text.Parser
-import Utils.Either
-import Utils.String
+import Libraries.Text.Lexer
+import Libraries.Text.Parser
+import Libraries.Utils.Either
+import Libraries.Utils.String
 
 %default total
 

src/Idris/IDEMode/REPL.idr

@@ -42,7 +42,7 @@ import TTImp.Elab
 import TTImp.TTImp
 import TTImp.ProcessDecls
 
-import Utils.Hex
+import Libraries.Utils.Hex
 
 import Data.List
 import System

src/Idris/IDEMode/TokenLine.idr

@@ -2,7 +2,7 @@
 module Idris.IDEMode.TokenLine
 
 import Parser.Lexer.Source
-import Text.Lexer
+import Libraries.Text.Lexer
 
 %default total
 

src/Idris/ModTree.idr

@@ -20,12 +20,12 @@ import Idris.Syntax
 import Idris.Pretty
 
 import Data.List
-import Data.StringMap
+import Libraries.Data.StringMap
 
 import System.Directory
 import System.File
 
-import Utils.Either
+import Libraries.Utils.Either
 
 %default covering
 

src/Idris/Package.idr

@@ -12,9 +12,9 @@ import Core.Unify
 import Data.List
 import Data.Maybe
 import Data.So
-import Data.StringMap
+import Libraries.Data.StringMap
 import Data.Strings
-import Data.StringTrie
+import Libraries.Data.StringTrie
 import Data.These
 
 import Parser.Package
@@ -22,11 +22,11 @@ import System
 import System.Directory
 import System.File
 
-import Text.Parser
-import Text.PrettyPrint.Prettyprinter
-import Utils.Binary
-import Utils.String
-import Utils.Path
+import Libraries.Text.Parser
+import Libraries.Text.PrettyPrint.Prettyprinter
+import Libraries.Utils.Binary
+import Libraries.Utils.String
+import Libraries.Utils.Path
 
 import Idris.CommandLine
 import Idris.ModTree

src/Idris/Parser.idr

@@ -6,14 +6,14 @@ import public Parser.Source
 import        Parser.Lexer.Source
 import        TTImp.TTImp
 
-import public Text.Parser
+import public Libraries.Text.Parser
 import        Data.Either
 import        Data.List
 import        Data.List.Views
 import        Data.List1
 import        Data.Maybe
 import        Data.Strings
-import Utils.String
+import Libraries.Utils.String
 
 import Idris.Parser.Let
 

src/Idris/Parser/Let.idr

@@ -1,12 +1,12 @@
 module Idris.Parser.Let
 
 import Idris.Syntax
-import Text.Bounded
+import Libraries.Text.Bounded
 
 import Data.Either
 import Data.List1
 
-import Utils.String
+import Libraries.Utils.String
 
 %default total
 

src/Idris/Pretty.idr

@@ -2,15 +2,15 @@ module Idris.Pretty
 
 import Data.List
 import Data.Strings
-import Control.ANSI.SGR
-import public Text.PrettyPrint.Prettyprinter
-import public Text.PrettyPrint.Prettyprinter.Render.Terminal
-import public Text.PrettyPrint.Prettyprinter.Util
+import Libraries.Control.ANSI.SGR
+import public Libraries.Text.PrettyPrint.Prettyprinter
+import public Libraries.Text.PrettyPrint.Prettyprinter.Render.Terminal
+import public Libraries.Text.PrettyPrint.Prettyprinter.Util
 
 import Algebra
 import Idris.REPLOpts
 import Idris.Syntax
-import Utils.Term
+import Libraries.Utils.Term
 
 %default covering
 

src/Idris/ProcessIdr.idr

@@ -26,7 +26,7 @@ import Idris.Syntax
 import Idris.Pretty
 
 import Data.List
-import Data.NameMap
+import Libraries.Data.NameMap
 
 import System.File
 

src/Idris/REPL.idr

@@ -53,13 +53,13 @@ import TTImp.ProcessDecls
 
 import Data.List
 import Data.Maybe
-import Data.NameMap
-import Data.ANameMap
+import Libraries.Data.ANameMap
+import Libraries.Data.NameMap
 import Data.Stream
 import Data.Strings
-import Text.PrettyPrint.Prettyprinter
-import Text.PrettyPrint.Prettyprinter.Util
-import Text.PrettyPrint.Prettyprinter.Render.Terminal
+import Libraries.Text.PrettyPrint.Prettyprinter
+import Libraries.Text.PrettyPrint.Prettyprinter.Util
+import Libraries.Text.PrettyPrint.Prettyprinter.Render.Terminal
 
 import System
 import System.File

src/Idris/REPLCommon.idr

@@ -13,8 +13,8 @@ import Idris.Syntax
 import Idris.Pretty
 
 import Data.List
-import Text.PrettyPrint.Prettyprinter
-import Text.PrettyPrint.Prettyprinter.Render.Terminal
+import Libraries.Text.PrettyPrint.Prettyprinter
+import Libraries.Text.PrettyPrint.Prettyprinter.Render.Terminal
 
 %default covering
 

src/Idris/REPLOpts.idr

@@ -7,7 +7,7 @@ import TTImp.Interactive.ExprSearch
 import TTImp.TTImp
 
 import Data.List
-import Data.List.Extra
+import Libraries.Data.List.Extra
 import Data.Strings
 import System.File
 

src/Idris/Resugar.idr

@@ -13,7 +13,7 @@ import TTImp.Utils
 import Data.List
 import Data.List1
 import Data.Maybe
-import Data.StringMap
+import Libraries.Data.StringMap
 
 %default covering
 

src/Idris/SetOptions.idr

@@ -5,7 +5,7 @@ import Core.Directory
 import Core.Metadata
 import Core.Options
 import Core.Unify
-import Utils.Path
+import Libraries.Utils.Path
 
 import Idris.CommandLine
 import Idris.REPL

src/Idris/Syntax.idr

@@ -11,13 +11,13 @@ import public Core.TT
 
 import TTImp.TTImp
 
-import Data.ANameMap
+import Libraries.Data.ANameMap
 import Data.List
 import Data.Maybe
-import Data.NameMap
-import Data.StringMap
-import Text.PrettyPrint.Prettyprinter
-import Text.PrettyPrint.Prettyprinter.Util
+import Libraries.Data.NameMap
+import Libraries.Data.StringMap
+import Libraries.Text.PrettyPrint.Prettyprinter
+import Libraries.Text.PrettyPrint.Prettyprinter.Util
 
 %default covering
 

src/Libraries/Control/ANSI.idr

@@ -0,0 +1,36 @@
+module Libraries.Control.ANSI
+
+import public Libraries.Control.ANSI.CSI
+import public Libraries.Control.ANSI.SGR
+
+%default total
+
+public export
+record DecoratedString where
+  constructor MkDString
+  sgr : List SGR
+  str : String
+
+export
+Show DecoratedString where
+  show dstr = escapeSGR dstr.sgr ++ dstr.str ++ escapeSGR [Reset]
+
+export
+colored : Color -> String -> DecoratedString
+colored c = MkDString [SetForeground c]
+
+export
+background : Color -> String -> DecoratedString
+background c = MkDString [SetBackground c]
+
+export
+bolden : String -> DecoratedString
+bolden = MkDString [SetStyle Bold]
+
+export
+italicize : String -> DecoratedString
+italicize = MkDString [SetStyle Italic]
+
+export
+underline : String -> DecoratedString
+underline = MkDString [SetStyle SingleUnderline]

src/Libraries/Control/ANSI/CSI.idr

@@ -0,0 +1,105 @@
+module Libraries.Control.ANSI.CSI
+
+%default total
+
+||| Moves the cursor n columns up.
+||| If the cursor is at the edge of the screen it has no effect.
+export
+cursorUp : Nat -> String
+cursorUp n = "\x1B[" ++ show n ++ "A"
+
+export
+cursorUp1 : String
+cursorUp1 = cursorUp 1
+
+||| Moves the cursor n columns down.
+||| If the cursor is at the edge of the screen it has no effect.
+export
+cursorDown : Nat -> String
+cursorDown n = "\x1B[" ++ show n ++ "B"
+
+export
+cursorDown1 : String
+cursorDown1 = cursorDown 1
+
+||| Moves the cursor n columns forward.
+||| If the cursor is at the edge of the screen it has no effect.
+export
+cursorForward : Nat -> String
+cursorForward n = "\x1B[" ++ show n ++ "C"
+
+export
+cursorForward1 : String
+cursorForward1 = cursorForward 1
+
+||| Moves the cursor n columns back.
+||| If the cursor is at the edge of the screen it has no effect.
+export
+cursorBack : Nat -> String
+cursorBack n = "\x1B[" ++ show n ++ "D"
+
+export
+cursorBack1 : String
+cursorBack1 = cursorBack 1
+
+||| Moves the cursor at the beginning of n lines down.
+||| If the cursor is at the edge of the screen it has no effect.
+export
+cursorNextLine : Nat -> String
+cursorNextLine n = "\x1B[" ++ show n ++ "E"
+
+export
+cursorNextLine1 : String
+cursorNextLine1 = cursorNextLine 1
+
+||| Moves the cursor at the beginning of n lines up.
+||| If the cursor is at the edge of the screen it has no effect.
+export
+cursorPrevLine : Nat -> String
+cursorPrevLine n = "\x1B[" ++ show n ++ "F"
+
+export
+cursorPrevLine1 : String
+cursorPrevLine1 = cursorPrevLine 1
+
+||| Moves the cursor at an arbitrary line and column.
+||| Both lines and columns start at 1.
+export
+cursorMove : (row : Nat) -> (col : Nat) -> String
+cursorMove row col = "\x1B[" ++ show row ++ ";" ++ show col ++ "H"
+
+public export
+data EraseDirection = Start | End | All
+
+Cast EraseDirection String where
+  cast Start = "1"
+  cast End = "0"
+  cast All = "2"
+
+||| Clears part of the screen.
+export
+eraseScreen : EraseDirection -> String
+eraseScreen to = "\x1B[" ++ cast to ++ "J"
+
+||| Clears part of the line.
+export
+eraseLine : EraseDirection -> String
+eraseLine to = "\x1B[" ++ cast to ++ "K"
+
+||| Scrolls the whole screen up by n lines.
+export
+scrollUp : Nat -> String
+scrollUp n = "\x1B[" ++ show n ++ "S"
+
+export
+scrollUp1 : String
+scrollUp1 = scrollUp 1
+
+||| Scrolls the whole screen down by n lines.
+export
+scrollDown : Nat -> String
+scrollDown n = "\x1B[" ++ show n ++ "T"
+
+export
+scrollDown1 : String
+scrollDown1 = scrollDown 1

src/Libraries/Control/ANSI/SGR.idr

@@ -0,0 +1,73 @@
+module Libraries.Control.ANSI.SGR
+
+import Data.List
+
+%default total
+
+public export
+data Color
+  = Black | Red | Green | Yellow | Blue | Magenta | Cyan | White
+  | BrightBlack | BrightRed | BrightGreen | BrightYellow | BrightBlue | BrightMagenta | BrightCyan | BrightWhite
+
+Cast Color String where
+  cast Black = "0"
+  cast Red = "1"
+  cast Green = "2"
+  cast Yellow = "3"
+  cast Blue = "4"
+  cast Magenta = "5"
+  cast Cyan = "6"
+  cast White = "7"
+  cast BrightBlack = "8"
+  cast BrightRed = "9"
+  cast BrightGreen = "10"
+  cast BrightYellow = "11"
+  cast BrightBlue = "12"
+  cast BrightMagenta = "13"
+  cast BrightCyan = "14"
+  cast BrightWhite = "15"
+
+public export
+data Style
+  = Bold | Faint | NotBoldOrFaint | Italic
+  | SingleUnderline | DoubleUnderline | NoUnderline
+  | Striked | NotStriked
+
+Cast Style String where
+  cast Bold = "1"
+  cast Faint = "2"
+  cast NotBoldOrFaint = "22"
+  cast Italic = "3"
+  cast SingleUnderline = "4"
+  cast DoubleUnderline = "21"
+  cast NoUnderline = "24"
+  cast Striked = "9"
+  cast NotStriked = "29"
+
+public export
+data Blink = Slow | Rapid | NoBlink
+
+Cast Blink String where
+  cast Slow = "5"
+  cast Rapid = "6"
+  cast NoBlink = "25"
+
+public export
+data SGR
+  = Reset
+  | SetForeground Color
+  | SetBackground Color
+  | SetStyle Style
+  | SetBlink Blink
+
+||| Returns the ANSI escape code equivalent to the list of operations provided.
+export
+escapeSGR : List SGR -> String
+escapeSGR xs = "\x1B[" ++ concat (intersperse ";" (toCode <$> xs)) ++ "m"
+  where
+    toCode : SGR -> String
+    toCode Reset = "0"
+    toCode (SetForeground c) = "38;5;" ++ cast c
+    toCode (SetBackground c) = "48;5;" ++ cast c
+    toCode (SetStyle s) = cast s
+    toCode (SetBlink b) = cast b

src/Libraries/Control/Delayed.idr

@@ -0,0 +1,14 @@
+||| Utilities functions for contitionally delaying values.
+module Libraries.Control.Delayed
+
+||| Type-level function for a conditionally infinite type.
+public export
+inf : Bool -> Type -> Type
+inf False t = t
+inf True t = Inf t
+
+||| Type-level function for a conditionally lazy type.
+public export
+lazy : Bool -> Type -> Type
+lazy False t = t
+lazy True t = Lazy t

src/Libraries/Data/ANameMap.idr

@@ -1,11 +1,11 @@
 -- like name map, but able to return ambiguous names
-module Data.ANameMap
+module Libraries.Data.ANameMap
 
 import Core.Name
 
 import Data.List
-import Data.NameMap
-import Data.StringMap
+import Libraries.Data.NameMap
+import Libraries.Data.StringMap
 
 %default total
 

src/Libraries/Data/Bool/Extra.idr

@@ -1,4 +1,4 @@
-module Data.Bool.Extra
+module Libraries.Data.Bool.Extra
 
 %default total
 

src/Libraries/Data/DList.idr

@@ -1,4 +1,4 @@
-module Data.DList
+module Libraries.Data.DList
 
 %default total
 

src/Libraries/Data/IntMap.idr

@@ -1,4 +1,4 @@
-module Data.IntMap
+module Libraries.Data.IntMap
 
 -- Hand specialised map, for efficiency...
 

src/Libraries/Data/LengthMatch.idr

@@ -1,4 +1,4 @@
-module Data.LengthMatch
+module Libraries.Data.LengthMatch
 
 %default total
 

src/Libraries/Data/List/Extra.idr

@@ -1,4 +1,4 @@
-module Data.List.Extra
+module Libraries.Data.List.Extra
 
 %default total
 

src/Libraries/Data/List/Lazy.idr

@@ -0,0 +1,142 @@
+module Libraries.Data.List.Lazy
+
+%default total
+
+-- All functions here are public export
+-- because their definitions are pretty much the specification.
+
+public export
+data LazyList : Type -> Type where
+  Nil : LazyList a
+  (::) : (1 x : a) -> (1 xs : Lazy (LazyList a)) -> LazyList a
+
+--- Interface implementations ---
+
+public export
+Semigroup (LazyList a) where
+  [] <+> ys = ys
+  (x :: xs) <+> ys = x :: (xs <+> ys)
+
+public export
+Monoid (LazyList a) where
+  neutral = []
+
+public export
+Foldable LazyList where
+  foldr op nil [] = nil
+  foldr op nil (x :: xs) = x `op` foldr op nil xs
+
+  foldl op acc [] = acc
+  foldl op acc (x :: xs) = foldl op (acc `op` x) xs
+
+  null []     = True
+  null (_::_) = False
+
+public export
+Functor LazyList where
+  map f [] = []
+  map f (x :: xs) = f x :: map f xs
+
+public export
+Applicative LazyList where
+  pure x = [x]
+  fs <*> vs = concatMap (\f => map f vs) fs
+
+public export
+Alternative LazyList where
+  empty = []
+  (<|>) = (<+>)
+
+public export
+Monad LazyList where
+  m >>= f = concatMap f m
+
+-- There is no Traversable instance for lazy lists.
+-- The result of a traversal will be a non-lazy list in general
+-- (you can't delay the "effect" of an applicative functor).
+public export
+traverse : Applicative f => (a -> f b) -> LazyList a -> f (List b)
+traverse g [] = pure []
+traverse g (x :: xs) = [| g x :: traverse g xs |]
+
+public export
+sequence : Applicative f => LazyList (f a) -> f (List a)
+sequence = traverse id
+
+--- Lists creation ---
+
+public export
+fromList : List a -> LazyList a
+fromList []      = []
+fromList (x::xs) = x :: fromList xs
+
+covering
+public export
+iterate : (f : a -> Maybe a) -> (x : a) -> LazyList a
+iterate f x = x :: case f x of
+  Nothing => []
+  Just y  => iterate f y
+
+covering
+public export
+unfoldr : (b -> Maybe (a, b)) -> b -> LazyList a
+unfoldr f c = case f c of
+  Nothing     => []
+  Just (a, n) => a :: unfoldr f n
+
+public export
+iterateN : Nat -> (a -> a) -> a -> LazyList a
+iterateN Z     _ _ = []
+iterateN (S n) f x = x :: iterateN n f (f x)
+
+public export
+replicate : (n : Nat) -> (x : a) -> LazyList a
+replicate Z     _ = []
+replicate (S n) x = x :: replicate n x
+
+--- Functions acquiring parts of list ---
+
+public export
+head' : LazyList a -> Maybe a
+head' []     = Nothing
+head' (x::_) = Just x
+
+export
+tail' : LazyList a -> Maybe (LazyList a)
+tail' []      = Nothing
+tail' (_::xs) = Just xs
+
+--- Functions for acquiring different types of sublists ---
+
+public export
+take : Nat -> LazyList a -> LazyList a
+take (S k) (x::xs) = x :: take k xs
+take _ _ = []
+
+public export
+drop : Nat -> LazyList a -> LazyList a
+drop Z     xs      = xs
+drop (S _) []      = []
+drop (S n) (_::xs) = drop n xs
+
+public export
+takeWhile : (a -> Bool) -> LazyList a -> LazyList a
+takeWhile p []      = []
+takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []
+
+public export
+dropWhile : (a -> Bool) -> LazyList a -> LazyList a
+dropWhile p []      = []
+dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
+
+public export
+filter : (a -> Bool) -> LazyList a -> LazyList a
+filter p []      = []
+filter p (x::xs) = if p x then x :: filter p xs else filter p xs
+
+public export
+mapMaybe : (a -> Maybe b) -> LazyList a -> LazyList b
+mapMaybe f []      = []
+mapMaybe f (x::xs) = case f x of
+  Nothing => mapMaybe f xs
+  Just y  => y :: mapMaybe f xs

src/Libraries/Data/NameMap.idr

@@ -1,4 +1,4 @@
-module Data.NameMap
+module Libraries.Data.NameMap
 
 import Core.Name
 

src/Libraries/Data/SortedMap.idr

@@ -0,0 +1,334 @@
+module Libraries.Data.SortedMap
+
+-- TODO: write split
+
+private
+data Tree : Nat -> (k : Type) -> Type -> Ord k -> Type where
+  Leaf : k -> v -> Tree Z k v o
+  Branch2 : Tree n k v o -> k -> Tree n k v o -> Tree (S n) k v o
+  Branch3 : Tree n k v o -> k -> Tree n k v o -> k -> Tree n k v o -> Tree (S n) k v o
+
+branch4 :
+  Tree n k v o -> k ->
+  Tree n k v o -> k ->
+  Tree n k v o -> k ->
+  Tree n k v o ->
+  Tree (S (S n)) k v o
+branch4 a b c d e f g =
+  Branch2 (Branch2 a b c) d (Branch2 e f g)
+
+branch5 :
+  Tree n k v o -> k ->
+  Tree n k v o -> k ->
+  Tree n k v o -> k ->
+  Tree n k v o -> k ->
+  Tree n k v o ->
+  Tree (S (S n)) k v o
+branch5 a b c d e f g h i =
+  Branch2 (Branch2 a b c) d (Branch3 e f g h i)
+
+branch6 :
+  Tree n k v o -> k ->
+  Tree n k v o -> k ->
+  Tree n k v o -> k ->
+  Tree n k v o -> k ->
+  Tree n k v o -> k ->
+  Tree n k v o ->
+  Tree (S (S n)) k v o
+branch6 a b c d e f g h i j k =
+  Branch3 (Branch2 a b c) d (Branch2 e f g) h (Branch2 i j k)
+
+branch7 :
+  Tree n k v o -> k ->
+  Tree n k v o -> k ->
+  Tree n k v o -> k ->
+  Tree n k v o -> k ->
+  Tree n k v o -> k ->
+  Tree n k v o -> k ->
+  Tree n k v o ->
+  Tree (S (S n)) k v o
+branch7 a b c d e f g h i j k l m =
+  Branch3 (Branch3 a b c d e) f (Branch2 g h i) j (Branch2 k l m)
+
+merge1 : Tree n k v o -> k -> Tree (S n) k v o -> k -> Tree (S n) k v o -> Tree (S (S n)) k v o
+merge1 a b (Branch2 c d e) f (Branch2 g h i) = branch5 a b c d e f g h i
+merge1 a b (Branch2 c d e) f (Branch3 g h i j k) = branch6 a b c d e f g h i j k
+merge1 a b (Branch3 c d e f g) h (Branch2 i j k) = branch6 a b c d e f g h i j k
+merge1 a b (Branch3 c d e f g) h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m
+
+merge2 : Tree (S n) k v o -> k -> Tree n k v o -> k -> Tree (S n) k v o -> Tree (S (S n)) k v o
+merge2 (Branch2 a b c) d e f (Branch2 g h i) = branch5 a b c d e f g h i
+merge2 (Branch2 a b c) d e f (Branch3 g h i j k) = branch6 a b c d e f g h i j k
+merge2 (Branch3 a b c d e) f g h (Branch2 i j k) = branch6 a b c d e f g h i j k
+merge2 (Branch3 a b c d e) f g h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m
+
+merge3 : Tree (S n) k v o -> k -> Tree (S n) k v o -> k -> Tree n k v o -> Tree (S (S n)) k v o
+merge3 (Branch2 a b c) d (Branch2 e f g) h i = branch5 a b c d e f g h i
+merge3 (Branch2 a b c) d (Branch3 e f g h i) j k = branch6 a b c d e f g h i j k
+merge3 (Branch3 a b c d e) f (Branch2 g h i) j k = branch6 a b c d e f g h i j k
+merge3 (Branch3 a b c d e) f (Branch3 g h i j k) l m = branch7 a b c d e f g h i j k l m
+
+treeLookup : Ord k => k -> Tree n k v o -> Maybe v
+treeLookup k (Leaf k' v) =
+  if k == k' then
+    Just v
+  else
+    Nothing
+treeLookup k (Branch2 t1 k' t2) =
+  if k <= k' then
+    treeLookup k t1
+  else
+    treeLookup k t2
+treeLookup k (Branch3 t1 k1 t2 k2 t3) =
+  if k <= k1 then
+    treeLookup k t1
+  else if k <= k2 then
+    treeLookup k t2
+  else
+    treeLookup k t3
+
+treeInsert' : Ord k => k -> v -> Tree n k v o -> Either (Tree n k v o) (Tree n k v o, k, Tree n k v o)
+treeInsert' k v (Leaf k' v') =
+  case compare k k' of
+    LT => Right (Leaf k v, k, Leaf k' v')
+    EQ => Left (Leaf k v)
+    GT => Right (Leaf k' v', k', Leaf k v)
+treeInsert' k v (Branch2 t1 k' t2) =
+  if k <= k' then
+    case treeInsert' k v t1 of
+      Left t1' => Left (Branch2 t1' k' t2)
+      Right (a, b, c) => Left (Branch3 a b c k' t2)
+  else
+    case treeInsert' k v t2 of
+      Left t2' => Left (Branch2 t1 k' t2')
+      Right (a, b, c) => Left (Branch3 t1 k' a b c)
+treeInsert' k v (Branch3 t1 k1 t2 k2 t3) =
+  if k <= k1 then
+    case treeInsert' k v t1 of
+      Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
+      Right (a, b, c) => Right (Branch2 a b c, k1, Branch2 t2 k2 t3)
+  else
+    if k <= k2 then
+      case treeInsert' k v t2 of
+        Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
+        Right (a, b, c) => Right (Branch2 t1 k1 a, b, Branch2 c k2 t3)
+    else
+      case treeInsert' k v t3 of
+        Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
+        Right (a, b, c) => Right (Branch2 t1 k1 t2, k2, Branch2 a b c)
+
+treeInsert : Ord k => k -> v -> Tree n k v o -> Either (Tree n k v o) (Tree (S n) k v o)
+treeInsert k v t =
+  case treeInsert' k v t of
+    Left t' => Left t'
+    Right (a, b, c) => Right (Branch2 a b c)
+
+delType : Nat -> (k : Type) -> Type -> Ord k -> Type
+delType Z k v o = ()
+delType (S n) k v o = Tree n k v o
+
+treeDelete : Ord k => (n : Nat) -> k -> Tree n k v o -> Either (Tree n k v o) (delType n k v o)
+treeDelete _ k (Leaf k' v) =
+  if k == k' then
+    Right ()
+  else
+    Left (Leaf k' v)
+treeDelete (S Z) k (Branch2 t1 k' t2) =
+  if k <= k' then
+    case treeDelete Z k t1 of
+      Left t1' => Left (Branch2 t1' k' t2)
+      Right () => Right t2
+  else
+    case treeDelete Z k t2 of
+      Left t2' => Left (Branch2 t1 k' t2')
+      Right () => Right t1
+treeDelete (S Z) k (Branch3 t1 k1 t2 k2 t3) =
+  if k <= k1 then
+    case treeDelete Z k t1 of
+      Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
+      Right () => Left (Branch2 t2 k2 t3)
+  else if k <= k2 then
+    case treeDelete Z k t2 of
+      Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
+      Right () => Left (Branch2 t1 k1 t3)
+  else
+    case treeDelete Z k t3 of
+      Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
+      Right () => Left (Branch2 t1 k1 t2)
+treeDelete (S (S n)) k (Branch2 t1 k' t2) =
+  if k <= k' then
+    case treeDelete (S n) k t1 of
+      Left t1' => Left (Branch2 t1' k' t2)
+      Right t1' =>
+        case t2 of
+          Branch2 a b c => Right (Branch3 t1' k' a b c)
+          Branch3 a b c d e => Left (branch4 t1' k' a b c d e)
+  else
+    case treeDelete (S n) k t2 of
+      Left t2' => Left (Branch2 t1 k' t2')
+      Right t2' =>
+        case t1 of
+          Branch2 a b c => Right (Branch3 a b c k' t2')
+          Branch3 a b c d e => Left (branch4 a b c d e k' t2')
+treeDelete (S (S n)) k (Branch3 t1 k1 t2 k2 t3) =
+  if k <= k1 then
+    case treeDelete (S n) k t1 of
+      Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
+      Right t1' => Left (merge1 t1' k1 t2 k2 t3)
+  else if k <= k2 then
+    case treeDelete (S n) k t2 of
+      Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
+      Right t2' => Left (merge2 t1 k1 t2' k2 t3)
+  else
+    case treeDelete (S n) k t3 of
+      Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
+      Right t3' => Left (merge3 t1 k1 t2 k2 t3')
+
+treeToList : Tree n k v o -> List (k, v)
+treeToList = treeToList' (:: [])
+  where
+    -- explicit quantification to avoid conflation with {n} from treeToList
+    treeToList' : {0 n : Nat} -> ((k, v) -> List (k, v)) -> Tree n k v o -> List (k, v)
+    treeToList' cont (Leaf k v) = cont (k, v)
+    treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1
+    treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1
+
+export
+data SortedMap : Type -> Type -> Type where
+  Empty : Ord k => SortedMap k v
+  M : (o : Ord k) => (n:Nat) -> Tree n k v o -> SortedMap k v
+
+export
+empty : Ord k => SortedMap k v
+empty = Empty
+
+export
+lookup : k -> SortedMap k v -> Maybe v
+lookup _ Empty = Nothing
+lookup k (M _ t) = treeLookup k t
+
+export
+insert : k -> v -> SortedMap k v -> SortedMap k v
+insert k v Empty = M Z (Leaf k v)
+insert k v (M _ t) =
+  case treeInsert k v t of
+    Left t' => (M _ t')
+    Right t' => (M _ t')
+
+export
+singleton : Ord k => k -> v -> SortedMap k v
+singleton k v = insert k v empty
+
+export
+insertFrom : Foldable f => f (k, v) -> SortedMap k v -> SortedMap k v
+insertFrom = flip $ foldl $ flip $ uncurry insert
+
+export
+delete : k -> SortedMap k v -> SortedMap k v
+delete _ Empty = Empty
+delete k (M Z t) =
+  case treeDelete Z k t of
+    Left t' => (M _ t')
+    Right () => Empty
+delete k (M (S n) t) =
+  case treeDelete (S n) k t of
+    Left t' => (M _ t')
+    Right t' => (M _ t')
+
+export
+fromList : Ord k => List (k, v) -> SortedMap k v
+fromList l = foldl (flip (uncurry insert)) empty l
+
+export
+toList : SortedMap k v -> List (k, v)
+toList Empty = []
+toList (M _ t) = treeToList t
+
+||| Gets the keys of the map.
+export
+keys : SortedMap k v -> List k
+keys = map fst . toList
+
+||| Gets the values of the map. Could contain duplicates.
+export
+values : SortedMap k v -> List v
+values = map snd . toList
+
+treeMap : (a -> b) -> Tree n k a o -> Tree n k b o
+treeMap f (Leaf k v) = Leaf k (f v)
+treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
+treeMap f (Branch3 t1 k1 t2 k2 t3)
+    = Branch3 (treeMap f t1) k1 (treeMap f t2) k2 (treeMap f t3)
+
+treeTraverse : Applicative f => (a -> f b) -> Tree n k a o -> f (Tree n k b o)
+treeTraverse f (Leaf k v) = Leaf k <$> f v
+treeTraverse f (Branch2 t1 k t2) =
+  Branch2
+    <$> treeTraverse f t1
+    <*> pure k
+    <*> treeTraverse f t2
+treeTraverse f (Branch3 t1 k1 t2 k2 t3) =
+  Branch3
+    <$> treeTraverse f t1
+    <*> pure k1
+    <*> treeTraverse f t2
+    <*> pure k2
+    <*> treeTraverse f t3
+
+export
+implementation Functor (SortedMap k) where
+  map _ Empty = Empty
+  map f (M n t) = M _ (treeMap f t)
+
+export
+implementation Foldable (SortedMap k) where
+  foldr f z = foldr f z . values
+
+  null Empty = True
+  null (M _ _) = False
+
+export
+implementation Traversable (SortedMap k) where
+  traverse _ Empty = pure Empty
+  traverse f (M n t) = M _ <$> treeTraverse f t
+
+||| Merge two maps. When encountering duplicate keys, using a function to combine the values.
+||| Uses the ordering of the first map given.
+export
+mergeWith : (v -> v -> v) -> SortedMap k v -> SortedMap k v -> SortedMap k v
+mergeWith f x y = insertFrom inserted x where
+  inserted : List (k, v)
+  inserted = do
+    (k, v) <- toList y
+    let v' = (maybe id f $ lookup k x) v
+    pure (k, v')
+
+||| Merge two maps using the Semigroup (and by extension, Monoid) operation.
+||| Uses mergeWith internally, so the ordering of the left map is kept.
+export
+merge : Semigroup v => SortedMap k v -> SortedMap k v -> SortedMap k v
+merge = mergeWith (<+>)
+
+||| Left-biased merge, also keeps the ordering specified  by the left map.
+export
+mergeLeft : SortedMap k v -> SortedMap k v -> SortedMap k v
+mergeLeft = mergeWith const
+
+export
+(Show k, Show v) => Show (SortedMap k v) where
+   show m = "fromList " ++ (show $ toList m)
+
+-- TODO: is this the right variant of merge to use for this? I think it is, but
+-- I could also see the advantages of using `mergeLeft`. The current approach is
+-- strictly more powerful I believe, because `mergeLeft` can be emulated with
+-- the `First` monoid. However, this does require more code to do the same
+-- thing.
+export
+Semigroup v => Semigroup (SortedMap k v) where
+  (<+>) = merge
+
+||| For `neutral <+> y`, y is rebuilt in `Ord k`, so this is not a "strict" Monoid.
+||| However, semantically, it should be equal.
+export
+(Ord k, Semigroup v) => Monoid (SortedMap k v) where
+  neutral = empty

src/Libraries/Data/SortedSet.idr

@@ -0,0 +1,73 @@
+module Libraries.Data.SortedSet
+
+import Data.Maybe
+import Libraries.Data.SortedMap
+
+export
+data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())
+
+export
+empty : Ord k => SortedSet k
+empty = SetWrapper Data.SortedMap.empty
+
+export
+insert : k -> SortedSet k -> SortedSet k
+insert k (SetWrapper m) = SetWrapper (Data.SortedMap.insert k () m)
+
+export
+delete : k -> SortedSet k -> SortedSet k
+delete k (SetWrapper m) = SetWrapper (Data.SortedMap.delete k m)
+
+export
+contains : k -> SortedSet k -> Bool
+contains k (SetWrapper m) = isJust (Data.SortedMap.lookup k m)
+
+export
+fromList : Ord k => List k -> SortedSet k
+fromList l = SetWrapper (Data.SortedMap.fromList (map (\i => (i, ())) l))
+
+export
+toList : SortedSet k -> List k
+toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)
+
+export
+Foldable SortedSet where
+  foldr f e xs = foldr f e (Data.SortedSet.toList xs)
+
+  null (SetWrapper m) = null m
+
+||| Set union. Inserts all elements of x into y
+export
+union : (x, y : SortedSet k) -> SortedSet k
+union x y = foldr insert x y
+
+||| Set difference. Delete all elments in y from x
+export
+difference : (x, y : SortedSet k) -> SortedSet k
+difference x y = foldr delete x y
+
+||| Set symmetric difference. Uses the union of the differences.
+export
+symDifference : (x, y : SortedSet k) -> SortedSet k
+symDifference x y = union (difference x y) (difference y x)
+
+||| Set intersection. Implemented as the difference of the union and the symetric difference.
+export
+intersection : (x, y : SortedSet k) -> SortedSet k
+intersection x y = difference x (difference x y)
+
+export
+Ord k => Semigroup (SortedSet k) where
+  (<+>) = union
+
+export
+Ord k => Monoid (SortedSet k) where
+  neutral = empty
+
+export
+keySet : SortedMap k v -> SortedSet k
+keySet = SetWrapper . map (const ())
+
+export
+singleton : Ord k => k -> SortedSet k
+singleton k = insert k empty

src/Libraries/Data/String/Extra.idr

@@ -0,0 +1,104 @@
+module Libraries.Data.String.Extra
+
+import Data.List
+import Data.Nat
+import Data.Strings
+
+%default total
+
+
+infixl 5 +>
+infixr 5 <+
+
+||| Adds a character to the end of the specified string.
+|||
+||| ```idris example
+||| strSnoc "AB" 'C'
+||| ```
+||| ```idris example
+||| strSnoc "" 'A'
+||| ```
+public export
+strSnoc : String -> Char -> String
+strSnoc s c = s ++ (singleton c)
+
+||| Alias of `strSnoc`
+|||
+||| ```idris example
+||| "AB" +> 'C'
+||| ```
+public export
+(+>) : String -> Char -> String
+(+>) = strSnoc
+
+||| Alias of `strCons`
+|||
+||| ```idris example
+||| 'A' <+ "AB"
+||| ```
+public export
+(<+) : Char -> String -> String
+(<+) = strCons
+
+||| Take the first `n` characters from a string. Returns the whole string
+||| if it's too short.
+public export
+take : (n : Nat) -> (input : String) -> String
+take n str = substr Z n str
+
+||| Take the last `n` characters from a string. Returns the whole string
+||| if it's too short.
+public export
+takeLast : (n : Nat) -> (input : String) -> String
+takeLast n str with (length str)
+  takeLast n str | len with (isLTE n len)
+    takeLast n str | len | Yes prf = substr (len `minus` n) len str
+    takeLast n str | len | No contra = str
+
+||| Remove the first `n` characters from a string. Returns the empty string if
+||| the input string is too short.
+public export
+drop : (n : Nat) -> (input : String) -> String
+drop n str = substr n (length str) str
+
+||| Remove the last `n` characters from a string. Returns the empty string if
+||| the input string is too short.
+public export
+dropLast : (n : Nat) -> (input : String) -> String
+dropLast n str = reverse (drop n (reverse str))
+
+||| Remove the first and last `n` characters from a string. Returns the empty
+||| string if the input string is too short.
+public export
+shrink : (n : Nat) -> (input : String) -> String
+shrink n str = dropLast n (drop n str)
+
+||| Concatenate the strings from a `Foldable` containing strings, separated by
+||| the given string.
+public export
+join : (sep : String) -> Foldable t => (xs : t String) -> String
+join sep xs = drop (length sep)
+                   (foldl (\acc, x => acc ++ sep ++ x) "" xs)
+
+||| Get a character from a string if the string is long enough.
+public export
+index : (n : Nat) -> (input : String) -> Maybe Char
+index n str with (unpack str)
+  index n str | [] = Nothing
+  index Z str | (x :: xs) = Just x
+  index (S n) str | (x :: xs) = index n str | xs
+
+||| Produce a string by repeating the character `c` `n` times.
+public export
+replicate : (n : Nat) -> (c : Char) -> String
+replicate n c = pack $ replicate n c
+
+||| Indent a given string by `n` spaces.
+public export
+indent : (n : Nat) -> String -> String
+indent n x = replicate n ' ' ++ x
+
+||| Indent each line of a given string by `n` spaces.
+public export
+indentLines : (n : Nat) -> String -> String
+indentLines n str = unlines $ map (indent n) $ lines str

src/Libraries/Data/String/Iterator.idr

@@ -0,0 +1,74 @@
+module Libraries.Data.String.Iterator
+
+import public Libraries.Data.List.Lazy
+
+%default total
+
+-- Backend-dependent string iteration type,
+-- parameterised by the string that it iterates over.
+--
+-- Beware: the index is checked only up to definitional equality.
+-- In theory, you could run `decEq` on two strings
+-- with the same content but allocated in different memory locations
+-- and use the obtained Refl to coerce iterators between them.
+--
+-- The strictly correct solution is to make the iterators independent
+-- from the exact memory location of the string given to `uncons`.
+-- (For example, byte offsets satisfy this requirement.)
+export
+data StringIterator : String -> Type where [external]
+
+-- This function is private
+-- to avoid subverting the linearity guarantees of withString.
+%foreign
+  "scheme:blodwen-string-iterator-new"
+  "javascript:stringIterator:new"
+private
+fromString : (str : String) -> StringIterator str
+
+-- This function uses a linear string iterator
+-- so that backends can use mutating iterators.
+export
+withString : (str : String) -> ((1 it : StringIterator str) -> a) -> a
+withString str f = f (fromString str)
+
+-- We use a custom data type instead of Maybe (Char, StringIterator)
+-- to remove one level of pointer indirection
+-- in every iteration of something that's likely to be a hot loop,
+-- and to avoid one allocation per character.
+--
+-- The Char field of Character is unrestricted for flexibility.
+public export
+data UnconsResult : String -> Type where
+  EOF : UnconsResult str
+  Character : (c : Char) -> (1 it : StringIterator str) -> UnconsResult str
+
+-- We pass the whole string to the uncons function
+-- to avoid yet another allocation per character
+-- because for many backends, StringIterator can be simply an integer
+-- (e.g. byte offset into an UTF-8 string).
+%foreign
+  "scheme:blodwen-string-iterator-next"
+  "javascript:stringIterator:next"
+export
+uncons : (str : String) -> (1 it : StringIterator str) -> UnconsResult str
+
+export
+foldl : (accTy -> Char -> accTy) -> accTy -> String -> accTy
+foldl op acc str = withString str (loop acc)
+  where
+    loop : accTy -> (1 it : StringIterator str) -> accTy
+    loop acc it =
+      case uncons str it of
+        EOF => acc
+        Character c it' => loop (acc `op` c) (assert_smaller it it')
+
+export
+unpack : String -> LazyList Char
+unpack str = withString str unpack'
+  where
+    unpack' : (1 it : StringIterator str) -> LazyList Char
+    unpack' it =
+      case uncons str it of
+        EOF => []
+        Character c it' => c :: Delay (unpack' $ assert_smaller it it')

src/Libraries/Data/StringMap.idr

@@ -1,4 +1,4 @@
-module Data.StringMap
+module Libraries.Data.StringMap
 
 -- Hand specialised map, for efficiency...
 

src/Libraries/Data/StringTrie.idr

@@ -1,7 +1,7 @@
-module Data.StringTrie
+module Libraries.Data.StringTrie
 
 import Data.These
-import Data.StringMap
+import Libraries.Data.StringMap
 
 %default total
 

src/Libraries/Text/Bounded.idr

@@ -1,4 +1,4 @@
-module Text.Bounded
+module Libraries.Text.Bounded
 
 %default total
 

src/Libraries/Text/Lexer.idr

@@ -1,12 +1,12 @@
-module Text.Lexer
+module Libraries.Text.Lexer
 
-import Data.Bool.Extra
+import Libraries.Data.Bool.Extra
 import Data.List
 import Data.Nat
 
-import public Text.Lexer.Core
-import public Text.Quantity
-import public Text.Token
+import public Libraries.Text.Lexer.Core
+import public Libraries.Text.Quantity
+import public Libraries.Text.Token
 
 %default total
 

src/Libraries/Text/Lexer/Core.idr

@@ -1,12 +1,12 @@
-module Text.Lexer.Core
+module Libraries.Text.Lexer.Core
 
-import public Control.Delayed
-import Data.Bool.Extra
+import public Libraries.Control.Delayed
+import Libraries.Data.Bool.Extra
 import Data.List
 import Data.Maybe
 import Data.Nat
 import Data.Strings
-import public Text.Bounded
+import public Libraries.Text.Bounded
 
 %default total
 

src/Libraries/Text/Literate.idr

@@ -21,9 +21,9 @@
 ||| the markers within the document's main text: This will confuse the
 ||| lexer.
 |||
-module Text.Literate
+module Libraries.Text.Literate
 
-import Text.Lexer
+import Libraries.Text.Lexer
 
 import Data.List
 import Data.List.Views

src/Libraries/Text/Parser.idr

@@ -1,12 +1,12 @@
-module Text.Parser
+module Libraries.Text.Parser
 
-import Data.Bool.Extra
+import Libraries.Data.Bool.Extra
 import Data.List
 import Data.Nat
 
-import public Text.Parser.Core
-import public Text.Quantity
-import public Text.Token
+import public Libraries.Text.Parser.Core
+import public Libraries.Text.Quantity
+import public Libraries.Text.Token
 
 %default total
 

src/Libraries/Text/Parser/Core.idr

@@ -1,9 +1,9 @@
-module Text.Parser.Core
+module Libraries.Text.Parser.Core
 
-import Data.Bool.Extra
+import Libraries.Data.Bool.Extra
 import Data.List
-import public Control.Delayed
-import public Text.Bounded
+import public Libraries.Control.Delayed
+import public Libraries.Text.Bounded
 
 %default total
 

src/Libraries/Text/PrettyPrint/Prettyprinter.idr

@@ -0,0 +1,12 @@
+||| A Idris port of the prettyprinter library [1] and
+||| the ANSI terminal backend [2].
+|||
+||| [1] https://hackage.haskell.org/package/prettyprinter
+||| [2] https://hackage.haskell.org/package/prettyprinter-ansi-terminal
+
+module Libraries.Text.PrettyPrint.Prettyprinter
+
+import public Libraries.Text.PrettyPrint.Prettyprinter.Doc
+import public Libraries.Text.PrettyPrint.Prettyprinter.Symbols
+
+%default total

src/Libraries/Text/PrettyPrint/Prettyprinter/Doc.idr

@@ -0,0 +1,750 @@
+module Libraries.Text.PrettyPrint.Prettyprinter.Doc
+
+import Data.List
+import Data.Maybe
+import Data.Strings
+import Libraries.Data.String.Extra
+
+%default total
+
+export
+textSpaces : Int -> String
+textSpaces n = replicate (integerToNat $ cast n) ' '
+
+||| Maximum number of characters that fit in one line.
+public export
+data PageWidth : Type where
+  ||| The `Int` is the number of characters, including whitespace, that fit in a line.
+  ||| The `Double` is the ribbon, the fraction of the toal page width that can be printed on.
+  AvailablePerLine : Int -> Double -> PageWidth
+  ||| The layouters should not introduce line breaks.
+  Unbounded : PageWidth
+
+data FlattenResult : Type -> Type where
+  Flattened : a -> FlattenResult a
+  AlreadyFlat : FlattenResult a
+  NeverFlat : FlattenResult a
+
+Functor FlattenResult where
+  map f (Flattened a) = Flattened (f a)
+  map _ AlreadyFlat = AlreadyFlat
+  map _ NeverFlat = NeverFlat
+
+||| Fusion depth parameter.
+public export
+data FusionDepth : Type where
+  ||| Do not dive deep into nested documents.
+  Shallow : FusionDepth
+  ||| Recurse into all parts of the `Doc`. May impact performace.
+  Deep : FusionDepth
+
+||| This data type represents pretty documents that have
+||| been annotated with an arbitrary data type `ann`.
+public export
+data Doc : Type -> Type where
+  Empty : Doc ann
+  Chara : (c : Char) -> Doc ann                         -- Invariant: not '\n'
+  Text : (len : Int) -> (text : String) -> Doc ann      -- Invariant: at least two characters long and no '\n'
+  Line : Doc ann
+  FlatAlt : Lazy (Doc ann) -> Lazy (Doc ann) -> Doc ann
+  Cat : Doc ann -> Doc ann -> Doc ann
+  Nest : (i : Int) -> Doc ann -> Doc ann
+  Union : Lazy (Doc ann) -> Lazy (Doc ann) -> Doc ann   -- Invariant: the first line of the first document should be
+                                                        -- longer than the first lines of the second one
+  Column : (Int -> Doc ann) -> Doc ann
+  WithPageWidth : (PageWidth -> Doc ann) -> Doc ann
+  Nesting : (Int -> Doc ann) -> Doc ann
+  Annotated : ann -> Doc ann -> Doc ann
+
+export
+Semigroup (Doc ann) where
+  (<+>) = Cat
+
+export
+Monoid (Doc ann) where
+  neutral = Empty
+
+||| Layout a document depending on which column it starts at.
+export
+column : (Int -> Doc ann) -> Doc ann
+column = Column
+
+||| Lays out a document with the current nesting level increased by `i`.
+export
+nest : Int -> Doc ann -> Doc ann
+nest 0 x = x
+nest i x = Nest i x
+
+||| Layout a document depending on the current nesting level.
+export
+nesting : (Int -> Doc ann) -> Doc ann
+nesting = Nesting
+
+||| Lays out a document, and makes the column width of it available to a function.
+export
+width : Doc ann -> (Int -> Doc ann) -> Doc ann
+width doc f = column (\colStart => doc <+> column (\colEnd => f (colEnd - colStart)))
+
+||| Layout a document depending on the page width, if one has been specified.
+export
+pageWidth : (PageWidth -> Doc ann) -> Doc ann
+pageWidth = WithPageWidth
+
+||| Lays out a document with the nesting level set to the current column.
+export
+align : Doc ann -> Doc ann
+align d = column (\k => nesting (\i => nest (k - i) d))
+
+||| Lays out a document with a nesting level set to the current column plus `i`.
+||| Negative values are allowed, and decrease the nesting level accordingly.
+export
+hang : Int -> Doc ann -> Doc ann
+hang i d = align (nest i d)
+
+||| Insert a number of spaces.
+export
+spaces : Int -> Doc ann
+spaces n = if n <= 0
+              then Empty
+              else if n == 1
+                      then Chara ' '
+                      else Text n (textSpaces n)
+
+||| Indents a document with `i` spaces, starting from the current cursor position.
+export
+indent : Int -> Doc ann -> Doc ann
+indent i d = hang i (spaces i <+> d)
+
+||| Lays out a document. It then appends spaces until the width is equal to `i`.
+||| If the width is already larger, nothing is appended.
+export
+fill : Int -> Doc ann -> Doc ann
+fill n doc = width doc (\w => spaces $ n - w)
+
+infixr 6 <++>
+||| Concatenates two documents with a space in between.
+export
+(<++>) : Doc ann -> Doc ann -> Doc ann
+x <++> y = x <+> Chara ' ' <+> y
+
+||| The empty document behaves like `pretty ""`, so it has a height of 1.
+export
+emptyDoc : Doc ann
+emptyDoc = Empty
+
+||| Behaves like `space` if the resulting output fits the page, otherwise like `line`.
+export
+softline : Doc ann
+softline = Union (Chara ' ') Line
+
+||| Like `softline`, but behaves like `neutral` if the resulting output does not fit
+||| on the page.
+export
+softline' : Doc ann
+softline' = Union neutral Line
+
+||| A line break, even when grouped.
+export
+hardline : Doc ann
+hardline = Line
+
+flatten : Doc ann -> Doc ann
+flatten Empty = Empty
+flatten (Chara x) = Chara x
+flatten (Text len x) = Text len x
+flatten Line = Empty
+flatten (FlatAlt _ y) = flatten y
+flatten (Cat x y) = Cat (flatten x) (flatten y)
+flatten (Nest i x) = Nest i (flatten x)
+flatten (Union x _) = flatten x
+flatten (Column f) = Column (\x => flatten $ f x)
+flatten (WithPageWidth f) = WithPageWidth (\x => flatten $ f x)
+flatten (Nesting f) = Nesting (\x => flatten $ f x)
+flatten (Annotated ann x) = Annotated ann (flatten x)
+
+changesUponFlattening : Doc ann -> FlattenResult (Doc ann)
+changesUponFlattening Empty = AlreadyFlat
+changesUponFlattening (Chara x) = AlreadyFlat
+changesUponFlattening (Text x y) = AlreadyFlat
+changesUponFlattening Line = NeverFlat
+changesUponFlattening (FlatAlt _ y) = Flattened (flatten y)
+changesUponFlattening (Cat x y) = case (changesUponFlattening x, changesUponFlattening y) of
+  (NeverFlat, _) => NeverFlat
+  (_, NeverFlat) => NeverFlat
+  (Flattened x', Flattened y') => Flattened (Cat x' y')
+  (Flattened x', AlreadyFlat) => Flattened (Cat x' y)
+  (AlreadyFlat , Flattened y') => Flattened (Cat x y')
+  (AlreadyFlat , AlreadyFlat) => AlreadyFlat
+changesUponFlattening (Nest i x) = map (Nest i) (changesUponFlattening x)
+changesUponFlattening (Union x _) = Flattened x
+changesUponFlattening (Column f) = Flattened (Column (flatten . f))
+changesUponFlattening (WithPageWidth f) = Flattened (WithPageWidth (flatten . f))
+changesUponFlattening (Nesting f) = Flattened (Nesting (flatten . f))
+changesUponFlattening (Annotated ann x) = map (Annotated ann) (changesUponFlattening x)
+
+||| Tries laying out a document into a single line by removing the contained
+||| line breaks; if this does not fit the page, or has an `hardline`, the document
+||| is laid out without changes.
+export
+group : Doc ann -> Doc ann
+group (Union x y) = Union x y
+group (FlatAlt x y) = case changesUponFlattening y of
+  Flattened y' => Union y' x
+  AlreadyFlat => Union y x
+  NeverFlat => x
+group x = case changesUponFlattening x of
+  Flattened x' => Union x' x
+  AlreadyFlat => x
+  NeverFlat => x
+
+||| By default renders the first document, When grouped renders the second, with
+||| the first as fallback when there is not enough space.
+export
+flatAlt : Lazy (Doc ann) -> Lazy (Doc ann) -> Doc ann
+flatAlt = FlatAlt
+
+||| Advances to the next line and indents to the current nesting level.
+export
+line : Doc ann
+line = FlatAlt Line (Chara ' ')
+
+||| Like `line`, but behaves like `neutral` if the line break is undone by `group`.
+export
+line' : Doc ann
+line' = FlatAlt Line Empty
+
+||| First lays out the document. It then appends spaces until the width is equal to `i`.
+||| If the width is already larger than `i`, the nesting level is decreased by `i`
+||| and a line is appended.
+export
+fillBreak : Int -> Doc ann -> Doc ann
+fillBreak f x  = width x (\w => if w > f
+                                   then nest f line'
+                                   else spaces $ f - w)
+
+||| Concatenate all documents element-wise with a binary function.
+export
+concatWith : (Doc ann -> Doc ann -> Doc ann) -> List (Doc ann) -> Doc ann
+concatWith f [] = neutral
+concatWith f (x :: xs) = foldl f x xs
+
+||| Concatenates all documents horizontally with `(<++>)`.
+export
+hsep : List (Doc ann) -> Doc ann
+hsep = concatWith (<++>)
+
+||| Concatenates all documents above each other. If a `group` undoes the line breaks,
+||| the documents are separated with a space instead.
+export
+vsep : List (Doc ann) -> Doc ann
+vsep = concatWith (\x, y => x <+> line <+> y)
+
+||| Concatenates the documents horizontally with `(<++>)` as long as it fits the page,
+||| then inserts a line and continues.
+export
+fillSep : List (Doc ann) -> Doc ann
+fillSep = concatWith (\x, y => x <+> softline <+> y)
+
+||| Tries laying out the documents separated with spaces and if this does not fit,
+||| separates them with newlines.
+export
+sep : List (Doc ann) -> Doc ann
+sep = group . vsep
+
+||| Concatenates all documents horizontally with `(<+>)`.
+export
+hcat : List (Doc ann) -> Doc ann
+hcat = concatWith (<+>)
+
+||| Vertically concatenates the documents. If it is grouped, the line breaks are removed.
+export
+vcat : List (Doc ann) -> Doc ann
+vcat = concatWith (\x, y => x <+> line' <+> y)
+
+||| Concatenates documents horizontally with `(<+>)` as log as it fits the page, then
+||| inserts a line and continues.
+export
+fillCat : List (Doc ann) -> Doc ann
+fillCat = concatWith (\x, y => x <+> softline' <+> y)
+
+||| Tries laying out the documents separated with nothing, and if it does not fit the page,
+||| separates them with newlines.
+export
+cat : List (Doc ann) -> Doc ann
+cat = group . vcat
+
+||| Appends `p` to all but the last document.
+export
+punctuate : Doc ann -> List (Doc ann) -> List (Doc ann)
+punctuate _ [] = []
+punctuate _ [d] = [d]
+punctuate p (d :: ds) = (d <+> p) :: punctuate p ds
+
+export
+plural : (Num amount, Eq amount) => doc -> doc -> amount -> doc
+plural one multiple n = if n == 1 then one else multiple
+
+||| Encloses the document between two other documents using `(<+>)`.
+export
+enclose : Doc ann -> Doc ann -> Doc ann -> Doc ann
+enclose l r x = l <+> x <+> r
+
+||| Reordering of `encloses`.
+||| Example: concatWith (surround (pretty ".")) [pretty "Text", pretty "PrettyPrint", pretty "Doc"]
+|||          Text.PrettyPrint.Doc
+export
+surround : Doc ann -> Doc ann -> Doc ann -> Doc ann
+surround x l r = l <+> x <+> r
+
+||| Concatenates the documents separated by `s` and encloses the resulting document by `l` and `r`.
+export
+encloseSep : Doc ann -> Doc ann -> Doc ann -> List (Doc ann) -> Doc ann
+encloseSep l r s []  = l <+> r
+encloseSep l r s [d] = l <+> d <+> r
+encloseSep l r s ds  = cat (zipWith (<+>) (l :: replicate (length ds `minus` 1) s) ds) <+> r
+
+unsafeTextWithoutNewLines : String -> Doc ann
+unsafeTextWithoutNewLines str = case strM str of
+  StrNil => Empty
+  StrCons c cs => if cs == ""
+                     then Chara c
+                     else Text (cast $ length str) str
+
+||| Adds an annotation to a document.
+export
+annotate : ann -> Doc ann -> Doc ann
+annotate = Annotated
+
+||| Changes the annotations of a document. Individual annotations can be removed,
+||| changed, or replaced by multiple ones.
+export
+alterAnnotations : (ann -> List ann') -> Doc ann -> Doc ann'
+alterAnnotations re Empty = Empty
+alterAnnotations re (Chara c) = Chara c
+alterAnnotations re (Text l t) = Text l t
+alterAnnotations re Line = Line
+alterAnnotations re (FlatAlt x y) = FlatAlt (alterAnnotations re x) (alterAnnotations re y)
+alterAnnotations re (Cat x y) = Cat (alterAnnotations re x) (alterAnnotations re y)
+alterAnnotations re (Nest i x) = Nest i (alterAnnotations re x)
+alterAnnotations re (Union x y) = Union (alterAnnotations re x) (alterAnnotations re y)
+alterAnnotations re (Column f) = Column (\x => alterAnnotations re $ f x)
+alterAnnotations re (WithPageWidth f) = WithPageWidth (\x => alterAnnotations re $ f x)
+alterAnnotations re (Nesting f) = Nesting (\x => alterAnnotations re $ f x)
+alterAnnotations re (Annotated ann x) = foldr Annotated (alterAnnotations re x) (re ann)
+
+||| Removes all annotations.
+export
+unAnnotate : Doc ann -> Doc xxx
+unAnnotate = alterAnnotations (const [])
+
+||| Changes the annotations of a document.
+export
+reAnnotate : (ann -> ann') -> Doc ann -> Doc ann'
+reAnnotate re = alterAnnotations (pure . re)
+
+||| Alter the document's annotations.
+export
+Functor Doc where
+  map = reAnnotate
+
+||| Overloaded converison to `Doc`.
+public export
+interface Pretty a where
+  pretty : a -> Doc ann
+  pretty x = prettyPrec Open x
+
+  prettyPrec : Prec -> a -> Doc ann
+  prettyPrec _ x = pretty x
+
+export
+Pretty String where
+  pretty = vsep . map unsafeTextWithoutNewLines . lines
+
+public export
+FromString (Doc ann) where
+  fromString = pretty
+
+||| Variant of `encloseSep` with braces and comma as separator.
+export
+list : List (Doc ann) -> Doc ann
+list = group . encloseSep (flatAlt (pretty "[ ") (pretty "["))
+                          (flatAlt (pretty " ]") (pretty "]"))
+                          (pretty ", ")
+
+||| Variant of `encloseSep` with parentheses and comma as separator.
+export
+tupled : List (Doc ann) -> Doc ann
+tupled = group . encloseSep (flatAlt (pretty "( ") (pretty "("))
+                            (flatAlt (pretty " )") (pretty ")"))
+                            (pretty ", ")
+
+export
+Pretty a => Pretty (List a) where
+  pretty = align . list . map pretty
+
+export
+[prettyListMaybe] Pretty a => Pretty (List (Maybe a)) where
+  pretty = pretty . catMaybes
+    where catMaybes : List (Maybe a) -> List a
+          catMaybes [] = []
+          catMaybes (Nothing :: xs) = catMaybes xs
+          catMaybes ((Just x) :: xs) = x :: catMaybes xs
+
+export
+Pretty () where
+  pretty _ = pretty "()"
+
+export
+Pretty Bool where
+  pretty True = pretty "True"
+  pretty False = pretty "False"
+
+export
+Pretty Char where
+  pretty '\n' = line
+  pretty c = Chara c
+
+export Pretty Nat where pretty = unsafeTextWithoutNewLines . show
+export Pretty Int where pretty = unsafeTextWithoutNewLines . show
+export Pretty Integer where pretty = unsafeTextWithoutNewLines . show
+export Pretty Double where pretty = unsafeTextWithoutNewLines . show
+export Pretty Bits8 where pretty = unsafeTextWithoutNewLines . show
+export Pretty Bits16 where pretty = unsafeTextWithoutNewLines . show
+export Pretty Bits32 where pretty = unsafeTextWithoutNewLines . show
+export Pretty Bits64 where pretty = unsafeTextWithoutNewLines . show
+
+export
+(Pretty a, Pretty b) => Pretty (a, b) where
+  pretty (x, y) = tupled [pretty x, pretty y]
+
+export
+Pretty a => Pretty (Maybe a) where
+  pretty = maybe neutral pretty
+
+||| Combines text nodes so they can be rendered more efficiently.
+export
+fuse : FusionDepth -> Doc ann -> Doc ann
+fuse depth (Cat Empty x) = fuse depth x
+fuse depth (Cat x Empty) = fuse depth x
+fuse depth (Cat (Chara c1) (Chara c2)) = Text 2 (strCons c1 (strCons c2 ""))
+fuse depth (Cat (Text lt t) (Chara c)) = Text (lt + 1) (t ++ singleton c)
+fuse depth (Cat (Chara c) (Text lt t)) = Text (lt + 1) (strCons c t)
+fuse depth (Cat (Text l1 t1) (Text l2 t2)) = Text (l1 + l2) (t1 ++ t2)
+fuse depth (Cat (Chara x) (Cat (Chara y) z)) =
+  let sub = Text 2 (strCons x (strCons y "")) in
+      fuse depth $ assert_smaller (Cat (Chara x) (Cat (Chara y) z)) (Cat sub z)
+fuse depth (Cat (Text lx x) (Cat (Chara y) z)) =
+  let sub = Text (lx + 1) (x ++ singleton y) in
+      fuse depth $ assert_smaller (Cat (Text lx x) (Cat (Chara y) z)) (Cat sub z)
+fuse depth (Cat (Chara x) (Cat (Text ly y) z)) =
+  let sub = Text (ly + 1) (strCons x y) in
+      fuse depth $ assert_smaller (Cat (Chara x) (Cat (Text ly y) z)) (Cat sub z)
+fuse depth (Cat (Text lx x) (Cat (Text ly y) z)) =
+  let sub = Text (lx + ly) (x ++ y) in
+      fuse depth $ assert_smaller (Cat (Text lx x) (Cat (Text ly y) z)) (Cat sub z)
+fuse depth (Cat (Cat x (Chara y)) z) =
+  let sub = fuse depth (Cat (Chara y) z) in
+      assert_total $ fuse depth (Cat x sub)
+fuse depth (Cat (Cat x (Text ly y)) z) =
+  let sub = fuse depth (Cat (Text ly y) z) in
+      assert_total $ fuse depth (Cat x sub)
+fuse depth (Cat x y) = Cat (fuse depth x) (fuse depth y)
+fuse depth (Nest i (Nest j x)) = fuse depth $ assert_smaller (Nest i (Nest j x)) (Nest (i + j) x)
+fuse depth (Nest _ Empty) = Empty
+fuse depth (Nest _ (Text lx x)) = Text lx x
+fuse depth (Nest _ (Chara x)) = Chara x
+fuse depth (Nest 0 x) = fuse depth x
+fuse depth (Nest i x) = Nest i (fuse depth x)
+fuse depth (Annotated ann x) = Annotated ann (fuse depth x)
+fuse depth (FlatAlt x y) = FlatAlt (fuse depth x) (fuse depth y)
+fuse depth (Union x y) = Union (fuse depth x) (fuse depth y)
+fuse Shallow (Column f) = Column f
+fuse depth (Column f) = Column (\x => fuse depth $ f x)
+fuse Shallow (WithPageWidth f) = WithPageWidth f
+fuse depth (WithPageWidth f) = WithPageWidth (\x => fuse depth $ f x)
+fuse Shallow (Nesting f) = Nesting f
+fuse depth (Nesting f) = Nesting (\x => fuse depth $ f x)
+fuse depth x = x
+
+||| This data type represents laid out documents and is used by the display functions.
+public export
+data SimpleDocStream : Type -> Type where
+  SEmpty : SimpleDocStream ann
+  SChar : (c : Char) -> (rest : Lazy (SimpleDocStream ann)) -> SimpleDocStream ann
+  SText : (len : Int) -> (text : String) -> (rest : Lazy (SimpleDocStream ann)) -> SimpleDocStream ann
+  SLine : (i : Int) -> (rest : SimpleDocStream ann) -> SimpleDocStream ann
+  SAnnPush : ann -> (rest : SimpleDocStream ann) -> SimpleDocStream ann
+  SAnnPop : (rest : SimpleDocStream ann) -> SimpleDocStream ann
+
+internalError : SimpleDocStream ann
+internalError = let msg = "<internal pretty printing error>" in
+                    SText (cast $ length msg) msg SEmpty
+
+data AnnotationRemoval = Remove | DontRemove
+
+||| Changes the annotation of a document to a different annotation or none.
+export
+alterAnnotationsS : (ann -> Maybe ann') -> SimpleDocStream ann -> SimpleDocStream ann'
+alterAnnotationsS re = fromMaybe internalError . go []
+  where
+    go : List AnnotationRemoval -> SimpleDocStream ann -> Maybe (SimpleDocStream ann')
+    go stack SEmpty = pure SEmpty
+    go stack (SChar c rest) = SChar c . delay <$> go stack rest
+    go stack (SText l t rest) = SText l t . delay <$> go stack rest
+    go stack (SLine l rest) = SLine l <$> go stack rest
+    go stack (SAnnPush ann rest) = case re ann of
+      Nothing => go (Remove :: stack) rest
+      Just ann' => SAnnPush ann' <$> go (DontRemove :: stack) rest
+    go stack (SAnnPop rest) = case stack of
+      [] => Nothing
+      DontRemove :: stack' => SAnnPop <$> go stack' rest
+      Remove :: stack' => go stack' rest
+
+||| Removes all annotations.
+export
+unAnnotateS : SimpleDocStream ann -> SimpleDocStream xxx
+unAnnotateS SEmpty = SEmpty
+unAnnotateS (SChar c rest) = SChar c (unAnnotateS rest)
+unAnnotateS (SText l t rest) = SText l t (unAnnotateS rest)
+unAnnotateS (SLine l rest) = SLine l (unAnnotateS rest)
+unAnnotateS (SAnnPush ann rest) = unAnnotateS rest
+unAnnotateS (SAnnPop rest) = unAnnotateS rest
+
+||| Changes the annotation of a document.
+export
+reAnnotateS : (ann -> ann') -> SimpleDocStream ann -> SimpleDocStream ann'
+reAnnotateS re SEmpty = SEmpty
+reAnnotateS re (SChar c rest) = SChar c (reAnnotateS re rest)
+reAnnotateS re (SText l t rest) = SText l t (reAnnotateS re rest)
+reAnnotateS re (SLine l rest) = SLine l (reAnnotateS re rest)
+reAnnotateS re (SAnnPush ann rest) = SAnnPush (re ann) (reAnnotateS re rest)
+reAnnotateS re (SAnnPop rest) = SAnnPop (reAnnotateS re rest)
+
+export
+Functor SimpleDocStream where
+  map = reAnnotateS
+
+||| Collects all annotations from a document.
+export
+collectAnnotations : Monoid m => (ann -> m) -> SimpleDocStream ann -> m
+collectAnnotations f SEmpty = neutral
+collectAnnotations f (SChar c rest) = collectAnnotations f rest
+collectAnnotations f (SText l t rest) = collectAnnotations f rest
+collectAnnotations f (SLine l rest) = collectAnnotations f rest
+collectAnnotations f (SAnnPush ann rest) = f ann <+> collectAnnotations f rest
+collectAnnotations f (SAnnPop rest) = collectAnnotations f rest
+
+||| Transform a document based on its annotations.
+export
+traverse : Applicative f => (ann -> f ann') -> SimpleDocStream ann -> f (SimpleDocStream ann')
+traverse f SEmpty = pure SEmpty
+traverse f (SChar c rest) = SChar c . delay <$> traverse f rest
+traverse f (SText l t rest) = SText l t . delay <$> traverse f rest
+traverse f (SLine l rest) = SLine l <$> traverse f rest
+traverse f (SAnnPush ann rest) = SAnnPush <$> f ann <*> traverse f rest
+traverse f (SAnnPop rest) = SAnnPop <$> traverse f rest
+
+data WhitespaceStrippingState = AnnotationLevel Int | RecordedWithespace (List Int) Int
+
+dropWhileEnd : (a -> Bool) -> List a -> List a
+dropWhileEnd p = foldr (\x, xs => if p x && isNil xs then [] else x :: xs) []
+
+||| Removes all trailing space characters.
+export
+removeTrailingWhitespace : SimpleDocStream ann -> SimpleDocStream ann
+removeTrailingWhitespace = fromMaybe internalError . go (RecordedWithespace [] 0)
+  where
+    prependEmptyLines : List Int -> SimpleDocStream ann -> SimpleDocStream ann
+    prependEmptyLines is sds0 = foldr (\_, sds => SLine 0 sds) sds0 is
+
+    commitWhitespace : List Int -> Int -> SimpleDocStream ann -> SimpleDocStream ann
+    commitWhitespace [] 0 sds = sds
+    commitWhitespace [] 1 sds = SChar ' ' sds
+    commitWhitespace [] n sds = SText n (textSpaces n) sds
+    commitWhitespace (i :: is) n sds = prependEmptyLines is (SLine (i + n) sds)
+
+    go : WhitespaceStrippingState -> SimpleDocStream ann -> Maybe (SimpleDocStream ann)
+    go (AnnotationLevel _) SEmpty = pure SEmpty
+    go l@(AnnotationLevel _) (SChar c rest) = SChar c . delay <$> go l rest
+    go l@(AnnotationLevel _) (SText lt text rest) = SText lt text . delay <$> go l rest
+    go l@(AnnotationLevel _) (SLine i rest) = SLine i <$> go l rest
+    go (AnnotationLevel l) (SAnnPush ann rest) = SAnnPush ann <$> go (AnnotationLevel (l + 1)) rest
+    go (AnnotationLevel l) (SAnnPop rest) =
+      if l > 1
+         then SAnnPop <$> go (AnnotationLevel (l - 1)) rest
+         else SAnnPop <$> go (RecordedWithespace [] 0) rest
+    go (RecordedWithespace _ _) SEmpty = pure SEmpty
+    go (RecordedWithespace lines spaces) (SChar ' ' rest) = go (RecordedWithespace lines (spaces + 1)) rest
+    go (RecordedWithespace lines spaces) (SChar c rest) =
+      do rest' <- go (RecordedWithespace [] 0) rest
+         pure $ commitWhitespace lines spaces (SChar c rest')
+    go (RecordedWithespace lines spaces) (SText l text rest) =
+      let stripped = pack $ dropWhileEnd (== ' ') $ unpack text
+          strippedLength = cast $ length stripped
+          trailingLength = l - strippedLength in
+          if strippedLength == 0
+             then go (RecordedWithespace lines (spaces + l)) rest
+             else do rest' <- go (RecordedWithespace [] trailingLength) rest
+                     pure $ commitWhitespace lines spaces (SText strippedLength stripped rest')
+    go (RecordedWithespace lines spaces) (SLine i rest) = go (RecordedWithespace (i :: lines) 0) rest
+    go (RecordedWithespace lines spaces) (SAnnPush ann rest) =
+      do rest' <- go (AnnotationLevel 1) rest
+         pure $ commitWhitespace lines spaces (SAnnPush ann rest')
+    go (RecordedWithespace lines spaces) (SAnnPop _) = Nothing
+
+public export
+FittingPredicate : Type -> Type
+FittingPredicate ann = Int -> Int -> Maybe Int -> SimpleDocStream ann -> Bool
+
+data LayoutPipeline ann = Nil | Cons Int (Doc ann) (LayoutPipeline ann) | UndoAnn (LayoutPipeline ann)
+
+export
+defaultPageWidth : PageWidth
+defaultPageWidth = AvailablePerLine 80 1
+
+round : Double -> Int
+round x = if x > 0
+             then if x - floor x < 0.5 then cast $ floor x else cast $ ceiling x
+             else if ceiling x - x < 0.5 then cast $ ceiling x else cast $ floor x
+
+||| The remaining width on the current line.
+remainingWidth : Int -> Double -> Int -> Int -> Int
+remainingWidth lineLength ribbonFraction lineIndent currentColumn =
+  let columnsLeftInLine = lineLength - currentColumn
+      ribbonWidth = (max 0 . min lineLength . round) (cast lineLength * ribbonFraction)
+      columnsLeftInRibbon = lineIndent + ribbonWidth - currentColumn in
+      min columnsLeftInLine columnsLeftInRibbon
+
+public export
+record LayoutOptions where
+  constructor MkLayoutOptions
+  layoutPageWidth : PageWidth
+
+export
+defaultLayoutOptions : LayoutOptions
+defaultLayoutOptions = MkLayoutOptions defaultPageWidth
+
+||| The Wadler/Leijen layout algorithm.
+export
+layoutWadlerLeijen : FittingPredicate ann -> PageWidth -> Doc ann -> SimpleDocStream ann
+layoutWadlerLeijen fits pageWidth_ doc = best 0 0 (Cons 0 doc Nil)
+  where
+    initialIndentation : SimpleDocStream ann -> Maybe Int
+    initialIndentation (SLine i _) = Just i
+    initialIndentation (SAnnPush _ s) = initialIndentation s
+    initialIndentation (SAnnPop s) = initialIndentation s
+    initialIndentation _ = Nothing
+
+    selectNicer : Int -> Int -> SimpleDocStream ann -> Lazy (SimpleDocStream ann) -> SimpleDocStream ann
+    selectNicer lineIndent currentColumn x y =
+      if fits lineIndent currentColumn (initialIndentation y) x then x else y
+
+    best : Int -> Int -> LayoutPipeline ann -> SimpleDocStream ann
+    best _ _ Nil = SEmpty
+    best nl cc (UndoAnn ds) = SAnnPop (best nl cc ds)
+    best nl cc (Cons i Empty ds) = best nl cc ds
+    best nl cc (Cons i (Chara c) ds) = SChar c (best nl (cc + 1) ds)
+    best nl cc (Cons i (Text l t) ds) = SText l t (best nl (cc + l) ds)
+    best nl cc (Cons i Line ds) = let x = best i i ds
+                                      i' = case x of
+                                                SEmpty => 0
+                                                SLine _ _ => 0
+                                                _ => i in
+                                      SLine i' x
+    best nl cc c@(Cons i (FlatAlt x y) ds) = best nl cc $ assert_smaller c (Cons i x ds)
+    best nl cc (Cons i (Cat x y) ds) = assert_total $ best nl cc (Cons i x (Cons i y ds))
+    best nl cc c@(Cons i (Nest j x) ds) = best nl cc $ assert_smaller c (Cons (i + j) x ds)
+    best nl cc c@(Cons i (Union x y) ds) = let x' = best nl cc $ assert_smaller c (Cons i x ds)
+                                               y' = delay $ best nl cc $ assert_smaller c (Cons i y ds) in
+                                               selectNicer nl cc x' y'
+    best nl cc c@(Cons i (Column f) ds) = best nl cc $ assert_smaller c (Cons i (f cc) ds)
+    best nl cc c@(Cons i (WithPageWidth f) ds) = best nl cc $ assert_smaller c (Cons i (f pageWidth_) ds)
+    best nl cc c@(Cons i (Nesting f) ds) = best nl cc $ assert_smaller c (Cons i (f i) ds)
+    best nl cc c@(Cons i (Annotated ann x) ds) = SAnnPush ann $ best nl cc $ assert_smaller c (Cons i x (UndoAnn ds))
+
+||| Layout a document with unbounded page width.
+export
+layoutUnbounded : Doc ann -> SimpleDocStream ann
+layoutUnbounded = layoutWadlerLeijen (\_, _, _, sdoc => True) Unbounded
+
+fits : Int -> SimpleDocStream ann -> Bool
+fits w s = if w < 0 then False
+  else case s of
+            SEmpty => True
+            SChar _ x => fits (w - 1) x
+            SText l _ x => fits (w - l) x
+            SLine i x => True
+            SAnnPush _ x => fits w x
+            SAnnPop x => fits w x
+
+||| The default layout algorithm.
+export
+layoutPretty : LayoutOptions -> Doc ann -> SimpleDocStream ann
+layoutPretty (MkLayoutOptions pageWidth_@(AvailablePerLine lineLength ribbonFraction)) =
+    layoutWadlerLeijen (\lineIndent, currentColumn, _, sdoc =>
+      fits (remainingWidth lineLength ribbonFraction lineIndent currentColumn) sdoc) pageWidth_
+layoutPretty (MkLayoutOptions Unbounded) = layoutUnbounded
+
+||| Layout algorithm with more lookahead than layoutPretty.
+export
+layoutSmart : LayoutOptions -> Doc ann -> SimpleDocStream ann
+layoutSmart (MkLayoutOptions pageWidth_@(AvailablePerLine lineLength ribbonFraction)) =
+    layoutWadlerLeijen fits pageWidth_
+  where
+    fits : Int -> Int -> Maybe Int -> SimpleDocStream ann -> Bool
+    fits lineIndent currentColumn initialIndentY sdoc = go availableWidth sdoc
+      where
+        availableWidth : Int
+        availableWidth = remainingWidth lineLength ribbonFraction lineIndent currentColumn
+
+        minNestingLevel : Int
+        minNestingLevel = case initialIndentY of
+                               Just i => min i currentColumn
+                               Nothing => currentColumn
+
+        go : Int -> SimpleDocStream ann -> Bool
+        go w s = if w < 0
+          then False
+          else case s of
+                    SEmpty => True
+                    SChar _ x => go (w - 1) $ assert_smaller s x
+                    SText l _ x => go (w - l) $ assert_smaller s x
+                    SLine i x => if minNestingLevel < i
+                                    then go (lineLength - i) $ assert_smaller s x
+                                    else True
+                    SAnnPush _ x => go w x
+                    SAnnPop x => go w x
+layoutSmart (MkLayoutOptions Unbounded) = layoutUnbounded
+
+||| Lays out the document without adding any indentation. This layouter is very fast.
+export
+layoutCompact : Doc ann -> SimpleDocStream ann
+layoutCompact doc = scan 0 [doc]
+  where
+    scan : Int -> List (Doc ann) -> SimpleDocStream ann
+    scan _ [] = SEmpty
+    scan col (Empty :: ds) = scan col ds
+    scan col ((Chara c) :: ds) = SChar c (scan (col + 1) ds)
+    scan col ((Text l t) :: ds) = SText l t (scan (col + l) ds)
+    scan col s@((FlatAlt x _) :: ds) = scan col $ assert_smaller s (x :: ds)
+    scan col (Line :: ds) = SLine 0 (scan 0 ds)
+    scan col s@((Cat x y) :: ds) = scan col $ assert_smaller s (x :: y :: ds)
+    scan col s@((Nest _ x) :: ds) = scan col $ assert_smaller s (x :: ds)
+    scan col s@((Union _ y) :: ds) = scan col $ assert_smaller s (y :: ds)
+    scan col s@((Column f) :: ds) = scan col $ assert_smaller s (f col :: ds)
+    scan col s@((WithPageWidth f) :: ds) = scan col $ assert_smaller s (f Unbounded :: ds)
+    scan col s@((Nesting f) :: ds) = scan col $ assert_smaller s (f 0 :: ds)
+    scan col s@((Annotated _ x) :: ds) = scan col $ assert_smaller s (x :: ds)
+
+export
+renderShow : SimpleDocStream ann -> (String -> String)
+renderShow SEmpty = id
+renderShow (SChar c x) = (strCons c) . renderShow x
+renderShow (SText _ t x) = (t ++) . renderShow x
+renderShow (SLine i x) = ((strCons '\n' $ textSpaces i) ++) . renderShow x
+renderShow (SAnnPush _ x) = renderShow x
+renderShow (SAnnPop x) = renderShow x
+
+export
+Show (Doc ann) where
+  show doc = renderShow (layoutPretty defaultLayoutOptions doc) ""

src/Libraries/Text/PrettyPrint/Prettyprinter/Render/String.idr

@@ -0,0 +1,32 @@
+module Libraries.Text.PrettyPrint.Prettyprinter.Render.String
+
+import Data.Strings
+import Libraries.Data.String.Extra
+import Libraries.Text.PrettyPrint.Prettyprinter.Doc
+
+%default total
+
+export
+renderString : SimpleDocStream ann -> String
+renderString SEmpty = neutral
+renderString (SChar c rest) = singleton c <+> renderString rest
+renderString (SText l t rest) = t <+> renderString rest
+renderString (SLine l rest) = singleton '\n' <+> textSpaces l <+> renderString rest
+renderString (SAnnPush ann rest) = renderString rest
+renderString (SAnnPop rest) = renderString rest
+
+export
+renderIO : SimpleDocStream ann -> IO ()
+renderIO SEmpty = pure ()
+renderIO (SChar c rest) = do putChar c; renderIO rest
+renderIO (SText l t rest) = do putStr t; renderIO rest
+renderIO (SLine l rest) = do putChar '\n'
+                             putStr (textSpaces l)
+                             renderIO rest
+renderIO (SAnnPush ann rest) = renderIO rest
+renderIO (SAnnPop rest) = renderIO rest
+
+||| Prettyprints a document to standard output, using default options.
+export
+putDoc : Doc ann -> IO ()
+putDoc = renderIO . layoutPretty defaultLayoutOptions

src/Libraries/Text/PrettyPrint/Prettyprinter/Render/Terminal.idr

@@ -0,0 +1,98 @@
+module Libraries.Text.PrettyPrint.Prettyprinter.Render.Terminal
+
+import Data.Maybe
+import Data.Strings
+import public Libraries.Control.ANSI
+import Control.Monad.ST
+import Libraries.Text.PrettyPrint.Prettyprinter.Doc
+
+%default covering
+
+public export
+AnsiStyle : Type
+AnsiStyle = List SGR
+
+export
+color : Color -> AnsiStyle
+color c = pure $ SetForeground c
+
+export
+bgColor : Color -> AnsiStyle
+bgColor c = pure $ SetBackground c
+
+export
+bold : AnsiStyle
+bold = pure $ SetStyle Bold
+
+export
+italic : AnsiStyle
+italic = pure $ SetStyle Italic
+
+export
+underline : AnsiStyle
+underline = pure $ SetStyle SingleUnderline
+
+export
+strike : AnsiStyle
+strike = pure $ SetStyle Striked
+
+export
+renderString : SimpleDocStream AnsiStyle -> String
+renderString sdoc = fromMaybe "<internal pretty printing error>" $ runST $ do
+    styleStackRef <- newSTRef {a = List AnsiStyle} [neutral]
+    outputRef <- newSTRef {a = String} neutral
+    go styleStackRef outputRef sdoc
+    readSTRef styleStackRef >>= \case
+      [] => pure Nothing
+      [_] => Just <$> readSTRef outputRef
+      _ => pure Nothing
+  where
+    push : STRef s (List AnsiStyle) -> List SGR -> ST s ()
+    push stack x = modifySTRef stack (x ::)
+
+    peek : STRef s (List AnsiStyle) -> ST s (Maybe AnsiStyle)
+    peek stack = do
+      (x :: _) <- readSTRef stack | [] => pure Nothing
+      pure (Just x)
+
+    pop : STRef s (List AnsiStyle) -> ST s (Maybe AnsiStyle)
+    pop stack = do
+      (x :: xs) <- readSTRef stack | [] => pure Nothing
+      writeSTRef stack xs
+      pure (Just x)
+
+    writeOutput : STRef s String -> String -> ST s ()
+    writeOutput out x = modifySTRef out (<+> x)
+
+    go : STRef s (List AnsiStyle) -> STRef s String -> SimpleDocStream AnsiStyle -> ST s ()
+    go stack out SEmpty = pure ()
+    go stack out (SChar c rest) = do
+      writeOutput out (singleton c)
+      go stack out rest
+    go stack out (SText l t rest) = do
+      writeOutput out t
+      go stack out rest
+    go stack out (SLine l rest) = do
+      writeOutput out (singleton '\n' <+> textSpaces l)
+      go stack out rest
+    go stack out (SAnnPush style rest) = do
+      Just currentStyle <- peek stack
+        | Nothing => writeSTRef stack []
+      let newStyle = style <+> currentStyle
+      push stack newStyle
+      writeOutput out (escapeSGR newStyle)
+      go stack out rest
+    go stack out (SAnnPop rest) = do
+      _ <- pop stack
+      Just newStyle <- peek stack
+        | Nothing => writeSTRef stack []
+      writeOutput out (escapeSGR (Reset :: newStyle))
+      go stack out rest
+
+export
+renderIO : SimpleDocStream AnsiStyle -> IO ()
+renderIO = putStrLn . renderString
+
+export
+putDoc : Doc AnsiStyle -> IO ()
+putDoc = renderIO . layoutPretty defaultLayoutOptions

src/Libraries/Text/PrettyPrint/Prettyprinter/SimpleDocTree.idr

@@ -0,0 +1,95 @@
+module Libraries.Text.PrettyPrint.Prettyprinter.SimpleDocTree
+
+import Libraries.Text.PrettyPrint.Prettyprinter.Doc
+import Libraries.Text.Parser
+
+%default total
+
+||| Tree-like structure more suitable for rendering to a structured
+||| format such as HTML.
+public export
+data SimpleDocTree : Type -> Type where
+  STEmpty : SimpleDocTree ann
+  STChar : (c : Char) -> SimpleDocTree ann
+  STText : (len : Int) -> (text : String) -> SimpleDocTree ann
+  STLine : (i : Int) -> SimpleDocTree ann
+  STAnn : ann -> (rest : SimpleDocTree ann) -> SimpleDocTree ann
+  STConcat : List (SimpleDocTree ann) -> SimpleDocTree ann
+
+||| Changes the annotation of a document, or none at all.
+export
+alterAnnotationsST : (ann -> List ann') -> SimpleDocTree ann -> SimpleDocTree ann'
+alterAnnotationsST re STEmpty = STEmpty
+alterAnnotationsST re (STChar c) = STChar c
+alterAnnotationsST re (STText len text) = STText len text
+alterAnnotationsST re (STLine i) = STLine i
+alterAnnotationsST re (STAnn ann rest) = foldr STAnn (alterAnnotationsST re rest) (re ann)
+alterAnnotationsST re (STConcat xs) = assert_total $ STConcat (map (alterAnnotationsST re) xs)
+
+||| Changes the annotation of a document.
+export
+reAnnotateST : (ann -> ann') -> SimpleDocTree ann -> SimpleDocTree ann'
+reAnnotateST f = alterAnnotationsST (pure . f)
+
+||| Removes all annotations.
+export
+unAnnotateST : SimpleDocTree ann -> SimpleDocTree xxx
+unAnnotateST = alterAnnotationsST (const [])
+
+||| Collects all annotations from a document.
+export
+collectAnnotations : Monoid m => (ann -> m) -> SimpleDocTree ann -> m
+collectAnnotations f STEmpty = neutral
+collectAnnotations f (STChar c) = neutral
+collectAnnotations f (STText len text) = neutral
+collectAnnotations f (STLine i) = neutral
+collectAnnotations f (STAnn ann rest) = f ann <+> collectAnnotations f rest
+collectAnnotations f (STConcat xs) = assert_total $ concat $ map (collectAnnotations f) xs
+
+||| Transform a document based on its annotations.
+export
+traverse : Applicative f => (ann -> f ann') -> SimpleDocTree ann -> f (SimpleDocTree ann')
+traverse f STEmpty = pure STEmpty
+traverse f (STChar c) = pure $ STChar c
+traverse f (STText len text) = pure $ STText len text
+traverse f (STLine i) = pure $ STLine i
+traverse f (STAnn ann rest) = STAnn <$> f ann <*> traverse f rest
+traverse f (STConcat xs) = assert_total $ STConcat <$> Prelude.traverse (traverse f) xs
+
+sdocToTreeParser : SimpleDocStream ann -> (Maybe (SimpleDocTree ann), Maybe (SimpleDocStream ann))
+sdocToTreeParser SEmpty = (Just STEmpty, Nothing)
+sdocToTreeParser (SChar c rest) = case sdocToTreeParser rest of
+  (Just tree, rest') => (Just $ STConcat [STChar c, tree], rest')
+  (Nothing, rest') => (Just $ STChar c, rest')
+sdocToTreeParser (SText len text rest) = case sdocToTreeParser rest of
+  (Just tree, rest') => (Just $ STConcat [STText len text, tree], rest')
+  (Nothing, rest') => (Just $ STText len text, rest')
+sdocToTreeParser (SLine i rest) = case sdocToTreeParser rest of
+  (Just tree, rest') => (Just $ STConcat [STLine i, tree], rest')
+  (Nothing, rest') => (Just $ STLine i, rest')
+sdocToTreeParser (SAnnPush ann rest) = case sdocToTreeParser rest of
+  (tree, Nothing) => (Nothing, Nothing)
+  (Just tree, Nothing) => (Just $ STAnn ann tree, Nothing)
+  (Just tree, Just rest') => case sdocToTreeParser rest' of
+    (Just tree', rest'') => (Just $ STConcat [STAnn ann tree, tree'], rest'')
+    (Nothing, rest'') => (Just $ STAnn ann tree, rest'')
+  (Nothing, Just rest') => assert_total $ sdocToTreeParser rest'
+  (Nothing, Nothing) => (Nothing, Nothing)
+sdocToTreeParser (SAnnPop rest) = (Nothing, Just rest)
+
+export
+fromStream : SimpleDocStream ann -> SimpleDocTree ann
+fromStream sdoc = case sdocToTreeParser sdoc of
+    (Just tree, Nothing) => flatten tree
+    _ => internalError
+  where
+    flatten : SimpleDocTree ann -> SimpleDocTree ann
+    flatten (STConcat [x, STEmpty]) = flatten x
+    flatten (STConcat [x, STConcat xs]) = case flatten (STConcat xs) of
+      (STConcat xs') => STConcat (x :: xs')
+      y => y
+    flatten x = x
+
+    internalError : SimpleDocTree ann
+    internalError = let msg = "<internal pretty printing error>" in
+                        STText (cast $ length msg) msg

src/Libraries/Text/PrettyPrint/Prettyprinter/Symbols.idr

@@ -0,0 +1,109 @@
+module Libraries.Text.PrettyPrint.Prettyprinter.Symbols
+
+import Libraries.Text.PrettyPrint.Prettyprinter.Doc
+
+%default total
+
+export
+squote : Doc ann
+squote = pretty '\''
+
+export
+dquote : Doc ann
+dquote = pretty '"'
+
+export
+lparen : Doc ann
+lparen = pretty '('
+
+export
+rparen : Doc ann
+rparen = pretty ')'
+
+export
+langle : Doc ann
+langle = pretty '<'
+
+export
+rangle : Doc ann
+rangle = pretty '>'
+
+export
+lbracket : Doc ann
+lbracket = pretty '['
+
+export
+rbracket : Doc ann
+rbracket = pretty ']'
+
+export
+lbrace : Doc ann
+lbrace = pretty '{'
+
+export
+rbrace : Doc ann
+rbrace = pretty '}'
+
+export
+semi : Doc ann
+semi = pretty ';'
+
+export
+colon : Doc ann
+colon = pretty ':'
+
+export
+comma : Doc ann
+comma = pretty ','
+
+export
+space : Doc ann
+space = pretty ' '
+
+export
+dot : Doc ann
+dot = pretty '.'
+
+export
+slash : Doc ann
+slash = pretty '/'
+
+export
+backslash : Doc ann
+backslash = pretty '\\'
+
+export
+equals : Doc ann
+equals = pretty '='
+
+export
+pipe : Doc ann
+pipe = pretty '|'
+
+export
+squotes : Doc ann -> Doc ann
+squotes = enclose squote squote
+
+export
+dquotes : Doc ann -> Doc ann
+dquotes = enclose dquote dquote
+
+export
+parens : Doc ann -> Doc ann
+parens = enclose lparen rparen
+
+export
+parenthesise : Bool -> Doc ann -> Doc ann
+parenthesise b = if b then parens else id
+
+export
+angles : Doc ann -> Doc ann
+angles = enclose langle rangle
+
+export
+brackets : Doc ann -> Doc ann
+brackets = enclose lbracket rbracket
+
+export
+braces : Doc ann -> Doc ann
+braces = enclose lbrace rbrace

src/Libraries/Text/PrettyPrint/Prettyprinter/Util.idr

@@ -0,0 +1,31 @@
+module Libraries.Text.PrettyPrint.Prettyprinter.Util
+
+import Data.List
+import Data.Strings
+import Libraries.Text.PrettyPrint.Prettyprinter.Doc
+import Libraries.Text.PrettyPrint.Prettyprinter.Render.String
+
+%default total
+
+||| Split an input into word-sized `Doc`.
+export
+words : String -> List (Doc ann)
+words s = map pretty $ map pack (helper (unpack s))
+  where
+    helper : List Char -> List (List Char)
+    helper s =
+      case dropWhile isSpace s of
+           [] => []
+           s' => let (w, s'') = break isSpace s' in
+                     w :: helper (assert_smaller s s'')
+
+||| Insert soft linebreaks between words, so that text is broken into multiple
+||| lines when it exceeds the available width.
+export
+reflow : String -> Doc ann
+reflow = fillSep . words
+
+||| Renders a document with a certain width.
+export
+putDocW : Nat -> Doc ann -> IO ()
+putDocW w = renderIO . layoutPretty (record { layoutPageWidth = AvailablePerLine (cast w) 1 } defaultLayoutOptions)

src/Libraries/Text/Quantity.idr

@@ -1,4 +1,4 @@
-module Text.Quantity
+module Libraries.Text.Quantity
 
 %default total
 

src/Libraries/Text/Token.idr

@@ -1,4 +1,4 @@
-module Text.Token
+module Libraries.Text.Token
 
 %default total