198 if (check_for_constr thy atyp trm) then |
198 if (check_for_constr thy atyp trm) then |
199 (if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false) |
199 (if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false) |
200 (* the case with transrel *) |
200 (* the case with transrel *) |
201 else |
201 else |
202 (trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)), |
202 (trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)), |
203 "(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag)) |
203 "(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag)) |
204 else |
204 else |
205 error("transition " ^ actstr ^ " is not a pure constructor term") |
205 error("transition " ^ actstr ^ " is not a pure constructor term") |
206 end; |
206 end; |
207 (* used by make_alt_string *) |
207 (* used by make_alt_string *) |
208 fun extended_list _ _ _ [] = [] | |
208 fun extended_list _ _ _ [] = [] | |
209 extended_list thy atyp statetupel (a::r) = |
209 extended_list thy atyp statetupel (a::r) = |
210 (extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r); |
210 (extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r); |
211 |
211 |
212 (* used by write_alts *) |
212 (* used by write_alts *) |
213 fun write_alt thy (chead,tr) inp out int [] = |
213 fun write_alt thy (chead,tr) inp out int [] = |
214 if (chead mem inp) then |
214 if (chead mem inp) then |
215 ( |
215 ( |
228 in |
228 in |
229 if (chead=(hd_of a)) then |
229 if (chead=(hd_of a)) then |
230 (if ((chead mem inp) andalso e) then ( |
230 (if ((chead mem inp) andalso e) then ( |
231 error("Input action " ^ b ^ " has a precondition") |
231 error("Input action " ^ b ^ " has a precondition") |
232 ) else (if (chead mem (inp@out@int)) then |
232 ) else (if (chead mem (inp@out@int)) then |
233 (if (occurs_again chead r) then ( |
233 (if (occurs_again chead r) then ( |
234 error("Two specifications for action: " ^ b) |
234 error("Two specifications for action: " ^ b) |
235 ) else (b ^ " => " ^ c,b ^ " => " ^ d)) |
235 ) else (b ^ " => " ^ c,b ^ " => " ^ d)) |
236 else ( |
236 else ( |
237 error("Action " ^ b ^ " is not in automaton signature") |
237 error("Action " ^ b ^ " is not in automaton signature") |
238 ))) else (write_alt thy (chead,ctrm) inp out int r) |
238 ))) else (write_alt thy (chead,ctrm) inp out int r) |
239 handle malformed => |
239 handle malformed => |
240 error ("malformed action term: " ^ (string_of_term thy a)) |
240 error ("malformed action term: " ^ (string_of_term thy a)) |
241 end; |
241 end; |
342 val inp_head_list = constructor_head_list thy action_type inp; |
342 val inp_head_list = constructor_head_list thy action_type inp; |
343 val out_head_list = constructor_head_list thy action_type out; |
343 val out_head_list = constructor_head_list thy action_type out; |
344 val int_head_list = constructor_head_list thy action_type int; |
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)); |
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 |
346 val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list |
347 atyp statetupel trans; |
347 atyp statetupel trans; |
348 val thy2 = (thy |
348 val thy2 = (thy |
349 |> Sign.add_consts |
349 |> Sign.add_consts |
350 [(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn), |
350 [(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn), |
351 (Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn), |
351 (Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn), |
352 (Binding.name (automaton_name ^ "_trans"), |
352 (Binding.name (automaton_name ^ "_trans"), |