+++ /dev/null
-requires="helm-registry sqlite3 mysql helm-extlib"
-version="0.0.1"
-archive(byte)="hmysql.cma"
-archive(native)="hmysql.cmxa"
-requires="helm-cic helm-getter helm-hmysql"
+requires="helm-cic helm-getter"
version="0.0.1"
archive(byte)="library.cma"
archive(native)="library.cmxa"
-requires="helm-library"
+requires="helm-cic"
version="0.0.1"
archive(byte)="ng_kernel.cma"
archive(native)="ng_kernel.cmxa"
xml \
hgdome \
registry \
- hmysql \
syntax_extensions \
thread \
urimanager \
#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@%)
+++ /dev/null
-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
+++ /dev/null
-<?xml version="1.0" encoding="utf-8"?>
-<helm_registry>
- <section name="db">
- <key name="metadata">mysql://mowgli.cs.unibo.it mowgli helm none legacy</key>
- <key name="type">legacy</key>
- </section>
-</helm_registry>
+++ /dev/null
-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
module GP = GrafiteAstPp
module G = GrafiteAst
module H = HExtlib
-module HG = Http_getter
let floc = H.dummy_floc
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
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
| _ -> [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
;;
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 ()
;;
* 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
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;
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]
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-(* 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);;
+++ /dev/null
-(* 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]
-;;
+++ /dev/null
-(* 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
-
+++ /dev/null
-(* 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);;
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-(* 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
-;;
+++ /dev/null
-(* 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
-
+++ /dev/null
-(* 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;;
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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;
-;;
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-
-type 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
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
- *)
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
-*)
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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"
-
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
- *)
-;;
-
-
+++ /dev/null
-(* 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
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
#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 ->
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,_) ->
wants [ ConfigurationFile; CmdLine ] init_status;
if not (already_configured [ Db ] init_status) then
begin
- LibraryDb.create_owner_environment ();
Db::init_status
end
else
let initialize_environment () =
status := initialize_environment !status
-
-let _ =
- CicFix.init ()
-;;
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
~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);
let clean_all () =
if Helm_registry.get_bool "matita.system" then
ask_confirmation ();
- LibraryDb.clean_owner_environment ();
let prefixes =
HExtlib.filter_map
(fun s ->
projects / helm.git / commitdiff