# HG changeset patch
# User wenzelm
# Date 869590004 -7200
# Node ID 7c013a61781315209e05659c6635022ff50e8f3c
# Parent  2c833cb21f8d490aad2ccfae39983263aa9ea06e
added print_ss;
improved merge;

diff -r 2c833cb21f8d -r 7c013a617813 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Tue Jul 22 18:45:43 1997 +0200
+++ b/src/Provers/simplifier.ML	Tue Jul 22 18:46:44 1997 +0200
@@ -4,32 +4,29 @@
     Copyright   1993  TU Munich
 
 Generic simplifier, suitable for most logics.
-
-TODO:
-  - stamps to identify funs / tacs
-  - merge: fail if incompatible funs
-  - improve merge
 *)
 
-infix 4 setsubgoaler setloop addloop setSSolver addSSolver setSolver addSolver 
-        setmksimps addsimps delsimps addeqcongs deleqcongs
-	settermless addsimprocs delsimprocs;
+infix 4
+  setsubgoaler setloop addloop setSSolver addSSolver setSolver
+  addSolver setmksimps addsimps delsimps addeqcongs deleqcongs
+  settermless addsimprocs delsimprocs;
 
 
 signature SIMPLIFIER =
 sig
   type simproc
   val mk_simproc: string -> cterm list -> (Sign.sg -> term -> thm option) -> simproc
-  val name_of_simproc: simproc -> string
   val conv_prover: (term * term -> term) -> thm -> (thm -> thm)
     -> tactic -> (int -> tactic) -> Sign.sg -> term -> term -> thm	(* FIXME move?, rename? *)
   type simpset
   val empty_ss: simpset
-  val rep_ss: simpset -> {simps: thm list, procs: string list, congs: thm list,
-			  subgoal_tac:        simpset -> int -> tactic,
-			  loop_tac:                      int -> tactic,
-			         finish_tac: thm list -> int -> tactic,
-			  unsafe_finish_tac: thm list -> int -> tactic}
+  val rep_ss: simpset ->
+   {mss: meta_simpset,
+    subgoal_tac:        simpset -> int -> tactic,
+    loop_tac:                      int -> tactic,
+           finish_tac: thm list -> int -> tactic,
+    unsafe_finish_tac: thm list -> int -> tactic};
+  val print_ss: simpset -> unit
   val setsubgoaler: simpset *  (simpset -> int -> tactic) -> simpset
   val setloop:      simpset *             (int -> tactic) -> simpset
   val addloop:      simpset *             (int -> tactic) -> simpset
@@ -73,23 +70,10 @@
 (* datatype simproc *)
 
 datatype simproc =
-  Simproc of {
-    name: string,
-    procs: (Sign.sg * term * (Sign.sg -> term -> thm option) * stamp) list}
-
-(* FIXME stamps!? *)
-fun eq_simproc (Simproc {name = name1, ...}, Simproc {name = name2, ...}) =
-  (name1 = name2);
+  Simproc of string * cterm list * (Sign.sg -> term -> thm option) * stamp;
 
