forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
diffProgScript.sml
208 lines (181 loc) · 7.11 KB
/
diffProgScript.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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
(*
diff example: find a patch representing the difference between two files.
*)
open preamble basis
charsetTheory lcsTheory diffTheory
val _ = temp_delsimps ["NORMEQ_CONV"]
val _ = new_theory "diffProg";
val _ = translation_extends"basisProg";
fun def_of_const tm = let
val res = dest_thy_const tm handle HOL_ERR _ =>
failwith ("Unable to translate: " ^ term_to_string tm)
val name = (#Name res)
fun def_from_thy thy name =
DB.fetch thy (name ^ "_def") handle HOL_ERR _ =>
DB.fetch thy (name ^ "_DEF") handle HOL_ERR _ =>
DB.fetch thy (name ^ "_thm") handle HOL_ERR _ =>
DB.fetch thy name
val def = def_from_thy (#Thy res) name handle HOL_ERR _ =>
failwith ("Unable to find definition of " ^ name)
in def end
val _ = find_def_for_const := def_of_const;
val _ = translate dynamic_lcs_def
(*val _ = translate (optimised_lcs_def |> REWRITE_RULE [GSYM mllistTheory.drop_def]);*)
val dynamic_lcs_row_side_def = Q.prove(
`∀h l previous_col previous_row diagonal.
dynamic_lcs_row_side h l previous_col previous_row diagonal ⇔
(LENGTH l <= LENGTH previous_row)`,
Induct_on `l`
>> rw[Once(fetch "-" "dynamic_lcs_row_side_def")]
>> Cases_on `diagonal`
>> Cases_on `previous_row`
>> fs[] >> metis_tac[]) |> update_precondition;
val dynamic_lcs_rows_side_def = Q.prove(
`∀l r previous_row.
dynamic_lcs_rows_side l r previous_row ⇔
(l = [] \/ LENGTH r <= LENGTH previous_row)`,
Induct_on `l`
>> rw[Once(fetch "-" "dynamic_lcs_rows_side_def"),dynamic_lcs_row_side_def,dynamic_lcs_length])
|> update_precondition;
val dynamic_lcs_side_def = Q.prove(
`∀l r. dynamic_lcs_side l r ⇔ T`,
rw[fetch "-" "dynamic_lcs_side_def",dynamic_lcs_rows_side_def,LENGTH_REPLICATE])
|> update_precondition;
val _ = translate(diff_alg2_def |> REWRITE_RULE [GSYM mllistTheory.drop_def]);
val longest_common_suffix_length_side = Q.prove(
`!l l' n. longest_common_suffix_length_side l l' n = (LENGTH l = LENGTH l')`,
ho_match_mp_tac (fetch "lcs" "longest_common_suffix_length_ind")
>> rpt strip_tac
>> rw[Once(fetch "-" "longest_common_suffix_length_side_def")]
>> rw[EQ_IMP_THM]
>> Cases_on `f = f'` >> fs[]
>> fs[EQ_IMP_THM]
>> fs[ADD1]) |> update_precondition
val diff_alg2_side_def = Q.prove(`
!l r. diff_alg2_side l r ⇔ T`,
rw[fetch "-" "diff_alg2_side_def"]
>> rw[longest_common_suffix_length_side]
>> fs[mllistTheory.drop_def]) |> update_precondition;
val notfound_string_def = Define`
notfound_string f = concat[strlit"cake_diff: ";f;strlit": No such file or directory\n"]`;
val r = translate notfound_string_def;
val usage_string_def = Define`
usage_string = strlit"Usage: diff <file> <file>\n"`;
val r = translate usage_string_def;
val _ = (append_prog o process_topdecs) `
fun diff' fname1 fname2 =
case TextIO.inputLinesFrom fname1 of
None => TextIO.output TextIO.stdErr (notfound_string fname1)
| Some lines1 =>
case TextIO.inputLinesFrom fname2 of
None => TextIO.output TextIO.stdErr (notfound_string fname2)
| Some lines2 => TextIO.print_list (diff_alg2 lines1 lines2)`
Theorem diff'_spec:
FILENAME f1 fv1 ∧ FILENAME f2 fv2 /\
hasFreeFD fs
⇒
app (p:'ffi ffi_proj) ^(fetch_v"diff'"(get_ml_prog_state()))
[fv1; fv2]
(STDIO fs)
(POSTv uv.
&UNIT_TYPE () uv *
STDIO (
if inFS_fname fs f1 then
if inFS_fname fs f2 then
add_stdout fs (
concat ((diff_alg2 (all_lines fs f1)
(all_lines fs f2))))
else add_stderr fs (notfound_string f2)
else add_stderr fs (notfound_string f1)))
Proof
rpt strip_tac
\\ xcf"diff'"(get_ml_prog_state())
\\ xlet_auto_spec(SOME inputLinesFrom_spec)
>- xsimpl
\\ reverse(Cases_on `inFS_fname fs f1`) \\ fs[OPTION_TYPE_def]
\\ xmatch
>- (xlet_auto >- xsimpl
\\ xapp_spec output_stderr_spec \\ xsimpl)
\\ xlet_auto_spec(SOME inputLinesFrom_spec)
>- xsimpl
\\ reverse(Cases_on `inFS_fname fs f2`) \\ fs[OPTION_TYPE_def]
\\ xmatch
>- (xlet_auto >- xsimpl
\\ xapp_spec output_stderr_spec \\ xsimpl)
\\ xlet_auto >- xsimpl
\\ xapp \\ rw[]
QED
val _ = (append_prog o process_topdecs) `
fun diff u =
case CommandLine.arguments () of
(f1::f2::[]) => diff' f1 f2
| _ => TextIO.output TextIO.stdErr usage_string`;
val diff_sem_def = Define`
diff_sem cl fs =
if (LENGTH cl = 3) then
if inFS_fname fs (EL 1 cl) then
if inFS_fname fs (EL 2 cl) then
add_stdout fs (
concat
(diff_alg2
(all_lines fs (EL 1 cl))
(all_lines fs (EL 2 cl))))
else add_stderr fs (notfound_string (EL 2 cl))
else add_stderr fs (notfound_string (EL 1 cl))
else add_stderr fs usage_string`;
Theorem diff_spec:
hasFreeFD fs
⇒
app (p:'ffi ffi_proj) ^(fetch_v"diff"(get_ml_prog_state()))
[Conv NONE []]
(STDIO fs * COMMANDLINE cl)
(POSTv uv. &UNIT_TYPE () uv *
STDIO (diff_sem cl fs) * (COMMANDLINE cl))
Proof
once_rewrite_tac[diff_sem_def]
\\ strip_tac \\ xcf "diff" (get_ml_prog_state())
\\ xlet_auto >- (xcon \\ xsimpl)
\\ reverse(Cases_on`wfcl cl`) >- (fs[COMMANDLINE_def] \\ xpull)
\\ xlet_auto >- xsimpl
\\ Cases_on `cl` \\ fs[wfcl_def]
\\ Cases_on `t` \\ fs[ml_translatorTheory.LIST_TYPE_def]
>- (xmatch \\ xapp_spec output_stderr_spec \\ xsimpl \\ CONV_TAC SWAP_EXISTS_CONV
\\ qexists_tac `usage_string` \\ simp [theorem "usage_string_v_thm"]
\\ CONV_TAC SWAP_EXISTS_CONV \\ qexists_tac `fs` \\ xsimpl)
\\ Cases_on `t'` \\ fs[ml_translatorTheory.LIST_TYPE_def]
>- (xmatch \\ xapp_spec output_stderr_spec \\ xsimpl \\ CONV_TAC SWAP_EXISTS_CONV
\\ qexists_tac `usage_string` \\ simp [theorem "usage_string_v_thm"]
\\ CONV_TAC SWAP_EXISTS_CONV \\ qexists_tac `fs` \\ xsimpl)
\\ xmatch
\\ reverse(Cases_on `t`) \\ fs[ml_translatorTheory.LIST_TYPE_def]
\\ PURE_REWRITE_TAC [GSYM CONJ_ASSOC] \\ (reverse strip_tac >- (EVAL_TAC \\ rw[]))
>- (xapp_spec output_stderr_spec \\ xsimpl \\ CONV_TAC SWAP_EXISTS_CONV
\\ qexists_tac `usage_string` \\ simp [theorem "usage_string_v_thm"]
\\ CONV_TAC SWAP_EXISTS_CONV \\ qexists_tac `fs` \\ xsimpl)
\\ xapp \\ CONV_TAC SWAP_EXISTS_CONV \\ qexists_tac `fs`
\\ CONV_TAC SWAP_EXISTS_CONV \\ qexists_tac `h''`
\\ CONV_TAC SWAP_EXISTS_CONV \\ qexists_tac `h'`
\\ xsimpl \\ fs[FILENAME_def]
\\ fs[validArg_def,EVERY_MEM]
QED
val st = get_ml_prog_state();
Theorem diff_whole_prog_spec:
hasFreeFD fs ⇒
whole_prog_spec ^(fetch_v"diff"st) cl fs NONE ((=) (diff_sem cl fs))
Proof
rw[whole_prog_spec_def]
\\ qexists_tac`diff_sem cl fs`
\\ reverse conj_tac
>- ( rw[diff_sem_def,GSYM add_stdo_with_numchars,with_same_numchars] )
\\ simp [SEP_CLAUSES]
\\ match_mp_tac (MP_CANON (DISCH_ALL (MATCH_MP app_wgframe (UNDISCH diff_spec))))
\\ xsimpl
QED
val name = "diff"
val (sem_thm,prog_tm) = whole_prog_thm st name (UNDISCH diff_whole_prog_spec)
val diff_prog_def = Define`diff_prog = ^prog_tm`;
val diff_semantics = save_thm("diff_semantics",
sem_thm |> REWRITE_RULE[GSYM diff_prog_def]
|> DISCH_ALL
|> SIMP_RULE(srw_ss())[GSYM CONJ_ASSOC,AND_IMP_INTRO]);
val _ = export_theory ();