- (* 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 []);
- lemmas
-
-let remove_coercion uri =
- try
- let (composites_in_db, composites_in_lib) =
- UriManager.UriHashtbl.find coercion_hashtbl uri
+ 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);