renamed ioa to automaton
authorhaftmann
Tue Jun 23 12:09:14 2009 +0200 (2009-06-23)
changeset 317745c8cfaed32e6
parent 31773 4d33c5d7575b
child 31775 2b04504fcb69
renamed ioa to automaton
src/HOLCF/IOA/meta_theory/automaton.ML
src/HOLCF/IOA/meta_theory/ioa.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/IOA/meta_theory/automaton.ML	Tue Jun 23 12:09:14 2009 +0200
     1.3 @@ -0,0 +1,536 @@
     1.4 +(*  Title:      HOLCF/IOA/meta_theory/automaton.ML
     1.5 +    Author:     Tobias Hamberger, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +signature AUTOMATON =
     1.9 +sig
    1.10 +  val add_ioa: string -> string
    1.11 +    -> (string) list -> (string) list -> (string) list
    1.12 +    -> (string * string) list -> string
    1.13 +    -> (string * string * (string * string)list) list
    1.14 +    -> theory -> theory
    1.15 +  val add_composition : string -> (string)list -> theory -> theory
    1.16 +  val add_hiding : string -> string -> (string)list -> theory -> theory
    1.17 +  val add_restriction : string -> string -> (string)list -> theory -> theory
    1.18 +  val add_rename : string -> string -> string -> theory -> theory
    1.19 +end;
    1.20 +
    1.21 +structure Automaton: AUTOMATON =
    1.22 +struct
    1.23 +
    1.24 +val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
    1.25 +val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global;
    1.26 +
    1.27 +exception malformed;
    1.28 +
    1.29 +(* stripping quotes *)
    1.30 +fun strip [] = [] |
    1.31 +strip ("\""::r) = strip r |
    1.32 +strip (a::r) = a :: (strip r);
    1.33 +fun strip_quote s = implode(strip(explode(s)));
    1.34 +
    1.35 +(* used by *_of_varlist *)
    1.36 +fun extract_first (a,b) = strip_quote a;
    1.37 +fun extract_second (a,b) = strip_quote b;
    1.38 +(* following functions producing sth from a varlist *)
    1.39 +fun comma_list_of_varlist [] = "" |
    1.40 +comma_list_of_varlist [a] = extract_first a |
    1.41 +comma_list_of_varlist (a::r) = (extract_first a) ^ "," ^ (comma_list_of_varlist r);
    1.42 +fun primed_comma_list_of_varlist [] = "" |
    1.43 +primed_comma_list_of_varlist [a] = (extract_first a) ^ "'" |
    1.44 +primed_comma_list_of_varlist (a::r) = (extract_first a) ^ "'," ^
    1.45 + (primed_comma_list_of_varlist r);
    1.46 +fun type_product_of_varlist [] = "" |
    1.47 +type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" |
    1.48 +type_product_of_varlist(a::r) = "(" ^ extract_second(a) ^ ")*" ^ type_product_of_varlist r;
    1.49 +
    1.50 +(* listing a list *)
    1.51 +fun list_elements_of [] = "" |
    1.52 +list_elements_of (a::r) = a ^ " " ^ (list_elements_of r);
    1.53 +
    1.54 +(* extracting type parameters from a type list *)
    1.55 +(* fun param_tupel thy [] res = res |
    1.56 +param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res |
    1.57 +param_tupel thy ((TFree(a,_))::r) res = 
    1.58 +if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) |
    1.59 +param_tupel thy (a::r) res =
    1.60 +error ("one component of a statetype is a TVar: " ^ (string_of_typ thy a));
    1.61 +*)
    1.62 +
    1.63 +(* used by constr_list *)
    1.64 +fun extract_constrs thy [] = [] |
    1.65 +extract_constrs thy (a::r) =
    1.66 +let
    1.67 +fun delete_bold [] = []
    1.68 +| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
    1.69 +        then (let val (_::_::_::s) = xs in delete_bold s end)
    1.70 +        else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
    1.71 +                then  (let val (_::_::_::s) = xs in delete_bold s end)
    1.72 +                else (x::delete_bold xs));
    1.73 +fun delete_bold_string s = implode(delete_bold(explode s));
    1.74 +(* from a constructor term in *.induct (with quantifiers,
    1.75 +"Trueprop" and ?P stripped away) delivers the head *)
    1.76 +fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r |
    1.77 +extract_hd (Const("Trueprop",_) $ r) = extract_hd r |
    1.78 +extract_hd (Var(_,_) $ r) = extract_hd r |
    1.79 +extract_hd (a $ b) = extract_hd a |
    1.80 +extract_hd (Const(s,_)) = s |
    1.81 +extract_hd _ = raise malformed;
    1.82 +(* delivers constructor term string from a prem of *.induct *)
    1.83 +fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))|
    1.84 +extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r |
    1.85 +extract_constr thy (Var(_,_) $ r) =  delete_bold_string(string_of_term thy r) |
    1.86 +extract_constr _ _ = raise malformed;
    1.87 +in
    1.88 +(extract_hd a,extract_constr thy a) :: (extract_constrs thy r)
    1.89 +end;
    1.90 +
    1.91 +(* delivering list of constructor terms of a datatype *)
    1.92 +fun constr_list thy atyp =
    1.93 +let
    1.94 +fun act_name thy (Type(s,_)) = s |
    1.95 +act_name _ s = 
    1.96 +error("malformed action type: " ^ (string_of_typ thy s));
    1.97 +fun afpl ("." :: a) = [] |
    1.98 +afpl [] = [] |
    1.99 +afpl (a::r) = a :: (afpl r);
   1.100 +fun unqualify s = implode(rev(afpl(rev(explode s))));
   1.101 +val q_atypstr = act_name thy atyp;
   1.102 +val uq_atypstr = unqualify q_atypstr;
   1.103 +val prem = prems_of (PureThy.get_thm thy (uq_atypstr ^ ".induct"));
   1.104 +in
   1.105 +extract_constrs thy prem
   1.106 +handle malformed =>
   1.107 +error("malformed theorem : " ^ uq_atypstr ^ ".induct")
   1.108 +end;
   1.109 +
   1.110 +fun check_for_constr thy atyp (a $ b) =
   1.111 +let
   1.112 +fun all_free (Free(_,_)) = true |
   1.113 +all_free (a $ b) = if (all_free a) then (all_free b) else false |
   1.114 +all_free _ = false; 
   1.115 +in 
   1.116 +if (all_free b) then (check_for_constr thy atyp a) else false
   1.117 +end |
   1.118 +check_for_constr thy atyp (Const(a,_)) =
   1.119 +let
   1.120 +val cl = constr_list thy atyp;
   1.121 +fun fstmem a [] = false |
   1.122 +fstmem a ((f,s)::r) = if (a=f) then true else (fstmem a r)
   1.123 +in
   1.124 +if (fstmem a cl) then true else false
   1.125 +end |
   1.126 +check_for_constr _ _ _ = false;
   1.127 +
   1.128 +(* delivering the free variables of a constructor term *)
   1.129 +fun free_vars_of (t1 $ t2) = (free_vars_of t1) @ (free_vars_of t2) |
   1.130 +free_vars_of (Const(_,_)) = [] |
   1.131 +free_vars_of (Free(a,_)) = [a] |
   1.132 +free_vars_of _ = raise malformed;
   1.133 +
   1.134 +(* making a constructor set from a constructor term (of signature) *)
   1.135 +fun constr_set_string thy atyp ctstr =
   1.136 +let
   1.137 +val trm = OldGoals.simple_read_term thy atyp ctstr;
   1.138 +val l = free_vars_of trm
   1.139 +in
   1.140 +if (check_for_constr thy atyp trm) then
   1.141 +(if (l=[]) then ("{" ^ ctstr ^ "}")
   1.142 +else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})")
   1.143 +else (raise malformed) 
   1.144 +handle malformed => 
   1.145 +error("malformed action term: " ^ (string_of_term thy trm))
   1.146 +end;
   1.147 +
   1.148 +(* extracting constructor heads *)
   1.149 +fun constructor_head thy atypstr s =
   1.150 +let
   1.151 +fun hd_of (Const(a,_)) = a |
   1.152 +hd_of (t $ _) = hd_of t |
   1.153 +hd_of _ = raise malformed;
   1.154 +val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
   1.155 +in
   1.156 +hd_of trm handle malformed =>
   1.157 +error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
   1.158 +end;
   1.159 +fun constructor_head_list _ _ [] = [] |
   1.160 +constructor_head_list thy atypstr (a::r) =
   1.161 + (constructor_head thy atypstr a)::(constructor_head_list thy atypstr r);
   1.162 +
   1.163 +(* producing an action set *)
   1.164 +(*FIXME*)
   1.165 +fun action_set_string thy atyp [] = "Set.empty" |
   1.166 +action_set_string thy atyp [a] = constr_set_string thy atyp (strip_quote a) |
   1.167 +action_set_string thy atyp (a::r) = (constr_set_string thy atyp (strip_quote a)) ^
   1.168 +         " Un " ^ (action_set_string thy atyp r);
   1.169 +
   1.170 +(* used by extend *)
   1.171 +fun pstr s [] = "(" ^ s ^ "' = " ^ s ^ ")" |
   1.172 +pstr s ((a,b)::r) =
   1.173 +if (s=a) then ("(" ^ s ^ "' = (" ^ b ^ "))") else (pstr s r);
   1.174 +fun poststring [] l = "" |
   1.175 +poststring [(a,b)] l = pstr a l |
   1.176 +poststring ((a,b)::r) l = (pstr a l) ^ " & " ^ (poststring r l);
   1.177 +
   1.178 +(* extends a (action string,condition,assignlist) tupel by a
   1.179 +(action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list 
   1.180 +(where bool indicates whether there is a precondition *)
   1.181 +fun extend thy atyp statetupel (actstr,r,[]) =
   1.182 +let
   1.183 +val trm = OldGoals.simple_read_term thy atyp actstr;
   1.184 +val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
   1.185 +val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
   1.186 +in
   1.187 +if (check_for_constr thy atyp trm)
   1.188 +then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag)
   1.189 +else
   1.190 +error("transition " ^ actstr ^ " is not a pure constructor term")
   1.191 +end |
   1.192 +extend thy atyp statetupel (actstr,r,(a,b)::c) =
   1.193 +let
   1.194 +fun pseudo_poststring [] = "" |
   1.195 +pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
   1.196 +pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); 
   1.197 +val trm = OldGoals.simple_read_term thy atyp actstr;
   1.198 +val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
   1.199 +val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
   1.200 +in
   1.201 +if (check_for_constr thy atyp trm) then
   1.202 +(if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false)
   1.203 +(* the case with transrel *)
   1.204 + else 
   1.205 + (trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)),
   1.206 +	"(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag))
   1.207 +else
   1.208 +error("transition " ^ actstr ^ " is not a pure constructor term")
   1.209 +end;
   1.210 +(* used by make_alt_string *) 
   1.211 +fun extended_list _ _ _ [] = [] |
   1.212 +extended_list thy atyp statetupel (a::r) =
   1.213 +	 (extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r);
   1.214 +
   1.215 +(* used by write_alts *)
   1.216 +fun write_alt thy (chead,tr) inp out int [] =
   1.217 +if (chead mem inp) then
   1.218 +(
   1.219 +error("Input action " ^ tr ^ " was not specified")
   1.220 +) else (
   1.221 +if (chead mem (out@int)) then
   1.222 +(writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else ();
   1.223 +(tr ^ " => False",tr ^ " => False")) |
   1.224 +write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) =
   1.225 +let
   1.226 +fun hd_of (Const(a,_)) = a |
   1.227 +hd_of (t $ _) = hd_of t |
   1.228 +hd_of _ = raise malformed;
   1.229 +fun occurs_again c [] = false |
   1.230 +occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r);
   1.231 +in
   1.232 +if (chead=(hd_of a)) then 
   1.233 +(if ((chead mem inp) andalso e) then (
   1.234 +error("Input action " ^ b ^ " has a precondition")
   1.235 +) else (if (chead mem (inp@out@int)) then 
   1.236 +		(if (occurs_again chead r) then (
   1.237 +error("Two specifications for action: " ^ b)
   1.238 +		) else (b ^ " => " ^ c,b ^ " => " ^ d))
   1.239 +	else (
   1.240 +error("Action " ^ b ^ " is not in automaton signature")
   1.241 +))) else (write_alt thy (chead,ctrm) inp out int r)
   1.242 +handle malformed =>
   1.243 +error ("malformed action term: " ^ (string_of_term thy a))
   1.244 +end;
   1.245 +
   1.246 +(* used by make_alt_string *)
   1.247 +fun write_alts thy (a,b) inp out int [] ttr = (a,b) |
   1.248 +write_alts thy (a,b) inp out int [c] ttr =
   1.249 +let
   1.250 +val wa = write_alt thy c inp out int ttr
   1.251 +in
   1.252 + (a ^ (fst wa),b ^ (snd wa))
   1.253 +end |
   1.254 +write_alts thy (a,b) inp out int (c::r) ttr =
   1.255 +let
   1.256 +val wa = write_alt thy c inp out int ttr
   1.257 +in
   1.258 + write_alts thy (a ^ (fst wa) ^ " | ", b ^ (snd wa) ^ " | ") inp out int r ttr
   1.259 +end;
   1.260 +
   1.261 +fun make_alt_string thy inp out int atyp statetupel trans =
   1.262 +let
   1.263 +val cl = constr_list thy atyp;
   1.264 +val ttr = extended_list thy atyp statetupel trans;
   1.265 +in
   1.266 +write_alts thy ("","") inp out int cl ttr
   1.267 +end;
   1.268 +
   1.269 +(* used in add_ioa *)
   1.270 +fun check_free_primed (Free(a,_)) = 
   1.271 +let
   1.272 +val (f::r) = rev(explode a)
   1.273 +in
   1.274 +if (f="'") then [a] else []
   1.275 +end | 
   1.276 +check_free_primed (a $ b) = ((check_free_primed a) @ (check_free_primed b)) |
   1.277 +check_free_primed (Abs(_,_,t)) = check_free_primed t |
   1.278 +check_free_primed _ = [];
   1.279 +
   1.280 +fun overlap [] _ = true |
   1.281 +overlap (a::r) l = if (a mem l) then (
   1.282 +error("Two occurences of action " ^ a ^ " in automaton signature")
   1.283 +) else (overlap r l);
   1.284 +
   1.285 +(* delivering some types of an automaton *)
   1.286 +fun aut_type_of thy aut_name =
   1.287 +let
   1.288 +fun left_of (( _ $ left) $ _) = left |
   1.289 +left_of _ = raise malformed;
   1.290 +val aut_def = concl_of (PureThy.get_thm thy (aut_name ^ "_def"));
   1.291 +in
   1.292 +(#T(rep_cterm(cterm_of thy (left_of aut_def))))
   1.293 +handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
   1.294 +end;
   1.295 +
   1.296 +fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp |
   1.297 +act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^
   1.298 +(string_of_typ thy t));
   1.299 +fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp |
   1.300 +st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^
   1.301 +(string_of_typ thy t));
   1.302 +
   1.303 +fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) |
   1.304 +comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) |
   1.305 +comp_st_type_of _ _ = error "empty automaton list";
   1.306 +
   1.307 +(* checking consistency of action types (for composition) *)
   1.308 +fun check_ac thy (a::r) =
   1.309 +let
   1.310 +fun ch_f_a thy acttyp [] = acttyp |
   1.311 +ch_f_a thy acttyp (a::r) =
   1.312 +let
   1.313 +val auttyp = aut_type_of thy a;
   1.314 +val ac = (act_type_of thy auttyp);
   1.315 +in
   1.316 +if (ac=acttyp) then (ch_f_a thy acttyp r) else (error "A")
   1.317 +end;
   1.318 +val auttyp = aut_type_of thy a;
   1.319 +val acttyp = (act_type_of thy auttyp);
   1.320 +in
   1.321 +ch_f_a thy acttyp r
   1.322 +end |
   1.323 +check_ac _ [] = error "empty automaton list";
   1.324 +
   1.325 +fun clist [] = "" |
   1.326 +clist [a] = a |
   1.327 +clist (a::r) = a ^ " || " ^ (clist r);
   1.328 +
   1.329 +val add_defs = snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes o map (apfst Binding.name));
   1.330 +
   1.331 +
   1.332 +(* add_ioa *)
   1.333 +
   1.334 +fun add_ioa automaton_name action_type inp out int statetupel ini trans thy =
   1.335 +(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   1.336 +let
   1.337 +val state_type_string = type_product_of_varlist(statetupel);
   1.338 +val styp = Syntax.read_typ_global thy state_type_string;
   1.339 +val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")";
   1.340 +val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")";
   1.341 +val atyp = Syntax.read_typ_global thy action_type;
   1.342 +val inp_set_string = action_set_string thy atyp inp;
   1.343 +val out_set_string = action_set_string thy atyp out;
   1.344 +val int_set_string = action_set_string thy atyp int;
   1.345 +val inp_head_list = constructor_head_list thy action_type inp;
   1.346 +val out_head_list = constructor_head_list thy action_type out;
   1.347 +val int_head_list = constructor_head_list thy action_type int;
   1.348 +val overlap_flag = ((overlap inp out) andalso (overlap inp int) andalso (overlap out int)); 
   1.349 +val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list 
   1.350 +							atyp statetupel trans;
   1.351 +val thy2 = (thy
   1.352 +|> Sign.add_consts
   1.353 +[(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn),
   1.354 +(Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn),
   1.355 +(Binding.name (automaton_name ^ "_trans"),
   1.356 + "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
   1.357 +(Binding.name automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
   1.358 +|> add_defs
   1.359 +[(automaton_name ^ "_initial_def",
   1.360 +automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
   1.361 +(automaton_name ^ "_asig_def",
   1.362 +automaton_name ^ "_asig == (" ^
   1.363 + inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"),
   1.364 +(automaton_name ^ "_trans_def",
   1.365 +automaton_name ^ "_trans == {(" ^
   1.366 + state_vars_tupel ^ ", act_of_" ^ automaton_name ^ ", " ^ state_vars_primed ^
   1.367 +"). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"),
   1.368 +(automaton_name ^ "_def",
   1.369 +automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
   1.370 +"_initial, " ^ automaton_name ^ "_trans,{},{})")
   1.371 +])
   1.372 +val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[]))
   1.373 +( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
   1.374 +in
   1.375 +(
   1.376 +if (chk_prime_list = []) then thy2
   1.377 +else (
   1.378 +error("Precondition or assignment terms in postconditions contain following primed variables:\n"
   1.379 + ^ (list_elements_of chk_prime_list)))
   1.380 +)
   1.381 +end)
   1.382 +
   1.383 +fun add_composition automaton_name aut_list thy =
   1.384 +(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   1.385 +let
   1.386 +val acttyp = check_ac thy aut_list; 
   1.387 +val st_typ = comp_st_type_of thy aut_list; 
   1.388 +val comp_list = clist aut_list;
   1.389 +in
   1.390 +thy
   1.391 +|> Sign.add_consts_i
   1.392 +[(Binding.name automaton_name,
   1.393 +Type("*",
   1.394 +[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
   1.395 + Type("*",[Type("set",[st_typ]),
   1.396 +  Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
   1.397 +   Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
   1.398 +,NoSyn)]
   1.399 +|> add_defs
   1.400 +[(automaton_name ^ "_def",
   1.401 +automaton_name ^ " == " ^ comp_list)]
   1.402 +end)
   1.403 +
   1.404 +fun add_restriction automaton_name aut_source actlist thy =
   1.405 +(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   1.406 +let
   1.407 +val auttyp = aut_type_of thy aut_source;
   1.408 +val acttyp = act_type_of thy auttyp; 
   1.409 +val rest_set = action_set_string thy acttyp actlist
   1.410 +in
   1.411 +thy
   1.412 +|> Sign.add_consts_i
   1.413 +[(Binding.name automaton_name, auttyp,NoSyn)]
   1.414 +|> add_defs
   1.415 +[(automaton_name ^ "_def",
   1.416 +automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] 
   1.417 +end)
   1.418 +fun add_hiding automaton_name aut_source actlist thy =
   1.419 +(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   1.420 +let
   1.421 +val auttyp = aut_type_of thy aut_source;
   1.422 +val acttyp = act_type_of thy auttyp; 
   1.423 +val hid_set = action_set_string thy acttyp actlist
   1.424 +in
   1.425 +thy
   1.426 +|> Sign.add_consts_i
   1.427 +[(Binding.name automaton_name, auttyp,NoSyn)]
   1.428 +|> add_defs
   1.429 +[(automaton_name ^ "_def",
   1.430 +automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] 
   1.431 +end)
   1.432 +
   1.433 +fun ren_act_type_of thy funct =
   1.434 +  (case Term.fastype_of (Syntax.read_term_global thy funct) of
   1.435 +    Type ("fun", [a, b]) => a
   1.436 +  | _ => error "could not extract argument type of renaming function term");
   1.437 + 
   1.438 +fun add_rename automaton_name aut_source fun_name thy =
   1.439 +(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   1.440 +let
   1.441 +val auttyp = aut_type_of thy aut_source;
   1.442 +val st_typ = st_type_of thy auttyp;
   1.443 +val acttyp = ren_act_type_of thy fun_name
   1.444 +in
   1.445 +thy
   1.446 +|> Sign.add_consts_i
   1.447 +[(Binding.name automaton_name,
   1.448 +Type("*",
   1.449 +[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
   1.450 + Type("*",[Type("set",[st_typ]),
   1.451 +  Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
   1.452 +   Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
   1.453 +,NoSyn)]
   1.454 +|> add_defs
   1.455 +[(automaton_name ^ "_def",
   1.456 +automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
   1.457 +end)
   1.458 +
   1.459 +
   1.460 +(** outer syntax **)
   1.461 +
   1.462 +(* prepare results *)
   1.463 +
   1.464 +(*encoding transition specifications with a element of ParseTrans*)
   1.465 +datatype ParseTrans = Rel of string | PP of string*(string*string)list;
   1.466 +fun mk_trans_of_rel s = Rel(s);
   1.467 +fun mk_trans_of_prepost (s,l) = PP(s,l); 
   1.468 +
   1.469 +fun trans_of (a, Rel b) = (a, b, [("", "")])
   1.470 +  | trans_of (a, PP (b, l)) = (a, b, l);
   1.471 +
   1.472 +
   1.473 +fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) =
   1.474 +  add_ioa aut action_type inp out int states initial (map trans_of trans);
   1.475 +
   1.476 +fun mk_composition_decl (aut, autlist) =
   1.477 +  add_composition aut autlist;
   1.478 +
   1.479 +fun mk_hiding_decl (aut, (actlist, source_aut)) =
   1.480 +  add_hiding aut source_aut actlist;
   1.481 +
   1.482 +fun mk_restriction_decl (aut, (source_aut, actlist)) =
   1.483 +  add_restriction aut source_aut actlist;
   1.484 +
   1.485 +fun mk_rename_decl (aut, (source_aut, rename_f)) =
   1.486 +  add_rename aut source_aut rename_f;
   1.487 +
   1.488 +
   1.489 +(* outer syntax *)
   1.490 +
   1.491 +local structure P = OuterParse and K = OuterKeyword in
   1.492 +
   1.493 +val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs",
   1.494 +  "outputs", "internals", "states", "initially", "transitions", "pre",
   1.495 +  "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
   1.496 +  "rename"];
   1.497 +
   1.498 +val actionlist = P.list1 P.term;
   1.499 +val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
   1.500 +val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
   1.501 +val internalslist = P.$$$ "internals" |-- P.!!! actionlist;
   1.502 +val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ));
   1.503 +val initial = P.$$$ "initially" |-- P.!!! P.term;
   1.504 +val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term);
   1.505 +val pre = P.$$$ "pre" |-- P.!!! P.term;
   1.506 +val post = P.$$$ "post" |-- P.!!! assign_list;
   1.507 +val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost;
   1.508 +val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost;
   1.509 +val transrel =  (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel;
   1.510 +val transition = P.term -- (transrel || pre1 || post1);
   1.511 +val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition);
   1.512 +
   1.513 +val ioa_decl =
   1.514 +  (P.name -- (P.$$$ "=" |--
   1.515 +    (P.$$$ "signature" |--
   1.516 +      P.!!! (P.$$$ "actions" |--
   1.517 +        (P.typ --
   1.518 +          (Scan.optional inputslist []) --
   1.519 +          (Scan.optional outputslist []) --
   1.520 +          (Scan.optional internalslist []) --
   1.521 +          stateslist --
   1.522 +          (Scan.optional initial "True") --
   1.523 +        translist))))) >> mk_ioa_decl ||
   1.524 +  (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name))))
   1.525 +    >> mk_composition_decl ||
   1.526 +  (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |--
   1.527 +      P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl ||
   1.528 +  (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |--
   1.529 +      P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl ||
   1.530 +  (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
   1.531 +    >> mk_rename_decl;
   1.532 +
   1.533 +val _ =
   1.534 +  OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
   1.535 +    (ioa_decl >> Toplevel.theory);
   1.536 +
   1.537 +end;
   1.538 +
   1.539 +end;
     2.1 --- a/src/HOLCF/IOA/meta_theory/ioa.ML	Tue Jun 23 12:08:35 2009 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,536 +0,0 @@
     2.4 -(*  Title:      HOLCF/IOA/meta_theory/ioa.ML
     2.5 -    Author:     Tobias Hamberger, TU Muenchen
     2.6 -*)
     2.7 -
     2.8 -signature IOA =
     2.9 -sig
    2.10 -  val add_ioa: string -> string
    2.11 -    -> (string) list -> (string) list -> (string) list
    2.12 -    -> (string * string) list -> string
    2.13 -    -> (string * string * (string * string)list) list
    2.14 -    -> theory -> theory
    2.15 -  val add_composition : string -> (string)list -> theory -> theory
    2.16 -  val add_hiding : string -> string -> (string)list -> theory -> theory
    2.17 -  val add_restriction : string -> string -> (string)list -> theory -> theory
    2.18 -  val add_rename : string -> string -> string -> theory -> theory
    2.19 -end;
    2.20 -
    2.21 -structure Ioa: IOA =
    2.22 -struct
    2.23 -
    2.24 -val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
    2.25 -val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global;
    2.26 -
    2.27 -exception malformed;
    2.28 -
    2.29 -(* stripping quotes *)
    2.30 -fun strip [] = [] |
    2.31 -strip ("\""::r) = strip r |
    2.32 -strip (a::r) = a :: (strip r);
    2.33 -fun strip_quote s = implode(strip(explode(s)));
    2.34 -
    2.35 -(* used by *_of_varlist *)
    2.36 -fun extract_first (a,b) = strip_quote a;
    2.37 -fun extract_second (a,b) = strip_quote b;
    2.38 -(* following functions producing sth from a varlist *)
    2.39 -fun comma_list_of_varlist [] = "" |
    2.40 -comma_list_of_varlist [a] = extract_first a |
    2.41 -comma_list_of_varlist (a::r) = (extract_first a) ^ "," ^ (comma_list_of_varlist r);
    2.42 -fun primed_comma_list_of_varlist [] = "" |
    2.43 -primed_comma_list_of_varlist [a] = (extract_first a) ^ "'" |
    2.44 -primed_comma_list_of_varlist (a::r) = (extract_first a) ^ "'," ^
    2.45 - (primed_comma_list_of_varlist r);
    2.46 -fun type_product_of_varlist [] = "" |
    2.47 -type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" |
    2.48 -type_product_of_varlist(a::r) = "(" ^ extract_second(a) ^ ")*" ^ type_product_of_varlist r;
    2.49 -
    2.50 -(* listing a list *)
    2.51 -fun list_elements_of [] = "" |
    2.52 -list_elements_of (a::r) = a ^ " " ^ (list_elements_of r);
    2.53 -
    2.54 -(* extracting type parameters from a type list *)
    2.55 -(* fun param_tupel thy [] res = res |
    2.56 -param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res |
    2.57 -param_tupel thy ((TFree(a,_))::r) res = 
    2.58 -if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) |
    2.59 -param_tupel thy (a::r) res =
    2.60 -error ("one component of a statetype is a TVar: " ^ (string_of_typ thy a));
    2.61 -*)
    2.62 -
    2.63 -(* used by constr_list *)
    2.64 -fun extract_constrs thy [] = [] |
    2.65 -extract_constrs thy (a::r) =
    2.66 -let
    2.67 -fun delete_bold [] = []
    2.68 -| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
    2.69 -        then (let val (_::_::_::s) = xs in delete_bold s end)
    2.70 -        else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
    2.71 -                then  (let val (_::_::_::s) = xs in delete_bold s end)
    2.72 -                else (x::delete_bold xs));
    2.73 -fun delete_bold_string s = implode(delete_bold(explode s));
    2.74 -(* from a constructor term in *.induct (with quantifiers,
    2.75 -"Trueprop" and ?P stripped away) delivers the head *)
    2.76 -fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r |
    2.77 -extract_hd (Const("Trueprop",_) $ r) = extract_hd r |
    2.78 -extract_hd (Var(_,_) $ r) = extract_hd r |
    2.79 -extract_hd (a $ b) = extract_hd a |
    2.80 -extract_hd (Const(s,_)) = s |
    2.81 -extract_hd _ = raise malformed;
    2.82 -(* delivers constructor term string from a prem of *.induct *)
    2.83 -fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))|
    2.84 -extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r |
    2.85 -extract_constr thy (Var(_,_) $ r) =  delete_bold_string(string_of_term thy r) |
    2.86 -extract_constr _ _ = raise malformed;
    2.87 -in
    2.88 -(extract_hd a,extract_constr thy a) :: (extract_constrs thy r)
    2.89 -end;
    2.90 -
    2.91 -(* delivering list of constructor terms of a datatype *)
    2.92 -fun constr_list thy atyp =
    2.93 -let
    2.94 -fun act_name thy (Type(s,_)) = s |
    2.95 -act_name _ s = 
    2.96 -error("malformed action type: " ^ (string_of_typ thy s));
    2.97 -fun afpl ("." :: a) = [] |
    2.98 -afpl [] = [] |
    2.99 -afpl (a::r) = a :: (afpl r);
   2.100 -fun unqualify s = implode(rev(afpl(rev(explode s))));
   2.101 -val q_atypstr = act_name thy atyp;
   2.102 -val uq_atypstr = unqualify q_atypstr;
   2.103 -val prem = prems_of (PureThy.get_thm thy (uq_atypstr ^ ".induct"));
   2.104 -in
   2.105 -extract_constrs thy prem
   2.106 -handle malformed =>
   2.107 -error("malformed theorem : " ^ uq_atypstr ^ ".induct")
   2.108 -end;
   2.109 -
   2.110 -fun check_for_constr thy atyp (a $ b) =
   2.111 -let
   2.112 -fun all_free (Free(_,_)) = true |
   2.113 -all_free (a $ b) = if (all_free a) then (all_free b) else false |
   2.114 -all_free _ = false; 
   2.115 -in 
   2.116 -if (all_free b) then (check_for_constr thy atyp a) else false
   2.117 -end |
   2.118 -check_for_constr thy atyp (Const(a,_)) =
   2.119 -let
   2.120 -val cl = constr_list thy atyp;
   2.121 -fun fstmem a [] = false |
   2.122 -fstmem a ((f,s)::r) = if (a=f) then true else (fstmem a r)
   2.123 -in
   2.124 -if (fstmem a cl) then true else false
   2.125 -end |
   2.126 -check_for_constr _ _ _ = false;
   2.127 -
   2.128 -(* delivering the free variables of a constructor term *)
   2.129 -fun free_vars_of (t1 $ t2) = (free_vars_of t1) @ (free_vars_of t2) |
   2.130 -free_vars_of (Const(_,_)) = [] |
   2.131 -free_vars_of (Free(a,_)) = [a] |
   2.132 -free_vars_of _ = raise malformed;
   2.133 -
   2.134 -(* making a constructor set from a constructor term (of signature) *)
   2.135 -fun constr_set_string thy atyp ctstr =
   2.136 -let
   2.137 -val trm = OldGoals.simple_read_term thy atyp ctstr;
   2.138 -val l = free_vars_of trm
   2.139 -in
   2.140 -if (check_for_constr thy atyp trm) then
   2.141 -(if (l=[]) then ("{" ^ ctstr ^ "}")
   2.142 -else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})")
   2.143 -else (raise malformed) 
   2.144 -handle malformed => 
   2.145 -error("malformed action term: " ^ (string_of_term thy trm))
   2.146 -end;
   2.147 -
   2.148 -(* extracting constructor heads *)
   2.149 -fun constructor_head thy atypstr s =
   2.150 -let
   2.151 -fun hd_of (Const(a,_)) = a |
   2.152 -hd_of (t $ _) = hd_of t |
   2.153 -hd_of _ = raise malformed;
   2.154 -val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
   2.155 -in
   2.156 -hd_of trm handle malformed =>
   2.157 -error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
   2.158 -end;
   2.159 -fun constructor_head_list _ _ [] = [] |
   2.160 -constructor_head_list thy atypstr (a::r) =
   2.161 - (constructor_head thy atypstr a)::(constructor_head_list thy atypstr r);
   2.162 -
   2.163 -(* producing an action set *)
   2.164 -(*FIXME*)
   2.165 -fun action_set_string thy atyp [] = "Set.empty" |
   2.166 -action_set_string thy atyp [a] = constr_set_string thy atyp (strip_quote a) |
   2.167 -action_set_string thy atyp (a::r) = (constr_set_string thy atyp (strip_quote a)) ^
   2.168 -         " Un " ^ (action_set_string thy atyp r);
   2.169 -
   2.170 -(* used by extend *)
   2.171 -fun pstr s [] = "(" ^ s ^ "' = " ^ s ^ ")" |
   2.172 -pstr s ((a,b)::r) =
   2.173 -if (s=a) then ("(" ^ s ^ "' = (" ^ b ^ "))") else (pstr s r);
   2.174 -fun poststring [] l = "" |
   2.175 -poststring [(a,b)] l = pstr a l |
   2.176 -poststring ((a,b)::r) l = (pstr a l) ^ " & " ^ (poststring r l);
   2.177 -
   2.178 -(* extends a (action string,condition,assignlist) tupel by a
   2.179 -(action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list 
   2.180 -(where bool indicates whether there is a precondition *)
   2.181 -fun extend thy atyp statetupel (actstr,r,[]) =
   2.182 -let
   2.183 -val trm = OldGoals.simple_read_term thy atyp actstr;
   2.184 -val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
   2.185 -val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
   2.186 -in
   2.187 -if (check_for_constr thy atyp trm)
   2.188 -then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag)
   2.189 -else
   2.190 -error("transition " ^ actstr ^ " is not a pure constructor term")
   2.191 -end |
   2.192 -extend thy atyp statetupel (actstr,r,(a,b)::c) =
   2.193 -let
   2.194 -fun pseudo_poststring [] = "" |
   2.195 -pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
   2.196 -pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); 
   2.197 -val trm = OldGoals.simple_read_term thy atyp actstr;
   2.198 -val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
   2.199 -val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
   2.200 -in
   2.201 -if (check_for_constr thy atyp trm) then
   2.202 -(if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false)
   2.203 -(* the case with transrel *)
   2.204 - else 
   2.205 - (trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)),
   2.206 -	"(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag))
   2.207 -else
   2.208 -error("transition " ^ actstr ^ " is not a pure constructor term")
   2.209 -end;
   2.210 -(* used by make_alt_string *) 
   2.211 -fun extended_list _ _ _ [] = [] |
   2.212 -extended_list thy atyp statetupel (a::r) =
   2.213 -	 (extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r);
   2.214 -
   2.215 -(* used by write_alts *)
   2.216 -fun write_alt thy (chead,tr) inp out int [] =
   2.217 -if (chead mem inp) then
   2.218 -(
   2.219 -error("Input action " ^ tr ^ " was not specified")
   2.220 -) else (
   2.221 -if (chead mem (out@int)) then
   2.222 -(writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else ();
   2.223 -(tr ^ " => False",tr ^ " => False")) |
   2.224 -write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) =
   2.225 -let
   2.226 -fun hd_of (Const(a,_)) = a |
   2.227 -hd_of (t $ _) = hd_of t |
   2.228 -hd_of _ = raise malformed;
   2.229 -fun occurs_again c [] = false |
   2.230 -occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r);
   2.231 -in
   2.232 -if (chead=(hd_of a)) then 
   2.233 -(if ((chead mem inp) andalso e) then (
   2.234 -error("Input action " ^ b ^ " has a precondition")
   2.235 -) else (if (chead mem (inp@out@int)) then 
   2.236 -		(if (occurs_again chead r) then (
   2.237 -error("Two specifications for action: " ^ b)
   2.238 -		) else (b ^ " => " ^ c,b ^ " => " ^ d))
   2.239 -	else (
   2.240 -error("Action " ^ b ^ " is not in automaton signature")
   2.241 -))) else (write_alt thy (chead,ctrm) inp out int r)
   2.242 -handle malformed =>
   2.243 -error ("malformed action term: " ^ (string_of_term thy a))
   2.244 -end;
   2.245 -
   2.246 -(* used by make_alt_string *)
   2.247 -fun write_alts thy (a,b) inp out int [] ttr = (a,b) |
   2.248 -write_alts thy (a,b) inp out int [c] ttr =
   2.249 -let
   2.250 -val wa = write_alt thy c inp out int ttr
   2.251 -in
   2.252 - (a ^ (fst wa),b ^ (snd wa))
   2.253 -end |
   2.254 -write_alts thy (a,b) inp out int (c::r) ttr =
   2.255 -let
   2.256 -val wa = write_alt thy c inp out int ttr
   2.257 -in
   2.258 - write_alts thy (a ^ (fst wa) ^ " | ", b ^ (snd wa) ^ " | ") inp out int r ttr
   2.259 -end;
   2.260 -
   2.261 -fun make_alt_string thy inp out int atyp statetupel trans =
   2.262 -let
   2.263 -val cl = constr_list thy atyp;
   2.264 -val ttr = extended_list thy atyp statetupel trans;
   2.265 -in
   2.266 -write_alts thy ("","") inp out int cl ttr
   2.267 -end;
   2.268 -
   2.269 -(* used in add_ioa *)
   2.270 -fun check_free_primed (Free(a,_)) = 
   2.271 -let
   2.272 -val (f::r) = rev(explode a)
   2.273 -in
   2.274 -if (f="'") then [a] else []
   2.275 -end | 
   2.276 -check_free_primed (a $ b) = ((check_free_primed a) @ (check_free_primed b)) |
   2.277 -check_free_primed (Abs(_,_,t)) = check_free_primed t |
   2.278 -check_free_primed _ = [];
   2.279 -
   2.280 -fun overlap [] _ = true |
   2.281 -overlap (a::r) l = if (a mem l) then (
   2.282 -error("Two occurences of action " ^ a ^ " in automaton signature")
   2.283 -) else (overlap r l);
   2.284 -
   2.285 -(* delivering some types of an automaton *)
   2.286 -fun aut_type_of thy aut_name =
   2.287 -let
   2.288 -fun left_of (( _ $ left) $ _) = left |
   2.289 -left_of _ = raise malformed;
   2.290 -val aut_def = concl_of (PureThy.get_thm thy (aut_name ^ "_def"));
   2.291 -in
   2.292 -(#T(rep_cterm(cterm_of thy (left_of aut_def))))
   2.293 -handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
   2.294 -end;
   2.295 -
   2.296 -fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp |
   2.297 -act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^
   2.298 -(string_of_typ thy t));
   2.299 -fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp |
   2.300 -st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^
   2.301 -(string_of_typ thy t));
   2.302 -
   2.303 -fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) |
   2.304 -comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) |
   2.305 -comp_st_type_of _ _ = error "empty automaton list";
   2.306 -
   2.307 -(* checking consistency of action types (for composition) *)
   2.308 -fun check_ac thy (a::r) =
   2.309 -let
   2.310 -fun ch_f_a thy acttyp [] = acttyp |
   2.311 -ch_f_a thy acttyp (a::r) =
   2.312 -let
   2.313 -val auttyp = aut_type_of thy a;
   2.314 -val ac = (act_type_of thy auttyp);
   2.315 -in
   2.316 -if (ac=acttyp) then (ch_f_a thy acttyp r) else (error "A")
   2.317 -end;
   2.318 -val auttyp = aut_type_of thy a;
   2.319 -val acttyp = (act_type_of thy auttyp);
   2.320 -in
   2.321 -ch_f_a thy acttyp r
   2.322 -end |
   2.323 -check_ac _ [] = error "empty automaton list";
   2.324 -
   2.325 -fun clist [] = "" |
   2.326 -clist [a] = a |
   2.327 -clist (a::r) = a ^ " || " ^ (clist r);
   2.328 -
   2.329 -val add_defs = snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes o map (apfst Binding.name));
   2.330 -
   2.331 -
   2.332 -(* add_ioa *)
   2.333 -
   2.334 -fun add_ioa automaton_name action_type inp out int statetupel ini trans thy =
   2.335 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   2.336 -let
   2.337 -val state_type_string = type_product_of_varlist(statetupel);
   2.338 -val styp = Syntax.read_typ_global thy state_type_string;
   2.339 -val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")";
   2.340 -val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")";
   2.341 -val atyp = Syntax.read_typ_global thy action_type;
   2.342 -val inp_set_string = action_set_string thy atyp inp;
   2.343 -val out_set_string = action_set_string thy atyp out;
   2.344 -val int_set_string = action_set_string thy atyp int;
   2.345 -val inp_head_list = constructor_head_list thy action_type inp;
   2.346 -val out_head_list = constructor_head_list thy action_type out;
   2.347 -val int_head_list = constructor_head_list thy action_type int;
   2.348 -val overlap_flag = ((overlap inp out) andalso (overlap inp int) andalso (overlap out int)); 
   2.349 -val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list 
   2.350 -							atyp statetupel trans;
   2.351 -val thy2 = (thy
   2.352 -|> Sign.add_consts
   2.353 -[(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn),
   2.354 -(Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn),
   2.355 -(Binding.name (automaton_name ^ "_trans"),
   2.356 - "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
   2.357 -(Binding.name automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
   2.358 -|> add_defs
   2.359 -[(automaton_name ^ "_initial_def",
   2.360 -automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
   2.361 -(automaton_name ^ "_asig_def",
   2.362 -automaton_name ^ "_asig == (" ^
   2.363 - inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"),
   2.364 -(automaton_name ^ "_trans_def",
   2.365 -automaton_name ^ "_trans == {(" ^
   2.366 - state_vars_tupel ^ ", act_of_" ^ automaton_name ^ ", " ^ state_vars_primed ^
   2.367 -"). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"),
   2.368 -(automaton_name ^ "_def",
   2.369 -automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
   2.370 -"_initial, " ^ automaton_name ^ "_trans,{},{})")
   2.371 -])
   2.372 -val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[]))
   2.373 -( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
   2.374 -in
   2.375 -(
   2.376 -if (chk_prime_list = []) then thy2
   2.377 -else (
   2.378 -error("Precondition or assignment terms in postconditions contain following primed variables:\n"
   2.379 - ^ (list_elements_of chk_prime_list)))
   2.380 -)
   2.381 -end)
   2.382 -
   2.383 -fun add_composition automaton_name aut_list thy =
   2.384 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   2.385 -let
   2.386 -val acttyp = check_ac thy aut_list; 
   2.387 -val st_typ = comp_st_type_of thy aut_list; 
   2.388 -val comp_list = clist aut_list;
   2.389 -in
   2.390 -thy
   2.391 -|> Sign.add_consts_i
   2.392 -[(Binding.name automaton_name,
   2.393 -Type("*",
   2.394 -[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
   2.395 - Type("*",[Type("set",[st_typ]),
   2.396 -  Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
   2.397 -   Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
   2.398 -,NoSyn)]
   2.399 -|> add_defs
   2.400 -[(automaton_name ^ "_def",
   2.401 -automaton_name ^ " == " ^ comp_list)]
   2.402 -end)
   2.403 -
   2.404 -fun add_restriction automaton_name aut_source actlist thy =
   2.405 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   2.406 -let
   2.407 -val auttyp = aut_type_of thy aut_source;
   2.408 -val acttyp = act_type_of thy auttyp; 
   2.409 -val rest_set = action_set_string thy acttyp actlist
   2.410 -in
   2.411 -thy
   2.412 -|> Sign.add_consts_i
   2.413 -[(Binding.name automaton_name, auttyp,NoSyn)]
   2.414 -|> add_defs
   2.415 -[(automaton_name ^ "_def",
   2.416 -automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] 
   2.417 -end)
   2.418 -fun add_hiding automaton_name aut_source actlist thy =
   2.419 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   2.420 -let
   2.421 -val auttyp = aut_type_of thy aut_source;
   2.422 -val acttyp = act_type_of thy auttyp; 
   2.423 -val hid_set = action_set_string thy acttyp actlist
   2.424 -in
   2.425 -thy
   2.426 -|> Sign.add_consts_i
   2.427 -[(Binding.name automaton_name, auttyp,NoSyn)]
   2.428 -|> add_defs
   2.429 -[(automaton_name ^ "_def",
   2.430 -automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] 
   2.431 -end)
   2.432 -
   2.433 -fun ren_act_type_of thy funct =
   2.434 -  (case Term.fastype_of (Syntax.read_term_global thy funct) of
   2.435 -    Type ("fun", [a, b]) => a
   2.436 -  | _ => error "could not extract argument type of renaming function term");
   2.437 - 
   2.438 -fun add_rename automaton_name aut_source fun_name thy =
   2.439 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   2.440 -let
   2.441 -val auttyp = aut_type_of thy aut_source;
   2.442 -val st_typ = st_type_of thy auttyp;
   2.443 -val acttyp = ren_act_type_of thy fun_name
   2.444 -in
   2.445 -thy
   2.446 -|> Sign.add_consts_i
   2.447 -[(Binding.name automaton_name,
   2.448 -Type("*",
   2.449 -[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
   2.450 - Type("*",[Type("set",[st_typ]),
   2.451 -  Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
   2.452 -   Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
   2.453 -,NoSyn)]
   2.454 -|> add_defs
   2.455 -[(automaton_name ^ "_def",
   2.456 -automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
   2.457 -end)
   2.458 -
   2.459 -
   2.460 -(** outer syntax **)
   2.461 -
   2.462 -(* prepare results *)
   2.463 -
   2.464 -(*encoding transition specifications with a element of ParseTrans*)
   2.465 -datatype ParseTrans = Rel of string | PP of string*(string*string)list;
   2.466 -fun mk_trans_of_rel s = Rel(s);
   2.467 -fun mk_trans_of_prepost (s,l) = PP(s,l); 
   2.468 -
   2.469 -fun trans_of (a, Rel b) = (a, b, [("", "")])
   2.470 -  | trans_of (a, PP (b, l)) = (a, b, l);
   2.471 -
   2.472 -
   2.473 -fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) =
   2.474 -  add_ioa aut action_type inp out int states initial (map trans_of trans);
   2.475 -
   2.476 -fun mk_composition_decl (aut, autlist) =
   2.477 -  add_composition aut autlist;
   2.478 -
   2.479 -fun mk_hiding_decl (aut, (actlist, source_aut)) =
   2.480 -  add_hiding aut source_aut actlist;
   2.481 -
   2.482 -fun mk_restriction_decl (aut, (source_aut, actlist)) =
   2.483 -  add_restriction aut source_aut actlist;
   2.484 -
   2.485 -fun mk_rename_decl (aut, (source_aut, rename_f)) =
   2.486 -  add_rename aut source_aut rename_f;
   2.487 -
   2.488 -
   2.489 -(* outer syntax *)
   2.490 -
   2.491 -local structure P = OuterParse and K = OuterKeyword in
   2.492 -
   2.493 -val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs",
   2.494 -  "outputs", "internals", "states", "initially", "transitions", "pre",
   2.495 -  "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
   2.496 -  "rename"];
   2.497 -
   2.498 -val actionlist = P.list1 P.term;
   2.499 -val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
   2.500 -val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
   2.501 -val internalslist = P.$$$ "internals" |-- P.!!! actionlist;
   2.502 -val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ));
   2.503 -val initial = P.$$$ "initially" |-- P.!!! P.term;
   2.504 -val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term);
   2.505 -val pre = P.$$$ "pre" |-- P.!!! P.term;
   2.506 -val post = P.$$$ "post" |-- P.!!! assign_list;
   2.507 -val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost;
   2.508 -val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost;
   2.509 -val transrel =  (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel;
   2.510 -val transition = P.term -- (transrel || pre1 || post1);
   2.511 -val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition);
   2.512 -
   2.513 -val ioa_decl =
   2.514 -  (P.name -- (P.$$$ "=" |--
   2.515 -    (P.$$$ "signature" |--
   2.516 -      P.!!! (P.$$$ "actions" |--
   2.517 -        (P.typ --
   2.518 -          (Scan.optional inputslist []) --
   2.519 -          (Scan.optional outputslist []) --
   2.520 -          (Scan.optional internalslist []) --
   2.521 -          stateslist --
   2.522 -          (Scan.optional initial "True") --
   2.523 -        translist))))) >> mk_ioa_decl ||
   2.524 -  (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name))))
   2.525 -    >> mk_composition_decl ||
   2.526 -  (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |--
   2.527 -      P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl ||
   2.528 -  (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |--
   2.529 -      P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl ||
   2.530 -  (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
   2.531 -    >> mk_rename_decl;
   2.532 -
   2.533 -val _ =
   2.534 -  OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
   2.535 -    (ioa_decl >> Toplevel.theory);
   2.536 -
   2.537 -end;
   2.538 -
   2.539 -end;