print_coq.ml 10.7 KB
Newer Older
1 2 3
open PPrint
open Coq

POTTIER Francois's avatar
POTTIER Francois committed
4
(* These functions could move to [PPrint]. *)
POTTIER Francois's avatar
POTTIER Francois committed
5

6
let sprintf format =
POTTIER Francois's avatar
POTTIER Francois committed
7
  Printf.ksprintf arbitrary_string format
8

POTTIER Francois's avatar
POTTIER Francois committed
9 10 11 12 13
let run (print : Buffer.t -> 'a -> unit) (x : 'a) : string =
  let b = Buffer.create 1024 in
  print b x;
  Buffer.contents b

14 15
(* -------------------------------------------------------------------------- *)

16 17 18 19 20 21
(* Global parameters. *)

let indentation =
  2

let width =
22
  ref 80
23 24 25

(* -------------------------------------------------------------------------- *)

26 27 28
(* Various fixed elements. *)

let arrow =
POTTIER Francois's avatar
POTTIER Francois committed
29
  string "->"
30 31

let doublearrow =
32
  string "=>"
33 34

let colonequals =
POTTIER Francois's avatar
POTTIER Francois committed
35
  string ":="
36

POTTIER Francois's avatar
POTTIER Francois committed
37 38
let spacecolon =
  string " :"
39

POTTIER Francois's avatar
POTTIER Francois committed
40 41
(* -------------------------------------------------------------------------- *)

42 43 44
(* Applications. *)

let app d1 d2 =
45 46
  (* The following definition would reject a large argument on a line of
     its own, indented: *)
47
  (* group (d1 ^^ nest indentation (break 1 ^^ d2)) *)
48 49 50 51
  (* However, that would be redundant with the fact that large arguments
     are usually parenthesized, and we already break lines and indent
     within the parentheses. So, the following suffices: *)
  group (d1 ^^ space ^^ d2)
52 53 54 55 56 57 58 59

let apps ds =
  match ds with
  | [] ->
      assert false
  | d :: ds ->
     List.fold_left app d ds

60 61
(* -------------------------------------------------------------------------- *)

62 63 64 65 66
(* A block with indentation. *)

let block n opening contents closing =
  group (opening ^^ nest n (contents) ^^ closing)

67 68 69
let block =
  block indentation

70 71
(* -------------------------------------------------------------------------- *)

72 73 74 75
(* Parentheses with indentation. *)

(* We allow breaking a parenthesized thing into several lines by leaving the
   opening and closing parentheses alone on a line and indenting the content. *)
76

77
let parens d =
78 79 80 81
  block
    lparen
    (break 0 ^^ d)
    (break 0 ^^ rparen)
82

83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98
(* Braces with spacing and indentation. *)

let braces d =
  block
    lbrace
    (break 1 ^^ d)
    (break 1 ^^ rbrace)

(* Brackets with spacing and indentation. *)

let brackets d =
  block
    lbracket
    (break 1 ^^ d)
    (break 1 ^^ rbracket)

POTTIER Francois's avatar
POTTIER Francois committed
99 100
(* -------------------------------------------------------------------------- *)

101 102 103 104
(* Tuples. *)

let tuple expr es =
  parens (separate_map (comma ^^ break 1) expr es)
105 106 107

(* -------------------------------------------------------------------------- *)

charguer's avatar
charguer committed
108 109
(* FOR FUTURE USE 
   Labels (part of [Coq_tag]). *)
110 111 112 113 114 115

let label = function
  | None ->
      string "_"
  | Some l ->
      parens (
POTTIER Francois's avatar
POTTIER Francois committed
116
        string "Label_create" ^/^ squote ^^ string l
117 118
      )

POTTIER Francois's avatar
POTTIER Francois committed
119 120
(* -------------------------------------------------------------------------- *)

121 122 123 124 125 126 127
(* Bindings, or annotations: [x : t]. *)

let binding x t =
  block (x ^^ spacecolon) (space ^^ t) empty

(* -------------------------------------------------------------------------- *)

POTTIER Francois's avatar
POTTIER Francois committed
128 129
(* Expressions. *)

130 131 132
let rec expr0 = function
  | Coq_var s ->
      string s
