src/Pure/logic.ML
changeset 19806 f860b7a98445
parent 19775 06cb6743adf6
child 19879 6a346150611a
     1.1 --- a/src/Pure/logic.ML	Wed Jun 07 02:01:27 2006 +0200
     1.2 +++ b/src/Pure/logic.ML	Wed Jun 07 02:01:28 2006 +0200
     1.3 @@ -67,8 +67,14 @@
     1.4    val set_rename_prefix: string -> unit
     1.5    val list_rename_params: string list * term -> term
     1.6    val assum_pairs: int * term -> (term*term)list
     1.7 +  val varifyT: typ -> typ
     1.8 +  val unvarifyT: typ -> typ
     1.9    val varify: term -> term
    1.10    val unvarify: term -> term
    1.11 +  val legacy_varifyT: typ -> typ
    1.12 +  val legacy_unvarifyT: typ -> typ
    1.13 +  val legacy_varify: term -> term
    1.14 +  val legacy_unvarify: term -> term
    1.15    val get_goal: term -> int -> term
    1.16    val goal_params: term -> int -> term * term list
    1.17    val prems_of_goal: term -> int -> term list
    1.18 @@ -492,7 +498,7 @@
    1.19        all T $ Abs(c, T, list_rename_params (cs, t))
    1.20    | list_rename_params (cs, B) = B;
    1.21  
    1.22 -(*** Treatmsent of "assume", "erule", etc. ***)
    1.23 +(*** Treatment of "assume", "erule", etc. ***)
    1.24  
    1.25  (*Strips assumptions in goal yielding
    1.26     HS = [Hn,...,H1],   params = [xm,...,x1], and B,
    1.27 @@ -529,22 +535,46 @@
    1.28    in  pairrev (Hs,[])
    1.29    end;
    1.30  
    1.31 -(*Converts Frees to Vars and TFrees to TVars*)
    1.32 -fun varify (Const(a, T)) = Const (a, Type.varifyT T)
    1.33 -  | varify (Free (a, T)) = Var ((a, 0), Type.varifyT T)
    1.34 -  | varify (Var (ixn, T)) = Var (ixn, Type.varifyT T)
    1.35 -  | varify (t as Bound _) = t
    1.36 -  | varify (Abs (a, T, body)) = Abs (a, Type.varifyT T, varify body)
    1.37 -  | varify (f $ t) = varify f $ varify t;
    1.38 +
    1.39 +(* global schematic variables *)
    1.40 +
    1.41 +fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
    1.42 +fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
    1.43 +
    1.44 +fun varifyT ty = ty |> Term.map_atyps
    1.45 +  (fn TFree (a, S) => TVar ((a, 0), S)
    1.46 +    | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
    1.47 +
    1.48 +fun unvarifyT ty = ty |> Term.map_atyps
    1.49 +  (fn TVar ((a, 0), S) => TFree (a, S)
    1.50 +    | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
    1.51 +    | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
    1.52  
    1.53 -(*Inverse of varify.*)
    1.54 -fun unvarify (Const (a, T)) = Const (a, Type.unvarifyT T)
    1.55 -  | unvarify (Free (a, T)) = Free (a, Type.unvarifyT T)
    1.56 -  | unvarify (Var ((a, 0), T)) = Free (a, Type.unvarifyT T)
    1.57 -  | unvarify (Var (ixn, T)) = Var (ixn, Type.unvarifyT T)  (*non-0 index!*)
    1.58 -  | unvarify (t as Bound _) = t
    1.59 -  | unvarify (Abs (a, T, body)) = Abs (a, Type.unvarifyT T, unvarify body)
    1.60 -  | unvarify (f $ t) = unvarify f $ unvarify t;
    1.61 +fun varify tm =
    1.62 +  tm |> Term.map_aterms
    1.63 +    (fn Free (x, T) => Var ((x, 0), T)
    1.64 +      | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
    1.65 +      | t => t)
    1.66 +  |> Term.map_term_types varifyT;
    1.67 +
    1.68 +fun unvarify tm =
    1.69 +  tm |> Term.map_aterms
    1.70 +    (fn Var ((x, 0), T) => Free (x, T)
    1.71 +      | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
    1.72 +      | Free (x, _) => raise TERM (bad_fixed x, [tm])
    1.73 +      | t => t)
    1.74 +  |> Term.map_term_types unvarifyT;
    1.75 +
    1.76 +val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
    1.77 +val legacy_unvarifyT = Term.map_atyps (fn TVar ((a, 0), S) => TFree (a, S) | T => T);
    1.78 +
    1.79 +val legacy_varify =
    1.80 +  Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #>
    1.81 +  Term.map_term_types legacy_varifyT;
    1.82 +
    1.83 +val legacy_unvarify =
    1.84 +  Term.map_aterms (fn Var ((x, 0), T) => Free (x, T) | t => t) #>
    1.85 +  Term.map_term_types legacy_unvarifyT;
    1.86  
    1.87  
    1.88  (* goal states *)