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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples of format strings and printf
------------------------------------------------------------------------
{-# OPTIONS --safe --cubical-compatible #-}
module README.Text.Printf where
open import Data.Nat.Base
open import Data.Char.Base
open import Data.List.Base
open import Data.String.Base
open import Data.Sum.Base
open import Relation.Binary.PropositionalEquality
------------------------------------------------------------------------
-- Format strings
open import Text.Format
-- We can specify a format by writing a string which will get interpreted
-- by a lexer into a list of formatting directives.
-- The specification types are always started with a '%' character:
-- Integers (%d or %i)
-- Naturals (%u)
-- Floats (%f)
-- Chars (%c)
-- Strings (%s)
-- Anything which is not a type specification is a raw string to be spliced
-- in the output of printf.
-- For instance the following format alternates types and raw strings
_ : lexer "%s: %u + %u ≡ %u"
≡ inj₂ (`String ∷ Raw ": " ∷ `ℕ ∷ Raw " + " ∷ `ℕ ∷ Raw " ≡ " ∷ `ℕ ∷ [])
_ = refl
-- Lexing can fail. There are two possible errors:
-- If we start a specification type with a '%' but the string ends then
-- we get an UnexpectedEndOfString error
_ : lexer "%s: %u + %u ≡ %"
≡ inj₁ (UnexpectedEndOfString "%s: %u + %u ≡ %")
_ = refl
-- If we start a specification type with a '%' and the following character
-- does not correspond to an existing type, we get an InvalidType error
-- together with a focus highlighting the position of the problematic type.
_ : lexer "%s: %u + %a ≡ %u"
≡ inj₁ (InvalidType "%s: %u + %" 'a' " ≡ %u")
_ = refl
------------------------------------------------------------------------
-- Printf
open import Text.Printf
-- printf is a function which takes a format string as an argument and
-- returns a function expecting a value for each type specification present
-- in the format and returns a string splicing in these values into the
-- format string.
-- For instance `printf "%s: %u + %u ≡ %u"` is a
-- `String → ℕ → ℕ → ℕ → String` function.
_ : String → ℕ → ℕ → ℕ → String
_ = printf "%s: %u + %u ≡ %u"
_ : printf "%s: %u + %u ≡ %u" "example" 3 2 5
≡ "example: 3 + 2 ≡ 5"
_ = refl
-- If the format string str is invalid then `printf str` will have type
-- `Error e` where `e` is the lexing error.
_ : Text.Printf.Error (UnexpectedEndOfString "%s: %u + %u ≡ %")
_ = printf "%s: %u + %u ≡ %"
_ : Text.Printf.Error (InvalidType "%s: %u + %" 'a' " ≡ %u")
_ = printf "%s: %u + %a ≡ %u"
-- Trying to pass arguments to such an ̀Error` type will lead to a
-- unification error which hopefully makes the problem clear e.g.
-- `printf "%s: %u + %a ≡ %u" "example" 3 2 5` fails with the error:
-- Text.Printf.Error (InvalidType "%s: %u + %" 'a' " ≡ %u") should be
-- a function type, but it isn't
-- when checking that "example" 3 2 5 are valid arguments to a
-- function of type Text.Printf.Printf (lexer "%s: %u + %a ≡ %u")
|
