src/Pure/IsaPlanner/rw_tools.ML

domain package generates compactness lemmas for new constructors

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
(*  Title:      Pure/IsaPlanner/rw_tools.ML
    ID:		$Id$
    Author:     Lucas Dixon, University of Edinburgh
                [e-mail]
    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;