-(* given a new coercion uri from src to tgt returns
- * a list of (new coercion uri, coercion obj, universe graph)
- *)
-let close_coercion_graph src tgt uri =
- (* check if the coercion already exists *)
- let coercions = CoercDb.to_list () in
- let todo_list = get_closure_coercions src tgt uri coercions in
- let todo_list = filter_duplicates todo_list coercions in
- let new_coercions, new_coercions_obj =
- List.split (
- List.map (
- fun (src, l , tgt) ->
- match l with
- | [] -> assert false
- | he :: tl ->
- let first_step =
- Cic.Constant ("",
- Some (term_of_carr (CoercDb.Uri he)), Cic.Sort Cic.Prop, [], obj_attrs)
- in
- let o,u =
- List.fold_left (fun (o,univ) coer ->
- match o with
- | Cic.Constant (_,Some c,_,[],_) ->
- generate_composite_closure c (term_of_carr (CoercDb.Uri
- coer)) univ
- | _ -> assert false
- ) (first_step, CicUniv.empty_ugraph) tl
- in
- let name_src = CoercDb.name_of_carr src in
- let name_tgt = CoercDb.name_of_carr tgt in
- let name = name_tgt ^ "_of_" ^ name_src in
- let buri = UriManager.buri_of_uri uri in
- let c_uri =
- UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
- in
- let named_obj =
- match o with
- | Cic.Constant (_,bo,ty,vl,attrs) ->
- Cic.Constant (name,bo,ty,vl,attrs)
- | _ -> assert false
- in
- ((src,tgt,c_uri),(c_uri,named_obj,u))
- ) todo_list)
- in
- List.iter CoercDb.add_coercion (new_coercions @ [src,tgt,uri]);
- new_coercions_obj
-;;
-
-let coercion_hashtbl = UriManager.UriHashtbl.create 3
-
-let add_coercion ~basedir ~add_composites uri =
- let coer_ty,_ =
- CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri uri)
- CicUniv.empty_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
- *)
- let extract_last_two_p ty =
- let rec aux = function
- | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2))
- | Cic.Prod( _, src, tgt) -> src, tgt
- | _ -> assert false
- in
- aux ty
- in
- let ty_src,ty_tgt = extract_last_two_p coer_ty in
- let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
- let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
- let new_coercions = close_coercion_graph src_uri tgt_uri uri in
- let uris = ref [] in
- if add_composites then
- try
- let lemmas =
- List.fold_left
- (fun lemmas (uri,o,_) ->
- let lemmas' = LibrarySync.add_obj ~basedir uri o in
- uris := uri :: !uris;
- uri::lemmas'@lemmas
- ) [] new_coercions;
- in
- UriManager.UriHashtbl.add coercion_hashtbl uri !uris;
- lemmas
- with
- exn ->
- List.iter LibrarySync.remove_obj !uris;
- raise exn
- else
- []
-
-let remove_coercion uri =
- let uris =