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