src/Tools/Metis/src/Print.sig
author blanchet
Thu, 16 Sep 2010 07:30:15 +0200
changeset 39444 beabb8443ee4
parent 39443 e330437cd22a
child 39501 aaa7078fff55
permissions -rw-r--r--
MIT license -> BSD License
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     1
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     2
(* PRETTY-PRINTING                                                           *)
39444
beabb8443ee4 MIT license -> BSD License
blanchet
parents: 39443
diff changeset
     3
(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License            *)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     4
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     5
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     6
signature Print =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     7
sig
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     8
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     9
(* ------------------------------------------------------------------------- *)
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    10
(* Escaping strings.                                                         *)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    11
(* ------------------------------------------------------------------------- *)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    12
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    13
val escapeString : {escape : char list} -> string -> string
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    14
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    15
(* ------------------------------------------------------------------------- *)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    16
(* A type of strings annotated with their size.                              *)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    17
(* ------------------------------------------------------------------------- *)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    18
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    19
type stringSize = string * int
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    20
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    21
val mkStringSize : string -> stringSize
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    22
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    23
(* ------------------------------------------------------------------------- *)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    24
(* A type of pretty-printers.                                                *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    25
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    26
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    27
datatype breakStyle = Consistent | Inconsistent
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    28
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    29
datatype step =
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    30
    BeginBlock of breakStyle * int
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    31
  | EndBlock
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    32
  | AddString of stringSize
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    33
  | AddBreak of int
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    34
  | AddNewline
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    35
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    36
type ppstream = step Stream.stream
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    37
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    38
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    39
(* Pretty-printer primitives.                                                *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    40
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    41
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    42
val beginBlock : breakStyle -> int -> ppstream
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    43
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    44
val endBlock : ppstream
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    45
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    46
val addString : stringSize -> ppstream
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    47
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    48
val addBreak : int -> ppstream
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    49
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    50
val addNewline : ppstream
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    51
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    52
val skip : ppstream
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    53
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    54
val sequence : ppstream -> ppstream -> ppstream
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    55
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    56
val duplicate : int -> ppstream -> ppstream
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    57
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    58
val program : ppstream list -> ppstream
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    59
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    60
val stream : ppstream Stream.stream -> ppstream
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    61
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    62
val block : breakStyle -> int -> ppstream -> ppstream
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    63
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    64
val blockProgram : breakStyle -> int -> ppstream list -> ppstream
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    65
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    66
(* ------------------------------------------------------------------------- *)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    67
(* Executing pretty-printers to generate lines.                              *)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    68
(* ------------------------------------------------------------------------- *)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    69
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    70
val execute :
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    71
    {lineLength : int} -> ppstream ->
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    72
    {indent : int, line : string} Stream.stream
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    73
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    74
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    75
(* Pretty-printer combinators.                                               *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    76
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    77
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    78
type 'a pp = 'a -> ppstream
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    79
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    80
val ppMap : ('a -> 'b) -> 'b pp -> 'a pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    81
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    82
val ppString : string pp
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
    83
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    84
val ppBracket : string -> string -> 'a pp -> 'a pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    85
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    86
val ppOp : string -> ppstream
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    87
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    88
val ppOp2 : string -> 'a pp -> 'b pp -> ('a * 'b) pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    89
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    90
val ppOp3 : string -> string -> 'a pp -> 'b pp -> 'c pp -> ('a * 'b * 'c) pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    91
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    92
val ppOpList : string -> 'a pp -> 'a list pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    93
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    94
val ppOpStream : string -> 'a pp -> 'a Stream.stream pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    95
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    96
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    97
(* Pretty-printers for common types.                                         *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    98
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    99
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   100
val ppChar : char pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   101
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   102
val ppEscapeString : {escape : char list} -> string pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   103
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   104
val ppUnit : unit pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   105
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   106
val ppBool : bool pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   107
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   108
val ppInt : int pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   109
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   110
val ppPrettyInt : int pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   111
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   112
val ppReal : real pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   113
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   114
val ppPercent : real pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   115
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   116
val ppOrder : order pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   117
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   118
val ppList : 'a pp -> 'a list pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   119
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   120
val ppStream : 'a pp -> 'a Stream.stream pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   121
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   122
val ppOption : 'a pp -> 'a option pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   123
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   124
val ppPair : 'a pp -> 'b pp -> ('a * 'b) pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   125
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   126
val ppTriple : 'a pp -> 'b pp -> 'c pp -> ('a * 'b * 'c) pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   127
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   128
val ppBreakStyle : breakStyle pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   129
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   130
val ppStep : step pp
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   131
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   132
val ppPpstream : ppstream pp
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   133
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   134
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   135
(* Pretty-printing infix operators.                                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   136
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   137
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   138
type token = string
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   139
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   140
datatype assoc =
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   141
    LeftAssoc
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   142
  | NonAssoc
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   143
  | RightAssoc
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   144
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   145
datatype infixes =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   146
    Infixes of
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   147
      {token : token,
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   148
       precedence : int,
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   149
       assoc : assoc} list
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   150
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   151
val tokensInfixes : infixes -> StringSet.set
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   152
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   153
val layerInfixes : infixes -> {tokens : StringSet.set, assoc : assoc} list
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   154
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   155
val ppInfixes :
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   156
    infixes ->
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   157
    ('a -> (token * 'a * 'a) option) -> ('a * token) pp ->
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39349
diff changeset
   158
    ('a * bool) pp -> ('a * bool) pp
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   159
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   160
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   161
(* Executing pretty-printers with a global line length.                      *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   162
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   163
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   164
val lineLength : int ref
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   165
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   166
val toString : 'a pp -> 'a -> string
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   167
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   168
val toStream : 'a pp -> 'a -> string Stream.stream
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   169
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   170
val trace : 'a pp -> string -> 'a -> unit
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   171
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   172
end