From: Andrea Asperti Date: Fri, 8 Oct 2010 10:51:07 +0000 (+0000) Subject: SVN bug: library lost, copying it again from previous version (???) X-Git-Tag: make_still_working~2790 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=08ae8b17903359fa9086a465096fd568c562d1d3;p=helm.git SVN bug: library lost, copying it again from previous version (???) --- diff --git a/matita/components/library/.depend b/matita/components/library/.depend new file mode 100644 index 000000000..cfa1295ed --- /dev/null +++ b/matita/components/library/.depend @@ -0,0 +1,32 @@ +librarian.cmi: +libraryMisc.cmi: +libraryDb.cmi: +coercDb.cmi: +cicCoercion.cmi: coercDb.cmi +librarySync.cmi: +cicElim.cmi: +cicRecord.cmi: +cicFix.cmi: +libraryClean.cmi: +librarian.cmo: librarian.cmi +librarian.cmx: librarian.cmi +libraryMisc.cmo: libraryMisc.cmi +libraryMisc.cmx: libraryMisc.cmi +libraryDb.cmo: libraryDb.cmi +libraryDb.cmx: libraryDb.cmi +coercDb.cmo: coercDb.cmi +coercDb.cmx: coercDb.cmi +cicCoercion.cmo: coercDb.cmi cicCoercion.cmi +cicCoercion.cmx: coercDb.cmx cicCoercion.cmi +librarySync.cmo: libraryDb.cmi coercDb.cmi cicCoercion.cmi librarySync.cmi +librarySync.cmx: libraryDb.cmx coercDb.cmx cicCoercion.cmx librarySync.cmi +cicElim.cmo: librarySync.cmi cicElim.cmi +cicElim.cmx: librarySync.cmx cicElim.cmi +cicRecord.cmo: librarySync.cmi cicRecord.cmi +cicRecord.cmx: librarySync.cmx cicRecord.cmi +cicFix.cmo: librarySync.cmi cicFix.cmi +cicFix.cmx: librarySync.cmx cicFix.cmi +libraryClean.cmo: librarySync.cmi libraryMisc.cmi libraryDb.cmi \ + libraryClean.cmi +libraryClean.cmx: librarySync.cmx libraryMisc.cmx libraryDb.cmx \ + libraryClean.cmi diff --git a/matita/components/library/.depend.opt b/matita/components/library/.depend.opt new file mode 100644 index 000000000..cfa1295ed --- /dev/null +++ b/matita/components/library/.depend.opt @@ -0,0 +1,32 @@ +librarian.cmi: +libraryMisc.cmi: +libraryDb.cmi: +coercDb.cmi: +cicCoercion.cmi: coercDb.cmi +librarySync.cmi: +cicElim.cmi: +cicRecord.cmi: +cicFix.cmi: +libraryClean.cmi: +librarian.cmo: librarian.cmi +librarian.cmx: librarian.cmi +libraryMisc.cmo: libraryMisc.cmi +libraryMisc.cmx: libraryMisc.cmi +libraryDb.cmo: libraryDb.cmi +libraryDb.cmx: libraryDb.cmi +coercDb.cmo: coercDb.cmi +coercDb.cmx: coercDb.cmi +cicCoercion.cmo: coercDb.cmi cicCoercion.cmi +cicCoercion.cmx: coercDb.cmx cicCoercion.cmi +librarySync.cmo: libraryDb.cmi coercDb.cmi cicCoercion.cmi librarySync.cmi +librarySync.cmx: libraryDb.cmx coercDb.cmx cicCoercion.cmx librarySync.cmi +cicElim.cmo: librarySync.cmi cicElim.cmi +cicElim.cmx: librarySync.cmx cicElim.cmi +cicRecord.cmo: librarySync.cmi cicRecord.cmi +cicRecord.cmx: librarySync.cmx cicRecord.cmi +cicFix.cmo: librarySync.cmi cicFix.cmi +cicFix.cmx: librarySync.cmx cicFix.cmi +libraryClean.cmo: librarySync.cmi libraryMisc.cmi libraryDb.cmi \ + libraryClean.cmi +libraryClean.cmx: librarySync.cmx libraryMisc.cmx libraryDb.cmx \ + libraryClean.cmi diff --git a/matita/components/library/Makefile b/matita/components/library/Makefile new file mode 100644 index 000000000..5b9dc226f --- /dev/null +++ b/matita/components/library/Makefile @@ -0,0 +1,20 @@ +PACKAGE = library +PREDICATES = + +INTERFACE_FILES = \ + librarian.mli \ + libraryMisc.mli \ + libraryDb.mli \ + coercDb.mli \ + cicCoercion.mli \ + librarySync.mli \ + cicElim.mli \ + cicRecord.mli \ + cicFix.mli \ + libraryClean.mli \ + $(NULL) +IMPLEMENTATION_FILES = \ + $(INTERFACE_FILES:%.mli=%.ml) + +include ../../Makefile.defs +include ../Makefile.common diff --git a/matita/components/library/cicCoercion.ml b/matita/components/library/cicCoercion.ml new file mode 100644 index 000000000..b45599ceb --- /dev/null +++ b/matita/components/library/cicCoercion.ml @@ -0,0 +1,40 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* $Id$ *) + +let close_coercion_graph_ref = ref + (fun _ _ _ _ _ -> [] : + CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> + string (* baseuri *) -> + (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj * + int * int) list) +;; + +let set_close_coercion_graph f = close_coercion_graph_ref := f;; + +let close_coercion_graph c1 c2 u sat s = + !close_coercion_graph_ref c1 c2 u sat s +;; diff --git a/matita/components/library/cicCoercion.mli b/matita/components/library/cicCoercion.mli new file mode 100644 index 000000000..8356de8cd --- /dev/null +++ b/matita/components/library/cicCoercion.mli @@ -0,0 +1,40 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* This module implements the Coercions transitive closure *) + +val set_close_coercion_graph : + (CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> + string (* baseuri *) -> + (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * + int (* saturations *) * Cic.obj * int (* arity *) * int (* cpos *)) list) + -> unit + +val close_coercion_graph: + CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> + string (* baseuri *) -> + (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * + int (* saturations *) * Cic.obj * int (* arity *) * int (* cpos *)) list + diff --git a/matita/components/library/cicElim.ml b/matita/components/library/cicElim.ml new file mode 100644 index 000000000..9f3bda423 --- /dev/null +++ b/matita/components/library/cicElim.ml @@ -0,0 +1,461 @@ +(* Copyright (C) 2004, 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 + +exception Elim_failure of string Lazy.t +exception Can_t_eliminate + +let debug_print = fun _ -> () +(*let debug_print s = prerr_endline (Lazy.force s) *) + +let counter = ref ~-1 ;; + +let fresh_binder () = Cic.Name "matita_dummy" +(* + incr counter; + Cic.Name ("e" ^ string_of_int !counter) *) + + (** verifies if a given inductive type occurs in a term in target position *) +let rec recursive uri typeno = function + | Cic.Prod (_, _, target) -> recursive uri typeno target + | Cic.MutInd (uri', typeno', []) + | Cic.Appl (Cic.MutInd (uri', typeno', []) :: _) -> + UriManager.eq uri uri' && typeno = typeno' + | _ -> false + + (** given a list of constructor types, return true if at least one of them is + * recursive, false otherwise *) +let recursive_type uri typeno constructors = + let rec aux = function + | Cic.Prod (_, src, tgt) -> recursive uri typeno src || aux tgt + | _ -> false + in + List.exists (fun (_, ty) -> aux ty) constructors + +let unfold_appl = function + | Cic.Appl ((Cic.Appl args) :: tl) -> Cic.Appl (args @ tl) + | t -> t + +let rec split l n = + match (l,n) with + (l,0) -> ([], l) + | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2) + | (_,_) -> assert false + + (** build elimination principle part related to a single constructor + * @param paramsno number of Prod to ignore in this constructor (i.e. number of + * inductive parameters) + * @param dependent true if we are in the dependent case (i.e. sort <> Prop) *) +let rec delta (uri, typeno) dependent paramsno consno t p args = + match t with + | Cic.MutInd (uri', typeno', []) when + UriManager.eq uri uri' && typeno = typeno' -> + if dependent then + (match args with + | [] -> assert false + | [arg] -> unfold_appl (Cic.Appl [p; arg]) + | _ -> unfold_appl (Cic.Appl [p; unfold_appl (Cic.Appl args)])) + else + p + | Cic.Appl (Cic.MutInd (uri', typeno', []) :: tl) when + UriManager.eq uri uri' && typeno = typeno' -> + let (lparams, rparams) = split tl paramsno in + if dependent then + (match args with + | [] -> assert false + | [arg] -> unfold_appl (Cic.Appl (p :: rparams @ [arg])) + | _ -> + unfold_appl (Cic.Appl (p :: + rparams @ [unfold_appl (Cic.Appl args)]))) + else (* non dependent *) + (match rparams with + | [] -> p + | _ -> Cic.Appl (p :: rparams)) + | Cic.Prod (binder, src, tgt) -> + if recursive uri typeno src then + let args = List.map (CicSubstitution.lift 2) args in + let phi = + let src = CicSubstitution.lift 1 src in + delta (uri, typeno) dependent paramsno consno src + (CicSubstitution.lift 1 p) [Cic.Rel 1] + in + let tgt = CicSubstitution.lift 1 tgt in + Cic.Prod (fresh_binder (), src, + Cic.Prod (Cic.Anonymous, phi, + delta (uri, typeno) dependent paramsno consno tgt + (CicSubstitution.lift 2 p) (args @ [Cic.Rel 2]))) + else (* non recursive *) + let args = List.map (CicSubstitution.lift 1) args in + Cic.Prod (fresh_binder (), src, + delta (uri, typeno) dependent paramsno consno tgt + (CicSubstitution.lift 1 p) (args @ [Cic.Rel 1])) + | _ -> assert false + +let rec strip_left_params consno leftno = function + | t when leftno = 0 -> t (* no need to lift, the term is (hopefully) closed *) + | Cic.Prod (_, _, tgt) (* when leftno > 0 *) -> + (* after stripping the parameters we lift of consno. consno is 1 based so, + * the first constructor will be lifted by 1 (for P), the second by 2 (1 + * for P and 1 for the 1st constructor), and so on *) + if leftno = 1 then + CicSubstitution.lift consno tgt + else + strip_left_params consno (leftno - 1) tgt + | _ -> assert false + +let delta (ury, typeno) dependent paramsno consno t p args = + let t = strip_left_params consno paramsno t in + delta (ury, typeno) dependent paramsno consno t p args + +let rec add_params binder indno ty eliminator = + if indno = 0 then + eliminator + else + match ty with + | Cic.Prod (name, src, tgt) -> + let name = + match name with + Cic.Name _ -> name + | Cic.Anonymous -> fresh_binder () + in + binder name src (add_params binder (indno - 1) tgt eliminator) + | _ -> assert false + +let rec mk_rels consno = function + | 0 -> [] + | n -> Cic.Rel (n+consno) :: mk_rels consno (n-1) + +let rec strip_pi ctx t = + match CicReduction.whd ~delta:true ctx t with + | Cic.Prod (n, s, tgt) -> strip_pi (Some (n,Cic.Decl s) :: ctx) tgt + | t -> t + +let strip_pi t = strip_pi [] t + +let rec count_pi ctx t = + match CicReduction.whd ~delta:true ctx t with + | Cic.Prod (n, s, tgt) -> count_pi (Some (n,Cic.Decl s)::ctx) tgt + 1 + | t -> 0 + +let count_pi t = count_pi [] t + +let rec type_of_p sort dependent leftno indty = function + | Cic.Prod (n, src, tgt) when leftno = 0 -> + let n = + if dependent then + match n with + Cic.Name _ -> n + | Cic.Anonymous -> fresh_binder () + else + n + in + Cic.Prod (n, src, type_of_p sort dependent leftno indty tgt) + | Cic.Prod (_, _, tgt) -> type_of_p sort dependent (leftno - 1) indty tgt + | t -> + if dependent then + Cic.Prod (Cic.Anonymous, indty, Cic.Sort sort) + else + Cic.Sort sort + +let rec add_right_pi dependent strip liftno liftfrom rightno indty = function + | Cic.Prod (_, src, tgt) when strip = 0 -> + Cic.Prod (fresh_binder (), + CicSubstitution.lift_from liftfrom liftno src, + add_right_pi dependent strip liftno (liftfrom + 1) rightno indty tgt) + | Cic.Prod (_, _, tgt) -> + add_right_pi dependent (strip - 1) liftno liftfrom rightno indty tgt + | t -> + if dependent then + Cic.Prod (fresh_binder (), + CicSubstitution.lift_from (rightno + 1) liftno indty, + Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 0 (rightno + 1))) + else + Cic.Prod (Cic.Anonymous, + CicSubstitution.lift_from (rightno + 1) liftno indty, + if rightno = 0 then + Cic.Rel (1 + liftno + rightno) + else + Cic.Appl (Cic.Rel (1 + liftno + rightno) :: mk_rels 1 rightno)) + +let rec add_right_lambda dependent strip liftno liftfrom rightno indty case = +function + | Cic.Prod (_, src, tgt) when strip = 0 -> + Cic.Lambda (fresh_binder (), + CicSubstitution.lift_from liftfrom liftno src, + add_right_lambda dependent strip liftno (liftfrom + 1) rightno indty + case tgt) + | Cic.Prod (_, _, tgt) -> + add_right_lambda true (strip - 1) liftno liftfrom rightno indty + case tgt + | t -> + Cic.Lambda (fresh_binder (), + CicSubstitution.lift_from (rightno + 1) liftno indty, case) + +let rec branch (uri, typeno) insource paramsno t fix head args = + match t with + | Cic.MutInd (uri', typeno', []) when + UriManager.eq uri uri' && typeno = typeno' -> + if insource then + (match args with + | [arg] -> Cic.Appl (fix :: args) + | _ -> Cic.Appl (fix :: [Cic.Appl args])) + else + (match args with + | [] -> head + | _ -> Cic.Appl (head :: args)) + | Cic.Appl (Cic.MutInd (uri', typeno', []) :: tl) when + UriManager.eq uri uri' && typeno = typeno' -> + if insource then + let (lparams, rparams) = split tl paramsno in + match args with + | [arg] -> Cic.Appl (fix :: rparams @ args) + | _ -> Cic.Appl (fix :: rparams @ [Cic.Appl args]) + else + (match args with + | [] -> head + | _ -> Cic.Appl (head :: args)) + | Cic.Prod (binder, src, tgt) -> + if recursive uri typeno src then + let args = List.map (CicSubstitution.lift 1) args in + let phi = + let fix = CicSubstitution.lift 1 fix in + let src = CicSubstitution.lift 1 src in + branch (uri, typeno) true paramsno src fix head [Cic.Rel 1] + in + Cic.Lambda (fresh_binder (), src, + branch (uri, typeno) insource paramsno tgt + (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head) + (args @ [Cic.Rel 1; phi])) + else (* non recursive *) + let args = List.map (CicSubstitution.lift 1) args in + Cic.Lambda (fresh_binder (), src, + branch (uri, typeno) insource paramsno tgt + (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head) + (args @ [Cic.Rel 1])) + | _ -> assert false + +let branch (uri, typeno) insource liftno paramsno t fix head args = + let t = strip_left_params liftno paramsno t in + branch (uri, typeno) insource paramsno t fix head args + +let elim_of ~sort uri typeno = + counter := ~-1; + let (obj, univ) = (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) in + match obj with + | Cic.InductiveDefinition (indTypes, params, leftno, _) -> + let (name, inductive, ty, constructors) = + try + List.nth indTypes typeno + with Failure _ -> assert false + in + let ty = Unshare.unshare ~fresh_univs:true ty in + let constructors = + List.map (fun (name,c)-> name,Unshare.unshare ~fresh_univs:true c) constructors + in + let paramsno = count_pi ty in (* number of (left or right) parameters *) + let rightno = paramsno - leftno in + let dependent = (strip_pi ty <> Cic.Sort Cic.Prop) in + let head = + match strip_pi ty with + Cic.Sort s -> s + | _ -> assert false + in + let conslen = List.length constructors in + let consno = ref (conslen + 1) in + if + not + (CicTypeChecker.check_allowed_sort_elimination uri typeno head sort) + then + raise Can_t_eliminate; + let indty = + let indty = Cic.MutInd (uri, typeno, []) in + if paramsno = 0 then + indty + else + Cic.Appl (indty :: mk_rels 0 paramsno) + in + let mk_constructor consno = + let constructor = Cic.MutConstruct (uri, typeno, consno, []) in + if leftno = 0 then + constructor + else + Cic.Appl (constructor :: mk_rels consno leftno) + in + let p_ty = type_of_p sort dependent leftno indty ty in + let final_ty = + add_right_pi dependent leftno (conslen + 1) 1 rightno indty ty + in + let eliminator_type = + let cic = + Cic.Prod (Cic.Name "P", p_ty, + (List.fold_right + (fun (_, constructor) acc -> + decr consno; + let p = Cic.Rel !consno in + Cic.Prod (Cic.Anonymous, + (delta (uri, typeno) dependent leftno !consno + constructor p [mk_constructor !consno]), + acc)) + constructors final_ty)) + in + add_params (fun b s t -> Cic.Prod (b, s, t)) leftno ty cic + in + let consno = ref (conslen + 1) in + let eliminator_body = + let fix = Cic.Rel (rightno + 2) in + let is_recursive = recursive_type uri typeno constructors in + let recshift = if is_recursive then 1 else 0 in + let (_, branches) = + List.fold_right + (fun (_, ty) (shift, branches) -> + let head = Cic.Rel (rightno + shift + 1 + recshift) in + let b = + branch (uri, typeno) false + (rightno + conslen + 2 + recshift) leftno ty fix head [] + in + (shift + 1, b :: branches)) + constructors (1, []) + in + let shiftno = conslen + rightno + 2 + recshift in + let outtype = + if dependent then + Cic.Rel shiftno + else + let head = + if rightno = 0 then + CicSubstitution.lift 1 (Cic.Rel shiftno) + else + Cic.Appl + ((CicSubstitution.lift (rightno + 1) (Cic.Rel shiftno)) :: + mk_rels 1 rightno) + in + add_right_lambda true leftno shiftno 1 rightno indty head ty + in + let mutcase = + Cic.MutCase (uri, typeno, outtype, Cic.Rel 1, branches) + in + let body = + if is_recursive then + let fixfun = + add_right_lambda dependent leftno (conslen + 2) 1 rightno + indty mutcase ty + in + (* rightno is the decreasing argument, i.e. the argument of + * inductive type *) + Cic.Fix (0, ["aux", rightno, final_ty, fixfun]) + else + add_right_lambda dependent leftno (conslen + 1) 1 rightno indty + mutcase ty + in + let cic = + Cic.Lambda (Cic.Name "P", p_ty, + (List.fold_right + (fun (_, constructor) acc -> + decr consno; + let p = Cic.Rel !consno in + Cic.Lambda (fresh_binder (), + (delta (uri, typeno) dependent leftno !consno + constructor p [mk_constructor !consno]), + acc)) + constructors body)) + in + add_params (fun b s t -> Cic.Lambda (b, s, t)) leftno ty cic + in +(* +debug_print (lazy (CicPp.ppterm eliminator_type)); +debug_print (lazy (CicPp.ppterm eliminator_body)); +*) + let eliminator_type = + FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_type in + let eliminator_body = + FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_body in +(* +debug_print (lazy (CicPp.ppterm eliminator_type)); +debug_print (lazy (CicPp.ppterm eliminator_body)); +*) + let (computed_type, ugraph) = + try + CicTypeChecker.type_of_aux' [] [] eliminator_body + CicUniv.oblivion_ugraph + with CicTypeChecker.TypeCheckerFailure msg -> + raise (Elim_failure (lazy (sprintf + "type checker failure while type checking:\n%s\nerror:\n%s" + (CicPp.ppterm eliminator_body) (Lazy.force msg)))) + in + if not (fst (CicReduction.are_convertible [] + eliminator_type computed_type ugraph)) + then + raise (Failure (sprintf + "internal error: type mismatch on eliminator type\n%s\n%s" + (CicPp.ppterm eliminator_type) (CicPp.ppterm computed_type))); + let suffix = + match sort with + | Cic.Prop -> "_ind" + | Cic.Set -> "_rec" + | Cic.Type _ -> "_rect" + | _ -> assert false + in + (* let name = UriManager.name_of_uri uri ^ suffix in *) + let name = name ^ suffix in + let buri = UriManager.buri_of_uri uri in + let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in + let obj_attrs = [`Class (`Elim sort); `Generated] in + uri, + Cic.Constant (name, Some eliminator_body, eliminator_type, [], obj_attrs) + | _ -> + failwith (sprintf "not an inductive definition (%s)" + (UriManager.string_of_uri uri)) +;; + +let generate_elimination_principles ~add_obj ~add_coercion uri obj = + match obj with + | Cic.InductiveDefinition (indTypes,_,_,attrs) -> + let _,inductive,_,_ = List.hd indTypes in + if not inductive then [] + else + let _,all_eliminators = + List.fold_left + (fun (i,res) _ -> + let elim sort = + try Some (elim_of ~sort uri i) + with Can_t_eliminate -> None + in + i+1, + HExtlib.filter_map + elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ] @ res + ) (0,[]) indTypes + in + List.fold_left + (fun lemmas (uri,obj) -> add_obj uri obj @ uri::lemmas) + [] all_eliminators + | _ -> [] +;; + + +let init () = + LibrarySync.add_object_declaration_hook generate_elimination_principles;; diff --git a/matita/components/library/cicElim.mli b/matita/components/library/cicElim.mli new file mode 100644 index 000000000..70c1c2167 --- /dev/null +++ b/matita/components/library/cicElim.mli @@ -0,0 +1,29 @@ +(* Copyright (C) 2004, 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/ + *) + + (** internal error while generating elimination principle *) +exception Elim_failure of string Lazy.t + +val init : unit -> unit diff --git a/matita/components/library/cicFix.ml b/matita/components/library/cicFix.ml new file mode 100644 index 000000000..21cb99093 --- /dev/null +++ b/matita/components/library/cicFix.ml @@ -0,0 +1,69 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* $Id: librarySync.ml 9482 2009-01-08 18:12:28Z tassi $ *) + +let generate_sibling_mutual_definitions ~add_obj ~add_coercion uri obj = + match obj with + | Cic.Constant (name_to_avoid,Some bo,_,_,attrs) when + List.mem (`Flavour `MutualDefinition) attrs -> + (match bo with + Cic.Fix (_,funs) -> + snd ( + List.fold_right + (fun (name,idx,ty,bo) (n,uris) -> + if name = name_to_avoid then + (n-1,uris) + else + let uri = + UriManager.uri_of_string + (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in + let bo = Cic.Fix (n-1,funs) in + let obj = Cic.Constant (name,Some bo,ty,[],attrs) in + let lemmas = add_obj uri obj in + (n-1,lemmas @ uri::uris)) + (List.tl funs) (List.length funs,[])) + | Cic.CoFix (_,funs) -> + snd ( + List.fold_right + (fun (name,ty,bo) (n,uris) -> + if name = name_to_avoid then + (n-1,uris) + else + let uri = + UriManager.uri_of_string + (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in + let bo = Cic.CoFix (n-1,funs) in + let obj = Cic.Constant (name,Some bo,ty,[],attrs) in + let lemmas = add_obj uri obj in + (n-1,lemmas @ uri::uris)) + (List.tl funs) (List.length funs,[])) + | _ -> assert false) + | _ -> [] +;; + + +let init () = + LibrarySync.add_object_declaration_hook generate_sibling_mutual_definitions;; diff --git a/matita/components/library/cicFix.mli b/matita/components/library/cicFix.mli new file mode 100644 index 000000000..de361cc7c --- /dev/null +++ b/matita/components/library/cicFix.mli @@ -0,0 +1,26 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +val init : unit -> unit diff --git a/matita/components/library/cicRecord.ml b/matita/components/library/cicRecord.ml new file mode 100644 index 000000000..e76ca9ca2 --- /dev/null +++ b/matita/components/library/cicRecord.ml @@ -0,0 +1,135 @@ +(* 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 rec_ty uri leftno = + let rec_ty = Cic.MutInd (uri,0,[]) in + if leftno = 0 then rec_ty else + Cic.Appl (rec_ty :: (CicUtil.mk_rels leftno 0)) + +let generate_one_proj uri params paramsno fields t i = + let mk_lambdas l start = + List.fold_right (fun (name,ty) acc -> + Cic.Lambda (Cic.Name name,ty,acc)) l start in + let recty = rec_ty uri paramsno in + let outtype = Cic.Lambda (Cic.Name "w'", CicSubstitution.lift 1 recty, t) in + (mk_lambdas params + (Cic.Lambda (Cic.Name "w", recty, + Cic.MutCase (uri,0,outtype, Cic.Rel 1, + [mk_lambdas fields (Cic.Rel i)])))) + +let projections_of uri field_names = + let buri = UriManager.buri_of_uri uri in + let obj,ugraph = CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri in + match obj with + Cic.InductiveDefinition ([_,_,sort,[_,ty]],params,paramsno,_) -> + assert (params = []); (* general case not implemented *) + let leftparams,ty = + let rec aux = + function + 0,ty -> [],ty + | n,Cic.Prod (Cic.Name name,s,t) -> + let leftparams,ty = aux (n - 1,t) in + (name,s)::leftparams,ty + | _,_ -> assert false + in + aux (paramsno,ty) + in + let fields = + let rec aux = + function + Cic.MutInd _, [] + | Cic.Appl _, [] -> [] + | Cic.Prod (_,s,t), name::tl -> (name,s)::aux (t,tl) + | _,_ -> assert false + in + aux ((CicSubstitution.lift 1 ty),field_names) + in + let rec aux i = + function + Cic.MutInd _, [] + | Cic.Appl _, [] -> [] + | Cic.Prod (_,s,t), name::tl -> + let p = generate_one_proj uri leftparams paramsno fields s i in + let puri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in + (puri,name,p) :: + aux (i - 1) + (CicSubstitution.subst + (Cic.Appl + (Cic.Const (puri,[]) :: + CicUtil.mk_rels paramsno 2 @ [Cic.Rel 1]) + ) t, tl) + | _,_ -> assert false + in + aux (List.length fields) (CicSubstitution.lift 2 ty,field_names) + | _ -> assert false +;; + +let generate_projections ~add_obj ~add_coercion (uri as orig_uri) obj = + match obj with + | Cic.InductiveDefinition (inductivefuns,_,_,attrs) -> + let rec get_record_attrs = + function + | [] -> None + | (`Class (`Record fields))::_ -> Some fields + | _::tl -> get_record_attrs tl + in + (match get_record_attrs attrs with + | None -> [] + | Some fields -> + let uris = ref [] in + let projections = + projections_of uri (List.map (fun (x,_,_) -> x) fields) + in + List.iter2 + (fun (uri, name, bo) (_name, coercion, arity) -> + try + let ty, _ = + CicTypeChecker.type_of_aux' [] [] bo CicUniv.oblivion_ugraph in + let attrs = [`Class `Projection; `Generated] in + let obj = Cic.Constant (name,Some bo,ty,[],attrs) in + let lemmas = add_obj uri obj in + let lemmas1 = + if not coercion then [] else + add_coercion uri arity 0 (UriManager.buri_of_uri orig_uri) + in + uris := lemmas1 @ lemmas @ uri::!uris + with + CicTypeChecker.TypeCheckerFailure s -> + HLog.message ("Unable to create projection " ^ name ^ + " cause: " ^ Lazy.force s); + | CicEnvironment.Object_not_found uri -> + let depend = UriManager.name_of_uri uri in + HLog.message ("Unable to create projection " ^ name ^ + " because it requires " ^ depend) + ) projections fields; + !uris) + | _ -> [] +;; + + +let init () = + LibrarySync.add_object_declaration_hook generate_projections;; diff --git a/matita/components/library/cicRecord.mli b/matita/components/library/cicRecord.mli new file mode 100644 index 000000000..de361cc7c --- /dev/null +++ b/matita/components/library/cicRecord.mli @@ -0,0 +1,26 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +val init : unit -> unit diff --git a/matita/components/library/coercDb.ml b/matita/components/library/coercDb.ml new file mode 100644 index 000000000..b7e390229 --- /dev/null +++ b/matita/components/library/coercDb.ml @@ -0,0 +1,175 @@ +(* 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 = + match src, tgt with + | Uri src, Uri tgt -> + let coarse_eq = UriManager.eq src tgt in + let t = CicUtil.term_of_uri src in + let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in + (match ty, exact with + | Cic.Prod _, true -> false + | Cic.Prod _, false -> coarse_eq + | _ -> coarse_eq) + | Sort _, Sort _ -> true + | Fun _,Fun _ when not exact -> true (* only one Funclass *) + | Fun i,Fun j when i = j -> true (* only one Funclass *) + | _, _ -> false +;; + +let to_list db = + List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b,c -> a,b,c) l) db +;; + +let rec myfilter p = function + | [] -> [] + | (s,t,l)::tl -> + let l = + HExtlib.filter_map + (fun (u,n,saturations,cpos) as e -> + if p (s,t,u,saturations,cpos) then + if n = 1 then None + else Some (u,n-1,saturations,cpos) + else Some e) + l + in + if l = [] then myfilter p tl else (s,t,l)::myfilter p tl +;; + +let remove_coercion p = db := myfilter p !db;; + +let find_coercion f = + List.map + (fun (uri,_,saturations,_) -> uri,saturations) + (List.flatten + (HExtlib.filter_map (fun (s,t,l) -> if f (s,t) then Some l else None) !db)) +;; + +let is_a_coercion t = + try + let uri = CicUtil.uri_of_term t in + match + HExtlib.filter_map + (fun (src,tgt,xl) -> + let xl = List.filter (fun (x,_,_,_) -> UriManager.eq uri x) xl in + if xl = [] then None else Some (src,tgt,xl)) + !db + with + | [] -> None + | (_,_,[])::_ -> assert false + | [src,tgt,[u,_,s,p]] -> Some (src,tgt,u,s,p) + | (src,tgt,(u,_,s,p)::_)::_ -> + debug_print + (lazy "coercion has multiple entries, returning the first one"); + Some (src,tgt,u,s,p) + with Invalid_argument _ -> + debug_print (lazy "this term is not a constant"); + None +;; + +let add_coercion (src,tgt,u,saturations,cpos) = + let f s t = eq_carr s src && eq_carr t tgt in + let where = List.filter (fun (s,t,_) -> f s t) !db in + let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in + match where with + | [] -> db := (src,tgt,[u,1,saturations,cpos]) :: !db + | (src,tgt,l)::tl -> + assert (tl = []); (* not sure, this may be a feature *) + if List.exists (fun (x,_,_,_) -> UriManager.eq u x) l then + let l = + let l = + (* this code reorders the list so that adding an already declared + * coercion moves it to the begging of the list *) + let item = List.find (fun (x,_,_,_) -> UriManager.eq u x) l in + let rest=List.filter (fun (x,_,_,_) -> not (UriManager.eq u x)) l in + item :: rest + in + List.map + (fun (x,n,x_saturations,x_cpos) as e -> + if UriManager.eq u x then + (* not sure, this may be a feature *) + (assert (x_saturations = saturations && x_cpos = cpos); + (x,n+1,saturations,cpos)) + else e) + l + in + db := (src,tgt,l)::tl @ rest + else + db := (src,tgt,(u,1,saturations,cpos)::l)::tl @ rest +;; + +let prefer u = + let prefer (s,t,l) = + let lb,la = List.partition (fun (uri,_,_,_) -> UriManager.eq uri u) l in + s,t,lb@la + in + db := List.map prefer !db; +;; diff --git a/matita/components/library/coercDb.mli b/matita/components/library/coercDb.mli new file mode 100644 index 000000000..59c07f447 --- /dev/null +++ b/matita/components/library/coercDb.mli @@ -0,0 +1,67 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + +type coerc_carr = private + | Uri of UriManager.uri (* const, mutind, mutconstr *) + | Sort of Cic.sort (* Prop, Set, Type *) + | Fun of int + | Dead +;; + +val eq_carr: ?exact:bool -> coerc_carr -> coerc_carr -> bool +val string_of_carr: coerc_carr -> string + +(* takes a term in whnf ~delta:false and a desired ariety *) +val coerc_carr_of_term: Cic.term -> int -> coerc_carr + +type coerc_db +val empty_coerc_db : coerc_db +val dump: unit -> coerc_db +val restore: coerc_db -> unit + +val to_list: + coerc_db -> + (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list + +(* src carr, tgt carr, uri, saturations, coerced position + * invariant: + * if the constant pointed by uri has n argments + * n = coerced position + saturations + FunClass arity + *) + +type saturations = int +type coerced_pos = int +type coercion_entry = + coerc_carr * coerc_carr * UriManager.uri * saturations * coerced_pos +val add_coercion: coercion_entry -> unit +val remove_coercion: (coercion_entry -> bool) -> unit + +val find_coercion: + (coerc_carr * coerc_carr -> bool) -> (UriManager.uri * int) list + +val is_a_coercion: Cic.term -> coercion_entry option + +val prefer: UriManager.uri -> unit diff --git a/matita/components/library/librarian.ml b/matita/components/library/librarian.ml new file mode 100644 index 000000000..2c2ba6ff2 --- /dev/null +++ b/matita/components/library/librarian.ml @@ -0,0 +1,418 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +let debug = ref 0 + +let time_stamp = + let old = ref 0.0 in + fun msg -> + if !debug > 0 then begin + let times = Unix.times () in + let stamp = times.Unix.tms_utime +. times.Unix.tms_stime in + let lap = stamp -. !old in + Printf.eprintf "TIME STAMP (%s): %f\n" msg lap; flush stderr; + old := stamp + end + +exception NoRootFor of string + +let absolutize path = + let path = + if String.length path > 0 && path.[0] <> '/' then + Sys.getcwd () ^ "/" ^ path + else + path + in + HExtlib.normalize_path path +;; + + +let find_root path = + let path = absolutize path in + let paths = List.rev (Str.split (Str.regexp "/") path) in + let rec build = function + | he::tl as l -> ("/" ^ String.concat "/" (List.rev l) ^ "/") :: build tl + | [] -> ["/"] + in + let paths = List.map HExtlib.normalize_path (build paths) in + try HExtlib.find_in paths "root" + with Failure "find_in" -> + raise (NoRootFor (path ^ " (" ^ String.concat ", " paths ^ ")")) +;; + +let ensure_trailing_slash s = + if s = "" then "/" else + if s.[String.length s-1] <> '/' then s^"/" else s +;; + +let remove_trailing_slash s = + if s = "" then "" else + let len = String.length s in + if s.[len-1] = '/' then String.sub s 0 (len-1) else s +;; + +let load_root_file rootpath = + let data = HExtlib.input_file rootpath in + let lines = Str.split (Str.regexp "\n") data in + let clean s = + Pcre.replace ~pat:"[ \t]+" ~templ:" " + (Pcre.replace ~pat:"^ *" (Pcre.replace ~pat:" *$" s)) + in + List.map + (fun l -> + match Str.split (Str.regexp "=") l with + | [k;v] -> clean k, Http_getter_misc.strip_trailing_slash (clean v) + | _ -> raise (Failure ("Malformed root file: " ^ rootpath))) + lines +;; + +let find_root_for ~include_paths file = + let include_paths = "" :: Sys.getcwd () :: include_paths in + let rec find_path_for file = + try HExtlib.find_in include_paths file + with Failure "find_in" -> + if Filename.check_suffix file ".ma" then begin + let mma = Filename.chop_suffix file ".ma" ^ ".mma" in + HLog.warn ("We look for: " ^ mma); + let path = find_path_for mma in + Filename.chop_suffix path ".mma" ^ ".ma" + end else begin + HLog.error ("We are in: " ^ Sys.getcwd ()); + HLog.error ("Unable to find: "^file^"\nPaths explored:"); + List.iter (fun x -> HLog.error (" - "^x)) include_paths; + raise (NoRootFor file) + end + in + let path = find_path_for file in + let path = absolutize path in +(* HLog.debug ("file "^file^" resolved as "^path); *) + let rootpath, root, buri = + try + let mburi = Helm_registry.get "matita.baseuri" in + match Str.split (Str.regexp " ") mburi with + | [root; buri] when HExtlib.is_prefix_of root path -> + ":registry:", root, buri + | _ -> raise (Helm_registry.Key_not_found "matita.baseuri") + with Helm_registry.Key_not_found "matita.baseuri" -> + let rootpath = find_root path in + let buri = List.assoc "baseuri" (load_root_file rootpath) in + rootpath, Filename.dirname rootpath, buri + in +(* HLog.debug ("file "^file^" rooted by "^rootpath^""); *) + let uri = Http_getter_misc.strip_trailing_slash buri in + if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then + HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri); + ensure_trailing_slash root, remove_trailing_slash uri, path + +;; + +let mk_baseuri root extra = + let chop name = + assert(Filename.check_suffix name ".ma" || + Filename.check_suffix name ".mma"); + try Filename.chop_extension name + with Invalid_argument "Filename.chop_extension" -> name + in + remove_trailing_slash (HExtlib.normalize_path (root ^ "/" ^ chop extra)) +;; + +let baseuri_of_script ~include_paths file = + let root, buri, path = find_root_for ~include_paths file in + let path = HExtlib.normalize_path path in + let root = HExtlib.normalize_path root in + let lpath = Str.split (Str.regexp "/") path in + let lroot = Str.split (Str.regexp "/") root in + let rec substract l1 l2 = + match l1, l2 with + | h1::tl1,h2::tl2 when h1 = h2 -> substract tl1 tl2 + | l,[] -> l + | _ -> raise (NoRootFor (file ^" "^path^" "^root)) + in + let extra_buri = substract lpath lroot in + let extra = String.concat "/" extra_buri in + root, + mk_baseuri buri extra, + path, + extra +;; + +let find_roots_in_dir dir = + HExtlib.find ~test:(fun f -> + Filename.basename f = "root" && + try (Unix.stat f).Unix.st_kind = Unix.S_REG + with Unix.Unix_error _ -> false) + dir +;; + +(* make *) +let load_deps_file f = + let deps = ref [] in + let ic = open_in f in + try + while true do + begin + let l = input_line ic in + match Str.split (Str.regexp " ") l with + | [] -> + HLog.error ("Malformed deps file: " ^ f); + raise (Failure ("Malformed deps file: " ^ f)) + | he::tl -> deps := (he,tl) :: !deps + end + done; !deps + with End_of_file -> !deps +;; + +type options = (string * string) list + +module type Format = + sig + type source_object + type target_object + val load_deps_file: string -> (source_object * source_object list) list + val string_of_source_object: source_object -> string + val string_of_target_object: target_object -> string + val build: options -> source_object -> bool + val root_and_target_of: + options -> source_object -> + (* root, relative source, writeable target, read only target *) + string option * source_object * target_object * target_object + val mtime_of_source_object: source_object -> float option + val mtime_of_target_object: target_object -> float option + val is_readonly_buri_of: options -> source_object -> bool + end + +module Make = functor (F:Format) -> struct + + type status = Done of bool + | Ready of bool + + let say s = if !debug > 0 then prerr_endline ("make: "^s);; + + let unopt_or_call x f y = match x with Some _ -> x | None -> f y;; + + let fst4 = function (x,_,_,_) -> x;; + + let modified_before_s_t (_,cs, ct, _, _) a b = + + if !debug > 1 then time_stamp ("L s_t: a " ^ F.string_of_source_object a); + if !debug > 1 then time_stamp ("L s_t: b " ^ F.string_of_target_object b); + + let a = try Hashtbl.find cs a with Not_found -> assert false in + let b = + try + match Hashtbl.find ct b with + | Some _ as x -> x + | None -> + match F.mtime_of_target_object b with + | Some t as x -> + Hashtbl.remove ct b; + Hashtbl.add ct b x; x + | x -> x + with Not_found -> assert false + in + let r = match a, b with + | Some a, Some b -> a <= b + | _ -> false + in + + if !debug > 1 then time_stamp ("L s_t: " ^ string_of_bool r); + + r + + let modified_before_t_t (_,_,ct, _, _) a b = + + if !debug > 1 then time_stamp ("L t_t: a " ^ F.string_of_target_object a); + if !debug > 1 then time_stamp ("L t_t: b " ^ F.string_of_target_object b); + + let a = + try + match Hashtbl.find ct a with + | Some _ as x -> x + | None -> + match F.mtime_of_target_object a with + | Some t as x -> + Hashtbl.remove ct a; + Hashtbl.add ct a x; x + | x -> x + with Not_found -> assert false + in + let b = + try + match Hashtbl.find ct b with + | Some _ as x -> x + | None -> + match F.mtime_of_target_object b with + | Some t as x -> + Hashtbl.remove ct b; + Hashtbl.add ct b x; x + | x -> x + with Not_found -> assert false + in + let r = match a, b with + | Some a, Some b -> + + if !debug > 1 then time_stamp ("tt: a " ^ string_of_float a); + if !debug > 1 then time_stamp ("tt: b " ^ string_of_float b); + + a <= b + | _ -> false + in + + if !debug > 1 then time_stamp ("L t_t: " ^ string_of_bool r); + + r + + let rec purge_unwanted_roots wanted deps = + let roots, rest = + List.partition + (fun (t,_,d,_,_) -> + not (List.exists (fun (_,_,d1,_,_) -> List.mem t d1) deps)) + deps + in + let newroots = List.filter (fun (t,_,_,_,_) -> List.mem t wanted) roots in + if newroots = roots then + deps + else + purge_unwanted_roots wanted (newroots @ rest) + ;; + + let is_not_ro (opts,_,_,_,_) (f,_,_,r,_) = + match r with + | Some root -> not (F.is_readonly_buri_of opts f) + | None -> assert false + ;; + +(* FG: new sorting algorithm ************************************************) + + let rec make_aux root opts ok deps = + List.fold_left (make_one root opts) ok deps + + and make_one root opts ok what = + let lo, _, ct, cc, cd = opts in + let t, path, deps, froot, tgt = what in + let str = F.string_of_source_object t in + let map (okd, okt) d = + let (_, _, _, _, tgtd) as whatd = (Hashtbl.find cd d) in + let r = make_one root opts okd whatd in + r, okt && modified_before_t_t opts tgtd tgt + in + time_stamp ("L : processing " ^ str); + try + let r = Hashtbl.find cc t in + time_stamp ("L : " ^ string_of_bool r ^ " " ^ str); + ok && r +(* say "already built" *) + with Not_found -> + let okd, okt = List.fold_left map (true, modified_before_s_t opts t tgt) deps in + let res = + if okd then + if okt then true else + let build path = match froot with + | Some froot when froot = root -> + if is_not_ro opts what then F.build lo path else + (HLog.error ("Read only baseuri for: " ^ str ^ + ", I won't compile it even if it is out of date"); + false) + | Some froot -> make froot [path] + | None -> HLog.error ("No root for: " ^ str); false + in + Hashtbl.remove ct tgt; + Hashtbl.add ct tgt None; + time_stamp ("L : BUILDING " ^ str); + let res = build path in + time_stamp ("L : DONE " ^ str); res + else false + in + time_stamp ("L : " ^ string_of_bool res ^ " " ^ str); + Hashtbl.add cc t res; ok && res + +(****************************************************************************) + + and make root targets = + time_stamp "L : ENTERING"; + HLog.debug ("Entering directory '"^root^"'"); + let old_root = Sys.getcwd () in + Sys.chdir root; + let deps = F.load_deps_file (root^"/depends") in + let local_options = load_root_file (root^"/root") in + let baseuri = List.assoc "baseuri" local_options in + print_endline ("Entering HELM directory: " ^ baseuri); flush stdout; + let caches,cachet,cachec,cached = + Hashtbl.create 73, Hashtbl.create 73, Hashtbl.create 73, Hashtbl.create 73 + in + (* deps are enriched with these informations to sped up things later *) + let deps = + List.map + (fun (file,d) -> + let r,path,wtgt,rotgt = F.root_and_target_of local_options file in + Hashtbl.add caches file (F.mtime_of_source_object file); + (* if a read only target exists, we use that one, otherwise + we use the writeable one that may be compiled *) + let _,_,_,_, tgt as tuple = + match F.mtime_of_target_object rotgt with + | Some _ as mtime -> + Hashtbl.add cachet rotgt mtime; + (file, path, d, r, rotgt) + | None -> + Hashtbl.add cachet wtgt (F.mtime_of_target_object wtgt); + (file, path, d, r, wtgt) + in + Hashtbl.add cached file tuple; + tuple + ) + deps + in + let opts = local_options, caches, cachet, cachec, cached in + let ok = + if targets = [] then + make_aux root opts true deps + else + make_aux root opts true (purge_unwanted_roots targets deps) + in + print_endline ("Leaving HELM directory: " ^ baseuri); flush stdout; + HLog.debug ("Leaving directory '"^root^"'"); + Sys.chdir old_root; + time_stamp "L : LEAVING"; + ok + ;; + +end + +let write_deps_file where deps = match where with + | Some root -> + let oc = open_out (root ^ "/depends") in + let map (t, d) = output_string oc (t^" "^String.concat " " d^"\n") in + List.iter map deps; close_out oc; + HLog.message ("Generated: " ^ root ^ "/depends") + | None -> + print_endline (String.concat " " (List.flatten (List.map snd deps))) + +(* FG ***********************************************************************) + +(* scheme uri part as defined in URI Generic Syntax (RFC 3986) *) +let uri_scheme_rex = Pcre.regexp "^[[:alpha:]][[:alnum:]\-+.]*:" + +let is_uri str = + Pcre.pmatch ~rex:uri_scheme_rex str diff --git a/matita/components/library/librarian.mli b/matita/components/library/librarian.mli new file mode 100644 index 000000000..4eed9051d --- /dev/null +++ b/matita/components/library/librarian.mli @@ -0,0 +1,105 @@ +(* Copyright (C) 2004-2008, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +exception NoRootFor of string + +(* make a relative path absolute *) +val absolutize: string -> string + +(* a root file is a text, line oriented, file containing pairs separated by + * the '=' character. Example: + * + * baseuri = cic:/foo/bar + * include_paths = ../baz ../../pippo + * + * spaces at the end/begin of the line and around '=' are ignored, + * multiple spaces in the middle of an item are shrinked to one. + *) +val load_root_file: string -> (string*string) list + +(* baseuri_of_script ?(inc:REG[matita.includes]) fname + * -> + * root, buri, fullpath, rootrelativepath + * sample: baseuri_of_script a.ma -> /home/pippo/devel/, cic:/matita/a, + * /home/pippo/devel/a.ma, a.ma *) +val baseuri_of_script: + include_paths:string list -> string -> string * string * string * string + +(* given a baseuri and a file name (relative to its root) + * returns a baseuri: + * mk_baseuri "cic:/matita" "nat/plus.ma" -> "cic:/matita/nat/plus" + *) +val mk_baseuri: string -> string -> string + +(* finds all the roots files in the specified dir, roots are + * text files, readable by the user named 'root' + *) +val find_roots_in_dir: string -> string list + +(* make implementation *) +type options = (string * string) list + +module type Format = + sig + type source_object + type target_object + val load_deps_file: string -> (source_object * source_object list) list + val string_of_source_object: source_object -> string + val string_of_target_object: target_object -> string + val build: options -> source_object -> bool + val root_and_target_of: + options -> source_object -> + (* root, relative source, writeable target, read only target *) + string option * source_object * target_object * target_object + val mtime_of_source_object: source_object -> float option + val mtime_of_target_object: target_object -> float option + val is_readonly_buri_of: options -> source_object -> bool + end + +module Make : + functor (F : Format) -> + sig + (* make [root dir] [targets], targets = [] means make all *) + val make : string -> F.source_object list -> bool + end + +(* deps are made with scripts names, for example lines like + * + * nat/plus.ma nat/nat.ma logic/equality.ma + * + * state that plus.ma needs nat and equality + *) +val load_deps_file: string -> (string * string list) list +val write_deps_file: string option -> (string * string list) list -> unit + +(* FG ***********************************************************************) + +(* true if the argunent starts with a uri scheme prefix *) +val is_uri: string -> bool + +(* Valid values: 0: no debug; 1: normal debug; > 1: extra debug *) +val debug: int ref + +val time_stamp: string -> unit diff --git a/matita/components/library/libraryClean.ml b/matita/components/library/libraryClean.ml new file mode 100644 index 000000000..8e9f430ba --- /dev/null +++ b/matita/components/library/libraryClean.ml @@ -0,0 +1,275 @@ +(* 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 = + 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 = + 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 = + let cache_of_processed_baseuri = Hashtbl.create 1024 in + let dbd = LibraryDb.instance () in + let dbtype = + if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User + in + Hashtbl.clear cache_of_processed_baseuri; + let buris = List.map Http_getter_misc.strip_trailing_slash buris in + debug_prerr "clean_baseuris called on:"; + if debug then + List.iter debug_prerr buris; + let l = close_db cache_of_processed_baseuri [] buris in + let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in + let l = List.map UriManager.uri_of_string l in + debug_prerr "clean_baseuri will remove:"; + if debug then + List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; + List.iter + (fun baseuri -> + !decompile ~baseuri; + try + let obj_file = + LibraryMisc.obj_file_of_baseuri ~must_exist:false ~writable:true ~baseuri + in + HExtlib.safe_remove obj_file ; + HExtlib.safe_remove + (LibraryMisc.lexicon_file_of_baseuri + ~must_exist:false ~writable:true ~baseuri) ; + HExtlib.rmdir_descend (Filename.chop_extension obj_file) + with Http_getter_types.Key_not_found _ -> ()) + (HExtlib.list_uniq (List.fast_sort Pervasives.compare + (List.map (UriManager.buri_of_uri) l @ buris))); + List.iter + (let last_baseuri = ref "" in + fun uri -> + let buri = UriManager.buri_of_uri uri in + if buri <> !last_baseuri then + begin + if not (Helm_registry.get_bool "matita.verbose") then + (print_endline ("matitaclean " ^ buri ^ "/");flush stdout) + else + HLog.message ("Removing: " ^ buri ^ "/*"); + last_baseuri := buri + end; + LibrarySync.remove_obj uri + ) l; + if HSql.isMysql dbtype dbd then + begin + cleaned_no := !cleaned_no + List.length l; + if !cleaned_no > 30 && HSql.isMysql dbtype dbd then + begin + cleaned_no := 0; + List.iter + (function table -> + ignore (HSql.exec dbtype dbd ("OPTIMIZE TABLE " ^ table))) + [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl (); + MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl(); + MetadataTypes.count_tbl()] + end + end diff --git a/matita/components/library/libraryClean.mli b/matita/components/library/libraryClean.mli new file mode 100644 index 000000000..89f3b7b1d --- /dev/null +++ b/matita/components/library/libraryClean.mli @@ -0,0 +1,29 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +val set_decompile_cb: (baseuri: string -> unit) -> unit + +val db_uris_of_baseuri : string -> string list +val clean_baseuris : ?verbose:bool -> string list -> unit diff --git a/matita/components/library/libraryDb.ml b/matita/components/library/libraryDb.ml new file mode 100644 index 000000000..e82e91f97 --- /dev/null +++ b/matita/components/library/libraryDb.ml @@ -0,0 +1,212 @@ +(* 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 () = + 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 () = + 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 = + 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 = + let dbd = instance () in + let name_tbl = MetadataTypes.name_tbl () in + let dbtype = + if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User + in + let escape s = + Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" + (HSql.escape dbtype dbd s) + in + let query = Printf.sprintf + ("SELECT source FROM %s WHERE source LIKE '%s#xpointer%%' " + ^^ HSql.escape_string_for_like dbtype dbd) + name_tbl (escape (UriManager.string_of_uri uri)) + in + let rc = HSql.exec dbtype dbd query in + let l = ref [] in + HSql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l); + List.map UriManager.uri_of_string !l + diff --git a/matita/components/library/libraryDb.mli b/matita/components/library/libraryDb.mli new file mode 100644 index 000000000..e608a9c24 --- /dev/null +++ b/matita/components/library/libraryDb.mli @@ -0,0 +1,35 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +val dbtype_of_string: string -> HSql.dbtype + +val instance: unit -> HSql.dbd +val parse_dbd_conf: unit -> HSql.dbspec + +val create_owner_environment: unit -> unit +val clean_owner_environment: unit -> unit + +val remove_uri: UriManager.uri -> unit +val xpointers_of_ind: UriManager.uri -> UriManager.uri list diff --git a/matita/components/library/libraryMisc.ml b/matita/components/library/libraryMisc.ml new file mode 100644 index 000000000..7c82e27c4 --- /dev/null +++ b/matita/components/library/libraryMisc.ml @@ -0,0 +1,38 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* $Id$ *) + +let resolve ~must_exist ~writable ~local baseuri = + if must_exist then + Http_getter.resolve ~local ~writable baseuri + else + Http_getter.filename ~local ~writable baseuri + +let obj_file_of_baseuri ~must_exist ~writable ~baseuri = + resolve ~must_exist ~writable ~local:true baseuri ^ ".moo" +let lexicon_file_of_baseuri ~must_exist ~writable ~baseuri = + resolve ~must_exist ~writable ~local:true baseuri ^ ".lexicon" + diff --git a/matita/components/library/libraryMisc.mli b/matita/components/library/libraryMisc.mli new file mode 100644 index 000000000..2c6bfd193 --- /dev/null +++ b/matita/components/library/libraryMisc.mli @@ -0,0 +1,30 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* only for local uris *) +val obj_file_of_baseuri: + must_exist:bool -> writable:bool -> baseuri:string -> string +val lexicon_file_of_baseuri: + must_exist:bool -> writable:bool -> baseuri:string -> string diff --git a/matita/components/library/librarySync.ml b/matita/components/library/librarySync.ml new file mode 100644 index 000000000..185ae5315 --- /dev/null +++ b/matita/components/library/librarySync.ml @@ -0,0 +1,374 @@ +(* 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 = + 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 -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj + +let index_obj = + let profiler = HExtlib.profile "add_obj.index_obj" in + fun ~dbd ~uri -> + profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri + +let remove_obj uri = + 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 = + 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 += + let coer_ty,_ = + let coer = CicUtil.term_of_uri uri in + CicTypeChecker.type_of_aux' [] [] coer CicUniv.oblivion_ugraph + in + (* we have to get the source and the tgt type uri + * in Coq syntax we have already their names, but + * since we don't support Funclass and similar I think + * all the coercion should be of the form + * (A:?)(B:?)T1->T2 + * So we should be able to extract them from the coercion type + * + * Currently only (_:T1)T2 is supported. + * should we saturate it with metas in case we insert it? + * + *) + let spine2list ty = + let rec aux = function + | Cic.Prod( _, src, tgt) -> src::aux tgt + | t -> [t] + in + aux ty + in + let src_carr, tgt_carr, no_args = + let get_classes arity saturations l = + (* this is the ackerman's function revisited *) + let rec aux = function + 0,0,None,tgt::src::_ -> src,Some (`Class tgt) + | 0,0,target,src::_ -> src,target + | 0,saturations,None,tgt::tl -> aux (0,saturations,Some (`Class tgt),tl) + | 0,saturations,target,_::tl -> aux (0,saturations - 1,target,tl) + | arity,saturations,None,_::tl -> + aux (arity, saturations, Some `Funclass, tl) + | arity,saturations,target,_::tl -> + aux (arity - 1, saturations, target, tl) + | _ -> assert false + in + aux (arity,saturations,None,List.rev l) + in + let types = spine2list coer_ty in + let src,tgt = get_classes arity saturations types in + CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src) 0, + (match tgt with + | None -> assert false + | Some `Funclass -> CoercDb.coerc_carr_of_term (Cic.Implicit None) arity + | Some (`Class tgt) -> + CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) 0), + List.length types - 1 + in + let already_in_obj src_carr tgt_carr uri obj = + List.exists + (fun (s,t,ul) -> + if not (CoercDb.eq_carr s src_carr && + CoercDb.eq_carr t tgt_carr) + then false + else + List.exists + (fun u,_,_ -> + let bo, ty = + match obj with + | Cic.Constant (_, Some bo, ty, _, _) -> bo, ty + | _ -> + (* this is not a composite coercion, thus the uri is valid *) + let bo = CicUtil.term_of_uri uri in + bo, + fst (CicTypeChecker.type_of_aux' [] [] bo + CicUniv.oblivion_ugraph) + in + let are_body_convertible = + fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo + CicUniv.oblivion_ugraph) + in + if not are_body_convertible then + (HLog.warn + ("Coercions " ^ + UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri + uri^" are not convertible, but are between the same nodes.\n"^ + "From now on unification can fail randomly."); + false) + else + match t, tgt_carr with + | CoercDb.Sort (Cic.Type i), CoercDb.Sort (Cic.Type j) + | CoercDb.Sort (Cic.CProp i), CoercDb.Sort (Cic.CProp j) + when not (CicUniv.eq i j) -> + (HLog.warn + ("Coercion " ^ UriManager.string_of_uri uri ^ " has the same " ^ + "body of " ^ UriManager.string_of_uri u ^ " but lives in a " ^ + "different universe : " ^ + CicUniv.string_of_universe j ^ " <> " ^ + CicUniv.string_of_universe i); false) + | CoercDb.Sort Cic.Prop , CoercDb.Sort Cic.Prop + | CoercDb.Sort (Cic.Type _) , CoercDb.Sort (Cic.Type _) + | CoercDb.Sort (Cic.CProp _), CoercDb.Sort (Cic.CProp _) -> + (HLog.warn + ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^ + "it is a duplicate of " ^ UriManager.string_of_uri u); + true) + | CoercDb.Sort s1, CoercDb.Sort s2 -> + (HLog.warn + ("Coercion " ^ UriManager.string_of_uri uri ^ " has the same " ^ + "body of " ^ UriManager.string_of_uri u ^ " but lives in a " ^ + "different universe : " ^ + CicPp.ppterm (Cic.Sort s1) ^ " <> " ^ + CicPp.ppterm (Cic.Sort s2)); false) + | _ -> + let ty', _ = + CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri u) + CicUniv.oblivion_ugraph + in + if CicUtil.alpha_equivalence ty ty' then + (HLog.warn + ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^ + "it is a duplicate of " ^ UriManager.string_of_uri u); + true) + else false + + ) + ul) + (CoercDb.to_list (CoercDb.dump ())) + in + let cpos = no_args - arity - saturations - 1 in + if not add_composites then + (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos); []) + else + let _ = + if already_in_obj src_carr tgt_carr uri + (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri)) then + raise (AlreadyDefined uri); + in + let new_coercions = + CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations + baseuri + in + let new_coercions = + List.filter (fun (s,t,u,_,obj,_,_) -> not(already_in_obj s t u obj)) + new_coercions + in + (* update the DB *) + let lemmas = + List.fold_left + (fun acc (src,tgt,uri,saturations,obj,arity,cpos) -> + CoercDb.add_coercion (src,tgt,uri,saturations,cpos); + let acc = add_obj uri obj pack_coercion_obj @ uri::acc in + acc) + [] new_coercions + in + CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos); +(* CoercDb.prefer uri; *) + lemmas +;; + + diff --git a/matita/components/library/librarySync.mli b/matita/components/library/librarySync.mli new file mode 100644 index 000000000..bfab37330 --- /dev/null +++ b/matita/components/library/librarySync.mli @@ -0,0 +1,59 @@ +(* 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