src/Tools/IsaPlanner/rw_tools.ML
author wenzelm
Sat Oct 06 16:50:04 2007 +0200 (2007-10-06)
changeset 24867 e5b55d7be9bb
parent 23175 267ba70e7a9d
child 30161 c26e515f1c29
permissions -rw-r--r--
simplified interfaces for outer syntax;
     1 (*  Title:      Tools/IsaPlanner/rw_tools.ML
     2     ID:		$Id$
     3     Author:     Lucas Dixon, University of Edinburgh
     4 
     5 Term related tools used for rewriting.
     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;