# HG changeset patch
# User wenzelm
# Date 1303919925 -7200
# Node ID 4638622bcaa1f743341b3cc76ea8930e533bee56
# Parent  398d7d6bba4260d811f7831fbf79ff786bf0355b
reorganized fixes as specialized (global) name space;

diff -r 398d7d6bba42 -r 4638622bcaa1 src/HOL/Nominal/nominal_induct.ML
--- 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
diff -r 398d7d6bba42 -r 4638622bcaa1 src/HOL/Statespace/state_space.ML
--- 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
 
 
diff -r 398d7d6bba42 -r 4638622bcaa1 src/Pure/Isar/element.ML
--- 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
diff -r 398d7d6bba42 -r 4638622bcaa1 src/Pure/Isar/generic_target.ML
--- 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;
diff -r 398d7d6bba42 -r 4638622bcaa1 src/Pure/Isar/obtain.ML
--- 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;
diff -r 398d7d6bba42 -r 4638622bcaa1 src/Pure/Isar/proof_context.ML
--- 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 ::
diff -r 398d7d6bba42 -r 4638622bcaa1 src/Pure/Syntax/syntax_phases.ML
--- 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;
 
diff -r 398d7d6bba42 -r 4638622bcaa1 src/Pure/variable.ML
--- 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;
diff -r 398d7d6bba42 -r 4638622bcaa1 src/Tools/coherent.ML
--- 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
diff -r 398d7d6bba42 -r 4638622bcaa1 src/Tools/induct.ML
--- 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 =>