-
Notifications
You must be signed in to change notification settings - Fork 85
/
PrettyPrinterProgScript.sml
132 lines (102 loc) · 3.52 KB
/
PrettyPrinterProgScript.sml
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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
(*
Module providing pretty-printer implementation, and setup
of the global builtin pretty-printer functions.
*)
open
preamble
ml_translatorLib
ml_progLib
mlprettyprinterTheory
astSyntax
local open IntProgTheory addPrettyPrintersLib in end
val _ = (
new_theory "PrettyPrinterProg";
translation_extends "IntProg"
)
val previous_prog_pps = get_prog (get_ml_prog_state ())
|> addPrettyPrintersLib.pps_of_global_tys;
val _ = ml_prog_update (open_module "PrettyPrinter")
val _ = (use_full_type_names := false);
val _ = register_type ``: pp_data``;
val _ = register_type ``: default_type``;
fun tr name def = (
next_ml_names := [name];
translate def
)
val _ = ml_prog_update open_local_block;
val res = translate app_intersperse_def;
val res = translate app_list_wrap_def;
val res = translate pp_paren_contents_def;
val _ = translate escape_str_app_list_def;
Triviality escape_str_app_list_side:
!i s. escape_str_app_list_side i s <=> i <= strlen s
Proof
recInduct escape_str_app_list_ind
\\ rw []
\\ simp [Once (theorem "escape_str_app_list_side_def")]
\\ Cases_on `str_findi (\c. IS_SOME (char_escape_seq c)) i s`
\\ fs []
\\ imp_res_tac mlstringTheory.str_findi_range
\\ simp []
QED
val res = update_precondition escape_str_app_list_side;
val _ = ml_prog_update open_local_in_block;
val res = tr "toAppList" pp_contents_def;
val res = tr "no_parens" pp_no_parens_def;
val res = tr "token" pp_token_def;
val res = tr "tuple" pp_paren_tuple_def;
val res = tr "spaced_block" pp_spaced_block_def;
val res = tr "app_block" pp_app_block_def;
val res = tr "val_eq" pp_val_eq_def;
val res = tr "val_eq" pp_val_eq_def;
val res = tr "val_hidden_type" pp_val_hidden_type_def;
val res = tr "failure_message" pp_failure_message_def;
val res = tr "unprintable" pp_unprintable_def;
val res = translate pp_list_def;
val res = translate pp_bool_def;
val res = translate pp_char_def;
val res = translate pp_string_def;
val res = translate pp_app_list_def;
val res = translate pp_pp_data_def;
val res = translate pp_default_type_def;
val _ = ml_prog_update close_local_blocks;
val _ = ml_prog_update (close_module NONE);
(* pretty-printers for global (builtin) types, at global scope *)
val res = translate pp_exn_def;
val res = translate pp_unit_def;
val res = translate pp_vector_def;
(* add global names for some printers, esp. those used in pp_pp_data *)
Definition rename_pp_list_def:
rename_pp_list = pp_list
End
val res = tr "pp_list" rename_pp_list_def;
Definition rename_pp_bool_def:
rename_pp_bool = pp_bool
End
val res = tr "pp_bool" rename_pp_bool_def;
Definition rename_pp_char_def:
rename_pp_char = pp_char
End
val res = tr "pp_char" rename_pp_char_def;
Definition rename_pp_string_def:
rename_pp_string = pp_string
End
val res = tr "pp_string" rename_pp_string_def;
Definition rename_pp_app_list_def:
rename_pp_app_list = pp_app_list
End
val res = tr "pp_app_list" rename_pp_app_list_def;
(* useless pretty-printers for impure types.
should be replaced later in the basis *)
val res = translate pp_ref_def;
val res = translate pp_array_def;
val res = translate pp_word8array_def;
(* candle needs constants in the basis to be defined as literals, no funcalls *)
val res = translate (REWRITE_RULE [pp_token_def] pp_fun_def);
(* pretty printers for numeric types *)
val res = translate pp_int_def;
val res = translate pp_word8_def;
val res = translate pp_word64_def;
(* setup pretty-printers for previously existing global types *)
val _ = ml_prog_update (addPrettyPrintersLib.add_pps previous_prog_pps)
val _ = export_theory ()