File: Main.agda

package info (click to toggle)
agda-stdlib 2.1-4
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 9,196 kB
  • sloc: haskell: 375; makefile: 32; sh: 28; lisp: 1
file content (83 lines) | stat: -rw-r--r-- 2,091 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
-- 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" ∷ [])
          ∷ []))