- Fixed bug in shrink
authorberghofe
Mon Nov 19 17:36:05 2001 +0100 (2001-11-19 ago)
changeset 122333348aa8061d1
parent 12232 ff75ed08b3fb
child 12234 9d86f1cd2969
- Fixed bug in shrink
- Restored old behaviour of thm_proof
- Eliminated reference from theory data
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/proofterm.ML	Mon Nov 19 17:34:02 2001 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Mon Nov 19 17:36:05 2001 +0100
     1.3 @@ -96,9 +96,9 @@
     1.4    val get_name_tags : term -> proof -> string * (string * string list) list
     1.5  
     1.6    (** rewriting on proof terms **)
     1.7 -  val add_prf_rrules : theory -> (proof * proof) list -> unit
     1.8 -  val add_prf_rprocs : theory ->
     1.9 -    (string * (Term.typ list -> proof -> proof option)) list -> unit
    1.10 +  val add_prf_rrules : (proof * proof) list -> theory -> theory
    1.11 +  val add_prf_rprocs : (string * (Term.typ list -> proof -> proof option)) list ->
    1.12 +    theory -> theory
    1.13    val rewrite_proof : Type.type_sig -> (proof * proof) list *
    1.14      (string * (typ list -> proof -> proof option)) list -> proof -> proof
    1.15    val rewrite_proof_notypes : (proof * proof) list *
    1.16 @@ -821,6 +821,8 @@
    1.17        in (is, ch orelse ch', ts', if ch orelse ch' then prf' % t' else prf) end
    1.18    | shrink' ls lev ts prfs (prf as PBound i) =
    1.19        (if exists (fn Some (Bound j) => lev-j <= nth_elem (i, ls) | _ => true) ts
    1.20 +         orelse not (null (duplicates
    1.21 +           (foldl (fn (js, Some (Bound j)) => j :: js | (js, _) => js) ([], ts))))
    1.22           orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
    1.23    | shrink' ls lev ts prfs (prf as Hyp _) = ([], false, map (pair false) ts, prf)
    1.24    | shrink' ls lev ts prfs (prf as MinProof _) =
    1.25 @@ -998,13 +1000,13 @@
    1.26  struct
    1.27    val name = "Pure/proof";
    1.28    type T = ((proof * proof) list *
    1.29 -    (string * (typ list -> proof -> proof option)) list) ref;
    1.30 +    (string * (typ list -> proof -> proof option)) list);
    1.31  
    1.32 -  val empty = (ref ([], [])): T;
    1.33 -  fun copy (ref rews) = (ref rews): T;            (*create new reference!*)
    1.34 +  val empty = ([], []);
    1.35 +  val copy = I;
    1.36    val finish = I;
    1.37 -  val prep_ext = copy;
    1.38 -  fun merge (ref (rules1, procs1), ref (rules2, procs2)) = ref
    1.39 +  val prep_ext = I;
    1.40 +  fun merge ((rules1, procs1), (rules2, procs2)) =
    1.41      (merge_lists rules1 rules2,
    1.42       generic_merge (uncurry equal o pairself fst) I I procs1 procs2);
    1.43    fun print _ _ = ();
    1.44 @@ -1014,13 +1016,13 @@
    1.45  
    1.46  val init = ProofData.init;
    1.47  
    1.48 -fun add_prf_rrules thy rs =
    1.49 +fun add_prf_rrules rs thy =
    1.50    let val r = ProofData.get thy
    1.51 -  in r := (rs @ fst (!r), snd (!r)) end;
    1.52 +  in ProofData.put (rs @ fst r, snd r) thy end;
    1.53  
    1.54 -fun add_prf_rprocs thy ps =
    1.55 +fun add_prf_rprocs ps thy =
    1.56    let val r = ProofData.get thy
    1.57 -  in r := (fst (!r), ps @ snd (!r)) end;
    1.58 +  in ProofData.put (fst r, ps @ snd r) thy end;
    1.59  
    1.60  fun thm_proof sign (name, tags) hyps prop prf =
    1.61    let
    1.62 @@ -1031,10 +1033,10 @@
    1.63          if ixn mem nvs then Some v else None) (vars_of prop) @
    1.64        map Some (sort (make_ord atless) (term_frees prop));
    1.65      val opt_prf = if ! proofs = 2 then
    1.66 -        #4 (shrink [] 0 (rewrite_prf fst (!(ProofData.get_sg sign))
    1.67 +        #4 (shrink [] 0 (rewrite_prf fst (ProofData.get_sg sign)
    1.68            (foldr (uncurry implies_intr_proof) (hyps', prf))))
    1.69        else MinProof (mk_min_proof ([], prf));
    1.70 -    val head = (case strip_combt (fst (strip_combP opt_prf)) of
    1.71 +    val head = (case strip_combt (fst (strip_combP prf)) of
    1.72          (PThm ((old_name, _), prf', prop', None), args') =>
    1.73            if (old_name="" orelse old_name=name) andalso
    1.74               prop = prop' andalso args = args' then