(* $Id$ *)
+let object_declaration_hook = ref []
+let add_object_declaration_hook f =
+ object_declaration_hook := f :: !object_declaration_hook
+
exception AlreadyDefined of UriManager.uri
-let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29
+type coercion_decl =
+ UriManager.uri -> int (* arity *) ->
+ int (* saturations *) -> string (* baseuri *) ->
+ UriManager.uri list (* lemmas (new objs) *)
-(* uri |--> (derived_coercions_in_the_coercion_DB, derived_coercions_in_lib)
- *
- * in case of remove_coercion uri, the first component is removed from the
- * coercion DB, while the second is passed to remove_obj (and is not [] only if
- * add_coercion is called with add_composites
- * *)
-let coercion_hashtbl = UriManager.UriHashtbl.create 3
+
+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
innertypesuri,bodyuri,univgraphuri
let paths_and_uris_of_obj uri =
- let resolved = Http_getter.filename' ~writable:true uri in
+ 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
HExtlib.mkdir dir
in
(* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
- let annobj = Cic2acic.plain_acic_object_of_cic_object obj in
+ 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:None ~ask_dtd_to_the_getter:false annobj
- in
+ 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
(* 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,_ -> []
fun ~dbd ~uri ->
profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
-let add_single_obj uri obj refinement_toolkit =
- let module RT = RefinementTool in
+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 (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
- not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
- then
- refinement_toolkit.RT.pack_coercion_obj obj
- else
- 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)
- else begin
- (*CicUniv.reset_spent_time ();
- let before = Unix.gettimeofday () in*)
+ if CicEnvironment.in_library uri then raise (AlreadyDefined uri);
+ begin (* ATOMIC *)
typecheck_obj uri obj; (* 1 *)
- (*let after = Unix.gettimeofday () in
- let univ_time = CicUniv.get_spent_time () in
- let total_time = after -. before in
- prerr_endline
- (Printf.sprintf "QED: %%univ = %2.5f, total = %2.5f, univ = %2.5f, %s\n"
- (univ_time *. 100. /. total_time) (total_time) (univ_time)
- (UriManager.name_of_uri uri));*)
- let _, ugraph, univlist =
- CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in
+ 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
raise exc
with exc ->
CicEnvironment.remove_obj uri; (* -1 *)
- raise exc
- end
-
-let remove_single_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' ~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);
- (*CoercGraph.remove_coercion uri;*)
- CicEnvironment.remove_obj uri
- ) uris_to_remove
-
-(*** GENERATION OF AUXILIARY LEMMAS ***)
-
-let generate_elimination_principles uri refinement_toolkit =
- let uris = ref [] in
- let elim i =
- let elim sort =
- try
- let uri,obj = CicElim.elim_of ~sort uri i in
- add_single_obj uri obj refinement_toolkit;
- uris := uri :: !uris
- with CicElim.Can_t_eliminate -> ()
- in
- try
- List.iter
- elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
- with exn ->
- List.iter remove_single_obj !uris;
- raise exn
- in
- let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
- match obj with
- | Cic.InductiveDefinition (indTypes, _, _, _) ->
- let counter = ref 0 in
- List.iter (fun _ -> elim !counter; counter := !counter+1) indTypes;
- !uris
- | _ ->
- failwith (Printf.sprintf "not an inductive definition (%s)"
- (UriManager.string_of_uri uri))
-
-(* COERCIONS ***********************************************************)
-
-let remove_all_coercions () =
- UriManager.UriHashtbl.clear coercion_hashtbl;
- CoercDb.remove_coercion (fun (_,_,u1) -> true)
+ 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 *)
-let add_coercion ~add_composites refinement_toolkit uri arity =
+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.empty_ugraph
+ 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
* should we saturate it with metas in case we insert it?
*
*)
- let spline2list ty =
+ 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 =
- let list_remove_from_tail n l =
- let rec aux n = function
- | hd::tl when n > 0 -> aux (n-1) tl
- | l when n = 0 -> l
- | _ -> assert false
+ 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 n (List.rev l)
+ aux (arity,saturations,None,List.rev l)
in
- let types = spline2list coer_ty in
- match arity, list_remove_from_tail arity types with
- | 0,tgt::src::_ ->
- (* if ~delta is true, it is impossible to define an identity coercion *)
- CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
- CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
- | n,_::src::_ ->
- CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
- CoercDb.Fun arity
- | _ -> assert false
+ 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 =
+ 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 ->
- UriManager.eq u uri &&
- CoercDb.eq_carr s src_carr &&
- CoercDb.eq_carr t tgt_carr)
+ (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.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);[])
+ (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 =
- CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri
+ List.filter (fun (s,t,u,_,obj,_,_) -> not(already_in_obj s t u obj))
+ new_coercions
in
- let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
- if already_in then
- (* this if starts here just to be sure the closure function works fine *)
- begin
- assert (new_coercions = []);
- HLog.warn
- (UriManager.string_of_uri uri ^
- " is already declared as a coercion! skipping...");
- []
- end
- else
- begin
- (* update the DB *)
- List.iter
- (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri))
- new_coercions;
- CoercDb.add_coercion (src_carr, tgt_carr, uri);
- (* add the composites obj and they eventual lemmas *)
- let lemmas =
- if add_composites then
- List.fold_left
- (fun acc (_,_,uri,obj) ->
- add_single_obj uri obj refinement_toolkit;
- uri::acc)
- [] new_coercions
- else
- []
- in
- (* store that composite_uris are related to uri. the first component is
- * the stuff in the DB while the second is stuff for remove_obj *)
- (*
- prerr_endline ("adding: " ^
- string_of_bool add_composites ^ UriManager.string_of_uri uri);
- List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
- composite_uris;
- *)
- UriManager.UriHashtbl.add coercion_hashtbl uri
- (composite_uris,if add_composites then composite_uris else []);
- (*
- prerr_endline ("lemmas:");
- List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
- lemmas;
- prerr_endline ("lemmas END");*)
- lemmas
- end
+ (* 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
;;
-let remove_coercion uri =
- try
- let (composites_in_db, composites_in_lib) =
- UriManager.UriHashtbl.find coercion_hashtbl uri
- in
- (*prerr_endline ("removing: " ^UriManager.string_of_uri uri);
- List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
- composites_in_db;*)
- UriManager.UriHashtbl.remove coercion_hashtbl uri;
- CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u);
- (* remove from the DB *)
- List.iter
- (fun u -> CoercDb.remove_coercion (fun (_,_,u1) -> UriManager.eq u u1))
- composites_in_db;
- (* remove composites from the lib *)
- List.iter remove_single_obj composites_in_lib
- with
- Not_found -> () (* mhh..... *)
-
-let generate_projections refinement_toolkit uri fields =
- let uris = ref [] in
- let projections =
- CicRecord.projections_of uri
- (List.map (fun (x,_,_) -> x) fields)
- in
- try
- List.iter2
- (fun (uri, name, bo) (_name, coercion, arity) ->
- try
- let ty, ugraph =
- CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
- let attrs = [`Class `Projection; `Generated] in
- let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
- add_single_obj uri obj refinement_toolkit;
- let composites =
- if coercion then
- begin
-(*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
- let x =
- add_coercion ~add_composites:true refinement_toolkit uri arity
- in
-(*prerr_endline ("are: ");
- List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
- prerr_endline "---";
-*)
- x
- end
- else
- []
- in
- uris := uri :: composites @ !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
- with exn ->
- List.iter remove_single_obj !uris;
- raise exn
-
-let build_inversion_principle = ref (fun a b -> assert false);;
-
-let generate_inversion refinement_toolkit uri obj =
- List.map
- (fun (ind_uri,ind_obj) ->
- add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri)
- (!build_inversion_principle uri obj)
-
-let add_obj refinement_toolkit uri obj =
- add_single_obj uri obj refinement_toolkit;
- let uris = ref [] in
- try
- begin
- match obj with
- | Cic.Constant _ -> ()
- | Cic.InductiveDefinition (_,_,_,attrs) ->
- uris := !uris @
- generate_elimination_principles uri refinement_toolkit;
- uris := !uris @ generate_inversion refinement_toolkit uri obj;
- 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 -> () (* not a record *)
- | Some fields ->
- uris := !uris @
- (generate_projections refinement_toolkit uri fields))
- | Cic.CurrentProof _
- | Cic.Variable _ -> assert false
- end;
- UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris;
- !uris
- with exn ->
- List.iter remove_single_obj !uris;
- raise exn
-
-let remove_obj uri =
- let uris =
- try
- let res = UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri in
- UriManager.UriHashtbl.remove auxiliary_lemmas_hashtbl uri;
- res
- with
- Not_found -> [] (*assert false*)
- in
- List.iter remove_single_obj (uri::uris)
-
projects / helm.git / blobdiff