charguer's avatar
charguer committed
133 134
  | Coq_nat n ->
      parens (string (string_of_int n)) ^^ string "%nat"
135 136
  | Coq_int n ->
      parens (string (string_of_int n)) ^^ string "%Z"
charguer's avatar
charguer committed
137
   (* DEPRECATED ; maybe future ?
charguer's avatar
charguer committed
138
  | Coq_list cs ->
charguer's avatar
charguer committed
139
      if (cs = []) then string cnil else 
charguer's avatar
charguer committed
140
        parens ((separate_map (string "::" ^^ break 1) expr0 cs) ^^ string "::nil")
charguer's avatar
charguer committed
141
     *)
142 143 144 145 146 147 148 149 150
  | Coq_wild ->
      string "_"
  | Coq_prop ->
      string "Prop"
  | Coq_type ->
      string "Type"
  | Coq_tuple [] ->
      expr0 coq_tt
  | Coq_tuple es ->
151
      tuple expr es
152 153 154
  | Coq_record _les ->
      assert false (* TODO *)
  | Coq_annot (e1, e2) ->
155
      parens (binding (expr e1) (expr e2))
156 157 158 159 160 161 162
  | Coq_app _
  | Coq_tag _
  | Coq_impl _
  | Coq_lettuple _
  | Coq_forall _
  | Coq_fun _
    as e ->
163
      parens (expr e)
164 165 166 167

and expr1 = function
  | Coq_app (e1, e2) ->
      app (expr1 e1) (expr0 e2)
charguer's avatar
charguer committed
168 169 170 171 172 173
  | Coq_tag (tag, args, l, e) ->
      let stag =
        if args = [] 
           then string tag 
           else parens (apps ((string tag)::(List.map expr0 args)))
        in
174
      apps [
charguer's avatar
charguer committed
175
        string "CFML.CFPrint.tag"; (* @ *)
charguer's avatar
charguer committed
176
        stag;
charguer's avatar
charguer committed
177
        (* FUTURE USE: label l;*)
charguer's avatar
charguer committed
178
        (* string "_"; *)
179 180 181 182 183 184 185
        expr0 e
      ]
  | e ->
     expr0 e

and expr2 = function
  | Coq_impl (e1, e2) ->
POTTIER Francois's avatar
POTTIER Francois committed
186
      group (expr1 e1 ^^ space ^^ arrow ^/^ expr2 e2)
187 188 189 190 191
  | e ->
      expr1 e

and expr3 = function
  | Coq_lettuple (es, e1, e2) ->
192
      block
POTTIER Francois's avatar
POTTIER Francois committed
193
        (string "let '" ^^ tuple expr es ^^ space ^^ colonequals)
194
        (break 1 ^^ expr e1)
POTTIER Francois's avatar
POTTIER Francois committed
195
        (break 1 ^^ string "in")
196 197 198
      ^/^
      expr3 e2
  | Coq_forall ((x, e1), e2) ->
199
      block
POTTIER Francois's avatar
POTTIER Francois committed
200
        (string "forall " ^^ string x ^^ spacecolon)
201 202 203
        (break 1 ^^ expr e1 ^^ comma)
        empty
      ^/^
POTTIER Francois's avatar
POTTIER Francois committed
204
      expr3 e2
205
  | Coq_fun ((x, e1), e2) ->
206
      block
POTTIER Francois's avatar
POTTIER Francois committed
207
        (string "fun " ^^ string x ^^ spacecolon)
208 209
        (break 1 ^^ expr e1)
        (break 1 ^^ doublearrow)
210 211
      ^/^
      expr3 e2
212 213 214 215 216 217
  | e ->
      expr2 e

and expr e =
  expr3 e

POTTIER Francois's avatar
POTTIER Francois committed
218 219
(* -------------------------------------------------------------------------- *)

220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252
(* Module types. *)

let rec mod_typ0 = function
  | Mod_typ_var x ->
      string x
  | Mod_typ_app _
  | Mod_typ_with_def _
  | Mod_typ_with_mod _
    as mt ->
      parens (mod_typ mt)

and mod_typ1 = function
  | Mod_typ_app xs -> 
      separate_map space string xs
  | mt ->
      mod_typ0 mt

