From a0c8e5f59273c09542a1b8184dd1577d8f4240d7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 28 Jun 2015 18:47:24 +0000 Subject: [PATCH] new semantics of the -g option completed --- helm/software/helena/Makefile | 24 ++++----- helm/software/helena/src/basic_rg/brgLP.ml | 50 +++++++++---------- .../helena/src/basic_rg/brgReduction.ml | 11 ++-- helm/software/helena/src/toplevel/top.ml | 6 +-- helm/software/helena/src/xml/xmlCrg.ml | 12 ++--- helm/software/helena/src/xml/xmlLibrary.ml | 7 ++- helm/software/helena/src/xml/xmlLibrary.mli | 2 + 7 files changed, 57 insertions(+), 55 deletions(-) diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile index 991d490f0..f4b0075ba 100644 --- a/helm/software/helena/Makefile +++ b/helm/software/helena/Makefile @@ -47,8 +47,8 @@ PREAMBLE_V = coq/grundlagen.template PREAMBLE_LP = lp/lp.template test-si-fast: $(MAIN).opt etc - @echo " HELENA -q -u -x -1 $(INPUTFAST)" - $(H)./$(MAIN).opt -T 1 -q -u -x -1 $(O) $(INPUTFAST) > etc/log.txt + @echo " HELENA -q -u -x -y -1 $(INPUTFAST)" + $(H)./$(MAIN).opt -T 1 -q -u -x -y -1 $(O) $(INPUTFAST) > etc/log.txt test-si: $(MAIN).opt etc @echo " HELENA -d -l -u -0 $(INPUT)" @@ -56,7 +56,7 @@ test-si: $(MAIN).opt etc test2: $(MAIN).opt etc @echo " HELENA -T 2 -l $(INPUT)" - $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -T 2 -l $(O) $(INPUT) > etc/log.txt + $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -T 2 -l -q -1 $(O) $(INPUT) > etc/log.txt test3: $(MAIN).opt etc @echo " HELENA -T 3 -l $(INPUT)" @@ -67,20 +67,20 @@ test6: $(MAIN).opt etc $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -T 6 -l $(O) $(INPUT) > etc/log.txt xml-si: $(MAIN).opt etc - @echo " HELENA -l -o -s 1 -u $(INPUT)" - $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 1 -u $(O) $(INPUT) > etc/log.txt + @echo " HELENA -l -o -s 1 -u -y $(INPUT)" + $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 1 -u -y $(O) $(INPUT) > etc/log.txt xml-si-v3: $(MAIN).opt etc - @echo " HELENA -l -o -s 2 -u $(INPUT)" - $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 2 -u $(O) $(INPUT) > etc/log.txt + @echo " HELENA -l -o -s 2 -u -y $(INPUT)" + $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 2 -u -y $(O) $(INPUT) > etc/log.txt xml: $(MAIN).opt etc - @echo " HELENA -l -o -s 1 $(INPUT)" - $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 1 $(O) $(INPUT) > etc/log.txt + @echo " HELENA -l -o -s 1 -y $(INPUT)" + $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 1 -y $(O) $(INPUT) > etc/log.txt xml-v3: $(MAIN).opt etc @echo " HELENA -l -o -s 2 $(INPUT)" - $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 2 $(O) $(INPUT) > etc/log.txt + $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 2 -y $(O) $(INPUT) > etc/log.txt export-coq coq/$(V): $(MAIN).opt etc @echo " HELENA -l -m V8 -u $(INPUT)" @@ -109,13 +109,13 @@ export-tj3 lp/$(TJ3): $(MAIN).opt etc profile-fast: $(MAIN).opt etc @echo " HELENA -q -u -x $(INPUTFAST) (31 TIMES)" $(H)rm -f etc/log.txt - $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -q -u -x $(O) $(INPUTFAST) >> etc/log.txt; done + $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -q -u -x -1 $(O) $(INPUTFAST) >> etc/log.txt; done $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt profile: $(MAIN).opt etc @echo " HELENA -l -u $(INPUT) (31 TIMES)" $(H)rm -f etc/log.txt - $(H)for _ in `seq 31`; do ./$(MAIN).opt -T 1 -l -u $(O) $(INPUT) >> etc/log.txt; done + $(H)for _ in `seq 31`; do ./$(MAIN).opt -T 1 -l -q -u -1 $(O) $(INPUT) >> etc/log.txt; done $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt profile-coq: $(MAIN).opt etc diff --git a/helm/software/helena/src/basic_rg/brgLP.ml b/helm/software/helena/src/basic_rg/brgLP.ml index d4ed3c9dd..0eb193b7d 100644 --- a/helm/software/helena/src/basic_rg/brgLP.ml +++ b/helm/software/helena/src/basic_rg/brgLP.ml @@ -113,15 +113,15 @@ let rec out_term st e och = function (* elpi variant 1 ***********************************************************) -let output_entity_lp1 och st (_, na, s, b) = +let output_entity_lp1 och st (_, na, u, b) = if na.E.n_apix <= !G.last then begin match b with - | E.Abbr t -> - KP.fprintf och "(gdef+1 c+%u %a\n %a\\\n" na.E.n_apix (out_term st B.empty) t out_uri s; - uris := (true, s) :: !uris; !ok - | E.Abst u -> - KP.fprintf och "(gdec+1 c+%u %a\n%a\\\n" na.E.n_apix (out_term st B.empty) u out_uri s; - uris := (false, s) :: !uris; !ok + | E.Abbr v -> + KP.fprintf och "(gdef+1 c+%u %a\n %a\\\n" na.E.n_apix (out_term st B.empty) v out_uri u; + uris := (true, u) :: !uris; !ok + | E.Abst w -> + KP.fprintf och "(gdec+1 c+%u %a\n%a\\\n" na.E.n_apix (out_term st B.empty) w out_uri u; + uris := (false, u) :: !uris; !ok | E.Void -> C.err () end else !ok @@ -134,17 +134,17 @@ let close_out_lp1 och () = (* elpi variant 2 ***********************************************************) -let output_entity_lp2 och st (_, na, s, b) = +let output_entity_lp2 och st (_, na, u, b) = if na.E.n_apix <= !G.last then begin match b with - | E.Abbr t -> + | E.Abbr v -> KP.fprintf och "g+line %a c+%u\n %a\n.\n\n" - out_uri s na.E.n_apix (out_term st B.empty) t; - uris := (true, s) :: !uris; !ok - | E.Abst u -> + out_uri u na.E.n_apix (out_term st B.empty) v; + uris := (true, u) :: !uris; !ok + | E.Abst w -> KP.fprintf och "g+line %a c+%u\n %a\n.\n\n" - out_uri s na.E.n_apix (out_term st B.empty) u; - uris := (false, s) :: !uris; !ok + out_uri u na.E.n_apix (out_term st B.empty) w; + uris := (false, u) :: !uris; !ok | E.Void -> C.err () end else !ok @@ -160,7 +160,7 @@ let close_out_lp2 och () = out_clause och "tv+c C T :- tv+ T." end; out_clause och "main :- grundlagen."; - out_clause och "grundlagen :- gv+ "; + out_clause och "grundlagen :- gv+"; List.iter aux_name (List.rev !uris); KP.fprintf och "%s" "gtop"; List.iter aux_sep !uris; @@ -169,25 +169,25 @@ let close_out_lp2 och () = (* teyjus variant 2 *************************************************) -let output_entity_tj2 och st (_, na, s, b) = +let output_entity_tj2 och st (_, na, u, b) = if na.E.n_apix <= !G.last then begin out_comment och (KP.sprintf "constant %u" na.E.n_apix); match b with - | E.Abbr t -> + | E.Abbr v -> KP.fprintf och "g+line %a %u\n %a\n.\n\n" - out_uri s (top_age - na.E.n_apix) (out_term st B.empty) t; - uris := (true, s) :: !uris; !ok - | E.Abst u -> + out_uri u (top_age - na.E.n_apix) (out_term st B.empty) v; + uris := (true, u) :: !uris; !ok + | E.Abst w -> KP.fprintf och "g+line %a %u\n %a\n.\n\n" - out_uri s (top_age - na.E.n_apix) (out_term st B.empty) u; - uris := (false, s) :: !uris; !ok + out_uri u (top_age - na.E.n_apix) (out_term st B.empty) w; + uris := (false, u) :: !uris; !ok | E.Void -> C.err () end else !ok let close_out_tj2 och () = - let aux_name (b, s) = + let aux_name (b, u) = let gde = if b then "gdef+2" else "gdec+2" in - KP.fprintf och "(%s %a\n" gde out_uri s + KP.fprintf och "(%s %a\n" gde out_uri u in let aux_sep _ = KP.fprintf och "%s" ")" in if !G.first > 0 then begin @@ -196,7 +196,7 @@ let close_out_tj2 och () = out_clause och "tv+c C T :- tv+ T." end; out_clause och "main :- grundlagen."; - out_clause och "grundlagen :- gv+ "; + out_clause och "grundlagen :- gv+"; List.iter aux_name (List.rev !uris); KP.fprintf och "%s" "gtop"; List.iter aux_sep !uris; diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml index f20335193..35f5f0222 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.ml +++ b/helm/software/helena/src/basic_rg/brgReduction.ml @@ -147,9 +147,6 @@ let rec step st m r = | [] -> m, B.Bind (a, B.Abst (true, n, w), t), None | (c, v) :: s -> -(* - if !G.cc && not (N.assert_not_zero st n) then assert false; -*) if !G.summary then O.add ~beta:1 ~theta:(List.length s) (); let v = B.Cast (E.empty_node, w, v) in let e = B.push m.e c a (B.abbr v) in @@ -190,17 +187,17 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = if U.eq u1 u2 && assert_iterations m1 m2 then ac_stacks st m1 m2 else false | B.GRef ({E.n_apix = e1}, u1), Some v1, B.GRef ({E.n_apix = e2}, u2), Some v2 -> - if e1 < e2 then begin + if U.eq u1 u2 && assert_iterations m1 m2 && ac_stacks st m1 m2 then true + else if e1 < e2 then begin if !G.summary then O.add ~gdelta:1 (); ac_nfs st (m1, t1, r1) (step st m2 v2) end else if e2 < e1 then begin if !G.summary then O.add ~gdelta:1 (); ac_nfs st (step st m1 v1) (m2, t2, r2) - end else if U.eq u1 u2 && assert_iterations m1 m2 && ac_stacks st m1 m2 then true - else begin + end else begin if !G.summary then O.add ~gdelta:2 (); ac st m1 v1 m2 v2 - end + end | _, _, B.GRef _, Some v2 -> if !G.summary then O.add ~gdelta:1 (); ac_nfs st (m1, t1, r1) (step st m2 v2) diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml index 3e7f8aa91..641871603 100644 --- a/helm/software/helena/src/toplevel/top.ml +++ b/helm/software/helena/src/toplevel/top.ml @@ -381,7 +381,7 @@ let main = let help_b = " [begin] Begin trace at this global constant (default: first)" in let help_d = " [data] Show summary information (requires trace >= 2)" in let help_e = " [end] End trace at this global constant (default: last)" in - let help_g = " [global] Always expand global definitions (default: false)" in + let help_g = " [global] Disable age-driven expansion of global definitions (default: enable)" in let help_h = " [hierarchy] Set type hierarchy (default: \"Z1\")" in let help_i = " [indexes] Show local references by index" in let help_k = " [kernel] Set kernel version (default: \"V3\")" in @@ -390,11 +390,11 @@ let main = let help_n = " [names] Show short constants (default: qualified constants)" in let help_o = " [objects] Export kernel entities (XML)" in let help_p = " [preamble] Set preamble to this file (default: empty)" in - let help_q = " [quote] Disable quotation of identifiers (default: false)" in + let help_q = " [quote] Disable quotation of identifiers (default: enable)" in let help_r = " [root] Set initial segment of URI hierarchy (default: empty)" in let help_s = " [stage] Set translation stage (see above)" in let help_t = " [type] Type check (default: validate)" in - let help_u = " [upsilon] Activate type comparison by sort inclusion (default: false)" in + let help_u = " [upsilon] Activate type comparison by sort inclusion (default: deactivate)" in let help_x = " [extended] Use extended applications (Automath)" in let help_y = " [infinity] Use ∞-abstractions in contexts" in let help_0 = " [zero] Preprocess source (Automath)" in diff --git a/helm/software/helena/src/xml/xmlCrg.ml b/helm/software/helena/src/xml/xmlCrg.ml index b04f5f6e1..b2029149b 100644 --- a/helm/software/helena/src/xml/xmlCrg.ml +++ b/helm/software/helena/src/xml/xmlCrg.ml @@ -37,13 +37,13 @@ let lenv_iter map_bind map_appl map_proj st e lenv out tab = ignore (aux lenv) let rec exp_term st e t out tab = match t with - | D.TSort (a, l) -> + | D.TSort (a, h) -> let a = let err _ = a in let f s = {a with E.n_name = Some (s, true)} in - H.string_of_sort err f l + H.string_of_sort err f h in - let attrs = [XL.position l; XL.name a] in + let attrs = [XL.position h; XL.name a] in XL.tag XL.sort attrs out tab | D.TLRef (a, i) -> let a = @@ -51,11 +51,11 @@ let rec exp_term st e t out tab = match t with let f n r = {a with E.n_name = Some (n, r)} in D.get_name err f i e in - let attrs = [XL.position i; XL.name a ] in + let attrs = [XL.depth i; XL.name a] in XL.tag XL.lref attrs out tab | D.TGRef (a, n) -> let a = {a with E.n_name = Some (U.name_of_uri n, true)} in - let attrs = [XL.uri n; XL.name a ] in + let attrs = [XL.uri n; XL.name a] in XL.tag XL.gref attrs out tab | D.TCast (a, u, t) -> let attrs = [] in @@ -81,7 +81,7 @@ and exp_appl st e a x v out tab = and exp_bind st e a b out tab = match b with | D.Abst (_, n, w) -> - let attrs = XL.layer st n :: XL.name a :: XL.main a in + let attrs = [XL.layer st n; XL.name a] in XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab | D.Abbr v -> let attrs = [XL.name a] in diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml index dcc18c94b..002688b31 100644 --- a/helm/software/helena/src/xml/xmlLibrary.ml +++ b/helm/software/helena/src/xml/xmlLibrary.ml @@ -88,6 +88,9 @@ let void = "Void" let position i = "position", string_of_int i +let depth i = + "depth", string_of_int i + let uri u = "uri", U.string_of_uri u @@ -101,13 +104,13 @@ let layer st n = let main a = let sort, degr = a.E.n_main in - ["main-sort", string_of_int sort; + ["main-position", string_of_int sort; "main-degree", string_of_int degr; ] let side a = let sort, degr = a.E.n_side in - ["side-sort", string_of_int sort; + ["side-position", string_of_int sort; "side-degree", string_of_int degr; ] diff --git a/helm/software/helena/src/xml/xmlLibrary.mli b/helm/software/helena/src/xml/xmlLibrary.mli index e49d0e8d8..0dbfb54aa 100644 --- a/helm/software/helena/src/xml/xmlLibrary.mli +++ b/helm/software/helena/src/xml/xmlLibrary.mli @@ -39,6 +39,8 @@ val void: string val position: int -> attr +val depth: int -> attr + val uri: Entity.uri -> attr val layer: Layer.status -> Layer.layer -> attr -- 2.39.2