From a12fefc78e783661fbb638907252d2265c6af9dd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 24 Oct 2001 15:33:16 +0000 Subject: [PATCH] New procedure to create metadata committed and old procedure removed. The new procedure is based on ocaml code and builds metadata for both forward and backward pointers. The old one was based on a stylesheet. --- helm/metadata/create/Makefile | 14 - helm/metadata/create/mkindex.sh | 4 - helm/metadata/create/mywget.pl | 66 -- helm/metadata/create/split.pl | 26 - helm/metadata/create2/Makefile | 27 + helm/metadata/{create => create2}/fix_rdf.pl | 11 +- helm/metadata/create2/invert.pl | 31 + helm/metadata/create2/mk_forward/.cvsignore | 1 + helm/metadata/create2/mk_forward/Makefile | 48 + helm/metadata/create2/mk_forward/cic.ml | 162 +++ .../create2/mk_forward/cicMiniReduction.ml | 60 + .../create2/mk_forward/cicMiniReduction.mli | 26 + helm/metadata/create2/mk_forward/cicParser.ml | 95 ++ .../metadata/create2/mk_forward/cicParser.mli | 44 + .../metadata/create2/mk_forward/cicParser2.ml | 289 +++++ .../create2/mk_forward/cicParser2.mli | 57 + .../metadata/create2/mk_forward/cicParser3.ml | 565 +++++++++ .../create2/mk_forward/cicParser3.mli | 67 ++ .../create2/mk_forward/cicSubstitution.ml | 142 +++ .../create2/mk_forward/cicSubstitution.mli | 28 + .../metadata/create2/mk_forward/clientHTTP.ml | 60 + .../create2/mk_forward/clientHTTP.mli | 30 + .../create2/mk_forward/configuration.ml.in | 119 ++ .../create2/mk_forward/csc_pxp_reader.ml | 1008 +++++++++++++++++ .../metadata/create2/mk_forward/deannotate.ml | 98 ++ helm/metadata/create2/mk_forward/getter.ml | 63 ++ helm/metadata/create2/mk_forward/getter.mli | 53 + .../metadata/create2/mk_forward/mk_forward.ml | 392 +++++++ .../create2/mk_forward/pxpUriResolver.ml | 266 +++++ .../metadata/create2/mk_forward/uriManager.ml | 139 +++ .../create2/mk_forward/uriManager.mli | 51 + helm/metadata/create2/mk_forward/xml.ml | 101 ++ helm/metadata/create2/mk_forward/xml.mli | 60 + helm/metadata/create2/mkindex.sh | 4 + helm/metadata/create2/touch/.cvsignore | 1 + helm/metadata/create2/touch/Makefile | 46 + helm/metadata/create2/touch/cic.ml | 162 +++ helm/metadata/create2/touch/cicParser.ml | 95 ++ helm/metadata/create2/touch/cicParser.mli | 44 + helm/metadata/create2/touch/cicParser2.ml | 289 +++++ helm/metadata/create2/touch/cicParser2.mli | 57 + helm/metadata/create2/touch/cicParser3.ml | 565 +++++++++ helm/metadata/create2/touch/cicParser3.mli | 67 ++ helm/metadata/create2/touch/clientHTTP.ml | 60 + helm/metadata/create2/touch/clientHTTP.mli | 30 + .../create2/touch/configuration.ml.in | 117 ++ helm/metadata/create2/touch/csc_pxp_reader.ml | 1008 +++++++++++++++++ helm/metadata/create2/touch/deannotate.ml | 98 ++ helm/metadata/create2/touch/getter.ml | 63 ++ helm/metadata/create2/touch/getter.mli | 53 + helm/metadata/create2/touch/pxpUriResolver.ml | 266 +++++ helm/metadata/create2/touch/touch.ml | 137 +++ helm/metadata/create2/touch/uriManager.ml | 139 +++ helm/metadata/create2/touch/uriManager.mli | 51 + .../{create => create2}/uris_of_filenames.pl | 4 +- helm/metadata/xslt/occurrences.xsl | 554 --------- 56 files changed, 7443 insertions(+), 670 deletions(-) delete mode 100644 helm/metadata/create/Makefile delete mode 100755 helm/metadata/create/mkindex.sh delete mode 100755 helm/metadata/create/mywget.pl delete mode 100755 helm/metadata/create/split.pl create mode 100644 helm/metadata/create2/Makefile rename helm/metadata/{create => create2}/fix_rdf.pl (61%) create mode 100755 helm/metadata/create2/invert.pl create mode 100644 helm/metadata/create2/mk_forward/.cvsignore create mode 100644 helm/metadata/create2/mk_forward/Makefile create mode 100644 helm/metadata/create2/mk_forward/cic.ml create mode 100644 helm/metadata/create2/mk_forward/cicMiniReduction.ml create mode 100644 helm/metadata/create2/mk_forward/cicMiniReduction.mli create mode 100644 helm/metadata/create2/mk_forward/cicParser.ml create mode 100644 helm/metadata/create2/mk_forward/cicParser.mli create mode 100644 helm/metadata/create2/mk_forward/cicParser2.ml create mode 100644 helm/metadata/create2/mk_forward/cicParser2.mli create mode 100644 helm/metadata/create2/mk_forward/cicParser3.ml create mode 100644 helm/metadata/create2/mk_forward/cicParser3.mli create mode 100644 helm/metadata/create2/mk_forward/cicSubstitution.ml create mode 100644 helm/metadata/create2/mk_forward/cicSubstitution.mli create mode 100644 helm/metadata/create2/mk_forward/clientHTTP.ml create mode 100644 helm/metadata/create2/mk_forward/clientHTTP.mli create mode 100644 helm/metadata/create2/mk_forward/configuration.ml.in create mode 100644 helm/metadata/create2/mk_forward/csc_pxp_reader.ml create mode 100644 helm/metadata/create2/mk_forward/deannotate.ml create mode 100644 helm/metadata/create2/mk_forward/getter.ml create mode 100644 helm/metadata/create2/mk_forward/getter.mli create mode 100644 helm/metadata/create2/mk_forward/mk_forward.ml create mode 100644 helm/metadata/create2/mk_forward/pxpUriResolver.ml create mode 100644 helm/metadata/create2/mk_forward/uriManager.ml create mode 100644 helm/metadata/create2/mk_forward/uriManager.mli create mode 100644 helm/metadata/create2/mk_forward/xml.ml create mode 100644 helm/metadata/create2/mk_forward/xml.mli create mode 100755 helm/metadata/create2/mkindex.sh create mode 100644 helm/metadata/create2/touch/.cvsignore create mode 100644 helm/metadata/create2/touch/Makefile create mode 100644 helm/metadata/create2/touch/cic.ml create mode 100644 helm/metadata/create2/touch/cicParser.ml create mode 100644 helm/metadata/create2/touch/cicParser.mli create mode 100644 helm/metadata/create2/touch/cicParser2.ml create mode 100644 helm/metadata/create2/touch/cicParser2.mli create mode 100644 helm/metadata/create2/touch/cicParser3.ml create mode 100644 helm/metadata/create2/touch/cicParser3.mli create mode 100644 helm/metadata/create2/touch/clientHTTP.ml create mode 100644 helm/metadata/create2/touch/clientHTTP.mli create mode 100644 helm/metadata/create2/touch/configuration.ml.in create mode 100644 helm/metadata/create2/touch/csc_pxp_reader.ml create mode 100644 helm/metadata/create2/touch/deannotate.ml create mode 100644 helm/metadata/create2/touch/getter.ml create mode 100644 helm/metadata/create2/touch/getter.mli create mode 100644 helm/metadata/create2/touch/pxpUriResolver.ml create mode 100644 helm/metadata/create2/touch/touch.ml create mode 100644 helm/metadata/create2/touch/uriManager.ml create mode 100644 helm/metadata/create2/touch/uriManager.mli rename helm/metadata/{create => create2}/uris_of_filenames.pl (56%) delete mode 100644 helm/metadata/xslt/occurrences.xsl diff --git a/helm/metadata/create/Makefile b/helm/metadata/create/Makefile deleted file mode 100644 index a8ce85cbb..000000000 --- a/helm/metadata/create/Makefile +++ /dev/null @@ -1,14 +0,0 @@ -marcello: - time for i in `cat pluto` ; do ./mywget.pl $$i ; done - -rdf: - find output -type f -exec ./split.pl {} \; - find rdf -type f -exec ./fix_rdf.pl {} \; - (cd rdf ; ../mkindex.sh) - -.PHONY: clean rdf clean-rdf -clean: - find output -type f -exec rm {} \; - -clean-rdf: - rm -rf rdf/* diff --git a/helm/metadata/create/mkindex.sh b/helm/metadata/create/mkindex.sh deleted file mode 100755 index 8c52a9276..000000000 --- a/helm/metadata/create/mkindex.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/bash - -echo `find . -name "*.xml"` | ../uris_of_filenames.pl > rdf_index.txt -echo `find . -name "*.xml.gz"` | ../uris_of_filenames.pl -gz >> rdf_index.txt diff --git a/helm/metadata/create/mywget.pl b/helm/metadata/create/mywget.pl deleted file mode 100755 index 2ffcde643..000000000 --- a/helm/metadata/create/mywget.pl +++ /dev/null @@ -1,66 +0,0 @@ -#!/usr/bin/perl - -# Copyright (C) 2000, HELM Team. -# -# This file is part of HELM, an Hypertextual, Electronic -# Library of Mathematics, developed at the Computer Science -# Department, University of Bologna, Italy. -# -# HELM is free software; you can redistribute it and/or -# modify it under the terms of the GNU General Public License -# as published by the Free Software Foundation; either version 2 -# of the License, or (at your option) any later version. -# -# HELM is distributed in the hope that it will be useful, -# but WITHOUT ANY WARRANTY; without even the implied warranty of -# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -# GNU General Public License for more details. -# -# You should have received a copy of the GNU General Public License -# along with HELM; if not, write to the Free Software -# Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. -# -# For details, see the HELM World-Wide-Web page, -# http://cs.unibo.it/helm/. - -#use strict; - -use HTTP::Daemon; -use HTTP::Status; -use HTTP::Request; -use LWP::UserAgent; -use DB_File; -use Compress::Zlib; -use URI::Escape; - -foreach $i (@ARGV) { - my $filename = $i; - $filename =~ s/\//./g; - open(FD,">output/$filename"); - -# my $url = "http://phd.cs.unibo.it:8080/helm/servlet/uwobo/apply?keys=pfi%2Creorder&xmluri=http%3A//phd.cs.unibo.it%3A8081/ls%3Fformat%3Dxml%26baseuri%3D$i¶m.uri=$i¶m.getterURL=http://phd.cs.unibo.it:8081/"; - -#my $url = "http://dotto.cs.unibo.it:8080/helm/servlet/uwobo/apply?keys=pfi%2Creorder&xmluri=http%3A//dotto.cs.unibo.it%3A8081/ls%3Fformat%3Dxml%26baseuri%3D$i¶m.uri=$i¶m.getterURL=http://dotto.cs.unibo.it:8081/"; - -my $url = "http://phd.cs.unibo.it:8080/helm/servlet/uwobo/apply?keys=occ&xmluri=http%3A//phd.cs.unibo.it%3A8081/getxml%3Furi%3D$i¶m.CICURI=$i"; - - print "Now processing $i...\n"; - print "$url\n"; - - my $time = time(); - my $ua = LWP::UserAgent->new; - my $request = HTTP::Request->new(GET => "$url"); - my $response = $ua->request($request, \&callback2); - $time = time() - $time; - print "Finished. Time elapsed: $time\n\n"; - - close(FD); -} - -exit; - -sub callback2 -{ - my ($data) = @_; - print FD $data; -} diff --git a/helm/metadata/create/split.pl b/helm/metadata/create/split.pl deleted file mode 100755 index 9b3a3746e..000000000 --- a/helm/metadata/create/split.pl +++ /dev/null @@ -1,26 +0,0 @@ -#!/usr/bin/perl - -foreach $inputfile (@ARGV) { - print "Now splitting file $inputfile\n"; - open(IN, "<$inputfile"); - while($line = ) { - if (not ($line =~ /^/)) { - if ($line =~ /^$/$1/; - $line =~ s/^cic:/rdf/; - $line =~ s/#xpointer\(1\/([^\/]*)\/([^\/]*)\)/,$1,$2/; - $line =~ s/#xpointer\(1\/([^\/]*)\)/,$1/; - $dir = $line; - $dir =~ s/\/[^\/]*$//; - close(OUT); - system("mkdir -p $dir"); - open(OUT, ">>$line"); - } else { - print OUT $line; - } - } - } - close(IN); -} -close(OUT); diff --git a/helm/metadata/create2/Makefile b/helm/metadata/create2/Makefile new file mode 100644 index 000000000..b1ce8e195 --- /dev/null +++ b/helm/metadata/create2/Makefile @@ -0,0 +1,27 @@ +all: + @echo Available targets: + @echo " forward, backward, compress, clean-forward, clean-backward" + +forward: + time for i in `cat pluto` ; do mk_forward/mk_forward.opt $$i ; done > log 2>&1 + (cd forward ; ../mkindex.sh forward) + +backward: + time for i in `cat pluto` ; do touch/touch.opt $$i ; done + find forward -type f -exec ./invert.pl {} \; + find backward -type f -exec ./fix_rdf.pl {} \; + (cd backward ; ../mkindex.sh backward) + +compress: + find forward -name "*.xml" -exec gzip {} \; + find backward -name "*.xml" -exec gzip {} \; + (cd forward ; ../mkindex.sh forward) + (cd backward ; ../mkindex.sh backward) + +clean-forward: + rm -rf forward/* + +clean-backward: + rm -rf backward/* + +.PHONY: all forward backward compress clean-forward clean-backward diff --git a/helm/metadata/create/fix_rdf.pl b/helm/metadata/create2/fix_rdf.pl similarity index 61% rename from helm/metadata/create/fix_rdf.pl rename to helm/metadata/create2/fix_rdf.pl index 070136bc0..cd3051f3f 100755 --- a/helm/metadata/create/fix_rdf.pl +++ b/helm/metadata/create2/fix_rdf.pl @@ -2,7 +2,7 @@ $filename = $uri = $ARGV[0]; $outputfile = $filename.".xml"; -$uri =~ s/^rdf/cic:/; +$uri =~ s/^backward/cic:/; $uri =~ s/(.*),([^,]*),([^,]*)/$1#xpointer(1\/$2\/$3)/; $uri =~ s/(.*),([^,]*)/$1#xpointer(1\/$2)/; @@ -10,8 +10,10 @@ print "Now processing file $filename\n"; open(HEADER,">>$outputfile"); print HEADER < - + + + + EOT close(HEADER); @@ -19,7 +21,8 @@ system("cat $filename >> $outputfile"); open(FOOTER,">>$outputfile"); print FOOTER < + + EOT close(FOOTER); diff --git a/helm/metadata/create2/invert.pl b/helm/metadata/create2/invert.pl new file mode 100755 index 000000000..5616177e8 --- /dev/null +++ b/helm/metadata/create2/invert.pl @@ -0,0 +1,31 @@ +#!/usr/bin/perl + +my $inputfile = $ARGV[0]; + +print "Now splitting file $inputfile\n"; +open(IN, "<$inputfile") or die "Error opening file $inputfile"; +$dummy = ; # +$dummy = ; # +$dummy = ; # +$where = ; # +chomp($where); +$where =~ s/^[^"]*"([^"]*)">$/$1/; +while(($line1 = ) && not ($line1 =~ /<\/h:Object>/)) { + $line2 = ; + $line3 = ; # + $uri = $line2; + chomp($uri); + $uri =~ s/^ *$/$1/; + $who = $uri; + $who =~ s/^cic:/backward/; + $who =~ s/#xpointer\(1\/([^\/]*)\/([^\/]*)\)/,$1,$2/; + $who =~ s/#xpointer\(1\/([^\/]*)\)/,$1/; + $line2 =~ s/\Q$uri\E/$where/; + + open(OUT, ">>$who") or die "Error opening file $who"; + print OUT " \n"; + print OUT $line2; + print OUT " \n"; + close(OUT); +} +close(IN); diff --git a/helm/metadata/create2/mk_forward/.cvsignore b/helm/metadata/create2/mk_forward/.cvsignore new file mode 100644 index 000000000..4f907d655 --- /dev/null +++ b/helm/metadata/create2/mk_forward/.cvsignore @@ -0,0 +1 @@ +*.cmi *.cmo *.cmx .depend mk_forward mk_forward.opt configuration.ml diff --git a/helm/metadata/create2/mk_forward/Makefile b/helm/metadata/create2/mk_forward/Makefile new file mode 100644 index 000000000..d8bcc9bd3 --- /dev/null +++ b/helm/metadata/create2/mk_forward/Makefile @@ -0,0 +1,48 @@ +OCAMLOPTIONS = -package netstring -package netclient -package pxp + +OCAMLDEP = ocamldep +OCAMLFIND = ocamlfind +OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) +OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS) + +all: mk_forward +opt: mk_forward.opt + +DEPOBJS = xml.ml xml.mli csc_pxp_reader.ml configuration.ml \ + clientHTTP.ml clientHTTP.mli cic.ml deannotate.ml \ + uriManager.ml uriManager.mli getter.ml getter.mli \ + pxpUriResolver.ml cicParser3.ml cicParser3.mli \ + cicParser2.ml cicParser2.mli cicParser.ml \ + cicParser.mli cicSubstitution.ml cicSubstitution.mli \ + cicMiniReduction.ml cicMiniReduction.mli mk_forward.ml + +MKFORWARDOBJS = xml.cmo csc_pxp_reader.cmo configuration.cmo \ + clientHTTP.cmo cic.cmo deannotate.cmo \ + uriManager.cmo getter.cmo pxpUriResolver.ml \ + cicParser3.cmo cicParser2.cmo cicParser.cmo \ + cicSubstitution.cmo cicMiniReduction.cmo \ + mk_forward.cmo + +depend: + $(OCAMLDEP) $(DEPOBJS) > .depend + +mk_forward: $(MKFORWARDOBJS) + $(OCAMLC) -linkpkg -o mk_forward $(MKFORWARDOBJS) + +mk_forward.opt: $(MKFORWARDOBJS:.cmo=.cmx) + $(OCAMLOPT) -linkpkg -o mk_forward.opt $(MKFORWARDOBJS:.cmo=.cmx) + +.SUFFIXES: .ml .mli .cmo .cmi .cmx +.ml.cmo: + $(OCAMLC) -c $< +.mli.cmi: + $(OCAMLC) -c $< +.ml.cmx: + $(OCAMLOPT) -c $< + +clean: + rm -f *.cm[iox] *.o mk_forward mk_forward.opt + +.PHONY: clean + +include .depend diff --git a/helm/metadata/create2/mk_forward/cic.ml b/helm/metadata/create2/mk_forward/cic.ml new file mode 100644 index 000000000..8c08b0075 --- /dev/null +++ b/helm/metadata/create2/mk_forward/cic.ml @@ -0,0 +1,162 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 14/06/2000 *) +(* *) +(* This module defines the internal representation of the objects (variables, *) +(* blocks of (co)inductive definitions and constants) and the terms of cic *) +(* *) +(******************************************************************************) + +(* STUFF TO MANAGE IDENTIFIERS *) +type id = string (* the abstract type of the (annotated) node identifiers *) +type anntarget = + Object of annobj + | Term of annterm + +(* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *) +and sort = + Prop + | Set + | Type +and name = + Name of string + | Anonimous +and term = + Rel of int (* DeBrujin index *) + | Var of UriManager.uri (* uri *) + | Meta of int (* numeric id *) + | Sort of sort (* sort *) + | Implicit (* *) + | Cast of term * term (* value, type *) + | Prod of name * term * term (* binder, source, target *) + | Lambda of name * term * term (* binder, source, target *) + | LetIn of name * term * term (* binder, term, target *) + | Appl of term list (* arguments *) + | Const of UriManager.uri * int (* uri, number of cookings*) + | Abst of UriManager.uri (* uri *) + | MutInd of UriManager.uri * int * int (* uri, cookingsno, typeno*) + | MutConstruct of UriManager.uri * int * (* uri, cookingsno, *) + int * int (* typeno, consno *) + (*CSC: serve cookingsno?*) + | MutCase of UriManager.uri * int * (* ind. uri, cookingsno, *) + int * (* ind. typeno, *) + term * term * (* outtype, ind. term *) + term list (* patterns *) + | Fix of int * inductiveFun list (* funno, functions *) + | CoFix of int * coInductiveFun list (* funno, functions *) +and obj = + Definition of string * term * term * (* id, value, type, *) + (int * UriManager.uri list) list (* parameters *) + | Axiom of string * term * + (int * UriManager.uri list) list (* id, type, parameters *) + | Variable of string * term option * term (* name, body, type *) + | CurrentProof of string * (int * term) list * (* name, conjectures, *) + term * term (* value, type *) + | InductiveDefinition of inductiveType list * (* inductive types, *) + (int * UriManager.uri list) list * int (* parameters, n ind. pars *) +and inductiveType = + string * bool * term * (* typename, inductive, arity *) + constructor list (* constructors *) +and constructor = + string * term * bool list option ref (* id, type, really recursive *) +and inductiveFun = + string * int * term * term (* name, ind. index, type, body *) +and coInductiveFun = + string * term * term (* name, type, body *) + +and annterm = + ARel of id * annotation option ref * + int * string option (* DeBrujin index, binder *) + | AVar of id * annotation option ref * + UriManager.uri (* uri *) + | AMeta of id * annotation option ref * int (* numeric id *) + | ASort of id * annotation option ref * sort (* sort *) + | AImplicit of id * annotation option ref (* *) + | ACast of id * annotation option ref * + annterm * annterm (* value, type *) + | AProd of id * annotation option ref * + name * annterm * annterm (* binder, source, target *) + | ALambda of id * annotation option ref * + name * annterm * annterm (* binder, source, target *) + | ALetIn of id * annotation option ref * + name * annterm * annterm (* binder, term, target *) + | AAppl of id * annotation option ref * + annterm list (* arguments *) + | AConst of id * annotation option ref * + UriManager.uri * int (* uri, number of cookings*) + | AAbst of id * annotation option ref * + UriManager.uri (* uri *) + | AMutInd of id * annotation option ref * + UriManager.uri * int * int (* uri, cookingsno, typeno*) + | AMutConstruct of id * annotation option ref * + UriManager.uri * int * (* uri, cookingsno, *) + int * int (* typeno, consno *) + (*CSC: serve cookingsno?*) + | AMutCase of id * annotation option ref * + UriManager.uri * int * (* ind. uri, cookingsno *) + int * (* ind. typeno, *) + annterm * annterm * (* outtype, ind. term *) + annterm list (* patterns *) + | AFix of id * annotation option ref * + int * anninductiveFun list (* funno, functions *) + | ACoFix of id * annotation option ref * + int * anncoInductiveFun list (* funno, functions *) +and annobj = + ADefinition of id * annotation option ref * + string * (* id, *) + annterm * annterm * (* value, type, *) + (int * UriManager.uri list) list exactness (* parameters *) + | AAxiom of id * annotation option ref * + string * annterm * (* id, type *) + (int * UriManager.uri list) list (* parameters *) + | AVariable of id * annotation option ref * + string * annterm option * annterm (* name, body, type *) + | ACurrentProof of id * annotation option ref * + string * (int * annterm) list * (* name, conjectures, *) + annterm * annterm (* value, type *) + | AInductiveDefinition of id * + annotation option ref * anninductiveType list * (* inductive types , *) + (int * UriManager.uri list) list * int (* parameters,n ind. pars*) +and anninductiveType = + string * bool * annterm * (* typename, inductive, arity *) + annconstructor list (* constructors *) +and annconstructor = + string * annterm * bool list option ref (* id, type, really recursive *) +and anninductiveFun = + string * int * annterm * annterm (* name, ind. index, type, body *) +and anncoInductiveFun = + string * annterm * annterm (* name, type, body *) +and annotation = + string +and 'a exactness = + Possible of 'a (* an approximation to something *) + | Actual of 'a (* something *) +;; diff --git a/helm/metadata/create2/mk_forward/cicMiniReduction.ml b/helm/metadata/create2/mk_forward/cicMiniReduction.ml new file mode 100644 index 000000000..cb5875f73 --- /dev/null +++ b/helm/metadata/create2/mk_forward/cicMiniReduction.ml @@ -0,0 +1,60 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +let rec letin_nf = + let module C = Cic in + function + C.Rel _ as t -> t + | C.Var _ as t -> t + | C.Meta _ as t -> t + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (letin_nf te, letin_nf ty) + | C.Prod (n,s,t) -> C.Prod (n, letin_nf s, letin_nf t) + | C.Lambda (n,s,t) -> C.Lambda (n, letin_nf s, letin_nf t) + | C.LetIn (n,s,t) -> CicSubstitution.subst (letin_nf s) t + | C.Appl l -> C.Appl (List.map letin_nf l) + | C.Const _ as t -> t + | C.Abst _ as t -> t + | C.MutInd _ as t -> t + | C.MutConstruct _ as t -> t + | C.MutCase (sp,cookingsno,i,outt,t,pl) -> + C.MutCase (sp,cookingsno,i,letin_nf outt, letin_nf t, + List.map letin_nf pl) + | C.Fix (i,fl) -> + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, letin_nf ty, letin_nf bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, letin_nf ty, letin_nf bo)) + fl + in + C.CoFix (i, substitutedfl) +;; diff --git a/helm/metadata/create2/mk_forward/cicMiniReduction.mli b/helm/metadata/create2/mk_forward/cicMiniReduction.mli new file mode 100644 index 000000000..c923c6acf --- /dev/null +++ b/helm/metadata/create2/mk_forward/cicMiniReduction.mli @@ -0,0 +1,26 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val letin_nf : Cic.term -> Cic.term diff --git a/helm/metadata/create2/mk_forward/cicParser.ml b/helm/metadata/create2/mk_forward/cicParser.ml new file mode 100644 index 000000000..bf75243ec --- /dev/null +++ b/helm/metadata/create2/mk_forward/cicParser.ml @@ -0,0 +1,95 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This is the main (top level) module of a parser for cic objects from xml *) +(* files to the internal representation. It uses the modules cicParser2 *) +(* (objects level) and cicParser3 (terms level) *) +(* *) +(******************************************************************************) + +exception Warnings;; + +class warner = + object + method warn w = + print_endline ("WARNING: " ^ w) ; + (raise Warnings : unit) + end +;; + +exception EmptyUri;; + +(* given an uri u it returns the list of tokens of the base uri of u *) +(* e.g.: token_of_uri "cic:/a/b/c/d.xml" returns ["a" ; "b" ; "c"] *) +let tokens_of_uri uri = + let uri' = UriManager.string_of_uri uri in + let rec chop_list = + function + [] -> raise EmptyUri + | he::[fn] -> [he] + | he::tl -> he::(chop_list tl) + in + let trimmed_uri = Str.replace_first (Str.regexp "cic:") "" uri' in + let list_of_tokens = Str.split (Str.regexp "/") trimmed_uri in + chop_list list_of_tokens +;; + +(* given the filename of an xml file of a cic object it returns its internal *) +(* representation. process_annotations is true if the annotations do really *) +(* matter *) +let term_of_xml filename uri process_annotations = + let module Y = Pxp_yacc in + try + let d = + (* sets the current base uri to resolve relative URIs *) + CicParser3.current_sp := tokens_of_uri uri ; + CicParser3.current_uri := uri ; + CicParser3.process_annotations := process_annotations ; + CicParser3.ids_to_targets := + if process_annotations then Some (Hashtbl.create 500) else None ; + let config = {Y.default_config with Y.warner = new warner} in + Y.parse_document_entity config +(*PXP (Y.ExtID (Pxp_types.System filename, + new Pxp_reader.resolve_as_file ~url_of_id ())) +*) (PxpUriResolver.from_file filename) + CicParser3.domspec + in + let ids_to_targets = !CicParser3.ids_to_targets in + let res = (CicParser2.get_term d#root, ids_to_targets) in + CicParser3.ids_to_targets := None ; (* let's help the GC *) + res + with + e -> + print_endline ("Filename: " ^ filename ^ "\nException: ") ; + print_endline (Pxp_types.string_of_exn e) ; + raise e +;; diff --git a/helm/metadata/create2/mk_forward/cicParser.mli b/helm/metadata/create2/mk_forward/cicParser.mli new file mode 100644 index 000000000..0078f6f33 --- /dev/null +++ b/helm/metadata/create2/mk_forward/cicParser.mli @@ -0,0 +1,44 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 22/03/2000 *) +(* *) +(* This is the main (top level) module of a parser for cic objects from xml *) +(* files to the internal representation. It uses the modules cicParser2 *) +(* (objects level) and cicParser3 (terms level) *) +(* *) +(******************************************************************************) + +(* given the filename of an xml file of a cic object and it's uri, it returns *) +(* its internal annotated representation. The boolean is set to true if the *) +(* annotations do really matter *) +val term_of_xml : + string -> UriManager.uri -> bool -> + Cic.annobj * (Cic.id, Cic.anntarget) Hashtbl.t option diff --git a/helm/metadata/create2/mk_forward/cicParser2.ml b/helm/metadata/create2/mk_forward/cicParser2.ml new file mode 100644 index 000000000..562f79bba --- /dev/null +++ b/helm/metadata/create2/mk_forward/cicParser2.ml @@ -0,0 +1,289 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This module is the objects level of a parser for cic objects from xml *) +(* files to the internal representation. It uses the module cicParser3 *) +(* cicParser3 (terms level) and it is used only through cicParser2 (top *) +(* level). *) +(* *) +(******************************************************************************) + +exception IllFormedXml of int;; +exception NotImplemented;; + +(* Utility functions that transform a Pxp attribute into something useful *) + +(* mk_absolute_uris "n1: v1 ... vn n2 : u1 ... un ...." *) +(* returns [(n1,[absolute_uri_for_v1 ; ... ; absolute_uri_for_vn]) ; (n2,...) *) +let mk_absolute_uris s = + let l = (Str.split (Str.regexp ":") s) in + let absolute_of_relative n v = + let module P3 = CicParser3 in + let rec mkburi = + function + (0,_) -> "/" + | (n,he::tl) when n > 0 -> + "/" ^ he ^ mkburi (n - 1, tl) + | _ -> raise (IllFormedXml 12) + in + let m = List.length !P3.current_sp - (int_of_string n) in + let buri = mkburi (m, !P3.current_sp) in + UriManager.uri_of_string ("cic:" ^ buri ^ v ^ ".var") + in + let rec absolutize = + function + [] -> [] + | [no ; vs] -> + let vars = (Str.split (Str.regexp " ") vs) in + [(int_of_string no, List.map (absolute_of_relative no) vars)] + | no::vs::tl -> + let vars = (Str.split (Str.regexp " ") vs) in + let rec add_prefix = + function + [no2] -> ([], no2) + | he::tl -> + let (pvars, no2) = add_prefix tl in + ((absolute_of_relative no he)::pvars, no2) + | _ -> raise (IllFormedXml 11) + in + let (pvars, no2) = add_prefix vars in + (int_of_string no, pvars)::(absolutize (no2::tl)) + | _ -> raise (IllFormedXml 10) + in + (* last parameter must be applied first *) + absolutize l +;; + +let option_uri_list_of_attr a1 a2 = + let module T = Pxp_types in + let parameters = + match a1 with + T.Value s -> mk_absolute_uris s + | _ -> raise (IllFormedXml 0) + in + match a2 with + T.Value "POSSIBLE" -> Cic.Possible parameters + | T.Implied_value -> Cic.Actual parameters + | _ -> raise (IllFormedXml 0) +;; + +let uri_list_of_attr a = + let module T = Pxp_types in + match a with + T.Value s -> mk_absolute_uris s + | _ -> raise (IllFormedXml 0) +;; + +let string_of_attr a = + let module T = Pxp_types in + match a with + T.Value s -> s + | _ -> raise (IllFormedXml 0) +;; + +let int_of_attr a = + int_of_string (string_of_attr a) +;; + +let bool_of_attr a = + bool_of_string (string_of_attr a) +;; + +(* Other utility functions *) + +let get_content n = + match n#sub_nodes with + [ t ] -> t + | _ -> raise (IllFormedXml 1) +;; + +let register_id id node = + if !CicParser3.process_annotations then + match !CicParser3.ids_to_targets with + None -> assert false + | Some ids_to_targets -> + Hashtbl.add ids_to_targets id (Cic.Object node) +;; + +(* Functions that, given the list of sons of a node of the cic dom (objects *) +(* level), retrieve the internal representation associated to the node. *) +(* Everytime a cic term subtree is found, it is translated to the internal *) +(* representation using the method to_cic_term defined in cicParser3. *) +(* Each function raise IllFormedXml if something goes wrong, but this should *) +(* be impossible due to the presence of the dtd *) +(* The functions should really be obvious looking at their name and the cic *) +(* dtd *) + +(* called when a CurrentProof is found *) +let get_conjs_value_type l = + let rec rget (c, v, t) l = + let module D = Pxp_document in + match l with + [] -> (c, v, t) + | conj::tl when conj#node_type = D.T_element "Conjecture" -> + let no = int_of_attr (conj#attribute "no") + and typ = (get_content conj)#extension#to_cic_term in + rget ((no, typ)::c, v, t) tl + | value::tl when value#node_type = D.T_element "body" -> + let v' = (get_content value)#extension#to_cic_term in + (match v with + None -> rget (c, Some v', t) tl + | _ -> raise (IllFormedXml 2) + ) + | typ::tl when typ#node_type = D.T_element "type" -> + let t' = (get_content typ)#extension#to_cic_term in + (match t with + None -> rget (c, v, Some t') tl + | _ -> raise (IllFormedXml 3) + ) + | _ -> raise (IllFormedXml 4) + in + match rget ([], None, None) l with + (c, Some v, Some t) -> (c, v, t) + | _ -> raise (IllFormedXml 5) +;; + +(* used only by get_inductive_types; called one time for each inductive *) +(* definitions in a block of inductive definitions *) +let get_names_arity_constructors l = + let rec rget (a,c) l = + let module D = Pxp_document in + match l with + [] -> (a, c) + | arity::tl when arity#node_type = D.T_element "arity" -> + let a' = (get_content arity)#extension#to_cic_term in + rget (Some a',c) tl + | con::tl when con#node_type = D.T_element "Constructor" -> + let id = string_of_attr (con#attribute "name") + and ty = (get_content con)#extension#to_cic_term in + rget (a,(id,ty,ref None)::c) tl + | _ -> raise (IllFormedXml 9) + in + match rget (None,[]) l with + (Some a, c) -> (a, List.rev c) + | _ -> raise (IllFormedXml 8) +;; + +(* called when an InductiveDefinition is found *) +let rec get_inductive_types = + function + [] -> [] + | he::tl -> + let tyname = string_of_attr (he#attribute "name") + and inductive = bool_of_attr (he#attribute "inductive") + and (arity,cons) = + get_names_arity_constructors (he#sub_nodes) + in + (tyname,inductive,arity,cons)::(get_inductive_types tl) (*CSC 0 a caso *) +;; + +(* This is the main function and also the only one used directly from *) +(* cicParser. Given the root of the dom tree, it returns the internal *) +(* representation of the cic object described in the tree *) +(* It uses the previous functions and the to_cic_term method defined *) +(* in cicParser3 (used for subtrees that encode cic terms) *) +let rec get_term n = + let module D = Pxp_document in + let module C = Cic in + let ntype = n # node_type in + match ntype with + D.T_element "Definition" -> + let id = string_of_attr (n # attribute "name") + and params = + option_uri_list_of_attr (n#attribute "params") (n#attribute "paramMode") + and (value, typ) = + let sons = n#sub_nodes in + match sons with + [v ; t] when + v#node_type = D.T_element "body" && + t#node_type = D.T_element "type" -> + let v' = get_content v + and t' = get_content t in + (v'#extension#to_cic_term, t'#extension#to_cic_term) + | _ -> raise (IllFormedXml 6) + and xid = string_of_attr (n#attribute "id") in + let res = C.ADefinition (xid, ref None, id, value, typ, params) in + register_id xid res ; + res + | D.T_element "Axiom" -> + let id = string_of_attr (n # attribute "name") + and params = uri_list_of_attr (n # attribute "params") + and typ = + (get_content (get_content n))#extension#to_cic_term + and xid = string_of_attr (n#attribute "id") in + let res = C.AAxiom (xid, ref None, id, typ, params) in + register_id xid res ; + res + | D.T_element "CurrentProof" -> + let name = string_of_attr (n#attribute "name") + and xid = string_of_attr (n#attribute "id") in + let sons = n#sub_nodes in + let (conjs, value, typ) = get_conjs_value_type sons in + let res = C.ACurrentProof (xid, ref None, name, conjs, value, typ) in + register_id xid res ; + res + | D.T_element "InductiveDefinition" -> + let sons = n#sub_nodes + and xid = string_of_attr (n#attribute "id") in + let inductiveTypes = get_inductive_types sons + and params = uri_list_of_attr (n#attribute "params") + and nparams = int_of_attr (n#attribute "noParams") in + let res = + C.AInductiveDefinition (xid, ref None, inductiveTypes, params, nparams) + in + register_id xid res ; + res + | D.T_element "Variable" -> + let name = string_of_attr (n#attribute "name") + and xid = string_of_attr (n#attribute "id") + and (body, typ) = + let sons = n#sub_nodes in + match sons with + [b ; t] when + b#node_type = D.T_element "body" && + t#node_type = D.T_element "type" -> + let b' = get_content b + and t' = get_content t in + (Some (b'#extension#to_cic_term), t'#extension#to_cic_term) + | [t] when t#node_type = D.T_element "type" -> + let t' = get_content t in + (None, t'#extension#to_cic_term) + | _ -> raise (IllFormedXml 6) + in + let res = C.AVariable (xid,ref None,name,body,typ) in + register_id xid res ; + res + | D.T_element _ + | D.T_data + | _ -> + raise (IllFormedXml 7) +;; diff --git a/helm/metadata/create2/mk_forward/cicParser2.mli b/helm/metadata/create2/mk_forward/cicParser2.mli new file mode 100644 index 000000000..be0a00054 --- /dev/null +++ b/helm/metadata/create2/mk_forward/cicParser2.mli @@ -0,0 +1,57 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This module is the objects level of a parser for cic objects from xml *) +(* files to the internal representation. It uses the module cicParser3 *) +(* cicParser3 (terms level) and it is used only through cicParser2 (top *) +(* level). *) +(* *) +(******************************************************************************) + +exception IllFormedXml of int +exception NotImplemented + +(* This is the main function and also the only one used directly from *) +(* cicParser. Given the root of the dom tree, it returns the internal *) +(* representation of the cic object described in the tree *) +(* It uses the previous functions and the to_cic_term method defined *) +(* in cicParser3 (used for subtrees that encode cic terms) *) +val get_term : + < attribute : string -> Pxp_types.att_value; + node_type : Pxp_document.node_type; + sub_nodes : < attribute : string -> Pxp_types.att_value; + node_type : Pxp_document.node_type; + sub_nodes : CicParser3.cic_term Pxp_document.node list; + .. > + list; + .. > -> + Cic.annobj diff --git a/helm/metadata/create2/mk_forward/cicParser3.ml b/helm/metadata/create2/mk_forward/cicParser3.ml new file mode 100644 index 000000000..ff356b13e --- /dev/null +++ b/helm/metadata/create2/mk_forward/cicParser3.ml @@ -0,0 +1,565 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This module is the terms level of a parser for cic objects from xml *) +(* files to the internal representation. It is used by the module cicParser2 *) +(* (objects level). It defines an extension of the standard dom using the *) +(* object-oriented extension machinery of markup: an object with a method *) +(* to_cic_term that returns the internal representation of the subtree is *) +(* added to each node of the dom tree *) +(* *) +(******************************************************************************) + +exception IllFormedXml of int;; + +(* The hashtable from the current identifiers to the object or the terms *) +let ids_to_targets = ref None;; + +(* The list of tokens of the current section path. *) +(* Used to resolve relative URIs *) +let current_sp = ref [];; + +(* The uri of the object been parsed *) +let current_uri = ref (UriManager.uri_of_string "cic:/.xml");; + +(* True if annotation really matter *) +let process_annotations = ref false;; + +(* Utility functions to map a markup attribute to something useful *) + +let cic_attr_of_xml_attr = + function + Pxp_types.Value s -> Cic.Name s + | Pxp_types.Implied_value -> Cic.Anonimous + | _ -> raise (IllFormedXml 1) + +let cic_sort_of_xml_attr = + function + Pxp_types.Value "Prop" -> Cic.Prop + | Pxp_types.Value "Set" -> Cic.Set + | Pxp_types.Value "Type" -> Cic.Type + | _ -> raise (IllFormedXml 2) + +let int_of_xml_attr = + function + Pxp_types.Value n -> int_of_string n + | _ -> raise (IllFormedXml 3) + +let uri_of_xml_attr = + function + Pxp_types.Value s -> UriManager.uri_of_string s + | _ -> raise (IllFormedXml 4) + +let string_of_xml_attr = + function + Pxp_types.Value s -> s + | _ -> raise (IllFormedXml 5) + +let binder_of_xml_attr = + function + Pxp_types.Value s -> if !process_annotations then Some s else None + | _ -> raise (IllFormedXml 17) +;; + +let register_id id node = + if !process_annotations then + match !ids_to_targets with + None -> assert false + | Some ids_to_targets -> + Hashtbl.add ids_to_targets id (Cic.Term node) +;; + +(* the "interface" of the class linked to each node of the dom tree *) + +class virtual cic_term = + object (self) + + (* fields and methods ever required by markup *) + val mutable node = (None : cic_term Pxp_document.node option) + + method clone = {< >} + method node = + match node with + None -> + assert false + | Some n -> n + method set_node n = + node <- Some n + + (* a method that returns the internal representation of the tree (term) *) + (* rooted in this node *) + method virtual to_cic_term : Cic.annterm + end +;; + +(* the class of the objects linked to nodes that are not roots of cic terms *) +class eltype_not_of_cic = + object (self) + + inherit cic_term + + method to_cic_term = raise (IllFormedXml 6) + end +;; + +(* the class of the objects linked to nodes whose content is a cic term *) +(* (syntactic sugar xml entities) e.g. ... *) +class eltype_transparent = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + match n#sub_nodes with + [ t ] -> t#extension#to_cic_term + | _ -> raise (IllFormedXml 7) + end +;; + +(* A class for each cic node type *) + +class eltype_fix = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let nofun = int_of_xml_attr (n#attribute "noFun") + and id = string_of_xml_attr (n#attribute "id") + and functions = + let sons = n#sub_nodes in + List.map + (function + f when f#node_type = Pxp_document.T_element "FixFunction" -> + let name = string_of_xml_attr (f#attribute "name") + and recindex = int_of_xml_attr (f#attribute "recIndex") + and (ty, body) = + match f#sub_nodes with + [t ; b] when + t#node_type = Pxp_document.T_element "type" && + b#node_type = Pxp_document.T_element "body" -> + (t#extension#to_cic_term, b#extension#to_cic_term) + | _ -> raise (IllFormedXml 14) + in + (name, recindex, ty, body) + | _ -> raise (IllFormedXml 13) + ) sons + in + let res = Cic.AFix (id, ref None, nofun, functions) in + register_id id res ; + res + end +;; + +class eltype_cofix = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let nofun = int_of_xml_attr (n#attribute "noFun") + and id = string_of_xml_attr (n#attribute "id") + and functions = + let sons = n#sub_nodes in + List.map + (function + f when f#node_type = Pxp_document.T_element "CofixFunction" -> + let name = string_of_xml_attr (f#attribute "name") + and (ty, body) = + match f#sub_nodes with + [t ; b] when + t#node_type = Pxp_document.T_element "type" && + b#node_type = Pxp_document.T_element "body" -> + (t#extension#to_cic_term, b#extension#to_cic_term) + | _ -> raise (IllFormedXml 16) + in + (name, ty, body) + | _ -> raise (IllFormedXml 15) + ) sons + in + let res = Cic.ACoFix (id, ref None, nofun, functions) in + register_id id res ; + res + end +;; + +class eltype_implicit = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let id = string_of_xml_attr (n#attribute "id") in + let res = Cic.AImplicit (id, ref None) in + register_id id res ; + res + end +;; + +class eltype_rel = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let value = int_of_xml_attr (n#attribute "value") + and binder = binder_of_xml_attr (n#attribute "binder") + and id = string_of_xml_attr (n#attribute "id") in + let res = Cic.ARel (id,ref None,value,binder) in + register_id id res ; + res + end +;; + +class eltype_meta = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let value = int_of_xml_attr (n#attribute "no") + and id = string_of_xml_attr (n#attribute "id") in + let res = Cic.AMeta (id,ref None,value) in + register_id id res ; + res + end +;; + +class eltype_var = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let name = string_of_xml_attr (n#attribute "relUri") + and xid = string_of_xml_attr (n#attribute "id") in + match Str.split (Str.regexp ",") name with + [index; id] -> + let get_prefix n = + let rec aux = + function + (0,_) -> "/" + | (n,he::tl) when n > 0 -> "/" ^ he ^ aux (n - 1, tl) + | _ -> raise (IllFormedXml 19) + in + aux (List.length !current_sp - n,!current_sp) + in + let res = + Cic.AVar + (xid,ref None, + (UriManager.uri_of_string + ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var")) + ) + in + register_id id res ; + res + | _ -> raise (IllFormedXml 18) + end +;; + +class eltype_apply = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let children = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + if List.length children < 2 then raise (IllFormedXml 8) + else + let res = + Cic.AAppl + (id,ref None,List.map (fun x -> x#extension#to_cic_term) children) + in + register_id id res ; + res + end +;; + +class eltype_cast = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let sons = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + match sons with + [te ; ty] when + te#node_type = Pxp_document.T_element "term" && + ty#node_type = Pxp_document.T_element "type" -> + let term = te#extension#to_cic_term + and typ = ty#extension#to_cic_term in + let res = Cic.ACast (id,ref None,term,typ) in + register_id id res ; + res + | _ -> raise (IllFormedXml 9) + end +;; + +class eltype_sort = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let sort = cic_sort_of_xml_attr (n#attribute "value") + and id = string_of_xml_attr (n#attribute "id") in + let res = Cic.ASort (id,ref None,sort) in + register_id id res ; + res + end +;; + +class eltype_abst = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let value = uri_of_xml_attr (n#attribute "uri") + and id = string_of_xml_attr (n#attribute "id") in + let res = Cic.AAbst (id,ref None,value) in + register_id id res ; + res + end +;; + +class eltype_const = + object (self) + + inherit cic_term + + method to_cic_term = + let module U = UriManager in + let n = self#node in + let value = uri_of_xml_attr (n#attribute "uri") + and id = string_of_xml_attr (n#attribute "id") in + let res = + Cic.AConst (id,ref None,value, U.relative_depth !current_uri value 0) + in + register_id id res ; + res + end +;; + +class eltype_mutind = + object (self) + + inherit cic_term + + method to_cic_term = + let module U = UriManager in + let n = self#node in + let name = uri_of_xml_attr (n#attribute "uri") + and noType = int_of_xml_attr (n#attribute "noType") + and id = string_of_xml_attr (n#attribute "id") in + let res = + Cic.AMutInd + (id,ref None,name, U.relative_depth !current_uri name 0, noType) + in + register_id id res ; + res + end +;; + +class eltype_mutconstruct = + object (self) + + inherit cic_term + + method to_cic_term = + let module U = UriManager in + let n = self#node in + let name = uri_of_xml_attr (n#attribute "uri") + and noType = int_of_xml_attr (n#attribute "noType") + and noConstr = int_of_xml_attr (n#attribute "noConstr") + and id = string_of_xml_attr (n#attribute "id") in + let res = + Cic.AMutConstruct + (id, ref None, name, U.relative_depth !current_uri name 0, + noType, noConstr) + in + register_id id res ; + res + end +;; + +class eltype_prod = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let sons = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + match sons with + [s ; t] when + s#node_type = Pxp_document.T_element "source" && + t#node_type = Pxp_document.T_element "target" -> + let name = cic_attr_of_xml_attr (t#attribute "binder") + and source = s#extension#to_cic_term + and target = t#extension#to_cic_term in + let res = Cic.AProd (id,ref None,name,source,target) in + register_id id res ; + res + | _ -> raise (IllFormedXml 10) + end +;; + +class eltype_mutcase = + object (self) + + inherit cic_term + + method to_cic_term = + let module U = UriManager in + let n = self#node in + let sons = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + match sons with + ty::te::patterns when + ty#node_type = Pxp_document.T_element "patternsType" && + te#node_type = Pxp_document.T_element "inductiveTerm" -> + let ci = uri_of_xml_attr (n#attribute "uriType") + and typeno = int_of_xml_attr (n#attribute "noType") + and inductiveType = ty#extension#to_cic_term + and inductiveTerm = te#extension#to_cic_term + and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns + in + let res = + Cic.AMutCase (id,ref None,ci,U.relative_depth !current_uri ci 0, + typeno,inductiveType,inductiveTerm,lpattern) + in + register_id id res ; + res + | _ -> raise (IllFormedXml 11) + end +;; + +class eltype_lambda = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let sons = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + match sons with + [s ; t] when + s#node_type = Pxp_document.T_element "source" && + t#node_type = Pxp_document.T_element "target" -> + let name = cic_attr_of_xml_attr (t#attribute "binder") + and source = s#extension#to_cic_term + and target = t#extension#to_cic_term in + let res = Cic.ALambda (id,ref None,name,source,target) in + register_id id res ; + res + | _ -> raise (IllFormedXml 12) + end +;; + +class eltype_letin = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let sons = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + match sons with + [s ; t] when + s#node_type = Pxp_document.T_element "term" && + t#node_type = Pxp_document.T_element "letintarget" -> + let name = cic_attr_of_xml_attr (t#attribute "binder") + and source = s#extension#to_cic_term + and target = t#extension#to_cic_term in + let res = Cic.ALetIn (id,ref None,name,source,target) in + register_id id res ; + res + | _ -> raise (IllFormedXml 12) + end +;; + +(* The definition of domspec, an hashtable that maps each node type to the *) +(* object that must be linked to it. Used by markup. *) + +let domspec = + let module D = Pxp_document in + D.make_spec_from_alist + ~data_exemplar: (new D.data_impl (new eltype_not_of_cic)) + ~default_element_exemplar: (new D.element_impl (new eltype_not_of_cic)) + ~element_alist: + [ "REL", (new D.element_impl (new eltype_rel)) ; + "VAR", (new D.element_impl (new eltype_var)) ; + "META", (new D.element_impl (new eltype_meta)) ; + "SORT", (new D.element_impl (new eltype_sort)) ; + "IMPLICIT", (new D.element_impl (new eltype_implicit)) ; + "CAST", (new D.element_impl (new eltype_cast)) ; + "PROD", (new D.element_impl (new eltype_prod)) ; + "LAMBDA", (new D.element_impl (new eltype_lambda)) ; + "LETIN", (new D.element_impl (new eltype_letin)) ; + "APPLY", (new D.element_impl (new eltype_apply)) ; + "CONST", (new D.element_impl (new eltype_const)) ; + "ABST", (new D.element_impl (new eltype_abst)) ; + "MUTIND", (new D.element_impl (new eltype_mutind)) ; + "MUTCONSTRUCT", (new D.element_impl (new eltype_mutconstruct)) ; + "MUTCASE", (new D.element_impl (new eltype_mutcase)) ; + "FIX", (new D.element_impl (new eltype_fix)) ; + "COFIX", (new D.element_impl (new eltype_cofix)) ; + "arity", (new D.element_impl (new eltype_transparent)) ; + "term", (new D.element_impl (new eltype_transparent)) ; + "type", (new D.element_impl (new eltype_transparent)) ; + "body", (new D.element_impl (new eltype_transparent)) ; + "source", (new D.element_impl (new eltype_transparent)) ; + "target", (new D.element_impl (new eltype_transparent)) ; + "letintarget", (new D.element_impl (new eltype_transparent)) ; + "patternsType", (new D.element_impl (new eltype_transparent)) ; + "inductiveTerm", (new D.element_impl (new eltype_transparent)) ; + "pattern", (new D.element_impl (new eltype_transparent)) + ] + () +;; diff --git a/helm/metadata/create2/mk_forward/cicParser3.mli b/helm/metadata/create2/mk_forward/cicParser3.mli new file mode 100644 index 000000000..ada1b2e81 --- /dev/null +++ b/helm/metadata/create2/mk_forward/cicParser3.mli @@ -0,0 +1,67 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This module is the terms level of a parser for cic objects from xml *) +(* files to the internal representation. It is used by the module cicParser2 *) +(* (objects level). It defines an extension of the standard dom using the *) +(* object-oriented extension machinery of markup: an object with a method *) +(* to_cic_term that returns the internal representation of the subtree is *) +(* added to each node of the dom tree *) +(* *) +(******************************************************************************) + +exception IllFormedXml of int + +val ids_to_targets : (Cic.id, Cic.anntarget) Hashtbl.t option ref +val current_sp : string list ref +val current_uri : UriManager.uri ref +val process_annotations : bool ref + +(* the "interface" of the class linked to each node of the dom tree *) +class virtual cic_term : + object ('a) + + (* fields and methods ever required by markup *) + val mutable node : cic_term Pxp_document.node option + method clone : 'a + method node : cic_term Pxp_document.node + method set_node : cic_term Pxp_document.node -> unit + + (* a method that returns the internal representation of the tree (term) *) + (* rooted in this node *) + method virtual to_cic_term : Cic.annterm + + end + +(* The definition of domspec, an hashtable that maps each node type to the *) +(* object that must be linked to it. Used by markup. *) +val domspec : cic_term Pxp_document.spec diff --git a/helm/metadata/create2/mk_forward/cicSubstitution.ml b/helm/metadata/create2/mk_forward/cicSubstitution.ml new file mode 100644 index 000000000..28dbe24e3 --- /dev/null +++ b/helm/metadata/create2/mk_forward/cicSubstitution.ml @@ -0,0 +1,142 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +let lift n = + let rec liftaux k = + let module C = Cic in + function + C.Rel m -> + if m < k then + C.Rel m + else + C.Rel (m + n) + | C.Var _ as t -> t + | C.Meta _ as t -> t + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty) + | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t) + | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t) + | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t) + | C.Appl l -> C.Appl (List.map (liftaux k) l) + | C.Const _ as t -> t + | C.Abst _ as t -> t + | C.MutInd _ as t -> t + | C.MutConstruct _ as t -> t + | C.MutCase (sp,cookingsno,i,outty,t,pl) -> + C.MutCase (sp, cookingsno, i, liftaux k outty, liftaux k t, + List.map (liftaux k) pl) + | C.Fix (i, fl) -> + let len = List.length fl in + let liftedfl = + List.map + (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo)) + fl + in + C.Fix (i, liftedfl) + | C.CoFix (i, fl) -> + let len = List.length fl in + let liftedfl = + List.map + (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo)) + fl + in + C.CoFix (i, liftedfl) + in + liftaux 1 +;; + +let subst arg = + let rec substaux k = + let module C = Cic in + function + C.Rel n as t -> + (match n with + n when n = k -> lift (k - 1) arg + | n when n < k -> t + | _ -> C.Rel (n - 1) + ) + | C.Var _ as t -> t + | C.Meta _ as t -> t + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) (*CSC ??? *) + | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t) + | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t) + | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t) + | C.Appl l -> C.Appl (List.map (substaux k) l) + | C.Const _ as t -> t + | C.Abst _ as t -> t + | C.MutInd _ as t -> t + | C.MutConstruct _ as t -> t + | C.MutCase (sp,cookingsno,i,outt,t,pl) -> + C.MutCase (sp,cookingsno,i,substaux k outt, substaux k t, + List.map (substaux k) pl) + | C.Fix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo)) + fl + in + C.CoFix (i, substitutedfl) + in + substaux 1 +;; + +let undebrujin_inductive_def uri = + function + Cic.InductiveDefinition (dl,params,n_ind_params) -> + let dl' = + List.map + (fun (name,inductive,arity,constructors) -> + let constructors' = + List.map + (fun (name,ty,r) -> + let ty' = + let counter = ref (List.length dl) in + List.fold_right + (fun _ -> + decr counter ; + subst (Cic.MutInd (uri,0,!counter)) + ) dl ty + in + (name,ty',r) + ) constructors + in + (name,inductive,arity,constructors') + ) dl + in + Cic.InductiveDefinition (dl', params, n_ind_params) + | obj -> obj +;; diff --git a/helm/metadata/create2/mk_forward/cicSubstitution.mli b/helm/metadata/create2/mk_forward/cicSubstitution.mli new file mode 100644 index 000000000..72e9a32c2 --- /dev/null +++ b/helm/metadata/create2/mk_forward/cicSubstitution.mli @@ -0,0 +1,28 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val lift : int -> Cic.term -> Cic.term +val subst : Cic.term -> Cic.term -> Cic.term +val undebrujin_inductive_def : UriManager.uri -> Cic.obj -> Cic.obj diff --git a/helm/metadata/create2/mk_forward/clientHTTP.ml b/helm/metadata/create2/mk_forward/clientHTTP.ml new file mode 100644 index 000000000..4d5488c00 --- /dev/null +++ b/helm/metadata/create2/mk_forward/clientHTTP.ml @@ -0,0 +1,60 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +exception HttpClientError of exn * string;; + +let send cmd = + try + ignore (Http_client.Convenience.http_get cmd) + with + e -> raise (HttpClientError (e,cmd)) +;; + +let get uri = + try + Http_client.Convenience.http_get uri + with + e -> raise (HttpClientError (e,uri)) +;; + +let get_and_save uri dest_filename = + let reply = get uri + and out_channel = open_out dest_filename in + output_string out_channel reply ; + close_out out_channel +;; + +let get_and_save_to_tmp uri = + let flat_string s s' c = + let cs = String.copy s in + for i = 0 to (String.length s) - 1 do + if String.contains s' s.[i] then cs.[i] <- c + done ; + cs + in + let tmp_file = Configuration.tmp_dir ^ "/" ^ (flat_string uri ".-=:;!?/&" '_') in + get_and_save uri tmp_file ; + tmp_file +;; diff --git a/helm/metadata/create2/mk_forward/clientHTTP.mli b/helm/metadata/create2/mk_forward/clientHTTP.mli new file mode 100644 index 000000000..59587edc2 --- /dev/null +++ b/helm/metadata/create2/mk_forward/clientHTTP.mli @@ -0,0 +1,30 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +exception HttpClientError of exn * string;; +val send : string -> unit +val get : string -> string +val get_and_save : string -> string -> unit +val get_and_save_to_tmp : string -> string diff --git a/helm/metadata/create2/mk_forward/configuration.ml.in b/helm/metadata/create2/mk_forward/configuration.ml.in new file mode 100644 index 000000000..c743be135 --- /dev/null +++ b/helm/metadata/create2/mk_forward/configuration.ml.in @@ -0,0 +1,119 @@ +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 28/12/2000 *) +(* *) +(* This is the parser that reads the configuration file of helm *) +(* *) +(******************************************************************************) + +exception MalformedDir of string + +(* this should be the only hard coded constant *) +let filename = + let prefix = + try + Sys.getenv "HELM_CONFIGURATION_DIR" + with + Not_found -> "@HELM_CONFIGURATION_DIR@" + in + if prefix.[(String.length prefix) - 1] = '/' then + raise (MalformedDir prefix) ; + prefix ^ "/configuration.xml";; + +exception Warnings;; + +class warner = + object + method warn w = + print_endline ("WARNING: " ^ w) ; + (raise Warnings : unit) + end +;; + +let xml_document () = + let module Y = Pxp_yacc in + try + let config = {Y.default_config with Y.warner = new warner} in + Y.parse_document_entity config (Y.from_file filename) Y.default_spec + with + e -> + print_endline (Pxp_types.string_of_exn e) ; + raise e +;; + +exception Impossible;; + +let vars = Hashtbl.create 14;; + +(* resolve tags and returns the string values of the variable tags *) +let rec resolve = + let module D = Pxp_document in + function + [] -> "" + | he::tl when he#node_type = D.T_element "value-of" -> + (match he#attribute "var" with + Pxp_types.Value var -> Hashtbl.find vars var + | _ -> raise Impossible + ) ^ resolve tl + | he::tl when he#node_type = D.T_data -> + he#data ^ resolve tl + | _ -> raise Impossible +;; + +(* we trust the xml file to be valid because of the validating xml parser *) +let _ = + List.iter + (function + n -> + match n#node_type with + Pxp_document.T_element var -> + Hashtbl.add vars var (resolve (n#sub_nodes)) + | _ -> raise Impossible + ) + ((xml_document ())#root#sub_nodes) +;; + +(* try to read a configuration variable, given its name into the + * configuration.xml file and its name into the shell environment. + * The shell variable, if present, has precedence over configuration.xml + *) +let read_configuration_var_env xml_name env_name = + try + try + Sys.getenv env_name + with + Not_found -> Hashtbl.find vars xml_name + with + Not_found -> + Printf.printf "Sorry, cannot find variable `%s', please check your configuration\n" xml_name ; + flush stdout ; + raise Not_found + +let read_configuration_var xml_name = + try + Hashtbl.find vars xml_name + with + Not_found -> + Printf.printf "Sorry, cannot find variable `%s', please check your configuration\n" xml_name ; + flush stdout ; + raise Not_found + +let helm_dir = read_configuration_var "helm_dir";; +let dtd_dir = read_configuration_var "dtd_dir";; +let style_dir = read_configuration_var_env "style_dir" "HELM_STYLE_DIR";; +let servers_file = read_configuration_var "servers_file";; +let uris_dbm = read_configuration_var "uris_dbm";; +let dest = read_configuration_var "dest";; +let indexname = read_configuration_var "indexname";; +let tmp_dir = read_configuration_var "tmp_dir" +let helm_dir = read_configuration_var "helm_dir";; +let getter_url = read_configuration_var_env "getter_url" "HELM_GETTER_URL";; +let processor_url = read_configuration_var_env "processor_url" "HELM_PROCESSOR_URL";; +let annotations_dir = read_configuration_var_env "annotations_dir" "HELM_ANNOTATIONS_DIR" +let annotations_url = read_configuration_var_env "annotations_url" "HELM_ANNOTATIONS_URL" + +let _ = Hashtbl.clear vars;; + diff --git a/helm/metadata/create2/mk_forward/csc_pxp_reader.ml b/helm/metadata/create2/mk_forward/csc_pxp_reader.ml new file mode 100644 index 000000000..587c60c8a --- /dev/null +++ b/helm/metadata/create2/mk_forward/csc_pxp_reader.ml @@ -0,0 +1,1008 @@ +(* $Id$ + * ---------------------------------------------------------------------- + * PXP: The polymorphic XML parser for Objective Caml. + * Copyright by Gerd Stolpmann. See LICENSE for details. + *) + +open Pxp_types;; +exception Not_competent;; +exception Not_resolvable of exn;; + +class type resolver = + object + method init_rep_encoding : rep_encoding -> unit + method init_warner : collect_warnings -> unit + method rep_encoding : rep_encoding + method open_in : ext_id -> Lexing.lexbuf + method close_in : unit + method close_all : unit + method change_encoding : string -> unit + method clone : resolver + end +;; + + +class virtual resolve_general + = + object (self) + val mutable internal_encoding = `Enc_utf8 + + val mutable encoding = `Enc_utf8 + val mutable encoding_requested = false + + val mutable warner = new drop_warnings + + val mutable enc_initialized = false + val mutable wrn_initialized = false + + val mutable clones = [] + + method init_rep_encoding e = + internal_encoding <- e; + enc_initialized <- true; + + method init_warner w = + warner <- w; + wrn_initialized <- true; + + method rep_encoding = (internal_encoding :> rep_encoding) + +(* + method clone = + ( {< encoding = `Enc_utf8; + encoding_requested = false; + >} + : # resolver :> resolver ) +*) + + method private warn (k:int) = + (* Called if a character not representable has been found. + * k is the character code. + *) + if k < 0xd800 or (k >= 0xe000 & k <= 0xfffd) or + (k >= 0x10000 & k <= 0x10ffff) then begin + warner # warn ("Code point cannot be represented: " ^ string_of_int k); + end + else + raise (WF_error("Code point " ^ string_of_int k ^ + " outside the accepted range of code points")) + + + method private autodetect s = + (* s must be at least 4 bytes long. The slot 'encoding' is + * set to: + * "UTF-16-BE": UTF-16/UCS-2 encoding big endian + * "UTF-16-LE": UTF-16/UCS-2 encoding little endian + * "UTF-8": UTF-8 encoding + *) + if String.length s < 4 then + encoding <- `Enc_utf8 + else if String.sub s 0 2 = "\254\255" then + encoding <- `Enc_utf16 + (* Note: Netconversion.recode will detect the big endianess, too *) + else if String.sub s 0 2 = "\255\254" then + encoding <- `Enc_utf16 + (* Note: Netconversion.recode will detect the little endianess, too *) + else + encoding <- `Enc_utf8 + + + method private virtual next_string : string -> int -> int -> int + method private virtual init_in : ext_id -> unit + method virtual close_in : unit + + method close_all = + List.iter (fun r -> r # close_in) clones + + method open_in xid = + assert(enc_initialized && wrn_initialized); + + encoding <- `Enc_utf8; + encoding_requested <- false; + self # init_in xid; (* may raise Not_competent *) + (* init_in: may already set 'encoding' *) + + let buffer_max = 512 in + let buffer = String.make buffer_max ' ' in + let buffer_len = ref 0 in + let buffer_end = ref false in + let fillup () = + if not !buffer_end & !buffer_len < buffer_max then begin + let l = + self # next_string buffer !buffer_len (buffer_max - !buffer_len) in + if l = 0 then + buffer_end := true + else begin + buffer_len := !buffer_len + l + end + end + in + let consume n = + let l = !buffer_len - n in + String.blit buffer n buffer 0 l; + buffer_len := l + in + + fillup(); + if not encoding_requested then self # autodetect buffer; + + Lexing.from_function + (fun s n -> + (* TODO: if encoding = internal_encoding, it is possible to + * avoid copying buffer to s because s can be directly used + * as buffer. + *) + + fillup(); + if !buffer_len = 0 then + 0 + else begin + let m_in = !buffer_len in + let m_max = if encoding_requested then n else 1 in + let n_in, n_out, encoding' = + if encoding = (internal_encoding : rep_encoding :> encoding) && + encoding_requested + then begin + (* Special case encoding = internal_encoding *) + String.blit buffer 0 s 0 m_in; + m_in, m_in, encoding + end + else + Netconversion.recode + ~in_enc:encoding + ~in_buf:buffer + ~in_pos:0 + ~in_len:m_in + ~out_enc:(internal_encoding : rep_encoding :> encoding) + ~out_buf:s + ~out_pos:0 + ~out_len:n + ~max_chars:m_max + ~subst:(fun k -> self # warn k; "") + in + if n_in = 0 then + (* An incomplete character at the end of the stream: *) + raise Netconversion.Malformed_code; + (* failwith "Badly encoded character"; *) + encoding <- encoding'; + consume n_in; + assert(n_out <> 0); + n_out + end) + + method change_encoding enc = + if not encoding_requested then begin + if enc <> "" then begin + match Netconversion.encoding_of_string enc with + `Enc_utf16 -> + (match encoding with + (`Enc_utf16_le | `Enc_utf16_be) -> () + | `Enc_utf16 -> assert false + | _ -> + raise(WF_error "Encoding of data stream and encoding declaration mismatch") + ) + | e -> + encoding <- e + end; + (* else: the autodetected encoding counts *) + encoding_requested <- true; + end; + end +;; + + +class resolve_read_any_channel ?(close=close_in) ~channel_of_id () = + object (self) + inherit resolve_general as super + + val f_open = channel_of_id + val mutable current_channel = None + val close = close + + method private init_in (id:ext_id) = + if current_channel <> None then + failwith "Pxp_reader.resolve_read_any_channel # init_in"; + let ch, enc_opt = f_open id in (* may raise Not_competent *) + begin match enc_opt with + None -> () + | Some enc -> encoding <- enc; encoding_requested <- true + end; + current_channel <- Some ch; + + method private next_string s ofs len = + match current_channel with + None -> failwith "Pxp_reader.resolve_read_any_channel # next_string" + | Some ch -> + input ch s ofs len + + method close_in = + match current_channel with + None -> () + | Some ch -> + close ch; + current_channel <- None + + method clone = + let c = new resolve_read_any_channel + ?close:(Some close) f_open () in + c # init_rep_encoding internal_encoding; + c # init_warner warner; + clones <- c :: clones; + (c :> resolver) + + end +;; + + +class resolve_read_this_channel1 is_stale ?id ?fixenc ?close ch = + + let getchannel = ref (fun xid -> assert false) in + + object (self) + inherit resolve_read_any_channel + ?close + (fun xid -> !getchannel xid) + () + as super + + val mutable is_stale = is_stale + (* The channel can only be read once. To avoid that the channel + * is opened several times, the flag 'is_stale' is set after the + * first time. + *) + + val fixid = id + val fixenc = fixenc + val fixch = ch + + initializer + getchannel := self # getchannel + + method private getchannel xid = + begin match fixid with + None -> () + | Some bound_xid -> + if xid <> bound_xid then raise Not_competent + end; + ch, fixenc + + method private init_in (id:ext_id) = + if is_stale then + raise Not_competent + else begin + super # init_in id; + is_stale <- true + end + + method close_in = + current_channel <- None + + method clone = + let c = new resolve_read_this_channel1 + is_stale + ?id:fixid ?fixenc:fixenc ?close:(Some close) fixch + in + c # init_rep_encoding internal_encoding; + c # init_warner warner; + clones <- c :: clones; + (c :> resolver) + + end +;; + + +class resolve_read_this_channel = + resolve_read_this_channel1 false +;; + + +class resolve_read_any_string ~string_of_id () = + object (self) + inherit resolve_general as super + + val f_open = string_of_id + val mutable current_string = None + val mutable current_pos = 0 + + method private init_in (id:ext_id) = + if current_string <> None then + failwith "Pxp_reader.resolve_read_any_string # init_in"; + let s, enc_opt = f_open id in (* may raise Not_competent *) + begin match enc_opt with + None -> () + | Some enc -> encoding <- enc; encoding_requested <- true + end; + current_string <- Some s; + current_pos <- 0; + + method private next_string s ofs len = + match current_string with + None -> failwith "Pxp_reader.resolve_read_any_string # next_string" + | Some str -> + let l = min len (String.length str - current_pos) in + String.blit str current_pos s ofs l; + current_pos <- current_pos + l; + l + + method close_in = + match current_string with + None -> () + | Some _ -> + current_string <- None + + method clone = + let c = new resolve_read_any_string f_open () in + c # init_rep_encoding internal_encoding; + c # init_warner warner; + clones <- c :: clones; + (c :> resolver) + end +;; + + +class resolve_read_this_string1 is_stale ?id ?fixenc str = + + let getstring = ref (fun xid -> assert false) in + + object (self) + inherit resolve_read_any_string (fun xid -> !getstring xid) () as super + + val is_stale = is_stale + (* For some reasons, it is not allowed to open a clone of the resolver + * a second time when the original resolver is already open. + *) + + val fixid = id + val fixenc = fixenc + val fixstr = str + + initializer + getstring := self # getstring + + method private getstring xid = + begin match fixid with + None -> () + | Some bound_xid -> + if xid <> bound_xid then raise Not_competent + end; + fixstr, fixenc + + + method private init_in (id:ext_id) = + if is_stale then + raise Not_competent + else + super # init_in id + + method clone = + let c = new resolve_read_this_string1 + (is_stale or current_string <> None) + ?id:fixid ?fixenc:fixenc fixstr + in + c # init_rep_encoding internal_encoding; + c # init_warner warner; + clones <- c :: clones; + (c :> resolver) + end +;; + + +class resolve_read_this_string = + resolve_read_this_string1 false +;; + + +class resolve_read_url_channel + ?(base_url = Neturl.null_url) + ?close + ~url_of_id + ~channel_of_url + () + + : resolver + = + + let getchannel = ref (fun xid -> assert false) in + + object (self) + inherit resolve_read_any_channel + ?close + (fun xid -> !getchannel xid) + () + as super + + val base_url = base_url + val mutable own_url = Neturl.null_url + + val url_of_id = url_of_id + val channel_of_url = channel_of_url + + + initializer + getchannel := self # getchannel + + method private getchannel xid = + let rel_url = url_of_id xid in (* may raise Not_competent *) + + try + (* Now compute the absolute URL: *) + let abs_url = + if Neturl.url_provides ~scheme:true rel_url then + rel_url + else + Neturl.apply_relative_url base_url rel_url in + (* may raise Malformed_URL *) + + (* Simple check whether 'abs_url' is really absolute: *) + if not(Neturl.url_provides ~scheme:true abs_url) + then raise Not_competent; + + own_url <- abs_url; + (* FIXME: Copy 'abs_url' ? *) + + (* Get and return the channel: *) + channel_of_url xid abs_url (* may raise Not_competent *) + with + Neturl.Malformed_URL -> raise (Not_resolvable Neturl.Malformed_URL) + | Not_competent -> raise (Not_resolvable Not_found) + + method clone = + let c = + new resolve_read_url_channel + ?base_url:(Some own_url) + ?close:(Some close) + ~url_of_id:url_of_id + ~channel_of_url:channel_of_url + () + in + c # init_rep_encoding internal_encoding; + c # init_warner warner; + clones <- c :: clones; + (c :> resolve_read_url_channel) + end +;; + + +type spec = [ `Not_recognized | `Allowed | `Required ] + +class resolve_as_file + ?(file_prefix = (`Allowed :> spec)) + ?(host_prefix = (`Allowed :> spec)) + ?(system_encoding = `Enc_utf8) + ?(map_private_id = (fun _ -> raise Not_competent)) + ?(open_private_id = (fun _ -> raise Not_competent)) + () + = + + let url_syntax = + let enable_if = + function + `Not_recognized -> Neturl.Url_part_not_recognized + | `Allowed -> Neturl.Url_part_allowed + | `Required -> Neturl.Url_part_required + in + { Neturl.null_url_syntax with + Neturl.url_enable_scheme = enable_if file_prefix; + Neturl.url_enable_host = enable_if host_prefix; + Neturl.url_enable_path = Neturl.Url_part_required; + Neturl.url_accepts_8bits = true; + } + in + + let base_url_syntax = + { Neturl.null_url_syntax with + Neturl.url_enable_scheme = Neturl.Url_part_required; + Neturl.url_enable_host = Neturl.Url_part_allowed; + Neturl.url_enable_path = Neturl.Url_part_required; + Neturl.url_accepts_8bits = true; + } + in + + let default_base_url = + Neturl.make_url + ~scheme: "file" + ~host: "" + ~path: (Neturl.split_path (Sys.getcwd() ^ "/")) + base_url_syntax + in + + let file_url_of_id xid = + let file_url_of_sysname sysname = + (* By convention, we can assume that sysname is a URL conforming + * to RFC 1738 with the exception that it may contain non-ASCII + * UTF-8 characters. + *) + try + Neturl.url_of_string url_syntax sysname + (* may raise Malformed_URL *) + with + Neturl.Malformed_URL -> raise Not_competent + in + let url = + match xid with + Anonymous -> raise Not_competent + | Public (_,sysname) -> if sysname <> "" then file_url_of_sysname sysname + else raise Not_competent + | System sysname -> file_url_of_sysname sysname + | Private pid -> map_private_id pid + in + let scheme = + try Neturl.url_scheme url with Not_found -> "file" in + let host = + try Neturl.url_host url with Not_found -> "" in + + if scheme <> "file" then raise Not_competent; + if host <> "" && host <> "localhost" then raise Not_competent; + + url + in + + let channel_of_file_url xid url = + match xid with + Private pid -> open_private_id pid + | _ -> + ( try + let path_utf8 = + try Neturl.join_path (Neturl.url_path ~encoded:false url) + with Not_found -> raise Not_competent + in + + let path = + Netconversion.recode_string + ~in_enc: `Enc_utf8 + ~out_enc: system_encoding + path_utf8 in + (* May raise Malformed_code *) + + open_in_bin path, None + (* May raise Sys_error *) + + with + | Netconversion.Malformed_code -> assert false + (* should not happen *) + | Sys_error _ as e -> + raise (Not_resolvable e) + ) + in + + resolve_read_url_channel + ~base_url: default_base_url + ~url_of_id: file_url_of_id + ~channel_of_url: channel_of_file_url + () +;; + + +let make_file_url ?(system_encoding = `Enc_utf8) ?(enc = `Enc_utf8) filename = + let utf8_filename = + Netconversion.recode_string + ~in_enc: enc + ~out_enc: `Enc_utf8 + filename + in + + let utf8_abs_filename = + if utf8_filename <> "" && utf8_filename.[0] = '/' then + utf8_filename + else + let cwd = Sys.getcwd() in + let cwd_utf8 = + Netconversion.recode_string + ~in_enc: system_encoding + ~out_enc: `Enc_utf8 in + cwd ^ "/" ^ utf8_filename + in + + let syntax = { Neturl.ip_url_syntax with Neturl.url_accepts_8bits = true } in + let url = Neturl.make_url + ~scheme:"file" + ~host:"localhost" + ~path:(Neturl.split_path utf8_abs_filename) + syntax + in + url +;; + + +class lookup_public_id (catalog : (string * resolver) list) = + let norm_catalog = + List.map (fun (id,s) -> Pxp_aux.normalize_public_id id, s) catalog in +( object (self) + val cat = norm_catalog + val mutable internal_encoding = `Enc_utf8 + val mutable warner = new drop_warnings + val mutable active_resolver = None + + method init_rep_encoding enc = + internal_encoding <- enc + + method init_warner w = + warner <- w; + + method rep_encoding = internal_encoding + (* CAUTION: This may not be the truth! *) + + method open_in xid = + + if active_resolver <> None then failwith "Pxp_reader.lookup_* # open_in"; + + let r = + match xid with + Public(pubid,_) -> + begin + (* Search pubid in catalog: *) + try + let norm_pubid = Pxp_aux.normalize_public_id pubid in + List.assoc norm_pubid cat + with + Not_found -> + raise Not_competent + end + | _ -> + raise Not_competent + in + + let r' = r # clone in + r' # init_rep_encoding internal_encoding; + r' # init_warner warner; + let lb = r' # open_in xid in (* may raise Not_competent *) + active_resolver <- Some r'; + lb + + method close_in = + match active_resolver with + None -> () + | Some r -> r # close_in; + active_resolver <- None + + method close_all = + self # close_in + + method change_encoding (enc:string) = + match active_resolver with + None -> failwith "Pxp_reader.lookup_* # change_encoding" + | Some r -> r # change_encoding enc + + method clone = + let c = new lookup_public_id cat in + c # init_rep_encoding internal_encoding; + c # init_warner warner; + c + end : resolver ) +;; + + +let lookup_public_id_as_file ?(fixenc:encoding option) catalog = + let ch_of_id filename id = + let ch = open_in_bin filename in (* may raise Sys_error *) + ch, fixenc + in + let catalog' = + List.map + (fun (id,s) -> + (id, new resolve_read_any_channel (ch_of_id s) ()) + ) + catalog + in + new lookup_public_id catalog' +;; + + +let lookup_public_id_as_string ?(fixenc:encoding option) catalog = + let catalog' = + List.map + (fun (id,s) -> + (id, new resolve_read_any_string (fun _ -> s, fixenc) ()) + ) + catalog + in + new lookup_public_id catalog' +;; + + +class lookup_system_id (catalog : (string * resolver) list) = +( object (self) + val cat = catalog + val mutable internal_encoding = `Enc_utf8 + val mutable warner = new drop_warnings + val mutable active_resolver = None + + method init_rep_encoding enc = + internal_encoding <- enc + + method init_warner w = + warner <- w; + + method rep_encoding = internal_encoding + (* CAUTION: This may not be the truth! *) + + + method open_in xid = + + if active_resolver <> None then failwith "Pxp_reader.lookup_system_id # open_in"; + + let lookup sysid = + try + List.assoc sysid cat + with + Not_found -> + raise Not_competent + in + + let r = + match xid with + System sysid -> lookup sysid + | Public(_,sysid) -> lookup sysid + | _ -> raise Not_competent + in + + let r' = r # clone in + r' # init_rep_encoding internal_encoding; + r' # init_warner warner; + let lb = r' # open_in xid in (* may raise Not_competent *) + active_resolver <- Some r'; + lb + + + method close_in = + match active_resolver with + None -> () + | Some r -> r # close_in; + active_resolver <- None + + method close_all = + self # close_in + + method change_encoding (enc:string) = + match active_resolver with + None -> failwith "Pxp_reader.lookup_system # change_encoding" + | Some r -> r # change_encoding enc + + method clone = + let c = new lookup_system_id cat in + c # init_rep_encoding internal_encoding; + c # init_warner warner; + c + end : resolver) +;; + + +let lookup_system_id_as_file ?(fixenc:encoding option) catalog = + let ch_of_id filename id = + let ch = open_in_bin filename in (* may raise Sys_error *) + ch, fixenc + in + let catalog' = + List.map + (fun (id,s) -> + (id, new resolve_read_any_channel (ch_of_id s) ()) + ) + catalog + in + new lookup_system_id catalog' +;; + + +let lookup_system_id_as_string ?(fixenc:encoding option) catalog = + let catalog' = + List.map + (fun (id,s) -> + (id, new resolve_read_any_string (fun _ -> s, fixenc) ()) + ) + catalog + in + new lookup_system_id catalog' +;; + + +type combination_mode = + Public_before_system + | System_before_public +;; + + +class combine ?prefer ?(mode = Public_before_system) rl = + object (self) + val prefered_resolver = prefer + val mode = mode + val resolvers = (rl : resolver list) + val mutable internal_encoding = `Enc_utf8 + val mutable warner = new drop_warnings + val mutable active_resolver = None + val mutable clones = [] + + method init_rep_encoding enc = + List.iter + (fun r -> r # init_rep_encoding enc) + rl; + internal_encoding <- enc + + method init_warner w = + List.iter + (fun r -> r # init_warner w) + rl; + warner <- w; + + method rep_encoding = internal_encoding + (* CAUTION: This may not be the truth! *) + + method open_in xid = + let rec find_competent_resolver_for xid' rl = + match rl with + r :: rl' -> + begin try + r, (r # open_in xid') + with + Not_competent -> find_competent_resolver_for xid' rl' + end; + | [] -> + raise Not_competent + in + + let find_competent_resolver rl = + match xid with + Public(pubid,sysid) -> + ( match mode with + Public_before_system -> + ( try + find_competent_resolver_for(Public(pubid,"")) rl + with + Not_competent -> + find_competent_resolver_for(System sysid) rl + ) + | System_before_public -> + ( try + find_competent_resolver_for(System sysid) rl + with + Not_competent -> + find_competent_resolver_for(Public(pubid,"")) rl + ) + ) + | other -> + find_competent_resolver_for other rl + in + + if active_resolver <> None then failwith "Pxp_reader.combine # open_in"; + let r, lb = + match prefered_resolver with + None -> find_competent_resolver resolvers + | Some r -> find_competent_resolver (r :: resolvers) + in + active_resolver <- Some r; + lb + + method close_in = + match active_resolver with + None -> () + | Some r -> r # close_in; + active_resolver <- None + + method close_all = + List.iter (fun r -> r # close_in) clones + + method change_encoding (enc:string) = + match active_resolver with + None -> failwith "Pxp_reader.combine # change_encoding" + | Some r -> r # change_encoding enc + + method clone = + let c = + match active_resolver with + None -> + new combine ?prefer:None ?mode:(Some mode) + (List.map (fun q -> q # clone) resolvers) + | Some r -> + let r' = r # clone in + new combine + ?prefer:(Some r') + ?mode:(Some mode) + (List.map + (fun q -> if q == r then r' else q # clone) + resolvers) + in + c # init_rep_encoding internal_encoding; + c # init_warner warner; + clones <- c :: clones; + c + end + + + +(* ====================================================================== + * History: + * + * $Log$ + * Revision 1.1 2001/10/24 15:33:16 sacerdot + * New procedure to create metadata committed and old procedure removed. + * The new procedure is based on ocaml code and builds metadata for both + * forward and backward pointers. The old one was based on a stylesheet. + * + * Revision 1.16 2001/07/01 09:46:40 gerd + * Fix: resolve_read_url_channel does not use the base_url if + * the current URL is already absolute + * + * Revision 1.15 2001/07/01 08:35:23 gerd + * Instead of the ~auto_close argument, there is now a + * ~close argument for several functions/classes. This allows some + * additional action when the resolver is closed. + * + * Revision 1.14 2001/06/14 23:28:02 gerd + * Fix: class combine works now with private IDs. + * + * Revision 1.13 2001/04/22 14:16:48 gerd + * resolve_as_file: you can map private IDs to arbitrary channels. + * resolve_read_url_channel: changed type of the channel_of_url + * argument (ext_id is also passed) + * More examples and documentation. + * + * Revision 1.12 2001/04/21 17:40:48 gerd + * Bugfix in 'combine' + * + * Revision 1.11 2001/04/03 20:22:44 gerd + * New resolvers for catalogs of PUBLIC and SYSTEM IDs. + * Improved "combine": PUBLIC and SYSTEM IDs are handled + * separately. + * Rewritten from_file: Is now a simple application of the + * Pxp_reader classes and functions. (The same has still to be done + * for from_channel!) + * + * Revision 1.10 2001/02/01 20:38:49 gerd + * New support for PUBLIC identifiers. + * + * Revision 1.9 2000/08/14 22:24:55 gerd + * Moved the module Pxp_encoding to the netstring package under + * the new name Netconversion. + * + * Revision 1.8 2000/07/16 18:31:09 gerd + * The exception Illegal_character has been dropped. + * + * Revision 1.7 2000/07/09 15:32:01 gerd + * Fix in resolve_this_channel, resolve_this_string + * + * Revision 1.6 2000/07/09 01:05:33 gerd + * New methode 'close_all' that closes the clones, too. + * + * Revision 1.5 2000/07/08 16:24:56 gerd + * Introduced the exception 'Not_resolvable' to indicate that + * 'combine' should not try the next resolver of the list. + * + * Revision 1.4 2000/07/06 23:04:46 gerd + * Quick fix for 'combine': The active resolver is "prefered", + * but the other resolvers are also used. + * + * Revision 1.3 2000/07/06 21:43:45 gerd + * Fix: Public(_,name) is now treated as System(name) if + * name is non-empty. + * + * Revision 1.2 2000/07/04 22:13:30 gerd + * Implemented the new API rev. 1.2 of pxp_reader.mli. + * + * Revision 1.1 2000/05/29 23:48:38 gerd + * Changed module names: + * Markup_aux into Pxp_aux + * Markup_codewriter into Pxp_codewriter + * Markup_document into Pxp_document + * Markup_dtd into Pxp_dtd + * Markup_entity into Pxp_entity + * Markup_lexer_types into Pxp_lexer_types + * Markup_reader into Pxp_reader + * Markup_types into Pxp_types + * Markup_yacc into Pxp_yacc + * See directory "compatibility" for (almost) compatible wrappers emulating + * Markup_document, Markup_dtd, Markup_reader, Markup_types, and Markup_yacc. + * + * ====================================================================== + * Old logs from markup_reader.ml: + * + * Revision 1.3 2000/05/29 21:14:57 gerd + * Changed the type 'encoding' into a polymorphic variant. + * + * Revision 1.2 2000/05/20 20:31:40 gerd + * Big change: Added support for various encodings of the + * internal representation. + * + * Revision 1.1 2000/03/13 23:41:44 gerd + * Initial revision; this code was formerly part of Markup_entity. + * + * + *) diff --git a/helm/metadata/create2/mk_forward/deannotate.ml b/helm/metadata/create2/mk_forward/deannotate.ml new file mode 100644 index 000000000..00d4854db --- /dev/null +++ b/helm/metadata/create2/mk_forward/deannotate.ml @@ -0,0 +1,98 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +let expect_possible_parameters = ref false;; + +exception NotExpectingPossibleParameters;; + +let rec deannotate_term = + let module C = Cic in + function + C.ARel (_,_,n,_) -> C.Rel n + | C.AVar (_,_,uri) -> C.Var uri + | C.AMeta (_,_,n) -> C.Meta n + | C.ASort (_,_,s) -> C.Sort s + | C.AImplicit _ -> C.Implicit + | C.ACast (_,_,va,ty) -> C.Cast (deannotate_term va, deannotate_term ty) + | C.AProd (_,_,name,so,ta) -> + C.Prod (name, deannotate_term so, deannotate_term ta) + | C.ALambda (_,_,name,so,ta) -> + C.Lambda (name, deannotate_term so, deannotate_term ta) + | C.ALetIn (_,_,name,so,ta) -> + C.LetIn (name, deannotate_term so, deannotate_term ta) + | C.AAppl (_,_,l) -> C.Appl (List.map deannotate_term l) + | C.AConst (_,_,uri, cookingsno) -> C.Const (uri, cookingsno) + | C.AAbst (_,_,uri) -> C.Abst uri + | C.AMutInd (_,_,uri,cookingsno,i) -> C.MutInd (uri,cookingsno,i) + | C.AMutConstruct (_,_,uri,cookingsno,i,j) -> + C.MutConstruct (uri,cookingsno,i,j) + | C.AMutCase (_,_,uri,cookingsno,i,outtype,te,pl) -> + C.MutCase (uri,cookingsno,i,deannotate_term outtype, + deannotate_term te, List.map deannotate_term pl) + | C.AFix (_,_,funno,ifl) -> + C.Fix (funno, List.map deannotate_inductiveFun ifl) + | C.ACoFix (_,_,funno,ifl) -> + C.CoFix (funno, List.map deannotate_coinductiveFun ifl) + +and deannotate_inductiveFun (name,index,ty,bo) = + (name, index, deannotate_term ty, deannotate_term bo) + +and deannotate_coinductiveFun (name,ty,bo) = + (name, deannotate_term ty, deannotate_term bo) +;; + +let deannotate_inductiveType (name, isinductive, arity, cons) = + (name, isinductive, deannotate_term arity, + List.map (fun (id,ty,recs) -> (id,deannotate_term ty, recs)) cons) +;; + +let deannotate_obj = + let module C = Cic in + function + C.ADefinition (_, _, id, bo, ty, params) -> + (match params with + C.Possible params -> + if !expect_possible_parameters then + C.Definition (id, deannotate_term bo, deannotate_term ty, params) + else + raise NotExpectingPossibleParameters + | C.Actual params -> + C.Definition (id, deannotate_term bo, deannotate_term ty, params) + ) + | C.AAxiom (_, _, id, ty, params) -> + C.Axiom (id, deannotate_term ty, params) + | C.AVariable (_, _, name, bo, ty) -> + C.Variable (name, + (match bo with None -> None | Some bo -> Some (deannotate_term bo)), + deannotate_term ty) + | C.ACurrentProof (_, _, name, conjs, bo, ty) -> + C.CurrentProof ( + name, List.map (fun (id,con) -> (id,deannotate_term con)) conjs, + deannotate_term bo, deannotate_term ty + ) + | C.AInductiveDefinition (_, _, tys, params, parno) -> + C.InductiveDefinition ( List.map deannotate_inductiveType tys, + params, parno) +;; diff --git a/helm/metadata/create2/mk_forward/getter.ml b/helm/metadata/create2/mk_forward/getter.ml new file mode 100644 index 000000000..894bf3ea9 --- /dev/null +++ b/helm/metadata/create2/mk_forward/getter.ml @@ -0,0 +1,63 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(******************************************************************************) + +let getter_url = ref Configuration.getter_url;; + +let update () = + (* deliver update request to http_getter *) + ClientHTTP.send (!getter_url ^ "update") +;; + +type format = + Normal + | GZipped +;; + +let getxml ?(format=Normal) ?(patchdtd=true) uri = + (* deliver getxml request to http_getter *) + ClientHTTP.get_and_save_to_tmp + (!getter_url ^ "getxml" ^ + "?uri=" ^ UriManager.string_of_uri uri ^ + "&format=" ^ (match format with Normal -> "normal" | GZipped -> "gzipped") ^ + "&patch_dtd=" ^ (match patchdtd with true -> "yes" | false -> "no") + ) +;; + +let register uri url = + (* deliver register request to http_getter *) + ClientHTTP.send + (!getter_url ^ "register" ^ + "?uri=" ^ (UriManager.string_of_uri uri) ^ + "&url=" ^ url) +;; diff --git a/helm/metadata/create2/mk_forward/getter.mli b/helm/metadata/create2/mk_forward/getter.mli new file mode 100644 index 000000000..6b1d2ca29 --- /dev/null +++ b/helm/metadata/create2/mk_forward/getter.mli @@ -0,0 +1,53 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* *) +(******************************************************************************) + +(* THE URL OF THE HTTP GETTER *) +val getter_url : string ref + +(* SIMPLE BINDINGS TO THE HTTP GETTER *) +(* synchronize with the servers *) +val update : unit -> unit + +type format = + Normal + | GZipped +;; + +(* get the xml file *) +(* defaults: format = Normal and patchdtd = true *) +val getxml : ?format:format -> ?patchdtd:bool -> UriManager.uri -> string + +(* adds an (URI -> URL) entry in the map from URIs to URLs *) +val register : UriManager.uri -> string -> unit diff --git a/helm/metadata/create2/mk_forward/mk_forward.ml b/helm/metadata/create2/mk_forward/mk_forward.ml new file mode 100644 index 000000000..294746124 --- /dev/null +++ b/helm/metadata/create2/mk_forward/mk_forward.ml @@ -0,0 +1,392 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 03/04/2001 *) +(* *) +(* Missing description *) +(* *) +(******************************************************************************) + +let iteri foo = + let counter = ref 0 in + List.iter (function e -> incr counter ; foo e !counter) +;; + +let pathname_of_uri uristring = + "forward" ^ + Str.replace_first (Str.regexp "^cic:") "" uristring +;; + +let make_dirs dirpath = + ignore (Unix.system ("mkdir -p \"" ^ dirpath ^ "\"")) +;; + +module UriHash = + struct + type classification = + Backbone + | Branch + | InConclusion + | InHypothesis + | InBody + ;; + +let soften_classification = + function + Backbone -> InConclusion + | Branch -> InHypothesis + | InBody -> assert false + | k -> k +;; + + let hash = Hashtbl.create 117 ;; + + let add_uri uri kind = + let old_kinds = + try + Hashtbl.find hash uri + with + Not_found -> [] + in + let new_kinds = + match kind,old_kinds with + InBody,[] -> [InBody] + | InBody,_ -> old_kinds + | k,_ when List.mem k old_kinds -> old_kinds + | k,_ -> k::old_kinds + in + Hashtbl.replace hash uri new_kinds + ;; + + (* It also removes every element in the hash *) + let uris_fold foo init = + let xml_element_name_of_kind = + function + Backbone -> "MainConclusion" + | Branch -> "MainHypothesis" + | InConclusion -> "InConclusion" + | InHypothesis -> "InHypothesis" + | InBody -> "InBody" + in + let res = + Hashtbl.fold + (fun uri kinds i -> + List.fold_left + (fun j kind -> + foo j uri (xml_element_name_of_kind kind) + ) i kinds + ) hash init + in + Hashtbl.clear hash ; + res + ;; + end +;; + +let output_content () = + UriHash.uris_fold + (fun i uri kind -> + [< Xml.xml_nempty "h:refObj" [] + (Xml.xml_empty "h:Occurrence" + ["rdf:about","http://www.cs.unibo.it/helm/schemas/schema-h.rdf#" ^ kind ; + "rdf:value",uri] + ) ; + i + >] + ) [<>] +;; + +let output_file cic_string_uri rdf_string_uri = + let module U = UriManager in + let module X = Xml in + let content = output_content () in + let rdf_uri = U.uri_of_string rdf_string_uri in + make_dirs (pathname_of_uri (U.buri_of_uri rdf_uri)) ; + X.pp + [< X.xml_cdata "\n" ; + X.xml_nempty "rdf:RDF" + ["xml:lang","en" ; + "xmlns:rdf","http://www.w3.org/1999/02/22-rdf-syntax-ns#"; + "xmlns:h","http:/www.cs.unibo.it/helm/schemas/schema-h.rdf#"] + + (try + Stream.empty content ; (* raise Stream.failure if not empty *) + X.xml_empty "h:Object" ["rdf:about",cic_string_uri] + with + Stream.Failure -> + X.xml_nempty "h:Object" ["rdf:about",cic_string_uri] content + ) + >] + (Some (pathname_of_uri rdf_string_uri ^ ".xml")) +;; + +let get_obj uri = + let cicfilename = Getter.getxml uri in + let res = + match CicParser.term_of_xml cicfilename uri false with + (annobj, None) -> + Deannotate.deannotate_obj annobj + | _ -> assert false + in + Unix.unlink cicfilename ; + res +;; + +let add_every_constructor uri typeno kind = + let module C = Cic in + match (get_obj uri) with + (C.InductiveDefinition (itys,_,_)) -> + let string_uri = UriManager.string_of_uri uri in + let sn = string_of_int (typeno + 1) in + let (_,_,_,cons) = List.nth itys typeno in + iteri + (fun (_,cty,_) m -> + let sm = string_of_int m in + UriHash.add_uri + (string_uri ^ "#xpointer(1/" ^ sn ^ "/" ^ sm ^ ")") + kind + ) cons + | _ -> assert false +;; + +let process_type term = + let module U = UriManager in + let module H = UriHash in + let module C = Cic in + let rec process_type_aux kind = + function + | C.Var uri -> + H.add_uri (U.string_of_uri uri) kind + | C.Cast (te,_) -> + (* type ignored *) + process_type_aux kind te + | C.Prod (_,sou,ta) -> + let (source_kind,target_kind) = + match kind with + H.Backbone -> (H.Branch,H.Backbone) + | H.Branch -> (H.InHypothesis,H.InHypothesis) + | H.InBody -> assert false + | k -> (k,k) + in + process_type_aux source_kind sou ; + process_type_aux target_kind ta + | C.Lambda (_,sou,ta) -> + let kind' = H.soften_classification kind in + process_type_aux kind' sou ; + process_type_aux kind' ta + | C.LetIn (_,te,ta)-> + let kind' = H.soften_classification kind in + process_type_aux kind' te ; + process_type_aux kind ta + | C.Appl (he::tl) -> + let kind' = H.soften_classification kind in + process_type_aux kind he ; + List.iter (process_type_aux kind') tl + | C.Appl _ -> assert false + | C.Const (uri,_) -> + UriHash.add_uri (U.string_of_uri uri) kind + | C.Abst _ -> assert false + | C.MutInd (uri,_,typeno) -> + H.add_uri + (U.string_of_uri uri ^ "#xpointer(1/" ^ + string_of_int (typeno + 1) ^ ")") + kind + | C.MutConstruct (uri,_,typeno,consno) -> + H.add_uri + (U.string_of_uri uri ^ "#xpointer(1/" ^ + string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")") + kind + | C.MutCase (uri,_,typeno,_,term,patterns) -> + (* outtype ignored *) + let kind' = H.soften_classification kind in + add_every_constructor uri typeno kind' ; + process_type_aux kind' term ; + List.iter (process_type_aux kind') patterns + | C.Fix (_,funs) -> + let kind' = H.soften_classification kind in + List.iter + (function (_,_,bo,ty) -> + process_type_aux kind' bo ; + process_type_aux kind' ty ; + ) funs + | C.CoFix (_,funs) -> + let kind' = H.soften_classification kind in + List.iter + (function (_,bo,ty) -> + process_type_aux kind' bo ; + process_type_aux kind' ty ; + ) funs + | _ -> () +in + process_type_aux H.Backbone (CicMiniReduction.letin_nf term) +;; + +let process_body = + let module U = UriManager in + let module H = UriHash in + let module C = Cic in + let rec process_body_aux = + function + C.Var uri -> + H.add_uri (U.string_of_uri uri) H.InBody + | C.Cast (te,ty) -> + process_body_aux te ; + process_body_aux ty + | C.Prod (_,sou,ta) -> + process_body_aux sou ; + process_body_aux ta + | C.Lambda (_,sou,ta) -> + process_body_aux sou ; + process_body_aux ta + | C.LetIn (_,te,ta)-> + process_body_aux te ; + process_body_aux ta + | C.Appl l -> + List.iter process_body_aux l + | C.Const (uri,_) -> + UriHash.add_uri (U.string_of_uri uri) H.InBody + | C.Abst _ -> assert false + | C.MutInd (uri,_,typeno) -> + H.add_uri + (U.string_of_uri uri ^ "#xpointer(1/" ^ + string_of_int (typeno + 1) ^ ")") + H.InBody + | C.MutConstruct (uri,_,typeno,consno) -> + H.add_uri + (U.string_of_uri uri ^ "#xpointer(1/" ^ + string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")") + H.InBody + | C.MutCase (uri,_,typeno,outtype,term,patterns) -> + add_every_constructor uri typeno H.InBody ; + process_body_aux outtype ; + process_body_aux term ; + List.iter process_body_aux patterns + | C.Fix (_,funs) -> + List.iter + (function (_,_,bo,ty) -> + process_body_aux bo ; + process_body_aux ty ; + ) funs + | C.CoFix (_,funs) -> + List.iter + (function (_,bo,ty) -> + process_body_aux bo ; + process_body_aux ty ; + ) funs + | _ -> () +in + process_body_aux +;; + +let process_obj string_uri = + let module U = UriManager in + let module C = Cic in + function + (C.Definition (_,bo,ty,_)) -> + process_type ty ; + process_body bo ; + output_file string_uri string_uri + | (C.Axiom (_,ty,_)) -> + process_type ty ; + output_file string_uri string_uri + | (C.Variable (_,bo,ty)) -> + process_type ty ; + begin + match bo with + (Some bo') -> process_body bo' + | _ -> () + end ; + output_file string_uri string_uri + | (C.InductiveDefinition _) as id -> + begin + let id' = + CicSubstitution.undebrujin_inductive_def + (U.uri_of_string string_uri) id + in + match id' with + (C.InductiveDefinition (itys,_,_)) -> + iteri + (fun (_,_,ty,cons) n -> + let sn = string_of_int n in + process_type ty ; + output_file + (string_uri ^ "#xpointer(1/" ^ sn ^ ")") + (string_uri ^ "," ^ sn) ; + iteri + (fun (_,cty,_) m -> + let sm = string_of_int m in + process_type cty ; + output_file + (string_uri ^ "#xpointer(1/" ^ sn ^ "/" ^ sm ^ ")") + (string_uri ^ "," ^ sn ^ "," ^ sm) + ) cons + ) itys + | _ -> assert false + end + | (C.CurrentProof _) -> assert false +;; + +let mk_forward string_uri = + let module U = UriManager in + print_endline ("Now computing metadata of " ^ string_uri) ; + flush stdout ; + let uri = U.uri_of_string string_uri in + let obj = get_obj uri in + process_obj string_uri obj +;; + +let _ = + let usage_msg = "usage: mk_forward[.opt] URI" in + let uri = ref "" in + Arg.parse [] + (fun x -> + if x = "" then + begin + prerr_string "No URI provided.\n" ; + Arg.usage [] usage_msg ; + exit (-1) + end + else if !uri = "" then + uri := x + else + begin + prerr_string "More than two arguments provided.\n" ; + Arg.usage [] usage_msg ; + exit (-1) + end + ) usage_msg ; + if !uri = "" then + begin + prerr_string "No URI provided.\n" ; + Arg.usage [] usage_msg ; + exit (-1) + end ; + mk_forward !uri +;; diff --git a/helm/metadata/create2/mk_forward/pxpUriResolver.ml b/helm/metadata/create2/mk_forward/pxpUriResolver.ml new file mode 100644 index 000000000..1e2fec918 --- /dev/null +++ b/helm/metadata/create2/mk_forward/pxpUriResolver.ml @@ -0,0 +1,266 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 11/10/2000 *) +(* *) +(* *) +(******************************************************************************) + +let resolve s = + let starts_with s s' = + if String.length s < String.length s' then + false + else + (String.sub s 0 (String.length s')) = s' + in + if starts_with s "http:" then + ClientHTTP.get_and_save_to_tmp s + else + s +;; + +(*PXP 1.0 +let url_syntax = + let enable_if = + function + `Not_recognized -> Neturl.Url_part_not_recognized + | `Allowed -> Neturl.Url_part_allowed + | `Required -> Neturl.Url_part_required + in + { Neturl.null_url_syntax with + Neturl.url_enable_scheme = enable_if `Allowed; + Neturl.url_enable_host = enable_if `Allowed; + Neturl.url_enable_path = Neturl.Url_part_required; + Neturl.url_accepts_8bits = true; + } +;; + +exception Unexpected;; (* Added when porting the file to PXP 1.1 *) + +let file_url_of_id xid = + let file_url_of_sysname sysname = + (* By convention, we can assume that sysname is a URL conforming + * to RFC 1738 with the exception that it may contain non-ASCII + * UTF-8 characters. + *) + try + Neturl.url_of_string url_syntax sysname + (* may raise Malformed_URL *) + with + Neturl.Malformed_URL -> raise Pxp_reader.Not_competent + in + let url = + match xid with + Pxp_types.Anonymous -> raise Pxp_reader.Not_competent + | Pxp_types.Public (_,sysname) -> + let sysname = resolve sysname in + if sysname <> "" then file_url_of_sysname sysname + else raise Pxp_reader.Not_competent + | Pxp_types.System sysname -> + let sysname = resolve sysname in + file_url_of_sysname sysname + | Pxp_types.Private pid -> raise Unexpected + in + let scheme = + try Neturl.url_scheme url with Not_found -> "file" in + let host = + try Neturl.url_host url with Not_found -> "" in + + if scheme <> "file" then raise Pxp_reader.Not_competent; + if host <> "" && host <> "localhost" then raise Pxp_reader.Not_competent; + + url +;; + +let from_file ?system_encoding utf8_filename = + + let r = + new Pxp_reader.resolve_as_file + ?system_encoding:system_encoding + ~url_of_id:file_url_of_id + () + in + + let utf8_abs_filename = + if utf8_filename <> "" && utf8_filename.[0] = '/' then + utf8_filename + else + Sys.getcwd() ^ "/" ^ utf8_filename + in + + let syntax = { Neturl.ip_url_syntax with Neturl.url_accepts_8bits = true } in + let url = Neturl.make_url + ~scheme:"file" + ~host:"localhost" + ~path:(Neturl.split_path utf8_abs_filename) + syntax + in + + let xid = Pxp_types.System (Neturl.string_of_url url) in + + + Pxp_yacc.ExtID(xid, r) +;; +*) + +(*PXP 1.1*) +(* csc_pxp_reader.ml is an exact copy of PXP pxp_reader.ml *) +(* The only reason is to loosen the interface *) + +class resolve_as_file + ?(file_prefix = (`Allowed :> Csc_pxp_reader.spec)) + ?(host_prefix = (`Allowed :> Csc_pxp_reader.spec)) + ?(system_encoding = `Enc_utf8) + ?(map_private_id = (fun _ -> raise Csc_pxp_reader.Not_competent)) + ?(open_private_id = (fun _ -> raise Csc_pxp_reader.Not_competent)) + () + = + + let url_syntax = + let enable_if = + function + `Not_recognized -> Neturl.Url_part_not_recognized + | `Allowed -> Neturl.Url_part_allowed + | `Required -> Neturl.Url_part_required + in + { Neturl.null_url_syntax with + Neturl.url_enable_scheme = enable_if file_prefix; + Neturl.url_enable_host = enable_if host_prefix; + Neturl.url_enable_path = Neturl.Url_part_required; + Neturl.url_accepts_8bits = true; + } + in + + let base_url_syntax = + { Neturl.null_url_syntax with + Neturl.url_enable_scheme = Neturl.Url_part_required; + Neturl.url_enable_host = Neturl.Url_part_allowed; + Neturl.url_enable_path = Neturl.Url_part_required; + Neturl.url_accepts_8bits = true; + } + in + + let default_base_url = + Neturl.make_url + ~scheme: "file" + ~host: "" + ~path: (Neturl.split_path (Sys.getcwd() ^ "/")) + base_url_syntax + in + + let file_url_of_id xid = + let module P = Csc_pxp_reader in + let module T = Pxp_types in + let file_url_of_sysname sysname = + (* By convention, we can assume that sysname is a URL conforming + * to RFC 1738 with the exception that it may contain non-ASCII + * UTF-8 characters. + *) + try + Neturl.url_of_string url_syntax sysname + (* may raise Malformed_URL *) + with + Neturl.Malformed_URL -> raise P.Not_competent + in + let url = + match xid with + T.Anonymous -> raise P.Not_competent + | T.Public (_,sysname) -> let sysname = resolve sysname in + if sysname <> "" then file_url_of_sysname sysname + else raise P.Not_competent + | T.System sysname -> let sysname = resolve sysname in + file_url_of_sysname sysname + | T.Private pid -> map_private_id pid + in + let scheme = + try Neturl.url_scheme url with Not_found -> "file" in + let host = + try Neturl.url_host url with Not_found -> "" in + + if scheme <> "file" then raise P.Not_competent; + if host <> "" && host <> "localhost" then raise P.Not_competent; + + url + in + + let channel_of_file_url xid url = + let module P = Csc_pxp_reader in + let module T = Pxp_types in + match xid with + T.Private pid -> open_private_id pid + | _ -> + ( try + let path_utf8 = + try Neturl.join_path (Neturl.url_path ~encoded:false url) + with Not_found -> raise P.Not_competent + in + + let path = + Netconversion.recode_string + ~in_enc: `Enc_utf8 + ~out_enc: system_encoding + path_utf8 in + (* May raise Malformed_code *) + + open_in_bin path, None + (* May raise Sys_error *) + + with + | Netconversion.Malformed_code -> assert false + (* should not happen *) + | Sys_error _ as e -> + raise (P.Not_resolvable e) + ) + in + + Csc_pxp_reader.resolve_read_url_channel + ~base_url: default_base_url + ~url_of_id: file_url_of_id + ~channel_of_url: channel_of_file_url + () +;; + +let from_file ?(alt = []) ?system_encoding ?enc utf8_filename = + let r = + new resolve_as_file + ?system_encoding:system_encoding + () + in + + let url = Csc_pxp_reader.make_file_url + ?system_encoding + ?enc + utf8_filename in + + let xid = Pxp_types.System (Neturl.string_of_url url) in + + Pxp_yacc.ExtID(xid, new Csc_pxp_reader.combine (r :: alt)) +;; + diff --git a/helm/metadata/create2/mk_forward/uriManager.ml b/helm/metadata/create2/mk_forward/uriManager.ml new file mode 100644 index 000000000..0fa24cfcd --- /dev/null +++ b/helm/metadata/create2/mk_forward/uriManager.ml @@ -0,0 +1,139 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* "cic:/a/b/c.con" => [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c" |] *) +type uri = string array;; + +let eq uri1 uri2 = + uri1 == uri2 +;; + +let string_of_uri uri = uri.(Array.length uri - 2);; +let name_of_uri uri = uri.(Array.length uri - 1);; +let buri_of_uri uri = uri.(Array.length uri - 3);; +let depth_of_uri uri = Array.length uri - 2;; + +(*CSC: ora e' diventato poco efficiente, migliorare *) +let relative_depth curi uri cookingsno = + let rec length_of_current_prefix l1 l2 = + match (l1, l2) with + (he1::tl1, he2::tl2) when he1 == he2 -> + 1 + length_of_current_prefix tl1 tl2 + | (_,_) -> 0 + in + depth_of_uri uri - + length_of_current_prefix + (Array.to_list (Array.sub curi 0 (Array.length curi - (2 + cookingsno)))) + (Array.to_list (Array.sub uri 0 (Array.length uri - 2))) + (*CSC: vecchio codice da eliminare + if eq curi uri then 0 + else + depth_of_uri uri - + length_of_current_prefix (Array.to_list curi) (Array.to_list uri) + *) +;; + +module OrderedStrings = + struct + type t = string + let compare (s1 : t) (s2 : t) = compare s1 s2 + end +;; + +module SetOfStrings = Map.Make(OrderedStrings);; + +(*CSC: commento obsoleto ed errato *) +(* Invariant: the map is the identity function, *) +(* i.e. (SetOfStrings.find str !set_of_uri) == str *) +let set_of_uri = ref SetOfStrings.empty;; +let set_of_prefixes = ref SetOfStrings.empty;; + +(* similar to uri_of_string, but used for prefixes of uris *) +let normalize prefix = + try + SetOfStrings.find prefix !set_of_prefixes + with + Not_found -> + set_of_prefixes := SetOfStrings.add prefix prefix !set_of_prefixes ; + prefix +;; + +exception IllFormedUri of string;; + +let mk_prefixes str = + let rec aux curi = + function + [he] -> + let prefix_uri = curi ^ "/" ^ he + and name = List.hd (Str.split (Str.regexp "\.") he) in + [ normalize prefix_uri ; name ] + | he::tl -> + let prefix_uri = curi ^ "/" ^ he in + (normalize prefix_uri)::(aux prefix_uri tl) + | _ -> raise (IllFormedUri str) + in + let tokens = (Str.split (Str.regexp "/") str) in + (* ty = "cic:" *) + let (ty, sp) = (List.hd tokens, List.tl tokens) in + aux ty sp +;; + +let uri_of_string str = + try + SetOfStrings.find str !set_of_uri + with + Not_found -> + let uri = Array.of_list (mk_prefixes str) in + set_of_uri := SetOfStrings.add str uri !set_of_uri ; + uri +;; + +let cicuri_of_uri uri = + let completeuri = string_of_uri uri in + let newcompleteuri = + (Str.replace_first (Str.regexp "\.types$") "" + (Str.replace_first (Str.regexp "\.ann$") "" completeuri)) + in + if completeuri = newcompleteuri then + uri + else + let newuri = Array.copy uri in + newuri.(Array.length uri - 2) <- newcompleteuri ; + newuri +;; + +let annuri_of_uri uri = + let completeuri = string_of_uri uri in + if Str.string_match (Str.regexp ".*\.ann$") completeuri 0 then + uri + else + let newuri = Array.copy uri in + newuri.(Array.length uri - 2) <- completeuri ^ ".ann" ; + newuri +;; + +let uri_is_annuri uri = + Str.string_match (Str.regexp ".*\.ann$") (string_of_uri uri) 0 +;; diff --git a/helm/metadata/create2/mk_forward/uriManager.mli b/helm/metadata/create2/mk_forward/uriManager.mli new file mode 100644 index 000000000..2cdd27e3d --- /dev/null +++ b/helm/metadata/create2/mk_forward/uriManager.mli @@ -0,0 +1,51 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +type uri + +val eq : uri -> uri -> bool + +val uri_of_string : string -> uri + +val string_of_uri : uri -> string (* complete uri *) +val name_of_uri : uri -> string (* name only (without extension)*) +val buri_of_uri : uri -> string (* base uri only *) +val depth_of_uri : uri -> int (* length of the path *) + +(* relative_depth curi uri cookingsno *) +(* is the number of times to cook uri to use it when the current uri is curi *) +(* cooked cookingsno times *) +val relative_depth : uri -> uri -> int -> int + +(* given an uri, returns the uri of the corresponding cic file, *) +(* i.e. removes the [.types][.ann] suffix *) +val cicuri_of_uri : uri -> uri + +(* given an uri, returns the uri of the corresponding annotation file, *) +(* i.e. adds the .ann suffix if not already present *) +val annuri_of_uri : uri -> uri + +(* given an uri, tells if it refers to an annotation *) +val uri_is_annuri : uri -> bool diff --git a/helm/metadata/create2/mk_forward/xml.ml b/helm/metadata/create2/mk_forward/xml.ml new file mode 100644 index 000000000..302aef23f --- /dev/null +++ b/helm/metadata/create2/mk_forward/xml.ml @@ -0,0 +1,101 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* A tactic to print Coq objects in XML *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 18/10/2000 *) +(* *) +(* This module defines a pretty-printer and the stream of commands to the pp *) +(* *) +(******************************************************************************) + + +(* the type token for XML cdata, empty elements and not-empty elements *) +(* Usage: *) +(* Str cdata *) +(* Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen] *) +(* NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *) +(* content *) +type token = Str of string + | Empty of string * (string * string) list + | NEmpty of string * (string * string) list * token Stream.t +;; + +(* currified versions of the constructors make the code more readable *) +let xml_empty name attrs = [< 'Empty(name,attrs) >] +let xml_nempty name attrs content = [< 'NEmpty(name,attrs,content) >] +let xml_cdata str = [< 'Str str >] + +(* Usage: *) +(* pp tokens None pretty prints the output on stdout *) +(* pp tokens (Some filename) pretty prints the output on the file filename *) +let pp ?(quiet=false) strm fn = + let channel = ref stdout in + let rec pp_r m = + parser + [< 'Str a ; s >] -> + print_spaces m ; + fprint_string (a ^ "\n") ; + pp_r m s + | [< 'Empty(n,l) ; s >] -> + print_spaces m ; + fprint_string ("<" ^ n) ; + List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l; + fprint_string "/>\n" ; + pp_r m s + | [< 'NEmpty(n,l,c) ; s >] -> + print_spaces m ; + fprint_string ("<" ^ n) ; + List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l; + fprint_string ">\n" ; + pp_r (m+1) c ; + print_spaces m ; + fprint_string ("\n") ; + pp_r m s + | [< >] -> () + and print_spaces m = + for i = 1 to m do fprint_string " " done + and fprint_string str = + output_string !channel str + in + match fn with + Some filename -> + channel := open_out filename ; + pp_r 0 strm ; + close_out !channel ; + if not quiet then + begin + print_string ("\nWriting on file \"" ^ filename ^ + "\" was succesfull\n"); + flush stdout + end + | None -> + pp_r 0 strm +;; diff --git a/helm/metadata/create2/mk_forward/xml.mli b/helm/metadata/create2/mk_forward/xml.mli new file mode 100644 index 000000000..a68110b29 --- /dev/null +++ b/helm/metadata/create2/mk_forward/xml.mli @@ -0,0 +1,60 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* A tactic to print Coq objects in XML *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 18/10/2000 *) +(* *) +(* This module defines a pretty-printer and the stream of commands to the pp *) +(* *) +(******************************************************************************) + +(* Tokens for XML cdata, empty elements and not-empty elements *) +(* Usage: *) +(* Str cdata *) +(* Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen] *) +(* NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *) +(* content *) +type token = + | Str of string + | Empty of string * (string * string) list + | NEmpty of string * (string * string) list * token Stream.t + +(* currified versions of the token constructors make the code more readable *) +val xml_empty : string -> (string * string) list -> token Stream.t +val xml_nempty : + string -> (string * string) list -> token Stream.t -> token Stream.t +val xml_cdata : string -> token Stream.t + +(* The pretty printer for streams of token *) +(* Usage: *) +(* pp tokens None pretty prints the output on stdout *) +(* pp tokens (Some filename) pretty prints the output on the file filename *) +val pp : ?quiet:bool -> token Stream.t -> string option -> unit diff --git a/helm/metadata/create2/mkindex.sh b/helm/metadata/create2/mkindex.sh new file mode 100755 index 000000000..3a814ba17 --- /dev/null +++ b/helm/metadata/create2/mkindex.sh @@ -0,0 +1,4 @@ +#!/bin/bash + +echo `find . -name "*.xml"` | ../uris_of_filenames.pl $1 > rdf_index.txt +echo `find . -name "*.xml.gz"` | ../uris_of_filenames.pl $1 -gz >> rdf_index.txt diff --git a/helm/metadata/create2/touch/.cvsignore b/helm/metadata/create2/touch/.cvsignore new file mode 100644 index 000000000..cf77f4b1d --- /dev/null +++ b/helm/metadata/create2/touch/.cvsignore @@ -0,0 +1 @@ +*.cmi *.cmo *.cmx .depend touch touch.opt configuration.ml diff --git a/helm/metadata/create2/touch/Makefile b/helm/metadata/create2/touch/Makefile new file mode 100644 index 000000000..2d7ef5a8a --- /dev/null +++ b/helm/metadata/create2/touch/Makefile @@ -0,0 +1,46 @@ +OCAMLOPTIONS = -package netstring -package netclient -package pxp + +OCAMLDEP = ocamldep +OCAMLFIND = ocamlfind +OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) +OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS) + +all: touch +opt: touch.opt + +DEPOBJS = csc_pxp_reader.ml configuration.ml \ + clientHTTP.ml clientHTTP.mli cic.ml deannotate.ml \ + uriManager.ml uriManager.mli getter.ml getter.mli \ + pxpUriResolver.ml cicParser3.ml cicParser3.mli \ + cicParser2.ml cicParser2.mli cicParser.ml \ + cicParser.mli touch.ml + +TOUCHOBJS = csc_pxp_reader.cmo configuration.cmo \ + clientHTTP.cmo cic.cmo deannotate.cmo \ + uriManager.cmo getter.cmo pxpUriResolver.ml \ + cicParser3.cmo cicParser2.cmo cicParser.cmo \ + touch.cmo + +depend: + $(OCAMLDEP) $(DEPOBJS) > .depend + +touch: $(TOUCHOBJS) + $(OCAMLC) -linkpkg -o touch $(TOUCHOBJS) + +touch.opt: $(TOUCHOBJS:.cmo=.cmx) + $(OCAMLOPT) -linkpkg -o touch.opt $(TOUCHOBJS:.cmo=.cmx) + +.SUFFIXES: .ml .mli .cmo .cmi .cmx +.ml.cmo: + $(OCAMLC) -c $< +.mli.cmi: + $(OCAMLC) -c $< +.ml.cmx: + $(OCAMLOPT) -c $< + +clean: + rm -f *.cm[iox] *.o touch touch.opt + +.PHONY: clean + +include .depend diff --git a/helm/metadata/create2/touch/cic.ml b/helm/metadata/create2/touch/cic.ml new file mode 100644 index 000000000..8c08b0075 --- /dev/null +++ b/helm/metadata/create2/touch/cic.ml @@ -0,0 +1,162 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 14/06/2000 *) +(* *) +(* This module defines the internal representation of the objects (variables, *) +(* blocks of (co)inductive definitions and constants) and the terms of cic *) +(* *) +(******************************************************************************) + +(* STUFF TO MANAGE IDENTIFIERS *) +type id = string (* the abstract type of the (annotated) node identifiers *) +type anntarget = + Object of annobj + | Term of annterm + +(* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *) +and sort = + Prop + | Set + | Type +and name = + Name of string + | Anonimous +and term = + Rel of int (* DeBrujin index *) + | Var of UriManager.uri (* uri *) + | Meta of int (* numeric id *) + | Sort of sort (* sort *) + | Implicit (* *) + | Cast of term * term (* value, type *) + | Prod of name * term * term (* binder, source, target *) + | Lambda of name * term * term (* binder, source, target *) + | LetIn of name * term * term (* binder, term, target *) + | Appl of term list (* arguments *) + | Const of UriManager.uri * int (* uri, number of cookings*) + | Abst of UriManager.uri (* uri *) + | MutInd of UriManager.uri * int * int (* uri, cookingsno, typeno*) + | MutConstruct of UriManager.uri * int * (* uri, cookingsno, *) + int * int (* typeno, consno *) + (*CSC: serve cookingsno?*) + | MutCase of UriManager.uri * int * (* ind. uri, cookingsno, *) + int * (* ind. typeno, *) + term * term * (* outtype, ind. term *) + term list (* patterns *) + | Fix of int * inductiveFun list (* funno, functions *) + | CoFix of int * coInductiveFun list (* funno, functions *) +and obj = + Definition of string * term * term * (* id, value, type, *) + (int * UriManager.uri list) list (* parameters *) + | Axiom of string * term * + (int * UriManager.uri list) list (* id, type, parameters *) + | Variable of string * term option * term (* name, body, type *) + | CurrentProof of string * (int * term) list * (* name, conjectures, *) + term * term (* value, type *) + | InductiveDefinition of inductiveType list * (* inductive types, *) + (int * UriManager.uri list) list * int (* parameters, n ind. pars *) +and inductiveType = + string * bool * term * (* typename, inductive, arity *) + constructor list (* constructors *) +and constructor = + string * term * bool list option ref (* id, type, really recursive *) +and inductiveFun = + string * int * term * term (* name, ind. index, type, body *) +and coInductiveFun = + string * term * term (* name, type, body *) + +and annterm = + ARel of id * annotation option ref * + int * string option (* DeBrujin index, binder *) + | AVar of id * annotation option ref * + UriManager.uri (* uri *) + | AMeta of id * annotation option ref * int (* numeric id *) + | ASort of id * annotation option ref * sort (* sort *) + | AImplicit of id * annotation option ref (* *) + | ACast of id * annotation option ref * + annterm * annterm (* value, type *) + | AProd of id * annotation option ref * + name * annterm * annterm (* binder, source, target *) + | ALambda of id * annotation option ref * + name * annterm * annterm (* binder, source, target *) + | ALetIn of id * annotation option ref * + name * annterm * annterm (* binder, term, target *) + | AAppl of id * annotation option ref * + annterm list (* arguments *) + | AConst of id * annotation option ref * + UriManager.uri * int (* uri, number of cookings*) + | AAbst of id * annotation option ref * + UriManager.uri (* uri *) + | AMutInd of id * annotation option ref * + UriManager.uri * int * int (* uri, cookingsno, typeno*) + | AMutConstruct of id * annotation option ref * + UriManager.uri * int * (* uri, cookingsno, *) + int * int (* typeno, consno *) + (*CSC: serve cookingsno?*) + | AMutCase of id * annotation option ref * + UriManager.uri * int * (* ind. uri, cookingsno *) + int * (* ind. typeno, *) + annterm * annterm * (* outtype, ind. term *) + annterm list (* patterns *) + | AFix of id * annotation option ref * + int * anninductiveFun list (* funno, functions *) + | ACoFix of id * annotation option ref * + int * anncoInductiveFun list (* funno, functions *) +and annobj = + ADefinition of id * annotation option ref * + string * (* id, *) + annterm * annterm * (* value, type, *) + (int * UriManager.uri list) list exactness (* parameters *) + | AAxiom of id * annotation option ref * + string * annterm * (* id, type *) + (int * UriManager.uri list) list (* parameters *) + | AVariable of id * annotation option ref * + string * annterm option * annterm (* name, body, type *) + | ACurrentProof of id * annotation option ref * + string * (int * annterm) list * (* name, conjectures, *) + annterm * annterm (* value, type *) + | AInductiveDefinition of id * + annotation option ref * anninductiveType list * (* inductive types , *) + (int * UriManager.uri list) list * int (* parameters,n ind. pars*) +and anninductiveType = + string * bool * annterm * (* typename, inductive, arity *) + annconstructor list (* constructors *) +and annconstructor = + string * annterm * bool list option ref (* id, type, really recursive *) +and anninductiveFun = + string * int * annterm * annterm (* name, ind. index, type, body *) +and anncoInductiveFun = + string * annterm * annterm (* name, type, body *) +and annotation = + string +and 'a exactness = + Possible of 'a (* an approximation to something *) + | Actual of 'a (* something *) +;; diff --git a/helm/metadata/create2/touch/cicParser.ml b/helm/metadata/create2/touch/cicParser.ml new file mode 100644 index 000000000..bf75243ec --- /dev/null +++ b/helm/metadata/create2/touch/cicParser.ml @@ -0,0 +1,95 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This is the main (top level) module of a parser for cic objects from xml *) +(* files to the internal representation. It uses the modules cicParser2 *) +(* (objects level) and cicParser3 (terms level) *) +(* *) +(******************************************************************************) + +exception Warnings;; + +class warner = + object + method warn w = + print_endline ("WARNING: " ^ w) ; + (raise Warnings : unit) + end +;; + +exception EmptyUri;; + +(* given an uri u it returns the list of tokens of the base uri of u *) +(* e.g.: token_of_uri "cic:/a/b/c/d.xml" returns ["a" ; "b" ; "c"] *) +let tokens_of_uri uri = + let uri' = UriManager.string_of_uri uri in + let rec chop_list = + function + [] -> raise EmptyUri + | he::[fn] -> [he] + | he::tl -> he::(chop_list tl) + in + let trimmed_uri = Str.replace_first (Str.regexp "cic:") "" uri' in + let list_of_tokens = Str.split (Str.regexp "/") trimmed_uri in + chop_list list_of_tokens +;; + +(* given the filename of an xml file of a cic object it returns its internal *) +(* representation. process_annotations is true if the annotations do really *) +(* matter *) +let term_of_xml filename uri process_annotations = + let module Y = Pxp_yacc in + try + let d = + (* sets the current base uri to resolve relative URIs *) + CicParser3.current_sp := tokens_of_uri uri ; + CicParser3.current_uri := uri ; + CicParser3.process_annotations := process_annotations ; + CicParser3.ids_to_targets := + if process_annotations then Some (Hashtbl.create 500) else None ; + let config = {Y.default_config with Y.warner = new warner} in + Y.parse_document_entity config +(*PXP (Y.ExtID (Pxp_types.System filename, + new Pxp_reader.resolve_as_file ~url_of_id ())) +*) (PxpUriResolver.from_file filename) + CicParser3.domspec + in + let ids_to_targets = !CicParser3.ids_to_targets in + let res = (CicParser2.get_term d#root, ids_to_targets) in + CicParser3.ids_to_targets := None ; (* let's help the GC *) + res + with + e -> + print_endline ("Filename: " ^ filename ^ "\nException: ") ; + print_endline (Pxp_types.string_of_exn e) ; + raise e +;; diff --git a/helm/metadata/create2/touch/cicParser.mli b/helm/metadata/create2/touch/cicParser.mli new file mode 100644 index 000000000..0078f6f33 --- /dev/null +++ b/helm/metadata/create2/touch/cicParser.mli @@ -0,0 +1,44 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 22/03/2000 *) +(* *) +(* This is the main (top level) module of a parser for cic objects from xml *) +(* files to the internal representation. It uses the modules cicParser2 *) +(* (objects level) and cicParser3 (terms level) *) +(* *) +(******************************************************************************) + +(* given the filename of an xml file of a cic object and it's uri, it returns *) +(* its internal annotated representation. The boolean is set to true if the *) +(* annotations do really matter *) +val term_of_xml : + string -> UriManager.uri -> bool -> + Cic.annobj * (Cic.id, Cic.anntarget) Hashtbl.t option diff --git a/helm/metadata/create2/touch/cicParser2.ml b/helm/metadata/create2/touch/cicParser2.ml new file mode 100644 index 000000000..562f79bba --- /dev/null +++ b/helm/metadata/create2/touch/cicParser2.ml @@ -0,0 +1,289 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This module is the objects level of a parser for cic objects from xml *) +(* files to the internal representation. It uses the module cicParser3 *) +(* cicParser3 (terms level) and it is used only through cicParser2 (top *) +(* level). *) +(* *) +(******************************************************************************) + +exception IllFormedXml of int;; +exception NotImplemented;; + +(* Utility functions that transform a Pxp attribute into something useful *) + +(* mk_absolute_uris "n1: v1 ... vn n2 : u1 ... un ...." *) +(* returns [(n1,[absolute_uri_for_v1 ; ... ; absolute_uri_for_vn]) ; (n2,...) *) +let mk_absolute_uris s = + let l = (Str.split (Str.regexp ":") s) in + let absolute_of_relative n v = + let module P3 = CicParser3 in + let rec mkburi = + function + (0,_) -> "/" + | (n,he::tl) when n > 0 -> + "/" ^ he ^ mkburi (n - 1, tl) + | _ -> raise (IllFormedXml 12) + in + let m = List.length !P3.current_sp - (int_of_string n) in + let buri = mkburi (m, !P3.current_sp) in + UriManager.uri_of_string ("cic:" ^ buri ^ v ^ ".var") + in + let rec absolutize = + function + [] -> [] + | [no ; vs] -> + let vars = (Str.split (Str.regexp " ") vs) in + [(int_of_string no, List.map (absolute_of_relative no) vars)] + | no::vs::tl -> + let vars = (Str.split (Str.regexp " ") vs) in + let rec add_prefix = + function + [no2] -> ([], no2) + | he::tl -> + let (pvars, no2) = add_prefix tl in + ((absolute_of_relative no he)::pvars, no2) + | _ -> raise (IllFormedXml 11) + in + let (pvars, no2) = add_prefix vars in + (int_of_string no, pvars)::(absolutize (no2::tl)) + | _ -> raise (IllFormedXml 10) + in + (* last parameter must be applied first *) + absolutize l +;; + +let option_uri_list_of_attr a1 a2 = + let module T = Pxp_types in + let parameters = + match a1 with + T.Value s -> mk_absolute_uris s + | _ -> raise (IllFormedXml 0) + in + match a2 with + T.Value "POSSIBLE" -> Cic.Possible parameters + | T.Implied_value -> Cic.Actual parameters + | _ -> raise (IllFormedXml 0) +;; + +let uri_list_of_attr a = + let module T = Pxp_types in + match a with + T.Value s -> mk_absolute_uris s + | _ -> raise (IllFormedXml 0) +;; + +let string_of_attr a = + let module T = Pxp_types in + match a with + T.Value s -> s + | _ -> raise (IllFormedXml 0) +;; + +let int_of_attr a = + int_of_string (string_of_attr a) +;; + +let bool_of_attr a = + bool_of_string (string_of_attr a) +;; + +(* Other utility functions *) + +let get_content n = + match n#sub_nodes with + [ t ] -> t + | _ -> raise (IllFormedXml 1) +;; + +let register_id id node = + if !CicParser3.process_annotations then + match !CicParser3.ids_to_targets with + None -> assert false + | Some ids_to_targets -> + Hashtbl.add ids_to_targets id (Cic.Object node) +;; + +(* Functions that, given the list of sons of a node of the cic dom (objects *) +(* level), retrieve the internal representation associated to the node. *) +(* Everytime a cic term subtree is found, it is translated to the internal *) +(* representation using the method to_cic_term defined in cicParser3. *) +(* Each function raise IllFormedXml if something goes wrong, but this should *) +(* be impossible due to the presence of the dtd *) +(* The functions should really be obvious looking at their name and the cic *) +(* dtd *) + +(* called when a CurrentProof is found *) +let get_conjs_value_type l = + let rec rget (c, v, t) l = + let module D = Pxp_document in + match l with + [] -> (c, v, t) + | conj::tl when conj#node_type = D.T_element "Conjecture" -> + let no = int_of_attr (conj#attribute "no") + and typ = (get_content conj)#extension#to_cic_term in + rget ((no, typ)::c, v, t) tl + | value::tl when value#node_type = D.T_element "body" -> + let v' = (get_content value)#extension#to_cic_term in + (match v with + None -> rget (c, Some v', t) tl + | _ -> raise (IllFormedXml 2) + ) + | typ::tl when typ#node_type = D.T_element "type" -> + let t' = (get_content typ)#extension#to_cic_term in + (match t with + None -> rget (c, v, Some t') tl + | _ -> raise (IllFormedXml 3) + ) + | _ -> raise (IllFormedXml 4) + in + match rget ([], None, None) l with + (c, Some v, Some t) -> (c, v, t) + | _ -> raise (IllFormedXml 5) +;; + +(* used only by get_inductive_types; called one time for each inductive *) +(* definitions in a block of inductive definitions *) +let get_names_arity_constructors l = + let rec rget (a,c) l = + let module D = Pxp_document in + match l with + [] -> (a, c) + | arity::tl when arity#node_type = D.T_element "arity" -> + let a' = (get_content arity)#extension#to_cic_term in + rget (Some a',c) tl + | con::tl when con#node_type = D.T_element "Constructor" -> + let id = string_of_attr (con#attribute "name") + and ty = (get_content con)#extension#to_cic_term in + rget (a,(id,ty,ref None)::c) tl + | _ -> raise (IllFormedXml 9) + in + match rget (None,[]) l with + (Some a, c) -> (a, List.rev c) + | _ -> raise (IllFormedXml 8) +;; + +(* called when an InductiveDefinition is found *) +let rec get_inductive_types = + function + [] -> [] + | he::tl -> + let tyname = string_of_attr (he#attribute "name") + and inductive = bool_of_attr (he#attribute "inductive") + and (arity,cons) = + get_names_arity_constructors (he#sub_nodes) + in + (tyname,inductive,arity,cons)::(get_inductive_types tl) (*CSC 0 a caso *) +;; + +(* This is the main function and also the only one used directly from *) +(* cicParser. Given the root of the dom tree, it returns the internal *) +(* representation of the cic object described in the tree *) +(* It uses the previous functions and the to_cic_term method defined *) +(* in cicParser3 (used for subtrees that encode cic terms) *) +let rec get_term n = + let module D = Pxp_document in + let module C = Cic in + let ntype = n # node_type in + match ntype with + D.T_element "Definition" -> + let id = string_of_attr (n # attribute "name") + and params = + option_uri_list_of_attr (n#attribute "params") (n#attribute "paramMode") + and (value, typ) = + let sons = n#sub_nodes in + match sons with + [v ; t] when + v#node_type = D.T_element "body" && + t#node_type = D.T_element "type" -> + let v' = get_content v + and t' = get_content t in + (v'#extension#to_cic_term, t'#extension#to_cic_term) + | _ -> raise (IllFormedXml 6) + and xid = string_of_attr (n#attribute "id") in + let res = C.ADefinition (xid, ref None, id, value, typ, params) in + register_id xid res ; + res + | D.T_element "Axiom" -> + let id = string_of_attr (n # attribute "name") + and params = uri_list_of_attr (n # attribute "params") + and typ = + (get_content (get_content n))#extension#to_cic_term + and xid = string_of_attr (n#attribute "id") in + let res = C.AAxiom (xid, ref None, id, typ, params) in + register_id xid res ; + res + | D.T_element "CurrentProof" -> + let name = string_of_attr (n#attribute "name") + and xid = string_of_attr (n#attribute "id") in + let sons = n#sub_nodes in + let (conjs, value, typ) = get_conjs_value_type sons in + let res = C.ACurrentProof (xid, ref None, name, conjs, value, typ) in + register_id xid res ; + res + | D.T_element "InductiveDefinition" -> + let sons = n#sub_nodes + and xid = string_of_attr (n#attribute "id") in + let inductiveTypes = get_inductive_types sons + and params = uri_list_of_attr (n#attribute "params") + and nparams = int_of_attr (n#attribute "noParams") in + let res = + C.AInductiveDefinition (xid, ref None, inductiveTypes, params, nparams) + in + register_id xid res ; + res + | D.T_element "Variable" -> + let name = string_of_attr (n#attribute "name") + and xid = string_of_attr (n#attribute "id") + and (body, typ) = + let sons = n#sub_nodes in + match sons with + [b ; t] when + b#node_type = D.T_element "body" && + t#node_type = D.T_element "type" -> + let b' = get_content b + and t' = get_content t in + (Some (b'#extension#to_cic_term), t'#extension#to_cic_term) + | [t] when t#node_type = D.T_element "type" -> + let t' = get_content t in + (None, t'#extension#to_cic_term) + | _ -> raise (IllFormedXml 6) + in + let res = C.AVariable (xid,ref None,name,body,typ) in + register_id xid res ; + res + | D.T_element _ + | D.T_data + | _ -> + raise (IllFormedXml 7) +;; diff --git a/helm/metadata/create2/touch/cicParser2.mli b/helm/metadata/create2/touch/cicParser2.mli new file mode 100644 index 000000000..be0a00054 --- /dev/null +++ b/helm/metadata/create2/touch/cicParser2.mli @@ -0,0 +1,57 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This module is the objects level of a parser for cic objects from xml *) +(* files to the internal representation. It uses the module cicParser3 *) +(* cicParser3 (terms level) and it is used only through cicParser2 (top *) +(* level). *) +(* *) +(******************************************************************************) + +exception IllFormedXml of int +exception NotImplemented + +(* This is the main function and also the only one used directly from *) +(* cicParser. Given the root of the dom tree, it returns the internal *) +(* representation of the cic object described in the tree *) +(* It uses the previous functions and the to_cic_term method defined *) +(* in cicParser3 (used for subtrees that encode cic terms) *) +val get_term : + < attribute : string -> Pxp_types.att_value; + node_type : Pxp_document.node_type; + sub_nodes : < attribute : string -> Pxp_types.att_value; + node_type : Pxp_document.node_type; + sub_nodes : CicParser3.cic_term Pxp_document.node list; + .. > + list; + .. > -> + Cic.annobj diff --git a/helm/metadata/create2/touch/cicParser3.ml b/helm/metadata/create2/touch/cicParser3.ml new file mode 100644 index 000000000..ff356b13e --- /dev/null +++ b/helm/metadata/create2/touch/cicParser3.ml @@ -0,0 +1,565 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This module is the terms level of a parser for cic objects from xml *) +(* files to the internal representation. It is used by the module cicParser2 *) +(* (objects level). It defines an extension of the standard dom using the *) +(* object-oriented extension machinery of markup: an object with a method *) +(* to_cic_term that returns the internal representation of the subtree is *) +(* added to each node of the dom tree *) +(* *) +(******************************************************************************) + +exception IllFormedXml of int;; + +(* The hashtable from the current identifiers to the object or the terms *) +let ids_to_targets = ref None;; + +(* The list of tokens of the current section path. *) +(* Used to resolve relative URIs *) +let current_sp = ref [];; + +(* The uri of the object been parsed *) +let current_uri = ref (UriManager.uri_of_string "cic:/.xml");; + +(* True if annotation really matter *) +let process_annotations = ref false;; + +(* Utility functions to map a markup attribute to something useful *) + +let cic_attr_of_xml_attr = + function + Pxp_types.Value s -> Cic.Name s + | Pxp_types.Implied_value -> Cic.Anonimous + | _ -> raise (IllFormedXml 1) + +let cic_sort_of_xml_attr = + function + Pxp_types.Value "Prop" -> Cic.Prop + | Pxp_types.Value "Set" -> Cic.Set + | Pxp_types.Value "Type" -> Cic.Type + | _ -> raise (IllFormedXml 2) + +let int_of_xml_attr = + function + Pxp_types.Value n -> int_of_string n + | _ -> raise (IllFormedXml 3) + +let uri_of_xml_attr = + function + Pxp_types.Value s -> UriManager.uri_of_string s + | _ -> raise (IllFormedXml 4) + +let string_of_xml_attr = + function + Pxp_types.Value s -> s + | _ -> raise (IllFormedXml 5) + +let binder_of_xml_attr = + function + Pxp_types.Value s -> if !process_annotations then Some s else None + | _ -> raise (IllFormedXml 17) +;; + +let register_id id node = + if !process_annotations then + match !ids_to_targets with + None -> assert false + | Some ids_to_targets -> + Hashtbl.add ids_to_targets id (Cic.Term node) +;; + +(* the "interface" of the class linked to each node of the dom tree *) + +class virtual cic_term = + object (self) + + (* fields and methods ever required by markup *) + val mutable node = (None : cic_term Pxp_document.node option) + + method clone = {< >} + method node = + match node with + None -> + assert false + | Some n -> n + method set_node n = + node <- Some n + + (* a method that returns the internal representation of the tree (term) *) + (* rooted in this node *) + method virtual to_cic_term : Cic.annterm + end +;; + +(* the class of the objects linked to nodes that are not roots of cic terms *) +class eltype_not_of_cic = + object (self) + + inherit cic_term + + method to_cic_term = raise (IllFormedXml 6) + end +;; + +(* the class of the objects linked to nodes whose content is a cic term *) +(* (syntactic sugar xml entities) e.g. ... *) +class eltype_transparent = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + match n#sub_nodes with + [ t ] -> t#extension#to_cic_term + | _ -> raise (IllFormedXml 7) + end +;; + +(* A class for each cic node type *) + +class eltype_fix = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let nofun = int_of_xml_attr (n#attribute "noFun") + and id = string_of_xml_attr (n#attribute "id") + and functions = + let sons = n#sub_nodes in + List.map + (function + f when f#node_type = Pxp_document.T_element "FixFunction" -> + let name = string_of_xml_attr (f#attribute "name") + and recindex = int_of_xml_attr (f#attribute "recIndex") + and (ty, body) = + match f#sub_nodes with + [t ; b] when + t#node_type = Pxp_document.T_element "type" && + b#node_type = Pxp_document.T_element "body" -> + (t#extension#to_cic_term, b#extension#to_cic_term) + | _ -> raise (IllFormedXml 14) + in + (name, recindex, ty, body) + | _ -> raise (IllFormedXml 13) + ) sons + in + let res = Cic.AFix (id, ref None, nofun, functions) in + register_id id res ; + res + end +;; + +class eltype_cofix = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let nofun = int_of_xml_attr (n#attribute "noFun") + and id = string_of_xml_attr (n#attribute "id") + and functions = + let sons = n#sub_nodes in + List.map + (function + f when f#node_type = Pxp_document.T_element "CofixFunction" -> + let name = string_of_xml_attr (f#attribute "name") + and (ty, body) = + match f#sub_nodes with + [t ; b] when + t#node_type = Pxp_document.T_element "type" && + b#node_type = Pxp_document.T_element "body" -> + (t#extension#to_cic_term, b#extension#to_cic_term) + | _ -> raise (IllFormedXml 16) + in + (name, ty, body) + | _ -> raise (IllFormedXml 15) + ) sons + in + let res = Cic.ACoFix (id, ref None, nofun, functions) in + register_id id res ; + res + end +;; + +class eltype_implicit = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let id = string_of_xml_attr (n#attribute "id") in + let res = Cic.AImplicit (id, ref None) in + register_id id res ; + res + end +;; + +class eltype_rel = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let value = int_of_xml_attr (n#attribute "value") + and binder = binder_of_xml_attr (n#attribute "binder") + and id = string_of_xml_attr (n#attribute "id") in + let res = Cic.ARel (id,ref None,value,binder) in + register_id id res ; + res + end +;; + +class eltype_meta = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let value = int_of_xml_attr (n#attribute "no") + and id = string_of_xml_attr (n#attribute "id") in + let res = Cic.AMeta (id,ref None,value) in + register_id id res ; + res + end +;; + +class eltype_var = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let name = string_of_xml_attr (n#attribute "relUri") + and xid = string_of_xml_attr (n#attribute "id") in + match Str.split (Str.regexp ",") name with + [index; id] -> + let get_prefix n = + let rec aux = + function + (0,_) -> "/" + | (n,he::tl) when n > 0 -> "/" ^ he ^ aux (n - 1, tl) + | _ -> raise (IllFormedXml 19) + in + aux (List.length !current_sp - n,!current_sp) + in + let res = + Cic.AVar + (xid,ref None, + (UriManager.uri_of_string + ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var")) + ) + in + register_id id res ; + res + | _ -> raise (IllFormedXml 18) + end +;; + +class eltype_apply = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let children = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + if List.length children < 2 then raise (IllFormedXml 8) + else + let res = + Cic.AAppl + (id,ref None,List.map (fun x -> x#extension#to_cic_term) children) + in + register_id id res ; + res + end +;; + +class eltype_cast = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let sons = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + match sons with + [te ; ty] when + te#node_type = Pxp_document.T_element "term" && + ty#node_type = Pxp_document.T_element "type" -> + let term = te#extension#to_cic_term + and typ = ty#extension#to_cic_term in + let res = Cic.ACast (id,ref None,term,typ) in + register_id id res ; + res + | _ -> raise (IllFormedXml 9) + end +;; + +class eltype_sort = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let sort = cic_sort_of_xml_attr (n#attribute "value") + and id = string_of_xml_attr (n#attribute "id") in + let res = Cic.ASort (id,ref None,sort) in + register_id id res ; + res + end +;; + +class eltype_abst = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let value = uri_of_xml_attr (n#attribute "uri") + and id = string_of_xml_attr (n#attribute "id") in + let res = Cic.AAbst (id,ref None,value) in + register_id id res ; + res + end +;; + +class eltype_const = + object (self) + + inherit cic_term + + method to_cic_term = + let module U = UriManager in + let n = self#node in + let value = uri_of_xml_attr (n#attribute "uri") + and id = string_of_xml_attr (n#attribute "id") in + let res = + Cic.AConst (id,ref None,value, U.relative_depth !current_uri value 0) + in + register_id id res ; + res + end +;; + +class eltype_mutind = + object (self) + + inherit cic_term + + method to_cic_term = + let module U = UriManager in + let n = self#node in + let name = uri_of_xml_attr (n#attribute "uri") + and noType = int_of_xml_attr (n#attribute "noType") + and id = string_of_xml_attr (n#attribute "id") in + let res = + Cic.AMutInd + (id,ref None,name, U.relative_depth !current_uri name 0, noType) + in + register_id id res ; + res + end +;; + +class eltype_mutconstruct = + object (self) + + inherit cic_term + + method to_cic_term = + let module U = UriManager in + let n = self#node in + let name = uri_of_xml_attr (n#attribute "uri") + and noType = int_of_xml_attr (n#attribute "noType") + and noConstr = int_of_xml_attr (n#attribute "noConstr") + and id = string_of_xml_attr (n#attribute "id") in + let res = + Cic.AMutConstruct + (id, ref None, name, U.relative_depth !current_uri name 0, + noType, noConstr) + in + register_id id res ; + res + end +;; + +class eltype_prod = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let sons = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + match sons with + [s ; t] when + s#node_type = Pxp_document.T_element "source" && + t#node_type = Pxp_document.T_element "target" -> + let name = cic_attr_of_xml_attr (t#attribute "binder") + and source = s#extension#to_cic_term + and target = t#extension#to_cic_term in + let res = Cic.AProd (id,ref None,name,source,target) in + register_id id res ; + res + | _ -> raise (IllFormedXml 10) + end +;; + +class eltype_mutcase = + object (self) + + inherit cic_term + + method to_cic_term = + let module U = UriManager in + let n = self#node in + let sons = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + match sons with + ty::te::patterns when + ty#node_type = Pxp_document.T_element "patternsType" && + te#node_type = Pxp_document.T_element "inductiveTerm" -> + let ci = uri_of_xml_attr (n#attribute "uriType") + and typeno = int_of_xml_attr (n#attribute "noType") + and inductiveType = ty#extension#to_cic_term + and inductiveTerm = te#extension#to_cic_term + and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns + in + let res = + Cic.AMutCase (id,ref None,ci,U.relative_depth !current_uri ci 0, + typeno,inductiveType,inductiveTerm,lpattern) + in + register_id id res ; + res + | _ -> raise (IllFormedXml 11) + end +;; + +class eltype_lambda = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let sons = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + match sons with + [s ; t] when + s#node_type = Pxp_document.T_element "source" && + t#node_type = Pxp_document.T_element "target" -> + let name = cic_attr_of_xml_attr (t#attribute "binder") + and source = s#extension#to_cic_term + and target = t#extension#to_cic_term in + let res = Cic.ALambda (id,ref None,name,source,target) in + register_id id res ; + res + | _ -> raise (IllFormedXml 12) + end +;; + +class eltype_letin = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let sons = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + match sons with + [s ; t] when + s#node_type = Pxp_document.T_element "term" && + t#node_type = Pxp_document.T_element "letintarget" -> + let name = cic_attr_of_xml_attr (t#attribute "binder") + and source = s#extension#to_cic_term + and target = t#extension#to_cic_term in + let res = Cic.ALetIn (id,ref None,name,source,target) in + register_id id res ; + res + | _ -> raise (IllFormedXml 12) + end +;; + +(* The definition of domspec, an hashtable that maps each node type to the *) +(* object that must be linked to it. Used by markup. *) + +let domspec = + let module D = Pxp_document in + D.make_spec_from_alist + ~data_exemplar: (new D.data_impl (new eltype_not_of_cic)) + ~default_element_exemplar: (new D.element_impl (new eltype_not_of_cic)) + ~element_alist: + [ "REL", (new D.element_impl (new eltype_rel)) ; + "VAR", (new D.element_impl (new eltype_var)) ; + "META", (new D.element_impl (new eltype_meta)) ; + "SORT", (new D.element_impl (new eltype_sort)) ; + "IMPLICIT", (new D.element_impl (new eltype_implicit)) ; + "CAST", (new D.element_impl (new eltype_cast)) ; + "PROD", (new D.element_impl (new eltype_prod)) ; + "LAMBDA", (new D.element_impl (new eltype_lambda)) ; + "LETIN", (new D.element_impl (new eltype_letin)) ; + "APPLY", (new D.element_impl (new eltype_apply)) ; + "CONST", (new D.element_impl (new eltype_const)) ; + "ABST", (new D.element_impl (new eltype_abst)) ; + "MUTIND", (new D.element_impl (new eltype_mutind)) ; + "MUTCONSTRUCT", (new D.element_impl (new eltype_mutconstruct)) ; + "MUTCASE", (new D.element_impl (new eltype_mutcase)) ; + "FIX", (new D.element_impl (new eltype_fix)) ; + "COFIX", (new D.element_impl (new eltype_cofix)) ; + "arity", (new D.element_impl (new eltype_transparent)) ; + "term", (new D.element_impl (new eltype_transparent)) ; + "type", (new D.element_impl (new eltype_transparent)) ; + "body", (new D.element_impl (new eltype_transparent)) ; + "source", (new D.element_impl (new eltype_transparent)) ; + "target", (new D.element_impl (new eltype_transparent)) ; + "letintarget", (new D.element_impl (new eltype_transparent)) ; + "patternsType", (new D.element_impl (new eltype_transparent)) ; + "inductiveTerm", (new D.element_impl (new eltype_transparent)) ; + "pattern", (new D.element_impl (new eltype_transparent)) + ] + () +;; diff --git a/helm/metadata/create2/touch/cicParser3.mli b/helm/metadata/create2/touch/cicParser3.mli new file mode 100644 index 000000000..ada1b2e81 --- /dev/null +++ b/helm/metadata/create2/touch/cicParser3.mli @@ -0,0 +1,67 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This module is the terms level of a parser for cic objects from xml *) +(* files to the internal representation. It is used by the module cicParser2 *) +(* (objects level). It defines an extension of the standard dom using the *) +(* object-oriented extension machinery of markup: an object with a method *) +(* to_cic_term that returns the internal representation of the subtree is *) +(* added to each node of the dom tree *) +(* *) +(******************************************************************************) + +exception IllFormedXml of int + +val ids_to_targets : (Cic.id, Cic.anntarget) Hashtbl.t option ref +val current_sp : string list ref +val current_uri : UriManager.uri ref +val process_annotations : bool ref + +(* the "interface" of the class linked to each node of the dom tree *) +class virtual cic_term : + object ('a) + + (* fields and methods ever required by markup *) + val mutable node : cic_term Pxp_document.node option + method clone : 'a + method node : cic_term Pxp_document.node + method set_node : cic_term Pxp_document.node -> unit + + (* a method that returns the internal representation of the tree (term) *) + (* rooted in this node *) + method virtual to_cic_term : Cic.annterm + + end + +(* The definition of domspec, an hashtable that maps each node type to the *) +(* object that must be linked to it. Used by markup. *) +val domspec : cic_term Pxp_document.spec diff --git a/helm/metadata/create2/touch/clientHTTP.ml b/helm/metadata/create2/touch/clientHTTP.ml new file mode 100644 index 000000000..4d5488c00 --- /dev/null +++ b/helm/metadata/create2/touch/clientHTTP.ml @@ -0,0 +1,60 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +exception HttpClientError of exn * string;; + +let send cmd = + try + ignore (Http_client.Convenience.http_get cmd) + with + e -> raise (HttpClientError (e,cmd)) +;; + +let get uri = + try + Http_client.Convenience.http_get uri + with + e -> raise (HttpClientError (e,uri)) +;; + +let get_and_save uri dest_filename = + let reply = get uri + and out_channel = open_out dest_filename in + output_string out_channel reply ; + close_out out_channel +;; + +let get_and_save_to_tmp uri = + let flat_string s s' c = + let cs = String.copy s in + for i = 0 to (String.length s) - 1 do + if String.contains s' s.[i] then cs.[i] <- c + done ; + cs + in + let tmp_file = Configuration.tmp_dir ^ "/" ^ (flat_string uri ".-=:;!?/&" '_') in + get_and_save uri tmp_file ; + tmp_file +;; diff --git a/helm/metadata/create2/touch/clientHTTP.mli b/helm/metadata/create2/touch/clientHTTP.mli new file mode 100644 index 000000000..59587edc2 --- /dev/null +++ b/helm/metadata/create2/touch/clientHTTP.mli @@ -0,0 +1,30 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +exception HttpClientError of exn * string;; +val send : string -> unit +val get : string -> string +val get_and_save : string -> string -> unit +val get_and_save_to_tmp : string -> string diff --git a/helm/metadata/create2/touch/configuration.ml.in b/helm/metadata/create2/touch/configuration.ml.in new file mode 100644 index 000000000..d20a3c0c0 --- /dev/null +++ b/helm/metadata/create2/touch/configuration.ml.in @@ -0,0 +1,117 @@ +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 28/12/2000 *) +(* *) +(* This is the parser that reads the configuration file of helm *) +(* *) +(******************************************************************************) + +exception MalformedDir of string + +(* this should be the only hard coded constant *) +let filename = + let prefix = + try + Sys.getenv "HELM_CONFIGURATION_DIR" + with + Not_found -> "@HELM_CONFIGURATION_DIR@" + in + if prefix.[(String.length prefix) - 1] = '/' then + raise (MalformedDir prefix) ; + prefix ^ "/configuration.xml";; + +exception Warnings;; + +class warner = + object + method warn w = + print_endline ("WARNING: " ^ w) ; + (raise Warnings : unit) + end +;; + +let xml_document () = + let module Y = Pxp_yacc in + try + let config = {Y.default_config with Y.warner = new warner} in + Y.parse_document_entity config (Y.from_file filename) Y.default_spec + with + e -> + print_endline (Pxp_types.string_of_exn e) ; + raise e +;; + +exception Impossible;; + +let vars = Hashtbl.create 14;; + +(* resolve tags and returns the string values of the variable tags *) +let rec resolve = + let module D = Pxp_document in + function + [] -> "" + | he::tl when he#node_type = D.T_element "value-of" -> + (match he#attribute "var" with + Pxp_types.Value var -> Hashtbl.find vars var + | _ -> raise Impossible + ) ^ resolve tl + | he::tl when he#node_type = D.T_data -> + he#data ^ resolve tl + | _ -> raise Impossible +;; + +(* we trust the xml file to be valid because of the validating xml parser *) +let _ = + List.iter + (function + n -> + match n#node_type with + Pxp_document.T_element var -> + Hashtbl.add vars var (resolve (n#sub_nodes)) + | _ -> raise Impossible + ) + ((xml_document ())#root#sub_nodes) +;; + +(* try to read a configuration variable, given its name into the + * configuration.xml file and its name into the shell environment. + * The shell variable, if present, has precedence over configuration.xml + *) +let read_configuration_var_env xml_name env_name = + try + try + Sys.getenv env_name + with + Not_found -> Hashtbl.find vars xml_name + with + Not_found -> + Printf.printf "Sorry, cannot find variable `%s', please check your configuration\n" xml_name ; + flush stdout ; + raise Not_found + +let read_configuration_var xml_name = + try + Hashtbl.find vars xml_name + with + Not_found -> + Printf.printf "Sorry, cannot find variable `%s', please check your configuration\n" xml_name ; + flush stdout ; + raise Not_found + +let helm_dir = read_configuration_var "helm_dir";; +let dtd_dir = read_configuration_var "dtd_dir";; +let style_dir = read_configuration_var_env "style_dir" "HELM_STYLE_DIR";; +let servers_file = read_configuration_var "servers_file";; +let uris_dbm = read_configuration_var "uris_dbm";; +let dest = read_configuration_var "dest";; +let indexname = read_configuration_var "indexname";; +let tmp_dir = read_configuration_var "tmp_dir" +let helm_dir = read_configuration_var "helm_dir";; +let getter_url = read_configuration_var_env "getter_url" "HELM_GETTER_URL";; +let processor_url = read_configuration_var_env "processor_url" "HELM_PROCESSOR_URL";; + +let _ = Hashtbl.clear vars;; + diff --git a/helm/metadata/create2/touch/csc_pxp_reader.ml b/helm/metadata/create2/touch/csc_pxp_reader.ml new file mode 100644 index 000000000..587c60c8a --- /dev/null +++ b/helm/metadata/create2/touch/csc_pxp_reader.ml @@ -0,0 +1,1008 @@ +(* $Id$ + * ---------------------------------------------------------------------- + * PXP: The polymorphic XML parser for Objective Caml. + * Copyright by Gerd Stolpmann. See LICENSE for details. + *) + +open Pxp_types;; +exception Not_competent;; +exception Not_resolvable of exn;; + +class type resolver = + object + method init_rep_encoding : rep_encoding -> unit + method init_warner : collect_warnings -> unit + method rep_encoding : rep_encoding + method open_in : ext_id -> Lexing.lexbuf + method close_in : unit + method close_all : unit + method change_encoding : string -> unit + method clone : resolver + end +;; + + +class virtual resolve_general + = + object (self) + val mutable internal_encoding = `Enc_utf8 + + val mutable encoding = `Enc_utf8 + val mutable encoding_requested = false + + val mutable warner = new drop_warnings + + val mutable enc_initialized = false + val mutable wrn_initialized = false + + val mutable clones = [] + + method init_rep_encoding e = + internal_encoding <- e; + enc_initialized <- true; + + method init_warner w = + warner <- w; + wrn_initialized <- true; + + method rep_encoding = (internal_encoding :> rep_encoding) + +(* + method clone = + ( {< encoding = `Enc_utf8; + encoding_requested = false; + >} + : # resolver :> resolver ) +*) + + method private warn (k:int) = + (* Called if a character not representable has been found. + * k is the character code. + *) + if k < 0xd800 or (k >= 0xe000 & k <= 0xfffd) or + (k >= 0x10000 & k <= 0x10ffff) then begin + warner # warn ("Code point cannot be represented: " ^ string_of_int k); + end + else + raise (WF_error("Code point " ^ string_of_int k ^ + " outside the accepted range of code points")) + + + method private autodetect s = + (* s must be at least 4 bytes long. The slot 'encoding' is + * set to: + * "UTF-16-BE": UTF-16/UCS-2 encoding big endian + * "UTF-16-LE": UTF-16/UCS-2 encoding little endian + * "UTF-8": UTF-8 encoding + *) + if String.length s < 4 then + encoding <- `Enc_utf8 + else if String.sub s 0 2 = "\254\255" then + encoding <- `Enc_utf16 + (* Note: Netconversion.recode will detect the big endianess, too *) + else if String.sub s 0 2 = "\255\254" then + encoding <- `Enc_utf16 + (* Note: Netconversion.recode will detect the little endianess, too *) + else + encoding <- `Enc_utf8 + + + method private virtual next_string : string -> int -> int -> int + method private virtual init_in : ext_id -> unit + method virtual close_in : unit + + method close_all = + List.iter (fun r -> r # close_in) clones + + method open_in xid = + assert(enc_initialized && wrn_initialized); + + encoding <- `Enc_utf8; + encoding_requested <- false; + self # init_in xid; (* may raise Not_competent *) + (* init_in: may already set 'encoding' *) + + let buffer_max = 512 in + let buffer = String.make buffer_max ' ' in + let buffer_len = ref 0 in + let buffer_end = ref false in + let fillup () = + if not !buffer_end & !buffer_len < buffer_max then begin + let l = + self # next_string buffer !buffer_len (buffer_max - !buffer_len) in + if l = 0 then + buffer_end := true + else begin + buffer_len := !buffer_len + l + end + end + in + let consume n = + let l = !buffer_len - n in + String.blit buffer n buffer 0 l; + buffer_len := l + in + + fillup(); + if not encoding_requested then self # autodetect buffer; + + Lexing.from_function + (fun s n -> + (* TODO: if encoding = internal_encoding, it is possible to + * avoid copying buffer to s because s can be directly used + * as buffer. + *) + + fillup(); + if !buffer_len = 0 then + 0 + else begin + let m_in = !buffer_len in + let m_max = if encoding_requested then n else 1 in + let n_in, n_out, encoding' = + if encoding = (internal_encoding : rep_encoding :> encoding) && + encoding_requested + then begin + (* Special case encoding = internal_encoding *) + String.blit buffer 0 s 0 m_in; + m_in, m_in, encoding + end + else + Netconversion.recode + ~in_enc:encoding + ~in_buf:buffer + ~in_pos:0 + ~in_len:m_in + ~out_enc:(internal_encoding : rep_encoding :> encoding) + ~out_buf:s + ~out_pos:0 + ~out_len:n + ~max_chars:m_max + ~subst:(fun k -> self # warn k; "") + in + if n_in = 0 then + (* An incomplete character at the end of the stream: *) + raise Netconversion.Malformed_code; + (* failwith "Badly encoded character"; *) + encoding <- encoding'; + consume n_in; + assert(n_out <> 0); + n_out + end) + + method change_encoding enc = + if not encoding_requested then begin + if enc <> "" then begin + match Netconversion.encoding_of_string enc with + `Enc_utf16 -> + (match encoding with + (`Enc_utf16_le | `Enc_utf16_be) -> () + | `Enc_utf16 -> assert false + | _ -> + raise(WF_error "Encoding of data stream and encoding declaration mismatch") + ) + | e -> + encoding <- e + end; + (* else: the autodetected encoding counts *) + encoding_requested <- true; + end; + end +;; + + +class resolve_read_any_channel ?(close=close_in) ~channel_of_id () = + object (self) + inherit resolve_general as super + + val f_open = channel_of_id + val mutable current_channel = None + val close = close + + method private init_in (id:ext_id) = + if current_channel <> None then + failwith "Pxp_reader.resolve_read_any_channel # init_in"; + let ch, enc_opt = f_open id in (* may raise Not_competent *) + begin match enc_opt with + None -> () + | Some enc -> encoding <- enc; encoding_requested <- true + end; + current_channel <- Some ch; + + method private next_string s ofs len = + match current_channel with + None -> failwith "Pxp_reader.resolve_read_any_channel # next_string" + | Some ch -> + input ch s ofs len + + method close_in = + match current_channel with + None -> () + | Some ch -> + close ch; + current_channel <- None + + method clone = + let c = new resolve_read_any_channel + ?close:(Some close) f_open () in + c # init_rep_encoding internal_encoding; + c # init_warner warner; + clones <- c :: clones; + (c :> resolver) + + end +;; + + +class resolve_read_this_channel1 is_stale ?id ?fixenc ?close ch = + + let getchannel = ref (fun xid -> assert false) in + + object (self) + inherit resolve_read_any_channel + ?close + (fun xid -> !getchannel xid) + () + as super + + val mutable is_stale = is_stale + (* The channel can only be read once. To avoid that the channel + * is opened several times, the flag 'is_stale' is set after the + * first time. + *) + + val fixid = id + val fixenc = fixenc + val fixch = ch + + initializer + getchannel := self # getchannel + + method private getchannel xid = + begin match fixid with + None -> () + | Some bound_xid -> + if xid <> bound_xid then raise Not_competent + end; + ch, fixenc + + method private init_in (id:ext_id) = + if is_stale then + raise Not_competent + else begin + super # init_in id; + is_stale <- true + end + + method close_in = + current_channel <- None + + method clone = + let c = new resolve_read_this_channel1 + is_stale + ?id:fixid ?fixenc:fixenc ?close:(Some close) fixch + in + c # init_rep_encoding internal_encoding; + c # init_warner warner; + clones <- c :: clones; + (c :> resolver) + + end +;; + + +class resolve_read_this_channel = + resolve_read_this_channel1 false +;; + + +class resolve_read_any_string ~string_of_id () = + object (self) + inherit resolve_general as super + + val f_open = string_of_id + val mutable current_string = None + val mutable current_pos = 0 + + method private init_in (id:ext_id) = + if current_string <> None then + failwith "Pxp_reader.resolve_read_any_string # init_in"; + let s, enc_opt = f_open id in (* may raise Not_competent *) + begin match enc_opt with + None -> () + | Some enc -> encoding <- enc; encoding_requested <- true + end; + current_string <- Some s; + current_pos <- 0; + + method private next_string s ofs len = + match current_string with + None -> failwith "Pxp_reader.resolve_read_any_string # next_string" + | Some str -> + let l = min len (String.length str - current_pos) in + String.blit str current_pos s ofs l; + current_pos <- current_pos + l; + l + + method close_in = + match current_string with + None -> () + | Some _ -> + current_string <- None + + method clone = + let c = new resolve_read_any_string f_open () in + c # init_rep_encoding internal_encoding; + c # init_warner warner; + clones <- c :: clones; + (c :> resolver) + end +;; + + +class resolve_read_this_string1 is_stale ?id ?fixenc str = + + let getstring = ref (fun xid -> assert false) in + + object (self) + inherit resolve_read_any_string (fun xid -> !getstring xid) () as super + + val is_stale = is_stale + (* For some reasons, it is not allowed to open a clone of the resolver + * a second time when the original resolver is already open. + *) + + val fixid = id + val fixenc = fixenc + val fixstr = str + + initializer + getstring := self # getstring + + method private getstring xid = + begin match fixid with + None -> () + | Some bound_xid -> + if xid <> bound_xid then raise Not_competent + end; + fixstr, fixenc + + + method private init_in (id:ext_id) = + if is_stale then + raise Not_competent + else + super # init_in id + + method clone = + let c = new resolve_read_this_string1 + (is_stale or current_string <> None) + ?id:fixid ?fixenc:fixenc fixstr + in + c # init_rep_encoding internal_encoding; + c # init_warner warner; + clones <- c :: clones; + (c :> resolver) + end +;; + + +class resolve_read_this_string = + resolve_read_this_string1 false +;; + + +class resolve_read_url_channel + ?(base_url = Neturl.null_url) + ?close + ~url_of_id + ~channel_of_url + () + + : resolver + = + + let getchannel = ref (fun xid -> assert false) in + + object (self) + inherit resolve_read_any_channel + ?close + (fun xid -> !getchannel xid) + () + as super + + val base_url = base_url + val mutable own_url = Neturl.null_url + + val url_of_id = url_of_id + val channel_of_url = channel_of_url + + + initializer + getchannel := self # getchannel + + method private getchannel xid = + let rel_url = url_of_id xid in (* may raise Not_competent *) + + try + (* Now compute the absolute URL: *) + let abs_url = + if Neturl.url_provides ~scheme:true rel_url then + rel_url + else + Neturl.apply_relative_url base_url rel_url in + (* may raise Malformed_URL *) + + (* Simple check whether 'abs_url' is really absolute: *) + if not(Neturl.url_provides ~scheme:true abs_url) + then raise Not_competent; + + own_url <- abs_url; + (* FIXME: Copy 'abs_url' ? *) + + (* Get and return the channel: *) + channel_of_url xid abs_url (* may raise Not_competent *) + with + Neturl.Malformed_URL -> raise (Not_resolvable Neturl.Malformed_URL) + | Not_competent -> raise (Not_resolvable Not_found) + + method clone = + let c = + new resolve_read_url_channel + ?base_url:(Some own_url) + ?close:(Some close) + ~url_of_id:url_of_id + ~channel_of_url:channel_of_url + () + in + c # init_rep_encoding internal_encoding; + c # init_warner warner; + clones <- c :: clones; + (c :> resolve_read_url_channel) + end +;; + + +type spec = [ `Not_recognized | `Allowed | `Required ] + +class resolve_as_file + ?(file_prefix = (`Allowed :> spec)) + ?(host_prefix = (`Allowed :> spec)) + ?(system_encoding = `Enc_utf8) + ?(map_private_id = (fun _ -> raise Not_competent)) + ?(open_private_id = (fun _ -> raise Not_competent)) + () + = + + let url_syntax = + let enable_if = + function + `Not_recognized -> Neturl.Url_part_not_recognized + | `Allowed -> Neturl.Url_part_allowed + | `Required -> Neturl.Url_part_required + in + { Neturl.null_url_syntax with + Neturl.url_enable_scheme = enable_if file_prefix; + Neturl.url_enable_host = enable_if host_prefix; + Neturl.url_enable_path = Neturl.Url_part_required; + Neturl.url_accepts_8bits = true; + } + in + + let base_url_syntax = + { Neturl.null_url_syntax with + Neturl.url_enable_scheme = Neturl.Url_part_required; + Neturl.url_enable_host = Neturl.Url_part_allowed; + Neturl.url_enable_path = Neturl.Url_part_required; + Neturl.url_accepts_8bits = true; + } + in + + let default_base_url = + Neturl.make_url + ~scheme: "file" + ~host: "" + ~path: (Neturl.split_path (Sys.getcwd() ^ "/")) + base_url_syntax + in + + let file_url_of_id xid = + let file_url_of_sysname sysname = + (* By convention, we can assume that sysname is a URL conforming + * to RFC 1738 with the exception that it may contain non-ASCII + * UTF-8 characters. + *) + try + Neturl.url_of_string url_syntax sysname + (* may raise Malformed_URL *) + with + Neturl.Malformed_URL -> raise Not_competent + in + let url = + match xid with + Anonymous -> raise Not_competent + | Public (_,sysname) -> if sysname <> "" then file_url_of_sysname sysname + else raise Not_competent + | System sysname -> file_url_of_sysname sysname + | Private pid -> map_private_id pid + in + let scheme = + try Neturl.url_scheme url with Not_found -> "file" in + let host = + try Neturl.url_host url with Not_found -> "" in + + if scheme <> "file" then raise Not_competent; + if host <> "" && host <> "localhost" then raise Not_competent; + + url + in + + let channel_of_file_url xid url = + match xid with + Private pid -> open_private_id pid + | _ -> + ( try + let path_utf8 = + try Neturl.join_path (Neturl.url_path ~encoded:false url) + with Not_found -> raise Not_competent + in + + let path = + Netconversion.recode_string + ~in_enc: `Enc_utf8 + ~out_enc: system_encoding + path_utf8 in + (* May raise Malformed_code *) + + open_in_bin path, None + (* May raise Sys_error *) + + with + | Netconversion.Malformed_code -> assert false + (* should not happen *) + | Sys_error _ as e -> + raise (Not_resolvable e) + ) + in + + resolve_read_url_channel + ~base_url: default_base_url + ~url_of_id: file_url_of_id + ~channel_of_url: channel_of_file_url + () +;; + + +let make_file_url ?(system_encoding = `Enc_utf8) ?(enc = `Enc_utf8) filename = + let utf8_filename = + Netconversion.recode_string + ~in_enc: enc + ~out_enc: `Enc_utf8 + filename + in + + let utf8_abs_filename = + if utf8_filename <> "" && utf8_filename.[0] = '/' then + utf8_filename + else + let cwd = Sys.getcwd() in + let cwd_utf8 = + Netconversion.recode_string + ~in_enc: system_encoding + ~out_enc: `Enc_utf8 in + cwd ^ "/" ^ utf8_filename + in + + let syntax = { Neturl.ip_url_syntax with Neturl.url_accepts_8bits = true } in + let url = Neturl.make_url + ~scheme:"file" + ~host:"localhost" + ~path:(Neturl.split_path utf8_abs_filename) + syntax + in + url +;; + + +class lookup_public_id (catalog : (string * resolver) list) = + let norm_catalog = + List.map (fun (id,s) -> Pxp_aux.normalize_public_id id, s) catalog in +( object (self) + val cat = norm_catalog + val mutable internal_encoding = `Enc_utf8 + val mutable warner = new drop_warnings + val mutable active_resolver = None + + method init_rep_encoding enc = + internal_encoding <- enc + + method init_warner w = + warner <- w; + + method rep_encoding = internal_encoding + (* CAUTION: This may not be the truth! *) + + method open_in xid = + + if active_resolver <> None then failwith "Pxp_reader.lookup_* # open_in"; + + let r = + match xid with + Public(pubid,_) -> + begin + (* Search pubid in catalog: *) + try + let norm_pubid = Pxp_aux.normalize_public_id pubid in + List.assoc norm_pubid cat + with + Not_found -> + raise Not_competent + end + | _ -> + raise Not_competent + in + + let r' = r # clone in + r' # init_rep_encoding internal_encoding; + r' # init_warner warner; + let lb = r' # open_in xid in (* may raise Not_competent *) + active_resolver <- Some r'; + lb + + method close_in = + match active_resolver with + None -> () + | Some r -> r # close_in; + active_resolver <- None + + method close_all = + self # close_in + + method change_encoding (enc:string) = + match active_resolver with + None -> failwith "Pxp_reader.lookup_* # change_encoding" + | Some r -> r # change_encoding enc + + method clone = + let c = new lookup_public_id cat in + c # init_rep_encoding internal_encoding; + c # init_warner warner; + c + end : resolver ) +;; + + +let lookup_public_id_as_file ?(fixenc:encoding option) catalog = + let ch_of_id filename id = + let ch = open_in_bin filename in (* may raise Sys_error *) + ch, fixenc + in + let catalog' = + List.map + (fun (id,s) -> + (id, new resolve_read_any_channel (ch_of_id s) ()) + ) + catalog + in + new lookup_public_id catalog' +;; + + +let lookup_public_id_as_string ?(fixenc:encoding option) catalog = + let catalog' = + List.map + (fun (id,s) -> + (id, new resolve_read_any_string (fun _ -> s, fixenc) ()) + ) + catalog + in + new lookup_public_id catalog' +;; + + +class lookup_system_id (catalog : (string * resolver) list) = +( object (self) + val cat = catalog + val mutable internal_encoding = `Enc_utf8 + val mutable warner = new drop_warnings + val mutable active_resolver = None + + method init_rep_encoding enc = + internal_encoding <- enc + + method init_warner w = + warner <- w; + + method rep_encoding = internal_encoding + (* CAUTION: This may not be the truth! *) + + + method open_in xid = + + if active_resolver <> None then failwith "Pxp_reader.lookup_system_id # open_in"; + + let lookup sysid = + try + List.assoc sysid cat + with + Not_found -> + raise Not_competent + in + + let r = + match xid with + System sysid -> lookup sysid + | Public(_,sysid) -> lookup sysid + | _ -> raise Not_competent + in + + let r' = r # clone in + r' # init_rep_encoding internal_encoding; + r' # init_warner warner; + let lb = r' # open_in xid in (* may raise Not_competent *) + active_resolver <- Some r'; + lb + + + method close_in = + match active_resolver with + None -> () + | Some r -> r # close_in; + active_resolver <- None + + method close_all = + self # close_in + + method change_encoding (enc:string) = + match active_resolver with + None -> failwith "Pxp_reader.lookup_system # change_encoding" + | Some r -> r # change_encoding enc + + method clone = + let c = new lookup_system_id cat in + c # init_rep_encoding internal_encoding; + c # init_warner warner; + c + end : resolver) +;; + + +let lookup_system_id_as_file ?(fixenc:encoding option) catalog = + let ch_of_id filename id = + let ch = open_in_bin filename in (* may raise Sys_error *) + ch, fixenc + in + let catalog' = + List.map + (fun (id,s) -> + (id, new resolve_read_any_channel (ch_of_id s) ()) + ) + catalog + in + new lookup_system_id catalog' +;; + + +let lookup_system_id_as_string ?(fixenc:encoding option) catalog = + let catalog' = + List.map + (fun (id,s) -> + (id, new resolve_read_any_string (fun _ -> s, fixenc) ()) + ) + catalog + in + new lookup_system_id catalog' +;; + + +type combination_mode = + Public_before_system + | System_before_public +;; + + +class combine ?prefer ?(mode = Public_before_system) rl = + object (self) + val prefered_resolver = prefer + val mode = mode + val resolvers = (rl : resolver list) + val mutable internal_encoding = `Enc_utf8 + val mutable warner = new drop_warnings + val mutable active_resolver = None + val mutable clones = [] + + method init_rep_encoding enc = + List.iter + (fun r -> r # init_rep_encoding enc) + rl; + internal_encoding <- enc + + method init_warner w = + List.iter + (fun r -> r # init_warner w) + rl; + warner <- w; + + method rep_encoding = internal_encoding + (* CAUTION: This may not be the truth! *) + + method open_in xid = + let rec find_competent_resolver_for xid' rl = + match rl with + r :: rl' -> + begin try + r, (r # open_in xid') + with + Not_competent -> find_competent_resolver_for xid' rl' + end; + | [] -> + raise Not_competent + in + + let find_competent_resolver rl = + match xid with + Public(pubid,sysid) -> + ( match mode with + Public_before_system -> + ( try + find_competent_resolver_for(Public(pubid,"")) rl + with + Not_competent -> + find_competent_resolver_for(System sysid) rl + ) + | System_before_public -> + ( try + find_competent_resolver_for(System sysid) rl + with + Not_competent -> + find_competent_resolver_for(Public(pubid,"")) rl + ) + ) + | other -> + find_competent_resolver_for other rl + in + + if active_resolver <> None then failwith "Pxp_reader.combine # open_in"; + let r, lb = + match prefered_resolver with + None -> find_competent_resolver resolvers + | Some r -> find_competent_resolver (r :: resolvers) + in + active_resolver <- Some r; + lb + + method close_in = + match active_resolver with + None -> () + | Some r -> r # close_in; + active_resolver <- None + + method close_all = + List.iter (fun r -> r # close_in) clones + + method change_encoding (enc:string) = + match active_resolver with + None -> failwith "Pxp_reader.combine # change_encoding" + | Some r -> r # change_encoding enc + + method clone = + let c = + match active_resolver with + None -> + new combine ?prefer:None ?mode:(Some mode) + (List.map (fun q -> q # clone) resolvers) + | Some r -> + let r' = r # clone in + new combine + ?prefer:(Some r') + ?mode:(Some mode) + (List.map + (fun q -> if q == r then r' else q # clone) + resolvers) + in + c # init_rep_encoding internal_encoding; + c # init_warner warner; + clones <- c :: clones; + c + end + + + +(* ====================================================================== + * History: + * + * $Log$ + * Revision 1.1 2001/10/24 15:33:16 sacerdot + * New procedure to create metadata committed and old procedure removed. + * The new procedure is based on ocaml code and builds metadata for both + * forward and backward pointers. The old one was based on a stylesheet. + * + * Revision 1.16 2001/07/01 09:46:40 gerd + * Fix: resolve_read_url_channel does not use the base_url if + * the current URL is already absolute + * + * Revision 1.15 2001/07/01 08:35:23 gerd + * Instead of the ~auto_close argument, there is now a + * ~close argument for several functions/classes. This allows some + * additional action when the resolver is closed. + * + * Revision 1.14 2001/06/14 23:28:02 gerd + * Fix: class combine works now with private IDs. + * + * Revision 1.13 2001/04/22 14:16:48 gerd + * resolve_as_file: you can map private IDs to arbitrary channels. + * resolve_read_url_channel: changed type of the channel_of_url + * argument (ext_id is also passed) + * More examples and documentation. + * + * Revision 1.12 2001/04/21 17:40:48 gerd + * Bugfix in 'combine' + * + * Revision 1.11 2001/04/03 20:22:44 gerd + * New resolvers for catalogs of PUBLIC and SYSTEM IDs. + * Improved "combine": PUBLIC and SYSTEM IDs are handled + * separately. + * Rewritten from_file: Is now a simple application of the + * Pxp_reader classes and functions. (The same has still to be done + * for from_channel!) + * + * Revision 1.10 2001/02/01 20:38:49 gerd + * New support for PUBLIC identifiers. + * + * Revision 1.9 2000/08/14 22:24:55 gerd + * Moved the module Pxp_encoding to the netstring package under + * the new name Netconversion. + * + * Revision 1.8 2000/07/16 18:31:09 gerd + * The exception Illegal_character has been dropped. + * + * Revision 1.7 2000/07/09 15:32:01 gerd + * Fix in resolve_this_channel, resolve_this_string + * + * Revision 1.6 2000/07/09 01:05:33 gerd + * New methode 'close_all' that closes the clones, too. + * + * Revision 1.5 2000/07/08 16:24:56 gerd + * Introduced the exception 'Not_resolvable' to indicate that + * 'combine' should not try the next resolver of the list. + * + * Revision 1.4 2000/07/06 23:04:46 gerd + * Quick fix for 'combine': The active resolver is "prefered", + * but the other resolvers are also used. + * + * Revision 1.3 2000/07/06 21:43:45 gerd + * Fix: Public(_,name) is now treated as System(name) if + * name is non-empty. + * + * Revision 1.2 2000/07/04 22:13:30 gerd + * Implemented the new API rev. 1.2 of pxp_reader.mli. + * + * Revision 1.1 2000/05/29 23:48:38 gerd + * Changed module names: + * Markup_aux into Pxp_aux + * Markup_codewriter into Pxp_codewriter + * Markup_document into Pxp_document + * Markup_dtd into Pxp_dtd + * Markup_entity into Pxp_entity + * Markup_lexer_types into Pxp_lexer_types + * Markup_reader into Pxp_reader + * Markup_types into Pxp_types + * Markup_yacc into Pxp_yacc + * See directory "compatibility" for (almost) compatible wrappers emulating + * Markup_document, Markup_dtd, Markup_reader, Markup_types, and Markup_yacc. + * + * ====================================================================== + * Old logs from markup_reader.ml: + * + * Revision 1.3 2000/05/29 21:14:57 gerd + * Changed the type 'encoding' into a polymorphic variant. + * + * Revision 1.2 2000/05/20 20:31:40 gerd + * Big change: Added support for various encodings of the + * internal representation. + * + * Revision 1.1 2000/03/13 23:41:44 gerd + * Initial revision; this code was formerly part of Markup_entity. + * + * + *) diff --git a/helm/metadata/create2/touch/deannotate.ml b/helm/metadata/create2/touch/deannotate.ml new file mode 100644 index 000000000..00d4854db --- /dev/null +++ b/helm/metadata/create2/touch/deannotate.ml @@ -0,0 +1,98 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +let expect_possible_parameters = ref false;; + +exception NotExpectingPossibleParameters;; + +let rec deannotate_term = + let module C = Cic in + function + C.ARel (_,_,n,_) -> C.Rel n + | C.AVar (_,_,uri) -> C.Var uri + | C.AMeta (_,_,n) -> C.Meta n + | C.ASort (_,_,s) -> C.Sort s + | C.AImplicit _ -> C.Implicit + | C.ACast (_,_,va,ty) -> C.Cast (deannotate_term va, deannotate_term ty) + | C.AProd (_,_,name,so,ta) -> + C.Prod (name, deannotate_term so, deannotate_term ta) + | C.ALambda (_,_,name,so,ta) -> + C.Lambda (name, deannotate_term so, deannotate_term ta) + | C.ALetIn (_,_,name,so,ta) -> + C.LetIn (name, deannotate_term so, deannotate_term ta) + | C.AAppl (_,_,l) -> C.Appl (List.map deannotate_term l) + | C.AConst (_,_,uri, cookingsno) -> C.Const (uri, cookingsno) + | C.AAbst (_,_,uri) -> C.Abst uri + | C.AMutInd (_,_,uri,cookingsno,i) -> C.MutInd (uri,cookingsno,i) + | C.AMutConstruct (_,_,uri,cookingsno,i,j) -> + C.MutConstruct (uri,cookingsno,i,j) + | C.AMutCase (_,_,uri,cookingsno,i,outtype,te,pl) -> + C.MutCase (uri,cookingsno,i,deannotate_term outtype, + deannotate_term te, List.map deannotate_term pl) + | C.AFix (_,_,funno,ifl) -> + C.Fix (funno, List.map deannotate_inductiveFun ifl) + | C.ACoFix (_,_,funno,ifl) -> + C.CoFix (funno, List.map deannotate_coinductiveFun ifl) + +and deannotate_inductiveFun (name,index,ty,bo) = + (name, index, deannotate_term ty, deannotate_term bo) + +and deannotate_coinductiveFun (name,ty,bo) = + (name, deannotate_term ty, deannotate_term bo) +;; + +let deannotate_inductiveType (name, isinductive, arity, cons) = + (name, isinductive, deannotate_term arity, + List.map (fun (id,ty,recs) -> (id,deannotate_term ty, recs)) cons) +;; + +let deannotate_obj = + let module C = Cic in + function + C.ADefinition (_, _, id, bo, ty, params) -> + (match params with + C.Possible params -> + if !expect_possible_parameters then + C.Definition (id, deannotate_term bo, deannotate_term ty, params) + else + raise NotExpectingPossibleParameters + | C.Actual params -> + C.Definition (id, deannotate_term bo, deannotate_term ty, params) + ) + | C.AAxiom (_, _, id, ty, params) -> + C.Axiom (id, deannotate_term ty, params) + | C.AVariable (_, _, name, bo, ty) -> + C.Variable (name, + (match bo with None -> None | Some bo -> Some (deannotate_term bo)), + deannotate_term ty) + | C.ACurrentProof (_, _, name, conjs, bo, ty) -> + C.CurrentProof ( + name, List.map (fun (id,con) -> (id,deannotate_term con)) conjs, + deannotate_term bo, deannotate_term ty + ) + | C.AInductiveDefinition (_, _, tys, params, parno) -> + C.InductiveDefinition ( List.map deannotate_inductiveType tys, + params, parno) +;; diff --git a/helm/metadata/create2/touch/getter.ml b/helm/metadata/create2/touch/getter.ml new file mode 100644 index 000000000..894bf3ea9 --- /dev/null +++ b/helm/metadata/create2/touch/getter.ml @@ -0,0 +1,63 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(******************************************************************************) + +let getter_url = ref Configuration.getter_url;; + +let update () = + (* deliver update request to http_getter *) + ClientHTTP.send (!getter_url ^ "update") +;; + +type format = + Normal + | GZipped +;; + +let getxml ?(format=Normal) ?(patchdtd=true) uri = + (* deliver getxml request to http_getter *) + ClientHTTP.get_and_save_to_tmp + (!getter_url ^ "getxml" ^ + "?uri=" ^ UriManager.string_of_uri uri ^ + "&format=" ^ (match format with Normal -> "normal" | GZipped -> "gzipped") ^ + "&patch_dtd=" ^ (match patchdtd with true -> "yes" | false -> "no") + ) +;; + +let register uri url = + (* deliver register request to http_getter *) + ClientHTTP.send + (!getter_url ^ "register" ^ + "?uri=" ^ (UriManager.string_of_uri uri) ^ + "&url=" ^ url) +;; diff --git a/helm/metadata/create2/touch/getter.mli b/helm/metadata/create2/touch/getter.mli new file mode 100644 index 000000000..6b1d2ca29 --- /dev/null +++ b/helm/metadata/create2/touch/getter.mli @@ -0,0 +1,53 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* *) +(******************************************************************************) + +(* THE URL OF THE HTTP GETTER *) +val getter_url : string ref + +(* SIMPLE BINDINGS TO THE HTTP GETTER *) +(* synchronize with the servers *) +val update : unit -> unit + +type format = + Normal + | GZipped +;; + +(* get the xml file *) +(* defaults: format = Normal and patchdtd = true *) +val getxml : ?format:format -> ?patchdtd:bool -> UriManager.uri -> string + +(* adds an (URI -> URL) entry in the map from URIs to URLs *) +val register : UriManager.uri -> string -> unit diff --git a/helm/metadata/create2/touch/pxpUriResolver.ml b/helm/metadata/create2/touch/pxpUriResolver.ml new file mode 100644 index 000000000..1e2fec918 --- /dev/null +++ b/helm/metadata/create2/touch/pxpUriResolver.ml @@ -0,0 +1,266 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 11/10/2000 *) +(* *) +(* *) +(******************************************************************************) + +let resolve s = + let starts_with s s' = + if String.length s < String.length s' then + false + else + (String.sub s 0 (String.length s')) = s' + in + if starts_with s "http:" then + ClientHTTP.get_and_save_to_tmp s + else + s +;; + +(*PXP 1.0 +let url_syntax = + let enable_if = + function + `Not_recognized -> Neturl.Url_part_not_recognized + | `Allowed -> Neturl.Url_part_allowed + | `Required -> Neturl.Url_part_required + in + { Neturl.null_url_syntax with + Neturl.url_enable_scheme = enable_if `Allowed; + Neturl.url_enable_host = enable_if `Allowed; + Neturl.url_enable_path = Neturl.Url_part_required; + Neturl.url_accepts_8bits = true; + } +;; + +exception Unexpected;; (* Added when porting the file to PXP 1.1 *) + +let file_url_of_id xid = + let file_url_of_sysname sysname = + (* By convention, we can assume that sysname is a URL conforming + * to RFC 1738 with the exception that it may contain non-ASCII + * UTF-8 characters. + *) + try + Neturl.url_of_string url_syntax sysname + (* may raise Malformed_URL *) + with + Neturl.Malformed_URL -> raise Pxp_reader.Not_competent + in + let url = + match xid with + Pxp_types.Anonymous -> raise Pxp_reader.Not_competent + | Pxp_types.Public (_,sysname) -> + let sysname = resolve sysname in + if sysname <> "" then file_url_of_sysname sysname + else raise Pxp_reader.Not_competent + | Pxp_types.System sysname -> + let sysname = resolve sysname in + file_url_of_sysname sysname + | Pxp_types.Private pid -> raise Unexpected + in + let scheme = + try Neturl.url_scheme url with Not_found -> "file" in + let host = + try Neturl.url_host url with Not_found -> "" in + + if scheme <> "file" then raise Pxp_reader.Not_competent; + if host <> "" && host <> "localhost" then raise Pxp_reader.Not_competent; + + url +;; + +let from_file ?system_encoding utf8_filename = + + let r = + new Pxp_reader.resolve_as_file + ?system_encoding:system_encoding + ~url_of_id:file_url_of_id + () + in + + let utf8_abs_filename = + if utf8_filename <> "" && utf8_filename.[0] = '/' then + utf8_filename + else + Sys.getcwd() ^ "/" ^ utf8_filename + in + + let syntax = { Neturl.ip_url_syntax with Neturl.url_accepts_8bits = true } in + let url = Neturl.make_url + ~scheme:"file" + ~host:"localhost" + ~path:(Neturl.split_path utf8_abs_filename) + syntax + in + + let xid = Pxp_types.System (Neturl.string_of_url url) in + + + Pxp_yacc.ExtID(xid, r) +;; +*) + +(*PXP 1.1*) +(* csc_pxp_reader.ml is an exact copy of PXP pxp_reader.ml *) +(* The only reason is to loosen the interface *) + +class resolve_as_file + ?(file_prefix = (`Allowed :> Csc_pxp_reader.spec)) + ?(host_prefix = (`Allowed :> Csc_pxp_reader.spec)) + ?(system_encoding = `Enc_utf8) + ?(map_private_id = (fun _ -> raise Csc_pxp_reader.Not_competent)) + ?(open_private_id = (fun _ -> raise Csc_pxp_reader.Not_competent)) + () + = + + let url_syntax = + let enable_if = + function + `Not_recognized -> Neturl.Url_part_not_recognized + | `Allowed -> Neturl.Url_part_allowed + | `Required -> Neturl.Url_part_required + in + { Neturl.null_url_syntax with + Neturl.url_enable_scheme = enable_if file_prefix; + Neturl.url_enable_host = enable_if host_prefix; + Neturl.url_enable_path = Neturl.Url_part_required; + Neturl.url_accepts_8bits = true; + } + in + + let base_url_syntax = + { Neturl.null_url_syntax with + Neturl.url_enable_scheme = Neturl.Url_part_required; + Neturl.url_enable_host = Neturl.Url_part_allowed; + Neturl.url_enable_path = Neturl.Url_part_required; + Neturl.url_accepts_8bits = true; + } + in + + let default_base_url = + Neturl.make_url + ~scheme: "file" + ~host: "" + ~path: (Neturl.split_path (Sys.getcwd() ^ "/")) + base_url_syntax + in + + let file_url_of_id xid = + let module P = Csc_pxp_reader in + let module T = Pxp_types in + let file_url_of_sysname sysname = + (* By convention, we can assume that sysname is a URL conforming + * to RFC 1738 with the exception that it may contain non-ASCII + * UTF-8 characters. + *) + try + Neturl.url_of_string url_syntax sysname + (* may raise Malformed_URL *) + with + Neturl.Malformed_URL -> raise P.Not_competent + in + let url = + match xid with + T.Anonymous -> raise P.Not_competent + | T.Public (_,sysname) -> let sysname = resolve sysname in + if sysname <> "" then file_url_of_sysname sysname + else raise P.Not_competent + | T.System sysname -> let sysname = resolve sysname in + file_url_of_sysname sysname + | T.Private pid -> map_private_id pid + in + let scheme = + try Neturl.url_scheme url with Not_found -> "file" in + let host = + try Neturl.url_host url with Not_found -> "" in + + if scheme <> "file" then raise P.Not_competent; + if host <> "" && host <> "localhost" then raise P.Not_competent; + + url + in + + let channel_of_file_url xid url = + let module P = Csc_pxp_reader in + let module T = Pxp_types in + match xid with + T.Private pid -> open_private_id pid + | _ -> + ( try + let path_utf8 = + try Neturl.join_path (Neturl.url_path ~encoded:false url) + with Not_found -> raise P.Not_competent + in + + let path = + Netconversion.recode_string + ~in_enc: `Enc_utf8 + ~out_enc: system_encoding + path_utf8 in + (* May raise Malformed_code *) + + open_in_bin path, None + (* May raise Sys_error *) + + with + | Netconversion.Malformed_code -> assert false + (* should not happen *) + | Sys_error _ as e -> + raise (P.Not_resolvable e) + ) + in + + Csc_pxp_reader.resolve_read_url_channel + ~base_url: default_base_url + ~url_of_id: file_url_of_id + ~channel_of_url: channel_of_file_url + () +;; + +let from_file ?(alt = []) ?system_encoding ?enc utf8_filename = + let r = + new resolve_as_file + ?system_encoding:system_encoding + () + in + + let url = Csc_pxp_reader.make_file_url + ?system_encoding + ?enc + utf8_filename in + + let xid = Pxp_types.System (Neturl.string_of_url url) in + + Pxp_yacc.ExtID(xid, new Csc_pxp_reader.combine (r :: alt)) +;; + diff --git a/helm/metadata/create2/touch/touch.ml b/helm/metadata/create2/touch/touch.ml new file mode 100644 index 000000000..8538a8faa --- /dev/null +++ b/helm/metadata/create2/touch/touch.ml @@ -0,0 +1,137 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 03/04/2001 *) +(* *) +(* Missing description *) +(* *) +(******************************************************************************) + +let iteri foo = + let counter = ref 0 in + List.iter (function e -> incr counter ; foo e !counter) +;; + +let pathname_of_uri uristring = + "backward" ^ + Str.replace_first (Str.regexp "^cic:") "" uristring +;; + +let make_dirs dirpath = + ignore (Unix.system ("mkdir -p \"" ^ dirpath ^ "\"")) +;; + +let touch_file rdf_string_uri = + let module U = UriManager in + let rdf_uri = U.uri_of_string rdf_string_uri in + make_dirs (pathname_of_uri (U.buri_of_uri rdf_uri)) ; + ignore ( + Unix.system + ("touch \"" ^ (pathname_of_uri rdf_string_uri) ^ "\"") + ) +;; + +let get_obj uri = + let cicfilename = Getter.getxml uri in + let res = + match CicParser.term_of_xml cicfilename uri false with + (annobj, None) -> + Deannotate.deannotate_obj annobj + | _ -> assert false + in + Unix.unlink cicfilename ; + res +;; + +let touch_obj string_uri = + let module U = UriManager in + let module C = Cic in + function + Some (C.InductiveDefinition (itys,_,_)) -> + iteri + (fun (_,_,_,cons) n -> + let sn = string_of_int n in + touch_file + (string_uri ^ "," ^ sn) ; + iteri + (fun (_,_,_) m -> + let sm = string_of_int m in + touch_file + (string_uri ^ "," ^ sn ^ "," ^ sm) + ) cons + ) itys + | Some _ -> assert false + | None -> + touch_file string_uri +;; + +let touch string_uri = + let module S = String in + let module U = UriManager in + print_endline ("Now touching metadata file for " ^ string_uri) ; + flush stdout ; + let uri = U.uri_of_string string_uri in + let obj = + if S.sub string_uri (S.length string_uri - 3) 3 = "ind" then + Some (get_obj uri) + else + None + in + touch_obj string_uri obj +;; + +let _ = + let usage_msg = "usage: touch[.opt] URI" in + let uri = ref "" in + Arg.parse [] + (fun x -> + if x = "" then + begin + prerr_string "No URI provided.\n" ; + Arg.usage [] usage_msg ; + exit (-1) + end + else if !uri = "" then + uri := x + else + begin + prerr_string "More than two arguments provided.\n" ; + Arg.usage [] usage_msg ; + exit (-1) + end + ) usage_msg ; + if !uri = "" then + begin + prerr_string "No URI provided.\n" ; + Arg.usage [] usage_msg ; + exit (-1) + end ; + touch !uri +;; diff --git a/helm/metadata/create2/touch/uriManager.ml b/helm/metadata/create2/touch/uriManager.ml new file mode 100644 index 000000000..0fa24cfcd --- /dev/null +++ b/helm/metadata/create2/touch/uriManager.ml @@ -0,0 +1,139 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* "cic:/a/b/c.con" => [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c" |] *) +type uri = string array;; + +let eq uri1 uri2 = + uri1 == uri2 +;; + +let string_of_uri uri = uri.(Array.length uri - 2);; +let name_of_uri uri = uri.(Array.length uri - 1);; +let buri_of_uri uri = uri.(Array.length uri - 3);; +let depth_of_uri uri = Array.length uri - 2;; + +(*CSC: ora e' diventato poco efficiente, migliorare *) +let relative_depth curi uri cookingsno = + let rec length_of_current_prefix l1 l2 = + match (l1, l2) with + (he1::tl1, he2::tl2) when he1 == he2 -> + 1 + length_of_current_prefix tl1 tl2 + | (_,_) -> 0 + in + depth_of_uri uri - + length_of_current_prefix + (Array.to_list (Array.sub curi 0 (Array.length curi - (2 + cookingsno)))) + (Array.to_list (Array.sub uri 0 (Array.length uri - 2))) + (*CSC: vecchio codice da eliminare + if eq curi uri then 0 + else + depth_of_uri uri - + length_of_current_prefix (Array.to_list curi) (Array.to_list uri) + *) +;; + +module OrderedStrings = + struct + type t = string + let compare (s1 : t) (s2 : t) = compare s1 s2 + end +;; + +module SetOfStrings = Map.Make(OrderedStrings);; + +(*CSC: commento obsoleto ed errato *) +(* Invariant: the map is the identity function, *) +(* i.e. (SetOfStrings.find str !set_of_uri) == str *) +let set_of_uri = ref SetOfStrings.empty;; +let set_of_prefixes = ref SetOfStrings.empty;; + +(* similar to uri_of_string, but used for prefixes of uris *) +let normalize prefix = + try + SetOfStrings.find prefix !set_of_prefixes + with + Not_found -> + set_of_prefixes := SetOfStrings.add prefix prefix !set_of_prefixes ; + prefix +;; + +exception IllFormedUri of string;; + +let mk_prefixes str = + let rec aux curi = + function + [he] -> + let prefix_uri = curi ^ "/" ^ he + and name = List.hd (Str.split (Str.regexp "\.") he) in + [ normalize prefix_uri ; name ] + | he::tl -> + let prefix_uri = curi ^ "/" ^ he in + (normalize prefix_uri)::(aux prefix_uri tl) + | _ -> raise (IllFormedUri str) + in + let tokens = (Str.split (Str.regexp "/") str) in + (* ty = "cic:" *) + let (ty, sp) = (List.hd tokens, List.tl tokens) in + aux ty sp +;; + +let uri_of_string str = + try + SetOfStrings.find str !set_of_uri + with + Not_found -> + let uri = Array.of_list (mk_prefixes str) in + set_of_uri := SetOfStrings.add str uri !set_of_uri ; + uri +;; + +let cicuri_of_uri uri = + let completeuri = string_of_uri uri in + let newcompleteuri = + (Str.replace_first (Str.regexp "\.types$") "" + (Str.replace_first (Str.regexp "\.ann$") "" completeuri)) + in + if completeuri = newcompleteuri then + uri + else + let newuri = Array.copy uri in + newuri.(Array.length uri - 2) <- newcompleteuri ; + newuri +;; + +let annuri_of_uri uri = + let completeuri = string_of_uri uri in + if Str.string_match (Str.regexp ".*\.ann$") completeuri 0 then + uri + else + let newuri = Array.copy uri in + newuri.(Array.length uri - 2) <- completeuri ^ ".ann" ; + newuri +;; + +let uri_is_annuri uri = + Str.string_match (Str.regexp ".*\.ann$") (string_of_uri uri) 0 +;; diff --git a/helm/metadata/create2/touch/uriManager.mli b/helm/metadata/create2/touch/uriManager.mli new file mode 100644 index 000000000..2cdd27e3d --- /dev/null +++ b/helm/metadata/create2/touch/uriManager.mli @@ -0,0 +1,51 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +type uri + +val eq : uri -> uri -> bool + +val uri_of_string : string -> uri + +val string_of_uri : uri -> string (* complete uri *) +val name_of_uri : uri -> string (* name only (without extension)*) +val buri_of_uri : uri -> string (* base uri only *) +val depth_of_uri : uri -> int (* length of the path *) + +(* relative_depth curi uri cookingsno *) +(* is the number of times to cook uri to use it when the current uri is curi *) +(* cooked cookingsno times *) +val relative_depth : uri -> uri -> int -> int + +(* given an uri, returns the uri of the corresponding cic file, *) +(* i.e. removes the [.types][.ann] suffix *) +val cicuri_of_uri : uri -> uri + +(* given an uri, returns the uri of the corresponding annotation file, *) +(* i.e. adds the .ann suffix if not already present *) +val annuri_of_uri : uri -> uri + +(* given an uri, tells if it refers to an annotation *) +val uri_is_annuri : uri -> bool diff --git a/helm/metadata/create/uris_of_filenames.pl b/helm/metadata/create2/uris_of_filenames.pl similarity index 56% rename from helm/metadata/create/uris_of_filenames.pl rename to helm/metadata/create2/uris_of_filenames.pl index f67d30d4f..db835bf9c 100755 --- a/helm/metadata/create/uris_of_filenames.pl +++ b/helm/metadata/create2/uris_of_filenames.pl @@ -6,8 +6,8 @@ while() { for (@_) { $GZSUFF = ""; if (/.gz$/) - { s/.gz$//; $GZSUFF = " gz" if ($ARGV[0] == "-gz"); } - s/\./helm:rdf:www.cs.unibo.it\/helm\/rdf\/rdfprova\/\/cic:/; + { s/.gz$//; $GZSUFF = " gz" if ($ARGV[1] == "-gz"); } + s/\./helm:rdf:www.cs.unibo.it\/helm\/rdf\/$ARGV[0]\/\/cic:/; s/\.xml//; print $_.$GZSUFF."\n"; } diff --git a/helm/metadata/xslt/occurrences.xsl b/helm/metadata/xslt/occurrences.xsl deleted file mode 100644 index 55dbacbcc..000000000 --- a/helm/metadata/xslt/occurrences.xsl +++ /dev/null @@ -1,554 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - , - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ; - - - - - - - - - - - ; - - - - - - - - - - - - - - - - - - - - - - - - - ; - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -- 2.39.2