open Printf;;
type coercion_search_result =
- | SomeCoercion of Cic.term
+ | SomeCoercion of Cic.term list
| NoCoercion
| NotMetaClosed
| NotHandled of string Lazy.t
(CoercDb.name_of_carr src)
(CoercDb.name_of_carr tgt)));
None
- | [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)));
- Some 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"
(List.length l)
(CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)
- (UriManager.name_of_uri u)));
- Some u
+ (CoercDb.name_of_carr tgt)));
+ Some l
in
(match uri with
None -> NoCoercion
- | Some u ->
- let c = CicUtil.term_of_uri u in
- let arity = arity_of c in
- let args = mk_implicits (arity - 1) in
- let newt =
- match args with
- [] -> c
- | _ -> Cic.Appl (c::args)
+ | Some ul ->
+ let cl = List.map CicUtil.term_of_uri ul in
+ let arityl = List.map arity_of cl in
+ let argsl = List.map (fun arity -> mk_implicits (arity - 1)) arityl in
+ let newtl =
+ List.map2
+ (fun args c ->
+ match args with
+ | [] -> c
+ | _ -> Cic.Appl (c::args))
+ argsl cl
in
- SomeCoercion newt)
+ SomeCoercion newtl)
with
| CoercDb.EqCarrNotImplemented s -> NotHandled s
| CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
in
let conclusion = " } \n" in
let data = List.fold_left
- (fun acc (src,tgt,c) ->
- acc ^ CoercDb.name_of_carr src ^ " -> " ^
- CoercDb.name_of_carr tgt ^ "[label=\"" ^ UriManager.name_of_uri c ^
- "\"];\n") "" l
+ (fun acc (src,tgt,cl) ->
+ List.fold_left
+ (fun acc c ->
+ acc ^ CoercDb.name_of_carr src ^ " -> " ^
+ CoercDb.name_of_carr tgt ^ "[label=\"" ^ UriManager.name_of_uri c ^
+ "\"];\n")
+ acc cl)
+ "" l
in
preamble ^ data ^ conclusion