--- /dev/null
+librarian.cmi:
+libraryMisc.cmi:
+libraryDb.cmi:
+coercDb.cmi:
+cicCoercion.cmi: coercDb.cmi
+librarySync.cmi:
+cicElim.cmi:
+cicRecord.cmi:
+cicFix.cmi:
+libraryClean.cmi:
+librarian.cmo: librarian.cmi
+librarian.cmx: librarian.cmi
+libraryMisc.cmo: libraryMisc.cmi
+libraryMisc.cmx: libraryMisc.cmi
+libraryDb.cmo: libraryDb.cmi
+libraryDb.cmx: libraryDb.cmi
+coercDb.cmo: coercDb.cmi
+coercDb.cmx: coercDb.cmi
+cicCoercion.cmo: coercDb.cmi cicCoercion.cmi
+cicCoercion.cmx: coercDb.cmx cicCoercion.cmi
+librarySync.cmo: libraryDb.cmi coercDb.cmi cicCoercion.cmi librarySync.cmi
+librarySync.cmx: libraryDb.cmx coercDb.cmx cicCoercion.cmx librarySync.cmi
+cicElim.cmo: librarySync.cmi cicElim.cmi
+cicElim.cmx: librarySync.cmx cicElim.cmi
+cicRecord.cmo: librarySync.cmi cicRecord.cmi
+cicRecord.cmx: librarySync.cmx cicRecord.cmi
+cicFix.cmo: librarySync.cmi cicFix.cmi
+cicFix.cmx: librarySync.cmx cicFix.cmi
+libraryClean.cmo: librarySync.cmi libraryMisc.cmi libraryDb.cmi \
+ libraryClean.cmi
+libraryClean.cmx: librarySync.cmx libraryMisc.cmx libraryDb.cmx \
+ libraryClean.cmi
--- /dev/null
+librarian.cmi:
+libraryMisc.cmi:
+libraryDb.cmi:
+coercDb.cmi:
+cicCoercion.cmi: coercDb.cmi
+librarySync.cmi:
+cicElim.cmi:
+cicRecord.cmi:
+cicFix.cmi:
+libraryClean.cmi:
+librarian.cmo: librarian.cmi
+librarian.cmx: librarian.cmi
+libraryMisc.cmo: libraryMisc.cmi
+libraryMisc.cmx: libraryMisc.cmi
+libraryDb.cmo: libraryDb.cmi
+libraryDb.cmx: libraryDb.cmi
+coercDb.cmo: coercDb.cmi
+coercDb.cmx: coercDb.cmi
+cicCoercion.cmo: coercDb.cmi cicCoercion.cmi
+cicCoercion.cmx: coercDb.cmx cicCoercion.cmi
+librarySync.cmo: libraryDb.cmi coercDb.cmi cicCoercion.cmi librarySync.cmi
+librarySync.cmx: libraryDb.cmx coercDb.cmx cicCoercion.cmx librarySync.cmi
+cicElim.cmo: librarySync.cmi cicElim.cmi
+cicElim.cmx: librarySync.cmx cicElim.cmi
+cicRecord.cmo: librarySync.cmi cicRecord.cmi
+cicRecord.cmx: librarySync.cmx cicRecord.cmi
+cicFix.cmo: librarySync.cmi cicFix.cmi
+cicFix.cmx: librarySync.cmx cicFix.cmi
+libraryClean.cmo: librarySync.cmi libraryMisc.cmi libraryDb.cmi \
+ libraryClean.cmi
+libraryClean.cmx: librarySync.cmx libraryMisc.cmx libraryDb.cmx \
+ libraryClean.cmi
--- /dev/null
+PACKAGE = library
+PREDICATES =
+
+INTERFACE_FILES = \
+ librarian.mli \
+ libraryMisc.mli \
+ libraryDb.mli \
+ coercDb.mli \
+ cicCoercion.mli \
+ librarySync.mli \
+ cicElim.mli \
+ cicRecord.mli \
+ cicFix.mli \
+ libraryClean.mli \
+ $(NULL)
+IMPLEMENTATION_FILES = \
+ $(INTERFACE_FILES:%.mli=%.ml)
+
+include ../../Makefile.defs
+include ../Makefile.common
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+let close_coercion_graph_ref = ref
+ (fun _ _ _ _ _ -> [] :
+ CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
+ string (* baseuri *) ->
+ (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj *
+ int * int) list)
+;;
+
+let set_close_coercion_graph f = close_coercion_graph_ref := f;;
+
+let close_coercion_graph c1 c2 u sat s =
+ !close_coercion_graph_ref c1 c2 u sat s
+;;
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* This module implements the Coercions transitive closure *)
+
+val set_close_coercion_graph :
+ (CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
+ string (* baseuri *) ->
+ (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri *
+ int (* saturations *) * Cic.obj * int (* arity *) * int (* cpos *)) list)
+ -> unit
+
+val close_coercion_graph:
+ CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
+ string (* baseuri *) ->
+ (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri *
+ int (* saturations *) * Cic.obj * int (* arity *) * int (* cpos *)) list
+
--- /dev/null
+(* Copyright (C) 2004, 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;;
--- /dev/null
+(* 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
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id: librarySync.ml 9482 2009-01-08 18:12:28Z tassi $ *)
+
+let generate_sibling_mutual_definitions ~add_obj ~add_coercion uri obj =
+ match obj with
+ | Cic.Constant (name_to_avoid,Some bo,_,_,attrs) when
+ List.mem (`Flavour `MutualDefinition) attrs ->
+ (match bo with
+ Cic.Fix (_,funs) ->
+ snd (
+ List.fold_right
+ (fun (name,idx,ty,bo) (n,uris) ->
+ if name = name_to_avoid then
+ (n-1,uris)
+ else
+ let uri =
+ UriManager.uri_of_string
+ (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
+ let bo = Cic.Fix (n-1,funs) in
+ let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+ let lemmas = add_obj uri obj in
+ (n-1,lemmas @ uri::uris))
+ (List.tl funs) (List.length funs,[]))
+ | Cic.CoFix (_,funs) ->
+ snd (
+ List.fold_right
+ (fun (name,ty,bo) (n,uris) ->
+ if name = name_to_avoid then
+ (n-1,uris)
+ else
+ let uri =
+ UriManager.uri_of_string
+ (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
+ let bo = Cic.CoFix (n-1,funs) in
+ let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+ let lemmas = add_obj uri obj in
+ (n-1,lemmas @ uri::uris))
+ (List.tl funs) (List.length funs,[]))
+ | _ -> assert false)
+ | _ -> []
+;;
+
+
+let init () =
+ LibrarySync.add_object_declaration_hook generate_sibling_mutual_definitions;;
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+val init : unit -> unit
--- /dev/null
+(* Copyright (C) 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;;
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+val init : unit -> unit
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+let debug = false
+let debug_print =
+ if debug then fun x -> prerr_endline (Lazy.force x)
+ else ignore
+;;
+
+type coerc_carr =
+ | Uri of UriManager.uri
+ | Sort of Cic.sort
+ | Fun of int
+ | Dead
+;;
+
+type saturations = int
+type coerced_pos = int
+type coercion_entry =
+ coerc_carr * coerc_carr * UriManager.uri * saturations * coerced_pos
+
+type coerc_db = (* coercion_entry grouped by carrier with molteplicity *)
+ (coerc_carr * coerc_carr *
+ (UriManager.uri * int * saturations * coerced_pos) list) list
+
+let db = ref ([] : coerc_db)
+let dump () = !db
+let restore coerc_db = db := coerc_db
+let empty_coerc_db = []
+
+let rec coerc_carr_of_term t a =
+ try
+ match t, a with
+ | Cic.Sort s, 0 -> Sort s
+ | Cic.Appl (t::_), 0 -> coerc_carr_of_term t a
+ | t, 0 -> Uri (CicUtil.uri_of_term t)
+ | _, n -> Fun n
+ with Invalid_argument _ -> Dead
+;;
+
+let string_of_carr = function
+ | Uri u -> UriManager.name_of_uri u
+ | Sort s -> CicPp.ppsort s
+ | Fun i -> "FunClass_" ^ string_of_int i
+ | Dead -> "UnsupportedCarrier"
+;;
+
+let eq_carr ?(exact=false) src tgt =
+ match src, tgt with
+ | Uri src, Uri tgt ->
+ let coarse_eq = UriManager.eq src tgt in
+ let t = CicUtil.term_of_uri src in
+ let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in
+ (match ty, exact with
+ | Cic.Prod _, true -> false
+ | Cic.Prod _, false -> coarse_eq
+ | _ -> coarse_eq)
+ | Sort _, Sort _ -> true
+ | Fun _,Fun _ when not exact -> true (* only one Funclass *)
+ | Fun i,Fun j when i = j -> true (* only one Funclass *)
+ | _, _ -> false
+;;
+
+let to_list db =
+ List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b,c -> a,b,c) l) db
+;;
+
+let rec myfilter p = function
+ | [] -> []
+ | (s,t,l)::tl ->
+ let l =
+ HExtlib.filter_map
+ (fun (u,n,saturations,cpos) as e ->
+ if p (s,t,u,saturations,cpos) then
+ if n = 1 then None
+ else Some (u,n-1,saturations,cpos)
+ else Some e)
+ l
+ in
+ if l = [] then myfilter p tl else (s,t,l)::myfilter p tl
+;;
+
+let remove_coercion p = db := myfilter p !db;;
+
+let find_coercion f =
+ List.map
+ (fun (uri,_,saturations,_) -> uri,saturations)
+ (List.flatten
+ (HExtlib.filter_map (fun (s,t,l) -> if f (s,t) then Some l else None) !db))
+;;
+
+let is_a_coercion t =
+ try
+ let uri = CicUtil.uri_of_term t in
+ match
+ HExtlib.filter_map
+ (fun (src,tgt,xl) ->
+ let xl = List.filter (fun (x,_,_,_) -> UriManager.eq uri x) xl in
+ if xl = [] then None else Some (src,tgt,xl))
+ !db
+ with
+ | [] -> None
+ | (_,_,[])::_ -> assert false
+ | [src,tgt,[u,_,s,p]] -> Some (src,tgt,u,s,p)
+ | (src,tgt,(u,_,s,p)::_)::_ ->
+ debug_print
+ (lazy "coercion has multiple entries, returning the first one");
+ Some (src,tgt,u,s,p)
+ with Invalid_argument _ ->
+ debug_print (lazy "this term is not a constant");
+ None
+;;
+
+let add_coercion (src,tgt,u,saturations,cpos) =
+ let f s t = eq_carr s src && eq_carr t tgt in
+ let where = List.filter (fun (s,t,_) -> f s t) !db in
+ let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in
+ match where with
+ | [] -> db := (src,tgt,[u,1,saturations,cpos]) :: !db
+ | (src,tgt,l)::tl ->
+ assert (tl = []); (* not sure, this may be a feature *)
+ if List.exists (fun (x,_,_,_) -> UriManager.eq u x) l then
+ let l =
+ let l =
+ (* this code reorders the list so that adding an already declared
+ * coercion moves it to the begging of the list *)
+ let item = List.find (fun (x,_,_,_) -> UriManager.eq u x) l in
+ let rest=List.filter (fun (x,_,_,_) -> not (UriManager.eq u x)) l in
+ item :: rest
+ in
+ List.map
+ (fun (x,n,x_saturations,x_cpos) as e ->
+ if UriManager.eq u x then
+ (* not sure, this may be a feature *)
+ (assert (x_saturations = saturations && x_cpos = cpos);
+ (x,n+1,saturations,cpos))
+ else e)
+ l
+ in
+ db := (src,tgt,l)::tl @ rest
+ else
+ db := (src,tgt,(u,1,saturations,cpos)::l)::tl @ rest
+;;
+
+let prefer u =
+ let prefer (s,t,l) =
+ let lb,la = List.partition (fun (uri,_,_,_) -> UriManager.eq uri u) l in
+ s,t,lb@la
+ in
+ db := List.map prefer !db;
+;;
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+
+type coerc_carr = private
+ | Uri of UriManager.uri (* const, mutind, mutconstr *)
+ | Sort of Cic.sort (* Prop, Set, Type *)
+ | Fun of int
+ | Dead
+;;
+
+val eq_carr: ?exact:bool -> coerc_carr -> coerc_carr -> bool
+val string_of_carr: coerc_carr -> string
+
+(* takes a term in whnf ~delta:false and a desired ariety *)
+val coerc_carr_of_term: Cic.term -> int -> coerc_carr
+
+type coerc_db
+val empty_coerc_db : coerc_db
+val dump: unit -> coerc_db
+val restore: coerc_db -> unit
+
+val to_list:
+ coerc_db ->
+ (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list
+
+(* src carr, tgt carr, uri, saturations, coerced position
+ * invariant:
+ * if the constant pointed by uri has n argments
+ * n = coerced position + saturations + FunClass arity
+ *)
+
+type saturations = int
+type coerced_pos = int
+type coercion_entry =
+ coerc_carr * coerc_carr * UriManager.uri * saturations * coerced_pos
+val add_coercion: coercion_entry -> unit
+val remove_coercion: (coercion_entry -> bool) -> unit
+
+val find_coercion:
+ (coerc_carr * coerc_carr -> bool) -> (UriManager.uri * int) list
+
+val is_a_coercion: Cic.term -> coercion_entry option
+
+val prefer: UriManager.uri -> unit
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+let debug = ref 0
+
+let time_stamp =
+ let old = ref 0.0 in
+ fun msg ->
+ if !debug > 0 then begin
+ let times = Unix.times () in
+ let stamp = times.Unix.tms_utime +. times.Unix.tms_stime in
+ let lap = stamp -. !old in
+ Printf.eprintf "TIME STAMP (%s): %f\n" msg lap; flush stderr;
+ old := stamp
+ end
+
+exception NoRootFor of string
+
+let absolutize path =
+ let path =
+ if String.length path > 0 && path.[0] <> '/' then
+ Sys.getcwd () ^ "/" ^ path
+ else
+ path
+ in
+ HExtlib.normalize_path path
+;;
+
+
+let find_root path =
+ let path = absolutize path in
+ let paths = List.rev (Str.split (Str.regexp "/") path) in
+ let rec build = function
+ | he::tl as l -> ("/" ^ String.concat "/" (List.rev l) ^ "/") :: build tl
+ | [] -> ["/"]
+ in
+ let paths = List.map HExtlib.normalize_path (build paths) in
+ try HExtlib.find_in paths "root"
+ with Failure "find_in" ->
+ raise (NoRootFor (path ^ " (" ^ String.concat ", " paths ^ ")"))
+;;
+
+let ensure_trailing_slash s =
+ if s = "" then "/" else
+ if s.[String.length s-1] <> '/' then s^"/" else s
+;;
+
+let remove_trailing_slash s =
+ if s = "" then "" else
+ let len = String.length s in
+ if s.[len-1] = '/' then String.sub s 0 (len-1) else s
+;;
+
+let load_root_file rootpath =
+ let data = HExtlib.input_file rootpath in
+ let lines = Str.split (Str.regexp "\n") data in
+ let clean s =
+ Pcre.replace ~pat:"[ \t]+" ~templ:" "
+ (Pcre.replace ~pat:"^ *" (Pcre.replace ~pat:" *$" s))
+ in
+ List.map
+ (fun l ->
+ match Str.split (Str.regexp "=") l with
+ | [k;v] -> clean k, Http_getter_misc.strip_trailing_slash (clean v)
+ | _ -> raise (Failure ("Malformed root file: " ^ rootpath)))
+ lines
+;;
+
+let find_root_for ~include_paths file =
+ let include_paths = "" :: Sys.getcwd () :: include_paths in
+ let rec find_path_for file =
+ try HExtlib.find_in include_paths file
+ with Failure "find_in" ->
+ if Filename.check_suffix file ".ma" then begin
+ let mma = Filename.chop_suffix file ".ma" ^ ".mma" in
+ HLog.warn ("We look for: " ^ mma);
+ let path = find_path_for mma in
+ Filename.chop_suffix path ".mma" ^ ".ma"
+ end else begin
+ HLog.error ("We are in: " ^ Sys.getcwd ());
+ HLog.error ("Unable to find: "^file^"\nPaths explored:");
+ List.iter (fun x -> HLog.error (" - "^x)) include_paths;
+ raise (NoRootFor file)
+ end
+ in
+ let path = find_path_for file in
+ let path = absolutize path in
+(* HLog.debug ("file "^file^" resolved as "^path); *)
+ let rootpath, root, buri =
+ try
+ let mburi = Helm_registry.get "matita.baseuri" in
+ match Str.split (Str.regexp " ") mburi with
+ | [root; buri] when HExtlib.is_prefix_of root path ->
+ ":registry:", root, buri
+ | _ -> raise (Helm_registry.Key_not_found "matita.baseuri")
+ with Helm_registry.Key_not_found "matita.baseuri" ->
+ let rootpath = find_root path in
+ let buri = List.assoc "baseuri" (load_root_file rootpath) in
+ rootpath, Filename.dirname rootpath, buri
+ in
+(* HLog.debug ("file "^file^" rooted by "^rootpath^""); *)
+ let uri = Http_getter_misc.strip_trailing_slash buri in
+ if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then
+ HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri);
+ ensure_trailing_slash root, remove_trailing_slash uri, path
+
+;;
+
+let mk_baseuri root extra =
+ let chop name =
+ assert(Filename.check_suffix name ".ma" ||
+ Filename.check_suffix name ".mma");
+ try Filename.chop_extension name
+ with Invalid_argument "Filename.chop_extension" -> name
+ in
+ remove_trailing_slash (HExtlib.normalize_path (root ^ "/" ^ chop extra))
+;;
+
+let baseuri_of_script ~include_paths file =
+ let root, buri, path = find_root_for ~include_paths file in
+ let path = HExtlib.normalize_path path in
+ let root = HExtlib.normalize_path root in
+ let lpath = Str.split (Str.regexp "/") path in
+ let lroot = Str.split (Str.regexp "/") root in
+ let rec substract l1 l2 =
+ match l1, l2 with
+ | h1::tl1,h2::tl2 when h1 = h2 -> substract tl1 tl2
+ | l,[] -> l
+ | _ -> raise (NoRootFor (file ^" "^path^" "^root))
+ in
+ let extra_buri = substract lpath lroot in
+ let extra = String.concat "/" extra_buri in
+ root,
+ mk_baseuri buri extra,
+ path,
+ extra
+;;
+
+let find_roots_in_dir dir =
+ HExtlib.find ~test:(fun f ->
+ Filename.basename f = "root" &&
+ try (Unix.stat f).Unix.st_kind = Unix.S_REG
+ with Unix.Unix_error _ -> false)
+ dir
+;;
+
+(* make *)
+let load_deps_file f =
+ let deps = ref [] in
+ let ic = open_in f in
+ try
+ while true do
+ begin
+ let l = input_line ic in
+ match Str.split (Str.regexp " ") l with
+ | [] ->
+ HLog.error ("Malformed deps file: " ^ f);
+ raise (Failure ("Malformed deps file: " ^ f))
+ | he::tl -> deps := (he,tl) :: !deps
+ end
+ done; !deps
+ with End_of_file -> !deps
+;;
+
+type options = (string * string) list
+
+module type Format =
+ sig
+ type source_object
+ type target_object
+ val load_deps_file: string -> (source_object * source_object list) list
+ val string_of_source_object: source_object -> string
+ val string_of_target_object: target_object -> string
+ val build: options -> source_object -> bool
+ val root_and_target_of:
+ options -> source_object ->
+ (* root, relative source, writeable target, read only target *)
+ string option * source_object * target_object * target_object
+ val mtime_of_source_object: source_object -> float option
+ val mtime_of_target_object: target_object -> float option
+ val is_readonly_buri_of: options -> source_object -> bool
+ end
+
+module Make = functor (F:Format) -> struct
+
+ type status = Done of bool
+ | Ready of bool
+
+ let say s = if !debug > 0 then prerr_endline ("make: "^s);;
+
+ let unopt_or_call x f y = match x with Some _ -> x | None -> f y;;
+
+ let fst4 = function (x,_,_,_) -> x;;
+
+ let modified_before_s_t (_,cs, ct, _, _) a b =
+
+ if !debug > 1 then time_stamp ("L s_t: a " ^ F.string_of_source_object a);
+ if !debug > 1 then time_stamp ("L s_t: b " ^ F.string_of_target_object b);
+
+ let a = try Hashtbl.find cs a with Not_found -> assert false in
+ let b =
+ try
+ match Hashtbl.find ct b with
+ | Some _ as x -> x
+ | None ->
+ match F.mtime_of_target_object b with
+ | Some t as x ->
+ Hashtbl.remove ct b;
+ Hashtbl.add ct b x; x
+ | x -> x
+ with Not_found -> assert false
+ in
+ let r = match a, b with
+ | Some a, Some b -> a <= b
+ | _ -> false
+ in
+
+ if !debug > 1 then time_stamp ("L s_t: " ^ string_of_bool r);
+
+ r
+
+ let modified_before_t_t (_,_,ct, _, _) a b =
+
+ if !debug > 1 then time_stamp ("L t_t: a " ^ F.string_of_target_object a);
+ if !debug > 1 then time_stamp ("L t_t: b " ^ F.string_of_target_object b);
+
+ let a =
+ try
+ match Hashtbl.find ct a with
+ | Some _ as x -> x
+ | None ->
+ match F.mtime_of_target_object a with
+ | Some t as x ->
+ Hashtbl.remove ct a;
+ Hashtbl.add ct a x; x
+ | x -> x
+ with Not_found -> assert false
+ in
+ let b =
+ try
+ match Hashtbl.find ct b with
+ | Some _ as x -> x
+ | None ->
+ match F.mtime_of_target_object b with
+ | Some t as x ->
+ Hashtbl.remove ct b;
+ Hashtbl.add ct b x; x
+ | x -> x
+ with Not_found -> assert false
+ in
+ let r = match a, b with
+ | Some a, Some b ->
+
+ if !debug > 1 then time_stamp ("tt: a " ^ string_of_float a);
+ if !debug > 1 then time_stamp ("tt: b " ^ string_of_float b);
+
+ a <= b
+ | _ -> false
+ in
+
+ if !debug > 1 then time_stamp ("L t_t: " ^ string_of_bool r);
+
+ r
+
+ let rec purge_unwanted_roots wanted deps =
+ let roots, rest =
+ List.partition
+ (fun (t,_,d,_,_) ->
+ not (List.exists (fun (_,_,d1,_,_) -> List.mem t d1) deps))
+ deps
+ in
+ let newroots = List.filter (fun (t,_,_,_,_) -> List.mem t wanted) roots in
+ if newroots = roots then
+ deps
+ else
+ purge_unwanted_roots wanted (newroots @ rest)
+ ;;
+
+ let is_not_ro (opts,_,_,_,_) (f,_,_,r,_) =
+ match r with
+ | Some root -> not (F.is_readonly_buri_of opts f)
+ | None -> assert false
+ ;;
+
+(* FG: new sorting algorithm ************************************************)
+
+ let rec make_aux root opts ok deps =
+ List.fold_left (make_one root opts) ok deps
+
+ and make_one root opts ok what =
+ let lo, _, ct, cc, cd = opts in
+ let t, path, deps, froot, tgt = what in
+ let str = F.string_of_source_object t in
+ let map (okd, okt) d =
+ let (_, _, _, _, tgtd) as whatd = (Hashtbl.find cd d) in
+ let r = make_one root opts okd whatd in
+ r, okt && modified_before_t_t opts tgtd tgt
+ in
+ time_stamp ("L : processing " ^ str);
+ try
+ let r = Hashtbl.find cc t in
+ time_stamp ("L : " ^ string_of_bool r ^ " " ^ str);
+ ok && r
+(* say "already built" *)
+ with Not_found ->
+ let okd, okt = List.fold_left map (true, modified_before_s_t opts t tgt) deps in
+ let res =
+ if okd then
+ if okt then true else
+ let build path = match froot with
+ | Some froot when froot = root ->
+ if is_not_ro opts what then F.build lo path else
+ (HLog.error ("Read only baseuri for: " ^ str ^
+ ", I won't compile it even if it is out of date");
+ false)
+ | Some froot -> make froot [path]
+ | None -> HLog.error ("No root for: " ^ str); false
+ in
+ Hashtbl.remove ct tgt;
+ Hashtbl.add ct tgt None;
+ time_stamp ("L : BUILDING " ^ str);
+ let res = build path in
+ time_stamp ("L : DONE " ^ str); res
+ else false
+ in
+ time_stamp ("L : " ^ string_of_bool res ^ " " ^ str);
+ Hashtbl.add cc t res; ok && res
+
+(****************************************************************************)
+
+ and make root targets =
+ time_stamp "L : ENTERING";
+ HLog.debug ("Entering directory '"^root^"'");
+ let old_root = Sys.getcwd () in
+ Sys.chdir root;
+ let deps = F.load_deps_file (root^"/depends") in
+ let local_options = load_root_file (root^"/root") in
+ let baseuri = List.assoc "baseuri" local_options in
+ print_endline ("Entering HELM directory: " ^ baseuri); flush stdout;
+ let caches,cachet,cachec,cached =
+ Hashtbl.create 73, Hashtbl.create 73, Hashtbl.create 73, Hashtbl.create 73
+ in
+ (* deps are enriched with these informations to sped up things later *)
+ let deps =
+ List.map
+ (fun (file,d) ->
+ let r,path,wtgt,rotgt = F.root_and_target_of local_options file in
+ Hashtbl.add caches file (F.mtime_of_source_object file);
+ (* if a read only target exists, we use that one, otherwise
+ we use the writeable one that may be compiled *)
+ let _,_,_,_, tgt as tuple =
+ match F.mtime_of_target_object rotgt with
+ | Some _ as mtime ->
+ Hashtbl.add cachet rotgt mtime;
+ (file, path, d, r, rotgt)
+ | None ->
+ Hashtbl.add cachet wtgt (F.mtime_of_target_object wtgt);
+ (file, path, d, r, wtgt)
+ in
+ Hashtbl.add cached file tuple;
+ tuple
+ )
+ deps
+ in
+ let opts = local_options, caches, cachet, cachec, cached in
+ let ok =
+ if targets = [] then
+ make_aux root opts true deps
+ else
+ make_aux root opts true (purge_unwanted_roots targets deps)
+ in
+ print_endline ("Leaving HELM directory: " ^ baseuri); flush stdout;
+ HLog.debug ("Leaving directory '"^root^"'");
+ Sys.chdir old_root;
+ time_stamp "L : LEAVING";
+ ok
+ ;;
+
+end
+
+let write_deps_file where deps = match where with
+ | Some root ->
+ let oc = open_out (root ^ "/depends") in
+ let map (t, d) = output_string oc (t^" "^String.concat " " d^"\n") in
+ List.iter map deps; close_out oc;
+ HLog.message ("Generated: " ^ root ^ "/depends")
+ | None ->
+ print_endline (String.concat " " (List.flatten (List.map snd deps)))
+
+(* FG ***********************************************************************)
+
+(* scheme uri part as defined in URI Generic Syntax (RFC 3986) *)
+let uri_scheme_rex = Pcre.regexp "^[[:alpha:]][[:alnum:]\-+.]*:"
+
+let is_uri str =
+ Pcre.pmatch ~rex:uri_scheme_rex str
--- /dev/null
+(* Copyright (C) 2004-2008, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+exception NoRootFor of string
+
+(* make a relative path absolute *)
+val absolutize: string -> string
+
+(* a root file is a text, line oriented, file containing pairs separated by
+ * the '=' character. Example:
+ *
+ * baseuri = cic:/foo/bar
+ * include_paths = ../baz ../../pippo
+ *
+ * spaces at the end/begin of the line and around '=' are ignored,
+ * multiple spaces in the middle of an item are shrinked to one.
+ *)
+val load_root_file: string -> (string*string) list
+
+(* baseuri_of_script ?(inc:REG[matita.includes]) fname
+ * ->
+ * root, buri, fullpath, rootrelativepath
+ * sample: baseuri_of_script a.ma -> /home/pippo/devel/, cic:/matita/a,
+ * /home/pippo/devel/a.ma, a.ma *)
+val baseuri_of_script:
+ include_paths:string list -> string -> string * string * string * string
+
+(* given a baseuri and a file name (relative to its root)
+ * returns a baseuri:
+ * mk_baseuri "cic:/matita" "nat/plus.ma" -> "cic:/matita/nat/plus"
+ *)
+val mk_baseuri: string -> string -> string
+
+(* finds all the roots files in the specified dir, roots are
+ * text files, readable by the user named 'root'
+ *)
+val find_roots_in_dir: string -> string list
+
+(* make implementation *)
+type options = (string * string) list
+
+module type Format =
+ sig
+ type source_object
+ type target_object
+ val load_deps_file: string -> (source_object * source_object list) list
+ val string_of_source_object: source_object -> string
+ val string_of_target_object: target_object -> string
+ val build: options -> source_object -> bool
+ val root_and_target_of:
+ options -> source_object ->
+ (* root, relative source, writeable target, read only target *)
+ string option * source_object * target_object * target_object
+ val mtime_of_source_object: source_object -> float option
+ val mtime_of_target_object: target_object -> float option
+ val is_readonly_buri_of: options -> source_object -> bool
+ end
+
+module Make :
+ functor (F : Format) ->
+ sig
+ (* make [root dir] [targets], targets = [] means make all *)
+ val make : string -> F.source_object list -> bool
+ end
+
+(* deps are made with scripts names, for example lines like
+ *
+ * nat/plus.ma nat/nat.ma logic/equality.ma
+ *
+ * state that plus.ma needs nat and equality
+ *)
+val load_deps_file: string -> (string * string list) list
+val write_deps_file: string option -> (string * string list) list -> unit
+
+(* FG ***********************************************************************)
+
+(* true if the argunent starts with a uri scheme prefix *)
+val is_uri: string -> bool
+
+(* Valid values: 0: no debug; 1: normal debug; > 1: extra debug *)
+val debug: int ref
+
+val time_stamp: string -> unit
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+open Printf
+
+let debug = false
+let debug_prerr = if debug then prerr_endline else ignore
+
+module HGT = Http_getter_types;;
+module HG = Http_getter;;
+module UM = UriManager;;
+
+let decompile = ref (fun ~baseuri -> assert false);;
+let set_decompile_cb f = decompile := f;;
+
+let strip_xpointer s = Pcre.replace ~pat:"#.*$" s ;;
+
+let safe_buri_of_suri suri =
+ try
+ UM.buri_of_uri (UM.uri_of_string suri)
+ with
+ UM.IllFormedUri _ -> suri
+
+let one_step_depend cache_of_processed_baseuri suri dbtype dbd =
+ 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
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+val set_decompile_cb: (baseuri: string -> unit) -> unit
+
+val db_uris_of_baseuri : string -> string list
+val clean_baseuris : ?verbose:bool -> string list -> unit
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+let dbtype_of_string dbtype =
+ if dbtype = "library" then HSql.Library
+ else if dbtype = "user" then HSql.User
+ else if dbtype = "legacy" then HSql.Legacy
+ else raise (HSql.Error "HSql: wrong config file format")
+
+let parse_dbd_conf _ =
+ let metadata = Helm_registry.get_list Helm_registry.string "db.metadata" in
+ List.map
+ (fun s ->
+ match Pcre.split ~pat:"\\s+" s with
+ | [path;db;user;pwd;dbtype] ->
+ let dbtype = dbtype_of_string dbtype in
+ let pwd = if pwd = "none" then None else Some pwd in
+ (* TODO parse port *)
+ path, None, db, user, pwd, dbtype
+ | _ -> raise (HSql.Error "HSql: Bad format in config file"))
+ metadata
+;;
+
+let parse_dbd_conf _ =
+ HSql.mk_dbspec (parse_dbd_conf ())
+;;
+
+let instance =
+ let dbd = lazy (
+ let dbconf = parse_dbd_conf () in
+ HSql.quick_connect dbconf)
+ in
+ fun () -> Lazy.force dbd
+;;
+
+let xpointer_RE = Pcre.regexp "#.*$"
+let file_scheme_RE = Pcre.regexp "^file://"
+
+let clean_owner_environment () =
+ 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
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+val dbtype_of_string: string -> HSql.dbtype
+
+val instance: unit -> HSql.dbd
+val parse_dbd_conf: unit -> HSql.dbspec
+
+val create_owner_environment: unit -> unit
+val clean_owner_environment: unit -> unit
+
+val remove_uri: UriManager.uri -> unit
+val xpointers_of_ind: UriManager.uri -> UriManager.uri list
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+let resolve ~must_exist ~writable ~local baseuri =
+ if must_exist then
+ Http_getter.resolve ~local ~writable baseuri
+ else
+ Http_getter.filename ~local ~writable baseuri
+
+let obj_file_of_baseuri ~must_exist ~writable ~baseuri =
+ resolve ~must_exist ~writable ~local:true baseuri ^ ".moo"
+let lexicon_file_of_baseuri ~must_exist ~writable ~baseuri =
+ resolve ~must_exist ~writable ~local:true baseuri ^ ".lexicon"
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* only for local uris *)
+val obj_file_of_baseuri:
+ must_exist:bool -> writable:bool -> baseuri:string -> string
+val lexicon_file_of_baseuri:
+ must_exist:bool -> writable:bool -> baseuri:string -> string
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+let object_declaration_hook = ref []
+let add_object_declaration_hook f =
+ object_declaration_hook := f :: !object_declaration_hook
+
+exception AlreadyDefined of UriManager.uri
+
+type coercion_decl =
+ UriManager.uri -> int (* arity *) ->
+ int (* saturations *) -> string (* baseuri *) ->
+ UriManager.uri list (* lemmas (new objs) *)
+
+
+let stack = ref [];;
+
+let push () =
+ stack := CoercDb.dump () :: !stack;
+ CoercDb.restore CoercDb.empty_coerc_db;
+;;
+
+let pop () =
+ match !stack with
+ | [] -> raise (Failure "Unable to POP from librarySync.ml")
+ | db :: tl ->
+ stack := tl;
+ CoercDb.restore db;
+;;
+
+let uris_of_obj uri =
+ let innertypesuri = UriManager.innertypesuri_of_uri uri in
+ let bodyuri = UriManager.bodyuri_of_uri uri in
+ let univgraphuri = UriManager.univgraphuri_of_uri uri in
+ innertypesuri,bodyuri,univgraphuri
+
+let paths_and_uris_of_obj uri =
+ let resolved = Http_getter.filename' ~local:true ~writable:true uri in
+ let basepath = Filename.dirname resolved in
+ let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
+ let innertypesfilename=(UriManager.nameext_of_uri innertypesuri)^".xml.gz"in
+ let innertypespath = basepath ^ "/" ^ innertypesfilename in
+ let xmlfilename = (UriManager.nameext_of_uri uri) ^ ".xml.gz" in
+ let xmlpath = basepath ^ "/" ^ xmlfilename in
+ let xmlbodyfilename = (UriManager.nameext_of_uri uri) ^ ".body.xml.gz" in
+ let xmlbodypath = basepath ^ "/" ^ xmlbodyfilename in
+ let xmlunivgraphfilename=(UriManager.nameext_of_uri univgraphuri)^".xml.gz"in
+ let xmlunivgraphpath = basepath ^ "/" ^ xmlunivgraphfilename in
+ xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
+ xmlunivgraphpath, univgraphuri
+
+let save_object_to_disk uri obj ugraph univlist =
+ 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
+;;
+
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+exception AlreadyDefined of UriManager.uri
+
+type coercion_decl =
+ UriManager.uri -> int (* arity *) ->
+ int (* saturations *) -> string (* baseuri *) ->
+ UriManager.uri list (* lemmas (new objs) *)
+
+(* the add_single_obj fun passed to the callback can raise AlreadyDefined *)
+val add_object_declaration_hook :
+ (add_obj:(UriManager.uri -> Cic.obj -> UriManager.uri list) ->
+ add_coercion:coercion_decl ->
+ UriManager.uri -> Cic.obj -> UriManager.uri list) -> unit
+
+(* adds an object to the library together with all auxiliary lemmas on it *)
+(* (e.g. elimination principles, projections, etc.) *)
+(* it returns the list of the uris of the auxiliary lemmas generated *)
+val add_obj:
+ UriManager.uri -> Cic.obj -> pack_coercion_obj:(Cic.obj -> Cic.obj) ->
+ UriManager.uri list
+
+(* removes an object (does not remove its associated lemmas) *)
+val remove_obj: UriManager.uri -> unit
+
+(* Informs the library that [uri] is a coercion. *)
+(* This can generate some composite coercions that, if [add_composites] *)
+(* is true are added to the library. *)
+(* The list of added objects is returned. *)
+val add_coercion:
+ add_composites:bool -> pack_coercion_obj:(Cic.obj -> Cic.obj) -> coercion_decl
+
+(* these just push/pop the coercions database, since the library is not
+ * pushable/poppable *)
+val push: unit -> unit
+val pop: unit -> unit
projects / helm.git / commitdiff