author | wenzelm |
Thu, 12 Oct 2000 17:28:18 +0200 | |
changeset 10203 | 746eb6791aed |
parent 9317 | 7a72952ca068 |
child 12339 | f0b62ad4e1a6 |
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 |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
8 |
val add_ioa: string -> string -> |
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_ioa_i : string -> string -> |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
14 |
(string) list -> (string) list -> (string) list -> |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
15 |
(string * string) list -> string -> |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
16 |
(string * string * (string * string)list) list |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
17 |
-> theory -> theory |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
18 |
val add_composition : string -> (string)list -> theory -> theory |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
19 |
val add_composition_i : string -> (string)list -> theory -> theory |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
20 |
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
|
21 |
val add_hiding_i : string -> string -> (string)list -> theory -> theory |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
22 |
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
|
23 |
val add_restriction_i : string -> string -> (string)list -> theory -> theory |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
24 |
val add_rename : string -> string -> string -> theory -> theory |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
25 |
val add_rename_i : string -> string -> string -> theory -> theory |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
26 |
end; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
27 |
|
6508 | 28 |
structure IoaPackage: IOA_PACKAGE = |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
29 |
struct |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
30 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
31 |
local |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
32 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
33 |
exception malformed; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
34 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
35 |
(* stripping quotes *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
36 |
fun strip [] = [] | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
37 |
strip ("\""::r) = strip r | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
38 |
strip (a::r) = a :: (strip r); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
39 |
fun strip_quote s = implode(strip(explode(s))); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
40 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
41 |
(* used by *_of_varlist *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
42 |
fun extract_first (a,b) = strip_quote a; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
43 |
fun extract_second (a,b) = strip_quote b; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
44 |
(* following functions producing sth from a varlist *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
45 |
fun comma_list_of_varlist [] = "" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
46 |
comma_list_of_varlist [a] = extract_first a | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
47 |
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
|
48 |
fun primed_comma_list_of_varlist [] = "" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
49 |
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
|
50 |
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
|
51 |
(primed_comma_list_of_varlist r); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
52 |
fun type_product_of_varlist [] = "" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
53 |
type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
54 |
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
|
55 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
56 |
(* listing a list *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
57 |
fun list_elements_of [] = "" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
58 |
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
|
59 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
60 |
(* extracting type parameters from a type list *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
61 |
(* fun param_tupel thy [] res = res | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
62 |
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
|
63 |
param_tupel thy ((TFree(a,_))::r) res = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
64 |
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
|
65 |
param_tupel thy (a::r) res = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
66 |
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
|
67 |
*) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
68 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
69 |
(* used by constr_list *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
70 |
fun extract_constrs thy [] = [] | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
71 |
extract_constrs thy (a::r) = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
72 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
73 |
fun is_prefix [] s = true |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
74 |
| is_prefix (p::ps) [] = false |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
75 |
| 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
|
76 |
fun delete_bold [] = [] |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
77 |
| 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
|
78 |
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
|
79 |
else (if (is_prefix ("\^["::"["::"0"::"m"::[]) (x::xs)) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
80 |
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
|
81 |
else (x::delete_bold xs)); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
82 |
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
|
83 |
(* from a constructor term in *.induct (with quantifiers, |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
84 |
"Trueprop" and ?P stripped away) delivers the head *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
85 |
fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
86 |
extract_hd (Const("Trueprop",_) $ r) = extract_hd r | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
87 |
extract_hd (Var(_,_) $ r) = extract_hd r | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
88 |
extract_hd (a $ b) = extract_hd a | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
89 |
extract_hd (Const(s,_)) = s | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
90 |
extract_hd _ = raise malformed; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
91 |
(* 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
|
92 |
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
|
93 |
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
|
94 |
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
|
95 |
extract_constr _ _ = raise malformed; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
96 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
97 |
(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
|
98 |
end; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
99 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
100 |
(* delivering list of constructor terms of a datatype *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
101 |
fun constr_list thy atyp = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
102 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
103 |
fun act_name thy (Type(s,_)) = s | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
104 |
act_name _ s = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
105 |
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
|
106 |
fun afpl ("." :: a) = [] | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
107 |
afpl [] = [] | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
108 |
afpl (a::r) = a :: (afpl r); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
109 |
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
|
110 |
val q_atypstr = act_name thy atyp; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
111 |
val uq_atypstr = unqualify q_atypstr; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
112 |
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
|
113 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
114 |
extract_constrs thy prem |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
115 |
handle malformed => |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
116 |
error("malformed theorem : " ^ uq_atypstr ^ ".induct") |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
117 |
end; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
118 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
119 |
fun check_for_constr thy atyp (a $ b) = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
120 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
121 |
fun all_free (Free(_,_)) = true | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
122 |
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
|
123 |
all_free _ = false; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
124 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
125 |
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
|
126 |
end | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
127 |
check_for_constr thy atyp (Const(a,_)) = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
128 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
129 |
val cl = constr_list thy atyp; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
130 |
fun fstmem a [] = false | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
131 |
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
|
132 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
133 |
if (fstmem a cl) then true else false |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
134 |
end | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
135 |
check_for_constr _ _ _ = false; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
136 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
137 |
(* delivering the free variables of a constructor term *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
138 |
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
|
139 |
free_vars_of (Const(_,_)) = [] | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
140 |
free_vars_of (Free(a,_)) = [a] | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
141 |
free_vars_of _ = raise malformed; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
142 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
143 |
(* 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
|
144 |
fun constr_set_string thy atyp ctstr = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
145 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
146 |
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
|
147 |
val l = free_vars_of trm |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
148 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
149 |
if (check_for_constr thy atyp trm) then |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
150 |
(if (l=[]) then ("{" ^ ctstr ^ "}") |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
151 |
else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})") |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
152 |
else (raise malformed) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
153 |
handle malformed => |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
154 |
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
|
155 |
end; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
156 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
157 |
(* extracting constructor heads *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
158 |
fun constructor_head thy atypstr s = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
159 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
160 |
fun hd_of (Const(a,_)) = a | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
161 |
hd_of (t $ _) = hd_of t | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
162 |
hd_of _ = raise malformed; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
163 |
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
|
164 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
165 |
hd_of trm handle malformed => |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
166 |
error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
167 |
end; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
168 |
fun constructor_head_list _ _ [] = [] | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
169 |
constructor_head_list thy atypstr (a::r) = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
170 |
(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
|
171 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
172 |
(* producing an action set *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
173 |
fun action_set_string thy atyp [] = "{}" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
174 |
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
|
175 |
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
|
176 |
" Un " ^ (action_set_string thy atyp r); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
177 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
178 |
(* used by extend *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
179 |
fun pstr s [] = "(" ^ s ^ "' = " ^ s ^ ")" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
180 |
pstr s ((a,b)::r) = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
181 |
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
|
182 |
fun poststring [] l = "" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
183 |
poststring [(a,b)] l = pstr a l | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
184 |
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
|
185 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
186 |
(* 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
|
187 |
(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
|
188 |
(where bool indicates whether there is a precondition *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
189 |
fun extend thy atyp statetupel (actstr,r,[]) = |
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 |
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
|
192 |
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
|
193 |
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
|
194 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
195 |
if (check_for_constr thy atyp trm) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
196 |
then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
197 |
else |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
198 |
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
|
199 |
end | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
200 |
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
|
201 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
202 |
fun pseudo_poststring [] = "" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
203 |
pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
204 |
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
|
205 |
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
|
206 |
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
|
207 |
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
|
208 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
209 |
if (check_for_constr thy atyp trm) then |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
210 |
(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
|
211 |
(* the case with transrel *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
212 |
else |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
213 |
(trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)), |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
214 |
"(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag)) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
215 |
else |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
216 |
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
|
217 |
end; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
218 |
(* used by make_alt_string *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
219 |
fun extended_list _ _ _ [] = [] | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
220 |
extended_list thy atyp statetupel (a::r) = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
221 |
(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
|
222 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
223 |
(* used by write_alts *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
224 |
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
|
225 |
if (chead mem inp) then |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
226 |
( |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
227 |
error("Input action " ^ tr ^ " was not specified") |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
228 |
) else ( |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
229 |
if (chead mem (out@int)) then |
10203 | 230 |
(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
|
231 |
(tr ^ " => False",tr ^ " => False")) | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
232 |
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
|
233 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
234 |
fun hd_of (Const(a,_)) = a | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
235 |
hd_of (t $ _) = hd_of t | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
236 |
hd_of _ = raise malformed; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
237 |
fun occurs_again c [] = false | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
238 |
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
|
239 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
240 |
if (chead=(hd_of a)) then |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
241 |
(if ((chead mem inp) andalso e) then ( |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
242 |
error("Input action " ^ b ^ " has a precondition") |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
243 |
) else (if (chead mem (inp@out@int)) then |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
244 |
(if (occurs_again chead r) then ( |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
245 |
error("Two specifications for action: " ^ b) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
246 |
) else (b ^ " => " ^ c,b ^ " => " ^ d)) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
247 |
else ( |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
248 |
error("Action " ^ b ^ " is not in automaton signature") |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
249 |
))) 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
|
250 |
handle malformed => |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
251 |
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
|
252 |
end; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
253 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
254 |
(* used by make_alt_string *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
255 |
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
|
256 |
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
|
257 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
258 |
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
|
259 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
260 |
(a ^ (fst wa),b ^ (snd wa)) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
261 |
end | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
262 |
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
|
263 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
264 |
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
|
265 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
266 |
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
|
267 |
end; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
268 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
269 |
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
|
270 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
271 |
val cl = constr_list thy atyp; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
272 |
val ttr = extended_list thy atyp statetupel trans; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
273 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
274 |
write_alts thy ("","") inp out int cl ttr |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
275 |
end; |
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 |
(* used in gen_add_ioa *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
278 |
fun check_free_primed (Free(a,_)) = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
279 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
280 |
val (f::r) = rev(explode a) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
281 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
282 |
if (f="'") then [a] else [] |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
283 |
end | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
284 |
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
|
285 |
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
|
286 |
check_free_primed _ = []; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
287 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
288 |
fun overlap [] _ = true | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
289 |
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
|
290 |
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
|
291 |
) else (overlap r l); |
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 |
(* delivering some types of an automaton *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
294 |
fun aut_type_of thy aut_name = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
295 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
296 |
fun left_of (( _ $ left) $ _) = left | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
297 |
left_of _ = raise malformed; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
298 |
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
|
299 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
300 |
(#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
|
301 |
handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def") |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
302 |
end; |
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 |
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
|
305 |
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
|
306 |
(Sign.string_of_typ (sign_of thy) t)); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
307 |
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
|
308 |
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
|
309 |
(Sign.string_of_typ (sign_of thy) t)); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
310 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
311 |
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
|
312 |
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
|
313 |
comp_st_type_of _ _ = error "empty automaton list"; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
314 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
315 |
(* checking consistency of action types (for composition) *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
316 |
fun check_ac thy (a::r) = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
317 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
318 |
fun ch_f_a thy acttyp [] = acttyp | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
319 |
ch_f_a thy acttyp (a::r) = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
320 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
321 |
val auttyp = aut_type_of thy a; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
322 |
val ac = (act_type_of thy auttyp); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
323 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
324 |
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
|
325 |
end; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
326 |
val auttyp = aut_type_of thy a; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
327 |
val acttyp = (act_type_of thy auttyp); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
328 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
329 |
ch_f_a thy acttyp r |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
330 |
end | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
331 |
check_ac _ [] = error "empty automaton list"; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
332 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
333 |
fun clist [] = "" | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
334 |
clist [a] = a | |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
335 |
clist (a::r) = a ^ " || " ^ (clist r); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
336 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
337 |
(* gen_add_ioa *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
338 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
339 |
fun gen_add_ioa prep_term automaton_name action_type inp out int statetupel ini trans thy = |
6508 | 340 |
(writeln("Constructing automaton " ^ automaton_name ^ " ..."); |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
341 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
342 |
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
|
343 |
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
|
344 |
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
|
345 |
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
|
346 |
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
|
347 |
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
|
348 |
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
|
349 |
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
|
350 |
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
|
351 |
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
|
352 |
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
|
353 |
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
|
354 |
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
|
355 |
atyp statetupel trans; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
356 |
val thy2 = (thy |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
357 |
|> ContConsts.add_consts |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
358 |
[(automaton_name ^ "_initial", "(" ^ state_type_string ^ ")set" ,NoSyn), |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
359 |
(automaton_name ^ "_asig", "(" ^ action_type ^ ")signature" ,NoSyn), |
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 |
"(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn), |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
362 |
(automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)] |
9317 | 363 |
|> (#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
|
364 |
[(automaton_name ^ "_initial_def", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
365 |
automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"), |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
366 |
(automaton_name ^ "_asig_def", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
367 |
automaton_name ^ "_asig == (" ^ |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
368 |
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
|
369 |
(automaton_name ^ "_trans_def", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
370 |
automaton_name ^ "_trans == {(" ^ |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
371 |
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
|
372 |
"). 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
|
373 |
(automaton_name ^ "_def", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
374 |
automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^ |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
375 |
"_initial, " ^ automaton_name ^ "_trans,{},{})") |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
376 |
]) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
377 |
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
|
378 |
( "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
|
379 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
380 |
( |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
381 |
if (chk_prime_list = []) then thy2 |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
382 |
else ( |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
383 |
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
|
384 |
^ (list_elements_of chk_prime_list))) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
385 |
) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
386 |
end) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
387 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
388 |
fun gen_add_composition prep_term automaton_name aut_list thy = |
6508 | 389 |
(writeln("Constructing automaton " ^ automaton_name ^ " ..."); |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
390 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
391 |
val acttyp = check_ac thy aut_list; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
392 |
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
|
393 |
val comp_list = clist aut_list; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
394 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
395 |
thy |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
396 |
|> ContConsts.add_consts_i |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
397 |
[(automaton_name, |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
398 |
Type("*", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
399 |
[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
|
400 |
Type("*",[Type("set",[st_typ]), |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
401 |
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
|
402 |
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
|
403 |
,NoSyn)] |
9317 | 404 |
|> (#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
|
405 |
[(automaton_name ^ "_def", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
406 |
automaton_name ^ " == " ^ comp_list)] |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
407 |
end) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
408 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
409 |
fun gen_add_restriction prep_term automaton_name aut_source actlist thy = |
6508 | 410 |
(writeln("Constructing automaton " ^ automaton_name ^ " ..."); |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
411 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
412 |
val auttyp = aut_type_of thy aut_source; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
413 |
val acttyp = act_type_of thy auttyp; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
414 |
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
|
415 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
416 |
thy |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
417 |
|> ContConsts.add_consts_i |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
418 |
[(automaton_name, auttyp,NoSyn)] |
9317 | 419 |
|> (#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
|
420 |
[(automaton_name ^ "_def", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
421 |
automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
422 |
end) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
423 |
fun gen_add_hiding prep_term automaton_name aut_source actlist thy = |
6508 | 424 |
(writeln("Constructing automaton " ^ automaton_name ^ " ..."); |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
425 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
426 |
val auttyp = aut_type_of thy aut_source; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
427 |
val acttyp = act_type_of thy auttyp; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
428 |
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
|
429 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
430 |
thy |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
431 |
|> ContConsts.add_consts_i |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
432 |
[(automaton_name, auttyp,NoSyn)] |
9317 | 433 |
|> (#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
|
434 |
[(automaton_name ^ "_def", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
435 |
automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
436 |
end) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
437 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
438 |
fun ren_act_type_of thy funct = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
439 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
440 |
(* 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
|
441 |
val _ = goal thy (funct ^ " = t"); |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
442 |
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
|
443 |
arg_typ_of _ = raise malformed; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
444 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
445 |
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
|
446 |
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
|
447 |
end; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
448 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
449 |
fun gen_add_rename prep_term automaton_name aut_source fun_name thy = |
6508 | 450 |
(writeln("Constructing automaton " ^ automaton_name ^ " ..."); |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
451 |
let |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
452 |
val auttyp = aut_type_of thy aut_source; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
453 |
val st_typ = st_type_of thy auttyp; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
454 |
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
|
455 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
456 |
thy |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
457 |
|> ContConsts.add_consts_i |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
458 |
[(automaton_name, |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
459 |
Type("*", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
460 |
[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
|
461 |
Type("*",[Type("set",[st_typ]), |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
462 |
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
|
463 |
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
|
464 |
,NoSyn)] |
9317 | 465 |
|> (#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
|
466 |
[(automaton_name ^ "_def", |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
467 |
automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")] |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
468 |
end) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
469 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
470 |
(* external interfaces *) |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
471 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
472 |
fun read_term sg str = |
8100 | 473 |
read_cterm sg (str, HOLogic.termT); |
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
474 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
475 |
fun cert_term sg tm = |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
476 |
cterm_of sg tm handle TERM (msg, _) => error msg; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
477 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
478 |
in |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
479 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
480 |
val add_ioa = gen_add_ioa read_term; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
481 |
val add_ioa_i = gen_add_ioa cert_term; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
482 |
val add_composition = gen_add_composition read_term; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
483 |
val add_composition_i = gen_add_composition cert_term; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
484 |
val add_hiding = gen_add_hiding read_term; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
485 |
val add_hiding_i = gen_add_hiding cert_term; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
486 |
val add_restriction = gen_add_restriction read_term; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
487 |
val add_restriction_i = gen_add_restriction cert_term; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
488 |
val add_rename = gen_add_rename read_term; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
489 |
val add_rename_i = gen_add_rename cert_term; |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
490 |
|
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
491 |
end |
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
492 |
|
6508 | 493 |
|
494 |
||
495 |
(** outer syntax **) |
|
496 |
||
497 |
(* prepare results *) |
|
498 |
||
499 |
(*encoding transition specifications with a element of ParseTrans*) |
|
500 |
datatype ParseTrans = Rel of string | PP of string*(string*string)list; |
|
501 |
fun mk_trans_of_rel s = Rel(s); |
|
502 |
fun mk_trans_of_prepost (s,l) = PP(s,l); |
|
503 |
||
504 |
fun trans_of (a, Rel b) = (a, b, [("", "")]) |
|
505 |
| trans_of (a, PP (b, l)) = (a, b, l); |
|
506 |
||
507 |
||
508 |
fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) = |
|
509 |
add_ioa aut action_type inp out int states initial (map trans_of trans); |
|
510 |
||
511 |
fun mk_composition_decl (aut, autlist) = |
|
512 |
add_composition aut autlist; |
|
513 |
||
514 |
fun mk_hiding_decl (aut, (actlist, source_aut)) = |
|
515 |
add_hiding aut source_aut actlist; |
|
516 |
||
517 |
fun mk_restriction_decl (aut, (source_aut, actlist)) = |
|
518 |
add_restriction aut source_aut actlist; |
|
519 |
||
520 |
fun mk_rename_decl (aut, (source_aut, rename_f)) = |
|
521 |
add_rename aut source_aut rename_f; |
|
522 |
||
523 |
||
524 |
(* parsers *) |
|
525 |
||
6723 | 526 |
local structure P = OuterParse and K = OuterSyntax.Keyword in |
6508 | 527 |
|
6723 | 528 |
val actionlist = P.list1 P.term; |
529 |
val inputslist = P.$$$ "inputs" |-- actionlist; |
|
530 |
val outputslist = P.$$$ "outputs" |-- actionlist; |
|
531 |
val internalslist = P.$$$ "internals" |-- actionlist; |
|
532 |
val stateslist = P.$$$ "states" |-- Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ); |
|
533 |
val initial = P.$$$ "initially" |-- P.term; |
|
534 |
val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.term); |
|
535 |
val pre = P.$$$ "pre" |-- P.term; |
|
536 |
val post = P.$$$ "post" |-- assign_list; |
|
6508 | 537 |
val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost; |
538 |
val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost; |
|
6723 | 539 |
val transrel = (P.$$$ "transrel" |-- P.term) >> mk_trans_of_rel; |
540 |
val transition = P.term -- (transrel || pre1 || post1); |
|
541 |
val translist = P.$$$ "transitions" |-- Scan.repeat1 transition; |
|
6508 | 542 |
|
543 |
val ioa_decl = |
|
6723 | 544 |
(P.name -- (P.$$$ "=" |-- |
545 |
(P.$$$ "signature" |-- |
|
546 |
(P.$$$ "actions" |-- |
|
547 |
(P.typ -- |
|
6508 | 548 |
(Scan.optional inputslist []) -- |
549 |
(Scan.optional outputslist []) -- |
|
550 |
(Scan.optional internalslist []) -- |
|
551 |
stateslist -- |
|
552 |
(Scan.optional initial "True") -- |
|
553 |
translist))))) >> mk_ioa_decl || |
|
6723 | 554 |
(P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.list1 P.name))) >> mk_composition_decl || |
8733 | 555 |
(P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |-- P.list1 P.term -- (P.$$$ "in" |-- P.name)))) |
6723 | 556 |
>> mk_hiding_decl || |
557 |
(P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |-- P.name -- (P.$$$ "to" |-- P.list1 P.term)))) |
|
6508 | 558 |
>> mk_restriction_decl || |
7040 | 559 |
(P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- P.name -- (P.$$$ "using" |-- P.term)))) |
6723 | 560 |
>> mk_rename_decl; |
6508 | 561 |
|
6723 | 562 |
val automatonP = |
563 |
OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl |
|
564 |
(ioa_decl >> Toplevel.theory); |
|
6508 | 565 |
|
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset
|
566 |
end; |
6508 | 567 |
|
568 |
||
569 |
(* setup outer syntax *) |
|
570 |
||
571 |
val _ = OuterSyntax.add_keywords ["signature", "actions", "inputs", |
|
572 |
"outputs", "internals", "states", "initially", "transitions", "pre", |
|
8733 | 573 |
"post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to", |
7040 | 574 |
"rename", "using"]; |
6508 | 575 |
|
576 |
val _ = OuterSyntax.add_parsers [automatonP]; |
|
577 |
||
578 |
||
579 |
end; |