src/Pure/IsaPlanner/rw_tools.ML
author haftmann
Tue Sep 06 08:30:43 2005 +0200 (2005-09-06)
changeset 17271 2756a73f63a5
parent 16179 fa7e70be26b0
permissions -rw-r--r--
introduced some new-style AList operations
     1 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     2 (*  Title:      Pure/IsaPlanner/rw_tools.ML
     3     ID:		$Id$
     4     Author:     Lucas Dixon, University of Edinburgh
     5                 lucas.dixon@ed.ac.uk
     6     Created:    28 May 2004
     7 *)
     8 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     9 (*  DESCRIPTION:
    10 
    11     term related tools used for rewriting
    12 
    13 *)   
    14 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    15 
    16 signature RWTOOLS =
    17 sig
    18 end;
    19 
    20 structure RWTools 
    21 = struct
    22 
    23 (* THINKABOUT: don't need this: should be able to generate the paired 
    24    NsTs directly ? --already implemented as ~~
    25 fun join_lists ([],[]) = []
    26   | join_lists (x::xs, y::ys) = (x,y) :: (join_lists (xs,ys))
    27   | join_lists (_, _) = raise ERROR_MESSAGE "join_lists: unequal size lists";
    28  *)
    29 
    30 (* fake free variable names for locally bound variables - these work
    31 as placeholders. *)
    32 
    33 (* don't use dest_fake.. - we should instead be working with numbers
    34 and a list... else we rely on naming conventions which can break, or
    35 be violated - in contrast list locations are correct by
    36 construction/definition. *)
    37 (*
    38 fun dest_fake_bound_name n = 
    39     case (explode n) of 
    40       (":" :: realchars) => implode realchars
    41     | _ => n; *)
    42 fun is_fake_bound_name n = (hd (explode n) = ":");
    43 fun mk_fake_bound_name n = ":b_" ^ n;
    44 
    45 
    46 
    47 (* fake free variable names for local meta variables - these work
    48 as placeholders. *)
    49 fun dest_fake_fix_name n = 
    50     case (explode n) of 
    51       ("@" :: realchars) => implode realchars
    52     | _ => n;
    53 fun is_fake_fix_name n = (hd (explode n) = "@");
    54 fun mk_fake_fix_name n = "@" ^ n;
    55 
    56 
    57 
    58 (* fake free variable names for meta level bound variables *)
    59 fun dest_fake_all_name n = 
    60     case (explode n) of 
    61       ("+" :: realchars) => implode realchars
    62     | _ => n;
    63 fun is_fake_all_name n = (hd (explode n) = "+");
    64 fun mk_fake_all_name n = "+" ^ n;
    65 
    66 
    67 
    68 
    69 (* Ys and Ts not used, Ns are real names of faked local bounds, the
    70 idea is that this will be mapped to free variables thus if a free
    71 variable is a faked local bound then we change it to being a meta
    72 variable so that it can later be instantiated *)
    73 (* FIXME: rename this - avoid the word fix! *)
    74 (* note we are not really "fix"'ing the free, more like making it variable! *)
    75 (* fun trymkvar_of_fakefree (Ns, Ts) Ys (n,ty) = 
    76     if n mem Ns then Var((n,0),ty) else Free (n,ty);
    77 *)
    78 
    79 (* make a var into a fixed free (ie prefixed with "@") *)
    80 fun mk_fakefixvar Ts ((n,i),ty) = Free(mk_fake_fix_name n, ty);
    81 
    82 
    83 (* mk_frees_bound: string list -> Term.term -> Term.term *)
    84 (* This function changes free variables to being represented as bound
    85 variables if the free's variable name is in the given list. The debruijn 
    86 index is simply the position in the list *)
    87 (* THINKABOUT: danger of an existing free variable with the same name: fix
    88 this so that name conflict are avoided automatically! In the meantime,
    89 don't have free variables named starting with a ":" *)
    90 fun bounds_of_fakefrees Ys (a $ b) = 
    91     (bounds_of_fakefrees Ys a) $ (bounds_of_fakefrees Ys b)
    92   | bounds_of_fakefrees Ys (Abs(n,ty,t)) = 
    93     Abs(n,ty, bounds_of_fakefrees (n::Ys) t)
    94   | bounds_of_fakefrees Ys (Free (n,ty)) = 
    95     let fun try_mk_bound_of_free (i,[]) = Free (n,ty)
    96           | try_mk_bound_of_free (i,(y::ys)) = 
    97             if n = y then Bound i else try_mk_bound_of_free (i+1,ys)
    98     in try_mk_bound_of_free (0,Ys) end
    99   | bounds_of_fakefrees Ys t = t;
   100 
   101 
   102 (* map a function f onto each free variables *)
   103 fun map_to_frees f Ys (a $ b) = 
   104     (map_to_frees f Ys a) $ (map_to_frees f Ys b)
   105   | map_to_frees f Ys (Abs(n,ty,t)) = 
   106     Abs(n,ty, map_to_frees f ((n,ty)::Ys) t)
   107   | map_to_frees f Ys (Free a) = 
   108     f Ys a
   109   | map_to_frees f Ys t = t;
   110 
   111 
   112 (* map a function f onto each meta variable  *)
   113 fun map_to_vars f Ys (a $ b) = 
   114     (map_to_vars f Ys a) $ (map_to_vars f Ys b)
   115   | map_to_vars f Ys (Abs(n,ty,t)) = 
   116     Abs(n,ty, map_to_vars f ((n,ty)::Ys) t)
   117   | map_to_vars f Ys (Var a) = 
   118     f Ys a
   119   | map_to_vars f Ys t = t;
   120 
   121 (* map a function f onto each free variables *)
   122 fun map_to_alls f (Const("all",allty) $ Abs(n,ty,t)) = 
   123     let val (n2,ty2) = f (n,ty) 
   124     in (Const("all",allty) $ Abs(n2,ty2,map_to_alls f t)) end
   125   | map_to_alls f x = x;
   126 
   127 (* map a function f to each type variable in a term *)
   128 (* implicit arg: term *)
   129 fun map_to_term_tvars f =
   130     Term.map_term_types (fn TVar(ix,ty) => f (ix,ty) | x => x);
   131 
   132 
   133 
   134 (* what if a param desn't occur in the concl? think about! Note: This
   135 simply fixes meta level univ bound vars as Frees.  At the end, we will
   136 change them back to schematic vars that will then unify
   137 appropriactely, ie with unfake_vars *)
   138 fun fake_concl_of_goal gt i = 
   139     let 
   140       val prems = Logic.strip_imp_prems gt
   141       val sgt = List.nth (prems, i - 1)
   142 
   143       val tbody = Logic.strip_imp_concl (Term.strip_all_body sgt)
   144       val tparams = Term.strip_all_vars sgt
   145 
   146       val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) 
   147                           tparams
   148     in
   149       Term.subst_bounds (rev fakefrees,tbody)
   150     end;
   151 
   152 (* what if a param desn't occur in the concl? think about! Note: This
   153 simply fixes meta level univ bound vars as Frees.  At the end, we will
   154 change them back to schematic vars that will then unify
   155 appropriactely, ie with unfake_vars *)
   156 fun fake_goal gt i = 
   157     let 
   158       val prems = Logic.strip_imp_prems gt
   159       val sgt = List.nth (prems, i - 1)
   160 
   161       val tbody = Term.strip_all_body sgt
   162       val tparams = Term.strip_all_vars sgt
   163 
   164       val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) 
   165                           tparams
   166     in
   167       Term.subst_bounds (rev fakefrees,tbody)
   168     end;
   169 
   170 
   171 (* hand written - for some reason the Isabelle version in drule is broken!
   172 Example? something to do with Bin Yangs examples? 
   173  *)
   174 fun rename_term_bvars ns (Abs(s,ty,t)) = 
   175     let val s2opt = Library.find_first (fn (x,y) => s = x) ns
   176     in case s2opt of 
   177          NONE => (Abs(s,ty,rename_term_bvars  ns t))
   178        | SOME (_,s2) => Abs(s2,ty, rename_term_bvars ns t) end
   179   | rename_term_bvars ns (a$b) = 
   180     (rename_term_bvars ns a) $ (rename_term_bvars ns b)
   181   | rename_term_bvars _ x = x;
   182 
   183 fun rename_thm_bvars ns th = 
   184     let val t = Thm.prop_of th 
   185     in Thm.rename_boundvars t (rename_term_bvars ns t) th end;
   186 
   187 (* Finish this to show how it breaks! (raises the exception): 
   188 
   189 exception rename_thm_bvars_exp of ((string * string) list * Thm.thm)
   190 
   191     Drule.rename_bvars ns th 
   192     handle TERM _ => raise rename_thm_bvars_exp (ns, th); 
   193 *)
   194 
   195 end;