Implemented indentation schema for conditional rewrite trace.
authornipkow
Tue Aug 28 14:25:26 2001 +0200 (2001-08-28)
changeset 11505a410fa8acfca
parent 11504 935f9e8de0d0
child 11506 244a02a2968b
Implemented indentation schema for conditional rewrite trace.
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Thu Aug 23 14:32:48 2001 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Tue Aug 28 14:25:26 2001 +0200
     1.3 @@ -54,7 +54,11 @@
     1.4  
     1.5  exception SIMPLIFIER of string * thm;
     1.6  
     1.7 -fun prnt warn a = if warn then warning a else writeln a;
     1.8 +val simp_depth = ref 0;
     1.9 +
    1.10 +fun println a = writeln(replicate_string (!simp_depth) " " ^ a)
    1.11 +
    1.12 +fun prnt warn a = if warn then warning a else println a;
    1.13  
    1.14  fun prtm warn a sign t =
    1.15    (prnt warn a; prnt warn (Sign.string_of_term sign t));
    1.16 @@ -592,27 +596,24 @@
    1.17          if perm andalso not (termless (rhs', lhs'))
    1.18          then (trace_thm false "Cannot apply permutative rewrite rule:" thm;
    1.19                trace_thm false "Term does not become smaller:" thm'; None)
    1.20 -        else
    1.21 -          let val ds = "[" ^ string_of_int depth ^ "]"
    1.22 -          in trace_thm false "Applying instance of rewrite rule:" thm;
    1.23 +        else (trace_thm false "Applying instance of rewrite rule:" thm;
    1.24             if unconditional
    1.25             then
    1.26 -             (trace_thm false (ds ^ "Rewriting:") thm';
    1.27 +             (trace_thm false "Rewriting:" thm';
    1.28                let val lr = Logic.dest_equals prop;
    1.29                    val Some thm'' = check_conv false eta_thm thm'
    1.30                in Some (thm'', uncond_skel (congs, lr)) end)
    1.31             else
    1.32 -             (trace_thm false (ds ^ "Trying to rewrite:") thm';
    1.33 +             (trace_thm false "Trying to rewrite:" thm';
    1.34                case prover (incr_depth mss) thm' of
    1.35 -                None       => (trace_thm false (ds ^ "FAILED") thm'; None)
    1.36 +                None       => (trace_thm false "FAILED" thm'; None)
    1.37                | Some thm2 =>
    1.38                    (case check_conv true eta_thm thm2 of
    1.39                       None => None |
    1.40                       Some thm2' =>
    1.41                         let val concl = Logic.strip_imp_concl prop
    1.42                             val lr = Logic.dest_equals concl
    1.43 -                       in Some (thm2', cond_skel (congs, lr)) end))
    1.44 -          end
    1.45 +                       in Some (thm2', cond_skel (congs, lr)) end)))
    1.46        end
    1.47  
    1.48      fun rews [] = None
    1.49 @@ -907,7 +908,10 @@
    1.50  
    1.51  fun rewrite_cterm mode prover mss ct =
    1.52    let val {sign, t, maxidx, ...} = rep_cterm ct
    1.53 -  in bottomc (mode, prover, sign, maxidx) mss ct end
    1.54 +      val Mss{depth, ...} = mss
    1.55 +  in simp_depth := depth;
    1.56 +     bottomc (mode, prover, sign, maxidx) mss ct
    1.57 +  end
    1.58    handle THM (s, _, thms) =>
    1.59      error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
    1.60        Pretty.string_of (pretty_thms thms));