src/Tools/IsaPlanner/rw_tools.ML

author | wenzelm |

Sat, 07 Apr 2012 16:41:59 +0200 | |

changeset 47389 | e8552cba702d |

parent 42364 | 8c674b3b8e44 |

permissions | -rw-r--r-- |

explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
tuned;

(* Title: Tools/IsaPlanner/rw_tools.ML Author: Lucas Dixon, University of Edinburgh Term related tools used for rewriting. *) signature RWTOOLS = sig end; structure RWTools = struct (* fake free variable names for locally bound variables - these work as placeholders. *) (* don't use dest_fake.. - we should instead be working with numbers and a list... else we rely on naming conventions which can break, or be violated - in contrast list locations are correct by construction/definition. *) (* fun dest_fake_bound_name n = case (raw_explode n) of (* FIXME Symbol.explode (?) *) (":" :: realchars) => implode realchars | _ => n; *) fun is_fake_bound_name n = (hd (raw_explode n) = ":"); (* FIXME Symbol.explode (?) *) fun mk_fake_bound_name n = ":b_" ^ n; (* fake free variable names for local meta variables - these work as placeholders. *) fun dest_fake_fix_name n = case (raw_explode n) of (* FIXME Symbol.explode (?) *) ("@" :: realchars) => implode realchars | _ => n; fun is_fake_fix_name n = (hd (raw_explode n) = "@"); (* FIXME Symbol.explode (?) *) fun mk_fake_fix_name n = "@" ^ n; (* fake free variable names for meta level bound variables *) fun dest_fake_all_name n = case (raw_explode n) of (* FIXME Symbol.explode (?) *) ("+" :: realchars) => implode realchars | _ => n; fun is_fake_all_name n = (hd (raw_explode n) = "+"); (* FIXME Symbol.explode (?) *) fun mk_fake_all_name n = "+" ^ n; (* Ys and Ts not used, Ns are real names of faked local bounds, the idea is that this will be mapped to free variables thus if a free variable is a faked local bound then we change it to being a meta variable so that it can later be instantiated *) (* FIXME: rename this - avoid the word fix! *) (* note we are not really "fix"'ing the free, more like making it variable! *) (* fun trymkvar_of_fakefree (Ns, Ts) Ys (n,ty) = if n mem Ns then Var((n,0),ty) else Free (n,ty); *) (* make a var into a fixed free (ie prefixed with "@") *) fun mk_fakefixvar Ts ((n,i),ty) = Free(mk_fake_fix_name n, ty); (* mk_frees_bound: string list -> Term.term -> Term.term *) (* This function changes free variables to being represented as bound variables if the free's variable name is in the given list. The debruijn index is simply the position in the list *) (* THINKABOUT: danger of an existing free variable with the same name: fix this so that name conflict are avoided automatically! In the meantime, don't have free variables named starting with a ":" *) fun bounds_of_fakefrees Ys (a $ b) = (bounds_of_fakefrees Ys a) $ (bounds_of_fakefrees Ys b) | bounds_of_fakefrees Ys (Abs(n,ty,t)) = Abs(n,ty, bounds_of_fakefrees (n::Ys) t) | bounds_of_fakefrees Ys (Free (n,ty)) = let fun try_mk_bound_of_free (i,[]) = Free (n,ty) | try_mk_bound_of_free (i,(y::ys)) = if n = y then Bound i else try_mk_bound_of_free (i+1,ys) in try_mk_bound_of_free (0,Ys) end | bounds_of_fakefrees Ys t = t; (* map a function f onto each free variables *) fun map_to_frees f Ys (a $ b) = (map_to_frees f Ys a) $ (map_to_frees f Ys b) | map_to_frees f Ys (Abs(n,ty,t)) = Abs(n,ty, map_to_frees f ((n,ty)::Ys) t) | map_to_frees f Ys (Free a) = f Ys a | map_to_frees f Ys t = t; (* map a function f onto each meta variable *) fun map_to_vars f Ys (a $ b) = (map_to_vars f Ys a) $ (map_to_vars f Ys b) | map_to_vars f Ys (Abs(n,ty,t)) = Abs(n,ty, map_to_vars f ((n,ty)::Ys) t) | map_to_vars f Ys (Var a) = f Ys a | map_to_vars f Ys t = t; (* map a function f onto each free variables *) fun map_to_alls f (Const("all",allty) $ Abs(n,ty,t)) = let val (n2,ty2) = f (n,ty) in (Const("all",allty) $ Abs(n2,ty2,map_to_alls f t)) end | map_to_alls f x = x; (* map a function f to each type variable in a term *) (* implicit arg: term *) fun map_to_term_tvars f = Term.map_types (fn TVar(ix,ty) => f (ix,ty) | x => x); (* FIXME map_atyps !? *) (* what if a param desn't occur in the concl? think about! Note: This simply fixes meta level univ bound vars as Frees. At the end, we will change them back to schematic vars that will then unify appropriactely, ie with unfake_vars *) fun fake_concl_of_goal gt i = let val prems = Logic.strip_imp_prems gt val sgt = nth prems (i - 1) val tbody = Logic.strip_imp_concl (Term.strip_all_body sgt) val tparams = Term.strip_all_vars sgt val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) tparams in Term.subst_bounds (rev fakefrees,tbody) end; (* what if a param desn't occur in the concl? think about! Note: This simply fixes meta level univ bound vars as Frees. At the end, we will change them back to schematic vars that will then unify appropriactely, ie with unfake_vars *) fun fake_goal gt i = let val prems = Logic.strip_imp_prems gt val sgt = nth prems (i - 1) val tbody = Term.strip_all_body sgt val tparams = Term.strip_all_vars sgt val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) tparams in Term.subst_bounds (rev fakefrees,tbody) end; (* hand written - for some reason the Isabelle version in drule is broken! Example? something to do with Bin Yangs examples? *) fun rename_term_bvars ns (Abs(s,ty,t)) = let val s2opt = Library.find_first (fn (x,y) => s = x) ns in case s2opt of NONE => (Abs(s,ty,rename_term_bvars ns t)) | SOME (_,s2) => Abs(s2,ty, rename_term_bvars ns t) end | rename_term_bvars ns (a$b) = (rename_term_bvars ns a) $ (rename_term_bvars ns b) | rename_term_bvars _ x = x; fun rename_thm_bvars ns th = let val t = Thm.prop_of th in Thm.rename_boundvars t (rename_term_bvars ns t) th end; (* Finish this to show how it breaks! (raises the exception): exception rename_thm_bvars_exp of ((string * string) list * Thm.thm) Drule.rename_bvars ns th handle TERM _ => raise rename_thm_bvars_exp (ns, th); *) end;