X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgOutput.ml;h=ac873ec6677dd24cdc27c8745edb996b6baea16f;hb=1be981691870cca039b1af1fb954491c2020d483;hp=a491778558762f1128710d9d4102a2edfe01e304;hpb=bbc1c6ccb596693c46f4d75d7875b94c79f1d575;p=helm.git diff --git a/helm/software/helena/src/basic_rg/brgOutput.ml b/helm/software/helena/src/basic_rg/brgOutput.ml index a49177855..ac873ec66 100644 --- a/helm/software/helena/src/basic_rg/brgOutput.ml +++ b/helm/software/helena/src/basic_rg/brgOutput.ml @@ -9,7 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module P = Printf +module KP = Printf module U = NUri module C = Cps @@ -18,6 +18,7 @@ module G = Options module H = Hierarchy module N = Layer module E = Entity +module R = Alpha module XD = XmlCrg module B = Brg module BD = BrgCrg @@ -51,13 +52,13 @@ let initial_counters = { } let rec count_term_binder f c e = function - | B.Abst (_, w) -> + | B.Abst (_, _, w) -> let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in count_term f c e w - | B.Abbr v -> + | B.Abbr v -> let c = {c with tabbrs = succ c.tabbrs; xnodes = succ c.xnodes} in count_term f c e v - | B.Void -> + | B.Void -> let c = {c with tvoids = succ c.tvoids; xnodes = succ c.xnodes} in f c @@ -109,107 +110,79 @@ let print_counters f c = in let items = c.eabsts + c.eabbrs in let nodes = c.nodes + c.xnodes in - L.warn level (P.sprintf "Kernel representation summary (basic_rg)"); - L.warn level (P.sprintf " Total entry items: %7u" items); - L.warn level (P.sprintf " Declaration items: %7u" c.eabsts); - L.warn level (P.sprintf " Definition items: %7u" c.eabbrs); - L.warn level (P.sprintf " Total term items: %7u" terms); - L.warn level (P.sprintf " Sort items: %7u" c.tsorts); - L.warn level (P.sprintf " Local reference items: %7u" c.tlrefs); - L.warn level (P.sprintf " Global reference items: %7u" c.tgrefs); - L.warn level (P.sprintf " Explicit Cast items: %7u" c.tcasts); - L.warn level (P.sprintf " Application items: %7u" c.tappls); - L.warn level (P.sprintf " Abstraction items: %7u" c.tabsts); - L.warn level (P.sprintf " Abbreviation items: %7u" c.tabbrs); - L.warn level (P.sprintf " Global Int. Complexity: %7u" c.nodes); - L.warn level (P.sprintf " + Abbreviation nodes: %7u" nodes); + L.warn level (KP.sprintf "Kernel representation summary (basic_rg)"); + L.warn level (KP.sprintf " Total entry items: %7u" items); + L.warn level (KP.sprintf " Declaration items: %7u" c.eabsts); + L.warn level (KP.sprintf " Definition items: %7u" c.eabbrs); + L.warn level (KP.sprintf " Total term items: %7u" terms); + L.warn level (KP.sprintf " Sort items: %7u" c.tsorts); + L.warn level (KP.sprintf " Local reference items: %7u" c.tlrefs); + L.warn level (KP.sprintf " Global reference items: %7u" c.tgrefs); + L.warn level (KP.sprintf " Explicit Cast items: %7u" c.tcasts); + L.warn level (KP.sprintf " Application items: %7u" c.tappls); + L.warn level (KP.sprintf " Abstraction items: %7u" c.tabsts); + L.warn level (KP.sprintf " Abbreviation items: %7u" c.tabbrs); + L.warn level (KP.sprintf " Global Int. Complexity: %7u" c.nodes); + L.warn level (KP.sprintf " + Abbreviation nodes: %7u" nodes); f () -(* supplementary annotation *************************************************) - -let rec does_not_occur f n r = function - | B.Null -> f true - | B.Cons (e, _, a, _) -> - let f n1 r1 = - if n1 = n && r1 = r then f false else does_not_occur f n r e - in - E.name C.err f a - -let rename f e a = - let rec aux f e n r = - let f = function - | true -> f n r - | false -> aux f e (n ^ "_") r - in - does_not_occur f n r e - in - let f n0 r0 = - let f n r = if n = n0 && r = r0 then f a else f {a with E.n_name = Some (n, r)} in - aux f e n0 r0 - in - E.name C.err f a - (* lenv/term pretty printing ************************************************) let name err och a = let f n = function - | true -> P.fprintf och "%s" n - | false -> P.fprintf och "-%s" n - in + | true -> KP.fprintf och "%s" n + | false -> KP.fprintf och "-%s" n + in E.name err f a +let pp_reduced och x = + if x then KP.fprintf och "%s" "^" + let pp_level st och n = - P.fprintf och "%s" (N.to_string st n) + KP.fprintf och "%s" (N.to_string st n) let rec pp_term st e och = function - | B.Sort (_, h) -> - let err _ = P.fprintf och "*%u" h in - let f s = P.fprintf och "%s" s in + | B.Sort (_, h) -> + let err _ = KP.fprintf och "*%u" h in + let f s = KP.fprintf och "%s" s in H.string_of_sort err f h - | B.LRef (_, i) -> - let err _ = P.fprintf och "#%u" i in + | B.LRef (_, i) -> + let err _ = KP.fprintf och "#%u" i in if !G.indexes then err () else let _, _, a, b = B.get e i in - P.fprintf och "%a" (name err) a - | B.GRef (_, s) -> - P.fprintf och "$%s" (U.string_of_uri s) - | B.Cast (_, u, t) -> - P.fprintf och "{%a}.%a" (pp_term st e) u (pp_term st e) t - | B.Appl (_, v, t) -> - P.fprintf och "(%a).%a" (pp_term st e) v (pp_term st e) t - | B.Bind (a, B.Abst (n, w), t) -> - let f a = - let ee = B.push e B.empty a (B.abst n w) in - P.fprintf och "%a[%a:%a].%a" (pp_level st) n (name C.err) a (pp_term st e) w (pp_term st ee) t - in - rename f e a - | B.Bind (a, B.Abbr v, t) -> - let f a = - let ee = B.push e B.empty a (B.abbr v) in - P.fprintf och "[%a=%a].%a" (name C.err) a (pp_term st e) v (pp_term st ee) t - in - rename f e a - | B.Bind (a, B.Void, t) -> - let f a = - let ee = B.push e B.empty a B.Void in - P.fprintf och "[%a].%a" (name C.err) a (pp_term st ee) t - in - rename f e a + KP.fprintf och "%a" (name err) a + | B.GRef (_, s) -> + KP.fprintf och "$%s" (U.string_of_uri s) + | B.Cast (_, u, t) -> + KP.fprintf och "{%a}.%a" (pp_term st e) u (pp_term st e) t + | B.Appl (_, v, t) -> + KP.fprintf och "(%a).%a" (pp_term st e) v (pp_term st e) t + | B.Bind (a, B.Abst (x, n, w), t) -> + let a = R.alpha B.mem e a in + let ee = B.push e B.empty a (B.abst x n w) in + KP.fprintf och "%a%a[%a:%a].%a" (pp_level st) n pp_reduced x (name C.start) a (pp_term st e) w (pp_term st ee) t + | B.Bind (a, B.Abbr v, t) -> + let a = R.alpha B.mem e a in + let ee = B.push e B.empty a (B.abbr v) in + KP.fprintf och "[%a=%a].%a" (name C.start) a (pp_term st e) v (pp_term st ee) t + | B.Bind (a, B.Void, t) -> + let a = R.alpha B.mem e a in + let ee = B.push e B.empty a B.Void in + KP.fprintf och "[%a].%a" (name C.start) a (pp_term st ee) t let pp_lenv st och e = - let pp_entry f e c a b x = f x (* match b with - | B.Abst (a, w) -> - let f a = P.fprintf och "%a : %a\n" (name C.err) a (pp_term st e) w; f a in - rename f x a - | B.Abbr (a, v) -> - let f a = P.fprintf och "%a = %a\n" (name C.err) a (pp_term st e) v; f a in - rename f c a - | B.Void a -> - let f a = P.fprintf och "%a\n" (name C.err) a; f a in - rename f c a -*) in - let e = B.empty in - if e = B.empty then P.fprintf och "%s\n" "not shown" else + let pp_entry f c a b x = + let a = R.alpha B.mem e a in + let x = B.push x c a b in + match b with + | B.Abst (_, _, w) -> + KP.fprintf och "[%a : %a] " (name C.start) a (pp_term st c) w; f x + | B.Abbr v -> + KP.fprintf och "[%a = %a] " (name C.start) a (pp_term st c) v; f x + | B.Void -> + KP.fprintf och "[%a]" (name C.start) a; f x + in + if e = B.empty then KP.fprintf och "%s" "empty" else B.fold_right ignore pp_entry e B.empty let specs = {