-fun mk_simproc name lhss proc =
-  let
-    fun mk_proc lhs =
-      (#sign (Thm.rep_cterm lhs), Logic.varify (term_of lhs), proc, stamp ());
-  in
-    Simproc {name = name, procs = map mk_proc lhss}
-  end;
-
-fun name_of_simproc (Simproc {name, ...}) = name;
+fun mk_simproc name lhss proc = Simproc (name, lhss, proc, stamp ());
+fun rep_simproc (Simproc args) = args;
 
 
 (* generic conversion prover *)		(* FIXME move?, rename? *)
@@ -119,144 +103,125 @@
 datatype simpset =
   Simpset of {
     mss: meta_simpset,
-    simps: thm list,
-    procs: simproc list,
-    congs: thm list,
     subgoal_tac:        simpset -> int -> tactic,
     loop_tac:                      int -> tactic,
            finish_tac: thm list -> int -> tactic,
     unsafe_finish_tac: thm list -> int -> tactic};
 
-fun make_ss (mss, simps, procs, congs, 
-	     subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac) =
-  Simpset {mss = mss, simps = simps, procs = procs, congs = congs,
-    subgoal_tac = subgoal_tac, loop_tac = loop_tac,
+fun make_ss (mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac) =
+  Simpset {mss = mss, subgoal_tac = subgoal_tac, loop_tac = loop_tac,
     finish_tac = finish_tac, unsafe_finish_tac = unsafe_finish_tac};
 
 val empty_ss =
-  make_ss (Thm.empty_mss, [], [], [], 
-	   K (K no_tac), K no_tac, K (K no_tac), K (K no_tac));
+  make_ss (Thm.empty_mss, K (K no_tac), K no_tac, K (K no_tac), K (K no_tac));
+
+fun rep_ss (Simpset args) = args;
+fun prems_of_ss (Simpset {mss, ...}) = Thm.prems_of_mss mss;
+
+
+(* print simpsets *)
 
-fun rep_ss (Simpset {simps, procs, congs, subgoal_tac, loop_tac, 
-		     finish_tac, unsafe_finish_tac, ...}) =
-  {simps = simps, procs = map name_of_simproc procs, congs = congs,
-   subgoal_tac = subgoal_tac, loop_tac = loop_tac,
-   finish_tac = finish_tac, unsafe_finish_tac = unsafe_finish_tac};
+fun print_ss ss =
+  let
+    val Simpset {mss, ...} = ss;
+    val {simps, procs, congs} = Thm.dest_mss mss;
 
-fun prems_of_ss (Simpset {mss, ...}) = Thm.prems_of_mss mss;
+    val pretty_thms = map Display.pretty_thm;
+    fun pretty_proc (name, lhss) =
+      Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss);
+  in
+    Pretty.writeln (Pretty.big_list "simplification rules:" (pretty_thms simps));
+    Pretty.writeln (Pretty.big_list "simplification procedures:" (map pretty_proc procs));
+    Pretty.writeln (Pretty.big_list "congruences:" (pretty_thms congs))
+  end;
 
 
 (* extend simpsets *)
 
-fun (Simpset {mss, simps, procs, congs, subgoal_tac = _, loop_tac, 
-	      finish_tac, unsafe_finish_tac}) setsubgoaler subgoal_tac =
-  make_ss (mss, simps, procs, congs, subgoal_tac, loop_tac, 
-	   finish_tac, unsafe_finish_tac);
+fun (Simpset {mss, subgoal_tac = _, loop_tac, finish_tac, unsafe_finish_tac})
+    setsubgoaler subgoal_tac =
+  make_ss (mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac = _, 
-	      finish_tac, unsafe_finish_tac}) setloop loop_tac =
-  make_ss (mss, simps, procs, congs, subgoal_tac, DETERM o loop_tac, 
-	   finish_tac, unsafe_finish_tac);
+fun (Simpset {mss, subgoal_tac, loop_tac = _, finish_tac, unsafe_finish_tac})
+    setloop loop_tac =
+  make_ss (mss, subgoal_tac, DETERM o loop_tac, finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
-	      finish_tac, unsafe_finish_tac}) addloop tac =
-  make_ss (mss, simps, procs, congs, subgoal_tac, loop_tac ORELSE'(DETERM o tac),
-	   finish_tac, unsafe_finish_tac);
+fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+    addloop tac =
+  make_ss (mss, subgoal_tac, loop_tac ORELSE' (DETERM o tac), finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac,
-	      finish_tac = _, unsafe_finish_tac}) setSSolver finish_tac =
-  make_ss (mss, simps, procs, congs, subgoal_tac, loop_tac, 
-	   finish_tac, unsafe_finish_tac);
+fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac = _, unsafe_finish_tac})
+    setSSolver finish_tac =
+  make_ss (mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
-	      finish_tac, unsafe_finish_tac}) addSSolver tac =
-  make_ss (mss, simps, procs, congs, subgoal_tac, loop_tac,
-    fn hyps => finish_tac hyps ORELSE' tac hyps, unsafe_finish_tac);
+fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+    addSSolver tac =
+  make_ss (mss, subgoal_tac, loop_tac, fn hyps => finish_tac hyps ORELSE' tac hyps,
+    unsafe_finish_tac);
 
-fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac,
-	      finish_tac, unsafe_finish_tac = _}) setSolver unsafe_finish_tac =
-  make_ss (mss, simps, procs, congs, subgoal_tac, loop_tac, 
-	   finish_tac, unsafe_finish_tac);
+fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac = _})
+    setSolver unsafe_finish_tac =
+  make_ss (mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
-	      finish_tac, unsafe_finish_tac}) addSolver tac =
-  make_ss (mss, simps, procs, congs, subgoal_tac, loop_tac,
-    finish_tac, fn hyps => unsafe_finish_tac hyps ORELSE' tac hyps);
+fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+    addSolver tac =
+  make_ss (mss, subgoal_tac, loop_tac, finish_tac,
+    fn hyps => unsafe_finish_tac hyps ORELSE' tac hyps);
 
-fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
-	      finish_tac, unsafe_finish_tac}) setmksimps mk_simps =
+fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+    setmksimps mk_simps =
   make_ss (Thm.set_mk_rews (mss, map (Thm.strip_shyps o Drule.zero_var_indexes) o mk_simps),
-    simps, procs, congs, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
-
-fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
-	      finish_tac, unsafe_finish_tac}) settermless termless =
-  make_ss (Thm.set_termless (mss, termless), simps, procs, congs,
     subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
-	      finish_tac, unsafe_finish_tac}) addsimps rews =
+fun (Simpset {mss, subgoal_tac, loop_tac,  finish_tac, unsafe_finish_tac})
+    settermless termless =
+  make_ss (Thm.set_termless (mss, termless), subgoal_tac, loop_tac,
+    finish_tac, unsafe_finish_tac);
+
+fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+    addsimps rews =
   let val rews' = flat (map (Thm.mk_rews_of_mss mss) rews) in
