diff -r 81d6dc597559 -r 5181e317e9ff src/Pure/IsaPlanner/rw_tools.ML --- a/src/Pure/IsaPlanner/rw_tools.ML Sun Jun 11 00:28:18 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,195 +0,0 @@ -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* Title: Pure/IsaPlanner/rw_tools.ML - ID: $Id$ - Author: Lucas Dixon, University of Edinburgh - lucas.dixon@ed.ac.uk - Created: 28 May 2004 -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* DESCRIPTION: - - term related tools used for rewriting - -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) - -signature RWTOOLS = -sig -end; - -structure RWTools -= struct - -(* THINKABOUT: don't need this: should be able to generate the paired - NsTs directly ? --already implemented as ~~ -fun join_lists ([],[]) = [] - | join_lists (x::xs, y::ys) = (x,y) :: (join_lists (xs,ys)) - | join_lists (_, _) = raise ERROR_MESSAGE "join_lists: unequal size lists"; - *) - -(* 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 (explode n) of - (":" :: realchars) => implode realchars - | _ => n; *) -fun is_fake_bound_name n = (hd (explode n) = ":"); -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 (explode n) of - ("@" :: realchars) => implode realchars - | _ => n; -fun is_fake_fix_name n = (hd (explode n) = "@"); -fun mk_fake_fix_name n = "@" ^ n; - - - -(* fake free variable names for meta level bound variables *) -fun dest_fake_all_name n = - case (explode n) of - ("+" :: realchars) => implode realchars - | _ => n; -fun is_fake_all_name n = (hd (explode n) = "+"); -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_term_types (fn TVar(ix,ty) => f (ix,ty) | x => x); - - - -(* 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 = List.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 = List.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;