From 9935a5bf5bdc98ad01a2b0234cf4e612a62c939f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 24 Dec 2014 17:03:22 +0000 Subject: [PATCH] - bugfix is refreshed state of AutCrg: now we return a fresh state - minor changes in the xml format - some refactoring --- helm/software/helena/.depend.opt | 36 +++++------ helm/software/helena/Makefile | 18 +++--- helm/software/helena/src/automath/autCrg.ml | 4 +- helm/software/helena/src/basic_ag/bag.ml | 8 +-- helm/software/helena/src/basic_ag/bagCrg.ml | 8 +-- .../software/helena/src/basic_ag/bagOutput.ml | 64 +++++++++---------- .../helena/src/basic_ag/bagReduction.ml | 12 ++-- helm/software/helena/src/common/Make | 2 +- helm/software/helena/src/common/layer.ml | 46 ++++++------- helm/software/helena/src/common/options.ml | 22 +++---- .../helena/src/complete_rg/crgOutput.ml | 46 ++++++------- helm/software/helena/src/lib/Make | 2 +- .../helena/src/{common => lib}/marks.ml | 0 .../helena/src/{common => lib}/marks.mli | 0 helm/software/helena/src/modules.ml | 8 ++- helm/software/helena/src/toplevel/top.ml | 44 ++++++------- helm/software/helena/src/xml/xmlLibrary.ml | 27 ++++---- helm/www/lambdadelta/Makefile | 16 ++--- helm/www/lambdadelta/xml/ld.dtd | 7 +- 19 files changed, 180 insertions(+), 190 deletions(-) rename helm/software/helena/src/{common => lib}/marks.ml (100%) rename helm/software/helena/src/{common => lib}/marks.mli (100%) diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt index bc669964b..7c4fa4e93 100644 --- a/helm/software/helena/.depend.opt +++ b/helm/software/helena/.depend.opt @@ -7,18 +7,18 @@ src/lib/log.cmo : src/lib/log.cmi src/lib/log.cmx : src/lib/log.cmi src/lib/time.cmo : src/lib/log.cmi src/lib/time.cmx : src/lib/log.cmx +src/lib/marks.cmi : +src/lib/marks.cmo : src/lib/marks.cmi +src/lib/marks.cmx : src/lib/marks.cmi src/common/options.cmo : src/lib/cps.cmx src/common/options.cmx : src/lib/cps.cmx -src/common/marks.cmi : -src/common/marks.cmo : src/common/marks.cmi -src/common/marks.cmx : src/common/marks.cmi src/common/hierarchy.cmi : src/common/hierarchy.cmo : src/lib/cps.cmx src/common/hierarchy.cmi src/common/hierarchy.cmx : src/lib/cps.cmx src/common/hierarchy.cmi src/common/layer.cmi : -src/common/layer.cmo : src/common/options.cmx src/common/marks.cmi \ +src/common/layer.cmo : src/common/options.cmx src/lib/marks.cmi \ src/lib/log.cmi src/common/layer.cmi -src/common/layer.cmx : src/common/options.cmx src/common/marks.cmx \ +src/common/layer.cmx : src/common/options.cmx src/lib/marks.cmx \ src/lib/log.cmx src/common/layer.cmi src/common/entity.cmo : src/common/layer.cmi src/common/entity.cmx : src/common/layer.cmx @@ -35,10 +35,10 @@ src/complete_rg/crg.cmo : src/common/layer.cmi src/common/entity.cmx \ src/complete_rg/crg.cmx : src/common/layer.cmx src/common/entity.cmx \ src/lib/cps.cmx src/complete_rg/crgOutput.cmi : src/common/layer.cmi src/complete_rg/crg.cmx -src/complete_rg/crgOutput.cmo : src/common/marks.cmi src/lib/log.cmi \ +src/complete_rg/crgOutput.cmo : src/lib/marks.cmi src/lib/log.cmi \ src/common/layer.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/marks.cmx src/lib/log.cmx \ +src/complete_rg/crgOutput.cmx : src/lib/marks.cmx src/lib/log.cmx \ src/common/layer.cmx src/common/entity.cmx src/complete_rg/crg.cmx \ src/lib/cps.cmx src/complete_rg/crgOutput.cmi src/text/txt.cmo : src/common/layer.cmi @@ -189,26 +189,26 @@ src/basic_rg/brgGrafite.cmo : src/common/options.cmx src/common/layer.cmi \ src/basic_rg/brgGrafite.cmx : src/common/options.cmx src/common/layer.cmx \ src/common/entity.cmx src/lib/cps.cmx src/basic_rg/brg.cmx \ src/common/alpha.cmx src/basic_rg/brgGrafite.cmi -src/basic_ag/bag.cmo : src/common/marks.cmi src/lib/log.cmi \ +src/basic_ag/bag.cmo : src/lib/marks.cmi src/lib/log.cmi \ src/common/entity.cmx src/lib/cps.cmx -src/basic_ag/bag.cmx : src/common/marks.cmx src/lib/log.cmx \ +src/basic_ag/bag.cmx : src/lib/marks.cmx src/lib/log.cmx \ src/common/entity.cmx src/lib/cps.cmx src/basic_ag/bagCrg.cmi : src/common/layer.cmi src/complete_rg/crg.cmx \ src/basic_ag/bag.cmx -src/basic_ag/bagCrg.cmo : src/common/marks.cmi src/common/layer.cmi \ +src/basic_ag/bagCrg.cmo : src/lib/marks.cmi src/common/layer.cmi \ src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ src/basic_ag/bag.cmx src/basic_ag/bagCrg.cmi -src/basic_ag/bagCrg.cmx : src/common/marks.cmx src/common/layer.cmx \ +src/basic_ag/bagCrg.cmx : src/lib/marks.cmx src/common/layer.cmx \ src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ src/basic_ag/bag.cmx src/basic_ag/bagCrg.cmi src/basic_ag/bagOutput.cmi : src/xml/xmlLibrary.cmi src/lib/log.cmi \ src/common/layer.cmi src/basic_ag/bag.cmx src/basic_ag/bagOutput.cmo : src/xml/xmlCrg.cmi src/common/options.cmx \ - src/common/marks.cmi src/lib/log.cmi src/common/hierarchy.cmi \ + src/lib/marks.cmi src/lib/log.cmi src/common/hierarchy.cmi \ src/common/entity.cmx src/basic_ag/bagCrg.cmi src/basic_ag/bag.cmx \ src/basic_ag/bagOutput.cmi src/basic_ag/bagOutput.cmx : src/xml/xmlCrg.cmx src/common/options.cmx \ - src/common/marks.cmx src/lib/log.cmx src/common/hierarchy.cmx \ + src/lib/marks.cmx src/lib/log.cmx src/common/hierarchy.cmx \ src/common/entity.cmx src/basic_ag/bagCrg.cmx src/basic_ag/bag.cmx \ src/basic_ag/bagOutput.cmi src/basic_ag/bagEnvironment.cmi : src/basic_ag/bag.cmx @@ -216,18 +216,18 @@ src/basic_ag/bagEnvironment.cmo : src/lib/log.cmi src/common/entity.cmx \ src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi src/basic_ag/bagEnvironment.cmx : src/lib/log.cmx src/common/entity.cmx \ src/basic_ag/bag.cmx src/basic_ag/bagEnvironment.cmi -src/basic_ag/bagSubstitution.cmi : src/common/marks.cmi src/basic_ag/bag.cmx +src/basic_ag/bagSubstitution.cmi : src/lib/marks.cmi src/basic_ag/bag.cmx src/basic_ag/bagSubstitution.cmo : src/lib/share.cmx src/basic_ag/bag.cmx \ src/basic_ag/bagSubstitution.cmi src/basic_ag/bagSubstitution.cmx : src/lib/share.cmx src/basic_ag/bag.cmx \ src/basic_ag/bagSubstitution.cmi src/basic_ag/bagReduction.cmi : src/common/layer.cmi src/basic_ag/bag.cmx -src/basic_ag/bagReduction.cmo : src/common/options.cmx src/common/marks.cmi \ +src/basic_ag/bagReduction.cmo : src/common/options.cmx src/lib/marks.cmi \ src/lib/log.cmi src/common/entity.cmx src/lib/cps.cmx \ src/basic_ag/bagSubstitution.cmi src/basic_ag/bagOutput.cmi \ src/basic_ag/bagEnvironment.cmi src/basic_ag/bag.cmx \ src/basic_ag/bagReduction.cmi -src/basic_ag/bagReduction.cmx : src/common/options.cmx src/common/marks.cmx \ +src/basic_ag/bagReduction.cmx : src/common/options.cmx src/lib/marks.cmx \ src/lib/log.cmx src/common/entity.cmx src/lib/cps.cmx \ src/basic_ag/bagSubstitution.cmx src/basic_ag/bagOutput.cmx \ src/basic_ag/bagEnvironment.cmx src/basic_ag/bag.cmx \ @@ -253,7 +253,7 @@ src/basic_ag/bagUntrusted.cmx : src/lib/log.cmx src/common/entity.cmx \ src/toplevel/top.cmo : src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \ src/text/txtParser.cmi src/text/txtLexer.cmx src/text/txtCrg.cmi \ src/text/txt.cmx src/lib/time.cmx src/common/output.cmi \ - src/common/options.cmx src/common/marks.cmi src/lib/log.cmi \ + src/common/options.cmx src/lib/marks.cmi src/lib/log.cmi \ src/common/layer.cmi src/common/hierarchy.cmi src/common/entity.cmx \ src/complete_rg/crgOutput.cmi src/complete_rg/crg.cmx src/lib/cps.cmx \ src/basic_rg/brgUntrusted.cmi src/basic_rg/brgReduction.cmi \ @@ -267,7 +267,7 @@ src/toplevel/top.cmo : src/xml/xmlLibrary.cmi src/xml/xmlCrg.cmi \ src/toplevel/top.cmx : src/xml/xmlLibrary.cmx src/xml/xmlCrg.cmx \ src/text/txtParser.cmx src/text/txtLexer.cmx src/text/txtCrg.cmx \ src/text/txt.cmx src/lib/time.cmx src/common/output.cmx \ - src/common/options.cmx src/common/marks.cmx src/lib/log.cmx \ + src/common/options.cmx src/lib/marks.cmx src/lib/log.cmx \ src/common/layer.cmx src/common/hierarchy.cmx src/common/entity.cmx \ src/complete_rg/crgOutput.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \ src/basic_rg/brgUntrusted.cmx src/basic_rg/brgReduction.cmx \ diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile index db940e373..07ecd4e4e 100644 --- a/helm/software/helena/Makefile +++ b/helm/software/helena/Makefile @@ -10,7 +10,7 @@ KEEP = README CLEAN = etc/log.txt etc/profile.txt -TAGS = test-si-fast test-si test-si-matita test profile xml-si-crg xml-si matita matitac +TAGS = test-si-fast test-si test-si-matita test profile xml xml-v3 matita matitac include Makefile.common @@ -29,8 +29,8 @@ MA = grundlagen_2.ma PREAMBLE = ../matita/matita.ma.templ test-si-fast: $(MAIN).opt etc - @echo " HELENA -o -q $(INPUTFAST)" - $(H)./$(MAIN).opt -T 1 -o -q $(O) $(INPUTFAST) > etc/log.txt + @echo " HELENA -o -q -1 $(INPUTFAST)" + $(H)./$(MAIN).opt -T 1 -o -q -1 $(O) $(INPUTFAST) > etc/log.txt test-si: $(MAIN).opt etc @echo " HELENA -d -l -p -o $(INPUT)" @@ -50,13 +50,13 @@ profile: $(MAIN).opt etc $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -o -q $(O) $(INPUTFAST) >> etc/log.txt; done $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile-new.txt -xml-si-crg: $(MAIN).opt etc - @echo " HELENA -l -o -s 1 -x $(INPUT)" - $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 1 -x $(INPUT) > etc/log.txt +xml: $(MAIN).opt etc + @echo " HELENA -l -s 1 -x $(INPUT)" + $(H)./$(MAIN).opt -l -o $(INPUT) -X -O $(XMLDIR) -T 1 -l -s 1 -x $(INPUT) > etc/log.txt -xml-si: $(MAIN).opt etc - @echo " HELENA -l -o -s 2 -x $(INPUT)" - $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 2 -x $(INPUT) > etc/log.txt +xml-v3: $(MAIN).opt etc + @echo " HELENA -l -s 2 -x $(INPUT)" + $(H)./$(MAIN).opt -l -o $(INPUT) -X -O $(XMLDIR) -T 1 -l -s 3 -x $(INPUT) > etc/log.txt matita: matita/$(MA) @echo " MATITA $(MA)" diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml index 866f38341..a92b6fea9 100644 --- a/helm/software/helena/src/automath/autCrg.ml +++ b/helm/software/helena/src/automath/autCrg.ml @@ -239,8 +239,6 @@ let initial_status () = path = []; node = None; nodes = []; line = 1; mk_uri = G.get_mk_uri (); } -let refresh_status lst = {lst with - mk_uri = G.get_mk_uri (); line = 1; -} +let refresh_status lst = initial_status () let crg_of_aut = xlate_entity diff --git a/helm/software/helena/src/basic_ag/bag.ml b/helm/software/helena/src/basic_ag/bag.ml index 74c305156..c0e540963 100644 --- a/helm/software/helena/src/basic_ag/bag.ml +++ b/helm/software/helena/src/basic_ag/bag.ml @@ -12,7 +12,7 @@ (* kernel version: basic, absolute, global *) (* note : experimental *) -module J = Marks +module P = Marks module E = Entity type uri = E.uri @@ -23,15 +23,15 @@ type bind = Void (* exclusion *) | Abbr of term (* abbreviation *) and term = Sort of int (* hierarchy index *) - | LRef of J.mark (* location *) + | LRef of P.mark (* location *) | GRef of uri (* reference *) | Cast of term * term (* domain, element *) | Appl of term * term (* argument, function *) - | Bind of attrs * J.mark * bind * term (* name, location, binder, scope *) + | Bind of attrs * P.mark * bind * term (* name, location, binder, scope *) type entity = term E.entity (* attrs, uri, binder *) -type lenv = (attrs * J.mark * bind) list (* name, location, binder *) +type lenv = (attrs * P.mark * bind) list (* name, location, binder *) type message = (lenv, term) Log.item list diff --git a/helm/software/helena/src/basic_ag/bagCrg.ml b/helm/software/helena/src/basic_ag/bagCrg.ml index 8d35483ea..6a83282b3 100644 --- a/helm/software/helena/src/basic_ag/bagCrg.ml +++ b/helm/software/helena/src/basic_ag/bagCrg.ml @@ -10,7 +10,7 @@ V_______________________________________________________________ *) module C = Cps -module J = Marks +module P = Marks module N = Layer module E = Entity module D = Crg @@ -46,13 +46,13 @@ let rec xlate_term st f c = function and xlate_bind st f c a = function | D.Abst (_, w) -> - let f ww = Z.push "xlate_bind" f c a (J.new_mark ()) (Z.Abst ww) in + let f ww = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abst ww) in xlate_term st f c w | D.Abbr v -> - let f vv = Z.push "xlate_bind" f c a (J.new_mark ()) (Z.Abbr vv) in + let f vv = Z.push "xlate_bind" f c a (P.new_mark ()) (Z.Abbr vv) in xlate_term st f c v | D.Void -> - Z.push "xlate_bind" f c a (J.new_mark ()) Z.Void + Z.push "xlate_bind" f c a (P.new_mark ()) Z.Void (* internal functions: bag to crg term **************************************) diff --git a/helm/software/helena/src/basic_ag/bagOutput.ml b/helm/software/helena/src/basic_ag/bagOutput.ml index c5cb51091..88e64e5d0 100644 --- a/helm/software/helena/src/basic_ag/bagOutput.ml +++ b/helm/software/helena/src/basic_ag/bagOutput.ml @@ -9,12 +9,12 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module P = Printf +module KP = Printf module U = NUri module L = Log +module P = Marks module G = Options -module J = Marks module H = Hierarchy module E = Entity module XD = XmlCrg @@ -83,72 +83,72 @@ let print_counters f c = c.tabbrs in let items = c.eabsts + c.eabbrs in - let locations = J.marks () in - L.warn level (P.sprintf "Kernel representation summary (basic_ag)"); - L.warn level (P.sprintf " Total entry items: %7u" items); - L.warn level (P.sprintf " Declaration items: %7u" c.eabsts); - L.warn level (P.sprintf " Definition items: %7u" c.eabbrs); - L.warn level (P.sprintf " Total term items: %7u" terms); - L.warn level (P.sprintf " Sort items: %7u" c.tsorts); - L.warn level (P.sprintf " Local reference items: %7u" c.tlrefs); - L.warn level (P.sprintf " Global reference items: %7u" c.tgrefs); - L.warn level (P.sprintf " Explicit Cast items: %7u" c.tcasts); - L.warn level (P.sprintf " Application items: %7u" c.tappls); - L.warn level (P.sprintf " Abstraction items: %7u" c.tabsts); - L.warn level (P.sprintf " Abbreviation items: %7u" c.tabbrs); - L.warn level (P.sprintf " Total binder locations: %7u" locations); + let locations = P.marks () in + L.warn level (KP.sprintf "Kernel representation summary (basic_ag)"); + L.warn level (KP.sprintf " Total entry items: %7u" items); + L.warn level (KP.sprintf " Declaration items: %7u" c.eabsts); + L.warn level (KP.sprintf " Definition items: %7u" c.eabbrs); + L.warn level (KP.sprintf " Total term items: %7u" terms); + L.warn level (KP.sprintf " Sort items: %7u" c.tsorts); + L.warn level (KP.sprintf " Local reference items: %7u" c.tlrefs); + L.warn level (KP.sprintf " Global reference items: %7u" c.tgrefs); + L.warn level (KP.sprintf " Explicit Cast items: %7u" c.tcasts); + L.warn level (KP.sprintf " Application items: %7u" c.tappls); + L.warn level (KP.sprintf " Abstraction items: %7u" c.tabsts); + L.warn level (KP.sprintf " Abbreviation items: %7u" c.tabbrs); + L.warn level (KP.sprintf " Total binder locations: %7u" locations); f () let name err och a = let f n = function - | true -> P.fprintf och "%s" n - | false -> P.fprintf och "-%s" n + | true -> KP.fprintf och "%s" n + | false -> KP.fprintf och "-%s" n in E.name err f a let res a l och = - let err () = P.fprintf och "#%s" (J.string_of_mark l) in + let err () = KP.fprintf och "#%s" (P.string_of_mark l) in if !G.indexes then err () else name err och a let rec pp_term st c och = function | Z.Sort h -> - let err () = P.fprintf och "*%u" h in - let f s = P.fprintf och "%s" s in + let err () = KP.fprintf och "*%u" h in + let f s = KP.fprintf och "%s" s in H.string_of_sort err f h | Z.LRef i -> - let err () = P.fprintf och "#%s" (J.string_of_mark i) in + let err () = KP.fprintf och "#%s" (P.string_of_mark i) in let f a _ = name err och a in if !G.indexes then err () else Z.get err f c i - | Z.GRef s -> P.fprintf och "$%s" (U.string_of_uri s) + | Z.GRef s -> KP.fprintf och "$%s" (U.string_of_uri s) | Z.Cast (u, t) -> - P.fprintf och "{%a}.%a" (pp_term st c) u (pp_term st c) t + KP.fprintf och "{%a}.%a" (pp_term st c) u (pp_term st c) t | Z.Appl (v, t) -> - P.fprintf och "(%a).%a" (pp_term st c) v (pp_term st c) t + KP.fprintf och "(%a).%a" (pp_term st c) v (pp_term st c) t | Z.Bind (a, l, Z.Abst w, t) -> let f cc = - P.fprintf och "[%t:%a].%a" (res a l) (pp_term st c) w (pp_term st cc) t + KP.fprintf och "[%t:%a].%a" (res a l) (pp_term st c) w (pp_term st cc) t in Z.push "output abst" f c a l (Z.Abst w) | Z.Bind (a, l, Z.Abbr v, t) -> let f cc = - P.fprintf och "[%t=%a].%a" (res a l) (pp_term st c) v (pp_term st cc) t + KP.fprintf och "[%t=%a].%a" (res a l) (pp_term st c) v (pp_term st cc) t in Z.push "output abbr" f c a l (Z.Abbr v) | Z.Bind (a, l, Z.Void, t) -> - let f cc = P.fprintf och "[%t].%a" (res a l) (pp_term st cc) t in + let f cc = KP.fprintf och "[%t].%a" (res a l) (pp_term st cc) t in Z.push "output void" f c a l Z.Void let pp_lenv st och c = let pp_entry och = function | a, l, Z.Abst w -> - P.fprintf och "%t : %a\n" (res a l) (pp_term st c) w + KP.fprintf och "%t : %a\n" (res a l) (pp_term st c) w | a, l, Z.Abbr v -> - P.fprintf och "%t = %a\n" (res a l) (pp_term st c) v + KP.fprintf och "%t = %a\n" (res a l) (pp_term st c) v | a, l, Z.Void -> - P.fprintf och "%t\n" (res a l) + KP.fprintf och "%t\n" (res a l) in let iter map och l = List.iter (map och) l in - let f es = P.fprintf och "%a" (iter pp_entry) (List.rev es) in + let f es = KP.fprintf och "%a" (iter pp_entry) (List.rev es) in Z.contents f c let specs = { diff --git a/helm/software/helena/src/basic_ag/bagReduction.ml b/helm/software/helena/src/basic_ag/bagReduction.ml index 6524dda86..287978f50 100644 --- a/helm/software/helena/src/basic_ag/bagReduction.ml +++ b/helm/software/helena/src/basic_ag/bagReduction.ml @@ -12,8 +12,8 @@ module U = NUri module C = Cps module L = Log +module P = Marks module G = Options -module J = Marks module E = Entity module Z = Bag module ZO = BagOutput @@ -28,9 +28,9 @@ type machine = { type whd_result = | Sort_ of int - | LRef_ of J.mark * Z.term option + | LRef_ of P.mark * Z.term option | GRef_ of Z.entity - | Bind_ of Z.attrs * J.mark * Z.term * Z.term + | Bind_ of Z.attrs * P.mark * Z.term * Z.term type ho_whd_result = | Sort of int @@ -98,12 +98,12 @@ let rec whd f c m x = begin match m.s with | [] -> f m (Bind_ (a, l, w, t)) | v :: tl -> - let nl = J.new_mark () in + let nl = P.new_mark () in let f mc = ZS.subst (whd f c {m with c = mc; s = tl}) nl l t in Z.push "!" f m.c a nl (Z.Abbr (Z.Cast (w, v))) end | Z.Bind (a, l, b, t) -> - let nl = J.new_mark () in + let nl = P.new_mark () in let f mc = ZS.subst (whd f c {m with c = mc}) nl l t in Z.push "!" f m.c a nl b @@ -156,7 +156,7 @@ let rec are_convertible f st a c m1 t1 m2 t2 = | GRef_ (_, _, _, E.Abbr v1), _ -> whd (aux_rev m2 r2) c m1 v1 | Bind_ (a1, l1, w1, t1), Bind_ (a2, l2, w2, t2) -> - let l = J.new_mark () in + let l = P.new_mark () in let h c = let m1, m2 = inc m1, inc m2 in let f t1 = ZS.subst (are_convertible f st a c m1 t1 m2) l l2 t2 in diff --git a/helm/software/helena/src/common/Make b/helm/software/helena/src/common/Make index c019e1d23..4abdda084 100644 --- a/helm/software/helena/src/common/Make +++ b/helm/software/helena/src/common/Make @@ -1 +1 @@ -options marks hierarchy layer entity output alpha +options hierarchy layer entity output alpha diff --git a/helm/software/helena/src/common/layer.ml b/helm/software/helena/src/common/layer.ml index ed2b140e4..ea02538d2 100644 --- a/helm/software/helena/src/common/layer.ml +++ b/helm/software/helena/src/common/layer.ml @@ -9,15 +9,15 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module H = Hashtbl +module KH = Hashtbl module L = Log +module P = Marks module G = Options -module J = Marks type value = Inf (* infinite layer *) | Fin of int (* finite layer *) - | Ref of J.mark * int (* referred layer, step *) + | Ref of P.mark * int (* referred layer, step *) | Unk (* no layer set *) type layer = { @@ -26,7 +26,7 @@ type layer = { mutable b: bool; (* beta allowed? *) } -type status = (J.mark, layer) H.t (* environment for layer variables *) +type status = (P.mark, layer) KH.t (* environment for layer variables *) (* Internal functions *******************************************************) @@ -41,17 +41,17 @@ let zero = Fin 0 let string_of_value k = function | Inf -> "" | Fin i -> string_of_int i - | Ref (k, i) -> "-" ^ J.string_of_mark k ^ "-" ^ string_of_int i - | Unk -> "-" ^ J.string_of_mark k + | Ref (k, i) -> "-" ^ P.string_of_mark k ^ "-" ^ string_of_int i + | Unk -> "-" ^ P.string_of_mark k (* Note: remove assigned variables *) let pp_table st = let map k n = warn (Printf.sprintf "%s: v %s (s:%b b:%b)" - (J.string_of_mark k) (string_of_value k n.v) n.s n.b + (P.string_of_mark k) (string_of_value k n.v) n.s n.b ) in - H.iter map st + KH.iter map st let cell s v = { v = v; s = s; b = false @@ -62,10 +62,10 @@ let empty () = cell true Unk let dynamic k i = cell false (Ref (k, i)) let find_with_default st default k = - try H.find st k with Not_found -> H.add st k default; default + try KH.find st k with Not_found -> KH.add st k default; default let find st k = - try H.find st k with Not_found -> assert false + try KH.find st k with Not_found -> assert false let rec resolve_key_with_default st default k = match find_with_default st default k with | {v = Ref (k, i)} when i = 0 -> resolve_key_with_default st default k @@ -77,14 +77,14 @@ let rec resolve_key st k = match find st k with let resolve_layer st = function | {v = Ref (k, i)} when i = 0 -> resolve_key st k - | cell -> J.null_mark, cell + | cell -> P.null_mark, cell let rec generated st h i = let default = dynamic h i in - let k = J.new_mark () in + let k = P.new_mark () in let k, n = resolve_key_with_default st default k in if n.s then generated st h i else begin - if n <> default then H.replace st k default; + if n <> default then KH.replace st k default; if !G.trace >= level then pp_table st; default end @@ -93,15 +93,15 @@ let assert_finite st n j = let rec aux (k, n) j = match n.v with | Fin i when i = j -> true | Fin i -> - Printf.printf "binder %s is %u but must be %u\n" (J.string_of_mark k) i j; true (**) + Printf.printf "binder %s is %u but must be %u\n" (P.string_of_mark k) i j; true (**) | Inf -> - Printf.printf "binder %s is infinite but must be %u\n" (J.string_of_mark k) j; true (**) + Printf.printf "binder %s is infinite but must be %u\n" (P.string_of_mark k) j; true (**) | Unk -> n.v <- Fin j; if !G.trace >= level then pp_table st; true | Ref (k, i) -> n.v <- Fin j; aux (resolve_key st k) (i+j) in let k, n = resolve_layer st n in (* if j = 0 && n.b then begin - Printf.printf "^Pi reduction on binder %s\n" (J.string_of_mark k); false (**) + Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false (**) end else *) aux (k, n) j @@ -110,7 +110,7 @@ let assert_infinite st n = let rec aux (k, n) = match n.v with | Inf -> true | Fin i -> - Printf.printf "binder %s is %u but must be infinite\n" (J.string_of_mark k) i; true (**) + Printf.printf "binder %s is %u but must be infinite\n" (P.string_of_mark k) i; true (**) | Unk -> n.v <- Inf; if !G.trace >= level then pp_table st; true | Ref (k, _) -> n.v <- Inf; aux (resolve_key st k) in @@ -119,7 +119,7 @@ let assert_infinite st n = (* Interface functions ******************************************************) let initial_status () = - H.create env_size + KH.create env_size let refresh_status st = st @@ -134,7 +134,7 @@ let two = finite 2 let rec unknown st = if !G.trace >= level then warn "UNKNOWN"; let default = empty () in - let k = J.new_mark () in + let k = P.new_mark () in let k, n = resolve_key_with_default st default k in if n.s then match n.v with | Inf @@ -150,7 +150,7 @@ let minus st n j = | Fin i when i > j -> cell false (Fin (i - j)) | Fin _ -> cell false zero | Unk -> - if k = J.null_mark then assert false else generated st k j + if k = P.null_mark then assert false else generated st k j | Ref (k, i) -> let k, n = resolve_key st k in aux k n (i+j) @@ -168,8 +168,8 @@ let assert_not_zero st n = match n.b, n.v with | true, _ -> n.b (* | _ , Fin i when i = 0 -> - Printf.printf "^Pi reduction on binder %s\n" (J.string_of_mark k); false *) (**) -(* if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (J.string_of_mark k); *) + Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false *) (**) +(* if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (P.string_of_mark k); *) | _ -> n.b <- true; if !G.trace >= level then pp_table st; n.b let assert_zero st n = assert_finite st n 0 @@ -187,7 +187,7 @@ let assert_equal st n1 n2 = else false in begin if !G.trace >= level then warn "ASSERT EQUAL"; - if b && k1 <> J.null_mark && k2 <> J.null_mark then begin + if b && k1 <> P.null_mark && k2 <> P.null_mark then begin n1.v <- Ref (k2, 0); if !G.trace >= level then pp_table st end; b end diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml index 47ee34272..3a394c5b7 100644 --- a/helm/software/helena/src/common/options.ml +++ b/helm/software/helena/src/common/options.ml @@ -9,13 +9,13 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module F = Filename +module KF = Filename module C = Cps type uri_generator = string -> string -type kernel = Crg | Brg | Bag +type kernel = V4 | V3 | V0 (* interface functions ******************************************************) @@ -29,7 +29,7 @@ let summary = ref false (* log summary information *) let xdir = ref "" (* directory for XML output *) -let kernel = ref Brg (* kernel type *) +let kernel = ref V3 (* kernel type *) let si = ref false (* use sort inclusion *) @@ -55,25 +55,21 @@ let ma_preamble = ref "" (* location of grafite preamble file *) let alpha = ref "" (* prefix of numeric identifiers *) -let kernel_id () = - let id = match !kernel with - | Crg -> "crg" - | Brg -> "brg" - | Bag -> "bag" - in - let si = if !si then "_si" else "" in - id ^ si +let kernel_id () = match !kernel with + | V4 -> "" + | V3 -> "V3" + | V0 -> "V0" let get_baseuri () = String.concat "/" ["ld:"; kernel_id (); !cover; "" ] let get_mk_uri () = let bu = get_baseuri () in - fun s -> F.concat bu (s ^ ".ld") + fun s -> KF.concat bu (s ^ ".ld") let clear () = stage := 3; trace := 0; summary := false; - xdir := ""; kernel := Brg; si := false; cover := ""; + xdir := ""; kernel := V3; si := false; cover := ""; expand := false; indexes := false; icm := 0; unquote := false; debug_parser := false; debug_lexer := false; ma_dir := ""; ma_preamble := "" diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml index 6ccf47af0..7275dd462 100644 --- a/helm/software/helena/src/complete_rg/crgOutput.ml +++ b/helm/software/helena/src/complete_rg/crgOutput.ml @@ -9,12 +9,12 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module P = Printf +module KP = Printf module U = NUri module C = Cps module L = Log -module J = Marks +module P = Marks module N = Layer module E = Entity module D = Crg @@ -109,35 +109,35 @@ let print_counters f c = in let items = c.eabsts + c.eabbrs in let nodes = c.nodes + c.xnodes in - let marks = J.marks () in - L.warn level (P.sprintf "Intermediate representation summary (complete_rg)"); - L.warn level (P.sprintf " Total entry items: %7u" items); - L.warn level (P.sprintf " Declaration items: %7u" c.eabsts); - L.warn level (P.sprintf " Definition items: %7u" c.eabbrs); - L.warn level (P.sprintf " Total term items: %7u" terms); - L.warn level (P.sprintf " Sort items: %7u" c.tsorts); - L.warn level (P.sprintf " Local reference items: %7u" c.tlrefs); - L.warn level (P.sprintf " Global reference items: %7u" c.tgrefs); - L.warn level (P.sprintf " Explicit Cast items: %7u" c.tcasts); - L.warn level (P.sprintf " Application items: %7u" c.tappls); - L.warn level (P.sprintf " Abstraction items: %7u" c.tabsts); - L.warn level (P.sprintf " Abbreviation items: %7u" c.tabbrs); - L.warn level (P.sprintf " Ambiguous abstractions: %7u" marks); - L.warn level (P.sprintf " Global Int. Complexity: %7u" c.nodes); - L.warn level (P.sprintf " + Abbreviation nodes: %7u" nodes); + let marks = P.marks () in + L.warn level (KP.sprintf "Intermediate representation summary (complete_rg)"); + L.warn level (KP.sprintf " Total entry items: %7u" items); + L.warn level (KP.sprintf " Declaration items: %7u" c.eabsts); + L.warn level (KP.sprintf " Definition items: %7u" c.eabbrs); + L.warn level (KP.sprintf " Total term items: %7u" terms); + L.warn level (KP.sprintf " Sort items: %7u" c.tsorts); + L.warn level (KP.sprintf " Local reference items: %7u" c.tlrefs); + L.warn level (KP.sprintf " Global reference items: %7u" c.tgrefs); + L.warn level (KP.sprintf " Explicit Cast items: %7u" c.tcasts); + L.warn level (KP.sprintf " Application items: %7u" c.tappls); + L.warn level (KP.sprintf " Abstraction items: %7u" c.tabsts); + L.warn level (KP.sprintf " Abbreviation items: %7u" c.tabbrs); + L.warn level (KP.sprintf " Ambiguous abstractions: %7u" marks); + L.warn level (KP.sprintf " Global Int. Complexity: %7u" c.nodes); + L.warn level (KP.sprintf " + Abbreviation nodes: %7u" nodes); f () (* term/environment pretty printer ******************************************) let pp_attrs out a = - let f s b = if b then out (P.sprintf "%s;" s) else out (P.sprintf "~%s;" s) in + let f s b = if b then out (KP.sprintf "%s;" s) else out (KP.sprintf "~%s;" s) in E.name ignore f a; - out (P.sprintf "+%i;" a.E.n_apix) + out (KP.sprintf "+%i;" a.E.n_apix) let rec pp_term out st = function - | D.TSort (a, l) -> pp_attrs out a; out (P.sprintf "*%u" l) - | D.TLRef (a, i ) -> pp_attrs out a; out (P.sprintf "#%u" i) - | D.TGRef (a, u) -> pp_attrs out a; out (P.sprintf "$") + | D.TSort (a, l) -> pp_attrs out a; out (KP.sprintf "*%u" l) + | D.TLRef (a, i ) -> pp_attrs out a; out (KP.sprintf "#%u" i) + | D.TGRef (a, u) -> pp_attrs out a; out (KP.sprintf "$") | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out st x; out ">."; pp_term out st y | D.TAppl (a, x, y) -> pp_attrs out a; out "("; pp_term out st x; out ")."; pp_term out st y | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out st x; out "."; pp_term out st y diff --git a/helm/software/helena/src/lib/Make b/helm/software/helena/src/lib/Make index 45d5eac3b..c72a054c3 100644 --- a/helm/software/helena/src/lib/Make +++ b/helm/software/helena/src/lib/Make @@ -1 +1 @@ -cps share log time +cps share log time marks diff --git a/helm/software/helena/src/common/marks.ml b/helm/software/helena/src/lib/marks.ml similarity index 100% rename from helm/software/helena/src/common/marks.ml rename to helm/software/helena/src/lib/marks.ml diff --git a/helm/software/helena/src/common/marks.mli b/helm/software/helena/src/lib/marks.mli similarity index 100% rename from helm/software/helena/src/common/marks.mli rename to helm/software/helena/src/lib/marks.mli diff --git a/helm/software/helena/src/modules.ml b/helm/software/helena/src/modules.ml index 834a9a19f..3de74e13f 100644 --- a/helm/software/helena/src/modules.ml +++ b/helm/software/helena/src/modules.ml @@ -1,4 +1,8 @@ -(* free = F I K M P Q U V W *) +(* free = F I J M Q U V W *) + +module KF = Filename +module KH = Hashtbl +module KP = Printf module U = NUri module UH = NUri.UriHash @@ -7,9 +11,9 @@ module C = Cps module S = Share module L = Log module Y = Time (**) +module P = Marks module G = Options -module J = Marks (**) module H = Hierarchy module N = Layer module E = Entity diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml index d57c2b007..66baa8658 100644 --- a/helm/software/helena/src/toplevel/top.ml +++ b/helm/software/helena/src/toplevel/top.ml @@ -9,15 +9,15 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module F = Filename -module P = Printf +module KF = Filename +module KP = Printf module U = NUri module C = Cps module L = Log module Y = Time +module P = Marks module G = Options -module J = Marks module H = Hierarchy module N = Layer module E = Entity @@ -84,21 +84,21 @@ type kernel_entity = BrgEntity of Brg.entity | CrgEntity of Crg.entity let print_counters st = function - | 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 + | G.V4 -> DO.print_counters C.start st.dc + | G.V3 -> BO.print_counters C.start st.bc + | G.V0 -> ZO.print_counters C.start st.zc let xlate_entity st entity = match !G.kernel, entity with - | G.Brg, CrgEntity e -> + | G.V3, CrgEntity e -> let f e = (BrgEntity e) in E.xlate f BD.brg_of_crg e - | G.Bag, CrgEntity e -> + | G.V0, CrgEntity e -> let f e = (BagEntity e) in E.xlate f (ZD.bag_of_crg st.kst) e | _, entity -> entity let pp_progress e = let f _ na u = let s = U.string_of_uri u in - L.warn 2 (P.sprintf "[%u] <%s>" na.E.n_apix s); + L.warn 2 (KP.sprintf "[%u] <%s>" na.E.n_apix s); in Y.utime_stamp "intermediate"; match e with @@ -168,13 +168,13 @@ type input_entity = TxtEntity of Txt.command | NoEntity let type_of_input name = - if F.check_suffix name ".hln" then Text - else if F.check_suffix name ".aut" then + if KF.check_suffix name ".hln" then Text + else if KF.check_suffix name ".aut" then let _ = H.set_sorts 0 ["Set"; "Prop"] in assert (H.set_graph "Z2"); Automath else begin - L.warn level (P.sprintf "Unknown file type: %s" name); exit 2 + L.warn level (KP.sprintf "Unknown file type: %s" name); exit 2 end let txt_xl = initial_lexer TxtLexer.token @@ -288,12 +288,12 @@ let main = let print_version () = L.warn level (G.version_string ^ "\n"); exit 0 in let set_hierarchy s = if H.set_graph s then () else - L.warn level (P.sprintf "Unknown type hierarchy: %s" s) + L.warn level (KP.sprintf "Unknown type hierarchy: %s" s) in let set_kernel = function - | "brg" -> G.kernel := G.Brg - | "bag" -> G.kernel := G.Bag - | s -> L.warn level (P.sprintf "Unknown kernel version: %s" s) + | "V3" -> G.kernel := G.V3 + | "V0" -> G.kernel := G.V0 + | s -> L.warn level (KP.sprintf "Unknown kernel version: %s" s) in let set_trace i = if !G.trace = 0 && i > 0 then Y.gmtime G.version_string; @@ -316,14 +316,14 @@ let main = version := true in let process_file name = - if !G.trace >= 2 then L.warn 1 (P.sprintf "Processing file: %s" name); + if !G.trace >= 2 then L.warn 1 (KP.sprintf "Processing file: %s" name); if !G.trace >= 2 then Y.utime_stamp "started"; let base_name = Filename.chop_extension (Filename.basename name) in - let cover = F.concat !root base_name in - if !G.stage <= 1 then G.kernel := G.Crg; + let cover = KF.concat !root base_name in + if !G.stage <= 1 then G.kernel := G.V4; G.cover := cover; if !G.ma_preamble <> "" then st := {!st with och = Some (BG.open_out base_name)}; - J.clear_marks (); + P.clear_marks (); let sst, input = process (refresh_status !st) name in st := begin match sst.och with | None -> sst @@ -333,7 +333,7 @@ let main = if !G.summary then begin AO.print_counters C.start !st.ac; if !preprocess then AO.print_process_counters C.start !st.pst; - if !G.stage >= 1 then print_counters !st G.Crg; + if !G.stage >= 1 then print_counters !st G.V4; if !G.stage >= 2 then print_counters !st !G.kernel; if !G.stage >= 3 then O.print_reductions () end @@ -361,7 +361,7 @@ let main = let help_g = " always expand global definitions" in let help_h = " set type hierarchy (default: \"Z1\")" in let help_i = " show local references by index" in - let help_k = " set kernel version (default: \"brg\")" in + let help_k = " set kernel version (default: \"V3\")" in let help_l = " disambiguate binders level (Automath)" in let help_m = " export kernel entities (Grafite) setting location of preamble to (default: empty)" in let help_o = " activate sort inclusion (default: false)" in diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml index 77fb9351a..d51af0bfb 100644 --- a/helm/software/helena/src/xml/xmlLibrary.ml +++ b/helm/software/helena/src/xml/xmlLibrary.ml @@ -9,14 +9,14 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module F = Filename +module KF = Filename -module U = NUri -module C = Cps -module G = Options -module H = Hierarchy -module N = Layer -module E = Entity +module U = NUri +module C = Cps +module G = Options +module H = Hierarchy +module N = Layer +module E = Entity (* internal functions *******************************************************) @@ -24,17 +24,17 @@ let base = "xml" let ext = ".xml" -let obj_root = "ENTITY" +let obj_root = "CONSTANT" let home = "http://lambdadelta.info/" -let system = F.concat (F.concat home base) "ld.dtd" +let system = KF.concat (KF.concat home base) "ld.dtd" let xmlns = "xmlns", home let path_of_uri xdir uri = - let base = F.concat xdir base in - F.concat base (Str.string_after (U.string_of_uri uri) 3) + let base = KF.concat xdir base in + KF.concat base (Str.string_after (U.string_of_uri uri) 3) (* interface functions ******************************************************) @@ -122,7 +122,7 @@ let info a = let export_entity pp_term (ra, na, u, b) = let path = path_of_uri !G.xdir u in - let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in + let _ = Sys.command (Printf.sprintf "mkdir -p %s" (KF.dirname path)) in let och = open_out (path ^ ext) in let out = output_string och in xml out "1.0" "UTF-8"; doctype out obj_root system; @@ -133,8 +133,7 @@ let export_entity pp_term (ra, na, u, b) = | E.Abbr v -> tag "GDef" attrs ~contents:(pp_term v) | E.Void -> assert false in - let opts = if !G.si then "si" else "" in let shp = H.string_of_graph () in - let attrs = [xmlns; "hierarchy", shp; "options", opts] in + let attrs = [xmlns; "hierarchy", shp] in tag obj_root attrs ~contents out 0; close_out och diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile index 4c610a09a..c583563f0 100644 --- a/helm/www/lambdadelta/Makefile +++ b/helm/www/lambdadelta/Makefile @@ -30,17 +30,11 @@ SLS = helena.sl automath.sl BIB = lambdadelta.bib CONTRIB = lambdadelta_2.tar.gz -XMLS = brg_si/grundlagen/l/not.ld.xml \ - brg_si/grundlagen/l/et.ld.xml \ - brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \ - brg_si/grundlagen/l/e/pairis1.ld.xml \ - brg_si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \ - crg_si/grundlagen/l/not.ld.xml \ - crg_si/grundlagen/l/et.ld.xml \ - crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \ - crg_si/grundlagen/l/e/pairis1.ld.xml \ - crg_si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \ - brg_si/grundlagen/ccs.ldc.xml +XMLS = grundlagen_2/l/not.ld.xml \ + grundlagen_2/l/et.ld.xml \ + grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \ + grundlagen_2/l/e/pairis1.ld.xml \ + grundlagen_2/l/e/st/eq/landau/n/327/t25.ld.xml \ LDWEB = ld_web.xsl ld_web_root.xsl ld_web_library.xsl diff --git a/helm/www/lambdadelta/xml/ld.dtd b/helm/www/lambdadelta/xml/ld.dtd index a6bb14c88..a01238d91 100644 --- a/helm/www/lambdadelta/xml/ld.dtd +++ b/helm/www/lambdadelta/xml/ld.dtd @@ -62,7 +62,7 @@ - + - - + -- 2.39.2