- improved logging

- optimization in subst

diff --git a/helm/software/lambda-delta/basic_ag/bag.ml b/helm/software/lambda-delta/basic_ag/bag.ml
index d0c193a2a71a0ad4528d21952320ae93ea022181..0ca3140151d4e5eefaa3f0d90aa92eec43d0ab5f 100644 (file)
--- a/helm/software/lambda-delta/basic_ag/bag.ml
+++ b/helm/software/lambda-delta/basic_ag/bag.ml
@@ -55,6 +55,8 @@ let location = ref 0
 
 let new_location () = let loc = !location in incr location; loc
 
+let locations () = !location
+
 (* context handling functions ***********************************************)
 
 let empty_context = []

diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.ml b/helm/software/lambda-delta/basic_ag/bagOutput.ml
index 589ce60f0f89912bfdf2eba98c448c01345ebceb..4e7ab87a027234fd21ecf276c77257a45b7ddbda 100644 (file)
--- a/helm/software/lambda-delta/basic_ag/bagOutput.ml
+++ b/helm/software/lambda-delta/basic_ag/bagOutput.ml
@@ -84,6 +84,7 @@ let print_counters f c =
       c.tabbrs
    in
    let items = c.eabsts + c.eabbrs in
+   let locations = B.locations () in
    L.warn (P.sprintf "  Kernel representation summary (basic_ag)");
    L.warn (P.sprintf "    Total entry items:        %6u" items);
    L.warn (P.sprintf "      Declaration items:      %6u" c.eabsts);
@@ -96,6 +97,7 @@ let print_counters f c =
    L.warn (P.sprintf "      Application items:      %6u" c.tappls);
    L.warn (P.sprintf "      Abstraction items:      %6u" c.tabsts);
    L.warn (P.sprintf "      Abbreviation items:     %6u" c.tabbrs);
+   L.warn (P.sprintf "    Total binder locations:   %6u" locations);   
    f ()
 
 let indexes = ref false

diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml
index 0310e8d2833de378e435ae3ffcf80b998da5dcad..b0cd88d6cc3b66d41136ec36fae68d2878f1270c 100644 (file)
--- a/helm/software/lambda-delta/basic_ag/bagReduction.ml
+++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml
@@ -107,8 +107,8 @@ let rec ho_whd f c m x =
    whd aux c m x
    
 let ho_whd f c t =
-   let f c r = L.unbox (); f c r in
-   L.box (); L.log O.specs level (L.ct_items1 "Now scanning" c t);
+   let f c r = L.unbox level; f c r in
+   L.box level; L.log O.specs level (L.ct_items1 "Now scanning" c t);
    ho_whd f c empty_machine t
 
 let rec are_convertible f c m1 t1 m2 t2 =
@@ -148,7 +148,7 @@ and are_convertible_stacks f c m1 m2 =
    C.forall2 f map m1.s m2.s
 
 let are_convertible f c t1 t2 = 
-   let f b = L.unbox (); f b in
-   L.box ();
+   let f b = L.unbox level; f b in
+   L.box level;
    L.log O.specs level (L.ct_items2 "Now converting" c t1 "and" c t2);
    are_convertible f c empty_machine t1 empty_machine t2

diff --git a/helm/software/lambda-delta/basic_ag/bagSubstitution.ml b/helm/software/lambda-delta/basic_ag/bagSubstitution.ml
index 25725520dca13730153d53d0cf4aa8259e7b09c5..ad75d63b83e06efbefed39b32d6f172ac044329c 100644 (file)
--- a/helm/software/lambda-delta/basic_ag/bagSubstitution.ml
+++ b/helm/software/lambda-delta/basic_ag/bagSubstitution.ml
@@ -45,4 +45,4 @@ and lref_map f map t = match t with
 
 let subst f new_l old_l t =
    let map i = if i = old_l then new_l else i in
-   lref_map f map t
+   if new_l = old_l then f t else lref_map f map t

