tuned signature;
authorwenzelm
Sat Apr 14 00:46:21 2007 +0200 (2007-04-14)
changeset 226713c62305fbee6
parent 22670 c803b2696ada
child 22672 777af26d5713
tuned signature;
export: precomputed closure, no reference to contexts;
src/Pure/Isar/local_defs.ML
src/Pure/variable.ML
     1.1 --- a/src/Pure/Isar/local_defs.ML	Sat Apr 14 00:46:20 2007 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Sat Apr 14 00:46:21 2007 +0200
     1.3 @@ -100,17 +100,22 @@
     1.4    end;
     1.5  
     1.6  
     1.7 -(* specific export -- result based on educated guessing *)
     1.8 +(* specific export -- result based on educated guessing (beware of closure sizes) *)
     1.9  
    1.10 -fun export inner outer th =
    1.11 +fun export inner outer =
    1.12    let
    1.13 -    val th' = Assumption.export false inner outer th;
    1.14 -    val still_fixed = map #1 (Drule.fold_terms Term.add_frees th' []);
    1.15 -    val defs = Assumption.prems_of inner |> filter_out (fn prem =>
    1.16 -      (case try (head_of_def o Thm.prop_of) prem of
    1.17 -        SOME x => member (op =) still_fixed x
    1.18 -      | NONE => true));
    1.19 -  in (map Drule.abs_def defs, th') end;
    1.20 +    val exp = Assumption.export false inner outer;
    1.21 +    val prems = Assumption.prems_of inner;
    1.22 +  in fn th =>
    1.23 +    let
    1.24 +      val th' = exp th;
    1.25 +      val still_fixed = map #1 (Drule.fold_terms Term.add_frees th' []);
    1.26 +      val defs = prems |> filter_out (fn prem =>
    1.27 +        (case try (head_of_def o Thm.prop_of) prem of
    1.28 +          SOME x => member (op =) still_fixed x
    1.29 +        | NONE => true));
    1.30 +    in (map Drule.abs_def defs, th') end
    1.31 +  end;
    1.32  
    1.33  
    1.34  (* basic transitivity reasoning -- modulo beta-eta *)
     2.1 --- a/src/Pure/variable.ML	Sat Apr 14 00:46:20 2007 +0200
     2.2 +++ b/src/Pure/variable.ML	Sat Apr 14 00:46:21 2007 +0200
     2.3 @@ -35,8 +35,6 @@
     2.4    val auto_fixes: term -> Proof.context -> Proof.context
     2.5    val variant_fixes: string list -> Proof.context -> string list * Proof.context
     2.6    val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
     2.7 -  val export_inst: Proof.context -> Proof.context -> string list * string list
     2.8 -  val exportT_inst: Proof.context -> Proof.context -> string list
     2.9    val export_terms: Proof.context -> Proof.context -> term list -> term list
    2.10    val exportT_terms: Proof.context -> Proof.context -> term list -> term list
    2.11    val exportT: Proof.context -> Proof.context -> thm list -> thm list
    2.12 @@ -161,10 +159,12 @@
    2.13  
    2.14  (* type occurrences *)
    2.15  
    2.16 -val declare_type_occs = map_type_occs o fold_term_types
    2.17 +val decl_type_occs = fold_term_types
    2.18    (fn Free (x, _) => fold_atyps (fn TFree (a, _) => Symtab.insert_list (op =) (a, x) | _ => I)
    2.19      | _ => fold_atyps (fn TFree (a, _) => Symtab.default (a, []) | _ => I));
    2.20  
    2.21 +val declare_type_occs = map_type_occs o decl_type_occs;
    2.22 +
    2.23  
    2.24  (* constraints *)
    2.25  
    2.26 @@ -302,7 +302,7 @@
    2.27  
    2.28  
    2.29  
    2.30 -(** export -- generalize type/term variables **)
    2.31 +(** export -- generalize type/term variables (beware of closure sizes) **)
    2.32  
    2.33  fun export_inst inner outer =
    2.34    let
    2.35 @@ -312,37 +312,48 @@
    2.36  
    2.37      val gen_fixes = map #2 (Library.take (length fixes_inner - length fixes_outer, fixes_inner));
    2.38      val still_fixed = not o member (op =) gen_fixes;
    2.39 -    val gen_fixesT =
    2.40 +
    2.41 +    val type_occs_inner = type_occs_of inner;
    2.42 +    fun gen_fixesT ts =
    2.43        Symtab.fold (fn (a, xs) =>
    2.44          if declared_outer a orelse exists still_fixed xs
    2.45 -        then I else cons a) (type_occs_of inner) [];
    2.46 +        then I else cons a) (fold decl_type_occs ts type_occs_inner) [];
    2.47    in (gen_fixesT, gen_fixes) end;
    2.48  
    2.49  fun exportT_inst inner outer = #1 (export_inst inner outer);
    2.50  
    2.51 -fun exportT_terms inner outer ts =
    2.52 -  map (TermSubst.generalize (exportT_inst (fold declare_type_occs ts inner) outer, [])
    2.53 -    (fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1)) ts;
    2.54 +fun exportT_terms inner outer =
    2.55 +  let val mk_tfrees = exportT_inst inner outer in
    2.56 +    fn ts => ts |> map
    2.57 +      (TermSubst.generalize (mk_tfrees ts, [])
    2.58 +        (fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1))
    2.59 +  end;
    2.60  
    2.61 -fun export_terms inner outer ts =
    2.62 -  map (TermSubst.generalize (export_inst (fold declare_type_occs ts inner) outer)
    2.63 -    (fold Term.maxidx_term ts ~1 + 1)) ts;
    2.64 +fun export_terms inner outer =
    2.65 +  let val (mk_tfrees, tfrees) = export_inst inner outer in
    2.66 +    fn ts => ts |> map
    2.67 +      (TermSubst.generalize (mk_tfrees ts, tfrees)
    2.68 +        (fold Term.maxidx_term ts ~1 + 1))
    2.69 +  end;
    2.70  
    2.71  fun export_prf inner outer prf =
    2.72    let
    2.73 -    val insts = export_inst (declare_prf prf inner) outer;
    2.74 +    val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer;
    2.75 +    val tfrees = mk_tfrees [];
    2.76      val idx = Proofterm.maxidx_proof prf ~1 + 1;
    2.77 -    val gen_term = TermSubst.generalize_option insts idx;
    2.78 -    val gen_typ = TermSubst.generalizeT_option (#1 insts) idx;
    2.79 +    val gen_term = TermSubst.generalize_option (tfrees, frees) idx;
    2.80 +    val gen_typ = TermSubst.generalizeT_option tfrees idx;
    2.81    in Proofterm.map_proof_terms_option gen_term gen_typ prf end;
    2.82  
    2.83 -fun gen_export inst inner outer ths =
    2.84 +
    2.85 +fun gen_export (mk_tfrees, frees) ths =
    2.86    let
    2.87 -    val inner' = fold (declare_type_occs o Thm.full_prop_of) ths inner;
    2.88 -  in map (Thm.generalize (inst inner' outer) (fold Thm.maxidx_thm ths ~1 + 1)) ths end;
    2.89 +    val tfrees = mk_tfrees (map Thm.full_prop_of ths);
    2.90 +    val maxidx = fold Thm.maxidx_thm ths ~1;
    2.91 +  in map (Thm.generalize (tfrees, frees) (maxidx + 1)) ths end;
    2.92  
    2.93 -val exportT = gen_export (rpair [] oo exportT_inst);
    2.94 -val export = gen_export export_inst;
    2.95 +fun exportT inner outer = gen_export (exportT_inst inner outer, []);
    2.96 +fun export inner outer = gen_export (export_inst inner outer);
    2.97  
    2.98  fun export_morphism inner outer =
    2.99    let