From 3f6af93003bef461be59c8d4c96009c631f0c2e7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 5 Jan 2010 19:13:40 +0000 Subject: [PATCH] - we now add the kernel options in the preamble of the URI hierarchy - we now quote the identifiers by default to make them NMTOKENS but we added a command line option to disable this quoting (it can be time consuming) --- helm/software/lambda-delta/Makefile | 55 ++++++++++++------- helm/software/lambda-delta/Makefile.common | 1 + .../lambda-delta/automath/autLexer.mll | 19 ++++++- helm/software/lambda-delta/basic_ag/bag.ml | 5 +- helm/software/lambda-delta/basic_rg/brg.ml | 5 +- .../lambda-delta/basic_rg/brgOutput.ml | 2 +- helm/software/lambda-delta/complete_rg/crg.ml | 5 +- .../lambda-delta/complete_rg/crgAut.ml | 6 +- helm/software/lambda-delta/toplevel/top.ml | 12 +++- helm/software/lambda-delta/xml/ld.dtd | 50 ++++++++--------- 10 files changed, 102 insertions(+), 58 deletions(-) diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index 9903f4fc4..86d068f6a 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -6,42 +6,37 @@ KEEP = README automath/*.aut CLEAN = etc/log.txt -TAGS = test test-si test-si-fast hal xml-si-drg xml-si-old profile +TAGS = test-si test-si-fast hal xml-si-drg xml-si profile -XMLS = xml/brg/grundlagen/l/not.ld.xml xml/brg/grundlagen/l/et.ld.xml \ - xml/brg/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \ - xml/brg/grundlagen/l/e/pairis1.ld.xml +XMLS = xml/brg-si/grundlagen/l/not.ld.xml \ + xml/brg-si/grundlagen/l/et.ld.xml \ + xml/brg-si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \ + xml/brg-si/grundlagen/l/e/pairis1.ld.xml include Makefile.common INPUT = automath/grundlagen.aut -INPUT-ORIG = automath/grundlagen-orig.aut - -test: $(MAIN).opt - @echo " HELENA -o -p -r $(INPUT)" - $(H)./$(MAIN).opt -o -p -r -S 3 $(O) $(INPUT) > etc/log.txt - test-si: $(MAIN).opt - @echo " HELENA -o -p -r -u $(INPUT)" - $(H)./$(MAIN).opt -o -p -r -u -S 3 $(O) $(INPUT) > etc/log.txt + @echo " HELENA -p -r -u $(INPUT)" + $(H)./$(MAIN).opt -p -r -u -S 3 $(O) $(INPUT) > etc/log.txt test-si-fast: $(MAIN).opt - @echo " HELENA -o -r -u $(INPUT)" - $(H)./$(MAIN).opt -o -r -u -S 1 $(O) $(INPUT) > etc/log.txt + @echo " HELENA -r -u -q $(INPUT)" + $(H)./$(MAIN).opt -r -u -q -S 1 $(O) $(INPUT) > etc/log.txt profile: $(MAIN).opt - @echo " HELENA -r -u $(INPUT) (30 TIMES)" - $(H)for T in `seq 30`; do ./$(MAIN).opt -r -u -S 1 $(O) automath/grundlagen.aut >> etc/log.txt; done + @echo " HELENA -r -u -q $(INPUT) (30 TIMES)" + $(H)for T in `seq 30`; do ./$(MAIN).opt -r -u -q -S 1 $(O) automath/grundlagen.aut >> etc/log.txt; done $(H)grep "at exit" etc/log.txt | sort | uniq | less hal: $(MAIN).opt @echo " HELENA -o -x -m $(INPUT)" $(H)./$(MAIN).opt -o -x -m -s 1 -S 1 $(INPUT) > etc/log.txt -xml-si-old: $(MAIN).opt - @echo " HELENA -o -u -x -s 2 $(INPUT)" - $(H)./$(MAIN).opt -o -u -x -s 2 -S 1 $(INPUT) > etc/log.txt +xml-si: $(MAIN).opt + @echo " HELENA -u -x -s 2 $(INPUT)" + $(H)./$(MAIN).opt -u -x -s 2 -S 1 $(INPUT) > etc/log.txt xml-si-drg: $(MAIN).opt @echo " HELENA -u -x -s 1 $(INPUT)" @@ -69,3 +64,25 @@ test-html: lddl: index @echo " GENERATE lddl.tar.bz2" $(H)tar -cjf $(DOWNDIR)/lddl.tar.bz2 -X etc/exclude.txt xml + +install-xml: etc/make-html.sh + @echo " INSTALL xml" + cp -a xml/index.txt xml/ld.dtd xml/brg-si/ $(XMLDIR) + +# old targets ########################################################## + +test: $(MAIN).opt + @echo " HELENA -o -p -r $(INPUT)" + $(H)./$(MAIN).opt -o -p -r -S 3 $(O) $(INPUT) > etc/log.txt + +test-si-old: $(MAIN).opt + @echo " HELENA -o -p -r -u $(INPUT)" + $(H)./$(MAIN).opt -o -p -r -u -S 3 $(O) $(INPUT) > etc/log.txt + +test-si-fast-old: $(MAIN).opt + @echo " HELENA -o -r -u -q $(INPUT)" + $(H)./$(MAIN).opt -o -r -u -q -S 1 $(O) $(INPUT) > etc/log.txt + +xml-si-old: $(MAIN).opt + @echo " HELENA -o -u -x -s 2 $(INPUT)" + $(H)./$(MAIN).opt -o -u -x -s 2 -S 1 $(INPUT) > etc/log.txt diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common index ca219ca66..332200949 100644 --- a/helm/software/lambda-delta/Makefile.common +++ b/helm/software/lambda-delta/Makefile.common @@ -3,6 +3,7 @@ H=@ LDDLURL = http://helm.cs.unibo.it/lambda-delta/static/lddl LDDLDIR = /projects/helm/public_html/lambda-delta/static/lddl DOWNDIR = /projects/helm/public_html/lambda-delta/download +XMLDIR = /projects/helm/public_html/lambda-delta/xml DIRECTORIES = $(shell cat Make) diff --git a/helm/software/lambda-delta/automath/autLexer.mll b/helm/software/lambda-delta/automath/autLexer.mll index 006c056b9..b7009f924 100644 --- a/helm/software/lambda-delta/automath/autLexer.mll +++ b/helm/software/lambda-delta/automath/autLexer.mll @@ -15,6 +15,20 @@ let debug = false let out s = if debug then L.warn s else () + + let unquote = ref false + +(* This turns an Automath identifier into an XML nmtoken *) + let quote id = + let l = String.length id in + let rec aux i = + if i < l then begin + if id.[i] = '\'' || id.[i] = '`' then id.[i] <- '_'; + aux (succ i) + end else + id + in + aux 0 } let LC = ['#' '%'] @@ -53,7 +67,10 @@ and token = parse | "'prop'" { out "PROP"; P.PROP } | "TYPE" { out "TYPE"; P.TYPE } | "'type'" { out "TYPE"; P.TYPE } - | ID { out "ID"; P.IDENT (Lexing.lexeme lexbuf) } + | ID { out "ID"; + let s = Lexing.lexeme lexbuf in + if !unquote then P.IDENT s else P.IDENT (quote s) + } | ":=" { out "DEF"; P.DEF } | "(" { out "OP"; P.OP } | ")" { out "CP"; P.CP } diff --git a/helm/software/lambda-delta/basic_ag/bag.ml b/helm/software/lambda-delta/basic_ag/bag.ml index 8a07f55a8..1aa9b62e7 100644 --- a/helm/software/lambda-delta/basic_ag/bag.ml +++ b/helm/software/lambda-delta/basic_ag/bag.ml @@ -34,8 +34,9 @@ type message = (lenv, term) Log.item list (* helpers ******************************************************************) -let mk_uri root s = - String.concat "/" ["ld:"; "bag"; root; s ^ ".ld"] +let mk_uri si root s = + let kernel = if si then "bag-si" else "bag" in + String.concat "/" ["ld:"; kernel; root; s ^ ".ld"] (* Currified constructors ***************************************************) diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index fd93f397a..efc5d7556 100644 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -35,8 +35,9 @@ type lenv = Null (* helpers ******************************************************************) -let mk_uri root s = - String.concat "/" ["ld:"; "brg"; root; s ^ ".ld"] +let mk_uri si root s = + let kernel = if si then "brg-si" else "brg" in + String.concat "/" ["ld:"; kernel; root; s ^ ".ld"] (* Currified constructors ***************************************************) diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index 70464fde7..e4e7489ca 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -135,7 +135,7 @@ let rename f e a = let rec aux f e n r = let f = function | true -> f n r - | false -> aux f e (n ^ "'") r + | false -> aux f e (n ^ "_") r in does_not_occur f n r e in diff --git a/helm/software/lambda-delta/complete_rg/crg.ml b/helm/software/lambda-delta/complete_rg/crg.ml index 6db1b5481..fa76c6164 100644 --- a/helm/software/lambda-delta/complete_rg/crg.ml +++ b/helm/software/lambda-delta/complete_rg/crg.ml @@ -36,8 +36,9 @@ type entity = term Entity.entity (* helpers ******************************************************************) -let mk_uri root s = - String.concat "/" ["ld:"; "crg"; root; s ^ ".ld"] +let mk_uri si root s = + let kernel = if si then "crg-si" else "crg" in + String.concat "/" ["ld:"; kernel; root; s ^ ".ld"] let empty_lenv = ESort diff --git a/helm/software/lambda-delta/complete_rg/crgAut.ml b/helm/software/lambda-delta/complete_rg/crgAut.ml index 267e2b403..8420cbea7 100644 --- a/helm/software/lambda-delta/complete_rg/crgAut.ml +++ b/helm/software/lambda-delta/complete_rg/crgAut.ml @@ -62,9 +62,9 @@ let id_of_name (id, _, _) = id let mk_qid f st id path = let str = String.concat "/" path in let str = Filename.concat str id in - let f str = f (U.uri_of_string str, id, path) in - f (st.mk_uri str) - + let str = st.mk_uri str in + f (U.uri_of_string str, id, path) + let uri_of_qid (uri, _, _) = uri let complete_qid f st (id, is_local, qs) = diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index c1c353844..515e6590e 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -18,6 +18,7 @@ module H = Hierarchy module O = Output module Y = Entity module X = Library +module AL = AutLexer module AP = AutProcess module AO = AutOutput module DA = CrgAut @@ -52,7 +53,7 @@ let initial_status mk_uri cover g expand si = { brgc = BrgO.initial_counters; bagc = BagO.initial_counters; mst = MA.initial_status ~cover (); - dst = DA.initial_status (mk_uri cover); + dst = DA.initial_status (mk_uri si cover); ast = AP.initial_status; kst = Y.initial_status g expand si } @@ -181,7 +182,7 @@ let rec process st = function let main = try - let version_string = "Helena 0.8.1 M - December 2009" in + let version_string = "Helena 0.8.1 M - January 2010" in let set_hierarchy s = let err () = L.warn (P.sprintf "Unknown type hierarchy: %s" s) in let f g = graph := g in @@ -199,6 +200,9 @@ try let f och = moch := Some och in ML.open_out f name in + let unquote () = + AL.unquote := true + in let close = function | None -> () | Some och -> ML.close_out C.start och @@ -240,7 +244,7 @@ try flush_all () in let help = - "Usage: helena [ -Vcgijmopux | -Ss | -hk ] ...\n\n" ^ + "Usage: helena [ -Vcgijmopqrux | -Ss | -hk ] ...\n\n" ^ "Summary levels: 0 just errors (default), 1 time stamps, 2 processed file names, \ 3 data information, 4 typing information, 5 reduction information\n\n" ^ "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n" @@ -257,6 +261,7 @@ try let help_m = " output intermediate representation (HAL)" in let help_o = " use old abstract language instead of crg" in let help_p = " preprocess Automath source" in + let help_q = " disable quotation of identifiers" in let help_r = " disable initial segment of URI hierarchy" in let help_s = " set translation stage (see above)" in let help_u = " activate sort inclusion" in @@ -276,6 +281,7 @@ try ("-m", Arg.Set meta, help_m); ("-o", Arg.Set old, help_o); ("-p", Arg.Set preprocess, help_p); + ("-q", Arg.Unit unquote, help_q); ("-r", Arg.Clear use_cover, help_r); ("-s", Arg.Int set_stage, help_s); ("-u", Arg.Set si, help_u); diff --git a/helm/software/lambda-delta/xml/ld.dtd b/helm/software/lambda-delta/xml/ld.dtd index 49da57521..83cfc0596 100644 --- a/helm/software/lambda-delta/xml/ld.dtd +++ b/helm/software/lambda-delta/xml/ld.dtd @@ -12,53 +12,53 @@ @@ -67,16 +67,16 @@ -- 2.39.2