From e7f64fe2cc67f3514131c8831f87311ff600d005 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 31 Oct 2010 22:52:29 +0000 Subject: [PATCH] the old intermediate language (meta) is now obsolete --- helm/software/lambda-delta/.depend.opt | 26 ++-- helm/software/lambda-delta/Makefile | 4 +- .../lambda-delta/src/complete_rg/crg.ml | 27 +++- .../lambda-delta/src/complete_rg/crgOutput.ml | 126 +++++++++++++++++- .../src/complete_rg/crgOutput.mli | 8 ++ .../lambda-delta/src/complete_rg/crgTxt.ml | 6 +- .../lambda-delta/src/toplevel/metaOutput.ml | 2 +- .../software/lambda-delta/src/toplevel/top.ml | 94 +++++++------ helm/software/lambda-delta/src/xml/xmlCrg.ml | 6 +- 9 files changed, 226 insertions(+), 73 deletions(-) diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 94d36ea3f..f5f9bcdcf 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -118,12 +118,12 @@ src/basic_ag/bagUntrusted.cmx: src/lib/log.cmx src/common/entity.cmx \ src/complete_rg/crg.cmo: src/common/level.cmi src/common/entity.cmx src/complete_rg/crg.cmx: src/common/level.cmx src/common/entity.cmx src/complete_rg/crgOutput.cmi: src/complete_rg/crg.cmx -src/complete_rg/crgOutput.cmo: src/common/level.cmi src/common/hierarchy.cmi \ - src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/complete_rg/crgOutput.cmi -src/complete_rg/crgOutput.cmx: src/common/level.cmx src/common/hierarchy.cmx \ - src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/complete_rg/crgOutput.cmi +src/complete_rg/crgOutput.cmo: src/lib/log.cmi src/common/level.cmi \ + src/common/hierarchy.cmi src/common/entity.cmx src/complete_rg/crg.cmx \ + src/lib/cps.cmx src/complete_rg/crgOutput.cmi +src/complete_rg/crgOutput.cmx: src/lib/log.cmx src/common/level.cmx \ + src/common/hierarchy.cmx src/common/entity.cmx src/complete_rg/crg.cmx \ + src/lib/cps.cmx src/complete_rg/crgOutput.cmi src/complete_rg/crgTxt.cmi: src/text/txt.cmx src/complete_rg/crg.cmx src/complete_rg/crgTxt.cmo: src/text/txtTxt.cmi src/text/txt.cmx \ src/common/options.cmx src/common/hierarchy.cmi src/common/entity.cmx \ @@ -249,9 +249,10 @@ src/toplevel/top.cmo: src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \ src/toplevel/metaBrg.cmi src/toplevel/metaBag.cmi \ src/toplevel/metaAut.cmi src/toplevel/meta.cmx src/lib/log.cmi \ src/common/hierarchy.cmi src/common/entity.cmx src/complete_rg/crgTxt.cmi \ - src/complete_rg/crgAut.cmi src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/basic_rg/brgUntrusted.cmi src/basic_rg/brgReduction.cmi \ - src/basic_rg/brgOutput.cmi src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \ + src/complete_rg/crgOutput.cmi src/complete_rg/crgAut.cmi \ + src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brgUntrusted.cmi \ + src/basic_rg/brgReduction.cmi src/basic_rg/brgOutput.cmi \ + src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \ src/basic_ag/bagUntrusted.cmi src/basic_ag/bagType.cmi \ src/basic_ag/bagOutput.cmi src/basic_ag/bag.cmx \ src/automath/autProcess.cmi src/automath/autParser.cmi \ @@ -263,9 +264,10 @@ src/toplevel/top.cmx: src/xml/xmlLibrary.cmx src/xml/xmlCrg.cmx \ src/toplevel/metaBrg.cmx src/toplevel/metaBag.cmx \ src/toplevel/metaAut.cmx src/toplevel/meta.cmx src/lib/log.cmx \ src/common/hierarchy.cmx src/common/entity.cmx src/complete_rg/crgTxt.cmx \ - src/complete_rg/crgAut.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ - src/basic_rg/brgUntrusted.cmx src/basic_rg/brgReduction.cmx \ - src/basic_rg/brgOutput.cmx src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \ + src/complete_rg/crgOutput.cmx src/complete_rg/crgAut.cmx \ + src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brgUntrusted.cmx \ + src/basic_rg/brgReduction.cmx src/basic_rg/brgOutput.cmx \ + src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \ src/basic_ag/bagUntrusted.cmx src/basic_ag/bagType.cmx \ src/basic_ag/bagOutput.cmx src/basic_ag/bag.cmx \ src/automath/autProcess.cmx src/automath/autParser.cmx \ diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index c5992e90a..03f1f1704 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -97,8 +97,8 @@ test: $(MAIN).opt etc $(H)./$(MAIN).opt -o -p -S 3 $(O) $(INPUT) > etc/log.txt test-si-old: $(MAIN).opt etc - @echo " HELENA -o -p -u $(INPUT)" - $(H)./$(MAIN).opt -o -p -u -S 3 $(O) $(INPUT) > etc/log.txt + @echo " HELENA -o -p -u -c $(INPUT)" + $(H)./$(MAIN).opt -o -p -u -c -S 3 $(O) $(INPUT) > etc/log.txt test-si-fast-old: $(MAIN).opt etc @echo " HELENA -o -u -q $(INPUT)" diff --git a/helm/software/lambda-delta/src/complete_rg/crg.ml b/helm/software/lambda-delta/src/complete_rg/crg.ml index 9020048af..07305e9c1 100644 --- a/helm/software/lambda-delta/src/complete_rg/crg.ml +++ b/helm/software/lambda-delta/src/complete_rg/crg.ml @@ -45,14 +45,20 @@ let push_bind f lenv a b = f (EBind (lenv, a, b)) let push_proj f lenv a e = f (EProj (lenv, a, e)) -let push2 err f lenv attr ?t () = match lenv, t with - | EBind (e, a, Abst (n, ws)), Some t -> +let push2 err f lenv ?attr ?t () = match lenv, attr, t with + | EBind (e, a, Abst (n, ws)), Some attr, Some t -> f (EBind (e, (attr :: a), Abst (n, t :: ws))) - | EBind (e, a, Abbr vs), Some t -> + | EBind (e, a, Abst (n, ws)), None, Some t -> + f (EBind (e, a, Abst (n, t :: ws))) + | EBind (e, a, Abbr vs), Some attr, Some t -> f (EBind (e, (attr :: a), Abbr (t :: vs))) - | EBind (e, a, Void n), None -> + | EBind (e, a, Abbr vs), None, Some t -> + f (EBind (e, a, Abbr (t :: vs))) + | EBind (e, a, Void n), Some attr, None -> f (EBind (e, (attr :: a), Void (succ n))) - | _ -> err () + | EBind (e, a, Void n), None, None -> + f (EBind (e, a, Void (succ n))) + | _ -> err () (* this id not tail recursive *) let resolve_lref err f id lenv = @@ -101,3 +107,14 @@ let rec names_of_lenv ns = function | ESort -> ns | EBind (tl, a, _) -> names_of_lenv (E.rev_append_names ns a) tl | EProj (tl, _, e) -> names_of_lenv (names_of_lenv ns e) tl + +let rec get i = function + | ESort -> ESort, [], Void 0 + | EBind (e, _, Abst (_, [])) + | EBind (e, _, Abbr []) + | EBind (e, _, Void 0) -> get i e + | EBind (e, a, b) when i = 0 -> e, a, b + | EBind (e, _, _) -> get (pred i) e + | EProj _ -> assert false (* TODO *) + +let get e i = get i e diff --git a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml index 0b3964258..c8d3bad88 100644 --- a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml +++ b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml @@ -12,12 +12,134 @@ module P = Printf module U = NUri module C = Cps +module L = Log module H = Hierarchy 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 @@ -58,5 +180,3 @@ 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 - -(****************************************************************************) diff --git a/helm/software/lambda-delta/src/complete_rg/crgOutput.mli b/helm/software/lambda-delta/src/complete_rg/crgOutput.mli index d804937f8..5740b6ba8 100644 --- a/helm/software/lambda-delta/src/complete_rg/crgOutput.mli +++ b/helm/software/lambda-delta/src/complete_rg/crgOutput.mli @@ -9,4 +9,12 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +type counters + +val initial_counters: counters + +val count_entity: (counters -> 'a) -> counters -> Crg.entity -> 'a + +val print_counters: (unit -> 'a) -> counters -> 'a + val pp_term: (string -> unit) -> Crg.term -> unit diff --git a/helm/software/lambda-delta/src/complete_rg/crgTxt.ml b/helm/software/lambda-delta/src/complete_rg/crgTxt.ml index 141b467bb..980b74a08 100644 --- a/helm/software/lambda-delta/src/complete_rg/crgTxt.ml +++ b/helm/software/lambda-delta/src/complete_rg/crgTxt.ml @@ -73,16 +73,16 @@ let rec xlate_term f st lenv = function let abst_map (lenv, a, wws) (id, r, w) = let attr = name_of_id ~r id in let ww = xlate_term C.start st lenv w in - D.push2 C.err C.start lenv attr ~t:ww (), attr :: a, ww :: wws + D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws in let abbr_map (lenv, a, wws) (id, w) = let attr = name_of_id id in let ww = xlate_term C.start st lenv w in - D.push2 C.err C.start lenv attr ~t:ww (), attr :: a, ww :: wws + D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws in let void_map (lenv, a, n) id = let attr = name_of_id id in - D.push2 C.err C.start lenv attr (), attr :: a, succ n + D.push2 C.err C.start lenv ~attr (), attr :: a, succ n in let lenv, aa, bb = match b with | T.Abst xws -> diff --git a/helm/software/lambda-delta/src/toplevel/metaOutput.ml b/helm/software/lambda-delta/src/toplevel/metaOutput.ml index 0f25e13e5..73ff70e59 100644 --- a/helm/software/lambda-delta/src/toplevel/metaOutput.ml +++ b/helm/software/lambda-delta/src/toplevel/metaOutput.ml @@ -90,7 +90,7 @@ let print_counters f c = let pars = c.pabsts + c.pappls in let entries = c.eabsts + c.eabbrs in let nodes = c.nodes + c.xnodes in - L.warn (P.sprintf " Intermediate representation summary"); + L.warn (P.sprintf " Intermediate representation summary (meta)"); L.warn (P.sprintf " Total entries: %7u" entries); L.warn (P.sprintf " Declaration items: %7u" c.eabsts); L.warn (P.sprintf " Definition items: %7u" c.eabbrs); diff --git a/helm/software/lambda-delta/src/toplevel/top.ml b/helm/software/lambda-delta/src/toplevel/top.ml index 4a1446734..579f5e658 100644 --- a/helm/software/lambda-delta/src/toplevel/top.ml +++ b/helm/software/lambda-delta/src/toplevel/top.ml @@ -20,34 +20,37 @@ module H = Hierarchy module O = Output module E = Entity module S = Status -module XL = XmlLibrary -module XD = XmlCrg +module TD = CrgTxt module AA = AutProcess module AO = AutOutput -module TD = CrgTxt module AD = CrgAut -module MA = MetaAut -module MO = MetaOutput -module MB = MetaBrg +module DO = CrgOutput +module XL = XmlLibrary +module XD = XmlCrg module BD = BrgCrg module BO = BrgOutput module BR = BrgReduction module BU = BrgUntrusted -module MZ = MetaBag module ZO = BagOutput module ZT = BagType module ZU = BagUntrusted +module MA = MetaAut +module MO = MetaOutput +module MB = MetaBrg +module MZ = MetaBag + type status = { - ast : AA.status; - dst : AD.status; - mst : MA.status; - tst : TD.status; - ac : AO.counters; - mc : MO.counters; - brgc: BO.counters; - bagc: ZO.counters; - kst : S.status + kst: S.status; + tst: TD.status; + pst: AA.status; + ast: AD.status; + ac : AO.counters; + dc : DO.counters; + bc : BO.counters; + zc : ZO.counters; + mst: MA.status; + mc : MO.counters; } let flush_all () = L.flush 0; L.flush_err () @@ -59,22 +62,23 @@ let brg_error s msg = L.error BR.specs (L.Warn s :: L.Loc :: msg); flush_all () let initial_status () = { - ac = AO.initial_counters; - mc = MO.initial_counters; - brgc = BO.initial_counters; - bagc = ZO.initial_counters; - mst = MA.initial_status (); - dst = AD.initial_status (); - tst = TD.initial_status (); - ast = AA.initial_status (); - kst = S.initial_status () + kst = S.initial_status (); + tst = TD.initial_status (); + pst = AA.initial_status (); + ast = AD.initial_status (); + ac = AO.initial_counters; + dc = DO.initial_counters; + bc = BO.initial_counters; + zc = ZO.initial_counters; + mst = MA.initial_status (); + mc = MO.initial_counters; } let refresh_status st = {st with - mst = MA.refresh_status st.mst; - dst = AD.refresh_status st.dst; + kst = S.refresh_status st.kst; tst = TD.refresh_status st.tst; - kst = S.refresh_status st.kst + ast = AD.refresh_status st.ast; + mst = MA.refresh_status st.mst; } (* kernel related ***********************************************************) @@ -85,9 +89,9 @@ type kernel_entity = BrgEntity of Brg.entity | MetaEntity of Meta.entity let print_counters st = function - | G.Brg -> BO.print_counters C.start st.brgc - | G.Bag -> ZO.print_counters C.start st.bagc - | G.Crg -> () + | G.Crg -> DO.print_counters C.start st.dc + | G.Brg -> BO.print_counters C.start st.bc + | G.Bag -> ZO.print_counters C.start st.zc let xlate_entity entity = match !G.kernel, entity with | G.Brg, CrgEntity e -> @@ -106,16 +110,16 @@ let pp_progress e = E.mark err f a in match e with - | CrgEntity e -> E.common f e - | BrgEntity e -> E.common f e - | BagEntity e -> E.common f e + | CrgEntity e -> E.common f e + | BrgEntity e -> E.common f e + | BagEntity e -> E.common f e | MetaEntity e -> E.common f e let count_entity st = function + | BrgEntity e -> {st with bc = BO.count_entity C.start st.bc e} + | BagEntity e -> {st with zc = ZO.count_entity C.start st.zc e} + | CrgEntity e -> {st with dc = DO.count_entity C.start st.dc e} | MetaEntity e -> {st with mc = MO.count_entity C.start st.mc e} - | BrgEntity e -> {st with brgc = BO.count_entity C.start st.brgc e} - | BagEntity e -> {st with bagc = ZO.count_entity C.start st.bagc e} - | _ -> st let export_entity = function | CrgEntity e -> XL.export_entity XD.export_term e @@ -194,8 +198,8 @@ let entity_of_input lexbuf i = match i, !parbuf with let process_input f st = function | AutEntity e -> - let f ast e = f {st with ast = ast} (AutEntity e) in - AA.process_command f st.ast e + let f pst e = f {st with pst = pst} (AutEntity e) in + AA.process_command f st.pst e | xe -> f st xe let count_input st = function @@ -233,9 +237,9 @@ let process_0 st entity = let h mst e = process_1 {st with mst = mst} (MetaEntity e) in MA.meta_of_aut frr h st.mst e | AutEntity e, false -> - let err dst = {st with dst = dst} in - let g dst e = process_1 {st with dst = dst} (CrgEntity e) in - AD.crg_of_aut err g st.dst e + let err ast = {st with ast = ast} in + let g ast e = process_1 {st with ast = ast} (CrgEntity e) in + AD.crg_of_aut err g st.ast e | TxtEntity e, _ -> let crr tst = {st with tst = tst} in let d tst e = process_1 {st with tst = tst} (CrgEntity e) in @@ -314,8 +318,10 @@ try if !L.level > 0 then Y.utime_stamp "processed"; if !L.level > 2 then begin AO.print_counters C.start !st.ac; - if !preprocess then AO.print_process_counters C.start !st.ast; - if !stage > 0 then MO.print_counters C.start !st.mc; + if !preprocess then AO.print_process_counters C.start !st.pst; + if !stage > 0 then + if !old then MO.print_counters C.start !st.mc + else print_counters !st G.Crg; if !stage > 1 then print_counters !st !G.kernel; if !stage > 2 then O.print_reductions () end diff --git a/helm/software/lambda-delta/src/xml/xmlCrg.ml b/helm/software/lambda-delta/src/xml/xmlCrg.ml index 3eea8cd87..45e33178a 100644 --- a/helm/software/lambda-delta/src/xml/xmlCrg.ml +++ b/helm/software/lambda-delta/src/xml/xmlCrg.ml @@ -32,7 +32,7 @@ let list_rev_iter map e ns l out tab = pp_lenv print_string e; print_string " |- "; pp_term print_string hd; print_newline (); *) - map e hd out tab; f (D.push2 C.err C.start e n ~t:hd ()) + map e hd out tab; f (D.push2 C.err C.start e ~attr:n ~t:hd ()) in aux err f e (ns, tl) | _ -> err () @@ -91,11 +91,11 @@ and exp_bind e a b out tab = let a, ns = Y.get_names f a in match b with | D.Abst (n, ws) -> - let e = D.push_bind C.start e a (D.Abst (n, ws)) in + let e = D.push_bind C.start e a (D.Abst (n, [])) in let attrs = [XL.level n; XL.name ns; XL.mark a; XL.arity ws] in XL.tag XL.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab | D.Abbr vs -> - let e = D.push_bind C.start e a (D.Abbr vs) in + let e = D.push_bind C.start e a (D.Abbr []) in let attrs = [XL.name ns; XL.mark a; XL.arity vs] in XL.tag XL.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab | D.Void n -> -- 2.39.2