From 9f8544610ba0245bde47f367de6716e1f256ab18 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 10 Jul 2009 21:36:41 +0000 Subject: [PATCH] - brgOutput: the nodes count is now implemented - brgReduction: the type annotation in the beta-reductum is useless - brgType: a never-occurring condition marked with assert false --- helm/software/lambda-delta/.depend.opt | 4 +- .../lambda-delta/basic_rg/brgOutput.ml | 95 ++++++++++++------- .../lambda-delta/basic_rg/brgReduction.ml | 2 +- .../software/lambda-delta/basic_rg/brgType.ml | 2 +- 4 files changed, 65 insertions(+), 38 deletions(-) diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index eb7f894e2..1f272e29e 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -35,9 +35,9 @@ basic_rg/brg.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx automath/aut.cmx basic_rg/brg.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx automath/aut.cmx basic_rg/brgOutput.cmi: lib/log.cmi basic_rg/brg.cmx basic_rg/brgOutput.cmo: lib/output.cmi lib/nUri.cmi lib/log.cmi \ - lib/hierarchy.cmi basic_rg/brg.cmx basic_rg/brgOutput.cmi + lib/hierarchy.cmi lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi basic_rg/brgOutput.cmx: lib/output.cmx lib/nUri.cmx lib/log.cmx \ - lib/hierarchy.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi + lib/hierarchy.cmx lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi basic_rg/brgEnvironment.cmi: lib/nUri.cmi basic_rg/brg.cmx basic_rg/brgEnvironment.cmo: lib/nUri.cmi lib/log.cmi basic_rg/brg.cmx \ basic_rg/brgEnvironment.cmi diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index 2d1fa96ae..aaa559be6 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -22,59 +22,83 @@ module B = Brg 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 : U.uri list; + nodes : int; + xnodes: int } 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 + 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 = function - | B.Sort _ -> - f {c with tsorts = succ c.tsorts} - | B.LRef _ -> - f {c with tlrefs = succ c.tlrefs} - | B.GRef _ -> +and count_term f c e = function + | B.Sort _ -> + f {c with tsorts = succ c.tsorts; nodes = succ c.nodes} + | B.LRef (_, i) -> + let f _ = function + | None + | Some (_, B.Abst _) -> + f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes} + | Some (_, B.Abbr _) + | Some (_, B.Void) -> + f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes} + in + B.get 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) -> let c = {c with tcasts = succ c.tcasts} in - let f c = count_term f c t in - count_term f c v + 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} 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 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 + | (_, _, B.Void) -> + let c = {c with evoids = succ c.evoids; xnodes = succ c.xnodes} in + f c let count_item f c = function | Some obj -> count_obj f c obj @@ -86,6 +110,7 @@ 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: %7u" items); L.warn (P.sprintf " Declaration items: %7u" c.eabsts); @@ -98,6 +123,8 @@ let print_counters f c = 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 *********************************************) diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml index 87d093d82..16dc395bb 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -107,7 +107,7 @@ let rec step f ?(delta=false) ?(rt=false) c m x = P.add ~beta:1 ~upsilon:(List.length tl) (); let f mc sc = step f ~delta ~rt c {c = mc; s = sc} t in let f mc = lift_stack (f mc) tl in - let f v = B.push f m.c a (B.Abbr (B.Cast ([], w, v))) in + let f v = B.push f m.c a (B.Abbr v (* (B.Cast ([], w, v)) *) ) in S.lift f h (0) v end | B.Bind (a, b, t) -> diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml index 4bf5882a4..85ecf995a 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -80,7 +80,7 @@ let rec b_type_of f g c x = let f xv = B.push (f xv) c a (B.Abbr xv) in let f xv vv = match xv with | B.Cast _ -> f xv - | _ -> f (B.Cast ([], vv, xv)) + | _ -> assert false (* f (B.Cast ([], vv, xv)) *) in type_of f g c v | B.Bind (a, B.Abst u, t) -> -- 2.39.2