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