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