-(* 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
-;;
-