Source file Specs.ml

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
(** An [ENRICHER] is a type that represents a capability that
    can be added to strings. *)
module type ENRICHER = sig
  type t

  val ( = ) : t -> t -> bool
  val enrich : t -> string -> string
end

module type TYPE = sig
  (** The type of a rich string. *)

  (** The enricher. *)
  module Enricher : ENRICHER

  (** The type of a rich string. *)
  type t =
    | Empty
    | String of string
    | Enriched of Enricher.t * t
    | Join of t * t list

  (** [rs1 = rs2] determines whether [rs1] and [rs2] are equal.

      {b IMPORTANT:} no pruning or optimization is performed.
      This means that two rich strings that render the same
      might not be considered equal. *)
  val ( = ) : t -> t -> bool

  (** [empty] is the identity string with respect to {!( ++ )}. *)
  val empty : t

  (** [rs1 ++ rs2] appends [rs2] at the end of [rs1].

      It is equivalent to the built-in string operator [^].

      {[
        # print (String "hello" ++ String "world")
        "helloworld"
        - : unit = ()
      ]} *)
  val ( ++ ) : t -> t -> t

  (** [string s] lifts the built-in string [s] to the enriched
      world.

      For example, if the enricher is an ANSI style type, this
      enables the ability to stylize [s]. *)
  val string : string -> t

  (** [enrich enrichment rs] adds the [enrichment] to the rich
      string [rs].

      For example, if the enricher is an ANSI style type, this
      translates to adding a new style to [s]. *)
  val enrich : Enricher.t -> t -> t

  (** [join ?on:sep rss] concatenates all [rss] into one,
      separated by [sep]. By default, [sep] is a single space.

      It is equivalent to the built-in string function
      [String.concat]. *)
  val join : ?on:t -> t list -> t

  (** [flatten rss] concatenates all [rss] into one.
  
      It is equivalent to {!join}[~on:Empty rss]. *)
  val flatten : t list -> t

  (** [join_lines rss] concatenates all [rss] into one,
      separated by line feeds.

      It is equivalent to {!join}[~on:(String "\n") rss]. *)
  val join_lines : t list -> t

  (** [is_empty rs] tests whether [rs] is [Empty]. *)
  val is_empty : t -> bool

  (** [is_enriched rs] tests whether [rs] is {i not} just a
      plain [String]. *)
  val is_enriched : t -> bool

  (** [render rs] generates a built-in string such that [rs]
      can be used in interfaces that expect strings, e.g. IO. *)
  val render : t -> string

  (** [print ?out ?ending rs] prints [rs] in [out], appending
      [ending] after. [out] defaults to [stdout] and [ending]
      defaults to [Some (String "\n")]. *)
  val print : ?out:out_channel -> ?ending:t option -> t -> unit
end