--- a/src/Pure/logic.ML Thu Jul 16 20:32:40 2009 +0200
+++ b/src/Pure/logic.ML Thu Jul 16 21:00:09 2009 +0200
@@ -304,44 +304,33 @@
| rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
-local exception SAME in
-
-fun incrT k =
- let
- fun incr (TVar ((a, i), S)) = TVar ((a, i + k), S)
- | incr (Type (a, Ts)) = Type (a, incrs Ts)
- | incr _ = raise SAME
- and incrs (T :: Ts) =
- (incr T :: (incrs Ts handle SAME => Ts)
- handle SAME => T :: incrs Ts)
- | incrs [] = raise SAME;
- in incr end;
+fun incrT k = Term_Subst.map_atypsT_same
+ (fn TVar ((a, i), S) => TVar ((a, i + k), S)
+ | _ => raise Same.SAME);
(*For all variables in the term, increment indexnames and lift over the Us
result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
fun incr_indexes ([], 0) t = t
| incr_indexes (Ts, k) t =
- let
- val n = length Ts;
- val incrT = if k = 0 then I else incrT k;
+ let
+ val n = length Ts;
+ val incrT = if k = 0 then I else incrT k;
- fun incr lev (Var ((x, i), T)) =
- combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n)
- | incr lev (Abs (x, T, body)) =
- (Abs (x, incrT T, incr (lev + 1) body handle SAME => body)
- handle SAME => Abs (x, T, incr (lev + 1) body))
- | incr lev (t $ u) =
- (incr lev t $ (incr lev u handle SAME => u)
- handle SAME => t $ incr lev u)
- | incr _ (Const (c, T)) = Const (c, incrT T)
- | incr _ (Free (x, T)) = Free (x, incrT T)
- | incr _ (t as Bound _) = t;
- in incr 0 t handle SAME => t end;
+ fun incr lev (Var ((x, i), T)) =
+ combound (Var ((x, i + k), Ts ---> Same.commit incrT T), lev, n)
+ | incr lev (Abs (x, T, body)) =
+ (Abs (x, incrT T, incr (lev + 1) body handle Same.SAME => body)
+ handle Same.SAME => Abs (x, T, incr (lev + 1) body))
+ | incr lev (t $ u) =
+ (incr lev t $ (incr lev u handle Same.SAME => u)
+ handle Same.SAME => t $ incr lev u)
+ | incr _ (Const (c, T)) = Const (c, incrT T)
+ | incr _ (Free (x, T)) = Free (x, incrT T)
+ | incr _ (t as Bound _) = t;
+ in incr 0 t handle Same.SAME => t end;
fun incr_tvar 0 T = T
- | incr_tvar k T = incrT k T handle SAME => T;
-
-end;
+ | incr_tvar k T = incrT k T handle Same.SAME => T;
(* Lifting functions from subgoal and increment:
@@ -473,35 +462,35 @@
fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
-fun varifyT_option ty = ty
- |> Term_Subst.map_atypsT_option
- (fn TFree (a, S) => SOME (TVar ((a, 0), S))
+fun varifyT_same ty = ty
+ |> Term_Subst.map_atypsT_same
+ (fn TFree (a, S) => TVar ((a, 0), S)
| TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
-fun unvarifyT_option ty = ty
- |> Term_Subst.map_atypsT_option
- (fn TVar ((a, 0), S) => SOME (TFree (a, S))
+fun unvarifyT_same ty = ty
+ |> Term_Subst.map_atypsT_same
+ (fn TVar ((a, 0), S) => TFree (a, S)
| TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
| TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
-val varifyT = perhaps varifyT_option;
-val unvarifyT = perhaps unvarifyT_option;
+val varifyT = Same.commit varifyT_same;
+val unvarifyT = Same.commit unvarifyT_same;
fun varify tm = tm
- |> perhaps (Term_Subst.map_aterms_option
- (fn Free (x, T) => SOME (Var ((x, 0), T))
+ |> Same.commit (Term_Subst.map_aterms_same
+ (fn Free (x, T) => Var ((x, 0), T)
| Var (xi, _) => raise TERM (bad_schematic xi, [tm])
- | _ => NONE))
- |> perhaps (Term_Subst.map_types_option varifyT_option)
+ | _ => raise Same.SAME))
+ |> Same.commit (Term_Subst.map_types_same varifyT_same)
handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
fun unvarify tm = tm
- |> perhaps (Term_Subst.map_aterms_option
- (fn Var ((x, 0), T) => SOME (Free (x, T))
+ |> Same.commit (Term_Subst.map_aterms_same
+ (fn Var ((x, 0), T) => Free (x, T)
| Var (xi, _) => raise TERM (bad_schematic xi, [tm])
| Free (x, _) => raise TERM (bad_fixed x, [tm])
- | _ => NONE))
- |> perhaps (Term_Subst.map_types_option unvarifyT_option)
+ | _ => raise Same.SAME))
+ |> Same.commit (Term_Subst.map_types_same unvarifyT_same)
handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
--- a/src/Pure/term.ML Thu Jul 16 20:32:40 2009 +0200
+++ b/src/Pure/term.ML Thu Jul 16 21:00:09 2009 +0200
@@ -634,31 +634,31 @@
*)
fun subst_bounds (args: term list, t) : term =
let
- exception SAME;
val n = length args;
fun subst (t as Bound i, lev) =
- (if i < lev then raise SAME (*var is locally bound*)
+ (if i < lev then raise Same.SAME (*var is locally bound*)
else incr_boundvars lev (nth args (i - lev))
handle Subscript => Bound (i - n)) (*loose: change it*)
| subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
| subst (f $ t, lev) =
- (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
- | subst _ = raise SAME;
- in case args of [] => t | _ => (subst (t, 0) handle SAME => t) end;
+ (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
+ handle Same.SAME => f $ subst (t, lev))
+ | subst _ = raise Same.SAME;
+ in case args of [] => t | _ => (subst (t, 0) handle Same.SAME => t) end;
(*Special case: one argument*)
fun subst_bound (arg, t) : term =
let
- exception SAME;
fun subst (Bound i, lev) =
- if i < lev then raise SAME (*var is locally bound*)
+ if i < lev then raise Same.SAME (*var is locally bound*)
else if i = lev then incr_boundvars lev arg
else Bound (i - 1) (*loose: change it*)
| subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
| subst (f $ t, lev) =
- (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
- | subst _ = raise SAME;
- in subst (t, 0) handle SAME => t end;
+ (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
+ handle Same.SAME => f $ subst (t, lev))
+ | subst _ = raise Same.SAME;
+ in subst (t, 0) handle Same.SAME => t end;
(*beta-reduce if possible, else form application*)
fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
@@ -708,15 +708,16 @@
The resulting term is ready to become the body of an Abs.*)
fun abstract_over (v, body) =
let
- exception SAME;
fun abs lev tm =
if v aconv tm then Bound lev
else
(case tm of
Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
- | t $ u => (abs lev t $ (abs lev u handle SAME => u) handle SAME => t $ abs lev u)
- | _ => raise SAME);
- in abs 0 body handle SAME => body end;
+ | t $ u =>
+ (abs lev t $ (abs lev u handle Same.SAME => u)
+ handle Same.SAME => t $ abs lev u)
+ | _ => raise Same.SAME);
+ in abs 0 body handle Same.SAME => body end;
fun lambda v t =
let val x =
--- a/src/Pure/term_subst.ML Thu Jul 16 20:32:40 2009 +0200
+++ b/src/Pure/term_subst.ML Thu Jul 16 21:00:09 2009 +0200
@@ -39,10 +39,8 @@
fun map_atypsT_same f =
let
- fun typ (Type (a, Ts)) = Type (a, typs Ts)
- | typ T = f T
- and typs (T :: Ts) = (typ T :: Same.commit typs Ts handle Same.SAME => T :: typs Ts)
- | typs [] = raise Same.SAME;
+ fun typ (Type (a, Ts)) = Type (a, Same.map typ Ts)
+ | typ T = f T;
in typ end;
fun map_types_same f =
@@ -50,7 +48,7 @@
fun term (Const (a, T)) = Const (a, f T)
| term (Free (a, T)) = Free (a, f T)
| term (Var (v, T)) = Var (v, f T)
- | term (Bound _) = raise Same.SAME
+ | term (Bound _) = raise Same.SAME
| term (Abs (x, T, t)) =
(Abs (x, f T, Same.commit term t)
handle Same.SAME => Abs (x, T, term t))
@@ -77,16 +75,12 @@
fun generalizeT_same [] _ _ = raise Same.SAME
| generalizeT_same tfrees idx ty =
let
- fun gen_typ (Type (a, Ts)) = Type (a, gen_typs Ts)
- | gen_typ (TFree (a, S)) =
+ fun gen (Type (a, Ts)) = Type (a, Same.map gen Ts)
+ | gen (TFree (a, S)) =
if member (op =) tfrees a then TVar ((a, idx), S)
else raise Same.SAME
- | gen_typ _ = raise Same.SAME
- and gen_typs (T :: Ts) =
- (gen_typ T :: Same.commit gen_typs Ts
- handle Same.SAME => T :: gen_typs Ts)
- | gen_typs [] = raise Same.SAME;
- in gen_typ ty end;
+ | gen _ = raise Same.SAME;
+ in gen ty end;
fun generalize_same ([], []) _ _ = raise Same.SAME
| generalize_same (tfrees, frees) idx tm =