author | wenzelm |
Sat, 17 Oct 2009 14:43:18 +0200 | |
changeset 32960 | 69916a850301 |
parent 31774 | 5c8cfaed32e6 |
child 36692 | 54b64d4ad524 |
permissions | -rw-r--r-- |
31774 | 1 |
(* Title: HOLCF/IOA/meta_theory/automaton.ML |
18358 | 2 |
Author: Tobias Hamberger, TU Muenchen |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
3 |
*) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
4 |
|
31774 | 5 |
signature AUTOMATON = |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
6 |
sig |
18358 | 7 |
val add_ioa: string -> string |
8 |
-> (string) list -> (string) list -> (string) list |
|
9 |
-> (string * string) list -> string |
|
10 |
-> (string * string * (string * string)list) list |
|
11 |
-> theory -> theory |
|
12 |
val add_composition : string -> (string)list -> theory -> theory |
|
13 |
val add_hiding : string -> string -> (string)list -> theory -> theory |
|
14 |
val add_restriction : string -> string -> (string)list -> theory -> theory |
|
15 |
val add_rename : string -> string -> string -> theory -> theory |
|
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
16 |
end; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
17 |
|
31774 | 18 |
structure Automaton: AUTOMATON = |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
19 |
struct |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
20 |
|
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26343
diff
changeset
|
21 |
val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global; |
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26343
diff
changeset
|
22 |
val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global; |
17243
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset
|
23 |
|
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
24 |
exception malformed; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
25 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
26 |
(* stripping quotes *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
27 |
fun strip [] = [] | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
28 |
strip ("\""::r) = strip r | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
29 |
strip (a::r) = a :: (strip r); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
30 |
fun strip_quote s = implode(strip(explode(s))); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
31 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
32 |
(* used by *_of_varlist *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
33 |
fun extract_first (a,b) = strip_quote a; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
34 |
fun extract_second (a,b) = strip_quote b; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
35 |
(* following functions producing sth from a varlist *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
36 |
fun comma_list_of_varlist [] = "" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
37 |
comma_list_of_varlist [a] = extract_first a | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
38 |
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
|
39 |
fun primed_comma_list_of_varlist [] = "" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
40 |
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
|
41 |
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
|
42 |
(primed_comma_list_of_varlist r); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
43 |
fun type_product_of_varlist [] = "" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
44 |
type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
45 |
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
|
46 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
47 |
(* listing a list *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
48 |
fun list_elements_of [] = "" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
49 |
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
|
50 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
51 |
(* extracting type parameters from a type list *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
52 |
(* fun param_tupel thy [] res = res | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
53 |
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
|
54 |
param_tupel thy ((TFree(a,_))::r) res = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
55 |
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
|
56 |
param_tupel thy (a::r) res = |
22578 | 57 |
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
|
58 |
*) |
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 |
(* used by constr_list *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
61 |
fun extract_constrs thy [] = [] | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
62 |
extract_constrs thy (a::r) = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
63 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
64 |
fun delete_bold [] = [] |
18443 | 65 |
| 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
|
66 |
then (let val (_::_::_::s) = xs in delete_bold s end) |
18443 | 67 |
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
|
68 |
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
|
69 |
else (x::delete_bold xs)); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
70 |
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
|
71 |
(* from a constructor term in *.induct (with quantifiers, |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
72 |
"Trueprop" and ?P stripped away) delivers the head *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
73 |
fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
74 |
extract_hd (Const("Trueprop",_) $ r) = extract_hd r | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
75 |
extract_hd (Var(_,_) $ r) = extract_hd r | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
76 |
extract_hd (a $ b) = extract_hd a | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
77 |
extract_hd (Const(s,_)) = s | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
78 |
extract_hd _ = raise malformed; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
79 |
(* delivers constructor term string from a prem of *.induct *) |
20194 | 80 |
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
|
81 |
extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r | |
22578 | 82 |
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
|
83 |
extract_constr _ _ = raise malformed; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
84 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
85 |
(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
|
86 |
end; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
87 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
88 |
(* delivering list of constructor terms of a datatype *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
89 |
fun constr_list thy atyp = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
90 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
91 |
fun act_name thy (Type(s,_)) = s | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
92 |
act_name _ s = |
22578 | 93 |
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
|
94 |
fun afpl ("." :: a) = [] | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
95 |
afpl [] = [] | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
96 |
afpl (a::r) = a :: (afpl r); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
97 |
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
|
98 |
val q_atypstr = act_name thy atyp; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
99 |
val uq_atypstr = unqualify q_atypstr; |
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset
|
100 |
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
|
101 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
102 |
extract_constrs thy prem |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
103 |
handle malformed => |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
104 |
error("malformed theorem : " ^ uq_atypstr ^ ".induct") |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
105 |
end; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
106 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
107 |
fun check_for_constr thy atyp (a $ b) = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
108 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
109 |
fun all_free (Free(_,_)) = true | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
110 |
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
|
111 |
all_free _ = false; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
112 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
113 |
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
|
114 |
end | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
115 |
check_for_constr thy atyp (Const(a,_)) = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
116 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
117 |
val cl = constr_list thy atyp; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
118 |
fun fstmem a [] = false | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
119 |
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
|
120 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
121 |
if (fstmem a cl) then true else false |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
122 |
end | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
123 |
check_for_constr _ _ _ = false; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
124 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
125 |
(* delivering the free variables of a constructor term *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
126 |
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
|
127 |
free_vars_of (Const(_,_)) = [] | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
128 |
free_vars_of (Free(a,_)) = [a] | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
129 |
free_vars_of _ = raise malformed; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
130 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
131 |
(* 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
|
132 |
fun constr_set_string thy atyp ctstr = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
133 |
let |
27251 | 134 |
val trm = OldGoals.simple_read_term thy atyp ctstr; |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
135 |
val l = free_vars_of trm |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
136 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
137 |
if (check_for_constr thy atyp trm) then |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
138 |
(if (l=[]) then ("{" ^ ctstr ^ "}") |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
139 |
else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})") |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
140 |
else (raise malformed) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
141 |
handle malformed => |
22578 | 142 |
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
|
143 |
end; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
144 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
145 |
(* extracting constructor heads *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
146 |
fun constructor_head thy atypstr s = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
147 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
148 |
fun hd_of (Const(a,_)) = a | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
149 |
hd_of (t $ _) = hd_of t | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
150 |
hd_of _ = raise malformed; |
27251 | 151 |
val trm = OldGoals.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
|
152 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
153 |
hd_of trm handle malformed => |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
154 |
error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
155 |
end; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
156 |
fun constructor_head_list _ _ [] = [] | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
157 |
constructor_head_list thy atypstr (a::r) = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
158 |
(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
|
159 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
160 |
(* producing an action set *) |
30304
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
27691
diff
changeset
|
161 |
(*FIXME*) |
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
27691
diff
changeset
|
162 |
fun action_set_string thy atyp [] = "Set.empty" | |
6467
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 |
27251 | 180 |
val trm = OldGoals.simple_read_term thy atyp actstr; |
181 |
val rtrm = OldGoals.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); |
27251 | 194 |
val trm = OldGoals.simple_read_term thy atyp actstr; |
195 |
val rtrm = OldGoals.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)), |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31774
diff
changeset
|
203 |
"(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag)) |
6467
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) = |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31774
diff
changeset
|
210 |
(extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r); |
6467
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 | 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 |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31774
diff
changeset
|
233 |
(if (occurs_again chead r) then ( |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
234 |
error("Two specifications for action: " ^ b) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31774
diff
changeset
|
235 |
) else (b ^ " => " ^ c,b ^ " => " ^ d)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31774
diff
changeset
|
236 |
else ( |
6467
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 | 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 | 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 | 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 | 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 | 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 |
|
30346 | 326 |
val add_defs = snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes o map (apfst Binding.name)); |
327 |
||
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
328 |
|
12339 | 329 |
(* add_ioa *) |
330 |
||
331 |
fun add_ioa automaton_name action_type inp out int statetupel ini trans thy = |
|
6508 | 332 |
(writeln("Constructing automaton " ^ automaton_name ^ " ..."); |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
333 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
334 |
val state_type_string = type_product_of_varlist(statetupel); |
24707 | 335 |
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
|
336 |
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
|
337 |
val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")"; |
24707 | 338 |
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
|
339 |
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
|
340 |
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
|
341 |
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
|
342 |
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
|
343 |
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
|
344 |
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
|
345 |
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
|
346 |
val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31774
diff
changeset
|
347 |
atyp statetupel trans; |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
348 |
val thy2 = (thy |
30918
21ce52733a4d
use Sign.add_consts instead of ContConsts.add_consts
huffman
parents:
30346
diff
changeset
|
349 |
|> Sign.add_consts |
21ce52733a4d
use Sign.add_consts instead of ContConsts.add_consts
huffman
parents:
30346
diff
changeset
|
350 |
[(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn), |
21ce52733a4d
use Sign.add_consts instead of ContConsts.add_consts
huffman
parents:
30346
diff
changeset
|
351 |
(Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn), |
21ce52733a4d
use Sign.add_consts instead of ContConsts.add_consts
huffman
parents:
30346
diff
changeset
|
352 |
(Binding.name (automaton_name ^ "_trans"), |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
353 |
"(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn), |
30918
21ce52733a4d
use Sign.add_consts instead of ContConsts.add_consts
huffman
parents:
30346
diff
changeset
|
354 |
(Binding.name automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)] |
30346 | 355 |
|> add_defs |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
356 |
[(automaton_name ^ "_initial_def", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
357 |
automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"), |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
358 |
(automaton_name ^ "_asig_def", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
359 |
automaton_name ^ "_asig == (" ^ |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
360 |
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
|
361 |
(automaton_name ^ "_trans_def", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
362 |
automaton_name ^ "_trans == {(" ^ |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
363 |
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
|
364 |
"). 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
|
365 |
(automaton_name ^ "_def", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
366 |
automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^ |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
367 |
"_initial, " ^ automaton_name ^ "_trans,{},{})") |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
368 |
]) |
27251 | 369 |
val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[])) |
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22578
diff
changeset
|
370 |
( "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
|
371 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
372 |
( |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
373 |
if (chk_prime_list = []) then thy2 |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
374 |
else ( |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
375 |
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
|
376 |
^ (list_elements_of chk_prime_list))) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
377 |
) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
378 |
end) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
379 |
|
12339 | 380 |
fun add_composition automaton_name aut_list thy = |
6508 | 381 |
(writeln("Constructing automaton " ^ automaton_name ^ " ..."); |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
382 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
383 |
val acttyp = check_ac thy aut_list; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
384 |
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
|
385 |
val comp_list = clist aut_list; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
386 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
387 |
thy |
30918
21ce52733a4d
use Sign.add_consts instead of ContConsts.add_consts
huffman
parents:
30346
diff
changeset
|
388 |
|> Sign.add_consts_i |
21ce52733a4d
use Sign.add_consts instead of ContConsts.add_consts
huffman
parents:
30346
diff
changeset
|
389 |
[(Binding.name automaton_name, |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
390 |
Type("*", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
391 |
[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
|
392 |
Type("*",[Type("set",[st_typ]), |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
393 |
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
|
394 |
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
|
395 |
,NoSyn)] |
30346 | 396 |
|> add_defs |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
397 |
[(automaton_name ^ "_def", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
398 |
automaton_name ^ " == " ^ comp_list)] |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
399 |
end) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
400 |
|
12339 | 401 |
fun add_restriction automaton_name aut_source actlist thy = |
6508 | 402 |
(writeln("Constructing automaton " ^ automaton_name ^ " ..."); |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
403 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
404 |
val auttyp = aut_type_of thy aut_source; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
405 |
val acttyp = act_type_of thy auttyp; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
406 |
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
|
407 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
408 |
thy |
30918
21ce52733a4d
use Sign.add_consts instead of ContConsts.add_consts
huffman
parents:
30346
diff
changeset
|
409 |
|> Sign.add_consts_i |
21ce52733a4d
use Sign.add_consts instead of ContConsts.add_consts
huffman
parents:
30346
diff
changeset
|
410 |
[(Binding.name automaton_name, auttyp,NoSyn)] |
30346 | 411 |
|> add_defs |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
412 |
[(automaton_name ^ "_def", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
413 |
automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
414 |
end) |
12339 | 415 |
fun add_hiding automaton_name aut_source actlist thy = |
6508 | 416 |
(writeln("Constructing automaton " ^ automaton_name ^ " ..."); |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
417 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
418 |
val auttyp = aut_type_of thy aut_source; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
419 |
val acttyp = act_type_of thy auttyp; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
420 |
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
|
421 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
422 |
thy |
30918
21ce52733a4d
use Sign.add_consts instead of ContConsts.add_consts
huffman
parents:
30346
diff
changeset
|
423 |
|> Sign.add_consts_i |
21ce52733a4d
use Sign.add_consts instead of ContConsts.add_consts
huffman
parents:
30346
diff
changeset
|
424 |
[(Binding.name automaton_name, auttyp,NoSyn)] |
30346 | 425 |
|> add_defs |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
426 |
[(automaton_name ^ "_def", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
427 |
automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
428 |
end) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
429 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
430 |
fun ren_act_type_of thy funct = |
24707 | 431 |
(case Term.fastype_of (Syntax.read_term_global thy funct) of |
17925 | 432 |
Type ("fun", [a, b]) => a |
433 |
| _ => 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
|
434 |
|
12339 | 435 |
fun add_rename automaton_name aut_source fun_name thy = |
6508 | 436 |
(writeln("Constructing automaton " ^ automaton_name ^ " ..."); |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
437 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
438 |
val auttyp = aut_type_of thy aut_source; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
439 |
val st_typ = st_type_of thy auttyp; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
440 |
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
|
441 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
442 |
thy |
30918
21ce52733a4d
use Sign.add_consts instead of ContConsts.add_consts
huffman
parents:
30346
diff
changeset
|
443 |
|> Sign.add_consts_i |
21ce52733a4d
use Sign.add_consts instead of ContConsts.add_consts
huffman
parents:
30346
diff
changeset
|
444 |
[(Binding.name automaton_name, |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
445 |
Type("*", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
446 |
[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
|
447 |
Type("*",[Type("set",[st_typ]), |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
448 |
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
|
449 |
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
|
450 |
,NoSyn)] |
30346 | 451 |
|> add_defs |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
452 |
[(automaton_name ^ "_def", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
453 |
automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")] |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
454 |
end) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
455 |
|
6508 | 456 |
|
457 |
(** outer syntax **) |
|
458 |
||
459 |
(* prepare results *) |
|
460 |
||
461 |
(*encoding transition specifications with a element of ParseTrans*) |
|
462 |
datatype ParseTrans = Rel of string | PP of string*(string*string)list; |
|
463 |
fun mk_trans_of_rel s = Rel(s); |
|
464 |
fun mk_trans_of_prepost (s,l) = PP(s,l); |
|
465 |
||
466 |
fun trans_of (a, Rel b) = (a, b, [("", "")]) |
|
467 |
| trans_of (a, PP (b, l)) = (a, b, l); |
|
468 |
||
469 |
||
470 |
fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) = |
|
471 |
add_ioa aut action_type inp out int states initial (map trans_of trans); |
|
472 |
||
473 |
fun mk_composition_decl (aut, autlist) = |
|
474 |
add_composition aut autlist; |
|
475 |
||
476 |
fun mk_hiding_decl (aut, (actlist, source_aut)) = |
|
477 |
add_hiding aut source_aut actlist; |
|
478 |
||
479 |
fun mk_restriction_decl (aut, (source_aut, actlist)) = |
|
480 |
add_restriction aut source_aut actlist; |
|
481 |
||
482 |
fun mk_rename_decl (aut, (source_aut, rename_f)) = |
|
483 |
add_rename aut source_aut rename_f; |
|
484 |
||
485 |
||
24867 | 486 |
(* outer syntax *) |
6508 | 487 |
|
17057 | 488 |
local structure P = OuterParse and K = OuterKeyword in |
6508 | 489 |
|
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
27251
diff
changeset
|
490 |
val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs", |
24867 | 491 |
"outputs", "internals", "states", "initially", "transitions", "pre", |
492 |
"post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to", |
|
493 |
"rename"]; |
|
494 |
||
6723 | 495 |
val actionlist = P.list1 P.term; |
17243
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset
|
496 |
val inputslist = P.$$$ "inputs" |-- P.!!! actionlist; |
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset
|
497 |
val outputslist = P.$$$ "outputs" |-- P.!!! actionlist; |
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset
|
498 |
val internalslist = P.$$$ "internals" |-- P.!!! actionlist; |
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset
|
499 |
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
|
500 |
val initial = P.$$$ "initially" |-- P.!!! P.term; |
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset
|
501 |
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
|
502 |
val pre = P.$$$ "pre" |-- P.!!! P.term; |
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset
|
503 |
val post = P.$$$ "post" |-- P.!!! assign_list; |
6508 | 504 |
val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost; |
505 |
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
|
506 |
val transrel = (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel; |
6723 | 507 |
val transition = P.term -- (transrel || pre1 || post1); |
17243
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset
|
508 |
val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition); |
6508 | 509 |
|
510 |
val ioa_decl = |
|
6723 | 511 |
(P.name -- (P.$$$ "=" |-- |
512 |
(P.$$$ "signature" |-- |
|
17243
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset
|
513 |
P.!!! (P.$$$ "actions" |-- |
6723 | 514 |
(P.typ -- |
6508 | 515 |
(Scan.optional inputslist []) -- |
516 |
(Scan.optional outputslist []) -- |
|
517 |
(Scan.optional internalslist []) -- |
|
518 |
stateslist -- |
|
519 |
(Scan.optional initial "True") -- |
|
520 |
translist))))) >> mk_ioa_decl || |
|
17243
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset
|
521 |
(P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name)))) |
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset
|
522 |
>> mk_composition_decl || |
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset
|
523 |
(P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |-- |
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset
|
524 |
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
|
525 |
(P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |-- |
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset
|
526 |
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
|
527 |
(P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term)))))) |
6723 | 528 |
>> mk_rename_decl; |
6508 | 529 |
|
24867 | 530 |
val _ = |
6723 | 531 |
OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl |
532 |
(ioa_decl >> Toplevel.theory); |
|
6508 | 533 |
|
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
534 |
end; |
6508 | 535 |
|
536 |
end; |