From b8dac1f8f6b664b78e58c152cd3960e121713f5d Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 8 Oct 2010 10:30:47 +0000 Subject: [PATCH] - hmysql removed (RIP) - library simplified to handle only new files, moo and lexicon - BROKEN FEATURES: recursive decompilation of library files is currently broken since, without the db, there is currently no way to compute the reverse dependencies --- matita/components/METAS/meta.helm-hmysql.src | 4 - matita/components/METAS/meta.helm-library.src | 2 +- .../components/METAS/meta.helm-ng_kernel.src | 2 +- matita/components/Makefile | 1 - matita/components/binaries/Makefile | 2 +- matita/components/binaries/heights/.depend | 0 .../components/binaries/heights/.depend.opt | 0 matita/components/binaries/heights/Makefile | 104 ----- .../binaries/heights/heights.conf.xml | 7 - matita/components/binaries/heights/heights.ml | 48 -- .../components/binaries/transcript/grafite.ml | 3 +- .../grafite_engine/grafiteEngine.ml | 15 - .../components/grafite_engine/grafiteSync.ml | 26 -- .../components/grafite_engine/grafiteSync.mli | 10 - .../components/grafite_engine/grafiteTypes.ml | 3 - .../grafite_engine/grafiteTypes.mli | 2 - matita/components/hmysql/.depend | 7 - matita/components/hmysql/.depend.opt | 7 - matita/components/hmysql/Makefile | 14 - matita/components/hmysql/hMysql.ml | 92 ---- matita/components/hmysql/hSql.ml | 178 -------- matita/components/hmysql/hSql.mli | 70 --- matita/components/hmysql/hSqlite3.ml | 234 ---------- matita/components/library/.depend | 32 -- matita/components/library/.depend.opt | 32 -- matita/components/library/Makefile | 18 - matita/components/library/cicCoercion.ml | 40 -- matita/components/library/cicCoercion.mli | 40 -- matita/components/library/cicFix.ml | 69 --- matita/components/library/cicFix.mli | 26 -- matita/components/library/coercDb.ml | 177 -------- matita/components/library/coercDb.mli | 67 --- matita/components/library/librarian.ml | 418 ------------------ matita/components/library/librarian.mli | 105 ----- matita/components/library/libraryClean.ml | 281 ------------ matita/components/library/libraryClean.mli | 29 -- matita/components/library/libraryDb.ml | 215 --------- matita/components/library/libraryDb.mli | 35 -- matita/components/library/libraryMisc.ml | 38 -- matita/components/library/libraryMisc.mli | 30 -- matita/components/library/librarySync.ml | 387 ---------------- matita/components/library/librarySync.mli | 59 --- matita/components/ng_refiner/nCicCoercion.ml | 38 -- matita/components/ng_refiner/nCicCoercion.mli | 3 - matita/matita/matitaExcPp.ml | 2 - matita/matita/matitaInit.ml | 5 - matita/matita/matitaScript.ml | 1 - matita/matita/matitacLib.ml | 3 +- matita/matita/matitaclean.ml | 1 - 49 files changed, 5 insertions(+), 2977 deletions(-) delete mode 100644 matita/components/METAS/meta.helm-hmysql.src delete mode 100644 matita/components/binaries/heights/.depend delete mode 100644 matita/components/binaries/heights/.depend.opt delete mode 100644 matita/components/binaries/heights/Makefile delete mode 100644 matita/components/binaries/heights/heights.conf.xml delete mode 100644 matita/components/binaries/heights/heights.ml delete mode 100644 matita/components/hmysql/.depend delete mode 100644 matita/components/hmysql/.depend.opt delete mode 100644 matita/components/hmysql/Makefile delete mode 100644 matita/components/hmysql/hMysql.ml delete mode 100644 matita/components/hmysql/hSql.ml delete mode 100644 matita/components/hmysql/hSql.mli delete mode 100644 matita/components/hmysql/hSqlite3.ml delete mode 100644 matita/components/library/.depend delete mode 100644 matita/components/library/.depend.opt delete mode 100644 matita/components/library/Makefile delete mode 100644 matita/components/library/cicCoercion.ml delete mode 100644 matita/components/library/cicCoercion.mli delete mode 100644 matita/components/library/cicFix.ml delete mode 100644 matita/components/library/cicFix.mli delete mode 100644 matita/components/library/coercDb.ml delete mode 100644 matita/components/library/coercDb.mli delete mode 100644 matita/components/library/librarian.ml delete mode 100644 matita/components/library/librarian.mli delete mode 100644 matita/components/library/libraryClean.ml delete mode 100644 matita/components/library/libraryClean.mli delete mode 100644 matita/components/library/libraryDb.ml delete mode 100644 matita/components/library/libraryDb.mli delete mode 100644 matita/components/library/libraryMisc.ml delete mode 100644 matita/components/library/libraryMisc.mli delete mode 100644 matita/components/library/librarySync.ml delete mode 100644 matita/components/library/librarySync.mli diff --git a/matita/components/METAS/meta.helm-hmysql.src b/matita/components/METAS/meta.helm-hmysql.src deleted file mode 100644 index 21841b5ca..000000000 --- a/matita/components/METAS/meta.helm-hmysql.src +++ /dev/null @@ -1,4 +0,0 @@ -requires="helm-registry sqlite3 mysql helm-extlib" -version="0.0.1" -archive(byte)="hmysql.cma" -archive(native)="hmysql.cmxa" diff --git a/matita/components/METAS/meta.helm-library.src b/matita/components/METAS/meta.helm-library.src index 2871ae878..ee7026024 100644 --- a/matita/components/METAS/meta.helm-library.src +++ b/matita/components/METAS/meta.helm-library.src @@ -1,4 +1,4 @@ -requires="helm-cic helm-getter helm-hmysql" +requires="helm-cic helm-getter" version="0.0.1" archive(byte)="library.cma" archive(native)="library.cmxa" diff --git a/matita/components/METAS/meta.helm-ng_kernel.src b/matita/components/METAS/meta.helm-ng_kernel.src index 549e479d7..7e913b61d 100644 --- a/matita/components/METAS/meta.helm-ng_kernel.src +++ b/matita/components/METAS/meta.helm-ng_kernel.src @@ -1,4 +1,4 @@ -requires="helm-library" +requires="helm-cic" version="0.0.1" archive(byte)="ng_kernel.cma" archive(native)="ng_kernel.cmxa" diff --git a/matita/components/Makefile b/matita/components/Makefile index 86fc08c69..de0d4ed30 100644 --- a/matita/components/Makefile +++ b/matita/components/Makefile @@ -10,7 +10,6 @@ MODULES = \ xml \ hgdome \ registry \ - hmysql \ syntax_extensions \ thread \ urimanager \ diff --git a/matita/components/binaries/Makefile b/matita/components/binaries/Makefile index 7966f3a61..f8b952233 100644 --- a/matita/components/binaries/Makefile +++ b/matita/components/binaries/Makefile @@ -3,7 +3,7 @@ H=@ #CSC: saturate is broken after the huge refactoring of auto/paramodulation #CSC: by Andrea #BINARIES=extractor table_creator utilities saturate -BINARIES=transcript heights +BINARIES=transcript all: $(BINARIES:%=rec@all@%) opt: $(BINARIES:%=rec@opt@%) diff --git a/matita/components/binaries/heights/.depend b/matita/components/binaries/heights/.depend deleted file mode 100644 index e69de29bb..000000000 diff --git a/matita/components/binaries/heights/.depend.opt b/matita/components/binaries/heights/.depend.opt deleted file mode 100644 index e69de29bb..000000000 diff --git a/matita/components/binaries/heights/Makefile b/matita/components/binaries/heights/Makefile deleted file mode 100644 index cd270082a..000000000 --- a/matita/components/binaries/heights/Makefile +++ /dev/null @@ -1,104 +0,0 @@ -include ../../../Makefile.defs - -H=@ - -REQUIRES = helm-library - -MLS = heights.ml -MLIS = -CLEAN = - -LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) -LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) - -CMOS = $(MLS:%.ml=%.cmo) -CMXS = $(MLS:%.ml=%.cmx) -CMIS = $(MLIS:%.mli=%.cmi) -EXTRAS = - -OCAMLC = $(OCAMLFIND) ocamlc -thread -package "$(REQUIRES)" -linkpkg -rectypes -OCAMLOPT = $(OCAMLFIND) ocamlopt -thread -package "$(REQUIRES)" -linkpkg -rectypes -OCAMLDEP = $(OCAMLFIND) ocamldep -OCAMLYACC = ocamlyacc -OCAMLLEX = ocamllex - -all: heights .depend - @echo -n - -opt: heights.opt $(EXTRAS) .depend.opt - @echo -n - -heights: $(CMIS) $(CMOS) $(EXTRAS) - @echo " OCAMLC $(CMOS)" - $(H)$(OCAMLC) -o $@ $(CMOS) - -heights.opt: $(CMIS) $(CMXS) $(EXTRAS) - @echo " OCAMLOPT $(CMXS)" - $(H)$(OCAMLOPT) -o $@ $(CMXS) - -clean: - $(H)rm -f *.cm[iox] *.a *.o *.output - $(H)rm -f heights heights.opt $(CLEAN) - -.depend: $(MLIS) $(MLS) $(EXTRAS) - @echo " OCAMLDEP $(MLIS) $(MLS)" - $(H)$(OCAMLDEP) $(MLIS) $(MLS) > .depend - -.depend.opt: $(MLIS) $(MLS) $(EXTRAS) - @echo " OCAMLDEP -native $(MLIS) $(MLS)" - $(H)$(OCAMLDEP) -native $(MLIS) $(MLS) > .depend.opt - -test: heights heights.conf.xml - @echo " HEIGHTS" - $(H)$< 1> heights.txt 2> errors.txt - -test.opt: heights.opt heights.conf.xml $(PACKAGES:%=%.conf.xml) - @echo " HEIGHTS.OPT" - $(H)$< 1> heights.txt 2> errors.txt - -export: clean - $(H)rm -f *~ - @echo " TAR heights" - $(H)cd .. && tar --exclude=heights/.svn -czf heights.tgz heights - -depend: .depend - -depend.opt: .depend.opt - -%.cmi: %.mli $(EXTRAS) - @echo " OCAMLC $<" - $(H)$(OCAMLC) -c $< -%.cmo %.cmi: %.ml $(EXTRAS) $(LIBRARIES) - @echo " OCAMLC $<" - $(H)$(OCAMLC) -c $< -%.cmx: %.ml $(EXTRAS) $(LIBRARIES_OPT) - @echo " OCAMLOPT $<" - $(H)$(OCAMLOPT) -c $< -%.ml %.mli: %.mly $(EXTRAS) - @echo " OCAMLYACC $<" - $(H)$(OCAMLYACC) -v $< -%.ml: %.mll $(EXTRAS) - @echo " OCAMLLEX $<" - $(H)$(OCAMLLEX) $< - -include ../../../Makefile.defs - -ifeq ($(MAKECMDGOALS),) - include .depend -endif - -ifeq ($(MAKECMDGOALS), all) - include .depend -endif - -ifeq ($(MAKECMDGOALS), opt) - include .depend.opt -endif - -ifeq ($(MAKECMDGOALS), test) - include .depend -endif - -ifeq ($(MAKECMDGOALS), test.opt) - include .depend.opt -endif diff --git a/matita/components/binaries/heights/heights.conf.xml b/matita/components/binaries/heights/heights.conf.xml deleted file mode 100644 index 9ecb8b687..000000000 --- a/matita/components/binaries/heights/heights.conf.xml +++ /dev/null @@ -1,7 +0,0 @@ - - -
- mysql://mowgli.cs.unibo.it mowgli helm none legacy - legacy -
- diff --git a/matita/components/binaries/heights/heights.ml b/matita/components/binaries/heights/heights.ml deleted file mode 100644 index f77c6cb4d..000000000 --- a/matita/components/binaries/heights/heights.ml +++ /dev/null @@ -1,48 +0,0 @@ -module Registry = Helm_registry -module SQL = HSql -module DB = LibraryDb - -let tbl = Hashtbl.create 50147 -let ord = ref 1 -let conf_file = ref "heights.conf.xml" - -let rec mesure db_type dbd prim str = - try - let h, p = Hashtbl.find tbl str in - if prim then begin - if p > 0 then Printf.eprintf "Hit %2u: %s\n" (succ p) str; - Hashtbl.replace tbl str (h, succ p) - end; - h - with Not_found -> - let query = - Printf.sprintf "SELECT h_occurrence FROM refObj WHERE source = '%s'" - (SQL.escape db_type dbd str) - in - let result = SQL.exec db_type dbd query in - let f res = match res.(0) with - | Some str -> mesure db_type dbd false str - | None -> assert false - in - let hs = SQL.map result ~f in - let h = succ (List.fold_left max 0 hs) in - Printf.printf "%3u %5u %s\n" h !ord str; flush stdout; - ord := succ !ord; - let p = if prim then 1 else 0 in - Hashtbl.add tbl str (h, p); h - -let scan_objs db_type dbd = - let query = "SELECT source FROM objectName" in - let result = SQL.exec db_type dbd query in - let f res = match res.(0) with - | Some str -> ignore (mesure db_type dbd true str) - | None -> assert false - in - SQL.iter result ~f - -let _ = - Registry.load_from !conf_file; - let db_type = DB.dbtype_of_string (Registry.get_string "db.type") in - let db_spec = DB.parse_dbd_conf () in - let dbd = SQL.quick_connect db_spec in - scan_objs db_type dbd diff --git a/matita/components/binaries/transcript/grafite.ml b/matita/components/binaries/transcript/grafite.ml index 719b4854a..89f8d2d02 100644 --- a/matita/components/binaries/transcript/grafite.ml +++ b/matita/components/binaries/transcript/grafite.ml @@ -31,7 +31,6 @@ module NP = NotationPp module GP = GrafiteAstPp module G = GrafiteAst module H = HExtlib -module HG = Http_getter let floc = H.dummy_floc @@ -100,7 +99,7 @@ let out_alias och name uri = Printf.fprintf och "alias id \"%s\" = \"%s\".\n\n" name uri let check och src = - if HG.exists ~local:false src then () else + if Http_getter.exists ~local:false src then () else let msg = "UNAVAILABLE OBJECT: " ^ src in out_line_comment och msg; prerr_endline msg diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index e87795900..d428bad22 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -289,21 +289,6 @@ let eval_add_constraint status u1 u2 = status,`New [] ;; -let add_coercions_of_lemmas lemmas status = - let moo_content = - HExtlib.filter_map - (fun uri -> - match CoercDb.is_a_coercion (Cic.Const (uri,[])) with - | None -> None - | Some (_,tgt,_,sat,_) -> - let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in - Some (coercion_moo_statement_of (uri,arity,sat,0))) - lemmas - in - let status = GrafiteTypes.add_moo_content moo_content status in - status#set_coercions (CoercDb.dump ()), - lemmas - let eval_ng_punct (_text, _prefix_len, punct) = match punct with | GrafiteAst.Dot _ -> NTactics.dot_tac diff --git a/matita/components/grafite_engine/grafiteSync.ml b/matita/components/grafite_engine/grafiteSync.ml index 8e925db62..60c366a0e 100644 --- a/matita/components/grafite_engine/grafiteSync.ml +++ b/matita/components/grafite_engine/grafiteSync.ml @@ -55,24 +55,6 @@ let uris_for_inductive_type uri obj = | _ -> [uri] ;; -let add_coercion ~pack_coercion_obj ~add_composites status uri arity - saturations baseuri -= - let lemmas = - LibrarySync.add_coercion ~add_composites ~pack_coercion_obj - uri arity saturations baseuri in - let status = - (status - #set_coercions (CoercDb.dump ())) ; - #set_objects (lemmas @ status#objects) - in - let status = NCicCoercion.index_old_db (CoercDb.dump ()) status in - status, lemmas - -let prefer_coercion status u = - CoercDb.prefer u; - status#set_coercions (CoercDb.dump ()) - (** @return l2 \ l1 *) let uri_list_diff l2 l1 = let module S = UriManager.UriSet in @@ -86,25 +68,17 @@ let initial_status lexicon_status baseuri = ;; let time_travel ~present ?(past=initial_status present present#baseuri) () = - let objs_to_remove = - uri_list_diff present#objects past#objects in - List.iter LibrarySync.remove_obj objs_to_remove; - CoercDb.restore past#coercions; NCicLibrary.time_travel past ;; let init lexicon_status = - CoercDb.restore CoercDb.empty_coerc_db; - LibraryObjects.reset_defaults (); initial_status lexicon_status ;; let pop () = - LibrarySync.pop (); LibraryObjects.pop () ;; let push () = - LibrarySync.push (); LibraryObjects.push () ;; diff --git a/matita/components/grafite_engine/grafiteSync.mli b/matita/components/grafite_engine/grafiteSync.mli index 5b4971132..9f562ad86 100644 --- a/matita/components/grafite_engine/grafiteSync.mli +++ b/matita/components/grafite_engine/grafiteSync.mli @@ -23,16 +23,6 @@ * http://helm.cs.unibo.it/ *) -val add_coercion: - pack_coercion_obj:(Cic.obj -> Cic.obj) -> - add_composites:bool -> GrafiteTypes.status -> - UriManager.uri -> int -> int -> - string (* baseuri *) -> - GrafiteTypes.status * UriManager.uri list - -val prefer_coercion: - GrafiteTypes.status -> UriManager.uri -> GrafiteTypes.status - val time_travel: present:GrafiteTypes.status -> ?past:GrafiteTypes.status -> unit -> unit diff --git a/matita/components/grafite_engine/grafiteTypes.ml b/matita/components/grafite_engine/grafiteTypes.ml index 618d20050..7f264d6fa 100644 --- a/matita/components/grafite_engine/grafiteTypes.ml +++ b/matita/components/grafite_engine/grafiteTypes.ml @@ -39,15 +39,12 @@ class status = fun (b : string) -> object val moo_content_rev = ([] : GrafiteMarshal.moo) val objects = ([] : UriManager.uri list) - val coercions = CoercDb.empty_coerc_db val baseuri = b val ng_mode = (`CommandMode : [`CommandMode | `ProofMode]) method moo_content_rev = moo_content_rev method set_moo_content_rev v = {< moo_content_rev = v >} method objects = objects method set_objects v = {< objects = v >} - method coercions = coercions - method set_coercions v = {< coercions = v >} method baseuri = baseuri method set_baseuri v = {< baseuri = v >} method ng_mode = ng_mode; diff --git a/matita/components/grafite_engine/grafiteTypes.mli b/matita/components/grafite_engine/grafiteTypes.mli index 03a5c05d3..bfa5f9cdb 100644 --- a/matita/components/grafite_engine/grafiteTypes.mli +++ b/matita/components/grafite_engine/grafiteTypes.mli @@ -38,8 +38,6 @@ class status : method set_moo_content_rev: GrafiteMarshal.moo -> 'self method objects: UriManager.uri list method set_objects: UriManager.uri list -> 'self - method coercions: CoercDb.coerc_db - method set_coercions: CoercDb.coerc_db -> 'self method baseuri: string method set_baseuri: string -> 'self method ng_mode: [`ProofMode | `CommandMode] diff --git a/matita/components/hmysql/.depend b/matita/components/hmysql/.depend deleted file mode 100644 index ce439d961..000000000 --- a/matita/components/hmysql/.depend +++ /dev/null @@ -1,7 +0,0 @@ -hSql.cmi: -hSqlite3.cmo: -hSqlite3.cmx: -hMysql.cmo: -hMysql.cmx: -hSql.cmo: hSqlite3.cmo hMysql.cmo hSql.cmi -hSql.cmx: hSqlite3.cmx hMysql.cmx hSql.cmi diff --git a/matita/components/hmysql/.depend.opt b/matita/components/hmysql/.depend.opt deleted file mode 100644 index c2289bff2..000000000 --- a/matita/components/hmysql/.depend.opt +++ /dev/null @@ -1,7 +0,0 @@ -hSql.cmi: -hSqlite3.cmo: -hSqlite3.cmx: -hMysql.cmo: -hMysql.cmx: -hSql.cmo: hSqlite3.cmx hMysql.cmx hSql.cmi -hSql.cmx: hSqlite3.cmx hMysql.cmx hSql.cmi diff --git a/matita/components/hmysql/Makefile b/matita/components/hmysql/Makefile deleted file mode 100644 index 356e6e068..000000000 --- a/matita/components/hmysql/Makefile +++ /dev/null @@ -1,14 +0,0 @@ -PACKAGE = hmysql -PREDICATES = - -INTERFACE_FILES = \ - hSql.mli -IMPLEMENTATION_FILES = \ - hSqlite3.ml \ - hMysql.ml \ - $(INTERFACE_FILES:%.mli=%.ml) -EXTRA_OBJECTS_TO_INSTALL = -EXTRA_OBJECTS_TO_CLEAN = - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/hmysql/hMysql.ml b/matita/components/hmysql/hMysql.ml deleted file mode 100644 index b9ace8e83..000000000 --- a/matita/components/hmysql/hMysql.ml +++ /dev/null @@ -1,92 +0,0 @@ -(* Copyright (C) 2005, 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/. - *) - -(* $Id$ *) - -type dbd = Mysql.dbd option -type result = Mysql.result option -type error_code = - | OK - | Table_exists_error - | Dup_keyname - | No_such_table - | No_such_index - | Bad_table_error - | GENERIC_ERROR of string -exception Error of string - -let profiler = HExtlib.profile "mysql" - -let quick_connect ?host ?database ?port ?password ?user () = - profiler.HExtlib.profile - (fun () -> - Some (Mysql.quick_connect ?host ?database ?port ?password ?user ())) - () -;; - -let disconnect = function - | None -> () - | Some dbd -> profiler.HExtlib.profile Mysql.disconnect dbd - -let escape s = - profiler.HExtlib.profile Mysql.escape s - -let exec s dbd = - match dbd with - | None -> None - | Some dbd -> - try - Some (profiler.HExtlib.profile (Mysql.exec dbd) s) - with Mysql.Error s -> raise (Error s) - -let map res ~f = - match res with - | None -> [] - | Some res -> - let map f = Mysql.map res ~f in - profiler.HExtlib.profile map f - -let iter res ~f = - match res with - | None -> () - | Some res -> - let iter f = Mysql.iter res ~f in - profiler.HExtlib.profile iter f - -let errno = function - | None -> GENERIC_ERROR "Mysql.Connection_error" - | Some dbd -> - match Mysql.errno dbd with - | Mysql.No_such_table -> No_such_table - | Mysql.Table_exists_error -> Table_exists_error - | Mysql.Dup_keyname -> Dup_keyname - | Mysql.No_such_index -> No_such_index - | Mysql.Bad_table_error -> Bad_table_error - | _ -> GENERIC_ERROR "Mysql_generic_error" -;; - -let isMysql = true - -let escape_string_for_like = ("ESCAPE \"\\\\\"" : ('a,'b,'c,'a) format4);; diff --git a/matita/components/hmysql/hSql.ml b/matita/components/hmysql/hSql.ml deleted file mode 100644 index ad2b55993..000000000 --- a/matita/components/hmysql/hSql.ml +++ /dev/null @@ -1,178 +0,0 @@ -(* Copyright (C) 2005, 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 error_code = - | OK - | Table_exists_error - | Dup_keyname - | No_such_table - | No_such_index - | Bad_table_error - | GENERIC_ERROR of string - -exception Error of string - -(* the exceptions raised are from the Mysql module *) - -type dbtype = User | Library | Legacy -type dbimplementation = Mysql of HMysql.dbd | Sqlite of HSqlite3.dbd | FakeMySql -type result = Mysql_rc of HMysql.result | Sqlite_rc of HSqlite3.result | Nothing - - (* host port dbname user password type *) -type dbspec = (string * int option * string * string * string option * dbtype) list -type dbd = (dbtype * dbimplementation) list - -let debug = false;; -let debug_print s = if debug then prerr_endline (Lazy.force s) else ();; - -let pp_dbtype = function - | User -> "User" - | Library -> "Library" - | Legacy -> "Legacy" -;; - -let mk_dbspec l = l;; - -let quick_connect dbspec = - HExtlib.filter_map - (fun (host, port, database, user, password, kind) -> - if Pcre.pmatch ~pat:"^file://" host then - Some (kind, (Sqlite (HSqlite3.quick_connect (kind = Library) - ~host:(Pcre.replace ~pat:"^file://" host) - ?port ~user ~database ?password ()))) - else if Pcre.pmatch ~pat:"^mysql://" host then - Some (kind, (Mysql (HMysql.quick_connect - ~host:(Pcre.replace ~pat:"^mysql://" host) - ?port ~user ~database ?password ()))) - else - None) - dbspec -;; - -let mk f1 f2 = function - | (Sqlite dbd) -> Sqlite_rc (f1 dbd) - | (Mysql dbd) -> Mysql_rc (f2 dbd) - | FakeMySql -> assert false -;; - -let mk_u f1 f2 = function - | (_, (Sqlite dbd)) -> f1 dbd - | (_, (Mysql dbd)) -> f2 dbd - | (_, FakeMySql) -> assert false -;; - -let wrap f x = - try f x with - | HMysql.Error s | HSqlite3.Error s -> raise (Error s) - | Not_found -> raise (Error "Not_found") -;; - -let disconnect dbd = - wrap (List.iter (mk_u HSqlite3.disconnect HMysql.disconnect)) dbd -;; - -let exec (dbtype : dbtype) (dbd : dbd) (query : string) = - try - debug_print (lazy ("EXEC: " ^ pp_dbtype dbtype ^ "|" ^ query)); - let dbd = List.assoc dbtype dbd in - wrap (mk (HSqlite3.exec query) (HMysql.exec query)) dbd - with Not_found -> Nothing -;; - -let map result ~f = - match result with - | Mysql_rc rc -> HMysql.map rc ~f - | Sqlite_rc rc -> HSqlite3.map rc ~f - | Nothing -> [] -;; - -let iter result ~f = - match result with - | Mysql_rc rc -> HMysql.iter rc ~f - | Sqlite_rc rc -> HSqlite3.iter rc ~f - | Nothing -> () -;; - -let sqlite_err = function - | HSqlite3.OK -> OK - | HSqlite3.Table_exists_error -> Table_exists_error - | HSqlite3.Dup_keyname -> Dup_keyname - | HSqlite3.No_such_table -> No_such_table - | HSqlite3.No_such_index -> No_such_index - | HSqlite3.Bad_table_error -> Bad_table_error - | HSqlite3.GENERIC_ERROR s -> GENERIC_ERROR s -;; - -let mysql_err = function - | HMysql.OK -> OK - | HMysql.Table_exists_error -> Table_exists_error - | HMysql.Dup_keyname -> Dup_keyname - | HMysql.No_such_table -> No_such_table - | HMysql.No_such_index -> No_such_index - | HMysql.Bad_table_error -> Bad_table_error - | HMysql.GENERIC_ERROR s -> GENERIC_ERROR s -;; - -let errno dbtype dbd = - wrap - (fun d -> - try - match List.assoc dbtype d with - | Mysql dbd -> mysql_err (HMysql.errno dbd) - | Sqlite dbd -> sqlite_err (HSqlite3.errno dbd) - | FakeMySql -> assert false - with Not_found -> OK) - dbd -;; - -let escape dbtype dbd s = - try - match List.assoc dbtype dbd with - | Mysql _ | FakeMySql -> wrap HMysql.escape s - | Sqlite _ -> wrap HSqlite3.escape s - with Not_found -> s -;; - -let escape_string_for_like dbtype dbd = - try - match List.assoc dbtype dbd with - | Mysql _ | FakeMySql -> HMysql.escape_string_for_like - | Sqlite _ -> HSqlite3.escape_string_for_like - with Not_found -> - ("ESCAPE \"\\\"" : ('a,'b,'c,'a) format4) -;; - -let isMysql dbtype dbd = - wrap - (fun d -> - try - match List.assoc dbtype d with Mysql _ -> true | _ -> false - with Not_found -> false) - dbd -;; - -let fake_db_for_mysql dbtype = - [dbtype, FakeMySql] -;; diff --git a/matita/components/hmysql/hSql.mli b/matita/components/hmysql/hSql.mli deleted file mode 100644 index 3c7de40cc..000000000 --- a/matita/components/hmysql/hSql.mli +++ /dev/null @@ -1,70 +0,0 @@ -(* Copyright (C) 2005, 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 dbd -type result -type error_code = - | OK - | Table_exists_error - | Dup_keyname - | No_such_table - | No_such_index - | Bad_table_error - | GENERIC_ERROR of string - -exception Error of string - -(* the exceptions raised are from the Mysql module *) - -type dbtype = User | Library | Legacy - - (* host port dbname user password type *) -type dbspec - -val mk_dbspec : - (string * int option * string * string * string option * dbtype) list -> - dbspec - -val quick_connect : dbspec -> dbd - -val disconnect : dbd -> unit - -val exec: dbtype -> dbd -> string -> result -val map : result -> f:(string option array -> 'a) -> 'a list -val iter : result -> f:(string option array -> unit) -> unit - - -val errno : dbtype -> dbd -> error_code -(* val status : dbd -> Mysql.status *) - -val escape: dbtype -> dbd -> string -> string - -val escape_string_for_like: dbtype -> dbd -> ('a,'b,'c,'a) format4 - -val isMysql : dbtype -> dbd -> bool - -(* this dbd can't do queries, used only in table_creator *) -val fake_db_for_mysql: dbtype -> dbd - diff --git a/matita/components/hmysql/hSqlite3.ml b/matita/components/hmysql/hSqlite3.ml deleted file mode 100644 index 707b482bc..000000000 --- a/matita/components/hmysql/hSqlite3.ml +++ /dev/null @@ -1,234 +0,0 @@ -(* Copyright (C) 2005, 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/. - *) - -(* $Id: hMysql.ml 5769 2006-01-08 18:00:22Z sacerdot $ *) - -(* -type result = Mysql.result option -*) - - -let debug = false -let debug_print = - if debug then prerr_endline else (fun _ ->()) -;; - -type result = Sqlite3.row list -type dbd = Sqlite3.db option - -type error_code = - | OK - | Table_exists_error - | Dup_keyname - | No_such_table - | No_such_index - | Bad_table_error - | GENERIC_ERROR of string - -exception Error of string - -let profiler = HExtlib.profile "Sqlite3" - -let quick_connect - is_library - ?(host = Helm_registry.get "matita.basedir") - ?(database = "sqlite") ?port ?password ?user () -= - let username = Helm_registry.get "user.name" in - let host_mangled = Pcre.replace ~pat:"[/ .]" ~templ:"_" host in - let find_db _ = - let base = "matita.db." ^ username ^ "." ^ host_mangled ^ "." in - let root = "/dev/shm/" in - let files = HExtlib.find ~test:(Pcre.pmatch ~pat:(base^"[0-9]+")) root in - let rec aux = function - | [] -> - debug_print ("HSqlite3: no valid db files found in memory"); - let name = root ^ base ^ string_of_int (Unix.getpid ()) in - debug_print ("HSqlite3: memory db file name: "^name); - name, true - | x::tl -> - debug_print ("HSqlite3: found a .db in memory: " ^ x); - match Array.to_list (Pcre.extract ~pat:"\\.([0-9]+)$" x) with - | [] | _::_::_::_ -> assert false - | [_;p] when HExtlib.is_dir ("/proc/" ^ p) -> - debug_print ("HSqlite3: found valid db file: " ^ x); - x, false - | _ -> - HLog.warn ("HSqlite3: dead process db file found: " ^ x); - HLog.warn ("HSqlite3: removing: " ^ x); - ignore (Sys.command ("rm " ^ x)); - aux tl - in - aux files - in - let db_name = host ^ "/" ^ database in - let db_to_open = - if HExtlib.is_dir "/dev/shm/" && HExtlib.writable_dir "/dev/shm/" - && (not is_library) - then ( - let tmp_db_name, first_time = find_db () in - let cp_to_ram_cmd = "cp " ^ db_name ^ " " ^ tmp_db_name in - if first_time then - if HExtlib.is_regular db_name then ignore (Sys.command cp_to_ram_cmd) - else debug_print ("HSqlite3: no initial db: " ^ db_name) - else debug_print "HSqlite3: not copying the db, already in memory"; - let mv_to_disk_cmd _ = - if first_time then ignore (Sys.command ("mv "^tmp_db_name^" "^db_name)) - else debug_print "HSqlite3: not copying back the db" - in - at_exit mv_to_disk_cmd; - tmp_db_name) - else - db_name - in - HExtlib.mkdir (Filename.dirname db_to_open); - let db = Sqlite3.db_open db_to_open in - (* attach the REGEX function *) - Sqlite3.create_fun2 db "REGEXP" - (fun s rex -> - try - match rex, s with - | Sqlite3.Data.TEXT rex, Sqlite3.Data.BLOB s - | Sqlite3.Data.TEXT rex, Sqlite3.Data.TEXT s -> - let r = Str.regexp rex in - if Str.string_match r s 0 then - Sqlite3.Data.INT 1L - else - Sqlite3.Data.INT 0L - | _ -> raise (Error "wrong types to 'REGEXP'") - with Sys.Break -> Sqlite3.Data.INT 0L - | exn -> HLog.error (Printexc.to_string exn); raise exn); - Some db -;; - -let disconnect db = - match db with - | None -> () - | Some db -> - let b = Sqlite3.db_close db in - if b=false then debug_print "No Closed DataBase" -;; - -(* XXX hack, sqlite has a print "%q" that should be used, but is not bound *) -let escape s = - let s_escaped = Pcre.replace ~pat:"'" ~templ:"''" s in - (*let s_escaped = Pcre.replace ~pat:"([^'])'([^'])" ~templ:"$1''$2" s in*) - debug_print s; - debug_print s_escaped; - s_escaped -;; - -let string_of_rc = function - |Sqlite3.Rc.OK -> "Sqlite3.Rc.OK" - |Sqlite3.Rc.ERROR -> "Sqlite3.Rc.ERROR" - |Sqlite3.Rc.INTERNAL -> "Sqlite3.Rc.INTERNAL" - |Sqlite3.Rc.PERM -> "Sqlite3.Rc.PERM" - |Sqlite3.Rc.ABORT -> "Sqlite3.Rc.ABORT" - |Sqlite3.Rc.BUSY -> "Sqlite3.Rc.BUSY" - |Sqlite3.Rc.LOCKED -> "Sqlite3.Rc.LOCKED" - |Sqlite3.Rc.NOMEM -> "Sqlite3.Rc.NOMEM" - |Sqlite3.Rc.READONLY -> "Sqlite3.Rc.READONLY" - |Sqlite3.Rc.INTERRUPT -> "Sqlite3.Rc.INTERRUPT" - |Sqlite3.Rc.IOERR -> "Sqlite3.Rc.IOERR" - |Sqlite3.Rc.CORRUPT -> "Sqlite3.Rc.CORRUPT" - |Sqlite3.Rc.NOTFOUND -> "Sqlite3.Rc.NOTFOUND" - |Sqlite3.Rc.FULL -> "Sqlite3.Rc.FULL" - |Sqlite3.Rc.CANTOPEN -> "Sqlite3.Rc.CANTOPEN" - |Sqlite3.Rc.PROTOCOL -> "Sqlite3.Rc.PROTOCOL" - |Sqlite3.Rc.EMPTY -> "Sqlite3.Rc.EMPTY" - |Sqlite3.Rc.SCHEMA -> "Sqlite3.Rc.SCHEMA" - |Sqlite3.Rc.TOOBIG -> "Sqlite3.Rc.TOOBIG" - |Sqlite3.Rc.CONSTRAINT -> "Sqlite3.Rc.CONSTRAINT" - |Sqlite3.Rc.MISMATCH -> "Sqlite3.Rc.MISMATCH" - |Sqlite3.Rc.MISUSE -> "Sqlite3.Rc.MISUSE" - |Sqlite3.Rc.NOFLS -> "Sqlite3.Rc.NOFLS" - |Sqlite3.Rc.AUTH -> "Sqlite3.Rc.AUTH" - |Sqlite3.Rc.FORMAT -> "Sqlite3.Rc.FORMAT" - |Sqlite3.Rc.RANGE -> "Sqlite3.Rc.RANGE" - |Sqlite3.Rc.NOTADB -> "Sqlite3.Rc.NOTADB" - |Sqlite3.Rc.ROW -> "Sqlite3.Rc.ROW" - |Sqlite3.Rc.DONE -> "Sqlite3.Rc.DONE" - |Sqlite3.Rc.UNKNOWN n -> - "Sqlite3.Rc.UNKNOWN " ^ string_of_int (Sqlite3.Rc.int_of_unknown n) -;; - -let pp_rc rc = debug_print (string_of_rc rc);; - -let exec s db = - debug_print s; - let stored_result = ref [] in - let store row = - stored_result := row :: !stored_result - in - match db with - | None -> [] - | Some db -> - let rc = - profiler.HExtlib.profile (Sqlite3.exec_no_headers db ~cb:store) s - in - match rc with - | Sqlite3.Rc.OK -> !stored_result - | _ -> raise (Error (string_of_rc rc ^ ": " ^ Sqlite3.errmsg db )) -;; - -let rec map res ~f = - let map f = List.map f res in - profiler.HExtlib.profile map f -;; - -let iter res ~f = - let iter f = List.iter f res in - profiler.HExtlib.profile iter f -;; - -let errno = function - | None -> OK - | Some db -> - match Sqlite3.errcode db with - |Sqlite3.Rc.OK -> OK - |Sqlite3.Rc.ERROR -> - let errmsg = (Sqlite3.errmsg db) in - if Pcre.pmatch errmsg ~pat:"^table .* already exists" then - Table_exists_error - else - if Pcre.pmatch errmsg ~pat:"^index .* already exists" then Dup_keyname - else if Pcre.pmatch errmsg ~pat:"^no such table: .*" then No_such_table - else if Pcre.pmatch errmsg ~pat:"^no such index: .*" then No_such_index - else GENERIC_ERROR errmsg - |Sqlite3.Rc.INTERNAL |Sqlite3.Rc.PERM |Sqlite3.Rc.ABORT - |Sqlite3.Rc.BUSY |Sqlite3.Rc.LOCKED |Sqlite3.Rc.NOMEM - |Sqlite3.Rc.READONLY |Sqlite3.Rc.INTERRUPT |Sqlite3.Rc.IOERR - |Sqlite3.Rc.CORRUPT |Sqlite3.Rc.NOTFOUND |Sqlite3.Rc.FULL - |Sqlite3.Rc.CANTOPEN |Sqlite3.Rc.PROTOCOL |Sqlite3.Rc.EMPTY - |Sqlite3.Rc.SCHEMA |Sqlite3.Rc.TOOBIG |Sqlite3.Rc.CONSTRAINT - |Sqlite3.Rc.MISMATCH |Sqlite3.Rc.MISUSE |Sqlite3.Rc.NOFLS - |Sqlite3.Rc.AUTH |Sqlite3.Rc.FORMAT |Sqlite3.Rc.RANGE - |Sqlite3.Rc.NOTADB |Sqlite3.Rc.ROW |Sqlite3.Rc.DONE - |Sqlite3.Rc.UNKNOWN _ -> GENERIC_ERROR "Sqlite3_generic_error" -;; - -let isMysql = false - -let escape_string_for_like = ("ESCAPE \"\\\"" : ('a,'b,'c,'a) format4);; diff --git a/matita/components/library/.depend b/matita/components/library/.depend deleted file mode 100644 index cfa1295ed..000000000 --- a/matita/components/library/.depend +++ /dev/null @@ -1,32 +0,0 @@ -librarian.cmi: -libraryMisc.cmi: -libraryDb.cmi: -coercDb.cmi: -cicCoercion.cmi: coercDb.cmi -librarySync.cmi: -cicElim.cmi: -cicRecord.cmi: -cicFix.cmi: -libraryClean.cmi: -librarian.cmo: librarian.cmi -librarian.cmx: librarian.cmi -libraryMisc.cmo: libraryMisc.cmi -libraryMisc.cmx: libraryMisc.cmi -libraryDb.cmo: libraryDb.cmi -libraryDb.cmx: libraryDb.cmi -coercDb.cmo: coercDb.cmi -coercDb.cmx: coercDb.cmi -cicCoercion.cmo: coercDb.cmi cicCoercion.cmi -cicCoercion.cmx: coercDb.cmx cicCoercion.cmi -librarySync.cmo: libraryDb.cmi coercDb.cmi cicCoercion.cmi librarySync.cmi -librarySync.cmx: libraryDb.cmx coercDb.cmx cicCoercion.cmx librarySync.cmi -cicElim.cmo: librarySync.cmi cicElim.cmi -cicElim.cmx: librarySync.cmx cicElim.cmi -cicRecord.cmo: librarySync.cmi cicRecord.cmi -cicRecord.cmx: librarySync.cmx cicRecord.cmi -cicFix.cmo: librarySync.cmi cicFix.cmi -cicFix.cmx: librarySync.cmx cicFix.cmi -libraryClean.cmo: librarySync.cmi libraryMisc.cmi libraryDb.cmi \ - libraryClean.cmi -libraryClean.cmx: librarySync.cmx libraryMisc.cmx libraryDb.cmx \ - libraryClean.cmi diff --git a/matita/components/library/.depend.opt b/matita/components/library/.depend.opt deleted file mode 100644 index cfa1295ed..000000000 --- a/matita/components/library/.depend.opt +++ /dev/null @@ -1,32 +0,0 @@ -librarian.cmi: -libraryMisc.cmi: -libraryDb.cmi: -coercDb.cmi: -cicCoercion.cmi: coercDb.cmi -librarySync.cmi: -cicElim.cmi: -cicRecord.cmi: -cicFix.cmi: -libraryClean.cmi: -librarian.cmo: librarian.cmi -librarian.cmx: librarian.cmi -libraryMisc.cmo: libraryMisc.cmi -libraryMisc.cmx: libraryMisc.cmi -libraryDb.cmo: libraryDb.cmi -libraryDb.cmx: libraryDb.cmi -coercDb.cmo: coercDb.cmi -coercDb.cmx: coercDb.cmi -cicCoercion.cmo: coercDb.cmi cicCoercion.cmi -cicCoercion.cmx: coercDb.cmx cicCoercion.cmi -librarySync.cmo: libraryDb.cmi coercDb.cmi cicCoercion.cmi librarySync.cmi -librarySync.cmx: libraryDb.cmx coercDb.cmx cicCoercion.cmx librarySync.cmi -cicElim.cmo: librarySync.cmi cicElim.cmi -cicElim.cmx: librarySync.cmx cicElim.cmi -cicRecord.cmo: librarySync.cmi cicRecord.cmi -cicRecord.cmx: librarySync.cmx cicRecord.cmi -cicFix.cmo: librarySync.cmi cicFix.cmi -cicFix.cmx: librarySync.cmx cicFix.cmi -libraryClean.cmo: librarySync.cmi libraryMisc.cmi libraryDb.cmi \ - libraryClean.cmi -libraryClean.cmx: librarySync.cmx libraryMisc.cmx libraryDb.cmx \ - libraryClean.cmi diff --git a/matita/components/library/Makefile b/matita/components/library/Makefile deleted file mode 100644 index 10f52c680..000000000 --- a/matita/components/library/Makefile +++ /dev/null @@ -1,18 +0,0 @@ -PACKAGE = library -PREDICATES = - -INTERFACE_FILES = \ - librarian.mli \ - libraryMisc.mli \ - libraryDb.mli \ - coercDb.mli \ - cicCoercion.mli \ - librarySync.mli \ - cicFix.mli \ - libraryClean.mli \ - $(NULL) -IMPLEMENTATION_FILES = \ - $(INTERFACE_FILES:%.mli=%.ml) - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/library/cicCoercion.ml b/matita/components/library/cicCoercion.ml deleted file mode 100644 index b45599ceb..000000000 --- a/matita/components/library/cicCoercion.ml +++ /dev/null @@ -1,40 +0,0 @@ -(* Copyright (C) 2005, 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://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -let close_coercion_graph_ref = ref - (fun _ _ _ _ _ -> [] : - CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> - string (* baseuri *) -> - (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj * - int * int) list) -;; - -let set_close_coercion_graph f = close_coercion_graph_ref := f;; - -let close_coercion_graph c1 c2 u sat s = - !close_coercion_graph_ref c1 c2 u sat s -;; diff --git a/matita/components/library/cicCoercion.mli b/matita/components/library/cicCoercion.mli deleted file mode 100644 index 8356de8cd..000000000 --- a/matita/components/library/cicCoercion.mli +++ /dev/null @@ -1,40 +0,0 @@ -(* Copyright (C) 2005, 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://helm.cs.unibo.it/ - *) - -(* This module implements the Coercions transitive closure *) - -val set_close_coercion_graph : - (CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> - string (* baseuri *) -> - (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * - int (* saturations *) * Cic.obj * int (* arity *) * int (* cpos *)) list) - -> unit - -val close_coercion_graph: - CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> - string (* baseuri *) -> - (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * - int (* saturations *) * Cic.obj * int (* arity *) * int (* cpos *)) list - diff --git a/matita/components/library/cicFix.ml b/matita/components/library/cicFix.ml deleted file mode 100644 index 21cb99093..000000000 --- a/matita/components/library/cicFix.ml +++ /dev/null @@ -1,69 +0,0 @@ -(* Copyright (C) 2004-2005, 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://helm.cs.unibo.it/ - *) - -(* $Id: librarySync.ml 9482 2009-01-08 18:12:28Z tassi $ *) - -let generate_sibling_mutual_definitions ~add_obj ~add_coercion uri obj = - match obj with - | Cic.Constant (name_to_avoid,Some bo,_,_,attrs) when - List.mem (`Flavour `MutualDefinition) attrs -> - (match bo with - Cic.Fix (_,funs) -> - snd ( - List.fold_right - (fun (name,idx,ty,bo) (n,uris) -> - if name = name_to_avoid then - (n-1,uris) - else - let uri = - UriManager.uri_of_string - (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in - let bo = Cic.Fix (n-1,funs) in - let obj = Cic.Constant (name,Some bo,ty,[],attrs) in - let lemmas = add_obj uri obj in - (n-1,lemmas @ uri::uris)) - (List.tl funs) (List.length funs,[])) - | Cic.CoFix (_,funs) -> - snd ( - List.fold_right - (fun (name,ty,bo) (n,uris) -> - if name = name_to_avoid then - (n-1,uris) - else - let uri = - UriManager.uri_of_string - (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in - let bo = Cic.CoFix (n-1,funs) in - let obj = Cic.Constant (name,Some bo,ty,[],attrs) in - let lemmas = add_obj uri obj in - (n-1,lemmas @ uri::uris)) - (List.tl funs) (List.length funs,[])) - | _ -> assert false) - | _ -> [] -;; - - -let init () = - LibrarySync.add_object_declaration_hook generate_sibling_mutual_definitions;; diff --git a/matita/components/library/cicFix.mli b/matita/components/library/cicFix.mli deleted file mode 100644 index de361cc7c..000000000 --- a/matita/components/library/cicFix.mli +++ /dev/null @@ -1,26 +0,0 @@ -(* Copyright (C) 2004-2005, 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://helm.cs.unibo.it/ - *) - -val init : unit -> unit diff --git a/matita/components/library/coercDb.ml b/matita/components/library/coercDb.ml deleted file mode 100644 index 0bd9461ca..000000000 --- a/matita/components/library/coercDb.ml +++ /dev/null @@ -1,177 +0,0 @@ -(* Copyright (C) 2005, 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://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -let debug = false -let debug_print = - if debug then fun x -> prerr_endline (Lazy.force x) - else ignore -;; - -type coerc_carr = - | Uri of UriManager.uri - | Sort of Cic.sort - | Fun of int - | Dead -;; - -type saturations = int -type coerced_pos = int -type coercion_entry = - coerc_carr * coerc_carr * UriManager.uri * saturations * coerced_pos - -type coerc_db = (* coercion_entry grouped by carrier with molteplicity *) - (coerc_carr * coerc_carr * - (UriManager.uri * int * saturations * coerced_pos) list) list - -let db = ref ([] : coerc_db) -let dump () = !db -let restore coerc_db = db := coerc_db -let empty_coerc_db = [] - -let rec coerc_carr_of_term t a = - try - match t, a with - | Cic.Sort s, 0 -> Sort s - | Cic.Appl (t::_), 0 -> coerc_carr_of_term t a - | t, 0 -> Uri (CicUtil.uri_of_term t) - | _, n -> Fun n - with Invalid_argument _ -> Dead -;; - -let string_of_carr = function - | Uri u -> UriManager.name_of_uri u - | Sort s -> CicPp.ppsort s - | Fun i -> "FunClass_" ^ string_of_int i - | Dead -> "UnsupportedCarrier" -;; - -let eq_carr ?(exact=false) src tgt = - assert false (* MATITA 1.0 - match src, tgt with - | Uri src, Uri tgt -> - let coarse_eq = UriManager.eq src tgt in - let t = CicUtil.term_of_uri src in - let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in - (match ty, exact with - | Cic.Prod _, true -> false - | Cic.Prod _, false -> coarse_eq - | _ -> coarse_eq) - | Sort _, Sort _ -> true - | Fun _,Fun _ when not exact -> true (* only one Funclass *) - | Fun i,Fun j when i = j -> true (* only one Funclass *) - | _, _ -> false - *) -;; - -let to_list db = - List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b,c -> a,b,c) l) db -;; - -let rec myfilter p = function - | [] -> [] - | (s,t,l)::tl -> - let l = - HExtlib.filter_map - (fun (u,n,saturations,cpos) as e -> - if p (s,t,u,saturations,cpos) then - if n = 1 then None - else Some (u,n-1,saturations,cpos) - else Some e) - l - in - if l = [] then myfilter p tl else (s,t,l)::myfilter p tl -;; - -let remove_coercion p = db := myfilter p !db;; - -let find_coercion f = - List.map - (fun (uri,_,saturations,_) -> uri,saturations) - (List.flatten - (HExtlib.filter_map (fun (s,t,l) -> if f (s,t) then Some l else None) !db)) -;; - -let is_a_coercion t = - try - let uri = CicUtil.uri_of_term t in - match - HExtlib.filter_map - (fun (src,tgt,xl) -> - let xl = List.filter (fun (x,_,_,_) -> UriManager.eq uri x) xl in - if xl = [] then None else Some (src,tgt,xl)) - !db - with - | [] -> None - | (_,_,[])::_ -> assert false - | [src,tgt,[u,_,s,p]] -> Some (src,tgt,u,s,p) - | (src,tgt,(u,_,s,p)::_)::_ -> - debug_print - (lazy "coercion has multiple entries, returning the first one"); - Some (src,tgt,u,s,p) - with Invalid_argument _ -> - debug_print (lazy "this term is not a constant"); - None -;; - -let add_coercion (src,tgt,u,saturations,cpos) = - let f s t = eq_carr s src && eq_carr t tgt in - let where = List.filter (fun (s,t,_) -> f s t) !db in - let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in - match where with - | [] -> db := (src,tgt,[u,1,saturations,cpos]) :: !db - | (src,tgt,l)::tl -> - assert (tl = []); (* not sure, this may be a feature *) - if List.exists (fun (x,_,_,_) -> UriManager.eq u x) l then - let l = - let l = - (* this code reorders the list so that adding an already declared - * coercion moves it to the begging of the list *) - let item = List.find (fun (x,_,_,_) -> UriManager.eq u x) l in - let rest=List.filter (fun (x,_,_,_) -> not (UriManager.eq u x)) l in - item :: rest - in - List.map - (fun (x,n,x_saturations,x_cpos) as e -> - if UriManager.eq u x then - (* not sure, this may be a feature *) - (assert (x_saturations = saturations && x_cpos = cpos); - (x,n+1,saturations,cpos)) - else e) - l - in - db := (src,tgt,l)::tl @ rest - else - db := (src,tgt,(u,1,saturations,cpos)::l)::tl @ rest -;; - -let prefer u = - let prefer (s,t,l) = - let lb,la = List.partition (fun (uri,_,_,_) -> UriManager.eq uri u) l in - s,t,lb@la - in - db := List.map prefer !db; -;; diff --git a/matita/components/library/coercDb.mli b/matita/components/library/coercDb.mli deleted file mode 100644 index 59c07f447..000000000 --- a/matita/components/library/coercDb.mli +++ /dev/null @@ -1,67 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - - -type coerc_carr = private - | Uri of UriManager.uri (* const, mutind, mutconstr *) - | Sort of Cic.sort (* Prop, Set, Type *) - | Fun of int - | Dead -;; - -val eq_carr: ?exact:bool -> coerc_carr -> coerc_carr -> bool -val string_of_carr: coerc_carr -> string - -(* takes a term in whnf ~delta:false and a desired ariety *) -val coerc_carr_of_term: Cic.term -> int -> coerc_carr - -type coerc_db -val empty_coerc_db : coerc_db -val dump: unit -> coerc_db -val restore: coerc_db -> unit - -val to_list: - coerc_db -> - (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list - -(* src carr, tgt carr, uri, saturations, coerced position - * invariant: - * if the constant pointed by uri has n argments - * n = coerced position + saturations + FunClass arity - *) - -type saturations = int -type coerced_pos = int -type coercion_entry = - coerc_carr * coerc_carr * UriManager.uri * saturations * coerced_pos -val add_coercion: coercion_entry -> unit -val remove_coercion: (coercion_entry -> bool) -> unit - -val find_coercion: - (coerc_carr * coerc_carr -> bool) -> (UriManager.uri * int) list - -val is_a_coercion: Cic.term -> coercion_entry option - -val prefer: UriManager.uri -> unit diff --git a/matita/components/library/librarian.ml b/matita/components/library/librarian.ml deleted file mode 100644 index 2c2ba6ff2..000000000 --- a/matita/components/library/librarian.ml +++ /dev/null @@ -1,418 +0,0 @@ -(* Copyright (C) 2005, 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://helm.cs.unibo.it/ - *) - -let debug = ref 0 - -let time_stamp = - let old = ref 0.0 in - fun msg -> - if !debug > 0 then begin - let times = Unix.times () in - let stamp = times.Unix.tms_utime +. times.Unix.tms_stime in - let lap = stamp -. !old in - Printf.eprintf "TIME STAMP (%s): %f\n" msg lap; flush stderr; - old := stamp - end - -exception NoRootFor of string - -let absolutize path = - let path = - if String.length path > 0 && path.[0] <> '/' then - Sys.getcwd () ^ "/" ^ path - else - path - in - HExtlib.normalize_path path -;; - - -let find_root path = - let path = absolutize path in - let paths = List.rev (Str.split (Str.regexp "/") path) in - let rec build = function - | he::tl as l -> ("/" ^ String.concat "/" (List.rev l) ^ "/") :: build tl - | [] -> ["/"] - in - let paths = List.map HExtlib.normalize_path (build paths) in - try HExtlib.find_in paths "root" - with Failure "find_in" -> - raise (NoRootFor (path ^ " (" ^ String.concat ", " paths ^ ")")) -;; - -let ensure_trailing_slash s = - if s = "" then "/" else - if s.[String.length s-1] <> '/' then s^"/" else s -;; - -let remove_trailing_slash s = - if s = "" then "" else - let len = String.length s in - if s.[len-1] = '/' then String.sub s 0 (len-1) else s -;; - -let load_root_file rootpath = - let data = HExtlib.input_file rootpath in - let lines = Str.split (Str.regexp "\n") data in - let clean s = - Pcre.replace ~pat:"[ \t]+" ~templ:" " - (Pcre.replace ~pat:"^ *" (Pcre.replace ~pat:" *$" s)) - in - List.map - (fun l -> - match Str.split (Str.regexp "=") l with - | [k;v] -> clean k, Http_getter_misc.strip_trailing_slash (clean v) - | _ -> raise (Failure ("Malformed root file: " ^ rootpath))) - lines -;; - -let find_root_for ~include_paths file = - let include_paths = "" :: Sys.getcwd () :: include_paths in - let rec find_path_for file = - try HExtlib.find_in include_paths file - with Failure "find_in" -> - if Filename.check_suffix file ".ma" then begin - let mma = Filename.chop_suffix file ".ma" ^ ".mma" in - HLog.warn ("We look for: " ^ mma); - let path = find_path_for mma in - Filename.chop_suffix path ".mma" ^ ".ma" - end else begin - HLog.error ("We are in: " ^ Sys.getcwd ()); - HLog.error ("Unable to find: "^file^"\nPaths explored:"); - List.iter (fun x -> HLog.error (" - "^x)) include_paths; - raise (NoRootFor file) - end - in - let path = find_path_for file in - let path = absolutize path in -(* HLog.debug ("file "^file^" resolved as "^path); *) - let rootpath, root, buri = - try - let mburi = Helm_registry.get "matita.baseuri" in - match Str.split (Str.regexp " ") mburi with - | [root; buri] when HExtlib.is_prefix_of root path -> - ":registry:", root, buri - | _ -> raise (Helm_registry.Key_not_found "matita.baseuri") - with Helm_registry.Key_not_found "matita.baseuri" -> - let rootpath = find_root path in - let buri = List.assoc "baseuri" (load_root_file rootpath) in - rootpath, Filename.dirname rootpath, buri - in -(* HLog.debug ("file "^file^" rooted by "^rootpath^""); *) - let uri = Http_getter_misc.strip_trailing_slash buri in - if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then - HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri); - ensure_trailing_slash root, remove_trailing_slash uri, path - -;; - -let mk_baseuri root extra = - let chop name = - assert(Filename.check_suffix name ".ma" || - Filename.check_suffix name ".mma"); - try Filename.chop_extension name - with Invalid_argument "Filename.chop_extension" -> name - in - remove_trailing_slash (HExtlib.normalize_path (root ^ "/" ^ chop extra)) -;; - -let baseuri_of_script ~include_paths file = - let root, buri, path = find_root_for ~include_paths file in - let path = HExtlib.normalize_path path in - let root = HExtlib.normalize_path root in - let lpath = Str.split (Str.regexp "/") path in - let lroot = Str.split (Str.regexp "/") root in - let rec substract l1 l2 = - match l1, l2 with - | h1::tl1,h2::tl2 when h1 = h2 -> substract tl1 tl2 - | l,[] -> l - | _ -> raise (NoRootFor (file ^" "^path^" "^root)) - in - let extra_buri = substract lpath lroot in - let extra = String.concat "/" extra_buri in - root, - mk_baseuri buri extra, - path, - extra -;; - -let find_roots_in_dir dir = - HExtlib.find ~test:(fun f -> - Filename.basename f = "root" && - try (Unix.stat f).Unix.st_kind = Unix.S_REG - with Unix.Unix_error _ -> false) - dir -;; - -(* make *) -let load_deps_file f = - let deps = ref [] in - let ic = open_in f in - try - while true do - begin - let l = input_line ic in - match Str.split (Str.regexp " ") l with - | [] -> - HLog.error ("Malformed deps file: " ^ f); - raise (Failure ("Malformed deps file: " ^ f)) - | he::tl -> deps := (he,tl) :: !deps - end - done; !deps - with End_of_file -> !deps -;; - -type options = (string * string) list - -module type Format = - sig - type source_object - type target_object - val load_deps_file: string -> (source_object * source_object list) list - val string_of_source_object: source_object -> string - val string_of_target_object: target_object -> string - val build: options -> source_object -> bool - val root_and_target_of: - options -> source_object -> - (* root, relative source, writeable target, read only target *) - string option * source_object * target_object * target_object - val mtime_of_source_object: source_object -> float option - val mtime_of_target_object: target_object -> float option - val is_readonly_buri_of: options -> source_object -> bool - end - -module Make = functor (F:Format) -> struct - - type status = Done of bool - | Ready of bool - - let say s = if !debug > 0 then prerr_endline ("make: "^s);; - - let unopt_or_call x f y = match x with Some _ -> x | None -> f y;; - - let fst4 = function (x,_,_,_) -> x;; - - let modified_before_s_t (_,cs, ct, _, _) a b = - - if !debug > 1 then time_stamp ("L s_t: a " ^ F.string_of_source_object a); - if !debug > 1 then time_stamp ("L s_t: b " ^ F.string_of_target_object b); - - let a = try Hashtbl.find cs a with Not_found -> assert false in - let b = - try - match Hashtbl.find ct b with - | Some _ as x -> x - | None -> - match F.mtime_of_target_object b with - | Some t as x -> - Hashtbl.remove ct b; - Hashtbl.add ct b x; x - | x -> x - with Not_found -> assert false - in - let r = match a, b with - | Some a, Some b -> a <= b - | _ -> false - in - - if !debug > 1 then time_stamp ("L s_t: " ^ string_of_bool r); - - r - - let modified_before_t_t (_,_,ct, _, _) a b = - - if !debug > 1 then time_stamp ("L t_t: a " ^ F.string_of_target_object a); - if !debug > 1 then time_stamp ("L t_t: b " ^ F.string_of_target_object b); - - let a = - try - match Hashtbl.find ct a with - | Some _ as x -> x - | None -> - match F.mtime_of_target_object a with - | Some t as x -> - Hashtbl.remove ct a; - Hashtbl.add ct a x; x - | x -> x - with Not_found -> assert false - in - let b = - try - match Hashtbl.find ct b with - | Some _ as x -> x - | None -> - match F.mtime_of_target_object b with - | Some t as x -> - Hashtbl.remove ct b; - Hashtbl.add ct b x; x - | x -> x - with Not_found -> assert false - in - let r = match a, b with - | Some a, Some b -> - - if !debug > 1 then time_stamp ("tt: a " ^ string_of_float a); - if !debug > 1 then time_stamp ("tt: b " ^ string_of_float b); - - a <= b - | _ -> false - in - - if !debug > 1 then time_stamp ("L t_t: " ^ string_of_bool r); - - r - - let rec purge_unwanted_roots wanted deps = - let roots, rest = - List.partition - (fun (t,_,d,_,_) -> - not (List.exists (fun (_,_,d1,_,_) -> List.mem t d1) deps)) - deps - in - let newroots = List.filter (fun (t,_,_,_,_) -> List.mem t wanted) roots in - if newroots = roots then - deps - else - purge_unwanted_roots wanted (newroots @ rest) - ;; - - let is_not_ro (opts,_,_,_,_) (f,_,_,r,_) = - match r with - | Some root -> not (F.is_readonly_buri_of opts f) - | None -> assert false - ;; - -(* FG: new sorting algorithm ************************************************) - - let rec make_aux root opts ok deps = - List.fold_left (make_one root opts) ok deps - - and make_one root opts ok what = - let lo, _, ct, cc, cd = opts in - let t, path, deps, froot, tgt = what in - let str = F.string_of_source_object t in - let map (okd, okt) d = - let (_, _, _, _, tgtd) as whatd = (Hashtbl.find cd d) in - let r = make_one root opts okd whatd in - r, okt && modified_before_t_t opts tgtd tgt - in - time_stamp ("L : processing " ^ str); - try - let r = Hashtbl.find cc t in - time_stamp ("L : " ^ string_of_bool r ^ " " ^ str); - ok && r -(* say "already built" *) - with Not_found -> - let okd, okt = List.fold_left map (true, modified_before_s_t opts t tgt) deps in - let res = - if okd then - if okt then true else - let build path = match froot with - | Some froot when froot = root -> - if is_not_ro opts what then F.build lo path else - (HLog.error ("Read only baseuri for: " ^ str ^ - ", I won't compile it even if it is out of date"); - false) - | Some froot -> make froot [path] - | None -> HLog.error ("No root for: " ^ str); false - in - Hashtbl.remove ct tgt; - Hashtbl.add ct tgt None; - time_stamp ("L : BUILDING " ^ str); - let res = build path in - time_stamp ("L : DONE " ^ str); res - else false - in - time_stamp ("L : " ^ string_of_bool res ^ " " ^ str); - Hashtbl.add cc t res; ok && res - -(****************************************************************************) - - and make root targets = - time_stamp "L : ENTERING"; - HLog.debug ("Entering directory '"^root^"'"); - let old_root = Sys.getcwd () in - Sys.chdir root; - let deps = F.load_deps_file (root^"/depends") in - let local_options = load_root_file (root^"/root") in - let baseuri = List.assoc "baseuri" local_options in - print_endline ("Entering HELM directory: " ^ baseuri); flush stdout; - let caches,cachet,cachec,cached = - Hashtbl.create 73, Hashtbl.create 73, Hashtbl.create 73, Hashtbl.create 73 - in - (* deps are enriched with these informations to sped up things later *) - let deps = - List.map - (fun (file,d) -> - let r,path,wtgt,rotgt = F.root_and_target_of local_options file in - Hashtbl.add caches file (F.mtime_of_source_object file); - (* if a read only target exists, we use that one, otherwise - we use the writeable one that may be compiled *) - let _,_,_,_, tgt as tuple = - match F.mtime_of_target_object rotgt with - | Some _ as mtime -> - Hashtbl.add cachet rotgt mtime; - (file, path, d, r, rotgt) - | None -> - Hashtbl.add cachet wtgt (F.mtime_of_target_object wtgt); - (file, path, d, r, wtgt) - in - Hashtbl.add cached file tuple; - tuple - ) - deps - in - let opts = local_options, caches, cachet, cachec, cached in - let ok = - if targets = [] then - make_aux root opts true deps - else - make_aux root opts true (purge_unwanted_roots targets deps) - in - print_endline ("Leaving HELM directory: " ^ baseuri); flush stdout; - HLog.debug ("Leaving directory '"^root^"'"); - Sys.chdir old_root; - time_stamp "L : LEAVING"; - ok - ;; - -end - -let write_deps_file where deps = match where with - | Some root -> - let oc = open_out (root ^ "/depends") in - let map (t, d) = output_string oc (t^" "^String.concat " " d^"\n") in - List.iter map deps; close_out oc; - HLog.message ("Generated: " ^ root ^ "/depends") - | None -> - print_endline (String.concat " " (List.flatten (List.map snd deps))) - -(* FG ***********************************************************************) - -(* scheme uri part as defined in URI Generic Syntax (RFC 3986) *) -let uri_scheme_rex = Pcre.regexp "^[[:alpha:]][[:alnum:]\-+.]*:" - -let is_uri str = - Pcre.pmatch ~rex:uri_scheme_rex str diff --git a/matita/components/library/librarian.mli b/matita/components/library/librarian.mli deleted file mode 100644 index 4eed9051d..000000000 --- a/matita/components/library/librarian.mli +++ /dev/null @@ -1,105 +0,0 @@ -(* Copyright (C) 2004-2008, 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://helm.cs.unibo.it/ - *) - -exception NoRootFor of string - -(* make a relative path absolute *) -val absolutize: string -> string - -(* a root file is a text, line oriented, file containing pairs separated by - * the '=' character. Example: - * - * baseuri = cic:/foo/bar - * include_paths = ../baz ../../pippo - * - * spaces at the end/begin of the line and around '=' are ignored, - * multiple spaces in the middle of an item are shrinked to one. - *) -val load_root_file: string -> (string*string) list - -(* baseuri_of_script ?(inc:REG[matita.includes]) fname - * -> - * root, buri, fullpath, rootrelativepath - * sample: baseuri_of_script a.ma -> /home/pippo/devel/, cic:/matita/a, - * /home/pippo/devel/a.ma, a.ma *) -val baseuri_of_script: - include_paths:string list -> string -> string * string * string * string - -(* given a baseuri and a file name (relative to its root) - * returns a baseuri: - * mk_baseuri "cic:/matita" "nat/plus.ma" -> "cic:/matita/nat/plus" - *) -val mk_baseuri: string -> string -> string - -(* finds all the roots files in the specified dir, roots are - * text files, readable by the user named 'root' - *) -val find_roots_in_dir: string -> string list - -(* make implementation *) -type options = (string * string) list - -module type Format = - sig - type source_object - type target_object - val load_deps_file: string -> (source_object * source_object list) list - val string_of_source_object: source_object -> string - val string_of_target_object: target_object -> string - val build: options -> source_object -> bool - val root_and_target_of: - options -> source_object -> - (* root, relative source, writeable target, read only target *) - string option * source_object * target_object * target_object - val mtime_of_source_object: source_object -> float option - val mtime_of_target_object: target_object -> float option - val is_readonly_buri_of: options -> source_object -> bool - end - -module Make : - functor (F : Format) -> - sig - (* make [root dir] [targets], targets = [] means make all *) - val make : string -> F.source_object list -> bool - end - -(* deps are made with scripts names, for example lines like - * - * nat/plus.ma nat/nat.ma logic/equality.ma - * - * state that plus.ma needs nat and equality - *) -val load_deps_file: string -> (string * string list) list -val write_deps_file: string option -> (string * string list) list -> unit - -(* FG ***********************************************************************) - -(* true if the argunent starts with a uri scheme prefix *) -val is_uri: string -> bool - -(* Valid values: 0: no debug; 1: normal debug; > 1: extra debug *) -val debug: int ref - -val time_stamp: string -> unit diff --git a/matita/components/library/libraryClean.ml b/matita/components/library/libraryClean.ml deleted file mode 100644 index c3eb8919f..000000000 --- a/matita/components/library/libraryClean.ml +++ /dev/null @@ -1,281 +0,0 @@ -(* Copyright (C) 2005, 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://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -open Printf - -let debug = false -let debug_prerr = if debug then prerr_endline else ignore - -module HGT = Http_getter_types;; -module HG = Http_getter;; -module UM = UriManager;; - -let decompile = ref (fun ~baseuri -> assert false);; -let set_decompile_cb f = decompile := f;; - -let strip_xpointer s = Pcre.replace ~pat:"#.*$" s ;; - -let safe_buri_of_suri suri = - try - UM.buri_of_uri (UM.uri_of_string suri) - with - UM.IllFormedUri _ -> suri - -let one_step_depend cache_of_processed_baseuri suri dbtype dbd = - assert false (* MATITA 1.0 - let buri = safe_buri_of_suri suri in - if Hashtbl.mem cache_of_processed_baseuri buri then - [] - else - begin - Hashtbl.add cache_of_processed_baseuri buri true; - let query = - let buri = buri ^ "/" in - let buri = HSql.escape dbtype dbd buri in - let obj_tbl = MetadataTypes.obj_tbl () in - if HSql.isMysql dbtype dbd then - sprintf ("SELECT source, h_occurrence FROM %s WHERE " - ^^ "h_occurrence REGEXP '"^^ - "^%s\\([^/]+\\|[^/]+#xpointer.*\\)$"^^"'") - obj_tbl buri - else - begin - sprintf ("SELECT source, h_occurrence FROM %s WHERE " - ^^ "REGEXP(h_occurrence, '"^^ - "^%s\\([^/]+\\|[^/]+#xpointer.*\\)$"^^"')") - obj_tbl buri - (* implementation with vanilla ocaml-sqlite3 - HLog.debug "Warning SELECT without REGEXP"; - sprintf - ("SELECT source, h_occurrence FROM %s WHERE " ^^ - "h_occurrence LIKE '%s%%' " ^^ HSql.escape_string_for_like) - obj_tbl buri*) - end - in - try - let rc = HSql.exec dbtype dbd query in - let l = ref [] in - HSql.iter rc ( - fun row -> - match row.(0), row.(1) with - | Some uri, Some occ when - Filename.dirname (strip_xpointer occ) = buri -> - l := uri :: !l - | _ -> ()); - let l = List.sort Pervasives.compare !l in - HExtlib.list_uniq l - with - exn -> raise exn (* no errors should be accepted *) - end - *) - -let db_uris_of_baseuri buri = - [] (* MATITA 1.0 - let dbd = LibraryDb.instance () in - let dbtype = - if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User - in - let query = - let buri = buri ^ "/" in - let buri = HSql.escape dbtype dbd buri in - let obj_tbl = MetadataTypes.name_tbl () in - if HSql.isMysql dbtype dbd then - sprintf ("SELECT source FROM %s WHERE " - ^^ "source REGEXP '^%s[^/]*(#xpointer.*)?$'") obj_tbl buri - else - begin - sprintf ("SELECT source FROM %s WHERE " - ^^ "REGEXP(source, '^%s[^/]*\\(#xpointer.*\\)?$')") obj_tbl buri - end - in - try - let rc = HSql.exec dbtype dbd query in - let l = ref [] in - HSql.iter rc ( - fun row -> - match row.(0) with - | Some uri when Filename.dirname (strip_xpointer uri) = buri -> - l := uri :: !l - | _ -> ()); - let l = List.sort Pervasives.compare !l in - HExtlib.list_uniq l - with - exn -> raise exn (* no errors should be accepted *) - *) -;; - -let close_uri_list cache_of_processed_baseuri uri_to_remove = - let dbd = LibraryDb.instance () in - let dbtype = - if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User - in - (* to remove an uri you have to remove the whole script *) - let buri_to_remove = - HExtlib.list_uniq - (List.fast_sort Pervasives.compare - (List.map safe_buri_of_suri uri_to_remove)) - in - (* cleand the already visided baseuris *) - let buri_to_remove = - List.filter - (fun buri -> - if Hashtbl.mem cache_of_processed_baseuri buri then false - else true) - buri_to_remove - in - (* now calculate the list of objects that belong to these baseuris *) - let uri_to_remove = - try - List.fold_left - (fun acc buri -> - let inhabitants = HG.ls ~local:true (buri ^ "/") in - let inhabitants = List.filter - (function HGT.Ls_object _ -> true | _ -> false) - inhabitants - in - let inhabitants = List.map - (function - | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri - | _ -> assert false) - inhabitants - in - inhabitants @ acc) - [] buri_to_remove - with HGT.Invalid_URI u -> - HLog.error ("We were listing an invalid buri: " ^ u); - exit 1 - in - let uri_to_remove_from_db = - List.fold_left - (fun acc buri -> - let dbu = db_uris_of_baseuri buri in - dbu @ acc - ) [] buri_to_remove - in - let uri_to_remove = uri_to_remove @ uri_to_remove_from_db in - let uri_to_remove = - HExtlib.list_uniq (List.sort Pervasives.compare uri_to_remove) in - (* now we want the list of all uri that depend on them *) - let depend = - List.fold_left - (fun acc u -> one_step_depend cache_of_processed_baseuri u dbtype dbd @ acc) - [] uri_to_remove - in - let depend = - HExtlib.list_uniq (List.fast_sort Pervasives.compare depend) - in - uri_to_remove, depend -;; - -let rec close_db cache_of_processed_baseuri uris next = - match next with - | [] -> uris - | l -> - let uris, next = close_uri_list cache_of_processed_baseuri l in - close_db cache_of_processed_baseuri uris next @ uris -;; - -let cleaned_no = ref 0;; - - (** TODO repellent code ... *) -let moo_root_dir = lazy ( - let url = - List.assoc "cic:/matita/" - (List.map - (fun pair -> - match - Str.split (Str.regexp "[ \t\r\n]+") (HExtlib.trim_blanks pair) - with - | a::b::_ -> a, b - | _ -> assert false) - (Helm_registry.get_list Helm_registry.string "getter.prefix")) - in - String.sub url 7 (String.length url - 7)) -;; - -let clean_baseuris ?(verbose=true) buris = - prerr_endline "CLEAN_BASEURIS to be removed MATITA 1.0"; (* MATITA 1.0 - let cache_of_processed_baseuri = Hashtbl.create 1024 in - let dbd = LibraryDb.instance () in - let dbtype = - if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User - in - Hashtbl.clear cache_of_processed_baseuri; - let buris = List.map Http_getter_misc.strip_trailing_slash buris in - debug_prerr "clean_baseuris called on:"; - if debug then - List.iter debug_prerr buris; - let l = close_db cache_of_processed_baseuri [] buris in - let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in - let l = List.map UriManager.uri_of_string l in - debug_prerr "clean_baseuri will remove:"; - if debug then - List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; - List.iter - (fun baseuri -> - !decompile ~baseuri; - try - let obj_file = - LibraryMisc.obj_file_of_baseuri ~must_exist:false ~writable:true ~baseuri - in - HExtlib.safe_remove obj_file ; - HExtlib.safe_remove - (LibraryMisc.lexicon_file_of_baseuri - ~must_exist:false ~writable:true ~baseuri) ; - HExtlib.rmdir_descend (Filename.chop_extension obj_file) - with Http_getter_types.Key_not_found _ -> ()) - (HExtlib.list_uniq (List.fast_sort Pervasives.compare - (List.map (UriManager.buri_of_uri) l @ buris))); - List.iter - (let last_baseuri = ref "" in - fun uri -> - let buri = UriManager.buri_of_uri uri in - if buri <> !last_baseuri then - begin - if not (Helm_registry.get_bool "matita.verbose") then - (print_endline ("matitaclean " ^ buri ^ "/");flush stdout) - else - HLog.message ("Removing: " ^ buri ^ "/*"); - last_baseuri := buri - end; - LibrarySync.remove_obj uri - ) l; - if HSql.isMysql dbtype dbd then - begin - cleaned_no := !cleaned_no + List.length l; - if !cleaned_no > 30 && HSql.isMysql dbtype dbd then - begin - cleaned_no := 0; - List.iter - (function table -> - ignore (HSql.exec dbtype dbd ("OPTIMIZE TABLE " ^ table))) - [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl (); - MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl(); - MetadataTypes.count_tbl()] - end - end - *) diff --git a/matita/components/library/libraryClean.mli b/matita/components/library/libraryClean.mli deleted file mode 100644 index 89f3b7b1d..000000000 --- a/matita/components/library/libraryClean.mli +++ /dev/null @@ -1,29 +0,0 @@ -(* Copyright (C) 2004-2005, 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://helm.cs.unibo.it/ - *) - -val set_decompile_cb: (baseuri: string -> unit) -> unit - -val db_uris_of_baseuri : string -> string list -val clean_baseuris : ?verbose:bool -> string list -> unit diff --git a/matita/components/library/libraryDb.ml b/matita/components/library/libraryDb.ml deleted file mode 100644 index 34ad77077..000000000 --- a/matita/components/library/libraryDb.ml +++ /dev/null @@ -1,215 +0,0 @@ -(* Copyright (C) 2004-2005, 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://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -let dbtype_of_string dbtype = - if dbtype = "library" then HSql.Library - else if dbtype = "user" then HSql.User - else if dbtype = "legacy" then HSql.Legacy - else raise (HSql.Error "HSql: wrong config file format") - -let parse_dbd_conf _ = - let metadata = Helm_registry.get_list Helm_registry.string "db.metadata" in - List.map - (fun s -> - match Pcre.split ~pat:"\\s+" s with - | [path;db;user;pwd;dbtype] -> - let dbtype = dbtype_of_string dbtype in - let pwd = if pwd = "none" then None else Some pwd in - (* TODO parse port *) - path, None, db, user, pwd, dbtype - | _ -> raise (HSql.Error "HSql: Bad format in config file")) - metadata -;; - -let parse_dbd_conf _ = - HSql.mk_dbspec (parse_dbd_conf ()) -;; - -let instance = - let dbd = lazy ( - let dbconf = parse_dbd_conf () in - HSql.quick_connect dbconf) - in - fun () -> Lazy.force dbd -;; - -let xpointer_RE = Pcre.regexp "#.*$" -let file_scheme_RE = Pcre.regexp "^file://" - -let clean_owner_environment () = assert false (* MATITA 1.0 - let dbd = instance () in - let obj_tbl = MetadataTypes.obj_tbl () in - let sort_tbl = MetadataTypes.sort_tbl () in - let rel_tbl = MetadataTypes.rel_tbl () in - let name_tbl = MetadataTypes.name_tbl () in - let count_tbl = MetadataTypes.count_tbl () in - let tbls = [ - (obj_tbl,`RefObj) ; (sort_tbl,`RefSort) ; (rel_tbl,`RefRel) ; - (name_tbl,`ObjectName) ; (count_tbl,`Count) ] - in - let dbtype = - if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User - in - let statements = - (SqlStatements.drop_tables tbls) @ - (SqlStatements.drop_indexes tbls dbtype dbd) - in - let owned_uris = - try - MetadataDb.clean ~dbd - with (HSql.Error _) as exn -> - match HSql.errno dbtype dbd with - | HSql.No_such_table -> [] - | _ -> raise exn - in - List.iter - (fun uri -> - let uri = Pcre.replace ~rex:xpointer_RE ~templ:"" uri in - List.iter - (fun suffix -> - try - HExtlib.safe_remove - (Http_getter.resolve ~local:true ~writable:true (uri ^ suffix)) - with Http_getter_types.Key_not_found _ -> ()) - [""; ".body"; ".types"]) - owned_uris; - List.iter (fun statement -> - try - ignore (HSql.exec dbtype dbd statement) - with (HSql.Error _) as exn -> - match HSql.errno dbtype dbd with - | HSql.No_such_table - | HSql.Bad_table_error - | HSql.No_such_index -> () - | _ -> raise exn - ) statements; - *) -;; - -let create_owner_environment () = () (* MATITA 1.0 - let dbd = instance () in - let obj_tbl = MetadataTypes.obj_tbl () in - let sort_tbl = MetadataTypes.sort_tbl () in - let rel_tbl = MetadataTypes.rel_tbl () in - let name_tbl = MetadataTypes.name_tbl () in - let count_tbl = MetadataTypes.count_tbl () in - let l_obj_tbl = MetadataTypes.library_obj_tbl in - let l_sort_tbl = MetadataTypes.library_sort_tbl in - let l_rel_tbl = MetadataTypes.library_rel_tbl in - let l_name_tbl = MetadataTypes.library_name_tbl in - let l_count_tbl = MetadataTypes.library_count_tbl in - let tbls = [ - (obj_tbl,`RefObj) ; (sort_tbl,`RefSort) ; (rel_tbl,`RefRel) ; - (name_tbl,`ObjectName) ; (count_tbl,`Count) ] - in - let system_tbls = [ - (l_obj_tbl,`RefObj) ; (l_sort_tbl,`RefSort) ; (l_rel_tbl,`RefRel) ; - (l_name_tbl,`ObjectName) ; (l_count_tbl,`Count) ] - in - let tag tag l = List.map (fun x -> tag, x) l in - let statements = - (tag HSql.Library (SqlStatements.create_tables system_tbls)) @ - (tag HSql.User (SqlStatements.create_tables tbls)) @ - (tag HSql.Library (SqlStatements.create_indexes system_tbls)) @ - (tag HSql.User (SqlStatements.create_indexes tbls)) - in - List.iter - (fun (dbtype, statement) -> - try - ignore (HSql.exec dbtype dbd statement) - with - (HSql.Error _) as exc -> - let status = HSql.errno dbtype dbd in - match status with - | HSql.Table_exists_error -> () - | HSql.Dup_keyname -> () - | HSql.GENERIC_ERROR _ -> - prerr_endline statement; - raise exc - | _ -> ()) - statements - *) -;; - -(* removes uri from the ownerized tables, and returns the list of other objects - * (theyr uris) that ref the one removed. - * AFAIK there is no need to return it, since the MatitaTypes.staus should - * contain all defined objects. but to double check we do not garbage the - * metadata... - *) -let remove_uri uri = assert false (* MATITA 1.0 - let obj_tbl = MetadataTypes.obj_tbl () in - let sort_tbl = MetadataTypes.sort_tbl () in - let rel_tbl = MetadataTypes.rel_tbl () in - let name_tbl = MetadataTypes.name_tbl () in - (*let conclno_tbl = MetadataTypes.conclno_tbl () in - let conclno_hyp_tbl = MetadataTypes.fullno_tbl () in*) - let count_tbl = MetadataTypes.count_tbl () in - - let dbd = instance () in - let suri = UriManager.string_of_uri uri in - let dbtype = - if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User - in - let query table suri = - if HSql.isMysql dbtype dbd then - Printf.sprintf "DELETE QUICK LOW_PRIORITY FROM %s WHERE source='%s'" table - (HSql.escape dbtype dbd suri) - else - Printf.sprintf "DELETE FROM %s WHERE source='%s'" table - (HSql.escape dbtype dbd suri) - in - List.iter (fun t -> - try - ignore (HSql.exec dbtype dbd (query t suri)) - with - exn -> raise exn (* no errors should be accepted *) - ) - [obj_tbl;sort_tbl;rel_tbl;name_tbl;(*conclno_tbl;conclno_hyp_tbl*)count_tbl]; - *) -;; - -let xpointers_of_ind uri = assert false (* MATITA 1.0 - let dbd = instance () in - let name_tbl = MetadataTypes.name_tbl () in - let dbtype = - if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User - in - let escape s = - Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" - (HSql.escape dbtype dbd s) - in - let query = Printf.sprintf - ("SELECT source FROM %s WHERE source LIKE '%s#xpointer%%' " - ^^ HSql.escape_string_for_like dbtype dbd) - name_tbl (escape (UriManager.string_of_uri uri)) - in - let rc = HSql.exec dbtype dbd query in - let l = ref [] in - HSql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l); - List.map UriManager.uri_of_string !l -*) diff --git a/matita/components/library/libraryDb.mli b/matita/components/library/libraryDb.mli deleted file mode 100644 index e608a9c24..000000000 --- a/matita/components/library/libraryDb.mli +++ /dev/null @@ -1,35 +0,0 @@ -(* Copyright (C) 2004-2005, 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://helm.cs.unibo.it/ - *) - -val dbtype_of_string: string -> HSql.dbtype - -val instance: unit -> HSql.dbd -val parse_dbd_conf: unit -> HSql.dbspec - -val create_owner_environment: unit -> unit -val clean_owner_environment: unit -> unit - -val remove_uri: UriManager.uri -> unit -val xpointers_of_ind: UriManager.uri -> UriManager.uri list diff --git a/matita/components/library/libraryMisc.ml b/matita/components/library/libraryMisc.ml deleted file mode 100644 index 7c82e27c4..000000000 --- a/matita/components/library/libraryMisc.ml +++ /dev/null @@ -1,38 +0,0 @@ -(* Copyright (C) 2004-2005, 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://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -let resolve ~must_exist ~writable ~local baseuri = - if must_exist then - Http_getter.resolve ~local ~writable baseuri - else - Http_getter.filename ~local ~writable baseuri - -let obj_file_of_baseuri ~must_exist ~writable ~baseuri = - resolve ~must_exist ~writable ~local:true baseuri ^ ".moo" -let lexicon_file_of_baseuri ~must_exist ~writable ~baseuri = - resolve ~must_exist ~writable ~local:true baseuri ^ ".lexicon" - diff --git a/matita/components/library/libraryMisc.mli b/matita/components/library/libraryMisc.mli deleted file mode 100644 index 2c6bfd193..000000000 --- a/matita/components/library/libraryMisc.mli +++ /dev/null @@ -1,30 +0,0 @@ -(* Copyright (C) 2004-2005, 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://helm.cs.unibo.it/ - *) - -(* only for local uris *) -val obj_file_of_baseuri: - must_exist:bool -> writable:bool -> baseuri:string -> string -val lexicon_file_of_baseuri: - must_exist:bool -> writable:bool -> baseuri:string -> string diff --git a/matita/components/library/librarySync.ml b/matita/components/library/librarySync.ml deleted file mode 100644 index 0eeef7d78..000000000 --- a/matita/components/library/librarySync.ml +++ /dev/null @@ -1,387 +0,0 @@ -(* Copyright (C) 2004-2005, 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://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -let object_declaration_hook = ref [] -let add_object_declaration_hook f = - object_declaration_hook := f :: !object_declaration_hook - -exception AlreadyDefined of UriManager.uri - -type coercion_decl = - UriManager.uri -> int (* arity *) -> - int (* saturations *) -> string (* baseuri *) -> - UriManager.uri list (* lemmas (new objs) *) - - -let stack = ref [];; - -let push () = - stack := CoercDb.dump () :: !stack; - CoercDb.restore CoercDb.empty_coerc_db; -;; - -let pop () = - match !stack with - | [] -> raise (Failure "Unable to POP from librarySync.ml") - | db :: tl -> - stack := tl; - CoercDb.restore db; -;; - -let uris_of_obj uri = - let innertypesuri = UriManager.innertypesuri_of_uri uri in - let bodyuri = UriManager.bodyuri_of_uri uri in - let univgraphuri = UriManager.univgraphuri_of_uri uri in - innertypesuri,bodyuri,univgraphuri - -let paths_and_uris_of_obj uri = - let resolved = Http_getter.filename' ~local:true ~writable:true uri in - let basepath = Filename.dirname resolved in - let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in - let innertypesfilename=(UriManager.nameext_of_uri innertypesuri)^".xml.gz"in - let innertypespath = basepath ^ "/" ^ innertypesfilename in - let xmlfilename = (UriManager.nameext_of_uri uri) ^ ".xml.gz" in - let xmlpath = basepath ^ "/" ^ xmlfilename in - let xmlbodyfilename = (UriManager.nameext_of_uri uri) ^ ".body.xml.gz" in - let xmlbodypath = basepath ^ "/" ^ xmlbodyfilename in - let xmlunivgraphfilename=(UriManager.nameext_of_uri univgraphuri)^".xml.gz"in - let xmlunivgraphpath = basepath ^ "/" ^ xmlunivgraphfilename in - xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, - xmlunivgraphpath, univgraphuri - -let save_object_to_disk uri obj ugraph univlist = - assert false (* - let write f x = - if not (Helm_registry.get_opt_default - Helm_registry.bool "matita.nodisk" ~default:false) - then - f x - in - let ensure_path_exists path = - let dir = Filename.dirname path in - HExtlib.mkdir dir - in - (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *) - let annobj, innertypes, ids_to_inner_sorts, generate_attributes = - if Helm_registry.get_bool "matita.system" && - not (Helm_registry.get_bool "matita.noinnertypes") - then - let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ = - Cic2acic.acic_object_of_cic_object obj - in - let innertypesxml = - Cic2Xml.print_inner_types - uri ~ids_to_inner_sorts ~ids_to_inner_types ~ask_dtd_to_the_getter:false - in - annobj, Some innertypesxml, Some ids_to_inner_sorts, false - else - let annobj = Cic2acic.plain_acic_object_of_cic_object obj in - annobj, None, None, true - in - (* prepare XML *) - let xml, bodyxml = - Cic2Xml.print_object - uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter:false - ~generate_attributes annobj - in - let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, - xmlunivgraphpath, univgraphuri = - paths_and_uris_of_obj uri - in - write (List.iter HExtlib.mkdir) (List.map Filename.dirname [xmlpath]); - (* now write to disk *) - write ensure_path_exists xmlpath; - write (Xml.pp ~gzip:true xml) (Some xmlpath); - write (CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph) univlist; - (* we return a list of uri,path we registered/created *) - (uri,xmlpath) :: - (univgraphuri,xmlunivgraphpath) :: - (* now the optional inner types, both write and register *) - (match innertypes with - | None -> [] - | Some innertypesxml -> - write ensure_path_exists innertypespath; - write (Xml.pp ~gzip:true innertypesxml) (Some innertypespath); - [innertypesuri, innertypespath] - ) @ - (* now the optional body, both write and register *) - (match bodyxml,bodyuri with - None,_ -> [] - | Some bodyxml,Some bodyuri-> - write ensure_path_exists xmlbodypath; - write (Xml.pp ~gzip:true bodyxml) (Some xmlbodypath); - [bodyuri, xmlbodypath] - | _-> assert false) - *) - - -let typecheck_obj = - let profiler = HExtlib.profile "add_obj.typecheck_obj" in - fun uri obj -> - assert false (* MATITA 1.0 - profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj - *) - -let index_obj = - let profiler = HExtlib.profile "add_obj.index_obj" in - fun ~dbd ~uri -> - assert false (* MATITA 1.0 - profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri - *) - -let remove_obj uri = - assert false (* MATITA 1.0 - let derived_uris_of_uri uri = - let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in - innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u]) - in - let uris_to_remove = - if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else [uri] - in - let files_to_remove = uri :: derived_uris_of_uri uri in - List.iter - (fun uri -> - (try - let file = Http_getter.resolve' ~local:true ~writable:true uri in - HExtlib.safe_remove file; - HExtlib.rmdir_descend (Filename.dirname file) - with Http_getter_types.Key_not_found _ -> ()); - ) files_to_remove ; - List.iter (fun uri -> ignore (LibraryDb.remove_uri uri)) uris_to_remove ; - CicEnvironment.remove_obj uri -;; -*) - -let rec add_obj uri obj ~pack_coercion_obj = - assert false (* MATITA 1.0 - let obj = - if CoercDb.is_a_coercion (Cic.Const (uri, [])) = None - then pack_coercion_obj obj - else obj - in - let dbd = LibraryDb.instance () in - if CicEnvironment.in_library uri then raise (AlreadyDefined uri); - begin (* ATOMIC *) - typecheck_obj uri obj; (* 1 *) - let obj, ugraph, univlist = - try CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri - with CicEnvironment.Object_not_found _ -> assert false - in - try - index_obj ~dbd ~uri; (* 2 must be in the env *) - try - (*3*) - let new_stuff = save_object_to_disk uri obj ugraph univlist in - try - HLog.message - (Printf.sprintf "%s defined" (UriManager.string_of_uri uri)) - with exc -> - List.iter HExtlib.safe_remove (List.map snd new_stuff); (* -3 *) - raise exc - with exc -> - ignore(LibraryDb.remove_uri uri); (* -2 *) - raise exc - with exc -> - CicEnvironment.remove_obj uri; (* -1 *) - raise exc - end; - let added = ref [] in - let add_obj_with_parachute u o = - added := u :: !added; - add_obj u o ~pack_coercion_obj in - let old_db = CoercDb.dump () in - try - List.fold_left - (fun lemmas f -> - f ~add_obj:add_obj_with_parachute - ~add_coercion:(add_coercion ~add_composites:true ~pack_coercion_obj) - uri obj @ lemmas) - [] !object_declaration_hook - with exn -> - List.iter remove_obj !added; - remove_obj uri; - CoercDb.restore old_db; - raise exn - (* /ATOMIC *) - *) - -and - add_coercion ~add_composites ~pack_coercion_obj uri arity saturations baseuri -= - assert false (* MATITA 1.0 - let coer_ty,_ = - let coer = CicUtil.term_of_uri uri in - CicTypeChecker.type_of_aux' [] [] coer CicUniv.oblivion_ugraph - in - (* we have to get the source and the tgt type uri - * in Coq syntax we have already their names, but - * since we don't support Funclass and similar I think - * all the coercion should be of the form - * (A:?)(B:?)T1->T2 - * So we should be able to extract them from the coercion type - * - * Currently only (_:T1)T2 is supported. - * should we saturate it with metas in case we insert it? - * - *) - let spine2list ty = - let rec aux = function - | Cic.Prod( _, src, tgt) -> src::aux tgt - | t -> [t] - in - aux ty - in - let src_carr, tgt_carr, no_args = - let get_classes arity saturations l = - (* this is the ackerman's function revisited *) - let rec aux = function - 0,0,None,tgt::src::_ -> src,Some (`Class tgt) - | 0,0,target,src::_ -> src,target - | 0,saturations,None,tgt::tl -> aux (0,saturations,Some (`Class tgt),tl) - | 0,saturations,target,_::tl -> aux (0,saturations - 1,target,tl) - | arity,saturations,None,_::tl -> - aux (arity, saturations, Some `Funclass, tl) - | arity,saturations,target,_::tl -> - aux (arity - 1, saturations, target, tl) - | _ -> assert false - in - aux (arity,saturations,None,List.rev l) - in - let types = spine2list coer_ty in - let src,tgt = get_classes arity saturations types in - CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src) 0, - (match tgt with - | None -> assert false - | Some `Funclass -> CoercDb.coerc_carr_of_term (Cic.Implicit None) arity - | Some (`Class tgt) -> - CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) 0), - List.length types - 1 - in - let already_in_obj src_carr tgt_carr uri obj = - List.exists - (fun (s,t,ul) -> - if not (CoercDb.eq_carr s src_carr && - CoercDb.eq_carr t tgt_carr) - then false - else - List.exists - (fun u,_,_ -> - let bo, ty = - match obj with - | Cic.Constant (_, Some bo, ty, _, _) -> bo, ty - | _ -> - (* this is not a composite coercion, thus the uri is valid *) - let bo = CicUtil.term_of_uri uri in - bo, - fst (CicTypeChecker.type_of_aux' [] [] bo - CicUniv.oblivion_ugraph) - in - let are_body_convertible = - fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo - CicUniv.oblivion_ugraph) - in - if not are_body_convertible then - (HLog.warn - ("Coercions " ^ - UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri - uri^" are not convertible, but are between the same nodes.\n"^ - "From now on unification can fail randomly."); - false) - else - match t, tgt_carr with - | CoercDb.Sort (Cic.Type i), CoercDb.Sort (Cic.Type j) - | CoercDb.Sort (Cic.CProp i), CoercDb.Sort (Cic.CProp j) - when not (CicUniv.eq i j) -> - (HLog.warn - ("Coercion " ^ UriManager.string_of_uri uri ^ " has the same " ^ - "body of " ^ UriManager.string_of_uri u ^ " but lives in a " ^ - "different universe : " ^ - CicUniv.string_of_universe j ^ " <> " ^ - CicUniv.string_of_universe i); false) - | CoercDb.Sort Cic.Prop , CoercDb.Sort Cic.Prop - | CoercDb.Sort (Cic.Type _) , CoercDb.Sort (Cic.Type _) - | CoercDb.Sort (Cic.CProp _), CoercDb.Sort (Cic.CProp _) -> - (HLog.warn - ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^ - "it is a duplicate of " ^ UriManager.string_of_uri u); - true) - | CoercDb.Sort s1, CoercDb.Sort s2 -> - (HLog.warn - ("Coercion " ^ UriManager.string_of_uri uri ^ " has the same " ^ - "body of " ^ UriManager.string_of_uri u ^ " but lives in a " ^ - "different universe : " ^ - CicPp.ppterm (Cic.Sort s1) ^ " <> " ^ - CicPp.ppterm (Cic.Sort s2)); false) - | _ -> - let ty', _ = - CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri u) - CicUniv.oblivion_ugraph - in - if CicUtil.alpha_equivalence ty ty' then - (HLog.warn - ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^ - "it is a duplicate of " ^ UriManager.string_of_uri u); - true) - else false - - ) - ul) - (CoercDb.to_list (CoercDb.dump ())) - in - let cpos = no_args - arity - saturations - 1 in - if not add_composites then - (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos); []) - else - let _ = - if already_in_obj src_carr tgt_carr uri - (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri)) then - raise (AlreadyDefined uri); - in - let new_coercions = - CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations - baseuri - in - let new_coercions = - List.filter (fun (s,t,u,_,obj,_,_) -> not(already_in_obj s t u obj)) - new_coercions - in - (* update the DB *) - let lemmas = - List.fold_left - (fun acc (src,tgt,uri,saturations,obj,arity,cpos) -> - CoercDb.add_coercion (src,tgt,uri,saturations,cpos); - let acc = add_obj uri obj pack_coercion_obj @ uri::acc in - acc) - [] new_coercions - in - CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos); -(* CoercDb.prefer uri; *) - lemmas - *) -;; - - diff --git a/matita/components/library/librarySync.mli b/matita/components/library/librarySync.mli deleted file mode 100644 index bfab37330..000000000 --- a/matita/components/library/librarySync.mli +++ /dev/null @@ -1,59 +0,0 @@ -(* Copyright (C) 2004-2005, 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://helm.cs.unibo.it/ - *) - -exception AlreadyDefined of UriManager.uri - -type coercion_decl = - UriManager.uri -> int (* arity *) -> - int (* saturations *) -> string (* baseuri *) -> - UriManager.uri list (* lemmas (new objs) *) - -(* the add_single_obj fun passed to the callback can raise AlreadyDefined *) -val add_object_declaration_hook : - (add_obj:(UriManager.uri -> Cic.obj -> UriManager.uri list) -> - add_coercion:coercion_decl -> - UriManager.uri -> Cic.obj -> UriManager.uri list) -> unit - -(* adds an object to the library together with all auxiliary lemmas on it *) -(* (e.g. elimination principles, projections, etc.) *) -(* it returns the list of the uris of the auxiliary lemmas generated *) -val add_obj: - UriManager.uri -> Cic.obj -> pack_coercion_obj:(Cic.obj -> Cic.obj) -> - UriManager.uri list - -(* removes an object (does not remove its associated lemmas) *) -val remove_obj: UriManager.uri -> unit - -(* Informs the library that [uri] is a coercion. *) -(* This can generate some composite coercions that, if [add_composites] *) -(* is true are added to the library. *) -(* The list of added objects is returned. *) -val add_coercion: - add_composites:bool -> pack_coercion_obj:(Cic.obj -> Cic.obj) -> coercion_decl - -(* these just push/pop the coercions database, since the library is not - * pushable/poppable *) -val push: unit -> unit -val pop: unit -> unit diff --git a/matita/components/ng_refiner/nCicCoercion.ml b/matita/components/ng_refiner/nCicCoercion.ml index 04fddee83..73da9579f 100644 --- a/matita/components/ng_refiner/nCicCoercion.ml +++ b/matita/components/ng_refiner/nCicCoercion.ml @@ -64,44 +64,6 @@ let index_coercion status name c src tgt arity arg = status#set_coerc_db (db_src, db_tgt) ;; -let index_old_db odb (status : #status) = - List.fold_left - (fun status (_,tgt,clist) -> - List.fold_left - (fun status (uri,_,arg) -> - try - let c=fst (!convert_term uri (CicUtil.term_of_uri uri)) in - let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in - let src, tgt = - let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in - let scty, metasenv,_ = - NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1) - in - match scty with - | NCic.Prod (_, src, tgt) -> - let tgt = - NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt - in -(* - debug (lazy (Printf.sprintf "indicizzo %s (%d)) : %s ===> %s" - (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] scty) (arity+1) - (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] src) - (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] tgt)); -*) - src, tgt - | t -> - debug (lazy ( - NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t)); - assert false - in - index_coercion status "foo" c src tgt arity arg - with - | NCicEnvironment.BadDependency _ - | NCicTypeChecker.TypeCheckerFailure _ -> status) - status clist) - status (CoercDb.to_list odb) -;; - let look_for_coercion status metasenv subst context infty expty = let db_src,db_tgt = status#coerc_db in match diff --git a/matita/components/ng_refiner/nCicCoercion.mli b/matita/components/ng_refiner/nCicCoercion.mli index ff6b43997..1094753cf 100644 --- a/matita/components/ng_refiner/nCicCoercion.mli +++ b/matita/components/ng_refiner/nCicCoercion.mli @@ -40,9 +40,6 @@ val index_coercion: #status as 'status -> string -> NCic.term -> NCic.term -> NCic.term -> int -> int -> 'status - (* gets the old imperative coercion DB (list format) *) -val index_old_db: CoercDb.coerc_db -> (#status as 'status) -> 'status - val look_for_coercion: #status -> NCic.metasenv -> NCic.substitution -> NCic.context -> diff --git a/matita/matita/matitaExcPp.ml b/matita/matita/matitaExcPp.ml index fe013421d..99e6ec944 100644 --- a/matita/matita/matitaExcPp.ml +++ b/matita/matita/matitaExcPp.ml @@ -157,8 +157,6 @@ let rec to_string = None, "NCicUnification failure: " ^ Lazy.force msg | NCicUnification.Uncertain msg -> None, "NCicUnification uncertain: " ^ Lazy.force msg - | LibrarySync.AlreadyDefined s -> - None, "Already defined: " ^ UriManager.string_of_uri s | DisambiguateChoices.Choice_not_found msg -> None, ("Disambiguation choice not found: " ^ Lazy.force msg) | MatitaEngine.EnrichedWithStatus (exn,_) -> diff --git a/matita/matita/matitaInit.ml b/matita/matita/matitaInit.ml index c40f81dff..a78fb0972 100644 --- a/matita/matita/matitaInit.ml +++ b/matita/matita/matitaInit.ml @@ -97,7 +97,6 @@ let initialize_db init_status = wants [ ConfigurationFile; CmdLine ] init_status; if not (already_configured [ Db ] init_status) then begin - LibraryDb.create_owner_environment (); Db::init_status end else @@ -284,7 +283,3 @@ let parse_cmdline_and_configuration_file () = let initialize_environment () = status := initialize_environment !status - -let _ = - CicFix.init () -;; diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 1de645619..ae56969d3 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -193,7 +193,6 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac = (* no idea why ocaml wants this *) let parsed_text_length = String.length parsed_text in - let dbd = LibraryDb.instance () in match mac with (* REAL macro *) | TA.Hint (loc, rewrite) -> (* MATITA 1.0 *) assert false diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml index d9ce848d5..706981937 100644 --- a/matita/matita/matitacLib.ml +++ b/matita/matita/matitacLib.ml @@ -185,8 +185,7 @@ let compile atstart options fname = ~must_exist:false ~baseuri ~writable:true in (* cleanup of previously compiled objects *) - if (not (Http_getter_storage.is_empty ~local:true baseuri) || - LibraryClean.db_uris_of_baseuri baseuri <> []) + if (not (Http_getter_storage.is_empty ~local:true baseuri)) then begin HLog.message ("baseuri " ^ baseuri ^ " is not empty"); HLog.message ("cleaning baseuri " ^ baseuri); diff --git a/matita/matita/matitaclean.ml b/matita/matita/matitaclean.ml index a3183c161..f0f45b126 100644 --- a/matita/matita/matitaclean.ml +++ b/matita/matita/matitaclean.ml @@ -58,7 +58,6 @@ let ask_confirmation _ = let clean_all () = if Helm_registry.get_bool "matita.system" then ask_confirmation (); - LibraryDb.clean_owner_environment (); let prefixes = HExtlib.filter_map (fun s -> -- 2.39.2