author | wenzelm |
Sun, 24 Feb 2002 21:45:57 +0100 | |
changeset 12928 | 6ffd206f93ee |
parent 12339 | f0b62ad4e1a6 |
child 15457 | 1fbd4aba46e3 |
permissions | -rw-r--r-- |
6508 | 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$ |
6508 | 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 |
12339 | 8 |
val add_ioa: string -> string -> |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
9 |
(string) list -> (string) list -> (string) list -> |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
10 |
(string * string) list -> string -> |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
11 |
(string * string * (string * string)list) list |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
12 |
-> theory -> theory |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
13 |
val add_composition : string -> (string)list -> theory -> theory |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
14 |
val add_hiding : string -> string -> (string)list -> theory -> theory |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
15 |
val add_restriction : string -> string -> (string)list -> theory -> theory |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
16 |
val add_rename : string -> string -> string -> theory -> theory |
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 | 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 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
22 |
exception malformed; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
23 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
24 |
(* stripping quotes *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
25 |
fun strip [] = [] | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
26 |
strip ("\""::r) = strip r | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
27 |
strip (a::r) = a :: (strip r); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
28 |
fun strip_quote s = implode(strip(explode(s))); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
29 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
30 |
(* used by *_of_varlist *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
31 |
fun extract_first (a,b) = strip_quote a; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
32 |
fun extract_second (a,b) = strip_quote b; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
33 |
(* following functions producing sth from a varlist *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
34 |
fun comma_list_of_varlist [] = "" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
35 |
comma_list_of_varlist [a] = extract_first a | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
36 |
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
|
37 |
fun primed_comma_list_of_varlist [] = "" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
38 |
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
|
39 |
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
|
40 |
(primed_comma_list_of_varlist r); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
41 |
fun type_product_of_varlist [] = "" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
42 |
type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
43 |
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
|
44 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
45 |
(* listing a list *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
46 |
fun list_elements_of [] = "" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
47 |
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
|
48 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
49 |
(* extracting type parameters from a type list *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
50 |
(* fun param_tupel thy [] res = res | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
51 |
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
|
52 |
param_tupel thy ((TFree(a,_))::r) res = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
53 |
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
|
54 |
param_tupel thy (a::r) res = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
55 |
error ("one component of a statetype is a TVar: " ^ (Sign.string_of_typ (sign_of thy) a)); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
56 |
*) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
57 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
58 |
(* used by constr_list *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
59 |
fun extract_constrs thy [] = [] | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
60 |
extract_constrs thy (a::r) = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
61 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
62 |
fun is_prefix [] s = true |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
63 |
| is_prefix (p::ps) [] = false |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
64 |
| is_prefix (p::ps) (x::xs) = (p=x) andalso (is_prefix ps xs); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
65 |
fun delete_bold [] = [] |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
66 |
| delete_bold (x::xs) = if (is_prefix ("\^["::"["::"1"::"m"::[]) (x::xs)) |
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) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
68 |
else (if (is_prefix ("\^["::"["::"0"::"m"::[]) (x::xs)) |
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 *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
81 |
fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(variant_abs(a,T,r)))| |
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 | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
83 |
extract_constr thy (Var(_,_) $ r) = delete_bold_string(Sign.string_of_term (sign_of thy) r) | |
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 = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
94 |
error("malformed action type: " ^ (Sign.string_of_typ (sign_of thy) s)); |
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; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
101 |
val prem = prems_of (get_thm thy (uq_atypstr ^ ".induct")); |
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 |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
135 |
val trm = #t(rep_cterm(read_cterm (sign_of thy) (ctstr,atyp))); |
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 => |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
143 |
error("malformed action term: " ^ (Sign.string_of_term (sign_of thy) trm)) |
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; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
152 |
val trm = #t(rep_cterm(read_cterm (sign_of thy) (s,#T(rep_ctyp(read_ctyp (sign_of thy) atypstr))) )) |
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 |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
180 |
val trm = #t(rep_cterm(read_cterm (sign_of thy) (actstr,atyp))); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
181 |
val rtrm = #t(rep_cterm(read_cterm (sign_of thy) (r,Type("bool",[])))); |
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); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
194 |
val trm = #t(rep_cterm(read_cterm (sign_of thy) (actstr,atyp))); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
195 |
val rtrm = #t(rep_cterm(read_cterm (sign_of thy) (r,Type("bool",[])))); |
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 | 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 => |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
240 |
error ("malformed action term: " ^ (Sign.string_of_term (sign_of thy) a)) |
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; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
287 |
val aut_def = concl_of(get_thm thy (aut_name ^ "_def")); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
288 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
289 |
(#T(rep_cterm(cterm_of (sign_of thy) (left_of aut_def)))) |
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" ^ |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
295 |
(Sign.string_of_typ (sign_of thy) t)); |
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" ^ |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
298 |
(Sign.string_of_typ (sign_of thy) t)); |
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 | 327 |
(* add_ioa *) |
328 |
||
329 |
fun add_ioa automaton_name action_type inp out int statetupel ini trans thy = |
|
6508 | 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); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
333 |
val styp = #T(rep_ctyp (read_ctyp (sign_of thy) state_type_string)) ; |
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) ^ ")"; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
336 |
val atyp = #T(rep_ctyp (read_ctyp (sign_of thy) action_type)); |
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)] |
9317 | 353 |
|> (#1 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 |
]) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
367 |
val chk_prime_list = (check_free_primed (#t(rep_cterm(read_cterm (sign_of thy2) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
368 |
( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string),Type("bool",[])))))); |
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 | 378 |
fun add_composition automaton_name aut_list thy = |
6508 | 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)] |
9317 | 394 |
|> (#1 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 | 399 |
fun add_restriction automaton_name aut_source actlist thy = |
6508 | 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)] |
9317 | 409 |
|> (#1 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 | 413 |
fun add_hiding automaton_name aut_source actlist thy = |
6508 | 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)] |
9317 | 423 |
|> (#1 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 = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
429 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
430 |
(* going into a pseudo-proof-state to enable the use of function read *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
431 |
val _ = goal thy (funct ^ " = t"); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
432 |
fun arg_typ_of (Type("fun",[a,b])) = a | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
433 |
arg_typ_of _ = raise malformed; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
434 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
435 |
arg_typ_of(#T(rep_cterm(cterm_of (sign_of thy) (read(funct))))) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
436 |
handle malformed => error ("could not extract argument type of renaming function term") |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
437 |
end; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
438 |
|
12339 | 439 |
fun add_rename automaton_name aut_source fun_name thy = |
6508 | 440 |
(writeln("Constructing automaton " ^ automaton_name ^ " ..."); |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
441 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
442 |
val auttyp = aut_type_of thy aut_source; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
443 |
val st_typ = st_type_of thy auttyp; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
444 |
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
|
445 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
446 |
thy |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
447 |
|> ContConsts.add_consts_i |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
448 |
[(automaton_name, |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
449 |
Type("*", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
450 |
[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
|
451 |
Type("*",[Type("set",[st_typ]), |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
452 |
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
|
453 |
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
|
454 |
,NoSyn)] |
9317 | 455 |
|> (#1 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
|
456 |
[(automaton_name ^ "_def", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
457 |
automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")] |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
458 |
end) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
459 |
|
6508 | 460 |
|
461 |
(** outer syntax **) |
|
462 |
||
463 |
(* prepare results *) |
|
464 |
||
465 |
(*encoding transition specifications with a element of ParseTrans*) |
|
466 |
datatype ParseTrans = Rel of string | PP of string*(string*string)list; |
|
467 |
fun mk_trans_of_rel s = Rel(s); |
|
468 |
fun mk_trans_of_prepost (s,l) = PP(s,l); |
|
469 |
||
470 |
fun trans_of (a, Rel b) = (a, b, [("", "")]) |
|
471 |
| trans_of (a, PP (b, l)) = (a, b, l); |
|
472 |
||
473 |
||
474 |
fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) = |
|
475 |
add_ioa aut action_type inp out int states initial (map trans_of trans); |
|
476 |
||
477 |
fun mk_composition_decl (aut, autlist) = |
|
478 |
add_composition aut autlist; |
|
479 |
||
480 |
fun mk_hiding_decl (aut, (actlist, source_aut)) = |
|
481 |
add_hiding aut source_aut actlist; |
|
482 |
||
483 |
fun mk_restriction_decl (aut, (source_aut, actlist)) = |
|
484 |
add_restriction aut source_aut actlist; |
|
485 |
||
486 |
fun mk_rename_decl (aut, (source_aut, rename_f)) = |
|
487 |
add_rename aut source_aut rename_f; |
|
488 |
||
489 |
||
490 |
(* parsers *) |
|
491 |
||
6723 | 492 |
local structure P = OuterParse and K = OuterSyntax.Keyword in |
6508 | 493 |
|
6723 | 494 |
val actionlist = P.list1 P.term; |
495 |
val inputslist = P.$$$ "inputs" |-- actionlist; |
|
496 |
val outputslist = P.$$$ "outputs" |-- actionlist; |
|
497 |
val internalslist = P.$$$ "internals" |-- actionlist; |
|
498 |
val stateslist = P.$$$ "states" |-- Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ); |
|
499 |
val initial = P.$$$ "initially" |-- P.term; |
|
500 |
val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.term); |
|
501 |
val pre = P.$$$ "pre" |-- P.term; |
|
502 |
val post = P.$$$ "post" |-- assign_list; |
|
6508 | 503 |
val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost; |
504 |
val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost; |
|
6723 | 505 |
val transrel = (P.$$$ "transrel" |-- P.term) >> mk_trans_of_rel; |
506 |
val transition = P.term -- (transrel || pre1 || post1); |
|
507 |
val translist = P.$$$ "transitions" |-- Scan.repeat1 transition; |
|
6508 | 508 |
|
509 |
val ioa_decl = |
|
6723 | 510 |
(P.name -- (P.$$$ "=" |-- |
511 |
(P.$$$ "signature" |-- |
|
512 |
(P.$$$ "actions" |-- |
|
513 |
(P.typ -- |
|
6508 | 514 |
(Scan.optional inputslist []) -- |
515 |
(Scan.optional outputslist []) -- |
|
516 |
(Scan.optional internalslist []) -- |
|
517 |
stateslist -- |
|
518 |
(Scan.optional initial "True") -- |
|
519 |
translist))))) >> mk_ioa_decl || |
|
6723 | 520 |
(P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.list1 P.name))) >> mk_composition_decl || |
8733 | 521 |
(P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |-- P.list1 P.term -- (P.$$$ "in" |-- P.name)))) |
6723 | 522 |
>> mk_hiding_decl || |
523 |
(P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |-- P.name -- (P.$$$ "to" |-- P.list1 P.term)))) |
|
6508 | 524 |
>> mk_restriction_decl || |
12928 | 525 |
(P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- P.name -- (P.$$$ "to" |-- P.term)))) |
6723 | 526 |
>> mk_rename_decl; |
6508 | 527 |
|
6723 | 528 |
val automatonP = |
529 |
OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl |
|
530 |
(ioa_decl >> Toplevel.theory); |
|
6508 | 531 |
|
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
532 |
end; |
6508 | 533 |
|
534 |
||
535 |
(* setup outer syntax *) |
|
536 |
||
537 |
val _ = OuterSyntax.add_keywords ["signature", "actions", "inputs", |
|
538 |
"outputs", "internals", "states", "initially", "transitions", "pre", |
|
8733 | 539 |
"post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to", |
12928 | 540 |
"rename"]; |
6508 | 541 |
|
542 |
val _ = OuterSyntax.add_parsers [automatonP]; |
|
543 |
||
544 |
||
545 |
end; |