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