- 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)
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)"
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
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)
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 = ['#' '%']
| "'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 }
(* 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 ***************************************************)
(* 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 ***************************************************)
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
(* 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
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) =
module O = Output
module Y = Entity
module X = Library
+module AL = AutLexer
module AP = AutProcess
module AO = AutOutput
module DA = CrgAut
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
}
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
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
flush_all ()
in
let help =
- "Usage: helena [ -Vcgijmopux | -Ss <number> | -hk <string> ] <file> ...\n\n" ^
+ "Usage: helena [ -Vcgijmopqrux | -Ss <number> | -hk <string> ] <file> ...\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"
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 = "<number> set translation stage (see above)" in
let help_u = " activate sort inclusion" in
("-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);
<!ELEMENT Sort EMPTY>
<!ATTLIST Sort
- position NMTOKEN #REQUIRED
- name CDATA #IMPLIED
- mark NMTOKEN #IMPLIED
+ position NMTOKEN #REQUIRED
+ name NMTOKENS #IMPLIED
+ mark NMTOKENS #IMPLIED
>
<!ELEMENT LRef EMPTY>
<!ATTLIST LRef
- position NMTOKEN #REQUIRED
- name CDATA #IMPLIED
- mark NMTOKEN #IMPLIED
+ position NMTOKEN #REQUIRED
+ name NMTOKENS #IMPLIED
+ mark NMTOKENS #IMPLIED
>
<!ELEMENT GRef EMPTY>
<!ATTLIST GRef
- uri CDATA #REQUIRED
- name CDATA #IMPLIED
- mark NMTOKEN #IMPLIED
+ uri CDATA #REQUIRED
+ name NMTOKENS #IMPLIED
+ mark NMTOKENS #IMPLIED
>
<!ELEMENT Cast %term;>
<!ATTLIST Cast
- name CDATA #IMPLIED
- mark NMTOKEN #IMPLIED
+ name NMTOKENS #IMPLIED
+ mark NMTOKENS #IMPLIED
>
<!ELEMENT Appl %term;>
<!ATTLIST Appl
- name CDATA #IMPLIED
- mark NMTOKEN #IMPLIED
+ name NMTOKENS #IMPLIED
+ mark NMTOKENS #IMPLIED
>
<!ELEMENT Abst %term;>
<!ATTLIST Abst
- name CDATA #IMPLIED
- mark NMTOKEN #IMPLIED
+ name NMTOKENS #IMPLIED
+ mark NMTOKENS #IMPLIED
>
<!ELEMENT Abbr %term;>
<!ATTLIST Abbr
- name CDATA #IMPLIED
- mark NMTOKEN #IMPLIED
+ name NMTOKENS #IMPLIED
+ mark NMTOKENS #IMPLIED
>
<!ELEMENT Void EMPTY>
<!ATTLIST Void
- name CDATA #IMPLIED
- mark NMTOKEN #IMPLIED
+ name NMTOKENS #IMPLIED
+ mark NMTOKENS #IMPLIED
>
<!-- ENVIRONMENT ENTRIES -->
<!ELEMENT ABST %term;>
<!ATTLIST ABST
- uri CDATA #REQUIRED
- name CDATA #IMPLIED
- mark NMTOKEN #IMPLIED
+ uri CDATA #REQUIRED
+ name NMTOKENS #IMPLIED
+ mark NMTOKENS #IMPLIED
>
<!ELEMENT ABBR %term;>
<!ATTLIST ABBR
- uri CDATA #REQUIRED
- name CDATA #IMPLIED
- mark NMTOKEN #IMPLIED
+ uri CDATA #REQUIRED
+ name NMTOKENS #IMPLIED
+ mark NMTOKENS #IMPLIED
>
<!-- ROOT -->
projects / helm.git / commitdiff