canonical merge operations
authorhaftmann
Mon Apr 16 16:11:03 2007 +0200 (2007-04-16)
changeset 2271774dbc7696083
parent 22716 85f0ab03eeed
child 22718 936f7580937d
canonical merge operations
src/Pure/Proof/extraction.ML
src/Pure/meta_simplifier.ML
src/Pure/simplifier.ML
     1.1 --- a/src/Pure/Proof/extraction.ML	Mon Apr 16 12:16:11 2007 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Mon Apr 16 16:11:03 2007 +0200
     1.3 @@ -204,7 +204,7 @@
     1.4         realizers = realizers2, defs = defs2, expand = expand2, prep = prep2}) : T * T) =
     1.5      {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
     1.6       typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
     1.7 -     types = merge_alists types1 types2,
     1.8 +     types = AList.merge (op =) (K true) (types1, types2),
     1.9       realizers = Symtab.merge_list (gen_eq_set (op =) o pairself #1) (realizers1, realizers2),
    1.10       defs = Library.merge Thm.eq_thm (defs1, defs2),
    1.11       expand = Library.merge (op =) (expand1, expand2),
    1.12 @@ -343,7 +343,7 @@
    1.13      val thy' = add_syntax thy;
    1.14      val {realizes_eqns, typeof_eqns, defs, types, ...} =
    1.15        ExtractionData.get thy';
    1.16 -    val procs = maps (fst o snd) types;
    1.17 +    val procs = maps (rev o fst o snd) types;
    1.18      val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
    1.19      val prop' = Pattern.rewrite_term thy'
    1.20        (map (Logic.dest_equals o prop_of) defs) [] prop;
    1.21 @@ -390,14 +390,12 @@
    1.22  (** types with computational content **)
    1.23  
    1.24  fun add_types tys thy =
    1.25 -  let val {realizes_eqns, typeof_eqns, types, realizers,
    1.26 -    defs, expand, prep} = ExtractionData.get thy;
    1.27 -  in
    1.28 -    ExtractionData.put
    1.29 +  ExtractionData.map
    1.30 +    (fn {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =>
    1.31        {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns,
    1.32 -       types = map (apfst (Sign.intern_type thy)) tys @ types,
    1.33 -       realizers = realizers, defs = defs, expand = expand, prep = prep} thy
    1.34 -  end;
    1.35 +       types = fold (AList.update (op =) o apfst (Sign.intern_type thy)) tys types,
    1.36 +       realizers = realizers, defs = defs, expand = expand, prep = prep})
    1.37 +    thy;
    1.38  
    1.39  
    1.40  (** Pure setup **)
    1.41 @@ -460,7 +458,7 @@
    1.42      val thy' = add_syntax thy;
    1.43      val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =
    1.44        ExtractionData.get thy;
    1.45 -    val procs = maps (fst o snd) types;
    1.46 +    val procs = maps (rev o fst o snd) types;
    1.47      val rtypes = map fst types;
    1.48      val typroc = typeof_proc (Sign.defaultS thy');
    1.49      val prep = the_default (K I) prep thy' o ProofRewriteRules.elim_defs thy' false defs o
     2.1 --- a/src/Pure/meta_simplifier.ML	Mon Apr 16 12:16:11 2007 +0200
     2.2 +++ b/src/Pure/meta_simplifier.ML	Mon Apr 16 16:11:03 2007 +0200
     2.3 @@ -247,7 +247,6 @@
     2.4  fun solver_name (Solver {name, ...}) = name;
     2.5  fun solver ss (Solver {solver = tac, ...}) = tac ss;
     2.6  fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2);
     2.7 -val merge_solvers = gen_merge_lists eq_solver;
     2.8  
     2.9  
    2.10  (* diagnostics *)
    2.11 @@ -742,7 +741,7 @@
    2.12  
    2.13  fun ss addSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
    2.14    subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
    2.15 -    subgoal_tac, loop_tacs, (unsafe_solvers, merge_solvers solvers [solver])));
    2.16 +    subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers)));
    2.17  
    2.18  fun ss setSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
    2.19    subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless,
    2.20 @@ -750,7 +749,7 @@
    2.21  
    2.22  fun ss addSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
    2.23    subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
    2.24 -    subgoal_tac, loop_tacs, (merge_solvers unsafe_solvers [solver], solvers)));
    2.25 +    subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers)));
    2.26  
    2.27  fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless,
    2.28    subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless,
    2.29 @@ -795,8 +794,8 @@
    2.30      val weak' = merge (op =) (weak1, weak2);
    2.31      val procs' = Net.merge eq_proc (procs1, procs2);
    2.32      val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
    2.33 -    val unsafe_solvers' = merge_solvers unsafe_solvers1 unsafe_solvers2;
    2.34 -    val solvers' = merge_solvers solvers1 solvers2;
    2.35 +    val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
    2.36 +    val solvers' = merge eq_solver (solvers1, solvers2);
    2.37    in
    2.38      make_simpset ((rules', prems', bounds', NONE), ((congs', weak'), procs',
    2.39        mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
     3.1 --- a/src/Pure/simplifier.ML	Mon Apr 16 12:16:11 2007 +0200
     3.2 +++ b/src/Pure/simplifier.ML	Mon Apr 16 16:11:03 2007 +0200
     3.3 @@ -274,7 +274,7 @@
     3.4      val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.rep_ss ss;
     3.5      val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs));
     3.6      val solve_tac = FIRST' (map (MetaSimplifier.solver ss)
     3.7 -      (if safe then solvers else unsafe_solvers));
     3.8 +      (rev (if safe then solvers else unsafe_solvers)));
     3.9  
    3.10      fun simp_loop_tac i =
    3.11        Goal.asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
    3.12 @@ -286,7 +286,7 @@
    3.13  fun simp rew mode ss thm =
    3.14    let
    3.15      val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.rep_ss ss;
    3.16 -    val tacf = solve_all_tac unsafe_solvers;
    3.17 +    val tacf = solve_all_tac (rev unsafe_solvers);
    3.18      fun prover s th = Option.map #1 (Seq.pull (tacf s th));
    3.19    in rew mode prover ss thm end;
    3.20