author  wenzelm 
Thu, 20 Mar 2008 00:20:44 +0100  
changeset 26343  0dd2eab7b296 
parent 26336  a0e2b706ce73 
child 26939  1035c89b4c02 
permissions  rwrr 
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$ 
18358  3 
Author: Tobias Hamberger, TU Muenchen 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

4 
*) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

5 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

6 
signature IOA_PACKAGE = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

7 
sig 
18358  8 
val add_ioa: string > string 
9 
> (string) list > (string) list > (string) list 

10 
> (string * string) list > string 

11 
> (string * string * (string * string)list) list 

12 
> theory > theory 

13 
val add_composition : string > (string)list > theory > theory 

14 
val add_hiding : string > string > (string)list > theory > theory 

15 
val add_restriction : string > string > (string)list > theory > theory 

16 
val add_rename : string > string > string > theory > theory 

6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

17 
end; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

18 

6508  19 
structure IoaPackage: IOA_PACKAGE = 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

20 
struct 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

21 

24634  22 
val string_of_typ = PrintMode.setmp [] o Sign.string_of_typ; 
23 
val string_of_term = PrintMode.setmp [] o Sign.string_of_term; 

17243
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

24 

6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

25 
exception malformed; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

26 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

27 
(* stripping quotes *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

28 
fun strip [] = []  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

29 
strip ("\""::r) = strip r  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

30 
strip (a::r) = a :: (strip r); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

31 
fun strip_quote s = implode(strip(explode(s))); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

32 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

33 
(* used by *_of_varlist *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

34 
fun extract_first (a,b) = strip_quote a; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

35 
fun extract_second (a,b) = strip_quote b; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

36 
(* following functions producing sth from a varlist *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

37 
fun comma_list_of_varlist [] = ""  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

38 
comma_list_of_varlist [a] = extract_first a  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

39 
comma_list_of_varlist (a::r) = (extract_first a) ^ "," ^ (comma_list_of_varlist r); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

40 
fun primed_comma_list_of_varlist [] = ""  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

41 
primed_comma_list_of_varlist [a] = (extract_first a) ^ "'"  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

42 
primed_comma_list_of_varlist (a::r) = (extract_first a) ^ "'," ^ 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

43 
(primed_comma_list_of_varlist r); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

44 
fun type_product_of_varlist [] = ""  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

45 
type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")"  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

46 
type_product_of_varlist(a::r) = "(" ^ extract_second(a) ^ ")*" ^ type_product_of_varlist r; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

47 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

48 
(* listing a list *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

49 
fun list_elements_of [] = ""  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

50 
list_elements_of (a::r) = a ^ " " ^ (list_elements_of r); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

51 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

52 
(* extracting type parameters from a type list *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

53 
(* fun param_tupel thy [] res = res  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

54 
param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

55 
param_tupel thy ((TFree(a,_))::r) res = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

56 
if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res))  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

57 
param_tupel thy (a::r) res = 
22578  58 
error ("one component of a statetype is a TVar: " ^ (string_of_typ thy a)); 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

59 
*) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

60 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

61 
(* used by constr_list *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

62 
fun extract_constrs thy [] = []  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

63 
extract_constrs thy (a::r) = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

64 
let 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

65 
fun delete_bold [] = [] 
18443  66 
 delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs)) 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

67 
then (let val (_::_::_::s) = xs in delete_bold s end) 
18443  68 
else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs)) 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

69 
then (let val (_::_::_::s) = xs in delete_bold s end) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

70 
else (x::delete_bold xs)); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

71 
fun delete_bold_string s = implode(delete_bold(explode s)); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

72 
(* from a constructor term in *.induct (with quantifiers, 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

73 
"Trueprop" and ?P stripped away) delivers the head *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

74 
fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

75 
extract_hd (Const("Trueprop",_) $ r) = extract_hd r  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

76 
extract_hd (Var(_,_) $ r) = extract_hd r  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

77 
extract_hd (a $ b) = extract_hd a  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

78 
extract_hd (Const(s,_)) = s  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

79 
extract_hd _ = raise malformed; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

80 
(* delivers constructor term string from a prem of *.induct *) 
20194  81 
fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r))) 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

82 
extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r  
22578  83 
extract_constr thy (Var(_,_) $ r) = delete_bold_string(string_of_term thy r)  
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

84 
extract_constr _ _ = raise malformed; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

85 
in 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

86 
(extract_hd a,extract_constr thy a) :: (extract_constrs thy r) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

87 
end; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

88 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

89 
(* delivering list of constructor terms of a datatype *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

90 
fun constr_list thy atyp = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

91 
let 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

92 
fun act_name thy (Type(s,_)) = s  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

93 
act_name _ s = 
22578  94 
error("malformed action type: " ^ (string_of_typ thy s)); 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

95 
fun afpl ("." :: a) = []  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

96 
afpl [] = []  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

97 
afpl (a::r) = a :: (afpl r); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

98 
fun unqualify s = implode(rev(afpl(rev(explode s)))); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

99 
val q_atypstr = act_name thy atyp; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

100 
val uq_atypstr = unqualify q_atypstr; 
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

101 
val prem = prems_of (PureThy.get_thm thy (uq_atypstr ^ ".induct")); 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

102 
in 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

103 
extract_constrs thy prem 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

104 
handle malformed => 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

105 
error("malformed theorem : " ^ uq_atypstr ^ ".induct") 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

106 
end; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

107 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

108 
fun check_for_constr thy atyp (a $ b) = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

109 
let 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

110 
fun all_free (Free(_,_)) = true  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

111 
all_free (a $ b) = if (all_free a) then (all_free b) else false  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

112 
all_free _ = false; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

113 
in 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

114 
if (all_free b) then (check_for_constr thy atyp a) else false 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

115 
end  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

116 
check_for_constr thy atyp (Const(a,_)) = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

117 
let 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

118 
val cl = constr_list thy atyp; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

119 
fun fstmem a [] = false  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

120 
fstmem a ((f,s)::r) = if (a=f) then true else (fstmem a r) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

121 
in 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

122 
if (fstmem a cl) then true else false 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

123 
end  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

124 
check_for_constr _ _ _ = false; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

125 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

126 
(* delivering the free variables of a constructor term *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

127 
fun free_vars_of (t1 $ t2) = (free_vars_of t1) @ (free_vars_of t2)  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

128 
free_vars_of (Const(_,_)) = []  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

129 
free_vars_of (Free(a,_)) = [a]  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

130 
free_vars_of _ = raise malformed; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

131 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

132 
(* making a constructor set from a constructor term (of signature) *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

133 
fun constr_set_string thy atyp ctstr = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

134 
let 
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22578
diff
changeset

135 
val trm = Sign.simple_read_term thy atyp ctstr; 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

136 
val l = free_vars_of trm 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

137 
in 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

138 
if (check_for_constr thy atyp trm) then 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

139 
(if (l=[]) then ("{" ^ ctstr ^ "}") 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

140 
else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})") 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

141 
else (raise malformed) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

142 
handle malformed => 
22578  143 
error("malformed action term: " ^ (string_of_term thy trm)) 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

144 
end; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

145 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

146 
(* extracting constructor heads *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

147 
fun constructor_head thy atypstr s = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

148 
let 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

149 
fun hd_of (Const(a,_)) = a  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

150 
hd_of (t $ _) = hd_of t  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

151 
hd_of _ = raise malformed; 
24707  152 
val trm = Sign.simple_read_term thy (Syntax.read_typ_global thy atypstr) s; 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

153 
in 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

154 
hd_of trm handle malformed => 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

155 
error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

156 
end; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

157 
fun constructor_head_list _ _ [] = []  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

158 
constructor_head_list thy atypstr (a::r) = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

159 
(constructor_head thy atypstr a)::(constructor_head_list thy atypstr r); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

160 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

161 
(* producing an action set *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

162 
fun action_set_string thy atyp [] = "{}"  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

163 
action_set_string thy atyp [a] = constr_set_string thy atyp (strip_quote a)  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

164 
action_set_string thy atyp (a::r) = (constr_set_string thy atyp (strip_quote a)) ^ 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

165 
" Un " ^ (action_set_string thy atyp r); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

166 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

167 
(* used by extend *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

168 
fun pstr s [] = "(" ^ s ^ "' = " ^ s ^ ")"  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

169 
pstr s ((a,b)::r) = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

170 
if (s=a) then ("(" ^ s ^ "' = (" ^ b ^ "))") else (pstr s r); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

171 
fun poststring [] l = ""  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

172 
poststring [(a,b)] l = pstr a l  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

173 
poststring ((a,b)::r) l = (pstr a l) ^ " & " ^ (poststring r l); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

174 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

175 
(* extends a (action string,condition,assignlist) tupel by a 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

176 
(action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

177 
(where bool indicates whether there is a precondition *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

178 
fun extend thy atyp statetupel (actstr,r,[]) = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

179 
let 
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22578
diff
changeset

180 
val trm = Sign.simple_read_term thy atyp actstr; 
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22578
diff
changeset

181 
val rtrm = Sign.simple_read_term thy (Type("bool",[])) r; 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

182 
val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

183 
in 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

184 
if (check_for_constr thy atyp trm) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

185 
then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

186 
else 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

187 
error("transition " ^ actstr ^ " is not a pure constructor term") 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

188 
end  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

189 
extend thy atyp statetupel (actstr,r,(a,b)::c) = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

190 
let 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

191 
fun pseudo_poststring [] = ""  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

192 
pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))"  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

193 
pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); 
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22578
diff
changeset

194 
val trm = Sign.simple_read_term thy atyp actstr; 
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22578
diff
changeset

195 
val rtrm = Sign.simple_read_term thy (Type("bool",[])) r; 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

196 
val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

197 
in 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

198 
if (check_for_constr thy atyp trm) then 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

199 
(if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

200 
(* the case with transrel *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

201 
else 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

202 
(trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)), 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

203 
"(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag)) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

204 
else 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

205 
error("transition " ^ actstr ^ " is not a pure constructor term") 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

206 
end; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

207 
(* used by make_alt_string *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

208 
fun extended_list _ _ _ [] = []  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

209 
extended_list thy atyp statetupel (a::r) = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

210 
(extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

211 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

212 
(* used by write_alts *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

213 
fun write_alt thy (chead,tr) inp out int [] = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

214 
if (chead mem inp) then 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

215 
( 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

216 
error("Input action " ^ tr ^ " was not specified") 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

217 
) else ( 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

218 
if (chead mem (out@int)) then 
10203  219 
(writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else (); 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

220 
(tr ^ " => False",tr ^ " => False"))  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

221 
write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

222 
let 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

223 
fun hd_of (Const(a,_)) = a  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

224 
hd_of (t $ _) = hd_of t  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

225 
hd_of _ = raise malformed; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

226 
fun occurs_again c [] = false  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

227 
occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

228 
in 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

229 
if (chead=(hd_of a)) then 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

230 
(if ((chead mem inp) andalso e) then ( 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

231 
error("Input action " ^ b ^ " has a precondition") 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

232 
) else (if (chead mem (inp@out@int)) then 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

233 
(if (occurs_again chead r) then ( 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

234 
error("Two specifications for action: " ^ b) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

235 
) else (b ^ " => " ^ c,b ^ " => " ^ d)) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

236 
else ( 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

237 
error("Action " ^ b ^ " is not in automaton signature") 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

238 
))) else (write_alt thy (chead,ctrm) inp out int r) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

239 
handle malformed => 
22578  240 
error ("malformed action term: " ^ (string_of_term thy a)) 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

241 
end; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

242 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

243 
(* used by make_alt_string *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

244 
fun write_alts thy (a,b) inp out int [] ttr = (a,b)  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

245 
write_alts thy (a,b) inp out int [c] ttr = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

246 
let 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

247 
val wa = write_alt thy c inp out int ttr 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

248 
in 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

249 
(a ^ (fst wa),b ^ (snd wa)) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

250 
end  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

251 
write_alts thy (a,b) inp out int (c::r) ttr = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

252 
let 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

253 
val wa = write_alt thy c inp out int ttr 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

254 
in 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

255 
write_alts thy (a ^ (fst wa) ^ "  ", b ^ (snd wa) ^ "  ") inp out int r ttr 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

256 
end; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

257 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

258 
fun make_alt_string thy inp out int atyp statetupel trans = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

259 
let 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

260 
val cl = constr_list thy atyp; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

261 
val ttr = extended_list thy atyp statetupel trans; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

262 
in 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

263 
write_alts thy ("","") inp out int cl ttr 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

264 
end; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

265 

12339  266 
(* used in add_ioa *) 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

267 
fun check_free_primed (Free(a,_)) = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

268 
let 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

269 
val (f::r) = rev(explode a) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

270 
in 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

271 
if (f="'") then [a] else [] 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

272 
end  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

273 
check_free_primed (a $ b) = ((check_free_primed a) @ (check_free_primed b))  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

274 
check_free_primed (Abs(_,_,t)) = check_free_primed t  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

275 
check_free_primed _ = []; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

276 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

277 
fun overlap [] _ = true  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

278 
overlap (a::r) l = if (a mem l) then ( 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

279 
error("Two occurences of action " ^ a ^ " in automaton signature") 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

280 
) else (overlap r l); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

281 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

282 
(* delivering some types of an automaton *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

283 
fun aut_type_of thy aut_name = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

284 
let 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

285 
fun left_of (( _ $ left) $ _) = left  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

286 
left_of _ = raise malformed; 
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset

287 
val aut_def = concl_of (PureThy.get_thm thy (aut_name ^ "_def")); 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

288 
in 
22578  289 
(#T(rep_cterm(cterm_of thy (left_of aut_def)))) 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

290 
handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def") 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

291 
end; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

292 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

293 
fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

294 
act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^ 
22578  295 
(string_of_typ thy t)); 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

296 
fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

297 
st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^ 
22578  298 
(string_of_typ thy t)); 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

299 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

300 
fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a)  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

301 
comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r])  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

302 
comp_st_type_of _ _ = error "empty automaton list"; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

303 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

304 
(* checking consistency of action types (for composition) *) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

305 
fun check_ac thy (a::r) = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

306 
let 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

307 
fun ch_f_a thy acttyp [] = acttyp  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

308 
ch_f_a thy acttyp (a::r) = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

309 
let 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

310 
val auttyp = aut_type_of thy a; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

311 
val ac = (act_type_of thy auttyp); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

312 
in 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

313 
if (ac=acttyp) then (ch_f_a thy acttyp r) else (error "A") 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

314 
end; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

315 
val auttyp = aut_type_of thy a; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

316 
val acttyp = (act_type_of thy auttyp); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

317 
in 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

318 
ch_f_a thy acttyp r 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

319 
end  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

320 
check_ac _ [] = error "empty automaton list"; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

321 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

322 
fun clist [] = ""  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

323 
clist [a] = a  
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

324 
clist (a::r) = a ^ "  " ^ (clist r); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

325 

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); 
24707  333 
val styp = Syntax.read_typ_global thy state_type_string; 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

334 
val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")"; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

335 
val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")"; 
24707  336 
val atyp = Syntax.read_typ_global thy action_type; 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

337 
val inp_set_string = action_set_string thy atyp inp; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

338 
val out_set_string = action_set_string thy atyp out; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

339 
val int_set_string = action_set_string thy atyp int; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

340 
val inp_head_list = constructor_head_list thy action_type inp; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

341 
val out_head_list = constructor_head_list thy action_type out; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

342 
val int_head_list = constructor_head_list thy action_type int; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

343 
val overlap_flag = ((overlap inp out) andalso (overlap inp int) andalso (overlap out int)); 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

344 
val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

345 
atyp statetupel trans; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

346 
val thy2 = (thy 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

347 
> ContConsts.add_consts 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

348 
[(automaton_name ^ "_initial", "(" ^ state_type_string ^ ")set" ,NoSyn), 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

349 
(automaton_name ^ "_asig", "(" ^ action_type ^ ")signature" ,NoSyn), 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

350 
(automaton_name ^ "_trans", 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

351 
"(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn), 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

352 
(automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)] 
18358  353 
> (snd oo (PureThy.add_defs false o map Thm.no_attributes)) 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

354 
[(automaton_name ^ "_initial_def", 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

355 
automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"), 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

356 
(automaton_name ^ "_asig_def", 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

357 
automaton_name ^ "_asig == (" ^ 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

358 
inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"), 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

359 
(automaton_name ^ "_trans_def", 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

360 
automaton_name ^ "_trans == {(" ^ 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

361 
state_vars_tupel ^ ", act_of_" ^ automaton_name ^ ", " ^ state_vars_primed ^ 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

362 
"). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"), 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

363 
(automaton_name ^ "_def", 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

364 
automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^ 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

365 
"_initial, " ^ automaton_name ^ "_trans,{},{})") 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

366 
]) 
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22578
diff
changeset

367 
val chk_prime_list = (check_free_primed (Sign.simple_read_term thy2 (Type("bool",[])) 
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22578
diff
changeset

368 
( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string)))) 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

369 
in 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

370 
( 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

371 
if (chk_prime_list = []) then thy2 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

372 
else ( 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

373 
error("Precondition or assignment terms in postconditions contain following primed variables:\n" 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

374 
^ (list_elements_of chk_prime_list))) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

375 
) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

376 
end) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

377 

12339  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)] 
18358  394 
> (snd oo (PureThy.add_defs false o map Thm.no_attributes)) 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

395 
[(automaton_name ^ "_def", 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

396 
automaton_name ^ " == " ^ comp_list)] 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

397 
end) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

398 

12339  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)] 
18358  409 
> (snd oo (PureThy.add_defs false o map Thm.no_attributes)) 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

410 
[(automaton_name ^ "_def", 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

411 
automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

412 
end) 
12339  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)] 
18358  423 
> (snd oo (PureThy.add_defs false o map Thm.no_attributes)) 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

424 
[(automaton_name ^ "_def", 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

425 
automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

426 
end) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

427 

863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

428 
fun ren_act_type_of thy funct = 
24707  429 
(case Term.fastype_of (Syntax.read_term_global thy funct) of 
17925  430 
Type ("fun", [a, b]) => a 
431 
 _ => error "could not extract argument type of renaming function term"); 

6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

432 

12339  433 
fun add_rename automaton_name aut_source fun_name thy = 
6508  434 
(writeln("Constructing automaton " ^ automaton_name ^ " ..."); 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

435 
let 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

436 
val auttyp = aut_type_of thy aut_source; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

437 
val st_typ = st_type_of thy auttyp; 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

438 
val acttyp = ren_act_type_of thy fun_name 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

439 
in 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

440 
thy 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

441 
> ContConsts.add_consts_i 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

442 
[(automaton_name, 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

443 
Type("*", 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

444 
[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]), 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

445 
Type("*",[Type("set",[st_typ]), 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

446 
Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

447 
Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

448 
,NoSyn)] 
18358  449 
> (snd oo (PureThy.add_defs false o map Thm.no_attributes)) 
6467
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

450 
[(automaton_name ^ "_def", 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

451 
automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")] 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

452 
end) 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

453 

6508  454 

455 
(** outer syntax **) 

456 

457 
(* prepare results *) 

458 

459 
(*encoding transition specifications with a element of ParseTrans*) 

460 
datatype ParseTrans = Rel of string  PP of string*(string*string)list; 

461 
fun mk_trans_of_rel s = Rel(s); 

462 
fun mk_trans_of_prepost (s,l) = PP(s,l); 

463 

464 
fun trans_of (a, Rel b) = (a, b, [("", "")]) 

465 
 trans_of (a, PP (b, l)) = (a, b, l); 

466 

467 

468 
fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) = 

469 
add_ioa aut action_type inp out int states initial (map trans_of trans); 

470 

471 
fun mk_composition_decl (aut, autlist) = 

472 
add_composition aut autlist; 

473 

474 
fun mk_hiding_decl (aut, (actlist, source_aut)) = 

475 
add_hiding aut source_aut actlist; 

476 

477 
fun mk_restriction_decl (aut, (source_aut, actlist)) = 

478 
add_restriction aut source_aut actlist; 

479 

480 
fun mk_rename_decl (aut, (source_aut, rename_f)) = 

481 
add_rename aut source_aut rename_f; 

482 

483 

24867  484 
(* outer syntax *) 
6508  485 

17057  486 
local structure P = OuterParse and K = OuterKeyword in 
6508  487 

24867  488 
val _ = OuterSyntax.keywords ["signature", "actions", "inputs", 
489 
"outputs", "internals", "states", "initially", "transitions", "pre", 

490 
"post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to", 

491 
"rename"]; 

492 

6723  493 
val actionlist = P.list1 P.term; 
17243
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

494 
val inputslist = P.$$$ "inputs"  P.!!! actionlist; 
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

495 
val outputslist = P.$$$ "outputs"  P.!!! actionlist; 
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

496 
val internalslist = P.$$$ "internals"  P.!!! actionlist; 
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

497 
val stateslist = P.$$$ "states"  P.!!! (Scan.repeat1 (P.name  P.$$$ "::"  P.typ)); 
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

498 
val initial = P.$$$ "initially"  P.!!! P.term; 
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

499 
val assign_list = P.list1 (P.name  P.$$$ ":="  P.!!! P.term); 
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

500 
val pre = P.$$$ "pre"  P.!!! P.term; 
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

501 
val post = P.$$$ "post"  P.!!! assign_list; 
6508  502 
val pre1 = (pre  (Scan.optional post [])) >> mk_trans_of_prepost; 
503 
val post1 = ((Scan.optional pre "True")  post) >> mk_trans_of_prepost; 

17243
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

504 
val transrel = (P.$$$ "transrel"  P.!!! P.term) >> mk_trans_of_rel; 
6723  505 
val transition = P.term  (transrel  pre1  post1); 
17243
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

506 
val translist = P.$$$ "transitions"  P.!!! (Scan.repeat1 transition); 
6508  507 

508 
val ioa_decl = 

6723  509 
(P.name  (P.$$$ "="  
510 
(P.$$$ "signature"  

17243
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

511 
P.!!! (P.$$$ "actions"  
6723  512 
(P.typ  
6508  513 
(Scan.optional inputslist [])  
514 
(Scan.optional outputslist [])  

515 
(Scan.optional internalslist [])  

516 
stateslist  

517 
(Scan.optional initial "True")  

518 
translist))))) >> mk_ioa_decl  

17243
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

519 
(P.name  (P.$$$ "="  (P.$$$ "compose"  P.!!! (P.list1 P.name)))) 
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

520 
>> mk_composition_decl  
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

521 
(P.name  (P.$$$ "="  (P.$$$ "hide_action"  
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

522 
P.!!! (P.list1 P.term  (P.$$$ "in"  P.name))))) >> mk_hiding_decl  
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

523 
(P.name  (P.$$$ "="  (P.$$$ "restrict"  
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

524 
P.!!! (P.name  (P.$$$ "to"  P.list1 P.term))))) >> mk_restriction_decl  
c4ff384ee28f
setmp print_mode []; more robust outer syntax; tuned;
wenzelm
parents:
17057
diff
changeset

525 
(P.name  (P.$$$ "="  (P.$$$ "rename"  (P.!!! (P.name  (P.$$$ "to"  P.term)))))) 
6723  526 
>> mk_rename_decl; 
6508  527 

24867  528 
val _ = 
6723  529 
OuterSyntax.command "automaton" "define Lynch/Vaandragerstyle 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 
end; 