(fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt)
in
match l with
- | [] -> debug_print (lazy ":( coercion non trovata"); NoCoercion
+ | [] ->
+ debug_print
+ (lazy
+ (sprintf ":-( coercion non trovata da %s a %s"
+ (CoercDb.name_of_carr src)
+ (CoercDb.name_of_carr tgt)));
+ NoCoercion
+ | [u] ->
+ debug_print (lazy (
+ sprintf ":-) TROVATA 1 coercion da %s a %s: %s"
+ (CoercDb.name_of_carr src)
+ (CoercDb.name_of_carr tgt)
+ (UriManager.name_of_uri u)));
+ SomeCoercion (CicUtil.term_of_uri u)
| u::_ ->
debug_print (lazy (
- sprintf ":) TROVATE %d coercion(s) da %s a %s, prendo la prima: %s"
+ sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s"
(List.length l)
(CoercDb.name_of_carr src)
(CoercDb.name_of_carr tgt)
* (source, list of coercions to follow, target)
*)
let get_closure_coercions src tgt uri coercions =
+ let eq_carr s t =
+ try
+ CoercDb.eq_carr s t
+ with
+ | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false
+ in
match src,tgt with
| CoercDb.Uri _, CoercDb.Uri _ ->
let c_from_tgt =
- List.filter (fun (f,_,_) -> CoercDb.eq_carr f tgt) coercions
+ List.filter (fun (f,_,_) -> eq_carr f tgt) coercions
in
let c_to_src =
- List.filter (fun (_,t,_) -> CoercDb.eq_carr t src) coercions
+ List.filter (fun (_,t,_) -> eq_carr t src) coercions
in
(List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @
(List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @