improved tracing
authorpaulson
Fri Oct 17 11:03:48 2003 +0200 (2003-10-17)
changeset 14240d3843feb9de7
parent 14239 af2a9e68bea9
child 14241 dfae7eb2830c
improved tracing
TFL/post.ML
TFL/tfl.ML
     1.1 --- a/TFL/post.ML	Thu Oct 16 12:13:43 2003 +0200
     1.2 +++ b/TFL/post.ML	Fri Oct 17 11:03:48 2003 +0200
     1.3 @@ -138,9 +138,16 @@
     1.4                       if (solved th) then (th::So, Si, St)
     1.5                       else (So, th::Si, St)) nested_tcs ([],[],[])
     1.6                val simplified' = map join_assums simplified
     1.7 +              val dummy = (Prim.trace_thms "solved =" solved;
     1.8 +                           Prim.trace_thms "simplified' =" simplified')
     1.9                val rewr = full_simplify (ss addsimps (solved @ simplified'));
    1.10 +              val dummy = Prim.trace_thms "Simplifying the induction rule..."
    1.11 +                                          [induction]
    1.12                val induction' = rewr induction
    1.13 -              and rules'     = rewr rules
    1.14 +              val dummy = Prim.trace_thms "Simplifying the recursion rules..."
    1.15 +                                          [rules]
    1.16 +              val rules'     = rewr rules
    1.17 +              val _ = message "... Postprocessing finished";
    1.18            in
    1.19            {induction = induction',
    1.20                 rules = rules',
    1.21 @@ -162,18 +169,25 @@
    1.22  (*Strip off the outer !P*)
    1.23  val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
    1.24  
    1.25 +fun tracing true _ = ()
    1.26 +  | tracing false msg = writeln msg;
    1.27 +
    1.28  fun simplify_defn strict thy cs ss congs wfs id pats def0 =
    1.29     let val def = freezeT def0 RS meta_eq_to_obj_eq
    1.30 -       val {theory,rules,rows,TCs,full_pats_TCs} = Prim.post_definition congs (thy, (def,pats))
    1.31 +       val {theory,rules,rows,TCs,full_pats_TCs} =
    1.32 +           Prim.post_definition congs (thy, (def,pats))
    1.33         val {lhs=f,rhs} = S.dest_eq (concl def)
    1.34         val (_,[R,_]) = S.strip_comb rhs
    1.35 +       val dummy = Prim.trace_thms "congs =" congs
    1.36 +       (*the next step has caused simplifier looping in some cases*)
    1.37         val {induction, rules, tcs} =
    1.38               proof_stage strict cs ss wfs theory
    1.39                 {f = f, R = R, rules = rules,
    1.40                  full_pats_TCs = full_pats_TCs,
    1.41                  TCs = TCs}
    1.42 -       val rules' = map (standard o ObjectLogic.rulify_no_asm) (R.CONJUNCTS rules)
    1.43 -   in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
    1.44 +       val rules' = map (standard o ObjectLogic.rulify_no_asm)
    1.45 +                        (R.CONJUNCTS rules)
    1.46 +         in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
    1.47          rules = ListPair.zip(rules', rows),
    1.48          tcs = (termination_goals rules') @ tcs}
    1.49     end
     2.1 --- a/TFL/tfl.ML	Thu Oct 16 12:13:43 2003 +0200
     2.2 +++ b/TFL/tfl.ML	Fri Oct 17 11:03:48 2003 +0200
     2.3 @@ -9,6 +9,8 @@
     2.4  signature PRIM =
     2.5  sig
     2.6    val trace: bool ref
     2.7 +  val trace_thms: string -> thm list -> unit
     2.8 +  val trace_cterms: string -> cterm list -> unit
     2.9    type pattern
    2.10    val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
    2.11    val wfrec_definition0: theory -> string -> term -> term -> theory * thm
    2.12 @@ -914,6 +916,15 @@
    2.13     (R.MP rule tcthm, R.PROVE_HYP tcthm induction)
    2.14  
    2.15  
    2.16 +fun trace_thms s L =
    2.17 +  if !trace then writeln (cat_lines (s :: map string_of_thm L))
    2.18 +  else ();
    2.19 +
    2.20 +fun trace_cterms s L =
    2.21 +  if !trace then writeln (cat_lines (s :: map string_of_cterm L))
    2.22 +  else ();;
    2.23 +
    2.24 +
    2.25  fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
    2.26  let val tych = Thry.typecheck theory
    2.27      val prove = R.prove strict;
    2.28 @@ -937,19 +948,11 @@
    2.29      *   3. replace tc by tc' in both the rules and the induction theorem.
    2.30      *---------------------------------------------------------------------*)
    2.31  
    2.32 -   fun print_thms s L =
    2.33 -     if !trace then writeln (cat_lines (s :: map string_of_thm L))
    2.34 -     else ();
    2.35 -
    2.36 -   fun print_cterms s L =
    2.37 -     if !trace then writeln (cat_lines (s :: map string_of_cterm L))
    2.38 -     else ();;
    2.39 -
    2.40     fun simplify_tc tc (r,ind) =
    2.41         let val tc1 = tych tc
    2.42 -           val _ = print_cterms "TC before simplification: " [tc1]
    2.43 +           val _ = trace_cterms "TC before simplification: " [tc1]
    2.44             val tc_eq = simplifier tc1
    2.45 -           val _ = print_thms "result: " [tc_eq]
    2.46 +           val _ = trace_thms "result: " [tc_eq]
    2.47         in
    2.48         elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
    2.49         handle U.ERR _ =>