src/HOLCF/IOA/meta_theory/automaton.ML
author haftmann
Wed May 05 18:25:34 2010 +0200 (2010-05-05)
changeset 36692 54b64d4ad524
parent 32960 69916a850301
child 36960 01594f816e3a
permissions -rw-r--r--
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
     1 (*  Title:      HOLCF/IOA/meta_theory/automaton.ML
     2     Author:     Tobias Hamberger, TU Muenchen
     3 *)
     4 
     5 signature AUTOMATON =
     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 Automaton: AUTOMATON =
    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 member (op =) inp chead then
   215 (
   216 error("Input action " ^ tr ^ " was not specified")
   217 ) else (
   218 if member (op =) out chead orelse member (op =) int chead 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 member (op =) inp chead andalso e then (
   231 error("Input action " ^ b ^ " has a precondition")
   232 ) else (if member (op =) (inp@out@int) chead 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 member (op =) l a 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;