tuned merge operations via pointer_eq;
authorwenzelm
Mon Aug 20 20:43:58 2007 +0200 (2007-08-20)
changeset 24358d75af3e90e82
parent 24357 d42cf77da51f
child 24359 44556727197a
tuned merge operations via pointer_eq;
src/Provers/classical.ML
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Provers/classical.ML	Mon Aug 20 20:38:32 2007 +0200
     1.2 +++ b/src/Provers/classical.ML	Mon Aug 20 20:43:58 2007 +0200
     1.3 @@ -655,22 +655,24 @@
     1.4    Merging the term nets may look more efficient, but the rather delicate
     1.5    treatment of priority might get muddled up.*)
     1.6  fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...},
     1.7 -    CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2,
     1.8 +    cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2,
     1.9        swrappers, uwrappers, ...}) =
    1.10 -  let
    1.11 -    val safeIs' = fold rem_thm safeIs safeIs2;
    1.12 -    val safeEs' = fold rem_thm safeEs safeEs2;
    1.13 -    val hazIs' = fold rem_thm hazIs hazIs2;
    1.14 -    val hazEs' = fold rem_thm hazEs hazEs2;
    1.15 -    val cs1   = cs addSIs safeIs'
    1.16 -                   addSEs safeEs'
    1.17 -                   addIs  hazIs'
    1.18 -                   addEs  hazEs';
    1.19 -    val cs2 = map_swrappers
    1.20 -      (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1;
    1.21 -    val cs3 = map_uwrappers
    1.22 -      (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2;
    1.23 -  in cs3 end;
    1.24 +  if pointer_eq (cs, cs') then cs
    1.25 +  else
    1.26 +    let
    1.27 +      val safeIs' = fold rem_thm safeIs safeIs2;
    1.28 +      val safeEs' = fold rem_thm safeEs safeEs2;
    1.29 +      val hazIs' = fold rem_thm hazIs hazIs2;
    1.30 +      val hazEs' = fold rem_thm hazEs hazEs2;
    1.31 +      val cs1   = cs addSIs safeIs'
    1.32 +                     addSEs safeEs'
    1.33 +                     addIs  hazIs'
    1.34 +                     addEs  hazEs';
    1.35 +      val cs2 = map_swrappers
    1.36 +        (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1;
    1.37 +      val cs3 = map_uwrappers
    1.38 +        (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2;
    1.39 +    in cs3 end;
    1.40  
    1.41  
    1.42  (**** Simple tactics for theorem proving ****)
    1.43 @@ -851,12 +853,14 @@
    1.44  val empty_context_cs = make_context_cs ([], []);
    1.45  
    1.46  fun merge_context_cs (ctxt_cs1, ctxt_cs2) =
    1.47 -  let
    1.48 -    val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
    1.49 -    val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
    1.50 -    val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2);
    1.51 -    val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2);
    1.52 -  in make_context_cs (swrappers', uwrappers') end;
    1.53 +  if pointer_eq (ctxt_cs1, ctxt_cs2) then ctxt_cs1
    1.54 +  else
    1.55 +    let
    1.56 +      val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
    1.57 +      val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
    1.58 +      val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2);
    1.59 +      val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2);
    1.60 +    in make_context_cs (swrappers', uwrappers') end;
    1.61  
    1.62  
    1.63  
     2.1 --- a/src/Pure/meta_simplifier.ML	Mon Aug 20 20:38:32 2007 +0200
     2.2 +++ b/src/Pure/meta_simplifier.ML	Mon Aug 20 20:43:58 2007 +0200
     2.3 @@ -791,28 +791,30 @@
     2.4  (* merge *)  (*NOTE: ignores some fields of 2nd simpset*)
     2.5  
     2.6  fun merge_ss (ss1, ss2) =
     2.7 -  let
     2.8 -    val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1, context = _},
     2.9 -     {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac,
    2.10 -      loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
    2.11 -    val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _},
    2.12 -     {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
    2.13 -      loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
    2.14 -
    2.15 -    val rules' = Net.merge eq_rrule (rules1, rules2);
    2.16 -    val prems' = merge Thm.eq_thm_prop (prems1, prems2);
    2.17 -    val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
    2.18 -    val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
    2.19 -    val congs' = merge (eq_cong o pairself #2) (congs1, congs2);
    2.20 -    val weak' = merge (op =) (weak1, weak2);
    2.21 -    val procs' = Net.merge eq_proc (procs1, procs2);
    2.22 -    val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
    2.23 -    val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
    2.24 -    val solvers' = merge eq_solver (solvers1, solvers2);
    2.25 -  in
    2.26 -    make_simpset ((rules', prems', bounds', depth', NONE), ((congs', weak'), procs',
    2.27 -      mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
    2.28 -  end;
    2.29 +  if pointer_eq (ss1, ss2) then ss1
    2.30 +  else
    2.31 +    let
    2.32 +      val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1, context = _},
    2.33 +       {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac,
    2.34 +        loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
    2.35 +      val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _},
    2.36 +       {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
    2.37 +        loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
    2.38 +  
    2.39 +      val rules' = Net.merge eq_rrule (rules1, rules2);
    2.40 +      val prems' = merge Thm.eq_thm_prop (prems1, prems2);
    2.41 +      val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
    2.42 +      val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
    2.43 +      val congs' = merge (eq_cong o pairself #2) (congs1, congs2);
    2.44 +      val weak' = merge (op =) (weak1, weak2);
    2.45 +      val procs' = Net.merge eq_proc (procs1, procs2);
    2.46 +      val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
    2.47 +      val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
    2.48 +      val solvers' = merge eq_solver (solvers1, solvers2);
    2.49 +    in
    2.50 +      make_simpset ((rules', prems', bounds', depth', NONE), ((congs', weak'), procs',
    2.51 +        mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
    2.52 +    end;
    2.53  
    2.54  
    2.55