reorganize declarations (more efficient);
authorwenzelm
Wed Jul 19 12:12:05 2006 +0200 (2006-07-19)
changeset 20162d4bcb27686f9
parent 20161 b8b1d4a380aa
child 20163 08f2833ca433
reorganize declarations (more efficient);
renamed rename_wrt to variant_frees (avoid confusion with Term.rename_wrt_term, which reverses the result);
tuned;
src/Pure/variable.ML
     1.1 --- a/src/Pure/variable.ML	Wed Jul 19 12:12:04 2006 +0200
     1.2 +++ b/src/Pure/variable.ML	Wed Jul 19 12:12:05 2006 +0200
     1.3 @@ -10,23 +10,22 @@
     1.4    val is_body: Context.proof -> bool
     1.5    val set_body: bool -> Context.proof -> Context.proof
     1.6    val restore_body: Context.proof -> Context.proof -> Context.proof
     1.7 +  val names_of: Context.proof -> Name.context
     1.8    val fixes_of: Context.proof -> (string * string) list
     1.9    val binds_of: Context.proof -> (typ * term) Vartab.table
    1.10 -  val defaults_of: Context.proof ->
    1.11 -    typ Vartab.table * sort Vartab.table * string list * string list Symtab.table
    1.12 -  val used_types: Context.proof -> string list
    1.13 +  val constraints_of: Context.proof -> typ Vartab.table * sort Vartab.table
    1.14    val is_declared: Context.proof -> string -> bool
    1.15    val is_fixed: Context.proof -> string -> bool
    1.16    val newly_fixed: Context.proof -> Context.proof -> string -> bool
    1.17 -  val def_sort: Context.proof -> indexname -> sort option
    1.18 +  val default_type: Context.proof -> string -> typ option
    1.19    val def_type: Context.proof -> bool -> indexname -> typ option
    1.20 -  val default_type: Context.proof -> string -> typ option
    1.21 -  val declare_type: typ -> Context.proof -> Context.proof
    1.22 -  val declare_syntax: term -> Context.proof -> Context.proof
    1.23 +  val def_sort: Context.proof -> indexname -> sort option
    1.24 +  val declare_constraints: term -> Context.proof -> Context.proof
    1.25 +  val declare_internal: term -> Context.proof -> Context.proof
    1.26    val declare_term: term -> Context.proof -> Context.proof
    1.27    val declare_thm: thm -> Context.proof -> Context.proof
    1.28    val thm_context: thm -> Context.proof
    1.29 -  val rename_wrt: Context.proof -> term list -> (string * 'a) list -> (string * 'a) list
    1.30 +  val variant_frees: Context.proof -> term list -> (string * 'a) list -> (string * 'a) list
    1.31    val add_fixes: string list -> Context.proof -> string list * Context.proof
    1.32    val invent_fixes: string list -> Context.proof -> string list * Context.proof
    1.33    val invent_types: sort list -> Context.proof -> (string * sort) list * Context.proof
    1.34 @@ -56,67 +55,66 @@
    1.35  structure Variable: VARIABLE =
    1.36  struct
    1.37  
    1.38 -
    1.39  (** local context data **)
    1.40  
    1.41  datatype data = Data of
    1.42   {is_body: bool,                        (*inner body mode*)
    1.43 -  names: Name.context,        		(*used type/term variable names*)
    1.44 -  fixes: (string * string) list, 	(*term fixes -- extern/intern*)
    1.45 +  names: Name.context,                  (*type/term variable names*)
    1.46 +  fixes: (string * string) list,        (*term fixes -- extern/intern*)
    1.47    binds: (typ * term) Vartab.table,     (*term bindings*)
    1.48 -  defaults:
    1.49 +  type_occs: string list Symtab.table,  (*type variables -- possibly within term variables*)
    1.50 +  constraints:
    1.51      typ Vartab.table *                  (*type constraints*)
    1.52 -    sort Vartab.table *                 (*default sorts*)
    1.53 -    string list *                       (*used type variables*)
    1.54 -    string list Symtab.table};          (*occurrences of type variables in term variables*)
    1.55 +    sort Vartab.table};                 (*default sorts*)
    1.56  
    1.57 -fun make_data (is_body, names, fixes, binds, defaults) =
    1.58 -  Data {is_body = is_body, names = names, fixes = fixes, binds = binds, defaults = defaults};
    1.59 +fun make_data (is_body, names, fixes, binds, type_occs, constraints) =
    1.60 +  Data {is_body = is_body, names = names, fixes = fixes, binds = binds,
    1.61 +    type_occs = type_occs, constraints = constraints};
    1.62  
    1.63  structure Data = ProofDataFun
    1.64  (
    1.65    val name = "Pure/variable";
    1.66    type T = data;
    1.67    fun init thy =
    1.68 -    make_data (false, Name.context, [], Vartab.empty,
    1.69 -      (Vartab.empty, Vartab.empty, [], Symtab.empty));
    1.70 +    make_data (false, Name.context, [], Vartab.empty, Symtab.empty, (Vartab.empty, Vartab.empty));
    1.71    fun print _ _ = ();
    1.72  );
    1.73  
    1.74  val _ = Context.add_setup Data.init;
    1.75  
    1.76  fun map_data f =
    1.77 -  Data.map (fn Data {is_body, names, fixes, binds, defaults} =>
    1.78 -    make_data (f (is_body, names, fixes, binds, defaults)));
    1.79 +  Data.map (fn Data {is_body, names, fixes, binds, type_occs, constraints} =>
    1.80 +    make_data (f (is_body, names, fixes, binds, type_occs, constraints)));
    1.81  
    1.82 -fun map_names f = map_data (fn (is_body, names, fixes, binds, defaults) =>
    1.83 -  (is_body, f names, fixes, binds, defaults));
    1.84 +fun map_names f = map_data (fn (is_body, names, fixes, binds, type_occs, constraints) =>
    1.85 +  (is_body, f names, fixes, binds, type_occs, constraints));
    1.86 +
    1.87 +fun map_fixes f = map_data (fn (is_body, names, fixes, binds, type_occs, constraints) =>
    1.88 +  (is_body, names, f fixes, binds, type_occs, constraints));
    1.89  
    1.90 -fun map_fixes f = map_data (fn (is_body, names, fixes, binds, defaults) =>
    1.91 -  (is_body, names, f fixes, binds, defaults));
    1.92 +fun map_binds f = map_data (fn (is_body, names, fixes, binds, type_occs, constraints) =>
    1.93 +  (is_body, names, fixes, f binds, type_occs, constraints));
    1.94  
    1.95 -fun map_binds f = map_data (fn (is_body, names, fixes, binds, defaults) =>
    1.96 -  (is_body, names, fixes, f binds, defaults));
    1.97 +fun map_type_occs f = map_data (fn (is_body, names, fixes, binds, type_occs, constraints) =>
    1.98 +  (is_body, names, fixes, binds, f type_occs, constraints));
    1.99  
   1.100 -fun map_defaults f = map_data (fn (is_body, names, fixes, binds, defaults) =>
   1.101 -  (is_body, names, fixes, binds, f defaults));
   1.102 +fun map_constraints f = map_data (fn (is_body, names, fixes, binds, type_occs, constraints) =>
   1.103 +  (is_body, names, fixes, binds, type_occs, f constraints));
   1.104  
   1.105  fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
   1.106  
   1.107  val is_body = #is_body o rep_data;
   1.108 -fun set_body b = map_data (fn (_, names, fixes, binds, defaults) =>
   1.109 -  (b, names, fixes, binds, defaults));
   1.110 +fun set_body b = map_data (fn (_, names, fixes, binds, type_occs, constraints) =>
   1.111 +  (b, names, fixes, binds, type_occs, constraints));
   1.112  fun restore_body ctxt = set_body (is_body ctxt);
   1.113  
   1.114  val names_of = #names o rep_data;
   1.115  val fixes_of = #fixes o rep_data;
   1.116  val binds_of = #binds o rep_data;
   1.117 +val type_occs_of = #type_occs o rep_data;
   1.118 +val constraints_of = #constraints o rep_data;
   1.119  
   1.120 -val defaults_of = #defaults o rep_data;
   1.121 -val used_types = #3 o defaults_of;
   1.122 -val type_occs_of = #4 o defaults_of;
   1.123 -
   1.124 -fun is_declared ctxt x = Vartab.defined (#1 (defaults_of ctxt)) (x, ~1);
   1.125 +val is_declared = Name.is_declared o names_of;
   1.126  fun is_fixed ctxt x = exists (fn (_, y) => x = y) (fixes_of ctxt);
   1.127  fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
   1.128  
   1.129 @@ -126,10 +124,10 @@
   1.130  
   1.131  (* default sorts and types *)
   1.132  
   1.133 -val def_sort = Vartab.lookup o #2 o defaults_of;
   1.134 +fun default_type ctxt x = Vartab.lookup (#1 (constraints_of ctxt)) (x, ~1);
   1.135  
   1.136  fun def_type ctxt pattern xi =
   1.137 -  let val {binds, defaults = (types, _, _, _), ...} = rep_data ctxt in
   1.138 +  let val {binds, constraints = (types, _), ...} = rep_data ctxt in
   1.139      (case Vartab.lookup types xi of
   1.140        NONE =>
   1.141          if pattern then NONE
   1.142 @@ -137,82 +135,70 @@
   1.143      | some => some)
   1.144    end;
   1.145  
   1.146 -fun default_type ctxt x = Vartab.lookup (#1 (defaults_of ctxt)) (x, ~1);
   1.147 +val def_sort = Vartab.lookup o #2 o constraints_of;
   1.148 +
   1.149 +
   1.150 +(* names *)
   1.151 +
   1.152 +val declare_type_names = map_names o
   1.153 +  fold_types (fold_atyps (fn TFree (a, _) => Name.declare a | _ => I));
   1.154 +
   1.155 +fun declare_names t =
   1.156 +  declare_type_names t #>
   1.157 +  map_names (fold_aterms (fn Free (x, _) => Name.declare x | _ => I) t);
   1.158 +
   1.159 +
   1.160 +(* type occurrences *)
   1.161 +
   1.162 +val declare_type_occs = map_type_occs o fold_term_types
   1.163 +  (fn Free (x, _) => fold_atyps (fn TFree (a, _) => Symtab.insert_list (op =) (a, x) | _ => I)
   1.164 +    | _ => fold_atyps (fn TFree (a, _) => Symtab.default (a, []) | _ => I));
   1.165  
   1.166  
   1.167 -(* declare types/terms *)
   1.168 -
   1.169 -local
   1.170 -
   1.171 -val ins_types = fold_aterms
   1.172 -  (fn Free (x, T) => Vartab.update ((x, ~1), T)
   1.173 -    | Var v => Vartab.update v
   1.174 -    | _ => I);
   1.175 -
   1.176 -val ins_sorts = fold_atyps
   1.177 -  (fn TFree (x, S) => Vartab.default ((x, ~1), S)
   1.178 -    | TVar v => Vartab.default v
   1.179 -    | _ => I);
   1.180 +(* constraints *)
   1.181  
   1.182 -val ins_used = fold_atyps
   1.183 -  (fn TFree (x, _) => insert (op =) x | _ => I);
   1.184 -
   1.185 -val ins_occs = fold_term_types (fn t =>
   1.186 -  let val x = case t of Free (x, _) => x | _ => ""
   1.187 -  in fold_atyps (fn TFree (a, _) => Symtab.insert_list (op =) (a, x) | _ => I) end);
   1.188 -
   1.189 -fun ins_skolem def_ty = fold_rev (fn (x, x') =>
   1.190 -  (case def_ty x' of
   1.191 -    SOME T => Vartab.update ((x, ~1), T)
   1.192 -  | NONE => I));
   1.193 -
   1.194 -val ins_namesT = fold_atyps
   1.195 -  (fn TFree (x, _) => Name.declare x | _ => I);
   1.196 -
   1.197 -fun ins_names t =
   1.198 -  fold_types ins_namesT t #>
   1.199 -  fold_aterms (fn Free (x, _) => Name.declare x | _ => I) t;
   1.200 +fun redeclare_skolems ctxt = ctxt |> map_constraints (apfst (fn types =>
   1.201 +  let
   1.202 +    fun decl (x, x') =
   1.203 +      (case default_type ctxt x' of
   1.204 +        SOME T => Vartab.update ((x, ~1), T)
   1.205 +      | NONE => I);
   1.206 +  in fold_rev decl (fixes_of ctxt) types end));
   1.207  
   1.208 -in
   1.209 -
   1.210 -fun declare_type T = map_defaults (fn (types, sorts, used, occ) =>
   1.211 -  (types,
   1.212 -    ins_sorts T sorts,
   1.213 -    ins_used T used,
   1.214 -    occ)) #>
   1.215 -  map_names (ins_namesT T);
   1.216 -
   1.217 -fun declare_syntax t = map_defaults (fn (types, sorts, used, occ) =>
   1.218 -  (ins_types t types,
   1.219 -    fold_types ins_sorts t sorts,
   1.220 -    fold_types ins_used t used,
   1.221 -    occ)) #>
   1.222 -  map_names (ins_names t);
   1.223 +fun declare_constraints t = map_constraints (fn (types, sorts) =>
   1.224 +  let
   1.225 +    val types' = fold_aterms
   1.226 +      (fn Free (x, T) => Vartab.update ((x, ~1), T)
   1.227 +        | Var v => Vartab.update v
   1.228 +        | _ => I) t types;
   1.229 +    val sorts' = fold_types (fold_atyps
   1.230 +      (fn TFree (x, S) => Vartab.update ((x, ~1), S)
   1.231 +        | TVar v => Vartab.update v
   1.232 +        | _ => I)) t sorts;
   1.233 +  in (types', sorts') end)
   1.234 +  #> declare_type_names t
   1.235 +  #> redeclare_skolems;
   1.236  
   1.237 -fun declare_occs t = map_defaults (fn (types, sorts, used, occ) =>
   1.238 -  (types, sorts, used, ins_occs t occ));
   1.239 +
   1.240 +(* common declarations *)
   1.241 +
   1.242 +fun declare_internal t =
   1.243 +  declare_names t #>
   1.244 +  declare_type_occs t;
   1.245  
   1.246 -fun declare_term t ctxt =
   1.247 -  ctxt
   1.248 -  |> declare_syntax t
   1.249 -  |> map_defaults (fn (types, sorts, used, occ) =>
   1.250 -     (ins_skolem (fn x => Vartab.lookup types (x, ~1)) (fixes_of ctxt) types,
   1.251 -      sorts,
   1.252 -      used,
   1.253 -      ins_occs t occ))
   1.254 -  |> map_names (ins_names t);
   1.255 +fun declare_term t =
   1.256 +  declare_internal t #>
   1.257 +  declare_constraints t;
   1.258  
   1.259 -fun declare_thm th = fold declare_term (Thm.full_prop_of th :: Thm.hyps_of th);
   1.260 -fun thm_context th = Context.init_proof (Thm.theory_of_thm th) |> declare_thm th;
   1.261 -
   1.262 -end;
   1.263 +fun declare_thm th = fold declare_internal (Thm.full_prop_of th :: Thm.hyps_of th);
   1.264 +fun thm_context th = declare_thm th (Context.init_proof (Thm.theory_of_thm th));
   1.265  
   1.266  
   1.267  (* renaming term/type frees *)
   1.268  
   1.269 -fun rename_wrt ctxt ts frees =
   1.270 +fun variant_frees ctxt ts frees =
   1.271    let
   1.272 -    val names = names_of (ctxt |> fold declare_syntax ts);
   1.273 +    val names = names_of (fold declare_names ts ctxt);
   1.274      val xs = fst (Name.variants (map #1 frees) names);
   1.275    in xs ~~ map snd frees end;
   1.276  
   1.277 @@ -228,7 +214,7 @@
   1.278  fun new_fixes names' xs xs' =
   1.279    map_names (K names') #>
   1.280    map_fixes (fn fixes => (rev (xs ~~ xs') @ fixes)) #>
   1.281 -  fold (declare_syntax o Syntax.free) xs' #>
   1.282 +  fold (declare_constraints o Syntax.free) xs' #>
   1.283    pair xs';
   1.284  
   1.285  in
   1.286 @@ -259,7 +245,7 @@
   1.287  fun invent_types Ss ctxt =
   1.288    let
   1.289      val tfrees = Name.invents (names_of ctxt) "'a" (length Ss) ~~ Ss;
   1.290 -    val ctxt' = fold (declare_type o TFree) tfrees ctxt;
   1.291 +    val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
   1.292    in (tfrees, ctxt') end;
   1.293  
   1.294  
   1.295 @@ -268,32 +254,32 @@
   1.296  
   1.297  fun export_inst inner outer =
   1.298    let
   1.299 -    val types_outer = used_types outer;
   1.300 +    val declared_outer = is_declared outer;
   1.301      val fixes_inner = fixes_of inner;
   1.302      val fixes_outer = fixes_of outer;
   1.303  
   1.304      val gen_fixes = map #2 (Library.take (length fixes_inner - length fixes_outer, fixes_inner));
   1.305 -    val still_fixed = not o member (op =) ("" :: gen_fixes);
   1.306 +    val still_fixed = not o member (op =) gen_fixes;
   1.307      val gen_fixesT =
   1.308        Symtab.fold (fn (a, xs) =>
   1.309 -        if member (op =) types_outer a orelse exists still_fixed xs
   1.310 +        if declared_outer a orelse exists still_fixed xs
   1.311          then I else cons a) (type_occs_of inner) [];
   1.312    in (gen_fixesT, gen_fixes) end;
   1.313  
   1.314  fun exportT_inst inner outer = #1 (export_inst inner outer);
   1.315  
   1.316  fun exportT_terms inner outer ts =
   1.317 -  map (Term.generalize (exportT_inst (fold declare_occs ts inner) outer, [])
   1.318 +  map (Term.generalize (exportT_inst (fold declare_type_occs ts inner) outer, [])
   1.319      (fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1)) ts;
   1.320  
   1.321  fun export_terms inner outer ts =
   1.322 -  map (Term.generalize (export_inst (fold declare_occs ts inner) outer)
   1.323 +  map (Term.generalize (export_inst (fold declare_type_occs ts inner) outer)
   1.324      (fold Term.maxidx_term ts ~1 + 1)) ts;
   1.325  
   1.326  fun gen_export inst inner outer ths =
   1.327    let
   1.328      val ths' = map Thm.adjust_maxidx_thm ths;
   1.329 -    val inner' = fold (declare_occs o Thm.full_prop_of) ths' inner;
   1.330 +    val inner' = fold (declare_type_occs o Thm.full_prop_of) ths' inner;
   1.331    in map (Thm.generalize (inst inner' outer) (fold Thm.maxidx_thm ths' ~1 + 1)) ths' end;
   1.332  
   1.333  val exportT = gen_export (rpair [] oo exportT_inst);
   1.334 @@ -357,7 +343,7 @@
   1.335  val trade = gen_trade (import true) export;
   1.336  
   1.337  
   1.338 -(* focus on outer params *)
   1.339 +(* focus on outermost parameters *)
   1.340  
   1.341  fun forall_elim_prop t prop =
   1.342    Thm.beta_conversion false (Thm.capply (#2 (Thm.dest_comb prop)) t)
   1.343 @@ -367,7 +353,7 @@
   1.344    let
   1.345      val cert = Thm.cterm_of (Thm.theory_of_cterm goal);
   1.346      val t = Thm.term_of goal;
   1.347 -    val ps = rev (Term.rename_wrt_term t (Term.strip_all_vars t));   (*as they are printed :-*)
   1.348 +    val ps = Term.variant_frees t (Term.strip_all_vars t);   (*as they are printed :-*)
   1.349      val (xs, Ts) = split_list ps;
   1.350      val (xs', ctxt') = invent_fixes xs ctxt;
   1.351      val ps' = xs' ~~ Ts;
   1.352 @@ -382,13 +368,13 @@
   1.353  fun warn_extra_tfrees ctxt1 ctxt2 =
   1.354    let
   1.355      fun occs_typ a = Term.exists_subtype (fn TFree (b, _) => a = b | _ => false);
   1.356 -    fun occs_free _ "" = I
   1.357 -      | occs_free a x =
   1.358 -          (case def_type ctxt1 false (x, ~1) of
   1.359 -            SOME T => if occs_typ a T then I else cons (a, x)
   1.360 -          | NONE => cons (a, x));
   1.361 +    fun occs_free a x =
   1.362 +      (case def_type ctxt1 false (x, ~1) of
   1.363 +        SOME T => if occs_typ a T then I else cons (a, x)
   1.364 +      | NONE => cons (a, x));
   1.365  
   1.366 -    val occs1 = type_occs_of ctxt1 and occs2 = type_occs_of ctxt2;
   1.367 +    val occs1 = type_occs_of ctxt1;
   1.368 +    val occs2 = type_occs_of ctxt2;
   1.369      val extras = Symtab.fold (fn (a, xs) =>
   1.370        if Symtab.defined occs1 a then I else fold (occs_free a) xs) occs2 [];
   1.371      val tfrees = map #1 extras |> sort_distinct string_ord;
   1.372 @@ -402,20 +388,15 @@
   1.373  
   1.374  (* polymorphic terms *)
   1.375  
   1.376 -fun monomorphic ctxt ts =
   1.377 -  #1 (importT_terms ts (fold declare_term ts ctxt));
   1.378 -
   1.379  fun polymorphic ctxt ts =
   1.380    let
   1.381      val ctxt' = fold declare_term ts ctxt;
   1.382 -    val types = subtract (op =) (used_types ctxt) (used_types ctxt');
   1.383 +    val occs = type_occs_of ctxt;
   1.384 +    val occs' = type_occs_of ctxt';
   1.385 +    val types = Symtab.fold (fn (a, _) => if Symtab.defined occs a then I else cons a) occs' [];
   1.386      val idx = fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1;
   1.387    in map (Term.generalize (types, []) idx) ts end;
   1.388  
   1.389 -
   1.390 -
   1.391 -(** term bindings **)
   1.392 -
   1.393  fun hidden_polymorphism t T =
   1.394    let
   1.395      val tvarsT = Term.add_tvarsT T [];
   1.396 @@ -423,6 +404,10 @@
   1.397        (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
   1.398    in extra_tvars end;
   1.399  
   1.400 +
   1.401 +
   1.402 +(** term bindings **)
   1.403 +
   1.404  fun add_bind (xi, NONE) = map_binds (Vartab.delete_safe xi)
   1.405    | add_bind ((x, i), SOME t) =
   1.406        let