blob: 9131e18debbbf5ad2278bdfcd1820bc452aadc17 (
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 'finfo' *)
let rec print_farg x0 br arg =
match arg with
Fint n -> print_int n
| Fstring x -> print_fstring x
| Fterm tm -> print_fterm tm
| Ftype ty -> print_ftype ty
| Fthm prf -> print_finfo "<rule>" br prf
| Fpair (arg1,arg2)
-> let sep = if (forall is_atomic_farg [arg1;arg2]) then "," else ", " in
(print_string_if br "(";
print_farg x0 false arg1;
print_string sep;
print_farg x0 false arg2;
print_string_if br ")")
| Flist args
-> let sep = if (forall is_atomic_farg args) then ";" else "; " in
(print_string "[";
print_seplist (print_farg x0 false) sep args;
print_string "]")
| Ffn f
-> (print_finfo x0 br f)
and print_finfo x0 br ((x_,args):finfo) =
(print_string_if (br & not (is_empty args)) "(";
print_option x0 x_;
do_list (fun arg -> print_string " "; print_farg x0 true arg) args;
print_string_if (br & not (is_empty args)) ")");;
(* Printer for labels *)
let print_label l =
match l with
Tactical (Some x, _) | Label x -> print_fstring x
| Tactical (None, _) -> print_fstring "<tactical>";;
|
