X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgOutput.ml;h=2d1fa96ae846b1f81cc10fa06ebc637af621ad2f;hb=55274856efac172aba293d4216fdc659d07a89d7;hp=741a2567dbb41fdb4dd8b56acdfdc28b825c5fa7;hpb=e86383ae4805a526b3acca2ef3c936b3f22daaad;p=helm.git diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index 741a2567d..2d1fa96ae 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -9,8 +9,16 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module P = Printf +module F = Format +module U = NUri +module L = Log +module H = Hierarchy +module O = Output module B = Brg +(* nodes count **************************************************************) + type counters = { eabsts: int; eabbrs: int; @@ -28,41 +36,49 @@ let initial_counters = { tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0 } -let count_term_binder f c = function - | B.Abst -> f {c with tabsts = succ c.tabsts} - | B.Abbr -> f {c with tabbrs = succ c.tabbrs} +let rec count_term_binder f c = function + | B.Abst w -> + let c = {c with tabsts = succ c.tabsts} in + count_term f c w + | B.Abbr v -> + let c = {c with tabbrs = succ c.tabbrs} in + count_term f c v + | B.Void -> f c -let rec count_term f c = function +and count_term f c = function | B.Sort _ -> f {c with tsorts = succ c.tsorts} - | B.LRef _ -> + | B.LRef _ -> f {c with tlrefs = succ c.tlrefs} - | B.GRef _ -> + | B.GRef _ -> f {c with tgrefs = succ c.tgrefs} - | B.Cast (v, t) -> + | B.Cast (_, v, t) -> let c = {c with tcasts = succ c.tcasts} in let f c = count_term f c t in count_term f c v - | B.Appl (v, t) -> + | B.Appl (_, v, t) -> let c = {c with tappls = succ c.tappls} in let f c = count_term f c t in count_term f c v - | B.Bind (_, b, u, t) -> + | B.Bind (_, b, t) -> let f c = count_term_binder f c b in - let f c = count_term f c t in - count_term f c u + count_term f c t -let count_entry_binder f c = function - | B.Abst -> f {c with eabsts = succ c.eabsts} - | B.Abbr -> f {c with eabbrs = succ c.eabbrs} +let count_obj_binder f c = function + | B.Abst w -> + let c = {c with eabsts = succ c.eabsts} in + count_term f c w + | B.Abbr v -> + let c = {c with eabbrs = succ c.eabbrs} in + count_term f c v + | B.Void -> f c -let count_entry f c (_, b, t) = - let f c = count_entry_binder f c b in - count_term f c t +let count_obj f c (_, _, b) = + count_obj_binder f c b let count_item f c = function - | Some e -> count_entry f c e - | None -> f c + | Some obj -> count_obj f c obj + | None -> f c let print_counters f c = let terms = @@ -70,16 +86,75 @@ let print_counters f c = c.tabbrs in let items = c.eabsts + c.eabbrs in - Printf.printf " Kernel representation summary (basic_rg)\n"; - Printf.printf " Total entry items: %6u\n" items; - Printf.printf " Declaration items: %6u\n" c.eabsts; - Printf.printf " Definition items: %6u\n" c.eabbrs; - Printf.printf " Total term items: %6u\n" terms; - Printf.printf " Sort items: %6u\n" c.tsorts; - Printf.printf " Local reference items: %6u\n" c.tlrefs; - Printf.printf " Global reference items: %6u\n" c.tgrefs; - Printf.printf " Explicit Cast items: %6u\n" c.tcasts; - Printf.printf " Application items: %6u\n" c.tappls; - Printf.printf " Abstraction items: %6u\n" c.tabsts; - Printf.printf " Abbreviation items: %6u\n" c.tabbrs; - flush stdout; f () + L.warn (P.sprintf " Kernel representation summary (basic_rg)"); + L.warn (P.sprintf " Total entry items: %7u" items); + L.warn (P.sprintf " Declaration items: %7u" c.eabsts); + L.warn (P.sprintf " Definition items: %7u" c.eabbrs); + L.warn (P.sprintf " Total term items: %7u" terms); + L.warn (P.sprintf " Sort items: %7u" c.tsorts); + L.warn (P.sprintf " Local reference items: %7u" c.tlrefs); + L.warn (P.sprintf " Global reference items: %7u" c.tgrefs); + L.warn (P.sprintf " Explicit Cast items: %7u" c.tcasts); + L.warn (P.sprintf " Application items: %7u" c.tappls); + L.warn (P.sprintf " Abstraction items: %7u" c.tabsts); + L.warn (P.sprintf " Abbreviation items: %7u" c.tabbrs); + f () + +(* context/term pretty printing *********************************************) + +let id frm a = + let f = function + | None -> assert false + | Some (true, n) -> F.fprintf frm "%s" n + | Some (false, n) -> F.fprintf frm "^%s" n + in + B.name f a + +let rec pp_term c frm = function + | B.Sort (_, h) -> + let f = function + | Some s -> F.fprintf frm "@[%s@]" s + | None -> F.fprintf frm "@[*%u@]" h + in + H.get_sort f h + | B.LRef (_, i) -> + let f _ = function + | Some (a, _) -> F.fprintf frm "@[%a@]" id a + | None -> F.fprintf frm "@[#%u@]" i + in + if !O.indexes then f 0 None else B.get f c i + | B.GRef (_, s) -> F.fprintf frm "@[$%s@]" (U.string_of_uri s) + | B.Cast (_, u, t) -> + F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t + | B.Appl (_, v, t) -> + F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t + | B.Bind (a, B.Abst w, t) -> + let f cc = + F.fprintf frm "@[[%a:%a].%a@]" id a (pp_term c) w (pp_term cc) t + in + B.push f c a (B.Abst w) + | B.Bind (a, B.Abbr v, t) -> + let f cc = + F.fprintf frm "@[[%a=%a].%a@]" id a (pp_term c) v (pp_term cc) t + in + B.push f c a (B.Abbr v) + | B.Bind (a, B.Void, t) -> + let f cc = F.fprintf frm "@[[%a].%a@]" id a (pp_term cc) t in + B.push f c a B.Void + +let pp_context frm c = + let pp_entry frm = function + | a, B.Abst w -> + F.fprintf frm "@,@[%a : %a@]" id a (pp_term c) w + | a, B.Abbr v -> + F.fprintf frm "@,@[%a = %a@]" id a (pp_term c) v + | a, B.Void -> + F.fprintf frm "@,%a" id a + in + let iter map frm l = List.iter (map frm) l in + let f es = F.fprintf frm "%a" (iter pp_entry) (List.rev es) in + B.contents f c + +let specs = { + L.pp_term = pp_term; L.pp_context = pp_context +}