--- a/src/HOL/Nominal/nominal_induct.ML Wed Apr 27 17:44:06 2011 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Wed Apr 27 17:58:45 2011 +0200
@@ -92,7 +92,7 @@
val finish_rule =
split_all_tuples
#> rename_params_rule true
- (map (Name.clean o Proof_Context.revert_skolem defs_ctxt o fst) avoiding);
+ (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding);
fun rule_cases ctxt r =
let val r' = if simp then Induct.simplified_rule ctxt r else r
--- a/src/HOL/Statespace/state_space.ML Wed Apr 27 17:44:06 2011 +0200
+++ b/src/HOL/Statespace/state_space.ML Wed Apr 27 17:58:45 2011 +0200
@@ -187,16 +187,11 @@
Symtab.lookup (StateSpaceData.get ctxt) name;
-fun lookupI eq xs n =
- (case AList.lookup eq xs n of
- SOME v => v
- | NONE => n);
-
fun mk_free ctxt name =
if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name
then
- let val n' = lookupI (op =) (Variable.fixes_of ctxt) name
- in SOME (Free (n',Proof_Context.infer_type ctxt (n', dummyT))) end
+ let val n' = Variable.intern_fixed ctxt name
+ in SOME (Free (n', Proof_Context.infer_type ctxt (n', dummyT))) end
else NONE
--- a/src/Pure/Isar/element.ML Wed Apr 27 17:44:06 2011 +0200
+++ b/src/Pure/Isar/element.ML Wed Apr 27 17:58:45 2011 +0200
@@ -222,7 +222,7 @@
fun obtain prop ctxt =
let
val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
- fun fix (x, T) = (Binding.name (Proof_Context.revert_skolem ctxt' x), SOME T);
+ fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T);
val xs = map (fix o Term.dest_Free o Thm.term_of o #2) ps;
val As = Logic.strip_imp_prems (Thm.term_of prop');
in ((Binding.empty, (xs, As)), ctxt') end;
@@ -242,7 +242,7 @@
val fixes = fold_aterms (fn v as Free (x, T) =>
if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
- then insert (op =) (Proof_Context.revert_skolem ctxt' x, T) else I | _ => I) prop [] |> rev;
+ then insert (op =) (Variable.revert_fixed ctxt' x, T) else I | _ => I) prop [] |> rev;
val (assumes, cases) = take_suffix (fn prem =>
is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
in
--- a/src/Pure/Isar/generic_target.ML Wed Apr 27 17:44:06 2011 +0200
+++ b/src/Pure/Isar/generic_target.ML Wed Apr 27 17:58:45 2011 +0200
@@ -67,12 +67,11 @@
val mx' = check_mixfix lthy (b, extra_tfrees) mx;
val type_params = map (Logic.mk_type o TFree) extra_tfrees;
+ val target_ctxt = Local_Theory.target_of lthy;
val term_params =
- rev (Variable.fixes_of (Local_Theory.target_of lthy))
- |> map_filter (fn (_, x) =>
- (case AList.lookup (op =) xs x of
- SOME T => SOME (Free (x, T))
- | NONE => NONE));
+ filter (Variable.is_fixed target_ctxt o #1) xs
+ |> sort (Variable.fixed_ord target_ctxt o pairself #1)
+ |> map Free;
val params = type_params @ term_params;
val U = map Term.fastype_of params ---> T;
--- a/src/Pure/Isar/obtain.ML Wed Apr 27 17:44:06 2011 +0200
+++ b/src/Pure/Isar/obtain.ML Wed Apr 27 17:58:45 2011 +0200
@@ -134,7 +134,7 @@
val asm_frees = fold Term.add_frees asm_props [];
val parms = xs |> map (fn x =>
- let val x' = Proof_Context.get_skolem fix_ctxt x
+ let val x' = Variable.intern_fixed fix_ctxt x
in (x', the_default propT (AList.lookup (op =) asm_frees x')) end);
val that_name = if name = "" then thatN else name;
--- a/src/Pure/Isar/proof_context.ML Wed Apr 27 17:44:06 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Apr 27 17:58:45 2011 +0200
@@ -63,8 +63,6 @@
val cert_typ: Proof.context -> typ -> typ
val cert_typ_syntax: Proof.context -> typ -> typ
val cert_typ_abbrev: Proof.context -> typ -> typ
- val get_skolem: Proof.context -> string -> string
- val revert_skolem: Proof.context -> string -> string
val infer_type: Proof.context -> string * typ -> typ
val inferred_param: string -> Proof.context -> typ * Proof.context
val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
@@ -408,10 +406,7 @@
(** prepare variables **)
-(* internalize Skolem constants *)
-
-val lookup_skolem = AList.lookup (op =) o Variable.fixes_of;
-fun get_skolem ctxt x = the_default x (lookup_skolem ctxt x);
+(* check Skolem constants *)
fun no_skolem internal x =
if can Name.dest_skolem x then
@@ -421,14 +416,6 @@
else x;
-(* revert Skolem constants -- if possible *)
-
-fun revert_skolem ctxt x =
- (case find_first (fn (_, y) => y = x) (Variable.fixes_of ctxt) of
- SOME (x', _) => if lookup_skolem ctxt x' = SOME x then x' else x
- | NONE => x);
-
-
(** prepare terms and propositions **)
@@ -443,7 +430,7 @@
fun inferred_fixes ctxt =
let
- val xs = rev (map #2 (Variable.fixes_of ctxt));
+ val xs = map #2 (Variable.dest_fixes ctxt);
val (Ts, ctxt') = fold_map inferred_param xs ctxt;
in (xs ~~ Ts, ctxt') end;
@@ -508,7 +495,7 @@
val (c, pos) = token_content text;
val _ = no_skolem false c;
in
- (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
+ (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
(SOME x, false) =>
(Context_Position.report ctxt pos
(Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free));
@@ -524,7 +511,7 @@
fun intern_skolem ctxt x =
let
val _ = no_skolem false x;
- val sko = lookup_skolem ctxt x;
+ val sko = Variable.lookup_fixed ctxt x;
val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x;
val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
in
@@ -1061,7 +1048,7 @@
val (_, ctxt') = ctxt |> add_fixes (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
fun bind (t as Free (x, T)) =
if member (op =) xs x then
- (case lookup_skolem ctxt' x of SOME x' => Free (x', T) | NONE => t)
+ (case Variable.lookup_fixed ctxt' x of SOME x' => Free (x', T) | NONE => t)
else t
| bind (t $ u) = bind t $ bind u
| bind (Abs (x, T, t)) = Abs (x, T, bind t)
@@ -1282,8 +1269,8 @@
if x = x' then Pretty.str x
else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
val fixes =
- rev (filter_out ((can Name.dest_internal orf member (op =) structs) o #1)
- (Variable.fixes_of ctxt));
+ filter_out ((can Name.dest_internal orf member (op =) structs) o #1)
+ (Variable.dest_fixes ctxt);
val prt_fixes =
if null fixes then []
else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
--- a/src/Pure/Syntax/syntax_phases.ML Wed Apr 27 17:44:06 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Wed Apr 27 17:58:45 2011 +0200
@@ -592,7 +592,7 @@
else Markup.hilite;
in
if can Name.dest_skolem x
- then ([m, Markup.skolem], Proof_Context.revert_skolem ctxt x)
+ then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
else ([m, Markup.free], x)
end;
--- a/src/Pure/variable.ML Wed Apr 27 17:44:06 2011 +0200
+++ b/src/Pure/variable.ML Wed Apr 27 17:58:45 2011 +0200
@@ -10,14 +10,11 @@
val set_body: bool -> Proof.context -> Proof.context
val restore_body: Proof.context -> Proof.context -> Proof.context
val names_of: Proof.context -> Name.context
- val fixes_of: Proof.context -> (string * string) list
val binds_of: Proof.context -> (typ * term) Vartab.table
val maxidx_of: Proof.context -> int
val sorts_of: Proof.context -> sort list
val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table
val is_declared: Proof.context -> string -> bool
- val is_fixed: Proof.context -> string -> bool
- val newly_fixed: Proof.context -> Proof.context -> string -> bool
val name: binding -> string
val default_type: Proof.context -> string -> typ option
val def_type: Proof.context -> bool -> indexname -> typ option
@@ -35,14 +32,22 @@
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 fixed_ord: Proof.context -> string * string -> order
+ val is_fixed: Proof.context -> string -> bool
+ val newly_fixed: Proof.context -> Proof.context -> string -> bool
+ val intern_fixed: Proof.context -> string -> string
+ val lookup_fixed: Proof.context -> string -> string option
+ val revert_fixed: Proof.context -> string -> string
val add_fixed_names: Proof.context -> term -> string list -> string list
val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list
val add_free_names: Proof.context -> term -> string list -> string list
val add_frees: Proof.context -> term -> (string * typ) list -> (string * typ) list
+ val add_fixes_binding: binding list -> Proof.context -> string list * Proof.context
val add_fixes: string list -> Proof.context -> string list * Proof.context
val add_fixes_direct: string list -> Proof.context -> Proof.context
val auto_fixes: term -> Proof.context -> Proof.context
val variant_fixes: string list -> Proof.context -> string list * Proof.context
+ val dest_fixes: Proof.context -> (string * string) list
val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
val export_terms: Proof.context -> Proof.context -> term list -> term list
val exportT_terms: Proof.context -> Proof.context -> term list -> term list
@@ -73,11 +78,14 @@
(** local context data **)
+type fixes = string Name_Space.table;
+val empty_fixes: fixes = Name_Space.empty_table "fixed variable";
+
datatype data = Data of
{is_body: bool, (*inner body mode*)
names: Name.context, (*type/term variable names*)
consts: string Symtab.table, (*consts within the local scope*)
- fixes: (string * string) list, (*term fixes -- extern/intern*)
+ 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*)
maxidx: int, (*maximum var index*)
@@ -94,8 +102,8 @@
(
type T = data;
fun init _ =
- make_data (false, Name.context, Symtab.empty, [], Vartab.empty, Symtab.empty,
- ~1, [], (Vartab.empty, Vartab.empty));
+ make_data (false, Name.context, Symtab.empty, empty_fixes, Vartab.empty,
+ Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty));
);
fun map_data f =
@@ -153,8 +161,6 @@
val constraints_of = #constraints o rep_data;
val is_declared = Name.is_declared o names_of;
-fun is_fixed ctxt x = exists (fn (_, y) => x = y) (fixes_of ctxt);
-fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
(*checked name binding*)
val name = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
@@ -281,6 +287,29 @@
(** fixes **)
+(* specialized name space *)
+
+fun fixed_ord ctxt = Name_Space.entry_ord (#1 (fixes_of ctxt));
+
+fun is_fixed ctxt x = can (Name_Space.the_entry (#1 (fixes_of ctxt))) x;
+fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
+
+fun intern_fixed ctxt = Name_Space.intern (#1 (fixes_of ctxt));
+
+fun lookup_fixed ctxt x =
+ let val x' = intern_fixed ctxt x
+ in if is_fixed ctxt x' then SOME x' else NONE end;
+
+fun revert_fixed ctxt x =
+ (case Symtab.lookup (#2 (fixes_of ctxt)) x of
+ SOME x' => if intern_fixed ctxt x' = x then x' else x
+ | NONE => x);
+
+fun dest_fixes ctxt =
+ let val (space, tab) = fixes_of ctxt
+ in sort (Name_Space.entry_ord space o pairself #2) (map swap (Symtab.dest tab)) end;
+
+
(* collect variables *)
fun add_free_names ctxt =
@@ -300,41 +329,54 @@
local
-fun no_dups [] = ()
- | no_dups dups = error ("Duplicate fixed variable(s): " ^ commas_quote dups);
+fun err_dups dups =
+ error ("Duplicate fixed variable(s): " ^ commas (map Binding.print dups));
-fun new_fixes names' xs xs' =
+fun new_fixed ((x, x'), pos) ctxt =
+ if is_some (lookup_fixed ctxt x') then err_dups [Binding.make (x, pos)]
+ else
+ ctxt
+ |> map_fixes
+ (Name_Space.define ctxt true Name_Space.default_naming (Binding.make (x', pos), x) #> snd #>>
+ Name_Space.alias Name_Space.default_naming (Binding.make (x, pos)) x')
+ |> declare_fixed x
+ |> declare_constraints (Syntax.free x');
+
+fun new_fixes names' xs xs' ps =
map_names (K names') #>
- fold declare_fixed xs #>
- map_fixes (fn fixes => (rev (xs ~~ xs') @ fixes)) #>
- fold (declare_constraints o Syntax.free) xs' #>
+ fold new_fixed ((xs ~~ xs') ~~ ps) #>
pair xs';
in
-fun add_fixes xs ctxt =
+fun add_fixes_binding bs ctxt =
let
val _ =
- (case filter (can Name.dest_skolem) xs of [] => ()
- | bads => error ("Illegal internal Skolem constant(s): " ^ commas_quote bads));
- val _ = no_dups (duplicates (op =) xs);
- val (ys, zs) = split_list (fixes_of ctxt);
+ (case filter (can Name.dest_skolem o Binding.name_of) bs of
+ [] => ()
+ | bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads)));
+ val _ =
+ (case duplicates (op = o pairself Binding.name_of) bs of
+ [] => ()
+ | dups => err_dups dups);
+
+ val xs = map name bs;
val names = names_of ctxt;
val (xs', names') =
if is_body ctxt then Name.variants xs names |>> map Name.skolem
- else (no_dups (inter (op =) xs ys); no_dups (inter (op =) xs zs);
- (xs, fold Name.declare xs names));
- in ctxt |> new_fixes names' xs xs' end;
+ else (xs, fold Name.declare xs names);
+ in ctxt |> new_fixes names' xs xs' (map Binding.pos_of bs) end;
fun variant_fixes raw_xs ctxt =
let
val names = names_of ctxt;
val xs = map (fn x => Name.clean x |> can Name.dest_internal x ? Name.internal) raw_xs;
val (xs', names') = Name.variants xs names |>> (is_body ctxt ? map Name.skolem);
- in ctxt |> new_fixes names' xs xs' end;
+ in ctxt |> new_fixes names' xs xs' (replicate (length xs) Position.none) end;
end;
+val add_fixes = add_fixes_binding o map Binding.name;
fun add_fixes_direct xs ctxt = ctxt
|> set_body false
@@ -358,10 +400,10 @@
fun export_inst inner outer =
let
val declared_outer = is_declared outer;
- val fixes_inner = fixes_of inner;
- val fixes_outer = fixes_of outer;
- val gen_fixes = map #2 (take (length fixes_inner - length fixes_outer) fixes_inner);
+ val gen_fixes =
+ Symtab.fold (fn (y, _) => not (is_fixed outer y) ? cons y)
+ (#2 (fixes_of inner)) [];
val still_fixed = not o member (op =) gen_fixes;
val type_occs_inner = type_occs_of inner;
--- a/src/Tools/coherent.ML Wed Apr 27 17:44:06 2011 +0200
+++ b/src/Tools/coherent.ML Wed Apr 27 17:58:45 2011 +0200
@@ -213,7 +213,7 @@
SUBPROOF (fn {prems = prems', concl, context, ...} =>
let val xs = map (term_of o #2) params @
map (fn (_, s) => Free (s, the (Variable.default_type context s)))
- (Variable.fixes_of context)
+ (rev (Variable.dest_fixes context)) (* FIXME !? *)
in
case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl)
(mk_dom xs) Net.empty 0 0 of
--- a/src/Tools/induct.ML Wed Apr 27 17:44:06 2011 +0200
+++ b/src/Tools/induct.ML Wed Apr 27 17:58:45 2011 +0200
@@ -599,7 +599,7 @@
fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] =
let
- val x = Name.clean (Proof_Context.revert_skolem ctxt z);
+ val x = Name.clean (Variable.revert_fixed ctxt z);
fun index i [] = []
| index i (y :: ys) =
if x = y then x ^ string_of_int i :: index (i + 1) ys
@@ -646,7 +646,7 @@
val v = Free (x, T);
fun spec_rule prfx (xs, body) =
@{thm Pure.meta_spec}
- |> Thm.rename_params_rule ([Name.clean (Proof_Context.revert_skolem ctxt x)], 1)
+ |> Thm.rename_params_rule ([Name.clean (Variable.revert_fixed ctxt x)], 1)
|> Thm.lift_rule (cert prfx)
|> `(Thm.prop_of #> Logic.strip_assums_concl)
|-> (fn pred $ arg =>