From cd5e575ed60527edac0a99196bd8d20f06841254 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 8 Oct 2010 11:01:14 +0000 Subject: [PATCH] Library committed again (because of a bug in SVN) --- matita/components/library/.depend | 27 +- matita/components/library/.depend.opt | 27 +- matita/components/library/Makefile | 7 - matita/components/library/cicCoercion.ml | 40 -- matita/components/library/cicCoercion.mli | 40 -- matita/components/library/cicElim.ml | 461 --------------------- matita/components/library/cicElim.mli | 29 -- matita/components/library/cicFix.ml | 69 --- matita/components/library/cicFix.mli | 26 -- matita/components/library/cicRecord.ml | 135 ------ matita/components/library/cicRecord.mli | 26 -- matita/components/library/coercDb.ml | 175 -------- matita/components/library/coercDb.mli | 67 --- matita/components/library/libraryClean.ml | 57 +-- matita/components/library/libraryClean.mli | 1 - matita/components/library/libraryDb.ml | 212 ---------- matita/components/library/libraryDb.mli | 35 -- matita/components/library/librarySync.ml | 374 ----------------- matita/components/library/librarySync.mli | 59 --- 19 files changed, 20 insertions(+), 1847 deletions(-) delete mode 100644 matita/components/library/cicCoercion.ml delete mode 100644 matita/components/library/cicCoercion.mli delete mode 100644 matita/components/library/cicElim.ml delete mode 100644 matita/components/library/cicElim.mli delete mode 100644 matita/components/library/cicFix.ml delete mode 100644 matita/components/library/cicFix.mli delete mode 100644 matita/components/library/cicRecord.ml delete mode 100644 matita/components/library/cicRecord.mli delete mode 100644 matita/components/library/coercDb.ml delete mode 100644 matita/components/library/coercDb.mli delete mode 100644 matita/components/library/libraryDb.ml delete mode 100644 matita/components/library/libraryDb.mli delete mode 100644 matita/components/library/librarySync.ml delete mode 100644 matita/components/library/librarySync.mli diff --git a/matita/components/library/.depend b/matita/components/library/.depend index cfa1295ed..975c9e8da 100644 --- a/matita/components/library/.depend +++ b/matita/components/library/.depend @@ -1,32 +1,9 @@ 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 +libraryClean.cmo: libraryMisc.cmi libraryClean.cmi +libraryClean.cmx: libraryMisc.cmx libraryClean.cmi diff --git a/matita/components/library/.depend.opt b/matita/components/library/.depend.opt index cfa1295ed..975c9e8da 100644 --- a/matita/components/library/.depend.opt +++ b/matita/components/library/.depend.opt @@ -1,32 +1,9 @@ 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 +libraryClean.cmo: libraryMisc.cmi libraryClean.cmi +libraryClean.cmx: libraryMisc.cmx libraryClean.cmi diff --git a/matita/components/library/Makefile b/matita/components/library/Makefile index 5b9dc226f..715ee8f01 100644 --- a/matita/components/library/Makefile +++ b/matita/components/library/Makefile @@ -4,13 +4,6 @@ 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 = \ diff --git a/matita/components/library/cicCoercion.ml b/matita/components/library/cicCoercion.ml deleted file mode 100644 index b45599ceb..000000000 --- a/matita/components/library/cicCoercion.ml +++ /dev/null @@ -1,40 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -let close_coercion_graph_ref = ref - (fun _ _ _ _ _ -> [] : - CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> - string (* baseuri *) -> - (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj * - int * int) list) -;; - -let set_close_coercion_graph f = close_coercion_graph_ref := f;; - -let close_coercion_graph c1 c2 u sat s = - !close_coercion_graph_ref c1 c2 u sat s -;; diff --git a/matita/components/library/cicCoercion.mli b/matita/components/library/cicCoercion.mli deleted file mode 100644 index 8356de8cd..000000000 --- a/matita/components/library/cicCoercion.mli +++ /dev/null @@ -1,40 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* This module implements the Coercions transitive closure *) - -val set_close_coercion_graph : - (CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> - string (* baseuri *) -> - (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * - int (* saturations *) * Cic.obj * int (* arity *) * int (* cpos *)) list) - -> unit - -val close_coercion_graph: - CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> - string (* baseuri *) -> - (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * - int (* saturations *) * Cic.obj * int (* arity *) * int (* cpos *)) list - diff --git a/matita/components/library/cicElim.ml b/matita/components/library/cicElim.ml deleted file mode 100644 index 9f3bda423..000000000 --- a/matita/components/library/cicElim.ml +++ /dev/null @@ -1,461 +0,0 @@ -(* 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 deleted file mode 100644 index 70c1c2167..000000000 --- a/matita/components/library/cicElim.mli +++ /dev/null @@ -1,29 +0,0 @@ -(* 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 deleted file mode 100644 index 21cb99093..000000000 --- a/matita/components/library/cicFix.ml +++ /dev/null @@ -1,69 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* $Id: librarySync.ml 9482 2009-01-08 18:12:28Z tassi $ *) - -let generate_sibling_mutual_definitions ~add_obj ~add_coercion uri obj = - match obj with - | Cic.Constant (name_to_avoid,Some bo,_,_,attrs) when - List.mem (`Flavour `MutualDefinition) attrs -> - (match bo with - Cic.Fix (_,funs) -> - snd ( - List.fold_right - (fun (name,idx,ty,bo) (n,uris) -> - if name = name_to_avoid then - (n-1,uris) - else - let uri = - UriManager.uri_of_string - (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in - let bo = Cic.Fix (n-1,funs) in - let obj = Cic.Constant (name,Some bo,ty,[],attrs) in - let lemmas = add_obj uri obj in - (n-1,lemmas @ uri::uris)) - (List.tl funs) (List.length funs,[])) - | Cic.CoFix (_,funs) -> - snd ( - List.fold_right - (fun (name,ty,bo) (n,uris) -> - if name = name_to_avoid then - (n-1,uris) - else - let uri = - UriManager.uri_of_string - (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in - let bo = Cic.CoFix (n-1,funs) in - let obj = Cic.Constant (name,Some bo,ty,[],attrs) in - let lemmas = add_obj uri obj in - (n-1,lemmas @ uri::uris)) - (List.tl funs) (List.length funs,[])) - | _ -> assert false) - | _ -> [] -;; - - -let init () = - LibrarySync.add_object_declaration_hook generate_sibling_mutual_definitions;; diff --git a/matita/components/library/cicFix.mli b/matita/components/library/cicFix.mli deleted file mode 100644 index de361cc7c..000000000 --- a/matita/components/library/cicFix.mli +++ /dev/null @@ -1,26 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -val init : unit -> unit diff --git a/matita/components/library/cicRecord.ml b/matita/components/library/cicRecord.ml deleted file mode 100644 index e76ca9ca2..000000000 --- a/matita/components/library/cicRecord.ml +++ /dev/null @@ -1,135 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -let 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 deleted file mode 100644 index de361cc7c..000000000 --- a/matita/components/library/cicRecord.mli +++ /dev/null @@ -1,26 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -val init : unit -> unit diff --git a/matita/components/library/coercDb.ml b/matita/components/library/coercDb.ml deleted file mode 100644 index b7e390229..000000000 --- a/matita/components/library/coercDb.ml +++ /dev/null @@ -1,175 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -let debug = false -let debug_print = - if debug then fun x -> prerr_endline (Lazy.force x) - else ignore -;; - -type coerc_carr = - | Uri of UriManager.uri - | Sort of Cic.sort - | Fun of int - | Dead -;; - -type saturations = int -type coerced_pos = int -type coercion_entry = - coerc_carr * coerc_carr * UriManager.uri * saturations * coerced_pos - -type coerc_db = (* coercion_entry grouped by carrier with molteplicity *) - (coerc_carr * coerc_carr * - (UriManager.uri * int * saturations * coerced_pos) list) list - -let db = ref ([] : coerc_db) -let dump () = !db -let restore coerc_db = db := coerc_db -let empty_coerc_db = [] - -let rec coerc_carr_of_term t a = - try - match t, a with - | Cic.Sort s, 0 -> Sort s - | Cic.Appl (t::_), 0 -> coerc_carr_of_term t a - | t, 0 -> Uri (CicUtil.uri_of_term t) - | _, n -> Fun n - with Invalid_argument _ -> Dead -;; - -let string_of_carr = function - | Uri u -> UriManager.name_of_uri u - | Sort s -> CicPp.ppsort s - | Fun i -> "FunClass_" ^ string_of_int i - | Dead -> "UnsupportedCarrier" -;; - -let eq_carr ?(exact=false) src tgt = - match src, tgt with - | Uri src, Uri tgt -> - let coarse_eq = UriManager.eq src tgt in - let t = CicUtil.term_of_uri src in - let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in - (match ty, exact with - | Cic.Prod _, true -> false - | Cic.Prod _, false -> coarse_eq - | _ -> coarse_eq) - | Sort _, Sort _ -> true - | Fun _,Fun _ when not exact -> true (* only one Funclass *) - | Fun i,Fun j when i = j -> true (* only one Funclass *) - | _, _ -> false -;; - -let to_list db = - List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b,c -> a,b,c) l) db -;; - -let rec myfilter p = function - | [] -> [] - | (s,t,l)::tl -> - let l = - HExtlib.filter_map - (fun (u,n,saturations,cpos) as e -> - if p (s,t,u,saturations,cpos) then - if n = 1 then None - else Some (u,n-1,saturations,cpos) - else Some e) - l - in - if l = [] then myfilter p tl else (s,t,l)::myfilter p tl -;; - -let remove_coercion p = db := myfilter p !db;; - -let find_coercion f = - List.map - (fun (uri,_,saturations,_) -> uri,saturations) - (List.flatten - (HExtlib.filter_map (fun (s,t,l) -> if f (s,t) then Some l else None) !db)) -;; - -let is_a_coercion t = - try - let uri = CicUtil.uri_of_term t in - match - HExtlib.filter_map - (fun (src,tgt,xl) -> - let xl = List.filter (fun (x,_,_,_) -> UriManager.eq uri x) xl in - if xl = [] then None else Some (src,tgt,xl)) - !db - with - | [] -> None - | (_,_,[])::_ -> assert false - | [src,tgt,[u,_,s,p]] -> Some (src,tgt,u,s,p) - | (src,tgt,(u,_,s,p)::_)::_ -> - debug_print - (lazy "coercion has multiple entries, returning the first one"); - Some (src,tgt,u,s,p) - with Invalid_argument _ -> - debug_print (lazy "this term is not a constant"); - None -;; - -let add_coercion (src,tgt,u,saturations,cpos) = - let f s t = eq_carr s src && eq_carr t tgt in - let where = List.filter (fun (s,t,_) -> f s t) !db in - let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in - match where with - | [] -> db := (src,tgt,[u,1,saturations,cpos]) :: !db - | (src,tgt,l)::tl -> - assert (tl = []); (* not sure, this may be a feature *) - if List.exists (fun (x,_,_,_) -> UriManager.eq u x) l then - let l = - let l = - (* this code reorders the list so that adding an already declared - * coercion moves it to the begging of the list *) - let item = List.find (fun (x,_,_,_) -> UriManager.eq u x) l in - let rest=List.filter (fun (x,_,_,_) -> not (UriManager.eq u x)) l in - item :: rest - in - List.map - (fun (x,n,x_saturations,x_cpos) as e -> - if UriManager.eq u x then - (* not sure, this may be a feature *) - (assert (x_saturations = saturations && x_cpos = cpos); - (x,n+1,saturations,cpos)) - else e) - l - in - db := (src,tgt,l)::tl @ rest - else - db := (src,tgt,(u,1,saturations,cpos)::l)::tl @ rest -;; - -let prefer u = - let prefer (s,t,l) = - let lb,la = List.partition (fun (uri,_,_,_) -> UriManager.eq uri u) l in - s,t,lb@la - in - db := List.map prefer !db; -;; diff --git a/matita/components/library/coercDb.mli b/matita/components/library/coercDb.mli deleted file mode 100644 index 59c07f447..000000000 --- a/matita/components/library/coercDb.mli +++ /dev/null @@ -1,67 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - - -type coerc_carr = private - | Uri of UriManager.uri (* const, mutind, mutconstr *) - | Sort of Cic.sort (* Prop, Set, Type *) - | Fun of int - | Dead -;; - -val eq_carr: ?exact:bool -> coerc_carr -> coerc_carr -> bool -val string_of_carr: coerc_carr -> string - -(* takes a term in whnf ~delta:false and a desired ariety *) -val coerc_carr_of_term: Cic.term -> int -> coerc_carr - -type coerc_db -val empty_coerc_db : coerc_db -val dump: unit -> coerc_db -val restore: coerc_db -> unit - -val to_list: - coerc_db -> - (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list - -(* src carr, tgt carr, uri, saturations, coerced position - * invariant: - * if the constant pointed by uri has n argments - * n = coerced position + saturations + FunClass arity - *) - -type saturations = int -type coerced_pos = int -type coercion_entry = - coerc_carr * coerc_carr * UriManager.uri * saturations * coerced_pos -val add_coercion: coercion_entry -> unit -val remove_coercion: (coercion_entry -> bool) -> unit - -val find_coercion: - (coerc_carr * coerc_carr -> bool) -> (UriManager.uri * int) list - -val is_a_coercion: Cic.term -> coercion_entry option - -val prefer: UriManager.uri -> unit diff --git a/matita/components/library/libraryClean.ml b/matita/components/library/libraryClean.ml index 8e9f430ba..1f92b5868 100644 --- a/matita/components/library/libraryClean.ml +++ b/matita/components/library/libraryClean.ml @@ -37,6 +37,7 @@ 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 = @@ -46,6 +47,7 @@ let safe_buri_of_suri suri = UM.IllFormedUri _ -> suri let one_step_depend cache_of_processed_baseuri suri dbtype dbd = + assert false (* MATITA 1.0 let buri = safe_buri_of_suri suri in if Hashtbl.mem cache_of_processed_baseuri buri then [] @@ -90,8 +92,10 @@ let one_step_depend cache_of_processed_baseuri suri dbtype dbd = with exn -> raise exn (* no errors should be accepted *) end + *) let db_uris_of_baseuri buri = + [] (* MATITA 1.0 let dbd = LibraryDb.instance () in let dbtype = if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User @@ -122,6 +126,7 @@ let db_uris_of_baseuri buri = HExtlib.list_uniq l with exn -> raise exn (* no errors should be accepted *) + *) ;; let close_uri_list cache_of_processed_baseuri uri_to_remove = @@ -212,14 +217,14 @@ let moo_root_dir = lazy ( in String.sub url 7 (String.length url - 7)) ;; +*) + +let rec close_db cache_of_processed_baseuri uris next = + prerr_endline "CLOSE_DB "; uris (* MATITA 1.0 *) +;; 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 @@ -234,42 +239,12 @@ let clean_baseuris ?(verbose=true) buris = (fun baseuri -> !decompile ~baseuri; try - let obj_file = - LibraryMisc.obj_file_of_baseuri ~must_exist:false ~writable:true ~baseuri + let lexiconfile = + LibraryMisc.lexicon_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) + HExtlib.safe_remove lexiconfile; + HExtlib.rmdir_descend (Filename.chop_extension lexiconfile) 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 + (List.map (UriManager.buri_of_uri) l @ buris))) diff --git a/matita/components/library/libraryClean.mli b/matita/components/library/libraryClean.mli index 89f3b7b1d..f6999106a 100644 --- a/matita/components/library/libraryClean.mli +++ b/matita/components/library/libraryClean.mli @@ -25,5 +25,4 @@ val set_decompile_cb: (baseuri: string -> unit) -> unit -val db_uris_of_baseuri : string -> string list val clean_baseuris : ?verbose:bool -> string list -> unit diff --git a/matita/components/library/libraryDb.ml b/matita/components/library/libraryDb.ml deleted file mode 100644 index e82e91f97..000000000 --- a/matita/components/library/libraryDb.ml +++ /dev/null @@ -1,212 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -let dbtype_of_string dbtype = - if dbtype = "library" then HSql.Library - else if dbtype = "user" then HSql.User - else if dbtype = "legacy" then HSql.Legacy - else raise (HSql.Error "HSql: wrong config file format") - -let parse_dbd_conf _ = - let metadata = Helm_registry.get_list Helm_registry.string "db.metadata" in - List.map - (fun s -> - match Pcre.split ~pat:"\\s+" s with - | [path;db;user;pwd;dbtype] -> - let dbtype = dbtype_of_string dbtype in - let pwd = if pwd = "none" then None else Some pwd in - (* TODO parse port *) - path, None, db, user, pwd, dbtype - | _ -> raise (HSql.Error "HSql: Bad format in config file")) - metadata -;; - -let parse_dbd_conf _ = - HSql.mk_dbspec (parse_dbd_conf ()) -;; - -let instance = - let dbd = lazy ( - let dbconf = parse_dbd_conf () in - HSql.quick_connect dbconf) - in - fun () -> Lazy.force dbd -;; - -let xpointer_RE = Pcre.regexp "#.*$" -let file_scheme_RE = Pcre.regexp "^file://" - -let clean_owner_environment () = - 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 deleted file mode 100644 index e608a9c24..000000000 --- a/matita/components/library/libraryDb.mli +++ /dev/null @@ -1,35 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -val dbtype_of_string: string -> HSql.dbtype - -val instance: unit -> HSql.dbd -val parse_dbd_conf: unit -> HSql.dbspec - -val create_owner_environment: unit -> unit -val clean_owner_environment: unit -> unit - -val remove_uri: UriManager.uri -> unit -val xpointers_of_ind: UriManager.uri -> UriManager.uri list diff --git a/matita/components/library/librarySync.ml b/matita/components/library/librarySync.ml deleted file mode 100644 index 185ae5315..000000000 --- a/matita/components/library/librarySync.ml +++ /dev/null @@ -1,374 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -let object_declaration_hook = ref [] -let add_object_declaration_hook f = - object_declaration_hook := f :: !object_declaration_hook - -exception AlreadyDefined of UriManager.uri - -type coercion_decl = - UriManager.uri -> int (* arity *) -> - int (* saturations *) -> string (* baseuri *) -> - UriManager.uri list (* lemmas (new objs) *) - - -let stack = ref [];; - -let push () = - stack := CoercDb.dump () :: !stack; - CoercDb.restore CoercDb.empty_coerc_db; -;; - -let pop () = - match !stack with - | [] -> raise (Failure "Unable to POP from librarySync.ml") - | db :: tl -> - stack := tl; - CoercDb.restore db; -;; - -let uris_of_obj uri = - let innertypesuri = UriManager.innertypesuri_of_uri uri in - let bodyuri = UriManager.bodyuri_of_uri uri in - let univgraphuri = UriManager.univgraphuri_of_uri uri in - innertypesuri,bodyuri,univgraphuri - -let paths_and_uris_of_obj uri = - let resolved = Http_getter.filename' ~local:true ~writable:true uri in - let basepath = Filename.dirname resolved in - let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in - let innertypesfilename=(UriManager.nameext_of_uri innertypesuri)^".xml.gz"in - let innertypespath = basepath ^ "/" ^ innertypesfilename in - let xmlfilename = (UriManager.nameext_of_uri uri) ^ ".xml.gz" in - let xmlpath = basepath ^ "/" ^ xmlfilename in - let xmlbodyfilename = (UriManager.nameext_of_uri uri) ^ ".body.xml.gz" in - let xmlbodypath = basepath ^ "/" ^ xmlbodyfilename in - let xmlunivgraphfilename=(UriManager.nameext_of_uri univgraphuri)^".xml.gz"in - let xmlunivgraphpath = basepath ^ "/" ^ xmlunivgraphfilename in - xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, - xmlunivgraphpath, univgraphuri - -let save_object_to_disk uri obj ugraph univlist = - 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 deleted file mode 100644 index bfab37330..000000000 --- a/matita/components/library/librarySync.mli +++ /dev/null @@ -1,59 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -exception AlreadyDefined of UriManager.uri - -type coercion_decl = - UriManager.uri -> int (* arity *) -> - int (* saturations *) -> string (* baseuri *) -> - UriManager.uri list (* lemmas (new objs) *) - -(* the add_single_obj fun passed to the callback can raise AlreadyDefined *) -val add_object_declaration_hook : - (add_obj:(UriManager.uri -> Cic.obj -> UriManager.uri list) -> - add_coercion:coercion_decl -> - UriManager.uri -> Cic.obj -> UriManager.uri list) -> unit - -(* adds an object to the library together with all auxiliary lemmas on it *) -(* (e.g. elimination principles, projections, etc.) *) -(* it returns the list of the uris of the auxiliary lemmas generated *) -val add_obj: - UriManager.uri -> Cic.obj -> pack_coercion_obj:(Cic.obj -> Cic.obj) -> - UriManager.uri list - -(* removes an object (does not remove its associated lemmas) *) -val remove_obj: UriManager.uri -> unit - -(* Informs the library that [uri] is a coercion. *) -(* This can generate some composite coercions that, if [add_composites] *) -(* is true are added to the library. *) -(* The list of added objects is returned. *) -val add_coercion: - add_composites:bool -> pack_coercion_obj:(Cic.obj -> Cic.obj) -> coercion_decl - -(* these just push/pop the coercions database, since the library is not - * pushable/poppable *) -val push: unit -> unit -val pop: unit -> unit -- 2.39.2