maintain Name.context for fixes/defaults;
authorwenzelm
Tue Jul 11 12:17:09 2006 +0200 (2006-07-11)
changeset 20084aa320957f00c
parent 20083 717b1eb434f1
child 20085 c5d60752587f
maintain Name.context for fixes/defaults;
more efficient inventing/renaming of local names (cf. name.ML);
src/Pure/variable.ML
     1.1 --- a/src/Pure/variable.ML	Tue Jul 11 12:17:08 2006 +0200
     1.2 +++ b/src/Pure/variable.ML	Tue Jul 11 12:17:09 2006 +0200
     1.3 @@ -11,10 +11,9 @@
     1.4    val set_body: bool -> Context.proof -> Context.proof
     1.5    val restore_body: Context.proof -> Context.proof -> Context.proof
     1.6    val fixes_of: Context.proof -> (string * string) list
     1.7 -  val fixed_names_of: Context.proof -> string list
     1.8    val binds_of: Context.proof -> (typ * term) Vartab.table
     1.9    val defaults_of: Context.proof ->
    1.10 -    typ Vartab.table * sort Vartab.table * string list * string list Symtab.table
    1.11 +    typ Vartab.table * sort Vartab.table * string list * string list Symtab.table * Name.context
    1.12    val used_types: Context.proof -> string list
    1.13    val is_declared: Context.proof -> string -> bool
    1.14    val is_fixed: Context.proof -> string -> bool
    1.15 @@ -56,17 +55,19 @@
    1.16  structure Variable: VARIABLE =
    1.17  struct
    1.18  
    1.19 +
    1.20  (** local context data **)
    1.21  
    1.22  datatype data = Data of
    1.23 - {is_body: bool,                          (*inner body mode*)
    1.24 -  fixes: (string * string) list,          (*term fixes -- extern/intern*)
    1.25 -  binds: (typ * term) Vartab.table,       (*term bindings*)
    1.26 + {is_body: bool,                                (*inner body mode*)
    1.27 +  fixes: (string * string) list * Name.context, (*term fixes -- extern/intern*)
    1.28 +  binds: (typ * term) Vartab.table,             (*term bindings*)
    1.29    defaults:
    1.30 -    typ Vartab.table *                    (*type constraints*)
    1.31 -    sort Vartab.table *                   (*default sorts*)
    1.32 -    string list *                         (*used type variables*)
    1.33 -    string list Symtab.table};            (*occurrences of type variables in term variables*)
    1.34 +    typ Vartab.table *                          (*type constraints*)
    1.35 +    sort Vartab.table *                         (*default sorts*)
    1.36 +    string list *                               (*used type variables*)
    1.37 +    string list Symtab.table *                  (*occurrences of type variables in term variables*)
    1.38 +    Name.context};                              (*type/term variable names*)
    1.39  
    1.40  fun make_data (is_body, fixes, binds, defaults) =
    1.41    Data {is_body = is_body, fixes = fixes, binds = binds, defaults = defaults};
    1.42 @@ -76,7 +77,8 @@
    1.43    val name = "Pure/variable";
    1.44    type T = data;
    1.45    fun init thy =
    1.46 -    make_data (false, [], Vartab.empty, (Vartab.empty, Vartab.empty, [], Symtab.empty));
    1.47 +    make_data (false, ([], Name.context), Vartab.empty,
    1.48 +      (Vartab.empty, Vartab.empty, [], Symtab.empty, Name.make_context ["", "'"]));
    1.49    fun print _ _ = ();
    1.50  );
    1.51  
    1.52 @@ -98,11 +100,12 @@
    1.53  fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
    1.54  
    1.55  val is_body = #is_body o rep_data;
    1.56 -fun set_body b = map_data (fn (_, fixes, binds, defaults) => (b, fixes, binds, defaults));
    1.57 +fun set_body b = map_data (fn (_, fixes, binds, defaults) =>
    1.58 +  (b, fixes, binds, defaults));
    1.59  fun restore_body ctxt = set_body (is_body ctxt);
    1.60  
    1.61 -val fixes_of = #fixes o rep_data;
    1.62 -val fixed_names_of = map #2 o fixes_of;
    1.63 +val fixes_of = #1 o #fixes o rep_data;
    1.64 +val fixed_names_of = #2 o #fixes o rep_data;
    1.65  
    1.66  val binds_of = #binds o rep_data;
    1.67  
    1.68 @@ -122,7 +125,7 @@
    1.69  val def_sort = Vartab.lookup o #2 o defaults_of;
    1.70  
    1.71  fun def_type ctxt pattern xi =
    1.72 -  let val {binds, defaults = (types, _, _, _), ...} = rep_data ctxt in
    1.73 +  let val {binds, defaults = (types, _, _, _, _), ...} = rep_data ctxt in
    1.74      (case Vartab.lookup types xi of
    1.75        NONE =>
    1.76          if pattern then NONE
    1.77 @@ -159,31 +162,41 @@
    1.78      SOME T => Vartab.update ((x, ~1), T)
    1.79    | NONE => I));
    1.80  
    1.81 +val ins_namesT = fold_atyps
    1.82 +  (fn TFree (x, _) => Name.declare x | _ => I);
    1.83 +
    1.84 +fun ins_names t =
    1.85 +  fold_types ins_namesT t #>
    1.86 +  fold_aterms (fn Free (x, _) => Name.declare x | _ => I) t;
    1.87 +
    1.88  in
    1.89  
    1.90 -fun declare_type T = map_defaults (fn (types, sorts, used, occ) =>
    1.91 +fun declare_type T = map_defaults (fn (types, sorts, used, occ, names) =>
    1.92   (types,
    1.93    ins_sorts T sorts,
    1.94    ins_used T used,
    1.95 -  occ));
    1.96 +  occ,
    1.97 +  ins_namesT T names));
    1.98  
    1.99 -fun declare_syntax t = map_defaults (fn (types, sorts, used, occ) =>
   1.100 +fun declare_syntax t = map_defaults (fn (types, sorts, used, occ, names) =>
   1.101   (ins_types t types,
   1.102    fold_types ins_sorts t sorts,
   1.103    fold_types ins_used t used,
   1.104 -  occ));
   1.105 +  occ,
   1.106 +  ins_names t names));
   1.107  
   1.108 -fun declare_occs t = map_defaults (fn (types, sorts, used, occ) =>
   1.109 -  (types, sorts, used, ins_occs t occ));
   1.110 +fun declare_occs t = map_defaults (fn (types, sorts, used, occ, names) =>
   1.111 +  (types, sorts, used, ins_occs t occ, names));
   1.112  
   1.113  fun declare_term t ctxt =
   1.114    ctxt
   1.115    |> declare_syntax t
   1.116 -  |> map_defaults (fn (types, sorts, used, occ) =>
   1.117 +  |> map_defaults (fn (types, sorts, used, occ, names) =>
   1.118       (ins_skolem (fn x => Vartab.lookup types (x, ~1)) (fixes_of ctxt) types,
   1.119        sorts,
   1.120        used,
   1.121 -      ins_occs t occ));
   1.122 +      ins_occs t occ,
   1.123 +      ins_names t names));
   1.124  
   1.125  fun declare_thm th = fold declare_term (Thm.full_prop_of th :: Thm.hyps_of th);
   1.126  fun thm_context th = Context.init_proof (Thm.theory_of_thm th) |> declare_thm th;
   1.127 @@ -195,48 +208,52 @@
   1.128  
   1.129  fun rename_wrt ctxt ts frees =
   1.130    let
   1.131 -    val (types, sorts, _, _) = defaults_of (ctxt |> fold declare_syntax ts);
   1.132 -    fun ren (x, X) xs =
   1.133 -      let
   1.134 -        fun used y = y = "" orelse y = "'" orelse member (op =) xs y orelse
   1.135 -          Vartab.defined types (y, ~1) orelse Vartab.defined sorts (y, ~1);
   1.136 -        val x' = Term.variant_name used x;
   1.137 -      in ((x', X), x' :: xs) end;
   1.138 -  in #1 (fold_map ren frees []) end;
   1.139 +    val names = #5 (defaults_of (ctxt |> fold declare_syntax ts));
   1.140 +    val xs = fst (Name.variants (map #1 frees) names);
   1.141 +  in xs ~~ map snd frees end;
   1.142  
   1.143  
   1.144  
   1.145  (** fixes **)
   1.146  
   1.147 +local
   1.148 +
   1.149  fun no_dups [] = ()
   1.150    | no_dups dups = error ("Duplicate fixed variable(s): " ^ commas_quote dups);
   1.151  
   1.152 +fun new_fixes xs xs' names' =
   1.153 +  map_fixes (fn (fixes, _) => (rev (xs ~~ xs') @ fixes, names')) #>
   1.154 +  fold (declare_syntax o Syntax.free) xs' #>
   1.155 +  pair xs';
   1.156 +
   1.157 +in
   1.158 +
   1.159  fun add_fixes xs ctxt =
   1.160    let
   1.161 -    val (ys, zs) = split_list (fixes_of ctxt);
   1.162 -    val _ = no_dups (duplicates (op =) xs);
   1.163      val _ =
   1.164 -      (case filter (can Term.dest_skolem) xs of [] => ()
   1.165 +      (case filter (can Name.dest_skolem) xs of [] => ()
   1.166        | bads => error ("Illegal internal Skolem constant(s): " ^ commas_quote bads));
   1.167 -    val xs' =
   1.168 -      if is_body ctxt then Term.variantlist (map Term.skolem xs, zs)
   1.169 -      else (no_dups (xs inter_string ys); no_dups (xs inter_string zs); xs);
   1.170 -  in
   1.171 -    ctxt
   1.172 -    |> map_fixes (fn fixes => rev (xs ~~ xs') @ fixes)
   1.173 -    |> fold (declare_syntax o Syntax.free) xs'
   1.174 -    |> pair xs'
   1.175 -  end;
   1.176 +    val _ = no_dups (duplicates (op =) xs);
   1.177 +    val (ys, zs) = split_list (fixes_of ctxt);
   1.178 +    val names = fixed_names_of ctxt;
   1.179 +    val (xs', names') =
   1.180 +      if is_body ctxt then Name.variants (map Name.skolem xs) names
   1.181 +      else (no_dups (xs inter_string ys); no_dups (xs inter_string zs);
   1.182 +        (xs, fold Name.declare xs names));
   1.183 +  in ctxt |> new_fixes xs xs' names' end;
   1.184  
   1.185 -fun invent_fixes xs ctxt =
   1.186 -  ctxt
   1.187 -  |> set_body true
   1.188 -  |> add_fixes (Term.variantlist (xs, []))
   1.189 -  ||> restore_body ctxt;
   1.190 +fun invent_fixes raw_xs ctxt =
   1.191 +  let
   1.192 +    val names = fixed_names_of ctxt;
   1.193 +    val (xs, names') = Name.variants (map Name.clean raw_xs) names;
   1.194 +    val xs' = map Name.skolem xs;
   1.195 +  in ctxt |> new_fixes xs xs' names' end;
   1.196 +
   1.197 +end;
   1.198  
   1.199  fun invent_types Ss ctxt =
   1.200    let
   1.201 -    val tfrees = Term.invent_names (used_types ctxt) "'a" (length Ss) ~~ Ss;
   1.202 +    val tfrees = Name.invents (#5 (defaults_of ctxt)) "'a" (length Ss) ~~ Ss;
   1.203      val ctxt' = fold (declare_type o TFree) tfrees ctxt;
   1.204    in (tfrees, ctxt') end;
   1.205  
   1.206 @@ -291,7 +308,7 @@
   1.207    let
   1.208      val (instT, ctxt') = importT_inst ts ctxt;
   1.209      val vars = map (apsnd (Term.instantiateT instT)) (rev (fold Term.add_vars ts []));
   1.210 -    val ren = if is_open then I else Term.internal;
   1.211 +    val ren = if is_open then I else Name.internal;
   1.212      val (xs, ctxt'') = invent_fixes (map (ren o #1 o #1) vars) ctxt';
   1.213      val inst = vars ~~ map Free (xs ~~ map #2 vars);
   1.214    in ((instT, inst), ctxt'') end;