# HG changeset patch
# User paulson
# Date 1066381428 -7200
# Node ID d3843feb9de77c94e2d2474e21f02d7b06175dd4
# Parent  af2a9e68bea92f5c2190ea6185a22bbb868788d2
improved tracing

diff -r af2a9e68bea9 -r d3843feb9de7 TFL/post.ML
--- a/TFL/post.ML	Thu Oct 16 12:13:43 2003 +0200
+++ b/TFL/post.ML	Fri Oct 17 11:03:48 2003 +0200
@@ -138,9 +138,16 @@
                      if (solved th) then (th::So, Si, St)
                      else (So, th::Si, St)) nested_tcs ([],[],[])
               val simplified' = map join_assums simplified
+              val dummy = (Prim.trace_thms "solved =" solved;
+                           Prim.trace_thms "simplified' =" simplified')
               val rewr = full_simplify (ss addsimps (solved @ simplified'));
+              val dummy = Prim.trace_thms "Simplifying the induction rule..."
+                                          [induction]
               val induction' = rewr induction
-              and rules'     = rewr rules
+              val dummy = Prim.trace_thms "Simplifying the recursion rules..."
+                                          [rules]
+              val rules'     = rewr rules
+              val _ = message "... Postprocessing finished";
           in
           {induction = induction',
                rules = rules',
@@ -162,18 +169,25 @@
 (*Strip off the outer !P*)
 val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
 
+fun tracing true _ = ()
+  | tracing false msg = writeln msg;
+
 fun simplify_defn strict thy cs ss congs wfs id pats def0 =
    let val def = freezeT def0 RS meta_eq_to_obj_eq
-       val {theory,rules,rows,TCs,full_pats_TCs} = Prim.post_definition congs (thy, (def,pats))
+       val {theory,rules,rows,TCs,full_pats_TCs} =
+           Prim.post_definition congs (thy, (def,pats))
        val {lhs=f,rhs} = S.dest_eq (concl def)
        val (_,[R,_]) = S.strip_comb rhs
+       val dummy = Prim.trace_thms "congs =" congs
+       (*the next step has caused simplifier looping in some cases*)
        val {induction, rules, tcs} =
              proof_stage strict cs ss wfs theory
                {f = f, R = R, rules = rules,
                 full_pats_TCs = full_pats_TCs,
                 TCs = TCs}
-       val rules' = map (standard o ObjectLogic.rulify_no_asm) (R.CONJUNCTS rules)
-   in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
+       val rules' = map (standard o ObjectLogic.rulify_no_asm)
+                        (R.CONJUNCTS rules)
+         in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
         rules = ListPair.zip(rules', rows),
         tcs = (termination_goals rules') @ tcs}
    end
diff -r af2a9e68bea9 -r d3843feb9de7 TFL/tfl.ML
--- a/TFL/tfl.ML	Thu Oct 16 12:13:43 2003 +0200
+++ b/TFL/tfl.ML	Fri Oct 17 11:03:48 2003 +0200
@@ -9,6 +9,8 @@
 signature PRIM =
 sig
   val trace: bool ref
+  val trace_thms: string -> thm list -> unit
+  val trace_cterms: string -> cterm list -> unit
   type pattern
   val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
   val wfrec_definition0: theory -> string -> term -> term -> theory * thm
@@ -914,6 +916,15 @@
    (R.MP rule tcthm, R.PROVE_HYP tcthm induction)
 
 
+fun trace_thms s L =
+  if !trace then writeln (cat_lines (s :: map string_of_thm L))
+  else ();
+
+fun trace_cterms s L =
+  if !trace then writeln (cat_lines (s :: map string_of_cterm L))
+  else ();;
+
+
 fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
 let val tych = Thry.typecheck theory
     val prove = R.prove strict;
@@ -937,19 +948,11 @@
     *   3. replace tc by tc' in both the rules and the induction theorem.
     *---------------------------------------------------------------------*)
 
-   fun print_thms s L =
-     if !trace then writeln (cat_lines (s :: map string_of_thm L))
-     else ();
-
-   fun print_cterms s L =
-     if !trace then writeln (cat_lines (s :: map string_of_cterm L))
-     else ();;
-
    fun simplify_tc tc (r,ind) =
        let val tc1 = tych tc
-           val _ = print_cterms "TC before simplification: " [tc1]
+           val _ = trace_cterms "TC before simplification: " [tc1]
            val tc_eq = simplifier tc1
-           val _ = print_thms "result: " [tc_eq]
+           val _ = trace_thms "result: " [tc_eq]
        in
        elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
        handle U.ERR _ =>