--- a/src/Pure/raw_simplifier.ML Wed Jan 15 19:02:58 2014 +0100
+++ b/src/Pure/raw_simplifier.ML Wed Jan 15 22:24:57 2014 +0100
@@ -249,8 +249,6 @@
(*A simpset contains data required during conversion:
rules: discrimination net of rewrite rules;
prems: current premises;
- bounds: maximal index of bound variables already used
- (for generating new names when rewriting under lambda abstractions);
depth: simp_depth and exceeded flag;
congs: association list of congruence rules and
a list of `weak' congruence constants.
@@ -268,7 +266,6 @@
Simpset of
{rules: rrule Net.net,
prems: thm list,
- bounds: int * ((string * typ) * string) list,
depth: int * bool Unsynchronized.ref} *
{congs: (cong_name * thm) list * cong_name list,
procs: proc Net.net,
@@ -285,11 +282,9 @@
fun internal_ss (Simpset (_, ss2)) = ss2;
-fun make_ss1 (rules, prems, bounds, depth) =
- {rules = rules, prems = prems, bounds = bounds, depth = depth};
+fun make_ss1 (rules, prems, depth) = {rules = rules, prems = prems, depth = depth};
-fun map_ss1 f {rules, prems, bounds, depth} =
- make_ss1 (f (rules, prems, bounds, depth));
+fun map_ss1 f {rules, prems, depth} = make_ss1 (f (rules, prems, depth));
fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =
{congs = congs, procs = procs, mk_rews = mk_rews, termless = termless,
@@ -316,16 +311,14 @@
(* empty *)
-fun init_ss bounds depth mk_rews termless subgoal_tac solvers =
- make_simpset ((Net.empty, [], bounds, depth),
+fun init_ss depth mk_rews termless subgoal_tac solvers =
+ make_simpset ((Net.empty, [], depth),
(([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
fun default_mk_sym _ th = SOME (th RS Drule.symmetric_thm);
val empty_ss =
- init_ss
- (0, [])
- (0, Unsynchronized.ref false)
+ init_ss (0, Unsynchronized.ref false)
{mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
mk_cong = K I,
mk_sym = default_mk_sym,
@@ -340,16 +333,15 @@
if pointer_eq (ss1, ss2) then ss1
else
let
- val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1},
+ val Simpset ({rules = rules1, prems = prems1, depth = depth1},
{congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac,
loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
- val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2},
+ val Simpset ({rules = rules2, prems = prems2, depth = depth2},
{congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
val rules' = Net.merge eq_rrule (rules1, rules2);
val prems' = Thm.merge_thms (prems1, prems2);
- val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2);
val weak' = merge (op =) (weak1, weak2);
@@ -358,7 +350,7 @@
val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
val solvers' = merge eq_solver (solvers1, solvers2);
in
- make_simpset ((rules', prems', bounds', depth'), ((congs', weak'), procs',
+ make_simpset ((rules', prems', depth'), ((congs', weak'), procs',
mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
end;
@@ -385,8 +377,8 @@
fun put_simpset ss = map_simpset (fn context_ss =>
let
val Simpset ({rules, prems, ...}, ss2) = ss; (* FIXME prems from context (!?) *)
- val Simpset ({bounds, depth, ...}, _) = context_ss;
- in Simpset (make_ss1 (rules, prems, bounds, depth), ss2) end);
+ val Simpset ({depth, ...}, _) = context_ss;
+ in Simpset (make_ss1 (rules, prems, depth), ss2) end);
val empty_simpset = put_simpset empty_ss;
@@ -399,8 +391,8 @@
fun map_ss f = Context.mapping (map_theory_simpset f) f;
val clear_simpset =
- map_simpset (fn Simpset ({bounds, depth, ...}, {mk_rews, termless, subgoal_tac, solvers, ...}) =>
- init_ss bounds depth mk_rews termless subgoal_tac solvers);
+ map_simpset (fn Simpset ({depth, ...}, {mk_rews, termless, subgoal_tac, solvers, ...}) =>
+ init_ss depth mk_rews termless subgoal_tac solvers);
(* simp depth *)
@@ -424,8 +416,8 @@
end;
fun inc_simp_depth ctxt =
- ctxt |> map_simpset1 (fn (rules, prems, bounds, (depth, exceeded)) =>
- (rules, prems, bounds,
+ ctxt |> map_simpset1 (fn (rules, prems, (depth, exceeded)) =>
+ (rules, prems,
(depth + 1,
if depth = Config.get ctxt simp_trace_depth_limit
then Unsynchronized.ref false else exceeded)));
@@ -448,23 +440,9 @@
fun if_enabled ctxt flag f = if Config.get ctxt flag then f ctxt else ();
-local
-
fun prnt ctxt warn a = if warn then warning a else trace_depth ctxt a;
-fun show_bounds ctxt t =
- let
- val Simpset ({bounds = (_, bs), ...}, _) = simpset_of ctxt;
- val names = Term.declare_term_names t Name.context;
- val xs = rev (#1 (fold_map Name.variant (rev (map #2 bs)) names));
- fun subst (((b, T), _), x') = (Free (b, T), Syntax_Trans.mark_bound_abs (x', T));
- in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
-
-in
-
-fun print_term ctxt warn a t =
- prnt ctxt warn (a () ^ "\n" ^
- Syntax.string_of_term ctxt (if Config.get ctxt simp_debug then t else show_bounds ctxt t));
+fun print_term ctxt warn a t = prnt ctxt warn (a () ^ "\n" ^ Syntax.string_of_term ctxt t);
fun debug ctxt warn a = if_enabled ctxt simp_debug (fn _ => prnt ctxt warn (a ()));
fun trace ctxt warn a = if_enabled ctxt simp_trace (fn _ => prnt ctxt warn (a ()));
@@ -487,41 +465,33 @@
fun warn_thm ctxt a th = print_term ctxt true a (Thm.full_prop_of th);
fun cond_warn_thm ctxt a th = Context_Position.if_visible ctxt (fn () => warn_thm ctxt a th) ();
-end;
-
(** simpset operations **)
-(* context *)
-
-fun eq_bound (x: string, (y, _)) = x = y;
-
-fun add_bound bound =
- map_simpset1 (fn (rules, prems, (count, bounds), depth) =>
- (rules, prems, (count + 1, bound :: bounds), depth));
+(* prems *)
fun prems_of ctxt =
let val Simpset ({prems, ...}, _) = simpset_of ctxt in prems end;
fun add_prems ths =
- map_simpset1 (fn (rules, prems, bounds, depth) => (rules, ths @ prems, bounds, depth));
+ map_simpset1 (fn (rules, prems, depth) => (rules, ths @ prems, depth));
(* maintain simp rules *)
fun del_rrule (rrule as {thm, elhs, ...}) ctxt =
- ctxt |> map_simpset1 (fn (rules, prems, bounds, depth) =>
- (Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, bounds, depth))
+ ctxt |> map_simpset1 (fn (rules, prems, depth) =>
+ (Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, depth))
handle Net.DELETE => (cond_warn_thm ctxt (fn () => "Rewrite rule not in simpset:") thm; ctxt);
fun insert_rrule (rrule as {thm, name, ...}) ctxt =
(trace_named_thm ctxt (fn () => "Adding rewrite rule") (thm, name);
- ctxt |> map_simpset1 (fn (rules, prems, bounds, depth) =>
+ ctxt |> map_simpset1 (fn (rules, prems, depth) =>
let
val rrule2 as {elhs, ...} = mk_rrule2 rrule;
val rules' = Net.insert_term eq_rrule (term_of elhs, rrule2) rules;
- in (rules', prems, bounds, depth) end)
+ in (rules', prems, depth) end)
handle Net.INSERT => (cond_warn_thm ctxt (fn () => "Ignoring duplicate rewrite rule:") thm; ctxt));
local
@@ -1112,11 +1082,11 @@
| NONE => Thm.reflexive t)
and subc skel ctxt t0 =
- let val Simpset ({bounds, ...}, {congs, ...}) = simpset_of ctxt in
+ let val Simpset (_, {congs, ...}) = simpset_of ctxt in
(case term_of t0 of
Abs (a, T, _) =>
let
- val b = Name.bound (#1 bounds);
+ val (b, ctxt') = Variable.next_bound (a, T) ctxt;
val (v, t') = Thm.dest_abs (SOME b) t0;
val b' = #1 (Term.dest_Free (Thm.term_of v));
val _ =
@@ -1124,7 +1094,6 @@
warning ("Simplifier: renamed bound variable " ^
quote b ^ " to " ^ quote b' ^ Position.here (Position.thread_data ()))
else ();
- val ctxt' = add_bound ((b', T), a) ctxt;
val skel' = (case skel of Abs (_, _, sk) => sk | _ => skel0);
in
(case botc skel' ctxt' t' of
--- a/src/Pure/variable.ML Wed Jan 15 19:02:58 2014 +0100
+++ b/src/Pure/variable.ML Wed Jan 15 22:24:57 2014 +0100
@@ -32,6 +32,8 @@
val lookup_const: Proof.context -> string -> string option
val is_const: Proof.context -> string -> bool
val declare_const: string * string -> Proof.context -> Proof.context
+ val next_bound: string * typ -> Proof.context -> string * Proof.context
+ val revert_bounds: Proof.context -> term -> term
val is_fixed: Proof.context -> string -> bool
val newly_fixed: Proof.context -> Proof.context -> string -> bool
val fixed_ord: Proof.context -> string * string -> order
@@ -87,6 +89,7 @@
{is_body: bool, (*inner body mode*)
names: Name.context, (*type/term variable names*)
consts: string Symtab.table, (*consts within the local scope*)
+ bounds: int * ((string * typ) * string) list, (*next index, internal name, type, external name*)
fixes: fixes, (*term fixes -- global name space, intern ~> extern*)
binds: (typ * term) Vartab.table, (*term bindings*)
type_occs: string list Symtab.table, (*type variables -- possibly within term variables*)
@@ -96,61 +99,77 @@
typ Vartab.table * (*type constraints*)
sort Vartab.table}; (*default sorts*)
-fun make_data (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) =
- Data {is_body = is_body, names = names, consts = consts, fixes = fixes, binds = binds,
- type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints};
+fun make_data
+ (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =
+ Data {is_body = is_body, names = names, consts = consts, bounds = bounds, fixes = fixes,
+ binds = binds, type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints};
structure Data = Proof_Data
(
type T = data;
fun init _ =
- make_data (false, Name.context, Symtab.empty, empty_fixes, Vartab.empty,
+ make_data (false, Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty,
Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty));
);
fun map_data f =
- Data.map (fn Data {is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints} =>
- make_data (f (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints)));
+ Data.map (fn
+ Data {is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints} =>
+ make_data
+ (f (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)));
fun map_names f =
- map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) =>
- (is_body, f names, consts, fixes, binds, type_occs, maxidx, sorts, constraints));
+ map_data (fn
+ (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+ (is_body, f names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
fun map_consts f =
- map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) =>
- (is_body, names, f consts, fixes, binds, type_occs, maxidx, sorts, constraints));
+ map_data (fn
+ (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+ (is_body, names, f consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
+
+fun map_bounds f =
+ map_data (fn
+ (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+ (is_body, names, consts, f bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
fun map_fixes f =
- map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) =>
- (is_body, names, consts, f fixes, binds, type_occs, maxidx, sorts, constraints));
+ map_data (fn
+ (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+ (is_body, names, consts, bounds, f fixes, binds, type_occs, maxidx, sorts, constraints));
fun map_binds f =
- map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) =>
- (is_body, names, consts, fixes, f binds, type_occs, maxidx, sorts, constraints));
+ map_data (fn
+ (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+ (is_body, names, consts, bounds, fixes, f binds, type_occs, maxidx, sorts, constraints));
fun map_type_occs f =
- map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) =>
- (is_body, names, consts, fixes, binds, f type_occs, maxidx, sorts, constraints));
+ map_data (fn
+ (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+ (is_body, names, consts, bounds, fixes, binds, f type_occs, maxidx, sorts, constraints));
fun map_maxidx f =
- map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) =>
- (is_body, names, consts, fixes, binds, type_occs, f maxidx, sorts, constraints));
+ map_data (fn
+ (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+ (is_body, names, consts, bounds, fixes, binds, type_occs, f maxidx, sorts, constraints));
fun map_sorts f =
- map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) =>
- (is_body, names, consts, fixes, binds, type_occs, maxidx, f sorts, constraints));
+ map_data (fn
+ (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+ (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, f sorts, constraints));
fun map_constraints f =
- map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) =>
- (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, f constraints));
+ map_data (fn
+ (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+ (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, f constraints));
fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
val is_body = #is_body o rep_data;
fun set_body b =
- map_data (fn (_, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) =>
- (b, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints));
+ map_data (fn (_, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) =>
+ (b, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints));
fun restore_body ctxt = set_body (is_body ctxt);
@@ -288,6 +307,26 @@
+(** bounds **)
+
+fun next_bound (a, T) ctxt =
+ let
+ val b = Name.bound (#1 (#bounds (rep_data ctxt)));
+ val ctxt' = ctxt |> map_bounds (fn (next, bounds) => (next + 1, ((b, T), a) :: bounds));
+ in (b, ctxt') end;
+
+fun revert_bounds ctxt t =
+ (case #2 (#bounds (rep_data ctxt)) of
+ [] => t
+ | bounds =>
+ let
+ val names = Term.declare_term_names t (names_of ctxt);
+ val xs = rev (#1 (fold_map Name.variant (rev (map #2 bounds)) names));
+ fun subst ((b, T), _) x' = (Free (b, T), Syntax_Trans.mark_bound_abs (x', T));
+ in Term.subst_atomic (map2 subst bounds xs) t end);
+
+
+
(** fixes **)
(* specialized name space *)