-    make_ss (Thm.add_simps (mss, rews'), gen_union eq_thm (rews', simps),
-    procs, congs, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac)
+    make_ss (Thm.add_simps (mss, rews'), subgoal_tac, loop_tac,
+      finish_tac, unsafe_finish_tac)
   end;
 
-fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
-	      finish_tac, unsafe_finish_tac}) delsimps rews =
+fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+    delsimps rews =
   let val rews' = flat (map (Thm.mk_rews_of_mss mss) rews) in
-    make_ss (Thm.del_simps (mss, rews'), foldl (gen_rem eq_thm) (simps, rews'),
-    procs, congs, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac)
+    make_ss (Thm.del_simps (mss, rews'), subgoal_tac, loop_tac,
+      finish_tac, unsafe_finish_tac)
   end;
 
-fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
-	      finish_tac, unsafe_finish_tac}) addeqcongs newcongs =
-  make_ss (Thm.add_congs (mss, newcongs), simps, procs, 
-  gen_union eq_thm (congs, newcongs), subgoal_tac, loop_tac, 
-  finish_tac, unsafe_finish_tac);
+fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+    addeqcongs newcongs =
+  make_ss (Thm.add_congs (mss, newcongs), subgoal_tac, loop_tac,
+    finish_tac, unsafe_finish_tac);
 
-fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
-	      finish_tac, unsafe_finish_tac}) deleqcongs oldcongs =
-  make_ss (Thm.del_congs (mss, oldcongs), simps, procs, 
-  foldl (gen_rem eq_thm) (congs, oldcongs), subgoal_tac, loop_tac, 
-  finish_tac, unsafe_finish_tac);
+fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+    deleqcongs oldcongs =
+  make_ss (Thm.del_congs (mss, oldcongs), subgoal_tac, loop_tac,
+    finish_tac, unsafe_finish_tac);
 
