From 5a92117eeff70048d29e91ba24e113155d956e1b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 26 Nov 2001 18:28:28 +0000 Subject: [PATCH] HELM OCaml libraries with findlib support. --- helm/ocaml/META.helm-cic | 6 + helm/ocaml/META.helm-cic_annotations | 6 + helm/ocaml/META.helm-cic_annotations_cache | 6 + helm/ocaml/META.helm-cic_cache | 6 + helm/ocaml/META.helm-cic_proof_checking | 8 + helm/ocaml/META.helm-getter | 6 + helm/ocaml/META.helm-pxp | 6 + helm/ocaml/META.helm-urimanager | 6 + helm/ocaml/META.helm-xml | 6 + helm/ocaml/cic/Makefile | 37 + helm/ocaml/cic/cic.ml | 162 +++ helm/ocaml/cic/cicParser.ml | 95 ++ helm/ocaml/cic/cicParser.mli | 44 + helm/ocaml/cic/cicParser2.ml | 289 ++++ helm/ocaml/cic/cicParser2.mli | 57 + helm/ocaml/cic/cicParser3.ml | 565 ++++++++ helm/ocaml/cic/cicParser3.mli | 67 + helm/ocaml/cic/deannotate.ml | 98 ++ helm/ocaml/cic_annotations/Makefile | 39 + .../cic_annotations/cicAnnotation2Xml.ml | 225 +++ .../cic_annotations/cicAnnotationHinter.ml | 381 +++++ .../cic_annotations/cicAnnotationParser.ml | 55 + .../cic_annotations/cicAnnotationParser2.ml | 129 ++ helm/ocaml/cic_annotations/cicXPath.ml | 77 + helm/ocaml/cic_annotations_cache/Makefile | 36 + helm/ocaml/cic_annotations_cache/cicCache.ml | 51 + helm/ocaml/cic_annotations_cache/cicCache.mli | 37 + helm/ocaml/cic_cache/Makefile | 36 + helm/ocaml/cic_cache/cicCache.ml | 49 + helm/ocaml/cic_cache/cicCache.mli | 37 + helm/ocaml/cic_proof_checking/Makefile | 41 + helm/ocaml/cic_proof_checking/cicCooking.ml | 217 +++ helm/ocaml/cic_proof_checking/cicCooking.mli | 31 + .../cic_proof_checking/cicEnvironment.ml | 217 +++ .../cic_proof_checking/cicEnvironment.mli | 83 ++ .../cic_proof_checking/cicMiniReduction.ml | 60 + .../cic_proof_checking/cicMiniReduction.mli | 26 + helm/ocaml/cic_proof_checking/cicPp.ml | 211 +++ helm/ocaml/cic_proof_checking/cicPp.mli | 41 + helm/ocaml/cic_proof_checking/cicReduction.ml | 278 ++++ .../ocaml/cic_proof_checking/cicReduction.mli | 34 + .../cic_proof_checking/cicSubstitution.ml | 142 ++ .../cic_proof_checking/cicSubstitution.mli | 28 + .../cic_proof_checking/cicTypeChecker.ml | 1289 +++++++++++++++++ .../cic_proof_checking/cicTypeChecker.mli | 34 + helm/ocaml/getter/Makefile | 36 + helm/ocaml/getter/clientHTTP.ml | 60 + helm/ocaml/getter/clientHTTP.mli | 30 + helm/ocaml/getter/configuration.ml | 118 ++ helm/ocaml/getter/getter.ml | 63 + helm/ocaml/getter/getter.mli | 53 + helm/ocaml/pxp/Makefile | 36 + helm/ocaml/pxp/csc_pxp_reader.ml | 1011 +++++++++++++ helm/ocaml/pxp/pxpUriResolver.ml | 266 ++++ helm/ocaml/urimanager/Makefile | 36 + helm/ocaml/urimanager/uriManager.ml | 139 ++ helm/ocaml/urimanager/uriManager.mli | 51 + helm/ocaml/xml/Makefile | 36 + helm/ocaml/xml/xml.ml | 101 ++ helm/ocaml/xml/xml.mli | 60 + 60 files changed, 7450 insertions(+) create mode 100644 helm/ocaml/META.helm-cic create mode 100644 helm/ocaml/META.helm-cic_annotations create mode 100644 helm/ocaml/META.helm-cic_annotations_cache create mode 100644 helm/ocaml/META.helm-cic_cache create mode 100644 helm/ocaml/META.helm-cic_proof_checking create mode 100644 helm/ocaml/META.helm-getter create mode 100644 helm/ocaml/META.helm-pxp create mode 100644 helm/ocaml/META.helm-urimanager create mode 100644 helm/ocaml/META.helm-xml create mode 100644 helm/ocaml/cic/Makefile create mode 100644 helm/ocaml/cic/cic.ml create mode 100644 helm/ocaml/cic/cicParser.ml create mode 100644 helm/ocaml/cic/cicParser.mli create mode 100644 helm/ocaml/cic/cicParser2.ml create mode 100644 helm/ocaml/cic/cicParser2.mli create mode 100644 helm/ocaml/cic/cicParser3.ml create mode 100644 helm/ocaml/cic/cicParser3.mli create mode 100644 helm/ocaml/cic/deannotate.ml create mode 100644 helm/ocaml/cic_annotations/Makefile create mode 100644 helm/ocaml/cic_annotations/cicAnnotation2Xml.ml create mode 100644 helm/ocaml/cic_annotations/cicAnnotationHinter.ml create mode 100644 helm/ocaml/cic_annotations/cicAnnotationParser.ml create mode 100644 helm/ocaml/cic_annotations/cicAnnotationParser2.ml create mode 100644 helm/ocaml/cic_annotations/cicXPath.ml create mode 100644 helm/ocaml/cic_annotations_cache/Makefile create mode 100644 helm/ocaml/cic_annotations_cache/cicCache.ml create mode 100644 helm/ocaml/cic_annotations_cache/cicCache.mli create mode 100644 helm/ocaml/cic_cache/Makefile create mode 100644 helm/ocaml/cic_cache/cicCache.ml create mode 100644 helm/ocaml/cic_cache/cicCache.mli create mode 100644 helm/ocaml/cic_proof_checking/Makefile create mode 100644 helm/ocaml/cic_proof_checking/cicCooking.ml create mode 100644 helm/ocaml/cic_proof_checking/cicCooking.mli create mode 100644 helm/ocaml/cic_proof_checking/cicEnvironment.ml create mode 100644 helm/ocaml/cic_proof_checking/cicEnvironment.mli create mode 100644 helm/ocaml/cic_proof_checking/cicMiniReduction.ml create mode 100644 helm/ocaml/cic_proof_checking/cicMiniReduction.mli create mode 100644 helm/ocaml/cic_proof_checking/cicPp.ml create mode 100644 helm/ocaml/cic_proof_checking/cicPp.mli create mode 100644 helm/ocaml/cic_proof_checking/cicReduction.ml create mode 100644 helm/ocaml/cic_proof_checking/cicReduction.mli create mode 100644 helm/ocaml/cic_proof_checking/cicSubstitution.ml create mode 100644 helm/ocaml/cic_proof_checking/cicSubstitution.mli create mode 100644 helm/ocaml/cic_proof_checking/cicTypeChecker.ml create mode 100644 helm/ocaml/cic_proof_checking/cicTypeChecker.mli create mode 100644 helm/ocaml/getter/Makefile create mode 100644 helm/ocaml/getter/clientHTTP.ml create mode 100644 helm/ocaml/getter/clientHTTP.mli create mode 100644 helm/ocaml/getter/configuration.ml create mode 100644 helm/ocaml/getter/getter.ml create mode 100644 helm/ocaml/getter/getter.mli create mode 100644 helm/ocaml/pxp/Makefile create mode 100644 helm/ocaml/pxp/csc_pxp_reader.ml create mode 100644 helm/ocaml/pxp/pxpUriResolver.ml create mode 100644 helm/ocaml/urimanager/Makefile create mode 100644 helm/ocaml/urimanager/uriManager.ml create mode 100644 helm/ocaml/urimanager/uriManager.mli create mode 100644 helm/ocaml/xml/Makefile create mode 100644 helm/ocaml/xml/xml.ml create mode 100644 helm/ocaml/xml/xml.mli diff --git a/helm/ocaml/META.helm-cic b/helm/ocaml/META.helm-cic new file mode 100644 index 000000000..119b9a406 --- /dev/null +++ b/helm/ocaml/META.helm-cic @@ -0,0 +1,6 @@ +requires="helm-urimanager helm-pxp" +version="0.0.1" +archive(byte)="cic.cmo deannotate.cmo cicParser3.cmo cicParser2.cmo cicParser.cmo" +archive(native)="cic.cmx deannotate.cmx cicParser3.cmx cicParser2.cmx cicParser.cmx" +linkopts="" +directory="/home/sacerdot/miohelm/ocaml/helm/cic" diff --git a/helm/ocaml/META.helm-cic_annotations b/helm/ocaml/META.helm-cic_annotations new file mode 100644 index 000000000..64cc7956a --- /dev/null +++ b/helm/ocaml/META.helm-cic_annotations @@ -0,0 +1,6 @@ +requires="helm-cic helm-xml lablgtk" +version="0.0.1" +archive(byte)="cicAnnotation2Xml.cmo cicAnnotationHinter.cmo cicAnnotationParser2.cmo cicAnnotationParser.cmo cicXPath.cmo" +archive(native)="cicAnnotation2Xml.cmx cicAnnotationHinter.cmx cicAnnotationParser2.cmx cicAnnotationParser.cmx cicXPath.cmx" +linkopts="" +directory="/home/sacerdot/miohelm/ocaml/helm/cic_annotations" diff --git a/helm/ocaml/META.helm-cic_annotations_cache b/helm/ocaml/META.helm-cic_annotations_cache new file mode 100644 index 000000000..88ebb07f7 --- /dev/null +++ b/helm/ocaml/META.helm-cic_annotations_cache @@ -0,0 +1,6 @@ +requires="helm-cic_annotations" +version="0.0.1" +archive(byte)="cicCache.cmo" +archive(native)="cicCache.cmx" +linkopts="" +directory="/home/sacerdot/miohelm/ocaml/helm/cic_annotations_cache" diff --git a/helm/ocaml/META.helm-cic_cache b/helm/ocaml/META.helm-cic_cache new file mode 100644 index 000000000..d0401a489 --- /dev/null +++ b/helm/ocaml/META.helm-cic_cache @@ -0,0 +1,6 @@ +requires="helm-cic" +version="0.0.1" +archive(byte)="cicCache.cmo" +archive(native)="cicCache.cmx" +linkopts="" +directory="/home/sacerdot/miohelm/ocaml/helm/cic_cache" diff --git a/helm/ocaml/META.helm-cic_proof_checking b/helm/ocaml/META.helm-cic_proof_checking new file mode 100644 index 000000000..858f59e6e --- /dev/null +++ b/helm/ocaml/META.helm-cic_proof_checking @@ -0,0 +1,8 @@ +requires="helm-cic" +version="0.0.1" +archive(byte)="cicSubstitution.cmo cicEnvironment.cmo cicPp.cmo cicReduction.cmo cicTypeChecker.cmo cicCooking.cmo" +archive(native)="cicSubstitution.cmx cicEnvironment.cmx cicPp.cmx cicReduction.cmx cicTypeChecker.cmx cicCooking.cmx" +archive(byte,miniReduction)="cicSubstitution.cmo cicMiniReduction.cmo" +archive(native,miniReduction)="cicSubstitution.cmx cicMiniReduction.cmx" +linkopts="" +directory="/home/sacerdot/miohelm/ocaml/helm/cic_proof_checking" diff --git a/helm/ocaml/META.helm-getter b/helm/ocaml/META.helm-getter new file mode 100644 index 000000000..90e330e90 --- /dev/null +++ b/helm/ocaml/META.helm-getter @@ -0,0 +1,6 @@ +requires="helm-urimanager pxp netclient" +version="0.0.1" +archive(byte)="configuration.cmo clientHTTP.cmo getter.cmo" +archive(native)="configuration.cmx clientHTTP.cmx getter.cmx" +linkopts="" +directory="/home/sacerdot/miohelm/ocaml/helm/getter" diff --git a/helm/ocaml/META.helm-pxp b/helm/ocaml/META.helm-pxp new file mode 100644 index 000000000..1a5b02463 --- /dev/null +++ b/helm/ocaml/META.helm-pxp @@ -0,0 +1,6 @@ +requires="helm-getter" +version="0.0.1" +archive(byte)="csc_pxp_reader.cmo pxpUriResolver.cmo" +archive(native)="csc_pxp_reader.cmx pxpUriResolver.cmx" +linkopts="" +directory="/home/sacerdot/miohelm/ocaml/helm/pxp" diff --git a/helm/ocaml/META.helm-urimanager b/helm/ocaml/META.helm-urimanager new file mode 100644 index 000000000..281b1260d --- /dev/null +++ b/helm/ocaml/META.helm-urimanager @@ -0,0 +1,6 @@ +requires="str" +version="0.0.1" +archive(byte)="uriManager.cmo" +archive(native)="uriManager.cmx" +linkopts="" +directory="/home/sacerdot/miohelm/ocaml/helm/urimanager" diff --git a/helm/ocaml/META.helm-xml b/helm/ocaml/META.helm-xml new file mode 100644 index 000000000..616b5f186 --- /dev/null +++ b/helm/ocaml/META.helm-xml @@ -0,0 +1,6 @@ +requires="" +version="0.0.1" +archive(byte)="xml.cmo" +archive(native)="xml.cmx" +linkopts="" +directory="/home/sacerdot/miohelm/ocaml/helm/xml" diff --git a/helm/ocaml/cic/Makefile b/helm/ocaml/cic/Makefile new file mode 100644 index 000000000..36e718dc6 --- /dev/null +++ b/helm/ocaml/cic/Makefile @@ -0,0 +1,37 @@ +BIN_DIR = /usr/local/bin +REQUIRES = helm-urimanager helm-pxp +PREDICATES = +OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" +OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) +OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLDEP = ocamldep + +all: cic.cmo deannotate.cmo cicParser3.cmo cicParser2.cmo cicParser.cmo +opt: cic.cmx deannotate.cmx cicParser3.cmx cicParser2.cmx cicParser.cmx + +DEPOBJS = cic.ml deannotate.mli deannotate.ml cicParser3.mli cicParser3.ml \ + cicParser2.mli cicParser2.ml cicParser.mli cicParser.ml + +depend: + $(OCAMLDEP) $(DEPOBJS) > .depend + +.SUFFIXES: .ml .mli .cmo .cmi .cmx +.ml.cmo: + $(OCAMLC) -c $< +.mli.cmi: + $(OCAMLC) -c $< +.ml.cmx: + $(OCAMLOPT) -c $< + +clean: + rm -f *.cm[iox] + +install: + #cp + +uninstall: + #rm -f + +.PHONY: install uninstall clean + +include .depend diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml new file mode 100644 index 000000000..8c08b0075 --- /dev/null +++ b/helm/ocaml/cic/cic.ml @@ -0,0 +1,162 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 14/06/2000 *) +(* *) +(* This module defines the internal representation of the objects (variables, *) +(* blocks of (co)inductive definitions and constants) and the terms of cic *) +(* *) +(******************************************************************************) + +(* STUFF TO MANAGE IDENTIFIERS *) +type id = string (* the abstract type of the (annotated) node identifiers *) +type anntarget = + Object of annobj + | Term of annterm + +(* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *) +and sort = + Prop + | Set + | Type +and name = + Name of string + | Anonimous +and term = + Rel of int (* DeBrujin index *) + | Var of UriManager.uri (* uri *) + | Meta of int (* numeric id *) + | Sort of sort (* sort *) + | Implicit (* *) + | Cast of term * term (* value, type *) + | Prod of name * term * term (* binder, source, target *) + | Lambda of name * term * term (* binder, source, target *) + | LetIn of name * term * term (* binder, term, target *) + | Appl of term list (* arguments *) + | Const of UriManager.uri * int (* uri, number of cookings*) + | Abst of UriManager.uri (* uri *) + | MutInd of UriManager.uri * int * int (* uri, cookingsno, typeno*) + | MutConstruct of UriManager.uri * int * (* uri, cookingsno, *) + int * int (* typeno, consno *) + (*CSC: serve cookingsno?*) + | MutCase of UriManager.uri * int * (* ind. uri, cookingsno, *) + int * (* ind. typeno, *) + term * term * (* outtype, ind. term *) + term list (* patterns *) + | Fix of int * inductiveFun list (* funno, functions *) + | CoFix of int * coInductiveFun list (* funno, functions *) +and obj = + Definition of string * term * term * (* id, value, type, *) + (int * UriManager.uri list) list (* parameters *) + | Axiom of string * term * + (int * UriManager.uri list) list (* id, type, parameters *) + | Variable of string * term option * term (* name, body, type *) + | CurrentProof of string * (int * term) list * (* name, conjectures, *) + term * term (* value, type *) + | InductiveDefinition of inductiveType list * (* inductive types, *) + (int * UriManager.uri list) list * int (* parameters, n ind. pars *) +and inductiveType = + string * bool * term * (* typename, inductive, arity *) + constructor list (* constructors *) +and constructor = + string * term * bool list option ref (* id, type, really recursive *) +and inductiveFun = + string * int * term * term (* name, ind. index, type, body *) +and coInductiveFun = + string * term * term (* name, type, body *) + +and annterm = + ARel of id * annotation option ref * + int * string option (* DeBrujin index, binder *) + | AVar of id * annotation option ref * + UriManager.uri (* uri *) + | AMeta of id * annotation option ref * int (* numeric id *) + | ASort of id * annotation option ref * sort (* sort *) + | AImplicit of id * annotation option ref (* *) + | ACast of id * annotation option ref * + annterm * annterm (* value, type *) + | AProd of id * annotation option ref * + name * annterm * annterm (* binder, source, target *) + | ALambda of id * annotation option ref * + name * annterm * annterm (* binder, source, target *) + | ALetIn of id * annotation option ref * + name * annterm * annterm (* binder, term, target *) + | AAppl of id * annotation option ref * + annterm list (* arguments *) + | AConst of id * annotation option ref * + UriManager.uri * int (* uri, number of cookings*) + | AAbst of id * annotation option ref * + UriManager.uri (* uri *) + | AMutInd of id * annotation option ref * + UriManager.uri * int * int (* uri, cookingsno, typeno*) + | AMutConstruct of id * annotation option ref * + UriManager.uri * int * (* uri, cookingsno, *) + int * int (* typeno, consno *) + (*CSC: serve cookingsno?*) + | AMutCase of id * annotation option ref * + UriManager.uri * int * (* ind. uri, cookingsno *) + int * (* ind. typeno, *) + annterm * annterm * (* outtype, ind. term *) + annterm list (* patterns *) + | AFix of id * annotation option ref * + int * anninductiveFun list (* funno, functions *) + | ACoFix of id * annotation option ref * + int * anncoInductiveFun list (* funno, functions *) +and annobj = + ADefinition of id * annotation option ref * + string * (* id, *) + annterm * annterm * (* value, type, *) + (int * UriManager.uri list) list exactness (* parameters *) + | AAxiom of id * annotation option ref * + string * annterm * (* id, type *) + (int * UriManager.uri list) list (* parameters *) + | AVariable of id * annotation option ref * + string * annterm option * annterm (* name, body, type *) + | ACurrentProof of id * annotation option ref * + string * (int * annterm) list * (* name, conjectures, *) + annterm * annterm (* value, type *) + | AInductiveDefinition of id * + annotation option ref * anninductiveType list * (* inductive types , *) + (int * UriManager.uri list) list * int (* parameters,n ind. pars*) +and anninductiveType = + string * bool * annterm * (* typename, inductive, arity *) + annconstructor list (* constructors *) +and annconstructor = + string * annterm * bool list option ref (* id, type, really recursive *) +and anninductiveFun = + string * int * annterm * annterm (* name, ind. index, type, body *) +and anncoInductiveFun = + string * annterm * annterm (* name, type, body *) +and annotation = + string +and 'a exactness = + Possible of 'a (* an approximation to something *) + | Actual of 'a (* something *) +;; diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml new file mode 100644 index 000000000..bf75243ec --- /dev/null +++ b/helm/ocaml/cic/cicParser.ml @@ -0,0 +1,95 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This is the main (top level) module of a parser for cic objects from xml *) +(* files to the internal representation. It uses the modules cicParser2 *) +(* (objects level) and cicParser3 (terms level) *) +(* *) +(******************************************************************************) + +exception Warnings;; + +class warner = + object + method warn w = + print_endline ("WARNING: " ^ w) ; + (raise Warnings : unit) + end +;; + +exception EmptyUri;; + +(* given an uri u it returns the list of tokens of the base uri of u *) +(* e.g.: token_of_uri "cic:/a/b/c/d.xml" returns ["a" ; "b" ; "c"] *) +let tokens_of_uri uri = + let uri' = UriManager.string_of_uri uri in + let rec chop_list = + function + [] -> raise EmptyUri + | he::[fn] -> [he] + | he::tl -> he::(chop_list tl) + in + let trimmed_uri = Str.replace_first (Str.regexp "cic:") "" uri' in + let list_of_tokens = Str.split (Str.regexp "/") trimmed_uri in + chop_list list_of_tokens +;; + +(* given the filename of an xml file of a cic object it returns its internal *) +(* representation. process_annotations is true if the annotations do really *) +(* matter *) +let term_of_xml filename uri process_annotations = + let module Y = Pxp_yacc in + try + let d = + (* sets the current base uri to resolve relative URIs *) + CicParser3.current_sp := tokens_of_uri uri ; + CicParser3.current_uri := uri ; + CicParser3.process_annotations := process_annotations ; + CicParser3.ids_to_targets := + if process_annotations then Some (Hashtbl.create 500) else None ; + let config = {Y.default_config with Y.warner = new warner} in + Y.parse_document_entity config +(*PXP (Y.ExtID (Pxp_types.System filename, + new Pxp_reader.resolve_as_file ~url_of_id ())) +*) (PxpUriResolver.from_file filename) + CicParser3.domspec + in + let ids_to_targets = !CicParser3.ids_to_targets in + let res = (CicParser2.get_term d#root, ids_to_targets) in + CicParser3.ids_to_targets := None ; (* let's help the GC *) + res + with + e -> + print_endline ("Filename: " ^ filename ^ "\nException: ") ; + print_endline (Pxp_types.string_of_exn e) ; + raise e +;; diff --git a/helm/ocaml/cic/cicParser.mli b/helm/ocaml/cic/cicParser.mli new file mode 100644 index 000000000..0078f6f33 --- /dev/null +++ b/helm/ocaml/cic/cicParser.mli @@ -0,0 +1,44 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 22/03/2000 *) +(* *) +(* This is the main (top level) module of a parser for cic objects from xml *) +(* files to the internal representation. It uses the modules cicParser2 *) +(* (objects level) and cicParser3 (terms level) *) +(* *) +(******************************************************************************) + +(* given the filename of an xml file of a cic object and it's uri, it returns *) +(* its internal annotated representation. The boolean is set to true if the *) +(* annotations do really matter *) +val term_of_xml : + string -> UriManager.uri -> bool -> + Cic.annobj * (Cic.id, Cic.anntarget) Hashtbl.t option diff --git a/helm/ocaml/cic/cicParser2.ml b/helm/ocaml/cic/cicParser2.ml new file mode 100644 index 000000000..562f79bba --- /dev/null +++ b/helm/ocaml/cic/cicParser2.ml @@ -0,0 +1,289 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This module is the objects level of a parser for cic objects from xml *) +(* files to the internal representation. It uses the module cicParser3 *) +(* cicParser3 (terms level) and it is used only through cicParser2 (top *) +(* level). *) +(* *) +(******************************************************************************) + +exception IllFormedXml of int;; +exception NotImplemented;; + +(* Utility functions that transform a Pxp attribute into something useful *) + +(* mk_absolute_uris "n1: v1 ... vn n2 : u1 ... un ...." *) +(* returns [(n1,[absolute_uri_for_v1 ; ... ; absolute_uri_for_vn]) ; (n2,...) *) +let mk_absolute_uris s = + let l = (Str.split (Str.regexp ":") s) in + let absolute_of_relative n v = + let module P3 = CicParser3 in + let rec mkburi = + function + (0,_) -> "/" + | (n,he::tl) when n > 0 -> + "/" ^ he ^ mkburi (n - 1, tl) + | _ -> raise (IllFormedXml 12) + in + let m = List.length !P3.current_sp - (int_of_string n) in + let buri = mkburi (m, !P3.current_sp) in + UriManager.uri_of_string ("cic:" ^ buri ^ v ^ ".var") + in + let rec absolutize = + function + [] -> [] + | [no ; vs] -> + let vars = (Str.split (Str.regexp " ") vs) in + [(int_of_string no, List.map (absolute_of_relative no) vars)] + | no::vs::tl -> + let vars = (Str.split (Str.regexp " ") vs) in + let rec add_prefix = + function + [no2] -> ([], no2) + | he::tl -> + let (pvars, no2) = add_prefix tl in + ((absolute_of_relative no he)::pvars, no2) + | _ -> raise (IllFormedXml 11) + in + let (pvars, no2) = add_prefix vars in + (int_of_string no, pvars)::(absolutize (no2::tl)) + | _ -> raise (IllFormedXml 10) + in + (* last parameter must be applied first *) + absolutize l +;; + +let option_uri_list_of_attr a1 a2 = + let module T = Pxp_types in + let parameters = + match a1 with + T.Value s -> mk_absolute_uris s + | _ -> raise (IllFormedXml 0) + in + match a2 with + T.Value "POSSIBLE" -> Cic.Possible parameters + | T.Implied_value -> Cic.Actual parameters + | _ -> raise (IllFormedXml 0) +;; + +let uri_list_of_attr a = + let module T = Pxp_types in + match a with + T.Value s -> mk_absolute_uris s + | _ -> raise (IllFormedXml 0) +;; + +let string_of_attr a = + let module T = Pxp_types in + match a with + T.Value s -> s + | _ -> raise (IllFormedXml 0) +;; + +let int_of_attr a = + int_of_string (string_of_attr a) +;; + +let bool_of_attr a = + bool_of_string (string_of_attr a) +;; + +(* Other utility functions *) + +let get_content n = + match n#sub_nodes with + [ t ] -> t + | _ -> raise (IllFormedXml 1) +;; + +let register_id id node = + if !CicParser3.process_annotations then + match !CicParser3.ids_to_targets with + None -> assert false + | Some ids_to_targets -> + Hashtbl.add ids_to_targets id (Cic.Object node) +;; + +(* Functions that, given the list of sons of a node of the cic dom (objects *) +(* level), retrieve the internal representation associated to the node. *) +(* Everytime a cic term subtree is found, it is translated to the internal *) +(* representation using the method to_cic_term defined in cicParser3. *) +(* Each function raise IllFormedXml if something goes wrong, but this should *) +(* be impossible due to the presence of the dtd *) +(* The functions should really be obvious looking at their name and the cic *) +(* dtd *) + +(* called when a CurrentProof is found *) +let get_conjs_value_type l = + let rec rget (c, v, t) l = + let module D = Pxp_document in + match l with + [] -> (c, v, t) + | conj::tl when conj#node_type = D.T_element "Conjecture" -> + let no = int_of_attr (conj#attribute "no") + and typ = (get_content conj)#extension#to_cic_term in + rget ((no, typ)::c, v, t) tl + | value::tl when value#node_type = D.T_element "body" -> + let v' = (get_content value)#extension#to_cic_term in + (match v with + None -> rget (c, Some v', t) tl + | _ -> raise (IllFormedXml 2) + ) + | typ::tl when typ#node_type = D.T_element "type" -> + let t' = (get_content typ)#extension#to_cic_term in + (match t with + None -> rget (c, v, Some t') tl + | _ -> raise (IllFormedXml 3) + ) + | _ -> raise (IllFormedXml 4) + in + match rget ([], None, None) l with + (c, Some v, Some t) -> (c, v, t) + | _ -> raise (IllFormedXml 5) +;; + +(* used only by get_inductive_types; called one time for each inductive *) +(* definitions in a block of inductive definitions *) +let get_names_arity_constructors l = + let rec rget (a,c) l = + let module D = Pxp_document in + match l with + [] -> (a, c) + | arity::tl when arity#node_type = D.T_element "arity" -> + let a' = (get_content arity)#extension#to_cic_term in + rget (Some a',c) tl + | con::tl when con#node_type = D.T_element "Constructor" -> + let id = string_of_attr (con#attribute "name") + and ty = (get_content con)#extension#to_cic_term in + rget (a,(id,ty,ref None)::c) tl + | _ -> raise (IllFormedXml 9) + in + match rget (None,[]) l with + (Some a, c) -> (a, List.rev c) + | _ -> raise (IllFormedXml 8) +;; + +(* called when an InductiveDefinition is found *) +let rec get_inductive_types = + function + [] -> [] + | he::tl -> + let tyname = string_of_attr (he#attribute "name") + and inductive = bool_of_attr (he#attribute "inductive") + and (arity,cons) = + get_names_arity_constructors (he#sub_nodes) + in + (tyname,inductive,arity,cons)::(get_inductive_types tl) (*CSC 0 a caso *) +;; + +(* This is the main function and also the only one used directly from *) +(* cicParser. Given the root of the dom tree, it returns the internal *) +(* representation of the cic object described in the tree *) +(* It uses the previous functions and the to_cic_term method defined *) +(* in cicParser3 (used for subtrees that encode cic terms) *) +let rec get_term n = + let module D = Pxp_document in + let module C = Cic in + let ntype = n # node_type in + match ntype with + D.T_element "Definition" -> + let id = string_of_attr (n # attribute "name") + and params = + option_uri_list_of_attr (n#attribute "params") (n#attribute "paramMode") + and (value, typ) = + let sons = n#sub_nodes in + match sons with + [v ; t] when + v#node_type = D.T_element "body" && + t#node_type = D.T_element "type" -> + let v' = get_content v + and t' = get_content t in + (v'#extension#to_cic_term, t'#extension#to_cic_term) + | _ -> raise (IllFormedXml 6) + and xid = string_of_attr (n#attribute "id") in + let res = C.ADefinition (xid, ref None, id, value, typ, params) in + register_id xid res ; + res + | D.T_element "Axiom" -> + let id = string_of_attr (n # attribute "name") + and params = uri_list_of_attr (n # attribute "params") + and typ = + (get_content (get_content n))#extension#to_cic_term + and xid = string_of_attr (n#attribute "id") in + let res = C.AAxiom (xid, ref None, id, typ, params) in + register_id xid res ; + res + | D.T_element "CurrentProof" -> + let name = string_of_attr (n#attribute "name") + and xid = string_of_attr (n#attribute "id") in + let sons = n#sub_nodes in + let (conjs, value, typ) = get_conjs_value_type sons in + let res = C.ACurrentProof (xid, ref None, name, conjs, value, typ) in + register_id xid res ; + res + | D.T_element "InductiveDefinition" -> + let sons = n#sub_nodes + and xid = string_of_attr (n#attribute "id") in + let inductiveTypes = get_inductive_types sons + and params = uri_list_of_attr (n#attribute "params") + and nparams = int_of_attr (n#attribute "noParams") in + let res = + C.AInductiveDefinition (xid, ref None, inductiveTypes, params, nparams) + in + register_id xid res ; + res + | D.T_element "Variable" -> + let name = string_of_attr (n#attribute "name") + and xid = string_of_attr (n#attribute "id") + and (body, typ) = + let sons = n#sub_nodes in + match sons with + [b ; t] when + b#node_type = D.T_element "body" && + t#node_type = D.T_element "type" -> + let b' = get_content b + and t' = get_content t in + (Some (b'#extension#to_cic_term), t'#extension#to_cic_term) + | [t] when t#node_type = D.T_element "type" -> + let t' = get_content t in + (None, t'#extension#to_cic_term) + | _ -> raise (IllFormedXml 6) + in + let res = C.AVariable (xid,ref None,name,body,typ) in + register_id xid res ; + res + | D.T_element _ + | D.T_data + | _ -> + raise (IllFormedXml 7) +;; diff --git a/helm/ocaml/cic/cicParser2.mli b/helm/ocaml/cic/cicParser2.mli new file mode 100644 index 000000000..be0a00054 --- /dev/null +++ b/helm/ocaml/cic/cicParser2.mli @@ -0,0 +1,57 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This module is the objects level of a parser for cic objects from xml *) +(* files to the internal representation. It uses the module cicParser3 *) +(* cicParser3 (terms level) and it is used only through cicParser2 (top *) +(* level). *) +(* *) +(******************************************************************************) + +exception IllFormedXml of int +exception NotImplemented + +(* This is the main function and also the only one used directly from *) +(* cicParser. Given the root of the dom tree, it returns the internal *) +(* representation of the cic object described in the tree *) +(* It uses the previous functions and the to_cic_term method defined *) +(* in cicParser3 (used for subtrees that encode cic terms) *) +val get_term : + < attribute : string -> Pxp_types.att_value; + node_type : Pxp_document.node_type; + sub_nodes : < attribute : string -> Pxp_types.att_value; + node_type : Pxp_document.node_type; + sub_nodes : CicParser3.cic_term Pxp_document.node list; + .. > + list; + .. > -> + Cic.annobj diff --git a/helm/ocaml/cic/cicParser3.ml b/helm/ocaml/cic/cicParser3.ml new file mode 100644 index 000000000..ff356b13e --- /dev/null +++ b/helm/ocaml/cic/cicParser3.ml @@ -0,0 +1,565 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This module is the terms level of a parser for cic objects from xml *) +(* files to the internal representation. It is used by the module cicParser2 *) +(* (objects level). It defines an extension of the standard dom using the *) +(* object-oriented extension machinery of markup: an object with a method *) +(* to_cic_term that returns the internal representation of the subtree is *) +(* added to each node of the dom tree *) +(* *) +(******************************************************************************) + +exception IllFormedXml of int;; + +(* The hashtable from the current identifiers to the object or the terms *) +let ids_to_targets = ref None;; + +(* The list of tokens of the current section path. *) +(* Used to resolve relative URIs *) +let current_sp = ref [];; + +(* The uri of the object been parsed *) +let current_uri = ref (UriManager.uri_of_string "cic:/.xml");; + +(* True if annotation really matter *) +let process_annotations = ref false;; + +(* Utility functions to map a markup attribute to something useful *) + +let cic_attr_of_xml_attr = + function + Pxp_types.Value s -> Cic.Name s + | Pxp_types.Implied_value -> Cic.Anonimous + | _ -> raise (IllFormedXml 1) + +let cic_sort_of_xml_attr = + function + Pxp_types.Value "Prop" -> Cic.Prop + | Pxp_types.Value "Set" -> Cic.Set + | Pxp_types.Value "Type" -> Cic.Type + | _ -> raise (IllFormedXml 2) + +let int_of_xml_attr = + function + Pxp_types.Value n -> int_of_string n + | _ -> raise (IllFormedXml 3) + +let uri_of_xml_attr = + function + Pxp_types.Value s -> UriManager.uri_of_string s + | _ -> raise (IllFormedXml 4) + +let string_of_xml_attr = + function + Pxp_types.Value s -> s + | _ -> raise (IllFormedXml 5) + +let binder_of_xml_attr = + function + Pxp_types.Value s -> if !process_annotations then Some s else None + | _ -> raise (IllFormedXml 17) +;; + +let register_id id node = + if !process_annotations then + match !ids_to_targets with + None -> assert false + | Some ids_to_targets -> + Hashtbl.add ids_to_targets id (Cic.Term node) +;; + +(* the "interface" of the class linked to each node of the dom tree *) + +class virtual cic_term = + object (self) + + (* fields and methods ever required by markup *) + val mutable node = (None : cic_term Pxp_document.node option) + + method clone = {< >} + method node = + match node with + None -> + assert false + | Some n -> n + method set_node n = + node <- Some n + + (* a method that returns the internal representation of the tree (term) *) + (* rooted in this node *) + method virtual to_cic_term : Cic.annterm + end +;; + +(* the class of the objects linked to nodes that are not roots of cic terms *) +class eltype_not_of_cic = + object (self) + + inherit cic_term + + method to_cic_term = raise (IllFormedXml 6) + end +;; + +(* the class of the objects linked to nodes whose content is a cic term *) +(* (syntactic sugar xml entities) e.g. ... *) +class eltype_transparent = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + match n#sub_nodes with + [ t ] -> t#extension#to_cic_term + | _ -> raise (IllFormedXml 7) + end +;; + +(* A class for each cic node type *) + +class eltype_fix = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let nofun = int_of_xml_attr (n#attribute "noFun") + and id = string_of_xml_attr (n#attribute "id") + and functions = + let sons = n#sub_nodes in + List.map + (function + f when f#node_type = Pxp_document.T_element "FixFunction" -> + let name = string_of_xml_attr (f#attribute "name") + and recindex = int_of_xml_attr (f#attribute "recIndex") + and (ty, body) = + match f#sub_nodes with + [t ; b] when + t#node_type = Pxp_document.T_element "type" && + b#node_type = Pxp_document.T_element "body" -> + (t#extension#to_cic_term, b#extension#to_cic_term) + | _ -> raise (IllFormedXml 14) + in + (name, recindex, ty, body) + | _ -> raise (IllFormedXml 13) + ) sons + in + let res = Cic.AFix (id, ref None, nofun, functions) in + register_id id res ; + res + end +;; + +class eltype_cofix = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let nofun = int_of_xml_attr (n#attribute "noFun") + and id = string_of_xml_attr (n#attribute "id") + and functions = + let sons = n#sub_nodes in + List.map + (function + f when f#node_type = Pxp_document.T_element "CofixFunction" -> + let name = string_of_xml_attr (f#attribute "name") + and (ty, body) = + match f#sub_nodes with + [t ; b] when + t#node_type = Pxp_document.T_element "type" && + b#node_type = Pxp_document.T_element "body" -> + (t#extension#to_cic_term, b#extension#to_cic_term) + | _ -> raise (IllFormedXml 16) + in + (name, ty, body) + | _ -> raise (IllFormedXml 15) + ) sons + in + let res = Cic.ACoFix (id, ref None, nofun, functions) in + register_id id res ; + res + end +;; + +class eltype_implicit = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let id = string_of_xml_attr (n#attribute "id") in + let res = Cic.AImplicit (id, ref None) in + register_id id res ; + res + end +;; + +class eltype_rel = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let value = int_of_xml_attr (n#attribute "value") + and binder = binder_of_xml_attr (n#attribute "binder") + and id = string_of_xml_attr (n#attribute "id") in + let res = Cic.ARel (id,ref None,value,binder) in + register_id id res ; + res + end +;; + +class eltype_meta = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let value = int_of_xml_attr (n#attribute "no") + and id = string_of_xml_attr (n#attribute "id") in + let res = Cic.AMeta (id,ref None,value) in + register_id id res ; + res + end +;; + +class eltype_var = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let name = string_of_xml_attr (n#attribute "relUri") + and xid = string_of_xml_attr (n#attribute "id") in + match Str.split (Str.regexp ",") name with + [index; id] -> + let get_prefix n = + let rec aux = + function + (0,_) -> "/" + | (n,he::tl) when n > 0 -> "/" ^ he ^ aux (n - 1, tl) + | _ -> raise (IllFormedXml 19) + in + aux (List.length !current_sp - n,!current_sp) + in + let res = + Cic.AVar + (xid,ref None, + (UriManager.uri_of_string + ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var")) + ) + in + register_id id res ; + res + | _ -> raise (IllFormedXml 18) + end +;; + +class eltype_apply = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let children = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + if List.length children < 2 then raise (IllFormedXml 8) + else + let res = + Cic.AAppl + (id,ref None,List.map (fun x -> x#extension#to_cic_term) children) + in + register_id id res ; + res + end +;; + +class eltype_cast = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let sons = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + match sons with + [te ; ty] when + te#node_type = Pxp_document.T_element "term" && + ty#node_type = Pxp_document.T_element "type" -> + let term = te#extension#to_cic_term + and typ = ty#extension#to_cic_term in + let res = Cic.ACast (id,ref None,term,typ) in + register_id id res ; + res + | _ -> raise (IllFormedXml 9) + end +;; + +class eltype_sort = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let sort = cic_sort_of_xml_attr (n#attribute "value") + and id = string_of_xml_attr (n#attribute "id") in + let res = Cic.ASort (id,ref None,sort) in + register_id id res ; + res + end +;; + +class eltype_abst = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let value = uri_of_xml_attr (n#attribute "uri") + and id = string_of_xml_attr (n#attribute "id") in + let res = Cic.AAbst (id,ref None,value) in + register_id id res ; + res + end +;; + +class eltype_const = + object (self) + + inherit cic_term + + method to_cic_term = + let module U = UriManager in + let n = self#node in + let value = uri_of_xml_attr (n#attribute "uri") + and id = string_of_xml_attr (n#attribute "id") in + let res = + Cic.AConst (id,ref None,value, U.relative_depth !current_uri value 0) + in + register_id id res ; + res + end +;; + +class eltype_mutind = + object (self) + + inherit cic_term + + method to_cic_term = + let module U = UriManager in + let n = self#node in + let name = uri_of_xml_attr (n#attribute "uri") + and noType = int_of_xml_attr (n#attribute "noType") + and id = string_of_xml_attr (n#attribute "id") in + let res = + Cic.AMutInd + (id,ref None,name, U.relative_depth !current_uri name 0, noType) + in + register_id id res ; + res + end +;; + +class eltype_mutconstruct = + object (self) + + inherit cic_term + + method to_cic_term = + let module U = UriManager in + let n = self#node in + let name = uri_of_xml_attr (n#attribute "uri") + and noType = int_of_xml_attr (n#attribute "noType") + and noConstr = int_of_xml_attr (n#attribute "noConstr") + and id = string_of_xml_attr (n#attribute "id") in + let res = + Cic.AMutConstruct + (id, ref None, name, U.relative_depth !current_uri name 0, + noType, noConstr) + in + register_id id res ; + res + end +;; + +class eltype_prod = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let sons = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + match sons with + [s ; t] when + s#node_type = Pxp_document.T_element "source" && + t#node_type = Pxp_document.T_element "target" -> + let name = cic_attr_of_xml_attr (t#attribute "binder") + and source = s#extension#to_cic_term + and target = t#extension#to_cic_term in + let res = Cic.AProd (id,ref None,name,source,target) in + register_id id res ; + res + | _ -> raise (IllFormedXml 10) + end +;; + +class eltype_mutcase = + object (self) + + inherit cic_term + + method to_cic_term = + let module U = UriManager in + let n = self#node in + let sons = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + match sons with + ty::te::patterns when + ty#node_type = Pxp_document.T_element "patternsType" && + te#node_type = Pxp_document.T_element "inductiveTerm" -> + let ci = uri_of_xml_attr (n#attribute "uriType") + and typeno = int_of_xml_attr (n#attribute "noType") + and inductiveType = ty#extension#to_cic_term + and inductiveTerm = te#extension#to_cic_term + and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns + in + let res = + Cic.AMutCase (id,ref None,ci,U.relative_depth !current_uri ci 0, + typeno,inductiveType,inductiveTerm,lpattern) + in + register_id id res ; + res + | _ -> raise (IllFormedXml 11) + end +;; + +class eltype_lambda = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let sons = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + match sons with + [s ; t] when + s#node_type = Pxp_document.T_element "source" && + t#node_type = Pxp_document.T_element "target" -> + let name = cic_attr_of_xml_attr (t#attribute "binder") + and source = s#extension#to_cic_term + and target = t#extension#to_cic_term in + let res = Cic.ALambda (id,ref None,name,source,target) in + register_id id res ; + res + | _ -> raise (IllFormedXml 12) + end +;; + +class eltype_letin = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let sons = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + match sons with + [s ; t] when + s#node_type = Pxp_document.T_element "term" && + t#node_type = Pxp_document.T_element "letintarget" -> + let name = cic_attr_of_xml_attr (t#attribute "binder") + and source = s#extension#to_cic_term + and target = t#extension#to_cic_term in + let res = Cic.ALetIn (id,ref None,name,source,target) in + register_id id res ; + res + | _ -> raise (IllFormedXml 12) + end +;; + +(* The definition of domspec, an hashtable that maps each node type to the *) +(* object that must be linked to it. Used by markup. *) + +let domspec = + let module D = Pxp_document in + D.make_spec_from_alist + ~data_exemplar: (new D.data_impl (new eltype_not_of_cic)) + ~default_element_exemplar: (new D.element_impl (new eltype_not_of_cic)) + ~element_alist: + [ "REL", (new D.element_impl (new eltype_rel)) ; + "VAR", (new D.element_impl (new eltype_var)) ; + "META", (new D.element_impl (new eltype_meta)) ; + "SORT", (new D.element_impl (new eltype_sort)) ; + "IMPLICIT", (new D.element_impl (new eltype_implicit)) ; + "CAST", (new D.element_impl (new eltype_cast)) ; + "PROD", (new D.element_impl (new eltype_prod)) ; + "LAMBDA", (new D.element_impl (new eltype_lambda)) ; + "LETIN", (new D.element_impl (new eltype_letin)) ; + "APPLY", (new D.element_impl (new eltype_apply)) ; + "CONST", (new D.element_impl (new eltype_const)) ; + "ABST", (new D.element_impl (new eltype_abst)) ; + "MUTIND", (new D.element_impl (new eltype_mutind)) ; + "MUTCONSTRUCT", (new D.element_impl (new eltype_mutconstruct)) ; + "MUTCASE", (new D.element_impl (new eltype_mutcase)) ; + "FIX", (new D.element_impl (new eltype_fix)) ; + "COFIX", (new D.element_impl (new eltype_cofix)) ; + "arity", (new D.element_impl (new eltype_transparent)) ; + "term", (new D.element_impl (new eltype_transparent)) ; + "type", (new D.element_impl (new eltype_transparent)) ; + "body", (new D.element_impl (new eltype_transparent)) ; + "source", (new D.element_impl (new eltype_transparent)) ; + "target", (new D.element_impl (new eltype_transparent)) ; + "letintarget", (new D.element_impl (new eltype_transparent)) ; + "patternsType", (new D.element_impl (new eltype_transparent)) ; + "inductiveTerm", (new D.element_impl (new eltype_transparent)) ; + "pattern", (new D.element_impl (new eltype_transparent)) + ] + () +;; diff --git a/helm/ocaml/cic/cicParser3.mli b/helm/ocaml/cic/cicParser3.mli new file mode 100644 index 000000000..ada1b2e81 --- /dev/null +++ b/helm/ocaml/cic/cicParser3.mli @@ -0,0 +1,67 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This module is the terms level of a parser for cic objects from xml *) +(* files to the internal representation. It is used by the module cicParser2 *) +(* (objects level). It defines an extension of the standard dom using the *) +(* object-oriented extension machinery of markup: an object with a method *) +(* to_cic_term that returns the internal representation of the subtree is *) +(* added to each node of the dom tree *) +(* *) +(******************************************************************************) + +exception IllFormedXml of int + +val ids_to_targets : (Cic.id, Cic.anntarget) Hashtbl.t option ref +val current_sp : string list ref +val current_uri : UriManager.uri ref +val process_annotations : bool ref + +(* the "interface" of the class linked to each node of the dom tree *) +class virtual cic_term : + object ('a) + + (* fields and methods ever required by markup *) + val mutable node : cic_term Pxp_document.node option + method clone : 'a + method node : cic_term Pxp_document.node + method set_node : cic_term Pxp_document.node -> unit + + (* a method that returns the internal representation of the tree (term) *) + (* rooted in this node *) + method virtual to_cic_term : Cic.annterm + + end + +(* The definition of domspec, an hashtable that maps each node type to the *) +(* object that must be linked to it. Used by markup. *) +val domspec : cic_term Pxp_document.spec diff --git a/helm/ocaml/cic/deannotate.ml b/helm/ocaml/cic/deannotate.ml new file mode 100644 index 000000000..00d4854db --- /dev/null +++ b/helm/ocaml/cic/deannotate.ml @@ -0,0 +1,98 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +let expect_possible_parameters = ref false;; + +exception NotExpectingPossibleParameters;; + +let rec deannotate_term = + let module C = Cic in + function + C.ARel (_,_,n,_) -> C.Rel n + | C.AVar (_,_,uri) -> C.Var uri + | C.AMeta (_,_,n) -> C.Meta n + | C.ASort (_,_,s) -> C.Sort s + | C.AImplicit _ -> C.Implicit + | C.ACast (_,_,va,ty) -> C.Cast (deannotate_term va, deannotate_term ty) + | C.AProd (_,_,name,so,ta) -> + C.Prod (name, deannotate_term so, deannotate_term ta) + | C.ALambda (_,_,name,so,ta) -> + C.Lambda (name, deannotate_term so, deannotate_term ta) + | C.ALetIn (_,_,name,so,ta) -> + C.LetIn (name, deannotate_term so, deannotate_term ta) + | C.AAppl (_,_,l) -> C.Appl (List.map deannotate_term l) + | C.AConst (_,_,uri, cookingsno) -> C.Const (uri, cookingsno) + | C.AAbst (_,_,uri) -> C.Abst uri + | C.AMutInd (_,_,uri,cookingsno,i) -> C.MutInd (uri,cookingsno,i) + | C.AMutConstruct (_,_,uri,cookingsno,i,j) -> + C.MutConstruct (uri,cookingsno,i,j) + | C.AMutCase (_,_,uri,cookingsno,i,outtype,te,pl) -> + C.MutCase (uri,cookingsno,i,deannotate_term outtype, + deannotate_term te, List.map deannotate_term pl) + | C.AFix (_,_,funno,ifl) -> + C.Fix (funno, List.map deannotate_inductiveFun ifl) + | C.ACoFix (_,_,funno,ifl) -> + C.CoFix (funno, List.map deannotate_coinductiveFun ifl) + +and deannotate_inductiveFun (name,index,ty,bo) = + (name, index, deannotate_term ty, deannotate_term bo) + +and deannotate_coinductiveFun (name,ty,bo) = + (name, deannotate_term ty, deannotate_term bo) +;; + +let deannotate_inductiveType (name, isinductive, arity, cons) = + (name, isinductive, deannotate_term arity, + List.map (fun (id,ty,recs) -> (id,deannotate_term ty, recs)) cons) +;; + +let deannotate_obj = + let module C = Cic in + function + C.ADefinition (_, _, id, bo, ty, params) -> + (match params with + C.Possible params -> + if !expect_possible_parameters then + C.Definition (id, deannotate_term bo, deannotate_term ty, params) + else + raise NotExpectingPossibleParameters + | C.Actual params -> + C.Definition (id, deannotate_term bo, deannotate_term ty, params) + ) + | C.AAxiom (_, _, id, ty, params) -> + C.Axiom (id, deannotate_term ty, params) + | C.AVariable (_, _, name, bo, ty) -> + C.Variable (name, + (match bo with None -> None | Some bo -> Some (deannotate_term bo)), + deannotate_term ty) + | C.ACurrentProof (_, _, name, conjs, bo, ty) -> + C.CurrentProof ( + name, List.map (fun (id,con) -> (id,deannotate_term con)) conjs, + deannotate_term bo, deannotate_term ty + ) + | C.AInductiveDefinition (_, _, tys, params, parno) -> + C.InductiveDefinition ( List.map deannotate_inductiveType tys, + params, parno) +;; diff --git a/helm/ocaml/cic_annotations/Makefile b/helm/ocaml/cic_annotations/Makefile new file mode 100644 index 000000000..776d6c459 --- /dev/null +++ b/helm/ocaml/cic_annotations/Makefile @@ -0,0 +1,39 @@ +BIN_DIR = /usr/local/bin +REQUIRES = helm-cic helm-xml lablgtk +PREDICATES = +OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" +OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) +OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLDEP = ocamldep + +all: cicAnnotation2Xml.cmo cicAnnotationHinter.cmo cicAnnotationParser2.cmo \ + cicAnnotationParser.cmo cicXPath.cmo +opt: cicAnnotation2Xml.cmx cicAnnotationHinter.cmx cicAnnotationParser2.cmx \ + cicAnnotationParser.cmx cicXPath.cmx + +DEPOBJS = cicAnnotation2Xml.ml cicAnnotationHinter.ml cicAnnotationParser2.ml \ + cicAnnotationParser.ml cicXPath.ml + +depend: + $(OCAMLDEP) $(DEPOBJS) > .depend + +.SUFFIXES: .ml .mli .cmo .cmi .cmx +.ml.cmo: + $(OCAMLC) -c $< +.mli.cmi: + $(OCAMLC) -c $< +.ml.cmx: + $(OCAMLOPT) -c $< + +clean: + rm -f *.cm[iox] + +install: + #cp + +uninstall: + #rm -f + +.PHONY: install uninstall clean + +include .depend diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml new file mode 100644 index 000000000..c5410b080 --- /dev/null +++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml @@ -0,0 +1,225 @@ +(* 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/. + *) + +(*CSC codice cut & paste da cicPp e xmlcommand *) + +exception ImpossiblePossible;; +exception NotImplemented;; +exception BinderNotSpecified;; + +let dtdname = "http://www.cs.unibo.it/helm/dtd/annotations.dtd";; + +(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *) +let print_term = + let rec aux = + let module C = Cic in + let module X = Xml in + let module U = UriManager in + function + C.ARel (id,ann,_,_) -> + (match !ann with + None -> [<>] + | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) + ) + | C.AVar (id,ann,_) -> + (match !ann with + None -> [<>] + | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) + ) + | C.AMeta (id,ann,_) -> + (match !ann with + None -> [<>] + | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) + ) + | C.ASort (id,ann,_) -> + (match !ann with + None -> [<>] + | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) + ) + | C.AImplicit _ -> raise NotImplemented + | C.AProd (id,ann,_,s,t) -> + [< (match !ann with + None -> [<>] + | Some ann -> + (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) + ) ; + aux s ; + aux t + >] + | C.ACast (id,ann,v,t) -> + [< (match !ann with + None -> [<>] + | Some ann -> + (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) + ) ; + aux v ; + aux t + >] + | C.ALambda (id,ann,_,s,t) -> + [< (match !ann with + None -> [<>] + | Some ann -> + (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) + ) ; + aux s ; + aux t + >] + | C.ALetIn (id,ann,_,s,t) -> + [< (match !ann with + None -> [<>] + | Some ann -> + (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) + ) ; + aux s ; + aux t + >] + | C.AAppl (id,ann,li) -> + [< (match !ann with + None -> [<>] + | Some ann -> + (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) + ) ; + List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>] + >] + | C.AConst (id,ann,_,_) -> + (match !ann with + None -> [<>] + | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) + ) + | C.AAbst (id,ann,_) -> raise NotImplemented + | C.AMutInd (id,ann,_,_,_) -> + (match !ann with + None -> [<>] + | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) + ) + | C.AMutConstruct (id,ann,_,_,_,_) -> + (match !ann with + None -> [<>] + | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) + ) + | C.AMutCase (id,ann,_,_,_,ty,te,patterns) -> + [< (match !ann with + None -> [<>] + | Some ann -> + (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) + ) ; + aux ty ; + aux te ; + List.fold_right + (fun x i -> [< aux x ; i>]) + patterns [<>] + >] + | C.AFix (id, ann, _, funs) -> + [< (match !ann with + None -> [<>] + | Some ann -> + (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) + ) ; + List.fold_right + (fun (_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>] + >] + | C.ACoFix (id, ann,no,funs) -> + [< (match !ann with + None -> [<>] + | Some ann -> + (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) + ) ; + List.fold_right + (fun (_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>] + >] + in + aux +;; + +let print_mutual_inductive_type (_,_,arity,constructors) = + [< print_term arity ; + List.fold_right + (fun (name,ty,_) i -> [< print_term ty ; i >]) constructors [<>] + >] +;; + +let pp_annotation obj curi = + let module C = Cic in + let module X = Xml in + [< X.xml_cdata "\n" ; + X.xml_cdata ("\n\n") ; + X.xml_nempty "Annotations" + ["of", UriManager.string_of_uri (UriManager.cicuri_of_uri curi)] + begin + match obj with + C.ADefinition (xid, ann, _, te, ty, _) -> + [< (match !ann with + None -> [<>] + | Some ann -> + X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann) + ) ; + print_term te ; + print_term ty + >] + | C.AAxiom (xid, ann, _, ty, _) -> + [< (match !ann with + None -> [<>] + | Some ann -> + X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann) + ) ; + print_term ty + >] + | C.AVariable (xid, ann, _, bo, ty) -> + [< (match !ann with + None -> [<>] + | Some ann -> + X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann) + ) ; + (match bo with + None -> [<>] + | Some bo -> print_term bo + ) ; + print_term ty + >] + | C.ACurrentProof (xid, ann, _, conjs, bo, ty) -> + [< (match !ann with + None -> [<>] + | Some ann -> + X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann) + ) ; + List.fold_right + (fun (_,t) i -> [< print_term t ; i >]) + conjs [<>] ; + print_term bo ; + print_term ty + >] + | C.AInductiveDefinition (xid, ann, tys, params, paramsno) -> + [< (match !ann with + None -> [<>] + | Some ann -> + X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann) + ) ; + List.fold_right + (fun x i -> [< print_mutual_inductive_type x ; i >]) + tys [< >] + >] + end + >] +;; diff --git a/helm/ocaml/cic_annotations/cicAnnotationHinter.ml b/helm/ocaml/cic_annotations/cicAnnotationHinter.ml new file mode 100644 index 000000000..86bcb4588 --- /dev/null +++ b/helm/ocaml/cic_annotations/cicAnnotationHinter.ml @@ -0,0 +1,381 @@ +(* 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 *) +(* *) +(* *) +(******************************************************************************) + +let deactivate_hints_from annotation_window n = + let annotation_hints = annotation_window#annotation_hints in + for i = n to Array.length annotation_hints - 1 do + annotation_hints.(i)#misc#hide () + done +;; + +(* CSC: orripilante *) +(* the list of the signal ids *) +let sig_ids = ref ([] : GtkSignal.id list);; + +let disconnect_hint annotation_window buttonno = + match !sig_ids with + id::ids -> + annotation_window#annotation_hints.(buttonno)#misc#disconnect id ; + sig_ids := ids + | _ -> assert false +;; + +(* link_hint annotation_window n label hint *) +(* set the label of the nth hint button of annotation_window to label *) +(* and the correspondent hint to hint *) +let link_hint annotation_window buttonno label hint = + let button = annotation_window#annotation_hints.(buttonno) in + sig_ids := + (button#connect#clicked + (fun () -> (annotation_window#annotation : GEdit.text)#insert hint) + ) :: !sig_ids ; + button#misc#show () ; + match button#children with + [labelw] -> (GMisc.label_cast labelw)#set_text label + | _ -> assert false +;; + +exception TooManyHints;; + +let link_hints annotation_window a = + if Array.length a > Array.length annotation_window#annotation_hints then + raise TooManyHints ; + for i = List.length !sig_ids - 1 downto 0 do + disconnect_hint annotation_window i + done ; + Array.iteri + (fun i (label,hint) -> link_hint annotation_window i label hint) a ; + deactivate_hints_from annotation_window (Array.length a) +;; + +let list_mapi f = + let rec aux n = + function + [] -> [] + | he::tl -> (f n he)::(aux (n + 1) tl) + in + aux 0 +;; + +let get_id annterm = + let module C = Cic in + match annterm with + C.ARel (id,_,_,_) -> id + | C.AVar (id,_,_) -> id + | C.AMeta (id,_,_) -> id + | C.ASort (id,_,_) -> id + | C.AImplicit (id,_) -> id + | C.ACast (id,_,_,_) -> id + | C.AProd (id,_,_,_,_) -> id + | C.ALambda (id,_,_,_,_) -> id + | C.ALetIn (id,_,_,_,_) -> id + | C.AAppl (id,_,_) -> id + | C.AConst (id,_,_,_) -> id + | C.AAbst (id,_,_) -> id + | C.AMutInd (id,_,_,_,_) -> id + | C.AMutConstruct (id,_,_,_,_,_)-> id + | C.AMutCase (id,_,_,_,_,_,_,_) -> id + | C.AFix (id,_,_,_) -> id + | C.ACoFix (id,_,_,_) -> id +;; + +let create_hint_from_term annotation_window annterm = + let module C = Cic in + match annterm with + C.ARel (id,_,_,_) -> + link_hints annotation_window + [| "Binder", "" |] + | C.AVar (id,_,_) -> + link_hints annotation_window + [| "relURI???", "" |] + | C.AMeta (id,_,_) -> + link_hints annotation_window + [| "Number", "" |] + | C.ASort (id,_,_) -> + link_hints annotation_window + [| "Value", "" |] + | C.AImplicit (id,_) -> + link_hints annotation_window [| |] + | C.ACast (id,_,bo,ty) -> + let boid = get_id bo + and tyid = get_id ty in + link_hints annotation_window + [| "Body", "" ; + "Type", "" + |] + | C.AProd (id,_,_,ty,bo) -> + let boid = get_id bo + and tyid = get_id ty in + link_hints annotation_window + [| "Binder", + "" ; + "Body", "" ; + "Type", "" + |] + | C.ALambda (id,_,_,ty,bo) -> + let boid = get_id bo + and tyid = get_id ty in + link_hints annotation_window + [| "Binder", + "" ; + "Body", "" ; + "Type", "" + |] + | C.ALetIn (id,_,_,ty,bo) -> + let boid = get_id bo + and tyid = get_id ty in + link_hints annotation_window + [| "Binder", + "" ; + "Term", "" ; + "Target", "" + |] + | C.AAppl (id,_,args) -> + let argsid = + Array.mapi + (fun i te -> "Argument " ^ string_of_int i, "") + (Array.of_list args) + in + link_hints annotation_window argsid + | C.AConst (id,_,_,_) -> + link_hints annotation_window + [| "Uri???", "" |] + | C.AAbst (id,_,_) -> + link_hints annotation_window + [| "Uri???", "" |] + | C.AMutInd (id,_,_,_,_) -> + link_hints annotation_window + [| "Uri???", "" |] + | C.AMutConstruct (id,_,_,_,_,_) -> + link_hints annotation_window + [| "Uri???", "" |] + | C.AMutCase (id,_,_,_,_,outty,te,pl) -> + let outtyid = get_id outty + and teid = get_id te + and plid = + Array.mapi + (fun i te -> "Pattern " ^ string_of_int i, "") + (Array.of_list pl) + in + link_hints annotation_window + (Array.append + [| "Uri???", "" ; + "Case Type", "" ; + "Term", "" ; + |] + plid) + | C.AFix (id,_,_,funl) -> + let funtylid = + Array.mapi + (fun i (_,_,ty,_) -> + "Type " ^ string_of_int i, "") + (Array.of_list funl) + and funbolid = + Array.mapi + (fun i (_,_,_,bo) -> + "Body " ^ string_of_int i, "") + (Array.of_list funl) + and funnamel = + Array.mapi + (fun i (_,_,_,_) -> + "Name " ^ string_of_int i, "") + (Array.of_list funl) + and funrecindexl = + Array.mapi + (fun i (_,_,_,_) -> + "Recursive Index??? " ^ string_of_int i, "") + (Array.of_list funl) + in + link_hints annotation_window + (Array.concat + [ funtylid ; + funbolid ; + funnamel ; + funrecindexl ; + [| "NoFun???", "" |] + ] + ) + | C.ACoFix (id,_,_,funl) -> + let funtylid = + Array.mapi + (fun i (_,ty,_) -> + "Type " ^ string_of_int i, "") + (Array.of_list funl) + and funbolid = + Array.mapi + (fun i (_,_,bo) -> + "Body " ^ string_of_int i, "") + (Array.of_list funl) + and funnamel = + Array.mapi + (fun i (_,_,_) -> + "Name " ^ string_of_int i, "") + (Array.of_list funl) + in + link_hints annotation_window + (Array.concat + [ funtylid ; + funbolid ; + funnamel ; + [| "NoFun???", "" |] + ] + ) +;; + +(*CSC: da riscrivere completamente eliminando il paciugo degli array - liste *) +let create_hint_from_obj annotation_window annobj = + let module C = Cic in + match annobj with + C.ADefinition (id,_,_,bo,ty,_) -> + let boid = get_id bo + and tyid = get_id ty in + link_hints annotation_window + [| "Name", "" ; + "Ingredients", "" ; + "Body", "" ; + "Type", "" + |] + | C.AAxiom (id,_,_,ty,_) -> + let tyid = get_id ty in + link_hints annotation_window + [| "Name", "" ; + "Ingredients", "" ; + "Type", "" + |] + | C.AVariable (id,_,_,bo,ty) -> + let tyid = get_id ty in + link_hints annotation_window + (match bo with + None -> + [| "Name", "" ; + "Type", "" + |] + | Some bo -> + let boid = get_id bo in + [| "Name", "" ; + "Body", "" ; + "Type", "" + |] + ) + | C.ACurrentProof (id,_,_,conjs,bo,ty) -> + let boid = get_id bo + and tyid = get_id ty + and conjsid = List.map (fun (_,te) -> get_id te) conjs in + link_hints annotation_window + (Array.append + [| "Name", "" ; + "Ingredients", "" ; + "Body", "" ; + "Type", "" + |] + (Array.mapi + (fun i id -> + "Conjecture " ^ string_of_int i, "" + ) (Array.of_list conjsid) + ) + ) + | C.AInductiveDefinition (id,_,itl,_,_) -> + let itlids = + List.map + (fun (_,_,arity,cons) -> + get_id arity, + List.map (fun (_,ty,_) -> get_id ty) cons + ) itl + in + link_hints annotation_window + (Array.concat + [ + [| "Ingredients","" |]; + (Array.mapi + (fun i _ -> + "Type Name " ^ string_of_int i, + "" + ) (Array.of_list itlids) + ) ; + (Array.mapi + (fun i (id,_) -> + "Type " ^ string_of_int i, "" + ) (Array.of_list itlids) + ) ; + (Array.concat + (list_mapi + (fun i (_,consid) -> + (Array.mapi + (fun j _ -> + "Constructor Name " ^ string_of_int i ^ " " ^ string_of_int j, + "" + ) (Array.of_list consid) + ) ; + ) itlids + ) + ) ; + (Array.concat + (list_mapi + (fun i (_,consid) -> + (Array.mapi + (fun j id -> + "Constructor " ^ string_of_int i ^ " " ^ string_of_int j, + "" + ) (Array.of_list consid) + ) ; + ) itlids + ) + ) + ] + ) +;; + +exception IdUnknown of string;; + +let create_hints annotation_window (annobj,ids_to_targets) xpath = + try + match Hashtbl.find ids_to_targets xpath with + Cic.Object annobj -> create_hint_from_obj annotation_window annobj + | Cic.Term annterm -> create_hint_from_term annotation_window annterm + with + Not_found -> raise (IdUnknown xpath) +;; diff --git a/helm/ocaml/cic_annotations/cicAnnotationParser.ml b/helm/ocaml/cic_annotations/cicAnnotationParser.ml new file mode 100644 index 000000000..9c4a58d53 --- /dev/null +++ b/helm/ocaml/cic_annotations/cicAnnotationParser.ml @@ -0,0 +1,55 @@ +(* 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 Warnings;; + +class warner = + object + method warn w = + print_endline ("WARNING: " ^ w) ; + (raise Warnings : unit) + end +;; + +exception EmptyUri;; + +let annotate filename ids_to_targets = + let module Y = Pxp_yacc in + try + let d = + 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) + Y.default_spec + + in + CicAnnotationParser2.annotate ids_to_targets d#root + with + e -> + print_endline (Pxp_types.string_of_exn e) ; + raise e +;; diff --git a/helm/ocaml/cic_annotations/cicAnnotationParser2.ml b/helm/ocaml/cic_annotations/cicAnnotationParser2.ml new file mode 100644 index 000000000..58edc4ca8 --- /dev/null +++ b/helm/ocaml/cic_annotations/cicAnnotationParser2.ml @@ -0,0 +1,129 @@ +(* 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 IllFormedXml of int;; + +(* Utility functions that transform a Pxp attribute into something useful *) + +let string_of_attr a = + let module T = Pxp_types in + match a with + T.Value s -> s + | _ -> raise (IllFormedXml 0) +;; + +exception DontKnowWhatToDo;; + +let rec string_of_annotations n = + let module D = Pxp_document in + let module T = Pxp_types in + match n#node_type with + D.T_element s -> + "<" ^ s ^ + List.fold_right + (fun att i -> + match n#attribute att with + T.Value s -> " " ^ att ^ "=\"" ^ s ^ "\"" ^ i + | T.Implied_value -> i + | T.Valuelist l -> " " ^ att ^ "=\"" ^ String.concat " " l ^ "\"" ^ i + ) (n#attribute_names) "" ^ + (match n#sub_nodes with + [] -> "/>" + | l -> + ">" ^ + String.concat "" (List.map string_of_annotations l) ^ + "" + ) + | D.T_data -> n#data + | _ -> raise DontKnowWhatToDo +;; + +let get_annotation n = + String.concat "" (List.map string_of_annotations (n#sub_nodes)) +;; + +let annotate_object ann obj = + let module C = Cic in + let rann = + match obj with + C.ADefinition (_, rann, _, _, _, _) -> rann + | C.AAxiom (_, rann, _, _, _) -> rann + | C.AVariable (_, rann, _, _, _) -> rann + | C.ACurrentProof (_, rann, _, _, _, _) -> rann + | C.AInductiveDefinition (_, rann, _, _, _) -> rann + in + rann := Some ann +;; + +let annotate_term ann term = + let module C = Cic in + let rann = + match term with + C.ARel (_, rann, _, _) -> rann + | C.AVar (_, rann, _) -> rann + | C.AMeta (_, rann, _) -> rann + | C.ASort (_, rann, _) -> rann + | C.AImplicit (_, rann) -> rann + | C.ACast (_, rann, _, _) -> rann + | C.AProd (_, rann, _, _, _) -> rann + | C.ALambda (_, rann, _, _, _) -> rann + | C.ALetIn (_, rann, _, _, _) -> rann + | C.AAppl (_, rann, _) -> rann + | C.AConst (_, rann, _, _) -> rann + | C.AAbst (_, rann, _) -> rann + | C.AMutInd (_, rann, _, _, _) -> rann + | C.AMutConstruct (_, rann, _, _, _, _) -> rann + | C.AMutCase (_, rann, _, _, _, _, _, _) -> rann + | C.AFix (_, rann, _, _) -> rann + | C.ACoFix (_, rann, _, _) -> rann + in + rann := Some ann +;; + +let annotate ids_to_targets n = + let module D = Pxp_document in + let module C = Cic in + let annotate_elem n = + let ntype = n # node_type in + match ntype with + D.T_element "Annotation" -> + let of_uri = string_of_attr (n # attribute "of") in + begin + try + match Hashtbl.find ids_to_targets of_uri with + C.Object o -> annotate_object (get_annotation n) o + | C.Term t -> annotate_term (get_annotation n) t + with + Not_found -> assert false + end + | D.T_element _ | D.T_data -> + raise (IllFormedXml 1) + | _ -> raise DontKnowWhatToDo + in + match n # node_type with + D.T_element "Annotations" -> + List.iter annotate_elem (n # sub_nodes) + | _ -> raise (IllFormedXml 2) +;; diff --git a/helm/ocaml/cic_annotations/cicXPath.ml b/helm/ocaml/cic_annotations/cicXPath.ml new file mode 100644 index 000000000..776d229af --- /dev/null +++ b/helm/ocaml/cic_annotations/cicXPath.ml @@ -0,0 +1,77 @@ +(* 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 *) +(* *) +(* *) +(******************************************************************************) + +let get_annotation_from_term annterm = + let module C = Cic in + match annterm with + C.ARel (_,ann,_,_) -> ann + | C.AVar (_,ann,_) -> ann + | C.AMeta (_,ann,_) -> ann + | C.ASort (_,ann,_) -> ann + | C.AImplicit (_,ann) -> ann + | C.ACast (_,ann,_,_) -> ann + | C.AProd (_,ann,_,_,_) -> ann + | C.ALambda (_,ann,_,_,_) -> ann + | C.ALetIn (_,ann,_,_,_) -> ann + | C.AAppl (_,ann,_) -> ann + | C.AConst (_,ann,_,_) -> ann + | C.AAbst (_,ann,_) -> ann + | C.AMutInd (_,ann,_,_,_) -> ann + | C.AMutConstruct (_,ann,_,_,_,_)-> ann + | C.AMutCase (_,ann,_,_,_,_,_,_) -> ann + | C.AFix (_,ann,_,_) -> ann + | C.ACoFix (_,ann,_,_) -> ann +;; + +let get_annotation_from_obj annobj = + let module C = Cic in + match annobj with + C.ADefinition (_,ann,_,_,_,_) -> ann + | C.AAxiom (_,ann,_,_,_) -> ann + | C.AVariable (_,ann,_,_,_) -> ann + | C.ACurrentProof (_,ann,_,_,_,_) -> ann + | C.AInductiveDefinition (_,ann,_,_,_) -> ann +;; + +exception IdUnknown of string;; + +let get_annotation (annobj,ids_to_targets) xpath = + try + match Hashtbl.find ids_to_targets xpath with + Cic.Object annobj -> get_annotation_from_obj annobj + | Cic.Term annterm -> get_annotation_from_term annterm + with + Not_found -> raise (IdUnknown xpath) +;; diff --git a/helm/ocaml/cic_annotations_cache/Makefile b/helm/ocaml/cic_annotations_cache/Makefile new file mode 100644 index 000000000..d5abc7bb4 --- /dev/null +++ b/helm/ocaml/cic_annotations_cache/Makefile @@ -0,0 +1,36 @@ +BIN_DIR = /usr/local/bin +REQUIRES = helm-cic_annotations +PREDICATES = +OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" +OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) +OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLDEP = ocamldep + +all: cicCache.cmo +opt: cicCache.cmx + +DEPOBJS = cicCache.mli cicCache.ml + +depend: + $(OCAMLDEP) $(DEPOBJS) > .depend + +.SUFFIXES: .ml .mli .cmo .cmi .cmx +.ml.cmo: + $(OCAMLC) -c $< +.mli.cmi: + $(OCAMLC) -c $< +.ml.cmx: + $(OCAMLOPT) -c $< + +clean: + rm -f *.cm[iox] + +install: + #cp + +uninstall: + #rm -f + +.PHONY: install uninstall clean + +include .depend diff --git a/helm/ocaml/cic_annotations_cache/cicCache.ml b/helm/ocaml/cic_annotations_cache/cicCache.ml new file mode 100644 index 000000000..b26bddbf8 --- /dev/null +++ b/helm/ocaml/cic_annotations_cache/cicCache.ml @@ -0,0 +1,51 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This module implements a trival cache system (an hash-table) for cic *) +(* objects. Uses the getter (getter.ml) and the parser (cicParser.ml) *) +(* *) +(******************************************************************************) + +let get_annobj uri = + let module G = Getter in + let module U = UriManager in + let cicfilename = G.getxml (U.cicuri_of_uri uri) in + match CicParser.term_of_xml cicfilename uri true with + (_, None) -> assert false + | (annobj, Some ids_to_targets) -> + if U.uri_is_annuri uri then + begin + let annfilename = G.getxml (U.annuri_of_uri uri) in + CicAnnotationParser.annotate annfilename ids_to_targets + end ; + (annobj, ids_to_targets) +;; diff --git a/helm/ocaml/cic_annotations_cache/cicCache.mli b/helm/ocaml/cic_annotations_cache/cicCache.mli new file mode 100644 index 000000000..b4c50c6c4 --- /dev/null +++ b/helm/ocaml/cic_annotations_cache/cicCache.mli @@ -0,0 +1,37 @@ +(* 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 implements a trival cache system (an hash-table) for cic *)(* objects. Uses the getter (getter.ml) and the parser (cicParser.ml) *)(* *) +(******************************************************************************) + +val get_annobj : + UriManager.uri -> Cic.annobj * (Cic.id, Cic.anntarget) Hashtbl.t diff --git a/helm/ocaml/cic_cache/Makefile b/helm/ocaml/cic_cache/Makefile new file mode 100644 index 000000000..f149ac97d --- /dev/null +++ b/helm/ocaml/cic_cache/Makefile @@ -0,0 +1,36 @@ +BIN_DIR = /usr/local/bin +REQUIRES = helm-cic +PREDICATES = +OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" +OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) +OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLDEP = ocamldep + +all: cicCache.cmo +opt: cicCache.cmx + +DEPOBJS = cicCache.mli cicCache.ml + +depend: + $(OCAMLDEP) $(DEPOBJS) > .depend + +.SUFFIXES: .ml .mli .cmo .cmi .cmx +.ml.cmo: + $(OCAMLC) -c $< +.mli.cmi: + $(OCAMLC) -c $< +.ml.cmx: + $(OCAMLOPT) -c $< + +clean: + rm -f *.cm[iox] + +install: + #cp + +uninstall: + #rm -f + +.PHONY: install uninstall clean + +include .depend diff --git a/helm/ocaml/cic_cache/cicCache.ml b/helm/ocaml/cic_cache/cicCache.ml new file mode 100644 index 000000000..7dfd8242d --- /dev/null +++ b/helm/ocaml/cic_cache/cicCache.ml @@ -0,0 +1,49 @@ +(* 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 implements a trival cache system (an hash-table) for cic *) +(* objects. Uses the getter (getter.ml) and the parser (cicParser.ml) *) +(* *) +(******************************************************************************) + +let get_annobj uri = + let module G = Getter in + let module U = UriManager in + let cicfilename = G.getxml (U.cicuri_of_uri uri) in + match CicParser.term_of_xml cicfilename uri false with + (_, Some _) -> assert false + | (annobj, None) -> annobj +;; + +let get_obj uri = + Deannotate.deannotate_obj (get_annobj uri) +;; diff --git a/helm/ocaml/cic_cache/cicCache.mli b/helm/ocaml/cic_cache/cicCache.mli new file mode 100644 index 000000000..58aa61763 --- /dev/null +++ b/helm/ocaml/cic_cache/cicCache.mli @@ -0,0 +1,37 @@ +(* 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 implements a trival cache system (an hash-table) for cic *)(* objects. Uses the getter (getter.ml) and the parser (cicParser.ml) *)(* *) +(******************************************************************************) + +val get_obj : UriManager.uri -> Cic.obj +val get_annobj : UriManager.uri -> Cic.annobj diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile new file mode 100644 index 000000000..61ba3b55d --- /dev/null +++ b/helm/ocaml/cic_proof_checking/Makefile @@ -0,0 +1,41 @@ +BIN_DIR = /usr/local/bin +REQUIRES = helm-cic +PREDICATES = +OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" +OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) +OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLDEP = ocamldep + +all: cicSubstitution.cmo cicEnvironment.cmo cicPp.cmo cicMiniReduction.cmo \ + cicReduction.cmo cicTypeChecker.cmo cicCooking.cmo +opt: cicSubstitution.cmx cicEnvironment.cmx cicPp.cmx cicMiniReduction.cmx \ + cicReduction.cmx cicTypeChecker.cmx cicCooking.cmx + +DEPOBJS = cicPp.mli cicPp.ml cicEnvironment.mli cicEnvironment.ml \ + cicSubstitution.mli cicSubstitution.ml cicReduction.mli \ + cicReduction.ml cicTypeChecker.mli cicTypeChecker.ml \ + cicCooking.mli cicCooking.ml cicMinireduction.mli cicMiniReduction.ml + +depend: + $(OCAMLDEP) $(DEPOBJS) > .depend + +.SUFFIXES: .ml .mli .cmo .cmi .cmx +.ml.cmo: + $(OCAMLC) -c $< +.mli.cmi: + $(OCAMLC) -c $< +.ml.cmx: + $(OCAMLOPT) -c $< + +clean: + rm -f *.cm[iox] + +install: + #cp + +uninstall: + #rm -f + +.PHONY: install uninstall clean + +include .depend diff --git a/helm/ocaml/cic_proof_checking/cicCooking.ml b/helm/ocaml/cic_proof_checking/cicCooking.ml new file mode 100644 index 000000000..86bf31660 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicCooking.ml @@ -0,0 +1,217 @@ +(* 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 Impossible;; +exception NotImplemented of int * string;; +exception WrongUriToConstant;; +exception WrongUriToVariable of string;; +exception WrongUriToInductiveDefinition;; + +(* mem x lol is true if x is a member of one *) +(* of the lists of the list of (int * list) lol *) +let mem x lol = + List.fold_right (fun (_,l) i -> i || List.mem x l) lol false +;; + +(* cook var term *) +let cook curi cookingsno var = + let rec aux k = + let module C = Cic in + function + C.Rel n as t -> + (match n with + n when n >= k -> C.Rel (n + 1) + | _ -> C.Rel n + ) + | C.Var uri as t -> + if UriManager.eq uri var then + C.Rel k + else + t + | C.Meta _ as t -> t + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te, ty) -> C.Cast (aux k te, aux k ty) + | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t) + | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t) + | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t) + | C.Appl (he::tl) -> + (* Get rid of C.Appl (C.Appl l1) l2 *) + let newtl = List.map (aux k) tl in + (match aux k he with + C.Appl (he'::tl') -> C.Appl (he'::(tl'@newtl)) + | t -> C.Appl (t::newtl) + ) + | C.Appl [] -> raise Impossible + | C.Const (uri,_) -> + if match CicEnvironment.get_obj uri with + C.Definition (_,_,_,params) when mem var params -> true + | C.Definition _ -> false + | C.Axiom (_,_,params) when mem var params -> true + | C.Axiom _ -> false + | C.CurrentProof _ -> + raise (NotImplemented (2,(UriManager.string_of_uri uri))) + | _ -> raise WrongUriToConstant + then + C.Appl + ((C.Const (uri,UriManager.relative_depth curi uri cookingsno)):: + [C.Rel k]) + else + C.Const (uri,UriManager.relative_depth curi uri cookingsno) + | C.Abst _ as t -> t + | C.MutInd (uri,_,i) -> + if match CicEnvironment.get_obj uri with + C.InductiveDefinition (_,params,_) when mem var params -> true + | C.InductiveDefinition _ -> false + | _ -> raise WrongUriToInductiveDefinition + then + C.Appl ((C.MutInd (uri,UriManager.relative_depth curi uri cookingsno,i))::[C.Rel k]) + else + C.MutInd (uri,UriManager.relative_depth curi uri cookingsno,i) + | C.MutConstruct (uri,_,i,j) -> + if match CicEnvironment.get_obj uri with + C.InductiveDefinition (_,params,_) when mem var params -> true + | C.InductiveDefinition _ -> false + | _ -> raise WrongUriToInductiveDefinition + then + C.Appl ((C.MutConstruct (uri,UriManager.relative_depth curi uri cookingsno,i,j))::[C.Rel k]) + else + C.MutConstruct (uri,UriManager.relative_depth curi uri cookingsno,i,j) + | C.MutCase (uri,_,i,outt,term,pl) -> + let substitutedfl = + List.map (aux k) pl + in + C.MutCase (uri,UriManager.relative_depth curi uri cookingsno,i, + aux k outt,aux k term, substitutedfl) + | C.Fix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name,i,aux k ty, aux (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,aux k ty, aux (k+len) bo)) + fl + in + C.CoFix (i, substitutedfl) + in + aux 1 +;; + +let cook_gen add_binder curi cookingsno ty vars = + let module C = Cic in + let module U = UriManager in + let rec cookrec ty = + function + var::tl -> + let (varname, varbody, vartype) = + match CicEnvironment.get_obj var with + C.Variable (varname, varbody, vartype) -> (varname, varbody, vartype) + | _ -> raise (WrongUriToVariable (U.string_of_uri var)) + in + cookrec (add_binder (C.Name varname) varbody vartype + (cook curi cookingsno var ty)) tl + | _ -> ty + in + cookrec ty vars +;; + +let cook_prod = + cook_gen (fun n b s t -> + match b with + None -> Cic.Prod (n,s,t) + | Some b -> Cic.LetIn (n,b,t) + ) +and cook_lambda = + cook_gen (fun n b s t -> + match b with + None -> Cic.Lambda (n,s,t) + | Some b -> Cic.LetIn (n,b,t) + ) +;; + +(*CSC: sbagliato da rifare e completare *) +let cook_one_level obj curi cookingsno vars = + let module C = Cic in + match obj with + C.Definition (id,te,ty,params) -> + let ty' = cook_prod curi cookingsno ty vars in + let te' = cook_lambda curi cookingsno te vars in + C.Definition (id,te',ty',params) + | C.Axiom (id,ty,parameters) -> + let ty' = cook_prod curi cookingsno ty vars in + C.Axiom (id,ty',parameters) + | C.Variable _ as obj -> obj + | C.CurrentProof (id,conjs,te,ty) -> + let ty' = cook_prod curi cookingsno ty vars in + let te' = cook_lambda curi cookingsno te vars in + C.CurrentProof (id,conjs,te',ty') + | C.InductiveDefinition (dl, params, n_ind_params) -> + let dl' = + List.map + (fun (name,inductive,arity,constructors) -> + let constructors' = + List.map + (fun (name,ty,r) -> + let r' = + match !r with + None -> raise Impossible + | Some r -> List.map (fun _ -> false) vars @ r + in + (name,cook_prod curi cookingsno ty vars,ref (Some r')) + ) constructors + in + (name,inductive,cook_prod curi cookingsno arity vars,constructors') + ) dl + in + C.InductiveDefinition (dl', params, n_ind_params + List.length vars) +;; + +let cook_obj obj uri = + let module C = Cic in + let params = + match obj with + C.Definition (_,_,_,params) -> params + | C.Axiom (_,_,params) -> params + | C.Variable _ -> [] + | C.CurrentProof _ -> [] + | C.InductiveDefinition (_,params,_) -> params + in + let rec cook_all_levels obj = + function + [] -> [] + | (n,vars)::tl -> + let cooked_obj = cook_one_level obj uri (n + 1) (List.rev vars) in + (n,cooked_obj)::(cook_all_levels cooked_obj tl) + in + cook_all_levels obj (List.rev params) +;; + +CicEnvironment.set_cooking_function cook_obj;; diff --git a/helm/ocaml/cic_proof_checking/cicCooking.mli b/helm/ocaml/cic_proof_checking/cicCooking.mli new file mode 100644 index 000000000..203bf6c33 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicCooking.mli @@ -0,0 +1,31 @@ +(* 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 Impossible +exception NotImplemented of int * string +exception WrongUriToConstant +exception WrongUriToVariable of string +exception WrongUriToInductiveDefinition +val cook_obj : Cic.obj -> UriManager.uri -> (int * Cic.obj) list diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml new file mode 100644 index 000000000..fbe5e4b26 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -0,0 +1,217 @@ +(* 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 implements a trival cache system (an hash-table) for cic *) +(* objects. Uses the getter (getter.ml) and the parser (cicParser.ml) *) +(* *) +(******************************************************************************) + +let raise e = print_endline "***" ; flush stdout ; print_endline (Printexc.to_string e) ; flush stdout ; raise e;; + +(*CSC: forse i due seguenti tipi sono da unificare? *) +type cooked_obj = + Cooked of Cic.obj + | Frozen of Cic.obj + | Unchecked of Cic.obj +type type_checked_obj = + CheckedObj of Cic.obj (* cooked obj *) + | UncheckedObj of Cic.obj (* uncooked obj *) +;; + +exception NoFunctionProvided;; + +let cook_obj = ref (fun obj uri -> raise NoFunctionProvided);; + +let set_cooking_function foo = + cook_obj := foo +;; + +exception CircularDependency of string;; +exception CouldNotUnfreeze of string;; +exception Impossible;; +exception UncookedObj;; + +module HashedType = + struct + type t = UriManager.uri * int (* uri, livello di cottura *) + let equal (u1,n1) (u2,n2) = UriManager.eq u1 u2 && n1 = n2 + let hash = Hashtbl.hash + end +;; + +(* Hashtable that uses == instead of = for testing equality *) +module HashTable = Hashtbl.Make(HashedType);; + +let hashtable = HashTable.create 271;; + +(* n is the number of time that the object must be cooked *) +let get_obj_and_type_checking_info uri n = + try + HashTable.find hashtable (uri,n) + with + Not_found -> + try + match HashTable.find hashtable (uri,0) with + Cooked _ + | Frozen _ -> raise Impossible + | Unchecked _ as t -> t + with + Not_found -> + let filename = Getter.getxml uri in + let (annobj,_) = CicParser.term_of_xml filename uri false in + let obj = Deannotate.deannotate_obj annobj in + let output = Unchecked obj in + HashTable.add hashtable (uri,0) output ; + output +;; + +(* DANGEROUS!!! *) +(* USEFUL ONLY DURING THE FIXING OF THE FILES *) +(* change_obj uri (Some newobj) *) +(* maps uri to newobj in cache. *) +(* change_obj uri None *) +(* maps uri to a freeze dummy-object. *) +let change_obj uri newobj = + let newobj = + match newobj with + Some newobj' -> Unchecked newobj' + | None -> Frozen (Cic.Variable ("frozen-dummy", None, Cic.Implicit)) + in + HashTable.remove hashtable (uri,0) ; + HashTable.add hashtable (uri,0) newobj +;; + +let is_annotation_uri uri = + Str.string_match (Str.regexp ".*\.ann$") (UriManager.string_of_uri uri) 0 +;; + +(* returns both the annotated and deannotated uncooked forms (plus the *) +(* map from ids to annotation targets) *) +let get_annobj_and_type_checking_info uri = + let filename = Getter.getxml uri in + match CicParser.term_of_xml filename uri true with + (_, None) -> raise Impossible + | (annobj, Some ids_to_targets) -> + (* If uri is the uri of an annotation, let's use the annotation file *) + if is_annotation_uri uri then +(* CSC: la roba annotata non dovrebbe piu' servire + AnnotationParser.annotate (Getter.get_ann uri) ids_to_targets ; +*) assert false ; + try + (annobj, ids_to_targets, HashTable.find hashtable (uri,0)) + with + Not_found -> + let obj = Deannotate.deannotate_obj annobj in + let output = Unchecked obj in + HashTable.add hashtable (uri,0) output ; + (annobj, ids_to_targets, output) +;; + + +(* get_obj uri *) +(* returns the cic object whose uri is uri. If the term is not just in cache, *) +(* then it is parsed via CicParser.term_of_xml from the file whose name is *) +(* the result of Getter.getxml uri *) +let get_obj uri = + match get_obj_and_type_checking_info uri 0 with + Unchecked obj -> obj + | Frozen obj -> obj + | Cooked obj -> obj +;; + +(* get_annobj uri *) +(* returns the cic object whose uri is uri either in annotated and *) +(* deannotated form. The term is put into the cache if it's not there yet. *) +let get_annobj uri = + let (ann, ids_to_targets, deann) = get_annobj_and_type_checking_info uri in + let deannobj = + match deann with + Unchecked obj -> obj + | Frozen _ -> raise (CircularDependency (UriManager.string_of_uri uri)) + | Cooked obj -> obj + in + (ann, ids_to_targets, deannobj) +;; + +(*CSC Commento falso *) +(* get_obj uri *) +(* returns the cooked cic object whose uri is uri. The term must be present *) +(* and cooked in cache *) +let rec get_cooked_obj uri cookingsno = + match get_obj_and_type_checking_info uri cookingsno with + Unchecked _ + | Frozen _ -> raise UncookedObj + | Cooked obj -> obj +;; + +(* is_type_checked uri *) +(* CSC: commento falso ed obsoleto *) +(* returns true if the term has been type-checked *) +(* otherwise it returns false and freeze the term for type-checking *) +(* set_type_checking_info must be called to unfreeze the term *) +let is_type_checked uri cookingsno = + match get_obj_and_type_checking_info uri cookingsno with + Cooked obj -> CheckedObj obj + | Unchecked obj -> + HashTable.remove hashtable (uri,0) ; + HashTable.add hashtable (uri,0) (Frozen obj) ; + UncheckedObj obj + | Frozen _ -> raise (CircularDependency (UriManager.string_of_uri uri)) +;; + +(* set_type_checking_info uri *) +(* must be called once the type-checking of uri is finished *) +(* The object whose uri is uri is unfreezed *) +let set_type_checking_info uri = + match HashTable.find hashtable (uri,0) with + Frozen obj -> + (* let's cook the object at every level *) + HashTable.remove hashtable (uri,0) ; + let obj' = CicSubstitution.undebrujin_inductive_def uri obj in + HashTable.add hashtable (uri,0) (Cooked obj') ; + let cooked_objs = !cook_obj obj' uri in + let last_cooked_level = ref 0 in + let last_cooked_obj = ref obj' in + List.iter + (fun (n,cobj) -> + for i = !last_cooked_level + 1 to n do + HashTable.add hashtable (uri,i) (Cooked !last_cooked_obj) + done ; + HashTable.add hashtable (uri,n + 1) (Cooked cobj) ; + last_cooked_level := n + 1 ; + last_cooked_obj := cobj + ) cooked_objs ; + for i = !last_cooked_level + 1 to UriManager.depth_of_uri uri + 1 do + HashTable.add hashtable (uri,i) (Cooked !last_cooked_obj) + done + | _ -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri)) +;; diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli new file mode 100644 index 000000000..c3ffd6fe4 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -0,0 +1,83 @@ +(* 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 implements a trival cache system (an hash-table) for cic *)(* objects. Uses the getter (getter.ml) and the parser (cicParser.ml) *)(* *) +(******************************************************************************) + +exception CircularDependency of string;; + +(* get_obj uri *) +(* returns the cic object whose uri is uri. If the term is not just in cache, *) +(* then it is parsed via CicParser.term_of_xml from the file whose name is *) +(* the result of Getter.get uri *) +val get_obj : UriManager.uri -> Cic.obj + +(* get_annobj uri *) +(* returns the cic object whose uri is uri either in annotated and in *) +(* deannotated form. It returns also the map from ids to annotation targets. *) +(* The term is put in cache if it's not there yet. *) +(* The functions raise CircularDependency if asked to retrieve a Frozen object*) +val get_annobj : + UriManager.uri -> Cic.annobj * (Cic.id, Cic.anntarget) Hashtbl.t * Cic.obj + +(* DANGEROUS!!! *) +(* USEFUL ONLY DURING THE FIXING OF THE FILES *) +(* change_obj uri (Some newobj) *) +(* maps uri to newobj in cache. *) +(* change_obj uri None *) +(* maps uri to a freeze dummy-object. *) +val change_obj : UriManager.uri -> Cic.obj option -> unit + +type type_checked_obj = + CheckedObj of Cic.obj (* cooked obj *) + | UncheckedObj of Cic.obj (* uncooked obj *) + +(* is_type_checked uri cookingsno *) +(*CSC commento falso ed obsoleto *) +(* returns (true,object) if the object has been type-checked *) +(* otherwise it returns (false,object) and freeze the object for *) +(* type-checking *) +(* set_type_checking_info must be called to unfreeze the object *) +val is_type_checked : UriManager.uri -> int -> type_checked_obj + +(* set_type_checking_info uri *) +(* must be called once the type-checking of uri is finished *) +(* The object whose uri is uri is unfreezed and won't be type-checked *) +(* again in the future (is_type_checked will return true) *) +val set_type_checking_info : UriManager.uri -> unit + +(* get_cooked_obj uri cookingsno *) +val get_cooked_obj : UriManager.uri -> int -> Cic.obj + +(* set_cooking_function cooking_function *) +val set_cooking_function : + (Cic.obj -> UriManager.uri -> (int * Cic.obj) list) -> unit diff --git a/helm/ocaml/cic_proof_checking/cicMiniReduction.ml b/helm/ocaml/cic_proof_checking/cicMiniReduction.ml new file mode 100644 index 000000000..cb5875f73 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicMiniReduction.ml @@ -0,0 +1,60 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +let rec letin_nf = + let module C = Cic in + function + C.Rel _ as t -> t + | C.Var _ as t -> t + | C.Meta _ as t -> t + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (letin_nf te, letin_nf ty) + | C.Prod (n,s,t) -> C.Prod (n, letin_nf s, letin_nf t) + | C.Lambda (n,s,t) -> C.Lambda (n, letin_nf s, letin_nf t) + | C.LetIn (n,s,t) -> CicSubstitution.subst (letin_nf s) t + | C.Appl l -> C.Appl (List.map letin_nf l) + | C.Const _ as t -> t + | C.Abst _ as t -> t + | C.MutInd _ as t -> t + | C.MutConstruct _ as t -> t + | C.MutCase (sp,cookingsno,i,outt,t,pl) -> + C.MutCase (sp,cookingsno,i,letin_nf outt, letin_nf t, + List.map letin_nf pl) + | C.Fix (i,fl) -> + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, letin_nf ty, letin_nf bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, letin_nf ty, letin_nf bo)) + fl + in + C.CoFix (i, substitutedfl) +;; diff --git a/helm/ocaml/cic_proof_checking/cicMiniReduction.mli b/helm/ocaml/cic_proof_checking/cicMiniReduction.mli new file mode 100644 index 000000000..c923c6acf --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicMiniReduction.mli @@ -0,0 +1,26 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val letin_nf : Cic.term -> Cic.term diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml new file mode 100644 index 000000000..fafbd8848 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -0,0 +1,211 @@ +(* 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 implements a very simple Coq-like pretty printer that, given *) +(* an object of cic (internal representation) returns a string describing the *) +(* object in a syntax similar to that of coq *) +(* *) +(******************************************************************************) + +exception CicPpInternalError;; + +(* Utility functions *) + +let string_of_name = + function + Cic.Name s -> s + | Cic.Anonimous -> "_" +;; + +(* get_nth l n returns the nth element of the list l if it exists or raise *) +(* a CicPpInternalError if l has less than n elements or n < 1 *) +let rec get_nth l n = + match (n,l) with + (1, he::_) -> he + | (n, he::tail) when n > 1 -> get_nth tail (n-1) + | (_,_) -> raise CicPpInternalError +;; + +(* pp t l *) +(* pretty-prints a term t of cic in an environment l where l is a list of *) +(* identifier names used to resolve DeBrujin indexes. The head of l is the *) +(* name associated to the greatest DeBrujin index in t *) +let rec pp t l = + let module C = Cic in + match t with + C.Rel n -> + (match get_nth l n with + C.Name s -> s + | _ -> raise CicPpInternalError + ) + | C.Var uri -> UriManager.name_of_uri uri + | C.Meta n -> "?" ^ (string_of_int n) + | C.Sort s -> + (match s with + C.Prop -> "Prop" + | C.Set -> "Set" + | C.Type -> "Type" + ) + | C.Implicit -> "?" + | C.Prod (b,s,t) -> + (match b with + C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t (b::l) + | C.Anonimous -> "(" ^ pp s l ^ "->" ^ pp t (b::l) ^ ")" + ) + | C.Cast (v,t) -> pp v l + | C.Lambda (b,s,t) -> + "[" ^ string_of_name b ^ ":" ^ pp s l ^ "]" ^ pp t (b::l) + | C.LetIn (b,s,t) -> + "[" ^ string_of_name b ^ ":=" ^ pp s l ^ "]" ^ pp t (b::l) + | C.Appl li -> + "(" ^ + (List.fold_right + (fun x i -> pp x l ^ (match i with "" -> "" | _ -> " ") ^ i) + li "" + ) ^ ")" + | C.Const (uri,_) -> UriManager.name_of_uri uri + | C.Abst uri -> UriManager.name_of_uri uri + | C.MutInd (uri,_,n) -> + (match CicEnvironment.get_obj uri with + C.InductiveDefinition (dl,_,_) -> + let (name,_,_,_) = get_nth dl (n+1) in + name + | _ -> raise CicPpInternalError + ) + | C.MutConstruct (uri,_,n1,n2) -> + (match CicEnvironment.get_obj uri with + C.InductiveDefinition (dl,_,_) -> + let (_,_,_,cons) = get_nth dl (n1+1) in + let (id,_,_) = get_nth cons n2 in + id + | _ -> raise CicPpInternalError + ) + | C.MutCase (uri,_,n1,ty,te,patterns) -> + let connames = + (match CicEnvironment.get_obj uri with + C.InductiveDefinition (dl,_,_) -> + let (_,_,_,cons) = get_nth dl (n1+1) in + List.map (fun (id,_,_) -> id) cons + | _ -> raise CicPpInternalError + ) + in + "\n<" ^ pp ty l ^ ">Cases " ^ pp te l ^ " of " ^ + List.fold_right (fun (x,y) i -> "\n " ^ x ^ " => " ^ pp y l ^ i) + (List.combine connames patterns) "" ^ + "\nend" + | C.Fix (no, funs) -> + let snames = List.map (fun (name,_,_,_) -> name) funs in + let names = List.rev (List.map (function name -> C.Name name) snames) in + "\nFix " ^ get_nth snames (no + 1) ^ " {" ^ + List.fold_right + (fun (name,ind,ty,bo) i -> "\n" ^ name ^ " / " ^ string_of_int ind ^ + " : " ^ pp ty l ^ " := \n" ^ + pp bo (names@l) ^ i) + funs "" ^ + "}\n" + | C.CoFix (no,funs) -> + let snames = List.map (fun (name,_,_) -> name) funs in + let names = List.rev (List.map (function name -> C.Name name) snames) in + "\nCoFix " ^ get_nth snames (no + 1) ^ " {" ^ + List.fold_right + (fun (name,ty,bo) i -> "\n" ^ name ^ + " : " ^ pp ty l ^ " := \n" ^ + pp bo (names@l) ^ i) + funs "" ^ + "}\n" +;; + +(* ppinductiveType (typename, inductive, arity, cons) names *) +(* pretty-prints a single inductive definition (typename, inductive, arity, *) +(* cons) where the cic terms in the inductive definition need to be *) +(* evaluated in the environment names that is the list of typenames of the *) +(* mutual inductive definitions defined in the block of mutual inductive *) +(* definitions to which this one belongs to *) +let ppinductiveType (typename, inductive, arity, cons) names = + (if inductive then "\nInductive " else "\nCoInductive ") ^ typename ^ ": " ^ + (*CSC: bug found: was pp arity names ^ " =\n " ^*) + pp arity [] ^ " =\n " ^ + List.fold_right + (fun (id,ty,_) i -> id ^ " : " ^ pp ty names ^ + (if i = "" then "\n" else "\n | ") ^ i) + cons "" +;; + +(* ppobj obj returns a string with describing the cic object obj in a syntax *) +(* similar to the one used by Coq *) +let ppobj obj = + let module C = Cic in + let module U = UriManager in + match obj with + C.Definition (id, t1, t2, params) -> + "Definition of " ^ id ^ + "(" ^ + List.fold_right + (fun (_,x) i -> + List.fold_right + (fun x i -> + U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i' + ) x "" ^ match i with "" -> "" | i' -> " " ^ i' + ) params "" ^ ")" ^ + ":\n" ^ pp t1 [] ^ " : " ^ pp t2 [] + | C.Axiom (id, ty, params) -> + "Axiom " ^ id ^ "(" ^ + List.fold_right + (fun (_,x) i -> + List.fold_right + (fun x i -> + U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i' + ) x "" ^ match i with "" -> "" | i' -> " " ^ i' + ) params "" ^ + "):\n" ^ pp ty [] + | C.Variable (name, bo, ty) -> + "Variable " ^ name ^ ":\n" ^ pp ty [] ^ "\n" ^ + (match bo with None -> "" | Some bo -> ":= " ^ pp bo []) + | C.CurrentProof (name, conjectures, value, ty) -> + "Current Proof:\n" ^ + List.fold_right + (fun (n, t) i -> "?" ^ (string_of_int n) ^ ": " ^ pp t [] ^ "\n" ^ i) + conjectures "" ^ + "\n" ^ pp value [] ^ " : " ^ pp ty [] + | C.InductiveDefinition (l, params, nparams) -> + "Parameters = " ^ + List.fold_right + (fun (_,x) i -> + List.fold_right + (fun x i -> + U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i' + ) x "" ^ match i with "" -> "" | i' -> " " ^ i' + ) params "" ^ "\n" ^ + "NParams = " ^ string_of_int nparams ^ "\n" ^ + let names = List.rev (List.map (fun (n,_,_,_) -> C.Name n) l) in + List.fold_right (fun x i -> ppinductiveType x names ^ i) l "" +;; diff --git a/helm/ocaml/cic_proof_checking/cicPp.mli b/helm/ocaml/cic_proof_checking/cicPp.mli new file mode 100644 index 000000000..99757d186 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicPp.mli @@ -0,0 +1,41 @@ +(* 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 implements a very simple Coq-like pretty printer that, given *) +(* an object of cic (internal representation) returns a string describing the *) +(* object in a syntax similar to that of coq *) +(* *) +(******************************************************************************) + +(* ppobj obj returns a string with describing the cic object obj in a syntax *) +(* similar to the one used by Coq *) +val ppobj : Cic.obj -> string diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml new file mode 100644 index 000000000..285e660a8 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicReduction.ml @@ -0,0 +1,278 @@ +(* 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 CicReductionInternalError;; +exception WrongUriToInductiveDefinition;; + +let fdebug = ref 1;; +let debug t env s = + let rec debug_aux t i = + let module C = Cic in + let module U = UriManager in + CicPp.ppobj (C.Variable ("DEBUG", None, + C.Prod (C.Name "-9", C.Const (U.uri_of_string "cic:/dummy-9",0), + C.Prod (C.Name "-8", C.Const (U.uri_of_string "cic:/dummy-8",0), + C.Prod (C.Name "-7", C.Const (U.uri_of_string "cic:/dummy-7",0), + C.Prod (C.Name "-6", C.Const (U.uri_of_string "cic:/dummy-6",0), + C.Prod (C.Name "-5", C.Const (U.uri_of_string "cic:/dummy-5",0), + C.Prod (C.Name "-4", C.Const (U.uri_of_string "cic:/dummy-4",0), + C.Prod (C.Name "-3", C.Const (U.uri_of_string "cic:/dummy-3",0), + C.Prod (C.Name "-2", C.Const (U.uri_of_string "cic:/dummy-2",0), + C.Prod (C.Name "-1", C.Const (U.uri_of_string "cic:/dummy-1",0), + t + ) + ) + ) + ) + ) + ) + ) + ) + ) + )) ^ "\n" ^ i + in + if !fdebug = 0 then + begin + print_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") ; + flush stdout + end +;; + +exception Impossible of int;; +exception ReferenceToDefinition;; +exception ReferenceToAxiom;; +exception ReferenceToVariable;; +exception ReferenceToCurrentProof;; +exception ReferenceToInductiveDefinition;; + +(* takes a well-typed term *) +let whd = + let rec whdaux l = + let module C = Cic in + let module S = CicSubstitution in + function + C.Rel _ as t -> if l = [] then t else C.Appl (t::l) + | C.Var _ as t -> if l = [] then t else C.Appl (t::l) + | C.Meta _ as t -> if l = [] then t else C.Appl (t::l) + | C.Sort _ as t -> t (* l should be empty *) + | C.Implicit as t -> t + | C.Cast (te,ty) -> whdaux l te (*CSC E' GIUSTO BUTTARE IL CAST? *) + | C.Prod _ as t -> t (* l should be empty *) + | C.Lambda (name,s,t) as t' -> + (match l with + [] -> t' + | he::tl -> whdaux tl (S.subst he t) + (* when name is Anonimous the substitution should be superfluous *) + ) + | C.Appl (he::tl) -> whdaux (tl@l) he + | C.Appl [] -> raise (Impossible 1) + | C.Const (uri,cookingsno) as t -> + (match CicEnvironment.get_cooked_obj uri cookingsno with + C.Definition (_,body,_,_) -> whdaux l body + | C.Axiom _ -> if l = [] then t else C.Appl (t::l) + (*CSC: Prossima riga sbagliata: Var punta alle variabili, non Const *) + | C.Variable _ -> if l = [] then t else C.Appl (t::l) + | C.CurrentProof (_,_,body,_) -> whdaux l body + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + ) + | C.Abst _ as t -> t (*CSC l should be empty ????? *) + | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l) + | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l) + | C.MutCase (mutind,cookingsno,i,_,term,pl) as t -> + let decofix = + function + C.CoFix (i,fl) as t -> + let (_,_,body) = List.nth fl i in + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + whdaux [] body' + | C.Appl (C.CoFix (i,fl) :: tl) -> + let (_,_,body) = List.nth fl i in + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + whdaux tl body' + | t -> t + in + (match decofix (whdaux [] term) with + C.MutConstruct (_,_,_,j) -> whdaux l (List.nth pl (j-1)) + | C.Appl (C.MutConstruct (_,_,_,j) :: tl) -> + let (arity, r, num_ingredients) = + match CicEnvironment.get_obj mutind with + C.InductiveDefinition (tl,ingredients,r) -> + let (_,_,arity,_) = List.nth tl i + and num_ingredients = + List.fold_right + (fun (k,l) i -> + if k < cookingsno then i + List.length l else i + ) ingredients 0 + in + (arity,r,num_ingredients) + | _ -> raise WrongUriToInductiveDefinition + in + let ts = + let num_to_eat = r + num_ingredients in + let rec eat_first = + function + (0,l) -> l + | (n,he::tl) when n > 0 -> eat_first (n - 1, tl) + | _ -> raise (Impossible 5) + in + eat_first (num_to_eat,tl) + in + whdaux (ts@l) (List.nth pl (j-1)) + | C.Abst _| C.Cast _ | C.Implicit -> + raise (Impossible 2) (* we don't trust our whd ;-) *) + | _ -> t + ) + | C.Fix (i,fl) as t -> + let (_,recindex,_,body) = List.nth fl i in + let recparam = + try + Some (List.nth l recindex) + with + _ -> None + in + (match recparam with + Some recparam -> + (match whdaux [] recparam with + C.MutConstruct _ + | C.Appl ((C.MutConstruct _)::_) -> + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl))) + fl + body + in + (* Possible optimization: substituting whd recparam in l *) + whdaux l body' + | _ -> if l = [] then t else C.Appl (t::l) + ) + | None -> if l = [] then t else C.Appl (t::l) + ) + | C.CoFix (i,fl) as t -> + (*CSC vecchio codice + let (_,_,body) = List.nth fl i in + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + whdaux l body' + *) + if l = [] then t else C.Appl (t::l) + in + whdaux [] +;; + +(* t1, t2 must be well-typed *) +let are_convertible t1 t2 = + let module U = UriManager in + let rec aux t1 t2 = + debug t1 [t2] "PREWHD"; + (* this trivial euristic cuts down the total time of about five times ;-) *) + (* this because most of the time t1 and t2 are "sintactically" the same *) + if t1 = t2 then + true + else + begin + let module C = Cic in + let t1' = whd t1 + and t2' = whd t2 in + debug t1' [t2'] "POSTWHD"; + (*if !fdebug = 0 then ignore(Unix.system "read" );*) + match (t1',t2') with + (C.Rel n1, C.Rel n2) -> n1 = n2 + | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2 + | (C.Meta n1, C.Meta n2) -> n1 = n2 + | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *) + | (C.Prod (_,s1,t1), C.Prod(_,s2,t2)) -> + aux s1 s2 && aux t1 t2 + | (C.Lambda (_,s1,t1), C.Lambda(_,s2,t2)) -> + aux s1 s2 && aux t1 t2 + | (C.Appl l1, C.Appl l2) -> + (try + List.fold_right2 (fun x y b -> aux x y && b) l1 l2 true + with + Invalid_argument _ -> false + ) + | (C.Const (uri1,_), C.Const (uri2,_)) -> + (*CSC: questo commento e' chiaro o delirante? Io lo sto scrivendo *) + (*CSC: mentre sono delirante, quindi ... *) + (* WARNING: it is really important that the two cookingsno are not *) + (* checked for equality. This allows not to cook an object with no *) + (* ingredients only to update the cookingsno. E.g: if a term t has *) + (* a reference to a term t1 which does not depend on any variable *) + (* and t1 depends on a term t2 (that can't depend on any variable *) + (* because of t1), then t1 cooked at every level could be the same *) + (* as t1 cooked at level 0. Doing so, t2 will be extended in t *) + (* with cookingsno 0 and not 2. But this will not cause any trouble*) + (* if here we don't check that the two cookingsno are equal. *) + U.eq uri1 uri2 + | (C.MutInd (uri1,k1,i1), C.MutInd (uri2,k2,i2)) -> + (* WARNIG: see the previous warning *) + U.eq uri1 uri2 && i1 = i2 + | (C.MutConstruct (uri1,_,i1,j1), C.MutConstruct (uri2,_,i2,j2)) -> + (* WARNIG: see the previous warning *) + U.eq uri1 uri2 && i1 = i2 && j1 = j2 + | (C.MutCase (uri1,_,i1,outtype1,term1,pl1), + C.MutCase (uri2,_,i2,outtype2,term2,pl2)) -> + (* WARNIG: see the previous warning *) + (* aux outtype1 outtype2 should be true if aux pl1 pl2 *) + U.eq uri1 uri2 && i1 = i2 && aux outtype1 outtype2 && + aux term1 term2 && + List.fold_right2 (fun x y b -> b && aux x y) pl1 pl2 true + | (C.Fix (i1,fl1), C.Fix (i2,fl2)) -> + i1 = i2 && + List.fold_right2 + (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b -> + b && recindex1 = recindex2 && aux ty1 ty2 && aux bo1 bo2) + fl1 fl2 true + | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) -> + i1 = i2 && + List.fold_right2 + (fun (_,ty1,bo1) (_,ty2,bo2) b -> + b && aux ty1 ty2 && aux bo1 bo2) + fl1 fl2 true + | (C.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _) + | (C.Implicit, _) | (_, C.Implicit) -> + raise (Impossible 3) (* we don't trust our whd ;-) *) + | (_,_) -> false + end + in + aux t1 t2 +;; diff --git a/helm/ocaml/cic_proof_checking/cicReduction.mli b/helm/ocaml/cic_proof_checking/cicReduction.mli new file mode 100644 index 000000000..d61bc7251 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicReduction.mli @@ -0,0 +1,34 @@ +(* 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 WrongUriToInductiveDefinition +exception ReferenceToDefinition +exception ReferenceToAxiom +exception ReferenceToVariable +exception ReferenceToCurrentProof +exception ReferenceToInductiveDefinition +val fdebug : int ref +val whd : Cic.term -> Cic.term +val are_convertible : Cic.term -> Cic.term -> bool diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml new file mode 100644 index 000000000..28dbe24e3 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml @@ -0,0 +1,142 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +let lift n = + let rec liftaux k = + let module C = Cic in + function + C.Rel m -> + if m < k then + C.Rel m + else + C.Rel (m + n) + | C.Var _ as t -> t + | C.Meta _ as t -> t + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty) + | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t) + | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t) + | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t) + | C.Appl l -> C.Appl (List.map (liftaux k) l) + | C.Const _ as t -> t + | C.Abst _ as t -> t + | C.MutInd _ as t -> t + | C.MutConstruct _ as t -> t + | C.MutCase (sp,cookingsno,i,outty,t,pl) -> + C.MutCase (sp, cookingsno, i, liftaux k outty, liftaux k t, + List.map (liftaux k) pl) + | C.Fix (i, fl) -> + let len = List.length fl in + let liftedfl = + List.map + (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo)) + fl + in + C.Fix (i, liftedfl) + | C.CoFix (i, fl) -> + let len = List.length fl in + let liftedfl = + List.map + (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo)) + fl + in + C.CoFix (i, liftedfl) + in + liftaux 1 +;; + +let subst arg = + let rec substaux k = + let module C = Cic in + function + C.Rel n as t -> + (match n with + n when n = k -> lift (k - 1) arg + | n when n < k -> t + | _ -> C.Rel (n - 1) + ) + | C.Var _ as t -> t + | C.Meta _ as t -> t + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) (*CSC ??? *) + | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t) + | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t) + | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t) + | C.Appl l -> C.Appl (List.map (substaux k) l) + | C.Const _ as t -> t + | C.Abst _ as t -> t + | C.MutInd _ as t -> t + | C.MutConstruct _ as t -> t + | C.MutCase (sp,cookingsno,i,outt,t,pl) -> + C.MutCase (sp,cookingsno,i,substaux k outt, substaux k t, + List.map (substaux k) pl) + | C.Fix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo)) + fl + in + C.CoFix (i, substitutedfl) + in + substaux 1 +;; + +let undebrujin_inductive_def uri = + function + Cic.InductiveDefinition (dl,params,n_ind_params) -> + let dl' = + List.map + (fun (name,inductive,arity,constructors) -> + let constructors' = + List.map + (fun (name,ty,r) -> + let ty' = + let counter = ref (List.length dl) in + List.fold_right + (fun _ -> + decr counter ; + subst (Cic.MutInd (uri,0,!counter)) + ) dl ty + in + (name,ty',r) + ) constructors + in + (name,inductive,arity,constructors') + ) dl + in + Cic.InductiveDefinition (dl', params, n_ind_params) + | obj -> obj +;; diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli new file mode 100644 index 000000000..72e9a32c2 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.mli @@ -0,0 +1,28 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val lift : int -> Cic.term -> Cic.term +val subst : Cic.term -> Cic.term -> Cic.term +val undebrujin_inductive_def : UriManager.uri -> Cic.obj -> Cic.obj diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml new file mode 100644 index 000000000..2ccc1e743 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -0,0 +1,1289 @@ +(* 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 NotImplemented;; +exception Impossible;; +exception NotWellTyped of string;; +exception WrongUriToConstant of string;; +exception WrongUriToVariable of string;; +exception WrongUriToMutualInductiveDefinitions of string;; +exception ListTooShort;; +exception NotPositiveOccurrences of string;; +exception NotWellFormedTypeOfInductiveConstructor of string;; +exception WrongRequiredArgument of string;; + +let log = + let module U = UriManager in + let indent = ref 0 in + function + `Start_type_checking uri -> + print_string ( + (String.make !indent ' ') ^ + "
" ^ + "Type-Checking of " ^ (U.string_of_uri uri) ^ " started
\n" + ) ; + flush stdout ; + incr indent + | `Type_checking_completed uri -> + decr indent ; + print_string ( + (String.make !indent ' ') ^ + "
" ^ + "Type-Checking of " ^ (U.string_of_uri uri) ^ " completed.
\n" + ) ; + flush stdout +;; + +let fdebug = ref 0;; +let debug t env = + let rec debug_aux t i = + let module C = Cic in + let module U = UriManager in + CicPp.ppobj (C.Variable ("DEBUG", None, + C.Prod (C.Name "-15", C.Const (U.uri_of_string "cic:/dummy-15",0), + C.Prod (C.Name "-14", C.Const (U.uri_of_string "cic:/dummy-14",0), + C.Prod (C.Name "-13", C.Const (U.uri_of_string "cic:/dummy-13",0), + C.Prod (C.Name "-12", C.Const (U.uri_of_string "cic:/dummy-12",0), + C.Prod (C.Name "-11", C.Const (U.uri_of_string "cic:/dummy-11",0), + C.Prod (C.Name "-10", C.Const (U.uri_of_string "cic:/dummy-10",0), + C.Prod (C.Name "-9", C.Const (U.uri_of_string "cic:/dummy-9",0), + C.Prod (C.Name "-8", C.Const (U.uri_of_string "cic:/dummy-8",0), + C.Prod (C.Name "-7", C.Const (U.uri_of_string "cic:/dummy-7",0), + C.Prod (C.Name "-6", C.Const (U.uri_of_string "cic:/dummy-6",0), + C.Prod (C.Name "-5", C.Const (U.uri_of_string "cic:/dummy-5",0), + C.Prod (C.Name "-4", C.Const (U.uri_of_string "cic:/dummy-4",0), + C.Prod (C.Name "-3", C.Const (U.uri_of_string "cic:/dummy-3",0), + C.Prod (C.Name "-2", C.Const (U.uri_of_string "cic:/dummy-2",0), + C.Prod (C.Name "-1", C.Const (U.uri_of_string "cic:/dummy-1",0), + t + ) + ) + ) + ) + ) + ) + ) + ) + ))))))) + )) ^ "\n" ^ i + in + if !fdebug = 0 then + raise (NotWellTyped ("\n" ^ List.fold_right debug_aux (t::env) "")) + (*print_endline ("\n" ^ List.fold_right debug_aux (t::env) "") ; flush stdout*) +;; + +let rec split l n = + match (l,n) with + (l,0) -> ([], l) + | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2) + | (_,_) -> raise ListTooShort +;; + +exception CicEnvironmentError;; + +let rec cooked_type_of_constant uri cookingsno = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let cobj = + match CicEnvironment.is_type_checked uri cookingsno with + CicEnvironment.CheckedObj cobj -> cobj + | CicEnvironment.UncheckedObj uobj -> + log (`Start_type_checking uri) ; + (* let's typecheck the uncooked obj *) + (match uobj with + C.Definition (_,te,ty,_) -> + let _ = type_of ty in + if not (R.are_convertible (type_of te) ty) then + raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri))) + | C.Axiom (_,ty,_) -> + (* only to check that ty is well-typed *) + let _ = type_of ty in () + | C.CurrentProof (_,_,te,ty) -> + let _ = type_of ty in + if not (R.are_convertible (type_of te) ty) then + raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri))) + | _ -> raise (WrongUriToConstant (U.string_of_uri uri)) + ) ; + CicEnvironment.set_type_checking_info uri ; + log (`Type_checking_completed uri) ; + match CicEnvironment.is_type_checked uri cookingsno with + CicEnvironment.CheckedObj cobj -> cobj + | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError + in + match cobj with + C.Definition (_,_,ty,_) -> ty + | C.Axiom (_,ty,_) -> ty + | C.CurrentProof (_,_,_,ty) -> ty + | _ -> raise (WrongUriToConstant (U.string_of_uri uri)) + +and type_of_variable uri = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + (* 0 because a variable is never cooked => no partial cooking at one level *) + match CicEnvironment.is_type_checked uri 0 with + CicEnvironment.CheckedObj (C.Variable (_,_,ty)) -> ty + | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty)) -> + log (`Start_type_checking uri) ; + (* only to check that ty is well-typed *) + let _ = type_of ty in + (match bo with + None -> () + | Some bo -> + if not (R.are_convertible (type_of bo) ty) then + raise (NotWellTyped ("Variable " ^ (U.string_of_uri uri))) + ) ; + CicEnvironment.set_type_checking_info uri ; + log (`Type_checking_completed uri) ; + ty + | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) + +and does_not_occur n nn te = + let module C = Cic in + (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *) + (*CSC: venga mangiata durante la whd sembra presentare problemi di *) + (*CSC: universi *) + match CicReduction.whd te with + C.Rel m when m > n && m <= nn -> false + | C.Rel _ + | C.Var _ + | C.Meta _ + | C.Sort _ + | C.Implicit -> true + | C.Cast (te,ty) -> does_not_occur n nn te && does_not_occur n nn ty + | C.Prod (_,so,dest) -> + does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest + | C.Lambda (_,so,dest) -> + does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest + | C.LetIn (_,so,dest) -> + does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest + | C.Appl l -> + List.fold_right (fun x i -> i && does_not_occur n nn x) l true + | C.Const _ + | C.Abst _ + | C.MutInd _ + | C.MutConstruct _ -> true + | C.MutCase (_,_,_,out,te,pl) -> + does_not_occur n nn out && does_not_occur n nn te && + List.fold_right (fun x i -> i && does_not_occur n nn x) pl true + | C.Fix (_,fl) -> + let len = List.length fl in + let n_plus_len = n + len in + let nn_plus_len = nn + len in + List.fold_right + (fun (_,_,ty,bo) i -> + i && does_not_occur n_plus_len nn_plus_len ty && + does_not_occur n_plus_len nn_plus_len bo + ) fl true + | C.CoFix (_,fl) -> + let len = List.length fl in + let n_plus_len = n + len in + let nn_plus_len = nn + len in + List.fold_right + (fun (_,ty,bo) i -> + i && does_not_occur n_plus_len nn_plus_len ty && + does_not_occur n_plus_len nn_plus_len bo + ) fl true + +(*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *) +(*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *) +(*CSC dei controlli leggermente diversi. Viene invocata solamente dalla *) +(*CSC strictly_positive *) +(*CSC definizione (giusta???) tratta dalla mail di Hugo ;-) *) +and weakly_positive n nn uri te = + let module C = Cic in + (*CSC mettere in cicSubstitution *) + let rec subst_inductive_type_with_dummy_rel = + function + C.MutInd (uri',_,0) when UriManager.eq uri' uri -> + C.Rel 0 (* dummy rel *) + | C.Appl ((C.MutInd (uri',_,0))::tl) when UriManager.eq uri' uri -> + C.Rel 0 (* dummy rel *) + | C.Cast (te,ty) -> subst_inductive_type_with_dummy_rel te + | C.Prod (name,so,ta) -> + C.Prod (name, subst_inductive_type_with_dummy_rel so, + subst_inductive_type_with_dummy_rel ta) + | C.Lambda (name,so,ta) -> + C.Lambda (name, subst_inductive_type_with_dummy_rel so, + subst_inductive_type_with_dummy_rel ta) + | C.Appl tl -> + C.Appl (List.map subst_inductive_type_with_dummy_rel tl) + | C.MutCase (uri,cookingsno,i,outtype,term,pl) -> + C.MutCase (uri,cookingsno,i, + subst_inductive_type_with_dummy_rel outtype, + subst_inductive_type_with_dummy_rel term, + List.map subst_inductive_type_with_dummy_rel pl) + | C.Fix (i,fl) -> + C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i, + subst_inductive_type_with_dummy_rel ty, + subst_inductive_type_with_dummy_rel bo)) fl) + | C.CoFix (i,fl) -> + C.CoFix (i,List.map (fun (name,ty,bo) -> (name, + subst_inductive_type_with_dummy_rel ty, + subst_inductive_type_with_dummy_rel bo)) fl) + | t -> t + in + match CicReduction.whd te with + C.Appl ((C.MutInd (uri',_,0))::tl) when UriManager.eq uri' uri -> true + | C.MutInd (uri',_,0) when UriManager.eq uri' uri -> true + | C.Prod (C.Anonimous,source,dest) -> + strictly_positive n nn (subst_inductive_type_with_dummy_rel source) && + weakly_positive (n + 1) (nn + 1) uri dest + | C.Prod (name,source,dest) when does_not_occur 0 n dest -> + (* dummy abstraction, so we behave as in the anonimous case *) + strictly_positive n nn (subst_inductive_type_with_dummy_rel source) && + weakly_positive (n + 1) (nn + 1) uri dest + | C.Prod (_,source,dest) -> + does_not_occur n nn (subst_inductive_type_with_dummy_rel source) && + weakly_positive (n + 1) (nn + 1) uri dest + | _ -> raise (NotWellFormedTypeOfInductiveConstructor ("Guess where the error is ;-)")) + +(* instantiate_parameters ps (x1:T1)...(xn:Tn)C *) +(* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *) +and instantiate_parameters params c = + let module C = Cic in + match (c,params) with + (c,[]) -> c + | (C.Prod (_,_,ta), he::tl) -> + instantiate_parameters tl + (CicSubstitution.subst he ta) + | (C.Cast (te,_), _) -> instantiate_parameters params te + | (t,l) -> raise Impossible + +and strictly_positive n nn te = + let module C = Cic in + let module U = UriManager in + match CicReduction.whd te with + C.Rel _ -> true + | C.Cast (te,ty) -> + (*CSC: bisogna controllare ty????*) + strictly_positive n nn te + | C.Prod (_,so,ta) -> + does_not_occur n nn so && + strictly_positive (n+1) (nn+1) ta + | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> + List.fold_right (fun x i -> i && does_not_occur n nn x) tl true + | C.Appl ((C.MutInd (uri,_,i))::tl) -> + let (ok,paramsno,cl) = + match CicEnvironment.get_obj uri with + C.InductiveDefinition (tl,_,paramsno) -> + let (_,_,_,cl) = List.nth tl i in + (List.length tl = 1, paramsno, cl) + | _ -> raise(WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) + in + let (params,arguments) = split tl paramsno in + let lifted_params = List.map (CicSubstitution.lift 1) params in + let cl' = + List.map (fun (_,te,_) -> instantiate_parameters lifted_params te) cl + in + ok && + List.fold_right + (fun x i -> i && does_not_occur n nn x) + arguments true && + (*CSC: MEGAPATCH3 (sara' quella giusta?)*) + List.fold_right + (fun x i -> + i && + weakly_positive (n+1) (nn+1) uri x + ) cl' true + | C.MutInd (uri,_,i) -> + (match CicEnvironment.get_obj uri with + C.InductiveDefinition (tl,_,_) -> + List.length tl = 1 + | _ -> raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) + ) + | t -> does_not_occur n nn t + +(*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *) +and are_all_occurrences_positive uri indparamsno i n nn te = + let module C = Cic in + match CicReduction.whd te with + C.Appl ((C.Rel m)::tl) when m = i -> + (*CSC: riscrivere fermandosi a 0 *) + (* let's check if the inductive type is applied at least to *) + (* indparamsno parameters *) + let last = + List.fold_left + (fun k x -> + if k = 0 then 0 + else + match CicReduction.whd x with + C.Rel m when m = n - (indparamsno - k) -> k - 1 + | _ -> raise (WrongRequiredArgument (UriManager.string_of_uri uri)) + ) indparamsno tl + in + if last = 0 then + List.fold_right (fun x i -> i && does_not_occur n nn x) tl true + else + raise (WrongRequiredArgument (UriManager.string_of_uri uri)) + | C.Rel m when m = i -> + if indparamsno = 0 then + true + else + raise (WrongRequiredArgument (UriManager.string_of_uri uri)) + | C.Prod (C.Anonimous,source,dest) -> + strictly_positive n nn source && + are_all_occurrences_positive uri indparamsno (i+1) (n + 1) (nn + 1) dest + | C.Prod (name,source,dest) when does_not_occur 0 n dest -> + (* dummy abstraction, so we behave as in the anonimous case *) + strictly_positive n nn source && + are_all_occurrences_positive uri indparamsno (i+1) (n + 1) (nn + 1) dest + | C.Prod (_,source,dest) -> + does_not_occur n nn source && + are_all_occurrences_positive uri indparamsno (i+1) (n + 1) (nn + 1) dest + | _ -> raise (NotWellFormedTypeOfInductiveConstructor (UriManager.string_of_uri uri)) + +(*CSC: cambiare il nome, torna unit! *) +and cooked_mutual_inductive_defs uri = + let module U = UriManager in + function + Cic.InductiveDefinition (itl, _, indparamsno) -> + (* let's check if the arity of the inductive types are well *) + (* formed *) + List.iter (fun (_,_,x,_) -> let _ = type_of x in ()) itl ; + + (* let's check if the types of the inductive constructors *) + (* are well formed. *) + (* In order not to use type_of_aux we put the types of the *) + (* mutual inductive types at the head of the types of the *) + (* constructors using Prods *) + (*CSC: piccola??? inefficienza *) + let len = List.length itl in + let _ = + List.fold_right + (fun (_,_,_,cl) i -> + List.iter + (fun (name,te,r) -> + let augmented_term = + List.fold_right + (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i)) + itl te + in + let _ = type_of augmented_term in + (* let's check also the positivity conditions *) + if not (are_all_occurrences_positive uri indparamsno i 0 len te) + then + raise (NotPositiveOccurrences (U.string_of_uri uri)) + else + match !r with + Some _ -> raise Impossible + | None -> r := Some (recursive_args 0 len te) + ) cl ; + (i + 1) + ) itl 1 + in + () + | _ -> + raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + +and cooked_type_of_mutual_inductive_defs uri cookingsno i = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let cobj = + match CicEnvironment.is_type_checked uri cookingsno with + CicEnvironment.CheckedObj cobj -> cobj + | CicEnvironment.UncheckedObj uobj -> + log (`Start_type_checking uri) ; + cooked_mutual_inductive_defs uri uobj ; + CicEnvironment.set_type_checking_info uri ; + log (`Type_checking_completed uri) ; + (match CicEnvironment.is_type_checked uri cookingsno with + CicEnvironment.CheckedObj cobj -> cobj + | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError + ) + in + match cobj with + C.InductiveDefinition (dl,_,_) -> + let (_,_,arity,_) = List.nth dl i in + arity + | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + +and cooked_type_of_mutual_inductive_constr uri cookingsno i j = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let cobj = + match CicEnvironment.is_type_checked uri cookingsno with + CicEnvironment.CheckedObj cobj -> cobj + | CicEnvironment.UncheckedObj uobj -> + log (`Start_type_checking uri) ; + cooked_mutual_inductive_defs uri uobj ; + CicEnvironment.set_type_checking_info uri ; + log (`Type_checking_completed uri) ; + (match CicEnvironment.is_type_checked uri cookingsno with + CicEnvironment.CheckedObj cobj -> cobj + | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError + ) + in + match cobj with + C.InductiveDefinition (dl,_,_) -> + let (_,_,_,cl) = List.nth dl i in + let (_,ty,_) = List.nth cl (j-1) in + ty + | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + +and recursive_args n nn te = + let module C = Cic in + match CicReduction.whd te with + C.Rel _ -> [] + | C.Var _ + | C.Meta _ + | C.Sort _ + | C.Implicit + | C.Cast _ (*CSC ??? *) -> raise Impossible (* due to type-checking *) + | C.Prod (_,so,de) -> + (not (does_not_occur n nn so))::(recursive_args (n+1) (nn + 1) de) + | C.Lambda _ -> raise Impossible (* due to type-checking *) + | C.LetIn _ -> raise NotImplemented + | C.Appl _ -> [] + | C.Const _ + | C.Abst _ -> raise Impossible + | C.MutInd _ + | C.MutConstruct _ + | C.MutCase _ + | C.Fix _ + | C.CoFix _ -> raise Impossible (* due to type-checking *) + +and get_new_safes p c rl safes n nn x = + let module C = Cic in + let module U = UriManager in + let module R = CicReduction in + match (R.whd c, R.whd p, rl) with + (C.Prod (_,_,ta1), C.Lambda (_,_,ta2), b::tl) -> + (* we are sure that the two sources are convertible because we *) + (* have just checked this. So let's go along ... *) + let safes' = + List.map (fun x -> x + 1) safes + in + let safes'' = + if b then 1::safes' else safes' + in + get_new_safes ta2 ta1 tl safes'' (n+1) (nn+1) (x+1) + | (C.MutInd _, e, []) -> (e,safes,n,nn,x) + | (C.Appl _, e, []) -> (e,safes,n,nn,x) + | (_,_,_) -> raise Impossible + +and eat_prods n te = + let module C = Cic in + let module R = CicReduction in + match (n, R.whd te) with + (0, _) -> te + | (n, C.Prod (_,_,ta)) when n > 0 -> eat_prods (n - 1) ta + | (_, _) -> raise Impossible + +and eat_lambdas n te = + let module C = Cic in + let module R = CicReduction in + match (n, R.whd te) with + (0, _) -> (te, 0) + | (n, C.Lambda (_,_,ta)) when n > 0 -> + let (te, k) = eat_lambdas (n - 1) ta in + (te, k + 1) + | (_, _) -> raise Impossible + +(*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) +and check_is_really_smaller_arg n nn kl x safes te = + (*CSC: forse la whd si puo' fare solo quando serve veramente. *) + (*CSC: cfr guarded_by_destructors *) + let module C = Cic in + let module U = UriManager in + match CicReduction.whd te with + C.Rel m when List.mem m safes -> true + | C.Rel _ -> false + | C.Var _ + | C.Meta _ + | C.Sort _ + | C.Implicit + | C.Cast _ +(* | C.Cast (te,ty) -> + check_is_really_smaller_arg n nn kl x safes te && + check_is_really_smaller_arg n nn kl x safes ty*) +(* | C.Prod (_,so,ta) -> + check_is_really_smaller_arg n nn kl x safes so && + check_is_really_smaller_arg (n+1) (nn+1) kl (x+1) + (List.map (fun x -> x + 1) safes) ta*) + | C.Prod _ -> raise Impossible + | C.Lambda (_,so,ta) -> + check_is_really_smaller_arg n nn kl x safes so && + check_is_really_smaller_arg (n+1) (nn+1) kl (x+1) + (List.map (fun x -> x + 1) safes) ta + | C.LetIn (_,so,ta) -> + check_is_really_smaller_arg n nn kl x safes so && + check_is_really_smaller_arg (n+1) (nn+1) kl (x+1) + (List.map (fun x -> x + 1) safes) ta + | C.Appl (he::_) -> + (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *) + (*CSC: solo perche' non abbiamo trovato controesempi *) + check_is_really_smaller_arg n nn kl x safes he + | C.Appl [] -> raise Impossible + | C.Const _ + | C.Abst _ + | C.MutInd _ -> raise Impossible + | C.MutConstruct _ -> false + | C.MutCase (uri,_,i,outtype,term,pl) -> + (match term with + C.Rel m when List.mem m safes || m = x -> + let (isinductive,paramsno,cl) = + match CicEnvironment.get_obj uri with + C.InductiveDefinition (tl,_,paramsno) -> + let (_,isinductive,_,cl) = List.nth tl i in + let cl' = + List.map (fun (id,ty,r) -> (id, eat_prods paramsno ty, r)) cl + in + (isinductive,paramsno,cl') + | _ -> + raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) + in + if not isinductive then + List.fold_right + (fun p i -> i && check_is_really_smaller_arg n nn kl x safes p) + pl true + else + List.fold_right + (fun (p,(_,c,rl)) i -> + let rl' = + match !rl with + Some rl' -> + let (_,rl'') = split rl' paramsno in + rl'' + | None -> raise Impossible + in + let (e,safes',n',nn',x') = + get_new_safes p c rl' safes n nn x + in + i && + check_is_really_smaller_arg n' nn' kl x' safes' e + ) (List.combine pl cl) true + | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> + let (isinductive,paramsno,cl) = + match CicEnvironment.get_obj uri with + C.InductiveDefinition (tl,_,paramsno) -> + let (_,isinductive,_,cl) = List.nth tl i in + let cl' = + List.map (fun (id,ty,r) -> (id, eat_prods paramsno ty, r)) cl + in + (isinductive,paramsno,cl') + | _ -> + raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) + in + if not isinductive then + List.fold_right + (fun p i -> i && check_is_really_smaller_arg n nn kl x safes p) + pl true + else + (*CSC: supponiamo come prima che nessun controllo sia necessario*) + (*CSC: sugli argomenti di una applicazione *) + List.fold_right + (fun (p,(_,c,rl)) i -> + let rl' = + match !rl with + Some rl' -> + let (_,rl'') = split rl' paramsno in + rl'' + | None -> raise Impossible + in + let (e, safes',n',nn',x') = + get_new_safes p c rl' safes n nn x + in + i && + check_is_really_smaller_arg n' nn' kl x' safes' e + ) (List.combine pl cl) true + | _ -> + List.fold_right + (fun p i -> i && check_is_really_smaller_arg n nn kl x safes p) + pl true + ) + | C.Fix (_, fl) -> + let len = List.length fl in + let n_plus_len = n + len + and nn_plus_len = nn + len + and x_plus_len = x + len + and safes' = List.map (fun x -> x + len) safes in + List.fold_right + (fun (_,_,ty,bo) i -> + i && + check_is_really_smaller_arg n_plus_len nn_plus_len kl x_plus_len + safes' bo + ) fl true + | C.CoFix (_, fl) -> + let len = List.length fl in + let n_plus_len = n + len + and nn_plus_len = nn + len + and x_plus_len = x + len + and safes' = List.map (fun x -> x + len) safes in + List.fold_right + (fun (_,ty,bo) i -> + i && + check_is_really_smaller_arg n_plus_len nn_plus_len kl x_plus_len + safes' bo + ) fl true + +and guarded_by_destructors n nn kl x safes = + let module C = Cic in + let module U = UriManager in + function + C.Rel m when m > n && m <= nn -> false + | C.Rel _ + | C.Var _ + | C.Meta _ + | C.Sort _ + | C.Implicit -> true + | C.Cast (te,ty) -> + guarded_by_destructors n nn kl x safes te && + guarded_by_destructors n nn kl x safes ty + | C.Prod (_,so,ta) -> + guarded_by_destructors n nn kl x safes so && + guarded_by_destructors (n+1) (nn+1) kl (x+1) + (List.map (fun x -> x + 1) safes) ta + | C.Lambda (_,so,ta) -> + guarded_by_destructors n nn kl x safes so && + guarded_by_destructors (n+1) (nn+1) kl (x+1) + (List.map (fun x -> x + 1) safes) ta + | C.LetIn (_,so,ta) -> + guarded_by_destructors n nn kl x safes so && + guarded_by_destructors (n+1) (nn+1) kl (x+1) + (List.map (fun x -> x + 1) safes) ta + | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> + let k = List.nth kl (m - n - 1) in + if not (List.length tl > k) then false + else + List.fold_right + (fun param i -> + i && guarded_by_destructors n nn kl x safes param + ) tl true && + check_is_really_smaller_arg n nn kl x safes (List.nth tl k) + | C.Appl tl -> + List.fold_right (fun t i -> i && guarded_by_destructors n nn kl x safes t) + tl true + | C.Const _ + | C.Abst _ + | C.MutInd _ + | C.MutConstruct _ -> true + | C.MutCase (uri,_,i,outtype,term,pl) -> + (match term with + C.Rel m when List.mem m safes || m = x -> + let (isinductive,paramsno,cl) = + match CicEnvironment.get_obj uri with + C.InductiveDefinition (tl,_,paramsno) -> + let (_,isinductive,_,cl) = List.nth tl i in + let cl' = + List.map (fun (id,ty,r) -> (id, eat_prods paramsno ty, r)) cl + in + (isinductive,paramsno,cl') + | _ -> + raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) + in + if not isinductive then + guarded_by_destructors n nn kl x safes outtype && + guarded_by_destructors n nn kl x safes term && + (*CSC: manca ??? il controllo sul tipo di term? *) + List.fold_right + (fun p i -> i && guarded_by_destructors n nn kl x safes p) + pl true + else + guarded_by_destructors n nn kl x safes outtype && + (*CSC: manca ??? il controllo sul tipo di term? *) + List.fold_right + (fun (p,(_,c,rl)) i -> + let rl' = + match !rl with + Some rl' -> + let (_,rl'') = split rl' paramsno in + rl'' + | None -> raise Impossible + in + let (e,safes',n',nn',x') = + get_new_safes p c rl' safes n nn x + in + i && + guarded_by_destructors n' nn' kl x' safes' e + ) (List.combine pl cl) true + | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> + let (isinductive,paramsno,cl) = + match CicEnvironment.get_obj uri with + C.InductiveDefinition (tl,_,paramsno) -> + let (_,isinductive,_,cl) = List.nth tl i in + let cl' = + List.map (fun (id,ty,r) -> (id, eat_prods paramsno ty, r)) cl + in + (isinductive,paramsno,cl') + | _ -> + raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) + in + if not isinductive then + guarded_by_destructors n nn kl x safes outtype && + guarded_by_destructors n nn kl x safes term && + (*CSC: manca ??? il controllo sul tipo di term? *) + List.fold_right + (fun p i -> i && guarded_by_destructors n nn kl x safes p) + pl true + else + guarded_by_destructors n nn kl x safes outtype && + (*CSC: manca ??? il controllo sul tipo di term? *) + List.fold_right + (fun t i -> i && guarded_by_destructors n nn kl x safes t) + tl true && + List.fold_right + (fun (p,(_,c,rl)) i -> + let rl' = + match !rl with + Some rl' -> + let (_,rl'') = split rl' paramsno in + rl'' + | None -> raise Impossible + in + let (e, safes',n',nn',x') = + get_new_safes p c rl' safes n nn x + in + i && + guarded_by_destructors n' nn' kl x' safes' e + ) (List.combine pl cl) true + | _ -> + guarded_by_destructors n nn kl x safes outtype && + guarded_by_destructors n nn kl x safes term && + (*CSC: manca ??? il controllo sul tipo di term? *) + List.fold_right + (fun p i -> i && guarded_by_destructors n nn kl x safes p) + pl true + ) + | C.Fix (_, fl) -> + let len = List.length fl in + let n_plus_len = n + len + and nn_plus_len = nn + len + and x_plus_len = x + len + and safes' = List.map (fun x -> x + len) safes in + List.fold_right + (fun (_,_,ty,bo) i -> + i && guarded_by_destructors n_plus_len nn_plus_len kl x_plus_len + safes' ty && + guarded_by_destructors n_plus_len nn_plus_len kl x_plus_len + safes' bo + ) fl true + | C.CoFix (_, fl) -> + let len = List.length fl in + let n_plus_len = n + len + and nn_plus_len = nn + len + and x_plus_len = x + len + and safes' = List.map (fun x -> x + len) safes in + List.fold_right + (fun (_,ty,bo) i -> + i && guarded_by_destructors n_plus_len nn_plus_len kl x_plus_len + safes' ty && + guarded_by_destructors n_plus_len nn_plus_len kl x_plus_len safes' + bo + ) fl true + +(*CSC h = 0 significa non ancora protetto *) +and guarded_by_constructors n nn h = + let module C = Cic in + function + C.Rel m when m > n && m <= nn -> h = 1 + | C.Rel _ + | C.Var _ + | C.Meta _ + | C.Sort _ + | C.Implicit -> true (*CSC: ma alcuni sono impossibili!!!! vedi Prod *) + | C.Cast (te,ty) -> + guarded_by_constructors n nn h te && + guarded_by_constructors n nn h ty + | C.Prod (_,so,de) -> + raise Impossible (* the term has just been type-checked *) + | C.Lambda (_,so,de) -> + does_not_occur n nn so && + guarded_by_constructors (n + 1) (nn + 1) h de + | C.LetIn (_,so,de) -> + does_not_occur n nn so && + guarded_by_constructors (n + 1) (nn + 1) h de + | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> + h = 1 && + List.fold_right (fun x i -> i && does_not_occur n nn x) tl true + | C.Appl ((C.MutConstruct (uri,cookingsno,i,j))::tl) -> + let (is_coinductive, rl) = + match CicEnvironment.get_cooked_obj uri cookingsno with + C.InductiveDefinition (itl,_,_) -> + let (_,is_inductive,_,cl) = List.nth itl i in + let (_,cons,rrec_args) = List.nth cl (j - 1) in + (match !rrec_args with + None -> raise Impossible + | Some rec_args -> (not is_inductive, rec_args) + ) + | _ -> + raise (WrongUriToMutualInductiveDefinitions + (UriManager.string_of_uri uri)) + in + is_coinductive && + List.fold_right + (fun (x,r) i -> + i && + if r then + guarded_by_constructors n nn 1 x + else + does_not_occur n nn x + ) (List.combine tl rl) true + | C.Appl l -> + List.fold_right (fun x i -> i && does_not_occur n nn x) l true + | C.Const _ + | C.Abst _ + | C.MutInd _ + | C.MutConstruct _ -> true (*CSC: ma alcuni sono impossibili!!!! vedi Prod *) + | C.MutCase (_,_,_,out,te,pl) -> + let rec returns_a_coinductive = + function + (*CSC: per le regole di tipaggio, la chiamata ricorsiva verra' *) + (*CSC: effettata solo una volta, per mangiarsi l'astrazione *) + (*CSC: non dummy *) + C.Lambda (_,_,de) -> returns_a_coinductive de + | C.MutInd (uri,_,i) -> + (*CSC: definire una funzioncina per questo codice sempre replicato *) + (match CicEnvironment.get_obj uri with + C.InductiveDefinition (itl,_,_) -> + let (_,is_inductive,_,_) = List.nth itl i in + not is_inductive + | _ -> + raise (WrongUriToMutualInductiveDefinitions + (UriManager.string_of_uri uri)) + ) + (*CSC: bug nella prossima riga (manca la whd) *) + | C.Appl ((C.MutInd (uri,_,i))::_) -> + (match CicEnvironment.get_obj uri with + C.InductiveDefinition (itl,_,_) -> + let (_,is_inductive,_,_) = List.nth itl i in + not is_inductive + | _ -> + raise (WrongUriToMutualInductiveDefinitions + (UriManager.string_of_uri uri)) + ) + | _ -> false + in + does_not_occur n nn out && + does_not_occur n nn te && + if returns_a_coinductive out then + List.fold_right + (fun x i -> i && guarded_by_constructors n nn h x) pl true + else + List.fold_right (fun x i -> i && does_not_occur n nn x) pl true + | C.Fix (_,fl) -> + let len = List.length fl in + let n_plus_len = n + len + and nn_plus_len = nn + len in + List.fold_right + (fun (_,_,ty,bo) i -> + i && does_not_occur n_plus_len nn_plus_len ty && + does_not_occur n_plus_len nn_plus_len bo + ) fl true + | C.CoFix (_,fl) -> + let len = List.length fl in + let n_plus_len = n + len + and nn_plus_len = nn + len in + List.fold_right + (fun (_,ty,bo) i -> + i && does_not_occur n_plus_len nn_plus_len ty && + does_not_occur n_plus_len nn_plus_len bo + ) fl true + +and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 = + let module C = Cic in + let module U = UriManager in + match (CicReduction.whd arity1, CicReduction.whd arity2) with + (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) + when CicReduction.are_convertible so1 so2 -> + check_allowed_sort_elimination uri i need_dummy + (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 + | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true + | (C.Sort C.Prop, C.Sort C.Set) when need_dummy -> + (match CicEnvironment.get_obj uri with + C.InductiveDefinition (itl,_,_) -> + let (_,_,_,cl) = List.nth itl i in + (* is a singleton definition? *) + List.length cl = 1 + | _ -> + raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + ) + | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true + | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true + | (C.Sort C.Set, C.Sort C.Type) when need_dummy -> + (match CicEnvironment.get_obj uri with + C.InductiveDefinition (itl,_,_) -> + let (_,_,_,cl) = List.nth itl i in + (* is a small inductive type? *) + (*CSC: ottimizzare calcolando staticamente *) + let rec is_small = + function + C.Prod (_,so,de) -> + let s = type_of so in + (s = C.Sort C.Prop || s = C.Sort C.Set) && + is_small de + | _ -> true (*CSC: we trust the type-checker *) + in + List.fold_right (fun (_,x,_) i -> i && is_small x) cl true + | _ -> + raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + ) + | (C.Sort C.Type, C.Sort _) when need_dummy -> true + | (C.Sort C.Prop, C.Prod (_,so,ta)) when not need_dummy -> + let res = CicReduction.are_convertible so ind + in + res && + (match CicReduction.whd ta with + C.Sort C.Prop -> true + | C.Sort C.Set -> + (match CicEnvironment.get_obj uri with + C.InductiveDefinition (itl,_,_) -> + let (_,_,_,cl) = List.nth itl i in + (* is a singleton definition? *) + List.length cl = 1 + | _ -> + raise (WrongUriToMutualInductiveDefinitions + (U.string_of_uri uri)) + ) + | _ -> false + ) + | (C.Sort C.Set, C.Prod (_,so,ta)) when not need_dummy -> + let res = CicReduction.are_convertible so ind + in + res && + (match CicReduction.whd ta with + C.Sort C.Prop + | C.Sort C.Set -> true + | C.Sort C.Type -> + (match CicEnvironment.get_obj uri with + C.InductiveDefinition (itl,_,_) -> + let (_,_,_,cl) = List.nth itl i in + (* is a small inductive type? *) + let rec is_small = + function + C.Prod (_,so,de) -> + let s = type_of so in + (s = C.Sort C.Prop || s = C.Sort C.Set) && + is_small de + | _ -> true (*CSC: we trust the type-checker *) + in + List.fold_right (fun (_,x,_) i -> i && is_small x) cl true + | _ -> + raise (WrongUriToMutualInductiveDefinitions + (U.string_of_uri uri)) + ) + | _ -> raise Impossible + ) + | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy -> + CicReduction.are_convertible so ind + | (_,_) -> false + +and type_of_branch argsno need_dummy outtype term constype = + let module C = Cic in + let module R = CicReduction in + match R.whd constype with + C.MutInd (_,_,_) -> + if need_dummy then + outtype + else + C.Appl [outtype ; term] + | C.Appl (C.MutInd (_,_,_)::tl) -> + let (_,arguments) = split tl argsno + in + if need_dummy && arguments = [] then + outtype + else + C.Appl (outtype::arguments@(if need_dummy then [] else [term])) + | C.Prod (name,so,de) -> + C.Prod (C.Name "pippo",so,type_of_branch argsno need_dummy + (CicSubstitution.lift 1 outtype) + (C.Appl [CicSubstitution.lift 1 term ; C.Rel 1]) de) + | _ -> raise Impossible + + +and type_of t = + let rec type_of_aux env = + let module C = Cic in + let module R = CicReduction in + let module S = CicSubstitution in + let module U = UriManager in + function + C.Rel n -> S.lift n (List.nth env (n - 1)) + | C.Var uri -> + incr fdebug ; + let ty = type_of_variable uri in + decr fdebug ; + ty + | C.Meta n -> raise NotImplemented + | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) + | C.Implicit -> raise Impossible + | C.Cast (te,ty) -> + let _ = type_of ty in + if R.are_convertible (type_of_aux env te) ty then ty + else raise (NotWellTyped "Cast") + | C.Prod (_,s,t) -> + let sort1 = type_of_aux env s + and sort2 = type_of_aux (s::env) t in + sort_of_prod (sort1,sort2) + | C.Lambda (n,s,t) -> + let sort1 = type_of_aux env s + and type2 = type_of_aux (s::env) t in + let sort2 = type_of_aux (s::env) type2 in + (* only to check if the product is well-typed *) + let _ = sort_of_prod (sort1,sort2) in + C.Prod (n,s,type2) + | C.LetIn (n,s,t) -> + let type1 = type_of_aux env s in + let type2 = type_of_aux (type1::env) t in + type2 + | C.Appl (he::tl) when List.length tl > 0 -> + let hetype = type_of_aux env he + and tlbody_and_type = List.map (fun x -> (x, type_of_aux env x)) tl in + (try + eat_prods hetype tlbody_and_type + with _ -> debug (C.Appl (he::tl)) env ; C.Implicit) + | C.Appl _ -> raise (NotWellTyped "Appl: no arguments") + | C.Const (uri,cookingsno) -> + incr fdebug ; + let cty = cooked_type_of_constant uri cookingsno in + decr fdebug ; + cty + | C.Abst _ -> raise Impossible + | C.MutInd (uri,cookingsno,i) -> + incr fdebug ; + let cty = cooked_type_of_mutual_inductive_defs uri cookingsno i in + decr fdebug ; + cty + | C.MutConstruct (uri,cookingsno,i,j) -> + let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j + in + cty + | C.MutCase (uri,cookingsno,i,outtype,term,pl) -> + let outsort = type_of_aux env outtype in + let (need_dummy, k) = + let rec guess_args t = + match decast t with + C.Sort _ -> (true, 0) + | C.Prod (_, s, t) -> + let (b, n) = guess_args t in + if n = 0 then + (* last prod before sort *) + match CicReduction.whd s with + (*CSC vedi nota delirante su cookingsno in cicReduction.ml *) + C.MutInd (uri',_,i') when U.eq uri' uri && i' = i -> (false, 1) + | C.Appl ((C.MutInd (uri',_,i')) :: _) + when U.eq uri' uri && i' = i -> (false, 1) + | _ -> (true, 1) + else + (b, n + 1) + | _ -> raise (NotWellTyped "MutCase: outtype ill-formed") + in + (*CSC whd non serve dopo type_of_aux ? *) + let (b, k) = guess_args outsort in + if not b then (b, k - 1) else (b, k) + in + let (parameters, arguments) = + match R.whd (type_of_aux env term) with + (*CSC manca il caso dei CAST *) + C.MutInd (uri',_,i') -> + (*CSC vedi nota delirante sui cookingsno in cicReduction.ml*) + if U.eq uri uri' && i = i' then ([],[]) + else raise (NotWellTyped ("MutCase: the term is of type " ^ + (U.string_of_uri uri') ^ "," ^ string_of_int i' ^ + " instead of type " ^ (U.string_of_uri uri') ^ "," ^ + string_of_int i)) + | C.Appl (C.MutInd (uri',_,i') :: tl) -> + if U.eq uri uri' && i = i' then split tl (List.length tl - k) + else raise (NotWellTyped ("MutCase: the term is of type " ^ + (U.string_of_uri uri') ^ "," ^ string_of_int i' ^ + " instead of type " ^ (U.string_of_uri uri) ^ "," ^ + string_of_int i)) + | _ -> raise (NotWellTyped "MutCase: the term is not an inductive one") + in + (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *) + let sort_of_ind_type = + if parameters = [] then + C.MutInd (uri,cookingsno,i) + else + C.Appl ((C.MutInd (uri,cookingsno,i))::parameters) + in + if not (check_allowed_sort_elimination uri i need_dummy + sort_of_ind_type (type_of_aux env sort_of_ind_type) outsort) + then + raise (NotWellTyped "MutCase: not allowed sort elimination") ; + + (* let's check if the type of branches are right *) + let (cl,parsno) = + match CicEnvironment.get_cooked_obj uri cookingsno with + C.InductiveDefinition (tl,_,parsno) -> + let (_,_,_,cl) = List.nth tl i in (cl,parsno) + | _ -> + raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + in + let (_,branches_ok) = + List.fold_left + (fun (j,b) (p,(_,c,_)) -> + let cons = + if parameters = [] then + (C.MutConstruct (uri,cookingsno,i,j)) + else + (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters)) + in + (j + 1, b && + R.are_convertible (type_of_aux env p) + (type_of_branch parsno need_dummy outtype cons + (type_of_aux env cons)) + ) + ) (1,true) (List.combine pl cl) + in + if not branches_ok then + raise (NotWellTyped "MutCase: wrong type of a branch") ; + + if not need_dummy then + C.Appl ((outtype::arguments)@[term]) + else if arguments = [] then + outtype + else + C.Appl (outtype::arguments) + | C.Fix (i,fl) -> + let types_times_kl = + List.rev + (List.map (fun (_,k,ty,_) -> let _ = type_of_aux env ty in (ty,k)) fl) + in + let (types,kl) = List.split types_times_kl in + let len = List.length types in + List.iter + (fun (name,x,ty,bo) -> + if (R.are_convertible (type_of_aux (types @ env) bo) + (CicSubstitution.lift len ty)) + then + begin + let (m, eaten) = eat_lambdas (x + 1) bo in + (*let's control the guarded by destructors conditions D{f,k,x,M}*) + if not (guarded_by_destructors eaten (len + eaten) kl 1 [] m) then + raise (NotWellTyped "Fix: not guarded by destructors") + end + else + raise (NotWellTyped "Fix: ill-typed bodies") + ) fl ; + + (*CSC: controlli mancanti solo su D{f,k,x,M} *) + let (_,_,ty,_) = List.nth fl i in + ty + | C.CoFix (i,fl) -> + let types = + List.rev (List.map (fun (_,ty,_) -> let _ = type_of_aux env ty in ty) fl) + in + let len = List.length types in + List.iter + (fun (_,ty,bo) -> + if (R.are_convertible (type_of_aux (types @ env) bo) + (CicSubstitution.lift len ty)) + then + begin + (* let's control the guarded by constructors conditions C{f,M} *) + if not (guarded_by_constructors 0 len 0 bo) then + raise (NotWellTyped "CoFix: not guarded by constructors") + end + else + raise (NotWellTyped "CoFix: ill-typed bodies") + ) fl ; + + let (_,ty,_) = List.nth fl i in + ty + + and decast = + let module C = Cic in + function + C.Cast (t,_) -> t + | t -> t + + and sort_of_prod (t1, t2) = + let module C = Cic in + match (decast t1, decast t2) with + (C.Sort s1, C.Sort s2) + when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *) + C.Sort s2 + | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) + | (_,_) -> raise (NotWellTyped "Prod") + + and eat_prods hetype = + (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *) + (*CSC: cucinati *) + function + [] -> hetype + | (hete, hety)::tl -> + (match (CicReduction.whd hetype) with + Cic.Prod (n,s,t) -> + if CicReduction.are_convertible s hety then + (CicReduction.fdebug := -1 ; + eat_prods (CicSubstitution.subst hete t) tl + ) + else + ( + CicReduction.fdebug := 0 ; + let _ = CicReduction.are_convertible s hety in + debug hete [hety ; s] ; + raise (NotWellTyped "Appl: wrong parameter-type") +) + | _ -> raise (NotWellTyped "Appl: wrong Prod-type") + ) + in + type_of_aux [] t +;; + +let typecheck uri = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + match CicEnvironment.is_type_checked uri 0 with + CicEnvironment.CheckedObj _ -> () + | CicEnvironment.UncheckedObj uobj -> + (* let's typecheck the uncooked object *) + log (`Start_type_checking uri) ; + (match uobj with + C.Definition (_,te,ty,_) -> + let _ = type_of ty in + if not (R.are_convertible (type_of te ) ty) then + raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri))) + | C.Axiom (_,ty,_) -> + (* only to check that ty is well-typed *) + let _ = type_of ty in () + | C.CurrentProof (_,_,te,ty) -> + (*CSC [] wrong *) + let _ = type_of ty in + debug (type_of te) [] ; + if not (R.are_convertible (type_of te) ty) then + raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri))) + | C.Variable (_,bo,ty) -> + (* only to check that ty is well-typed *) + let _ = type_of ty in + (match bo with + None -> () + | Some bo -> + if not (R.are_convertible (type_of bo) ty) then + raise (NotWellTyped ("Variable" ^ (U.string_of_uri uri))) + ) + | C.InductiveDefinition _ -> + cooked_mutual_inductive_defs uri uobj + ) ; + CicEnvironment.set_type_checking_info uri ; + log (`Type_checking_completed uri) +;; diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli new file mode 100644 index 000000000..72dd63c57 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli @@ -0,0 +1,34 @@ +(* 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 NotWellTyped of string +exception WrongUriToConstant of string +exception WrongUriToVariable of string +exception WrongUriToMutualInductiveDefinitions of string +exception ListTooShort +exception NotPositiveOccurrences of string +exception NotWellFormedTypeOfInductiveConstructor of string +exception WrongRequiredArgument of string +val typecheck : UriManager.uri -> unit diff --git a/helm/ocaml/getter/Makefile b/helm/ocaml/getter/Makefile new file mode 100644 index 000000000..686b2ddd3 --- /dev/null +++ b/helm/ocaml/getter/Makefile @@ -0,0 +1,36 @@ +BIN_DIR = /usr/local/bin +REQUIRES = pxp netclient helm-urimanager pxp netclient +PREDICATES = +OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" +OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) +OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLDEP = ocamldep + +all: clientHTTP.cmo getter.cmo configuration.cmo +opt: clientHTTP.cmx getter.cmx configuration.cmx + +DEPOBJS = clientHTTP.mli clientHTTP.ml getter.mli getter.ml configuration.ml + +depend: + $(OCAMLDEP) $(DEPOBJS) > .depend + +.SUFFIXES: .ml .mli .cmo .cmi .cmx +.ml.cmo: + $(OCAMLC) -c $< +.mli.cmi: + $(OCAMLC) -c $< +.ml.cmx: + $(OCAMLOPT) -c $< + +clean: + rm -f *.cm[iox] + +install: + #cp + +uninstall: + #rm -f + +.PHONY: install uninstall clean + +include .depend diff --git a/helm/ocaml/getter/clientHTTP.ml b/helm/ocaml/getter/clientHTTP.ml new file mode 100644 index 000000000..4d5488c00 --- /dev/null +++ b/helm/ocaml/getter/clientHTTP.ml @@ -0,0 +1,60 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +exception HttpClientError of exn * string;; + +let send cmd = + try + ignore (Http_client.Convenience.http_get cmd) + with + e -> raise (HttpClientError (e,cmd)) +;; + +let get uri = + try + Http_client.Convenience.http_get uri + with + e -> raise (HttpClientError (e,uri)) +;; + +let get_and_save uri dest_filename = + let reply = get uri + and out_channel = open_out dest_filename in + output_string out_channel reply ; + close_out out_channel +;; + +let get_and_save_to_tmp uri = + let flat_string s s' c = + let cs = String.copy s in + for i = 0 to (String.length s) - 1 do + if String.contains s' s.[i] then cs.[i] <- c + done ; + cs + in + let tmp_file = Configuration.tmp_dir ^ "/" ^ (flat_string uri ".-=:;!?/&" '_') in + get_and_save uri tmp_file ; + tmp_file +;; diff --git a/helm/ocaml/getter/clientHTTP.mli b/helm/ocaml/getter/clientHTTP.mli new file mode 100644 index 000000000..59587edc2 --- /dev/null +++ b/helm/ocaml/getter/clientHTTP.mli @@ -0,0 +1,30 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +exception HttpClientError of exn * string;; +val send : string -> unit +val get : string -> string +val get_and_save : string -> string -> unit +val get_and_save_to_tmp : string -> string diff --git a/helm/ocaml/getter/configuration.ml b/helm/ocaml/getter/configuration.ml new file mode 100644 index 000000000..2c7ead3dc --- /dev/null +++ b/helm/ocaml/getter/configuration.ml @@ -0,0 +1,118 @@ +(******************************************************************************) +(* *) +(* 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 -> "/projects/helm/V7/phd/local/etc/helm" + 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/ocaml/getter/getter.ml b/helm/ocaml/getter/getter.ml new file mode 100644 index 000000000..894bf3ea9 --- /dev/null +++ b/helm/ocaml/getter/getter.ml @@ -0,0 +1,63 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(******************************************************************************) + +let getter_url = ref Configuration.getter_url;; + +let update () = + (* deliver update request to http_getter *) + ClientHTTP.send (!getter_url ^ "update") +;; + +type format = + Normal + | GZipped +;; + +let getxml ?(format=Normal) ?(patchdtd=true) uri = + (* deliver getxml request to http_getter *) + ClientHTTP.get_and_save_to_tmp + (!getter_url ^ "getxml" ^ + "?uri=" ^ UriManager.string_of_uri uri ^ + "&format=" ^ (match format with Normal -> "normal" | GZipped -> "gzipped") ^ + "&patch_dtd=" ^ (match patchdtd with true -> "yes" | false -> "no") + ) +;; + +let register uri url = + (* deliver register request to http_getter *) + ClientHTTP.send + (!getter_url ^ "register" ^ + "?uri=" ^ (UriManager.string_of_uri uri) ^ + "&url=" ^ url) +;; diff --git a/helm/ocaml/getter/getter.mli b/helm/ocaml/getter/getter.mli new file mode 100644 index 000000000..6b1d2ca29 --- /dev/null +++ b/helm/ocaml/getter/getter.mli @@ -0,0 +1,53 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* *) +(******************************************************************************) + +(* THE URL OF THE HTTP GETTER *) +val getter_url : string ref + +(* SIMPLE BINDINGS TO THE HTTP GETTER *) +(* synchronize with the servers *) +val update : unit -> unit + +type format = + Normal + | GZipped +;; + +(* get the xml file *) +(* defaults: format = Normal and patchdtd = true *) +val getxml : ?format:format -> ?patchdtd:bool -> UriManager.uri -> string + +(* adds an (URI -> URL) entry in the map from URIs to URLs *) +val register : UriManager.uri -> string -> unit diff --git a/helm/ocaml/pxp/Makefile b/helm/ocaml/pxp/Makefile new file mode 100644 index 000000000..09b7e613e --- /dev/null +++ b/helm/ocaml/pxp/Makefile @@ -0,0 +1,36 @@ +BIN_DIR = /usr/local/bin +REQUIRES = helm-getter +PREDICATES = +OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" +OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) +OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLDEP = ocamldep + +all: csc_pxp_reader.cmo pxpUriResolver.cmo +opt: csc_pxp_reader.cmx pxpUriResolver.cmx + +DEPOBJS = csc_pxp_reader.ml pxpUriResolver.ml + +depend: + $(OCAMLDEP) $(DEPOBJS) > .depend + +.SUFFIXES: .ml .mli .cmo .cmi .cmx +.ml.cmo: + $(OCAMLC) -c $< +.mli.cmi: + $(OCAMLC) -c $< +.ml.cmx: + $(OCAMLOPT) -c $< + +clean: + rm -f *.cm[iox] + +install: + #cp + +uninstall: + #rm -f + +.PHONY: install uninstall clean + +include .depend diff --git a/helm/ocaml/pxp/csc_pxp_reader.ml b/helm/ocaml/pxp/csc_pxp_reader.ml new file mode 100644 index 000000000..daabedc90 --- /dev/null +++ b/helm/ocaml/pxp/csc_pxp_reader.ml @@ -0,0 +1,1011 @@ +(* $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/11/26 18:28:28 sacerdot + * HELM OCaml libraries with findlib support. + * + * 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/ocaml/pxp/pxpUriResolver.ml b/helm/ocaml/pxp/pxpUriResolver.ml new file mode 100644 index 000000000..1e2fec918 --- /dev/null +++ b/helm/ocaml/pxp/pxpUriResolver.ml @@ -0,0 +1,266 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 11/10/2000 *) +(* *) +(* *) +(******************************************************************************) + +let resolve s = + let starts_with s s' = + if String.length s < String.length s' then + false + else + (String.sub s 0 (String.length s')) = s' + in + if starts_with s "http:" then + ClientHTTP.get_and_save_to_tmp s + else + s +;; + +(*PXP 1.0 +let url_syntax = + let enable_if = + function + `Not_recognized -> Neturl.Url_part_not_recognized + | `Allowed -> Neturl.Url_part_allowed + | `Required -> Neturl.Url_part_required + in + { Neturl.null_url_syntax with + Neturl.url_enable_scheme = enable_if `Allowed; + Neturl.url_enable_host = enable_if `Allowed; + Neturl.url_enable_path = Neturl.Url_part_required; + Neturl.url_accepts_8bits = true; + } +;; + +exception Unexpected;; (* Added when porting the file to PXP 1.1 *) + +let file_url_of_id xid = + let file_url_of_sysname sysname = + (* By convention, we can assume that sysname is a URL conforming + * to RFC 1738 with the exception that it may contain non-ASCII + * UTF-8 characters. + *) + try + Neturl.url_of_string url_syntax sysname + (* may raise Malformed_URL *) + with + Neturl.Malformed_URL -> raise Pxp_reader.Not_competent + in + let url = + match xid with + Pxp_types.Anonymous -> raise Pxp_reader.Not_competent + | Pxp_types.Public (_,sysname) -> + let sysname = resolve sysname in + if sysname <> "" then file_url_of_sysname sysname + else raise Pxp_reader.Not_competent + | Pxp_types.System sysname -> + let sysname = resolve sysname in + file_url_of_sysname sysname + | Pxp_types.Private pid -> raise Unexpected + in + let scheme = + try Neturl.url_scheme url with Not_found -> "file" in + let host = + try Neturl.url_host url with Not_found -> "" in + + if scheme <> "file" then raise Pxp_reader.Not_competent; + if host <> "" && host <> "localhost" then raise Pxp_reader.Not_competent; + + url +;; + +let from_file ?system_encoding utf8_filename = + + let r = + new Pxp_reader.resolve_as_file + ?system_encoding:system_encoding + ~url_of_id:file_url_of_id + () + in + + let utf8_abs_filename = + if utf8_filename <> "" && utf8_filename.[0] = '/' then + utf8_filename + else + Sys.getcwd() ^ "/" ^ utf8_filename + in + + let syntax = { Neturl.ip_url_syntax with Neturl.url_accepts_8bits = true } in + let url = Neturl.make_url + ~scheme:"file" + ~host:"localhost" + ~path:(Neturl.split_path utf8_abs_filename) + syntax + in + + let xid = Pxp_types.System (Neturl.string_of_url url) in + + + Pxp_yacc.ExtID(xid, r) +;; +*) + +(*PXP 1.1*) +(* csc_pxp_reader.ml is an exact copy of PXP pxp_reader.ml *) +(* The only reason is to loosen the interface *) + +class resolve_as_file + ?(file_prefix = (`Allowed :> Csc_pxp_reader.spec)) + ?(host_prefix = (`Allowed :> Csc_pxp_reader.spec)) + ?(system_encoding = `Enc_utf8) + ?(map_private_id = (fun _ -> raise Csc_pxp_reader.Not_competent)) + ?(open_private_id = (fun _ -> raise Csc_pxp_reader.Not_competent)) + () + = + + let url_syntax = + let enable_if = + function + `Not_recognized -> Neturl.Url_part_not_recognized + | `Allowed -> Neturl.Url_part_allowed + | `Required -> Neturl.Url_part_required + in + { Neturl.null_url_syntax with + Neturl.url_enable_scheme = enable_if file_prefix; + Neturl.url_enable_host = enable_if host_prefix; + Neturl.url_enable_path = Neturl.Url_part_required; + Neturl.url_accepts_8bits = true; + } + in + + let base_url_syntax = + { Neturl.null_url_syntax with + Neturl.url_enable_scheme = Neturl.Url_part_required; + Neturl.url_enable_host = Neturl.Url_part_allowed; + Neturl.url_enable_path = Neturl.Url_part_required; + Neturl.url_accepts_8bits = true; + } + in + + let default_base_url = + Neturl.make_url + ~scheme: "file" + ~host: "" + ~path: (Neturl.split_path (Sys.getcwd() ^ "/")) + base_url_syntax + in + + let file_url_of_id xid = + let module P = Csc_pxp_reader in + let module T = Pxp_types in + let file_url_of_sysname sysname = + (* By convention, we can assume that sysname is a URL conforming + * to RFC 1738 with the exception that it may contain non-ASCII + * UTF-8 characters. + *) + try + Neturl.url_of_string url_syntax sysname + (* may raise Malformed_URL *) + with + Neturl.Malformed_URL -> raise P.Not_competent + in + let url = + match xid with + T.Anonymous -> raise P.Not_competent + | T.Public (_,sysname) -> let sysname = resolve sysname in + if sysname <> "" then file_url_of_sysname sysname + else raise P.Not_competent + | T.System sysname -> let sysname = resolve sysname in + file_url_of_sysname sysname + | T.Private pid -> map_private_id pid + in + let scheme = + try Neturl.url_scheme url with Not_found -> "file" in + let host = + try Neturl.url_host url with Not_found -> "" in + + if scheme <> "file" then raise P.Not_competent; + if host <> "" && host <> "localhost" then raise P.Not_competent; + + url + in + + let channel_of_file_url xid url = + let module P = Csc_pxp_reader in + let module T = Pxp_types in + match xid with + T.Private pid -> open_private_id pid + | _ -> + ( try + let path_utf8 = + try Neturl.join_path (Neturl.url_path ~encoded:false url) + with Not_found -> raise P.Not_competent + in + + let path = + Netconversion.recode_string + ~in_enc: `Enc_utf8 + ~out_enc: system_encoding + path_utf8 in + (* May raise Malformed_code *) + + open_in_bin path, None + (* May raise Sys_error *) + + with + | Netconversion.Malformed_code -> assert false + (* should not happen *) + | Sys_error _ as e -> + raise (P.Not_resolvable e) + ) + in + + Csc_pxp_reader.resolve_read_url_channel + ~base_url: default_base_url + ~url_of_id: file_url_of_id + ~channel_of_url: channel_of_file_url + () +;; + +let from_file ?(alt = []) ?system_encoding ?enc utf8_filename = + let r = + new resolve_as_file + ?system_encoding:system_encoding + () + in + + let url = Csc_pxp_reader.make_file_url + ?system_encoding + ?enc + utf8_filename in + + let xid = Pxp_types.System (Neturl.string_of_url url) in + + Pxp_yacc.ExtID(xid, new Csc_pxp_reader.combine (r :: alt)) +;; + diff --git a/helm/ocaml/urimanager/Makefile b/helm/ocaml/urimanager/Makefile new file mode 100644 index 000000000..b935779d8 --- /dev/null +++ b/helm/ocaml/urimanager/Makefile @@ -0,0 +1,36 @@ +BIN_DIR = /usr/local/bin +REQUIRES = str +PREDICATES = +OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" +OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) +OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLDEP = ocamldep + +all: uriManager.cmo +opt: uriManager.cmx + +DEPOBJS = uriManager.mli uriManager.ml + +depend: + $(OCAMLDEP) $(DEPOBJS) > .depend + +.SUFFIXES: .ml .mli .cmo .cmi .cmx +.ml.cmo: + $(OCAMLC) -c $< +.mli.cmi: + $(OCAMLC) -c $< +.ml.cmx: + $(OCAMLOPT) -c $< + +clean: + rm -f *.cm[iox] + +install: + #cp + +uninstall: + #rm -f + +.PHONY: install uninstall clean + +include .depend diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml new file mode 100644 index 000000000..0fa24cfcd --- /dev/null +++ b/helm/ocaml/urimanager/uriManager.ml @@ -0,0 +1,139 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* "cic:/a/b/c.con" => [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c" |] *) +type uri = string array;; + +let eq uri1 uri2 = + uri1 == uri2 +;; + +let string_of_uri uri = uri.(Array.length uri - 2);; +let name_of_uri uri = uri.(Array.length uri - 1);; +let buri_of_uri uri = uri.(Array.length uri - 3);; +let depth_of_uri uri = Array.length uri - 2;; + +(*CSC: ora e' diventato poco efficiente, migliorare *) +let relative_depth curi uri cookingsno = + let rec length_of_current_prefix l1 l2 = + match (l1, l2) with + (he1::tl1, he2::tl2) when he1 == he2 -> + 1 + length_of_current_prefix tl1 tl2 + | (_,_) -> 0 + in + depth_of_uri uri - + length_of_current_prefix + (Array.to_list (Array.sub curi 0 (Array.length curi - (2 + cookingsno)))) + (Array.to_list (Array.sub uri 0 (Array.length uri - 2))) + (*CSC: vecchio codice da eliminare + if eq curi uri then 0 + else + depth_of_uri uri - + length_of_current_prefix (Array.to_list curi) (Array.to_list uri) + *) +;; + +module OrderedStrings = + struct + type t = string + let compare (s1 : t) (s2 : t) = compare s1 s2 + end +;; + +module SetOfStrings = Map.Make(OrderedStrings);; + +(*CSC: commento obsoleto ed errato *) +(* Invariant: the map is the identity function, *) +(* i.e. (SetOfStrings.find str !set_of_uri) == str *) +let set_of_uri = ref SetOfStrings.empty;; +let set_of_prefixes = ref SetOfStrings.empty;; + +(* similar to uri_of_string, but used for prefixes of uris *) +let normalize prefix = + try + SetOfStrings.find prefix !set_of_prefixes + with + Not_found -> + set_of_prefixes := SetOfStrings.add prefix prefix !set_of_prefixes ; + prefix +;; + +exception IllFormedUri of string;; + +let mk_prefixes str = + let rec aux curi = + function + [he] -> + let prefix_uri = curi ^ "/" ^ he + and name = List.hd (Str.split (Str.regexp "\.") he) in + [ normalize prefix_uri ; name ] + | he::tl -> + let prefix_uri = curi ^ "/" ^ he in + (normalize prefix_uri)::(aux prefix_uri tl) + | _ -> raise (IllFormedUri str) + in + let tokens = (Str.split (Str.regexp "/") str) in + (* ty = "cic:" *) + let (ty, sp) = (List.hd tokens, List.tl tokens) in + aux ty sp +;; + +let uri_of_string str = + try + SetOfStrings.find str !set_of_uri + with + Not_found -> + let uri = Array.of_list (mk_prefixes str) in + set_of_uri := SetOfStrings.add str uri !set_of_uri ; + uri +;; + +let cicuri_of_uri uri = + let completeuri = string_of_uri uri in + let newcompleteuri = + (Str.replace_first (Str.regexp "\.types$") "" + (Str.replace_first (Str.regexp "\.ann$") "" completeuri)) + in + if completeuri = newcompleteuri then + uri + else + let newuri = Array.copy uri in + newuri.(Array.length uri - 2) <- newcompleteuri ; + newuri +;; + +let annuri_of_uri uri = + let completeuri = string_of_uri uri in + if Str.string_match (Str.regexp ".*\.ann$") completeuri 0 then + uri + else + let newuri = Array.copy uri in + newuri.(Array.length uri - 2) <- completeuri ^ ".ann" ; + newuri +;; + +let uri_is_annuri uri = + Str.string_match (Str.regexp ".*\.ann$") (string_of_uri uri) 0 +;; diff --git a/helm/ocaml/urimanager/uriManager.mli b/helm/ocaml/urimanager/uriManager.mli new file mode 100644 index 000000000..2cdd27e3d --- /dev/null +++ b/helm/ocaml/urimanager/uriManager.mli @@ -0,0 +1,51 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +type uri + +val eq : uri -> uri -> bool + +val uri_of_string : string -> uri + +val string_of_uri : uri -> string (* complete uri *) +val name_of_uri : uri -> string (* name only (without extension)*) +val buri_of_uri : uri -> string (* base uri only *) +val depth_of_uri : uri -> int (* length of the path *) + +(* relative_depth curi uri cookingsno *) +(* is the number of times to cook uri to use it when the current uri is curi *) +(* cooked cookingsno times *) +val relative_depth : uri -> uri -> int -> int + +(* given an uri, returns the uri of the corresponding cic file, *) +(* i.e. removes the [.types][.ann] suffix *) +val cicuri_of_uri : uri -> uri + +(* given an uri, returns the uri of the corresponding annotation file, *) +(* i.e. adds the .ann suffix if not already present *) +val annuri_of_uri : uri -> uri + +(* given an uri, tells if it refers to an annotation *) +val uri_is_annuri : uri -> bool diff --git a/helm/ocaml/xml/Makefile b/helm/ocaml/xml/Makefile new file mode 100644 index 000000000..90e1011e5 --- /dev/null +++ b/helm/ocaml/xml/Makefile @@ -0,0 +1,36 @@ +BIN_DIR = /usr/local/bin +REQUIRES = +PREDICATES = +OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" +OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) +OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLDEP = ocamldep + +all: xml.cmo +opt: xml.cmx + +DEPOBJS = xml.mli xml.ml + +depend: + $(OCAMLDEP) $(DEPOBJS) > .depend + +.SUFFIXES: .ml .mli .cmo .cmi .cmx +.ml.cmo: + $(OCAMLC) -c $< +.mli.cmi: + $(OCAMLC) -c $< +.ml.cmx: + $(OCAMLOPT) -c $< + +clean: + rm -f *.cm[iox] + +install: + #cp + +uninstall: + #rm -f + +.PHONY: install uninstall clean + +include .depend diff --git a/helm/ocaml/xml/xml.ml b/helm/ocaml/xml/xml.ml new file mode 100644 index 000000000..302aef23f --- /dev/null +++ b/helm/ocaml/xml/xml.ml @@ -0,0 +1,101 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* A tactic to print Coq objects in XML *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 18/10/2000 *) +(* *) +(* This module defines a pretty-printer and the stream of commands to the pp *) +(* *) +(******************************************************************************) + + +(* the type token for XML cdata, empty elements and not-empty elements *) +(* Usage: *) +(* Str cdata *) +(* Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen] *) +(* NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *) +(* content *) +type token = Str of string + | Empty of string * (string * string) list + | NEmpty of string * (string * string) list * token Stream.t +;; + +(* currified versions of the constructors make the code more readable *) +let xml_empty name attrs = [< 'Empty(name,attrs) >] +let xml_nempty name attrs content = [< 'NEmpty(name,attrs,content) >] +let xml_cdata str = [< 'Str str >] + +(* Usage: *) +(* pp tokens None pretty prints the output on stdout *) +(* pp tokens (Some filename) pretty prints the output on the file filename *) +let pp ?(quiet=false) strm fn = + let channel = ref stdout in + let rec pp_r m = + parser + [< 'Str a ; s >] -> + print_spaces m ; + fprint_string (a ^ "\n") ; + pp_r m s + | [< 'Empty(n,l) ; s >] -> + print_spaces m ; + fprint_string ("<" ^ n) ; + List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l; + fprint_string "/>\n" ; + pp_r m s + | [< 'NEmpty(n,l,c) ; s >] -> + print_spaces m ; + fprint_string ("<" ^ n) ; + List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l; + fprint_string ">\n" ; + pp_r (m+1) c ; + print_spaces m ; + fprint_string ("\n") ; + pp_r m s + | [< >] -> () + and print_spaces m = + for i = 1 to m do fprint_string " " done + and fprint_string str = + output_string !channel str + in + match fn with + Some filename -> + channel := open_out filename ; + pp_r 0 strm ; + close_out !channel ; + if not quiet then + begin + print_string ("\nWriting on file \"" ^ filename ^ + "\" was succesfull\n"); + flush stdout + end + | None -> + pp_r 0 strm +;; diff --git a/helm/ocaml/xml/xml.mli b/helm/ocaml/xml/xml.mli new file mode 100644 index 000000000..a68110b29 --- /dev/null +++ b/helm/ocaml/xml/xml.mli @@ -0,0 +1,60 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* A tactic to print Coq objects in XML *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 18/10/2000 *) +(* *) +(* This module defines a pretty-printer and the stream of commands to the pp *) +(* *) +(******************************************************************************) + +(* Tokens for XML cdata, empty elements and not-empty elements *) +(* Usage: *) +(* Str cdata *) +(* Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen] *) +(* NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *) +(* content *) +type token = + | Str of string + | Empty of string * (string * string) list + | NEmpty of string * (string * string) list * token Stream.t + +(* currified versions of the token constructors make the code more readable *) +val xml_empty : string -> (string * string) list -> token Stream.t +val xml_nempty : + string -> (string * string) list -> token Stream.t -> token Stream.t +val xml_cdata : string -> token Stream.t + +(* The pretty printer for streams of token *) +(* Usage: *) +(* pp tokens None pretty prints the output on stdout *) +(* pp tokens (Some filename) pretty prints the output on the file filename *) +val pp : ?quiet:bool -> token Stream.t -> string option -> unit -- 2.39.2