author  wenzelm 
Sat, 09 Jul 2011 21:53:27 +0200  
changeset 43721  fad8634cee62 
parent 42364  8c674b3b8e44 
permissions  rwrr 
23175  1 
(* Title: Tools/IsaPlanner/rw_tools.ML 
23171  2 
Author: Lucas Dixon, University of Edinburgh 
3 

23175  4 
Term related tools used for rewriting. 
23171  5 
*) 
6 

7 
signature RWTOOLS = 

8 
sig 

9 
end; 

10 

11 
structure RWTools 

12 
= struct 

13 

14 
(* fake free variable names for locally bound variables  these work 

15 
as placeholders. *) 

16 

17 
(* don't use dest_fake..  we should instead be working with numbers 

18 
and a list... else we rely on naming conventions which can break, or 

19 
be violated  in contrast list locations are correct by 

20 
construction/definition. *) 

21 
(* 

22 
fun dest_fake_bound_name n = 

40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
30161
diff
changeset

23 
case (raw_explode n) of (* FIXME Symbol.explode (?) *) 
23171  24 
(":" :: realchars) => implode realchars 
25 
 _ => n; *) 

40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
30161
diff
changeset

26 
fun is_fake_bound_name n = (hd (raw_explode n) = ":"); (* FIXME Symbol.explode (?) *) 
23171  27 
fun mk_fake_bound_name n = ":b_" ^ n; 
28 

29 

30 

31 
(* fake free variable names for local meta variables  these work 

32 
as placeholders. *) 

33 
fun dest_fake_fix_name n = 

40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
30161
diff
changeset

34 
case (raw_explode n) of (* FIXME Symbol.explode (?) *) 
23171  35 
("@" :: realchars) => implode realchars 
36 
 _ => n; 

40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
30161
diff
changeset

37 
fun is_fake_fix_name n = (hd (raw_explode n) = "@"); (* FIXME Symbol.explode (?) *) 
23171  38 
fun mk_fake_fix_name n = "@" ^ n; 
39 

40 

41 

42 
(* fake free variable names for meta level bound variables *) 

43 
fun dest_fake_all_name n = 

40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
30161
diff
changeset

44 
case (raw_explode n) of (* FIXME Symbol.explode (?) *) 
23171  45 
("+" :: realchars) => implode realchars 
46 
 _ => n; 

40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
30161
diff
changeset

47 
fun is_fake_all_name n = (hd (raw_explode n) = "+"); (* FIXME Symbol.explode (?) *) 
23171  48 
fun mk_fake_all_name n = "+" ^ n; 
49 

50 

51 

52 

53 
(* Ys and Ts not used, Ns are real names of faked local bounds, the 

54 
idea is that this will be mapped to free variables thus if a free 

55 
variable is a faked local bound then we change it to being a meta 

56 
variable so that it can later be instantiated *) 

57 
(* FIXME: rename this  avoid the word fix! *) 

