src/Tools/IsaPlanner/rw_tools.ML
author wenzelm
Sat Feb 28 14:09:58 2009 +0100 (2009-02-28)
changeset 30161 c26e515f1c29
parent 23175 267ba70e7a9d
child 40627 becf5d5187cc
permissions -rw-r--r--
removed Ids;
     1 (*  Title:      Tools/IsaPlanner/rw_tools.ML
     2     Author:     Lucas Dixon, University of Edinburgh
     3 
     4 Term related tools used for rewriting.
     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 = 
    23     case (explode n) of 
    24       (":" :: realchars) => implode realchars
    25     | _ => n; *)
    26 fun is_fake_bound_name n = (hd (explode n) = ":");
    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 = 
    34     case (explode n) of 
    35       ("@" :: realchars) => implode realchars
    36     | _ => n;
    37 fun is_fake_fix_name n = (hd (explode n) = "@");
    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 = 
    44     case (explode n) of 
    45       ("+" :: realchars) => implode realchars
    46     | _ => n;
    47 fun is_fake_all_name n = (hd (explode n) = "+");
    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
   125       val sgt = List.nth (prems, i - 1)
   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
   143       val sgt = List.nth (prems, i - 1)
   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;