(* searches a coercion fron src to tgt in the !coercions list *)
let look_for_coercion src tgt =
+ let arity_of con =
+ try
+ let ty,_ = CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in
+ let rec count_pi = function
+ | Cic.Prod (_,_,t) -> 1 + count_pi t
+ | _ -> 0
+ in
+ count_pi ty
+ with Invalid_argument _ -> assert false (* all coercions have an uri *)
+ in
+ let rec mk_implicits = function
+ | 0 -> []
+ | n -> Cic.Implicit None :: mk_implicits (n-1)
+ in
try
let l =
CoercDb.find_coercion
- (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt)
+ (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) in
+ let uri =
+ match l with
+ | [] ->
+ debug_print
+ (lazy
+ (sprintf ":-( coercion non trovata da %s a %s"
+ (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"
+ (List.length l)
+ (CoercDb.name_of_carr src)
+ (CoercDb.name_of_carr tgt)
+ (UriManager.name_of_uri u)));
+ Some u
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)
+ (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)
+ in
+ SomeCoercion newt)
with
| CoercDb.EqCarrNotImplemented s -> NotHandled s
| CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
CoercDb.term_of_carr (snd (CoercDb.get_carr uri))
with Invalid_argument _ -> assert false (* t must be a coercion *)
+let generate_dot_file () =
+ let l = CoercDb.to_list () in
+ let preamble = "
+ digraph pippo {
+ node [fontsize=9, width=.4, height=.4];
+ edge [fontsize=10];
+ \n"
+ 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
+ in
+ preamble ^ data ^ conclusion
+
(* EOF *)