58 
(* note we are not really "fix"'ing the free, more like making it variable! *) 

59 
(* fun trymkvar_of_fakefree (Ns, Ts) Ys (n,ty) = 

60 
if n mem Ns then Var((n,0),ty) else Free (n,ty); 

61 
*) 

62 

63 
(* make a var into a fixed free (ie prefixed with "@") *) 

64 
fun mk_fakefixvar Ts ((n,i),ty) = Free(mk_fake_fix_name n, ty); 

65 

66 

67 
(* mk_frees_bound: string list > Term.term > Term.term *) 

68 
(* This function changes free variables to being represented as bound 

69 
variables if the free's variable name is in the given list. The debruijn 

70 
index is simply the position in the list *) 

71 
(* THINKABOUT: danger of an existing free variable with the same name: fix 

72 
this so that name conflict are avoided automatically! In the meantime, 

73 
don't have free variables named starting with a ":" *) 

74 
fun bounds_of_fakefrees Ys (a $ b) = 

75 
(bounds_of_fakefrees Ys a) $ (bounds_of_fakefrees Ys b) 

76 
 bounds_of_fakefrees Ys (Abs(n,ty,t)) = 

77 
Abs(n,ty, bounds_of_fakefrees (n::Ys) t) 

78 
 bounds_of_fakefrees Ys (Free (n,ty)) = 

79 
let fun try_mk_bound_of_free (i,[]) = Free (n,ty) 

80 
 try_mk_bound_of_free (i,(y::ys)) = 

81 
if n = y then Bound i else try_mk_bound_of_free (i+1,ys) 

82 
in try_mk_bound_of_free (0,Ys) end 

83 
 bounds_of_fakefrees Ys t = t; 

84 

85 

86 
(* map a function f onto each free variables *) 

87 
fun map_to_frees f Ys (a $ b) = 

88 
(map_to_frees f Ys a) $ (map_to_frees f Ys b) 

89 
 map_to_frees f Ys (Abs(n,ty,t)) = 

90 
Abs(n,ty, map_to_frees f ((n,ty)::Ys) t) 

91 
 map_to_frees f Ys (Free a) = 

92 
f Ys a 

93 
 map_to_frees f Ys t = t; 

94 

95 

96 
(* map a function f onto each meta variable *) 

97 
fun map_to_vars f Ys (a $ b) = 

98 
(map_to_vars f Ys a) $ (map_to_vars f Ys b) 

99 
 map_to_vars f Ys (Abs(n,ty,t)) = 

100 
Abs(n,ty, map_to_vars f ((n,ty)::Ys) t) 

101 
 map_to_vars f Ys (Var a) = 

102 
f Ys a 

103 
 map_to_vars f Ys t = t; 

104 

105 
(* map a function f onto each free variables *) 

106 
fun map_to_alls f (Const("all",allty) $ Abs(n,ty,t)) = 

107 
let val (n2,ty2) = f (n,ty) 

108 
in (Const("all",allty) $ Abs(n2,ty2,map_to_alls f t)) end 

109 
 map_to_alls f x = x; 

110 

111 
(* map a function f to each type variable in a term *) 

112 
(* implicit arg: term *) 

113 
fun map_to_term_tvars f = 

114 
Term.map_types (fn TVar(ix,ty) => f (ix,ty)  x => x); (* FIXME map_atyps !? *) 

115 

116 

117 

118 
(* what if a param desn't occur in the concl? think about! Note: This 

119 
simply fixes meta level univ bound vars as Frees. At the end, we will 

120 
change them back to schematic vars that will then unify 

121 
appropriactely, ie with unfake_vars *) 

122 
fun fake_concl_of_goal gt i = 

123 
let 

124 
val prems = Logic.strip_imp_prems gt 

42364  125 
val sgt = nth prems (i  1) 
23171  126 

127 
val tbody = Logic.strip_imp_concl (Term.strip_all_body sgt) 

128 
val tparams = Term.strip_all_vars sgt 

129 

130 
val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) 

131 
tparams 

132 
in 

133 
Term.subst_bounds (rev fakefrees,tbody) 

134 
end; 

135 

136 
(* what if a param desn't occur in the concl? think about! Note: This 

137 
simply fixes meta level univ bound vars as Frees. At the end, we will 

138 
change them back to schematic vars that will then unify 

139 
appropriactely, ie with unfake_vars *) 

140 
fun fake_goal gt i = 

141 
let 

142 
val prems = Logic.strip_imp_prems gt 

42364  143 
val sgt = nth prems (i  1) 
23171  144 

145 
val tbody = Term.strip_all_body sgt 

146 
val tparams = Term.strip_all_vars sgt 

147 

148 
val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) 

149 
tparams 

150 
in 

151 
Term.subst_bounds (rev fakefrees,tbody) 

152 
end; 

153 

154 

155 
(* hand written  for some reason the Isabelle version in drule is broken! 

156 
Example? something to do with Bin Yangs examples? 

157 
*) 

158 
fun rename_term_bvars ns (Abs(s,ty,t)) = 

159 
let val s2opt = Library.find_first (fn (x,y) => s = x) ns 

160 
in case s2opt of 

161 
NONE => (Abs(s,ty,rename_term_bvars ns t)) 

162 
 SOME (_,s2) => Abs(s2,ty, rename_term_bvars ns t) end 

163 
 rename_term_bvars ns (a$b) = 

164 
(rename_term_bvars ns a) $ (rename_term_bvars ns b) 

165 
 rename_term_bvars _ x = x; 

166 

167 
fun rename_thm_bvars ns th = 

168 
let val t = Thm.prop_of th 

169 
in Thm.rename_boundvars t (rename_term_bvars ns t) th end; 

170 

171 
(* Finish this to show how it breaks! (raises the exception): 

172 

173 
exception rename_thm_bvars_exp of ((string * string) list * Thm.thm) 

174 

175 
Drule.rename_bvars ns th 

176 
handle TERM _ => raise rename_thm_bvars_exp (ns, th); 

177 
*) 

178 

179 
end; 