author  wenzelm 
Mon, 24 May 1999 21:57:13 +0200  
changeset 6723  f342449d73ca 
parent 6508  b8a1e395edd7 
child 7040  613724c2ee6b 
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$ 
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 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

230 
(writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else print(""); 
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)] 
6508  363 
> (PureThy.add_defs o map Thm.no_attributes) (* old: Attributes.none *) 
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)] 
6508  404 
> (PureThy.add_defs 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)] 
6508  419 
> (PureThy.add_defs 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)] 
6508  433 
> (PureThy.add_defs 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 pseudoproofstate 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)] 
6508  465 
> (PureThy.add_defs 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 = 
863834a37769
added frontend syntax for IOA, moved trivial examples to folder ex;
mueller
parents:
diff
changeset

473 
read_cterm sg (str, HOLogic.termTVar); 
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  
555 
(P.name  (P.$$$ "="  (P.$$$ "hide"  P.list1 P.term  (P.$$$ "in"  P.name)))) 

556 
>> mk_hiding_decl  

557 
(P.name  (P.$$$ "="  (P.$$$ "restrict"  P.name  (P.$$$ "to"  P.list1 P.term)))) 

6508  558 
>> mk_restriction_decl  
6723  559 
(P.name  (P.$$$ "="  (P.$$$ "rename"  P.name  (P.$$$ "with"  P.term)))) 
560 
>> mk_rename_decl; 

6508  561 

6723  562 
val automatonP = 
563 
OuterSyntax.command "automaton" "define Lynch/Vaandragerstyle 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", 

573 
"post", "transrel", ":=", "compose", "hide", "in", "restrict", "to", 

574 
"rename", "with"]; 

575 

576 
val _ = OuterSyntax.add_parsers [automatonP]; 

577 

578 

579 
end; 