129 free_vars_of _ = raise malformed; |
129 free_vars_of _ = raise malformed; |
130 |
130 |
131 (* making a constructor set from a constructor term (of signature) *) |
131 (* making a constructor set from a constructor term (of signature) *) |
132 fun constr_set_string thy atyp ctstr = |
132 fun constr_set_string thy atyp ctstr = |
133 let |
133 let |
134 val trm = OldGoals.simple_read_term thy atyp ctstr; |
134 val trm = Misc_Legacy.simple_read_term thy atyp ctstr; |
135 val l = free_vars_of trm |
135 val l = free_vars_of trm |
136 in |
136 in |
137 if (check_for_constr thy atyp trm) then |
137 if (check_for_constr thy atyp trm) then |
138 (if (l=[]) then ("{" ^ ctstr ^ "}") |
138 (if (l=[]) then ("{" ^ ctstr ^ "}") |
139 else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})") |
139 else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})") |
146 fun constructor_head thy atypstr s = |
146 fun constructor_head thy atypstr s = |
147 let |
147 let |
148 fun hd_of (Const(a,_)) = a | |
148 fun hd_of (Const(a,_)) = a | |
149 hd_of (t $ _) = hd_of t | |
149 hd_of (t $ _) = hd_of t | |
150 hd_of _ = raise malformed; |
150 hd_of _ = raise malformed; |
151 val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s; |
151 val trm = Misc_Legacy.simple_read_term thy (Syntax.read_typ_global thy atypstr) s; |
152 in |
152 in |
153 hd_of trm handle malformed => |
153 hd_of trm handle malformed => |
154 error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s) |
154 error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s) |
155 end; |
155 end; |
156 fun constructor_head_list _ _ [] = [] | |
156 fun constructor_head_list _ _ [] = [] | |
175 (* extends a (action string,condition,assignlist) tupel by a |
175 (* extends a (action string,condition,assignlist) tupel by a |
176 (action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list |
176 (action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list |
177 (where bool indicates whether there is a precondition *) |
177 (where bool indicates whether there is a precondition *) |
178 fun extend thy atyp statetupel (actstr,r,[]) = |
178 fun extend thy atyp statetupel (actstr,r,[]) = |
179 let |
179 let |
180 val trm = OldGoals.simple_read_term thy atyp actstr; |
180 val trm = Misc_Legacy.simple_read_term thy atyp actstr; |
181 val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r; |
181 val rtrm = Misc_Legacy.simple_read_term thy (Type("bool",[])) r; |
182 val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true |
182 val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true |
183 in |
183 in |
184 if (check_for_constr thy atyp trm) |
184 if (check_for_constr thy atyp trm) |
185 then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag) |
185 then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag) |
186 else |
186 else |
189 extend thy atyp statetupel (actstr,r,(a,b)::c) = |
189 extend thy atyp statetupel (actstr,r,(a,b)::c) = |
190 let |
190 let |
191 fun pseudo_poststring [] = "" | |
191 fun pseudo_poststring [] = "" | |
192 pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" | |
192 pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" | |
193 pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); |
193 pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); |
194 val trm = OldGoals.simple_read_term thy atyp actstr; |
194 val trm = Misc_Legacy.simple_read_term thy atyp actstr; |
195 val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r; |
195 val rtrm = Misc_Legacy.simple_read_term thy (Type("bool",[])) r; |
196 val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true |
196 val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true |
197 in |
197 in |
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 *) |
364 "). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"), |
364 "). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"), |
365 (automaton_name ^ "_def", |
365 (automaton_name ^ "_def", |
366 automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^ |
366 automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^ |
367 "_initial, " ^ automaton_name ^ "_trans,{},{})") |
367 "_initial, " ^ automaton_name ^ "_trans,{},{})") |
368 ]) |
368 ]) |
369 val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[])) |
369 val chk_prime_list = (check_free_primed (Misc_Legacy.simple_read_term thy2 (Type("bool",[])) |
370 ( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string)))) |
370 ( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string)))) |
371 in |
371 in |
372 ( |
372 ( |
373 if (chk_prime_list = []) then thy2 |
373 if (chk_prime_list = []) then thy2 |
374 else ( |
374 else ( |