- try
- let src = CicUtil.uri_of_term src in
- let tgt = CicUtil.uri_of_term tgt in
- let l =
- CoercDb.find_coercion
- (fun (s,t) -> UriManager.eq s src && UriManager.eq t tgt)
- in
- match l with
- | [] -> debug_print ":( coercion non trovata"; None
- | u::_ ->
- debug_print (
- sprintf ":) TROVATE %d coercion(s) da %s a %s, prendo la prima: %s"
- (List.length l)
- (UriManager.name_of_uri src)
- (UriManager.name_of_uri tgt)
- (UriManager.name_of_uri u));
- Some (CicUtil.term_of_uri u)
- with Invalid_argument s ->
- debug_print (":( coercion non trovata (fallita la uri_of_term): " ^ s);
- None
+ try
+ let l =
+ CoercDb.find_coercion
+ (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt)
+ in
+ match l with
+ | [] ->
+ 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"
+ (List.length l)
+ (CoercDb.name_of_carr src)
+ (CoercDb.name_of_carr tgt)
+ (UriManager.name_of_uri u)));
+ SomeCoercion (CicUtil.term_of_uri u)
+ with
+ | CoercDb.EqCarrNotImplemented s -> NotHandled s
+ | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed