name: tabular
include: ../../../src/ .

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

┌───┬───┬───┐
│foo│bar│baz│
├───┼───┼───┤
│  1│2  │ 3 │
├───┼───┼───┤
│  6│5  │ 4 │
└───┴───┴───┘
┌───┬───┐
│foo│bar│
├───┼───┤
│  1│2  │
├───┼───┤
│  4│3  │
└───┴───┘
+-------+
|foo|bar|
|---+---|
|  1|2  |
|---+---|
|  4|3  |
+-------+
foo bar
  1 2  
  4 3  
┌───┬───┐
│foo│bar│
│  1│2  │
│  4│3  │
└───┴───┘
foo│bar
───┼───
  1│2  
───┼───
  4│3  
┌─────┬─────┐
│ foo │ bar │
├─────┼─────┤
│   1 │ 2   │
├─────┼─────┤
│   4 │ 3   │
└─────┴─────┘
┌─────┬─────┐
│ foo │ bar │
│   1 │ 2   │
│   4 │ 3   │
└─────┴─────┘
┌───────┬────┬───┬───┬─────────┐
│  foo  │ bar│   │   │         │
├───────┼────┼───┼───┼─────────┤
│partial│rows│are│ok │         │
├───────┼────┼───┼───┼─────────┤
│   3   │   2│1  │...│surprise!│
└───────┴────┴───┴───┴─────────┘
┌───┬───┐
│foo│bar│
│  1│  2│
│  4│  3│
└───┴───┘

-- This is taken from README.Text.Tabular
{-# OPTIONS --guardedness #-}
module Main where
open import Function.Base
open import Data.List.Base
open import Data.String.Base
open import Data.Vec.Base
open import IO.Base
open import IO.Finite
open import Text.Tabular.Base
import Text.Tabular.List as Tabularˡ
import Text.Tabular.Vec  as Tabularᵛ
main : Main
main = run $ do
  putStrLn $
    unlines (Tabularᵛ.display unicode
            (Right ∷ Left ∷ Center ∷ [])
          ( ("foo" ∷ "bar" ∷ "baz" ∷ [])
          ∷ ("1"   ∷ "2"   ∷ "3" ∷ [])
          ∷ ("6"   ∷ "5"   ∷ "4" ∷ [])
          ∷ []))
  let foobar = ("foo" ∷ "bar" ∷ [])
             ∷ ("1"   ∷ "2"   ∷ [])
             ∷ ("4"   ∷ "3"   ∷ [])
             ∷ []
  putStrLn $
    unlines (Tabularᵛ.display unicode
            (Right ∷ Left ∷ [])
            foobar)
  putStrLn $
    unlines (Tabularᵛ.display ascii
            (Right ∷ Left ∷ [])
            foobar)
  putStrLn $
    unlines (Tabularᵛ.display whitespace
            (Right ∷ Left ∷ [])
            foobar)
  putStrLn $
    unlines (Tabularᵛ.display (compact unicode)
            (Right ∷ Left ∷ [])
            foobar)
  putStrLn $
    unlines (Tabularᵛ.display (noBorder unicode)
            (Right ∷ Left ∷ [])
            foobar)
  putStrLn $
    unlines (Tabularᵛ.display (addSpace unicode)
            (Right ∷ Left ∷ [])
            foobar)
  putStrLn $
    unlines (Tabularᵛ.display (compact (addSpace unicode))
            (Right ∷ Left ∷ [])
            foobar)
  putStrLn $
    unlines (Tabularˡ.display unicode
            (Center ∷ Right ∷ [])
            ( ("foo" ∷ "bar" ∷ [])
            ∷ ("partial" ∷ "rows" ∷ "are" ∷ "ok" ∷ [])
            ∷ ("3" ∷ "2" ∷ "1" ∷ "..." ∷ "surprise!" ∷ [])
            ∷ []))
  putStrLn $
    unlines (unsafeDisplay (compact unicode)
          ( ("foo" ∷ "bar" ∷ [])
          ∷ ("  1" ∷ "  2" ∷ [])
          ∷ ("  4" ∷ "  3" ∷ [])
          ∷ []))

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

name: regex
include: ../../../src/ .

Match found: $1 --compile-dir=../../_build -c [Main.agda] > log
Match found: ./../../[_build/]Main > output
No match found
Match found: rm ../../[_build/]Main
Match found: rm ../../[_build/MAlonzo/Code/]Main*

{-# OPTIONS --guardedness #-}
module Main where
open import Data.Bool.Base using (true; false)
open import Data.List.Base using (_∷_; [])
open import Data.List.Relation.Binary.Infix.Heterogeneous using (toView; MkView)
open import Data.String using (String; toList; fromList; lines; concat)
open import IO
open import Function.Base using (_$_; case_of_)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Nullary
open import Text.Regex.String
show : ∀ e {xs} → Dec (Match (Span e _≡_) xs (Regex.expression e)) → String
show _ (no _) = "No match found"
show e (yes match) = case toView (toInfix e (match .Match.related)) of λ where
  (MkView pref x suff) → concat
    $ "Match found: "
    ∷ fromList pref
    ∷ "["
    ∷ fromList (match .Match.list)
    ∷ "]"
    ∷ fromList suff
    ∷ []
agdaFile : Exp
agdaFile = [ 'a' ─ 'z' ∷ 'A' ─ 'Z' ∷ [] ] +
         ∙ singleton '.'
         ∙ singleton 'a'
         ∙ singleton 'g'
         ∙ singleton 'd'
         ∙ singleton 'a'
buildDir : Exp
buildDir = singleton '_'
         ∙ ([ 'a' ─ 'z' ∷ 'A' ─ 'Z' ∷ [] ] + ∙ singleton '/') +
regex : Regex
regex .Regex.fromStart  = false
regex .Regex.tillEnd    = false
regex .Regex.expression
  = agdaFile ∣ buildDir
main : Main
main = run $ do
  text ← readFiniteFile "run"
  List.forM′ (lines text) $ λ l →
    putStrLn (show regex $ search (toList l) regex)

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

name: printf
include: ../../../src/ .

example: 3 + 2 ≡ 5
example: 3 + -3 ≡ 0
gcd(-9,15) ≡ 3
lcm(-9,15) ≡ 45
A char: c
A float: 3.14

{-# OPTIONS --guardedness #-}
module Main where
open import Data.Integer.Base as ℤ using (+_)
open import Data.Integer.Literals
open import Data.Integer.GCD
open import Data.Integer.LCM
open import Data.Nat.Base
open import Data.String.Base
open import Data.Unit.Base
open import Function.Base using (_$_)
open import IO.Base
open import IO.Finite
open import Text.Printf
main : Main
main = run $ do
  let instance _ = negative
  putStrLn $ printf "%s: %u + %u ≡ %u" "example" 3 2 5
  putStrLn $ printf "%s: %u + %i ≡ %d" "example" 3 -3 (+ 3 ℤ.+ -3)
  putStrLn $ printf "gcd(%d,%i) ≡ %d" -9 (+ 15) (gcd -9 (+ 15))
  putStrLn $ printf "lcm(%d,%i) ≡ %d" -9 (+ 15) (lcm -9 (+ 15))
  putStrLn $ printf "A %s: %c" "char" 'c'
  putStrLn $ printf "A %s: %f" "float" 3.14

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

name: pretty
include: ../../../src/ .

(setq column-number-mode t)
(setq-default show-trailing-whitespace
              t)
(add-hook 'write-file-hooks
          'delete-trailing-whitespace)
(setq column-number-mode t)
(setq-default show-trailing-whitespace t)
(add-hook 'write-file-hooks 'delete-trailing-whitespace)

{-# OPTIONS --guardedness --sized-types #-}
module Main where
open import Size
open import Data.List.Base
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Data.Nat.Base using (ℕ)
open import Data.String.Base using (String)
open import Data.Tree.Rose using (Rose; node)
open import IO.Base
open import IO.Finite
open import Function.Base using (_$_)
open import Text.Pretty using (Doc; render)
open module Pretty {w} = Text.Pretty w hiding (Doc; render)
private
  variable
    i : Size
    w : ℕ
pretty : Rose (Maybe String) i → Doc w
pretty (node nothing  ts) = vcat (map pretty ts)
pretty (node (just a) []) = text a
pretty (node (just a) ts) = parens $ text a <+> sep (map pretty ts)
SEXP = Rose (Maybe String) _
atom : String → SEXP
atom a = node (just a) []
list : List SEXP → SEXP
list = node nothing
colMode : SEXP
colMode = node (just "setq") (atom "column-number-mode" ∷ atom "t" ∷ [])
showTrailing : SEXP
showTrailing = node (just "setq-default")
             $ atom "show-trailing-whitespace" ∷ atom "t" ∷ []
deleteTrailing : SEXP
deleteTrailing =  node (just "add-hook")
               $ atom "'write-file-hooks"
               ∷ atom "'delete-trailing-whitespace"
               ∷ []
dotEmacs : SEXP
dotEmacs = node nothing
         $ colMode ∷ showTrailing ∷ deleteTrailing ∷ []
main : Main
main = run $ do
  let doc : Doc w; doc = pretty dotEmacs
  putStrLn $ render 40 doc
  putStrLn $ render 80 doc

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > random_values
touch output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

name: ansi
include: ../../../src/ .

{-# OPTIONS --guardedness #-}
module Main where
open import Level using (0ℓ)
open import Data.Unit.Polymorphic.Base using (⊤)
import Data.Char.Base as Char
import Data.Fin.Base as Fin
import Data.Fin.Show as Fin
import Data.Float.Base as Float
open import Data.Integer.Base using (-[1+_]; +_; -≤+)
import Data.Integer.Show as ℤ
open import Data.List.Base as List using ([]; _∷_)
import Data.List.Show as List
import Data.Nat.Base
import Data.Nat.Properties as ℕ
import Data.Nat.Show as ℕ
open import Data.String.Base as String
import Data.Vec.Show as Vec
import Data.Word.Base as Word64
open import IO.Base
open import IO.Finite
open import Function.Base using (_$_; _∘_)
open import System.Random
import Data.Vec.Bounded.Show as Vec≤
open import Relation.Binary.Construct.Closure.Reflexive
asA : String → String → IO {0ℓ} ⊤
asA ty str = putStrLn (ty ++ ": " ++ str)
main : Main
main = run $ do
  asA "Char" ∘ Char.show =<< Char.randomIO
  asA "Char" ∘ Char.show ∘ InBounds.value =<< Char.randomRIO ' ' '~' [ ℕ.≤ᵇ⇒≤ _ _ _ ]
  asA "Float" ∘ Float.show =<< Float.randomIO
  asA "Float" ∘ Float.show ∘ InBounds.value =<< Float.randomRIO 0.0 1.0 _
  asA "Integer" ∘ ℤ.show =<< ℤ.randomIO
  asA "Integer" ∘ ℤ.show ∘ InBounds.value =<< ℤ.randomRIO -[1+ 2 ] (+ 5) -≤+
  asA "Nat" ∘ ℕ.show =<< ℕ.randomIO
  asA "Nat" ∘ ℕ.show ∘ InBounds.value =<< ℕ.randomRIO 1 10 (ℕ.≤ᵇ⇒≤ _ _ _)
  asA "Word" ∘ ℕ.show ∘ Word64.toℕ =<< Word64.randomIO
  asA "Word" ∘ ℕ.show ∘ Word64.toℕ ∘ InBounds.value =<<
    Word64.randomRIO (Word64.fromℕ 10) (Word64.fromℕ 20) (ℕ.≤ᵇ⇒≤ _ _ _)
  asA "Fin 10" ∘ Fin.show =<< Fin.randomIO {n = 10}
  asA "Fin 10" ∘ Fin.show ∘ InBounds.value =<<
    Fin.randomRIO {n = 10}
      (Fin.fromℕ< {m = 3} (ℕ.≤ᵇ⇒≤ _ _ _))
      (Fin.fromℕ< {m = 8} (ℕ.≤ᵇ⇒≤ _ _ _))
      (ℕ.≤ᵇ⇒≤ _ _ _)
  asA "Vec≤ Integer 10" ∘ Vec≤.show (ℤ.show ∘ InBounds.value) =<< Vec≤.randomIO (ℤ.randomRIO -[1+ 10 ] (+ 11) -≤+) 10
  asA "Vec Float 5" ∘ Vec.show (Float.show ∘ InBounds.value) =<< Vec.randomIO (Float.randomRIO -20.0 20.0 _) 5
  asA "String≤ 20" ∘ String.show =<< RangedString≤.randomIO ' ' '~' [ ℕ.≤ᵇ⇒≤ _ _ _ ] 20

random_values

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main hello world < input > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

name: io
include: ../../../src/ .

hello
my
name
is
Agda
exit

echo< echo> hello
echo< echo> my
echo< echo> name
echo< echo> is
echo< echo> Agda
echo< 

{-# OPTIONS --guardedness #-}
module Main where
open import Data.String.Base
open import Function.Base using (_$_; case_of_)
open import IO
open import System.Exit using (exitSuccess)
main : Main
main = run $ do
  -- Ensure no buffering so that the prompt "echo< "
  -- gets outputed immediately
  hSetBuffering stdout noBuffering
  forever $ do
    putStr "echo< "
    -- Get a line from the user and immediately inspect it
    -- If it's a magic "exit" keyword then we exit, otherwise
    -- we print the echo'd message and let the `forever` action
    -- continue
    str ← getLine
    case str of λ where
      "exit" → exitSuccess
      _ → putStrLn ("echo> " ++ str)

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main hello world > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

Main
hello world
hello back!

name: environment
include: ../../../src/ .

{-# OPTIONS --guardedness #-}
module Main where
open import Data.Maybe.Base using (fromMaybe)
open import Data.String.Base using (unwords)
open import IO
open import Function.Base using (_$_)
open import System.Environment
main : Main
main = run $ do
  prog ← getProgName
  putStrLn prog
  args ← getArgs
  putStrLn $ unwords args
  let var = "AGDA_STDLIB_ENVIRONMENT_TEST"
  setEnv var "hello back!"
  msg ← lookupEnv var
  unsetEnv var
  putStrLn $ fromMaybe ":(" msg

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

Creating tmp1
Creating tmp2
Saw _build
Saw tmp1
Saw tmp2
Removing tmp1
Removing tmp2

name: directory
include: ../../../src/ .

{-# OPTIONS --guardedness #-}
module Main where
open import Data.Bool.Base using (true; false)
open import Data.List.Base as List using (_∷_; [])
import Data.List.Sort as Sort
open import Data.String.Base using (_++_; unwords)
import Data.String.Properties as Stringₚ
open import IO
open import Function.Base using (_$_)
open import Relation.Binary.Bundles using (DecTotalOrder)
import Relation.Binary.Construct.On as On
open import System.Directory
open import System.FilePath.Posix
decTotalOrder : DecTotalOrder _ _ _
decTotalOrder =
  On.decTotalOrder Stringₚ.≤-decTotalOrder-≈
                   (getFilePath {n = Nature.relative})
open Sort decTotalOrder using (sort)
main : Main
main = run $ do
  let dirs = "tmp1" ∷ "tmp2" ∷ []
  List.forM′ dirs $ λ d → do
    putStrLn $ "Creating " ++ d
    createDirectory (mkFilePath d)
  ds ← listDirectory (mkFilePath ".")
  List.forM′ (sort ds) $ λ d → do
    true ← doesDirectoryExist d
      where false → pure _
    let str = getFilePath d
    putStrLn $ "Saw " ++ str
  List.forM′ dirs $ λ d → do
    putStrLn $ unwords $ "Removing" ∷ d ∷ []
    removeDirectory (mkFilePath d)

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main hello world > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

Classic blue on white
White on bright blue
Bold bright yellow on bright blue
Italic bright red on yellow
PARTYYYY

name: ansi
include: ../../../src/ .

{-# OPTIONS --guardedness #-}
module Main where
open import Data.List.Base using ([]; _∷_)
open import IO.Base
open import IO.Finite
open import Function.Base using (_$_)
open import System.Console.ANSI
main : Main
main = run $ do
  putStrLn $ withCommands (setColour foreground classic blue
                          ∷ setColour background classic white
                          ∷ [])
             "Classic blue on white"
  putStrLn $ withCommands (setColour foreground classic white
                          ∷ setColour background bright blue
                          ∷ [])
             "White on bright blue"
  putStrLn $ withCommands (setWeight bold
                          ∷ setColour foreground bright yellow
                          ∷ setColour background bright blue
                          ∷ [])
             "Bold bright yellow on bright blue"
  putStrLn $ withCommands (setStyle italic
                          ∷ setColour foreground bright red
                          ∷ setColour background classic yellow
                          ∷ [])
             "Italic bright red on yellow"
  putStrLn $ withCommands (setBlinking rapid
                          ∷ setUnderline double
                          ∷ setWeight bold
                          ∷ setColour background classic red
                          ∷ setColour foreground bright black
                          ∷ [])
             "PARTYYYY"

name: standard-library-tests
include: ../src/ .

name: tree
include: ../../../src/ .

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

standard-library
 ├ Agda
 │  ├ Haskell
 │  │  ├ Haskell (bootstrap)
 │  │  └ C
 │  ├ cabal
 │  │  └ Haskell
 │  │     ├ Haskell (bootstrap)
 │  │     └ C
 │  ├ alex
 │  │  └ Haskell
 │  │     ├ Haskell (bootstrap)
 │  │     └ C
 │  └ happy
 │     └ Haskell
 │        ├ Haskell (bootstrap)
 │        └ C
 ├ cabal
 │  └ Haskell
 │     ├ Haskell (bootstrap)
 │     └ C
 └ Haskell
    ├ Haskell (bootstrap)
    └ C

{-# OPTIONS --guardedness --sized-types #-}
module Main where
open import Data.List.Base using (_∷_; [])
open import Data.String.Base using (String; unlines)
open import Data.Tree.Rose
open import Data.Tree.Rose.Show
open import IO.Base
open import IO.Finite
open import Function.Base using (_$_; id)
dependencies : Rose String _
dependencies = node "standard-library"
  $ agda
  ∷ cabal
  ∷ haskell
  ∷ [] where
  haskell : Rose String _
  haskell = node "Haskell"
    $ node "Haskell (bootstrap)" []
    ∷ node "C" []
    ∷ []
  cabal : Rose String _
  cabal = node "cabal" (haskell ∷ [])
  agda : Rose String _
  agda = node "Agda"
    $ haskell
    ∷ cabal
    ∷ node "alex" (haskell ∷ [])
    ∷ node "happy" (haskell ∷ [])
    ∷ []
main : Main
main = run $ do
  putStrLn $ unlines $ showSimple id dependencies

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

name: reflection
include: ../../../src/ .

Data.List.Base.map : Π ({A.a} : Agda.Primitive.Level) (Π ({A} : (Set (var 0))) (Π ({B.b} : Agda.Primitive.Level) (Π ({B} : (Set (var 0))) (Π (_ : (Π (_ : (var 2)) (var 1))) (Π (_ : (Agda.Builtin.List.List {var 4} (var 3))) (Agda.Builtin.List.List {var 3} (var 2)))))))
Data.List.Base.map = function {[ {A.a : Agda.Primitive.Level}{A : Set (var 0)}{B.b : Agda.Primitive.Level}{B : Set (var 0)}(f : Π (_ : (var 2)) (var 1)) ] {pat-var 4} {pat-var 3} {pat-var 2} {pat-var 1} pat-var 0 Agda.Builtin.List.List.[] → Agda.Builtin.List.List.[] {unknown} {unknown} ; [ {A.a : Agda.Primitive.Level}{A : Set (var 0)}{B.b : Agda.Primitive.Level}{B : Set (var 0)}(f : Π (_ : (var 2)) (var 1))(x : var 3)(xs : Agda.Builtin.List.List {var 5} (var 4)) ] {pat-var 6} {pat-var 5} {pat-var 4} {pat-var 3} pat-var 2 (Agda.Builtin.List.List._∷_ pat-var 1 pat-var 0) → Agda.Builtin.List.List._∷_ {unknown} {unknown} (var 2 (var 1)) (Data.List.Base.map {var 6} {var 5} {var 4} {var 3} (var 2) (var 0)) ;}

{-# OPTIONS --guardedness --sized-types #-}
module Main where
open import Data.List.Base as List using (_∷_; [])
open import Data.String.Base as String using (String)
open import Data.Unit.Base using (⊤)
open import Function.Base using (_$_; id)
open import Reflection using (TC; Term; getType; getDefinition)
open import Reflection.AST.Show
macro
  runTC : TC String → Term → TC ⊤
  runTC tc t = let open Reflection in do
    u ← tc
    unify t (lit (string u))
open import IO.Base hiding (_<$>_)
open import IO.Finite
open import Reflection.TCM.Syntax using (_<$>_)
main : Main
main = run $ do
  let name = quote List.map
  putStr   $ showName name String.++ " : "
  putStrLn $ runTC (showTerm <$> getType name)
  putStr   $ showName name String.++ " = "
  putStrLn $ runTC (showDefinition <$> getDefinition name)

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

name: num
include: ../../../src/ .

0
0
13
1101
42
101010
1024
10000000000
0
0
13
-13
42
-42
1024
-1024
0/1 * 1/14 ≡ 0/14
0/1 * 1/43 ≡ 0/43
0/1 * 1/1025 ≡ 0/1025
13/1 * 1/1 ≡ 13/1
13/1 * 1/43 ≡ 13/43
13/1 * 1/1025 ≡ 13/1025
42/1 * 1/1 ≡ 42/1
42/1 * 1/14 ≡ 42/14
42/1 * 1/1025 ≡ 42/1025
1024/1 * 1/1 ≡ 1024/1
1024/1 * 1/14 ≡ 1024/14
1024/1 * 1/43 ≡ 1024/43
0/1 * 1/14 ≡ 0/1
0/1 * 1/43 ≡ 0/1
0/1 * 1/1025 ≡ 0/1
13/1 * 1/1 ≡ 13/1
13/1 * 1/43 ≡ 13/43
13/1 * 1/1025 ≡ 13/1025
42/1 * 1/1 ≡ 42/1
42/1 * 1/14 ≡ 3/1
42/1 * 1/1025 ≡ 42/1025
1024/1 * 1/1 ≡ 1024/1
1024/1 * 1/14 ≡ 512/7
1024/1 * 1/43 ≡ 1024/43

{-# OPTIONS --guardedness #-}
module Main where
open import Level
open import Data.List.Base using (List; _∷_; [])
open import Data.String using (unwords)
open import IO
open import Function.Base using (_$_)
import Data.Nat.Base as Nat
import Data.Nat.Show as ShowNat
tests : List Nat.ℕ
tests = 0 ∷ 13 ∷ 42 ∷ 2 Nat.^ 10 ∷ []
nats : IO {0ℓ} _
nats = let open ShowNat in
  List.forM′ tests $ λ n → do
    putStrLn (show n)
    putStrLn (showInBase 2 n)
import Data.Integer.Base as Int
import Data.Integer.Show as ShowInt
ints : IO {0ℓ} _
ints = let open Int; open ShowInt in
  List.forM′ tests $ λ n → do
    putStrLn (show (+ n))
    putStrLn (show (- + n))
import Data.Rational.Unnormalised.Base as URat
import Data.Rational.Unnormalised.Show as ShowURat
urats : IO {0ℓ} _
urats = let open URat; open ShowURat in
  List.forM′ tests $ λ num →
    List.forM′ tests $ λ denum →
      unless (num Nat.≡ᵇ denum) $ do
        putStrLn $ unwords
          $ show (mkℚᵘ (Int.+ num) 0)
          ∷ "*"
          ∷ show (mkℚᵘ (Int.+ 1) denum)
          ∷ "≡"
          ∷ show (mkℚᵘ (Int.+ num) denum)
          ∷ []
import Data.Rational.Base as Rat
import Data.Rational.Show as ShowRat
open import Data.Nat.Coprimality
rats : IO {0ℓ} _
rats = let open Rat; open ShowRat in
  List.forM′ tests $ λ num →
    List.forM′ tests $ λ denum →
      unless (num Nat.≡ᵇ denum) $ do
        putStrLn $ unwords
          $ show (normalize num 1)
          ∷ "*"
          ∷ show (normalize 1 (Nat.suc denum))
          ∷ "≡"
          ∷ show (normalize num (Nat.suc denum))
          ∷ []
main : Main
main = run $ do
  nats
  ints
  urats
  rats

{-# OPTIONS --guardedness #-}
module runtests where
open import Data.List.Base as List using (_∷_; [])
open import Data.String.Base using (String; _++_)
open import IO.Base
open import Function.Base
open import Test.Golden
dataTests : TestPool
dataTests = mkTestPool "Data structures"
  $ "appending"
  ∷ "colist"
  ∷ "list"
  ∷ "rational"
  ∷ "rational-unnormalised"
  ∷ "trie"
  ∷ "bytestring"
  ∷ []
systemTests : TestPool
systemTests = mkTestPool "System modules"
  $ "ansi"
  ∷ "directory"
  ∷ "environment"
  ∷ "io"
  ∷ "random"
  ∷ []
showTests : TestPool
showTests = mkTestPool "Show instances"
  $ "num"
  ∷ "reflection"
  ∷ "tree"
  ∷ []
textTests : TestPool
textTests = mkTestPool "Text libraries"
  $ "pretty"
  ∷ "printf"
  ∷ "regex"
  ∷ "tabular"
  ∷ []
monadTests : TestPool
monadTests = mkTestPool "Monad transformers"
  $ "counting"
  ∷ "fibonacci"
  ∷ "pythagorean"
  ∷ "tcm"
  ∷ []
reflectionTests : TestPool
reflectionTests = mkTestPool "Reflection machinery"
  $ "assumption"
  ∷ []
main : Main
main = run $ ignore $ runner
  $ testPaths "data"          dataTests
  ∷ testPaths "monad"         monadTests
  ∷ testPaths "reflection"    reflectionTests
  ∷ testPaths "show"          showTests
  ∷ testPaths "system"        systemTests
  ∷ testPaths "text"          textTests
  ∷ [] where
  testPaths : String → TestPool → TestPool
  testPaths dir pool =
    let testCases = List.map ((dir ++ "/") ++_) (pool .TestPool.testCases)
    in record pool { testCases = testCases }

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

function {[ {A.a : Agda.Primitive.Level}{A : Set (var 0)}{B.b : Agda.Primitive.Level}{B : Set (var 0)}(x : var 2)(y : var 1) ] {pat-var 5} {pat-var 4} {pat-var 3} {pat-var 2} pat-var 1 pat-var 0 → var 0 ;}
function {[ {A.a : Agda.Primitive.Level}{A : Set (var 0)}{B.b : Agda.Primitive.Level}{B : Set (var 0)}(x : var 2)(y : var 1) ] {pat-var 5} {pat-var 4} {pat-var 3} {pat-var 2} pat-var 1 pat-var 0 → var 1 ;}
function {[ {A.a : Agda.Primitive.Level}{A : Set (var 0)}{B.b : Agda.Primitive.Level}{B : Set (var 0)}(x : var 2)(y : var 1)(z : var 2) ] {pat-var 6} {pat-var 5} {pat-var 4} {pat-var 3} pat-var 2 pat-var 1 pat-var 0 → var 2 ;}
function {[ {A.a : Agda.Primitive.Level}{A : Set (var 0)}{B.b : Agda.Primitive.Level}{B : Set (var 0)}(x : Agda.Builtin.List.List {Agda.Primitive._⊔_ (var 3) (var 1)} (Π (_ : (var 2)) (var 1)))(y : var 3)(z : var 2)(a : var 3) ] {pat-var 7} {pat-var 6} {pat-var 5} {pat-var 4} pat-var 3 pat-var 2 pat-var 1 pat-var 0 → var 3 ;}
function {[ {A.a : Agda.Primitive.Level}{A : Set (var 0)}{B.b : Agda.Primitive.Level}{B : Set (var 0)}(x : Π (_ : (var 2)) (Agda.Builtin.List.List {var 2} (var 1)))(y : var 3)(z : var 2)(a : Agda.Builtin.List.List {var 4} (var 3)) ] {pat-var 7} {pat-var 6} {pat-var 5} {pat-var 4} pat-var 3 pat-var 2 pat-var 1 pat-var 0 → var 3 ;}

name: assumption
include: ../../../src/ .

{-# OPTIONS --guardedness #-}
module Main where
open import Data.String.Base using (String)
open import Data.Bool.Base using (if_then_else_)
open import Data.List.Base using (List; []; _∷_; concatMap; map)
open import Data.Maybe.Base using (Maybe; nothing; just)
open import Data.Nat.Base using (ℕ; suc)
open import Data.Product.Base using (_×_; _,_)
open import Level using (Level)
open import Data.Unit.Base using (⊤)
open import Function.Base using (case_of_; _$_)
open import Reflection.TCM hiding (pure)
open import Reflection.AST.Term
open import Reflection.AST.Literal hiding (_≟_)
open import Reflection.AST.Argument using (Arg; unArg; arg)
open import Reflection.AST.DeBruijn
open import Reflection.AST.Show
open import Relation.Nullary.Decidable using (does)
open import Effect.Monad
open RawMonad {{...}}
open import Data.Maybe.Instances
open import Reflection.TCM.Instances
private
  variable
    a b : Level
    A : Set a
    B : Set b
-- As the doc states (cf. https://agda.readthedocs.io/en/latest/language/reflection.html#type-checking-computations)
-- Note that the types in the context are valid in the rest of the context.
-- To use in the current context they need to be weakened by 1 + their position
-- in the list.
-- That is to say that the type of the current goal needs to be strengthened
-- before being compared to the type of the most local variable. The goal
-- indeed lives below that variable's binding site!
searchEntry : ℕ → Type → List (String × Arg Type) → Maybe ℕ
searchEntry n ty [] = nothing
searchEntry n ty ((_ , e) ∷ es) = do
  ty ← strengthen ty
  if does (ty ≟ unArg e)
    then just n
    else searchEntry (suc n) ty es
macro
  assumption : Term → TC ⊤
  assumption hole = do
    asss ← getContext
    goal ← inferType hole
    debugPrint "" 10
      (strErr "Context : "
       ∷ concatMap (λ where (_ , arg info ty) → strErr "\n  " ∷ termErr ty ∷ []) asss)
    let res = searchEntry 0 goal asss
    case res of λ where
      nothing → typeError (strErr "Couldn't find an assumption of type: " ∷ termErr goal ∷ [])
      (just idx) → unify hole (var idx [])
test₀ : A → B → B
test₀ x y = assumption
test₁ : A → B → A
test₁ x y = assumption
test₂ : A → B → B → A
test₂ x y z = assumption
test₃ : List (A → B) → A → B → B → List (A → B)
test₃ x y z a = assumption
test₄ : (A → List B) → A → B → List B → A → List B
test₄ x y z a = assumption
open import IO.Base using (Main; run)
open import IO.Finite
open import IO.Instances
macro
  runTC : TC String → Term → TC ⊤
  runTC tc t = do
    u ← tc
    unify t (lit (string u))
main : Main
main = run $ do
  putStrLn $ runTC (showDefinition <$> getDefinition (quote test₀))
  putStrLn $ runTC (showDefinition <$> getDefinition (quote test₁))
  putStrLn $ runTC (showDefinition <$> getDefinition (quote test₂))
  putStrLn $ runTC (showDefinition <$> getDefinition (quote test₃))
  putStrLn $ runTC (showDefinition <$> getDefinition (quote test₄))

name: tcm
include: ../../../src/ .

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

IO.Base.Main
Π ({a} : Agda.Primitive.Level) (Π (_ : Agda.Builtin.String.String) (IO.Base.IO {var 1} (Data.Unit.Polymorphic.Base.⊤ {var 1})))

{-# OPTIONS --guardedness #-}
module Main where
-- Taken from #1530
open import Data.String.Base using (String)
open import Data.Maybe.Base using (Maybe; nothing; just)
open import Data.Unit using (⊤; tt)
open import Reflection.AST.Literal
open import Reflection.AST.Term
open import Reflection.AST.Show using (showTerm)
open import Reflection.TCM using (TC; inferType; unify)
open import Effect.Monad
open RawMonad {{...}} public using (pure; _>>=_; _>>_)
open import Data.Maybe.Instances
open import Reflection.TCM.Instances
macro
   goalErr : Term → Term → TC ⊤
   goalErr t goal = do
     goalType ← inferType t
     unify goal (lit (string (showTerm goalType)))
open import IO.Base hiding (_>>=_; _>>_)
open import IO.Finite
open import IO.Instances
open import Function.Base using (_$_)
main : Main
main = run $ do
  putStrLn (goalErr main)
  putStrLn (goalErr putStrLn)

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

name: pythagorean
include: ../../../src/ .

3² + 4² = 5²
4² + 3² = 5²
5² + 12² = 13²
6² + 8² = 10²
7² + 24² = 25²
8² + 6² = 10²
8² + 15² = 17²
9² + 12² = 15²
9² + 40² = 41²
10² + 24² = 26²
11² + 60² = 61²
12² + 5² = 13²
12² + 9² = 15²
12² + 16² = 20²
12² + 35² = 37²
13² + 84² = 85²
14² + 48² = 50²
15² + 8² = 17²
15² + 20² = 25²
15² + 36² = 39²
16² + 12² = 20²
16² + 30² = 34²
16² + 63² = 65²
18² + 24² = 30²
18² + 80² = 82²
20² + 15² = 25²
20² + 21² = 29²
20² + 48² = 52²
21² + 20² = 29²
21² + 28² = 35²
21² + 72² = 75²
24² + 7² = 25²
24² + 10² = 26²
24² + 18² = 30²
24² + 32² = 40²
24² + 45² = 51²
24² + 70² = 74²
25² + 60² = 65²
27² + 36² = 45²
28² + 21² = 35²
28² + 45² = 53²
28² + 96² = 100²
30² + 16² = 34²
30² + 40² = 50²
30² + 72² = 78²
32² + 24² = 40²
32² + 60² = 68²
33² + 44² = 55²
33² + 56² = 65²
35² + 12² = 37²
35² + 84² = 91²
36² + 15² = 39²
36² + 27² = 45²
36² + 48² = 60²
36² + 77² = 85²
39² + 52² = 65²
39² + 80² = 89²
40² + 9² = 41²
40² + 30² = 50²
40² + 42² = 58²
40² + 75² = 85²
42² + 40² = 58²
42² + 56² = 70²
44² + 33² = 55²
45² + 24² = 51²
45² + 28² = 53²
45² + 60² = 75²
48² + 14² = 50²
48² + 20² = 52²
48² + 36² = 60²
48² + 55² = 73²
48² + 64² = 80²
51² + 68² = 85²
52² + 39² = 65²
54² + 72² = 90²
55² + 48² = 73²
56² + 33² = 65²
56² + 42² = 70²
57² + 76² = 95²
60² + 11² = 61²
60² + 25² = 65²
60² + 32² = 68²
60² + 45² = 75²
60² + 63² = 87²
60² + 80² = 100²
63² + 16² = 65²
63² + 60² = 87²
64² + 48² = 80²
65² + 72² = 97²
68² + 51² = 85²
70² + 24² = 74²
72² + 21² = 75²
72² + 30² = 78²
72² + 54² = 90²
72² + 65² = 97²
75² + 40² = 85²
76² + 57² = 95²
77² + 36² = 85²
80² + 18² = 82²
80² + 39² = 89²
80² + 60² = 100²
84² + 13² = 85²
84² + 35² = 91²
96² + 28² = 100²

{-# OPTIONS --guardedness #-}
module Main where
open import Data.Bool.Base using (if_then_else_)
open import Data.List.Base using (List; []; _∷_; catMaybes)
open import Data.List.Effectful.Transformer
open import Data.List.Effectful
open import Data.Maybe.Base using (just; nothing)
open import Data.Maybe.Effectful.Transformer
open import Data.Nat.Base using (ℕ; zero; suc; _+_; _^_; _≡ᵇ_)
open import Data.Nat.Show using (show)
open import Data.Product.Base using (_×_; _,_)
open import Data.String.Base using (_++_)
open import Function.Base using (_$_)
open import Effect.Applicative
open import Effect.Monad
open import Effect.Monad.Identity
open import IO.Base using (Main; run)
open import IO.Finite using (putStrLn)
open import Data.List.Instances
open import Data.Maybe.Instances
open import Effect.Monad.Identity.Instances
open import IO.Instances
open RawMonad {{...}}
open RawApplicativeZero {{...}} using (guard)
open TraversableA {{...}}
1⋯100 : List ℕ
1⋯100 = rangeFrom 1 100 where
  rangeFrom : (start steps : ℕ) → List ℕ
  rangeFrom start zero    = []
  rangeFrom start (suc n) = start ∷ rangeFrom (suc start) n
triples : MaybeT (ListT Identity) (ℕ × ℕ × ℕ)
triples = do
  let range = mkMaybeT (mkListT (pure (pure <$> 1⋯100)))
  p ← range
  q ← range
  r ← range
  mkMaybeT (mkListT (pure (pure (guard (p ^ 2 + q ^ 2 ≡ᵇ r ^ 2)))))
  pure (p , q , r)
main : Main
main = run
     $ ignore $ forA (catMaybes $ runIdentity $ runListT $ runMaybeT triples)
     $ λ (p , q , r) → do let sqStr = λ x → show x ++ "²"
                          putStrLn (sqStr p ++ " + " ++ sqStr q ++ " = " ++ sqStr r)

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

name: fibonacci
include: ../../../src/ .

fib 0 = 0
fib 1 = 1
fib 2 = 1
fib 3 = 2
fib 5 = 5
fib 6 = 8
fib 7 = 13
fib 8 = 21
fib 9 = 34
fib 10 = 55

{-# OPTIONS --guardedness --rewriting #-}
module Main where
open import Data.Bool.Base using (Bool; true; false)
open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Data.Nat.Show using (show)
open import Data.Product.Base using (_,_)
open import Data.String.Base using (String; _++_)
open import Data.Default
open import Debug.Trace using (trace)
open import IO.Base using (Main; run)
open import IO.Finite using (putStrLn)
open import Function.Base using (_$_)
open import Effect.Monad
open import Effect.Monad.State
open import Effect.Monad.State.Instances
open import Effect.Monad.Identity.Instances
open import IO.Instances
open RawMonad {{...}}
open RawMonadState {{...}}
record Fib : Set where
  field tracing : Bool
        index   : ℕ
        current : ℕ
        next    : ℕ
open Fib
initFib : Bool → Fib
initFib b = record
  { tracing = b
  ; index = 0
  ; current = 0
  ; next = 1
  }
displayFib : ℕ → ℕ → String
displayFib idx fibn = "fib " ++ show idx ++ " = " ++ show fibn
fibM : ℕ → State Fib ℕ
fibM 0 = gets current
fibM (suc n) = do
  b ← gets tracing
  when b $ do
    idx ← gets index
    fibn ← gets current
    trace (displayFib idx fibn) (pure _)
  modify (λ r → record r { index = suc (index r) ; current = next r ; next = next r + current r })
  fibM n
fib : ℕ → Bool → ℕ
fib n b = evalState (fibM n) (initFib b)
fibStr : ℕ → {{WithDefault false}} → String
fibStr n {{b}} = displayFib n (fib n (value b))
main : Main
main = run $ do
  putStrLn $ fibStr 0
  putStrLn $ fibStr 1
  putStrLn $ fibStr 2
  putStrLn $ fibStr 3
  putStrLn $ fibStr 5
  putStrLn $ fibStr 6
  putStrLn $ fibStr 7
  putStrLn $ fibStr 8
  putStrLn $ fibStr 9
  putStrLn $ fibStr 10

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

First: 1
Second: 3
Third: 8

name: counting
include: ../../../src/ .

{-# OPTIONS --guardedness #-}
module Main where
open import Data.Nat.Base
open import Data.Nat.Show using (show)
open import Data.Product.Base using (_,_)
open import Data.String.Base using (String; _++_)
open import IO.Base as IO using (IO; Main; run)
open import IO.Finite using (putStrLn)
open import IO.Effectful as IO
open import Function.Base using (_∘′_; _$_; const)
open import Level using (Lift; 0ℓ; lift; lower)
open import Effect.Monad
open import Effect.Monad.Reader.Transformer as Reader
open import Effect.Monad.State.Transformer as State
open import Effect.Monad.IO
open import IO.Instances
open import Effect.Monad.IO.Instances
open import Effect.Monad.State.Instances
open import Effect.Monad.Reader.Instances
open RawMonad {{...}}
open RawMonadReader {{...}}
open RawMonadState {{...}}
open RawMonadIO {{...}}
step : ∀ {M : Set Level.zero → Set (Level.suc Level.zero)} →
  {{RawMonad M}} →
  {{RawMonadReader String M}} →
  {{RawMonadState ℕ M}} →
  {{RawMonadIO M}} →
  (ℕ → ℕ) →
  M _
step f = do
  modify f
  str ← ask
  n ← get
  let msg = str ++ show n
  liftIO (putStrLn msg)
script : ∀ {M} →
  {{RawMonad M}} →
  {{RawMonadReader String M}} →
  {{RawMonadState ℕ M}} →
  {{RawMonadIO M}} →
  M _
script = do
  step suc
  local (const "Second: ") $ step (3 *_)
  local (const "Third: ") $ step (2 ^_)
it : ∀ {a} {A : Set a} → {{A}} → A
it {{x}} = x
main : Main
main = run $ evalStateT it (runReaderT script "First: ") 0

name: trie
include: ../../../src/ .

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

ID "fix"
ID "f"
ID "x"
EQ
LET
ID "b"
EQ
ID "fix"
ID "f"
IN
LPAR
ID "f"
ID "b"
RPAR
ID "x"

-- Taken from README.Data.Trie.NonDependent
{-# OPTIONS --guardedness --sized-types #-}
module Main where
open import Level
open import Data.Unit
open import Data.Bool
open import Data.Char         as Char hiding (show)
import Data.Char.Properties   as Char
open import Data.List.Base    as List using (List; []; _∷_)
open import Data.List.Fresh   as List# using (List#; []; _∷#_)
open import Data.Maybe        as Maybe
open import Data.Product      as Prod
open import Data.String       as String using (String; unlines; _++_)
open import Data.These        as These
open import Function.Base using (case_of_; _$_; _∘′_; id; _on_)
open import Relation.Nary
open import Relation.Binary.Core using (Rel)
open import Relation.Nullary.Decidable using (¬?)
open import Data.Trie Char.<-strictTotalOrder
open import Data.Tree.AVL.Value
open import IO.Base
open import IO.Finite
record Lexer t : Set (suc t) where
  field
    Tok : Set t
  Keyword : Set t
  Keyword = String × Tok
  Distinct : Rel Keyword 0ℓ
  Distinct a b = ⌊ ¬? ((proj₁ a) String.≟ (proj₁ b)) ⌋
  field
    keywords : List# Keyword Distinct
    breaking : Char → ∃ λ b → if b then Maybe Tok else Lift _ ⊤
    default  : String → Tok
module _ {t} (L : Lexer t) where
  open Lexer L
  tokenize : String → List Tok
  tokenize = start ∘′ String.toList where
   mutual
    Keywords : Set _
    Keywords = Trie (const _ Tok) _
    init : Keywords
    init = fromList $ List.map (Prod.map₁ String.toList) $ proj₁ $ List#.toList keywords
    start : List Char → List Tok
    start = loop [] init
    loop : (acc  : List Char)  → -- chars read so far in this token
           (toks : Keywords)   → -- keyword candidates left at this point
           (input : List Char) → -- list of chars to tokenize
           List Tok
    loop acc toks []         = push acc []
    loop acc toks (c ∷ cs)   = case breaking c of λ where
      (true , m)  → push acc $ maybe′ _∷_ id m $ start cs
      (false , _) → case lookupValue toks (c ∷ []) of λ where
        (just tok) → tok ∷ start cs
        nothing    → loop (c ∷ acc) (lookupTrie toks c) cs
    push : List Char → List Tok → List Tok
    push [] ts = ts
    push cs ts = default (String.fromList (List.reverse cs)) ∷ ts
module LetIn where
  data TOK : Set where
    LET EQ IN : TOK
    LPAR RPAR : TOK
    ID : String → TOK
  show : TOK → String
  show LET    = "LET"
  show EQ     = "EQ"
  show IN     = "IN"
  show LPAR   = "LPAR"
  show RPAR   = "RPAR"
  show (ID x) = "ID \"" ++ x ++ "\""
  keywords : List# (String × TOK) (λ a b → ⌊ ¬? ((proj₁ a) String.≟ (proj₁ b)) ⌋)
  keywords =  ("let" , LET)
           ∷# ("="   , EQ)
           ∷# ("in"  , IN)
           ∷# []
  breaking : Char → ∃ (λ b → if b then Maybe TOK else Lift 0ℓ ⊤)
  breaking c = if isSpace c then true , nothing else parens c where
    parens : Char → _
    parens '(' = true , just LPAR
    parens ')' = true , just RPAR
    parens _   = false , _
  default : String → TOK
  default = ID
letIn : Lexer 0ℓ
letIn = record { LetIn }
main : Main
main = run $ do
  let open LetIn
  putStrLn $ unlines $ List.map show $
    tokenize letIn "fix f x = let b = fix f in (f b) x"

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

name: rational
include: ../../../src/ .

[-4, -3, -2, -1, 0, 1, 2, 3]
[-3, -2, -1, 0, 1, 2, 3, 4]
[-3, -2, -1, 0, 0, 1, 2, 3]
[-4, -3, -2, 0, 0, 2, 3, 4]
[5/10, 7/10, 5/10, 3/10, 3/10, 5/10, 7/10, 5/10]

{-# OPTIONS --guardedness --sized-types #-}
module Main where
open import Data.Integer.Base using (ℤ; +_)
import Data.Integer.Show as ℤ
open import Data.List.Base as List using (List; _∷_; [])
import Data.Nat.Base
open import Data.Rational.Unnormalised.Base
  using (ℚᵘ; -_; _/_; floor; ceiling; truncate; round; fracPart)
import Data.Rational.Unnormalised.Show as ℚᵘ
open import Data.String.Base as String using (String)
open import IO.Base
open import IO.Finite
open import Function.Base using (_$_)
testList : List ℚᵘ
testList = - (+ 35 / 10) ∷ - (+ 27 / 10) ∷ - (+ 15 / 10) ∷ - (+ 3 / 10)
         ∷ + 3 / 10 ∷ + 15 / 10 ∷ + 27 / 10 ∷ + 35 / 10 ∷ []
showInts : List ℤ → String
showInts is = String.concat
            $ "["
            ∷ String.intersperse ", " (List.map ℤ.show is)
            ∷ "]" ∷ []
showRats : List ℚᵘ → String
showRats ps = String.concat
            $ "["
            ∷ String.intersperse ", " (List.map ℚᵘ.show ps)
            ∷ "]" ∷ []
main : Main
main = run $ do
  putStrLn $ showInts (List.map floor testList)
  putStrLn $ showInts (List.map ceiling testList)
  putStrLn $ showInts (List.map truncate testList)
  putStrLn $ showInts (List.map round testList)
  putStrLn $ showRats (List.map fracPart testList)

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

name: rational
include: ../../../src/ .

[-4, -3, -2, -1, 0, 1, 2, 3]
[-3, -2, -1, 0, 1, 2, 3, 4]
[-3, -2, -1, 0, 0, 1, 2, 3]
[-4, -3, -2, 0, 0, 2, 3, 4]
[1/2, 7/10, 1/2, 3/10, 3/10, 1/2, 7/10, 1/2]

{-# OPTIONS --guardedness --sized-types #-}
module Main where
open import Data.Integer.Base using (ℤ; +_)
import Data.Integer.Show as ℤ
open import Data.List.Base as List using (List; _∷_; [])
import Data.Nat.Base
open import Data.Rational.Base
  using (ℚ; -_; _/_; floor; ceiling; truncate; round; fracPart)
import Data.Rational.Show as ℚ
open import Data.String.Base as String using (String)
open import IO.Base
open import IO.Finite
open import Function.Base using (_$_)
testList : List ℚ
testList = - (+ 35 / 10) ∷ - (+ 27 / 10) ∷ - (+ 15 / 10) ∷ - (+ 3 / 10)
         ∷ + 3 / 10 ∷ + 15 / 10 ∷ + 27 / 10 ∷ + 35 / 10 ∷ []
showInts : List ℤ → String
showInts is = String.concat
            $ "["
            ∷ String.intersperse ", " (List.map ℤ.show is)
            ∷ "]" ∷ []
showRats : List ℚ → String
showRats ps = String.concat
            $ "["
            ∷ String.intersperse ", " (List.map ℚ.show ps)
            ∷ "]" ∷ []
main : Main
main = run $ do
  putStrLn $ showInts (List.map floor testList)
  putStrLn $ showInts (List.map ceiling testList)
  putStrLn $ showInts (List.map truncate testList)
  putStrLn $ showInts (List.map round testList)
  putStrLn $ showRats (List.map fracPart testList)

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

name: list
include: ../../../src/ .

[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19]
[14, 36, 20, 16, 15, 196, 13, 12, 11, 20, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0]
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11, 12, 13, 14, 15, 16, 20, 20, 36, 196]
[14, 18, 17, 16, 15, 392, 13, 12, 11, 20, 9, 11, 7, 6, 5, 4, 3, 2, 1, 0]
[0, 1, 2, 3, 4, 5, 6, 7, 9, 11, 11, 12, 13, 14, 15, 16, 17, 18, 20, 392]

{-# OPTIONS --guardedness --sized-types #-}
module Main where
open import Level
open import Data.List.Base as List using (List; _∷_; []; _++_; reverse)
open import Data.List.Zipper
import Data.List.Sort as Sort
open import Data.Maybe.Base
open import Data.Nat.Base
open import Data.Nat.Show using (show)
import Data.Nat.Properties as ℕₚ
open import Data.String.Base as String using (String)
import Data.Vec.Base as Vec
open import Codata.Sized.Stream using (nats; take)
open Sort ℕₚ.≤-decTotalOrder
open import IO.Base
open import IO.Finite
open import Function.Base using (_$_; _∘_)
private
  variable
    a : Level
    A : Set a
data Direction : Set where Left Right : Direction
turn : Direction → Zipper A → Zipper A
turn Left  zip = fromMaybe zip (left zip)
turn Right zip = fromMaybe zip (right zip)
follow : List Direction → Zipper A → Zipper A
follow dirs init = go dirs init where
  go : List Direction → Zipper A → Zipper A
  go []         zip = zip
  go (d ∷ dirs) zip = go dirs (turn d zip)
updateFocus : (A → A) → Zipper A → Zipper A
updateFocus f (mkZipper ctx (a ∷ val)) = mkZipper ctx (f a ∷ val)
updateFocus f zip = zip
updateAt : List Direction → (A → A) → Zipper A → Zipper A
updateAt dirs f = updateFocus f ∘ follow dirs
applyAt : List Direction → (A → A) → List A → List A
applyAt dirs f xs = toList
                  $ updateFocus f
                  $ follow dirs
                  $ fromList xs
someNats : List ℕ
someNats = Vec.toList $ take 20 $ nats
otherNats : List ℕ
otherNats
  = applyAt (Right ∷ Right ∷ [])                   (3 +_)
  $ applyAt (List.replicate 10 Right ++ Left ∷ []) (10 +_)
  $ applyAt (List.replicate 10 Left)               (_∸ 5)
  $ applyAt (Left ∷ Right ∷ Right ∷ Left ∷ [])     (2 *_)
  $ applyAt (List.replicate 5 Right)               (_^ 2)
  $ List.reverse someNats
chaoticNats : List ℕ
chaoticNats
  = toList
  $ updateAt (Right ∷ Right ∷ [])                   (3 +_)
  $ updateAt (List.replicate 10 Right ++ Left ∷ []) (10 +_)
  $ updateAt (List.replicate 10 Left)               (_∸ 5)
  $ updateAt (Left ∷ Right ∷ Right ∷ Left ∷ [])     (2 *_)
  $ updateAt (List.replicate 5 Right)               (_^ 2)
  $ fromList
  $ List.reverse someNats
showNats : List ℕ → String
showNats ns = String.concat
            $ "["
            ∷ String.intersperse ", " (List.map show ns)
            ∷ "]" ∷ []
main : Main
main = run $ do
  putStrLn $ showNats someNats
  putStrLn $ showNats otherNats
  putStrLn $ showNats $ sort otherNats
  putStrLn $ showNats chaoticNats
  putStrLn $ showNats $ sort chaoticNats

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

λ 0
(λ 0) ((λ 0) (λ 0) ((λ 0) (λ 0)))
(λ 0) (λ 0) ((λ 0) (λ 0))
(λ 0) ((λ 0) (λ 0))
(λ 0) (λ 0)
λ 0

name: colist
include: ../../../src/ .

{-# OPTIONS --guardedness --sized-types #-}
module Main where
open import Level using (0ℓ)
open import Size
open import Data.Bool.Base using (Bool; true; false; if_then_else_)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Fin
import Data.Fin.Show as Fin
open import Data.String.Base using (String; _++_; parens)
open import Data.Unit.Polymorphic.Base using (⊤)
open import Codata.Sized.Thunk
open import Function.Base using (_$_; _∘_; id)
open import Relation.Nullary
open import Codata.Musical.Notation
open import Codata.Sized.Colist using (Colist; _∷_; [])
open import Codata.Musical.Colist renaming (Colist to Colist♩) using (_∷_; [])
open import Codata.Musical.Conversion
variable
  i : Size
  m n : ℕ
  A : Set
data Lam (n : ℕ) : Set where
  var : Fin n → Lam n
  app : Lam n → Lam n → Lam n
  lam : Lam (suc n) → Lam n
data Loc : Set where appL appR lam : Loc
appParens : Loc → String → String
appParens appR str = parens str
appParens _ str = str
lamParens : Loc → String → String
lamParens lam str = str
lamParens _ str = parens str
show : Loc → Lam n → String
show i (var v)   = Fin.show v
show i (app f t) = appParens i $ show appL f ++ " " ++ show appR t
show i (lam b)   = lamParens i $ "λ " ++ show lam b
variable
  b f t : Lam n
_∙_ : (Fin m → A) → A → Fin (suc m) → A
(ρ ∙ v) zero    = v
(ρ ∙ v) (suc k) = ρ k
rename : (Fin m → Fin n) → Lam m → Lam n
rename ρ (var v)   = var (ρ v)
rename ρ (app f t) = app (rename ρ f) (rename ρ t)
rename ρ (lam b)   = lam (rename ((suc ∘ ρ) ∙ zero) b)
subst : (Fin m → Lam n) → Lam m → Lam n
subst ρ (var v)   = ρ v
subst ρ (app f t) = app (subst ρ f) (subst ρ t)
subst ρ (lam b)   = lam (subst ((rename suc ∘ ρ) ∙ var zero) b)
data Redex {n} : Lam n → Set where
  here : ∀ b t → Redex (app (lam b) t)
  lam  : Redex b → Redex (lam b)
  appL : Redex f → ∀ t → Redex (app f t)
  appR : ∀ f → Redex t → Redex (app f t)
redex : ∀ {n} (t : Lam n) → Dec (Redex t)
redex (var v)             = no (λ ())
redex (app (lam b) t)     = yes (here b t)
redex (app f@(var _) t)   with redex t
... | yes rt = yes (appR f rt)
... | no nrt = no λ where (appR _ rt) → nrt rt
redex (app f@(app _ _) t) with redex f | redex t
... | yes rf | _ = yes (appL rf t)
... | _ | yes rt = yes (appR f rt)
... | no nrf | no nrt = no λ where
  (appL rf _) → nrf rf
  (appR _ rt) → nrt rt
redex (lam b) with redex b
... | yes rb = yes (lam rb)
... | no nrb = no λ where (lam rb) → nrb rb
fire : Redex {n} t → Lam n
fire (here b t)  = subst (var ∙ t) b
fire (lam rt)    = lam (fire rt)
fire (appL rf t) = app (fire rf) t
fire (appR f rt) = app f (fire rt)
eval : Lam n → Colist (Lam n) i
eval t with redex t
... | yes rt = t ∷ λ where .force → eval (fire rt)
... | no nrt = t ∷ λ where .force → []
open import IO.Base
open import IO.Finite
trace : Colist♩ (Lam n) → IO {0ℓ} ⊤
trace []       = pure _
trace (t ∷ ts) = seq (♯ putStrLn (show lam t))
                     (♯ trace (♭ ts))
`id : Lam 0
`id = lam (var (# 0))
main : Main
main = run $ do
  trace (Colist.toMusical $ eval `id)
  trace (Colist.toMusical $ eval (app `id (app (app `id `id) (app `id `id))))

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

"\SOH\STX\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\ETX"
------------------------------------------------------------------------
1 = 0b00000001
1 = 0x01
1 = 1
144 = 0b10010000
144 = 0x90
144 = 144
------------------------------------------------------------------------
2 = 0b0000000000000000000000000000000000000000000000000000000000000010
2 = 0x00000002
2 = 2
------------------------------------------------------------------------
3 = 0b0000000000000000000000000000000000000000000000000000000000000011
3 = 0x00000003
3 = 3
------------------------------------------------------------------------
2024 = 0b0000000000000000000000000000000000000000000000000000011111101000
2024 = 0x000007e8
2024 = 2024

name: bytestring
include: ../../../src/ .

{-# OPTIONS --guardedness #-}
module Main where
open import Agda.Builtin.FromNat
open import Data.Bytestring.Base as Bytestring
open import Data.Bytestring.Builder.Base
open import Data.List.Base using ([]; _∷_)
import Data.Nat.Literals; instance numberNat = Data.Nat.Literals.number
open import Data.Product.Base using (_×_; _,_)
open import Data.String using (String; _++_; fromVec)
open import Data.Unit.Base using (⊤; tt)
import Data.Vec.Base as Vec
open import Data.Word8.Base as Word8
import Data.Word8.Show as Word8
import Data.Word8.Literals; instance numberWord8 = Data.Word8.Literals.number
open import Data.Word64.Base as Word64 using (Word64)
import Data.Word64.Unsafe as Word64
import Data.Word64.Show as Word64
import Data.Word64.Literals; instance numberWord64 = Data.Word64.Literals.number
open import Function.Base using (_$_)
open import IO.Base
open import IO.Finite
1⋯3 : Bytestring
1⋯3 = toBytestring
    $ List.concat
    $ word8 1
    ∷ word64LE 2
    ∷ word64BE 3
    ∷ []
1,⋯,3 : Word8 × Word64 × Word64
1,⋯,3 = getWord8 1⋯3 0
      , getWord64LE 1⋯3 1
      , getWord64BE 1⋯3 9
main : Main
main = run $ do
  let separation = fromVec (Vec.replicate 72 '-')
  putStrLn (Bytestring.show 1⋯3)
  putStrLn separation
  let (one , two , three) = 1,⋯,3
  let word8test : Word8 → IO _
      word8test w = do
        putStrLn (Word8.show w ++ " = " ++ Word8.showBits w)
        putStrLn (Word8.show w ++ " = " ++ Word8.showHexa w)
        putStrLn (Word8.show w ++ " = " ++ Word8.show (Word8.fromBits (Word8.toBits w)))
  let word64test : Word64 → IO _
      word64test w = do
        putStrLn separation
        putStrLn (Word64.show w ++ " = " ++ Word64.showBits w)
        putStrLn (Word64.show w ++ " = " ++ Word64.showHexa w)
        putStrLn (Word64.show w ++ " = " ++ Word64.show (Word64.fromBits (Word64.toBits w)))
  word8test one
  word8test (Word8.fromℕ 144)
  word64test two
  word64test three
  word64test (Word64.fromℕ 2024)

$1 --compile-dir=../../_build -c Main.agda > log
./../../_build/Main < input > output
rm ../../_build/Main
rm ../../_build/MAlonzo/Code/Main*

helLo
teST
parcequecestnotrePROJEEET

hel
te
parcequecestnotre

name: list
include: ../../../src/ .

{-# OPTIONS --safe --cubical-compatible #-}
module TakeWhile where
open import Level
open import Data.List.Base hiding (takeWhile)
open import Data.List.Relation.Unary.All as List using ([]; _∷_)
open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_; refl)
open import Data.List.Relation.Ternary.Appending.Propositional
open import Data.Product.Base using (_×_; proj₁)
open import Data.Maybe.Relation.Unary.All as Maybe using (nothing; just)
import Data.Nat
open import Relation.Unary
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Relation.Nullary.Product
-- Original bug reported in #1765 by James Wood
_ : Appending (3 ∷ []) (2 ∷ []) (3 ∷ 2 ∷ [])
_ = P.refl ∷ []++ P.refl ∷ []
variable
  a p : Level
  A : Set a
  P : A → Set p
infix 1 _,_,_
record TakeWhile {A : Set a} (P : A → Set p) xs : Set (a ⊔ p) where
  constructor _,_,_
  field
    {prefix rest} : List A
    goodPrefix : List.All P prefix
    isPrefix : Appending prefix rest xs
    isBiggest : Maybe.All (proj₁ ⊢ ∁ P) (uncons rest)
open TakeWhile public
takeWhile : Decidable P → Π[ TakeWhile P ]
takeWhile P? [] = [] , []++ [] , nothing
takeWhile P? (x ∷ xs) with P? x
... | yes px = let (pxs' , prf , biggest) = takeWhile P? xs in
               px ∷ pxs' , P.refl ∷ prf , biggest
... | no ¬px = [] , []++ refl P.refl , just ¬px
open import Data.Char
open import Data.String using (toList)
lower? : (c : Char) → Dec ('a' ≤ c × c ≤ 'z')
lower? c = 'a' ≤? c ×-dec c ≤? 'z'
_ : takeWhile lower? (toList "helLo")
  ≡ record { prefix = toList "hel"
           ; isPrefix = P.refl ∷ P.refl ∷ P.refl ∷ []++ P.refl ∷ P.refl ∷ []
           }
_ = P.refl

{-# OPTIONS --guardedness #-}
module Main where
open import Data.List.Base using (replicate)
open import Data.String using (toList; fromList)
open import IO
open import Function.Base using (_$_)
open import TakeWhile
main : Main
main = run $ List.sequence′ $ replicate 3 $ do
  str ← getLine
  let taken = takeWhile lower? (toList str)
  putStrLn $ fromList (taken .prefix)

INTERACTIVE ?= --interactive
runtests: runtests.agda
	rm -f _build/runtests
	rm -f _build/MAlonzo/Code/Qruntests*
	$(AGDA) --compile-dir=_build/ -c runtests.agda
test: runtests
	./_build/runtests $(AGDA_EXEC) $(INTERACTIVE) --timing --failure-file failures --only $(only)
retest: runtests
	./_build/runtests $(AGDA_EXEC) $(INTERACTIVE) --timing --failure-file failures --only-file failures --only $(only)

name: standard-library-2.1
include: src
flags:
  --warning=noUnsupportedIndexedMatch

resolver: nightly-2023-08-27
compiler: ghc-9.6.2
compiler-check: match-exact
packages:
- '.'

resolver: lts-21.7
compiler: ghc-9.4.5
compiler-check: match-exact
packages:
- '.'

resolver: lts-20.26
compiler: ghc-9.2.8
compiler-check: match-exact
packages:
- '.'

resolver: lts-19.33
compiler: ghc-9.0.2
compiler-check: match-exact
packages:
- '.'

resolver: lts-16.31
compiler: ghc-8.8.4
compiler-check: match-exact
packages:
- '.'

resolver: lts-16.5
compiler: ghc-8.8.3
compiler-check: match-exact
packages:
- '.'

resolver: lts-15.3
compiler: ghc-8.8.2
compiler-check: match-exact
packages:
- '.'

resolver: lts-14.27
compiler: ghc-8.6.5
compiler-check: match-exact
packages:
- '.'

resolver: lts-12.26
compiler: ghc-8.4.4
compiler-check: match-exact
packages:
- '.'

resolver: lts-11.22
compiler: ghc-8.2.2
compiler-check: match-exact
packages:
- '.'

resolver: lts-18.23
compiler: ghc-8.10.7
compiler-check: match-exact
# extra-deps:
#   - filemanip-0.3.6.3
#   - unix-compat-0.5.2
packages:
- '.'

resolver: lts-18.0
compiler: ghc-8.10.5
compiler-check: match-exact
# extra-deps:
#   - filemanip-0.3.6.3
#   - unix-compat-0.5.2
packages:
- '.'

resolver: lts-9.21
compiler: ghc-8.0.2
compiler-check: match-exact
packages:
- '.'

------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use the Data.Tree.Rose.Show module
-- directly
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --sized-types #-}
module Text.Tree.Linear where
open import Data.Tree.Rose.Show public using (display)
{-# WARNING_ON_IMPORT
"Text.Tree.Linear was deprecated in v1.6. Use Data.Tree.Rose.Show instead."
#-}

------------------------------------------------------------------------
-- The Agda standard library
--
-- Fancy display functions for Vec-based tables
------------------------------------------------------------------------
{-# OPTIONS --safe --cubical-compatible #-}
module Text.Tabular.Vec where
open import Data.List.Base using (List)
open import Data.Product.Base as Prod using (uncurry)
open import Data.String using (String; rectangle; fromAlignment)
open import Data.Vec.Base
open import Function.Base
open import Text.Tabular.Base
display : ∀ {m n} → TabularConfig → Vec Alignment n → Vec (Vec String n) m →
          List String
display c a = unsafeDisplay c
            ∘ toList
            ∘ map toList
            ∘ transpose
            ∘ map (uncurry rectangle ∘ unzip)
            ∘ transpose
            ∘ map (zip (map fromAlignment a))

------------------------------------------------------------------------
-- The Agda standard library
--
-- Fancy display functions for List-based tables
------------------------------------------------------------------------
{-# OPTIONS --safe --cubical-compatible #-}
module Text.Tabular.List where
open import Data.String.Base using (String)
open import Data.List.Base
import Data.Nat.Properties as ℕ
open import Data.Product.Base using (-,_; proj₂)
open import Data.Vec.Base as Vec using (Vec)
open import Data.Vec.Bounded.Base as Vec≤ using (Vec≤)
open import Function.Base
open import Text.Tabular.Base
import Text.Tabular.Vec as Show
display : TabularConfig → List Alignment → List (List String) → List String
display c a rows = Show.display c alignment rectangle
  where
  alignment : Vec Alignment _
  alignment = Vec≤.padRight Left
            $ Vec≤.≤-cast (ℕ.m⊓n≤m _ _)
            $ Vec≤.take _ (Vec≤.fromList a)
  rectangle : Vec (Vec String _) _
  rectangle = Vec.fromList
            $ map (Vec≤.padRight "")
            $ proj₂
            $ Vec≤.rectangle
            $ map (λ row → -, Vec≤.fromList row) rows

------------------------------------------------------------------------
-- The Agda standard library
--
-- Fancy display functions for List-based tables
--
-- The functions in this module assume some (unenforced) invariants.
-- If you cannot guarantee that your data respects these invariants,
-- you should instead use Text.Tabular.List.
------------------------------------------------------------------------
{-# OPTIONS --safe --cubical-compatible #-}
module Text.Tabular.Base where
open import Data.Bool.Base using (if_then_else_)
open import Data.Char.Base using (Char)
open import Data.List.Base as List
  using (List; []; _∷_; _?∷_; _++_; _∷ʳ?_; null; map; intersperse)
open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe)
open import Data.Nat.Base
open import Data.String.Base as String
  using (String; fromChar; unlines; replicate; length)
open import Function.Base
open import Agda.Builtin.Equality
open String
  using ( Alignment
        ; Left
        ; Center
        ; Right
        ) public
record TabularLine : Set where
  field
    left  : Maybe String
    cont  : Maybe Char
    sep   : String
    right : Maybe String
open TabularLine
record TabularConfig : Set where
  field
    top : Maybe TabularLine
    sep : Maybe TabularLine
    row : TabularLine
    bot : Maybe TabularLine
open TabularConfig
unicode : TabularConfig
unicode .top = just λ where
  .left  → just "┌"
  .cont  → just '─'
  .sep   → "┬"
  .right → just "┐"
unicode .sep = just λ where
  .left  → just "├"
  .cont  → just '─'
  .sep   → "┼"
  .right → just "┤"
unicode .row = λ where
  .left  → just "│"
  .cont  → nothing
  .sep   → "│"
  .right → just "│"
unicode .bot = just λ where
  .left  → just "└"
  .cont  → just '─'
  .sep   → "┴"
  .right → just "┘"
ascii : TabularConfig
ascii .top = just λ where
  .left  → just "+"
  .cont  → just '-'
  .sep   → "-"
  .right → just "+"
ascii .sep = just λ where
  .left  → just "|"
  .cont  → just '-'
  .sep   → "+"
  .right → just "|"
ascii .row = λ where
  .left  → just "|"
  .cont  → nothing
  .sep   → "|"
  .right → just "|"
ascii .bot = just λ where
  .left  → just "+"
  .cont  → just '-'
  .sep   → "-"
  .right → just "+"
compact : TabularConfig → TabularConfig
compact c = record c { sep = nothing }
private
  dropBorder : TabularLine → TabularLine
  dropBorder l = record l { left = nothing; right = nothing }
noBorder : TabularConfig → TabularConfig
noBorder c .top = nothing
noBorder c .sep = Maybe.map dropBorder (c .sep)
noBorder c .row = dropBorder (c .row)
noBorder c .bot = nothing
private
  space : TabularLine → TabularLine
  space l = let pad = maybe fromChar " " (l .cont) in λ where
    .left  → Maybe.map (String._++ pad) (l .left)
    .cont  → l .cont
    .sep   → pad String.++ l .sep String.++ pad
    .right → Maybe.map (pad String.++_) (l .right)
addSpace : TabularConfig → TabularConfig
addSpace c .top = Maybe.map space (c .top)
addSpace c .sep = Maybe.map space (c .sep)
addSpace c .row = space (c .row)
addSpace c .bot = Maybe.map space (c .bot)
whitespace : TabularConfig
whitespace .top = nothing
whitespace .sep = nothing
whitespace .row = λ where
  .left  → nothing
  .cont  → nothing
  .sep   → " "
  .right → nothing
whitespace .bot = nothing
-- /!\ Invariants:
-- * the table is presented as a list of rows
-- * header has the same length as each one of the rows
--   i.e. we have a rectangular table
-- * all of the strings in a given column have the same length
unsafeDisplay : TabularConfig → List (List String) → List String
unsafeDisplay _ []              = []
unsafeDisplay c (header ∷ rows) =
  map String.concat $ th ++ (trs ∷ʳ? lbot)
  where
  cellsOf : Maybe Char → List String → List String
  cellsOf nothing  = id
  cellsOf (just c) = map (λ cell → replicate (length cell) c)
  lineOf : TabularLine → List String → List String
  lineOf l xs = l .left
            ?∷  intersperse (l .sep) (cellsOf (l .cont) xs)
            ∷ʳ? l .right
  mlineOf : Maybe TabularLine → List String → Maybe (List String)
  mlineOf l xs = Maybe.map (λ l → lineOf l xs) l
  ltop : Maybe (List String)
  lsep : Maybe (List String)
  tr   : List String → List String
  lbot : Maybe (List String)
  ltop = mlineOf (c. top) header
  lsep = mlineOf (c. sep) header
  tr   = lineOf (c. row)
  lbot = mlineOf (c. bot) header
  th  = ltop ?∷ tr header ∷ []
  trs = if null rows then id else (maybe _∷_ id lsep)
      $ maybe intersperse id lsep
      $ map tr rows

------------------------------------------------------------------------
-- The Agda standard library
--
-- Regular expressions
--
-- The content of this module (and others in the Regex subdirectory) is
-- based on Alexandre Agular and Bassel Mannaa's 2009 technical report:
-- Regular Expressions in Agda
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (DecPoset)
module Text.Regex {a e r} (decPoset : DecPoset a e r) where
private
  preorder = DecPoset.preorder decPoset
import Text.Regex.Base                  preorder as Regex
import Text.Regex.SmartConstructors     preorder as Smart
import Text.Regex.Derivative.Brzozowski decPoset as Eat
import Text.Regex.Search                decPoset as Search
------------------------------------------------------------------------
-- Re-exporting basic definition and semantics
open Regex public
  using ( Range; module Range
        ; [_]; _─_
        ; Regex; module Regex; Exp; module Exp
        ; ε; [^_]; ∅; ·; singleton
        ; _∈ᴿ_; _∉ᴿ_
        ; _∈_; _∉_; sum; prod; star
        )
------------------------------------------------------------------------
-- Re-exporting smart constructors
open Smart public
  using (_∣_; _∙_; _⋆; _+; _⁇)
------------------------------------------------------------------------
-- Re-exporting semantics decidability
open Eat public
  using (_∈?_; _∉?_)
------------------------------------------------------------------------
-- Re-exporting search algorithms
open Search public
  using (Span; toInfix; Match; mkMatch; search)

------------------------------------------------------------------------
-- The Agda standard library
--
-- Regular expressions acting on strings
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Text.Regex.String where
import Data.Char.Properties as Char
------------------------------------------------------------------------
-- Re-exporting definitions
open import Text.Regex Char.≤-decPoset public

------------------------------------------------------------------------
-- The Agda standard library
--
-- Regular expressions acting on strings, using unsafe features
------------------------------------------------------------------------
{-# OPTIONS --with-K #-}
module Text.Regex.String.Unsafe where
open import Data.String.Base using (String; toList; fromList)
import Data.String.Unsafe as Stringₚ
open import Function.Base using (_on_; id)
open import Level using (0ℓ)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; sym; subst)
open import Relation.Nullary.Decidable using (map′)
------------------------------------------------------------------------
-- Re-exporting safe definitions
open import Text.Regex.String as Regex public
  hiding (_∈_; _∉_; _∈?_; _∉?_; Span; Match; search)
------------------------------------------------------------------------
-- Specialised definitions
infix 4 _∈_ _∉_ _∈?_ _∉?_
_∈_ : String → Exp → Set
str ∈ e = toList str Regex.∈ e
_∉_ : String → Exp → Set
str ∉ e = toList str Regex.∉ e
_∈?_ : Decidable _∈_
str ∈? e = toList str Regex.∈? e
_∉?_ : Decidable _∉_
str ∉? e = toList str Regex.∉? e
Span : Regex → Rel String 0ℓ
Span e = Regex.Span e _≡_ on toList
-- A match is a string, a proof it matches the regular expression,
-- and a proof it appears as the right sort of substring.
record Match (str : String) (e : Regex) : Set where
  constructor mkMatch
  field
    string  : String
    match   : string ∈ Regex.expression e
    related : Span e string str
open Match public
search : Decidable Match
search str e = map′ from to (Regex.search input e) where
  input = toList str
  exp = Regex.expression e
  from : Regex.Match (Regex.Span e _≡_) input exp → Match str e
  from (Regex.mkMatch list match related) =
    let eq = sym (Stringₚ.toList∘fromList list) in
    mkMatch (fromList list)
            (subst (Regex._∈ exp) eq match)
            (subst (λ str → Regex.Span e _≡_ str input) eq related)
  to : Match str e → Regex.Match (Regex.Span e _≡_) input exp
  to (mkMatch string match related) =
    Regex.mkMatch (toList string) match related

------------------------------------------------------------------------
-- The Agda standard library
--
-- Regular expressions: smart constructors
-- Computing the Brzozowski derivative of a regular expression may lead
-- to a blow-up in the size of the expression. To keep it tractable it
-- is crucial to use smart constructors.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (Preorder)
module Text.Regex.SmartConstructors {a e r} (P : Preorder a e r) where
open import Data.List.Base using ([])
open import Data.List.Relation.Ternary.Appending.Propositional
open import Data.Sum.Base using (inj₁; inj₂; fromInj₁; fromInj₂)
open import Relation.Nullary.Decidable using (yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary.PropositionalEquality.Core using (refl)
open import Text.Regex.Base P as R hiding (_∣_; _∙_; _⋆)
open import Text.Regex.Properties.Core P
------------------------------------------------------------------------
-- Sum
infixr 5 _∣_
_∣_ : (e f : Exp) → Exp
e ∣ f with is-∅ e | is-∅ f
... | yes _ | _ = f
... | _ | yes _ = e
... | _ | _     = e R.∣ f
∣-sound : ∀ {w} e f → w ∈ (e ∣ f) → w ∈ (e R.∣ f)
∣-sound e f p with is-∅ e | is-∅ f
... | yes _ | _     = sum (inj₂ p)
... | no _  | yes _ = sum (inj₁ p)
... | no _  | no _  = p
∣-complete : ∀ {w} e f → w ∈ (e R.∣ f) → w ∈ (e ∣ f)
∣-complete e f pr@(sum p) with is-∅ e | is-∅ f
... | yes refl | _        = fromInj₂ (λ p → contradiction p ∉∅) p
... | no _     | yes refl = fromInj₁ (λ p → contradiction p ∉∅) p
... | no _     | no _     = pr
------------------------------------------------------------------------
-- Product
infixr 6 _∙_
_∙_ : (e f : Exp) → Exp
e ∙ f with is-∅ e | is-ε e | is-∅ f | is-ε f
... | yes _ | _ | _ | _ = R.∅
... | _ | yes _ | _ | _ = f
... | _ | _ | yes _ | _ = R.∅
... | _ | _ | _ | yes _ = e
... | _ | _ | _ | _ = e R.∙ f
∙-sound : ∀ {w} e f → w ∈ (e ∙ f) → w ∈ (e R.∙ f)
∙-sound e f p with is-∅ e | is-ε e | is-∅ f | is-ε f
... | yes refl | _        | _        | _        = contradiction p ∉∅
... | no _     | yes refl | _        | _        = prod ([] ++ _) ε p
... | no _     | no _     | yes refl | _        = contradiction p ∉∅
... | no _     | no _     | no _     | yes refl = prod (_ ++[]) p ε
... | no _     | no _     | no _     | no _     = p
∙-complete : ∀ {w} e f → w ∈ (e R.∙ f) → w ∈ (e ∙ f)
∙-complete e f pr@(prod eq p q) with is-∅ e | is-ε e | is-∅ f | is-ε f
... | yes refl | _        | _        | _        = contradiction p ∉∅
... | no _     | yes refl | _        | _        = ∈ε∙e-inv pr
... | no _     | no _     | yes refl | _        = contradiction q ∉∅
... | no _     | no _     | no _     | yes refl = ∈e∙ε-inv pr
... | no _     | no _     | no _     | no _     = pr
------------------------------------------------------------------------
-- Kleene star
infix  7 _⋆
_⋆ : Exp → Exp
e ⋆ with is-∅ e | is-ε e
... | yes _ | _ = R.ε
... | _ | yes _ = R.ε
... | _ | _ = e R.⋆
⋆-sound : ∀ {w} e → w ∈ (e ⋆) → w ∈ (e R.⋆)
⋆-sound e p with is-∅ e | is-ε e
... | yes refl | _        = star (sum (inj₁ p))
... | no _     | yes refl = star (sum (inj₁ p))
... | no _     | no _     = p
⋆-complete : ∀ {w} e → w ∈ (e R.⋆) → w ∈ (e ⋆)
⋆-complete e pr with is-∅ e | is-ε e
... | yes refl | no _     = ∈∅⋆-inv pr
... | no _     | yes refl = ∈ε⋆-inv pr
... | no _     | no _     = pr
------------------------------------------------------------------------
-- Derived notions: at least one and maybe one
infixl 7 _+ _⁇
_+ : Exp → Exp
e + = e ∙ e ⋆
_⁇ : Exp → Exp
∅ ⁇ = ε
e ⁇ = ε ∣ e

------------------------------------------------------------------------
-- The Agda standard library
--
-- Regular expressions: search algorithms
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (DecPoset)
module Text.Regex.Search {a e r} (P? : DecPoset a e r) where
open import Level using (_⊔_)
open import Data.Bool.Base using (if_then_else_; true; false)
open import Data.List.Base using (List; []; _∷_)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Function.Base using (id; _∘′_; _∘_)
open import Data.List.Relation.Binary.Prefix.Heterogeneous
  using (Prefix; []; _∷_) hiding (module Prefix)
open import Data.List.Relation.Binary.Infix.Heterogeneous
  using (Infix; here; there) hiding (module Infix)
import Data.List.Relation.Binary.Infix.Heterogeneous.Properties as Infixₚ
open import Data.List.Relation.Binary.Pointwise
  as Pointwise using (Pointwise; []; _∷_)
open import Data.List.Relation.Binary.Suffix.Heterogeneous
  using (Suffix; here; there) hiding (module Suffix)
open import Relation.Nullary using (Dec; ¬_; yes; no)
open import Relation.Nullary.Decidable using (map′)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary.Core using (Rel; _⇒_)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.PropositionalEquality.Core
open DecPoset P? using (preorder) renaming (Carrier to A)
open import Text.Regex.Base preorder
open import Text.Regex.Properties P?
open import Text.Regex.Derivative.Brzozowski P?
------------------------------------------------------------------------
-- Type corresponding to a match
-- Users have control over whether the match should start at the
-- beginning or stop at the end. So we have a precise type of spans
-- ensuring their demands are respected
Span : ∀ {r} → Regex → Rel A r → Rel (List A) (a ⊔ r)
Span regex =
  if Regex.fromStart regex
  then if Regex.tillEnd regex
       then Pointwise
       else Prefix
  else if Regex.tillEnd regex
       then Suffix
       else Infix
-- All matches are selecting an infix sublist
toInfix : ∀ {r} {R : Rel A r} e → Span e R ⇒ Infix R
toInfix e with Regex.fromStart e | Regex.tillEnd e
... | true  | true  = Infixₚ.fromPointwise
... | true  | false = here
... | false | true  = Infixₚ.fromSuffix
... | false | false = id
-- A match is a list, a proof it matches the regular expression,
-- and a proof it is the right sort of sublist.
record Match {s} (R : Rel (List A) s) (xs : List A) (exp : Exp)
       : Set (a ⊔ e ⊔ r ⊔ s) where
  constructor mkMatch
  field
    list    : List A
    match   : list ∈ exp
    related : R list xs
open Match public
map : ∀ {r s} {R : Rel (List A) r} {S : Rel (List A) s} {xs ys e} →
      (∀ {a} → R a xs → S a ys) → Match R xs e → Match S ys e
map f (mkMatch ys ys∈e pys) = mkMatch ys ys∈e (f pys)
------------------------------------------------------------------------
-- Search algorithms
module Prefix where
  []ᴹ : ∀ {xs e} → [] ∈ e → Match (Prefix _≡_) xs e
  []ᴹ p = mkMatch [] p []
  []⁻¹ᴹ : ∀ {e} → Match (Prefix _≡_) [] e → [] ∈ e
  []⁻¹ᴹ (mkMatch .[] p []) = p
  infixr 5 _∷ᴹ_ _∷⁻¹ᴹ_
  _∷ᴹ_ : ∀ {xs e} x → Match (Prefix _≡_) xs (eat x e) → Match (Prefix _≡_) (x ∷ xs) e
  x ∷ᴹ (mkMatch ys ys∈e\x ys≤xs) = mkMatch (x ∷ ys) (eat-sound x _ ys∈e\x) (refl ∷ ys≤xs)
  _∷⁻¹ᴹ_ : ∀ {xs x e} → [] ∉ e →
           Match (Prefix _≡_) (x ∷ xs) e → Match (Prefix _≡_) xs (eat x e)
  []∉e ∷⁻¹ᴹ (mkMatch .[]       []∈e [])             = contradiction []∈e []∉e
  []∉e ∷⁻¹ᴹ (mkMatch (._ ∷ ys) ys∈e (refl ∷ ys≤xs)) = mkMatch ys (eat-complete _ _ ys∈e) ys≤xs
  shortest : Decidable (Match (Prefix _≡_))
  shortest xs ∅ = no (∉∅ ∘ match)
  shortest xs e with []∈? e
  ... | yes []∈e = yes ([]ᴹ []∈e)
  shortest []       e | no []∉e = no ([]∉e ∘′ []⁻¹ᴹ)
  shortest (x ∷ xs) e | no []∉e with shortest xs (eat x e)
  ... | yes p = yes (x ∷ᴹ p)
  ... | no ¬p = no (¬p ∘ ([]∉e ∷⁻¹ᴹ_))
  longest : Decidable (Match (Prefix _≡_))
  longest []       e = map′ []ᴹ []⁻¹ᴹ ([]∈? e)
  longest xs       ∅ = no (∉∅ ∘ match)
  longest (x ∷ xs) e with longest xs (eat x e)
  ... | yes p = yes (x ∷ᴹ p)
  ... | no ¬p with []∈? e
  ... | yes []∈e = yes ([]ᴹ []∈e)
  ... | no []∉e  = no (¬p ∘ ([]∉e ∷⁻¹ᴹ_))
module Infix where
  []⁻¹ᴹ : ∀ {e acc} → Match (Infix _≡_) [] e ⊎ Match (Prefix _≡_) [] acc → [] ∈ e ⊎ [] ∈ acc
  []⁻¹ᴹ (inj₁ (mkMatch .[] []∈e (here []))) = inj₁ []∈e
  []⁻¹ᴹ (inj₂ (mkMatch .[] []∈acc []))      = inj₂ []∈acc
  step : ∀ {e acc} x {xs} → Match (Infix _≡_) xs e ⊎ Match (Prefix _≡_) xs (eat x (acc ∣ e)) →
                            Match (Infix _≡_) (x ∷ xs) e ⊎ Match (Prefix _≡_) (x ∷ xs) acc
  step x (inj₁ (mkMatch ys ys∈e p)) = inj₁ (mkMatch ys ys∈e (there p))
  step {e} {acc} x (inj₂ (mkMatch ys ys∈e p)) with eat-sound x (acc ∣ e) ys∈e
  ... | sum (inj₂ xys∈e) = inj₁ (mkMatch (x ∷ ys) xys∈e (here (refl ∷ p)))
  ... | sum (inj₁ xys∈e) = inj₂ (mkMatch (x ∷ ys) xys∈e (refl ∷ p))
  step⁻¹ : ∀ {e acc} x {xs} →
           [] ∉ e → [] ∉ acc →
           Match (Infix _≡_) (x ∷ xs) e ⊎ Match (Prefix _≡_) (x ∷ xs) acc →
           Match (Infix _≡_) xs e ⊎ Match (Prefix _≡_) xs (eat x (acc ∣ e))
  -- can't possibly be the empty match
  step⁻¹ x []∉e []∉acc (inj₁ (mkMatch .[] ys∈e (here []))) = contradiction ys∈e []∉e
  step⁻¹ x []∉e []∉acc (inj₂ (mkMatch .[] ys∈e []))        = contradiction ys∈e []∉acc
  -- if it starts 'there', it's an infix solution
  step⁻¹ x []∉e []∉acc (inj₁ (mkMatch ys ys∈e (there p))) = inj₁ (mkMatch ys ys∈e p)
  -- if it starts 'here' we're in prefix territory
  step⁻¹ {e} {acc} x []∉e []∉acc (inj₁ (mkMatch (.x ∷ ys) ys∈e (here (refl ∷ p))))
    = inj₂ (mkMatch ys (eat-complete x (acc ∣ e) (sum (inj₂ ys∈e))) p)
  step⁻¹ {e} {acc} x []∉e []∉acc (inj₂ (mkMatch (.x ∷ ys) ys∈e (refl ∷ p)))
    = inj₂ (mkMatch ys (eat-complete x (acc ∣ e) (sum (inj₁ ys∈e))) p)
  -- search non-deterministically: at each step, the `acc` regex is
  -- changed to accomodate the fact the match may be starting just now
  searchND : ∀ xs e acc → [] ∉ e → Dec (Match (Infix _≡_) xs e ⊎ Match (Prefix _≡_) xs acc)
  searchND xs e acc []∉e with []∈? acc
  ... | yes []∈acc with Prefix.longest xs acc -- get the best match possible
  ...               | yes longer = yes (inj₂ longer)
  ...               | no noMatch = contradiction (mkMatch [] []∈acc []) noMatch
  searchND [] e acc []∉e | no []∉acc = no ([ []∉e , []∉acc ]′ ∘′ []⁻¹ᴹ)
  searchND (x ∷ xs) e acc []∉e | no []∉acc
    = map′ (step x) (step⁻¹ x []∉e []∉acc) (searchND xs e (eat x (acc ∣ e)) []∉e)
  search : Decidable (Match (Infix _≡_))
  search xs e with []∈? e
  ... | yes []∈e = yes (mkMatch [] []∈e (here []))
  ... | no []∉e with searchND xs e ∅ []∉e
  ... | no ¬p        = no (¬p ∘′ inj₁)
  ... | yes (inj₁ p) = yes p
  ... | yes (inj₂ p) = contradiction (match p) ∉∅
module Whole where
  whole : ∀ xs e → xs ∈ e → Match (Pointwise _≡_) xs e
  whole xs e p = mkMatch xs p (Pointwise.refl refl)
  whole⁻¹ : ∀ xs e → Match (Pointwise _≡_) xs e → xs ∈ e
  whole⁻¹ xs e (mkMatch ys ys∈e p) with Pointwise.Pointwise-≡⇒≡ p
  whole⁻¹ xs e (mkMatch .xs xs∈e p) | refl = xs∈e
  search : Decidable (Match (Pointwise _≡_))
  search xs e = map′ (whole xs e) (whole⁻¹ xs e) (xs ∈? e)
module Suffix where
  []⁻¹ᴹ : ∀ {e acc} → Match (Suffix _≡_) [] e ⊎ Match (Pointwise _≡_) [] acc → [] ∈ e ⊎ [] ∈ acc
  []⁻¹ᴹ (inj₁ (mkMatch .[] ys∈e (here []))) = inj₁ ys∈e
  []⁻¹ᴹ (inj₂ (mkMatch .[] ys∈acc []))      = inj₂ ys∈acc
  step : ∀ {e acc} x {xs} →
         Match (Suffix _≡_) xs e ⊎ Match (Pointwise _≡_) xs (eat x (e ∣ acc)) →
         Match (Suffix _≡_) (x ∷ xs) e ⊎ Match (Pointwise _≡_) (x ∷ xs) acc
  step x (inj₁ (mkMatch ys ys∈e p)) = inj₁ (mkMatch ys ys∈e (there p))
  step {e} {acc} x (inj₂ (mkMatch ys ys∈e p)) with eat-sound x (e ∣ acc) ys∈e
  ... | sum (inj₁ xys∈e)   = inj₁ (mkMatch (x ∷ ys) xys∈e (here (refl ∷ p)))
  ... | sum (inj₂ xys∈acc) = inj₂ (mkMatch (x ∷ ys) xys∈acc (refl ∷ p))
  step⁻¹ : ∀ {e acc} x {xs} →
           Match (Suffix _≡_) (x ∷ xs) e ⊎ Match (Pointwise _≡_) (x ∷ xs) acc →
           Match (Suffix _≡_) xs e ⊎ Match (Pointwise _≡_) xs (eat x (e ∣ acc))
  -- match starts later
  step⁻¹ x (inj₁ (mkMatch ys ys∈e (there p))) = inj₁ (mkMatch ys ys∈e p)
  -- match starts here!
  step⁻¹ {e} {acc} x (inj₁ (mkMatch (.x ∷ ys) ys∈e (here (refl ∷ p))))
    = inj₂ (mkMatch ys (eat-complete x (e ∣ acc) (sum (inj₁ ys∈e))) p)
  step⁻¹ {e} {acc} x (inj₂ (mkMatch (.x ∷ ys) ys∈e (refl ∷ p)))
    = inj₂ (mkMatch ys (eat-complete x (e ∣ acc) (sum (inj₂ ys∈e))) p)
  searchND : ∀ xs e acc → Dec (Match (Suffix _≡_) xs e ⊎ Match (Pointwise _≡_) xs acc)
  searchND []       e acc with []∈? e | []∈? acc
  ... | yes []∈e | _          = yes (inj₁ (mkMatch [] []∈e (here [])))
  ... | _        | yes []∈acc = yes (inj₂ (mkMatch [] []∈acc []))
  ... | no []∉e  | no []∉acc  = no ([ []∉e , []∉acc ]′ ∘′ []⁻¹ᴹ)
  searchND (x ∷ xs) e acc
    = map′ (step x) (step⁻¹ x) (searchND xs e (eat x (e ∣ acc)))
  search : Decidable (Match (Suffix _≡_))
  search xs e with searchND xs e ∅
  ... | no ¬p        = no (¬p ∘′ inj₁)
  ... | yes (inj₁ p) = yes p
  ... | yes (inj₂ p) = contradiction (match p) ∉∅
------------------------------------------------------------------------
-- Search for the user-specified span
search : ∀ xs e → Dec (Match (Span e _≡_) xs (Regex.expression e))
search xs e with Regex.fromStart e | Regex.tillEnd e
... | true  | true  = Whole.search    xs (Regex.expression e)
... | true  | false = Prefix.shortest xs (Regex.expression e)
... | false | true  = Suffix.search   xs (Regex.expression e)
... | false | false = Infix.search    xs (Regex.expression e)

------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of regular expressions and their semantics
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (DecPoset)
module Text.Regex.Properties {a e r} (P? : DecPoset a e r) where
open import Data.List.Base using (List; []; _∷_)
open import Data.List.Relation.Unary.All using (all?)
open import Data.List.Relation.Unary.Any using (any?)
open import Data.Product.Base using (_×_; _,_; uncurry)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Function.Base using (_$_)
open import Relation.Nullary.Decidable
  using (Dec; yes; no; map′; ¬?; _×-dec_; _⊎-dec_)
open import Relation.Nullary.Negation
  using (¬_; contradiction)
import Relation.Unary  as U
open import Relation.Binary.Definitions using (Decidable)
open DecPoset P? renaming (Carrier to A)
open import Text.Regex.Base preorder
open import Data.List.Relation.Binary.Pointwise.Base using ([])
open import Data.List.Relation.Ternary.Appending.Propositional {A = A}
open import Data.List.Relation.Ternary.Appending.Propositional.Properties {A = A}
------------------------------------------------------------------------
-- Publicly re-export core properties
open import Text.Regex.Properties.Core preorder public
------------------------------------------------------------------------
-- Decidability results
[]∈?_ : U.Decidable ([] ∈_)
[]∈? ε       = yes ε
[]∈? [ rs ]  = no (λ ())
[]∈? [^ rs ] = no (λ ())
[]∈? (e ∣ f) = map′ sum (λ where (sum pr) → pr)
             $ ([]∈? e) ⊎-dec ([]∈? f)
[]∈? (e ∙ f) = map′ (uncurry (prod ([]++ []))) []∈e∙f-inv
             $ ([]∈? e) ×-dec ([]∈? f)
[]∈? (e ⋆)   = yes (star (sum (inj₁ ε)))
infix 4 _∈ᴿ?_ _∉ᴿ?_ _∈?ε _∈?[_] _∈?[^_]
_∈ᴿ?_ : Decidable _∈ᴿ_
c ∈ᴿ? [ a ]     = map′ [_] (λ where [ eq ] → eq) (c ≟ a)
c ∈ᴿ? (lb ─ ub) = map′ (uncurry _─_) (λ where (ge ─ le) → ge , le)
                $ (lb ≤? c) ×-dec (c ≤? ub)
_∉ᴿ?_ : Decidable _∉ᴿ_
a ∉ᴿ? r = ¬? (a ∈ᴿ? r)
_∈?ε : U.Decidable (_∈ ε)
[]      ∈?ε = yes ε
(a ∷ _) ∈?ε = no (λ ())
_∈?[_] : ∀ w rs → Dec (w ∈ [ rs ])
[]          ∈?[ rs ] = no (λ ())
(a ∷ b ∷ _) ∈?[ rs ] = no (λ ())
(a ∷ [])    ∈?[ rs ] = map′ [_] (λ where [ p ] → p)
                      $ any? (a ∈ᴿ?_) rs
_∈?[^_] : ∀ w rs → Dec (w ∈ [^ rs ])
[]          ∈?[^ rs ] = no (λ ())
(a ∷ [])    ∈?[^ rs ] = map′ [^_] (λ where [^ p ] → p) $ all? (a ∉ᴿ?_) rs
(a ∷ b ∷ _) ∈?[^ rs ] = no (λ ())

------------------------------------------------------------------------
-- The Agda standard library
--
-- Regular expressions: core properties (only require a Preorder)
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (Preorder)
module Text.Regex.Properties.Core {a e r} (P : Preorder a e r) where
open import Level using (_⊔_)
open import Data.Bool.Base using (Bool)
open import Data.List.Base as List using (List; []; _∷_; _++_)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.Product.Base using (_×_; _,_)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Unary using (Pred)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
open Preorder P using (_≈_) renaming (Carrier to A; _∼_ to _≤_)
open import Text.Regex.Base P
open import Data.List.Relation.Ternary.Appending.Propositional.Properties {A = A}
  using (++[]⁻¹; []++⁻¹; conicalˡ; conicalʳ)
------------------------------------------------------------------------
-- Views
is-∅ : ∀ (e : Exp) → Dec (e ≡ ∅)
is-∅ ε          = no (λ ())
is-∅ [ [] ]     = yes refl
is-∅ [ r ∷ rs ] = no (λ ())
is-∅ [^ rs ]    = no (λ ())
is-∅ (e ∣ f)    = no (λ ())
is-∅ (e ∙ f)    = no (λ ())
is-∅ (e ⋆)      = no (λ ())
is-ε : ∀ (e : Exp) → Dec (e ≡ ε)
is-ε ε       = yes refl
is-ε [ rs ]  = no (λ ())
is-ε [^ rs ] = no (λ ())
is-ε (e ∣ f) = no (λ ())
is-ε (e ∙ f) = no (λ ())
is-ε (e ⋆)   = no (λ ())
------------------------------------------------------------------------
-- Inversion lemmas
∉∅ : ∀ {xs} → xs ∉ ∅
∉∅ [ () ]
∈ε⋆-inv : ∀ {w} → w ∈ (ε ⋆) → w ∈ ε
∈ε⋆-inv (star (sum (inj₁ ε))) = ε
∈ε⋆-inv (star (sum (inj₂ (prod eq ε p)))) rewrite []++⁻¹ eq = ∈ε⋆-inv p
∈∅⋆-inv : ∀ {w} → w ∈ (∅ ⋆) → w ∈ ε
∈∅⋆-inv (star (sum (inj₁ ε))) = ε
∈∅⋆-inv (star (sum (inj₂ (prod eq p q)))) = contradiction p ∉∅
∈ε∙e-inv : ∀ {w e} → w ∈ (ε ∙ e) → w ∈ e
∈ε∙e-inv (prod eq ε p) rewrite []++⁻¹ eq = p
∈e∙ε-inv : ∀ {w e} → w ∈ (e ∙ ε) → w ∈ e
∈e∙ε-inv (prod eq p ε) rewrite ++[]⁻¹ eq = p
[]∈e∙f-inv : ∀ {e f} → [] ∈ (e ∙ f) → [] ∈ e × [] ∈ f
[]∈e∙f-inv (prod eq p q) rewrite conicalˡ eq | conicalʳ eq = p , q

------------------------------------------------------------------------
-- The Agda standard library
--
-- Regular expressions: Brzozowski derivative
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (DecPoset)
module Text.Regex.Derivative.Brzozowski {a e r} (P? : DecPoset a e r) where
open import Data.List.Base using (List; []; _∷_)
open import Data.List.Relation.Binary.Equality.Propositional
open import Data.Sum.Base as Sum using (inj₁; inj₂)
open import Function.Base using (_$_; _∘′_; case_of_)
open import Relation.Nullary.Decidable using (Dec; yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Nullary.Decidable using (map′; ¬?)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
open DecPoset P? using (preorder) renaming (Carrier to A)
open import Text.Regex.Base preorder as R hiding (_∣_; _∙_; _⋆)
open import Text.Regex.Properties P?
open import Text.Regex.SmartConstructors preorder
open import Data.List.Relation.Ternary.Appending.Propositional {A = A}
open import Data.List.Relation.Ternary.Appending.Propositional.Properties {A = A}
------------------------------------------------------------------------
-- Action of characters on regular expressions
private
  decToExp : ∀ {p} {P : Set p} → Dec P → Exp
  decToExp (yes _) = ε
  decToExp (no _)  = ∅
eat : A → Exp → Exp
eat a ε         = ∅
eat a [ rs ]    = decToExp ((a ∷ []) ∈?[ rs ])
eat a [^ rs ]   = decToExp ((a ∷ []) ∈?[^ rs ])
eat a (e R.∣ f) = eat a e ∣ eat a f
eat a (e R.∙ f) = case []∈? e of λ where
  (yes _) → (eat a e ∙ f) ∣ (eat a f)
  (no ¬p) → eat a e ∙ f
eat a (e R.⋆)   = eat a e ∙ (e ⋆)
------------------------------------------------------------------------
-- This action is sound and complete with respect to matching
eat-sound : ∀ x {xs} e → xs ∈ eat x e → (x ∷ xs) ∈ e
eat-sound x ε         pr = contradiction pr ∉∅
eat-sound x [ rs ]    pr with (x ∷ []) ∈?[ rs ]
... | yes p = case pr of λ where ε → p
... | no _  = contradiction pr ∉∅
eat-sound x [^ rs ]   pr with (x ∷ []) ∈?[^ rs ]
... | yes p = case pr of λ where ε → p
... | no _  = contradiction pr ∉∅
eat-sound x (e R.∣ f) pr with ∣-sound (eat x e) (eat x f) pr
... | sum pr′ = sum $ Sum.map (eat-sound x e) (eat-sound x f) pr′
eat-sound x (e R.∙ f) pr with []∈? e
... | yes []∈e with ∣-sound (eat x e ∙ f) (eat x f) pr
... | sum (inj₂ pr') = prod ([] ++ _) []∈e (eat-sound x f pr')
... | sum (inj₁ pr') with ∙-sound (eat x e) f pr'
... | prod eq p q = prod (refl ∷ eq) (eat-sound x e p) q
eat-sound x (e R.∙ f) pr | no ¬p with ∙-sound (eat x e) f pr
... | prod eq p q = prod (refl ∷ eq) (eat-sound x e p) q
eat-sound x (e R.⋆) pr with ∙-sound (eat x e) (e ⋆) pr
... | prod eq p q =
  star (sum (inj₂ (prod (refl ∷ eq) (eat-sound x e p) (⋆-sound e q))))
eat-complete′ : ∀ x {xs w} e → w ≋ (x ∷ xs) → w ∈ e → xs ∈ eat x e
eat-complete  : ∀ x {xs} e → (x ∷ xs) ∈ e → xs ∈ eat x e
eat-complete x e = eat-complete′ x e ≋-refl
eat-complete′ x [ rs ] (refl ∷ []) [ p ]
  with (x ∷ []) ∈?[ rs ]
... | yes _ = ε
... | no ¬p = contradiction [ p ] ¬p
eat-complete′ x [^ rs ] (refl ∷ []) [^ p ]
  with (x ∷ []) ∈?[^ rs ]
... | yes _ = ε
... | no ¬p = contradiction [^ p ] ¬p
eat-complete′ x (e R.∣ f) eq (sum p) =
  ∣-complete (eat x e) (eat x f) $ sum $
  Sum.map (eat-complete′ x e eq) (eat-complete′ x f eq) p
eat-complete′ x (e R.∙ f) eq p with []∈? e
eat-complete′ x (e R.∙ f) (refl ∷ eq) (prod ([]++ _) p q) | no []∉e
  = contradiction p []∉e
eat-complete′ x (e R.∙ f) (refl ∷ eq) (prod (refl ∷ app) p q) | no []∉e
  = ∙-complete (eat x e) f (prod (respʳ-≋ app eq) (eat-complete x e p) q)
eat-complete′ x (e R.∙ f) eq (prod ([]++ eq′) p q) | yes []∈e
  = ∣-complete (eat x e ∙ f) (eat x f) $ sum $ inj₂
  $ eat-complete′ x f (≋-trans eq′ eq) q
eat-complete′ x (e R.∙ f) (refl ∷ eq) (prod (refl ∷ app) p q) | yes []∈e
  = ∣-complete (eat x e ∙ f) (eat x f) $ sum $ inj₁
  $ ∙-complete (eat x e) f (prod (respʳ-≋ app eq) (eat-complete x e p) q)
eat-complete′ x (e R.⋆) eq (star (sum (inj₂ (prod ([]++ app) p q))))
  = eat-complete′ x (e R.⋆) (≋-trans app eq) q
eat-complete′ x (e R.⋆) (refl ∷ eq) (star (sum (inj₂ (prod (refl ∷ app) p q))))
  = ∙-complete (eat x e) (e ⋆) $ prod (respʳ-≋ app eq) (eat-complete x e p)
  $ ⋆-complete e q
------------------------------------------------------------------------
-- Consequence: matching is decidable
infix 4 _∈?_ _∉?_
_∈?_ : Decidable _∈_
[]       ∈? e = []∈? e
(x ∷ xs) ∈? e = map′ (eat-sound x e) (eat-complete x e) (xs ∈? eat x e)
_∉?_ : Decidable _∉_
xs ∉? e = ¬? (xs ∈? e)

------------------------------------------------------------------------
-- The Agda standard library
--
-- Regular expressions: basic types and semantics
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (Preorder)
module Text.Regex.Base {a e r} (P : Preorder a e r) where
open import Level using (_⊔_)
open import Data.Bool.Base using (Bool)
open import Data.List.Base as L using (List; []; _∷_)
open import Data.List.Relation.Unary.Any using (Any)
open import Data.List.Relation.Unary.All using (All)
open import Data.Sum.Base using (_⊎_)
open import Relation.Nullary.Negation.Core using (¬_)
open Preorder P using (_≈_) renaming (Carrier to A; _∼_ to _≤_)
open import Data.List.Relation.Ternary.Appending.Propositional {A = A}
------------------------------------------------------------------------
-- Regular expressions on the alphabet A
infix 10 [_] _─_
data Range : Set a where
  [_] : (a : A)     → Range
  _─_ : (lb ub : A) → Range
infixr 5 _∣_
infixr 6 _∙_
infixl 7 _⋆
infix 10 [^_]
data Exp : Set a where
  ε    : Exp
  [_]  : (rs : List Range) → Exp
  [^_] : (rs : List Range) → Exp
  _∣_  : (e f : Exp) → Exp
  _∙_  : (e f : Exp) → Exp
  _⋆   : (e : Exp) → Exp
-- A regular expression has additional parameters:
-- * should the match begin at the very start of the input?
-- * should it span until the very end?
record Regex : Set a where
  field
    fromStart  : Bool
    tillEnd    : Bool
    expression : Exp
updateExp : (Exp → Exp) → Regex → Regex
updateExp f r = record r { expression = f (Regex.expression r) }
------------------------------------------------------------------------
-- Derived notions: nothing, anything, and singleton
pattern ∅ = [ List.[] ]
pattern · = [^ List.[] ]
pattern singleton a = [ Range.[ a ] ∷ [] ]
------------------------------------------------------------------------
-- Semantics: matching words
infix 4 _∈ᴿ_ _∉ᴿ_
data _∈ᴿ_ (c : A) : Range → Set (a ⊔ r ⊔ e) where
  [_] : ∀ {val}   → c ≈ val         → c ∈ᴿ [ val ]
  _─_ : ∀ {lb ub} → lb ≤ c → c ≤ ub → c ∈ᴿ (lb ─ ub)
_∉ᴿ_ : A → Range → Set (a ⊔ r ⊔ e)
a ∉ᴿ r = ¬ (a ∈ᴿ r)
infix 4 _∈_ _∉_
data _∈_ : List A → Exp → Set (a ⊔ r ⊔ e) where
  ε      :                                                     []      ∈ ε
  [_]    : ∀ {a rs} → Any (a ∈ᴿ_) rs →                         L.[ a ] ∈ [ rs ]
  [^_]   : ∀ {a rs} → All (a ∉ᴿ_) rs →                         L.[ a ] ∈ [^ rs ]
  sum    : ∀ {w e f} → (w ∈ e) ⊎ (w ∈ f) →                     w       ∈ (e ∣ f)
  prod   : ∀ {v w vw e f} → Appending v w vw → v ∈ e → w ∈ f → vw      ∈ (e ∙ f)
  star   : ∀ {v e} → v ∈ (ε ∣ e ∙ (e ⋆)) →                     v       ∈ (e ⋆)
_∉_ : List A → Exp → Set (a ⊔ r ⊔ e)
w ∉ e = ¬ (w ∈ e)

------------------------------------------------------------------------
-- The Agda standard library
--
-- Printf
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Text.Printf where
open import Data.String.Base using (String; fromChar; concat)
open import Function.Base using (id)
import Data.Integer.Show as ℤ
import Data.Float.Base   as Float
import Data.Nat.Show     as ℕ
open import Text.Format as Format hiding (Error)
open import Text.Printf.Generic
printfSpec : PrintfSpec formatSpec String
printfSpec .PrintfSpec.renderArg ℕArg      = ℕ.show
printfSpec .PrintfSpec.renderArg ℤArg      = ℤ.show
printfSpec .PrintfSpec.renderArg FloatArg  = Float.show
printfSpec .PrintfSpec.renderArg CharArg   = fromChar
printfSpec .PrintfSpec.renderArg StringArg = id
printfSpec .PrintfSpec.renderStr           = id
module Printf = Type formatSpec
open Printf public hiding (map)
open Render printfSpec public renaming (printf to gprintf)
printf : (fmt : String) → Printf (lexer fmt) String
printf fmt = Printf.map (lexer fmt) concat (gprintf fmt)

------------------------------------------------------------------------
-- The Agda standard library
--
-- Generic printf function.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Text.Printf.Generic where
open import Level using (Level; 0ℓ; _⊔_; Lift)
open import Data.List.Base as List using (List; []; _∷_)
open import Data.Char.Base
open import Data.Maybe.Base hiding (map)
open import Data.Nat.Base using (ℕ)
open import Data.Product.Base hiding (map)
open import Data.Product.Nary.NonDependent
open import Data.String.Base using (String)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Data.Unit.Base using (⊤)
open import Function.Nary.NonDependent
open import Function.Base
open import Text.Format.Generic
private
  variable
    ℓ : Level
    A B : Set ℓ
------------------------------------------------------------------------
-- Printf argument specifications.
-- Defines the rendering of chunks.
record PrintfSpec {ℓ} (spec : FormatSpec) (A : Set ℓ) : Set (Level.suc 0ℓ ⊔ ℓ) where
  open FormatSpec spec public
  field
    renderArg : ∀ arg → ArgType arg → A
    renderStr : String → A
module Type (spec : FormatSpec) where
  open Format spec renaming (Error to FormatError)
  record Error (e : FormatError) : Set ℓ where
  private
    Size : FormatError ⊎ Format → ℕ
    Size (inj₁ err) = 0
    Size (inj₂ fmt) = size fmt
  Printf : ∀ pr → Set ℓ → Set (ℓ ⊔ ⨆ (Size pr) 0ℓs)
  Printf (inj₁ err) _ = Error err
  Printf (inj₂ fmt) B = Arrows _ ⟦ fmt ⟧ B
  map : ∀ pr → (A → B) → Printf pr A → Printf pr B
  map (inj₁ err) f p = _
  map (inj₂ fmt) f p = mapₙ _ f p
module Render {spec : FormatSpec} (render : PrintfSpec spec A) where
  open PrintfSpec render
  open Type spec
  open Format spec renaming (Error to FormatError)
  assemble : ∀ fmt → Product⊤ _ ⟦ fmt ⟧ → List A
  assemble [] vs                    = []
  assemble (Arg a   ∷ fmt) (x , vs) = renderArg a x ∷ assemble fmt vs
  assemble (Raw str ∷ fmt) vs       = renderStr str ∷ assemble fmt vs
  private
    printf′ : ∀ pr → Printf pr (List A)
    printf′ (inj₁ err) = _
    printf′ (inj₂ fmt) = curry⊤ₙ _ (assemble fmt)
  printf : (input : String) → Printf (lexer input) (List A)
  printf input = printf′ (lexer input)

------------------------------------------------------------------------
-- The Agda standard library
--
-- Pretty Printing
-- This module is based on Jean-Philippe Bernardy's functional pearl
-- "A Pretty But Not Greedy Printer"
------------------------------------------------------------------------
{-# OPTIONS --with-K #-}
open import Data.Nat.Base using (ℕ)
module Text.Pretty (width : ℕ) where
import Level
open import Data.Char.Base using (Char)
open import Data.List.Base
  using (List; _∷_; []; [_]; uncons; _++_; map; filter)
open import Data.List.NonEmpty as List⁺ using (foldr₁)
open import Data.Maybe.Base using (maybe′)
open import Data.Product.Base using (uncurry)
open import Data.String.Base using (String; fromList; replicate)
open import Function.Base using (_∘_; _∘′_; _$_)
open import Effect.Monad using (RawMonad)
import Data.List.Effectful as List
open RawMonad (List.monad {Level.zero})
import Data.Nat.Properties as ℕ
open import Data.List.Extrema.Core ℕ.≤-totalOrder using (⊓ᴸ)
------------------------------------------------------------------------
-- Internal representation of documents and rendering function
import Text.Pretty.Core as Core
record Doc : Set where
  constructor mkDoc
  field runDoc : List Core.Block
open Doc public
render : Doc → String
render = Core.render
       ∘ maybe′ (foldr₁ (⊓ᴸ Core.Block.height) ∘′ uncurry List⁺._∷_) Core.empty
       ∘ uncons
       ∘′ runDoc
------------------------------------------------------------------------
-- Basic building blocks
fail : Doc
fail = mkDoc []
text : String → Doc
text = mkDoc ∘′ filter (Core.valid width) ∘ pure ∘ Core.text
empty : Doc
empty = text ""
char : Char → Doc
char c = text (fromList (c ∷ []))
spaces : ℕ → Doc
spaces n = text (replicate n ' ')
semi colon comma space dot : Doc
semi = char ';'; colon = char ':'
comma = char ','; space = char ' '; dot = char '.'
backslash forwardslash equal : Doc
backslash = char '\\'; forwardslash = char '/'; equal = char '='
squote dquote : Doc
squote = char '\''; dquote = char '"'
lparen rparen langle rangle : Doc
lparen = char '('; rparen = char ')'
langle = char '<'; rangle = char '>'
lbrace rbrace llbrace rrbrace : Doc
lbrace = char '{'; rbrace = char '}'
llbrace = char '⦃'; rrbrace = char '⦄'
lbracket rbracket llbracket rrbracket : Doc
lbracket = char '['; rbracket = char ']'
llbracket = char '⟦'; rrbracket = char '⟧'
------------------------------------------------------------------------
-- Combining two documents
infixr 5 _<>_
_<>_ : Doc → Doc → Doc
xs <> ys = mkDoc $
  let candidates = Core._<>_ <$> runDoc xs ⊛ runDoc ys in
  filter (Core.valid width) candidates
flush : Doc → Doc
flush = mkDoc ∘′ map Core.flush ∘′ runDoc
infixr 5 _<+>_
_<+>_ : Doc → Doc → Doc
x <+> y = x <> space <> y
infixr 5 _$$_
_$$_ : Doc → Doc → Doc
x $$ y = flush x <> y
infixr 4 _<|>_
_<|>_ : Doc → Doc → Doc
x <|> y = mkDoc (runDoc x ++ runDoc y)
------------------------------------------------------------------------
-- Combining lists of documents
foldDoc : (Doc → Doc → Doc) → List Doc → Doc
foldDoc _ []       = empty
foldDoc _ (x ∷ []) = x
foldDoc f (x ∷ xs) = f x (foldDoc f xs)
hsep vcat : List Doc → Doc
hsep = foldDoc _<+>_
vcat = foldDoc _$$_
sep : List Doc → Doc
sep [] = empty
sep xs = hsep xs <|> vcat xs
------------------------------------------------------------------------
-- Defined combinators
parens : Doc → Doc
parens d = lparen <> d <> rparen
commaSep : List Doc → Doc
commaSep = foldDoc (λ d e → d <> comma <+> e)
newline : Doc
newline = flush empty

------------------------------------------------------------------------
-- The Agda standard library
--
-- Pretty Printing
-- This module is based on Jean-Philippe Bernardy's functional pearl
-- "A Pretty But Not Greedy Printer"
------------------------------------------------------------------------
{-# OPTIONS --with-K #-}
module Text.Pretty.Core where
import Level
open import Data.Bool.Base using (Bool)
open import Data.Irrelevant as Irrelevant using (Irrelevant) hiding (module Irrelevant)
open import Data.List.Base as List   using (List; []; _∷_)
open import Data.Nat.Base            using (ℕ; zero; suc; _+_; _⊔_; _≤_; z≤n)
open import Data.Nat.Properties      using (≤-refl; ≤-trans; +-identityʳ;
  module ≤-Reasoning; m≤n⊔m; +-monoʳ-≤; m≤m⊔n; +-comm; _≤?_)
open import Data.Product.Base as Prod using (_×_; _,_; uncurry; proj₁; proj₂)
import Data.Product.Relation.Unary.All as Allᴾ
open import Data.Tree.Binary as Tree using (Tree; leaf; node; #nodes; mapₙ)
open import Data.Tree.Binary.Relation.Unary.All as Allᵀ using (leaf; node)
open import Data.Unit.Base using (⊤; tt)
import Data.Tree.Binary.Relation.Unary.All.Properties as Allᵀ
import Data.Tree.Binary.Properties as Tree
open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′)
open import Data.Maybe.Relation.Unary.All as Allᴹ using (nothing; just)
open import Data.String.Base as String
  using (String; length; replicate; _++_; unlines)
import Data.String.Unsafe as String
open import Function.Base using (_∘_; flip; _on_; id; _∘′_; _$_)
open import Relation.Nullary.Decidable.Core using (Dec)
open import Relation.Unary using (IUniversal; _⇒_; U)
open import Relation.Binary.PropositionalEquality.Core
  using (_≡_; refl; sym; cong; cong₂; subst)
open import Relation.Binary.PropositionalEquality.Properties
  using (module ≡-Reasoning)
open import Data.Refinement using (Refinement-syntax; _,_; value; proof)
import Data.Refinement.Relation.Unary.All as Allᴿ
------------------------------------------------------------------------
-- Block of text
-- Content is a representation of the first line and the middle of the
-- block. We use a tree rather than a list for the middle of the block
-- so that we can extend it with lines on the left and on the line for
-- free. We will ultimately render the block by traversing the tree left
-- to right in a depth-first manner.
Content : Set
Content = Maybe (String × Tree String ⊤)
size : Content → ℕ
size = maybe′ (suc ∘ #nodes ∘ proj₂) 0
All : ∀ {p} (P : String → Set p) → (Content → Set p)
All P = Allᴹ.All (Allᴾ.All P (Allᵀ.All P U))
All≤ : ℕ → Content → Set
All≤ n = All (λ s → length s ≤ n)
record Block : Set where
  field
    height    : ℕ
    block     : [ xs ∈ Content ∣ size xs ≡ height ]
  -- last line
    lastWidth : ℕ
    last      : [ s ∈ String ∣ length s ≡ lastWidth ]
  -- max of all the widths
    maxWidth  : [ n ∈ ℕ ∣ lastWidth ≤ n × All≤ n (block .value) ]
------------------------------------------------------------------------
-- Raw string
text : String → Block
text s = record
  { height    = 0
  ; block     = nothing , ⦇ refl ⦈
  ; lastWidth = width
  ; last      = s , ⦇ refl ⦈
  ; maxWidth  = width , ⦇ (≤-refl , nothing) ⦈
  } where width = length s; open Irrelevant
------------------------------------------------------------------------
-- Empty
empty : Block
empty = text ""
------------------------------------------------------------------------
-- Helper functions
node? : Content → String → Tree String ⊤ → Content
node? (just (x , xs)) y ys = just (x , node xs y ys)
node? nothing         y ys = just (y , ys)
∣node?∣ : ∀ b y ys → size (node? b y ys)
                   ≡ size b + suc (#nodes ys)
∣node?∣ (just (x , xs)) y ys = refl
∣node?∣ nothing         y ys = refl
≤-Content : ∀ {m n} {b : Content} → m ≤ n → All≤ m b → All≤ n b
≤-Content {m} {n} m≤n = Allᴹ.map (Prod.map step (Allᵀ.mapₙ step))
  where
  step : ∀ {p} → p ≤ m → p ≤ n
  step = flip ≤-trans m≤n
All≤-node? : ∀ {l m r n} →
             All≤ n l → length m ≤ n → Allᵀ.All (λ s → length s ≤ n) U r →
             All≤ n (node? l m r)
All≤-node? nothing           py pys = just (py , pys)
All≤-node? (just (px , pxs)) py pys = just (px , node pxs py pys)
------------------------------------------------------------------------
-- Appending two documents
private
  module append (x y : Block) where
    module x = Block x
    module y = Block y
    blockx = x.block .value
    blocky = y.block .value
    widthx = x.maxWidth .value
    widthy = y.maxWidth .value
    lastx = x.last .value
    lasty = y.last .value
    height : ℕ
    height = (_+_ on Block.height) x y
    lastWidth : ℕ
    lastWidth = (_+_ on Block.lastWidth) x y
    pad : Maybe String
    pad with x.lastWidth
    ... | 0         = nothing
    ... | l@(suc _) = just (replicate l ' ')
    size-pad : maybe′ length 0 pad ≡ x.lastWidth
    size-pad with x.lastWidth
    ... | 0         = refl
    ... | l@(suc _) = String.length-replicate l
    indent : Maybe String → String → String
    indent = maybe′ _++_ id
    size-indent : ∀ ma str → length (indent ma str)
                ≡ maybe′ length 0 ma + length str
    size-indent nothing    str = refl
    size-indent (just pad) str = String.length-++ pad str
    indents : Maybe String → Tree String ⊤ → Tree String ⊤
    indents = maybe′ (mapₙ ∘ _++_) id
    size-indents : ∀ ma t → #nodes (indents ma t) ≡ #nodes t
    size-indents nothing    t = refl
    size-indents (just pad) t = Tree.#nodes-mapₙ (pad ++_) t
    unfold-indents : ∀ ma t → indents ma t ≡ mapₙ (indent ma) t
    unfold-indents nothing    t = sym (Tree.map-id t)
    unfold-indents (just pad) t = refl
    vContent : Content × String
    vContent with blocky
    ... | nothing        = blockx
                         , lastx ++ lasty
    ... | just (hd , tl) = node?
      {-,--------------,-}
      {-|-} blockx   {-|-}
      {-|-}          {-'---,-}    {-,------------------,-}
      {-|-} (lastx       {-|-} ++ {-|-}  hd)         {-|-}
      {-'------------------'-}    {-|-}              {-|-}
      (indents pad                {-|-}  tl)    {-,----'-}
      , indent pad                {-|-} lasty   {-|-}
                                  {-'-------------'-}
    vBlock = proj₁ vContent
    vLast  = proj₂ vContent
    isBlock : size blockx ≡ x.height → size blocky ≡ y.height →
              size vBlock ≡ height
    isBlock ∣x∣ ∣y∣ with blocky
    ... | nothing        = begin
      size blockx         ≡⟨ ∣x∣ ⟩
      x.height            ≡⟨ +-identityʳ x.height ⟨
      x.height + 0        ≡⟨ cong (_ +_) ∣y∣ ⟩
      x.height + y.height ∎ where open ≡-Reasoning
    ... | just (hd , tl) = begin
      ∣node∣                            ≡⟨ ∣node?∣ blockx middle rest ⟩
      ∣blockx∣ + suc (#nodes rest) ≡⟨ cong ((size blockx +_) ∘′ suc) ∣rest∣ ⟩
      ∣blockx∣ + suc (#nodes tl)   ≡⟨ cong₂ _+_ ∣x∣ ∣y∣ ⟩
      x.height + y.height               ∎ where
      open ≡-Reasoning
      ∣blockx∣ = size blockx
      middle   = lastx ++ hd
      rest     = indents pad tl
      ∣rest∣   = size-indents pad tl
      ∣node∣   = size (node? blockx middle rest)
    block : [ xs ∈ Content ∣ size xs ≡ height ]
    block .value = vBlock
    block .proof = ⦇ isBlock (Block.block x .proof) (Block.block y .proof) ⦈
      where open Irrelevant
    isLastLine : length lastx ≡ x.lastWidth →
                 length lasty ≡ y.lastWidth →
                 length vLast ≡ lastWidth
    isLastLine ∣x∣ ∣y∣ with blocky
    ... | nothing        = begin
      length (lastx ++ lasty)       ≡⟨ String.length-++ lastx lasty ⟩
      length lastx + length lasty   ≡⟨ cong₂ _+_ ∣x∣ ∣y∣ ⟩
      x.lastWidth + y.lastWidth     ∎ where open ≡-Reasoning
    ... | just (hd , tl) = begin
      length (indent pad lasty)          ≡⟨ size-indent pad lasty ⟩
      maybe′ length 0 pad + length lasty ≡⟨ cong₂ _+_ size-pad ∣y∣ ⟩
      x.lastWidth + y.lastWidth          ∎ where open ≡-Reasoning
    last : [ s ∈ String ∣ length s ≡ lastWidth ]
    last .value = vLast
    last .proof = ⦇ isLastLine (Block.last x .proof) (Block.last y .proof) ⦈
      where open Irrelevant
    vMaxWidth : ℕ
    vMaxWidth = widthx ⊔ (x.lastWidth + widthy)
    isMaxWidth₁ : y.lastWidth ≤ widthy → lastWidth ≤ vMaxWidth
    isMaxWidth₁ p = begin
      lastWidth            ≤⟨ +-monoʳ-≤ x.lastWidth p ⟩
      x.lastWidth + widthy ≤⟨ m≤n⊔m _ _ ⟩
      vMaxWidth            ∎ where open ≤-Reasoning
    isMaxWidth₂ : length lastx ≡ x.lastWidth →
                  x.lastWidth ≤ widthx →
                  All≤ widthx blockx →
                  All≤ widthy blocky →
                  All≤ vMaxWidth vBlock
    isMaxWidth₂ ∣x∣≡ ∣x∣≤ ∣xs∣ ∣ys∣ with blocky
    ... | nothing        = ≤-Content (m≤m⊔n _ _) ∣xs∣
    isMaxWidth₂ ∣x∣≡ ∣x∣≤ ∣xs∣ (just (∣hd∣ , ∣tl∣))
        | just (hd , tl) =
      All≤-node? (≤-Content (m≤m⊔n _ _) ∣xs∣)
                 middle
                 (subst (Allᵀ.All _ U) (sym $ unfold-indents pad tl)
                 $ Allᵀ.mapₙ⁺ (indent pad) (Allᵀ.mapₙ (indented _) ∣tl∣))
      where
      middle : length (lastx ++ hd) ≤ vMaxWidth
      middle = begin
        length (lastx ++ hd)     ≡⟨ String.length-++ lastx hd ⟩
        length lastx + length hd ≡⟨ cong (_+ _) ∣x∣≡ ⟩
        x.lastWidth + length hd  ≤⟨ +-monoʳ-≤ x.lastWidth ∣hd∣ ⟩
        x.lastWidth + widthy     ≤⟨ m≤n⊔m _ _ ⟩
        vMaxWidth                ∎ where open ≤-Reasoning
      indented : ∀ s → length s ≤ widthy →
                 length (indent pad s) ≤ vMaxWidth
      indented s ∣s∣ = begin
        length (indent pad s)          ≡⟨ size-indent pad s ⟩
        maybe′ length 0 pad + length s ≡⟨ cong (_+ _) size-pad ⟩
        x.lastWidth + length s         ≤⟨ +-monoʳ-≤ x.lastWidth ∣s∣ ⟩
        x.lastWidth + widthy           ≤⟨ m≤n⊔m (widthx) _ ⟩
        vMaxWidth                      ∎ where open ≤-Reasoning
    maxWidth : [ n ∈ ℕ ∣ lastWidth ≤ n × All≤ n vBlock ]
    maxWidth .value = vMaxWidth
    maxWidth .proof =
      ⦇ _,_ ⦇ isMaxWidth₁ (map proj₁ (Block.maxWidth y .proof)) ⦈
            ⦇ isMaxWidth₂ (Block.last x .proof)
                          (map proj₁ (Block.maxWidth x .proof))
                          (map proj₂ (Block.maxWidth x .proof))
                          (map proj₂ (Block.maxWidth y .proof))
            ⦈
      ⦈ where open Irrelevant
infixl 4 _<>_
_<>_ : Block → Block → Block
x <> y = record { append x y }
------------------------------------------------------------------------
-- Flush (introduces a new line)
private
  module flush (x : Block) where
    module x = Block x
    blockx  = x.block .value
    lastx   = x.last .value
    widthx  = x.maxWidth .value
    heightx = x.height
    height    = suc heightx
    lastWidth = 0
    vMaxWidth = widthx
    last : [ s ∈ String ∣ length s ≡ lastWidth ]
    last = "" , ⦇ refl ⦈ where open Irrelevant
    vContent = node? blockx lastx (leaf tt)
    isBlock : size blockx ≡ heightx → size vContent ≡ height
    isBlock ∣x∣ = begin
      size vContent   ≡⟨ ∣node?∣ blockx lastx (leaf tt) ⟩
      size blockx + 1 ≡⟨ cong (_+ 1) ∣x∣ ⟩
      heightx + 1     ≡⟨ +-comm heightx 1 ⟩
      height          ∎ where open ≡-Reasoning
    block : [ xs ∈ Content ∣ size xs ≡ height ]
    block .value = vContent
    block .proof = Irrelevant.map isBlock $ Block.block x .proof
    maxWidth : [ n ∈ ℕ ∣ lastWidth ≤ n × All≤ n vContent ]
    maxWidth .value = widthx
    maxWidth .proof = map (z≤n ,_)
      ⦇ All≤-node? ⦇ proj₂ (Block.maxWidth x .proof) ⦈
                   ⦇ middle (Block.last x .proof) ⦇ proj₁ (Block.maxWidth x .proof) ⦈ ⦈
                   (pure (leaf tt))
      ⦈ where
      open Irrelevant
      middle : length lastx ≡ x.lastWidth → x.lastWidth ≤ vMaxWidth →
               length lastx ≤ vMaxWidth
      middle p q = begin
        length lastx ≡⟨ p ⟩
        x.lastWidth  ≤⟨ q ⟩
        vMaxWidth    ∎ where open ≤-Reasoning
flush : Block → Block
flush x = record { flush x }
------------------------------------------------------------------------
-- Other functions
render : Block → String
render x = unlines
  $ maybe′ (uncurry (λ hd tl → hd ∷ Tree.Infix.toList tl)) []
  $ node? (Block.block x .value) (Block.last x .value) (leaf tt)
valid : (width : ℕ) (b : Block) → Dec (Block.maxWidth b .value ≤ width)
valid width b = Block.maxWidth b .value ≤? width