From: Ferruccio Guidi Date: Sun, 14 Dec 2008 22:22:38 +0000 (+0000) Subject: - improved logging X-Git-Tag: make_still_working~4398 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=426005acf6fb05116de5bae20591eefe55a4df00;p=helm.git - 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 d0c193a2a..0ca314015 100644 --- 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 589ce60f0..4e7ab87a0 100644 --- 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 0310e8d28..b0cd88d6c 100644 --- 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 25725520d..ad75d63b8 100644 --- 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 a651c6e33..52c485ae7 100644 --- 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 b33f6726b..fd99db2d2 100644 --- 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 "@,@[%s" " "; F.pp_print_if_newline std () +let box l = + if !level >= l then + begin F.fprintf std "@,@[%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 "@[" diff --git a/helm/software/lambda-delta/lib/log.mli b/helm/software/lambda-delta/lib/log.mli index 43e811915..821cb0f31 100644 --- 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 1286db0bb..f1cea379d 100644 --- 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 = " output intermediate representation" in let help_s = " 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);