X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgOutput.ml;h=7bb9ce4363a73c9d91cf64cf1719224b521077c8;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hp=6a40aecd4df2c87a09a596cf5378e0352bdb7229;hpb=a7e986f3c381186e58aa1c6a65f03ee721deb9b1;p=helm.git diff --git a/helm/software/helena/src/basic_rg/brgOutput.ml b/helm/software/helena/src/basic_rg/brgOutput.ml index 6a40aecd4..7bb9ce436 100644 --- a/helm/software/helena/src/basic_rg/brgOutput.ml +++ b/helm/software/helena/src/basic_rg/brgOutput.ml @@ -52,6 +52,8 @@ let initial_counters = { uris = []; nodes = 0; xnodes = 0 } +IFDEF SUMMARY THEN + let rec count_term_binder f c e = function | B.Abst (_, _, w) -> let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in @@ -64,49 +66,49 @@ let rec count_term_binder f c e = function f c and count_term f c e = function - | B.Sort _ -> + | B.Sort _ -> f {c with tsorts = succ c.tsorts; nodes = succ c.nodes} - | B.LRef (_, i) -> + | B.LRef (_, i) -> begin match B.get e i with - | _, _, _, B.Abst _ - | _, _, _, B.Void -> + | _, _, _, _, B.Abst _ + | _, _, _, _, B.Void -> f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes} - | _, _, _, B.Abbr _ -> + | _, _, _, _, B.Abbr _ -> f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes} end - | B.GRef (_, u) -> + | 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 e t in count_term f c e v - | B.Appl (_, _, v, t) -> + | 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 = count_term f c (B.push e B.empty a b) t in + | B.Bind (y, b, t) -> + let f c = count_term f c (B.push e B.empty E.empty_node y b) t in count_term_binder f c e b let count_entity f c = function - | _, _, u, E.Abst w -> + | _, _, u, E.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 w - | _, _, _, E.Abbr v -> + | _, _, _, E.Abbr (_, v) -> let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in count_term f c B.empty v - | _, _, _, E.Void -> assert false + | _, _, _, E.Void -> assert false let print_counters f c = let terms = - c.tsorts + c.tgrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts + + c.tsorts + c.tlrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts + c.tabbrs in let items = c.eabsts + c.eabbrs in @@ -127,6 +129,8 @@ let print_counters f c = L.warn level (KP.sprintf " + Abbreviation nodes: %7u" nodes); f () +END + (* lenv/term pretty printing ************************************************) let name err och a = @@ -143,46 +147,46 @@ let pp_level st och n = KP.fprintf och "%s" (N.to_string st n) let rec pp_term st e och = function - | B.Sort (_, h) -> - let err _ = KP.fprintf och "*%u" h in + | B.Sort k -> + let err _ = KP.fprintf och "*%u" k in let f s = KP.fprintf och "%s" s in - H.string_of_sort err f h + H.string_of_sort err f k | 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 - KP.fprintf och "%a" (name err) a + let _, _, _, y, b = B.get e i in + KP.fprintf och "%a" (name err) y | B.GRef (_, s) -> let u = U.string_of_uri s in KP.fprintf och "$%s" (if !G.short then KF.basename u else u) - | B.Cast (_, u, t) -> + | B.Cast (u, t) -> KP.fprintf och "<%a>.%a" (pp_term st e) u (pp_term st e) t - | B.Appl (_, _, v, 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 (r, n, w), t) -> - let a = R.alpha B.mem e a in - let ee = B.push e B.empty a (B.abst r n w) in - KP.fprintf och "%a%a[%a:%a].%a" (pp_level st) n pp_reduced r (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 + | B.Bind (y, B.Abst (r, n, w), t) -> + let y = R.alpha B.mem e y in + let ee = B.push e B.empty E.empty_node y (B.abst r n w) in + KP.fprintf och "%a%a[%a:%a].%a" (pp_level st) n pp_reduced r (name C.start) y (pp_term st e) w (pp_term st ee) t + | B.Bind (y, B.Abbr v, t) -> + let y = R.alpha B.mem e y in + let ee = B.push e B.empty E.empty_node y (B.abbr v) in + KP.fprintf och "[%a=%a].%a" (name C.start) y (pp_term st e) v (pp_term st ee) t + | B.Bind (y, B.Void, t) -> + let y = R.alpha B.mem e y in + let ee = B.push e B.empty E.empty_node y B.Void in + KP.fprintf och "[%a].%a" (name C.start) y (pp_term st ee) t let pp_lenv st och e = - 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 + let pp_entry f c a y b x = + let y = R.alpha B.mem e y in + let x = B.push x c a y b in match b with | B.Abst (_, _, w) -> - KP.fprintf och "[%a : %a] " (name C.start) a (pp_term st c) w; f x + KP.fprintf och "[%a : %a] " (name C.start) y (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 + KP.fprintf och "[%a = %a] " (name C.start) y (pp_term st c) v; f x | B.Void -> - KP.fprintf och "[%a]" (name C.start) a; f x + KP.fprintf och "[%a]" (name C.start) y; f x in if e = B.empty then KP.fprintf och "%s" "empty" else B.fold_right ignore pp_entry e B.empty @@ -191,7 +195,11 @@ let specs = { L.pp_term = pp_term; L.pp_lenv = pp_lenv } +IFDEF OBJECTS THEN + (* term xml printing ********************************************************) let export_term st = BD.crg_of_brg (XD.export_term st) + +END