src/Pure/logic.ML
changeset 32020 9abf5d66606e
parent 32014 857367925493
child 32023 2d071ac5032f
     1.1 --- a/src/Pure/logic.ML	Thu Jul 16 20:32:40 2009 +0200
     1.2 +++ b/src/Pure/logic.ML	Thu Jul 16 21:00:09 2009 +0200
     1.3 @@ -304,44 +304,33 @@
     1.4    | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
     1.5  
     1.6  
     1.7 -local exception SAME in
     1.8 -
     1.9 -fun incrT k =
    1.10 -  let
    1.11 -    fun incr (TVar ((a, i), S)) = TVar ((a, i + k), S)
    1.12 -      | incr (Type (a, Ts)) = Type (a, incrs Ts)
    1.13 -      | incr _ = raise SAME
    1.14 -    and incrs (T :: Ts) =
    1.15 -        (incr T :: (incrs Ts handle SAME => Ts)
    1.16 -          handle SAME => T :: incrs Ts)
    1.17 -      | incrs [] = raise SAME;
    1.18 -  in incr end;
    1.19 +fun incrT 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  (*For all variables in the term, increment indexnames and lift over the Us
    1.24      result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
    1.25  fun incr_indexes ([], 0) t = t
    1.26    | incr_indexes (Ts, k) t =
    1.27 -  let
    1.28 -    val n = length Ts;
    1.29 -    val incrT = if k = 0 then I else incrT k;
    1.30 +      let
    1.31 +        val n = length Ts;
    1.32 +        val incrT = if k = 0 then I else incrT k;
    1.33  
    1.34 -    fun incr lev (Var ((x, i), T)) =
    1.35 -          combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n)
    1.36 -      | incr lev (Abs (x, T, body)) =
    1.37 -          (Abs (x, incrT T, incr (lev + 1) body handle SAME => body)
    1.38 -            handle SAME => Abs (x, T, incr (lev + 1) body))
    1.39 -      | incr lev (t $ u) =
    1.40 -          (incr lev t $ (incr lev u handle SAME => u)
    1.41 -            handle 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 => t end;
    1.46 +        fun incr lev (Var ((x, i), T)) =
    1.47 +              combound (Var ((x, i + k), Ts ---> Same.commit incrT T), lev, n)
    1.48 +          | incr lev (Abs (x, T, body)) =
    1.49 +              (Abs (x, incrT T, incr (lev + 1) body handle Same.SAME => body)
    1.50 +                handle Same.SAME => Abs (x, T, incr (lev + 1) body))
    1.51 +          | incr lev (t $ u) =
    1.52 +              (incr lev t $ (incr lev u handle Same.SAME => u)
    1.53 +                handle Same.SAME => t $ incr lev u)
    1.54 +          | incr _ (Const (c, T)) = Const (c, incrT T)
    1.55 +          | incr _ (Free (x, T)) = Free (x, incrT T)
    1.56 +          | incr _ (t as Bound _) = t;
    1.57 +      in incr 0 t handle Same.SAME => t end;
    1.58  
    1.59  fun incr_tvar 0 T = T
    1.60 -  | incr_tvar k T = incrT k T handle SAME => T;
    1.61 -
    1.62 -end;
    1.63 +  | incr_tvar k T = incrT k T handle Same.SAME => T;
    1.64  
    1.65  
    1.66  (* Lifting functions from subgoal and increment:
    1.67 @@ -473,35 +462,35 @@
    1.68  fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
    1.69  fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
    1.70  
    1.71 -fun varifyT_option ty = ty
    1.72 -  |> Term_Subst.map_atypsT_option
    1.73 -    (fn TFree (a, S) => SOME (TVar ((a, 0), S))
    1.74 +fun varifyT_same ty = ty
    1.75 +  |> Term_Subst.map_atypsT_same
    1.76 +    (fn TFree (a, S) => TVar ((a, 0), S)
    1.77        | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
    1.78  
    1.79 -fun unvarifyT_option ty = ty
    1.80 -  |> Term_Subst.map_atypsT_option
    1.81 -    (fn TVar ((a, 0), S) => SOME (TFree (a, S))
    1.82 +fun unvarifyT_same ty = ty
    1.83 +  |> Term_Subst.map_atypsT_same
    1.84 +    (fn TVar ((a, 0), S) => TFree (a, S)
    1.85        | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
    1.86        | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
    1.87  
    1.88 -val varifyT = perhaps varifyT_option;
    1.89 -val unvarifyT = perhaps unvarifyT_option;
    1.90 +val varifyT = Same.commit varifyT_same;
    1.91 +val unvarifyT = Same.commit unvarifyT_same;
    1.92  
    1.93  fun varify tm = tm
    1.94 -  |> perhaps (Term_Subst.map_aterms_option
    1.95 -    (fn Free (x, T) => SOME (Var ((x, 0), T))
    1.96 +  |> Same.commit (Term_Subst.map_aterms_same
    1.97 +    (fn Free (x, T) => Var ((x, 0), T)
    1.98        | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
    1.99 -      | _ => NONE))
   1.100 -  |> perhaps (Term_Subst.map_types_option varifyT_option)
   1.101 +      | _ => raise Same.SAME))
   1.102 +  |> Same.commit (Term_Subst.map_types_same varifyT_same)
   1.103    handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   1.104  
   1.105  fun unvarify tm = tm
   1.106 -  |> perhaps (Term_Subst.map_aterms_option
   1.107 -    (fn Var ((x, 0), T) => SOME (Free (x, T))
   1.108 +  |> Same.commit (Term_Subst.map_aterms_same
   1.109 +    (fn Var ((x, 0), T) => Free (x, T)
   1.110        | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   1.111        | Free (x, _) => raise TERM (bad_fixed x, [tm])
   1.112 -      | _ => NONE))
   1.113 -  |> perhaps (Term_Subst.map_types_option unvarifyT_option)
   1.114 +      | _ => raise Same.SAME))
   1.115 +  |> Same.commit (Term_Subst.map_types_same unvarifyT_same)
   1.116    handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   1.117  
   1.118