blob: 95a3b648841a76b8245d3c8820eef172e5f958df (
plain)
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
|
(** [show.lem] exports the typeclass [Show] and associated functions for pretty
* printing arbitrary values.
*)
open import Function
open import List
open import Maybe
open import Num
open import String
open import Missing_pervasives
class (Show 'a)
val show : 'a -> string
end
(** [string_of_bool b] produces a string representation of boolean [b].
*)
val string_of_bool : bool -> string
let string_of_bool b =
match b with
| true -> "true"
| false -> "false"
end
instance (Show bool)
let show = string_of_bool
end
instance (Show string)
let show = id
end
(** [string_of_pair p] produces a string representation of pair [p].
*)
val string_of_pair : forall 'a 'b. Show 'a, Show 'b => ('a * 'b) -> string
let string_of_pair (left, right) =
"(" ^ show left ^ ", " ^ show right ^ ")"
instance forall 'a 'b. Show 'a, Show 'b => (Show ('a * 'b))
let show = string_of_pair
end
(** [string_of_list l] produces a string representation of list [l].
*)
val string_of_list : forall 'a. Show 'a => list 'a -> string
let string_of_list l =
let result = intercalate "," (List.map show l) in
let folded = foldr (^) "" result in
"[" ^ folded ^ "]"
instance forall 'a. Show 'a => (Show (list 'a))
let show = string_of_list
end
val string_of_maybe : forall 'a. Show 'a => maybe 'a -> string
let string_of_maybe m =
match m with
| Nothing -> "Nothing"
| Just e -> "Just " ^ show e
end
instance forall 'a. Show 'a => (Show (maybe 'a))
let show = string_of_maybe
end
instance (Show nat)
let show = string_of_nat
end
|
