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