Reimplemented some operations on "code lemma" table to avoid that code
authorberghofe
Wed Nov 24 10:27:24 2004 +0100 (2004-11-24)
changeset 15321694f9d3ce90d
parent 15320 dfc2654eea9f
child 15322 c93e6fd5db59
Reimplemented some operations on "code lemma" table to avoid that code
lemmas get lost during merge.
src/HOL/Tools/recfun_codegen.ML
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Wed Nov 24 10:23:36 2004 +0100
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Wed Nov 24 10:27:24 2004 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4    val empty = Symtab.empty;
     1.5    val copy = I;
     1.6    val prep_ext = I;
     1.7 -  val merge = Symtab.merge_multi Drule.eq_thm_prop;
     1.8 +  val merge = Symtab.merge_multi' Drule.eq_thm_prop;
     1.9    fun print _ _ = ();
    1.10  end;
    1.11  
    1.12 @@ -31,6 +31,7 @@
    1.13  
    1.14  val prop_of = #prop o rep_thm;
    1.15  val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
    1.16 +val lhs_of = fst o dest_eqn o prop_of;
    1.17  val const_of = dest_Const o head_of o fst o dest_eqn;
    1.18  
    1.19  fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^
    1.20 @@ -38,32 +39,39 @@
    1.21  
    1.22  fun add (p as (thy, thm)) =
    1.23    let
    1.24 -    val tsig = Sign.tsig_of (sign_of thy);
    1.25      val tab = CodegenData.get thy;
    1.26      val (s, _) = const_of (prop_of thm);
    1.27 -
    1.28 -    val matches = curry
    1.29 -      (Pattern.matches tsig o pairself (fst o dest_eqn o prop_of));
    1.30 -
    1.31 -  in (CodegenData.put (Symtab.update ((s,
    1.32 -    filter_out (matches thm) (if_none (Symtab.lookup (tab, s)) []) @ [thm]),
    1.33 -      tab)) thy, thm)
    1.34 -  end handle TERM _ => (warn thm; p) | Pattern.Pattern => (warn thm; p);
    1.35 +  in
    1.36 +    if Pattern.pattern (lhs_of thm) then
    1.37 +      (CodegenData.put (Symtab.update ((s,
    1.38 +        thm :: if_none (Symtab.lookup (tab, s)) []), tab)) thy, thm)
    1.39 +    else (warn thm; p)
    1.40 +  end handle TERM _ => (warn thm; p);
    1.41  
    1.42  fun del (p as (thy, thm)) =
    1.43    let
    1.44      val tab = CodegenData.get thy;
    1.45      val (s, _) = const_of (prop_of thm);
    1.46 -  in (CodegenData.put (Symtab.update ((s,
    1.47 -    gen_rem eq_thm (if_none (Symtab.lookup (tab, s)) [], thm)),
    1.48 -      tab)) thy, thm)
    1.49 +  in case Symtab.lookup (tab, s) of
    1.50 +      None => p
    1.51 +    | Some thms => (CodegenData.put (Symtab.update ((s,
    1.52 +        gen_rem eq_thm (thms, thm)), tab)) thy, thm)
    1.53    end handle TERM _ => (warn thm; p);
    1.54  
    1.55 +fun del_redundant thy eqs [] = eqs
    1.56 +  | del_redundant thy eqs (eq :: eqs') =
    1.57 +    let
    1.58 +      val tsig = Sign.tsig_of (sign_of thy);
    1.59 +      val matches = curry
    1.60 +        (Pattern.matches tsig o pairself lhs_of)
    1.61 +    in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end;
    1.62 +
    1.63  fun get_equations thy (s, T) =
    1.64    (case Symtab.lookup (CodegenData.get thy, s) of
    1.65       None => []
    1.66 -   | Some thms => preprocess thy (filter (fn thm => is_instance thy T
    1.67 -       (snd (const_of (prop_of thm)))) thms));
    1.68 +   | Some thms => preprocess thy (del_redundant thy []
    1.69 +       (filter (fn thm => is_instance thy T
    1.70 +         (snd (const_of (prop_of thm)))) thms)));
    1.71  
    1.72  fun mk_poly_id thy (s, T) = mk_const_id (sign_of thy) s ^
    1.73    (case get_defn thy s T of