src/HOLCF/IOA/meta_theory/ioa_package.ML
author wenzelm
Wed Jun 25 17:38:32 2008 +0200 (2008-06-25)
changeset 27353 71c4dd53d4cb
parent 27251 121991a4884d
child 27691 ce171cbd4b93
permissions -rw-r--r--
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
     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 = PrintMode.setmp [] o Syntax.string_of_typ_global;
    23 val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global;
    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 thy a));
    59 *)
    60 
    61 (* used by constr_list *)
    62 fun extract_constrs thy [] = [] |
    63 extract_constrs thy (a::r) =
    64 let
    65 fun delete_bold [] = []
    66 | delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
    67         then (let val (_::_::_::s) = xs in delete_bold s end)
    68         else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
    69                 then  (let val (_::_::_::s) = xs in delete_bold s end)
    70                 else (x::delete_bold xs));
    71 fun delete_bold_string s = implode(delete_bold(explode s));
    72 (* from a constructor term in *.induct (with quantifiers,
    73 "Trueprop" and ?P stripped away) delivers the head *)
    74 fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r |
    75 extract_hd (Const("Trueprop",_) $ r) = extract_hd r |
    76 extract_hd (Var(_,_) $ r) = extract_hd r |
    77 extract_hd (a $ b) = extract_hd a |
    78 extract_hd (Const(s,_)) = s |
    79 extract_hd _ = raise malformed;
    80 (* delivers constructor term string from a prem of *.induct *)
    81 fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))|
    82 extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r |
    83 extract_constr thy (Var(_,_) $ r) =  delete_bold_string(string_of_term thy r) |
    84 extract_constr _ _ = raise malformed;
    85 in
    86 (extract_hd a,extract_constr thy a) :: (extract_constrs thy r)
    87 end;
    88 
    89 (* delivering list of constructor terms of a datatype *)
    90 fun constr_list thy atyp =
    91 let
    92 fun act_name thy (Type(s,_)) = s |
    93 act_name _ s = 
    94 error("malformed action type: " ^ (string_of_typ thy s));
    95 fun afpl ("." :: a) = [] |
    96 afpl [] = [] |
    97 afpl (a::r) = a :: (afpl r);
    98 fun unqualify s = implode(rev(afpl(rev(explode s))));
    99 val q_atypstr = act_name thy atyp;
   100 val uq_atypstr = unqualify q_atypstr;
   101 val prem = prems_of (PureThy.get_thm thy (uq_atypstr ^ ".induct"));
   102 in
   103 extract_constrs thy prem
   104 handle malformed =>
   105 error("malformed theorem : " ^ uq_atypstr ^ ".induct")
   106 end;
   107 
   108 fun check_for_constr thy atyp (a $ b) =
   109 let
   110 fun all_free (Free(_,_)) = true |
   111 all_free (a $ b) = if (all_free a) then (all_free b) else false |
   112 all_free _ = false; 
   113 in 
   114 if (all_free b) then (check_for_constr thy atyp a) else false
   115 end |
   116 check_for_constr thy atyp (Const(a,_)) =
   117 let
   118 val cl = constr_list thy atyp;
   119 fun fstmem a [] = false |
   120 fstmem a ((f,s)::r) = if (a=f) then true else (fstmem a r)
   121 in
   122 if (fstmem a cl) then true else false
   123 end |
   124 check_for_constr _ _ _ = false;
   125 
   126 (* delivering the free variables of a constructor term *)
   127 fun free_vars_of (t1 $ t2) = (free_vars_of t1) @ (free_vars_of t2) |
   128 free_vars_of (Const(_,_)) = [] |
   129 free_vars_of (Free(a,_)) = [a] |
   130 free_vars_of _ = raise malformed;
   131 
   132 (* making a constructor set from a constructor term (of signature) *)
   133 fun constr_set_string thy atyp ctstr =
   134 let
   135 val trm = OldGoals.simple_read_term thy atyp ctstr;
   136 val l = free_vars_of trm
   137 in
   138 if (check_for_constr thy atyp trm) then
   139 (if (l=[]) then ("{" ^ ctstr ^ "}")
   140 else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})")
   141 else (raise malformed) 
   142 handle malformed => 
   143 error("malformed action term: " ^ (string_of_term thy trm))
   144 end;
   145 
   146 (* extracting constructor heads *)
   147 fun constructor_head thy atypstr s =
   148 let
   149 fun hd_of (Const(a,_)) = a |
   150 hd_of (t $ _) = hd_of t |
   151 hd_of _ = raise malformed;
   152 val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
   153 in
   154 hd_of trm handle malformed =>
   155 error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
   156 end;
   157 fun constructor_head_list _ _ [] = [] |
   158 constructor_head_list thy atypstr (a::r) =
   159  (constructor_head thy atypstr a)::(constructor_head_list thy atypstr r);
   160 
   161 (* producing an action set *)
   162 fun action_set_string thy atyp [] = "{}" |
   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 (chead mem inp) then
   215 (
   216 error("Input action " ^ tr ^ " was not specified")
   217 ) else (
   218 if (chead mem (out@int)) 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 ((chead mem inp) andalso e) then (
   231 error("Input action " ^ b ^ " has a precondition")
   232 ) else (if (chead mem (inp@out@int)) 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 (a mem l) 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 
   327 (* add_ioa *)
   328 
   329 fun add_ioa automaton_name action_type inp out int statetupel ini trans thy =
   330 (writeln("Constructing automaton " ^ automaton_name ^ " ...");
   331 let
   332 val state_type_string = type_product_of_varlist(statetupel);
   333 val styp = Syntax.read_typ_global thy state_type_string;
   334 val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")";
   335 val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")";
   336 val atyp = Syntax.read_typ_global thy action_type;
   337 val inp_set_string = action_set_string thy atyp inp;
   338 val out_set_string = action_set_string thy atyp out;
   339 val int_set_string = action_set_string thy atyp int;
   340 val inp_head_list = constructor_head_list thy action_type inp;
   341 val out_head_list = constructor_head_list thy action_type out;
   342 val int_head_list = constructor_head_list thy action_type int;
   343 val overlap_flag = ((overlap inp out) andalso (overlap inp int) andalso (overlap out int)); 
   344 val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list 
   345 							atyp statetupel trans;
   346 val thy2 = (thy
   347 |> ContConsts.add_consts
   348 [(automaton_name ^ "_initial", "(" ^ state_type_string ^ ")set" ,NoSyn),
   349 (automaton_name ^ "_asig", "(" ^ action_type ^ ")signature" ,NoSyn),
   350 (automaton_name ^ "_trans",
   351  "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
   352 (automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
   353 |> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
   354 [(automaton_name ^ "_initial_def",
   355 automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
   356 (automaton_name ^ "_asig_def",
   357 automaton_name ^ "_asig == (" ^
   358  inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"),
   359 (automaton_name ^ "_trans_def",
   360 automaton_name ^ "_trans == {(" ^
   361  state_vars_tupel ^ ", act_of_" ^ automaton_name ^ ", " ^ state_vars_primed ^
   362 "). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"),
   363 (automaton_name ^ "_def",
   364 automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
   365 "_initial, " ^ automaton_name ^ "_trans,{},{})")
   366 ])
   367 val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[]))
   368 ( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
   369 in
   370 (
   371 if (chk_prime_list = []) then thy2
   372 else (
   373 error("Precondition or assignment terms in postconditions contain following primed variables:\n"
   374  ^ (list_elements_of chk_prime_list)))
   375 )
   376 end)
   377 
   378 fun add_composition automaton_name aut_list thy =
   379 (writeln("Constructing automaton " ^ automaton_name ^ " ...");
   380 let
   381 val acttyp = check_ac thy aut_list; 
   382 val st_typ = comp_st_type_of thy aut_list; 
   383 val comp_list = clist aut_list;
   384 in
   385 thy
   386 |> ContConsts.add_consts_i
   387 [(automaton_name,
   388 Type("*",
   389 [Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
   390  Type("*",[Type("set",[st_typ]),
   391   Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
   392    Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
   393 ,NoSyn)]
   394 |> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
   395 [(automaton_name ^ "_def",
   396 automaton_name ^ " == " ^ comp_list)]
   397 end)
   398 
   399 fun add_restriction automaton_name aut_source actlist thy =
   400 (writeln("Constructing automaton " ^ automaton_name ^ " ...");
   401 let
   402 val auttyp = aut_type_of thy aut_source;
   403 val acttyp = act_type_of thy auttyp; 
   404 val rest_set = action_set_string thy acttyp actlist
   405 in
   406 thy
   407 |> ContConsts.add_consts_i
   408 [(automaton_name, auttyp,NoSyn)]
   409 |> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
   410 [(automaton_name ^ "_def",
   411 automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] 
   412 end)
   413 fun add_hiding automaton_name aut_source actlist thy =
   414 (writeln("Constructing automaton " ^ automaton_name ^ " ...");
   415 let
   416 val auttyp = aut_type_of thy aut_source;
   417 val acttyp = act_type_of thy auttyp; 
   418 val hid_set = action_set_string thy acttyp actlist
   419 in
   420 thy
   421 |> ContConsts.add_consts_i
   422 [(automaton_name, auttyp,NoSyn)]
   423 |> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
   424 [(automaton_name ^ "_def",
   425 automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] 
   426 end)
   427 
   428 fun ren_act_type_of thy funct =
   429   (case Term.fastype_of (Syntax.read_term_global thy funct) of
   430     Type ("fun", [a, b]) => a
   431   | _ => error "could not extract argument type of renaming function term");
   432  
   433 fun add_rename automaton_name aut_source fun_name thy =
   434 (writeln("Constructing automaton " ^ automaton_name ^ " ...");
   435 let
   436 val auttyp = aut_type_of thy aut_source;
   437 val st_typ = st_type_of thy auttyp;
   438 val acttyp = ren_act_type_of thy fun_name
   439 in
   440 thy
   441 |> ContConsts.add_consts_i
   442 [(automaton_name,
   443 Type("*",
   444 [Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
   445  Type("*",[Type("set",[st_typ]),
   446   Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
   447    Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
   448 ,NoSyn)]
   449 |> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
   450 [(automaton_name ^ "_def",
   451 automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
   452 end)
   453 
   454 
   455 (** outer syntax **)
   456 
   457 (* prepare results *)
   458 
   459 (*encoding transition specifications with a element of ParseTrans*)
   460 datatype ParseTrans = Rel of string | PP of string*(string*string)list;
   461 fun mk_trans_of_rel s = Rel(s);
   462 fun mk_trans_of_prepost (s,l) = PP(s,l); 
   463 
   464 fun trans_of (a, Rel b) = (a, b, [("", "")])
   465   | trans_of (a, PP (b, l)) = (a, b, l);
   466 
   467 
   468 fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) =
   469   add_ioa aut action_type inp out int states initial (map trans_of trans);
   470 
   471 fun mk_composition_decl (aut, autlist) =
   472   add_composition aut autlist;
   473 
   474 fun mk_hiding_decl (aut, (actlist, source_aut)) =
   475   add_hiding aut source_aut actlist;
   476 
   477 fun mk_restriction_decl (aut, (source_aut, actlist)) =
   478   add_restriction aut source_aut actlist;
   479 
   480 fun mk_rename_decl (aut, (source_aut, rename_f)) =
   481   add_rename aut source_aut rename_f;
   482 
   483 
   484 (* outer syntax *)
   485 
   486 local structure P = OuterParse and K = OuterKeyword in
   487 
   488 val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs",
   489   "outputs", "internals", "states", "initially", "transitions", "pre",
   490   "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
   491   "rename"];
   492 
   493 val actionlist = P.list1 P.term;
   494 val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
   495 val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
   496 val internalslist = P.$$$ "internals" |-- P.!!! actionlist;
   497 val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ));
   498 val initial = P.$$$ "initially" |-- P.!!! P.term;
   499 val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term);
   500 val pre = P.$$$ "pre" |-- P.!!! P.term;
   501 val post = P.$$$ "post" |-- P.!!! assign_list;
   502 val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost;
   503 val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost;
   504 val transrel =  (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel;
   505 val transition = P.term -- (transrel || pre1 || post1);
   506 val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition);
   507 
   508 val ioa_decl =
   509   (P.name -- (P.$$$ "=" |--
   510     (P.$$$ "signature" |--
   511       P.!!! (P.$$$ "actions" |--
   512         (P.typ --
   513           (Scan.optional inputslist []) --
   514           (Scan.optional outputslist []) --
   515           (Scan.optional internalslist []) --
   516           stateslist --
   517           (Scan.optional initial "True") --
   518         translist))))) >> mk_ioa_decl ||
   519   (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name))))
   520     >> mk_composition_decl ||
   521   (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |--
   522       P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl ||
   523   (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |--
   524       P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl ||
   525   (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
   526     >> mk_rename_decl;
   527 
   528 val _ =
   529   OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
   530     (ioa_decl >> Toplevel.theory);
   531 
   532 end;
   533 
   534 end;