author | wenzelm |
Sat, 16 Apr 2011 18:11:20 +0200 | |
changeset 42364 | 8c674b3b8e44 |
parent 40627 | becf5d5187cc |
permissions | -rw-r--r-- |
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; |