X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fcomplete_rg%2FcrgOutput.ml;h=c8d3bad88ec4448ba8590f2ad993e6f6eccd8fde;hb=d145ea48ed0bdb9642ced01283231f3f13d476b8;hp=6da54cbc3dc9cb48dc870687369c147c69b0d87a;hpb=ab13cfa248f0ee58d239ceeddfb50ec49a6b5c6d;p=helm.git diff --git a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml index 6da54cbc3..c8d3bad88 100644 --- a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml +++ b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml @@ -12,20 +12,143 @@ module P = Printf module U = NUri module C = Cps +module L = Log module H = Hierarchy -module Y = Entity +module E = Entity +module N = Level module D = Crg -(****************************************************************************) +(* nodes count **************************************************************) + +type counters = { + eabsts: int; + eabbrs: int; + evoids: int; + tsorts: int; + tlrefs: int; + tgrefs: int; + tcasts: int; + tappls: int; + tabsts: int; + tabbrs: int; + tvoids: int; + uris : D.uri list; + nodes : int; + xnodes: int +} + +let initial_counters = { + 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 shift t = function + | D.ESort -> t + | D.EBind (e, a, b) -> shift (D.TBind (a, b, t)) e + | D.EProj (e, a, d) -> shift (D.TProj (a, d, t)) e + +let rec count_term f c e = function + | D.TSort _ -> + f {c with tsorts = succ c.tsorts; nodes = succ c.nodes} + | D.TLRef (_, i, j) -> + begin match D.get e i with + | _, _, D.Abbr vs when j < List.length vs -> + f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes} + | _ -> + f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes} + end + | D.TGRef (_, u) -> + let c = + if C.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} + | D.TCast (_, 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 + | D.TAppl (_, vs, t) -> + let c = {c with tappls = succ c.tappls; nodes = succ c.nodes} in + let f c = count_term f c e t in + C.list_fold_right f (map1 e) vs c + | D.TProj (a, d, t) -> + count_term f c e (shift t d) + | D.TBind (a, b, t) -> + let f c e = count_term f c e t in + count_binder f c e a b + +and count_binder f c e a = function + | D.Abst (n, ws) -> + let k = List.length ws in + let c = {c with tabsts = c.tabsts + k; nodes = c.nodes + k} in + let e = D.push_bind C.start e a (D.Abst (n, [])) in + let f (c, e) = f c e in + C.list_fold_right f map2 ws (c, e) + | D.Abbr vs -> + let k = List.length vs in + let c = {c with tabbrs = c.tabbrs + k; xnodes = c.xnodes + k} in + let e = D.push_bind C.start e a (D.Abbr []) in + let f (c, e) = f c e in + C.list_fold_right f map2 vs (c, e) + | D.Void k -> + let c = {c with tvoids = c.tvoids + k; xnodes = c.xnodes + k} in + let e = D.push_bind C.start e a (D.Void k) in + f c e + +and map1 e f t c = count_term f c e t + +and map2 f t (c, e) = + let f c e = f (c, e) in + let f c = D.push2 C.err (f c) e ~t () in + count_term f c e t + +let count_entity f c = function + | _, 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 D.ESort w + | _, _, E.Abbr v -> + let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in + count_term f c D.ESort v + | _, _, E.Void -> assert false + +let print_counters f c = + let terms = + c.tsorts + c.tgrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts + + c.tabbrs + in + let items = c.eabsts + c.eabbrs in + let nodes = c.nodes + c.xnodes in + L.warn (P.sprintf " Intermediate representation summary (crg)"); + 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 () + +(* term/environment pretty printer ******************************************) let pp_attrs out a = let map = function - | Y.Name (s, true) -> out (P.sprintf "%s;" s) - | Y.Name (s, false) -> out (P.sprintf "~%s;" s) - | Y.Apix i -> out (P.sprintf "+%i;" i) - | Y.Mark i -> out (P.sprintf "@%i;" i) - | Y.Meta s -> out (P.sprintf "\"%s\";" s) - | Y.Priv -> out (P.sprintf "%s;" "~") + | E.Name (s, true) -> out (P.sprintf "%s;" s) + | E.Name (s, false) -> out (P.sprintf "~%s;" s) + | E.Apix i -> out (P.sprintf "+%i;" i) + | E.Mark i -> out (P.sprintf "@%i;" i) + | E.Meta s -> out (P.sprintf "\"%s\";" s) + | E.Priv -> out (P.sprintf "%s;" "~") in List.iter map a @@ -47,13 +170,13 @@ and pp_terms bg eg out vs = out bg; aux vs; out (eg ^ ".") and pp_bind out = function - | D.Abst x -> pp_terms "[:" "]" out x - | D.Abbr x -> pp_terms "[=" "]" out x - | D.Void x -> out (P.sprintf "[%u]" x) + | D.Abst (n, x) when N.is_infinite n -> pp_terms "[:" "]" out x + | D.Abst (n, x) -> + pp_terms "[:" (P.sprintf "]^%s" (N.to_string n)) out x + | D.Abbr x -> pp_terms "[=" "]" out x + | D.Void x -> out (P.sprintf "[%u]" x) let rec pp_lenv out = function | D.ESort -> () | D.EProj (x, a, y) -> assert false | D.EBind (x, a, y) -> pp_lenv out x; pp_attrs out a; pp_bind out y - -(****************************************************************************)