author | blanchet |
Mon, 06 Jun 2011 20:56:06 +0200 | |
changeset 43212 | 050a03afe024 |
parent 43211 | 77c432fe28ff |
child 43224 | 97906dfd39b7 |
permissions | -rw-r--r-- |
39958 | 1 |
(* Title: HOL/Tools/Metis/metis_translate.ML |
38027 | 2 |
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
3 |
Author: Kong W. Susanto, Cambridge University Computer Laboratory |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
4 |
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory |
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents:
36378
diff
changeset
|
5 |
Author: Jasmin Blanchette, TU Muenchen |
15347 | 6 |
|
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39355
diff
changeset
|
7 |
Translation of HOL to FOL for Metis. |
15347 | 8 |
*) |
9 |
||
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39355
diff
changeset
|
10 |
signature METIS_TRANSLATE = |
24310 | 11 |
sig |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset
|
12 |
type type_literal = ATP_Translate.type_literal |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
13 |
|
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset
|
14 |
datatype isa_thm = |
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset
|
15 |
Isa_Reflexive_or_Trivial | |
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset
|
16 |
Isa_Raw of thm |
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset
|
17 |
|
43094 | 18 |
val metis_equal : string |
19 |
val metis_predicator : string |
|
20 |
val metis_app_op : string |
|
43106 | 21 |
val metis_type_tag : string |
42098
f978caf60bbe
more robust handling of variables in new Skolemizer
blanchet
parents:
41491
diff
changeset
|
22 |
val metis_generated_var_prefix : string |
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
23 |
val metis_name_table : ((string * int) * (string * bool)) list |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
24 |
val reveal_old_skolem_terms : (string * term) list -> term -> term |
40157 | 25 |
val prepare_metis_problem : |
43212 | 26 |
Proof.context -> string -> thm list -> thm list |
27 |
-> int Symtab.table * (Metis_Thm.thm * isa_thm) list * (string * term) list |
|
24310 | 28 |
end |
15347 | 29 |
|
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39355
diff
changeset
|
30 |
structure Metis_Translate : METIS_TRANSLATE = |
15347 | 31 |
struct |
32 |
||
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset
|
33 |
open ATP_Problem |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset
|
34 |
open ATP_Translate |
15347 | 35 |
|
43094 | 36 |
val metis_equal = "=" |
37 |
val metis_predicator = "{}" |
|
38 |
val metis_app_op = "." |
|
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
39 |
val metis_type_tag = ":" |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset
|
40 |
val metis_generated_var_prefix = "_" |
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset
|
41 |
|
43094 | 42 |
val metis_name_table = |
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
43 |
[((tptp_equal, 2), (metis_equal, false)), |
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
44 |
((tptp_old_equal, 2), (metis_equal, false)), |
43174 | 45 |
((prefixed_predicator_name, 1), (metis_predicator, false)), |
43130
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43129
diff
changeset
|
46 |
((prefixed_app_op_name, 2), (metis_app_op, false)), |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43129
diff
changeset
|
47 |
((prefixed_type_tag_name, 2), (metis_type_tag, true))] |
43094 | 48 |
|
39896
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39890
diff
changeset
|
49 |
fun old_skolem_const_name i j num_T_args = |
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39890
diff
changeset
|
50 |
old_skolem_const_prefix ^ Long_Name.separator ^ |
41491 | 51 |
(space_implode Long_Name.separator (map string_of_int [i, j, num_T_args])) |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
52 |
|
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
53 |
fun conceal_old_skolem_terms i old_skolems t = |
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39946
diff
changeset
|
54 |
if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
55 |
let |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
56 |
fun aux old_skolems |
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39946
diff
changeset
|
57 |
(t as (Const (@{const_name Meson.skolem}, Type (_, [_, T])) $ _)) = |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
58 |
let |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
59 |
val (old_skolems, s) = |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
60 |
if i = ~1 then |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
61 |
(old_skolems, @{const_name undefined}) |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
62 |
else case AList.find (op aconv) old_skolems t of |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
63 |
s :: _ => (old_skolems, s) |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
64 |
| [] => |
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
65 |
let |
39896
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39890
diff
changeset
|
66 |
val s = old_skolem_const_name i (length old_skolems) |
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39890
diff
changeset
|
67 |
(length (Term.add_tvarsT T [])) |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
68 |
in ((s, t) :: old_skolems, s) end |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
69 |
in (old_skolems, Const (s, T)) end |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
70 |
| aux old_skolems (t1 $ t2) = |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
71 |
let |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
72 |
val (old_skolems, t1) = aux old_skolems t1 |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
73 |
val (old_skolems, t2) = aux old_skolems t2 |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
74 |
in (old_skolems, t1 $ t2) end |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
75 |
| aux old_skolems (Abs (s, T, t')) = |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
76 |
let val (old_skolems, t') = aux old_skolems t' in |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
77 |
(old_skolems, Abs (s, T, t')) |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
78 |
end |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
79 |
| aux old_skolems t = (old_skolems, t) |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
80 |
in aux old_skolems t end |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
81 |
else |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
82 |
(old_skolems, t) |
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
83 |
|
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
84 |
fun reveal_old_skolem_terms old_skolems = |
37632 | 85 |
map_aterms (fn t as Const (s, _) => |
39896
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39890
diff
changeset
|
86 |
if String.isPrefix old_skolem_const_prefix s then |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset
|
87 |
AList.lookup (op =) old_skolems s |> the |
37632 | 88 |
|> map_types Type_Infer.paramify_vars |
89 |
else |
|
90 |
t |
|
91 |
| t => t) |
|
92 |
||
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset
|
93 |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
94 |
(* ------------------------------------------------------------------------- *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
95 |
(* Logic maps manage the interface between HOL and first-order logic. *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
96 |
(* ------------------------------------------------------------------------- *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
97 |
|
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset
|
98 |
datatype isa_thm = |
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset
|
99 |
Isa_Reflexive_or_Trivial | |
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset
|
100 |
Isa_Raw of thm |
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset
|
101 |
|
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset
|
102 |
val proxy_defs = map (fst o snd o snd) proxy_table |
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset
|
103 |
val prepare_helper = |
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset
|
104 |
Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs) |
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43132
diff
changeset
|
105 |
|
43094 | 106 |
fun metis_name_from_atp s ary = |
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
107 |
AList.lookup (op =) metis_name_table (s, ary) |> the_default (s, false) |
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset
|
108 |
fun metis_term_from_atp (ATerm (s, tms)) = |
43094 | 109 |
if is_tptp_variable s then |
110 |
Metis_Term.Var s |
|
111 |
else |
|
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
112 |
let val (s, swap) = metis_name_from_atp s (length tms) in |
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
113 |
Metis_Term.Fn (s, tms |> map metis_term_from_atp |> swap ? rev) |
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
114 |
end |
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
115 |
fun metis_atom_from_atp (AAtom tm) = |
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
116 |
(case metis_term_from_atp tm of |
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
117 |
Metis_Term.Fn x => x |
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
118 |
| _ => raise Fail "non CNF -- expected function") |
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset
|
119 |
| metis_atom_from_atp _ = raise Fail "not CNF -- expected atom" |
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset
|
120 |
fun metis_literal_from_atp (AConn (ANot, [phi])) = |
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset
|
121 |
(false, metis_atom_from_atp phi) |
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset
|
122 |
| metis_literal_from_atp phi = (true, metis_atom_from_atp phi) |
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset
|
123 |
fun metis_literals_from_atp (AConn (AOr, [phi1, phi2])) = |
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset
|
124 |
uncurry (union (op =)) (pairself metis_literals_from_atp (phi1, phi2)) |
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset
|
125 |
| metis_literals_from_atp phi = [metis_literal_from_atp phi] |
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset
|
126 |
fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) = |
43173 | 127 |
let |
128 |
fun some isa = |
|
129 |
SOME (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList |
|
130 |
|> Metis_Thm.axiom, isa) |
|
131 |
in |
|
132 |
if ident = type_tag_idempotence_helper_name orelse |
|
133 |
String.isPrefix lightweight_tags_sym_formula_prefix ident then |
|
134 |
Isa_Reflexive_or_Trivial |> some |
|
135 |
else if String.isPrefix helper_prefix ident then |
|
43194 | 136 |
case (String.isSuffix typed_helper_suffix ident, |
137 |
space_explode "_" ident) of |
|
138 |
(needs_fairly_sound, _ :: const :: j :: _) => |
|
139 |
nth ((const, needs_fairly_sound) |
|
140 |
|> AList.lookup (op =) helper_table |> the) |
|
43173 | 141 |
(the (Int.fromString j) - 1) |
43194 | 142 |
|> prepare_helper |
143 |
|> Isa_Raw |> some |
|
43173 | 144 |
| _ => raise Fail ("malformed helper identifier " ^ quote ident) |
145 |
else case try (unprefix conjecture_prefix) ident of |
|
146 |
SOME s => |
|
147 |
let val j = the (Int.fromString s) in |
|
148 |
if j = length clauses then NONE |
|
149 |
else Meson.make_meta_clause (nth clauses j) |> Isa_Raw |> some |
|
150 |
end |
|
151 |
| NONE => TrueI |> Isa_Raw |> some |
|
152 |
end |
|
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset
|
153 |
| metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula" |
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset
|
154 |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
155 |
(* Function to generate metis clauses, including comb and type clauses *) |
43212 | 156 |
fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses = |
157 |
let |
|
158 |
val type_sys = type_sys_from_string type_sys |
|
159 |
val explicit_apply = NONE |
|
160 |
val clauses = |
|
161 |
conj_clauses @ fact_clauses |
|
162 |
|> (if polymorphism_of_type_sys type_sys = Polymorphic then |
|
163 |
I |
|
164 |
else |
|
165 |
map (pair 0) |
|
166 |
#> rpair ctxt |
|
167 |
#-> Monomorph.monomorph Monomorph.all_schematic_consts_of |
|
168 |
#> fst #> maps (map (zero_var_indexes o snd))) |
|
169 |
val (old_skolems, props) = |
|
170 |
fold_rev (fn clause => fn (old_skolems, props) => |
|
171 |
clause |> prop_of |> Logic.strip_imp_concl |
|
172 |
|> conceal_old_skolem_terms (length clauses) |
|
173 |
old_skolems |
|
174 |
||> (fn prop => prop :: props)) |
|
175 |
clauses ([], []) |
|
43193
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43190
diff
changeset
|
176 |
(* |
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43190
diff
changeset
|
177 |
val _ = tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props)) |
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43190
diff
changeset
|
178 |
*) |
43212 | 179 |
val (atp_problem, _, _, _, _, _, sym_tab) = |
180 |
prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply |
|
181 |
false false props @{prop False} [] |
|
43193
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43190
diff
changeset
|
182 |
(* |
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43190
diff
changeset
|
183 |
val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_strings_for_atp_problem CNF atp_problem)) |
e11bd628f1a5
improved ATP clausifier so it can deal with "x => (y <=> z)"
blanchet
parents:
43190
diff
changeset
|
184 |
*) |
43212 | 185 |
(* "rev" is for compatibility *) |
186 |
val axioms = |
|
187 |
atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd) |
|
188 |
|> rev |
|
189 |
in (sym_tab, axioms, old_skolems) end |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
190 |
|
15347 | 191 |
end; |