diff --git a/helm/software/lambda-delta/basic_ag/bagType.ml b/helm/software/lambda-delta/basic_ag/bagType.ml
index a651c6e3379b3dbf586009f3a1e28d9d828deef2..52c485ae740426c3a178d03efd4438593905390a 100644 (file)
--- a/helm/software/lambda-delta/basic_ag/bagType.ml
+++ b/helm/software/lambda-delta/basic_ag/bagType.ml
@@ -90,9 +90,9 @@ let rec b_type_of f g c x =
       let h xv vv xt tt cc = function
          | R.Sort _ -> error1 "not a function" c xt
         | R.Abst w -> 
-            L.box ();
+            L.box (succ level);
            L.log O.specs (succ level) (L.ct_items1 "Just scanned" cc w);
-           L.unbox ();
+           L.unbox (succ level);
            let f b =
               if b then f (S.sh2 v xv t xt x B.appl) (B.appl xv tt) else
               error2 "the term" cc xv "must be of type" cc w
@@ -117,5 +117,5 @@ let rec b_type_of f g c x =
       type_of f g c u
 
 and type_of f g c x =
-   let f t u = L.unbox (); f t u in
-   L.box (); b_type_of f g c x
+   let f t u = L.unbox level; f t u in
+   L.box level; b_type_of f g c x

diff --git a/helm/software/lambda-delta/lib/log.ml b/helm/software/lambda-delta/lib/log.ml
index b33f6726b9b148d54bb15474eb23cf14853f3240..fd99db2d2c24d1b85d721cd990839d947f9a4ca6 100644 (file)
--- a/helm/software/lambda-delta/lib/log.ml
+++ b/helm/software/lambda-delta/lib/log.ml
@@ -31,12 +31,6 @@ let std = F.std_formatter
 
 let err = F.err_formatter
 
-let init =
-   let started = ref false in
-   fun () ->
-      if !started then () else 
-      begin P.printf "\n"; started := true end
-
 let pp_items frm st l items =   
    let pp_item frm = function
       | Term (c, t) -> F.fprintf frm "%a@,%a" st.pp_context c (st.pp_term c) t
@@ -49,15 +43,13 @@ let pp_items frm st l items =
 
 (* Interface functions ******************************************************)
 
-(*
-let warn msg = 
-   init (); P.printf " %s\n" msg; flush stdout
-*)
-let box () = F.fprintf std "@,@[<v 2>%s" "  "; F.pp_print_if_newline std ()
+let box l = 
+   if !level >= l then
+   begin F.fprintf std "@,@[<v 2>%s" "  "; F.pp_print_if_newline std () end
 
-let unbox () = F.fprintf std "@]"
+let unbox l = if !level >= l then F.fprintf std "@]"
 
-let flush () = F.fprintf std "@]@."
+let flush l = if !level >= l then F.fprintf std "@]@."
 
 let box_err () = F.fprintf err "@[<v>"
 

diff --git a/helm/software/lambda-delta/lib/log.mli b/helm/software/lambda-delta/lib/log.mli
index 43e81191597a844771504b62dfcd4822f5cda966..821cb0f3180063d09fcd854e5022f9854c8af2fb 100644 (file)
--- a/helm/software/lambda-delta/lib/log.mli
+++ b/helm/software/lambda-delta/lib/log.mli
@@ -23,11 +23,11 @@ val level: int ref
 
 val warn: string -> unit
 
-val box: unit -> unit
+val box: int -> unit
 
-val unbox: unit -> unit
+val unbox: int -> unit
 
-val flush: unit -> unit
+val flush: int -> unit
 
 val box_err: unit -> unit
 

diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index 1286db0bbd186c0030c07dcd4db0b035ffb553c9..f1cea379dc0db8396a370daa014d4e151332479a 100644 (file)
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -38,7 +38,7 @@ let initial_status = {
 let count count_fun c item =
    if !L.level > 2 then count_fun C.start c item else c
 
-let flush () = L.flush (); L.flush_err ()
+let flush () = L.flush 0; L.flush_err ()
 
 let bag_error s msg =
    L.error BagO.specs (L.Warn s :: msg); flush () 
@@ -129,7 +129,7 @@ try
    let help_i = " show local references by index" in
    let help_m = "<file>  output intermediate representation" in
    let help_s = "<number>  Set translation stage" in
-   L.box (); L.box_err ();
+   L.box 0; L.box_err ();
    H.set_new_sorts ignore ["Set"; "Prop"];
    Arg.parse [
       ("-S", Arg.Int set_summary, help_S);