author | pusch |
Wed, 17 Jul 1996 17:15:54 +0200 | |
changeset 1874 | 35f22792aade |
parent 1637 | b8a8ae2e5de1 |
child 2240 | a8c074224e11 |
permissions | -rw-r--r-- |
1274 | 1 |
(* interface.ML |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
2 |
Author: David von Oheimb |
1274 | 3 |
Created: 17-May-95 |
4 |
Updated: 24-May-95 |
|
5 |
Updated: 03-Jun-95 incremental change of ThySyn |
|
6 |
Updated: 11-Jul-95 use of ThyOps for cinfixes |
|
7 |
Updated: 21-Jul-95 gen_by-section |
|
8 |
Updated: 29-Aug-95 simultaneous domain equations |
|
9 |
Updated: 25-Aug-95 better syntax for simultaneous domain equations |
|
10 |
Copyright 1995 TU Muenchen |
|
11 |
*) |
|
12 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
13 |
structure ThySynData: THY_SYN_DATA = (* overwrites old version of ThySynData !!!!!! *) |
1274 | 14 |
|
15 |
struct |
|
16 |
||
17 |
local |
|
18 |
open ThyParse; |
|
19 |
open Domain_Library; |
|
20 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
21 |
(* --- generation of bindings for axioms and theorems in trailer of .thy.ML - *) |
1274 | 22 |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
23 |
fun gt_ax name = "get_axiom thy " ^ quote name; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
24 |
fun gen_val dname name = "val "^name^" = "^ gt_ax (dname^"_"^name)^";"; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
25 |
fun gen_vall name l = "val "^name^" = "^ mk_list l^";"; |
1274 | 26 |
val rews1 = "iso_rews @ when_rews @\n\ |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
27 |
\con_rews @ sel_rews @ dis_rews @ dists_le @ dists_eq @\n\ |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
28 |
\copy_rews"; |
1274 | 29 |
|
30 |
fun gen_domain eqname num ((dname,_), cons') = let |
|
31 |
val axioms1 = ["abs_iso", "rep_iso", "when_def"]; |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
32 |
(* con_defs , sel_defs, dis_defs *) |
1274 | 33 |
val axioms2 = ["copy_def"]; |
34 |
val theorems = |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
35 |
"iso_rews, exhaust, cases, when_rews, con_rews, sel_rews, dis_rews,\n \ |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
36 |
\dists_le, dists_eq, inverts, injects, copy_rews"; |
1274 | 37 |
in |
38 |
"structure "^dname^" = struct\n"^ |
|
39 |
cat_lines(map (gen_val dname) axioms1)^"\n"^ |
|
40 |
gen_vall"con_defs"(map(fn (con,_,_) => gt_ax(strip_esc con^"_def")) cons')^"\n"^ |
|
41 |
gen_vall"sel_defs"(flat(map (fn (_,_,args) => map (fn (_,sel,_) => |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
42 |
gt_ax(sel^"_def")) args) cons'))^"\n"^ |
1274 | 43 |
gen_vall"dis_defs"(map(fn (con,_,_) => gt_ax(dis_name_ con^"_def")) |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
44 |
cons')^"\n"^ |
1274 | 45 |
cat_lines(map (gen_val dname) axioms2)^"\n"^ |
46 |
"val ("^ theorems ^") =\n\ |
|
47 |
\Domain_Theorems.theorems thy "^eqname^";\n" ^ |
|
48 |
(if num > 1 then "val rews = " ^rews1 ^";\n" else "") |
|
49 |
end; |
|
50 |
||
51 |
fun mk_domain (eqs'') = let |
|
52 |
val dtnvs = map (type_name_vars o fst) eqs''; |
|
53 |
val dnames = map fst dtnvs; |
|
54 |
val num = length dnames; |
|
55 |
val comp_dname = implode (separate "_" dnames); |
|
56 |
val conss' = map (fn (dname,cons'') => |
|
57 |
let |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
58 |
fun sel n m = upd_second (fn None => dname^"_sel_"^(string_of_int n)^ |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
59 |
"_"^(string_of_int m) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
60 |
| Some s => s) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
61 |
fun fill_sels n con = upd_third (mapn (sel n) 1) con; |
1274 | 62 |
in mapn fill_sels 1 cons'' end) (dnames~~(map snd eqs'')); |
63 |
val eqs' = dtnvs~~conss'; |
|
64 |
||
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
65 |
(* ----- string for calling add_domain -------------------------------------- *) |
1284 | 66 |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
67 |
val thy_ext_string = let |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
68 |
fun mk_tnv (n,v) = mk_pair(quote n,mk_list(map mk_typ v)) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
69 |
and mk_typ (TFree(name,sort))= "TFree"^mk_pair(quote name, |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
70 |
mk_list(map quote sort)) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
71 |
| mk_typ (Type (name,args))= "Type" ^mk_tnv(name,args) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
72 |
| mk_typ _ = Imposs "interface:mk_typ"; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
73 |
fun mk_conslist cons' = mk_list (map |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
74 |
(fn (c,syn,ts)=>mk_triple(quote c,syn,mk_list |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
75 |
(map (fn (b,s ,tp) =>mk_triple(makestring(b:bool),quote s, |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
76 |
mk_typ tp)) ts))) cons'); |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
77 |
in "val (thy, "^comp_dname^"_equations) = thy |> Domain_Extender.add_domain \n" |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
78 |
^ mk_pair(quote comp_dname, |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
79 |
mk_list(map (fn (t,cs)=> mk_pair (mk_tnv t,mk_conslist cs)) eqs')) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
80 |
^ ";\nval thy = thy" |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
81 |
end; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
82 |
|
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
83 |
(* ----- string for calling (comp_)theorems and producing the structures ---------- *) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
84 |
|
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
85 |
val val_gen_string = let |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
86 |
fun plural s = if num > 1 then s^"s" else "["^s^"]"; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
87 |
val comp_axioms = [(* copy, *) "reach", "take_def", "finite_def" |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
88 |
(*, "bisim_def" *)]; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
89 |
val comp_theorems = "take_rews, " ^ implode (separate ", " (map plural |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
90 |
["take_lemma","finite"]))^", finite_ind, ind, coind"; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
91 |
fun eqname n = "(hd(funpow "^string_of_int n^" tl "^comp_dname^"_equations), " |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
92 |
^comp_dname^"_equations)"; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
93 |
fun collect sep name = if num = 1 then name else |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
94 |
implode (separate sep (map (fn s => s^"."^name) dnames)); |
1274 | 95 |
in |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
96 |
implode (separate "end; (* struct *)\n\n" |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
97 |
(mapn (fn n => gen_domain (eqname n) num) 0 eqs'))^(if num > 1 then |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
98 |
"end; (* struct *)\n\n\ |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
99 |
\structure "^comp_dname^" = struct\n" else "") ^ |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
100 |
(if num > 1 then gen_val comp_dname "copy_def" ^"\n" else "") ^ |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
101 |
implode ((map (fn s => gen_vall (plural s) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
102 |
(map (fn dn => gt_ax(dn ^ "_" ^ s)) dnames) ^"\n") comp_axioms)) ^ |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
103 |
gen_val comp_dname "bisim_def" ^"\n\ |
1274 | 104 |
\val ("^ comp_theorems ^") =\n\ |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
105 |
\Domain_Theorems.comp_theorems thy \ |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
106 |
\(" ^ quote comp_dname ^ ","^ comp_dname ^"_equations,\n\ |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
107 |
\ ["^collect " ," "cases" ^"],\n\ |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
108 |
\ "^collect "@" "con_rews " ^",\n\ |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
109 |
\ "^collect " @" "copy_rews" ^");\n\ |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
110 |
\val rews = "^(if num>1 then collect" @ " "rews"else rews1)^ " @ take_rews;\n\ |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
111 |
\end; (* struct *)" |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
112 |
end; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
113 |
in (thy_ext_string, val_gen_string) end; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
114 |
|
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
115 |
(* ----- strings for calling add_gen_by and producing the value binding ----------- *) |
1274 | 116 |
|
117 |
fun mk_gen_by (finite,eqs) = let |
|
118 |
val typs = map fst eqs; |
|
119 |
val cnstrss = map snd eqs; |
|
120 |
val tname = implode (separate "_" typs) in |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
121 |
("|> Domain_Extender.add_gen_by " |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
122 |
^ mk_pair(mk_pair(quote tname,makestring (finite:bool)), |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
123 |
mk_pair(mk_list(map quote typs), |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
124 |
mk_list (map (fn cns => mk_list(map quote cns)) cnstrss))), |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
125 |
"val "^tname^"_induct = " ^gt_ax (tname^"_induct")^";") end; |
1274 | 126 |
|
127 |
(* ----- parser for domain declaration equation ----------------------------------- *) |
|
128 |
||
129 |
(** |
|
130 |
val sort = name >> (fn s => [strip_quotes s]) |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
131 |
|| "{" $$-- !! (list (name >> strip_quotes) --$$ "}"); |
1274 | 132 |
val tvar = (type_var -- (optional ("::" $$-- !! sort) ["pcpo"])) >> TFree |
133 |
**) |
|
134 |
val tvar = type_var >> (fn tv => TFree(strip_quotes tv,["pcpo"])); |
|
135 |
||
136 |
val type_args = "(" $$-- !! (list1 tvar --$$ ")") |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
137 |
|| tvar >> (fn x => [x]) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
138 |
|| empty >> K []; |
1274 | 139 |
val con_typ = type_args -- ident >> (fn (x,y) => Type(y,x)); |
140 |
val typ = con_typ |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
141 |
|| tvar; |
1274 | 142 |
val domain_arg = "(" $$-- (optional ($$ "lazy" >> K true) false) |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
143 |
-- (optional ((ident >> Some) --$$ "::") None) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
144 |
-- typ --$$ ")" >> (fn ((lazy,sel),tp) => (lazy,sel,tp)) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
145 |
|| ident >> (fn x => (false,None,Type(x,[]))) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
146 |
|| tvar >> (fn x => (false,None,x)); |
1274 | 147 |
val domain_cons = (name >> strip_quotes) -- !! (repeat domain_arg) |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
148 |
-- ThyOps.opt_cmixfix |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
149 |
>> (fn ((con,args),syn) => (con,syn,args)); |
1274 | 150 |
in |
151 |
val domain_decl = (enum1 "," (con_typ --$$ "=" -- !! |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
152 |
(enum1 "|" domain_cons))) >> mk_domain; |
1274 | 153 |
val gen_by_decl = (optional ($$ "finite" >> K true) false) -- |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
154 |
(enum1 "," (ident --$$ "by" -- !! |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
155 |
(enum1 "|" (name >> strip_quotes)))) >> mk_gen_by; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
156 |
end; (* local *) |
1274 | 157 |
|
158 |
val user_keywords = "lazy"::"by"::"finite":: |
|
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
159 |
(**)filter_out (fn s=>s="lazy" orelse s="by" orelse s="finite")(**) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
160 |
ThySynData.user_keywords; |
1274 | 161 |
val user_sections = ("domain", domain_decl)::("generated", gen_by_decl):: |
1637
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
162 |
(**)filter_out (fn (s,_)=>s="domain" orelse s="generated")(**) |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
163 |
ThySynData.user_sections; |
b8a8ae2e5de1
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
oheimb
parents:
1461
diff
changeset
|
164 |
end; (* struct *) |
1274 | 165 |
|
166 |
structure ThySyn = ThySynFun(ThySynData); (* overwrites old version of ThySyn!!!!!! *) |