1 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
2 (* Title: Pure/IsaPlanner/rw_tools.ML |
|
3 ID: $Id$ |
|
4 Author: Lucas Dixon, University of Edinburgh |
|
5 lucas.dixon@ed.ac.uk |
|
6 Created: 28 May 2004 |
|
7 *) |
|
8 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
9 (* DESCRIPTION: |
|
10 |
|
11 term related tools used for rewriting |
|
12 |
|
13 *) |
|
14 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
15 |
|
16 signature RWTOOLS = |
|
17 sig |
|
18 end; |
|
19 |
|
20 structure RWTools |
|
21 = struct |
|
22 |
|
23 (* fake free variable names for locally bound variables - these work |
|
24 as placeholders. *) |
|
25 |
|
26 (* don't use dest_fake.. - we should instead be working with numbers |
|
27 and a list... else we rely on naming conventions which can break, or |
|
28 be violated - in contrast list locations are correct by |
|
29 construction/definition. *) |
|
30 (* |
|
31 fun dest_fake_bound_name n = |
|
32 case (explode n) of |
|
33 (":" :: realchars) => implode realchars |
|
34 | _ => n; *) |
|
35 fun is_fake_bound_name n = (hd (explode n) = ":"); |
|
36 fun mk_fake_bound_name n = ":b_" ^ n; |
|
37 |
|
38 |
|
39 |
|
40 (* fake free variable names for local meta variables - these work |
|
41 as placeholders. *) |
|
42 fun dest_fake_fix_name n = |
|
43 case (explode n) of |
|
44 ("@" :: realchars) => implode realchars |
|
45 | _ => n; |
|
46 fun is_fake_fix_name n = (hd (explode n) = "@"); |
|
47 fun mk_fake_fix_name n = "@" ^ n; |
|
48 |
|
49 |
|
50 |
|
51 (* fake free variable names for meta level bound variables *) |
|
52 fun dest_fake_all_name n = |
|
53 case (explode n) of |
|
54 ("+" :: realchars) => implode realchars |
|
55 | _ => n; |
|
56 fun is_fake_all_name n = (hd (explode n) = "+"); |
|
57 fun mk_fake_all_name n = "+" ^ n; |
|
58 |
|
59 |
|
60 |
|
61 |
|
62 (* Ys and Ts not used, Ns are real names of faked local bounds, the |
|
63 idea is that this will be mapped to free variables thus if a free |
|
64 variable is a faked local bound then we change it to being a meta |
|
65 variable so that it can later be instantiated *) |
|
66 (* FIXME: rename this - avoid the word fix! *) |
|
67 (* note we are not really "fix"'ing the free, more like making it variable! *) |
|
68 (* fun trymkvar_of_fakefree (Ns, Ts) Ys (n,ty) = |
|
69 if n mem Ns then Var((n,0),ty) else Free (n,ty); |
|
70 *) |
|
71 |
|
72 (* make a var into a fixed free (ie prefixed with "@") *) |
|
73 fun mk_fakefixvar Ts ((n,i),ty) = Free(mk_fake_fix_name n, ty); |
|
74 |
|
75 |
|
76 (* mk_frees_bound: string list -> Term.term -> Term.term *) |
|
77 (* This function changes free variables to being represented as bound |
|
78 variables if the free's variable name is in the given list. The debruijn |
|
79 index is simply the position in the list *) |
|
80 (* THINKABOUT: danger of an existing free variable with the same name: fix |
|
81 this so that name conflict are avoided automatically! In the meantime, |
|
82 don't have free variables named starting with a ":" *) |
|
83 fun bounds_of_fakefrees Ys (a $ b) = |
|
84 (bounds_of_fakefrees Ys a) $ (bounds_of_fakefrees Ys b) |
|
85 | bounds_of_fakefrees Ys (Abs(n,ty,t)) = |
|
86 Abs(n,ty, bounds_of_fakefrees (n::Ys) t) |
|
87 | bounds_of_fakefrees Ys (Free (n,ty)) = |
|
88 let fun try_mk_bound_of_free (i,[]) = Free (n,ty) |
|
89 | try_mk_bound_of_free (i,(y::ys)) = |
|
90 if n = y then Bound i else try_mk_bound_of_free (i+1,ys) |
|
91 in try_mk_bound_of_free (0,Ys) end |
|
92 | bounds_of_fakefrees Ys t = t; |
|
93 |
|
94 |
|
95 (* map a function f onto each free variables *) |
|
96 fun map_to_frees f Ys (a $ b) = |
|
97 (map_to_frees f Ys a) $ (map_to_frees f Ys b) |
|
98 | map_to_frees f Ys (Abs(n,ty,t)) = |
|
99 Abs(n,ty, map_to_frees f ((n,ty)::Ys) t) |
|
100 | map_to_frees f Ys (Free a) = |
|
101 f Ys a |
|
102 | map_to_frees f Ys t = t; |
|
103 |
|
104 |
|
105 (* map a function f onto each meta variable *) |
|
106 fun map_to_vars f Ys (a $ b) = |
|
107 (map_to_vars f Ys a) $ (map_to_vars f Ys b) |
|
108 | map_to_vars f Ys (Abs(n,ty,t)) = |
|
109 Abs(n,ty, map_to_vars f ((n,ty)::Ys) t) |
|
110 | map_to_vars f Ys (Var a) = |
|
111 f Ys a |
|
112 | map_to_vars f Ys t = t; |
|
113 |
|
114 (* map a function f onto each free variables *) |
|
115 fun map_to_alls f (Const("all",allty) $ Abs(n,ty,t)) = |
|
116 let val (n2,ty2) = f (n,ty) |
|
117 in (Const("all",allty) $ Abs(n2,ty2,map_to_alls f t)) end |
|
118 | map_to_alls f x = x; |
|
119 |
|
120 (* map a function f to each type variable in a term *) |
|
121 (* implicit arg: term *) |
|
122 fun map_to_term_tvars f = |
|
123 Term.map_types (fn TVar(ix,ty) => f (ix,ty) | x => x); (* FIXME map_atyps !? *) |
|
124 |
|
125 |
|
126 |
|
127 (* what if a param desn't occur in the concl? think about! Note: This |
|
128 simply fixes meta level univ bound vars as Frees. At the end, we will |
|
129 change them back to schematic vars that will then unify |
|
130 appropriactely, ie with unfake_vars *) |
|
131 fun fake_concl_of_goal gt i = |
|
132 let |
|
133 val prems = Logic.strip_imp_prems gt |
|
134 val sgt = List.nth (prems, i - 1) |
|
135 |
|
136 val tbody = Logic.strip_imp_concl (Term.strip_all_body sgt) |
|
137 val tparams = Term.strip_all_vars sgt |
|
138 |
|
139 val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) |
|
140 tparams |
|
141 in |
|
142 Term.subst_bounds (rev fakefrees,tbody) |
|
143 end; |
|
144 |
|
145 (* what if a param desn't occur in the concl? think about! Note: This |
|
146 simply fixes meta level univ bound vars as Frees. At the end, we will |
|
147 change them back to schematic vars that will then unify |
|
148 appropriactely, ie with unfake_vars *) |
|
149 fun fake_goal gt i = |
|
150 let |
|
151 val prems = Logic.strip_imp_prems gt |
|
152 val sgt = List.nth (prems, i - 1) |
|
153 |
|
154 val tbody = Term.strip_all_body sgt |
|
155 val tparams = Term.strip_all_vars sgt |
|
156 |
|
157 val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) |
|
158 tparams |
|
159 in |
|
160 Term.subst_bounds (rev fakefrees,tbody) |
|
161 end; |
|
162 |
|
163 |
|
164 (* hand written - for some reason the Isabelle version in drule is broken! |
|
165 Example? something to do with Bin Yangs examples? |
|
166 *) |
|
167 fun rename_term_bvars ns (Abs(s,ty,t)) = |
|
168 let val s2opt = Library.find_first (fn (x,y) => s = x) ns |
|
169 in case s2opt of |
|
170 NONE => (Abs(s,ty,rename_term_bvars ns t)) |
|
171 | SOME (_,s2) => Abs(s2,ty, rename_term_bvars ns t) end |
|
172 | rename_term_bvars ns (a$b) = |
|
173 (rename_term_bvars ns a) $ (rename_term_bvars ns b) |
|
174 | rename_term_bvars _ x = x; |
|
175 |
|
176 fun rename_thm_bvars ns th = |
|
177 let val t = Thm.prop_of th |
|
178 in Thm.rename_boundvars t (rename_term_bvars ns t) th end; |
|
179 |
|
180 (* Finish this to show how it breaks! (raises the exception): |
|
181 |
|
182 exception rename_thm_bvars_exp of ((string * string) list * Thm.thm) |
|
183 |
|
184 Drule.rename_bvars ns th |
|
185 handle TERM _ => raise rename_thm_bvars_exp (ns, th); |
|
186 *) |
|
187 |
|
188 end; |
|