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