blob: aa74ee2222e4550484dda5dcb8cbf57c35549b45 (
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
|
(* ========================================================================== *)
(* PRINTER UTILITIES (HOL LIGHT) *)
(* - Various basic utilities used in writing the exporters *)
(* *)
(* By Mark Adams *)
(* Copyright (c) Univeristy of Edinburgh, 2012 *)
(* ========================================================================== *)
(* Basics *)
let print_string_if b x = if b then print_string x;;
let print_fstring x = print_string ("\"" ^ String.escaped x ^ "\"");;
let print_fterm tm = print_string ("`" ^ string_of_term tm ^ "`");;
let print_ftype ty = print_string ("`" ^ string_of_type ty ^ "`");;
let print_goalid id = print_int id;;
let print_indent d = print_string (String.make d ' ');;
(* Printer for 'mldata' *)
let rec print_mlarg br arg =
match arg with
Mlint n -> print_int n
| Mlstring x -> print_fstring x
| Mlterm tm -> print_fterm tm
| Mltype ty -> print_ftype ty
| Mlthm prf -> print_mldata br prf
| Mlpair (arg1,arg2)
-> let sep =
if (forall is_atomic_mlarg [arg1;arg2]) then "," else ", " in
(print_string_if br "(";
print_mlarg false arg1;
print_string sep;
print_mlarg false arg2;
print_string_if br ")")
| Mllist args
-> let sep = if (forall is_atomic_mlarg args) then ";" else "; " in
(print_string "[";
print_seplist (print_mlarg false) sep args;
print_string "]")
| Mlfn f
-> (print_mldata br f)
and print_mldata br ((x,args):mldata) =
(print_string_if (br & not (is_empty args)) "(";
print_string x;
do_list (fun arg -> print_string " "; print_mlarg true arg) args;
print_string_if (br & not (is_empty args)) ")");;
(* Printer for labels *)
let print_label l =
match l with
Tactical (x,_) | Label x -> print_fstring x;;
|
