+++ /dev/null
-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/*
+++ /dev/null
-#!/usr/bin/perl
-
-$filename = $uri = $ARGV[0];
-$outputfile = $filename.".xml";
-$uri =~ s/^rdf/cic:/;
-$uri =~ s/(.*),([^,]*),([^,]*)/$1#xpointer(1\/$2\/$3)/;
-$uri =~ s/(.*),([^,]*)/$1#xpointer(1\/$2)/;
-
-print "Now processing file $filename\n";
-
-open(HEADER,">>$outputfile");
-print HEADER <<EOT;
-<?xml version="1.0" encoding="UTF-8"?>
-<occurs who="$uri">
-EOT
-close(HEADER);
-
-system("cat $filename >> $outputfile");
-
-open(FOOTER,">>$outputfile");
-print FOOTER <<EOT;
-</occurs>
-EOT
-close(FOOTER);
-
-unlink $filename;
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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;
-}
+++ /dev/null
-#!/usr/bin/perl
-
-foreach $inputfile (@ARGV) {
- print "Now splitting file $inputfile\n";
- open(IN, "<$inputfile");
- while($line = <IN>) {
- if (not ($line =~ /^<?xml/ || $line =~/^<(\/|)occurrences>/)) {
- if ($line =~ /^<!--/) {
- # Begin of a new output file
- $line =~ s/^<!--(.*)-->$/$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);
+++ /dev/null
-#!/usr/bin/perl
-
-while(<STDIN>) {
- chomp;
- split / /;
- for (@_) {
- $GZSUFF = "";
- if (/.gz$/)
- { s/.gz$//; $GZSUFF = " gz" if ($ARGV[0] == "-gz"); }
- s/\./helm:rdf:www.cs.unibo.it\/helm\/rdf\/rdfprova\/\/cic:/;
- s/\.xml//;
- print $_.$GZSUFF."\n";
- }
-}
--- /dev/null
+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
--- /dev/null
+#!/usr/bin/perl
+
+$filename = $uri = $ARGV[0];
+$outputfile = $filename.".xml";
+$uri =~ s/^backward/cic:/;
+$uri =~ s/(.*),([^,]*),([^,]*)/$1#xpointer(1\/$2\/$3)/;
+$uri =~ s/(.*),([^,]*)/$1#xpointer(1\/$2)/;
+
+print "Now processing file $filename\n";
+
+open(HEADER,">>$outputfile");
+print HEADER <<EOT;
+<?xml version="1.0" encoding="ISO-8859-1"?>
+
+<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#">
+ <h:Object rdf:about="$uri">
+EOT
+close(HEADER);
+
+system("cat $filename >> $outputfile");
+
+open(FOOTER,">>$outputfile");
+print FOOTER <<EOT;
+ </h:Object>
+</rdf:RDF>
+EOT
+close(FOOTER);
+
+unlink $filename;
--- /dev/null
+#!/usr/bin/perl
+
+my $inputfile = $ARGV[0];
+
+print "Now splitting file $inputfile\n";
+open(IN, "<$inputfile") or die "Error opening file $inputfile";
+$dummy = <IN>; # <?xml version="1.0" encoding="ISO-8859-1"?>
+$dummy = <IN>; #
+$dummy = <IN>; # <rdf:RDF .../>
+$where = <IN>; # <h:Object rdf:about="...">
+chomp($where);
+$where =~ s/^[^"]*"([^"]*)">$/$1/;
+while(($line1 = <IN>) && not ($line1 =~ /<\/h:Object>/)) {
+ $line2 = <IN>;
+ $line3 = <IN>; # </refObj>
+ $uri = $line2;
+ chomp($uri);
+ $uri =~ s/^ *<h:Occurrence rdf:about="[^"]*" rdf:value="([^"]*)"\/>$/$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 " <h:backpointer>\n";
+ print OUT $line2;
+ print OUT " </h:backpointer>\n";
+ close(OUT);
+}
+close(IN);
--- /dev/null
+*.cmi *.cmo *.cmx .depend mk_forward mk_forward.opt configuration.ml
--- /dev/null
+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
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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 *)
+;;
--- /dev/null
+(* 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)
+;;
--- /dev/null
+(* 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
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
+;;
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
--- /dev/null
+(* 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 <sacerdot@@cs.unibo.it> *)
+(* 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)
+;;
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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. <type> ... </type> *)
+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))
+ ]
+ ()
+;;
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
--- /dev/null
+(* 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
+;;
--- /dev/null
+(* 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
--- /dev/null
+(* 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
+;;
--- /dev/null
+(* 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
--- /dev/null
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 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 <value-of> 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;;
+
--- /dev/null
+(* $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.
+ *
+ *
+ *)
--- /dev/null
+(* 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)
+;;
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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)
+;;
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\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
+;;
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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))
+;;
+
--- /dev/null
+(* 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
+;;
--- /dev/null
+(* 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
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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 ^ ">\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
+;;
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
--- /dev/null
+#!/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
--- /dev/null
+*.cmi *.cmo *.cmx .depend touch touch.opt configuration.ml
--- /dev/null
+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
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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 *)
+;;
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
+;;
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
--- /dev/null
+(* 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 <sacerdot@@cs.unibo.it> *)
+(* 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)
+;;
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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. <type> ... </type> *)
+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))
+ ]
+ ()
+;;
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
--- /dev/null
+(* 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
+;;
--- /dev/null
+(* 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
--- /dev/null
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 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 <value-of> 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;;
+
--- /dev/null
+(* $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.
+ *
+ *
+ *)
--- /dev/null
+(* 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)
+;;
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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)
+;;
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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))
+;;
+
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
+;;
--- /dev/null
+(* 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
+;;
--- /dev/null
+(* 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
--- /dev/null
+#!/usr/bin/perl
+
+while(<STDIN>) {
+ chomp;
+ split / /;
+ for (@_) {
+ $GZSUFF = "";
+ if (/.gz$/)
+ { 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";
+ }
+}
+++ /dev/null
-<?xml version="1.0"?>
-
-<!-- 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/. -->
-
-<xsl:stylesheet version="0.1" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
-
-<xsl:param name="CICURI" select="''"/>
-
-<!-- <xsl:output method="html"/> -->
-<xsl:output method="xml"/>
-
-
-<xsl:template match="/">
- <occurrences>
- <xsl:text>
</xsl:text>
- <xsl:apply-templates select="*"/>
- </occurrences>
-</xsl:template>
-
-
-
-
-<!-- AGGIUNGERE cic: alle uri nei file Theory -->
-
-
-<xsl:template match="InductiveDefinition">
- <!-- The case of Inductive Definitions is peculiar due to REL -->
- <!-- Before reading this part, first look at the otherwise case -->
- <xsl:variable name="block" select="."/>
- <xsl:for-each select="InductiveType">
- <xsl:variable name="noType" select="position()"/>
- <xsl:for-each select="Constructor/*[1]">
- <xsl:variable name="noConstr" select="position()"/>
- <xsl:variable name="my_uri"
- select="concat($CICURI,'#','xpointer(1/',$noType,'/',$noConstr,
- ')')"/>
- <xsl:comment><xsl:value-of select="concat($CICURI,'#','xpointer(1/',$noType,')')"/></xsl:comment>
- <xsl:text>
</xsl:text>
- <main uri="{$my_uri}"/>
- <xsl:text>
</xsl:text>
- <xsl:variable name="inside_concl">
- <xsl:call-template name="look_for_main">
- <xsl:with-param name="current" select="."/>
- </xsl:call-template>
- </xsl:variable>
- <xsl:call-template name="build_pairs">
- <xsl:with-param name="uri" select="$my_uri"/>
- <xsl:with-param name="list" select="$inside_concl"/>
- <xsl:with-param name="kind" select="'in_conclusion'"/>
- </xsl:call-template>
- <xsl:variable name="main_hypothesis">
- <xsl:call-template name="look_for_main_hypothesis_of_constructor">
- <xsl:with-param name="current" select="."/>
- <xsl:with-param name="list" select="''"/>
- <xsl:with-param name="inductive_block" select="$block"/>
- <xsl:with-param name="inductive_uri" select="$CICURI"/>
- </xsl:call-template>
- </xsl:variable>
- <xsl:call-template name="build_pairs">
- <xsl:with-param name="uri" select="$my_uri"/>
- <xsl:with-param name="list" select="$main_hypothesis"/>
- <xsl:with-param name="kind" select="'main_hypothesis'"/>
- </xsl:call-template>
- <xsl:variable name="inside_hypothesis">
- <xsl:call-template name="look_for_hypothesis">
- <xsl:with-param name="current" select="."/>
- <xsl:with-param name="list" select="''"/>
- <xsl:with-param name="not_in" select="$main_hypothesis"/>
- </xsl:call-template>
- </xsl:variable>
- <xsl:call-template name="build_pairs">
- <xsl:with-param name="uri" select="$my_uri"/>
- <xsl:with-param name="list" select="$inside_hypothesis"/>
- <xsl:with-param name="kind" select="'in_hypothesis'"/>
- </xsl:call-template>
- </xsl:for-each>
- </xsl:for-each>
-</xsl:template>
-
-<xsl:template match="Definition|Axiom|CurrentProof|Variable">
- <!-- Definition, Axiom, CurrentProof and Variable -->
- <!-- all of them have a type -->
- <!-- first look for the main target of the type -->
- <!-- inside_concl contains the list of all identifiers occurring -->
- <!-- in the main target of the type. The main identifiers, if it -->
- <!-- exists, is in head position, separated by a comma form the -->
- <!-- other elements. All other elements are separated by a semicolon -->
- <xsl:variable name="inside_concl">
- <xsl:call-template name="look_for_main">
- <xsl:with-param name="current" select="type/*[1]"/>
- </xsl:call-template>
- </xsl:variable>
- <!-- variable main contains the (possibly empty) uri of the "main"
- identifier -->
- <xsl:variable name="main" select="substring-before($inside_concl,',')"/>
- <xsl:choose>
- <xsl:when test="$main = ''">
- <xsl:call-template name="build_pairs">
- <xsl:with-param name="uri" select="$CICURI"/>
- <xsl:with-param name="list" select="$inside_concl"/>
- <xsl:with-param name="kind" select="'in_conclusion'"/>
- </xsl:call-template>
- </xsl:when>
- <xsl:otherwise>
- <xsl:comment><xsl:value-of select="$main"/></xsl:comment>
- <xsl:text>
</xsl:text>
- <main uri="{$CICURI}"/>
- <xsl:text>
</xsl:text>
- <xsl:call-template name="build_pairs">
- <xsl:with-param name="uri" select="$CICURI"/>
- <xsl:with-param name="list" select="substring-after($inside_concl,',')"/>
- <xsl:with-param name="kind" select="'in_conclusion'"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
- <!-- now look for the main identifiers inside the hipothesis -->
- <xsl:variable name="main_hypothesis">
- <xsl:call-template name="look_for_main_hypothesis">
- <xsl:with-param name="current" select="type/*[1]"/>
- <xsl:with-param name="list" select="''"/>
- </xsl:call-template>
- </xsl:variable>
- <xsl:call-template name="build_pairs">
- <xsl:with-param name="uri" select="$CICURI"/>
- <xsl:with-param name="list" select="$main_hypothesis"/>
- <xsl:with-param name="kind" select="'main_hypothesis'"/>
- </xsl:call-template>
- <!-- now look for the all other identifiers inside the hipothesis -->
- <xsl:variable name="inside_hypothesis">
- <xsl:call-template name="look_for_hypothesis">
- <xsl:with-param name="current" select="type/*[1]"/>
- <xsl:with-param name="list" select="''"/>
- <xsl:with-param name="not_in" select="$main_hypothesis"/>
- </xsl:call-template>
- </xsl:variable>
- <xsl:call-template name="build_pairs">
- <xsl:with-param name="uri" select="$CICURI"/>
- <xsl:with-param name="list" select="$inside_hypothesis"/>
- <xsl:with-param name="kind" select="'in_hypothesis'"/>
- </xsl:call-template>
- <!-- Definition, Axiom, CurrentProof and Variable possibly -->
- <!-- have a body -->
- <xsl:if test="body">
- <xsl:variable name="inside_body">
- <xsl:call-template name="list_all">
- <xsl:with-param name="node" select="body/*[1]"/>
- <xsl:with-param name="not_in" select="concat($inside_hypothesis,';',$main_hypothesis,';',$inside_concl)"/>
- </xsl:call-template>
- </xsl:variable>
- <xsl:call-template name="build_pairs">
- <xsl:with-param name="uri" select="$CICURI"/>
- <xsl:with-param name="list" select="$inside_body"/>
- <xsl:with-param name="kind" select="'in_body'"/>
- </xsl:call-template>
- </xsl:if>
-</xsl:template>
-
- <!-- look_for_main recursively descend along the type looking for -->
- <!-- the main target. Then returns the list of all identifiers occurring -->
- <!-- in it. The main identifiers, if it exists, is in head position, -->
- <!-- separated by a comma form the other elements. -->
- <!-- All other elements are separated by a semicolon -->
-
-<xsl:template name="look_for_main">
- <xsl:param name="current" select="/.."/>
- <xsl:choose>
- <xsl:when test="name($current) = 'PROD'">
- <xsl:call-template name="look_for_main">
- <xsl:with-param name="current" select="$current/target/*[1]"/>
- </xsl:call-template>
- </xsl:when>
- <xsl:otherwise>
- <xsl:variable name="main">
- <xsl:choose>
- <xsl:when test="name($current) = 'APPLY'">
- <xsl:call-template name="get_expanded_name">
- <xsl:with-param name="node" select="$current/*[1]"/>
- </xsl:call-template>
- </xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="get_expanded_name">
- <xsl:with-param name="node" select="$current"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:variable>
- <xsl:choose>
- <xsl:when test="$main != ''">
- <xsl:value-of select="$main"/><xsl:text>,</xsl:text>
- <xsl:call-template name="list_all">
- <xsl:with-param name="node" select="$current"/>
- <xsl:with-param name="not_in" select="$main"/>
- </xsl:call-template>
- </xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="list_all">
- <xsl:with-param name="node" select="$current"/>
- <xsl:with-param name="not_in" select="''"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<!-- in case "node" is a CONST, MUTIND or MUTCONSTRUCT, the -->
-<!-- function get_expanded_name returns the (expanded) uri of the -->
-<!-- node. Otherwise it returns an empty string -->
-
-<xsl:template name="get_expanded_name">
- <xsl:param name="node" select="/.."/>
- <xsl:choose>
- <xsl:when test="name($node)='CONST'">
- <xsl:value-of select="$node/@uri"/>
- </xsl:when>
- <xsl:when test="name($node)='MUTIND'">
- <xsl:variable name="noType" select="$node/@noType + 1"/>
- <xsl:value-of select="concat($node/@uri,'#','xpointer(1/',
- $noType,')')"/>
- </xsl:when>
- <xsl:when test="name($node)='MUTCONSTRUCT'">
- <xsl:variable name="noType" select="$node/@noType + 1"/>
- <xsl:value-of select="concat($node/@uri,'#','xpointer(1/',
- $noType,'/',$node/@noConstr,')')"/>
- </xsl:when>
- </xsl:choose>
-</xsl:template>
-
-
-<xsl:template name="get_expanded_name_with_rel_case">
- <xsl:param name="node" select="/.."/>
- <xsl:param name="inductive_block" select="/.."/>
- <xsl:param name="inductive_uri" select="''"/>
- <xsl:choose>
- <xsl:when test="name($node)='CONST'">
- <xsl:value-of select="$node/@uri"/>
- </xsl:when>
- <xsl:when test="name($node)='MUTIND'">
- <xsl:variable name="noType" select="$node/@noType + 1"/>
- <xsl:value-of select="concat($node/@uri,'#','xpointer(1/',
- $noType,')')"/>
- </xsl:when>
- <xsl:when test="name($node)='MUTCONSTRUCT'">
- <xsl:variable name="noType" select="$node/@noType + 1"/>
- <xsl:value-of select="concat($node/@uri,'#','xpointer(1/',
- $noType,'/',$node/@noConstr,')')"/>
- </xsl:when>
- <xsl:when test="name($node)='REL'">
- <xsl:variable name="binder" select="$node/@binder"/>
- <xsl:if test="$inductive_block/InductiveType[@name=$binder]">
- <xsl:variable name="position">
- <xsl:for-each select="$inductive_block/InductiveType">
- <xsl:if test="@name=$binder">
- <xsl:value-of select="position()"/>
- </xsl:if>
- </xsl:for-each>
- </xsl:variable>
- <xsl:value-of select="concat($inductive_uri,'#','xpointer(1/',
- $position,')')"/>
- </xsl:if>
- </xsl:when>
- </xsl:choose>
-</xsl:template>
-
-<!-- The function look_for_main_hypothesis returns the list of all
- the uris of identifiers occurring in head position of some
- of the hypothesis -->
-
-<xsl:template name="look_for_main_hypothesis">
- <xsl:param name="current" select="/.."/>
- <xsl:param name="list" select="''"/>
- <xsl:choose>
- <xsl:when test="name($current) = 'PROD'">
- <xsl:variable name="source" select="$current/source/*[1]"/>
- <xsl:variable name="main">
- <xsl:choose>
- <xsl:when test="name($source) = 'APPLY'">
- <xsl:call-template name="get_expanded_name">
- <xsl:with-param name="node" select="$source/*[1]"/>
- </xsl:call-template>
- </xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="get_expanded_name">
- <xsl:with-param name="node" select="$source"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:variable>
- <xsl:choose>
- <xsl:when test="($main != '') and (not(contains($list,$main)))">
- <xsl:call-template name="look_for_main_hypothesis">
- <xsl:with-param name="current" select="$current/target/*[1]"/>
- <xsl:with-param name="list" select="concat($main,';',$list)"/>
- </xsl:call-template>
- </xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="look_for_main_hypothesis">
- <xsl:with-param name="current" select="$current/target/*[1]"/>
- <xsl:with-param name="list" select="$list"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <xsl:otherwise>
- <xsl:value-of select="$list"/>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<xsl:template name="look_for_main_hypothesis_of_constructor">
- <xsl:param name="current" select="/.."/>
- <xsl:param name="list" select="''"/>
- <xsl:param name="inductive_block" select="/.."/>
- <xsl:param name="inductive_uri" select="''"/>
- <xsl:choose>
- <xsl:when test="name($current) = 'PROD'">
- <xsl:variable name="source" select="$current/source/*[1]"/>
- <xsl:variable name="main">
- <xsl:choose>
- <xsl:when test="name($source) = 'APPLY'">
- <xsl:call-template name="get_expanded_name_with_rel_case">
- <xsl:with-param name="node" select="$source/*[1]"/>
- <xsl:with-param name="inductive_block" select="$inductive_block"/>
- <xsl:with-param name="inductive_uri" select="$inductive_uri"/>
- </xsl:call-template>
- </xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="get_expanded_name_with_rel_case">
- <xsl:with-param name="node" select="$source"/>
- <xsl:with-param name="inductive_block" select="$inductive_block"/>
- <xsl:with-param name="inductive_uri" select="$inductive_uri"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:variable>
- <xsl:choose>
- <xsl:when test="($main != '') and (not(contains($list,$main)))">
- <xsl:call-template name="look_for_main_hypothesis_of_constructor">
- <xsl:with-param name="current" select="$current/target/*[1]"/>
- <xsl:with-param name="list" select="concat($main,';',$list)"/>
- <xsl:with-param name="inductive_block" select="$inductive_block"/>
- <xsl:with-param name="inductive_uri" select="$inductive_uri"/>
- </xsl:call-template>
- </xsl:when>
- <xsl:otherwise>
- <xsl:call-template name="look_for_main_hypothesis_of_constructor">
- <xsl:with-param name="current" select="$current/target/*[1]"/>
- <xsl:with-param name="list" select="$list"/>
- <xsl:with-param name="inductive_block" select="$inductive_block"/>
- <xsl:with-param name="inductive_uri" select="$inductive_uri"/>
- </xsl:call-template>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <xsl:otherwise>
- <xsl:value-of select="$list"/>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<!-- look_for_hypothesis returns the list of uris of all other
-identifiers occurring inside the hypothesis -->
-
-<xsl:template name="look_for_hypothesis">
- <xsl:param name="current" select="/.."/>
- <xsl:param name="list" select="''"/>
- <xsl:param name="not_in" select="''"/>
- <xsl:choose>
- <xsl:when test="name($current) = 'PROD'">
- <xsl:variable name="source" select="$current/source/*[1]"/>
- <xsl:variable name="add_to_list">
- <xsl:call-template name="list_all">
- <xsl:with-param name="node" select="$source"/>
- <xsl:with-param name="not_in" select="$not_in"/>
- </xsl:call-template>
- </xsl:variable>
- <xsl:call-template name="look_for_hypothesis">
- <xsl:with-param name="current" select="$current/target/*[1]"/>
- <xsl:with-param name="list" select="concat($list,$add_to_list)"/>
- <xsl:with-param name="not_in" select="concat($not_in,$add_to_list)"/>
- </xsl:call-template>
- </xsl:when>
- <xsl:otherwise>
- <xsl:value-of select="$list"/>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<!-- list_all returns a list of all uris of CONST, MUTIND, and MUTCONSTRUCT -->
-<!-- elements appearing inside a given node, and not already contained -->
-<!-- in the not_in list -->
-
-<xsl:template name="list_all">
- <xsl:param name="node" select="/.."/>
- <xsl:param name="not_in" select="''"/>
- <xsl:variable name="all">
- <xsl:choose>
- <xsl:when test="$not_in = ''">
- <xsl:for-each select="$node//*[name()='CONST' or name()='MUTIND' or name()='MUTCONSTRUCT']">
- <xsl:sort select="@uri"/>
- <xsl:sort select="@noType"/>
- <xsl:sort select="@noConstr"/>
- <xsl:call-template name="get_expanded_name">
- <xsl:with-param name="node" select="."/>
- </xsl:call-template>
- <xsl:text>;</xsl:text>
- </xsl:for-each>
- </xsl:when>
- <xsl:otherwise>
- <xsl:for-each select="$node//*[(name()='CONST' and not(contains($not_in,@uri))) or (name()='MUTIND' and not(contains($not_in,concat(@uri,'#','xpointer(1/',@noType + 1,')')))) or (name()='MUTCONSTRUCT' and not(contains($not_in,concat(@uri,'#','xpointer(1/',@noType + 1,'/'
-,@noConstr,')'))))]">
- <xsl:sort select="@uri"/>
- <xsl:sort select="@noType"/>
- <xsl:sort select="@noConstr"/>
- <xsl:call-template name="get_expanded_name">
- <xsl:with-param name="node" select="."/>
- </xsl:call-template>
- <xsl:text>;</xsl:text>
- </xsl:for-each>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:variable>
- <xsl:call-template name="drop_repetitions">
- <xsl:with-param name="head" select="''"/>
- <xsl:with-param name="tail" select="$all"/>
- </xsl:call-template>
-</xsl:template>
-
-<!-- This is a different possible implementation of list_all -->
-<!-- It seems to be less effective than the previous one -->
-<!--
-<xsl:template name="list_all">
- <xsl:param name="node" select="/.."/>
- <xsl:param name="not_in" select="''"/>
- <xsl:apply-templates select="$node/*[1]" mode="list_all">
- <xsl:with-param name="not_in" select="$not_in"/>
- </xsl:apply-templates>
-</xsl:template>
-
-<xsl:template match="*" mode="list_all">
- <xsl:param name="not_in" select="''"/>
- <xsl:variable name="uri_to_add">
- <xsl:choose>
- <xsl:when test="name()='CONST' and not(contains($not_in,@uri))">
- <xsl:value-of select="@uri"/><xsl:text>;</xsl:text>
- </xsl:when>
- <xsl:when test="name()='MUTIND' and not(contains($not_in,concat(@uri,'#',@noType)))">
- <xsl:value-of select="concat(@uri,'#',@noType)"/><xsl:text>;</xsl:text>
- </xsl:when>
- <xsl:when test="name()='MUTCONSTRUCT' and not(contains($not_in,concat(@uri,'#',@noType,'#',@noConstr)))">
- <xsl:value-of select="concat(@uri,'#',@noType,'#',@noConstr)"/><xsl:text>;</xsl:text>
- </xsl:when>
- </xsl:choose>
- </xsl:variable>
- <xsl:value-of select="$uri_to_add"/>
- <xsl:variable name="child_list">
- <xsl:if test="count(child::*) != 0">
- <xsl:apply-templates select="*[1]" mode="list_all">
- <xsl:with-param name="not_in" select="concat($not_in,$uri_to_add)"/>
- </xsl:apply-templates>
- </xsl:if>
- </xsl:variable>
- <xsl:value-of select="$child_list"/>
- <xsl:if test="count(following-sibling::*) != 0">
- <xsl:apply-templates select="following-sibling::*[1]" mode="list_all">
- <xsl:with-param name="not_in" select="concat($not_in,$uri_to_add,$child_list)"/>
- </xsl:apply-templates>
- </xsl:if>
-</xsl:template>
--->
-
-<!-- The drop_repetitions function drops all repeated strigs in a -->
-<!-- ORDERED list of strings separated by semicolons -->
-
-<xsl:template name="drop_repetitions">
- <xsl:param name="head" select="''"/>
- <xsl:param name="tail" select="''"/>
- <xsl:if test="not($tail = '')">
- <xsl:variable name="newhead" select="substring-before($tail,';')"/>
- <xsl:variable name="newtail" select="substring-after($tail,';')"/>
- <xsl:if test="not($newhead = $head)">
- <xsl:value-of select="$newhead"/><xsl:text>;</xsl:text>
- </xsl:if>
- <xsl:call-template name="drop_repetitions">
- <xsl:with-param name="head" select="$newhead"/>
- <xsl:with-param name="tail" select="$newtail"/>
- </xsl:call-template>
- </xsl:if>
-</xsl:template>
-
-<!-- the function build_pairs takes in input a uri (uri), -->
-<!-- a list of uris (list) and a "kind" string, and returns -->
-<!-- a list of xml elements name "kind containing as first -->
-<!-- attribute an element of the list and as second attribute -->
-<!-- the given uri -->
-<xsl:template name="build_pairs">
- <xsl:param name="uri" select="''"/>
- <xsl:param name="list" select="''"/>
- <xsl:param name="kind" select="''"/>
- <xsl:if test="$list != ''">
- <xsl:variable name="head" select="substring-before($list,';')"/>
- <xsl:variable name="tail" select="substring-after($list,';')"/>
- <xsl:comment><xsl:value-of select="$head"/></xsl:comment>
- <xsl:text>
</xsl:text>
- <xsl:element name="{$kind}">
- <xsl:attribute name="uri"><xsl:value-of select="$uri"/></xsl:attribute>
- </xsl:element>
- <xsl:text>
</xsl:text>
- <xsl:call-template name="build_pairs">
- <xsl:with-param name="uri" select="$uri"/>
- <xsl:with-param name="list" select="$tail"/>
- <xsl:with-param name="kind" select="$kind"/>
- </xsl:call-template>
- </xsl:if>
-</xsl:template>
-
-
-
-</xsl:stylesheet>
-
-
-
-
-
-
-
-
-
-
-
-
-
projects / helm.git / commitdiff