|
1 (* Title: ioa_package.ML |
|
2 ID: $Id$ |
|
3 *) |
|
4 |
|
5 signature IOA_PACKAGE = |
|
6 sig |
|
7 val add_ioa: string -> string -> |
|
8 (string) list -> (string) list -> (string) list -> |
|
9 (string * string) list -> string -> |
|
10 (string * string * (string * string)list) list |
|
11 -> theory -> theory |
|
12 val add_ioa_i : string -> string -> |
|
13 (string) list -> (string) list -> (string) list -> |
|
14 (string * string) list -> string -> |
|
15 (string * string * (string * string)list) list |
|
16 -> theory -> theory |
|
17 val add_composition : string -> (string)list -> theory -> theory |
|
18 val add_composition_i : string -> (string)list -> theory -> theory |
|
19 val add_hiding : string -> string -> (string)list -> theory -> theory |
|
20 val add_hiding_i : string -> string -> (string)list -> theory -> theory |
|
21 val add_restriction : string -> string -> (string)list -> theory -> theory |
|
22 val add_restriction_i : string -> string -> (string)list -> theory -> theory |
|
23 val add_rename : string -> string -> string -> theory -> theory |
|
24 val add_rename_i : string -> string -> string -> theory -> theory |
|
25 end; |
|
26 |
|
27 structure IoaPackage(* FIXME : IOA_PACKAGE *) = |
|
28 struct |
|
29 |
|
30 local |
|
31 |
|
32 exception malformed; |
|
33 |
|
34 (* for usage of hidden function no_attributes of structure Thm : *) |
|
35 fun no_attributes x = (x, []); |
|
36 |
|
37 (* stripping quotes *) |
|
38 fun strip [] = [] | |
|
39 strip ("\""::r) = strip r | |
|
40 strip (a::r) = a :: (strip r); |
|
41 fun strip_quote s = implode(strip(explode(s))); |
|
42 |
|
43 (* used by *_of_varlist *) |
|
44 fun extract_first (a,b) = strip_quote a; |
|
45 fun extract_second (a,b) = strip_quote b; |
|
46 (* following functions producing sth from a varlist *) |
|
47 fun comma_list_of_varlist [] = "" | |
|
48 comma_list_of_varlist [a] = extract_first a | |
|
49 comma_list_of_varlist (a::r) = (extract_first a) ^ "," ^ (comma_list_of_varlist r); |
|
50 fun primed_comma_list_of_varlist [] = "" | |
|
51 primed_comma_list_of_varlist [a] = (extract_first a) ^ "'" | |
|
52 primed_comma_list_of_varlist (a::r) = (extract_first a) ^ "'," ^ |
|
53 (primed_comma_list_of_varlist r); |
|
54 fun type_product_of_varlist [] = "" | |
|
55 type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" | |
|
56 type_product_of_varlist(a::r) = "(" ^ extract_second(a) ^ ")*" ^ type_product_of_varlist r; |
|
57 |
|
58 (* listing a list *) |
|
59 fun list_elements_of [] = "" | |
|
60 list_elements_of (a::r) = a ^ " " ^ (list_elements_of r); |
|
61 |
|
62 (* extracting type parameters from a type list *) |
|
63 (* fun param_tupel thy [] res = res | |
|
64 param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res | |
|
65 param_tupel thy ((TFree(a,_))::r) res = |
|
66 if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) | |
|
67 param_tupel thy (a::r) res = |
|
68 error ("one component of a statetype is a TVar: " ^ (Sign.string_of_typ (sign_of thy) a)); |
|
69 *) |
|
70 |
|
71 (* used by constr_list *) |
|
72 fun extract_constrs thy [] = [] | |
|
73 extract_constrs thy (a::r) = |
|
74 let |
|
75 fun is_prefix [] s = true |
|
76 | is_prefix (p::ps) [] = false |
|
77 | is_prefix (p::ps) (x::xs) = (p=x) andalso (is_prefix ps xs); |
|
78 fun delete_bold [] = [] |
|
79 | delete_bold (x::xs) = if (is_prefix ("\^["::"["::"1"::"m"::[]) (x::xs)) |
|
80 then (let val (_::_::_::s) = xs in delete_bold s end) |
|
81 else (if (is_prefix ("\^["::"["::"0"::"m"::[]) (x::xs)) |
|
82 then (let val (_::_::_::s) = xs in delete_bold s end) |
|
83 else (x::delete_bold xs)); |
|
84 fun delete_bold_string s = implode(delete_bold(explode s)); |
|
85 (* from a constructor term in *.induct (with quantifiers, |
|
86 "Trueprop" and ?P stripped away) delivers the head *) |
|
87 fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r | |
|
88 extract_hd (Const("Trueprop",_) $ r) = extract_hd r | |
|
89 extract_hd (Var(_,_) $ r) = extract_hd r | |
|
90 extract_hd (a $ b) = extract_hd a | |
|
91 extract_hd (Const(s,_)) = s | |
|
92 extract_hd _ = raise malformed; |
|
93 (* delivers constructor term string from a prem of *.induct *) |
|
94 fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(variant_abs(a,T,r)))| |
|
95 extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r | |
|
96 extract_constr thy (Var(_,_) $ r) = delete_bold_string(Sign.string_of_term (sign_of thy) r) | |
|
97 extract_constr _ _ = raise malformed; |
|
98 in |
|
99 (extract_hd a,extract_constr thy a) :: (extract_constrs thy r) |
|
100 end; |
|
101 |
|
102 (* delivering list of constructor terms of a datatype *) |
|
103 fun constr_list thy atyp = |
|
104 let |
|
105 fun act_name thy (Type(s,_)) = s | |
|
106 act_name _ s = |
|
107 error("malformed action type: " ^ (Sign.string_of_typ (sign_of thy) s)); |
|
108 fun afpl ("." :: a) = [] | |
|
109 afpl [] = [] | |
|
110 afpl (a::r) = a :: (afpl r); |
|
111 fun unqualify s = implode(rev(afpl(rev(explode s)))); |
|
112 val q_atypstr = act_name thy atyp; |
|
113 val uq_atypstr = unqualify q_atypstr; |
|
114 val prem = prems_of (get_thm thy (uq_atypstr ^ ".induct")); |
|
115 in |
|
116 extract_constrs thy prem |
|
117 handle malformed => |
|
118 error("malformed theorem : " ^ uq_atypstr ^ ".induct") |
|
119 end; |
|
120 |
|
121 fun check_for_constr thy atyp (a $ b) = |
|
122 let |
|
123 fun all_free (Free(_,_)) = true | |
|
124 all_free (a $ b) = if (all_free a) then (all_free b) else false | |
|
125 all_free _ = false; |
|
126 in |
|
127 if (all_free b) then (check_for_constr thy atyp a) else false |
|
128 end | |
|
129 check_for_constr thy atyp (Const(a,_)) = |
|
130 let |
|
131 val cl = constr_list thy atyp; |
|
132 fun fstmem a [] = false | |
|
133 fstmem a ((f,s)::r) = if (a=f) then true else (fstmem a r) |
|
134 in |
|
135 if (fstmem a cl) then true else false |
|
136 end | |
|
137 check_for_constr _ _ _ = false; |
|
138 |
|
139 (* delivering the free variables of a constructor term *) |
|
140 fun free_vars_of (t1 $ t2) = (free_vars_of t1) @ (free_vars_of t2) | |
|
141 free_vars_of (Const(_,_)) = [] | |
|
142 free_vars_of (Free(a,_)) = [a] | |
|
143 free_vars_of _ = raise malformed; |
|
144 |
|
145 (* making a constructor set from a constructor term (of signature) *) |
|
146 fun constr_set_string thy atyp ctstr = |
|
147 let |
|
148 val trm = #t(rep_cterm(read_cterm (sign_of thy) (ctstr,atyp))); |
|
149 val l = free_vars_of trm |
|
150 in |
|
151 if (check_for_constr thy atyp trm) then |
|
152 (if (l=[]) then ("{" ^ ctstr ^ "}") |
|
153 else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})") |
|
154 else (raise malformed) |
|
155 handle malformed => |
|
156 error("malformed action term: " ^ (Sign.string_of_term (sign_of thy) trm)) |
|
157 end; |
|
158 |
|
159 (* extracting constructor heads *) |
|
160 fun constructor_head thy atypstr s = |
|
161 let |
|
162 fun hd_of (Const(a,_)) = a | |
|
163 hd_of (t $ _) = hd_of t | |
|
164 hd_of _ = raise malformed; |
|
165 val trm = #t(rep_cterm(read_cterm (sign_of thy) (s,#T(rep_ctyp(read_ctyp (sign_of thy) atypstr))) )) |
|
166 in |
|
167 hd_of trm handle malformed => |
|
168 error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s) |
|
169 end; |
|
170 fun constructor_head_list _ _ [] = [] | |
|
171 constructor_head_list thy atypstr (a::r) = |
|
172 (constructor_head thy atypstr a)::(constructor_head_list thy atypstr r); |
|
173 |
|
174 (* producing an action set *) |
|
175 fun action_set_string thy atyp [] = "{}" | |
|
176 action_set_string thy atyp [a] = constr_set_string thy atyp (strip_quote a) | |
|
177 action_set_string thy atyp (a::r) = (constr_set_string thy atyp (strip_quote a)) ^ |
|
178 " Un " ^ (action_set_string thy atyp r); |
|
179 |
|
180 (* used by extend *) |
|
181 fun pstr s [] = "(" ^ s ^ "' = " ^ s ^ ")" | |
|
182 pstr s ((a,b)::r) = |
|
183 if (s=a) then ("(" ^ s ^ "' = (" ^ b ^ "))") else (pstr s r); |
|
184 fun poststring [] l = "" | |
|
185 poststring [(a,b)] l = pstr a l | |
|
186 poststring ((a,b)::r) l = (pstr a l) ^ " & " ^ (poststring r l); |
|
187 |
|
188 (* extends a (action string,condition,assignlist) tupel by a |
|
189 (action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list |
|
190 (where bool indicates whether there is a precondition *) |
|
191 fun extend thy atyp statetupel (actstr,r,[]) = |
|
192 let |
|
193 val trm = #t(rep_cterm(read_cterm (sign_of thy) (actstr,atyp))); |
|
194 val rtrm = #t(rep_cterm(read_cterm (sign_of thy) (r,Type("bool",[])))); |
|
195 val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true |
|
196 in |
|
197 if (check_for_constr thy atyp trm) |
|
198 then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag) |
|
199 else |
|
200 error("transition " ^ actstr ^ " is not a pure constructor term") |
|
201 end | |
|
202 extend thy atyp statetupel (actstr,r,(a,b)::c) = |
|
203 let |
|
204 fun pseudo_poststring [] = "" | |
|
205 pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" | |
|
206 pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); |
|
207 val trm = #t(rep_cterm(read_cterm (sign_of thy) (actstr,atyp))); |
|
208 val rtrm = #t(rep_cterm(read_cterm (sign_of thy) (r,Type("bool",[])))); |
|
209 val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true |
|
210 in |
|
211 if (check_for_constr thy atyp trm) then |
|
212 (if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false) |
|
213 (* the case with transrel *) |
|
214 else |
|
215 (trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)), |
|
216 "(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag)) |
|
217 else |
|
218 error("transition " ^ actstr ^ " is not a pure constructor term") |
|
219 end; |
|
220 (* used by make_alt_string *) |
|
221 fun extended_list _ _ _ [] = [] | |
|
222 extended_list thy atyp statetupel (a::r) = |
|
223 (extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r); |
|
224 |
|
225 (* used by write_alts *) |
|
226 fun write_alt thy (chead,tr) inp out int [] = |
|
227 if (chead mem inp) then |
|
228 ( |
|
229 error("Input action " ^ tr ^ " was not specified") |
|
230 ) else ( |
|
231 if (chead mem (out@int)) then |
|
232 (writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else print(""); |
|
233 (tr ^ " => False",tr ^ " => False")) | |
|
234 write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) = |
|
235 let |
|
236 fun hd_of (Const(a,_)) = a | |
|
237 hd_of (t $ _) = hd_of t | |
|
238 hd_of _ = raise malformed; |
|
239 fun occurs_again c [] = false | |
|
240 occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r); |
|
241 in |
|
242 if (chead=(hd_of a)) then |
|
243 (if ((chead mem inp) andalso e) then ( |
|
244 error("Input action " ^ b ^ " has a precondition") |
|
245 ) else (if (chead mem (inp@out@int)) then |
|
246 (if (occurs_again chead r) then ( |
|
247 error("Two specifications for action: " ^ b) |
|
248 ) else (b ^ " => " ^ c,b ^ " => " ^ d)) |
|
249 else ( |
|
250 error("Action " ^ b ^ " is not in automaton signature") |
|
251 ))) else (write_alt thy (chead,ctrm) inp out int r) |
|
252 handle malformed => |
|
253 error ("malformed action term: " ^ (Sign.string_of_term (sign_of thy) a)) |
|
254 end; |
|
255 |
|
256 (* used by make_alt_string *) |
|
257 fun write_alts thy (a,b) inp out int [] ttr = (a,b) | |
|
258 write_alts thy (a,b) inp out int [c] ttr = |
|
259 let |
|
260 val wa = write_alt thy c inp out int ttr |
|
261 in |
|
262 (a ^ (fst wa),b ^ (snd wa)) |
|
263 end | |
|
264 write_alts thy (a,b) inp out int (c::r) ttr = |
|
265 let |
|
266 val wa = write_alt thy c inp out int ttr |
|
267 in |
|
268 write_alts thy (a ^ (fst wa) ^ " | ", b ^ (snd wa) ^ " | ") inp out int r ttr |
|
269 end; |
|
270 |
|
271 fun make_alt_string thy inp out int atyp statetupel trans = |
|
272 let |
|
273 val cl = constr_list thy atyp; |
|
274 val ttr = extended_list thy atyp statetupel trans; |
|
275 in |
|
276 write_alts thy ("","") inp out int cl ttr |
|
277 end; |
|
278 |
|
279 (* used in gen_add_ioa *) |
|
280 fun check_free_primed (Free(a,_)) = |
|
281 let |
|
282 val (f::r) = rev(explode a) |
|
283 in |
|
284 if (f="'") then [a] else [] |
|
285 end | |
|
286 check_free_primed (a $ b) = ((check_free_primed a) @ (check_free_primed b)) | |
|
287 check_free_primed (Abs(_,_,t)) = check_free_primed t | |
|
288 check_free_primed _ = []; |
|
289 |
|
290 fun overlap [] _ = true | |
|
291 overlap (a::r) l = if (a mem l) then ( |
|
292 error("Two occurences of action " ^ a ^ " in automaton signature") |
|
293 ) else (overlap r l); |
|
294 |
|
295 (* delivering some types of an automaton *) |
|
296 fun aut_type_of thy aut_name = |
|
297 let |
|
298 fun left_of (( _ $ left) $ _) = left | |
|
299 left_of _ = raise malformed; |
|
300 val aut_def = concl_of(get_thm thy (aut_name ^ "_def")); |
|
301 in |
|
302 (#T(rep_cterm(cterm_of (sign_of thy) (left_of aut_def)))) |
|
303 handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def") |
|
304 end; |
|
305 |
|
306 fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp | |
|
307 act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^ |
|
308 (Sign.string_of_typ (sign_of thy) t)); |
|
309 fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp | |
|
310 st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^ |
|
311 (Sign.string_of_typ (sign_of thy) t)); |
|
312 |
|
313 fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) | |
|
314 comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) | |
|
315 comp_st_type_of _ _ = error "empty automaton list"; |
|
316 |
|
317 (* checking consistency of action types (for composition) *) |
|
318 fun check_ac thy (a::r) = |
|
319 let |
|
320 fun ch_f_a thy acttyp [] = acttyp | |
|
321 ch_f_a thy acttyp (a::r) = |
|
322 let |
|
323 val auttyp = aut_type_of thy a; |
|
324 val ac = (act_type_of thy auttyp); |
|
325 in |
|
326 if (ac=acttyp) then (ch_f_a thy acttyp r) else (error "A") |
|
327 end; |
|
328 val auttyp = aut_type_of thy a; |
|
329 val acttyp = (act_type_of thy auttyp); |
|
330 in |
|
331 ch_f_a thy acttyp r |
|
332 end | |
|
333 check_ac _ [] = error "empty automaton list"; |
|
334 |
|
335 fun clist [] = "" | |
|
336 clist [a] = a | |
|
337 clist (a::r) = a ^ " || " ^ (clist r); |
|
338 |
|
339 (* gen_add_ioa *) |
|
340 |
|
341 fun gen_add_ioa prep_term automaton_name action_type inp out int statetupel ini trans thy = |
|
342 (writeln("Constructing automaton " ^ automaton_name ^ "..."); |
|
343 let |
|
344 val state_type_string = type_product_of_varlist(statetupel); |
|
345 val styp = #T(rep_ctyp (read_ctyp (sign_of thy) state_type_string)) ; |
|
346 val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")"; |
|
347 val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")"; |
|
348 val atyp = #T(rep_ctyp (read_ctyp (sign_of thy) action_type)); |
|
349 val inp_set_string = action_set_string thy atyp inp; |
|
350 val out_set_string = action_set_string thy atyp out; |
|
351 val int_set_string = action_set_string thy atyp int; |
|
352 val inp_head_list = constructor_head_list thy action_type inp; |
|
353 val out_head_list = constructor_head_list thy action_type out; |
|
354 val int_head_list = constructor_head_list thy action_type int; |
|
355 val overlap_flag = ((overlap inp out) andalso (overlap inp int) andalso (overlap out int)); |
|
356 val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list |
|
357 atyp statetupel trans; |
|
358 val thy2 = (thy |
|
359 |> ContConsts.add_consts |
|
360 [(automaton_name ^ "_initial", "(" ^ state_type_string ^ ")set" ,NoSyn), |
|
361 (automaton_name ^ "_asig", "(" ^ action_type ^ ")signature" ,NoSyn), |
|
362 (automaton_name ^ "_trans", |
|
363 "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn), |
|
364 (automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)] |
|
365 |> (PureThy.add_defs o map no_attributes) (* old: Attributes.none *) |
|
366 [(automaton_name ^ "_initial_def", |
|
367 automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"), |
|
368 (automaton_name ^ "_asig_def", |
|
369 automaton_name ^ "_asig == (" ^ |
|
370 inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"), |
|
371 (automaton_name ^ "_trans_def", |
|
372 automaton_name ^ "_trans == {(" ^ |
|
373 state_vars_tupel ^ ", act_of_" ^ automaton_name ^ ", " ^ state_vars_primed ^ |
|
374 "). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"), |
|
375 (automaton_name ^ "_def", |
|
376 automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^ |
|
377 "_initial, " ^ automaton_name ^ "_trans,{},{})") |
|
378 ]) |
|
379 val chk_prime_list = (check_free_primed (#t(rep_cterm(read_cterm (sign_of thy2) |
|
380 ( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string),Type("bool",[])))))); |
|
381 in |
|
382 ( |
|
383 if (chk_prime_list = []) then thy2 |
|
384 else ( |
|
385 error("Precondition or assignment terms in postconditions contain following primed variables:\n" |
|
386 ^ (list_elements_of chk_prime_list))) |
|
387 ) |
|
388 end) |
|
389 |
|
390 fun gen_add_composition prep_term automaton_name aut_list thy = |
|
391 (writeln("Constructing automaton " ^ automaton_name ^ "..."); |
|
392 let |
|
393 val acttyp = check_ac thy aut_list; |
|
394 val st_typ = comp_st_type_of thy aut_list; |
|
395 val comp_list = clist aut_list; |
|
396 in |
|
397 thy |
|
398 |> ContConsts.add_consts_i |
|
399 [(automaton_name, |
|
400 Type("*", |
|
401 [Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]), |
|
402 Type("*",[Type("set",[st_typ]), |
|
403 Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), |
|
404 Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) |
|
405 ,NoSyn)] |
|
406 |> (PureThy.add_defs o map no_attributes) |
|
407 [(automaton_name ^ "_def", |
|
408 automaton_name ^ " == " ^ comp_list)] |
|
409 end) |
|
410 |
|
411 fun gen_add_restriction prep_term automaton_name aut_source actlist thy = |
|
412 (writeln("Constructing automaton " ^ automaton_name ^ "..."); |
|
413 let |
|
414 val auttyp = aut_type_of thy aut_source; |
|
415 val acttyp = act_type_of thy auttyp; |
|
416 val rest_set = action_set_string thy acttyp actlist |
|
417 in |
|
418 thy |
|
419 |> ContConsts.add_consts_i |
|
420 [(automaton_name, auttyp,NoSyn)] |
|
421 |> (PureThy.add_defs o map no_attributes) |
|
422 [(automaton_name ^ "_def", |
|
423 automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] |
|
424 end) |
|
425 fun gen_add_hiding prep_term automaton_name aut_source actlist thy = |
|
426 (writeln("Constructing automaton " ^ automaton_name ^ "..."); |
|
427 let |
|
428 val auttyp = aut_type_of thy aut_source; |
|
429 val acttyp = act_type_of thy auttyp; |
|
430 val hid_set = action_set_string thy acttyp actlist |
|
431 in |
|
432 thy |
|
433 |> ContConsts.add_consts_i |
|
434 [(automaton_name, auttyp,NoSyn)] |
|
435 |> (PureThy.add_defs o map no_attributes) |
|
436 [(automaton_name ^ "_def", |
|
437 automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] |
|
438 end) |
|
439 |
|
440 fun ren_act_type_of thy funct = |
|
441 let |
|
442 (* going into a pseudo-proof-state to enable the use of function read *) |
|
443 val _ = goal thy (funct ^ " = t"); |
|
444 fun arg_typ_of (Type("fun",[a,b])) = a | |
|
445 arg_typ_of _ = raise malformed; |
|
446 in |
|
447 arg_typ_of(#T(rep_cterm(cterm_of (sign_of thy) (read(funct))))) |
|
448 handle malformed => error ("could not extract argument type of renaming function term") |
|
449 end; |
|
450 |
|
451 fun gen_add_rename prep_term automaton_name aut_source fun_name thy = |
|
452 (writeln("Constructing automaton " ^ automaton_name ^ "..."); |
|
453 let |
|
454 val auttyp = aut_type_of thy aut_source; |
|
455 val st_typ = st_type_of thy auttyp; |
|
456 val acttyp = ren_act_type_of thy fun_name |
|
457 in |
|
458 thy |
|
459 |> ContConsts.add_consts_i |
|
460 [(automaton_name, |
|
461 Type("*", |
|
462 [Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]), |
|
463 Type("*",[Type("set",[st_typ]), |
|
464 Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), |
|
465 Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) |
|
466 ,NoSyn)] |
|
467 |> (PureThy.add_defs o map no_attributes) |
|
468 [(automaton_name ^ "_def", |
|
469 automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")] |
|
470 end) |
|
471 |
|
472 (* external interfaces *) |
|
473 |
|
474 fun read_term sg str = |
|
475 read_cterm sg (str, HOLogic.termTVar); |
|
476 |
|
477 fun cert_term sg tm = |
|
478 cterm_of sg tm handle TERM (msg, _) => error msg; |
|
479 |
|
480 in |
|
481 |
|
482 val add_ioa = gen_add_ioa read_term; |
|
483 val add_ioa_i = gen_add_ioa cert_term; |
|
484 val add_composition = gen_add_composition read_term; |
|
485 val add_composition_i = gen_add_composition cert_term; |
|
486 val add_hiding = gen_add_hiding read_term; |
|
487 val add_hiding_i = gen_add_hiding cert_term; |
|
488 val add_restriction = gen_add_restriction read_term; |
|
489 val add_restriction_i = gen_add_restriction cert_term; |
|
490 val add_rename = gen_add_rename read_term; |
|
491 val add_rename_i = gen_add_rename cert_term; |
|
492 |
|
493 end |
|
494 |
|
495 end; |