tuned incr_tvar_same;
authorwenzelm
Thu Jul 16 22:58:07 2009 +0200 (2009-07-16)
changeset 320269898880061df
parent 32025 e8fbfa84c23f
child 32027 9dd548810ed1
tuned incr_tvar_same;
export tuned version of incr_indexes_same;
src/Pure/logic.ML
     1.1 --- a/src/Pure/logic.ML	Thu Jul 16 22:54:39 2009 +0200
     1.2 +++ b/src/Pure/logic.ML	Thu Jul 16 22:58:07 2009 +0200
     1.3 @@ -56,6 +56,7 @@
     1.4    val rlist_abs: (string * typ) list * term -> term
     1.5    val incr_tvar_same: int -> typ Same.operation
     1.6    val incr_tvar: int -> typ -> typ
     1.7 +  val incr_indexes_same: typ list * int -> term Same.operation
     1.8    val incr_indexes: typ list * int -> term -> term
     1.9    val lift_abs: int -> term -> term -> term
    1.10    val lift_all: int -> term -> term -> term
    1.11 @@ -304,20 +305,20 @@
    1.12  fun rlist_abs ([], body) = body
    1.13    | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
    1.14  
    1.15 -fun incr_tvar_same k = Term_Subst.map_atypsT_same
    1.16 -  (fn TVar ((a, i), S) => TVar ((a, i + k), S)
    1.17 -    | _ => raise Same.SAME);
    1.18 +fun incr_tvar_same 0 = Same.same
    1.19 +  | incr_tvar_same k = Term_Subst.map_atypsT_same
    1.20 +      (fn TVar ((a, i), S) => TVar ((a, i + k), S)
    1.21 +        | _ => raise Same.SAME);
    1.22  
    1.23 -fun incr_tvar 0 T = T
    1.24 -  | incr_tvar k T = incr_tvar_same k T handle Same.SAME => T;
    1.25 +fun incr_tvar k T = incr_tvar_same k T handle Same.SAME => T;
    1.26  
    1.27  (*For all variables in the term, increment indexnames and lift over the Us
    1.28      result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
    1.29 -fun incr_indexes ([], 0) t = t
    1.30 -  | incr_indexes (Ts, k) t =
    1.31 +fun incr_indexes_same ([], 0) = Same.same
    1.32 +  | incr_indexes_same (Ts, k) =
    1.33        let
    1.34          val n = length Ts;
    1.35 -        val incrT = if k = 0 then I else incr_tvar_same k;
    1.36 +        val incrT = incr_tvar_same k;
    1.37  
    1.38          fun incr lev (Var ((x, i), T)) =
    1.39                combound (Var ((x, i + k), Ts ---> Same.commit incrT T), lev, n)
    1.40 @@ -329,8 +330,10 @@
    1.41                  handle Same.SAME => t $ incr lev u)
    1.42            | incr _ (Const (c, T)) = Const (c, incrT T)
    1.43            | incr _ (Free (x, T)) = Free (x, incrT T)
    1.44 -          | incr _ (t as Bound _) = t;
    1.45 -      in incr 0 t handle Same.SAME => t end;
    1.46 +          | incr _ (Bound _) = raise Same.SAME;
    1.47 +      in incr 0 end;
    1.48 +
    1.49 +fun incr_indexes arg t = incr_indexes_same arg t handle Same.SAME => t;
    1.50  
    1.51  
    1.52  (* Lifting functions from subgoal and increment: