improved Net interface;
authorwenzelm
Wed Jul 13 16:07:21 2005 +0200 (2005-07-13)
changeset 1680090eff1b52428
parent 16799 978dcf30c3dd
child 16801 4bb13fa6ae72
improved Net interface;
src/FOLP/simp.ML
src/HOL/Tools/res_axioms.ML
src/Pure/Isar/net_rules.ML
src/Pure/Proof/extraction.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/FOLP/simp.ML	Wed Jul 13 16:07:18 2005 +0200
     1.2 +++ b/src/FOLP/simp.ML	Wed Jul 13 16:07:21 2005 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4  
     1.5  (*insert a thm in a discrimination net by its lhs*)
     1.6  fun lhs_insert_thm (th,net) =
     1.7 -    Net.insert_term((lhs_of (concl_of th), (false,th)), net, eq_brl)
     1.8 +    Net.insert_term eq_brl (lhs_of (concl_of th), (false,th)) net
     1.9      handle  Net.INSERT => net;
    1.10  
    1.11  (*match subgoal i against possible theorems in the net.
    1.12 @@ -247,7 +247,7 @@
    1.13  
    1.14  (*insert a thm in a thm net*)
    1.15  fun insert_thm_warn (th,net) = 
    1.16 -  Net.insert_term((concl_of th, th), net, Drule.eq_thm_prop)
    1.17 +  Net.insert_term Drule.eq_thm_prop (concl_of th, th) net
    1.18    handle Net.INSERT => 
    1.19      (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
    1.20       net);
    1.21 @@ -273,7 +273,7 @@
    1.22  
    1.23  (*delete a thm from a thm net*)
    1.24  fun delete_thm_warn (th,net) = 
    1.25 -  Net.delete_term((concl_of th, th), net, Drule.eq_thm_prop)
    1.26 +  Net.delete_term Drule.eq_thm_prop (concl_of th, th) net
    1.27    handle Net.DELETE => 
    1.28      (writeln"\nNo such rewrite or congruence rule:";  print_thm th;
    1.29       net);
     2.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Jul 13 16:07:18 2005 +0200
     2.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Jul 13 16:07:21 2005 +0200
     2.3 @@ -250,7 +250,7 @@
     2.4         |> ObjectLogic.atomize_thm |> make_nnf;
     2.5  
     2.6  (*The cache prevents repeated clausification of a theorem, 
     2.7 -  and also repeated declaration of Skolem functions*)  
     2.8 +  and also repeated declaration of Skolem functions*)  (* FIXME better use Termtab!? *)
     2.9  val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table)
    2.10  
    2.11  (*Declare Skolem functions for a theorem, supplied in nnf and with its name*)
    2.12 @@ -366,10 +366,8 @@
    2.13      end;
    2.14  
    2.15  fun simpset_rules_of_thy thy =
    2.16 -    let val rules = #rules(fst (rep_ss (simpset_of thy)))
    2.17 -    in
    2.18 -	map (fn (_,r) => (#name r, #thm r)) (Net.dest rules)
    2.19 -    end;
    2.20 +    let val rules = #rules (fst (rep_ss (simpset_of thy)))
    2.21 +    in map (fn r => (#name r, #thm r)) (Net.entries rules) end;
    2.22  
    2.23  
    2.24  (**** Translate a set of classical/simplifier rules into CNF (still as type "thm")  ****)
     3.1 --- a/src/Pure/Isar/net_rules.ML	Wed Jul 13 16:07:18 2005 +0200
     3.2 +++ b/src/Pure/Isar/net_rules.ML	Wed Jul 13 16:07:21 2005 +0200
     3.3 @@ -47,7 +47,7 @@
     3.4  
     3.5  fun add rule (Rules {eq, index, rules, next, net}) =
     3.6    mk_rules eq index (rule :: rules) (next - 1)
     3.7 -    (Net.insert_term ((index rule, (next, rule)), net, K false));
     3.8 +    (Net.insert_term (K false) (index rule, (next, rule)) net);
     3.9  
    3.10  fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
    3.11    let val rules = Library.gen_merge_lists' eq rules1 rules2
    3.12 @@ -56,7 +56,7 @@
    3.13  fun delete rule (rs as Rules {eq, index, rules, next, net}) =
    3.14    if not (Library.gen_mem eq (rule, rules)) then rs
    3.15    else mk_rules eq index (Library.gen_rem eq (rules, rule)) next
    3.16 -    (Net.delete_term ((index rule, (0, rule)), net, eq o pairself #2));
    3.17 +    (Net.delete_term (eq o pairself #2) (index rule, (0, rule)) net);
    3.18  
    3.19  fun insert rule rs = add rule (delete rule rs);    (*ensure that new rule gets precedence*)
    3.20  
     4.1 --- a/src/Pure/Proof/extraction.ML	Wed Jul 13 16:07:18 2005 +0200
     4.2 +++ b/src/Pure/Proof/extraction.ML	Wed Jul 13 16:07:21 2005 +0200
     4.3 @@ -79,8 +79,8 @@
     4.4  val empty_rules : rules = {next = 0, rs = [], net = Net.empty};
     4.5  
     4.6  fun add_rule (r as (_, (lhs, _)), {next, rs, net} : rules) =
     4.7 -  {next = next - 1, rs = r :: rs, net = Net.insert_term
     4.8 -     ((Pattern.eta_contract lhs, (next, r)), net, K false)};
     4.9 +  {next = next - 1, rs = r :: rs, net = Net.insert_term (K false)
    4.10 +     (Pattern.eta_contract lhs, (next, r)) net};
    4.11  
    4.12  fun merge_rules
    4.13    ({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
    4.14 @@ -316,7 +316,7 @@
    4.15        ExtractionData.get thy;
    4.16      val procs = List.concat (map (fst o snd) types);
    4.17      val rtypes = map fst types;
    4.18 -    val eqns = Net.merge (#net realizes_eqns, #net typeof_eqns, K false);
    4.19 +    val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
    4.20      val thy' = add_syntax thy;
    4.21      val rd = ProofSyntax.read_proof thy' false
    4.22    in fn (thm, (vs, s1, s2)) =>
    4.23 @@ -351,7 +351,7 @@
    4.24      val {realizes_eqns, typeof_eqns, defs, types, ...} =
    4.25        ExtractionData.get thy';
    4.26      val procs = List.concat (map (fst o snd) types);
    4.27 -    val eqns = Net.merge (#net realizes_eqns, #net typeof_eqns, K false);
    4.28 +    val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
    4.29      val prop' = Pattern.rewrite_term (Sign.tsig_of thy')
    4.30        (map (Logic.dest_equals o prop_of) defs) [] prop;
    4.31    in freeze_thaw (condrew thy' eqns
    4.32 @@ -470,7 +470,7 @@
    4.33      val typroc = typeof_proc (Sign.defaultS thy');
    4.34      val prep = getOpt (prep, K I) thy' o ProofRewriteRules.elim_defs thy' false defs o
    4.35        Reconstruct.expand_proof thy' (("", NONE) :: map (apsnd SOME) expand);
    4.36 -    val rrews = Net.merge (#net realizes_eqns, #net typeof_eqns, K false);
    4.37 +    val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
    4.38  
    4.39      fun find_inst prop Ts ts vs =
    4.40        let
     5.1 --- a/src/ZF/Tools/typechk.ML	Wed Jul 13 16:07:18 2005 +0200
     5.2 +++ b/src/ZF/Tools/typechk.ML	Wed Jul 13 16:07:21 2005 +0200
     5.3 @@ -58,12 +58,12 @@
     5.4            cs)
     5.5    else
     5.6        TC{rules  = th::rules,
     5.7 -         net = Net.insert_term ((concl_of th, th), net, K false)};
     5.8 +         net = Net.insert_term (K false) (concl_of th, th) net};
     5.9  
    5.10  
    5.11  fun delTC (cs as TC{rules, net}, th) =
    5.12    if mem_thm (th, rules) then
    5.13 -      TC{net = Net.delete_term ((concl_of th, th), net, Drule.eq_thm_prop),
    5.14 +      TC{net = Net.delete_term Drule.eq_thm_prop (concl_of th, th) net,
    5.15           rules  = rem_thm (rules,th)}
    5.16    else (warning ("No such type-checking rule\n" ^ (string_of_thm th));
    5.17          cs);
    5.18 @@ -113,7 +113,7 @@
    5.19  
    5.20  fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) =
    5.21      TC {rules = gen_union Drule.eq_thm_prop (rules,rules'),
    5.22 -        net = Net.merge (net, net', Drule.eq_thm_prop)};
    5.23 +        net = Net.merge Drule.eq_thm_prop (net, net')};
    5.24  
    5.25  (*print tcsets*)
    5.26  fun print_tc (TC{rules,...}) =