- improved logging

[helm.git] / helm / software / lambda-delta / basic_ag / bagReduction.ml

diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml
index 279ca072f1a38b5b9db5fbf96d7b956a562a1810..ca22c1dbc3f44beccf5aa05d6a9debef3cb5eb96 100644 (file)
--- a/helm/software/lambda-delta/basic_ag/bagReduction.ml
+++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml
@@ -51,6 +51,14 @@ let level = 5
 
 let error i = raise (LRefNotFound (L.items1 (string_of_int i)))
 
+let log1 s c t =
+   let sc, st = s ^ " in the context", "the term" in
+   L.log O.specs level (L.ct_items1 sc c st t)
+
+let log2 s c u t =
+   let sc, su, st = s ^ " in the context", "the term", "and the term" in
+   L.log O.specs level (L.ct_items2 sc c su u st t)
+
 let empty_machine = {i = 0; c = B.empty_context; s = []}
 
 let inc m = {m with i = succ m.i}
@@ -131,13 +139,13 @@ let rec ho_whd f c m x =
    
 let ho_whd f c t =
    let f r = L.unbox level; f r in
-   L.box level; L.log O.specs level (L.ct_items1 "Now scanning" c t);
+   L.box level; log1 "Now scanning" c t;
    ho_whd f c empty_machine t
 
 let rec are_convertible f xl c m1 t1 m2 t2 =
    let rec aux m1 r1 m2 r2 =
    let u, t = term_of_whdr r1, term_of_whdr r2 in
-   L.log O.specs level (L.ct_items2 "Now really converting" c u "and" c t);   
+   log2 "Now really converting" c u t;   
    match r1, r2 with
       | Sort_ h1, Sort_ h2                                 -> 
          if h1 = h2 then f xl else f None
@@ -181,6 +189,5 @@ and are_convertible_stacks f xl c m1 m2 =
 
 let are_convertible f c u t = 
    let f b = L.unbox level; f b in
-   L.box level;
-   L.log O.specs level (L.ct_items2 "Now converting" c u "and" c t);
+   L.box level; log2 "Now converting" c u t;
    are_convertible f (Some []) c empty_machine u empty_machine t