X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgOutput.ml;h=5dc3887c572799dd6b68c8722cadd41f79bf76b4;hb=de66af7241ad8ab71d5857d14570e4662f2488dc;hp=66c7ed3d87a980350f00e2532ca5992e276fb841;hpb=f23388dbd51574725a11b0ab5373f09838a32ab5;p=helm.git diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index 66c7ed3d8..5dc3887c5 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -11,70 +11,97 @@ module P = Printf module F = Format -module U = NUri module C = Cps +module U = NUri module L = Log module H = Hierarchy +module O = Output module B = Brg +(* nodes count **************************************************************) + type counters = { eabsts: int; eabbrs: int; + evoids: int; tsorts: int; tlrefs: int; tgrefs: int; tcasts: int; tappls: int; tabsts: int; - tabbrs: int + tabbrs: int; + tvoids: int; + uris : B.uri list; + nodes : int; + xnodes: int } -let indexes = ref false - let initial_counters = { - eabsts = 0; eabbrs = 0; tsorts = 0; tlrefs = 0; tgrefs = 0; - tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0 + eabsts = 0; eabbrs = 0; evoids = 0; + tsorts = 0; tlrefs = 0; tgrefs = 0; tcasts = 0; tappls = 0; + tabsts = 0; tabbrs = 0; tvoids = 0; + uris = []; nodes = 0; xnodes = 0 } -let rec count_term_binder f c = function +let rec count_term_binder f c e = function | B.Abst w -> - let c = {c with tabsts = succ c.tabsts} in - count_term f c w + let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in + count_term f c e w | B.Abbr v -> - let c = {c with tabbrs = succ c.tabbrs} in - count_term f c v - | B.Void -> f c - -and count_term f c = function - | B.Sort _ -> - f {c with tsorts = succ c.tsorts} - | B.LRef _ -> - f {c with tlrefs = succ c.tlrefs} - | B.GRef _ -> + let c = {c with tabbrs = succ c.tabbrs; xnodes = succ c.xnodes} in + count_term f c e v + | B.Void -> + let c = {c with tvoids = succ c.tvoids; xnodes = succ c.xnodes} in + f c + +and count_term f c e = function + | B.Sort _ -> + f {c with tsorts = succ c.tsorts; nodes = succ c.nodes} + | B.LRef (_, i) -> + let err _ = f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes} in + let f _ _ = function + | B.Abst _ + | B.Void -> + f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes} + | B.Abbr _ -> + f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes} + in + B.get err f e i + | B.GRef (_, u) -> + let c = + if Cps.list_mem ~eq:U.eq u c.uris + then {c with nodes = succ c.nodes} + else {c with xnodes = succ c.xnodes} + in 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) -> - 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, t) -> - let f c = count_term_binder f c b in - count_term f c t - -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 f c = count_term f c e t in + count_term f c e v + | B.Appl (_, v, t) -> + let c = {c with tappls = succ c.tappls; nodes = succ c.nodes} in + let f c = count_term f c e t in + count_term f c e v + | B.Bind (a, b, t) -> + let f c e = count_term f c e t in + let f c = B.push (f c) e a b in + count_term_binder f c e b -let count_obj f c (_, _, b) = - count_obj_binder f c b +let count_obj f c = function + | (_, u, B.Abst w) -> + let c = {c with + eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris + } in + count_term f c B.empty_context w + | (_, _, B.Abbr v) -> + let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in + count_term f c B.empty_context v + | (_, u, B.Void) -> + let c = {c with + evoids = succ c.evoids; nodes = succ c.nodes; uris = u :: c.uris + } in + f c let count_item f c = function | Some obj -> count_obj f c obj @@ -86,65 +113,119 @@ let print_counters f c = c.tabbrs in let items = c.eabsts + c.eabbrs in + let nodes = c.nodes + c.xnodes in L.warn (P.sprintf " Kernel representation summary (basic_rg)"); - L.warn (P.sprintf " Total entry items: %6u" items); - L.warn (P.sprintf " Declaration items: %6u" c.eabsts); - L.warn (P.sprintf " Definition items: %6u" c.eabbrs); - L.warn (P.sprintf " Total term items: %6u" terms); - L.warn (P.sprintf " Sort items: %6u" c.tsorts); - L.warn (P.sprintf " Local reference items: %6u" c.tlrefs); - L.warn (P.sprintf " Global reference items: %6u" c.tgrefs); - L.warn (P.sprintf " Explicit Cast items: %6u" c.tcasts); - 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 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); + L.warn (P.sprintf " Global Int. Complexity: %7u" c.nodes); + L.warn (P.sprintf " + Abbreviation nodes: %7u" nodes); f () +(* context/term pretty printing *********************************************) + +let id frm a = + let f n = function + | true -> F.fprintf frm "%s" n + | false -> F.fprintf frm "^%s" n + in + B.name C.err 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 (id, _) -> F.fprintf frm "@[%s@]" id - | None -> F.fprintf frm "@[#%u@]" i - in - if !indexes then f None else B.get f c i - | B.GRef s -> F.fprintf frm "@[$%s@]" (U.string_of_uri s) - | B.Cast (u, t) -> + | B.Sort (_, h) -> + let err () = F.fprintf frm "@[*%u@]" h in + let f s = F.fprintf frm "@[%s@]" s in + H.get_sort err f h + | B.LRef (_, i) -> + let err i = F.fprintf frm "@[#%u@]" i in + let f _ a _ = F.fprintf frm "@[%a@]" id a in + if !O.indexes then err i else B.get err 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) -> + | B.Appl (_, v, t) -> F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t - | B.Bind (id, B.Abst w, t) -> + | B.Bind (a, B.Abst w, t) -> let f cc = - F.fprintf frm "@[[%s:%a].%a@]" id (pp_term c) w (pp_term cc) t + F.fprintf frm "@[[%a:%a].%a@]" id a (pp_term c) w (pp_term cc) t in - B.push f c id (B.Abst w) - | B.Bind (id, B.Abbr v, t) -> + B.push f c a (B.Abst w) + | B.Bind (a, B.Abbr v, t) -> let f cc = - F.fprintf frm "@[[%s=%a].%a@]" id (pp_term c) v (pp_term cc) t + F.fprintf frm "@[[%a=%a].%a@]" id a (pp_term c) v (pp_term cc) t in - B.push f c id (B.Abbr v) - | B.Bind (id, B.Void, t) -> - let f cc = F.fprintf frm "@[[%s].%a@]" id (pp_term cc) t in - B.push f c id B.Void + 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 - | id, B.Abst w -> - F.fprintf frm "@,@[%s : %a@]" id (pp_term c) w - | id, B.Abbr v -> - F.fprintf frm "@,@[%s = %a@]" id (pp_term c) v - | id, B.Void -> - F.fprintf frm "@,%s" id + let pp_entry f c a = function + | B.Abst w -> + F.fprintf frm "@,@[%a : %a@]" id a (pp_term c) w; f () + | B.Abbr v -> + F.fprintf frm "@,@[%a = %a@]" id a (pp_term c) v; f () + | B.Void -> + F.fprintf frm "@,%a" id a; f () 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 + B.rev_iter C.start pp_entry c let specs = { L.pp_term = pp_term; L.pp_context = pp_context } + +(* term xml printing ********************************************************) + +let id frm a = + let f s = function + | true -> F.fprintf frm " name=%S" s + | false -> F.fprintf frm " name=%S" ("^" ^ s) + in + B.name C.start f a + +let rec exp_term frm = function + | B.Sort (a, l) -> + F.fprintf frm "" (string_of_int l) id a + | B.LRef (a, i) -> + F.fprintf frm "" (string_of_int i) id a + | B.GRef (a, u) -> + F.fprintf frm "" (U.string_of_uri u) id a + | B.Cast (a, w, t) -> + F.fprintf frm "%a%a" id a exp_boxed w exp_term t + | B.Appl (a, v, t) -> + F.fprintf frm "%a%a" id a exp_boxed v exp_term t + | B.Bind (a, b, t) -> + F.fprintf frm "%a%a" (exp_bind a) b exp_term t + +and exp_boxed frm t = + F.fprintf frm "@,@[ %a@]@," exp_term t + +and exp_bind a frm = function + | B.Abst w -> + F.fprintf frm "%a" id a exp_boxed w + | B.Abbr v -> + F.fprintf frm "%a" id a exp_boxed v + | B.Void -> + F.fprintf frm "" id a + +let exp_obj frm = function + | _, uri, B.Abst w -> + let str = U.string_of_uri uri in + F.fprintf frm "@,%a" str exp_term w + | _, uri, B.Abbr v -> + let str = U.string_of_uri uri in + F.fprintf frm "@,%a" str exp_term v + | _, uri, B.Void -> + let str = U.string_of_uri uri in + F.fprintf frm "" str + +let export_obj frm obj = + F.fprintf frm "@,@[ %a@]@," exp_obj obj