(* $Id$ *)
-let object_declaration_hook = ref (fun _ _ -> ());;
-let set_object_declaration_hook f =
- object_declaration_hook := f
+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
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 (CoercDb.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 obj, ugraph, univlist =
try CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri
with CicEnvironment.Object_not_found _ -> assert false
try
(*3*)
let new_stuff = save_object_to_disk uri obj ugraph univlist in
- (* EXPERIMENTAL: pretty print the object in natural language *)
- (try !object_declaration_hook uri obj
- with exc ->
- prerr_endline ("Error: object_declaration_hook failed"^
- Printexc.to_string exc));
try
HLog.message
(Printf.sprintf "%s defined" (UriManager.string_of_uri uri))
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' ~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);
- (*CoercGraph.remove_coercion uri;*)
- ) uris_to_remove ;
- CicEnvironment.remove_obj uri
-
-(*** 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, _ = (CicEnvironment.get_obj CicUniv.oblivion_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 (_,_,_,_) -> true)
-
-let stack = ref [];;
-
-let h2l h =
- UriManager.UriHashtbl.fold
- (fun k v acc -> (k,v) :: acc) h []
-;;
-
-let push () =
- stack := (CoercDb.dump (), h2l coercion_hashtbl) :: !stack;
- remove_all_coercions ()
-;;
-
-let pop () =
- match !stack with
- | [] -> raise (Failure "Unable to POP from librarySync.ml")
- | (db,h) :: tl ->
- stack := tl;
- remove_all_coercions ();
- CoercDb.restore db;
- List.iter (fun (k,v) -> UriManager.UriHashtbl.add coercion_hashtbl k v)
- h
-;;
+ 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 saturations
- baseuri
+and
+ add_coercion ~add_composites ~pack_coercion_obj uri arity saturations baseuri
=
let coer_ty,_ =
let coer = CicUtil.term_of_uri uri in
in
aux ty
in
- let src_carr, tgt_carr =
+ let src_carr, tgt_carr, no_args =
let get_classes arity saturations l =
(* this is the ackerman's function revisited *)
let rec aux = function
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),
- match tgt with
- None -> assert false
- | Some `Funclass -> CoercDb.Fun arity
- | Some (`Class tgt) ->
- CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
+ 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 =
+ (fun u,_,_ ->
+ let bo, ty =
match obj with
- | Cic.Constant (_, Some bo, _, _, _) -> bo
- | _ -> assert false
+ | 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
- CoercDb.eq_carr s src_carr &&
- CoercDb.eq_carr t tgt_carr &&
- if fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo
- CicUniv.oblivion_ugraph)
- then true else
- (HLog.warn
+ 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))
+ 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, saturations);
- UriManager.UriHashtbl.add coercion_hashtbl 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 =
- List.filter (fun (s,t,u,_,obj,_) -> not(already_in_obj s t u obj))
+ 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
(* update the DB *)
- List.iter
- (fun (src,tgt,uri,saturations,_,_) ->
- CoercDb.add_coercion (src,tgt,uri,saturations))
- new_coercions;
- CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
- (* add the composites obj and they eventual lemmas *)
let lemmas =
- List.fold_left
- (fun acc (_,tgt,uri,saturations,obj,arity) ->
- add_single_obj uri obj refinement_toolkit;
- (uri,arity,saturations)::acc)
- [] new_coercions
+ 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
- (* 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,composite_uris);
- (*
- prerr_endline ("lemmas:");
- List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
- lemmas;
- prerr_endline ("lemmas END");*)
+ 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 -> HLog.warn "Coercion removal raise 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) ->
- let saturations = 0 in
- 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
- add_single_obj uri obj refinement_toolkit;
- let composites =
- if coercion then
- begin
-(*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
- (*CSC: I think there is a bug here. The composite coercions
- are not remembered in the .moo file. Thus they are re-generated
- every time. Right? *)
- let x =
- add_coercion ~add_composites:true refinement_toolkit uri arity
- saturations (UriManager.buri_of_uri uri)
- in
-(*prerr_endline ("are: ");
- List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
- prerr_endline "---";
-*)
- (*CSC: I throw the arity away. See comment above *)
- List.map (fun u,_,_ -> u) 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
- generate_sibling_mutual_definitions refinement_toolkit uri attrs name_to_avoid
-=
- function
- 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
- (add_single_obj uri obj refinement_toolkit;
- (n-1,uri::uris)))
- 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
- add_single_obj uri obj refinement_toolkit;
- (n-1,uri::uris)
- ) funs (List.length funs,[]))
- | _ -> assert false
-
-let add_obj refinement_toolkit uri obj =
- add_single_obj uri obj refinement_toolkit;
- let uris = ref [] in
- let not_debug = not (Helm_registry.get_bool "matita.debug") in
- try
- begin
- match obj with
- | Cic.Constant (name,Some bo,_,_,attrs) when
- List.mem (`Flavour `MutualDefinition) attrs ->
- uris :=
- !uris @
- generate_sibling_mutual_definitions refinement_toolkit uri attrs
- name bo
- | Cic.Constant _ -> ()
- | Cic.InductiveDefinition (inductivefuns,_,_,attrs) ->
- let _,inductive,_,_ = List.hd inductivefuns in
- if inductive then
- begin
- uris := !uris @
- generate_elimination_principles uri refinement_toolkit;
- uris := !uris @ generate_inversion refinement_toolkit uri obj;
- end ;
- 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 when not_debug ->
- 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)
-