-fun addsimproc ((Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
-			  finish_tac, unsafe_finish_tac}),
-			  simproc as Simproc {name = _, procs = procs'}) =
-  make_ss (Thm.add_simprocs (mss, procs'),
-    simps, gen_ins eq_simproc (simproc, procs),
-    congs, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
-
-val op addsimprocs = foldl addsimproc;
+fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+    addsimprocs simprocs =
+  make_ss
+    (Thm.add_simprocs (mss, map rep_simproc simprocs),
+      subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
 
-fun delsimproc ((Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
-			  finish_tac, unsafe_finish_tac}),
-			  simproc as Simproc {name = _, procs = procs'}) =
-  make_ss (Thm.del_simprocs (mss, procs'),
-    simps, gen_rem eq_simproc (procs, simproc),
-    congs, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
-
-val op delsimprocs = foldl delsimproc;
+fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
+    delsimprocs simprocs =
+  make_ss
+    (Thm.del_simprocs (mss, map rep_simproc simprocs),
+      subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
 
 
-(* merge simpsets *)
+(* merge simpsets *)	(*NOTE: ignores tactics of 2nd simpset*)
 
-(*prefers first simpset (FIXME improve?)*)
-fun merge_ss (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
-		       finish_tac, unsafe_finish_tac},
-    Simpset {simps = simps2, procs = procs2, congs = congs2, ...}) =
-  let
-    val simps' = gen_union eq_thm (simps, simps2);
-    val procs' = gen_union eq_simproc (procs, procs2);
-    val meta_procs' = flat (map (fn Simproc {procs, ...} => procs) procs');
-    val congs' = gen_union eq_thm (congs, congs2);
-    val mss' = Thm.set_mk_rews (empty_mss, Thm.mk_rews_of_mss mss);
-    val mss' = Thm.add_simps (mss', simps');
-    val mss' = Thm.add_simprocs (mss', meta_procs');
-    val mss' = Thm.add_congs (mss', congs');
-  in
-    make_ss (mss', simps', procs', congs', subgoal_tac, loop_tac, 
-	     finish_tac, unsafe_finish_tac)
-  end;
+fun merge_ss
+   (Simpset {mss = mss1, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac},
+    Simpset {mss = mss2, ...}) =
+  make_ss (Thm.merge_mss (mss1, mss2),
+    subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
 
 
 (* the current simpset *)
@@ -272,30 +237,31 @@
 
 (** simplification tactics **)
 
-fun NEWSUBGOALS tac tacf st0 = st0 |>
-    (tac THEN (fn st1 => tacf (nprems_of st1 - nprems_of st0) st1));
+fun NEWSUBGOALS tac tacf st0 =
+  st0 |> (tac THEN (fn st1 => tacf (nprems_of st1 - nprems_of st0) st1));
 
 (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
 fun basic_gen_simp_tac mode =
-  fn (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
-	       finish_tac, unsafe_finish_tac}) =>
-  let fun solve_all_tac mss =
-        let val ss =
-              make_ss (mss, simps, procs, congs, subgoal_tac, loop_tac,
-		       unsafe_finish_tac, unsafe_finish_tac);
-            val solve1_tac =
-              NEWSUBGOALS (subgoal_tac ss 1)
-                          (fn n => if n<0 then all_tac else no_tac)
-        in DEPTH_SOLVE(solve1_tac) end
+  fn (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac}) =>
+    let
+      fun solve_all_tac mss =
+        let
+          val ss =
+            make_ss (mss, subgoal_tac, loop_tac, unsafe_finish_tac, unsafe_finish_tac);
+          val solve1_tac =
+            NEWSUBGOALS (subgoal_tac ss 1) (fn n => if n < 0 then all_tac else no_tac)
+        in DEPTH_SOLVE solve1_tac end;
+
       fun simp_loop_tac i thm =
-          (asm_rewrite_goal_tac mode solve_all_tac mss i THEN
-           (finish_tac (prems_of_mss mss) i  ORELSE  looper i))  thm
-      and allsimp i n = EVERY(map (fn j => simp_loop_tac (i+j)) (n downto 0))
-      and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i))
+        (asm_rewrite_goal_tac mode solve_all_tac mss i THEN
+          (finish_tac (prems_of_mss mss) i ORELSE looper i)) thm
+      and allsimp i n = EVERY (map (fn j => simp_loop_tac (i + j)) (n downto 0))
+      and looper i = TRY (NEWSUBGOALS (loop_tac i) (allsimp i));
   in simp_loop_tac end;
 
-fun gen_simp_tac mode ss = basic_gen_simp_tac mode 
-			   (ss setSSolver #unsafe_finish_tac (rep_ss ss));
+fun gen_simp_tac mode (ss as Simpset {unsafe_finish_tac, ...}) =
+  basic_gen_simp_tac mode (ss setSSolver unsafe_finish_tac);
+
 
 val          simp_tac = gen_simp_tac (false, false);
 val      asm_simp_tac = gen_simp_tac (false, true);