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