and mod_typ2 = function
  | Mod_typ_with_def (mt, x, e) ->
      mod_typ2 mt ^/^
      block
        (string "with Definition " ^^ string x ^^ space ^^ colonequals)
        (break 1 ^^ expr e)
        empty
  | Mod_typ_with_mod (mt, x, y) ->
      mod_typ2 mt ^/^
      sprintf "with Module %s := %s " x y
  | mt ->
      mod_typ1 mt

and mod_typ mt =
  mod_typ1 mt

253 254 255 256 257
(* Module bindings. *)

let mod_binding (xs, mt) = 
  binding (separate_map space string xs) (mod_typ mt)

258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285
let pmod_binding mb =
  space ^^ parens (mod_binding mb)

let pmod_bindings mbs = 
  group (concat_map pmod_binding mbs)

(* Module expressions. *)

let mod_expr xs =
  separate_map space string xs

(* Module definitions. *)

let mod_def = function
  | Mod_def_inline me ->
      block (space ^^ colonequals) (break 1 ^^ mod_expr me) dot
  | Mod_def_declare ->
      dot

(* Module casts. *)

let mod_cast = function
  | Mod_cast_exact mt ->
      spacecolon ^^ space ^^ mod_typ mt
  | Mod_cast_super mt ->
      space ^^ string "<:" ^^ space ^^ mod_typ mt
  | Mod_cast_free ->
      empty
286

287 288
(* -------------------------------------------------------------------------- *)

289
(* Typed variables: [x : t]. *)
290 291 292 293

(* Raw. *)

let var (x, t) =
294
  binding (string x) (expr t)
295

296
(* With parentheses and with a leading space. *)
297 298

let pvar xt =
299
  space ^^ parens (var xt)
300 301

let pvars xts =
302
  group (concat_map pvar xts)
303 304 305 306 307 308 309 310

(* A list of field declarations, separated with semicolons. *)

let fields xts =
  separate_map (semi ^^ break 1) var xts

(* -------------------------------------------------------------------------- *)

POTTIER Francois's avatar
POTTIER Francois committed
311
(* Tools for toplevel elements. *)
312 313

(* A definition, without a leading keyword, but with a leading space.
314
   [ x : d1 :=]. *)
315

316
let definition x d1 =
317
  block
POTTIER Francois's avatar
POTTIER Francois committed
318
    (space ^^ x ^^ spacecolon)
319
    (break 1 ^^ d1)
POTTIER Francois's avatar
POTTIER Francois committed
320
    (break 1 ^^ colonequals)
321 322

(* A parameter, without a leading keyword, but with a leading space.
323
   [ x : d1.]. *)
324 325 326

let parameter x d1 =
  block
POTTIER Francois's avatar
POTTIER Francois committed
327
    (space ^^ x ^^ spacecolon)
328
    (break 1 ^^ d1)
329
    dot
330

331
(* The right-hand side of a record declaration. [ Foo { ... }]. *)
332 333

let record_rhs r =
334
  space ^^
charguer's avatar
charguer committed
335
  string (r.coqind_constructor_name) ^^ space ^^
336 337 338 339 340 341
  braces (fields r.coqind_branches)

(* The right-hand side of a sum declaration. [| x1 : T1 | x2 : T2 ...]. *)

let sum_rhs r =
  concat_map (fun xt ->
342
    hardline ^^ block (string "| ") (var xt) empty
343 344 345 346 347 348
  ) r.coqind_branches

(* The left-hand side of a record or sum declaration. [ foo params : T := rhs]. *)

let inductive_lhs rhs r =
  definition
349
    (string r.coqind_name ^^ pvars r.coqind_targs)
350
    (expr r.coqind_ret)
351 352
  ^^
  rhs r
353

354 355 356 357 358 359 360 361 362
(* An implicit argument specification. *)

let implicit (x, i) = 
  match i with
  | Coqi_maximal ->
      brackets (string x)
  | Coqi_implicit ->
      string x
  | Coqi_explicit ->
363
      sprintf "(* %s *)" x
364

POTTIER Francois's avatar
POTTIER Francois committed
365 366 367
(* -------------------------------------------------------------------------- *)

(* Toplevel elements. *)
368 369 370 371

let top = function
  | Coqtop_def ((x, e1), e2) ->
      string "Definition" ^^
