reorganized fixes as specialized (global) name space;
authorwenzelm
Wed Apr 27 17:58:45 2011 +0200 (2011-04-27)
changeset 424884638622bcaa1
parent 42487 398d7d6bba42
child 42489 db9b9e46131c
reorganized fixes as specialized (global) name space;
src/HOL/Nominal/nominal_induct.ML
src/HOL/Statespace/state_space.ML
src/Pure/Isar/element.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/variable.ML
src/Tools/coherent.ML
src/Tools/induct.ML
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Wed Apr 27 17:44:06 2011 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Wed Apr 27 17:58:45 2011 +0200
     1.3 @@ -92,7 +92,7 @@
     1.4      val finish_rule =
     1.5        split_all_tuples
     1.6        #> rename_params_rule true
     1.7 -        (map (Name.clean o Proof_Context.revert_skolem defs_ctxt o fst) avoiding);
     1.8 +        (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding);
     1.9  
    1.10      fun rule_cases ctxt r =
    1.11        let val r' = if simp then Induct.simplified_rule ctxt r else r
     2.1 --- a/src/HOL/Statespace/state_space.ML	Wed Apr 27 17:44:06 2011 +0200
     2.2 +++ b/src/HOL/Statespace/state_space.ML	Wed Apr 27 17:58:45 2011 +0200
     2.3 @@ -187,16 +187,11 @@
     2.4        Symtab.lookup (StateSpaceData.get ctxt) name;
     2.5  
     2.6  
     2.7 -fun lookupI eq xs n =
     2.8 -  (case AList.lookup eq xs n of
     2.9 -     SOME v => v
    2.10 -   | NONE => n);
    2.11 -
    2.12  fun mk_free ctxt name =
    2.13    if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name
    2.14    then
    2.15 -    let val n' = lookupI (op =) (Variable.fixes_of ctxt) name
    2.16 -    in SOME (Free (n',Proof_Context.infer_type ctxt (n', dummyT))) end
    2.17 +    let val n' = Variable.intern_fixed ctxt name
    2.18 +    in SOME (Free (n', Proof_Context.infer_type ctxt (n', dummyT))) end
    2.19    else NONE
    2.20  
    2.21  
     3.1 --- a/src/Pure/Isar/element.ML	Wed Apr 27 17:44:06 2011 +0200
     3.2 +++ b/src/Pure/Isar/element.ML	Wed Apr 27 17:58:45 2011 +0200
     3.3 @@ -222,7 +222,7 @@
     3.4  fun obtain prop ctxt =
     3.5    let
     3.6      val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
     3.7 -    fun fix (x, T) = (Binding.name (Proof_Context.revert_skolem ctxt' x), SOME T);
     3.8 +    fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T);
     3.9      val xs = map (fix o Term.dest_Free o Thm.term_of o #2) ps;
    3.10      val As = Logic.strip_imp_prems (Thm.term_of prop');
    3.11    in ((Binding.empty, (xs, As)), ctxt') end;
    3.12 @@ -242,7 +242,7 @@
    3.13  
    3.14      val fixes = fold_aterms (fn v as Free (x, T) =>
    3.15          if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
    3.16 -        then insert (op =) (Proof_Context.revert_skolem ctxt' x, T) else I | _ => I) prop [] |> rev;
    3.17 +        then insert (op =) (Variable.revert_fixed ctxt' x, T) else I | _ => I) prop [] |> rev;
    3.18      val (assumes, cases) = take_suffix (fn prem =>
    3.19        is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
    3.20    in
     4.1 --- a/src/Pure/Isar/generic_target.ML	Wed Apr 27 17:44:06 2011 +0200
     4.2 +++ b/src/Pure/Isar/generic_target.ML	Wed Apr 27 17:58:45 2011 +0200
     4.3 @@ -67,12 +67,11 @@
     4.4      val mx' = check_mixfix lthy (b, extra_tfrees) mx;
     4.5  
     4.6      val type_params = map (Logic.mk_type o TFree) extra_tfrees;
     4.7 +    val target_ctxt = Local_Theory.target_of lthy;
     4.8      val term_params =
     4.9 -      rev (Variable.fixes_of (Local_Theory.target_of lthy))
    4.10 -      |> map_filter (fn (_, x) =>
    4.11 -        (case AList.lookup (op =) xs x of
    4.12 -          SOME T => SOME (Free (x, T))
    4.13 -        | NONE => NONE));
    4.14 +      filter (Variable.is_fixed target_ctxt o #1) xs
    4.15 +      |> sort (Variable.fixed_ord target_ctxt o pairself #1)
    4.16 +      |> map Free;
    4.17      val params = type_params @ term_params;
    4.18  
    4.19      val U = map Term.fastype_of params ---> T;
     5.1 --- a/src/Pure/Isar/obtain.ML	Wed Apr 27 17:44:06 2011 +0200
     5.2 +++ b/src/Pure/Isar/obtain.ML	Wed Apr 27 17:58:45 2011 +0200
     5.3 @@ -134,7 +134,7 @@
     5.4  
     5.5      val asm_frees = fold Term.add_frees asm_props [];
     5.6      val parms = xs |> map (fn x =>
     5.7 -      let val x' = Proof_Context.get_skolem fix_ctxt x
     5.8 +      let val x' = Variable.intern_fixed fix_ctxt x
     5.9        in (x', the_default propT (AList.lookup (op =) asm_frees x')) end);
    5.10  
    5.11      val that_name = if name = "" then thatN else name;
     6.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 27 17:44:06 2011 +0200
     6.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 27 17:58:45 2011 +0200
     6.3 @@ -63,8 +63,6 @@
     6.4    val cert_typ: Proof.context -> typ -> typ
     6.5    val cert_typ_syntax: Proof.context -> typ -> typ
     6.6    val cert_typ_abbrev: Proof.context -> typ -> typ
     6.7 -  val get_skolem: Proof.context -> string -> string
     6.8 -  val revert_skolem: Proof.context -> string -> string
     6.9    val infer_type: Proof.context -> string * typ -> typ
    6.10    val inferred_param: string -> Proof.context -> typ * Proof.context
    6.11    val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
    6.12 @@ -408,10 +406,7 @@
    6.13  
    6.14  (** prepare variables **)
    6.15  
    6.16 -(* internalize Skolem constants *)
    6.17 -
    6.18 -val lookup_skolem = AList.lookup (op =) o Variable.fixes_of;
    6.19 -fun get_skolem ctxt x = the_default x (lookup_skolem ctxt x);
    6.20 +(* check Skolem constants *)
    6.21  
    6.22  fun no_skolem internal x =
    6.23    if can Name.dest_skolem x then
    6.24 @@ -421,14 +416,6 @@
    6.25    else x;
    6.26  
    6.27  
    6.28 -(* revert Skolem constants -- if possible *)
    6.29 -
    6.30 -fun revert_skolem ctxt x =
    6.31 -  (case find_first (fn (_, y) => y = x) (Variable.fixes_of ctxt) of
    6.32 -    SOME (x', _) => if lookup_skolem ctxt x' = SOME x then x' else x
    6.33 -  | NONE => x);
    6.34 -
    6.35 -
    6.36  
    6.37  (** prepare terms and propositions **)
    6.38  
    6.39 @@ -443,7 +430,7 @@
    6.40  
    6.41  fun inferred_fixes ctxt =
    6.42    let
    6.43 -    val xs = rev (map #2 (Variable.fixes_of ctxt));
    6.44 +    val xs = map #2 (Variable.dest_fixes ctxt);
    6.45      val (Ts, ctxt') = fold_map inferred_param xs ctxt;
    6.46    in (xs ~~ Ts, ctxt') end;
    6.47  
    6.48 @@ -508,7 +495,7 @@
    6.49      val (c, pos) = token_content text;
    6.50      val _ = no_skolem false c;
    6.51    in
    6.52 -    (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
    6.53 +    (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
    6.54        (SOME x, false) =>
    6.55          (Context_Position.report ctxt pos
    6.56              (Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free));
    6.57 @@ -524,7 +511,7 @@
    6.58  fun intern_skolem ctxt x =
    6.59    let
    6.60      val _ = no_skolem false x;
    6.61 -    val sko = lookup_skolem ctxt x;
    6.62 +    val sko = Variable.lookup_fixed ctxt x;
    6.63      val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x;
    6.64      val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
    6.65    in
    6.66 @@ -1061,7 +1048,7 @@
    6.67      val (_, ctxt') = ctxt |> add_fixes (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
    6.68      fun bind (t as Free (x, T)) =
    6.69            if member (op =) xs x then
    6.70 -            (case lookup_skolem ctxt' x of SOME x' => Free (x', T) | NONE => t)
    6.71 +            (case Variable.lookup_fixed ctxt' x of SOME x' => Free (x', T) | NONE => t)
    6.72            else t
    6.73        | bind (t $ u) = bind t $ bind u
    6.74        | bind (Abs (x, T, t)) = Abs (x, T, bind t)
    6.75 @@ -1282,8 +1269,8 @@
    6.76          if x = x' then Pretty.str x
    6.77          else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
    6.78        val fixes =
    6.79 -        rev (filter_out ((can Name.dest_internal orf member (op =) structs) o #1)
    6.80 -          (Variable.fixes_of ctxt));
    6.81 +        filter_out ((can Name.dest_internal orf member (op =) structs) o #1)
    6.82 +          (Variable.dest_fixes ctxt);
    6.83        val prt_fixes =
    6.84          if null fixes then []
    6.85          else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
     7.1 --- a/src/Pure/Syntax/syntax_phases.ML	Wed Apr 27 17:44:06 2011 +0200
     7.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Wed Apr 27 17:58:45 2011 +0200
     7.3 @@ -592,7 +592,7 @@
     7.4        else Markup.hilite;
     7.5    in
     7.6      if can Name.dest_skolem x
     7.7 -    then ([m, Markup.skolem], Proof_Context.revert_skolem ctxt x)
     7.8 +    then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
     7.9      else ([m, Markup.free], x)
    7.10    end;
    7.11  
     8.1 --- a/src/Pure/variable.ML	Wed Apr 27 17:44:06 2011 +0200
     8.2 +++ b/src/Pure/variable.ML	Wed Apr 27 17:58:45 2011 +0200
     8.3 @@ -10,14 +10,11 @@
     8.4    val set_body: bool -> Proof.context -> Proof.context
     8.5    val restore_body: Proof.context -> Proof.context -> Proof.context
     8.6    val names_of: Proof.context -> Name.context
     8.7 -  val fixes_of: Proof.context -> (string * string) list
     8.8    val binds_of: Proof.context -> (typ * term) Vartab.table
     8.9    val maxidx_of: Proof.context -> int
    8.10    val sorts_of: Proof.context -> sort list
    8.11    val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table
    8.12    val is_declared: Proof.context -> string -> bool
    8.13 -  val is_fixed: Proof.context -> string -> bool
    8.14 -  val newly_fixed: Proof.context -> Proof.context -> string -> bool
    8.15    val name: binding -> string
    8.16    val default_type: Proof.context -> string -> typ option
    8.17    val def_type: Proof.context -> bool -> indexname -> typ option
    8.18 @@ -35,14 +32,22 @@
    8.19    val lookup_const: Proof.context -> string -> string option
    8.20    val is_const: Proof.context -> string -> bool
    8.21    val declare_const: string * string -> Proof.context -> Proof.context
    8.22 +  val fixed_ord: Proof.context -> string * string -> order
    8.23 +  val is_fixed: Proof.context -> string -> bool
    8.24 +  val newly_fixed: Proof.context -> Proof.context -> string -> bool
    8.25 +  val intern_fixed: Proof.context -> string -> string
    8.26 +  val lookup_fixed: Proof.context -> string -> string option
    8.27 +  val revert_fixed: Proof.context -> string -> string
    8.28    val add_fixed_names: Proof.context -> term -> string list -> string list
    8.29    val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list
    8.30    val add_free_names: Proof.context -> term -> string list -> string list
    8.31    val add_frees: Proof.context -> term -> (string * typ) list -> (string * typ) list
    8.32 +  val add_fixes_binding: binding list -> Proof.context -> string list * Proof.context
    8.33    val add_fixes: string list -> Proof.context -> string list * Proof.context
    8.34    val add_fixes_direct: string list -> Proof.context -> Proof.context
    8.35    val auto_fixes: term -> Proof.context -> Proof.context
    8.36    val variant_fixes: string list -> Proof.context -> string list * Proof.context
    8.37 +  val dest_fixes: Proof.context -> (string * string) list
    8.38    val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
    8.39    val export_terms: Proof.context -> Proof.context -> term list -> term list
    8.40    val exportT_terms: Proof.context -> Proof.context -> term list -> term list
    8.41 @@ -73,11 +78,14 @@
    8.42  
    8.43  (** local context data **)
    8.44  
    8.45 +type fixes = string Name_Space.table;
    8.46 +val empty_fixes: fixes = Name_Space.empty_table "fixed variable";
    8.47 +
    8.48  datatype data = Data of
    8.49   {is_body: bool,                        (*inner body mode*)
    8.50    names: Name.context,                  (*type/term variable names*)
    8.51    consts: string Symtab.table,          (*consts within the local scope*)
    8.52 -  fixes: (string * string) list,        (*term fixes -- extern/intern*)
    8.53 +  fixes: fixes,                         (*term fixes -- global name space, intern ~> extern*)
    8.54    binds: (typ * term) Vartab.table,     (*term bindings*)
    8.55    type_occs: string list Symtab.table,  (*type variables -- possibly within term variables*)
    8.56    maxidx: int,                          (*maximum var index*)
    8.57 @@ -94,8 +102,8 @@
    8.58  (
    8.59    type T = data;
    8.60    fun init _ =
    8.61 -    make_data (false, Name.context, Symtab.empty, [], Vartab.empty, Symtab.empty,
    8.62 -      ~1, [], (Vartab.empty, Vartab.empty));
    8.63 +    make_data (false, Name.context, Symtab.empty, empty_fixes, Vartab.empty,
    8.64 +      Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty));
    8.65  );
    8.66  
    8.67  fun map_data f =
    8.68 @@ -153,8 +161,6 @@
    8.69  val constraints_of = #constraints o rep_data;
    8.70  
    8.71  val is_declared = Name.is_declared o names_of;
    8.72 -fun is_fixed ctxt x = exists (fn (_, y) => x = y) (fixes_of ctxt);
    8.73 -fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
    8.74  
    8.75  (*checked name binding*)
    8.76  val name = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
    8.77 @@ -281,6 +287,29 @@
    8.78  
    8.79  (** fixes **)
    8.80  
    8.81 +(* specialized name space *)
    8.82 +
    8.83 +fun fixed_ord ctxt = Name_Space.entry_ord (#1 (fixes_of ctxt));
    8.84 +
    8.85 +fun is_fixed ctxt x = can (Name_Space.the_entry (#1 (fixes_of ctxt))) x;
    8.86 +fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
    8.87 +
    8.88 +fun intern_fixed ctxt = Name_Space.intern (#1 (fixes_of ctxt));
    8.89 +
    8.90 +fun lookup_fixed ctxt x =
    8.91 +  let val x' = intern_fixed ctxt x
    8.92 +  in if is_fixed ctxt x' then SOME x' else NONE end;
    8.93 +
    8.94 +fun revert_fixed ctxt x =
    8.95 +  (case Symtab.lookup (#2 (fixes_of ctxt)) x of
    8.96 +    SOME x' => if intern_fixed ctxt x' = x then x' else x
    8.97 +  | NONE => x);
    8.98 +
    8.99 +fun dest_fixes ctxt =
   8.100 +  let val (space, tab) = fixes_of ctxt
   8.101 +  in sort (Name_Space.entry_ord space o pairself #2) (map swap (Symtab.dest tab)) end;
   8.102 +
   8.103 +
   8.104  (* collect variables *)
   8.105  
   8.106  fun add_free_names ctxt =
   8.107 @@ -300,41 +329,54 @@
   8.108  
   8.109  local
   8.110  
   8.111 -fun no_dups [] = ()
   8.112 -  | no_dups dups = error ("Duplicate fixed variable(s): " ^ commas_quote dups);
   8.113 +fun err_dups dups =
   8.114 +  error ("Duplicate fixed variable(s): " ^ commas (map Binding.print dups));
   8.115  
   8.116 -fun new_fixes names' xs xs' =
   8.117 +fun new_fixed ((x, x'), pos) ctxt =
   8.118 +  if is_some (lookup_fixed ctxt x') then err_dups [Binding.make (x, pos)]
   8.119 +  else
   8.120 +    ctxt
   8.121 +    |> map_fixes
   8.122 +      (Name_Space.define ctxt true Name_Space.default_naming (Binding.make (x', pos), x) #> snd #>>
   8.123 +        Name_Space.alias Name_Space.default_naming (Binding.make (x, pos)) x')
   8.124 +    |> declare_fixed x
   8.125 +    |> declare_constraints (Syntax.free x');
   8.126 +
   8.127 +fun new_fixes names' xs xs' ps =
   8.128    map_names (K names') #>
   8.129 -  fold declare_fixed xs #>
   8.130 -  map_fixes (fn fixes => (rev (xs ~~ xs') @ fixes)) #>
   8.131 -  fold (declare_constraints o Syntax.free) xs' #>
   8.132 +  fold new_fixed ((xs ~~ xs') ~~ ps) #>
   8.133    pair xs';
   8.134  
   8.135  in
   8.136  
   8.137 -fun add_fixes xs ctxt =
   8.138 +fun add_fixes_binding bs ctxt =
   8.139    let
   8.140      val _ =
   8.141 -      (case filter (can Name.dest_skolem) xs of [] => ()
   8.142 -      | bads => error ("Illegal internal Skolem constant(s): " ^ commas_quote bads));
   8.143 -    val _ = no_dups (duplicates (op =) xs);
   8.144 -    val (ys, zs) = split_list (fixes_of ctxt);
   8.145 +      (case filter (can Name.dest_skolem o Binding.name_of) bs of
   8.146 +        [] => ()
   8.147 +      | bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads)));
   8.148 +    val _ =
   8.149 +      (case duplicates (op = o pairself Binding.name_of) bs of
   8.150 +        [] => ()
   8.151 +      | dups => err_dups dups);
   8.152 +
   8.153 +    val xs = map name bs;
   8.154      val names = names_of ctxt;
   8.155      val (xs', names') =
   8.156        if is_body ctxt then Name.variants xs names |>> map Name.skolem
   8.157 -      else (no_dups (inter (op =) xs ys); no_dups (inter (op =) xs zs);
   8.158 -        (xs, fold Name.declare xs names));
   8.159 -  in ctxt |> new_fixes names' xs xs' end;
   8.160 +      else (xs, fold Name.declare xs names);
   8.161 +  in ctxt |> new_fixes names' xs xs' (map Binding.pos_of bs) end;
   8.162  
   8.163  fun variant_fixes raw_xs ctxt =
   8.164    let
   8.165      val names = names_of ctxt;
   8.166      val xs = map (fn x => Name.clean x |> can Name.dest_internal x ? Name.internal) raw_xs;
   8.167      val (xs', names') = Name.variants xs names |>> (is_body ctxt ? map Name.skolem);
   8.168 -  in ctxt |> new_fixes names' xs xs' end;
   8.169 +  in ctxt |> new_fixes names' xs xs' (replicate (length xs) Position.none) end;
   8.170  
   8.171  end;
   8.172  
   8.173 +val add_fixes = add_fixes_binding o map Binding.name;
   8.174  
   8.175  fun add_fixes_direct xs ctxt = ctxt
   8.176    |> set_body false
   8.177 @@ -358,10 +400,10 @@
   8.178  fun export_inst inner outer =
   8.179    let
   8.180      val declared_outer = is_declared outer;
   8.181 -    val fixes_inner = fixes_of inner;
   8.182 -    val fixes_outer = fixes_of outer;
   8.183  
   8.184 -    val gen_fixes = map #2 (take (length fixes_inner - length fixes_outer) fixes_inner);
   8.185 +    val gen_fixes =
   8.186 +      Symtab.fold (fn (y, _) => not (is_fixed outer y) ? cons y)
   8.187 +        (#2 (fixes_of inner)) [];
   8.188      val still_fixed = not o member (op =) gen_fixes;
   8.189  
   8.190      val type_occs_inner = type_occs_of inner;
     9.1 --- a/src/Tools/coherent.ML	Wed Apr 27 17:44:06 2011 +0200
     9.2 +++ b/src/Tools/coherent.ML	Wed Apr 27 17:58:45 2011 +0200
     9.3 @@ -213,7 +213,7 @@
     9.4    SUBPROOF (fn {prems = prems', concl, context, ...} =>
     9.5      let val xs = map (term_of o #2) params @
     9.6        map (fn (_, s) => Free (s, the (Variable.default_type context s)))
     9.7 -        (Variable.fixes_of context)
     9.8 +        (rev (Variable.dest_fixes context))  (* FIXME !? *)
     9.9      in
    9.10        case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl)
    9.11             (mk_dom xs) Net.empty 0 0 of
    10.1 --- a/src/Tools/induct.ML	Wed Apr 27 17:44:06 2011 +0200
    10.2 +++ b/src/Tools/induct.ML	Wed Apr 27 17:58:45 2011 +0200
    10.3 @@ -599,7 +599,7 @@
    10.4  
    10.5  fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] =
    10.6        let
    10.7 -        val x = Name.clean (Proof_Context.revert_skolem ctxt z);
    10.8 +        val x = Name.clean (Variable.revert_fixed ctxt z);
    10.9          fun index i [] = []
   10.10            | index i (y :: ys) =
   10.11                if x = y then x ^ string_of_int i :: index (i + 1) ys
   10.12 @@ -646,7 +646,7 @@
   10.13      val v = Free (x, T);
   10.14      fun spec_rule prfx (xs, body) =
   10.15        @{thm Pure.meta_spec}
   10.16 -      |> Thm.rename_params_rule ([Name.clean (Proof_Context.revert_skolem ctxt x)], 1)
   10.17 +      |> Thm.rename_params_rule ([Name.clean (Variable.revert_fixed ctxt x)], 1)
   10.18        |> Thm.lift_rule (cert prfx)
   10.19        |> `(Thm.prop_of #> Logic.strip_assums_concl)
   10.20        |-> (fn pred $ arg =>