rep_cterm/rep_thm: no longer dereference theory_ref;
authorwenzelm
Sat Apr 12 17:00:45 2008 +0200 (2008-04-12)
changeset 26631d6b6c74a8bcf
parent 26630 3074b3de4f4f
child 26632 90c0b075c0d3
rep_cterm/rep_thm: no longer dereference theory_ref;
removed obsolete compression;
src/Pure/proofterm.ML
src/Pure/sign.ML
src/Pure/theory.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/proofterm.ML	Sat Apr 12 17:00:43 2008 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Sat Apr 12 17:00:45 2008 +0200
     1.3 @@ -916,16 +916,13 @@
     1.4  
     1.5  fun shrink_proof thy =
     1.6    let
     1.7 -    val compress_typ = Compress.typ thy;
     1.8 -    val compress_term = Compress.term thy;
     1.9 -
    1.10      fun shrink ls lev (prf as Abst (a, T, body)) =
    1.11            let val (b, is, ch, body') = shrink ls (lev+1) body
    1.12 -          in (b, is, ch, if ch then Abst (a, Option.map compress_typ T, body') else prf) end
    1.13 +          in (b, is, ch, if ch then Abst (a, T, body') else prf) end
    1.14        | shrink ls lev (prf as AbsP (a, t, body)) =
    1.15            let val (b, is, ch, body') = shrink (lev::ls) lev body
    1.16            in (b orelse member (op =) is 0, map_filter (fn 0 => NONE | i => SOME (i-1)) is,
    1.17 -            ch, if ch then AbsP (a, Option.map compress_term t, body') else prf)
    1.18 +            ch, if ch then AbsP (a, t, body') else prf)
    1.19            end
    1.20        | shrink ls lev prf =
    1.21            let val (is, ch, _, prf') = shrink' ls lev [] [] prf
    1.22 @@ -940,13 +937,13 @@
    1.23        | shrink' ls lev ts prfs (prf as prf1 % t) =
    1.24            let val (is, ch, (ch', t')::ts', prf') = shrink' ls lev (t::ts) prfs prf1
    1.25            in (is, ch orelse ch', ts',
    1.26 -              if ch orelse ch' then prf' % Option.map compress_term t' else prf) end
    1.27 +              if ch orelse ch' then prf' % t' else prf) end
    1.28        | shrink' ls lev ts prfs (prf as PBound i) =
    1.29            (if exists (fn SOME (Bound j) => lev-j <= List.nth (ls, i) | _ => true) ts
    1.30               orelse has_duplicates (op =)
    1.31                 (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))
    1.32               orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
    1.33 -      | shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp (compress_term t))
    1.34 +      | shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp t)
    1.35        | shrink' ls lev ts prfs (prf as MinProof _) =
    1.36            ([], false, map (pair false) ts, prf)
    1.37        | shrink' ls lev ts prfs prf =
     2.1 --- a/src/Pure/sign.ML	Sat Apr 12 17:00:43 2008 +0200
     2.2 +++ b/src/Pure/sign.ML	Sat Apr 12 17:00:45 2008 +0200
     2.3 @@ -661,7 +661,7 @@
     2.4          val c' = if authentic then Syntax.constN ^ full_c else c;
     2.5          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
     2.6            cat_error msg ("in declaration of constant " ^ quote c);
     2.7 -        val T' = Compress.typ thy (Logic.varifyT T);
     2.8 +        val T' = Logic.varifyT T;
     2.9        in ((c, T'), (c', T', mx), Const (full_c, T)) end;
    2.10      val args = map prep raw_args;
    2.11    in
    2.12 @@ -686,7 +686,7 @@
    2.13  fun add_abbrev mode tags (c, raw_t) thy =
    2.14    let
    2.15      val pp = pp thy;
    2.16 -    val prep_tm = Compress.term thy o no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
    2.17 +    val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
    2.18      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
    2.19        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
    2.20      val (res, consts') = consts_of thy
     3.1 --- a/src/Pure/theory.ML	Sat Apr 12 17:00:43 2008 +0200
     3.2 +++ b/src/Pure/theory.ML	Sat Apr 12 17:00:45 2008 +0200
     3.3 @@ -211,7 +211,7 @@
     3.4  
     3.5  fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
     3.6    let
     3.7 -    val axms = map (apsnd (Compress.term thy o Logic.varify) o prep_axm thy) raw_axms;
     3.8 +    val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
     3.9      val axioms' = NameSpace.extend_table (Sign.naming_of thy) axms axioms
    3.10        handle Symtab.DUP dup => err_dup_axm dup;
    3.11    in axioms' end);
    3.12 @@ -235,7 +235,7 @@
    3.13      val consts = Sign.consts_of thy;
    3.14      fun prep const =
    3.15        let val Const (c, T) = Sign.no_vars pp (Const const)
    3.16 -      in (c, Consts.typargs consts (c, Compress.typ thy (Logic.varifyT T))) end;
    3.17 +      in (c, Consts.typargs consts (c, Logic.varifyT T)) end;
    3.18  
    3.19      val lhs_vars = Term.add_tfreesT (#2 lhs) [];
    3.20      val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>
     4.1 --- a/src/Pure/thm.ML	Sat Apr 12 17:00:43 2008 +0200
     4.2 +++ b/src/Pure/thm.ML	Sat Apr 12 17:00:45 2008 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4    (*certified types*)
     4.5    type ctyp
     4.6    val rep_ctyp: ctyp ->
     4.7 -   {thy: theory,
     4.8 +   {thy_ref: theory_ref,
     4.9      T: typ,
    4.10      maxidx: int,
    4.11      sorts: sort list}
    4.12 @@ -24,12 +24,12 @@
    4.13    type cterm
    4.14    exception CTERM of string * cterm list
    4.15    val rep_cterm: cterm ->
    4.16 -   {thy: theory,
    4.17 +   {thy_ref: theory_ref,
    4.18      t: term,
    4.19      T: typ,
    4.20      maxidx: int,
    4.21      sorts: sort list}
    4.22 -  val crep_cterm: cterm -> {thy: theory, t: term, T: ctyp, maxidx: int, sorts: sort list}
    4.23 +  val crep_cterm: cterm -> {thy_ref: theory_ref, t: term, T: ctyp, maxidx: int, sorts: sort list}
    4.24    val theory_of_cterm: cterm -> theory
    4.25    val term_of: cterm -> term
    4.26    val cterm_of: theory -> term -> cterm
    4.27 @@ -40,7 +40,7 @@
    4.28    type conv = cterm -> thm
    4.29    type attribute = Context.generic * thm -> Context.generic * thm
    4.30    val rep_thm: thm ->
    4.31 -   {thy: theory,
    4.32 +   {thy_ref: theory_ref,
    4.33      der: bool * Proofterm.proof,
    4.34      tags: Markup.property list,
    4.35      maxidx: int,
    4.36 @@ -49,7 +49,7 @@
    4.37      tpairs: (term * term) list,
    4.38      prop: term}
    4.39    val crep_thm: thm ->
    4.40 -   {thy: theory,
    4.41 +   {thy_ref: theory_ref,
    4.42      der: bool * Proofterm.proof,
    4.43      tags: Markup.property list,
    4.44      maxidx: int,
    4.45 @@ -140,7 +140,6 @@
    4.46    val put_name: string -> thm -> thm
    4.47    val get_tags: thm -> Markup.property list
    4.48    val map_tags: (Markup.property list -> Markup.property list) -> thm -> thm
    4.49 -  val compress: thm -> thm
    4.50    val norm_proof: thm -> thm
    4.51    val adjust_maxidx_thm: int -> thm -> thm
    4.52    val rename_boundvars: term -> term -> thm -> thm
    4.53 @@ -181,12 +180,8 @@
    4.54    sorts: sort list}
    4.55  with
    4.56  
    4.57 -fun rep_ctyp (Ctyp {thy_ref, T, maxidx, sorts}) =
    4.58 -  let val thy = Theory.deref thy_ref
    4.59 -  in {thy = thy, T = T, maxidx = maxidx, sorts = sorts} end;
    4.60 -
    4.61 +fun rep_ctyp (Ctyp args) = args;
    4.62  fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref;
    4.63 -
    4.64  fun typ_of (Ctyp {T, ...}) = T;
    4.65  
    4.66  fun ctyp_of thy raw_T =
    4.67 @@ -215,16 +210,11 @@
    4.68  
    4.69  exception CTERM of string * cterm list;
    4.70  
    4.71 -fun rep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) =
    4.72 -  let val thy =  Theory.deref thy_ref
    4.73 -  in {thy = thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
    4.74 +fun rep_cterm (Cterm args) = args;
    4.75  
    4.76  fun crep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) =
    4.77 -  let val thy = Theory.deref thy_ref in
    4.78 -   {thy = thy, t = t,
    4.79 -      T = Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts},
    4.80 -    maxidx = maxidx, sorts = sorts}
    4.81 -  end;
    4.82 +  {thy_ref = thy_ref, t = t, maxidx = maxidx, sorts = sorts,
    4.83 +    T = Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}};
    4.84  
    4.85  fun theory_of_cterm (Cterm {thy_ref, ...}) = Theory.deref thy_ref;
    4.86  fun term_of (Cterm {t, ...}) = t;
    4.87 @@ -376,19 +366,11 @@
    4.88  (*errors involving theorems*)
    4.89  exception THM of string * int * thm list;
    4.90  
    4.91 -fun rep_thm (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
    4.92 -  let val thy = Theory.deref thy_ref in
    4.93 -   {thy = thy, der = der, tags = tags, maxidx = maxidx,
    4.94 -    shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}
    4.95 -  end;
    4.96 +fun rep_thm (Thm args) = args;
    4.97  
    4.98 -(*version of rep_thm returning cterms instead of terms*)
    4.99  fun crep_thm (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
   4.100 -  let
   4.101 -    val thy = Theory.deref thy_ref;
   4.102 -    fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max, sorts = shyps};
   4.103 -  in
   4.104 -   {thy = thy, der = der, tags = tags, maxidx = maxidx, shyps = shyps,
   4.105 +  let fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max, sorts = shyps} in
   4.106 +   {thy_ref = thy_ref, der = der, tags = tags, maxidx = maxidx, shyps = shyps,
   4.107      hyps = map (cterm ~1) hyps,
   4.108      tpairs = map (pairself (cterm maxidx)) tpairs,
   4.109      prop = cterm maxidx prop}
   4.110 @@ -578,25 +560,6 @@
   4.111      shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop};
   4.112  
   4.113  
   4.114 -(*Compression of theorems -- a separate rule, not integrated with the others,
   4.115 -  as it could be slow.*)
   4.116 -fun compress (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
   4.117 -  let
   4.118 -    val thy = Theory.deref thy_ref;
   4.119 -    val hyps' = map (Compress.term thy) hyps;
   4.120 -    val tpairs' = map (pairself (Compress.term thy)) tpairs;
   4.121 -    val prop' = Compress.term thy prop;
   4.122 -  in
   4.123 -    Thm {thy_ref = Theory.check_thy thy,
   4.124 -      der = der,
   4.125 -      tags = tags,
   4.126 -      maxidx = maxidx,
   4.127 -      shyps = shyps,
   4.128 -      hyps = hyps',
   4.129 -      tpairs = tpairs',
   4.130 -      prop = prop'}
   4.131 -  end;
   4.132 -
   4.133  fun norm_proof (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
   4.134    let
   4.135      val thy = Theory.deref thy_ref;