372 373
      definition (string x) (expr e1) ^/^
      expr e2 ^^ dot
374 375
  | Coqtop_param (x, e1) ->
      string "Parameter" ^^
376
      parameter (string x) (expr e1)
377 378
  | Coqtop_instance ((x, e1), global) ->
      string ((if global then "Global " else "") ^ "Instance") ^^
379
      parameter (string x) (expr e1)
380 381
  | Coqtop_lemma (x, e1) ->
      string "Lemma" ^^
382
      parameter (string x) (expr e1)
383
  | Coqtop_proof s ->
384
      sprintf "Proof. %s Qed." s
385 386 387
  | Coqtop_record r ->
      string "Record" ^^
      inductive_lhs record_rhs r
388
      ^^ dot
389 390 391 392 393 394
  | Coqtop_ind rs ->
      string "Inductive" ^^
      separate_map
        (hardline ^^ hardline ^^ string "with")
        (inductive_lhs sum_rhs)
        rs
395 396
      ^^ dot
  | Coqtop_label (x, n) ->
POTTIER Francois's avatar
POTTIER Francois committed
397 398
      sprintf "Notation \"''%s'\" := (%s) (at level 0) : atom_scope."
        x (value_variable n)
399 400
  | Coqtop_implicit (x, xs) -> 
      string "Implicit Arguments " ^^
401
      string x ^/^
POTTIER Francois's avatar
POTTIER Francois committed
402
      brackets (flow_map space implicit xs)
403 404
      ^^ dot
  | Coqtop_register (db, x, v) ->
charguer's avatar
charguer committed
405
      sprintf "Hint Extern 1 (Register %s %s) => CFHeader_Provide %s." db x v
406 407
  | Coqtop_hint_constructors (xs, base) ->
      string "Hint Constructors " ^^
POTTIER Francois's avatar
POTTIER Francois committed
408
      flow_map space string xs ^^
POTTIER Francois's avatar
POTTIER Francois committed
409
      spacecolon ^/^
410 411 412 413
      string base
      ^^ dot
  | Coqtop_hint_unfold (xs, base) ->
      string "Hint Unfold " ^^
POTTIER Francois's avatar
POTTIER Francois committed
414
      flow_map space string xs ^^
POTTIER Francois's avatar
POTTIER Francois committed
415
      spacecolon ^/^
416 417
      string base
      ^^ dot
charguer's avatar
charguer committed
418 419 420 421 422 423 424 425 426 427 428 429
  | Coqtop_require xs ->
      string "Require " ^^
      flow_map space string xs
      ^^ dot
  | Coqtop_import xs ->
      string "Import " ^^
      flow_map space string xs 
      ^^ dot
  | Coqtop_require_import xs ->
      string "Require Import " ^^
      flow_map space string xs 
      ^^ dot
430 431 432
  | Coqtop_set_implicit_args -> 
      sprintf "Set Implicit Arguments."
  | Coqtop_text s -> 
433
      sprintf "%s" s
434 435 436 437 438 439 440 441 442 443 444 445 446 447
  | Coqtop_declare_module (x, mt) ->
      string "Declare Module" ^^
      parameter (string x) (mod_typ mt)
  | Coqtop_module (x, bs, c, d) ->
      string "Module" ^^ space ^^
      string x ^^
      pmod_bindings bs ^^
      mod_cast c ^^
      mod_def d
  | Coqtop_module_type (x, bs, d) ->
      string "Module Type" ^^ space ^^
      string x ^^
      pmod_bindings bs ^^
      mod_def d
448 449 450 451
  | Coqtop_module_type_include x ->
      sprintf "Include Type %s." x
  | Coqtop_end x ->
      sprintf "End %s." x
charguer's avatar
charguer committed
452 453 454
  | Coqtop_custom x ->
      sprintf "%s" x

455 456 457 458 459 460 461

let top t =
  group (top t)

let tops ts =
  concat_map (fun t -> top t ^^ hardline ^^ hardline) ts

462 463
(* -------------------------------------------------------------------------- *)

POTTIER Francois's avatar
POTTIER Francois committed
464 465
(* The main entry point translates a list of toplevel elements to a string. *)

466
let tops ts : string =
467
  run (PPrintEngine.ToBuffer.pretty 0.9 !width) (tops ts)
468