author | blanchet |
Thu, 17 Jan 2013 19:20:56 +0100 | |
changeset 50954 | 7bc58677860e |
parent 50907 | a86708897266 |
child 50965 | 7a7d1418301e |
permissions | -rw-r--r-- |
48234 | 1 |
(* Title: HOL/TPTP/mash_export.ML |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
Copyright 2012 |
|
4 |
||
5 |
Export Isabelle theory information for MaSh (Machine-learning for Sledgehammer). |
|
6 |
*) |
|
7 |
||
8 |
signature MASH_EXPORT = |
|
9 |
sig |
|
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset
|
10 |
type params = Sledgehammer_Provers.params |
48235 | 11 |
|
50349 | 12 |
val generate_accessibility : |
13 |
Proof.context -> theory list -> bool -> string -> unit |
|
48318 | 14 |
val generate_features : |
50349 | 15 |
Proof.context -> string -> theory list -> bool -> string -> unit |
48333 | 16 |
val generate_isar_dependencies : |
50349 | 17 |
Proof.context -> theory list -> bool -> string -> unit |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
18 |
val generate_prover_dependencies : |
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
19 |
Proof.context -> params -> int * int option -> theory list -> bool -> string |
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
20 |
-> unit |
50411 | 21 |
val generate_isar_commands : |
50954 | 22 |
Proof.context -> string -> (int * int option) * int -> theory list -> string |
23 |
-> unit |
|
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
24 |
val generate_prover_commands : |
50954 | 25 |
Proof.context -> params -> (int * int option) * int -> theory list -> string |
26 |
-> unit |
|
48379
2b5ad61e2ccc
renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents:
48378
diff
changeset
|
27 |
val generate_mepo_suggestions : |
50954 | 28 |
Proof.context -> params -> (int * int option) * int -> theory list -> int |
29 |
-> string -> unit |
|
50814 | 30 |
val generate_mesh_suggestions : int -> string -> string -> string -> unit |
48234 | 31 |
end; |
32 |
||
33 |
structure MaSh_Export : MASH_EXPORT = |
|
34 |
struct |
|
35 |
||
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50484
diff
changeset
|
36 |
open Sledgehammer_Fact |
48381 | 37 |
open Sledgehammer_MePo |
38 |
open Sledgehammer_MaSh |
|
48245 | 39 |
|
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
40 |
fun in_range (from, to) j = |
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
41 |
j >= from andalso (to = NONE orelse j <= the to) |
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
42 |
|
50349 | 43 |
fun has_thm_thy th thy = |
48316
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
44 |
Context.theory_name thy = Context.theory_name (theory_of_thm th) |
252f45c04042
drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents:
48315
diff
changeset
|
45 |
|
50349 | 46 |
fun has_thys thys th = exists (has_thm_thy th) thys |
47 |
||
48 |
fun all_facts ctxt = |
|
48531 | 49 |
let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in |
50442
4f6a4d32522c
don't blacklist "case" theorems -- this causes problems in MaSh later
blanchet
parents:
50434
diff
changeset
|
50 |
Sledgehammer_Fact.all_facts ctxt true false Symtab.empty [] [] css |
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50484
diff
changeset
|
51 |
|> sort (thm_ord o pairself snd) |
48531 | 52 |
end |
53 |
||
50349 | 54 |
fun generate_accessibility ctxt thys include_thys file_name = |
48304 | 55 |
let |
56 |
val path = file_name |> Path.explode |
|
57 |
val _ = File.write path "" |
|
58 |
fun do_fact fact prevs = |
|
59 |
let |
|
50826 | 60 |
val s = encode_str fact ^ ": " ^ encode_strs prevs ^ "\n" |
48304 | 61 |
val _ = File.append path s |
62 |
in [fact] end |
|
50611
99af6b652b3a
linearize eval driver, to work around horrible bug in previous implementation
blanchet
parents:
50582
diff
changeset
|
63 |
val facts = |
50349 | 64 |
all_facts ctxt |
65 |
|> not include_thys ? filter_out (has_thys thys o snd) |
|
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50611
diff
changeset
|
66 |
|> map (snd #> nickname_of_thm) |
50611
99af6b652b3a
linearize eval driver, to work around horrible bug in previous implementation
blanchet
parents:
50582
diff
changeset
|
67 |
in fold do_fact facts []; () end |
48304 | 68 |
|
50349 | 69 |
fun generate_features ctxt prover thys include_thys file_name = |
48304 | 70 |
let |
71 |
val path = file_name |> Path.explode |
|
72 |
val _ = File.write path "" |
|
73 |
val facts = |
|
50349 | 74 |
all_facts ctxt |
75 |
|> not include_thys ? filter_out (has_thys thys o snd) |
|
48385 | 76 |
fun do_fact ((_, stature), th) = |
48304 | 77 |
let |
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50611
diff
changeset
|
78 |
val name = nickname_of_thm th |
48318 | 79 |
val feats = |
48385 | 80 |
features_of ctxt prover (theory_of_thm th) stature [prop_of th] |
50582 | 81 |
val s = |
50826 | 82 |
encode_str name ^ ": " ^ encode_features (sort_wrt fst feats) ^ "\n" |
48304 | 83 |
in File.append path s end |
84 |
in List.app do_fact facts end |
|
85 |
||
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50624
diff
changeset
|
86 |
fun isar_or_prover_dependencies_of ctxt params_opt facts name_tabs th |
50515
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
87 |
isar_deps_opt = |
50754
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50735
diff
changeset
|
88 |
case params_opt of |
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50735
diff
changeset
|
89 |
SOME (params as {provers = prover :: _, ...}) => |
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50735
diff
changeset
|
90 |
prover_dependencies_of ctxt params prover 0 facts name_tabs th |> snd |
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50735
diff
changeset
|
91 |
| NONE => |
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50735
diff
changeset
|
92 |
case isar_deps_opt of |
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50735
diff
changeset
|
93 |
SOME deps => deps |
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50735
diff
changeset
|
94 |
| NONE => isar_dependencies_of name_tabs th |
50411 | 95 |
|
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
96 |
fun generate_isar_or_prover_dependencies ctxt params_opt range thys include_thys |
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
97 |
file_name = |
48304 | 98 |
let |
99 |
val path = file_name |> Path.explode |
|
100 |
val facts = |
|
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50484
diff
changeset
|
101 |
all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd) |
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50624
diff
changeset
|
102 |
val name_tabs = build_name_tables nickname_of_thm facts |
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
103 |
fun do_fact (j, (_, th)) = |
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
104 |
if in_range range j then |
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
105 |
let |
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50611
diff
changeset
|
106 |
val name = nickname_of_thm th |
50561 | 107 |
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) |
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
108 |
val deps = |
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50624
diff
changeset
|
109 |
isar_or_prover_dependencies_of ctxt params_opt facts name_tabs th |
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
110 |
NONE |
50826 | 111 |
in encode_str name ^ ": " ^ encode_strs deps ^ "\n" end |
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
112 |
else |
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
113 |
"" |
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
114 |
val lines = Par_List.map do_fact (tag_list 1 facts) |
50519 | 115 |
in File.write_list path lines end |
48304 | 116 |
|
50411 | 117 |
fun generate_isar_dependencies ctxt = |
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
118 |
generate_isar_or_prover_dependencies ctxt NONE (1, NONE) |
50411 | 119 |
|
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
120 |
fun generate_prover_dependencies ctxt params = |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
121 |
generate_isar_or_prover_dependencies ctxt (SOME params) |
50411 | 122 |
|
50954 | 123 |
fun is_bad_query ctxt ho_atp step j th isar_deps = |
124 |
j mod step <> 0 orelse |
|
50859
c0f38015a632
don't generate queries with empty dependency list
blanchet
parents:
50829
diff
changeset
|
125 |
Thm.legacy_get_kind th = "" orelse |
c0f38015a632
don't generate queries with empty dependency list
blanchet
parents:
50829
diff
changeset
|
126 |
null (these (trim_dependencies th isar_deps)) orelse |
50523
0799339fea0f
get rid of some junk facts in the MaSh evaluation driver
blanchet
parents:
50519
diff
changeset
|
127 |
is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th) |
50515
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
128 |
|
50954 | 129 |
fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys |
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
130 |
file_name = |
48234 | 131 |
let |
50511
8825c36cb1ce
don't query blacklisted theorems in evaluation driver
blanchet
parents:
50485
diff
changeset
|
132 |
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover |
48234 | 133 |
val path = file_name |> Path.explode |
50349 | 134 |
val facts = all_facts ctxt |
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50484
diff
changeset
|
135 |
val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd) |
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50624
diff
changeset
|
136 |
val name_tabs = build_name_tables nickname_of_thm facts |
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
137 |
fun do_fact (j, ((name, ((_, stature), th)), prevs)) = |
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
138 |
if in_range range j then |
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
139 |
let |
50561 | 140 |
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) |
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
141 |
val feats = |
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
142 |
features_of ctxt prover (theory_of_thm th) stature [prop_of th] |
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50624
diff
changeset
|
143 |
val isar_deps = isar_dependencies_of name_tabs th |
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
144 |
val deps = |
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50624
diff
changeset
|
145 |
isar_or_prover_dependencies_of ctxt params_opt facts name_tabs th |
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
146 |
(SOME isar_deps) |
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
147 |
val core = |
50826 | 148 |
encode_str name ^ ": " ^ encode_strs prevs ^ "; " ^ |
50582 | 149 |
encode_features (sort_wrt fst feats) |
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
150 |
val query = |
50954 | 151 |
if is_bad_query ctxt ho_atp step j th isar_deps then "" |
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
152 |
else "? " ^ core ^ "\n" |
50754
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50735
diff
changeset
|
153 |
val update = |
74a6adcb96ac
also generate queries for goals with too many Isar dependencies
blanchet
parents:
50735
diff
changeset
|
154 |
"! " ^ core ^ "; " ^ |
50826 | 155 |
encode_strs (these (trim_dependencies th deps)) ^ "\n" |
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
156 |
in query ^ update end |
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
157 |
else |
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
158 |
"" |
50624
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50611
diff
changeset
|
159 |
val parents = |
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50611
diff
changeset
|
160 |
map (nickname_of_thm o snd) (the_list (try List.last old_facts)) |
4d0997abce79
improved thm order hack, in case the default names are overridden
blanchet
parents:
50611
diff
changeset
|
161 |
val new_facts = new_facts |> map (`(nickname_of_thm o snd)) |
50519 | 162 |
val prevss = fst (split_last (parents :: map (single o fst) new_facts)) |
50559
89c0d2f13cca
MaSh exporter can now export subsets of the facts, as consecutive ranges
blanchet
parents:
50523
diff
changeset
|
163 |
val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ prevss)) |
50519 | 164 |
in File.write_list path lines end |
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
165 |
|
50411 | 166 |
fun generate_isar_commands ctxt prover = |
50954 | 167 |
generate_isar_or_prover_commands ctxt prover NONE |
50411 | 168 |
|
50484
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
169 |
fun generate_prover_commands ctxt (params as {provers = prover :: _, ...}) = |
8ec31bdb9d36
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents:
50442
diff
changeset
|
170 |
generate_isar_or_prover_commands ctxt prover (SOME params) |
50411 | 171 |
|
50906 | 172 |
fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...}) |
50954 | 173 |
(range, step) thys max_suggs file_name = |
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
174 |
let |
50515
c4a27ab89c9b
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
blanchet
parents:
50511
diff
changeset
|
175 |
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover |
48239
0016290f904c
generate Meng--Paulson facts for evaluation purposes
blanchet
parents:
48235
diff
changeset
|
176 |
val path = file_name |> Path.explode |
50349 | 177 |
val facts = all_facts ctxt |
50485
3c6ac2da2f45
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents:
50484
diff
changeset
|
178 |
val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd) |
50735
6b232d76cbc9
refined class handling, to prevent cycles in fact graph
blanchet
parents:
50624
diff
changeset
|
179 |
val name_tabs = build_name_tables nickname_of_thm facts |
50814 | 180 |
fun do_fact (j, ((_, th), old_facts)) = |
50906 | 181 |
if in_range range j then |
182 |
let |
|
183 |
val name = nickname_of_thm th |
|
184 |
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) |
|
185 |
val goal = goal_of_thm (Proof_Context.theory_of ctxt) th |
|
186 |
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
|
187 |
val isar_deps = isar_dependencies_of name_tabs th |
|
188 |
in |
|
50954 | 189 |
if is_bad_query ctxt ho_atp step j th isar_deps then |
50906 | 190 |
"" |
191 |
else |
|
192 |
let |
|
193 |
val suggs = |
|
194 |
old_facts |
|
195 |
|> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover |
|
196 |
max_suggs NONE hyp_ts concl_t |
|
197 |
|> map (nickname_of_thm o snd) |
|
198 |
in encode_str name ^ ": " ^ encode_strs suggs ^ "\n" end |
|
199 |
end |
|
200 |
else |
|
201 |
"" |
|
50519 | 202 |
fun accum x (yss as ys :: _) = (x :: ys) :: yss |
203 |
val old_factss = tl (fold accum new_facts [old_facts]) |
|
50814 | 204 |
val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ rev old_factss)) |
50519 | 205 |
in File.write_list path lines end |
48234 | 206 |
|
50814 | 207 |
fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name |
208 |
mesh_file_name = |
|
209 |
let |
|
210 |
val mesh_path = Path.explode mesh_file_name |
|
211 |
val _ = File.write mesh_path "" |
|
212 |
fun do_fact (mash_line, mepo_line) = |
|
213 |
let |
|
50829 | 214 |
val (name, mash_suggs) = |
50814 | 215 |
extract_suggestions mash_line |
216 |
||> (map fst #> weight_mash_facts) |
|
50829 | 217 |
val (name', mepo_suggs) = |
50814 | 218 |
extract_suggestions mepo_line |
219 |
||> (map fst #> weight_mash_facts) |
|
50829 | 220 |
val _ = if name = name' then () else error "Input files out of sync." |
50814 | 221 |
val mess = |
222 |
[(mepo_weight, (mepo_suggs, [])), |
|
223 |
(mash_weight, (mash_suggs, []))] |
|
224 |
val mesh_suggs = mesh_facts (op =) max_suggs mess |
|
50829 | 225 |
val mesh_line = encode_str name ^ ": " ^ encode_strs mesh_suggs ^ "\n" |
50814 | 226 |
in File.append mesh_path mesh_line end |
227 |
val mash_lines = Path.explode mash_file_name |> File.read_lines |
|
228 |
val mepo_lines = Path.explode mepo_file_name |> File.read_lines |
|
50907 | 229 |
in |
230 |
if length mash_lines = length mepo_lines then |
|
231 |
List.app do_fact (mash_lines ~~ mepo_lines) |
|
232 |
else |
|
233 |
warning "Skipped: MaSh file missing or out of sync with MePo file." |
|
234 |
end |
|
50814 | 235 |
|
48234 | 236 |
end; |