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
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
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 = \
+++ /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
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 =
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
[]
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
HExtlib.list_uniq l
with
exn -> raise exn (* no errors should be accepted *)
+ *)
;;
let close_uri_list cache_of_processed_baseuri uri_to_remove =
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
(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)))
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 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