23175

1 
(* Title: Tools/IsaPlanner/rw_tools.ML

23171

2 
ID: $Id$


3 
Author: Lucas Dixon, University of Edinburgh


4 

23175

5 
Term related tools used for rewriting.

23171

6 
*)


7 


8 
signature RWTOOLS =


9 
sig


10 
end;


11 


12 
structure RWTools


13 
= struct


14 


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


16 
as placeholders. *)


17 


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


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


20 
be violated  in contrast list locations are correct by


21 
construction/definition. *)


22 
(*


23 
fun dest_fake_bound_name n =


24 
case (explode n) of


25 
(":" :: realchars) => implode realchars


26 
 _ => n; *)


27 
fun is_fake_bound_name n = (hd (explode n) = ":");


28 
fun mk_fake_bound_name n = ":b_" ^ n;


29 


30 


31 


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


33 
as placeholders. *)


34 
fun dest_fake_fix_name n =


35 
case (explode n) of


36 
("@" :: realchars) => implode realchars


37 
 _ => n;


38 
fun is_fake_fix_name n = (hd (explode n) = "@");


39 
fun mk_fake_fix_name n = "@" ^ n;


40 


41 


42 


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


44 
fun dest_fake_all_name n =


45 
case (explode n) of


46 
("+" :: realchars) => implode realchars


47 
 _ => n;


48 
fun is_fake_all_name n = (hd (explode n) = "+");


49 
fun mk_fake_all_name n = "+" ^ n;


50 


51 


52 


53 


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


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


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


57 
variable so that it can later be instantiated *)


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


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


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


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


62 
*)


63 


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


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


66 


67 


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


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


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


71 
index is simply the position in the list *)


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


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


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


75 
fun bounds_of_fakefrees Ys (a $ b) =


76 
(bounds_of_fakefrees Ys a) $ (bounds_of_fakefrees Ys b)


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


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


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


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


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


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


83 
in try_mk_bound_of_free (0,Ys) end


84 
 bounds_of_fakefrees Ys t = t;


85 


86 


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


88 
fun map_to_frees f Ys (a $ b) =


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


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


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


92 
 map_to_frees f Ys (Free a) =


93 
f Ys a


94 
 map_to_frees f Ys t = t;


95 


96 


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


98 
fun map_to_vars f Ys (a $ b) =


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


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


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


102 
 map_to_vars f Ys (Var a) =


103 
f Ys a


104 
 map_to_vars f Ys t = t;


105 


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


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


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


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


110 
 map_to_alls f x = x;


111 


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


113 
(* implicit arg: term *)


114 
fun map_to_term_tvars f =


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


116 


117 


118 


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


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


121 
change them back to schematic vars that will then unify


122 
appropriactely, ie with unfake_vars *)


123 
fun fake_concl_of_goal gt i =


124 
let


125 
val prems = Logic.strip_imp_prems gt


126 
val sgt = List.nth (prems, i  1)


127 


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


129 
val tparams = Term.strip_all_vars sgt


130 


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


132 
tparams


133 
in


134 
Term.subst_bounds (rev fakefrees,tbody)


135 
end;


136 


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


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


139 
change them back to schematic vars that will then unify


140 
appropriactely, ie with unfake_vars *)


141 
fun fake_goal gt i =


142 
let


143 
val prems = Logic.strip_imp_prems gt


144 
val sgt = List.nth (prems, i  1)


145 


146 
val tbody = Term.strip_all_body sgt


147 
val tparams = Term.strip_all_vars sgt


148 


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


150 
tparams


151 
in


152 
Term.subst_bounds (rev fakefrees,tbody)


153 
end;


154 


155 


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


157 
Example? something to do with Bin Yangs examples?


158 
*)


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


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


161 
in case s2opt of


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


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


164 
 rename_term_bvars ns (a$b) =


165 
(rename_term_bvars ns a) $ (rename_term_bvars ns b)


166 
 rename_term_bvars _ x = x;


167 


168 
fun rename_thm_bvars ns th =


169 
let val t = Thm.prop_of th


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


171 


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


173 


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


175 


176 
Drule.rename_bvars ns th


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


178 
*)


179 


180 
end;
